The tiger is cold. All blue people are green. All blue, round people are cold. Cold people are green. Green people are cold. If someone is round then they are green. All cold, nice people are round. If the tiger is green then the tiger is round. All round, cold people are nice.
The tiger is cold.
("tiger" "is" "cold" "+")
All blue people are green.
((("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
All blue, round people are cold.
((("someone" "is" "blue" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
Cold people are green.
((("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
Green people are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
If someone is round then they are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
All cold, nice people are round.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
If the tiger is green then the tiger is round.
((("tiger" "is" "green" "+")) -> ("tiger" "is" "round" "+"))
All round, cold people are nice.
((("someone" "is" "round" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
The tiger is cold.
True
1
proof
[(triple1)]
("tiger" "is" "cold" "+")
triple1
The tiger is not cold.
False
1
inv-proof
[(triple1)]
("tiger" "is" "cold" "-")
triple1
The tiger is green.
True
2
proof
[(((triple1) -> rule3))]
("tiger" "is" "green" "+")
((triple1) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is not green.
False
2
inv-proof
[(((triple1) -> rule3))]
("tiger" "is" "green" "-")
((triple1) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is round.
True
3
proof
[(((((triple1) -> rule3)) -> rule7))]
("tiger" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger is not round.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule7))]
("tiger" "is" "round" "-")
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger is nice.
True
5
proof
[(((((((triple1) -> rule3)) -> rule7) triple1) -> rule8))]
("tiger" "is" "nice" "+")
((((((triple1) -> (rule3 % int3))) -> (rule7 % int2)) triple1) -> (rule8 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The tiger is not nice.
False
5
inv-proof
[(((((((triple1) -> rule3)) -> rule7) triple1) -> rule8))]
("tiger" "is" "nice" "-")
((((((triple1) -> (rule3 % int3))) -> (rule7 % int2)) triple1) -> (rule8 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
The tiger does not chase the tiger.
Unknown
inv-random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "-")
The tiger is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
@0: The tiger is cold.[(triple1)] @1: The tiger is green.[(((triple1) -> rule3))] @2: The tiger is round.[(((((triple1) -> rule3)) -> rule7))] @3: The tiger is nice.[(((((((triple1) -> rule3)) -> rule7) triple1) -> rule8))]
The tiger is cold.
("tiger" "is" "cold" "+")
triple1
The tiger is green.
("tiger" "is" "green" "+")
((triple1) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
((((((triple1) -> (rule3 % int3))) -> (rule7 % int2)) triple1) -> (rule8 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3