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