Harry is blue. Harry is furry. Harry is green. If something is furry then it is nice. If something is green then it is blue. If something is nice and furry then it is cold. If something is green then it is red. All green, furry things are nice. All young, red things are cold. Red, green things are blue. If Harry is red then Harry is nice.
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
If something is furry then it is nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
If something is green then it is blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
If something is nice and furry then it is cold.
((("something" "is" "nice" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
If something is green then it is red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
All green, furry things are nice.
((("something" "is" "green" "+") ("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
All young, red things are cold.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
Red, green things are blue.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
If Harry is red then Harry is nice.
((("Harry" "is" "red" "+")) -> ("Harry" "is" "nice" "+"))
Harry is furry.
True
1
proof
[(triple2)]
("Harry" "is" "furry" "+")
triple2
Harry is not blue.
False
1
inv-proof
[(triple1 OR ((triple3) -> rule2) OR ((((triple3) -> rule4) triple3) -> rule7))]
("Harry" "is" "blue" "-")
triple1
((triple3) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple3) -> (rule4 % int2)) triple3) -> (rule7 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is nice.
True
2
proof
[(((triple2) -> rule1) OR ((triple3 triple2) -> rule5) OR ((((triple3) -> rule4)) -> rule8))]
("Harry" "is" "nice" "+")
((triple2) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple3 triple2) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not red.
False
2
inv-proof
[(((triple3) -> rule4))]
("Harry" "is" "red" "-")
((triple3) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is cold.
True
4
proof
[(((((triple2) -> rule1) triple2) -> rule3) OR ((((triple3 triple2) -> rule5) triple2) -> rule3) OR ((((((triple3) -> rule4)) -> rule8) triple2) -> rule3))]
("Harry" "is" "cold" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple3 triple2) -> (rule5 % int2)) triple2) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((((triple3) -> (rule4 % int3))) -> (rule8 % int2)) triple2) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is not cold.
False
4
inv-proof
[(((((triple2) -> rule1) triple2) -> rule3) OR ((((triple3 triple2) -> rule5) triple2) -> rule3) OR ((((((triple3) -> rule4)) -> rule8) triple2) -> rule3))]
("Harry" "is" "cold" "-")
((((triple2) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple3 triple2) -> (rule5 % int2)) triple2) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((((triple3) -> (rule4 % int3))) -> (rule8 % int2)) triple2) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
@0: Harry is blue.[(triple1 OR ((triple3) -> rule2) OR ((((triple3) -> rule4) triple3) -> rule7))] Harry is furry.[(triple2)] Harry is green.[(triple3)] @1: Harry is nice.[(((triple2) -> rule1) OR ((triple3 triple2) -> rule5) OR ((((triple3) -> rule4)) -> rule8))] Harry is red.[(((triple3) -> rule4))] @2: Harry is cold.[(((((triple2) -> rule1) triple2) -> rule3) OR ((((triple3 triple2) -> rule5) triple2) -> rule3) OR ((((((triple3) -> rule4)) -> rule8) triple2) -> rule3))]
Harry is blue.
("Harry" "is" "blue" "+")
triple1
((triple3) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple3) -> (rule4 % int2)) triple3) -> (rule7 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
triple2
Harry is green.
("Harry" "is" "green" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
((triple2) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple3 triple2) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((triple3) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple3 triple2) -> (rule5 % int2)) triple2) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((((triple3) -> (rule4 % int3))) -> (rule8 % int2)) triple2) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3