Harry is cold. Harry is kind. Harry is nice. Harry is quiet. Harry is round. Harry is smart. Harry is young. If Harry is not cold then Harry is not nice. If something is smart and not kind then it is quiet. All cold things are quiet. If something is kind then it is round. If Harry is smart and Harry is not cold then Harry is not round. Young things are nice. Quiet things are nice. All young things are smart.
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is not cold then Harry is not nice.
((("Harry" "is" "cold" "~")) -> ("Harry" "is" "nice" "-"))
If something is smart and not kind then it is quiet.
((("something" "is" "smart" "+") ("something" "is" "kind" "~")) -> ("something" "is" "quiet" "+"))
All cold things are quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
If something is kind then it is round.
((("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
If Harry is smart and Harry is not cold then Harry is not round.
((("Harry" "is" "smart" "+") ("Harry" "is" "cold" "~")) -> ("Harry" "is" "round" "-"))
Young things are nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
Quiet things are nice.
((("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
All young things are smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
Harry is smart.
True
1
proof
[(triple6 OR ((triple7) -> rule8))]
("Harry" "is" "smart" "+")
triple6
((triple7) -> (rule8 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not young.
False
1
inv-proof
[(triple7)]
("Harry" "is" "young" "-")
triple7
@0: Harry is cold.[(triple1)] Harry is kind.[(triple2)] Harry is nice.[(triple3 OR ((triple4) -> rule7) OR ((triple7) -> rule6) OR ((((triple1) -> rule3)) -> rule7))] Harry is quiet.[(triple4 OR ((triple1) -> rule3))] Harry is round.[(triple5 OR ((triple2) -> rule4))] Harry is smart.[(triple6 OR ((triple7) -> rule8))] Harry is young.[(triple7)]
Harry is cold.
("Harry" "is" "cold" "+")
triple1
Harry is kind.
("Harry" "is" "kind" "+")
triple2
Harry is nice.
("Harry" "is" "nice" "+")
triple3
((triple4) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple7) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
((triple1) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple5
((triple2) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple6
((triple7) -> (rule8 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple7