Harry is green. Harry is red. Harry is white. All smart things are furry. Furry things are nice. Green, nice things are big. Red things are smart. Nice, white things are furry. All big things are smart.
Harry is green.
("Harry" "is" "green" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is white.
("Harry" "is" "white" "+")
All smart things are furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
Furry things are nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
Green, nice things are big.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
Red things are smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
Nice, white things are furry.
((("something" "is" "nice" "+") ("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
All big things are smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
Harry is red.
True
1
proof
[(triple2)]
("Harry" "is" "red" "+")
triple2
Harry is not green.
False
1
inv-proof
[(triple1)]
("Harry" "is" "green" "-")
triple1
Harry is smart.
True
2
proof
[(((triple2) -> rule4))]
("Harry" "is" "smart" "+")
((triple2) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not smart.
False
2
inv-proof
[(((triple2) -> rule4))]
("Harry" "is" "smart" "-")
((triple2) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is furry.
True
3
proof
[(((((triple2) -> rule4)) -> rule1))]
("Harry" "is" "furry" "+")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not furry.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule1))]
("Harry" "is" "furry" "-")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is nice.
True
4
proof
[(((((((triple2) -> rule4)) -> rule1)) -> rule2))]
("Harry" "is" "nice" "+")
((((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is not nice.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule1)) -> rule2))]
("Harry" "is" "nice" "-")
((((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
@0: Harry is green.[(triple1)] Harry is red.[(triple2)] Harry is white.[(triple3)] @1: Harry is smart.[(((triple2) -> rule4))] @2: Harry is furry.[(((((triple2) -> rule4)) -> rule1))] @3: Harry is nice.[(((((((triple2) -> rule4)) -> rule1)) -> rule2))] @4: Harry is big.[(((triple1 ((((((triple2) -> rule4)) -> rule1)) -> rule2)) -> rule3))]
Harry is green.
("Harry" "is" "green" "+")
triple1
Harry is red.
("Harry" "is" "red" "+")
triple2
Harry is white.
("Harry" "is" "white" "+")
triple3
Harry is smart.
("Harry" "is" "smart" "+")
((triple2) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
((triple1 ((((((triple2) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4