Harry is big. Harry is furry. Harry is green. Harry is nice. Harry is red. Harry is round. Harry is young. If someone is young and big then they are green. If someone is green and round then they are red. Green people are red.
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is young and big then they are green.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
If someone is green and round then they are red.
((("someone" "is" "green" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
Green people are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
Harry is round.
True
1
proof
[(triple6)]
("Harry" "is" "round" "+")
triple6
Harry is not green.
False
1
inv-proof
[(triple3 OR ((triple7 triple1) -> rule1))]
("Harry" "is" "green" "-")
triple3
((triple7 triple1) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
@0: Harry is big.[(triple1)] Harry is furry.[(triple2)] Harry is green.[(triple3 OR ((triple7 triple1) -> rule1))] Harry is nice.[(triple4)] Harry is red.[(triple5 OR ((triple3) -> rule3) OR ((triple3 triple6) -> rule2) OR ((((triple7 triple1) -> rule1)) -> rule3) OR ((((triple7 triple1) -> rule1) triple6) -> rule2))] Harry is round.[(triple6)] Harry is young.[(triple7)]
Harry is big.
("Harry" "is" "big" "+")
triple1
Harry is furry.
("Harry" "is" "furry" "+")
triple2
Harry is green.
("Harry" "is" "green" "+")
triple3
((triple7 triple1) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple4
Harry is red.
("Harry" "is" "red" "+")
triple5
((triple3) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple3 triple6) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple7 triple1) -> (rule1 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple7 triple1) -> (rule1 % int2)) triple6) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7