Harry is big. Harry is red. Harry is smart. All quiet, nice things are big. Smart things are quiet. Cold, big things are green. If Harry is green and Harry is nice then Harry is cold. Nice things are red. Red things are cold. If Harry is cold then Harry is red. If something is nice then it is big.
Harry is big.
("Harry" "is" "big" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All quiet, nice things are big.
((("something" "is" "quiet" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
Smart things are quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
Cold, big things are green.
((("something" "is" "cold" "+") ("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If Harry is green and Harry is nice then Harry is cold.
((("Harry" "is" "green" "+") ("Harry" "is" "nice" "+")) -> ("Harry" "is" "cold" "+"))
Nice things are red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
Red things are cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If Harry is cold then Harry is red.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "red" "+"))
If something is nice then it is big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
Harry is big.
True
1
proof
[(triple1)]
("Harry" "is" "big" "+")
triple1
Harry is not smart.
False
1
inv-proof
[(triple3)]
("Harry" "is" "smart" "-")
triple3
Harry is quiet.
True
2
proof
[(((triple3) -> rule2))]
("Harry" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple2) -> rule6))]
("Harry" "is" "cold" "-")
((triple2) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
True
4
proof
[(((((triple2) -> rule6) triple1) -> rule3))]
("Harry" "is" "green" "+")
((((triple2) -> (rule6 % int2)) triple1) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not green.
False
4
inv-proof
[(((((triple2) -> rule6) triple1) -> rule3))]
("Harry" "is" "green" "-")
((((triple2) -> (rule6 % int2)) triple1) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
@0: Harry is big.[(triple1)] Harry is red.[(triple2)] Harry is smart.[(triple3)] @1: Harry is cold.[(((triple2) -> rule6))] Harry is quiet.[(((triple3) -> rule2))] @2: Harry is green.[(((((triple2) -> rule6) triple1) -> rule3))]
Harry is big.
("Harry" "is" "big" "+")
triple1
Harry is red.
("Harry" "is" "red" "+")
triple2
Harry is smart.
("Harry" "is" "smart" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
((triple2) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((((triple2) -> (rule6 % int2)) triple1) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2