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