Harry is blue. Harry is green. Harry is rough. If Harry is kind and Harry is young then Harry is nice. Young, smart things are nice. If something is young then it is rough. All smart things are kind. All nice, blue things are kind. If Harry is nice then Harry is kind. All kind, nice things are smart. If Harry is green then Harry is nice.
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If Harry is kind and Harry is young then Harry is nice.
((("Harry" "is" "kind" "+") ("Harry" "is" "young" "+")) -> ("Harry" "is" "nice" "+"))
Young, smart things are nice.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
If something is young then it is rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
All smart things are kind.
((("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
All nice, blue things are kind.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If Harry is nice then Harry is kind.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "kind" "+"))
All kind, nice things are smart.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
If Harry is green then Harry is nice.
((("Harry" "is" "green" "+")) -> ("Harry" "is" "nice" "+"))
Harry is green.
True
1
proof
[(triple2)]
("Harry" "is" "green" "+")
triple2
Harry is not blue.
False
1
inv-proof
[(triple1)]
("Harry" "is" "blue" "-")
triple1
Harry is nice.
True
2
proof
[(((triple2) -> rule8))]
("Harry" "is" "nice" "+")
((triple2) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not nice.
False
2
inv-proof
[(((triple2) -> rule8))]
("Harry" "is" "nice" "-")
((triple2) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is kind.
True
3
proof
[(((((triple2) -> rule8)) -> rule6) OR ((((triple2) -> rule8) triple1) -> rule5))]
("Harry" "is" "kind" "+")
((((triple2) -> (rule8 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple2) -> (rule8 % int2)) triple1) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not kind.
False
3
inv-proof
[(((((triple2) -> rule8)) -> rule6) OR ((((triple2) -> rule8) triple1) -> rule5))]
("Harry" "is" "kind" "-")
((((triple2) -> (rule8 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple2) -> (rule8 % int2)) triple1) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is smart.
True
6
proof
[(((((((triple2) -> rule8)) -> rule6) ((triple2) -> rule8)) -> rule7) OR ((((((triple2) -> rule8) triple1) -> rule5) ((triple2) -> rule8)) -> rule7))]
("Harry" "is" "smart" "+")
((((((triple2) -> (rule8 % int3))) -> (rule6 % int2)) ((triple2) -> (rule8 % int3))) -> (rule7 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((((triple2) -> (rule8 % int3)) triple1) -> (rule5 % int2)) ((triple2) -> (rule8 % int3))) -> (rule7 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is not smart.
False
6
inv-proof
[(((((((triple2) -> rule8)) -> rule6) ((triple2) -> rule8)) -> rule7) OR ((((((triple2) -> rule8) triple1) -> rule5) ((triple2) -> rule8)) -> rule7))]
("Harry" "is" "smart" "-")
((((((triple2) -> (rule8 % int3))) -> (rule6 % int2)) ((triple2) -> (rule8 % int3))) -> (rule7 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((((triple2) -> (rule8 % int3)) triple1) -> (rule5 % int2)) ((triple2) -> (rule8 % int3))) -> (rule7 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
@0: Harry is blue.[(triple1)] Harry is green.[(triple2)] Harry is rough.[(triple3)] @1: Harry is nice.[(((triple2) -> rule8))] @2: Harry is kind.[(((((triple2) -> rule8)) -> rule6) OR ((((triple2) -> rule8) triple1) -> rule5))] @3: Harry is smart.[(((((((triple2) -> rule8)) -> rule6) ((triple2) -> rule8)) -> rule7) OR ((((((triple2) -> rule8) triple1) -> rule5) ((triple2) -> rule8)) -> rule7))]
Harry is blue.
("Harry" "is" "blue" "+")
triple1
Harry is green.
("Harry" "is" "green" "+")
triple2
Harry is rough.
("Harry" "is" "rough" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
((triple2) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((((triple2) -> (rule8 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple2) -> (rule8 % int2)) triple1) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((((((triple2) -> (rule8 % int3))) -> (rule6 % int2)) ((triple2) -> (rule8 % int3))) -> (rule7 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((((triple2) -> (rule8 % int3)) triple1) -> (rule5 % int2)) ((triple2) -> (rule8 % int3))) -> (rule7 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3