Harry is not blue. Harry is furry. Harry is nice. Harry is quiet. Harry is rough. Harry is not round. Harry is smart. All smart things are quiet. Blue things are smart. If Harry is blue and Harry is nice then Harry is smart. If Harry is furry then Harry is not blue. All rough things are not blue. All round things are nice.
Harry is not blue.
("Harry" "is" "blue" "-")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is not round.
("Harry" "is" "round" "-")
Harry is smart.
("Harry" "is" "smart" "+")
All smart things are quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
Blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
If Harry is blue and Harry is nice then Harry is smart.
((("Harry" "is" "blue" "+") ("Harry" "is" "nice" "+")) -> ("Harry" "is" "smart" "+"))
If Harry is furry then Harry is not blue.
((("Harry" "is" "furry" "+")) -> ("Harry" "is" "blue" "-"))
All rough things are not blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "-"))
All round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
Harry is not round.
True
1
proof
[(triple6)]
("Harry" "is" "round" "-")
triple6
Harry is blue.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule4) OR ((triple5) -> rule5))]
("Harry" "is" "blue" "+")
triple1
((triple2) -> (rule4 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
((triple5) -> (rule5 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
@0: Harry is furry.[(triple2)] Harry is nice.[(triple3)] Harry is not blue.[(triple1 OR ((triple2) -> rule4) OR ((triple5) -> rule5))] Harry is not round.[(triple6)] Harry is quiet.[(triple4 OR ((triple7) -> rule1))] Harry is rough.[(triple5)] Harry is smart.[(triple7)]
Harry is furry.
("Harry" "is" "furry" "+")
triple2
Harry is nice.
("Harry" "is" "nice" "+")
triple3
Harry is not blue.
("Harry" "is" "blue" "-")
triple1
((triple2) -> (rule4 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
((triple5) -> (rule5 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is not round.
("Harry" "is" "round" "-")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
((triple7) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple5
Harry is smart.
("Harry" "is" "smart" "+")
triple7