The dog is kind. The dog does not see the tiger. The rabbit eats the tiger. The rabbit is not nice. The rabbit is round. The squirrel eats the rabbit. The squirrel eats the tiger. The squirrel is big. The squirrel does not see the rabbit. The tiger does not eat the squirrel. The tiger is kind. The tiger is not nice. If someone eats the rabbit then the rabbit does not need the squirrel.
The dog is kind.
("dog" "is" "kind" "+")
The dog does not see the tiger.
("dog" "sees" "tiger" "-")
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit is not nice.
("rabbit" "is" "nice" "-")
The rabbit is round.
("rabbit" "is" "round" "+")
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel does not see the rabbit.
("squirrel" "sees" "rabbit" "-")
The tiger does not eat the squirrel.
("tiger" "eats" "squirrel" "-")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is not nice.
("tiger" "is" "nice" "-")
If someone eats the rabbit then the rabbit does not need the squirrel.
((("someone" "eats" "rabbit" "+")) -> ("rabbit" "needs" "squirrel" "-"))
The tiger is not nice.
True
1
proof
[(triple12)]
("tiger" "is" "nice" "-")
triple12
The rabbit is not round.
False
1
inv-proof
[(triple5)]
("rabbit" "is" "round" "-")
triple5
The rabbit does not need the squirrel.
True
2
proof
[(((triple6) -> rule1))]
("rabbit" "needs" "squirrel" "-")
((triple6) -> (rule1 % int1))
The rabbit does not need the squirrel.
("rabbit" "needs" "squirrel" "-")
int1
The rabbit needs the squirrel.
False
2
inv-proof
[(((triple6) -> rule1))]
("rabbit" "needs" "squirrel" "+")
((triple6) -> (rule1 % int1))
The rabbit does not need the squirrel.
("rabbit" "needs" "squirrel" "-")
int1
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 tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The squirrel is round.
Unknown
random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "+")
@0: The dog does not see the tiger.[(triple2)] The dog is kind.[(triple1)] The rabbit eats the tiger.[(triple3)] The rabbit is not nice.[(triple4)] The rabbit is round.[(triple5)] The squirrel does not see the rabbit.[(triple9)] The squirrel eats the rabbit.[(triple6)] The squirrel eats the tiger.[(triple7)] The squirrel is big.[(triple8)] The tiger does not eat the squirrel.[(triple10)] The tiger is kind.[(triple11)] The tiger is not nice.[(triple12)] @1: The rabbit does not need the squirrel.[(((triple6) -> rule1))]
The dog does not see the tiger.
("dog" "sees" "tiger" "-")
triple2
The dog is kind.
("dog" "is" "kind" "+")
triple1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple3
The rabbit is not nice.
("rabbit" "is" "nice" "-")
triple4
The rabbit is round.
("rabbit" "is" "round" "+")
triple5
The squirrel does not see the rabbit.
("squirrel" "sees" "rabbit" "-")
triple9
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
triple6
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple7
The squirrel is big.
("squirrel" "is" "big" "+")
triple8
The tiger does not eat the squirrel.
("tiger" "eats" "squirrel" "-")
triple10
The tiger is kind.
("tiger" "is" "kind" "+")
triple11
The tiger is not nice.
("tiger" "is" "nice" "-")
triple12
The rabbit does not need the squirrel.
("rabbit" "needs" "squirrel" "-")
((triple6) -> (rule1 % int1))
The rabbit does not need the squirrel.
("rabbit" "needs" "squirrel" "-")
int1