%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP577-1 : TPTP v8.2.0. Released v2.6.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n017.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:39:58 EDT 2024 % Result : Unsatisfiable 181.50s 182.45s % Output : CNFRefutation 181.60s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.05/0.11 % Problem : GRP577-1 : TPTP v8.2.0. Released v2.6.0. % 0.05/0.11 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.10/0.31 % Computer : n017.cluster.edu % 0.10/0.31 % Model : x86_64 x86_64 % 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.31 % Memory : 8042.1875MB % 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.31 % CPULimit : 300 % 0.10/0.31 % WCLimit : 300 % 0.10/0.31 % DateTime : Thu Jun 20 07:14:24 EDT 2024 % 0.10/0.31 % CPUTime : % 0.51/0.55 start to proof:theBenchmark % 181.50/182.42 %------------------------------------------- % 181.50/182.42 % File :CSE---1.7 % 181.50/182.42 % Problem :theBenchmark % 181.50/182.42 % Transform :cnf % 181.50/182.42 % Format :tptp:raw % 181.50/182.42 % Command :java -jar mcs_scs.jar %d %s % 181.50/182.42 % 181.50/182.42 % Result :Theorem 180.880000s % 181.50/182.42 % Output :CNFRefutation 180.880000s % 181.50/182.42 %------------------------------------------- % 181.50/182.45 %-------------------------------------------------------------------------- % 181.50/182.45 % File : GRP577-1 : TPTP v8.2.0. Released v2.6.0. % 181.50/182.45 % Domain : Group Theory (Abelian) % 181.50/182.45 % Problem : Axiom for Abelian group theory, in double div and id, part 1 % 181.50/182.45 % Version : [McC93] (equality) axioms. % 181.50/182.45 % English : % 181.50/182.45 % 181.50/182.45 % Refs : [McC93] McCune (1993), Single Axioms for Groups and Abelian Gr % 181.50/182.45 % Source : [TPTP] % 181.50/182.45 % Names : % 181.50/182.45 % 181.50/182.45 % Status : Unsatisfiable % 181.50/182.45 % Rating : 0.05 v8.2.0, 0.04 v8.1.0, 0.05 v7.5.0, 0.04 v7.4.0, 0.09 v7.3.0, 0.05 v7.1.0, 0.00 v7.0.0, 0.05 v6.4.0, 0.11 v6.3.0, 0.06 v6.2.0, 0.07 v6.1.0, 0.06 v6.0.0, 0.19 v5.5.0, 0.16 v5.4.0, 0.00 v5.1.0, 0.07 v5.0.0, 0.00 v2.6.0 % 181.50/182.45 % Syntax : Number of clauses : 5 ( 5 unt; 0 nHn; 1 RR) % 181.50/182.45 % Number of literals : 5 ( 5 equ; 1 neg) % 181.50/182.45 % Maximal clause size : 1 ( 1 avg) % 181.50/182.45 % Maximal term depth : 6 ( 2 avg) % 181.50/182.45 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 181.50/182.45 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty) % 181.50/182.45 % Number of variables : 7 ( 0 sgn) % 181.50/182.45 % SPC : CNF_UNS_RFO_PEQ_UEQ % 181.50/182.45 % 181.50/182.45 % Comments : A UEQ part of GRP102-1 % 181.50/182.45 %-------------------------------------------------------------------------- % 181.50/182.45 cnf(single_axiom,axiom, % 181.50/182.45 double_divide(double_divide(A,double_divide(double_divide(double_divide(B,A),C),double_divide(B,identity))),double_divide(identity,identity)) = C ). % 181.50/182.45 % 181.50/182.45 cnf(multiply,axiom, % 181.50/182.45 multiply(A,B) = double_divide(double_divide(B,A),identity) ). % 181.50/182.45 % 181.50/182.45 cnf(inverse,axiom, % 181.50/182.45 inverse(A) = double_divide(A,identity) ). % 181.50/182.45 % 181.50/182.45 cnf(identity,axiom, % 181.50/182.45 identity = double_divide(A,inverse(A)) ). % 181.50/182.45 % 181.50/182.45 cnf(prove_these_axioms_1,negated_conjecture, % 181.50/182.45 multiply(inverse(a1),a1) != identity ). % 181.50/182.45 % 181.50/182.45 %-------------------------------------------------------------------------- % 181.50/182.45 %------------------------------------------- % 181.50/182.45 % Proof found % 181.50/182.45 % SZS status Theorem for theBenchmark % 181.50/182.45 % SZS output start Proof % 181.58/182.48 %ClaNum:8(EqnAxiom:5) % 181.58/182.48 %VarNum:8(SingletonVarNum:4) % 181.58/182.48 %MaxLitNum:1 % 181.58/182.48 %MaxfuncDepth:3 % 181.58/182.48 %SharedTerms:7 % 181.58/182.48 %goalClause: 8 % 181.58/182.48 %singleGoalClaCount:1 % 181.58/182.48 [8]~E(f2(f2(a3,f2(a3,a1)),a1),a1) % 181.58/182.48 [6]E(f2(x61,f2(x61,a1)),a1) % 181.58/182.48 [7]E(f2(f2(x71,f2(f2(f2(x72,x71),x73),f2(x72,a1))),f2(a1,a1)),x73) % 181.58/182.48 %EqnAxiom % 181.58/182.48 [1]E(x11,x11) % 181.58/182.48 [2]E(x22,x21)+~E(x21,x22) % 181.58/182.48 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 181.58/182.48 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 181.58/182.48 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 181.58/182.48 % 181.58/182.48 %------------------------------------------- % 181.60/182.52 cnf(9,plain, % 181.60/182.52 (E(x91,f2(f2(x92,f2(f2(f2(x93,x92),x91),f2(x93,a1))),f2(a1,a1)))), % 181.60/182.52 inference(scs_inference,[],[7,2])). % 181.60/182.52 cnf(10,plain, % 181.60/182.52 (~E(f2(f2(a3,f2(a3,a1)),a1),f2(x101,f2(x101,a1)))), % 181.60/182.52 inference(scs_inference,[],[8,7,6,2,3])). % 181.60/182.52 cnf(11,plain, % 181.60/182.52 (~E(a1,f2(f2(a3,f2(a3,a1)),a1))), % 181.60/182.52 inference(scs_inference,[],[8,7,6,2,3,5])). % 181.60/182.52 cnf(12,plain, % 181.60/182.52 (E(a1,f2(x121,f2(x121,a1)))), % 181.60/182.52 inference(scs_inference,[],[6,2])). % 181.60/182.52 cnf(13,plain, % 181.60/182.52 (E(f2(x131,f2(x131,a1)),f2(f2(x132,f2(f2(f2(x133,x132),a1),f2(x133,a1))),f2(a1,a1)))), % 181.60/182.52 inference(scs_inference,[],[6,9,3])). % 181.60/182.52 cnf(15,plain, % 181.60/182.52 (E(f2(f2(x151,f2(f2(f2(x152,x151),a1),f2(x152,a1))),f2(a1,a1)),f2(x153,f2(x153,a1)))), % 181.60/182.52 inference(scs_inference,[],[6,9,3,2])). % 181.60/182.52 cnf(16,plain, % 181.60/182.52 (~E(f2(f2(a3,f2(a3,a1)),a1),f2(f2(x161,f2(f2(f2(x162,x161),a1),f2(x162,a1))),f2(a1,a1)))), % 181.60/182.52 inference(scs_inference,[],[15,10,3])). % 181.60/182.52 cnf(18,plain, % 181.60/182.52 (E(f2(f2(x181,f2(x181,a1)),x182),f2(a1,x182))), % 181.60/182.52 inference(scs_inference,[],[6,4])). % 181.60/182.52 cnf(19,plain, % 181.60/182.52 (E(f2(x191,f2(x192,f2(x192,a1))),f2(x191,a1))), % 181.60/182.52 inference(scs_inference,[],[6,4,5])). % 181.60/182.52 cnf(21,plain, % 181.60/182.52 (~E(f2(x211,f2(x211,a1)),f2(f2(a3,f2(a3,a1)),a1))), % 181.60/182.52 inference(scs_inference,[],[6,12,11,16,4,5,2,3])). % 181.60/182.52 cnf(22,plain, % 181.60/182.52 (E(f2(f2(f2(x221,f2(x221,a1)),x222),x223),f2(f2(a1,x222),x223))), % 181.60/182.52 inference(scs_inference,[],[18,4])). % 181.60/182.52 cnf(23,plain, % 181.60/182.52 (E(f2(x231,f2(f2(x232,f2(x232,a1)),x233)),f2(x231,f2(a1,x233)))), % 181.60/182.52 inference(scs_inference,[],[18,4,5])). % 181.60/182.52 cnf(24,plain, % 181.60/182.52 (E(f2(f2(x241,f2(x241,a1)),f2(x242,f2(x242,a1))),f2(a1,a1))), % 181.60/182.52 inference(scs_inference,[],[18,19,4,5,3])). % 181.60/182.52 cnf(27,plain, % 181.60/182.52 (E(f2(f2(f2(x271,f2(x271,a1)),f2(x272,f2(x272,a1))),x273),f2(f2(a1,a1),x273))), % 181.60/182.52 inference(scs_inference,[],[24,4])). % 181.60/182.52 cnf(28,plain, % 181.60/182.52 (E(f2(x281,f2(f2(x282,f2(x282,a1)),f2(x283,f2(x283,a1)))),f2(x281,f2(a1,a1)))), % 181.60/182.52 inference(scs_inference,[],[24,4,5])). % 181.60/182.52 cnf(29,plain, % 181.60/182.52 (~E(f2(f2(x291,f2(x291,a1)),f2(a1,a1)),f2(f2(a3,f2(a3,a1)),a1))), % 181.60/182.52 inference(scs_inference,[],[24,21,23,4,5,3])). % 181.60/182.52 cnf(32,plain, % 181.60/182.52 (E(f2(a1,x321),f2(f2(x322,f2(x322,a1)),x321))), % 181.60/182.52 inference(scs_inference,[],[12,4])). % 181.60/182.52 cnf(33,plain, % 181.60/182.52 (E(f2(x331,a1),f2(x331,f2(x332,f2(x332,a1))))), % 181.60/182.52 inference(scs_inference,[],[12,4,5])). % 181.60/182.52 cnf(34,plain, % 181.60/182.52 (~E(f2(f2(a3,f2(a3,a1)),a1),f2(f2(x341,f2(x341,a1)),f2(a1,a1)))), % 181.60/182.52 inference(scs_inference,[],[29,12,4,5,2])). % 181.60/182.52 cnf(35,plain, % 181.60/182.52 (E(f2(f2(a1,x351),x352),f2(f2(f2(x353,f2(x353,a1)),x351),x352))), % 181.60/182.52 inference(scs_inference,[],[32,4])). % 181.60/182.52 cnf(36,plain, % 181.60/182.52 (E(f2(x361,f2(a1,x362)),f2(x361,f2(f2(x363,f2(x363,a1)),x362)))), % 181.60/182.52 inference(scs_inference,[],[32,4,5])). % 181.60/182.52 cnf(37,plain, % 181.60/182.52 (~E(f2(f2(a3,f2(a3,a1)),f2(x371,f2(x371,a1))),f2(f2(x372,f2(x372,a1)),f2(a1,a1)))), % 181.60/182.52 inference(scs_inference,[],[32,33,34,4,5,3])). % 181.60/182.52 cnf(39,plain, % 181.60/182.52 (~E(f2(f2(x391,f2(x391,a1)),f2(a1,a1)),f2(f2(a3,f2(a3,a1)),f2(x392,f2(x392,a1))))), % 181.60/182.52 inference(scs_inference,[],[32,33,34,4,5,3,2])). % 181.60/182.52 cnf(41,plain, % 181.60/182.52 (E(f2(x411,f2(x412,f2(x413,f2(x413,a1)))),f2(x411,f2(x412,a1)))), % 181.60/182.52 inference(scs_inference,[],[19,4,5])). % 181.60/182.52 cnf(42,plain, % 181.60/182.52 (~E(f2(f2(f2(x421,f2(x421,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(a3,f2(a3,a1)),f2(x422,f2(x422,a1))))), % 181.60/182.52 inference(scs_inference,[],[39,35,19,4,5,3])). % 181.60/182.52 cnf(46,plain, % 181.60/182.52 (E(f2(x461,f2(x462,a1)),f2(x461,f2(x462,f2(x463,f2(x463,a1)))))), % 181.60/182.52 inference(scs_inference,[],[33,4,5])). % 181.60/182.52 cnf(47,plain, % 181.60/182.52 (~E(f2(f2(a3,f2(a3,a1)),f2(x471,f2(x471,a1))),f2(f2(f2(x472,f2(x472,a1)),f2(a1,a1)),f2(a1,a1)))), % 181.60/182.52 inference(scs_inference,[],[42,33,4,5,2])). % 181.60/182.52 cnf(48,plain, % 181.60/182.52 (~E(f2(f2(a3,f2(a3,a1)),f2(f2(x481,f2(x481,a1)),f2(a1,a1))),f2(f2(x482,f2(x482,a1)),f2(a1,a1)))), % 181.60/182.52 inference(scs_inference,[],[37,42,36,33,4,5,2,3])). % 181.60/182.52 cnf(51,plain, % 181.60/182.52 (E(f2(x511,x512),f2(f2(f2(x513,f2(f2(f2(x514,x513),x511),f2(x514,a1))),f2(a1,a1)),x512))), % 181.60/182.52 inference(scs_inference,[],[9,4])). % 181.60/182.52 cnf(52,plain, % 181.60/182.52 (E(f2(x521,x522),f2(x521,f2(f2(x523,f2(f2(f2(x524,x523),x522),f2(x524,a1))),f2(a1,a1))))), % 181.60/182.52 inference(scs_inference,[],[9,4,5])). % 181.60/182.52 cnf(53,plain, % 181.60/182.52 (~E(f2(f2(x531,f2(x531,a1)),f2(a1,a1)),f2(f2(a3,f2(a3,a1)),f2(f2(x532,f2(x532,a1)),f2(a1,a1))))), % 181.60/182.52 inference(scs_inference,[],[48,9,4,5,2])). % 181.60/182.52 cnf(54,plain, % 181.60/182.52 (E(f2(x541,f2(x541,f2(x542,f2(x542,a1)))),a1)), % 181.60/182.52 inference(scs_inference,[],[6,41,48,9,4,5,2,3])). % 181.60/182.52 cnf(56,plain, % 181.60/182.52 (E(f2(f2(f2(x561,f2(f2(f2(x562,x561),x563),f2(x562,a1))),f2(a1,a1)),x564),f2(x563,x564))), % 181.60/182.52 inference(scs_inference,[],[7,4])). % 181.60/182.52 cnf(57,plain, % 181.60/182.52 (E(f2(x571,f2(f2(x572,f2(f2(f2(x573,x572),x574),f2(x573,a1))),f2(a1,a1))),f2(x571,x574))), % 181.60/182.52 inference(scs_inference,[],[7,4,5])). % 181.60/182.52 cnf(58,plain, % 181.60/182.52 (E(f2(x581,f2(x581,f2(x582,f2(x582,a1)))),f2(x583,f2(x583,a1)))), % 181.60/182.52 inference(scs_inference,[],[54,12,3])). % 181.60/182.52 cnf(59,plain, % 181.60/182.52 (~E(f2(f2(f2(x591,f2(x591,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(a3,f2(a3,a1)),f2(f2(x592,f2(x592,a1)),f2(a1,a1))))), % 181.60/182.52 inference(scs_inference,[],[53,35,3])). % 181.60/182.52 cnf(62,plain, % 181.60/182.52 (~E(f2(f2(a3,f2(a3,a1)),f2(f2(x621,f2(x621,a1)),f2(a1,a1))),f2(f2(f2(x622,f2(x622,a1)),f2(a1,a1)),f2(a1,a1)))), % 181.60/182.52 inference(scs_inference,[],[59,2])). % 181.60/182.52 cnf(63,plain, % 181.60/182.52 (~E(f2(a1,a1),f2(f2(f2(x631,f2(x631,a1)),f2(a1,a1)),f2(a1,a1)))), % 181.60/182.52 inference(scs_inference,[],[47,24,3])). % 181.60/182.52 cnf(88,plain, % 181.60/182.52 (~E(f2(a1,f2(f2(x881,f2(x881,a1)),f2(a1,a1))),f2(f2(f2(x882,f2(x882,a1)),f2(a1,a1)),f2(a1,a1)))), % 181.60/182.52 inference(scs_inference,[],[18,62,3])). % 181.60/182.52 cnf(91,plain, % 181.60/182.52 (~E(f2(a1,f2(a1,f2(a1,a1))),f2(f2(f2(x911,f2(x911,a1)),f2(a1,a1)),f2(a1,a1)))), % 181.60/182.52 inference(scs_inference,[],[88,23,3])). % 181.60/182.52 cnf(94,plain, % 181.60/182.52 (~E(f2(a1,a1),a1)), % 181.60/182.52 inference(scs_inference,[],[18,91,8,2,3])). % 181.60/182.52 cnf(96,plain, % 181.60/182.52 (~E(a1,f2(a1,a1))), % 181.60/182.52 inference(scs_inference,[],[94,2])). % 181.60/182.52 cnf(97,plain, % 181.60/182.52 (~E(f2(f2(f2(x971,f2(f2(f2(x972,x971),a1),f2(x972,a1))),f2(a1,a1)),a1),a1)), % 181.60/182.52 inference(scs_inference,[],[94,51,2,3])). % 181.60/182.52 cnf(99,plain, % 181.60/182.52 (~E(a1,f2(f2(f2(x991,f2(f2(f2(x992,x991),a1),f2(x992,a1))),f2(a1,a1)),a1))), % 181.60/182.52 inference(scs_inference,[],[97,2])). % 181.60/182.52 cnf(100,plain, % 181.60/182.52 (~E(f2(f2(x1001,f2(f2(f2(x1002,x1001),a1),f2(x1002,a1))),f2(a1,a1)),f2(a1,a1))), % 181.60/182.52 inference(scs_inference,[],[96,97,9,2,3])). % 181.60/182.52 cnf(102,plain, % 181.60/182.52 (~E(f2(a1,a1),f2(f2(x1021,f2(f2(f2(x1022,x1021),a1),f2(x1022,a1))),f2(a1,a1)))), % 181.60/182.52 inference(scs_inference,[],[100,2])). % 181.60/182.52 cnf(103,plain, % 181.60/182.52 (~E(f2(x1031,f2(x1031,a1)),f2(a1,a1))), % 181.60/182.52 inference(scs_inference,[],[100,15,2,3])). % 181.60/182.52 cnf(105,plain, % 181.60/182.52 (~E(f2(a1,a1),f2(x1051,f2(x1051,a1)))), % 181.60/182.52 inference(scs_inference,[],[103,2])). % 181.60/182.52 cnf(106,plain, % 181.60/182.52 (~E(f2(a1,f2(f2(x1061,f2(x1061,a1)),a1)),f2(a1,a1))), % 181.60/182.52 inference(scs_inference,[],[18,103,2,3])). % 181.60/182.52 cnf(110,plain, % 181.60/182.52 (~E(f2(a1,f2(f2(x1101,f2(f2(f2(x1102,x1101),a1),f2(x1102,a1))),f2(a1,a1))),f2(x1103,f2(x1103,a1)))), % 181.60/182.52 inference(scs_inference,[],[105,106,52,2,3])). % 181.60/182.52 cnf(113,plain, % 181.60/182.52 (~E(f2(x1131,f2(x1131,a1)),f2(f2(f2(x1132,f2(f2(f2(x1133,x1132),a1),f2(x1133,a1))),f2(a1,a1)),a1))), % 181.60/182.52 inference(scs_inference,[],[99,110,12,2,3])). % 181.60/182.52 cnf(115,plain, % 181.60/182.52 (~E(f2(a1,f2(x1151,f2(x1151,a1))),f2(f2(f2(x1152,f2(x1152,a1)),f2(a1,a1)),f2(a1,a1)))), % 181.60/182.52 inference(scs_inference,[],[63,113,33,2,3])). % 181.60/182.52 cnf(117,plain, % 181.60/182.52 (~E(f2(f2(f2(x1171,f2(x1171,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,f2(x1172,f2(x1172,a1))))), % 181.60/182.52 inference(scs_inference,[],[115,2])). % 181.60/182.52 cnf(118,plain, % 181.60/182.52 (~E(f2(a1,a1),f2(f2(x1181,f2(x1181,a1)),f2(a1,a1)))), % 181.60/182.52 inference(scs_inference,[],[18,115,34,2,3])). % 181.60/182.52 cnf(120,plain, % 181.60/182.52 (~E(f2(f2(x1201,f2(x1201,a1)),f2(a1,a1)),f2(a1,a1))), % 181.60/182.52 inference(scs_inference,[],[118,2])). % 181.60/182.52 cnf(121,plain, % 181.60/182.52 (~E(f2(f2(x1211,f2(x1211,a1)),a1),f2(f2(x1212,f2(x1212,a1)),f2(a1,a1)))), % 181.60/182.52 inference(scs_inference,[],[118,32,2,3])). % 181.60/182.52 cnf(123,plain, % 181.60/182.52 (~E(f2(f2(x1231,f2(x1231,a1)),f2(a1,a1)),f2(f2(x1232,f2(x1232,a1)),a1))), % 181.60/182.52 inference(scs_inference,[],[121,2])). % 181.60/182.52 cnf(124,plain, % 181.60/182.52 (~E(f2(f2(x1241,f2(x1241,a1)),f2(f2(x1242,f2(x1242,a1)),a1)),f2(a1,a1))), % 181.60/182.52 inference(scs_inference,[],[120,121,36,2,3])). % 181.60/182.52 cnf(127,plain, % 181.60/182.52 (~E(f2(f2(x1271,f2(x1271,a1)),a1),f2(f2(x1272,f2(f2(f2(x1273,x1272),a1),f2(x1273,a1))),f2(a1,a1)))), % 181.60/182.52 inference(scs_inference,[],[102,124,32,2,3])). % 181.60/182.52 cnf(129,plain, % 181.60/182.52 (~E(f2(f2(x1291,f2(f2(f2(x1292,x1291),a1),f2(x1292,a1))),f2(a1,a1)),f2(f2(x1293,f2(x1293,a1)),a1))), % 181.60/182.52 inference(scs_inference,[],[127,2])). % 181.60/182.52 cnf(130,plain, % 181.60/182.52 (~E(f2(f2(x1301,f2(x1301,a1)),f2(a1,f2(x1302,f2(x1302,a1)))),f2(a1,a1))), % 181.60/182.52 inference(scs_inference,[],[127,120,46,2,3])). % 181.60/182.52 cnf(133,plain, % 181.60/182.52 (~E(f2(x1331,f2(x1331,a1)),f2(f2(x1332,f2(x1332,a1)),a1))), % 181.60/182.52 inference(scs_inference,[],[130,129,15,2,3])). % 181.60/182.52 cnf(135,plain, % 181.60/182.52 (~E(f2(f2(x1351,f2(x1351,a1)),a1),f2(x1352,f2(x1352,a1)))), % 181.60/182.52 inference(scs_inference,[],[133,2])). % 181.60/182.52 cnf(136,plain, % 181.60/182.52 (~E(f2(f2(a1,f2(a1,a1)),f2(a1,a1)),f2(a1,f2(x1361,f2(x1361,a1))))), % 181.60/182.52 inference(scs_inference,[],[22,133,117,2,3])). % 181.60/182.52 cnf(140,plain, % 181.60/182.52 (E(f2(x1401,f2(x1401,f2(x1402,f2(x1402,a1)))),f2(f2(x1403,f2(x1403,a1)),f2(a1,a1)))), % 181.60/182.52 inference(scs_inference,[],[23,136,58,2,3])). % 181.60/182.52 cnf(192,plain, % 181.60/182.52 (~E(f2(x1921,f2(x1921,a1)),f2(a1,f2(x1922,f2(x1922,a1))))), % 181.60/182.52 inference(scs_inference,[],[33,105,3,2])). % 181.60/182.52 cnf(193,plain, % 181.60/182.52 (~E(f2(f2(x1931,f2(f2(f2(x1932,x1931),a1),f2(x1932,a1))),f2(a1,a1)),f2(a1,f2(x1933,f2(x1933,a1))))), % 181.60/182.52 inference(scs_inference,[],[192,13,3])). % 181.60/182.52 cnf(205,plain, % 181.60/182.52 (~E(f2(x2051,f2(x2051,a1)),f2(f2(x2052,f2(x2052,a1)),f2(x2053,f2(x2053,a1))))), % 181.60/182.52 inference(scs_inference,[],[33,135,3,2])). % 181.60/182.52 cnf(208,plain, % 181.60/182.52 (~E(f2(a1,f2(x2081,f2(x2081,a1))),a1)), % 181.60/182.52 inference(scs_inference,[],[193,7,3,2])). % 181.60/182.52 cnf(212,plain, % 181.60/182.52 (~E(f2(f2(f2(x2121,f2(f2(f2(x2122,x2121),a1),f2(x2122,a1))),f2(a1,a1)),f2(x2123,f2(x2123,a1))),a1)), % 181.60/182.52 inference(scs_inference,[],[208,51,3])). % 181.60/182.53 cnf(215,plain, % 181.60/182.53 (~E(f2(a1,f2(x2151,f2(x2151,a1))),f2(f2(x2152,f2(x2152,a1)),f2(a1,a1)))), % 181.60/182.53 inference(scs_inference,[],[33,212,118,2,3])). % 181.60/182.53 cnf(217,plain, % 181.60/182.53 (~E(f2(f2(x2171,f2(x2171,a1)),f2(a1,a1)),f2(a1,f2(x2172,f2(x2172,a1))))), % 181.60/182.53 inference(scs_inference,[],[215,2])). % 181.60/182.53 cnf(234,plain, % 181.60/182.53 (~E(f2(f2(x2341,f2(f2(f2(x2342,x2341),f2(a1,a1)),f2(x2342,a1))),f2(a1,a1)),f2(f2(f2(x2343,f2(x2343,a1)),f2(a1,a1)),f2(a1,a1)))), % 181.60/182.53 inference(scs_inference,[],[63,9,3])). % 181.60/182.53 cnf(256,plain, % 181.60/182.53 (~E(f2(x2561,f2(x2561,a1)),f2(f2(x2562,f2(f2(f2(x2563,x2562),f2(a1,a1)),f2(x2563,a1))),f2(a1,a1)))), % 181.60/182.53 inference(scs_inference,[],[105,9,3,2])). % 181.60/182.53 cnf(275,plain, % 181.60/182.53 (~E(f2(f2(x2751,f2(f2(f2(x2752,x2751),f2(a1,a1)),f2(x2752,a1))),f2(a1,a1)),f2(f2(x2753,f2(x2753,a1)),f2(a1,a1)))), % 181.60/182.53 inference(scs_inference,[],[118,9,3])). % 181.60/182.53 cnf(327,plain, % 181.60/182.53 (~E(f2(f2(f2(x3271,f2(x3271,a1)),f2(f2(f2(x3272,a1),f2(a1,a1)),f2(x3272,a1))),f2(a1,a1)),f2(f2(x3273,f2(x3273,a1)),f2(a1,a1)))), % 181.60/182.53 inference(scs_inference,[],[275,35,3])). % 181.60/182.53 cnf(338,plain, % 181.60/182.53 (~E(f2(x3381,f2(x3381,f2(x3382,f2(x3382,a1)))),f2(a1,a1))), % 181.60/182.53 inference(scs_inference,[],[46,103,3])). % 181.60/182.53 cnf(356,plain, % 181.60/182.53 (E(f2(f2(f2(f2(x3561,f2(f2(f2(x3562,x3561),x3563),f2(x3562,a1))),f2(a1,a1)),x3564),x3565),f2(f2(x3563,x3564),x3565))), % 181.60/182.53 inference(scs_inference,[],[56,4])). % 181.60/182.53 cnf(357,plain, % 181.60/182.53 (E(f2(x3571,f2(f2(f2(x3572,f2(f2(f2(x3573,x3572),x3574),f2(x3573,a1))),f2(a1,a1)),x3575)),f2(x3571,f2(x3574,x3575)))), % 181.60/182.53 inference(scs_inference,[],[56,4,5])). % 181.60/182.53 cnf(358,plain, % 181.60/182.53 (~E(f2(f2(a1,a1),f2(f2(f2(x3581,f2(x3581,a1)),f2(x3582,f2(x3582,a1))),a1)),f2(f2(x3583,f2(x3583,a1)),f2(x3584,f2(x3584,a1))))), % 181.60/182.53 inference(scs_inference,[],[205,56,27,4,5,3])). % 181.60/182.53 cnf(361,plain, % 181.60/182.53 (E(f2(f2(x3611,f2(f2(x3612,f2(f2(f2(x3613,x3612),x3614),f2(x3613,a1))),f2(a1,a1))),x3615),f2(f2(x3611,x3614),x3615))), % 181.60/182.53 inference(scs_inference,[],[57,4])). % 181.60/182.53 cnf(364,plain, % 181.60/182.53 (~E(f2(f2(x3641,f2(f2(f2(x3642,f2(f2(f2(x3643,x3642),x3641),f2(x3643,a1))),f2(a1,a1)),a1)),f2(a1,a1)),f2(f2(x3644,f2(x3644,a1)),a1))), % 181.60/182.53 inference(scs_inference,[],[123,57,356,358,4,5,2,3])). % 181.60/182.53 cnf(367,plain, % 181.60/182.53 (E(f2(f2(x3671,f2(x3671,f2(x3672,f2(x3672,a1)))),x3673),f2(f2(f2(x3674,f2(x3674,a1)),f2(a1,a1)),x3673))), % 181.60/182.53 inference(scs_inference,[],[140,4])). % 181.60/182.53 cnf(368,plain, % 181.60/182.53 (E(f2(x3681,f2(x3682,f2(x3682,f2(x3683,f2(x3683,a1))))),f2(x3681,f2(f2(x3684,f2(x3684,a1)),f2(a1,a1))))), % 181.60/182.53 inference(scs_inference,[],[140,4,5])). % 181.60/182.53 cnf(370,plain, % 181.60/182.53 (~E(f2(f2(f2(x3701,f2(f2(f2(x3702,x3701),x3703),f2(x3702,a1))),f2(a1,a1)),f2(x3703,f2(x3704,f2(x3704,a1)))),f2(a1,a1))), % 181.60/182.53 inference(scs_inference,[],[338,140,357,364,4,5,2,3])). % 181.60/182.53 cnf(376,plain, % 181.60/182.53 (~E(f2(f2(x3761,f2(f2(f2(x3762,f2(f2(f2(x3763,x3762),x3761),f2(x3763,a1))),f2(a1,a1)),a1)),f2(a1,a1)),f2(a1,f2(x3764,f2(x3764,a1))))), % 181.60/182.53 inference(scs_inference,[],[217,28,370,356,4,5,2,3])). % 181.60/182.53 cnf(382,plain, % 181.60/182.53 (~E(f2(f2(x3821,f2(f2(f2(x3822,x3821),a1),f2(x3822,a1))),f2(a1,a1)),f2(f2(x3823,f2(f2(f2(x3824,x3823),f2(a1,a1)),f2(x3824,a1))),f2(a1,a1)))), % 181.60/182.53 inference(scs_inference,[],[256,376,13,4,5,2,3])). % 181.60/182.53 cnf(422,plain, % 181.60/182.53 (E(f2(f2(x4221,f2(f2(x4222,f2(x4222,a1)),x4223)),x4224),f2(f2(x4221,f2(a1,x4223)),x4224))), % 181.60/182.53 inference(scs_inference,[],[23,4])). % 181.60/182.53 cnf(443,plain, % 181.60/182.53 (E(f2(f2(x4431,x4432),x4433),f2(f2(f2(f2(x4434,f2(f2(f2(x4435,x4434),x4431),f2(x4435,a1))),f2(a1,a1)),x4432),x4433))), % 181.60/182.53 inference(scs_inference,[],[51,4])). % 181.60/182.53 cnf(444,plain, % 181.60/182.53 (E(f2(x4441,f2(x4442,x4443)),f2(x4441,f2(f2(f2(x4444,f2(f2(f2(x4445,x4444),x4442),f2(x4445,a1))),f2(a1,a1)),x4443)))), % 181.60/182.53 inference(scs_inference,[],[51,4,5])). % 181.60/182.53 cnf(479,plain, % 181.60/182.53 (~E(f2(x4791,f2(f2(f2(x4792,x4791),a1),f2(x4792,a1))),f2(x4793,f2(f2(f2(x4794,x4793),f2(a1,a1)),f2(x4794,a1))))), % 181.60/182.53 inference(scs_inference,[],[382,4])). % 181.60/182.53 cnf(480,plain, % 181.60/182.53 (E(f2(x4801,f2(x4801,a1)),f2(x4802,f2(x4802,f2(x4803,f2(x4803,a1)))))), % 181.60/182.53 inference(scs_inference,[],[58,382,4,2])). % 181.60/182.53 cnf(492,plain, % 181.60/182.53 (~E(f2(x4921,f2(f2(f2(x4922,x4921),f2(a1,a1)),f2(x4922,a1))),f2(x4923,f2(x4923,a1)))), % 181.60/182.53 inference(scs_inference,[],[275,4])). % 181.60/182.53 cnf(501,plain, % 181.60/182.53 (E(f2(x5011,f2(a1,a1)),f2(x5011,f2(f2(x5012,f2(x5012,a1)),f2(x5013,f2(x5013,a1)))))), % 181.60/182.53 inference(scs_inference,[],[28,327,492,4,5,2])). % 181.60/182.53 cnf(512,plain, % 181.60/182.53 (~E(f2(f2(f2(x5121,x5122),a1),f2(x5121,a1)),f2(f2(f2(x5123,x5122),f2(a1,a1)),f2(x5123,a1)))), % 181.60/182.53 inference(scs_inference,[],[234,479,4,5])). % 181.60/182.53 cnf(542,plain, % 181.60/182.53 (~E(f2(f2(x5421,x5422),a1),f2(f2(x5421,x5422),f2(a1,a1)))), % 181.60/182.53 inference(scs_inference,[],[512,4])). % 181.60/182.53 cnf(561,plain, % 181.60/182.53 (E(f2(f2(x5611,f2(f2(f2(x5612,x5611),f2(x5613,f2(a1,a1))),f2(x5612,a1))),f2(a1,a1)),f2(x5613,f2(f2(x5614,f2(x5614,a1)),f2(x5615,f2(x5615,a1)))))), % 181.60/182.53 inference(scs_inference,[],[7,367,501,2,3])). % 181.60/182.53 cnf(564,plain, % 181.60/182.53 (E(f2(f2(x5641,f2(f2(f2(x5642,x5641),f2(x5643,f2(x5643,a1))),f2(x5642,a1))),f2(a1,a1)),f2(x5644,f2(x5644,f2(x5645,f2(x5645,a1)))))), % 181.60/182.53 inference(scs_inference,[],[7,368,480,2,3])). % 181.60/182.53 cnf(608,plain, % 181.60/182.53 (E(x6081,f2(f2(f2(f2(x6082,f2(f2(f2(x6083,x6082),x6084),f2(x6083,a1))),f2(a1,a1)),f2(f2(f2(x6085,x6084),x6081),f2(x6085,a1))),f2(a1,a1)))), % 181.60/182.53 inference(scs_inference,[],[9,443,564,2,3])). % 181.60/182.53 cnf(611,plain, % 181.60/182.53 (E(x6111,f2(f2(x6112,f2(f2(f2(x6113,x6112),x6111),f2(x6113,a1))),f2(f2(f2(x6114,f2(f2(f2(x6115,x6114),a1),f2(x6115,a1))),f2(a1,a1)),a1)))), % 181.60/182.53 inference(scs_inference,[],[9,444,608,2,3])). % 181.60/182.53 cnf(617,plain, % 181.60/182.53 (E(f2(f2(f2(x6171,f2(a1,x6172)),x6173),f2(x6171,a1)),f2(f2(x6172,x6173),f2(a1,a1)))), % 181.60/182.53 inference(scs_inference,[],[9,361,561,2,3])). % 181.60/182.53 cnf(620,plain, % 181.60/182.53 (E(f2(f2(x6201,x6202),f2(a1,a1)),f2(f2(f2(x6203,f2(a1,x6201)),x6202),f2(x6203,a1)))), % 181.60/182.53 inference(scs_inference,[],[617,2])). % 181.60/182.53 cnf(634,plain, % 181.60/182.53 (E(x6341,f2(f2(f2(x6342,f2(a1,x6343)),f2(f2(f2(x6344,x6343),x6341),f2(x6344,a1))),f2(x6342,a1)))), % 181.60/182.53 inference(scs_inference,[],[9,620,611,2,3])). % 181.60/182.53 cnf(637,plain, % 181.60/182.53 (E(f2(f2(x6371,x6372),a1),f2(f2(x6372,f2(a1,f2(x6371,a1))),f2(a1,a1)))), % 181.60/182.53 inference(scs_inference,[],[9,634,422,2,3])). % 181.60/182.53 cnf(1594,plain, % 181.60/182.53 ($false), % 181.60/182.53 inference(scs_inference,[],[542,637,617,3]), % 181.60/182.53 ['proof']). % 181.60/182.53 % SZS output end Proof % 181.60/182.53 % Total time :180.880000s %------------------------------------------------------------------------------