The cow is cold. The cow does not like the mouse. The cow needs the mouse. The mouse is big. The mouse is blue. The mouse is cold. The mouse likes the cow. If the cow chases the mouse and the cow needs the mouse then the cow is not young. If the cow is blue then the cow is not big. Big things are cold.
The cow is cold.
("cow" "is" "cold" "+")
The cow does not like the mouse.
("cow" "likes" "mouse" "-")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
If the cow chases the mouse and the cow needs the mouse then the cow is not young.
((("cow" "chases" "mouse" "+") ("cow" "needs" "mouse" "+")) -> ("cow" "is" "young" "-"))
If the cow is blue then the cow is not big.
((("cow" "is" "blue" "+")) -> ("cow" "is" "big" "-"))
Big things are cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
The mouse is cold.
True
1
proof
[(triple6 OR ((triple4) -> rule3))]
("mouse" "is" "cold" "+")
triple6
((triple4) -> (rule3 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The cow likes the mouse.
False
1
inv-proof
[(triple2)]
("cow" "likes" "mouse" "+")
triple2
The cow does not like the cow.
Unknown
inv-random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
@0: The cow does not like the mouse.[(triple2)] The cow is cold.[(triple1)] The cow needs the mouse.[(triple3)] The mouse is big.[(triple4)] The mouse is blue.[(triple5)] The mouse is cold.[(triple6 OR ((triple4) -> rule3))] The mouse likes the cow.[(triple7)]
The cow does not like the mouse.
("cow" "likes" "mouse" "-")
triple2
The cow is cold.
("cow" "is" "cold" "+")
triple1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple3
The mouse is big.
("mouse" "is" "big" "+")
triple4
The mouse is blue.
("mouse" "is" "blue" "+")
triple5
The mouse is cold.
("mouse" "is" "cold" "+")
triple6
((triple4) -> (rule3 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple7