Harry is not blue. Harry is furry. Harry is not green. Harry is nice. Harry is not quiet. Harry is white. Harry is young. White people are furry. If someone is furry then they are nice. All furry people are young. If someone is furry and not quiet then they are young. If someone is quiet and furry then they are blue. If someone is quiet then they are not blue.
Harry is not blue.
("Harry" "is" "blue" "-")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is not green.
("Harry" "is" "green" "-")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is not quiet.
("Harry" "is" "quiet" "-")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
White people are furry.
((("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
If someone is furry then they are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
All furry people are young.
((("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
If someone is furry and not quiet then they are young.
((("someone" "is" "furry" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "young" "+"))
If someone is quiet and furry then they are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
If someone is quiet then they are not blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "-"))
Harry is young.
True
1
proof
[(triple7 OR ((triple2) -> rule3) OR ((triple2 triple5) -> rule4) OR ((((triple6) -> rule1)) -> rule3) OR ((((triple6) -> rule1) triple5) -> rule4))]
("Harry" "is" "young" "+")
triple7
((triple2) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple2 triple5) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((triple6) -> (rule1 % int2)) triple5) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not furry.
False
1
inv-proof
[(triple2 OR ((triple6) -> rule1))]
("Harry" "is" "furry" "-")
triple2
((triple6) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
@0: Harry is furry.[(triple2 OR ((triple6) -> rule1))] Harry is nice.[(triple4 OR ((triple2) -> rule2) OR ((((triple6) -> rule1)) -> rule2))] Harry is not blue.[(triple1)] Harry is not green.[(triple3)] Harry is not quiet.[(triple5)] Harry is white.[(triple6)] Harry is young.[(triple7 OR ((triple2) -> rule3) OR ((triple2 triple5) -> rule4) OR ((((triple6) -> rule1)) -> rule3) OR ((((triple6) -> rule1) triple5) -> rule4))]
Harry is furry.
("Harry" "is" "furry" "+")
triple2
((triple6) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple4
((triple2) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not blue.
("Harry" "is" "blue" "-")
triple1
Harry is not green.
("Harry" "is" "green" "-")
triple3
Harry is not quiet.
("Harry" "is" "quiet" "-")
triple5
Harry is white.
("Harry" "is" "white" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
((triple2) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple2 triple5) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((triple6) -> (rule1 % int2)) triple5) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2