The lion is big. All big, cold people are blue. If the lion is blue and the lion is not young then the lion is cold. If someone is blue and big then they are red. Big people are cold. If someone is blue and not young then they are cold. If the lion is not young then the lion is big.
The lion is big.
("lion" "is" "big" "+")
All big, cold people are blue.
((("someone" "is" "big" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
If the lion is blue and the lion is not young then the lion is cold.
((("lion" "is" "blue" "+") ("lion" "is" "young" "~")) -> ("lion" "is" "cold" "+"))
If someone is blue and big then they are red.
((("someone" "is" "blue" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
Big people are cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
If someone is blue and not young then they are cold.
((("someone" "is" "blue" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "cold" "+"))
If the lion is not young then the lion is big.
((("lion" "is" "young" "~")) -> ("lion" "is" "big" "+"))
The lion is big.
True
1
proof
[(triple1)]
("lion" "is" "big" "+")
triple1
The lion is not big.
False
1
inv-proof
[(triple1)]
("lion" "is" "big" "-")
triple1
The lion is cold.
True
2
proof
[(((triple1) -> rule4))]
("lion" "is" "cold" "+")
((triple1) -> (rule4 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is not cold.
False
2
inv-proof
[(((triple1) -> rule4))]
("lion" "is" "cold" "-")
((triple1) -> (rule4 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is blue.
True
4
proof
[(((triple1 ((triple1) -> rule4)) -> rule1))]
("lion" "is" "blue" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is not blue.
False
4
inv-proof
[(((triple1 ((triple1) -> rule4)) -> rule1))]
("lion" "is" "blue" "-")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is red.
True
6
proof
[(((((triple1 ((triple1) -> rule4)) -> rule1) triple1) -> rule3))]
("lion" "is" "red" "+")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule1 % int2)) triple1) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The lion is not red.
False
6
inv-proof
[(((((triple1 ((triple1) -> rule4)) -> rule1) triple1) -> rule3))]
("lion" "is" "red" "-")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule1 % int2)) triple1) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
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" "+")
The lion is not young.
Unknown
inv-random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
@0: The lion is big.[(triple1)] @1: The lion is cold.[(((triple1) -> rule4))] @2: The lion is blue.[(((triple1 ((triple1) -> rule4)) -> rule1))] @3: The lion is red.[(((((triple1 ((triple1) -> rule4)) -> rule1) triple1) -> rule3))]
The lion is big.
("lion" "is" "big" "+")
triple1
The lion is cold.
("lion" "is" "cold" "+")
((triple1) -> (rule4 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is red.
("lion" "is" "red" "+")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule1 % int2)) triple1) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3