The cow is red. The cow is not young. The cow likes the mouse. The mouse is not green. The mouse likes the cow. The mouse needs the cow. The mouse does not visit the cow. If the mouse likes the cow and the mouse visits the cow then the mouse needs the cow. If something likes the mouse then it needs the mouse. If something needs the cow then it likes the mouse.
The cow is red.
("cow" "is" "red" "+")
The cow is not young.
("cow" "is" "young" "-")
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The mouse is not green.
("mouse" "is" "green" "-")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The mouse does not visit the cow.
("mouse" "visits" "cow" "-")
If the mouse likes the cow and the mouse visits the cow then the mouse needs the cow.
((("mouse" "likes" "cow" "+") ("mouse" "visits" "cow" "+")) -> ("mouse" "needs" "cow" "+"))
If something likes the mouse then it needs the mouse.
((("something" "likes" "mouse" "+")) -> ("something" "needs" "mouse" "+"))
If something needs the cow then it likes the mouse.
((("something" "needs" "cow" "+")) -> ("something" "likes" "mouse" "+"))
The cow is red.
True
1
proof
[(triple1)]
("cow" "is" "red" "+")
triple1
The cow is not red.
False
1
inv-proof
[(triple1)]
("cow" "is" "red" "-")
triple1
The mouse likes the mouse.
True
2
proof
[(((triple6) -> rule3))]
("mouse" "likes" "mouse" "+")
((triple6) -> (rule3 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse does not like the mouse.
False
2
inv-proof
[(((triple6) -> rule3))]
("mouse" "likes" "mouse" "-")
((triple6) -> (rule3 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse needs the mouse.
True
3
proof
[(((((triple6) -> rule3)) -> rule2))]
("mouse" "needs" "mouse" "+")
((((triple6) -> (rule3 % int2))) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse does not need the mouse.
False
3
inv-proof
[(((((triple6) -> rule3)) -> rule2))]
("mouse" "needs" "mouse" "-")
((((triple6) -> (rule3 % int2))) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The cow is not cold.
Unknown
inv-random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "-")
The cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
The mouse is not young.
Unknown
inv-random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
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 cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
@0: The cow is not young.[(triple2)] The cow is red.[(triple1)] The cow likes the mouse.[(triple3)] The mouse does not visit the cow.[(triple7)] The mouse is not green.[(triple4)] The mouse likes the cow.[(triple5)] The mouse needs the cow.[(triple6)] @1: The cow needs the mouse.[(((triple3) -> rule2))] The mouse likes the mouse.[(((triple6) -> rule3))] @2: The mouse needs the mouse.[(((((triple6) -> rule3)) -> rule2))]
The cow is not young.
("cow" "is" "young" "-")
triple2
The cow is red.
("cow" "is" "red" "+")
triple1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple3
The mouse does not visit the cow.
("mouse" "visits" "cow" "-")
triple7
The mouse is not green.
("mouse" "is" "green" "-")
triple4
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple5
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple6
The cow needs the mouse.
("cow" "needs" "mouse" "+")
((triple3) -> (rule2 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((triple6) -> (rule3 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((((triple6) -> (rule3 % int2))) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2