The cow needs the mouse. The mouse chases the cow. The mouse eats the cow. If something is round and it needs the cow then it needs the mouse. If something eats the cow then it needs the mouse. If something needs the mouse then it is not round.
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
If something is round and it needs the cow then it needs the mouse.
((("something" "is" "round" "+") ("something" "needs" "cow" "+")) -> ("something" "needs" "mouse" "+"))
If something eats the cow then it needs the mouse.
((("something" "eats" "cow" "+")) -> ("something" "needs" "mouse" "+"))
If something needs the mouse then it is not round.
((("something" "needs" "mouse" "+")) -> ("something" "is" "round" "-"))
The mouse chases the cow.
True
1
proof
[(triple2)]
("mouse" "chases" "cow" "+")
triple2
The mouse does not chase the cow.
False
1
inv-proof
[(triple2)]
("mouse" "chases" "cow" "-")
triple2
The cow is not round.
True
2
proof
[(((triple1) -> rule3))]
("cow" "is" "round" "-")
((triple1) -> (rule3 % int1))
The cow is not round.
("cow" "is" "round" "-")
int1
The mouse does not need the mouse.
False
2
inv-proof
[(((triple3) -> rule2))]
("mouse" "needs" "mouse" "-")
((triple3) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is not round.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("mouse" "is" "round" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is not round.
("mouse" "is" "round" "-")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse is round.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("mouse" "is" "round" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is not round.
("mouse" "is" "round" "-")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The cow does not eat the cow.
Unknown
inv-random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
The cow does not chase the mouse.
Unknown
inv-random
[@0: The cow chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "mouse" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
The cow is not young.
Unknown
inv-random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
@0: The cow needs the mouse.[(triple1)] The mouse chases the cow.[(triple2)] The mouse eats the cow.[(triple3)] @1: The cow is not round.[(((triple1) -> rule3))] The mouse needs the mouse.[(((triple3) -> rule2))] @2: The mouse is not round.[(((((triple3) -> rule2)) -> rule3))]
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple2
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple3
The cow is not round.
("cow" "is" "round" "-")
((triple1) -> (rule3 % int1))
The cow is not round.
("cow" "is" "round" "-")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((triple3) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is not round.
("mouse" "is" "round" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is not round.
("mouse" "is" "round" "-")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2