The dog visits the mouse. The mouse visits the dog. If something visits the dog and it chases the mouse then the mouse visits the dog. If something chases the mouse then the mouse needs the dog. If the mouse visits the dog then the dog needs the mouse. If something is rough and it chases the dog then it visits the mouse. If the mouse is cold and the mouse is round then the mouse is rough. If something is young then it needs the dog.
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
If something visits the dog and it chases the mouse then the mouse visits the dog.
((("something" "visits" "dog" "+") ("something" "chases" "mouse" "+")) -> ("mouse" "visits" "dog" "+"))
If something chases the mouse then the mouse needs the dog.
((("something" "chases" "mouse" "+")) -> ("mouse" "needs" "dog" "+"))
If the mouse visits the dog then the dog needs the mouse.
((("mouse" "visits" "dog" "+")) -> ("dog" "needs" "mouse" "+"))
If something is rough and it chases the dog then it visits the mouse.
((("something" "is" "rough" "+") ("something" "chases" "dog" "+")) -> ("something" "visits" "mouse" "+"))
If the mouse is cold and the mouse is round then the mouse is rough.
((("mouse" "is" "cold" "+") ("mouse" "is" "round" "+")) -> ("mouse" "is" "rough" "+"))
If something is young then it needs the dog.
((("something" "is" "young" "+")) -> ("something" "needs" "dog" "+"))
The dog visits the mouse.
True
1
proof
[(triple1)]
("dog" "visits" "mouse" "+")
triple1
The mouse does not visit the dog.
False
1
inv-proof
[(triple2)]
("mouse" "visits" "dog" "-")
triple2
The dog needs the mouse.
True
2
proof
[(((triple2) -> rule3))]
("dog" "needs" "mouse" "+")
((triple2) -> (rule3 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The dog does not need the mouse.
False
2
inv-proof
[(((triple2) -> rule3))]
("dog" "needs" "mouse" "-")
((triple2) -> (rule3 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The mouse is not rough.
Unknown
inv-rconc
[@1: The mouse is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "rough" "-")
The mouse needs the dog.
Unknown
rconc
[@1: The mouse needs the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "needs" "dog" "+")
The mouse is not cold.
Unknown
inv-random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "-")
The dog is cold.
Unknown
random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "+")
@0: The dog visits the mouse.[(triple1)] The mouse visits the dog.[(triple2)] @1: The dog needs the mouse.[(((triple2) -> rule3))]
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
((triple2) -> (rule3 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1