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