Erin is big. Erin is blue. Erin is cold. Erin is furry. Erin is nice. Erin is young. Harry is blue. Harry is cold. Harry is furry. Harry is nice. Harry is red. Harry is young. If Erin is young and Erin is big then Erin is furry. Furry, cold things are red.
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is young.
("Harry" "is" "young" "+")
If Erin is young and Erin is big then Erin is furry.
((("Erin" "is" "young" "+") ("Erin" "is" "big" "+")) -> ("Erin" "is" "furry" "+"))
Furry, cold things are red.
((("something" "is" "furry" "+") ("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
Erin is nice.
True
1
proof
[(triple5)]
("Erin" "is" "nice" "+")
triple5
Erin is not big.
False
1
inv-proof
[(triple1)]
("Erin" "is" "big" "-")
triple1
Erin is red.
True
3
proof
[(((triple4 triple3) -> rule2) OR ((((triple6 triple1) -> rule1) triple3) -> rule2))]
("Erin" "is" "red" "+")
((triple4 triple3) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple6 triple1) -> (rule1 % int2)) triple3) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is not red.
False
3
inv-proof
[(((triple4 triple3) -> rule2) OR ((((triple6 triple1) -> rule1) triple3) -> rule2))]
("Erin" "is" "red" "-")
((triple4 triple3) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple6 triple1) -> (rule1 % int2)) triple3) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
@0: Erin is big.[(triple1)] Erin is blue.[(triple2)] Erin is cold.[(triple3)] Erin is furry.[(triple4 OR ((triple6 triple1) -> rule1))] Erin is nice.[(triple5)] Erin is young.[(triple6)] Harry is blue.[(triple7)] Harry is cold.[(triple8)] Harry is furry.[(triple9)] Harry is nice.[(triple10)] Harry is red.[(triple11 OR ((triple9 triple8) -> rule2))] Harry is young.[(triple12)] @1: Erin is red.[(((triple4 triple3) -> rule2) OR ((((triple6 triple1) -> rule1) triple3) -> rule2))]
Erin is big.
("Erin" "is" "big" "+")
triple1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Erin is furry.
("Erin" "is" "furry" "+")
triple4
((triple6 triple1) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple5
Erin is young.
("Erin" "is" "young" "+")
triple6
Harry is blue.
("Harry" "is" "blue" "+")
triple7
Harry is cold.
("Harry" "is" "cold" "+")
triple8
Harry is furry.
("Harry" "is" "furry" "+")
triple9
Harry is nice.
("Harry" "is" "nice" "+")
triple10
Harry is red.
("Harry" "is" "red" "+")
triple11
((triple9 triple8) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple12
Erin is red.
("Erin" "is" "red" "+")
((triple4 triple3) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple6 triple1) -> (rule1 % int2)) triple3) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2