The lion eats the squirrel. The lion is big. The lion is green. The lion is kind. The lion sees the squirrel. The lion visits the squirrel. The squirrel eats the lion. The squirrel is green. The squirrel is kind. The squirrel is rough. The squirrel sees the lion. The squirrel visits the lion. If something eats the squirrel then the squirrel is kind. If something is big and kind then it eats the lion.
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If something eats the squirrel then the squirrel is kind.
((("something" "eats" "squirrel" "+")) -> ("squirrel" "is" "kind" "+"))
If something is big and kind then it eats the lion.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "eats" "lion" "+"))
The lion eats the squirrel.
True
1
proof
[(triple1)]
("lion" "eats" "squirrel" "+")
triple1
The squirrel is not kind.
False
1
inv-proof
[(triple9 OR ((triple1) -> rule1))]
("squirrel" "is" "kind" "-")
triple9
((triple1) -> (rule1 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The lion eats the lion.
True
3
proof
[(((triple2 triple4) -> rule2))]
("lion" "eats" "lion" "+")
((triple2 triple4) -> (rule2 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion does not eat the lion.
False
3
inv-proof
[(((triple2 triple4) -> rule2))]
("lion" "eats" "lion" "-")
((triple2 triple4) -> (rule2 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion is not red.
Unknown
inv-random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "-")
The squirrel is red.
Unknown
random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "+")
The squirrel is not big.
Unknown
inv-random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
@0: The lion eats the squirrel.[(triple1)] The lion is big.[(triple2)] The lion is green.[(triple3)] The lion is kind.[(triple4)] The lion sees the squirrel.[(triple5)] The lion visits the squirrel.[(triple6)] The squirrel eats the lion.[(triple7)] The squirrel is green.[(triple8)] The squirrel is kind.[(triple9 OR ((triple1) -> rule1))] The squirrel is rough.[(triple10)] The squirrel sees the lion.[(triple11)] The squirrel visits the lion.[(triple12)] @1: The lion eats the lion.[(((triple2 triple4) -> rule2))]
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple1
The lion is big.
("lion" "is" "big" "+")
triple2
The lion is green.
("lion" "is" "green" "+")
triple3
The lion is kind.
("lion" "is" "kind" "+")
triple4
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple5
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple6
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
triple7
The squirrel is green.
("squirrel" "is" "green" "+")
triple8
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple9
((triple1) -> (rule1 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple10
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple11
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple12
The lion eats the lion.
("lion" "eats" "lion" "+")
((triple2 triple4) -> (rule2 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1