Harry is big. Harry is furry. Harry is green. Harry is kind. Harry is quiet. Harry is round. Harry is white. All round, kind things are quiet. If something is big and green then it is white. Green things are quiet.
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
All round, kind things are quiet.
((("something" "is" "round" "+") ("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
If something is big and green then it is white.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
Green things are quiet.
((("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
Harry is green.
True
1
proof
[(triple3)]
("Harry" "is" "green" "+")
triple3
Harry is not quiet.
False
1
inv-proof
[(triple5 OR ((triple3) -> rule3) OR ((triple6 triple4) -> rule1))]
("Harry" "is" "quiet" "-")
triple5
((triple3) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple6 triple4) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
@0: Harry is big.[(triple1)] Harry is furry.[(triple2)] Harry is green.[(triple3)] Harry is kind.[(triple4)] Harry is quiet.[(triple5 OR ((triple3) -> rule3) OR ((triple6 triple4) -> rule1))] Harry is round.[(triple6)] Harry is white.[(triple7 OR ((triple1 triple3) -> rule2))]
Harry is big.
("Harry" "is" "big" "+")
triple1
Harry is furry.
("Harry" "is" "furry" "+")
triple2
Harry is green.
("Harry" "is" "green" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Harry is quiet.
("Harry" "is" "quiet" "+")
triple5
((triple3) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple6 triple4) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
((triple1 triple3) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1