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