%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP134-1.003 : 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 : n027.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:58 EDT 2024 % Result : Unsatisfiable 79.46s 79.61s % Output : CNFRefutation 79.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : GRP134-1.003 : TPTP v8.2.0. Released v1.2.0. % 0.12/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n027.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Thu Jun 20 07:18:24 EDT 2024 % 0.12/0.34 % CPUTime : % 0.54/0.59 start to proof:theBenchmark % 79.37/79.60 %------------------------------------------- % 79.37/79.60 % File :CSE---1.7 % 79.37/79.60 % Problem :theBenchmark % 79.37/79.60 % Transform :cnf % 79.37/79.60 % Format :tptp:raw % 79.37/79.60 % Command :java -jar mcs_scs.jar %d %s % 79.37/79.60 % 79.37/79.60 % Result :Theorem 78.830000s % 79.37/79.60 % Output :CNFRefutation 78.830000s % 79.37/79.60 %------------------------------------------- % 79.37/79.61 %-------------------------------------------------------------------------- % 79.37/79.61 % File : GRP134-1.003 : TPTP v8.2.0. Released v1.2.0. % 79.37/79.61 % Domain : Group Theory (Quasigroups) % 79.37/79.61 % Problem : (a.b).(b.a) = b, no idempotence % 79.37/79.61 % Version : [Sla93] axioms. % 79.37/79.61 % English : Generate the multiplication table for the specified quasi- % 79.37/79.61 % group with 3 elements. % 79.37/79.61 % 79.46/79.61 % Refs : [FSB93] Fujita et al. (1993), Automatic Generation of Some Res % 79.46/79.61 % : [Sla93] Slaney (1993), Email to G. Sutcliffe % 79.46/79.61 % : [SFS95] Slaney et al. (1995), Automated Reasoning and Exhausti % 79.46/79.61 % Source : [Sla93] % 79.46/79.61 % Names : QG4-ni [Sla93] % 79.46/79.61 % 79.46/79.61 % Status : Unsatisfiable % 79.46/79.61 % Rating : 0.00 v2.1.0 % 79.46/79.61 % Syntax : Number of clauses : 14 ( 9 unt; 1 nHn; 14 RR) % 79.46/79.61 % Number of literals : 26 ( 0 equ; 16 neg) % 79.46/79.61 % Maximal clause size : 5 ( 1 avg) % 79.46/79.61 % Maximal term depth : 1 ( 1 avg) % 79.46/79.61 % Number of predicates : 3 ( 3 usr; 0 prp; 1-3 aty) % 79.46/79.61 % Number of functors : 3 ( 3 usr; 3 con; 0-0 aty) % 79.46/79.61 % Number of variables : 18 ( 0 sgn) % 79.46/79.61 % SPC : CNF_UNS_EPR_NEQ_NHN % 79.46/79.61 % 79.46/79.61 % Comments : Slaney's [1993] axiomatization has been modified for this. % 79.46/79.61 % : Substitution axioms are not needed, as any positive equality % 79.46/79.61 % literals should resolve on negative ones directly. % 79.46/79.61 % : tptp2X: -f tptp -s3 GRP134-1.g % 79.46/79.61 %-------------------------------------------------------------------------- % 79.46/79.61 cnf(element_1,axiom, % 79.46/79.61 group_element(e_1) ). % 79.46/79.61 % 79.46/79.61 cnf(element_2,axiom, % 79.46/79.61 group_element(e_2) ). % 79.46/79.61 % 79.46/79.61 cnf(element_3,axiom, % 79.46/79.61 group_element(e_3) ). % 79.46/79.61 % 79.46/79.61 cnf(e_1_is_not_e_2,axiom, % 79.46/79.61 ~ equalish(e_1,e_2) ). % 79.46/79.61 % 79.46/79.61 cnf(e_1_is_not_e_3,axiom, % 79.46/79.61 ~ equalish(e_1,e_3) ). % 79.46/79.61 % 79.46/79.61 cnf(e_2_is_not_e_1,axiom, % 79.46/79.61 ~ equalish(e_2,e_1) ). % 79.46/79.61 % 79.46/79.61 cnf(e_2_is_not_e_3,axiom, % 79.46/79.61 ~ equalish(e_2,e_3) ). % 79.46/79.61 % 79.46/79.61 cnf(e_3_is_not_e_1,axiom, % 79.46/79.61 ~ equalish(e_3,e_1) ). % 79.46/79.61 % 79.46/79.61 cnf(e_3_is_not_e_2,axiom, % 79.46/79.61 ~ equalish(e_3,e_2) ). % 79.46/79.61 % 79.46/79.61 cnf(product_total_function1,axiom, % 79.46/79.61 ( ~ group_element(X) % 79.46/79.61 | ~ group_element(Y) % 79.46/79.61 | product(X,Y,e_1) % 79.46/79.61 | product(X,Y,e_2) % 79.46/79.61 | product(X,Y,e_3) ) ). % 79.46/79.61 % 79.46/79.61 cnf(product_total_function2,axiom, % 79.46/79.61 ( ~ product(X,Y,W) % 79.46/79.61 | ~ product(X,Y,Z) % 79.46/79.61 | equalish(W,Z) ) ). % 79.46/79.61 % 79.46/79.61 cnf(product_right_cancellation,axiom, % 79.46/79.61 ( ~ product(X,W,Y) % 79.46/79.61 | ~ product(X,Z,Y) % 79.46/79.61 | equalish(W,Z) ) ). % 79.46/79.61 % 79.46/79.61 cnf(product_left_cancellation,axiom, % 79.46/79.61 ( ~ product(W,Y,X) % 79.46/79.61 | ~ product(Z,Y,X) % 79.46/79.61 | equalish(W,Z) ) ). % 79.46/79.61 % 79.46/79.61 cnf(qg4,negated_conjecture, % 79.46/79.61 ( ~ product(X,Y,Z1) % 79.46/79.61 | ~ product(Y,X,Z2) % 79.46/79.61 | product(Z1,Z2,Y) ) ). % 79.46/79.61 % 79.46/79.61 %-------------------------------------------------------------------------- % 79.46/79.61 %------------------------------------------- % 79.46/79.61 % Proof found % 79.46/79.61 % SZS status Theorem for theBenchmark % 79.46/79.61 % SZS output start Proof % 79.46/79.61 %ClaNum:14(EqnAxiom:0) % 79.46/79.61 %VarNum:41(SingletonVarNum:18) % 79.46/79.61 %MaxLitNum:5 % 79.46/79.61 %MaxfuncDepth:0 % 79.46/79.61 %SharedTerms:12 % 79.46/79.61 %goalClause: 14 % 79.46/79.61 [1]P1(a1) % 79.46/79.61 [2]P1(a2) % 79.46/79.61 [3]P1(a3) % 79.46/79.61 [4]~P2(a1,a2) % 79.46/79.61 [5]~P2(a1,a3) % 79.46/79.61 [6]~P2(a2,a1) % 79.46/79.61 [7]~P2(a2,a3) % 79.46/79.61 [8]~P2(a3,a1) % 79.46/79.61 [9]~P2(a3,a2) % 79.46/79.61 [11]~P3(x113,x114,x111)+P2(x111,x112)+~P3(x113,x114,x112) % 79.46/79.61 [12]~P3(x123,x121,x124)+P2(x121,x122)+~P3(x123,x122,x124) % 79.46/79.61 [13]~P3(x131,x133,x134)+P2(x131,x132)+~P3(x132,x133,x134) % 79.46/79.61 [14]~P3(x144,x143,x141)+P3(x141,x142,x143)+~P3(x143,x144,x142) % 79.46/79.61 [10]~P1(x102)+~P1(x101)+P3(x101,x102,a2)+P3(x101,x102,a3)+P3(x101,x102,a1) % 79.46/79.61 %EqnAxiom % 79.46/79.61 % 79.46/79.61 %------------------------------------------- % 79.46/79.63 cnf(15,plain, % 79.46/79.63 (~P3(a2,x151,x152)+~P3(x153,x152,a1)+~P3(x151,a2,x153)), % 79.46/79.63 inference(scs_inference,[],[4,11,14])). % 79.46/79.63 cnf(16,plain, % 79.46/79.63 (~P3(x161,x162,a3)+~P3(x163,a1,x161)+~P3(x162,x161,x163)), % 79.46/79.63 inference(scs_inference,[],[5,12,14])). % 79.46/79.63 cnf(17,plain, % 79.46/79.63 (~P3(x171,x172,x173)+~P3(a1,x173,x171)+~P3(x172,x171,a2)), % 79.46/79.63 inference(scs_inference,[],[4,13,14])). % 79.46/79.63 cnf(18,plain, % 79.46/79.63 (~P3(x181,x182,a1)+~P3(a3,x183,x182)+~P3(x183,a3,x181)), % 79.46/79.63 inference(scs_inference,[],[8,11,14])). % 79.46/79.63 cnf(19,plain, % 79.46/79.63 (~P3(a1,x191,x192)+~P3(x193,x192,a2)+~P3(x191,a1,x193)), % 79.46/79.63 inference(scs_inference,[],[6,11,14])). % 79.46/79.63 cnf(20,plain, % 79.46/79.63 (~P3(x201,x202,a3)+~P3(a2,x203,x202)+~P3(x203,a2,x201)), % 79.46/79.63 inference(scs_inference,[],[7,11,14])). % 79.46/79.63 cnf(24,plain, % 79.46/79.63 (~P3(x241,x242,a3)+~P3(a1,x243,x242)+~P3(x243,a1,x241)), % 79.46/79.63 inference(scs_inference,[],[5,11,14])). % 79.46/79.63 cnf(27,plain, % 79.46/79.63 (~P3(a3,x271,x272)+~P3(x273,x272,a2)+~P3(x271,a3,x273)), % 79.46/79.63 inference(scs_inference,[],[7,11,14])). % 79.46/79.63 cnf(37,plain, % 79.46/79.63 (~P3(x371,a2,x372)+~P3(x372,x373,a3)+~P3(x373,x372,x371)), % 79.46/79.63 inference(scs_inference,[],[9,12,14])). % 79.46/79.63 cnf(39,plain, % 79.46/79.63 (~P3(x391,a3,x392)+~P3(x392,x393,a1)+~P3(x393,x392,x391)), % 79.46/79.63 inference(scs_inference,[],[5,12,14])). % 79.46/79.63 cnf(40,plain, % 79.46/79.63 (~P3(a2,a2,a3)+P3(a2,a3,a2)+P3(a2,a3,a1)), % 79.46/79.63 inference(scs_inference,[],[7,3,2,12,10])). % 79.46/79.63 cnf(42,plain, % 79.46/79.63 (~P3(a2,a3,a3)+P3(a2,a1,a2)+P3(a2,a1,a1)), % 79.46/79.63 inference(scs_inference,[],[8,1,2,12,10])). % 79.46/79.63 cnf(43,plain, % 79.46/79.63 (~P3(a2,a1,a2)+~P3(a2,a2,a3)+P3(a2,a3,a1)), % 79.46/79.63 inference(scs_inference,[],[8,12,40])). % 79.46/79.63 cnf(46,plain, % 79.46/79.63 (~P3(x461,x462,a2)+~P3(x463,a1,x461)+~P3(x462,x461,x463)), % 79.46/79.63 inference(scs_inference,[],[4,12,14])). % 79.46/79.63 cnf(47,plain, % 79.46/79.63 (~P3(x471,a3,x472)+~P3(x472,x473,a2)+~P3(x473,x472,x471)), % 79.46/79.63 inference(scs_inference,[],[7,12,14])). % 79.46/79.63 cnf(63,plain, % 79.46/79.63 (~P3(a2,a1,a1)+~P3(a2,a1,a2)+~P3(a2,a2,a3)), % 79.46/79.63 inference(scs_inference,[],[8,12,43])). % 79.46/79.63 cnf(65,plain, % 79.46/79.63 (~P3(a3,a2,a3)+P3(a3,a3,a2)+P3(a3,a3,a1)), % 79.46/79.63 inference(scs_inference,[],[9,3,12,10])). % 79.46/79.63 cnf(66,plain, % 79.46/79.63 (P3(a3,a3,a2)+~P3(a1,a1,a1)+~P3(a3,a2,a3)), % 79.46/79.63 inference(scs_inference,[],[65,18])). % 79.46/79.63 cnf(75,plain, % 79.46/79.63 (~P3(a1,a2,a3)+P3(a1,a1,a2)+P3(a1,a1,a1)), % 79.46/79.63 inference(scs_inference,[],[4,1,12,10])). % 79.46/79.63 cnf(83,plain, % 79.46/79.63 (~P3(a2,a1,a2)+P3(a2,a2,a3)+P3(a2,a2,a1)), % 79.46/79.63 inference(scs_inference,[],[6,2,12,10])). % 79.46/79.63 cnf(87,plain, % 79.46/79.63 (~P3(a2,a3,a3)+~P3(a2,a1,a2)+P3(a2,a2,a1)), % 79.46/79.63 inference(scs_inference,[],[7,12,83])). % 79.46/79.63 cnf(88,plain, % 79.46/79.63 (P3(a2,a2,a1)+~P3(a2,a3,a3)+P3(a2,a1,a1)), % 79.46/79.63 inference(scs_inference,[],[87,42])). % 79.46/79.63 cnf(89,plain, % 79.46/79.63 (~P3(a2,a3,a3)+~P3(a1,a1,a1)+P3(a2,a1,a1)), % 79.46/79.63 inference(scs_inference,[],[88,15])). % 79.46/79.63 cnf(94,plain, % 79.46/79.63 (~P3(a2,a1,a1)+~P3(a2,a1,a2)+P3(a2,a2,a3)), % 79.46/79.63 inference(scs_inference,[],[4,12,83])). % 79.46/79.63 cnf(95,plain, % 79.46/79.63 (~P3(a2,a1,a2)+~P3(a2,a1,a1)), % 79.46/79.63 inference(scs_inference,[],[94,63])). % 79.46/79.63 cnf(103,plain, % 79.46/79.63 (~P3(a2,a1,a2)+~P3(a1,a1,a1)+~P3(a2,a3,a3)), % 79.46/79.63 inference(scs_inference,[],[95,89])). % 79.46/79.63 cnf(106,plain, % 79.46/79.63 (~P3(a3,a2,a2)+P3(a3,a3,a3)+P3(a3,a3,a1)), % 79.46/79.63 inference(scs_inference,[],[9,3,12,10])). % 79.46/79.63 cnf(123,plain, % 79.46/79.63 (~P3(a2,a3,a2)+P3(a2,a1,a3)+P3(a2,a1,a1)), % 79.46/79.63 inference(scs_inference,[],[5,1,2,12,10])). % 79.46/79.63 cnf(126,plain, % 79.46/79.63 (~P3(a3,a3,a3)+P3(a3,a1,a2)+P3(a3,a1,a1)), % 79.46/79.63 inference(scs_inference,[],[8,1,3,12,10])). % 79.46/79.63 cnf(127,plain, % 79.46/79.63 (~P3(a1,a3,a3)+P3(a1,a2,a2)+P3(a1,a2,a1)), % 79.46/79.63 inference(scs_inference,[],[7,2,1,12,10])). % 79.46/79.63 cnf(128,plain, % 79.46/79.63 (P3(a1,a2,a2)+~P3(a2,a1,a2)+~P3(a1,a3,a3)), % 79.46/79.63 inference(scs_inference,[],[127,15])). % 79.46/79.63 cnf(129,plain, % 79.46/79.63 (~P3(a2,a1,a2)+~P3(a1,a3,a3)), % 79.46/79.63 inference(scs_inference,[],[128,46])). % 79.46/79.63 cnf(132,plain, % 79.46/79.63 (~P3(a2,a1,a2)+P3(a1,a3,a2)+P3(a1,a3,a1)), % 79.46/79.63 inference(scs_inference,[],[3,1,129,10])). % 79.46/79.63 cnf(144,plain, % 79.46/79.63 (~P3(a2,a2,a3)+~P3(a2,a3,a2)+P3(a2,a1,a1)), % 79.46/79.63 inference(scs_inference,[],[4,12,123])). % 79.46/79.63 cnf(145,plain, % 79.46/79.63 (~P3(a2,a2,a3)+P3(a2,a1,a1)+P3(a2,a3,a1)), % 79.46/79.63 inference(scs_inference,[],[144,40])). % 79.46/79.63 cnf(164,plain, % 79.46/79.63 (~P3(a3,a2,a2)+~P3(a3,a3,a3)+P3(a3,a1,a1)), % 79.46/79.63 inference(scs_inference,[],[6,12,126])). % 79.46/79.63 cnf(165,plain, % 79.46/79.63 (P3(a3,a3,a1)+~P3(a3,a2,a2)+P3(a3,a1,a1)), % 79.46/79.63 inference(scs_inference,[],[164,106])). % 79.46/79.63 cnf(166,plain, % 79.46/79.63 (~P3(a3,a2,a2)+~P3(a1,a1,a1)+P3(a3,a1,a1)), % 79.46/79.63 inference(scs_inference,[],[165,18])). % 79.46/79.63 cnf(196,plain, % 79.46/79.63 (~P3(a3,a3,a1)+P3(a3,a1,a2)+P3(a3,a1,a3)), % 79.46/79.63 inference(scs_inference,[],[8,1,3,12,10])). % 79.46/79.63 cnf(227,plain, % 79.46/79.63 (~P3(a1,a2,a1)+P3(a1,a3,a2)+P3(a1,a3,a3)), % 79.46/79.63 inference(scs_inference,[],[9,3,1,12,10])). % 79.46/79.63 cnf(228,plain, % 79.46/79.63 (~P3(a1,a1,a3)+~P3(a1,a2,a1)+P3(a1,a3,a2)), % 79.46/79.63 inference(scs_inference,[],[5,12,227])). % 79.46/79.63 cnf(234,plain, % 79.46/79.63 (~P3(a1,a2,a1)+P3(a1,a1,a2)+P3(a1,a1,a3)), % 79.46/79.63 inference(scs_inference,[],[4,1,12,10])). % 79.46/79.63 cnf(235,plain, % 79.46/79.63 (P3(a1,a1,a3)+~P3(a1,a2,a1)), % 79.46/79.63 inference(scs_inference,[],[234,17])). % 79.46/79.63 cnf(253,plain, % 79.46/79.63 (P3(a1,a1,a3)+P3(a1,a2,a2)+P3(a1,a2,a3)), % 79.46/79.63 inference(scs_inference,[],[2,1,235,10])). % 79.46/79.63 cnf(258,plain, % 79.46/79.63 (P3(a3,a3,a1)+~P3(a1,a2,a1)), % 79.46/79.63 inference(scs_inference,[],[235,14])). % 79.46/79.63 cnf(13410,plain, % 79.46/79.63 (~P3(x134101,x134102,a2)+~P3(x134101,x134102,a3)), % 79.46/79.63 inference(scs_inference,[],[9,11])). % 79.46/79.63 cnf(13412,plain, % 79.46/79.63 (~P3(a2,x134121,x134122)+~P3(a3,x134121,x134122)), % 79.46/79.63 inference(scs_inference,[],[9,11,13])). % 79.46/79.63 cnf(13414,plain, % 79.46/79.63 (~P3(a1,a2,a1)+~P3(a1,a1,a2)), % 79.46/79.63 inference(scs_inference,[],[13410,235])). % 79.46/79.63 cnf(13417,plain, % 79.46/79.63 (~P3(x134171,a1,x134172)+~P3(x134171,a3,x134172)), % 79.46/79.63 inference(scs_inference,[],[8,11,12])). % 79.46/79.63 cnf(13422,plain, % 79.46/79.63 (~P3(a1,x134221,x134222)+~P3(a3,x134221,x134222)), % 79.46/79.63 inference(scs_inference,[],[8,13])). % 79.46/79.63 cnf(13427,plain, % 79.46/79.63 (~P3(a1,x134271,x134272)+~P3(a2,x134271,x134272)), % 79.46/79.63 inference(scs_inference,[],[6,13])). % 79.46/79.63 cnf(13429,plain, % 79.46/79.63 (~P3(a1,a1,a1)+~P3(a2,a3,a3)+P3(a2,a1,a2)), % 79.46/79.63 inference(scs_inference,[],[6,13,42])). % 79.46/79.63 cnf(13430,plain, % 79.46/79.63 (~P3(x134301,a2,x134302)+~P3(x134301,a3,x134302)), % 79.46/79.63 inference(scs_inference,[],[9,12])). % 79.46/79.63 cnf(13433,plain, % 79.46/79.63 (P3(a2,a2,a2)+P3(a2,a2,a3)+P3(a2,a2,a1)), % 79.46/79.63 inference(scs_inference,[],[2,10])). % 79.46/79.63 cnf(13435,plain, % 79.46/79.63 (~P3(x134351,a2,x134352)+~P3(x134351,a1,x134352)), % 79.46/79.63 inference(scs_inference,[],[4,12])). % 79.46/79.63 cnf(13443,plain, % 79.46/79.63 (~P3(a2,a2,a3)+P3(a2,a3,a1)+~P3(a1,a3,a2)), % 79.46/79.63 inference(scs_inference,[],[13427,40])). % 79.46/79.63 cnf(13447,plain, % 79.46/79.63 (P3(a3,a3,a2)+P3(a3,a3,a3)+P3(a3,a3,a1)), % 79.46/79.63 inference(scs_inference,[],[3,10])). % 79.46/79.63 cnf(13454,plain, % 79.46/79.63 (P3(a1,a1,a2)+P3(a1,a1,a3)+P3(a1,a1,a1)), % 79.46/79.63 inference(scs_inference,[],[1,10])). % 79.46/79.63 cnf(13458,plain, % 79.46/79.63 (~P3(a2,a3,a3)+~P3(a1,a1,a1)), % 79.46/79.63 inference(scs_inference,[],[103,13429])). % 79.46/79.63 cnf(13459,plain, % 79.46/79.63 (~P3(a1,a1,a1)+P3(a2,a3,a2)+P3(a2,a3,a1)), % 79.46/79.63 inference(scs_inference,[],[3,2,13458,10])). % 79.46/79.63 cnf(13465,plain, % 79.46/79.63 (~P3(a3,a2,a2)+~P3(a1,a1,a1)), % 79.46/79.63 inference(scs_inference,[],[166,13422])). % 79.46/79.63 cnf(13466,plain, % 79.46/79.63 (~P3(a1,x134661,a1)+~P3(x134661,a1,a1)+~P3(a3,a2,a2)), % 79.46/79.63 inference(scs_inference,[],[13465,14])). % 79.46/79.63 cnf(13469,plain, % 79.46/79.63 (~P3(a1,a2,a1)+P3(a1,a3,a2)), % 79.46/79.63 inference(scs_inference,[],[228,235])). % 79.46/79.63 cnf(13478,plain, % 79.46/79.63 (P3(a2,a2,a3)+P3(a2,a2,a2)+~P3(a1,a1,a3)), % 79.46/79.63 inference(scs_inference,[],[13433,20])). % 79.46/79.63 cnf(16733,plain, % 79.46/79.63 (P3(a1,a2,a3)+P3(a1,a2,a2)+~P3(a1,a1,a2)), % 79.46/79.63 inference(scs_inference,[],[13410,253])). % 79.46/79.63 cnf(16734,plain, % 79.46/79.63 (P3(a1,a2,a3)+~P3(a1,a1,a2)), % 79.46/79.63 inference(scs_inference,[],[16733,13435])). % 79.46/79.63 cnf(16735,plain, % 79.46/79.63 (P3(a1,a2,a3)+P3(a1,a1,a1)+P3(a1,a1,a3)), % 79.46/79.63 inference(scs_inference,[],[16734,13454])). % 79.46/79.63 cnf(16765,plain, % 79.46/79.63 (P3(a2,a2,a2)+~P3(a1,a1,a3)+~P3(a3,a2,a3)), % 79.46/79.63 inference(scs_inference,[],[13412,13478])). % 79.46/79.63 cnf(16768,plain, % 79.46/79.63 (P3(a3,a1,a1)+P3(a3,a1,a3)+~P3(a2,a1,a2)), % 79.46/79.63 inference(scs_inference,[],[1,3,13412,10])). % 79.46/79.63 cnf(16769,plain, % 79.46/79.63 (~P3(a3,a2,a2)+P3(a2,a2,a1)+P3(a2,a2,a3)), % 79.46/79.63 inference(scs_inference,[],[2,13412,10])). % 79.46/79.63 cnf(16770,plain, % 79.46/79.63 (P3(a2,a2,a1)+~P3(a3,a2,a2)+~P3(a3,a3,a3)), % 79.46/79.63 inference(scs_inference,[],[16769,20])). % 79.46/79.63 cnf(16771,plain, % 79.46/79.63 (P3(a2,a2,a1)+P3(a3,a3,a1)+~P3(a3,a2,a2)), % 79.46/79.63 inference(scs_inference,[],[16770,106])). % 79.46/79.63 cnf(16775,plain, % 79.46/79.63 (P3(a2,a2,a1)+~P3(a3,a2,a2)+~P3(a2,a3,a1)), % 79.46/79.63 inference(scs_inference,[],[13412,16771])). % 79.46/79.63 cnf(16776,plain, % 79.46/79.63 (~P3(a3,a2,a2)+~P3(a2,a3,a1)), % 79.46/79.63 inference(scs_inference,[],[16775,13430])). % 79.46/79.63 cnf(16778,plain, % 79.46/79.63 (~P3(a3,a2,a2)+P3(a2,a3,a3)+P3(a2,a3,a2)), % 79.46/79.63 inference(scs_inference,[],[2,3,16776,10])). % 79.46/79.63 cnf(16779,plain, % 79.46/79.63 (~P3(a3,a2,a2)+P3(a2,a3,a3)), % 79.46/79.63 inference(scs_inference,[],[16778,47])). % 79.46/79.63 cnf(16780,plain, % 79.46/79.63 (P3(a2,a3,a3)+P3(a3,a2,a3)+P3(a3,a2,a1)), % 79.46/79.63 inference(scs_inference,[],[2,3,16779,10])). % 79.46/79.63 cnf(16788,plain, % 79.46/79.63 (P3(a3,a2,a3)+P3(a3,a2,a1)+~P3(a3,a3,a3)), % 79.46/79.63 inference(scs_inference,[],[13412,16780])). % 79.46/79.63 cnf(16789,plain, % 79.46/79.63 (P3(a3,a2,a1)+~P3(a3,a3,a3)), % 79.46/79.63 inference(scs_inference,[],[16788,13430])). % 79.46/79.63 cnf(16790,plain, % 79.46/79.63 (~P3(a3,x167901,a3)+~P3(x167901,a3,a3)+P3(a3,a2,a1)), % 79.46/79.63 inference(scs_inference,[],[16789,14])). % 79.46/79.63 cnf(16791,plain, % 79.46/79.63 (~P3(a3,a1,a1)+~P3(x167911,a3,a3)+~P3(a3,x167911,a3)), % 79.46/79.63 inference(scs_inference,[],[16790,13435])). % 79.46/79.64 cnf(16801,plain, % 79.46/79.64 (P3(a3,a2,a1)+P3(a2,a3,a3)+~P3(a2,a2,a3)), % 79.46/79.64 inference(scs_inference,[],[13412,16780])). % 79.46/79.64 cnf(16803,plain, % 79.46/79.64 (P3(a3,a2,a1)+~P3(a2,a2,a3)), % 79.46/79.64 inference(scs_inference,[],[16801,13430])). % 79.46/79.64 cnf(16806,plain, % 79.46/79.64 (~P3(a3,a1,a1)+P3(a2,a1,a3)+P3(a2,a1,a2)), % 79.46/79.64 inference(scs_inference,[],[2,1,13412,10])). % 79.46/79.64 cnf(16809,plain, % 79.46/79.64 (P3(a3,a1,a2)+P3(a3,a1,a1)+~P3(a2,a1,a3)), % 79.46/79.64 inference(scs_inference,[],[1,3,13412,10])). % 79.46/79.64 cnf(16833,plain, % 79.46/79.64 (~P3(a3,a2,a2)+~P3(a2,a1,a3)), % 79.46/79.64 inference(scs_inference,[],[13417,16779])). % 79.46/79.64 cnf(16835,plain, % 79.46/79.64 (~P3(a3,a3,a2)+P3(a3,a1,a3)+P3(a3,a1,a1)), % 79.46/79.64 inference(scs_inference,[],[3,1,13417,10])). % 79.46/79.64 cnf(16843,plain, % 79.46/79.64 (P3(a3,a3,a2)+P3(a3,a3,a3)+~P3(a3,a1,a1)), % 79.46/79.64 inference(scs_inference,[],[13417,13447])). % 79.46/79.64 cnf(16845,plain, % 79.46/79.64 (P3(a3,a3,a2)+~P3(a3,a1,a1)), % 79.46/79.64 inference(scs_inference,[],[16843,16791])). % 79.46/79.64 cnf(16867,plain, % 79.46/79.64 (~P3(a2,a2,a3)+~P3(a1,a2,a1)), % 79.46/79.64 inference(scs_inference,[],[13422,16803])). % 79.46/79.64 cnf(16868,plain, % 79.46/79.64 (~P3(a3,x168681,a2)+~P3(x168681,a3,a2)+~P3(a1,a2,a1)), % 79.46/79.64 inference(scs_inference,[],[16867,14])). % 79.46/79.64 cnf(16869,plain, % 79.46/79.64 (~P3(a1,a2,a1)+~P3(a3,a1,a2)), % 79.46/79.64 inference(scs_inference,[],[16868,13469])). % 79.46/79.64 cnf(16870,plain, % 79.46/79.64 (~P3(a3,a3,a1)+~P3(a1,a2,a1)+P3(a3,a1,a3)), % 79.46/79.64 inference(scs_inference,[],[16869,196])). % 79.46/79.64 cnf(16872,plain, % 79.46/79.64 (~P3(a1,a2,a1)+P3(a3,a1,a3)), % 79.46/79.64 inference(scs_inference,[],[16870,258])). % 79.46/79.64 cnf(16878,plain, % 79.46/79.64 (~P3(a3,a1,a1)+~P3(a1,a3,a2)), % 79.46/79.64 inference(scs_inference,[],[13422,16845])). % 79.46/79.64 cnf(16880,plain, % 79.46/79.64 (P3(a1,a1,a1)+P3(a1,a1,a3)+~P3(a3,a2,a3)), % 79.46/79.64 inference(scs_inference,[],[13422,16735])). % 79.46/79.64 cnf(16881,plain, % 79.46/79.64 (P3(a1,a1,a1)+P3(a2,a2,a2)+~P3(a3,a2,a3)), % 79.46/79.64 inference(scs_inference,[],[16880,16765])). % 79.46/79.64 cnf(16890,plain, % 79.46/79.64 (P3(a1,a2,a3)+P3(a1,a1,a3)+~P3(a3,a1,a1)), % 79.46/79.64 inference(scs_inference,[],[13422,16735])). % 79.46/79.64 cnf(16891,plain, % 79.46/79.64 (P3(a1,a2,a3)+~P3(a3,a1,a1)), % 79.46/79.64 inference(scs_inference,[],[16890,16])). % 79.46/79.64 cnf(16892,plain, % 79.46/79.64 (P3(a1,a2,a3)+~P3(a2,a1,a2)+P3(a3,a1,a3)), % 79.46/79.64 inference(scs_inference,[],[16891,16768])). % 79.46/79.64 cnf(16905,plain, % 79.46/79.64 (~P3(a3,a3,a2)+P3(a3,a1,a3)+~P3(a1,a1,a1)), % 79.46/79.64 inference(scs_inference,[],[13422,16835])). % 79.46/79.64 cnf(16906,plain, % 79.46/79.64 (~P3(a3,a2,a3)+~P3(a1,a1,a1)+P3(a3,a1,a3)), % 79.46/79.64 inference(scs_inference,[],[16905,66])). % 79.46/79.64 cnf(16907,plain, % 79.46/79.64 (P3(a1,a1,a3)+~P3(a3,a2,a3)+P3(a3,a1,a3)), % 79.46/79.64 inference(scs_inference,[],[16906,16880])). % 79.46/79.64 cnf(16909,plain, % 79.46/79.64 (P3(a1,a1,a3)+~P3(a3,a2,a3)), % 79.46/79.64 inference(scs_inference,[],[16907,13435])). % 79.46/79.64 cnf(16910,plain, % 79.46/79.64 (P3(a1,a1,a3)+P3(a3,a2,a1)+P3(a3,a2,a2)), % 79.46/79.64 inference(scs_inference,[],[2,3,16909,10])). % 79.46/79.64 cnf(16912,plain, % 79.46/79.64 (P3(a3,a2,a1)+P3(a3,a2,a2)+~P3(a3,a1,a3)), % 79.46/79.64 inference(scs_inference,[],[13422,16910])). % 79.46/79.64 cnf(16913,plain, % 79.46/79.64 (~P3(a1,a2,a1)+P3(a3,a2,a1)+P3(a3,a2,a2)), % 79.46/79.64 inference(scs_inference,[],[16912,16872])). % 79.46/79.64 cnf(16915,plain, % 79.46/79.64 (P3(a3,a2,a2)+~P3(a1,a2,a1)), % 79.46/79.64 inference(scs_inference,[],[16913,13422])). % 79.46/79.64 cnf(16921,plain, % 79.46/79.64 (P3(a1,a2,a3)+P3(a1,a1,a1)+~P3(a3,a1,a3)), % 79.46/79.64 inference(scs_inference,[],[13422,16735])). % 79.46/79.64 cnf(16922,plain, % 79.46/79.64 (P3(a1,a1,a1)+~P3(a2,a1,a2)+P3(a1,a2,a3)), % 79.46/79.64 inference(scs_inference,[],[16921,16892])). % 79.46/79.64 cnf(16923,plain, % 79.46/79.64 (P3(a1,a1,a1)+~P3(a2,a1,a2)+~P3(a1,a3,a1)), % 79.46/79.64 inference(scs_inference,[],[16922,17])). % 79.46/79.64 cnf(16924,plain, % 79.46/79.64 (P3(a1,a1,a1)+~P3(a2,a1,a2)+P3(a1,a3,a2)), % 79.46/79.64 inference(scs_inference,[],[16923,132])). % 79.46/79.64 cnf(16931,plain, % 79.46/79.64 (~P3(a2,a1,a2)+P3(a1,a3,a2)+~P3(a3,a1,a1)), % 79.46/79.64 inference(scs_inference,[],[13422,16924])). % 79.46/79.64 cnf(16932,plain, % 79.46/79.64 (~P3(a3,a1,a1)+P3(a2,a1,a3)+P3(a1,a3,a2)), % 79.46/79.64 inference(scs_inference,[],[16931,16806])). % 79.46/79.64 cnf(16933,plain, % 79.46/79.64 (~P3(a3,a1,a1)+P3(a2,a1,a3)), % 79.46/79.64 inference(scs_inference,[],[16932,16878])). % 79.46/79.64 cnf(16960,plain, % 79.46/79.64 (~P3(a3,a1,a1)+P3(a1,a1,a2)+P3(a1,a1,a3)), % 79.46/79.64 inference(scs_inference,[],[1,13422,10])). % 79.46/79.64 cnf(16961,plain, % 79.46/79.64 (P3(a1,a1,a2)+~P3(a3,a1,a1)+~P3(a3,a3,a2)), % 79.46/79.64 inference(scs_inference,[],[16960,19])). % 79.46/79.64 cnf(16962,plain, % 79.46/79.64 (P3(a1,a1,a2)+~P3(a3,a1,a1)), % 79.46/79.64 inference(scs_inference,[],[16961,16845])). % 79.46/79.64 cnf(16980,plain, % 79.46/79.64 (P3(a3,a2,a2)+P3(a3,a2,a1)+~P3(a1,a2,a3)), % 79.46/79.64 inference(scs_inference,[],[3,2,13422,10])). % 79.46/79.64 cnf(16981,plain, % 79.46/79.64 (~P3(a1,a1,a2)+P3(a3,a2,a1)+P3(a3,a2,a2)), % 79.46/79.64 inference(scs_inference,[],[16980,16734])). % 79.46/79.64 cnf(16982,plain, % 79.46/79.64 (~P3(a3,a1,a1)+P3(a3,a2,a1)+P3(a3,a2,a2)), % 79.46/79.64 inference(scs_inference,[],[16981,16962])). % 79.46/79.64 cnf(16983,plain, % 79.46/79.64 (P3(a3,a2,a2)+~P3(a3,a1,a1)), % 79.46/79.64 inference(scs_inference,[],[16982,13435])). % 79.46/79.64 cnf(16985,plain, % 79.46/79.64 (~P3(a2,a1,a3)+P3(a3,a1,a2)+P3(a3,a2,a2)), % 79.46/79.64 inference(scs_inference,[],[16983,16809])). % 79.46/79.64 cnf(16986,plain, % 79.46/79.64 (~P3(a2,a1,a3)+P3(a3,a1,a2)), % 79.46/79.64 inference(scs_inference,[],[16985,16833])). % 79.46/79.64 cnf(17004,plain, % 79.46/79.64 (~P3(a3,a1,a3)+P3(a1,a1,a1)+P3(a1,a1,a2)), % 79.46/79.64 inference(scs_inference,[],[1,13422,10])). % 79.46/79.64 cnf(17006,plain, % 79.46/79.64 (P3(a1,a1,a1)+P3(a1,a1,a2)+~P3(a1,a2,a1)), % 79.46/79.64 inference(scs_inference,[],[17004,16872])). % 79.46/79.64 cnf(17007,plain, % 79.46/79.64 (P3(a1,a1,a2)+~P3(a1,a2,a1)+~P3(a3,a2,a2)), % 79.46/79.64 inference(scs_inference,[],[17006,13466])). % 79.46/79.64 cnf(17008,plain, % 79.46/79.64 (~P3(a1,a2,a1)+~P3(a3,a2,a2)), % 79.46/79.64 inference(scs_inference,[],[17007,13414])). % 79.46/79.64 cnf(17009,plain, % 79.46/79.64 (~P3(a3,a2,a2)+P3(a1,a2,a3)+P3(a1,a2,a2)), % 79.46/79.64 inference(scs_inference,[],[2,1,17008,10])). % 79.46/79.64 cnf(17014,plain, % 79.46/79.64 (~P3(a2,a1,a3)+~P3(a1,a1,a2)), % 79.46/79.64 inference(scs_inference,[],[13422,16986])). % 79.46/79.64 cnf(17015,plain, % 79.46/79.64 (~P3(a3,a1,a1)+~P3(a2,a1,a3)), % 79.46/79.64 inference(scs_inference,[],[17014,16962])). % 79.46/79.64 cnf(17016,plain, % 79.46/79.64 (~P3(a3,a1,a1)), % 79.46/79.64 inference(scs_inference,[],[17015,16933])). % 79.46/79.64 cnf(17019,plain, % 79.46/79.64 (~P3(a1,x170191,a1)+~P3(x170191,a1,a3)), % 79.46/79.64 inference(scs_inference,[],[17016,14])). % 79.46/79.64 cnf(17024,plain, % 79.46/79.64 (~P3(a3,a2,a3)+~P3(a1,a1,a1)), % 79.46/79.64 inference(scs_inference,[],[17019,16909])). % 79.46/79.64 cnf(17026,plain, % 79.46/79.64 (P3(a2,a2,a2)+~P3(a3,a2,a3)), % 79.46/79.64 inference(scs_inference,[],[17024,16881])). % 79.46/79.64 cnf(17050,plain, % 79.46/79.64 (P3(a1,a2,a3)+~P3(a3,a2,a2)), % 79.46/79.64 inference(scs_inference,[],[13422,17009])). % 79.46/79.64 cnf(17051,plain, % 79.46/79.64 (~P3(a3,a2,a2)+~P3(a1,a1,a3)), % 79.46/79.64 inference(scs_inference,[],[17050,13435])). % 79.46/79.64 cnf(17052,plain, % 79.46/79.64 (~P3(a3,x170521,a1)+~P3(x170521,a3,a1)+~P3(a3,a2,a2)), % 79.46/79.64 inference(scs_inference,[],[17051,14])). % 79.46/79.64 cnf(17053,plain, % 79.46/79.64 (~P3(a1,a2,a1)+~P3(x170531,a3,a1)+~P3(a3,x170531,a1)), % 79.46/79.64 inference(scs_inference,[],[17052,16915])). % 79.46/79.64 cnf(17054,plain, % 79.46/79.64 (~P3(a1,a2,a1)+~P3(a3,a3,a1)), % 79.46/79.64 inference(scs_inference,[],[17053,258])). % 79.46/79.64 cnf(17056,plain, % 79.46/79.64 (~P3(a1,a2,a1)), % 79.46/79.64 inference(scs_inference,[],[17054,258])). % 79.46/79.64 cnf(17061,plain, % 79.46/79.64 (P3(a1,a2,a3)+P3(a1,a2,a2)), % 79.46/79.64 inference(scs_inference,[],[17056,2,1,10])). % 79.46/79.64 cnf(17066,plain, % 79.46/79.64 (P3(a1,a2,a3)+~P3(a2,a2,a2)), % 79.46/79.64 inference(scs_inference,[],[17061,13427])). % 79.46/79.64 cnf(17067,plain, % 79.46/79.64 (P3(a1,a2,a3)+~P3(a3,a2,a3)), % 79.46/79.64 inference(scs_inference,[],[17066,17026])). % 79.46/79.64 cnf(17108,plain, % 79.46/79.64 (~P3(a3,a2,a3)), % 79.46/79.64 inference(scs_inference,[],[13422,17067])). % 79.46/79.64 cnf(17116,plain, % 79.46/79.64 (~P3(a3,x171161,a2)+~P3(x171161,a3,a3)), % 79.46/79.64 inference(scs_inference,[],[17108,14])). % 79.46/79.64 cnf(17127,plain, % 79.46/79.64 (P3(a3,a2,a2)+P3(a3,a2,a1)), % 79.46/79.64 inference(scs_inference,[],[17108,3,2,10])). % 79.46/79.64 cnf(17134,plain, % 79.46/79.64 (~P3(a3,a2,a2)), % 79.46/79.64 inference(scs_inference,[],[17116,16779])). % 79.46/79.64 cnf(17139,plain, % 79.46/79.64 (P3(a3,a2,a1)), % 79.46/79.64 inference(scs_inference,[],[17134,17127])). % 79.46/79.64 cnf(17159,plain, % 79.46/79.64 (~P3(a2,a2,a1)), % 79.46/79.64 inference(scs_inference,[],[17139,13412])). % 79.46/79.64 cnf(17165,plain, % 79.46/79.64 (~P3(a2,a3,x171651)+~P3(a1,x171651,a1)), % 79.46/79.64 inference(scs_inference,[],[17139,13412,13,39,15])). % 79.46/79.64 cnf(17167,plain, % 79.46/79.64 (~P3(a2,a3,a3)+~P3(a2,a1,a2)), % 79.46/79.64 inference(scs_inference,[],[17159,87])). % 79.46/79.64 cnf(17169,plain, % 79.46/79.64 (P3(a2,a2,a2)+P3(a2,a2,a3)), % 79.46/79.64 inference(scs_inference,[],[17159,13433])). % 79.46/79.64 cnf(17179,plain, % 79.46/79.64 (~P3(a2,a3,a1)), % 79.46/79.64 inference(scs_inference,[],[17139,27,14])). % 79.46/79.64 cnf(17184,plain, % 79.46/79.64 (~P3(a2,a2,a3)+P3(a2,a1,a1)), % 79.46/79.64 inference(scs_inference,[],[17179,145])). % 79.46/79.64 cnf(17185,plain, % 79.46/79.64 (~P3(a2,a2,a3)+~P3(a1,a3,a2)), % 79.46/79.64 inference(scs_inference,[],[17179,13443])). % 79.46/79.64 cnf(17186,plain, % 79.46/79.64 (~P3(a1,a1,a1)+P3(a2,a3,a2)), % 79.46/79.64 inference(scs_inference,[],[17179,13459])). % 79.46/79.64 cnf(17202,plain, % 79.46/79.64 (~P3(a2,a1,a3)), % 79.46/79.64 inference(scs_inference,[],[17056,17139,2,1,37,10,17066,17169,17184,17185,13435])). % 79.46/79.64 cnf(17215,plain, % 79.46/79.64 (~P3(a2,a3,a2)), % 79.46/79.64 inference(scs_inference,[],[17202,17139,14])). % 79.46/79.64 cnf(17227,plain, % 79.46/79.64 (~P3(a1,a1,a1)), % 79.46/79.64 inference(scs_inference,[],[17215,17186])). % 79.46/79.64 cnf(17234,plain, % 79.46/79.64 (~P3(a1,a1,a2)), % 79.46/79.64 inference(scs_inference,[],[17215,17179,17139,3,2,10,17167,24,16])). % 79.46/79.64 cnf(17245,plain, % 79.46/79.64 (P3(a1,a2,a3)), % 79.46/79.64 inference(scs_inference,[],[17215,17179,17139,6,3,2,10,17167,24,16,27,37,42,13,17165,17061])). % 79.46/79.64 cnf(17274,plain, % 79.46/79.64 ($false), % 79.46/79.64 inference(scs_inference,[],[17227,17234,17245,75]), % 79.46/79.64 ['proof']). % 79.46/79.64 % SZS output end Proof % 79.46/79.64 % Total time :78.830000s %------------------------------------------------------------------------------