The cat chases the cow. The cat chases the squirrel. The cow chases the cat. The cow chases the squirrel. The squirrel chases the cat. The squirrel eats the cat. The squirrel is green. If something eats the squirrel and the squirrel is green then it likes the squirrel. If something likes the cat then the cat chases the cow. If something chases the cow then it eats the cat. If something eats the cow then it is kind. If something chases the cow and the cow eats the squirrel then the squirrel is cold. If something is red and it eats the cat then it is cold.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
The cow chases the cat.
("cow" "chases" "cat" "+")
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
If something eats the squirrel and the squirrel is green then it likes the squirrel.
((("something" "eats" "squirrel" "+") ("squirrel" "is" "green" "+")) -> ("something" "likes" "squirrel" "+"))
If something likes the cat then the cat chases the cow.
((("something" "likes" "cat" "+")) -> ("cat" "chases" "cow" "+"))
If something chases the cow then it eats the cat.
((("something" "chases" "cow" "+")) -> ("something" "eats" "cat" "+"))
If something eats the cow then it is kind.
((("something" "eats" "cow" "+")) -> ("something" "is" "kind" "+"))
If something chases the cow and the cow eats the squirrel then the squirrel is cold.
((("something" "chases" "cow" "+") ("cow" "eats" "squirrel" "+")) -> ("squirrel" "is" "cold" "+"))
If something is red and it eats the cat then it is cold.
((("something" "is" "red" "+") ("something" "eats" "cat" "+")) -> ("something" "is" "cold" "+"))
The cow chases the cat.
True
1
proof
[(triple3)]
("cow" "chases" "cat" "+")
triple3
The squirrel does not chase the cat.
False
1
inv-proof
[(triple5)]
("squirrel" "chases" "cat" "-")
triple5
The cat is not cold.
Unknown
inv-rconc
[@1: The cat is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "is" "cold" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
@0: The cat chases the cow.[(triple1)] The cat chases the squirrel.[(triple2)] The cow chases the cat.[(triple3)] The cow chases the squirrel.[(triple4)] The squirrel chases the cat.[(triple5)] The squirrel eats the cat.[(triple6)] The squirrel is green.[(triple7)] @1: The cat eats the cat.[(((triple1) -> rule3))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
triple2
The cow chases the cat.
("cow" "chases" "cat" "+")
triple3
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
triple4
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
triple5
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple6
The squirrel is green.
("squirrel" "is" "green" "+")
triple7
The cat eats the cat.
("cat" "eats" "cat" "+")
((triple1) -> (rule3 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1