Erin is white. If Erin is kind then Erin is not round. White things are rough. Kind things are white. Rough things are kind. All cold things are nice. All rough things are cold. If something is white then it is green. If something is green and not nice then it is round.
Erin is white.
("Erin" "is" "white" "+")
If Erin is kind then Erin is not round.
((("Erin" "is" "kind" "+")) -> ("Erin" "is" "round" "-"))
White things are rough.
((("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
Kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
All cold things are nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
All rough things are cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If something is white then it is green.
((("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
If something is green and not nice then it is round.
((("something" "is" "green" "+") ("something" "is" "nice" "~")) -> ("something" "is" "round" "+"))
Erin is white.
True
1
proof
[(triple1)]
("Erin" "is" "white" "+")
triple1
Erin is not white.
False
1
inv-proof
[(triple1)]
("Erin" "is" "white" "-")
triple1
Erin is rough.
True
2
proof
[(((triple1) -> rule2))]
("Erin" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple1) -> rule7))]
("Erin" "is" "green" "-")
((triple1) -> (rule7 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
@0: Erin is white.[(triple1)] @1: Erin is green.[(((triple1) -> rule7))] Erin is rough.[(((triple1) -> rule2))] @2: Erin is cold.[(((((triple1) -> rule2)) -> rule6))] Erin is kind.[(((((triple1) -> rule2)) -> rule4))] @3: Erin is nice.[(((((((triple1) -> rule2)) -> rule6)) -> rule5))] Erin is not round.[(((((((triple1) -> rule2)) -> rule4)) -> rule1))]
Erin is white.
("Erin" "is" "white" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
((triple1) -> (rule7 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is not round.
("Erin" "is" "round" "-")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Erin is not round.
("Erin" "is" "round" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3