%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET825-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 : n027.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 14:22:35 EDT 2024 % Result : Unsatisfiable 124.36s 125.13s % Output : CNFRefutation 124.50s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SET825-2 : TPTP v8.2.0. Released v3.2.0. % 0.00/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n027.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Sun Jun 23 13:26:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.18/0.56 start to proof:theBenchmark % 124.36/125.12 %------------------------------------------- % 124.36/125.12 % File :CSE---1.7 % 124.36/125.12 % Problem :theBenchmark % 124.36/125.12 % Transform :cnf % 124.36/125.12 % Format :tptp:raw % 124.36/125.12 % Command :java -jar mcs_scs.jar %d %s % 124.36/125.12 % 124.36/125.12 % Result :Theorem 123.810000s % 124.36/125.12 % Output :CNFRefutation 123.810000s % 124.36/125.12 %------------------------------------------- % 124.36/125.13 %------------------------------------------------------------------------------ % 124.36/125.13 % File : SET825-2 : TPTP v8.2.0. Released v3.2.0. % 124.36/125.13 % Domain : Set Theory % 124.36/125.13 % Problem : Problem about set theory % 124.36/125.13 % Version : [Pau06] axioms : Reduced > Especial. % 124.36/125.13 % English : % 124.36/125.13 % 124.36/125.13 % Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe % 124.36/125.13 % Source : [Pau06] % 124.36/125.13 % Names : % 124.36/125.13 % 124.36/125.13 % Status : Unsatisfiable % 124.36/125.13 % Rating : 0.10 v8.1.0, 0.00 v7.5.0, 0.05 v7.4.0, 0.06 v7.3.0, 0.08 v7.1.0, 0.00 v7.0.0, 0.13 v6.4.0, 0.07 v6.3.0, 0.09 v6.2.0, 0.10 v6.1.0, 0.14 v6.0.0, 0.10 v5.5.0, 0.05 v5.4.0, 0.10 v5.3.0, 0.17 v5.2.0, 0.12 v5.0.0, 0.07 v4.1.0, 0.08 v4.0.1, 0.09 v4.0.0, 0.00 v3.4.0, 0.08 v3.3.0, 0.21 v3.2.0 % 124.36/125.13 % Syntax : Number of clauses : 6 ( 3 unt; 1 nHn; 5 RR) % 124.36/125.13 % Number of literals : 11 ( 1 equ; 5 neg) % 124.36/125.13 % Maximal clause size : 3 ( 1 avg) % 124.36/125.13 % Maximal term depth : 4 ( 1 avg) % 124.36/125.13 % Number of predicates : 3 ( 2 usr; 0 prp; 1-3 aty) % 124.36/125.13 % Number of functors : 10 ( 10 usr; 5 con; 0-4 aty) % 124.36/125.13 % Number of variables : 7 ( 0 sgn) % 124.36/125.13 % SPC : CNF_UNS_RFO_SEQ_NHN % 124.36/125.13 % 124.36/125.13 % Comments : The problems in the [Pau06] collection each have very many axioms, % 124.36/125.13 % of which only a small selection are required for the refutation. % 124.36/125.13 % The mission is to find those few axioms, after which a refutation % 124.36/125.13 % can be quite easily found. This version has only the necessary % 124.36/125.13 % axioms. % 124.36/125.13 %------------------------------------------------------------------------------ % 124.36/125.13 cnf(cls_Relation_OIdI_0,axiom, % 124.36/125.13 c_in(c_Pair(V_a,V_a,T_a,T_a),c_Relation_OId,tc_prod(T_a,T_a)) ). % 124.36/125.13 % 124.36/125.13 cnf(cls_Relation_Opair__in__Id__conv__iff1_0,axiom, % 124.36/125.13 ( ~ c_in(c_Pair(V_a,V_b,T_a,T_a),c_Relation_OId,tc_prod(T_a,T_a)) % 124.36/125.13 | V_a = V_b ) ). % 124.36/125.13 % 124.36/125.13 cnf(cls_conjecture_0,negated_conjecture, % 124.36/125.13 v_Q(v_n) ). % 124.36/125.13 % 124.36/125.13 cnf(cls_conjecture_1,negated_conjecture, % 124.36/125.13 ~ v_Q(v_m) ). % 124.36/125.13 % 124.36/125.13 cnf(cls_conjecture_2,negated_conjecture, % 124.36/125.13 ( c_in(c_Pair(v_n,v_m,tc_nat,tc_nat),V_U,tc_prod(tc_nat,tc_nat)) % 124.36/125.13 | c_in(c_Pair(v_x(V_U),v_xa(V_U),tc_nat,tc_nat),V_U,tc_prod(tc_nat,tc_nat)) % 124.36/125.13 | ~ c_in(c_Pair(c_0,c_0,tc_nat,tc_nat),V_U,tc_prod(tc_nat,tc_nat)) ) ). % 124.36/125.13 % 124.36/125.13 cnf(cls_conjecture_3,negated_conjecture, % 124.36/125.13 ( c_in(c_Pair(v_n,v_m,tc_nat,tc_nat),V_U,tc_prod(tc_nat,tc_nat)) % 124.36/125.13 | ~ c_in(c_Pair(c_Suc(v_x(V_U)),c_Suc(v_xa(V_U)),tc_nat,tc_nat),V_U,tc_prod(tc_nat,tc_nat)) % 124.36/125.13 | ~ c_in(c_Pair(c_0,c_0,tc_nat,tc_nat),V_U,tc_prod(tc_nat,tc_nat)) ) ). % 124.36/125.13 % 124.36/125.13 %------------------------------------------------------------------------------ % 124.36/125.13 %------------------------------------------- % 124.36/125.13 % Proof found % 124.36/125.13 % SZS status Theorem for theBenchmark % 124.36/125.13 % SZS output start Proof % 124.36/125.14 %ClaNum:22(EqnAxiom:16) % 124.36/125.14 %VarNum:24(SingletonVarNum:7) % 124.36/125.14 %MaxLitNum:3 % 124.36/125.14 %MaxfuncDepth:3 % 124.36/125.14 %SharedTerms:10 % 124.36/125.14 %goalClause: 17 19 21 22 % 124.36/125.14 %singleGoalClaCount:2 % 124.36/125.14 [17]P1(a1) % 124.36/125.14 [19]~P1(a8) % 124.36/125.14 [18]P2(f2(x181,x181,x182,x182),a4,f5(x182,x182)) % 124.36/125.14 [20]E(x201,x202)+~P2(f2(x201,x202,x203,x203),a4,f5(x203,x203)) % 124.36/125.14 [21]~P2(f2(a3,a3,a6,a6),x211,f5(a6,a6))+P2(f2(a1,a8,a6,a6),x211,f5(a6,a6))+P2(f2(f9(x211),f10(x211),a6,a6),x211,f5(a6,a6)) % 124.36/125.14 [22]~P2(f2(a3,a3,a6,a6),x221,f5(a6,a6))+P2(f2(a1,a8,a6,a6),x221,f5(a6,a6))+~P2(f2(f7(f9(x221)),f7(f10(x221)),a6,a6),x221,f5(a6,a6)) % 124.36/125.14 %EqnAxiom % 124.36/125.14 [1]E(x11,x11) % 124.36/125.14 [2]E(x22,x21)+~E(x21,x22) % 124.36/125.14 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 124.36/125.14 [4]~E(x41,x42)+E(f2(x41,x43,x44,x45),f2(x42,x43,x44,x45)) % 124.36/125.14 [5]~E(x51,x52)+E(f2(x53,x51,x54,x55),f2(x53,x52,x54,x55)) % 124.36/125.14 [6]~E(x61,x62)+E(f2(x63,x64,x61,x65),f2(x63,x64,x62,x65)) % 124.36/125.14 [7]~E(x71,x72)+E(f2(x73,x74,x75,x71),f2(x73,x74,x75,x72)) % 124.36/125.14 [8]~E(x81,x82)+E(f5(x81,x83),f5(x82,x83)) % 124.36/125.14 [9]~E(x91,x92)+E(f5(x93,x91),f5(x93,x92)) % 124.36/125.14 [10]~E(x101,x102)+E(f9(x101),f9(x102)) % 124.36/125.14 [11]~E(x111,x112)+E(f7(x111),f7(x112)) % 124.36/125.14 [12]~E(x121,x122)+E(f10(x121),f10(x122)) % 124.36/125.14 [13]~P1(x131)+P1(x132)+~E(x131,x132) % 124.36/125.14 [14]P2(x142,x143,x144)+~E(x141,x142)+~P2(x141,x143,x144) % 124.36/125.14 [15]P2(x153,x152,x154)+~E(x151,x152)+~P2(x153,x151,x154) % 124.36/125.14 [16]P2(x163,x164,x162)+~E(x161,x162)+~P2(x163,x164,x161) % 124.36/125.14 % 124.36/125.14 %------------------------------------------- % 124.44/125.15 cnf(23,plain, % 124.44/125.15 (P2(x231,a4,f5(x232,x232))+~E(f2(x233,x233,x232,x232),x231)), % 124.44/125.15 inference(scs_inference,[],[18,14])). % 124.44/125.15 cnf(24,plain, % 124.44/125.15 (E(x241,x242)+~E(f2(x243,x243,x244,x244),f2(x241,x242,x244,x244))), % 124.44/125.15 inference(scs_inference,[],[18,14,20])). % 124.44/125.15 cnf(26,plain, % 124.44/125.15 (E(x261,x262)+~E(f2(x263,x263,x264,x264),f2(x262,x261,x264,x264))), % 124.44/125.15 inference(scs_inference,[],[18,14,20,2])). % 124.44/125.15 cnf(34,plain, % 124.44/125.15 (P2(f2(x341,x341,x342,x342),a4,x343)+~E(f5(x342,x342),x343)), % 124.44/125.15 inference(scs_inference,[],[18,16])). % 124.44/125.15 cnf(40,plain, % 124.44/125.15 (~E(f2(x401,x401,x402,x402),f2(x403,x404,x402,x402))+E(f9(x403),f9(x404))), % 124.44/125.15 inference(scs_inference,[],[10,24])). % 124.44/125.15 cnf(42,plain, % 124.44/125.15 (~E(f2(x421,x421,x422,x422),f2(x423,x424,x422,x422))+E(f7(x424),f7(x423))), % 124.44/125.15 inference(scs_inference,[],[11,26])). % 124.44/125.15 cnf(52,plain, % 124.44/125.15 (~E(x521,x522)+E(f2(x523,f2(x521,x524,x525,x526),x527,x528),f2(x523,f2(x522,x524,x525,x526),x527,x528))), % 124.44/125.15 inference(scs_inference,[],[5,4])). % 124.44/125.15 cnf(63,plain, % 124.44/125.15 (~E(a8,a1)), % 124.44/125.15 inference(scs_inference,[],[17,19,13,2])). % 124.44/125.15 cnf(64,plain, % 124.44/125.15 (~E(f2(x641,x641,x642,x642),f2(x643,a1,x642,x642))+~E(a8,x643)), % 124.44/125.15 inference(scs_inference,[],[63,3,24])). % 124.44/125.15 cnf(65,plain, % 124.44/125.15 (~E(f2(x651,x651,x652,x652),f2(f2(x653,a1,x654,x654),f2(x655,x655,x654,x654),x652,x652))+~E(a8,x653)), % 124.44/125.15 inference(scs_inference,[],[64,26])). % 124.44/125.15 cnf(66,plain, % 124.44/125.15 (~E(x661,a1)+~E(a8,x661)), % 124.44/125.15 inference(scs_inference,[],[65,52])). % 124.44/125.15 cnf(67,plain, % 124.44/125.15 (~E(x671,a8)+~E(x671,a1)), % 124.44/125.15 inference(scs_inference,[],[66,2])). % 124.44/125.15 cnf(68,plain, % 124.44/125.15 (~E(a1,a8)), % 124.44/125.15 inference(scs_inference,[],[18,67,20])). % 124.44/125.15 cnf(69,plain, % 124.44/125.15 (P2(f2(f9(a4),f10(a4),a6,a6),a4,f5(a6,a6))), % 124.44/125.15 inference(scs_inference,[],[18,68,21,20])). % 124.44/125.15 cnf(70,plain, % 124.44/125.15 (E(f9(a4),f10(a4))), % 124.44/125.15 inference(scs_inference,[],[69,20])). % 124.44/125.15 cnf(72,plain, % 124.44/125.15 (E(f10(a4),f9(a4))), % 124.44/125.15 inference(scs_inference,[],[69,20,2])). % 124.44/125.15 cnf(75,plain, % 124.44/125.15 (P2(x751,a4,f5(a6,a6))+~E(f2(f9(a4),f10(a4),a6,a6),x751)), % 124.44/125.15 inference(scs_inference,[],[69,20,2,13,15,14])). % 124.44/125.15 cnf(82,plain, % 124.44/125.15 (E(f2(f10(a4),x821,x822,x823),f2(f9(a4),x821,x822,x823))), % 124.44/125.15 inference(scs_inference,[],[70,2,4])). % 124.44/125.15 cnf(83,plain, % 124.44/125.15 (E(f2(f9(a4),x831,x832,x833),f2(f10(a4),x831,x832,x833))), % 124.44/125.15 inference(scs_inference,[],[82,2])). % 124.44/125.15 cnf(84,plain, % 124.44/125.15 (P2(f2(f9(a4),f10(a4),x841,x841),a4,f5(x841,x841))), % 124.44/125.15 inference(scs_inference,[],[18,82,2,14])). % 124.44/125.15 cnf(86,plain, % 124.44/125.15 (E(f2(f10(a4),x861,x862,x863),f2(f9(a4),x861,x862,x863))), % 124.44/125.15 inference(rename_variables,[],[82])). % 124.44/125.15 cnf(89,plain, % 124.44/125.15 (P2(f2(f9(a4),f10(a4),x891,x891),a4,x892)+~E(f5(x891,x891),x892)), % 124.44/125.15 inference(scs_inference,[],[18,82,86,2,14,13,15,16])). % 124.44/125.15 cnf(92,plain, % 124.44/125.15 (P2(f2(f10(a4),f9(a4),x921,x921),a4,f5(x921,x921))), % 124.44/125.15 inference(scs_inference,[],[18,83,14])). % 124.44/125.15 cnf(100,plain, % 124.44/125.15 (P2(f2(f10(a4),f9(a4),x1001,x1001),a4,x1002)+~E(f5(x1001,x1001),x1002)), % 124.44/125.15 inference(scs_inference,[],[92,15,16])). % 124.44/125.15 cnf(104,plain, % 124.44/125.15 (E(f2(x1041,f10(a4),x1042,x1043),f2(x1041,f9(a4),x1042,x1043))), % 124.44/125.15 inference(scs_inference,[],[70,2,5])). % 124.44/125.15 cnf(105,plain, % 124.44/125.15 (E(f2(x1051,f9(a4),x1052,x1053),f2(x1051,f10(a4),x1052,x1053))), % 124.44/125.15 inference(scs_inference,[],[104,2])). % 124.44/125.15 cnf(106,plain, % 124.44/125.15 (E(f2(f10(a4),f10(a4),x1061,x1062),f2(f9(a4),f9(a4),x1061,x1062))), % 124.44/125.15 inference(scs_inference,[],[82,104,2,3])). % 124.44/125.15 cnf(116,plain, % 124.44/125.15 (E(f2(f10(a4),f9(a4),x1161,x1162),f2(f9(a4),f10(a4),x1161,x1162))), % 124.44/125.15 inference(scs_inference,[],[82,105,106,2,3])). % 124.44/125.15 cnf(125,plain, % 124.44/125.15 (E(f2(f9(a4),f10(a4),x1251,x1252),f2(f10(a4),f9(a4),x1251,x1252))), % 124.44/125.15 inference(scs_inference,[],[116,2])). % 124.44/125.15 cnf(128,plain, % 124.44/125.15 (E(f2(x1281,x1282,f10(a4),x1283),f2(x1281,x1282,f9(a4),x1283))), % 124.44/125.15 inference(scs_inference,[],[70,2,6])). % 124.44/125.15 cnf(129,plain, % 124.44/125.15 (E(f2(x1291,x1292,f9(a4),x1293),f2(x1291,x1292,f10(a4),x1293))), % 124.44/125.15 inference(scs_inference,[],[128,2])). % 124.44/125.15 cnf(130,plain, % 124.44/125.15 (E(f2(f9(a4),x1301,f10(a4),x1302),f2(f10(a4),x1301,f9(a4),x1302))), % 124.44/125.15 inference(scs_inference,[],[83,128,2,3])). % 124.44/125.15 cnf(141,plain, % 124.44/125.15 (E(f2(f10(a4),x1411,f9(a4),x1412),f2(f9(a4),x1411,f10(a4),x1412))), % 124.44/125.15 inference(scs_inference,[],[130,2])). % 124.44/125.15 cnf(142,plain, % 124.44/125.15 (E(f2(f10(a4),x1421,f10(a4),x1422),f2(f9(a4),x1421,f9(a4),x1422))), % 124.44/125.15 inference(scs_inference,[],[82,130,128,2,3])). % 124.44/125.15 cnf(153,plain, % 124.44/125.15 (E(f2(f9(a4),x1531,f9(a4),x1532),f2(f10(a4),x1531,f10(a4),x1532))), % 124.44/125.15 inference(scs_inference,[],[142,2])). % 124.44/125.15 cnf(171,plain, % 124.44/125.15 (E(f2(x1711,f10(a4),f9(a4),x1712),f2(x1711,f9(a4),f10(a4),x1712))), % 124.44/125.15 inference(scs_inference,[],[104,129,3])). % 124.44/125.15 cnf(174,plain, % 124.44/125.15 (E(f2(x1741,f9(a4),f10(a4),x1742),f2(x1741,f10(a4),f9(a4),x1742))), % 124.44/125.15 inference(scs_inference,[],[104,129,3,2])). % 124.44/125.15 cnf(179,plain, % 124.44/125.15 (E(f2(f9(a4),f9(a4),f10(a4),x1791),f2(f10(a4),f10(a4),f9(a4),x1791))), % 124.44/125.15 inference(scs_inference,[],[104,141,3,2])). % 124.44/125.15 cnf(185,plain, % 124.44/125.15 (E(f2(f9(a4),f10(a4),f10(a4),x1851),f2(f10(a4),f9(a4),f9(a4),x1851))), % 124.44/125.15 inference(scs_inference,[],[104,130,3])). % 124.44/125.15 cnf(188,plain, % 124.44/125.15 (E(f2(f10(a4),f9(a4),f9(a4),x1881),f2(f9(a4),f10(a4),f10(a4),x1881))), % 124.44/125.15 inference(scs_inference,[],[104,130,3,2])). % 124.44/125.15 cnf(190,plain, % 124.44/125.15 (E(f2(x1901,f10(a4),f10(a4),x1902),f2(x1901,f9(a4),f9(a4),x1902))), % 124.44/125.15 inference(scs_inference,[],[104,128,3])). % 124.44/125.15 cnf(193,plain, % 124.44/125.15 (E(f2(x1931,f9(a4),f9(a4),x1932),f2(x1931,f10(a4),f10(a4),x1932))), % 124.44/125.15 inference(scs_inference,[],[104,128,3,2])). % 124.44/125.15 cnf(195,plain, % 124.44/125.15 (E(f2(f9(a4),f10(a4),f9(a4),x1951),f2(f10(a4),f9(a4),f10(a4),x1951))), % 124.44/125.15 inference(scs_inference,[],[104,153,3])). % 124.44/125.15 cnf(198,plain, % 124.44/125.15 (E(f2(f10(a4),f9(a4),f10(a4),x1981),f2(f9(a4),f10(a4),f9(a4),x1981))), % 124.44/125.15 inference(scs_inference,[],[104,153,3,2])). % 124.44/125.15 cnf(204,plain, % 124.44/125.15 (P2(f2(x2041,x2041,f9(a4),f10(a4)),a4,f5(f10(a4),f10(a4)))), % 124.44/125.15 inference(scs_inference,[],[128,18,14])). % 124.44/125.15 cnf(212,plain, % 124.44/125.15 (P2(f2(f9(a4),f10(a4),f9(a4),f10(a4)),a4,f5(f10(a4),f10(a4)))), % 124.44/125.15 inference(scs_inference,[],[128,84,14])). % 124.44/125.15 cnf(219,plain, % 124.44/125.15 (E(f9(f2(x2191,x2192,f9(a4),x2193)),f9(f2(x2191,x2192,f10(a4),x2193)))), % 124.44/125.15 inference(scs_inference,[],[128,2,10])). % 124.44/125.15 cnf(220,plain, % 124.44/125.15 (P2(f2(f10(a4),f9(a4),f9(a4),f10(a4)),a4,f5(f10(a4),f10(a4)))), % 124.44/125.15 inference(scs_inference,[],[128,92,14])). % 124.44/125.15 cnf(229,plain, % 124.44/125.15 (P2(f2(x2291,x2291,f10(a4),f9(a4)),a4,f5(f9(a4),f9(a4)))), % 124.44/125.15 inference(scs_inference,[],[129,18,14])). % 124.44/125.15 cnf(233,plain, % 124.44/125.15 (P2(f2(x2331,x2331,f10(a4),f9(a4)),a4,x2332)+~E(f5(f9(a4),f9(a4)),x2332)), % 124.44/125.15 inference(scs_inference,[],[129,18,14,15,16])). % 124.44/125.15 cnf(236,plain, % 124.44/125.15 (E(f9(f9(a4)),f9(f10(a4)))), % 124.44/125.15 inference(scs_inference,[],[83,2,40])). % 124.44/125.15 cnf(237,plain, % 124.44/125.15 (E(f9(f10(a4)),f9(f9(a4)))), % 124.44/125.15 inference(scs_inference,[],[236,2])). % 124.44/125.15 cnf(238,plain, % 124.44/125.15 (P2(f2(f9(a4),f10(a4),f10(a4),f9(a4)),a4,f5(f9(a4),f9(a4)))), % 124.44/125.15 inference(scs_inference,[],[129,84,236,2,14])). % 124.44/125.15 cnf(243,plain, % 124.44/125.15 (P2(f2(f9(a4),f10(a4),f10(a4),f9(a4)),a4,x2431)+~E(f5(f9(a4),f9(a4)),x2431)), % 124.44/125.15 inference(scs_inference,[],[129,84,236,2,14,13,15,16])). % 124.44/125.15 cnf(246,plain, % 124.44/125.15 (P2(f2(f10(a4),f9(a4),f10(a4),f9(a4)),a4,f5(f9(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[129,92,14])). % 124.44/125.16 cnf(251,plain, % 124.44/125.16 (P2(f2(f10(a4),f9(a4),f10(a4),f9(a4)),a4,x2511)+~E(f5(f9(a4),f9(a4)),x2511)), % 124.44/125.16 inference(scs_inference,[],[129,92,237,14,13,15,16])). % 124.44/125.16 cnf(264,plain, % 124.44/125.16 (E(f7(f10(a4)),f7(f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[83,2,42])). % 124.44/125.16 cnf(279,plain, % 124.44/125.16 (~P2(f2(a1,a8,x2791,x2791),a4,f5(x2791,x2791))), % 124.44/125.16 inference(scs_inference,[],[63,2,20])). % 124.44/125.16 cnf(286,plain, % 124.44/125.16 (~E(f2(x2861,x2861,x2862,x2862),f2(a1,a8,x2862,x2862))), % 124.44/125.16 inference(scs_inference,[],[279,23])). % 124.44/125.16 cnf(288,plain, % 124.44/125.16 (~P2(f2(a1,a8,x2881,x2881),a4,f5(x2881,x2881))), % 124.44/125.16 inference(rename_variables,[],[279])). % 124.44/125.16 cnf(289,plain, % 124.44/125.16 (~E(f2(f9(a4),f10(a4),f10(a4),f9(a4)),f2(a1,a8,f9(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[238,279,288,23,75,14])). % 124.44/125.16 cnf(291,plain, % 124.44/125.16 (~E(f2(f9(a4),f10(a4),f10(a4),f9(a4)),f2(a1,a8,f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[238,279,288,128,23,75,14,3])). % 124.44/125.16 cnf(294,plain, % 124.44/125.16 (~E(f2(f9(a4),f10(a4),x2941,x2941),f2(a1,a8,x2941,x2941))), % 124.44/125.16 inference(scs_inference,[],[279,84,14])). % 124.44/125.16 cnf(297,plain, % 124.44/125.16 (~E(f2(f10(a4),f9(a4),x2971,x2971),f2(a1,a8,x2971,x2971))), % 124.44/125.16 inference(scs_inference,[],[279,92,14])). % 124.44/125.16 cnf(300,plain, % 124.44/125.16 (~E(f2(x3001,x3001,f9(a4),f10(a4)),f2(a1,a8,f10(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[279,204,14])). % 124.44/125.16 cnf(303,plain, % 124.44/125.16 (~E(f2(f9(a4),f10(a4),f9(a4),f10(a4)),f2(a1,a8,f10(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[279,212,14])). % 124.44/125.16 cnf(306,plain, % 124.44/125.16 (~E(f2(f9(a4),f10(a4),f9(a4),f10(a4)),f2(a1,a8,f9(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[129,303,3])). % 124.44/125.16 cnf(308,plain, % 124.44/125.16 (~E(f2(f10(a4),f9(a4),f9(a4),f10(a4)),f2(a1,a8,f10(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[279,220,129,303,3,14])). % 124.44/125.16 cnf(313,plain, % 124.44/125.16 (~E(f2(x3131,x3131,f10(a4),f9(a4)),f2(a1,a8,f9(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[279,229,129,308,3,14])). % 124.44/125.16 cnf(316,plain, % 124.44/125.16 (~E(f2(f10(a4),f9(a4),f10(a4),f9(a4)),f2(a1,a8,f9(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[279,246,14])). % 124.44/125.16 cnf(319,plain, % 124.44/125.16 (~E(f2(f10(a4),f9(a4),f10(a4),f9(a4)),f2(a1,a8,f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[128,316,3])). % 124.44/125.16 cnf(331,plain, % 124.44/125.16 (~E(f2(x3311,x3311,f10(a4),f10(a4)),f2(a1,a8,f9(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[286,129,3])). % 124.44/125.16 cnf(335,plain, % 124.44/125.16 (~E(f2(x3351,x3351,f9(a4),f9(a4)),f2(a1,a8,f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[286,128,3])). % 124.44/125.16 cnf(342,plain, % 124.44/125.16 (~E(f2(f9(a4),f10(a4),f10(a4),f10(a4)),f2(a1,a8,f9(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[294,129,3])). % 124.44/125.16 cnf(346,plain, % 124.44/125.16 (~E(f2(f9(a4),f10(a4),f9(a4),f9(a4)),f2(a1,a8,f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[294,128,3])). % 124.44/125.16 cnf(351,plain, % 124.44/125.16 (~E(f2(f10(a4),f9(a4),f10(a4),f10(a4)),f2(a1,a8,f9(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[297,129,3])). % 124.44/125.16 cnf(355,plain, % 124.44/125.16 (~E(f2(f10(a4),f9(a4),f9(a4),f9(a4)),f2(a1,a8,f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[297,128,3])). % 124.44/125.16 cnf(360,plain, % 124.44/125.16 (~E(f2(x3601,x3601,f9(a4),f10(a4)),f2(a1,a8,f9(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[300,129,3])). % 124.44/125.16 cnf(368,plain, % 124.44/125.16 (~E(f2(x3681,x3681,f10(a4),f9(a4)),f2(a1,a8,f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[313,128,3])). % 124.44/125.16 cnf(396,plain, % 124.44/125.16 (~P2(f2(f2(a1,a8,f10(a4),f9(a4)),f2(f9(a4),f10(a4),f10(a4),f9(a4)),x3961,x3961),a4,f5(x3961,x3961))), % 124.44/125.16 inference(scs_inference,[],[291,2,20])). % 124.44/125.16 cnf(398,plain, % 124.44/125.16 (~P2(f2(f2(a1,a8,f10(a4),f9(a4)),f2(f9(a4),f10(a4),f10(a4),f9(a4)),x3981,x3981),a4,f5(x3981,x3981))), % 124.44/125.16 inference(rename_variables,[],[396])). % 124.44/125.16 cnf(399,plain, % 124.44/125.16 (~E(f2(x3991,x3991,x3992,x3992),f2(f2(a1,a8,f10(a4),f9(a4)),f2(f9(a4),f10(a4),f10(a4),f9(a4)),x3992,x3992))), % 124.44/125.16 inference(scs_inference,[],[396,398,75,23])). % 124.44/125.16 cnf(400,plain, % 124.44/125.16 (~E(f2(a1,a8,f10(a4),f9(a4)),f2(f9(a4),f10(a4),f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[399,2,4])). % 124.44/125.16 cnf(401,plain, % 124.44/125.16 (~E(f2(a1,a8,f10(a4),f9(a4)),f2(f10(a4),f10(a4),f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[82,400,3])). % 124.44/125.16 cnf(404,plain, % 124.44/125.16 (~E(f2(a1,a8,f10(a4),f9(a4)),f2(f9(a4),f9(a4),f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[105,400,3])). % 124.44/125.16 cnf(406,plain, % 124.44/125.16 (~E(f2(a1,a8,f10(a4),f9(a4)),f2(f10(a4),f9(a4),f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[83,404,2,3])). % 124.44/125.16 cnf(407,plain, % 124.44/125.16 (~E(f2(a1,a8,f10(a4),f9(a4)),f2(f10(a4),f9(a4),f9(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[141,404,3])). % 124.44/125.16 cnf(409,plain, % 124.44/125.16 (~P2(f2(f2(f10(a4),f9(a4),f10(a4),f9(a4)),f2(a1,a8,f10(a4),f9(a4)),x4091,x4091),a4,f5(x4091,x4091))), % 124.44/125.16 inference(scs_inference,[],[406,2,20])). % 124.44/125.16 cnf(411,plain, % 124.44/125.16 (~P2(f2(f2(f10(a4),f9(a4),f10(a4),f9(a4)),f2(a1,a8,f10(a4),f9(a4)),x4111,x4111),a4,f5(x4111,x4111))), % 124.44/125.16 inference(rename_variables,[],[409])). % 124.44/125.16 cnf(413,plain, % 124.44/125.16 (~E(f2(a1,a8,f10(a4),f9(a4)),f2(f9(a4),f9(a4),f9(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[83,407,409,411,75,23,3])). % 124.44/125.16 cnf(416,plain, % 124.44/125.16 (~E(f2(a1,a8,f10(a4),f9(a4)),f2(f9(a4),f10(a4),f9(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[104,413,3])). % 124.44/125.16 cnf(418,plain, % 124.44/125.16 (~E(f2(a1,a8,f10(a4),f9(a4)),f2(f10(a4),f10(a4),f9(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[83,416,2,3])). % 124.44/125.16 cnf(459,plain, % 124.44/125.16 (E(f7(f2(f9(a4),x4591,f9(a4),x4592)),f7(f2(f10(a4),x4591,f10(a4),x4592)))), % 124.44/125.16 inference(scs_inference,[],[142,2,11])). % 124.44/125.16 cnf(513,plain, % 124.44/125.16 (~E(f2(x5131,x5131,x5132,x5132),f2(f2(a1,a8,f9(a4),f10(a4)),f2(f10(a4),f9(a4),f10(a4),f10(a4)),x5132,x5132))), % 124.44/125.16 inference(scs_inference,[],[351,2,24])). % 124.44/125.16 cnf(516,plain, % 124.44/125.16 (~E(f2(a1,a8,f9(a4),f10(a4)),f2(f10(a4),f9(a4),f10(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[513,2,4])). % 124.44/125.16 cnf(517,plain, % 124.44/125.16 (~E(f2(a1,a8,f9(a4),f10(a4)),f2(f9(a4),f9(a4),f10(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[83,516,3])). % 124.44/125.16 cnf(519,plain, % 124.44/125.16 (~P2(f2(f2(a1,a8,f10(a4),f9(a4)),f2(f9(a4),f10(a4),f9(a4),f9(a4)),x5191,x5191),a4,f5(x5191,x5191))), % 124.44/125.16 inference(scs_inference,[],[346,2,20])). % 124.44/125.16 cnf(521,plain, % 124.44/125.16 (~P2(f2(f2(a1,a8,f10(a4),f9(a4)),f2(f9(a4),f10(a4),f9(a4),f9(a4)),x5211,x5211),a4,f5(x5211,x5211))), % 124.44/125.16 inference(rename_variables,[],[519])). % 124.44/125.16 cnf(523,plain, % 124.44/125.16 (~E(f2(a1,a8,f9(a4),f10(a4)),f2(f9(a4),f10(a4),f10(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[104,517,519,521,75,23,3])). % 124.44/125.16 cnf(526,plain, % 124.44/125.16 (~E(f2(a1,a8,f9(a4),f10(a4)),f2(f10(a4),f10(a4),f10(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[82,523,3])). % 124.44/125.16 cnf(532,plain, % 124.44/125.16 (~P2(f2(f2(a1,a8,f9(a4),f10(a4)),f2(f9(a4),f10(a4),f10(a4),f10(a4)),x5321,x5321),a4,f5(x5321,x5321))), % 124.44/125.16 inference(scs_inference,[],[342,2,20])). % 124.44/125.16 cnf(534,plain, % 124.44/125.16 (~P2(f2(f2(a1,a8,f9(a4),f10(a4)),f2(f9(a4),f10(a4),f10(a4),f10(a4)),x5341,x5341),a4,f5(x5341,x5341))), % 124.44/125.16 inference(rename_variables,[],[532])). % 124.44/125.16 cnf(535,plain, % 124.44/125.16 (~E(f2(x5351,x5351,x5352,x5352),f2(f2(a1,a8,f9(a4),f10(a4)),f2(f9(a4),f10(a4),f10(a4),f10(a4)),x5352,x5352))), % 124.44/125.16 inference(scs_inference,[],[532,534,75,23])). % 124.44/125.16 cnf(536,plain, % 124.44/125.16 (~E(f2(a1,a8,f9(a4),f10(a4)),f2(f9(a4),f10(a4),f9(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[153,526,532,534,75,23,3])). % 124.44/125.16 cnf(538,plain, % 124.44/125.16 (~E(f2(a1,a8,f9(a4),f10(a4)),f2(f10(a4),f10(a4),f9(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[83,536,2,3])). % 124.44/125.16 cnf(539,plain, % 124.44/125.16 (~E(f2(a1,a8,f9(a4),f10(a4)),f2(f10(a4),f9(a4),f9(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[105,538,3])). % 124.44/125.16 cnf(541,plain, % 124.44/125.16 (~E(f2(x5411,x5411,x5412,x5412),f2(f2(f10(a4),f9(a4),f9(a4),f10(a4)),f2(a1,a8,f9(a4),f10(a4)),x5412,x5412))), % 124.44/125.16 inference(scs_inference,[],[539,2,24])). % 124.44/125.16 cnf(545,plain, % 124.44/125.16 (~P2(f2(f2(f2(f10(a4),f9(a4),f9(a4),f10(a4)),f2(a1,a8,f9(a4),f10(a4)),x5451,x5451),f2(x5452,x5452,x5451,x5451),x5453,x5453),a4,f5(x5453,x5453))), % 124.44/125.16 inference(scs_inference,[],[541,2,20])). % 124.44/125.16 cnf(546,plain, % 124.44/125.16 (~E(f2(x5461,x5461,x5462,x5462),f2(f2(f2(f10(a4),f9(a4),f9(a4),f10(a4)),f2(a1,a8,f9(a4),f10(a4)),x5463,x5463),f2(x5464,x5464,x5463,x5463),x5462,x5462))), % 124.44/125.16 inference(scs_inference,[],[545,23])). % 124.44/125.16 cnf(550,plain, % 124.44/125.16 (~E(f2(f2(f10(a4),f9(a4),f9(a4),f10(a4)),f2(a1,a8,f9(a4),f10(a4)),x5501,x5501),f2(x5502,x5502,x5501,x5501))), % 124.44/125.16 inference(scs_inference,[],[546,2,4])). % 124.44/125.16 cnf(551,plain, % 124.44/125.16 (~E(f2(f2(f10(a4),f9(a4),f9(a4),f10(a4)),f2(a1,a8,f9(a4),f10(a4)),x5511,x5511),f2(f9(a4),f10(a4),x5511,x5511))), % 124.44/125.16 inference(scs_inference,[],[83,550,3])). % 124.44/125.16 cnf(554,plain, % 124.44/125.16 (~E(f2(x5541,x5541,x5542,x5542),f2(f2(f2(a1,a8,f9(a4),f10(a4)),f2(f9(a4),f10(a4),f10(a4),f10(a4)),x5543,x5543),f2(x5544,x5544,x5543,x5543),x5542,x5542))), % 124.44/125.16 inference(scs_inference,[],[535,2,24])). % 124.44/125.16 cnf(557,plain, % 124.44/125.16 (~E(f2(f2(a1,a8,f9(a4),f10(a4)),f2(f9(a4),f10(a4),f10(a4),f10(a4)),x5571,x5571),f2(x5572,x5572,x5571,x5571))), % 124.44/125.16 inference(scs_inference,[],[554,2,4])). % 124.44/125.16 cnf(558,plain, % 124.44/125.16 (~E(f2(f2(a1,a8,f9(a4),f10(a4)),f2(f9(a4),f10(a4),f10(a4),f10(a4)),x5581,x5581),f2(f10(a4),f9(a4),x5581,x5581))), % 124.44/125.16 inference(scs_inference,[],[82,557,3])). % 124.44/125.16 cnf(562,plain, % 124.44/125.16 (~E(f2(f2(f10(a4),f9(a4),f9(a4),f10(a4)),f2(a1,a8,f9(a4),f10(a4)),x5621,x5621),f2(f10(a4),f9(a4),x5621,x5621))), % 124.44/125.16 inference(scs_inference,[],[116,551,3])). % 124.44/125.16 cnf(565,plain, % 124.44/125.16 (~E(f2(f2(a1,a8,f9(a4),f10(a4)),f2(f9(a4),f10(a4),f10(a4),f10(a4)),f9(a4),f9(a4)),f2(f9(a4),f9(a4),f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[130,558,3])). % 124.44/125.16 cnf(569,plain, % 124.44/125.16 (~E(f2(f2(f10(a4),f9(a4),f9(a4),f10(a4)),f2(a1,a8,f9(a4),f10(a4)),f9(a4),f9(a4)),f2(f9(a4),f9(a4),f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[130,562,3])). % 124.44/125.16 cnf(575,plain, % 124.44/125.16 (~P2(f2(f2(a1,a8,f10(a4),f9(a4)),f2(f10(a4),f9(a4),f10(a4),f9(a4)),x5751,x5751),a4,f5(x5751,x5751))), % 124.44/125.16 inference(scs_inference,[],[319,2,20])). % 124.44/125.16 cnf(577,plain, % 124.44/125.16 (~P2(f2(f2(a1,a8,f10(a4),f9(a4)),f2(f10(a4),f9(a4),f10(a4),f9(a4)),x5771,x5771),a4,f5(x5771,x5771))), % 124.44/125.16 inference(rename_variables,[],[575])). % 124.44/125.16 cnf(578,plain, % 124.44/125.16 (~E(f2(x5781,x5781,x5782,x5782),f2(f2(a1,a8,f10(a4),f9(a4)),f2(f10(a4),f9(a4),f10(a4),f9(a4)),x5782,x5782))), % 124.44/125.16 inference(scs_inference,[],[575,577,75,23])). % 124.44/125.16 cnf(581,plain, % 124.44/125.16 (~E(f2(x5811,x5811,x5812,x5812),f2(f2(f2(a1,a8,f10(a4),f9(a4)),f2(f10(a4),f9(a4),f10(a4),f9(a4)),x5813,x5813),f2(x5814,x5814,x5813,x5813),x5812,x5812))), % 124.44/125.16 inference(scs_inference,[],[578,2,24])). % 124.44/125.16 cnf(582,plain, % 124.44/125.16 (~E(f2(f2(a1,a8,f10(a4),f9(a4)),f2(f10(a4),f9(a4),f10(a4),f9(a4)),x5821,x5821),f2(x5822,x5822,x5821,x5821))), % 124.44/125.16 inference(scs_inference,[],[581,2,4])). % 124.44/125.16 cnf(590,plain, % 124.44/125.16 (~E(f2(f2(a1,a8,f10(a4),f9(a4)),f2(f10(a4),f9(a4),f10(a4),f9(a4)),f9(a4),f9(a4)),f2(f10(a4),f9(a4),f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[142,582,3])). % 124.44/125.16 cnf(593,plain, % 124.44/125.16 (~E(f2(f2(a1,a8,f10(a4),f9(a4)),f2(f10(a4),f9(a4),f10(a4),f9(a4)),f9(a4),f9(a4)),f2(f9(a4),f9(a4),f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[82,590,2,3])). % 124.44/125.16 cnf(605,plain, % 124.44/125.16 (~E(f2(x6051,x6051,x6052,x6052),f2(a1,x6053,x6052,x6052))+~E(a8,x6053)), % 124.44/125.16 inference(scs_inference,[],[66,26])). % 124.44/125.16 cnf(606,plain, % 124.44/125.16 (~E(f2(x6061,x6061,x6062,x6062),f2(f2(x6063,x6063,x6064,x6064),f2(a1,x6065,x6064,x6064),x6062,x6062))+~E(a8,x6065)), % 124.44/125.16 inference(scs_inference,[],[605,24])). % 124.44/125.16 cnf(607,plain, % 124.44/125.16 (~E(f2(x6071,x6071,x6072,x6072),f2(f2(x6073,x6073,x6074,x6074),f2(a1,a8,x6074,x6074),x6072,x6072))), % 124.44/125.16 inference(scs_inference,[],[18,606,20])). % 124.44/125.16 cnf(608,plain, % 124.44/125.16 (~E(f2(a1,a8,x6081,x6081),f2(x6082,x6082,x6081,x6081))), % 124.44/125.16 inference(scs_inference,[],[607,4])). % 124.44/125.16 cnf(610,plain, % 124.44/125.16 (~E(f2(x6101,x6101,x6102,x6102),f2(a8,x6103,x6102,x6102))+~E(x6103,a1)), % 124.44/125.16 inference(scs_inference,[],[66,24])). % 124.44/125.16 cnf(611,plain, % 124.44/125.16 (~E(f2(a1,a8,x6111,x6111),f2(f9(a4),f10(a4),x6111,x6111))), % 124.44/125.16 inference(scs_inference,[],[83,608,3])). % 124.44/125.16 cnf(614,plain, % 124.44/125.16 (~E(f2(x6141,x6141,x6142,x6142),f2(f2(a8,x6143,x6144,x6144),f2(x6145,x6145,x6144,x6144),x6142,x6142))+~E(x6143,a1)), % 124.44/125.16 inference(scs_inference,[],[610,26])). % 124.44/125.16 cnf(615,plain, % 124.44/125.16 (~E(f2(a1,a8,x6151,x6151),f2(f10(a4),f9(a4),x6151,x6151))), % 124.44/125.16 inference(scs_inference,[],[116,611,3])). % 124.44/125.16 cnf(617,plain, % 124.44/125.16 (~E(f2(x6171,x6171,x6172,x6172),f2(f2(a8,a1,x6173,x6173),f2(x6174,x6174,x6173,x6173),x6172,x6172))), % 124.44/125.16 inference(scs_inference,[],[18,614,20])). % 124.44/125.16 cnf(618,plain, % 124.44/125.16 (~E(f2(a8,a1,x6181,x6181),f2(x6182,x6182,x6181,x6181))), % 124.44/125.16 inference(scs_inference,[],[617,5])). % 124.44/125.16 cnf(619,plain, % 124.44/125.16 (~E(f2(x6191,x6191,x6192,x6192),f2(f2(a8,a1,x6193,x6193),f2(x6194,x6194,x6193,x6193),x6192,x6192))), % 124.44/125.16 inference(rename_variables,[],[617])). % 124.44/125.16 cnf(620,plain, % 124.44/125.16 (~E(f2(x6201,x6201,x6202,x6202),f2(a8,a1,x6202,x6202))), % 124.44/125.16 inference(scs_inference,[],[617,619,5,4])). % 124.44/125.16 cnf(622,plain, % 124.44/125.16 (~E(f2(a1,a8,f10(a4),f10(a4)),f2(f9(a4),f9(a4),f9(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[153,617,619,615,5,4,3])). % 124.44/125.16 cnf(626,plain, % 124.44/125.16 (~E(f2(a1,a8,f10(a4),f10(a4)),f2(f10(a4),f9(a4),f9(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[82,622,3])). % 124.44/125.16 cnf(629,plain, % 124.44/125.16 (~E(f2(a8,a1,x6291,x6291),f2(f10(a4),f9(a4),x6291,x6291))), % 124.44/125.16 inference(scs_inference,[],[105,618,3])). % 124.44/125.16 cnf(633,plain, % 124.44/125.16 (~E(f2(a1,a8,f10(a4),f10(a4)),f2(f10(a4),f10(a4),f9(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[104,626,3])). % 124.44/125.16 cnf(636,plain, % 124.44/125.16 (~E(f2(a1,a8,f10(a4),f10(a4)),f2(f9(a4),f10(a4),f9(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[83,633,3])). % 124.44/125.16 cnf(639,plain, % 124.44/125.16 (~E(f2(a8,a1,x6391,x6391),f2(f9(a4),f10(a4),x6391,x6391))), % 124.44/125.16 inference(scs_inference,[],[125,629,3])). % 124.44/125.16 cnf(663,plain, % 124.44/125.16 (~E(f2(x6631,x6631,x6632,x6632),f2(x6633,a1,x6632,x6632))+~E(x6633,a8)), % 124.44/125.16 inference(scs_inference,[],[67,24])). % 124.44/125.16 cnf(664,plain, % 124.44/125.16 (~E(f2(x6641,x6641,x6642,x6642),f2(f2(x6643,a1,x6644,x6644),f2(x6645,x6645,x6644,x6644),x6642,x6642))+~E(x6643,a8)), % 124.44/125.16 inference(scs_inference,[],[663,26])). % 124.44/125.16 cnf(667,plain, % 124.44/125.16 (~E(f2(x6671,x6671,x6672,x6672),f2(x6673,a8,x6672,x6672))+~E(f2(x6674,x6674,x6675,x6675),f2(f2(x6673,a1,x6676,x6676),f2(x6677,x6677,x6676,x6676),x6675,x6675))), % 124.44/125.16 inference(scs_inference,[],[664,24])). % 124.44/125.16 cnf(670,plain, % 124.44/125.16 (~E(f2(x6701,x6701,x6702,x6702),f2(f2(x6703,a8,x6704,x6704),f2(x6705,x6705,x6704,x6704),x6702,x6702))+~E(f2(x6706,x6706,x6707,x6707),f2(f2(x6703,a1,x6708,x6708),f2(x6709,x6709,x6708,x6708),x6707,x6707))), % 124.44/125.16 inference(scs_inference,[],[667,26])). % 124.44/125.16 cnf(673,plain, % 124.44/125.16 (~E(f2(x6731,x6731,x6732,x6732),f2(f2(a1,a8,x6733,x6733),f2(x6734,x6734,x6733,x6733),x6732,x6732))), % 124.44/125.16 inference(scs_inference,[],[18,670,20])). % 124.44/125.16 cnf(721,plain, % 124.44/125.16 (~E(f2(f10(a4),f9(a4),f10(a4),f9(a4)),f2(f2(a1,a8,f10(a4),f9(a4)),f2(f9(a4),f10(a4),f10(a4),f9(a4)),f9(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[396,246,14])). % 124.44/125.16 cnf(771,plain, % 124.44/125.16 (~E(f2(f9(a4),f10(a4),f10(a4),f9(a4)),f2(f2(f10(a4),f9(a4),f10(a4),f9(a4)),f2(a1,a8,f10(a4),f9(a4)),f9(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[409,238,14])). % 124.44/125.16 cnf(796,plain, % 124.44/125.16 (~E(f2(f2(a1,a8,f10(a4),f9(a4)),f2(f10(a4),f9(a4),f10(a4),f9(a4)),f9(a4),f9(a4)),f2(f9(a4),f10(a4),f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[104,593,3])). % 124.44/125.16 cnf(799,plain, % 124.44/125.16 (~E(f2(f2(a1,a8,f9(a4),f10(a4)),f2(f9(a4),f10(a4),f10(a4),f10(a4)),f9(a4),f9(a4)),f2(f9(a4),f10(a4),f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[104,565,3])). % 124.44/125.16 cnf(802,plain, % 124.44/125.16 (~E(f2(f2(f10(a4),f9(a4),f9(a4),f10(a4)),f2(a1,a8,f9(a4),f10(a4)),f9(a4),f9(a4)),f2(f9(a4),f10(a4),f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[104,569,3])). % 124.44/125.16 cnf(896,plain, % 124.44/125.16 (~E(f2(a1,a8,f9(a4),f10(a4)),f2(f9(a4),f9(a4),f9(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[516,153,3])). % 124.44/125.16 cnf(969,plain, % 124.44/125.16 (~E(f2(a1,a8,f9(a4),f9(a4)),f2(f10(a4),f9(a4),f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[142,608,3])). % 124.44/125.16 cnf(974,plain, % 124.44/125.16 (~E(f2(a1,a8,f9(a4),f9(a4)),f2(f9(a4),f10(a4),f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[125,969,3])). % 124.44/125.16 cnf(976,plain, % 124.44/125.16 (~E(f2(a8,a1,f10(a4),f10(a4)),f2(f10(a4),f9(a4),f9(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[141,618,3])). % 124.44/125.16 cnf(980,plain, % 124.44/125.16 (~E(f2(a8,a1,f10(a4),f10(a4)),f2(f9(a4),f10(a4),f9(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[125,976,3])). % 124.44/125.16 cnf(983,plain, % 124.44/125.16 (~E(f2(a8,a1,f9(a4),f9(a4)),f2(f10(a4),f9(a4),f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[142,618,3])). % 124.44/125.16 cnf(987,plain, % 124.44/125.16 (~E(f2(a8,a1,f9(a4),f9(a4)),f2(f9(a4),f10(a4),f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[125,983,3])). % 124.44/125.16 cnf(1002,plain, % 124.44/125.16 (~E(f2(x10021,x10021,f9(a4),f9(a4)),f2(f2(a1,a8,x10022,x10022),f2(x10023,x10023,x10022,x10022),f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[128,673,3])). % 124.44/125.16 cnf(1006,plain, % 124.44/125.16 (~E(f2(x10061,x10061,f9(a4),f9(a4)),f2(f2(x10062,x10062,x10063,x10063),f2(a1,a8,x10063,x10063),f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[128,607,3])). % 124.44/125.16 cnf(1011,plain, % 124.44/125.16 (~E(f2(x10111,x10111,f9(a4),f9(a4)),f2(f2(a8,a1,x10112,x10112),f2(x10113,x10113,x10112,x10112),f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[128,617,3])). % 124.44/125.16 cnf(1015,plain, % 124.44/125.16 (~E(f2(x10151,x10151,f10(a4),f10(a4)),f2(f2(a1,a8,x10152,x10152),f2(x10153,x10153,x10152,x10152),f9(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[129,673,3])). % 124.44/125.16 cnf(1019,plain, % 124.44/125.16 (~E(f2(x10191,x10191,f10(a4),f10(a4)),f2(f2(x10192,x10192,x10193,x10193),f2(a1,a8,x10193,x10193),f9(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[129,607,3])). % 124.44/125.16 cnf(1022,plain, % 124.44/125.16 (~E(f2(x10221,x10221,f10(a4),f10(a4)),f2(f2(a8,a1,x10222,x10222),f2(x10223,x10223,x10222,x10222),f9(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[129,617,3])). % 124.44/125.16 cnf(1030,plain, % 124.44/125.16 (~E(f2(f2(f10(a4),f9(a4),f9(a4),f10(a4)),f2(a1,a8,f9(a4),f10(a4)),f10(a4),f10(a4)),f2(f10(a4),f9(a4),f9(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[550,141,3])). % 124.44/125.16 cnf(1034,plain, % 124.44/125.16 (~E(f2(f2(f10(a4),f9(a4),f9(a4),f10(a4)),f2(a1,a8,f9(a4),f10(a4)),f10(a4),f10(a4)),f2(f9(a4),f10(a4),f9(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[125,1030,3])). % 124.44/125.16 cnf(1077,plain, % 124.44/125.16 (~E(f2(f2(a1,a8,f9(a4),f10(a4)),f2(f9(a4),f10(a4),f10(a4),f10(a4)),f9(a4),f9(a4)),f2(f10(a4),f9(a4),f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[557,142,3])). % 124.44/125.16 cnf(1116,plain, % 124.44/125.16 (~E(f2(f2(a1,a8,f10(a4),f9(a4)),f2(f10(a4),f9(a4),f10(a4),f9(a4)),f10(a4),f10(a4)),f2(f10(a4),f9(a4),f9(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[582,141,3])). % 124.44/125.16 cnf(1141,plain, % 124.44/125.16 (E(f5(f10(a4),x11411),f5(f9(a4),x11411))), % 124.44/125.16 inference(scs_inference,[],[82,8,26])). % 124.44/125.16 cnf(1142,plain, % 124.44/125.16 (E(f5(f9(a4),x11421),f5(f10(a4),x11421))), % 124.44/125.16 inference(scs_inference,[],[1141,2])). % 124.44/125.16 cnf(1233,plain, % 124.44/125.16 (~E(f2(a1,a8,f9(a4),f9(a4)),f2(x12331,x12331,f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[608,128,3])). % 124.44/125.16 cnf(1237,plain, % 124.44/125.16 (~E(f2(a1,a8,f10(a4),f10(a4)),f2(x12371,x12371,f9(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[608,129,3])). % 124.44/125.16 cnf(1245,plain, % 124.44/125.16 (~E(f2(a8,a1,f9(a4),f9(a4)),f2(x12451,x12451,f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[618,128,3])). % 124.44/125.16 cnf(1249,plain, % 124.44/125.16 (~E(f2(a8,a1,f10(a4),f10(a4)),f2(x12491,x12491,f9(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[618,129,3])). % 124.44/125.16 cnf(1254,plain, % 124.44/125.16 (~E(f2(x12541,x12541,f9(a4),f9(a4)),f2(a8,a1,f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[620,128,3])). % 124.44/125.16 cnf(1258,plain, % 124.44/125.16 (~E(f2(x12581,x12581,f10(a4),f10(a4)),f2(a8,a1,f9(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[620,129,3])). % 124.44/125.16 cnf(1341,plain, % 124.44/125.16 (~E(f2(f10(a4),f9(a4),f10(a4),f9(a4)),f2(f2(a1,a8,f10(a4),f9(a4)),f2(f9(a4),f10(a4),f10(a4),f9(a4)),f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[721,128,3])). % 124.44/125.16 cnf(1379,plain, % 124.44/125.16 (~E(f2(f9(a4),f10(a4),f10(a4),f9(a4)),f2(f2(f10(a4),f9(a4),f10(a4),f9(a4)),f2(a1,a8,f10(a4),f9(a4)),f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[771,128,3])). % 124.44/125.16 cnf(1689,plain, % 124.44/125.16 (E(f5(x16891,f9(a4)),f5(x16891,f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[83,9,26])). % 124.44/125.16 cnf(1690,plain, % 124.44/125.16 (E(f5(x16901,f10(a4)),f5(x16901,f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[1689,2])). % 124.44/125.16 cnf(1691,plain, % 124.44/125.16 (E(f5(f10(a4),f9(a4)),f5(f9(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[1141,1689,2,3])). % 124.44/125.16 cnf(1699,plain, % 124.44/125.16 (E(f5(f9(a4),f10(a4)),f5(f10(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[1691,2])). % 124.44/125.16 cnf(1700,plain, % 124.44/125.16 (E(f5(f9(a4),f9(a4)),f5(f10(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[1142,1691,1689,2,3])). % 124.44/125.16 cnf(1708,plain, % 124.44/125.16 (E(f5(f10(a4),f10(a4)),f5(f9(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[1700,2])). % 124.44/125.16 cnf(1869,plain, % 124.44/125.16 (E(f2(x18691,x18692,x18693,f10(a4)),f2(x18691,x18692,x18693,f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[1708,72,34,7])). % 124.44/125.16 cnf(1875,plain, % 124.44/125.16 (~E(f2(x18751,x18751,x18752,x18752),f2(f2(a1,a8,f10(a4),f10(a4)),f2(f9(a4),f10(a4),f9(a4),f10(a4)),x18752,x18752))), % 124.44/125.16 inference(scs_inference,[],[636,1708,1700,72,34,7,89,100,233,243,251,24])). % 124.44/125.16 cnf(1877,plain, % 124.44/125.16 (~E(f2(x18771,x18771,x18772,x18772),f2(f2(f9(a4),f10(a4),f9(a4),f10(a4)),f2(a1,a8,f10(a4),f10(a4)),x18772,x18772))), % 124.44/125.16 inference(scs_inference,[],[636,1708,1700,72,34,7,89,100,233,243,251,24,26])). % 124.44/125.16 cnf(1878,plain, % 124.44/125.16 (~P2(f2(f2(a1,a8,f10(a4),f10(a4)),f2(f9(a4),f10(a4),f9(a4),f10(a4)),x18781,x18781),a4,f5(x18781,x18781))), % 124.44/125.16 inference(scs_inference,[],[636,1708,1700,72,34,7,89,100,233,243,251,24,26,20])). % 124.44/125.16 cnf(1880,plain, % 124.44/125.16 (~E(f2(f9(a4),f10(a4),f9(a4),f10(a4)),f2(a8,a1,f10(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[636,980,1708,1700,72,34,7,89,100,233,243,251,24,26,20,2])). % 124.44/125.16 cnf(1881,plain, % 124.44/125.16 (~P2(f2(f7(f9(a4)),f7(f10(a4)),a6,a6),a4,f5(a6,a6))), % 124.44/125.16 inference(scs_inference,[],[636,980,1708,1700,72,279,18,34,7,89,100,233,243,251,24,26,20,2,22])). % 124.44/125.16 cnf(1885,plain, % 124.44/125.16 (~P2(f2(f2(a1,a8,f10(a4),f9(a4)),f2(f9(a4),f10(a4),f9(a4),f9(a4)),f9(a4),f9(a4)),a4,f5(f10(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[636,980,1708,519,1700,72,279,18,34,7,89,100,233,243,251,24,26,20,2,22,16])). % 124.44/125.16 cnf(1886,plain, % 124.44/125.16 (~P2(f2(f2(a1,a8,f10(a4),f9(a4)),f2(f9(a4),f10(a4),f9(a4),f9(a4)),x18861,x18861),a4,f5(x18861,x18861))), % 124.44/125.16 inference(rename_variables,[],[519])). % 124.44/125.16 cnf(1887,plain, % 124.44/125.16 (~P2(f2(f2(a1,a8,f10(a4),f9(a4)),f2(f9(a4),f10(a4),f9(a4),f9(a4)),f9(a4),f10(a4)),a4,f5(f10(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[636,980,1708,519,1886,1700,72,279,18,129,34,7,89,100,233,243,251,24,26,20,2,22,16,14])). % 124.44/125.16 cnf(1890,plain, % 124.44/125.16 (~E(f2(a8,a1,f9(a4),f10(a4)),f2(f9(a4),f10(a4),f9(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[636,980,1708,519,1886,1700,72,279,18,129,128,34,7,89,100,233,243,251,24,26,20,2,22,16,14,3])). % 124.44/125.16 cnf(1897,plain, % 124.44/125.16 (E(f5(x18971,f10(a4)),f5(x18971,f9(a4)))), % 124.44/125.16 inference(rename_variables,[],[1690])). % 124.44/125.16 cnf(1899,plain, % 124.44/125.16 (E(f5(x18991,f9(a4)),f5(x18991,f10(a4)))), % 124.44/125.16 inference(rename_variables,[],[1689])). % 124.44/125.16 cnf(1900,plain, % 124.44/125.16 (E(f2(x19001,x19002,x19003,f9(a4)),f2(x19001,x19002,x19003,f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[1690,1689,70,89,251,7])). % 124.44/125.16 cnf(1901,plain, % 124.44/125.16 (~E(f2(x19011,x19011,x19012,x19012),f2(f2(f9(a4),f10(a4),f10(a4),f9(a4)),f2(a1,a8,f9(a4),f9(a4)),x19012,x19012))), % 124.44/125.16 inference(scs_inference,[],[974,1690,1689,70,89,251,7,26])). % 124.44/125.16 cnf(1903,plain, % 124.44/125.16 (E(f5(x19031,f10(a4)),f5(x19031,f9(a4)))), % 124.44/125.16 inference(rename_variables,[],[1690])). % 124.44/125.16 cnf(1905,plain, % 124.44/125.16 (E(f5(x19051,f10(a4)),f5(x19051,f9(a4)))), % 124.44/125.16 inference(rename_variables,[],[1690])). % 124.44/125.16 cnf(1909,plain, % 124.44/125.16 (E(f5(x19091,f9(a4)),f5(x19091,f10(a4)))), % 124.44/125.16 inference(rename_variables,[],[1689])). % 124.44/125.16 cnf(1912,plain, % 124.44/125.16 (~P2(f2(f2(a8,a1,f9(a4),f9(a4)),f2(f9(a4),f10(a4),f10(a4),f9(a4)),x19121,x19121),a4,f5(x19121,x19121))), % 124.44/125.16 inference(scs_inference,[],[974,987,1690,1897,1903,1689,1899,1909,70,89,251,7,26,34,100,24,243,233,20])). % 124.44/125.16 cnf(1914,plain, % 124.44/125.16 (~E(f2(f9(a4),f10(a4),f10(a4),f9(a4)),f2(a8,a1,f9(a4),f9(a4)))), % 124.44/125.16 inference(scs_inference,[],[974,987,1690,1897,1903,1689,1899,1909,70,89,251,7,26,34,100,24,243,233,20,2])). % 124.44/125.16 cnf(1915,plain, % 124.44/125.16 (~P2(f2(f2(a1,a8,f10(a4),f10(a4)),f2(f9(a4),f10(a4),f9(a4),f10(a4)),f9(a4),f9(a4)),a4,f5(f9(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[974,987,1878,1690,1897,1903,1905,1689,1899,1909,70,89,251,7,26,34,100,24,243,233,20,2,16])). % 124.44/125.16 cnf(1917,plain, % 124.44/125.16 (~P2(f2(f2(a1,a8,f10(a4),f10(a4)),f2(f9(a4),f10(a4),f9(a4),f10(a4)),x19171,x19171),a4,f5(x19171,x19171))), % 124.44/125.16 inference(rename_variables,[],[1878])). % 124.44/125.16 cnf(1919,plain, % 124.44/125.16 (E(f2(x19191,x19192,x19193,f10(a4)),f2(x19191,x19192,x19193,f9(a4)))), % 124.44/125.16 inference(rename_variables,[],[1869])). % 124.44/125.16 cnf(1921,plain, % 124.44/125.16 (~E(f2(f9(a4),f10(a4),f9(a4),f9(a4)),f2(a8,a1,f10(a4),f10(a4)))), % 124.44/125.16 inference(scs_inference,[],[974,987,1880,1869,1919,1878,1917,1690,1897,1903,1905,1689,1899,1909,70,89,251,7,26,34,100,24,243,233,20,2,16,14,3])). % 124.44/125.16 cnf(1927,plain, % 124.44/125.17 (~E(f2(x19271,x19271,x19272,x19272),f2(f2(f9(a4),f10(a4),f10(a4),f9(a4)),f2(a8,a1,f9(a4),f9(a4)),x19272,x19272))), % 124.44/125.17 inference(scs_inference,[],[1914,24])). % 124.44/125.17 cnf(1930,plain, % 124.44/125.17 (~E(f2(x19301,x19301,x19302,x19302),f2(f2(a8,a1,f10(a4),f10(a4)),f2(f9(a4),f10(a4),f9(a4),f9(a4)),x19302,x19302))), % 124.44/125.17 inference(scs_inference,[],[1914,1921,1700,24,89,26])). % 124.44/125.17 cnf(1933,plain, % 124.50/125.17 (~P2(f2(f2(f9(a4),f10(a4),f10(a4),f9(a4)),f2(a8,a1,f9(a4),f9(a4)),x19331,x19331),a4,f5(x19331,x19331))), % 124.50/125.17 inference(scs_inference,[],[1914,1921,1700,24,89,26,100,34,20])). % 124.50/125.17 cnf(1935,plain, % 124.50/125.17 (~E(f2(a8,a1,f10(a4),f10(a4)),f2(f9(a4),f10(a4),f9(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[1914,1921,1700,24,89,26,100,34,20,2])). % 124.50/125.17 cnf(1936,plain, % 124.50/125.17 (~P2(f2(f2(a8,a1,f9(a4),f9(a4)),f2(f9(a4),f10(a4),f10(a4),f9(a4)),f9(a4),f9(a4)),a4,f5(f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[1914,1921,1912,1690,1700,24,89,26,100,34,20,2,16])). % 124.50/125.17 cnf(1941,plain, % 124.50/125.17 (~E(f2(f9(a4),f10(a4),f10(a4),f10(a4)),f2(a8,a1,f9(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[1914,1921,1900,1881,1912,1690,1700,92,24,89,26,100,34,20,2,16,14,3])). % 124.50/125.17 cnf(1948,plain, % 124.50/125.17 (~E(f2(x19481,x19481,x19482,x19482),f2(f2(f9(a4),f10(a4),f10(a4),f10(a4)),f2(a8,a1,f9(a4),f9(a4)),x19482,x19482))), % 124.50/125.17 inference(scs_inference,[],[1941,24])). % 124.50/125.17 cnf(1951,plain, % 124.50/125.17 (E(f5(x19511,f9(a4)),f5(x19511,f10(a4)))), % 124.50/125.17 inference(rename_variables,[],[1689])). % 124.50/125.17 cnf(1952,plain, % 124.50/125.17 (~E(f2(x19521,x19521,x19522,x19522),f2(f2(f9(a4),f10(a4),f9(a4),f9(a4)),f2(a8,a1,f10(a4),f10(a4)),x19522,x19522))), % 124.50/125.17 inference(scs_inference,[],[1935,1941,1689,24,89,26])). % 124.50/125.17 cnf(1954,plain, % 124.50/125.17 (E(f5(x19541,f9(a4)),f5(x19541,f10(a4)))), % 124.50/125.17 inference(rename_variables,[],[1689])). % 124.50/125.17 cnf(1957,plain, % 124.50/125.17 (~P2(f2(f2(a8,a1,f10(a4),f10(a4)),f2(f9(a4),f10(a4),f9(a4),f9(a4)),x19571,x19571),a4,f5(x19571,x19571))), % 124.50/125.17 inference(scs_inference,[],[1935,1941,1689,1951,1954,24,89,26,100,34,20])). % 124.50/125.17 cnf(1959,plain, % 124.50/125.17 (~E(f2(a8,a1,f9(a4),f9(a4)),f2(f9(a4),f10(a4),f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[1935,1941,1689,1951,1954,24,89,26,100,34,20,2])). % 124.50/125.17 cnf(1960,plain, % 124.50/125.17 (~P2(f2(f2(a1,a8,f10(a4),f10(a4)),f2(f9(a4),f10(a4),f9(a4),f10(a4)),f9(a4),f9(a4)),a4,f5(f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[1935,1941,1915,1691,1689,1951,1954,24,89,26,100,34,20,2,16])). % 124.50/125.17 cnf(1961,plain, % 124.50/125.17 (~P2(f2(f2(f9(a4),f10(a4),f10(a4),f9(a4)),f2(a8,a1,f9(a4),f9(a4)),f10(a4),f9(a4)),a4,f5(f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[1935,1941,1933,1915,1900,1691,1689,1951,1954,24,89,26,100,34,20,2,16,14])). % 124.50/125.17 cnf(1962,plain, % 124.50/125.17 (E(f2(x19621,x19622,x19623,f9(a4)),f2(x19621,x19622,x19623,f10(a4)))), % 124.50/125.17 inference(rename_variables,[],[1900])). % 124.50/125.17 cnf(1964,plain, % 124.50/125.17 (~E(f2(x19641,x19641,f9(a4),f10(a4)),f2(a1,a8,f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[1935,1941,335,1933,1915,1900,1962,1691,1689,1951,1954,24,89,26,100,34,20,2,16,14,3])). % 124.50/125.17 cnf(1974,plain, % 124.50/125.17 (~P2(f2(f2(a8,a1,f9(a4),f9(a4)),f2(f9(a4),f10(a4),f10(a4),f10(a4)),x19741,x19741),a4,f5(x19741,x19741))), % 124.50/125.17 inference(scs_inference,[],[1959,896,24,26,20])). % 124.50/125.17 cnf(1976,plain, % 124.50/125.17 (~E(f2(f9(a4),f10(a4),f9(a4),f10(a4)),f2(a8,a1,f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[1959,896,1890,24,26,20,2])). % 124.50/125.17 cnf(1977,plain, % 124.50/125.17 (~P2(f2(f2(a8,a1,f10(a4),f10(a4)),f2(f9(a4),f10(a4),f9(a4),f9(a4)),f9(a4),f9(a4)),a4,f5(f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[1959,896,1890,1957,1690,24,26,20,2,16])). % 124.50/125.17 cnf(1978,plain, % 124.50/125.17 (~P2(f2(f2(a8,a1,f10(a4),f10(a4)),f2(f9(a4),f10(a4),f9(a4),f9(a4)),x19781,x19781),a4,f5(x19781,x19781))), % 124.50/125.17 inference(rename_variables,[],[1957])). % 124.50/125.17 cnf(1983,plain, % 124.50/125.17 (~E(f2(a8,a1,f9(a4),f10(a4)),f2(f9(a4),f10(a4),f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[1959,896,1890,1957,1978,1869,1900,1690,24,26,20,2,16,14,3])). % 124.50/125.17 cnf(1992,plain, % 124.50/125.17 (~P2(f2(f2(a8,a1,f9(a4),f10(a4)),f2(f9(a4),f10(a4),f10(a4),f10(a4)),x19921,x19921),a4,f5(x19921,x19921))), % 124.50/125.17 inference(scs_inference,[],[1983,24,26,20])). % 124.50/125.17 cnf(1994,plain, % 124.50/125.17 (~E(f2(f9(a4),f10(a4),f10(a4),f10(a4)),f2(a8,a1,f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[1983,24,26,20,2])). % 124.50/125.17 cnf(1999,plain, % 124.50/125.17 (~E(f2(f10(a4),f9(a4),f10(a4),f10(a4)),f2(a8,a1,f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[1983,1976,1974,1936,1869,1691,195,24,26,20,2,16,14,3])). % 124.50/125.17 cnf(2008,plain, % 124.50/125.17 (~P2(f2(f2(f9(a4),f10(a4),f10(a4),f10(a4)),f2(a8,a1,f9(a4),f10(a4)),x20081,x20081),a4,f5(x20081,x20081))), % 124.50/125.17 inference(scs_inference,[],[1994,1999,24,26,20])). % 124.50/125.17 cnf(2010,plain, % 124.50/125.17 (~E(f2(a8,a1,f9(a4),f10(a4)),f2(f10(a4),f9(a4),f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[1994,1999,24,26,20,2])). % 124.50/125.17 cnf(2011,plain, % 124.50/125.17 (~P2(f2(f2(a8,a1,f9(a4),f10(a4)),f2(f9(a4),f10(a4),f10(a4),f10(a4)),f9(a4),f9(a4)),a4,f5(f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[1994,1999,1992,1690,24,26,20,2,16])). % 124.50/125.17 cnf(2012,plain, % 124.50/125.17 (~P2(f2(f2(a8,a1,f9(a4),f10(a4)),f2(f9(a4),f10(a4),f10(a4),f10(a4)),x20121,x20121),a4,f5(x20121,x20121))), % 124.50/125.17 inference(rename_variables,[],[1992])). % 124.50/125.17 cnf(2017,plain, % 124.50/125.17 (~E(f2(f10(a4),f9(a4),f9(a4),f10(a4)),f2(a8,a1,f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[1994,1999,1992,2012,185,1900,1690,24,26,20,2,16,14,3])). % 124.50/125.17 cnf(2025,plain, % 124.50/125.17 (~P2(f2(f2(a8,a1,f9(a4),f10(a4)),f2(f10(a4),f9(a4),f10(a4),f10(a4)),x20251,x20251),a4,f5(x20251,x20251))), % 124.50/125.17 inference(scs_inference,[],[2010,2017,24,26,20])). % 124.50/125.17 cnf(2027,plain, % 124.50/125.17 (~E(f2(a8,a1,f9(a4),f10(a4)),f2(f10(a4),f9(a4),f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2010,2017,24,26,20,2])). % 124.50/125.17 cnf(2028,plain, % 124.50/125.17 (~P2(f2(f2(a8,a1,f10(a4),f10(a4)),f2(f9(a4),f10(a4),f9(a4),f9(a4)),f9(a4),f9(a4)),a4,f5(f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2010,2017,1977,1691,24,26,20,2,16])). % 124.50/125.17 cnf(2030,plain, % 124.50/125.17 (E(f2(x20301,x20302,x20303,f10(a4)),f2(x20301,x20302,x20303,f9(a4)))), % 124.50/125.17 inference(rename_variables,[],[1869])). % 124.50/125.17 cnf(2032,plain, % 124.50/125.17 (~E(f2(a8,a1,f9(a4),f9(a4)),f2(f10(a4),f9(a4),f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2010,2017,2008,1977,1869,2030,1691,24,26,20,2,16,14,3])). % 124.50/125.17 cnf(2040,plain, % 124.50/125.17 (~E(f2(x20401,x20401,x20402,x20402),f2(f2(f10(a4),f9(a4),f10(a4),f10(a4)),f2(a8,a1,f9(a4),f9(a4)),x20402,x20402))), % 124.50/125.17 inference(scs_inference,[],[2032,24,26])). % 124.50/125.17 cnf(2041,plain, % 124.50/125.17 (~P2(f2(f2(a8,a1,f9(a4),f9(a4)),f2(f10(a4),f9(a4),f10(a4),f10(a4)),x20411,x20411),a4,f5(x20411,x20411))), % 124.50/125.17 inference(scs_inference,[],[2032,24,26,20])). % 124.50/125.17 cnf(2043,plain, % 124.50/125.17 (~E(f2(f10(a4),f9(a4),f10(a4),f10(a4)),f2(a8,a1,f9(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2032,24,26,20,2])). % 124.50/125.17 cnf(2044,plain, % 124.50/125.17 (~P2(f2(f2(a8,a1,f9(a4),f10(a4)),f2(f10(a4),f9(a4),f10(a4),f10(a4)),f9(a4),f9(a4)),a4,f5(f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2032,2025,1690,24,26,20,2,16])). % 124.50/125.17 cnf(2045,plain, % 124.50/125.17 (~P2(f2(f2(a8,a1,f9(a4),f10(a4)),f2(f10(a4),f9(a4),f10(a4),f10(a4)),x20451,x20451),a4,f5(x20451,x20451))), % 124.50/125.17 inference(rename_variables,[],[2025])). % 124.50/125.17 cnf(2050,plain, % 124.50/125.17 (~E(f2(a8,a1,f9(a4),f9(a4)),f2(f10(a4),f9(a4),f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2032,2027,2025,2045,1900,1869,1690,24,26,20,2,16,14,3])). % 124.50/125.17 cnf(2059,plain, % 124.50/125.17 (~E(f2(x20591,x20591,x20592,x20592),f2(f2(f10(a4),f9(a4),f9(a4),f10(a4)),f2(a8,a1,f9(a4),f9(a4)),x20592,x20592))), % 124.50/125.17 inference(scs_inference,[],[2050,24,26])). % 124.50/125.17 cnf(2060,plain, % 124.50/125.17 (~P2(f2(f2(f10(a4),f9(a4),f10(a4),f10(a4)),f2(a8,a1,f9(a4),f9(a4)),x20601,x20601),a4,f5(x20601,x20601))), % 124.50/125.17 inference(scs_inference,[],[2043,2050,24,26,20])). % 124.50/125.17 cnf(2062,plain, % 124.50/125.17 (~E(f2(f10(a4),f9(a4),f9(a4),f10(a4)),f2(a8,a1,f9(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2043,2050,24,26,20,2])). % 124.50/125.17 cnf(2064,plain, % 124.50/125.17 (~P2(f2(f2(a8,a1,f9(a4),f9(a4)),f2(f10(a4),f9(a4),f10(a4),f10(a4)),f10(a4),f9(a4)),a4,f5(f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2043,2050,2041,2011,1691,1900,24,26,20,2,16,14])). % 124.50/125.17 cnf(2067,plain, % 124.50/125.17 (~E(f2(f9(a4),f10(a4),f9(a4),f10(a4)),f2(a8,a1,f9(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2043,2050,2041,2011,198,1691,1900,24,26,20,2,16,14,3])). % 124.50/125.17 cnf(2076,plain, % 124.50/125.17 (~P2(f2(f2(f10(a4),f9(a4),f9(a4),f10(a4)),f2(a8,a1,f9(a4),f9(a4)),x20761,x20761),a4,f5(x20761,x20761))), % 124.50/125.17 inference(scs_inference,[],[2062,2067,24,26,20])). % 124.50/125.17 cnf(2078,plain, % 124.50/125.17 (~E(f2(a8,a1,f9(a4),f9(a4)),f2(f9(a4),f10(a4),f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2062,2067,24,26,20,2])). % 124.50/125.17 cnf(2080,plain, % 124.50/125.17 (~P2(f2(f2(f10(a4),f9(a4),f10(a4),f10(a4)),f2(a8,a1,f9(a4),f9(a4)),x20801,x20801),a4,f5(x20801,x20801))), % 124.50/125.17 inference(rename_variables,[],[2060])). % 124.50/125.17 cnf(2085,plain, % 124.50/125.17 (~E(f2(a1,a8,f9(a4),f10(a4)),f2(x20851,x20851,f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2062,2067,1233,2060,2080,1869,1689,1900,24,26,20,2,14,16,3])). % 124.50/125.17 cnf(2093,plain, % 124.50/125.17 (~P2(f2(f2(a8,a1,f9(a4),f9(a4)),f2(f9(a4),f10(a4),f9(a4),f10(a4)),x20931,x20931),a4,f5(x20931,x20931))), % 124.50/125.17 inference(scs_inference,[],[2078,306,24,26,20])). % 124.50/125.17 cnf(2095,plain, % 124.50/125.17 (~E(f2(x20951,x20951,f10(a4),f9(a4)),f2(a8,a1,f9(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2078,306,1245,24,26,20,2])). % 124.50/125.17 cnf(2100,plain, % 124.50/125.17 (~E(f2(f9(a4),f10(a4),f10(a4),f10(a4)),f2(a1,a8,f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2078,306,1245,1964,2076,2044,193,1691,1869,24,26,20,2,14,16,3])). % 124.50/125.17 cnf(2110,plain, % 124.50/125.17 (~P2(f2(f2(f9(a4),f10(a4),f10(a4),f10(a4)),f2(a1,a8,f10(a4),f9(a4)),x21101,x21101),a4,f5(x21101,x21101))), % 124.50/125.17 inference(scs_inference,[],[2100,24,26,20])). % 124.50/125.17 cnf(2112,plain, % 124.50/125.17 (~E(f2(a1,a8,f10(a4),f9(a4)),f2(f9(a4),f10(a4),f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2100,24,26,20,2])). % 124.50/125.17 cnf(2114,plain, % 124.50/125.17 (~P2(f2(f2(a8,a1,f9(a4),f9(a4)),f2(f9(a4),f10(a4),f9(a4),f10(a4)),x21141,x21141),a4,f5(x21141,x21141))), % 124.50/125.17 inference(rename_variables,[],[2093])). % 124.50/125.17 cnf(2116,plain, % 124.50/125.17 (~P2(f2(f2(a8,a1,f9(a4),f9(a4)),f2(f9(a4),f10(a4),f9(a4),f10(a4)),f9(a4),f9(a4)),a4,f5(f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2100,2093,2114,1708,1900,24,26,20,2,14,16])). % 124.50/125.17 cnf(2118,plain, % 124.50/125.17 (~E(f2(a1,a8,f10(a4),f9(a4)),f2(x21181,x21181,f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2100,1237,2093,2114,1708,1900,1869,24,26,20,2,14,16,3])). % 124.50/125.17 cnf(2126,plain, % 124.50/125.17 (~P2(f2(f2(a1,a8,f10(a4),f9(a4)),f2(f9(a4),f10(a4),f10(a4),f10(a4)),x21261,x21261),a4,f5(x21261,x21261))), % 124.50/125.17 inference(scs_inference,[],[2112,1249,24,26,20])). % 124.50/125.17 cnf(2128,plain, % 124.50/125.17 (~E(f2(x21281,x21281,f9(a4),f10(a4)),f2(a8,a1,f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2112,1249,24,26,20,2])). % 124.50/125.17 cnf(2131,plain, % 124.50/125.17 (~P2(f2(f2(f9(a4),f10(a4),f10(a4),f10(a4)),f2(a1,a8,f10(a4),f9(a4)),x21311,x21311),a4,f5(x21311,x21311))), % 124.50/125.17 inference(rename_variables,[],[2110])). % 124.50/125.17 cnf(2132,plain, % 124.50/125.17 (~P2(f2(f2(f9(a4),f10(a4),f10(a4),f10(a4)),f2(a1,a8,f10(a4),f9(a4)),f9(a4),f9(a4)),a4,f5(f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2112,1249,2110,2131,1690,1900,24,26,20,2,14,16])). % 124.50/125.17 cnf(2135,plain, % 124.50/125.17 (~E(f2(f10(a4),f9(a4),f9(a4),f9(a4)),f2(a8,a1,f9(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2112,1249,2095,2110,2131,190,1690,1900,24,26,20,2,14,16,3])). % 124.50/125.17 cnf(2144,plain, % 124.50/125.17 (~P2(f2(f2(f10(a4),f9(a4),f9(a4),f9(a4)),f2(a8,a1,f9(a4),f9(a4)),x21441,x21441),a4,f5(x21441,x21441))), % 124.50/125.17 inference(scs_inference,[],[2135,24,26,20])). % 124.50/125.17 cnf(2146,plain, % 124.50/125.17 (~E(f2(x21461,x21461,f10(a4),f9(a4)),f2(a1,a8,f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2135,2085,24,26,20,2])). % 124.50/125.17 cnf(2148,plain, % 124.50/125.17 (~P2(f2(f2(a1,a8,f10(a4),f9(a4)),f2(f9(a4),f10(a4),f10(a4),f10(a4)),x21481,x21481),a4,f5(x21481,x21481))), % 124.50/125.17 inference(rename_variables,[],[2126])). % 124.50/125.17 cnf(2153,plain, % 124.50/125.17 (~E(f2(f9(a4),f10(a4),f9(a4),f10(a4)),f2(f2(a1,a8,x21531,x21531),f2(x21532,x21532,x21531,x21531),f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2135,2085,1015,2126,2148,174,1689,1869,24,26,20,2,14,16,3])). % 124.50/125.17 cnf(2165,plain, % 124.50/125.17 (~P2(f2(f2(a1,a8,f10(a4),f9(a4)),f2(x21651,x21651,f9(a4),f10(a4)),x21652,x21652),a4,f5(x21652,x21652))), % 124.50/125.17 inference(scs_inference,[],[2118,24,26,20])). % 124.50/125.17 cnf(2167,plain, % 124.50/125.17 (~E(f2(a1,a8,f9(a4),f10(a4)),f2(x21671,x21671,f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2118,331,24,26,20,2])). % 124.50/125.17 cnf(2172,plain, % 124.50/125.17 (~E(f2(f10(a4),f9(a4),f10(a4),f10(a4)),f2(f2(a1,a8,x21721,x21721),f2(x21722,x21722,x21721,x21721),f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2118,331,2153,2144,2132,195,1691,1900,24,26,20,2,14,16,3])). % 124.50/125.17 cnf(2181,plain, % 124.50/125.17 (~P2(f2(f2(x21811,x21811,f9(a4),f10(a4)),f2(a8,a1,f10(a4),f10(a4)),x21812,x21812),a4,f5(x21812,x21812))), % 124.50/125.17 inference(scs_inference,[],[2128,2146,24,26,20])). % 124.50/125.17 cnf(2183,plain, % 124.50/125.17 (~E(f2(f2(a1,a8,x21831,x21831),f2(x21832,x21832,x21831,x21831),f9(a4),f10(a4)),f2(f10(a4),f9(a4),f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2128,2146,2172,24,26,20,2])). % 124.50/125.17 cnf(2185,plain, % 124.50/125.17 (~P2(f2(f2(a1,a8,f10(a4),f9(a4)),f2(x21851,x21851,f9(a4),f10(a4)),x21852,x21852),a4,f5(x21852,x21852))), % 124.50/125.17 inference(rename_variables,[],[2165])). % 124.50/125.17 cnf(2189,plain, % 124.50/125.17 (~E(f2(f10(a4),f9(a4),f9(a4),f9(a4)),f2(a1,a8,f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2128,2146,2172,2165,2185,190,1708,1869,24,26,20,2,14,16,3])). % 124.50/125.17 cnf(2199,plain, % 124.50/125.17 (~P2(f2(f2(f10(a4),f9(a4),f9(a4),f9(a4)),f2(a1,a8,f9(a4),f10(a4)),x21991,x21991),a4,f5(x21991,x21991))), % 124.50/125.17 inference(scs_inference,[],[2189,24,26,20])). % 124.50/125.17 cnf(2201,plain, % 124.50/125.17 (~E(f2(a1,a8,f9(a4),f10(a4)),f2(f10(a4),f9(a4),f9(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2189,24,26,20,2])). % 124.50/125.17 cnf(2204,plain, % 124.50/125.17 (~P2(f2(f2(x22041,x22041,f9(a4),f10(a4)),f2(a8,a1,f10(a4),f10(a4)),x22042,x22042),a4,f5(x22042,x22042))), % 124.50/125.17 inference(rename_variables,[],[2181])). % 124.50/125.17 cnf(2205,plain, % 124.50/125.17 (~P2(f2(f2(x22051,x22051,f9(a4),f10(a4)),f2(a8,a1,f10(a4),f10(a4)),f9(a4),f9(a4)),a4,f5(f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2189,2181,2204,1690,1900,24,26,20,2,14,16])). % 124.50/125.17 cnf(2208,plain, % 124.50/125.17 (~E(f2(f9(a4),f10(a4),f10(a4),f9(a4)),f2(a1,a8,f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2189,2181,2204,188,1690,1900,24,26,20,2,14,16,3])). % 124.50/125.17 cnf(2217,plain, % 124.50/125.17 (~P2(f2(f2(a1,a8,f9(a4),f10(a4)),f2(f10(a4),f9(a4),f9(a4),f9(a4)),x22171,x22171),a4,f5(x22171,x22171))), % 124.50/125.17 inference(scs_inference,[],[2201,2208,24,26,20])). % 124.50/125.17 cnf(2219,plain, % 124.50/125.17 (~E(f2(a1,a8,f9(a4),f10(a4)),f2(f9(a4),f10(a4),f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2201,2208,24,26,20,2])). % 124.50/125.17 cnf(2221,plain, % 124.50/125.17 (~P2(f2(f2(f10(a4),f9(a4),f9(a4),f9(a4)),f2(a1,a8,f9(a4),f10(a4)),x22211,x22211),a4,f5(x22211,x22211))), % 124.50/125.17 inference(rename_variables,[],[2199])). % 124.50/125.17 cnf(2222,plain, % 124.50/125.17 (E(f2(x22221,x22222,x22223,f10(a4)),f2(x22221,x22222,x22223,f9(a4)))), % 124.50/125.17 inference(rename_variables,[],[1869])). % 124.50/125.17 cnf(2226,plain, % 124.50/125.17 (~E(f2(a1,a8,f9(a4),f9(a4)),f2(x22261,x22261,f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2201,2208,2167,2199,2221,1689,1869,2222,24,26,20,2,14,16,3])). % 124.50/125.17 cnf(2236,plain, % 124.50/125.17 (~P2(f2(f2(a1,a8,f9(a4),f10(a4)),f2(f9(a4),f10(a4),f10(a4),f9(a4)),x22361,x22361),a4,f5(x22361,x22361))), % 124.50/125.17 inference(scs_inference,[],[2219,2226,24,20])). % 124.50/125.17 cnf(2239,plain, % 124.50/125.17 (~E(f2(x22391,x22391,f10(a4),f10(a4)),f2(a1,a8,f9(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2219,2226,24,20,26,2])). % 124.50/125.17 cnf(2244,plain, % 124.50/125.17 (~E(f2(f9(a4),f10(a4),f9(a4),f10(a4)),f2(f2(x22441,x22441,x22442,x22442),f2(a1,a8,x22442,x22442),f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2219,2226,1019,2217,2205,174,1691,1900,24,20,26,2,14,16,3])). % 124.50/125.17 cnf(2256,plain, % 124.50/125.17 (~E(f2(f2(x22561,x22561,x22562,x22562),f2(a1,a8,x22562,x22562),f9(a4),f10(a4)),f2(f9(a4),f10(a4),f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2239,2183,2244,24,20,26,2])). % 124.50/125.17 cnf(2258,plain, % 124.50/125.17 (~P2(f2(f2(a1,a8,f9(a4),f10(a4)),f2(f9(a4),f10(a4),f10(a4),f9(a4)),x22581,x22581),a4,f5(x22581,x22581))), % 124.50/125.17 inference(rename_variables,[],[2236])). % 124.50/125.17 cnf(2259,plain, % 124.50/125.17 (E(f2(x22591,x22592,x22593,f10(a4)),f2(x22591,x22592,x22593,f9(a4)))), % 124.50/125.17 inference(rename_variables,[],[1869])). % 124.50/125.17 cnf(2262,plain, % 124.50/125.17 (~E(f2(f2(a1,a8,x22621,x22621),f2(x22622,x22622,x22621,x22621),f9(a4),f9(a4)),f2(f10(a4),f9(a4),f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2239,2183,2244,2236,2258,1700,1869,2259,24,20,26,2,14,16,3])). % 124.50/125.17 cnf(2269,plain, % 124.50/125.17 (~E(f2(f10(a4),f9(a4),f10(a4),f10(a4)),f2(f2(a1,a8,x22691,x22691),f2(x22692,x22692,x22691,x22691),f9(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2262,2])). % 124.50/125.17 cnf(2275,plain, % 124.50/125.17 (~E(f2(f9(a4),f10(a4),f10(a4),f9(a4)),f2(f2(a1,a8,x22751,x22751),f2(x22752,x22752,x22751,x22751),f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2256,2262,1002,193,2,24,20,26,3])). % 124.50/125.17 cnf(2287,plain, % 124.50/125.17 (~E(f2(f2(a1,a8,x22871,x22871),f2(x22872,x22872,x22871,x22871),f10(a4),f9(a4)),f2(f9(a4),f10(a4),f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2275,2])). % 124.50/125.17 cnf(2290,plain, % 124.50/125.17 (~P2(f2(a8,a1,x22901,x22901),a4,f5(x22901,x22901))), % 124.50/125.17 inference(scs_inference,[],[63,2275,1254,2,24,20])). % 124.50/125.17 cnf(2293,plain, % 124.50/125.17 (~E(f2(f9(a4),f10(a4),f9(a4),f10(a4)),f2(f2(a1,a8,x22931,x22931),f2(x22932,x22932,x22931,x22931),f9(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[63,2269,2275,1254,198,2,24,20,26,3])). % 124.50/125.17 cnf(2306,plain, % 124.50/125.17 (~E(f2(f2(a1,a8,x23061,x23061),f2(x23062,x23062,x23061,x23061),f9(a4),f9(a4)),f2(f9(a4),f10(a4),f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2293,1258,24,2])). % 124.50/125.17 cnf(2310,plain, % 124.50/125.17 (~E(f2(f10(a4),f9(a4),f9(a4),f10(a4)),f2(f2(a8,a1,x23101,x23101),f2(x23102,x23102,x23101,x23101),f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2287,2293,1022,1258,190,24,2,20,26,3])). % 124.50/125.17 cnf(2313,plain, % 124.50/125.17 (~P2(f2(a8,a1,f10(a4),f9(a4)),a4,f5(f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2290,2287,2293,1022,1258,190,1900,24,2,20,26,3,14])). % 124.50/125.17 cnf(2323,plain, % 124.50/125.17 (~E(f2(f2(a8,a1,x23231,x23231),f2(x23232,x23232,x23231,x23231),f9(a4),f10(a4)),f2(f10(a4),f9(a4),f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2310,360,24,2])). % 124.50/125.17 cnf(2327,plain, % 124.50/125.17 (~E(f2(f2(a1,a8,x23271,x23271),f2(x23272,x23272,x23271,x23271),f9(a4),f10(a4)),f2(f9(a4),f10(a4),f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2306,2310,360,1900,24,2,20,26,3])). % 124.50/125.17 cnf(2340,plain, % 124.50/125.17 (~E(f2(f2(x23401,x23401,x23402,x23402),f2(a1,a8,x23402,x23402),f10(a4),f9(a4)),f2(x23403,x23403,f9(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2327,1006,24,2])). % 124.50/125.17 cnf(2344,plain, % 124.50/125.17 (~E(f2(f10(a4),f9(a4),f10(a4),f9(a4)),f2(f2(x23441,x23441,x23442,x23442),f2(a1,a8,x23442,x23442),f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2323,2327,1006,171,24,2,20,26,3])). % 124.50/125.17 cnf(2355,plain, % 124.50/125.17 (~E(f2(f2(x23551,x23551,x23552,x23552),f2(a1,a8,x23552,x23552),f10(a4),f9(a4)),f2(f10(a4),f9(a4),f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2344,368,24,2])). % 124.50/125.17 cnf(2359,plain, % 124.50/125.17 (~E(f2(f9(a4),f10(a4),f9(a4),f9(a4)),f2(f2(x23591,x23591,x23592,x23592),f2(a1,a8,x23592,x23592),f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2344,368,198,24,2,20,26,3])). % 124.50/125.17 cnf(2369,plain, % 124.50/125.17 (~E(f2(x23691,x23691,x23692,x23692),f2(f2(a1,a8,x23693,x23693),f2(f9(a4),f10(a4),x23693,x23693),x23692,x23692))), % 124.50/125.17 inference(scs_inference,[],[611,24])). % 124.50/125.17 cnf(2371,plain, % 124.50/125.17 (~E(f2(f2(x23711,x23711,x23712,x23712),f2(a1,a8,x23712,x23712),f10(a4),f9(a4)),f2(f9(a4),f10(a4),f9(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2359,611,24,2])). % 124.50/125.17 cnf(2375,plain, % 124.50/125.17 (~E(f2(f9(a4),f10(a4),f10(a4),f9(a4)),f2(f2(a8,a1,x23751,x23751),f2(x23752,x23752,x23751,x23751),f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2355,2359,1011,611,193,24,2,20,26,3])). % 124.50/125.17 cnf(2387,plain, % 124.50/125.17 (~E(f2(x23871,x23871,x23872,x23872),f2(f2(a1,a8,x23873,x23873),f2(f10(a4),f9(a4),x23873,x23873),x23872,x23872))), % 124.50/125.17 inference(scs_inference,[],[615,24])). % 124.50/125.17 cnf(2389,plain, % 124.50/125.17 (~E(f2(f2(a8,a1,x23891,x23891),f2(x23892,x23892,x23891,x23891),f10(a4),f9(a4)),f2(f9(a4),f10(a4),f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2375,615,24,2])). % 124.50/125.17 cnf(2393,plain, % 124.50/125.17 (~E(f2(f2(x23931,x23931,x23932,x23932),f2(a1,a8,x23932,x23932),f10(a4),f10(a4)),f2(f9(a4),f10(a4),f9(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2371,2375,615,1900,24,2,20,26,3])). % 124.50/125.17 cnf(2408,plain, % 124.50/125.17 (~E(f2(f9(a4),f10(a4),f9(a4),f9(a4)),f2(f2(x24081,x24081,x24082,x24082),f2(a1,a8,x24082,x24082),f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2393,24,2])). % 124.50/125.17 cnf(2412,plain, % 124.50/125.17 (~E(f2(f10(a4),f10(a4),f9(a4),f10(a4)),f2(f2(a1,a8,x24121,x24121),f2(f9(a4),f10(a4),x24121,x24121),f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2389,2393,2369,179,24,2,20,26,3])). % 124.50/125.17 cnf(2423,plain, % 124.50/125.17 (~E(f2(x24231,x24231,x24232,x24232),f2(f2(a8,a1,x24233,x24233),f2(f10(a4),f9(a4),x24233,x24233),x24232,x24232))), % 124.50/125.17 inference(scs_inference,[],[629,24])). % 124.50/125.17 cnf(2425,plain, % 124.50/125.17 (~E(f2(f2(a1,a8,x24251,x24251),f2(f9(a4),f10(a4),x24251,x24251),f10(a4),f10(a4)),f2(f10(a4),f10(a4),f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2412,629,24,2])). % 124.50/125.17 cnf(2426,plain, % 124.50/125.17 (~P2(f2(f2(f9(a4),f10(a4),f9(a4),f9(a4)),f2(f2(x24261,x24261,x24262,x24262),f2(a1,a8,x24262,x24262),f10(a4),f10(a4)),x24263,x24263),a4,f5(x24263,x24263))), % 124.50/125.17 inference(scs_inference,[],[2408,2412,629,24,2,20])). % 124.50/125.17 cnf(2429,plain, % 124.50/125.17 (~E(f2(f10(a4),f9(a4),f10(a4),f9(a4)),f2(f2(x24291,x24291,x24292,x24292),f2(a1,a8,x24292,x24292),f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2408,2412,629,195,24,2,20,26,3])). % 124.50/125.17 cnf(2442,plain, % 124.50/125.17 (~E(f2(x24421,x24421,x24422,x24422),f2(f2(a8,a1,x24423,x24423),f2(f9(a4),f10(a4),x24423,x24423),x24422,x24422))), % 124.50/125.17 inference(scs_inference,[],[639,24])). % 124.50/125.17 cnf(2444,plain, % 124.50/125.17 (~E(f2(f2(x24441,x24441,x24442,x24442),f2(a1,a8,x24442,x24442),f10(a4),f10(a4)),f2(f10(a4),f9(a4),f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2429,639,24,2])). % 124.50/125.17 cnf(2445,plain, % 124.50/125.17 (~P2(f2(f2(f10(a4),f9(a4),f10(a4),f9(a4)),f2(f2(x24451,x24451,x24452,x24452),f2(a1,a8,x24452,x24452),f10(a4),f10(a4)),x24453,x24453),a4,f5(x24453,x24453))), % 124.50/125.17 inference(scs_inference,[],[2429,639,24,2,20])). % 124.50/125.17 cnf(2448,plain, % 124.50/125.17 (~E(f2(f10(a4),f10(a4),f9(a4),f9(a4)),f2(f2(x24481,x24481,x24482,x24482),f2(a1,a8,x24482,x24482),f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2429,639,174,24,2,20,26,3])). % 124.50/125.17 cnf(2461,plain, % 124.50/125.17 (~E(f2(f2(x24611,x24611,x24612,x24612),f2(a1,a8,x24612,x24612),f10(a4),f10(a4)),f2(f10(a4),f10(a4),f9(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2448,308,24,2])). % 124.50/125.17 cnf(2467,plain, % 124.50/125.17 (~E(f2(f9(a4),f9(a4),f9(a4),f9(a4)),f2(f2(x24671,x24671,x24672,x24672),f2(a1,a8,x24672,x24672),f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2444,2448,2426,308,106,1708,24,2,20,26,16,3])). % 124.50/125.17 cnf(2481,plain, % 124.50/125.17 (~E(f2(f2(x24811,x24811,x24812,x24812),f2(a1,a8,x24812,x24812),f10(a4),f10(a4)),f2(f9(a4),f9(a4),f9(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2467,316,24,2])). % 124.50/125.17 cnf(2482,plain, % 124.50/125.17 (~P2(f2(f2(f2(x24821,x24821,x24822,x24822),f2(a1,a8,x24822,x24822),f10(a4),f10(a4)),f2(f10(a4),f10(a4),f9(a4),f9(a4)),x24823,x24823),a4,f5(x24823,x24823))), % 124.50/125.17 inference(scs_inference,[],[2461,2467,316,24,2,20])). % 124.50/125.17 cnf(2485,plain, % 124.50/125.17 (~P2(f2(f2(f10(a4),f9(a4),f10(a4),f9(a4)),f2(f2(x24851,x24851,x24852,x24852),f2(a1,a8,x24852,x24852),f10(a4),f10(a4)),f9(a4),f9(a4)),a4,f5(f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2461,2467,2445,316,1690,24,2,20,26,16])). % 124.50/125.17 cnf(2488,plain, % 124.50/125.17 (~E(f2(f10(a4),f9(a4),f9(a4),f10(a4)),f2(f2(a1,a8,x24881,x24881),f2(f10(a4),f9(a4),x24881,x24881),f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2461,2467,2387,2445,316,190,1690,24,2,20,26,16,3])). % 124.50/125.17 cnf(2502,plain, % 124.50/125.17 (~E(f2(f2(a1,a8,x25021,x25021),f2(f10(a4),f9(a4),x25021,x25021),f10(a4),f10(a4)),f2(f10(a4),f9(a4),f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2481,2488,401,24,20,2])). % 124.50/125.17 cnf(2505,plain, % 124.50/125.17 (~E(f2(f2(x25051,x25051,x25052,x25052),f2(a1,a8,x25052,x25052),f10(a4),f10(a4)),f2(x25053,x25053,f9(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2481,2340,2488,2485,401,1691,1900,24,20,2,26,16,3])). % 124.50/125.17 cnf(2517,plain, % 124.50/125.17 (~P2(f2(f2(f2(x25171,x25171,x25172,x25172),f2(a1,a8,x25172,x25172),f10(a4),f10(a4)),f2(x25173,x25173,f9(a4),f9(a4)),x25174,x25174),a4,f5(x25174,x25174))), % 124.50/125.17 inference(scs_inference,[],[2505,24,20])). % 124.50/125.17 cnf(2519,plain, % 124.50/125.17 (~E(f2(x25191,x25191,f9(a4),f9(a4)),f2(f2(x25192,x25192,x25193,x25193),f2(a1,a8,x25193,x25193),f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2505,24,20,2])). % 124.50/125.17 cnf(2523,plain, % 124.50/125.17 (~E(f2(f10(a4),f9(a4),f10(a4),f9(a4)),f2(f2(a8,a1,x25231,x25231),f2(f10(a4),f9(a4),x25231,x25231),f9(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2505,2423,2482,171,1700,24,20,2,26,16,3])). % 124.50/125.17 cnf(2535,plain, % 124.50/125.17 (~P2(f2(f2(x25351,x25351,f9(a4),f9(a4)),f2(f2(x25352,x25352,x25353,x25353),f2(a1,a8,x25353,x25353),f10(a4),f10(a4)),x25354,x25354),a4,f5(x25354,x25354))), % 124.50/125.17 inference(scs_inference,[],[2519,413,24,20])). % 124.50/125.17 cnf(2537,plain, % 124.50/125.17 (~E(f2(f2(a8,a1,x25371,x25371),f2(f10(a4),f9(a4),x25371,x25371),f9(a4),f9(a4)),f2(f10(a4),f9(a4),f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2519,2523,413,24,20,2])). % 124.50/125.17 cnf(2541,plain, % 124.50/125.17 (~E(f2(f2(a1,a8,x25411,x25411),f2(f9(a4),f10(a4),x25411,x25411),f10(a4),f9(a4)),f2(f10(a4),f10(a4),f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2519,2425,2523,2517,413,1708,1869,24,20,2,26,16,3])). % 124.50/125.17 cnf(2557,plain, % 124.50/125.17 (~E(f2(f10(a4),f10(a4),f9(a4),f10(a4)),f2(f2(a1,a8,x25571,x25571),f2(f9(a4),f10(a4),x25571,x25571),f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2502,2541,24,20,2])). % 124.50/125.17 cnf(2559,plain, % 124.50/125.17 (~P2(f2(f2(x25591,x25591,f9(a4),f9(a4)),f2(f2(x25592,x25592,x25593,x25593),f2(a1,a8,x25593,x25593),f10(a4),f10(a4)),f9(a4),f9(a4)),a4,f5(f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2502,2541,2442,2535,1690,24,20,2,26,16])). % 124.50/125.17 cnf(2562,plain, % 124.50/125.17 (~E(f2(f9(a4),f10(a4),f9(a4),f10(a4)),f2(f2(a8,a1,x25621,x25621),f2(f9(a4),f10(a4),x25621,x25621),f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2502,2541,2442,2535,174,1690,24,20,2,26,16,3])). % 124.50/125.17 cnf(2576,plain, % 124.50/125.17 (~E(f2(f2(a8,a1,x25761,x25761),f2(f9(a4),f10(a4),x25761,x25761),f10(a4),f10(a4)),f2(f9(a4),f10(a4),f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2537,2562,418,24,20,2])). % 124.50/125.17 cnf(2579,plain, % 124.50/125.17 (~E(f2(f2(a8,a1,x25791,x25791),f2(f10(a4),f9(a4),x25791,x25791),f9(a4),f10(a4)),f2(f10(a4),f9(a4),f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2537,2562,2559,418,1691,1900,24,20,2,26,16,3])). % 124.50/125.17 cnf(2581,plain, % 124.50/125.17 (~P2(f2(f2(a1,a8,f10(a4),f10(a4)),f2(f9(a4),f10(a4),f9(a4),f10(a4)),f9(a4),f10(a4)),a4,f5(f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2537,2562,1960,2559,418,1691,1869,1900,24,20,2,26,16,3,14])). % 124.50/125.17 cnf(2594,plain, % 124.50/125.17 (~E(f2(f10(a4),f9(a4),f10(a4),f9(a4)),f2(f2(a8,a1,x25941,x25941),f2(f10(a4),f9(a4),x25941,x25941),f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2557,2579,24,20,2])). % 124.50/125.17 cnf(2596,plain, % 124.50/125.17 (~P2(f2(f2(a1,a8,f10(a4),f9(a4)),f2(f9(a4),f10(a4),f9(a4),f9(a4)),f9(a4),f9(a4)),a4,f5(f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2557,2579,1885,1875,1689,24,20,2,26,16])). % 124.50/125.17 cnf(2598,plain, % 124.50/125.17 (~E(f2(f9(a4),f9(a4),f9(a4),f10(a4)),f2(f2(a1,a8,x25981,x25981),f2(f9(a4),f10(a4),x25981,x25981),f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2557,2579,1885,1875,106,1689,24,20,2,26,16,3])). % 124.50/125.17 cnf(2610,plain, % 124.50/125.17 (~E(f2(f2(a1,a8,x26101,x26101),f2(f9(a4),f10(a4),x26101,x26101),f10(a4),f9(a4)),f2(f9(a4),f9(a4),f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2576,2598,538,24,20,2])). % 124.50/125.17 cnf(2613,plain, % 124.50/125.17 (~E(f2(f2(a8,a1,x26131,x26131),f2(f9(a4),f10(a4),x26131,x26131),f10(a4),f9(a4)),f2(f9(a4),f10(a4),f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2576,2598,2596,538,1699,1869,24,20,2,26,16,3])). % 124.50/125.17 cnf(2634,plain, % 124.50/125.17 (~E(f2(f9(a4),f10(a4),f9(a4),f10(a4)),f2(f2(a8,a1,x26341,x26341),f2(f9(a4),f10(a4),x26341,x26341),f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2594,2613,24,20,2])). % 124.50/125.17 cnf(2636,plain, % 124.50/125.17 (~P2(f2(f2(a1,a8,f10(a4),f9(a4)),f2(f9(a4),f10(a4),f9(a4),f9(a4)),f9(a4),f10(a4)),a4,f5(f9(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2594,2613,1887,1877,1700,24,20,2,26,16])). % 124.50/125.17 cnf(2637,plain, % 124.50/125.17 (~E(f2(f9(a4),f10(a4),f9(a4),f9(a4)),f2(f2(a8,a1,x26371,x26371),f2(f10(a4),f9(a4),x26371,x26371),f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2594,2613,1887,1877,198,1700,24,20,2,26,16,3])). % 124.50/125.17 cnf(2650,plain, % 124.50/125.17 (~E(f2(f2(a8,a1,x26501,x26501),f2(f10(a4),f9(a4),x26501,x26501),f9(a4),f10(a4)),f2(f9(a4),f10(a4),f9(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2610,2637,626,24,20,2])). % 124.50/125.17 cnf(2653,plain, % 124.50/125.17 (~E(f2(f2(a1,a8,x26531,x26531),f2(f9(a4),f10(a4),x26531,x26531),f10(a4),f10(a4)),f2(f9(a4),f9(a4),f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2610,2637,1961,626,1700,1900,24,20,2,26,16,3])). % 124.50/125.17 cnf(2667,plain, % 124.50/125.17 (~E(f2(f9(a4),f9(a4),f9(a4),f10(a4)),f2(f2(a1,a8,x26671,x26671),f2(f9(a4),f10(a4),x26671,x26671),f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2634,2653,24,20,2])). % 124.50/125.17 cnf(2670,plain, % 124.50/125.17 (~E(f2(f10(a4),f9(a4),f10(a4),f10(a4)),f2(f2(a8,a1,x26701,x26701),f2(f9(a4),f10(a4),x26701,x26701),f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2634,2653,2581,1901,195,1699,24,20,2,26,16,3])). % 124.50/125.17 cnf(2672,plain, % 124.50/125.17 (~P2(f2(f2(a8,a1,f10(a4),f10(a4)),f2(f9(a4),f10(a4),f9(a4),f9(a4)),f9(a4),f10(a4)),a4,f5(f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2634,2653,2581,2028,1901,195,1699,1869,24,20,2,26,16,3,14])). % 124.50/125.17 cnf(2682,plain, % 124.50/125.17 (~E(f2(f2(a8,a1,x26821,x26821),f2(f9(a4),f10(a4),x26821,x26821),f10(a4),f9(a4)),f2(f10(a4),f9(a4),f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2650,2670,969,24,20,2])). % 124.50/125.17 cnf(2685,plain, % 124.50/125.17 (~E(f2(f2(a8,a1,x26851,x26851),f2(f10(a4),f9(a4),x26851,x26851),f9(a4),f9(a4)),f2(f9(a4),f10(a4),f9(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2650,2670,2064,969,1700,1869,24,20,2,26,16,3])). % 124.50/125.17 cnf(2701,plain, % 124.50/125.17 (~E(f2(f9(a4),f10(a4),f9(a4),f9(a4)),f2(f2(a8,a1,x27011,x27011),f2(f10(a4),f9(a4),x27011,x27011),f9(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2667,2685,24,20,2])). % 124.50/125.17 cnf(2714,plain, % 124.50/125.17 (~E(f2(x27141,x27141,x27142,x27142),f2(f2(a8,a1,f10(a4),f10(a4)),f2(f10(a4),f9(a4),f9(a4),f10(a4)),x27142,x27142))), % 124.50/125.17 inference(scs_inference,[],[976,24])). % 124.50/125.17 cnf(2721,plain, % 124.50/125.17 (~E(f2(f2(a8,a1,x27211,x27211),f2(f9(a4),f10(a4),x27211,x27211),f10(a4),f10(a4)),f2(f10(a4),f9(a4),f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2682,799,2672,1927,976,1699,1900,24,20,2,26,16,3])). % 124.50/125.17 cnf(2723,plain, % 124.50/125.17 (~P2(f2(f2(a1,a8,f10(a4),f9(a4)),f2(f9(a4),f10(a4),f9(a4),f9(a4)),f10(a4),f10(a4)),a4,f5(f9(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2682,799,2636,2672,1927,976,1699,1900,128,24,20,2,26,16,3,14])). % 124.50/125.17 cnf(2733,plain, % 124.50/125.17 (~E(f2(f10(a4),f9(a4),f10(a4),f10(a4)),f2(f2(a8,a1,x27331,x27331),f2(f9(a4),f10(a4),x27331,x27331),f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2701,2721,24,20,2])). % 124.50/125.17 cnf(2735,plain, % 124.50/125.17 (~P2(f2(f2(a8,a1,f9(a4),f9(a4)),f2(f9(a4),f10(a4),f9(a4),f10(a4)),f9(a4),f9(a4)),a4,f5(f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2701,2721,2116,1930,1689,24,20,2,26,16])). % 124.50/125.17 cnf(2745,plain, % 124.50/125.17 (~E(f2(x27451,x27451,x27452,x27452),f2(f2(a8,a1,f9(a4),f9(a4)),f2(f10(a4),f9(a4),f10(a4),f9(a4)),x27452,x27452))), % 124.50/125.17 inference(scs_inference,[],[983,24])). % 124.50/125.17 cnf(2753,plain, % 124.50/125.17 (E(f2(x27531,x27532,x27533,f9(a4)),f2(x27531,x27532,x27533,f10(a4)))), % 124.50/125.17 inference(rename_variables,[],[1900])). % 124.50/125.17 cnf(2754,plain, % 124.50/125.17 (~P2(f2(f2(a1,a8,f10(a4),f9(a4)),f2(f9(a4),f10(a4),f9(a4),f9(a4)),f10(a4),f9(a4)),a4,f5(f9(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2733,802,2723,2735,1948,983,1699,1900,2753,24,20,2,26,16,3,14])). % 124.50/125.17 cnf(2761,plain, % 124.50/125.17 (~E(f2(x27611,x27611,x27612,x27612),f2(f2(f9(a4),f10(a4),f9(a4),f10(a4)),f2(a8,a1,f10(a4),f10(a4)),x27612,x27612))), % 124.50/125.17 inference(scs_inference,[],[1880,24])). % 124.50/125.17 cnf(2766,plain, % 124.50/125.17 (~E(f2(x27661,x27661,x27662,x27662),f2(f2(f2(f9(a4),f10(a4),f9(a4),f9(a4)),f2(a8,a1,f10(a4),f10(a4)),x27663,x27663),f2(x27664,x27664,x27663,x27663),x27662,x27662))), % 124.50/125.17 inference(scs_inference,[],[1379,1952,289,1880,24,20,2,26])). % 124.50/125.17 cnf(2767,plain, % 124.50/125.17 (~P2(f2(f2(a1,a8,f10(a4),f9(a4)),f2(f9(a4),f10(a4),f9(a4),f9(a4)),f10(a4),f9(a4)),a4,f5(f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[1379,2754,1952,289,1880,1708,24,20,2,26,16])). % 124.50/125.17 cnf(2799,plain, % 124.50/125.17 (~E(f2(x27991,x27991,x27992,x27992),f2(f2(f9(a4),f10(a4),f10(a4),f9(a4)),f2(a1,a8,f10(a4),f9(a4)),x27992,x27992))), % 124.50/125.17 inference(scs_inference,[],[291,24])). % 124.50/125.17 cnf(2801,plain, % 124.50/125.17 (~P2(f2(f2(a1,a8,f10(a4),f9(a4)),f2(f10(a4),f9(a4),f9(a4),f9(a4)),x28011,x28011),a4,f5(x28011,x28011))), % 124.50/125.17 inference(scs_inference,[],[407,291,24,20])). % 124.50/125.17 cnf(2818,plain, % 124.50/125.17 (~E(f2(x28181,x28181,x28182,x28182),f2(f2(f10(a4),f9(a4),f9(a4),f9(a4)),f2(a1,a8,f10(a4),f9(a4)),x28182,x28182))), % 124.50/125.17 inference(scs_inference,[],[355,24])). % 124.50/125.17 cnf(2824,plain, % 124.50/125.17 (~P2(f2(f2(a1,a8,f10(a4),f9(a4)),f2(f10(a4),f9(a4),f9(a4),f9(a4)),f9(a4),f9(a4)),a4,f5(f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[2801,1077,2040,536,355,1690,24,20,2,26,16])). % 124.50/125.17 cnf(2842,plain, % 124.50/125.17 (~P2(f2(f2(a1,a8,f9(a4),f10(a4)),f2(f10(a4),f9(a4),f9(a4),f10(a4)),x28421,x28421),a4,f5(x28421,x28421))), % 124.50/125.17 inference(scs_inference,[],[539,351,24,20])). % 124.50/125.17 cnf(2867,plain, % 124.50/125.17 (~P2(f2(f2(a1,a8,f10(a4),f9(a4)),f2(f10(a4),f9(a4),f9(a4),f9(a4)),f9(a4),f9(a4)),a4,f5(f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[2842,1341,2824,2059,346,1691,1869,26,24,20,2,14,16])). % 124.50/125.17 cnf(3106,plain, % 124.50/125.17 (~E(f2(x31061,x31061,x31062,x31062),f2(f2(f9(a4),f10(a4),x31063,x31063),f2(a1,a8,x31063,x31063),x31062,x31062))), % 124.50/125.17 inference(scs_inference,[],[1034,2714,294,2,26,24])). % 124.50/125.17 cnf(3124,plain, % 124.50/125.17 (~E(f2(x31241,x31241,x31242,x31242),f2(f2(f2(f9(a4),f10(a4),x31243,x31243),f2(a1,a8,x31243,x31243),x31244,x31244),f2(x31245,x31245,x31244,x31244),x31242,x31242))), % 124.50/125.17 inference(scs_inference,[],[3106,2,26])). % 124.50/125.17 cnf(3144,plain, % 124.50/125.17 (~E(f2(f2(f2(f9(a4),f10(a4),x31441,x31441),f2(a1,a8,x31441,x31441),x31442,x31442),f2(x31443,x31443,x31442,x31442),x31444,x31444),f2(x31445,x31445,x31444,x31444))), % 124.50/125.17 inference(scs_inference,[],[3124,2])). % 124.50/125.17 cnf(3166,plain, % 124.50/125.17 (~E(f2(x31661,x31661,x31662,x31662),f2(f2(f10(a4),f9(a4),x31663,x31663),f2(a1,a8,x31663,x31663),x31662,x31662))), % 124.50/125.17 inference(scs_inference,[],[1116,2745,297,2,26,24])). % 124.50/125.17 cnf(3168,plain, % 124.50/125.17 (~P2(f2(f2(f2(f2(f9(a4),f10(a4),x31681,x31681),f2(a1,a8,x31681,x31681),x31682,x31682),f2(x31683,x31683,x31682,x31682),x31684,x31684),f2(x31685,x31685,x31684,x31684),x31686,x31686),a4,f5(x31686,x31686))), % 124.50/125.17 inference(scs_inference,[],[3144,1116,2745,297,2,26,24,20])). % 124.50/125.17 cnf(3190,plain, % 124.50/125.17 (~E(f2(f2(f10(a4),f9(a4),x31901,x31901),f2(a1,a8,x31901,x31901),x31902,x31902),f2(x31903,x31903,x31902,x31902))), % 124.50/125.17 inference(scs_inference,[],[3166,2])). % 124.50/125.17 cnf(3191,plain, % 124.50/125.17 (~E(f2(x31911,x31911,x31912,x31912),f2(f2(f2(f10(a4),f9(a4),x31913,x31913),f2(a1,a8,x31913,x31913),x31914,x31914),f2(x31915,x31915,x31914,x31914),x31912,x31912))), % 124.50/125.17 inference(scs_inference,[],[3166,2,26])). % 124.50/125.17 cnf(3194,plain, % 124.50/125.17 (~P2(f2(f2(x31941,x31941,x31942,x31942),f2(f2(f10(a4),f9(a4),x31943,x31943),f2(a1,a8,x31943,x31943),x31942,x31942),x31944,x31944),a4,f5(x31944,x31944))), % 124.50/125.17 inference(scs_inference,[],[3166,2,26,24,20])). % 124.50/125.17 cnf(3198,plain, % 124.50/125.17 (~E(f2(f9(a4),f10(a4),x31981,x31981),f2(f2(f10(a4),f9(a4),x31982,x31982),f2(a1,a8,x31982,x31982),x31981,x31981))), % 124.50/125.17 inference(scs_inference,[],[82,3166,3168,1708,2,26,24,20,16,3])). % 124.50/125.17 cnf(3208,plain, % 124.50/125.17 (~E(f2(f2(f2(f10(a4),f9(a4),x32081,x32081),f2(a1,a8,x32081,x32081),x32082,x32082),f2(x32083,x32083,x32082,x32082),x32084,x32084),f2(x32085,x32085,x32084,x32084))), % 124.50/125.17 inference(scs_inference,[],[3191,2])). % 124.50/125.17 cnf(3217,plain, % 124.50/125.17 (~E(f2(f2(f10(a4),f9(a4),x32171,x32171),f2(a1,a8,x32171,x32171),f10(a4),f9(a4)),f2(x32172,x32172,f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[3190,3191,3198,3194,1690,1869,2,26,24,20,16,3])). % 124.50/125.17 cnf(3235,plain, % 124.50/125.17 (~E(f2(x32351,x32351,f10(a4),f10(a4)),f2(f2(f10(a4),f9(a4),x32352,x32352),f2(a1,a8,x32352,x32352),f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[3217,2])). % 124.50/125.17 cnf(3239,plain, % 124.50/125.17 (~P2(f2(f2(f2(f2(f10(a4),f9(a4),x32391,x32391),f2(a1,a8,x32391,x32391),x32392,x32392),f2(x32393,x32393,x32392,x32392),x32394,x32394),f2(x32395,x32395,x32394,x32394),x32396,x32396),a4,f5(x32396,x32396))), % 124.50/125.17 inference(scs_inference,[],[3208,3217,2761,2,26,24,20])). % 124.50/125.17 cnf(3263,plain, % 124.50/125.17 (~E(f2(f9(a4),f10(a4),f10(a4),f10(a4)),f2(f2(f10(a4),f9(a4),x32631,x32631),f2(a1,a8,x32631,x32631),f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[82,3235,3239,796,2799,404,1700,2,26,24,20,16,3])). % 124.50/125.17 cnf(3275,plain, % 124.50/125.17 (~E(f2(f2(f10(a4),f9(a4),x32751,x32751),f2(a1,a8,x32751,x32751),f10(a4),f9(a4)),f2(f9(a4),f10(a4),f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[3263,2])). % 124.50/125.17 cnf(3281,plain, % 124.50/125.17 (~P2(f2(f2(a1,a8,f10(a4),f9(a4)),f2(f9(a4),f10(a4),f9(a4),f9(a4)),f10(a4),f9(a4)),a4,f5(f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[3263,2767,980,1689,2,26,24,20,16])). % 124.50/125.17 cnf(3283,plain, % 124.50/125.17 (~E(f2(f10(a4),f9(a4),f9(a4),f10(a4)),f2(f2(f10(a4),f9(a4),x32831,x32831),f2(a1,a8,x32831,x32831),f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[3263,2767,980,185,1689,2,26,24,20,16,3])). % 124.50/125.17 cnf(3296,plain, % 124.50/125.17 (~E(f2(x32961,x32961,x32962,x32962),f2(f2(x32963,x32963,x32964,x32964),f2(a8,a1,x32964,x32964),x32962,x32962))), % 124.50/125.17 inference(scs_inference,[],[3275,3283,620,20,2,26,24])). % 124.50/125.17 cnf(3299,plain, % 124.50/125.17 (~E(f2(f2(f10(a4),f9(a4),x32991,x32991),f2(a1,a8,x32991,x32991),f10(a4),f10(a4)),f2(f9(a4),f10(a4),f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[3275,3283,3281,620,1699,1900,20,2,26,24,16,3])). % 124.50/125.17 cnf(3301,plain, % 124.50/125.17 (~P2(f2(f2(a1,a8,f10(a4),f9(a4)),f2(f9(a4),f10(a4),f9(a4),f9(a4)),f10(a4),f10(a4)),a4,f5(f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[3275,3283,3281,620,1699,1869,1900,20,2,26,24,16,3,14])). % 124.50/125.17 cnf(3310,plain, % 124.50/125.17 (~P2(f2(f2(x33101,x33101,x33102,x33102),f2(f2(x33103,x33103,x33104,x33104),f2(a8,a1,x33104,x33104),x33102,x33102),x33105,x33105),a4,f5(x33105,x33105))), % 124.50/125.17 inference(scs_inference,[],[3296,20])). % 124.50/125.17 cnf(3312,plain, % 124.50/125.17 (~E(f2(f2(x33121,x33121,x33122,x33122),f2(a8,a1,x33122,x33122),x33123,x33123),f2(x33124,x33124,x33123,x33123))), % 124.50/125.17 inference(scs_inference,[],[3296,20,2])). % 124.50/125.17 cnf(3313,plain, % 124.50/125.17 (~E(f2(x33131,x33131,x33132,x33132),f2(f2(f2(x33133,x33133,x33134,x33134),f2(a8,a1,x33134,x33134),x33135,x33135),f2(x33136,x33136,x33135,x33135),x33132,x33132))), % 124.50/125.17 inference(scs_inference,[],[3296,20,2,26])). % 124.50/125.17 cnf(3314,plain, % 124.50/125.17 (~E(f2(x33141,x33141,x33142,x33142),f2(f2(x33143,x33143,x33144,x33144),f2(f2(x33145,x33145,x33146,x33146),f2(a8,a1,x33146,x33146),x33144,x33144),x33142,x33142))), % 124.50/125.17 inference(scs_inference,[],[3296,20,2,26,24])). % 124.50/125.17 cnf(3317,plain, % 124.50/125.17 (~E(f2(f10(a4),f9(a4),x33171,x33171),f2(f2(x33172,x33172,x33173,x33173),f2(a8,a1,x33173,x33173),x33171,x33171))), % 124.50/125.17 inference(scs_inference,[],[83,3296,3301,1699,20,2,26,24,16,3])). % 124.50/125.17 cnf(3320,plain, % 124.50/125.17 (~P2(f2(f2(a1,a8,f10(a4),f9(a4)),f2(f10(a4),f9(a4),f9(a4),f9(a4)),f9(a4),f10(a4)),a4,f5(f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[83,3296,3301,2867,1699,1869,20,2,26,24,16,3,14])). % 124.50/125.17 cnf(3326,plain, % 124.50/125.17 (~P2(f2(f2(f2(x33261,x33261,x33262,x33262),f2(a8,a1,x33262,x33262),x33263,x33263),f2(x33264,x33264,x33263,x33263),x33265,x33265),a4,f5(x33265,x33265))), % 124.50/125.17 inference(scs_inference,[],[3312,20])). % 124.50/125.17 cnf(3328,plain, % 124.50/125.17 (~E(f2(f2(f2(x33281,x33281,x33282,x33282),f2(a8,a1,x33282,x33282),x33283,x33283),f2(x33284,x33284,x33283,x33283),x33285,x33285),f2(x33286,x33286,x33285,x33285))), % 124.50/125.17 inference(scs_inference,[],[3312,3313,20,2])). % 124.50/125.17 cnf(3329,plain, % 124.50/125.17 (~E(f2(x33291,x33291,x33292,x33292),f2(f2(f2(f2(x33293,x33293,x33294,x33294),f2(a8,a1,x33294,x33294),x33295,x33295),f2(x33296,x33296,x33295,x33295),x33297,x33297),f2(x33298,x33298,x33297,x33297),x33292,x33292))), % 124.50/125.17 inference(scs_inference,[],[3312,3313,20,2,26])). % 124.50/125.17 cnf(3333,plain, % 124.50/125.17 (~E(f2(f2(x33331,x33331,x33332,x33332),f2(a8,a1,x33332,x33332),f10(a4),f9(a4)),f2(x33333,x33333,f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[3312,3313,3320,1699,1869,20,2,26,24,16,3])). % 124.50/125.17 cnf(3335,plain, % 124.50/125.17 (E(f2(x33351,x33352,x33353,f10(a4)),f2(x33351,x33352,x33353,f9(a4)))), % 124.50/125.17 inference(rename_variables,[],[1869])). % 124.50/125.17 cnf(3336,plain, % 124.50/125.17 (~P2(f2(f2(x33361,x33361,x33362,x33362),f2(f2(x33363,x33363,x33364,x33364),f2(a8,a1,x33364,x33364),x33362,x33362),f9(a4),f10(a4)),a4,f5(f9(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[3312,3313,3310,3320,1699,1869,3335,20,2,26,24,16,3,14])). % 124.50/125.17 cnf(3346,plain, % 124.50/125.17 (~P2(f2(f2(f2(f2(x33461,x33461,x33462,x33462),f2(a8,a1,x33462,x33462),x33463,x33463),f2(x33464,x33464,x33463,x33463),x33465,x33465),f2(x33466,x33466,x33465,x33465),x33467,x33467),a4,f5(x33467,x33467))), % 124.50/125.17 inference(scs_inference,[],[3328,20])). % 124.50/125.17 cnf(3348,plain, % 124.50/125.17 (~E(f2(f2(x33481,x33481,x33482,x33482),f2(a8,a1,x33482,x33482),x33483,x33483),f2(f10(a4),f9(a4),x33483,x33483))), % 124.50/125.17 inference(scs_inference,[],[3328,3317,20,2])). % 124.50/125.17 cnf(3352,plain, % 124.50/125.17 (~P2(f2(f2(f2(x33521,x33521,x33522,x33522),f2(a8,a1,x33522,x33522),x33523,x33523),f2(x33524,x33524,x33523,x33523),f9(a4),f9(a4)),a4,f5(f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[3328,3326,3317,1708,20,2,26,24,16])). % 124.50/125.17 cnf(3353,plain, % 124.50/125.17 (~P2(f2(f2(f2(x33531,x33531,x33532,x33532),f2(a8,a1,x33532,x33532),x33533,x33533),f2(x33534,x33534,x33533,x33533),x33535,x33535),a4,f5(x33535,x33535))), % 124.50/125.17 inference(rename_variables,[],[3326])). % 124.50/125.17 cnf(3357,plain, % 124.50/125.17 (~P2(f2(f2(f2(x33571,x33571,x33572,x33572),f2(a8,a1,x33572,x33572),x33573,x33573),f2(x33574,x33574,x33573,x33573),f10(a4),f9(a4)),a4,f5(f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[83,3328,3326,3353,3317,3329,1708,1900,20,2,26,24,16,3,14])). % 124.50/125.17 cnf(3366,plain, % 124.50/125.17 (~E(f2(x33661,x33661,f10(a4),f10(a4)),f2(f2(x33662,x33662,x33663,x33663),f2(a8,a1,x33663,x33663),f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[3348,3333,20,2])). % 124.50/125.17 cnf(3373,plain, % 124.50/125.17 (~E(f2(f2(x33731,x33731,x33732,x33732),f2(a8,a1,x33732,x33732),f10(a4),f9(a4)),f2(f10(a4),f9(a4),f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[3348,3333,3346,3314,1690,1869,20,2,26,24,16,3])). % 124.50/125.17 cnf(3390,plain, % 124.50/125.17 (~E(f2(f10(a4),f9(a4),f10(a4),f10(a4)),f2(f2(x33901,x33901,x33902,x33902),f2(a8,a1,x33902,x33902),f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[3373,20,2])). % 124.50/125.17 cnf(3395,plain, % 124.50/125.17 (~E(f2(f10(a4),f9(a4),f9(a4),f10(a4)),f2(f2(x33951,x33951,x33952,x33952),f2(a8,a1,x33952,x33952),f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[3373,3366,3336,2818,190,1708,20,2,26,24,16,3])). % 124.50/125.17 cnf(3398,plain, % 124.50/125.17 (~P2(f2(f2(f2(x33981,x33981,x33982,x33982),f2(a8,a1,x33982,x33982),x33983,x33983),f2(x33984,x33984,x33983,x33983),f9(a4),f10(a4)),a4,f5(f10(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[3373,3366,3336,3352,2818,190,1708,1869,20,2,26,24,16,3,14])). % 124.50/125.17 cnf(3407,plain, % 124.50/125.17 (~E(f2(f2(x34071,x34071,x34072,x34072),f2(a8,a1,x34072,x34072),f10(a4),f9(a4)),f2(f10(a4),f9(a4),f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[3390,3395,20,2])). % 124.50/125.17 cnf(3412,plain, % 124.50/125.17 (~E(f2(f10(a4),f10(a4),f9(a4),f10(a4)),f2(f2(x34121,x34121,x34122,x34122),f2(a8,a1,x34122,x34122),f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[3390,3395,3299,3357,174,1700,20,2,26,24,16,3])). % 124.50/125.17 cnf(3428,plain, % 124.50/125.17 (~E(f2(f2(x34281,x34281,x34282,x34282),f2(a8,a1,x34282,x34282),f10(a4),f9(a4)),f2(f10(a4),f10(a4),f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[3407,3412,20,2])). % 124.50/125.17 cnf(3430,plain, % 124.50/125.17 (~E(f2(x34301,x34301,x34302,x34302),f2(f2(x34303,x34303,x34304,x34304),f2(f2(a1,a8,x34305,x34305),f2(x34306,x34306,x34305,x34305),x34304,x34304),x34302,x34302))), % 124.50/125.17 inference(scs_inference,[],[3407,3412,673,20,2,26,24])). % 124.50/125.17 cnf(3432,plain, % 124.50/125.17 (~P2(f2(f2(f2(x34321,x34321,x34322,x34322),f2(a8,a1,x34322,x34322),x34323,x34323),f2(x34324,x34324,x34323,x34323),f9(a4),f10(a4)),a4,f5(f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[3407,3412,3398,673,1689,20,2,26,24,16])). % 124.50/125.17 cnf(3434,plain, % 124.50/125.17 (~E(f2(f9(a4),f9(a4),f9(a4),f10(a4)),f2(f2(x34341,x34341,x34342,x34342),f2(a8,a1,x34342,x34342),f10(a4),f9(a4)))), % 124.50/125.17 inference(scs_inference,[],[3407,3412,3398,673,106,1689,20,2,26,24,16,3])). % 124.50/125.17 cnf(3445,plain, % 124.50/125.17 (~E(f2(f2(x34451,x34451,x34452,x34452),f2(a8,a1,x34452,x34452),f10(a4),f9(a4)),f2(f9(a4),f9(a4),f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[3428,3434,20,2])). % 124.50/125.17 cnf(3450,plain, % 124.50/125.17 (~E(f2(f2(x34501,x34501,x34502,x34502),f2(a8,a1,x34502,x34502),f10(a4),f10(a4)),f2(f10(a4),f10(a4),f9(a4),f10(a4)))), % 124.50/125.17 inference(scs_inference,[],[3428,3434,3432,607,1699,1900,20,2,26,24,16,3])). % 124.50/125.17 cnf(3458,plain, % 124.50/125.17 (~E(f2(x34581,x34581,x34582,x34582),f2(f2(f2(x34583,x34583,x34584,x34584),f2(f2(a1,a8,x34585,x34585),f2(x34586,x34586,x34585,x34585),x34584,x34584),x34587,x34587),f2(x34588,x34588,x34587,x34587),x34582,x34582))), % 124.50/125.17 inference(scs_inference,[],[3445,3450,3430,20,2,26])). % 124.50/125.17 cnf(3753,plain, % 124.50/125.17 (~E(f2(x37531,x37531,a6,a6),f2(f7(f9(a4)),f7(f10(a4)),a6,a6))), % 124.50/125.17 inference(scs_inference,[],[459,1881,2423,1878,3458,2,75,4,5,23])). % 124.50/125.17 cnf(4084,plain, % 124.50/125.17 ($false), % 124.50/125.17 inference(scs_inference,[],[264,219,2144,2313,2766,3753,2,75,5,23,4]), % 124.50/125.17 ['proof']). % 124.50/125.17 % SZS output end Proof % 124.50/125.17 % Total time :123.810000s %------------------------------------------------------------------------------