Gary is big. Gary is not blue. Gary is quiet. Gary is rough. Gary is round. Gary is not smart. Gary is young. If someone is smart and not big then they are not round. If someone is quiet then they are round. If someone is blue then they are round. If Gary is blue and Gary is not rough then Gary is round. If Gary is young then Gary is round. If Gary is blue then Gary is not round.
Gary is big.
("Gary" "is" "big" "+")
Gary is not blue.
("Gary" "is" "blue" "-")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is not smart.
("Gary" "is" "smart" "-")
Gary is young.
("Gary" "is" "young" "+")
If someone is smart and not big then they are not round.
((("someone" "is" "smart" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "round" "-"))
If someone is quiet then they are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
If someone is blue then they are round.
((("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If Gary is blue and Gary is not rough then Gary is round.
((("Gary" "is" "blue" "+") ("Gary" "is" "rough" "~")) -> ("Gary" "is" "round" "+"))
If Gary is young then Gary is round.
((("Gary" "is" "young" "+")) -> ("Gary" "is" "round" "+"))
If Gary is blue then Gary is not round.
((("Gary" "is" "blue" "+")) -> ("Gary" "is" "round" "-"))
Gary is round.
True
1
proof
[(triple5 OR ((triple3) -> rule2) OR ((triple7) -> rule5))]
("Gary" "is" "round" "+")
triple5
((triple3) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple7) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is blue.
False
1
inv-proof
[(triple2)]
("Gary" "is" "blue" "+")
triple2
@0: Gary is big.[(triple1)] Gary is not blue.[(triple2)] Gary is not smart.[(triple6)] Gary is quiet.[(triple3)] Gary is rough.[(triple4)] Gary is round.[(triple5 OR ((triple3) -> rule2) OR ((triple7) -> rule5))] Gary is young.[(triple7)]
Gary is big.
("Gary" "is" "big" "+")
triple1
Gary is not blue.
("Gary" "is" "blue" "-")
triple2
Gary is not smart.
("Gary" "is" "smart" "-")
triple6
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Gary is rough.
("Gary" "is" "rough" "+")
triple4
Gary is round.
("Gary" "is" "round" "+")
triple5
((triple3) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple7) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
triple7