The mouse likes the tiger. The mouse visits the tiger. The tiger visits the mouse. If the mouse is red and the mouse is rough then the mouse visits the tiger. If the mouse likes the tiger then the mouse is rough. If someone visits the mouse then the mouse eats the tiger.
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If the mouse is red and the mouse is rough then the mouse visits the tiger.
((("mouse" "is" "red" "+") ("mouse" "is" "rough" "+")) -> ("mouse" "visits" "tiger" "+"))
If the mouse likes the tiger then the mouse is rough.
((("mouse" "likes" "tiger" "+")) -> ("mouse" "is" "rough" "+"))
If someone visits the mouse then the mouse eats the tiger.
((("someone" "visits" "mouse" "+")) -> ("mouse" "eats" "tiger" "+"))
The mouse visits the tiger.
True
1
proof
[(triple2)]
("mouse" "visits" "tiger" "+")
triple2
The tiger does not visit the mouse.
False
1
inv-proof
[(triple3)]
("tiger" "visits" "mouse" "-")
triple3
The mouse is rough.
True
2
proof
[(((triple1) -> rule2))]
("mouse" "is" "rough" "+")
((triple1) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is not rough.
False
2
inv-proof
[(((triple1) -> rule2))]
("mouse" "is" "rough" "-")
((triple1) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The tiger is not green.
Unknown
inv-random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
The tiger does not like the mouse.
Unknown
inv-random
[@0: The tiger likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "mouse" "-")
The tiger is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
@0: The mouse likes the tiger.[(triple1)] The mouse visits the tiger.[(triple2)] The tiger visits the mouse.[(triple3)] @1: The mouse eats the tiger.[(((triple3) -> rule3))] The mouse is rough.[(((triple1) -> rule2))]
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple2
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple3
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
((triple3) -> (rule3 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
((triple1) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1