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