The bear chases the squirrel. The bear is blue. The cat chases the bear. The cat eats the bear. The cat eats the squirrel. The cat is big. The cat is blue. The cat sees the squirrel. The squirrel chases the bear. The squirrel eats the bear. The squirrel eats the cat. The squirrel is big. The squirrel is blue. The squirrel is round. The squirrel is young. The squirrel sees the bear. If something sees the bear then it sees the cat. If something is blue and it sees the cat then the cat sees the bear. If the cat chases the bear then the cat is green.
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
The bear is blue.
("bear" "is" "blue" "+")
The cat chases the bear.
("cat" "chases" "bear" "+")
The cat eats the bear.
("cat" "eats" "bear" "+")
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
If something sees the bear then it sees the cat.
((("something" "sees" "bear" "+")) -> ("something" "sees" "cat" "+"))
If something is blue and it sees the cat then the cat sees the bear.
((("something" "is" "blue" "+") ("something" "sees" "cat" "+")) -> ("cat" "sees" "bear" "+"))
If the cat chases the bear then the cat is green.
((("cat" "chases" "bear" "+")) -> ("cat" "is" "green" "+"))
The cat sees the squirrel.
True
1
proof
[(triple8)]
("cat" "sees" "squirrel" "+")
triple8
The bear is not blue.
False
1
inv-proof
[(triple2)]
("bear" "is" "blue" "-")
triple2
The squirrel sees the cat.
True
2
proof
[(((triple16) -> rule1))]
("squirrel" "sees" "cat" "+")
((triple16) -> (rule1 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The squirrel does not see the cat.
False
2
inv-proof
[(((triple16) -> rule1))]
("squirrel" "sees" "cat" "-")
((triple16) -> (rule1 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The cat sees the bear.
True
4
proof
[(((triple13 ((triple16) -> rule1)) -> rule2))]
("cat" "sees" "bear" "+")
((triple13 ((triple16) -> (rule1 % int2))) -> (rule2 % int1))
The cat sees the bear.
("cat" "sees" "bear" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int2
The cat does not see the bear.
False
4
inv-proof
[(((triple13 ((triple16) -> rule1)) -> rule2))]
("cat" "sees" "bear" "-")
((triple13 ((triple16) -> (rule1 % int2))) -> (rule2 % int1))
The cat sees the bear.
("cat" "sees" "bear" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int2
The cat sees the cat.
True
5
proof
[(((((triple13 ((triple16) -> rule1)) -> rule2)) -> rule1))]
("cat" "sees" "cat" "+")
((((triple13 ((triple16) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat sees the bear.
("cat" "sees" "bear" "+")
int2
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int3
The cat does not see the cat.
False
5
inv-proof
[(((((triple13 ((triple16) -> rule1)) -> rule2)) -> rule1))]
("cat" "sees" "cat" "-")
((((triple13 ((triple16) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat sees the bear.
("cat" "sees" "bear" "+")
int2
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int3
The bear does not see the cat.
Unknown
inv-rconc
[@1: The bear sees the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "sees" "cat" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
The bear does not eat the bear.
Unknown
inv-random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "-")
The bear eats the cat.
Unknown
random
[@0: The bear eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "cat" "+")
The bear does not chase the cat.
Unknown
inv-random
[@0: The bear chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "cat" "-")
The bear is big.
Unknown
random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "+")
The bear does not chase the bear.
Unknown
inv-random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
@0: The bear chases the squirrel.[(triple1)] The bear is blue.[(triple2)] The cat chases the bear.[(triple3)] The cat eats the bear.[(triple4)] The cat eats the squirrel.[(triple5)] The cat is big.[(triple6)] The cat is blue.[(triple7)] The cat sees the squirrel.[(triple8)] The squirrel chases the bear.[(triple9)] The squirrel eats the bear.[(triple10)] The squirrel eats the cat.[(triple11)] The squirrel is big.[(triple12)] The squirrel is blue.[(triple13)] The squirrel is round.[(triple14)] The squirrel is young.[(triple15)] The squirrel sees the bear.[(triple16)] @1: The cat is green.[(((triple3) -> rule3))] The squirrel sees the cat.[(((triple16) -> rule1))] @2: The cat sees the bear.[(((triple13 ((triple16) -> rule1)) -> rule2))] @3: The cat sees the cat.[(((((triple13 ((triple16) -> rule1)) -> rule2)) -> rule1))]
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
triple1
The bear is blue.
("bear" "is" "blue" "+")
triple2
The cat chases the bear.
("cat" "chases" "bear" "+")
triple3
The cat eats the bear.
("cat" "eats" "bear" "+")
triple4
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
triple5
The cat is big.
("cat" "is" "big" "+")
triple6
The cat is blue.
("cat" "is" "blue" "+")
triple7
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
triple8
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
triple9
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
triple10
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple11
The squirrel is big.
("squirrel" "is" "big" "+")
triple12
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple13
The squirrel is round.
("squirrel" "is" "round" "+")
triple14
The squirrel is young.
("squirrel" "is" "young" "+")
triple15
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple16
The cat is green.
("cat" "is" "green" "+")
((triple3) -> (rule3 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
((triple16) -> (rule1 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The cat sees the bear.
("cat" "sees" "bear" "+")
((triple13 ((triple16) -> (rule1 % int2))) -> (rule2 % int1))
The cat sees the bear.
("cat" "sees" "bear" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int2
The cat sees the cat.
("cat" "sees" "cat" "+")
((((triple13 ((triple16) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat sees the bear.
("cat" "sees" "bear" "+")
int2
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int3