Harry is green. Harry is red. Harry is round. If Harry is white and Harry is round then Harry is big. Cold things are green. If something is cold and round then it is white. Big things are red. Red things are cold. If Harry is red and Harry is nice then Harry is green.
Harry is green.
("Harry" "is" "green" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
If Harry is white and Harry is round then Harry is big.
((("Harry" "is" "white" "+") ("Harry" "is" "round" "+")) -> ("Harry" "is" "big" "+"))
Cold things are green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
If something is cold and round then it is white.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
Big things are red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
Red things are cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If Harry is red and Harry is nice then Harry is green.
((("Harry" "is" "red" "+") ("Harry" "is" "nice" "+")) -> ("Harry" "is" "green" "+"))
Harry is green.
True
1
proof
[(triple1 OR ((((triple2) -> rule5)) -> rule2))]
("Harry" "is" "green" "+")
triple1
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not red.
False
1
inv-proof
[(triple2)]
("Harry" "is" "red" "-")
triple2
Harry is cold.
True
2
proof
[(((triple2) -> rule5))]
("Harry" "is" "cold" "+")
((triple2) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple2) -> rule5))]
("Harry" "is" "cold" "-")
((triple2) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
True
4
proof
[(((((triple2) -> rule5) triple3) -> rule3))]
("Harry" "is" "white" "+")
((((triple2) -> (rule5 % int2)) triple3) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not white.
False
4
inv-proof
[(((((triple2) -> rule5) triple3) -> rule3))]
("Harry" "is" "white" "-")
((((triple2) -> (rule5 % int2)) triple3) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is big.
True
6
proof
[(((((((triple2) -> rule5) triple3) -> rule3) triple3) -> rule1))]
("Harry" "is" "big" "+")
((((((triple2) -> (rule5 % int3)) triple3) -> (rule3 % int2)) triple3) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not big.
False
6
inv-proof
[(((((((triple2) -> rule5) triple3) -> rule3) triple3) -> rule1))]
("Harry" "is" "big" "-")
((((((triple2) -> (rule5 % int3)) triple3) -> (rule3 % int2)) triple3) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
@0: Harry is green.[(triple1 OR ((((triple2) -> rule5)) -> rule2))] Harry is red.[(triple2)] Harry is round.[(triple3)] @1: Harry is cold.[(((triple2) -> rule5))] @2: Harry is white.[(((((triple2) -> rule5) triple3) -> rule3))] @3: Harry is big.[(((((((triple2) -> rule5) triple3) -> rule3) triple3) -> rule1))]
Harry is green.
("Harry" "is" "green" "+")
triple1
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
triple2
Harry is round.
("Harry" "is" "round" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
((triple2) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((((triple2) -> (rule5 % int2)) triple3) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((((((triple2) -> (rule5 % int3)) triple3) -> (rule3 % int2)) triple3) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3