The cat eats the cow. The cat eats the squirrel. The cat is rough. The cat is round. The cat likes the squirrel. The cat visits the cow. The cow likes the squirrel. The cow visits the squirrel. The squirrel eats the cow. The squirrel likes the cat. The squirrel visits the cat. The squirrel visits the cow. If something eats the cow then the cow likes the cat. If something likes the squirrel and it likes the cat then the squirrel eats the cat. If something eats the cow then it likes the cow. If the squirrel visits the cat then the squirrel eats the cow. If something likes the squirrel and the squirrel eats the cow then the squirrel visits the cat. If something is round then it eats the cow.
The cat eats the cow.
("cat" "eats" "cow" "+")
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is round.
("cat" "is" "round" "+")
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
If something eats the cow then the cow likes the cat.
((("something" "eats" "cow" "+")) -> ("cow" "likes" "cat" "+"))
If something likes the squirrel and it likes the cat then the squirrel eats the cat.
((("something" "likes" "squirrel" "+") ("something" "likes" "cat" "+")) -> ("squirrel" "eats" "cat" "+"))
If something eats the cow then it likes the cow.
((("something" "eats" "cow" "+")) -> ("something" "likes" "cow" "+"))
If the squirrel visits the cat then the squirrel eats the cow.
((("squirrel" "visits" "cat" "+")) -> ("squirrel" "eats" "cow" "+"))
If something likes the squirrel and the squirrel eats the cow then the squirrel visits the cat.
((("something" "likes" "squirrel" "+") ("squirrel" "eats" "cow" "+")) -> ("squirrel" "visits" "cat" "+"))
If something is round then it eats the cow.
((("something" "is" "round" "+")) -> ("something" "eats" "cow" "+"))
The squirrel visits the cow.
True
1
proof
[(triple12)]
("squirrel" "visits" "cow" "+")
triple12
The cat is not round.
False
1
inv-proof
[(triple4)]
("cat" "is" "round" "-")
triple4
The cat likes the cow.
True
2
proof
[(((triple1) -> rule3) OR ((((triple4) -> rule6)) -> rule3))]
("cat" "likes" "cow" "+")
((triple1) -> (rule3 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule3 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
int2
The squirrel does not like the cow.
False
2
inv-proof
[(((triple9) -> rule3) OR ((((triple11) -> rule4)) -> rule3))]
("squirrel" "likes" "cow" "-")
((triple9) -> (rule3 % int1))
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int1
((((triple11) -> (rule4 % int2))) -> (rule3 % int1))
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int1
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int2
The squirrel eats the cat.
True
4
proof
[(((triple7 ((triple1) -> rule1)) -> rule2) OR ((triple7 ((triple9) -> rule1)) -> rule2) OR ((triple7 ((((triple11) -> rule4)) -> rule1)) -> rule2) OR ((triple7 ((((triple4) -> rule6)) -> rule1)) -> rule2))]
("squirrel" "eats" "cat" "+")
((triple7 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
int2
((triple7 ((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
int2
((triple7 ((((triple11) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
int2
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int3
((triple7 ((((triple4) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
int2
The cat eats the cow.
("cat" "eats" "cow" "+")
int3
The squirrel does not eat the cat.
False
4
inv-proof
[(((triple7 ((triple1) -> rule1)) -> rule2) OR ((triple7 ((triple9) -> rule1)) -> rule2) OR ((triple7 ((((triple11) -> rule4)) -> rule1)) -> rule2) OR ((triple7 ((((triple4) -> rule6)) -> rule1)) -> rule2))]
("squirrel" "eats" "cat" "-")
((triple7 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
int2
((triple7 ((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
int2
((triple7 ((((triple11) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
int2
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int3
((triple7 ((((triple4) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
int2
The cat eats the cow.
("cat" "eats" "cow" "+")
int3
The cow does not like the cow.
Unknown
inv-rconc
[@2: The cow likes the cow.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("cow" "likes" "cow" "-")
The cow eats the cow.
Unknown
rconc
[@1: The cow eats the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "eats" "cow" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The squirrel is rough.
Unknown
random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "+")
The cow does not visit the cat.
Unknown
inv-random
[@0: The cow visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cat" "-")
The cat is red.
Unknown
random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "+")
@0: The cat eats the cow.[(triple1 OR ((triple4) -> rule6))] The cat eats the squirrel.[(triple2)] The cat is rough.[(triple3)] The cat is round.[(triple4)] The cat likes the squirrel.[(triple5)] The cat visits the cow.[(triple6)] The cow likes the squirrel.[(triple7)] The cow visits the squirrel.[(triple8)] The squirrel eats the cow.[(triple9 OR ((triple11) -> rule4))] The squirrel likes the cat.[(triple10)] The squirrel visits the cat.[(triple11 OR ((triple5 triple9) -> rule5) OR ((triple7 triple9) -> rule5))] The squirrel visits the cow.[(triple12)] @1: The cat likes the cow.[(((triple1) -> rule3) OR ((((triple4) -> rule6)) -> rule3))] The cow likes the cat.[(((triple1) -> rule1) OR ((triple9) -> rule1) OR ((((triple11) -> rule4)) -> rule1) OR ((((triple4) -> rule6)) -> rule1))] The squirrel likes the cow.[(((triple9) -> rule3) OR ((((triple11) -> rule4)) -> rule3))] @2: The squirrel eats the cat.[(((triple7 ((triple1) -> rule1)) -> rule2) OR ((triple7 ((triple9) -> rule1)) -> rule2) OR ((triple7 ((((triple11) -> rule4)) -> rule1)) -> rule2) OR ((triple7 ((((triple4) -> rule6)) -> rule1)) -> rule2))]
The cat eats the cow.
("cat" "eats" "cow" "+")
triple1
((triple4) -> (rule6 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
triple2
The cat is rough.
("cat" "is" "rough" "+")
triple3
The cat is round.
("cat" "is" "round" "+")
triple4
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple5
The cat visits the cow.
("cat" "visits" "cow" "+")
triple6
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
triple7
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
triple8
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
triple9
((triple11) -> (rule4 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
triple10
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
triple11
((triple5 triple9) -> (rule5 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
((triple7 triple9) -> (rule5 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple12
The cat likes the cow.
("cat" "likes" "cow" "+")
((triple1) -> (rule3 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule3 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
int2
The cow likes the cat.
("cow" "likes" "cat" "+")
((triple1) -> (rule1 % int1))
The cow likes the cat.
("cow" "likes" "cat" "+")
int1
((triple9) -> (rule1 % int1))
The cow likes the cat.
("cow" "likes" "cat" "+")
int1
((((triple11) -> (rule4 % int2))) -> (rule1 % int1))
The cow likes the cat.
("cow" "likes" "cat" "+")
int1
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int2
((((triple4) -> (rule6 % int2))) -> (rule1 % int1))
The cow likes the cat.
("cow" "likes" "cat" "+")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
int2
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
((triple9) -> (rule3 % int1))
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int1
((((triple11) -> (rule4 % int2))) -> (rule3 % int1))
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int1
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int2
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
((triple7 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
int2
((triple7 ((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
int2
((triple7 ((((triple11) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
int2
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int3
((triple7 ((((triple4) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
int2
The cat eats the cow.
("cat" "eats" "cow" "+")
int3