Erin is cold. Cold things are smart. Nice things are cold. Nice things are big. All nice, blue things are cold. All nice, cold things are furry. Blue, cold things are big. If something is blue and big then it is nice. If something is smart then it is blue.
Erin is cold.
("Erin" "is" "cold" "+")
Cold things are smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
Nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
Nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
All nice, blue things are cold.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
All nice, cold things are furry.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
Blue, cold things are big.
((("something" "is" "blue" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If something is blue and big then it is nice.
((("something" "is" "blue" "+") ("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If something is smart then it is blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
Erin is cold.
True
1
proof
[(triple1)]
("Erin" "is" "cold" "+")
triple1
Erin is not cold.
False
1
inv-proof
[(triple1)]
("Erin" "is" "cold" "-")
triple1
Erin is smart.
True
2
proof
[(((triple1) -> rule1))]
("Erin" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not smart.
False
2
inv-proof
[(((triple1) -> rule1))]
("Erin" "is" "smart" "-")
((triple1) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
True
3
proof
[(((((triple1) -> rule1)) -> rule8))]
("Erin" "is" "blue" "+")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not blue.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule8))]
("Erin" "is" "blue" "-")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is big.
True
5
proof
[(((((((triple1) -> rule1)) -> rule8) triple1) -> rule6))]
("Erin" "is" "big" "+")
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is not big.
False
5
inv-proof
[(((((((triple1) -> rule1)) -> rule8) triple1) -> rule6))]
("Erin" "is" "big" "-")
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
@0: Erin is cold.[(triple1)] @1: Erin is smart.[(((triple1) -> rule1))] @2: Erin is blue.[(((((triple1) -> rule1)) -> rule8))] @3: Erin is big.[(((((((triple1) -> rule1)) -> rule8) triple1) -> rule6))] @4: Erin is nice.[(((((((triple1) -> rule1)) -> rule8) ((((((triple1) -> rule1)) -> rule8) triple1) -> rule6)) -> rule7))] @5: Erin is furry.[(((((((((triple1) -> rule1)) -> rule8) ((((((triple1) -> rule1)) -> rule8) triple1) -> rule6)) -> rule7) triple1) -> rule5))]
Erin is cold.
("Erin" "is" "cold" "+")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
((((((triple1) -> (rule1 % int4))) -> (rule8 % int3)) ((((((triple1) -> (rule1 % int4))) -> (rule8 % int3)) triple1) -> (rule6 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is furry.
("Erin" "is" "furry" "+")
((((((((triple1) -> (rule1 % int5))) -> (rule8 % int4)) ((((((triple1) -> (rule1 % int5))) -> (rule8 % int4)) triple1) -> (rule6 % int3))) -> (rule7 % int2)) triple1) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
int5