The lion is red. If the lion is red then the lion is nice. All red, nice people are cold. If someone is cold then they are round.
The lion is red.
("lion" "is" "red" "+")
If the lion is red then the lion is nice.
((("lion" "is" "red" "+")) -> ("lion" "is" "nice" "+"))
All red, nice people are cold.
((("someone" "is" "red" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold then they are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
The lion is red.
True
1
proof
[(triple1)]
("lion" "is" "red" "+")
triple1
The lion is not red.
False
1
inv-proof
[(triple1)]
("lion" "is" "red" "-")
triple1
The lion is nice.
True
2
proof
[(((triple1) -> rule1))]
("lion" "is" "nice" "+")
((triple1) -> (rule1 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is not nice.
False
2
inv-proof
[(((triple1) -> rule1))]
("lion" "is" "nice" "-")
((triple1) -> (rule1 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is cold.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule2))]
("lion" "is" "cold" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion is not cold.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule2))]
("lion" "is" "cold" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion is round.
True
5
proof
[(((((triple1 ((triple1) -> rule1)) -> rule2)) -> rule3))]
("lion" "is" "round" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3
The lion is not round.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule1)) -> rule2)) -> rule3))]
("lion" "is" "round" "-")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3
The lion does not like the lion.
Unknown
inv-random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
The lion does not visit the lion.
Unknown
inv-random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "-")
The lion is green.
Unknown
random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "+")
@0: The lion is red.[(triple1)] @1: The lion is nice.[(((triple1) -> rule1))] @2: The lion is cold.[(((triple1 ((triple1) -> rule1)) -> rule2))] @3: The lion is round.[(((((triple1 ((triple1) -> rule1)) -> rule2)) -> rule3))]
The lion is red.
("lion" "is" "red" "+")
triple1
The lion is nice.
("lion" "is" "nice" "+")
((triple1) -> (rule1 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion is round.
("lion" "is" "round" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3