%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PUZ019-1 : TPTP v9.3.1. Bugfixed v5.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:23:07 AM UTC 2026
% Result : Unsatisfiable 0.12s 0.46s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 39
% Syntax : Number of formulae : 197 ( 77 unt; 0 def)
% Number of atoms : 590 ( 0 equ)
% Maximal formula atoms : 13 ( 2 avg)
% Number of connectives : 626 ( 233 ~; 393 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 12 con; 0-0 aty)
% Number of variables : 176 ( 87 sgn 28 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(males_are_not_female,axiom,
! [VAR_0] :
( ~ female(VAR_0)
| ~ male(VAR_0) ),
file('theBenchmark.p',males_are_not_female) ).
cnf(c_1,plain,
( ~ female(A)
| ~ male(A) ),
inference(clausify,[status(thm)],[males_are_not_female]) ).
fof(actor_is_male,axiom,
! [VAR_0] :
( male(VAR_0)
| ~ has_job(VAR_0,actor) ),
file('theBenchmark.p',actor_is_male) ).
cnf(c_2,plain,
( male(A)
| ~ has_job(A,actor) ),
inference(clausify,[status(thm)],[actor_is_male]) ).
fof(nurse_is_male,axiom,
! [VAR_0] :
( male(VAR_0)
| ~ has_job(VAR_0,nurse) ),
file('theBenchmark.p',nurse_is_male) ).
cnf(c_3,plain,
( male(A)
| ~ has_job(A,nurse) ),
inference(clausify,[status(thm)],[nurse_is_male]) ).
fof(husband_is_male,axiom,
! [VAR_0,VAR_1] :
( male(VAR_1)
| ~ husband(VAR_0,VAR_1) ),
file('theBenchmark.p',husband_is_male) ).
cnf(c_5,plain,
( male(B)
| ~ husband(A,B) ),
inference(clausify,[status(thm)],[husband_is_male]) ).
fof(steve_is_male,axiom,
male(steve),
file('theBenchmark.p',steve_is_male) ).
cnf(c_6,plain,
male(steve),
inference(clausify,[status(thm)],[steve_is_male]) ).
fof(pete_is_male,axiom,
male(pete),
file('theBenchmark.p',pete_is_male) ).
cnf(c_7,plain,
male(pete),
inference(clausify,[status(thm)],[pete_is_male]) ).
fof(thelma_is_female,axiom,
female(thelma),
file('theBenchmark.p',thelma_is_female) ).
cnf(c_8,plain,
female(thelma),
inference(clausify,[status(thm)],[thelma_is_female]) ).
cnf(c_9,plain,
( ~ has_job(A,actor)
| ~ female(A) ),
inference(resolve,[status(thm)],[c_1,c_2]) ).
cnf(c_10,plain,
( ~ has_job(A,nurse)
| ~ female(A) ),
inference(resolve,[status(thm)],[c_1,c_3]) ).
cnf(c_11,plain,
( ~ female(B)
| ~ husband(A,B) ),
inference(resolve,[status(thm)],[c_5,c_1]) ).
cnf(c_12,plain,
~ female(steve),
inference(resolve,[status(thm)],[c_6,c_1]) ).
cnf(c_13,plain,
~ female(pete),
inference(resolve,[status(thm)],[c_7,c_1]) ).
fof(roberta_is_female,axiom,
female(roberta),
file('theBenchmark.p',roberta_is_female) ).
cnf(c_14,plain,
female(roberta),
inference(clausify,[status(thm)],[roberta_is_female]) ).
fof(wife_is_female,axiom,
! [VAR_0,VAR_1] :
( female(VAR_0)
| ~ husband(VAR_0,VAR_1) ),
file('theBenchmark.p',wife_is_female) ).
cnf(c_15,plain,
( female(A)
| ~ husband(A,B) ),
inference(clausify,[status(thm)],[wife_is_female]) ).
fof(chef_is_female,axiom,
! [VAR_0] :
( female(VAR_0)
| ~ has_job(VAR_0,chef) ),
file('theBenchmark.p',chef_is_female) ).
cnf(c_16,plain,
( female(A)
| ~ has_job(A,chef) ),
inference(clausify,[status(thm)],[chef_is_female]) ).
fof(pete_is_not_educated,axiom,
~ educated(pete),
file('theBenchmark.p',pete_is_not_educated) ).
cnf(c_17,plain,
~ educated(pete),
inference(clausify,[status(thm)],[pete_is_not_educated]) ).
fof(police_is_educated,axiom,
! [VAR_0] :
( educated(VAR_0)
| ~ has_job(VAR_0,police) ),
file('theBenchmark.p',police_is_educated) ).
cnf(c_18,plain,
( educated(A)
| ~ has_job(A,police) ),
inference(clausify,[status(thm)],[police_is_educated]) ).
fof(teacher_is_educated,axiom,
! [VAR_0] :
( educated(VAR_0)
| ~ has_job(VAR_0,teacher) ),
file('theBenchmark.p',teacher_is_educated) ).
cnf(c_19,plain,
( educated(A)
| ~ has_job(A,teacher) ),
inference(clausify,[status(thm)],[teacher_is_educated]) ).
fof(nurse_is_educated,axiom,
! [VAR_0] :
( educated(VAR_0)
| ~ has_job(VAR_0,nurse) ),
file('theBenchmark.p',nurse_is_educated) ).
cnf(c_20,plain,
( educated(A)
| ~ has_job(A,nurse) ),
inference(clausify,[status(thm)],[nurse_is_educated]) ).
cnf(c_21,plain,
~ has_job(pete,nurse),
inference(resolve,[status(thm)],[c_17,c_20]) ).
cnf(c_22,plain,
~ has_job(pete,teacher),
inference(resolve,[status(thm)],[c_17,c_19]) ).
cnf(c_23,plain,
~ has_job(pete,police),
inference(resolve,[status(thm)],[c_17,c_18]) ).
fof(find_who_has_each_job,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7] :
( ~ has_job(VAR_7,boxer)
| ~ has_job(VAR_6,actor)
| ~ has_job(VAR_5,teacher)
| ~ has_job(VAR_4,police)
| ~ has_job(VAR_3,operator)
| ~ has_job(VAR_2,nurse)
| ~ has_job(VAR_1,guard)
| ~ has_job(VAR_0,chef) ),
file('theBenchmark.p',find_who_has_each_job) ).
cnf(c_24,plain,
( ~ has_job(V7,boxer)
| ~ has_job(V6,actor)
| ~ has_job(F,teacher)
| ~ has_job(E,police)
| ~ has_job(D,operator)
| ~ has_job(C,nurse)
| ~ has_job(B,guard)
| ~ has_job(A,chef) ),
inference(clausify,[status(thm)],[find_who_has_each_job]) ).
fof(roberta_is_not_police,axiom,
~ has_job(roberta,police),
file('theBenchmark.p',roberta_is_not_police) ).
cnf(c_25,plain,
~ has_job(roberta,police),
inference(clausify,[status(thm)],[roberta_is_not_police]) ).
fof(roberta_is_not_boxer,axiom,
~ has_job(roberta,boxer),
file('theBenchmark.p',roberta_is_not_boxer) ).
cnf(c_26,plain,
~ has_job(roberta,boxer),
inference(clausify,[status(thm)],[roberta_is_not_boxer]) ).
fof(roberta_is_not_chef,axiom,
~ has_job(roberta,chef),
file('theBenchmark.p',roberta_is_not_chef) ).
cnf(c_27,plain,
~ has_job(roberta,chef),
inference(clausify,[status(thm)],[roberta_is_not_chef]) ).
fof(everyone_works,axiom,
! [VAR_0] :
( has_job(VAR_0,boxer)
| has_job(VAR_0,actor)
| has_job(VAR_0,teacher)
| has_job(VAR_0,police)
| has_job(VAR_0,operator)
| has_job(VAR_0,nurse)
| has_job(VAR_0,guard)
| has_job(VAR_0,chef) ),
file('theBenchmark.p',everyone_works) ).
cnf(c_28,plain,
( has_job(A,boxer)
| has_job(A,actor)
| has_job(A,teacher)
| has_job(A,police)
| has_job(A,operator)
| has_job(A,nurse)
| has_job(A,guard)
| has_job(A,chef) ),
inference(clausify,[status(thm)],[everyone_works]) ).
fof(every_job_is_used,axiom,
! [VAR_0] :
( has_job(steve,VAR_0)
| has_job(pete,VAR_0)
| has_job(thelma,VAR_0)
| has_job(roberta,VAR_0) ),
file('theBenchmark.p',every_job_is_used) ).
cnf(c_29,plain,
( has_job(steve,A)
| has_job(pete,A)
| has_job(thelma,A)
| has_job(roberta,A) ),
inference(clausify,[status(thm)],[every_job_is_used]) ).
fof(each_has_maximum_of_two_jobs,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( equal_jobs(VAR_2,VAR_3)
| equal_jobs(VAR_1,VAR_3)
| equal_jobs(VAR_1,VAR_2)
| ~ has_job(VAR_0,VAR_3)
| ~ has_job(VAR_0,VAR_2)
| ~ has_job(VAR_0,VAR_1) ),
file('theBenchmark.p',each_has_maximum_of_two_jobs) ).
cnf(c_30,plain,
( equal_jobs(C,D)
| equal_jobs(B,D)
| equal_jobs(B,C)
| ~ has_job(A,D)
| ~ has_job(A,C)
| ~ has_job(A,B) ),
inference(clausify,[status(thm)],[each_has_maximum_of_two_jobs]) ).
fof(husband_of_chef_is_operator1,axiom,
! [VAR_0,VAR_1] :
( husband(VAR_0,VAR_1)
| ~ has_job(VAR_1,operator)
| ~ has_job(VAR_0,chef) ),
file('theBenchmark.p',husband_of_chef_is_operator1) ).
cnf(c_33,plain,
( husband(A,B)
| ~ has_job(B,operator)
| ~ has_job(A,chef) ),
inference(clausify,[status(thm)],[husband_of_chef_is_operator1]) ).
fof(chef_is_not_also_police,axiom,
! [VAR_0] :
( ~ has_job(VAR_0,police)
| ~ has_job(VAR_0,chef) ),
file('theBenchmark.p',chef_is_not_also_police) ).
cnf(c_34,plain,
( ~ has_job(A,police)
| ~ has_job(A,chef) ),
inference(clausify,[status(thm)],[chef_is_not_also_police]) ).
fof(actor_not_boxer,axiom,
~ equal_jobs(actor,boxer),
file('theBenchmark.p',actor_not_boxer) ).
cnf(c_37,plain,
~ equal_jobs(actor,boxer),
inference(clausify,[status(thm)],[actor_not_boxer]) ).
fof(police_not_teacher,axiom,
~ equal_jobs(police,teacher),
file('theBenchmark.p',police_not_teacher) ).
cnf(c_38,plain,
~ equal_jobs(police,teacher),
inference(clausify,[status(thm)],[police_not_teacher]) ).
fof(police_not_boxer,axiom,
~ equal_jobs(police,boxer),
file('theBenchmark.p',police_not_boxer) ).
cnf(c_39,plain,
~ equal_jobs(police,boxer),
inference(clausify,[status(thm)],[police_not_boxer]) ).
fof(police_not_actor,axiom,
~ equal_jobs(police,actor),
file('theBenchmark.p',police_not_actor) ).
cnf(c_40,plain,
~ equal_jobs(police,actor),
inference(clausify,[status(thm)],[police_not_actor]) ).
fof(operator_not_boxer,axiom,
~ equal_jobs(operator,boxer),
file('theBenchmark.p',operator_not_boxer) ).
cnf(c_42,plain,
~ equal_jobs(operator,boxer),
inference(clausify,[status(thm)],[operator_not_boxer]) ).
fof(operator_not_actor,axiom,
~ equal_jobs(operator,actor),
file('theBenchmark.p',operator_not_actor) ).
cnf(c_43,plain,
~ equal_jobs(operator,actor),
inference(clausify,[status(thm)],[operator_not_actor]) ).
fof(operator_not_police,axiom,
~ equal_jobs(operator,police),
file('theBenchmark.p',operator_not_police) ).
cnf(c_44,plain,
~ equal_jobs(operator,police),
inference(clausify,[status(thm)],[operator_not_police]) ).
fof(nurse_not_teacher,axiom,
~ equal_jobs(nurse,teacher),
file('theBenchmark.p',nurse_not_teacher) ).
cnf(c_45,plain,
~ equal_jobs(nurse,teacher),
inference(clausify,[status(thm)],[nurse_not_teacher]) ).
fof(nurse_not_boxer,axiom,
~ equal_jobs(nurse,boxer),
file('theBenchmark.p',nurse_not_boxer) ).
cnf(c_46,plain,
~ equal_jobs(nurse,boxer),
inference(clausify,[status(thm)],[nurse_not_boxer]) ).
fof(nurse_not_actor,axiom,
~ equal_jobs(nurse,actor),
file('theBenchmark.p',nurse_not_actor) ).
cnf(c_47,plain,
~ equal_jobs(nurse,actor),
inference(clausify,[status(thm)],[nurse_not_actor]) ).
fof(nurse_not_police,axiom,
~ equal_jobs(nurse,police),
file('theBenchmark.p',nurse_not_police) ).
cnf(c_48,plain,
~ equal_jobs(nurse,police),
inference(clausify,[status(thm)],[nurse_not_police]) ).
fof(nurse_not_operator,axiom,
~ equal_jobs(nurse,operator),
file('theBenchmark.p',nurse_not_operator) ).
cnf(c_49,plain,
~ equal_jobs(nurse,operator),
inference(clausify,[status(thm)],[nurse_not_operator]) ).
fof(guard_not_actor,axiom,
~ equal_jobs(guard,actor),
file('theBenchmark.p',guard_not_actor) ).
cnf(c_52,plain,
~ equal_jobs(guard,actor),
inference(clausify,[status(thm)],[guard_not_actor]) ).
fof(guard_not_police,axiom,
~ equal_jobs(guard,police),
file('theBenchmark.p',guard_not_police) ).
cnf(c_53,plain,
~ equal_jobs(guard,police),
inference(clausify,[status(thm)],[guard_not_police]) ).
fof(guard_not_operator,axiom,
~ equal_jobs(guard,operator),
file('theBenchmark.p',guard_not_operator) ).
cnf(c_54,plain,
~ equal_jobs(guard,operator),
inference(clausify,[status(thm)],[guard_not_operator]) ).
fof(guard_not_nurse,axiom,
~ equal_jobs(guard,nurse),
file('theBenchmark.p',guard_not_nurse) ).
cnf(c_55,plain,
~ equal_jobs(guard,nurse),
inference(clausify,[status(thm)],[guard_not_nurse]) ).
cnf(c_73,plain,
~ has_job(thelma,actor),
inference(resolve,[status(thm)],[c_8,c_9]) ).
cnf(c_74,plain,
~ has_job(thelma,nurse),
inference(resolve,[status(thm)],[c_8,c_10]) ).
cnf(c_76,plain,
~ has_job(roberta,actor),
inference(resolve,[status(thm)],[c_14,c_9]) ).
cnf(c_77,plain,
~ has_job(roberta,nurse),
inference(resolve,[status(thm)],[c_14,c_10]) ).
cnf(c_78,plain,
~ husband(A,roberta),
inference(resolve,[status(thm)],[c_14,c_11]) ).
cnf(c_81,plain,
( ~ husband(C,A)
| ~ husband(A,B) ),
inference(resolve,[status(thm)],[c_15,c_11]) ).
cnf(c_87,plain,
~ has_job(steve,chef),
inference(resolve,[status(thm)],[c_16,c_12]) ).
cnf(c_88,plain,
~ has_job(pete,chef),
inference(resolve,[status(thm)],[c_16,c_13]) ).
cnf(c_89,plain,
~ husband(A,A),
inference(factor,[status(thm)],[c_81]) ).
cnf(c_291,plain,
( ~ has_job(V6,boxer)
| ~ has_job(F,actor)
| ~ has_job(E,teacher)
| ~ has_job(D,police)
| ~ has_job(C,operator)
| ~ has_job(B,nurse)
| ~ has_job(A,guard)
| has_job(steve,chef)
| has_job(pete,chef)
| has_job(roberta,chef) ),
inference(resolve,[status(thm)],[c_29,c_24]) ).
cnf(c_292,plain,
( ~ has_job(V6,boxer)
| ~ has_job(F,actor)
| ~ has_job(E,teacher)
| ~ has_job(D,police)
| ~ has_job(C,operator)
| ~ has_job(B,nurse)
| ~ has_job(A,guard)
| has_job(steve,chef)
| has_job(pete,chef) ),
inference(resolve,[status(thm)],[c_27,c_291]) ).
cnf(c_293,plain,
( ~ has_job(V6,boxer)
| ~ has_job(F,actor)
| ~ has_job(E,teacher)
| ~ has_job(D,police)
| ~ has_job(C,operator)
| ~ has_job(B,nurse)
| ~ has_job(A,guard)
| has_job(steve,chef) ),
inference(resolve,[status(thm)],[c_88,c_292]) ).
cnf(c_99,plain,
( ~ has_job(V6,boxer)
| ~ has_job(F,actor)
| ~ has_job(E,teacher)
| ~ has_job(D,police)
| ~ has_job(C,operator)
| ~ has_job(B,nurse)
| ~ has_job(A,guard) ),
inference(resolve,[status(thm)],[c_87,c_293]) ).
cnf(c_294,plain,
( has_job(steve,chef)
| has_job(pete,chef)
| has_job(roberta,chef)
| husband(thelma,A)
| ~ has_job(A,operator) ),
inference(resolve,[status(thm)],[c_33,c_29]) ).
cnf(c_295,plain,
( has_job(steve,chef)
| has_job(pete,chef)
| husband(thelma,A)
| ~ has_job(A,operator) ),
inference(resolve,[status(thm)],[c_27,c_294]) ).
cnf(c_296,plain,
( has_job(steve,chef)
| husband(thelma,A)
| ~ has_job(A,operator) ),
inference(resolve,[status(thm)],[c_88,c_295]) ).
cnf(c_117,plain,
( husband(thelma,A)
| ~ has_job(A,operator) ),
inference(resolve,[status(thm)],[c_87,c_296]) ).
cnf(c_297,plain,
( has_job(steve,chef)
| has_job(pete,chef)
| has_job(roberta,chef)
| husband(thelma,A)
| ~ has_job(A,operator) ),
inference(resolve,[status(thm)],[c_33,c_29]) ).
cnf(c_298,plain,
( has_job(steve,operator)
| has_job(pete,operator)
| has_job(roberta,operator)
| has_job(steve,chef)
| has_job(pete,chef)
| has_job(roberta,chef)
| husband(thelma,thelma) ),
inference(resolve,[status(thm)],[c_297,c_29]) ).
cnf(c_299,plain,
( has_job(steve,operator)
| has_job(pete,operator)
| has_job(roberta,operator)
| has_job(steve,chef)
| has_job(pete,chef)
| has_job(roberta,chef) ),
inference(resolve,[status(thm)],[c_89,c_298]) ).
cnf(c_300,plain,
( has_job(steve,operator)
| has_job(pete,operator)
| has_job(roberta,operator)
| has_job(steve,chef)
| has_job(pete,chef) ),
inference(resolve,[status(thm)],[c_27,c_299]) ).
cnf(c_301,plain,
( has_job(steve,operator)
| has_job(pete,operator)
| has_job(roberta,operator)
| has_job(steve,chef) ),
inference(resolve,[status(thm)],[c_88,c_300]) ).
cnf(c_119,plain,
( has_job(steve,operator)
| has_job(pete,operator)
| has_job(roberta,operator) ),
inference(resolve,[status(thm)],[c_87,c_301]) ).
cnf(c_302,plain,
( has_job(steve,chef)
| has_job(pete,chef)
| has_job(roberta,chef)
| ~ has_job(thelma,police) ),
inference(resolve,[status(thm)],[c_34,c_29]) ).
cnf(c_303,plain,
( has_job(steve,police)
| has_job(pete,police)
| has_job(roberta,police)
| has_job(steve,chef)
| has_job(pete,chef)
| has_job(roberta,chef) ),
inference(resolve,[status(thm)],[c_302,c_29]) ).
cnf(c_304,plain,
( has_job(steve,police)
| has_job(pete,police)
| has_job(roberta,police)
| has_job(steve,chef)
| has_job(pete,chef) ),
inference(resolve,[status(thm)],[c_27,c_303]) ).
cnf(c_305,plain,
( has_job(steve,police)
| has_job(pete,police)
| has_job(roberta,police)
| has_job(steve,chef) ),
inference(resolve,[status(thm)],[c_88,c_304]) ).
cnf(c_306,plain,
( has_job(steve,police)
| has_job(pete,police)
| has_job(roberta,police) ),
inference(resolve,[status(thm)],[c_87,c_305]) ).
cnf(c_307,plain,
( has_job(steve,police)
| has_job(pete,police) ),
inference(resolve,[status(thm)],[c_25,c_306]) ).
cnf(c_121,plain,
has_job(steve,police),
inference(resolve,[status(thm)],[c_23,c_307]) ).
cnf(c_308,plain,
( has_job(steve,actor)
| has_job(pete,actor)
| has_job(roberta,actor) ),
inference(resolve,[status(thm)],[c_73,c_29]) ).
cnf(c_156,plain,
( has_job(steve,actor)
| has_job(pete,actor) ),
inference(resolve,[status(thm)],[c_76,c_308]) ).
cnf(c_309,plain,
( has_job(steve,nurse)
| has_job(pete,nurse)
| has_job(roberta,nurse) ),
inference(resolve,[status(thm)],[c_74,c_29]) ).
cnf(c_310,plain,
( has_job(steve,nurse)
| has_job(pete,nurse) ),
inference(resolve,[status(thm)],[c_77,c_309]) ).
cnf(c_157,plain,
has_job(steve,nurse),
inference(resolve,[status(thm)],[c_21,c_310]) ).
cnf(c_311,plain,
( equal_jobs(nurse,B)
| equal_jobs(A,B)
| equal_jobs(A,nurse)
| ~ has_job(steve,B)
| ~ has_job(steve,A) ),
inference(resolve,[status(thm)],[c_30,c_157]) ).
cnf(c_312,plain,
( equal_jobs(nurse,police)
| equal_jobs(A,police)
| equal_jobs(A,nurse)
| ~ has_job(steve,A) ),
inference(resolve,[status(thm)],[c_311,c_121]) ).
cnf(c_313,plain,
( equal_jobs(nurse,police)
| equal_jobs(guard,police)
| ~ has_job(steve,guard) ),
inference(resolve,[status(thm)],[c_312,c_55]) ).
cnf(c_314,plain,
( equal_jobs(nurse,police)
| ~ has_job(steve,guard) ),
inference(resolve,[status(thm)],[c_313,c_53]) ).
cnf(c_176,plain,
~ has_job(steve,guard),
inference(resolve,[status(thm)],[c_314,c_48]) ).
cnf(c_315,plain,
( equal_jobs(A,B)
| equal_jobs(nurse,B)
| equal_jobs(nurse,A)
| ~ has_job(steve,B)
| ~ has_job(steve,A) ),
inference(resolve,[status(thm)],[c_30,c_157]) ).
cnf(c_316,plain,
( equal_jobs(A,police)
| equal_jobs(nurse,police)
| equal_jobs(nurse,A)
| ~ has_job(steve,A) ),
inference(resolve,[status(thm)],[c_315,c_121]) ).
cnf(c_317,plain,
( equal_jobs(operator,police)
| equal_jobs(nurse,police)
| ~ has_job(steve,operator) ),
inference(resolve,[status(thm)],[c_316,c_49]) ).
cnf(c_318,plain,
( equal_jobs(operator,police)
| ~ has_job(steve,operator) ),
inference(resolve,[status(thm)],[c_317,c_48]) ).
cnf(c_177,plain,
~ has_job(steve,operator),
inference(resolve,[status(thm)],[c_318,c_44]) ).
cnf(c_319,plain,
( equal_jobs(A,B)
| equal_jobs(nurse,B)
| equal_jobs(nurse,A)
| ~ has_job(steve,B)
| ~ has_job(steve,A) ),
inference(resolve,[status(thm)],[c_30,c_157]) ).
cnf(c_320,plain,
( equal_jobs(police,A)
| equal_jobs(nurse,A)
| equal_jobs(nurse,police)
| ~ has_job(steve,A) ),
inference(resolve,[status(thm)],[c_319,c_121]) ).
cnf(c_321,plain,
( equal_jobs(police,A)
| equal_jobs(nurse,A)
| ~ has_job(steve,A) ),
inference(resolve,[status(thm)],[c_320,c_48]) ).
cnf(c_322,plain,
( equal_jobs(police,actor)
| ~ has_job(steve,actor) ),
inference(resolve,[status(thm)],[c_321,c_47]) ).
cnf(c_178,plain,
~ has_job(steve,actor),
inference(resolve,[status(thm)],[c_322,c_40]) ).
cnf(c_323,plain,
( equal_jobs(A,B)
| equal_jobs(nurse,B)
| equal_jobs(nurse,A)
| ~ has_job(steve,B)
| ~ has_job(steve,A) ),
inference(resolve,[status(thm)],[c_30,c_157]) ).
cnf(c_324,plain,
( equal_jobs(police,A)
| equal_jobs(nurse,A)
| equal_jobs(nurse,police)
| ~ has_job(steve,A) ),
inference(resolve,[status(thm)],[c_323,c_121]) ).
cnf(c_325,plain,
( equal_jobs(police,A)
| equal_jobs(nurse,A)
| ~ has_job(steve,A) ),
inference(resolve,[status(thm)],[c_324,c_48]) ).
cnf(c_326,plain,
( equal_jobs(police,boxer)
| ~ has_job(steve,boxer) ),
inference(resolve,[status(thm)],[c_325,c_46]) ).
cnf(c_179,plain,
~ has_job(steve,boxer),
inference(resolve,[status(thm)],[c_326,c_39]) ).
cnf(c_327,plain,
( equal_jobs(A,B)
| equal_jobs(nurse,B)
| equal_jobs(nurse,A)
| ~ has_job(steve,B)
| ~ has_job(steve,A) ),
inference(resolve,[status(thm)],[c_30,c_157]) ).
cnf(c_328,plain,
( equal_jobs(police,A)
| equal_jobs(nurse,A)
| equal_jobs(nurse,police)
| ~ has_job(steve,A) ),
inference(resolve,[status(thm)],[c_327,c_121]) ).
cnf(c_329,plain,
( equal_jobs(police,A)
| equal_jobs(nurse,A)
| ~ has_job(steve,A) ),
inference(resolve,[status(thm)],[c_328,c_48]) ).
cnf(c_330,plain,
( equal_jobs(police,teacher)
| ~ has_job(steve,teacher) ),
inference(resolve,[status(thm)],[c_329,c_45]) ).
cnf(c_180,plain,
~ has_job(steve,teacher),
inference(resolve,[status(thm)],[c_330,c_38]) ).
cnf(c_184,plain,
( has_job(pete,operator)
| has_job(roberta,operator) ),
inference(resolve,[status(thm)],[c_177,c_119]) ).
cnf(c_185,plain,
has_job(pete,actor),
inference(resolve,[status(thm)],[c_178,c_156]) ).
cnf(c_197,plain,
~ has_job(roberta,operator),
inference(resolve,[status(thm)],[c_117,c_78]) ).
cnf(c_201,plain,
has_job(pete,operator),
inference(resolve,[status(thm)],[c_197,c_184]) ).
cnf(c_204,plain,
( ~ has_job(F,boxer)
| ~ has_job(E,actor)
| ~ has_job(D,teacher)
| ~ has_job(C,police)
| ~ has_job(B,operator)
| ~ has_job(A,guard) ),
inference(resolve,[status(thm)],[c_99,c_157]) ).
cnf(c_331,plain,
( equal_jobs(operator,B)
| equal_jobs(A,B)
| equal_jobs(A,operator)
| ~ has_job(pete,B)
| ~ has_job(pete,A) ),
inference(resolve,[status(thm)],[c_30,c_201]) ).
cnf(c_332,plain,
( equal_jobs(operator,actor)
| equal_jobs(A,actor)
| equal_jobs(A,operator)
| ~ has_job(pete,A) ),
inference(resolve,[status(thm)],[c_331,c_185]) ).
cnf(c_333,plain,
( equal_jobs(operator,actor)
| equal_jobs(guard,actor)
| ~ has_job(pete,guard) ),
inference(resolve,[status(thm)],[c_332,c_54]) ).
cnf(c_334,plain,
( equal_jobs(operator,actor)
| ~ has_job(pete,guard) ),
inference(resolve,[status(thm)],[c_333,c_52]) ).
cnf(c_216,plain,
~ has_job(pete,guard),
inference(resolve,[status(thm)],[c_334,c_43]) ).
cnf(c_335,plain,
( equal_jobs(A,B)
| equal_jobs(operator,B)
| equal_jobs(operator,A)
| ~ has_job(pete,B)
| ~ has_job(pete,A) ),
inference(resolve,[status(thm)],[c_30,c_201]) ).
cnf(c_336,plain,
( equal_jobs(actor,A)
| equal_jobs(operator,A)
| equal_jobs(operator,actor)
| ~ has_job(pete,A) ),
inference(resolve,[status(thm)],[c_335,c_185]) ).
cnf(c_337,plain,
( equal_jobs(actor,A)
| equal_jobs(operator,A)
| ~ has_job(pete,A) ),
inference(resolve,[status(thm)],[c_336,c_43]) ).
cnf(c_338,plain,
( equal_jobs(actor,boxer)
| ~ has_job(pete,boxer) ),
inference(resolve,[status(thm)],[c_337,c_42]) ).
cnf(c_217,plain,
~ has_job(pete,boxer),
inference(resolve,[status(thm)],[c_338,c_37]) ).
cnf(c_238,plain,
( ~ has_job(E,boxer)
| ~ has_job(D,actor)
| ~ has_job(C,teacher)
| ~ has_job(B,police)
| ~ has_job(A,guard) ),
inference(resolve,[status(thm)],[c_204,c_201]) ).
cnf(c_339,plain,
( has_job(steve,guard)
| has_job(pete,guard)
| has_job(roberta,guard)
| ~ has_job(E,boxer)
| ~ has_job(D,actor)
| ~ has_job(C,teacher)
| ~ has_job(B,police)
| ~ has_job(A,operator) ),
inference(resolve,[status(thm)],[c_204,c_29]) ).
cnf(c_340,plain,
( has_job(steve,guard)
| has_job(pete,guard)
| has_job(roberta,guard)
| ~ has_job(D,boxer)
| ~ has_job(C,actor)
| ~ has_job(B,teacher)
| ~ has_job(A,police) ),
inference(resolve,[status(thm)],[c_339,c_201]) ).
cnf(c_341,plain,
( has_job(steve,guard)
| has_job(pete,guard)
| has_job(roberta,guard)
| ~ has_job(C,boxer)
| ~ has_job(B,actor)
| ~ has_job(A,teacher) ),
inference(resolve,[status(thm)],[c_340,c_121]) ).
cnf(c_342,plain,
( has_job(C,boxer)
| has_job(C,actor)
| has_job(C,police)
| has_job(C,operator)
| has_job(C,nurse)
| has_job(C,guard)
| has_job(C,chef)
| has_job(steve,guard)
| has_job(pete,guard)
| has_job(roberta,guard)
| ~ has_job(B,boxer)
| ~ has_job(A,actor) ),
inference(resolve,[status(thm)],[c_341,c_28]) ).
cnf(c_343,plain,
( has_job(B,boxer)
| has_job(B,actor)
| has_job(B,police)
| has_job(B,operator)
| has_job(B,nurse)
| has_job(B,guard)
| has_job(B,chef)
| has_job(steve,guard)
| has_job(pete,guard)
| has_job(roberta,guard)
| ~ has_job(A,boxer) ),
inference(resolve,[status(thm)],[c_342,c_185]) ).
cnf(c_344,plain,
( has_job(steve,boxer)
| has_job(pete,boxer)
| has_job(roberta,boxer)
| has_job(A,boxer)
| has_job(A,actor)
| has_job(A,police)
| has_job(A,operator)
| has_job(A,nurse)
| has_job(A,guard)
| has_job(A,chef)
| has_job(steve,guard)
| has_job(pete,guard)
| has_job(roberta,guard) ),
inference(resolve,[status(thm)],[c_343,c_29]) ).
cnf(c_345,plain,
( has_job(steve,boxer)
| has_job(pete,boxer)
| has_job(roberta,boxer)
| has_job(A,boxer)
| has_job(A,actor)
| has_job(A,police)
| has_job(A,operator)
| has_job(A,nurse)
| has_job(A,guard)
| has_job(A,chef)
| has_job(steve,guard)
| has_job(roberta,guard) ),
inference(resolve,[status(thm)],[c_216,c_344]) ).
cnf(c_346,plain,
( has_job(steve,boxer)
| has_job(pete,boxer)
| has_job(roberta,boxer)
| has_job(A,boxer)
| has_job(A,actor)
| has_job(A,police)
| has_job(A,operator)
| has_job(A,nurse)
| has_job(A,guard)
| has_job(A,chef)
| has_job(roberta,guard) ),
inference(resolve,[status(thm)],[c_176,c_345]) ).
cnf(c_347,plain,
( has_job(steve,boxer)
| has_job(pete,boxer)
| has_job(A,boxer)
| has_job(A,actor)
| has_job(A,police)
| has_job(A,operator)
| has_job(A,nurse)
| has_job(A,guard)
| has_job(A,chef)
| has_job(roberta,guard) ),
inference(resolve,[status(thm)],[c_26,c_346]) ).
cnf(c_348,plain,
( has_job(steve,boxer)
| has_job(A,boxer)
| has_job(A,actor)
| has_job(A,police)
| has_job(A,operator)
| has_job(A,nurse)
| has_job(A,guard)
| has_job(A,chef)
| has_job(roberta,guard) ),
inference(resolve,[status(thm)],[c_217,c_347]) ).
cnf(c_245,plain,
( has_job(A,boxer)
| has_job(A,actor)
| has_job(A,police)
| has_job(A,operator)
| has_job(A,nurse)
| has_job(A,guard)
| has_job(A,chef)
| has_job(roberta,guard) ),
inference(resolve,[status(thm)],[c_179,c_348]) ).
cnf(c_349,plain,
( has_job(roberta,boxer)
| has_job(roberta,actor)
| has_job(roberta,police)
| has_job(roberta,operator)
| has_job(roberta,nurse)
| has_job(roberta,chef)
| has_job(roberta,guard) ),
inference(factor,[status(thm)],[c_245]) ).
cnf(c_350,plain,
( has_job(roberta,boxer)
| has_job(roberta,actor)
| has_job(roberta,police)
| has_job(roberta,operator)
| has_job(roberta,nurse)
| has_job(roberta,guard) ),
inference(resolve,[status(thm)],[c_27,c_349]) ).
cnf(c_351,plain,
( has_job(roberta,boxer)
| has_job(roberta,actor)
| has_job(roberta,police)
| has_job(roberta,operator)
| has_job(roberta,guard) ),
inference(resolve,[status(thm)],[c_77,c_350]) ).
cnf(c_352,plain,
( has_job(roberta,boxer)
| has_job(roberta,actor)
| has_job(roberta,police)
| has_job(roberta,guard) ),
inference(resolve,[status(thm)],[c_197,c_351]) ).
cnf(c_353,plain,
( has_job(roberta,boxer)
| has_job(roberta,actor)
| has_job(roberta,guard) ),
inference(resolve,[status(thm)],[c_25,c_352]) ).
cnf(c_354,plain,
( has_job(roberta,boxer)
| has_job(roberta,guard) ),
inference(resolve,[status(thm)],[c_76,c_353]) ).
cnf(c_246,plain,
has_job(roberta,guard),
inference(resolve,[status(thm)],[c_26,c_354]) ).
cnf(c_247,plain,
( ~ has_job(D,boxer)
| ~ has_job(C,actor)
| ~ has_job(B,teacher)
| ~ has_job(A,guard) ),
inference(resolve,[status(thm)],[c_238,c_121]) ).
cnf(c_280,plain,
( ~ has_job(C,boxer)
| ~ has_job(B,actor)
| ~ has_job(A,teacher) ),
inference(resolve,[status(thm)],[c_247,c_246]) ).
cnf(c_355,plain,
( ~ has_job(C,boxer)
| ~ has_job(B,actor)
| ~ has_job(A,teacher) ),
inference(resolve,[status(thm)],[c_247,c_246]) ).
cnf(c_356,plain,
( has_job(steve,teacher)
| has_job(pete,teacher)
| has_job(roberta,teacher)
| ~ has_job(B,boxer)
| ~ has_job(A,actor) ),
inference(resolve,[status(thm)],[c_355,c_29]) ).
cnf(c_357,plain,
( has_job(steve,teacher)
| has_job(pete,teacher)
| has_job(roberta,teacher)
| ~ has_job(A,boxer) ),
inference(resolve,[status(thm)],[c_356,c_185]) ).
cnf(c_358,plain,
( has_job(steve,boxer)
| has_job(pete,boxer)
| has_job(roberta,boxer)
| has_job(steve,teacher)
| has_job(pete,teacher)
| has_job(roberta,teacher) ),
inference(resolve,[status(thm)],[c_357,c_29]) ).
cnf(c_359,plain,
( has_job(steve,boxer)
| has_job(pete,boxer)
| has_job(roberta,boxer)
| has_job(steve,teacher)
| has_job(roberta,teacher) ),
inference(resolve,[status(thm)],[c_22,c_358]) ).
cnf(c_360,plain,
( has_job(steve,boxer)
| has_job(pete,boxer)
| has_job(roberta,boxer)
| has_job(roberta,teacher) ),
inference(resolve,[status(thm)],[c_180,c_359]) ).
cnf(c_361,plain,
( has_job(steve,boxer)
| has_job(pete,boxer)
| has_job(roberta,teacher) ),
inference(resolve,[status(thm)],[c_26,c_360]) ).
cnf(c_362,plain,
( has_job(steve,boxer)
| has_job(roberta,teacher) ),
inference(resolve,[status(thm)],[c_217,c_361]) ).
cnf(c_285,plain,
has_job(roberta,teacher),
inference(resolve,[status(thm)],[c_179,c_362]) ).
cnf(c_287,plain,
( ~ has_job(B,boxer)
| ~ has_job(A,teacher) ),
inference(resolve,[status(thm)],[c_280,c_185]) ).
cnf(c_363,plain,
( has_job(steve,boxer)
| has_job(pete,boxer)
| has_job(roberta,boxer)
| ~ has_job(A,teacher) ),
inference(resolve,[status(thm)],[c_287,c_29]) ).
cnf(c_364,plain,
( has_job(steve,boxer)
| has_job(pete,boxer)
| ~ has_job(A,teacher) ),
inference(resolve,[status(thm)],[c_26,c_363]) ).
cnf(c_365,plain,
( has_job(steve,boxer)
| ~ has_job(A,teacher) ),
inference(resolve,[status(thm)],[c_217,c_364]) ).
cnf(c_289,plain,
~ has_job(A,teacher),
inference(resolve,[status(thm)],[c_179,c_365]) ).
cnf(c_290,plain,
$false,
inference(resolve,[status(thm)],[c_289,c_285]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ019-1 : TPTP v9.3.1. Bugfixed v5.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.34 % Computer : n017.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Sat Sep 26 05:00:49 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.35 % Process 4068846 was started by sandbox2 on n017,
% 0.09/0.35 % Sat Sep 26 05:00:49 2026
% 0.09/0.35 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.36
% 0.09/0.36 % From the command line: assign(max_seconds, 300).
% 0.12/0.46
% 0.12/0.46 % SZS status Unsatisfiable for theBenchmark
% 0.12/0.46
% 0.12/0.46 % Proof 1 at 0.07 (+ 0.03) seconds.
% 0.12/0.46 % Length of proof is 83.
% 0.12/0.46 % Level of proof is 13.
% 0.12/0.46 % Maximum clause weight is 29.000.
% 0.12/0.46 % Given clauses 161.
% 0.12/0.46
% 0.12/0.46 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------