%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : ANA032-2 : TPTP v8.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n001.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 04:13:58 EDT 2024 % Result : Unsatisfiable 63.73s 63.76s % Output : CNFRefutation 63.73s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : ANA032-2 : TPTP v8.2.0. Released v3.2.0. % 0.12/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n001.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 : Sun Jun 23 04:32:53 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.56 start to proof:theBenchmark % 63.73/63.74 %------------------------------------------- % 63.73/63.74 % File :CSE---1.7 % 63.73/63.74 % Problem :theBenchmark % 63.73/63.74 % Transform :cnf % 63.73/63.74 % Format :tptp:raw % 63.73/63.74 % Command :java -jar mcs_scs.jar %d %s % 63.73/63.74 % 63.73/63.74 % Result :Theorem 63.150000s % 63.73/63.74 % Output :CNFRefutation 63.150000s % 63.73/63.74 %------------------------------------------- % 63.73/63.75 %------------------------------------------------------------------------------ % 63.73/63.75 % File : ANA032-2 : TPTP v8.2.0. Released v3.2.0. % 63.73/63.75 % Domain : Analysis % 63.73/63.75 % Problem : Problem about Big-O notation % 63.73/63.75 % Version : [Pau06] axioms : Reduced > Especial. % 63.73/63.75 % English : % 63.73/63.75 % 63.73/63.75 % Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe % 63.73/63.75 % Source : [Pau06] % 63.73/63.75 % Names : % 63.73/63.76 % 63.73/63.76 % Status : Unsatisfiable % 63.73/63.76 % Rating : 0.06 v8.2.0, 0.08 v8.1.0, 0.00 v7.5.0, 0.10 v7.4.0, 0.11 v7.2.0, 0.12 v7.1.0, 0.14 v6.3.0, 0.17 v6.2.0, 0.00 v6.1.0, 0.20 v6.0.0, 0.11 v5.5.0, 0.31 v5.4.0, 0.27 v5.3.0, 0.42 v5.2.0, 0.12 v5.1.0, 0.14 v5.0.0, 0.29 v4.1.0, 0.22 v4.0.1, 0.33 v3.3.0, 0.43 v3.2.0 % 63.73/63.76 % Syntax : Number of clauses : 11 ( 3 unt; 0 nHn; 8 RR) % 63.73/63.76 % Number of literals : 21 ( 2 equ; 11 neg) % 63.73/63.76 % Maximal clause size : 4 ( 1 avg) % 63.73/63.76 % Maximal term depth : 5 ( 1 avg) % 63.73/63.76 % Number of predicates : 7 ( 6 usr; 0 prp; 1-3 aty) % 63.73/63.76 % Number of functors : 9 ( 9 usr; 4 con; 0-3 aty) % 63.73/63.76 % Number of variables : 17 ( 1 sgn) % 63.73/63.76 % SPC : CNF_UNS_RFO_SEQ_HRN % 63.73/63.76 % 63.73/63.76 % Comments : The problems in the [Pau06] collection each have very many axioms, % 63.73/63.76 % of which only a small selection are required for the refutation. % 63.73/63.76 % The mission is to find those few axioms, after which a refutation % 63.73/63.76 % can be quite easily found. This version has only the necessary % 63.73/63.76 % axioms. % 63.73/63.76 %------------------------------------------------------------------------------ % 63.73/63.76 cnf(cls_OrderedGroup_Oabs__ge__zero_0,axiom, % 63.73/63.76 ( ~ class_OrderedGroup_Olordered__ab__group__abs(T_a) % 63.73/63.76 | c_lessequals(c_0,c_HOL_Oabs(V_a,T_a),T_a) ) ). % 63.73/63.76 % 63.73/63.76 cnf(cls_OrderedGroup_Omult__ac__1_0,axiom, % 63.73/63.76 ( ~ class_OrderedGroup_Osemigroup__mult(T_a) % 63.73/63.76 | c_times(c_times(V_a,V_b,T_a),V_c,T_a) = c_times(V_a,c_times(V_b,V_c,T_a),T_a) ) ). % 63.73/63.76 % 63.73/63.76 cnf(cls_OrderedGroup_Omult__ac__2_0,axiom, % 63.73/63.76 ( ~ class_OrderedGroup_Oab__semigroup__mult(T_a) % 63.73/63.76 | c_times(V_a,V_b,T_a) = c_times(V_b,V_a,T_a) ) ). % 63.73/63.76 % 63.73/63.76 cnf(cls_Ring__and__Field_Opordered__semiring__class_Omult__left__mono_0,axiom, % 63.73/63.76 ( ~ class_Ring__and__Field_Opordered__semiring(T_a) % 63.73/63.76 | ~ c_lessequals(V_a,V_b,T_a) % 63.73/63.76 | ~ c_lessequals(c_0,V_c,T_a) % 63.73/63.76 | c_lessequals(c_times(V_c,V_a,T_a),c_times(V_c,V_b,T_a),T_a) ) ). % 63.73/63.76 % 63.73/63.76 cnf(cls_conjecture_0,negated_conjecture, % 63.73/63.76 c_lessequals(c_HOL_Oabs(v_b(v_x),t_b),c_times(v_c,c_HOL_Oabs(v_g(v_x),t_b),t_b),t_b) ). % 63.73/63.76 % 63.73/63.76 cnf(cls_conjecture_1,negated_conjecture, % 63.73/63.76 ~ c_lessequals(c_times(c_HOL_Oabs(v_b(v_x),t_b),c_HOL_Oabs(v_f(v_x),t_b),t_b),c_times(v_c,c_times(c_HOL_Oabs(v_f(v_x),t_b),c_HOL_Oabs(v_g(v_x),t_b),t_b),t_b),t_b) ). % 63.73/63.76 % 63.73/63.76 cnf(clsrel_Ring__and__Field_Oordered__idom_17,axiom, % 63.73/63.76 ( ~ class_Ring__and__Field_Oordered__idom(T) % 63.73/63.76 | class_OrderedGroup_Oab__semigroup__mult(T) ) ). % 63.73/63.76 % 63.73/63.76 cnf(clsrel_Ring__and__Field_Oordered__idom_21,axiom, % 63.73/63.76 ( ~ class_Ring__and__Field_Oordered__idom(T) % 63.73/63.76 | class_OrderedGroup_Osemigroup__mult(T) ) ). % 63.73/63.76 % 63.73/63.76 cnf(clsrel_Ring__and__Field_Oordered__idom_42,axiom, % 63.73/63.76 ( ~ class_Ring__and__Field_Oordered__idom(T) % 63.73/63.76 | class_Ring__and__Field_Opordered__semiring(T) ) ). % 63.73/63.76 % 63.73/63.76 cnf(clsrel_Ring__and__Field_Oordered__idom_50,axiom, % 63.73/63.76 ( ~ class_Ring__and__Field_Oordered__idom(T) % 63.73/63.76 | class_OrderedGroup_Olordered__ab__group__abs(T) ) ). % 63.73/63.76 % 63.73/63.76 cnf(tfree_tcs,negated_conjecture, % 63.73/63.76 class_Ring__and__Field_Oordered__idom(t_b) ). % 63.73/63.76 % 63.73/63.76 %------------------------------------------------------------------------------ % 63.73/63.76 %------------------------------------------- % 63.73/63.76 % Proof found % 63.73/63.76 % SZS status Theorem for theBenchmark % 63.73/63.76 % SZS output start Proof % 63.73/63.76 %ClaNum:30(EqnAxiom:19) % 63.73/63.76 %VarNum:43(SingletonVarNum:17) % 63.73/63.76 %MaxLitNum:4 % 63.73/63.76 %MaxfuncDepth:4 % 63.73/63.76 %SharedTerms:17 % 63.73/63.76 %goalClause: 20 21 22 % 63.73/63.76 %singleGoalClaCount:3 % 63.73/63.76 [20]P1(a1) % 63.73/63.76 [21]P2(f2(f6(a5),a1),f4(a7,f2(f8(a5),a1),a1),a1) % 63.73/63.76 [22]~P2(f4(f2(f6(a5),a1),f2(f9(a5),a1),a1),f4(a7,f4(f2(f9(a5),a1),f2(f8(a5),a1),a1),a1),a1) % 63.73/63.76 [23]~P1(x231)+P3(x231) % 63.73/63.76 [24]~P1(x241)+P5(x241) % 63.73/63.76 [25]~P1(x251)+P4(x251) % 63.73/63.76 [26]~P1(x261)+P6(x261) % 63.73/63.76 [27]~P3(x272)+P2(a3,f2(x271,x272),x272) % 63.73/63.76 [28]~P4(x283)+E(f4(x281,x282,x283),f4(x282,x281,x283)) % 63.73/63.76 [29]~P5(x293)+E(f4(f4(x291,x292,x293),x294,x293),f4(x291,f4(x292,x294,x293),x293)) % 63.73/63.76 [30]~P6(x303)+~P2(x302,x304,x303)+~P2(a3,x301,x303)+P2(f4(x301,x302,x303),f4(x301,x304,x303),x303) % 63.73/63.76 %EqnAxiom % 63.73/63.76 [1]E(x11,x11) % 63.73/63.76 [2]E(x22,x21)+~E(x21,x22) % 63.73/63.76 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 63.73/63.76 [4]~E(x41,x42)+E(f6(x41),f6(x42)) % 63.73/63.76 [5]~E(x51,x52)+E(f2(x51,x53),f2(x52,x53)) % 63.73/63.76 [6]~E(x61,x62)+E(f2(x63,x61),f2(x63,x62)) % 63.73/63.76 [7]~E(x71,x72)+E(f8(x71),f8(x72)) % 63.73/63.76 [8]~E(x81,x82)+E(f4(x81,x83,x84),f4(x82,x83,x84)) % 63.73/63.76 [9]~E(x91,x92)+E(f4(x93,x91,x94),f4(x93,x92,x94)) % 63.73/63.76 [10]~E(x101,x102)+E(f4(x103,x104,x101),f4(x103,x104,x102)) % 63.73/63.76 [11]~E(x111,x112)+E(f9(x111),f9(x112)) % 63.73/63.76 [12]~P1(x121)+P1(x122)+~E(x121,x122) % 63.73/63.76 [13]P2(x132,x133,x134)+~E(x131,x132)+~P2(x131,x133,x134) % 63.73/63.76 [14]P2(x143,x142,x144)+~E(x141,x142)+~P2(x143,x141,x144) % 63.73/63.76 [15]P2(x153,x154,x152)+~E(x151,x152)+~P2(x153,x154,x151) % 63.73/63.76 [16]~P5(x161)+P5(x162)+~E(x161,x162) % 63.73/63.76 [17]~P3(x171)+P3(x172)+~E(x171,x172) % 63.73/63.76 [18]~P4(x181)+P4(x182)+~E(x181,x182) % 63.73/63.76 [19]~P6(x191)+P6(x192)+~E(x191,x192) % 63.73/63.76 % 63.73/63.76 %------------------------------------------- % 63.73/63.79 cnf(41,plain, % 63.73/63.79 (P2(a3,f2(x411,a1),a1)), % 63.73/63.79 inference(scs_inference,[],[20,23,27])). % 63.73/63.79 cnf(48,plain, % 63.73/63.79 (E(f4(f4(x481,x482,a1),x483,a1),f4(x481,f4(x482,x483,a1),a1))), % 63.73/63.79 inference(scs_inference,[],[20,24,29])). % 63.73/63.79 cnf(49,plain, % 63.73/63.79 (E(f4(x491,f4(x492,x493,a1),a1),f4(f4(x491,x492,a1),x493,a1))), % 63.73/63.79 inference(scs_inference,[],[48,2])). % 63.73/63.79 cnf(55,plain, % 63.73/63.79 (E(f4(x551,x552,a1),f4(x552,x551,a1))), % 63.73/63.79 inference(scs_inference,[],[20,25,28])). % 63.73/63.79 cnf(56,plain, % 63.73/63.79 (E(f4(f4(x561,x562,a1),x563,a1),f4(f4(x563,x561,a1),x562,a1))), % 63.73/63.79 inference(scs_inference,[],[55,49,3])). % 63.73/63.79 cnf(58,plain, % 63.73/63.79 (E(f4(x581,x582,a1),f4(x582,x581,a1))), % 63.73/63.79 inference(rename_variables,[],[55])). % 63.73/63.79 cnf(59,plain, % 63.73/63.79 (P2(f2(f6(a5),a1),f4(f2(f8(a5),a1),a7,a1),a1)), % 63.73/63.79 inference(scs_inference,[],[21,55,58,49,3,14])). % 63.73/63.79 cnf(61,plain, % 63.73/63.79 (E(f4(f4(x611,x612,a1),x613,a1),f4(f4(x612,x613,a1),x611,a1))), % 63.73/63.79 inference(scs_inference,[],[21,55,58,49,3,14,2])). % 63.73/63.79 cnf(71,plain, % 63.73/63.79 (P2(f4(f2(x711,a1),f2(f6(a5),a1),a1),f4(f2(x711,a1),f4(a7,f2(f8(a5),a1),a1),a1),a1)), % 63.73/63.79 inference(scs_inference,[],[20,41,21,26,30])). % 63.73/63.79 cnf(72,plain, % 63.73/63.79 (E(f4(f4(x721,f4(x722,x723,a1),a1),x724,a1),f4(f4(f4(x724,x721,a1),x722,a1),x723,a1))), % 63.73/63.79 inference(scs_inference,[],[56,49,3])). % 63.73/63.79 cnf(76,plain, % 63.73/63.79 (E(f4(x761,x762,a1),f4(x762,x761,a1))), % 63.73/63.79 inference(rename_variables,[],[55])). % 63.73/63.79 cnf(77,plain, % 63.73/63.79 (P2(f4(f2(x771,a1),f2(f6(a5),a1),a1),f4(f4(a7,f2(f8(a5),a1),a1),f2(x771,a1),a1),a1)), % 63.73/63.79 inference(scs_inference,[],[56,71,55,76,49,3,13,14])). % 63.73/63.79 cnf(79,plain, % 63.73/63.79 (E(f4(f4(f4(x791,x792,a1),x793,a1),x794,a1),f4(f4(x792,f4(x793,x794,a1),a1),x791,a1))), % 63.73/63.79 inference(scs_inference,[],[56,71,55,76,49,3,13,14,2])). % 63.73/63.79 cnf(84,plain, % 63.73/63.79 (E(f4(f4(x841,f4(x842,x843,a1),a1),x844,a1),f4(f4(x843,f4(x844,x841,a1),a1),x842,a1))), % 63.73/63.79 inference(scs_inference,[],[61,79,3])). % 63.73/63.79 cnf(86,plain, % 63.73/63.79 (E(f4(f4(x861,x862,a1),x863,a1),f4(f4(x862,x863,a1),x861,a1))), % 63.73/63.79 inference(rename_variables,[],[61])). % 63.73/63.79 cnf(89,plain, % 63.73/63.79 (P2(f4(f2(x891,a1),f2(f6(a5),a1),a1),f4(f4(f2(f8(a5),a1),f2(x891,a1),a1),a7,a1),a1)), % 63.73/63.79 inference(scs_inference,[],[61,86,79,77,55,3,13,14])). % 63.73/63.79 cnf(104,plain, % 63.73/63.79 (E(f4(f4(f4(x1041,x1042,a1),x1043,a1),x1044,a1),f4(f4(f4(x1043,x1044,a1),x1041,a1),x1042,a1))), % 63.73/63.79 inference(scs_inference,[],[56,72,3])). % 63.73/63.79 cnf(106,plain, % 63.73/63.79 (E(f4(f4(x1061,x1062,a1),x1063,a1),f4(f4(x1063,x1061,a1),x1062,a1))), % 63.73/63.79 inference(rename_variables,[],[56])). % 63.73/63.79 cnf(109,plain, % 63.73/63.79 (P2(f4(f2(x1091,a1),f2(f6(a5),a1),a1),f4(f4(f2(x1091,a1),a7,a1),f2(f8(a5),a1),a1),a1)), % 63.73/63.79 inference(scs_inference,[],[56,106,72,89,77,55,3,13,14])). % 63.73/63.79 cnf(121,plain, % 63.73/63.79 (E(f4(x1211,f4(f4(x1212,x1213,a1),x1214,a1),a1),f4(f4(f4(x1214,x1211,a1),x1212,a1),x1213,a1))), % 63.73/63.79 inference(scs_inference,[],[49,72,3])). % 63.73/63.79 cnf(124,plain, % 63.73/63.79 (P2(f4(f2(x1241,a1),f2(f6(a5),a1),a1),f4(f2(f8(a5),a1),f4(f2(x1241,a1),a7,a1),a1),a1)), % 63.73/63.79 inference(scs_inference,[],[49,48,72,89,3,14])). % 63.73/63.79 cnf(128,plain, % 63.73/63.79 (E(f4(f4(f4(x1281,x1282,a1),x1283,a1),x1284,a1),f4(x1282,f4(f4(x1283,x1284,a1),x1281,a1),a1))), % 63.73/63.79 inference(scs_inference,[],[49,48,72,109,89,55,3,14,13,2])). % 63.73/63.79 cnf(148,plain, % 63.73/63.79 (P2(f4(f2(x1481,a1),f2(f6(a5),a1),a1),f4(a7,f4(f2(f8(a5),a1),f2(x1481,a1),a1),a1),a1)), % 63.73/63.79 inference(scs_inference,[],[49,48,121,124,77,55,3,13,14])). % 63.73/63.79 cnf(150,plain, % 63.73/63.79 (E(f4(f4(f4(x1501,f4(x1502,x1503,a1),a1),x1504,a1),x1505,a1),f4(x1502,f4(x1503,f4(f4(x1504,x1505,a1),x1501,a1),a1),a1))), % 63.73/63.79 inference(scs_inference,[],[49,48,121,124,77,55,3,13,14,2])). % 63.73/63.79 cnf(169,plain, % 63.73/63.79 (E(f6(f4(f4(x1691,x1692,a1),x1693,a1)),f6(f4(x1691,f4(x1692,x1693,a1),a1)))), % 63.73/63.79 inference(scs_inference,[],[49,4,2])). % 63.73/63.79 cnf(173,plain, % 63.73/63.79 (E(f4(f4(x1731,x1732,a1),f4(x1733,x1734,a1),a1),f4(x1732,f4(f4(x1733,x1734,a1),x1731,a1),a1))), % 63.73/63.79 inference(scs_inference,[],[49,169,128,148,55,2,13,3])). % 63.73/63.79 cnf(182,plain, % 63.73/63.79 (E(f4(f4(x1821,f4(x1822,x1823,a1),a1),f4(x1824,x1825,a1),a1),f4(x1822,f4(x1823,f4(f4(x1824,x1825,a1),x1821,a1),a1),a1))), % 63.73/63.79 inference(scs_inference,[],[49,150,173,2,3])). % 63.73/63.79 cnf(191,plain, % 63.73/63.79 (E(f4(f4(f4(f4(x1911,x1912,a1),x1913,a1),x1914,a1),x1915,a1),f4(f4(x1912,f4(x1913,f4(x1914,x1915,a1),a1),a1),x1911,a1))), % 63.73/63.79 inference(scs_inference,[],[48,79,182,2,3])). % 63.73/63.79 cnf(202,plain, % 63.73/63.79 (E(f4(x2021,f4(x2022,f4(x2023,x2024,a1),a1),a1),f4(x2022,f4(f4(x2023,x2024,a1),x2021,a1),a1))), % 63.73/63.79 inference(scs_inference,[],[49,191,173,2,3])). % 63.73/63.79 cnf(215,plain, % 63.73/63.79 (E(f4(f4(f4(x2151,f4(x2152,x2153,a1),a1),x2154,a1),x2155,a1),f4(f4(f4(f4(x2154,x2155,a1),x2151,a1),x2152,a1),x2153,a1))), % 63.73/63.79 inference(scs_inference,[],[48,72,202,2,3])). % 63.73/63.79 cnf(227,plain, % 63.73/63.79 (E(f4(f4(f4(f4(x2271,x2272,a1),x2273,a1),x2274,a1),x2275,a1),f4(x2272,f4(f4(x2273,f4(x2274,x2275,a1),a1),x2271,a1),a1))), % 63.73/63.79 inference(scs_inference,[],[48,215,128,2,3])). % 63.73/63.79 cnf(239,plain, % 63.73/63.79 (E(f4(f4(x2391,x2392,a1),f4(x2393,x2394,a1),a1),f4(f4(x2394,f4(x2391,x2392,a1),a1),x2393,a1))), % 63.73/63.79 inference(scs_inference,[],[56,79,227,2,3])). % 63.73/63.79 cnf(253,plain, % 63.73/63.79 (E(f4(x2531,f4(x2532,f4(x2533,x2534,a1),a1),a1),f4(f4(x2534,f4(x2531,x2532,a1),a1),x2533,a1))), % 63.73/63.79 inference(scs_inference,[],[49,239,2,3])). % 63.73/63.79 cnf(264,plain, % 63.73/63.79 (E(f4(f4(x2641,f4(x2642,x2643,a1),a1),x2644,a1),f4(x2643,f4(f4(x2644,x2641,a1),x2642,a1),a1))), % 63.73/63.79 inference(scs_inference,[],[48,84,253,2,3])). % 63.73/63.79 cnf(275,plain, % 63.73/63.79 (E(f4(f4(x2751,f4(x2752,f4(x2753,x2754,a1),a1),a1),x2755,a1),f4(f4(x2754,f4(f4(x2755,x2751,a1),x2752,a1),a1),x2753,a1))), % 63.73/63.79 inference(scs_inference,[],[56,253,264,2,3])). % 63.73/63.79 cnf(292,plain, % 63.73/63.79 (E(f4(f4(x2921,x2922,a1),x2923,a1),f4(x2922,f4(x2923,x2921,a1),a1))), % 63.73/63.79 inference(scs_inference,[],[61,48,275,2,3])). % 63.73/63.79 cnf(301,plain, % 63.73/63.79 (E(f4(x3011,f4(x3012,x3013,a1),a1),f4(f4(x3013,x3011,a1),x3012,a1))), % 63.73/63.79 inference(scs_inference,[],[292,2])). % 63.73/63.79 cnf(701,plain, % 63.73/63.79 (E(f4(f4(x7011,f4(f4(x7012,x7013,a1),x7014,a1),x7015),x7016,x7017),f4(f4(x7011,f4(x7012,f4(x7013,x7014,a1),a1),x7015),x7016,x7017))), % 63.73/63.79 inference(scs_inference,[],[48,8,9])). % 63.73/63.79 cnf(702,plain, % 63.73/63.79 (E(f4(f4(x7021,f4(x7022,f4(x7023,x7024,a1),a1),x7025),x7026,x7027),f4(f4(x7021,f4(f4(x7022,x7023,a1),x7024,a1),x7025),x7026,x7027))), % 63.73/63.79 inference(scs_inference,[],[701,2])). % 63.73/63.79 cnf(4084,plain, % 63.73/63.79 (E(f4(f4(x40841,f4(x40842,f4(x40843,x40844,a1),a1),a1),x40845,a1),f4(f4(f4(x40845,x40841,a1),f4(x40842,x40843,a1),a1),x40844,a1))), % 63.73/63.79 inference(scs_inference,[],[79,701,3,2])). % 63.73/63.79 cnf(4351,plain, % 63.73/63.79 (E(f4(f4(x43511,f4(f4(x43512,x43513,a1),x43514,a1),a1),x43515,a1),f4(f4(f4(x43515,x43511,a1),x43512,a1),f4(x43513,x43514,a1),a1))), % 63.73/63.79 inference(scs_inference,[],[79,702,3,2])). % 63.73/63.79 cnf(4786,plain, % 63.73/63.79 (E(f4(f4(f4(x47861,x47862,a1),x47863,a1),f4(x47864,x47865,a1),a1),f4(f4(f4(x47861,x47862,a1),f4(x47863,x47864,a1),a1),x47865,a1))), % 63.73/63.79 inference(scs_inference,[],[79,4084,3])). % 63.73/63.79 cnf(4789,plain, % 63.73/63.79 (E(f4(f4(f4(x47891,x47892,a1),f4(x47893,x47894,a1),a1),x47895,a1),f4(f4(f4(x47891,x47892,a1),x47893,a1),f4(x47894,x47895,a1),a1))), % 63.73/63.79 inference(scs_inference,[],[79,4084,3,2])). % 63.73/63.79 cnf(4934,plain, % 63.73/63.79 (P6(a1)), % 63.73/63.79 inference(scs_inference,[],[20,26])). % 63.73/63.79 cnf(4952,plain, % 63.73/63.79 (~P2(f4(f2(f6(a5),a1),f2(f9(a5),a1),a1),f4(f4(f2(f8(a5),a1),a7,a1),f2(f9(a5),a1),a1),a1)), % 63.73/63.79 inference(scs_inference,[],[20,4789,22,292,55,26,4,7,11,5,6,8,10,9,24,23,25,13,14])). % 63.73/63.79 cnf(4970,plain, % 63.73/63.79 (~P2(f4(f2(f6(a5),a1),f2(f9(a5),a1),a1),f4(f4(a7,f2(f9(a5),a1),a1),f2(f8(a5),a1),a1),a1)), % 63.73/63.79 inference(scs_inference,[],[4786,4952,56,55,8,7,5,4,10,6,11,9,13,14])). % 63.73/63.79 cnf(4988,plain, % 63.73/63.79 (~P2(f4(f2(f6(a5),a1),f2(f9(a5),a1),a1),f4(f2(f9(a5),a1),f4(f2(f8(a5),a1),a7,a1),a1),a1)), % 63.73/63.80 inference(scs_inference,[],[4970,4351,301,55,8,5,7,11,10,4,6,9,13,14])). % 63.73/63.80 cnf(5017,plain, % 63.73/63.80 (~P2(f4(f2(f9(a5),a1),f2(f6(a5),a1),a1),f4(f2(f9(a5),a1),f4(f2(f8(a5),a1),a7,a1),a1),a1)), % 63.73/63.80 inference(scs_inference,[],[4988,104,55,8,5,7,6,10,4,11,9,13])). % 63.73/63.80 cnf(5461,plain, % 63.73/63.80 (E(f4(f4(x54611,f4(x54612,x54613,a1),a1),x54614,x54615),f4(f4(f4(x54613,x54611,a1),x54612,a1),x54614,x54615))), % 63.73/63.80 inference(scs_inference,[],[301,8])). % 63.73/63.80 cnf(5478,plain, % 63.73/63.80 ($false), % 63.73/63.80 inference(scs_inference,[],[5461,5017,59,4934,41,8,7,6,10,11,4,9,5,30]), % 63.73/63.80 ['proof']). % 63.73/63.80 % SZS output end Proof % 63.73/63.80 % Total time :63.150000s %------------------------------------------------------------------------------