The squirrel chases the tiger. The squirrel is red. The squirrel is rough. The squirrel sees the tiger. The tiger is red. The tiger is rough. The tiger visits the squirrel. If someone is rough then they see the tiger. If someone chases the tiger then the tiger chases the squirrel. If someone is blue then they see the tiger. If someone chases the squirrel and they are red then they are big. If someone is big and they chase the tiger then the tiger is blue. If someone sees the squirrel and the squirrel is rough then they chase the tiger. If someone visits the tiger and they are blue then they chase the squirrel. If someone sees the tiger and they visit the squirrel then the tiger chases the squirrel.
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If someone is rough then they see the tiger.
((("someone" "is" "rough" "+")) -> ("someone" "sees" "tiger" "+"))
If someone chases the tiger then the tiger chases the squirrel.
((("someone" "chases" "tiger" "+")) -> ("tiger" "chases" "squirrel" "+"))
If someone is blue then they see the tiger.
((("someone" "is" "blue" "+")) -> ("someone" "sees" "tiger" "+"))
If someone chases the squirrel and they are red then they are big.
((("someone" "chases" "squirrel" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If someone is big and they chase the tiger then the tiger is blue.
((("someone" "is" "big" "+") ("someone" "chases" "tiger" "+")) -> ("tiger" "is" "blue" "+"))
If someone sees the squirrel and the squirrel is rough then they chase the tiger.
((("someone" "sees" "squirrel" "+") ("squirrel" "is" "rough" "+")) -> ("someone" "chases" "tiger" "+"))
If someone visits the tiger and they are blue then they chase the squirrel.
((("someone" "visits" "tiger" "+") ("someone" "is" "blue" "+")) -> ("someone" "chases" "squirrel" "+"))
If someone sees the tiger and they visit the squirrel then the tiger chases the squirrel.
((("someone" "sees" "tiger" "+") ("someone" "visits" "squirrel" "+")) -> ("tiger" "chases" "squirrel" "+"))
The tiger visits the squirrel.
True
1
proof
[(triple7)]
("tiger" "visits" "squirrel" "+")
triple7
The squirrel is not red.
False
1
inv-proof
[(triple2)]
("squirrel" "is" "red" "-")
triple2
The tiger chases the squirrel.
True
2
proof
[(((triple1) -> rule2) OR ((((triple6) -> rule1) triple7) -> rule8))]
("tiger" "chases" "squirrel" "+")
((triple1) -> (rule2 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
((((triple6) -> (rule1 % int2)) triple7) -> (rule8 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger does not see the tiger.
False
2
inv-proof
[(((triple6) -> rule1))]
("tiger" "sees" "tiger" "-")
((triple6) -> (rule1 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is big.
True
4
proof
[(((((triple1) -> rule2) triple5) -> rule4) OR ((((((triple6) -> rule1) triple7) -> rule8) triple5) -> rule4))]
("tiger" "is" "big" "+")
((((triple1) -> (rule2 % int2)) triple5) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int2
((((((triple6) -> (rule1 % int3)) triple7) -> (rule8 % int2)) triple5) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int2
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int3
The tiger is not big.
False
4
inv-proof
[(((((triple1) -> rule2) triple5) -> rule4) OR ((((((triple6) -> rule1) triple7) -> rule8) triple5) -> rule4))]
("tiger" "is" "big" "-")
((((triple1) -> (rule2 % int2)) triple5) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int2
((((((triple6) -> (rule1 % int3)) triple7) -> (rule8 % int2)) triple5) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int2
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int3
The tiger does not chase the tiger.
Unknown
inv-rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "chases" "tiger" "-")
The squirrel chases the squirrel.
Unknown
rconc
[@1: The squirrel chases the squirrel.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "chases" "squirrel" "+")
The tiger is not blue.
Unknown
inv-rconc
[@3: The tiger is blue.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule7 <- FAIL)]]
("tiger" "is" "blue" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
The squirrel does not visit the tiger.
Unknown
inv-random
[@0: The squirrel visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "tiger" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
@0: The squirrel chases the tiger.[(triple1)] The squirrel is red.[(triple2)] The squirrel is rough.[(triple3)] The squirrel sees the tiger.[(triple4 OR ((triple3) -> rule1))] The tiger is red.[(triple5)] The tiger is rough.[(triple6)] The tiger visits the squirrel.[(triple7)] @1: The tiger chases the squirrel.[(((triple1) -> rule2) OR ((((triple6) -> rule1) triple7) -> rule8))] The tiger sees the tiger.[(((triple6) -> rule1))] @2: The tiger is big.[(((((triple1) -> rule2) triple5) -> rule4) OR ((((((triple6) -> rule1) triple7) -> rule8) triple5) -> rule4))]
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple1
The squirrel is red.
("squirrel" "is" "red" "+")
triple2
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple3
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple4
((triple3) -> (rule1 % int1))
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
triple5
The tiger is rough.
("tiger" "is" "rough" "+")
triple6
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple7
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
((triple1) -> (rule2 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
((((triple6) -> (rule1 % int2)) triple7) -> (rule8 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((triple6) -> (rule1 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
((((triple1) -> (rule2 % int2)) triple5) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int2
((((((triple6) -> (rule1 % int3)) triple7) -> (rule8 % int2)) triple5) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int2
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int3