The lion chases the squirrel. The rabbit sees the lion. The squirrel is cold. If someone is green and they see the rabbit then they are rough. If someone likes the lion and the lion chases the squirrel then the lion likes the rabbit. If someone chases the squirrel then they are round. If someone is round then they see the rabbit. If someone sees the squirrel and the squirrel chases the rabbit then the rabbit is rough. If the rabbit is rough then the rabbit chases the lion.
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
If someone is green and they see the rabbit then they are rough.
((("someone" "is" "green" "+") ("someone" "sees" "rabbit" "+")) -> ("someone" "is" "rough" "+"))
If someone likes the lion and the lion chases the squirrel then the lion likes the rabbit.
((("someone" "likes" "lion" "+") ("lion" "chases" "squirrel" "+")) -> ("lion" "likes" "rabbit" "+"))
If someone chases the squirrel then they are round.
((("someone" "chases" "squirrel" "+")) -> ("someone" "is" "round" "+"))
If someone is round then they see the rabbit.
((("someone" "is" "round" "+")) -> ("someone" "sees" "rabbit" "+"))
If someone sees the squirrel and the squirrel chases the rabbit then the rabbit is rough.
((("someone" "sees" "squirrel" "+") ("squirrel" "chases" "rabbit" "+")) -> ("rabbit" "is" "rough" "+"))
If the rabbit is rough then the rabbit chases the lion.
((("rabbit" "is" "rough" "+")) -> ("rabbit" "chases" "lion" "+"))
The lion chases the squirrel.
True
1
proof
[(triple1)]
("lion" "chases" "squirrel" "+")
triple1
The squirrel is not cold.
False
1
inv-proof
[(triple3)]
("squirrel" "is" "cold" "-")
triple3
The lion is round.
True
2
proof
[(((triple1) -> rule3))]
("lion" "is" "round" "+")
((triple1) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is not round.
False
2
inv-proof
[(((triple1) -> rule3))]
("lion" "is" "round" "-")
((triple1) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion sees the rabbit.
True
3
proof
[(((((triple1) -> rule3)) -> rule4))]
("lion" "sees" "rabbit" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion does not see the rabbit.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule4))]
("lion" "sees" "rabbit" "-")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The rabbit is not round.
Unknown
inv-rconc
[@1: The rabbit is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "round" "-")
The squirrel is round.
Unknown
rconc
[@1: The squirrel is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "round" "+")
The squirrel does not see the rabbit.
Unknown
inv-rconc
[@2: The squirrel sees the rabbit.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("squirrel" "sees" "rabbit" "-")
The rabbit likes the squirrel.
Unknown
random
[@0: The rabbit likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "squirrel" "+")
The rabbit is not green.
Unknown
inv-random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
@0: The lion chases the squirrel.[(triple1)] The rabbit sees the lion.[(triple2)] The squirrel is cold.[(triple3)] @1: The lion is round.[(((triple1) -> rule3))] @2: The lion sees the rabbit.[(((((triple1) -> rule3)) -> rule4))]
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple2
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple3
The lion is round.
("lion" "is" "round" "+")
((triple1) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2