Harry is blue. All green people are furry. Blue people are furry. All cold people are red. Cold, red people are furry. All rough people are cold. If Harry is furry and Harry is red then Harry is round. If Harry is round then Harry is green. If someone is furry then they are rough.
Harry is blue.
("Harry" "is" "blue" "+")
All green people are furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
Blue people are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
All cold people are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
Cold, red people are furry.
((("someone" "is" "cold" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
All rough people are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If Harry is furry and Harry is red then Harry is round.
((("Harry" "is" "furry" "+") ("Harry" "is" "red" "+")) -> ("Harry" "is" "round" "+"))
If Harry is round then Harry is green.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "green" "+"))
If someone is furry then they are rough.
((("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
Harry is blue.
True
1
proof
[(triple1)]
("Harry" "is" "blue" "+")
triple1
Harry is not blue.
False
1
inv-proof
[(triple1)]
("Harry" "is" "blue" "-")
triple1
Harry is furry.
True
2
proof
[(((triple1) -> rule2))]
("Harry" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple1) -> rule2))]
("Harry" "is" "furry" "-")
((triple1) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is rough.
True
3
proof
[(((((triple1) -> rule2)) -> rule8))]
("Harry" "is" "rough" "+")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not rough.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule8))]
("Harry" "is" "rough" "-")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is cold.
True
4
proof
[(((((((triple1) -> rule2)) -> rule8)) -> rule5))]
("Harry" "is" "cold" "+")
((((((triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is not cold.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule8)) -> rule5))]
("Harry" "is" "cold" "-")
((((((triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
@0: Harry is blue.[(triple1)] @1: Harry is furry.[(((triple1) -> rule2))] @2: Harry is rough.[(((((triple1) -> rule2)) -> rule8))] @3: Harry is cold.[(((((((triple1) -> rule2)) -> rule8)) -> rule5))] @4: Harry is red.[(((((((((triple1) -> rule2)) -> rule8)) -> rule5)) -> rule3))] @5: Harry is round.[(((((triple1) -> rule2) ((((((((triple1) -> rule2)) -> rule8)) -> rule5)) -> rule3)) -> rule6))] @6: Harry is green.[(((((((triple1) -> rule2) ((((((((triple1) -> rule2)) -> rule8)) -> rule5)) -> rule3)) -> rule6)) -> rule7))]
Harry is blue.
("Harry" "is" "blue" "+")
triple1
Harry is furry.
("Harry" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((((((triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
((((((((triple1) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is round.
("Harry" "is" "round" "+")
((((triple1) -> (rule2 % int5)) ((((((((triple1) -> (rule2 % int5))) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is furry.
("Harry" "is" "furry" "+")
int5
Harry is green.
("Harry" "is" "green" "+")
((((((triple1) -> (rule2 % int6)) ((((((((triple1) -> (rule2 % int6))) -> (rule8 % int5))) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
int5
Harry is furry.
("Harry" "is" "furry" "+")
int6