The cow eats the mouse. The cow eats the tiger. The cow is not kind. The cow likes the tiger. The cow does not visit the mouse. The mouse does not eat the cow. The mouse does not visit the cow. The tiger eats the mouse. The tiger is blue. The tiger likes the mouse. If someone eats the mouse then the mouse does not visit the tiger.
The cow eats the mouse.
("cow" "eats" "mouse" "+")
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The cow is not kind.
("cow" "is" "kind" "-")
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The cow does not visit the mouse.
("cow" "visits" "mouse" "-")
The mouse does not eat the cow.
("mouse" "eats" "cow" "-")
The mouse does not visit the cow.
("mouse" "visits" "cow" "-")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
If someone eats the mouse then the mouse does not visit the tiger.
((("someone" "eats" "mouse" "+")) -> ("mouse" "visits" "tiger" "-"))
The cow eats the mouse.
True
1
proof
[(triple1)]
("cow" "eats" "mouse" "+")
triple1
The cow does not eat the mouse.
False
1
inv-proof
[(triple1)]
("cow" "eats" "mouse" "-")
triple1
The mouse does not visit the tiger.
True
2
proof
[(((triple1) -> rule1) OR ((triple8) -> rule1))]
("mouse" "visits" "tiger" "-")
((triple1) -> (rule1 % int1))
The mouse does not visit the tiger.
("mouse" "visits" "tiger" "-")
int1
((triple8) -> (rule1 % int1))
The mouse does not visit the tiger.
("mouse" "visits" "tiger" "-")
int1
The mouse visits the tiger.
False
2
inv-proof
[(((triple1) -> rule1) OR ((triple8) -> rule1))]
("mouse" "visits" "tiger" "+")
((triple1) -> (rule1 % int1))
The mouse does not visit the tiger.
("mouse" "visits" "tiger" "-")
int1
((triple8) -> (rule1 % int1))
The mouse does not visit the tiger.
("mouse" "visits" "tiger" "-")
int1
The cow does not visit the tiger.
Unknown
inv-random
[@0: The cow visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "tiger" "-")
The mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
The tiger is not cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
The tiger likes the cow.
Unknown
random
[@0: The tiger likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "cow" "+")
@0: The cow does not visit the mouse.[(triple5)] The cow eats the mouse.[(triple1)] The cow eats the tiger.[(triple2)] The cow is not kind.[(triple3)] The cow likes the tiger.[(triple4)] The mouse does not eat the cow.[(triple6)] The mouse does not visit the cow.[(triple7)] The tiger eats the mouse.[(triple8)] The tiger is blue.[(triple9)] The tiger likes the mouse.[(triple10)] @1: The mouse does not visit the tiger.[(((triple1) -> rule1) OR ((triple8) -> rule1))]
The cow does not visit the mouse.
("cow" "visits" "mouse" "-")
triple5
The cow eats the mouse.
("cow" "eats" "mouse" "+")
triple1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple2
The cow is not kind.
("cow" "is" "kind" "-")
triple3
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple4
The mouse does not eat the cow.
("mouse" "eats" "cow" "-")
triple6
The mouse does not visit the cow.
("mouse" "visits" "cow" "-")
triple7
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple8
The tiger is blue.
("tiger" "is" "blue" "+")
triple9
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple10
The mouse does not visit the tiger.
("mouse" "visits" "tiger" "-")
((triple1) -> (rule1 % int1))
The mouse does not visit the tiger.
("mouse" "visits" "tiger" "-")
int1
((triple8) -> (rule1 % int1))
The mouse does not visit the tiger.
("mouse" "visits" "tiger" "-")
int1