The lion is blue. The lion is round. The lion is young. If the lion is green then the lion is young. If the lion is green and the lion is blue then the lion is round. Blue, young things are green. If something is blue then it is nice. If something is young then it is green. If the lion is blue and the lion is nice then the lion is green.
The lion is blue.
("lion" "is" "blue" "+")
The lion is round.
("lion" "is" "round" "+")
The lion is young.
("lion" "is" "young" "+")
If the lion is green then the lion is young.
((("lion" "is" "green" "+")) -> ("lion" "is" "young" "+"))
If the lion is green and the lion is blue then the lion is round.
((("lion" "is" "green" "+") ("lion" "is" "blue" "+")) -> ("lion" "is" "round" "+"))
Blue, young things are green.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If something is blue then it is nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
If something is young then it is green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If the lion is blue and the lion is nice then the lion is green.
((("lion" "is" "blue" "+") ("lion" "is" "nice" "+")) -> ("lion" "is" "green" "+"))
The lion is blue.
True
1
proof
[(triple1)]
("lion" "is" "blue" "+")
triple1
The lion is not blue.
False
1
inv-proof
[(triple1)]
("lion" "is" "blue" "-")
triple1
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
@0: The lion is blue.[(triple1)] The lion is round.[(triple2 OR ((((triple3) -> rule5) triple1) -> rule2) OR ((((triple1 triple3) -> rule3) triple1) -> rule2) OR ((((triple1 ((triple1) -> rule4)) -> rule6) triple1) -> rule2))] The lion is young.[(triple3 OR ((((triple1 ((triple1) -> rule4)) -> rule6)) -> rule1))] @1: The lion is green.[(((triple3) -> rule5) OR ((triple1 triple3) -> rule3) OR ((triple1 ((triple1) -> rule4)) -> rule6))] The lion is nice.[(((triple1) -> rule4))]
The lion is blue.
("lion" "is" "blue" "+")
triple1
The lion is round.
("lion" "is" "round" "+")
triple2
((((triple3) -> (rule5 % int2)) triple1) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
((((triple1 triple3) -> (rule3 % int2)) triple1) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3
The lion is young.
("lion" "is" "young" "+")
triple3
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3
The lion is green.
("lion" "is" "green" "+")
((triple3) -> (rule5 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
((triple1 triple3) -> (rule3 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
((triple1 ((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
((triple1) -> (rule4 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1