The mouse is blue. The mouse is red. The mouse visits the tiger. The tiger is red. The tiger likes the mouse. The tiger sees the mouse. The tiger visits the mouse. If someone visits the tiger and the tiger visits the mouse then the mouse is green. If someone sees the mouse and the mouse visits the tiger then the mouse is green. If the mouse visits the tiger then the tiger visits the mouse.
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If someone visits the tiger and the tiger visits the mouse then the mouse is green.
((("someone" "visits" "tiger" "+") ("tiger" "visits" "mouse" "+")) -> ("mouse" "is" "green" "+"))
If someone sees the mouse and the mouse visits the tiger then the mouse is green.
((("someone" "sees" "mouse" "+") ("mouse" "visits" "tiger" "+")) -> ("mouse" "is" "green" "+"))
If the mouse visits the tiger then the tiger visits the mouse.
((("mouse" "visits" "tiger" "+")) -> ("tiger" "visits" "mouse" "+"))
The tiger likes the mouse.
True
1
proof
[(triple5)]
("tiger" "likes" "mouse" "+")
triple5
The tiger does not visit the mouse.
False
1
inv-proof
[(triple7 OR ((triple3) -> rule3))]
("tiger" "visits" "mouse" "-")
triple7
((triple3) -> (rule3 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The mouse is green.
True
3
proof
[(((triple3 triple7) -> rule1) OR ((triple6 triple3) -> rule2) OR ((triple3 ((triple3) -> rule3)) -> rule1))]
("mouse" "is" "green" "+")
((triple3 triple7) -> (rule1 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
((triple6 triple3) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
((triple3 ((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2
The mouse is not green.
False
3
inv-proof
[(((triple3 triple7) -> rule1) OR ((triple6 triple3) -> rule2) OR ((triple3 ((triple3) -> rule3)) -> rule1))]
("mouse" "is" "green" "-")
((triple3 triple7) -> (rule1 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
((triple6 triple3) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
((triple3 ((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2
The tiger is not rough.
Unknown
inv-random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "-")
The tiger is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
The mouse is not rough.
Unknown
inv-random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The mouse is blue.[(triple1)] The mouse is red.[(triple2)] The mouse visits the tiger.[(triple3)] The tiger is red.[(triple4)] The tiger likes the mouse.[(triple5)] The tiger sees the mouse.[(triple6)] The tiger visits the mouse.[(triple7 OR ((triple3) -> rule3))] @1: The mouse is green.[(((triple3 triple7) -> rule1) OR ((triple6 triple3) -> rule2) OR ((triple3 ((triple3) -> rule3)) -> rule1))]
The mouse is blue.
("mouse" "is" "blue" "+")
triple1
The mouse is red.
("mouse" "is" "red" "+")
triple2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple3
The tiger is red.
("tiger" "is" "red" "+")
triple4
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple5
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple6
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple7
((triple3) -> (rule3 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
((triple3 triple7) -> (rule1 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
((triple6 triple3) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
((triple3 ((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2