Harry is big. Harry is blue. Harry is not furry. All furry people are not nice. Young people are white. If Harry is not blue then Harry is young. If Harry is big then Harry is not nice. If Harry is big then Harry is white. White people are quiet.
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is not furry.
("Harry" "is" "furry" "-")
All furry people are not nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "-"))
Young people are white.
((("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
If Harry is not blue then Harry is young.
((("Harry" "is" "blue" "~")) -> ("Harry" "is" "young" "+"))
If Harry is big then Harry is not nice.
((("Harry" "is" "big" "+")) -> ("Harry" "is" "nice" "-"))
If Harry is big then Harry is white.
((("Harry" "is" "big" "+")) -> ("Harry" "is" "white" "+"))
White people are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
Harry is big.
True
1
proof
[(triple1)]
("Harry" "is" "big" "+")
triple1
Harry is furry.
False
1
inv-proof
[(triple3)]
("Harry" "is" "furry" "+")
triple3
Harry is not nice.
True
2
proof
[(((triple1) -> rule4))]
("Harry" "is" "nice" "-")
((triple1) -> (rule4 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is not white.
False
2
inv-proof
[(((triple1) -> rule5))]
("Harry" "is" "white" "-")
((triple1) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is quiet.
True
3
proof
[(((((triple1) -> rule5)) -> rule6))]
("Harry" "is" "quiet" "+")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not quiet.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule6))]
("Harry" "is" "quiet" "-")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
@0: Harry is big.[(triple1)] Harry is blue.[(triple2)] Harry is not furry.[(triple3)] @1: Harry is not nice.[(((triple1) -> rule4))] Harry is white.[(((triple1) -> rule5))] @2: Harry is quiet.[(((((triple1) -> rule5)) -> rule6))]
Harry is big.
("Harry" "is" "big" "+")
triple1
Harry is blue.
("Harry" "is" "blue" "+")
triple2
Harry is not furry.
("Harry" "is" "furry" "-")
triple3
Harry is not nice.
("Harry" "is" "nice" "-")
((triple1) -> (rule4 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple1) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2