The lion is green. The squirrel chases the lion. The squirrel eats the lion. The squirrel is green. The squirrel is rough. The squirrel is round. The squirrel sees the lion. If something sees the squirrel then it does not chase the lion. If the lion is nice and the lion sees the squirrel then the squirrel is nice. If something is green then it is nice. If the lion is nice then the lion is not rough. If the squirrel is nice then the squirrel is rough. If something is rough and it eats the squirrel then it does not eat the lion. If the lion chases the squirrel and the squirrel does not chase the lion then the lion does not eat the squirrel. If something sees the lion then the lion does not eat the squirrel.
The lion is green.
("lion" "is" "green" "+")
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
If something sees the squirrel then it does not chase the lion.
((("something" "sees" "squirrel" "+")) -> ("something" "chases" "lion" "-"))
If the lion is nice and the lion sees the squirrel then the squirrel is nice.
((("lion" "is" "nice" "+") ("lion" "sees" "squirrel" "+")) -> ("squirrel" "is" "nice" "+"))
If something is green then it is nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If the lion is nice then the lion is not rough.
((("lion" "is" "nice" "+")) -> ("lion" "is" "rough" "-"))
If the squirrel is nice then the squirrel is rough.
((("squirrel" "is" "nice" "+")) -> ("squirrel" "is" "rough" "+"))
If something is rough and it eats the squirrel then it does not eat the lion.
((("something" "is" "rough" "+") ("something" "eats" "squirrel" "+")) -> ("something" "eats" "lion" "-"))
If the lion chases the squirrel and the squirrel does not chase the lion then the lion does not eat the squirrel.
((("lion" "chases" "squirrel" "+") ("squirrel" "chases" "lion" "~")) -> ("lion" "eats" "squirrel" "-"))
If something sees the lion then the lion does not eat the squirrel.
((("something" "sees" "lion" "+")) -> ("lion" "eats" "squirrel" "-"))
The squirrel is round.
True
1
proof
[(triple6)]
("squirrel" "is" "round" "+")
triple6
The squirrel is not rough.
False
1
inv-proof
[(triple5 OR ((((triple4) -> rule3)) -> rule5))]
("squirrel" "is" "rough" "-")
triple5
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is nice.
True
2
proof
[(((triple4) -> rule3))]
("squirrel" "is" "nice" "+")
((triple4) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is not nice.
False
2
inv-proof
[(((triple4) -> rule3))]
("squirrel" "is" "nice" "-")
((triple4) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The lion is not rough.
True
3
proof
[(((((triple1) -> rule3)) -> rule4))]
("lion" "is" "rough" "-")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The lion is not rough.
("lion" "is" "rough" "-")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion is rough.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule4))]
("lion" "is" "rough" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The lion is not rough.
("lion" "is" "rough" "-")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The squirrel does not chase the squirrel.
Unknown
inv-random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "-")
The squirrel is young.
Unknown
random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "+")
The lion is not round.
Unknown
inv-random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
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 sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
@0: The lion is green.[(triple1)] The squirrel chases the lion.[(triple2)] The squirrel eats the lion.[(triple3)] The squirrel is green.[(triple4)] The squirrel is rough.[(triple5 OR ((((triple4) -> rule3)) -> rule5))] The squirrel is round.[(triple6)] The squirrel sees the lion.[(triple7)] @1: The lion does not eat the squirrel.[(((triple7) -> rule8))] The lion is nice.[(((triple1) -> rule3))] The squirrel is nice.[(((triple4) -> rule3))] @2: The lion is not rough.[(((((triple1) -> rule3)) -> rule4))]
The lion is green.
("lion" "is" "green" "+")
triple1
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
triple2
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
triple3
The squirrel is green.
("squirrel" "is" "green" "+")
triple4
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple5
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
triple6
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple7
The lion does not eat the squirrel.
("lion" "eats" "squirrel" "-")
((triple7) -> (rule8 % int1))
The lion does not eat the squirrel.
("lion" "eats" "squirrel" "-")
int1
The lion is nice.
("lion" "is" "nice" "+")
((triple1) -> (rule3 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
((triple4) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The lion is not rough.
("lion" "is" "rough" "-")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The lion is not rough.
("lion" "is" "rough" "-")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2