Erin is green. Erin is white. Erin is young. If something is cold then it is smart. White things are cold. If Erin is nice and Erin is white then Erin is cold. If Erin is nice then Erin is cold. All young things are quiet. If something is smart and white then it is nice.
Erin is green.
("Erin" "is" "green" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
If something is cold then it is smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
White things are cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
If Erin is nice and Erin is white then Erin is cold.
((("Erin" "is" "nice" "+") ("Erin" "is" "white" "+")) -> ("Erin" "is" "cold" "+"))
If Erin is nice then Erin is cold.
((("Erin" "is" "nice" "+")) -> ("Erin" "is" "cold" "+"))
All young things are quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
If something is smart and white then it is nice.
((("something" "is" "smart" "+") ("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
Erin is green.
True
1
proof
[(triple1)]
("Erin" "is" "green" "+")
triple1
Erin is not young.
False
1
inv-proof
[(triple3)]
("Erin" "is" "young" "-")
triple3
Erin is cold.
True
2
proof
[(((triple2) -> rule2))]
("Erin" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not cold.
False
2
inv-proof
[(((triple2) -> rule2))]
("Erin" "is" "cold" "-")
((triple2) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is smart.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("Erin" "is" "smart" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is not smart.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Erin" "is" "smart" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is nice.
True
5
proof
[(((((((triple2) -> rule2)) -> rule1) triple2) -> rule6))]
("Erin" "is" "nice" "+")
((((((triple2) -> (rule2 % int3))) -> (rule1 % int2)) triple2) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is not nice.
False
5
inv-proof
[(((((((triple2) -> rule2)) -> rule1) triple2) -> rule6))]
("Erin" "is" "nice" "-")
((((((triple2) -> (rule2 % int3))) -> (rule1 % int2)) triple2) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
@0: Erin is green.[(triple1)] Erin is white.[(triple2)] Erin is young.[(triple3)] @1: Erin is cold.[(((triple2) -> rule2))] Erin is quiet.[(((triple3) -> rule5))] @2: Erin is smart.[(((((triple2) -> rule2)) -> rule1))] @3: Erin is nice.[(((((((triple2) -> rule2)) -> rule1) triple2) -> rule6))]
Erin is green.
("Erin" "is" "green" "+")
triple1
Erin is white.
("Erin" "is" "white" "+")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple3) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((((triple2) -> (rule2 % int3))) -> (rule1 % int2)) triple2) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3