Harry is green. Harry is red. Harry is smart. If something is round then it is not red. If something is young and rough then it is red. All smart things are nice. Nice, smart things are rough. If something is rough then it is not round. If Harry is not green and Harry is not smart then Harry is not round.
Harry is green.
("Harry" "is" "green" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is round then it is not red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "-"))
If something is young and rough then it is red.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
All smart things are nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
Nice, smart things are rough.
((("something" "is" "nice" "+") ("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If something is rough then it is not round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "-"))
If Harry is not green and Harry is not smart then Harry is not round.
((("Harry" "is" "green" "~") ("Harry" "is" "smart" "~")) -> ("Harry" "is" "round" "-"))
Harry is red.
True
1
proof
[(triple2)]
("Harry" "is" "red" "+")
triple2
Harry is not smart.
False
1
inv-proof
[(triple3)]
("Harry" "is" "smart" "-")
triple3
Harry is nice.
True
2
proof
[(((triple3) -> rule3))]
("Harry" "is" "nice" "+")
((triple3) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not nice.
False
2
inv-proof
[(((triple3) -> rule3))]
("Harry" "is" "nice" "-")
((triple3) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
True
4
proof
[(((((triple3) -> rule3) triple3) -> rule4))]
("Harry" "is" "rough" "+")
((((triple3) -> (rule3 % int2)) triple3) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not rough.
False
4
inv-proof
[(((((triple3) -> rule3) triple3) -> rule4))]
("Harry" "is" "rough" "-")
((((triple3) -> (rule3 % int2)) triple3) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not round.
True
5
proof
[(((((((triple3) -> rule3) triple3) -> rule4)) -> rule5))]
("Harry" "is" "round" "-")
((((((triple3) -> (rule3 % int3)) triple3) -> (rule4 % int2))) -> (rule5 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is round.
False
5
inv-proof
[(((((((triple3) -> rule3) triple3) -> rule4)) -> rule5))]
("Harry" "is" "round" "+")
((((((triple3) -> (rule3 % int3)) triple3) -> (rule4 % int2))) -> (rule5 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
@0: Harry is green.[(triple1)] Harry is red.[(triple2)] Harry is smart.[(triple3)] @1: Harry is nice.[(((triple3) -> rule3))] @2: Harry is rough.[(((((triple3) -> rule3) triple3) -> rule4))] @3: Harry is not round.[(((((((triple3) -> rule3) triple3) -> rule4)) -> rule5))]
Harry is green.
("Harry" "is" "green" "+")
triple1
Harry is red.
("Harry" "is" "red" "+")
triple2
Harry is smart.
("Harry" "is" "smart" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
((triple3) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((((triple3) -> (rule3 % int2)) triple3) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not round.
("Harry" "is" "round" "-")
((((((triple3) -> (rule3 % int3)) triple3) -> (rule4 % int2))) -> (rule5 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3