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