%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : ANA016-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 : n022.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 70.01s 70.11s % Output : CNFRefutation 70.10s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : ANA016-2 : TPTP v8.2.0. Released v3.2.0. % 0.08/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n022.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sun Jun 23 04:12:09 EDT 2024 % 0.13/0.34 % CPUTime : % 0.21/0.57 start to proof:theBenchmark % 70.01/70.10 %------------------------------------------- % 70.01/70.10 % File :CSE---1.7 % 70.01/70.10 % Problem :theBenchmark % 70.01/70.10 % Transform :cnf % 70.01/70.10 % Format :tptp:raw % 70.01/70.10 % Command :java -jar mcs_scs.jar %d %s % 70.01/70.10 % 70.01/70.10 % Result :Theorem 69.450000s % 70.01/70.10 % Output :CNFRefutation 69.450000s % 70.01/70.10 %------------------------------------------- % 70.01/70.11 %------------------------------------------------------------------------------ % 70.01/70.11 % File : ANA016-2 : TPTP v8.2.0. Released v3.2.0. % 70.01/70.11 % Domain : Analysis % 70.01/70.11 % Problem : Problem about Big-O notation % 70.01/70.11 % Version : [Pau06] axioms : Reduced > Especial. % 70.01/70.11 % English : % 70.01/70.11 % 70.01/70.11 % Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe % 70.01/70.11 % Source : [Pau06] % 70.01/70.11 % Names : % 70.01/70.11 % 70.01/70.11 % Status : Unsatisfiable % 70.01/70.11 % Rating : 0.10 v8.1.0, 0.05 v7.5.0, 0.11 v7.4.0, 0.12 v7.3.0, 0.17 v7.1.0, 0.08 v7.0.0, 0.13 v6.3.0, 0.18 v6.2.0, 0.10 v6.1.0, 0.29 v6.0.0, 0.10 v5.5.0, 0.25 v5.3.0, 0.33 v5.2.0, 0.19 v5.1.0, 0.18 v5.0.0, 0.14 v4.1.0, 0.23 v4.0.1, 0.27 v3.7.0, 0.10 v3.5.0, 0.18 v3.4.0, 0.25 v3.3.0, 0.29 v3.2.0 % 70.01/70.11 % Syntax : Number of clauses : 9 ( 3 unt; 1 nHn; 6 RR) % 70.01/70.11 % Number of literals : 16 ( 6 equ; 8 neg) % 70.01/70.11 % Maximal clause size : 3 ( 1 avg) % 70.01/70.11 % Maximal term depth : 4 ( 1 avg) % 70.01/70.11 % Number of predicates : 5 ( 4 usr; 0 prp; 1-2 aty) % 70.01/70.11 % Number of functors : 8 ( 8 usr; 5 con; 0-3 aty) % 70.01/70.11 % Number of variables : 11 ( 0 sgn) % 70.01/70.11 % SPC : CNF_UNS_RFO_SEQ_NHN % 70.01/70.11 % 70.01/70.11 % Comments : The problems in the [Pau06] collection each have very many axioms, % 70.01/70.11 % of which only a small selection are required for the refutation. % 70.01/70.11 % The mission is to find those few axioms, after which a refutation % 70.01/70.11 % can be quite easily found. This version has only the necessary % 70.01/70.11 % axioms. % 70.01/70.11 %------------------------------------------------------------------------------ % 70.01/70.11 cnf(cls_conjecture_0,negated_conjecture, % 70.01/70.11 v_c != c_0 ). % 70.01/70.11 % 70.01/70.11 cnf(cls_conjecture_2,negated_conjecture, % 70.01/70.11 v_g(v_x) != c_times(v_c,c_times(c_HOL_Oinverse(v_c,t_a),v_g(v_x),t_a),t_a) ). % 70.01/70.11 % 70.01/70.11 cnf(tfree_tcs,negated_conjecture, % 70.01/70.11 class_Ring__and__Field_Oordered__field(t_a) ). % 70.01/70.11 % 70.01/70.11 cnf(cls_OrderedGroup_Omonoid__mult__class_Oaxioms__1_0,axiom, % 70.01/70.11 ( ~ class_OrderedGroup_Omonoid__mult(T_a) % 70.01/70.11 | c_times(c_1,V_y,T_a) = V_y ) ). % 70.01/70.11 % 70.01/70.11 cnf(cls_OrderedGroup_Osemigroup__mult__class_Omult__assoc_0,axiom, % 70.01/70.11 ( ~ class_OrderedGroup_Osemigroup__mult(T_a) % 70.01/70.11 | 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) ) ). % 70.01/70.11 % 70.01/70.11 cnf(cls_Ring__and__Field_Oright__inverse_0,axiom, % 70.01/70.11 ( ~ class_Ring__and__Field_Ofield(T_a) % 70.01/70.11 | V_a = c_0 % 70.01/70.11 | c_times(V_a,c_HOL_Oinverse(V_a,T_a),T_a) = c_1 ) ). % 70.01/70.11 % 70.01/70.11 cnf(clsrel_Ring__and__Field_Ofield_12,axiom, % 70.01/70.11 ( ~ class_Ring__and__Field_Ofield(T) % 70.01/70.11 | class_OrderedGroup_Omonoid__mult(T) ) ). % 70.01/70.11 % 70.01/70.11 cnf(clsrel_Ring__and__Field_Ofield_21,axiom, % 70.01/70.11 ( ~ class_Ring__and__Field_Ofield(T) % 70.01/70.11 | class_OrderedGroup_Osemigroup__mult(T) ) ). % 70.01/70.11 % 70.01/70.11 cnf(clsrel_Ring__and__Field_Oordered__field_0,axiom, % 70.01/70.11 ( ~ class_Ring__and__Field_Oordered__field(T) % 70.01/70.11 | class_Ring__and__Field_Ofield(T) ) ). % 70.01/70.11 % 70.01/70.11 %------------------------------------------------------------------------------ % 70.01/70.11 %------------------------------------------- % 70.01/70.11 % Proof found % 70.01/70.11 % SZS status Theorem for theBenchmark % 70.01/70.11 % SZS output start Proof % 70.01/70.12 %ClaNum:22(EqnAxiom:13) % 70.01/70.12 %VarNum:27(SingletonVarNum:11) % 70.01/70.12 %MaxLitNum:3 % 70.01/70.12 %MaxfuncDepth:3 % 70.01/70.12 %SharedTerms:12 % 70.01/70.12 %goalClause: 14 15 16 % 70.01/70.12 %singleGoalClaCount:3 % 70.01/70.12 [14]P1(a1) % 70.01/70.12 [15]~E(a6,a2) % 70.01/70.12 [16]~E(f5(a6,f5(f3(a6,a1),f8(a7),a1),a1),f8(a7)) % 70.01/70.12 [17]~P3(x171)+P2(x171) % 70.01/70.12 [18]~P3(x181)+P4(x181) % 70.01/70.12 [19]~P1(x191)+P3(x191) % 70.01/70.12 [20]~P2(x202)+E(f5(a4,x201,x202),x201) % 70.01/70.12 [22]~P4(x223)+E(f5(f5(x221,x222,x223),x224,x223),f5(x221,f5(x222,x224,x223),x223)) % 70.01/70.12 [21]~P3(x212)+E(x211,a2)+E(f5(x211,f3(x211,x212),x212),a4) % 70.01/70.12 %EqnAxiom % 70.01/70.12 [1]E(x11,x11) % 70.01/70.12 [2]E(x22,x21)+~E(x21,x22) % 70.01/70.12 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 70.01/70.12 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43)) % 70.01/70.12 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52)) % 70.01/70.12 [6]~E(x61,x62)+E(f8(x61),f8(x62)) % 70.01/70.12 [7]~E(x71,x72)+E(f5(x71,x73,x74),f5(x72,x73,x74)) % 70.01/70.12 [8]~E(x81,x82)+E(f5(x83,x81,x84),f5(x83,x82,x84)) % 70.01/70.12 [9]~E(x91,x92)+E(f5(x93,x94,x91),f5(x93,x94,x92)) % 70.01/70.12 [10]~P1(x101)+P1(x102)+~E(x101,x102) % 70.01/70.12 [11]~P2(x111)+P2(x112)+~E(x111,x112) % 70.01/70.12 [12]~P3(x121)+P3(x122)+~E(x121,x122) % 70.01/70.12 [13]~P4(x131)+P4(x132)+~E(x131,x132) % 70.01/70.12 % 70.01/70.12 %------------------------------------------- % 70.01/70.13 cnf(23,plain, % 70.01/70.13 (~P3(x231)+E(f5(a4,x232,x231),x232)), % 70.01/70.13 inference(scs_inference,[],[17,20])). % 70.01/70.13 cnf(25,plain, % 70.01/70.13 (E(f5(a4,x251,a1),x251)), % 70.01/70.13 inference(scs_inference,[],[14,19,23])). % 70.01/70.13 cnf(26,plain, % 70.01/70.13 (E(x261,f5(a4,x261,a1))), % 70.01/70.13 inference(scs_inference,[],[25,2])). % 70.01/70.13 cnf(27,plain, % 70.01/70.13 (P1(f5(a4,a1,a1))), % 70.01/70.13 inference(scs_inference,[],[14,25,2,10])). % 70.01/70.13 cnf(28,plain, % 70.01/70.13 (~P2(f5(a4,a1,a1))+P2(a1)), % 70.01/70.13 inference(scs_inference,[],[14,25,2,10,11])). % 70.01/70.13 cnf(29,plain, % 70.01/70.13 (E(f5(a4,x291,a1),x291)), % 70.01/70.13 inference(rename_variables,[],[25])). % 70.01/70.13 cnf(32,plain, % 70.01/70.13 (~E(a6,f5(a4,a2,a1))+P2(a1)), % 70.01/70.13 inference(scs_inference,[],[14,15,25,29,2,10,11,17,3])). % 70.01/70.13 cnf(33,plain, % 70.01/70.13 (E(f5(a4,x331,a1),x331)), % 70.01/70.13 inference(rename_variables,[],[25])). % 70.01/70.13 cnf(34,plain, % 70.01/70.13 (~P3(f5(a4,f5(a4,a1,a1),a1))+P2(a1)), % 70.01/70.13 inference(scs_inference,[],[14,15,25,29,33,2,10,11,17,3,12])). % 70.01/70.13 cnf(37,plain, % 70.01/70.13 (~E(f5(a6,f5(f3(a6,a1),f8(a7),a1),a1),f5(a4,f8(a7),a1))), % 70.01/70.13 inference(scs_inference,[],[16,25,3])). % 70.01/70.13 cnf(39,plain, % 70.01/70.13 (~P2(x391)+P2(f5(a4,x391,a1))), % 70.01/70.13 inference(scs_inference,[],[16,26,25,3,11])). % 70.01/70.13 cnf(43,plain, % 70.01/70.13 (~P3(a1)+P2(f5(a4,a1,a1))), % 70.01/70.13 inference(scs_inference,[],[16,26,25,3,11,28,32,34,17])). % 70.01/70.13 cnf(48,plain, % 70.01/70.13 (~E(a6,f5(a4,a2,a1))), % 70.01/70.13 inference(scs_inference,[],[15,25,3])). % 70.01/70.13 cnf(49,plain, % 70.01/70.13 (E(f5(a4,x491,a1),x491)), % 70.01/70.13 inference(rename_variables,[],[25])). % 70.01/70.13 cnf(50,plain, % 70.01/70.13 (~P2(f5(a4,x501,a1))+P2(x501)), % 70.01/70.13 inference(scs_inference,[],[15,25,49,3,11])). % 70.01/70.13 cnf(52,plain, % 70.01/70.13 (~P3(f5(a4,x521,a1))+P2(x521)), % 70.01/70.13 inference(scs_inference,[],[15,25,49,3,11,39,17])). % 70.01/70.13 cnf(57,plain, % 70.01/70.13 (~P3(x571)+P3(f5(a4,x571,a1))), % 70.01/70.13 inference(scs_inference,[],[26,12])). % 70.01/70.13 cnf(63,plain, % 70.01/70.13 (~P4(x631)+P4(f5(a4,x631,a1))), % 70.01/70.13 inference(scs_inference,[],[26,13])). % 70.01/70.13 cnf(64,plain, % 70.01/70.13 (~P3(x641)+P4(f5(a4,x641,a1))), % 70.01/70.13 inference(scs_inference,[],[26,13,18])). % 70.01/70.13 cnf(66,plain, % 70.01/70.13 (~P3(x661)+P4(f5(a4,f5(a4,x661,a1),a1))), % 70.01/70.13 inference(scs_inference,[],[26,13,18,57])). % 70.01/70.13 cnf(73,plain, % 70.01/70.13 (~P4(f5(a4,x731,a1))+P4(x731)), % 70.01/70.13 inference(scs_inference,[],[25,13])). % 70.01/70.13 cnf(81,plain, % 70.01/70.13 (~P3(f5(a4,x811,a1))+P3(x811)), % 70.01/70.13 inference(scs_inference,[],[25,12])). % 70.01/70.13 cnf(85,plain, % 70.01/70.13 (E(f5(a4,x851,f5(a4,a1,a1)),x851)+~P3(a1)), % 70.01/70.13 inference(scs_inference,[],[43,20])). % 70.01/70.13 cnf(86,plain, % 70.01/70.13 (~P2(f5(a4,x861,a1))+E(f5(a4,x862,x861),x862)), % 70.01/70.13 inference(scs_inference,[],[50,20])). % 70.01/70.13 cnf(88,plain, % 70.01/70.13 (P1(f5(a4,f5(a4,a1,a1),a1))), % 70.01/70.13 inference(scs_inference,[],[27,26,10])). % 70.01/70.13 cnf(90,plain, % 70.01/70.13 (P4(f5(a4,f5(a4,a1,a1),a1))), % 70.01/70.13 inference(scs_inference,[],[27,64,19])). % 70.01/70.13 cnf(91,plain, % 70.01/70.13 (P4(f5(a4,a1,a1))), % 70.01/70.13 inference(scs_inference,[],[90,73])). % 70.01/70.13 cnf(92,plain, % 70.01/70.13 (P4(f5(a4,f5(a4,f5(a4,a1,a1),a1),a1))), % 70.01/70.13 inference(scs_inference,[],[26,90,73,13])). % 70.01/70.13 cnf(94,plain, % 70.01/70.13 (P4(x941)+~P3(f5(a4,x941,a1))), % 70.01/70.13 inference(scs_inference,[],[81,18])). % 70.01/70.13 cnf(95,plain, % 70.01/70.13 (P4(a1)), % 70.01/70.13 inference(scs_inference,[],[91,73])). % 70.01/70.13 cnf(97,plain, % 70.01/70.13 (E(f8(x971),f8(f5(a4,x971,a1)))), % 70.01/70.13 inference(scs_inference,[],[25,6,2])). % 70.01/70.13 cnf(98,plain, % 70.01/70.13 (E(f8(f5(a4,x981,a1)),f8(x981))), % 70.01/70.13 inference(scs_inference,[],[97,2])). % 70.01/70.13 cnf(99,plain, % 70.01/70.13 (E(f5(a4,f8(x991),a1),f8(f5(a4,x991,a1)))), % 70.01/70.13 inference(scs_inference,[],[25,97,2,3])). % 70.01/70.13 cnf(107,plain, % 70.01/70.13 (~E(f5(a6,f5(f3(a6,a1),f8(a7),a1),a1),f8(f5(a4,a7,a1)))), % 70.01/70.14 inference(scs_inference,[],[16,98,99,2,3])). % 70.01/70.14 cnf(185,plain, % 70.10/70.14 (~E(a6,f5(a4,f5(a4,a2,a1),a1))), % 70.10/70.14 inference(scs_inference,[],[48,25,3])). % 70.10/70.14 cnf(189,plain, % 70.10/70.14 (P1(f5(a4,f5(a4,f5(a4,a1,a1),a1),a1))), % 70.10/70.14 inference(scs_inference,[],[88,26,10])). % 70.10/70.14 cnf(202,plain, % 70.10/70.14 (~E(a6,f5(a4,f5(a4,f5(a4,a2,a1),a1),a1))), % 70.10/70.14 inference(scs_inference,[],[185,25,3])). % 70.10/70.14 cnf(232,plain, % 70.10/70.14 (E(x2321,f5(a4,x2321,f5(a4,a1,a1)))+~P3(a1)), % 70.10/70.14 inference(scs_inference,[],[85,2])). % 70.10/70.14 cnf(233,plain, % 70.10/70.14 (E(f3(x2331,x2332),f3(f5(a4,x2331,f5(a4,a1,a1)),x2332))+~P3(a1)), % 70.10/70.14 inference(scs_inference,[],[232,4])). % 70.10/70.14 cnf(287,plain, % 70.10/70.14 (E(f3(f5(a4,x2871,f5(a4,a1,a1)),x2872),f3(x2871,x2872))+~P3(a1)), % 70.10/70.14 inference(scs_inference,[],[233,2])). % 70.10/70.14 cnf(338,plain, % 70.10/70.14 (E(f5(a6,f3(a6,a1),a1),a4)), % 70.10/70.14 inference(scs_inference,[],[15,14,21,19])). % 70.10/70.14 cnf(339,plain, % 70.10/70.14 (E(a4,f5(a6,f3(a6,a1),a1))), % 70.10/70.14 inference(scs_inference,[],[338,2])). % 70.10/70.14 cnf(340,plain, % 70.10/70.14 (E(f5(a4,f5(a6,f3(a6,a1),a1),a1),a4)), % 70.10/70.14 inference(scs_inference,[],[25,338,2,3])). % 70.10/70.14 cnf(347,plain, % 70.10/70.14 (E(a4,f5(a4,f5(a6,f3(a6,a1),a1),a1))), % 70.10/70.14 inference(scs_inference,[],[340,2])). % 70.10/70.14 cnf(348,plain, % 70.10/70.14 (E(f5(a4,a4,a1),f5(a6,f3(a6,a1),a1))), % 70.10/70.14 inference(scs_inference,[],[25,339,340,2,3])). % 70.10/70.14 cnf(355,plain, % 70.10/70.14 (E(f5(a6,f3(a6,a1),a1),f5(a4,a4,a1))), % 70.10/70.14 inference(scs_inference,[],[348,2])). % 70.10/70.14 cnf(356,plain, % 70.10/70.14 (E(f5(a4,f5(a4,a4,a1),a1),f5(a6,f3(a6,a1),a1))), % 70.10/70.14 inference(scs_inference,[],[25,348,2,3])). % 70.10/70.14 cnf(363,plain, % 70.10/70.14 (E(f5(a6,f3(a6,a1),a1),f5(a4,f5(a4,a4,a1),a1))), % 70.10/70.14 inference(scs_inference,[],[356,2])). % 70.10/70.14 cnf(364,plain, % 70.10/70.14 (E(f5(a4,f5(a4,f5(a4,a4,a1),a1),a1),f5(a6,f3(a6,a1),a1))), % 70.10/70.14 inference(scs_inference,[],[25,356,2,3])). % 70.10/70.14 cnf(371,plain, % 70.10/70.14 (E(f5(a6,f3(a6,a1),a1),f5(a4,f5(a4,f5(a4,a4,a1),a1),a1))), % 70.10/70.14 inference(scs_inference,[],[364,2])). % 70.10/70.14 cnf(372,plain, % 70.10/70.14 (E(f5(a4,f5(a6,f3(a6,a1),a1),a1),f5(a4,f5(a4,a4,a1),a1))), % 70.10/70.14 inference(scs_inference,[],[25,364,363,2,3])). % 70.10/70.14 cnf(380,plain, % 70.10/70.14 (E(f5(a4,f5(a6,f3(a6,a1),a1),a1),f5(a4,a4,a1))), % 70.10/70.14 inference(scs_inference,[],[25,372,355,2,3])). % 70.10/70.14 cnf(386,plain, % 70.10/70.14 (E(f5(a4,a4,a1),f5(a4,f5(a6,f3(a6,a1),a1),a1))), % 70.10/70.14 inference(scs_inference,[],[380,2])). % 70.10/70.14 cnf(495,plain, % 70.10/70.14 (E(a4,f5(a4,f5(a4,a4,a1),a1))), % 70.10/70.14 inference(scs_inference,[],[339,363,3])). % 70.10/70.14 cnf(496,plain, % 70.10/70.14 (E(f5(a4,f5(a4,a4,a1),a1),a4)), % 70.10/70.14 inference(scs_inference,[],[339,363,3,2])). % 70.10/70.14 cnf(511,plain, % 70.10/70.14 (E(a4,f5(a4,f5(a4,f5(a4,a4,a1),a1),a1))), % 70.10/70.14 inference(scs_inference,[],[339,371,3])). % 70.10/70.14 cnf(512,plain, % 70.10/70.14 (E(f5(a4,f5(a4,f5(a4,a4,a1),a1),a1),a4)), % 70.10/70.14 inference(scs_inference,[],[339,371,3,2])). % 70.10/70.14 cnf(579,plain, % 70.10/70.14 (E(f5(a4,a4,a1),f5(a4,f5(a4,f5(a4,a4,a1),a1),a1))), % 70.10/70.14 inference(scs_inference,[],[348,371,3])). % 70.10/70.14 cnf(580,plain, % 70.10/70.14 (E(f5(a4,f5(a4,f5(a4,a4,a1),a1),a1),f5(a4,a4,a1))), % 70.10/70.14 inference(scs_inference,[],[348,371,3,2])). % 70.10/70.14 cnf(919,plain, % 70.10/70.14 (P2(a1)), % 70.10/70.14 inference(scs_inference,[],[14,17,19])). % 70.10/70.14 cnf(920,plain, % 70.10/70.14 (P2(f5(a4,a1,a1))), % 70.10/70.14 inference(scs_inference,[],[26,919,11])). % 70.10/70.14 cnf(922,plain, % 70.10/70.14 (~P3(x9221)+P2(f5(a4,x9221,a1))), % 70.10/70.14 inference(scs_inference,[],[17,39])). % 70.10/70.14 cnf(923,plain, % 70.10/70.14 (P2(f5(a4,f5(a4,a1,a1),a1))), % 70.10/70.14 inference(scs_inference,[],[26,920,11])). % 70.10/70.14 cnf(925,plain, % 70.10/70.14 (E(f5(a4,x9251,f5(a4,a1,a1)),x9251)), % 70.10/70.14 inference(scs_inference,[],[26,920,11,86])). % 70.10/70.14 cnf(927,plain, % 70.10/70.14 (E(x9271,f5(a4,x9271,f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[26,920,11,86,2])). % 70.10/70.14 cnf(928,plain, % 70.10/70.14 (~E(f5(a6,f5(f3(a6,a1),f8(a7),a1),a1),f5(a4,f8(a7),f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[16,26,920,11,86,2,3])). % 70.10/70.14 cnf(933,plain, % 70.10/70.14 (P1(f5(a4,a1,f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[14,927,10])). % 70.10/70.14 cnf(934,plain, % 70.10/70.14 (E(x9341,f5(a4,x9341,f5(a4,a1,a1)))), % 70.10/70.14 inference(rename_variables,[],[927])). % 70.10/70.14 cnf(936,plain, % 70.10/70.14 (E(x9361,f5(a4,x9361,f5(a4,a1,a1)))), % 70.10/70.14 inference(rename_variables,[],[927])). % 70.10/70.14 cnf(937,plain, % 70.10/70.14 (P2(f5(a4,f5(a4,a1,a1),f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[14,92,920,927,934,936,10,13,11])). % 70.10/70.14 cnf(939,plain, % 70.10/70.14 (~P3(f5(a4,x9391,f5(a4,a1,a1)))+P3(x9391)), % 70.10/70.14 inference(scs_inference,[],[14,92,920,925,927,934,936,10,13,11,12])). % 70.10/70.14 cnf(970,plain, % 70.10/70.14 (P4(x9701)+~P3(f5(a4,x9701,f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[939,18])). % 70.10/70.14 cnf(972,plain, % 70.10/70.14 (E(x9721,f5(a4,x9721,f5(a4,a1,a1)))), % 70.10/70.14 inference(rename_variables,[],[927])). % 70.10/70.14 cnf(973,plain, % 70.10/70.14 (~P3(x9731)+P3(f5(a4,x9731,f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[91,927,972,13,12])). % 70.10/70.14 cnf(974,plain, % 70.10/70.14 (~P3(f5(a4,x9741,f5(a4,a1,a1)))+E(f5(f5(x9742,x9743,x9741),x9744,x9741),f5(x9742,f5(x9743,x9744,x9741),x9741))), % 70.10/70.14 inference(scs_inference,[],[970,22])). % 70.10/70.14 cnf(975,plain, % 70.10/70.14 (P4(f5(a4,f5(a4,f5(a4,a1,a1),a1),f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[90,927,13])). % 70.10/70.14 cnf(977,plain, % 70.10/70.14 (P3(f5(a4,a1,f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[14,973,19])). % 70.10/70.14 cnf(978,plain, % 70.10/70.14 (P3(a1)), % 70.10/70.14 inference(scs_inference,[],[977,939])). % 70.10/70.14 cnf(979,plain, % 70.10/70.14 (E(f5(f5(x9791,x9792,a1),x9793,a1),f5(x9791,f5(x9792,x9793,a1),a1))), % 70.10/70.14 inference(scs_inference,[],[977,939,974])). % 70.10/70.14 cnf(981,plain, % 70.10/70.14 (E(f5(x9811,f5(x9812,x9813,a1),a1),f5(f5(x9811,x9812,a1),x9813,a1))), % 70.10/70.14 inference(scs_inference,[],[977,939,974,2])). % 70.10/70.14 cnf(982,plain, % 70.10/70.14 (~E(a6,f5(f5(a4,a4,a1),f5(a4,a2,a1),a1))), % 70.10/70.14 inference(scs_inference,[],[202,977,939,974,2,3])). % 70.10/70.14 cnf(985,plain, % 70.10/70.14 (E(f3(x9851,x9852),f3(f5(a4,x9851,f5(a4,a1,a1)),x9852))), % 70.10/70.14 inference(scs_inference,[],[26,202,977,939,974,2,3,12,233])). % 70.10/70.14 cnf(986,plain, % 70.10/70.14 (E(f3(f5(a4,x9861,f5(a4,a1,a1)),x9862),f3(x9861,x9862))), % 70.10/70.14 inference(scs_inference,[],[26,202,977,939,974,2,3,12,233,287])). % 70.10/70.14 cnf(987,plain, % 70.10/70.14 (P4(f5(a4,a1,f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[26,202,977,939,974,2,3,12,233,287,94])). % 70.10/70.14 cnf(989,plain, % 70.10/70.14 (P2(f5(a4,a1,f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[26,202,977,939,974,2,3,12,233,287,94,52])). % 70.10/70.14 cnf(996,plain, % 70.10/70.14 (~E(a6,f5(f5(f5(a4,a4,a1),a4,a1),a2,a1))), % 70.10/70.14 inference(scs_inference,[],[979,982,3])). % 70.10/70.14 cnf(998,plain, % 70.10/70.14 (P1(f5(f5(a4,a4,a1),f5(a4,a1,a1),a1))), % 70.10/70.14 inference(scs_inference,[],[189,979,981,982,3,10])). % 70.10/70.14 cnf(999,plain, % 70.10/70.14 (E(f5(x9991,f5(x9992,x9993,a1),a1),f5(f5(x9991,x9992,a1),x9993,a1))), % 70.10/70.14 inference(rename_variables,[],[981])). % 70.10/70.14 cnf(1000,plain, % 70.10/70.14 (P4(f5(f5(a4,a4,a1),f5(a4,a1,a1),a1))), % 70.10/70.14 inference(scs_inference,[],[189,92,979,981,999,982,3,10,13])). % 70.10/70.14 cnf(1001,plain, % 70.10/70.14 (E(f5(x10011,f5(x10012,x10013,a1),a1),f5(f5(x10011,x10012,a1),x10013,a1))), % 70.10/70.14 inference(rename_variables,[],[981])). % 70.10/70.14 cnf(1002,plain, % 70.10/70.14 (P2(f5(f5(a4,a4,a1),a1,a1))), % 70.10/70.14 inference(scs_inference,[],[189,92,923,979,981,999,1001,982,3,10,13,11])). % 70.10/70.14 cnf(1004,plain, % 70.10/70.14 (P3(f5(a4,f5(a4,a1,f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[189,92,923,927,977,979,981,999,1001,982,3,10,13,11,12])). % 70.10/70.14 cnf(1007,plain, % 70.10/70.14 (~E(a6,f5(f5(a4,a4,a1),a2,a1))), % 70.10/70.14 inference(scs_inference,[],[185,979,3])). % 70.10/70.14 cnf(1009,plain, % 70.10/70.14 (P1(f5(f5(f5(a4,a4,a1),a4,a1),a1,a1))), % 70.10/70.14 inference(scs_inference,[],[998,185,979,981,3,10])). % 70.10/70.14 cnf(1010,plain, % 70.10/70.14 (E(f5(x10101,f5(x10102,x10103,a1),a1),f5(f5(x10101,x10102,a1),x10103,a1))), % 70.10/70.14 inference(rename_variables,[],[981])). % 70.10/70.14 cnf(1011,plain, % 70.10/70.14 (P4(f5(f5(a4,a4,a1),a1,a1))), % 70.10/70.14 inference(scs_inference,[],[998,90,185,979,981,1010,3,10,13])). % 70.10/70.14 cnf(1020,plain, % 70.10/70.14 (P1(f5(f5(a4,a4,a1),a1,a1))), % 70.10/70.14 inference(scs_inference,[],[88,981,10])). % 70.10/70.14 cnf(1030,plain, % 70.10/70.14 (~P3(f5(f5(x10301,x10302,a1),x10303,a1))+P3(f5(x10301,f5(x10302,x10303,a1),a1))), % 70.10/70.14 inference(scs_inference,[],[979,986,10,13,12])). % 70.10/70.14 cnf(1042,plain, % 70.10/70.14 (~P3(f5(x10421,f5(x10422,x10423,a1),a1))+P3(f5(f5(x10421,x10422,a1),x10423,a1))), % 70.10/70.14 inference(scs_inference,[],[981,12])). % 70.10/70.14 cnf(1046,plain, % 70.10/70.14 (~E(a6,f5(a4,a2,f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[15,925,3])). % 70.10/70.14 cnf(1110,plain, % 70.10/70.14 (P1(f5(a4,f5(a4,a1,a1),f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[27,927,10])). % 70.10/70.14 cnf(1115,plain, % 70.10/70.14 (~E(a6,f5(a4,f5(a4,a2,a1),f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[48,925,3])). % 70.10/70.14 cnf(1119,plain, % 70.10/70.14 (P1(f5(a4,f5(a4,f5(a4,a1,a1),a1),f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[88,927,10])). % 70.10/70.14 cnf(1132,plain, % 70.10/70.14 (~E(a6,f5(a4,f5(a4,f5(a4,a2,a1),a1),f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[185,925,3])). % 70.10/70.14 cnf(1136,plain, % 70.10/70.14 (P1(f5(a4,f5(a4,f5(a4,f5(a4,a1,a1),a1),a1),f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[189,927,10])). % 70.10/70.14 cnf(1139,plain, % 70.10/70.14 (~P3(f5(x11391,f5(x11392,x11393,a1),a1))+P3(f5(a4,f5(f5(x11391,x11392,a1),x11393,a1),a1))), % 70.10/70.14 inference(scs_inference,[],[1042,57])). % 70.10/70.14 cnf(1140,plain, % 70.10/70.14 (~E(a6,f5(a4,f5(a4,f5(a4,f5(a4,a2,a1),a1),a1),f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[202,925,3])). % 70.10/70.14 cnf(1170,plain, % 70.10/70.14 (E(x11701,f5(a4,x11701,f5(a4,f5(a4,a1,a1),a1)))), % 70.10/70.14 inference(scs_inference,[],[923,26,11,86,2])). % 70.10/70.14 cnf(1171,plain, % 70.10/70.14 (~E(a6,f5(a4,a2,f5(a4,f5(a4,a1,a1),a1)))), % 70.10/70.14 inference(scs_inference,[],[923,15,26,11,86,2,3])). % 70.10/70.14 cnf(1176,plain, % 70.10/70.14 (P1(f5(a4,a1,f5(a4,f5(a4,a1,a1),a1)))), % 70.10/70.14 inference(scs_inference,[],[14,1170,10])). % 70.10/70.14 cnf(1177,plain, % 70.10/70.14 (E(x11771,f5(a4,x11771,f5(a4,f5(a4,a1,a1),a1)))), % 70.10/70.14 inference(rename_variables,[],[1170])). % 70.10/70.14 cnf(1178,plain, % 70.10/70.14 (P2(f5(a4,f5(a4,f5(a4,a1,a1),a1),f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[923,14,927,1170,10,11])). % 70.10/70.14 cnf(1181,plain, % 70.10/70.14 (E(x11811,f5(a4,x11811,f5(a4,f5(a4,a1,a1),a1)))), % 70.10/70.14 inference(rename_variables,[],[1170])). % 70.10/70.14 cnf(1182,plain, % 70.10/70.14 (P3(f5(a4,f5(a4,a1,f5(a4,a1,a1)),f5(a4,f5(a4,a1,a1),a1)))), % 70.10/70.14 inference(scs_inference,[],[923,14,91,927,977,1170,1177,1181,10,11,13,12])). % 70.10/70.14 cnf(1189,plain, % 70.10/70.14 (E(f5(a4,f5(a6,f3(a6,a1),a1),f5(a4,a1,a1)),a4)), % 70.10/70.14 inference(scs_inference,[],[925,338,3])). % 70.10/70.14 cnf(1193,plain, % 70.10/70.14 (E(a4,f5(a4,f5(a6,f3(a6,a1),a1),f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[925,338,920,1170,3,11,2])). % 70.10/70.14 cnf(1308,plain, % 70.10/70.14 (E(f5(a4,f5(a6,f3(a6,a1),a1),f5(a4,a1,a1)),f5(a4,f5(a4,a4,a1),a1))), % 70.10/70.14 inference(scs_inference,[],[925,363,3])). % 70.10/70.14 cnf(1310,plain, % 70.10/70.14 (E(f5(a4,f5(a4,a4,a1),a1),f5(a4,f5(a6,f3(a6,a1),a1),f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[925,363,3,2])). % 70.10/70.14 cnf(1317,plain, % 70.10/70.14 (E(f5(a4,f5(a6,f3(a6,a1),a1),a1),f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[925,386,3,2])). % 70.10/70.14 cnf(1339,plain, % 70.10/70.14 (E(f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)),f5(a6,f3(a6,a1),a1))), % 70.10/70.14 inference(scs_inference,[],[925,348,3])). % 70.10/70.14 cnf(1341,plain, % 70.10/70.14 (E(f5(a6,f3(a6,a1),a1),f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[925,348,3,2])). % 70.10/70.14 cnf(1410,plain, % 70.10/70.14 (E(f5(a4,f5(a4,f5(a4,a4,a1),a1),f5(a4,a1,a1)),f5(a6,f3(a6,a1),a1))), % 70.10/70.14 inference(scs_inference,[],[925,356,3])). % 70.10/70.14 cnf(1412,plain, % 70.10/70.14 (E(f5(a6,f3(a6,a1),a1),f5(a4,f5(a4,f5(a4,a4,a1),a1),f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[925,356,3,2])). % 70.10/70.14 cnf(1417,plain, % 70.10/70.14 (E(f5(a4,f5(a6,f3(a6,a1),a1),f5(a4,a1,a1)),f5(a4,a4,a1))), % 70.10/70.14 inference(scs_inference,[],[925,355,3])). % 70.10/70.14 cnf(1419,plain, % 70.10/70.14 (E(f5(a4,a4,a1),f5(a4,f5(a6,f3(a6,a1),a1),f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[925,355,3,2])). % 70.10/70.14 cnf(1470,plain, % 70.10/70.14 (E(f5(a4,a4,f5(a4,a1,a1)),f5(a6,f3(a6,a1),a1))), % 70.10/70.14 inference(scs_inference,[],[925,339,3])). % 70.10/70.14 cnf(1472,plain, % 70.10/70.14 (E(f5(a6,f3(a6,a1),a1),f5(a4,a4,f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[925,339,3,2])). % 70.10/70.14 cnf(1476,plain, % 70.10/70.14 (E(f5(a4,f5(a4,f5(a6,f3(a6,a1),a1),a1),f5(a4,a1,a1)),f5(a4,a4,a1))), % 70.10/70.14 inference(scs_inference,[],[925,380,3])). % 70.10/70.14 cnf(1488,plain, % 70.10/70.14 (E(f5(a4,f5(a4,f5(a6,f3(a6,a1),a1),a1),f5(a4,a1,a1)),a4)), % 70.10/70.14 inference(scs_inference,[],[925,340,1476,2,3])). % 70.10/70.14 cnf(1558,plain, % 70.10/70.14 (E(f5(a4,a4,f5(a4,a1,a1)),f5(a4,f5(a4,a4,a1),a1))), % 70.10/70.14 inference(scs_inference,[],[925,495,1488,2,3])). % 70.10/70.14 cnf(1565,plain, % 70.10/70.14 (E(f5(a4,f5(a4,f5(a4,a4,a1),a1),f5(a4,a1,a1)),a4)), % 70.10/70.14 inference(scs_inference,[],[925,496,1558,2,3])). % 70.10/70.14 cnf(1571,plain, % 70.10/70.14 (E(a4,f5(a4,f5(a4,f5(a4,a4,a1),a1),f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[1565,2])). % 70.10/70.14 cnf(1572,plain, % 70.10/70.14 (E(f5(a4,a4,f5(a4,a1,a1)),f5(a4,f5(a4,f5(a4,a4,a1),a1),a1))), % 70.10/70.14 inference(scs_inference,[],[925,511,1565,2,3])). % 70.10/70.14 cnf(1579,plain, % 70.10/70.14 (E(f5(a4,f5(a4,f5(a4,f5(a4,a4,a1),a1),a1),f5(a4,a1,a1)),a4)), % 70.10/70.14 inference(scs_inference,[],[925,512,1572,2,3])). % 70.10/70.14 cnf(1586,plain, % 70.10/70.14 (E(f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)),f5(a4,f5(a4,f5(a4,a4,a1),a1),a1))), % 70.10/70.14 inference(scs_inference,[],[925,579,1579,2,3])). % 70.10/70.14 cnf(1593,plain, % 70.10/70.14 (E(f5(a4,f5(a4,f5(a4,f5(a4,a4,a1),a1),a1),f5(a4,a1,a1)),f5(a4,a4,a1))), % 70.10/70.14 inference(scs_inference,[],[925,580,1586,2,3])). % 70.10/70.14 cnf(1615,plain, % 70.10/70.14 (E(f5(a4,f3(x16151,x16152),f5(a4,a1,a1)),f3(f5(a4,x16151,f5(a4,a1,a1)),x16152))), % 70.10/70.14 inference(scs_inference,[],[925,985,1593,2,3])). % 70.10/70.14 cnf(1622,plain, % 70.10/70.14 (E(f5(a4,f3(f5(a4,x16221,f5(a4,a1,a1)),x16222),f5(a4,a1,a1)),f3(x16221,x16222))), % 70.10/70.14 inference(scs_inference,[],[925,986,1615,2,3])). % 70.10/70.14 cnf(1629,plain, % 70.10/70.14 (E(f5(a4,f5(a4,f5(a6,f3(a6,a1),a1),f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,f5(a4,a4,a1),a1))), % 70.10/70.14 inference(scs_inference,[],[925,1308,1622,2,3])). % 70.10/70.14 cnf(1636,plain, % 70.10/70.14 (E(f5(a4,f5(a4,f5(a6,f3(a6,a1),a1),f5(a4,a1,a1)),f5(a4,a1,a1)),a4)), % 70.10/70.14 inference(scs_inference,[],[925,1189,1629,2,3])). % 70.10/70.14 cnf(1716,plain, % 70.10/70.14 (E(a4,f5(a4,f5(a4,f5(a6,f3(a6,a1),a1),f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[1636,2])). % 70.10/70.14 cnf(1717,plain, % 70.10/70.14 (E(f5(a4,f5(a4,f5(a6,f3(a6,a1),a1),f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,a4,a1))), % 70.10/70.14 inference(scs_inference,[],[925,1417,1636,2,3])). % 70.10/70.14 cnf(1728,plain, % 70.10/70.14 (E(f5(a4,f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a6,f3(a6,a1),a1))), % 70.10/70.14 inference(scs_inference,[],[925,1339,1717,2,3])). % 70.10/70.14 cnf(1734,plain, % 70.10/70.14 (E(f5(a6,f3(a6,a1),a1),f5(a4,f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[1728,2])). % 70.10/70.14 cnf(1735,plain, % 70.10/70.14 (E(f5(a4,f5(a4,a4,f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a6,f3(a6,a1),a1))), % 70.10/70.14 inference(scs_inference,[],[925,1470,1728,2,3])). % 70.10/70.14 cnf(1746,plain, % 70.10/70.14 (E(f5(a6,f3(a6,a1),a1),f5(a4,f5(a4,a4,f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[1735,2])). % 70.10/70.14 cnf(1747,plain, % 70.10/70.14 (E(f5(a4,a4,f5(a4,a1,a1)),f5(a4,f5(a6,f3(a6,a1),a1),f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[925,1193,1735,2,3])). % 70.10/70.14 cnf(1754,plain, % 70.10/70.14 (E(f5(a4,f5(a6,f3(a6,a1),a1),f5(a4,a1,a1)),f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)))), % 70.10/70.14 inference(scs_inference,[],[925,1341,1747,2,3])). % 70.10/70.15 cnf(1762,plain, % 70.10/70.15 (E(f5(a4,f5(a6,f3(a6,a1),a1),f5(a4,a1,a1)),f5(a4,f5(a4,f5(a4,a4,a1),a1),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[925,1412,1754,2,3])). % 70.10/70.15 cnf(1768,plain, % 70.10/70.15 (E(f5(a4,f5(a4,f5(a4,f5(a4,a4,a1),a1),f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a6,f3(a6,a1),a1))), % 70.10/70.15 inference(scs_inference,[],[925,1410,1762,2,3])). % 70.10/70.15 cnf(1776,plain, % 70.10/70.15 (E(f5(a4,f5(a4,f5(a4,f5(a6,f3(a6,a1),a1),f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,a4,a1))), % 70.10/70.15 inference(scs_inference,[],[925,1717,1768,2,3])). % 70.10/70.15 cnf(1783,plain, % 70.10/70.15 (E(f5(a4,f5(a6,f3(a6,a1),a1),f5(a4,a1,a1)),f5(a4,f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[925,1776,1734,2,3])). % 70.10/70.15 cnf(1868,plain, % 70.10/70.15 (E(f5(a4,f5(a6,f3(a6,a1),a1),f5(a4,a1,a1)),f5(a4,f5(a4,a4,f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[925,1783,1746,2,3])). % 70.10/70.15 cnf(1874,plain, % 70.10/70.15 (E(f5(a4,f5(a4,a4,f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,f5(a6,f3(a6,a1),a1),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[1868,2])). % 70.10/70.15 cnf(1875,plain, % 70.10/70.15 (E(f5(a4,a4,f5(a4,a1,a1)),f5(a4,f5(a4,f5(a4,a4,a1),a1),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[925,1868,1571,2,3])). % 70.10/70.15 cnf(1881,plain, % 70.10/70.15 (E(f5(a4,f5(a4,f5(a4,a4,a1),a1),f5(a4,a1,a1)),f5(a4,a4,f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[1875,2])). % 70.10/70.15 cnf(1882,plain, % 70.10/70.15 (E(f5(a4,f5(a4,a4,f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,f5(a4,f5(a4,a4,a1),a1),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[925,1875,2,3])). % 70.10/70.15 cnf(1889,plain, % 70.10/70.15 (E(f5(a4,f5(a4,f5(a4,f5(a4,a4,a1),a1),f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,a4,f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[925,1881,1882,2,3])). % 70.10/70.15 cnf(1895,plain, % 70.10/70.15 (E(f5(a4,a4,f5(a4,a1,a1)),f5(a4,f5(a4,f5(a6,f3(a6,a1),a1),f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[925,1889,1716,2,3])). % 70.10/70.15 cnf(1902,plain, % 70.10/70.15 (E(f5(a4,f5(a4,f5(a6,f3(a6,a1),a1),f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[925,1895,1754,2,3])). % 70.10/70.15 cnf(1914,plain, % 70.10/70.15 (E(f5(a4,f5(a4,a4,f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,f5(a4,a4,a1),a1))), % 70.10/70.15 inference(scs_inference,[],[925,1902,1558,2,3])). % 70.10/70.15 cnf(1992,plain, % 70.10/70.15 (E(f5(a4,f5(a4,f5(a4,a4,f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,f5(a4,a4,a1),a1))), % 70.10/70.15 inference(scs_inference,[],[925,1914,2,3])). % 70.10/70.15 cnf(2005,plain, % 70.10/70.15 (E(f5(a4,f5(a4,f5(a4,f5(a4,a4,a1),a1),f5(a4,a1,a1)),f5(a4,a1,a1)),a4)), % 70.10/70.15 inference(scs_inference,[],[925,1992,1565,2,3])). % 70.10/70.15 cnf(2011,plain, % 70.10/70.15 (E(a4,f5(a4,f5(a4,f5(a4,f5(a4,a4,a1),a1),f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[2005,2])). % 70.10/70.15 cnf(3600,plain, % 70.10/70.15 (E(f5(a4,a4,a1),f5(a4,a4,f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[348,1472,3])). % 70.10/70.15 cnf(3607,plain, % 70.10/70.15 (E(f5(a4,a4,a1),f5(a4,f5(a4,f5(a4,a4,a1),a1),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[348,1412,3])). % 70.10/70.15 cnf(3608,plain, % 70.10/70.15 (E(f5(a4,f5(a4,f5(a4,a4,a1),a1),f5(a4,a1,a1)),f5(a4,a4,a1))), % 70.10/70.15 inference(scs_inference,[],[348,1412,3,2])). % 70.10/70.15 cnf(3626,plain, % 70.10/70.15 (E(f5(a4,a4,a1),f5(a4,f5(a4,a4,f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[348,1746,3])). % 70.10/70.15 cnf(3627,plain, % 70.10/70.15 (E(f5(a4,f5(a4,a4,f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,a4,a1))), % 70.10/70.15 inference(scs_inference,[],[348,1746,3,2])). % 70.10/70.15 cnf(3633,plain, % 70.10/70.15 (E(a4,f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[347,1317,3])). % 70.10/70.15 cnf(3634,plain, % 70.10/70.15 (E(f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)),a4)), % 70.10/70.15 inference(scs_inference,[],[347,1317,3,2])). % 70.10/70.15 cnf(3654,plain, % 70.10/70.15 (E(f5(a4,a4,a1),f5(a4,f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[348,1734,3])). % 70.10/70.15 cnf(3655,plain, % 70.10/70.15 (E(f5(a4,f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,a4,a1))), % 70.10/70.15 inference(scs_inference,[],[348,1734,3,2])). % 70.10/70.15 cnf(5858,plain, % 70.10/70.15 (E(f5(a4,f5(a4,a4,a1),a1),f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[1310,1754,3])). % 70.10/70.15 cnf(5859,plain, % 70.10/70.15 (P1(f5(a4,f5(a4,a1,f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[933,1310,927,1754,3,10])). % 70.10/70.15 cnf(5872,plain, % 70.10/70.15 (E(a4,f5(a4,f5(a4,a4,f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[1193,1868,3])). % 70.10/70.15 cnf(5873,plain, % 70.10/70.15 (P1(f5(a4,f5(a4,a1,f5(a4,a1,a1)),a1))), % 70.10/70.15 inference(scs_inference,[],[933,1193,1868,26,3,10])). % 70.10/70.15 cnf(5875,plain, % 70.10/70.15 (E(f5(a4,f5(a4,a4,f5(a4,a1,a1)),f5(a4,a1,a1)),a4)), % 70.10/70.15 inference(scs_inference,[],[933,1193,1868,26,3,10,2])). % 70.10/70.15 cnf(5908,plain, % 70.10/70.15 (E(a4,f5(a4,f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[1193,1783,3])). % 70.10/70.15 cnf(5909,plain, % 70.10/70.15 (E(f5(a4,f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)),f5(a4,a1,a1)),a4)), % 70.10/70.15 inference(scs_inference,[],[1193,1783,3,2])). % 70.10/70.15 cnf(6014,plain, % 70.10/70.15 (E(x60141,f5(a4,x60141,f5(a4,f5(a4,a1,a1),f5(a4,a1,a1))))), % 70.10/70.15 inference(scs_inference,[],[937,26,11,86,2])). % 70.10/70.15 cnf(6015,plain, % 70.10/70.15 (E(f5(a6,f3(a6,a1),a1),f5(a4,a4,f5(a4,f5(a4,a1,a1),f5(a4,a1,a1))))), % 70.10/70.15 inference(scs_inference,[],[937,338,26,11,86,2,3])). % 70.10/70.15 cnf(6157,plain, % 70.10/70.15 (P1(f5(a4,a1,f5(a4,f5(a4,a1,a1),f5(a4,a1,a1))))), % 70.10/70.15 inference(scs_inference,[],[14,348,6014,6015,2,3,10])). % 70.10/70.15 cnf(6158,plain, % 70.10/70.15 (E(x61581,f5(a4,x61581,f5(a4,f5(a4,a1,a1),f5(a4,a1,a1))))), % 70.10/70.15 inference(rename_variables,[],[6014])). % 70.10/70.15 cnf(6159,plain, % 70.10/70.15 (P3(f5(a4,f5(a4,a1,f5(a4,a1,a1)),f5(a4,f5(a4,a1,a1),f5(a4,a1,a1))))), % 70.10/70.15 inference(scs_inference,[],[14,348,977,6014,6158,6015,2,3,10,12])). % 70.10/70.15 cnf(6428,plain, % 70.10/70.15 (P3(f5(a4,f5(a4,f5(a4,a1,f5(a4,a1,a1)),f5(a4,f5(a4,a1,a1),a1)),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[989,1182,5858,1004,20,23,6,4,5,7,8,9,973])). % 70.10/70.15 cnf(6429,plain, % 70.10/70.15 (E(f5(f5(x64291,x64292,f5(a4,a1,a1)),x64293,f5(a4,a1,a1)),f5(x64291,f5(x64292,x64293,f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[989,1182,5858,1004,91,20,23,6,4,5,7,8,9,973,22])). % 70.10/70.15 cnf(6436,plain, % 70.10/70.15 (P3(f5(a4,f5(a4,a1,a1),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[1110,989,1182,5858,1004,91,20,23,6,4,5,7,8,9,973,22,922,39,17,19])). % 70.10/70.15 cnf(6439,plain, % 70.10/70.15 (P3(f5(a4,a1,a1))), % 70.10/70.15 inference(scs_inference,[],[978,1110,989,1182,5858,1004,91,977,20,23,6,4,5,7,8,9,973,22,922,39,17,19,66,57])). % 70.10/70.15 cnf(6445,plain, % 70.10/70.15 (~E(f5(f5(a4,a4,a1),a2,a1),a6)), % 70.10/70.15 inference(scs_inference,[],[978,1110,989,1011,1007,1182,5858,1004,91,977,20,23,6,4,5,7,8,9,973,22,922,39,17,19,66,57,64,63,18,2])). % 70.10/70.15 cnf(6447,plain, % 70.10/70.15 (E(x64471,f5(a4,x64471,f5(a4,f5(a4,a1,a1),f5(a4,a1,a1))))), % 70.10/70.15 inference(rename_variables,[],[6014])). % 70.10/70.15 cnf(6448,plain, % 70.10/70.15 (P1(f5(a4,f5(a4,f5(a4,a1,a1),f5(a4,a1,a1)),f5(a4,f5(a4,a1,a1),f5(a4,a1,a1))))), % 70.10/70.15 inference(scs_inference,[],[978,1110,989,1011,1007,1182,5858,1004,6014,6447,91,977,20,23,6,4,5,7,8,9,973,22,922,39,17,19,66,57,64,63,18,2,3,10])). % 70.10/70.15 cnf(6449,plain, % 70.10/70.15 (E(x64491,f5(a4,x64491,f5(a4,f5(a4,a1,a1),f5(a4,a1,a1))))), % 70.10/70.15 inference(rename_variables,[],[6014])). % 70.10/70.15 cnf(6451,plain, % 70.10/70.15 (E(x64511,f5(a4,x64511,f5(a4,f5(a4,a1,a1),f5(a4,a1,a1))))), % 70.10/70.15 inference(rename_variables,[],[6014])). % 70.10/70.15 cnf(6452,plain, % 70.10/70.15 (P3(f5(a4,a1,f5(a4,f5(a4,a1,a1),f5(a4,a1,a1))))), % 70.10/70.15 inference(scs_inference,[],[95,978,1110,989,1011,1007,1182,5858,1004,6014,6447,6449,6451,91,977,20,23,6,4,5,7,8,9,973,22,922,39,17,19,66,57,64,63,18,2,3,10,13,12])). % 70.10/70.15 cnf(6462,plain, % 70.10/70.15 (E(f5(f5(a4,a4,a1),x64621,x64622),f5(f5(a4,f5(a4,f5(a4,a4,a1),a1),f5(a4,a1,a1)),x64621,x64622))), % 70.10/70.15 inference(scs_inference,[],[1002,3607,20,4,8,7])). % 70.10/70.15 cnf(6463,plain, % 70.10/70.15 (P3(f5(a4,f5(a4,f5(a4,a1,a1),f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[6436,1002,3607,20,4,8,7,973])). % 70.10/70.15 cnf(6472,plain, % 70.10/70.15 (P3(f5(f5(a4,a4,a1),a1,a1))), % 70.10/70.15 inference(scs_inference,[],[6436,1020,1002,6452,3607,20,4,8,7,973,9,6,5,922,39,17,19])). % 70.10/70.15 cnf(6474,plain, % 70.10/70.15 (P3(f5(a4,f5(a4,a1,a1),a1))), % 70.10/70.15 inference(scs_inference,[],[6436,1020,1002,6452,3607,20,4,8,7,973,9,6,5,922,39,17,19,1030])). % 70.10/70.15 cnf(6477,plain, % 70.10/70.15 (P3(f5(a4,f5(a4,f5(a4,a1,a1),f5(a4,a1,a1)),a1))), % 70.10/70.15 inference(scs_inference,[],[6436,1020,1002,6452,3607,20,4,8,7,973,9,6,5,922,39,17,19,1030,64,57])). % 70.10/70.15 cnf(6481,plain, % 70.10/70.15 (~E(f5(f5(f5(a4,a4,a1),a4,a1),a2,a1),a6)), % 70.10/70.15 inference(scs_inference,[],[6436,1020,1000,1002,996,6452,6159,3607,20,4,8,7,973,9,6,5,922,39,17,19,1030,64,57,63,18,2])). % 70.10/70.15 cnf(6482,plain, % 70.10/70.15 (E(f5(a6,f3(a6,f5(a4,a1,a1)),f5(a4,a1,a1)),a4)), % 70.10/70.15 inference(scs_inference,[],[6439,6436,1020,1000,1002,996,6452,6159,3607,15,20,4,8,7,973,9,6,5,922,39,17,19,1030,64,57,63,18,2,21])). % 70.10/70.15 cnf(6486,plain, % 70.10/70.15 (P3(f5(a4,f5(f5(a4,a4,a1),a1,a1),a1))), % 70.10/70.15 inference(scs_inference,[],[6439,6436,1020,1000,1002,6445,996,6452,6159,3607,6014,15,20,4,8,7,973,9,6,5,922,39,17,19,1030,64,57,63,18,2,21,3,1139])). % 70.10/70.15 cnf(6489,plain, % 70.10/70.15 (P3(f5(f5(a4,f5(a4,a4,a1),a1),a1,a1))), % 70.10/70.15 inference(scs_inference,[],[6439,6436,1020,1000,1002,6445,996,6452,6159,3607,6014,15,20,4,8,7,973,9,6,5,922,39,17,19,1030,64,57,63,18,2,21,3,1139,23,1042])). % 70.10/70.15 cnf(6497,plain, % 70.10/70.15 (P3(f5(a4,f5(f5(a4,a4,a1),a1,a1),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[6472,1178,6482,20,7,4,9,6,8,973])). % 70.10/70.15 cnf(6502,plain, % 70.10/70.15 (P3(f5(a4,f5(a4,f5(a4,a1,a1),a1),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[6472,1178,1119,6482,6489,20,7,4,9,6,8,973,5,39,17,19])). % 70.10/70.15 cnf(6506,plain, % 70.10/70.15 (P3(f5(a4,f5(a4,f5(a4,a1,a1),a1),a1))), % 70.10/70.15 inference(scs_inference,[],[6472,6474,6463,1178,1119,6482,6489,20,7,4,9,6,8,973,5,39,17,19,64,57])). % 70.10/70.15 cnf(6508,plain, % 70.10/70.15 (P4(f5(a4,f5(a4,f5(a4,a1,a1),f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[6472,6474,6463,1178,1119,975,6482,6489,20,7,4,9,6,8,973,5,39,17,19,64,57,63,18])). % 70.10/70.15 cnf(6511,plain, % 70.10/70.15 (E(f5(a6,f3(a6,f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,f5(a4,a4,f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[6472,6474,6463,1178,1119,975,6482,1171,6489,5872,20,7,4,9,6,8,973,5,39,17,19,64,57,63,18,2,3])). % 70.10/70.15 cnf(6512,plain, % 70.10/70.15 (P3(f5(f5(a4,a4,a1),f5(a4,a1,a1),a1))), % 70.10/70.15 inference(scs_inference,[],[6472,6474,6463,1178,1119,975,6482,1171,6489,5872,20,7,4,9,6,8,973,5,39,17,19,64,57,63,18,2,3,1042])). % 70.10/70.15 cnf(6515,plain, % 70.10/70.15 (P3(f5(a4,f5(f5(a4,a4,a1),f5(a4,a1,a1),a1),a1))), % 70.10/70.15 inference(scs_inference,[],[6472,6474,6463,1178,1119,975,6482,1171,6489,5872,20,7,4,9,6,8,973,5,39,17,19,64,57,63,18,2,3,1042,23,1139])). % 70.10/70.15 cnf(6518,plain, % 70.10/70.15 (E(f5(a4,x65181,f5(f5(a4,a4,a1),f5(a4,a1,a1),a1)),x65181)), % 70.10/70.15 inference(scs_inference,[],[6512,23])). % 70.10/70.15 cnf(6520,plain, % 70.10/70.15 (P3(f5(a4,f5(f5(a4,f5(a4,a4,a1),a1),f5(a4,a1,a1),a1),a1))), % 70.10/70.15 inference(scs_inference,[],[6512,6515,23,1139])). % 70.10/70.15 cnf(6521,plain, % 70.10/70.15 (P3(f5(f5(f5(a4,a4,a1),a4,a1),a1,a1))), % 70.10/70.15 inference(scs_inference,[],[6512,6515,23,1139,1042])). % 70.10/70.15 cnf(6528,plain, % 70.10/70.15 (P3(f5(a4,f5(f5(a4,a4,a1),f5(a4,a1,a1),a1),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[6512,6515,3608,23,1139,1042,9,922,7,4,8,973])). % 70.10/70.15 cnf(6533,plain, % 70.10/70.15 (P3(f5(a4,a1,f5(a4,f5(a4,a1,a1),a1)))), % 70.10/70.15 inference(scs_inference,[],[6512,6515,1176,3608,23,1139,1042,9,922,7,4,8,973,6,5,17,19])). % 70.10/70.15 cnf(6537,plain, % 70.10/70.15 (P3(f5(a4,f5(a4,f5(a4,f5(a4,a1,a1),a1),f5(a4,a1,a1)),a1))), % 70.10/70.15 inference(scs_inference,[],[6512,6502,6497,6515,1176,3608,23,1139,1042,9,922,7,4,8,973,6,5,17,19,64,57])). % 70.10/70.15 cnf(6539,plain, % 70.10/70.15 (P4(f5(a4,f5(f5(a4,a4,a1),a1,a1),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[6512,6502,6497,6515,1176,3608,987,23,1139,1042,9,922,7,4,8,973,6,5,17,19,64,57,63,18])). % 70.10/70.15 cnf(6542,plain, % 70.10/70.15 (~E(f5(a4,a6,f5(a4,f5(a4,a1,a1),f5(a4,a1,a1))),f5(f5(a4,a4,a1),f5(a4,a2,a1),a1))), % 70.10/70.15 inference(scs_inference,[],[6512,6502,6497,6515,1176,107,3608,982,987,6014,23,1139,1042,9,922,7,4,8,973,6,5,17,19,64,57,63,18,2,3])). % 70.10/70.15 cnf(6543,plain, % 70.10/70.15 (E(x65431,f5(a4,x65431,f5(a4,f5(a4,a1,a1),f5(a4,a1,a1))))), % 70.10/70.15 inference(rename_variables,[],[6014])). % 70.10/70.15 cnf(6544,plain, % 70.10/70.15 (P1(f5(a4,f5(a4,f5(a4,a1,f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,f5(a4,a1,a1),f5(a4,a1,a1))))), % 70.10/70.15 inference(scs_inference,[],[6512,5859,6502,6497,6515,1176,107,3608,982,987,6014,6543,23,1139,1042,9,922,7,4,8,973,6,5,17,19,64,57,63,18,2,3,10])). % 70.10/70.15 cnf(6549,plain, % 70.10/70.15 (P3(f5(f5(a4,f5(a4,f5(a4,a4,a1),a1),a1),f5(a4,a1,a1),a1))), % 70.10/70.15 inference(scs_inference,[],[6528,6520,5875,23,9,1042])). % 70.10/70.15 cnf(6556,plain, % 70.10/70.15 (E(f5(x65561,f5(a4,f5(a4,a4,f5(a4,a1,a1)),f5(a4,a1,a1)),x65562),f5(x65561,a4,x65562))), % 70.10/70.15 inference(scs_inference,[],[6528,6520,5875,23,9,1042,922,7,4,6,5,8])). % 70.10/70.15 cnf(6557,plain, % 70.10/70.15 (P3(f5(a4,f5(a4,f5(f5(a4,a4,a1),f5(a4,a1,a1),a1),f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[6528,6520,5875,23,9,1042,922,7,4,6,5,8,973])). % 70.10/70.15 cnf(6560,plain, % 70.10/70.15 (P3(f5(a4,f5(a4,f5(a4,f5(a4,a1,a1),a1),a1),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[6528,1136,6520,5875,23,9,1042,922,7,4,6,5,8,973,17,19])). % 70.10/70.15 cnf(6564,plain, % 70.10/70.15 (P3(f5(a4,f5(a4,f5(f5(a4,a4,a1),f5(a4,a1,a1),a1),f5(a4,a1,a1)),a1))), % 70.10/70.15 inference(scs_inference,[],[6528,1136,6520,5875,23,9,1042,922,7,4,6,5,8,973,17,19,64,57])). % 70.10/70.15 cnf(6567,plain, % 70.10/70.15 (~E(f5(a4,f8(a7),f5(a4,a1,a1)),f5(a6,f5(f3(a6,a1),f8(a7),a1),a1))), % 70.10/70.15 inference(scs_inference,[],[6528,928,1136,6520,5875,23,9,1042,922,7,4,6,5,8,973,17,19,64,57,18,2])). % 70.10/70.15 cnf(6584,plain, % 70.10/70.15 (P3(f5(f5(a4,f5(a4,a4,a1),a1),f5(a4,a1,a1),a1))), % 70.10/70.15 inference(scs_inference,[],[6557,6515,3627,23,922,9,1042])). % 70.10/70.15 cnf(6586,plain, % 70.10/70.15 (E(f5(f5(a4,f5(a4,a4,f5(a4,a1,a1)),f5(a4,a1,a1)),x65861,x65862),f5(f5(a4,a4,a1),x65861,x65862))), % 70.10/70.15 inference(scs_inference,[],[6557,6515,3627,23,922,9,1042,4,7])). % 70.10/70.15 cnf(6587,plain, % 70.10/70.15 (P3(f5(a4,f5(a4,f5(a4,f5(f5(a4,a4,a1),f5(a4,a1,a1),a1),f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[6557,6515,3627,23,922,9,1042,4,7,973])). % 70.10/70.15 cnf(6591,plain, % 70.10/70.15 (P2(f5(a4,f5(a4,f5(f5(a4,a4,a1),f5(a4,a1,a1),a1),f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[6557,6515,3627,23,922,9,1042,4,7,973,6,8,5,17])). % 70.10/70.15 cnf(6593,plain, % 70.10/70.15 (P3(f5(a4,f5(a4,f5(a4,a1,a1),f5(a4,a1,a1)),f5(a4,f5(a4,a1,a1),f5(a4,a1,a1))))), % 70.10/70.15 inference(scs_inference,[],[6557,6448,6515,3627,23,922,9,1042,4,7,973,6,8,5,17,19])). % 70.10/70.15 cnf(6598,plain, % 70.10/70.15 (P4(f5(a4,f5(a4,f5(f5(a4,a4,a1),f5(a4,a1,a1),a1),f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[6557,6448,6515,3627,23,922,9,1042,4,7,973,6,8,5,17,19,64,57,18])). % 70.10/70.15 cnf(6600,plain, % 70.10/70.15 (~E(f5(f5(a4,a4,a1),f5(a4,a2,a1),a1),f5(a4,a6,f5(a4,f5(a4,a1,a1),f5(a4,a1,a1))))), % 70.10/70.15 inference(scs_inference,[],[6557,6542,6448,6515,3627,23,922,9,1042,4,7,973,6,8,5,17,19,64,57,18,2])). % 70.10/70.15 cnf(6601,plain, % 70.10/70.15 (~E(f5(f5(a4,a4,a1),f5(a4,a2,a1),a1),a6)), % 70.10/70.15 inference(scs_inference,[],[6557,6481,6542,6448,6515,3627,979,23,922,9,1042,4,7,973,6,8,5,17,19,64,57,18,2,3])). % 70.10/70.15 cnf(6607,plain, % 70.10/70.15 (P2(f5(f5(a4,f5(a4,a4,a1),a1),f5(a4,a1,a1),a1))), % 70.10/70.15 inference(scs_inference,[],[6584,23,922,17])). % 70.10/70.15 cnf(6610,plain, % 70.10/70.15 (E(f5(a4,x66101,x66102),f5(f5(a4,f5(a4,a4,f5(a4,a1,a1)),f5(a4,a1,a1)),x66101,x66102))), % 70.10/70.15 inference(scs_inference,[],[6584,5872,23,922,17,9,7])). % 70.10/70.15 cnf(6611,plain, % 70.10/70.15 (P3(f5(a4,f5(f5(a4,f5(a4,a4,a1),a1),f5(a4,a1,a1),a1),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[6584,5872,23,922,17,9,7,973])). % 70.10/70.15 cnf(6620,plain, % 70.10/70.15 (P3(f5(a4,f5(a4,f5(a4,f5(a4,a1,a1),f5(a4,a1,a1)),f5(a4,a1,a1)),a1))), % 70.10/70.15 inference(scs_inference,[],[6584,6544,6463,5872,23,922,17,9,7,973,5,4,6,8,19,64,57])). % 70.10/70.15 cnf(6633,plain, % 70.10/70.15 (P3(f5(a4,f5(a4,f5(f5(a4,f5(a4,a4,a1),a1),f5(a4,a1,a1),a1),f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[6611,3654,23,922,17,9,973])). % 70.10/70.15 cnf(6635,plain, % 70.10/70.15 (E(f5(f5(a4,a4,a1),x66351,x66352),f5(f5(a4,f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)),f5(a4,a1,a1)),x66351,x66352))), % 70.10/70.15 inference(scs_inference,[],[6611,3654,23,922,17,9,973,5,7])). % 70.10/70.15 cnf(6642,plain, % 70.10/70.15 (P4(f5(a4,f5(f5(a4,f5(a4,a4,a1),a1),f5(a4,a1,a1),a1),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[6611,3654,23,922,17,9,973,5,7,8,6,4,64,57,18])). % 70.10/70.15 cnf(6644,plain, % 70.10/70.15 (~E(f5(a4,a2,f5(a4,a1,a1)),a6)), % 70.10/70.15 inference(scs_inference,[],[6611,1046,3654,23,922,17,9,973,5,7,8,6,4,64,57,18,2])). % 70.10/70.15 cnf(6645,plain, % 70.10/70.15 (~E(f5(f5(a4,f5(a4,f5(a4,a4,a1),a1),f5(a4,a1,a1)),f5(a4,a2,a1),a1),a6)), % 70.10/70.15 inference(scs_inference,[],[6601,6611,1046,6462,3654,23,922,17,9,973,5,7,8,6,4,64,57,18,2,3])). % 70.10/70.15 cnf(6647,plain, % 70.10/70.15 (P1(f5(f5(a4,f5(a4,a4,f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,a1,f5(a4,a1,a1)),a1))), % 70.10/70.15 inference(scs_inference,[],[6601,6611,5873,6610,1046,6462,3654,23,922,17,9,973,5,7,8,6,4,64,57,18,2,3,10])). % 70.10/70.15 cnf(6653,plain, % 70.10/70.15 (P3(f5(a4,f5(f5(f5(a4,a4,a1),a4,a1),a1,a1),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[6521,3626,17,9,5,973])). % 70.10/70.15 cnf(6655,plain, % 70.10/70.15 (P3(f5(f5(a4,f5(a4,a4,f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,a1,f5(a4,a1,a1)),a1))), % 70.10/70.15 inference(scs_inference,[],[6521,6647,3626,17,9,5,973,7,19])). % 70.10/70.15 cnf(6660,plain, % 70.10/70.15 (P3(f5(a4,f5(a4,f5(f5(a4,a4,a1),a1,a1),f5(a4,a1,a1)),a1))), % 70.10/70.15 inference(scs_inference,[],[6521,6647,6497,3626,17,9,5,973,7,19,4,8,6,57])). % 70.10/70.15 cnf(6668,plain, % 70.10/70.15 (E(f5(a4,x66681,x66682),f5(f5(a4,f5(a4,a4,f5(a4,a1,a1)),f5(a4,a1,a1)),x66681,x66682))), % 70.10/70.15 inference(rename_variables,[],[6610])). % 70.10/70.15 cnf(6669,plain, % 70.10/70.15 (P3(f5(f5(a4,f5(a4,a4,f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,f5(a4,a1,a1),a1),a1))), % 70.10/70.15 inference(scs_inference,[],[6508,6645,6506,6521,6518,6556,6647,6610,6668,6497,3626,17,9,5,973,7,19,4,8,6,57,18,2,3,13,12])). % 70.10/70.15 cnf(6674,plain, % 70.10/70.15 (P3(f5(f5(f5(a4,f5(a4,a4,f5(a4,a1,a1)),f5(a4,a1,a1)),a4,a1),f5(a4,a1,a1),a1))), % 70.10/70.15 inference(scs_inference,[],[6669,1042])). % 70.10/70.15 cnf(6684,plain, % 70.10/70.15 (P3(f5(a4,f5(a4,f5(a4,a1,f5(a4,a1,a1)),f5(a4,a1,a1)),a1))), % 70.10/70.15 inference(scs_inference,[],[6533,6669,3655,1004,1042,17,9,5,973,7,4,8,6,57])). % 70.10/70.15 cnf(6687,plain, % 70.10/70.15 (~E(f5(a4,f5(a4,a2,a1),f5(a4,a1,a1)),a6)), % 70.10/70.15 inference(scs_inference,[],[6533,6669,1115,3655,1004,1042,17,9,5,973,7,4,8,6,57,18,2])). % 70.10/70.15 cnf(6688,plain, % 70.10/70.15 (~E(f5(f5(a4,f5(a4,a4,f5(a4,a1,a1)),f5(a4,a1,a1)),a2,f5(a4,a1,a1)),a6)), % 70.10/70.15 inference(scs_inference,[],[6644,6533,6669,1115,6610,3655,1004,1042,17,9,5,973,7,4,8,6,57,18,2,3])). % 70.10/70.15 cnf(6694,plain, % 70.10/70.15 (P3(f5(a4,f5(a4,f5(a4,f5(a4,a1,a1),f5(a4,a1,a1)),a1),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[6477,6560,3600,17,9,5,973])). % 70.10/70.15 cnf(6695,plain, % 70.10/70.15 (E(f5(f5(a4,a4,a1),x66951,x66952),f5(f5(a4,a4,f5(a4,a1,a1)),x66951,x66952))), % 70.10/70.15 inference(scs_inference,[],[6477,6560,3600,17,9,5,973,7])). % 70.10/70.15 cnf(6702,plain, % 70.10/70.15 (~E(f5(a4,f5(f5(a4,a4,f5(a4,a1,a1)),a2,f5(a4,a1,a1)),f5(a4,a1,a1)),a6)), % 70.10/70.15 inference(scs_inference,[],[6688,6477,6429,6560,6549,3600,17,9,5,973,7,4,6,8,18,2,3])). % 70.10/70.15 cnf(6708,plain, % 70.10/70.15 (P3(f5(a4,f5(a4,f5(f5(a4,a4,a1),a1,a1),a1),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[6486,6653,5909,17,9,5,973])). % 70.10/70.15 cnf(6716,plain, % 70.10/70.15 (~E(f5(f5(a4,f5(a4,a4,f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,a2,a1),f5(a4,a1,a1)),a6)), % 70.10/70.15 inference(scs_inference,[],[6687,6702,6486,6653,6610,5909,17,9,5,973,7,4,6,8,18,2,3])). % 70.10/70.15 cnf(6720,plain, % 70.10/70.15 (P3(f5(f5(a4,a4,f5(a4,a1,a1)),a1,a1))), % 70.10/70.15 inference(scs_inference,[],[6687,6702,6486,6653,6695,1020,6610,5909,17,9,5,973,7,4,6,8,18,2,3,10,19])). % 70.10/70.15 cnf(6726,plain, % 70.10/70.15 (P3(f5(a4,f5(f5(a4,a4,f5(a4,a1,a1)),a1,a1),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[6720,5908,17,9,5,973])). % 70.10/70.15 cnf(6737,plain, % 70.10/70.15 (P3(f5(f5(a4,a4,a1),f5(a4,a1,f5(a4,a1,a1)),a1))), % 70.10/70.15 inference(scs_inference,[],[6539,6716,6720,6511,6586,6655,1874,5908,6610,17,9,5,973,7,4,6,8,18,2,3,13,12])). % 70.10/70.15 cnf(6744,plain, % 70.10/70.15 (E(f3(x67441,a4),f3(x67441,f5(a4,f5(a4,a4,a1),f5(a4,a1,a1))))), % 70.10/70.15 inference(scs_inference,[],[6737,3633,17,9,5])). % 70.10/70.15 cnf(6745,plain, % 70.10/70.15 (E(f5(a4,x67451,x67452),f5(f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)),x67451,x67452))), % 70.10/70.15 inference(scs_inference,[],[6737,3633,17,9,5,7])). % 70.10/70.15 cnf(6746,plain, % 70.10/70.15 (P3(f5(a4,f5(f5(a4,a4,a1),f5(a4,a1,f5(a4,a1,a1)),a1),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[6737,3633,17,9,5,7,973])). % 70.10/70.15 cnf(6747,plain, % 70.10/70.15 (E(f3(a4,x67471),f3(f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)),x67471))), % 70.10/70.15 inference(scs_inference,[],[6737,3633,17,9,5,7,973,4])). % 70.10/70.15 cnf(6752,plain, % 70.10/70.15 (~E(f5(a4,f5(a4,f5(a4,a2,a1),a1),f5(a4,a1,a1)),a6)), % 70.10/70.15 inference(scs_inference,[],[6737,1132,3633,17,9,5,7,973,4,6,8,18,2])). % 70.10/70.15 cnf(6773,plain, % 70.10/70.15 (E(f3(x67731,f5(a4,f5(a4,a4,a1),a1)),f3(x67731,a4))), % 70.10/70.15 inference(scs_inference,[],[6694,496,17,9,5])). % 70.10/70.15 cnf(6774,plain, % 70.10/70.15 (E(f5(f5(a4,f5(a4,a4,a1),a1),x67741,x67742),f5(a4,x67741,x67742))), % 70.10/70.15 inference(scs_inference,[],[6694,496,17,9,5,7])). % 70.10/70.15 cnf(6776,plain, % 70.10/70.15 (E(f3(f5(a4,f5(a4,a4,a1),a1),x67761),f3(a4,x67761))), % 70.10/70.15 inference(scs_inference,[],[6694,496,17,9,5,7,973,4])). % 70.10/70.15 cnf(6783,plain, % 70.10/70.15 (E(f5(a4,x67831,x67832),f5(f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)),x67831,x67832))), % 70.10/70.15 inference(rename_variables,[],[6745])). % 70.10/70.15 cnf(6784,plain, % 70.10/70.15 (P1(f5(f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)),a1,f5(a4,f5(a4,a1,a1),f5(a4,a1,a1))))), % 70.10/70.15 inference(scs_inference,[],[6752,6157,6694,6745,6783,37,496,17,9,5,7,973,4,6,8,18,2,3,10])). % 70.10/70.15 cnf(6786,plain, % 70.10/70.15 (P3(f5(f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)),a1,f5(a4,f5(a4,a1,a1),f5(a4,a1,a1))))), % 70.10/70.15 inference(scs_inference,[],[6784,19])). % 70.10/70.15 cnf(6792,plain, % 70.10/70.15 (E(f5(a4,x67921,x67922),f5(f5(a4,f5(a4,a4,a1),a1),x67921,x67922))), % 70.10/70.15 inference(scs_inference,[],[6708,6784,495,19,17,9,5,7])). % 70.10/70.15 cnf(6812,plain, % 70.10/70.15 (E(f3(x68121,f5(a4,f5(a4,a4,a1),f5(a4,a1,a1))),f3(x68121,a4))), % 70.10/70.15 inference(scs_inference,[],[6726,3634,17,9,5])). % 70.10/70.15 cnf(6816,plain, % 70.10/70.15 (E(f3(f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)),x68161),f3(a4,x68161))), % 70.10/70.15 inference(scs_inference,[],[6726,3634,17,9,5,7,6,973,4])). % 70.10/70.15 cnf(6821,plain, % 70.10/70.15 (~E(f5(f5(a4,f5(a4,a4,a1),a1),f8(a7),f5(a4,a1,a1)),f5(a6,f5(f3(a6,a1),f8(a7),a1),a1))), % 70.10/70.15 inference(scs_inference,[],[6792,6726,6567,1140,3634,17,9,5,7,6,973,4,8,18,2,3])). % 70.10/70.15 cnf(6827,plain, % 70.10/70.15 (E(f5(a4,x68271,x68272),f5(f5(a4,f5(a4,f5(a4,f5(a4,a4,a1),a1),f5(a4,a1,a1)),f5(a4,a1,a1)),x68271,x68272))), % 70.10/70.15 inference(scs_inference,[],[6633,2011,17,9,5,7])). % 70.10/70.15 cnf(6834,plain, % 70.10/70.15 (~E(f5(a6,f5(f3(a6,a1),f8(a7),a1),a1),f5(f5(a4,f5(a4,a4,a1),a1),f8(a7),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[6633,6821,2011,17,9,5,7,6,973,8,4,18,2])). % 70.10/70.15 cnf(6843,plain, % 70.10/70.15 (E(f5(f5(a4,a4,a1),x68431,x68432),f5(f5(a4,f5(a6,f3(a6,a1),a1),f5(a4,a1,a1)),x68431,x68432))), % 70.10/70.15 inference(scs_inference,[],[6587,1419,17,9,5,6,7])). % 70.10/70.15 cnf(6849,plain, % 70.10/70.15 (~E(f5(a4,f5(a4,f5(a4,a2,a1),a1),a1),a6)), % 70.10/70.15 inference(scs_inference,[],[6587,202,1419,17,9,5,6,7,4,973,8,18,2])). % 70.10/70.15 cnf(6850,plain, % 70.10/70.15 (~E(f5(f5(a6,f3(a6,a1),a1),f8(a7),a1),f5(f5(a4,f5(a4,a4,a1),a1),f8(a7),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[6587,6834,202,981,1419,17,9,5,6,7,4,973,8,18,2,3])). % 70.10/70.15 cnf(6852,plain, % 70.10/70.15 (P1(f5(f5(a4,f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,a1,a1),a1))), % 70.10/70.15 inference(scs_inference,[],[6587,6834,6635,998,202,981,1419,17,9,5,6,7,4,973,8,18,2,3,10])). % 70.10/70.15 cnf(6854,plain, % 70.10/70.15 (P3(f5(f5(a4,f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,a1,a1),a1))), % 70.10/70.15 inference(scs_inference,[],[6587,6834,6635,998,202,981,1419,17,9,5,6,7,4,973,8,18,2,3,10,19])). % 70.10/70.15 cnf(6858,plain, % 70.10/70.15 (P3(f5(a4,f5(f5(a4,f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,a1,a1),a1),a1))), % 70.10/70.15 inference(scs_inference,[],[6587,6834,6635,998,202,981,1419,17,9,5,6,7,4,973,8,18,2,3,10,19,64,57])). % 70.10/70.15 cnf(6863,plain, % 70.10/70.15 (P3(f5(f5(a4,f5(a4,f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)),f5(a4,a1,a1)),a1),f5(a4,a1,a1),a1))), % 70.10/70.15 inference(scs_inference,[],[6854,6858,23,922,1042])). % 70.10/70.15 cnf(6872,plain, % 70.10/70.15 (P3(f5(a4,f5(f5(a4,f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,a1,a1),a1),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[6854,6858,1417,23,922,1042,17,9,5,4,8,6,7,973])). % 70.10/70.15 cnf(6875,plain, % 70.10/70.15 (~E(f5(f5(a4,f5(a4,a4,a1),a1),f8(a7),f5(a4,a1,a1)),f5(f5(a6,f3(a6,a1),a1),f8(a7),a1))), % 70.10/70.15 inference(scs_inference,[],[6854,6850,6858,1417,23,922,1042,17,9,5,4,8,6,7,973,18,2])). % 70.10/70.15 cnf(6896,plain, % 70.10/70.15 (~E(f5(a4,a2,a1),a6)), % 70.10/70.15 inference(scs_inference,[],[6872,48,1189,17,9,5,8,4,7,6,973,18,2])). % 70.10/70.15 cnf(6897,plain, % 70.10/70.15 (~E(f5(f5(a4,f5(a4,a4,a1),a1),f5(a4,f5(a4,a2,a1),a1),a1),a6)), % 70.10/70.15 inference(scs_inference,[],[6849,6872,6792,48,1189,17,9,5,8,4,7,6,973,18,2,3])). % 70.10/70.15 cnf(6905,plain, % 70.10/70.15 (E(f5(a4,x69051,x69052),f5(f5(a4,f5(a4,f5(a6,f3(a6,a1),a1),f5(a4,a1,a1)),f5(a4,a1,a1)),x69051,x69052))), % 70.10/70.15 inference(scs_inference,[],[6746,1716,17,9,5,973,8,7])). % 70.10/70.15 cnf(6911,plain, % 70.10/70.15 (E(f3(f5(a4,f5(a4,a4,a1),a1),f5(a4,f5(a4,a4,a1),a1)),f3(a4,a4))), % 70.10/70.15 inference(scs_inference,[],[6773,6776,6746,6897,1716,17,9,5,973,8,7,6,4,18,2,3])). % 70.10/70.15 cnf(6919,plain, % 70.10/70.15 (P3(f5(a4,f5(a4,f5(a4,f5(a4,a1,f5(a4,a1,a1)),f5(a4,a1,a1)),a1),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[6684,6786,1571,17,9,5,6,973])). % 70.10/70.15 cnf(6921,plain, % 70.10/70.15 (E(f5(a4,x69211,x69212),f5(f5(a4,f5(a4,f5(a4,a4,a1),a1),f5(a4,a1,a1)),x69211,x69212))), % 70.10/70.15 inference(scs_inference,[],[6684,6786,1571,17,9,5,6,973,8,7])). % 70.10/70.15 cnf(6925,plain, % 70.10/70.15 (~E(f5(a4,f5(a4,a2,a1),a1),a6)), % 70.10/70.15 inference(scs_inference,[],[6684,6786,185,1571,17,9,5,6,973,8,7,4,18,2])). % 70.10/70.15 cnf(6926,plain, % 70.10/70.15 (~E(f5(f5(a4,f5(a4,f5(a6,f3(a6,a1),a1),f5(a4,a1,a1)),f5(a4,a1,a1)),a2,a1),a6)), % 70.10/70.15 inference(scs_inference,[],[6896,6684,6786,6905,185,1571,17,9,5,6,973,8,7,4,18,2,3])). % 70.10/70.15 cnf(6927,plain, % 70.10/70.15 (E(f5(a4,x69271,x69272),f5(f5(a4,f5(a4,f5(a6,f3(a6,a1),a1),f5(a4,a1,a1)),f5(a4,a1,a1)),x69271,x69272))), % 70.10/70.15 inference(rename_variables,[],[6905])). % 70.10/70.15 cnf(6928,plain, % 70.10/70.15 (P1(f5(f5(a4,f5(a4,f5(a6,f3(a6,a1),a1),f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,a1,f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[6896,6684,6786,6905,6927,5859,185,1571,17,9,5,6,973,8,7,4,18,2,3,10])). % 70.10/70.15 cnf(6931,plain, % 70.10/70.15 (P3(f5(f5(a4,f5(a4,f5(a6,f3(a6,a1),a1),f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,a1,f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[6928,19])). % 70.10/70.15 cnf(6933,plain, % 70.10/70.15 (P2(f5(f5(f5(a4,f5(a4,a4,f5(a4,a1,a1)),f5(a4,a1,a1)),a4,a1),f5(a4,a1,a1),a1))), % 70.10/70.15 inference(scs_inference,[],[6928,6674,19,17])). % 70.10/70.15 cnf(6942,plain, % 70.10/70.15 (P4(f5(f5(f5(a4,f5(a4,a4,f5(a4,a1,a1)),f5(a4,a1,a1)),a4,a1),f5(a4,a1,a1),a1))), % 70.10/70.15 inference(scs_inference,[],[6620,6928,6674,1636,19,17,9,5,6,7,973,8,4,18])). % 70.10/70.15 cnf(6949,plain, % 70.10/70.15 (E(f5(a4,x69491,x69492),f5(f5(a4,f5(a4,f5(a4,a4,a1),a1),f5(a4,a1,a1)),x69491,x69492))), % 70.10/70.15 inference(rename_variables,[],[6921])). % 70.10/70.15 cnf(6952,plain, % 70.10/70.15 (P3(f5(f5(a4,f5(a6,f3(a6,a1),a1),f5(a4,a1,a1)),a1,a1))), % 70.10/70.15 inference(scs_inference,[],[6812,6816,6642,6591,6620,6921,6949,6928,6674,6843,6926,6472,1636,19,17,9,5,6,7,973,8,4,18,2,3,13,11,12])). % 70.10/70.15 cnf(6966,plain, % 70.10/70.15 (~E(f5(a4,f8(a7),f5(a4,a1,a1)),f5(f5(a6,f3(a6,a1),a1),f8(a7),a1))), % 70.10/70.15 inference(scs_inference,[],[6875,6660,6952,6774,2005,16,17,9,5,973,6,7,8,4,18,2,3])). % 70.10/70.15 cnf(6979,plain, % 70.10/70.15 (~E(f5(f5(a6,f3(a6,a1),a1),f8(a7),a1),f5(a4,f8(a7),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[6966,6593,6931,1565,17,9,5,6,973,8,7,4,18,2])). % 70.10/70.15 cnf(6995,plain, % 70.10/70.15 (~E(f5(f5(a4,a4,f5(a4,a1,a1)),f5(a4,a2,a1),a1),f5(a4,a6,f5(a4,f5(a4,a1,a1),f5(a4,a1,a1))))), % 70.10/70.15 inference(scs_inference,[],[6537,6600,6863,6695,97,1193,15,17,9,7,973,5,6,8,4,18,2,3])). % 70.10/70.15 cnf(6997,plain, % 70.10/70.15 (P1(f5(f5(a4,f5(a4,f5(a4,a4,a1),a1),f5(a4,a1,a1)),f5(a4,f5(a4,a1,a1),a1),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[6537,6600,6863,1119,6695,6921,97,1193,15,17,9,7,973,5,6,8,4,18,2,3,10])). % 70.10/70.15 cnf(7007,plain, % 70.10/70.15 (E(f5(f5(a6,f3(a6,a1),a1),x70071,x70072),f5(f5(a4,a4,a1),x70071,x70072))), % 70.10/70.15 inference(scs_inference,[],[6997,6564,6428,355,19,17,9,5,6,973,7])). % 70.10/70.15 cnf(7017,plain, % 70.10/70.15 (E(f5(f5(x70171,x70172,a1),x70173,a1),f5(x70171,f5(x70172,x70173,a1),a1))), % 70.10/70.15 inference(rename_variables,[],[979])). % 70.10/70.15 cnf(7020,plain, % 70.10/70.15 (P3(f5(f5(a4,f5(a4,f5(a4,f5(a4,a4,a1),a1),f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,a1,a1),a1))), % 70.10/70.15 inference(scs_inference,[],[6744,6747,6997,6564,6933,6942,6428,6995,6474,6827,979,7017,355,19,17,9,5,6,973,7,8,4,18,2,3,13,11,12])). % 70.10/70.15 cnf(7038,plain, % 70.10/70.15 (E(f5(x70381,x70382,x70383),f5(x70381,x70382,f5(a4,x70383,a1)))), % 70.10/70.15 inference(scs_inference,[],[7020,26,17,9])). % 70.10/70.15 cnf(7041,plain, % 70.10/70.15 (E(f5(x70411,x70412,x70413),f5(f5(a4,x70411,a1),x70412,x70413))), % 70.10/70.15 inference(scs_inference,[],[7020,26,339,17,9,6,973,7])). % 70.10/70.15 cnf(7042,plain, % 70.10/70.15 (E(f3(x70421,x70422),f3(x70421,f5(a4,x70422,a1)))), % 70.10/70.15 inference(scs_inference,[],[7020,26,339,17,9,6,973,7,5])). % 70.10/70.15 cnf(7043,plain, % 70.10/70.15 (E(f5(x70431,x70432,x70433),f5(x70431,f5(a4,x70432,a1),x70433))), % 70.10/70.15 inference(scs_inference,[],[7020,26,339,17,9,6,973,7,5,8])). % 70.10/70.15 cnf(7044,plain, % 70.10/70.15 (E(f3(x70441,x70442),f3(f5(a4,x70441,a1),x70442))), % 70.10/70.15 inference(scs_inference,[],[7020,26,339,17,9,6,973,7,5,8,4])). % 70.10/70.15 cnf(7054,plain, % 70.10/70.15 (P3(f5(a4,f5(a4,f5(a4,f5(a4,a1,a1),a1),f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[7038,6919,6502,17,9,6,973])). % 70.10/70.15 cnf(7056,plain, % 70.10/70.15 (E(f5(f5(x70561,x70562,x70563),x70564,x70565),f5(f5(x70561,x70562,f5(a4,x70563,a1)),x70564,x70565))), % 70.10/70.15 inference(scs_inference,[],[7038,6919,6502,17,9,6,973,5,7])). % 70.10/70.15 cnf(7057,plain, % 70.10/70.15 (E(f5(x70571,f5(x70572,x70573,x70574),x70575),f5(x70571,f5(x70572,x70573,f5(a4,x70574,a1)),x70575))), % 70.10/70.15 inference(scs_inference,[],[7038,6919,6502,17,9,6,973,5,7,8])). % 70.10/70.15 cnf(7061,plain, % 70.10/70.15 (~E(f5(f5(a6,f3(a6,a1),a1),f8(a7),f5(a4,a1,a1)),f5(a4,f8(a7),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[7038,6979,6919,6502,17,9,6,973,5,7,8,4,18,3])). % 70.10/70.15 cnf(7062,plain, % 70.10/70.15 (E(f5(x70621,x70622,x70623),f5(x70621,x70622,f5(a4,x70623,a1)))), % 70.10/70.15 inference(rename_variables,[],[7038])). % 70.10/70.15 cnf(7071,plain, % 70.10/70.15 (P1(f5(f5(a4,f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,a1,a1),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[7038,7062,6979,6852,6919,6502,17,9,6,973,5,7,8,4,18,3,23,922,64,57,2,10])). % 70.10/70.15 cnf(7073,plain, % 70.10/70.15 (P3(f5(f5(a4,f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,a1,a1),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[7071,19])). % 70.10/70.15 cnf(7082,plain, % 70.10/70.15 (P3(f5(a4,f5(a4,f5(a4,f5(a4,f5(a4,a1,a1),a1),f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[7041,7071,7054,19,64,17,57,9,6,973])). % 70.10/70.15 cnf(7089,plain, % 70.10/70.15 (E(f3(x70891,x70892),f3(f5(a4,x70891,a1),f5(a4,x70892,a1)))), % 70.10/70.15 inference(scs_inference,[],[7041,7042,7044,7071,7054,19,64,17,57,9,6,973,5,7,8,4,18,3])). % 70.10/70.15 cnf(7096,plain, % 70.10/70.15 (P4(f5(f5(a4,a4,a1),f5(a4,f5(f5(a4,a4,a1),f5(a4,a1,a1),a1),f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[7041,7042,7044,7071,6598,7054,19,64,17,57,9,6,973,5,7,8,4,18,3,23,922,13])). % 70.10/70.15 cnf(7097,plain, % 70.10/70.15 (E(f5(x70971,x70972,x70973),f5(f5(a4,x70971,a1),x70972,x70973))), % 70.10/70.15 inference(rename_variables,[],[7041])). % 70.10/70.15 cnf(7099,plain, % 70.10/70.15 (E(f5(x70991,x70992,x70993),f5(f5(a4,x70991,a1),x70992,x70993))), % 70.10/70.15 inference(rename_variables,[],[7041])). % 70.10/70.15 cnf(7100,plain, % 70.10/70.15 (P3(f5(f5(a4,a4,a1),f5(a4,f5(a4,f5(a4,a1,a1),a1),f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[7041,7097,7099,7042,7044,6607,7071,6598,7054,19,64,17,57,9,6,973,5,7,8,4,18,3,23,922,13,11,12])). % 70.10/70.15 cnf(7116,plain, % 70.10/70.15 (P3(f5(a4,f5(f5(a4,f5(a4,f5(a4,a4,a1),f5(a4,a1,a1)),f5(a4,a1,a1)),f5(a4,a1,a1),f5(a4,a1,a1)),f5(a4,a1,a1)))), % 70.10/70.15 inference(scs_inference,[],[7043,7073,7100,7096,23,922,64,17,57,63,9,6,5,7,973])). % 70.10/70.15 cnf(7135,plain, % 70.10/70.15 (E(f3(f5(a4,a4,a1),f5(a4,a4,a1)),f3(a4,a4))), % 70.10/70.15 inference(scs_inference,[],[7089,6911,7116,17,9,6,5,7,973,8,4,18,3])). % 70.10/70.15 cnf(7151,plain, % 70.10/70.15 (P1(f5(f5(f5(a4,a4,a1),a4,f5(a4,a1,a1)),a1,a1))), % 70.10/70.15 inference(scs_inference,[],[7135,6925,1009,7082,7056,7057,17,9,6,5,7,973,8,4,18,3,2,10])). % 70.10/70.15 cnf(7153,plain, % 70.10/70.15 (P3(f5(f5(f5(a4,a4,a1),a4,f5(a4,a1,a1)),a1,a1))), % 70.10/70.15 inference(scs_inference,[],[7151,19])). % 70.10/70.15 cnf(7189,plain, % 70.10/70.15 ($false), % 70.10/70.15 inference(scs_inference,[],[7061,7153,7007,7044,7041,17,9,6,5,973,7,4,8,18,3,2]), % 70.10/70.15 ['proof']). % 70.10/70.15 % SZS output end Proof % 70.10/70.15 % Total time :69.450000s %------------------------------------------------------------------------------