The cat eats the tiger. The cat is round. The cat is young. The cat likes the mouse. The mouse eats the squirrel. The mouse is blue. The mouse is red. The squirrel likes the cat. The squirrel likes the mouse. The squirrel visits the tiger. The tiger eats the cat. The tiger eats the squirrel. The tiger is red. The tiger is young. The tiger visits the cat. If someone is young then they eat the cat. If someone likes the squirrel and the squirrel eats the cat then the squirrel eats the tiger. If someone eats the squirrel and they are cold then they like the mouse. If someone eats the cat and they eat the squirrel then they eat the mouse. If someone visits the cat then the cat visits the squirrel. If the squirrel is round and the squirrel is cold then the squirrel is young. If the squirrel visits the cat and the squirrel visits the mouse then the squirrel is red. If someone is cold and they visit the squirrel then they like the tiger.
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat is round.
("cat" "is" "round" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is red.
("mouse" "is" "red" "+")
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If someone is young then they eat the cat.
((("someone" "is" "young" "+")) -> ("someone" "eats" "cat" "+"))
If someone likes the squirrel and the squirrel eats the cat then the squirrel eats the tiger.
((("someone" "likes" "squirrel" "+") ("squirrel" "eats" "cat" "+")) -> ("squirrel" "eats" "tiger" "+"))
If someone eats the squirrel and they are cold then they like the mouse.
((("someone" "eats" "squirrel" "+") ("someone" "is" "cold" "+")) -> ("someone" "likes" "mouse" "+"))
If someone eats the cat and they eat the squirrel then they eat the mouse.
((("someone" "eats" "cat" "+") ("someone" "eats" "squirrel" "+")) -> ("someone" "eats" "mouse" "+"))
If someone visits the cat then the cat visits the squirrel.
((("someone" "visits" "cat" "+")) -> ("cat" "visits" "squirrel" "+"))
If the squirrel is round and the squirrel is cold then the squirrel is young.
((("squirrel" "is" "round" "+") ("squirrel" "is" "cold" "+")) -> ("squirrel" "is" "young" "+"))
If the squirrel visits the cat and the squirrel visits the mouse then the squirrel is red.
((("squirrel" "visits" "cat" "+") ("squirrel" "visits" "mouse" "+")) -> ("squirrel" "is" "red" "+"))
If someone is cold and they visit the squirrel then they like the tiger.
((("someone" "is" "cold" "+") ("someone" "visits" "squirrel" "+")) -> ("someone" "likes" "tiger" "+"))
The tiger visits the cat.
True
1
proof
[(triple15)]
("tiger" "visits" "cat" "+")
triple15
The cat is not round.
False
1
inv-proof
[(triple2)]
("cat" "is" "round" "-")
triple2
The tiger eats the mouse.
True
3
proof
[(((triple11 triple12) -> rule4) OR ((((triple14) -> rule1) triple12) -> rule4))]
("tiger" "eats" "mouse" "+")
((triple11 triple12) -> (rule4 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
((((triple14) -> (rule1 % int2)) triple12) -> (rule4 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int2
The cat does not visit the squirrel.
False
2
inv-proof
[(((triple15) -> rule5))]
("cat" "visits" "squirrel" "-")
((triple15) -> (rule5 % int1))
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int1
The cat does not eat the mouse.
Unknown
inv-rconc
[@1: The cat eats the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "eats" "mouse" "-")
The tiger likes the mouse.
Unknown
rconc
[@1: The tiger likes the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "likes" "mouse" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
@0: The cat eats the tiger.[(triple1)] The cat is round.[(triple2)] The cat is young.[(triple3)] The cat likes the mouse.[(triple4)] The mouse eats the squirrel.[(triple5)] The mouse is blue.[(triple6)] The mouse is red.[(triple7)] The squirrel likes the cat.[(triple8)] The squirrel likes the mouse.[(triple9)] The squirrel visits the tiger.[(triple10)] The tiger eats the cat.[(triple11 OR ((triple14) -> rule1))] The tiger eats the squirrel.[(triple12)] The tiger is red.[(triple13)] The tiger is young.[(triple14)] The tiger visits the cat.[(triple15)] @1: The cat eats the cat.[(((triple3) -> rule1))] The cat visits the squirrel.[(((triple15) -> rule5))] The tiger eats the mouse.[(((triple11 triple12) -> rule4) OR ((((triple14) -> rule1) triple12) -> rule4))]
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple1
The cat is round.
("cat" "is" "round" "+")
triple2
The cat is young.
("cat" "is" "young" "+")
triple3
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple4
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple5
The mouse is blue.
("mouse" "is" "blue" "+")
triple6
The mouse is red.
("mouse" "is" "red" "+")
triple7
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
triple8
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple9
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple10
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple11
((triple14) -> (rule1 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
triple12
The tiger is red.
("tiger" "is" "red" "+")
triple13
The tiger is young.
("tiger" "is" "young" "+")
triple14
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple15
The cat eats the cat.
("cat" "eats" "cat" "+")
((triple3) -> (rule1 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
((triple15) -> (rule5 % int1))
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
((triple11 triple12) -> (rule4 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
((((triple14) -> (rule1 % int2)) triple12) -> (rule4 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int2