The cow is blue. The mouse needs the cow. If something needs the mouse then the mouse visits the cow. If something needs the cow then the cow needs the mouse.
The cow is blue.
("cow" "is" "blue" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
If something needs the mouse then the mouse visits the cow.
((("something" "needs" "mouse" "+")) -> ("mouse" "visits" "cow" "+"))
If something needs the cow then the cow needs the mouse.
((("something" "needs" "cow" "+")) -> ("cow" "needs" "mouse" "+"))
The cow is blue.
True
1
proof
[(triple1)]
("cow" "is" "blue" "+")
triple1
The cow is not blue.
False
1
inv-proof
[(triple1)]
("cow" "is" "blue" "-")
triple1
The cow needs the mouse.
True
2
proof
[(((triple2) -> rule2))]
("cow" "needs" "mouse" "+")
((triple2) -> (rule2 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The cow does not need the mouse.
False
2
inv-proof
[(((triple2) -> rule2))]
("cow" "needs" "mouse" "-")
((triple2) -> (rule2 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The mouse visits the cow.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("mouse" "visits" "cow" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The mouse does not visit the cow.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("mouse" "visits" "cow" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The cow does not need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
The mouse is not round.
Unknown
inv-random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
@0: The cow is blue.[(triple1)] The mouse needs the cow.[(triple2)] @1: The cow needs the mouse.[(((triple2) -> rule2))] @2: The mouse visits the cow.[(((((triple2) -> rule2)) -> rule1))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
((triple2) -> (rule2 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2