The bear needs the squirrel. The lion needs the squirrel. The squirrel eats the tiger. The tiger is big. The tiger is round. The tiger needs the bear. The tiger needs the squirrel. If someone needs the squirrel then they chase the squirrel. If someone chases the lion and they are green then they chase the squirrel.
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
If someone needs the squirrel then they chase the squirrel.
((("someone" "needs" "squirrel" "+")) -> ("someone" "chases" "squirrel" "+"))
If someone chases the lion and they are green then they chase the squirrel.
((("someone" "chases" "lion" "+") ("someone" "is" "green" "+")) -> ("someone" "chases" "squirrel" "+"))
The tiger is round.
True
1
proof
[(triple5)]
("tiger" "is" "round" "+")
triple5
The tiger does not need the bear.
False
1
inv-proof
[(triple6)]
("tiger" "needs" "bear" "-")
triple6
The tiger chases the squirrel.
True
2
proof
[(((triple7) -> rule1))]
("tiger" "chases" "squirrel" "+")
((triple7) -> (rule1 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
The bear does not chase the squirrel.
False
2
inv-proof
[(((triple1) -> rule1))]
("bear" "chases" "squirrel" "-")
((triple1) -> (rule1 % int1))
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int1
The squirrel does not chase the squirrel.
Unknown
inv-rconc
[@1: The squirrel chases the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "chases" "squirrel" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
The tiger does not chase the lion.
Unknown
inv-random
[@0: The tiger chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "lion" "-")
The lion is big.
Unknown
random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "+")
@0: The bear needs the squirrel.[(triple1)] The lion needs the squirrel.[(triple2)] The squirrel eats the tiger.[(triple3)] The tiger is big.[(triple4)] The tiger is round.[(triple5)] The tiger needs the bear.[(triple6)] The tiger needs the squirrel.[(triple7)] @1: The bear chases the squirrel.[(((triple1) -> rule1))] The lion chases the squirrel.[(((triple2) -> rule1))] The tiger chases the squirrel.[(((triple7) -> rule1))]
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
triple1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple2
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple3
The tiger is big.
("tiger" "is" "big" "+")
triple4
The tiger is round.
("tiger" "is" "round" "+")
triple5
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple6
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple7
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
((triple1) -> (rule1 % int1))
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
((triple2) -> (rule1 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
((triple7) -> (rule1 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1