%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP124-6.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 : n026.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 59.27s 59.33s % Output : CNFRefutation 59.48s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GRP124-6.004 : TPTP v8.2.0. Released v1.2.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.32 % Computer : n026.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 300 % 0.12/0.32 % DateTime : Thu Jun 20 08:42:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.49/0.56 start to proof:theBenchmark % 59.27/59.31 %------------------------------------------- % 59.27/59.31 % File :CSE---1.7 % 59.27/59.31 % Problem :theBenchmark % 59.27/59.31 % Transform :cnf % 59.27/59.31 % Format :tptp:raw % 59.27/59.31 % Command :java -jar mcs_scs.jar %d %s % 59.27/59.31 % 59.27/59.31 % Result :Theorem 58.710000s % 59.27/59.31 % Output :CNFRefutation 58.710000s % 59.27/59.31 %------------------------------------------- % 59.27/59.32 %-------------------------------------------------------------------------- % 59.27/59.32 % File : GRP124-6.004 : TPTP v8.2.0. Released v1.2.0. % 59.27/59.32 % Domain : Group Theory (Quasigroups) % 59.27/59.32 % Problem : (3,1,2) conjugate orthogonality % 59.27/59.32 % Version : [Sla93] axioms. % 59.27/59.32 % Theorem formulation : Uses a second group. % 59.27/59.32 % English : If ab=xy and a*b = x*y then a=x and b=y, where c*a=b iff ab=c. % 59.27/59.32 % Generate the multiplication table for the specified quasi- % 59.27/59.32 % group with 4 elements. % 59.27/59.32 % 59.27/59.32 % Refs : [FSB93] Fujita et al. (1993), Automatic Generation of Some Res % 59.27/59.32 % : [Sla93] Slaney (1993), Email to G. Sutcliffe % 59.27/59.32 % : [SFS95] Slaney et al. (1995), Automated Reasoning and Exhausti % 59.27/59.32 % Source : [Sla93] % 59.27/59.32 % Names : QG2a [Sla93] % 59.27/59.32 % 59.27/59.32 % Status : Unsatisfiable % 59.27/59.32 % Rating : 0.00 v2.1.0 % 59.27/59.32 % Syntax : Number of clauses : 27 ( 18 unt; 2 nHn; 25 RR) % 59.27/59.32 % Number of literals : 51 ( 0 equ; 30 neg) % 59.27/59.32 % Maximal clause size : 6 ( 1 avg) % 59.27/59.32 % Maximal term depth : 1 ( 1 avg) % 59.27/59.32 % Number of predicates : 4 ( 4 usr; 0 prp; 1-3 aty) % 59.27/59.32 % Number of functors : 4 ( 4 usr; 4 con; 0-0 aty) % 59.27/59.32 % Number of variables : 34 ( 0 sgn) % 59.27/59.32 % SPC : CNF_UNS_EPR_NEQ_NHN % 59.27/59.32 % 59.27/59.32 % Comments : [SFS93]'s axiomatization has been modified for this. % 59.27/59.32 % : Substitution axioms are not needed, as any positive equality % 59.27/59.32 % literals should resolve on negative ones directly. % 59.27/59.32 % : tptp2X: -f tptp -s4 GRP124-6.g % 59.27/59.32 %-------------------------------------------------------------------------- % 59.27/59.32 cnf(element_1,axiom, % 59.27/59.32 group_element(e_1) ). % 59.27/59.32 % 59.27/59.32 cnf(element_2,axiom, % 59.27/59.32 group_element(e_2) ). % 59.27/59.32 % 59.27/59.32 cnf(element_3,axiom, % 59.27/59.32 group_element(e_3) ). % 59.27/59.32 % 59.27/59.32 cnf(element_4,axiom, % 59.27/59.32 group_element(e_4) ). % 59.27/59.32 % 59.27/59.32 cnf(e_1_is_not_e_2,axiom, % 59.27/59.32 ~ equalish(e_1,e_2) ). % 59.27/59.32 % 59.27/59.32 cnf(e_1_is_not_e_3,axiom, % 59.27/59.32 ~ equalish(e_1,e_3) ). % 59.27/59.32 % 59.27/59.32 cnf(e_1_is_not_e_4,axiom, % 59.27/59.32 ~ equalish(e_1,e_4) ). % 59.27/59.32 % 59.27/59.32 cnf(e_2_is_not_e_1,axiom, % 59.27/59.32 ~ equalish(e_2,e_1) ). % 59.27/59.32 % 59.27/59.32 cnf(e_2_is_not_e_3,axiom, % 59.27/59.32 ~ equalish(e_2,e_3) ). % 59.27/59.32 % 59.27/59.32 cnf(e_2_is_not_e_4,axiom, % 59.27/59.32 ~ equalish(e_2,e_4) ). % 59.27/59.32 % 59.27/59.32 cnf(e_3_is_not_e_1,axiom, % 59.27/59.32 ~ equalish(e_3,e_1) ). % 59.27/59.32 % 59.27/59.32 cnf(e_3_is_not_e_2,axiom, % 59.27/59.32 ~ equalish(e_3,e_2) ). % 59.27/59.32 % 59.27/59.32 cnf(e_3_is_not_e_4,axiom, % 59.27/59.32 ~ equalish(e_3,e_4) ). % 59.27/59.32 % 59.27/59.32 cnf(e_4_is_not_e_1,axiom, % 59.27/59.32 ~ equalish(e_4,e_1) ). % 59.27/59.32 % 59.27/59.32 cnf(e_4_is_not_e_2,axiom, % 59.27/59.32 ~ equalish(e_4,e_2) ). % 59.27/59.32 % 59.27/59.32 cnf(e_4_is_not_e_3,axiom, % 59.27/59.32 ~ equalish(e_4,e_3) ). % 59.27/59.32 % 59.27/59.32 cnf(product1_total_function1,axiom, % 59.27/59.32 ( ~ group_element(X) % 59.27/59.32 | ~ group_element(Y) % 59.27/59.32 | product1(X,Y,e_1) % 59.27/59.32 | product1(X,Y,e_2) % 59.27/59.32 | product1(X,Y,e_3) % 59.27/59.32 | product1(X,Y,e_4) ) ). % 59.27/59.32 % 59.27/59.32 cnf(product1_total_function2,axiom, % 59.27/59.32 ( ~ product1(X,Y,W) % 59.27/59.32 | ~ product1(X,Y,Z) % 59.27/59.32 | equalish(W,Z) ) ). % 59.27/59.32 % 59.27/59.32 cnf(product1_right_cancellation,axiom, % 59.27/59.32 ( ~ product1(X,W,Y) % 59.27/59.32 | ~ product1(X,Z,Y) % 59.27/59.32 | equalish(W,Z) ) ). % 59.27/59.32 % 59.27/59.32 cnf(product1_left_cancellation,axiom, % 59.27/59.32 ( ~ product1(W,Y,X) % 59.27/59.32 | ~ product1(Z,Y,X) % 59.27/59.32 | equalish(W,Z) ) ). % 59.27/59.32 % 59.27/59.32 cnf(product1_idempotence,axiom, % 59.27/59.32 product1(X,X,X) ). % 59.27/59.32 % 59.27/59.32 cnf(product2_total_function1,axiom, % 59.27/59.32 ( ~ group_element(X) % 59.27/59.32 | ~ group_element(Y) % 59.27/59.32 | product2(X,Y,e_1) % 59.27/59.32 | product2(X,Y,e_2) % 59.27/59.32 | product2(X,Y,e_3) % 59.27/59.32 | product2(X,Y,e_4) ) ). % 59.27/59.32 % 59.27/59.32 cnf(product2_total_function2,axiom, % 59.27/59.32 ( ~ product2(X,Y,W) % 59.27/59.32 | ~ product2(X,Y,Z) % 59.27/59.33 | equalish(W,Z) ) ). % 59.27/59.33 % 59.27/59.33 cnf(product2_right_cancellation,axiom, % 59.27/59.33 ( ~ product2(X,W,Y) % 59.27/59.33 | ~ product2(X,Z,Y) % 59.27/59.33 | equalish(W,Z) ) ). % 59.27/59.33 % 59.27/59.33 cnf(product2_left_cancellation,axiom, % 59.27/59.33 ( ~ product2(W,Y,X) % 59.27/59.33 | ~ product2(Z,Y,X) % 59.27/59.33 | equalish(W,Z) ) ). % 59.27/59.33 % 59.27/59.33 cnf(product2_idempotence,axiom, % 59.27/59.33 product2(X,X,X) ). % 59.27/59.33 % 59.27/59.33 cnf(qg2a,negated_conjecture, % 59.27/59.33 ( ~ product1(X,Y,Z1) % 59.27/59.33 | ~ product1(Z1,X,Z2) % 59.27/59.33 | product2(Z2,Y,X) ) ). % 59.27/59.33 % 59.27/59.33 %-------------------------------------------------------------------------- % 59.27/59.33 %------------------------------------------- % 59.27/59.33 % Proof found % 59.27/59.33 % SZS status Theorem for theBenchmark % 59.27/59.33 % SZS output start Proof % 59.27/59.33 %ClaNum:27(EqnAxiom:0) % 59.27/59.33 %VarNum:83(SingletonVarNum:34) % 59.27/59.33 %MaxLitNum:6 % 59.27/59.33 %MaxfuncDepth:0 % 59.27/59.33 %SharedTerms:20 % 59.27/59.33 %goalClause: 25 % 59.27/59.33 [1]P1(a1) % 59.27/59.33 [2]P1(a2) % 59.27/59.33 [3]P1(a3) % 59.27/59.33 [4]P1(a4) % 59.27/59.33 [7]~P2(a1,a2) % 59.27/59.33 [8]~P2(a1,a3) % 59.27/59.33 [9]~P2(a1,a4) % 59.27/59.33 [10]~P2(a2,a1) % 59.27/59.33 [11]~P2(a2,a3) % 59.27/59.33 [12]~P2(a2,a4) % 59.27/59.33 [13]~P2(a3,a1) % 59.27/59.33 [14]~P2(a3,a2) % 59.27/59.33 [15]~P2(a3,a4) % 59.27/59.33 [16]~P2(a4,a1) % 59.27/59.33 [17]~P2(a4,a2) % 59.27/59.33 [18]~P2(a4,a3) % 59.27/59.33 [5]P3(x51,x51,x51) % 59.27/59.33 [6]P4(x61,x61,x61) % 59.27/59.33 [19]~P3(x193,x194,x191)+P2(x191,x192)+~P3(x193,x194,x192) % 59.27/59.33 [20]~P4(x203,x204,x201)+P2(x201,x202)+~P4(x203,x204,x202) % 59.27/59.33 [21]~P3(x213,x211,x214)+P2(x211,x212)+~P3(x213,x212,x214) % 59.27/59.33 [22]~P4(x223,x221,x224)+P2(x221,x222)+~P4(x223,x222,x224) % 59.27/59.33 [23]~P3(x231,x233,x234)+P2(x231,x232)+~P3(x232,x233,x234) % 59.27/59.33 [24]~P4(x241,x243,x244)+P2(x241,x242)+~P4(x242,x243,x244) % 59.27/59.33 [25]~P3(x253,x252,x254)+P4(x251,x252,x253)+~P3(x254,x253,x251) % 59.27/59.33 [26]~P1(x262)+~P1(x261)+P3(x261,x262,a2)+P3(x261,x262,a3)+P3(x261,x262,a4)+P3(x261,x262,a1) % 59.27/59.33 [27]~P1(x272)+~P1(x271)+P4(x271,x272,a2)+P4(x271,x272,a3)+P4(x271,x272,a4)+P4(x271,x272,a1) % 59.27/59.33 %EqnAxiom % 59.27/59.33 % 59.27/59.33 %------------------------------------------- % 59.43/59.42 cnf(121,plain, % 59.43/59.42 (~P3(x1211,a2,a1)+~P3(a2,a1,x1211)), % 59.43/59.42 inference(scs_inference,[],[6,7,20,25])). % 59.43/59.42 cnf(243,plain, % 59.43/59.42 (~P3(x2431,a4,a1)+~P3(a4,a1,x2431)), % 59.43/59.42 inference(scs_inference,[],[9,6,20,25])). % 59.43/59.42 cnf(304,plain, % 59.43/59.42 (~P3(x3041,a1,a2)+~P3(a1,a2,x3041)), % 59.43/59.42 inference(scs_inference,[],[10,6,20,25])). % 59.43/59.42 cnf(487,plain, % 59.43/59.42 (~P3(x4871,a3,a1)+~P3(a3,a1,x4871)), % 59.43/59.42 inference(scs_inference,[],[13,6,20,25])). % 59.43/59.42 cnf(548,plain, % 59.43/59.42 (~P3(x5481,a3,a2)+~P3(a3,a2,x5481)), % 59.43/59.42 inference(scs_inference,[],[14,6,20,25])). % 59.43/59.42 cnf(670,plain, % 59.43/59.42 (~P3(x6701,a1,a4)+~P3(a1,a4,x6701)), % 59.43/59.42 inference(scs_inference,[],[16,6,20,25])). % 59.43/59.42 cnf(792,plain, % 59.43/59.42 (~P3(x7921,a3,a4)+~P3(a3,a4,x7921)), % 59.43/59.42 inference(scs_inference,[],[18,6,20,25])). % 59.43/59.42 cnf(883,plain, % 59.43/59.42 (P3(a2,a1,a3)+P3(a2,a1,a4)+P3(a2,a1,a1)), % 59.43/59.42 inference(scs_inference,[],[5,10,1,2,21,26])). % 59.43/59.42 cnf(4757,plain, % 59.43/59.42 (~P3(a2,a3,a2)), % 59.43/59.42 inference(scs_inference,[],[6,11,5,22,25])). % 59.43/59.42 cnf(4760,plain, % 59.43/59.42 (P3(a2,a3,a4)+P3(a2,a3,a1)+P3(a2,a3,a3)), % 59.43/59.42 inference(scs_inference,[],[3,4757,2,6,24,26])). % 59.43/59.42 cnf(5032,plain, % 59.43/59.42 (~P3(a3,a2,a3)), % 59.43/59.42 inference(scs_inference,[],[14,6,5,22,25])). % 59.43/59.42 cnf(5078,plain, % 59.43/59.42 (~P3(a4,a3,a4)), % 59.43/59.42 inference(scs_inference,[],[15,6,5,22,25])). % 59.43/59.42 cnf(5216,plain, % 59.43/59.42 (~P3(a3,a4,a3)), % 59.43/59.42 inference(scs_inference,[],[18,6,5,22,25])). % 59.43/59.42 cnf(5307,plain, % 59.43/59.42 (P3(a3,a2,a4)+P3(a3,a2,a1)), % 59.43/59.42 inference(scs_inference,[],[5,11,5032,2,3,23,26])). % 59.43/59.42 cnf(5491,plain, % 59.43/59.42 (~P3(a2,a1,a3)+P3(a3,a2,a4)), % 59.43/59.42 inference(scs_inference,[],[5307,121])). % 59.43/59.42 cnf(5537,plain, % 59.43/59.42 (P3(a3,a2,a4)+P3(a2,a1,a4)+P3(a2,a1,a1)), % 59.43/59.42 inference(scs_inference,[],[5491,883])). % 59.43/59.42 cnf(190398,plain, % 59.43/59.42 (P3(x1903981,x1903981,x1903981)), % 59.43/59.42 inference(rename_variables,[],[5])). % 59.43/59.42 cnf(190401,plain, % 59.43/59.42 (P4(x1904011,x1904011,x1904011)), % 59.43/59.42 inference(rename_variables,[],[6])). % 59.43/59.42 cnf(190403,plain, % 59.43/59.42 (~P3(a2,a3,a3)), % 59.43/59.42 inference(scs_inference,[],[14,6,5,190398,19,22,23])). % 59.43/59.42 cnf(190404,plain, % 59.43/59.42 (P3(x1904041,x1904041,x1904041)), % 59.43/59.42 inference(rename_variables,[],[5])). % 59.43/59.42 cnf(190407,plain, % 59.43/59.42 (P4(x1904071,x1904071,x1904071)), % 59.43/59.42 inference(rename_variables,[],[6])). % 59.43/59.42 cnf(190409,plain, % 59.43/59.42 (~P4(a2,a3,a3)), % 59.43/59.42 inference(scs_inference,[],[14,6,190401,190407,5,190398,19,22,23,20,24])). % 59.43/59.42 cnf(190412,plain, % 59.43/59.42 (~P3(a1,a4,a1)), % 59.43/59.42 inference(scs_inference,[],[14,9,6,190401,190407,5,190398,190404,19,22,23,20,24,21])). % 59.43/59.42 cnf(190418,plain, % 59.43/59.42 (P3(a2,a3,a1)+P3(a2,a3,a4)), % 59.43/59.42 inference(scs_inference,[],[190403,4760])). % 59.43/59.42 cnf(190421,plain, % 59.43/59.42 (P4(x1904211,x1904211,x1904211)), % 59.43/59.42 inference(rename_variables,[],[6])). % 59.43/59.42 cnf(190424,plain, % 59.43/59.42 (P4(x1904241,x1904241,x1904241)), % 59.43/59.42 inference(rename_variables,[],[6])). % 59.43/59.42 cnf(190427,plain, % 59.43/59.42 (P3(x1904271,x1904271,x1904271)), % 59.43/59.42 inference(rename_variables,[],[5])). % 59.43/59.42 cnf(190430,plain, % 59.43/59.42 (P3(x1904301,x1904301,x1904301)), % 59.43/59.42 inference(rename_variables,[],[5])). % 59.43/59.42 cnf(190435,plain, % 59.43/59.42 (~P3(a4,a1,a4)), % 59.43/59.42 inference(scs_inference,[],[15,16,6,190421,190424,5,190427,190430,24,22,23,19,20,21])). % 59.43/59.42 cnf(190440,plain, % 59.43/59.42 (P3(a4,a3,a2)+~P3(a3,a1,a4)), % 59.43/59.42 inference(scs_inference,[],[5078,15,16,3,4,6,190421,190424,5,190427,190430,24,22,23,19,20,21,26,487])). % 59.43/59.42 cnf(190445,plain, % 59.43/59.42 (P4(x1904451,x1904451,x1904451)), % 59.43/59.42 inference(rename_variables,[],[6])). % 59.43/59.42 cnf(190448,plain, % 59.43/59.42 (P3(x1904481,x1904481,x1904481)), % 59.43/59.42 inference(rename_variables,[],[5])). % 59.43/59.42 cnf(190451,plain, % 59.43/59.42 (P3(x1904511,x1904511,x1904511)), % 59.43/59.42 inference(rename_variables,[],[5])). % 59.43/59.42 cnf(190454,plain, % 59.43/59.42 (P4(x1904541,x1904541,x1904541)), % 59.43/59.42 inference(rename_variables,[],[6])). % 59.43/59.42 cnf(190459,plain, % 59.43/59.42 (~P3(a1,a2,a1)), % 59.43/59.42 inference(scs_inference,[],[17,7,6,190445,190454,5,190448,190451,20,23,19,22,24,21])). % 59.43/59.42 cnf(190467,plain, % 59.43/59.42 (P3(x1904671,x1904671,x1904671)), % 59.43/59.42 inference(rename_variables,[],[5])). % 59.43/59.42 cnf(190469,plain, % 59.43/59.42 (~P3(a3,a4,a4)), % 59.43/59.42 inference(scs_inference,[],[18,5,190467,19,23])). % 59.43/59.42 cnf(190488,plain, % 59.43/59.42 (P4(x1904881,x1904881,x1904881)), % 59.43/59.42 inference(rename_variables,[],[6])). % 59.43/59.42 cnf(190490,plain, % 59.43/59.42 (~P4(a2,a3,a2)), % 59.43/59.42 inference(scs_inference,[],[11,6,190488,20,22])). % 59.43/59.42 cnf(190491,plain, % 59.43/59.42 (P4(x1904911,x1904911,x1904911)), % 59.43/59.42 inference(rename_variables,[],[6])). % 59.43/59.42 cnf(190497,plain, % 59.43/59.42 (P3(x1904971,x1904971,x1904971)), % 59.43/59.42 inference(rename_variables,[],[5])). % 59.43/59.42 cnf(190500,plain, % 59.43/59.42 (P3(x1905001,x1905001,x1905001)), % 59.43/59.42 inference(rename_variables,[],[5])). % 59.43/59.42 cnf(190502,plain, % 59.43/59.42 (~P3(a3,a1,a3)), % 59.43/59.42 inference(scs_inference,[],[11,13,6,190488,190491,5,190497,190500,20,22,24,23,19,21])). % 59.43/59.42 cnf(190509,plain, % 59.43/59.42 (P3(x1905091,x1905091,x1905091)), % 59.43/59.42 inference(rename_variables,[],[5])). % 59.43/59.42 cnf(190515,plain, % 59.43/59.42 (P4(x1905151,x1905151,x1905151)), % 59.43/59.42 inference(rename_variables,[],[6])). % 59.43/59.42 cnf(190518,plain, % 59.43/59.42 (P4(x1905181,x1905181,x1905181)), % 59.43/59.42 inference(rename_variables,[],[6])). % 59.43/59.42 cnf(190525,plain, % 59.43/59.42 (P3(a3,a1,a4)+P3(a3,a1,a2)), % 59.43/59.42 inference(scs_inference,[],[1,190502,190409,190490,8,3,2,6,190515,190518,5,190509,19,23,24,22,20,27,26])). % 59.43/59.42 cnf(190528,plain, % 59.43/59.42 (P3(x1905281,x1905281,x1905281)), % 59.43/59.42 inference(rename_variables,[],[5])). % 59.43/59.42 cnf(190533,plain, % 59.43/59.42 (P3(a4,a1,a3)+P3(a4,a1,a2)), % 59.43/59.42 inference(scs_inference,[],[1,190435,9,4,5,190528,23,19,26])). % 59.43/59.42 cnf(190539,plain, % 59.43/59.42 (P3(x1905391,x1905391,x1905391)), % 59.43/59.42 inference(rename_variables,[],[5])). % 59.43/59.42 cnf(190541,plain, % 59.43/59.42 (~P3(a1,a4,a4)), % 59.43/59.42 inference(scs_inference,[],[16,5,190539,19,23])). % 59.43/59.42 cnf(190552,plain, % 59.43/59.42 (P4(x1905521,x1905521,x1905521)), % 59.43/59.42 inference(rename_variables,[],[6])). % 59.43/59.42 cnf(190557,plain, % 59.43/59.42 (~P3(a2,a1,a1)), % 59.43/59.42 inference(scs_inference,[],[7,6,190552,5,24,22,23])). % 59.43/59.42 cnf(190558,plain, % 59.43/59.42 (P3(x1905581,x1905581,x1905581)), % 59.43/59.42 inference(rename_variables,[],[5])). % 59.43/59.42 cnf(190565,plain, % 59.43/59.42 (P3(a3,a4,a2)+~P3(a4,a1,a3)), % 59.43/59.42 inference(scs_inference,[],[5216,190469,7,4,3,6,190552,5,190558,24,22,23,19,26,243])). % 59.43/59.42 cnf(190573,plain, % 59.43/59.42 (P3(a2,a1,a4)+P3(a3,a2,a4)), % 59.43/59.42 inference(scs_inference,[],[190557,5537])). % 59.43/59.42 cnf(190574,plain, % 59.43/59.42 (~P3(a1,a2,a2)), % 59.43/59.42 inference(scs_inference,[],[10,5,23])). % 59.43/59.42 cnf(190596,plain, % 59.43/59.42 (P4(x1905961,x1905961,x1905961)), % 59.43/59.42 inference(rename_variables,[],[6])). % 59.43/59.42 cnf(190601,plain, % 59.43/59.42 (P3(a1,a4,a3)+P3(a1,a4,a2)), % 59.43/59.42 inference(scs_inference,[],[1,190412,190541,9,4,6,190596,22,24,26])). % 59.43/59.42 cnf(190625,plain, % 59.43/59.42 (P3(a1,a2,a4)+~P3(a3,a1,a2)), % 59.43/59.42 inference(scs_inference,[],[1,2,190459,190574,304,26])). % 59.43/59.42 cnf(190663,plain, % 59.43/59.42 (P3(a1,a4,a2)+~P3(a3,a1,a4)), % 59.43/59.42 inference(scs_inference,[],[670,190601])). % 59.43/59.42 cnf(190707,plain, % 59.43/59.42 (~P3(a3,a1,a2)+~P3(a4,a1,a2)), % 59.43/59.42 inference(scs_inference,[],[190625,304])). % 59.43/59.42 cnf(190713,plain, % 59.43/59.42 (~P3(a3,a1,a4)+~P3(a2,a1,a4)), % 59.43/59.42 inference(scs_inference,[],[190663,670])). % 59.43/59.42 cnf(190734,plain, % 59.43/59.42 (P3(a4,a1,a3)+~P3(a3,a1,a2)), % 59.43/59.42 inference(scs_inference,[],[190707,190533])). % 59.43/59.42 cnf(190737,plain, % 59.43/59.42 (P3(a3,a2,a4)+~P3(a3,a1,a4)), % 59.43/59.42 inference(scs_inference,[],[190713,190573])). % 59.43/59.42 cnf(190752,plain, % 59.43/59.42 (P3(a3,a4,a2)+~P3(a3,a1,a2)), % 59.43/59.42 inference(scs_inference,[],[190734,190565])). % 59.43/59.42 cnf(190754,plain, % 59.43/59.42 (~P3(a3,a1,a4)+~P3(a4,a3,a2)), % 59.43/59.42 inference(scs_inference,[],[190737,548])). % 59.43/59.42 cnf(190769,plain, % 59.43/59.42 (~P3(a3,a1,a2)+~P3(a2,a3,a4)), % 59.43/59.42 inference(scs_inference,[],[190752,792])). % 59.43/59.42 cnf(190783,plain, % 59.43/59.42 (P3(a2,a3,a1)+~P3(a3,a1,a2)), % 59.43/59.42 inference(scs_inference,[],[190769,190418])). % 59.43/59.42 cnf(190796,plain, % 59.43/59.42 (~P3(a3,a1,a2)), % 59.43/59.42 inference(scs_inference,[],[190783,487])). % 59.43/59.42 cnf(190797,plain, % 59.43/59.42 (P3(a3,a1,a4)), % 59.43/59.42 inference(scs_inference,[],[190796,190525])). % 59.43/59.42 cnf(190799,plain, % 59.43/59.42 (P3(a4,a3,a2)), % 59.43/59.42 inference(scs_inference,[],[190797,190440])). % 59.43/59.42 cnf(190808,plain, % 59.43/59.42 (~P3(a4,a3,a2)), % 59.43/59.42 inference(scs_inference,[],[190797,190754])). % 59.43/59.42 cnf(190814,plain, % 59.43/59.42 ($false), % 59.43/59.42 inference(scs_inference,[],[190799,190808]), % 59.43/59.42 ['proof']). % 59.48/59.50 % SZS output end Proof % 59.48/59.50 % Total time :58.710000s %------------------------------------------------------------------------------