The bear chases the tiger. The bear eats the tiger. The bear is blue. The bear is green. The bear needs the tiger. The tiger chases the bear. The tiger eats the bear. The tiger is cold. The tiger is green. The tiger needs the bear. If someone is cold then they need the tiger. If someone needs the tiger then they eat the bear. If someone is blue and they chase the bear then they eat the bear. If someone chases the tiger then the tiger eats the bear. If the tiger is kind then the tiger chases the bear. If someone chases the tiger and they eat the bear then they are blue.
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The bear eats the tiger.
("bear" "eats" "tiger" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear is green.
("bear" "is" "green" "+")
The bear needs the tiger.
("bear" "needs" "tiger" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
If someone is cold then they need the tiger.
((("someone" "is" "cold" "+")) -> ("someone" "needs" "tiger" "+"))
If someone needs the tiger then they eat the bear.
((("someone" "needs" "tiger" "+")) -> ("someone" "eats" "bear" "+"))
If someone is blue and they chase the bear then they eat the bear.
((("someone" "is" "blue" "+") ("someone" "chases" "bear" "+")) -> ("someone" "eats" "bear" "+"))
If someone chases the tiger then the tiger eats the bear.
((("someone" "chases" "tiger" "+")) -> ("tiger" "eats" "bear" "+"))
If the tiger is kind then the tiger chases the bear.
((("tiger" "is" "kind" "+")) -> ("tiger" "chases" "bear" "+"))
If someone chases the tiger and they eat the bear then they are blue.
((("someone" "chases" "tiger" "+") ("someone" "eats" "bear" "+")) -> ("someone" "is" "blue" "+"))
The bear eats the tiger.
True
1
proof
[(triple2)]
("bear" "eats" "tiger" "+")
triple2
The tiger is not cold.
False
1
inv-proof
[(triple8)]
("tiger" "is" "cold" "-")
triple8
The tiger is not blue.
Unknown
inv-rconc
[@1: The tiger is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "is" "blue" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
@0: The bear chases the tiger.[(triple1)] The bear eats the tiger.[(triple2)] The bear is blue.[(triple3 OR ((triple1 ((triple5) -> rule2)) -> rule6))] The bear is green.[(triple4)] The bear needs the tiger.[(triple5)] The tiger chases the bear.[(triple6)] The tiger eats the bear.[(triple7 OR ((triple1) -> rule4) OR ((((triple8) -> rule1)) -> rule2))] The tiger is cold.[(triple8)] The tiger is green.[(triple9)] The tiger needs the bear.[(triple10)] @1: The bear eats the bear.[(((triple5) -> rule2))] The tiger needs the tiger.[(((triple8) -> rule1))]
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
triple2
The bear is blue.
("bear" "is" "blue" "+")
triple3
((triple1 ((triple5) -> (rule2 % int2))) -> (rule6 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear eats the bear.
("bear" "eats" "bear" "+")
int2
The bear is green.
("bear" "is" "green" "+")
triple4
The bear needs the tiger.
("bear" "needs" "tiger" "+")
triple5
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple6
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple7
((triple1) -> (rule4 % int1))
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int1
((((triple8) -> (rule1 % int2))) -> (rule2 % int1))
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
triple8
The tiger is green.
("tiger" "is" "green" "+")
triple9
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple10
The bear eats the bear.
("bear" "eats" "bear" "+")
((triple5) -> (rule2 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((triple8) -> (rule1 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1