%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PUZ019-1 : TPTP v8.2.0. Bugfixed v5.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 13:42:05 EDT 2024 % Result : Unsatisfiable 58.63s 58.97s % Output : CNFRefutation 58.77s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : PUZ019-1 : TPTP v8.2.0. Bugfixed v5.1.0. % 0.06/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.11/0.32 % Computer : n017.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 300 % 0.11/0.32 % DateTime : Tue Jun 18 10:21:54 EDT 2024 % 0.11/0.33 % CPUTime : % 0.44/0.57 start to proof:theBenchmark % 58.63/58.94 %------------------------------------------- % 58.63/58.94 % File :CSE---1.7 % 58.63/58.94 % Problem :theBenchmark % 58.63/58.94 % Transform :cnf % 58.63/58.94 % Format :tptp:raw % 58.63/58.95 % Command :java -jar mcs_scs.jar %d %s % 58.63/58.95 % 58.63/58.95 % Result :Theorem 58.080000s % 58.63/58.95 % Output :CNFRefutation 58.080000s % 58.63/58.95 %------------------------------------------- % 58.63/58.96 %-------------------------------------------------------------------------- % 58.63/58.96 % File : PUZ019-1 : TPTP v8.2.0. Bugfixed v5.1.0. % 58.63/58.96 % Domain : Puzzles % 58.63/58.96 % Problem : The Jobs Puzzles % 58.63/58.96 % Version : Especial. % 58.63/58.96 % English : There are four people: Roberta, Thelma, Steve, and Pete. Among % 58.63/58.96 % them they hold eight different jobs. Each holds exactly two jobs. % 58.63/58.96 % The jobs are: chef, guard, nurse, telephone operator, police % 58.63/58.96 % officer (either gender), teacher, actor, and boxer. The job of % 58.63/58.96 % a nurse is held by a male. The husband of the chef is the % 58.63/58.96 % telephone operator. Roberta is not a boxer. Pete has no % 58.63/58.96 % education past the ninth grade. Roberta, the chef, and the % 58.63/58.96 % police officer went golfing together. Question : Who holds % 58.63/58.96 % which job? % 58.63/58.96 % 58.63/58.96 % Refs : [WO+92] Wos et al. (1992), Automated Reasoning: Introduction a % 58.63/58.96 % Source : [ANL] % 58.63/58.96 % Names : jobs.ver1.in [ANL] % 58.63/58.96 % 58.63/58.96 % Status : Unsatisfiable % 58.63/58.96 % Rating : 0.00 v5.1.0 % 58.63/58.96 % Syntax : Number of clauses : 64 ( 44 unt; 4 nHn; 59 RR) % 58.63/58.96 % Number of literals : 105 ( 0 equ; 69 neg) % 58.63/58.96 % Maximal clause size : 8 ( 1 avg) % 58.63/58.96 % Maximal term depth : 1 ( 1 avg) % 58.63/58.96 % Number of predicates : 7 ( 7 usr; 0 prp; 1-2 aty) % 58.63/58.96 % Number of functors : 12 ( 12 usr; 12 con; 0-0 aty) % 58.63/58.96 % Number of variables : 40 ( 10 sgn) % 58.63/58.96 % SPC : CNF_UNS_EPR_NEQ_NHN % 58.63/58.96 % 58.63/58.96 % Comments : % 58.63/58.96 % Bugfixes : v1.1.3 - Changed peteacher to pete in clauses roberta_not_pete % 58.63/58.96 % and pete_is_male. % 58.63/58.96 % : v5.1.0 - Adding missing axiom thelma_not_steve % 58.63/58.96 %-------------------------------------------------------------------------- % 58.63/58.96 cnf(reflexivity_for_equal_people,axiom, % 58.63/58.96 equal_people(X,X) ). % 58.63/58.96 % 58.63/58.96 cnf(reflexivity_for_equal_jobs,axiom, % 58.63/58.96 equal_jobs(X,X) ). % 58.63/58.96 % 58.63/58.96 cnf(symmetry_of_equal_people,axiom, % 58.63/58.96 ( ~ equal_people(X,Y) % 58.63/58.96 | equal_people(Y,X) ) ). % 58.63/58.96 % 58.63/58.96 cnf(symmetry_of_equal_jobs,axiom, % 58.63/58.96 ( ~ equal_jobs(X,Y) % 58.63/58.96 | equal_jobs(Y,X) ) ). % 58.63/58.96 % 58.63/58.96 cnf(roberta_not_thelma,axiom, % 58.63/58.96 ~ equal_people(roberta,thelma) ). % 58.63/58.96 % 58.63/58.96 cnf(roberta_not_pete,axiom, % 58.63/58.96 ~ equal_people(roberta,pete) ). % 58.63/58.96 % 58.63/58.96 cnf(roberta_not_steve,axiom, % 58.63/58.96 ~ equal_people(roberta,steve) ). % 58.63/58.96 % 58.63/58.96 cnf(pete_not_thelma,axiom, % 58.63/58.96 ~ equal_people(pete,thelma) ). % 58.63/58.96 % 58.63/58.96 cnf(pete_not_steve,axiom, % 58.63/58.96 ~ equal_people(pete,steve) ). % 58.63/58.96 % 58.63/58.96 cnf(thelma_not_steve,axiom, % 58.63/58.96 ~ equal_people(thelma,steve) ). % 58.63/58.96 % 58.63/58.96 cnf(chef_not_guard,axiom, % 58.63/58.96 ~ equal_jobs(chef,guard) ). % 58.63/58.96 % 58.63/58.96 cnf(chef_not_nurse,axiom, % 58.63/58.96 ~ equal_jobs(chef,nurse) ). % 58.63/58.96 % 58.63/58.96 cnf(chef_not_operator,axiom, % 58.63/58.96 ~ equal_jobs(chef,operator) ). % 58.63/58.96 % 58.63/58.96 cnf(chef_not_police,axiom, % 58.63/58.96 ~ equal_jobs(chef,police) ). % 58.63/58.96 % 58.63/58.96 cnf(chef_not_actor,axiom, % 58.63/58.96 ~ equal_jobs(chef,actor) ). % 58.63/58.96 % 58.63/58.96 cnf(chef_not_boxer,axiom, % 58.63/58.96 ~ equal_jobs(chef,boxer) ). % 58.63/58.96 % 58.63/58.96 cnf(chef_not_teacher,axiom, % 58.63/58.96 ~ equal_jobs(chef,teacher) ). % 58.63/58.96 % 58.63/58.96 cnf(guard_not_nurse,axiom, % 58.63/58.96 ~ equal_jobs(guard,nurse) ). % 58.63/58.96 % 58.63/58.96 cnf(guard_not_operator,axiom, % 58.63/58.96 ~ equal_jobs(guard,operator) ). % 58.63/58.96 % 58.63/58.96 cnf(guard_not_police,axiom, % 58.63/58.96 ~ equal_jobs(guard,police) ). % 58.63/58.96 % 58.63/58.96 cnf(guard_not_actor,axiom, % 58.63/58.96 ~ equal_jobs(guard,actor) ). % 58.63/58.96 % 58.63/58.96 cnf(guard_not_boxer,axiom, % 58.63/58.96 ~ equal_jobs(guard,boxer) ). % 58.63/58.96 % 58.63/58.96 cnf(guard_not_teacher,axiom, % 58.63/58.96 ~ equal_jobs(guard,teacher) ). % 58.63/58.96 % 58.63/58.96 cnf(nurse_not_operator,axiom, % 58.63/58.96 ~ equal_jobs(nurse,operator) ). % 58.63/58.96 % 58.63/58.96 cnf(nurse_not_police,axiom, % 58.63/58.96 ~ equal_jobs(nurse,police) ). % 58.63/58.96 % 58.63/58.96 cnf(nurse_not_actor,axiom, % 58.63/58.96 ~ equal_jobs(nurse,actor) ). % 58.63/58.96 % 58.63/58.96 cnf(nurse_not_boxer,axiom, % 58.63/58.96 ~ equal_jobs(nurse,boxer) ). % 58.63/58.96 % 58.63/58.96 cnf(nurse_not_teacher,axiom, % 58.63/58.96 ~ equal_jobs(nurse,teacher) ). % 58.63/58.96 % 58.63/58.96 cnf(operator_not_police,axiom, % 58.63/58.96 ~ equal_jobs(operator,police) ). % 58.63/58.96 % 58.63/58.96 cnf(operator_not_actor,axiom, % 58.63/58.96 ~ equal_jobs(operator,actor) ). % 58.63/58.96 % 58.63/58.96 cnf(operator_not_boxer,axiom, % 58.63/58.96 ~ equal_jobs(operator,boxer) ). % 58.63/58.96 % 58.63/58.96 cnf(operator_not_teacher,axiom, % 58.63/58.96 ~ equal_jobs(operator,teacher) ). % 58.63/58.96 % 58.63/58.96 cnf(police_not_actor,axiom, % 58.63/58.96 ~ equal_jobs(police,actor) ). % 58.63/58.96 % 58.63/58.96 cnf(police_not_boxer,axiom, % 58.63/58.96 ~ equal_jobs(police,boxer) ). % 58.63/58.96 % 58.63/58.96 cnf(police_not_teacher,axiom, % 58.63/58.96 ~ equal_jobs(police,teacher) ). % 58.63/58.96 % 58.63/58.96 cnf(actor_not_boxer,axiom, % 58.63/58.96 ~ equal_jobs(actor,boxer) ). % 58.63/58.96 % 58.63/58.96 cnf(actor_not_teacher,axiom, % 58.63/58.96 ~ equal_jobs(actor,teacher) ). % 58.63/58.96 % 58.63/58.96 cnf(boxer_not_teacher,axiom, % 58.63/58.96 ~ equal_jobs(boxer,teacher) ). % 58.63/58.96 % 58.63/58.96 cnf(nurse_is_male,axiom, % 58.63/58.96 ( ~ has_job(X,nurse) % 58.63/58.96 | male(X) ) ). % 58.63/58.96 % 58.63/58.96 cnf(actor_is_male,axiom, % 58.63/58.96 ( ~ has_job(X,actor) % 58.63/58.96 | male(X) ) ). % 58.63/58.96 % 58.63/58.96 cnf(chef_is_female,axiom, % 58.63/58.96 ( ~ has_job(X,chef) % 58.63/58.96 | female(X) ) ). % 58.63/58.96 % 58.63/58.96 cnf(nurse_is_educated,axiom, % 58.63/58.96 ( ~ has_job(X,nurse) % 58.63/58.96 | educated(X) ) ). % 58.63/58.96 % 58.63/58.96 cnf(teacher_is_educated,axiom, % 58.63/58.96 ( ~ has_job(X,teacher) % 58.63/58.96 | educated(X) ) ). % 58.63/58.96 % 58.63/58.96 cnf(police_is_educated,axiom, % 58.63/58.96 ( ~ has_job(X,police) % 58.63/58.97 | educated(X) ) ). % 58.63/58.97 % 58.63/58.97 cnf(chef_is_not_also_police,axiom, % 58.63/58.97 ( ~ has_job(X,chef) % 58.63/58.97 | ~ has_job(X,police) ) ). % 58.63/58.97 % 58.63/58.97 cnf(males_are_not_female,axiom, % 58.63/58.97 ( ~ male(X) % 58.63/58.97 | ~ female(X) ) ). % 58.63/58.97 % 58.63/58.97 cnf(everyone_male_or_female,axiom, % 58.63/58.97 ( male(X) % 58.63/58.97 | female(X) ) ). % 58.63/58.97 % 58.63/58.97 cnf(husband_is_male,axiom, % 58.63/58.97 ( ~ husband(X,Y) % 58.63/58.97 | male(Y) ) ). % 58.63/58.97 % 58.63/58.97 cnf(wife_is_female,axiom, % 58.63/58.97 ( ~ husband(X,Y) % 58.63/58.97 | female(X) ) ). % 58.63/58.97 % 58.63/58.97 cnf(husband_of_chef_is_operator1,hypothesis, % 58.63/58.97 ( ~ has_job(X,chef) % 58.63/58.97 | ~ has_job(Y,operator) % 58.63/58.97 | husband(X,Y) ) ). % 58.63/58.97 % 58.63/58.97 cnf(husband_of_chef_is_operator2,hypothesis, % 58.63/58.97 ( ~ has_job(X,chef) % 58.63/58.97 | has_job(Y,operator) % 58.63/58.97 | ~ husband(X,Y) ) ). % 58.63/58.97 % 58.63/58.97 cnf(each_job_held_once,hypothesis, % 58.63/58.97 ( ~ has_job(X,Z) % 58.63/58.97 | ~ has_job(Y,Z) % 58.63/58.97 | equal_people(X,Y) ) ). % 58.63/58.97 % 58.63/58.97 cnf(each_has_maximum_of_two_jobs,hypothesis, % 58.63/58.97 ( ~ has_job(Z,U) % 58.63/58.97 | ~ has_job(Z,X) % 58.63/58.97 | ~ has_job(Z,Y) % 58.63/58.97 | equal_jobs(U,X) % 58.63/58.97 | equal_jobs(U,Y) % 58.63/58.97 | equal_jobs(X,Y) ) ). % 58.63/58.97 % 58.63/58.97 cnf(every_job_is_used,hypothesis, % 58.63/58.97 ( has_job(roberta,X) % 58.63/58.97 | has_job(thelma,X) % 58.63/58.97 | has_job(pete,X) % 58.63/58.97 | has_job(steve,X) ) ). % 58.63/58.97 % 58.63/58.97 cnf(everyone_works,hypothesis, % 58.63/58.97 ( has_job(X,chef) % 58.63/58.97 | has_job(X,guard) % 58.63/58.97 | has_job(X,nurse) % 58.63/58.97 | has_job(X,operator) % 58.63/58.97 | has_job(X,police) % 58.63/58.97 | has_job(X,teacher) % 58.63/58.97 | has_job(X,actor) % 58.63/58.97 | has_job(X,boxer) ) ). % 58.63/58.97 % 58.63/58.97 cnf(pete_is_not_educated,hypothesis, % 58.63/58.97 ~ educated(pete) ). % 58.63/58.97 % 58.63/58.97 cnf(roberta_is_not_chef,hypothesis, % 58.63/58.97 ~ has_job(roberta,chef) ). % 58.63/58.97 % 58.63/58.97 cnf(roberta_is_not_boxer,hypothesis, % 58.63/58.97 ~ has_job(roberta,boxer) ). % 58.63/58.97 % 58.63/58.97 cnf(roberta_is_not_police,hypothesis, % 58.63/58.97 ~ has_job(roberta,police) ). % 58.63/58.97 % 58.63/58.97 cnf(steve_is_male,hypothesis, % 58.63/58.97 male(steve) ). % 58.63/58.97 % 58.63/58.97 cnf(pete_is_male,hypothesis, % 58.63/58.97 male(pete) ). % 58.63/58.97 % 58.63/58.97 cnf(roberta_is_female,hypothesis, % 58.63/58.97 female(roberta) ). % 58.63/58.97 % 58.63/58.97 cnf(thelma_is_female,hypothesis, % 58.63/58.97 female(thelma) ). % 58.63/58.97 % 58.63/58.97 cnf(find_who_has_each_job,negated_conjecture, % 58.63/58.97 ( ~ has_job(X1,chef) % 58.63/58.97 | ~ has_job(X2,guard) % 58.63/58.97 | ~ has_job(X3,nurse) % 58.63/58.97 | ~ has_job(X4,operator) % 58.63/58.97 | ~ has_job(X5,police) % 58.63/58.97 | ~ has_job(X6,teacher) % 58.63/58.97 | ~ has_job(X7,actor) % 58.63/58.97 | ~ has_job(X8,boxer) ) ). % 58.63/58.97 % 58.63/58.97 %-------------------------------------------------------------------------- % 58.63/58.97 %------------------------------------------- % 58.63/58.97 % Proof found % 58.63/58.97 % SZS status Theorem for theBenchmark % 58.63/58.97 % SZS output start Proof % 58.63/58.97 %ClaNum:64(EqnAxiom:0) % 58.63/58.97 %VarNum:82(SingletonVarNum:40) % 58.63/58.97 %MaxLitNum:8 % 58.63/58.97 %MaxfuncDepth:0 % 58.63/58.97 %SharedTerms:54 % 58.63/58.97 %goalClause: 64 % 58.63/58.97 [1]P1(a1) % 58.63/58.97 [2]P1(a8) % 58.63/58.97 [3]P2(a9) % 58.63/58.97 [4]P2(a11) % 58.63/58.97 [7]~P5(a1) % 58.63/58.97 [8]~P3(a9,a11) % 58.63/58.97 [9]~P3(a9,a1) % 58.63/58.97 [10]~P3(a9,a8) % 58.63/58.97 [11]~P3(a11,a8) % 58.63/58.97 [12]~P3(a1,a11) % 58.63/58.97 [13]~P3(a1,a8) % 58.63/58.97 [14]~P4(a2,a5) % 58.63/58.97 [15]~P4(a2,a6) % 58.63/58.97 [16]~P4(a2,a7) % 58.63/58.97 [17]~P4(a2,a10) % 58.63/58.97 [18]~P4(a2,a3) % 58.63/58.97 [19]~P4(a2,a4) % 58.63/58.97 [20]~P4(a2,a12) % 58.63/58.97 [21]~P4(a5,a6) % 58.63/58.97 [22]~P4(a5,a7) % 58.63/58.97 [23]~P4(a5,a10) % 58.63/58.97 [24]~P4(a5,a3) % 58.63/58.97 [25]~P4(a5,a4) % 58.63/58.97 [26]~P4(a5,a12) % 58.63/58.97 [27]~P4(a6,a7) % 58.63/58.97 [28]~P4(a6,a10) % 58.63/58.97 [29]~P4(a6,a3) % 58.63/58.97 [30]~P4(a6,a4) % 58.63/58.97 [31]~P4(a6,a12) % 58.63/58.97 [32]~P4(a7,a10) % 58.63/58.97 [33]~P4(a7,a3) % 58.63/58.97 [34]~P4(a7,a4) % 58.63/58.97 [35]~P4(a7,a12) % 58.63/58.97 [36]~P4(a10,a3) % 58.63/58.97 [37]~P4(a10,a4) % 58.63/58.97 [38]~P4(a10,a12) % 58.63/58.97 [39]~P4(a3,a4) % 58.63/58.97 [40]~P4(a3,a12) % 58.63/58.97 [41]~P4(a4,a12) % 58.63/58.97 [42]~P6(a9,a2) % 58.63/58.97 [43]~P6(a9,a10) % 58.63/58.97 [44]~P6(a9,a4) % 58.63/58.97 [5]P3(x51,x51) % 58.63/58.97 [6]P4(x61,x61) % 58.63/58.97 [45]P2(x451)+P1(x451) % 58.63/58.97 [46]~P2(x461)+~P1(x461) % 58.63/58.97 [47]P1(x471)+~P6(x471,a6) % 58.63/58.97 [48]P1(x481)+~P6(x481,a3) % 58.63/58.97 [49]P2(x491)+~P6(x491,a2) % 58.63/58.97 [50]P5(x501)+~P6(x501,a6) % 58.63/58.97 [51]P5(x511)+~P6(x511,a10) % 58.63/58.97 [52]P5(x521)+~P6(x521,a12) % 58.63/58.97 [57]~P6(x571,a10)+~P6(x571,a2) % 58.63/58.97 [53]P1(x531)+~P7(x532,x531) % 58.63/58.97 [54]P2(x541)+~P7(x541,x542) % 58.63/58.97 [55]~P3(x552,x551)+P3(x551,x552) % 58.63/58.97 [56]~P4(x562,x561)+P4(x561,x562) % 58.63/58.97 [59]P7(x591,x592)+~P6(x592,a7)+~P6(x591,a2) % 58.63/58.97 [60]~P7(x602,x601)+~P6(x602,a2)+P6(x601,a7) % 58.63/58.97 [61]~P6(x611,x613)+P3(x611,x612)+~P6(x612,x613) % 58.63/58.97 [58]P6(a11,x581)+P6(a1,x581)+P6(a8,x581)+P6(a9,x581) % 58.63/58.97 [63]P4(x633,x631)+~P6(x634,x631)+~P6(x634,x633)+P4(x631,x632)+P4(x633,x632)+~P6(x634,x632) % 58.63/58.97 [62]P6(x621,a5)+P6(x621,a6)+P6(x621,a7)+P6(x621,a10)+P6(x621,a3)+P6(x621,a4)+P6(x621,a12)+P6(x621,a2) % 58.63/58.97 [64]~P6(x641,a4)+~P6(x642,a3)+~P6(x643,a12)+~P6(x644,a10)+~P6(x645,a7)+~P6(x646,a6)+~P6(x647,a5)+~P6(x648,a2) % 58.63/58.97 %EqnAxiom % 58.63/58.97 % 58.63/58.97 %------------------------------------------- % 58.63/59.00 cnf(65,plain, % 58.63/59.00 (~P2(a1)), % 58.63/59.00 inference(scs_inference,[],[1,46])). % 58.63/59.00 cnf(75,plain, % 58.63/59.00 (~P3(a1,a9)), % 58.63/59.00 inference(scs_inference,[],[9,15,56,55])). % 58.63/59.00 cnf(93,plain, % 58.63/59.00 (~P4(a4,a2)), % 58.63/59.00 inference(scs_inference,[],[19,56])). % 58.63/59.00 cnf(99,plain, % 58.63/59.00 (~P4(a6,a5)), % 58.63/59.00 inference(scs_inference,[],[21,56])). % 58.63/59.00 cnf(101,plain, % 58.63/59.00 (~P4(a7,a5)), % 58.63/59.00 inference(scs_inference,[],[22,56])). % 58.63/59.00 cnf(103,plain, % 58.63/59.00 (~P4(a10,a5)), % 58.63/59.00 inference(scs_inference,[],[23,56])). % 58.63/59.00 cnf(105,plain, % 58.63/59.00 (~P4(a3,a5)), % 58.63/59.00 inference(scs_inference,[],[24,56])). % 58.63/59.00 cnf(107,plain, % 58.63/59.00 (~P4(a4,a5)), % 58.63/59.00 inference(scs_inference,[],[25,56])). % 58.63/59.00 cnf(111,plain, % 58.63/59.00 (~P4(a7,a6)), % 58.63/59.00 inference(scs_inference,[],[27,56])). % 58.63/59.00 cnf(113,plain, % 58.63/59.00 (~P4(a10,a6)), % 58.63/59.00 inference(scs_inference,[],[28,56])). % 58.63/59.00 cnf(115,plain, % 58.63/59.00 (~P4(a3,a6)), % 58.63/59.00 inference(scs_inference,[],[29,56])). % 58.63/59.00 cnf(117,plain, % 58.63/59.00 (~P4(a4,a6)), % 58.63/59.00 inference(scs_inference,[],[30,56])). % 58.63/59.00 cnf(123,plain, % 58.63/59.00 (~P4(a3,a7)), % 58.63/59.00 inference(scs_inference,[],[33,56])). % 58.63/59.00 cnf(125,plain, % 58.63/59.00 (~P4(a4,a7)), % 58.63/59.00 inference(scs_inference,[],[34,56])). % 58.63/59.00 cnf(129,plain, % 58.63/59.00 (~P4(a3,a10)), % 58.63/59.00 inference(scs_inference,[],[36,56])). % 58.63/59.00 cnf(131,plain, % 58.63/59.00 (~P4(a4,a10)), % 58.63/59.00 inference(scs_inference,[],[37,56])). % 58.63/59.00 cnf(135,plain, % 58.63/59.00 (~P4(a4,a3)), % 58.63/59.00 inference(scs_inference,[],[39,56])). % 58.63/59.00 cnf(141,plain, % 58.63/59.00 (~P6(a9,a6)), % 58.63/59.00 inference(scs_inference,[],[3,47,46])). % 58.63/59.00 cnf(143,plain, % 58.63/59.00 (~P6(a11,a3)), % 58.63/59.00 inference(scs_inference,[],[4,48,46])). % 58.63/59.00 cnf(158,plain, % 58.63/59.00 (~P6(a8,a2)), % 58.63/59.00 inference(scs_inference,[],[2,49,46])). % 58.63/59.00 cnf(174,plain, % 58.63/59.00 (P5(a1)+P6(a8,a6)+P6(a11,a6)), % 58.63/59.00 inference(scs_inference,[],[7,141,50,58])). % 58.63/59.00 cnf(175,plain, % 58.63/59.00 (P6(a8,a6)+P6(a11,a6)), % 58.63/59.00 inference(scs_inference,[],[7,174])). % 58.63/59.00 cnf(193,plain, % 58.63/59.00 (P5(a1)+P6(a8,a10)+P6(a11,a10)), % 58.63/59.00 inference(scs_inference,[],[7,43,51,58])). % 58.63/59.00 cnf(194,plain, % 58.63/59.00 (P6(a8,a10)+P6(a11,a10)), % 58.63/59.00 inference(scs_inference,[],[7,193])). % 58.63/59.00 cnf(243,plain, % 58.63/59.00 (P6(a1,a2)+~P6(a11,a10)), % 58.63/59.00 inference(scs_inference,[],[158,42,57,58])). % 58.63/59.00 cnf(291,plain, % 58.63/59.00 (~P6(a11,a10)), % 58.63/59.00 inference(scs_inference,[],[65,243,49])). % 58.63/59.00 cnf(292,plain, % 58.63/59.00 (P6(a8,a10)), % 58.63/59.00 inference(scs_inference,[],[291,194])). % 58.63/59.00 cnf(294,plain, % 58.63/59.00 (~P6(x2941,a4)+~P6(x2942,a3)+~P6(x2943,a12)+~P6(x2944,a7)+~P6(x2945,a6)+~P6(x2946,a5)+~P6(x2947,a2)), % 58.63/59.00 inference(scs_inference,[],[292,64])). % 58.63/59.00 cnf(331,plain, % 58.63/59.00 (P1(x3311)+~P6(x3311,a7)+~P6(x3312,a2)), % 58.63/59.00 inference(scs_inference,[],[59,53])). % 58.63/59.00 cnf(377,plain, % 58.63/59.00 (~P6(a9,a7)+~P6(x3771,a2)), % 58.63/59.00 inference(scs_inference,[],[3,331,46])). % 58.63/59.00 cnf(423,plain, % 58.63/59.00 (P6(a1,a2)+~P6(a9,a7)), % 58.63/59.00 inference(scs_inference,[],[158,42,377,58])). % 58.63/59.00 cnf(469,plain, % 58.63/59.00 (~P6(a9,a7)), % 58.63/59.00 inference(scs_inference,[],[65,423,49])). % 58.63/59.00 cnf(833,plain, % 58.63/59.00 (~P6(a11,a6)), % 58.63/59.00 inference(scs_inference,[],[4,46,47])). % 58.63/59.00 cnf(834,plain, % 58.63/59.00 (P6(a8,a6)), % 58.63/59.00 inference(scs_inference,[],[833,175])). % 58.63/59.00 cnf(838,plain, % 58.63/59.00 (~P6(x8381,a4)+~P6(x8382,a3)+~P6(x8383,a12)+~P6(x8384,a7)+~P6(x8385,a5)+~P6(x8386,a2)), % 58.63/59.00 inference(scs_inference,[],[834,294])). % 58.63/59.00 cnf(875,plain, % 58.63/59.00 (~P6(a1,a2)), % 58.63/59.00 inference(scs_inference,[],[1,46,49])). % 58.63/59.00 cnf(878,plain, % 58.63/59.00 (P6(a11,a2)), % 58.63/59.00 inference(scs_inference,[],[834,875,158,42,50,58])). % 58.63/59.00 cnf(881,plain, % 58.63/59.00 (P1(x8811)+~P6(x8811,a7)), % 58.63/59.00 inference(scs_inference,[],[878,331])). % 58.63/59.00 cnf(882,plain, % 58.63/59.00 (~P6(x8821,a4)+~P6(x8822,a3)+~P6(x8823,a12)+~P6(x8824,a7)+~P6(x8825,a5)), % 58.63/59.00 inference(scs_inference,[],[878,838])). % 58.63/59.00 cnf(919,plain, % 58.63/59.00 (~P6(a11,a7)), % 58.63/59.00 inference(scs_inference,[],[4,881,46])). % 58.63/59.00 cnf(1193,plain, % 58.63/59.00 (P1(a9)+P6(a1,a3)+P6(a8,a3)), % 58.63/59.00 inference(scs_inference,[],[143,48,58])). % 58.63/59.00 cnf(1239,plain, % 58.63/59.00 (P6(a1,a3)+P6(a8,a3)), % 58.63/59.00 inference(scs_inference,[],[3,1193,46])). % 58.63/59.00 cnf(19823,plain, % 58.63/59.00 (P6(a8,a7)+P6(a1,a7)), % 58.63/59.00 inference(scs_inference,[],[834,469,919,50,58])). % 58.63/59.00 cnf(19825,plain, % 58.63/59.00 (P7(a11,a8)+P6(a1,a7)), % 58.63/59.00 inference(scs_inference,[],[878,834,469,919,50,58,59])). % 58.63/59.00 cnf(19870,plain, % 58.63/59.00 (P7(a11,a1)+P6(a8,a7)), % 58.63/59.00 inference(scs_inference,[],[878,19823,59])). % 58.63/59.00 cnf(54881,plain, % 58.63/59.00 (~P6(a1,a12)), % 58.63/59.00 inference(scs_inference,[],[7,52])). % 58.63/59.00 cnf(54889,plain, % 58.63/59.00 (~P6(a11,a5)+~P6(a11,a4)), % 58.63/59.00 inference(scs_inference,[],[75,93,107,14,7,878,52,51,50,61,63])). % 58.63/59.00 cnf(54891,plain, % 58.63/59.00 (~P6(a8,a5)), % 58.63/59.00 inference(scs_inference,[],[99,103,28,834,292,63])). % 58.63/59.00 cnf(54893,plain, % 58.63/59.00 (P6(a8,a12)+P6(a9,a12)+P6(a11,a12)), % 58.63/59.00 inference(scs_inference,[],[54881,58])). % 58.63/59.00 cnf(54896,plain, % 58.63/59.00 (~P6(a11,a4)+P6(a1,a5)+P6(a9,a5)), % 58.63/59.00 inference(scs_inference,[],[54891,54889,58])). % 58.63/59.00 cnf(54906,plain, % 58.63/59.00 (~P6(a8,a7)), % 58.63/59.00 inference(scs_inference,[],[111,113,32,834,292,63])). % 58.63/59.00 cnf(54909,plain, % 58.63/59.00 (~P7(a11,a8)), % 58.63/59.00 inference(scs_inference,[],[111,113,32,878,834,292,63,19870,60])). % 58.63/59.00 cnf(54912,plain, % 58.63/59.00 (P6(a1,a7)), % 58.63/59.00 inference(scs_inference,[],[54906,19823])). % 58.63/59.00 cnf(54913,plain, % 58.63/59.00 (P6(a1,a7)), % 58.63/59.00 inference(scs_inference,[],[54909,19825])). % 58.63/59.00 cnf(54914,plain, % 58.63/59.00 (~P6(x549141,a4)+~P6(x549142,a3)+~P6(x549143,a12)+~P6(x549144,a5)), % 58.63/59.00 inference(scs_inference,[],[54912,882])). % 58.63/59.00 cnf(54921,plain, % 58.63/59.00 (~P6(a8,a3)), % 58.63/59.00 inference(scs_inference,[],[115,129,28,54881,834,292,58,63])). % 58.63/59.00 cnf(54924,plain, % 58.77/59.00 (P6(a1,a3)), % 58.77/59.00 inference(scs_inference,[],[54921,1239])). % 58.77/59.00 cnf(54926,plain, % 58.77/59.00 (~P6(x549261,a4)+~P6(x549262,a12)+~P6(x549263,a5)), % 58.77/59.00 inference(scs_inference,[],[54924,54914])). % 58.77/59.00 cnf(54927,plain, % 58.77/59.00 (~P6(a1,a4)), % 58.77/59.00 inference(scs_inference,[],[54924,54912,123,125,135,63])). % 58.77/59.00 cnf(54931,plain, % 58.77/59.00 (~P6(a1,a5)), % 58.77/59.00 inference(scs_inference,[],[54913,101,105,54924,123,63])). % 58.77/59.00 cnf(54934,plain, % 58.77/59.00 (P6(a9,a5)+~P6(a11,a4)), % 58.77/59.00 inference(scs_inference,[],[54931,54896])). % 58.77/59.00 cnf(54939,plain, % 58.77/59.00 (~P6(a11,a4)+~P6(x549391,a4)+~P6(x549392,a12)), % 58.77/59.00 inference(scs_inference,[],[54934,54926])). % 58.77/59.00 cnf(54940,plain, % 58.77/59.00 (~P6(a11,a4)+~P6(x549401,a12)), % 58.77/59.00 inference(factoring_inference,[],[54939])). % 58.77/59.00 cnf(54941,plain, % 58.77/59.00 (P6(a8,a4)+P6(a11,a4)), % 58.77/59.00 inference(scs_inference,[],[54927,44,58])). % 58.77/59.00 cnf(54943,plain, % 58.77/59.00 (~P6(a11,a5)+P6(a8,a4)), % 58.77/59.00 inference(scs_inference,[],[54927,44,58,54889])). % 58.77/59.00 cnf(54950,plain, % 58.77/59.00 (P6(a9,a5)), % 58.77/59.00 inference(scs_inference,[],[131,54931,113,117,54891,834,292,63,54943,58])). % 58.77/59.00 cnf(54952,plain, % 58.77/59.00 (P6(a11,a4)), % 58.77/59.00 inference(scs_inference,[],[131,54931,113,117,54891,834,292,63,54943,58,54941])). % 58.77/59.00 cnf(54955,plain, % 58.77/59.00 (~P6(x549551,a12)), % 58.77/59.00 inference(scs_inference,[],[54950,54952,54926])). % 58.77/59.00 cnf(54956,plain, % 58.77/59.00 (~P6(x549561,a12)), % 58.77/59.00 inference(scs_inference,[],[54952,54940])). % 58.77/59.00 cnf(54957,plain, % 58.77/59.00 (P6(a11,a12)), % 58.77/59.00 inference(scs_inference,[],[54955,54956,54893])). % 58.77/59.00 cnf(54962,plain, % 58.77/59.00 ($false), % 58.77/59.00 inference(scs_inference,[],[54957,54955]), % 58.77/59.00 ['proof']). % 58.77/59.03 % SZS output end Proof % 58.77/59.03 % Total time :58.080000s %------------------------------------------------------------------------------