The cow chases the mouse. The cow is not cold. The cow is nice. The cow is red. The cow is young. The cow needs the mouse. The cow sees the mouse. The mouse is red. The mouse is young. The mouse does not see the cow. If someone needs the cow then they are round. If the mouse chases the cow and the mouse is round then the cow does not see the mouse. If someone is young then they need the cow. If someone needs the mouse and they chase the cow then they are not nice. If the mouse is not young then the mouse chases the cow. If someone sees the cow and the cow chases the mouse then they are not cold. If someone needs the mouse and they do not see the cow then the mouse needs the cow. If the mouse does not need the cow then the cow is not round.
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The cow is not cold.
("cow" "is" "cold" "-")
The cow is nice.
("cow" "is" "nice" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is young.
("cow" "is" "young" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse does not see the cow.
("mouse" "sees" "cow" "-")
If someone needs the cow then they are round.
((("someone" "needs" "cow" "+")) -> ("someone" "is" "round" "+"))
If the mouse chases the cow and the mouse is round then the cow does not see the mouse.
((("mouse" "chases" "cow" "+") ("mouse" "is" "round" "+")) -> ("cow" "sees" "mouse" "-"))
If someone is young then they need the cow.
((("someone" "is" "young" "+")) -> ("someone" "needs" "cow" "+"))
If someone needs the mouse and they chase the cow then they are not nice.
((("someone" "needs" "mouse" "+") ("someone" "chases" "cow" "+")) -> ("someone" "is" "nice" "-"))
If the mouse is not young then the mouse chases the cow.
((("mouse" "is" "young" "~")) -> ("mouse" "chases" "cow" "+"))
If someone sees the cow and the cow chases the mouse then they are not cold.
((("someone" "sees" "cow" "+") ("cow" "chases" "mouse" "+")) -> ("someone" "is" "cold" "-"))
If someone needs the mouse and they do not see the cow then the mouse needs the cow.
((("someone" "needs" "mouse" "+") ("someone" "sees" "cow" "~")) -> ("mouse" "needs" "cow" "+"))
If the mouse does not need the cow then the cow is not round.
((("mouse" "needs" "cow" "~")) -> ("cow" "is" "round" "-"))
The cow is young.
True
1
proof
[(triple5)]
("cow" "is" "young" "+")
triple5
The cow does not chase the mouse.
False
1
inv-proof
[(triple1)]
("cow" "chases" "mouse" "-")
triple1
The cow needs the cow.
True
2
proof
[(((triple5) -> rule3))]
("cow" "needs" "cow" "+")
((triple5) -> (rule3 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The mouse does not need the cow.
False
2
inv-proof
[(((triple9) -> rule3))]
("mouse" "needs" "cow" "-")
((triple9) -> (rule3 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
The mouse does not chase the cow.
Unknown
inv-rconc
[@1: The mouse chases the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "chases" "cow" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
@0: The cow chases the mouse.[(triple1)] The cow is nice.[(triple3)] The cow is not cold.[(triple2)] The cow is red.[(triple4)] The cow is young.[(triple5)] The cow needs the mouse.[(triple6)] The cow sees the mouse.[(triple7)] The mouse does not see the cow.[(triple10)] The mouse is red.[(triple8)] The mouse is young.[(triple9)] @1: The cow needs the cow.[(((triple5) -> rule3))] The mouse needs the cow.[(((triple9) -> rule3))] @2: The cow is round.[(((((triple5) -> rule3)) -> rule1))] The mouse is round.[(((((triple9) -> rule3)) -> rule1))]
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple1
The cow is nice.
("cow" "is" "nice" "+")
triple3
The cow is not cold.
("cow" "is" "cold" "-")
triple2
The cow is red.
("cow" "is" "red" "+")
triple4
The cow is young.
("cow" "is" "young" "+")
triple5
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple6
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple7
The mouse does not see the cow.
("mouse" "sees" "cow" "-")
triple10
The mouse is red.
("mouse" "is" "red" "+")
triple8
The mouse is young.
("mouse" "is" "young" "+")
triple9
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple5) -> (rule3 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The mouse needs the cow.
("mouse" "needs" "cow" "+")
((triple9) -> (rule3 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
The cow is round.
("cow" "is" "round" "+")
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
((((triple9) -> (rule3 % int2))) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int2