Gary is cold. Gary is not green. Gary is kind. Gary is quiet. Gary is not round. Gary is not smart. Gary is young. Harry is not cold. Harry is not green. Harry is kind. Harry is quiet. Harry is round. Harry is not smart. Harry is young. If someone is round and kind then they are quiet. All young, smart people are cold. If someone is green and not young then they are cold. If someone is kind and smart then they are not cold. If someone is smart and not round then they are not kind. If Gary is green and Gary is round then Gary is cold. If someone is quiet and young then they are not smart. If Gary is round and Gary is quiet then Gary is kind.
Gary is cold.
("Gary" "is" "cold" "+")
Gary is not green.
("Gary" "is" "green" "-")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is not round.
("Gary" "is" "round" "-")
Gary is not smart.
("Gary" "is" "smart" "-")
Gary is young.
("Gary" "is" "young" "+")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is not green.
("Harry" "is" "green" "-")
Harry is kind.
("Harry" "is" "kind" "+")
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" "+")
If someone is round and kind then they are quiet.
((("someone" "is" "round" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
All young, smart people are cold.
((("someone" "is" "young" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
If someone is green and not young then they are cold.
((("someone" "is" "green" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "cold" "+"))
If someone is kind and smart then they are not cold.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "-"))
If someone is smart and not round then they are not kind.
((("someone" "is" "smart" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "kind" "-"))
If Gary is green and Gary is round then Gary is cold.
((("Gary" "is" "green" "+") ("Gary" "is" "round" "+")) -> ("Gary" "is" "cold" "+"))
If someone is quiet and young then they are not smart.
((("someone" "is" "quiet" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "smart" "-"))
If Gary is round and Gary is quiet then Gary is kind.
((("Gary" "is" "round" "+") ("Gary" "is" "quiet" "+")) -> ("Gary" "is" "kind" "+"))
Gary is not smart.
True
1
proof
[(triple6 OR ((triple4 triple7) -> rule7))]
("Gary" "is" "smart" "-")
triple6
((triple4 triple7) -> (rule7 % int1))
Gary is not smart.
("Gary" "is" "smart" "-")
int1
Gary is not cold.
False
1
inv-proof
[(triple1)]
("Gary" "is" "cold" "-")
triple1
@0: Gary is cold.[(triple1)] Gary is kind.[(triple3)] Gary is not green.[(triple2)] Gary is not round.[(triple5)] Gary is not smart.[(triple6 OR ((triple4 triple7) -> rule7))] Gary is quiet.[(triple4)] Gary is young.[(triple7)] Harry is kind.[(triple10)] Harry is not cold.[(triple8)] Harry is not green.[(triple9)] Harry is not smart.[(triple13 OR ((triple11 triple14) -> rule7) OR ((((triple12 triple10) -> rule1) triple14) -> rule7))] Harry is quiet.[(triple11 OR ((triple12 triple10) -> rule1))] Harry is round.[(triple12)] Harry is young.[(triple14)]
Gary is cold.
("Gary" "is" "cold" "+")
triple1
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Gary is not green.
("Gary" "is" "green" "-")
triple2
Gary is not round.
("Gary" "is" "round" "-")
triple5
Gary is not smart.
("Gary" "is" "smart" "-")
triple6
((triple4 triple7) -> (rule7 % int1))
Gary is not smart.
("Gary" "is" "smart" "-")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple4
Gary is young.
("Gary" "is" "young" "+")
triple7
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Harry is not cold.
("Harry" "is" "cold" "-")
triple8
Harry is not green.
("Harry" "is" "green" "-")
triple9
Harry is not smart.
("Harry" "is" "smart" "-")
triple13
((triple11 triple14) -> (rule7 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
((((triple12 triple10) -> (rule1 % int2)) triple14) -> (rule7 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
((triple12 triple10) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple12
Harry is young.
("Harry" "is" "young" "+")
triple14