The bear is kind. The bear needs the squirrel. The cow is cold. The cow is kind. The cow is nice. The cow sees the bear. The rabbit eats the bear. The rabbit eats the cow. The rabbit is round. The squirrel eats the bear. The squirrel eats the rabbit. The squirrel needs the bear. The squirrel needs the rabbit. The squirrel sees the cow. If someone needs the rabbit then they need the bear. If someone sees the rabbit then they eat the squirrel. If someone eats the rabbit then they eat the squirrel. If someone eats the bear and they eat the squirrel then they need the rabbit. If someone sees the squirrel then the squirrel is round. If someone sees the rabbit and the rabbit is green then they see the squirrel. If someone is kind and they need the cow then they are cold. If someone eats the bear and they are nice then the bear sees the rabbit. If someone is kind then they eat the bear.
The bear is kind.
("bear" "is" "kind" "+")
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
If someone needs the rabbit then they need the bear.
((("someone" "needs" "rabbit" "+")) -> ("someone" "needs" "bear" "+"))
If someone sees the rabbit then they eat the squirrel.
((("someone" "sees" "rabbit" "+")) -> ("someone" "eats" "squirrel" "+"))
If someone eats the rabbit then they eat the squirrel.
((("someone" "eats" "rabbit" "+")) -> ("someone" "eats" "squirrel" "+"))
If someone eats the bear and they eat the squirrel then they need the rabbit.
((("someone" "eats" "bear" "+") ("someone" "eats" "squirrel" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone sees the squirrel then the squirrel is round.
((("someone" "sees" "squirrel" "+")) -> ("squirrel" "is" "round" "+"))
If someone sees the rabbit and the rabbit is green then they see the squirrel.
((("someone" "sees" "rabbit" "+") ("rabbit" "is" "green" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone is kind and they need the cow then they are cold.
((("someone" "is" "kind" "+") ("someone" "needs" "cow" "+")) -> ("someone" "is" "cold" "+"))
If someone eats the bear and they are nice then the bear sees the rabbit.
((("someone" "eats" "bear" "+") ("someone" "is" "nice" "+")) -> ("bear" "sees" "rabbit" "+"))
If someone is kind then they eat the bear.
((("someone" "is" "kind" "+")) -> ("someone" "eats" "bear" "+"))
The squirrel needs the rabbit.
True
1
proof
[(triple13 OR ((triple10 ((triple11) -> rule3)) -> rule4))]
("squirrel" "needs" "rabbit" "+")
triple13
((triple10 ((triple11) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The rabbit is not round.
False
1
inv-proof
[(triple9)]
("rabbit" "is" "round" "-")
triple9
The cow eats the bear.
True
2
proof
[(((triple4) -> rule9))]
("cow" "eats" "bear" "+")
((triple4) -> (rule9 % int1))
The cow eats the bear.
("cow" "eats" "bear" "+")
int1
The cow does not eat the bear.
False
2
inv-proof
[(((triple4) -> rule9))]
("cow" "eats" "bear" "-")
((triple4) -> (rule9 % int1))
The cow eats the bear.
("cow" "eats" "bear" "+")
int1
The bear sees the rabbit.
True
4
proof
[(((((triple4) -> rule9) triple5) -> rule8))]
("bear" "sees" "rabbit" "+")
((((triple4) -> (rule9 % int2)) triple5) -> (rule8 % int1))
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
int2
The bear does not see the rabbit.
False
4
inv-proof
[(((((triple4) -> rule9) triple5) -> rule8))]
("bear" "sees" "rabbit" "-")
((((triple4) -> (rule9 % int2)) triple5) -> (rule8 % int1))
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
int2
The bear eats the squirrel.
True
5
proof
[(((((((triple4) -> rule9) triple5) -> rule8)) -> rule2))]
("bear" "eats" "squirrel" "+")
((((((triple4) -> (rule9 % int3)) triple5) -> (rule8 % int2))) -> (rule2 % int1))
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
int1
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int2
The cow eats the bear.
("cow" "eats" "bear" "+")
int3
The bear does not eat the squirrel.
False
5
inv-proof
[(((((((triple4) -> rule9) triple5) -> rule8)) -> rule2))]
("bear" "eats" "squirrel" "-")
((((((triple4) -> (rule9 % int3)) triple5) -> (rule8 % int2))) -> (rule2 % int1))
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
int1
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int2
The cow eats the bear.
("cow" "eats" "bear" "+")
int3
The bear needs the rabbit.
True
8
proof
[(((((triple1) -> rule9) ((((((triple4) -> rule9) triple5) -> rule8)) -> rule2)) -> rule4))]
("bear" "needs" "rabbit" "+")
((((triple1) -> (rule9 % int5)) ((((((triple4) -> (rule9 % int4)) triple5) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int1
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
int2
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int3
The cow eats the bear.
("cow" "eats" "bear" "+")
int4
The bear eats the bear.
("bear" "eats" "bear" "+")
int5
The bear does not need the rabbit.
False
8
inv-proof
[(((((triple1) -> rule9) ((((((triple4) -> rule9) triple5) -> rule8)) -> rule2)) -> rule4))]
("bear" "needs" "rabbit" "-")
((((triple1) -> (rule9 % int5)) ((((((triple4) -> (rule9 % int4)) triple5) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int1
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
int2
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int3
The cow eats the bear.
("cow" "eats" "bear" "+")
int4
The bear eats the bear.
("bear" "eats" "bear" "+")
int5
The bear needs the bear.
True
9
proof
[(((((((triple1) -> rule9) ((((((triple4) -> rule9) triple5) -> rule8)) -> rule2)) -> rule4)) -> rule1))]
("bear" "needs" "bear" "+")
((((((triple1) -> (rule9 % int6)) ((((((triple4) -> (rule9 % int5)) triple5) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int2
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
int3
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int4
The cow eats the bear.
("cow" "eats" "bear" "+")
int5
The bear eats the bear.
("bear" "eats" "bear" "+")
int6
The bear does not need the bear.
False
9
inv-proof
[(((((((triple1) -> rule9) ((((((triple4) -> rule9) triple5) -> rule8)) -> rule2)) -> rule4)) -> rule1))]
("bear" "needs" "bear" "-")
((((((triple1) -> (rule9 % int6)) ((((((triple4) -> (rule9 % int5)) triple5) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int2
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
int3
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int4
The cow eats the bear.
("cow" "eats" "bear" "+")
int5
The bear eats the bear.
("bear" "eats" "bear" "+")
int6
The bear does not see the squirrel.
Unknown
inv-rconc
[@1: The bear sees the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "sees" "squirrel" "-")
The cow sees the squirrel.
Unknown
rconc
[@1: The cow sees the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "sees" "squirrel" "+")
The rabbit does not need the rabbit.
Unknown
inv-rconc
[@2: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("rabbit" "needs" "rabbit" "-")
The rabbit is cold.
Unknown
rconc
[@1: The rabbit is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "is" "cold" "+")
The squirrel does not see the squirrel.
Unknown
inv-rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "sees" "squirrel" "-")
The cow needs the rabbit.
Unknown
rconc
[@2: The cow needs the rabbit.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("cow" "needs" "rabbit" "+")
The rabbit is not green.
Unknown
inv-random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "-")
The bear sees the cow.
Unknown
random
[@0: The bear sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "cow" "+")
The squirrel does not eat the cow.
Unknown
inv-random
[@0: The squirrel eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "cow" "-")
The squirrel needs the cow.
Unknown
random
[@0: The squirrel needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "cow" "+")
The bear is not round.
Unknown
inv-random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
@0: The bear is kind.[(triple1)] The bear needs the squirrel.[(triple2)] The cow is cold.[(triple3)] The cow is kind.[(triple4)] The cow is nice.[(triple5)] The cow sees the bear.[(triple6)] The rabbit eats the bear.[(triple7)] The rabbit eats the cow.[(triple8)] The rabbit is round.[(triple9)] The squirrel eats the bear.[(triple10)] The squirrel eats the rabbit.[(triple11)] The squirrel needs the bear.[(triple12 OR ((triple13) -> rule1) OR ((((triple10 ((triple11) -> rule3)) -> rule4)) -> rule1))] The squirrel needs the rabbit.[(triple13 OR ((triple10 ((triple11) -> rule3)) -> rule4))] The squirrel sees the cow.[(triple14)] @1: The bear eats the bear.[(((triple1) -> rule9))] The cow eats the bear.[(((triple4) -> rule9))] The squirrel eats the squirrel.[(((triple11) -> rule3))] @2: The bear sees the rabbit.[(((((triple4) -> rule9) triple5) -> rule8))] @3: The bear eats the squirrel.[(((((((triple4) -> rule9) triple5) -> rule8)) -> rule2))] @4: The bear needs the rabbit.[(((((triple1) -> rule9) ((((((triple4) -> rule9) triple5) -> rule8)) -> rule2)) -> rule4))] @5: The bear needs the bear.[(((((((triple1) -> rule9) ((((((triple4) -> rule9) triple5) -> rule8)) -> rule2)) -> rule4)) -> rule1))]
The bear is kind.
("bear" "is" "kind" "+")
triple1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
triple2
The cow is cold.
("cow" "is" "cold" "+")
triple3
The cow is kind.
("cow" "is" "kind" "+")
triple4
The cow is nice.
("cow" "is" "nice" "+")
triple5
The cow sees the bear.
("cow" "sees" "bear" "+")
triple6
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
triple7
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
triple8
The rabbit is round.
("rabbit" "is" "round" "+")
triple9
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
triple10
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
triple11
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
triple12
((triple13) -> (rule1 % int1))
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int1
((((triple10 ((triple11) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int1
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int3
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple13
((triple10 ((triple11) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
triple14
The bear eats the bear.
("bear" "eats" "bear" "+")
((triple1) -> (rule9 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
((triple4) -> (rule9 % int1))
The cow eats the bear.
("cow" "eats" "bear" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
((triple11) -> (rule3 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
((((triple4) -> (rule9 % int2)) triple5) -> (rule8 % int1))
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
int2
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
((((((triple4) -> (rule9 % int3)) triple5) -> (rule8 % int2))) -> (rule2 % int1))
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
int1
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int2
The cow eats the bear.
("cow" "eats" "bear" "+")
int3
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
((((triple1) -> (rule9 % int5)) ((((((triple4) -> (rule9 % int4)) triple5) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int1
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
int2
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int3
The cow eats the bear.
("cow" "eats" "bear" "+")
int4
The bear eats the bear.
("bear" "eats" "bear" "+")
int5
The bear needs the bear.
("bear" "needs" "bear" "+")
((((((triple1) -> (rule9 % int6)) ((((((triple4) -> (rule9 % int5)) triple5) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int2
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
int3
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int4
The cow eats the bear.
("cow" "eats" "bear" "+")
int5
The bear eats the bear.
("bear" "eats" "bear" "+")
int6