The bear is big. The bear is round. The bear likes the tiger. The bear sees the lion. The lion eats the squirrel. The lion is big. The lion likes the squirrel. The lion sees the squirrel. The lion sees the tiger. The squirrel is round. The squirrel likes the bear. The squirrel sees the lion. The tiger eats the lion. The tiger likes the bear. The tiger likes the lion. The tiger sees the bear. If something is round then it is kind.
The bear is big.
("bear" "is" "big" "+")
The bear is round.
("bear" "is" "round" "+")
The bear likes the tiger.
("bear" "likes" "tiger" "+")
The bear sees the lion.
("bear" "sees" "lion" "+")
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The lion is big.
("lion" "is" "big" "+")
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
The tiger likes the bear.
("tiger" "likes" "bear" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
If something is round then it is kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
The squirrel likes the bear.
True
1
proof
[(triple11)]
("squirrel" "likes" "bear" "+")
triple11
The bear is not round.
False
1
inv-proof
[(triple2)]
("bear" "is" "round" "-")
triple2
The squirrel is kind.
True
2
proof
[(((triple10) -> rule1))]
("squirrel" "is" "kind" "+")
((triple10) -> (rule1 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is not kind.
False
2
inv-proof
[(((triple10) -> rule1))]
("squirrel" "is" "kind" "-")
((triple10) -> (rule1 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The tiger is not kind.
Unknown
inv-rconc
[@1: The tiger is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "kind" "-")
The lion is kind.
Unknown
rconc
[@1: The lion is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "kind" "+")
The squirrel does not eat the tiger.
Unknown
inv-random
[@0: The squirrel eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "tiger" "-")
The squirrel eats the bear.
Unknown
random
[@0: The squirrel eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "bear" "+")
@0: The bear is big.[(triple1)] The bear is round.[(triple2)] The bear likes the tiger.[(triple3)] The bear sees the lion.[(triple4)] The lion eats the squirrel.[(triple5)] The lion is big.[(triple6)] The lion likes the squirrel.[(triple7)] The lion sees the squirrel.[(triple8)] The lion sees the tiger.[(triple9)] The squirrel is round.[(triple10)] The squirrel likes the bear.[(triple11)] The squirrel sees the lion.[(triple12)] The tiger eats the lion.[(triple13)] The tiger likes the bear.[(triple14)] The tiger likes the lion.[(triple15)] The tiger sees the bear.[(triple16)] @1: The bear is kind.[(((triple2) -> rule1))] The squirrel is kind.[(((triple10) -> rule1))]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear is round.
("bear" "is" "round" "+")
triple2
The bear likes the tiger.
("bear" "likes" "tiger" "+")
triple3
The bear sees the lion.
("bear" "sees" "lion" "+")
triple4
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple5
The lion is big.
("lion" "is" "big" "+")
triple6
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
triple7
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple8
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple9
The squirrel is round.
("squirrel" "is" "round" "+")
triple10
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
triple11
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple12
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple13
The tiger likes the bear.
("tiger" "likes" "bear" "+")
triple14
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple15
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple16
The bear is kind.
("bear" "is" "kind" "+")
((triple2) -> (rule1 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
((triple10) -> (rule1 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1