The bald eagle does not chase the cat. The bald eagle needs the squirrel. The bald eagle sees the squirrel. The cat chases the bald eagle. The cat chases the squirrel. The cat sees the bald eagle. The rabbit is kind. The rabbit does not see the bald eagle. The squirrel is not kind. The squirrel needs the cat. If the rabbit is kind then the rabbit needs the squirrel. Big, green things are not cold. If something chases the rabbit then it is kind. If the squirrel chases the rabbit and the squirrel does not need the cat then the rabbit does not need the cat. If something chases the squirrel and the squirrel is not green then the squirrel is round. If something needs the cat then it needs the rabbit. If something chases the rabbit then the rabbit sees the squirrel. If something needs the cat then the cat is round.
The bald eagle does not chase the cat.
("bald eagle" "chases" "cat" "-")
The bald eagle needs the squirrel.
("bald eagle" "needs" "squirrel" "+")
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
The cat chases the bald eagle.
("cat" "chases" "bald eagle" "+")
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit does not see the bald eagle.
("rabbit" "sees" "bald eagle" "-")
The squirrel is not kind.
("squirrel" "is" "kind" "-")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
If the rabbit is kind then the rabbit needs the squirrel.
((("rabbit" "is" "kind" "+")) -> ("rabbit" "needs" "squirrel" "+"))
Big, green things are not cold.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "-"))
If something chases the rabbit then it is kind.
((("something" "chases" "rabbit" "+")) -> ("something" "is" "kind" "+"))
If the squirrel chases the rabbit and the squirrel does not need the cat then the rabbit does not need the cat.
((("squirrel" "chases" "rabbit" "+") ("squirrel" "needs" "cat" "~")) -> ("rabbit" "needs" "cat" "-"))
If something chases the squirrel and the squirrel is not green then the squirrel is round.
((("something" "chases" "squirrel" "+") ("squirrel" "is" "green" "~")) -> ("squirrel" "is" "round" "+"))
If something needs the cat then it needs the rabbit.
((("something" "needs" "cat" "+")) -> ("something" "needs" "rabbit" "+"))
If something chases the rabbit then the rabbit sees the squirrel.
((("something" "chases" "rabbit" "+")) -> ("rabbit" "sees" "squirrel" "+"))
If something needs the cat then the cat is round.
((("something" "needs" "cat" "+")) -> ("cat" "is" "round" "+"))
The rabbit is kind.
True
1
proof
[(triple7)]
("rabbit" "is" "kind" "+")
triple7
The squirrel does not need the cat.
False
1
inv-proof
[(triple10)]
("squirrel" "needs" "cat" "-")
triple10
The cat is round.
True
2
proof
[(((triple10) -> rule8))]
("cat" "is" "round" "+")
((triple10) -> (rule8 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The rabbit does not need the squirrel.
False
2
inv-proof
[(((triple7) -> rule1))]
("rabbit" "needs" "squirrel" "-")
((triple7) -> (rule1 % int1))
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
int1
The rabbit does not see the squirrel.
Unknown
inv-rconc
[@1: The rabbit sees the squirrel.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "sees" "squirrel" "-")
The rabbit needs the rabbit.
Unknown
rconc
[@1: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "needs" "rabbit" "+")
The bald eagle does not chase the rabbit.
Unknown
inv-random
[@0: The bald eagle chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "chases" "rabbit" "-")
The rabbit chases the cat.
Unknown
random
[@0: The rabbit chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "cat" "+")
@0: The bald eagle does not chase the cat.[(triple1)] The bald eagle needs the squirrel.[(triple2)] The bald eagle sees the squirrel.[(triple3)] The cat chases the bald eagle.[(triple4)] The cat chases the squirrel.[(triple5)] The cat sees the bald eagle.[(triple6)] The rabbit does not see the bald eagle.[(triple8)] The rabbit is kind.[(triple7)] The squirrel is not kind.[(triple9)] The squirrel needs the cat.[(triple10)] @1: The cat is round.[(((triple10) -> rule8))] The rabbit needs the squirrel.[(((triple7) -> rule1))] The squirrel needs the rabbit.[(((triple10) -> rule6))]
The bald eagle does not chase the cat.
("bald eagle" "chases" "cat" "-")
triple1
The bald eagle needs the squirrel.
("bald eagle" "needs" "squirrel" "+")
triple2
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
triple3
The cat chases the bald eagle.
("cat" "chases" "bald eagle" "+")
triple4
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
triple5
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
triple6
The rabbit does not see the bald eagle.
("rabbit" "sees" "bald eagle" "-")
triple8
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple7
The squirrel is not kind.
("squirrel" "is" "kind" "-")
triple9
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple10
The cat is round.
("cat" "is" "round" "+")
((triple10) -> (rule8 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
((triple7) -> (rule1 % int1))
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
int1
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
((triple10) -> (rule6 % int1))
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int1