The bear eats the tiger. The bear likes the tiger. The squirrel eats the tiger. The squirrel is blue. The squirrel is green. The squirrel is rough. The squirrel likes the bear. The squirrel needs the tiger. The tiger is blue. The tiger is nice. If something is blue then it likes the tiger. If something is kind then it eats the squirrel. If something needs the bear and the bear eats the tiger then the tiger is blue.
The bear eats the tiger.
("bear" "eats" "tiger" "+")
The bear likes the tiger.
("bear" "likes" "tiger" "+")
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
If something is blue then it likes the tiger.
((("something" "is" "blue" "+")) -> ("something" "likes" "tiger" "+"))
If something is kind then it eats the squirrel.
((("something" "is" "kind" "+")) -> ("something" "eats" "squirrel" "+"))
If something needs the bear and the bear eats the tiger then the tiger is blue.
((("something" "needs" "bear" "+") ("bear" "eats" "tiger" "+")) -> ("tiger" "is" "blue" "+"))
The squirrel is blue.
True
1
proof
[(triple4)]
("squirrel" "is" "blue" "+")
triple4
The squirrel does not eat the tiger.
False
1
inv-proof
[(triple3)]
("squirrel" "eats" "tiger" "-")
triple3
The squirrel likes the tiger.
True
2
proof
[(((triple4) -> rule1))]
("squirrel" "likes" "tiger" "+")
((triple4) -> (rule1 % int1))
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
int1
The tiger does not like the tiger.
False
2
inv-proof
[(((triple9) -> rule1))]
("tiger" "likes" "tiger" "-")
((triple9) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The bear does not eat the squirrel.
Unknown
inv-rconc
[@1: The bear eats the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "eats" "squirrel" "-")
The squirrel eats the squirrel.
Unknown
rconc
[@1: The squirrel eats the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "eats" "squirrel" "+")
The bear does not need the tiger.
Unknown
inv-random
[@0: The bear needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "tiger" "-")
The squirrel is nice.
Unknown
random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "+")
@0: The bear eats the tiger.[(triple1)] The bear likes the tiger.[(triple2)] The squirrel eats the tiger.[(triple3)] The squirrel is blue.[(triple4)] The squirrel is green.[(triple5)] The squirrel is rough.[(triple6)] The squirrel likes the bear.[(triple7)] The squirrel needs the tiger.[(triple8)] The tiger is blue.[(triple9)] The tiger is nice.[(triple10)] @1: The squirrel likes the tiger.[(((triple4) -> rule1))] The tiger likes the tiger.[(((triple9) -> rule1))]
The bear eats the tiger.
("bear" "eats" "tiger" "+")
triple1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
triple2
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple3
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple4
The squirrel is green.
("squirrel" "is" "green" "+")
triple5
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple6
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
triple7
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
triple8
The tiger is blue.
("tiger" "is" "blue" "+")
triple9
The tiger is nice.
("tiger" "is" "nice" "+")
triple10
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
((triple4) -> (rule1 % int1))
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple9) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1