%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP124-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 : n001.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:49 EDT 2024 % Result : Unsatisfiable 66.66s 66.74s % Output : CNFRefutation 67.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : GRP124-3.004 : TPTP v8.2.0. Released v1.2.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n001.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 07:54:54 EDT 2024 % 0.13/0.34 % CPUTime : % 0.43/0.61 start to proof:theBenchmark % 66.66/66.71 %------------------------------------------- % 66.66/66.71 % File :CSE---1.7 % 66.66/66.71 % Problem :theBenchmark % 66.66/66.71 % Transform :cnf % 66.66/66.71 % Format :tptp:raw % 66.66/66.71 % Command :java -jar mcs_scs.jar %d %s % 66.66/66.71 % 66.66/66.71 % Result :Theorem 66.070000s % 66.66/66.71 % Output :CNFRefutation 66.070000s % 66.66/66.71 %------------------------------------------- % 66.66/66.74 %-------------------------------------------------------------------------- % 66.66/66.74 % File : GRP124-3.004 : TPTP v8.2.0. Released v1.2.0. % 66.66/66.74 % Domain : Group Theory (Quasigroups) % 66.66/66.74 % Problem : (3,1,2) conjugate orthogonality % 66.66/66.74 % Version : [Sla93] axioms : Augmented. % 66.66/66.74 % English : If ab=xy and a*b = x*y then a=x and b=y, where c*a=b iff ab=c. % 66.66/66.74 % Generate the multiplication table for the specified quasi- % 66.66/66.74 % group with 4 elements. % 66.66/66.74 % 66.66/66.74 % Refs : [FSB93] Fujita et al. (1993), Automatic Generation of Some Res % 66.66/66.74 % : [Sla93] Slaney (1993), Email to G. Sutcliffe % 66.66/66.74 % : [SFS95] Slaney et al. (1995), Automated Reasoning and Exhausti % 66.66/66.74 % Source : [TPTP] % 66.66/66.74 % Names : % 66.66/66.74 % 66.66/66.74 % Status : Unsatisfiable % 66.66/66.74 % Rating : 0.00 v2.1.0 % 66.66/66.74 % Syntax : Number of clauses : 44 ( 32 unt; 2 nHn; 43 RR) % 66.66/66.74 % Number of literals : 85 ( 0 equ; 49 neg) % 66.66/66.74 % Maximal clause size : 6 ( 1 avg) % 66.66/66.74 % Maximal term depth : 1 ( 1 avg) % 66.66/66.74 % Number of predicates : 6 ( 6 usr; 0 prp; 1-3 aty) % 66.66/66.74 % Number of functors : 5 ( 5 usr; 5 con; 0-0 aty) % 66.66/66.74 % Number of variables : 47 ( 0 sgn) % 66.66/66.74 % SPC : CNF_UNS_EPR_NEQ_NHN % 66.66/66.74 % 66.66/66.74 % Comments : [SFS93]'s axiomatization has been modified for this. % 66.66/66.74 % : Substitution axioms are not needed, as any positive equality % 66.66/66.74 % literals should resolve on negative ones directly. % 66.66/66.74 % : As in GRP123-1, either one of qg2_1 or qg2_2 may be used, as % 66.66/66.74 % each implies the other in this scenario, with the help of % 66.66/66.74 % cancellation. The dependence cannot be proved, so both have % 66.66/66.74 % been left in here. % 66.66/66.74 % : Version 3 has complex isomorphism avoidance (mentioned in % 66.66/66.74 % [SFS95] % 66.66/66.74 % : tptp2X: -f tptp -s4 GRP124-3.g % 66.66/66.74 %-------------------------------------------------------------------------- % 66.66/66.74 cnf(e_0_then_e_1,axiom, % 66.66/66.74 next(e_0,e_1) ). % 66.66/66.74 % 66.66/66.74 cnf(e_1_then_e_2,axiom, % 66.66/66.74 next(e_1,e_2) ). % 66.66/66.74 % 66.66/66.74 cnf(e_2_then_e_3,axiom, % 66.66/66.74 next(e_2,e_3) ). % 66.66/66.74 % 66.66/66.74 cnf(e_3_then_e_4,axiom, % 66.66/66.74 next(e_3,e_4) ). % 66.66/66.74 % 66.66/66.74 cnf(e_1_greater_e_0,axiom, % 66.66/66.74 greater(e_1,e_0) ). % 66.66/66.74 % 66.66/66.74 cnf(e_2_greater_e_0,axiom, % 66.66/66.74 greater(e_2,e_0) ). % 66.66/66.74 % 66.66/66.74 cnf(e_3_greater_e_0,axiom, % 66.66/66.74 greater(e_3,e_0) ). % 66.66/66.74 % 66.66/66.74 cnf(e_4_greater_e_0,axiom, % 66.66/66.74 greater(e_4,e_0) ). % 66.66/66.74 % 66.66/66.74 cnf(e_2_greater_e_1,axiom, % 66.66/66.74 greater(e_2,e_1) ). % 66.66/66.74 % 66.66/66.74 cnf(e_3_greater_e_1,axiom, % 66.66/66.74 greater(e_3,e_1) ). % 66.66/66.74 % 66.66/66.74 cnf(e_4_greater_e_1,axiom, % 66.66/66.74 greater(e_4,e_1) ). % 66.66/66.74 % 66.66/66.74 cnf(e_3_greater_e_2,axiom, % 66.66/66.74 greater(e_3,e_2) ). % 66.66/66.74 % 66.66/66.74 cnf(e_4_greater_e_2,axiom, % 66.66/66.74 greater(e_4,e_2) ). % 66.66/66.74 % 66.66/66.74 cnf(e_4_greater_e_3,axiom, % 66.66/66.74 greater(e_4,e_3) ). % 66.66/66.74 % 66.66/66.74 cnf(cycle1,axiom, % 66.66/66.74 ( ~ cycle(X,Y) % 66.66/66.74 | ~ cycle(X,Z) % 66.66/66.74 | equalish(Y,Z) ) ). % 66.66/66.74 % 66.66/66.74 cnf(cycle2,axiom, % 66.66/66.74 ( ~ group_element(X) % 66.66/66.74 | cycle(X,e_0) % 66.66/66.74 | cycle(X,e_1) % 66.66/66.74 | cycle(X,e_2) % 66.66/66.74 | cycle(X,e_3) ) ). % 66.66/66.74 % 66.66/66.74 cnf(cycle3,axiom, % 66.66/66.74 cycle(e_4,e_0) ). % 66.66/66.74 % 66.66/66.74 cnf(cycle4,axiom, % 66.66/66.74 ( ~ cycle(X,Y) % 66.66/66.74 | ~ cycle(W,Z) % 66.66/66.74 | ~ next(X,W) % 66.66/66.74 | ~ greater(Y,e_0) % 66.66/66.74 | ~ next(Z,Z1) % 66.66/66.74 | equalish(Y,Z1) ) ). % 66.66/66.74 % 66.66/66.74 cnf(cycle5,axiom, % 66.66/66.74 ( ~ cycle(X,Z1) % 66.66/66.74 | ~ cycle(Y,e_0) % 66.66/66.74 | ~ cycle(W,Z2) % 66.66/66.74 | ~ next(Y,W) % 66.66/66.74 | ~ greater(Y,X) % 66.66/66.74 | ~ greater(Z1,Z2) ) ). % 66.66/66.74 % 66.66/66.74 cnf(cycle6,axiom, % 66.66/66.74 ( ~ cycle(X,e_0) % 66.66/66.74 | ~ product(X,e_1,Y) % 66.66/66.74 | ~ greater(Y,X) ) ). % 66.66/66.74 % 66.66/66.74 cnf(cycle7,axiom, % 66.66/66.74 ( ~ cycle(X,Y) % 66.66/66.74 | ~ product(X,e_1,Z) % 66.66/66.74 | ~ greater(Y,e_0) % 66.66/66.74 | ~ next(X,X1) % 66.66/66.74 | equalish(Z,X1) ) ). % 66.66/66.74 % 66.66/66.74 cnf(element_1,axiom, % 66.66/66.74 group_element(e_1) ). % 66.66/66.74 % 66.66/66.74 cnf(element_2,axiom, % 66.66/66.74 group_element(e_2) ). % 66.66/66.74 % 66.66/66.74 cnf(element_3,axiom, % 66.66/66.74 group_element(e_3) ). % 66.66/66.74 % 66.66/66.74 cnf(element_4,axiom, % 66.66/66.74 group_element(e_4) ). % 66.66/66.74 % 66.66/66.74 cnf(e_1_is_not_e_2,axiom, % 66.66/66.74 ~ equalish(e_1,e_2) ). % 66.66/66.74 % 66.66/66.74 cnf(e_1_is_not_e_3,axiom, % 66.66/66.74 ~ equalish(e_1,e_3) ). % 66.66/66.74 % 66.66/66.74 cnf(e_1_is_not_e_4,axiom, % 66.66/66.74 ~ equalish(e_1,e_4) ). % 66.66/66.74 % 66.66/66.74 cnf(e_2_is_not_e_1,axiom, % 66.66/66.74 ~ equalish(e_2,e_1) ). % 66.66/66.74 % 66.66/66.74 cnf(e_2_is_not_e_3,axiom, % 66.66/66.74 ~ equalish(e_2,e_3) ). % 66.66/66.74 % 66.66/66.74 cnf(e_2_is_not_e_4,axiom, % 66.66/66.74 ~ equalish(e_2,e_4) ). % 66.66/66.74 % 66.66/66.74 cnf(e_3_is_not_e_1,axiom, % 66.66/66.74 ~ equalish(e_3,e_1) ). % 66.66/66.74 % 66.66/66.74 cnf(e_3_is_not_e_2,axiom, % 66.66/66.74 ~ equalish(e_3,e_2) ). % 66.66/66.74 % 66.66/66.74 cnf(e_3_is_not_e_4,axiom, % 66.66/66.74 ~ equalish(e_3,e_4) ). % 66.66/66.74 % 66.66/66.74 cnf(e_4_is_not_e_1,axiom, % 66.66/66.74 ~ equalish(e_4,e_1) ). % 66.66/66.74 % 66.66/66.74 cnf(e_4_is_not_e_2,axiom, % 66.66/66.74 ~ equalish(e_4,e_2) ). % 66.66/66.74 % 66.66/66.74 cnf(e_4_is_not_e_3,axiom, % 66.66/66.74 ~ equalish(e_4,e_3) ). % 66.66/66.74 % 66.66/66.74 cnf(product_total_function1,axiom, % 66.66/66.74 ( ~ group_element(X) % 66.66/66.74 | ~ group_element(Y) % 66.66/66.74 | product(X,Y,e_1) % 66.66/66.74 | product(X,Y,e_2) % 66.66/66.74 | product(X,Y,e_3) % 66.66/66.74 | product(X,Y,e_4) ) ). % 66.66/66.74 % 66.66/66.74 cnf(product_total_function2,axiom, % 66.66/66.74 ( ~ product(X,Y,W) % 66.66/66.74 | ~ product(X,Y,Z) % 66.66/66.74 | equalish(W,Z) ) ). % 66.66/66.74 % 66.66/66.74 cnf(product_right_cancellation,axiom, % 66.66/66.74 ( ~ product(X,W,Y) % 66.66/66.74 | ~ product(X,Z,Y) % 66.66/66.74 | equalish(W,Z) ) ). % 66.66/66.74 % 66.66/66.74 cnf(product_left_cancellation,axiom, % 66.66/66.74 ( ~ product(W,Y,X) % 66.66/66.74 | ~ product(Z,Y,X) % 66.66/66.74 | equalish(W,Z) ) ). % 66.66/66.74 % 66.66/66.74 cnf(product_idempotence,axiom, % 66.66/66.74 product(X,X,X) ). % 66.66/66.74 % 66.66/66.74 cnf(qg2_1,negated_conjecture, % 66.66/66.74 ( ~ product(X1,Y1,Z1) % 66.66/66.74 | ~ product(X2,Y2,Z1) % 66.66/66.74 | ~ product(Z2,X1,Y1) % 66.66/66.74 | ~ product(Z2,X2,Y2) % 66.66/66.74 | equalish(X1,X2) ) ). % 66.66/66.74 % 66.66/66.74 cnf(qg2_2,negated_conjecture, % 66.66/66.74 ( ~ product(X1,Y1,Z1) % 66.66/66.74 | ~ product(X2,Y2,Z1) % 66.66/66.74 | ~ product(Z2,X1,Y1) % 66.66/66.74 | ~ product(Z2,X2,Y2) % 66.66/66.74 | equalish(Y1,Y2) ) ). % 66.66/66.74 % 66.66/66.74 %-------------------------------------------------------------------------- % 66.66/66.74 %------------------------------------------- % 66.66/66.74 % Proof found % 66.66/66.74 % SZS status Theorem for theBenchmark % 66.66/66.74 % SZS output start Proof % 66.66/66.76 %ClaNum:44(EqnAxiom:0) % 66.66/66.76 %VarNum:112(SingletonVarNum:47) % 66.66/66.76 %MaxLitNum:6 % 66.66/66.76 %MaxfuncDepth:0 % 66.66/66.76 %SharedTerms:36 % 66.66/66.76 %goalClause: 43 44 % 66.66/66.76 [1]P1(a1) % 66.66/66.76 [2]P1(a3) % 66.66/66.76 [3]P1(a4) % 66.66/66.76 [4]P1(a5) % 66.66/66.76 [5]P5(a2,a1) % 66.66/66.76 [6]P5(a1,a3) % 66.66/66.76 [7]P5(a3,a4) % 66.66/66.76 [8]P5(a4,a5) % 66.66/66.76 [9]P2(a1,a2) % 66.66/66.76 [10]P2(a3,a2) % 66.66/66.76 [11]P2(a3,a1) % 66.66/66.76 [12]P2(a4,a2) % 66.66/66.76 [13]P2(a4,a1) % 66.66/66.76 [14]P2(a4,a3) % 66.66/66.76 [15]P2(a5,a2) % 66.66/66.76 [16]P2(a5,a1) % 66.66/66.76 [17]P2(a5,a3) % 66.66/66.76 [18]P2(a5,a4) % 66.66/66.76 [19]P3(a5,a2) % 66.66/66.76 [21]~P4(a1,a3) % 66.66/66.76 [22]~P4(a1,a4) % 66.66/66.76 [23]~P4(a1,a5) % 66.66/66.76 [24]~P4(a3,a1) % 66.66/66.76 [25]~P4(a3,a4) % 66.66/66.76 [26]~P4(a3,a5) % 66.66/66.76 [27]~P4(a4,a1) % 66.66/66.76 [28]~P4(a4,a3) % 66.66/66.76 [29]~P4(a4,a5) % 66.66/66.76 [30]~P4(a5,a1) % 66.66/66.76 [31]~P4(a5,a3) % 66.66/66.76 [32]~P4(a5,a4) % 66.66/66.76 [20]P6(x201,x201,x201) % 66.66/66.76 [36]~P2(x361,x362)+~P6(x362,a1,x361)+~P3(x362,a2) % 66.66/66.76 [34]~P3(x343,x341)+P4(x341,x342)+~P3(x343,x342) % 66.66/66.76 [39]~P6(x393,x394,x391)+P4(x391,x392)+~P6(x393,x394,x392) % 66.66/66.76 [40]~P6(x403,x401,x404)+P4(x401,x402)+~P6(x403,x402,x404) % 66.66/66.76 [41]~P6(x411,x413,x414)+P4(x411,x412)+~P6(x412,x413,x414) % 66.66/66.76 [33]~P1(x331)+P3(x331,a1)+P3(x331,a3)+P3(x331,a4)+P3(x331,a2) % 66.66/66.76 [38]P4(x381,x382)+~P5(x383,x382)+~P3(x383,x384)+~P6(x383,a1,x381)+~P2(x384,a2) % 66.66/66.76 [43]~P6(x435,x431,x436)+P4(x431,x432)+~P6(x433,x434,x432)+~P6(x433,x435,x431)+~P6(x434,x432,x436) % 66.66/66.76 [44]~P6(x441,x445,x446)+P4(x441,x442)+~P6(x443,x442,x444)+~P6(x443,x441,x445)+~P6(x442,x444,x446) % 66.66/66.76 [42]~P1(x422)+~P1(x421)+P6(x421,x422,a3)+P6(x421,x422,a4)+P6(x421,x422,a5)+P6(x421,x422,a1) % 66.66/66.76 [35]~P3(x355,x353)+~P3(x354,x351)+P4(x351,x352)+~P5(x353,x352)+~P5(x354,x355)+~P2(x351,a2) % 66.66/66.76 [37]~P3(x372,x375)+~P3(x373,x374)+~P5(x371,x372)+~P2(x371,x373)+~P2(x374,x375)+~P3(x371,a2) % 66.66/66.76 %EqnAxiom % 66.66/66.76 % 66.66/66.76 %------------------------------------------- % 67.21/67.22 cnf(49,plain, % 67.21/67.22 (~P3(a1,a1)), % 67.21/67.22 inference(scs_inference,[],[20,21,9,6,19,34,39,38])). % 67.21/67.22 cnf(76,plain, % 67.21/67.22 (P3(a1,a4)+P3(a1,a2)), % 67.21/67.22 inference(scs_inference,[],[1,20,21,49,10,6,19,34,40,38,36,33])). % 67.21/67.22 cnf(88,plain, % 67.21/67.22 (P3(a1,a2)), % 67.21/67.22 inference(scs_inference,[],[20,21,12,6,41,38,76])). % 67.21/67.22 cnf(1645,plain, % 67.21/67.22 (P6(a3,a4,a4)+P6(a3,a4,a5)+P6(a3,a4,a1)), % 67.21/67.22 inference(scs_inference,[],[20,25,3,2,40,42])). % 67.21/67.22 cnf(4829,plain, % 67.21/67.22 (~P6(a3,a1,a5)+P6(a3,a4,a4)+P6(a3,a4,a1)), % 67.21/67.22 inference(scs_inference,[],[27,40,1645])). % 67.21/67.22 cnf(460931,plain, % 67.21/67.22 (P6(x4609311,x4609311,x4609311)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(460935,plain, % 67.21/67.22 (~P6(a3,a1,a3)), % 67.21/67.22 inference(scs_inference,[],[24,20,460931,88,36,34,40])). % 67.21/67.22 cnf(460936,plain, % 67.21/67.22 (P6(x4609361,x4609361,x4609361)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(460938,plain, % 67.21/67.22 (~P6(a1,a3,a3)), % 67.21/67.22 inference(scs_inference,[],[24,20,460931,460936,88,36,34,40,41])). % 67.21/67.22 cnf(460939,plain, % 67.21/67.22 (P6(x4609391,x4609391,x4609391)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(460942,plain, % 67.21/67.22 (P6(x4609421,x4609421,x4609421)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(460946,plain, % 67.21/67.22 (~P6(a1,x4609461,a3)+~P6(a3,a1,x4609461)), % 67.21/67.22 inference(scs_inference,[],[24,20,460931,460936,460939,460942,88,36,34,40,41,39,43,44])). % 67.21/67.22 cnf(460947,plain, % 67.21/67.22 (P6(x4609471,x4609471,x4609471)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(460952,plain, % 67.21/67.22 (~P3(a4,a3)), % 67.21/67.22 inference(scs_inference,[],[24,10,5,21,6,20,460931,460936,460939,460942,460947,88,8,19,36,34,40,41,39,43,44,38,35])). % 67.21/67.22 cnf(460955,plain, % 67.21/67.22 (~P6(a3,a5,a3)), % 67.21/67.22 inference(scs_inference,[],[26,20,40])). % 67.21/67.22 cnf(460977,plain, % 67.21/67.22 (~P6(a5,a4,a4)), % 67.21/67.22 inference(scs_inference,[],[29,20,41])). % 67.21/67.22 cnf(460978,plain, % 67.21/67.22 (P6(x4609781,x4609781,x4609781)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(460981,plain, % 67.21/67.22 (P6(x4609811,x4609811,x4609811)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(460984,plain, % 67.21/67.22 (P6(x4609841,x4609841,x4609841)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(460986,plain, % 67.21/67.22 (~P6(a4,a5,a4)), % 67.21/67.22 inference(scs_inference,[],[29,20,460978,460981,460984,88,41,39,36,40])). % 67.21/67.22 cnf(460987,plain, % 67.21/67.22 (P6(x4609871,x4609871,x4609871)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(460993,plain, % 67.21/67.22 (~P6(a1,x4609931,a3)+~P6(x4609931,a3,a1)), % 67.21/67.22 inference(scs_inference,[],[24,29,5,30,20,460978,460981,460984,460987,15,88,41,39,36,40,34,35,43])). % 67.21/67.22 cnf(461000,plain, % 67.21/67.22 (~P6(a1,a4,a4)), % 67.21/67.22 inference(scs_inference,[],[27,20,41])). % 67.21/67.22 cnf(461001,plain, % 67.21/67.22 (P6(x4610011,x4610011,x4610011)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(461004,plain, % 67.21/67.22 (P6(x4610041,x4610041,x4610041)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(461008,plain, % 67.21/67.22 (~P6(a4,a1,a4)), % 67.21/67.22 inference(scs_inference,[],[13,27,20,461001,461004,88,41,39,36,40])). % 67.21/67.22 cnf(461019,plain, % 67.21/67.22 (P6(x4610191,x4610191,x4610191)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(461022,plain, % 67.21/67.22 (P6(x4610221,x4610221,x4610221)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(461025,plain, % 67.21/67.22 (P6(x4610251,x4610251,x4610251)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(461029,plain, % 67.21/67.22 (~P6(a4,a3,a4)), % 67.21/67.22 inference(scs_inference,[],[28,20,461019,461022,461025,88,41,39,36,34,40])). % 67.21/67.22 cnf(461030,plain, % 67.21/67.22 (P6(x4610301,x4610301,x4610301)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(461037,plain, % 67.21/67.22 (~P6(a3,a1,a5)+P6(a3,a4,a1)), % 67.21/67.22 inference(scs_inference,[],[28,21,6,20,461019,461022,461025,461030,88,41,39,36,34,40,43,38,4829])). % 67.21/67.22 cnf(461043,plain, % 67.21/67.22 (P6(x4610431,x4610431,x4610431)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(461045,plain, % 67.21/67.22 (~P6(a4,a5,a5)), % 67.21/67.22 inference(scs_inference,[],[32,20,461043,39,41])). % 67.21/67.22 cnf(461046,plain, % 67.21/67.22 (P6(x4610461,x4610461,x4610461)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(461050,plain, % 67.21/67.22 (~P6(a5,a4,a5)), % 67.21/67.22 inference(scs_inference,[],[32,16,20,461043,461046,88,39,41,36,40])). % 67.21/67.22 cnf(461061,plain, % 67.21/67.22 (~P6(a4,a3,a3)), % 67.21/67.22 inference(scs_inference,[],[25,20,41])). % 67.21/67.22 cnf(461062,plain, % 67.21/67.22 (P6(x4610621,x4610621,x4610621)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(461065,plain, % 67.21/67.22 (P6(x4610651,x4610651,x4610651)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(461068,plain, % 67.21/67.22 (P6(x4610681,x4610681,x4610681)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(461071,plain, % 67.21/67.22 (P6(x4610711,x4610711,x4610711)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(461075,plain, % 67.21/67.22 (~P6(a5,x4610751,a3)+~P6(x4610751,a3,a5)), % 67.21/67.22 inference(scs_inference,[],[26,25,20,461062,461065,461068,461071,88,41,39,36,40,34,43])). % 67.21/67.22 cnf(461078,plain, % 67.21/67.22 (~P6(a5,a4,a3)+P6(a4,a3,a1)), % 67.21/67.22 inference(scs_inference,[],[2,461029,3,26,25,20,461062,461065,461068,461071,88,41,39,36,40,34,43,42])). % 67.21/67.22 cnf(461083,plain, % 67.21/67.22 (P6(x4610831,x4610831,x4610831)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(461085,plain, % 67.21/67.22 (~P6(a4,a1,a1)), % 67.21/67.22 inference(scs_inference,[],[22,30,20,461083,39,41])). % 67.21/67.22 cnf(461086,plain, % 67.21/67.22 (P6(x4610861,x4610861,x4610861)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(461088,plain, % 67.21/67.22 (~P6(a1,a4,a1)), % 67.21/67.22 inference(scs_inference,[],[22,30,20,461083,461086,39,41,40])). % 67.21/67.22 cnf(461095,plain, % 67.21/67.22 (~P6(a5,a1,a1)), % 67.21/67.22 inference(scs_inference,[],[23,20,41])). % 67.21/67.22 cnf(461096,plain, % 67.21/67.22 (P6(x4610961,x4610961,x4610961)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(461099,plain, % 67.21/67.22 (P6(x4610991,x4610991,x4610991)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(461102,plain, % 67.21/67.22 (P6(x4611021,x4611021,x4611021)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(461106,plain, % 67.21/67.22 (~P6(a1,a5,a1)), % 67.21/67.22 inference(scs_inference,[],[23,20,461096,461099,461102,88,31,41,39,36,34,40])). % 67.21/67.22 cnf(461116,plain, % 67.21/67.22 (~P6(a3,a1,a1)), % 67.21/67.22 inference(scs_inference,[],[21,20,41])). % 67.21/67.22 cnf(461117,plain, % 67.21/67.22 (P6(x4611171,x4611171,x4611171)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(461119,plain, % 67.21/67.22 (~P6(a1,a3,a1)), % 67.21/67.22 inference(scs_inference,[],[21,20,461117,41,40])). % 67.21/67.22 cnf(461131,plain, % 67.21/67.22 (~P6(a1,a5,a5)), % 67.21/67.22 inference(scs_inference,[],[30,20,41])). % 67.21/67.22 cnf(461132,plain, % 67.21/67.22 (P6(x4611321,x4611321,x4611321)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(461135,plain, % 67.21/67.22 (P6(x4611351,x4611351,x4611351)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(461139,plain, % 67.21/67.22 (~P6(a5,a1,a5)), % 67.21/67.22 inference(scs_inference,[],[30,20,461132,461135,88,41,36,34,40])). % 67.21/67.22 cnf(461140,plain, % 67.21/67.22 (P6(x4611401,x4611401,x4611401)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(461145,plain, % 67.21/67.22 (P6(x4611451,x4611451,x4611451)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(461147,plain, % 67.21/67.22 (~P6(a1,x4611471,a4)+~P6(a4,a1,x4611471)), % 67.21/67.22 inference(scs_inference,[],[27,21,30,6,20,461132,461135,461140,461145,88,41,36,34,40,43,38,44])). % 67.21/67.22 cnf(461151,plain, % 67.21/67.22 (P6(a5,a4,a1)+P6(a5,a4,a3)), % 67.21/67.22 inference(scs_inference,[],[460977,461050,3,27,21,30,6,20,461132,461135,461140,461145,88,4,41,36,34,40,43,38,44,42])). % 67.21/67.22 cnf(461153,plain, % 67.21/67.22 (~P6(a3,a5,a5)), % 67.21/67.22 inference(scs_inference,[],[20,31,41])). % 67.21/67.22 cnf(461177,plain, % 67.21/67.22 (~P6(a4,a1,a5)+~P3(a4,a2)), % 67.21/67.22 inference(scs_inference,[],[18,36])). % 67.21/67.22 cnf(461205,plain, % 67.21/67.22 (P6(a1,a4,a5)+P6(a1,a4,a3)), % 67.21/67.22 inference(scs_inference,[],[3,461000,461088,12,21,6,20,88,1,34,43,38,36,42])). % 67.21/67.22 cnf(461224,plain, % 67.21/67.22 (P6(x4612241,x4612241,x4612241)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(461226,plain, % 67.21/67.22 (~P6(a1,a4,x4612261)+~P6(a4,x4612261,a1)), % 67.21/67.22 inference(scs_inference,[],[27,9,21,6,20,461224,88,34,43,36,38,44])). % 67.21/67.22 cnf(461232,plain, % 67.21/67.22 (P6(x4612321,x4612321,x4612321)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(461235,plain, % 67.21/67.22 (P6(x4612351,x4612351,x4612351)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(461241,plain, % 67.21/67.22 (~P6(a3,x4612411,a4)+~P6(x4612411,a4,a3)), % 67.21/67.22 inference(scs_inference,[],[26,28,21,6,20,461232,461235,88,36,38,44,34,43])). % 67.21/67.22 cnf(461270,plain, % 67.21/67.22 (P6(a4,a1,a5)+P6(a4,a1,a3)), % 67.21/67.22 inference(scs_inference,[],[3,461008,461085,21,6,20,88,1,34,43,38,42])). % 67.21/67.22 cnf(461272,plain, % 67.21/67.22 (P6(a4,a1,a3)+~P6(a1,a5,a4)), % 67.21/67.22 inference(scs_inference,[],[3,461008,461085,21,6,20,88,1,34,43,38,42,461147])). % 67.21/67.22 cnf(461274,plain, % 67.21/67.22 (~P3(a4,a2)+P6(a4,a1,a3)), % 67.21/67.22 inference(scs_inference,[],[3,461008,461085,21,6,20,88,1,34,43,38,42,461147,461177])). % 67.21/67.22 cnf(461290,plain, % 67.21/67.22 (P6(x4612901,x4612901,x4612901)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(461297,plain, % 67.21/67.22 (P6(a3,a5,a1)+P6(a3,a5,a4)), % 67.21/67.22 inference(scs_inference,[],[460955,461153,22,2,20,461290,88,4,34,36,43,38,42])). % 67.21/67.22 cnf(461310,plain, % 67.21/67.22 (P6(x4613101,x4613101,x4613101)), % 67.21/67.22 inference(rename_variables,[],[20])). % 67.21/67.22 cnf(461312,plain, % 67.21/67.23 (~P6(x4613121,a3,a4)+~P6(a4,x4613121,a3)), % 67.21/67.23 inference(scs_inference,[],[28,21,6,20,461310,88,34,38,43])). % 67.21/67.23 cnf(461317,plain, % 67.21/67.23 (~P6(a1,a3,a4)+P6(a4,a1,a5)), % 67.21/67.23 inference(scs_inference,[],[28,21,6,20,461310,88,34,38,43,461274,461270])). % 67.21/67.23 cnf(461318,plain, % 67.21/67.23 (~P6(a1,a3,a4)+~P6(a1,a5,a4)), % 67.21/67.23 inference(scs_inference,[],[28,21,6,20,461310,88,34,38,43,461274,461270,461272])). % 67.21/67.23 cnf(461335,plain, % 67.21/67.23 (P6(a5,a1,a4)+P6(a5,a1,a3)), % 67.21/67.23 inference(scs_inference,[],[4,461095,461139,9,88,1,34,37,42])). % 67.21/67.23 cnf(461342,plain, % 67.21/67.23 (P6(x4613421,x4613421,x4613421)), % 67.21/67.23 inference(rename_variables,[],[20])). % 67.21/67.23 cnf(461344,plain, % 67.21/67.23 (~P6(a3,a4,x4613441)+~P6(a4,x4613441,a3)), % 67.21/67.23 inference(scs_inference,[],[26,28,20,461342,88,34,43,36,44])). % 67.21/67.23 cnf(461363,plain, % 67.21/67.23 (P6(x4613631,x4613631,x4613631)), % 67.21/67.23 inference(rename_variables,[],[20])). % 67.21/67.23 cnf(461372,plain, % 67.21/67.23 (P6(a3,a1,a4)+P6(a3,a1,a5)), % 67.21/67.23 inference(scs_inference,[],[461116,460935,29,21,2,6,20,461363,88,1,36,43,38,34,42])). % 67.21/67.23 cnf(461393,plain, % 67.21/67.23 (P6(x4613931,x4613931,x4613931)), % 67.21/67.23 inference(rename_variables,[],[20])). % 67.21/67.23 cnf(461397,plain, % 67.21/67.23 (P6(a4,a5,a1)+P6(a4,a5,a3)), % 67.21/67.23 inference(scs_inference,[],[4,460986,461045,3,21,6,20,461393,19,88,34,38,44,42])). % 67.21/67.23 cnf(461405,plain, % 67.21/67.23 (P6(x4614051,x4614051,x4614051)), % 67.21/67.23 inference(rename_variables,[],[20])). % 67.21/67.23 cnf(461409,plain, % 67.21/67.23 (~P6(a5,a4,x4614091)+~P6(a4,x4614091,a5)), % 67.21/67.23 inference(scs_inference,[],[29,21,6,20,461405,19,88,38,34,44])). % 67.21/67.23 cnf(461502,plain, % 67.21/67.23 (P6(a1,a3,a5)+P6(a1,a3,a4)), % 67.21/67.23 inference(scs_inference,[],[460938,461119,29,2,21,6,20,88,1,38,34,42])). % 67.21/67.23 cnf(461523,plain, % 67.21/67.23 (~P6(a4,a3,x4615231)+~P6(a3,x4615231,a4)), % 67.21/67.23 inference(scs_inference,[],[25,20,19,34,43,44])). % 67.21/67.23 cnf(461525,plain, % 67.21/67.23 (P6(x4615251,x4615251,x4615251)), % 67.21/67.23 inference(rename_variables,[],[20])). % 67.21/67.23 cnf(461530,plain, % 67.21/67.23 (~P6(a4,a3,a1)+P6(a3,a1,a5)), % 67.21/67.23 inference(scs_inference,[],[6,460935,461116,25,2,21,20,461525,19,88,1,34,43,44,38,42])). % 67.21/67.23 cnf(461546,plain, % 67.21/67.23 (P6(a4,a3,a5)+P6(a4,a3,a1)), % 67.21/67.23 inference(scs_inference,[],[6,461061,461029,3,29,2,21,20,88,44,38,34,42])). % 67.21/67.23 cnf(461556,plain, % 67.21/67.23 (P6(a1,a5,a4)+P6(a1,a5,a3)), % 67.21/67.23 inference(scs_inference,[],[461106,461131,23,20,19,4,88,1,34,44,38,42])). % 67.21/67.23 cnf(461568,plain, % 67.21/67.23 (P6(x4615681,x4615681,x4615681)), % 67.21/67.23 inference(rename_variables,[],[20])). % 67.21/67.23 cnf(461571,plain, % 67.21/67.23 (P6(x4615711,x4615711,x4615711)), % 67.21/67.23 inference(rename_variables,[],[20])). % 67.21/67.23 cnf(461573,plain, % 67.21/67.23 (~P6(a1,x4615731,a5)+~P6(x4615731,a5,a1)), % 67.21/67.23 inference(scs_inference,[],[6,30,21,20,461568,461571,19,88,34,38,36,43])). % 67.21/67.23 cnf(461577,plain, % 67.21/67.23 (~P6(a1,a3,a5)+P6(a3,a5,a4)), % 67.21/67.23 inference(scs_inference,[],[6,30,21,20,461568,461571,19,88,34,38,36,43,461297])). % 67.21/67.23 cnf(461595,plain, % 67.21/67.23 (P3(a4,a2)+P3(a4,a1)), % 67.21/67.23 inference(scs_inference,[],[460952,3,27,12,5,22,8,20,19,88,34,43,35,38,33])). % 67.21/67.23 cnf(461599,plain, % 67.21/67.23 (~P6(a5,x4615991,a3)+~P6(a3,a5,x4615991)), % 67.21/67.23 inference(scs_inference,[],[26,20,19,34,44])). % 67.21/67.23 cnf(461603,plain, % 67.21/67.23 (~P6(a5,a4,a3)+~P6(a1,a3,a5)), % 67.21/67.23 inference(scs_inference,[],[26,20,19,34,44,461577])). % 67.21/67.23 cnf(461652,plain, % 67.21/67.23 (P6(x4616521,x4616521,x4616521)), % 67.21/67.23 inference(rename_variables,[],[20])). % 67.21/67.23 cnf(461655,plain, % 67.21/67.23 (P6(x4616551,x4616551,x4616551)), % 67.21/67.23 inference(rename_variables,[],[20])). % 67.21/67.23 cnf(461663,plain, % 67.21/67.23 (~P6(a5,a1,a4)+~P6(a4,a3,a1)), % 67.21/67.23 inference(scs_inference,[],[461000,461088,3,23,21,6,20,461652,461655,19,1,88,34,38,36,44,42,461226])). % 67.21/67.23 cnf(461665,plain, % 67.21/67.23 (~P6(a5,a1,a4)+~P6(a3,a1,a4)), % 67.21/67.23 inference(scs_inference,[],[461000,461088,3,23,21,6,20,461652,461655,19,1,88,34,38,36,44,42,461226,461241])). % 67.21/67.23 cnf(461716,plain, % 67.21/67.23 (~P6(a1,a5,x4617161)+~P6(a5,x4617161,a1)), % 67.21/67.23 inference(scs_inference,[],[30,20,19,34,44])). % 67.21/67.23 cnf(468325,plain, % 67.21/67.23 (P6(a4,a5,a1)+~P6(a5,a3,a4)), % 67.21/67.23 inference(scs_inference,[],[461312,461397])). % 67.21/67.23 cnf(468438,plain, % 67.21/67.23 (P6(a1,a3,a5)+~P6(a1,a5,a4)), % 67.21/67.23 inference(scs_inference,[],[461318,461502])). % 67.21/67.23 cnf(468661,plain, % 67.21/67.23 (P6(a4,a1,a3)+~P6(a5,a4,a1)), % 67.21/67.23 inference(scs_inference,[],[461409,461270])). % 67.21/67.23 cnf(469225,plain, % 67.21/67.23 (P6(a3,a5,a1)+~P6(a4,a3,a5)), % 67.21/67.23 inference(scs_inference,[],[461523,461297])). % 67.21/67.23 cnf(469571,plain, % 67.21/67.23 (~P6(a5,a3,a4)+~P6(a1,a4,a5)), % 67.21/67.23 inference(scs_inference,[],[461573,468325])). % 67.21/67.23 cnf(469683,plain, % 67.21/67.23 (~P6(a5,a4,a3)+~P6(a1,a5,a4)), % 67.21/67.23 inference(scs_inference,[],[461603,468438])). % 67.21/67.23 cnf(470033,plain, % 67.21/67.23 (P6(a5,a1,a3)+~P6(a4,a3,a1)), % 67.21/67.23 inference(scs_inference,[],[461663,461335])). % 67.21/67.23 cnf(470144,plain, % 67.21/67.23 (P6(a3,a1,a5)+~P6(a5,a1,a4)), % 67.21/67.23 inference(scs_inference,[],[461665,461372])). % 67.21/67.23 cnf(470548,plain, % 67.21/67.23 (P6(x4705481,x4705481,x4705481)), % 67.21/67.23 inference(rename_variables,[],[20])). % 67.21/67.23 cnf(470553,plain, % 67.21/67.23 (~P3(a5,a1)+~P3(a4,a1)), % 67.21/67.23 inference(scs_inference,[],[8,19,21,9,6,20,470548,88,34,38,36,35])). % 67.21/67.23 cnf(470608,plain, % 67.21/67.23 (P3(a4,a2)+~P3(a5,a1)), % 67.21/67.23 inference(scs_inference,[],[470553,461595])). % 67.21/67.23 cnf(470724,plain, % 67.21/67.23 (~P6(a4,a1,a5)+~P3(a5,a1)), % 67.21/67.23 inference(scs_inference,[],[470608,461177])). % 67.21/67.23 cnf(470841,plain, % 67.21/67.23 (~P6(a1,a3,a4)+~P3(a5,a1)), % 67.21/67.23 inference(scs_inference,[],[470724,461317])). % 67.21/67.23 cnf(470955,plain, % 67.21/67.23 (P6(a1,a3,a5)+~P3(a5,a1)), % 67.21/67.23 inference(scs_inference,[],[470841,461502])). % 67.21/67.23 cnf(471066,plain, % 67.21/67.23 (~P3(a5,a1)+~P6(a5,a1,a3)), % 67.21/67.23 inference(scs_inference,[],[470955,461075])). % 67.21/67.23 cnf(471186,plain, % 67.21/67.23 (~P6(a4,a3,a1)+~P3(a5,a1)), % 67.21/67.23 inference(scs_inference,[],[471066,470033])). % 67.21/67.23 cnf(471299,plain, % 67.21/67.23 (~P3(a5,a1)+~P6(a5,a4,a3)), % 67.21/67.23 inference(scs_inference,[],[471186,461078])). % 67.21/67.23 cnf(471415,plain, % 67.21/67.23 (P6(a5,a4,a1)+~P3(a5,a1)), % 67.21/67.23 inference(scs_inference,[],[471299,461151])). % 67.21/67.23 cnf(471527,plain, % 67.21/67.23 (P6(a4,a1,a3)+~P3(a5,a1)), % 67.21/67.23 inference(scs_inference,[],[471415,468661])). % 67.21/67.23 cnf(471642,plain, % 67.21/67.23 (~P3(a5,a1)+~P6(a3,a4,a1)), % 67.21/67.23 inference(scs_inference,[],[471527,461344])). % 67.21/67.23 cnf(471760,plain, % 67.21/67.23 (~P6(a3,a1,a5)+~P3(a5,a1)), % 67.21/67.23 inference(scs_inference,[],[471642,461037])). % 67.21/67.23 cnf(471874,plain, % 67.21/67.23 (~P6(a5,a1,a4)+~P3(a5,a1)), % 67.21/67.23 inference(scs_inference,[],[471760,470144])). % 67.21/67.23 cnf(471986,plain, % 67.21/67.23 (P6(a5,a1,a3)+~P3(a5,a1)), % 67.21/67.23 inference(scs_inference,[],[471874,461335])). % 67.21/67.23 cnf(472106,plain, % 67.21/67.23 (~P3(a5,a1)+~P6(a3,a5,a1)), % 67.21/67.23 inference(scs_inference,[],[471986,461599])). % 67.21/67.23 cnf(472221,plain, % 67.21/67.23 (~P3(a5,a1)+~P6(a4,a3,a5)), % 67.21/67.23 inference(scs_inference,[],[472106,469225])). % 67.21/67.23 cnf(473771,plain, % 67.21/67.23 (P6(a5,a4,a1)+~P6(a1,a5,a4)), % 67.21/67.23 inference(scs_inference,[],[469683,461151])). % 67.21/67.23 cnf(475119,plain, % 67.21/67.23 (~P6(a1,a5,a4)), % 67.21/67.23 inference(scs_inference,[],[473771,461716])). % 67.21/67.23 cnf(475120,plain, % 67.21/67.23 (P6(a1,a5,a3)), % 67.21/67.23 inference(scs_inference,[],[475119,461556])). % 67.21/67.23 cnf(475143,plain, % 67.21/67.23 (P6(x4751431,x4751431,x4751431)), % 67.21/67.23 inference(rename_variables,[],[20])). % 67.21/67.23 cnf(475158,plain, % 67.21/67.23 ($false), % 67.21/67.23 inference(scs_inference,[],[475120,460986,461045,3,21,4,6,20,475143,32,29,88,22,460946,461530,470144,461546,41,34,40,43,38,42,460993,472221,461205,461335,469225,469571,461078,461226]), % 67.21/67.23 ['proof']). % 67.47/67.44 % SZS output end Proof % 67.47/67.44 % Total time :66.070000s %------------------------------------------------------------------------------