Erin is cold. If something is cold and blue then it is furry. Furry things are red. If something is furry then it is nice. If Erin is cold then Erin is furry. Red things are green. If Erin is cold then Erin is white.
Erin is cold.
("Erin" "is" "cold" "+")
If something is cold and blue then it is furry.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
Furry things are red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
If something is furry then it is nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
If Erin is cold then Erin is furry.
((("Erin" "is" "cold" "+")) -> ("Erin" "is" "furry" "+"))
Red things are green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If Erin is cold then Erin is white.
((("Erin" "is" "cold" "+")) -> ("Erin" "is" "white" "+"))
Erin is cold.
True
1
proof
[(triple1)]
("Erin" "is" "cold" "+")
triple1
Erin is not cold.
False
1
inv-proof
[(triple1)]
("Erin" "is" "cold" "-")
triple1
Erin is furry.
True
2
proof
[(((triple1) -> rule4))]
("Erin" "is" "furry" "+")
((triple1) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is not white.
False
2
inv-proof
[(((triple1) -> rule6))]
("Erin" "is" "white" "-")
((triple1) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is nice.
True
3
proof
[(((((triple1) -> rule4)) -> rule3))]
("Erin" "is" "nice" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is not red.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule2))]
("Erin" "is" "red" "-")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is green.
True
4
proof
[(((((((triple1) -> rule4)) -> rule2)) -> rule5))]
("Erin" "is" "green" "+")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is not green.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule2)) -> rule5))]
("Erin" "is" "green" "-")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
@0: Erin is cold.[(triple1)] @1: Erin is furry.[(((triple1) -> rule4))] Erin is white.[(((triple1) -> rule6))] @2: Erin is nice.[(((((triple1) -> rule4)) -> rule3))] Erin is red.[(((((triple1) -> rule4)) -> rule2))] @3: Erin is green.[(((((((triple1) -> rule4)) -> rule2)) -> rule5))]
Erin is cold.
("Erin" "is" "cold" "+")
triple1
Erin is furry.
("Erin" "is" "furry" "+")
((triple1) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple1) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3