The dog visits the mouse. The mouse likes the dog. The squirrel is blue. The tiger eats the mouse. If someone visits the dog then the dog visits the squirrel. If someone is blue and they eat the mouse then they visit the mouse. If the squirrel eats the tiger then the tiger eats the squirrel. If the dog visits the squirrel and the squirrel eats the tiger then the tiger is young. If the tiger eats the squirrel and the tiger eats the dog then the dog is blue. If someone likes the dog then the dog visits the squirrel.
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
If someone visits the dog then the dog visits the squirrel.
((("someone" "visits" "dog" "+")) -> ("dog" "visits" "squirrel" "+"))
If someone is blue and they eat the mouse then they visit the mouse.
((("someone" "is" "blue" "+") ("someone" "eats" "mouse" "+")) -> ("someone" "visits" "mouse" "+"))
If the squirrel eats the tiger then the tiger eats the squirrel.
((("squirrel" "eats" "tiger" "+")) -> ("tiger" "eats" "squirrel" "+"))
If the dog visits the squirrel and the squirrel eats the tiger then the tiger is young.
((("dog" "visits" "squirrel" "+") ("squirrel" "eats" "tiger" "+")) -> ("tiger" "is" "young" "+"))
If the tiger eats the squirrel and the tiger eats the dog then the dog is blue.
((("tiger" "eats" "squirrel" "+") ("tiger" "eats" "dog" "+")) -> ("dog" "is" "blue" "+"))
If someone likes the dog then the dog visits the squirrel.
((("someone" "likes" "dog" "+")) -> ("dog" "visits" "squirrel" "+"))
The squirrel is blue.
True
1
proof
[(triple3)]
("squirrel" "is" "blue" "+")
triple3
The squirrel is not blue.
False
1
inv-proof
[(triple3)]
("squirrel" "is" "blue" "-")
triple3
The dog visits the squirrel.
True
2
proof
[(((triple2) -> rule6))]
("dog" "visits" "squirrel" "+")
((triple2) -> (rule6 % int1))
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int1
The dog does not visit the squirrel.
False
2
inv-proof
[(((triple2) -> rule6))]
("dog" "visits" "squirrel" "-")
((triple2) -> (rule6 % int1))
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int1
The tiger is not young.
Unknown
inv-rconc
[@1: The tiger is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "is" "young" "-")
The squirrel visits the mouse.
Unknown
rconc
[@1: The squirrel visits the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "visits" "mouse" "+")
The dog is not round.
Unknown
inv-random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
@0: The dog visits the mouse.[(triple1)] The mouse likes the dog.[(triple2)] The squirrel is blue.[(triple3)] The tiger eats the mouse.[(triple4)] @1: The dog visits the squirrel.[(((triple2) -> rule6))]
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple2
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple3
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple4
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
((triple2) -> (rule6 % int1))
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int1