The bear is nice. The cow eats the squirrel. The cow is green. The mouse eats the bear. The squirrel is not green. The squirrel is nice. The squirrel needs the cow. If someone is round then they do not like the cow. If someone likes the squirrel and the squirrel needs the cow then the cow is nice. If someone is nice then they need the squirrel. If someone likes the mouse then they need the squirrel. If someone eats the cow and the cow needs the bear then they are not green. If someone likes the squirrel then they eat the mouse. If someone likes the squirrel and the squirrel needs the mouse then the squirrel is not green. If someone needs the squirrel then they like the squirrel.
The bear is nice.
("bear" "is" "nice" "+")
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
The cow is green.
("cow" "is" "green" "+")
The mouse eats the bear.
("mouse" "eats" "bear" "+")
The squirrel is not green.
("squirrel" "is" "green" "-")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
If someone is round then they do not like the cow.
((("someone" "is" "round" "+")) -> ("someone" "likes" "cow" "-"))
If someone likes the squirrel and the squirrel needs the cow then the cow is nice.
((("someone" "likes" "squirrel" "+") ("squirrel" "needs" "cow" "+")) -> ("cow" "is" "nice" "+"))
If someone is nice then they need the squirrel.
((("someone" "is" "nice" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone likes the mouse then they need the squirrel.
((("someone" "likes" "mouse" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone eats the cow and the cow needs the bear then they are not green.
((("someone" "eats" "cow" "+") ("cow" "needs" "bear" "+")) -> ("someone" "is" "green" "-"))
If someone likes the squirrel then they eat the mouse.
((("someone" "likes" "squirrel" "+")) -> ("someone" "eats" "mouse" "+"))
If someone likes the squirrel and the squirrel needs the mouse then the squirrel is not green.
((("someone" "likes" "squirrel" "+") ("squirrel" "needs" "mouse" "+")) -> ("squirrel" "is" "green" "-"))
If someone needs the squirrel then they like the squirrel.
((("someone" "needs" "squirrel" "+")) -> ("someone" "likes" "squirrel" "+"))
The squirrel needs the cow.
True
1
proof
[(triple7)]
("squirrel" "needs" "cow" "+")
triple7
The mouse does not eat the bear.
False
1
inv-proof
[(triple4)]
("mouse" "eats" "bear" "-")
triple4
The bear needs the squirrel.
True
2
proof
[(((triple1) -> rule3))]
("bear" "needs" "squirrel" "+")
((triple1) -> (rule3 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The bear does not need the squirrel.
False
2
inv-proof
[(((triple1) -> rule3))]
("bear" "needs" "squirrel" "-")
((triple1) -> (rule3 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The squirrel likes the squirrel.
True
3
proof
[(((((triple6) -> rule3)) -> rule8))]
("squirrel" "likes" "squirrel" "+")
((((triple6) -> (rule3 % int2))) -> (rule8 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int2
The bear does not like the squirrel.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule8))]
("bear" "likes" "squirrel" "-")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int2
The cow is nice.
True
5
proof
[(((((((triple1) -> rule3)) -> rule8) triple7) -> rule2) OR ((((((triple6) -> rule3)) -> rule8) triple7) -> rule2))]
("cow" "is" "nice" "+")
((((((triple1) -> (rule3 % int3))) -> (rule8 % int2)) triple7) -> (rule2 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int2
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int3
((((((triple6) -> (rule3 % int3))) -> (rule8 % int2)) triple7) -> (rule2 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int2
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int3
The bear does not eat the mouse.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule8)) -> rule6))]
("bear" "eats" "mouse" "-")
((((((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The bear eats the mouse.
("bear" "eats" "mouse" "+")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int2
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int3
The cow needs the squirrel.
True
6
proof
[(((((((((triple1) -> rule3)) -> rule8) triple7) -> rule2)) -> rule3) OR ((((((((triple6) -> rule3)) -> rule8) triple7) -> rule2)) -> rule3))]
("cow" "needs" "squirrel" "+")
((((((((triple1) -> (rule3 % int4))) -> (rule8 % int3)) triple7) -> (rule2 % int2))) -> (rule3 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int3
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int4
((((((((triple6) -> (rule3 % int4))) -> (rule8 % int3)) triple7) -> (rule2 % int2))) -> (rule3 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int3
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int4
The cow does not need the squirrel.
False
6
inv-proof
[(((((((((triple1) -> rule3)) -> rule8) triple7) -> rule2)) -> rule3) OR ((((((((triple6) -> rule3)) -> rule8) triple7) -> rule2)) -> rule3))]
("cow" "needs" "squirrel" "-")
((((((((triple1) -> (rule3 % int4))) -> (rule8 % int3)) triple7) -> (rule2 % int2))) -> (rule3 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int3
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int4
((((((((triple6) -> (rule3 % int4))) -> (rule8 % int3)) triple7) -> (rule2 % int2))) -> (rule3 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int3
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int4
The cow likes the squirrel.
True
7
proof
[(((((((((((triple1) -> rule3)) -> rule8) triple7) -> rule2)) -> rule3)) -> rule8) OR ((((((((((triple6) -> rule3)) -> rule8) triple7) -> rule2)) -> rule3)) -> rule8))]
("cow" "likes" "squirrel" "+")
((((((((((triple1) -> (rule3 % int5))) -> (rule8 % int4)) triple7) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int4
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int5
((((((((((triple6) -> (rule3 % int5))) -> (rule8 % int4)) triple7) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int4
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int5
The cow does not like the squirrel.
False
7
inv-proof
[(((((((((((triple1) -> rule3)) -> rule8) triple7) -> rule2)) -> rule3)) -> rule8) OR ((((((((((triple6) -> rule3)) -> rule8) triple7) -> rule2)) -> rule3)) -> rule8))]
("cow" "likes" "squirrel" "-")
((((((((((triple1) -> (rule3 % int5))) -> (rule8 % int4)) triple7) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int4
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int5
((((((((((triple6) -> (rule3 % int5))) -> (rule8 % int4)) triple7) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int4
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int5
The mouse does not need the squirrel.
Unknown
inv-rconc
[@1: The mouse needs the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "needs" "squirrel" "-")
The mouse eats the mouse.
Unknown
rconc
[@3: The mouse eats the mouse.[CWA. Example of deepest failure = (rule6 <- rule8 <- rule3 <- FAIL)]]
("mouse" "eats" "mouse" "+")
The mouse does not like the squirrel.
Unknown
inv-rconc
[@2: The mouse likes the squirrel.[CWA. Example of deepest failure = (rule8 <- rule3 <- FAIL)]]
("mouse" "likes" "squirrel" "-")
The squirrel likes the cow.
Unknown
random
[@0: The squirrel likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "cow" "+")
The cow does not like the mouse.
Unknown
inv-random
[@0: The cow likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "mouse" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
The squirrel is not rough.
Unknown
inv-random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "-")
The cow needs the bear.
Unknown
random
[@0: The cow needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "bear" "+")
The mouse is not cold.
Unknown
inv-random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "-")
The squirrel likes the mouse.
Unknown
random
[@0: The squirrel likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "mouse" "+")
The bear does not like the cow.
Unknown
inv-random
[@0: The bear likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "cow" "-")
The mouse is round.
Unknown
random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "+")
@0: The bear is nice.[(triple1)] The cow eats the squirrel.[(triple2)] The cow is green.[(triple3)] The mouse eats the bear.[(triple4)] The squirrel is nice.[(triple6)] The squirrel is not green.[(triple5)] The squirrel needs the cow.[(triple7)] @1: The bear needs the squirrel.[(((triple1) -> rule3))] The squirrel needs the squirrel.[(((triple6) -> rule3))] @2: The bear likes the squirrel.[(((((triple1) -> rule3)) -> rule8))] The squirrel likes the squirrel.[(((((triple6) -> rule3)) -> rule8))] @3: The bear eats the mouse.[(((((((triple1) -> rule3)) -> rule8)) -> rule6))] The cow is nice.[(((((((triple1) -> rule3)) -> rule8) triple7) -> rule2) OR ((((((triple6) -> rule3)) -> rule8) triple7) -> rule2))] The squirrel eats the mouse.[(((((((triple6) -> rule3)) -> rule8)) -> rule6))] @4: The cow needs the squirrel.[(((((((((triple1) -> rule3)) -> rule8) triple7) -> rule2)) -> rule3) OR ((((((((triple6) -> rule3)) -> rule8) triple7) -> rule2)) -> rule3))] @5: The cow likes the squirrel.[(((((((((((triple1) -> rule3)) -> rule8) triple7) -> rule2)) -> rule3)) -> rule8) OR ((((((((((triple6) -> rule3)) -> rule8) triple7) -> rule2)) -> rule3)) -> rule8))] @6: The cow eats the mouse.[(((((((((((((triple1) -> rule3)) -> rule8) triple7) -> rule2)) -> rule3)) -> rule8)) -> rule6) OR ((((((((((((triple6) -> rule3)) -> rule8) triple7) -> rule2)) -> rule3)) -> rule8)) -> rule6))]
The bear is nice.
("bear" "is" "nice" "+")
triple1
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
triple2
The cow is green.
("cow" "is" "green" "+")
triple3
The mouse eats the bear.
("mouse" "eats" "bear" "+")
triple4
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple6
The squirrel is not green.
("squirrel" "is" "green" "-")
triple5
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
triple7
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
((triple1) -> (rule3 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((triple6) -> (rule3 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int2
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
((((triple6) -> (rule3 % int2))) -> (rule8 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int2
The bear eats the mouse.
("bear" "eats" "mouse" "+")
((((((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The bear eats the mouse.
("bear" "eats" "mouse" "+")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int2
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int3
The cow is nice.
("cow" "is" "nice" "+")
((((((triple1) -> (rule3 % int3))) -> (rule8 % int2)) triple7) -> (rule2 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int2
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int3
((((((triple6) -> (rule3 % int3))) -> (rule8 % int2)) triple7) -> (rule2 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int2
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int3
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
((((((triple6) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int2
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int3
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
((((((((triple1) -> (rule3 % int4))) -> (rule8 % int3)) triple7) -> (rule2 % int2))) -> (rule3 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int3
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int4
((((((((triple6) -> (rule3 % int4))) -> (rule8 % int3)) triple7) -> (rule2 % int2))) -> (rule3 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int3
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int4
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
((((((((((triple1) -> (rule3 % int5))) -> (rule8 % int4)) triple7) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int4
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int5
((((((((((triple6) -> (rule3 % int5))) -> (rule8 % int4)) triple7) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int4
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int5
The cow eats the mouse.
("cow" "eats" "mouse" "+")
((((((((((((triple1) -> (rule3 % int6))) -> (rule8 % int5)) triple7) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int1
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int2
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int3
The cow is nice.
("cow" "is" "nice" "+")
int4
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int5
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int6
((((((((((((triple6) -> (rule3 % int6))) -> (rule8 % int5)) triple7) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int1
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int2
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int3
The cow is nice.
("cow" "is" "nice" "+")
int4
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int5
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int6