Harry is big. Harry is green. Harry is kind. Harry is red. Harry is rough. Harry is round. Harry is young. If Harry is green and Harry is rough then Harry is red. If something is green then it is red. If Harry is green then Harry is rough.
Harry is big.
("Harry" "is" "big" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is green and Harry is rough then Harry is red.
((("Harry" "is" "green" "+") ("Harry" "is" "rough" "+")) -> ("Harry" "is" "red" "+"))
If something is green then it is red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If Harry is green then Harry is rough.
((("Harry" "is" "green" "+")) -> ("Harry" "is" "rough" "+"))
Harry is green.
True
1
proof
[(triple2)]
("Harry" "is" "green" "+")
triple2
Harry is not green.
False
1
inv-proof
[(triple2)]
("Harry" "is" "green" "-")
triple2
@0: Harry is big.[(triple1)] Harry is green.[(triple2)] Harry is kind.[(triple3)] Harry is red.[(triple4 OR ((triple2) -> rule2) OR ((triple2 triple5) -> rule1) OR ((triple2 ((triple2) -> rule3)) -> rule1))] Harry is rough.[(triple5 OR ((triple2) -> rule3))] Harry is round.[(triple6)] Harry is young.[(triple7)]
Harry is big.
("Harry" "is" "big" "+")
triple1
Harry is green.
("Harry" "is" "green" "+")
triple2
Harry is kind.
("Harry" "is" "kind" "+")
triple3
Harry is red.
("Harry" "is" "red" "+")
triple4
((triple2) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple2 triple5) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple2 ((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
triple5
((triple2) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7