Harry is big. Harry is kind. Harry is young. If Harry is furry then Harry is not blue. All young people are white. All white people are furry.
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is furry then Harry is not blue.
((("Harry" "is" "furry" "+")) -> ("Harry" "is" "blue" "-"))
All young people are white.
((("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
All white people are furry.
((("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
Harry is big.
True
1
proof
[(triple1)]
("Harry" "is" "big" "+")
triple1
Harry is not young.
False
1
inv-proof
[(triple3)]
("Harry" "is" "young" "-")
triple3
Harry is white.
True
2
proof
[(((triple3) -> rule2))]
("Harry" "is" "white" "+")
((triple3) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple3) -> rule2))]
("Harry" "is" "white" "-")
((triple3) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("Harry" "is" "furry" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not furry.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("Harry" "is" "furry" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not blue.
True
4
proof
[(((((((triple3) -> rule2)) -> rule3)) -> rule1))]
("Harry" "is" "blue" "-")
((((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is blue.
False
4
inv-proof
[(((((((triple3) -> rule2)) -> rule3)) -> rule1))]
("Harry" "is" "blue" "+")
((((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
@0: Harry is big.[(triple1)] Harry is kind.[(triple2)] Harry is young.[(triple3)] @1: Harry is white.[(((triple3) -> rule2))] @2: Harry is furry.[(((((triple3) -> rule2)) -> rule3))] @3: Harry is not blue.[(((((((triple3) -> rule2)) -> rule3)) -> rule1))]
Harry is big.
("Harry" "is" "big" "+")
triple1
Harry is kind.
("Harry" "is" "kind" "+")
triple2
Harry is young.
("Harry" "is" "young" "+")
triple3
Harry is white.
("Harry" "is" "white" "+")
((triple3) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not blue.
("Harry" "is" "blue" "-")
((((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3