Erin is nice. Erin is rough. Erin is white. Round things are red. If Erin is nice then Erin is round. If something is red then it is not blue. Smart things are blue. If something is red and not round then it is white. If Erin is not red then Erin is blue.
Erin is nice.
("Erin" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is white.
("Erin" "is" "white" "+")
Round things are red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
If Erin is nice then Erin is round.
((("Erin" "is" "nice" "+")) -> ("Erin" "is" "round" "+"))
If something is red then it is not blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "-"))
Smart things are blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
If something is red and not round then it is white.
((("something" "is" "red" "+") ("something" "is" "round" "~")) -> ("something" "is" "white" "+"))
If Erin is not red then Erin is blue.
((("Erin" "is" "red" "~")) -> ("Erin" "is" "blue" "+"))
Erin is white.
True
1
proof
[(triple3)]
("Erin" "is" "white" "+")
triple3
Erin is not white.
False
1
inv-proof
[(triple3)]
("Erin" "is" "white" "-")
triple3
Erin is round.
True
2
proof
[(((triple1) -> rule2))]
("Erin" "is" "round" "+")
((triple1) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is not round.
False
2
inv-proof
[(((triple1) -> rule2))]
("Erin" "is" "round" "-")
((triple1) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("Erin" "is" "red" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is not red.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("Erin" "is" "red" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is not blue.
True
4
proof
[(((((((triple1) -> rule2)) -> rule1)) -> rule3))]
("Erin" "is" "blue" "-")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is blue.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule1)) -> rule3))]
("Erin" "is" "blue" "+")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
@0: Erin is nice.[(triple1)] Erin is rough.[(triple2)] Erin is white.[(triple3)] @1: Erin is round.[(((triple1) -> rule2))] @2: Erin is red.[(((((triple1) -> rule2)) -> rule1))] @3: Erin is not blue.[(((((((triple1) -> rule2)) -> rule1)) -> rule3))]
Erin is nice.
("Erin" "is" "nice" "+")
triple1
Erin is rough.
("Erin" "is" "rough" "+")
triple2
Erin is white.
("Erin" "is" "white" "+")
triple3
Erin is round.
("Erin" "is" "round" "+")
((triple1) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is not blue.
("Erin" "is" "blue" "-")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3