The rabbit chases the squirrel. The squirrel chases the rabbit. The squirrel eats the rabbit. The squirrel is blue. The squirrel is cold. The squirrel is not red. The squirrel needs the rabbit. If the rabbit needs the squirrel and the rabbit is not round then the rabbit chases the squirrel. If someone is green then they are red. If someone is green and they need the squirrel then the squirrel does not eat the rabbit. If someone is red then they do not chase the squirrel. If someone is cold then they chase the squirrel. If someone needs the rabbit then they chase the rabbit. If someone chases the squirrel then they do not eat the squirrel. If someone is green and they do not need the rabbit then they do not eat the squirrel.
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is not red.
("squirrel" "is" "red" "-")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
If the rabbit needs the squirrel and the rabbit is not round then the rabbit chases the squirrel.
((("rabbit" "needs" "squirrel" "+") ("rabbit" "is" "round" "~")) -> ("rabbit" "chases" "squirrel" "+"))
If someone is green then they are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
If someone is green and they need the squirrel then the squirrel does not eat the rabbit.
((("someone" "is" "green" "+") ("someone" "needs" "squirrel" "+")) -> ("squirrel" "eats" "rabbit" "-"))
If someone is red then they do not chase the squirrel.
((("someone" "is" "red" "+")) -> ("someone" "chases" "squirrel" "-"))
If someone is cold then they chase the squirrel.
((("someone" "is" "cold" "+")) -> ("someone" "chases" "squirrel" "+"))
If someone needs the rabbit then they chase the rabbit.
((("someone" "needs" "rabbit" "+")) -> ("someone" "chases" "rabbit" "+"))
If someone chases the squirrel then they do not eat the squirrel.
((("someone" "chases" "squirrel" "+")) -> ("someone" "eats" "squirrel" "-"))
If someone is green and they do not need the rabbit then they do not eat the squirrel.
((("someone" "is" "green" "+") ("someone" "needs" "rabbit" "~")) -> ("someone" "eats" "squirrel" "-"))
The squirrel chases the rabbit.
True
1
proof
[(triple2 OR ((triple7) -> rule6))]
("squirrel" "chases" "rabbit" "+")
triple2
((triple7) -> (rule6 % int1))
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int1
The squirrel is red.
False
1
inv-proof
[(triple6)]
("squirrel" "is" "red" "+")
triple6
The squirrel chases the squirrel.
True
2
proof
[(((triple5) -> rule5))]
("squirrel" "chases" "squirrel" "+")
((triple5) -> (rule5 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel does not chase the squirrel.
False
2
inv-proof
[(((triple5) -> rule5))]
("squirrel" "chases" "squirrel" "-")
((triple5) -> (rule5 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel does not eat the squirrel.
True
3
proof
[(((((triple5) -> rule5)) -> rule7))]
("squirrel" "eats" "squirrel" "-")
((((triple5) -> (rule5 % int2))) -> (rule7 % int1))
The squirrel does not eat the squirrel.
("squirrel" "eats" "squirrel" "-")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The squirrel eats the squirrel.
False
3
inv-proof
[(((((triple5) -> rule5)) -> rule7))]
("squirrel" "eats" "squirrel" "+")
((((triple5) -> (rule5 % int2))) -> (rule7 % int1))
The squirrel does not eat the squirrel.
("squirrel" "eats" "squirrel" "-")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The rabbit is not red.
Unknown
inv-rconc
[@1: The rabbit is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "red" "-")
The rabbit chases the rabbit.
Unknown
rconc
[@1: The rabbit chases the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "chases" "rabbit" "+")
The rabbit does not need the squirrel.
Unknown
inv-random
[@0: The rabbit needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "squirrel" "-")
The squirrel is round.
Unknown
random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The rabbit is green.
Unknown
random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "+")
@0: The rabbit chases the squirrel.[(triple1)] The squirrel chases the rabbit.[(triple2 OR ((triple7) -> rule6))] The squirrel eats the rabbit.[(triple3)] The squirrel is blue.[(triple4)] The squirrel is cold.[(triple5)] The squirrel is not red.[(triple6)] The squirrel needs the rabbit.[(triple7)] @1: The rabbit does not eat the squirrel.[(((triple1) -> rule7))] The squirrel chases the squirrel.[(((triple5) -> rule5))] @2: The squirrel does not eat the squirrel.[(((((triple5) -> rule5)) -> rule7))]
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
triple1
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
triple2
((triple7) -> (rule6 % int1))
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int1
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
triple3
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple4
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple5
The squirrel is not red.
("squirrel" "is" "red" "-")
triple6
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple7
The rabbit does not eat the squirrel.
("rabbit" "eats" "squirrel" "-")
((triple1) -> (rule7 % int1))
The rabbit does not eat the squirrel.
("rabbit" "eats" "squirrel" "-")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
((triple5) -> (rule5 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel does not eat the squirrel.
("squirrel" "eats" "squirrel" "-")
((((triple5) -> (rule5 % int2))) -> (rule7 % int1))
The squirrel does not eat the squirrel.
("squirrel" "eats" "squirrel" "-")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2