The tiger is rough. If something is cold then it is big. If something is big then it is green. Big, rough things are green. If something is rough then it is cold. If the tiger is big then the tiger is blue. Cold, big things are blue.
The tiger is rough.
("tiger" "is" "rough" "+")
If something is cold then it is big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If something is big then it is green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
Big, rough things are green.
((("something" "is" "big" "+") ("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
If something is rough then it is cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If the tiger is big then the tiger is blue.
((("tiger" "is" "big" "+")) -> ("tiger" "is" "blue" "+"))
Cold, big things are blue.
((("something" "is" "cold" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
The tiger is rough.
True
1
proof
[(triple1)]
("tiger" "is" "rough" "+")
triple1
The tiger is not rough.
False
1
inv-proof
[(triple1)]
("tiger" "is" "rough" "-")
triple1
The tiger is cold.
True
2
proof
[(((triple1) -> rule4))]
("tiger" "is" "cold" "+")
((triple1) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is not cold.
False
2
inv-proof
[(((triple1) -> rule4))]
("tiger" "is" "cold" "-")
((triple1) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is big.
True
3
proof
[(((((triple1) -> rule4)) -> rule1))]
("tiger" "is" "big" "+")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is not big.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule1))]
("tiger" "is" "big" "-")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is blue.
True
4
proof
[(((((((triple1) -> rule4)) -> rule1)) -> rule5) OR ((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule1)) -> rule6))]
("tiger" "is" "blue" "+")
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
The tiger is not blue.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule1)) -> rule5) OR ((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule1)) -> rule6))]
("tiger" "is" "blue" "-")
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
@0: The tiger is rough.[(triple1)] @1: The tiger is cold.[(((triple1) -> rule4))] @2: The tiger is big.[(((((triple1) -> rule4)) -> rule1))] @3: The tiger is blue.[(((((((triple1) -> rule4)) -> rule1)) -> rule5) OR ((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule1)) -> rule6))] The tiger is green.[(((((((triple1) -> rule4)) -> rule1)) -> rule2) OR ((((((triple1) -> rule4)) -> rule1) triple1) -> rule3))]
The tiger is rough.
("tiger" "is" "rough" "+")
triple1
The tiger is cold.
("tiger" "is" "cold" "+")
((triple1) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
The tiger is green.
("tiger" "is" "green" "+")
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2)) triple1) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3