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