Erin is red. All kind, red things are rough. Nice things are kind. If Erin is red then Erin is white. If Erin is rough and Erin is not red then Erin is round. White things are nice. If something is red then it is furry.
Erin is red.
("Erin" "is" "red" "+")
All kind, red things are rough.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
Nice things are kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
If Erin is red then Erin is white.
((("Erin" "is" "red" "+")) -> ("Erin" "is" "white" "+"))
If Erin is rough and Erin is not red then Erin is round.
((("Erin" "is" "rough" "+") ("Erin" "is" "red" "~")) -> ("Erin" "is" "round" "+"))
White things are nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
If something is red then it is furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
Erin is red.
True
1
proof
[(triple1)]
("Erin" "is" "red" "+")
triple1
Erin is not red.
False
1
inv-proof
[(triple1)]
("Erin" "is" "red" "-")
triple1
Erin is furry.
True
2
proof
[(((triple1) -> rule6))]
("Erin" "is" "furry" "+")
((triple1) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is not furry.
False
2
inv-proof
[(((triple1) -> rule6))]
("Erin" "is" "furry" "-")
((triple1) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is nice.
True
3
proof
[(((((triple1) -> rule3)) -> rule5))]
("Erin" "is" "nice" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is not nice.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule5))]
("Erin" "is" "nice" "-")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is kind.
True
4
proof
[(((((((triple1) -> rule3)) -> rule5)) -> rule2))]
("Erin" "is" "kind" "+")
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is not kind.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule5)) -> rule2))]
("Erin" "is" "kind" "-")
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
@0: Erin is red.[(triple1)] @1: Erin is furry.[(((triple1) -> rule6))] Erin is white.[(((triple1) -> rule3))] @2: Erin is nice.[(((((triple1) -> rule3)) -> rule5))] @3: Erin is kind.[(((((((triple1) -> rule3)) -> rule5)) -> rule2))] @4: Erin is rough.[(((((((((triple1) -> rule3)) -> rule5)) -> rule2) triple1) -> rule1))]
Erin is red.
("Erin" "is" "red" "+")
triple1
Erin is furry.
("Erin" "is" "furry" "+")
((triple1) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple1) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
((((((((triple1) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4