Charlie is cold. All rough things are blue. If Charlie is cold then Charlie is red. Blue things are red. All cold, red things are rough. All blue things are kind. All rough things are green.
Charlie is cold.
("Charlie" "is" "cold" "+")
All rough things are blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
If Charlie is cold then Charlie is red.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "red" "+"))
Blue things are red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
All cold, red things are rough.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
All blue things are kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
All rough things are green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
Charlie is cold.
True
1
proof
[(triple1)]
("Charlie" "is" "cold" "+")
triple1
Charlie is not cold.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "cold" "-")
triple1
Charlie is red.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "red" "+")
((triple1) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is not red.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "red" "-")
((triple1) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is rough.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule4))]
("Charlie" "is" "rough" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is not rough.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule4))]
("Charlie" "is" "rough" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is green.
True
5
proof
[(((((triple1 ((triple1) -> rule2)) -> rule4)) -> rule6))]
("Charlie" "is" "green" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is not blue.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule2)) -> rule4)) -> rule1))]
("Charlie" "is" "blue" "-")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
@0: Charlie is cold.[(triple1)] @1: Charlie is red.[(((triple1) -> rule2))] @2: Charlie is rough.[(((triple1 ((triple1) -> rule2)) -> rule4))] @3: Charlie is blue.[(((((triple1 ((triple1) -> rule2)) -> rule4)) -> rule1))] Charlie is green.[(((((triple1 ((triple1) -> rule2)) -> rule4)) -> rule6))] @4: Charlie is kind.[(((((((triple1 ((triple1) -> rule2)) -> rule4)) -> rule1)) -> rule5))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
((triple1) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
((((((triple1 ((triple1) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4