The lion is round. The rabbit is cold. The squirrel sees the lion. If someone visits the rabbit then the rabbit is big. If someone is blue then they see the lion. If someone visits the squirrel then the squirrel eats the rabbit. If someone is nice then they are blue. If someone sees the lion then the lion is nice. If someone sees the squirrel and they are nice then they visit the squirrel. If someone sees the rabbit and the rabbit sees the squirrel then the rabbit sees the lion. If someone visits the squirrel and the squirrel visits the rabbit then they eat the rabbit.
The lion is round.
("lion" "is" "round" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
If someone visits the rabbit then the rabbit is big.
((("someone" "visits" "rabbit" "+")) -> ("rabbit" "is" "big" "+"))
If someone is blue then they see the lion.
((("someone" "is" "blue" "+")) -> ("someone" "sees" "lion" "+"))
If someone visits the squirrel then the squirrel eats the rabbit.
((("someone" "visits" "squirrel" "+")) -> ("squirrel" "eats" "rabbit" "+"))
If someone is nice then they are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
If someone sees the lion then the lion is nice.
((("someone" "sees" "lion" "+")) -> ("lion" "is" "nice" "+"))
If someone sees the squirrel and they are nice then they visit the squirrel.
((("someone" "sees" "squirrel" "+") ("someone" "is" "nice" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone sees the rabbit and the rabbit sees the squirrel then the rabbit sees the lion.
((("someone" "sees" "rabbit" "+") ("rabbit" "sees" "squirrel" "+")) -> ("rabbit" "sees" "lion" "+"))
If someone visits the squirrel and the squirrel visits the rabbit then they eat the rabbit.
((("someone" "visits" "squirrel" "+") ("squirrel" "visits" "rabbit" "+")) -> ("someone" "eats" "rabbit" "+"))
The lion is round.
True
1
proof
[(triple1)]
("lion" "is" "round" "+")
triple1
The rabbit is not cold.
False
1
inv-proof
[(triple2)]
("rabbit" "is" "cold" "-")
triple2
The lion is nice.
True
2
proof
[(((triple3) -> rule5))]
("lion" "is" "nice" "+")
((triple3) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is not nice.
False
2
inv-proof
[(((triple3) -> rule5))]
("lion" "is" "nice" "-")
((triple3) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
True
3
proof
[(((((triple3) -> rule5)) -> rule4))]
("lion" "is" "blue" "+")
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion is not blue.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule4))]
("lion" "is" "blue" "-")
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion sees the lion.
True
4
proof
[(((((((triple3) -> rule5)) -> rule4)) -> rule2))]
("lion" "sees" "lion" "+")
((((((triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3
The lion does not see the lion.
False
4
inv-proof
[(((((((triple3) -> rule5)) -> rule4)) -> rule2))]
("lion" "sees" "lion" "-")
((((((triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3
The squirrel does not eat the rabbit.
Unknown
inv-rconc
[@2: The squirrel eats the rabbit.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("squirrel" "eats" "rabbit" "-")
The rabbit is big.
Unknown
rconc
[@1: The rabbit is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "big" "+")
The rabbit does not visit the squirrel.
Unknown
inv-rconc
[@1: The rabbit visits the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "visits" "squirrel" "-")
The squirrel visits the squirrel.
Unknown
rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "visits" "squirrel" "+")
The rabbit is not nice.
Unknown
inv-random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "-")
The lion eats the squirrel.
Unknown
random
[@0: The lion eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "squirrel" "+")
The squirrel is not nice.
Unknown
inv-random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
@0: The lion is round.[(triple1)] The rabbit is cold.[(triple2)] The squirrel sees the lion.[(triple3)] @1: The lion is nice.[(((triple3) -> rule5))] @2: The lion is blue.[(((((triple3) -> rule5)) -> rule4))] @3: The lion sees the lion.[(((((((triple3) -> rule5)) -> rule4)) -> rule2))]
The lion is round.
("lion" "is" "round" "+")
triple1
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple2
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple3
The lion is nice.
("lion" "is" "nice" "+")
((triple3) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion sees the lion.
("lion" "sees" "lion" "+")
((((((triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3