Harry is green. Harry is nice. Harry is rough. Harry is round. Harry is smart. Harry is white. Harry is young. Nice, young things are rough. Rough things are round. If something is nice then it is white.
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
Nice, young things are rough.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
Rough things are round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If something is nice then it is white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
Harry is nice.
True
1
proof
[(triple2)]
("Harry" "is" "nice" "+")
triple2
Harry is not rough.
False
1
inv-proof
[(triple3 OR ((triple2 triple7) -> rule1))]
("Harry" "is" "rough" "-")
triple3
((triple2 triple7) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
@0: Harry is green.[(triple1)] Harry is nice.[(triple2)] Harry is rough.[(triple3 OR ((triple2 triple7) -> rule1))] Harry is round.[(triple4 OR ((triple3) -> rule2) OR ((((triple2 triple7) -> rule1)) -> rule2))] Harry is smart.[(triple5)] Harry is white.[(triple6 OR ((triple2) -> rule3))] Harry is young.[(triple7)]
Harry is green.
("Harry" "is" "green" "+")
triple1
Harry is nice.
("Harry" "is" "nice" "+")
triple2
Harry is rough.
("Harry" "is" "rough" "+")
triple3
((triple2 triple7) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple4
((triple3) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple2 triple7) -> (rule1 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple5
Harry is white.
("Harry" "is" "white" "+")
triple6
((triple2) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple7