The bear is green. The lion eats the squirrel. The lion is rough. The lion likes the tiger. The lion sees the bear. The lion sees the tiger. The squirrel eats the lion. The squirrel is red. The squirrel sees the tiger. The tiger eats the lion. The tiger likes the squirrel. The tiger sees the lion. If someone likes the bear and they eat the squirrel then the squirrel likes the lion. If someone is green then they eat the tiger. If the tiger likes the squirrel and the tiger likes the bear then the bear sees the lion. If the lion is kind then the lion likes the squirrel. If someone sees the lion then they see the tiger. If the bear is red then the bear eats the lion. If someone is red and they eat the tiger then the tiger likes the bear. If someone eats the squirrel then the squirrel is green.
The bear is green.
("bear" "is" "green" "+")
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If someone likes the bear and they eat the squirrel then the squirrel likes the lion.
((("someone" "likes" "bear" "+") ("someone" "eats" "squirrel" "+")) -> ("squirrel" "likes" "lion" "+"))
If someone is green then they eat the tiger.
((("someone" "is" "green" "+")) -> ("someone" "eats" "tiger" "+"))
If the tiger likes the squirrel and the tiger likes the bear then the bear sees the lion.
((("tiger" "likes" "squirrel" "+") ("tiger" "likes" "bear" "+")) -> ("bear" "sees" "lion" "+"))
If the lion is kind then the lion likes the squirrel.
((("lion" "is" "kind" "+")) -> ("lion" "likes" "squirrel" "+"))
If someone sees the lion then they see the tiger.
((("someone" "sees" "lion" "+")) -> ("someone" "sees" "tiger" "+"))
If the bear is red then the bear eats the lion.
((("bear" "is" "red" "+")) -> ("bear" "eats" "lion" "+"))
If someone is red and they eat the tiger then the tiger likes the bear.
((("someone" "is" "red" "+") ("someone" "eats" "tiger" "+")) -> ("tiger" "likes" "bear" "+"))
If someone eats the squirrel then the squirrel is green.
((("someone" "eats" "squirrel" "+")) -> ("squirrel" "is" "green" "+"))
The tiger likes the squirrel.
True
1
proof
[(triple11)]
("tiger" "likes" "squirrel" "+")
triple11
The tiger does not like the squirrel.
False
1
inv-proof
[(triple11)]
("tiger" "likes" "squirrel" "-")
triple11
The squirrel is green.
True
2
proof
[(((triple2) -> rule8))]
("squirrel" "is" "green" "+")
((triple2) -> (rule8 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The bear does not eat the tiger.
False
2
inv-proof
[(((triple1) -> rule2))]
("bear" "eats" "tiger" "-")
((triple1) -> (rule2 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
The squirrel eats the tiger.
True
3
proof
[(((((triple2) -> rule8)) -> rule2))]
("squirrel" "eats" "tiger" "+")
((((triple2) -> (rule8 % int2))) -> (rule2 % int1))
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel does not eat the tiger.
False
3
inv-proof
[(((((triple2) -> rule8)) -> rule2))]
("squirrel" "eats" "tiger" "-")
((((triple2) -> (rule8 % int2))) -> (rule2 % int1))
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The tiger likes the bear.
True
5
proof
[(((triple8 ((((triple2) -> rule8)) -> rule2)) -> rule7))]
("tiger" "likes" "bear" "+")
((triple8 ((((triple2) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int2
The squirrel is green.
("squirrel" "is" "green" "+")
int3
The tiger does not like the bear.
False
5
inv-proof
[(((triple8 ((((triple2) -> rule8)) -> rule2)) -> rule7))]
("tiger" "likes" "bear" "-")
((triple8 ((((triple2) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int2
The squirrel is green.
("squirrel" "is" "green" "+")
int3
The bear sees the lion.
True
7
proof
[(((triple11 ((triple8 ((((triple2) -> rule8)) -> rule2)) -> rule7)) -> rule3))]
("bear" "sees" "lion" "+")
((triple11 ((triple8 ((((triple2) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int3
The squirrel is green.
("squirrel" "is" "green" "+")
int4
The bear does not see the lion.
False
7
inv-proof
[(((triple11 ((triple8 ((((triple2) -> rule8)) -> rule2)) -> rule7)) -> rule3))]
("bear" "sees" "lion" "-")
((triple11 ((triple8 ((((triple2) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int3
The squirrel is green.
("squirrel" "is" "green" "+")
int4
The bear sees the tiger.
True
8
proof
[(((((triple11 ((triple8 ((((triple2) -> rule8)) -> rule2)) -> rule7)) -> rule3)) -> rule5))]
("bear" "sees" "tiger" "+")
((((triple11 ((triple8 ((((triple2) -> (rule8 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The bear sees the lion.
("bear" "sees" "lion" "+")
int2
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int3
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int4
The squirrel is green.
("squirrel" "is" "green" "+")
int5
The bear does not see the tiger.
False
8
inv-proof
[(((((triple11 ((triple8 ((((triple2) -> rule8)) -> rule2)) -> rule7)) -> rule3)) -> rule5))]
("bear" "sees" "tiger" "-")
((((triple11 ((triple8 ((((triple2) -> (rule8 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The bear sees the lion.
("bear" "sees" "lion" "+")
int2
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int3
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int4
The squirrel is green.
("squirrel" "is" "green" "+")
int5
The squirrel does not like the lion.
Unknown
inv-rconc
[@1: The squirrel likes the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "likes" "lion" "-")
The lion eats the tiger.
Unknown
rconc
[@1: The lion eats the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "eats" "tiger" "+")
The bear does not eat the lion.
Unknown
inv-rconc
[@1: The bear eats the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "eats" "lion" "-")
The lion likes the squirrel.
Unknown
rconc
[@1: The lion likes the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "likes" "squirrel" "+")
The tiger does not eat the tiger.
Unknown
inv-rconc
[@1: The tiger eats the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "eats" "tiger" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
The squirrel is not rough.
Unknown
inv-random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "-")
The bear likes the squirrel.
Unknown
random
[@0: The bear likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "squirrel" "+")
The squirrel does not see the lion.
Unknown
inv-random
[@0: The squirrel sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "lion" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
The tiger does not eat the bear.
Unknown
inv-random
[@0: The tiger eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "bear" "-")
The tiger eats the squirrel.
Unknown
random
[@0: The tiger eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "squirrel" "+")
@0: The bear is green.[(triple1)] The lion eats the squirrel.[(triple2)] The lion is rough.[(triple3)] The lion likes the tiger.[(triple4)] The lion sees the bear.[(triple5)] The lion sees the tiger.[(triple6)] The squirrel eats the lion.[(triple7)] The squirrel is red.[(triple8)] The squirrel sees the tiger.[(triple9)] The tiger eats the lion.[(triple10)] The tiger likes the squirrel.[(triple11)] The tiger sees the lion.[(triple12)] @1: The bear eats the tiger.[(((triple1) -> rule2))] The squirrel is green.[(((triple2) -> rule8))] The tiger sees the tiger.[(((triple12) -> rule5))] @2: The squirrel eats the tiger.[(((((triple2) -> rule8)) -> rule2))] @3: The tiger likes the bear.[(((triple8 ((((triple2) -> rule8)) -> rule2)) -> rule7))] @4: The bear sees the lion.[(((triple11 ((triple8 ((((triple2) -> rule8)) -> rule2)) -> rule7)) -> rule3))] @5: The bear sees the tiger.[(((((triple11 ((triple8 ((((triple2) -> rule8)) -> rule2)) -> rule7)) -> rule3)) -> rule5))]
The bear is green.
("bear" "is" "green" "+")
triple1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple2
The lion is rough.
("lion" "is" "rough" "+")
triple3
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple4
The lion sees the bear.
("lion" "sees" "bear" "+")
triple5
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple6
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
triple7
The squirrel is red.
("squirrel" "is" "red" "+")
triple8
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple9
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple10
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
triple11
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple12
The bear eats the tiger.
("bear" "eats" "tiger" "+")
((triple1) -> (rule2 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
((triple2) -> (rule8 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((triple12) -> (rule5 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
((((triple2) -> (rule8 % int2))) -> (rule2 % int1))
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The tiger likes the bear.
("tiger" "likes" "bear" "+")
((triple8 ((((triple2) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int2
The squirrel is green.
("squirrel" "is" "green" "+")
int3
The bear sees the lion.
("bear" "sees" "lion" "+")
((triple11 ((triple8 ((((triple2) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int3
The squirrel is green.
("squirrel" "is" "green" "+")
int4
The bear sees the tiger.
("bear" "sees" "tiger" "+")
((((triple11 ((triple8 ((((triple2) -> (rule8 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The bear sees the lion.
("bear" "sees" "lion" "+")
int2
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int3
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int4
The squirrel is green.
("squirrel" "is" "green" "+")
int5