The rabbit chases the squirrel. The rabbit eats the squirrel. The rabbit is cold. The rabbit is not green. The rabbit needs the squirrel. The squirrel chases the rabbit. The squirrel does not eat the rabbit. The squirrel is cold. The squirrel is nice. The squirrel is rough. If something is red then it needs the rabbit. If something needs the squirrel then it eats the squirrel. If the rabbit eats the squirrel then the squirrel is red. If something chases the rabbit and it does not need the squirrel then it does not eat the rabbit. If something is cold and it does not eat the squirrel then the squirrel needs the rabbit. If something chases the squirrel and it does not eat the squirrel then it is not cold.
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is not green.
("rabbit" "is" "green" "-")
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
The squirrel does not eat the rabbit.
("squirrel" "eats" "rabbit" "-")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
If something is red then it needs the rabbit.
((("something" "is" "red" "+")) -> ("something" "needs" "rabbit" "+"))
If something needs the squirrel then it eats the squirrel.
((("something" "needs" "squirrel" "+")) -> ("something" "eats" "squirrel" "+"))
If the rabbit eats the squirrel then the squirrel is red.
((("rabbit" "eats" "squirrel" "+")) -> ("squirrel" "is" "red" "+"))
If something chases the rabbit and it does not need the squirrel then it does not eat the rabbit.
((("something" "chases" "rabbit" "+") ("something" "needs" "squirrel" "~")) -> ("something" "eats" "rabbit" "-"))
If something is cold and it does not eat the squirrel then the squirrel needs the rabbit.
((("something" "is" "cold" "+") ("something" "eats" "squirrel" "~")) -> ("squirrel" "needs" "rabbit" "+"))
If something chases the squirrel and it does not eat the squirrel then it is not cold.
((("something" "chases" "squirrel" "+") ("something" "eats" "squirrel" "~")) -> ("something" "is" "cold" "-"))
The squirrel is nice.
True
1
proof
[(triple9)]
("squirrel" "is" "nice" "+")
triple9
The rabbit is green.
False
1
inv-proof
[(triple4)]
("rabbit" "is" "green" "+")
triple4
The squirrel is red.
True
2
proof
[(((triple2) -> rule3) OR ((((triple5) -> rule2)) -> rule3))]
("squirrel" "is" "red" "+")
((triple2) -> (rule3 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int2
The squirrel is not red.
False
2
inv-proof
[(((triple2) -> rule3) OR ((((triple5) -> rule2)) -> rule3))]
("squirrel" "is" "red" "-")
((triple2) -> (rule3 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int2
The squirrel needs the rabbit.
True
3
proof
[(((((triple2) -> rule3)) -> rule1) OR ((((((triple5) -> rule2)) -> rule3)) -> rule1))]
("squirrel" "needs" "rabbit" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
((((((triple5) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int3
The squirrel does not need the rabbit.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule1) OR ((((((triple5) -> rule2)) -> rule3)) -> rule1))]
("squirrel" "needs" "rabbit" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
((((((triple5) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int3
The rabbit does not need the rabbit.
Unknown
inv-rconc
[@1: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "needs" "rabbit" "-")
The squirrel eats the squirrel.
Unknown
rconc
[@1: The squirrel eats the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "eats" "squirrel" "+")
The rabbit does not eat the rabbit.
Unknown
inv-random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
The rabbit does not chase the rabbit.
Unknown
inv-random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "-")
The rabbit is nice.
Unknown
random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "+")
@0: The rabbit chases the squirrel.[(triple1)] The rabbit eats the squirrel.[(triple2 OR ((triple5) -> rule2))] The rabbit is cold.[(triple3)] The rabbit is not green.[(triple4)] The rabbit needs the squirrel.[(triple5)] The squirrel chases the rabbit.[(triple6)] The squirrel does not eat the rabbit.[(triple7)] The squirrel is cold.[(triple8)] The squirrel is nice.[(triple9)] The squirrel is rough.[(triple10)] @1: The squirrel is red.[(((triple2) -> rule3) OR ((((triple5) -> rule2)) -> rule3))] @2: The squirrel needs the rabbit.[(((((triple2) -> rule3)) -> rule1) OR ((((((triple5) -> rule2)) -> rule3)) -> rule1))]
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
triple1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
triple2
((triple5) -> (rule2 % int1))
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple3
The rabbit is not green.
("rabbit" "is" "green" "-")
triple4
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
triple5
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
triple6
The squirrel does not eat the rabbit.
("squirrel" "eats" "rabbit" "-")
triple7
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple8
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple9
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple10
The squirrel is red.
("squirrel" "is" "red" "+")
((triple2) -> (rule3 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int2
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
((((((triple5) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int3