The bear chases the squirrel. The bear sees the rabbit. The lion is big. The lion is nice. The rabbit chases the bear. The rabbit chases the lion. The rabbit chases the squirrel. The rabbit is blue. The rabbit is round. The squirrel sees the bear. The squirrel sees the lion. The squirrel sees the rabbit. If something likes the bear then the bear chases the rabbit. If something is big then it sees the squirrel. If something chases the lion then the lion sees the rabbit. If something likes the squirrel then the squirrel is round. If something likes the rabbit and the rabbit chases the squirrel then it is big. If something is round then it likes the rabbit. If something chases the lion and the lion likes the bear then it likes the bear. If something chases the squirrel and it chases the bear then it likes the squirrel. If something sees the squirrel then it sees the rabbit.
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is nice.
("lion" "is" "nice" "+")
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
If something likes the bear then the bear chases the rabbit.
((("something" "likes" "bear" "+")) -> ("bear" "chases" "rabbit" "+"))
If something is big then it sees the squirrel.
((("something" "is" "big" "+")) -> ("something" "sees" "squirrel" "+"))
If something chases the lion then the lion sees the rabbit.
((("something" "chases" "lion" "+")) -> ("lion" "sees" "rabbit" "+"))
If something likes the squirrel then the squirrel is round.
((("something" "likes" "squirrel" "+")) -> ("squirrel" "is" "round" "+"))
If something likes the rabbit and the rabbit chases the squirrel then it is big.
((("something" "likes" "rabbit" "+") ("rabbit" "chases" "squirrel" "+")) -> ("something" "is" "big" "+"))
If something is round then it likes the rabbit.
((("something" "is" "round" "+")) -> ("something" "likes" "rabbit" "+"))
If something chases the lion and the lion likes the bear then it likes the bear.
((("something" "chases" "lion" "+") ("lion" "likes" "bear" "+")) -> ("something" "likes" "bear" "+"))
If something chases the squirrel and it chases the bear then it likes the squirrel.
((("something" "chases" "squirrel" "+") ("something" "chases" "bear" "+")) -> ("something" "likes" "squirrel" "+"))
If something sees the squirrel then it sees the rabbit.
((("something" "sees" "squirrel" "+")) -> ("something" "sees" "rabbit" "+"))
The rabbit is round.
True
1
proof
[(triple9)]
("rabbit" "is" "round" "+")
triple9
The rabbit is not round.
False
1
inv-proof
[(triple9)]
("rabbit" "is" "round" "-")
triple9
The rabbit likes the rabbit.
True
2
proof
[(((triple9) -> rule6))]
("rabbit" "likes" "rabbit" "+")
((triple9) -> (rule6 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The lion does not see the rabbit.
False
2
inv-proof
[(((triple6) -> rule3) OR ((((triple3) -> rule2)) -> rule9))]
("lion" "sees" "rabbit" "-")
((triple6) -> (rule3 % int1))
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule9 % int1))
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int2
The rabbit is big.
True
4
proof
[(((((triple9) -> rule6) triple7) -> rule5))]
("rabbit" "is" "big" "+")
((((triple9) -> (rule6 % int2)) triple7) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The squirrel is not round.
False
4
inv-proof
[(((((triple7 triple5) -> rule8)) -> rule4))]
("squirrel" "is" "round" "-")
((((triple7 triple5) -> (rule8 % int2))) -> (rule4 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int2
The squirrel likes the rabbit.
True
5
proof
[(((((((triple7 triple5) -> rule8)) -> rule4)) -> rule6))]
("squirrel" "likes" "rabbit" "+")
((((((triple7 triple5) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int3
The squirrel does not like the rabbit.
False
5
inv-proof
[(((((((triple7 triple5) -> rule8)) -> rule4)) -> rule6))]
("squirrel" "likes" "rabbit" "-")
((((((triple7 triple5) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int3
The rabbit sees the rabbit.
True
6
proof
[(((((((((triple9) -> rule6) triple7) -> rule5)) -> rule2)) -> rule9))]
("rabbit" "sees" "rabbit" "+")
((((((((triple9) -> (rule6 % int4)) triple7) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int4
The squirrel is not big.
False
7
inv-proof
[(((((((((triple7 triple5) -> rule8)) -> rule4)) -> rule6) triple7) -> rule5))]
("squirrel" "is" "big" "-")
((((((((triple7 triple5) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule6 % int2)) triple7) -> (rule5 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int4
The squirrel sees the squirrel.
True
8
proof
[(((((((((((triple7 triple5) -> rule8)) -> rule4)) -> rule6) triple7) -> rule5)) -> rule2))]
("squirrel" "sees" "squirrel" "+")
((((((((((triple7 triple5) -> (rule8 % int5))) -> (rule4 % int4))) -> (rule6 % int3)) triple7) -> (rule5 % int2))) -> (rule2 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int3
The squirrel is round.
("squirrel" "is" "round" "+")
int4
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int5
The squirrel does not see the squirrel.
False
8
inv-proof
[(((((((((((triple7 triple5) -> rule8)) -> rule4)) -> rule6) triple7) -> rule5)) -> rule2))]
("squirrel" "sees" "squirrel" "-")
((((((((((triple7 triple5) -> (rule8 % int5))) -> (rule4 % int4))) -> (rule6 % int3)) triple7) -> (rule5 % int2))) -> (rule2 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int3
The squirrel is round.
("squirrel" "is" "round" "+")
int4
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int5
The lion does not like the squirrel.
Unknown
inv-rconc
[@1: The lion likes the squirrel.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "likes" "squirrel" "-")
The bear likes the squirrel.
Unknown
rconc
[@1: The bear likes the squirrel.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "likes" "squirrel" "+")
The bear is not big.
Unknown
inv-rconc
[@2: The bear is big.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("bear" "is" "big" "-")
The bear chases the rabbit.
Unknown
rconc
[@2: The bear chases the rabbit.[CWA. Example of deepest failure = (rule1 <- rule7 <- FAIL)]]
("bear" "chases" "rabbit" "+")
The lion does not like the rabbit.
Unknown
inv-rconc
[@1: The lion likes the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "likes" "rabbit" "-")
The bear likes the bear.
Unknown
rconc
[@1: The bear likes the bear.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "likes" "bear" "+")
The lion is not rough.
Unknown
inv-random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "-")
The squirrel chases the rabbit.
Unknown
random
[@0: The squirrel chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "rabbit" "+")
The lion does not see the bear.
Unknown
inv-random
[@0: The lion sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "bear" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
The rabbit does not chase the rabbit.
Unknown
inv-random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "-")
The bear chases the lion.
Unknown
random
[@0: The bear chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "lion" "+")
@0: The bear chases the squirrel.[(triple1)] The bear sees the rabbit.[(triple2)] The lion is big.[(triple3)] The lion is nice.[(triple4)] The rabbit chases the bear.[(triple5)] The rabbit chases the lion.[(triple6)] The rabbit chases the squirrel.[(triple7)] The rabbit is blue.[(triple8)] The rabbit is round.[(triple9)] The squirrel sees the bear.[(triple10)] The squirrel sees the lion.[(triple11)] The squirrel sees the rabbit.[(triple12 OR ((((((((((((triple7 triple5) -> rule8)) -> rule4)) -> rule6) triple7) -> rule5)) -> rule2)) -> rule9))] @1: The lion sees the rabbit.[(((triple6) -> rule3) OR ((((triple3) -> rule2)) -> rule9))] The lion sees the squirrel.[(((triple3) -> rule2))] The rabbit likes the rabbit.[(((triple9) -> rule6))] The rabbit likes the squirrel.[(((triple7 triple5) -> rule8))] @2: The rabbit is big.[(((((triple9) -> rule6) triple7) -> rule5))] The squirrel is round.[(((((triple7 triple5) -> rule8)) -> rule4))] @3: The rabbit sees the squirrel.[(((((((triple9) -> rule6) triple7) -> rule5)) -> rule2))] The squirrel likes the rabbit.[(((((((triple7 triple5) -> rule8)) -> rule4)) -> rule6))] @4: The rabbit sees the rabbit.[(((((((((triple9) -> rule6) triple7) -> rule5)) -> rule2)) -> rule9))] The squirrel is big.[(((((((((triple7 triple5) -> rule8)) -> rule4)) -> rule6) triple7) -> rule5))] @5: The squirrel sees the squirrel.[(((((((((((triple7 triple5) -> rule8)) -> rule4)) -> rule6) triple7) -> rule5)) -> rule2))]
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
triple1
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
triple2
The lion is big.
("lion" "is" "big" "+")
triple3
The lion is nice.
("lion" "is" "nice" "+")
triple4
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
triple5
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple6
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
triple7
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple8
The rabbit is round.
("rabbit" "is" "round" "+")
triple9
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple10
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple11
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple12
((((((((((((triple7 triple5) -> (rule8 % int6))) -> (rule4 % int5))) -> (rule6 % int4)) triple7) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
int3
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int4
The squirrel is round.
("squirrel" "is" "round" "+")
int5
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int6
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
((triple6) -> (rule3 % int1))
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule9 % int1))
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int2
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
((triple3) -> (rule2 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((triple9) -> (rule6 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
((triple7 triple5) -> (rule8 % int1))
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
((((triple9) -> (rule6 % int2)) triple7) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
((((triple7 triple5) -> (rule8 % int2))) -> (rule4 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
((((((triple9) -> (rule6 % int3)) triple7) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int3
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
((((((triple7 triple5) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int3
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((((((((triple9) -> (rule6 % int4)) triple7) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int4
The squirrel is big.
("squirrel" "is" "big" "+")
((((((((triple7 triple5) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule6 % int2)) triple7) -> (rule5 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int4
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((((((((((triple7 triple5) -> (rule8 % int5))) -> (rule4 % int4))) -> (rule6 % int3)) triple7) -> (rule5 % int2))) -> (rule2 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int3
The squirrel is round.
("squirrel" "is" "round" "+")
int4
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int5