Harry is cold. Harry is furry. Harry is kind. Harry is nice. Harry is quiet. Harry is not rough. Harry is round. If something is round then it is quiet. Rough things are round. If something is kind then it is nice. Round things are kind. If something is nice and not round then it is kind. If something is kind and not nice then it is not furry.
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
Harry is round.
("Harry" "is" "round" "+")
If something is round then it is quiet.
((("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
Rough things are round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If something is kind then it is nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
Round things are kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
If something is nice and not round then it is kind.
((("something" "is" "nice" "+") ("something" "is" "round" "~")) -> ("something" "is" "kind" "+"))
If something is kind and not nice then it is not furry.
((("something" "is" "kind" "+") ("something" "is" "nice" "~")) -> ("something" "is" "furry" "-"))
Harry is not rough.
True
1
proof
[(triple6)]
("Harry" "is" "rough" "-")
triple6
Harry is not cold.
False
1
inv-proof
[(triple1)]
("Harry" "is" "cold" "-")
triple1
@0: Harry is cold.[(triple1)] Harry is furry.[(triple2)] Harry is kind.[(triple3 OR ((triple7) -> rule4))] Harry is nice.[(triple4 OR ((triple3) -> rule3) OR ((((triple7) -> rule4)) -> rule3))] Harry is not rough.[(triple6)] Harry is quiet.[(triple5 OR ((triple7) -> rule1))] Harry is round.[(triple7)]
Harry is cold.
("Harry" "is" "cold" "+")
triple1
Harry is furry.
("Harry" "is" "furry" "+")
triple2
Harry is kind.
("Harry" "is" "kind" "+")
triple3
((triple7) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple4
((triple3) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple7) -> (rule4 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not rough.
("Harry" "is" "rough" "-")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple5
((triple7) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple7