Erin is furry. All smart, cold things are blue. All big things are cold. All cold things are big. Blue things are young. All cold things are big. All smart things are big. Young things are blue. Furry things are smart.
Erin is furry.
("Erin" "is" "furry" "+")
All smart, cold things are blue.
((("something" "is" "smart" "+") ("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
All big things are cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
All cold things are big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
Blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
All cold things are big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
All smart things are big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
Young things are blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
Furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
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 smart.
True
2
proof
[(((triple1) -> rule8))]
("Erin" "is" "smart" "+")
((triple1) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not smart.
False
2
inv-proof
[(((triple1) -> rule8))]
("Erin" "is" "smart" "-")
((triple1) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
True
3
proof
[(((((triple1) -> rule8)) -> rule6))]
("Erin" "is" "big" "+")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not big.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule6))]
("Erin" "is" "big" "-")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
True
4
proof
[(((((((triple1) -> rule8)) -> rule6)) -> rule2))]
("Erin" "is" "cold" "+")
((((((triple1) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is not cold.
False
4
inv-proof
[(((((((triple1) -> rule8)) -> rule6)) -> rule2))]
("Erin" "is" "cold" "-")
((((((triple1) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
@0: Erin is furry.[(triple1)] @1: Erin is smart.[(((triple1) -> rule8))] @2: Erin is big.[(((((triple1) -> rule8)) -> rule6))] @3: Erin is cold.[(((((((triple1) -> rule8)) -> rule6)) -> rule2))] @4: Erin is blue.[(((((triple1) -> rule8) ((((((triple1) -> rule8)) -> rule6)) -> rule2)) -> rule1))] @5: Erin is young.[(((((((triple1) -> rule8) ((((((triple1) -> rule8)) -> rule6)) -> rule2)) -> rule1)) -> rule4))]
Erin is furry.
("Erin" "is" "furry" "+")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
((triple1) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((((((triple1) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
((((triple1) -> (rule8 % int4)) ((((((triple1) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is young.
("Erin" "is" "young" "+")
((((((triple1) -> (rule8 % int5)) ((((((triple1) -> (rule8 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
int5