The bear eats the cat. The bear is nice. The cat is red. The cat sees the squirrel. The cat sees the tiger. The squirrel eats the tiger. The squirrel is young. The tiger eats the squirrel. The tiger sees the bear. The tiger sees the squirrel. If the squirrel eats the tiger then the squirrel does not see the tiger. If something sees the tiger and it is kind then it does not like the tiger.
The bear eats the cat.
("bear" "eats" "cat" "+")
The bear is nice.
("bear" "is" "nice" "+")
The cat is red.
("cat" "is" "red" "+")
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
If the squirrel eats the tiger then the squirrel does not see the tiger.
((("squirrel" "eats" "tiger" "+")) -> ("squirrel" "sees" "tiger" "-"))
If something sees the tiger and it is kind then it does not like the tiger.
((("something" "sees" "tiger" "+") ("something" "is" "kind" "+")) -> ("something" "likes" "tiger" "-"))
The cat is red.
True
1
proof
[(triple3)]
("cat" "is" "red" "+")
triple3
The tiger does not see the squirrel.
False
1
inv-proof
[(triple10)]
("tiger" "sees" "squirrel" "-")
triple10
The squirrel does not see the tiger.
True
2
proof
[(((triple6) -> rule1))]
("squirrel" "sees" "tiger" "-")
((triple6) -> (rule1 % int1))
The squirrel does not see the tiger.
("squirrel" "sees" "tiger" "-")
int1
The squirrel sees the tiger.
False
2
inv-proof
[(((triple6) -> rule1))]
("squirrel" "sees" "tiger" "+")
((triple6) -> (rule1 % int1))
The squirrel does not see the tiger.
("squirrel" "sees" "tiger" "-")
int1
The squirrel is not red.
Unknown
inv-random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
The bear does not like the squirrel.
Unknown
inv-random
[@0: The bear likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "squirrel" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
@0: The bear eats the cat.[(triple1)] The bear is nice.[(triple2)] The cat is red.[(triple3)] The cat sees the squirrel.[(triple4)] The cat sees the tiger.[(triple5)] The squirrel eats the tiger.[(triple6)] The squirrel is young.[(triple7)] The tiger eats the squirrel.[(triple8)] The tiger sees the bear.[(triple9)] The tiger sees the squirrel.[(triple10)] @1: The squirrel does not see the tiger.[(((triple6) -> rule1))]
The bear eats the cat.
("bear" "eats" "cat" "+")
triple1
The bear is nice.
("bear" "is" "nice" "+")
triple2
The cat is red.
("cat" "is" "red" "+")
triple3
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
triple4
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple5
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple6
The squirrel is young.
("squirrel" "is" "young" "+")
triple7
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
triple8
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple9
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple10
The squirrel does not see the tiger.
("squirrel" "sees" "tiger" "-")
((triple6) -> (rule1 % int1))
The squirrel does not see the tiger.
("squirrel" "sees" "tiger" "-")
int1