The cat does not chase the cow. The cat does not eat the squirrel. The cat is nice. The cat is young. The cat needs the squirrel. The cow eats the squirrel. The cow does not need the squirrel. The squirrel chases the cat. The squirrel does not chase the cow. The squirrel does not eat the cat. The squirrel eats the cow. The squirrel needs the cat. If someone needs the cow and the cow is rough then the cow does not eat the cat. If the squirrel does not chase the cow then the cow is not young. All rough people are nice. If someone is red then they eat the cat. If someone is red then they chase the cat. If someone needs the squirrel and they are not blue then the squirrel eats the cat.
The cat does not chase the cow.
("cat" "chases" "cow" "-")
The cat does not eat the squirrel.
("cat" "eats" "squirrel" "-")
The cat is nice.
("cat" "is" "nice" "+")
The cat is young.
("cat" "is" "young" "+")
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
The cow does not need the squirrel.
("cow" "needs" "squirrel" "-")
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
The squirrel does not chase the cow.
("squirrel" "chases" "cow" "-")
The squirrel does not eat the cat.
("squirrel" "eats" "cat" "-")
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
If someone needs the cow and the cow is rough then the cow does not eat the cat.
((("someone" "needs" "cow" "+") ("cow" "is" "rough" "+")) -> ("cow" "eats" "cat" "-"))
If the squirrel does not chase the cow then the cow is not young.
((("squirrel" "chases" "cow" "~")) -> ("cow" "is" "young" "-"))
All rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If someone is red then they eat the cat.
((("someone" "is" "red" "+")) -> ("someone" "eats" "cat" "+"))
If someone is red then they chase the cat.
((("someone" "is" "red" "+")) -> ("someone" "chases" "cat" "+"))
If someone needs the squirrel and they are not blue then the squirrel eats the cat.
((("someone" "needs" "squirrel" "+") ("someone" "is" "blue" "~")) -> ("squirrel" "eats" "cat" "+"))
The squirrel chases the cat.
True
1
proof
[(triple8)]
("squirrel" "chases" "cat" "+")
triple8
The squirrel chases the cow.
False
1
inv-proof
[(triple9)]
("squirrel" "chases" "cow" "+")
triple9
The cat does not chase the cat.
Unknown
inv-rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "chases" "cat" "-")
The squirrel is red.
Unknown
random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "+")
@0: The cat does not chase the cow.[(triple1)] The cat does not eat the squirrel.[(triple2)] The cat is nice.[(triple3)] The cat is young.[(triple4)] The cat needs the squirrel.[(triple5)] The cow does not need the squirrel.[(triple7)] The cow eats the squirrel.[(triple6)] The squirrel chases the cat.[(triple8)] The squirrel does not chase the cow.[(triple9)] The squirrel does not eat the cat.[(triple10)] The squirrel eats the cow.[(triple11)] The squirrel needs the cat.[(triple12)] @1: The cow is not young.[(((triple9) -> rule2))]
The cat does not chase the cow.
("cat" "chases" "cow" "-")
triple1
The cat does not eat the squirrel.
("cat" "eats" "squirrel" "-")
triple2
The cat is nice.
("cat" "is" "nice" "+")
triple3
The cat is young.
("cat" "is" "young" "+")
triple4
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
triple5
The cow does not need the squirrel.
("cow" "needs" "squirrel" "-")
triple7
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
triple6
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
triple8
The squirrel does not chase the cow.
("squirrel" "chases" "cow" "-")
triple9
The squirrel does not eat the cat.
("squirrel" "eats" "cat" "-")
triple10
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
triple11
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple12
The cow is not young.
("cow" "is" "young" "-")
((triple9) -> (rule2 % int1))
The cow is not young.
("cow" "is" "young" "-")
int1