The squirrel chases the tiger. The tiger eats the squirrel. If something eats the tiger and the tiger is green then it chases the tiger. If something is big and it does not eat the squirrel then it chases the tiger. If something is green then it is red. All green things are red. If something chases the tiger and it is green then the tiger chases the squirrel. If something eats the squirrel then the squirrel is green.
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
If something eats the tiger and the tiger is green then it chases the tiger.
((("something" "eats" "tiger" "+") ("tiger" "is" "green" "+")) -> ("something" "chases" "tiger" "+"))
If something is big and it does not eat the squirrel then it chases the tiger.
((("something" "is" "big" "+") ("something" "eats" "squirrel" "~")) -> ("something" "chases" "tiger" "+"))
If something is green then it is red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
All green things are red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If something chases the tiger and it is green then the tiger chases the squirrel.
((("something" "chases" "tiger" "+") ("something" "is" "green" "+")) -> ("tiger" "chases" "squirrel" "+"))
If something eats the squirrel then the squirrel is green.
((("something" "eats" "squirrel" "+")) -> ("squirrel" "is" "green" "+"))
The tiger eats the squirrel.
True
1
proof
[(triple2)]
("tiger" "eats" "squirrel" "+")
triple2
The squirrel does not chase the tiger.
False
1
inv-proof
[(triple1)]
("squirrel" "chases" "tiger" "-")
triple1
The squirrel is green.
True
2
proof
[(((triple2) -> rule6))]
("squirrel" "is" "green" "+")
((triple2) -> (rule6 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is not green.
False
2
inv-proof
[(((triple2) -> rule6))]
("squirrel" "is" "green" "-")
((triple2) -> (rule6 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is red.
True
3
proof
[(((((triple2) -> rule6)) -> rule3) OR ((((triple2) -> rule6)) -> rule4))]
("squirrel" "is" "red" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The tiger does not chase the squirrel.
False
4
inv-proof
[(((triple1 ((triple2) -> rule6)) -> rule5))]
("tiger" "chases" "squirrel" "-")
((triple1 ((triple2) -> (rule6 % int2))) -> (rule5 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The tiger does not chase the tiger.
Unknown
inv-rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "chases" "tiger" "-")
The tiger is red.
Unknown
rconc
[@1: The tiger is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "red" "+")
The squirrel is not blue.
Unknown
inv-random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
The squirrel is not rough.
Unknown
inv-random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "-")
The squirrel is big.
Unknown
random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "+")
@0: The squirrel chases the tiger.[(triple1)] The tiger eats the squirrel.[(triple2)] @1: The squirrel is green.[(((triple2) -> rule6))] @2: The squirrel is red.[(((((triple2) -> rule6)) -> rule3) OR ((((triple2) -> rule6)) -> rule4))] The tiger chases the squirrel.[(((triple1 ((triple2) -> rule6)) -> rule5))]
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
triple2
The squirrel is green.
("squirrel" "is" "green" "+")
((triple2) -> (rule6 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
((triple1 ((triple2) -> (rule6 % int2))) -> (rule5 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2