The lion visits the squirrel. The mouse chases the lion. The squirrel needs the lion. If someone needs the squirrel and the squirrel needs the mouse then the mouse needs the lion. If the squirrel is big and the squirrel visits the mouse then the squirrel is not rough. If someone needs the lion then the lion visits the mouse. If someone visits the squirrel and they do not chase the squirrel then the squirrel chases the mouse. If someone chases the lion and the lion chases the squirrel then the lion visits the squirrel. If someone chases the squirrel and the squirrel is blue then they do not visit the mouse. If someone visits the mouse then they need the lion. If the squirrel does not need the lion then the lion is not blue.
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
If someone needs the squirrel and the squirrel needs the mouse then the mouse needs the lion.
((("someone" "needs" "squirrel" "+") ("squirrel" "needs" "mouse" "+")) -> ("mouse" "needs" "lion" "+"))
If the squirrel is big and the squirrel visits the mouse then the squirrel is not rough.
((("squirrel" "is" "big" "+") ("squirrel" "visits" "mouse" "+")) -> ("squirrel" "is" "rough" "-"))
If someone needs the lion then the lion visits the mouse.
((("someone" "needs" "lion" "+")) -> ("lion" "visits" "mouse" "+"))
If someone visits the squirrel and they do not chase the squirrel then the squirrel chases the mouse.
((("someone" "visits" "squirrel" "+") ("someone" "chases" "squirrel" "~")) -> ("squirrel" "chases" "mouse" "+"))
If someone chases the lion and the lion chases the squirrel then the lion visits the squirrel.
((("someone" "chases" "lion" "+") ("lion" "chases" "squirrel" "+")) -> ("lion" "visits" "squirrel" "+"))
If someone chases the squirrel and the squirrel is blue then they do not visit the mouse.
((("someone" "chases" "squirrel" "+") ("squirrel" "is" "blue" "+")) -> ("someone" "visits" "mouse" "-"))
If someone visits the mouse then they need the lion.
((("someone" "visits" "mouse" "+")) -> ("someone" "needs" "lion" "+"))
If the squirrel does not need the lion then the lion is not blue.
((("squirrel" "needs" "lion" "~")) -> ("lion" "is" "blue" "-"))
The squirrel needs the lion.
True
1
proof
[(triple3)]
("squirrel" "needs" "lion" "+")
triple3
The lion does not visit the squirrel.
False
1
inv-proof
[(triple1)]
("lion" "visits" "squirrel" "-")
triple1
The lion visits the mouse.
True
2
proof
[(((triple3) -> rule3))]
("lion" "visits" "mouse" "+")
((triple3) -> (rule3 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The lion does not visit the mouse.
False
2
inv-proof
[(((triple3) -> rule3))]
("lion" "visits" "mouse" "-")
((triple3) -> (rule3 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The lion needs the lion.
True
3
proof
[(((((triple3) -> rule3)) -> rule7))]
("lion" "needs" "lion" "+")
((((triple3) -> (rule3 % int2))) -> (rule7 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int2
The lion does not need the lion.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule7))]
("lion" "needs" "lion" "-")
((((triple3) -> (rule3 % int2))) -> (rule7 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int2
The mouse does not need the lion.
Unknown
inv-rconc
[@1: The mouse needs the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "needs" "lion" "-")
The squirrel chases the mouse.
Unknown
rconc
[@1: The squirrel chases the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "chases" "mouse" "+")
The mouse does not chase the squirrel.
Unknown
inv-random
[@0: The mouse chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "squirrel" "-")
The squirrel is red.
Unknown
random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "+")
The lion does not chase the mouse.
Unknown
inv-random
[@0: The lion chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "mouse" "-")
The mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
@0: The lion visits the squirrel.[(triple1)] The mouse chases the lion.[(triple2)] The squirrel needs the lion.[(triple3)] @1: The lion visits the mouse.[(((triple3) -> rule3))] @2: The lion needs the lion.[(((((triple3) -> rule3)) -> rule7))]
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple1
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple2
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple3
The lion visits the mouse.
("lion" "visits" "mouse" "+")
((triple3) -> (rule3 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
((((triple3) -> (rule3 % int2))) -> (rule7 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int2