The lion likes the rabbit. The rabbit chases the squirrel. The rabbit is blue. The rabbit is cold. The squirrel chases the rabbit. The squirrel is cold. The squirrel is green. The squirrel likes the lion. The squirrel sees the lion. The squirrel sees the rabbit. If something chases the lion then the lion is young. If something chases the lion then the lion sees the squirrel. If something chases the squirrel then the squirrel chases the lion.
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
If something chases the lion then the lion is young.
((("something" "chases" "lion" "+")) -> ("lion" "is" "young" "+"))
If something chases the lion then the lion sees the squirrel.
((("something" "chases" "lion" "+")) -> ("lion" "sees" "squirrel" "+"))
If something chases the squirrel then the squirrel chases the lion.
((("something" "chases" "squirrel" "+")) -> ("squirrel" "chases" "lion" "+"))
The squirrel chases the rabbit.
True
1
proof
[(triple5)]
("squirrel" "chases" "rabbit" "+")
triple5
The squirrel does not see the rabbit.
False
1
inv-proof
[(triple10)]
("squirrel" "sees" "rabbit" "-")
triple10
The squirrel chases the lion.
True
2
proof
[(((triple2) -> rule3))]
("squirrel" "chases" "lion" "+")
((triple2) -> (rule3 % int1))
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int1
The squirrel does not chase the lion.
False
2
inv-proof
[(((triple2) -> rule3))]
("squirrel" "chases" "lion" "-")
((triple2) -> (rule3 % int1))
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int1
The lion is young.
True
3
proof
[(((((triple2) -> rule3)) -> rule1))]
("lion" "is" "young" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int2
The lion is not young.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule1))]
("lion" "is" "young" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int2
The rabbit is not young.
Unknown
inv-random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "-")
The lion chases the rabbit.
Unknown
random
[@0: The lion chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "rabbit" "+")
The rabbit does not chase the lion.
Unknown
inv-random
[@0: The rabbit chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "lion" "-")
The squirrel is blue.
Unknown
random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "+")
The squirrel is not red.
Unknown
inv-random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "-")
The lion is cold.
Unknown
random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "+")
@0: The lion likes the rabbit.[(triple1)] The rabbit chases the squirrel.[(triple2)] The rabbit is blue.[(triple3)] The rabbit is cold.[(triple4)] The squirrel chases the rabbit.[(triple5)] The squirrel is cold.[(triple6)] The squirrel is green.[(triple7)] The squirrel likes the lion.[(triple8)] The squirrel sees the lion.[(triple9)] The squirrel sees the rabbit.[(triple10)] @1: The squirrel chases the lion.[(((triple2) -> rule3))] @2: The lion is young.[(((((triple2) -> rule3)) -> rule1))] The lion sees the squirrel.[(((((triple2) -> rule3)) -> rule2))]
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple1
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
triple2
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple3
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple4
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
triple5
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple6
The squirrel is green.
("squirrel" "is" "green" "+")
triple7
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
triple8
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple9
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple10
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
((triple2) -> (rule3 % int1))
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int1
The lion is young.
("lion" "is" "young" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int2
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int2