The bald eagle chases the squirrel. The rabbit sees the squirrel. The squirrel chases the bald eagle. If the squirrel needs the rabbit and the squirrel is red then the rabbit needs the squirrel. If something needs the bald eagle and the bald eagle is blue then it chases the bald eagle. If something chases the rabbit then it chases the bald eagle. If something chases the bald eagle then the bald eagle sees the squirrel. If something is round and blue then it sees the bald eagle. If something needs the squirrel and it sees the bald eagle then it sees the rabbit.
The bald eagle chases the squirrel.
("bald eagle" "chases" "squirrel" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel chases the bald eagle.
("squirrel" "chases" "bald eagle" "+")
If the squirrel needs the rabbit and the squirrel is red then the rabbit needs the squirrel.
((("squirrel" "needs" "rabbit" "+") ("squirrel" "is" "red" "+")) -> ("rabbit" "needs" "squirrel" "+"))
If something needs the bald eagle and the bald eagle is blue then it chases the bald eagle.
((("something" "needs" "bald eagle" "+") ("bald eagle" "is" "blue" "+")) -> ("something" "chases" "bald eagle" "+"))
If something chases the rabbit then it chases the bald eagle.
((("something" "chases" "rabbit" "+")) -> ("something" "chases" "bald eagle" "+"))
If something chases the bald eagle then the bald eagle sees the squirrel.
((("something" "chases" "bald eagle" "+")) -> ("bald eagle" "sees" "squirrel" "+"))
If something is round and blue then it sees the bald eagle.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "sees" "bald eagle" "+"))
If something needs the squirrel and it sees the bald eagle then it sees the rabbit.
((("something" "needs" "squirrel" "+") ("something" "sees" "bald eagle" "+")) -> ("something" "sees" "rabbit" "+"))
The squirrel chases the bald eagle.
True
1
proof
[(triple3)]
("squirrel" "chases" "bald eagle" "+")
triple3
The bald eagle does not chase the squirrel.
False
1
inv-proof
[(triple1)]
("bald eagle" "chases" "squirrel" "-")
triple1
The bald eagle sees the squirrel.
True
2
proof
[(((triple3) -> rule4))]
("bald eagle" "sees" "squirrel" "+")
((triple3) -> (rule4 % int1))
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int1
The bald eagle does not see the squirrel.
False
2
inv-proof
[(((triple3) -> rule4))]
("bald eagle" "sees" "squirrel" "-")
((triple3) -> (rule4 % int1))
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int1
The bald eagle does not see the bald eagle.
Unknown
inv-rconc
[@1: The bald eagle sees the bald eagle.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bald eagle" "sees" "bald eagle" "-")
The rabbit chases the bald eagle.
Unknown
rconc
[@1: The rabbit chases the bald eagle.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "chases" "bald eagle" "+")
The squirrel does not see the squirrel.
Unknown
inv-random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
@0: The bald eagle chases the squirrel.[(triple1)] The rabbit sees the squirrel.[(triple2)] The squirrel chases the bald eagle.[(triple3)] @1: The bald eagle sees the squirrel.[(((triple3) -> rule4))]
The bald eagle chases the squirrel.
("bald eagle" "chases" "squirrel" "+")
triple1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple2
The squirrel chases the bald eagle.
("squirrel" "chases" "bald eagle" "+")
triple3
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
((triple3) -> (rule4 % int1))
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int1