Erin is big. Erin is furry. Erin is young. All cold things are red. All big things are nice. If Erin is red then Erin is green. If something is young and furry then it is cold. If Erin is nice and Erin is furry then Erin is big. Cold things are red.
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is young.
("Erin" "is" "young" "+")
All cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
All big things are nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If Erin is red then Erin is green.
((("Erin" "is" "red" "+")) -> ("Erin" "is" "green" "+"))
If something is young and furry then it is cold.
((("something" "is" "young" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
If Erin is nice and Erin is furry then Erin is big.
((("Erin" "is" "nice" "+") ("Erin" "is" "furry" "+")) -> ("Erin" "is" "big" "+"))
Cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
Erin is furry.
True
1
proof
[(triple2)]
("Erin" "is" "furry" "+")
triple2
Erin is not furry.
False
1
inv-proof
[(triple2)]
("Erin" "is" "furry" "-")
triple2
Erin is nice.
True
2
proof
[(((triple1) -> rule2))]
("Erin" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not cold.
False
3
inv-proof
[(((triple3 triple2) -> rule4))]
("Erin" "is" "cold" "-")
((triple3 triple2) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is red.
True
4
proof
[(((((triple3 triple2) -> rule4)) -> rule1) OR ((((triple3 triple2) -> rule4)) -> rule6))]
("Erin" "is" "red" "+")
((((triple3 triple2) -> (rule4 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((triple3 triple2) -> (rule4 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is not red.
False
4
inv-proof
[(((((triple3 triple2) -> rule4)) -> rule1) OR ((((triple3 triple2) -> rule4)) -> rule6))]
("Erin" "is" "red" "-")
((((triple3 triple2) -> (rule4 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((triple3 triple2) -> (rule4 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is green.
True
5
proof
[(((((((triple3 triple2) -> rule4)) -> rule1)) -> rule3) OR ((((((triple3 triple2) -> rule4)) -> rule6)) -> rule3))]
("Erin" "is" "green" "+")
((((((triple3 triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((((triple3 triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is not green.
False
5
inv-proof
[(((((((triple3 triple2) -> rule4)) -> rule1)) -> rule3) OR ((((((triple3 triple2) -> rule4)) -> rule6)) -> rule3))]
("Erin" "is" "green" "-")
((((((triple3 triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((((triple3 triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
@0: Erin is big.[(triple1)] Erin is furry.[(triple2)] Erin is young.[(triple3)] @1: Erin is cold.[(((triple3 triple2) -> rule4))] Erin is nice.[(((triple1) -> rule2))] @2: Erin is red.[(((((triple3 triple2) -> rule4)) -> rule1) OR ((((triple3 triple2) -> rule4)) -> rule6))] @3: Erin is green.[(((((((triple3 triple2) -> rule4)) -> rule1)) -> rule3) OR ((((((triple3 triple2) -> rule4)) -> rule6)) -> rule3))]
Erin is big.
("Erin" "is" "big" "+")
triple1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
((triple3 triple2) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((((triple3 triple2) -> (rule4 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((triple3 triple2) -> (rule4 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
((((((triple3 triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((((triple3 triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3