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