%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP533-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 : n024.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:52 EDT 2024 % Result : Unsatisfiable 117.53s 118.19s % Output : CNFRefutation 117.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : GRP533-1 : TPTP v8.2.0. Released v2.6.0. % 0.06/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n024.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 11:32:54 EDT 2024 % 0.12/0.34 % CPUTime : % 0.19/0.58 start to proof:theBenchmark % 117.46/118.18 %------------------------------------------- % 117.46/118.18 % File :CSE---1.7 % 117.46/118.18 % Problem :theBenchmark % 117.46/118.18 % Transform :cnf % 117.46/118.18 % Format :tptp:raw % 117.46/118.18 % Command :java -jar mcs_scs.jar %d %s % 117.46/118.18 % 117.46/118.18 % Result :Theorem 116.920000s % 117.46/118.18 % Output :CNFRefutation 116.920000s % 117.46/118.18 %------------------------------------------- % 117.53/118.19 %-------------------------------------------------------------------------- % 117.53/118.19 % File : GRP533-1 : TPTP v8.2.0. Released v2.6.0. % 117.53/118.19 % Domain : Group Theory (Abelian) % 117.53/118.19 % Problem : Axiom for Abelian group theory, in division, part 1 % 117.53/118.19 % Version : [McC93] (equality) axioms. % 117.53/118.19 % English : % 117.53/118.19 % 117.53/118.19 % Refs : [McC93] McCune (1993), Single Axioms for Groups and Abelian Gr % 117.53/118.19 % Source : [TPTP] % 117.53/118.19 % Names : % 117.53/118.19 % 117.53/118.19 % Status : Unsatisfiable % 117.53/118.19 % Rating : 0.00 v7.4.0, 0.04 v7.3.0, 0.00 v6.0.0, 0.05 v5.5.0, 0.00 v2.6.0 % 117.53/118.19 % Syntax : Number of clauses : 5 ( 5 unt; 0 nHn; 1 RR) % 117.53/118.19 % Number of literals : 5 ( 5 equ; 1 neg) % 117.53/118.19 % Maximal clause size : 1 ( 1 avg) % 117.53/118.19 % Maximal term depth : 5 ( 2 avg) % 117.53/118.19 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 117.53/118.19 % Number of functors : 6 ( 6 usr; 3 con; 0-2 aty) % 117.53/118.19 % Number of variables : 9 ( 0 sgn) % 117.53/118.19 % SPC : CNF_UNS_RFO_PEQ_UEQ % 117.53/118.19 % 117.53/118.19 % Comments : A UEQ part of GRP091-1 % 117.53/118.19 %-------------------------------------------------------------------------- % 117.53/118.19 cnf(single_axiom,axiom, % 117.53/118.19 divide(divide(A,divide(divide(A,B),C)),B) = C ). % 117.53/118.19 % 117.53/118.19 cnf(multiply,axiom, % 117.53/118.19 multiply(A,B) = divide(A,divide(divide(C,C),B)) ). % 117.53/118.19 % 117.53/118.19 cnf(inverse,axiom, % 117.53/118.19 inverse(A) = divide(divide(B,B),A) ). % 117.53/118.19 % 117.53/118.19 cnf(identity,axiom, % 117.53/118.19 identity = divide(A,A) ). % 117.53/118.19 % 117.53/118.19 cnf(prove_these_axioms_1,negated_conjecture, % 117.53/118.19 multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ). % 117.53/118.19 % 117.53/118.19 %-------------------------------------------------------------------------- % 117.53/118.19 %------------------------------------------- % 117.53/118.19 % Proof found % 117.53/118.19 % SZS status Theorem for theBenchmark % 117.53/118.19 % SZS output start Proof % 117.53/118.21 %ClaNum:13(EqnAxiom:8) % 117.53/118.21 %VarNum:18(SingletonVarNum:9) % 117.53/118.21 %MaxLitNum:1 % 117.53/118.21 %MaxfuncDepth:4 % 117.53/118.21 %SharedTerms:8 % 117.53/118.21 %goalClause: 13 % 117.53/118.21 %singleGoalClaCount:1 % 117.53/118.21 [13]~E(f6(f5(a2),a2),f6(f5(a3),a3)) % 117.53/118.21 [9]E(f1(x91,x91),a4) % 117.53/118.21 [10]E(f1(f1(x101,x101),x102),f5(x102)) % 117.53/118.21 [11]E(f1(x111,f1(f1(x112,x112),x113)),f6(x111,x113)) % 117.53/118.21 [12]E(f1(f1(x121,f1(f1(x121,x122),x123)),x122),x123) % 117.53/118.21 %EqnAxiom % 117.53/118.21 [1]E(x11,x11) % 117.53/118.21 [2]E(x22,x21)+~E(x21,x22) % 117.53/118.21 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 117.53/118.21 [4]~E(x41,x42)+E(f1(x41,x43),f1(x42,x43)) % 117.53/118.21 [5]~E(x51,x52)+E(f1(x53,x51),f1(x53,x52)) % 117.53/118.21 [6]~E(x61,x62)+E(f6(x61,x63),f6(x62,x63)) % 117.53/118.21 [7]~E(x71,x72)+E(f6(x73,x71),f6(x73,x72)) % 117.53/118.21 [8]~E(x81,x82)+E(f5(x81),f5(x82)) % 117.53/118.21 % 117.53/118.21 %------------------------------------------- % 117.53/118.22 cnf(14,plain, % 117.53/118.22 (E(a4,f1(x141,x141))), % 117.53/118.22 inference(scs_inference,[],[9,2])). % 117.53/118.22 cnf(15,plain, % 117.53/118.22 (E(f1(f1(x151,f1(f1(x151,x152),f1(x153,x153))),x152),a4)), % 117.53/118.22 inference(scs_inference,[],[9,12,2,3])). % 117.53/118.22 cnf(17,plain, % 117.53/118.22 (E(a4,f1(f1(x171,f1(f1(x171,x172),f1(x173,x173))),x172))), % 117.53/118.23 inference(scs_inference,[],[15,2])). % 117.53/118.23 cnf(18,plain, % 117.53/118.23 (E(f1(f1(x181,f1(f1(x181,x182),f1(x183,x183))),x182),f1(x184,x184))), % 117.53/118.23 inference(scs_inference,[],[14,15,2,3])). % 117.53/118.23 cnf(19,plain, % 117.53/118.23 (E(f1(x191,x191),f1(f1(x192,f1(f1(x192,x193),f1(x194,x194))),x193))), % 117.53/118.23 inference(scs_inference,[],[18,2])). % 117.53/118.23 cnf(20,plain, % 117.53/118.23 (E(a4,f5(f1(x201,x201)))), % 117.53/118.23 inference(scs_inference,[],[14,18,10,2,3])). % 117.53/118.23 cnf(23,plain, % 117.53/118.23 (E(f5(f1(x231,x231)),a4)), % 117.53/118.23 inference(scs_inference,[],[20,2])). % 117.53/118.23 cnf(24,plain, % 117.53/118.23 (E(f1(f1(x241,f1(f1(x241,x242),f1(x243,x243))),x242),f5(f1(x244,x244)))), % 117.53/118.23 inference(scs_inference,[],[20,15,2,3])). % 117.53/118.23 cnf(25,plain, % 117.53/118.23 (E(f5(f1(x251,x251)),f1(f1(x252,f1(f1(x252,x253),f1(x254,x254))),x253))), % 117.53/118.23 inference(scs_inference,[],[24,2])). % 117.53/118.23 cnf(26,plain, % 117.53/118.23 (E(f5(f1(x261,x261)),f1(x262,x262))), % 117.53/118.23 inference(scs_inference,[],[23,14,24,2,3])). % 117.53/118.23 cnf(27,plain, % 117.53/118.23 (E(f1(x271,x271),f5(f1(x272,x272)))), % 117.53/118.23 inference(scs_inference,[],[26,2])). % 117.53/118.23 cnf(28,plain, % 117.53/118.23 (E(f1(x281,x281),f1(x282,x282))), % 117.53/118.23 inference(scs_inference,[],[19,26,18,2,3])). % 117.53/118.23 cnf(30,plain, % 117.53/118.23 (E(f6(x301,x302),f1(x301,f1(f1(x303,x303),x302)))), % 117.53/118.23 inference(scs_inference,[],[11,2])). % 117.53/118.23 cnf(33,plain, % 117.53/118.23 (E(f5(x331),f1(f1(x332,x332),x331))), % 117.53/118.23 inference(scs_inference,[],[10,2])). % 117.53/118.23 cnf(34,plain, % 117.53/118.23 (E(f6(f1(f1(x341,x341),x342),x342),f5(f1(x343,x343)))), % 117.53/118.23 inference(scs_inference,[],[27,30,10,2,3])). % 117.53/118.23 cnf(37,plain, % 117.53/118.23 (E(f5(f1(x371,x371)),f6(f1(f1(x372,x372),x373),x373))), % 117.53/118.23 inference(scs_inference,[],[34,2])). % 117.53/118.23 cnf(38,plain, % 117.53/118.23 (E(f1(x381,x381),f1(f1(x382,x382),f1(x383,x383)))), % 117.53/118.23 inference(scs_inference,[],[33,27,34,2,3])). % 117.53/118.23 cnf(40,plain, % 117.53/118.23 (E(f1(f1(x401,x401),f1(x402,x402)),f1(x403,x403))), % 117.53/118.23 inference(scs_inference,[],[38,2])). % 117.53/118.23 cnf(41,plain, % 117.53/118.23 (E(f1(x411,x411),f6(f1(f1(x412,x412),x413),x413))), % 117.53/118.23 inference(scs_inference,[],[37,27,38,2,3])). % 117.53/118.23 cnf(43,plain, % 117.53/118.23 (E(f6(f1(f1(x431,x431),x432),x432),f1(x433,x433))), % 117.53/118.23 inference(scs_inference,[],[41,2])). % 117.53/118.23 cnf(44,plain, % 117.53/118.23 (E(f5(f1(x441,x441)),f1(f1(f1(x442,x442),x443),f1(f1(x444,x444),x443)))), % 117.53/118.23 inference(scs_inference,[],[30,37,41,2,3])). % 117.53/118.23 cnf(46,plain, % 117.53/118.23 (E(f1(f1(f1(x461,x461),x462),f1(f1(x463,x463),x462)),f5(f1(x464,x464)))), % 117.53/118.23 inference(scs_inference,[],[44,2])). % 117.53/118.23 cnf(47,plain, % 117.53/118.23 (E(f1(f1(x471,x471),f1(x472,x472)),f1(f1(x473,f1(f1(x473,x474),f1(x475,x475))),x474))), % 117.53/118.23 inference(scs_inference,[],[40,19,44,2,3])). % 117.53/118.23 cnf(49,plain, % 117.53/118.23 (E(f1(f1(x491,f1(f1(x491,x492),f1(x493,x493))),x492),f1(f1(x494,x494),f1(x495,x495)))), % 117.53/118.23 inference(scs_inference,[],[47,2])). % 117.53/118.23 cnf(50,plain, % 117.53/118.23 (E(f1(f1(f1(x501,x501),x502),f1(f1(x503,x503),x502)),f1(f1(x504,x504),f1(x505,x505)))), % 117.53/118.23 inference(scs_inference,[],[46,33,47,2,3])). % 117.53/118.23 cnf(52,plain, % 117.53/118.23 (E(f1(f1(x521,x521),f1(x522,x522)),f1(f1(f1(x523,x523),x524),f1(f1(x525,x525),x524)))), % 117.53/118.23 inference(scs_inference,[],[50,2])). % 117.53/118.23 cnf(53,plain, % 117.53/118.23 (E(a4,f1(f1(x531,x531),f1(x532,x532)))), % 117.53/118.23 inference(scs_inference,[],[49,17,50,2,3])). % 117.53/118.23 cnf(55,plain, % 117.53/118.23 (E(f1(f1(x551,x551),f1(x552,x552)),a4)), % 117.53/118.23 inference(scs_inference,[],[53,2])). % 117.53/118.23 cnf(56,plain, % 117.53/118.23 (E(f5(f1(x561,x561)),f1(f1(x562,x562),f1(x563,x563)))), % 117.53/118.23 inference(scs_inference,[],[49,25,53,2,3])). % 117.53/118.23 cnf(58,plain, % 117.53/118.23 (E(f1(f1(x581,x581),f1(x582,x582)),f5(f1(x583,x583)))), % 117.53/118.23 inference(scs_inference,[],[56,2])). % 117.53/118.23 cnf(59,plain, % 117.53/118.23 (E(f6(f1(f1(x591,x591),x592),x592),a4)), % 117.53/118.23 inference(scs_inference,[],[43,55,56,2,3])). % 117.53/118.23 cnf(62,plain, % 117.53/118.23 (E(a4,f6(f1(f1(x621,x621),x622),x622))), % 117.53/118.23 inference(scs_inference,[],[59,2])). % 117.53/118.23 cnf(66,plain, % 117.53/118.23 (E(f1(f1(f1(x661,x661),x662),f1(f1(x663,x663),x662)),a4)), % 117.53/118.23 inference(scs_inference,[],[46,23,12,2,3])). % 117.53/118.23 cnf(68,plain, % 117.53/118.23 (E(a4,f1(f1(f1(x681,x681),x682),f1(f1(x683,x683),x682)))), % 117.53/118.23 inference(scs_inference,[],[66,2])). % 117.53/118.23 cnf(69,plain, % 117.53/118.23 (E(f1(f1(x691,x691),f1(x692,x692)),f6(f1(f1(x693,x693),x694),x694))), % 117.53/118.23 inference(scs_inference,[],[62,55,66,2,3])). % 117.53/118.23 cnf(71,plain, % 117.53/118.23 (~E(f6(f5(a2),a2),f1(f5(a3),f1(f1(x711,x711),a3)))), % 117.53/118.23 inference(scs_inference,[],[13,69,11,2,3])). % 117.53/118.23 cnf(76,plain, % 117.53/118.23 (E(f1(f1(x761,x761),f1(x762,x762)),f5(f1(f1(x763,x763),f1(x764,x764))))), % 117.53/118.23 inference(scs_inference,[],[52,10,3])). % 117.53/118.23 cnf(79,plain, % 117.53/118.23 (E(f5(f1(f1(x791,x791),f1(x792,x792))),f1(f1(x793,x793),f1(x794,x794)))), % 117.53/118.23 inference(scs_inference,[],[52,10,3,2])). % 117.53/118.23 cnf(82,plain, % 117.53/118.23 (E(f5(f1(x821,x821)),f5(f1(f1(x822,x822),f1(x823,x823))))), % 117.53/118.23 inference(scs_inference,[],[79,58,3,2])). % 117.53/118.23 cnf(85,plain, % 117.53/118.23 (E(f1(f1(x851,x851),f1(f1(x852,x852),f1(x853,x853))),f5(f1(x854,x854)))), % 117.53/118.23 inference(scs_inference,[],[82,33,3,2])). % 117.53/118.23 cnf(90,plain, % 117.53/118.23 (E(f1(f1(x901,x901),f1(f1(x902,x902),f1(x903,x903))),f6(f1(f1(x904,x904),x905),x905))), % 117.53/118.23 inference(scs_inference,[],[85,37,3])). % 117.53/118.23 cnf(92,plain, % 117.53/118.23 (E(f6(f1(f1(x921,x921),x922),x922),f1(f1(x923,x923),f1(f1(x924,x924),f1(x925,x925))))), % 117.53/118.23 inference(scs_inference,[],[85,37,3,2])). % 117.53/118.23 cnf(95,plain, % 117.53/118.23 (E(f1(f1(x951,x951),f1(f1(x952,x952),f1(x953,x953))),a4)), % 117.53/118.23 inference(scs_inference,[],[92,62,3,2])). % 117.53/118.23 cnf(97,plain, % 117.53/118.23 (E(f1(f1(f1(x971,x971),x972),f1(f1(x973,x973),x972)),f1(f1(x974,x974),f1(f1(x975,x975),f1(x976,x976))))), % 117.53/118.23 inference(scs_inference,[],[68,95,3,2])). % 117.53/118.23 cnf(99,plain, % 117.53/118.23 (E(f1(x991,x991),f1(f1(x992,x992),f1(f1(x993,x993),f1(x994,x994))))), % 117.53/118.23 inference(scs_inference,[],[95,14,3,2])). % 117.53/118.23 cnf(104,plain, % 117.53/118.23 (E(f1(f1(f1(x1041,x1041),x1042),f1(f1(x1043,x1043),x1042)),f1(x1044,x1044))), % 117.53/118.23 inference(scs_inference,[],[9,68,3,2])). % 117.53/118.23 cnf(105,plain, % 117.53/118.23 (E(f1(f1(f1(x1051,x1051),x1052),f1(f1(x1053,x1053),x1052)),f5(f1(f1(x1054,x1054),f1(x1055,x1055))))), % 117.53/118.23 inference(scs_inference,[],[104,76,3])). % 117.53/118.23 cnf(108,plain, % 117.53/118.23 (E(f5(f1(f1(x1081,x1081),f1(x1082,x1082))),f1(f1(f1(x1083,x1083),x1084),f1(f1(x1085,x1085),x1084)))), % 117.53/118.23 inference(scs_inference,[],[104,76,3,2])). % 117.53/118.23 cnf(113,plain, % 117.53/118.23 (E(f1(f1(f1(x1131,x1131),x1132),f1(f1(x1133,x1133),x1132)),f6(f1(f1(x1134,x1134),x1135),x1135))), % 117.53/118.23 inference(scs_inference,[],[97,90,3])). % 117.53/118.23 cnf(119,plain, % 117.53/118.23 (E(f5(f1(f1(x1191,x1191),f1(x1192,x1192))),f1(x1193,x1193))), % 117.53/118.23 inference(scs_inference,[],[99,105,3,2])). % 117.53/118.23 cnf(120,plain, % 117.53/118.23 (E(f5(f1(f1(x1201,x1201),f1(x1202,x1202))),a4)), % 117.53/118.23 inference(scs_inference,[],[9,119,3])). % 117.53/118.23 cnf(122,plain, % 117.53/118.23 (E(a4,f5(f1(f1(x1221,x1221),f1(x1222,x1222))))), % 117.53/118.23 inference(scs_inference,[],[9,119,3,2])). % 117.53/118.23 cnf(125,plain, % 117.53/118.23 (E(f6(f1(f1(x1251,x1251),x1252),x1252),f5(f1(f1(x1253,x1253),f1(x1254,x1254))))), % 117.53/118.23 inference(scs_inference,[],[108,113,3,2])). % 117.53/118.23 cnf(129,plain, % 117.53/118.23 (E(f1(f1(x1291,x1291),x1292),f1(f1(x1293,x1293),x1292))), % 117.53/118.23 inference(scs_inference,[],[10,33,3])). % 117.53/118.23 cnf(137,plain, % 117.53/118.23 (E(f5(f1(x1371,x1371)),f6(f1(x1372,x1372),f1(x1373,x1373)))), % 117.53/118.23 inference(scs_inference,[],[30,58,3,2])). % 117.53/118.23 cnf(138,plain, % 117.53/118.23 (E(f6(f1(f1(x1381,x1381),x1382),x1382),f6(f1(x1383,x1383),f1(x1384,x1384)))), % 117.53/118.23 inference(scs_inference,[],[137,125,3])). % 117.53/118.23 cnf(145,plain, % 117.53/118.23 (E(a4,f6(f1(x1451,x1451),f1(x1452,x1452)))), % 117.53/118.23 inference(scs_inference,[],[122,137,3])). % 117.53/118.23 cnf(157,plain, % 117.53/118.23 (E(f6(f1(x1571,x1571),x1572),f5(f1(f1(x1573,x1573),x1572)))), % 117.53/118.23 inference(scs_inference,[],[30,10,3])). % 117.53/118.23 cnf(160,plain, % 117.53/118.23 (E(f5(f1(f1(x1601,x1601),x1602)),f6(f1(x1603,x1603),x1602))), % 117.53/118.23 inference(scs_inference,[],[30,10,3,2])). % 117.53/118.23 cnf(184,plain, % 117.53/118.23 (E(f6(f1(x1841,x1841),x1842),f6(f1(x1843,x1843),x1842))), % 117.53/118.23 inference(scs_inference,[],[157,160,3])). % 117.53/118.23 cnf(217,plain, % 117.53/118.23 (E(f6(x2171,a4),f6(x2171,f6(f1(x2172,x2172),f1(x2173,x2173))))), % 117.53/118.23 inference(scs_inference,[],[145,4,7])). % 117.53/118.23 cnf(219,plain, % 117.53/118.23 (E(f6(a4,x2191),f6(f6(f1(x2192,x2192),f1(x2193,x2193)),x2191))), % 117.53/118.23 inference(scs_inference,[],[145,4,7,5,6])). % 117.53/118.23 cnf(221,plain, % 117.53/118.23 (~E(f1(f5(a3),f1(f1(x2211,x2211),a3)),f6(f5(a2),a2))), % 117.53/118.23 inference(scs_inference,[],[145,71,4,7,5,6,8,2])). % 117.53/118.23 cnf(240,plain, % 117.53/118.23 (E(f1(f1(f1(x2401,x2401),x2402),x2403),f1(f1(f1(x2404,x2404),x2402),x2403))), % 117.53/118.23 inference(scs_inference,[],[129,7,5,4])). % 117.53/118.23 cnf(260,plain, % 117.53/118.23 (E(f5(f6(f1(x2601,x2601),x2602)),f5(f6(f1(x2603,x2603),x2602)))), % 117.53/118.23 inference(scs_inference,[],[184,7,5,4,6,8])). % 117.53/118.23 cnf(274,plain, % 117.53/118.23 (E(f5(f6(x2741,a4)),f5(f6(x2741,f6(f1(x2742,x2742),f1(x2743,x2743)))))), % 117.53/118.23 inference(scs_inference,[],[217,7,5,4,8])). % 117.53/118.23 cnf(297,plain, % 117.53/118.23 (E(f5(f5(f1(f1(x2971,x2971),f1(x2972,x2972)))),f5(a4))), % 117.53/118.23 inference(scs_inference,[],[120,5,4,7,8])). % 117.53/118.23 cnf(446,plain, % 117.53/118.23 (E(f1(f5(f1(x4461,x4461)),x4462),f1(f1(f1(x4463,x4463),f1(x4464,x4464)),x4462))), % 117.53/118.23 inference(scs_inference,[],[56,5,7,6,4])). % 117.53/118.23 cnf(493,plain, % 117.53/118.23 (E(f5(f6(a4,x4931)),f5(f6(f6(f1(x4932,x4932),f1(x4933,x4933)),x4931)))), % 117.53/118.23 inference(scs_inference,[],[219,5,7,6,4,8])). % 117.53/118.23 cnf(629,plain, % 117.53/118.23 (E(f1(a4,x6291),f1(f1(f1(x6292,x6292),f1(x6293,x6293)),x6291))), % 117.53/118.23 inference(scs_inference,[],[53,5,7,4])). % 117.53/118.23 cnf(661,plain, % 117.53/118.23 (E(f1(x6611,f1(a4,x6612)),f1(x6611,f1(f1(f1(x6613,x6613),f1(x6614,x6614)),x6612)))), % 117.53/118.23 inference(scs_inference,[],[629,7,5])). % 117.53/118.23 cnf(718,plain, % 117.53/118.23 (E(f5(a4),f5(f6(f1(f1(x7181,x7181),x7182),x7182)))), % 117.53/118.23 inference(scs_inference,[],[43,62,7,4,5,6,8])). % 117.53/118.23 cnf(837,plain, % 117.53/118.23 (E(f1(x8371,f1(f1(x8372,x8372),f1(x8373,x8373))),f1(x8371,a4))), % 117.53/118.23 inference(scs_inference,[],[55,85,7,4,8,5])). % 117.53/118.23 cnf(838,plain, % 117.53/118.23 (E(f6(f1(f1(x8381,x8381),f1(x8382,x8382)),x8383),f6(a4,x8383))), % 117.53/118.23 inference(scs_inference,[],[55,85,7,4,8,5,6])). % 117.53/118.23 cnf(844,plain, % 117.53/118.23 (E(f1(x8441,f1(x8442,x8442)),f1(x8441,a4))), % 117.53/118.23 inference(scs_inference,[],[9,5])). % 117.53/118.23 cnf(845,plain, % 117.53/118.23 (E(f5(f1(x8451,x8451)),f5(a4))), % 117.53/118.23 inference(scs_inference,[],[9,5,8])). % 117.53/118.23 cnf(846,plain, % 117.53/118.23 (E(f6(f1(x8461,x8461),x8462),f6(a4,x8462))), % 117.53/118.23 inference(scs_inference,[],[9,5,8,6])). % 117.53/118.23 cnf(847,plain, % 117.53/118.23 (E(f1(f1(x8471,x8471),x8472),f1(a4,x8472))), % 117.53/118.23 inference(scs_inference,[],[9,5,8,6,4])). % 117.53/118.23 cnf(848,plain, % 117.53/118.23 (E(f6(x8481,f1(x8482,x8482)),f6(x8481,a4))), % 117.53/118.23 inference(scs_inference,[],[9,5,8,6,4,7])). % 117.53/118.23 cnf(852,plain, % 117.53/118.23 (E(f1(x8521,f1(x8522,f1(x8523,x8523))),f1(x8521,f1(x8522,a4)))), % 117.53/118.23 inference(scs_inference,[],[844,5])). % 117.53/118.23 cnf(854,plain, % 117.53/118.23 (E(f6(f1(x8541,f1(x8542,x8542)),x8543),f6(f1(x8541,a4),x8543))), % 117.53/118.23 inference(scs_inference,[],[844,5,8,6])). % 117.53/118.23 cnf(856,plain, % 117.53/118.23 (E(f1(f1(x8561,f1(x8562,x8562)),x8563),f1(f1(x8561,a4),x8563))), % 117.53/118.23 inference(scs_inference,[],[844,5,8,6,7,4])). % 117.53/118.23 cnf(858,plain, % 117.53/118.23 (E(f5(f6(f1(x8581,x8581),x8582)),f5(f6(a4,x8582)))), % 117.53/118.23 inference(scs_inference,[],[846,5,8])). % 117.53/118.23 cnf(862,plain, % 117.53/118.23 (E(f1(x8621,f1(f1(x8622,x8622),x8623)),f1(x8621,f1(a4,x8623)))), % 117.53/118.23 inference(scs_inference,[],[847,5])). % 117.53/118.23 cnf(863,plain, % 117.53/118.23 (E(f5(f1(f1(x8631,x8631),x8632)),f5(f1(a4,x8632)))), % 117.53/118.23 inference(scs_inference,[],[847,5,8])). % 117.53/118.23 cnf(867,plain, % 117.53/118.23 (E(f5(f6(x8671,f1(x8672,x8672))),f5(f6(x8671,a4)))), % 117.53/118.23 inference(scs_inference,[],[848,8])). % 117.53/118.23 cnf(872,plain, % 117.53/118.23 (~E(f1(f5(a3),f1(a4,a3)),f6(f5(a2),a2))), % 117.53/118.23 inference(scs_inference,[],[848,862,221,8,5,4,6,7,3])). % 117.53/118.23 cnf(876,plain, % 117.53/118.23 (E(f1(x8761,f5(f1(x8762,x8762))),f1(x8761,f5(a4)))), % 117.53/118.23 inference(scs_inference,[],[845,5])). % 117.53/118.23 cnf(877,plain, % 117.53/118.23 (E(f5(f5(f1(x8771,x8771))),f5(f5(a4)))), % 117.53/118.23 inference(scs_inference,[],[845,5,8])). % 117.53/118.23 cnf(879,plain, % 117.53/118.23 (E(f1(f5(f1(x8791,x8791)),x8792),f1(f5(a4),x8792))), % 117.53/118.23 inference(scs_inference,[],[845,5,8,7,4])). % 117.53/118.23 cnf(881,plain, % 117.53/118.23 (E(f1(a4,f1(f1(x8811,x8811),f1(x8812,x8812))),a4)), % 117.53/118.23 inference(scs_inference,[],[9,845,837,5,8,7,4,6,3])). % 117.53/118.23 cnf(884,plain, % 117.53/118.23 (E(f5(f6(f1(f1(x8841,x8841),f1(x8842,x8842)),x8843)),f5(f6(a4,x8843)))), % 117.53/118.23 inference(scs_inference,[],[838,8])). % 117.53/118.23 cnf(898,plain, % 117.53/118.23 (E(f5(f1(a4,f1(f1(x8981,x8981),f1(x8982,x8982)))),f5(a4))), % 117.53/118.23 inference(scs_inference,[],[881,8])). % 117.53/118.23 cnf(903,plain, % 117.53/118.23 (~E(f1(f5(a3),f1(f1(f1(x9031,x9031),f1(x9032,x9032)),a3)),f6(f5(a2),a2))), % 117.53/118.23 inference(scs_inference,[],[881,661,872,8,5,7,4,6,3])). % 117.53/118.23 cnf(911,plain, % 117.53/118.23 (E(f1(f1(x9111,a4),f1(x9111,f1(x9112,x9112))),a4)), % 117.53/118.23 inference(scs_inference,[],[9,852,5,8,6,7,4,3])). % 117.53/118.23 cnf(915,plain, % 117.53/118.23 (E(f1(x9151,f1(f1(x9152,a4),f1(x9152,f1(x9153,x9153)))),f1(x9151,a4))), % 117.53/118.23 inference(scs_inference,[],[911,8,5])). % 117.53/118.23 cnf(920,plain, % 117.53/118.23 (E(f1(x9201,f1(f1(x9202,x9202),x9203)),f1(x9201,f5(x9203)))), % 117.53/118.23 inference(scs_inference,[],[10,5])). % 117.53/118.23 cnf(921,plain, % 117.53/118.23 (E(f5(f1(f1(x9211,x9211),x9212)),f5(f5(x9212)))), % 117.53/118.23 inference(scs_inference,[],[10,5,8])). % 117.53/118.23 cnf(924,plain, % 117.53/118.23 (E(f6(f1(f1(x9241,x9241),x9242),x9243),f6(f5(x9242),x9243))), % 117.53/118.23 inference(scs_inference,[],[10,5,8,7,4,6])). % 117.53/118.23 cnf(930,plain, % 117.53/118.23 (~E(f1(f5(a3),f5(a3)),f6(f5(a2),a2))), % 117.53/118.23 inference(scs_inference,[],[920,903,8,5,6,7,4,3])). % 117.53/118.23 cnf(939,plain, % 117.53/118.23 (E(f1(f1(x9391,x9391),f1(f1(x9392,x9392),x9393)),f5(f5(x9393)))), % 117.53/118.23 inference(scs_inference,[],[10,921,5,8,4,6,7,3])). % 117.53/118.23 cnf(961,plain, % 117.53/118.23 (~E(f1(x9611,x9611),f6(f5(a2),a2))), % 117.53/118.23 inference(scs_inference,[],[924,930,28,8,5,4,6,7,3])). % 117.53/118.23 cnf(969,plain, % 117.53/118.23 (~E(f5(f1(x9691,x9691)),f6(f5(a2),a2))), % 117.53/118.23 inference(scs_inference,[],[10,961,939,5,8,7,4,6,3])). % 117.53/118.23 cnf(972,plain, % 117.53/118.23 (~E(f6(f5(a2),a2),f5(f1(x9721,x9721)))), % 117.53/118.23 inference(scs_inference,[],[10,961,939,5,8,7,4,6,3,2])). % 117.53/118.23 cnf(978,plain, % 117.53/118.23 (~E(f5(f1(a4,f1(x9781,x9781))),f6(f5(a2),a2))), % 117.53/118.23 inference(scs_inference,[],[969,854,863,8,5,6,7,4,3])). % 117.53/118.23 cnf(995,plain, % 117.53/118.23 (~E(f5(a4),f6(f5(a2),a2))), % 117.53/118.23 inference(scs_inference,[],[856,978,898,8,5,7,4,6,3])). % 117.53/118.23 cnf(1045,plain, % 117.53/118.23 (~E(f5(f6(f1(f1(x10451,x10451),x10452),x10452)),f6(f5(a2),a2))), % 117.53/118.23 inference(scs_inference,[],[858,718,995,8,5,7,4,6,3])). % 117.53/118.23 cnf(1052,plain, % 117.53/118.23 (~E(f5(f6(f1(f1(x10521,x10521),f1(x10522,x10522)),a4)),f6(f5(a2),a2))), % 117.53/118.23 inference(scs_inference,[],[867,1045,5,8,6,7,4,3])). % 117.53/118.23 cnf(1061,plain, % 117.53/118.23 (~E(f5(f6(f1(x10611,x10611),a4)),f6(f5(a2),a2))), % 117.53/118.23 inference(scs_inference,[],[876,260,1052,8,5,4,6,7,3])). % 117.53/118.23 cnf(1078,plain, % 117.53/118.23 (~E(f5(f6(a4,a4)),f6(f5(a2),a2))), % 117.53/118.23 inference(scs_inference,[],[879,1061,884,8,5,6,7,4,3])). % 117.53/118.23 cnf(1096,plain, % 117.53/118.23 (~E(f5(f6(a4,f6(f1(x10961,x10961),f1(x10962,x10962)))),f6(f5(a2),a2))), % 117.53/118.23 inference(scs_inference,[],[1078,877,274,5,8,4,6,7,3])). % 117.53/118.23 cnf(1112,plain, % 117.53/118.23 (~E(f5(f6(f6(f1(x11121,x11121),f1(x11122,x11122)),a4)),f6(f5(a2),a2))), % 117.53/118.23 inference(scs_inference,[],[493,1078,837,5,8,4,6,7,3])). % 117.53/118.23 cnf(1187,plain, % 117.53/118.23 (E(f5(a4),f5(f1(x11871,x11871)))), % 117.53/118.23 inference(scs_inference,[],[14,8])). % 117.53/118.23 cnf(1188,plain, % 117.53/118.23 (E(f1(x11881,a4),f1(x11881,f1(x11882,x11882)))), % 117.53/118.23 inference(scs_inference,[],[14,8,5])). % 117.53/118.23 cnf(1189,plain, % 117.53/118.23 (E(f6(a4,x11891),f6(f1(x11892,x11892),x11891))), % 117.53/118.23 inference(scs_inference,[],[14,8,5,6])). % 117.53/118.23 cnf(1190,plain, % 117.53/118.23 (E(f1(a4,x11901),f1(f1(x11902,x11902),x11901))), % 117.53/118.23 inference(scs_inference,[],[14,8,5,6,4])). % 117.53/118.23 cnf(1191,plain, % 117.53/118.23 (E(f6(x11911,a4),f6(x11911,f1(x11912,x11912)))), % 117.53/118.23 inference(scs_inference,[],[14,8,5,6,4,7])). % 117.53/118.23 cnf(1192,plain, % 117.53/118.23 (~E(f1(f1(f1(x11921,a4),f1(x11921,f1(x11922,x11922))),a4),f6(f5(a2),a2))), % 117.53/118.23 inference(scs_inference,[],[14,915,961,8,5,6,4,7,3])). % 117.53/118.23 cnf(1197,plain, % 117.53/118.23 (E(f1(x11971,f1(x11972,a4)),f1(x11971,f1(x11972,f1(x11973,x11973))))), % 117.53/118.23 inference(scs_inference,[],[1188,8,5])). % 117.53/118.23 cnf(1201,plain, % 117.53/118.23 (~E(f1(f1(f1(x12011,a4),f1(x12011,f1(x12012,x12012))),f1(x12013,x12013)),f6(f5(a2),a2))), % 117.53/118.23 inference(scs_inference,[],[1188,1192,8,5,6,4,7,3])). % 117.53/118.23 cnf(1204,plain, % 117.53/118.23 (E(f5(f6(a4,x12041)),f5(f6(f1(x12042,x12042),x12041)))), % 117.53/118.23 inference(scs_inference,[],[1189,8])). % 117.53/118.23 cnf(1212,plain, % 117.53/118.23 (E(f5(f1(a4,x12121)),f5(f1(f1(x12122,x12122),x12121)))), % 117.53/118.23 inference(scs_inference,[],[1190,8])). % 117.53/118.23 cnf(1220,plain, % 117.53/118.23 (E(f5(f6(x12201,a4)),f5(f6(x12201,f1(x12202,x12202))))), % 117.53/118.23 inference(scs_inference,[],[1191,8])). % 117.53/118.23 cnf(1225,plain, % 117.53/118.23 (~E(f1(f1(f1(x12251,a4),f1(x12251,f1(x12252,x12252))),f1(a4,f1(x12253,x12253))),f6(f5(a2),a2))), % 117.53/118.23 inference(scs_inference,[],[1191,1197,1201,8,5,6,4,7,3])). % 117.53/118.23 cnf(1229,plain, % 117.53/118.23 (E(f5(f5(a4)),f5(f5(f1(x12291,x12291))))), % 117.53/118.23 inference(scs_inference,[],[1187,1225,2,8])). % 117.53/118.23 cnf(1230,plain, % 117.53/118.23 (E(f1(x12301,f5(a4)),f1(x12301,f5(f1(x12302,x12302))))), % 117.53/118.23 inference(scs_inference,[],[1187,1225,2,8,5])). % 117.53/118.23 cnf(1232,plain, % 117.53/118.23 (E(f1(f5(a4),x12321),f1(f5(f1(x12322,x12322)),x12321))), % 117.53/118.23 inference(scs_inference,[],[1187,1225,2,8,5,6,4])). % 117.53/118.23 cnf(1233,plain, % 117.53/118.23 (E(f6(x12331,f5(a4)),f6(x12331,f5(f1(x12332,x12332))))), % 117.53/118.23 inference(scs_inference,[],[1187,1225,2,8,5,6,4,7])). % 117.53/118.23 cnf(1309,plain, % 117.53/118.23 (~E(f5(f6(f1(x13091,x13091),f6(f1(x13092,x13092),f1(x13093,x13093)))),f6(f5(a2),a2))), % 117.53/118.23 inference(scs_inference,[],[1204,1096,8,5,6,4,7,3])). % 117.53/118.23 cnf(1317,plain, % 117.53/118.23 (~E(f5(f6(f6(f1(x13171,x13171),f1(x13172,x13172)),f1(x13173,x13173))),f6(f5(a2),a2))), % 117.53/118.23 inference(scs_inference,[],[1212,1220,1309,1112,2,8,5,6,4,7,3])). % 117.53/118.23 cnf(1325,plain, % 117.53/118.24 (~E(f1(f1(f1(x13251,x13251),f1(a4,f1(x13252,x13252))),f1(x13253,x13253)),f6(f5(a2),a2))), % 117.53/118.24 inference(scs_inference,[],[1230,1317,240,1201,2,8,5,6,4,7,3])). % 117.53/118.24 cnf(1334,plain, % 117.53/118.24 (~E(f1(f5(f1(x13341,x13341)),f5(a4)),f6(f5(a2),a2))), % 117.53/118.24 inference(scs_inference,[],[1232,1325,961,2,8,5,6,4,7,3])). % 117.53/118.24 cnf(1343,plain, % 117.53/118.24 (~E(f1(f1(f1(x13431,x13431),f1(x13432,x13432)),f5(a4)),f6(f5(a2),a2))), % 117.53/118.24 inference(scs_inference,[],[1334,1233,446,2,8,5,6,4,7,3])). % 117.53/118.24 cnf(1352,plain, % 117.53/118.24 (E(f5(f5(a4)),f5(a4))), % 117.53/118.24 inference(scs_inference,[],[1343,1229,297,2,8,5,6,4,7,3])). % 117.53/118.24 cnf(1355,plain, % 117.53/118.24 (E(f5(f5(f5(a4))),f5(f5(a4)))), % 117.53/118.24 inference(scs_inference,[],[1352,8])). % 117.53/118.24 cnf(1357,plain, % 117.53/118.24 (E(f6(f5(f5(a4)),x13571),f6(f5(a4),x13571))), % 117.53/118.24 inference(scs_inference,[],[1352,8,5,6])). % 117.53/118.24 cnf(1639,plain, % 117.53/118.24 (E(f6(f5(x16391),x16392),f6(f1(f1(x16393,x16393),x16391),x16392))), % 117.53/118.24 inference(scs_inference,[],[157,33,5,6])). % 117.53/118.24 cnf(1688,plain, % 117.53/118.24 (~E(f6(f5(a2),a2),f6(f1(x16881,x16881),f1(x16882,x16882)))), % 117.53/118.24 inference(scs_inference,[],[157,1355,972,2,3])). % 117.53/118.24 cnf(1695,plain, % 117.53/118.24 ($false), % 117.53/118.24 inference(scs_inference,[],[138,1357,1639,1688,2,3]), % 117.53/118.24 ['proof']). % 117.53/118.24 % SZS output end Proof % 117.53/118.24 % Total time :116.920000s %------------------------------------------------------------------------------