%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : PUZ019-1 : TPTP v9.3.1. Bugfixed v5.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n020.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 : Fri Sep 25 02:32:43 PM UTC 2026
% Result : Unsatisfiable 2.29s 1.20s
% Output : CNFRefutation 2.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 41
% Syntax : Number of formulae : 166 ( 66 unt; 0 def)
% Number of atoms : 384 ( 0 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 453 ( 235 ~; 218 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 15 ( 14 usr; 9 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 12 con; 0-0 aty)
% Number of variables : 95 ( 0 sgn 95 !; 0 ?; 68 :)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X0,X1] :
( equal_jobs(X1,X0)
| ~ equal_jobs(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',symmetry_of_equal_jobs) ).
fof(f11,axiom,
~ equal_jobs(chef,guard),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',chef_not_guard) ).
fof(f16,axiom,
~ equal_jobs(chef,boxer),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',chef_not_boxer) ).
fof(f17,axiom,
~ equal_jobs(chef,teacher),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',chef_not_teacher) ).
fof(f19,axiom,
~ equal_jobs(guard,operator),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',guard_not_operator) ).
fof(f21,axiom,
~ equal_jobs(guard,actor),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',guard_not_actor) ).
fof(f22,axiom,
~ equal_jobs(guard,boxer),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',guard_not_boxer) ).
fof(f24,axiom,
~ equal_jobs(nurse,operator),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nurse_not_operator) ).
fof(f25,axiom,
~ equal_jobs(nurse,police),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nurse_not_police) ).
fof(f26,axiom,
~ equal_jobs(nurse,actor),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nurse_not_actor) ).
fof(f27,axiom,
~ equal_jobs(nurse,boxer),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nurse_not_boxer) ).
fof(f28,axiom,
~ equal_jobs(nurse,teacher),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nurse_not_teacher) ).
fof(f29,axiom,
~ equal_jobs(operator,police),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',operator_not_police) ).
fof(f30,axiom,
~ equal_jobs(operator,actor),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',operator_not_actor) ).
fof(f31,axiom,
~ equal_jobs(operator,boxer),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',operator_not_boxer) ).
fof(f33,axiom,
~ equal_jobs(police,actor),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',police_not_actor) ).
fof(f34,axiom,
~ equal_jobs(police,boxer),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',police_not_boxer) ).
fof(f35,axiom,
~ equal_jobs(police,teacher),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',police_not_teacher) ).
fof(f36,axiom,
~ equal_jobs(actor,boxer),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',actor_not_boxer) ).
fof(f38,axiom,
~ equal_jobs(boxer,teacher),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',boxer_not_teacher) ).
fof(f39,axiom,
! [X0] :
( male(X0)
| ~ has_job(X0,nurse) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nurse_is_male) ).
fof(f40,axiom,
! [X0] :
( male(X0)
| ~ has_job(X0,actor) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',actor_is_male) ).
fof(f41,axiom,
! [X0] :
( female(X0)
| ~ has_job(X0,chef) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',chef_is_female) ).
fof(f42,axiom,
! [X0] :
( educated(X0)
| ~ has_job(X0,nurse) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nurse_is_educated) ).
fof(f43,axiom,
! [X0] :
( educated(X0)
| ~ has_job(X0,teacher) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',teacher_is_educated) ).
fof(f44,axiom,
! [X0] :
( educated(X0)
| ~ has_job(X0,police) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',police_is_educated) ).
fof(f45,axiom,
! [X0] :
( ~ has_job(X0,police)
| ~ has_job(X0,chef) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',chef_is_not_also_police) ).
fof(f46,axiom,
! [X0] :
( ~ female(X0)
| ~ male(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',males_are_not_female) ).
fof(f48,axiom,
! [X0,X1] :
( male(X1)
| ~ husband(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',husband_is_male) ).
fof(f50,axiom,
! [X0,X1] :
( husband(X0,X1)
| ~ has_job(X1,operator)
| ~ has_job(X0,chef) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',husband_of_chef_is_operator1) ).
fof(f53,axiom,
! [X2,X3,X0,X1] :
( equal_jobs(X2,X3)
| equal_jobs(X1,X3)
| equal_jobs(X1,X2)
| ~ has_job(X0,X3)
| ~ has_job(X0,X2)
| ~ has_job(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',each_has_maximum_of_two_jobs) ).
fof(f54,axiom,
! [X0] :
( has_job(steve,X0)
| has_job(pete,X0)
| has_job(thelma,X0)
| has_job(roberta,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_job_is_used) ).
fof(f56,axiom,
~ educated(pete),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',pete_is_not_educated) ).
fof(f57,axiom,
~ has_job(roberta,chef),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',roberta_is_not_chef) ).
fof(f58,axiom,
~ has_job(roberta,boxer),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',roberta_is_not_boxer) ).
fof(f59,axiom,
~ has_job(roberta,police),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',roberta_is_not_police) ).
fof(f60,axiom,
male(steve),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',steve_is_male) ).
fof(f61,axiom,
male(pete),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',pete_is_male) ).
fof(f62,axiom,
female(roberta),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',roberta_is_female) ).
fof(f63,axiom,
female(thelma),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thelma_is_female) ).
fof(f64,negated_conjecture,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ has_job(X7,boxer)
| ~ has_job(X6,actor)
| ~ has_job(X5,teacher)
| ~ has_job(X4,police)
| ~ has_job(X3,operator)
| ~ has_job(X2,nurse)
| ~ has_job(X1,guard)
| ~ has_job(X0,chef) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',find_who_has_each_job) ).
tcf(c_113,plain,
! [X0: $i,X1: $i] :
( husband(X1,X0)
| ~ has_job(X1,chef)
| ~ has_job(X0,operator) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_116,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( equal_jobs(X2,X3)
| equal_jobs(X1,X3)
| equal_jobs(X1,X2)
| ~ has_job(X0,X3)
| ~ has_job(X0,X2)
| ~ has_job(X0,X1) ),
inference(cnf_transformation,[],[f53]) ).
tcf(c_117,plain,
! [X0: $i] :
( has_job(steve,X0)
| has_job(pete,X0)
| has_job(thelma,X0)
| has_job(roberta,X0) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_119,plain,
~ educated(pete),
inference(cnf_transformation,[],[f56]) ).
tcf(c_120,plain,
~ has_job(roberta,chef),
inference(cnf_transformation,[],[f57]) ).
tcf(c_121,plain,
~ has_job(roberta,boxer),
inference(cnf_transformation,[],[f58]) ).
tcf(c_122,plain,
~ has_job(roberta,police),
inference(cnf_transformation,[],[f59]) ).
tcf(c_123,plain,
male(steve),
inference(cnf_transformation,[],[f60]) ).
tcf(c_124,plain,
male(pete),
inference(cnf_transformation,[],[f61]) ).
tcf(c_125,plain,
female(roberta),
inference(cnf_transformation,[],[f62]) ).
tcf(c_126,plain,
female(thelma),
inference(cnf_transformation,[],[f63]) ).
tcf(c_127,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( ~ has_job(X7,chef)
| ~ has_job(X6,boxer)
| ~ has_job(X5,actor)
| ~ has_job(X4,teacher)
| ~ has_job(X3,police)
| ~ has_job(X2,operator)
| ~ has_job(X1,nurse)
| ~ has_job(X0,guard) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_128,plain,
! [X0: $i] :
( ~ has_job(X0,police)
| ~ has_job(X0,chef) ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_129,plain,
~ equal_jobs(chef,teacher),
inference(cnf_transformation,[],[f17]) ).
tcf(c_130,plain,
~ equal_jobs(chef,boxer),
inference(cnf_transformation,[],[f16]) ).
tcf(c_136,plain,
! [X0: $i,X1: $i] :
( male(X1)
| ~ husband(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_138,plain,
~ equal_jobs(operator,boxer),
inference(cnf_transformation,[],[f31]) ).
tcf(c_139,plain,
~ equal_jobs(operator,actor),
inference(cnf_transformation,[],[f30]) ).
tcf(c_140,plain,
~ equal_jobs(operator,police),
inference(cnf_transformation,[],[f29]) ).
tcf(c_141,plain,
~ equal_jobs(nurse,operator),
inference(cnf_transformation,[],[f24]) ).
tcf(c_142,plain,
~ equal_jobs(guard,operator),
inference(cnf_transformation,[],[f19]) ).
tcf(c_146,plain,
! [X0: $i,X1: $i] :
( equal_jobs(X1,X0)
| ~ equal_jobs(X0,X1) ),
inference(cnf_transformation,[],[f4]) ).
tcf(c_154,plain,
~ equal_jobs(guard,boxer),
inference(cnf_transformation,[],[f22]) ).
tcf(c_155,plain,
~ equal_jobs(guard,actor),
inference(cnf_transformation,[],[f21]) ).
tcf(c_158,plain,
~ equal_jobs(chef,guard),
inference(cnf_transformation,[],[f11]) ).
tcf(c_159,plain,
~ equal_jobs(nurse,teacher),
inference(cnf_transformation,[],[f28]) ).
tcf(c_160,plain,
~ equal_jobs(nurse,boxer),
inference(cnf_transformation,[],[f27]) ).
tcf(c_161,plain,
~ equal_jobs(nurse,actor),
inference(cnf_transformation,[],[f26]) ).
tcf(c_162,plain,
~ equal_jobs(nurse,police),
inference(cnf_transformation,[],[f25]) ).
tcf(c_163,plain,
~ equal_jobs(police,teacher),
inference(cnf_transformation,[],[f35]) ).
tcf(c_164,plain,
~ equal_jobs(police,boxer),
inference(cnf_transformation,[],[f34]) ).
tcf(c_165,plain,
~ equal_jobs(police,actor),
inference(cnf_transformation,[],[f33]) ).
tcf(c_166,plain,
! [X0: $i] :
( male(X0)
| ~ has_job(X0,actor) ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_168,plain,
~ equal_jobs(actor,boxer),
inference(cnf_transformation,[],[f36]) ).
tcf(c_169,plain,
~ equal_jobs(boxer,teacher),
inference(cnf_transformation,[],[f38]) ).
tcf(c_170,plain,
! [X0: $i] :
( educated(X0)
| ~ has_job(X0,police) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_171,plain,
! [X0: $i] :
( educated(X0)
| ~ has_job(X0,teacher) ),
inference(cnf_transformation,[],[f43]) ).
tcf(c_172,plain,
! [X0: $i] :
( educated(X0)
| ~ has_job(X0,nurse) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_174,plain,
! [X0: $i] :
( ~ female(X0)
| ~ male(X0) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_175,plain,
! [X0: $i] :
( male(X0)
| ~ has_job(X0,nurse) ),
inference(cnf_transformation,[],[f39]) ).
tcf(c_176,plain,
! [X0: $i] :
( female(X0)
| ~ has_job(X0,chef) ),
inference(cnf_transformation,[],[f41]) ).
tcf(c_192,plain,
( has_job(steve,chef)
| has_job(pete,chef)
| has_job(thelma,chef)
| has_job(roberta,chef) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_195,plain,
! [X0: $i] :
( ~ male(X0)
| ~ female(X0) ),
inference(prop_impl_just,[status(thm)],[c_174]) ).
tcf(c_196,plain,
! [X0: $i] :
( ~ female(X0)
| ~ male(X0) ),
inference(renaming,[status(thm)],[c_195]) ).
tcf(c_203,plain,
! [X0: $i] :
( educated(X0)
| ~ has_job(X0,nurse) ),
inference(prop_impl_just,[status(thm)],[c_172]) ).
tcf(c_205,plain,
! [X0: $i] :
( ~ female(X0)
| ~ has_job(X0,nurse) ),
inference(prop_impl_just,[status(thm)],[c_175,c_174]) ).
tcf(c_207,plain,
! [X0: $i] :
( ~ female(X0)
| ~ has_job(X0,actor) ),
inference(prop_impl_just,[status(thm)],[c_174,c_166]) ).
tcf(c_209,plain,
! [X0: $i] :
( female(X0)
| ~ has_job(X0,chef) ),
inference(prop_impl_just,[status(thm)],[c_176]) ).
tcf(c_217,plain,
! [X0: $i] :
( educated(X0)
| ~ has_job(X0,teacher) ),
inference(prop_impl_just,[status(thm)],[c_171]) ).
tcf(c_221,plain,
! [X0: $i] :
( educated(X0)
| ~ has_job(X0,police) ),
inference(prop_impl_just,[status(thm)],[c_170]) ).
tcf(c_229,plain,
! [X0: $i,X1: $i] :
( male(X1)
| ~ husband(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_136]) ).
tcf(c_549,plain,
~ has_job(pete,police),
inference(resolution,[status(thm)],[c_221,c_119]) ).
tcf(c_553,plain,
~ has_job(pete,teacher),
inference(resolution,[status(thm)],[c_217,c_119]) ).
tcf(c_557,plain,
~ has_job(pete,nurse),
inference(resolution,[status(thm)],[c_203,c_119]) ).
tcf(c_565,plain,
! [X0: $i,X1: $i] :
( ~ female(X1)
| ~ husband(X0,X1) ),
inference(resolution,[status(thm)],[c_196,c_229]) ).
tcf(c_573,plain,
~ female(steve),
inference(resolution,[status(thm)],[c_196,c_123]) ).
tcf(c_577,plain,
~ female(pete),
inference(resolution,[status(thm)],[c_196,c_124]) ).
tcf(c_585,plain,
! [X0: $i,X1: $i] :
( ~ female(X0)
| ~ has_job(X1,chef)
| ~ has_job(X0,operator) ),
inference(resolution,[status(thm)],[c_565,c_113]) ).
tcf(c_601,plain,
! [X0: $i,X1: $i] :
( ~ has_job(X1,chef)
| ~ has_job(X0,operator)
| ~ has_job(X0,chef) ),
inference(resolution,[status(thm)],[c_209,c_585]) ).
tcf(c_628,plain,
! [X0: $i] :
( ~ has_job(roberta,operator)
| ~ has_job(X0,chef) ),
inference(resolution,[status(thm)],[c_585,c_125]) ).
tcf(c_636,plain,
~ has_job(roberta,actor),
inference(resolution,[status(thm)],[c_207,c_125]) ).
tcf(c_640,plain,
~ has_job(roberta,nurse),
inference(resolution,[status(thm)],[c_205,c_125]) ).
tcf(c_644,plain,
! [X0: $i] :
( ~ has_job(thelma,operator)
| ~ has_job(X0,chef) ),
inference(resolution,[status(thm)],[c_585,c_126]) ).
tcf(c_652,plain,
~ has_job(thelma,actor),
inference(resolution,[status(thm)],[c_207,c_126]) ).
tcf(c_656,plain,
~ has_job(thelma,nurse),
inference(resolution,[status(thm)],[c_205,c_126]) ).
tcf(c_660,plain,
~ has_job(steve,chef),
inference(resolution,[status(thm)],[c_209,c_573]) ).
tcf(c_664,plain,
~ has_job(pete,chef),
inference(resolution,[status(thm)],[c_209,c_577]) ).
tcf(c_873,plain,
! [X0: $i] :
( ~ iPr_def_10
| ~ has_job(X0,chef) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_601]) ).
tcf(c_876,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ~ has_job(X0,teacher) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_127]) ).
tcf(c_877,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ~ has_job(X0,police) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_127]) ).
tcf(c_878,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| ~ has_job(X0,actor) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_127]) ).
tcf(c_879,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_15
| ~ has_job(X0,operator) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_15])],[c_127]) ).
tcf(c_880,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_16
| ~ has_job(X0,boxer) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_16])],[c_127]) ).
tcf(c_881,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_17
| ~ has_job(X0,nurse) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_17])],[c_127]) ).
tcf(c_882,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_18
| ~ has_job(X0,guard) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_18])],[c_127]) ).
tcf(c_883,negated_conjecture,
( iPr_def_18
| iPr_def_17
| iPr_def_16
| iPr_def_15
| iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_127]) ).
tcf(c_896,plain,
( ~ iPr_def_10
| ~ has_job(thelma,chef) ),
inference(instantiation,[status(thm)],[c_873]) ).
tcf(c_897,plain,
( ~ has_job(thelma,operator)
| ~ has_job(thelma,chef) ),
inference(instantiation,[status(thm)],[c_644]) ).
tcf(c_898,plain,
( ~ has_job(thelma,chef)
| ~ has_job(roberta,operator) ),
inference(instantiation,[status(thm)],[c_628]) ).
tcf(c_899,plain,
( has_job(steve,police)
| has_job(pete,police)
| has_job(thelma,police)
| has_job(roberta,police) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_900,plain,
( ~ has_job(thelma,police)
| ~ has_job(thelma,chef) ),
inference(instantiation,[status(thm)],[c_128]) ).
tcf(c_901,plain,
( has_job(steve,actor)
| has_job(pete,actor)
| has_job(thelma,actor)
| has_job(roberta,actor) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_902,plain,
( has_job(steve,nurse)
| has_job(pete,nurse)
| has_job(thelma,nurse)
| has_job(roberta,nurse) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_908,plain,
! [X0: $i,X1: $i,X2: $i] :
( equal_jobs(X2,nurse)
| equal_jobs(X1,nurse)
| equal_jobs(X1,X2)
| ~ has_job(X0,nurse)
| ~ has_job(X0,X2)
| ~ has_job(X0,X1) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_909,plain,
! [X0: $i,X1: $i,X2: $i] :
( equal_jobs(X1,X2)
| equal_jobs(X0,X2)
| equal_jobs(X0,X1)
| ~ has_job(thelma,X2)
| ~ has_job(thelma,X1)
| ~ has_job(thelma,X0) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_931,plain,
( equal_jobs(guard,boxer)
| ~ equal_jobs(boxer,guard) ),
inference(instantiation,[status(thm)],[c_146]) ).
tcf(c_933,plain,
( equal_jobs(nurse,operator)
| ~ equal_jobs(operator,nurse) ),
inference(instantiation,[status(thm)],[c_146]) ).
tcf(c_934,plain,
( equal_jobs(nurse,police)
| ~ equal_jobs(police,nurse) ),
inference(instantiation,[status(thm)],[c_146]) ).
tcf(c_935,plain,
( equal_jobs(nurse,actor)
| ~ equal_jobs(actor,nurse) ),
inference(instantiation,[status(thm)],[c_146]) ).
tcf(c_936,plain,
( equal_jobs(nurse,boxer)
| ~ equal_jobs(boxer,nurse) ),
inference(instantiation,[status(thm)],[c_146]) ).
tcf(c_937,plain,
( equal_jobs(nurse,teacher)
| ~ equal_jobs(teacher,nurse) ),
inference(instantiation,[status(thm)],[c_146]) ).
tcf(c_939,plain,
( equal_jobs(operator,actor)
| ~ equal_jobs(actor,operator) ),
inference(instantiation,[status(thm)],[c_146]) ).
tcf(c_940,plain,
( equal_jobs(operator,boxer)
| ~ equal_jobs(boxer,operator) ),
inference(instantiation,[status(thm)],[c_146]) ).
tcf(c_942,plain,
( equal_jobs(police,actor)
| ~ equal_jobs(actor,police) ),
inference(instantiation,[status(thm)],[c_146]) ).
tcf(c_943,plain,
( equal_jobs(police,boxer)
| ~ equal_jobs(boxer,police) ),
inference(instantiation,[status(thm)],[c_146]) ).
tcf(c_944,plain,
( equal_jobs(police,teacher)
| ~ equal_jobs(teacher,police) ),
inference(instantiation,[status(thm)],[c_146]) ).
tcf(c_947,plain,
( equal_jobs(boxer,teacher)
| ~ equal_jobs(teacher,boxer) ),
inference(instantiation,[status(thm)],[c_146]) ).
tcf(c_954,plain,
( has_job(steve,teacher)
| has_job(pete,teacher)
| has_job(thelma,teacher)
| has_job(roberta,teacher) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_955,plain,
( has_job(steve,operator)
| has_job(pete,operator)
| has_job(thelma,operator)
| has_job(roberta,operator) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_960,plain,
! [X0: $i,X1: $i] :
( equal_jobs(X1,actor)
| equal_jobs(X0,actor)
| equal_jobs(X0,X1)
| ~ has_job(pete,actor)
| ~ has_job(pete,X1)
| ~ has_job(pete,X0) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_1025,plain,
! [X0: $i] :
( equal_jobs(police,nurse)
| equal_jobs(X0,police)
| equal_jobs(X0,nurse)
| ~ has_job(steve,police)
| ~ has_job(steve,nurse)
| ~ has_job(steve,X0) ),
inference(instantiation,[status(thm)],[c_908]) ).
tcf(c_1070,plain,
! [X0: $i] :
( equal_jobs(boxer,guard)
| equal_jobs(X0,boxer)
| equal_jobs(X0,guard)
| ~ has_job(thelma,boxer)
| ~ has_job(thelma,guard)
| ~ has_job(thelma,X0) ),
inference(instantiation,[status(thm)],[c_909]) ).
tcf(c_1071,plain,
( equal_jobs(boxer,guard)
| equal_jobs(chef,boxer)
| equal_jobs(chef,guard)
| ~ has_job(thelma,boxer)
| ~ has_job(thelma,guard)
| ~ has_job(thelma,chef) ),
inference(instantiation,[status(thm)],[c_1070]) ).
tcf(c_1088,plain,
! [X0: $i] :
( equal_jobs(teacher,boxer)
| equal_jobs(X0,teacher)
| equal_jobs(X0,boxer)
| ~ has_job(thelma,teacher)
| ~ has_job(thelma,boxer)
| ~ has_job(thelma,X0) ),
inference(instantiation,[status(thm)],[c_909]) ).
tcf(c_1089,plain,
( equal_jobs(teacher,boxer)
| equal_jobs(chef,teacher)
| equal_jobs(chef,boxer)
| ~ has_job(thelma,teacher)
| ~ has_job(thelma,boxer)
| ~ has_job(thelma,chef) ),
inference(instantiation,[status(thm)],[c_1088]) ).
tcf(c_1096,plain,
( ~ iPr_def_12
| ~ has_job(roberta,teacher) ),
inference(instantiation,[status(thm)],[c_876]) ).
tcf(c_1102,plain,
! [X0: $i,X1: $i] :
( equal_jobs(X1,operator)
| equal_jobs(X0,operator)
| equal_jobs(X0,X1)
| ~ has_job(pete,operator)
| ~ has_job(pete,X1)
| ~ has_job(pete,X0) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_1106,plain,
( has_job(steve,guard)
| has_job(pete,guard)
| has_job(thelma,guard)
| has_job(roberta,guard) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_1130,plain,
( has_job(steve,boxer)
| has_job(pete,boxer)
| has_job(thelma,boxer)
| has_job(roberta,boxer) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_1171,plain,
! [X0: $i] :
( equal_jobs(operator,actor)
| equal_jobs(X0,actor)
| equal_jobs(X0,operator)
| ~ has_job(pete,actor)
| ~ has_job(pete,operator)
| ~ has_job(pete,X0) ),
inference(instantiation,[status(thm)],[c_960]) ).
tcf(c_1177,plain,
( ~ iPr_def_13
| ~ has_job(steve,police) ),
inference(instantiation,[status(thm)],[c_877]) ).
tcf(c_1235,plain,
! [X0: $i] :
( equal_jobs(boxer,operator)
| equal_jobs(X0,boxer)
| equal_jobs(X0,operator)
| ~ has_job(pete,boxer)
| ~ has_job(pete,operator)
| ~ has_job(pete,X0) ),
inference(instantiation,[status(thm)],[c_1102]) ).
tcf(c_1245,plain,
( equal_jobs(actor,police)
| equal_jobs(actor,nurse)
| equal_jobs(police,nurse)
| ~ has_job(steve,actor)
| ~ has_job(steve,police)
| ~ has_job(steve,nurse) ),
inference(instantiation,[status(thm)],[c_1025]) ).
tcf(c_1278,plain,
( equal_jobs(operator,actor)
| equal_jobs(guard,actor)
| equal_jobs(guard,operator)
| ~ has_job(pete,actor)
| ~ has_job(pete,operator)
| ~ has_job(pete,guard) ),
inference(instantiation,[status(thm)],[c_1171]) ).
tcf(c_1303,plain,
( equal_jobs(teacher,police)
| equal_jobs(teacher,nurse)
| equal_jobs(police,nurse)
| ~ has_job(steve,teacher)
| ~ has_job(steve,police)
| ~ has_job(steve,nurse) ),
inference(instantiation,[status(thm)],[c_1025]) ).
tcf(c_1311,plain,
( ~ iPr_def_14
| ~ has_job(pete,actor) ),
inference(instantiation,[status(thm)],[c_878]) ).
tcf(c_1316,plain,
( equal_jobs(boxer,operator)
| equal_jobs(actor,boxer)
| equal_jobs(actor,operator)
| ~ has_job(pete,boxer)
| ~ has_job(pete,actor)
| ~ has_job(pete,operator) ),
inference(instantiation,[status(thm)],[c_1235]) ).
tcf(c_1354,plain,
( equal_jobs(police,nurse)
| equal_jobs(operator,police)
| equal_jobs(operator,nurse)
| ~ has_job(steve,police)
| ~ has_job(steve,operator)
| ~ has_job(steve,nurse) ),
inference(instantiation,[status(thm)],[c_1025]) ).
tcf(c_1377,plain,
( ~ iPr_def_15
| ~ has_job(pete,operator) ),
inference(instantiation,[status(thm)],[c_879]) ).
tcf(c_1410,plain,
( equal_jobs(boxer,police)
| equal_jobs(boxer,nurse)
| equal_jobs(police,nurse)
| ~ has_job(steve,boxer)
| ~ has_job(steve,police)
| ~ has_job(steve,nurse) ),
inference(instantiation,[status(thm)],[c_1025]) ).
tcf(c_1448,plain,
( ~ iPr_def_16
| ~ has_job(thelma,boxer) ),
inference(instantiation,[status(thm)],[c_880]) ).
tcf(c_1494,plain,
( ~ iPr_def_17
| ~ has_job(steve,nurse) ),
inference(instantiation,[status(thm)],[c_881]) ).
tcf(c_1514,plain,
( ~ iPr_def_18
| ~ has_job(roberta,guard) ),
inference(instantiation,[status(thm)],[c_882]) ).
tcf(c_1546,plain,
( ~ iPr_def_18
| ~ has_job(steve,guard) ),
inference(instantiation,[status(thm)],[c_882]) ).
tcf(c_1547,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_1546,c_1514,c_1494,c_1448,c_1410,c_1377,c_1354,c_1316,c_1311,c_1303,c_1278,c_1245,c_1177,c_1130,c_1106,c_1096,c_1089,c_1071,c_955,c_954,c_947,c_944,c_943,c_942,c_940,c_939,c_937,c_936,c_935,c_934,c_933,c_931,c_902,c_901,c_900,c_899,c_896,c_897,c_898,c_883,c_664,c_660,c_656,c_652,c_640,c_636,c_557,c_553,c_549,c_192,c_120,c_121,c_122,c_129,c_130,c_138,c_139,c_140,c_141,c_142,c_154,c_155,c_158,c_159,c_160,c_161,c_162,c_163,c_164,c_165,c_168,c_169]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ019-1 : TPTP v9.3.1. Bugfixed v5.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.08/0.35 % Computer : n020.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Thu Sep 24 06:41:03 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/0.39 Running EPR theorem proving
% 0.12/0.39 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s epr_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.40
% 0.12/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.40
% 0.12/0.40 % Detected problem language: tptp
% 0.12/0.42 % Proving...
% 2.29/1.20 % SZS status Started for theBenchmark.p
% 2.29/1.20 % SZS status Unsatisfiable for theBenchmark.p
% 2.29/1.20
% 2.29/1.20 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.29/1.20
% 2.29/1.20 % ------ iProver source info
% 2.29/1.20
% 2.29/1.20 % git: date: 2026-07-19 20:42:38 +0200
% 2.29/1.20 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.29/1.20 % git: non_committed_changes: false
% 2.29/1.20
% 2.29/1.20 % ------ Parsing...% successful
% 2.29/1.20
% 2.29/1.20
% 2.29/1.20 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Option_epr_non_horn_non_eq
% 2.29/1.20 %
% 2.29/1.20
% 2.29/1.20 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 2.29/1.20
% 2.29/1.20 % ------ Preprocessing...% ------ preprocesses with Option_epr_non_horn_non_eq
% 2.29/1.20 gs_s sp: 10 0s gs_e snvd_s sp: 0 0s snvd_e
% 2.29/1.20 % ------ Proving...
% 2.29/1.20 % ------ Problem Properties
% 2.29/1.20
% 2.29/1.20 %
% 2.29/1.20 % clauses 70
% 2.29/1.20 % conjectures 8
% 2.29/1.20 % EPR 70
% 2.29/1.20 % Horn 65
% 2.29/1.20 % unary 48
% 2.29/1.20 % binary 16
% 2.29/1.20 % lits 112
% 2.29/1.20 % lits eq 0
% 2.29/1.20 % fd_pure 0
% 2.29/1.20 % fd_pseudo 0
% 2.29/1.20 % fd_cond 0
% 2.29/1.20 % fd_pseudo_cond 0
% 2.29/1.20 % AC symbols 0
% 2.29/1.20
% 2.29/1.20 % ------ Schedule EPR non Horn non eq is on
% 2.29/1.20
% 2.29/1.20 % ------ no equalities: superposition off
% 2.29/1.20
% 2.29/1.20 % ------ Input Options "--resolution_flag false" Time Limit: 70.
% 2.29/1.20
% 2.29/1.20
% 2.29/1.20 % ------
% 2.29/1.20 % Current options:
% 2.29/1.20 % ------
% 2.29/1.20
% 2.29/1.20
% 2.29/1.20 %
% 2.29/1.20
% 2.29/1.20 % ------ Proving...
% 2.29/1.20 %
% 2.29/1.20
% 2.29/1.20 % SZS status Unsatisfiable for theBenchmark.p
% 2.29/1.20
% 2.29/1.20 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 2.29/1.20
% 2.29/1.20
%------------------------------------------------------------------------------