Erin is furry. If someone is kind then they are blue. If Erin is furry then Erin is nice. All furry people are kind. Young, furry people are quiet. All furry, blue people are quiet. If Erin is red then Erin is quiet. If someone is kind then they are not young. If someone is kind and not young then they are nice.
Erin is furry.
("Erin" "is" "furry" "+")
If someone is kind then they are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If Erin is furry then Erin is nice.
((("Erin" "is" "furry" "+")) -> ("Erin" "is" "nice" "+"))
All furry people are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
Young, furry people are quiet.
((("someone" "is" "young" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
All furry, blue people are quiet.
((("someone" "is" "furry" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
If Erin is red then Erin is quiet.
((("Erin" "is" "red" "+")) -> ("Erin" "is" "quiet" "+"))
If someone is kind then they are not young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "-"))
If someone is kind and not young then they are nice.
((("someone" "is" "kind" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "nice" "+"))
Erin is furry.
True
1
proof
[(triple1)]
("Erin" "is" "furry" "+")
triple1
Erin is not furry.
False
1
inv-proof
[(triple1)]
("Erin" "is" "furry" "-")
triple1
Erin is nice.
True
2
proof
[(((triple1) -> rule2) OR ((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule7)) -> rule8))]
("Erin" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not young.
("Erin" "is" "young" "-")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is not nice.
False
2
inv-proof
[(((triple1) -> rule2) OR ((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule7)) -> rule8))]
("Erin" "is" "nice" "-")
((triple1) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not young.
("Erin" "is" "young" "-")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is not young.
True
3
proof
[(((((triple1) -> rule3)) -> rule7))]
("Erin" "is" "young" "-")
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not blue.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("Erin" "is" "blue" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is quiet.
True
5
proof
[(((triple1 ((((triple1) -> rule3)) -> rule1)) -> rule5))]
("Erin" "is" "quiet" "+")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is not quiet.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule3)) -> rule1)) -> rule5))]
("Erin" "is" "quiet" "-")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
@0: Erin is furry.[(triple1)] @1: Erin is kind.[(((triple1) -> rule3))] Erin is nice.[(((triple1) -> rule2) OR ((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule7)) -> rule8))] @2: Erin is blue.[(((((triple1) -> rule3)) -> rule1))] Erin is not young.[(((((triple1) -> rule3)) -> rule7))] @3: Erin is quiet.[(((triple1 ((((triple1) -> rule3)) -> rule1)) -> rule5))]
Erin is furry.
("Erin" "is" "furry" "+")
triple1
Erin is kind.
("Erin" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not young.
("Erin" "is" "young" "-")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not young.
("Erin" "is" "young" "-")
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3