%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP484-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 : 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:46 EDT 2024 % Result : Unsatisfiable 164.23s 164.27s % Output : CNFRefutation 164.32s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : GRP484-1 : TPTP v8.2.0. Released v2.6.0. % 0.10/0.12 % Command : java -jar /export/starexec/sandbox2/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 08:14:24 EDT 2024 % 0.12/0.34 % CPUTime : % 0.20/0.58 start to proof:theBenchmark % 164.23/164.24 %------------------------------------------- % 164.23/164.24 % File :CSE---1.7 % 164.23/164.24 % Problem :theBenchmark % 164.23/164.24 % Transform :cnf % 164.23/164.24 % Format :tptp:raw % 164.23/164.24 % Command :java -jar mcs_scs.jar %d %s % 164.23/164.24 % 164.23/164.24 % Result :Theorem 163.600000s % 164.23/164.24 % Output :CNFRefutation 163.600000s % 164.23/164.24 %------------------------------------------- % 164.23/164.27 %-------------------------------------------------------------------------- % 164.23/164.27 % File : GRP484-1 : TPTP v8.2.0. Released v2.6.0. % 164.23/164.27 % Domain : Group Theory % 164.23/164.27 % Problem : Axiom for group theory, in double division and identity, part 1 % 164.23/164.27 % Version : [McC93] (equality) axioms. % 164.23/164.27 % English : % 164.23/164.27 % 164.23/164.27 % Refs : [McC93] McCune (1993), Single Axioms for Groups and Abelian Gr % 164.23/164.27 % Source : [TPTP] % 164.23/164.27 % Names : % 164.23/164.27 % 164.23/164.27 % Status : Unsatisfiable % 164.23/164.27 % Rating : 0.05 v8.2.0, 0.04 v8.1.0, 0.05 v7.5.0, 0.04 v7.4.0, 0.09 v7.3.0, 0.05 v7.1.0, 0.00 v7.0.0, 0.05 v6.3.0, 0.12 v6.2.0, 0.14 v6.1.0, 0.06 v6.0.0, 0.19 v5.5.0, 0.16 v5.4.0, 0.00 v5.1.0, 0.07 v5.0.0, 0.00 v2.6.0 % 164.23/164.27 % Syntax : Number of clauses : 5 ( 5 unt; 0 nHn; 1 RR) % 164.23/164.27 % Number of literals : 5 ( 5 equ; 1 neg) % 164.23/164.27 % Maximal clause size : 1 ( 1 avg) % 164.23/164.27 % Maximal term depth : 6 ( 2 avg) % 164.23/164.27 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 164.23/164.27 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty) % 164.23/164.27 % Number of variables : 7 ( 0 sgn) % 164.23/164.27 % SPC : CNF_UNS_RFO_PEQ_UEQ % 164.23/164.27 % 164.23/164.27 % Comments : A UEQ part of GRP076-1 % 164.23/164.27 %-------------------------------------------------------------------------- % 164.23/164.27 cnf(single_axiom,axiom, % 164.23/164.27 double_divide(double_divide(A,double_divide(double_divide(double_divide(A,B),C),double_divide(B,identity))),double_divide(identity,identity)) = C ). % 164.23/164.27 % 164.23/164.27 cnf(multiply,axiom, % 164.23/164.27 multiply(A,B) = double_divide(double_divide(B,A),identity) ). % 164.23/164.27 % 164.23/164.27 cnf(inverse,axiom, % 164.23/164.27 inverse(A) = double_divide(A,identity) ). % 164.23/164.27 % 164.23/164.27 cnf(identity,axiom, % 164.23/164.27 identity = double_divide(A,inverse(A)) ). % 164.23/164.27 % 164.23/164.27 cnf(prove_these_axioms_1,negated_conjecture, % 164.23/164.27 multiply(inverse(a1),a1) != identity ). % 164.23/164.27 % 164.23/164.27 %-------------------------------------------------------------------------- % 164.23/164.27 %------------------------------------------- % 164.23/164.27 % Proof found % 164.23/164.27 % SZS status Theorem for theBenchmark % 164.23/164.27 % SZS output start Proof % 164.23/164.30 %ClaNum:8(EqnAxiom:5) % 164.23/164.30 %VarNum:8(SingletonVarNum:4) % 164.23/164.30 %MaxLitNum:1 % 164.23/164.30 %MaxfuncDepth:3 % 164.23/164.30 %SharedTerms:7 % 164.23/164.30 %goalClause: 8 % 164.23/164.30 %singleGoalClaCount:1 % 164.23/164.30 [8]~E(f2(f2(a3,f2(a3,a1)),a1),a1) % 164.23/164.30 [6]E(f2(x61,f2(x61,a1)),a1) % 164.23/164.30 [7]E(f2(f2(x71,f2(f2(f2(x71,x72),x73),f2(x72,a1))),f2(a1,a1)),x73) % 164.23/164.30 %EqnAxiom % 164.23/164.30 [1]E(x11,x11) % 164.23/164.30 [2]E(x22,x21)+~E(x21,x22) % 164.23/164.30 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 164.23/164.30 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 164.23/164.30 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 164.23/164.30 % 164.23/164.30 %------------------------------------------- % 164.32/164.33 cnf(9,plain, % 164.32/164.33 (E(x91,f2(f2(x92,f2(f2(f2(x92,x93),x91),f2(x93,a1))),f2(a1,a1)))), % 164.32/164.33 inference(scs_inference,[],[7,2])). % 164.32/164.33 cnf(10,plain, % 164.32/164.33 (~E(f2(f2(a3,f2(a3,a1)),a1),f2(x101,f2(x101,a1)))), % 164.32/164.33 inference(scs_inference,[],[8,7,6,2,3])). % 164.32/164.33 cnf(11,plain, % 164.32/164.33 (~E(a1,f2(f2(a3,f2(a3,a1)),a1))), % 164.32/164.33 inference(scs_inference,[],[8,7,6,2,3,5])). % 164.32/164.33 cnf(12,plain, % 164.32/164.33 (E(a1,f2(x121,f2(x121,a1)))), % 164.32/164.33 inference(scs_inference,[],[6,2])). % 164.32/164.33 cnf(13,plain, % 164.32/164.33 (E(f2(x131,f2(x131,a1)),f2(f2(x132,f2(f2(f2(x132,x133),a1),f2(x133,a1))),f2(a1,a1)))), % 164.32/164.33 inference(scs_inference,[],[6,9,3])). % 164.32/164.33 cnf(15,plain, % 164.32/164.33 (E(f2(f2(x151,f2(f2(f2(x151,x152),a1),f2(x152,a1))),f2(a1,a1)),f2(x153,f2(x153,a1)))), % 164.32/164.33 inference(scs_inference,[],[6,9,3,2])). % 164.32/164.33 cnf(16,plain, % 164.32/164.33 (~E(f2(f2(a3,f2(a3,a1)),a1),f2(f2(x161,f2(f2(f2(x161,x162),a1),f2(x162,a1))),f2(a1,a1)))), % 164.32/164.33 inference(scs_inference,[],[10,15,3])). % 164.32/164.33 cnf(18,plain, % 164.32/164.33 (E(f2(f2(x181,f2(x181,a1)),x182),f2(a1,x182))), % 164.32/164.33 inference(scs_inference,[],[6,4])). % 164.32/164.33 cnf(19,plain, % 164.32/164.33 (E(f2(x191,f2(x192,f2(x192,a1))),f2(x191,a1))), % 164.32/164.33 inference(scs_inference,[],[6,4,5])). % 164.32/164.33 cnf(21,plain, % 164.32/164.33 (~E(f2(x211,f2(x211,a1)),f2(f2(a3,f2(a3,a1)),a1))), % 164.32/164.33 inference(scs_inference,[],[6,12,11,16,4,5,2,3])). % 164.32/164.33 cnf(23,plain, % 164.32/164.33 (E(f2(x231,f2(f2(x232,f2(x232,a1)),x233)),f2(x231,f2(a1,x233)))), % 164.32/164.33 inference(scs_inference,[],[18,4,5])). % 164.32/164.33 cnf(24,plain, % 164.32/164.33 (E(f2(f2(x241,f2(x241,a1)),f2(x242,f2(x242,a1))),f2(a1,a1))), % 164.32/164.33 inference(scs_inference,[],[18,19,4,5,3])). % 164.32/164.33 cnf(29,plain, % 164.32/164.33 (~E(f2(f2(x291,f2(x291,a1)),f2(a1,a1)),f2(f2(a3,f2(a3,a1)),a1))), % 164.32/164.33 inference(scs_inference,[],[24,21,23,4,5,3])). % 164.32/164.33 cnf(32,plain, % 164.32/164.33 (E(f2(a1,x321),f2(f2(x322,f2(x322,a1)),x321))), % 164.32/164.33 inference(scs_inference,[],[12,4])). % 164.32/164.33 cnf(33,plain, % 164.32/164.33 (E(f2(x331,a1),f2(x331,f2(x332,f2(x332,a1))))), % 164.32/164.33 inference(scs_inference,[],[12,4,5])). % 164.32/164.33 cnf(34,plain, % 164.32/164.33 (~E(f2(f2(a3,f2(a3,a1)),a1),f2(f2(x341,f2(x341,a1)),f2(a1,a1)))), % 164.32/164.33 inference(scs_inference,[],[29,12,4,5,2])). % 164.32/164.33 cnf(35,plain, % 164.32/164.33 (E(f2(f2(a1,x351),x352),f2(f2(f2(x353,f2(x353,a1)),x351),x352))), % 164.32/164.33 inference(scs_inference,[],[32,4])). % 164.32/164.33 cnf(36,plain, % 164.32/164.33 (E(f2(x361,f2(a1,x362)),f2(x361,f2(f2(x363,f2(x363,a1)),x362)))), % 164.32/164.33 inference(scs_inference,[],[32,4,5])). % 164.32/164.33 cnf(37,plain, % 164.32/164.33 (~E(f2(f2(a3,f2(a3,a1)),f2(x371,f2(x371,a1))),f2(f2(x372,f2(x372,a1)),f2(a1,a1)))), % 164.32/164.33 inference(scs_inference,[],[32,33,34,4,5,3])). % 164.32/164.33 cnf(39,plain, % 164.32/164.33 (~E(f2(f2(x391,f2(x391,a1)),f2(a1,a1)),f2(f2(a3,f2(a3,a1)),f2(x392,f2(x392,a1))))), % 164.32/164.33 inference(scs_inference,[],[32,33,34,4,5,3,2])). % 164.32/164.33 cnf(41,plain, % 164.32/164.33 (E(f2(x411,f2(x412,f2(x413,f2(x413,a1)))),f2(x411,f2(x412,a1)))), % 164.32/164.33 inference(scs_inference,[],[19,4,5])). % 164.32/164.33 cnf(42,plain, % 164.32/164.33 (~E(f2(f2(f2(x421,f2(x421,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(a3,f2(a3,a1)),f2(x422,f2(x422,a1))))), % 164.32/164.33 inference(scs_inference,[],[39,35,19,4,5,3])). % 164.32/164.33 cnf(47,plain, % 164.32/164.33 (~E(f2(f2(a3,f2(a3,a1)),f2(x471,f2(x471,a1))),f2(f2(f2(x472,f2(x472,a1)),f2(a1,a1)),f2(a1,a1)))), % 164.32/164.33 inference(scs_inference,[],[42,33,4,5,2])). % 164.32/164.33 cnf(48,plain, % 164.32/164.33 (~E(f2(f2(a3,f2(a3,a1)),f2(f2(x481,f2(x481,a1)),f2(a1,a1))),f2(f2(x482,f2(x482,a1)),f2(a1,a1)))), % 164.32/164.33 inference(scs_inference,[],[37,42,36,33,4,5,2,3])). % 164.32/164.33 cnf(51,plain, % 164.32/164.33 (E(f2(x511,x512),f2(f2(f2(x513,f2(f2(f2(x513,x514),x511),f2(x514,a1))),f2(a1,a1)),x512))), % 164.32/164.33 inference(scs_inference,[],[9,4])). % 164.32/164.33 cnf(52,plain, % 164.32/164.33 (E(f2(x521,x522),f2(x521,f2(f2(x523,f2(f2(f2(x523,x524),x522),f2(x524,a1))),f2(a1,a1))))), % 164.32/164.33 inference(scs_inference,[],[9,4,5])). % 164.32/164.33 cnf(53,plain, % 164.32/164.33 (~E(f2(f2(x531,f2(x531,a1)),f2(a1,a1)),f2(f2(a3,f2(a3,a1)),f2(f2(x532,f2(x532,a1)),f2(a1,a1))))), % 164.32/164.33 inference(scs_inference,[],[48,9,4,5,2])). % 164.32/164.33 cnf(54,plain, % 164.32/164.33 (E(f2(x541,f2(x541,f2(x542,f2(x542,a1)))),a1)), % 164.32/164.33 inference(scs_inference,[],[6,41,48,9,4,5,2,3])). % 164.32/164.33 cnf(59,plain, % 164.32/164.33 (~E(f2(f2(f2(x591,f2(x591,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(a3,f2(a3,a1)),f2(f2(x592,f2(x592,a1)),f2(a1,a1))))), % 164.32/164.33 inference(scs_inference,[],[53,35,3])). % 164.32/164.33 cnf(62,plain, % 164.32/164.33 (~E(f2(f2(a3,f2(a3,a1)),f2(f2(x621,f2(x621,a1)),f2(a1,a1))),f2(f2(f2(x622,f2(x622,a1)),f2(a1,a1)),f2(a1,a1)))), % 164.32/164.33 inference(scs_inference,[],[59,2])). % 164.32/164.33 cnf(63,plain, % 164.32/164.33 (~E(f2(a1,a1),f2(f2(f2(x631,f2(x631,a1)),f2(a1,a1)),f2(a1,a1)))), % 164.32/164.33 inference(scs_inference,[],[47,24,3])). % 164.32/164.33 cnf(88,plain, % 164.32/164.33 (~E(f2(a1,f2(f2(x881,f2(x881,a1)),f2(a1,a1))),f2(f2(f2(x882,f2(x882,a1)),f2(a1,a1)),f2(a1,a1)))), % 164.32/164.33 inference(scs_inference,[],[18,62,3])). % 164.32/164.33 cnf(91,plain, % 164.32/164.33 (~E(f2(a1,f2(a1,f2(a1,a1))),f2(f2(f2(x911,f2(x911,a1)),f2(a1,a1)),f2(a1,a1)))), % 164.32/164.33 inference(scs_inference,[],[88,23,3])). % 164.32/164.33 cnf(94,plain, % 164.32/164.33 (~E(f2(a1,a1),a1)), % 164.32/164.33 inference(scs_inference,[],[18,91,8,2,3])). % 164.32/164.33 cnf(96,plain, % 164.32/164.33 (~E(a1,f2(a1,a1))), % 164.32/164.33 inference(scs_inference,[],[94,2])). % 164.32/164.33 cnf(97,plain, % 164.32/164.33 (~E(f2(f2(f2(x971,f2(f2(f2(x971,x972),a1),f2(x972,a1))),f2(a1,a1)),a1),a1)), % 164.32/164.33 inference(scs_inference,[],[94,51,2,3])). % 164.32/164.33 cnf(99,plain, % 164.32/164.33 (~E(a1,f2(f2(f2(x991,f2(f2(f2(x991,x992),a1),f2(x992,a1))),f2(a1,a1)),a1))), % 164.32/164.33 inference(scs_inference,[],[97,2])). % 164.32/164.33 cnf(100,plain, % 164.32/164.33 (~E(f2(f2(x1001,f2(f2(f2(x1001,x1002),a1),f2(x1002,a1))),f2(a1,a1)),f2(a1,a1))), % 164.32/164.33 inference(scs_inference,[],[96,97,9,2,3])). % 164.32/164.33 cnf(103,plain, % 164.32/164.33 (~E(f2(x1031,f2(x1031,a1)),f2(a1,a1))), % 164.32/164.33 inference(scs_inference,[],[100,15,2,3])). % 164.32/164.33 cnf(105,plain, % 164.32/164.33 (~E(f2(a1,a1),f2(x1051,f2(x1051,a1)))), % 164.32/164.33 inference(scs_inference,[],[103,2])). % 164.32/164.33 cnf(106,plain, % 164.32/164.33 (~E(f2(a1,f2(f2(x1061,f2(x1061,a1)),a1)),f2(a1,a1))), % 164.32/164.33 inference(scs_inference,[],[18,103,2,3])). % 164.32/164.33 cnf(110,plain, % 164.32/164.33 (~E(f2(a1,f2(f2(x1101,f2(f2(f2(x1101,x1102),a1),f2(x1102,a1))),f2(a1,a1))),f2(x1103,f2(x1103,a1)))), % 164.32/164.33 inference(scs_inference,[],[105,106,52,2,3])). % 164.32/164.33 cnf(113,plain, % 164.32/164.33 (~E(f2(x1131,f2(x1131,a1)),f2(f2(f2(x1132,f2(f2(f2(x1132,x1133),a1),f2(x1133,a1))),f2(a1,a1)),a1))), % 164.32/164.33 inference(scs_inference,[],[99,110,12,2,3])). % 164.32/164.33 cnf(115,plain, % 164.32/164.33 (~E(f2(a1,f2(x1151,f2(x1151,a1))),f2(f2(f2(x1152,f2(x1152,a1)),f2(a1,a1)),f2(a1,a1)))), % 164.32/164.33 inference(scs_inference,[],[63,113,33,2,3])). % 164.32/164.33 cnf(118,plain, % 164.32/164.33 (~E(f2(a1,a1),f2(f2(x1181,f2(x1181,a1)),f2(a1,a1)))), % 164.32/164.33 inference(scs_inference,[],[18,115,34,2,3])). % 164.32/164.34 cnf(192,plain, % 164.32/164.34 (~E(f2(x1921,f2(x1921,a1)),f2(a1,f2(x1922,f2(x1922,a1))))), % 164.32/164.34 inference(scs_inference,[],[33,105,3,2])). % 164.32/164.34 cnf(195,plain, % 164.32/164.34 (~E(f2(a1,f2(x1951,f2(x1951,a1))),f2(f2(x1952,f2(f2(f2(x1952,x1953),a1),f2(x1953,a1))),f2(a1,a1)))), % 164.32/164.34 inference(scs_inference,[],[192,13,3,2])). % 164.32/164.34 cnf(264,plain, % 164.32/164.34 (~E(f2(f2(x2641,f2(f2(f2(x2641,x2642),f2(a1,a1)),f2(x2642,a1))),f2(a1,a1)),a1)), % 164.32/164.34 inference(scs_inference,[],[94,9,3])). % 164.32/164.34 cnf(266,plain, % 164.32/164.34 (~E(a1,f2(f2(x2661,f2(f2(f2(x2661,x2662),f2(a1,a1)),f2(x2662,a1))),f2(a1,a1)))), % 164.32/164.34 inference(scs_inference,[],[94,9,3,2])). % 164.32/164.34 cnf(275,plain, % 164.32/164.34 (~E(f2(f2(x2751,f2(f2(f2(x2751,x2752),f2(a1,a1)),f2(x2752,a1))),f2(a1,a1)),f2(f2(x2753,f2(x2753,a1)),f2(a1,a1)))), % 164.32/164.34 inference(scs_inference,[],[118,9,3])). % 164.32/164.34 cnf(277,plain, % 164.32/164.34 (~E(f2(f2(x2771,f2(x2771,a1)),f2(a1,a1)),f2(f2(x2772,f2(f2(f2(x2772,x2773),f2(a1,a1)),f2(x2773,a1))),f2(a1,a1)))), % 164.32/164.34 inference(scs_inference,[],[118,9,3,2])). % 164.32/164.34 cnf(315,plain, % 164.32/164.34 (~E(f2(f2(f2(x3151,f2(x3151,a1)),f2(f2(f2(a1,x3152),f2(a1,a1)),f2(x3152,a1))),f2(a1,a1)),a1)), % 164.32/164.34 inference(scs_inference,[],[264,35,3])). % 164.32/164.34 cnf(318,plain, % 164.32/164.34 (~E(a1,f2(f2(f2(x3181,f2(x3181,a1)),f2(f2(f2(a1,x3182),f2(a1,a1)),f2(x3182,a1))),f2(a1,a1)))), % 164.32/164.34 inference(scs_inference,[],[315,2])). % 164.32/164.34 cnf(327,plain, % 164.32/164.34 (~E(f2(f2(f2(x3271,f2(x3271,a1)),f2(f2(f2(a1,x3272),f2(a1,a1)),f2(x3272,a1))),f2(a1,a1)),f2(f2(x3273,f2(x3273,a1)),f2(a1,a1)))), % 164.32/164.34 inference(scs_inference,[],[275,35,3])). % 164.32/164.34 cnf(330,plain, % 164.32/164.34 (~E(f2(f2(x3301,f2(x3301,a1)),f2(a1,a1)),f2(f2(f2(x3302,f2(x3302,a1)),f2(f2(f2(a1,x3303),f2(a1,a1)),f2(x3303,a1))),f2(a1,a1)))), % 164.32/164.34 inference(scs_inference,[],[327,2])). % 164.32/164.34 cnf(420,plain, % 164.32/164.34 (~E(f2(x4201,a1),f2(f2(f2(x4201,x4202),f2(a1,a1)),f2(x4202,a1)))), % 164.32/164.34 inference(scs_inference,[],[277,4,5])). % 164.32/164.34 cnf(424,plain, % 164.32/164.34 (~E(f2(f2(x4241,f2(x4241,a1)),a1),f2(f2(f2(a1,x4242),f2(a1,a1)),f2(x4242,a1)))), % 164.32/164.34 inference(scs_inference,[],[54,330,4,2,5])). % 164.32/164.34 cnf(584,plain, % 164.32/164.34 (~E(f2(f2(f2(x5841,x5842),f2(a1,f2(x5843,f2(x5843,a1)))),f2(x5842,a1)),f2(f2(f2(x5841,x5844),a1),f2(x5844,a1)))), % 164.32/164.34 inference(scs_inference,[],[9,195,3,4,5])). % 164.32/164.34 cnf(587,plain, % 164.32/164.34 (~E(f2(f2(x5871,f2(f2(f2(x5871,x5872),f2(x5873,a1)),f2(x5872,a1))),f2(a1,a1)),f2(f2(f2(x5873,x5874),f2(a1,a1)),f2(x5874,a1)))), % 164.32/164.34 inference(scs_inference,[],[9,584,420,4,3])). % 164.32/164.34 cnf(592,plain, % 164.32/164.34 (~E(f2(f2(x5921,f2(f2(f2(x5921,x5922),f2(f2(x5923,f2(x5923,a1)),a1)),f2(x5922,a1))),f2(a1,a1)),f2(f2(f2(a1,x5924),f2(a1,a1)),f2(x5924,a1)))), % 164.32/164.34 inference(scs_inference,[],[9,587,424,4,5,3])). % 164.32/164.34 cnf(597,plain, % 164.32/164.34 (~E(f2(f2(x5971,f2(f2(f2(x5971,x5972),a1),f2(x5972,a1))),f2(a1,a1)),f2(f2(x5973,f2(f2(f2(x5973,x5974),f2(a1,a1)),f2(x5974,a1))),f2(a1,a1)))), % 164.32/164.34 inference(scs_inference,[],[9,592,266,4,5,3])). % 164.32/164.34 cnf(600,plain, % 164.32/164.34 (~E(f2(f2(f2(x6001,x6002),a1),f2(x6002,a1)),f2(f2(f2(x6001,x6003),f2(a1,a1)),f2(x6003,a1)))), % 164.32/164.34 inference(scs_inference,[],[597,4,5])). % 164.32/164.34 cnf(601,plain, % 164.32/164.34 (~E(f2(f2(x6011,f2(f2(f2(x6011,x6012),a1),f2(x6012,a1))),f2(a1,a1)),f2(f2(f2(x6013,f2(x6013,a1)),f2(f2(f2(a1,x6014),f2(a1,a1)),f2(x6014,a1))),f2(a1,a1)))), % 164.32/164.34 inference(scs_inference,[],[9,597,318,4,5,3])). % 164.32/164.34 cnf(605,plain, % 164.32/164.34 (~E(f2(f2(x6051,f2(f2(f2(x6051,x6052),f2(f2(f2(x6053,x6054),a1),f2(x6054,a1))),f2(x6052,a1))),f2(a1,a1)),f2(f2(f2(x6053,x6055),f2(a1,a1)),f2(x6055,a1)))), % 164.32/164.34 inference(scs_inference,[],[9,601,600,4,5,3])). % 164.32/164.34 cnf(607,plain, % 164.32/164.34 (~E(f2(f2(x6071,x6072),a1),f2(f2(x6071,x6072),f2(a1,a1)))), % 164.32/164.34 inference(scs_inference,[],[600,4])). % 164.32/164.34 cnf(614,plain, % 164.32/164.34 (~E(f2(f2(x6141,f2(f2(f2(x6141,x6142),f2(f2(x6143,x6144),a1)),f2(x6142,a1))),f2(a1,a1)),f2(f2(x6143,x6144),f2(a1,a1)))), % 164.32/164.34 inference(scs_inference,[],[9,605,607,4,5,3])). % 164.32/164.34 cnf(617,plain, % 164.32/164.34 (~E(f2(f2(f2(x6171,x6172),f2(f2(x6171,x6173),a1)),f2(x6172,a1)),x6173)), % 164.32/164.34 inference(scs_inference,[],[614,4,5])). % 164.32/164.34 cnf(1208,plain, % 164.32/164.34 ($false), % 164.32/164.34 inference(scs_inference,[],[18,6,617,3]), % 164.32/164.34 ['proof']). % 164.32/164.34 % SZS output end Proof % 164.32/164.34 % Total time :163.600000s %------------------------------------------------------------------------------