The cat sees the mouse. The lion sees the mouse. The mouse chases the lion. The squirrel is not cold. If the lion is cold and the lion is red then the lion eats the mouse. If someone is young and round then they chase the cat. If someone eats the mouse and the mouse chases the cat then the mouse is round. If someone eats the squirrel and the squirrel is not cold then they are round. If the cat is not round and the cat is not kind then the cat chases the lion. If someone chases the squirrel then the squirrel sees the cat. If someone chases the lion then they see the lion. If someone chases the lion then the lion chases the squirrel.
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The squirrel is not cold.
("squirrel" "is" "cold" "-")
If the lion is cold and the lion is red then the lion eats the mouse.
((("lion" "is" "cold" "+") ("lion" "is" "red" "+")) -> ("lion" "eats" "mouse" "+"))
If someone is young and round then they chase the cat.
((("someone" "is" "young" "+") ("someone" "is" "round" "+")) -> ("someone" "chases" "cat" "+"))
If someone eats the mouse and the mouse chases the cat then the mouse is round.
((("someone" "eats" "mouse" "+") ("mouse" "chases" "cat" "+")) -> ("mouse" "is" "round" "+"))
If someone eats the squirrel and the squirrel is not cold then they are round.
((("someone" "eats" "squirrel" "+") ("squirrel" "is" "cold" "~")) -> ("someone" "is" "round" "+"))
If the cat is not round and the cat is not kind then the cat chases the lion.
((("cat" "is" "round" "~") ("cat" "is" "kind" "~")) -> ("cat" "chases" "lion" "+"))
If someone chases the squirrel then the squirrel sees the cat.
((("someone" "chases" "squirrel" "+")) -> ("squirrel" "sees" "cat" "+"))
If someone chases the lion then they see the lion.
((("someone" "chases" "lion" "+")) -> ("someone" "sees" "lion" "+"))
If someone chases the lion then the lion chases the squirrel.
((("someone" "chases" "lion" "+")) -> ("lion" "chases" "squirrel" "+"))
The mouse chases the lion.
True
1
proof
[(triple3)]
("mouse" "chases" "lion" "+")
triple3
The squirrel is cold.
False
1
inv-proof
[(triple4)]
("squirrel" "is" "cold" "+")
triple4
The mouse sees the lion.
True
2
proof
[(((triple3) -> rule7))]
("mouse" "sees" "lion" "+")
((triple3) -> (rule7 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The mouse does not see the lion.
False
2
inv-proof
[(((triple3) -> rule7))]
("mouse" "sees" "lion" "-")
((triple3) -> (rule7 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The squirrel does not see the lion.
Unknown
inv-rconc
[@1: The squirrel sees the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "sees" "lion" "-")
The squirrel is round.
Unknown
rconc
[@1: The squirrel is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "is" "round" "+")
The cat is not young.
Unknown
inv-random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
@0: The cat sees the mouse.[(triple1)] The lion sees the mouse.[(triple2)] The mouse chases the lion.[(triple3)] The squirrel is not cold.[(triple4)] @1: The lion chases the squirrel.[(((triple3) -> rule8))] The mouse sees the lion.[(((triple3) -> rule7))] @2: The squirrel sees the cat.[(((((triple3) -> rule8)) -> rule6))]
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple3
The squirrel is not cold.
("squirrel" "is" "cold" "-")
triple4
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
((triple3) -> (rule8 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
((triple3) -> (rule7 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
((((triple3) -> (rule8 % int2))) -> (rule6 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int2