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