%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : ANA018-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 : 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 04:13:54 EDT 2024 % Result : Unsatisfiable 116.47s 116.73s % Output : CNFRefutation 116.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.14 % Problem : ANA018-2 : TPTP v8.2.0. Released v3.2.0. % 0.08/0.14 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.14/0.36 % Computer : n020.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 300 % 0.14/0.36 % DateTime : Sun Jun 23 04:14:24 EDT 2024 % 0.14/0.36 % CPUTime : % 0.46/0.60 start to proof:theBenchmark % 116.47/116.71 %------------------------------------------- % 116.47/116.71 % File :CSE---1.7 % 116.47/116.71 % Problem :theBenchmark % 116.47/116.71 % Transform :cnf % 116.47/116.71 % Format :tptp:raw % 116.47/116.71 % Command :java -jar mcs_scs.jar %d %s % 116.47/116.71 % 116.47/116.71 % Result :Theorem 115.830000s % 116.47/116.71 % Output :CNFRefutation 115.830000s % 116.47/116.71 %------------------------------------------- % 116.47/116.72 %------------------------------------------------------------------------------ % 116.47/116.72 % File : ANA018-2 : TPTP v8.2.0. Released v3.2.0. % 116.47/116.72 % Domain : Analysis % 116.47/116.72 % Problem : Problem about Big-O notation % 116.47/116.72 % Version : [Pau06] axioms : Reduced > Especial. % 116.47/116.72 % English : % 116.47/116.72 % 116.47/116.72 % Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe % 116.47/116.72 % Source : [Pau06] % 116.47/116.72 % Names : % 116.47/116.72 % 116.47/116.72 % Status : Unsatisfiable % 116.47/116.72 % Rating : 0.00 v5.3.0, 0.08 v5.2.0, 0.00 v5.0.0, 0.14 v4.1.0, 0.11 v4.0.1, 0.17 v3.3.0, 0.14 v3.2.0 % 116.47/116.72 % Syntax : Number of clauses : 13 ( 5 unt; 0 nHn; 10 RR) % 116.47/116.72 % Number of literals : 26 ( 1 equ; 14 neg) % 116.47/116.72 % Maximal clause size : 4 ( 2 avg) % 116.47/116.72 % Maximal term depth : 4 ( 1 avg) % 116.47/116.72 % Number of predicates : 8 ( 7 usr; 0 prp; 1-3 aty) % 116.47/116.72 % Number of functors : 10 ( 10 usr; 5 con; 0-3 aty) % 116.47/116.72 % Number of variables : 21 ( 0 sgn) % 116.47/116.72 % SPC : CNF_UNS_RFO_SEQ_HRN % 116.47/116.72 % 116.47/116.72 % Comments : The problems in the [Pau06] collection each have very many axioms, % 116.47/116.72 % of which only a small selection are required for the refutation. % 116.47/116.72 % The mission is to find those few axioms, after which a refutation % 116.47/116.72 % can be quite easily found. This version has only the necessary % 116.47/116.72 % axioms. % 116.47/116.72 %------------------------------------------------------------------------------ % 116.47/116.72 cnf(cls_conjecture_1,negated_conjecture, % 116.47/116.72 c_lessequals(c_HOL_Oabs(v_f(V_U),t_b),c_times(v_c,c_HOL_Oabs(v_g(V_U),t_b),t_b),t_b) ). % 116.47/116.72 % 116.47/116.72 cnf(cls_conjecture_2,negated_conjecture, % 116.47/116.72 c_less(c_0,v_ca,t_b) ). % 116.47/116.72 % 116.47/116.72 cnf(cls_conjecture_3,negated_conjecture, % 116.47/116.72 c_lessequals(c_HOL_Oabs(v_x(V_U),t_b),c_times(v_ca,c_HOL_Oabs(v_f(V_U),t_b),t_b),t_b) ). % 116.47/116.72 % 116.47/116.72 cnf(cls_conjecture_4,negated_conjecture, % 116.47/116.73 ~ c_lessequals(c_HOL_Oabs(v_x(v_xa),t_b),c_times(c_times(v_ca,v_c,t_b),c_HOL_Oabs(v_g(v_xa),t_b),t_b),t_b) ). % 116.47/116.73 % 116.47/116.73 cnf(tfree_tcs,negated_conjecture, % 116.47/116.73 class_Ring__and__Field_Oordered__idom(t_b) ). % 116.47/116.73 % 116.47/116.73 cnf(cls_OrderedGroup_Omult__ac__1_0,axiom, % 116.47/116.73 ( ~ class_OrderedGroup_Osemigroup__mult(T_a) % 116.47/116.73 | 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) ) ). % 116.47/116.73 % 116.47/116.73 cnf(cls_Orderings_Oorder__class_Oorder__trans_0,axiom, % 116.47/116.73 ( ~ class_Orderings_Oorder(T_a) % 116.47/116.73 | ~ c_lessequals(V_y,V_z,T_a) % 116.47/116.73 | ~ c_lessequals(V_x,V_y,T_a) % 116.47/116.73 | c_lessequals(V_x,V_z,T_a) ) ). % 116.47/116.73 % 116.47/116.73 cnf(cls_Orderings_Oorder__less__imp__le_0,axiom, % 116.47/116.73 ( ~ class_Orderings_Oorder(T_a) % 116.47/116.73 | ~ c_less(V_x,V_y,T_a) % 116.47/116.73 | c_lessequals(V_x,V_y,T_a) ) ). % 116.47/116.73 % 116.47/116.73 cnf(cls_Ring__and__Field_Opordered__semiring__class_Omult__left__mono_0,axiom, % 116.47/116.73 ( ~ class_Ring__and__Field_Opordered__semiring(T_a) % 116.47/116.73 | ~ c_lessequals(V_a,V_b,T_a) % 116.47/116.73 | ~ c_lessequals(c_0,V_c,T_a) % 116.47/116.73 | c_lessequals(c_times(V_c,V_a,T_a),c_times(V_c,V_b,T_a),T_a) ) ). % 116.47/116.73 % 116.47/116.73 cnf(clsrel_LOrder_Ojoin__semilorder_1,axiom, % 116.47/116.73 ( ~ class_LOrder_Ojoin__semilorder(T) % 116.47/116.73 | class_Orderings_Oorder(T) ) ). % 116.47/116.73 % 116.47/116.73 cnf(clsrel_Ring__and__Field_Oordered__idom_21,axiom, % 116.47/116.73 ( ~ class_Ring__and__Field_Oordered__idom(T) % 116.47/116.73 | class_OrderedGroup_Osemigroup__mult(T) ) ). % 116.47/116.73 % 116.47/116.73 cnf(clsrel_Ring__and__Field_Oordered__idom_35,axiom, % 116.47/116.73 ( ~ class_Ring__and__Field_Oordered__idom(T) % 116.47/116.73 | class_LOrder_Ojoin__semilorder(T) ) ). % 116.47/116.73 % 116.47/116.73 cnf(clsrel_Ring__and__Field_Oordered__idom_42,axiom, % 116.47/116.73 ( ~ class_Ring__and__Field_Oordered__idom(T) % 116.47/116.73 | class_Ring__and__Field_Opordered__semiring(T) ) ). % 116.47/116.73 % 116.47/116.73 %------------------------------------------------------------------------------ % 116.47/116.73 %------------------------------------------- % 116.47/116.73 % Proof found % 116.47/116.73 % SZS status Theorem for theBenchmark % 116.47/116.73 % SZS output start Proof % 116.47/116.73 %ClaNum:35(EqnAxiom:22) % 116.47/116.73 %VarNum:53(SingletonVarNum:21) % 116.47/116.73 %MaxLitNum:4 % 116.47/116.73 %MaxfuncDepth:3 % 116.47/116.73 %SharedTerms:14 % 116.47/116.73 %goalClause: 23 24 25 26 27 % 116.47/116.73 %singleGoalClaCount:5 % 116.47/116.73 [23]P1(a1) % 116.47/116.73 [24]P2(a2,a5,a1) % 116.47/116.73 [27]~P3(f3(f9(a10),a1),f4(f4(a5,a6,a1),f3(f8(a10),a1),a1),a1) % 116.47/116.73 [25]P3(f3(f7(x251),a1),f4(a6,f3(f8(x251),a1),a1),a1) % 116.47/116.73 [26]P3(f3(f9(x261),a1),f4(a5,f3(f7(x261),a1),a1),a1) % 116.47/116.73 [28]~P1(x281)+P4(x281) % 116.47/116.73 [29]~P5(x291)+P6(x291) % 116.47/116.73 [30]~P1(x301)+P7(x301) % 116.47/116.73 [31]~P1(x311)+P5(x311) % 116.47/116.73 [34]~P4(x343)+E(f4(f4(x341,x342,x343),x344,x343),f4(x341,f4(x342,x344,x343),x343)) % 116.47/116.73 [32]~P6(x323)+~P2(x321,x322,x323)+P3(x321,x322,x323) % 116.47/116.73 [33]~P6(x333)+~P3(x334,x332,x333)+P3(x331,x332,x333)+~P3(x331,x334,x333) % 116.47/116.73 [35]~P7(x353)+~P3(x352,x354,x353)+~P3(a2,x351,x353)+P3(f4(x351,x352,x353),f4(x351,x354,x353),x353) % 116.47/116.73 %EqnAxiom % 116.47/116.73 [1]E(x11,x11) % 116.47/116.73 [2]E(x22,x21)+~E(x21,x22) % 116.47/116.73 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 116.47/116.73 [4]~E(x41,x42)+E(f7(x41),f7(x42)) % 116.47/116.73 [5]~E(x51,x52)+E(f3(x51,x53),f3(x52,x53)) % 116.47/116.73 [6]~E(x61,x62)+E(f3(x63,x61),f3(x63,x62)) % 116.47/116.73 [7]~E(x71,x72)+E(f8(x71),f8(x72)) % 116.47/116.73 [8]~E(x81,x82)+E(f4(x81,x83,x84),f4(x82,x83,x84)) % 116.47/116.73 [9]~E(x91,x92)+E(f4(x93,x91,x94),f4(x93,x92,x94)) % 116.47/116.73 [10]~E(x101,x102)+E(f4(x103,x104,x101),f4(x103,x104,x102)) % 116.47/116.73 [11]~E(x111,x112)+E(f9(x111),f9(x112)) % 116.47/116.73 [12]~P1(x121)+P1(x122)+~E(x121,x122) % 116.47/116.73 [13]P2(x132,x133,x134)+~E(x131,x132)+~P2(x131,x133,x134) % 116.47/116.73 [14]P2(x143,x142,x144)+~E(x141,x142)+~P2(x143,x141,x144) % 116.47/116.74 [15]P2(x153,x154,x152)+~E(x151,x152)+~P2(x153,x154,x151) % 116.47/116.74 [16]P3(x162,x163,x164)+~E(x161,x162)+~P3(x161,x163,x164) % 116.47/116.74 [17]P3(x173,x172,x174)+~E(x171,x172)+~P3(x173,x171,x174) % 116.47/116.74 [18]P3(x183,x184,x182)+~E(x181,x182)+~P3(x183,x184,x181) % 116.47/116.74 [19]~P4(x191)+P4(x192)+~E(x191,x192) % 116.47/116.74 [20]~P6(x201)+P6(x202)+~E(x201,x202) % 116.47/116.74 [21]~P5(x211)+P5(x212)+~E(x211,x212) % 116.47/116.74 [22]~P7(x221)+P7(x222)+~E(x221,x222) % 116.47/116.74 % 116.47/116.74 %------------------------------------------- % 116.47/116.75 cnf(43,plain, % 116.47/116.75 (P2(a2,a5,x431)+~E(a1,x431)), % 116.47/116.75 inference(scs_inference,[],[26,24,18,15])). % 116.47/116.75 cnf(74,plain, % 116.47/116.75 (E(f4(f4(x741,x742,a1),x743,a1),f4(x741,f4(x742,x743,a1),a1))), % 116.47/116.75 inference(scs_inference,[],[23,28,34])). % 116.47/116.75 cnf(75,plain, % 116.47/116.75 (E(f4(x751,f4(x752,x753,a1),a1),f4(f4(x751,x752,a1),x753,a1))), % 116.47/116.75 inference(scs_inference,[],[74,2])). % 116.47/116.75 cnf(718,plain, % 116.47/116.75 (E(f4(f4(f4(x7181,x7182,a1),x7183,a1),x7184,a1),f4(x7181,f4(x7182,f4(x7183,x7184,a1),a1),a1))+~P4(a1)), % 116.47/116.75 inference(scs_inference,[],[74,3,34])). % 116.47/116.75 cnf(874,plain, % 116.47/116.75 (~E(a1,x8741)+P4(x8741)), % 116.47/116.75 inference(scs_inference,[],[23,28,19])). % 116.47/116.75 cnf(875,plain, % 116.47/116.75 (P4(a1)), % 116.47/116.75 inference(equality_inference,[],[874])). % 116.47/116.75 cnf(876,plain, % 116.47/116.75 (E(f4(f4(f4(x8761,x8762,a1),x8763,a1),x8764,a1),f4(x8761,f4(x8762,f4(x8763,x8764,a1),a1),a1))), % 116.47/116.75 inference(scs_inference,[],[875,718])). % 116.47/116.75 cnf(969,plain, % 116.47/116.75 (P6(a1)), % 116.47/116.75 inference(scs_inference,[],[23,29,31])). % 116.47/116.75 cnf(990,plain, % 116.47/116.75 (~E(a1,x9901)+P7(x9901)), % 116.47/116.75 inference(scs_inference,[],[23,30,22])). % 116.47/116.75 cnf(991,plain, % 116.47/116.75 (P7(a1)), % 116.47/116.75 inference(equality_inference,[],[990])). % 116.47/116.75 cnf(1069,plain, % 116.47/116.75 (E(f3(f4(x10691,f4(x10692,x10693,a1),a1),x10694),f3(f4(f4(x10691,x10692,a1),x10693,a1),x10694))), % 116.47/116.75 inference(scs_inference,[],[74,2,5])). % 116.47/116.75 cnf(1070,plain, % 116.47/116.75 (E(f3(x10701,f4(x10702,f4(x10703,x10704,a1),a1)),f3(x10701,f4(f4(x10702,x10703,a1),x10704,a1)))), % 116.47/116.75 inference(scs_inference,[],[74,2,6])). % 116.47/116.75 cnf(1072,plain, % 116.47/116.75 (E(f4(f4(x10721,f4(x10722,x10723,a1),a1),x10724,x10725),f4(f4(f4(x10721,x10722,a1),x10723,a1),x10724,x10725))), % 116.47/116.75 inference(scs_inference,[],[74,2,8])). % 116.47/116.75 cnf(1078,plain, % 116.47/116.75 (P3(a2,a5,a1)), % 116.47/116.75 inference(scs_inference,[],[969,43,32])). % 116.47/116.75 cnf(1079,plain, % 116.47/116.75 (P3(x10791,a5,a1)+~E(a2,x10791)), % 116.47/116.75 inference(scs_inference,[],[1078,16])). % 116.47/116.75 cnf(1088,plain, % 116.47/116.75 (P3(a2,x10881,a1)+~E(a5,x10881)), % 116.47/116.75 inference(scs_inference,[],[1078,17])). % 116.47/116.75 cnf(1162,plain, % 116.47/116.75 (P3(f4(a5,a2,a1),f4(a5,a5,a1),a1)), % 116.47/116.75 inference(scs_inference,[],[991,1079,35])). % 116.47/116.75 cnf(1240,plain, % 116.47/116.75 (~E(x12401,a5)+P3(a2,x12401,a1)), % 116.47/116.75 inference(scs_inference,[],[1088,2])). % 116.47/116.75 cnf(1250,plain, % 116.47/116.75 (P3(f4(x12501,f3(f7(x12502),a1),a1),f4(x12501,f4(a6,f3(f8(x12502),a1),a1),a1),a1)+~E(a5,x12501)), % 116.47/116.75 inference(scs_inference,[],[25,991,1088,35])). % 116.47/116.75 cnf(1251,plain, % 116.47/116.75 (P3(f4(a5,f3(f7(x12511),a1),a1),f4(a5,f4(a6,f3(f8(x12511),a1),a1),a1),a1)), % 116.47/116.75 inference(equality_inference,[],[1250])). % 116.47/116.75 cnf(1294,plain, % 116.47/116.75 (P3(f4(x12941,f4(a5,a2,a1),a1),f4(x12941,f4(a5,a5,a1),a1),a1)+~E(x12941,a5)), % 116.47/116.75 inference(scs_inference,[],[1162,991,1240,35])). % 116.47/116.75 cnf(1295,plain, % 116.47/116.75 (P3(f4(a5,f4(a5,a2,a1),a1),f4(a5,f4(a5,a5,a1),a1),a1)), % 116.47/116.75 inference(equality_inference,[],[1294])). % 116.47/116.75 cnf(1297,plain, % 116.47/116.75 (E(f4(x12971,f4(x12972,x12973,a1),a1),f4(f4(x12971,x12972,a1),x12973,a1))), % 116.47/116.75 inference(rename_variables,[],[75])). % 116.47/116.75 cnf(1298,plain, % 116.47/116.75 (P3(f4(a5,f4(a5,a2,a1),a1),f4(f4(a5,a5,a1),a5,a1),a1)), % 116.47/116.75 inference(scs_inference,[],[75,1297,1295,16,17])). % 116.47/116.75 cnf(1419,plain, % 116.47/116.75 (E(f9(f7(f4(f4(x14191,x14192,a1),x14193,a1))),f9(f7(f4(x14191,f4(x14192,x14193,a1),a1))))), % 116.47/116.75 inference(scs_inference,[],[74,4,11])). % 116.47/116.75 cnf(1426,plain, % 116.47/116.75 (E(f7(f4(x14261,f4(x14262,f4(x14263,x14264,a1),a1),x14265)),f7(f4(x14261,f4(f4(x14262,x14263,a1),x14264,a1),x14265)))), % 116.47/116.75 inference(scs_inference,[],[75,4,9])). % 116.47/116.75 cnf(1427,plain, % 116.47/116.75 (~E(f7(f4(x14271,f4(x14272,x14273,a1),a1)),x14274)+E(f7(f4(f4(x14271,x14272,a1),x14273,a1)),x14274)), % 116.47/116.75 inference(scs_inference,[],[74,4,3])). % 116.47/116.75 cnf(1501,plain, % 116.47/116.75 (E(f8(f4(x15011,f4(f4(x15012,x15013,a1),x15014,a1),x15015)),f8(f4(x15011,f4(x15012,f4(x15013,x15014,a1),a1),x15015)))), % 116.47/116.75 inference(scs_inference,[],[74,7,9])). % 116.47/116.75 cnf(1510,plain, % 116.47/116.75 (~E(f8(f4(x15101,f4(x15102,x15103,a1),a1)),x15104)+E(f8(f4(f4(x15101,x15102,a1),x15103,a1)),x15104)), % 116.47/116.75 inference(scs_inference,[],[74,7,3])). % 116.47/116.75 cnf(1583,plain, % 116.47/116.75 (E(f9(f4(f4(f4(x15831,x15832,a1),x15833,a1),x15834,x15835)),f9(f4(f4(x15831,f4(x15832,x15833,a1),a1),x15834,x15835)))), % 116.47/116.75 inference(scs_inference,[],[74,11,8])). % 116.47/116.75 cnf(1590,plain, % 116.47/116.75 (~E(f9(f4(x15901,f4(x15902,x15903,a1),a1)),x15904)+E(f9(f4(f4(x15901,x15902,a1),x15903,a1)),x15904)), % 116.47/116.75 inference(scs_inference,[],[74,11,3])). % 116.47/116.75 cnf(1747,plain, % 116.47/116.75 (~E(f3(f4(x17471,f4(x17472,x17473,a1),a1),x17474),x17475)+E(f3(f4(f4(x17471,x17472,a1),x17473,a1),x17474),x17475)), % 116.47/116.75 inference(scs_inference,[],[74,5,3])). % 116.47/116.75 cnf(1829,plain, % 116.47/116.75 (E(f3(f4(f4(x18291,x18292,a1),x18293,a1),f4(f4(x18294,x18295,a1),x18296,a1)),f3(f4(x18291,f4(x18292,x18293,a1),a1),f4(x18294,f4(x18295,x18296,a1),a1)))), % 116.47/116.75 inference(scs_inference,[],[74,6,1747])). % 116.47/116.75 cnf(1835,plain, % 116.47/116.75 (~E(f3(x18351,f4(x18352,f4(x18353,x18354,a1),a1)),x18355)+E(f3(x18351,f4(f4(x18352,x18353,a1),x18354,a1)),x18355)), % 116.47/116.75 inference(scs_inference,[],[74,6,3])). % 116.47/116.75 cnf(1935,plain, % 116.47/116.75 (E(f4(f4(f4(x19351,x19352,a1),x19353,a1),x19354,x19355),f4(f4(x19351,f4(x19352,x19353,a1),a1),x19354,x19355))), % 116.47/116.75 inference(scs_inference,[],[875,8,34])). % 116.47/116.75 cnf(1936,plain, % 116.47/116.75 (E(f4(f4(f4(x19361,x19362,a1),x19363,a1),f4(x19364,x19365,a1),a1),f4(f4(f4(x19361,f4(x19362,x19363,a1),a1),x19364,a1),x19365,a1))), % 116.47/116.75 inference(scs_inference,[],[74,75,8,3])). % 116.47/116.75 cnf(1938,plain, % 116.47/116.75 (E(f4(f4(x19381,x19382,a1),f4(x19383,x19384,a1),a1),f4(f4(x19381,f4(x19382,x19383,a1),a1),x19384,a1))), % 116.47/116.75 inference(scs_inference,[],[74,75,8,3])). % 116.47/116.75 cnf(1939,plain, % 116.47/116.75 (E(f4(f4(x19391,f4(x19392,x19393,a1),a1),x19394,a1),f4(f4(x19391,x19392,a1),f4(x19393,x19394,a1),a1))), % 116.47/116.75 inference(scs_inference,[],[1938,2])). % 116.47/116.75 cnf(2074,plain, % 116.47/116.75 (E(f4(f4(x20741,x20742,a1),f4(x20743,x20744,a1),a1),f4(x20741,f4(f4(x20742,x20743,a1),x20744,a1),a1))), % 116.47/116.75 inference(scs_inference,[],[1938,74,3])). % 116.47/116.75 cnf(2076,plain, % 116.47/116.75 (E(f4(x20761,f4(f4(x20762,x20763,a1),x20764,a1),a1),f4(f4(x20761,x20762,a1),f4(x20763,x20764,a1),a1))), % 116.47/116.75 inference(scs_inference,[],[1938,74,3,2])). % 116.47/116.75 cnf(2286,plain, % 116.47/116.75 (~P2(f4(f4(f4(x22861,x22862,a1),x22863,a1),x22864,x22865),x22866,x22867)+P2(f4(f4(x22861,f4(x22862,x22863,a1),a1),x22864,x22865),x22866,x22867)), % 116.47/116.75 inference(scs_inference,[],[74,8,13])). % 116.47/116.75 cnf(2301,plain, % 116.47/116.75 (E(f4(f4(x23011,f4(f4(x23012,x23013,a1),x23014,a1),a1),x23015,x23016),f4(f4(f4(x23011,x23012,a1),f4(x23013,x23014,a1),a1),x23015,x23016))), % 116.47/116.75 inference(scs_inference,[],[2074,8,2])). % 116.47/116.75 cnf(2303,plain, % 116.47/116.75 (~P3(f4(f4(f4(x23031,x23032,a1),x23033,a1),x23034,x23035),x23036,x23037)+P3(f4(f4(x23031,f4(x23032,x23033,a1),a1),x23034,x23035),x23036,x23037)), % 116.47/116.75 inference(scs_inference,[],[74,8,16])). % 116.47/116.75 cnf(2304,plain, % 116.47/116.75 (P3(f4(f4(x23041,f4(x23042,x23043,a1),a1),x23044,x23045),f4(x23046,f4(x23047,x23048,a1),a1),x23049)+~P3(f4(f4(f4(x23041,x23042,a1),x23043,a1),x23044,x23045),f4(f4(x23046,x23047,a1),x23048,a1),x23049)), % 116.47/116.75 inference(scs_inference,[],[74,2303,17])). % 116.47/116.75 cnf(2311,plain, % 116.47/116.75 (~P3(x23111,f4(f4(f4(x23112,x23113,a1),x23114,a1),x23115,x23116),x23117)+P3(x23111,f4(f4(x23112,f4(x23113,x23114,a1),a1),x23115,x23116),x23117)), % 116.47/116.75 inference(scs_inference,[],[74,8,17])). % 116.47/116.75 cnf(2401,plain, % 116.47/116.75 (E(f4(x24011,f4(f4(x24012,x24013,a1),x24014,a1),x24015),f4(x24011,f4(x24012,f4(x24013,x24014,a1),a1),x24015))), % 116.47/116.75 inference(scs_inference,[],[875,9,34])). % 116.47/116.75 cnf(2412,plain, % 116.47/116.75 (~P2(f4(x24121,f4(f4(x24122,x24123,a1),x24124,a1),x24125),x24126,x24127)+P2(f4(x24121,f4(x24122,f4(x24123,x24124,a1),a1),x24125),x24126,x24127)), % 116.47/116.75 inference(scs_inference,[],[74,9,13])). % 116.47/116.75 cnf(2437,plain, % 116.47/116.75 (~P3(f4(x24371,f4(f4(x24372,x24373,a1),x24374,a1),x24375),x24376,x24377)+P3(f4(x24371,f4(x24372,f4(x24373,x24374,a1),a1),x24375),x24376,x24377)), % 116.47/116.75 inference(scs_inference,[],[74,9,16])). % 116.47/116.75 cnf(2444,plain, % 116.47/116.75 (~P3(x24441,f4(x24442,f4(f4(x24443,x24444,a1),x24445,a1),x24446),x24447)+P3(x24441,f4(x24442,f4(x24443,f4(x24444,x24445,a1),a1),x24446),x24447)), % 116.47/116.75 inference(scs_inference,[],[74,9,17])). % 116.47/116.75 cnf(2574,plain, % 116.47/116.75 (~E(f4(x25741,x25742,f4(x25743,f4(x25744,x25745,a1),a1)),x25746)+E(f4(x25741,x25742,f4(f4(x25743,x25744,a1),x25745,a1)),x25746)), % 116.47/116.75 inference(scs_inference,[],[74,10,3])). % 116.47/116.75 cnf(3305,plain, % 116.47/116.75 (~P3(x33051,f4(f4(x33052,f4(x33053,x33054,a1),a1),x33055,a1),x33056)+P3(x33051,f4(f4(x33052,x33053,a1),f4(x33054,x33055,a1),a1),x33056)), % 116.47/116.75 inference(scs_inference,[],[1939,17])). % 116.47/116.75 cnf(3310,plain, % 116.47/116.75 (~P3(x33101,f4(f4(x33102,x33103,a1),f4(x33104,x33105,a1),a1),x33106)+P3(x33101,f4(f4(x33102,f4(x33103,x33104,a1),a1),x33105,a1),x33106)), % 116.47/116.75 inference(scs_inference,[],[1938,17])). % 116.47/116.75 cnf(3314,plain, % 116.47/116.75 (~P3(x33141,f4(x33142,f4(f4(x33143,x33144,a1),x33145,a1),a1),x33146)+P3(x33141,f4(f4(x33142,x33143,a1),f4(x33144,x33145,a1),a1),x33146)), % 116.47/116.75 inference(scs_inference,[],[2076,17])). % 116.47/116.75 cnf(3320,plain, % 116.47/116.75 (~P3(x33201,f4(f4(x33202,x33203,a1),f4(x33204,x33205,a1),a1),x33206)+P3(x33201,f4(x33202,f4(f4(x33203,x33204,a1),x33205,a1),a1),x33206)), % 116.47/116.75 inference(scs_inference,[],[2074,17])). % 116.47/116.75 cnf(3324,plain, % 116.47/116.75 (P3(f4(a5,f4(a5,f4(a5,a2,a1),a1),a1),f4(f4(a5,a5,a1),f4(a5,a5,a1),a1),a1)), % 116.47/116.75 inference(scs_inference,[],[1078,1298,991,3314,35])). % 116.47/116.75 cnf(3325,plain, % 116.47/116.75 (P3(f4(f4(a5,a5,a1),f4(a5,a2,a1),a1),f4(f4(a5,a5,a1),f4(a5,a5,a1),a1),a1)), % 116.47/116.75 inference(scs_inference,[],[75,3324,16])). % 116.47/116.75 cnf(3328,plain, % 116.47/116.75 (P3(f4(f4(a5,a5,a1),f4(a5,a2,a1),a1),f4(f4(a5,f4(a5,a5,a1),a1),a5,a1),a1)), % 116.47/116.75 inference(scs_inference,[],[75,3324,16,3320,3310])). % 116.47/116.75 cnf(3361,plain, % 116.47/116.75 (P3(f4(f4(f4(a5,a5,a1),a5,a1),a2,a1),f4(f4(a5,a5,a1),f4(a5,a5,a1),a1),a1)), % 116.47/116.75 inference(scs_inference,[],[75,3325,16])). % 116.47/116.75 cnf(3404,plain, % 116.47/116.75 (P3(f4(f4(a5,a5,a1),f4(a5,a2,a1),a1),f4(a5,f4(a5,f4(a5,a5,a1),a1),a1),a1)), % 116.47/116.75 inference(scs_inference,[],[3325,74,17])). % 116.47/116.75 cnf(3691,plain, % 116.47/116.75 (~P3(f4(a5,f3(f7(a10),a1),a1),f4(f4(a5,a6,a1),f3(f8(a10),a1),a1),a1)), % 116.47/116.75 inference(scs_inference,[],[26,27,74,3324,3328,3361,3404,1072,969,2304,3320,3310,16,17,33])). % 116.47/116.75 cnf(3700,plain, % 116.47/116.75 (P3(f4(f4(f4(a5,a5,a1),a5,a1),a2,a1),f4(a5,f4(f4(a5,a5,a1),a5,a1),a1),a1)), % 116.47/116.75 inference(scs_inference,[],[3361,3320])). % 116.47/116.75 cnf(3778,plain, % 116.47/116.75 (E(f3(f4(f4(x37781,x37782,a1),x37783,a1),f4(x37784,f4(x37785,x37786,a1),a1)),f3(f4(x37781,f4(x37782,x37783,a1),a1),f4(f4(x37784,x37785,a1),x37786,a1)))), % 116.47/116.75 inference(scs_inference,[],[1070,1747])). % 116.47/116.75 cnf(3780,plain, % 116.47/116.75 (E(f3(f4(x37801,f4(x37802,x37803,a1),a1),f4(f4(x37804,x37805,a1),x37806,a1)),f3(f4(f4(x37801,x37802,a1),x37803,a1),f4(x37804,f4(x37805,x37806,a1),a1)))), % 116.47/116.75 inference(scs_inference,[],[1069,1070,1747,1835])). % 116.47/116.75 cnf(3782,plain, % 116.47/116.75 (E(f4(f4(f4(x37821,x37822,a1),x37823,a1),x37824,f4(f4(x37825,x37826,a1),x37827,a1)),f4(f4(x37821,f4(x37822,x37823,a1),a1),x37824,f4(x37825,f4(x37826,x37827,a1),a1)))), % 116.47/116.75 inference(scs_inference,[],[1935,1069,1070,1747,1835,2574])). % 116.47/116.75 cnf(3783,plain, % 116.47/116.75 (E(f4(f4(f4(x37831,x37832,a1),x37833,a1),x37834,x37835),f4(f4(x37831,f4(x37832,x37833,a1),a1),x37834,x37835))), % 116.47/116.75 inference(rename_variables,[],[1935])). % 116.47/116.75 cnf(3786,plain, % 116.47/116.75 (E(f4(f4(f4(x37861,x37862,a1),x37863,a1),f4(x37864,x37865,a1),a1),f4(f4(x37861,f4(f4(x37862,x37863,a1),x37864,a1),a1),x37865,a1))), % 116.47/116.75 inference(scs_inference,[],[1829,1936,3700,1935,3783,1069,1070,1747,1835,2574,2444,2,3])). % 116.47/116.76 cnf(3799,plain, % 116.47/116.76 (E(f4(f4(x37991,f4(x37992,x37993,a1),a1),x37994,a1),f4(x37991,f4(x37992,f4(x37993,x37994,a1),a1),a1))), % 116.47/116.76 inference(scs_inference,[],[2401,876,74,2,3])). % 116.47/116.76 cnf(3809,plain, % 116.47/116.76 (E(f4(x38091,f4(x38092,f4(x38093,x38094,a1),a1),a1),f4(f4(x38091,f4(x38092,x38093,a1),a1),x38094,a1))), % 116.47/116.76 inference(scs_inference,[],[3799,2])). % 116.47/116.76 cnf(3871,plain, % 116.47/116.76 (E(f4(f4(f4(x38711,x38712,a1),f4(x38713,x38714,a1),a1),x38715,a1),f4(x38711,f4(f4(x38712,x38713,a1),f4(x38714,x38715,a1),a1),a1))), % 116.47/116.76 inference(scs_inference,[],[3799,2074,3])). % 116.47/116.76 cnf(3879,plain, % 116.47/116.76 (E(f4(x38791,f4(f4(x38792,x38793,a1),f4(x38794,x38795,a1),a1),a1),f4(f4(f4(x38791,x38792,a1),f4(x38793,x38794,a1),a1),x38795,a1))), % 116.47/116.76 inference(scs_inference,[],[3871,2])). % 116.47/116.76 cnf(3880,plain, % 116.47/116.76 (E(f4(f4(f4(x38801,x38802,a1),x38803,a1),f4(x38804,x38805,a1),a1),f4(x38801,f4(f4(x38802,x38803,a1),f4(x38804,x38805,a1),a1),a1))), % 116.47/116.76 inference(scs_inference,[],[3871,1938,2,3])). % 116.47/116.76 cnf(3887,plain, % 116.47/116.76 (E(f4(f4(x38871,x38872,a1),f4(f4(x38873,x38874,a1),x38875,a1),a1),f4(x38871,f4(f4(x38872,x38873,a1),f4(x38874,x38875,a1),a1),a1))), % 116.47/116.76 inference(scs_inference,[],[3880,2076,2,3])). % 116.47/116.76 cnf(3893,plain, % 116.47/116.76 (E(f4(x38931,f4(f4(x38932,x38933,a1),f4(x38934,x38935,a1),a1),a1),f4(f4(x38931,x38932,a1),f4(f4(x38933,x38934,a1),x38935,a1),a1))), % 116.47/116.76 inference(scs_inference,[],[3887,2])). % 116.47/116.76 cnf(3903,plain, % 116.47/116.76 (~P3(f4(a5,f3(f7(a10),a1),a1),x39031,a1)+~P3(x39031,f4(f4(a5,a6,a1),f3(f8(a10),a1),a1),a1)), % 116.47/116.76 inference(scs_inference,[],[3691,969,33])). % 116.47/116.76 cnf(3927,plain, % 116.47/116.76 (E(f4(f4(x39271,f4(x39272,x39273,a1),a1),f4(x39274,x39275,a1),a1),f4(f4(f4(x39271,x39272,a1),f4(x39273,x39274,a1),a1),x39275,a1))), % 116.47/116.76 inference(scs_inference,[],[3879,74,3])). % 116.47/116.76 cnf(3929,plain, % 116.47/116.76 (E(f4(f4(f4(x39291,x39292,a1),f4(x39293,x39294,a1),a1),x39295,a1),f4(f4(x39291,f4(x39292,x39293,a1),a1),f4(x39294,x39295,a1),a1))), % 116.47/116.76 inference(scs_inference,[],[3879,74,3,2])). % 116.47/116.76 cnf(3996,plain, % 116.47/116.76 (E(f4(f4(x39961,f4(x39962,x39963,a1),a1),f4(x39964,x39965,a1),a1),f4(f4(x39961,x39962,a1),f4(f4(x39963,x39964,a1),x39965,a1),a1))), % 116.47/116.76 inference(scs_inference,[],[3893,74,3])). % 116.47/116.76 cnf(3998,plain, % 116.47/116.76 (E(f4(f4(x39981,x39982,a1),f4(f4(x39983,x39984,a1),x39985,a1),a1),f4(f4(x39981,f4(x39982,x39983,a1),a1),f4(x39984,x39985,a1),a1))), % 116.47/116.76 inference(scs_inference,[],[3893,74,3,2])). % 116.47/116.76 cnf(3999,plain, % 116.47/116.76 (~P3(f4(f4(x39991,x39992,a1),f4(f4(x39993,x39994,a1),x39995,a1),a1),x39996,x39997)+P3(f4(f4(x39991,f4(x39992,x39993,a1),a1),f4(x39994,x39995,a1),a1),x39996,x39997)), % 116.47/116.76 inference(scs_inference,[],[3998,16])). % 116.47/116.76 cnf(4089,plain, % 116.47/116.76 (E(f4(f4(f4(x40891,x40892,a1),x40893,a1),x40894,a1),f4(x40891,f4(f4(x40892,x40893,a1),x40894,a1),a1))), % 116.47/116.76 inference(scs_inference,[],[1935,74,3])). % 116.47/116.76 cnf(4092,plain, % 116.47/116.76 (E(f4(x40921,f4(f4(x40922,x40923,a1),x40924,a1),a1),f4(f4(f4(x40921,x40922,a1),x40923,a1),x40924,a1))), % 116.47/116.76 inference(scs_inference,[],[1935,74,3,2])). % 116.47/116.76 cnf(4093,plain, % 116.47/116.76 (~P2(f4(f4(x40931,x40932,a1),f4(f4(x40933,x40934,a1),x40935,a1),a1),x40936,x40937)+P2(f4(f4(x40931,f4(x40932,x40933,a1),a1),f4(x40934,x40935,a1),a1),x40936,x40937)), % 116.47/116.76 inference(scs_inference,[],[1935,3998,74,3,2,13])). % 116.47/116.76 cnf(4165,plain, % 116.47/116.76 (~P3(f4(f4(f4(x41651,x41652,a1),f4(x41653,x41654,a1),a1),x41655,a1),x41656,x41657)+P3(f4(x41651,f4(f4(x41652,x41653,a1),f4(x41654,x41655,a1),a1),a1),x41656,x41657)), % 116.47/116.76 inference(scs_inference,[],[3871,16])). % 116.47/116.76 cnf(4195,plain, % 116.47/116.76 (~P3(f4(f4(x41951,f4(x41952,x41953,a1),a1),f4(x41954,x41955,a1),a1),x41956,x41957)+P3(f4(f4(x41951,x41952,a1),f4(f4(x41953,x41954,a1),x41955,a1),a1),x41956,x41957)), % 116.47/116.76 inference(scs_inference,[],[4089,3996,15,16])). % 116.47/116.76 cnf(4227,plain, % 116.47/116.76 (P3(f4(a5,f4(f4(a5,a5,a1),f4(a5,a2,a1),a1),a1),f4(a5,f4(f4(a5,a5,a1),f4(a5,a5,a1),a1),a1),a1)), % 116.47/116.76 inference(scs_inference,[],[3871,3325,1078,991,14,35])). % 116.47/116.76 cnf(4229,plain, % 116.47/116.76 (P3(f4(a5,f4(f4(a5,a5,a1),f4(a5,a2,a1),a1),a1),f4(f4(a5,a5,a1),f4(a5,f4(a5,a5,a1),a1),a1),a1)), % 116.47/116.76 inference(scs_inference,[],[4227,3314])). % 116.47/116.76 cnf(4230,plain, % 116.47/116.76 (P3(f4(a5,f4(f4(a5,a5,a1),f4(a5,a2,a1),a1),a1),f4(f4(a5,a5,a1),f4(f4(a5,a5,a1),a5,a1),a1),a1)), % 116.47/116.76 inference(scs_inference,[],[4227,3893,3314,17])). % 116.47/116.76 cnf(4231,plain, % 116.47/116.76 (E(f4(x42311,f4(f4(x42312,x42313,a1),f4(x42314,x42315,a1),a1),a1),f4(f4(x42311,x42312,a1),f4(f4(x42313,x42314,a1),x42315,a1),a1))), % 116.47/116.76 inference(rename_variables,[],[3893])). % 116.47/116.76 cnf(4232,plain, % 116.47/116.76 (~P2(f4(x42321,f4(f4(x42322,x42323,a1),f4(x42324,x42325,a1),a1),a1),x42326,x42327)+P2(f4(f4(x42321,x42322,a1),f4(f4(x42323,x42324,a1),x42325,a1),a1),x42326,x42327)), % 116.47/116.76 inference(scs_inference,[],[4227,3893,4231,3314,17,13])). % 116.47/116.76 cnf(4239,plain, % 116.47/116.76 (P3(f4(a5,f4(f4(a5,a5,a1),f4(a5,a2,a1),a1),a1),f4(f4(f4(a5,a5,a1),a5,a1),f4(a5,a5,a1),a1),a1)), % 116.47/116.76 inference(scs_inference,[],[4230,3314])). % 116.47/116.76 cnf(4240,plain, % 116.47/116.76 (P3(f4(a5,f4(f4(a5,a5,a1),f4(a5,a2,a1),a1),a1),f4(f4(a5,f4(a5,a5,a1),a1),f4(a5,a5,a1),a1),a1)), % 116.47/116.76 inference(scs_inference,[],[4230,3314,2311])). % 116.47/116.76 cnf(4243,plain, % 116.47/116.76 (P3(f4(f4(a5,f4(a5,a5,a1),a1),f4(a5,a2,a1),a1),f4(f4(a5,a5,a1),f4(a5,f4(a5,a5,a1),a1),a1),a1)), % 116.47/116.76 inference(scs_inference,[],[4229,4230,4092,3314,2311,16,2303])). % 116.47/116.76 cnf(4252,plain, % 116.47/116.76 (P3(f4(f4(a5,a5,a1),f4(a5,f4(a5,a2,a1),a1),a1),f4(f4(a5,a5,a1),f4(a5,f4(a5,a5,a1),a1),a1),a1)), % 116.47/116.76 inference(scs_inference,[],[4243,4195,2437])). % 116.47/116.76 cnf(4277,plain, % 116.47/116.76 (P3(f4(f4(a5,a5,a1),f4(a5,f4(a5,a2,a1),a1),a1),f4(f4(f4(a5,a5,a1),f4(a5,a5,a1),a1),a5,a1),a1)), % 116.47/116.76 inference(scs_inference,[],[4252,3809,17])). % 116.47/116.76 cnf(4294,plain, % 116.47/116.76 (~P3(f4(f4(f4(x42941,x42942,a1),f4(x42943,x42944,a1),a1),x42945,a1),x42946,x42947)+P3(f4(f4(x42941,f4(x42942,x42943,a1),a1),f4(x42944,x42945,a1),a1),x42946,x42947)), % 116.47/116.76 inference(scs_inference,[],[3929,16])). % 116.47/116.76 cnf(4331,plain, % 116.47/116.76 (P3(f4(f4(f4(a5,a5,a1),f4(a5,a5,a1),a1),a2,a1),f4(f4(a5,a5,a1),f4(a5,f4(a5,a5,a1),a1),a1),a1)), % 116.47/116.76 inference(scs_inference,[],[4243,3927,16])). % 116.47/116.76 cnf(4340,plain, % 116.47/116.76 (P3(f4(f4(f4(a5,a5,a1),f4(a5,a5,a1),a1),a2,a1),f4(f4(f4(a5,a5,a1),f4(a5,a5,a1),a1),a5,a1),a1)), % 116.47/116.76 inference(scs_inference,[],[4331,3809,17])). % 116.47/116.76 cnf(4358,plain, % 116.47/116.76 (P3(f4(f4(a5,a5,a1),f4(f4(a5,a5,a1),a2,a1),a1),f4(f4(f4(a5,a5,a1),f4(a5,a5,a1),a1),a5,a1),a1)), % 116.47/116.76 inference(scs_inference,[],[4340,4240,3893,4165,4294,3305,16,3999,4195])). % 116.47/116.76 cnf(4359,plain, % 116.47/116.76 (P3(f4(f4(f4(a5,a5,a1),f4(a5,a5,a1),a1),a2,a1),f4(f4(a5,f4(a5,a5,a1),a1),f4(a5,a5,a1),a1),a1)), % 116.47/116.76 inference(scs_inference,[],[4340,4240,3893,4165,4294,3305,16,3999,4195,2311])). % 116.47/116.76 cnf(4375,plain, % 116.47/116.76 (P3(f4(f4(a5,a5,a1),f4(f4(a5,a5,a1),a2,a1),a1),f4(f4(f4(a5,a5,a1),a5,a1),f4(a5,a5,a1),a1),a1)), % 116.47/116.76 inference(scs_inference,[],[4358,3305])). % 116.47/116.76 cnf(4377,plain, % 116.47/116.76 (P3(f4(f4(f4(a5,a5,a1),a5,a1),f4(a5,a2,a1),a1),f4(f4(f4(a5,a5,a1),a5,a1),f4(a5,a5,a1),a1),a1)), % 116.47/116.76 inference(scs_inference,[],[4375,2076,16])). % 116.47/116.76 cnf(4446,plain, % 116.47/116.76 (P3(f4(f4(a5,f4(a5,a5,a1),a1),f4(a5,a2,a1),a1),f4(a5,f4(f4(a5,a5,a1),f4(a5,a5,a1),a1),a1),a1)), % 116.47/116.76 inference(scs_inference,[],[4377,4089,17,2303])). % 116.47/116.76 cnf(4467,plain, % 116.47/116.76 (P3(f4(f4(a5,a5,a1),f4(a5,f4(a5,a2,a1),a1),a1),f4(a5,f4(f4(a5,a5,a1),f4(a5,a5,a1),a1),a1),a1)), % 116.47/116.76 inference(scs_inference,[],[4446,4195,2437])). % 116.47/116.76 cnf(4555,plain, % 116.47/116.76 (~P2(x45551,f4(f4(x45552,f4(x45553,x45554,a1),a1),x45555,x45556),x45557)+P2(x45551,f4(f4(f4(x45552,x45553,a1),x45554,a1),x45555,x45556),x45557)), % 116.47/116.76 inference(scs_inference,[],[1072,14])). % 116.47/116.76 cnf(4670,plain, % 116.47/116.76 (~P2(x46701,f4(f4(x46702,x46703,a1),x46704,a1),f4(f4(x46702,x46703,a1),x46704,a1))+P2(x46701,f4(x46702,f4(x46703,x46704,a1),a1),f4(x46702,f4(x46703,x46704,a1),a1))), % 116.47/116.76 inference(scs_inference,[],[74,15,14])). % 116.47/116.76 cnf(4686,plain, % 116.47/116.76 (~P2(f4(f4(x46861,x46862,a1),x46863,a1),x46864,x46865)+P2(f4(x46861,f4(x46862,x46863,a1),a1),x46864,x46865)), % 116.47/116.76 inference(scs_inference,[],[74,13])). % 116.47/116.76 cnf(4769,plain, % 116.47/116.76 (~P2(x47691,f4(f4(x47692,x47693,a1),f4(x47694,x47695,a1),a1),x47696)+P2(x47691,f4(f4(x47692,f4(x47693,x47694,a1),a1),x47695,a1),x47696)), % 116.47/116.76 inference(scs_inference,[],[1938,14])). % 116.47/116.76 cnf(4775,plain, % 116.47/116.76 (~P2(f4(x47751,f4(f4(x47752,x47753,a1),x47754,a1),a1),x47755,x47756)+P2(f4(f4(x47751,x47752,a1),f4(x47753,x47754,a1),a1),x47755,x47756)), % 116.47/116.76 inference(scs_inference,[],[2076,13])). % 116.47/116.76 cnf(4776,plain, % 116.47/116.76 (~P2(f4(x47761,f4(f4(x47762,x47763,a1),x47764,a1),a1),f4(x47765,f4(x47766,x47767,a1),a1),x47768)+P2(f4(f4(x47761,x47762,a1),f4(x47763,x47764,a1),a1),f4(f4(x47765,x47766,a1),x47767,a1),x47768)), % 116.47/116.76 inference(scs_inference,[],[75,2076,13,14])). % 116.47/116.76 cnf(4777,plain, % 116.47/116.76 (~P2(f4(x47771,f4(f4(x47772,x47773,a1),x47774,a1),a1),f4(f4(x47775,x47776,a1),f4(x47777,x47778,a1),a1),x47779)+P2(f4(f4(x47771,x47772,a1),f4(x47773,x47774,a1),a1),f4(f4(x47775,f4(x47776,x47777,a1),a1),x47778,a1),x47779)), % 116.47/116.76 inference(scs_inference,[],[75,2076,13,14,4769])). % 116.47/116.76 cnf(4810,plain, % 116.47/116.76 (~P2(f4(f4(f4(x48101,x48102,a1),f4(x48103,x48104,a1),a1),f4(x48105,x48106,a1),a1),f4(f4(x48107,x48108,a1),f4(x48109,x481010,a1),a1),f4(f4(f4(x48107,x48108,a1),x48109,a1),x481010,a1))+~P3(f4(a5,f3(f7(a10),a1),a1),x481011,a1)+~E(x481011,f4(f4(a5,a6,a1),f3(f8(a10),a1),a1))), % 116.47/116.76 inference(scs_inference,[],[75,2074,3691,13,14,4775,4670,4776,4777,4093,2412,4232,4686,4555,2286,17])). % 116.47/116.76 cnf(5108,plain, % 116.47/116.76 (P3(f4(a5,f3(f7(x51081),a1),a1),f4(a5,f4(a6,f3(f8(x51081),a1),a1),a1),a1)), % 116.47/116.76 inference(rename_variables,[],[1251])). % 116.47/116.76 cnf(5121,plain, % 116.47/116.76 (P3(f4(a5,f3(f7(x51211),a1),a1),f4(a5,f4(a6,f3(f8(x51211),a1),a1),a1),a1)), % 116.47/116.76 inference(rename_variables,[],[1251])). % 116.47/116.76 cnf(5122,plain, % 116.47/116.76 (E(f4(x51221,f4(x51222,x51223,a1),a1),f4(f4(x51221,x51222,a1),x51223,a1))), % 116.47/116.76 inference(rename_variables,[],[75])). % 116.47/116.76 cnf(5127,plain, % 116.47/116.76 ($false), % 116.47/116.76 inference(scs_inference,[],[1419,3782,3778,3780,3786,2301,1251,5108,5121,1426,1501,1583,4467,4277,4239,4359,3691,75,5122,1427,1510,1590,4,7,11,5,6,8,9,10,2311,3903,1747,1835,2574,2444,2,2437,2303,4810,14,13,17]), % 116.47/116.76 ['proof']). % 116.47/116.76 % SZS output end Proof % 116.47/116.76 % Total time :115.830000s %------------------------------------------------------------------------------