The cat needs the squirrel. The lion needs the squirrel. The mouse eats the lion. The squirrel needs the mouse. If someone chases the squirrel and the squirrel eats the lion then the squirrel chases the cat. If someone is red then they do not eat the squirrel. If someone eats the lion then the lion is not nice.
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
If someone chases the squirrel and the squirrel eats the lion then the squirrel chases the cat.
((("someone" "chases" "squirrel" "+") ("squirrel" "eats" "lion" "+")) -> ("squirrel" "chases" "cat" "+"))
If someone is red then they do not eat the squirrel.
((("someone" "is" "red" "+")) -> ("someone" "eats" "squirrel" "-"))
If someone eats the lion then the lion is not nice.
((("someone" "eats" "lion" "+")) -> ("lion" "is" "nice" "-"))
The cat needs the squirrel.
True
1
proof
[(triple1)]
("cat" "needs" "squirrel" "+")
triple1
The cat does not need the squirrel.
False
1
inv-proof
[(triple1)]
("cat" "needs" "squirrel" "-")
triple1
The lion is not nice.
True
2
proof
[(((triple3) -> rule3))]
("lion" "is" "nice" "-")
((triple3) -> (rule3 % int1))
The lion is not nice.
("lion" "is" "nice" "-")
int1
The lion is nice.
False
2
inv-proof
[(((triple3) -> rule3))]
("lion" "is" "nice" "+")
((triple3) -> (rule3 % int1))
The lion is not nice.
("lion" "is" "nice" "-")
int1
The squirrel does not chase the cat.
Unknown
inv-rconc
[@1: The squirrel chases the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "chases" "cat" "-")
The lion is red.
Unknown
random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "+")
The squirrel does not eat the cat.
Unknown
inv-random
[@0: The squirrel eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "cat" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
@0: The cat needs the squirrel.[(triple1)] The lion needs the squirrel.[(triple2)] The mouse eats the lion.[(triple3)] The squirrel needs the mouse.[(triple4)] @1: The lion is not nice.[(((triple3) -> rule3))]
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
triple1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple3
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple4
The lion is not nice.
("lion" "is" "nice" "-")
((triple3) -> (rule3 % int1))
The lion is not nice.
("lion" "is" "nice" "-")
int1