The lion chases the squirrel. The rabbit is round. The squirrel likes the rabbit. If something chases the squirrel and it sees the rabbit then the rabbit chases the lion. If something chases the lion then it likes the rabbit. If something is round and it chases the lion then the lion chases the rabbit. If something is blue and kind then it chases the lion. If something likes the squirrel and the squirrel is round then it likes the lion. If something likes the rabbit then it is blue. If something is round then it sees the squirrel. If something sees the rabbit then the rabbit sees the squirrel.
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
If something chases the squirrel and it sees the rabbit then the rabbit chases the lion.
((("something" "chases" "squirrel" "+") ("something" "sees" "rabbit" "+")) -> ("rabbit" "chases" "lion" "+"))
If something chases the lion then it likes the rabbit.
((("something" "chases" "lion" "+")) -> ("something" "likes" "rabbit" "+"))
If something is round and it chases the lion then the lion chases the rabbit.
((("something" "is" "round" "+") ("something" "chases" "lion" "+")) -> ("lion" "chases" "rabbit" "+"))
If something is blue and kind then it chases the lion.
((("something" "is" "blue" "+") ("something" "is" "kind" "+")) -> ("something" "chases" "lion" "+"))
If something likes the squirrel and the squirrel is round then it likes the lion.
((("something" "likes" "squirrel" "+") ("squirrel" "is" "round" "+")) -> ("something" "likes" "lion" "+"))
If something likes the rabbit then it is blue.
((("something" "likes" "rabbit" "+")) -> ("something" "is" "blue" "+"))
If something is round then it sees the squirrel.
((("something" "is" "round" "+")) -> ("something" "sees" "squirrel" "+"))
If something sees the rabbit then the rabbit sees the squirrel.
((("something" "sees" "rabbit" "+")) -> ("rabbit" "sees" "squirrel" "+"))
The lion chases the squirrel.
True
1
proof
[(triple1)]
("lion" "chases" "squirrel" "+")
triple1
The rabbit is not round.
False
1
inv-proof
[(triple2)]
("rabbit" "is" "round" "-")
triple2
The rabbit sees the squirrel.
True
2
proof
[(((triple2) -> rule7))]
("rabbit" "sees" "squirrel" "+")
((triple2) -> (rule7 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The rabbit does not see the squirrel.
False
2
inv-proof
[(((triple2) -> rule7))]
("rabbit" "sees" "squirrel" "-")
((triple2) -> (rule7 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The rabbit is not blue.
Unknown
inv-rconc
[@3: The rabbit is blue.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule1 <- FAIL)]]
("rabbit" "is" "blue" "-")
The lion sees the squirrel.
Unknown
rconc
[@1: The lion sees the squirrel.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "sees" "squirrel" "+")
The rabbit does not like the squirrel.
Unknown
inv-random
[@0: The rabbit likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "squirrel" "-")
The squirrel chases the rabbit.
Unknown
random
[@0: The squirrel chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "rabbit" "+")
@0: The lion chases the squirrel.[(triple1)] The rabbit is round.[(triple2)] The squirrel likes the rabbit.[(triple3)] @1: The rabbit sees the squirrel.[(((triple2) -> rule7))] The squirrel is blue.[(((triple3) -> rule6))]
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple1
The rabbit is round.
("rabbit" "is" "round" "+")
triple2
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
triple3
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
((triple2) -> (rule7 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
((triple3) -> (rule6 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1