The tiger is round. All cold, green things are round. If the tiger is green then the tiger is rough. Cold things are blue. All round, blue things are cold. All round things are blue. Green things are blue. Cold, rough things are round. All cold, blue things are rough.
The tiger is round.
("tiger" "is" "round" "+")
All cold, green things are round.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
If the tiger is green then the tiger is rough.
((("tiger" "is" "green" "+")) -> ("tiger" "is" "rough" "+"))
Cold things are blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
All round, blue things are cold.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
All round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
Green things are blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
Cold, rough things are round.
((("something" "is" "cold" "+") ("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
All cold, blue things are rough.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
The tiger is round.
True
1
proof
[(triple1)]
("tiger" "is" "round" "+")
triple1
The tiger is not round.
False
1
inv-proof
[(triple1)]
("tiger" "is" "round" "-")
triple1
The tiger is blue.
True
2
proof
[(((triple1) -> rule5))]
("tiger" "is" "blue" "+")
((triple1) -> (rule5 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is not blue.
False
2
inv-proof
[(((triple1) -> rule5))]
("tiger" "is" "blue" "-")
((triple1) -> (rule5 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is cold.
True
4
proof
[(((triple1 ((triple1) -> rule5)) -> rule4))]
("tiger" "is" "cold" "+")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is not cold.
False
4
inv-proof
[(((triple1 ((triple1) -> rule5)) -> rule4))]
("tiger" "is" "cold" "-")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is rough.
True
7
proof
[(((((triple1 ((triple1) -> rule5)) -> rule4) ((triple1) -> rule5)) -> rule8))]
("tiger" "is" "rough" "+")
((((triple1 ((triple1) -> (rule5 % int3))) -> (rule4 % int2)) ((triple1) -> (rule5 % int3))) -> (rule8 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3
The tiger is not rough.
False
7
inv-proof
[(((((triple1 ((triple1) -> rule5)) -> rule4) ((triple1) -> rule5)) -> rule8))]
("tiger" "is" "rough" "-")
((((triple1 ((triple1) -> (rule5 % int3))) -> (rule4 % int2)) ((triple1) -> (rule5 % int3))) -> (rule8 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3
The tiger is not green.
Unknown
inv-random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The tiger is round.[(triple1)] @1: The tiger is blue.[(((triple1) -> rule5))] @2: The tiger is cold.[(((triple1 ((triple1) -> rule5)) -> rule4))] @3: The tiger is rough.[(((((triple1 ((triple1) -> rule5)) -> rule4) ((triple1) -> rule5)) -> rule8))]
The tiger is round.
("tiger" "is" "round" "+")
triple1
The tiger is blue.
("tiger" "is" "blue" "+")
((triple1) -> (rule5 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is rough.
("tiger" "is" "rough" "+")
((((triple1 ((triple1) -> (rule5 % int3))) -> (rule4 % int2)) ((triple1) -> (rule5 % int3))) -> (rule8 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3