The bear eats the squirrel. The bear is big. The bear is green. The bear sees the squirrel. The lion is kind. The lion sees the mouse. The lion sees the squirrel. The mouse eats the squirrel. The mouse is cold. The squirrel chases the lion. The squirrel is cold. The squirrel sees the bear. If someone sees the bear then they eat the bear. All big, kind people are green.
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
The bear is big.
("bear" "is" "big" "+")
The bear is green.
("bear" "is" "green" "+")
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
If someone sees the bear then they eat the bear.
((("someone" "sees" "bear" "+")) -> ("someone" "eats" "bear" "+"))
All big, kind people are green.
((("someone" "is" "big" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
The squirrel sees the bear.
True
1
proof
[(triple12)]
("squirrel" "sees" "bear" "+")
triple12
The squirrel is not cold.
False
1
inv-proof
[(triple11)]
("squirrel" "is" "cold" "-")
triple11
The squirrel eats the bear.
True
2
proof
[(((triple12) -> rule1))]
("squirrel" "eats" "bear" "+")
((triple12) -> (rule1 % int1))
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int1
The squirrel does not eat the bear.
False
2
inv-proof
[(((triple12) -> rule1))]
("squirrel" "eats" "bear" "-")
((triple12) -> (rule1 % int1))
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int1
The lion does not eat the bear.
Unknown
inv-rconc
[@1: The lion eats the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "eats" "bear" "-")
The mouse is green.
Unknown
rconc
[@1: The mouse is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "green" "+")
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "-")
The lion eats the mouse.
Unknown
random
[@0: The lion eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "mouse" "+")
@0: The bear eats the squirrel.[(triple1)] The bear is big.[(triple2)] The bear is green.[(triple3)] The bear sees the squirrel.[(triple4)] The lion is kind.[(triple5)] The lion sees the mouse.[(triple6)] The lion sees the squirrel.[(triple7)] The mouse eats the squirrel.[(triple8)] The mouse is cold.[(triple9)] The squirrel chases the lion.[(triple10)] The squirrel is cold.[(triple11)] The squirrel sees the bear.[(triple12)] @1: The squirrel eats the bear.[(((triple12) -> rule1))]
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
triple1
The bear is big.
("bear" "is" "big" "+")
triple2
The bear is green.
("bear" "is" "green" "+")
triple3
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple4
The lion is kind.
("lion" "is" "kind" "+")
triple5
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple6
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple7
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple8
The mouse is cold.
("mouse" "is" "cold" "+")
triple9
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
triple10
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple11
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple12
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
((triple12) -> (rule1 % int1))
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int1