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