The dog visits the mouse. The mouse visits the dog. The mouse visits the tiger. The tiger eats the dog. The tiger is blue. The tiger needs the dog. The tiger needs the mouse. If the mouse visits the tiger and the mouse is big then the tiger eats the mouse. If something is big then it visits the tiger. If something needs the mouse then the mouse is red.
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger eats the dog.
("tiger" "eats" "dog" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
If the mouse visits the tiger and the mouse is big then the tiger eats the mouse.
((("mouse" "visits" "tiger" "+") ("mouse" "is" "big" "+")) -> ("tiger" "eats" "mouse" "+"))
If something is big then it visits the tiger.
((("something" "is" "big" "+")) -> ("something" "visits" "tiger" "+"))
If something needs the mouse then the mouse is red.
((("something" "needs" "mouse" "+")) -> ("mouse" "is" "red" "+"))
The dog visits the mouse.
True
1
proof
[(triple1)]
("dog" "visits" "mouse" "+")
triple1
The tiger does not eat the dog.
False
1
inv-proof
[(triple4)]
("tiger" "eats" "dog" "-")
triple4
The dog does not visit the tiger.
Unknown
inv-rconc
[@1: The dog visits the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "visits" "tiger" "-")
The mouse eats the tiger.
Unknown
random
[@0: The mouse eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "tiger" "+")
@0: The dog visits the mouse.[(triple1)] The mouse visits the dog.[(triple2)] The mouse visits the tiger.[(triple3)] The tiger eats the dog.[(triple4)] The tiger is blue.[(triple5)] The tiger needs the dog.[(triple6)] The tiger needs the mouse.[(triple7)] @1: The mouse is red.[(((triple7) -> rule3))]
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple3
The tiger eats the dog.
("tiger" "eats" "dog" "+")
triple4
The tiger is blue.
("tiger" "is" "blue" "+")
triple5
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple6
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple7
The mouse is red.
("mouse" "is" "red" "+")
((triple7) -> (rule3 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1