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