Gary is cold. All red, big things are cold. All rough things are cold. Cold things are kind. If Gary is red and Gary is rough then Gary is big. All blue things are rough. All cold things are red. Nice, kind things are cold. All red things are blue.
Gary is cold.
("Gary" "is" "cold" "+")
All red, big things are cold.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
All rough things are cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
Cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
If Gary is red and Gary is rough then Gary is big.
((("Gary" "is" "red" "+") ("Gary" "is" "rough" "+")) -> ("Gary" "is" "big" "+"))
All blue things are rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
All cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
Nice, kind things are cold.
((("something" "is" "nice" "+") ("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
All red things are blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
Gary is cold.
True
1
proof
[(triple1)]
("Gary" "is" "cold" "+")
triple1
Gary is not cold.
False
1
inv-proof
[(triple1)]
("Gary" "is" "cold" "-")
triple1
Gary is red.
True
2
proof
[(((triple1) -> rule6))]
("Gary" "is" "red" "+")
((triple1) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is not kind.
False
2
inv-proof
[(((triple1) -> rule3))]
("Gary" "is" "kind" "-")
((triple1) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is blue.
True
3
proof
[(((((triple1) -> rule6)) -> rule8))]
("Gary" "is" "blue" "+")
((((triple1) -> (rule6 % int2))) -> (rule8 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not blue.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule8))]
("Gary" "is" "blue" "-")
((((triple1) -> (rule6 % int2))) -> (rule8 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is rough.
True
4
proof
[(((((((triple1) -> rule6)) -> rule8)) -> rule5))]
("Gary" "is" "rough" "+")
((((((triple1) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is not rough.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule8)) -> rule5))]
("Gary" "is" "rough" "-")
((((((triple1) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
@0: Gary is cold.[(triple1)] @1: Gary is kind.[(((triple1) -> rule3))] Gary is red.[(((triple1) -> rule6))] @2: Gary is blue.[(((((triple1) -> rule6)) -> rule8))] @3: Gary is rough.[(((((((triple1) -> rule6)) -> rule8)) -> rule5))] @4: Gary is big.[(((((triple1) -> rule6) ((((((triple1) -> rule6)) -> rule8)) -> rule5)) -> rule4))]
Gary is cold.
("Gary" "is" "cold" "+")
triple1
Gary is kind.
("Gary" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple1) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((((triple1) -> (rule6 % int2))) -> (rule8 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((((((triple1) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
((((triple1) -> (rule6 % int4)) ((((((triple1) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4