The lion is big. The lion is green. The lion is not round. All blue, round things are big. If something is blue and round then it is green. All big things are blue. If the lion is blue then the lion is red. If the lion is big and the lion is blue then the lion is red. If the lion is not big then the lion is red. If the lion is blue and the lion is round then the lion is red. If the lion is blue and the lion is red then the lion is green.
The lion is big.
("lion" "is" "big" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is not round.
("lion" "is" "round" "-")
All blue, round things are big.
((("something" "is" "blue" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If something is blue and round then it is green.
((("something" "is" "blue" "+") ("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
All big things are blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
If the lion is blue then the lion is red.
((("lion" "is" "blue" "+")) -> ("lion" "is" "red" "+"))
If the lion is big and the lion is blue then the lion is red.
((("lion" "is" "big" "+") ("lion" "is" "blue" "+")) -> ("lion" "is" "red" "+"))
If the lion is not big then the lion is red.
((("lion" "is" "big" "~")) -> ("lion" "is" "red" "+"))
If the lion is blue and the lion is round then the lion is red.
((("lion" "is" "blue" "+") ("lion" "is" "round" "+")) -> ("lion" "is" "red" "+"))
If the lion is blue and the lion is red then the lion is green.
((("lion" "is" "blue" "+") ("lion" "is" "red" "+")) -> ("lion" "is" "green" "+"))
The lion is not round.
True
1
proof
[(triple3)]
("lion" "is" "round" "-")
triple3
The lion is not green.
False
1
inv-proof
[(triple2 OR ((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule4)) -> rule8) OR ((((triple1) -> rule3) ((triple1 ((triple1) -> rule3)) -> rule5)) -> rule8))]
("lion" "is" "green" "-")
triple2
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
((((triple1) -> (rule3 % int3)) ((triple1 ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
The lion is blue.
True
2
proof
[(((triple1) -> rule3))]
("lion" "is" "blue" "+")
((triple1) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is not blue.
False
2
inv-proof
[(((triple1) -> rule3))]
("lion" "is" "blue" "-")
((triple1) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is red.
True
3
proof
[(((((triple1) -> rule3)) -> rule4) OR ((triple1 ((triple1) -> rule3)) -> rule5))]
("lion" "is" "red" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
((triple1 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion is not red.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule4) OR ((triple1 ((triple1) -> rule3)) -> rule5))]
("lion" "is" "red" "-")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
((triple1 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
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 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 big.[(triple1)] The lion is green.[(triple2 OR ((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule4)) -> rule8) OR ((((triple1) -> rule3) ((triple1 ((triple1) -> rule3)) -> rule5)) -> rule8))] The lion is not round.[(triple3)] @1: The lion is blue.[(((triple1) -> rule3))] @2: The lion is red.[(((((triple1) -> rule3)) -> rule4) OR ((triple1 ((triple1) -> rule3)) -> rule5))]
The lion is big.
("lion" "is" "big" "+")
triple1
The lion is green.
("lion" "is" "green" "+")
triple2
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
((((triple1) -> (rule3 % int3)) ((triple1 ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
The lion is not round.
("lion" "is" "round" "-")
triple3
The lion is blue.
("lion" "is" "blue" "+")
((triple1) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is red.
("lion" "is" "red" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
((triple1 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2