The bear visits the cat. The cat is young. The squirrel eats the cat. If someone eats the cat and the cat is not young then they visit the cat. If someone eats the cat and they see the cat then they eat the bear.
The bear visits the cat.
("bear" "visits" "cat" "+")
The cat is young.
("cat" "is" "young" "+")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
If someone eats the cat and the cat is not young then they visit the cat.
((("someone" "eats" "cat" "+") ("cat" "is" "young" "~")) -> ("someone" "visits" "cat" "+"))
If someone eats the cat and they see the cat then they eat the bear.
((("someone" "eats" "cat" "+") ("someone" "sees" "cat" "+")) -> ("someone" "eats" "bear" "+"))
The squirrel eats the cat.
True
1
proof
[(triple3)]
("squirrel" "eats" "cat" "+")
triple3
The cat is not young.
False
1
inv-proof
[(triple2)]
("cat" "is" "young" "-")
triple2
The cat does not visit the cat.
Unknown
inv-rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "visits" "cat" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
@0: The bear visits the cat.[(triple1)] The cat is young.[(triple2)] The squirrel eats the cat.[(triple3)]
The bear visits the cat.
("bear" "visits" "cat" "+")
triple1
The cat is young.
("cat" "is" "young" "+")
triple2
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple3