Harry is blue. Harry is kind. Harry is nice. If something is furry and green then it is white. All blue things are rough. If Harry is furry and Harry is green then Harry is kind. Blue, furry things are green. All green things are rough. If something is white and blue then it is kind. If Harry is nice and Harry is white then Harry is furry. If something is nice and rough then it is white.
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
If something is furry and green then it is white.
((("something" "is" "furry" "+") ("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
All blue things are rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If Harry is furry and Harry is green then Harry is kind.
((("Harry" "is" "furry" "+") ("Harry" "is" "green" "+")) -> ("Harry" "is" "kind" "+"))
Blue, furry things are green.
((("something" "is" "blue" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
All green things are rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
If something is white and blue then it is kind.
((("something" "is" "white" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If Harry is nice and Harry is white then Harry is furry.
((("Harry" "is" "nice" "+") ("Harry" "is" "white" "+")) -> ("Harry" "is" "furry" "+"))
If something is nice and rough then it is white.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
Harry is kind.
True
1
proof
[(triple2 OR ((((triple3 ((triple1) -> rule2)) -> rule8) triple1) -> rule6) OR ((((triple3 ((triple3 ((triple1) -> rule2)) -> rule8)) -> rule7) ((triple1 ((triple3 ((triple3 ((triple1) -> rule2)) -> rule8)) -> rule7)) -> rule4)) -> rule3))]
("Harry" "is" "kind" "+")
triple2
((((triple3 ((triple1) -> (rule2 % int3))) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((triple3 ((triple3 ((triple1) -> (rule2 % int5))) -> (rule8 % int4))) -> (rule7 % int3)) ((triple1 ((triple3 ((triple3 ((triple1) -> (rule2 % int5))) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
int5
Harry is not blue.
False
1
inv-proof
[(triple1)]
("Harry" "is" "blue" "-")
triple1
Harry is rough.
True
2
proof
[(((triple1) -> rule2))]
("Harry" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not rough.
False
2
inv-proof
[(((triple1) -> rule2))]
("Harry" "is" "rough" "-")
((triple1) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
True
4
proof
[(((triple3 ((triple1) -> rule2)) -> rule8))]
("Harry" "is" "white" "+")
((triple3 ((triple1) -> (rule2 % int2))) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not white.
False
4
inv-proof
[(((triple3 ((triple1) -> rule2)) -> rule8))]
("Harry" "is" "white" "-")
((triple3 ((triple1) -> (rule2 % int2))) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is furry.
True
6
proof
[(((triple3 ((triple3 ((triple1) -> rule2)) -> rule8)) -> rule7))]
("Harry" "is" "furry" "+")
((triple3 ((triple3 ((triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is not furry.
False
6
inv-proof
[(((triple3 ((triple3 ((triple1) -> rule2)) -> rule8)) -> rule7))]
("Harry" "is" "furry" "-")
((triple3 ((triple3 ((triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
@0: Harry is blue.[(triple1)] Harry is kind.[(triple2 OR ((((triple3 ((triple1) -> rule2)) -> rule8) triple1) -> rule6) OR ((((triple3 ((triple3 ((triple1) -> rule2)) -> rule8)) -> rule7) ((triple1 ((triple3 ((triple3 ((triple1) -> rule2)) -> rule8)) -> rule7)) -> rule4)) -> rule3))] Harry is nice.[(triple3)] @1: Harry is rough.[(((triple1) -> rule2))] @2: Harry is white.[(((triple3 ((triple1) -> rule2)) -> rule8))] @3: Harry is furry.[(((triple3 ((triple3 ((triple1) -> rule2)) -> rule8)) -> rule7))] @4: Harry is green.[(((triple1 ((triple3 ((triple3 ((triple1) -> rule2)) -> rule8)) -> rule7)) -> rule4))]
Harry is blue.
("Harry" "is" "blue" "+")
triple1
Harry is kind.
("Harry" "is" "kind" "+")
triple2
((((triple3 ((triple1) -> (rule2 % int3))) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((triple3 ((triple3 ((triple1) -> (rule2 % int5))) -> (rule8 % int4))) -> (rule7 % int3)) ((triple1 ((triple3 ((triple3 ((triple1) -> (rule2 % int5))) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
int5
Harry is nice.
("Harry" "is" "nice" "+")
triple3
Harry is rough.
("Harry" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple3 ((triple1) -> (rule2 % int2))) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((triple3 ((triple3 ((triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
((triple1 ((triple3 ((triple3 ((triple1) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4