The cow eats the mouse. The cow is not blue. The cow is kind. The cow is not round. The cow needs the mouse. The cow sees the mouse. The mouse eats the cow. The mouse is round. The mouse needs the cow. The mouse sees the cow. If someone eats the mouse then they eat the cow. If the mouse sees the cow and the mouse does not eat the cow then the cow does not see the mouse. If someone needs the cow and they need the mouse then they see the cow. If someone eats the cow and the cow sees the mouse then they need the cow. If someone needs the cow and the cow eats the mouse then they need the mouse. If someone sees the cow and they are not red then they need the mouse.
The cow eats the mouse.
("cow" "eats" "mouse" "+")
The cow is not blue.
("cow" "is" "blue" "-")
The cow is kind.
("cow" "is" "kind" "+")
The cow is not round.
("cow" "is" "round" "-")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
If someone eats the mouse then they eat the cow.
((("someone" "eats" "mouse" "+")) -> ("someone" "eats" "cow" "+"))
If the mouse sees the cow and the mouse does not eat the cow then the cow does not see the mouse.
((("mouse" "sees" "cow" "+") ("mouse" "eats" "cow" "~")) -> ("cow" "sees" "mouse" "-"))
If someone needs the cow and they need the mouse then they see the cow.
((("someone" "needs" "cow" "+") ("someone" "needs" "mouse" "+")) -> ("someone" "sees" "cow" "+"))
If someone eats the cow and the cow sees the mouse then they need the cow.
((("someone" "eats" "cow" "+") ("cow" "sees" "mouse" "+")) -> ("someone" "needs" "cow" "+"))
If someone needs the cow and the cow eats the mouse then they need the mouse.
((("someone" "needs" "cow" "+") ("cow" "eats" "mouse" "+")) -> ("someone" "needs" "mouse" "+"))
If someone sees the cow and they are not red then they need the mouse.
((("someone" "sees" "cow" "+") ("someone" "is" "red" "~")) -> ("someone" "needs" "mouse" "+"))
The cow is not blue.
True
1
proof
[(triple2)]
("cow" "is" "blue" "-")
triple2
The mouse does not eat the cow.
False
1
inv-proof
[(triple7)]
("mouse" "eats" "cow" "-")
triple7
The cow eats the cow.
True
2
proof
[(((triple1) -> rule1))]
("cow" "eats" "cow" "+")
((triple1) -> (rule1 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow does not eat the cow.
False
2
inv-proof
[(((triple1) -> rule1))]
("cow" "eats" "cow" "-")
((triple1) -> (rule1 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow needs the cow.
True
4
proof
[(((((triple1) -> rule1) triple6) -> rule4))]
("cow" "needs" "cow" "+")
((((triple1) -> (rule1 % int2)) triple6) -> (rule4 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow does not need the cow.
False
4
inv-proof
[(((((triple1) -> rule1) triple6) -> rule4))]
("cow" "needs" "cow" "-")
((((triple1) -> (rule1 % int2)) triple6) -> (rule4 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow sees the cow.
True
6
proof
[(((((((triple1) -> rule1) triple6) -> rule4) triple5) -> rule3) OR ((((((triple1) -> rule1) triple6) -> rule4) ((((((triple1) -> rule1) triple6) -> rule4) triple1) -> rule5)) -> rule3))]
("cow" "sees" "cow" "+")
((((((triple1) -> (rule1 % int3)) triple6) -> (rule4 % int2)) triple5) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
((((((triple1) -> (rule1 % int4)) triple6) -> (rule4 % int3)) ((((((triple1) -> (rule1 % int4)) triple6) -> (rule4 % int3)) triple1) -> (rule5 % int2))) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
int3
The cow eats the cow.
("cow" "eats" "cow" "+")
int4
The cow does not see the cow.
False
6
inv-proof
[(((((((triple1) -> rule1) triple6) -> rule4) triple5) -> rule3) OR ((((((triple1) -> rule1) triple6) -> rule4) ((((((triple1) -> rule1) triple6) -> rule4) triple1) -> rule5)) -> rule3))]
("cow" "sees" "cow" "-")
((((((triple1) -> (rule1 % int3)) triple6) -> (rule4 % int2)) triple5) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
((((((triple1) -> (rule1 % int4)) triple6) -> (rule4 % int3)) ((((((triple1) -> (rule1 % int4)) triple6) -> (rule4 % int3)) triple1) -> (rule5 % int2))) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
int3
The cow eats the cow.
("cow" "eats" "cow" "+")
int4
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 is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
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 cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
The mouse is not kind.
Unknown
inv-random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
The mouse is not red.
Unknown
inv-random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
@0: The cow eats the mouse.[(triple1)] The cow is kind.[(triple3)] The cow is not blue.[(triple2)] The cow is not round.[(triple4)] The cow needs the mouse.[(triple5 OR ((((((triple1) -> rule1) triple6) -> rule4) triple1) -> rule5))] The cow sees the mouse.[(triple6)] The mouse eats the cow.[(triple7)] The mouse is round.[(triple8)] The mouse needs the cow.[(triple9 OR ((triple7 triple6) -> rule4))] The mouse sees the cow.[(triple10 OR ((triple9 ((triple9 triple1) -> rule5)) -> rule3) OR ((((triple7 triple6) -> rule4) ((triple9 triple1) -> rule5)) -> rule3) OR ((triple9 ((((triple7 triple6) -> rule4) triple1) -> rule5)) -> rule3) OR ((((triple7 triple6) -> rule4) ((((triple7 triple6) -> rule4) triple1) -> rule5)) -> rule3))] @1: The cow eats the cow.[(((triple1) -> rule1))] The mouse needs the mouse.[(((triple9 triple1) -> rule5) OR ((((triple7 triple6) -> rule4) triple1) -> rule5))] @2: The cow needs the cow.[(((((triple1) -> rule1) triple6) -> rule4))] @3: The cow sees the cow.[(((((((triple1) -> rule1) triple6) -> rule4) triple5) -> rule3) OR ((((((triple1) -> rule1) triple6) -> rule4) ((((((triple1) -> rule1) triple6) -> rule4) triple1) -> rule5)) -> rule3))]
The cow eats the mouse.
("cow" "eats" "mouse" "+")
triple1
The cow is kind.
("cow" "is" "kind" "+")
triple3
The cow is not blue.
("cow" "is" "blue" "-")
triple2
The cow is not round.
("cow" "is" "round" "-")
triple4
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple5
((((((triple1) -> (rule1 % int3)) triple6) -> (rule4 % int2)) triple1) -> (rule5 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple6
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple7
The mouse is round.
("mouse" "is" "round" "+")
triple8
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple9
((triple7 triple6) -> (rule4 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple10
((triple9 ((triple9 triple1) -> (rule5 % int2))) -> (rule3 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
((((triple7 triple6) -> (rule4 % int3)) ((triple9 triple1) -> (rule5 % int2))) -> (rule3 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int3
((triple9 ((((triple7 triple6) -> (rule4 % int3)) triple1) -> (rule5 % int2))) -> (rule3 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int3
((((triple7 triple6) -> (rule4 % int3)) ((((triple7 triple6) -> (rule4 % int3)) triple1) -> (rule5 % int2))) -> (rule3 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int3
The cow eats the cow.
("cow" "eats" "cow" "+")
((triple1) -> (rule1 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((triple9 triple1) -> (rule5 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
((((triple7 triple6) -> (rule4 % int2)) triple1) -> (rule5 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
((((triple1) -> (rule1 % int2)) triple6) -> (rule4 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow sees the cow.
("cow" "sees" "cow" "+")
((((((triple1) -> (rule1 % int3)) triple6) -> (rule4 % int2)) triple5) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
((((((triple1) -> (rule1 % int4)) triple6) -> (rule4 % int3)) ((((((triple1) -> (rule1 % int4)) triple6) -> (rule4 % int3)) triple1) -> (rule5 % int2))) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
int3
The cow eats the cow.
("cow" "eats" "cow" "+")
int4