Harry is cold. Harry is green. Harry is quiet. Harry is red. Harry is round. Harry is smart. Harry is white. If Harry is smart and Harry is white then Harry is quiet. All cold things are smart. If something is red then it is smart. All round, cold things are quiet. If Harry is round and Harry is green then Harry is red. If Harry is white then Harry is quiet.
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If Harry is smart and Harry is white then Harry is quiet.
((("Harry" "is" "smart" "+") ("Harry" "is" "white" "+")) -> ("Harry" "is" "quiet" "+"))
All cold things are smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
If something is red then it is smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
All round, cold things are quiet.
((("something" "is" "round" "+") ("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
If Harry is round and Harry is green then Harry is red.
((("Harry" "is" "round" "+") ("Harry" "is" "green" "+")) -> ("Harry" "is" "red" "+"))
If Harry is white then Harry is quiet.
((("Harry" "is" "white" "+")) -> ("Harry" "is" "quiet" "+"))
Harry is green.
True
1
proof
[(triple2)]
("Harry" "is" "green" "+")
triple2
Harry is not cold.
False
1
inv-proof
[(triple1)]
("Harry" "is" "cold" "-")
triple1
@0: Harry is cold.[(triple1)] Harry is green.[(triple2)] Harry is quiet.[(triple3 OR ((triple7) -> rule6) OR ((triple5 triple1) -> rule4) OR ((triple6 triple7) -> rule1) OR ((((triple1) -> rule2) triple7) -> rule1) OR ((((triple4) -> rule3) triple7) -> rule1) OR ((((((triple5 triple2) -> rule5)) -> rule3) triple7) -> rule1))] Harry is red.[(triple4 OR ((triple5 triple2) -> rule5))] Harry is round.[(triple5)] Harry is smart.[(triple6 OR ((triple1) -> rule2) OR ((triple4) -> rule3) OR ((((triple5 triple2) -> rule5)) -> rule3))] Harry is white.[(triple7)]
Harry is cold.
("Harry" "is" "cold" "+")
triple1
Harry is green.
("Harry" "is" "green" "+")
triple2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple3
((triple7) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple5 triple1) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple6 triple7) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple1) -> (rule2 % int2)) triple7) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((triple4) -> (rule3 % int2)) triple7) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((((triple5 triple2) -> (rule5 % int3))) -> (rule3 % int2)) triple7) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
triple4
((triple5 triple2) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple5
Harry is smart.
("Harry" "is" "smart" "+")
triple6
((triple1) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((triple4) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple5 triple2) -> (rule5 % int2))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
triple7