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