%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM458+1 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n024.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 12:24:21 EDT 2024 % Result : Theorem 117.30s 117.39s % Output : CNFRefutation 117.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : NUM458+1 : TPTP v8.2.0. Released v4.0.0. % 0.12/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n024.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 : Sat Jun 22 20:05:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.56 start to proof:theBenchmark % 117.30/117.37 %------------------------------------------- % 117.30/117.37 % File :CSE---1.7 % 117.30/117.37 % Problem :theBenchmark % 117.30/117.37 % Transform :cnf % 117.30/117.37 % Format :tptp:raw % 117.30/117.37 % Command :java -jar mcs_scs.jar %d %s % 117.30/117.37 % 117.30/117.37 % Result :Theorem 116.760000s % 117.30/117.37 % Output :CNFRefutation 116.760000s % 117.30/117.37 %------------------------------------------- % 117.30/117.38 %------------------------------------------------------------------------------ % 117.30/117.38 % File : NUM458+1 : TPTP v8.2.0. Released v4.0.0. % 117.30/117.38 % Domain : Number Theory % 117.30/117.38 % Problem : Square root of a prime is irrational 02, 00 expansion % 117.30/117.38 % Version : Especial. % 117.30/117.38 % English : % 117.30/117.38 % 117.30/117.38 % Refs : [LPV06] Lyaletski et al. (2006), SAD as a Mathematical Assista % 117.30/117.38 % : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 117.30/117.38 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 117.30/117.38 % Source : [Pas08] % 117.30/117.38 % Names : primes_02.00 [Pas08] % 117.30/117.38 % 117.30/117.38 % Status : Theorem % 117.30/117.38 % Rating : 0.11 v8.2.0, 0.14 v8.1.0, 0.06 v7.4.0, 0.10 v7.3.0, 0.07 v7.1.0, 0.04 v7.0.0, 0.07 v6.4.0, 0.12 v6.1.0, 0.13 v6.0.0, 0.09 v5.5.0, 0.19 v5.4.0, 0.25 v5.3.0, 0.26 v5.2.0, 0.15 v5.1.0, 0.33 v5.0.0, 0.29 v4.1.0, 0.39 v4.0.1, 0.70 v4.0.0 % 117.30/117.38 % Syntax : Number of formulae : 21 ( 3 unt; 2 def) % 117.30/117.38 % Number of atoms : 75 ( 29 equ) % 117.30/117.38 % Maximal formula atoms : 7 ( 3 avg) % 117.30/117.38 % Number of connectives : 56 ( 2 ~; 3 |; 25 &) % 117.30/117.38 % ( 2 <=>; 24 =>; 0 <=; 0 <~>) % 117.30/117.38 % Maximal formula depth : 9 ( 5 avg) % 117.30/117.38 % Maximal term depth : 3 ( 1 avg) % 117.30/117.38 % Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty) % 117.30/117.38 % Number of functors : 6 ( 6 usr; 3 con; 0-2 aty) % 117.30/117.38 % Number of variables : 37 ( 36 !; 1 ?) % 117.30/117.38 % SPC : FOF_THM_RFO_SEQ % 117.30/117.38 % 117.30/117.38 % Comments : Problem generated by the SAD system [VLP07] % 117.30/117.38 %------------------------------------------------------------------------------ % 117.30/117.38 fof(mNatSort,axiom, % 117.30/117.38 ! [W0] : % 117.30/117.38 ( aNaturalNumber0(W0) % 117.30/117.38 => $true ) ). % 117.30/117.38 % 117.30/117.38 fof(mSortsC,axiom, % 117.30/117.38 aNaturalNumber0(sz00) ). % 117.30/117.38 % 117.30/117.38 fof(mSortsC_01,axiom, % 117.30/117.38 ( aNaturalNumber0(sz10) % 117.30/117.38 & sz10 != sz00 ) ). % 117.30/117.38 % 117.30/117.38 fof(mSortsB,axiom, % 117.30/117.38 ! [W0,W1] : % 117.30/117.38 ( ( aNaturalNumber0(W0) % 117.30/117.38 & aNaturalNumber0(W1) ) % 117.30/117.38 => aNaturalNumber0(sdtpldt0(W0,W1)) ) ). % 117.30/117.38 % 117.30/117.38 fof(mSortsB_02,axiom, % 117.30/117.38 ! [W0,W1] : % 117.30/117.38 ( ( aNaturalNumber0(W0) % 117.30/117.38 & aNaturalNumber0(W1) ) % 117.30/117.38 => aNaturalNumber0(sdtasdt0(W0,W1)) ) ). % 117.30/117.38 % 117.30/117.38 fof(mAddComm,axiom, % 117.30/117.38 ! [W0,W1] : % 117.30/117.38 ( ( aNaturalNumber0(W0) % 117.30/117.38 & aNaturalNumber0(W1) ) % 117.30/117.38 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 117.30/117.38 % 117.30/117.38 fof(mAddAsso,axiom, % 117.30/117.38 ! [W0,W1,W2] : % 117.30/117.38 ( ( aNaturalNumber0(W0) % 117.30/117.39 & aNaturalNumber0(W1) % 117.30/117.39 & aNaturalNumber0(W2) ) % 117.30/117.39 => sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) ). % 117.30/117.39 % 117.30/117.39 fof(m_AddZero,axiom, % 117.30/117.39 ! [W0] : % 117.30/117.39 ( aNaturalNumber0(W0) % 117.30/117.39 => ( sdtpldt0(W0,sz00) = W0 % 117.30/117.39 & W0 = sdtpldt0(sz00,W0) ) ) ). % 117.30/117.39 % 117.30/117.39 fof(mMulComm,axiom, % 117.30/117.39 ! [W0,W1] : % 117.30/117.39 ( ( aNaturalNumber0(W0) % 117.30/117.39 & aNaturalNumber0(W1) ) % 117.30/117.39 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 117.30/117.39 % 117.30/117.39 fof(mMulAsso,axiom, % 117.30/117.39 ! [W0,W1,W2] : % 117.30/117.39 ( ( aNaturalNumber0(W0) % 117.30/117.39 & aNaturalNumber0(W1) % 117.30/117.39 & aNaturalNumber0(W2) ) % 117.30/117.39 => sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) ). % 117.30/117.39 % 117.30/117.39 fof(m_MulUnit,axiom, % 117.30/117.39 ! [W0] : % 117.30/117.39 ( aNaturalNumber0(W0) % 117.30/117.39 => ( sdtasdt0(W0,sz10) = W0 % 117.30/117.39 & W0 = sdtasdt0(sz10,W0) ) ) ). % 117.30/117.39 % 117.30/117.39 fof(m_MulZero,axiom, % 117.30/117.39 ! [W0] : % 117.30/117.39 ( aNaturalNumber0(W0) % 117.30/117.39 => ( sdtasdt0(W0,sz00) = sz00 % 117.30/117.39 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 117.30/117.39 % 117.30/117.39 fof(mAMDistr,axiom, % 117.30/117.39 ! [W0,W1,W2] : % 117.30/117.39 ( ( aNaturalNumber0(W0) % 117.30/117.39 & aNaturalNumber0(W1) % 117.30/117.39 & aNaturalNumber0(W2) ) % 117.30/117.39 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 117.30/117.39 & sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ). % 117.30/117.39 % 117.30/117.39 fof(mAddCanc,axiom, % 117.30/117.39 ! [W0,W1,W2] : % 117.30/117.39 ( ( aNaturalNumber0(W0) % 117.30/117.39 & aNaturalNumber0(W1) % 117.30/117.39 & aNaturalNumber0(W2) ) % 117.30/117.39 => ( ( sdtpldt0(W0,W1) = sdtpldt0(W0,W2) % 117.30/117.39 | sdtpldt0(W1,W0) = sdtpldt0(W2,W0) ) % 117.30/117.39 => W1 = W2 ) ) ). % 117.30/117.39 % 117.30/117.39 fof(mMulCanc,axiom, % 117.30/117.39 ! [W0] : % 117.30/117.39 ( aNaturalNumber0(W0) % 117.30/117.39 => ( W0 != sz00 % 117.30/117.39 => ! [W1,W2] : % 117.30/117.39 ( ( aNaturalNumber0(W1) % 117.30/117.39 & aNaturalNumber0(W2) ) % 117.30/117.39 => ( ( sdtasdt0(W0,W1) = sdtasdt0(W0,W2) % 117.30/117.39 | sdtasdt0(W1,W0) = sdtasdt0(W2,W0) ) % 117.30/117.39 => W1 = W2 ) ) ) ) ). % 117.30/117.39 % 117.30/117.39 fof(mZeroAdd,axiom, % 117.30/117.39 ! [W0,W1] : % 117.30/117.39 ( ( aNaturalNumber0(W0) % 117.30/117.39 & aNaturalNumber0(W1) ) % 117.30/117.39 => ( sdtpldt0(W0,W1) = sz00 % 117.30/117.39 => ( W0 = sz00 % 117.30/117.39 & W1 = sz00 ) ) ) ). % 117.30/117.39 % 117.30/117.39 fof(mZeroMul,axiom, % 117.30/117.39 ! [W0,W1] : % 117.30/117.39 ( ( aNaturalNumber0(W0) % 117.30/117.39 & aNaturalNumber0(W1) ) % 117.30/117.39 => ( sdtasdt0(W0,W1) = sz00 % 117.30/117.39 => ( W0 = sz00 % 117.30/117.39 | W1 = sz00 ) ) ) ). % 117.30/117.39 % 117.30/117.39 fof(mDefLE,definition, % 117.30/117.39 ! [W0,W1] : % 117.30/117.39 ( ( aNaturalNumber0(W0) % 117.30/117.39 & aNaturalNumber0(W1) ) % 117.30/117.39 => ( sdtlseqdt0(W0,W1) % 117.30/117.39 <=> ? [W2] : % 117.30/117.39 ( aNaturalNumber0(W2) % 117.30/117.39 & sdtpldt0(W0,W2) = W1 ) ) ) ). % 117.30/117.39 % 117.30/117.39 fof(mDefDiff,definition, % 117.30/117.39 ! [W0,W1] : % 117.30/117.39 ( ( aNaturalNumber0(W0) % 117.30/117.39 & aNaturalNumber0(W1) ) % 117.30/117.39 => ( sdtlseqdt0(W0,W1) % 117.30/117.39 => ! [W2] : % 117.30/117.39 ( W2 = sdtmndt0(W1,W0) % 117.30/117.39 <=> ( aNaturalNumber0(W2) % 117.30/117.39 & sdtpldt0(W0,W2) = W1 ) ) ) ) ). % 117.30/117.39 % 117.30/117.39 fof(m__718,hypothesis, % 117.30/117.39 aNaturalNumber0(xm) ). % 117.30/117.39 % 117.30/117.39 fof(m__,conjecture, % 117.30/117.39 sdtlseqdt0(xm,xm) ). % 117.30/117.39 % 117.30/117.39 %------------------------------------------------------------------------------ % 117.30/117.39 %------------------------------------------- % 117.30/117.39 % Proof found % 117.30/117.39 % SZS status Theorem for theBenchmark % 117.30/117.39 % SZS output start Proof % 117.30/117.39 %ClaNum:46(EqnAxiom:14) % 117.30/117.39 %VarNum:179(SingletonVarNum:60) % 117.30/117.39 %MaxLitNum:6 % 117.30/117.39 %MaxfuncDepth:2 % 117.30/117.39 %SharedTerms:8 % 117.30/117.39 %goalClause: 19 % 117.30/117.39 %singleGoalClaCount:1 % 117.30/117.39 [15]P1(a1) % 117.30/117.39 [16]P1(a6) % 117.30/117.39 [17]P1(a7) % 117.30/117.39 [18]~E(a1,a6) % 117.30/117.39 [19]~P2(a7,a7) % 117.30/117.39 [20]~P1(x201)+E(f2(a1,x201),a1) % 117.30/117.39 [21]~P1(x211)+E(f2(x211,a1),a1) % 117.30/117.39 [22]~P1(x221)+E(f4(a1,x221),x221) % 117.30/117.39 [23]~P1(x231)+E(f2(a6,x231),x231) % 117.30/117.39 [24]~P1(x241)+E(f4(x241,a1),x241) % 117.30/117.39 [25]~P1(x251)+E(f2(x251,a6),x251) % 117.30/117.39 [29]~P1(x292)+~P1(x291)+E(f4(x291,x292),f4(x292,x291)) % 117.30/117.39 [30]~P1(x302)+~P1(x301)+E(f2(x301,x302),f2(x302,x301)) % 117.30/117.39 [31]~P1(x312)+~P1(x311)+P1(f4(x311,x312)) % 117.30/117.39 [32]~P1(x322)+~P1(x321)+P1(f2(x321,x322)) % 117.30/117.39 [26]~P1(x262)+~P1(x261)+E(x261,a1)+~E(f4(x262,x261),a1) % 117.30/117.39 [27]~P1(x272)+~P1(x271)+E(x271,a1)+~E(f4(x271,x272),a1) % 117.30/117.39 [35]~P1(x352)+~P1(x351)+~P2(x351,x352)+P1(f3(x351,x352)) % 117.30/117.39 [41]~P1(x412)+~P1(x411)+~P2(x411,x412)+E(f4(x411,f3(x411,x412)),x412) % 117.30/117.39 [43]~P1(x433)+~P1(x432)+~P1(x431)+E(f4(f4(x431,x432),x433),f4(x431,f4(x432,x433))) % 117.30/117.39 [44]~P1(x443)+~P1(x442)+~P1(x441)+E(f2(f2(x441,x442),x443),f2(x441,f2(x442,x443))) % 117.30/117.39 [45]~P1(x453)+~P1(x452)+~P1(x451)+E(f4(f2(x451,x452),f2(x451,x453)),f2(x451,f4(x452,x453))) % 117.30/117.39 [46]~P1(x462)+~P1(x463)+~P1(x461)+E(f4(f2(x461,x462),f2(x463,x462)),f2(f4(x461,x463),x462)) % 117.30/117.39 [28]~P1(x281)+~P1(x282)+E(x281,a1)+E(x282,a1)+~E(f2(x282,x281),a1) % 117.30/117.39 [33]~P1(x332)+~P1(x331)+~P1(x333)+P2(x331,x332)+~E(f4(x331,x333),x332) % 117.30/117.39 [34]~P1(x343)+~P1(x342)+~P2(x343,x342)+P1(x341)+~E(x341,f5(x342,x343)) % 117.30/117.39 [36]~P1(x362)+~P1(x361)+~P1(x363)+E(x361,x362)+~E(f4(x363,x361),f4(x363,x362)) % 117.30/117.39 [37]~P1(x372)+~P1(x373)+~P1(x371)+E(x371,x372)+~E(f4(x371,x373),f4(x372,x373)) % 117.30/117.39 [40]~P1(x403)+~P1(x401)+~P2(x401,x403)+~E(x402,f5(x403,x401))+E(f4(x401,x402),x403) % 117.30/117.39 [38]~P1(x382)+~P1(x381)+~P1(x383)+E(x381,x382)+~E(f2(x383,x381),f2(x383,x382))+E(x383,a1) % 117.30/117.39 [39]~P1(x392)+~P1(x393)+~P1(x391)+E(x391,x392)+~E(f2(x391,x393),f2(x392,x393))+E(x393,a1) % 117.30/117.39 [42]~P1(x422)+~P1(x423)+~P1(x421)+~P2(x423,x422)+~E(f4(x423,x421),x422)+E(x421,f5(x422,x423)) % 117.30/117.39 %EqnAxiom % 117.30/117.39 [1]E(x11,x11) % 117.30/117.39 [2]E(x22,x21)+~E(x21,x22) % 117.30/117.39 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 117.30/117.39 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 117.30/117.39 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 117.30/117.39 [6]~E(x61,x62)+E(f4(x61,x63),f4(x62,x63)) % 117.30/117.39 [7]~E(x71,x72)+E(f4(x73,x71),f4(x73,x72)) % 117.30/117.39 [8]~E(x81,x82)+E(f3(x81,x83),f3(x82,x83)) % 117.30/117.39 [9]~E(x91,x92)+E(f3(x93,x91),f3(x93,x92)) % 117.30/117.39 [10]~E(x101,x102)+E(f5(x101,x103),f5(x102,x103)) % 117.30/117.39 [11]~E(x111,x112)+E(f5(x113,x111),f5(x113,x112)) % 117.30/117.39 [12]~P1(x121)+P1(x122)+~E(x121,x122) % 117.30/117.39 [13]P2(x132,x133)+~E(x131,x132)+~P2(x131,x133) % 117.30/117.39 [14]P2(x143,x142)+~E(x141,x142)+~P2(x143,x141) % 117.30/117.39 % 117.30/117.39 %------------------------------------------- % 117.40/117.40 cnf(47,plain, % 117.40/117.40 (P2(x471,f4(x471,x472))+~P1(f4(x471,x472))+~P1(x471)+~P1(x472)), % 117.40/117.40 inference(equality_inference,[],[33])). % 117.40/117.40 cnf(48,plain, % 117.40/117.40 (~P2(x481,x482)+~P1(x481)+~P1(x482)+P1(f5(x482,x481))), % 117.40/117.40 inference(equality_inference,[],[34])). % 117.40/117.40 cnf(53,plain, % 117.40/117.40 (~P2(x531,x532)+~P1(x532)+~P1(x531)+E(f4(x531,f5(x532,x531)),x532)), % 117.40/117.40 inference(equality_inference,[],[40])). % 117.40/117.40 cnf(54,plain, % 117.40/117.40 (~P2(x541,f4(x541,x542))+~P1(f4(x541,x542))+~P1(x541)+~P1(x542)+E(x542,f5(f4(x541,x542),x541))), % 117.40/117.40 inference(equality_inference,[],[42])). % 117.40/117.40 cnf(55,plain, % 117.40/117.40 (P2(a1,f4(a1,a1))+~P1(f4(a1,a1))), % 117.40/117.40 inference(scs_inference,[],[15,47])). % 117.40/117.41 cnf(58,plain, % 117.40/117.41 (P2(a6,f4(a6,a6))+~P1(f4(a6,a6))), % 117.40/117.41 inference(scs_inference,[],[16,47])). % 117.40/117.41 cnf(60,plain, % 117.40/117.41 (E(a6,f5(f4(a6,a6),a6))+~P1(f4(a6,a6))+~P2(a1,a1)), % 117.40/117.41 inference(scs_inference,[],[15,16,47,53,48,33,54])). % 117.40/117.41 cnf(61,plain, % 117.40/117.41 (P2(a7,f4(a7,a7))+~P1(f4(a7,a7))), % 117.40/117.41 inference(scs_inference,[],[17,47])). % 117.40/117.41 cnf(63,plain, % 117.40/117.41 (~P1(f4(a7,a7))+~E(f4(a7,a7),a7)), % 117.40/117.41 inference(scs_inference,[],[19,17,47,13,14])). % 117.40/117.41 cnf(66,plain, % 117.40/117.41 (E(f4(a1,f5(a1,a1)),a1)+~P2(a1,a1)), % 117.40/117.41 inference(scs_inference,[],[15,53])). % 117.40/117.41 cnf(68,plain, % 117.40/117.41 (E(a1,f4(a1,f5(a1,a1)))+~P2(a1,a1)), % 117.40/117.41 inference(scs_inference,[],[15,53,2])). % 117.40/117.41 cnf(71,plain, % 117.40/117.41 (E(f4(a6,f5(a6,a6)),a6)+~P2(a6,a6)), % 117.40/117.41 inference(scs_inference,[],[16,53])). % 117.40/117.41 cnf(77,plain, % 117.40/117.41 (P1(f5(a1,a1))+~P2(a1,a1)), % 117.40/117.41 inference(scs_inference,[],[15,48])). % 117.40/117.41 cnf(80,plain, % 117.40/117.41 (P1(f5(a6,a6))+~P2(a6,a6)), % 117.40/117.41 inference(scs_inference,[],[16,48])). % 117.40/117.41 cnf(92,plain, % 117.40/117.41 (E(f2(a1,f4(a1,a1)),a1)), % 117.40/117.41 inference(scs_inference,[],[15,20,31])). % 117.40/117.41 cnf(93,plain, % 117.40/117.41 (E(a1,f2(a1,f4(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[92,2])). % 117.40/117.41 cnf(94,plain, % 117.40/117.41 (P1(f2(a1,f4(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[15,92,2,12])). % 117.40/117.41 cnf(111,plain, % 117.40/117.41 (E(f2(f2(a1,f4(a1,a1)),a1),a1)), % 117.40/117.41 inference(scs_inference,[],[93,15,21,12])). % 117.40/117.41 cnf(112,plain, % 117.40/117.41 (E(a1,f2(f2(a1,f4(a1,a1)),a1))), % 117.40/117.41 inference(scs_inference,[],[111,2])). % 117.40/117.41 cnf(130,plain, % 117.40/117.41 (E(f4(a1,f2(a1,a1)),f2(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[15,22,32])). % 117.40/117.41 cnf(131,plain, % 117.40/117.41 (E(f2(a1,a1),f4(a1,f2(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[130,2])). % 117.40/117.41 cnf(132,plain, % 117.40/117.41 (~P1(f4(a1,f2(a1,a1)))+P1(f2(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[130,2,12])). % 117.40/117.41 cnf(133,plain, % 117.40/117.41 (P2(a1,f2(a1,a1))+~P1(f4(a1,f2(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[15,130,2,12,33])). % 117.40/117.41 cnf(135,plain, % 117.40/117.41 (~P1(f4(a1,f2(a1,a1)))+E(f2(a1,a1),f5(f2(a1,a1),a1))), % 117.40/117.41 inference(scs_inference,[],[15,130,2,12,33,42])). % 117.40/117.41 cnf(137,plain, % 117.40/117.41 (E(f4(a1,f2(a1,a1)),f5(f2(a1,a1),a1))+~P1(f4(a1,f2(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[15,130,2,12,33,42,3])). % 117.40/117.41 cnf(138,plain, % 117.40/117.41 (P2(f2(f2(a1,f4(a1,a1)),a1),f2(a1,a1))+~P1(f4(a1,f2(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[15,130,112,2,12,33,42,3,13])). % 117.40/117.41 cnf(139,plain, % 117.40/117.41 (P2(a1,f4(a1,f2(a1,a1)))+~P1(f4(a1,f2(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[15,130,112,2,12,33,42,3,13,14])). % 117.40/117.41 cnf(144,plain, % 117.40/117.41 (~P1(f2(a1,a1))+P1(f4(a1,f2(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[131,12])). % 117.40/117.41 cnf(146,plain, % 117.40/117.41 (~P1(f2(a1,a1))+P1(f2(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[131,12,138,132])). % 117.40/117.41 cnf(147,plain, % 117.40/117.41 (~P1(f2(a1,a1))+E(f2(a1,a1),f5(f2(a1,a1),a1))), % 117.40/117.41 inference(scs_inference,[],[131,12,138,132,135])). % 117.40/117.41 cnf(149,plain, % 117.40/117.41 (E(f5(f2(a1,a1),a1),f2(a1,a1))+~P1(f2(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[131,12,138,132,135,137,2])). % 117.40/117.41 cnf(152,plain, % 117.40/117.41 (P2(a1,f2(a1,a1))+~P1(f2(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[15,130,33])). % 117.40/117.41 cnf(154,plain, % 117.40/117.41 (P2(f2(a1,f4(a1,a1)),f2(a1,a1))+~P1(f2(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[15,130,93,33,13])). % 117.40/117.41 cnf(169,plain, % 117.40/117.41 (E(f2(a6,f4(a1,a1)),f4(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[15,23,31])). % 117.40/117.41 cnf(170,plain, % 117.40/117.41 (E(f4(a1,a1),f2(a6,f4(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[169,2])). % 117.40/117.41 cnf(171,plain, % 117.40/117.41 (~P1(f2(a6,f4(a1,a1)))+P1(f4(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[169,2,12])). % 117.40/117.41 cnf(172,plain, % 117.40/117.41 (P2(a1,f4(a1,a1))+~P1(f2(a6,f4(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[15,169,2,12,47])). % 117.40/117.41 cnf(174,plain, % 117.40/117.41 (E(a1,f5(f4(a1,a1),a1))+~P1(f2(a6,f4(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[15,169,2,12,47,54])). % 117.40/117.41 cnf(177,plain, % 117.40/117.41 (P2(f2(a1,f4(a1,a1)),f4(a1,a1))+~P1(f2(a6,f4(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[15,92,93,169,2,12,47,54,3,13])). % 117.40/117.41 cnf(181,plain, % 117.40/117.41 (~P1(f4(a1,a1))+P1(f2(a6,f4(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[170,12])). % 117.40/117.41 cnf(182,plain, % 117.40/117.41 (P2(a1,f2(a6,f4(a1,a1)))+~P1(f4(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[15,170,12,33])). % 117.40/117.41 cnf(186,plain, % 117.40/117.41 (~P1(f4(a1,a1))+P2(f2(a1,f4(a1,a1)),f4(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[15,170,12,33,42,177])). % 117.40/117.41 cnf(187,plain, % 117.40/117.41 (P1(f4(a1,a1))+~P1(f4(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[15,170,12,33,42,177,171])). % 117.40/117.41 cnf(206,plain, % 117.40/117.41 (E(f4(f2(a1,a1),a1),f2(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[15,24,32])). % 117.40/117.41 cnf(207,plain, % 117.40/117.41 (E(f2(a1,a1),f4(f2(a1,a1),a1))), % 117.40/117.41 inference(scs_inference,[],[206,2])). % 117.40/117.41 cnf(208,plain, % 117.40/117.41 (E(f4(a1,f2(a1,a1)),f4(f2(a1,a1),a1))), % 117.40/117.41 inference(scs_inference,[],[130,206,2,3])). % 117.40/117.41 cnf(209,plain, % 117.40/117.41 (~P1(f4(f2(a1,a1),a1))+P1(f2(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[130,206,2,3,12])). % 117.40/117.41 cnf(210,plain, % 117.40/117.41 (P2(a1,f2(a1,a1))+~P1(f4(f2(a1,a1),a1))), % 117.40/117.41 inference(scs_inference,[],[15,130,206,2,3,12,33])). % 117.40/117.41 cnf(212,plain, % 117.40/117.41 (~P1(f4(f2(a1,a1),a1))+E(f2(a1,a1),f5(f2(a1,a1),a1))), % 117.40/117.41 inference(scs_inference,[],[15,130,206,2,3,12,33,42])). % 117.40/117.41 cnf(214,plain, % 117.40/117.41 (~P1(f4(f2(a1,a1),a1))+E(f5(f2(a1,a1),a1),f2(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[15,130,206,2,3,12,33,42,149])). % 117.40/117.41 cnf(215,plain, % 117.40/117.41 (P2(f2(a1,f4(a1,a1)),f2(a1,a1))+~P1(f4(f2(a1,a1),a1))), % 117.40/117.41 inference(scs_inference,[],[15,130,206,93,2,3,12,33,42,149,13])). % 117.40/117.41 cnf(216,plain, % 117.40/117.41 (P2(a1,f4(a1,f2(a1,a1)))+~P1(f4(f2(a1,a1),a1))), % 117.40/117.41 inference(scs_inference,[],[15,130,206,131,93,2,3,12,33,42,149,13,14])). % 117.40/117.41 cnf(219,plain, % 117.40/117.41 (E(f4(f2(a1,a1),a1),f4(a1,f2(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[208,2])). % 117.40/117.41 cnf(220,plain, % 117.40/117.41 (~P1(f2(a1,a1))+P1(f4(f2(a1,a1),a1))), % 117.40/117.41 inference(scs_inference,[],[207,208,2,12])). % 117.40/117.41 cnf(222,plain, % 117.40/117.41 (P2(f2(a1,a1),f2(a1,a1))+~P1(f2(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[15,206,207,208,2,12,47,48,53,33])). % 117.40/117.41 cnf(225,plain, % 117.40/117.41 (~P1(f4(a1,f2(a1,a1)))+P1(f4(f2(a1,a1),a1))), % 117.40/117.41 inference(scs_inference,[],[208,12])). % 117.40/117.41 cnf(226,plain, % 117.40/117.41 (~P1(f4(a1,f2(a1,a1)))+P2(f2(a1,f4(a1,a1)),f2(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[208,12,215])). % 117.40/117.41 cnf(228,plain, % 117.40/117.41 (P2(f2(a1,f4(a1,a1)),f4(a1,f2(a1,a1)))+~P1(f4(a1,f2(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[131,208,12,215,214,3,14])). % 117.40/117.41 cnf(233,plain, % 117.40/117.41 (~P1(f4(f2(a1,a1),a1))+P1(f4(f2(a1,a1),a1))), % 117.40/117.41 inference(scs_inference,[],[219,12,228,225])). % 117.40/117.41 cnf(250,plain, % 117.40/117.41 (E(f2(f4(a1,a1),a6),f4(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[15,25,31])). % 117.40/117.41 cnf(251,plain, % 117.40/117.41 (E(f4(a1,a1),f2(f4(a1,a1),a6))), % 117.40/117.41 inference(scs_inference,[],[250,2])). % 117.40/117.41 cnf(252,plain, % 117.40/117.41 (E(f2(a6,f4(a1,a1)),f2(f4(a1,a1),a6))), % 117.40/117.41 inference(scs_inference,[],[169,250,2,3])). % 117.40/117.41 cnf(253,plain, % 117.40/117.41 (~P1(f2(f4(a1,a1),a6))+P1(f4(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[169,250,2,3,12])). % 117.40/117.41 cnf(254,plain, % 117.40/117.41 (P2(a1,f4(a1,a1))+~P1(f2(f4(a1,a1),a6))), % 117.40/117.41 inference(scs_inference,[],[15,169,250,2,3,12,47])). % 117.40/117.41 cnf(256,plain, % 117.40/117.41 (E(a1,f5(f4(a1,a1),a1))+~P1(f2(f4(a1,a1),a6))), % 117.40/117.41 inference(scs_inference,[],[15,169,250,2,3,12,47,54])). % 117.40/117.41 cnf(260,plain, % 117.40/117.41 (~P1(f2(f4(a1,a1),a6))+P1(f2(a6,f4(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[15,169,250,2,3,12,47,54,182,186,181])). % 117.40/117.41 cnf(266,plain, % 117.40/117.41 (E(f2(f4(a1,a1),a6),f2(a6,f4(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[252,2])). % 117.40/117.41 cnf(267,plain, % 117.40/117.41 (~P1(f4(a1,a1))+P1(f2(f4(a1,a1),a6))), % 117.40/117.41 inference(scs_inference,[],[251,252,2,12])). % 117.40/117.41 cnf(286,plain, % 117.40/117.41 (P2(a1,f2(f4(a1,a1),a6))+~P1(f2(f4(a1,a1),a6))), % 117.40/117.41 inference(scs_inference,[],[15,251,33])). % 117.40/117.41 cnf(316,plain, % 117.40/117.41 (P1(f5(a6,a6))+~E(f4(a6,a1),a6)), % 117.40/117.41 inference(scs_inference,[],[16,15,80,33])). % 117.40/117.41 cnf(362,plain, % 117.40/117.41 (~P1(f4(a1,a1))+P1(f3(a1,f4(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[15,55,35])). % 117.40/117.41 cnf(378,plain, % 117.40/117.41 (P2(x3781,f4(a6,a6))+~E(a6,x3781)+~P1(f4(a6,a6))), % 117.40/117.41 inference(scs_inference,[],[58,13])). % 117.40/117.41 cnf(395,plain, % 117.40/117.41 (P2(x3951,f4(a7,a7))+~E(a7,x3951)+~P1(f4(a7,a7))), % 117.40/117.41 inference(scs_inference,[],[61,13])). % 117.40/117.41 cnf(412,plain, % 117.40/117.41 (~E(f4(a7,a7),a7)), % 117.40/117.41 inference(scs_inference,[],[17,63,31])). % 117.40/117.41 cnf(444,plain, % 117.40/117.41 (~E(f4(a6,a1),a6)+P1(f2(f5(a6,a6),f5(a6,a6)))), % 117.40/117.41 inference(scs_inference,[],[316,32])). % 117.40/117.41 cnf(524,plain, % 117.40/117.41 (E(f5(x5241,f2(a1,a6)),f5(x5241,a1))), % 117.40/117.41 inference(scs_inference,[],[16,11,20])). % 117.40/117.41 cnf(525,plain, % 117.40/117.41 (E(f5(x5251,a1),f5(x5251,f2(a1,a6)))), % 117.40/117.41 inference(scs_inference,[],[524,2])). % 117.40/117.41 cnf(526,plain, % 117.40/117.41 (~P1(f5(x5261,f2(a1,a6)))+P1(f5(x5261,a1))), % 117.40/117.41 inference(scs_inference,[],[524,2,12])). % 117.40/117.41 cnf(529,plain, % 117.40/117.41 (~P1(f5(x5291,a1))+P1(f5(x5291,f2(a1,a6)))), % 117.40/117.41 inference(scs_inference,[],[525,12])). % 117.40/117.41 cnf(535,plain, % 117.40/117.41 (P2(a1,f4(f2(a1,a1),a1))+~P1(f4(f2(a1,a1),a1))+~P1(f2(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[16,15,208,524,33])). % 117.40/117.41 cnf(537,plain, % 117.40/117.41 (E(a6,f5(f4(a6,a6),a6))+~P2(a6,f4(a6,a6))+~P1(f4(a6,a6))), % 117.40/117.41 inference(scs_inference,[],[16,15,208,525,54])). % 117.40/117.41 cnf(574,plain, % 117.40/117.41 (E(a7,f5(f4(a7,a7),a7))+~P2(a7,f4(a7,a7))+~P1(f4(a7,a7))), % 117.40/117.41 inference(scs_inference,[],[17,15,524,208,54])). % 117.40/117.41 cnf(624,plain, % 117.40/117.41 (~P2(a1,a1)+E(f2(f4(a1,f5(a1,a1)),x6241),f2(a1,x6241))), % 117.40/117.41 inference(scs_inference,[],[66,4])). % 117.40/117.41 cnf(686,plain, % 117.40/117.41 (~P2(a6,a6)+E(f2(x6861,f4(a6,f5(a6,a6))),f2(x6861,a6))), % 117.40/117.41 inference(scs_inference,[],[71,5])). % 117.40/117.41 cnf(779,plain, % 117.40/117.41 (P1(f4(a1,f2(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[15,144,32])). % 117.40/117.41 cnf(780,plain, % 117.40/117.41 (P1(f2(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[779,132])). % 117.40/117.41 cnf(781,plain, % 117.40/117.41 (P2(a1,f2(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[779,133])). % 117.40/117.41 cnf(782,plain, % 117.40/117.41 (E(f2(a1,a1),f5(f2(a1,a1),a1))), % 117.40/117.41 inference(scs_inference,[],[779,135])). % 117.40/117.41 cnf(783,plain, % 117.40/117.41 (E(f4(a1,f2(a1,a1)),f5(f2(a1,a1),a1))), % 117.40/117.41 inference(scs_inference,[],[779,137])). % 117.40/117.41 cnf(785,plain, % 117.40/117.41 (P2(a1,f4(a1,f2(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[779,139])). % 117.40/117.41 cnf(786,plain, % 117.40/117.41 (P1(f4(f2(a1,a1),a1))), % 117.40/117.41 inference(scs_inference,[],[779,225])). % 117.40/117.41 cnf(787,plain, % 117.40/117.41 (P2(f2(a1,f4(a1,a1)),f2(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[779,226])). % 117.40/117.41 cnf(790,plain, % 117.40/117.41 (P2(f2(a1,a1),f4(a1,f2(a1,a1)))+~P1(f2(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[15,779,219,33])). % 117.40/117.41 cnf(792,plain, % 117.40/117.41 (P2(f4(a1,f2(a1,a1)),f4(a1,f2(a1,a1)))+~P1(f2(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[15,779,131,219,33,13])). % 117.40/117.41 cnf(796,plain, % 117.40/117.41 (P1(f2(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[780,146])). % 117.40/117.41 cnf(797,plain, % 117.40/117.41 (E(f2(a1,a1),f5(f2(a1,a1),a1))), % 117.40/117.41 inference(scs_inference,[],[780,147])). % 117.40/117.41 cnf(800,plain, % 117.40/117.41 (P2(a1,f2(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[780,152])). % 117.40/117.41 cnf(801,plain, % 117.40/117.41 (P2(f2(a1,f4(a1,a1)),f2(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[780,154])). % 117.40/117.41 cnf(802,plain, % 117.40/117.41 (P1(f2(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[786,209])). % 117.40/117.41 cnf(803,plain, % 117.40/117.41 (P2(a1,f2(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[786,210])). % 117.40/117.41 cnf(804,plain, % 117.40/117.41 (E(f2(a1,a1),f5(f2(a1,a1),a1))), % 117.40/117.41 inference(scs_inference,[],[786,212])). % 117.40/117.41 cnf(807,plain, % 117.40/117.41 (P2(a1,f4(a1,f2(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[786,216])). % 117.40/117.41 cnf(808,plain, % 117.40/117.41 (P1(f4(f2(a1,a1),a1))), % 117.40/117.41 inference(scs_inference,[],[780,220])). % 117.40/117.41 cnf(809,plain, % 117.40/117.41 (P2(f2(a1,a1),f2(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[780,222])). % 117.40/117.41 cnf(812,plain, % 117.40/117.41 (P1(f4(f2(a1,a1),a1))), % 117.40/117.41 inference(scs_inference,[],[786,233])). % 117.40/117.41 cnf(817,plain, % 117.40/117.41 (P2(a1,f4(f2(a1,a1),a1))), % 117.40/117.41 inference(scs_inference,[],[786,780,535])). % 117.40/117.41 cnf(819,plain, % 117.40/117.41 (P2(f2(a1,a1),f4(a1,f2(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[780,790])). % 117.40/117.41 cnf(820,plain, % 117.40/117.41 (E(f2(a1,a1),f5(f2(a1,a1),f2(a1,a6)))), % 117.40/117.41 inference(scs_inference,[],[782,780,525,790,3])). % 117.40/117.41 cnf(823,plain, % 117.40/117.41 (P1(f5(f2(a1,a1),a1))), % 117.40/117.41 inference(scs_inference,[],[782,780,525,790,3,13,12])). % 117.40/117.41 cnf(824,plain, % 117.40/117.41 (P2(a1,f5(f2(a1,a1),a1))), % 117.40/117.41 inference(scs_inference,[],[781,782,780,525,790,3,13,12,14])). % 117.40/117.41 cnf(825,plain, % 117.40/117.41 (P1(f5(f2(a1,a1),f2(a1,a6)))), % 117.40/117.41 inference(scs_inference,[],[15,781,782,780,524,525,790,3,13,12,14,34])). % 117.40/117.41 cnf(828,plain, % 117.40/117.41 (E(a1,f5(f4(a1,f2(a1,a1)),f2(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[15,781,782,780,779,524,525,219,790,3,13,12,14,34,42])). % 117.40/117.41 cnf(835,plain, % 117.40/117.41 (P2(f2(a1,a1),f4(f2(a1,a1),f2(a1,a1)))+~P1(f4(f2(a1,a1),f2(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[15,781,782,780,779,524,525,219,790,3,13,12,14,34,42,2,53,48,47])). % 117.40/117.41 cnf(838,plain, % 117.40/117.41 (P2(f4(a1,f2(a1,a1)),f4(a1,f2(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[796,792])). % 117.40/117.41 cnf(840,plain, % 117.40/117.41 (E(f2(a1,f4(a1,a1)),f5(f4(a1,f2(a1,a1)),f2(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[828,92,2,3])). % 117.40/117.41 cnf(842,plain, % 117.40/117.41 (P1(f5(f4(a1,f2(a1,a1)),f2(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[15,800,828,92,2,3,13,12])). % 117.40/117.41 cnf(843,plain, % 117.40/117.41 (P2(f2(a1,a1),f5(f2(a1,a1),a1))), % 117.40/117.41 inference(scs_inference,[],[15,800,809,797,828,92,2,3,13,12,14])). % 117.40/117.41 cnf(844,plain, % 117.40/117.41 (E(f4(f2(a1,a1),f5(f2(a1,a1),f2(a1,a1))),f2(a1,a1))), % 117.40/117.41 inference(scs_inference,[],[15,800,809,797,796,828,92,2,3,13,12,14,53])). % 117.40/117.41 cnf(846,plain, % 117.40/117.41 (P1(f5(f2(a1,a1),f2(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[15,800,809,797,796,828,92,2,3,13,12,14,53,48])). % 117.40/117.41 cnf(848,plain, % 117.40/117.41 (E(a1,f5(f2(a1,a1),f2(a1,a1)))), % 117.40/117.41 inference(scs_inference,[],[15,800,809,206,797,796,828,92,2,3,13,12,14,53,48,42])). % 117.40/117.41 cnf(853,plain, % 117.40/117.41 (P2(f5(f4(a1,f2(a1,a1)),f2(a1,a1)),f4(f2(a1,a1),a1))), % 117.40/117.41 inference(scs_inference,[],[817,828,844,2,13])). % 117.40/117.41 cnf(854,plain, % 117.40/117.41 (E(f4(a1,f2(a1,a1)),f5(f2(a1,a1),f2(a1,a6)))), % 117.40/117.41 inference(scs_inference,[],[817,130,828,844,820,2,13,3])). % 117.40/117.41 cnf(855,plain, % 117.40/117.41 (P2(a1,f5(f2(a1,a1),f2(a1,a6)))), % 117.40/117.41 inference(scs_inference,[],[817,824,130,828,844,525,820,2,13,3,14])). % 117.40/117.41 cnf(857,plain, % 117.40/117.41 (P1(f4(f2(a1,a1),f5(f2(a1,a1),f2(a1,a1))))), % 117.40/117.41 inference(scs_inference,[],[817,824,130,802,828,844,525,820,2,13,3,14,12])). % 117.40/117.42 cnf(858,plain, % 117.40/117.42 (E(f2(a1,a1),f5(f4(f2(a1,a1),a1),a1))), % 117.40/117.42 inference(scs_inference,[],[15,817,824,130,802,828,844,786,525,208,820,2,13,3,14,12,42])). % 117.40/117.42 cnf(862,plain, % 117.40/117.42 (E(f5(f2(a1,a1),f2(a1,a1)),a1)), % 117.40/117.42 inference(scs_inference,[],[848,2])). % 117.40/117.42 cnf(865,plain, % 117.40/117.42 (P2(f2(a1,a1),f5(f2(a1,a1),f2(a1,a6)))), % 117.40/117.42 inference(scs_inference,[],[843,802,804,848,858,525,2,13,12,14])). % 117.40/117.42 cnf(867,plain, % 117.40/117.42 (E(f2(a1,a1),f5(f5(f2(a1,a1),a1),a1))), % 117.40/117.42 inference(scs_inference,[],[15,843,824,802,804,848,823,858,525,783,2,13,12,14,42])). % 117.40/117.42 cnf(901,plain, % 117.40/117.42 (P2(f2(a1,f4(a1,a1)),f5(f2(a1,a1),a1))), % 117.40/117.42 inference(scs_inference,[],[787,855,804,828,854,2,13,14])). % 117.40/117.42 cnf(905,plain, % 117.40/117.42 (E(f5(f4(a1,f2(a1,a1)),f2(a1,a1)),f2(a1,f4(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[840,2])). % 117.40/117.42 cnf(908,plain, % 117.40/117.42 (P2(f5(f2(a1,a1),a1),f2(a1,a1))), % 117.40/117.42 inference(scs_inference,[],[901,809,797,525,840,2,14,13])). % 117.40/117.42 cnf(912,plain, % 117.40/117.42 (P2(f5(f2(a1,a1),f2(a1,a6)),f2(a1,a1))), % 117.40/117.42 inference(scs_inference,[],[908,525,13])). % 117.40/117.42 cnf(914,plain, % 117.40/117.42 (P2(f4(a1,f2(a1,a1)),f2(a1,a1))), % 117.40/117.42 inference(scs_inference,[],[908,838,130,525,13,14])). % 117.40/117.42 cnf(918,plain, % 117.40/117.42 (P2(f4(a1,f2(a1,a1)),f5(f2(a1,a1),a1))), % 117.40/117.42 inference(scs_inference,[],[914,804,14])). % 117.40/117.42 cnf(922,plain, % 117.40/117.42 (~P1(f2(f4(a1,a1),a6))+P1(f4(f4(a1,a1),f4(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[253,31])). % 117.40/117.42 cnf(926,plain, % 117.40/117.42 (E(a1,f5(f5(f2(a1,a1),a1),f2(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[15,918,843,206,796,797,823,525,3,14,42])). % 117.40/117.42 cnf(935,plain, % 117.40/117.42 (E(a1,f5(f5(f2(a1,a1),f2(a1,a6)),f2(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[15,865,206,802,926,825,820,2,3,42])). % 117.40/117.42 cnf(937,plain, % 117.40/117.42 (P1(f5(f5(f2(a1,a1),f2(a1,a6)),f2(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[15,865,206,802,926,825,820,2,3,42,12])). % 117.40/117.42 cnf(971,plain, % 117.40/117.42 (P1(f2(f4(a1,a1),a6))), % 117.40/117.42 inference(scs_inference,[],[15,267,31])). % 117.40/117.42 cnf(972,plain, % 117.40/117.42 (P1(f4(a1,a1))), % 117.40/117.42 inference(scs_inference,[],[971,253])). % 117.40/117.42 cnf(973,plain, % 117.40/117.42 (P2(a1,f4(a1,a1))), % 117.40/117.42 inference(scs_inference,[],[971,254])). % 117.40/117.42 cnf(974,plain, % 117.40/117.42 (E(a1,f5(f4(a1,a1),a1))), % 117.40/117.42 inference(scs_inference,[],[971,256])). % 117.40/117.42 cnf(977,plain, % 117.40/117.42 (P1(f2(a6,f4(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[971,260])). % 117.40/117.42 cnf(981,plain, % 117.40/117.42 (P2(a1,f2(f4(a1,a1),a6))), % 117.40/117.42 inference(scs_inference,[],[971,286])). % 117.40/117.42 cnf(982,plain, % 117.40/117.42 (P1(f4(f4(a1,a1),f4(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[971,922])). % 117.40/117.42 cnf(983,plain, % 117.40/117.42 (~P2(a1,f2(f4(a1,a1),a6))+E(a1,f5(f2(f4(a1,a1),a6),a1))), % 117.40/117.42 inference(scs_inference,[],[15,971,251,42])). % 117.40/117.42 cnf(986,plain, % 117.40/117.42 (~P2(a1,f2(f4(a1,a1),a6))+E(f5(f2(f4(a1,a1),a6),f2(a1,a6)),a1)), % 117.40/117.42 inference(scs_inference,[],[15,971,170,251,524,42,2,12,3])). % 117.40/117.42 cnf(990,plain, % 117.40/117.42 (P2(a1,f4(a1,a1))), % 117.40/117.42 inference(scs_inference,[],[972,55])). % 117.40/117.42 cnf(991,plain, % 117.40/117.42 (P1(f4(a1,a1))), % 117.40/117.42 inference(scs_inference,[],[977,171])). % 117.40/117.42 cnf(992,plain, % 117.40/117.42 (P2(a1,f4(a1,a1))), % 117.40/117.42 inference(scs_inference,[],[977,172])). % 117.40/117.42 cnf(993,plain, % 117.40/117.42 (E(a1,f5(f4(a1,a1),a1))), % 117.40/117.42 inference(scs_inference,[],[977,174])). % 117.40/117.42 cnf(995,plain, % 117.40/117.42 (P2(f2(a1,f4(a1,a1)),f4(a1,a1))), % 117.40/117.42 inference(scs_inference,[],[977,177])). % 117.40/117.42 cnf(1000,plain, % 117.40/117.42 (P2(f2(a1,f4(a1,a1)),f4(a1,a1))), % 117.40/117.42 inference(scs_inference,[],[972,186])). % 117.40/117.42 cnf(1001,plain, % 117.40/117.42 (P1(f4(a1,a1))), % 117.40/117.42 inference(scs_inference,[],[972,187])). % 117.40/117.42 cnf(1014,plain, % 117.40/117.42 (P1(f3(a1,f4(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[972,362])). % 117.40/117.42 cnf(1016,plain, % 117.40/117.42 (E(f5(f4(a1,a1),a1),a1)), % 117.40/117.42 inference(scs_inference,[],[974,2])). % 117.40/117.42 cnf(1018,plain, % 117.40/117.42 (P1(f5(f4(a1,a1),a1))), % 117.40/117.42 inference(scs_inference,[],[15,853,974,905,2,13,12])). % 117.40/117.42 cnf(1019,plain, % 117.40/117.42 (P2(f4(a1,a1),f4(f4(a1,a1),f4(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[15,853,972,982,974,905,2,13,12,47])). % 117.40/117.42 cnf(1021,plain, % 117.40/117.42 (E(f4(a1,a1),f5(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[15,853,972,982,974,905,2,13,12,47,54])). % 117.40/117.42 cnf(1023,plain, % 117.40/117.42 (P1(f5(f4(a1,a1),f2(a1,a6)))), % 117.40/117.42 inference(scs_inference,[],[15,853,972,982,974,905,2,13,12,47,54,529])). % 117.40/117.42 cnf(1024,plain, % 117.40/117.42 (P2(f4(a1,a1),x10241)+~E(f4(f4(a1,a1),f4(a1,a1)),x10241)), % 117.40/117.42 inference(scs_inference,[],[15,853,972,982,974,905,2,13,12,47,54,529,14])). % 117.40/117.42 cnf(1025,plain, % 117.40/117.42 (E(f2(a6,f4(a1,a1)),f5(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[15,853,972,982,974,169,905,2,13,12,47,54,529,14,3])). % 117.40/117.42 cnf(1033,plain, % 117.40/117.42 (E(a1,f5(f2(f4(a1,a1),a6),a1))), % 117.40/117.42 inference(scs_inference,[],[981,983])). % 117.40/117.42 cnf(1035,plain, % 117.40/117.42 (E(f5(f2(f4(a1,a1),a6),f2(a1,a6)),a1)), % 117.40/117.42 inference(scs_inference,[],[981,986])). % 117.40/117.42 cnf(1037,plain, % 117.40/117.42 (P2(f5(f4(a1,f2(a1,a1)),f2(a1,a1)),f4(a1,a1))), % 117.40/117.42 inference(scs_inference,[],[973,828,1021,2,13])). % 117.40/117.42 cnf(1039,plain, % 117.40/117.42 (P2(a1,f5(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[973,828,991,1021,2,13,12,14])). % 117.40/117.42 cnf(1057,plain, % 117.40/117.42 (E(f5(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1)),f2(a6,f4(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[1025,2])). % 117.40/117.42 cnf(1065,plain, % 117.40/117.42 (P2(f5(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1)),f4(f4(a1,a1),f4(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[1019,1021,1035,2,13])). % 117.40/117.42 cnf(1066,plain, % 117.40/117.42 (P2(f5(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1)),x10661)+~E(f4(f4(a1,a1),f4(a1,a1)),x10661)), % 117.40/117.42 inference(scs_inference,[],[1019,1021,1035,2,13,14])). % 117.40/117.42 cnf(1073,plain, % 117.40/117.42 (P2(f2(a6,f4(a1,a1)),x10731)+~E(f4(f4(a1,a1),f4(a1,a1)),x10731)), % 117.40/117.42 inference(scs_inference,[],[1065,1057,13,14])). % 117.40/117.42 cnf(1262,plain, % 117.40/117.42 (E(f2(a1,f4(a1,a1)),f5(f2(a1,a1),f2(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[848,92,3])). % 117.40/117.42 cnf(1263,plain, % 117.40/117.42 (E(f5(f2(a1,a1),f2(a1,a1)),f2(a1,f4(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[848,92,3,2])). % 117.40/117.42 cnf(1271,plain, % 117.40/117.42 (E(f2(a1,a1),f5(f4(f2(a1,a1),f2(a1,a1)),f2(a1,a1)))+~P2(f2(a1,a1),f4(f2(a1,a1),f2(a1,a1)))+~P1(f4(f2(a1,a1),f2(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[92,15,796,926,525,3,2,54])). % 117.40/117.42 cnf(1278,plain, % 117.40/117.42 (E(f5(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1)),f2(f4(a1,a1),a6))), % 117.40/117.42 inference(scs_inference,[],[266,1025,3,2])). % 117.40/117.42 cnf(1369,plain, % 117.40/117.42 (~E(f2(a1,a1),a1)+E(f2(f4(a1,f5(a1,a1)),x13691),f2(a1,x13691))), % 117.40/117.42 inference(scs_inference,[],[803,624,14])). % 117.40/117.42 cnf(1370,plain, % 117.40/117.42 (P1(f5(f4(a1,f2(a1,a1)),f2(a1,a6)))), % 117.40/117.42 inference(scs_inference,[],[15,807,779,524,34])). % 117.40/117.42 cnf(1402,plain, % 117.40/117.42 (E(f2(x14021,f4(a6,f5(a6,a6))),f2(x14021,a6))+~E(f4(a6,a1),a6)), % 117.40/117.42 inference(scs_inference,[],[16,15,686,33])). % 117.40/117.42 cnf(1636,plain, % 117.40/117.42 (P2(f5(f2(a1,a1),a1),f4(f2(a1,a1),f2(a1,a1)))+~P1(f4(f2(a1,a1),f2(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[804,835,13])). % 117.40/117.42 cnf(1790,plain, % 117.40/117.42 (P2(f5(f2(a1,a1),a1),x17901)+~E(f4(f2(a1,a1),f2(a1,a1)),x17901)+~P1(f4(f2(a1,a1),f2(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[1636,14])). % 117.40/117.42 cnf(1982,plain, % 117.40/117.42 (E(f2(a1,a1),f5(f5(f2(a1,a1),a1),f2(a1,a6)))), % 117.40/117.42 inference(scs_inference,[],[867,525,3])). % 117.40/117.42 cnf(1990,plain, % 117.40/117.42 (P2(f5(f5(f2(a1,a1),f2(a1,a6)),f2(a1,a1)),f4(a1,f2(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[785,935,130,1982,3,13])). % 117.40/117.42 cnf(2016,plain, % 117.40/117.42 (P2(f5(f5(f2(a1,a1),f2(a1,a6)),f2(a1,a1)),f2(a1,a1))), % 117.40/117.42 inference(scs_inference,[],[1990,130,14])). % 117.40/117.42 cnf(2023,plain, % 117.40/117.42 (P2(f5(f5(f2(a1,a1),f2(a1,a6)),f2(a1,a1)),f4(a1,a1))), % 117.40/117.42 inference(scs_inference,[],[992,935,13])). % 117.40/117.42 cnf(2117,plain, % 117.40/117.42 (P1(f5(f4(a6,a6),a6))+~P2(a6,f4(a6,a6))+~P1(f4(a6,a6))), % 117.40/117.42 inference(scs_inference,[],[16,537,12])). % 117.40/117.42 cnf(2133,plain, % 117.40/117.42 (~P2(a6,f4(a6,a6))+~P1(f4(a6,a6))+~E(f4(a7,f5(f4(a6,a6),a6)),a7)), % 117.40/117.42 inference(scs_inference,[],[19,17,2117,33])). % 117.40/117.42 cnf(2159,plain, % 117.40/117.42 (E(a7,f5(f4(a7,a7),a7))+~P1(f4(a7,a7))), % 117.40/117.42 inference(scs_inference,[],[17,574,47])). % 117.40/117.42 cnf(2190,plain, % 117.40/117.42 (E(f5(f4(a7,a7),a7),a7)+~P1(f4(a7,a7))), % 117.40/117.42 inference(scs_inference,[],[2159,2])). % 117.40/117.42 cnf(2221,plain, % 117.40/117.42 (E(f5(f4(a7,a7),a7),a7)), % 117.40/117.42 inference(scs_inference,[],[17,2190,31])). % 117.40/117.42 cnf(2222,plain, % 117.40/117.42 (E(a7,f5(f4(a7,a7),a7))), % 117.40/117.42 inference(scs_inference,[],[2221,2])). % 117.40/117.42 cnf(2223,plain, % 117.40/117.42 (P1(f5(f4(a7,a7),a7))), % 117.40/117.42 inference(scs_inference,[],[17,2221,2,12])). % 117.40/117.42 cnf(2224,plain, % 117.40/117.42 (~E(f4(a7,a7),f5(f4(a7,a7),a7))), % 117.40/117.42 inference(scs_inference,[],[412,17,2221,2,12,3])). % 117.40/117.42 cnf(2225,plain, % 117.40/117.42 (P2(f5(f4(a7,a7),a7),f4(a7,a7))+~P1(f4(a7,a7))), % 117.40/117.42 inference(scs_inference,[],[412,17,2221,2,12,3,395])). % 117.40/117.42 cnf(2258,plain, % 117.40/117.42 (P2(f5(f4(a7,a7),a7),x22581)+~E(f4(a7,a7),x22581)+~P1(f4(a7,a7))), % 117.40/117.42 inference(scs_inference,[],[2225,14])). % 117.40/117.42 cnf(2454,plain, % 117.40/117.42 (~P1(f4(a6,a6))+~E(f4(a7,f5(f4(a6,a6),a6)),a7)), % 117.40/117.42 inference(scs_inference,[],[2133,378])). % 117.40/117.42 cnf(2485,plain, % 117.40/117.42 (~E(f4(a7,f5(f4(a6,a6),a6)),a7)), % 117.40/117.42 inference(scs_inference,[],[16,2454,31])). % 117.40/117.42 cnf(2616,plain, % 117.40/117.42 (E(f2(a1,a1),f5(f4(f2(a1,a1),f2(a1,a1)),f2(a1,a1)))+~P1(f4(f2(a1,a1),f2(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[1271,835])). % 117.40/117.42 cnf(2632,plain, % 117.40/117.42 (E(f5(f4(f2(a1,a1),f2(a1,a1)),f2(a1,a1)),f2(a1,a1))+~P1(f4(f2(a1,a1),f2(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[2616,2])). % 117.40/117.42 cnf(2648,plain, % 117.40/117.42 (E(f5(f4(f2(a1,a1),f2(a1,a1)),f2(a1,a1)),f2(a1,a1))), % 117.40/117.42 inference(scs_inference,[],[802,2632,31])). % 117.40/117.42 cnf(2649,plain, % 117.40/117.42 (E(f2(a1,a1),f5(f4(f2(a1,a1),f2(a1,a1)),f2(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[2648,2])). % 117.40/117.42 cnf(2897,plain, % 117.40/117.42 (E(a1,f2(a1,a1))), % 117.40/117.42 inference(scs_inference,[],[15,2,20])). % 117.40/117.42 cnf(2898,plain, % 117.40/117.42 (E(f2(a1,a1),a1)), % 117.40/117.42 inference(scs_inference,[],[2897,2])). % 117.40/117.42 cnf(2899,plain, % 117.40/117.42 (E(f2(f2(a1,f4(a1,a1)),a1),f2(a1,a1))), % 117.40/117.42 inference(scs_inference,[],[111,2897,2,3])). % 117.40/117.42 cnf(2900,plain, % 117.40/117.42 (E(f2(f4(a1,f5(a1,a1)),x29001),f2(a1,x29001))), % 117.40/117.42 inference(scs_inference,[],[111,2897,2,3,1369])). % 117.40/117.42 cnf(2906,plain, % 117.40/117.42 (E(f4(f2(a1,a1),a1),a1)), % 117.40/117.42 inference(scs_inference,[],[206,2900,2898,2,3])). % 117.40/117.42 cnf(2908,plain, % 117.40/117.42 (P2(f2(a1,a1),a1)), % 117.40/117.42 inference(scs_inference,[],[206,15,802,2900,2898,2,3,12,33])). % 117.40/117.42 cnf(2910,plain, % 117.40/117.42 (E(a1,f5(a1,f2(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[206,15,802,2900,2898,2,3,12,33,42])). % 117.40/117.42 cnf(2912,plain, % 117.40/117.42 (P2(f2(a1,a1),f5(f4(a1,f2(a1,a1)),f2(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[206,15,802,828,2900,2898,2,3,12,33,42,14])). % 117.40/117.42 cnf(2913,plain, % 117.40/117.42 (P2(f5(f2(a1,a1),a1),a1)), % 117.40/117.42 inference(scs_inference,[],[206,15,802,804,828,2900,2898,2,3,12,33,42,14,13])). % 117.40/117.42 cnf(2916,plain, % 117.40/117.42 (E(f5(a1,f2(a1,a1)),a1)), % 117.40/117.42 inference(scs_inference,[],[2910,2])). % 117.40/117.42 cnf(2917,plain, % 117.40/117.42 (P2(f2(a1,a1),f2(a1,f4(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[2912,2910,905,2,14])). % 117.40/117.42 cnf(2918,plain, % 117.40/117.42 (P2(f5(f2(a1,a1),a1),f5(f4(a1,f2(a1,a1)),f2(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[2912,797,2910,905,2,14,13])). % 117.40/117.42 cnf(2919,plain, % 117.40/117.42 (P1(f5(a1,f2(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[15,2912,797,2910,905,2,14,13,12])). % 117.40/117.42 cnf(2924,plain, % 117.40/117.42 (P2(f5(f2(a1,a1),f2(a1,a6)),f5(f4(a1,f2(a1,a1)),f2(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[2918,525,905,2899,2,14,13])). % 117.40/117.42 cnf(2928,plain, % 117.40/117.42 (E(a1,f4(f2(a1,a1),a1))), % 117.40/117.42 inference(scs_inference,[],[2906,2])). % 117.40/117.42 cnf(2930,plain, % 117.40/117.42 (P2(f5(f2(a1,a1),f2(a1,a6)),a1)), % 117.40/117.42 inference(scs_inference,[],[2924,2913,525,905,2906,2,14,13])). % 117.40/117.42 cnf(3006,plain, % 117.40/117.42 (E(f4(f2(a1,a1),x30061),f4(f4(f2(a1,a1),a1),x30061))), % 117.40/117.42 inference(scs_inference,[],[206,2,6])). % 117.40/117.42 cnf(3046,plain, % 117.40/117.42 (E(f5(f2(a1,a1),f2(a1,a1)),f5(a1,f2(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[207,15,914,865,2908,844,796,846,2898,13,3,14,42])). % 117.40/117.42 cnf(3048,plain, % 117.40/117.42 (E(a1,f4(f2(a1,a1),f5(f2(a1,a1),f2(a1,a1))))), % 117.40/117.42 inference(scs_inference,[],[207,15,914,865,2908,844,796,846,2898,13,3,14,42,2])). % 117.40/117.42 cnf(3051,plain, % 117.40/117.42 (E(f5(a1,f2(a1,a1)),f5(f2(a1,a1),f2(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[3046,2])). % 117.40/117.42 cnf(3053,plain, % 117.40/117.42 (P2(f2(a1,a1),f4(f2(a1,a1),a1))), % 117.40/117.42 inference(scs_inference,[],[207,843,809,3046,2,13,14])). % 117.40/117.42 cnf(3056,plain, % 117.40/117.42 (P2(f4(f2(a1,a1),a1),f2(a1,a1))), % 117.40/117.42 inference(scs_inference,[],[207,809,13])). % 117.40/117.42 cnf(3061,plain, % 117.40/117.42 (P2(f4(f2(a1,a1),a1),f4(f2(a1,a1),a1))), % 117.40/117.42 inference(scs_inference,[],[207,819,3056,13,14])). % 117.40/117.42 cnf(3071,plain, % 117.40/117.42 (P2(f4(f2(a1,a1),a1),a1)), % 117.40/117.42 inference(scs_inference,[],[207,2917,92,13,14])). % 117.40/117.42 cnf(3106,plain, % 117.40/117.42 (E(f4(f5(a1,f2(a1,a1)),x31061),f4(a1,x31061))), % 117.40/117.42 inference(scs_inference,[],[2916,1023,22,23,24,25,20,21,4,5,6])). % 117.40/117.42 cnf(3107,plain, % 117.40/117.42 (E(f4(x31071,f5(a1,f2(a1,a1))),f4(x31071,a1))), % 117.40/117.42 inference(scs_inference,[],[2916,1023,22,23,24,25,20,21,4,5,6,7])). % 117.40/117.42 cnf(3110,plain, % 117.40/117.42 (E(f5(f5(a1,f2(a1,a1)),x31101),f5(a1,x31101))), % 117.40/117.42 inference(scs_inference,[],[2916,1023,22,23,24,25,20,21,4,5,6,7,8,9,10])). % 117.40/117.42 cnf(3117,plain, % 117.40/117.42 (E(f4(f2(a1,a1),x31171),f4(f4(f2(a1,a1),a1),x31171))), % 117.40/117.42 inference(rename_variables,[],[3006])). % 117.40/117.42 cnf(3133,plain, % 117.40/117.42 (E(f4(f2(a6,a6),f2(a6,a6)),f2(f4(a6,a6),a6))), % 117.40/117.42 inference(scs_inference,[],[2916,2928,2930,3053,1023,808,2649,3061,1370,3048,3006,2485,2908,802,16,15,22,23,24,25,20,21,4,5,6,7,8,9,10,11,526,2,32,12,31,3,13,14,35,41,43,44,45,46])). % 117.40/117.42 cnf(3147,plain, % 117.40/117.42 (P2(f5(f2(a1,a1),a1),f4(f4(f2(a1,a1),a1),f2(a1,a1)))+~P1(f4(f2(a1,a1),f2(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[2916,2928,2930,3053,1023,808,2649,3051,3061,1370,3048,857,3006,3117,2485,2908,846,807,825,779,802,16,809,15,22,23,24,25,20,21,4,5,6,7,8,9,10,11,526,2,32,12,31,3,13,14,35,41,43,44,45,46,48,47,40,34,54,27,1790])). % 117.40/117.42 cnf(3152,plain, % 117.40/117.42 (E(f2(f2(a1,a1),a6),f2(a1,a1))), % 117.40/117.42 inference(scs_inference,[],[1014,780,21,25])). % 117.40/117.42 cnf(3155,plain, % 117.40/117.42 (E(f2(a6,f2(a1,a1)),f2(a1,a1))), % 117.40/117.42 inference(scs_inference,[],[1014,1016,780,21,25,7,23])). % 117.40/117.42 cnf(3159,plain, % 117.40/117.42 (E(f4(a1,f4(a1,a1)),f4(a1,a1))), % 117.40/117.42 inference(scs_inference,[],[1014,1016,991,780,21,25,7,23,20,22])). % 117.40/117.42 cnf(3170,plain, % 117.40/117.42 (~E(a6,a1)), % 117.40/117.42 inference(scs_inference,[],[1014,1016,18,991,780,21,25,7,23,20,22,6,24,8,10,11,4,5,9,2])). % 117.40/117.42 cnf(3171,plain, % 117.40/117.42 (P1(f2(f4(a1,a1),f4(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[1014,1016,18,991,780,21,25,7,23,20,22,6,24,8,10,11,4,5,9,2,32])). % 117.40/117.42 cnf(3173,plain, % 117.40/117.42 (P1(f4(f2(a1,a1),f2(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[1014,1016,18,991,780,21,25,7,23,20,22,6,24,8,10,11,4,5,9,2,32,31])). % 117.40/117.42 cnf(3177,plain, % 117.40/117.42 (~P2(a7,f5(f4(a7,a7),a7))), % 117.40/117.42 inference(scs_inference,[],[19,1014,1016,1033,18,2221,991,780,21,25,7,23,20,22,6,24,8,10,11,4,5,9,2,32,31,3,13,14])). % 117.40/117.42 cnf(3180,plain, % 117.40/117.42 (~E(f4(a6,a6),a1)), % 117.40/117.42 inference(scs_inference,[],[19,1014,1016,1033,18,2221,991,780,16,15,21,25,7,23,20,22,6,24,8,10,11,4,5,9,2,32,31,3,13,14,45,26])). % 117.40/117.42 cnf(3188,plain, % 117.40/117.42 (E(f4(f2(a1,a1),f2(a1,a1)),f2(f4(a1,a1),a1))), % 117.40/117.42 inference(scs_inference,[],[19,3071,1014,812,1016,1033,18,2221,991,780,16,809,15,21,25,7,23,20,22,6,24,8,10,11,4,5,9,2,32,31,3,13,14,45,26,44,41,35,46])). % 117.40/117.42 cnf(3192,plain, % 117.40/117.42 (P2(f2(a1,a1),f4(f2(a1,a1),f2(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[19,3071,1014,812,1016,1033,18,2221,991,780,16,809,15,21,25,7,23,20,22,6,24,8,10,11,4,5,9,2,32,31,3,13,14,45,26,44,41,35,46,43,47])). % 117.40/117.42 cnf(3196,plain, % 117.40/117.42 (~E(f4(a6,a6),f4(a6,a1))), % 117.40/117.42 inference(scs_inference,[],[19,3071,1014,812,1016,1033,18,2908,2221,991,780,16,809,15,21,25,7,23,20,22,6,24,8,10,11,4,5,9,2,32,31,3,13,14,45,26,44,41,35,46,43,47,53,36])). % 117.40/117.42 cnf(3198,plain, % 117.40/117.42 (~E(f4(a6,a6),f4(a1,a6))), % 117.40/117.42 inference(scs_inference,[],[19,3071,1014,812,1016,1033,18,2908,2221,991,780,16,809,15,21,25,7,23,20,22,6,24,8,10,11,4,5,9,2,32,31,3,13,14,45,26,44,41,35,46,43,47,53,36,37])). % 117.40/117.42 cnf(3200,plain, % 117.40/117.42 (~E(f2(a6,a6),a1)), % 117.40/117.42 inference(scs_inference,[],[19,3071,1014,812,1016,1033,18,2908,2221,991,780,16,809,15,21,25,7,23,20,22,6,24,8,10,11,4,5,9,2,32,31,3,13,14,45,26,44,41,35,46,43,47,53,36,37,28])). % 117.40/117.42 cnf(3209,plain, % 117.40/117.42 (~P2(a1,a1)+P1(f5(f5(a1,f2(a1,a1)),a1))), % 117.40/117.42 inference(scs_inference,[],[19,3071,1014,812,3110,1016,1262,1033,18,2908,2221,991,780,16,809,15,21,25,7,23,20,22,6,24,8,10,11,4,5,9,2,32,31,3,13,14,45,26,44,41,35,46,43,47,53,36,37,28,40,3147,27,48,34])). % 117.40/117.42 cnf(3214,plain, % 117.40/117.42 (~E(f2(a6,a6),f2(a6,a1))), % 117.40/117.42 inference(scs_inference,[],[19,3071,1014,812,3110,1016,1262,1033,18,2908,3053,2221,991,780,16,809,15,21,25,7,23,20,22,6,24,8,10,11,4,5,9,2,32,31,3,13,14,45,26,44,41,35,46,43,47,53,36,37,28,40,3147,27,48,34,54,38])). % 117.40/117.42 cnf(3216,plain, % 117.40/117.42 (~E(f2(a6,a6),f2(a1,a6))), % 117.40/117.42 inference(scs_inference,[],[19,3071,1014,812,3110,1016,1262,1033,18,2908,3053,2221,991,780,16,809,15,21,25,7,23,20,22,6,24,8,10,11,4,5,9,2,32,31,3,13,14,45,26,44,41,35,46,43,47,53,36,37,28,40,3147,27,48,34,54,38,39])). % 117.40/117.42 cnf(3221,plain, % 117.40/117.42 (~E(f4(f2(a1,a1),f2(a1,a1)),x32211)+P2(f5(f2(a1,a1),a1),x32211)), % 117.40/117.42 inference(scs_inference,[],[3173,1790])). % 117.40/117.42 cnf(3222,plain, % 117.40/117.42 (E(f2(a6,a6),a6)), % 117.40/117.42 inference(scs_inference,[],[16,23])). % 117.40/117.42 cnf(3224,plain, % 117.40/117.42 (E(f2(a1,a6),a1)), % 117.40/117.42 inference(scs_inference,[],[16,15,23,25])). % 117.40/117.42 cnf(3226,plain, % 117.40/117.42 (E(f4(a1,a6),a6)), % 117.40/117.42 inference(scs_inference,[],[16,15,23,25,22])). % 117.40/117.42 cnf(3233,plain, % 117.40/117.42 (E(f4(a6,a1),a6)), % 117.40/117.42 inference(scs_inference,[],[3171,862,16,15,23,25,22,21,20,10,24])). % 117.40/117.42 cnf(3242,plain, % 117.40/117.42 (~E(f4(a6,a1),f4(a6,a6))), % 117.40/117.42 inference(scs_inference,[],[3196,3171,862,16,15,23,25,22,21,20,10,24,8,6,11,7,5,9,4,2])). % 117.40/117.42 cnf(3243,plain, % 117.40/117.42 (P1(f2(f2(a1,a1),f2(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[3196,3171,862,796,16,15,23,25,22,21,20,10,24,8,6,11,7,5,9,4,2,32])). % 117.40/117.42 cnf(3245,plain, % 117.40/117.42 (P1(f4(a6,a6))), % 117.40/117.42 inference(scs_inference,[],[3196,3171,862,796,16,15,23,25,22,21,20,10,24,8,6,11,7,5,9,4,2,32,31])). % 117.40/117.42 cnf(3248,plain, % 117.40/117.42 (P2(f2(f4(a1,a1),a6),f4(f4(a1,a1),f4(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[3196,3159,3171,1278,862,1065,251,796,16,15,23,25,22,21,20,10,24,8,6,11,7,5,9,4,2,32,31,3,13])). % 117.40/117.42 cnf(3262,plain, % 117.40/117.42 (~E(f4(f4(a6,a6),f4(a6,a6)),a1)), % 117.40/117.42 inference(scs_inference,[],[3170,3196,3180,3159,3171,3173,3192,3188,1278,862,1065,251,796,16,15,17,23,25,22,21,20,10,24,8,6,11,7,5,9,4,2,32,31,3,13,14,26,45,43,44,46,35,27])). % 117.40/117.42 cnf(3266,plain, % 117.40/117.42 (~E(f4(a1,a1),f4(a6,a1))), % 117.40/117.42 inference(scs_inference,[],[3170,3196,3180,3159,3171,3173,3192,3188,1278,862,1065,18,251,1001,796,16,15,17,23,25,22,21,20,10,24,8,6,11,7,5,9,4,2,32,31,3,13,14,26,45,43,44,46,35,27,36,37])). % 117.40/117.42 cnf(3268,plain, % 117.40/117.42 (~E(f2(f4(a6,a6),a6),a1)), % 117.40/117.42 inference(scs_inference,[],[3170,3196,3180,3159,3171,3173,3192,3188,1278,862,1065,18,251,1001,796,16,15,17,23,25,22,21,20,10,24,8,6,11,7,5,9,4,2,32,31,3,13,14,26,45,43,44,46,35,27,36,37,28])). % 117.40/117.42 cnf(3270,plain, % 117.40/117.42 (~E(f2(a1,a6),f2(a6,a6))), % 117.40/117.42 inference(scs_inference,[],[3170,3196,3180,3159,3171,3173,3192,3188,1278,862,1065,18,251,1001,796,16,15,17,23,25,22,21,20,10,24,8,6,11,7,5,9,4,2,32,31,3,13,14,26,45,43,44,46,35,27,36,37,28,39])). % 117.40/117.42 cnf(3272,plain, % 117.40/117.42 (~E(f2(f4(a6,a6),a6),f2(f4(a6,a6),a1))), % 117.40/117.42 inference(scs_inference,[],[3170,3196,3180,3159,3171,3173,3192,3188,1278,862,1065,18,251,1001,796,16,15,17,23,25,22,21,20,10,24,8,6,11,7,5,9,4,2,32,31,3,13,14,26,45,43,44,46,35,27,36,37,28,39,38])). % 117.40/117.42 cnf(3276,plain, % 117.40/117.42 (P2(x32761,f4(a6,a6))+~E(a6,x32761)), % 117.40/117.42 inference(scs_inference,[],[3170,3196,3180,3159,3171,3173,3192,3188,1278,862,1065,18,251,1001,796,16,15,17,23,25,22,21,20,10,24,8,6,11,7,5,9,4,2,32,31,3,13,14,26,45,43,44,46,35,27,36,37,28,39,38,3221,378])). % 117.40/117.42 cnf(3277,plain, % 117.40/117.42 (P2(f5(f4(a6,a6),a6),f4(a6,a6))+~P2(a6,f4(a6,a6))), % 117.40/117.42 inference(scs_inference,[],[3170,3196,3180,3159,3171,3173,3192,3188,1278,862,1065,18,251,1001,796,16,15,17,23,25,22,21,20,10,24,8,6,11,7,5,9,4,2,32,31,3,13,14,26,45,43,44,46,35,27,36,37,28,39,38,3221,378,537])). % 117.40/117.42 cnf(3282,plain, % 117.40/117.42 (P2(a6,f4(a6,a6))), % 117.40/117.42 inference(equality_inference,[],[3276])). % 117.40/117.42 cnf(3283,plain, % 117.40/117.42 (~P2(a1,a1)+E(a6,f5(f4(a6,a6),a6))), % 117.40/117.42 inference(scs_inference,[],[3245,60])). % 117.40/117.42 cnf(3284,plain, % 117.40/117.42 (P1(f5(a6,a6))), % 117.40/117.42 inference(scs_inference,[],[3233,316])). % 117.40/117.42 cnf(3285,plain, % 117.40/117.42 (P1(f2(f5(a6,a6),f5(a6,a6)))), % 117.40/117.42 inference(scs_inference,[],[3233,444])). % 117.40/117.42 cnf(3288,plain, % 117.40/117.42 (E(f2(x32881,f4(a6,f5(a6,a6))),f2(x32881,a6))), % 117.40/117.42 inference(scs_inference,[],[3233,1402])). % 117.40/117.42 cnf(3291,plain, % 117.40/117.42 (P1(f5(f4(a6,a6),a6))), % 117.40/117.42 inference(scs_inference,[],[3282,3245,2117])). % 117.40/117.42 cnf(3294,plain, % 117.40/117.42 (P2(f5(f4(a6,a6),a6),f4(a6,a6))), % 117.40/117.42 inference(scs_inference,[],[3282,3277])). % 117.40/117.42 cnf(3295,plain, % 117.40/117.42 (E(f2(f4(a6,a6),a6),f4(a6,a6))), % 117.40/117.42 inference(scs_inference,[],[3245,3282,3277,25])). % 117.40/117.42 cnf(3297,plain, % 117.40/117.42 (E(f2(f4(a6,a6),a1),a1)), % 117.40/117.42 inference(scs_inference,[],[3245,3282,3277,25,21])). % 117.40/117.42 cnf(3299,plain, % 117.40/117.42 (E(f2(a6,f4(a6,a6)),f4(a6,a6))), % 117.40/117.42 inference(scs_inference,[],[3245,3282,3277,25,21,23])). % 117.40/117.42 cnf(3301,plain, % 117.40/117.42 (E(f2(a1,f4(a6,a6)),a1)), % 117.40/117.42 inference(scs_inference,[],[3245,3282,3277,25,21,23,20])). % 117.40/117.42 cnf(3303,plain, % 117.40/117.42 (E(f4(f4(a6,a6),a1),f4(a6,a6))), % 117.40/117.42 inference(scs_inference,[],[3245,3282,3277,25,21,23,20,24])). % 117.40/117.42 cnf(3307,plain, % 117.40/117.42 (E(f5(x33071,f2(a6,a6)),f5(x33071,a6))), % 117.40/117.42 inference(scs_inference,[],[3245,3282,3222,3277,25,21,23,20,24,22,11])). % 117.40/117.42 cnf(3308,plain, % 117.40/117.42 (E(f4(f2(a6,a6),x33081),f4(a6,x33081))), % 117.40/117.42 inference(scs_inference,[],[3245,3282,3222,3277,25,21,23,20,24,22,11,6])). % 117.40/117.42 cnf(3313,plain, % 117.40/117.42 (E(f2(f2(a6,a6),x33131),f2(a6,x33131))), % 117.40/117.42 inference(scs_inference,[],[3245,3282,3222,3277,25,21,23,20,24,22,11,6,10,8,7,9,4])). % 117.40/117.42 cnf(3314,plain, % 117.40/117.42 (E(f2(x33141,f2(a6,a6)),f2(x33141,a6))), % 117.40/117.42 inference(scs_inference,[],[3245,3282,3222,3277,25,21,23,20,24,22,11,6,10,8,7,9,4,5])). % 117.40/117.42 cnf(3315,plain, % 117.40/117.42 (~E(f4(a6,a1),f4(a1,a1))), % 117.40/117.42 inference(scs_inference,[],[3245,3282,3266,3222,3277,25,21,23,20,24,22,11,6,10,8,7,9,4,5,2])). % 117.40/117.42 cnf(3316,plain, % 117.40/117.42 (P1(f2(f4(a6,a6),f4(a6,a6)))), % 117.40/117.42 inference(scs_inference,[],[3245,3282,3266,3222,3277,25,21,23,20,24,22,11,6,10,8,7,9,4,5,2,32])). % 117.40/117.42 cnf(3318,plain, % 117.40/117.42 (P1(f4(f4(a6,a6),f4(a6,a6)))), % 117.40/117.42 inference(scs_inference,[],[3245,3282,3266,3222,3277,25,21,23,20,24,22,11,6,10,8,7,9,4,5,2,32,31])). % 117.40/117.42 cnf(3320,plain, % 117.40/117.42 (~E(f2(f4(a1,a1),a6),f4(a6,a1))), % 117.40/117.42 inference(scs_inference,[],[3245,3282,3266,3222,251,3277,25,21,23,20,24,22,11,6,10,8,7,9,4,5,2,32,31,3])). % 117.40/117.42 cnf(3324,plain, % 117.40/117.42 (P1(f3(f2(a1,a1),f2(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[3245,3282,3266,3222,3177,2221,251,796,16,809,3277,25,21,23,20,24,22,11,6,10,8,7,9,4,5,2,32,31,3,13,41,35])). % 117.40/117.42 cnf(3326,plain, % 117.40/117.42 (P2(f4(a6,a6),f4(f4(a6,a6),f4(a6,a6)))), % 117.40/117.42 inference(scs_inference,[],[3245,3282,3266,3222,3177,2221,251,796,16,809,3277,25,21,23,20,24,22,11,6,10,8,7,9,4,5,2,32,31,3,13,41,35,47])). % 117.40/117.42 cnf(3330,plain, % 117.40/117.42 (~E(f2(f4(a6,a6),f4(a6,a6)),a1)), % 117.40/117.42 inference(scs_inference,[],[3245,3282,3266,3222,3177,3180,2221,251,796,16,809,3277,25,21,23,20,24,22,11,6,10,8,7,9,4,5,2,32,31,3,13,41,35,47,53,28])). % 117.40/117.42 cnf(3336,plain, % 117.40/117.42 (P1(f5(f4(a6,a6),f2(a6,a6)))), % 117.40/117.42 inference(scs_inference,[],[3245,3282,3266,3222,3177,3262,3180,2221,251,796,16,809,15,3277,25,21,23,20,24,22,11,6,10,8,7,9,4,5,2,32,31,3,13,41,35,47,53,28,37,36,34])). % 117.40/117.42 cnf(3338,plain, % 117.40/117.42 (E(f4(a6,a6),f5(f4(f4(a6,a6),f4(a6,a6)),f4(a6,a6)))), % 117.40/117.42 inference(scs_inference,[],[3245,3282,3266,3222,3177,3262,3180,2221,251,796,16,809,15,3277,25,21,23,20,24,22,11,6,10,8,7,9,4,5,2,32,31,3,13,41,35,47,53,28,37,36,34,54])). % 117.40/117.42 cnf(3358,plain, % 117.40/117.42 (E(f2(f5(a6,a6),a6),f5(a6,a6))), % 117.40/117.42 inference(scs_inference,[],[3284,25])). % 117.40/117.42 cnf(3362,plain, % 117.40/117.42 (E(f4(f5(a6,a6),a1),f5(a6,a6))), % 117.40/117.42 inference(scs_inference,[],[3284,25,23,24])). % 117.40/117.42 cnf(3366,plain, % 117.40/117.42 (E(f2(a1,f5(a6,a6)),a1)), % 117.40/117.42 inference(scs_inference,[],[3284,25,23,24,22,20])). % 117.40/117.42 cnf(3368,plain, % 117.40/117.42 (E(f2(f5(a6,a6),a1),a1)), % 117.40/117.42 inference(scs_inference,[],[3284,25,23,24,22,20,21])). % 117.40/117.42 cnf(3372,plain, % 117.40/117.42 (E(f5(x33721,f4(a6,a1)),f5(x33721,a6))), % 117.40/117.42 inference(scs_inference,[],[3284,3233,25,23,24,22,20,21,10,6,11])). % 117.40/117.42 cnf(3376,plain, % 117.40/117.42 (E(f2(x33761,f4(a6,a1)),f2(x33761,a6))), % 117.40/117.42 inference(scs_inference,[],[3284,3233,25,23,24,22,20,21,10,6,11,8,7,9,5])). % 117.40/117.42 cnf(3377,plain, % 117.40/117.42 (E(f2(f4(a6,a1),x33771),f2(a6,x33771))), % 117.40/117.42 inference(scs_inference,[],[3284,3233,25,23,24,22,20,21,10,6,11,8,7,9,5,4])). % 117.40/117.42 cnf(3378,plain, % 117.40/117.42 (~E(f4(a1,a6),f4(a6,a6))), % 117.40/117.42 inference(scs_inference,[],[3284,3198,3233,25,23,24,22,20,21,10,6,11,8,7,9,5,4,2])). % 117.40/117.42 cnf(3379,plain, % 117.40/117.42 (P1(f2(a6,a6))), % 117.40/117.42 inference(scs_inference,[],[3284,3198,3233,16,25,23,24,22,20,21,10,6,11,8,7,9,5,4,2,32])). % 117.40/117.42 cnf(3381,plain, % 117.40/117.42 (P1(f5(f4(f4(a6,a6),f4(a6,a6)),f4(a6,a6)))), % 117.40/117.42 inference(scs_inference,[],[3284,3198,3233,3338,3245,16,25,23,24,22,20,21,10,6,11,8,7,9,5,4,2,32,12])). % 117.40/117.42 cnf(3382,plain, % 117.40/117.42 (P1(f4(f5(a6,a6),f5(a6,a6)))), % 117.40/117.42 inference(scs_inference,[],[3284,3198,3233,3338,3245,16,25,23,24,22,20,21,10,6,11,8,7,9,5,4,2,32,12,31])). % 117.40/117.42 cnf(3386,plain, % 117.40/117.42 (~E(f4(f2(a6,a6),f2(a6,a6)),a1)), % 117.40/117.42 inference(scs_inference,[],[3284,3315,3198,3200,3233,3326,3338,3245,16,25,23,24,22,20,21,10,6,11,8,7,9,5,4,2,32,12,31,3,13,26])). % 117.40/117.42 cnf(3392,plain, % 117.40/117.42 (P2(f5(a6,a6),f4(f5(a6,a6),f5(a6,a6)))), % 117.40/117.42 inference(scs_inference,[],[3284,3315,3198,3200,3233,3294,3326,3291,3338,3245,781,796,16,15,25,23,24,22,20,21,10,6,11,8,7,9,5,4,2,32,12,31,3,13,26,41,35,47])). % 117.40/117.42 cnf(3396,plain, % 117.40/117.42 (~E(f4(a7,f5(a6,a6)),a7)), % 117.40/117.42 inference(scs_inference,[],[19,3284,3315,3198,3200,3233,3294,3326,3291,3338,3245,781,796,16,15,17,25,23,24,22,20,21,10,6,11,8,7,9,5,4,2,32,12,31,3,13,26,41,35,47,27,33])). % 117.40/117.42 cnf(3400,plain, % 117.40/117.42 (E(f2(a6,a1),a1)), % 117.40/117.42 inference(scs_inference,[],[15,23])). % 117.40/117.42 cnf(3402,plain, % 117.40/117.42 (E(f2(a7,a6),a7)), % 117.40/117.42 inference(scs_inference,[],[15,17,23,25])). % 117.40/117.42 cnf(3404,plain, % 117.40/117.42 (E(f2(f2(a6,a6),a1),a1)), % 117.40/117.42 inference(scs_inference,[],[3379,15,17,23,25,21])). % 117.40/117.42 cnf(3406,plain, % 117.40/117.42 (E(f4(a1,f2(a6,a6)),f2(a6,a6))), % 117.40/117.42 inference(scs_inference,[],[3379,15,17,23,25,21,22])). % 117.40/117.42 cnf(3408,plain, % 117.40/117.42 (E(f2(a1,f2(a6,a6)),a1)), % 117.40/117.42 inference(scs_inference,[],[3379,15,17,23,25,21,22,20])). % 117.40/117.42 cnf(3410,plain, % 117.40/117.42 (E(f4(f2(a6,a6),a1),f2(a6,a6))), % 117.40/117.42 inference(scs_inference,[],[3379,15,17,23,25,21,22,20,24])). % 117.40/117.42 cnf(3415,plain, % 117.40/117.42 (E(f4(f2(a1,a6),x34151),f4(a1,x34151))), % 117.40/117.42 inference(scs_inference,[],[3379,3224,3226,15,17,23,25,21,22,20,24,10,8,11,6])). % 117.40/117.42 cnf(3421,plain, % 117.40/117.42 (P1(f2(f2(a6,a6),f2(a6,a6)))), % 117.40/117.42 inference(scs_inference,[],[3379,3214,3224,3226,15,17,23,25,21,22,20,24,10,8,11,6,7,5,4,9,2,32])). % 117.40/117.42 cnf(3423,plain, % 117.40/117.42 (P1(f4(f2(a6,a6),f2(a6,a6)))), % 117.40/117.42 inference(scs_inference,[],[3379,3214,3224,3226,15,17,23,25,21,22,20,24,10,8,11,6,7,5,4,9,2,32,31])). % 117.40/117.42 cnf(3425,plain, % 117.40/117.42 (~E(a1,f2(a6,a6))), % 117.40/117.42 inference(scs_inference,[],[3379,3270,3214,3224,3226,15,17,23,25,21,22,20,24,10,8,11,6,7,5,4,9,2,32,31,3])). % 117.40/117.42 cnf(3432,plain, % 117.40/117.42 (~E(f2(f2(a6,a6),f2(a6,a6)),a1)), % 117.40/117.42 inference(scs_inference,[],[3379,3270,3214,3224,3226,3382,3392,3386,3200,3284,15,17,23,25,21,22,20,24,10,8,11,6,7,5,4,9,2,32,31,3,26,27,35,28])). % 117.40/117.42 cnf(3446,plain, % 117.40/117.42 (E(f4(a1,a1),a1)), % 117.40/117.42 inference(scs_inference,[],[15,22])). % 117.40/117.42 cnf(3448,plain, % 117.40/117.42 (E(f2(a6,a7),a7)), % 117.40/117.42 inference(scs_inference,[],[15,17,22,23])). % 117.40/117.42 cnf(3450,plain, % 117.40/117.42 (E(f4(a7,a1),a7)), % 117.40/117.42 inference(scs_inference,[],[15,17,22,23,24])). % 117.40/117.42 cnf(3456,plain, % 117.40/117.42 (E(f4(f2(a6,a1),x34561),f4(a1,x34561))), % 117.40/117.42 inference(scs_inference,[],[3400,3243,15,17,22,23,24,20,21,6])). % 117.40/117.42 cnf(3458,plain, % 117.40/117.42 (E(f5(x34581,f2(a6,a1)),f5(x34581,a1))), % 117.40/117.42 inference(scs_inference,[],[3400,3243,15,17,22,23,24,20,21,6,10,11])). % 117.40/117.42 cnf(3460,plain, % 117.40/117.42 (E(f4(x34601,f2(a6,a1)),f4(x34601,a1))), % 117.40/117.42 inference(scs_inference,[],[3400,3243,15,17,22,23,24,20,21,6,10,11,8,7])). % 117.40/117.42 cnf(3465,plain, % 117.40/117.42 (P1(f4(a7,a7))), % 117.40/117.42 inference(scs_inference,[],[3400,3320,3243,15,17,22,23,24,20,21,6,10,11,8,7,4,5,9,2,31])). % 117.40/117.42 cnf(3467,plain, % 117.40/117.42 (P1(f2(a7,a7))), % 117.40/117.42 inference(scs_inference,[],[3400,3320,3243,15,17,22,23,24,20,21,6,10,11,8,7,4,5,9,2,31,32])). % 117.40/117.42 cnf(3469,plain, % 117.40/117.42 (E(f2(a7,a6),f5(f4(a7,a7),a7))), % 117.40/117.42 inference(scs_inference,[],[3400,3402,3320,3243,2222,15,17,22,23,24,20,21,6,10,11,8,7,4,5,9,2,31,32,3])). % 117.40/117.42 cnf(3470,plain, % 117.40/117.42 (~P2(a7,f2(a7,a6))), % 117.40/117.42 inference(scs_inference,[],[19,3400,3402,3320,3243,2222,15,17,22,23,24,20,21,6,10,11,8,7,4,5,9,2,31,32,3,14])). % 117.40/117.42 cnf(3471,plain, % 117.40/117.42 (~P2(f2(a7,a6),a7)), % 117.40/117.42 inference(scs_inference,[],[19,3400,3402,3320,3243,2222,15,17,22,23,24,20,21,6,10,11,8,7,4,5,9,2,31,32,3,14,13])). % 117.40/117.42 cnf(3476,plain, % 117.40/117.42 (P2(a1,a1)), % 117.40/117.42 inference(scs_inference,[],[19,3400,3402,3320,3243,3316,3330,3170,3200,3379,16,2222,15,17,22,23,24,20,21,6,10,11,8,7,4,5,9,2,31,32,3,14,13,27,28,33])). % 117.40/117.42 cnf(3478,plain, % 117.40/117.42 (E(a1,f5(a1,a1))), % 117.40/117.42 inference(scs_inference,[],[19,3400,3402,3320,3243,3316,3330,3170,3200,3379,16,2222,15,17,22,23,24,20,21,6,10,11,8,7,4,5,9,2,31,32,3,14,13,27,28,33,42])). % 117.40/117.42 cnf(3480,plain, % 117.40/117.42 (E(a1,f4(a1,f5(a1,a1)))), % 117.40/117.42 inference(scs_inference,[],[19,3400,3402,3320,3243,3316,3330,3170,3200,3379,16,2222,15,17,22,23,24,20,21,6,10,11,8,7,4,5,9,2,31,32,3,14,13,27,28,33,42,68])). % 117.40/117.42 cnf(3481,plain, % 117.40/117.42 (P1(f5(a1,a1))), % 117.40/117.42 inference(scs_inference,[],[19,3400,3402,3320,3243,3316,3330,3170,3200,3379,16,2222,15,17,22,23,24,20,21,6,10,11,8,7,4,5,9,2,31,32,3,14,13,27,28,33,42,68,77])). % 117.40/117.42 cnf(3482,plain, % 117.40/117.42 (E(f4(a1,f5(a1,a1)),a1)), % 117.40/117.42 inference(scs_inference,[],[19,3400,3402,3320,3243,3316,3330,3170,3200,3379,16,2222,15,17,22,23,24,20,21,6,10,11,8,7,4,5,9,2,31,32,3,14,13,27,28,33,42,68,77,66])). % 117.40/117.42 cnf(3483,plain, % 117.40/117.42 (E(f2(f4(a7,a7),a6),f4(a7,a7))), % 117.40/117.42 inference(scs_inference,[],[19,3400,3402,3320,3243,3316,3330,3170,3200,3379,16,2222,15,17,22,23,24,20,21,6,10,11,8,7,4,5,9,2,31,32,3,14,13,27,28,33,42,68,77,66,25])). % 117.40/117.42 cnf(3485,plain, % 117.40/117.42 (P2(f5(f4(a7,a7),a7),f4(a7,a7))), % 117.40/117.42 inference(scs_inference,[],[19,3400,3402,3320,3243,3316,3330,3170,3200,3379,16,2222,15,17,22,23,24,20,21,6,10,11,8,7,4,5,9,2,31,32,3,14,13,27,28,33,42,68,77,66,25,395])). % 117.40/117.42 cnf(3487,plain, % 117.40/117.42 (P1(f5(f4(f5(a6,a6),f5(a6,a6)),f5(a6,a6)))), % 117.40/117.42 inference(scs_inference,[],[19,3400,3402,3320,3243,3316,3330,3382,3392,3170,3200,3284,3379,16,2222,15,17,22,23,24,20,21,6,10,11,8,7,4,5,9,2,31,32,3,14,13,27,28,33,42,68,77,66,25,395,48])). % 117.40/117.42 cnf(3498,plain, % 117.40/117.42 (P2(a7,f4(a7,a7))), % 117.40/117.42 inference(scs_inference,[],[3465,61])). % 117.40/117.42 cnf(3499,plain, % 117.40/117.42 (P2(x34991,f4(a7,a7))+~E(a7,x34991)), % 117.40/117.42 inference(scs_inference,[],[3465,395])). % 117.40/117.42 cnf(3500,plain, % 117.40/117.42 (~E(f4(a7,a7),x35001)+P2(f5(f4(a7,a7),a7),x35001)), % 117.40/117.42 inference(scs_inference,[],[3465,2258])). % 117.40/117.42 cnf(3502,plain, % 117.40/117.42 (P1(f5(f5(a1,f2(a1,a1)),a1))), % 117.40/117.42 inference(scs_inference,[],[3476,3209])). % 117.40/117.42 cnf(3503,plain, % 117.40/117.42 (E(a6,f5(f4(a6,a6),a6))), % 117.40/117.42 inference(scs_inference,[],[3476,3283])). % 117.40/117.42 cnf(3507,plain, % 117.40/117.42 (E(f2(f2(a7,a7),a6),f2(a7,a7))), % 117.40/117.42 inference(scs_inference,[],[3467,25])). % 117.40/117.42 cnf(3509,plain, % 117.40/117.42 (E(f2(a6,f4(a7,a7)),f4(a7,a7))), % 117.40/117.42 inference(scs_inference,[],[3465,3467,25,23])). % 117.40/117.42 cnf(3513,plain, % 117.40/117.42 (E(f2(a1,f4(a7,a7)),a1)), % 117.40/117.42 inference(scs_inference,[],[3465,3467,25,23,22,20])). % 117.40/117.42 cnf(3515,plain, % 117.40/117.42 (E(f2(f4(a7,a7),a1),a1)), % 117.40/117.42 inference(scs_inference,[],[3465,3467,25,23,22,20,21])). % 117.40/117.42 cnf(3517,plain, % 117.40/117.42 (E(f4(f4(a7,a7),a1),f4(a7,a7))), % 117.40/117.42 inference(scs_inference,[],[3465,3467,25,23,22,20,21,24])). % 117.40/117.42 cnf(3520,plain, % 117.40/117.42 (E(f5(f4(a1,a1),x35201),f5(a1,x35201))), % 117.40/117.42 inference(scs_inference,[],[3465,3467,3446,25,23,22,20,21,24,6,10])). % 117.40/117.42 cnf(3522,plain, % 117.40/117.42 (E(f5(x35221,f4(a1,a1)),f5(x35221,a1))), % 117.40/117.42 inference(scs_inference,[],[3465,3467,3446,25,23,22,20,21,24,6,10,8,11])). % 117.40/117.42 cnf(3523,plain, % 117.40/117.42 (E(f4(x35231,f4(a1,a1)),f4(x35231,a1))), % 117.40/117.42 inference(scs_inference,[],[3465,3467,3446,25,23,22,20,21,24,6,10,8,11,7])). % 117.40/117.42 cnf(3524,plain, % 117.40/117.42 (E(f2(f4(a1,a1),x35241),f2(a1,x35241))), % 117.40/117.42 inference(scs_inference,[],[3465,3467,3446,25,23,22,20,21,24,6,10,8,11,7,4])). % 117.40/117.42 cnf(3527,plain, % 117.40/117.42 (~E(a1,f2(f2(a6,a6),f2(a6,a6)))), % 117.40/117.42 inference(scs_inference,[],[3465,3467,3446,3432,25,23,22,20,21,24,6,10,8,11,7,4,9,5,2])). % 117.40/117.42 cnf(3528,plain, % 117.40/117.42 (P1(f4(f4(a7,a7),f4(a7,a7)))), % 117.40/117.42 inference(scs_inference,[],[3465,3467,3446,3432,25,23,22,20,21,24,6,10,8,11,7,4,9,5,2,31])). % 117.40/117.42 cnf(3530,plain, % 117.40/117.42 (P1(f2(f4(a7,a7),f4(a7,a7)))), % 117.40/117.42 inference(scs_inference,[],[3465,3467,3446,3432,25,23,22,20,21,24,6,10,8,11,7,4,9,5,2,31,32])). % 117.40/117.42 cnf(3532,plain, % 117.40/117.42 (~E(a6,f2(a1,a6))), % 117.40/117.42 inference(scs_inference,[],[3465,3467,3446,3216,3432,3222,25,23,22,20,21,24,6,10,8,11,7,4,9,5,2,31,32,3])). % 117.40/117.42 cnf(3537,plain, % 117.40/117.42 (E(f4(a1,f3(a1,a1)),a1)), % 117.40/117.42 inference(scs_inference,[],[3476,3465,3467,3446,3216,3485,3432,1037,2223,1019,3222,15,25,23,22,20,21,24,6,10,8,11,7,4,9,5,2,31,32,3,13,14,48,41])). % 117.40/117.42 cnf(3539,plain, % 117.40/117.42 (P1(f3(a1,a1))), % 117.40/117.42 inference(scs_inference,[],[3476,3465,3467,3446,3216,3485,3432,1037,2223,1019,3222,15,25,23,22,20,21,24,6,10,8,11,7,4,9,5,2,31,32,3,13,14,48,41,35])). % 117.40/117.42 cnf(3544,plain, % 117.40/117.42 (~E(f4(a7,f4(a7,a7)),f4(a7,a7))), % 117.40/117.42 inference(scs_inference,[],[3476,3465,3498,3467,3446,3216,3485,3307,3432,1037,2223,2224,1019,3282,3222,3245,16,15,17,25,23,22,20,21,24,6,10,8,11,7,4,9,5,2,31,32,3,13,14,48,41,35,40,42])). % 117.40/117.42 cnf(3553,plain, % 117.40/117.42 (P1(f2(a7,a6))), % 117.40/117.42 inference(scs_inference,[],[3476,3465,3498,3467,3446,3216,3485,3307,3421,3469,3432,1037,2223,2224,1019,3282,3222,3245,16,15,17,25,23,22,20,21,24,6,10,8,11,7,4,9,5,2,31,32,3,13,14,48,41,35,40,42,1073,26,27,53,34])). % 117.40/117.42 cnf(3555,plain, % 117.40/117.42 (~E(f4(a7,f4(a7,a7)),a7)), % 117.40/117.42 inference(scs_inference,[],[19,3476,3465,3498,3467,3446,3216,3485,3307,3421,3469,3432,1037,2223,2224,1019,3282,3222,3245,16,15,17,25,23,22,20,21,24,6,10,8,11,7,4,9,5,2,31,32,3,13,14,48,41,35,40,42,1073,26,27,53,34,33])). % 117.40/117.42 cnf(3557,plain, % 117.40/117.42 (E(f4(a7,a7),f5(f4(f4(a7,a7),f4(a7,a7)),f4(a7,a7)))+~P2(f4(a7,a7),f4(f4(a7,a7),f4(a7,a7)))), % 117.40/117.42 inference(scs_inference,[],[19,3476,3465,3498,3467,3446,3216,3485,3307,3421,3469,3432,1037,2223,2224,1019,3282,3222,3245,16,15,17,25,23,22,20,21,24,6,10,8,11,7,4,9,5,2,31,32,3,13,14,48,41,35,40,42,1073,26,27,53,34,33,54])). % 117.40/117.42 cnf(3562,plain, % 117.40/117.43 (E(f2(f5(a1,a1),a6),f5(a1,a1))), % 117.40/117.43 inference(scs_inference,[],[3481,3523,1073,25])). % 117.40/117.43 cnf(3564,plain, % 117.40/117.43 (E(f2(a6,f5(a1,a1)),f5(a1,a1))), % 117.40/117.43 inference(scs_inference,[],[3481,3523,1073,25,23])). % 117.40/117.43 cnf(3566,plain, % 117.40/117.43 (E(f2(a1,f5(a1,a1)),a1)), % 117.40/117.43 inference(scs_inference,[],[3481,3523,1073,25,23,20])). % 117.40/117.43 cnf(3568,plain, % 117.40/117.43 (E(f4(f5(a1,a1),a1),f5(a1,a1))), % 117.40/117.43 inference(scs_inference,[],[3481,3523,1073,25,23,20,24])). % 117.40/117.43 cnf(3570,plain, % 117.40/117.43 (E(f2(f5(a1,a1),a1),a1)), % 117.40/117.43 inference(scs_inference,[],[3481,3523,1073,25,23,20,24,21])). % 117.40/117.43 cnf(3572,plain, % 117.40/117.43 (E(f4(a1,f5(a1,a1)),f5(a1,a1))), % 117.40/117.43 inference(scs_inference,[],[3481,3523,1073,25,23,20,24,21,22])). % 117.40/117.43 cnf(3574,plain, % 117.40/117.43 (E(f5(x35741,a1),f5(x35741,f5(a1,a1)))), % 117.40/117.43 inference(scs_inference,[],[3481,3478,3523,1073,25,23,20,24,21,22,11])). % 117.40/117.43 cnf(3575,plain, % 117.40/117.43 (E(f3(a1,x35751),f3(f5(a1,a1),x35751))), % 117.40/117.43 inference(scs_inference,[],[3481,3478,3523,1073,25,23,20,24,21,22,11,8])). % 117.40/117.43 cnf(3576,plain, % 117.40/117.43 (E(f4(a1,x35761),f4(f5(a1,a1),x35761))), % 117.40/117.43 inference(scs_inference,[],[3481,3478,3523,1073,25,23,20,24,21,22,11,8,6])). % 117.40/117.43 cnf(3578,plain, % 117.40/117.43 (E(f4(x35781,a1),f4(x35781,f5(a1,a1)))), % 117.40/117.43 inference(scs_inference,[],[3481,3478,3523,1073,25,23,20,24,21,22,11,8,6,10,7])). % 117.40/117.43 cnf(3579,plain, % 117.40/117.43 (E(f2(a1,x35791),f2(f5(a1,a1),x35791))), % 117.40/117.43 inference(scs_inference,[],[3481,3478,3523,1073,25,23,20,24,21,22,11,8,6,10,7,4])). % 117.40/117.43 cnf(3580,plain, % 117.40/117.43 (E(f3(x35801,a1),f3(x35801,f5(a1,a1)))), % 117.40/117.43 inference(scs_inference,[],[3481,3478,3523,1073,25,23,20,24,21,22,11,8,6,10,7,4,9])). % 117.40/117.43 cnf(3581,plain, % 117.40/117.43 (E(f2(x35811,a1),f2(x35811,f5(a1,a1)))), % 117.40/117.43 inference(scs_inference,[],[3481,3478,3523,1073,25,23,20,24,21,22,11,8,6,10,7,4,9,5])). % 117.40/117.43 cnf(3583,plain, % 117.40/117.43 (P1(f2(f5(a1,a1),f5(a1,a1)))), % 117.40/117.43 inference(scs_inference,[],[3481,3478,3532,3523,1073,25,23,20,24,21,22,11,8,6,10,7,4,9,5,2,32])). % 117.40/117.43 cnf(3585,plain, % 117.40/117.43 (P1(f4(f5(a1,a1),f5(a1,a1)))), % 117.40/117.43 inference(scs_inference,[],[3481,3478,3532,3523,1073,25,23,20,24,21,22,11,8,6,10,7,4,9,5,2,32,31])). % 117.40/117.43 cnf(3587,plain, % 117.40/117.43 (~E(f5(a1,a1),f2(a6,a6))), % 117.40/117.43 inference(scs_inference,[],[3481,3425,3478,3532,3523,1073,25,23,20,24,21,22,11,8,6,10,7,4,9,5,2,32,31,3])). % 117.40/117.43 cnf(3588,plain, % 117.40/117.43 (~P2(f2(a6,a7),a7)), % 117.40/117.43 inference(scs_inference,[],[19,3481,3425,3478,3532,3448,3523,1073,25,23,20,24,21,22,11,8,6,10,7,4,9,5,2,32,31,3,13])). % 117.40/117.43 cnf(3589,plain, % 117.40/117.43 (~P2(a7,f2(a6,a7))), % 117.40/117.43 inference(scs_inference,[],[19,3481,3425,3478,3532,3448,3523,1073,25,23,20,24,21,22,11,8,6,10,7,4,9,5,2,32,31,3,13,14])). % 117.40/117.43 cnf(3595,plain, % 117.40/117.43 (P1(f5(a1,f2(a1,a6)))), % 117.40/117.43 inference(scs_inference,[],[19,3481,3425,3478,3532,3448,3523,3372,3282,3379,3245,525,16,1073,25,23,20,24,21,22,11,8,6,10,7,4,9,5,2,32,31,3,13,14,36,40,12])). % 117.40/117.43 cnf(3599,plain, % 117.40/117.43 (P2(f5(a1,a1),f4(f5(a1,a1),f5(a1,a1)))), % 117.40/117.43 inference(scs_inference,[],[19,3481,3425,3478,3532,3448,3523,3372,3282,3379,3245,525,16,1073,25,23,20,24,21,22,11,8,6,10,7,4,9,5,2,32,31,3,13,14,36,40,12,26,47])). % 117.40/117.43 cnf(3603,plain, % 117.40/117.43 (E(f5(a6,a6),f5(f4(f5(a6,a6),f5(a6,a6)),f5(a6,a6)))), % 117.40/117.43 inference(scs_inference,[],[19,3481,3425,3478,3532,3448,3523,3372,3382,3392,3282,3284,3379,3245,525,16,1073,25,23,20,24,21,22,11,8,6,10,7,4,9,5,2,32,31,3,13,14,36,40,12,26,47,37,54])). % 117.40/117.43 cnf(3607,plain, % 117.40/117.43 (E(f2(f2(a7,a6),a6),f2(a7,a6))), % 117.40/117.43 inference(scs_inference,[],[3553,25])). % 117.40/117.43 cnf(3609,plain, % 117.40/117.43 (E(f2(a6,f2(a7,a6)),f2(a7,a6))), % 117.40/117.43 inference(scs_inference,[],[3553,25,23])). % 117.40/117.43 cnf(3611,plain, % 117.40/117.43 (E(f2(a1,f2(a7,a6)),a1)), % 117.40/117.43 inference(scs_inference,[],[3553,25,23,20])). % 117.40/117.43 cnf(3613,plain, % 117.40/117.43 (E(f4(a1,f2(a7,a6)),f2(a7,a6))), % 117.40/117.43 inference(scs_inference,[],[3553,25,23,20,22])). % 117.40/117.43 cnf(3615,plain, % 117.40/117.43 (E(f4(f2(a7,a6),a1),f2(a7,a6))), % 117.40/117.43 inference(scs_inference,[],[3553,25,23,20,22,24])). % 117.40/117.43 cnf(3617,plain, % 117.40/117.43 (E(f2(f2(a7,a6),a1),a1)), % 117.40/117.43 inference(scs_inference,[],[3553,25,23,20,22,24,21])). % 117.40/117.43 cnf(3621,plain, % 117.40/117.43 (E(f4(x36211,f4(a7,a1)),f4(x36211,a7))), % 117.40/117.43 inference(scs_inference,[],[3553,3450,25,23,20,22,24,21,8,10,7])). % 117.40/117.43 cnf(3622,plain, % 117.40/117.43 (E(f4(f4(a7,a1),x36221),f4(a7,x36221))), % 117.40/117.43 inference(scs_inference,[],[3553,3450,25,23,20,22,24,21,8,10,7,6])). % 117.40/117.43 cnf(3624,plain, % 117.40/117.43 (E(f2(f4(a7,a1),x36241),f2(a7,x36241))), % 117.40/117.43 inference(scs_inference,[],[3553,3450,25,23,20,22,24,21,8,10,7,6,11,4])). % 117.40/117.43 cnf(3626,plain, % 117.40/117.43 (E(f2(x36261,f4(a7,a1)),f2(x36261,a7))), % 117.40/117.43 inference(scs_inference,[],[3553,3450,25,23,20,22,24,21,8,10,7,6,11,4,9,5])). % 117.40/117.43 cnf(3627,plain, % 117.40/117.43 (~E(f2(a6,a6),f5(a1,a1))), % 117.40/117.43 inference(scs_inference,[],[3587,3553,3450,25,23,20,22,24,21,8,10,7,6,11,4,9,5,2])). % 117.40/117.43 cnf(3628,plain, % 117.40/117.43 (P1(f4(f2(a7,a6),f2(a7,a6)))), % 117.40/117.43 inference(scs_inference,[],[3587,3553,3450,25,23,20,22,24,21,8,10,7,6,11,4,9,5,2,31])). % 117.40/117.43 cnf(3630,plain, % 117.40/117.43 (P1(f2(f2(a7,a6),f2(a7,a6)))), % 117.40/117.43 inference(scs_inference,[],[3587,3553,3450,25,23,20,22,24,21,8,10,7,6,11,4,9,5,2,31,32])). % 117.40/117.43 cnf(3632,plain, % 117.40/117.43 (~E(f5(a1,f5(a1,a1)),f2(a6,a6))), % 117.40/117.43 inference(scs_inference,[],[3587,3553,3450,3574,25,23,20,22,24,21,8,10,7,6,11,4,9,5,2,31,32,3])). % 117.40/117.43 cnf(3634,plain, % 117.40/117.43 (~P2(f4(a7,a1),a7)), % 117.40/117.43 inference(scs_inference,[],[19,3587,3553,3450,3574,25,23,20,22,24,21,8,10,7,6,11,4,9,5,2,31,32,3,13])). % 117.40/117.43 cnf(3635,plain, % 117.40/117.43 (~P2(a7,f4(a7,a1))), % 117.40/117.43 inference(scs_inference,[],[19,3587,3553,3450,3574,25,23,20,22,24,21,8,10,7,6,11,4,9,5,2,31,32,3,13,14])). % 117.40/117.43 cnf(3638,plain, % 117.40/117.43 (~P1(f4(a7,a1))), % 117.40/117.43 inference(scs_inference,[],[19,3587,3553,3450,3574,3498,3465,15,17,25,23,20,22,24,21,8,10,7,6,11,4,9,5,2,31,32,3,13,14,41,47])). % 117.40/117.43 cnf(3646,plain, % 117.40/117.43 (~E(f4(a7,a1),f5(f2(a1,a1),f2(a1,a1)))), % 117.40/117.43 inference(scs_inference,[],[19,3587,3553,3450,3572,3574,2223,3476,2224,3498,3481,3465,3379,802,809,15,17,25,23,20,22,24,21,8,10,7,6,11,4,9,5,2,31,32,3,13,14,41,47,37,36,40,34])). % 117.40/117.43 cnf(3650,plain, % 117.40/117.43 (~E(f2(a7,a6),f4(a7,a1))), % 117.40/117.43 inference(scs_inference,[],[19,3587,3553,3450,3572,3574,2223,3476,2224,3498,3481,3465,3379,802,809,15,17,25,23,20,22,24,21,8,10,7,6,11,4,9,5,2,31,32,3,13,14,41,47,37,36,40,34,42,12])). % 117.40/117.43 cnf(3653,plain, % 117.40/117.43 (E(f5(a1,a1),f5(f4(f5(a1,a1),f5(a1,a1)),f5(a1,a1)))), % 117.40/117.43 inference(scs_inference,[],[19,3587,3553,3450,3572,3585,3599,3574,3268,2223,3476,2224,3498,3481,3465,3379,802,809,15,17,25,23,20,22,24,21,8,10,7,6,11,4,9,5,2,31,32,3,13,14,41,47,37,36,40,34,42,12,26,54])). % 117.40/117.43 cnf(3657,plain, % 117.40/117.43 (E(f2(f3(a1,a1),a6),f3(a1,a1))), % 117.40/117.43 inference(scs_inference,[],[3539,25])). % 117.40/117.43 cnf(3661,plain, % 117.40/117.43 (E(f2(a1,f3(a1,a1)),a1)), % 117.40/117.43 inference(scs_inference,[],[3539,25,23,20])). % 117.40/117.43 cnf(3663,plain, % 117.40/117.43 (E(f4(a1,f3(a1,a1)),f3(a1,a1))), % 117.40/117.43 inference(scs_inference,[],[3539,25,23,20,22])). % 117.40/117.43 cnf(3667,plain, % 117.40/117.43 (E(f2(f3(a1,a1),a1),a1)), % 117.40/117.43 inference(scs_inference,[],[3539,25,23,20,22,24,21])). % 117.40/117.43 cnf(3677,plain, % 117.40/117.43 (~E(f4(a7,a1),f2(a7,a6))), % 117.40/117.43 inference(scs_inference,[],[3650,3539,3482,3537,25,23,20,22,24,21,8,7,11,10,6,4,9,5,2])). % 117.40/117.43 cnf(3678,plain, % 117.40/117.43 (~E(f3(a1,a1),f4(a7,a1))), % 117.40/117.43 inference(scs_inference,[],[3650,3539,3638,3482,3537,25,23,20,22,24,21,8,7,11,10,6,4,9,5,2,12])). % 117.40/117.43 cnf(3679,plain, % 117.40/117.43 (P1(f2(f3(a1,a1),f3(a1,a1)))), % 117.40/117.43 inference(scs_inference,[],[3650,3539,3638,3482,3537,25,23,20,22,24,21,8,7,11,10,6,4,9,5,2,12,32])). % 117.40/117.43 cnf(3681,plain, % 117.40/117.43 (P1(f4(f3(a1,a1),f3(a1,a1)))), % 117.40/117.43 inference(scs_inference,[],[3650,3539,3638,3482,3537,25,23,20,22,24,21,8,7,11,10,6,4,9,5,2,12,32,31])). % 117.40/117.43 cnf(3685,plain, % 117.40/117.43 (~P2(f2(a6,a7),f2(a7,a6))), % 117.40/117.43 inference(scs_inference,[],[3650,3539,3638,3470,3152,3482,3579,3537,3448,25,23,20,22,24,21,8,7,11,10,6,4,9,5,2,12,32,31,3,13])). % 117.40/117.43 cnf(3694,plain, % 117.40/117.43 (P2(f4(a7,a7),f4(f4(a7,a7),f4(a7,a7)))), % 117.40/117.43 inference(scs_inference,[],[3650,3539,3638,3470,3152,3314,3482,3528,3579,3537,937,2023,3316,3330,3448,3465,992,972,15,25,23,20,22,24,21,8,7,11,10,6,4,9,5,2,12,32,31,3,13,14,26,35,41,47])). % 117.40/117.43 cnf(3707,plain, % 117.40/117.43 (E(f3(a1,a1),f5(a1,a1))), % 117.40/117.43 inference(scs_inference,[],[3627,3650,3539,3638,3470,3152,3314,3520,3482,3528,3579,3537,937,2023,3294,3316,3291,3330,3448,3476,3481,3465,3379,3245,992,972,15,25,23,20,22,24,21,8,7,11,10,6,4,9,5,2,12,32,31,3,13,14,26,35,41,47,37,36,40,27,34,42])). % 117.40/117.43 cnf(3711,plain, % 117.40/117.43 (E(f4(a7,a7),f5(f4(f4(a7,a7),f4(a7,a7)),f4(a7,a7)))), % 117.40/117.43 inference(scs_inference,[],[3694,3557])). % 117.40/117.43 cnf(3730,plain, % 117.40/117.43 (~E(f4(a7,a1),f3(a1,a1))), % 117.40/117.43 inference(scs_inference,[],[3707,3678,3285,3467,23,20,24,22,21,8,11,6,7,9,4,10,5,2])). % 117.40/117.43 cnf(3731,plain, % 117.40/117.43 (P1(f4(f2(a7,a7),f2(a7,a7)))), % 117.40/117.43 inference(scs_inference,[],[3707,3678,3285,3467,23,20,24,22,21,8,11,6,7,9,4,10,5,2,31])). % 117.40/117.43 cnf(3733,plain, % 117.40/117.43 (P1(f2(f2(a7,a7),f2(a7,a7)))), % 117.40/117.43 inference(scs_inference,[],[3707,3678,3285,3467,23,20,24,22,21,8,11,6,7,9,4,10,5,2,31,32])). % 117.40/117.43 cnf(3735,plain, % 117.40/117.43 (~E(f2(f5(a6,a6),f5(a6,a6)),f4(a7,a1))), % 117.40/117.43 inference(scs_inference,[],[3707,3678,3285,3467,3638,23,20,24,22,21,8,11,6,7,9,4,10,5,2,31,32,12])). % 117.40/117.43 cnf(3736,plain, % 117.40/117.43 (~E(f5(a1,a1),f4(a7,a1))), % 117.40/117.43 inference(scs_inference,[],[3707,3678,3285,3467,3638,23,20,24,22,21,8,11,6,7,9,4,10,5,2,31,32,12,3])). % 117.40/117.43 cnf(3738,plain, % 117.40/117.43 (E(f2(f2(a6,a6),x37381),f2(a6,x37381))), % 117.40/117.43 inference(rename_variables,[],[3313])). % 117.40/117.43 cnf(3739,plain, % 117.40/117.43 (~P2(f2(f2(a6,a6),a7),f2(a7,a6))), % 117.40/117.43 inference(scs_inference,[],[3707,3678,3685,3589,3313,3738,3285,3467,3638,23,20,24,22,21,8,11,6,7,9,4,10,5,2,31,32,12,3,14,13])). % 117.40/117.43 cnf(3745,plain, % 117.40/117.43 (P2(f2(a7,a7),f4(f2(a7,a7),f2(a7,a7)))), % 117.40/117.43 inference(scs_inference,[],[3707,3678,3685,3589,3313,3738,3285,3694,3467,3528,3638,3170,3465,16,23,20,24,22,21,8,11,6,7,9,4,10,5,2,31,32,12,3,14,13,35,27,47])). % 117.40/117.43 cnf(3761,plain, % 117.40/117.43 (E(f4(a1,a7),a7)), % 117.40/117.43 inference(scs_inference,[],[3324,3711,17,3500,20,22])). % 117.40/117.43 cnf(3766,plain, % 117.40/117.43 (E(f4(x37661,a1),f4(x37661,f4(a1,f5(a1,a1))))), % 117.40/117.43 inference(scs_inference,[],[3324,3480,3711,17,3500,20,22,21,11,7])). % 117.40/117.43 cnf(3770,plain, % 117.40/117.43 (E(f4(a1,x37701),f4(f4(a1,f5(a1,a1)),x37701))), % 117.40/117.43 inference(scs_inference,[],[3324,3480,3297,3711,17,3500,20,22,21,11,7,8,4,10,6])). % 117.40/117.43 cnf(3773,plain, % 117.40/117.43 (~E(f4(a7,a1),f5(a1,a1))), % 117.40/117.43 inference(scs_inference,[],[3736,3324,3480,3297,3711,17,3500,20,22,21,11,7,8,4,10,6,9,5,2])). % 117.40/117.43 cnf(3774,plain, % 117.40/117.43 (~E(f3(f2(a1,a1),f2(a1,a1)),f4(a7,a1))), % 117.40/117.43 inference(scs_inference,[],[3736,3324,3480,3297,3711,3638,17,3500,20,22,21,11,7,8,4,10,6,9,5,2,12])). % 117.40/117.43 cnf(3775,plain, % 117.40/117.43 (~E(f4(a6,a6),f2(f4(a6,a6),a1))), % 117.40/117.43 inference(scs_inference,[],[3736,3295,3324,3480,3297,3711,3272,3638,17,3500,20,22,21,11,7,8,4,10,6,9,5,2,12,3])). % 117.40/117.43 cnf(3778,plain, % 117.40/117.43 (~P2(f2(a7,a6),f2(a7,a6))), % 117.40/117.43 inference(scs_inference,[],[3736,3588,3471,3295,3377,3324,3480,3297,3711,3272,3402,3638,17,3500,20,22,21,11,7,8,4,10,6,9,5,2,12,3,13,14])). % 117.40/117.43 cnf(3779,plain, % 117.40/117.43 (P1(f5(f4(f2(a7,a7),f2(a7,a7)),f2(a7,a7)))), % 117.40/117.43 inference(scs_inference,[],[3736,3588,3471,3295,3377,3324,3745,3731,3480,3297,3711,3272,3402,3638,3467,17,3500,20,22,21,11,7,8,4,10,6,9,5,2,12,3,13,14,48])). % 117.40/117.43 cnf(3789,plain, % 117.40/117.43 (P2(f3(a1,a1),f4(f3(a1,a1),f3(a1,a1)))), % 117.40/117.43 inference(scs_inference,[],[3736,3588,3471,3295,3562,3377,3324,3745,3731,3681,3480,3297,3711,3272,3402,3638,3476,3467,3553,3539,15,17,3500,20,22,21,11,7,8,4,10,6,9,5,2,12,3,13,14,48,40,34,33,26,47])). % 117.40/117.43 cnf(3797,plain, % 117.40/117.43 (E(f5(x37971,f4(a1,a7)),f5(x37971,a7))), % 117.40/117.43 inference(scs_inference,[],[3761,3530,20,21,11])). % 117.40/117.43 cnf(3801,plain, % 117.40/117.43 (E(f4(x38011,f4(a1,a7)),f4(x38011,a7))), % 117.40/117.43 inference(scs_inference,[],[3761,3530,20,21,11,8,10,9,7])). % 117.40/117.43 cnf(3802,plain, % 117.40/117.43 (E(f2(f4(a1,a7),x38021),f2(a7,x38021))), % 117.40/117.43 inference(scs_inference,[],[3761,3530,20,21,11,8,10,9,7,4])). % 117.40/117.43 cnf(3803,plain, % 117.40/117.43 (E(f2(x38031,f4(a1,a7)),f2(x38031,a7))), % 117.40/117.43 inference(scs_inference,[],[3761,3530,20,21,11,8,10,9,7,4,5])). % 117.40/117.43 cnf(3804,plain, % 117.40/117.43 (E(f4(f4(a1,a7),x38041),f4(a7,x38041))), % 117.40/117.43 inference(scs_inference,[],[3761,3530,20,21,11,8,10,9,7,4,5,6])). % 117.40/117.43 cnf(3806,plain, % 117.40/117.43 (~E(f2(f4(a7,a7),f4(a7,a7)),f4(a7,a1))), % 117.40/117.43 inference(scs_inference,[],[3761,3544,3530,3638,20,21,11,8,10,9,7,4,5,6,2,12])). % 117.40/117.43 cnf(3807,plain, % 117.40/117.43 (~E(f4(a7,f5(a1,a1)),f5(a1,a1))), % 117.40/117.43 inference(scs_inference,[],[3773,3761,3544,3530,3578,3638,20,21,11,8,10,9,7,4,5,6,2,12,3])). % 117.40/117.43 cnf(3809,plain, % 117.40/117.43 (~P2(a7,f4(a1,a7))), % 117.40/117.43 inference(scs_inference,[],[19,3773,3761,3544,3530,3578,3638,20,21,11,8,10,9,7,4,5,6,2,12,3,14])). % 117.40/117.43 cnf(3810,plain, % 117.40/117.43 (~P2(f4(a1,a7),a7)), % 117.40/117.43 inference(scs_inference,[],[19,3773,3761,3544,3530,3578,3638,20,21,11,8,10,9,7,4,5,6,2,12,3,14,13])). % 117.40/117.43 cnf(3844,plain, % 117.40/117.43 (~E(f2(f5(a1,a1),f5(a1,a1)),f4(a7,a1))), % 117.40/117.43 inference(scs_inference,[],[3806,3583,3301,3638,20,21,11,10,8,5,7,9,6,4,2,12])). % 117.40/117.43 cnf(3847,plain, % 117.40/117.43 (~P2(f2(a7,a6),f2(f2(a7,a6),a6))), % 117.40/117.43 inference(scs_inference,[],[3778,3155,3806,3607,3583,3581,3301,3638,20,21,11,10,8,5,7,9,6,4,2,12,3,14])). % 117.40/117.43 cnf(3848,plain, % 117.40/117.43 (~P2(f2(f2(a7,a6),a6),f2(a7,a6))), % 117.40/117.43 inference(scs_inference,[],[3778,3155,3806,3607,3583,3581,3301,3638,20,21,11,10,8,5,7,9,6,4,2,12,3,14,13])). % 117.40/117.43 cnf(3855,plain, % 117.40/117.43 (E(f2(a7,a7),f5(f4(f2(a7,a7),f2(a7,a7)),f2(a7,a7)))), % 117.40/117.43 inference(scs_inference,[],[19,3778,3155,3806,3607,3564,3583,3789,3581,3301,3681,3745,3731,3638,3476,3467,3539,15,17,20,21,11,10,8,5,7,9,6,4,2,12,3,14,13,35,40,33,54])). % 117.40/117.43 cnf(3874,plain, % 117.40/117.43 (~E(f2(f2(a7,a7),f2(a7,a7)),f4(a7,a1))), % 117.40/117.43 inference(scs_inference,[],[3844,3733,3366,3638,20,21,11,8,7,10,6,5,9,4,2,12])). % 117.40/117.43 cnf(3882,plain, % 117.40/117.43 (~E(f4(f2(a7,a6),f2(a7,a6)),f2(a7,a6))), % 117.40/117.43 inference(scs_inference,[],[3730,3844,3848,3609,3458,3733,3847,3366,3766,3778,3638,3553,990,1001,15,20,21,11,8,7,10,6,5,9,4,2,12,3,14,13,40,33])). % 117.40/117.43 cnf(3905,plain, % 117.40/117.43 (~E(f2(f3(a1,a1),f3(a1,a1)),f4(a7,a1))), % 117.40/117.43 inference(scs_inference,[],[3874,3679,3368,3638,20,21,11,7,8,6,10,9,5,4,2,12])). % 117.40/117.43 cnf(3909,plain, % 117.40/117.43 (~P2(f2(a6,a7),f4(a1,a7))), % 117.40/117.43 inference(scs_inference,[],[3809,3874,3358,3415,3679,3368,3603,3448,3638,20,21,11,7,8,6,10,9,5,4,2,12,3,14,13])). % 117.40/117.43 cnf(3922,plain, % 117.40/117.43 (P2(f2(a7,a6),f4(f2(a7,a6),f2(a7,a6)))), % 117.40/117.43 inference(scs_inference,[],[3809,3874,3358,3568,3415,3679,3628,3527,3368,3603,2016,3585,3421,937,3599,3448,3476,3638,3467,3553,3481,802,15,20,21,11,7,8,6,10,9,5,4,2,12,3,14,13,35,37,36,40,48,28,47])). % 117.40/117.43 cnf(3939,plain, % 117.40/117.43 (~E(f5(f4(a6,a6),f2(a6,a6)),f4(a7,a1))), % 117.40/117.43 inference(scs_inference,[],[3905,3336,3404,3638,20,21,11,8,5,10,7,6,9,4,2,12])). % 117.40/117.43 cnf(3940,plain, % 117.40/117.43 (~E(f4(a6,f5(a1,a1)),f4(a6,a6))), % 117.40/117.43 inference(scs_inference,[],[3242,3905,3336,3404,3578,3638,20,21,11,8,5,10,7,6,9,4,2,12,3])). % 117.40/117.43 cnf(3942,plain, % 117.40/117.43 (~P2(f4(f2(a7,a6),a1),f2(f2(a7,a6),a6))), % 117.40/117.43 inference(scs_inference,[],[3242,3905,3615,3336,3404,3847,3578,3638,20,21,11,8,5,10,7,6,9,4,2,12,3,13])). % 117.40/117.43 cnf(3944,plain, % 117.40/117.43 (P1(f5(f4(f2(a7,a6),f2(a7,a6)),f2(a7,a6)))), % 117.40/117.43 inference(scs_inference,[],[3242,3905,3615,3739,3336,3922,3404,3628,3847,3578,3638,3553,20,21,11,8,5,10,7,6,9,4,2,12,3,13,14,48])). % 117.40/117.43 cnf(3948,plain, % 117.40/117.43 (~E(f4(a1,a1),f4(f2(a6,a6),a1))), % 117.40/117.43 inference(scs_inference,[],[3242,3905,3615,3739,3336,3922,3404,3425,3628,3847,3578,3638,3553,3379,15,20,21,11,8,5,10,7,6,9,4,2,12,3,13,14,48,35,37])). % 117.40/117.43 cnf(3953,plain, % 117.40/117.43 (P2(f2(a6,a6),f4(f2(a6,a6),f2(a6,a6)))), % 117.40/117.43 inference(scs_inference,[],[3242,3905,3615,3739,3797,3336,3423,3922,3404,3425,3628,3847,3578,3498,3638,3553,3465,3379,15,17,20,21,11,8,5,10,7,6,9,4,2,12,3,13,14,48,35,37,40,47])). % 117.40/117.43 cnf(3959,plain, % 117.40/117.43 (E(f2(a6,a6),f5(f4(f2(a6,a6),f2(a6,a6)),f2(a6,a6)))), % 117.40/117.43 inference(scs_inference,[],[3242,3905,3615,3739,3797,3336,3423,3922,3404,3425,3628,3847,3578,3392,3382,3498,3170,3638,3284,3553,3465,3379,16,15,17,20,21,11,8,5,10,7,6,9,4,2,12,3,13,14,48,35,37,40,47,28,34,54])). % 117.40/117.43 cnf(3976,plain, % 117.40/117.43 (~E(f2(f2(a7,a6),f2(a7,a6)),f4(a7,a1))), % 117.40/117.43 inference(scs_inference,[],[3939,3630,3408,3638,20,21,5,11,8,7,9,10,6,4,2,12])). % 117.40/117.43 cnf(3978,plain, % 117.40/117.43 (~P2(f2(a6,f4(a1,a7)),f4(a1,a7))), % 117.40/117.43 inference(scs_inference,[],[3909,3939,3299,3803,3630,3408,3338,3638,20,21,5,11,8,7,9,10,6,4,2,12,3,13])). % 117.40/117.43 cnf(3980,plain, % 117.40/117.43 (~P2(f2(a6,a7),f4(f2(a6,a1),a7))), % 117.40/117.43 inference(scs_inference,[],[3909,3939,3299,3456,3803,3630,3408,3338,3638,20,21,5,11,8,7,9,10,6,4,2,12,3,13,14])). % 117.40/117.43 cnf(4006,plain, % 117.40/117.43 (~E(f5(a1,f2(a1,a1)),f4(a7,a1))), % 117.40/117.43 inference(scs_inference,[],[3976,2919,3513,3638,20,21,8,11,5,9,7,6,10,4,2,12])). % 117.40/117.43 cnf(4007,plain, % 117.40/117.43 (~E(f4(f5(a1,a1),a6),f4(a6,a6))), % 117.40/117.43 inference(scs_inference,[],[3378,3976,3576,2919,3513,3638,20,21,8,11,5,9,7,6,10,4,2,12,3])). % 117.40/117.43 cnf(4010,plain, % 117.40/117.43 (~P2(f2(a6,a7),f4(a1,f2(a7,a6)))), % 117.40/117.43 inference(scs_inference,[],[3378,3976,3613,3576,2919,3513,3685,3471,3638,20,21,8,11,5,9,7,6,10,4,2,12,3,13,14])). % 117.40/117.43 cnf(4037,plain, % 117.40/117.43 (~P2(f4(a1,a7),f2(a7,a6))), % 117.40/117.43 inference(scs_inference,[],[3810,4006,3483,3801,3515,3381,3318,3711,3402,3638,20,21,5,11,8,7,9,6,10,4,2,12,3,13,14])). % 117.40/117.43 cnf(4038,plain, % 117.40/117.43 (P1(f3(f2(a1,f4(a1,a1)),f4(a1,a1)))), % 117.40/117.43 inference(scs_inference,[],[3810,4006,3483,3801,3515,3381,3318,995,3711,3402,3638,991,94,20,21,5,11,8,7,9,6,10,4,2,12,3,13,14,35])). % 117.40/117.43 cnf(4065,plain, % 117.40/117.43 (P1(f5(f4(f2(a6,a6),f2(a6,a6)),f2(a6,a6)))), % 117.40/117.43 inference(scs_inference,[],[3677,3882,3308,3524,3566,3487,3248,1018,3953,3766,3423,3638,3379,20,21,8,5,11,9,6,7,10,4,2,12,3,13,14,48])). % 117.40/117.43 cnf(4093,plain, % 117.40/117.43 (~P2(f4(a1,f4(a7,a1)),f2(a7,a6))), % 117.40/117.43 inference(scs_inference,[],[4037,3507,3774,3621,3570,3779,3855,3595,3638,20,21,5,11,8,7,9,6,10,4,2,12,3,13])). % 117.40/117.43 cnf(4095,plain, % 117.40/117.43 (~P2(f4(a1,a7),f2(a7,f4(a6,a1)))), % 117.40/117.43 inference(scs_inference,[],[4037,3507,3774,3376,3621,3570,3779,3855,3595,3638,20,21,5,11,8,7,9,6,10,4,2,12,3,13,14])). % 117.40/117.43 cnf(4099,plain, % 117.40/117.43 (P1(f3(f2(a1,f4(a1,a1)),f2(a1,a1)))), % 117.40/117.43 inference(scs_inference,[],[4037,3507,3774,3376,3621,3570,3779,3855,1000,801,3595,3638,1001,780,94,20,21,5,11,8,7,9,6,10,4,2,12,3,13,14,48,35])). % 117.40/117.43 cnf(4122,plain, % 117.40/117.43 (~E(f4(a7,a1),f2(f5(a6,a6),f5(a6,a6)))), % 117.40/117.43 inference(scs_inference,[],[3735,3661,971,20,21,8,11,5,7,6,9,10,4,2])). % 117.40/117.43 cnf(4157,plain, % 117.40/117.43 (~P2(f4(a7,a1),f2(a6,a7))), % 117.40/117.43 inference(scs_inference,[],[3634,3657,3632,3460,3575,3667,4065,3173,3448,3638,20,21,5,8,11,7,6,9,10,4,2,12,3,13,14])). % 117.40/117.43 cnf(4160,plain, % 117.40/117.43 (~E(f4(a1,a1),f4(a1,f2(a6,a6)))), % 117.40/117.43 inference(scs_inference,[],[3634,3657,3632,3460,3575,3667,4065,3173,3326,3425,3318,3448,3638,3379,3245,15,20,21,5,8,11,7,6,9,10,4,2,12,3,13,14,35,36])). % 117.40/117.43 cnf(4185,plain, % 117.40/117.43 (E(f2(f4(a1,a7),x41851),f2(a7,x41851))), % 117.40/117.43 inference(rename_variables,[],[3802])). % 117.40/117.43 cnf(4188,plain, % 117.40/117.43 (P1(f3(f5(f2(a1,a1),f2(a1,a6)),f2(a1,a1)))), % 117.40/117.43 inference(scs_inference,[],[3303,4093,3807,3940,3802,4185,3611,4038,912,786,3847,825,3638,802,20,21,11,7,5,8,6,9,10,4,2,12,3,13,14,35])). % 117.40/117.43 cnf(4211,plain, % 117.40/117.43 (~P2(f4(f4(a1,a7),a1),f2(a6,a7))), % 117.40/117.43 inference(scs_inference,[],[4157,3362,4007,3804,3617,4188,3603,3316,3638,20,21,5,11,8,7,6,10,9,4,2,12,3,13])). % 117.40/117.43 cnf(4215,plain, % 117.40/117.43 (P1(f5(f4(f4(a7,a7),f4(a7,a7)),f4(a7,a7)))), % 117.40/117.43 inference(scs_inference,[],[4157,3362,4007,3804,3626,3617,4188,3603,3316,3694,3528,3465,3638,20,21,5,11,8,7,6,10,9,4,2,12,3,13,14,48])). % 117.40/117.43 cnf(4234,plain, % 117.40/117.43 (~E(f4(a1,f2(a6,a6)),f4(a1,a1))), % 117.40/117.43 inference(scs_inference,[],[4160,3503,846,20,21,8,5,7,11,6,9,10,4,2])). % 117.40/117.43 cnf(4238,plain, % 117.40/117.43 (~P2(a7,f4(f4(a7,a1),a1))), % 117.40/117.43 inference(scs_inference,[],[3622,4122,4160,4215,3635,3503,3578,846,3638,20,21,8,5,7,11,6,9,10,4,2,12,3,14])). % 117.40/117.43 cnf(4263,plain, % 117.40/117.43 (~E(f5(f2(a1,a1),f2(a1,a1)),f4(a7,a1))), % 117.40/117.43 inference(scs_inference,[],[3646,993,823,20,21,8,7,5,11,6,10,9,4,2])). % 117.40/117.43 cnf(4270,plain, % 117.40/117.43 (P1(f3(f5(f4(a7,a7),a7),f4(a7,a7)))), % 117.40/117.43 inference(scs_inference,[],[3410,4211,3646,3959,4099,3107,993,3485,3313,823,2223,3465,3638,20,21,8,7,5,11,6,10,9,4,2,12,3,14,13,35])). % 117.40/117.43 cnf(4293,plain, % 117.40/117.43 (~E(f2(a1,f4(a1,a1)),f4(a7,a1))), % 117.40/117.43 inference(scs_inference,[],[4263,3948,4270,1263,2906,3421,3638,20,21,8,7,11,5,6,10,9,4,2,12,3])). % 117.40/117.43 cnf(4295,plain, % 117.40/117.43 (E(f2(f4(a7,a1),x42951),f2(a7,x42951))), % 117.40/117.43 inference(rename_variables,[],[3624])). % 117.40/117.43 cnf(4296,plain, % 117.40/117.43 (~P2(f2(f4(a7,a1),a6),f2(a7,a6))), % 117.40/117.43 inference(scs_inference,[],[4263,3624,4295,3948,4095,4270,1263,2906,3778,3421,3638,20,21,8,7,11,5,6,10,9,4,2,12,3,14,13])). % 117.40/117.43 cnf(4322,plain, % 117.40/117.43 (P1(f3(a6,f4(a6,a6)))), % 117.40/117.43 inference(scs_inference,[],[4293,3663,4296,4010,3580,3944,3106,3288,2928,3291,3282,3638,3245,16,20,21,8,7,5,11,10,6,9,4,2,12,3,14,13,35])). % 117.40/117.43 cnf(4342,plain, % 117.40/117.43 (~E(f3(a6,f4(a6,a6)),f4(a7,a1))), % 117.40/117.43 inference(scs_inference,[],[4322,3775,3297,2897,3638,20,21,8,7,5,9,6,11,10,4,2,12])). % 117.40/117.43 cnf(4343,plain, % 117.40/117.43 (~E(f2(a6,a6),f4(a1,a1))), % 117.40/117.43 inference(scs_inference,[],[4234,3406,4322,3775,3297,2897,3638,20,21,8,7,5,9,6,11,10,4,2,12,3])). % 117.40/117.43 cnf(4352,plain, % 117.40/117.43 (P1(f5(f4(f3(a1,a1),f3(a1,a1)),f3(a1,a1)))), % 117.40/117.43 inference(scs_inference,[],[4234,3406,4322,3775,3653,3133,2913,3297,2897,3789,3953,3681,3599,823,3170,3539,3638,16,15,20,21,8,7,5,9,6,11,10,4,2,12,3,14,13,26,27,35,48])). % 117.40/117.43 cnf(4364,plain, % 117.40/117.43 (E(f4(x43641,f2(a1,a1)),f4(x43641,a1))), % 117.40/117.43 inference(scs_inference,[],[2898,3585,20,21,7])). % 117.40/117.43 cnf(4372,plain, % 117.40/117.43 (~E(f4(a1,a1),f2(a6,a6))), % 117.40/117.43 inference(scs_inference,[],[4343,2898,3585,20,21,7,8,9,5,6,11,10,4,2])). % 117.40/117.43 cnf(4379,plain, % 117.40/117.43 (P1(f5(f2(a1,f4(a1,a1)),f2(a1,a1)))), % 117.40/117.43 inference(scs_inference,[],[4343,3509,3978,3980,4352,3377,3801,2917,2898,3711,3585,3638,796,94,20,21,7,8,9,5,6,11,10,4,2,12,3,14,13,48])). % 117.40/117.43 cnf(4408,plain, % 117.40/117.43 (~P2(a7,f4(f4(a7,a1),f2(a1,a1)))), % 117.40/117.43 inference(scs_inference,[],[4372,4342,4364,4238,4379,3770,3226,3537,2223,3638,20,21,7,8,9,5,6,10,11,4,2,12,3,14])). % 117.40/117.43 cnf(4409,plain, % 117.40/117.43 (E(f4(x44091,f2(a1,a1)),f4(x44091,a1))), % 117.40/117.43 inference(rename_variables,[],[4364])). % 117.40/117.43 cnf(4412,plain, % 117.40/117.43 (P1(f3(a7,f4(a7,a7)))), % 117.40/117.43 inference(scs_inference,[],[4372,4342,4364,4409,4238,4379,3942,3770,3226,3537,2223,3498,3465,3638,17,20,21,7,8,9,5,6,10,11,4,2,12,3,14,13,35])). % 117.40/117.43 cnf(4443,plain, % 117.40/117.43 (~E(f4(a7,a7),f4(f4(a7,a1),f2(a1,a1)))), % 117.40/117.43 inference(scs_inference,[],[3517,4412,4408,3555,2910,3711,3498,3638,20,21,7,8,6,9,10,11,5,4,2,12,3,14])). % 117.40/117.43 cnf(4495,plain, % 117.40/117.43 (~E(f4(f4(a7,a1),f2(a1,a1)),f4(a7,a7))), % 117.40/117.43 inference(scs_inference,[],[4443,2897,3382,3402,20,21,7,8,9,6,10,11,5,4,2])). % 117.40/117.43 cnf(4521,plain, % 117.40/117.43 (~E(f4(a7,f2(a1,a1)),f4(a7,a7))), % 117.40/117.43 inference(scs_inference,[],[4495,3396,842,3622,3537,3528,3448,3638,20,21,7,8,10,11,9,6,5,4,2,12,3])). % 117.40/117.43 cnf(4998,plain, % 117.40/117.43 (E(f4(x49981,f4(a1,a1)),f4(x49981,a1))), % 117.40/117.43 inference(rename_variables,[],[3523])). % 117.40/117.43 cnf(5007,plain, % 117.40/117.43 ($false), % 117.40/117.43 inference(scs_inference,[],[17,15,3638,524,1039,3402,3476,93,3480,3627,4521,4007,3522,3523,4998,3502,2,6,7,3499,529,1024,1066,13,14,3,12,31]), % 117.40/117.43 ['proof']). % 117.40/117.43 % SZS output end Proof % 117.40/117.43 % Total time :116.760000s %------------------------------------------------------------------------------