The cow is cold. The cow is green. The cow likes the mouse. The cow needs the mouse. The cow sees the mouse. The mouse is cold. The mouse is green. The mouse is nice. The mouse is young. The mouse likes the cow. The mouse needs the cow. The mouse sees the cow. If something is cold and it likes the mouse then it needs the cow. If something is cold and it likes the mouse then it needs the cow.
The cow is cold.
("cow" "is" "cold" "+")
The cow is green.
("cow" "is" "green" "+")
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
If something is cold and it likes the mouse then it needs the cow.
((("something" "is" "cold" "+") ("something" "likes" "mouse" "+")) -> ("something" "needs" "cow" "+"))
If something is cold and it likes the mouse then it needs the cow.
((("something" "is" "cold" "+") ("something" "likes" "mouse" "+")) -> ("something" "needs" "cow" "+"))
The cow is cold.
True
1
proof
[(triple1)]
("cow" "is" "cold" "+")
triple1
The mouse is not cold.
False
1
inv-proof
[(triple6)]
("mouse" "is" "cold" "-")
triple6
The cow needs the cow.
True
3
proof
[(((triple1 triple3) -> rule1) OR ((triple1 triple3) -> rule2))]
("cow" "needs" "cow" "+")
((triple1 triple3) -> (rule1 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
((triple1 triple3) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow does not need the cow.
False
3
inv-proof
[(((triple1 triple3) -> rule1) OR ((triple1 triple3) -> rule2))]
("cow" "needs" "cow" "-")
((triple1 triple3) -> (rule1 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
((triple1 triple3) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
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 sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
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 is cold.[(triple1)] The cow is green.[(triple2)] The cow likes the mouse.[(triple3)] The cow needs the mouse.[(triple4)] The cow sees the mouse.[(triple5)] The mouse is cold.[(triple6)] The mouse is green.[(triple7)] The mouse is nice.[(triple8)] The mouse is young.[(triple9)] The mouse likes the cow.[(triple10)] The mouse needs the cow.[(triple11)] The mouse sees the cow.[(triple12)] @1: The cow needs the cow.[(((triple1 triple3) -> rule1) OR ((triple1 triple3) -> rule2))]
The cow is cold.
("cow" "is" "cold" "+")
triple1
The cow is green.
("cow" "is" "green" "+")
triple2
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple3
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple4
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple5
The mouse is cold.
("mouse" "is" "cold" "+")
triple6
The mouse is green.
("mouse" "is" "green" "+")
triple7
The mouse is nice.
("mouse" "is" "nice" "+")
triple8
The mouse is young.
("mouse" "is" "young" "+")
triple9
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple10
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple11
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple12
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple1 triple3) -> (rule1 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
((triple1 triple3) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1