The bear chases the cat. The cat chases the bear. The squirrel eats the cat. If something eats the cat then it eats the squirrel. If the bear sees the cat and the cat eats the bear then the cat sees the squirrel.
The bear chases the cat.
("bear" "chases" "cat" "+")
The cat chases the bear.
("cat" "chases" "bear" "+")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
If something eats the cat then it eats the squirrel.
((("something" "eats" "cat" "+")) -> ("something" "eats" "squirrel" "+"))
If the bear sees the cat and the cat eats the bear then the cat sees the squirrel.
((("bear" "sees" "cat" "+") ("cat" "eats" "bear" "+")) -> ("cat" "sees" "squirrel" "+"))
The cat chases the bear.
True
1
proof
[(triple2)]
("cat" "chases" "bear" "+")
triple2
The squirrel does not eat the cat.
False
1
inv-proof
[(triple3)]
("squirrel" "eats" "cat" "-")
triple3
The cat does not eat the squirrel.
Unknown
inv-rconc
[@1: The cat eats the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "eats" "squirrel" "-")
The bear chases the bear.
Unknown
random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "+")
@0: The bear chases the cat.[(triple1)] The cat chases the bear.[(triple2)] The squirrel eats the cat.[(triple3)] @1: The squirrel eats the squirrel.[(((triple3) -> rule1))]
The bear chases the cat.
("bear" "chases" "cat" "+")
triple1
The cat chases the bear.
("cat" "chases" "bear" "+")
triple2
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple3
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
((triple3) -> (rule1 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1