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