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