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