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