The dog is blue. The lion visits the mouse. The mouse does not need the lion. The squirrel is blue. If something visits the mouse and it is not cold then it visits the squirrel. If something needs the mouse and it is not round then the mouse is not blue.
The dog is blue.
("dog" "is" "blue" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse does not need the lion.
("mouse" "needs" "lion" "-")
The squirrel is blue.
("squirrel" "is" "blue" "+")
If something visits the mouse and it is not cold then it visits the squirrel.
((("something" "visits" "mouse" "+") ("something" "is" "cold" "~")) -> ("something" "visits" "squirrel" "+"))
If something needs the mouse and it is not round then the mouse is not blue.
((("something" "needs" "mouse" "+") ("something" "is" "round" "~")) -> ("mouse" "is" "blue" "-"))
The lion visits the mouse.
True
1
proof
[(triple2)]
("lion" "visits" "mouse" "+")
triple2
The squirrel is not blue.
False
1
inv-proof
[(triple4)]
("squirrel" "is" "blue" "-")
triple4
The dog does not visit the squirrel.
Unknown
inv-rconc
[@1: The dog visits the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "visits" "squirrel" "-")
The mouse needs the dog.
Unknown
random
[@0: The mouse needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "dog" "+")
@0: The dog is blue.[(triple1)] The lion visits the mouse.[(triple2)] The mouse does not need the lion.[(triple3)] The squirrel is blue.[(triple4)]
The dog is blue.
("dog" "is" "blue" "+")
triple1
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple2
The mouse does not need the lion.
("mouse" "needs" "lion" "-")
triple3
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple4