The bear chases the lion. The bear sees the squirrel. The lion chases the squirrel. The lion is nice. The lion is round. The squirrel chases the bear. The squirrel chases the lion. The squirrel is cold. The squirrel is nice. The squirrel likes the bear. The squirrel likes the lion. The squirrel sees the bear. If someone sees the squirrel and they chase the bear then they are cold. If someone sees the bear and the bear is red then the bear likes the squirrel. If someone likes the lion and they like the bear then the bear is blue. If someone is cold then they like the bear. If the bear sees the lion and the bear is nice then the bear chases the lion. All blue people are cold.
The bear chases the lion.
("bear" "chases" "lion" "+")
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is round.
("lion" "is" "round" "+")
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
If someone sees the squirrel and they chase the bear then they are cold.
((("someone" "sees" "squirrel" "+") ("someone" "chases" "bear" "+")) -> ("someone" "is" "cold" "+"))
If someone sees the bear and the bear is red then the bear likes the squirrel.
((("someone" "sees" "bear" "+") ("bear" "is" "red" "+")) -> ("bear" "likes" "squirrel" "+"))
If someone likes the lion and they like the bear then the bear is blue.
((("someone" "likes" "lion" "+") ("someone" "likes" "bear" "+")) -> ("bear" "is" "blue" "+"))
If someone is cold then they like the bear.
((("someone" "is" "cold" "+")) -> ("someone" "likes" "bear" "+"))
If the bear sees the lion and the bear is nice then the bear chases the lion.
((("bear" "sees" "lion" "+") ("bear" "is" "nice" "+")) -> ("bear" "chases" "lion" "+"))
All blue people are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
The squirrel sees the bear.
True
1
proof
[(triple12)]
("squirrel" "sees" "bear" "+")
triple12
The squirrel does not chase the bear.
False
1
inv-proof
[(triple6)]
("squirrel" "chases" "bear" "-")
triple6
The bear is blue.
True
3
proof
[(((triple11 triple10) -> rule3) OR ((triple11 ((triple8) -> rule4)) -> rule3))]
("bear" "is" "blue" "+")
((triple11 triple10) -> (rule3 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
((triple11 ((triple8) -> (rule4 % int2))) -> (rule3 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int2
The bear is not blue.
False
3
inv-proof
[(((triple11 triple10) -> rule3) OR ((triple11 ((triple8) -> rule4)) -> rule3))]
("bear" "is" "blue" "-")
((triple11 triple10) -> (rule3 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
((triple11 ((triple8) -> (rule4 % int2))) -> (rule3 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int2
The bear is cold.
True
4
proof
[(((((triple11 triple10) -> rule3)) -> rule6) OR ((((triple11 ((triple8) -> rule4)) -> rule3)) -> rule6))]
("bear" "is" "cold" "+")
((((triple11 triple10) -> (rule3 % int2))) -> (rule6 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
((((triple11 ((triple8) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int3
The bear is not cold.
False
4
inv-proof
[(((((triple11 triple10) -> rule3)) -> rule6) OR ((((triple11 ((triple8) -> rule4)) -> rule3)) -> rule6))]
("bear" "is" "cold" "-")
((((triple11 triple10) -> (rule3 % int2))) -> (rule6 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
((((triple11 ((triple8) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int3
The bear likes the bear.
True
5
proof
[(((((((triple11 triple10) -> rule3)) -> rule6)) -> rule4) OR ((((((triple11 ((triple8) -> rule4)) -> rule3)) -> rule6)) -> rule4))]
("bear" "likes" "bear" "+")
((((((triple11 triple10) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
((((((triple11 ((triple8) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int4
The bear does not like the bear.
False
5
inv-proof
[(((((((triple11 triple10) -> rule3)) -> rule6)) -> rule4) OR ((((((triple11 ((triple8) -> rule4)) -> rule3)) -> rule6)) -> rule4))]
("bear" "likes" "bear" "-")
((((((triple11 triple10) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
((((((triple11 ((triple8) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int4
The lion is not cold.
Unknown
inv-rconc
[@1: The lion is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "cold" "-")
The lion likes the bear.
Unknown
rconc
[@2: The lion likes the bear.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("lion" "likes" "bear" "+")
The bear does not like the squirrel.
Unknown
inv-rconc
[@1: The bear likes the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "likes" "squirrel" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
The squirrel is not red.
Unknown
inv-random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "-")
The bear chases the squirrel.
Unknown
random
[@0: The bear chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "squirrel" "+")
The bear does not see the bear.
Unknown
inv-random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
@0: The bear chases the lion.[(triple1)] The bear sees the squirrel.[(triple2)] The lion chases the squirrel.[(triple3)] The lion is nice.[(triple4)] The lion is round.[(triple5)] The squirrel chases the bear.[(triple6)] The squirrel chases the lion.[(triple7)] The squirrel is cold.[(triple8)] The squirrel is nice.[(triple9)] The squirrel likes the bear.[(triple10 OR ((triple8) -> rule4))] The squirrel likes the lion.[(triple11)] The squirrel sees the bear.[(triple12)] @1: The bear is blue.[(((triple11 triple10) -> rule3) OR ((triple11 ((triple8) -> rule4)) -> rule3))] @2: The bear is cold.[(((((triple11 triple10) -> rule3)) -> rule6) OR ((((triple11 ((triple8) -> rule4)) -> rule3)) -> rule6))] @3: The bear likes the bear.[(((((((triple11 triple10) -> rule3)) -> rule6)) -> rule4) OR ((((((triple11 ((triple8) -> rule4)) -> rule3)) -> rule6)) -> rule4))]
The bear chases the lion.
("bear" "chases" "lion" "+")
triple1
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple3
The lion is nice.
("lion" "is" "nice" "+")
triple4
The lion is round.
("lion" "is" "round" "+")
triple5
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
triple6
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
triple7
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple8
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple9
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
triple10
((triple8) -> (rule4 % int1))
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int1
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
triple11
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple12
The bear is blue.
("bear" "is" "blue" "+")
((triple11 triple10) -> (rule3 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
((triple11 ((triple8) -> (rule4 % int2))) -> (rule3 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
((((triple11 triple10) -> (rule3 % int2))) -> (rule6 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
((((triple11 ((triple8) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int3
The bear likes the bear.
("bear" "likes" "bear" "+")
((((((triple11 triple10) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
((((((triple11 ((triple8) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int4