The squirrel chases the tiger. The squirrel is cold. The squirrel is green. The squirrel needs the tiger. The squirrel visits the tiger. The tiger chases the squirrel. The tiger is cold. The tiger is green. The tiger is red. The tiger is young. The tiger needs the squirrel. The tiger visits the squirrel. If someone chases the tiger and the tiger is red then they visit the squirrel. If someone is blue then they need the tiger. Blue, cold people are red. If someone is cold then they chase the tiger. If someone visits the tiger and the tiger is cold then the tiger needs the squirrel. If someone is cold and they chase the tiger then they need the tiger.
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If someone chases the tiger and the tiger is red then they visit the squirrel.
((("someone" "chases" "tiger" "+") ("tiger" "is" "red" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone is blue then they need the tiger.
((("someone" "is" "blue" "+")) -> ("someone" "needs" "tiger" "+"))
Blue, cold people are red.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If someone is cold then they chase the tiger.
((("someone" "is" "cold" "+")) -> ("someone" "chases" "tiger" "+"))
If someone visits the tiger and the tiger is cold then the tiger needs the squirrel.
((("someone" "visits" "tiger" "+") ("tiger" "is" "cold" "+")) -> ("tiger" "needs" "squirrel" "+"))
If someone is cold and they chase the tiger then they need the tiger.
((("someone" "is" "cold" "+") ("someone" "chases" "tiger" "+")) -> ("someone" "needs" "tiger" "+"))
The squirrel needs the tiger.
True
1
proof
[(triple4 OR ((triple2 triple1) -> rule6) OR ((triple2 ((triple2) -> rule4)) -> rule6))]
("squirrel" "needs" "tiger" "+")
triple4
((triple2 triple1) -> (rule6 % int1))
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int1
((triple2 ((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int1
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int2
The squirrel does not need the tiger.
False
1
inv-proof
[(triple4 OR ((triple2 triple1) -> rule6) OR ((triple2 ((triple2) -> rule4)) -> rule6))]
("squirrel" "needs" "tiger" "-")
triple4
((triple2 triple1) -> (rule6 % int1))
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int1
((triple2 ((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int1
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int2
The tiger chases the tiger.
True
2
proof
[(((triple7) -> rule4))]
("tiger" "chases" "tiger" "+")
((triple7) -> (rule4 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger does not chase the tiger.
False
2
inv-proof
[(((triple7) -> rule4))]
("tiger" "chases" "tiger" "-")
((triple7) -> (rule4 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The squirrel is not red.
Unknown
inv-rconc
[@1: The squirrel is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "red" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The squirrel is young.
Unknown
random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "+")
@0: The squirrel chases the tiger.[(triple1 OR ((triple2) -> rule4))] The squirrel is cold.[(triple2)] The squirrel is green.[(triple3)] The squirrel needs the tiger.[(triple4 OR ((triple2 triple1) -> rule6) OR ((triple2 ((triple2) -> rule4)) -> rule6))] The squirrel visits the tiger.[(triple5)] The tiger chases the squirrel.[(triple6)] The tiger is cold.[(triple7)] The tiger is green.[(triple8)] The tiger is red.[(triple9)] The tiger is young.[(triple10)] The tiger needs the squirrel.[(triple11 OR ((triple5 triple7) -> rule5))] The tiger visits the squirrel.[(triple12 OR ((((triple7) -> rule4) triple9) -> rule1))] @1: The squirrel visits the squirrel.[(((triple1 triple9) -> rule1) OR ((((triple2) -> rule4) triple9) -> rule1))] The tiger chases the tiger.[(((triple7) -> rule4))] @2: The tiger needs the tiger.[(((triple7 ((triple7) -> rule4)) -> rule6))]
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple1
((triple2) -> (rule4 % int1))
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple2
The squirrel is green.
("squirrel" "is" "green" "+")
triple3
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
triple4
((triple2 triple1) -> (rule6 % int1))
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int1
((triple2 ((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int1
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int2
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple5
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple6
The tiger is cold.
("tiger" "is" "cold" "+")
triple7
The tiger is green.
("tiger" "is" "green" "+")
triple8
The tiger is red.
("tiger" "is" "red" "+")
triple9
The tiger is young.
("tiger" "is" "young" "+")
triple10
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple11
((triple5 triple7) -> (rule5 % int1))
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple12
((((triple7) -> (rule4 % int2)) triple9) -> (rule1 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((triple1 triple9) -> (rule1 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
((((triple2) -> (rule4 % int2)) triple9) -> (rule1 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int2
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((triple7) -> (rule4 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((triple7 ((triple7) -> (rule4 % int2))) -> (rule6 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2