Erin is cold. Erin is quiet. Erin is young. If someone is blue then they are kind. All young, smart people are white. If someone is smart then they are quiet. If Erin is smart then Erin is young. If Erin is cold then Erin is white. If Erin is cold then Erin is quiet. If Erin is cold then Erin is young. If Erin is cold then Erin is blue.
Erin is cold.
("Erin" "is" "cold" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is young.
("Erin" "is" "young" "+")
If someone is blue then they are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
All young, smart people are white.
((("someone" "is" "young" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
If someone is smart then they are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
If Erin is smart then Erin is young.
((("Erin" "is" "smart" "+")) -> ("Erin" "is" "young" "+"))
If Erin is cold then Erin is white.
((("Erin" "is" "cold" "+")) -> ("Erin" "is" "white" "+"))
If Erin is cold then Erin is quiet.
((("Erin" "is" "cold" "+")) -> ("Erin" "is" "quiet" "+"))
If Erin is cold then Erin is young.
((("Erin" "is" "cold" "+")) -> ("Erin" "is" "young" "+"))
If Erin is cold then Erin is blue.
((("Erin" "is" "cold" "+")) -> ("Erin" "is" "blue" "+"))
Erin is young.
True
1
proof
[(triple3 OR ((triple1) -> rule7))]
("Erin" "is" "young" "+")
triple3
((triple1) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not quiet.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule6))]
("Erin" "is" "quiet" "-")
triple2
((triple1) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
True
2
proof
[(((triple1) -> rule5))]
("Erin" "is" "white" "+")
((triple1) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is not blue.
False
2
inv-proof
[(((triple1) -> rule8))]
("Erin" "is" "blue" "-")
((triple1) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
True
3
proof
[(((((triple1) -> rule8)) -> rule1))]
("Erin" "is" "kind" "+")
((((triple1) -> (rule8 % int2))) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not kind.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule1))]
("Erin" "is" "kind" "-")
((((triple1) -> (rule8 % int2))) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
@0: Erin is cold.[(triple1)] Erin is quiet.[(triple2 OR ((triple1) -> rule6))] Erin is young.[(triple3 OR ((triple1) -> rule7))] @1: Erin is blue.[(((triple1) -> rule8))] Erin is white.[(((triple1) -> rule5))] @2: Erin is kind.[(((((triple1) -> rule8)) -> rule1))]
Erin is cold.
("Erin" "is" "cold" "+")
triple1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple2
((triple1) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple3
((triple1) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple1) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple1) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((((triple1) -> (rule8 % int2))) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2