Erin is blue. Erin is cold. Erin is furry. Erin is nice. Erin is quiet. Erin is white. Harry is big. Harry is furry. Harry is quiet. Harry is white. Cold, nice things are blue. If something is furry then it is cold. Furry, quiet things are nice.
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 quiet.
("Erin" "is" "quiet" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is white.
("Harry" "is" "white" "+")
Cold, nice things are blue.
((("something" "is" "cold" "+") ("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
If something is furry then it is cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
Furry, quiet things are nice.
((("something" "is" "furry" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
Harry is furry.
True
1
proof
[(triple8)]
("Harry" "is" "furry" "+")
triple8
Erin is not nice.
False
1
inv-proof
[(triple4 OR ((triple3 triple5) -> rule3))]
("Erin" "is" "nice" "-")
triple4
((triple3 triple5) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Harry is nice.
True
3
proof
[(((triple8 triple9) -> rule3))]
("Harry" "is" "nice" "+")
((triple8 triple9) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple8) -> rule2))]
("Harry" "is" "cold" "-")
((triple8) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is blue.
True
6
proof
[(((((triple8) -> rule2) ((triple8 triple9) -> rule3)) -> rule1))]
("Harry" "is" "blue" "+")
((((triple8) -> (rule2 % int3)) ((triple8 triple9) -> (rule3 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not blue.
False
6
inv-proof
[(((((triple8) -> rule2) ((triple8 triple9) -> rule3)) -> rule1))]
("Harry" "is" "blue" "-")
((((triple8) -> (rule2 % int3)) ((triple8 triple9) -> (rule3 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
@0: Erin is blue.[(triple1 OR ((triple2 triple4) -> rule1) OR ((triple2 ((triple3 triple5) -> rule3)) -> rule1) OR ((((triple3) -> rule2) triple4) -> rule1) OR ((((triple3) -> rule2) ((triple3 triple5) -> rule3)) -> rule1))] Erin is cold.[(triple2 OR ((triple3) -> rule2))] Erin is furry.[(triple3)] Erin is nice.[(triple4 OR ((triple3 triple5) -> rule3))] Erin is quiet.[(triple5)] Erin is white.[(triple6)] Harry is big.[(triple7)] Harry is furry.[(triple8)] Harry is quiet.[(triple9)] Harry is white.[(triple10)] @1: Harry is cold.[(((triple8) -> rule2))] Harry is nice.[(((triple8 triple9) -> rule3))] @2: Harry is blue.[(((((triple8) -> rule2) ((triple8 triple9) -> rule3)) -> rule1))]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
((triple2 triple4) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple2 ((triple3 triple5) -> (rule3 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple3) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((triple3) -> (rule2 % int3)) ((triple3 triple5) -> (rule3 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
triple2
((triple3) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
triple4
((triple3 triple5) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
Erin is white.
("Erin" "is" "white" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
Harry is furry.
("Harry" "is" "furry" "+")
triple8
Harry is quiet.
("Harry" "is" "quiet" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
Harry is cold.
("Harry" "is" "cold" "+")
((triple8) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple8 triple9) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((((triple8) -> (rule2 % int3)) ((triple8 triple9) -> (rule3 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3