The lion is nice. The lion likes the squirrel. The lion needs the squirrel. The lion sees the squirrel. The squirrel is cold. The squirrel is green. The squirrel is nice. The squirrel likes the lion. The squirrel needs the lion. The squirrel sees the lion. If the lion is green then the lion sees the squirrel. If someone needs the lion then the lion sees the squirrel. If someone sees the squirrel then the squirrel sees the lion. If the squirrel needs the lion then the squirrel is rough. If someone is green and they need the lion then they see the lion. If someone sees the lion then they like the lion. If someone sees the lion and the lion likes the squirrel then they are rough. If someone is rough then they like the squirrel.
The lion is nice.
("lion" "is" "nice" "+")
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
If the lion is green then the lion sees the squirrel.
((("lion" "is" "green" "+")) -> ("lion" "sees" "squirrel" "+"))
If someone needs the lion then the lion sees the squirrel.
((("someone" "needs" "lion" "+")) -> ("lion" "sees" "squirrel" "+"))
If someone sees the squirrel then the squirrel sees the lion.
((("someone" "sees" "squirrel" "+")) -> ("squirrel" "sees" "lion" "+"))
If the squirrel needs the lion then the squirrel is rough.
((("squirrel" "needs" "lion" "+")) -> ("squirrel" "is" "rough" "+"))
If someone is green and they need the lion then they see the lion.
((("someone" "is" "green" "+") ("someone" "needs" "lion" "+")) -> ("someone" "sees" "lion" "+"))
If someone sees the lion then they like the lion.
((("someone" "sees" "lion" "+")) -> ("someone" "likes" "lion" "+"))
If someone sees the lion and the lion likes the squirrel then they are rough.
((("someone" "sees" "lion" "+") ("lion" "likes" "squirrel" "+")) -> ("someone" "is" "rough" "+"))
If someone is rough then they like the squirrel.
((("someone" "is" "rough" "+")) -> ("someone" "likes" "squirrel" "+"))
The squirrel likes the lion.
True
1
proof
[(triple8 OR ((triple10) -> rule6) OR ((((triple4) -> rule3)) -> rule6) OR ((((triple6 triple9) -> rule5)) -> rule6) OR ((((((triple9) -> rule2)) -> rule3)) -> rule6))]
("squirrel" "likes" "lion" "+")
triple8
((triple10) -> (rule6 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
((((triple6 triple9) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
((((((triple9) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int3
The squirrel is not nice.
False
1
inv-proof
[(triple7)]
("squirrel" "is" "nice" "-")
triple7
The lion does not like the lion.
Unknown
inv-rconc
[@2: The lion likes the lion.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("lion" "likes" "lion" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
@0: The lion is nice.[(triple1)] The lion likes the squirrel.[(triple2)] The lion needs the squirrel.[(triple3)] The lion sees the squirrel.[(triple4 OR ((triple9) -> rule2))] The squirrel is cold.[(triple5)] The squirrel is green.[(triple6)] The squirrel is nice.[(triple7)] The squirrel likes the lion.[(triple8 OR ((triple10) -> rule6) OR ((((triple4) -> rule3)) -> rule6) OR ((((triple6 triple9) -> rule5)) -> rule6) OR ((((((triple9) -> rule2)) -> rule3)) -> rule6))] The squirrel needs the lion.[(triple9)] The squirrel sees the lion.[(triple10 OR ((triple4) -> rule3) OR ((triple6 triple9) -> rule5) OR ((((triple9) -> rule2)) -> rule3))] @1: The squirrel is rough.[(((triple9) -> rule4) OR ((triple10 triple2) -> rule7) OR ((((triple4) -> rule3) triple2) -> rule7) OR ((((triple6 triple9) -> rule5) triple2) -> rule7) OR ((((((triple9) -> rule2)) -> rule3) triple2) -> rule7))] @2: The squirrel likes the squirrel.[(((((triple9) -> rule4)) -> rule8) OR ((((triple10 triple2) -> rule7)) -> rule8) OR ((((((triple4) -> rule3) triple2) -> rule7)) -> rule8) OR ((((((triple6 triple9) -> rule5) triple2) -> rule7)) -> rule8) OR ((((((((triple9) -> rule2)) -> rule3) triple2) -> rule7)) -> rule8))]
The lion is nice.
("lion" "is" "nice" "+")
triple1
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
triple2
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple3
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple4
((triple9) -> (rule2 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple5
The squirrel is green.
("squirrel" "is" "green" "+")
triple6
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple7
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
triple8
((triple10) -> (rule6 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
((((triple6 triple9) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
((((((triple9) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int3
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple9
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple10
((triple4) -> (rule3 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
((triple6 triple9) -> (rule5 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
((((triple9) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
((triple9) -> (rule4 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
((triple10 triple2) -> (rule7 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
((((triple4) -> (rule3 % int2)) triple2) -> (rule7 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
((((triple6 triple9) -> (rule5 % int2)) triple2) -> (rule7 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
((((((triple9) -> (rule2 % int3))) -> (rule3 % int2)) triple2) -> (rule7 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int3
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
((((triple9) -> (rule4 % int2))) -> (rule8 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
((((triple10 triple2) -> (rule7 % int2))) -> (rule8 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
((((((triple4) -> (rule3 % int3)) triple2) -> (rule7 % int2))) -> (rule8 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int3
((((((triple6 triple9) -> (rule5 % int3)) triple2) -> (rule7 % int2))) -> (rule8 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int3
((((((((triple9) -> (rule2 % int4))) -> (rule3 % int3)) triple2) -> (rule7 % int2))) -> (rule8 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int3
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int4