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