Harry is blue. Harry is cold. Harry is green. Cold things are furry. All big, blue things are furry. Furry things are green. If Harry is green then Harry is rough. If Harry is rough then Harry is round. All furry, big things are rough. All big, blue things are cold. All blue, cold things are rough.
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Cold things are furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
All big, blue things are furry.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
Furry things are green.
((("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
If Harry is green then Harry is rough.
((("Harry" "is" "green" "+")) -> ("Harry" "is" "rough" "+"))
If Harry is rough then Harry is round.
((("Harry" "is" "rough" "+")) -> ("Harry" "is" "round" "+"))
All furry, big things are rough.
((("something" "is" "furry" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
All big, blue things are cold.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
All blue, cold things are rough.
((("something" "is" "blue" "+") ("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
Harry is cold.
True
1
proof
[(triple2)]
("Harry" "is" "cold" "+")
triple2
Harry is not blue.
False
1
inv-proof
[(triple1)]
("Harry" "is" "blue" "-")
triple1
Harry is rough.
True
2
proof
[(((triple3) -> rule4) OR ((triple1 triple2) -> rule8) OR ((((((triple2) -> rule1)) -> rule3)) -> rule4))]
("Harry" "is" "rough" "+")
((triple3) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple1 triple2) -> (rule8 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is not rough.
False
2
inv-proof
[(((triple3) -> rule4) OR ((triple1 triple2) -> rule8) OR ((((((triple2) -> rule1)) -> rule3)) -> rule4))]
("Harry" "is" "rough" "-")
((triple3) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple1 triple2) -> (rule8 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is round.
True
3
proof
[(((((triple3) -> rule4)) -> rule5) OR ((((triple1 triple2) -> rule8)) -> rule5) OR ((((((((triple2) -> rule1)) -> rule3)) -> rule4)) -> rule5))]
("Harry" "is" "round" "+")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple1 triple2) -> (rule8 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((((((triple2) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is not round.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule5) OR ((((triple1 triple2) -> rule8)) -> rule5) OR ((((((((triple2) -> rule1)) -> rule3)) -> rule4)) -> rule5))]
("Harry" "is" "round" "-")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple1 triple2) -> (rule8 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((((((triple2) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
@0: Harry is blue.[(triple1)] Harry is cold.[(triple2)] Harry is green.[(triple3 OR ((((triple2) -> rule1)) -> rule3))] @1: Harry is furry.[(((triple2) -> rule1))] Harry is rough.[(((triple3) -> rule4) OR ((triple1 triple2) -> rule8) OR ((((((triple2) -> rule1)) -> rule3)) -> rule4))] @2: Harry is round.[(((((triple3) -> rule4)) -> rule5) OR ((((triple1 triple2) -> rule8)) -> rule5) OR ((((((((triple2) -> rule1)) -> rule3)) -> rule4)) -> rule5))]
Harry is blue.
("Harry" "is" "blue" "+")
triple1
Harry is cold.
("Harry" "is" "cold" "+")
triple2
Harry is green.
("Harry" "is" "green" "+")
triple3
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((triple2) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple3) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple1 triple2) -> (rule8 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple1 triple2) -> (rule8 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((((((triple2) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4