%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP127-3.004 : TPTP v8.2.0. Released v1.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n032.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:53 EDT 2024 % Result : Unsatisfiable 121.96s 122.30s % Output : CNFRefutation 122.64s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : GRP127-3.004 : TPTP v8.2.0. Released v1.2.0. % 0.06/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.11/0.33 % Computer : n032.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Thu Jun 20 08:49:23 EDT 2024 % 0.11/0.33 % CPUTime : % 0.49/0.58 start to proof:theBenchmark % 121.87/122.27 %------------------------------------------- % 121.87/122.27 % File :CSE---1.7 % 121.87/122.27 % Problem :theBenchmark % 121.87/122.27 % Transform :cnf % 121.87/122.27 % Format :tptp:raw % 121.87/122.27 % Command :java -jar mcs_scs.jar %d %s % 121.87/122.27 % 121.87/122.27 % Result :Theorem 121.290000s % 121.87/122.27 % Output :CNFRefutation 121.290000s % 121.87/122.27 %------------------------------------------- % 121.87/122.29 %-------------------------------------------------------------------------- % 121.87/122.29 % File : GRP127-3.004 : TPTP v8.2.0. Released v1.2.0. % 121.87/122.29 % Domain : Group Theory (Quasigroups) % 121.87/122.29 % Problem : ((b.a).b).b) = a % 121.87/122.29 % Version : [Sla93] axioms : Augmented. % 121.87/122.29 % English : Generate the multiplication table for the specified quasi- % 121.87/122.29 % group with 4 elements. % 121.87/122.29 % 121.87/122.29 % Refs : [Ben89] Bennett (1989), Quasigroup Identities and Mendelsohn D % 121.87/122.29 % : [FSB93] Fujita et al. (1993), Automatic Generation of Some Res % 121.87/122.29 % : [Sla93] Slaney (1993), Email to G. Sutcliffe % 121.87/122.29 % : [SFS95] Slaney et al. (1995), Automated Reasoning and Exhausti % 121.87/122.29 % Source : [TPTP] % 121.87/122.29 % Names : % 121.87/122.29 % 121.87/122.29 % Status : Unsatisfiable % 121.87/122.29 % Rating : 0.00 v2.1.0 % 121.87/122.29 % Syntax : Number of clauses : 43 ( 32 unt; 2 nHn; 42 RR) % 121.87/122.29 % Number of literals : 78 ( 0 equ; 43 neg) % 121.87/122.29 % Maximal clause size : 6 ( 1 avg) % 121.87/122.29 % Maximal term depth : 1 ( 1 avg) % 121.87/122.29 % Number of predicates : 6 ( 6 usr; 0 prp; 1-3 aty) % 121.87/122.29 % Number of functors : 5 ( 5 usr; 5 con; 0-0 aty) % 121.87/122.29 % Number of variables : 39 ( 0 sgn) % 121.87/122.29 % SPC : CNF_UNS_EPR_NEQ_NHN % 121.87/122.29 % 121.87/122.29 % Comments : [SFS93]'s axiomatization has been modified for this. % 121.87/122.29 % : Substitution axioms are not needed, as any positive equality % 121.87/122.29 % literals should resolve on negative ones directly. % 121.87/122.29 % : This problem is extensively investigated in [Ben89]. % 121.87/122.29 % : Version 3 has complex isomorphism avoidance (mentioned in % 121.87/122.29 % [SFS95] % 121.87/122.29 % : tptp2X: -f tptp -s4 GRP127-3.g % 121.87/122.29 %-------------------------------------------------------------------------- % 121.87/122.29 cnf(e_0_then_e_1,axiom, % 121.87/122.29 next(e_0,e_1) ). % 121.87/122.29 % 121.87/122.29 cnf(e_1_then_e_2,axiom, % 121.87/122.29 next(e_1,e_2) ). % 121.87/122.29 % 121.87/122.29 cnf(e_2_then_e_3,axiom, % 121.87/122.30 next(e_2,e_3) ). % 121.87/122.30 % 121.87/122.30 cnf(e_3_then_e_4,axiom, % 121.87/122.30 next(e_3,e_4) ). % 121.87/122.30 % 121.87/122.30 cnf(e_1_greater_e_0,axiom, % 121.87/122.30 greater(e_1,e_0) ). % 121.87/122.30 % 121.87/122.30 cnf(e_2_greater_e_0,axiom, % 121.87/122.30 greater(e_2,e_0) ). % 121.87/122.30 % 121.87/122.30 cnf(e_3_greater_e_0,axiom, % 121.87/122.30 greater(e_3,e_0) ). % 121.87/122.30 % 121.87/122.30 cnf(e_4_greater_e_0,axiom, % 121.87/122.30 greater(e_4,e_0) ). % 121.87/122.30 % 121.87/122.30 cnf(e_2_greater_e_1,axiom, % 121.87/122.30 greater(e_2,e_1) ). % 121.87/122.30 % 121.87/122.30 cnf(e_3_greater_e_1,axiom, % 121.87/122.30 greater(e_3,e_1) ). % 121.87/122.30 % 121.87/122.30 cnf(e_4_greater_e_1,axiom, % 121.87/122.30 greater(e_4,e_1) ). % 121.87/122.30 % 121.87/122.30 cnf(e_3_greater_e_2,axiom, % 121.87/122.30 greater(e_3,e_2) ). % 121.87/122.30 % 121.87/122.30 cnf(e_4_greater_e_2,axiom, % 121.87/122.30 greater(e_4,e_2) ). % 121.87/122.30 % 121.87/122.30 cnf(e_4_greater_e_3,axiom, % 121.87/122.30 greater(e_4,e_3) ). % 121.87/122.30 % 121.87/122.30 cnf(cycle1,axiom, % 121.87/122.30 ( ~ cycle(X,Y) % 121.87/122.30 | ~ cycle(X,Z) % 121.87/122.30 | equalish(Y,Z) ) ). % 121.87/122.30 % 121.87/122.30 cnf(cycle2,axiom, % 121.87/122.30 ( ~ group_element(X) % 121.87/122.30 | cycle(X,e_0) % 121.87/122.30 | cycle(X,e_1) % 121.87/122.30 | cycle(X,e_2) % 121.87/122.30 | cycle(X,e_3) ) ). % 121.87/122.30 % 121.87/122.30 cnf(cycle3,axiom, % 121.87/122.30 cycle(e_4,e_0) ). % 121.87/122.30 % 121.87/122.30 cnf(cycle4,axiom, % 121.87/122.30 ( ~ cycle(X,Y) % 121.87/122.30 | ~ cycle(W,Z) % 121.87/122.30 | ~ next(X,W) % 121.87/122.30 | ~ greater(Y,e_0) % 121.87/122.30 | ~ next(Z,Z1) % 121.87/122.30 | equalish(Y,Z1) ) ). % 121.87/122.30 % 121.87/122.30 cnf(cycle5,axiom, % 121.87/122.30 ( ~ cycle(X,Z1) % 121.87/122.30 | ~ cycle(Y,e_0) % 121.87/122.30 | ~ cycle(W,Z2) % 121.87/122.30 | ~ next(Y,W) % 121.87/122.30 | ~ greater(Y,X) % 121.87/122.30 | ~ greater(Z1,Z2) ) ). % 121.87/122.30 % 121.87/122.30 cnf(cycle6,axiom, % 121.87/122.30 ( ~ cycle(X,e_0) % 121.87/122.30 | ~ product(X,e_1,Y) % 121.87/122.30 | ~ greater(Y,X) ) ). % 121.96/122.30 % 121.96/122.30 cnf(cycle7,axiom, % 121.96/122.30 ( ~ cycle(X,Y) % 121.96/122.30 | ~ product(X,e_1,Z) % 121.96/122.30 | ~ greater(Y,e_0) % 121.96/122.30 | ~ next(X,X1) % 121.96/122.30 | equalish(Z,X1) ) ). % 121.96/122.30 % 121.96/122.30 cnf(element_1,axiom, % 121.96/122.30 group_element(e_1) ). % 121.96/122.30 % 121.96/122.30 cnf(element_2,axiom, % 121.96/122.30 group_element(e_2) ). % 121.96/122.30 % 121.96/122.30 cnf(element_3,axiom, % 121.96/122.30 group_element(e_3) ). % 121.96/122.30 % 121.96/122.30 cnf(element_4,axiom, % 121.96/122.30 group_element(e_4) ). % 121.96/122.30 % 121.96/122.30 cnf(e_1_is_not_e_2,axiom, % 121.96/122.30 ~ equalish(e_1,e_2) ). % 121.96/122.30 % 121.96/122.30 cnf(e_1_is_not_e_3,axiom, % 121.96/122.30 ~ equalish(e_1,e_3) ). % 121.96/122.30 % 121.96/122.30 cnf(e_1_is_not_e_4,axiom, % 121.96/122.30 ~ equalish(e_1,e_4) ). % 121.96/122.30 % 121.96/122.30 cnf(e_2_is_not_e_1,axiom, % 121.96/122.30 ~ equalish(e_2,e_1) ). % 121.96/122.30 % 121.96/122.30 cnf(e_2_is_not_e_3,axiom, % 121.96/122.30 ~ equalish(e_2,e_3) ). % 121.96/122.30 % 121.96/122.30 cnf(e_2_is_not_e_4,axiom, % 121.96/122.30 ~ equalish(e_2,e_4) ). % 121.96/122.30 % 121.96/122.30 cnf(e_3_is_not_e_1,axiom, % 121.96/122.30 ~ equalish(e_3,e_1) ). % 121.96/122.30 % 121.96/122.30 cnf(e_3_is_not_e_2,axiom, % 121.96/122.30 ~ equalish(e_3,e_2) ). % 121.96/122.30 % 121.96/122.30 cnf(e_3_is_not_e_4,axiom, % 121.96/122.30 ~ equalish(e_3,e_4) ). % 121.96/122.30 % 121.96/122.30 cnf(e_4_is_not_e_1,axiom, % 121.96/122.30 ~ equalish(e_4,e_1) ). % 121.96/122.30 % 121.96/122.30 cnf(e_4_is_not_e_2,axiom, % 121.96/122.30 ~ equalish(e_4,e_2) ). % 121.96/122.30 % 121.96/122.30 cnf(e_4_is_not_e_3,axiom, % 121.96/122.30 ~ equalish(e_4,e_3) ). % 121.96/122.30 % 121.96/122.30 cnf(product_total_function1,axiom, % 121.96/122.30 ( ~ group_element(X) % 121.96/122.30 | ~ group_element(Y) % 121.96/122.30 | product(X,Y,e_1) % 121.96/122.30 | product(X,Y,e_2) % 121.96/122.30 | product(X,Y,e_3) % 121.96/122.30 | product(X,Y,e_4) ) ). % 121.96/122.30 % 121.96/122.30 cnf(product_total_function2,axiom, % 121.96/122.30 ( ~ product(X,Y,W) % 121.96/122.30 | ~ product(X,Y,Z) % 121.96/122.30 | equalish(W,Z) ) ). % 121.96/122.30 % 121.96/122.30 cnf(product_right_cancellation,axiom, % 121.96/122.30 ( ~ product(X,W,Y) % 121.96/122.30 | ~ product(X,Z,Y) % 121.96/122.30 | equalish(W,Z) ) ). % 121.96/122.30 % 121.96/122.30 cnf(product_left_cancellation,axiom, % 121.96/122.30 ( ~ product(W,Y,X) % 121.96/122.30 | ~ product(Z,Y,X) % 121.96/122.30 | equalish(W,Z) ) ). % 121.96/122.30 % 121.96/122.30 cnf(product_idempotence,axiom, % 121.96/122.30 product(X,X,X) ). % 121.96/122.30 % 121.96/122.30 cnf(qg3,negated_conjecture, % 121.96/122.30 ( ~ product(Y,X,Z1) % 121.96/122.30 | ~ product(Z1,Y,Z2) % 121.96/122.30 | product(Z2,Y,X) ) ). % 121.96/122.30 % 121.96/122.30 %-------------------------------------------------------------------------- % 121.96/122.30 %------------------------------------------- % 121.96/122.30 % Proof found % 121.96/122.30 % SZS status Theorem for theBenchmark % 121.96/122.30 % SZS output start Proof % 121.96/122.32 %ClaNum:43(EqnAxiom:0) % 121.96/122.32 %VarNum:93(SingletonVarNum:39) % 121.96/122.32 %MaxLitNum:6 % 121.96/122.32 %MaxfuncDepth:0 % 121.96/122.32 %SharedTerms:36 % 121.96/122.32 %goalClause: 42 % 121.96/122.32 [1]P1(a1) % 121.96/122.32 [2]P1(a3) % 121.96/122.32 [3]P1(a4) % 121.96/122.32 [4]P1(a5) % 121.96/122.32 [5]P5(a2,a1) % 121.96/122.32 [6]P5(a1,a3) % 121.96/122.32 [7]P5(a3,a4) % 121.96/122.32 [8]P5(a4,a5) % 121.96/122.32 [9]P2(a1,a2) % 121.96/122.32 [10]P2(a3,a2) % 121.96/122.32 [11]P2(a3,a1) % 121.96/122.32 [12]P2(a4,a2) % 121.96/122.32 [13]P2(a4,a1) % 121.96/122.32 [14]P2(a4,a3) % 121.96/122.32 [15]P2(a5,a2) % 121.96/122.32 [16]P2(a5,a1) % 121.96/122.32 [17]P2(a5,a3) % 121.96/122.32 [18]P2(a5,a4) % 121.96/122.32 [19]P3(a5,a2) % 121.96/122.32 [21]~P4(a1,a3) % 121.96/122.32 [22]~P4(a1,a4) % 121.96/122.32 [23]~P4(a1,a5) % 121.96/122.32 [24]~P4(a3,a1) % 121.96/122.32 [25]~P4(a3,a4) % 121.96/122.32 [26]~P4(a3,a5) % 121.96/122.32 [27]~P4(a4,a1) % 121.96/122.32 [28]~P4(a4,a3) % 121.96/122.32 [29]~P4(a4,a5) % 121.96/122.32 [30]~P4(a5,a1) % 121.96/122.32 [31]~P4(a5,a3) % 121.96/122.32 [32]~P4(a5,a4) % 121.96/122.32 [20]P6(x201,x201,x201) % 121.96/122.32 [36]~P2(x361,x362)+~P6(x362,a1,x361)+~P3(x362,a2) % 121.96/122.32 [34]~P3(x343,x341)+P4(x341,x342)+~P3(x343,x342) % 121.96/122.32 [39]~P6(x393,x394,x391)+P4(x391,x392)+~P6(x393,x394,x392) % 121.96/122.32 [40]~P6(x403,x401,x404)+P4(x401,x402)+~P6(x403,x402,x404) % 121.96/122.32 [41]~P6(x411,x413,x414)+P4(x411,x412)+~P6(x412,x413,x414) % 121.96/122.32 [42]~P6(x422,x423,x424)+P6(x421,x422,x423)+~P6(x424,x422,x421) % 121.96/122.32 [33]~P1(x331)+P3(x331,a1)+P3(x331,a3)+P3(x331,a4)+P3(x331,a2) % 121.96/122.32 [38]P4(x381,x382)+~P5(x383,x382)+~P3(x383,x384)+~P6(x383,a1,x381)+~P2(x384,a2) % 121.96/122.32 [43]~P1(x432)+~P1(x431)+P6(x431,x432,a3)+P6(x431,x432,a4)+P6(x431,x432,a5)+P6(x431,x432,a1) % 121.96/122.32 [35]~P3(x355,x353)+~P3(x354,x351)+P4(x351,x352)+~P5(x353,x352)+~P5(x354,x355)+~P2(x351,a2) % 121.96/122.32 [37]~P3(x372,x375)+~P3(x373,x374)+~P5(x371,x372)+~P2(x371,x373)+~P2(x374,x375)+~P3(x371,a2) % 121.96/122.32 %EqnAxiom % 121.96/122.32 % 121.96/122.32 %------------------------------------------- % 122.39/122.76 cnf(46,plain, % 122.39/122.76 (~P3(a1,a1)), % 122.39/122.76 inference(scs_inference,[],[20,9,6,21,39,38])). % 122.39/122.76 cnf(77,plain, % 122.39/122.76 (P3(a1,a3)+P3(a1,a2)), % 122.39/122.76 inference(scs_inference,[],[1,20,46,12,19,6,21,40,38,36,33])). % 122.39/122.76 cnf(91,plain, % 122.39/122.76 (~P3(a5,a4)+~P3(a4,a1)), % 122.39/122.76 inference(scs_inference,[],[20,9,19,15,8,23,34,39,36,38,35])). % 122.39/122.76 cnf(99,plain, % 122.39/122.76 (P3(a1,a2)), % 122.39/122.76 inference(scs_inference,[],[20,10,6,21,41,38,77])). % 122.39/122.76 cnf(227871,plain, % 122.39/122.76 (~P6(a4,a1,a4)), % 122.39/122.76 inference(scs_inference,[],[27,13,99,20,36,40])). % 122.39/122.76 cnf(227872,plain, % 122.39/122.76 (P6(x2278721,x2278721,x2278721)), % 122.39/122.76 inference(rename_variables,[],[20])). % 122.39/122.76 cnf(227877,plain, % 122.39/122.76 (P6(x2278771,x2278771,x2278771)), % 122.39/122.76 inference(rename_variables,[],[20])). % 122.39/122.76 cnf(227879,plain, % 122.39/122.76 (~P6(a1,a4,a4)), % 122.39/122.76 inference(scs_inference,[],[27,13,99,20,227872,227877,36,40,34,39,41])). % 122.39/122.76 cnf(227884,plain, % 122.39/122.76 (~P3(a4,a4)), % 122.39/122.76 inference(scs_inference,[],[27,25,13,8,5,7,12,99,19,20,227872,227877,36,40,34,39,41,38,35])). % 122.39/122.76 cnf(227887,plain, % 122.39/122.76 (P6(x2278871,x2278871,x2278871)), % 122.39/122.76 inference(rename_variables,[],[20])). % 122.39/122.76 cnf(227889,plain, % 122.39/122.76 (~P6(a3,a1,a3)), % 122.39/122.76 inference(scs_inference,[],[24,20,227887,99,36,40])). % 122.39/122.76 cnf(227911,plain, % 122.39/122.76 (~P6(a3,a4,a3)), % 122.39/122.76 inference(scs_inference,[],[25,11,30,20,5,15,99,36,34,35,40])). % 122.39/122.76 cnf(227912,plain, % 122.39/122.76 (P6(x2279121,x2279121,x2279121)), % 122.39/122.76 inference(rename_variables,[],[20])). % 122.39/122.76 cnf(227915,plain, % 122.39/122.76 (P6(x2279151,x2279151,x2279151)), % 122.39/122.76 inference(rename_variables,[],[20])). % 122.39/122.76 cnf(227917,plain, % 122.39/122.76 (~P6(a4,a3,a3)), % 122.39/122.76 inference(scs_inference,[],[25,11,30,20,227912,227915,5,15,99,36,34,35,40,39,41])). % 122.39/122.76 cnf(227930,plain, % 122.39/122.76 (~P3(a3,a4)+~P3(a4,a2)), % 122.39/122.76 inference(scs_inference,[],[27,14,8,20,12,99,19,36,34,37])). % 122.39/122.76 cnf(227948,plain, % 122.39/122.76 (P6(x2279481,x2279481,x2279481)), % 122.39/122.76 inference(rename_variables,[],[20])). % 122.39/122.76 cnf(227951,plain, % 122.39/122.76 (P6(x2279511,x2279511,x2279511)), % 122.39/122.76 inference(rename_variables,[],[20])). % 122.39/122.76 cnf(227953,plain, % 122.39/122.76 (~P6(a4,a5,a4)), % 122.39/122.76 inference(scs_inference,[],[29,20,227948,227951,21,99,6,34,38,36,40])). % 122.39/122.76 cnf(227954,plain, % 122.39/122.76 (P6(x2279541,x2279541,x2279541)), % 122.39/122.76 inference(rename_variables,[],[20])). % 122.39/122.76 cnf(227957,plain, % 122.39/122.76 (P6(x2279571,x2279571,x2279571)), % 122.39/122.76 inference(rename_variables,[],[20])). % 122.39/122.76 cnf(227959,plain, % 122.39/122.76 (~P6(a5,a4,a4)), % 122.39/122.76 inference(scs_inference,[],[29,20,227948,227951,227954,227957,21,99,6,34,38,36,40,39,41])). % 122.39/122.76 cnf(227962,plain, % 122.39/122.76 (P3(a4,a1)+P3(a4,a2)+P3(a4,a3)), % 122.39/122.76 inference(scs_inference,[],[227884,3,29,20,227948,227951,227954,227957,21,99,6,34,38,36,40,39,41,33])). % 122.39/122.76 cnf(227966,plain, % 122.39/122.76 (~P6(a3,a1,a4)+~P3(a3,a2)), % 122.39/122.76 inference(scs_inference,[],[14,20,21,99,6,38,36])). % 122.39/122.76 cnf(227985,plain, % 122.39/122.76 (P6(x2279851,x2279851,x2279851)), % 122.39/122.76 inference(rename_variables,[],[20])). % 122.39/122.76 cnf(227989,plain, % 122.39/122.76 (~P6(a4,a3,a4)), % 122.39/122.76 inference(scs_inference,[],[28,20,227985,99,36,34,40])). % 122.39/122.76 cnf(227997,plain, % 122.39/122.76 (P6(x2279971,x2279971,x2279971)), % 122.39/122.76 inference(rename_variables,[],[20])). % 122.39/122.76 cnf(227999,plain, % 122.39/122.76 (~P6(a3,a4,a4)), % 122.39/122.76 inference(scs_inference,[],[28,20,227997,39,41])). % 122.39/122.76 cnf(228023,plain, % 122.39/122.76 (P6(x2280231,x2280231,x2280231)), % 122.39/122.76 inference(rename_variables,[],[20])). % 122.39/122.76 cnf(228025,plain, % 122.39/122.76 (~P6(a5,a1,a5)), % 122.39/122.76 inference(scs_inference,[],[30,20,228023,99,36,40])). % 122.39/122.76 cnf(228038,plain, % 122.39/122.76 (P6(x2280381,x2280381,x2280381)), % 122.39/122.76 inference(rename_variables,[],[20])). % 122.39/122.76 cnf(228040,plain, % 122.39/122.76 (~P6(a1,a5,a5)), % 122.39/122.76 inference(scs_inference,[],[30,20,228038,99,10,34,36,39,41])). % 122.39/122.76 cnf(228048,plain, % 122.39/122.76 (P6(x2280481,x2280481,x2280481)), % 122.39/122.76 inference(rename_variables,[],[20])). % 122.39/122.76 cnf(228057,plain, % 122.39/122.76 (P3(a4,a2)+P3(a4,a1)), % 122.39/122.76 inference(scs_inference,[],[24,29,8,20,228048,5,21,99,19,10,6,36,38,34,35,227962])). % 122.39/122.76 cnf(228063,plain, % 122.39/122.76 (~P6(a3,a1,a5)+~P3(a3,a2)), % 122.39/122.76 inference(scs_inference,[],[20,21,99,17,6,34,38,36])). % 122.39/122.76 cnf(228068,plain, % 122.39/122.76 (P6(x2280681,x2280681,x2280681)), % 122.39/122.76 inference(rename_variables,[],[20])). % 122.39/122.76 cnf(228072,plain, % 122.39/122.76 (~P6(a3,a5,a3)), % 122.39/122.76 inference(scs_inference,[],[29,26,20,228068,99,36,34,40])). % 122.39/122.76 cnf(228080,plain, % 122.39/122.76 (~P6(a4,a1,a5)+~P3(a4,a2)), % 122.39/122.76 inference(scs_inference,[],[99,18,34,36])). % 122.39/122.76 cnf(228083,plain, % 122.39/122.76 (P6(x2280831,x2280831,x2280831)), % 122.39/122.76 inference(rename_variables,[],[20])). % 122.39/122.76 cnf(228085,plain, % 122.39/122.76 (~P6(a5,a3,a3)), % 122.39/122.76 inference(scs_inference,[],[26,20,228083,99,18,34,36,39,41])). % 122.39/122.76 cnf(228105,plain, % 122.39/122.76 (P6(a1,a5,a4)+P6(a1,a5,a3)+P6(a1,a5,a1)), % 122.39/122.76 inference(scs_inference,[],[228040,1,20,21,99,6,4,34,38,43])). % 122.39/122.76 cnf(228107,plain, % 122.39/122.76 (P6(x2281071,x2281071,x2281071)), % 122.39/122.76 inference(rename_variables,[],[20])). % 122.39/122.76 cnf(228109,plain, % 122.39/122.76 (~P6(a5,a3,a5)), % 122.39/122.76 inference(scs_inference,[],[20,228107,31,99,36,40])). % 122.39/122.76 cnf(228120,plain, % 122.39/122.76 (P6(x2281201,x2281201,x2281201)), % 122.39/122.76 inference(rename_variables,[],[20])). % 122.39/122.76 cnf(228122,plain, % 122.39/122.76 (~P6(a3,a5,a5)), % 122.39/122.76 inference(scs_inference,[],[20,228120,31,99,34,39,41])). % 122.39/122.76 cnf(228123,plain, % 122.39/122.76 (P6(x2281231,x2281231,x2281231)), % 122.39/122.76 inference(rename_variables,[],[20])). % 122.39/122.76 cnf(228128,plain, % 122.39/122.76 (P6(a5,a3,a1)+P6(a5,a3,a4)), % 122.39/122.76 inference(scs_inference,[],[4,228085,228109,2,20,228120,228123,31,22,99,34,39,41,38,43])). % 122.39/122.76 cnf(228142,plain, % 122.39/122.76 (P6(a3,a4,a1)+P6(a3,a4,a5)), % 122.39/122.76 inference(scs_inference,[],[227911,227999,3,2,20,21,99,6,34,38,43])). % 122.39/122.76 cnf(228151,plain, % 122.39/122.76 (~P6(a1,a4,a1)), % 122.39/122.76 inference(scs_inference,[],[20,22,40])). % 122.39/122.76 cnf(228152,plain, % 122.39/122.76 (P6(x2281521,x2281521,x2281521)), % 122.39/122.77 inference(rename_variables,[],[20])). % 122.39/122.77 cnf(228155,plain, % 122.39/122.77 (P6(x2281551,x2281551,x2281551)), % 122.39/122.77 inference(rename_variables,[],[20])). % 122.39/122.77 cnf(228157,plain, % 122.39/122.77 (~P6(a4,a1,a1)), % 122.39/122.77 inference(scs_inference,[],[20,228152,228155,22,32,40,39,41])). % 122.39/122.77 cnf(228170,plain, % 122.39/122.77 (P6(a1,a4,a5)+P6(a1,a4,a3)), % 122.39/122.77 inference(scs_inference,[],[227879,228151,1,3,99,34,43])). % 122.39/122.77 cnf(228172,plain, % 122.39/122.77 (~P6(a1,a5,a1)), % 122.39/122.77 inference(scs_inference,[],[227879,228151,1,3,20,23,99,34,43,40])). % 122.39/122.77 cnf(228178,plain, % 122.39/122.77 (P6(a1,a5,a4)+P6(a1,a5,a3)), % 122.39/122.77 inference(scs_inference,[],[228172,228105])). % 122.39/122.77 cnf(228179,plain, % 122.39/122.77 (~P6(a5,a1,a1)), % 122.39/122.77 inference(scs_inference,[],[20,23,41])). % 122.39/122.77 cnf(228193,plain, % 122.39/122.77 (~P6(a3,a1,a1)), % 122.39/122.77 inference(scs_inference,[],[20,21,41])). % 122.39/122.77 cnf(228206,plain, % 122.39/122.77 (~P6(a1,a3,a1)), % 122.39/122.77 inference(scs_inference,[],[20,21,19,34,40])). % 122.39/122.77 cnf(228221,plain, % 122.39/122.77 (~P6(a3,a1,a4)+P6(a3,a5,a1)), % 122.39/122.77 inference(scs_inference,[],[4,228072,228122,2,30,20,21,19,99,6,38,34,43,40])). % 122.39/122.77 cnf(228226,plain, % 122.39/122.77 (~P6(a4,a5,a5)), % 122.39/122.77 inference(scs_inference,[],[20,32,41])). % 122.39/122.77 cnf(228227,plain, % 122.39/122.77 (P6(x2282271,x2282271,x2282271)), % 122.39/122.77 inference(rename_variables,[],[20])). % 122.39/122.77 cnf(228229,plain, % 122.39/122.77 (~P6(a5,a4,a5)), % 122.39/122.77 inference(scs_inference,[],[20,228227,32,41,40])). % 122.39/122.77 cnf(228230,plain, % 122.39/122.77 (P6(x2282301,x2282301,x2282301)), % 122.39/122.77 inference(rename_variables,[],[20])). % 122.39/122.77 cnf(228237,plain, % 122.39/122.77 (P6(a4,a1,a5)+P6(a4,a1,a3)), % 122.39/122.77 inference(scs_inference,[],[227871,228157,1,3,29,20,228227,228230,21,99,6,32,41,40,38,34,43])). % 122.39/122.77 cnf(228242,plain, % 122.39/122.77 (P6(x2282421,x2282421,x2282421)), % 122.39/122.77 inference(rename_variables,[],[20])). % 122.39/122.77 cnf(228247,plain, % 122.39/122.77 (P6(a3,a1,a5)+P6(a3,a1,a4)), % 122.39/122.77 inference(scs_inference,[],[227889,228193,1,2,20,228242,22,19,99,34,36,38,43])). % 122.39/122.77 cnf(228261,plain, % 122.39/122.77 (~P6(a1,a4,a5)+P6(a4,a5,a3)), % 122.39/122.77 inference(scs_inference,[],[227953,228226,228229,4,3,20,21,19,99,6,34,38,43,42])). % 122.39/122.77 cnf(228282,plain, % 122.39/122.77 (P6(x2282821,x2282821,x2282821)), % 122.39/122.77 inference(rename_variables,[],[20])). % 122.39/122.77 cnf(228287,plain, % 122.39/122.77 (P6(a5,a4,a1)+P6(a5,a4,a3)), % 122.39/122.77 inference(scs_inference,[],[227959,228229,4,3,29,20,228282,21,99,6,34,38,36,43])). % 122.39/122.77 cnf(228616,plain, % 122.39/122.77 (~P3(a3,a3)+~P3(a4,a2)), % 122.39/122.77 inference(scs_inference,[],[10,14,8,20,19,99,34,36,37])). % 122.39/122.77 cnf(228774,plain, % 122.39/122.77 (~P3(a4,a1)+~P3(a3,a4)), % 122.39/122.77 inference(scs_inference,[],[12,99,28,7,22,20,6,34,38,35])). % 122.39/122.77 cnf(228886,plain, % 122.39/122.77 (~P3(a3,a3)+P3(a4,a1)), % 122.39/122.77 inference(scs_inference,[],[228616,228057])). % 122.39/122.77 cnf(229072,plain, % 122.39/122.77 (~P3(a3,a4)+P3(a4,a2)), % 122.39/122.77 inference(scs_inference,[],[228774,228057])). % 122.39/122.77 cnf(229358,plain, % 122.39/122.77 (~P3(a3,a4)), % 122.39/122.77 inference(scs_inference,[],[229072,227930])). % 122.39/122.77 cnf(229411,plain, % 122.39/122.77 (P3(a3,a3)+P3(a3,a2)+P3(a3,a1)), % 122.39/122.77 inference(scs_inference,[],[21,229358,2,6,99,20,34,38,33])). % 122.39/122.77 cnf(229585,plain, % 122.39/122.77 (~P3(a3,a2)+P6(a3,a1,a5)), % 122.39/122.77 inference(scs_inference,[],[227966,228247])). % 122.39/122.77 cnf(230075,plain, % 122.39/122.77 (~P3(a3,a2)+P6(a3,a1,a4)), % 122.39/122.77 inference(scs_inference,[],[228063,228247])). % 122.39/122.77 cnf(230185,plain, % 122.39/122.77 (P6(a3,a1,a5)+P3(a3,a3)+P3(a3,a1)), % 122.39/122.77 inference(scs_inference,[],[229585,229411])). % 122.39/122.77 cnf(230283,plain, % 122.39/122.77 (P6(a3,a1,a4)+P3(a3,a1)+P3(a3,a3)), % 122.39/122.77 inference(scs_inference,[],[230075,229411])). % 122.39/122.77 cnf(230316,plain, % 122.39/122.77 (~P3(a4,a1)+~P3(a3,a1)), % 122.39/122.77 inference(scs_inference,[],[21,20,6,29,7,9,99,38,34,35])). % 122.39/122.77 cnf(230387,plain, % 122.39/122.77 (~P3(a4,a1)+P6(a3,a1,a5)+P3(a3,a3)), % 122.39/122.77 inference(scs_inference,[],[230316,230185])). % 122.39/122.77 cnf(230603,plain, % 122.39/122.77 (~P6(a5,a1,a4)+P6(a5,a3,a1)), % 122.39/122.77 inference(scs_inference,[],[24,228128,40])). % 122.39/122.77 cnf(230718,plain, % 122.39/122.77 (~P6(a1,a4,a5)+P6(a3,a4,a1)), % 122.39/122.77 inference(scs_inference,[],[24,228142,41])). % 122.39/122.77 cnf(231382,plain, % 122.39/122.77 (P6(a3,a1,a5)+P6(a3,a5,a1)), % 122.39/122.77 inference(scs_inference,[],[228221,228247])). % 122.39/122.77 cnf(231723,plain, % 122.39/122.77 (~P6(a4,a1,a3)+~P6(a1,a4,a5)), % 122.39/122.77 inference(scs_inference,[],[30,228261,40])). % 122.39/122.77 cnf(231842,plain, % 122.39/122.77 (P6(a5,a4,a3)+~P6(a1,a5,a4)), % 122.39/122.77 inference(scs_inference,[],[227953,228287,42])). % 122.39/122.77 cnf(232427,plain, % 122.39/122.77 (P6(a3,a5,a1)+~P3(a3,a2)), % 122.39/122.77 inference(scs_inference,[],[231382,228063])). % 122.39/122.77 cnf(232532,plain, % 122.39/122.77 (~P3(a3,a2)+~P6(a3,a4,a1)), % 122.39/122.77 inference(scs_inference,[],[29,232427,40])). % 122.39/122.77 cnf(232651,plain, % 122.39/122.77 (P3(a3,a1)+P3(a3,a3)+~P6(a3,a4,a1)), % 122.39/122.77 inference(scs_inference,[],[232532,229411])). % 122.39/122.77 cnf(232986,plain, % 122.39/122.77 (P6(a4,a1,a5)+~P6(a1,a4,a5)), % 122.39/122.77 inference(scs_inference,[],[231723,228237])). % 122.39/122.77 cnf(233094,plain, % 122.39/122.77 (~P6(a5,a4,a1)+~P6(a1,a5,a4)), % 122.39/122.77 inference(scs_inference,[],[24,231842,39])). % 122.39/122.77 cnf(233431,plain, % 122.39/122.77 (~P3(a4,a2)+~P6(a1,a4,a5)), % 122.39/122.77 inference(scs_inference,[],[232986,228080])). % 122.39/122.77 cnf(233521,plain, % 122.39/122.77 (P3(a4,a1)+~P6(a1,a4,a5)), % 122.39/122.77 inference(scs_inference,[],[233431,228057])). % 122.39/122.77 cnf(233629,plain, % 122.39/122.77 (~P3(a5,a4)+~P6(a1,a4,a5)), % 122.39/122.77 inference(scs_inference,[],[233521,91])). % 122.39/122.77 cnf(233730,plain, % 122.39/122.77 (~P3(a5,a4)+P6(a1,a4,a3)), % 122.39/122.77 inference(scs_inference,[],[233629,228170])). % 122.39/122.77 cnf(234381,plain, % 122.39/122.77 (P6(a1,a5,a3)+~P6(a5,a4,a1)), % 122.39/122.77 inference(scs_inference,[],[233094,228178])). % 122.39/122.77 cnf(234807,plain, % 122.39/122.77 (~P6(a1,a4,a3)+~P6(a5,a4,a1)), % 122.39/122.77 inference(scs_inference,[],[29,234381,40])). % 122.39/122.77 cnf(235037,plain, % 122.39/122.77 (P6(x2350371,x2350371,x2350371)), % 122.39/122.77 inference(rename_variables,[],[20])). % 122.39/122.77 cnf(235044,plain, % 122.39/122.77 (~P3(a5,a1)+~P6(a1,a4,a5)), % 122.39/122.77 inference(scs_inference,[],[21,20,235037,6,8,9,19,99,34,38,36,35,233521])). % 122.39/122.77 cnf(235733,plain, % 122.39/122.77 (P6(a1,a4,a3)+~P3(a5,a1)), % 122.39/122.77 inference(scs_inference,[],[235044,228170])). % 122.39/122.77 cnf(235963,plain, % 122.39/122.77 (~P3(a5,a1)+~P6(a5,a4,a1)), % 122.39/122.77 inference(scs_inference,[],[235733,234807])). % 122.39/122.77 cnf(242631,plain, % 122.39/122.77 (P4(x2426311,x2426312)+~P5(x2426313,x2426312)+~P3(x2426313,x2426314)+~P6(x2426313,a1,x2426311)+~P2(x2426314,a2)), % 122.39/122.77 inference(rename_variables,[],[38])). % 122.39/122.77 cnf(242632,plain, % 122.39/122.77 (~P3(a3,a1)+~P6(a3,a1,a5)), % 122.39/122.77 inference(scs_inference,[],[32,9,20,6,19,99,7,21,34,38,242631])). % 122.39/122.77 cnf(242736,plain, % 122.39/122.77 (~P3(a3,a1)+P6(a3,a1,a4)), % 122.39/122.77 inference(scs_inference,[],[242632,228247])). % 122.39/122.77 cnf(242837,plain, % 122.39/122.77 (P3(a3,a3)+P6(a3,a1,a4)), % 122.39/122.77 inference(scs_inference,[],[242736,230283])). % 122.39/122.77 cnf(242868,plain, % 122.39/122.77 (~P3(a3,a3)+~P6(a4,a1,a3)), % 122.39/122.77 inference(scs_inference,[],[9,19,8,26,34,38,228886])). % 122.39/122.77 cnf(243466,plain, % 122.39/122.77 (P6(a3,a1,a4)+~P6(a4,a1,a3)), % 122.39/122.77 inference(scs_inference,[],[242868,242837])). % 122.39/122.77 cnf(243901,plain, % 122.39/122.77 (~P3(a3,a2)+~P6(a4,a1,a3)), % 122.39/122.77 inference(scs_inference,[],[243466,227966])). % 122.39/122.77 cnf(244014,plain, % 122.39/122.77 (P3(a3,a3)+P3(a3,a1)+~P6(a4,a1,a3)), % 122.39/122.77 inference(scs_inference,[],[243901,229411])). % 122.39/122.77 cnf(250218,plain, % 122.39/122.77 (~P3(a5,a3)+~P3(a4,a1)), % 122.39/122.77 inference(scs_inference,[],[8,22,9,20,6,21,7,19,99,34,38,35])). % 122.39/122.77 cnf(250272,plain, % 122.39/122.77 (P3(a4,a2)+~P3(a5,a3)), % 122.39/122.77 inference(scs_inference,[],[250218,228057])). % 122.39/122.77 cnf(250377,plain, % 122.39/122.77 (~P6(a4,a1,a5)+~P3(a5,a3)), % 122.39/122.77 inference(scs_inference,[],[250272,228080])). % 122.39/122.77 cnf(250482,plain, % 122.39/122.77 (P6(a4,a1,a3)+~P3(a5,a3)), % 122.39/122.77 inference(scs_inference,[],[250377,228237])). % 122.39/122.77 cnf(250582,plain, % 122.39/122.77 (~P3(a5,a3)+~P6(a1,a4,a5)), % 122.39/122.77 inference(scs_inference,[],[250482,231723])). % 122.39/122.77 cnf(250684,plain, % 122.39/122.77 (P6(a1,a4,a3)+~P3(a5,a3)), % 122.39/122.77 inference(scs_inference,[],[250582,228170])). % 122.39/122.77 cnf(250788,plain, % 122.39/122.77 (~P3(a5,a3)+~P6(a5,a4,a1)), % 122.39/122.77 inference(scs_inference,[],[250684,234807])). % 122.39/122.77 cnf(315799,plain, % 122.39/122.77 (P6(x3157991,x3157991,x3157991)), % 122.39/122.77 inference(rename_variables,[],[20])). % 122.39/122.77 cnf(315810,plain, % 122.39/122.77 (P3(a4,a1)+~P6(a3,a1,a4)), % 122.39/122.77 inference(scs_inference,[],[1,19,99,5,6,20,315799,21,3,30,15,227871,228151,227879,34,36,38,35,42,43,233521])). % 122.39/122.77 cnf(315821,plain, % 122.39/122.77 (~P6(a3,a1,a4)+~P6(a1,a5,a3)), % 122.39/122.77 inference(scs_inference,[],[1,19,99,5,6,20,315799,22,21,3,30,15,227871,228151,227879,34,36,38,35,42,43,233521,233431,250684,233730,232986,230718,228261,235044,231723,232651,39,230387,41])). % 122.39/122.77 cnf(315825,plain, % 122.39/122.77 (P6(x3158251,x3158251,x3158251)), % 122.39/122.77 inference(rename_variables,[],[20])). % 122.39/122.77 cnf(315834,plain, % 122.39/122.77 (~P6(x3158341,a5,a1)+~P6(a5,a1,x3158341)), % 122.39/122.77 inference(scs_inference,[],[19,99,5,6,20,315825,21,30,15,228172,36,34,38,35,42])). % 122.39/122.77 cnf(315836,plain, % 122.39/122.77 (~P6(a3,a5,a1)+P6(a5,a1,a4)), % 122.39/122.77 inference(scs_inference,[],[1,19,99,5,6,20,315825,21,30,15,4,228172,228025,228179,36,34,38,35,42,43])). % 122.39/122.77 cnf(315838,plain, % 122.39/122.77 (P6(a5,a3,a1)+~P6(a3,a5,a1)), % 122.39/122.77 inference(scs_inference,[],[1,19,99,5,6,20,315825,21,30,15,4,228172,228025,228179,36,34,38,35,42,43,230603])). % 122.39/122.77 cnf(315839,plain, % 122.39/122.77 (~P6(a3,a5,a1)+~P6(a3,a1,a4)), % 122.39/122.77 inference(scs_inference,[],[1,19,99,5,26,6,20,315825,21,30,15,4,228172,228025,228179,36,34,38,35,42,43,230603,41])). % 122.39/122.77 cnf(315843,plain, % 122.39/122.77 (P6(x3158431,x3158431,x3158431)), % 122.39/122.77 inference(rename_variables,[],[20])). % 122.39/122.77 cnf(315852,plain, % 122.39/122.77 (~P6(a3,a1,a5)+P6(a1,a5,a4)), % 122.39/122.77 inference(scs_inference,[],[6,20,315843,21,15,1,4,19,99,228172,228025,228040,36,34,38,42,43])). % 122.39/122.77 cnf(315854,plain, % 122.39/122.77 (P6(a5,a4,a3)+~P6(a3,a1,a5)), % 122.39/122.77 inference(scs_inference,[],[6,20,315843,21,15,1,4,19,99,228172,228025,228040,36,34,38,42,43,231842])). % 122.39/122.77 cnf(315862,plain, % 122.39/122.77 (P6(x3158621,x3158621,x3158621)), % 122.39/122.77 inference(rename_variables,[],[20])). % 122.39/122.77 cnf(315869,plain, % 122.39/122.77 (~P6(x3158691,a5,a3)+~P6(a5,a3,x3158691)), % 122.39/122.77 inference(scs_inference,[],[6,20,315862,21,15,19,99,228072,36,34,38,42])). % 122.39/122.77 cnf(315899,plain, % 122.39/122.77 (P6(x3158991,x3158991,x3158991)), % 122.39/122.77 inference(rename_variables,[],[20])). % 122.39/122.77 cnf(315906,plain, % 122.39/122.77 (~P6(x3159061,a4,a1)+~P6(a4,a1,x3159061)), % 122.39/122.77 inference(scs_inference,[],[6,20,315899,21,15,19,99,228151,36,34,38,42])). % 122.39/122.77 cnf(315919,plain, % 122.39/122.77 (P6(x3159191,x3159191,x3159191)), % 122.39/122.77 inference(rename_variables,[],[20])). % 122.39/122.77 cnf(315933,plain, % 122.39/122.77 (~P6(a3,a5,a4)+~P6(a1,a5,a4)), % 122.39/122.77 inference(scs_inference,[],[6,20,315919,21,3,15,19,4,99,227953,228229,227959,34,36,38,42,43,315854,234381,315821,250788,235963,233094])). % 122.39/122.77 cnf(315954,plain, % 122.39/122.77 (~P6(a3,a1,a4)+~P3(a3,a1)), % 122.39/122.77 inference(scs_inference,[],[315810,230316])). % 122.39/122.77 cnf(315984,plain, % 122.39/122.77 (P6(x3159841,x3159841,x3159841)), % 122.39/122.77 inference(rename_variables,[],[20])). % 122.39/122.77 cnf(315991,plain, % 122.39/122.77 (~P6(x3159911,a4,a3)+~P6(a4,a3,x3159911)), % 122.39/122.77 inference(scs_inference,[],[6,20,315984,21,15,19,99,227911,36,34,38,42])). % 122.39/122.77 cnf(315993,plain, % 122.39/122.77 (~P6(a5,a4,a3)+P6(a4,a3,a1)), % 122.39/122.77 inference(scs_inference,[],[2,6,20,315984,21,3,15,19,99,227917,227989,227911,36,34,38,42,43])). % 122.39/122.77 cnf(316001,plain, % 122.39/122.77 (P6(x3160011,x3160011,x3160011)), % 122.39/122.77 inference(rename_variables,[],[20])). % 122.39/122.77 cnf(316010,plain, % 122.39/122.77 (P3(a3,a3)+~P6(a4,a3,a1)), % 122.39/122.77 inference(scs_inference,[],[2,6,20,316001,21,15,1,19,99,227889,228193,228206,34,36,38,42,43,242837])). % 122.39/122.77 cnf(316011,plain, % 122.39/122.77 (P6(a1,a5,a4)+~P6(a4,a3,a1)), % 122.39/122.77 inference(scs_inference,[],[2,6,20,316001,21,15,1,19,99,227889,228193,228206,34,36,38,42,43,242837,315852])). % 122.39/122.77 cnf(316013,plain, % 122.39/122.77 (~P6(a4,a3,a1)+~P6(a3,a5,a4)), % 122.39/122.77 inference(scs_inference,[],[2,6,20,316001,21,15,1,19,99,227889,228193,228206,34,36,38,42,43,242837,315852,242736,315933])). % 122.39/122.77 cnf(317622,plain, % 122.39/122.77 (~P3(a3,a1)), % 122.39/122.77 inference(scs_inference,[],[315954,242736])). % 122.39/122.77 cnf(317629,plain, % 122.39/122.77 (P3(a3,a3)+~P6(a4,a1,a3)), % 122.39/122.77 inference(scs_inference,[],[317622,244014])). % 122.39/122.77 cnf(320014,plain, % 122.39/122.77 (~P6(a4,a1,a3)), % 122.39/122.77 inference(scs_inference,[],[317629,242868])). % 122.39/122.77 cnf(320015,plain, % 122.39/122.77 (P6(a4,a1,a5)), % 122.39/122.77 inference(scs_inference,[],[320014,228237])). % 122.39/122.77 cnf(320044,plain, % 122.39/122.77 (P6(x3200441,x3200441,x3200441)), % 122.39/122.77 inference(rename_variables,[],[20])). % 122.39/122.77 cnf(320065,plain, % 122.39/122.77 ($false), % 122.39/122.77 inference(scs_inference,[],[2,6,20,320044,15,19,21,99,22,4,30,228025,228072,228122,320015,315906,228287,315993,316010,316013,315991,34,36,42,40,39,38,43,315838,315836,315839,315834,228886,315869,316011]), % 122.39/122.77 ['proof']). % 122.64/122.99 % SZS output end Proof % 122.64/122.99 % Total time :121.290000s %------------------------------------------------------------------------------