Erin is nice. Erin is rough. Erin is white. If someone is nice then they are cold. If someone is rough and cold then they are furry. If Erin is round and Erin is not nice then Erin is not furry. If someone is green and not rough then they are round. If someone is furry and cold then they are round. If someone is furry and not cold then they are round.
Erin is nice.
("Erin" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is white.
("Erin" "is" "white" "+")
If someone is nice then they are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If someone is rough and cold then they are furry.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
If Erin is round and Erin is not nice then Erin is not furry.
((("Erin" "is" "round" "+") ("Erin" "is" "nice" "~")) -> ("Erin" "is" "furry" "-"))
If someone is green and not rough then they are round.
((("someone" "is" "green" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "round" "+"))
If someone is furry and cold then they are round.
((("someone" "is" "furry" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If someone is furry and not cold then they are round.
((("someone" "is" "furry" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "round" "+"))
Erin is rough.
True
1
proof
[(triple2)]
("Erin" "is" "rough" "+")
triple2
Erin is not nice.
False
1
inv-proof
[(triple1)]
("Erin" "is" "nice" "-")
triple1
Erin is cold.
True
2
proof
[(((triple1) -> rule1))]
("Erin" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not cold.
False
2
inv-proof
[(((triple1) -> rule1))]
("Erin" "is" "cold" "-")
((triple1) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
True
4
proof
[(((triple2 ((triple1) -> rule1)) -> rule2))]
("Erin" "is" "furry" "+")
((triple2 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is not furry.
False
4
inv-proof
[(((triple2 ((triple1) -> rule1)) -> rule2))]
("Erin" "is" "furry" "-")
((triple2 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is round.
True
7
proof
[(((((triple2 ((triple1) -> rule1)) -> rule2) ((triple1) -> rule1)) -> rule5))]
("Erin" "is" "round" "+")
((((triple2 ((triple1) -> (rule1 % int3))) -> (rule2 % int2)) ((triple1) -> (rule1 % int3))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is not round.
False
7
inv-proof
[(((((triple2 ((triple1) -> rule1)) -> rule2) ((triple1) -> rule1)) -> rule5))]
("Erin" "is" "round" "-")
((((triple2 ((triple1) -> (rule1 % int3))) -> (rule2 % int2)) ((triple1) -> (rule1 % int3))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
@0: Erin is nice.[(triple1)] Erin is rough.[(triple2)] Erin is white.[(triple3)] @1: Erin is cold.[(((triple1) -> rule1))] @2: Erin is furry.[(((triple2 ((triple1) -> rule1)) -> rule2))] @3: Erin is round.[(((((triple2 ((triple1) -> rule1)) -> rule2) ((triple1) -> rule1)) -> rule5))]
Erin is nice.
("Erin" "is" "nice" "+")
triple1
Erin is rough.
("Erin" "is" "rough" "+")
triple2
Erin is white.
("Erin" "is" "white" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple2 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((((triple2 ((triple1) -> (rule1 % int3))) -> (rule2 % int2)) ((triple1) -> (rule1 % int3))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3