Harry is nice. All green things are round. Smart things are green. If something is rough and furry then it is smart. If Harry is nice then Harry is furry. Rough, round things are green. Furry things are smart. If something is rough then it is furry. Furry things are rough.
Harry is nice.
("Harry" "is" "nice" "+")
All green things are round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
Smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If something is rough and furry then it is smart.
((("something" "is" "rough" "+") ("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If Harry is nice then Harry is furry.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "furry" "+"))
Rough, round things are green.
((("something" "is" "rough" "+") ("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
Furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If something is rough then it is furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
Furry things are rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
Harry is nice.
True
1
proof
[(triple1)]
("Harry" "is" "nice" "+")
triple1
Harry is not nice.
False
1
inv-proof
[(triple1)]
("Harry" "is" "nice" "-")
triple1
Harry is furry.
True
2
proof
[(((triple1) -> rule4))]
("Harry" "is" "furry" "+")
((triple1) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple1) -> rule4))]
("Harry" "is" "furry" "-")
((triple1) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
True
3
proof
[(((((triple1) -> rule4)) -> rule6) OR ((((((triple1) -> rule4)) -> rule8) ((triple1) -> rule4)) -> rule3))]
("Harry" "is" "smart" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule8 % int2)) ((triple1) -> (rule4 % int3))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is not smart.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule6) OR ((((((triple1) -> rule4)) -> rule8) ((triple1) -> rule4)) -> rule3))]
("Harry" "is" "smart" "-")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule8 % int2)) ((triple1) -> (rule4 % int3))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is green.
True
4
proof
[(((((((triple1) -> rule4)) -> rule6)) -> rule2) OR ((((((((triple1) -> rule4)) -> rule8) ((triple1) -> rule4)) -> rule3)) -> rule2))]
("Harry" "is" "green" "+")
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((((((triple1) -> (rule4 % int4))) -> (rule8 % int3)) ((triple1) -> (rule4 % int4))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is not green.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule6)) -> rule2) OR ((((((((triple1) -> rule4)) -> rule8) ((triple1) -> rule4)) -> rule3)) -> rule2))]
("Harry" "is" "green" "-")
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((((((triple1) -> (rule4 % int4))) -> (rule8 % int3)) ((triple1) -> (rule4 % int4))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
@0: Harry is nice.[(triple1)] @1: Harry is furry.[(((triple1) -> rule4))] @2: Harry is rough.[(((((triple1) -> rule4)) -> rule8))] Harry is smart.[(((((triple1) -> rule4)) -> rule6) OR ((((((triple1) -> rule4)) -> rule8) ((triple1) -> rule4)) -> rule3))] @3: Harry is green.[(((((((triple1) -> rule4)) -> rule6)) -> rule2) OR ((((((((triple1) -> rule4)) -> rule8) ((triple1) -> rule4)) -> rule3)) -> rule2))] @4: Harry is round.[(((((((((triple1) -> rule4)) -> rule6)) -> rule2)) -> rule1) OR ((((((((((triple1) -> rule4)) -> rule8) ((triple1) -> rule4)) -> rule3)) -> rule2)) -> rule1))]
Harry is nice.
("Harry" "is" "nice" "+")
triple1
Harry is furry.
("Harry" "is" "furry" "+")
((triple1) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((((triple1) -> (rule4 % int2))) -> (rule8 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule8 % int2)) ((triple1) -> (rule4 % int3))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((((((triple1) -> (rule4 % int4))) -> (rule8 % int3)) ((triple1) -> (rule4 % int4))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is round.
("Harry" "is" "round" "+")
((((((((triple1) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
((((((((((triple1) -> (rule4 % int5))) -> (rule8 % int4)) ((triple1) -> (rule4 % int5))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is furry.
("Harry" "is" "furry" "+")
int5