The cat visits the mouse. The mouse is round. The squirrel visits the cat. The tiger sees the cat. If the mouse visits the cat and the mouse is cold then the mouse is young. If something is young then it sees the squirrel.
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The mouse is round.
("mouse" "is" "round" "+")
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
If the mouse visits the cat and the mouse is cold then the mouse is young.
((("mouse" "visits" "cat" "+") ("mouse" "is" "cold" "+")) -> ("mouse" "is" "young" "+"))
If something is young then it sees the squirrel.
((("something" "is" "young" "+")) -> ("something" "sees" "squirrel" "+"))
The squirrel visits the cat.
True
1
proof
[(triple3)]
("squirrel" "visits" "cat" "+")
triple3
The cat does not visit the mouse.
False
1
inv-proof
[(triple1)]
("cat" "visits" "mouse" "-")
triple1
The squirrel does not see the squirrel.
Unknown
inv-rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "sees" "squirrel" "-")
The tiger likes the squirrel.
Unknown
random
[@0: The tiger likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "squirrel" "+")
@0: The cat visits the mouse.[(triple1)] The mouse is round.[(triple2)] The squirrel visits the cat.[(triple3)] The tiger sees the cat.[(triple4)]
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple1
The mouse is round.
("mouse" "is" "round" "+")
triple2
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
triple3
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple4