%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP481-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 : 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:45 EDT 2024 % Result : Unsatisfiable 59.51s 59.59s % Output : CNFRefutation 59.58s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.13 % Problem : GRP481-1 : TPTP v8.2.0. Released v2.6.0. % 0.09/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n028.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Thu Jun 20 07:54:09 EDT 2024 % 0.13/0.33 % CPUTime : % 0.19/0.52 start to proof:theBenchmark % 59.49/59.56 %------------------------------------------- % 59.49/59.56 % File :CSE---1.7 % 59.49/59.56 % Problem :theBenchmark % 59.49/59.56 % Transform :cnf % 59.49/59.56 % Format :tptp:raw % 59.49/59.56 % Command :java -jar mcs_scs.jar %d %s % 59.49/59.56 % 59.49/59.56 % Result :Theorem 59.010000s % 59.49/59.56 % Output :CNFRefutation 59.010000s % 59.49/59.56 %------------------------------------------- % 59.51/59.58 %-------------------------------------------------------------------------- % 59.51/59.58 % File : GRP481-1 : TPTP v8.2.0. Released v2.6.0. % 59.51/59.58 % Domain : Group Theory % 59.51/59.58 % Problem : Axiom for group theory, in double division and identity, part 1 % 59.51/59.58 % Version : [McC93] (equality) axioms. % 59.51/59.58 % English : % 59.51/59.58 % 59.51/59.58 % Refs : [Neu86] Neumann (1986), Yet Another Single Law for Groups % 59.51/59.58 % : [McC93] McCune (1993), Single Axioms for Groups and Abelian Gr % 59.51/59.58 % Source : [TPTP] % 59.51/59.58 % Names : % 59.51/59.58 % 59.51/59.58 % Status : Unsatisfiable % 59.51/59.58 % 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.14 v5.5.0, 0.11 v5.4.0, 0.00 v2.6.0 % 59.51/59.58 % Syntax : Number of clauses : 5 ( 5 unt; 0 nHn; 1 RR) % 59.51/59.58 % Number of literals : 5 ( 5 equ; 1 neg) % 59.51/59.58 % Maximal clause size : 1 ( 1 avg) % 59.51/59.58 % Maximal term depth : 7 ( 2 avg) % 59.51/59.58 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 59.51/59.58 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty) % 59.51/59.58 % Number of variables : 8 ( 0 sgn) % 59.51/59.58 % SPC : CNF_UNS_RFO_PEQ_UEQ % 59.51/59.58 % 59.51/59.58 % Comments : A UEQ part of GRP075-1 % 59.51/59.58 %-------------------------------------------------------------------------- % 59.51/59.58 cnf(single_axiom,axiom, % 59.51/59.58 double_divide(double_divide(double_divide(A,double_divide(B,identity)),double_divide(double_divide(C,double_divide(D,double_divide(D,identity))),double_divide(A,identity))),B) = C ). % 59.51/59.58 % 59.51/59.58 cnf(multiply,axiom, % 59.51/59.58 multiply(A,B) = double_divide(double_divide(B,A),identity) ). % 59.51/59.58 % 59.51/59.59 cnf(inverse,axiom, % 59.51/59.59 inverse(A) = double_divide(A,identity) ). % 59.51/59.59 % 59.51/59.59 cnf(identity,axiom, % 59.51/59.59 identity = double_divide(A,inverse(A)) ). % 59.51/59.59 % 59.51/59.59 cnf(prove_these_axioms_1,negated_conjecture, % 59.51/59.59 multiply(inverse(a1),a1) != identity ). % 59.51/59.59 % 59.51/59.59 %-------------------------------------------------------------------------- % 59.51/59.59 %------------------------------------------- % 59.51/59.59 % Proof found % 59.51/59.59 % SZS status Theorem for theBenchmark % 59.51/59.59 % SZS output start Proof % 59.51/59.61 %ClaNum:8(EqnAxiom:5) % 59.51/59.61 %VarNum:10(SingletonVarNum:5) % 59.51/59.61 %MaxLitNum:1 % 59.51/59.61 %MaxfuncDepth:4 % 59.51/59.61 %SharedTerms:6 % 59.51/59.61 %goalClause: 8 % 59.51/59.61 %singleGoalClaCount:1 % 59.51/59.61 [8]~E(f2(f2(a3,f2(a3,a1)),a1),a1) % 59.51/59.61 [6]E(f2(x61,f2(x61,a1)),a1) % 59.51/59.61 [7]E(f2(f2(f2(x71,f2(x72,a1)),f2(f2(x73,f2(x74,f2(x74,a1))),f2(x71,a1))),x72),x73) % 59.51/59.61 %EqnAxiom % 59.51/59.61 [1]E(x11,x11) % 59.51/59.61 [2]E(x22,x21)+~E(x21,x22) % 59.51/59.61 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 59.51/59.61 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 59.51/59.61 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 59.51/59.61 % 59.51/59.61 %------------------------------------------- % 59.58/59.64 cnf(9,plain, % 59.58/59.64 (E(a1,f2(x91,f2(x91,a1)))), % 59.58/59.64 inference(scs_inference,[],[6,2])). % 59.58/59.64 cnf(10,plain, % 59.58/59.64 (~E(f2(f2(a3,f2(a3,a1)),a1),f2(x101,f2(x101,a1)))), % 59.58/59.64 inference(scs_inference,[],[8,6,2,3])). % 59.58/59.64 cnf(12,plain, % 59.58/59.64 (E(x121,f2(f2(f2(x122,f2(x123,a1)),f2(f2(x121,f2(x124,f2(x124,a1))),f2(x122,a1))),x123))), % 59.58/59.64 inference(scs_inference,[],[7,2])). % 59.58/59.64 cnf(15,plain, % 59.58/59.64 (E(f2(x151,f2(x151,a1)),f2(f2(f2(x152,f2(x153,a1)),f2(f2(a1,f2(x154,f2(x154,a1))),f2(x152,a1))),x153))), % 59.58/59.64 inference(scs_inference,[],[6,12,3])). % 59.58/59.64 cnf(17,plain, % 59.58/59.64 (E(f2(f2(f2(x171,f2(x172,a1)),f2(f2(a1,f2(x173,f2(x173,a1))),f2(x171,a1))),x172),f2(x174,f2(x174,a1)))), % 59.58/59.64 inference(scs_inference,[],[6,12,3,2])). % 59.58/59.64 cnf(18,plain, % 59.58/59.64 (~E(f2(f2(a3,f2(a3,a1)),a1),f2(f2(f2(x181,f2(x182,a1)),f2(f2(a1,f2(x183,f2(x183,a1))),f2(x181,a1))),x182))), % 59.58/59.64 inference(scs_inference,[],[17,10,3])). % 59.58/59.64 cnf(20,plain, % 59.58/59.64 (~E(f2(a3,f2(a3,a1)),f2(f2(x201,f2(a1,a1)),f2(f2(a1,f2(x202,f2(x202,a1))),f2(x201,a1))))), % 59.58/59.64 inference(scs_inference,[],[17,10,3,4])). % 59.58/59.64 cnf(25,plain, % 59.58/59.64 (E(f2(f2(x251,f2(x251,a1)),x252),f2(a1,x252))), % 59.58/59.64 inference(scs_inference,[],[6,4])). % 59.58/59.64 cnf(26,plain, % 59.58/59.64 (E(f2(x261,f2(x262,f2(x262,a1))),f2(x261,a1))), % 59.58/59.64 inference(scs_inference,[],[6,4,5])). % 59.58/59.64 cnf(27,plain, % 59.58/59.64 (~E(f2(f2(x271,f2(a1,a1)),f2(f2(a1,f2(x272,f2(x272,a1))),f2(x271,a1))),f2(a3,f2(a3,a1)))), % 59.58/59.64 inference(scs_inference,[],[6,20,4,5,2])). % 59.58/59.64 cnf(28,plain, % 59.58/59.64 (~E(a1,f2(f2(x281,f2(a1,a1)),f2(f2(a1,f2(x282,f2(x282,a1))),f2(x281,a1))))), % 59.58/59.64 inference(scs_inference,[],[6,20,4,5,2,3])). % 59.58/59.64 cnf(30,plain, % 59.58/59.64 (E(f2(f2(f2(x301,f2(x301,a1)),x302),x303),f2(f2(a1,x302),x303))), % 59.58/59.64 inference(scs_inference,[],[25,4])). % 59.58/59.64 cnf(31,plain, % 59.58/59.64 (E(f2(x311,f2(f2(x312,f2(x312,a1)),x313)),f2(x311,f2(a1,x313)))), % 59.58/59.64 inference(scs_inference,[],[25,4,5])). % 59.58/59.64 cnf(32,plain, % 59.58/59.64 (~E(f2(f2(x321,f2(a1,a1)),f2(f2(a1,f2(x322,f2(x322,a1))),f2(x321,a1))),a1)), % 59.58/59.64 inference(scs_inference,[],[25,28,4,5,2])). % 59.58/59.64 cnf(33,plain, % 59.58/59.64 (~E(f2(a1,f2(f2(a1,f2(x331,f2(x331,a1))),f2(a1,a1))),f2(a3,f2(a3,a1)))), % 59.58/59.64 inference(scs_inference,[],[25,28,27,4,5,2,3])). % 59.58/59.64 cnf(36,plain, % 59.58/59.64 (E(f2(f2(x361,f2(x362,f2(x362,a1))),x363),f2(f2(x361,a1),x363))), % 59.58/59.64 inference(scs_inference,[],[26,4])). % 59.58/59.64 cnf(37,plain, % 59.58/59.64 (E(f2(x371,f2(x372,f2(x373,f2(x373,a1)))),f2(x371,f2(x372,a1)))), % 59.58/59.64 inference(scs_inference,[],[26,4,5])). % 59.58/59.64 cnf(38,plain, % 59.58/59.64 (~E(f2(a3,f2(a3,a1)),f2(a1,f2(f2(a1,f2(x381,f2(x381,a1))),f2(a1,a1))))), % 59.58/59.64 inference(scs_inference,[],[26,33,4,5,2])). % 59.58/59.64 cnf(39,plain, % 59.58/59.64 (~E(f2(f2(f2(a1,f2(x391,f2(x391,a1))),f2(a1,a1)),a1),a1)), % 59.58/59.64 inference(scs_inference,[],[26,33,32,4,5,2,3])). % 59.58/59.64 cnf(42,plain, % 59.58/59.64 (E(f2(f2(f2(f2(x421,f2(x421,a1)),x422),x423),x424),f2(f2(f2(a1,x422),x423),x424))), % 59.58/59.64 inference(scs_inference,[],[30,4])). % 59.58/59.64 cnf(43,plain, % 59.58/59.64 (E(f2(x431,f2(f2(f2(x432,f2(x432,a1)),x433),x434)),f2(x431,f2(f2(a1,x433),x434)))), % 59.58/59.64 inference(scs_inference,[],[30,4,5])). % 59.58/59.64 cnf(44,plain, % 59.58/59.64 (~E(a1,f2(f2(f2(a1,f2(x441,f2(x441,a1))),f2(a1,a1)),a1))), % 59.58/59.64 inference(scs_inference,[],[39,30,4,5,2])). % 59.58/59.64 cnf(45,plain, % 59.58/59.64 (~E(a1,f2(a1,f2(f2(a1,f2(x451,f2(x451,a1))),f2(a1,a1))))), % 59.58/59.64 inference(scs_inference,[],[6,39,30,38,4,5,2,3])). % 59.58/59.64 cnf(47,plain, % 59.58/59.64 (E(f2(f2(x471,f2(f2(x472,f2(x472,a1)),x473)),x474),f2(f2(x471,f2(a1,x473)),x474))), % 59.58/59.64 inference(scs_inference,[],[31,4])). % 59.58/59.64 cnf(48,plain, % 59.58/59.64 (E(f2(x481,f2(x482,f2(f2(x483,f2(x483,a1)),x484))),f2(x481,f2(x482,f2(a1,x484))))), % 59.58/59.64 inference(scs_inference,[],[31,4,5])). % 59.58/59.64 cnf(49,plain, % 59.58/59.64 (~E(f2(a1,f2(f2(a1,f2(x491,f2(x491,a1))),f2(a1,a1))),a1)), % 59.58/59.64 inference(scs_inference,[],[45,31,4,5,2])). % 59.58/59.64 cnf(50,plain, % 59.58/59.64 (~E(f2(x501,f2(x501,a1)),f2(f2(f2(a1,f2(x502,f2(x502,a1))),f2(a1,a1)),a1))), % 59.58/59.64 inference(scs_inference,[],[44,45,31,9,4,5,2,3])). % 59.58/59.64 cnf(51,plain, % 59.58/59.64 (E(f2(f2(f2(x511,f2(x512,f2(x512,a1))),x513),x514),f2(f2(f2(x511,a1),x513),x514))), % 59.58/59.64 inference(scs_inference,[],[36,4])). % 59.58/59.64 cnf(52,plain, % 59.58/59.64 (E(f2(x521,f2(f2(x522,f2(x523,f2(x523,a1))),x524)),f2(x521,f2(f2(x522,a1),x524)))), % 59.58/59.64 inference(scs_inference,[],[36,4,5])). % 59.58/59.64 cnf(53,plain, % 59.58/59.64 (~E(f2(f2(f2(a1,f2(x531,f2(x531,a1))),f2(a1,a1)),a1),f2(x532,f2(x532,a1)))), % 59.58/59.64 inference(scs_inference,[],[36,50,4,5,2])). % 59.58/59.64 cnf(54,plain, % 59.58/59.64 (E(f2(x541,f2(x541,f2(x542,f2(x542,a1)))),a1)), % 59.58/59.64 inference(scs_inference,[],[6,36,37,50,4,5,2,3])). % 59.58/59.64 cnf(56,plain, % 59.58/59.64 (E(f2(f2(x561,f2(x561,f2(x562,f2(x562,a1)))),x563),f2(a1,x563))), % 59.58/59.64 inference(scs_inference,[],[54,4])). % 59.58/59.64 cnf(59,plain, % 59.58/59.64 (~E(f2(a1,f2(f2(a1,a1),f2(a1,a1))),a1)), % 59.58/59.64 inference(scs_inference,[],[49,54,52,18,4,5,2,3])). % 59.58/59.64 cnf(65,plain, % 59.58/59.64 (~E(f2(f2(f2(a1,a1),f2(a1,a1)),a1),f2(x651,f2(x651,a1)))), % 59.58/59.64 inference(scs_inference,[],[59,53,51,37,4,5,2,3])). % 59.58/59.64 cnf(67,plain, % 59.58/59.64 (E(f2(a1,x671),f2(f2(x672,f2(x672,a1)),x671))), % 59.58/59.64 inference(scs_inference,[],[9,4])). % 59.58/59.64 cnf(68,plain, % 59.58/59.64 (E(f2(x681,a1),f2(x681,f2(x682,f2(x682,a1))))), % 59.58/59.64 inference(scs_inference,[],[9,4,5])). % 59.58/59.64 cnf(69,plain, % 59.58/59.64 (~E(f2(x691,f2(x691,a1)),f2(f2(f2(a1,a1),f2(a1,a1)),a1))), % 59.58/59.64 inference(scs_inference,[],[65,9,4,5,2])). % 59.58/59.64 cnf(72,plain, % 59.58/59.64 (E(f2(f2(a1,x721),x722),f2(f2(f2(x723,f2(x723,a1)),x721),x722))), % 59.58/59.64 inference(scs_inference,[],[67,4])). % 59.58/59.64 cnf(73,plain, % 59.58/59.64 (E(f2(x731,f2(a1,x732)),f2(x731,f2(f2(x733,f2(x733,a1)),x732)))), % 59.58/59.64 inference(scs_inference,[],[67,4,5])). % 59.58/59.64 cnf(74,plain, % 59.58/59.64 (~E(f2(x741,f2(x741,a1)),f2(f2(a3,f2(a3,a1)),a1))), % 59.58/59.64 inference(scs_inference,[],[67,10,4,5,2])). % 59.58/59.64 cnf(75,plain, % 59.58/59.64 (~E(a1,f2(f2(f2(a1,a1),f2(a1,a1)),a1))), % 59.58/59.64 inference(scs_inference,[],[6,67,69,10,4,5,2,3])). % 59.58/59.64 cnf(77,plain, % 59.58/59.64 (~E(f2(f2(f2(a1,a1),f2(a1,a1)),a1),a1)), % 59.58/59.64 inference(scs_inference,[],[75,2])). % 59.58/59.64 cnf(78,plain, % 59.58/59.64 (E(f2(f2(x781,a1),x782),f2(f2(x781,f2(x783,f2(x783,a1))),x782))), % 59.58/59.64 inference(scs_inference,[],[68,75,2,4])). % 59.58/59.64 cnf(79,plain, % 59.58/59.64 (E(f2(x791,f2(x792,a1)),f2(x791,f2(x792,f2(x793,f2(x793,a1)))))), % 59.58/59.64 inference(scs_inference,[],[68,75,2,4,5])). % 59.58/59.64 cnf(82,plain, % 59.58/59.64 (E(f2(f2(f2(a1,x821),x822),x823),f2(f2(f2(f2(x824,f2(x824,a1)),x821),x822),x823))), % 59.58/59.64 inference(scs_inference,[],[72,4])). % 59.58/59.64 cnf(83,plain, % 59.58/59.64 (E(f2(x831,f2(f2(a1,x832),x833)),f2(x831,f2(f2(f2(x834,f2(x834,a1)),x832),x833)))), % 59.58/59.64 inference(scs_inference,[],[72,4,5])). % 59.58/59.64 cnf(84,plain, % 59.58/59.64 (~E(f2(f2(f2(x841,f2(x841,a1)),x842),f2(f2(a1,x842),a1)),f2(f2(a3,f2(a3,a1)),a1))), % 59.58/59.64 inference(scs_inference,[],[74,72,4,5,3])). % 59.58/59.64 cnf(87,plain, % 59.58/59.64 (~E(f2(f2(a3,f2(a3,a1)),a1),f2(f2(f2(x871,f2(x871,a1)),x872),f2(f2(a1,x872),a1)))), % 59.58/59.64 inference(scs_inference,[],[74,72,4,5,3,2])). % 59.58/59.64 cnf(88,plain, % 59.58/59.64 (E(f2(f2(x881,f2(a1,x882)),x883),f2(f2(x881,f2(f2(x884,f2(x884,a1)),x882)),x883))), % 59.58/59.64 inference(scs_inference,[],[73,4])). % 59.58/59.64 cnf(89,plain, % 59.58/59.64 (E(f2(x891,f2(x892,f2(a1,x893))),f2(x891,f2(x892,f2(f2(x894,f2(x894,a1)),x893))))), % 59.58/59.64 inference(scs_inference,[],[73,4,5])). % 59.58/59.64 cnf(90,plain, % 59.58/59.64 (~E(f2(f2(f2(f2(x901,f2(x901,a1)),a1),f2(a1,a1)),a1),a1)), % 59.58/59.64 inference(scs_inference,[],[77,73,82,4,5,3])). % 59.58/59.64 cnf(92,plain, % 59.58/59.64 (~E(a1,f2(f2(f2(f2(x921,f2(x921,a1)),a1),f2(a1,a1)),a1))), % 59.58/59.64 inference(scs_inference,[],[77,73,82,4,5,3,2])). % 59.58/59.64 cnf(93,plain, % 59.58/59.64 (E(f2(f2(f2(x931,a1),x932),x933),f2(f2(f2(x931,f2(x934,f2(x934,a1))),x932),x933))), % 59.58/59.64 inference(scs_inference,[],[78,4])). % 59.58/59.64 cnf(94,plain, % 59.58/59.64 (E(f2(x941,f2(f2(x942,a1),x943)),f2(x941,f2(f2(x942,f2(x944,f2(x944,a1))),x943)))), % 59.58/59.64 inference(scs_inference,[],[78,4,5])). % 59.58/59.64 cnf(95,plain, % 59.58/59.64 (~E(f2(f2(f2(x951,f2(x951,a1)),f2(x952,f2(x952,a1))),f2(f2(a1,a1),a1)),f2(f2(a3,f2(a3,a1)),a1))), % 59.58/59.64 inference(scs_inference,[],[78,84,4,5,3])). % 59.58/59.64 cnf(98,plain, % 59.58/59.64 (~E(f2(f2(a3,f2(a3,a1)),a1),f2(f2(f2(x981,f2(x981,a1)),f2(x982,f2(x982,a1))),f2(f2(a1,a1),a1)))), % 59.58/59.64 inference(scs_inference,[],[78,84,4,5,3,2])). % 59.58/59.64 cnf(99,plain, % 59.58/59.64 (E(f2(f2(x991,f2(x992,a1)),x993),f2(f2(x991,f2(x992,f2(x994,f2(x994,a1)))),x993))), % 59.58/59.64 inference(scs_inference,[],[79,4])). % 59.58/59.64 cnf(100,plain, % 59.58/59.64 (E(f2(x1001,f2(x1002,f2(x1003,a1))),f2(x1001,f2(x1002,f2(x1003,f2(x1004,f2(x1004,a1))))))), % 59.58/59.64 inference(scs_inference,[],[79,4,5])). % 59.58/59.64 cnf(101,plain, % 59.58/59.64 (~E(f2(f2(a3,f2(a3,a1)),f2(x1011,f2(x1011,a1))),f2(f2(f2(x1012,f2(x1012,a1)),x1013),f2(f2(a1,x1013),a1)))), % 59.58/59.64 inference(scs_inference,[],[79,87,68,4,5,3])). % 59.58/59.64 cnf(103,plain, % 59.58/59.64 (~E(f2(f2(f2(x1031,f2(x1031,a1)),x1032),f2(f2(a1,x1032),a1)),f2(f2(a3,f2(a3,a1)),f2(x1033,f2(x1033,a1))))), % 59.58/59.64 inference(scs_inference,[],[79,87,68,4,5,3,2])). % 59.58/59.64 cnf(104,plain, % 59.58/59.64 (~E(f2(f2(a3,f2(a3,a1)),f2(f2(x1041,f2(x1041,a1)),f2(a1,a1))),f2(f2(f2(x1042,f2(x1042,a1)),x1043),f2(f2(a1,x1043),a1)))), % 59.58/59.64 inference(scs_inference,[],[101,48,3])). % 59.58/59.64 cnf(108,plain, % 59.58/59.64 (~E(f2(f2(a3,f2(a3,f2(x1081,f2(x1081,a1)))),a1),a1)), % 59.58/59.64 inference(scs_inference,[],[104,99,8,2,3])). % 59.58/59.64 cnf(110,plain, % 59.58/59.65 (~E(a1,f2(f2(a3,f2(a3,f2(x1101,f2(x1101,a1)))),a1))), % 59.58/59.65 inference(scs_inference,[],[108,2])). % 59.58/59.65 cnf(111,plain, % 59.58/59.65 (~E(f2(f2(f2(f2(x1111,f2(x1111,a1)),a1),f2(f2(x1112,f2(x1112,a1)),a1)),a1),a1)), % 59.58/59.65 inference(scs_inference,[],[90,108,88,2,3])). % 59.58/59.65 cnf(114,plain, % 59.58/59.65 (~E(f2(f2(f2(a1,a1),f2(f2(x1141,f2(x1141,a1)),a1)),a1),a1)), % 59.58/59.65 inference(scs_inference,[],[42,111,2,3])). % 59.58/59.65 cnf(117,plain, % 59.58/59.65 (~E(a1,f2(f2(f2(a1,a1),f2(f2(x1171,f2(x1171,a1)),a1)),a1))), % 59.58/59.65 inference(scs_inference,[],[114,2])). % 59.58/59.65 cnf(118,plain, % 59.58/59.65 (~E(f2(f2(f2(a1,f2(x1181,f2(x1181,a1))),f2(f2(x1182,f2(x1182,a1)),a1)),a1),a1)), % 59.58/59.65 inference(scs_inference,[],[114,93,2,3])). % 59.58/59.65 cnf(121,plain, % 59.58/59.65 (~E(f2(a1,f2(f2(f2(x1211,f2(x1211,a1)),a1),f2(a1,a1))),a1)), % 59.58/59.65 inference(scs_inference,[],[83,118,59,2,3])). % 59.58/59.65 cnf(123,plain, % 59.58/59.65 (~E(a1,f2(a1,f2(f2(f2(x1231,f2(x1231,a1)),a1),f2(a1,a1))))), % 59.58/59.65 inference(scs_inference,[],[121,2])). % 59.58/59.65 cnf(124,plain, % 59.58/59.65 (~E(f2(a1,f2(f2(f2(x1241,f2(x1241,a1)),a1),f2(f2(x1242,f2(x1242,a1)),a1))),a1)), % 59.58/59.65 inference(scs_inference,[],[121,89,2,3])). % 59.58/59.65 cnf(127,plain, % 59.58/59.65 (~E(f2(x1271,f2(x1271,a1)),f2(f2(f2(f2(x1272,f2(x1272,a1)),a1),f2(a1,a1)),a1))), % 59.58/59.65 inference(scs_inference,[],[9,92,124,2,3])). % 59.58/59.65 cnf(128,plain, % 59.58/59.65 (~E(f2(f2(f2(f2(x1281,f2(x1281,a1)),a1),f2(a1,a1)),a1),f2(x1282,f2(x1282,a1)))), % 59.58/59.65 inference(scs_inference,[],[127,2])). % 59.58/59.65 cnf(129,plain, % 59.58/59.65 (~E(f2(x1291,f2(x1291,a1)),f2(a1,f2(f2(f2(x1292,f2(x1292,a1)),a1),f2(a1,a1))))), % 59.58/59.65 inference(scs_inference,[],[9,123,127,2,3])). % 59.58/59.65 cnf(130,plain, % 59.58/59.65 (~E(f2(a1,f2(f2(f2(x1301,f2(x1301,a1)),a1),f2(a1,a1))),f2(x1302,f2(x1302,a1)))), % 59.58/59.65 inference(scs_inference,[],[129,2])). % 59.58/59.65 cnf(131,plain, % 59.58/59.65 (~E(f2(x1311,f2(x1311,a1)),f2(f2(f2(a1,a1),f2(f2(x1312,f2(x1312,a1)),a1)),a1))), % 59.58/59.65 inference(scs_inference,[],[9,129,117,2,3])). % 59.58/59.65 cnf(133,plain, % 59.58/59.65 (~E(f2(x1331,f2(x1331,a1)),f2(f2(a3,f2(a3,f2(x1332,f2(x1332,a1)))),a1))), % 59.58/59.65 inference(scs_inference,[],[9,110,131,2,3])). % 59.58/59.65 cnf(134,plain, % 59.58/59.65 (~E(f2(f2(a3,f2(a3,f2(x1341,f2(x1341,a1)))),a1),f2(x1342,f2(x1342,a1)))), % 59.58/59.65 inference(scs_inference,[],[133,2])). % 59.58/59.65 cnf(135,plain, % 59.58/59.65 (~E(f2(a1,f2(f2(a1,a1),f2(a1,a1))),f2(x1351,f2(x1351,a1)))), % 59.58/59.65 inference(scs_inference,[],[130,133,43,2,3])). % 59.58/59.65 cnf(138,plain, % 59.58/59.65 (~E(f2(x1381,f2(x1381,a1)),f2(a1,f2(f2(a1,a1),f2(a1,a1))))), % 59.58/59.65 inference(scs_inference,[],[135,2])). % 59.58/59.65 cnf(139,plain, % 59.58/59.65 (~E(f2(a1,f2(f2(a1,f2(x1391,f2(x1391,a1))),f2(a1,a1))),f2(x1392,f2(x1392,a1)))), % 59.58/59.65 inference(scs_inference,[],[135,94,2,3])). % 59.58/59.65 cnf(141,plain, % 59.58/59.65 (~E(f2(x1411,f2(x1411,a1)),f2(a1,f2(f2(a1,f2(x1412,f2(x1412,a1))),f2(a1,a1))))), % 59.58/59.65 inference(scs_inference,[],[139,2])). % 59.58/59.65 cnf(142,plain, % 59.58/59.65 (~E(f2(a1,a1),f2(x1421,f2(x1421,a1)))), % 59.58/59.65 inference(scs_inference,[],[139,56,134,2,3])). % 59.58/59.65 cnf(145,plain, % 59.58/59.65 (~E(f2(x1451,f2(x1451,a1)),f2(a1,a1))), % 59.58/59.65 inference(scs_inference,[],[142,2])). % 59.58/59.65 cnf(146,plain, % 59.58/59.65 (~E(f2(f2(f2(x1461,f2(x1461,a1)),x1462),f2(f2(a1,x1462),a1)),f2(a1,f2(f2(a1,a1),f2(a1,a1))))), % 59.58/59.65 inference(scs_inference,[],[142,138,43,2,3])). % 59.58/59.65 cnf(149,plain, % 59.58/59.65 (~E(f2(a1,f2(f2(a1,a1),f2(a1,a1))),f2(f2(f2(x1491,f2(x1491,a1)),x1492),f2(f2(a1,x1492),a1)))), % 59.58/59.65 inference(scs_inference,[],[146,2])). % 59.58/59.65 cnf(150,plain, % 59.58/59.65 (~E(f2(f2(f2(x1501,f2(x1502,a1)),f2(f2(a1,f2(x1503,f2(x1503,a1))),f2(x1501,a1))),x1502),f2(a1,a1))), % 59.58/59.65 inference(scs_inference,[],[145,146,15,2,3])). % 59.58/59.65 cnf(152,plain, % 59.58/59.65 (~E(f2(f2(x1521,f2(x1522,f2(x1522,a1))),f2(f2(x1521,a1),a1)),f2(a1,f2(f2(a1,f2(x1523,f2(x1523,a1))),f2(a1,a1))))), % 59.58/59.65 inference(scs_inference,[],[141,52,3])). % 59.58/59.65 cnf(155,plain, % 59.58/59.65 (~E(f2(a1,f2(f2(a1,f2(x1551,f2(x1551,a1))),f2(a1,a1))),f2(f2(x1552,f2(x1553,f2(x1553,a1))),f2(f2(x1552,a1),a1)))), % 59.58/59.65 inference(scs_inference,[],[152,2])). % 59.58/59.65 cnf(156,plain, % 59.58/59.65 (~E(f2(f2(x1561,f2(x1561,a1)),a1),f2(x1562,f2(x1562,a1)))), % 59.58/59.65 inference(scs_inference,[],[152,142,67,2,3])). % 59.58/59.65 cnf(159,plain, % 59.58/59.65 (~E(f2(f2(f2(x1591,f2(x1591,a1)),f2(a1,a1)),a1),f2(x1592,f2(x1592,a1)))), % 59.58/59.65 inference(scs_inference,[],[156,47,2,3])). % 59.58/59.65 cnf(162,plain, % 59.58/59.65 (~E(f2(x1621,f2(x1621,a1)),f2(f2(f2(x1622,f2(x1622,a1)),f2(a1,a1)),a1))), % 59.58/59.65 inference(scs_inference,[],[159,2])). % 59.58/59.65 cnf(169,plain, % 59.58/59.65 (~E(f2(a1,f2(f2(a1,f2(x1691,f2(x1691,a1))),f2(a1,f2(x1692,f2(x1692,a1))))),a1)), % 59.58/59.65 inference(scs_inference,[],[100,49,3])). % 59.58/59.65 cnf(172,plain, % 59.58/59.65 (~E(f2(f2(x1721,f2(x1721,a1)),f2(a1,a1)),f2(f2(f2(x1722,f2(x1722,a1)),f2(a1,a1)),a1))), % 59.58/59.65 inference(scs_inference,[],[162,169,31,2,3])). % 59.58/59.65 cnf(175,plain, % 59.58/59.65 (~E(f2(f2(f2(x1751,f2(x1751,a1)),f2(a1,a1)),a1),f2(f2(x1752,f2(x1752,a1)),f2(a1,a1)))), % 59.58/59.65 inference(scs_inference,[],[172,2])). % 59.58/59.65 cnf(176,plain, % 59.58/59.65 (~E(f2(f2(f2(x1761,f2(x1761,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(f2(x1762,f2(x1762,a1)),f2(a1,a1)),a1))), % 59.58/59.65 inference(scs_inference,[],[172,47,2,3])). % 59.58/59.65 cnf(179,plain, % 59.58/59.65 (~E(f2(f2(f2(x1791,f2(x1791,a1)),f2(a1,a1)),a1),f2(f2(f2(x1792,f2(x1792,a1)),f2(a1,a1)),f2(a1,a1)))), % 59.58/59.65 inference(scs_inference,[],[176,2])). % 59.58/59.65 cnf(180,plain, % 59.58/59.65 (~E(f2(f2(f2(f2(x1801,f2(x1801,a1)),f2(a1,a1)),f2(a1,a1)),a1),f2(f2(x1802,f2(x1802,a1)),f2(a1,a1)))), % 59.58/59.65 inference(scs_inference,[],[175,176,82,2,3])). % 59.58/59.65 cnf(183,plain, % 59.58/59.65 (~E(f2(f2(x1831,f2(x1831,a1)),f2(a1,a1)),f2(f2(f2(f2(x1832,f2(x1832,a1)),f2(a1,a1)),f2(a1,a1)),a1))), % 59.58/59.65 inference(scs_inference,[],[180,2])). % 59.58/59.65 cnf(184,plain, % 59.58/59.65 (~E(f2(a1,f2(f2(f2(x1841,f2(x1841,a1)),a1),f2(a1,a1))),f2(f2(f2(x1842,f2(x1842,a1)),x1843),f2(f2(a1,x1843),a1)))), % 59.58/59.65 inference(scs_inference,[],[180,149,83,2,3])). % 59.58/59.65 cnf(187,plain, % 59.58/59.65 (~E(f2(f2(f2(f2(x1871,f2(x1871,a1)),f2(x1872,f2(x1872,a1))),f2(a1,a1)),a1),f2(x1873,f2(x1873,a1)))), % 59.58/59.65 inference(scs_inference,[],[128,184,93,2,3])). % 59.58/59.65 cnf(189,plain, % 59.58/59.65 (~E(f2(x1891,f2(x1891,a1)),f2(f2(f2(f2(x1892,f2(x1892,a1)),f2(x1893,f2(x1893,a1))),f2(a1,a1)),a1))), % 59.58/59.65 inference(scs_inference,[],[187,2])). % 59.58/59.65 cnf(190,plain, % 59.58/59.65 (~E(f2(f2(f2(x1901,f2(x1901,a1)),f2(f2(x1902,f2(x1902,a1)),f2(a1,a1))),f2(f2(a1,a1),a1)),f2(f2(a3,f2(a3,a1)),a1))), % 59.58/59.65 inference(scs_inference,[],[187,95,88,2,3])). % 59.58/59.65 cnf(194,plain, % 59.58/59.65 (~E(f2(f2(a1,f2(a1,a1)),a1),f2(f2(f2(x1941,f2(x1941,a1)),f2(a1,a1)),f2(a1,a1)))), % 59.58/59.65 inference(scs_inference,[],[179,190,30,2,3])). % 59.58/59.65 cnf(196,plain, % 59.58/59.65 (~E(f2(f2(f2(x1961,f2(x1961,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(a1,f2(a1,a1)),a1))), % 59.58/59.65 inference(scs_inference,[],[194,2])). % 59.58/59.65 cnf(200,plain, % 59.58/59.65 (~E(f2(f2(f2(x2001,f2(x2001,a1)),f2(a1,a1)),f2(f2(x2002,f2(x2002,a1)),a1)),f2(f2(a1,f2(a1,a1)),a1))), % 59.58/59.65 inference(scs_inference,[],[196,73,3])). % 59.58/59.65 cnf(203,plain, % 59.58/59.65 (~E(f2(f2(x2031,f2(x2031,a1)),f2(a1,f2(x2032,f2(x2032,a1)))),f2(f2(f2(f2(x2033,f2(x2033,a1)),f2(a1,a1)),f2(a1,a1)),a1))), % 59.58/59.65 inference(scs_inference,[],[183,79,3])). % 59.58/59.65 cnf(205,plain, % 59.58/59.65 (~E(f2(f2(f2(f2(x2051,f2(x2051,a1)),f2(a1,a1)),f2(a1,a1)),a1),f2(f2(x2052,f2(x2052,a1)),f2(a1,f2(x2053,f2(x2053,a1)))))), % 59.58/59.65 inference(scs_inference,[],[183,79,3,2])). % 59.58/59.65 cnf(209,plain, % 59.58/59.65 (~E(f2(f2(x2091,f2(x2091,a1)),f2(a1,f2(x2092,f2(x2092,a1)))),f2(f2(f2(a1,f2(a1,a1)),f2(a1,a1)),a1))), % 59.58/59.65 inference(scs_inference,[],[205,42,3,2])). % 59.58/59.65 cnf(212,plain, % 59.58/59.65 (~E(f2(a1,a1),a1)), % 59.58/59.65 inference(scs_inference,[],[150,7,3,2])). % 59.58/59.65 cnf(213,plain, % 59.58/59.65 (~E(f2(f2(x2131,f2(x2131,a1)),a1),a1)), % 59.58/59.65 inference(scs_inference,[],[212,67,3])). % 59.58/59.65 cnf(216,plain, % 59.58/59.65 (~E(f2(f2(x2161,f2(x2161,a1)),f2(a1,f2(f2(x2162,f2(x2162,a1)),f2(a1,a1)))),f2(f2(f2(a1,f2(a1,a1)),f2(a1,a1)),a1))), % 59.58/59.65 inference(scs_inference,[],[209,89,3])). % 59.58/59.65 cnf(220,plain, % 59.58/59.65 (~E(f2(a1,f2(x2201,f2(x2201,a1))),a1)), % 59.58/59.65 inference(scs_inference,[],[216,212,68,2,3])). % 59.58/59.65 cnf(223,plain, % 59.58/59.65 (~E(f2(a1,f2(f2(x2231,f2(x2231,a1)),f2(a1,a1))),a1)), % 59.58/59.65 inference(scs_inference,[],[220,48,2,3])). % 59.58/59.65 cnf(227,plain, % 59.58/59.65 (~E(f2(a1,f2(f2(x2271,f2(x2271,a1)),f2(a1,f2(x2272,f2(x2272,a1))))),a1)), % 59.58/59.65 inference(scs_inference,[],[223,100,2,3])). % 59.58/59.65 cnf(230,plain, % 59.58/59.65 (~E(f2(f2(f2(x2301,f2(x2301,a1)),x2302),f2(f2(a1,x2302),a1)),f2(f2(f2(f2(x2303,f2(x2303,a1)),f2(x2304,f2(x2304,a1))),f2(a1,a1)),a1))), % 59.58/59.65 inference(scs_inference,[],[189,227,43,2,3])). % 59.58/59.65 cnf(233,plain, % 59.58/59.65 (~E(f2(f2(f2(f2(x2331,f2(x2331,a1)),f2(x2332,f2(x2332,a1))),f2(a1,a1)),a1),f2(f2(f2(x2333,f2(x2333,a1)),x2334),f2(f2(a1,x2334),a1)))), % 59.58/59.65 inference(scs_inference,[],[230,2])). % 59.58/59.65 cnf(234,plain, % 59.58/59.65 (~E(f2(f2(f2(f2(x2341,f2(x2341,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(x2342,f2(x2342,a1)),a1)),f2(f2(a1,f2(a1,a1)),a1))), % 59.58/59.65 inference(scs_inference,[],[200,230,82,2,3])). % 59.58/59.65 cnf(238,plain, % 59.58/59.65 (~E(f2(f2(f2(x2381,f2(x2381,a1)),f2(a1,a1)),a1),a1)), % 59.58/59.65 inference(scs_inference,[],[213,234,47,2,3])). % 59.58/59.65 cnf(242,plain, % 59.58/59.65 (~E(f2(f2(f2(x2421,f2(x2421,a1)),f2(f2(x2422,f2(x2422,a1)),a1)),a1),a1)), % 59.58/59.65 inference(scs_inference,[],[238,88,2,3])). % 59.58/59.65 cnf(245,plain, % 59.58/59.65 (~E(f2(f2(f2(x2451,f2(x2451,a1)),f2(x2452,f2(x2452,a1))),f2(f2(a1,a1),a1)),f2(f2(a3,f2(a3,a1)),f2(x2453,f2(x2453,a1))))), % 59.58/59.65 inference(scs_inference,[],[103,242,52,2,3])). % 59.58/59.65 cnf(248,plain, % 59.58/59.65 (~E(f2(f2(a3,f2(a3,a1)),f2(x2481,f2(x2481,a1))),f2(f2(f2(x2482,f2(x2482,a1)),f2(x2483,f2(x2483,a1))),f2(f2(a1,a1),a1)))), % 59.58/59.65 inference(scs_inference,[],[245,2])). % 59.58/59.65 cnf(249,plain, % 59.58/59.65 (~E(f2(a1,f2(f2(f2(x2491,f2(x2491,a1)),f2(x2492,f2(x2492,a1))),f2(a1,a1))),f2(f2(x2493,f2(x2494,f2(x2494,a1))),f2(f2(x2493,a1),a1)))), % 59.58/59.65 inference(scs_inference,[],[245,155,83,2,3])). % 59.58/59.65 cnf(252,plain, % 59.58/59.65 (~E(f2(f2(a3,f2(a3,a1)),f2(f2(x2521,f2(x2521,a1)),f2(a1,a1))),f2(f2(f2(x2522,f2(x2522,a1)),f2(x2523,f2(x2523,a1))),f2(f2(a1,a1),a1)))), % 59.58/59.65 inference(scs_inference,[],[248,249,48,2,3])). % 59.58/59.65 cnf(256,plain, % 59.58/59.65 (~E(f2(f2(f2(f2(x2561,f2(x2561,a1)),a1),f2(a1,a1)),a1),f2(f2(f2(x2562,f2(x2562,a1)),x2563),f2(f2(a1,x2563),a1)))), % 59.58/59.65 inference(scs_inference,[],[252,233,51,2,3])). % 59.58/59.65 cnf(260,plain, % 59.58/59.65 (~E(f2(f2(x2601,f2(x2601,a1)),f2(a1,f2(f2(x2602,f2(x2602,a1)),f2(a1,a1)))),f2(f2(f2(f2(x2603,f2(x2603,a1)),f2(a1,a1)),f2(a1,a1)),a1))), % 59.58/59.65 inference(scs_inference,[],[203,256,89,2,3])). % 59.58/59.65 cnf(264,plain, % 59.58/59.65 (~E(f2(f2(f2(x2641,f2(x2641,a1)),f2(a1,f2(x2642,f2(x2642,a1)))),a1),f2(f2(x2643,f2(x2643,a1)),f2(a1,a1)))), % 59.58/59.65 inference(scs_inference,[],[260,175,99,2,3])). % 59.58/59.65 cnf(267,plain, % 59.58/59.65 (~E(f2(a1,a1),f2(f2(f2(x2671,f2(x2671,a1)),f2(x2672,f2(x2672,a1))),f2(f2(a1,a1),a1)))), % 59.58/59.65 inference(scs_inference,[],[98,264,25,2,3])). % 59.58/59.65 cnf(270,plain, % 59.58/59.65 ($false), % 59.58/59.65 inference(scs_inference,[],[267,37,12,2,3]), % 59.58/59.65 ['proof']). % 59.58/59.65 % SZS output end Proof % 59.58/59.65 % Total time :59.010000s %------------------------------------------------------------------------------