The cat does not chase the squirrel. The cat eats the squirrel. The cat needs the tiger. The squirrel chases the tiger. The squirrel eats the cat. The squirrel is green. The squirrel is not nice. The squirrel is red. The squirrel does not need the cat. The squirrel needs the tiger. The tiger does not chase the cat. The tiger eats the squirrel. The tiger is green. The tiger is nice. The tiger needs the cat. The tiger does not need the squirrel. If something chases the squirrel then it chases the cat. If the squirrel eats the tiger and the squirrel is not big then the tiger needs the squirrel. If something eats the squirrel and it is nice then it is red. If something is green then it eats the squirrel. Nice things are rough. If something eats the cat and it needs the tiger then it chases the squirrel.
The cat does not chase the squirrel.
("cat" "chases" "squirrel" "-")
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is not nice.
("squirrel" "is" "nice" "-")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel does not need the cat.
("squirrel" "needs" "cat" "-")
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
The tiger does not chase the cat.
("tiger" "chases" "cat" "-")
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger does not need the squirrel.
("tiger" "needs" "squirrel" "-")
If something chases the squirrel then it chases the cat.
((("something" "chases" "squirrel" "+")) -> ("something" "chases" "cat" "+"))
If the squirrel eats the tiger and the squirrel is not big then the tiger needs the squirrel.
((("squirrel" "eats" "tiger" "+") ("squirrel" "is" "big" "~")) -> ("tiger" "needs" "squirrel" "+"))
If something eats the squirrel and it is nice then it is red.
((("something" "eats" "squirrel" "+") ("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If something is green then it eats the squirrel.
((("something" "is" "green" "+")) -> ("something" "eats" "squirrel" "+"))
Nice things are rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If something eats the cat and it needs the tiger then it chases the squirrel.
((("something" "eats" "cat" "+") ("something" "needs" "tiger" "+")) -> ("something" "chases" "squirrel" "+"))
The squirrel is green.
True
1
proof
[(triple6)]
("squirrel" "is" "green" "+")
triple6
The squirrel needs the cat.
False
1
inv-proof
[(triple9)]
("squirrel" "needs" "cat" "+")
triple9
The tiger is rough.
True
2
proof
[(((triple14) -> rule5))]
("tiger" "is" "rough" "+")
((triple14) -> (rule5 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The squirrel does not chase the squirrel.
False
3
inv-proof
[(((triple5 triple10) -> rule6))]
("squirrel" "chases" "squirrel" "-")
((triple5 triple10) -> (rule6 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel chases the cat.
True
4
proof
[(((((triple5 triple10) -> rule6)) -> rule1))]
("squirrel" "chases" "cat" "+")
((((triple5 triple10) -> (rule6 % int2))) -> (rule1 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The squirrel does not chase the cat.
False
4
inv-proof
[(((((triple5 triple10) -> rule6)) -> rule1))]
("squirrel" "chases" "cat" "-")
((((triple5 triple10) -> (rule6 % int2))) -> (rule1 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The cat is not rough.
Unknown
inv-rconc
[@1: The cat is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "is" "rough" "-")
The cat chases the cat.
Unknown
rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "chases" "cat" "+")
The squirrel is not rough.
Unknown
inv-rconc
[@1: The squirrel is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "is" "rough" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
The squirrel is not big.
Unknown
inv-random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "-")
The cat eats the tiger.
Unknown
random
[@0: The cat eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "tiger" "+")
@0: The cat does not chase the squirrel.[(triple1)] The cat eats the squirrel.[(triple2)] The cat needs the tiger.[(triple3)] The squirrel chases the tiger.[(triple4)] The squirrel does not need the cat.[(triple9)] The squirrel eats the cat.[(triple5)] The squirrel is green.[(triple6)] The squirrel is not nice.[(triple7)] The squirrel is red.[(triple8)] The squirrel needs the tiger.[(triple10)] The tiger does not chase the cat.[(triple11)] The tiger does not need the squirrel.[(triple16)] The tiger eats the squirrel.[(triple12 OR ((triple13) -> rule4))] The tiger is green.[(triple13)] The tiger is nice.[(triple14)] The tiger needs the cat.[(triple15)] @1: The squirrel chases the squirrel.[(((triple5 triple10) -> rule6))] The squirrel eats the squirrel.[(((triple6) -> rule4))] The tiger is red.[(((triple12 triple14) -> rule3) OR ((((triple13) -> rule4) triple14) -> rule3))] The tiger is rough.[(((triple14) -> rule5))] @2: The squirrel chases the cat.[(((((triple5 triple10) -> rule6)) -> rule1))]
The cat does not chase the squirrel.
("cat" "chases" "squirrel" "-")
triple1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
triple2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple3
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple4
The squirrel does not need the cat.
("squirrel" "needs" "cat" "-")
triple9
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple5
The squirrel is green.
("squirrel" "is" "green" "+")
triple6
The squirrel is not nice.
("squirrel" "is" "nice" "-")
triple7
The squirrel is red.
("squirrel" "is" "red" "+")
triple8
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
triple10
The tiger does not chase the cat.
("tiger" "chases" "cat" "-")
triple11
The tiger does not need the squirrel.
("tiger" "needs" "squirrel" "-")
triple16
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
triple12
((triple13) -> (rule4 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
triple13
The tiger is nice.
("tiger" "is" "nice" "+")
triple14
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple15
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
((triple5 triple10) -> (rule6 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
((triple6) -> (rule4 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
((triple12 triple14) -> (rule3 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
((((triple13) -> (rule4 % int2)) triple14) -> (rule3 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int2
The tiger is rough.
("tiger" "is" "rough" "+")
((triple14) -> (rule5 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
((((triple5 triple10) -> (rule6 % int2))) -> (rule1 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2