Harry is smart. If someone is young and not kind then they are quiet. All kind people are quiet. If someone is smart then they are green. If someone is quiet and not kind then they are green. If Harry is round then Harry is quiet. All furry, green people are young. If someone is quiet and smart then they are furry. All green people are round.
Harry is smart.
("Harry" "is" "smart" "+")
If someone is young and not kind then they are quiet.
((("someone" "is" "young" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "quiet" "+"))
All kind people are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
If someone is smart then they are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
If someone is quiet and not kind then they are green.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "green" "+"))
If Harry is round then Harry is quiet.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "quiet" "+"))
All furry, green people are young.
((("someone" "is" "furry" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If someone is quiet and smart then they are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
All green people are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
Harry is smart.
True
1
proof
[(triple1)]
("Harry" "is" "smart" "+")
triple1
Harry is not smart.
False
1
inv-proof
[(triple1)]
("Harry" "is" "smart" "-")
triple1
Harry is green.
True
2
proof
[(((triple1) -> rule3))]
("Harry" "is" "green" "+")
((triple1) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple1) -> rule3))]
("Harry" "is" "green" "-")
((triple1) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is round.
True
3
proof
[(((((triple1) -> rule3)) -> rule8))]
("Harry" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is not round.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule8))]
("Harry" "is" "round" "-")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is quiet.
True
4
proof
[(((((((triple1) -> rule3)) -> rule8)) -> rule5))]
("Harry" "is" "quiet" "+")
((((((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is not quiet.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule8)) -> rule5))]
("Harry" "is" "quiet" "-")
((((((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
@0: Harry is smart.[(triple1)] @1: Harry is green.[(((triple1) -> rule3))] @2: Harry is round.[(((((triple1) -> rule3)) -> rule8))] @3: Harry is quiet.[(((((((triple1) -> rule3)) -> rule8)) -> rule5))] @4: Harry is furry.[(((((((((triple1) -> rule3)) -> rule8)) -> rule5) triple1) -> rule7))] @5: Harry is young.[(((((((((((triple1) -> rule3)) -> rule8)) -> rule5) triple1) -> rule7) ((triple1) -> rule3)) -> rule6))]
Harry is smart.
("Harry" "is" "smart" "+")
triple1
Harry is green.
("Harry" "is" "green" "+")
((triple1) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((((((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
((((((((triple1) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule5 % int2)) triple1) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is young.
("Harry" "is" "young" "+")
((((((((((triple1) -> (rule3 % int5))) -> (rule8 % int4))) -> (rule5 % int3)) triple1) -> (rule7 % int2)) ((triple1) -> (rule3 % int5))) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
Harry is green.
("Harry" "is" "green" "+")
int5