Anne is blue. Anne is cold. Anne is white. If Anne is blue then Anne is green. If Anne is green then Anne is round. If something is white and round then it is quiet.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is white.
("Anne" "is" "white" "+")
If Anne is blue then Anne is green.
((("Anne" "is" "blue" "+")) -> ("Anne" "is" "green" "+"))
If Anne is green then Anne is round.
((("Anne" "is" "green" "+")) -> ("Anne" "is" "round" "+"))
If something is white and round then it is quiet.
((("something" "is" "white" "+") ("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
Anne is cold.
True
1
proof
[(triple2)]
("Anne" "is" "cold" "+")
triple2
Anne is not white.
False
1
inv-proof
[(triple3)]
("Anne" "is" "white" "-")
triple3
Anne is green.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "green" "+")
((triple1) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is not green.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "green" "-")
((triple1) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is round.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("Anne" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not round.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("Anne" "is" "round" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is quiet.
True
5
proof
[(((triple3 ((((triple1) -> rule1)) -> rule2)) -> rule3))]
("Anne" "is" "quiet" "+")
((triple3 ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is not quiet.
False
5
inv-proof
[(((triple3 ((((triple1) -> rule1)) -> rule2)) -> rule3))]
("Anne" "is" "quiet" "-")
((triple3 ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
@0: Anne is blue.[(triple1)] Anne is cold.[(triple2)] Anne is white.[(triple3)] @1: Anne is green.[(((triple1) -> rule1))] @2: Anne is round.[(((((triple1) -> rule1)) -> rule2))] @3: Anne is quiet.[(((triple3 ((((triple1) -> rule1)) -> rule2)) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple3 ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3