The lion is kind. The lion needs the squirrel. The squirrel needs the lion. If something chases the squirrel and it is round then the squirrel is kind. If something needs the lion and it is round then the lion needs the squirrel. If something sees the squirrel then the squirrel is red. If something sees the lion and the lion needs the squirrel then the lion chases the squirrel. If something needs the squirrel then the squirrel chases the lion. If something needs the squirrel and the squirrel chases the lion then the squirrel sees the lion.
The lion is kind.
("lion" "is" "kind" "+")
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
If something chases the squirrel and it is round then the squirrel is kind.
((("something" "chases" "squirrel" "+") ("something" "is" "round" "+")) -> ("squirrel" "is" "kind" "+"))
If something needs the lion and it is round then the lion needs the squirrel.
((("something" "needs" "lion" "+") ("something" "is" "round" "+")) -> ("lion" "needs" "squirrel" "+"))
If something sees the squirrel then the squirrel is red.
((("something" "sees" "squirrel" "+")) -> ("squirrel" "is" "red" "+"))
If something sees the lion and the lion needs the squirrel then the lion chases the squirrel.
((("something" "sees" "lion" "+") ("lion" "needs" "squirrel" "+")) -> ("lion" "chases" "squirrel" "+"))
If something needs the squirrel then the squirrel chases the lion.
((("something" "needs" "squirrel" "+")) -> ("squirrel" "chases" "lion" "+"))
If something needs the squirrel and the squirrel chases the lion then the squirrel sees the lion.
((("something" "needs" "squirrel" "+") ("squirrel" "chases" "lion" "+")) -> ("squirrel" "sees" "lion" "+"))
The lion is kind.
True
1
proof
[(triple1)]
("lion" "is" "kind" "+")
triple1
The lion is not kind.
False
1
inv-proof
[(triple1)]
("lion" "is" "kind" "-")
triple1
The squirrel chases the lion.
True
2
proof
[(((triple2) -> rule5))]
("squirrel" "chases" "lion" "+")
((triple2) -> (rule5 % int1))
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int1
The squirrel does not chase the lion.
False
2
inv-proof
[(((triple2) -> rule5))]
("squirrel" "chases" "lion" "-")
((triple2) -> (rule5 % int1))
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int1
The squirrel sees the lion.
True
4
proof
[(((triple2 ((triple2) -> rule5)) -> rule6))]
("squirrel" "sees" "lion" "+")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int2
The squirrel does not see the lion.
False
4
inv-proof
[(((triple2 ((triple2) -> rule5)) -> rule6))]
("squirrel" "sees" "lion" "-")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int2
The lion chases the squirrel.
True
6
proof
[(((((triple2 ((triple2) -> rule5)) -> rule6) triple2) -> rule4))]
("lion" "chases" "squirrel" "+")
((((triple2 ((triple2) -> (rule5 % int3))) -> (rule6 % int2)) triple2) -> (rule4 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int3
The lion does not chase the squirrel.
False
6
inv-proof
[(((((triple2 ((triple2) -> rule5)) -> rule6) triple2) -> rule4))]
("lion" "chases" "squirrel" "-")
((((triple2 ((triple2) -> (rule5 % int3))) -> (rule6 % int2)) triple2) -> (rule4 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int3
The squirrel is not kind.
Unknown
inv-rconc
[@1: The squirrel is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "kind" "-")
The squirrel is red.
Unknown
rconc
[@1: The squirrel is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "red" "+")
The lion is not red.
Unknown
inv-random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
The squirrel is not rough.
Unknown
inv-random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "-")
The squirrel is big.
Unknown
random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "+")
The lion is not big.
Unknown
inv-random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
@0: The lion is kind.[(triple1)] The lion needs the squirrel.[(triple2)] The squirrel needs the lion.[(triple3)] @1: The squirrel chases the lion.[(((triple2) -> rule5))] @2: The squirrel sees the lion.[(((triple2 ((triple2) -> rule5)) -> rule6))] @3: The lion chases the squirrel.[(((((triple2 ((triple2) -> rule5)) -> rule6) triple2) -> rule4))]
The lion is kind.
("lion" "is" "kind" "+")
triple1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple2
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple3
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
((triple2) -> (rule5 % int1))
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
((((triple2 ((triple2) -> (rule5 % int3))) -> (rule6 % int2)) triple2) -> (rule4 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int3