The cat eats the tiger. The cat sees the tiger. The rabbit chases the cat. The rabbit is round. The rabbit sees the cat. The tiger chases the cat. The tiger is nice. If something is nice then it eats the rabbit. If something is rough then it eats the rabbit. If something sees the cat then it does not eat the cat. Young things are nice. If something is rough and it chases the cat then the cat sees the tiger. If something chases the tiger and it eats the tiger then the tiger is not nice.
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
If something is nice then it eats the rabbit.
((("something" "is" "nice" "+")) -> ("something" "eats" "rabbit" "+"))
If something is rough then it eats the rabbit.
((("something" "is" "rough" "+")) -> ("something" "eats" "rabbit" "+"))
If something sees the cat then it does not eat the cat.
((("something" "sees" "cat" "+")) -> ("something" "eats" "cat" "-"))
Young things are nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If something is rough and it chases the cat then the cat sees the tiger.
((("something" "is" "rough" "+") ("something" "chases" "cat" "+")) -> ("cat" "sees" "tiger" "+"))
If something chases the tiger and it eats the tiger then the tiger is not nice.
((("something" "chases" "tiger" "+") ("something" "eats" "tiger" "+")) -> ("tiger" "is" "nice" "-"))
The tiger is nice.
True
1
proof
[(triple7)]
("tiger" "is" "nice" "+")
triple7
The tiger does not chase the cat.
False
1
inv-proof
[(triple6)]
("tiger" "chases" "cat" "-")
triple6
The tiger eats the rabbit.
True
2
proof
[(((triple7) -> rule1))]
("tiger" "eats" "rabbit" "+")
((triple7) -> (rule1 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The tiger does not eat the rabbit.
False
2
inv-proof
[(((triple7) -> rule1))]
("tiger" "eats" "rabbit" "-")
((triple7) -> (rule1 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The rabbit is not nice.
Unknown
inv-rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "is" "nice" "-")
The cat is nice.
Unknown
rconc
[@1: The cat is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "is" "nice" "+")
The tiger does not chase the rabbit.
Unknown
inv-random
[@0: The tiger chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "rabbit" "-")
The rabbit eats the tiger.
Unknown
random
[@0: The rabbit eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "tiger" "+")
@0: The cat eats the tiger.[(triple1)] The cat sees the tiger.[(triple2)] The rabbit chases the cat.[(triple3)] The rabbit is round.[(triple4)] The rabbit sees the cat.[(triple5)] The tiger chases the cat.[(triple6)] The tiger is nice.[(triple7)] @1: The rabbit does not eat the cat.[(((triple5) -> rule3))] The tiger eats the rabbit.[(((triple7) -> rule1))]
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple2
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple3
The rabbit is round.
("rabbit" "is" "round" "+")
triple4
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple5
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple6
The tiger is nice.
("tiger" "is" "nice" "+")
triple7
The rabbit does not eat the cat.
("rabbit" "eats" "cat" "-")
((triple5) -> (rule3 % int1))
The rabbit does not eat the cat.
("rabbit" "eats" "cat" "-")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
((triple7) -> (rule1 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1