%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET916+1 : TPTP v8.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n017.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:58 EDT 2024 % Result : Theorem 180.75s 180.76s % Output : CNFRefutation 180.93s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : SET916+1 : TPTP v8.2.0. Released v3.2.0. % 0.07/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n017.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sun Jun 23 17:45:54 EDT 2024 % 0.13/0.34 % CPUTime : % 0.20/0.57 start to proof:theBenchmark % 180.75/180.73 %------------------------------------------- % 180.75/180.73 % File :CSE---1.7 % 180.75/180.73 % Problem :theBenchmark % 180.75/180.73 % Transform :cnf % 180.75/180.73 % Format :tptp:raw % 180.75/180.73 % Command :java -jar mcs_scs.jar %d %s % 180.75/180.73 % 180.75/180.73 % Result :Theorem 180.130000s % 180.75/180.73 % Output :CNFRefutation 180.130000s % 180.75/180.73 %------------------------------------------- % 180.75/180.75 %------------------------------------------------------------------------------ % 180.75/180.75 % File : SET916+1 : TPTP v8.2.0. Released v3.2.0. % 180.75/180.76 % Domain : Set theory % 180.75/180.76 % Problem : ~ ( ~ in(A,B) & ~ in(C,B) & ~ disjoint(unordered_pair(A,C),B) ) % 180.75/180.76 % Version : [Urb06] axioms : Especial. % 180.75/180.76 % English : % 180.75/180.76 % 180.75/180.76 % Refs : [Byl90] Bylinski (1990), Some Basic Properties of Sets % 180.75/180.76 % : [Urb06] Urban (2006), Email to G. Sutcliffe % 180.75/180.76 % Source : [Urb06] % 180.75/180.76 % Names : zfmisc_1__t57_zfmisc_1 [Urb06] % 180.75/180.76 % 180.75/180.76 % Status : Theorem % 180.75/180.76 % Rating : 0.44 v8.2.0, 0.42 v8.1.0, 0.39 v7.5.0, 0.47 v7.4.0, 0.37 v7.3.0, 0.34 v7.2.0, 0.31 v7.1.0, 0.39 v7.0.0, 0.33 v6.4.0, 0.42 v6.3.0, 0.46 v6.2.0, 0.48 v6.1.0, 0.60 v6.0.0, 0.61 v5.5.0, 0.59 v5.4.0, 0.64 v5.3.0, 0.63 v5.2.0, 0.50 v5.1.0, 0.52 v5.0.0, 0.54 v4.1.0, 0.61 v4.0.1, 0.57 v4.0.0, 0.58 v3.7.0, 0.60 v3.5.0, 0.58 v3.3.0, 0.57 v3.2.0 % 180.75/180.76 % Syntax : Number of formulae : 11 ( 5 unt; 0 def) % 180.75/180.76 % Number of atoms : 24 ( 7 equ) % 180.75/180.76 % Maximal formula atoms : 4 ( 2 avg) % 180.75/180.76 % Number of connectives : 23 ( 10 ~; 1 |; 6 &) % 180.75/180.76 % ( 4 <=>; 2 =>; 0 <=; 0 <~>) % 180.75/180.76 % Maximal formula depth : 8 ( 5 avg) % 180.75/180.76 % Maximal term depth : 2 ( 1 avg) % 180.75/180.76 % Number of predicates : 4 ( 3 usr; 0 prp; 1-2 aty) % 180.75/180.76 % Number of functors : 2 ( 2 usr; 0 con; 2-2 aty) % 180.75/180.76 % Number of variables : 27 ( 24 !; 3 ?) % 180.75/180.76 % SPC : FOF_THM_RFO_SEQ % 180.75/180.76 % 180.75/180.76 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 180.75/180.76 % library, www.mizar.org % 180.75/180.76 %------------------------------------------------------------------------------ % 180.75/180.76 fof(antisymmetry_r2_hidden,axiom, % 180.75/180.76 ! [A,B] : % 180.75/180.76 ( in(A,B) % 180.75/180.76 => ~ in(B,A) ) ). % 180.75/180.76 % 180.75/180.76 fof(commutativity_k2_tarski,axiom, % 180.75/180.76 ! [A,B] : unordered_pair(A,B) = unordered_pair(B,A) ). % 180.75/180.76 % 180.75/180.76 fof(commutativity_k3_xboole_0,axiom, % 180.75/180.76 ! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) ). % 180.75/180.76 % 180.75/180.76 fof(d2_tarski,axiom, % 180.75/180.76 ! [A,B,C] : % 180.75/180.76 ( C = unordered_pair(A,B) % 180.75/180.76 <=> ! [D] : % 180.75/180.76 ( in(D,C) % 180.75/180.76 <=> ( D = A % 180.75/180.76 | D = B ) ) ) ). % 180.75/180.76 % 180.75/180.76 fof(d3_xboole_0,axiom, % 180.75/180.76 ! [A,B,C] : % 180.75/180.76 ( C = set_intersection2(A,B) % 180.75/180.76 <=> ! [D] : % 180.75/180.76 ( in(D,C) % 180.75/180.76 <=> ( in(D,A) % 180.75/180.76 & in(D,B) ) ) ) ). % 180.75/180.76 % 180.75/180.76 fof(idempotence_k3_xboole_0,axiom, % 180.75/180.76 ! [A,B] : set_intersection2(A,A) = A ). % 180.75/180.76 % 180.75/180.76 fof(rc1_xboole_0,axiom, % 180.75/180.76 ? [A] : empty(A) ). % 180.75/180.76 % 180.75/180.76 fof(rc2_xboole_0,axiom, % 180.75/180.76 ? [A] : ~ empty(A) ). % 180.75/180.76 % 180.75/180.76 fof(symmetry_r1_xboole_0,axiom, % 180.75/180.76 ! [A,B] : % 180.75/180.76 ( disjoint(A,B) % 180.75/180.76 => disjoint(B,A) ) ). % 180.75/180.76 % 180.75/180.76 fof(t4_xboole_0,axiom, % 180.75/180.76 ! [A,B] : % 180.75/180.76 ( ~ ( ~ disjoint(A,B) % 180.75/180.76 & ! [C] : ~ in(C,set_intersection2(A,B)) ) % 180.75/180.76 & ~ ( ? [C] : in(C,set_intersection2(A,B)) % 180.75/180.76 & disjoint(A,B) ) ) ). % 180.75/180.76 % 180.75/180.76 fof(t57_zfmisc_1,conjecture, % 180.75/180.76 ! [A,B,C] : % 180.75/180.76 ~ ( ~ in(A,B) % 180.75/180.76 & ~ in(C,B) % 180.75/180.76 & ~ disjoint(unordered_pair(A,C),B) ) ). % 180.75/180.76 % 180.75/180.76 %------------------------------------------------------------------------------ % 180.75/180.76 %------------------------------------------- % 180.75/180.76 % Proof found % 180.75/180.76 % SZS status Theorem for theBenchmark % 180.75/180.76 % SZS output start Proof % 180.75/180.78 %ClaNum:44(EqnAxiom:20) % 180.75/180.78 %VarNum:150(SingletonVarNum:56) % 180.75/180.78 %MaxLitNum:4 % 180.75/180.78 %MaxfuncDepth:1 % 180.75/180.78 %SharedTerms:11 % 180.75/180.78 %goalClause: 26 27 28 % 180.75/180.78 %singleGoalClaCount:3 % 180.75/180.78 [21]P1(a1) % 180.75/180.78 [25]~P1(a5) % 180.75/180.78 [26]~P3(a6,a8) % 180.75/180.78 [27]~P3(a9,a8) % 180.75/180.78 [28]~P2(f10(a6,a9),a8) % 180.75/180.78 [22]E(f4(x221,x221),x221) % 180.75/180.78 [23]E(f10(x231,x232),f10(x232,x231)) % 180.75/180.78 [24]E(f4(x241,x242),f4(x242,x241)) % 180.75/180.78 [29]~P2(x292,x291)+P2(x291,x292) % 180.75/180.78 [32]~P3(x322,x321)+~P3(x321,x322) % 180.75/180.78 [36]P2(x361,x362)+P3(f7(x361,x362),f4(x361,x362)) % 180.75/180.78 [38]~P2(x381,x382)+~P3(x383,f4(x381,x382)) % 180.75/180.78 [40]P3(f3(x402,x403,x401),x401)+P3(f3(x402,x403,x401),x403)+E(x401,f4(x402,x403)) % 180.75/180.78 [41]P3(f3(x412,x413,x411),x411)+P3(f3(x412,x413,x411),x412)+E(x411,f4(x412,x413)) % 180.75/180.78 [42]~E(f2(x422,x423,x421),x423)+~P3(f2(x422,x423,x421),x421)+E(x421,f10(x422,x423)) % 180.75/180.78 [43]~E(f2(x432,x433,x431),x432)+~P3(f2(x432,x433,x431),x431)+E(x431,f10(x432,x433)) % 180.75/180.78 [30]P3(x301,x302)+~E(x301,x303)+~E(x302,f10(x304,x303)) % 180.75/180.78 [31]P3(x311,x312)+~E(x311,x313)+~E(x312,f10(x313,x314)) % 180.75/180.78 [34]~P3(x341,x343)+P3(x341,x342)+~E(x343,f4(x344,x342)) % 180.75/180.78 [35]~P3(x351,x353)+P3(x351,x352)+~E(x353,f4(x352,x354)) % 180.75/180.78 [39]E(f2(x392,x393,x391),x393)+E(f2(x392,x393,x391),x392)+P3(f2(x392,x393,x391),x391)+E(x391,f10(x392,x393)) % 180.75/180.78 [44]~P3(f3(x442,x443,x441),x441)+~P3(f3(x442,x443,x441),x443)+~P3(f3(x442,x443,x441),x442)+E(x441,f4(x442,x443)) % 180.75/180.78 [33]~P3(x331,x334)+E(x331,x332)+E(x331,x333)+~E(x334,f10(x333,x332)) % 180.75/180.78 [37]~P3(x371,x374)+~P3(x371,x373)+P3(x371,x372)+~E(x372,f4(x373,x374)) % 180.75/180.78 %EqnAxiom % 180.75/180.78 [1]E(x11,x11) % 180.75/180.78 [2]E(x22,x21)+~E(x21,x22) % 180.75/180.78 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 180.75/180.78 [4]~E(x41,x42)+E(f4(x41,x43),f4(x42,x43)) % 180.75/180.78 [5]~E(x51,x52)+E(f4(x53,x51),f4(x53,x52)) % 180.75/180.78 [6]~E(x61,x62)+E(f10(x61,x63),f10(x62,x63)) % 180.75/180.78 [7]~E(x71,x72)+E(f10(x73,x71),f10(x73,x72)) % 180.75/180.78 [8]~E(x81,x82)+E(f3(x81,x83,x84),f3(x82,x83,x84)) % 180.75/180.78 [9]~E(x91,x92)+E(f3(x93,x91,x94),f3(x93,x92,x94)) % 180.75/180.78 [10]~E(x101,x102)+E(f3(x103,x104,x101),f3(x103,x104,x102)) % 180.75/180.78 [11]~E(x111,x112)+E(f2(x111,x113,x114),f2(x112,x113,x114)) % 180.75/180.78 [12]~E(x121,x122)+E(f2(x123,x121,x124),f2(x123,x122,x124)) % 180.75/180.78 [13]~E(x131,x132)+E(f2(x133,x134,x131),f2(x133,x134,x132)) % 180.75/180.78 [14]~E(x141,x142)+E(f7(x141,x143),f7(x142,x143)) % 180.75/180.78 [15]~E(x151,x152)+E(f7(x153,x151),f7(x153,x152)) % 180.75/180.78 [16]~P1(x161)+P1(x162)+~E(x161,x162) % 180.75/180.78 [17]P3(x172,x173)+~E(x171,x172)+~P3(x171,x173) % 180.75/180.78 [18]P3(x183,x182)+~E(x181,x182)+~P3(x183,x181) % 180.75/180.78 [19]P2(x192,x193)+~E(x191,x192)+~P2(x191,x193) % 180.75/180.78 [20]P2(x203,x202)+~E(x201,x202)+~P2(x203,x201) % 180.75/180.78 % 180.75/180.78 %------------------------------------------- % 180.75/180.81 cnf(45,plain, % 180.75/180.81 (~P3(x451,f10(x452,x453))+E(x451,x453)+E(x451,x452)), % 180.75/180.81 inference(equality_inference,[],[33])). % 180.75/180.81 cnf(46,plain, % 180.75/180.81 (~P3(x461,f4(x462,x463))+P3(x461,x463)), % 180.75/180.81 inference(equality_inference,[],[34])). % 180.75/180.81 cnf(47,plain, % 180.75/180.81 (~P3(x471,f4(x472,x473))+P3(x471,x472)), % 180.75/180.81 inference(equality_inference,[],[35])). % 180.75/180.81 cnf(48,plain, % 180.75/180.81 (~P3(x481,x482)+~P3(x481,x483)+P3(x481,f4(x483,x482))), % 180.75/180.81 inference(equality_inference,[],[37])). % 180.75/180.81 cnf(49,plain, % 180.75/180.81 (~P2(a8,f10(a6,a9))), % 180.75/180.81 inference(scs_inference,[],[28,29])). % 180.75/180.81 cnf(51,plain, % 180.75/180.81 (~P3(a6,f4(x511,a8))), % 180.75/180.81 inference(scs_inference,[],[26,28,29,46])). % 180.75/180.81 cnf(53,plain, % 180.75/180.81 (~P3(a6,f4(a8,x531))), % 180.75/180.81 inference(scs_inference,[],[26,28,29,46,47])). % 180.75/180.81 cnf(55,plain, % 180.75/180.81 (E(x551,f4(x551,x551))), % 180.75/180.81 inference(scs_inference,[],[26,28,22,29,46,47,2])). % 180.75/180.81 cnf(56,plain, % 180.75/180.81 (P3(f4(x561,x561),f10(x561,x562))), % 180.75/180.81 inference(scs_inference,[],[26,28,22,23,29,46,47,2,30])). % 180.75/180.81 cnf(57,plain, % 180.75/180.81 (E(f10(x571,x572),f10(x572,x571))), % 180.75/180.81 inference(rename_variables,[],[23])). % 180.75/180.81 cnf(59,plain, % 180.75/180.81 (P3(f4(x591,x591),f10(x592,x591))), % 180.75/180.81 inference(scs_inference,[],[26,28,22,23,57,29,46,47,2,30,31])). % 180.75/180.81 cnf(60,plain, % 180.75/180.81 (E(f10(x601,x602),f10(x602,x601))), % 180.75/180.81 inference(rename_variables,[],[23])). % 180.75/180.81 cnf(63,plain, % 180.75/180.81 (E(f4(x631,x631),x631)), % 180.75/180.81 inference(rename_variables,[],[22])). % 180.75/180.81 cnf(66,plain, % 180.75/180.81 (E(f4(x661,x661),x661)), % 180.75/180.81 inference(rename_variables,[],[22])). % 180.75/180.81 cnf(69,plain, % 180.75/180.81 (E(f4(x691,x691),x691)), % 180.75/180.81 inference(rename_variables,[],[22])). % 180.75/180.81 cnf(72,plain, % 180.75/180.81 (~P1(f4(a5,a5))), % 180.75/180.81 inference(scs_inference,[],[26,28,22,63,66,69,23,57,60,25,29,46,47,2,30,31,34,35,17,18,16])). % 180.75/180.81 cnf(73,plain, % 180.75/180.81 (E(f4(x731,x731),x731)), % 180.75/180.81 inference(rename_variables,[],[22])). % 180.75/180.81 cnf(74,plain, % 180.75/180.81 (~P3(f10(f4(x741,a8),x742),f4(x741,a8))), % 180.75/180.81 inference(scs_inference,[],[26,28,22,63,66,69,23,57,60,25,29,46,47,2,30,31,34,35,17,18,16,32])). % 180.75/180.81 cnf(79,plain, % 180.75/180.81 (~P3(x791,f4(f10(x792,x793),f10(x792,x793)))+E(x791,x793)+E(x791,x792)), % 180.75/180.81 inference(scs_inference,[],[26,28,22,63,66,69,73,23,57,60,25,29,46,47,2,30,31,34,35,17,18,16,32,33])). % 180.75/180.81 cnf(80,plain, % 180.75/180.81 (~P3(a9,f4(a8,x801))), % 180.75/180.81 inference(scs_inference,[],[27,47])). % 180.75/180.81 cnf(82,plain, % 180.75/180.81 (~P3(a9,f4(x821,a8))), % 180.75/180.81 inference(scs_inference,[],[27,47,46])). % 180.75/180.81 cnf(84,plain, % 180.75/180.81 (~P3(f10(x841,x842),f4(x841,x841))), % 180.75/180.81 inference(scs_inference,[],[56,27,47,46,32])). % 180.75/180.81 cnf(86,plain, % 180.75/180.81 (E(f4(x861,x862),f4(f4(x862,x861),f4(x862,x861)))), % 180.75/180.81 inference(scs_inference,[],[56,27,55,24,47,46,32,3])). % 180.75/180.81 cnf(87,plain, % 180.75/180.81 (E(x871,f4(x871,x871))), % 180.75/180.81 inference(rename_variables,[],[55])). % 180.75/180.81 cnf(91,plain, % 180.75/180.81 (E(x911,f4(x911,x911))), % 180.75/180.81 inference(rename_variables,[],[55])). % 180.75/180.81 cnf(93,plain, % 180.75/180.81 (E(f10(x931,x932),f10(x932,x931))), % 180.75/180.81 inference(rename_variables,[],[23])). % 180.75/180.81 cnf(95,plain, % 180.75/180.81 (~P3(f10(x951,x952),x951)), % 180.75/180.81 inference(scs_inference,[],[56,27,74,55,87,91,24,23,47,46,32,3,35,17,31,48])). % 180.75/180.81 cnf(97,plain, % 180.75/180.81 (~E(f10(f10(x971,x972),x973),x971)), % 180.75/180.81 inference(scs_inference,[],[56,27,74,55,87,91,24,23,93,47,46,32,3,35,17,31,48,30])). % 180.75/180.81 cnf(99,plain, % 180.75/180.81 (P1(f4(a1,a1))), % 180.75/180.81 inference(scs_inference,[],[56,27,74,55,87,91,24,23,93,21,47,46,32,3,35,17,31,48,30,16])). % 180.75/180.81 cnf(100,plain, % 180.75/180.81 (E(x1001,f4(x1001,x1001))), % 180.75/180.81 inference(rename_variables,[],[55])). % 180.75/180.81 cnf(101,plain, % 180.75/180.81 (P3(f4(x1011,x1011),f4(f10(x1012,x1011),f10(x1012,x1011)))), % 180.75/180.81 inference(scs_inference,[],[56,27,59,74,55,87,91,100,24,23,93,21,47,46,32,3,35,17,31,48,30,16,18])). % 180.75/180.81 cnf(117,plain, % 180.75/180.81 (E(f4(x1171,x1171),x1171)), % 180.75/180.81 inference(rename_variables,[],[22])). % 180.75/180.81 cnf(118,plain, % 180.75/180.81 (~E(f10(f10(x1181,x1182),x1183),x1182)), % 180.75/180.81 inference(scs_inference,[],[84,101,97,22,117,86,47,32,46,2,3,30])). % 180.75/180.81 cnf(122,plain, % 180.75/180.81 (~P3(f4(f10(x1221,x1222),f10(x1221,x1222)),x1222)), % 180.75/180.81 inference(scs_inference,[],[84,101,97,22,117,86,47,32,46,2,3,30,48])). % 180.75/180.81 cnf(124,plain, % 180.75/180.81 (~E(f4(x1241,x1241),f10(f10(x1241,x1242),x1243))), % 180.75/180.81 inference(scs_inference,[],[56,84,95,101,97,22,117,86,47,32,46,2,3,30,48,17])). % 180.75/180.81 cnf(127,plain, % 180.75/180.81 (P3(f4(x1271,x1271),f10(x1271,x1272))), % 180.75/180.81 inference(rename_variables,[],[56])). % 180.75/180.81 cnf(128,plain, % 180.75/180.81 (P1(f4(f4(a1,a1),f4(a1,a1)))), % 180.75/180.81 inference(scs_inference,[],[56,84,95,101,97,22,117,86,99,47,32,46,2,3,30,48,17,18,16])). % 180.75/180.81 cnf(130,plain, % 180.75/180.81 (P3(f4(x1301,x1301),f4(f10(x1301,x1302),f10(x1301,x1302)))), % 180.75/180.81 inference(scs_inference,[],[56,127,84,95,101,97,22,117,86,24,99,47,32,46,2,3,30,48,17,18,16,37])). % 180.75/180.81 cnf(133,plain, % 180.75/180.81 (~E(f10(x1331,f10(x1332,x1333)),x1332)), % 180.75/180.81 inference(scs_inference,[],[56,127,84,95,101,97,22,117,86,24,99,47,32,46,2,3,30,48,17,18,16,37,6])). % 180.75/180.81 cnf(140,plain, % 180.75/180.81 (~P3(f4(f10(x1401,x1402),f10(x1401,x1402)),f4(x1403,x1402))), % 180.75/180.81 inference(scs_inference,[],[122,47,46])). % 180.75/180.81 cnf(283,plain, % 180.75/180.81 (~E(f10(x2831,f10(x2832,x2833)),f4(x2834,x2833))), % 180.75/180.81 inference(scs_inference,[],[140,80,118,59,133,47,46,45,18])). % 180.75/180.81 cnf(310,plain, % 180.75/180.81 (~P3(f10(x3101,x3102),f4(x3101,x3103))), % 180.75/180.81 inference(scs_inference,[],[95,47])). % 180.75/180.81 cnf(1435,plain, % 180.75/180.81 (~P2(a8,f10(a9,a6))), % 180.75/180.81 inference(scs_inference,[],[28,23,19,29])). % 180.75/180.81 cnf(1436,plain, % 180.75/180.81 (~P2(f10(a9,a6),a8)), % 180.75/180.81 inference(scs_inference,[],[1435,29])). % 180.75/180.81 cnf(2448,plain, % 180.75/180.81 (E(f4(f4(x24481,x24481),x24482),f4(x24481,x24482))), % 180.75/180.81 inference(scs_inference,[],[55,2,4])). % 180.75/180.81 cnf(2449,plain, % 180.75/180.81 (E(f4(x24491,x24492),f4(f4(x24491,x24491),x24492))), % 180.75/180.81 inference(scs_inference,[],[2448,2])). % 180.75/180.81 cnf(2450,plain, % 180.75/180.81 (P1(f4(a1,f4(a1,a1)))), % 180.75/180.81 inference(scs_inference,[],[2448,128,2,16])). % 180.75/180.81 cnf(2454,plain, % 180.75/180.81 (P1(f4(f4(a1,a1),a1))), % 180.75/180.81 inference(scs_inference,[],[24,2450,16])). % 180.75/180.81 cnf(2456,plain, % 180.75/180.81 (P3(f4(x24561,x24561),f4(f10(x24561,x24562),f10(x24561,x24563)))), % 180.75/180.81 inference(scs_inference,[],[56,130,24,2449,2450,16,37])). % 180.75/180.81 cnf(2462,plain, % 180.75/180.81 (~P2(f10(x24621,x24622),f10(x24621,x24623))), % 180.75/180.81 inference(scs_inference,[],[56,130,24,2449,2450,16,37,32,38])). % 180.75/180.81 cnf(2471,plain, % 180.75/180.81 (P3(f4(x24711,x24711),f4(f10(x24712,x24711),f10(x24711,x24713)))), % 180.75/180.81 inference(scs_inference,[],[56,101,2449,37])). % 180.75/180.81 cnf(2477,plain, % 180.75/180.81 (~P2(f10(x24771,x24772),f10(x24772,x24773))), % 180.75/180.81 inference(scs_inference,[],[56,101,2449,37,32,38])). % 180.75/180.81 cnf(2481,plain, % 180.75/180.81 (~P2(f10(x24811,x24812),f10(x24813,x24811))), % 180.75/180.81 inference(scs_inference,[],[56,101,2449,37,32,38,48,29])). % 180.75/180.81 cnf(2483,plain, % 180.75/180.81 (~P3(f4(f10(x24831,x24832),f10(x24832,x24833)),f4(x24832,x24834))), % 180.75/180.81 inference(scs_inference,[],[56,101,2449,37,32,38,48,29,47])). % 180.75/180.81 cnf(2627,plain, % 180.75/180.81 (E(f4(x26271,x26272),f4(x26271,f4(x26272,x26272)))), % 180.75/180.81 inference(scs_inference,[],[22,2,5])). % 180.75/180.81 cnf(2629,plain, % 180.75/180.81 (P3(x26291,f10(x26292,x26291))), % 180.75/180.81 inference(scs_inference,[],[59,22,2627,2,17])). % 180.75/180.81 cnf(2630,plain, % 180.75/180.81 (P3(f4(x26301,x26301),f10(x26302,x26301))), % 180.75/180.81 inference(rename_variables,[],[59])). % 180.75/180.81 cnf(2631,plain, % 180.75/180.81 (P3(f4(x26311,x26311),f4(f10(x26312,x26311),f10(x26313,x26311)))), % 180.75/180.81 inference(scs_inference,[],[59,2630,101,22,2449,2627,2,17,37])). % 180.75/180.81 cnf(2635,plain, % 180.75/180.81 (~P2(f10(x26351,x26352),f10(x26353,x26352))), % 180.75/180.81 inference(scs_inference,[],[59,2630,101,22,2449,2627,2,17,37,38])). % 180.75/180.81 cnf(2639,plain, % 180.75/180.81 (~E(f10(x26391,a6),a8)), % 180.75/180.81 inference(scs_inference,[],[59,2630,26,101,22,2449,2627,2,17,37,38,32,18])). % 180.75/180.81 cnf(2642,plain, % 180.75/180.81 (~P3(f10(x26421,a6),f10(a8,a8))), % 180.75/180.81 inference(scs_inference,[],[59,2630,26,101,22,2449,2627,2,17,37,38,32,18,48,45])). % 180.75/180.81 cnf(2657,plain, % 180.75/180.81 (P3(x26571,f10(x26571,x26572))), % 180.75/180.81 inference(scs_inference,[],[56,22,2642,47,46,17])). % 180.75/180.81 cnf(2667,plain, % 180.75/180.81 (~P3(f4(f10(x26671,x26672),f10(x26673,x26671)),x26671)), % 180.75/180.81 inference(scs_inference,[],[59,56,26,2456,22,2449,2642,47,46,17,37,32,18,48])). % 180.75/180.81 cnf(2669,plain, % 180.75/180.81 (~P3(f10(a6,x26691),f10(a8,a8))), % 180.75/180.81 inference(scs_inference,[],[59,56,26,2456,22,2449,2642,47,46,17,37,32,18,48,45])). % 180.75/180.81 cnf(2678,plain, % 180.75/180.81 (P3(x26781,f4(f10(x26782,x26781),f10(x26781,x26783)))), % 180.75/180.81 inference(scs_inference,[],[2471,2667,22,47,46,17])). % 180.75/180.81 cnf(2691,plain, % 180.75/180.81 (P3(x26911,f4(f10(x26911,x26912),f10(x26911,x26913)))), % 180.75/180.81 inference(scs_inference,[],[2456,22,2669,47,46,17])). % 180.75/180.81 cnf(2711,plain, % 180.75/180.81 (P3(x27111,f10(f4(x27111,x27111),x27112))), % 180.75/180.81 inference(scs_inference,[],[2657,22,17])). % 180.75/180.81 cnf(2713,plain, % 180.75/180.81 (~P3(f10(f4(x27131,x27131),x27132),x27131)), % 180.75/180.81 inference(scs_inference,[],[2657,22,17,32])). % 180.75/180.81 cnf(2728,plain, % 180.75/180.81 (P3(x27281,f4(f10(x27282,x27281),f10(x27283,x27281)))), % 180.75/180.81 inference(scs_inference,[],[2631,2713,22,47,17])). % 180.75/180.81 cnf(2812,plain, % 180.75/180.81 (P3(f10(x28121,x28122),f10(x28123,f10(x28122,x28121)))), % 180.75/180.81 inference(scs_inference,[],[2629,23,17])). % 180.75/180.81 cnf(2814,plain, % 180.75/180.81 (~P3(f10(x28141,f10(x28142,x28143)),f10(x28143,x28142))), % 180.75/180.81 inference(scs_inference,[],[2629,23,17,32])). % 180.75/180.81 cnf(3224,plain, % 180.75/180.81 (~E(f4(f10(x32241,a9),f10(a9,x32242)),f4(a8,x32243))), % 180.75/180.81 inference(scs_inference,[],[80,2678,18])). % 180.75/180.81 cnf(3226,plain, % 180.75/180.81 (~E(f10(x32261,a9),a8)), % 180.75/180.81 inference(scs_inference,[],[80,2678,18,4])). % 180.75/180.81 cnf(3236,plain, % 180.75/180.81 (~E(f4(f10(a9,x32361),f10(a9,x32362)),f4(a8,x32363))), % 180.75/180.81 inference(scs_inference,[],[80,2691,18])). % 180.75/180.81 cnf(3238,plain, % 180.75/180.81 (~E(f10(a9,x32381),a8)), % 180.75/180.81 inference(scs_inference,[],[80,2691,18,4])). % 180.75/180.81 cnf(3256,plain, % 180.75/180.81 (~E(f10(x32561,a9),f4(a8,x32562))), % 180.75/180.81 inference(scs_inference,[],[80,2629,18])). % 180.75/180.81 cnf(3258,plain, % 180.75/180.81 (P3(f3(a8,x32581,f10(x32582,a9)),f10(x32582,a9))+P3(f3(a8,x32581,f10(x32582,a9)),a8)), % 180.75/180.81 inference(scs_inference,[],[80,2629,18,41])). % 180.75/180.81 cnf(3280,plain, % 180.75/180.81 (~E(f10(a9,x32801),f4(a8,x32802))), % 180.75/180.81 inference(scs_inference,[],[80,2657,18])). % 180.75/180.81 cnf(3324,plain, % 180.75/180.81 (P3(f3(a8,x33241,f10(a9,x33242)),f10(a9,x33242))+P3(f3(a8,x33241,f10(a9,x33242)),x33241)), % 180.75/180.81 inference(scs_inference,[],[3280,40])). % 180.75/180.81 cnf(3351,plain, % 180.75/180.81 (~P3(f10(x33511,a9),f3(a8,x33512,f10(x33511,a9)))+P3(f3(a8,x33512,f10(x33511,a9)),a8)), % 180.75/180.81 inference(scs_inference,[],[3258,32])). % 180.75/180.81 cnf(3352,plain, % 180.75/180.81 (~E(f10(x33521,a9),f4(x33522,a8))), % 180.75/180.81 inference(scs_inference,[],[3256,24,3])). % 180.75/180.81 cnf(3591,plain, % 180.75/180.81 (~P3(f3(a8,x35911,f10(x35912,a9)),f10(x35912,a9))+~P3(f3(a8,x35911,f10(x35912,a9)),a8)+~P3(f3(a8,x35911,f10(x35912,a9)),x35911)), % 180.75/180.81 inference(scs_inference,[],[82,3256,124,2728,18,44])). % 180.75/180.81 cnf(3596,plain, % 180.75/180.81 (~E(f10(a9,x35961),f4(x35962,a8))), % 180.75/180.81 inference(scs_inference,[],[82,2657,18])). % 180.75/180.81 cnf(3635,plain, % 180.75/180.81 (~P3(f3(a8,f10(a9,a9),f10(a9,a9)),a8)), % 180.75/180.81 inference(scs_inference,[],[3324,3591])). % 180.75/180.81 cnf(3638,plain, % 180.75/180.81 (~P3(f10(a9,a9),f3(a8,f10(a9,a9),f10(a9,a9)))), % 180.75/180.81 inference(scs_inference,[],[3635,3258,3351])). % 180.75/180.81 cnf(3973,plain, % 180.75/180.81 (~P2(f4(a8,a8),f10(a6,a9))), % 180.75/180.81 inference(scs_inference,[],[49,3226,22,2,19])). % 180.75/180.81 cnf(3974,plain, % 180.75/180.81 (E(f4(x39741,x39741),x39741)), % 180.75/180.81 inference(rename_variables,[],[22])). % 180.75/180.81 cnf(3975,plain, % 180.75/180.81 (~P2(f10(a9,a6),f4(a8,a8))), % 180.75/180.81 inference(scs_inference,[],[1436,49,3226,22,3974,2,19,20])). % 180.75/180.81 cnf(3976,plain, % 180.75/180.81 (E(f4(x39761,x39761),x39761)), % 180.75/180.81 inference(rename_variables,[],[22])). % 180.75/180.81 cnf(3977,plain, % 180.75/180.81 (~E(f10(x39771,a6),f4(a8,x39772))), % 180.75/180.81 inference(scs_inference,[],[26,1436,49,3226,2629,22,3974,2,19,20,35])). % 180.75/180.81 cnf(3978,plain, % 180.75/180.81 (P3(x39781,f10(x39782,x39781))), % 180.75/180.81 inference(rename_variables,[],[2629])). % 180.75/180.81 cnf(3985,plain, % 180.75/180.81 (E(f4(x39851,x39851),x39851)), % 180.75/180.81 inference(rename_variables,[],[22])). % 180.75/180.81 cnf(3987,plain, % 180.75/180.81 (E(f4(x39871,x39871),x39871)), % 180.75/180.81 inference(rename_variables,[],[22])). % 180.75/180.81 cnf(3989,plain, % 180.75/180.81 (~E(a8,f10(x39891,a6))), % 180.75/180.81 inference(scs_inference,[],[26,72,1436,49,3226,21,2629,3978,22,3974,3976,3985,3987,2,19,20,35,34,16,17,31,30])). % 180.75/180.81 cnf(3995,plain, % 180.75/180.81 (~P2(f4(a8,a8),f10(a9,a6))), % 180.75/180.81 inference(scs_inference,[],[3973,3977,23,2,20])). % 180.75/180.81 cnf(3996,plain, % 180.75/180.81 (E(f10(x39961,x39962),f10(x39962,x39961))), % 180.75/180.81 inference(rename_variables,[],[23])). % 180.75/180.81 cnf(3997,plain, % 180.75/180.81 (~P2(f10(a6,a9),f4(a8,a8))), % 180.75/180.81 inference(scs_inference,[],[3973,3975,3977,23,3996,2,20,19])). % 180.75/180.81 cnf(3999,plain, % 180.75/180.81 (~E(a1,a5)), % 180.75/180.81 inference(scs_inference,[],[3973,3975,3977,25,21,23,3996,2,20,19,16])). % 180.75/180.81 cnf(4000,plain, % 180.75/180.81 (~E(f4(x40001,a8),f10(x40002,a6))), % 180.75/180.81 inference(scs_inference,[],[3973,3975,3977,25,21,24,23,3996,2,20,19,16,3])). % 180.75/180.81 cnf(4002,plain, % 180.75/180.81 (~E(f10(x40021,a1),f10(a5,a5))), % 180.75/180.81 inference(scs_inference,[],[3973,3975,3977,25,21,2629,24,23,3996,2,20,19,16,3,33])). % 180.75/180.81 cnf(4005,plain, % 180.75/180.81 (~E(a5,a1)), % 180.75/180.81 inference(scs_inference,[],[3999,2])). % 180.75/180.81 cnf(4006,plain, % 180.75/180.81 (~E(f10(a6,x40061),f4(x40062,a8))), % 180.75/180.81 inference(scs_inference,[],[26,3999,2657,2,34])). % 180.75/180.81 cnf(4007,plain, % 180.75/180.81 (P3(x40071,f10(x40071,x40072))), % 180.75/180.81 inference(rename_variables,[],[2657])). % 180.75/180.81 cnf(4009,plain, % 180.75/180.81 (~E(f10(a6,x40091),f4(a8,x40092))), % 180.75/180.81 inference(scs_inference,[],[26,3999,2657,4007,2,34,35])). % 180.75/180.81 cnf(4010,plain, % 180.75/180.81 (P3(x40101,f10(x40101,x40102))), % 180.75/180.81 inference(rename_variables,[],[2657])). % 180.75/180.81 cnf(4014,plain, % 180.75/180.81 (~E(f4(a1,a1),f4(a5,a5))), % 180.75/180.81 inference(scs_inference,[],[26,3999,72,99,2657,4007,55,2,34,35,3,16])). % 180.75/180.81 cnf(4015,plain, % 180.75/180.81 (~E(f10(a1,x40151),f10(a5,a5))), % 180.75/180.81 inference(scs_inference,[],[26,3999,72,99,2657,4007,4010,55,2,34,35,3,16,33])). % 180.75/180.81 cnf(4019,plain, % 180.75/180.81 (~E(f4(a5,a5),a1)), % 180.75/180.81 inference(scs_inference,[],[4005,4015,55,2,3])). % 180.75/180.81 cnf(4024,plain, % 180.75/180.81 (~E(f4(x40241,a8),f10(a6,x40242))), % 180.75/180.81 inference(scs_inference,[],[4006,2])). % 180.75/180.81 cnf(4034,plain, % 180.75/180.81 (~E(f4(a5,a5),f4(a1,a1))), % 180.75/180.81 inference(scs_inference,[],[4014,2])). % 180.75/180.81 cnf(4038,plain, % 180.75/180.81 (~E(f4(a8,x40381),f10(a6,x40382))), % 180.75/180.81 inference(scs_inference,[],[4009,2])). % 180.75/180.81 cnf(4040,plain, % 180.75/180.81 (~P3(f4(a6,a6),f4(x40401,a8))), % 180.75/180.81 inference(scs_inference,[],[4002,51,22,2,17])). % 180.75/180.81 cnf(4046,plain, % 180.75/180.81 (~E(a8,f10(a9,x40461))), % 180.75/180.81 inference(scs_inference,[],[3238,2])). % 180.75/180.81 cnf(4049,plain, % 180.75/180.81 (~E(f4(x40491,a8),f10(x40492,a9))), % 180.75/180.81 inference(scs_inference,[],[3352,2])). % 180.75/180.81 cnf(4050,plain, % 180.75/180.81 (~E(f4(a8,x40501),f10(a9,x40502))), % 180.75/180.81 inference(scs_inference,[],[3280,2])). % 180.75/180.81 cnf(4054,plain, % 180.75/180.81 (~E(f4(x40541,a8),f10(a9,x40542))), % 180.75/180.81 inference(scs_inference,[],[3596,2])). % 180.75/180.81 cnf(4055,plain, % 180.75/180.81 (~P3(f4(a9,a9),f4(a8,x40551))), % 180.75/180.81 inference(scs_inference,[],[80,22,17])). % 180.75/180.81 cnf(4057,plain, % 180.75/180.81 (E(f10(x40571,f4(x40572,x40572)),f10(x40571,x40572))), % 180.75/180.81 inference(scs_inference,[],[55,2,7])). % 180.75/180.81 cnf(4058,plain, % 180.75/180.81 (E(f3(f4(x40581,x40581),x40582,x40583),f3(x40581,x40582,x40583))), % 180.75/180.81 inference(scs_inference,[],[55,2,8])). % 180.75/180.81 cnf(4064,plain, % 180.75/180.81 (E(f7(f4(x40641,x40641),x40642),f7(x40641,x40642))), % 180.75/180.81 inference(scs_inference,[],[55,2,14])). % 180.75/180.81 cnf(4075,plain, % 180.75/180.81 (P3(f4(x40751,x40752),f4(f10(f4(x40752,x40751),x40753),f10(f4(x40752,x40751),x40753)))), % 180.75/180.81 inference(scs_inference,[],[55,24,2,31])). % 180.75/180.81 cnf(4082,plain, % 180.75/180.81 (~E(f4(f10(x40821,a6),f10(x40821,a6)),f4(x40822,a8))), % 180.75/180.81 inference(scs_inference,[],[4000,55,2,3])). % 180.75/180.81 cnf(4091,plain, % 180.75/180.81 (~P2(f10(x40911,x40912),f4(f10(x40913,x40912),f10(x40913,x40912)))), % 180.75/180.81 inference(scs_inference,[],[55,2635,2,20])). % 180.75/180.81 cnf(4130,plain, % 180.75/180.81 (~E(f4(f10(a6,x41301),f10(a6,x41301)),f4(a8,x41302))), % 180.75/180.81 inference(scs_inference,[],[4038,55,2,3])). % 180.75/180.81 cnf(4150,plain, % 180.75/180.81 (~E(f4(f4(a1,a1),f4(a1,a1)),f4(a5,a5))), % 180.75/180.81 inference(scs_inference,[],[4034,55,2,3])). % 180.75/180.81 cnf(4174,plain, % 180.75/180.81 (~P2(f4(f10(x41741,x41742),f10(x41741,x41742)),f10(x41743,x41742))), % 180.75/180.81 inference(scs_inference,[],[2635,22,29,20])). % 180.75/180.81 cnf(4175,plain, % 180.75/180.81 (P3(f7(f10(x41751,x41752),f10(x41751,x41753)),f4(f10(x41751,x41752),f10(x41751,x41753)))), % 180.75/180.81 inference(scs_inference,[],[2462,29,36])). % 180.75/180.81 cnf(4177,plain, % 180.75/180.81 (P3(f7(f10(x41771,x41772),f10(x41772,x41773)),f4(f10(x41771,x41772),f10(x41772,x41773)))), % 180.75/180.81 inference(scs_inference,[],[2481,29,36])). % 180.75/180.81 cnf(4179,plain, % 180.75/180.81 (P3(f7(a8,f10(a9,a6)),f4(a8,f10(a9,a6)))), % 180.75/180.81 inference(scs_inference,[],[1436,29,36])). % 180.75/180.81 cnf(4192,plain, % 180.75/180.81 (~P3(f10(f4(x41921,x41922),x41923),f4(x41922,x41921))), % 180.75/180.81 inference(scs_inference,[],[2657,24,32,18])). % 180.75/180.81 cnf(4199,plain, % 180.75/180.81 (~P2(x41991,x41992)+~P3(x41993,f4(x41992,x41991))), % 180.75/180.81 inference(scs_inference,[],[38,29])). % 180.75/180.81 cnf(4200,plain, % 180.75/180.81 (~P3(x42001,f4(x42002,x42003))+P3(f7(x42003,x42002),f4(x42003,x42002))), % 180.75/180.81 inference(scs_inference,[],[4199,36])). % 180.75/180.81 cnf(4201,plain, % 180.75/180.82 (~P3(f4(x42011,x42012),f7(x42011,x42012))+~P3(x42013,f4(x42012,x42011))), % 180.75/180.82 inference(scs_inference,[],[4200,32])). % 180.75/180.82 cnf(4202,plain, % 180.75/180.82 (~P3(x42021,f4(x42022,x42023))+~P3(f4(x42023,x42022),f4(x42024,f7(x42023,x42022)))), % 180.75/180.82 inference(scs_inference,[],[4201,46])). % 180.75/180.82 cnf(4203,plain, % 180.75/180.82 (P3(f7(x42031,x42032),f4(x42031,x42032))+~P3(x42033,f4(x42031,x42032))), % 180.75/180.82 inference(scs_inference,[],[38,36])). % 180.75/180.82 cnf(4204,plain, % 180.75/180.82 (~P3(f4(x42041,x42042),f7(x42041,x42042))+~P3(x42043,f4(x42041,x42042))), % 180.75/180.82 inference(scs_inference,[],[4203,32])). % 180.75/180.82 cnf(4205,plain, % 180.75/180.82 (~P3(x42051,f4(x42052,x42053))+~P3(f4(x42052,x42053),f4(x42054,f7(x42052,x42053)))), % 180.75/180.82 inference(scs_inference,[],[4204,46])). % 180.75/180.82 cnf(4206,plain, % 180.75/180.82 (~P2(f4(x42061,x42062),x42063)+~P3(x42064,f4(f4(x42062,x42061),x42063))), % 180.75/180.82 inference(scs_inference,[],[24,38,19])). % 180.75/180.82 cnf(4207,plain, % 180.75/180.82 (~P2(f10(x42071,x42072),x42073)+~P3(x42074,f4(f10(x42072,x42071),x42073))), % 180.75/180.82 inference(scs_inference,[],[23,38,19])). % 180.75/180.82 cnf(4208,plain, % 180.75/180.82 (~P2(x42081,f4(x42082,x42083))+~P3(x42084,f4(x42081,f4(x42083,x42082)))), % 180.75/180.82 inference(scs_inference,[],[24,38,20])). % 180.75/180.82 cnf(4210,plain, % 180.75/180.82 (P3(f7(f4(a8,a8),f10(a6,a9)),f10(a6,a9))), % 180.75/180.82 inference(scs_inference,[],[3973,46,36])). % 180.75/180.82 cnf(4212,plain, % 180.75/180.82 (P3(f7(f10(a9,a6),f4(a8,a8)),f4(a8,a8))), % 180.75/180.82 inference(scs_inference,[],[3975,46,36])). % 180.75/180.82 cnf(4216,plain, % 180.75/180.82 (P3(f7(f10(a6,a9),f4(a8,a8)),f4(a8,a8))), % 180.75/180.82 inference(scs_inference,[],[3997,46,36])). % 180.75/180.82 cnf(4224,plain, % 180.75/180.82 (P3(f7(f10(a9,a6),a8),a8)), % 180.75/180.82 inference(scs_inference,[],[1436,46,36])). % 180.75/180.82 cnf(4230,plain, % 180.75/180.82 (P3(f7(a8,f10(a9,a6)),f10(a9,a6))), % 180.75/180.82 inference(scs_inference,[],[1435,46,36])). % 180.75/180.82 cnf(4340,plain, % 180.75/180.82 (P3(f7(f4(a8,a8),f10(a9,a6)),f4(a8,a8))), % 180.75/180.82 inference(scs_inference,[],[3995,47,36])). % 180.75/180.82 cnf(4344,plain, % 180.75/180.82 (P3(f7(f4(a8,a8),f10(a6,a9)),f4(a8,a8))), % 180.75/180.82 inference(scs_inference,[],[3973,47,36])). % 180.75/180.82 cnf(4346,plain, % 180.75/180.82 (P3(f7(f10(a9,a6),f4(a8,a8)),f10(a9,a6))), % 180.75/180.82 inference(scs_inference,[],[3975,47,36])). % 180.75/180.82 cnf(4360,plain, % 180.75/180.82 (P3(f7(f10(a9,a6),a8),f10(a9,a6))), % 180.75/180.82 inference(scs_inference,[],[1436,47,36])). % 180.75/180.82 cnf(4362,plain, % 180.75/180.82 (P3(f7(f10(a6,a9),a8),f10(a6,a9))), % 180.75/180.82 inference(scs_inference,[],[28,47,36])). % 180.75/180.82 cnf(4481,plain, % 180.75/180.82 (~E(f4(f4(x44811,a8),x44812),f4(f10(x44813,a6),f10(x44813,a6)))), % 180.75/180.82 inference(scs_inference,[],[4040,59,47,37])). % 180.75/180.82 cnf(4495,plain, % 180.75/180.82 (~P2(f4(x44951,x44952),x44953)+~P3(x44954,f4(x44953,f4(x44952,x44951)))), % 180.75/180.82 inference(scs_inference,[],[24,4199,19])). % 180.75/180.82 cnf(4545,plain, % 180.75/180.82 (~E(f10(x45451,f4(x45452,a8)),f10(f10(x45453,a9),x45454))+E(f4(f4(x45452,a8),x45455),f4(x45454,x45455))), % 180.75/180.82 inference(scs_inference,[],[2629,4049,4,33])). % 180.75/180.82 cnf(4551,plain, % 180.75/180.82 (~E(f10(x45511,f4(x45512,a8)),f10(f10(a9,x45513),x45514))+E(f4(f4(x45512,a8),x45515),f4(x45514,x45515))), % 180.75/180.82 inference(scs_inference,[],[4054,2629,4,33])). % 180.75/180.82 cnf(4556,plain, % 180.75/180.82 (E(x45561,f4(f4(x45561,x45561),x45561))), % 180.75/180.82 inference(scs_inference,[],[55,4,3])). % 180.75/180.82 cnf(4557,plain, % 180.75/180.82 (~E(f10(f10(a1,x45571),x45572),f10(x45573,f10(a5,a5)))+E(f4(f10(a1,x45571),x45574),f4(x45573,x45574))), % 180.75/180.82 inference(scs_inference,[],[4015,2657,4,33])). % 180.75/180.82 cnf(4560,plain, % 180.75/180.82 (~E(f10(x45601,a8),f10(f10(x45602,a6),x45603))+E(f4(a8,x45604),f4(x45603,x45604))), % 180.75/180.82 inference(scs_inference,[],[3989,2629,4,33])). % 180.75/180.82 cnf(4562,plain, % 180.75/180.82 (~E(f10(f10(x45621,a9),x45622),f10(x45623,a8))+E(f4(f10(x45621,a9),x45624),f4(x45623,x45624))), % 180.75/180.82 inference(scs_inference,[],[2657,3226,4,33])). % 180.75/180.82 cnf(4564,plain, % 180.75/180.82 (~E(f10(x45641,f10(a9,x45642)),f10(a8,x45643))+E(f4(f10(a9,x45642),x45644),f4(x45643,x45644))), % 180.75/180.82 inference(scs_inference,[],[3238,2629,4,33])). % 180.75/180.82 cnf(4589,plain, % 180.75/180.82 (~E(f10(x45891,f10(x45892,a6)),f10(a8,x45893))+E(f4(x45894,f10(x45892,a6)),f4(x45894,x45893))), % 180.75/180.82 inference(scs_inference,[],[2639,2629,5,33])). % 180.75/180.82 cnf(4591,plain, % 180.75/180.82 (E(f10(f4(x45911,x45912),x45913),f10(f4(x45911,f4(x45912,x45912)),x45913))), % 180.75/180.82 inference(scs_inference,[],[55,5,6])). % 180.75/180.82 cnf(4601,plain, % 180.75/180.82 (E(f10(x46011,f4(x46012,x46013)),f10(x46011,f4(x46012,f4(x46013,x46013))))), % 180.75/180.82 inference(scs_inference,[],[55,5,7])). % 180.75/180.82 cnf(4614,plain, % 180.75/180.82 (~E(f10(a8,x46141),f10(x46142,f10(x46143,a6)))+E(f4(x46144,a8),f4(x46144,x46142))), % 180.75/180.82 inference(scs_inference,[],[2657,3989,5,33])). % 180.75/180.82 cnf(4616,plain, % 180.75/180.82 (P3(f4(x46161,f4(x46162,x46162)),f10(x46163,f4(x46161,x46162)))), % 180.75/180.82 inference(scs_inference,[],[55,2629,5,17])). % 180.75/180.82 cnf(4620,plain, % 180.75/180.82 (~E(f4(x46201,f4(a8,a8)),f10(a6,x46202))), % 180.75/180.82 inference(scs_inference,[],[55,4024,5,3])). % 180.75/180.82 cnf(4621,plain, % 180.75/180.82 (~P3(f10(a6,x46211),f4(f10(f4(x46212,a8),x46213),f10(f4(x46212,a8),x46213)))+E(f4(x46214,f10(a6,x46211)),f4(x46214,x46213))), % 180.75/180.82 inference(scs_inference,[],[22,4006,5,33])). % 180.75/180.82 cnf(4623,plain, % 180.75/180.82 (~P3(f10(a1,x46231),f4(f10(f10(a5,a5),x46232),f10(f10(a5,a5),x46232)))+E(f4(x46233,f10(a1,x46231)),f4(x46233,x46232))), % 180.75/180.82 inference(scs_inference,[],[4015,22,5,33])). % 180.75/180.82 cnf(4624,plain, % 180.75/180.82 (~E(f10(f4(a5,a5),x46241),f10(x46242,a1))+E(f4(x46243,f4(a5,a5)),f4(x46243,x46242))), % 180.75/180.82 inference(scs_inference,[],[2657,4019,5,33])). % 180.75/180.82 cnf(4632,plain, % 180.75/180.82 (~E(f10(x46321,f4(a8,x46322)),f10(f10(a6,x46323),x46324))+E(f4(x46325,f4(a8,x46322)),f4(x46325,x46324))), % 180.75/180.82 inference(scs_inference,[],[2629,4038,5,33])). % 180.75/180.82 cnf(4636,plain, % 180.75/180.82 (~E(f10(x46361,a8),f10(f10(a9,x46362),x46363))+E(f4(x46364,a8),f4(x46364,x46363))), % 180.75/180.82 inference(scs_inference,[],[2629,4046,5,33])). % 180.75/180.82 cnf(4640,plain, % 180.75/180.82 (~P3(a8,f4(f10(x46401,f10(a9,x46402)),f10(x46401,f10(a9,x46402))))+E(f4(x46403,a8),f4(x46403,x46401))), % 180.75/180.82 inference(scs_inference,[],[4046,22,5,33])). % 180.75/180.82 cnf(4646,plain, % 180.75/180.82 (~E(f10(f10(x46461,a6),x46462),f10(x46463,a8))+E(f4(x46464,f10(x46461,a6)),f4(x46464,x46463))), % 180.75/180.82 inference(scs_inference,[],[2657,2639,5,33])). % 180.75/180.82 cnf(4654,plain, % 180.75/180.82 (~E(f10(f10(a1,x46541),x46542),f10(x46543,f10(a5,a5)))+E(f4(x46544,f10(a1,x46541)),f4(x46544,x46543))), % 180.75/180.82 inference(scs_inference,[],[2657,4015,5,33])). % 180.75/180.82 cnf(4656,plain, % 180.75/180.82 (~E(f10(x46561,f4(x46562,a8)),f10(f10(a6,x46563),x46564))+E(f4(x46565,f4(x46562,a8)),f4(x46565,x46564))), % 180.75/180.82 inference(scs_inference,[],[2629,4024,5,33])). % 180.75/180.82 cnf(4658,plain, % 180.75/180.82 (~E(f10(f4(a8,x46581),x46582),f10(x46583,f10(a6,x46584)))+E(f4(x46585,f4(a8,x46581)),f4(x46585,x46583))), % 180.75/180.82 inference(scs_inference,[],[2657,4038,5,33])). % 180.75/180.82 cnf(4660,plain, % 180.75/180.82 (E(f10(f4(x46601,f4(x46602,x46602)),x46603),f10(f4(x46601,x46602),x46603))), % 180.75/180.82 inference(scs_inference,[],[22,5,6])). % 180.75/180.82 cnf(4662,plain, % 180.75/180.82 (~P3(a8,f4(f10(f10(x46621,a6),x46622),f10(f10(x46621,a6),x46622)))+E(f4(x46623,a8),f4(x46623,x46622))), % 180.75/180.82 inference(scs_inference,[],[3989,22,5,33])). % 180.75/180.82 cnf(4741,plain, % 180.75/180.82 (E(f10(x47411,f4(f4(x47412,x47412),x47413)),f10(x47411,f4(x47412,x47413)))), % 180.75/180.82 inference(scs_inference,[],[22,7,4])). % 180.75/180.82 cnf(4910,plain, % 180.75/180.82 (~E(f10(x49101,f4(x49102,a8)),f10(f10(x49103,a9),x49104))+E(f7(x49105,f4(x49102,a8)),f7(x49105,x49104))), % 180.75/180.82 inference(scs_inference,[],[2629,4049,15,33])). % 180.75/180.82 cnf(4912,plain, % 180.75/180.82 (~E(f10(f4(a8,x49121),x49122),f10(x49123,f10(a9,x49124)))+E(f7(x49125,f4(a8,x49121)),f7(x49125,x49123))), % 180.75/180.82 inference(scs_inference,[],[2657,4050,15,33])). % 180.75/180.82 cnf(4951,plain, % 180.75/180.82 (P3(f7(f4(a8,a8),f10(a9,a6)),f4(f4(a8,a8),f10(a9,a6)))), % 180.75/180.82 inference(scs_inference,[],[3975,36,29])). % 180.75/180.82 cnf(4956,plain, % 180.75/180.82 (P3(f7(f10(x49561,x49562),f10(x49563,x49561)),f4(f4(f10(x49561,x49562),f10(x49563,x49561)),f4(f10(x49561,x49562),f10(x49563,x49561))))), % 180.75/180.82 inference(scs_inference,[],[2481,36,48])). % 180.75/180.82 cnf(4957,plain, % 180.75/180.82 (P3(f7(f10(a9,a6),a8),f4(f10(a9,a6),a8))), % 180.75/180.82 inference(scs_inference,[],[1435,36,29])). % 180.75/180.82 cnf(4963,plain, % 180.75/180.82 (P3(f7(f10(x49631,x49632),f4(f10(x49632,x49633),f10(x49632,x49633))),f4(f10(x49631,x49632),f4(f10(x49632,x49633),f10(x49632,x49633))))), % 180.75/180.82 inference(scs_inference,[],[2477,22,36,20])). % 180.75/180.82 cnf(4971,plain, % 180.75/180.82 (P3(f7(f10(a6,a9),a8),a8)), % 180.75/180.82 inference(scs_inference,[],[28,36,46])). % 180.75/180.82 cnf(4973,plain, % 180.75/180.82 (P3(f7(f4(f4(a8,a8),f4(a8,a8)),f10(a6,a9)),f4(f4(f4(a8,a8),f4(a8,a8)),f10(a6,a9)))), % 180.75/180.82 inference(scs_inference,[],[3973,22,36,19])). % 180.75/180.82 cnf(4975,plain, % 180.75/180.82 (P3(f7(f4(f4(a8,a8),f4(a8,a8)),f10(a9,a6)),f4(f4(f4(a8,a8),f4(a8,a8)),f10(a9,a6)))), % 180.75/180.82 inference(scs_inference,[],[3995,22,36,19])). % 180.75/180.82 cnf(4985,plain, % 180.75/180.82 (~E(f7(f10(a6,a9),a8),a6)), % 180.75/180.82 inference(scs_inference,[],[28,51,36,17])). % 180.75/180.82 cnf(4987,plain, % 180.75/180.82 (~E(f7(f4(a8,a8),f10(a9,a6)),f10(f4(a8,a8),x49871))), % 180.75/180.82 inference(scs_inference,[],[3995,310,36,17])). % 180.75/180.82 cnf(4994,plain, % 180.75/180.82 (E(f7(f10(x49941,x49941),f10(x49941,x49941)),x49941)), % 180.75/180.82 inference(scs_inference,[],[2481,22,36,33])). % 180.75/180.82 cnf(4995,plain, % 180.75/180.82 (~E(f7(a8,f10(a9,a6)),a6)), % 180.75/180.82 inference(scs_inference,[],[1435,53,36,17])). % 180.75/180.82 cnf(4997,plain, % 180.75/180.82 (P3(f7(f10(a6,a9),a8),f4(a8,f10(a6,a9)))), % 180.75/180.82 inference(scs_inference,[],[28,24,36,18])). % 180.75/180.82 cnf(5000,plain, % 180.75/180.82 (E(f7(f10(a9,a6),f4(a8,a8)),x50001)+E(f7(f10(a9,a6),f4(a8,a8)),x50002)+~E(f4(f10(a9,a6),f4(a8,a8)),f10(x50002,x50001))), % 180.75/180.82 inference(scs_inference,[],[3975,36,33])). % 180.75/180.82 cnf(5010,plain, % 180.75/180.82 (~E(f7(f10(a9,a6),f4(a8,a8)),f10(f10(a9,a6),x50101))), % 180.75/180.82 inference(scs_inference,[],[3975,310,36,17])). % 180.75/180.82 cnf(5017,plain, % 180.75/180.82 (~E(f7(a8,f10(a9,a6)),f4(a9,a9))), % 180.75/180.82 inference(scs_inference,[],[1435,4055,36,17])). % 180.75/180.82 cnf(5371,plain, % 180.75/180.82 (P3(f7(x53711,x53712),x53712)+~P3(x53713,f4(x53712,x53711))), % 180.75/180.82 inference(scs_inference,[],[4200,46])). % 180.75/180.82 cnf(5372,plain, % 180.75/180.82 (~P3(x53721,f7(x53722,x53721))+~P3(x53723,f4(x53721,x53722))), % 180.75/180.82 inference(scs_inference,[],[5371,32])). % 180.75/180.82 cnf(5374,plain, % 180.75/180.82 (~P3(x53741,f4(f4(x53742,x53743),x53744))+~P2(x53742,x53743)), % 180.75/180.82 inference(scs_inference,[],[5371,38])). % 180.75/180.82 cnf(5375,plain, % 180.75/180.82 (P3(f7(x53751,f4(x53752,x53753)),x53752)+~P3(x53754,f4(f4(x53752,x53753),x53751))), % 180.75/180.82 inference(scs_inference,[],[5371,47])). % 180.75/180.82 cnf(5376,plain, % 180.75/180.82 (~P3(x53761,f4(f4(x53762,x53763),x53764))+~P2(x53763,x53762)), % 180.75/180.82 inference(scs_inference,[],[5371,4199])). % 180.75/180.82 cnf(5381,plain, % 180.75/180.82 (~P3(x53811,f4(a8,x53812))+~E(f7(x53812,a8),a9)), % 180.75/180.82 inference(scs_inference,[],[27,5371,17])). % 180.75/180.82 cnf(5382,plain, % 180.75/180.82 (~E(f7(f10(a6,a9),a8),a9)), % 180.75/180.82 inference(scs_inference,[],[49,5381,36])). % 180.75/180.82 cnf(5383,plain, % 180.75/180.82 (~P3(x53831,f4(f4(x53832,x53833),x53834))+P3(f7(x53834,f4(x53832,x53833)),f4(x53833,x53832))), % 180.75/180.82 inference(scs_inference,[],[24,5371,18])). % 180.75/180.82 cnf(5384,plain, % 180.75/180.82 (P3(f7(f4(f10(x53841,x53842),f10(x53841,x53842)),f4(f10(x53841,x53842),f10(x53841,x53842))),f4(f10(x53841,x53842),f10(x53841,x53842)))), % 180.75/180.82 inference(scs_inference,[],[56,22,5371,37])). % 180.75/180.82 cnf(5385,plain, % 180.75/180.82 (~P3(x53851,f4(x53852,x53853))+P3(f4(f7(x53853,x53852),f7(x53853,x53852)),x53852)), % 180.75/180.82 inference(scs_inference,[],[55,5371,17])). % 180.75/180.82 cnf(5386,plain, % 180.75/180.82 (~P3(x53861,f4(f10(x53862,x53863),x53864))+P3(f7(x53864,f10(x53862,x53863)),f10(x53863,x53862))), % 180.75/180.82 inference(scs_inference,[],[23,5371,18])). % 180.75/180.82 cnf(5387,plain, % 180.75/180.82 (~P3(x53871,f4(f4(x53872,x53873),x53874))+P3(f7(x53874,f4(x53872,x53873)),x53873)), % 180.75/180.82 inference(scs_inference,[],[24,5371,35])). % 180.75/180.82 cnf(5388,plain, % 180.75/180.82 (P3(f7(x53881,x53882),f4(f10(f7(x53881,x53882),x53883),x53882))+~P3(x53884,f4(x53882,x53881))), % 180.75/180.82 inference(scs_inference,[],[2657,5371,48])). % 180.75/180.82 cnf(5389,plain, % 180.75/180.82 (P3(f7(x53891,x53892),f4(f10(x53893,f7(x53891,x53892)),x53892))+~P3(x53894,f4(x53892,x53891))), % 180.75/180.82 inference(scs_inference,[],[2629,5371,48])). % 180.75/180.82 cnf(5390,plain, % 180.75/180.82 (P3(f7(x53901,x53902),f4(x53902,f10(f7(x53901,x53902),x53903)))+~P3(x53904,f4(x53902,x53901))), % 180.75/180.82 inference(scs_inference,[],[2657,5371,48])). % 180.75/180.82 cnf(5391,plain, % 180.75/180.82 (P3(f7(x53911,x53912),f4(x53912,f10(x53913,f7(x53911,x53912))))+~P3(x53914,f4(x53912,x53911))), % 180.75/180.82 inference(scs_inference,[],[2629,5371,48])). % 180.75/180.82 cnf(5392,plain, % 180.75/180.82 (~P3(x53921,f4(x53922,x53923))+P3(f7(x53923,x53922),f4(f4(f10(f7(x53923,x53922),x53924),x53922),f4(f10(f7(x53923,x53922),x53924),x53922)))), % 180.75/180.82 inference(scs_inference,[],[2657,22,5371,37])). % 180.75/180.82 cnf(5393,plain, % 180.75/180.82 (~P3(x53931,f4(f10(x53932,x53933),x53934))+E(f7(x53934,f10(x53932,x53933)),x53932)+E(f7(x53934,f10(x53932,x53933)),x53933)), % 180.75/180.82 inference(scs_inference,[],[23,5371,33])). % 180.75/180.82 cnf(5394,plain, % 180.75/180.82 (~P3(x53941,f4(x53942,x53943))+P3(f7(x53943,x53942),f4(x53942,x53942))), % 180.75/180.82 inference(scs_inference,[],[55,5371,18])). % 180.75/180.82 cnf(5395,plain, % 180.75/180.82 (~P3(f4(x53951,x53951),f7(x53952,x53951))+~P3(x53953,f4(x53951,x53952))), % 180.75/180.82 inference(scs_inference,[],[5394,32])). % 180.75/180.82 cnf(5396,plain, % 180.75/180.82 (~P3(x53961,f4(x53962,x53963))+~E(f7(x53963,x53962),f10(x53964,f4(x53962,x53962)))), % 180.75/180.82 inference(scs_inference,[],[24,5395,30])). % 180.75/180.82 cnf(5397,plain, % 180.75/180.82 (~P3(f4(x53971,x53971),f7(x53972,x53971))+~P3(x53973,f4(f4(x53971,x53972),x53974))), % 180.75/180.82 inference(scs_inference,[],[5371,5395])). % 180.75/180.82 cnf(5398,plain, % 180.75/180.82 (~P3(x53981,f4(x53982,x53983))+P3(f7(x53983,x53982),f4(f4(f10(x53984,f7(x53983,x53982)),x53982),f4(f10(x53984,f7(x53983,x53982)),x53982)))), % 180.75/180.82 inference(scs_inference,[],[2629,22,5371,37])). % 180.75/180.82 cnf(5400,plain, % 180.75/180.82 (~P3(x54001,f4(x54002,x54003))+~P3(x54002,f4(x54004,f7(x54003,x54002)))), % 180.75/180.82 inference(scs_inference,[],[5372,46])). % 180.75/180.82 cnf(5402,plain, % 180.75/180.82 (~P3(f10(x54021,x54022),f7(x54023,f10(x54022,x54021)))+~P3(x54024,f4(f10(x54022,x54021),x54023))), % 180.75/180.82 inference(scs_inference,[],[23,5372,17])). % 180.75/180.82 cnf(5404,plain, % 180.75/180.82 (~P3(x54041,f7(x54042,f4(x54041,x54041)))+~P3(x54043,f4(f4(x54041,x54041),x54042))), % 180.75/180.82 inference(scs_inference,[],[55,5372,17])). % 180.75/180.82 cnf(5406,plain, % 180.75/180.82 (~P3(f4(x54061,x54062),f7(x54063,f4(x54062,x54061)))+~P3(x54064,f4(f4(x54062,x54061),x54063))), % 180.75/180.82 inference(scs_inference,[],[24,5372,17])). % 180.75/180.82 cnf(5408,plain, % 180.75/180.82 (~P3(x54081,f4(f10(x54082,x54083),x54084))+~E(f7(x54084,f10(x54082,x54083)),f10(x54085,f10(x54083,x54082)))), % 180.75/180.82 inference(scs_inference,[],[23,5372,30])). % 180.75/180.82 cnf(5410,plain, % 180.75/180.82 (~P3(x54101,f4(x54102,x54103))+~E(f7(x54103,x54102),f10(f4(x54102,x54102),x54104))), % 180.75/180.82 inference(scs_inference,[],[55,5372,31])). % 180.75/180.82 cnf(5412,plain, % 180.75/180.82 (~P3(x54121,f4(f4(x54122,x54122),x54123))+~E(f7(x54123,f4(x54122,x54122)),f10(x54124,x54122))), % 180.75/180.82 inference(scs_inference,[],[22,5372,30])). % 180.75/180.82 cnf(5414,plain, % 180.75/180.82 (~P3(x54141,f4(f4(x54142,x54143),x54144))+~E(f7(x54144,f4(x54142,x54143)),f10(x54145,f4(x54143,x54142)))), % 180.75/180.82 inference(scs_inference,[],[24,5372,30])). % 180.75/180.82 cnf(5416,plain, % 180.75/180.82 (~P3(x54161,f4(f10(x54162,x54163),x54164))+~E(f7(x54164,f10(x54162,x54163)),f10(f10(x54163,x54162),x54165))), % 180.75/180.82 inference(scs_inference,[],[23,5372,31])). % 180.75/180.82 cnf(5418,plain, % 180.75/180.82 (~P3(x54181,f4(f4(x54182,x54182),x54183))+~E(f10(x54182,x54184),f4(x54185,f7(x54183,f4(x54182,x54182))))), % 180.75/180.82 inference(scs_inference,[],[56,5372,34])). % 180.75/180.82 cnf(5420,plain, % 180.75/180.82 (~P3(x54201,f4(x54202,x54203))+~E(f10(x54202,x54204),f4(x54205,f7(x54203,x54202)))), % 180.75/180.82 inference(scs_inference,[],[2657,5372,34])). % 180.75/180.82 cnf(5422,plain, % 180.75/180.82 (~P3(x54221,f4(x54222,x54223))+~E(f10(x54224,x54222),f4(x54225,f7(x54223,x54222)))), % 180.75/180.82 inference(scs_inference,[],[2629,5372,34])). % 180.75/180.82 cnf(5424,plain, % 180.75/180.82 (~P3(x54241,f4(x54242,x54243))+~E(f10(x54242,x54244),f4(f7(x54243,x54242),x54245))), % 180.75/180.82 inference(scs_inference,[],[2657,5372,35])). % 180.75/180.82 cnf(5425,plain, % 180.75/180.82 (~P3(x54251,f4(x54252,x54253))+~E(f10(x54254,x54252),f4(f7(x54253,x54252),x54255))), % 180.75/180.82 inference(scs_inference,[],[2629,5372,35])). % 180.75/180.82 cnf(5426,plain, % 180.75/180.82 (~P3(x54261,f4(f4(x54262,x54262),x54263))+~E(f10(x54262,x54264),f4(f7(x54263,f4(x54262,x54262)),x54265))), % 180.75/180.82 inference(scs_inference,[],[56,5372,35])). % 180.75/180.82 cnf(5427,plain, % 180.75/180.82 (~P3(x54271,f4(x54272,x54273))+~E(f7(x54273,x54272),f4(f10(x54272,x54274),f10(x54272,x54274)))), % 180.75/180.82 inference(scs_inference,[],[2657,5372,37])). % 180.75/180.82 cnf(5428,plain, % 180.75/180.82 (~P3(x54281,f4(x54282,x54283))+~E(f7(x54283,x54282),f4(f10(x54284,x54282),f10(x54284,x54282)))), % 180.75/180.82 inference(scs_inference,[],[2629,5372,37])). % 180.75/180.82 cnf(5429,plain, % 180.75/180.82 (~P3(x54291,f4(f4(x54292,x54292),x54293))+~E(f7(x54293,f4(x54292,x54292)),f4(f10(x54292,x54294),f10(x54292,x54294)))), % 180.75/180.82 inference(scs_inference,[],[56,5372,37])). % 180.75/180.82 cnf(5430,plain, % 180.75/180.82 (~P3(f7(x54301,a8),f10(a9,a9))+~P3(x54302,f4(a8,x54301))), % 180.75/180.82 inference(scs_inference,[],[23,5381,33])). % 180.75/180.82 cnf(5432,plain, % 180.75/180.82 (~P3(x54321,a8)+~E(f7(a8,a8),a9)), % 180.75/180.82 inference(scs_inference,[],[55,5381,18])). % 180.75/180.82 cnf(5433,plain, % 180.75/180.82 (~P3(x54331,f4(x54332,a8))+~E(f7(a8,a8),a9)), % 180.75/180.82 inference(scs_inference,[],[5432,46])). % 180.75/180.82 cnf(5434,plain, % 180.75/180.82 (~E(f7(a8,a8),a9)), % 180.75/180.82 inference(scs_inference,[],[1436,5433,36])). % 180.75/180.82 cnf(5435,plain, % 180.75/180.82 (~E(a9,f7(a8,a8))), % 180.75/180.82 inference(scs_inference,[],[5434,2])). % 180.75/180.82 cnf(5438,plain, % 180.75/180.82 (~P3(f7(x54381,a8),f4(f10(a9,a9),f10(a9,a9)))+~P3(x54382,f4(a8,x54381))), % 180.75/180.82 inference(scs_inference,[],[22,5381,33])). % 180.75/180.82 cnf(5441,plain, % 180.75/180.82 (~P3(f7(a8,a8),f10(a9,a9))), % 180.75/180.82 inference(scs_inference,[],[5434,23,33])). % 180.75/180.82 cnf(5444,plain, % 180.75/180.82 (~P3(x54441,f4(a8,x54442))+~E(f10(f7(x54442,a8),x54443),f10(a9,a9))), % 180.75/180.82 inference(scs_inference,[],[2657,5381,33])). % 180.75/180.82 cnf(5446,plain, % 180.75/180.82 (~P3(x54461,f4(a8,x54462))+~E(f10(x54463,f7(x54462,a8)),f10(a9,a9))), % 180.75/180.82 inference(scs_inference,[],[2629,5381,33])). % 180.75/180.82 cnf(5447,plain, % 180.75/180.82 (~P3(x54471,f4(x54472,a8))+~E(f7(x54472,a8),a9)), % 180.75/180.82 inference(scs_inference,[],[5381,4200])). % 180.75/180.82 cnf(5462,plain, % 180.75/180.82 (~P3(x54621,a8)+~E(f7(f10(x54622,x54621),a8),a9)), % 180.75/180.82 inference(scs_inference,[],[2629,5381,48])). % 180.75/180.82 cnf(5464,plain, % 180.75/180.82 (~P3(x54641,a8)+~E(f7(f10(x54641,x54642),a8),a9)), % 180.75/180.82 inference(scs_inference,[],[2657,5381,48])). % 180.75/180.82 cnf(5466,plain, % 180.75/180.82 (~P3(f7(x54661,a8),f4(f10(a9,a9),f10(a9,a9)))+~P3(x54662,f4(x54661,a8))), % 180.75/180.82 inference(scs_inference,[],[22,5447,33])). % 180.75/180.82 cnf(5468,plain, % 180.75/180.82 (~E(a9,f7(x54681,a8))+~P3(x54682,f4(x54681,a8))), % 180.75/180.82 inference(scs_inference,[],[5447,2])). % 180.75/180.82 cnf(5470,plain, % 180.75/180.82 (~E(f7(f10(a9,a6),a8),a9)), % 180.75/180.82 inference(scs_inference,[],[1436,5447,36])). % 180.75/180.82 cnf(5471,plain, % 180.75/180.82 (~P3(x54711,f4(x54712,a8))+~E(f10(f7(x54712,a8),x54713),f10(a9,a9))), % 180.75/180.82 inference(scs_inference,[],[2657,5447,33])). % 180.75/180.82 cnf(5473,plain, % 180.75/180.82 (~P3(f7(x54731,a8),f10(a9,a9))+~P3(x54732,f4(x54731,a8))), % 180.75/180.82 inference(scs_inference,[],[23,5447,33])). % 180.75/180.82 cnf(5474,plain, % 180.75/180.82 (~P3(f7(f10(a6,a9),a8),f10(a9,a9))), % 180.75/180.82 inference(scs_inference,[],[28,5473,36])). % 180.75/180.82 cnf(5487,plain, % 180.75/180.82 (~P3(x54871,f4(x54872,a8))+~E(f10(x54873,f7(x54872,a8)),f10(a9,a9))), % 180.75/180.82 inference(scs_inference,[],[2629,5447,33])). % 180.75/180.82 cnf(5490,plain, % 180.75/180.82 (~P3(x54901,f4(x54902,a8))+~E(f10(x54903,a9),f10(f7(x54902,a8),f7(x54902,a8)))), % 180.75/180.82 inference(scs_inference,[],[2629,5468,33])). % 180.75/180.82 cnf(5492,plain, % 180.75/180.82 (~P3(a9,f10(f7(x54921,a8),f7(x54921,a8)))+~P3(x54922,f4(x54921,a8))), % 180.75/180.82 inference(scs_inference,[],[23,5468,33])). % 180.75/180.82 cnf(5494,plain, % 180.75/180.82 (~P3(x54941,f4(a8,x54942))+~E(a9,f7(x54942,a8))), % 180.75/180.82 inference(scs_inference,[],[5468,4200])). % 180.75/180.82 cnf(5496,plain, % 180.75/180.82 (~P3(x54961,f4(x54962,a8))+~E(f10(a9,x54963),f10(f7(x54962,a8),f7(x54962,a8)))), % 180.75/180.82 inference(scs_inference,[],[2657,5468,33])). % 180.75/180.82 cnf(5511,plain, % 180.75/180.82 (~P3(x55111,a8)+~E(a9,f7(f10(x55112,x55111),a8))), % 180.75/180.82 inference(scs_inference,[],[2629,5468,48])). % 180.75/180.82 cnf(5512,plain, % 180.75/180.82 (~P3(f4(x55121,x55121),a8)+~E(a9,f7(f10(x55121,x55122),a8))), % 180.75/180.82 inference(scs_inference,[],[56,5468,48])). % 180.75/180.82 cnf(5513,plain, % 180.75/180.82 (~P3(x55131,a8)+~E(a9,f7(f10(x55131,x55132),a8))), % 180.75/180.82 inference(scs_inference,[],[2657,5468,48])). % 180.75/180.82 cnf(5515,plain, % 180.75/180.82 (~P3(x55151,f4(a8,x55152))+~E(f10(x55153,a9),f10(f7(x55152,a8),f7(x55152,a8)))), % 180.75/180.82 inference(scs_inference,[],[2629,5494,33])). % 180.75/180.82 cnf(5517,plain, % 180.75/180.82 (~P3(a9,f4(f10(f7(x55171,a8),f7(x55171,a8)),f10(f7(x55171,a8),f7(x55171,a8))))+~P3(x55172,f4(a8,x55171))), % 180.75/180.82 inference(scs_inference,[],[22,5494,33])). % 180.75/180.82 cnf(5519,plain, % 180.75/180.82 (~P3(a9,f10(f7(x55191,a8),f7(x55191,a8)))+~P3(x55192,f4(a8,x55191))), % 180.75/180.82 inference(scs_inference,[],[23,5494,33])). % 180.75/180.82 cnf(5521,plain, % 180.75/180.82 (~P3(x55211,f4(a8,x55212))+~E(f10(a9,x55213),f10(f7(x55212,a8),f7(x55212,a8)))), % 180.75/180.82 inference(scs_inference,[],[2657,5494,33])). % 180.75/180.82 cnf(5535,plain, % 180.75/180.82 (~P3(x55351,f4(a8,a8))+~E(f4(a8,a8),f4(f10(a9,a9),x55352))), % 180.75/180.82 inference(scs_inference,[],[5441,4200,35])). % 180.75/180.82 cnf(5536,plain, % 180.75/180.82 (P3(f7(x55361,x55362),f4(f4(x55361,x55362),f4(x55361,x55362)))+~P3(x55363,f4(x55362,x55361))), % 180.75/180.82 inference(scs_inference,[],[4200,48])). % 180.75/180.82 cnf(5537,plain, % 180.75/180.82 (~P3(x55371,f4(x55372,x55373))+~P3(f4(x55373,x55372),f4(f7(x55373,x55372),x55374))), % 180.75/180.82 inference(scs_inference,[],[4201,47])). % 180.75/180.82 cnf(5538,plain, % 180.75/180.82 (~P3(x55381,f4(x55382,x55383))+~E(f7(x55383,x55382),f10(x55384,f4(f4(x55383,x55382),f4(x55383,x55382))))), % 180.75/180.82 inference(scs_inference,[],[55,4201,30])). % 180.75/180.82 cnf(5539,plain, % 180.75/180.82 (~P3(f4(x55391,x55392),f7(x55392,x55391))+~P3(x55393,f4(x55391,x55392))), % 180.75/180.82 inference(scs_inference,[],[24,4201,17])). % 180.75/180.82 cnf(5540,plain, % 180.75/180.82 (~P3(x55401,f4(x55402,x55403))+~P3(f4(x55402,x55403),f4(x55404,f7(x55403,x55402)))), % 180.75/180.82 inference(scs_inference,[],[5539,46])). % 180.75/180.82 cnf(5542,plain, % 180.75/180.82 (~P3(x55421,f4(x55422,x55423))+~E(f7(x55423,x55422),f10(f4(f4(x55423,x55422),f4(x55423,x55422)),x55424))), % 180.75/180.82 inference(scs_inference,[],[55,4201,31])). % 180.75/180.82 cnf(5543,plain, % 180.75/180.82 (~P3(x55431,f4(x55432,x55433))+~E(f7(x55433,x55432),f10(x55434,f4(x55432,x55433)))), % 180.75/180.82 inference(scs_inference,[],[24,4201,30])). % 180.75/180.82 cnf(5544,plain, % 180.75/180.82 (~P3(x55441,f4(x55442,x55443))+~E(f10(x55444,f4(x55443,x55442)),f4(x55445,f7(x55443,x55442)))), % 180.75/180.82 inference(scs_inference,[],[2629,4201,34])). % 180.75/180.82 cnf(5545,plain, % 180.75/180.82 (P3(f7(x55451,x55452),f4(f4(x55451,x55452),f4(x55451,x55452)))+~P3(x55453,f4(x55451,x55452))), % 180.75/180.82 inference(scs_inference,[],[4203,48])). % 180.75/180.82 cnf(5546,plain, % 180.75/180.82 (~P3(x55461,f4(x55462,x55463))+~P3(f4(x55462,x55463),f4(f7(x55462,x55463),x55464))), % 180.75/180.82 inference(scs_inference,[],[4204,47])). % 180.75/180.82 cnf(5547,plain, % 180.75/180.82 (~P3(x55471,f4(x55472,x55473))+~E(f7(x55472,x55473),f10(x55474,f4(f4(x55472,x55473),f4(x55472,x55473))))), % 180.75/180.82 inference(scs_inference,[],[55,4204,30])). % 180.75/180.82 cnf(5548,plain, % 180.75/180.82 (~P3(f4(f4(x55481,x55482),f4(x55481,x55482)),f7(x55481,x55482))+~P3(x55483,f4(x55481,x55482))), % 180.75/180.82 inference(scs_inference,[],[22,4204,17])). % 180.75/180.82 cnf(5549,plain, % 180.75/180.82 (~P3(f4(x55491,x55492),f7(x55492,x55491))+~P3(x55493,f4(x55492,x55491))), % 180.75/180.82 inference(scs_inference,[],[24,4204,17])). % 180.75/180.82 cnf(5550,plain, % 180.75/180.82 (~P3(x55501,f4(x55502,x55503))+~P3(f4(x55503,x55502),f4(x55504,f7(x55502,x55503)))), % 180.75/180.82 inference(scs_inference,[],[5549,46])). % 180.75/180.82 cnf(5551,plain, % 180.75/180.82 (~P3(x55511,f4(x55512,x55513))+~E(f7(x55512,x55513),f10(f4(f4(x55512,x55513),f4(x55512,x55513)),x55514))), % 180.75/180.82 inference(scs_inference,[],[55,4204,31])). % 180.75/180.82 cnf(5552,plain, % 180.93/180.82 (~P3(x55521,f4(x55522,x55522))+~E(f7(x55522,x55522),f10(x55523,x55522))), % 180.93/180.82 inference(scs_inference,[],[22,4204,30])). % 180.93/180.82 cnf(5553,plain, % 180.93/180.82 (~P3(x55531,f4(x55532,x55532))+~P3(f7(x55532,x55532),f10(f10(x55533,x55532),f10(x55533,x55532)))), % 180.93/180.82 inference(scs_inference,[],[23,5552,33])). % 180.93/180.82 cnf(5554,plain, % 180.93/180.82 (~P3(x55541,f4(x55542,x55543))+~E(f7(x55542,x55543),f10(x55544,f4(x55543,x55542)))), % 180.93/180.82 inference(scs_inference,[],[24,4204,30])). % 180.93/180.82 cnf(5556,plain, % 180.93/180.82 (~P3(x55561,f4(x55562,x55563))+~P2(x55562,x55562)), % 180.93/180.82 inference(scs_inference,[],[5394,38])). % 180.93/180.82 cnf(5557,plain, % 180.93/180.82 (~P3(x55571,f4(x55572,x55573))+P3(f7(x55572,x55572),f4(x55572,x55572))), % 180.93/180.82 inference(scs_inference,[],[5556,36])). % 180.93/180.82 cnf(5558,plain, % 180.93/180.82 (~P3(x55581,f4(a8,x55582))+~E(f4(a8,a8),f4(x55583,f10(a9,a9)))), % 180.93/180.82 inference(scs_inference,[],[5441,5557,34])). % 180.93/180.82 cnf(5560,plain, % 180.93/180.82 (~P2(f4(x55601,x55602),f4(x55602,x55601))+~P3(x55603,f4(f4(x55602,x55601),x55604))), % 180.93/180.82 inference(scs_inference,[],[24,5556,19])). % 180.93/180.82 cnf(5561,plain, % 180.93/180.82 (~P2(a8,a8)), % 180.93/180.82 inference(scs_inference,[],[49,5556,36])). % 180.93/180.82 cnf(5562,plain, % 180.93/180.82 (P3(f7(a8,a8),f4(a8,a8))), % 180.93/180.82 inference(scs_inference,[],[5561,36])). % 180.93/180.82 cnf(5566,plain, % 180.93/180.82 (~P3(f4(a8,a8),f7(a8,a8))), % 180.93/180.82 inference(scs_inference,[],[5561,36,5372,4201])). % 180.93/180.82 cnf(5579,plain, % 180.93/180.82 (~E(f4(a8,a8),f4(f10(a9,a9),x55791))), % 180.93/180.82 inference(scs_inference,[],[5562,5535])). % 180.93/180.82 cnf(5580,plain, % 180.93/180.82 (~E(f4(a8,a8),f4(x55801,f10(a9,a9)))), % 180.93/180.82 inference(scs_inference,[],[5562,5558])). % 180.93/180.82 cnf(5596,plain, % 180.93/180.82 (P3(f7(a8,a8),f4(f4(a8,a8),f4(a8,a8)))), % 180.93/180.82 inference(scs_inference,[],[5562,5394,48])). % 180.93/180.82 cnf(5624,plain, % 180.93/180.82 (~P3(f4(f7(a8,a8),f7(a8,a8)),f10(a9,a9))), % 180.93/180.82 inference(scs_inference,[],[5562,22,5430,17])). % 180.93/180.82 cnf(5863,plain, % 180.93/180.82 (~E(f4(a8,a8),f4(x58631,f10(a9,a9)))), % 180.93/180.82 inference(rename_variables,[],[5580])). % 180.93/180.82 cnf(5866,plain, % 180.93/180.82 (~E(f4(a8,a8),f4(x58661,f10(a9,a9)))), % 180.93/180.82 inference(rename_variables,[],[5580])). % 180.93/180.82 cnf(5886,plain, % 180.93/180.82 (~E(f4(f4(x58861,a8),x58862),f4(f10(x58863,a6),f10(x58863,a6)))), % 180.93/180.82 inference(rename_variables,[],[4481])). % 180.93/180.82 cnf(5892,plain, % 180.93/180.82 (E(f10(f4(x58921,f4(x58922,x58922)),x58923),f10(f4(x58921,x58922),x58923))), % 180.93/180.82 inference(rename_variables,[],[4660])). % 180.93/180.82 cnf(5901,plain, % 180.93/180.82 (~E(f4(a8,a8),f4(x59011,f10(a9,a9)))), % 180.93/180.82 inference(rename_variables,[],[5580])). % 180.93/180.82 cnf(5909,plain, % 180.93/180.82 (~E(f4(f10(x59091,a6),f10(x59091,a6)),f4(x59092,a8))), % 180.93/180.82 inference(rename_variables,[],[4082])). % 180.93/180.82 cnf(5912,plain, % 180.93/180.82 (~E(f4(f10(x59121,a6),f10(x59121,a6)),f4(x59122,a8))), % 180.93/180.82 inference(rename_variables,[],[4082])). % 180.93/180.82 cnf(5943,plain, % 180.93/180.82 (E(f10(x59431,f4(x59432,x59432)),f10(x59431,x59432))), % 180.93/180.82 inference(rename_variables,[],[4057])). % 180.93/180.82 cnf(5944,plain, % 180.93/180.82 (~P3(f10(f4(x59441,x59442),x59443),f4(x59442,x59441))), % 180.93/180.82 inference(rename_variables,[],[4192])). % 180.93/180.82 cnf(5947,plain, % 180.93/180.82 (E(f10(x59471,f4(x59472,x59472)),f10(x59471,x59472))), % 180.93/180.82 inference(rename_variables,[],[4057])). % 180.93/180.82 cnf(5953,plain, % 180.93/180.82 (E(f10(x59531,f4(x59532,x59532)),f10(x59531,x59532))), % 180.93/180.82 inference(rename_variables,[],[4057])). % 180.93/180.82 cnf(5958,plain, % 180.93/180.82 (E(f7(f10(x59581,x59581),f10(x59581,x59581)),x59581)), % 180.93/180.82 inference(rename_variables,[],[4994])). % 180.93/180.82 cnf(6070,plain, % 180.93/180.82 (E(f10(x60701,f4(f4(x60702,x60702),x60703)),f10(x60701,f4(x60702,x60703)))), % 180.93/180.82 inference(rename_variables,[],[4741])). % 180.93/180.82 cnf(6106,plain, % 180.93/180.82 (~P2(a8,f10(f7(a8,a8),x61061))), % 180.93/180.82 inference(scs_inference,[],[2483,5566,4057,5943,5947,5953,4064,4058,4174,2814,4192,5944,4150,4210,4212,4216,4340,4360,4620,4082,5909,5912,4130,4994,5958,4556,4091,5579,5580,5863,5866,5901,5596,4971,5470,4995,4175,4177,4179,4616,4951,4957,4987,4997,5010,4481,5886,4660,5892,4741,6070,4973,4975,4075,4591,4601,5384,4956,4963,3224,3236,2812,72,2454,14,15,8,9,10,11,12,13,4203,4206,4208,4495,5462,5464,5557,5375,5410,5420,5422,5425,5540,5550,5560,5383,5402,5406,5412,5536,5545,5444,5446,5492,5519,4560,4614,4636,5414,5426,5551,5490,5515,5521,4564,5466,4545,4551,4658,4912,4557,4640,4662,5517,4621,4623,5,4199,5371,5372,5552,4201,36,32,7,47,6,4,46,2,45,35,30,31,20,19,34,18,48,16,17,3,37,33,4200,4207,5394,5400,5511,5513,4202,4205,5385,5387,5396,5397,5404,5424,5512,5537,5543,5546,5554,5386,5388,5389,5390,5391,5427,5428,5544,5548,5553,5471,5487,5408,5416,5418,5538,5542,5547,5496,4562,4589,4646,5429,5438,4624,4632,4656,4910,4654,5392,5398,5556,5473,4204,5395,5447,5468,5539,5549,5393,5000,79,5374,5376])). % 180.93/180.82 cnf(6383,plain, % 180.93/180.82 (E(x63831,f7(f10(x63831,x63831),f10(x63831,x63831)))), % 180.93/180.82 inference(scs_inference,[],[4994,2])). % 180.93/180.82 cnf(6811,plain, % 180.93/180.82 (E(f4(f4(x68111,x68111),x68111),x68111)), % 180.93/180.82 inference(scs_inference,[],[4556,2])). % 180.93/180.82 cnf(8795,plain, % 180.93/180.82 (E(f4(x87951,x87951),x87951)), % 180.93/180.82 inference(rename_variables,[],[22])). % 180.93/180.82 cnf(8801,plain, % 180.93/180.82 (E(f4(x88011,x88011),x88011)), % 180.93/180.82 inference(rename_variables,[],[22])). % 180.93/180.82 cnf(8820,plain, % 180.93/180.82 ($false), % 180.93/180.82 inference(scs_inference,[],[26,28,22,8795,8801,283,4230,4346,4362,5017,5435,5624,3638,6383,5382,4985,6106,4058,5474,6811,4224,2711,4344,4340,33,37,20,19,48,34,30,31,35,32,18,3,46,2,47,45]), % 180.93/180.82 ['proof']). % 180.93/180.82 % SZS output end Proof % 180.93/180.82 % Total time :180.130000s %------------------------------------------------------------------------------