%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP542-1 : TPTP v8.2.0. Released v2.6.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n020.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:54 EDT 2024 % Result : Unsatisfiable 59.94s 59.96s % Output : CNFRefutation 59.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : GRP542-1 : TPTP v8.2.0. Released v2.6.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n020.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 12:21:24 EDT 2024 % 0.12/0.34 % CPUTime : % 0.49/0.57 start to proof:theBenchmark % 59.94/59.94 %------------------------------------------- % 59.94/59.94 % File :CSE---1.7 % 59.94/59.94 % Problem :theBenchmark % 59.94/59.94 % Transform :cnf % 59.94/59.94 % Format :tptp:raw % 59.94/59.94 % Command :java -jar mcs_scs.jar %d %s % 59.94/59.94 % 59.94/59.94 % Result :Theorem 59.330000s % 59.94/59.94 % Output :CNFRefutation 59.330000s % 59.94/59.94 %------------------------------------------- % 59.94/59.95 %-------------------------------------------------------------------------- % 59.94/59.95 % File : GRP542-1 : TPTP v8.2.0. Released v2.6.0. % 59.94/59.95 % Domain : Group Theory (Abelian) % 59.94/59.95 % Problem : Axiom for Abelian group theory, in division and identity, part 2 % 59.94/59.96 % Version : [McC93] (equality) axioms. % 59.94/59.96 % English : % 59.94/59.96 % 59.94/59.96 % Refs : [McC93] McCune (1993), Single Axioms for Groups and Abelian Gr % 59.94/59.96 % Source : [TPTP] % 59.94/59.96 % Names : % 59.94/59.96 % 59.94/59.96 % Status : Unsatisfiable % 59.94/59.96 % Rating : 0.00 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.14 v5.5.0, 0.11 v5.4.0, 0.00 v5.1.0, 0.07 v4.1.0, 0.09 v4.0.1, 0.07 v4.0.0, 0.08 v3.7.0, 0.00 v2.6.0 % 59.94/59.96 % Syntax : Number of clauses : 5 ( 5 unt; 0 nHn; 1 RR) % 59.94/59.96 % Number of literals : 5 ( 5 equ; 1 neg) % 59.94/59.96 % Maximal clause size : 1 ( 1 avg) % 59.94/59.96 % Maximal term depth : 6 ( 2 avg) % 59.94/59.96 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 59.94/59.96 % Number of functors : 6 ( 6 usr; 3 con; 0-2 aty) % 59.94/59.96 % Number of variables : 7 ( 0 sgn) % 59.94/59.96 % SPC : CNF_UNS_RFO_PEQ_UEQ % 59.94/59.96 % 59.94/59.96 % Comments : A UEQ part of GRP093-1 % 59.94/59.96 %-------------------------------------------------------------------------- % 59.94/59.96 cnf(single_axiom,axiom, % 59.94/59.96 divide(divide(identity,divide(divide(divide(A,B),C),A)),C) = B ). % 59.94/59.96 % 59.94/59.96 cnf(multiply,axiom, % 59.94/59.96 multiply(A,B) = divide(A,divide(identity,B)) ). % 59.94/59.96 % 59.94/59.96 cnf(inverse,axiom, % 59.94/59.96 inverse(A) = divide(identity,A) ). % 59.94/59.96 % 59.94/59.96 cnf(identity,axiom, % 59.94/59.96 identity = divide(A,A) ). % 59.94/59.96 % 59.94/59.96 cnf(prove_these_axioms_2,negated_conjecture, % 59.94/59.96 multiply(multiply(inverse(b2),b2),a2) != a2 ). % 59.94/59.96 % 59.94/59.96 %-------------------------------------------------------------------------- % 59.94/59.96 %------------------------------------------- % 59.94/59.96 % Proof found % 59.94/59.96 % SZS status Theorem for theBenchmark % 59.94/59.96 % SZS output start Proof % 59.94/59.97 %ClaNum:8(EqnAxiom:5) % 59.94/59.97 %VarNum:8(SingletonVarNum:4) % 59.94/59.97 %MaxLitNum:1 % 59.94/59.97 %MaxfuncDepth:5 % 59.94/59.97 %SharedTerms:8 % 59.94/59.97 %goalClause: 8 % 59.94/59.97 %singleGoalClaCount:1 % 59.94/59.97 [8]~E(f1(f1(f1(a4,a2),f1(a4,a2)),f1(a4,a3)),a3) % 59.94/59.97 [6]E(f1(x61,x61),a4) % 59.94/59.97 [7]E(f1(f1(a4,f1(f1(f1(x71,x72),x73),x71)),x73),x72) % 59.94/59.97 %EqnAxiom % 59.94/59.97 [1]E(x11,x11) % 59.94/59.97 [2]E(x22,x21)+~E(x21,x22) % 59.94/59.97 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 59.94/59.97 [4]~E(x41,x42)+E(f1(x41,x43),f1(x42,x43)) % 59.94/59.97 [5]~E(x51,x52)+E(f1(x53,x51),f1(x53,x52)) % 59.94/59.97 % 59.94/59.97 %------------------------------------------- % 59.94/59.99 cnf(9,plain, % 59.94/59.99 (E(a4,f1(x91,x91))), % 59.94/59.99 inference(scs_inference,[],[6,2])). % 59.94/59.99 cnf(10,plain, % 59.94/59.99 (E(x101,f1(f1(a4,f1(f1(f1(x102,x101),x103),x102)),x103))), % 59.94/59.99 inference(scs_inference,[],[7,2])). % 59.94/59.99 cnf(11,plain, % 59.94/59.99 (E(f1(f1(a4,f1(f1(f1(x111,a4),x112),x111)),x112),f1(x113,x113))), % 59.94/59.99 inference(scs_inference,[],[9,7,2,3])). % 59.94/59.99 cnf(14,plain, % 59.94/59.99 (E(f1(x141,x141),f1(x142,x142))), % 59.94/59.99 inference(scs_inference,[],[9,11,6,2,3])). % 59.94/59.99 cnf(15,plain, % 59.94/59.99 (~E(f1(f1(f1(a4,a2),f1(a4,a2)),f1(a4,a3)),f1(f1(a4,f1(f1(f1(x151,a3),x152),x151)),x152))), % 59.94/59.99 inference(scs_inference,[],[8,7,3])). % 59.94/59.99 cnf(17,plain, % 59.94/59.99 (~E(f1(f1(a4,a2),f1(a4,a2)),f1(a4,f1(f1(f1(x171,a3),f1(a4,a3)),x171)))), % 59.94/59.99 inference(scs_inference,[],[8,7,3,4])). % 59.94/59.99 cnf(18,plain, % 59.94/59.99 (E(f1(x181,f1(x182,x182)),f1(x181,a4))), % 59.94/59.99 inference(scs_inference,[],[6,5])). % 59.94/59.99 cnf(19,plain, % 59.94/59.99 (E(f1(f1(x191,x191),x192),f1(a4,x192))), % 59.94/59.99 inference(scs_inference,[],[6,5,4])). % 59.94/59.99 cnf(21,plain, % 59.94/59.99 (~E(a4,f1(a4,f1(f1(f1(x211,a3),f1(a4,a3)),x211)))), % 59.94/59.99 inference(scs_inference,[],[6,17,5,4,2,3])). % 59.94/59.99 cnf(23,plain, % 59.94/59.99 (E(f1(x231,f1(x232,x232)),f1(x231,f1(x233,x233)))), % 59.94/59.99 inference(scs_inference,[],[14,5])). % 59.94/59.99 cnf(24,plain, % 59.94/59.99 (E(f1(f1(x241,x241),x242),f1(f1(x243,x243),x242))), % 59.94/59.99 inference(scs_inference,[],[14,5,4])). % 59.94/59.99 cnf(25,plain, % 59.94/59.99 (~E(f1(a4,f1(f1(f1(x251,a3),f1(a4,a3)),x251)),a4)), % 59.94/59.99 inference(scs_inference,[],[14,21,5,4,2])). % 59.94/59.99 cnf(26,plain, % 59.94/59.99 (~E(f1(x261,x261),f1(a4,f1(f1(f1(x262,a3),f1(a4,a3)),x262)))), % 59.94/59.99 inference(scs_inference,[],[14,21,17,5,4,2,3])). % 59.94/59.99 cnf(28,plain, % 59.94/59.99 (E(f1(x281,f1(x282,f1(x283,x283))),f1(x281,f1(x282,a4)))), % 59.94/59.99 inference(scs_inference,[],[18,5])). % 59.94/59.99 cnf(29,plain, % 59.94/59.99 (E(f1(f1(x291,f1(x292,x292)),x293),f1(f1(x291,a4),x293))), % 59.94/59.99 inference(scs_inference,[],[18,5,4])). % 59.94/59.99 cnf(30,plain, % 59.94/59.99 (~E(f1(a4,f1(f1(f1(x301,a3),f1(a4,a3)),x301)),f1(x302,x302))), % 59.94/59.99 inference(scs_inference,[],[18,26,5,4,2])). % 59.94/59.99 cnf(31,plain, % 59.94/59.99 (~E(f1(a4,f1(a4,a3)),f1(f1(a4,f1(f1(f1(x311,a3),x312),x311)),x312))), % 59.94/59.99 inference(scs_inference,[],[18,19,26,15,5,4,2,3])). % 59.94/59.99 cnf(33,plain, % 59.94/59.99 (E(f1(x331,f1(x332,f1(x333,x333))),f1(x331,f1(x332,f1(x334,x334))))), % 59.94/59.99 inference(scs_inference,[],[23,5])). % 59.94/59.99 cnf(34,plain, % 59.94/59.99 (E(f1(f1(x341,f1(x342,x342)),x343),f1(f1(x341,f1(x344,x344)),x343))), % 59.94/59.99 inference(scs_inference,[],[23,5,4])). % 59.94/59.99 cnf(35,plain, % 59.94/59.99 (~E(f1(f1(a4,f1(f1(f1(x351,a3),x352),x351)),x352),f1(a4,f1(a4,a3)))), % 59.94/59.99 inference(scs_inference,[],[23,31,5,4,2])). % 59.94/59.99 cnf(36,plain, % 59.94/59.99 (~E(f1(f1(x361,x361),f1(x362,x362)),f1(a4,f1(f1(f1(x363,a3),f1(a4,a3)),x363)))), % 59.94/59.99 inference(scs_inference,[],[23,31,26,5,4,2,3])). % 59.94/59.99 cnf(39,plain, % 59.94/59.99 (E(f1(x391,f1(f1(x392,x392),x393)),f1(x391,f1(f1(x394,x394),x393)))), % 59.94/59.99 inference(scs_inference,[],[24,5])). % 59.94/59.99 cnf(40,plain, % 59.94/59.99 (E(f1(f1(f1(x401,x401),x402),x403),f1(f1(f1(x404,x404),x402),x403))), % 59.94/59.99 inference(scs_inference,[],[24,5,4])). % 59.94/59.99 cnf(41,plain, % 59.94/59.99 (~E(f1(a4,f1(f1(f1(x411,a3),f1(a4,a3)),x411)),f1(f1(x412,x412),f1(x413,x413)))), % 59.94/59.99 inference(scs_inference,[],[24,36,5,4,2])). % 59.94/59.99 cnf(42,plain, % 59.94/59.99 (~E(f1(a4,f1(f1(f1(f1(x421,x421),a3),f1(a4,a3)),a4)),f1(x422,x422))), % 59.94/59.99 inference(scs_inference,[],[24,28,30,36,5,4,2,3])). % 59.94/59.99 cnf(45,plain, % 59.94/59.99 (E(f1(x451,f1(f1(x452,f1(x453,x453)),x454)),f1(x451,f1(f1(x452,a4),x454)))), % 59.94/59.99 inference(scs_inference,[],[29,5])). % 59.94/59.99 cnf(46,plain, % 59.94/59.99 (E(f1(f1(f1(x461,f1(x462,x462)),x463),x464),f1(f1(f1(x461,a4),x463),x464))), % 59.94/59.99 inference(scs_inference,[],[29,5,4])). % 59.94/59.99 cnf(47,plain, % 59.94/59.99 (~E(f1(x471,x471),f1(a4,f1(f1(f1(f1(x472,x472),a3),f1(a4,a3)),a4)))), % 59.94/59.99 inference(scs_inference,[],[29,42,5,4,2])). % 59.94/59.99 cnf(48,plain, % 59.94/59.99 (~E(f1(f1(f1(x481,x481),a4),f1(x482,x482)),f1(a4,f1(f1(f1(x483,a3),f1(a4,a3)),x483)))), % 59.94/59.99 inference(scs_inference,[],[29,42,36,5,4,2,3])). % 59.94/59.99 cnf(52,plain, % 59.94/59.99 (E(f1(f1(x521,f1(x522,f1(x523,x523))),x524),f1(f1(x521,f1(x522,f1(x525,x525))),x524))), % 59.94/59.99 inference(scs_inference,[],[33,5,4])). % 59.94/59.99 cnf(53,plain, % 59.94/59.99 (~E(f1(a4,f1(f1(f1(x531,a3),f1(a4,a3)),x531)),f1(f1(f1(x532,x532),a4),f1(x533,x533)))), % 59.94/59.99 inference(scs_inference,[],[33,48,5,4,2])). % 59.94/59.99 cnf(54,plain, % 59.94/59.99 (~E(f1(a4,f1(f1(f1(f1(x541,x541),a3),f1(a4,a3)),f1(x542,x542))),a4)), % 59.94/59.99 inference(scs_inference,[],[33,25,48,5,4,2,3])). % 59.94/59.99 cnf(59,plain, % 59.94/59.99 (~E(a4,f1(a4,f1(f1(f1(f1(x591,x591),a3),f1(a4,a3)),f1(x592,x592))))), % 59.94/59.99 inference(scs_inference,[],[54,34,5,4,2])). % 59.94/59.99 cnf(60,plain, % 59.94/59.99 (~E(a4,f1(a4,f1(f1(f1(f1(x601,x601),a3),f1(a4,a3)),a4)))), % 59.94/59.99 inference(scs_inference,[],[6,54,34,47,5,4,2,3])). % 59.94/59.99 cnf(65,plain, % 59.94/59.99 (~E(f1(a4,f1(f1(x651,x651),a4)),f1(f1(x652,x652),f1(x653,x653)))), % 59.94/59.99 inference(scs_inference,[],[39,41,60,5,4,2,3])). % 59.94/59.99 cnf(70,plain, % 59.94/59.99 (~E(f1(f1(x701,x701),f1(x702,x702)),f1(a4,f1(f1(x703,x703),a4)))), % 59.94/59.99 inference(scs_inference,[],[65,40,5,4,2])). % 59.94/59.99 cnf(71,plain, % 59.94/59.99 (~E(f1(f1(f1(x711,x711),x712),f1(f1(x713,x713),x712)),f1(a4,f1(f1(f1(f1(x714,x714),a3),f1(a4,a3)),a4)))), % 59.94/59.99 inference(scs_inference,[],[65,40,47,5,4,2,3])). % 59.94/59.99 cnf(75,plain, % 59.94/59.99 (E(f1(x751,f1(f1(x752,x752),x753)),f1(x751,f1(a4,x753)))), % 59.94/59.99 inference(scs_inference,[],[71,19,2,5])). % 59.94/59.99 cnf(76,plain, % 59.94/59.99 (E(f1(f1(f1(x761,x761),x762),x763),f1(f1(a4,x762),x763))), % 59.94/59.99 inference(scs_inference,[],[71,19,2,5,4])). % 59.94/59.99 cnf(77,plain, % 59.94/59.99 (~E(a4,f1(a4,f1(f1(x771,x771),a4)))), % 59.94/59.99 inference(scs_inference,[],[6,70,71,19,2,5,4,3])). % 59.94/59.99 cnf(80,plain, % 59.94/59.99 (~E(f1(a4,f1(f1(x801,x801),a4)),a4)), % 59.94/59.99 inference(scs_inference,[],[77,2])). % 59.94/59.99 cnf(81,plain, % 59.94/59.99 (E(f1(x811,f1(x812,f1(f1(x813,x813),x814))),f1(x811,f1(x812,f1(a4,x814))))), % 59.94/59.99 inference(scs_inference,[],[77,75,2,5])). % 59.94/59.99 cnf(82,plain, % 59.94/59.99 (E(f1(f1(x821,f1(f1(x822,x822),x823)),x824),f1(f1(x821,f1(a4,x823)),x824))), % 59.94/59.99 inference(scs_inference,[],[77,75,2,5,4])). % 59.94/59.99 cnf(83,plain, % 59.94/59.99 (~E(a3,f1(a4,f1(a4,a3)))), % 59.94/59.99 inference(scs_inference,[],[7,77,75,35,2,5,4,3])). % 59.94/59.99 cnf(85,plain, % 59.94/59.99 (~E(f1(a4,f1(a4,a3)),a3)), % 59.94/59.99 inference(scs_inference,[],[83,2])). % 59.94/59.99 cnf(86,plain, % 59.94/59.99 (E(f1(x861,f1(f1(f1(x862,x862),x863),x864)),f1(x861,f1(f1(a4,x863),x864)))), % 59.94/59.99 inference(scs_inference,[],[83,76,2,5])). % 59.94/59.99 cnf(87,plain, % 59.94/59.99 (E(f1(f1(f1(f1(x871,x871),x872),x873),x874),f1(f1(f1(a4,x872),x873),x874))), % 59.94/59.99 inference(scs_inference,[],[83,76,2,5,4])). % 59.94/59.99 cnf(88,plain, % 59.94/59.99 (~E(f1(a4,f1(f1(f1(x881,x881),a4),a4)),a4)), % 59.94/59.99 inference(scs_inference,[],[83,80,76,45,2,5,4,3])). % 59.94/59.99 cnf(91,plain, % 59.94/59.99 (~E(a4,f1(a4,f1(f1(f1(x911,x911),a4),a4)))), % 59.94/59.99 inference(scs_inference,[],[88,2])). % 59.94/59.99 cnf(92,plain, % 59.94/59.99 (E(f1(x921,f1(x922,f1(x923,f1(x924,x924)))),f1(x921,f1(x922,f1(x923,a4))))), % 59.94/59.99 inference(scs_inference,[],[88,28,2,5])). % 59.94/59.99 cnf(93,plain, % 59.94/59.99 (E(f1(f1(x931,f1(x932,f1(x933,x933))),x934),f1(f1(x931,f1(x932,a4)),x934))), % 59.94/59.99 inference(scs_inference,[],[88,28,2,5,4])). % 59.94/59.99 cnf(94,plain, % 59.94/59.99 (~E(f1(f1(f1(x941,a4),f1(x941,f1(x942,x942))),f1(x943,x943)),f1(a4,f1(f1(x944,x944),a4)))), % 59.94/59.99 inference(scs_inference,[],[88,46,28,70,2,5,4,3])). % 59.94/59.99 cnf(97,plain, % 59.94/59.99 (~E(f1(a4,f1(f1(x971,x971),a4)),f1(f1(f1(x972,a4),f1(x972,f1(x973,x973))),f1(x974,x974)))), % 59.94/59.99 inference(scs_inference,[],[94,2])). % 59.94/59.99 cnf(98,plain, % 59.94/59.99 (E(f1(x981,a4),f1(x981,f1(x982,x982)))), % 59.94/59.99 inference(scs_inference,[],[94,9,2,5])). % 59.94/59.99 cnf(99,plain, % 59.94/59.99 (E(f1(a4,x991),f1(f1(x992,x992),x991))), % 59.94/59.99 inference(scs_inference,[],[94,9,2,5,4])). % 59.94/59.99 cnf(100,plain, % 59.94/60.00 (~E(f1(f1(f1(x1001,a4),f1(x1001,f1(x1002,x1002))),f1(f1(f1(x1003,x1003),x1004),f1(a4,x1004))),f1(a4,f1(f1(x1005,x1005),a4)))), % 59.94/60.00 inference(scs_inference,[],[94,81,9,2,5,4,3])). % 59.94/60.00 cnf(104,plain, % 59.94/60.00 (E(f1(x1041,f1(x1042,a4)),f1(x1041,f1(x1042,f1(x1043,x1043))))), % 59.94/60.00 inference(scs_inference,[],[98,100,2,5])). % 59.94/60.00 cnf(105,plain, % 59.94/60.00 (E(f1(f1(x1051,a4),x1052),f1(f1(x1051,f1(x1053,x1053)),x1052))), % 59.94/60.00 inference(scs_inference,[],[98,100,2,5,4])). % 59.94/60.00 cnf(106,plain, % 59.94/60.00 (~E(f1(f1(a4,f1(f1(f1(x1061,a3),a4),x1061)),f1(x1062,x1062)),f1(a4,f1(a4,a3)))), % 59.94/60.00 inference(scs_inference,[],[98,100,35,2,5,4,3])). % 59.94/60.00 cnf(110,plain, % 59.94/60.00 (E(f1(x1101,f1(a4,x1102)),f1(x1101,f1(f1(x1103,x1103),x1102)))), % 59.94/60.00 inference(scs_inference,[],[99,106,2,5])). % 59.94/60.00 cnf(111,plain, % 59.94/60.00 (E(f1(f1(a4,x1111),x1112),f1(f1(f1(x1113,x1113),x1111),x1112))), % 59.94/60.00 inference(scs_inference,[],[99,106,2,5,4])). % 59.94/60.00 cnf(112,plain, % 59.94/60.00 (~E(f1(f1(x1121,x1121),f1(a4,a3)),a3)), % 59.94/60.00 inference(scs_inference,[],[99,85,106,2,5,4,3])). % 59.94/60.00 cnf(114,plain, % 59.94/60.00 (~E(a3,f1(f1(x1141,x1141),f1(a4,a3)))), % 59.94/60.00 inference(scs_inference,[],[112,2])). % 59.94/60.00 cnf(115,plain, % 59.94/60.00 (E(f1(x1151,f1(x1152,f1(x1153,a4))),f1(x1151,f1(x1152,f1(x1153,f1(x1154,x1154)))))), % 59.94/60.00 inference(scs_inference,[],[112,104,2,5])). % 59.94/60.00 cnf(116,plain, % 59.94/60.00 (E(f1(f1(x1161,f1(x1162,a4)),x1163),f1(f1(x1161,f1(x1162,f1(x1164,x1164))),x1163))), % 59.94/60.00 inference(scs_inference,[],[112,104,2,5,4])). % 59.94/60.00 cnf(117,plain, % 59.94/60.00 (~E(f1(x1171,x1171),f1(a4,f1(f1(f1(f1(x1172,x1172),a3),f1(a4,a3)),f1(x1173,x1173))))), % 59.94/60.00 inference(scs_inference,[],[9,112,104,59,2,5,4,3])). % 59.94/60.00 cnf(118,plain, % 59.94/60.00 (~E(f1(a4,f1(f1(f1(f1(x1181,x1181),a3),f1(a4,a3)),f1(x1182,x1182))),f1(x1183,x1183))), % 59.94/60.00 inference(scs_inference,[],[117,2])). % 59.94/60.00 cnf(119,plain, % 59.94/60.00 (E(f1(x1191,f1(f1(x1192,a4),x1193)),f1(x1191,f1(f1(x1192,f1(x1194,x1194)),x1193)))), % 59.94/60.00 inference(scs_inference,[],[105,117,2,5])). % 59.94/60.00 cnf(120,plain, % 59.94/60.00 (E(f1(f1(f1(x1201,a4),x1202),x1203),f1(f1(f1(x1201,f1(x1204,x1204)),x1202),x1203))), % 59.94/60.00 inference(scs_inference,[],[105,117,2,5,4])). % 59.94/60.00 cnf(121,plain, % 59.94/60.00 (~E(f1(f1(a4,f1(f1(f1(x1211,a3),x1212),x1211)),x1212),f1(f1(x1213,x1213),f1(a4,a3)))), % 59.94/60.00 inference(scs_inference,[],[114,105,117,10,2,5,4,3])). % 59.94/60.00 cnf(123,plain, % 59.94/60.00 (~E(f1(f1(x1231,x1231),f1(a4,a3)),f1(f1(a4,f1(f1(f1(x1232,a3),x1233),x1232)),x1233))), % 59.94/60.00 inference(scs_inference,[],[121,2])). % 59.94/60.00 cnf(124,plain, % 59.94/60.00 (E(f1(x1241,f1(x1242,f1(a4,x1243))),f1(x1241,f1(x1242,f1(f1(x1244,x1244),x1243))))), % 59.94/60.00 inference(scs_inference,[],[110,121,2,5])). % 59.94/60.00 cnf(125,plain, % 59.94/60.00 (E(f1(f1(x1251,f1(a4,x1252)),x1253),f1(f1(x1251,f1(f1(x1254,x1254),x1252)),x1253))), % 59.94/60.00 inference(scs_inference,[],[110,121,2,5,4])). % 59.94/60.00 cnf(126,plain, % 59.94/60.00 (~E(f1(x1261,x1261),f1(a4,f1(f1(f1(x1262,x1262),a4),a4)))), % 59.94/60.00 inference(scs_inference,[],[9,110,91,121,2,5,4,3])). % 59.94/60.00 cnf(127,plain, % 59.94/60.00 (~E(f1(a4,f1(f1(f1(x1271,x1271),a4),a4)),f1(x1272,x1272))), % 59.94/60.00 inference(scs_inference,[],[126,2])). % 59.94/60.00 cnf(128,plain, % 59.94/60.00 (E(f1(x1281,f1(f1(a4,x1282),x1283)),f1(x1281,f1(f1(f1(x1284,x1284),x1282),x1283)))), % 59.94/60.00 inference(scs_inference,[],[111,126,2,5])). % 59.94/60.00 cnf(129,plain, % 59.94/60.00 (E(f1(f1(f1(a4,x1291),x1292),x1293),f1(f1(f1(f1(x1294,x1294),x1291),x1292),x1293))), % 59.94/60.00 inference(scs_inference,[],[111,126,2,5,4])). % 59.94/60.00 cnf(130,plain, % 59.94/60.00 (~E(f1(a4,f1(f1(f1(f1(x1301,x1301),a3),f1(a4,a3)),f1(f1(x1302,x1302),a4))),f1(x1303,x1303))), % 59.94/60.00 inference(scs_inference,[],[111,118,126,92,2,5,4,3])). % 59.94/60.00 cnf(133,plain, % 59.94/60.00 (~E(f1(x1331,x1331),f1(a4,f1(f1(f1(f1(x1332,x1332),a3),f1(a4,a3)),f1(f1(x1333,x1333),a4))))), % 59.94/60.00 inference(scs_inference,[],[130,2])). % 59.94/60.00 cnf(134,plain, % 59.94/60.00 (~E(f1(x1341,x1341),f1(a4,f1(f1(x1342,x1342),a4)))), % 59.94/60.00 inference(scs_inference,[],[9,130,77,2,3])). % 59.94/60.00 cnf(135,plain, % 59.94/60.00 (~E(f1(a4,f1(f1(x1351,x1351),a4)),f1(x1352,x1352))), % 59.94/60.00 inference(scs_inference,[],[134,2])). % 59.94/60.00 cnf(143,plain, % 59.94/60.00 (~E(f1(x1431,x1431),f1(a4,f1(f1(a4,f1(x1432,x1432)),a4)))), % 59.94/60.00 inference(scs_inference,[],[135,86,3,2])). % 59.94/60.00 cnf(144,plain, % 59.94/60.00 (~E(f1(f1(x1441,f1(x1442,f1(x1443,x1443))),f1(x1441,f1(x1442,a4))),f1(a4,f1(f1(a4,f1(x1444,x1444)),a4)))), % 59.94/60.00 inference(scs_inference,[],[143,116,3])). % 59.94/60.00 cnf(148,plain, % 59.94/60.00 (~E(f1(a4,f1(f1(f1(x1481,x1481),f1(x1482,x1482)),a4)),f1(x1483,x1483))), % 59.94/60.00 inference(scs_inference,[],[127,119,144,2,3])). % 59.94/60.00 cnf(150,plain, % 59.94/60.00 (~E(f1(x1501,x1501),f1(a4,f1(f1(f1(x1502,x1502),f1(x1503,x1503)),a4)))), % 59.94/60.00 inference(scs_inference,[],[148,2])). % 59.94/60.00 cnf(151,plain, % 59.94/60.00 (~E(f1(a4,f1(f1(f1(f1(x1511,a4),a3),f1(a4,a3)),f1(x1511,f1(x1512,x1512)))),f1(f1(f1(x1513,x1513),a4),f1(x1514,x1514)))), % 59.94/60.00 inference(scs_inference,[],[148,53,115,2,3])). % 59.94/60.00 cnf(154,plain, % 59.94/60.00 (~E(f1(f1(f1(x1541,x1541),a4),f1(x1542,x1542)),f1(a4,f1(f1(f1(f1(x1543,a4),a3),f1(a4,a3)),f1(x1543,f1(x1544,x1544)))))), % 59.94/60.00 inference(scs_inference,[],[151,2])). % 59.94/60.00 cnf(155,plain, % 59.94/60.00 (~E(f1(a4,f1(f1(f1(x1551,x1551),a4),a4)),f1(f1(f1(x1552,a4),f1(x1552,f1(x1553,x1553))),f1(x1554,x1554)))), % 59.94/60.00 inference(scs_inference,[],[97,128,151,2,3])). % 59.94/60.00 cnf(158,plain, % 59.94/60.00 (~E(f1(f1(f1(x1581,a4),f1(x1581,f1(x1582,x1582))),f1(x1583,x1583)),f1(a4,f1(f1(f1(x1584,x1584),a4),a4)))), % 59.94/60.00 inference(scs_inference,[],[155,2])). % 59.94/60.00 cnf(159,plain, % 59.94/60.00 (~E(f1(f1(f1(x1591,f1(x1592,x1592)),x1593),f1(f1(x1591,a4),x1593)),f1(a4,f1(f1(f1(x1594,x1594),f1(x1595,x1595)),a4)))), % 59.94/60.00 inference(scs_inference,[],[150,120,155,2,3])). % 59.94/60.00 cnf(163,plain, % 59.94/60.00 (~E(f1(f1(f1(a4,f1(x1631,x1631)),a4),f1(x1632,x1632)),f1(a4,f1(f1(f1(f1(x1633,a4),a3),f1(a4,a3)),f1(x1633,f1(x1634,x1634)))))), % 59.94/60.00 inference(scs_inference,[],[87,154,159,2,3])). % 59.94/60.00 cnf(166,plain, % 59.94/60.00 (~E(f1(a4,f1(f1(f1(f1(x1661,a4),a3),f1(a4,a3)),f1(x1661,f1(x1662,x1662)))),f1(f1(f1(a4,f1(x1663,x1663)),a4),f1(x1664,x1664)))), % 59.94/60.00 inference(scs_inference,[],[163,2])). % 59.94/60.00 cnf(167,plain, % 59.94/60.00 (~E(f1(f1(x1671,x1671),a4),f1(a4,f1(f1(f1(f1(x1672,x1672),a3),f1(a4,a3)),f1(f1(x1673,x1673),a4))))), % 59.94/60.00 inference(scs_inference,[],[133,163,18,2,3])). % 59.94/60.00 cnf(170,plain, % 59.94/60.00 (~E(f1(a4,f1(f1(f1(f1(x1701,x1701),a3),f1(a4,a3)),f1(f1(x1702,x1702),a4))),f1(f1(x1703,x1703),a4))), % 59.94/60.00 inference(scs_inference,[],[167,2])). % 59.94/60.00 cnf(171,plain, % 59.94/60.00 (~E(f1(f1(f1(x1711,f1(x1712,x1712)),f1(x1711,a4)),a4),f1(a4,f1(f1(f1(f1(x1713,x1713),a3),f1(a4,a3)),f1(f1(x1714,x1714),a4))))), % 59.94/60.00 inference(scs_inference,[],[93,167,2,3])). % 59.94/60.00 cnf(175,plain, % 59.94/60.00 (~E(f1(f1(f1(a4,a4),f1(f1(x1751,x1751),f1(x1752,x1752))),f1(x1753,x1753)),f1(a4,f1(f1(f1(x1754,x1754),a4),a4)))), % 59.94/60.00 inference(scs_inference,[],[125,158,171,2,3])). % 59.94/60.00 cnf(178,plain, % 59.94/60.00 (~E(f1(a4,f1(f1(f1(x1781,x1781),a4),a4)),f1(f1(f1(a4,a4),f1(f1(x1782,x1782),f1(x1783,x1783))),f1(x1784,x1784)))), % 59.94/60.00 inference(scs_inference,[],[175,2])). % 59.94/60.00 cnf(179,plain, % 59.94/60.00 (~E(f1(a4,f1(f1(f1(f1(a4,a4),a3),f1(a4,a3)),f1(f1(x1791,x1791),f1(x1792,x1792)))),f1(f1(f1(a4,f1(x1793,x1793)),a4),f1(x1794,x1794)))), % 59.94/60.00 inference(scs_inference,[],[124,175,166,2,3])). % 59.94/60.00 cnf(183,plain, % 59.94/60.00 (~E(f1(a4,f1(f1(f1(f1(x1831,x1831),a3),f1(a4,a3)),f1(a4,a4))),f1(f1(x1832,x1832),a4))), % 59.94/60.00 inference(scs_inference,[],[170,179,81,2,3])). % 59.94/60.00 cnf(185,plain, % 59.94/60.00 (~E(f1(f1(x1851,x1851),a4),f1(a4,f1(f1(f1(f1(x1852,x1852),a3),f1(a4,a3)),f1(a4,a4))))), % 59.94/60.00 inference(scs_inference,[],[183,2])). % 59.94/60.00 cnf(186,plain, % 59.94/60.00 (~E(f1(a4,f1(f1(f1(f1(x1861,x1861),a3),f1(a4,a3)),f1(a4,f1(x1862,x1862)))),f1(f1(x1863,x1863),a4))), % 59.94/60.00 inference(scs_inference,[],[183,115,2,3])). % 59.94/60.00 cnf(188,plain, % 59.94/60.00 (~E(f1(f1(x1881,x1881),a4),f1(a4,f1(f1(f1(f1(x1882,x1882),a3),f1(a4,a3)),f1(a4,f1(x1883,x1883)))))), % 59.94/60.00 inference(scs_inference,[],[186,2])). % 59.94/60.00 cnf(189,plain, % 59.94/60.00 (~E(f1(f1(f1(f1(x1891,x1891),x1892),f1(a4,x1892)),a4),f1(a4,f1(f1(f1(f1(x1893,x1893),a3),f1(a4,a3)),f1(a4,a4))))), % 59.94/60.00 inference(scs_inference,[],[185,186,129,2,3])). % 59.94/60.00 cnf(192,plain, % 59.94/60.00 (~E(f1(a4,f1(f1(f1(f1(x1921,x1921),a3),f1(a4,a3)),f1(a4,a4))),f1(f1(f1(f1(x1922,x1922),x1923),f1(a4,x1923)),a4))), % 59.94/60.00 inference(scs_inference,[],[189,2])). % 59.94/60.00 cnf(193,plain, % 59.94/60.00 (~E(f1(f1(f1(f1(x1931,x1931),f1(x1932,x1932)),f1(a4,f1(x1933,x1933))),a4),f1(a4,f1(f1(f1(f1(x1934,x1934),a3),f1(a4,a3)),f1(a4,a4))))), % 59.94/60.00 inference(scs_inference,[],[189,52,2,3])). % 59.94/60.00 cnf(197,plain, % 59.94/60.00 (~E(f1(f1(f1(f1(x1971,x1971),x1972),f1(a4,x1972)),a4),f1(a4,f1(f1(f1(f1(x1973,x1973),a3),f1(a4,a3)),f1(a4,f1(x1974,x1974)))))), % 59.94/60.00 inference(scs_inference,[],[188,193,82,2,3])). % 59.94/60.00 cnf(201,plain, % 59.94/60.00 (~E(f1(a4,f1(f1(f1(f1(x2011,x2011),a3),f1(a4,a3)),f1(f1(x2012,x2012),a4))),f1(f1(f1(f1(x2013,x2013),x2014),f1(a4,x2014)),a4))), % 59.94/60.00 inference(scs_inference,[],[192,197,124,2,3])). % 59.94/60.00 cnf(204,plain, % 59.94/60.00 (~E(f1(a4,f1(f1(a4,a4),a4)),f1(f1(f1(a4,a4),f1(f1(x2041,x2041),f1(x2042,x2042))),f1(x2043,x2043)))), % 59.94/60.00 inference(scs_inference,[],[178,201,86,2,3])). % 59.94/60.00 cnf(207,plain, % 59.94/60.00 (~E(f1(a4,f1(f1(a4,f1(x2071,x2071)),a4)),f1(f1(f1(a4,a4),f1(f1(x2072,x2072),f1(x2073,x2073))),f1(x2074,x2074)))), % 59.94/60.00 inference(scs_inference,[],[204,119,2,3])). % 59.94/60.00 cnf(210,plain, % 59.94/60.00 ($false), % 59.94/60.00 inference(scs_inference,[],[207,123,87,76,2,3]), % 59.94/60.00 ['proof']). % 59.94/60.00 % SZS output end Proof % 59.94/60.00 % Total time :59.330000s %------------------------------------------------------------------------------