%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP537-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 : n028.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:53 EDT 2024 % Result : Unsatisfiable 204.39s 204.50s % Output : CNFRefutation 204.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : GRP537-1 : TPTP v8.2.0. Released v2.6.0. % 0.12/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.32 % Computer : n028.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 12:18:08 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.55 start to proof:theBenchmark % 204.37/204.47 %------------------------------------------- % 204.37/204.47 % File :CSE---1.7 % 204.37/204.47 % Problem :theBenchmark % 204.37/204.47 % Transform :cnf % 204.37/204.47 % Format :tptp:raw % 204.37/204.47 % Command :java -jar mcs_scs.jar %d %s % 204.37/204.47 % 204.37/204.47 % Result :Theorem 203.760000s % 204.37/204.47 % Output :CNFRefutation 203.760000s % 204.37/204.47 %------------------------------------------- % 204.39/204.50 %-------------------------------------------------------------------------- % 204.39/204.50 % File : GRP537-1 : TPTP v8.2.0. Released v2.6.0. % 204.39/204.50 % Domain : Group Theory (Abelian) % 204.39/204.50 % Problem : Axiom for Abelian group theory, in division, part 1 % 204.39/204.50 % Version : [McC93] (equality) axioms. % 204.39/204.50 % English : % 204.39/204.50 % 204.39/204.50 % Refs : [McC93] McCune (1993), Single Axioms for Groups and Abelian Gr % 204.39/204.50 % Source : [TPTP] % 204.39/204.50 % Names : % 204.39/204.50 % 204.39/204.50 % Status : Unsatisfiable % 204.39/204.50 % Rating : 0.00 v7.4.0, 0.04 v7.3.0, 0.00 v6.4.0, 0.05 v6.3.0, 0.12 v6.2.0, 0.14 v6.1.0, 0.00 v6.0.0, 0.05 v5.4.0, 0.00 v2.6.0 % 204.39/204.50 % Syntax : Number of clauses : 5 ( 5 unt; 0 nHn; 1 RR) % 204.39/204.50 % Number of literals : 5 ( 5 equ; 1 neg) % 204.39/204.50 % Maximal clause size : 1 ( 1 avg) % 204.39/204.50 % Maximal term depth : 4 ( 2 avg) % 204.39/204.50 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 204.39/204.50 % Number of functors : 6 ( 6 usr; 3 con; 0-2 aty) % 204.39/204.50 % Number of variables : 9 ( 0 sgn) % 204.39/204.50 % SPC : CNF_UNS_RFO_PEQ_UEQ % 204.39/204.50 % 204.39/204.50 % Comments : A UEQ part of GRP092-1 % 204.39/204.50 %-------------------------------------------------------------------------- % 204.39/204.50 cnf(single_axiom,axiom, % 204.39/204.50 divide(divide(A,B),divide(divide(A,C),B)) = C ). % 204.39/204.50 % 204.39/204.50 cnf(multiply,axiom, % 204.39/204.50 multiply(A,B) = divide(A,divide(divide(C,C),B)) ). % 204.39/204.50 % 204.39/204.50 cnf(inverse,axiom, % 204.39/204.50 inverse(A) = divide(divide(B,B),A) ). % 204.39/204.50 % 204.39/204.50 cnf(identity,axiom, % 204.39/204.50 identity = divide(A,A) ). % 204.39/204.50 % 204.39/204.50 cnf(prove_these_axioms_1,negated_conjecture, % 204.39/204.50 multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ). % 204.39/204.50 % 204.39/204.50 %-------------------------------------------------------------------------- % 204.39/204.50 %------------------------------------------- % 204.39/204.50 % Proof found % 204.39/204.50 % SZS status Theorem for theBenchmark % 204.39/204.50 % SZS output start Proof % 204.43/204.52 %ClaNum:13(EqnAxiom:8) % 204.43/204.52 %VarNum:18(SingletonVarNum:9) % 204.43/204.52 %MaxLitNum:1 % 204.43/204.52 %MaxfuncDepth:3 % 204.43/204.52 %SharedTerms:8 % 204.43/204.52 %goalClause: 13 % 204.43/204.52 %singleGoalClaCount:1 % 204.43/204.52 [13]~E(f6(f5(a2),a2),f6(f5(a3),a3)) % 204.43/204.52 [9]E(f1(x91,x91),a4) % 204.43/204.52 [10]E(f1(f1(x101,x101),x102),f5(x102)) % 204.43/204.52 [11]E(f1(x111,f1(f1(x112,x112),x113)),f6(x111,x113)) % 204.43/204.52 [12]E(f1(f1(x121,x122),f1(f1(x121,x123),x122)),x123) % 204.43/204.52 %EqnAxiom % 204.43/204.52 [1]E(x11,x11) % 204.43/204.52 [2]E(x22,x21)+~E(x21,x22) % 204.43/204.52 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 204.43/204.52 [4]~E(x41,x42)+E(f1(x41,x43),f1(x42,x43)) % 204.43/204.52 [5]~E(x51,x52)+E(f1(x53,x51),f1(x53,x52)) % 204.43/204.52 [6]~E(x61,x62)+E(f6(x61,x63),f6(x62,x63)) % 204.43/204.52 [7]~E(x71,x72)+E(f6(x73,x71),f6(x73,x72)) % 204.43/204.52 [8]~E(x81,x82)+E(f5(x81),f5(x82)) % 204.43/204.52 % 204.43/204.52 %------------------------------------------- % 204.46/204.54 cnf(14,plain, % 204.46/204.54 (E(a4,f1(x141,x141))), % 204.46/204.54 inference(scs_inference,[],[9,2])). % 204.46/204.54 cnf(15,plain, % 204.46/204.54 (~E(f6(f5(a2),a2),f1(f5(a3),f1(f1(x151,x151),a3)))), % 204.46/204.54 inference(scs_inference,[],[13,9,11,2,3])). % 204.46/204.54 cnf(17,plain, % 204.46/204.54 (E(f5(x171),f1(f1(x172,x172),x171))), % 204.46/204.54 inference(scs_inference,[],[10,2])). % 204.46/204.54 cnf(18,plain, % 204.46/204.54 (E(f1(f1(x181,x182),f1(f1(x181,a4),x182)),f1(x183,x183))), % 204.46/204.54 inference(scs_inference,[],[14,10,12,2,3])). % 204.46/204.54 cnf(20,plain, % 204.46/204.54 (E(f1(x201,x201),f1(f1(x202,x203),f1(f1(x202,a4),x203)))), % 204.46/204.54 inference(scs_inference,[],[18,2])). % 204.46/204.54 cnf(21,plain, % 204.46/204.54 (E(f1(f1(x211,x211),x212),f1(f1(x213,x213),x212))), % 204.46/204.54 inference(scs_inference,[],[17,18,10,2,3])). % 204.46/204.54 cnf(23,plain, % 204.46/204.54 (E(f6(x231,x232),f1(x231,f1(f1(x233,x233),x232)))), % 204.46/204.54 inference(scs_inference,[],[11,2])). % 204.46/204.54 cnf(24,plain, % 204.46/204.54 (E(f5(f1(x241,x241)),f1(f1(x242,x243),f1(f1(x242,a4),x243)))), % 204.46/204.54 inference(scs_inference,[],[20,17,11,2,3])). % 204.46/204.54 cnf(27,plain, % 204.46/204.54 (E(f1(f1(x271,x272),f1(f1(x271,a4),x272)),f5(f1(x273,x273)))), % 204.46/204.54 inference(scs_inference,[],[24,2])). % 204.46/204.54 cnf(29,plain, % 204.46/204.54 (E(x291,f1(f1(x292,x293),f1(f1(x292,x291),x293)))), % 204.46/204.54 inference(scs_inference,[],[12,2])). % 204.46/204.54 cnf(30,plain, % 204.46/204.54 (E(f6(f1(a4,x301),x301),f5(f1(x302,x302)))), % 204.46/204.54 inference(scs_inference,[],[23,27,12,2,3])). % 204.46/204.54 cnf(33,plain, % 204.46/204.54 (E(f5(f1(x331,x331)),f6(f1(a4,x332),x332))), % 204.46/204.54 inference(scs_inference,[],[30,2])). % 204.46/204.54 cnf(34,plain, % 204.46/204.54 (E(a4,f5(f1(x341,x341)))), % 204.46/204.54 inference(scs_inference,[],[29,27,30,2,3])). % 204.46/204.54 cnf(37,plain, % 204.46/204.54 (E(f5(f1(x371,x371)),a4)), % 204.46/204.54 inference(scs_inference,[],[34,2])). % 204.46/204.54 cnf(38,plain, % 204.46/204.54 (E(f1(f1(x381,x382),f1(f1(x381,a4),x382)),f6(f1(a4,x383),x383))), % 204.46/204.54 inference(scs_inference,[],[33,27,34,2,3])). % 204.46/204.54 cnf(40,plain, % 204.46/204.54 (E(f6(f1(a4,x401),x401),f1(f1(x402,x403),f1(f1(x402,a4),x403)))), % 204.46/204.54 inference(scs_inference,[],[38,2])). % 204.46/204.54 cnf(41,plain, % 204.46/204.54 (E(f1(f1(x411,x412),f1(f1(x411,a4),x412)),f1(f1(x413,x413),f1(x414,x414)))), % 204.46/204.54 inference(scs_inference,[],[17,27,38,2,3])). % 204.46/204.54 cnf(43,plain, % 204.46/204.54 (E(f1(f1(x431,x431),f1(x432,x432)),f1(f1(x433,x434),f1(f1(x433,a4),x434)))), % 204.46/204.54 inference(scs_inference,[],[41,2])). % 204.46/204.54 cnf(44,plain, % 204.46/204.54 (E(f5(f1(x441,x441)),f1(x442,x442))), % 204.46/204.54 inference(scs_inference,[],[37,14,41,2,3])). % 204.46/204.54 cnf(45,plain, % 204.46/204.54 (E(f1(x451,x451),f5(f1(x452,x452)))), % 204.46/204.54 inference(scs_inference,[],[44,2])). % 204.46/204.54 cnf(46,plain, % 204.46/204.54 (E(f6(f1(x461,x461),f1(x462,x462)),f1(f1(x463,x464),f1(f1(x463,a4),x464)))), % 204.46/204.54 inference(scs_inference,[],[43,23,44,2,3])). % 204.46/204.54 cnf(49,plain, % 204.46/204.54 (E(f1(f1(x491,x492),f1(f1(x491,a4),x492)),f6(f1(x493,x493),f1(x494,x494)))), % 204.46/204.54 inference(scs_inference,[],[46,2])). % 204.46/204.55 cnf(50,plain, % 204.46/204.55 (E(f6(f1(f1(x501,x501),x502),x502),f5(f1(x503,x503)))), % 204.46/204.55 inference(scs_inference,[],[45,23,46,2,3])). % 204.46/204.55 cnf(53,plain, % 204.46/204.55 (E(f5(f1(x531,x531)),f6(f1(f1(x532,x532),x533),x533))), % 204.46/204.55 inference(scs_inference,[],[50,2])). % 204.46/204.55 cnf(54,plain, % 204.46/204.55 (E(f6(f1(a4,x541),x541),f6(f1(x542,x542),f1(x543,x543)))), % 204.46/204.55 inference(scs_inference,[],[49,40,50,2,3])). % 204.46/204.55 cnf(57,plain, % 204.46/204.55 (E(f1(x571,x571),f6(f1(f1(x572,x572),x573),x573))), % 204.46/204.55 inference(scs_inference,[],[53,45,54,2,3])). % 204.46/204.55 cnf(59,plain, % 204.46/204.55 (E(f6(f1(f1(x591,x591),x592),x592),f1(x593,x593))), % 204.46/204.55 inference(scs_inference,[],[57,2])). % 204.46/204.55 cnf(60,plain, % 204.46/204.55 (E(a4,f6(f1(x601,x601),f1(x602,x602)))), % 204.46/204.55 inference(scs_inference,[],[29,49,57,2,3])). % 204.46/204.55 cnf(63,plain, % 204.46/204.55 (E(f6(f1(x631,x631),f1(x632,x632)),a4)), % 204.46/204.55 inference(scs_inference,[],[60,2])). % 204.46/204.55 cnf(64,plain, % 204.46/204.55 (E(f1(x641,x641),f6(f1(a4,x642),x642))), % 204.46/204.55 inference(scs_inference,[],[33,45,60,2,3])). % 204.46/204.55 cnf(66,plain, % 204.46/204.55 (E(f6(f1(a4,x661),x661),f1(x662,x662))), % 204.46/204.55 inference(scs_inference,[],[64,2])). % 204.46/204.55 cnf(67,plain, % 204.46/204.55 (E(f1(x671,x671),f6(f1(x672,x672),f1(x673,x673)))), % 204.46/204.55 inference(scs_inference,[],[20,49,64,2,3])). % 204.46/204.55 cnf(69,plain, % 204.46/204.55 (E(f6(f1(x691,x691),f1(x692,x692)),f1(x693,x693))), % 204.46/204.55 inference(scs_inference,[],[67,2])). % 204.46/204.55 cnf(70,plain, % 204.46/204.55 (E(f1(x701,x701),f1(f1(x702,x702),f1(x703,x703)))), % 204.46/204.55 inference(scs_inference,[],[17,45,67,2,3])). % 204.46/204.55 cnf(72,plain, % 204.46/204.55 (E(f1(f1(x721,x721),f1(x722,x722)),f1(x723,x723))), % 204.46/204.55 inference(scs_inference,[],[70,2])). % 204.46/204.55 cnf(73,plain, % 204.46/204.55 (E(f1(f1(x731,x731),f1(x732,x732)),f6(f1(x733,x733),f1(x734,x734)))), % 204.46/204.55 inference(scs_inference,[],[43,49,70,2,3])). % 204.46/204.55 cnf(75,plain, % 204.46/204.55 (E(f6(f1(x751,x751),f1(x752,x752)),f1(f1(x753,x753),f1(x754,x754)))), % 204.46/204.55 inference(scs_inference,[],[73,2])). % 204.46/204.55 cnf(76,plain, % 204.46/204.55 (E(f6(f1(f1(x761,x761),x762),x762),f6(f1(x763,x763),f1(x764,x764)))), % 204.46/204.55 inference(scs_inference,[],[59,73,2,3])). % 204.46/204.55 cnf(79,plain, % 204.46/204.55 (E(f6(f1(x791,x791),f1(x792,x792)),f6(f1(f1(x793,x793),x794),x794))), % 204.46/204.55 inference(scs_inference,[],[76,2])). % 204.46/204.55 cnf(80,plain, % 204.46/204.55 (E(f5(f1(x801,x801)),f1(f1(x802,x802),f1(x803,x803)))), % 204.46/204.55 inference(scs_inference,[],[75,53,76,2,3])). % 204.46/204.55 cnf(83,plain, % 204.46/204.55 (E(f1(f1(x831,x831),f1(x832,x832)),f5(f1(x833,x833)))), % 204.46/204.55 inference(scs_inference,[],[80,2])). % 204.46/204.55 cnf(84,plain, % 204.46/204.55 (E(f6(f1(x841,x841),f1(x842,x842)),f5(f1(x843,x843)))), % 204.46/204.55 inference(scs_inference,[],[69,45,80,2,3])). % 204.46/204.55 cnf(86,plain, % 204.46/204.55 (E(f5(f1(x861,x861)),f6(f1(x862,x862),f1(x863,x863)))), % 204.46/204.55 inference(scs_inference,[],[84,2])). % 204.46/204.55 cnf(87,plain, % 204.46/204.55 (E(f1(f1(x871,x871),f1(x872,x872)),a4)), % 204.46/204.55 inference(scs_inference,[],[83,37,84,2,3])). % 204.46/204.55 cnf(89,plain, % 204.46/204.55 (E(a4,f1(f1(x891,x891),f1(x892,x892)))), % 204.46/204.55 inference(scs_inference,[],[87,2])). % 204.46/204.55 cnf(90,plain, % 204.46/204.55 (E(f1(f1(x901,x901),f1(x902,x902)),f6(f1(f1(x903,x903),x904),x904))), % 204.46/204.55 inference(scs_inference,[],[83,53,87,2,3])). % 204.46/204.55 cnf(92,plain, % 204.46/204.55 (E(f6(f1(f1(x921,x921),x922),x922),f1(f1(x923,x923),f1(x924,x924)))), % 204.46/204.55 inference(scs_inference,[],[90,2])). % 204.46/204.55 cnf(93,plain, % 204.46/204.55 (E(f1(f1(x931,x931),f1(x932,x932)),f6(f1(a4,x933),x933))), % 204.46/204.55 inference(scs_inference,[],[83,33,90,2,3])). % 204.46/204.55 cnf(95,plain, % 204.46/204.55 (E(f6(f1(a4,x951),x951),f1(f1(x952,x952),f1(x953,x953)))), % 204.46/204.55 inference(scs_inference,[],[93,2])). % 204.46/204.55 cnf(96,plain, % 204.46/204.55 (E(f1(f1(x961,x961),f1(x962,x962)),f1(f1(x963,x963),f1(x964,x964)))), % 204.46/204.55 inference(scs_inference,[],[83,17,93,2,3])). % 204.46/204.55 cnf(103,plain, % 204.46/204.55 (E(f6(f1(a4,x1031),x1031),f6(f1(a4,x1032),x1032))), % 204.46/204.55 inference(scs_inference,[],[40,38,3])). % 204.46/204.55 cnf(105,plain, % 204.46/204.55 (E(a4,f6(f1(a4,x1051),x1051))), % 204.46/204.55 inference(scs_inference,[],[29,38,3])). % 204.46/204.55 cnf(108,plain, % 204.46/204.55 (E(f6(f1(a4,x1081),x1081),a4)), % 204.46/204.55 inference(scs_inference,[],[29,38,3,2])). % 204.46/204.55 cnf(109,plain, % 204.46/204.55 (E(f1(f1(a4,x1091),f1(f1(x1092,x1092),x1091)),f1(x1093,x1093))), % 204.46/204.55 inference(scs_inference,[],[11,66,3])). % 204.46/204.55 cnf(113,plain, % 204.46/204.55 (E(f1(f1(a4,x1131),f1(f1(x1132,x1132),x1131)),f1(f1(x1133,x1133),f1(x1134,x1134)))), % 204.46/204.55 inference(scs_inference,[],[11,95,3])). % 204.46/204.55 cnf(119,plain, % 204.46/204.55 (E(a4,f1(f1(x1191,x1191),f1(f1(x1192,x1192),f1(x1193,x1193))))), % 204.46/204.55 inference(scs_inference,[],[11,63,3,2])). % 204.46/204.55 cnf(121,plain, % 204.46/204.55 (E(f1(f1(x1211,x1211),f1(f1(x1212,x1212),f1(x1213,x1213))),f6(f1(a4,x1214),x1214))), % 204.46/204.55 inference(scs_inference,[],[119,108,3,2])). % 204.46/204.55 cnf(122,plain, % 204.46/204.55 (E(f1(f1(f1(x1221,x1221),x1222),f1(f1(x1223,x1223),x1222)),f1(x1224,x1224))), % 204.46/204.55 inference(scs_inference,[],[11,59,3])). % 204.46/204.55 cnf(125,plain, % 204.46/204.55 (E(f1(x1251,x1251),f1(f1(f1(x1252,x1252),x1253),f1(f1(x1254,x1254),x1253)))), % 204.46/204.55 inference(scs_inference,[],[122,2])). % 204.46/204.55 cnf(126,plain, % 204.46/204.55 (E(f1(f1(x1261,x1261),f1(f1(x1262,x1262),f1(x1263,x1263))),f1(x1264,x1264))), % 204.46/204.55 inference(scs_inference,[],[11,69,122,2,3])). % 204.46/204.55 cnf(129,plain, % 204.46/204.55 (E(f1(f1(x1291,x1291),f1(f1(x1292,x1292),f1(x1293,x1293))),f1(f1(x1294,x1294),f1(x1295,x1295)))), % 204.46/204.55 inference(scs_inference,[],[11,75,126,2,3])). % 204.46/204.55 cnf(132,plain, % 204.46/204.55 (E(f6(f1(x1321,x1321),f1(x1322,x1322)),f1(f1(x1323,x1323),f1(f1(x1324,x1324),f1(x1325,x1325))))), % 204.46/204.55 inference(scs_inference,[],[63,119,129,2,3])). % 204.46/204.55 cnf(133,plain, % 204.46/204.55 (E(f1(f1(x1331,x1331),f1(f1(x1332,x1332),f1(x1333,x1333))),f6(f1(x1334,x1334),f1(x1335,x1335)))), % 204.46/204.55 inference(scs_inference,[],[132,2])). % 204.46/204.55 cnf(134,plain, % 204.46/204.55 (E(f1(f1(a4,x1341),f1(f1(x1342,x1342),x1341)),a4)), % 204.46/204.55 inference(scs_inference,[],[11,108,132,2,3])). % 204.46/204.55 cnf(137,plain, % 204.46/204.55 (E(a4,f1(f1(a4,x1371),f1(f1(x1372,x1372),x1371)))), % 204.46/204.55 inference(scs_inference,[],[134,2])). % 204.46/204.55 cnf(138,plain, % 204.46/204.55 (E(f5(f1(x1381,x1381)),f1(f1(x1382,x1382),f1(f1(x1383,x1383),f1(x1384,x1384))))), % 204.46/204.55 inference(scs_inference,[],[37,119,134,2,3])). % 204.46/204.55 cnf(140,plain, % 204.46/204.55 (E(f6(f1(x1401,x1401),f1(x1402,x1402)),f1(f1(a4,x1403),f1(f1(x1404,x1404),x1403)))), % 204.46/204.55 inference(scs_inference,[],[137,63,138,2,3])). % 204.46/204.55 cnf(141,plain, % 204.46/204.55 (E(f1(f1(a4,x1411),f1(f1(x1412,x1412),x1411)),f6(f1(x1413,x1413),f1(x1414,x1414)))), % 204.46/204.55 inference(scs_inference,[],[140,2])). % 204.46/204.55 cnf(142,plain, % 204.46/204.55 (E(f6(f1(a4,x1421),x1421),f1(f1(a4,x1422),f1(f1(x1423,x1423),x1422)))), % 204.46/204.55 inference(scs_inference,[],[137,108,140,2,3])). % 204.46/204.55 cnf(143,plain, % 204.46/204.55 (E(f1(f1(a4,x1431),f1(f1(x1432,x1432),x1431)),f6(f1(a4,x1433),x1433))), % 204.46/204.55 inference(scs_inference,[],[142,2])). % 204.46/204.55 cnf(144,plain, % 204.46/204.55 (E(f5(f1(x1441,x1441)),f1(f1(a4,x1442),f1(f1(x1443,x1443),x1442)))), % 204.46/204.55 inference(scs_inference,[],[137,37,142,2,3])). % 204.46/204.55 cnf(145,plain, % 204.46/204.55 (E(f1(f1(a4,x1451),f1(f1(x1452,x1452),x1451)),f5(f1(x1453,x1453)))), % 204.46/204.55 inference(scs_inference,[],[144,2])). % 204.46/204.55 cnf(148,plain, % 204.46/204.55 (E(f6(f1(f1(x1481,x1481),x1482),x1482),a4)), % 204.46/204.55 inference(scs_inference,[],[14,57,3,2])). % 204.46/204.55 cnf(150,plain, % 204.46/204.55 (E(f6(f1(a4,x1501),x1501),f6(f1(f1(x1502,x1502),x1503),x1503))), % 204.46/204.55 inference(scs_inference,[],[148,105,3,2])). % 204.46/204.55 cnf(154,plain, % 204.46/204.55 (E(f6(f1(x1541,x1541),f1(x1542,x1542)),f5(f1(f1(x1543,x1543),f1(x1544,x1544))))), % 204.46/204.55 inference(scs_inference,[],[17,133,3,2])). % 204.46/204.55 cnf(178,plain, % 204.46/204.55 (E(f5(f1(x1781,x1781)),f5(f1(f1(x1782,a4),x1782)))), % 204.46/204.55 inference(scs_inference,[],[17,27,3,2])). % 204.46/204.55 cnf(182,plain, % 204.46/204.55 (E(f5(f1(f1(x1821,a4),x1821)),f6(f1(x1822,x1822),f1(x1823,x1823)))), % 204.46/204.55 inference(scs_inference,[],[154,178,3,2])). % 204.46/204.55 cnf(195,plain, % 204.46/204.55 (E(f5(f1(f1(x1951,a4),x1951)),f1(x1952,x1952))), % 204.46/204.55 inference(scs_inference,[],[17,18,3])). % 204.46/204.55 cnf(211,plain, % 204.46/204.55 (E(f1(f1(x2111,x2111),f1(f1(x2112,x2112),a4)),f6(f1(x2113,x2113),f1(x2114,x2114)))), % 204.46/204.55 inference(scs_inference,[],[21,141,3])). % 204.46/204.55 cnf(215,plain, % 204.46/204.55 (E(f1(f1(x2151,x2151),f1(f1(x2152,x2152),a4)),f5(f1(x2153,x2153)))), % 204.46/204.55 inference(scs_inference,[],[21,145,211,2,3])). % 204.46/204.55 cnf(219,plain, % 204.46/204.55 (E(f1(f1(x2191,x2191),f1(f1(x2192,x2192),a4)),f6(f1(a4,x2193),x2193))), % 204.46/204.55 inference(scs_inference,[],[21,143,215,2,3])). % 204.46/204.55 cnf(223,plain, % 204.46/204.55 (E(f1(f1(x2231,x2231),f1(f1(x2232,a4),x2232)),f6(f1(x2233,x2233),f1(x2234,x2234)))), % 204.46/204.55 inference(scs_inference,[],[21,49,219,2,3])). % 204.46/204.55 cnf(227,plain, % 204.46/204.55 (E(f1(f1(x2271,x2271),f1(f1(x2272,a4),x2272)),f5(f1(x2273,x2273)))), % 204.46/204.55 inference(scs_inference,[],[21,27,223,2,3])). % 204.46/204.55 cnf(231,plain, % 204.46/204.55 (E(f1(f1(x2311,x2311),f1(f1(x2312,x2312),a4)),f1(x2313,x2313))), % 204.46/204.55 inference(scs_inference,[],[21,227,109,2,3])). % 204.46/204.55 cnf(235,plain, % 204.46/204.55 (E(f1(f1(x2351,x2351),f1(f1(x2352,x2352),a4)),f1(f1(x2353,x2353),f1(x2354,x2354)))), % 204.46/204.55 inference(scs_inference,[],[21,231,113,2,3])). % 204.46/204.55 cnf(239,plain, % 204.46/204.55 (E(f1(f1(x2391,x2391),f1(f1(x2392,a4),x2392)),f1(x2393,x2393))), % 204.46/204.55 inference(scs_inference,[],[21,235,18,2,3])). % 204.46/204.55 cnf(258,plain, % 204.46/204.55 (E(f1(x2581,x2581),f6(f1(x2582,x2582),a4))), % 204.46/204.55 inference(scs_inference,[],[23,239,3,2])). % 204.46/204.55 cnf(263,plain, % 204.46/204.55 (E(f6(f1(f1(x2631,x2631),x2632),x2632),f6(f1(x2633,x2633),a4))), % 204.46/204.55 inference(scs_inference,[],[23,258,3])). % 204.46/204.55 cnf(267,plain, % 204.46/204.55 (E(f6(f1(x2671,x2671),f1(x2672,x2672)),f6(f1(x2673,x2673),a4))), % 204.46/204.55 inference(scs_inference,[],[79,263,3])). % 204.46/204.55 cnf(269,plain, % 204.46/204.55 (E(f6(f1(x2691,x2691),a4),f6(f1(x2692,x2692),f1(x2693,x2693)))), % 204.46/204.55 inference(scs_inference,[],[79,263,3,2])). % 204.46/204.55 cnf(270,plain, % 204.46/204.55 (E(f5(f1(f1(x2701,a4),x2701)),a4)), % 204.46/204.55 inference(scs_inference,[],[182,148,3])). % 204.46/204.55 cnf(274,plain, % 204.46/204.55 (E(f6(f1(a4,x2741),x2741),f6(f1(x2742,x2742),a4))), % 204.46/204.55 inference(scs_inference,[],[150,267,270,2,3])). % 204.46/204.55 cnf(278,plain, % 204.46/204.55 (E(f6(f1(x2781,x2781),a4),f1(f1(x2782,x2782),f1(x2783,x2783)))), % 204.46/204.55 inference(scs_inference,[],[92,269,274,2,3])). % 204.46/204.55 cnf(304,plain, % 204.46/204.55 (E(f6(f1(x3041,x3041),x3042),f5(f1(f1(x3043,x3043),x3042)))), % 204.46/204.55 inference(scs_inference,[],[23,10,3])). % 204.46/204.55 cnf(307,plain, % 204.46/204.55 (E(f5(f1(f1(x3071,x3071),x3072)),f6(f1(x3073,x3073),x3072))), % 204.46/204.55 inference(scs_inference,[],[23,10,3,2])). % 204.46/204.55 cnf(315,plain, % 204.46/204.55 (E(x3151,f5(f1(f1(x3152,x3151),x3152)))), % 204.46/204.55 inference(scs_inference,[],[29,10,3])). % 204.46/204.55 cnf(337,plain, % 204.46/204.55 (E(x3371,f6(f1(x3372,x3372),x3371))), % 204.46/204.55 inference(scs_inference,[],[315,307,3])). % 204.46/204.55 cnf(340,plain, % 204.46/204.55 (E(f6(f1(x3401,x3401),x3402),x3402)), % 204.46/204.55 inference(scs_inference,[],[315,307,3,2])). % 204.46/204.55 cnf(341,plain, % 204.46/204.55 (~E(f6(f5(a2),a2),f6(f1(x3411,x3411),f6(f5(a3),a3)))), % 204.46/204.55 inference(scs_inference,[],[340,13,3])). % 204.46/204.55 cnf(343,plain, % 204.46/204.55 (E(x3431,f5(f1(f1(x3432,x3432),x3431)))), % 204.46/204.55 inference(scs_inference,[],[337,304,3])). % 204.46/204.55 cnf(345,plain, % 204.46/204.55 (E(f5(f1(f1(x3451,x3451),x3452)),x3452)), % 204.46/204.55 inference(scs_inference,[],[337,304,3,2])). % 204.46/204.55 cnf(348,plain, % 204.46/204.55 (E(f1(f1(x3481,x3481),f1(f1(x3482,x3482),x3483)),x3483)), % 204.46/204.55 inference(scs_inference,[],[343,17,3,2])). % 204.46/204.55 cnf(349,plain, % 204.46/204.55 (E(f1(f1(x3491,x3491),f1(f1(x3492,x3492),f5(x3493))),f1(f1(x3494,x3494),x3493))), % 204.46/204.55 inference(scs_inference,[],[348,17,3])). % 204.46/204.55 cnf(358,plain, % 204.46/204.55 (E(f1(f1(x3581,x3581),x3582),f6(f1(x3583,x3583),f5(x3582)))), % 204.46/204.55 inference(scs_inference,[],[23,349,3,2])). % 204.46/204.55 cnf(359,plain, % 204.46/204.55 (E(f1(f1(x3591,x3591),f1(x3592,x3592)),f6(f1(x3593,x3593),f5(f1(x3594,x3594))))), % 204.46/204.55 inference(scs_inference,[],[72,358,3])). % 204.46/204.55 cnf(370,plain, % 204.46/204.55 (E(f6(f1(x3701,x3701),f5(f1(x3702,x3702))),f5(f1(x3703,x3703)))), % 204.46/204.55 inference(scs_inference,[],[44,358,3,2])). % 204.46/204.55 cnf(373,plain, % 204.46/204.55 (E(f6(f1(x3731,x3731),f1(x3732,x3732)),f6(f1(x3733,x3733),f5(f1(x3734,x3734))))), % 204.46/204.55 inference(scs_inference,[],[370,86,3,2])). % 204.46/204.55 cnf(377,plain, % 204.46/204.55 (E(a4,f6(f1(x3771,x3771),f5(f1(x3772,x3772))))), % 204.46/204.55 inference(scs_inference,[],[60,373,3])). % 204.46/204.55 cnf(387,plain, % 204.46/204.55 (E(x3871,f1(f1(x3872,x3872),f1(f1(x3873,x3871),x3873)))), % 204.46/204.55 inference(scs_inference,[],[315,17,3])). % 204.46/204.55 cnf(434,plain, % 204.46/204.55 (E(f6(f1(x4341,x4341),f5(x4342)),f6(f1(x4343,x4343),f1(f1(x4344,x4344),x4342)))), % 204.46/204.55 inference(scs_inference,[],[340,358,3,2])). % 204.46/204.55 cnf(447,plain, % 204.46/204.55 (E(f6(f1(x4471,x4471),f1(f1(x4472,x4472),f1(x4473,x4473))),f1(f1(x4474,x4474),f1(x4475,x4475)))), % 204.46/204.55 inference(scs_inference,[],[359,434,3,2])). % 204.46/204.55 cnf(456,plain, % 204.46/204.55 (E(f6(f1(x4561,x4561),f1(f1(x4562,x4562),f1(x4563,x4563))),a4)), % 204.46/204.55 inference(scs_inference,[],[377,434,3,2])). % 204.46/204.55 cnf(513,plain, % 204.46/204.55 (E(f1(f1(x5131,x5131),x5132),f1(a4,x5132))), % 204.46/204.55 inference(scs_inference,[],[9,8,4])). % 204.46/204.55 cnf(514,plain, % 204.46/204.55 (E(f1(x5141,f1(x5142,x5142)),f1(x5141,a4))), % 204.46/204.55 inference(scs_inference,[],[9,8,4,5])). % 204.46/204.55 cnf(515,plain, % 204.46/204.55 (E(f6(f1(x5151,x5151),x5152),f6(a4,x5152))), % 204.46/204.55 inference(scs_inference,[],[9,8,4,5,6])). % 204.46/204.55 cnf(517,plain, % 204.46/204.55 (~E(f6(f1(x5171,x5171),f6(f5(a3),a3)),f6(f5(a2),a2))), % 204.46/204.55 inference(scs_inference,[],[9,341,8,4,5,6,7,2])). % 204.46/204.55 cnf(526,plain, % 204.46/204.55 (~E(f6(a4,f6(f5(a3),a3)),f6(f5(a2),a2))), % 204.46/204.55 inference(scs_inference,[],[513,515,517,15,4,6,5,8,7,2,3])). % 204.46/204.55 cnf(535,plain, % 204.46/204.55 (E(f1(a4,f1(x5351,x5351)),a4)), % 204.46/204.55 inference(scs_inference,[],[9,514,526,6,5,4,8,7,2,3])). % 204.46/204.55 cnf(550,plain, % 204.46/204.55 (E(f1(x5501,a4),f1(x5501,f1(f1(x5502,x5502),f1(x5503,x5503))))), % 204.46/204.55 inference(scs_inference,[],[89,4,5])). % 204.46/204.55 cnf(555,plain, % 204.46/204.55 (E(f5(f1(a4,f1(x5551,x5551))),f5(a4))), % 204.46/204.55 inference(scs_inference,[],[535,5,8])). % 204.46/204.55 cnf(586,plain, % 204.46/204.55 (E(f1(f1(f1(x5861,x5861),x5862),x5863),f1(f5(x5862),x5863))), % 204.46/204.55 inference(scs_inference,[],[10,8,5,4])). % 204.46/204.55 cnf(663,plain, % 204.46/204.55 (E(f6(f6(f1(a4,x6631),x6631),x6632),f6(a4,x6632))), % 204.46/204.55 inference(scs_inference,[],[108,5,6])). % 204.46/204.55 cnf(666,plain, % 204.46/204.55 (E(f6(x6661,f6(f1(a4,x6662),x6662)),f6(x6661,a4))), % 204.46/204.55 inference(scs_inference,[],[108,5,6,4,8,7])). % 204.46/204.55 cnf(668,plain, % 204.46/204.55 (E(f1(a4,x6681),f1(f1(x6682,x6682),x6681))), % 204.46/204.55 inference(scs_inference,[],[14,5,4])). % 204.46/204.55 cnf(713,plain, % 204.46/204.55 (E(f6(f5(x7131),x7132),f6(f1(f1(x7133,x7133),x7131),x7132))), % 204.46/204.55 inference(scs_inference,[],[340,17,5,6])). % 204.46/204.55 cnf(732,plain, % 204.46/204.55 (~E(f6(f5(a3),a3),f1(f5(a2),f1(f1(x7321,x7321),a2)))), % 204.46/204.55 inference(scs_inference,[],[23,13,3,2])). % 204.46/204.55 cnf(763,plain, % 204.46/204.55 (E(f6(f6(f1(a4,x7631),x7631),f6(f1(a4,x7632),x7632)),f6(a4,a4))), % 204.46/204.55 inference(scs_inference,[],[663,666,3])). % 204.46/204.55 cnf(789,plain, % 204.46/204.55 (E(f1(f1(x7891,x7891),a4),f6(f1(a4,x7892),x7892))), % 204.46/204.55 inference(scs_inference,[],[121,550,3])). % 204.46/204.55 cnf(835,plain, % 204.46/204.55 (~E(f1(f5(a2),f1(f1(x8351,x8351),a2)),f6(f1(f1(x8352,x8352),a3),a3))), % 204.46/204.55 inference(scs_inference,[],[195,713,732,5,6,4,8,7,3,2])). % 204.46/204.55 cnf(862,plain, % 204.46/204.55 (E(f6(f1(x8621,x8621),f1(a4,f1(x8622,x8622))),a4)), % 204.46/204.55 inference(scs_inference,[],[340,535,789,2,3])). % 204.46/204.55 cnf(912,plain, % 204.46/204.55 (E(f6(f1(x9121,x9121),f1(f1(x9122,x9122),x9123)),f1(a4,x9123))), % 204.46/204.55 inference(scs_inference,[],[340,513,763,2,3])). % 204.46/204.55 cnf(930,plain, % 204.46/204.56 (E(f6(f1(x9301,x9301),f1(a4,x9302)),f1(f1(x9303,x9303),x9302))), % 204.46/204.56 inference(scs_inference,[],[340,668,912,2,3])). % 204.46/204.56 cnf(960,plain, % 204.46/204.56 (E(f6(f1(x9601,x9601),f5(f1(x9602,x9602))),f6(f1(f1(x9603,x9603),x9604),x9604))), % 204.46/204.56 inference(scs_inference,[],[340,53,555,2,3])). % 204.46/204.56 cnf(1103,plain, % 204.46/204.56 (E(f1(f1(x11031,x11031),x11032),f6(f1(x11033,x11033),f1(a4,x11032)))), % 204.46/204.56 inference(scs_inference,[],[930,2])). % 204.46/204.56 cnf(1415,plain, % 204.46/204.56 (E(f6(f1(f1(x14151,x14151),x14152),x14152),f6(f1(x14153,x14153),f5(f1(x14154,x14154))))), % 204.46/204.56 inference(scs_inference,[],[960,2])). % 204.46/204.56 cnf(1589,plain, % 204.46/204.56 (E(a4,f6(f1(x15891,x15891),f1(a4,f1(x15892,x15892))))), % 204.46/204.56 inference(scs_inference,[],[862,2])). % 204.46/204.56 cnf(1721,plain, % 204.46/204.56 (E(f6(x17211,f5(f1(f1(x17212,x17212),x17213))),f6(x17211,x17213))), % 204.46/204.56 inference(scs_inference,[],[345,7])). % 204.46/204.56 cnf(1722,plain, % 204.46/204.56 (E(f1(f5(f1(f1(x17221,x17221),x17222)),x17223),f1(x17222,x17223))), % 204.46/204.56 inference(scs_inference,[],[345,7,4])). % 204.46/204.56 cnf(1752,plain, % 204.46/204.56 (~E(f6(f1(f1(x17521,x17521),a3),a3),f6(f5(a2),a2))), % 204.46/204.56 inference(scs_inference,[],[11,1103,835,7,5,8,4,6,3,2])). % 204.46/204.56 cnf(1847,plain, % 204.46/204.56 (E(f1(f5(f1(f1(x18471,x18471),f1(x18472,x18473))),f1(f1(x18472,x18474),x18473)),x18474)), % 204.46/204.56 inference(scs_inference,[],[12,1722,1589,7,5,4,8,6,3])). % 204.46/204.56 cnf(1869,plain, % 204.46/204.56 (E(f1(f1(f1(x18691,x18691),x18692),f1(f1(x18693,x18693),x18694)),f6(f5(x18692),x18694))), % 204.46/204.56 inference(scs_inference,[],[11,586,96,7,5,4,8,6,3])). % 204.46/204.56 cnf(1901,plain, % 204.46/204.56 (~E(f6(f1(x19011,x19011),f5(f1(x19012,x19012))),f6(f5(a2),a2))), % 204.46/204.56 inference(scs_inference,[],[1415,1752,387,7,5,4,8,6,3])). % 204.46/204.56 cnf(1910,plain, % 204.46/204.56 (~E(f6(f1(x19101,x19101),f1(x19102,x19102)),f6(f5(a2),a2))), % 204.46/204.56 inference(scs_inference,[],[1721,1901,30,7,5,4,8,6,3])). % 204.46/204.56 cnf(1918,plain, % 204.46/204.56 (~E(f1(f1(x19181,x19181),f1(x19182,x19182)),f6(f5(a2),a2))), % 204.46/204.56 inference(scs_inference,[],[447,1910,103,7,5,4,8,6,3])). % 204.46/204.56 cnf(1929,plain, % 204.46/204.56 (~E(f1(f1(x19291,x19291),f1(x19292,x19292)),f6(f5(a2),a2))), % 204.46/204.56 inference(rename_variables,[],[1918])). % 204.46/204.56 cnf(1930,plain, % 204.46/204.56 (~E(f6(f5(a2),a2),f1(f1(x19301,x19301),f1(x19302,x19302)))), % 204.46/204.56 inference(scs_inference,[],[9,1918,1929,278,7,5,4,8,6,3,2])). % 204.46/204.56 cnf(2063,plain, % 204.46/204.56 (E(f6(f5(x20631),x20632),f1(f1(f1(x20633,x20633),x20631),f1(f1(x20634,x20634),x20632)))), % 204.46/204.56 inference(scs_inference,[],[456,1869,7,5,4,6,8,2])). % 204.46/204.56 cnf(2072,plain, % 204.46/204.56 ($false), % 204.46/204.56 inference(scs_inference,[],[125,2063,75,1847,1930,7,5,4,6,8,2,3]), % 204.46/204.56 ['proof']). % 204.46/204.56 % SZS output end Proof % 204.46/204.56 % Total time :203.760000s %------------------------------------------------------------------------------