%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP569-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:57 EDT 2024 % Result : Unsatisfiable 278.18s 278.28s % Output : CNFRefutation 278.31s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : GRP569-1 : TPTP v8.2.0. Released v2.6.0. % 0.00/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n028.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Thu Jun 20 09:28:24 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.56 start to proof:theBenchmark % 278.16/278.24 %------------------------------------------- % 278.16/278.24 % File :CSE---1.7 % 278.16/278.24 % Problem :theBenchmark % 278.16/278.24 % Transform :cnf % 278.16/278.24 % Format :tptp:raw % 278.16/278.24 % Command :java -jar mcs_scs.jar %d %s % 278.16/278.24 % 278.16/278.24 % Result :Theorem 277.490000s % 278.16/278.24 % Output :CNFRefutation 277.490000s % 278.16/278.24 %------------------------------------------- % 278.18/278.28 %-------------------------------------------------------------------------- % 278.18/278.28 % File : GRP569-1 : TPTP v8.2.0. Released v2.6.0. % 278.18/278.28 % Domain : Group Theory (Abelian) % 278.18/278.28 % Problem : Axiom for Abelian group theory, in double div and id, part 1 % 278.18/278.28 % Version : [McC93] (equality) axioms. % 278.18/278.28 % English : % 278.18/278.28 % 278.18/278.28 % Refs : [McC93] McCune (1993), Single Axioms for Groups and Abelian Gr % 278.18/278.28 % Source : [TPTP] % 278.18/278.28 % Names : % 278.18/278.28 % 278.18/278.28 % Status : Unsatisfiable % 278.18/278.28 % Rating : 0.00 v7.4.0, 0.04 v7.3.0, 0.00 v7.0.0, 0.05 v6.3.0, 0.06 v6.2.0, 0.07 v6.1.0, 0.06 v6.0.0, 0.10 v5.5.0, 0.11 v5.4.0, 0.00 v2.6.0 % 278.18/278.28 % Syntax : Number of clauses : 5 ( 5 unt; 0 nHn; 1 RR) % 278.18/278.28 % Number of literals : 5 ( 5 equ; 1 neg) % 278.18/278.28 % Maximal clause size : 1 ( 1 avg) % 278.18/278.28 % Maximal term depth : 6 ( 2 avg) % 278.18/278.28 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 278.18/278.28 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty) % 278.18/278.28 % Number of variables : 7 ( 0 sgn) % 278.18/278.28 % SPC : CNF_UNS_RFO_PEQ_UEQ % 278.18/278.28 % 278.18/278.28 % Comments : A UEQ part of GRP100-1 % 278.18/278.28 %-------------------------------------------------------------------------- % 278.18/278.28 cnf(single_axiom,axiom, % 278.18/278.28 double_divide(double_divide(A,double_divide(double_divide(B,double_divide(A,C)),double_divide(C,identity))),double_divide(identity,identity)) = B ). % 278.18/278.28 % 278.18/278.28 cnf(multiply,axiom, % 278.18/278.28 multiply(A,B) = double_divide(double_divide(B,A),identity) ). % 278.18/278.28 % 278.18/278.28 cnf(inverse,axiom, % 278.18/278.28 inverse(A) = double_divide(A,identity) ). % 278.18/278.28 % 278.18/278.28 cnf(identity,axiom, % 278.18/278.28 identity = double_divide(A,inverse(A)) ). % 278.18/278.28 % 278.18/278.28 cnf(prove_these_axioms_1,negated_conjecture, % 278.18/278.28 multiply(inverse(a1),a1) != identity ). % 278.18/278.28 % 278.18/278.28 %-------------------------------------------------------------------------- % 278.18/278.28 %------------------------------------------- % 278.18/278.28 % Proof found % 278.18/278.28 % SZS status Theorem for theBenchmark % 278.18/278.28 % SZS output start Proof % 278.18/278.32 %ClaNum:8(EqnAxiom:5) % 278.18/278.32 %VarNum:8(SingletonVarNum:4) % 278.18/278.32 %MaxLitNum:1 % 278.18/278.32 %MaxfuncDepth:3 % 278.18/278.32 %SharedTerms:7 % 278.18/278.32 %goalClause: 8 % 278.18/278.32 %singleGoalClaCount:1 % 278.18/278.32 [8]~E(f2(f2(a3,f2(a3,a1)),a1),a1) % 278.18/278.32 [6]E(f2(x61,f2(x61,a1)),a1) % 278.18/278.32 [7]E(f2(f2(x71,f2(f2(x72,f2(x71,x73)),f2(x73,a1))),f2(a1,a1)),x72) % 278.18/278.32 %EqnAxiom % 278.18/278.32 [1]E(x11,x11) % 278.18/278.32 [2]E(x22,x21)+~E(x21,x22) % 278.18/278.32 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 278.18/278.32 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 278.18/278.32 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 278.18/278.32 % 278.18/278.32 %------------------------------------------- % 278.27/278.38 cnf(9,plain, % 278.27/278.38 (E(x91,f2(f2(x92,f2(f2(x91,f2(x92,x93)),f2(x93,a1))),f2(a1,a1)))), % 278.27/278.38 inference(scs_inference,[],[7,2])). % 278.27/278.38 cnf(10,plain, % 278.27/278.38 (~E(f2(f2(a3,f2(a3,a1)),a1),f2(x101,f2(x101,a1)))), % 278.27/278.38 inference(scs_inference,[],[8,7,6,2,3])). % 278.27/278.38 cnf(11,plain, % 278.27/278.38 (~E(a1,f2(f2(a3,f2(a3,a1)),a1))), % 278.27/278.38 inference(scs_inference,[],[8,7,6,2,3,5])). % 278.27/278.38 cnf(12,plain, % 278.27/278.38 (E(a1,f2(x121,f2(x121,a1)))), % 278.27/278.38 inference(scs_inference,[],[6,2])). % 278.27/278.38 cnf(13,plain, % 278.27/278.38 (E(a1,f2(f2(x131,f2(f2(f2(x132,f2(x132,a1)),f2(x131,x133)),f2(x133,a1))),f2(a1,a1)))), % 278.27/278.38 inference(scs_inference,[],[9,12,3])). % 278.27/278.38 cnf(15,plain, % 278.27/278.38 (E(f2(f2(x151,f2(f2(f2(x152,f2(x152,a1)),f2(x151,x153)),f2(x153,a1))),f2(a1,a1)),a1)), % 278.27/278.38 inference(scs_inference,[],[13,2])). % 278.27/278.38 cnf(16,plain, % 278.27/278.38 (E(f2(x161,f2(x161,a1)),f2(f2(x162,f2(f2(a1,f2(x162,x163)),f2(x163,a1))),f2(a1,a1)))), % 278.27/278.38 inference(scs_inference,[],[6,9,3])). % 278.27/278.38 cnf(18,plain, % 278.27/278.38 (E(f2(f2(x181,f2(f2(a1,f2(x181,x182)),f2(x182,a1))),f2(a1,a1)),f2(x183,f2(x183,a1)))), % 278.27/278.38 inference(scs_inference,[],[6,9,3,2])). % 278.27/278.38 cnf(19,plain, % 278.27/278.38 (~E(f2(f2(a3,f2(a3,a1)),a1),f2(f2(x191,f2(f2(a1,f2(x191,x192)),f2(x192,a1))),f2(a1,a1)))), % 278.27/278.38 inference(scs_inference,[],[18,10,3])). % 278.27/278.38 cnf(21,plain, % 278.27/278.38 (~E(a1,f2(f2(x211,f2(f2(f2(f2(a3,f2(a3,a1)),a1),f2(x211,x212)),f2(x212,a1))),f2(a1,a1)))), % 278.27/278.38 inference(scs_inference,[],[11,7,3])). % 278.27/278.38 cnf(23,plain, % 278.27/278.38 (E(f2(x231,f2(x231,a1)),f2(f2(x232,f2(f2(f2(x233,f2(x233,a1)),f2(x232,x234)),f2(x234,a1))),f2(a1,a1)))), % 278.27/278.38 inference(scs_inference,[],[6,13,3])). % 278.27/278.38 cnf(25,plain, % 278.27/278.38 (E(f2(f2(x251,f2(x251,a1)),x252),f2(a1,x252))), % 278.27/278.38 inference(scs_inference,[],[6,4])). % 278.27/278.38 cnf(26,plain, % 278.27/278.38 (E(f2(x261,f2(x262,f2(x262,a1))),f2(x261,a1))), % 278.27/278.38 inference(scs_inference,[],[6,4,5])). % 278.27/278.38 cnf(28,plain, % 278.27/278.38 (~E(f2(x281,f2(x281,a1)),f2(f2(a3,f2(a3,a1)),a1))), % 278.27/278.38 inference(scs_inference,[],[6,19,12,11,4,5,2,3])). % 278.27/278.38 cnf(29,plain, % 278.27/278.38 (E(f2(f2(f2(x291,f2(x291,a1)),x292),x293),f2(f2(a1,x292),x293))), % 278.27/278.38 inference(scs_inference,[],[25,4])). % 278.27/278.38 cnf(30,plain, % 278.27/278.38 (E(f2(x301,f2(f2(x302,f2(x302,a1)),x303)),f2(x301,f2(a1,x303)))), % 278.27/278.38 inference(scs_inference,[],[25,4,5])). % 278.27/278.38 cnf(32,plain, % 278.27/278.38 (E(f2(f2(x321,f2(x321,a1)),f2(x322,f2(x322,a1))),f2(a1,a1))), % 278.27/278.38 inference(scs_inference,[],[25,26,21,4,5,2,3])). % 278.27/278.38 cnf(37,plain, % 278.27/278.38 (~E(f2(f2(x371,f2(x371,a1)),f2(a1,a1)),f2(f2(a3,f2(a3,a1)),a1))), % 278.27/278.38 inference(scs_inference,[],[32,28,30,4,5,3])). % 278.27/278.38 cnf(40,plain, % 278.27/278.38 (E(f2(f2(f2(x401,f2(f2(f2(x402,f2(x402,a1)),f2(x401,x403)),f2(x403,a1))),f2(a1,a1)),x404),f2(a1,x404))), % 278.27/278.38 inference(scs_inference,[],[15,4])). % 278.27/278.38 cnf(42,plain, % 278.27/278.38 (~E(f2(f2(a3,f2(a3,a1)),a1),f2(f2(x421,f2(x421,a1)),f2(a1,a1)))), % 278.27/278.38 inference(scs_inference,[],[37,15,4,5,2])). % 278.27/278.38 cnf(45,plain, % 278.27/278.38 (E(f2(a1,x451),f2(f2(x452,f2(x452,a1)),x451))), % 278.27/278.38 inference(scs_inference,[],[12,4])). % 278.27/278.38 cnf(46,plain, % 278.27/278.38 (E(f2(x461,a1),f2(x461,f2(x462,f2(x462,a1))))), % 278.27/278.38 inference(scs_inference,[],[12,4,5])). % 278.27/278.38 cnf(47,plain, % 278.27/278.38 (E(f2(f2(a1,x471),x472),f2(f2(f2(x473,f2(x473,a1)),x471),x472))), % 278.27/278.38 inference(scs_inference,[],[45,4])). % 278.27/278.38 cnf(48,plain, % 278.27/278.38 (E(f2(x481,f2(a1,x482)),f2(x481,f2(f2(x483,f2(x483,a1)),x482)))), % 278.27/278.38 inference(scs_inference,[],[45,4,5])). % 278.27/278.38 cnf(49,plain, % 278.27/278.38 (~E(f2(f2(a3,f2(a3,a1)),f2(x491,f2(x491,a1))),f2(f2(x492,f2(x492,a1)),f2(a1,a1)))), % 278.27/278.38 inference(scs_inference,[],[45,46,42,4,5,3])). % 278.27/278.38 cnf(51,plain, % 278.27/278.38 (~E(f2(f2(x511,f2(x511,a1)),f2(a1,a1)),f2(f2(a3,f2(a3,a1)),f2(x512,f2(x512,a1))))), % 278.27/278.38 inference(scs_inference,[],[45,46,42,4,5,3,2])). % 278.27/278.38 cnf(53,plain, % 278.27/278.38 (E(f2(x531,f2(x532,a1)),f2(x531,f2(x532,f2(x533,f2(x533,a1)))))), % 278.27/278.38 inference(scs_inference,[],[46,4,5])). % 278.27/278.38 cnf(56,plain, % 278.27/278.38 (E(f2(x561,x562),f2(f2(f2(x563,f2(f2(x561,f2(x563,x564)),f2(x564,a1))),f2(a1,a1)),x562))), % 278.27/278.38 inference(scs_inference,[],[9,4])). % 278.27/278.38 cnf(57,plain, % 278.27/278.38 (E(f2(x571,x572),f2(x571,f2(f2(x573,f2(f2(x572,f2(x573,x574)),f2(x574,a1))),f2(a1,a1))))), % 278.27/278.38 inference(scs_inference,[],[9,4,5])). % 278.27/278.38 cnf(58,plain, % 278.27/278.38 (~E(f2(f2(a3,f2(a3,a1)),f2(f2(x581,f2(x581,a1)),f2(a1,a1))),f2(f2(x582,f2(x582,a1)),f2(a1,a1)))), % 278.27/278.38 inference(scs_inference,[],[49,48,9,4,5,3])). % 278.27/278.38 cnf(61,plain, % 278.27/278.38 (E(f2(f2(f2(x611,f2(f2(x612,f2(x611,x613)),f2(x613,a1))),f2(a1,a1)),x614),f2(x612,x614))), % 278.27/278.38 inference(scs_inference,[],[7,4])). % 278.27/278.38 cnf(63,plain, % 278.27/278.38 (~E(f2(f2(x631,f2(x631,a1)),f2(a1,a1)),f2(f2(a3,f2(a3,a1)),f2(f2(x632,f2(x632,a1)),f2(a1,a1))))), % 278.27/278.38 inference(scs_inference,[],[58,7,4,5,2])). % 278.27/278.38 cnf(64,plain, % 278.27/278.38 (~E(f2(f2(f2(x641,f2(x641,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(a3,f2(a3,a1)),f2(x642,f2(x642,a1))))), % 278.27/278.38 inference(scs_inference,[],[51,58,47,7,4,5,2,3])). % 278.27/278.38 cnf(67,plain, % 278.27/278.38 (~E(f2(f2(a3,f2(a3,a1)),f2(x671,f2(x671,a1))),f2(f2(f2(x672,f2(x672,a1)),f2(a1,a1)),f2(a1,a1)))), % 278.27/278.38 inference(scs_inference,[],[64,2])). % 278.27/278.38 cnf(68,plain, % 278.27/278.38 (~E(f2(f2(f2(x681,f2(f2(f2(a3,f2(a3,a1)),f2(x681,x682)),f2(x682,a1))),f2(a1,a1)),a1),a1)), % 278.27/278.38 inference(scs_inference,[],[56,64,8,2,3])). % 278.27/278.38 cnf(71,plain, % 278.27/278.38 (~E(f2(a1,a1),a1)), % 278.27/278.38 inference(scs_inference,[],[40,68,2,3])). % 278.27/278.38 cnf(73,plain, % 278.27/278.38 (~E(a1,f2(a1,a1))), % 278.27/278.38 inference(scs_inference,[],[71,2])). % 278.27/278.38 cnf(74,plain, % 278.27/278.38 (~E(f2(a1,f2(f2(x741,f2(f2(a1,f2(x741,x742)),f2(x742,a1))),f2(a1,a1))),a1)), % 278.27/278.38 inference(scs_inference,[],[71,57,2,3])). % 278.27/278.38 cnf(77,plain, % 278.27/278.38 (~E(f2(f2(f2(x771,f2(x771,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(a3,f2(a3,a1)),f2(f2(x772,f2(x772,a1)),f2(a1,a1))))), % 278.27/278.38 inference(scs_inference,[],[63,74,47,2,3])). % 278.27/278.38 cnf(80,plain, % 278.27/278.38 (~E(f2(f2(a3,f2(a3,a1)),f2(f2(x801,f2(x801,a1)),f2(a1,a1))),f2(f2(f2(x802,f2(x802,a1)),f2(a1,a1)),f2(a1,a1)))), % 278.27/278.38 inference(scs_inference,[],[77,2])). % 278.27/278.38 cnf(81,plain, % 278.27/278.38 (~E(f2(f2(x811,f2(f2(f2(x812,f2(x812,a1)),f2(x811,x813)),f2(x813,a1))),f2(a1,a1)),f2(a1,a1))), % 278.27/278.38 inference(scs_inference,[],[73,77,13,2,3])). % 278.27/278.38 cnf(83,plain, % 278.27/278.38 (~E(f2(x831,f2(x831,a1)),f2(a1,a1))), % 278.27/278.38 inference(scs_inference,[],[7,81,2,3])). % 278.27/278.38 cnf(85,plain, % 278.27/278.38 (~E(f2(a1,a1),f2(x851,f2(x851,a1)))), % 278.27/278.38 inference(scs_inference,[],[83,2])). % 278.27/278.38 cnf(86,plain, % 278.27/278.38 (~E(f2(f2(x861,f2(f2(a1,f2(x861,x862)),f2(x862,a1))),f2(a1,a1)),f2(a1,a1))), % 278.27/278.38 inference(scs_inference,[],[83,16,2,3])). % 278.27/278.38 cnf(88,plain, % 278.27/278.38 (~E(f2(a1,a1),f2(f2(x881,f2(f2(a1,f2(x881,x882)),f2(x882,a1))),f2(a1,a1)))), % 278.27/278.38 inference(scs_inference,[],[86,2])). % 278.27/278.38 cnf(89,plain, % 278.27/278.38 (~E(f2(f2(f2(x891,f2(f2(a1,f2(x891,x892)),f2(x892,a1))),f2(a1,a1)),a1),f2(x893,f2(x893,a1)))), % 278.27/278.38 inference(scs_inference,[],[85,86,56,2,3])). % 278.27/278.38 cnf(92,plain, % 278.27/278.38 (~E(f2(a1,f2(f2(x921,f2(f2(a1,f2(x921,x922)),f2(x922,a1))),f2(a1,a1))),f2(x923,f2(x923,a1)))), % 278.27/278.38 inference(scs_inference,[],[89,85,57,2,3])). % 278.27/278.38 cnf(95,plain, % 278.27/278.38 (~E(f2(f2(x951,f2(x951,a1)),a1),f2(f2(x952,f2(f2(a1,f2(x952,x953)),f2(x953,a1))),f2(a1,a1)))), % 278.27/278.38 inference(scs_inference,[],[88,92,45,2,3])). % 278.27/278.38 cnf(97,plain, % 278.27/278.38 (~E(f2(f2(x971,f2(f2(a1,f2(x971,x972)),f2(x972,a1))),f2(a1,a1)),f2(f2(x973,f2(x973,a1)),a1))), % 278.27/278.38 inference(scs_inference,[],[95,2])). % 278.27/278.38 cnf(98,plain, % 278.27/278.38 (~E(f2(f2(f2(x981,f2(f2(a1,f2(x981,x982)),f2(x982,a1))),f2(a1,a1)),a1),a1)), % 278.27/278.38 inference(scs_inference,[],[95,71,56,2,3])). % 278.27/278.38 cnf(101,plain, % 278.27/278.38 (~E(f2(x1011,f2(x1011,a1)),f2(f2(x1012,f2(x1012,a1)),a1))), % 278.27/278.38 inference(scs_inference,[],[98,97,18,2,3])). % 278.27/278.38 cnf(103,plain, % 278.27/278.38 (~E(f2(f2(x1031,f2(x1031,a1)),a1),f2(x1032,f2(x1032,a1)))), % 278.27/278.38 inference(scs_inference,[],[101,2])). % 278.27/278.38 cnf(104,plain, % 278.27/278.38 (~E(f2(f2(x1041,f2(f2(f2(a1,a1),f2(x1041,x1042)),f2(x1042,a1))),f2(a1,a1)),f2(x1043,f2(x1043,a1)))), % 278.27/278.38 inference(scs_inference,[],[9,101,85,2,3])). % 278.27/278.38 cnf(106,plain, % 278.27/278.38 (~E(f2(x1061,f2(x1061,a1)),f2(f2(x1062,f2(f2(f2(a1,a1),f2(x1062,x1063)),f2(x1063,a1))),f2(a1,a1)))), % 278.27/278.38 inference(scs_inference,[],[104,2])). % 278.27/278.38 cnf(107,plain, % 278.27/278.38 (~E(f2(a1,a1),f2(f2(f2(x1071,f2(x1071,a1)),f2(a1,a1)),f2(a1,a1)))), % 278.27/278.38 inference(scs_inference,[],[104,67,32,2,3])). % 278.27/278.38 cnf(109,plain, % 278.27/278.38 (~E(f2(f2(f2(x1091,f2(x1091,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1))), % 278.27/278.38 inference(scs_inference,[],[107,2])). % 278.27/278.38 cnf(110,plain, % 278.27/278.38 (~E(f2(f2(x1101,f2(f2(f2(a1,a1),f2(x1101,x1102)),f2(x1102,a1))),f2(a1,a1)),f2(f2(f2(x1103,f2(x1103,a1)),f2(a1,a1)),f2(a1,a1)))), % 278.27/278.38 inference(scs_inference,[],[9,107,2,3])). % 278.27/278.38 cnf(113,plain, % 278.27/278.38 (~E(f2(f2(a1,f2(a1,a1)),f2(a1,a1)),f2(a1,a1))), % 278.27/278.38 inference(scs_inference,[],[109,29,110,2,3])). % 278.27/278.38 cnf(115,plain, % 278.27/278.38 (~E(f2(a1,a1),f2(f2(a1,f2(a1,a1)),f2(a1,a1)))), % 278.27/278.38 inference(scs_inference,[],[113,2])). % 278.27/278.38 cnf(116,plain, % 278.27/278.38 (~E(f2(f2(x1161,f2(f2(f2(f2(a1,f2(a1,a1)),f2(a1,a1)),f2(x1161,x1162)),f2(x1162,a1))),f2(a1,a1)),f2(a1,a1))), % 278.31/278.38 inference(scs_inference,[],[9,113,2,3])). % 278.31/278.38 cnf(119,plain, % 278.31/278.38 (~E(f2(f2(x1191,f2(f2(f2(a1,a1),f2(x1191,x1192)),f2(x1192,a1))),f2(a1,a1)),f2(f2(a1,f2(a1,a1)),f2(a1,a1)))), % 278.31/278.38 inference(scs_inference,[],[9,115,116,2,3])). % 278.31/278.38 cnf(122,plain, % 278.31/278.38 (~E(f2(f2(x1221,f2(f2(f2(a1,a1),f2(x1221,x1222)),f2(x1222,a1))),f2(a1,a1)),a1)), % 278.31/278.38 inference(scs_inference,[],[9,119,71,2,3])). % 278.31/278.38 cnf(125,plain, % 278.31/278.38 (~E(f2(f2(x1251,f2(x1251,a1)),f2(a1,a1)),f2(f2(x1252,f2(f2(f2(a1,a1),f2(x1252,x1253)),f2(x1253,a1))),f2(a1,a1)))), % 278.31/278.38 inference(scs_inference,[],[122,106,30,2,3])). % 278.31/278.38 cnf(129,plain, % 278.31/278.38 (~E(f2(f2(f2(x1291,f2(x1291,a1)),f2(a1,a1)),a1),f2(x1292,f2(x1292,a1)))), % 278.31/278.38 inference(scs_inference,[],[103,125,47,2,3])). % 278.31/278.38 cnf(132,plain, % 278.31/278.38 (~E(f2(x1321,f2(x1321,a1)),f2(f2(f2(x1322,f2(x1322,a1)),f2(a1,a1)),a1))), % 278.31/278.38 inference(scs_inference,[],[129,2])). % 278.31/278.38 cnf(133,plain, % 278.31/278.38 (E(f2(a1,x1331),f2(f2(f2(x1332,f2(f2(f2(x1333,f2(x1333,a1)),f2(x1332,x1334)),f2(x1334,a1))),f2(a1,a1)),x1331))), % 278.31/278.38 inference(scs_inference,[],[13,4])). % 278.31/278.38 cnf(135,plain, % 278.31/278.38 (~E(f2(f2(f2(x1351,f2(x1351,a1)),f2(a1,a1)),f2(a1,f2(x1352,f2(x1352,a1)))),f2(a1,a1))), % 278.31/278.38 inference(scs_inference,[],[53,109,13,4,5,3])). % 278.31/278.38 cnf(139,plain, % 278.31/278.38 (~E(f2(f2(a1,f2(a1,a1)),f2(a1,f2(x1391,f2(x1391,a1)))),f2(a1,a1))), % 278.31/278.38 inference(scs_inference,[],[29,135,3])). % 278.31/278.38 cnf(143,plain, % 278.31/278.38 (~E(f2(f2(x1431,f2(x1431,a1)),f2(a1,a1)),f2(f2(f2(x1432,f2(x1432,a1)),f2(a1,a1)),a1))), % 278.31/278.38 inference(scs_inference,[],[132,139,30,2,3])). % 278.31/278.38 cnf(146,plain, % 278.31/278.38 (~E(f2(f2(f2(x1461,f2(x1461,a1)),f2(a1,a1)),a1),f2(f2(x1462,f2(x1462,a1)),f2(a1,a1)))), % 278.31/278.38 inference(scs_inference,[],[143,2])). % 278.31/278.38 cnf(155,plain, % 278.31/278.38 (~E(f2(f2(a1,f2(a1,a1)),a1),f2(f2(x1551,f2(x1551,a1)),f2(a1,a1)))), % 278.31/278.38 inference(scs_inference,[],[146,29,3])). % 278.31/278.38 cnf(160,plain, % 278.31/278.38 (~E(f2(f2(f2(x1601,f2(x1601,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,f2(f2(x1602,f2(x1602,a1)),f2(a1,a1))))), % 278.31/278.38 inference(scs_inference,[],[80,25,3,2])). % 278.31/278.38 cnf(161,plain, % 278.31/278.38 (~E(f2(f2(a1,f2(a1,a1)),f2(x1611,f2(x1611,a1))),f2(f2(x1612,f2(x1612,a1)),f2(a1,a1)))), % 278.31/278.38 inference(scs_inference,[],[155,46,3])). % 278.31/278.38 cnf(164,plain, % 278.31/278.38 (~E(f2(f2(a1,f2(a1,a1)),f2(f2(x1641,f2(x1641,a1)),f2(a1,a1))),f2(f2(x1642,f2(x1642,a1)),f2(a1,a1)))), % 278.31/278.38 inference(scs_inference,[],[161,48,3])). % 278.31/278.38 cnf(168,plain, % 278.31/278.38 (~E(f2(a1,a1),f2(f2(x1681,f2(x1681,a1)),f2(a1,a1)))), % 278.31/278.38 inference(scs_inference,[],[164,161,32,2,3])). % 278.31/278.38 cnf(170,plain, % 278.31/278.39 (~E(f2(f2(x1701,f2(x1701,a1)),f2(a1,a1)),f2(a1,a1))), % 278.31/278.39 inference(scs_inference,[],[168,2])). % 278.31/278.39 cnf(171,plain, % 278.31/278.39 (~E(f2(f2(a3,f2(a3,a1)),a1),f2(f2(f2(x1711,f2(x1711,a1)),f2(a1,a1)),f2(a1,a1)))), % 278.31/278.39 inference(scs_inference,[],[168,67,26,2,3])). % 278.31/278.39 cnf(175,plain, % 278.31/278.39 (~E(f2(f2(x1751,f2(x1751,a1)),f2(a1,f2(x1752,f2(x1752,a1)))),f2(a1,a1))), % 278.31/278.39 inference(scs_inference,[],[170,171,53,2,3])). % 278.31/278.39 cnf(178,plain, % 278.31/278.39 (~E(f2(f2(a1,f2(a1,a1)),f2(a1,a1)),f2(a1,f2(f2(x1781,f2(x1781,a1)),f2(a1,a1))))), % 278.31/278.39 inference(scs_inference,[],[175,160,29,2,3])). % 278.31/278.39 cnf(181,plain, % 278.31/278.39 (~E(f2(a1,f2(f2(x1811,f2(x1811,a1)),f2(a1,a1))),f2(f2(a1,f2(a1,a1)),f2(a1,a1)))), % 278.31/278.39 inference(scs_inference,[],[178,2])). % 278.31/278.39 cnf(194,plain, % 278.31/278.39 (~E(f2(a1,f2(a1,f2(a1,a1))),f2(f2(a1,f2(a1,a1)),f2(a1,a1)))), % 278.31/278.39 inference(scs_inference,[],[181,30,3])). % 278.31/278.39 cnf(196,plain, % 278.31/278.39 (~E(f2(f2(a1,f2(a1,a1)),f2(a1,a1)),f2(a1,f2(a1,f2(a1,a1))))), % 278.31/278.39 inference(scs_inference,[],[181,30,3,2])). % 278.31/278.39 cnf(200,plain, % 278.31/278.39 (~E(f2(f2(x2001,f2(x2001,a1)),f2(a1,f2(a1,a1))),f2(f2(a1,f2(a1,a1)),f2(a1,a1)))), % 278.31/278.39 inference(scs_inference,[],[194,45,3])). % 278.31/278.39 cnf(203,plain, % 278.31/278.39 (~E(f2(f2(x2031,f2(x2031,a1)),f2(f2(x2032,f2(x2032,a1)),f2(a1,a1))),f2(f2(a1,f2(a1,a1)),f2(a1,a1)))), % 278.31/278.39 inference(scs_inference,[],[200,48,3])). % 278.31/278.39 cnf(206,plain, % 278.31/278.39 (~E(f2(a1,f2(a1,a1)),f2(a1,f2(a1,f2(a1,a1))))), % 278.31/278.39 inference(scs_inference,[],[196,203,25,2,3])). % 278.31/278.39 cnf(208,plain, % 278.31/278.39 (~E(f2(a1,f2(a1,f2(a1,a1))),f2(a1,f2(a1,a1)))), % 278.31/278.39 inference(scs_inference,[],[206,2])). % 278.31/278.39 cnf(209,plain, % 278.31/278.39 (~E(f2(f2(x2091,f2(x2091,a1)),a1),f2(f2(a1,f2(a1,a1)),f2(a1,a1)))), % 278.31/278.39 inference(scs_inference,[],[206,200,26,2,3])). % 278.31/278.39 cnf(211,plain, % 278.31/278.39 (~E(f2(f2(a1,f2(a1,a1)),f2(a1,a1)),f2(f2(x2111,f2(x2111,a1)),a1))), % 278.31/278.39 inference(scs_inference,[],[209,2])). % 278.31/278.39 cnf(212,plain, % 278.31/278.39 (~E(f2(f2(x2121,f2(x2121,a1)),f2(a1,f2(a1,a1))),f2(a1,f2(a1,a1)))), % 278.31/278.39 inference(scs_inference,[],[208,209,45,2,3])). % 278.31/278.39 cnf(215,plain, % 278.31/278.39 (~E(f2(f2(f2(x2151,f2(f2(f2(x2152,f2(x2152,a1)),f2(x2151,x2153)),f2(x2153,a1))),f2(a1,a1)),a1),a1)), % 278.31/278.39 inference(scs_inference,[],[212,133,71,2,3])). % 278.31/278.39 cnf(218,plain, % 278.31/278.39 (~E(f2(f2(f2(x2181,f2(x2181,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(x2182,f2(x2182,a1)),a1))), % 278.31/278.39 inference(scs_inference,[],[211,215,47,2,3])). % 278.31/278.39 cnf(221,plain, % 278.31/278.39 (~E(f2(f2(x2211,f2(x2211,a1)),a1),a1)), % 278.31/278.39 inference(scs_inference,[],[218,61,215,2,3])). % 278.31/278.39 cnf(225,plain, % 278.31/278.39 (~E(f2(f2(x2251,f2(x2251,a1)),f2(x2252,f2(x2252,a1))),a1)), % 278.31/278.39 inference(scs_inference,[],[221,46,2,3])). % 278.31/278.39 cnf(227,plain, % 278.31/278.39 (~E(a1,f2(f2(x2271,f2(x2271,a1)),f2(x2272,f2(x2272,a1))))), % 278.31/278.39 inference(scs_inference,[],[225,2])). % 278.31/278.39 cnf(228,plain, % 278.31/278.39 (~E(f2(f2(x2281,f2(f2(a1,f2(x2281,x2282)),f2(x2282,a1))),f2(a1,a1)),f2(a1,f2(a1,f2(a1,a1))))), % 278.31/278.39 inference(scs_inference,[],[16,225,206,2,3])). % 278.31/278.39 cnf(231,plain, % 278.31/278.39 (~E(f2(x2311,f2(x2311,a1)),f2(a1,f2(a1,f2(a1,a1))))), % 278.31/278.39 inference(scs_inference,[],[228,18,2,3])). % 278.31/278.39 cnf(234,plain, % 278.31/278.39 (~E(f2(x2341,f2(x2341,a1)),f2(f2(x2342,f2(x2342,a1)),f2(x2343,f2(x2343,a1))))), % 278.31/278.39 inference(scs_inference,[],[231,227,12,2,3])). % 278.31/278.39 cnf(235,plain, % 278.31/278.39 (~E(f2(f2(x2351,f2(x2351,a1)),f2(x2352,f2(x2352,a1))),f2(x2353,f2(x2353,a1)))), % 278.31/278.39 inference(scs_inference,[],[234,2])). % 278.31/278.39 cnf(379,plain, % 278.31/278.39 (~E(f2(f2(x3791,f2(x3791,a1)),f2(f2(x3792,f2(x3792,a1)),f2(a1,a1))),f2(x3793,f2(x3793,a1)))), % 278.31/278.39 inference(scs_inference,[],[235,48,3])). % 278.31/278.39 cnf(382,plain, % 278.31/278.39 (~E(f2(x3821,f2(x3821,a1)),f2(f2(x3822,f2(x3822,a1)),f2(f2(x3823,f2(x3823,a1)),f2(a1,a1))))), % 278.31/278.39 inference(scs_inference,[],[379,2])). % 278.31/278.39 cnf(445,plain, % 278.31/278.39 (~E(f2(f2(x4451,f2(x4451,a1)),f2(f2(x4452,f2(x4452,a1)),f2(a1,a1))),f2(f2(x4453,f2(f2(f2(x4454,f2(x4454,a1)),f2(x4453,x4455)),f2(x4455,a1))),f2(a1,a1)))), % 278.31/278.39 inference(scs_inference,[],[382,23,4,5,3,2])). % 278.31/278.39 cnf(468,plain, % 278.31/278.39 (E(f2(x4681,f2(f2(f2(x4682,f2(f2(x4683,f2(x4682,x4684)),f2(x4684,a1))),f2(a1,a1)),x4685)),f2(x4681,f2(x4683,x4685)))), % 278.31/278.39 inference(scs_inference,[],[61,4,5])). % 278.31/278.39 cnf(1925,plain, % 278.31/278.39 (E(f2(f2(x19251,f2(f2(f2(x19252,f2(f2(x19253,f2(x19252,x19254)),f2(x19254,a1))),f2(a1,a1)),x19255)),x19256),f2(f2(x19251,f2(x19253,x19255)),x19256))), % 278.31/278.39 inference(scs_inference,[],[468,5,4])). % 278.31/278.39 cnf(2524,plain, % 278.31/278.39 (E(f2(x25241,f2(f2(x25242,f2(x25241,x25243)),f2(x25243,a1))),f2(f2(a1,f2(x25242,f2(a1,a1))),f2(a1,a1)))), % 278.31/278.39 inference(scs_inference,[],[9,1925,3])). % 278.31/278.39 cnf(2528,plain, % 278.31/278.39 ($false), % 278.31/278.39 inference(scs_inference,[],[47,445,2524,3]), % 278.31/278.39 ['proof']). % 278.31/278.39 % SZS output end Proof % 278.31/278.39 % Total time :277.490000s %------------------------------------------------------------------------------