The rabbit eats the squirrel. The rabbit is cold. The rabbit is not green. The rabbit is kind. The rabbit is nice. The rabbit likes the squirrel. The rabbit needs the squirrel. The squirrel eats the rabbit. The squirrel is cold. The squirrel is green. The squirrel is kind. The squirrel is nice. The squirrel is round. The squirrel likes the rabbit. The squirrel does not need the rabbit. If something is nice then it eats the squirrel. If something is cold then it eats the squirrel. If something is nice then it does not need the rabbit. If the squirrel does not like the rabbit then the rabbit needs the squirrel. If something is kind and it eats the squirrel then it is nice. If something is cold and it does not eat the squirrel then it does not like the 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 is kind.
("rabbit" "is" "kind" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
The squirrel does not need the rabbit.
("squirrel" "needs" "rabbit" "-")
If something is nice then it eats the squirrel.
((("something" "is" "nice" "+")) -> ("something" "eats" "squirrel" "+"))
If something is cold then it eats the squirrel.
((("something" "is" "cold" "+")) -> ("something" "eats" "squirrel" "+"))
If something is nice then it does not need the rabbit.
((("something" "is" "nice" "+")) -> ("something" "needs" "rabbit" "-"))
If the squirrel does not like the rabbit then the rabbit needs the squirrel.
((("squirrel" "likes" "rabbit" "~")) -> ("rabbit" "needs" "squirrel" "+"))
If something is kind and it eats the squirrel then it is nice.
((("something" "is" "kind" "+") ("something" "eats" "squirrel" "+")) -> ("something" "is" "nice" "+"))
If something is cold and it does not eat the squirrel then it does not like the squirrel.
((("something" "is" "cold" "+") ("something" "eats" "squirrel" "~")) -> ("something" "likes" "squirrel" "-"))
The squirrel likes the rabbit.
True
1
proof
[(triple14)]
("squirrel" "likes" "rabbit" "+")
triple14
The squirrel is not nice.
False
1
inv-proof
[(triple12 OR ((triple11 ((triple9) -> rule2)) -> rule5))]
("squirrel" "is" "nice" "-")
triple12
((triple11 ((triple9) -> (rule2 % int2))) -> (rule5 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The squirrel eats the squirrel.
True
2
proof
[(((triple12) -> rule1) OR ((triple9) -> rule2))]
("squirrel" "eats" "squirrel" "+")
((triple12) -> (rule1 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
((triple9) -> (rule2 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The rabbit needs the rabbit.
False
2
inv-proof
[(((triple5) -> rule3) OR ((((triple4 triple1) -> rule5)) -> rule3) OR ((((triple4 ((triple2) -> rule2)) -> rule5)) -> rule3))]
("rabbit" "needs" "rabbit" "+")
((triple5) -> (rule3 % int1))
The rabbit does not need the rabbit.
("rabbit" "needs" "rabbit" "-")
int1
((((triple4 triple1) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit does not need the rabbit.
("rabbit" "needs" "rabbit" "-")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
((((triple4 ((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit does not need the rabbit.
("rabbit" "needs" "rabbit" "-")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int3
The squirrel does not need the squirrel.
Unknown
inv-random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "-")
The rabbit eats the rabbit.
Unknown
random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "+")
The rabbit does not like the rabbit.
Unknown
inv-random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
@0: The rabbit eats the squirrel.[(triple1 OR ((triple2) -> rule2) OR ((triple5) -> rule1))] The rabbit is cold.[(triple2)] The rabbit is kind.[(triple4)] The rabbit is nice.[(triple5 OR ((triple4 triple1) -> rule5) OR ((triple4 ((triple2) -> rule2)) -> rule5))] The rabbit is not green.[(triple3)] The rabbit likes the squirrel.[(triple6)] The rabbit needs the squirrel.[(triple7)] The squirrel does not need the rabbit.[(triple15 OR ((triple12) -> rule3) OR ((((triple11 ((triple9) -> rule2)) -> rule5)) -> rule3))] The squirrel eats the rabbit.[(triple8)] The squirrel is cold.[(triple9)] The squirrel is green.[(triple10)] The squirrel is kind.[(triple11)] The squirrel is nice.[(triple12 OR ((triple11 ((triple9) -> rule2)) -> rule5))] The squirrel is round.[(triple13)] The squirrel likes the rabbit.[(triple14)] @1: The rabbit does not need the rabbit.[(((triple5) -> rule3) OR ((((triple4 triple1) -> rule5)) -> rule3) OR ((((triple4 ((triple2) -> rule2)) -> rule5)) -> rule3))] The squirrel eats the squirrel.[(((triple12) -> rule1) OR ((triple9) -> rule2))]
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
triple1
((triple2) -> (rule2 % int1))
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int1
((triple5) -> (rule1 % int1))
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple2
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple4
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple5
((triple4 triple1) -> (rule5 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
((triple4 ((triple2) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int2
The rabbit is not green.
("rabbit" "is" "green" "-")
triple3
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
triple6
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
triple7
The squirrel does not need the rabbit.
("squirrel" "needs" "rabbit" "-")
triple15
((triple12) -> (rule3 % int1))
The squirrel does not need the rabbit.
("squirrel" "needs" "rabbit" "-")
int1
((((triple11 ((triple9) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel does not need the rabbit.
("squirrel" "needs" "rabbit" "-")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int3
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
triple8
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple9
The squirrel is green.
("squirrel" "is" "green" "+")
triple10
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple11
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple12
((triple11 ((triple9) -> (rule2 % int2))) -> (rule5 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
triple13
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
triple14
The rabbit does not need the rabbit.
("rabbit" "needs" "rabbit" "-")
((triple5) -> (rule3 % int1))
The rabbit does not need the rabbit.
("rabbit" "needs" "rabbit" "-")
int1
((((triple4 triple1) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit does not need the rabbit.
("rabbit" "needs" "rabbit" "-")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
((((triple4 ((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit does not need the rabbit.
("rabbit" "needs" "rabbit" "-")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int3
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
((triple12) -> (rule1 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
((triple9) -> (rule2 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1