The bear chases the tiger. The bear is not nice. The bear needs the tiger. The bear visits the tiger. The tiger does not chase the bear. The tiger is not cold. The tiger is nice. The tiger is round. The tiger needs the bear. The tiger visits the bear. If something is round and it needs the tiger then it chases the bear. If something needs the tiger then the tiger is green.
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The bear is not nice.
("bear" "is" "nice" "-")
The bear needs the tiger.
("bear" "needs" "tiger" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The tiger does not chase the bear.
("tiger" "chases" "bear" "-")
The tiger is not cold.
("tiger" "is" "cold" "-")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
If something is round and it needs the tiger then it chases the bear.
((("something" "is" "round" "+") ("something" "needs" "tiger" "+")) -> ("something" "chases" "bear" "+"))
If something needs the tiger then the tiger is green.
((("something" "needs" "tiger" "+")) -> ("tiger" "is" "green" "+"))
The tiger needs the bear.
True
1
proof
[(triple9)]
("tiger" "needs" "bear" "+")
triple9
The tiger is cold.
False
1
inv-proof
[(triple6)]
("tiger" "is" "cold" "+")
triple6
The bear does not chase the bear.
Unknown
inv-rconc
[@1: The bear chases the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "chases" "bear" "-")
The bear is green.
Unknown
random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "+")
@0: The bear chases the tiger.[(triple1)] The bear is not nice.[(triple2)] The bear needs the tiger.[(triple3)] The bear visits the tiger.[(triple4)] The tiger does not chase the bear.[(triple5)] The tiger is nice.[(triple7)] The tiger is not cold.[(triple6)] The tiger is round.[(triple8)] The tiger needs the bear.[(triple9)] The tiger visits the bear.[(triple10)] @1: The tiger is green.[(((triple3) -> rule2))]
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple1
The bear is not nice.
("bear" "is" "nice" "-")
triple2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
triple3
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple4
The tiger does not chase the bear.
("tiger" "chases" "bear" "-")
triple5
The tiger is nice.
("tiger" "is" "nice" "+")
triple7
The tiger is not cold.
("tiger" "is" "cold" "-")
triple6
The tiger is round.
("tiger" "is" "round" "+")
triple8
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple9
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple10
The tiger is green.
("tiger" "is" "green" "+")
((triple3) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1