Erin is red. Erin is rough. Erin is not white. If Erin is blue and Erin is quiet then Erin is rough. If Erin is rough then Erin is furry. All quiet people are blue. All rough, furry people are not white. If Erin is red then Erin is not white. Rough, furry people are quiet.
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is not white.
("Erin" "is" "white" "-")
If Erin is blue and Erin is quiet then Erin is rough.
((("Erin" "is" "blue" "+") ("Erin" "is" "quiet" "+")) -> ("Erin" "is" "rough" "+"))
If Erin is rough then Erin is furry.
((("Erin" "is" "rough" "+")) -> ("Erin" "is" "furry" "+"))
All quiet people are blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
All rough, furry people are not white.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "white" "-"))
If Erin is red then Erin is not white.
((("Erin" "is" "red" "+")) -> ("Erin" "is" "white" "-"))
Rough, furry people are quiet.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
Erin is rough.
True
1
proof
[(triple2)]
("Erin" "is" "rough" "+")
triple2
Erin is white.
False
1
inv-proof
[(triple3 OR ((triple1) -> rule5) OR ((triple2 ((triple2) -> rule2)) -> rule4))]
("Erin" "is" "white" "+")
triple3
((triple1) -> (rule5 % int1))
Erin is not white.
("Erin" "is" "white" "-")
int1
((triple2 ((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Erin is not white.
("Erin" "is" "white" "-")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is furry.
True
2
proof
[(((triple2) -> rule2))]
("Erin" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is not furry.
False
2
inv-proof
[(((triple2) -> rule2))]
("Erin" "is" "furry" "-")
((triple2) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is quiet.
True
4
proof
[(((triple2 ((triple2) -> rule2)) -> rule6))]
("Erin" "is" "quiet" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is not quiet.
False
4
inv-proof
[(((triple2 ((triple2) -> rule2)) -> rule6))]
("Erin" "is" "quiet" "-")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is blue.
True
5
proof
[(((((triple2 ((triple2) -> rule2)) -> rule6)) -> rule3))]
("Erin" "is" "blue" "+")
((((triple2 ((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is not blue.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule2)) -> rule6)) -> rule3))]
("Erin" "is" "blue" "-")
((((triple2 ((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
@0: Erin is not white.[(triple3 OR ((triple1) -> rule5) OR ((triple2 ((triple2) -> rule2)) -> rule4))] Erin is red.[(triple1)] Erin is rough.[(triple2)] @1: Erin is furry.[(((triple2) -> rule2))] @2: Erin is quiet.[(((triple2 ((triple2) -> rule2)) -> rule6))] @3: Erin is blue.[(((((triple2 ((triple2) -> rule2)) -> rule6)) -> rule3))]
Erin is not white.
("Erin" "is" "white" "-")
triple3
((triple1) -> (rule5 % int1))
Erin is not white.
("Erin" "is" "white" "-")
int1
((triple2 ((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Erin is not white.
("Erin" "is" "white" "-")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
triple1
Erin is rough.
("Erin" "is" "rough" "+")
triple2
Erin is furry.
("Erin" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
((((triple2 ((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3