The lion chases the rabbit. The lion is red. The mouse chases the lion. The mouse is red. The mouse sees the lion. The rabbit sees the lion. The squirrel is big. The squirrel is nice. The squirrel sees the lion. The squirrel sees the rabbit. If something chases the lion and it is red then it chases the squirrel. If something sees the squirrel then it is blue.
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion is red.
("lion" "is" "red" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
If something chases the lion and it is red then it chases the squirrel.
((("something" "chases" "lion" "+") ("something" "is" "red" "+")) -> ("something" "chases" "squirrel" "+"))
If something sees the squirrel then it is blue.
((("something" "sees" "squirrel" "+")) -> ("something" "is" "blue" "+"))
The mouse is red.
True
1
proof
[(triple4)]
("mouse" "is" "red" "+")
triple4
The squirrel is not big.
False
1
inv-proof
[(triple7)]
("squirrel" "is" "big" "-")
triple7
The mouse chases the squirrel.
True
3
proof
[(((triple3 triple4) -> rule1))]
("mouse" "chases" "squirrel" "+")
((triple3 triple4) -> (rule1 % int1))
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int1
The mouse does not chase the squirrel.
False
3
inv-proof
[(((triple3 triple4) -> rule1))]
("mouse" "chases" "squirrel" "-")
((triple3 triple4) -> (rule1 % int1))
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int1
The squirrel is not blue.
Unknown
inv-rconc
[@1: The squirrel is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "is" "blue" "-")
The squirrel chases the squirrel.
Unknown
rconc
[@1: The squirrel chases the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "chases" "squirrel" "+")
The squirrel does not see the mouse.
Unknown
inv-random
[@0: The squirrel sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "mouse" "-")
The squirrel chases the lion.
Unknown
random
[@0: The squirrel chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "lion" "+")
@0: The lion chases the rabbit.[(triple1)] The lion is red.[(triple2)] The mouse chases the lion.[(triple3)] The mouse is red.[(triple4)] The mouse sees the lion.[(triple5)] The rabbit sees the lion.[(triple6)] The squirrel is big.[(triple7)] The squirrel is nice.[(triple8)] The squirrel sees the lion.[(triple9)] The squirrel sees the rabbit.[(triple10)] @1: The mouse chases the squirrel.[(((triple3 triple4) -> rule1))]
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple1
The lion is red.
("lion" "is" "red" "+")
triple2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple3
The mouse is red.
("mouse" "is" "red" "+")
triple4
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple5
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple6
The squirrel is big.
("squirrel" "is" "big" "+")
triple7
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple8
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple9
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple10
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
((triple3 triple4) -> (rule1 % int1))
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int1