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