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