Charlie is cold. Charlie is rough. Charlie is young. Green, cold things are rough. If something is round then it is green. If something is cold then it is round. Rough things are green. All green things are blue. If something is green and round then it is rough.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Green, cold things are rough.
((("something" "is" "green" "+") ("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If something is round then it is green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
If something is cold then it is round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
Rough things are green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
All green things are blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
If something is green and round then it is rough.
((("something" "is" "green" "+") ("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
Charlie is cold.
True
1
proof
[(triple1)]
("Charlie" "is" "cold" "+")
triple1
Charlie is not young.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "young" "-")
triple3
Charlie is round.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "round" "+")
((triple1) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple2) -> rule4) OR ((((triple1) -> rule3)) -> rule2))]
("Charlie" "is" "green" "-")
((triple2) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is blue.
True
3
proof
[(((((triple2) -> rule4)) -> rule5) OR ((((((triple1) -> rule3)) -> rule2)) -> rule5))]
("Charlie" "is" "blue" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is not blue.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule5) OR ((((((triple1) -> rule3)) -> rule2)) -> rule5))]
("Charlie" "is" "blue" "-")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
@0: Charlie is cold.[(triple1)] Charlie is rough.[(triple2 OR ((((((triple1) -> rule3)) -> rule2) triple1) -> rule1) OR ((((((triple1) -> rule3)) -> rule2) ((triple1) -> rule3)) -> rule6))] Charlie is young.[(triple3)] @1: Charlie is green.[(((triple2) -> rule4) OR ((((triple1) -> rule3)) -> rule2))] Charlie is round.[(((triple1) -> rule3))] @2: Charlie is blue.[(((((triple2) -> rule4)) -> rule5) OR ((((((triple1) -> rule3)) -> rule2)) -> rule5))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2)) ((triple1) -> (rule3 % int3))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
((triple2) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((triple1) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3