The lion sees the squirrel. The lion does not visit the squirrel. The squirrel visits the lion. If the squirrel sees the lion then the squirrel is red. If something sees the squirrel then the squirrel is red. If something is red and it does not see the lion then it sees the squirrel. If something visits the lion then the lion is round. If something visits the lion then the lion is rough. If the squirrel is red and the squirrel visits the lion then the lion is blue. All blue things are rough. If the lion sees the squirrel and the squirrel needs the lion then the squirrel is not blue.
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The lion does not visit the squirrel.
("lion" "visits" "squirrel" "-")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If the squirrel sees the lion then the squirrel is red.
((("squirrel" "sees" "lion" "+")) -> ("squirrel" "is" "red" "+"))
If something sees the squirrel then the squirrel is red.
((("something" "sees" "squirrel" "+")) -> ("squirrel" "is" "red" "+"))
If something is red and it does not see the lion then it sees the squirrel.
((("something" "is" "red" "+") ("something" "sees" "lion" "~")) -> ("something" "sees" "squirrel" "+"))
If something visits the lion then the lion is round.
((("something" "visits" "lion" "+")) -> ("lion" "is" "round" "+"))
If something visits the lion then the lion is rough.
((("something" "visits" "lion" "+")) -> ("lion" "is" "rough" "+"))
If the squirrel is red and the squirrel visits the lion then the lion is blue.
((("squirrel" "is" "red" "+") ("squirrel" "visits" "lion" "+")) -> ("lion" "is" "blue" "+"))
All blue things are rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If the lion sees the squirrel and the squirrel needs the lion then the squirrel is not blue.
((("lion" "sees" "squirrel" "+") ("squirrel" "needs" "lion" "+")) -> ("squirrel" "is" "blue" "-"))
The lion sees the squirrel.
True
1
proof
[(triple1)]
("lion" "sees" "squirrel" "+")
triple1
The lion visits the squirrel.
False
1
inv-proof
[(triple2)]
("lion" "visits" "squirrel" "+")
triple2
The lion is round.
True
2
proof
[(((triple3) -> rule4))]
("lion" "is" "round" "+")
((triple3) -> (rule4 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The squirrel is not red.
False
2
inv-proof
[(((triple1) -> rule2))]
("squirrel" "is" "red" "-")
((triple1) -> (rule2 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel does not see the squirrel.
Unknown
inv-rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "sees" "squirrel" "-")
The squirrel is rough.
Unknown
rconc
[@1: The squirrel is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "is" "rough" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
@0: The lion does not visit the squirrel.[(triple2)] The lion sees the squirrel.[(triple1)] The squirrel visits the lion.[(triple3)] @1: The lion is rough.[(((triple3) -> rule5) OR ((((((triple1) -> rule2) triple3) -> rule6)) -> rule7))] The lion is round.[(((triple3) -> rule4))] The squirrel is red.[(((triple1) -> rule2))] @2: The lion is blue.[(((((triple1) -> rule2) triple3) -> rule6))]
The lion does not visit the squirrel.
("lion" "visits" "squirrel" "-")
triple2
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple3
The lion is rough.
("lion" "is" "rough" "+")
((triple3) -> (rule5 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
((((((triple1) -> (rule2 % int3)) triple3) -> (rule6 % int2))) -> (rule7 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3
The lion is round.
("lion" "is" "round" "+")
((triple3) -> (rule4 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
((triple1) -> (rule2 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
((((triple1) -> (rule2 % int2)) triple3) -> (rule6 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2