The lion needs the squirrel. The lion sees the rabbit. The lion sees the squirrel. The rabbit is young. The rabbit sees the squirrel. The squirrel chases the lion. The squirrel is round. The squirrel is young. The squirrel needs the lion. The squirrel needs the rabbit. If the rabbit is cold then the rabbit needs the lion. If something chases the lion then it sees the rabbit. If something sees the rabbit and it needs the lion then the rabbit chases the lion.
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
If the rabbit is cold then the rabbit needs the lion.
((("rabbit" "is" "cold" "+")) -> ("rabbit" "needs" "lion" "+"))
If something chases the lion then it sees the rabbit.
((("something" "chases" "lion" "+")) -> ("something" "sees" "rabbit" "+"))
If something sees the rabbit and it needs the lion then the rabbit chases the lion.
((("something" "sees" "rabbit" "+") ("something" "needs" "lion" "+")) -> ("rabbit" "chases" "lion" "+"))
The squirrel is round.
True
1
proof
[(triple7)]
("squirrel" "is" "round" "+")
triple7
The rabbit does not see the squirrel.
False
1
inv-proof
[(triple5)]
("rabbit" "sees" "squirrel" "-")
triple5
The squirrel sees the rabbit.
True
2
proof
[(((triple6) -> rule2))]
("squirrel" "sees" "rabbit" "+")
((triple6) -> (rule2 % int1))
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int1
The squirrel does not see the rabbit.
False
2
inv-proof
[(((triple6) -> rule2))]
("squirrel" "sees" "rabbit" "-")
((triple6) -> (rule2 % int1))
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int1
The rabbit chases the lion.
True
4
proof
[(((((triple6) -> rule2) triple9) -> rule3))]
("rabbit" "chases" "lion" "+")
((((triple6) -> (rule2 % int2)) triple9) -> (rule3 % int1))
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int1
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int2
The rabbit does not chase the lion.
False
4
inv-proof
[(((((triple6) -> rule2) triple9) -> rule3))]
("rabbit" "chases" "lion" "-")
((((triple6) -> (rule2 % int2)) triple9) -> (rule3 % int1))
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int1
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int2
The rabbit sees the rabbit.
True
5
proof
[(((((((triple6) -> rule2) triple9) -> rule3)) -> rule2))]
("rabbit" "sees" "rabbit" "+")
((((((triple6) -> (rule2 % int3)) triple9) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int2
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int3
The rabbit does not see the rabbit.
False
5
inv-proof
[(((((((triple6) -> rule2) triple9) -> rule3)) -> rule2))]
("rabbit" "sees" "rabbit" "-")
((((((triple6) -> (rule2 % int3)) triple9) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int2
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int3
The rabbit does not need the lion.
Unknown
inv-rconc
[@1: The rabbit needs the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "needs" "lion" "-")
The squirrel is cold.
Unknown
random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "+")
The squirrel does not see the lion.
Unknown
inv-random
[@0: The squirrel sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "lion" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
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 lion is red.
Unknown
random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "+")
The lion is not round.
Unknown
inv-random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "-")
The rabbit chases the squirrel.
Unknown
random
[@0: The rabbit chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "squirrel" "+")
@0: The lion needs the squirrel.[(triple1)] The lion sees the rabbit.[(triple2)] The lion sees the squirrel.[(triple3)] The rabbit is young.[(triple4)] The rabbit sees the squirrel.[(triple5)] The squirrel chases the lion.[(triple6)] The squirrel is round.[(triple7)] The squirrel is young.[(triple8)] The squirrel needs the lion.[(triple9)] The squirrel needs the rabbit.[(triple10)] @1: The squirrel sees the rabbit.[(((triple6) -> rule2))] @2: The rabbit chases the lion.[(((((triple6) -> rule2) triple9) -> rule3))] @3: The rabbit sees the rabbit.[(((((((triple6) -> rule2) triple9) -> rule3)) -> rule2))]
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple1
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple2
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple3
The rabbit is young.
("rabbit" "is" "young" "+")
triple4
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple5
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
triple6
The squirrel is round.
("squirrel" "is" "round" "+")
triple7
The squirrel is young.
("squirrel" "is" "young" "+")
triple8
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple9
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple10
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
((triple6) -> (rule2 % int1))
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int1
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
((((triple6) -> (rule2 % int2)) triple9) -> (rule3 % int1))
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int1
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int2
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((((((triple6) -> (rule2 % int3)) triple9) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int2
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int3