The bear eats the tiger. The bear is red. The squirrel is green. The squirrel likes the tiger. The squirrel needs the bear. The tiger eats the bear. The tiger eats the squirrel. The tiger is red. The tiger is young. The tiger likes the bear. The tiger likes the squirrel. The tiger needs the squirrel. If something eats the tiger and it is red then it likes the tiger. If something is cold and it likes the bear then it eats the squirrel. If something likes the tiger then the tiger eats the bear.
The bear eats the tiger.
("bear" "eats" "tiger" "+")
The bear is red.
("bear" "is" "red" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger likes the bear.
("tiger" "likes" "bear" "+")
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
If something eats the tiger and it is red then it likes the tiger.
((("something" "eats" "tiger" "+") ("something" "is" "red" "+")) -> ("something" "likes" "tiger" "+"))
If something is cold and it likes the bear then it eats the squirrel.
((("something" "is" "cold" "+") ("something" "likes" "bear" "+")) -> ("something" "eats" "squirrel" "+"))
If something likes the tiger then the tiger eats the bear.
((("something" "likes" "tiger" "+")) -> ("tiger" "eats" "bear" "+"))
The tiger eats the bear.
True
1
proof
[(triple6 OR ((triple4) -> rule3) OR ((((triple1 triple2) -> rule1)) -> rule3))]
("tiger" "eats" "bear" "+")
triple6
((triple4) -> (rule3 % int1))
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int1
((((triple1 triple2) -> (rule1 % int2))) -> (rule3 % int1))
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int2
The bear is not red.
False
1
inv-proof
[(triple2)]
("bear" "is" "red" "-")
triple2
The tiger does not like the tiger.
Unknown
inv-rconc
[@1: The tiger likes the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "likes" "tiger" "-")
The squirrel is young.
Unknown
random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "+")
@0: The bear eats the tiger.[(triple1)] The bear is red.[(triple2)] The squirrel is green.[(triple3)] The squirrel likes the tiger.[(triple4)] The squirrel needs the bear.[(triple5)] The tiger eats the bear.[(triple6 OR ((triple4) -> rule3) OR ((((triple1 triple2) -> rule1)) -> rule3))] The tiger eats the squirrel.[(triple7)] The tiger is red.[(triple8)] The tiger is young.[(triple9)] The tiger likes the bear.[(triple10)] The tiger likes the squirrel.[(triple11)] The tiger needs the squirrel.[(triple12)] @1: The bear likes the tiger.[(((triple1 triple2) -> rule1))]
The bear eats the tiger.
("bear" "eats" "tiger" "+")
triple1
The bear is red.
("bear" "is" "red" "+")
triple2
The squirrel is green.
("squirrel" "is" "green" "+")
triple3
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
triple4
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
triple5
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple6
((triple4) -> (rule3 % int1))
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int1
((((triple1 triple2) -> (rule1 % int2))) -> (rule3 % int1))
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int2
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
triple7
The tiger is red.
("tiger" "is" "red" "+")
triple8
The tiger is young.
("tiger" "is" "young" "+")
triple9
The tiger likes the bear.
("tiger" "likes" "bear" "+")
triple10
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
triple11
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple12
The bear likes the tiger.
("bear" "likes" "tiger" "+")
((triple1 triple2) -> (rule1 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1