The lion needs the squirrel. The squirrel needs the lion. If someone is nice then they see the squirrel. If someone visits the squirrel then they are nice. If someone sees the squirrel then they visit the squirrel. If someone visits the lion and the lion is nice then they see the lion. If someone visits the squirrel and they see the lion then the squirrel is nice. If someone sees the squirrel then they are green. If someone needs the lion then the lion visits the squirrel. If someone sees the lion then the lion is kind.
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
If someone is nice then they see the squirrel.
((("someone" "is" "nice" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone visits the squirrel then they are nice.
((("someone" "visits" "squirrel" "+")) -> ("someone" "is" "nice" "+"))
If someone sees the squirrel then they visit the squirrel.
((("someone" "sees" "squirrel" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone visits the lion and the lion is nice then they see the lion.
((("someone" "visits" "lion" "+") ("lion" "is" "nice" "+")) -> ("someone" "sees" "lion" "+"))
If someone visits the squirrel and they see the lion then the squirrel is nice.
((("someone" "visits" "squirrel" "+") ("someone" "sees" "lion" "+")) -> ("squirrel" "is" "nice" "+"))
If someone sees the squirrel then they are green.
((("someone" "sees" "squirrel" "+")) -> ("someone" "is" "green" "+"))
If someone needs the lion then the lion visits the squirrel.
((("someone" "needs" "lion" "+")) -> ("lion" "visits" "squirrel" "+"))
If someone sees the lion then the lion is kind.
((("someone" "sees" "lion" "+")) -> ("lion" "is" "kind" "+"))
The lion needs the squirrel.
True
1
proof
[(triple1)]
("lion" "needs" "squirrel" "+")
triple1
The squirrel does not need the lion.
False
1
inv-proof
[(triple2)]
("squirrel" "needs" "lion" "-")
triple2
The lion visits the squirrel.
True
2
proof
[(((triple2) -> rule7))]
("lion" "visits" "squirrel" "+")
((triple2) -> (rule7 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The lion does not visit the squirrel.
False
2
inv-proof
[(((triple2) -> rule7))]
("lion" "visits" "squirrel" "-")
((triple2) -> (rule7 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The lion is nice.
True
3
proof
[(((((triple2) -> rule7)) -> rule2))]
("lion" "is" "nice" "+")
((((triple2) -> (rule7 % int2))) -> (rule2 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The lion is not nice.
False
3
inv-proof
[(((((triple2) -> rule7)) -> rule2))]
("lion" "is" "nice" "-")
((((triple2) -> (rule7 % int2))) -> (rule2 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The lion is not kind.
Unknown
inv-rconc
[@2: The lion is kind.[CWA. Example of deepest failure = (rule8 <- rule4 <- FAIL)]]
("lion" "is" "kind" "-")
The squirrel is green.
Unknown
rconc
[@4: The squirrel is green.[CWA. Example of deepest failure = (rule6 <- rule1 <- rule2 <- rule3 <- FAIL)]]
("squirrel" "is" "green" "+")
The squirrel does not see the squirrel.
Unknown
inv-rconc
[@3: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule3 <- FAIL)]]
("squirrel" "sees" "squirrel" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
The squirrel does not visit the lion.
Unknown
inv-random
[@0: The squirrel visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "lion" "-")
The lion is rough.
Unknown
random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "+")
@0: The lion needs the squirrel.[(triple1)] The squirrel needs the lion.[(triple2)] @1: The lion visits the squirrel.[(((triple2) -> rule7))] @2: The lion is nice.[(((((triple2) -> rule7)) -> rule2))] @3: The lion sees the squirrel.[(((((((triple2) -> rule7)) -> rule2)) -> rule1))] @4: The lion is green.[(((((((((triple2) -> rule7)) -> rule2)) -> rule1)) -> rule6))]
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple1
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple2
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
((triple2) -> (rule7 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
((((triple2) -> (rule7 % int2))) -> (rule2 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
((((((triple2) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int3
The lion is green.
("lion" "is" "green" "+")
((((((((triple2) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int4