The cat likes the cow. The cow is nice. The squirrel is red. If the cow needs the cat and the cow likes the cat then the cat visits the cow. If someone needs the cat then the cat needs the cow. If someone needs the cow then the cow needs the squirrel. If someone is red then they need the cat. If someone likes the cat and the cat likes the squirrel then they like the cow. If someone is red and blue then they like the cow. If someone likes the cow and the cow is round then they need the squirrel. If someone needs the cat then they are nice.
The cat likes the cow.
("cat" "likes" "cow" "+")
The cow is nice.
("cow" "is" "nice" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
If the cow needs the cat and the cow likes the cat then the cat visits the cow.
((("cow" "needs" "cat" "+") ("cow" "likes" "cat" "+")) -> ("cat" "visits" "cow" "+"))
If someone needs the cat then the cat needs the cow.
((("someone" "needs" "cat" "+")) -> ("cat" "needs" "cow" "+"))
If someone needs the cow then the cow needs the squirrel.
((("someone" "needs" "cow" "+")) -> ("cow" "needs" "squirrel" "+"))
If someone is red then they need the cat.
((("someone" "is" "red" "+")) -> ("someone" "needs" "cat" "+"))
If someone likes the cat and the cat likes the squirrel then they like the cow.
((("someone" "likes" "cat" "+") ("cat" "likes" "squirrel" "+")) -> ("someone" "likes" "cow" "+"))
If someone is red and blue then they like the cow.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "likes" "cow" "+"))
If someone likes the cow and the cow is round then they need the squirrel.
((("someone" "likes" "cow" "+") ("cow" "is" "round" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone needs the cat then they are nice.
((("someone" "needs" "cat" "+")) -> ("someone" "is" "nice" "+"))
The cat likes the cow.
True
1
proof
[(triple1)]
("cat" "likes" "cow" "+")
triple1
The cow is not nice.
False
1
inv-proof
[(triple2)]
("cow" "is" "nice" "-")
triple2
The squirrel needs the cat.
True
2
proof
[(((triple3) -> rule4))]
("squirrel" "needs" "cat" "+")
((triple3) -> (rule4 % int1))
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int1
The squirrel does not need the cat.
False
2
inv-proof
[(((triple3) -> rule4))]
("squirrel" "needs" "cat" "-")
((triple3) -> (rule4 % int1))
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int1
The cat needs the cow.
True
3
proof
[(((((triple3) -> rule4)) -> rule2))]
("cat" "needs" "cow" "+")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int2
The cat does not need the cow.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule2))]
("cat" "needs" "cow" "-")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int2
The cow needs the squirrel.
True
4
proof
[(((((((triple3) -> rule4)) -> rule2)) -> rule3))]
("cow" "needs" "squirrel" "+")
((((((triple3) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
int2
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int3
The cow does not need the squirrel.
False
4
inv-proof
[(((((((triple3) -> rule4)) -> rule2)) -> rule3))]
("cow" "needs" "squirrel" "-")
((((((triple3) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
int2
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int3
The squirrel does not like the cow.
Unknown
inv-rconc
[@1: The squirrel likes the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "likes" "cow" "-")
The cat needs the cat.
Unknown
rconc
[@1: The cat needs the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "needs" "cat" "+")
The cat does not need the squirrel.
Unknown
inv-rconc
[@1: The cat needs the squirrel.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "needs" "squirrel" "-")
The cat is nice.
Unknown
rconc
[@2: The cat is nice.[CWA. Example of deepest failure = (rule8 <- rule4 <- FAIL)]]
("cat" "is" "nice" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The cow visits the cat.
Unknown
random
[@0: The cow visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cat" "+")
The cat is not red.
Unknown
inv-random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "-")
The cat is green.
Unknown
random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "+")
@0: The cat likes the cow.[(triple1)] The cow is nice.[(triple2)] The squirrel is red.[(triple3)] @1: The squirrel needs the cat.[(((triple3) -> rule4))] @2: The cat needs the cow.[(((((triple3) -> rule4)) -> rule2))] The squirrel is nice.[(((((triple3) -> rule4)) -> rule8))] @3: The cow needs the squirrel.[(((((((triple3) -> rule4)) -> rule2)) -> rule3))]
The cat likes the cow.
("cat" "likes" "cow" "+")
triple1
The cow is nice.
("cow" "is" "nice" "+")
triple2
The squirrel is red.
("squirrel" "is" "red" "+")
triple3
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
((triple3) -> (rule4 % int1))
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
((((triple3) -> (rule4 % int2))) -> (rule8 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int2
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
((((((triple3) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
int2
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int3