The cat does not visit the tiger. The cow visits the mouse. The mouse sees the tiger. The tiger visits the mouse. If something visits the mouse then the mouse does not see the cow.
The cat does not visit the tiger.
("cat" "visits" "tiger" "-")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If something visits the mouse then the mouse does not see the cow.
((("something" "visits" "mouse" "+")) -> ("mouse" "sees" "cow" "-"))
The cat does not visit the tiger.
True
1
proof
[(triple1)]
("cat" "visits" "tiger" "-")
triple1
The cow does not visit the mouse.
False
1
inv-proof
[(triple2)]
("cow" "visits" "mouse" "-")
triple2
The mouse does not see the cow.
True
2
proof
[(((triple2) -> rule1) OR ((triple4) -> rule1))]
("mouse" "sees" "cow" "-")
((triple2) -> (rule1 % int1))
The mouse does not see the cow.
("mouse" "sees" "cow" "-")
int1
((triple4) -> (rule1 % int1))
The mouse does not see the cow.
("mouse" "sees" "cow" "-")
int1
The mouse sees the cow.
False
2
inv-proof
[(((triple2) -> rule1) OR ((triple4) -> rule1))]
("mouse" "sees" "cow" "+")
((triple2) -> (rule1 % int1))
The mouse does not see the cow.
("mouse" "sees" "cow" "-")
int1
((triple4) -> (rule1 % int1))
The mouse does not see the cow.
("mouse" "sees" "cow" "-")
int1
The cow is not blue.
Unknown
inv-random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "-")
The tiger needs the mouse.
Unknown
random
[@0: The tiger needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "mouse" "+")
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
@0: The cat does not visit the tiger.[(triple1)] The cow visits the mouse.[(triple2)] The mouse sees the tiger.[(triple3)] The tiger visits the mouse.[(triple4)] @1: The mouse does not see the cow.[(((triple2) -> rule1) OR ((triple4) -> rule1))]
The cat does not visit the tiger.
("cat" "visits" "tiger" "-")
triple1
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple3
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple4
The mouse does not see the cow.
("mouse" "sees" "cow" "-")
((triple2) -> (rule1 % int1))
The mouse does not see the cow.
("mouse" "sees" "cow" "-")
int1
((triple4) -> (rule1 % int1))
The mouse does not see the cow.
("mouse" "sees" "cow" "-")
int1