%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP124-8.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 : n023.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:50 EDT 2024 % Result : Unsatisfiable 69.38s 69.43s % Output : CNFRefutation 69.72s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GRP124-8.004 : TPTP v8.2.0. Released v1.2.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n023.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Thu Jun 20 10:34:09 EDT 2024 % 0.13/0.33 % CPUTime : % 0.54/0.56 start to proof:theBenchmark % 69.38/69.40 %------------------------------------------- % 69.38/69.40 % File :CSE---1.7 % 69.38/69.40 % Problem :theBenchmark % 69.38/69.40 % Transform :cnf % 69.38/69.40 % Format :tptp:raw % 69.38/69.40 % Command :java -jar mcs_scs.jar %d %s % 69.38/69.40 % 69.38/69.40 % Result :Theorem 68.790000s % 69.38/69.40 % Output :CNFRefutation 68.790000s % 69.38/69.40 %------------------------------------------- % 69.38/69.42 %-------------------------------------------------------------------------- % 69.38/69.42 % File : GRP124-8.004 : TPTP v8.2.0. Released v1.2.0. % 69.38/69.42 % Domain : Group Theory (Quasigroups) % 69.38/69.42 % Problem : (3,1,2) conjugate orthogonality % 69.38/69.42 % Version : [Sla93] axioms : Augmented. % 69.38/69.42 % Theorem formulation : Uses a second group. % 69.38/69.42 % English : If ab=xy and a*b = x*y then a=x and b=y, where c*a=b iff ab=c. % 69.38/69.42 % Generate the multiplication table for the specified quasi- % 69.38/69.42 % group with 4 elements. % 69.38/69.42 % 69.38/69.42 % Refs : [FSB93] Fujita et al. (1993), Automatic Generation of Some Res % 69.38/69.42 % : [Sla93] Slaney (1993), Email to G. Sutcliffe % 69.38/69.42 % : [SFS95] Slaney et al. (1995), Automated Reasoning and Exhausti % 69.38/69.42 % Source : [TPTP] % 69.38/69.42 % Names : % 69.38/69.42 % 69.38/69.42 % Status : Unsatisfiable % 69.38/69.42 % Rating : 0.00 v2.3.0, 0.33 v2.2.1, 0.00 v2.1.0 % 69.38/69.42 % Syntax : Number of clauses : 48 ( 33 unt; 3 nHn; 46 RR) % 69.38/69.42 % Number of literals : 94 ( 0 equ; 51 neg) % 69.38/69.42 % Maximal clause size : 6 ( 1 avg) % 69.38/69.42 % Maximal term depth : 1 ( 1 avg) % 69.38/69.42 % Number of predicates : 8 ( 8 usr; 0 prp; 1-3 aty) % 69.38/69.42 % Number of functors : 5 ( 5 usr; 5 con; 0-0 aty) % 69.38/69.42 % Number of variables : 54 ( 0 sgn) % 69.38/69.42 % SPC : CNF_UNS_EPR_NEQ_NHN % 69.38/69.42 % 69.38/69.42 % Comments : [SFS93]'s axiomatization has been modified for this. % 69.38/69.42 % : Substitution axioms are not needed, as any positive equality % 69.38/69.42 % literals should resolve on negative ones directly. % 69.38/69.42 % : Version 8 has complex isomorphism avoidance (mentioned in % 69.38/69.42 % [SFS95] % 69.38/69.42 % : tptp2X: -f tptp -s4 GRP124-8.g % 69.38/69.42 %-------------------------------------------------------------------------- % 69.38/69.42 cnf(e_0_then_e_1,axiom, % 69.38/69.42 next(e_0,e_1) ). % 69.38/69.42 % 69.38/69.42 cnf(e_1_then_e_2,axiom, % 69.38/69.42 next(e_1,e_2) ). % 69.38/69.42 % 69.38/69.42 cnf(e_2_then_e_3,axiom, % 69.38/69.42 next(e_2,e_3) ). % 69.38/69.42 % 69.38/69.42 cnf(e_3_then_e_4,axiom, % 69.38/69.42 next(e_3,e_4) ). % 69.38/69.42 % 69.38/69.42 cnf(e_1_greater_e_0,axiom, % 69.38/69.42 greater(e_1,e_0) ). % 69.38/69.42 % 69.38/69.42 cnf(e_2_greater_e_0,axiom, % 69.38/69.42 greater(e_2,e_0) ). % 69.38/69.42 % 69.38/69.42 cnf(e_3_greater_e_0,axiom, % 69.38/69.42 greater(e_3,e_0) ). % 69.38/69.42 % 69.38/69.42 cnf(e_4_greater_e_0,axiom, % 69.38/69.42 greater(e_4,e_0) ). % 69.38/69.42 % 69.38/69.42 cnf(e_2_greater_e_1,axiom, % 69.38/69.42 greater(e_2,e_1) ). % 69.38/69.42 % 69.38/69.42 cnf(e_3_greater_e_1,axiom, % 69.38/69.42 greater(e_3,e_1) ). % 69.38/69.42 % 69.38/69.42 cnf(e_4_greater_e_1,axiom, % 69.38/69.42 greater(e_4,e_1) ). % 69.38/69.42 % 69.38/69.42 cnf(e_3_greater_e_2,axiom, % 69.38/69.42 greater(e_3,e_2) ). % 69.38/69.42 % 69.38/69.42 cnf(e_4_greater_e_2,axiom, % 69.38/69.42 greater(e_4,e_2) ). % 69.38/69.42 % 69.38/69.42 cnf(e_4_greater_e_3,axiom, % 69.38/69.42 greater(e_4,e_3) ). % 69.38/69.42 % 69.38/69.42 cnf(cycle1,axiom, % 69.38/69.42 ( ~ cycle(X,Y) % 69.38/69.42 | ~ cycle(X,Z) % 69.38/69.42 | equalish(Y,Z) ) ). % 69.38/69.42 % 69.38/69.42 cnf(cycle2,axiom, % 69.38/69.42 ( ~ group_element(X) % 69.38/69.42 | cycle(X,e_0) % 69.38/69.42 | cycle(X,e_1) % 69.38/69.42 | cycle(X,e_2) % 69.38/69.42 | cycle(X,e_3) ) ). % 69.38/69.42 % 69.38/69.42 cnf(cycle3,axiom, % 69.38/69.42 cycle(e_4,e_0) ). % 69.38/69.42 % 69.38/69.42 cnf(cycle4,axiom, % 69.38/69.42 ( ~ cycle(X,Y) % 69.38/69.42 | ~ cycle(W,Z) % 69.38/69.42 | ~ next(X,W) % 69.38/69.42 | ~ greater(Y,e_0) % 69.38/69.42 | ~ next(Z,Z1) % 69.38/69.42 | equalish(Y,Z1) ) ). % 69.38/69.42 % 69.38/69.42 cnf(cycle5,axiom, % 69.38/69.42 ( ~ cycle(X,Z1) % 69.38/69.42 | ~ cycle(Y,e_0) % 69.38/69.42 | ~ cycle(W,Z2) % 69.38/69.42 | ~ next(Y,W) % 69.38/69.42 | ~ greater(Y,X) % 69.38/69.42 | ~ greater(Z1,Z2) ) ). % 69.38/69.42 % 69.38/69.42 cnf(cycle6,axiom, % 69.38/69.42 ( ~ cycle(X,e_0) % 69.38/69.42 | ~ product(X,e_1,Y) % 69.38/69.42 | ~ greater(Y,X) ) ). % 69.38/69.42 % 69.38/69.42 cnf(cycle7,axiom, % 69.38/69.42 ( ~ cycle(X,Y) % 69.38/69.42 | ~ product(X,e_1,Z) % 69.38/69.42 | ~ greater(Y,e_0) % 69.38/69.42 | ~ next(X,X1) % 69.38/69.42 | equalish(Z,X1) ) ). % 69.38/69.42 % 69.38/69.42 cnf(element_1,axiom, % 69.38/69.42 group_element(e_1) ). % 69.38/69.42 % 69.38/69.42 cnf(element_2,axiom, % 69.38/69.42 group_element(e_2) ). % 69.38/69.42 % 69.38/69.42 cnf(element_3,axiom, % 69.38/69.42 group_element(e_3) ). % 69.38/69.42 % 69.38/69.42 cnf(element_4,axiom, % 69.38/69.42 group_element(e_4) ). % 69.38/69.42 % 69.38/69.42 cnf(e_1_is_not_e_2,axiom, % 69.38/69.42 ~ equalish(e_1,e_2) ). % 69.38/69.42 % 69.38/69.42 cnf(e_1_is_not_e_3,axiom, % 69.38/69.42 ~ equalish(e_1,e_3) ). % 69.38/69.42 % 69.38/69.42 cnf(e_1_is_not_e_4,axiom, % 69.38/69.42 ~ equalish(e_1,e_4) ). % 69.38/69.42 % 69.38/69.42 cnf(e_2_is_not_e_1,axiom, % 69.38/69.42 ~ equalish(e_2,e_1) ). % 69.38/69.42 % 69.38/69.42 cnf(e_2_is_not_e_3,axiom, % 69.38/69.42 ~ equalish(e_2,e_3) ). % 69.38/69.42 % 69.38/69.42 cnf(e_2_is_not_e_4,axiom, % 69.38/69.42 ~ equalish(e_2,e_4) ). % 69.38/69.42 % 69.38/69.42 cnf(e_3_is_not_e_1,axiom, % 69.38/69.42 ~ equalish(e_3,e_1) ). % 69.38/69.42 % 69.38/69.42 cnf(e_3_is_not_e_2,axiom, % 69.38/69.42 ~ equalish(e_3,e_2) ). % 69.38/69.42 % 69.38/69.42 cnf(e_3_is_not_e_4,axiom, % 69.38/69.42 ~ equalish(e_3,e_4) ). % 69.38/69.42 % 69.38/69.42 cnf(e_4_is_not_e_1,axiom, % 69.38/69.42 ~ equalish(e_4,e_1) ). % 69.38/69.42 % 69.38/69.42 cnf(e_4_is_not_e_2,axiom, % 69.38/69.42 ~ equalish(e_4,e_2) ). % 69.38/69.42 % 69.38/69.42 cnf(e_4_is_not_e_3,axiom, % 69.38/69.42 ~ equalish(e_4,e_3) ). % 69.38/69.42 % 69.38/69.42 cnf(product1_total_function1,axiom, % 69.38/69.42 ( ~ group_element(X) % 69.38/69.42 | ~ group_element(Y) % 69.38/69.42 | product1(X,Y,e_1) % 69.38/69.42 | product1(X,Y,e_2) % 69.38/69.42 | product1(X,Y,e_3) % 69.38/69.42 | product1(X,Y,e_4) ) ). % 69.38/69.42 % 69.38/69.42 cnf(product1_total_function2,axiom, % 69.38/69.42 ( ~ product1(X,Y,W) % 69.38/69.42 | ~ product1(X,Y,Z) % 69.38/69.42 | equalish(W,Z) ) ). % 69.38/69.42 % 69.38/69.42 cnf(product1_right_cancellation,axiom, % 69.38/69.42 ( ~ product1(X,W,Y) % 69.38/69.42 | ~ product1(X,Z,Y) % 69.38/69.42 | equalish(W,Z) ) ). % 69.38/69.42 % 69.38/69.42 cnf(product1_left_cancellation,axiom, % 69.38/69.42 ( ~ product1(W,Y,X) % 69.38/69.42 | ~ product1(Z,Y,X) % 69.38/69.42 | equalish(W,Z) ) ). % 69.38/69.42 % 69.38/69.42 cnf(product1_idempotence,axiom, % 69.38/69.42 product1(X,X,X) ). % 69.38/69.42 % 69.38/69.42 cnf(product2_total_function1,axiom, % 69.38/69.42 ( ~ group_element(X) % 69.38/69.42 | ~ group_element(Y) % 69.38/69.42 | product2(X,Y,e_1) % 69.38/69.42 | product2(X,Y,e_2) % 69.38/69.42 | product2(X,Y,e_3) % 69.38/69.42 | product2(X,Y,e_4) ) ). % 69.38/69.42 % 69.38/69.42 cnf(product2_total_function2,axiom, % 69.38/69.42 ( ~ product2(X,Y,W) % 69.38/69.42 | ~ product2(X,Y,Z) % 69.38/69.42 | equalish(W,Z) ) ). % 69.38/69.42 % 69.38/69.42 cnf(product2_right_cancellation,axiom, % 69.38/69.42 ( ~ product2(X,W,Y) % 69.38/69.42 | ~ product2(X,Z,Y) % 69.38/69.42 | equalish(W,Z) ) ). % 69.38/69.42 % 69.38/69.42 cnf(product2_left_cancellation,axiom, % 69.38/69.42 ( ~ product2(W,Y,X) % 69.38/69.42 | ~ product2(Z,Y,X) % 69.38/69.42 | equalish(W,Z) ) ). % 69.38/69.42 % 69.38/69.42 cnf(product2_idempotence,axiom, % 69.38/69.42 product2(X,X,X) ). % 69.38/69.43 % 69.38/69.43 cnf(qg2a,negated_conjecture, % 69.38/69.43 ( ~ product1(X,Y,Z1) % 69.38/69.43 | ~ product1(Z1,X,Z2) % 69.38/69.43 | product2(Z2,Y,X) ) ). % 69.38/69.43 % 69.38/69.43 %-------------------------------------------------------------------------- % 69.38/69.43 %------------------------------------------- % 69.38/69.43 % Proof found % 69.38/69.43 % SZS status Theorem for theBenchmark % 69.38/69.43 % SZS output start Proof % 69.38/69.43 %ClaNum:48(EqnAxiom:0) % 69.38/69.43 %VarNum:130(SingletonVarNum:54) % 69.38/69.43 %MaxLitNum:6 % 69.38/69.43 %MaxfuncDepth:0 % 69.38/69.43 %SharedTerms:36 % 69.38/69.43 %goalClause: 46 % 69.38/69.43 [1]P1(a1) % 69.38/69.43 [2]P1(a3) % 69.38/69.43 [3]P1(a4) % 69.38/69.43 [4]P1(a5) % 69.38/69.43 [5]P5(a2,a1) % 69.38/69.43 [6]P5(a1,a3) % 69.38/69.43 [7]P5(a3,a4) % 69.38/69.43 [8]P5(a4,a5) % 69.38/69.43 [9]P2(a1,a2) % 69.38/69.43 [10]P2(a3,a2) % 69.38/69.43 [11]P2(a3,a1) % 69.38/69.43 [12]P2(a4,a2) % 69.38/69.43 [13]P2(a4,a1) % 69.38/69.43 [14]P2(a4,a3) % 69.38/69.43 [15]P2(a5,a2) % 69.38/69.43 [16]P2(a5,a1) % 69.38/69.43 [17]P2(a5,a3) % 69.38/69.43 [18]P2(a5,a4) % 69.38/69.43 [19]P3(a5,a2) % 69.38/69.43 [22]~P4(a1,a3) % 69.38/69.43 [23]~P4(a1,a4) % 69.38/69.43 [24]~P4(a1,a5) % 69.38/69.43 [25]~P4(a3,a1) % 69.38/69.43 [26]~P4(a3,a4) % 69.38/69.43 [27]~P4(a3,a5) % 69.38/69.43 [28]~P4(a4,a1) % 69.38/69.43 [29]~P4(a4,a3) % 69.38/69.43 [30]~P4(a4,a5) % 69.38/69.43 [31]~P4(a5,a1) % 69.38/69.43 [32]~P4(a5,a3) % 69.38/69.43 [33]~P4(a5,a4) % 69.38/69.43 [20]P6(x201,x201,x201) % 69.38/69.43 [21]P8(x211,x211,x211) % 69.38/69.43 [37]~P2(x371,x372)+~P7(x372,a1,x371)+~P3(x372,a2) % 69.38/69.43 [35]~P3(x353,x351)+P4(x351,x352)+~P3(x353,x352) % 69.38/69.43 [40]~P6(x403,x404,x401)+P4(x401,x402)+~P6(x403,x404,x402) % 69.38/69.43 [41]~P8(x413,x414,x411)+P4(x411,x412)+~P8(x413,x414,x412) % 69.38/69.43 [42]~P6(x423,x421,x424)+P4(x421,x422)+~P6(x423,x422,x424) % 69.38/69.43 [43]~P8(x433,x431,x434)+P4(x431,x432)+~P8(x433,x432,x434) % 69.38/69.43 [44]~P6(x441,x443,x444)+P4(x441,x442)+~P6(x442,x443,x444) % 69.38/69.43 [45]~P8(x451,x453,x454)+P4(x451,x452)+~P8(x452,x453,x454) % 69.38/69.43 [46]~P6(x463,x462,x464)+P8(x461,x462,x463)+~P6(x464,x463,x461) % 69.38/69.43 [34]~P1(x341)+P3(x341,a1)+P3(x341,a3)+P3(x341,a4)+P3(x341,a2) % 69.38/69.43 [39]P4(x391,x392)+~P5(x393,x392)+~P3(x393,x394)+~P7(x393,a1,x391)+~P2(x394,a2) % 69.38/69.43 [47]~P1(x472)+~P1(x471)+P6(x471,x472,a3)+P6(x471,x472,a4)+P6(x471,x472,a5)+P6(x471,x472,a1) % 69.38/69.43 [48]~P1(x482)+~P1(x481)+P8(x481,x482,a3)+P8(x481,x482,a4)+P8(x481,x482,a5)+P8(x481,x482,a1) % 69.38/69.43 [36]~P3(x365,x363)+~P3(x364,x361)+P4(x361,x362)+~P5(x363,x362)+~P5(x364,x365)+~P2(x361,a2) % 69.38/69.43 [38]~P3(x382,x385)+~P3(x383,x384)+~P5(x381,x382)+~P2(x381,x383)+~P2(x384,x385)+~P3(x381,a2) % 69.38/69.43 %EqnAxiom % 69.38/69.43 % 69.38/69.43 %------------------------------------------- % 69.61/69.60 cnf(1197,plain, % 69.61/69.60 (~P6(x11971,a3,a1)+~P6(a3,a1,x11971)), % 69.61/69.60 inference(scs_inference,[],[21,22,41,46])). % 69.61/69.60 cnf(1372,plain, % 69.61/69.60 (~P6(x13721,a1,a4)+~P6(a1,a4,x13721)), % 69.61/69.60 inference(scs_inference,[],[23,21,41,46])). % 69.61/69.60 cnf(1541,plain, % 69.61/69.60 (~P6(x15411,a4,a3)+~P6(a4,a3,x15411)), % 69.61/69.60 inference(scs_inference,[],[26,21,41,46])). % 69.61/69.60 cnf(1895,plain, % 69.61/69.60 (~P6(x18951,a3,a4)+~P6(a3,a4,x18951)), % 69.61/69.60 inference(scs_inference,[],[29,21,41,46])). % 69.61/69.60 cnf(2066,plain, % 69.61/69.60 (~P6(x20661,a4,a5)+~P6(a4,a5,x20661)), % 69.61/69.60 inference(scs_inference,[],[30,21,41,46])). % 69.61/69.60 cnf(2310,plain, % 69.61/69.60 (P6(a3,a4,a4)+P6(a3,a4,a5)+P6(a3,a4,a1)), % 69.61/69.60 inference(scs_inference,[],[20,26,3,2,42,47])). % 69.61/69.60 cnf(6436,plain, % 69.61/69.60 (~P6(a5,a3,a5)), % 69.61/69.60 inference(scs_inference,[],[27,21,20,43,46])). % 69.61/69.60 cnf(6537,plain, % 69.61/69.60 (P6(a5,a3,a4)+P6(a5,a3,a1)), % 69.61/69.60 inference(scs_inference,[],[20,27,6436,2,4,44,47])). % 69.61/69.60 cnf(6587,plain, % 69.61/69.60 (~P6(a3,a4,a5)+P6(a5,a3,a1)), % 69.61/69.60 inference(scs_inference,[],[6537,1895])). % 69.61/69.60 cnf(256471,plain, % 69.61/69.60 (~P6(a4,a5,a4)), % 69.61/69.60 inference(scs_inference,[],[30,20,42])). % 69.61/69.60 cnf(256472,plain, % 69.61/69.60 (P6(x2564721,x2564721,x2564721)), % 69.61/69.60 inference(rename_variables,[],[20])). % 69.61/69.60 cnf(256475,plain, % 69.61/69.60 (P8(x2564751,x2564751,x2564751)), % 69.61/69.60 inference(rename_variables,[],[21])). % 69.61/69.60 cnf(256478,plain, % 69.61/69.60 (P6(x2564781,x2564781,x2564781)), % 69.61/69.60 inference(rename_variables,[],[20])). % 69.61/69.60 cnf(256486,plain, % 69.61/69.60 (P8(x2564861,x2564861,x2564861)), % 69.61/69.60 inference(rename_variables,[],[21])). % 69.61/69.60 cnf(256491,plain, % 69.61/69.60 (~P6(x2564911,a5,a3)+~P6(a5,a3,x2564911)), % 69.61/69.60 inference(scs_inference,[],[27,30,20,256472,256478,21,256475,256486,19,42,41,44,35,40,43,45,46])). % 69.61/69.60 cnf(256499,plain, % 69.61/69.60 (P6(x2564991,x2564991,x2564991)), % 69.61/69.60 inference(rename_variables,[],[20])). % 69.61/69.60 cnf(256501,plain, % 69.61/69.60 (~P6(a5,a4,a4)), % 69.61/69.60 inference(scs_inference,[],[30,26,20,256499,42,44])). % 69.61/69.60 cnf(256502,plain, % 69.61/69.60 (P6(x2565021,x2565021,x2565021)), % 69.61/69.60 inference(rename_variables,[],[20])). % 69.61/69.60 cnf(256508,plain, % 69.61/69.60 (P8(x2565081,x2565081,x2565081)), % 69.61/69.60 inference(rename_variables,[],[21])). % 69.61/69.60 cnf(256510,plain, % 69.61/69.60 (~P8(a4,a4,a5)), % 69.61/69.60 inference(scs_inference,[],[30,26,20,256499,256502,21,256508,42,44,40,43,41])). % 69.61/69.60 cnf(256521,plain, % 69.61/69.60 (P6(x2565211,x2565211,x2565211)), % 69.61/69.60 inference(rename_variables,[],[20])). % 69.61/69.60 cnf(256524,plain, % 69.61/69.60 (P6(x2565241,x2565241,x2565241)), % 69.61/69.61 inference(rename_variables,[],[20])). % 69.61/69.61 cnf(256530,plain, % 69.61/69.61 (P8(x2565301,x2565301,x2565301)), % 69.61/69.61 inference(rename_variables,[],[21])). % 69.61/69.61 cnf(256535,plain, % 69.61/69.61 (P8(x2565351,x2565351,x2565351)), % 69.61/69.61 inference(rename_variables,[],[21])). % 69.61/69.61 cnf(256542,plain, % 69.61/69.61 (P6(a4,a3,a1)+P6(a4,a3,a5)), % 69.61/69.61 inference(scs_inference,[],[26,29,20,256521,256524,12,3,17,21,256530,256535,19,2,42,40,44,41,35,45,43,38,47])). % 69.61/69.61 cnf(256544,plain, % 69.61/69.61 (~P6(a1,a4,a1)), % 69.61/69.61 inference(scs_inference,[],[23,20,42])). % 69.61/69.61 cnf(256545,plain, % 69.61/69.61 (P6(x2565451,x2565451,x2565451)), % 69.61/69.61 inference(rename_variables,[],[20])). % 69.61/69.61 cnf(256548,plain, % 69.61/69.61 (P6(x2565481,x2565481,x2565481)), % 69.61/69.61 inference(rename_variables,[],[20])). % 69.61/69.61 cnf(256556,plain, % 69.61/69.61 (P6(a5,a3,a1)+P6(a3,a4,a1)), % 69.61/69.61 inference(scs_inference,[],[29,23,20,256545,256548,42,44,40,2310,2066,6587])). % 69.61/69.61 cnf(256562,plain, % 69.61/69.61 (~P6(a3,a1,a3)), % 69.61/69.61 inference(scs_inference,[],[20,25,42])). % 69.61/69.61 cnf(256576,plain, % 69.61/69.61 (P6(x2565761,x2565761,x2565761)), % 69.61/69.61 inference(rename_variables,[],[20])). % 69.61/69.61 cnf(256578,plain, % 69.61/69.61 (~P6(a1,a3,a3)), % 69.61/69.61 inference(scs_inference,[],[20,256576,25,28,42,44])). % 69.61/69.61 cnf(256588,plain, % 69.61/69.61 (~P6(a1,a3,a1)), % 69.61/69.61 inference(scs_inference,[],[20,22,42])). % 69.61/69.61 cnf(256589,plain, % 69.61/69.61 (P6(x2565891,x2565891,x2565891)), % 69.61/69.61 inference(rename_variables,[],[20])). % 69.61/69.61 cnf(256592,plain, % 69.61/69.61 (P6(x2565921,x2565921,x2565921)), % 69.61/69.61 inference(rename_variables,[],[20])). % 69.61/69.61 cnf(256594,plain, % 69.61/69.61 (~P6(a1,a4,a4)), % 69.61/69.61 inference(scs_inference,[],[20,256589,256592,28,22,42,40,44])). % 69.61/69.61 cnf(256599,plain, % 69.61/69.61 (~P6(a5,a4,a5)), % 69.61/69.61 inference(scs_inference,[],[20,33,42])). % 69.61/69.61 cnf(256600,plain, % 69.61/69.61 (P6(x2566001,x2566001,x2566001)), % 69.61/69.61 inference(rename_variables,[],[20])). % 69.61/69.61 cnf(256603,plain, % 69.61/69.61 (P8(x2566031,x2566031,x2566031)), % 69.61/69.61 inference(rename_variables,[],[21])). % 69.61/69.61 cnf(256606,plain, % 69.61/69.61 (P8(x2566061,x2566061,x2566061)), % 69.61/69.61 inference(rename_variables,[],[21])). % 69.61/69.61 cnf(256611,plain, % 69.61/69.61 (~P6(a3,a1,a1)), % 69.61/69.61 inference(scs_inference,[],[29,20,256600,22,21,256603,256606,33,42,45,43,41,44])). % 69.61/69.61 cnf(256612,plain, % 69.61/69.61 (P6(x2566121,x2566121,x2566121)), % 69.61/69.61 inference(rename_variables,[],[20])). % 69.61/69.61 cnf(256621,plain, % 69.61/69.61 (P6(a1,a4,a3)+~P6(a4,a5,a1)), % 69.61/69.61 inference(scs_inference,[],[1,256544,256594,29,20,256600,256612,3,22,21,256603,256606,19,33,42,45,43,41,44,40,35,47,2066])). % 69.61/69.61 cnf(256624,plain, % 69.61/69.61 (~P6(a5,a1,a5)), % 69.61/69.61 inference(scs_inference,[],[20,31,42])). % 69.61/69.61 cnf(256625,plain, % 69.61/69.61 (P6(x2566251,x2566251,x2566251)), % 69.61/69.61 inference(rename_variables,[],[20])). % 69.61/69.61 cnf(256627,plain, % 69.61/69.61 (~P6(a4,a5,a5)), % 69.61/69.61 inference(scs_inference,[],[20,256625,33,31,42,44])). % 69.61/69.61 cnf(256637,plain, % 69.61/69.61 (~P6(a1,a5,a1)), % 69.61/69.61 inference(scs_inference,[],[20,24,42])). % 69.61/69.61 cnf(256650,plain, % 69.61/69.61 (~P6(a1,a5,a5)), % 69.61/69.61 inference(scs_inference,[],[20,31,44])). % 69.61/69.61 cnf(256662,plain, % 69.61/69.61 (~P6(a5,a1,a1)), % 69.61/69.61 inference(scs_inference,[],[20,24,44])). % 69.61/69.61 cnf(256663,plain, % 69.61/69.61 (P6(x2566631,x2566631,x2566631)), % 69.61/69.61 inference(rename_variables,[],[20])). % 69.61/69.61 cnf(256671,plain, % 69.61/69.61 (P8(x2566711,x2566711,x2566711)), % 69.61/69.61 inference(rename_variables,[],[21])). % 69.61/69.61 cnf(256674,plain, % 69.61/69.61 (P8(x2566741,x2566741,x2566741)), % 69.61/69.61 inference(rename_variables,[],[21])). % 69.61/69.61 cnf(256676,plain, % 69.61/69.61 (~P8(a1,a1,a4)), % 69.61/69.61 inference(scs_inference,[],[23,20,256663,21,256671,256674,19,24,44,40,35,43,45,41])). % 69.61/69.61 cnf(256680,plain, % 69.61/69.61 (~P6(x2566801,a4,a1)+~P6(a4,a1,x2566801)), % 69.61/69.61 inference(scs_inference,[],[256676,46])). % 69.61/69.61 cnf(256688,plain, % 69.61/69.61 (P6(a1,a5,a4)+P6(a1,a5,a3)), % 69.61/69.61 inference(scs_inference,[],[1,256637,256650,12,18,4,19,35,38,47])). % 69.61/69.61 cnf(256694,plain, % 69.61/69.61 (P6(a1,a4,a3)+P6(a4,a5,a3)), % 69.61/69.61 inference(scs_inference,[],[256471,256627,3,4,19,35,47,256621])). % 69.61/69.61 cnf(256698,plain, % 69.61/69.61 (P8(x2566981,x2566981,x2566981)), % 69.61/69.61 inference(rename_variables,[],[21])). % 69.61/69.61 cnf(256701,plain, % 69.61/69.61 (P8(x2567011,x2567011,x2567011)), % 69.61/69.61 inference(rename_variables,[],[21])). % 69.61/69.61 cnf(256703,plain, % 69.61/69.61 (~P8(a3,a3,a1)), % 69.61/69.61 inference(scs_inference,[],[25,21,256698,256701,45,43,41])). % 69.61/69.61 cnf(256714,plain, % 69.61/69.61 (~P6(a5,a1,a3)+P6(a1,a3,a4)), % 69.61/69.61 inference(scs_inference,[],[1,256588,256578,256703,19,2,35,46,47])). % 69.61/69.61 cnf(256729,plain, % 69.61/69.61 (~P6(a1,a5,a4)+P6(a5,a4,a3)), % 69.61/69.61 inference(scs_inference,[],[256501,256599,256510,3,4,19,35,47,256680,46])). % 69.61/69.61 cnf(256783,plain, % 69.61/69.61 (P6(a3,a1,a5)+P6(a3,a1,a4)), % 69.61/69.61 inference(scs_inference,[],[1,256562,256611,19,2,35,47])). % 69.61/69.61 cnf(257621,plain, % 69.61/69.61 (P6(a5,a3,a1)+~P6(a4,a5,a3)), % 69.61/69.61 inference(scs_inference,[],[256491,6537])). % 69.61/69.61 cnf(258169,plain, % 69.61/69.61 (P6(a4,a3,a1)+~P6(a5,a4,a3)), % 69.61/69.61 inference(scs_inference,[],[256542,1541])). % 69.61/69.61 cnf(258630,plain, % 69.61/69.61 (P6(a1,a5,a4)+~P6(a5,a3,a1)), % 69.61/69.61 inference(scs_inference,[],[256688,256491])). % 69.61/69.61 cnf(258720,plain, % 69.61/69.61 (P6(a1,a4,a3)+P6(a5,a3,a1)), % 69.61/69.61 inference(scs_inference,[],[256694,257621])). % 69.61/69.61 cnf(258899,plain, % 69.61/69.61 (P6(a4,a3,a1)+~P6(a1,a5,a4)), % 69.61/69.61 inference(scs_inference,[],[256729,258169])). % 69.61/69.61 cnf(259085,plain, % 69.61/69.61 (P6(a3,a1,a5)+~P6(a4,a3,a1)), % 69.61/69.61 inference(scs_inference,[],[256783,1197])). % 69.61/69.61 cnf(260435,plain, % 69.61/69.61 (P6(a3,a1,a5)+~P6(a1,a5,a4)), % 69.61/69.61 inference(scs_inference,[],[258899,259085])). % 69.61/69.61 cnf(262357,plain, % 69.61/69.61 (~P6(a1,a5,a4)+~P6(a5,a3,a1)), % 69.61/69.61 inference(scs_inference,[],[260435,1197])). % 69.61/69.61 cnf(263420,plain, % 69.61/69.61 (~P6(a5,a3,a1)), % 69.61/69.61 inference(scs_inference,[],[262357,258630])). % 69.61/69.61 cnf(263421,plain, % 69.61/69.61 (P6(a5,a3,a4)), % 69.61/69.61 inference(scs_inference,[],[263420,6537])). % 69.61/69.61 cnf(263423,plain, % 69.61/69.61 (P6(a3,a4,a1)), % 69.61/69.61 inference(scs_inference,[],[263420,256556])). % 69.61/69.61 cnf(263426,plain, % 69.61/69.61 (P6(a1,a4,a3)), % 69.61/69.61 inference(scs_inference,[],[263420,258720])). % 69.61/69.61 cnf(263456,plain, % 69.61/69.61 ($false), % 69.61/69.61 inference(scs_inference,[],[263421,263423,263426,256662,256624,19,25,4,1,1895,35,42,47,1372,1541,256542,256714]), % 69.61/69.61 ['proof']). % 69.72/69.74 % SZS output end Proof % 69.72/69.74 % Total time :68.790000s %------------------------------------------------------------------------------