%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP126-3.004 : TPTP v8.2.0. Released v1.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n018.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 06:38:52 EDT 2024 % Result : Unsatisfiable 68.10s 68.33s % Output : CNFRefutation 68.68s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : GRP126-3.004 : TPTP v8.2.0. Released v1.2.0. % 0.04/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n018.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Thu Jun 20 08:35:08 EDT 2024 % 0.12/0.33 % CPUTime : % 0.52/0.56 start to proof:theBenchmark % 68.10/68.30 %------------------------------------------- % 68.10/68.30 % File :CSE---1.7 % 68.10/68.30 % Problem :theBenchmark % 68.10/68.30 % Transform :cnf % 68.10/68.30 % Format :tptp:raw % 68.10/68.30 % Command :java -jar mcs_scs.jar %d %s % 68.10/68.30 % 68.10/68.30 % Result :Theorem 67.590000s % 68.10/68.30 % Output :CNFRefutation 67.590000s % 68.10/68.30 %------------------------------------------- % 68.10/68.32 %-------------------------------------------------------------------------- % 68.10/68.32 % File : GRP126-3.004 : TPTP v8.2.0. Released v1.2.0. % 68.10/68.32 % Domain : Group Theory (Quasigroups) % 68.10/68.32 % Problem : (a.b).(b.a) = b % 68.10/68.32 % Version : [Sla93] axioms : Augmented. % 68.10/68.32 % English : Generate the multiplication table for the specified quasi- % 68.10/68.32 % group with 4 elements. % 68.10/68.32 % 68.10/68.32 % Refs : [FSB93] Fujita et al. (1993), Automatic Generation of Some Res % 68.10/68.32 % : [Sla93] Slaney (1993), Email to G. Sutcliffe % 68.10/68.32 % : [SFS95] Slaney et al. (1995), Automated Reasoning and Exhausti % 68.10/68.32 % Source : [TPTP] % 68.10/68.32 % Names : % 68.10/68.32 % 68.10/68.32 % Status : Unsatisfiable % 68.10/68.32 % Rating : 0.00 v2.4.0, 0.00 v2.1.0 % 68.10/68.32 % Syntax : Number of clauses : 43 ( 32 unt; 2 nHn; 42 RR) % 68.10/68.32 % Number of literals : 78 ( 0 equ; 43 neg) % 68.10/68.32 % Maximal clause size : 6 ( 1 avg) % 68.10/68.32 % Maximal term depth : 1 ( 1 avg) % 68.10/68.32 % Number of predicates : 6 ( 6 usr; 0 prp; 1-3 aty) % 68.10/68.32 % Number of functors : 5 ( 5 usr; 5 con; 0-0 aty) % 68.10/68.32 % Number of variables : 39 ( 0 sgn) % 68.10/68.32 % SPC : CNF_UNS_EPR_NEQ_NHN % 68.10/68.32 % 68.10/68.32 % Comments : [SFS93]'s axiomatization has been modified for this. % 68.10/68.32 % : Substitution axioms are not needed, as any positive equality % 68.10/68.32 % literals should resolve on negative ones directly. % 68.10/68.32 % : Version 3 has complex isomorphism avoidance (mentioned in % 68.10/68.32 % [SFS95] % 68.10/68.32 % : tptp2X: -f tptp -s4 GRP126-3.g % 68.10/68.32 %-------------------------------------------------------------------------- % 68.10/68.32 cnf(e_0_then_e_1,axiom, % 68.10/68.32 next(e_0,e_1) ). % 68.10/68.32 % 68.10/68.32 cnf(e_1_then_e_2,axiom, % 68.10/68.32 next(e_1,e_2) ). % 68.10/68.32 % 68.10/68.32 cnf(e_2_then_e_3,axiom, % 68.10/68.32 next(e_2,e_3) ). % 68.10/68.32 % 68.10/68.32 cnf(e_3_then_e_4,axiom, % 68.10/68.32 next(e_3,e_4) ). % 68.10/68.32 % 68.10/68.32 cnf(e_1_greater_e_0,axiom, % 68.10/68.32 greater(e_1,e_0) ). % 68.10/68.32 % 68.10/68.32 cnf(e_2_greater_e_0,axiom, % 68.10/68.32 greater(e_2,e_0) ). % 68.10/68.32 % 68.10/68.32 cnf(e_3_greater_e_0,axiom, % 68.10/68.32 greater(e_3,e_0) ). % 68.10/68.32 % 68.10/68.32 cnf(e_4_greater_e_0,axiom, % 68.10/68.32 greater(e_4,e_0) ). % 68.10/68.32 % 68.10/68.32 cnf(e_2_greater_e_1,axiom, % 68.10/68.32 greater(e_2,e_1) ). % 68.10/68.32 % 68.10/68.32 cnf(e_3_greater_e_1,axiom, % 68.10/68.32 greater(e_3,e_1) ). % 68.10/68.32 % 68.10/68.32 cnf(e_4_greater_e_1,axiom, % 68.10/68.32 greater(e_4,e_1) ). % 68.10/68.32 % 68.10/68.32 cnf(e_3_greater_e_2,axiom, % 68.10/68.32 greater(e_3,e_2) ). % 68.10/68.32 % 68.10/68.32 cnf(e_4_greater_e_2,axiom, % 68.10/68.32 greater(e_4,e_2) ). % 68.10/68.32 % 68.10/68.32 cnf(e_4_greater_e_3,axiom, % 68.10/68.32 greater(e_4,e_3) ). % 68.10/68.32 % 68.10/68.32 cnf(cycle1,axiom, % 68.10/68.32 ( ~ cycle(X,Y) % 68.10/68.32 | ~ cycle(X,Z) % 68.10/68.32 | equalish(Y,Z) ) ). % 68.10/68.32 % 68.10/68.32 cnf(cycle2,axiom, % 68.10/68.32 ( ~ group_element(X) % 68.10/68.32 | cycle(X,e_0) % 68.10/68.32 | cycle(X,e_1) % 68.10/68.32 | cycle(X,e_2) % 68.10/68.32 | cycle(X,e_3) ) ). % 68.10/68.32 % 68.10/68.32 cnf(cycle3,axiom, % 68.10/68.32 cycle(e_4,e_0) ). % 68.10/68.32 % 68.10/68.32 cnf(cycle4,axiom, % 68.10/68.32 ( ~ cycle(X,Y) % 68.10/68.32 | ~ cycle(W,Z) % 68.10/68.32 | ~ next(X,W) % 68.10/68.32 | ~ greater(Y,e_0) % 68.10/68.32 | ~ next(Z,Z1) % 68.10/68.32 | equalish(Y,Z1) ) ). % 68.10/68.32 % 68.10/68.32 cnf(cycle5,axiom, % 68.10/68.32 ( ~ cycle(X,Z1) % 68.10/68.32 | ~ cycle(Y,e_0) % 68.10/68.32 | ~ cycle(W,Z2) % 68.10/68.32 | ~ next(Y,W) % 68.10/68.32 | ~ greater(Y,X) % 68.10/68.32 | ~ greater(Z1,Z2) ) ). % 68.10/68.32 % 68.10/68.32 cnf(cycle6,axiom, % 68.10/68.32 ( ~ cycle(X,e_0) % 68.10/68.32 | ~ product(X,e_1,Y) % 68.10/68.32 | ~ greater(Y,X) ) ). % 68.10/68.32 % 68.10/68.32 cnf(cycle7,axiom, % 68.10/68.32 ( ~ cycle(X,Y) % 68.10/68.32 | ~ product(X,e_1,Z) % 68.10/68.32 | ~ greater(Y,e_0) % 68.10/68.32 | ~ next(X,X1) % 68.10/68.32 | equalish(Z,X1) ) ). % 68.10/68.32 % 68.10/68.32 cnf(element_1,axiom, % 68.10/68.32 group_element(e_1) ). % 68.10/68.32 % 68.10/68.32 cnf(element_2,axiom, % 68.10/68.32 group_element(e_2) ). % 68.10/68.32 % 68.10/68.32 cnf(element_3,axiom, % 68.10/68.32 group_element(e_3) ). % 68.10/68.32 % 68.10/68.32 cnf(element_4,axiom, % 68.10/68.32 group_element(e_4) ). % 68.10/68.32 % 68.10/68.32 cnf(e_1_is_not_e_2,axiom, % 68.10/68.32 ~ equalish(e_1,e_2) ). % 68.10/68.32 % 68.10/68.32 cnf(e_1_is_not_e_3,axiom, % 68.10/68.32 ~ equalish(e_1,e_3) ). % 68.10/68.32 % 68.10/68.32 cnf(e_1_is_not_e_4,axiom, % 68.10/68.32 ~ equalish(e_1,e_4) ). % 68.10/68.32 % 68.10/68.32 cnf(e_2_is_not_e_1,axiom, % 68.10/68.32 ~ equalish(e_2,e_1) ). % 68.10/68.32 % 68.10/68.32 cnf(e_2_is_not_e_3,axiom, % 68.10/68.32 ~ equalish(e_2,e_3) ). % 68.10/68.32 % 68.10/68.32 cnf(e_2_is_not_e_4,axiom, % 68.10/68.32 ~ equalish(e_2,e_4) ). % 68.10/68.32 % 68.10/68.32 cnf(e_3_is_not_e_1,axiom, % 68.10/68.32 ~ equalish(e_3,e_1) ). % 68.10/68.32 % 68.10/68.32 cnf(e_3_is_not_e_2,axiom, % 68.10/68.32 ~ equalish(e_3,e_2) ). % 68.10/68.32 % 68.10/68.32 cnf(e_3_is_not_e_4,axiom, % 68.10/68.32 ~ equalish(e_3,e_4) ). % 68.10/68.32 % 68.10/68.32 cnf(e_4_is_not_e_1,axiom, % 68.10/68.32 ~ equalish(e_4,e_1) ). % 68.10/68.32 % 68.10/68.32 cnf(e_4_is_not_e_2,axiom, % 68.10/68.32 ~ equalish(e_4,e_2) ). % 68.10/68.33 % 68.10/68.33 cnf(e_4_is_not_e_3,axiom, % 68.10/68.33 ~ equalish(e_4,e_3) ). % 68.10/68.33 % 68.10/68.33 cnf(product_total_function1,axiom, % 68.10/68.33 ( ~ group_element(X) % 68.10/68.33 | ~ group_element(Y) % 68.10/68.33 | product(X,Y,e_1) % 68.10/68.33 | product(X,Y,e_2) % 68.10/68.33 | product(X,Y,e_3) % 68.10/68.33 | product(X,Y,e_4) ) ). % 68.10/68.33 % 68.10/68.33 cnf(product_total_function2,axiom, % 68.10/68.33 ( ~ product(X,Y,W) % 68.10/68.33 | ~ product(X,Y,Z) % 68.10/68.33 | equalish(W,Z) ) ). % 68.10/68.33 % 68.10/68.33 cnf(product_right_cancellation,axiom, % 68.10/68.33 ( ~ product(X,W,Y) % 68.10/68.33 | ~ product(X,Z,Y) % 68.10/68.33 | equalish(W,Z) ) ). % 68.10/68.33 % 68.10/68.33 cnf(product_left_cancellation,axiom, % 68.10/68.33 ( ~ product(W,Y,X) % 68.10/68.33 | ~ product(Z,Y,X) % 68.10/68.33 | equalish(W,Z) ) ). % 68.10/68.33 % 68.10/68.33 cnf(product_idempotence,axiom, % 68.10/68.33 product(X,X,X) ). % 68.10/68.33 % 68.10/68.33 cnf(qg4,negated_conjecture, % 68.10/68.33 ( ~ product(X,Y,Z1) % 68.10/68.33 | ~ product(Y,X,Z2) % 68.10/68.33 | product(Z1,Z2,Y) ) ). % 68.10/68.33 % 68.10/68.33 %-------------------------------------------------------------------------- % 68.10/68.33 %------------------------------------------- % 68.10/68.33 % Proof found % 68.10/68.33 % SZS status Theorem for theBenchmark % 68.10/68.33 % SZS output start Proof % 68.10/68.33 %ClaNum:43(EqnAxiom:0) % 68.10/68.33 %VarNum:93(SingletonVarNum:39) % 68.10/68.33 %MaxLitNum:6 % 68.10/68.33 %MaxfuncDepth:0 % 68.10/68.33 %SharedTerms:36 % 68.10/68.33 %goalClause: 42 % 68.10/68.33 [1]P1(a1) % 68.10/68.33 [2]P1(a3) % 68.10/68.33 [3]P1(a4) % 68.10/68.33 [4]P1(a5) % 68.10/68.33 [5]P5(a2,a1) % 68.10/68.33 [6]P5(a1,a3) % 68.10/68.33 [7]P5(a3,a4) % 68.10/68.33 [8]P5(a4,a5) % 68.10/68.33 [9]P2(a1,a2) % 68.10/68.33 [10]P2(a3,a2) % 68.10/68.33 [11]P2(a3,a1) % 68.10/68.33 [12]P2(a4,a2) % 68.10/68.33 [13]P2(a4,a1) % 68.10/68.33 [14]P2(a4,a3) % 68.10/68.33 [15]P2(a5,a2) % 68.10/68.33 [16]P2(a5,a1) % 68.10/68.33 [17]P2(a5,a3) % 68.10/68.33 [18]P2(a5,a4) % 68.10/68.33 [19]P3(a5,a2) % 68.10/68.33 [21]~P4(a1,a3) % 68.10/68.33 [22]~P4(a1,a4) % 68.10/68.33 [23]~P4(a1,a5) % 68.10/68.33 [24]~P4(a3,a1) % 68.10/68.33 [25]~P4(a3,a4) % 68.10/68.33 [26]~P4(a3,a5) % 68.10/68.33 [27]~P4(a4,a1) % 68.10/68.33 [28]~P4(a4,a3) % 68.10/68.33 [29]~P4(a4,a5) % 68.10/68.33 [30]~P4(a5,a1) % 68.10/68.33 [31]~P4(a5,a3) % 68.10/68.34 [32]~P4(a5,a4) % 68.10/68.34 [20]P6(x201,x201,x201) % 68.10/68.34 [36]~P2(x361,x362)+~P6(x362,a1,x361)+~P3(x362,a2) % 68.10/68.34 [34]~P3(x343,x341)+P4(x341,x342)+~P3(x343,x342) % 68.10/68.34 [39]~P6(x393,x394,x391)+P4(x391,x392)+~P6(x393,x394,x392) % 68.10/68.34 [40]~P6(x403,x401,x404)+P4(x401,x402)+~P6(x403,x402,x404) % 68.10/68.34 [41]~P6(x411,x413,x414)+P4(x411,x412)+~P6(x412,x413,x414) % 68.10/68.34 [42]~P6(x424,x423,x421)+P6(x421,x422,x423)+~P6(x423,x424,x422) % 68.10/68.34 [33]~P1(x331)+P3(x331,a1)+P3(x331,a3)+P3(x331,a4)+P3(x331,a2) % 68.10/68.34 [38]P4(x381,x382)+~P5(x383,x382)+~P3(x383,x384)+~P6(x383,a1,x381)+~P2(x384,a2) % 68.10/68.34 [43]~P1(x432)+~P1(x431)+P6(x431,x432,a3)+P6(x431,x432,a4)+P6(x431,x432,a5)+P6(x431,x432,a1) % 68.10/68.34 [35]~P3(x355,x353)+~P3(x354,x351)+P4(x351,x352)+~P5(x353,x352)+~P5(x354,x355)+~P2(x351,a2) % 68.10/68.34 [37]~P3(x372,x375)+~P3(x373,x374)+~P5(x371,x372)+~P2(x371,x373)+~P2(x374,x375)+~P3(x371,a2) % 68.10/68.34 %EqnAxiom % 68.10/68.34 % 68.10/68.34 %------------------------------------------- % 68.47/68.61 cnf(46,plain, % 68.47/68.61 (~P3(a1,a1)), % 68.47/68.61 inference(scs_inference,[],[20,9,6,21,39,38])). % 68.47/68.61 cnf(77,plain, % 68.47/68.61 (P3(a1,a3)+P3(a1,a2)), % 68.47/68.61 inference(scs_inference,[],[1,20,46,12,19,6,21,40,38,36,33])). % 68.47/68.61 cnf(359,plain, % 68.47/68.61 (P3(a1,a2)), % 68.47/68.61 inference(scs_inference,[],[20,10,21,6,41,38,77])). % 68.47/68.61 cnf(415774,plain, % 68.47/68.61 (P6(x4157741,x4157741,x4157741)), % 68.47/68.61 inference(rename_variables,[],[20])). % 68.47/68.61 cnf(415777,plain, % 68.47/68.61 (P6(x4157771,x4157771,x4157771)), % 68.47/68.61 inference(rename_variables,[],[20])). % 68.47/68.61 cnf(415786,plain, % 68.47/68.61 (~P6(a3,x4157861,a4)+~P6(x4157861,a3,a4)), % 68.47/68.61 inference(scs_inference,[],[28,13,359,20,415774,415777,41,40,34,39,36,42])). % 68.47/68.61 cnf(415792,plain, % 68.47/68.61 (P6(x4157921,x4157921,x4157921)), % 68.47/68.61 inference(rename_variables,[],[20])). % 68.47/68.61 cnf(415795,plain, % 68.47/68.61 (P6(x4157951,x4157951,x4157951)), % 68.47/68.61 inference(rename_variables,[],[20])). % 68.47/68.61 cnf(415797,plain, % 68.47/68.61 (~P6(a3,a3,a4)), % 68.47/68.61 inference(scs_inference,[],[25,20,415792,415795,41,40,39])). % 68.47/68.61 cnf(415798,plain, % 68.47/68.61 (P6(x4157981,x4157981,x4157981)), % 68.47/68.61 inference(rename_variables,[],[20])). % 68.47/68.61 cnf(415801,plain, % 68.47/68.61 (P6(x4158011,x4158011,x4158011)), % 68.47/68.61 inference(rename_variables,[],[20])). % 68.47/68.61 cnf(415808,plain, % 68.47/68.61 (~P3(a4,a3)), % 68.47/68.61 inference(scs_inference,[],[25,24,10,359,21,8,6,20,415792,415795,415798,415801,5,19,41,40,39,36,38,34,35])). % 68.47/68.61 cnf(415812,plain, % 68.47/68.61 (~P6(a5,a3,a3)), % 68.47/68.61 inference(scs_inference,[],[26,20,41])). % 68.47/68.61 cnf(415813,plain, % 68.47/68.61 (P6(x4158131,x4158131,x4158131)), % 68.47/68.61 inference(rename_variables,[],[20])). % 68.47/68.61 cnf(415815,plain, % 68.47/68.61 (~P6(a3,a5,a3)), % 68.47/68.61 inference(scs_inference,[],[26,20,415813,41,40])). % 68.47/68.61 cnf(415816,plain, % 68.47/68.61 (P6(x4158161,x4158161,x4158161)), % 68.47/68.61 inference(rename_variables,[],[20])). % 68.47/68.61 cnf(415823,plain, % 68.47/68.61 (~P6(a1,a1,a3)), % 68.47/68.61 inference(scs_inference,[],[26,359,11,20,415813,415816,41,40,34,39,36])). % 68.47/68.61 cnf(415830,plain, % 68.47/68.61 (~P6(a1,a4,a4)), % 68.47/68.61 inference(scs_inference,[],[27,20,41])). % 68.47/68.61 cnf(415831,plain, % 68.47/68.61 (P6(x4158311,x4158311,x4158311)), % 68.47/68.61 inference(rename_variables,[],[20])). % 68.47/68.61 cnf(415833,plain, % 68.47/68.61 (~P6(a4,a1,a4)), % 68.47/68.61 inference(scs_inference,[],[27,20,415831,41,40])). % 68.47/68.61 cnf(415845,plain, % 68.47/68.61 (~P6(a1,a3,a3)), % 68.47/68.61 inference(scs_inference,[],[24,20,41])). % 68.47/68.61 cnf(415846,plain, % 68.47/68.61 (P6(x4158461,x4158461,x4158461)), % 68.47/68.61 inference(rename_variables,[],[20])). % 68.47/68.61 cnf(415850,plain, % 68.47/68.61 (~P6(a3,a1,a3)), % 68.47/68.61 inference(scs_inference,[],[24,359,20,415846,41,34,40])). % 68.47/68.61 cnf(415851,plain, % 68.47/68.61 (P6(x4158511,x4158511,x4158511)), % 68.47/68.61 inference(rename_variables,[],[20])). % 68.47/68.61 cnf(415853,plain, % 68.47/68.61 (~P6(a3,a3,a1)), % 68.47/68.61 inference(scs_inference,[],[24,359,20,415846,415851,41,34,40,39])). % 68.47/68.61 cnf(415863,plain, % 68.47/68.61 (P6(x4158631,x4158631,x4158631)), % 68.47/68.61 inference(rename_variables,[],[20])). % 68.47/68.61 cnf(415866,plain, % 68.47/68.61 (P6(x4158661,x4158661,x4158661)), % 68.47/68.61 inference(rename_variables,[],[20])). % 68.47/68.61 cnf(415868,plain, % 68.47/68.61 (~P6(a4,a4,a5)), % 68.47/68.61 inference(scs_inference,[],[29,20,415863,415866,41,40,39])). % 68.47/68.61 cnf(415869,plain, % 68.47/68.61 (P6(x4158691,x4158691,x4158691)), % 68.47/68.61 inference(rename_variables,[],[20])). % 68.47/68.61 cnf(415876,plain, % 68.47/68.61 (~P3(a3,a4)+~P3(a4,a2)), % 68.47/68.61 inference(scs_inference,[],[29,14,12,359,8,20,415863,415866,415869,19,41,40,39,36,34,37])). % 68.47/68.61 cnf(415880,plain, % 68.47/68.61 (~P6(a3,a5,a5)), % 68.47/68.61 inference(scs_inference,[],[31,359,20,34,41])). % 68.47/68.61 cnf(415881,plain, % 68.47/68.61 (P6(x4158811,x4158811,x4158811)), % 68.47/68.61 inference(rename_variables,[],[20])). % 68.47/68.61 cnf(415883,plain, % 68.47/68.61 (~P6(a5,a3,a5)), % 68.47/68.61 inference(scs_inference,[],[31,359,20,415881,34,41,40])). % 68.47/68.61 cnf(415884,plain, % 68.47/68.61 (P6(x4158841,x4158841,x4158841)), % 68.47/68.61 inference(rename_variables,[],[20])). % 68.47/68.61 cnf(415886,plain, % 68.47/68.61 (~P6(a5,a5,a3)), % 68.47/68.61 inference(scs_inference,[],[31,359,20,415881,415884,34,41,40,39])). % 68.47/68.61 cnf(415901,plain, % 68.47/68.61 (~P6(a3,a1,a4)+~P3(a3,a2)), % 68.47/68.61 inference(scs_inference,[],[26,14,359,21,6,20,38,34,36])). % 68.47/68.61 cnf(415908,plain, % 68.47/68.61 (~P6(a4,x4159081,a3)+~P6(x4159081,a4,a3)), % 68.47/68.61 inference(scs_inference,[],[415797,359,20,34,36,42])). % 68.47/68.61 cnf(415920,plain, % 68.47/68.61 (P6(x4159201,x4159201,x4159201)), % 68.47/68.61 inference(rename_variables,[],[20])). % 68.47/68.61 cnf(415923,plain, % 68.47/68.61 (P6(x4159231,x4159231,x4159231)), % 68.47/68.61 inference(rename_variables,[],[20])). % 68.47/68.61 cnf(415925,plain, % 68.47/68.61 (~P6(a1,a5,a1)), % 68.47/68.61 inference(scs_inference,[],[359,23,20,415920,415923,34,36,41,40])). % 68.47/68.61 cnf(415926,plain, % 68.47/68.61 (P6(x4159261,x4159261,x4159261)), % 68.47/68.61 inference(rename_variables,[],[20])). % 68.47/68.61 cnf(415928,plain, % 68.47/68.61 (~P6(a5,a5,a4)), % 68.47/68.61 inference(scs_inference,[],[359,23,32,20,415920,415923,415926,34,36,41,40,39])). % 68.47/68.61 cnf(415939,plain, % 68.47/68.61 (~P3(a4,a4)), % 68.47/68.61 inference(scs_inference,[],[27,12,359,21,8,6,20,5,19,38,35])). % 68.47/68.61 cnf(415948,plain, % 68.47/68.61 (P6(x4159481,x4159481,x4159481)), % 68.47/68.61 inference(rename_variables,[],[20])). % 68.47/68.61 cnf(415955,plain, % 68.47/68.61 (~P6(a3,a5,a1)+P6(a5,a3,a4)), % 68.47/68.61 inference(scs_inference,[],[415823,415812,415883,2,359,21,4,6,20,415948,34,36,38,42,43])). % 68.47/68.61 cnf(415965,plain, % 68.47/68.61 (P6(x4159651,x4159651,x4159651)), % 68.47/68.61 inference(rename_variables,[],[20])). % 68.47/68.61 cnf(415967,plain, % 68.47/68.61 (~P6(a4,a1,a1)), % 68.47/68.61 inference(scs_inference,[],[359,22,20,415965,34,36,41])). % 68.47/68.61 cnf(415968,plain, % 68.47/68.61 (P6(x4159681,x4159681,x4159681)), % 68.47/68.61 inference(rename_variables,[],[20])). % 68.47/68.61 cnf(415970,plain, % 68.47/68.61 (~P6(a5,a5,a1)), % 68.47/68.61 inference(scs_inference,[],[359,22,20,415965,415968,30,34,36,41,39])). % 68.47/68.61 cnf(415971,plain, % 68.47/68.61 (P6(x4159711,x4159711,x4159711)), % 68.47/68.61 inference(rename_variables,[],[20])). % 68.47/68.61 cnf(415973,plain, % 68.47/68.61 (~P6(a1,a4,a1)), % 68.47/68.61 inference(scs_inference,[],[359,22,20,415965,415968,415971,30,34,36,41,39,40])). % 68.47/68.61 cnf(415976,plain, % 68.47/68.61 (P3(a4,a1)+P3(a4,a2)), % 68.47/68.61 inference(scs_inference,[],[415939,415808,3,359,22,20,415965,415968,415971,30,34,36,41,39,40,33])). % 68.47/68.61 cnf(415987,plain, % 68.47/68.61 (P6(a3,a5,a4)+P6(a3,a5,a1)), % 68.47/68.61 inference(scs_inference,[],[415815,415880,29,2,359,4,20,34,36,43])). % 68.47/68.61 cnf(415991,plain, % 68.47/68.61 (~P6(a3,x4159911,a5)+~P6(x4159911,a3,a5)), % 68.47/68.61 inference(scs_inference,[],[415886,359,34,42])). % 68.47/68.61 cnf(415993,plain, % 68.47/68.61 (~P6(a3,a1,a5)+~P3(a3,a2)), % 68.47/68.61 inference(scs_inference,[],[415886,359,17,34,42,36])). % 68.47/68.61 cnf(416006,plain, % 68.47/68.61 (P6(x4160061,x4160061,x4160061)), % 68.47/68.61 inference(rename_variables,[],[20])). % 68.47/68.61 cnf(416008,plain, % 68.47/68.61 (~P6(a3,a1,a1)), % 68.47/68.61 inference(scs_inference,[],[359,21,6,20,416006,34,38,41])). % 68.47/68.61 cnf(416009,plain, % 68.47/68.61 (P6(x4160091,x4160091,x4160091)), % 68.47/68.61 inference(rename_variables,[],[20])). % 68.47/68.61 cnf(416011,plain, % 68.47/68.61 (~P6(a1,a3,a1)), % 68.47/68.61 inference(scs_inference,[],[359,21,6,20,416006,416009,34,38,41,40])). % 68.47/68.61 cnf(416014,plain, % 68.47/68.61 (~P6(a4,a1,a5)+~P3(a4,a2)), % 68.47/68.61 inference(scs_inference,[],[359,18,21,6,20,416006,416009,34,38,41,40,36])). % 68.47/68.61 cnf(416032,plain, % 68.47/68.61 (~P6(a1,a4,a5)+P6(a4,a1,a3)), % 68.47/68.61 inference(scs_inference,[],[1,415833,415970,415967,3,42,43])). % 68.47/68.61 cnf(416063,plain, % 68.47/68.61 (P6(a1,a4,a5)+P6(a1,a4,a3)), % 68.47/68.61 inference(scs_inference,[],[1,415830,415973,3,359,21,6,20,34,38,43])). % 68.47/68.61 cnf(416069,plain, % 68.47/68.61 (P6(x4160691,x4160691,x4160691)), % 68.47/68.61 inference(rename_variables,[],[20])). % 68.47/68.61 cnf(416076,plain, % 68.47/68.61 (~P6(a4,a1,a5)+P6(a1,a4,a3)), % 68.47/68.61 inference(scs_inference,[],[415928,359,20,416069,30,40,36,42,416063])). % 68.47/68.61 cnf(416079,plain, % 68.47/68.61 (~P6(a5,a4,a3)+~P6(a4,a1,a5)), % 68.47/68.61 inference(scs_inference,[],[415928,359,23,20,416069,30,40,36,42,416063,415908,41])). % 68.47/68.61 cnf(416082,plain, % 68.47/68.61 (~P6(a1,a5,a5)), % 68.47/68.61 inference(scs_inference,[],[20,30,41])). % 68.47/68.61 cnf(416111,plain, % 68.47/68.61 (P6(a4,a1,a3)+P3(a4,a1)), % 68.47/68.61 inference(scs_inference,[],[1,415833,415967,415939,415808,3,359,18,21,6,20,34,38,43,36,33])). % 68.47/68.61 cnf(416113,plain, % 68.47/68.61 (~P3(a5,a4)+P6(a4,a1,a3)), % 68.47/68.61 inference(scs_inference,[],[1,415833,415967,415939,415808,3,359,23,18,21,8,6,9,20,34,38,43,36,33,35])). % 68.47/68.61 cnf(416119,plain, % 68.47/68.61 (~P6(a5,x4161191,a4)+~P6(x4161191,a5,a4)), % 68.47/68.61 inference(scs_inference,[],[415868,359,20,36,42])). % 68.47/68.61 cnf(416131,plain, % 68.47/68.61 (P6(a1,a3,a5)+P6(a1,a3,a4)), % 68.47/68.61 inference(scs_inference,[],[1,415845,416011,2,359,23,20,34,38,43])). % 68.47/68.61 cnf(416157,plain, % 68.47/68.61 (P6(x4161571,x4161571,x4161571)), % 68.47/68.61 inference(rename_variables,[],[20])). % 68.47/68.61 cnf(416164,plain, % 68.47/68.61 (P6(a3,a1,a4)+P6(a3,a1,a5)), % 68.47/68.61 inference(scs_inference,[],[1,415850,416008,26,2,359,21,6,20,416157,36,38,34,43])). % 68.47/68.61 cnf(416220,plain, % 68.47/68.61 (~P6(a1,x4162201,a3)+~P6(x4162201,a1,a3)), % 68.47/68.61 inference(scs_inference,[],[415853,359,21,6,20,34,38,42])). % 68.47/68.61 cnf(416228,plain, % 68.47/68.61 (~P6(a1,a4,a3)+~P6(a5,a4,a3)), % 68.47/68.61 inference(scs_inference,[],[1,415853,415967,415833,3,359,21,6,20,34,38,42,43,416014,416111,416113,416076,416079])). % 68.47/68.61 cnf(416364,plain, % 68.47/68.61 (P6(x4163641,x4163641,x4163641)), % 68.47/68.61 inference(rename_variables,[],[20])). % 68.47/68.61 cnf(416371,plain, % 68.47/68.61 (~P3(a4,a2)+~P3(a3,a3)), % 68.47/68.61 inference(scs_inference,[],[24,29,10,359,21,6,7,5,20,416364,38,34,36,35])). % 68.47/68.61 cnf(416632,plain, % 68.47/68.61 (~P3(a3,a3)+P3(a4,a1)), % 68.47/68.61 inference(scs_inference,[],[416371,415976])). % 68.47/68.61 cnf(417008,plain, % 68.47/68.61 (~P3(a3,a2)+P6(a3,a1,a5)), % 68.47/68.61 inference(scs_inference,[],[415901,416164])). % 68.47/68.61 cnf(417296,plain, % 68.47/68.61 (~P3(a4,a1)+~P3(a3,a4)), % 68.47/68.61 inference(scs_inference,[],[28,19,12,20,23,7,359,6,34,38,35])). % 68.47/68.61 cnf(417482,plain, % 68.47/68.61 (~P3(a3,a4)+P3(a4,a2)), % 68.47/68.61 inference(scs_inference,[],[417296,415976])). % 68.47/68.61 cnf(417955,plain, % 68.47/68.61 (~P3(a3,a2)+P6(a3,a1,a4)), % 68.47/68.61 inference(scs_inference,[],[415993,416164])). % 68.47/68.61 cnf(418597,plain, % 68.47/68.61 (~P3(a3,a2)+~P6(a1,a3,a5)), % 68.47/68.61 inference(scs_inference,[],[417008,415991])). % 68.47/68.61 cnf(418912,plain, % 68.47/68.61 (~P3(a3,a2)+~P6(a1,a3,a4)), % 68.47/68.61 inference(scs_inference,[],[417955,415786])). % 68.47/68.61 cnf(419289,plain, % 68.47/68.61 (~P3(a3,a2)+P6(a1,a3,a4)), % 68.47/68.62 inference(scs_inference,[],[418597,416131])). % 68.47/68.62 cnf(419478,plain, % 68.47/68.62 (~P3(a3,a2)), % 68.47/68.62 inference(scs_inference,[],[418912,419289])). % 68.47/68.62 cnf(419533,plain, % 68.47/68.62 (P3(a3,a1)+P3(a3,a4)+P3(a3,a3)), % 68.47/68.62 inference(scs_inference,[],[419478,2,6,19,20,359,21,38,34,33])). % 68.47/68.62 cnf(421248,plain, % 68.47/68.62 (P6(a3,a5,a1)+~P6(a5,a3,a4)), % 68.47/68.62 inference(scs_inference,[],[416119,415987])). % 68.47/68.62 cnf(422682,plain, % 68.47/68.62 (P6(a1,a4,a5)+~P6(a5,a4,a3)), % 68.47/68.62 inference(scs_inference,[],[416228,416063])). % 68.47/68.62 cnf(423953,plain, % 68.47/68.62 (~P6(a3,a4,a1)+~P6(a5,a3,a4)), % 68.47/68.62 inference(scs_inference,[],[29,421248,40])). % 68.47/68.62 cnf(424609,plain, % 68.47/68.62 (~P3(a3,a3)+P6(a3,a1,a4)), % 68.47/68.62 inference(scs_inference,[],[416008,415850,19,359,5,10,2,30,15,32,1,7,35,34,38,43])). % 68.47/68.62 cnf(424777,plain, % 68.47/68.62 (P6(a3,a1,a4)+P3(a3,a1)+P3(a3,a4)), % 68.47/68.62 inference(scs_inference,[],[424609,419533])). % 68.47/68.62 cnf(425467,plain, % 68.47/68.62 (~P6(a3,a5,a1)+~P6(a3,a4,a1)), % 68.47/68.62 inference(scs_inference,[],[423953,415955])). % 68.47/68.62 cnf(426015,plain, % 68.47/68.62 (P6(a3,a5,a4)+~P6(a3,a4,a1)), % 68.47/68.62 inference(scs_inference,[],[425467,415987])). % 68.47/68.62 cnf(426430,plain, % 68.47/68.62 (~P6(a3,a1,a4)+~P6(a3,a4,a1)), % 68.47/68.62 inference(scs_inference,[],[30,426015,40])). % 68.47/68.62 cnf(429758,plain, % 68.47/68.62 (~P3(a4,a1)+~P6(a4,a1,a3)), % 68.47/68.62 inference(scs_inference,[],[9,359,26,8,34,38])). % 68.47/68.62 cnf(429760,plain, % 68.47/68.62 (~P3(a4,a1)+~P6(a1,a4,a5)), % 68.47/68.62 inference(scs_inference,[],[9,359,26,8,34,38,416032])). % 68.47/68.62 cnf(430144,plain, % 68.47/68.62 (P3(a4,a2)+~P6(a4,a1,a3)), % 68.47/68.62 inference(scs_inference,[],[429758,415976])). % 68.47/68.62 cnf(430245,plain, % 68.47/68.62 (~P3(a3,a3)+~P6(a1,a4,a5)), % 68.47/68.62 inference(scs_inference,[],[429760,416632])). % 68.47/68.62 cnf(430646,plain, % 68.47/68.62 (P6(x4306461,x4306461,x4306461)), % 68.47/68.62 inference(rename_variables,[],[20])). % 68.47/68.62 cnf(430651,plain, % 68.47/68.62 (~P3(a4,a1)+~P3(a3,a1)), % 68.47/68.62 inference(scs_inference,[],[20,430646,21,19,6,7,9,359,34,38,36,35])). % 68.47/68.62 cnf(430674,plain, % 68.47/68.62 (~P3(a3,a1)+P6(a4,a1,a3)), % 68.47/68.62 inference(scs_inference,[],[430651,416111])). % 68.47/68.62 cnf(430780,plain, % 68.47/68.62 (P3(a3,a1)+P3(a3,a4)+~P6(a1,a4,a5)), % 68.47/68.62 inference(scs_inference,[],[430245,419533])). % 68.47/68.62 cnf(431536,plain, % 68.47/68.62 (P3(a3,a4)+~P6(a1,a4,a5)+~P3(a4,a2)), % 68.47/68.62 inference(scs_inference,[],[9,19,14,8,430780,37])). % 68.47/68.62 cnf(432941,plain, % 68.47/68.62 (~P3(a3,a4)), % 68.47/68.62 inference(scs_inference,[],[415876,417482])). % 68.47/68.62 cnf(432942,plain, % 68.47/68.62 (P3(a3,a1)+P3(a3,a3)), % 68.47/68.62 inference(scs_inference,[],[432941,419533])). % 68.47/68.62 cnf(432943,plain, % 68.47/68.62 (P6(a3,a1,a4)+P3(a3,a1)), % 68.47/68.62 inference(scs_inference,[],[432941,424777])). % 68.47/68.62 cnf(432945,plain, % 68.47/68.62 (~P3(a4,a2)+~P6(a1,a4,a5)), % 68.47/68.62 inference(scs_inference,[],[432941,431536])). % 68.47/68.62 cnf(433134,plain, % 68.47/68.62 (~P6(a4,a1,a3)+~P6(a1,a4,a5)), % 68.47/68.62 inference(scs_inference,[],[432945,430144])). % 68.47/68.62 cnf(434081,plain, % 68.47/68.62 (~P6(a1,a4,a5)), % 68.47/68.62 inference(scs_inference,[],[433134,416032])). % 68.47/68.62 cnf(434082,plain, % 68.47/68.62 (P6(a1,a4,a3)), % 68.47/68.62 inference(scs_inference,[],[434081,416063])). % 68.47/68.62 cnf(434083,plain, % 68.47/68.62 (~P6(a5,a4,a3)), % 68.47/68.62 inference(scs_inference,[],[434081,422682])). % 68.47/68.62 cnf(434111,plain, % 68.47/68.62 (~P6(a1,a3,a5)), % 68.47/68.62 inference(scs_inference,[],[434082,434083,29,359,416220,430674,432943,34,40,42])). % 68.47/68.62 cnf(434118,plain, % 68.47/68.62 (P6(x4341181,x4341181,x4341181)), % 68.47/68.62 inference(rename_variables,[],[20])). % 68.47/68.62 cnf(434125,plain, % 68.47/68.62 (~P6(a1,a3,a4)), % 68.47/68.62 inference(scs_inference,[],[434082,434083,416082,415925,25,10,20,434118,29,1,4,23,7,359,416220,430674,432943,34,40,42,43,426430,432942,36,38,35,415786])). % 68.47/68.62 cnf(434164,plain, % 68.47/68.62 ($false), % 68.47/68.62 inference(scs_inference,[],[434125,434111,416131]), % 68.47/68.62 ['proof']). % 68.68/68.79 % SZS output end Proof % 68.68/68.79 % Total time :67.590000s %------------------------------------------------------------------------------