%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM472+1 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n032.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:26 EDT 2024 % Result : Theorem 118.91s 119.02s % Output : CNFRefutation 119.03s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.09 % Problem : NUM472+1 : TPTP v8.2.0. Released v4.0.0. % 0.02/0.09 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.09/0.28 % Computer : n032.cluster.edu % 0.09/0.28 % Model : x86_64 x86_64 % 0.09/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.28 % Memory : 8042.1875MB % 0.09/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.28 % CPULimit : 300 % 0.09/0.28 % WCLimit : 300 % 0.09/0.28 % DateTime : Sun Jun 23 02:03:38 EDT 2024 % 0.09/0.28 % CPUTime : % 0.14/0.46 start to proof:theBenchmark % 118.91/119.00 %------------------------------------------- % 118.91/119.00 % File :CSE---1.7 % 118.91/119.00 % Problem :theBenchmark % 118.91/119.00 % Transform :cnf % 118.91/119.00 % Format :tptp:raw % 118.91/119.00 % Command :java -jar mcs_scs.jar %d %s % 118.91/119.00 % 118.91/119.00 % Result :Theorem 118.500000s % 118.91/119.00 % Output :CNFRefutation 118.500000s % 118.91/119.00 %------------------------------------------- % 118.91/119.00 %------------------------------------------------------------------------------ % 118.91/119.00 % File : NUM472+1 : TPTP v8.2.0. Released v4.0.0. % 118.91/119.00 % Domain : Number Theory % 118.91/119.00 % Problem : Square root of a prime is irrational 10_03_01, 00 expansion % 118.91/119.00 % Version : Especial. % 118.91/119.00 % English : % 118.91/119.00 % 118.91/119.00 % Refs : [LPV06] Lyaletski et al. (2006), SAD as a Mathematical Assista % 118.91/119.00 % : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 118.91/119.00 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 118.91/119.00 % Source : [Pas08] % 118.91/119.00 % Names : primes_10_03_01.00 [Pas08] % 118.91/119.01 % 118.91/119.01 % Status : Theorem % 118.91/119.01 % Rating : 0.11 v8.1.0, 0.06 v7.5.0, 0.03 v7.4.0, 0.07 v7.3.0, 0.03 v7.2.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.10 v6.4.0, 0.15 v6.3.0, 0.08 v6.2.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.42 v4.1.0, 0.48 v4.0.1, 0.78 v4.0.0 % 118.91/119.01 % Syntax : Number of formulae : 39 ( 5 unt; 4 def) % 118.91/119.01 % Number of atoms : 161 ( 50 equ) % 118.91/119.01 % Maximal formula atoms : 10 ( 4 avg) % 118.91/119.01 % Number of connectives : 137 ( 15 ~; 6 |; 63 &) % 118.91/119.01 % ( 4 <=>; 49 =>; 0 <=; 0 <~>) % 118.91/119.01 % Maximal formula depth : 11 ( 5 avg) % 118.91/119.01 % Maximal term depth : 3 ( 1 avg) % 118.91/119.01 % Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty) % 118.91/119.01 % Number of functors : 11 ( 11 usr; 7 con; 0-2 aty) % 118.91/119.01 % Number of variables : 70 ( 68 !; 2 ?) % 118.91/119.01 % SPC : FOF_THM_RFO_SEQ % 118.91/119.01 % 118.91/119.01 % Comments : Problem generated by the SAD system [VLP07] % 118.91/119.01 %------------------------------------------------------------------------------ % 118.91/119.01 fof(mNatSort,axiom, % 118.91/119.01 ! [W0] : % 118.91/119.01 ( aNaturalNumber0(W0) % 118.91/119.01 => $true ) ). % 118.91/119.01 % 118.91/119.01 fof(mSortsC,axiom, % 118.91/119.01 aNaturalNumber0(sz00) ). % 118.91/119.01 % 118.91/119.01 fof(mSortsC_01,axiom, % 118.91/119.01 ( aNaturalNumber0(sz10) % 118.91/119.01 & sz10 != sz00 ) ). % 118.91/119.01 % 118.91/119.01 fof(mSortsB,axiom, % 118.91/119.01 ! [W0,W1] : % 118.91/119.01 ( ( aNaturalNumber0(W0) % 118.91/119.01 & aNaturalNumber0(W1) ) % 118.91/119.01 => aNaturalNumber0(sdtpldt0(W0,W1)) ) ). % 118.91/119.01 % 118.91/119.01 fof(mSortsB_02,axiom, % 118.91/119.01 ! [W0,W1] : % 118.91/119.01 ( ( aNaturalNumber0(W0) % 118.91/119.01 & aNaturalNumber0(W1) ) % 118.91/119.01 => aNaturalNumber0(sdtasdt0(W0,W1)) ) ). % 118.91/119.01 % 118.91/119.01 fof(mAddComm,axiom, % 118.91/119.01 ! [W0,W1] : % 118.91/119.01 ( ( aNaturalNumber0(W0) % 118.91/119.01 & aNaturalNumber0(W1) ) % 118.91/119.01 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 118.91/119.01 % 118.91/119.01 fof(mAddAsso,axiom, % 118.91/119.01 ! [W0,W1,W2] : % 118.91/119.01 ( ( aNaturalNumber0(W0) % 118.91/119.01 & aNaturalNumber0(W1) % 118.91/119.01 & aNaturalNumber0(W2) ) % 118.91/119.01 => sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) ). % 118.91/119.01 % 118.91/119.01 fof(m_AddZero,axiom, % 118.91/119.01 ! [W0] : % 118.91/119.01 ( aNaturalNumber0(W0) % 118.91/119.01 => ( sdtpldt0(W0,sz00) = W0 % 118.91/119.01 & W0 = sdtpldt0(sz00,W0) ) ) ). % 118.91/119.01 % 118.91/119.01 fof(mMulComm,axiom, % 118.91/119.01 ! [W0,W1] : % 118.91/119.01 ( ( aNaturalNumber0(W0) % 118.91/119.01 & aNaturalNumber0(W1) ) % 118.91/119.01 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 118.91/119.01 % 118.91/119.01 fof(mMulAsso,axiom, % 118.91/119.01 ! [W0,W1,W2] : % 118.91/119.01 ( ( aNaturalNumber0(W0) % 118.91/119.01 & aNaturalNumber0(W1) % 118.91/119.01 & aNaturalNumber0(W2) ) % 118.91/119.01 => sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) ). % 118.91/119.01 % 118.91/119.01 fof(m_MulUnit,axiom, % 118.91/119.01 ! [W0] : % 118.91/119.01 ( aNaturalNumber0(W0) % 118.91/119.01 => ( sdtasdt0(W0,sz10) = W0 % 118.91/119.01 & W0 = sdtasdt0(sz10,W0) ) ) ). % 118.91/119.01 % 118.91/119.01 fof(m_MulZero,axiom, % 118.91/119.01 ! [W0] : % 118.91/119.01 ( aNaturalNumber0(W0) % 118.91/119.01 => ( sdtasdt0(W0,sz00) = sz00 % 118.91/119.01 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 118.91/119.01 % 118.91/119.01 fof(mAMDistr,axiom, % 118.91/119.01 ! [W0,W1,W2] : % 118.91/119.01 ( ( aNaturalNumber0(W0) % 118.91/119.01 & aNaturalNumber0(W1) % 118.91/119.01 & aNaturalNumber0(W2) ) % 118.91/119.01 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 118.91/119.01 & sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ). % 118.91/119.01 % 118.91/119.01 fof(mAddCanc,axiom, % 118.91/119.01 ! [W0,W1,W2] : % 118.91/119.01 ( ( aNaturalNumber0(W0) % 118.91/119.01 & aNaturalNumber0(W1) % 118.91/119.01 & aNaturalNumber0(W2) ) % 118.91/119.01 => ( ( sdtpldt0(W0,W1) = sdtpldt0(W0,W2) % 118.91/119.01 | sdtpldt0(W1,W0) = sdtpldt0(W2,W0) ) % 118.91/119.01 => W1 = W2 ) ) ). % 118.91/119.01 % 118.91/119.01 fof(mMulCanc,axiom, % 118.91/119.01 ! [W0] : % 118.91/119.01 ( aNaturalNumber0(W0) % 118.91/119.01 => ( W0 != sz00 % 118.91/119.01 => ! [W1,W2] : % 118.91/119.01 ( ( aNaturalNumber0(W1) % 118.91/119.01 & aNaturalNumber0(W2) ) % 118.91/119.01 => ( ( sdtasdt0(W0,W1) = sdtasdt0(W0,W2) % 118.91/119.01 | sdtasdt0(W1,W0) = sdtasdt0(W2,W0) ) % 118.91/119.01 => W1 = W2 ) ) ) ) ). % 118.91/119.01 % 118.91/119.01 fof(mZeroAdd,axiom, % 118.91/119.01 ! [W0,W1] : % 118.91/119.01 ( ( aNaturalNumber0(W0) % 118.91/119.01 & aNaturalNumber0(W1) ) % 118.91/119.01 => ( sdtpldt0(W0,W1) = sz00 % 118.91/119.01 => ( W0 = sz00 % 118.91/119.01 & W1 = sz00 ) ) ) ). % 118.91/119.01 % 118.91/119.01 fof(mZeroMul,axiom, % 118.91/119.01 ! [W0,W1] : % 118.91/119.01 ( ( aNaturalNumber0(W0) % 118.91/119.01 & aNaturalNumber0(W1) ) % 118.91/119.01 => ( sdtasdt0(W0,W1) = sz00 % 118.91/119.01 => ( W0 = sz00 % 118.91/119.01 | W1 = sz00 ) ) ) ). % 118.91/119.01 % 118.91/119.01 fof(mDefLE,definition, % 118.91/119.01 ! [W0,W1] : % 118.91/119.01 ( ( aNaturalNumber0(W0) % 118.91/119.01 & aNaturalNumber0(W1) ) % 118.91/119.01 => ( sdtlseqdt0(W0,W1) % 118.91/119.01 <=> ? [W2] : % 118.91/119.01 ( aNaturalNumber0(W2) % 118.91/119.01 & sdtpldt0(W0,W2) = W1 ) ) ) ). % 118.91/119.01 % 118.91/119.01 fof(mDefDiff,definition, % 118.91/119.01 ! [W0,W1] : % 118.91/119.01 ( ( aNaturalNumber0(W0) % 118.91/119.01 & aNaturalNumber0(W1) ) % 118.91/119.01 => ( sdtlseqdt0(W0,W1) % 118.91/119.01 => ! [W2] : % 118.91/119.01 ( W2 = sdtmndt0(W1,W0) % 118.91/119.01 <=> ( aNaturalNumber0(W2) % 118.91/119.01 & sdtpldt0(W0,W2) = W1 ) ) ) ) ). % 118.91/119.01 % 118.91/119.01 fof(mLERefl,axiom, % 118.91/119.01 ! [W0] : % 118.91/119.01 ( aNaturalNumber0(W0) % 118.91/119.01 => sdtlseqdt0(W0,W0) ) ). % 118.91/119.01 % 118.91/119.01 fof(mLEAsym,axiom, % 118.91/119.01 ! [W0,W1] : % 118.91/119.01 ( ( aNaturalNumber0(W0) % 118.91/119.01 & aNaturalNumber0(W1) ) % 118.91/119.01 => ( ( sdtlseqdt0(W0,W1) % 118.91/119.01 & sdtlseqdt0(W1,W0) ) % 118.91/119.01 => W0 = W1 ) ) ). % 118.91/119.01 % 118.91/119.01 fof(mLETran,axiom, % 118.91/119.01 ! [W0,W1,W2] : % 118.91/119.01 ( ( aNaturalNumber0(W0) % 118.91/119.01 & aNaturalNumber0(W1) % 118.91/119.01 & aNaturalNumber0(W2) ) % 118.91/119.01 => ( ( sdtlseqdt0(W0,W1) % 118.91/119.01 & sdtlseqdt0(W1,W2) ) % 118.91/119.01 => sdtlseqdt0(W0,W2) ) ) ). % 118.91/119.01 % 118.91/119.01 fof(mLETotal,axiom, % 118.91/119.01 ! [W0,W1] : % 118.91/119.01 ( ( aNaturalNumber0(W0) % 118.91/119.01 & aNaturalNumber0(W1) ) % 118.91/119.01 => ( sdtlseqdt0(W0,W1) % 118.91/119.01 | ( W1 != W0 % 118.91/119.01 & sdtlseqdt0(W1,W0) ) ) ) ). % 118.91/119.01 % 118.91/119.01 fof(mMonAdd,axiom, % 118.91/119.01 ! [W0,W1] : % 118.91/119.01 ( ( aNaturalNumber0(W0) % 118.91/119.01 & aNaturalNumber0(W1) ) % 118.91/119.01 => ( ( W0 != W1 % 118.91/119.01 & sdtlseqdt0(W0,W1) ) % 118.91/119.01 => ! [W2] : % 118.91/119.01 ( aNaturalNumber0(W2) % 118.91/119.01 => ( sdtpldt0(W2,W0) != sdtpldt0(W2,W1) % 118.91/119.01 & sdtlseqdt0(sdtpldt0(W2,W0),sdtpldt0(W2,W1)) % 118.91/119.01 & sdtpldt0(W0,W2) != sdtpldt0(W1,W2) % 118.91/119.01 & sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W2)) ) ) ) ) ). % 118.91/119.01 % 118.91/119.01 fof(mMonMul,axiom, % 118.91/119.01 ! [W0,W1,W2] : % 118.91/119.01 ( ( aNaturalNumber0(W0) % 118.91/119.01 & aNaturalNumber0(W1) % 118.91/119.01 & aNaturalNumber0(W2) ) % 118.91/119.01 => ( ( W0 != sz00 % 118.91/119.01 & W1 != W2 % 118.91/119.01 & sdtlseqdt0(W1,W2) ) % 118.91/119.01 => ( sdtasdt0(W0,W1) != sdtasdt0(W0,W2) % 118.91/119.01 & sdtlseqdt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 118.91/119.01 & sdtasdt0(W1,W0) != sdtasdt0(W2,W0) % 118.91/119.01 & sdtlseqdt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ) ). % 118.91/119.01 % 118.91/119.01 fof(mLENTr,axiom, % 118.91/119.01 ! [W0] : % 118.91/119.01 ( aNaturalNumber0(W0) % 118.91/119.01 => ( W0 = sz00 % 118.91/119.01 | W0 = sz10 % 118.91/119.01 | ( sz10 != W0 % 118.91/119.01 & sdtlseqdt0(sz10,W0) ) ) ) ). % 118.91/119.01 % 118.91/119.01 fof(mMonMul2,axiom, % 118.91/119.01 ! [W0,W1] : % 118.91/119.01 ( ( aNaturalNumber0(W0) % 118.91/119.01 & aNaturalNumber0(W1) ) % 118.91/119.01 => ( W0 != sz00 % 118.91/119.01 => sdtlseqdt0(W1,sdtasdt0(W1,W0)) ) ) ). % 118.91/119.01 % 118.91/119.01 fof(mIH,axiom, % 118.91/119.01 ! [W0,W1] : % 118.91/119.01 ( ( aNaturalNumber0(W0) % 118.91/119.01 & aNaturalNumber0(W1) ) % 118.91/119.01 => ( iLess0(W0,W1) % 118.91/119.01 => $true ) ) ). % 118.91/119.01 % 118.91/119.01 fof(mIH_03,axiom, % 118.91/119.01 ! [W0,W1] : % 118.91/119.01 ( ( aNaturalNumber0(W0) % 118.91/119.01 & aNaturalNumber0(W1) ) % 118.91/119.01 => ( ( W0 != W1 % 118.91/119.01 & sdtlseqdt0(W0,W1) ) % 118.91/119.01 => iLess0(W0,W1) ) ) ). % 118.91/119.01 % 118.91/119.01 fof(mDefDiv,definition, % 118.91/119.01 ! [W0,W1] : % 118.91/119.01 ( ( aNaturalNumber0(W0) % 118.91/119.01 & aNaturalNumber0(W1) ) % 118.91/119.01 => ( doDivides0(W0,W1) % 118.91/119.01 <=> ? [W2] : % 118.91/119.01 ( aNaturalNumber0(W2) % 118.91/119.01 & W1 = sdtasdt0(W0,W2) ) ) ) ). % 118.91/119.01 % 118.91/119.01 fof(mDefQuot,definition, % 118.91/119.01 ! [W0,W1] : % 118.91/119.01 ( ( aNaturalNumber0(W0) % 118.91/119.01 & aNaturalNumber0(W1) ) % 118.91/119.01 => ( ( W0 != sz00 % 118.91/119.01 & doDivides0(W0,W1) ) % 118.91/119.01 => ! [W2] : % 118.91/119.02 ( W2 = sdtsldt0(W1,W0) % 118.91/119.02 <=> ( aNaturalNumber0(W2) % 118.91/119.02 & W1 = sdtasdt0(W0,W2) ) ) ) ) ). % 118.91/119.02 % 118.91/119.02 fof(mDivTrans,axiom, % 118.91/119.02 ! [W0,W1,W2] : % 118.91/119.02 ( ( aNaturalNumber0(W0) % 118.91/119.02 & aNaturalNumber0(W1) % 118.91/119.02 & aNaturalNumber0(W2) ) % 118.91/119.02 => ( ( doDivides0(W0,W1) % 118.91/119.02 & doDivides0(W1,W2) ) % 118.91/119.02 => doDivides0(W0,W2) ) ) ). % 118.91/119.02 % 118.91/119.02 fof(mDivSum,axiom, % 118.91/119.02 ! [W0,W1,W2] : % 118.91/119.02 ( ( aNaturalNumber0(W0) % 118.91/119.02 & aNaturalNumber0(W1) % 118.91/119.02 & aNaturalNumber0(W2) ) % 118.91/119.02 => ( ( doDivides0(W0,W1) % 118.91/119.02 & doDivides0(W0,W2) ) % 118.91/119.02 => doDivides0(W0,sdtpldt0(W1,W2)) ) ) ). % 118.91/119.02 % 118.91/119.02 fof(m__1324,hypothesis, % 118.91/119.02 ( aNaturalNumber0(xl) % 118.91/119.02 & aNaturalNumber0(xm) % 118.91/119.02 & aNaturalNumber0(xn) ) ). % 118.91/119.02 % 118.91/119.02 fof(m__1324_04,hypothesis, % 118.91/119.02 ( doDivides0(xl,xm) % 118.91/119.02 & doDivides0(xl,sdtpldt0(xm,xn)) ) ). % 118.91/119.02 % 118.91/119.02 fof(m__1347,hypothesis, % 118.91/119.02 xl != sz00 ). % 118.91/119.02 % 118.91/119.02 fof(m__1360,hypothesis, % 118.91/119.02 xp = sdtsldt0(xm,xl) ). % 118.91/119.02 % 118.91/119.02 fof(m__1379,hypothesis, % 118.91/119.02 xq = sdtsldt0(sdtpldt0(xm,xn),xl) ). % 118.91/119.02 % 118.91/119.02 fof(m__,conjecture, % 118.91/119.02 sdtlseqdt0(xm,sdtpldt0(xm,xn)) ). % 118.91/119.02 % 118.91/119.02 %------------------------------------------------------------------------------ % 118.91/119.02 %------------------------------------------- % 118.91/119.02 % Proof found % 118.91/119.02 % SZS status Theorem for theBenchmark % 118.91/119.02 % SZS output start Proof % 118.91/119.02 %ClaNum:85(EqnAxiom:22) % 118.91/119.02 %VarNum:348(SingletonVarNum:109) % 118.91/119.02 %MaxLitNum:7 % 118.91/119.02 %MaxfuncDepth:2 % 118.91/119.02 %SharedTerms:22 % 118.91/119.02 %goalClause: 34 % 118.91/119.02 %singleGoalClaCount:1 % 118.91/119.02 [23]P1(a1) % 118.91/119.02 [24]P1(a8) % 118.91/119.02 [25]P1(a9) % 118.91/119.02 [26]P1(a10) % 118.91/119.02 [27]P1(a11) % 118.91/119.02 [29]P2(a9,a10) % 118.91/119.02 [32]~E(a1,a8) % 118.91/119.02 [33]~E(a1,a9) % 118.91/119.02 [28]E(f2(a10,a9),a12) % 118.91/119.02 [31]P2(a9,f3(a10,a11)) % 118.91/119.02 [34]~P3(a10,f3(a10,a11)) % 118.91/119.02 [30]E(f2(f3(a10,a11),a9),a13) % 118.91/119.02 [41]~P1(x411)+P3(x411,x411) % 118.91/119.02 [35]~P1(x351)+E(f4(a1,x351),a1) % 118.91/119.02 [36]~P1(x361)+E(f4(x361,a1),a1) % 118.91/119.02 [37]~P1(x371)+E(f3(a1,x371),x371) % 118.91/119.02 [38]~P1(x381)+E(f4(a8,x381),x381) % 118.91/119.02 [39]~P1(x391)+E(f3(x391,a1),x391) % 118.91/119.02 [40]~P1(x401)+E(f4(x401,a8),x401) % 118.91/119.02 [47]~P1(x472)+~P1(x471)+E(f3(x471,x472),f3(x472,x471)) % 118.91/119.02 [48]~P1(x482)+~P1(x481)+E(f4(x481,x482),f4(x482,x481)) % 118.91/119.02 [50]~P1(x502)+~P1(x501)+P1(f3(x501,x502)) % 118.91/119.02 [51]~P1(x512)+~P1(x511)+P1(f4(x511,x512)) % 118.91/119.02 [42]~P1(x421)+E(x421,a8)+P3(a8,x421)+E(x421,a1) % 118.91/119.02 [43]~E(x432,x431)+~P1(x431)+~P1(x432)+P3(x431,x432) % 118.91/119.02 [49]P3(x492,x491)+~P1(x491)+~P1(x492)+P3(x491,x492) % 118.91/119.02 [44]~P1(x442)+~P1(x441)+E(x441,a1)+~E(f3(x442,x441),a1) % 118.91/119.02 [45]~P1(x452)+~P1(x451)+E(x451,a1)+~E(f3(x451,x452),a1) % 118.91/119.02 [53]~P1(x532)+~P1(x531)+P3(x532,f4(x532,x531))+E(x531,a1) % 118.91/119.02 [59]~P1(x592)+~P1(x591)+~P3(x591,x592)+P1(f5(x591,x592)) % 118.91/119.02 [60]~P1(x602)+~P1(x601)+~P2(x601,x602)+P1(f6(x601,x602)) % 118.91/119.02 [67]~P1(x671)+~P1(x672)+~P2(x671,x672)+E(f4(x671,f6(x671,x672)),x672) % 118.91/119.02 [68]~P1(x682)+~P1(x681)+~P3(x681,x682)+E(f3(x681,f5(x681,x682)),x682) % 118.91/119.02 [77]~P1(x773)+~P1(x772)+~P1(x771)+E(f3(f3(x771,x772),x773),f3(x771,f3(x772,x773))) % 118.91/119.02 [78]~P1(x783)+~P1(x782)+~P1(x781)+E(f4(f4(x781,x782),x783),f4(x781,f4(x782,x783))) % 118.91/119.02 [84]~P1(x843)+~P1(x842)+~P1(x841)+E(f3(f4(x841,x842),f4(x841,x843)),f4(x841,f3(x842,x843))) % 118.91/119.02 [85]~P1(x852)+~P1(x853)+~P1(x851)+E(f3(f4(x851,x852),f4(x853,x852)),f4(f3(x851,x853),x852)) % 118.91/119.02 [52]P4(x521,x522)+~P1(x522)+~P1(x521)+~P3(x521,x522)+E(x521,x522) % 118.91/119.02 [56]~P1(x562)+~P1(x561)+~P3(x562,x561)+~P3(x561,x562)+E(x561,x562) % 118.91/119.02 [46]~P1(x461)+~P1(x462)+E(x461,a1)+E(x462,a1)+~E(f4(x462,x461),a1) % 118.91/119.02 [54]~P1(x541)+~P1(x542)+~P1(x543)+P2(x541,x542)+~E(x542,f4(x541,x543)) % 118.91/119.02 [55]~P1(x552)+~P1(x551)+~P1(x553)+P3(x551,x552)+~E(f3(x551,x553),x552) % 118.91/119.02 [57]~P1(x573)+~P1(x572)+~P3(x573,x572)+P1(x571)+~E(x571,f7(x572,x573)) % 118.91/119.02 [61]~P1(x612)+~P1(x611)+~P1(x613)+E(x611,x612)+~E(f3(x613,x611),f3(x613,x612)) % 118.91/119.02 [62]~P1(x622)+~P1(x623)+~P1(x621)+E(x621,x622)+~E(f3(x621,x623),f3(x622,x623)) % 118.91/119.02 [65]~P1(x653)+~P1(x651)+~P3(x651,x653)+~E(x652,f7(x653,x651))+E(f3(x651,x652),x653) % 118.91/119.02 [69]~P1(x692)+~P1(x691)+~P3(x693,x692)+~P3(x691,x693)+P3(x691,x692)+~P1(x693) % 118.91/119.02 [70]~P1(x702)+~P1(x701)+~P2(x703,x702)+~P2(x701,x703)+P2(x701,x702)+~P1(x703) % 118.91/119.02 [58]~P1(x581)+~P1(x583)+~P2(x581,x583)+P1(x582)+E(x581,a1)+~E(x582,f2(x583,x581)) % 118.91/119.02 [63]~P1(x632)+~P1(x631)+~P1(x633)+E(x631,x632)+~E(f4(x633,x631),f4(x633,x632))+E(x633,a1) % 118.91/119.02 [64]~P1(x642)+~P1(x643)+~P1(x641)+E(x641,x642)+~E(f4(x641,x643),f4(x642,x643))+E(x643,a1) % 118.91/119.02 [66]~P1(x661)+~P1(x662)+~P2(x661,x662)+~E(x663,f2(x662,x661))+E(x661,a1)+E(x662,f4(x661,x663)) % 118.91/119.02 [71]~P1(x712)+~P1(x713)+~P1(x711)+~P3(x713,x712)+~E(f3(x713,x711),x712)+E(x711,f7(x712,x713)) % 118.91/119.02 [79]~P1(x793)+~P1(x792)+~P1(x791)+~P2(x791,x793)+~P2(x791,x792)+P2(x791,f3(x792,x793)) % 118.91/119.02 [80]~P1(x802)+~P1(x801)+~P1(x803)+~P3(x801,x802)+E(x801,x802)+P3(f3(x803,x801),f3(x803,x802)) % 118.91/119.02 [81]~P1(x812)+~P1(x813)+~P1(x811)+~P3(x811,x812)+E(x811,x812)+P3(f3(x811,x813),f3(x812,x813)) % 118.91/119.02 [72]~P1(x721)+~P1(x723)+~P1(x722)+~P2(x721,x723)+~E(x723,f4(x721,x722))+E(x721,a1)+E(x722,f2(x723,x721)) % 118.91/119.02 [82]~P1(x822)+~P1(x821)+~P1(x823)+~P3(x821,x822)+E(x821,x822)+P3(f4(x823,x821),f4(x823,x822))+E(x823,a1) % 118.91/119.02 [83]~P1(x832)+~P1(x833)+~P1(x831)+~P3(x831,x832)+E(x831,x832)+P3(f4(x831,x833),f4(x832,x833))+E(x833,a1) % 118.91/119.02 %EqnAxiom % 118.91/119.02 [1]E(x11,x11) % 118.91/119.02 [2]E(x22,x21)+~E(x21,x22) % 118.91/119.02 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 118.91/119.02 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 118.91/119.02 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 118.91/119.02 [6]~E(x61,x62)+E(f3(x61,x63),f3(x62,x63)) % 118.91/119.02 [7]~E(x71,x72)+E(f3(x73,x71),f3(x73,x72)) % 118.91/119.02 [8]~E(x81,x82)+E(f4(x81,x83),f4(x82,x83)) % 118.91/119.02 [9]~E(x91,x92)+E(f4(x93,x91),f4(x93,x92)) % 118.91/119.02 [10]~E(x101,x102)+E(f7(x101,x103),f7(x102,x103)) % 118.91/119.02 [11]~E(x111,x112)+E(f7(x113,x111),f7(x113,x112)) % 118.91/119.02 [12]~E(x121,x122)+E(f5(x121,x123),f5(x122,x123)) % 118.91/119.02 [13]~E(x131,x132)+E(f5(x133,x131),f5(x133,x132)) % 118.91/119.02 [14]~E(x141,x142)+E(f6(x141,x143),f6(x142,x143)) % 118.91/119.02 [15]~E(x151,x152)+E(f6(x153,x151),f6(x153,x152)) % 118.91/119.02 [16]~P1(x161)+P1(x162)+~E(x161,x162) % 118.91/119.02 [17]P3(x172,x173)+~E(x171,x172)+~P3(x171,x173) % 118.91/119.02 [18]P3(x183,x182)+~E(x181,x182)+~P3(x183,x181) % 118.91/119.02 [19]P2(x192,x193)+~E(x191,x192)+~P2(x191,x193) % 118.91/119.02 [20]P2(x203,x202)+~E(x201,x202)+~P2(x203,x201) % 118.91/119.02 [21]P4(x212,x213)+~E(x211,x212)+~P4(x211,x213) % 118.91/119.02 [22]P4(x223,x222)+~E(x221,x222)+~P4(x223,x221) % 118.91/119.02 % 118.91/119.02 %------------------------------------------- % 119.03/119.02 cnf(87,plain, % 119.03/119.02 (P2(x871,f4(x871,x872))+~P1(x871)+~P1(f4(x871,x872))+~P1(x872)), % 119.03/119.02 inference(equality_inference,[],[54])). % 119.03/119.02 cnf(88,plain, % 119.03/119.02 (P3(x881,f3(x881,x882))+~P1(f3(x881,x882))+~P1(x881)+~P1(x882)), % 119.03/119.02 inference(equality_inference,[],[55])). % 119.03/119.02 cnf(89,plain, % 119.03/119.02 (~P3(x891,x892)+~P1(x891)+~P1(x892)+P1(f7(x892,x891))), % 119.03/119.02 inference(equality_inference,[],[57])). % 119.03/119.02 cnf(90,plain, % 119.03/119.02 (~P2(x901,x902)+~P1(x901)+~P1(x902)+P1(f2(x902,x901))+E(x901,a1)), % 119.03/119.02 inference(equality_inference,[],[58])). % 119.03/119.02 cnf(95,plain, % 119.03/119.02 (~P3(x951,x952)+~P1(x952)+~P1(x951)+E(f3(x951,f7(x952,x951)),x952)), % 119.03/119.02 inference(equality_inference,[],[65])). % 119.03/119.02 cnf(97,plain, % 119.03/119.02 (~P3(x971,f3(x971,x972))+~P1(f3(x971,x972))+~P1(x971)+~P1(x972)+E(x972,f7(f3(x971,x972),x971))), % 119.03/119.02 inference(equality_inference,[],[71])). % 119.03/119.02 cnf(100,plain, % 119.03/119.02 (P3(a1,a1)), % 119.03/119.02 inference(scs_inference,[],[28,23,2,49])). % 119.03/119.02 cnf(102,plain, % 119.03/119.02 (P1(f7(a1,a1))), % 119.03/119.02 inference(scs_inference,[],[28,23,2,49,89])). % 119.03/119.02 cnf(104,plain, % 119.03/119.02 (E(f3(a1,f7(a1,a1)),a1)), % 119.03/119.02 inference(scs_inference,[],[28,23,2,49,89,95])). % 119.03/119.02 cnf(106,plain, % 119.03/119.02 (P3(x1061,a1)+~E(a1,x1061)), % 119.03/119.02 inference(scs_inference,[],[28,23,2,49,89,95,17])). % 119.03/119.02 cnf(113,plain, % 119.03/119.02 (E(f7(a1,a1),a1)), % 119.03/119.02 inference(scs_inference,[],[30,102,104,23,2,44])). % 119.03/119.02 cnf(115,plain, % 119.03/119.02 (P3(f7(a1,a1),f7(a1,a1))), % 119.03/119.02 inference(scs_inference,[],[30,102,104,23,2,44,49])). % 119.03/119.02 cnf(117,plain, % 119.03/119.02 (E(x1171,a1)+~E(x1171,f3(a1,f7(a1,a1)))), % 119.03/119.02 inference(scs_inference,[],[30,102,104,23,2,44,49,3])). % 119.03/119.02 cnf(118,plain, % 119.03/119.02 (P3(f7(a1,a1),a1)), % 119.03/119.02 inference(scs_inference,[],[30,102,104,23,2,44,49,3,18])). % 119.03/119.02 cnf(119,plain, % 119.03/119.02 (P3(a1,f7(a1,a1))), % 119.03/119.02 inference(scs_inference,[],[30,102,104,23,2,44,49,3,18,17])). % 119.03/119.02 cnf(137,plain, % 119.03/119.02 (E(a1,f7(a1,a1))), % 119.03/119.02 inference(scs_inference,[],[113,2])). % 119.03/119.02 cnf(138,plain, % 119.03/119.02 (E(f3(f7(a1,a1),f7(f7(a1,a1),f7(a1,a1))),f7(a1,a1))), % 119.03/119.02 inference(scs_inference,[],[115,113,102,2,95])). % 119.03/119.02 cnf(140,plain, % 119.03/119.02 (P3(a8,a8)), % 119.03/119.02 inference(scs_inference,[],[115,113,24,102,2,95,49])). % 119.03/119.02 cnf(142,plain, % 119.03/119.02 (P1(f7(a8,a8))), % 119.03/119.02 inference(scs_inference,[],[115,113,24,102,2,95,49,89])). % 119.03/119.02 cnf(144,plain, % 119.03/119.02 (P1(f3(f7(a1,a1),f7(f7(a1,a1),f7(a1,a1))))), % 119.03/119.02 inference(scs_inference,[],[100,115,113,24,102,23,2,95,49,89,57])). % 119.03/119.02 cnf(146,plain, % 119.03/119.02 (E(x1461,f7(a1,a1))+~E(x1461,f3(f7(a1,a1),f7(f7(a1,a1),f7(a1,a1))))), % 119.03/119.02 inference(scs_inference,[],[100,115,113,24,102,23,2,95,49,89,57,3])). % 119.03/119.02 cnf(151,plain, % 119.03/119.02 (E(a1,f3(a1,f7(a1,a1)))), % 119.03/119.02 inference(scs_inference,[],[104,2])). % 119.03/119.02 cnf(152,plain, % 119.03/119.02 (E(f3(f7(a1,a1),f7(f7(a1,a1),f7(a1,a1))),a1)), % 119.03/119.02 inference(scs_inference,[],[113,104,138,2,3])). % 119.03/119.02 cnf(153,plain, % 119.03/119.02 (P1(f3(a1,f7(a1,a1)))), % 119.03/119.02 inference(scs_inference,[],[113,104,138,23,2,3,16])). % 119.03/119.02 cnf(154,plain, % 119.03/119.02 (E(f3(a8,f7(a8,a8)),a8)), % 119.03/119.02 inference(scs_inference,[],[140,113,104,138,24,23,2,3,16,95])). % 119.03/119.02 cnf(156,plain, % 119.03/119.02 (P3(f7(a8,a8),f7(a8,a8))), % 119.03/119.02 inference(scs_inference,[],[140,113,104,138,142,24,23,2,3,16,95,49])). % 119.03/119.02 cnf(158,plain, % 119.03/119.02 (P1(f7(f7(a8,a8),f7(a8,a8)))), % 119.03/119.02 inference(scs_inference,[],[140,113,104,138,142,24,23,2,3,16,95,49,89])). % 119.03/119.02 cnf(160,plain, % 119.03/119.02 (P3(f3(a1,f7(a1,a1)),a1)), % 119.03/119.02 inference(scs_inference,[],[140,113,104,138,142,24,23,2,3,16,95,49,89,106])). % 119.03/119.02 cnf(162,plain, % 119.03/119.02 (P3(f3(a1,f7(a1,a1)),f7(a1,a1))), % 119.03/119.02 inference(scs_inference,[],[140,113,104,138,137,142,31,24,23,2,3,16,95,49,89,106,19,18])). % 119.03/119.02 cnf(164,plain, % 119.03/119.02 (P3(x1641,a8)+~E(a8,x1641)), % 119.03/119.02 inference(scs_inference,[],[140,113,104,138,137,142,31,24,23,2,3,16,95,49,89,106,19,18,20,17])). % 119.03/119.02 cnf(176,plain, % 119.03/119.02 (E(f3(f7(a8,a8),f7(f7(a8,a8),f7(a8,a8))),f7(a8,a8))), % 119.03/119.02 inference(scs_inference,[],[156,113,138,151,142,2,3,95])). % 119.03/119.02 cnf(180,plain, % 119.03/119.02 (P1(f7(f7(a1,a1),f7(a1,a1)))), % 119.03/119.02 inference(scs_inference,[],[115,156,113,138,158,151,142,102,2,3,95,49,89])). % 119.03/119.02 cnf(182,plain, % 119.03/119.02 (P1(f3(f7(a8,a8),f7(f7(a8,a8),f7(a8,a8))))), % 119.03/119.02 inference(scs_inference,[],[115,156,140,113,138,158,151,142,24,102,2,3,95,49,89,57])). % 119.03/119.02 cnf(184,plain, % 119.03/119.02 (E(f7(f7(a1,a1),f7(a1,a1)),f7(a1,f7(a1,a1)))), % 119.03/119.02 inference(scs_inference,[],[118,115,156,140,113,138,158,152,151,142,24,102,23,2,3,95,49,89,57,71])). % 119.03/119.02 cnf(186,plain, % 119.03/119.02 (P2(x1861,a10)+~E(a9,x1861)), % 119.03/119.02 inference(scs_inference,[],[118,115,156,140,113,138,158,152,151,142,24,29,102,23,2,3,95,49,89,57,71,19])). % 119.03/119.02 cnf(187,plain, % 119.03/119.02 (P1(f7(a1,f7(a1,a1)))), % 119.03/119.02 inference(scs_inference,[],[118,115,156,140,113,138,158,152,151,142,24,29,102,23,2,3,95,49,89,57,71,19,16])). % 119.03/119.02 cnf(188,plain, % 119.03/119.02 (E(f7(f7(a1,a1),f7(a1,a1)),a1)), % 119.03/119.02 inference(scs_inference,[],[118,115,156,140,113,138,158,152,151,142,24,29,102,23,2,3,95,49,89,57,71,19,16,44])). % 119.03/119.02 cnf(190,plain, % 119.03/119.02 (P3(f7(a8,a8),x1901)+~E(f7(a8,a8),x1901)), % 119.03/119.02 inference(scs_inference,[],[118,115,156,140,113,138,158,152,151,142,24,29,102,23,2,3,95,49,89,57,71,19,16,44,18])). % 119.03/119.02 cnf(191,plain, % 119.03/119.02 (P2(a9,x1911)+~E(a10,x1911)), % 119.03/119.02 inference(scs_inference,[],[118,115,156,140,113,138,158,152,151,142,24,29,102,23,2,3,95,49,89,57,71,19,16,44,18,20])). % 119.03/119.02 cnf(192,plain, % 119.03/119.02 (P3(x1921,f7(a8,a8))+~E(f7(a8,a8),x1921)), % 119.03/119.02 inference(scs_inference,[],[118,115,156,140,113,138,158,152,151,142,24,29,102,23,2,3,95,49,89,57,71,19,16,44,18,20,17])). % 119.03/119.02 cnf(193,plain, % 119.03/119.02 (P3(f3(a1,f7(a1,a1)),f3(a1,f7(a1,a1)))), % 119.03/119.02 inference(scs_inference,[],[118,115,156,140,113,138,158,153,152,151,142,24,29,102,23,2,3,95,49,89,57,71,19,16,44,18,20,17,43])). % 119.03/119.02 cnf(201,plain, % 119.03/119.02 (E(a1,f7(f7(a1,a1),f7(a1,a1)))), % 119.03/119.02 inference(scs_inference,[],[188,2])). % 119.03/119.02 cnf(202,plain, % 119.03/119.02 (~E(a1,f3(a8,f7(a8,a8)))), % 119.03/119.02 inference(scs_inference,[],[188,154,32,2,3])). % 119.03/119.02 cnf(203,plain, % 119.03/119.02 (P3(a1,f3(a1,f7(a1,a1)))), % 119.03/119.02 inference(scs_inference,[],[193,188,104,154,32,2,3,17])). % 119.03/119.02 cnf(204,plain, % 119.03/119.02 (P3(f7(f7(a1,a1),f7(a1,a1)),f7(f7(a1,a1),f7(a1,a1)))), % 119.03/119.02 inference(scs_inference,[],[193,188,104,154,180,32,2,3,17,49])). % 119.03/119.02 cnf(206,plain, % 119.03/119.02 (P3(f7(f7(a1,a1),f7(a1,a1)),a1)), % 119.03/119.02 inference(scs_inference,[],[193,188,104,154,180,32,2,3,17,49,106])). % 119.03/119.02 cnf(208,plain, % 119.03/119.02 (P3(f7(f7(a1,a1),f7(a1,a1)),f7(a1,a1))), % 119.03/119.02 inference(scs_inference,[],[193,28,188,104,137,154,180,32,2,3,17,49,106,16,18])). % 119.03/119.02 cnf(213,plain, % 119.03/119.02 (P3(f7(a1,f7(a1,a1)),f7(a1,f7(a1,a1)))), % 119.03/119.02 inference(scs_inference,[],[193,28,188,104,137,154,180,187,32,25,2,3,17,49,106,16,18,95,88,43])). % 119.03/119.02 cnf(215,plain, % 119.03/119.02 (P2(a10,f4(a10,a10))+~P1(f4(a10,a10))), % 119.03/119.02 inference(scs_inference,[],[193,28,188,104,137,154,180,187,32,25,26,2,3,17,49,106,16,18,95,88,43,87])). % 119.03/119.02 cnf(219,plain, % 119.03/119.02 (E(a1,f3(f7(a1,a1),f7(f7(a1,a1),f7(a1,a1))))), % 119.03/119.02 inference(scs_inference,[],[152,2])). % 119.03/119.02 cnf(220,plain, % 119.03/119.02 (E(a1,f7(a1,f7(a1,a1)))), % 119.03/119.02 inference(scs_inference,[],[152,184,201,2,3])). % 119.03/119.02 cnf(221,plain, % 119.03/119.02 (P3(a1,f7(f7(a1,a1),f7(a1,a1)))), % 119.03/119.02 inference(scs_inference,[],[204,188,152,184,201,2,3,17])). % 119.03/119.02 cnf(222,plain, % 119.03/119.02 (P3(a9,a9)), % 119.03/119.02 inference(scs_inference,[],[204,188,152,184,25,201,2,3,17,49])). % 119.03/119.02 cnf(224,plain, % 119.03/119.02 (P1(f7(a9,a9))), % 119.03/119.02 inference(scs_inference,[],[204,188,152,184,25,201,2,3,17,49,89])). % 119.03/119.02 cnf(229,plain, % 119.03/119.02 (E(f3(a9,f7(a9,a9)),a9)), % 119.03/119.02 inference(scs_inference,[],[204,188,30,152,137,184,25,201,2,3,17,49,89,106,16,18,95])). % 119.03/119.02 cnf(231,plain, % 119.03/119.02 (P3(a8,f3(a8,a8))+~P1(f3(a8,a8))), % 119.03/119.03 inference(scs_inference,[],[204,188,30,152,137,24,184,25,201,2,3,17,49,89,106,16,18,95,88])). % 119.03/119.03 cnf(233,plain, % 119.03/119.03 (P3(a11,a11)), % 119.03/119.03 inference(scs_inference,[],[204,188,30,152,137,24,184,25,201,27,2,3,17,49,89,106,16,18,95,88,43])). % 119.03/119.03 cnf(235,plain, % 119.03/119.03 (P2(a8,f4(a8,a8))+~P1(f4(a8,a8))), % 119.03/119.03 inference(scs_inference,[],[204,188,30,152,137,24,184,25,201,27,2,3,17,49,89,106,16,18,95,88,43,87])). % 119.03/119.03 cnf(238,plain, % 119.03/119.03 (P3(f7(a1,f7(a1,a1)),a1)), % 119.03/119.03 inference(scs_inference,[],[220,106])). % 119.03/119.03 cnf(243,plain, % 119.03/119.03 (E(f3(a11,f7(a11,a11)),a11)), % 119.03/119.03 inference(scs_inference,[],[203,233,156,113,137,176,201,220,27,106,2,3,18,17,95])). % 119.03/119.03 cnf(245,plain, % 119.03/119.03 (P3(f7(a9,a9),f7(a9,a9))), % 119.03/119.03 inference(scs_inference,[],[203,233,156,113,137,176,201,224,220,27,106,2,3,18,17,95,49])). % 119.03/119.03 cnf(247,plain, % 119.03/119.03 (P1(f7(f7(a9,a9),f7(a9,a9)))), % 119.03/119.03 inference(scs_inference,[],[203,233,156,113,137,176,201,224,220,27,106,2,3,18,17,95,49,89])). % 119.03/119.03 cnf(249,plain, % 119.03/119.03 (E(f3(a1,f7(a1,a1)),f7(a1,a1))), % 119.03/119.03 inference(scs_inference,[],[162,203,233,156,113,137,176,102,201,153,224,220,27,106,2,3,18,17,95,49,89,56])). % 119.03/119.03 cnf(251,plain, % 119.03/119.03 (E(f7(a1,a1),f7(f7(a1,a1),a1))), % 119.03/119.03 inference(scs_inference,[],[119,162,203,233,156,113,137,176,102,23,201,153,224,220,27,106,2,3,18,17,95,49,89,56,71])). % 119.03/119.03 cnf(258,plain, % 119.03/119.03 (E(a8,f3(a8,f7(a8,a8)))), % 119.03/119.03 inference(scs_inference,[],[154,2])). % 119.03/119.03 cnf(259,plain, % 119.03/119.03 (~E(a1,f3(a9,f7(a9,a9)))), % 119.03/119.03 inference(scs_inference,[],[154,229,33,2,3])). % 119.03/119.03 cnf(260,plain, % 119.03/119.03 (P1(f7(f7(a1,a1),a1))), % 119.03/119.03 inference(scs_inference,[],[154,102,229,251,33,2,3,16])). % 119.03/119.03 cnf(263,plain, % 119.03/119.03 (E(f3(f7(a9,a9),f7(f7(a9,a9),f7(a9,a9))),f7(a9,a9))), % 119.03/119.03 inference(scs_inference,[],[245,221,238,137,154,102,229,251,33,224,2,3,16,18,17,95])). % 119.03/119.03 cnf(267,plain, % 119.03/119.03 (P1(f7(a11,a11))), % 119.03/119.03 inference(scs_inference,[],[245,221,238,233,137,154,102,229,247,251,33,224,27,2,3,16,18,17,95,49,89])). % 119.03/119.03 cnf(273,plain, % 119.03/119.03 (P3(f3(a8,f7(a8,a8)),a8)), % 119.03/119.03 inference(scs_inference,[],[208,245,222,221,238,233,137,154,102,180,25,229,247,251,33,224,27,2,3,16,18,17,95,49,89,56,57,164])). % 119.03/119.03 cnf(274,plain, % 119.03/119.03 (P3(f7(a1,a1),f3(f7(a1,a1),f7(a1,a1)))+~P1(f3(f7(a1,a1),f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[208,245,222,221,238,233,137,154,102,180,25,229,247,251,33,224,27,2,3,16,18,17,95,49,89,56,57,164,88])). % 119.03/119.03 cnf(276,plain, % 119.03/119.03 (P3(a10,a10)), % 119.03/119.03 inference(scs_inference,[],[208,245,222,221,238,233,137,154,102,180,25,229,247,251,33,224,26,27,2,3,16,18,17,95,49,89,56,57,164,88,43])). % 119.03/119.03 cnf(283,plain, % 119.03/119.03 (E(f7(a1,a1),f7(a1,f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[113,184,220,2,3])). % 119.03/119.03 cnf(285,plain, % 119.03/119.03 (P1(f3(a8,f7(a8,a8)))), % 119.03/119.03 inference(scs_inference,[],[213,113,24,184,220,258,2,3,18,16])). % 119.03/119.03 cnf(286,plain, % 119.03/119.03 (P3(f7(f7(a1,a1),f7(a1,a1)),f7(a1,f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[213,113,24,184,220,258,2,3,18,16,17])). % 119.03/119.03 cnf(287,plain, % 119.03/119.03 (P3(f7(a11,a11),f7(a11,a11))), % 119.03/119.03 inference(scs_inference,[],[213,113,24,184,220,267,258,2,3,18,16,17,49])). % 119.03/119.03 cnf(289,plain, % 119.03/119.03 (E(f3(f7(a11,a11),f7(f7(a11,a11),f7(a11,a11))),f7(a11,a11))), % 119.03/119.03 inference(scs_inference,[],[213,113,24,184,220,267,258,2,3,18,16,17,49,95])). % 119.03/119.03 cnf(291,plain, % 119.03/119.03 (P1(f7(f7(a11,a11),f7(a11,a11)))), % 119.03/119.03 inference(scs_inference,[],[213,113,24,184,220,267,258,2,3,18,16,17,49,95,89])). % 119.03/119.03 cnf(297,plain, % 119.03/119.03 (P3(f7(f7(a1,a1),a1),f7(f7(a1,a1),a1))), % 119.03/119.03 inference(scs_inference,[],[213,233,113,24,23,184,220,267,260,258,27,2,3,18,16,17,49,95,89,57,88,43])). % 119.03/119.03 cnf(301,plain, % 119.03/119.03 (E(a1,f7(f3(a1,a1),a1))+~P1(f3(a1,a1))), % 119.03/119.03 inference(scs_inference,[],[213,233,113,24,23,184,220,267,260,258,27,2,3,18,16,17,49,95,89,57,88,43,87,56,97])). % 119.03/119.03 cnf(303,plain, % 119.03/119.03 (E(a9,f3(a9,f7(a9,a9)))), % 119.03/119.03 inference(scs_inference,[],[229,2])). % 119.03/119.03 cnf(305,plain, % 119.03/119.03 (P1(f3(a9,f7(a9,a9)))), % 119.03/119.03 inference(scs_inference,[],[31,229,25,2,19,16])). % 119.03/119.03 cnf(306,plain, % 119.03/119.03 (P3(f3(a8,f7(a8,a8)),f3(a8,f7(a8,a8)))), % 119.03/119.03 inference(scs_inference,[],[273,31,229,25,258,2,19,16,18])). % 119.03/119.03 cnf(307,plain, % 119.03/119.03 (P3(a1,f7(a1,f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[273,286,188,31,229,25,258,2,19,16,18,17])). % 119.03/119.03 cnf(308,plain, % 119.03/119.03 (E(f3(a10,f7(a10,a10)),a10)), % 119.03/119.03 inference(scs_inference,[],[273,286,276,188,31,229,25,258,26,2,19,16,18,17,95])). % 119.03/119.03 cnf(312,plain, % 119.03/119.03 (P1(f7(a10,a10))), % 119.03/119.03 inference(scs_inference,[],[273,286,276,188,31,229,25,258,291,26,2,19,16,18,17,95,49,89])). % 119.03/119.03 cnf(314,plain, % 119.03/119.03 (E(f7(a1,f7(a1,a1)),a1)), % 119.03/119.03 inference(scs_inference,[],[273,238,286,276,188,31,23,229,25,187,258,291,26,2,19,16,18,17,95,49,89,56])). % 119.03/119.03 cnf(316,plain, % 119.03/119.03 (P2(f3(a9,f7(a9,a9)),a10)), % 119.03/119.03 inference(scs_inference,[],[273,238,286,276,188,31,23,229,25,187,258,291,26,2,19,16,18,17,95,49,89,56,186])). % 119.03/119.03 cnf(318,plain, % 119.03/119.03 (E(x3181,a11)+~E(x3181,f3(a11,f7(a11,a11)))), % 119.03/119.03 inference(scs_inference,[],[273,238,286,276,188,31,23,229,243,25,187,258,291,26,2,19,16,18,17,95,49,89,56,186,20,3])). % 119.03/119.03 cnf(319,plain, % 119.03/119.03 (P3(f7(a9,a9),f3(f7(a9,a9),f7(a9,a9)))+~P1(f3(f7(a9,a9),f7(a9,a9)))), % 119.03/119.03 inference(scs_inference,[],[273,238,286,276,188,31,23,229,243,25,187,224,258,291,26,2,19,16,18,17,95,49,89,56,186,20,3,88])). % 119.03/119.03 cnf(321,plain, % 119.03/119.03 (P3(f3(a9,f7(a9,a9)),f3(a9,f7(a9,a9)))), % 119.03/119.03 inference(scs_inference,[],[273,238,286,276,188,31,23,229,243,25,187,224,258,291,26,2,19,16,18,17,95,49,89,56,186,20,3,88,43])). % 119.03/119.03 cnf(330,plain, % 119.03/119.03 (E(a11,f3(a11,f7(a11,a11)))), % 119.03/119.03 inference(scs_inference,[],[243,2])). % 119.03/119.03 cnf(332,plain, % 119.03/119.03 (P1(f3(a11,f7(a11,a11)))), % 119.03/119.03 inference(scs_inference,[],[321,229,243,27,2,18,16])). % 119.03/119.03 cnf(333,plain, % 119.03/119.03 (P3(a8,f3(a8,f7(a8,a8)))), % 119.03/119.03 inference(scs_inference,[],[306,321,154,229,243,27,2,18,16,17])). % 119.03/119.03 cnf(334,plain, % 119.03/119.03 (P3(f7(a10,a10),f7(a10,a10))), % 119.03/119.03 inference(scs_inference,[],[306,321,154,229,243,27,312,2,18,16,17,49])). % 119.03/119.03 cnf(336,plain, % 119.03/119.03 (E(f3(f7(a10,a10),f7(f7(a10,a10),f7(a10,a10))),f7(a10,a10))), % 119.03/119.03 inference(scs_inference,[],[306,321,154,229,243,27,312,2,18,16,17,49,95])). % 119.03/119.03 cnf(338,plain, % 119.03/119.03 (P1(f7(f7(a10,a10),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[306,321,154,229,243,27,312,2,18,16,17,49,95,89])). % 119.03/119.03 cnf(342,plain, % 119.03/119.03 (P2(f3(a9,f7(a9,a9)),x3421)+~E(a10,x3421)), % 119.03/119.03 inference(scs_inference,[],[306,321,276,154,229,243,26,27,312,316,2,18,16,17,49,95,89,57,20])). % 119.03/119.03 cnf(344,plain, % 119.03/119.03 (P3(f7(a11,a11),f3(f7(a11,a11),f7(a11,a11)))+~P1(f3(f7(a11,a11),f7(a11,a11)))), % 119.03/119.03 inference(scs_inference,[],[306,321,276,154,229,243,263,267,26,27,312,316,2,18,16,17,49,95,89,57,20,3,88])). % 119.03/119.03 cnf(346,plain, % 119.03/119.03 (P3(f3(a11,f7(a11,a11)),f3(a11,f7(a11,a11)))), % 119.03/119.03 inference(scs_inference,[],[306,321,276,154,229,243,263,267,26,27,312,316,2,18,16,17,49,95,89,57,20,3,88,43])). % 119.03/119.03 cnf(348,plain, % 119.03/119.03 (P2(f7(a11,a11),f4(f7(a11,a11),f7(a11,a11)))+~P1(f4(f7(a11,a11),f7(a11,a11)))), % 119.03/119.03 inference(scs_inference,[],[306,321,276,154,229,243,263,267,26,27,312,316,2,18,16,17,49,95,89,57,20,3,88,43,87])). % 119.03/119.03 cnf(350,plain, % 119.03/119.03 (E(f7(a11,a11),f7(f3(f7(a11,a11),f7(a11,a11)),f7(a11,a11)))+~P1(f3(f7(a11,a11),f7(a11,a11)))), % 119.03/119.03 inference(scs_inference,[],[306,321,276,154,229,243,263,267,26,27,312,316,2,18,16,17,49,95,89,57,20,3,88,43,87,97])). % 119.03/119.03 cnf(357,plain, % 119.03/119.03 (P3(f7(f7(a10,a10),f7(a10,a10)),f7(f7(a10,a10),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[307,346,137,243,263,338,2,18,17,49])). % 119.03/119.03 cnf(365,plain, % 119.03/119.03 (E(f7(a11,a11),f3(f7(a11,a11),f7(f7(a11,a11),f7(a11,a11))))), % 119.03/119.03 inference(scs_inference,[],[289,2])). % 119.03/119.03 cnf(366,plain, % 119.03/119.03 (P3(f3(a1,f7(a1,a1)),f7(f7(a1,a1),f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[160,201,289,2,18])). % 119.03/119.03 cnf(367,plain, % 119.03/119.03 (P3(f7(f7(a1,a1),f7(a1,a1)),f3(a1,f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[160,203,201,289,2,18,17])). % 119.03/119.03 cnf(370,plain, % 119.03/119.03 (E(x3701,a10)+~E(x3701,f3(a10,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[160,203,201,289,180,153,308,2,18,17,56,3])). % 119.03/119.03 cnf(380,plain, % 119.03/119.03 (E(a10,f3(a10,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[308,2])). % 119.03/119.03 cnf(385,plain, % 119.03/119.03 (P3(f3(a10,f7(a10,a10)),f3(a10,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[287,29,26,308,365,2,20,16,18,17,49])). % 119.03/119.03 cnf(389,plain, % 119.03/119.03 (E(f7(a1,a1),f7(f7(f7(a1,a1),f7(a1,a1)),a1))), % 119.03/119.03 inference(scs_inference,[],[221,287,366,367,29,102,23,26,180,153,308,365,2,20,16,18,17,49,56,71])). % 119.03/119.03 cnf(393,plain, % 119.03/119.03 (~E(x3931,f3(f7(a10,a10),f7(f7(a10,a10),f7(a10,a10))))+P1(x3931)), % 119.03/119.03 inference(scs_inference,[],[221,287,366,367,276,29,102,23,26,180,153,308,336,365,2,20,16,18,17,49,56,71,342,3,57])). % 119.03/119.03 cnf(400,plain, % 119.03/119.03 (E(f7(a10,a10),f3(f7(a10,a10),f7(f7(a10,a10),f7(a10,a10))))), % 119.03/119.03 inference(scs_inference,[],[336,2])). % 119.03/119.03 cnf(401,plain, % 119.03/119.03 (~E(a10,f3(a10,a11))), % 119.03/119.03 inference(scs_inference,[],[34,276,336,2,18])). % 119.03/119.03 cnf(402,plain, % 119.03/119.03 (P1(f7(f7(f7(a1,a1),f7(a1,a1)),a1))), % 119.03/119.03 inference(scs_inference,[],[34,276,102,336,389,2,18,16])). % 119.03/119.03 cnf(403,plain, % 119.03/119.03 (P3(f3(a10,f7(a10,a10)),a10)), % 119.03/119.03 inference(scs_inference,[],[34,276,102,336,389,380,2,18,16,17])). % 119.03/119.03 cnf(406,plain, % 119.03/119.03 (E(f7(a8,a8),f7(f3(f7(a8,a8),f7(a8,a8)),f7(a8,a8)))+~P1(f4(f7(a10,a10),f7(a10,a10)))+~P1(f3(f7(a8,a8),f7(a8,a8)))), % 119.03/119.03 inference(scs_inference,[],[34,276,142,102,312,336,182,389,380,2,18,16,17,87,88,97])). % 119.03/119.03 cnf(407,plain, % 119.03/119.03 (P1(f5(f7(a8,a8),f7(a8,a8)))), % 119.03/119.03 inference(scs_inference,[],[142,41,59])). % 119.03/119.03 cnf(408,plain, % 119.03/119.03 (E(f7(f7(a1,a1),a1),f7(a1,a1))), % 119.03/119.03 inference(scs_inference,[],[251,2])). % 119.03/119.03 cnf(409,plain, % 119.03/119.03 (P3(f7(a10,a10),f3(f7(a10,a10),f7(f7(a10,a10),f7(a10,a10))))), % 119.03/119.03 inference(scs_inference,[],[334,251,400,2,18])). % 119.03/119.03 cnf(411,plain, % 119.03/119.03 (P3(f5(f7(a8,a8),f7(a8,a8)),f5(f7(a8,a8),f7(a8,a8)))), % 119.03/119.03 inference(scs_inference,[],[334,251,407,400,2,18,17,49])). % 119.03/119.03 cnf(413,plain, % 119.03/119.03 (P3(a10,f3(a10,a10))+~P1(f3(a10,a10))), % 119.03/119.03 inference(scs_inference,[],[334,26,251,407,400,2,18,17,49,88])). % 119.03/119.03 cnf(415,plain, % 119.03/119.03 (P2(a11,f4(a11,a11))+~P1(f4(a11,a11))), % 119.03/119.03 inference(scs_inference,[],[334,26,27,251,407,400,2,18,17,49,88,87])). % 119.03/119.03 cnf(418,plain, % 119.03/119.03 (E(f7(f7(f7(a1,a1),f7(a1,a1)),a1),f7(a1,a1))), % 119.03/119.03 inference(scs_inference,[],[389,2])). % 119.03/119.03 cnf(419,plain, % 119.03/119.03 (P3(f7(f7(a1,a1),a1),f7(a1,a1))), % 119.03/119.03 inference(scs_inference,[],[297,389,408,2,18])). % 119.03/119.03 cnf(420,plain, % 119.03/119.03 (P3(f7(a1,a1),f7(f7(a1,a1),a1))), % 119.03/119.03 inference(scs_inference,[],[297,389,408,2,18,17])). % 119.03/119.03 cnf(424,plain, % 119.03/119.03 (E(f3(a1,f7(a1,a1)),f7(a1,f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[249,283,3])). % 119.03/119.03 cnf(425,plain, % 119.03/119.03 (P3(f7(f7(a1,a1),a1),a1)), % 119.03/119.03 inference(scs_inference,[],[419,113,249,283,3,18])). % 119.03/119.03 cnf(426,plain, % 119.03/119.03 (P3(a10,f3(a10,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[385,419,113,249,308,283,3,18,17])). % 119.03/119.03 cnf(427,plain, % 119.03/119.03 (E(f7(a1,a1),f7(f7(a1,f7(a1,a1)),a1))), % 119.03/119.03 inference(scs_inference,[],[307,385,419,113,249,23,102,308,187,283,3,18,17,71])). % 119.03/119.03 cnf(429,plain, % 119.03/119.03 (E(f7(a1,f7(a1,a1)),f3(a1,f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[307,385,419,113,249,23,102,308,187,283,3,18,17,71,2])). % 119.03/119.03 cnf(431,plain, % 119.03/119.03 (P3(a11,f3(a11,a11))+~P1(f3(a11,a11))), % 119.03/119.03 inference(scs_inference,[],[307,385,419,113,249,23,102,27,308,187,283,3,18,17,71,2,16,88])). % 119.03/119.03 cnf(437,plain, % 119.03/119.03 (E(f3(a1,f7(a1,a1)),f7(f7(a1,a1),a1))), % 119.03/119.03 inference(scs_inference,[],[249,251,427,2,3])). % 119.03/119.03 cnf(438,plain, % 119.03/119.03 (P3(f7(f7(a1,a1),a1),f7(f7(a1,a1),f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[425,249,201,251,427,2,3,18])). % 119.03/119.03 cnf(439,plain, % 119.03/119.03 (P3(a1,f7(f7(a1,a1),a1))), % 119.03/119.03 inference(scs_inference,[],[420,425,113,249,201,251,427,2,3,18,17])). % 119.03/119.03 cnf(440,plain, % 119.03/119.03 (E(a1,f7(f7(a1,a1),a1))), % 119.03/119.03 inference(scs_inference,[],[420,425,113,23,249,201,260,251,427,2,3,18,17,56])). % 119.03/119.03 cnf(453,plain, % 119.03/119.03 (~E(f7(a10,a10),a11)), % 119.03/119.03 inference(scs_inference,[],[34,438,439,426,201,180,260,437,2,18,17,56,7])). % 119.03/119.03 cnf(454,plain, % 119.03/119.03 (~E(f7(a10,a10),f3(a11,f7(a11,a11)))), % 119.03/119.03 inference(scs_inference,[],[34,438,439,426,201,243,180,260,437,2,18,17,56,7,3])). % 119.03/119.03 cnf(497,plain, % 119.03/119.03 (P3(f7(f7(a10,a10),f7(a10,a10)),x4971)+~E(f7(f7(a10,a10),f7(a10,a10)),x4971)), % 119.03/119.03 inference(scs_inference,[],[357,18])). % 119.03/119.03 cnf(524,plain, % 119.03/119.03 (P3(x5241,f7(f7(a10,a10),f7(a10,a10)))+~E(f7(f7(a10,a10),f7(a10,a10)),x5241)), % 119.03/119.03 inference(scs_inference,[],[357,17])). % 119.03/119.03 cnf(584,plain, % 119.03/119.03 (E(f4(a1,f7(a10,a10)),a1)), % 119.03/119.03 inference(scs_inference,[],[400,35,393])). % 119.03/119.03 cnf(586,plain, % 119.03/119.03 (E(f7(a1,a1),f4(a1,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[113,584,2,3])). % 119.03/119.03 cnf(587,plain, % 119.03/119.03 (P1(f4(a1,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[113,584,23,2,3,16])). % 119.03/119.03 cnf(590,plain, % 119.03/119.03 (P2(a1,a1)), % 119.03/119.03 inference(scs_inference,[],[113,584,23,312,2,3,16,49,54])). % 119.03/119.03 cnf(592,plain, % 119.03/119.03 (P3(f4(a1,f7(a10,a10)),a1)), % 119.03/119.03 inference(scs_inference,[],[113,584,23,312,2,3,16,49,54,106])). % 119.03/119.03 cnf(593,plain, % 119.03/119.03 (P2(f7(f7(a1,a1),f7(a1,a1)),a1)), % 119.03/119.03 inference(scs_inference,[],[113,584,23,312,201,2,3,16,49,54,106,19])). % 119.03/119.03 cnf(594,plain, % 119.03/119.03 (P2(a1,f7(f7(a1,a1),f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[113,584,23,312,201,2,3,16,49,54,106,19,20])). % 119.03/119.03 cnf(595,plain, % 119.03/119.03 (P3(f4(a1,f7(a10,a10)),f7(f7(a1,a1),f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[113,584,23,312,201,2,3,16,49,54,106,19,20,18])). % 119.03/119.03 cnf(596,plain, % 119.03/119.03 (P3(a1,f4(a1,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[113,584,23,312,201,2,3,16,49,54,106,19,20,18,17])). % 119.03/119.03 cnf(602,plain, % 119.03/119.03 (E(f3(a1,f7(a1,a1)),f4(a1,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[249,201,586,594,2,19,3])). % 119.03/119.03 cnf(604,plain, % 119.03/119.03 (P2(a1,f7(a1,a1))), % 119.03/119.03 inference(scs_inference,[],[596,102,23,312,249,201,586,594,2,19,3,17,54])). % 119.03/119.03 cnf(606,plain, % 119.03/119.03 (E(f7(f7(a1,a1),f7(a1,a1)),f4(a1,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[595,596,102,23,312,249,201,180,586,587,594,2,19,3,17,54,56])). % 119.03/119.03 cnf(615,plain, % 119.03/119.03 (E(f4(a1,f7(a10,a10)),f7(f7(a1,a1),f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[606,2])). % 119.03/119.03 cnf(617,plain, % 119.03/119.03 (P2(a1,f3(a1,f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[23,312,201,153,606,602,604,2,19,54])). % 119.03/119.03 cnf(623,plain, % 119.03/119.03 (P2(f7(f7(a1,a1),f7(a1,a1)),f3(a1,f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[201,602,617,2,19])). % 119.03/119.03 cnf(679,plain, % 119.03/119.03 (E(f4(f7(a10,a10),a1),a1)), % 119.03/119.03 inference(scs_inference,[],[400,36,393])). % 119.03/119.03 cnf(681,plain, % 119.03/119.03 (E(f7(a1,a1),f4(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[113,679,2,3])). % 119.03/119.03 cnf(682,plain, % 119.03/119.03 (P1(f4(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[113,679,23,2,3,16])). % 119.03/119.03 cnf(685,plain, % 119.03/119.03 (P2(f7(a10,a10),a1)), % 119.03/119.03 inference(scs_inference,[],[113,679,23,312,2,3,16,49,54])). % 119.03/119.03 cnf(687,plain, % 119.03/119.03 (P3(f4(f7(a10,a10),a1),a1)), % 119.03/119.03 inference(scs_inference,[],[113,679,23,312,2,3,16,49,54,106])). % 119.03/119.03 cnf(689,plain, % 119.03/119.03 (P2(f7(a10,a10),f7(f7(a1,a1),f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[113,679,23,312,201,400,2,3,16,49,54,106,19,20])). % 119.03/119.03 cnf(690,plain, % 119.03/119.03 (P3(f4(f7(a10,a10),a1),f7(f7(a1,a1),f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[113,679,23,312,201,400,2,3,16,49,54,106,19,20,18])). % 119.03/119.03 cnf(691,plain, % 119.03/119.03 (P3(a1,f4(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[113,679,23,312,201,400,2,3,16,49,54,106,19,20,18,17])). % 119.03/119.03 cnf(695,plain, % 119.03/119.03 (E(f4(f7(a10,a10),a1),f7(a1,a1))), % 119.03/119.03 inference(scs_inference,[],[681,2])). % 119.03/119.03 cnf(696,plain, % 119.03/119.03 (E(f3(a1,f7(a1,a1)),f4(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[249,681,2,3])). % 119.03/119.03 cnf(698,plain, % 119.03/119.03 (P2(f7(a10,a10),f7(a1,a1))), % 119.03/119.03 inference(scs_inference,[],[691,102,23,312,249,201,681,2,3,17,54])). % 119.03/119.03 cnf(700,plain, % 119.03/119.03 (E(f7(f7(a1,a1),f7(a1,a1)),f4(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[690,691,102,23,312,249,201,180,681,682,2,3,17,54,56])). % 119.03/119.03 cnf(711,plain, % 119.03/119.03 (E(f4(f7(a10,a10),a1),f7(f7(a1,a1),f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[700,2])). % 119.03/119.03 cnf(712,plain, % 119.03/119.03 (P2(f7(a10,a10),f3(a1,f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[23,312,153,700,696,2,54])). % 119.03/119.03 cnf(719,plain, % 119.03/119.03 (E(f4(f7(a10,a10),a1),f3(a1,f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[696,2])). % 119.03/119.03 cnf(775,plain, % 119.03/119.03 (E(f3(a1,f7(a10,a10)),f7(a10,a10))), % 119.03/119.03 inference(scs_inference,[],[400,37,393])). % 119.03/119.03 cnf(777,plain, % 119.03/119.03 (P1(f3(a1,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[775,312,2,16])). % 119.03/119.03 cnf(780,plain, % 119.03/119.03 (P3(a1,f7(a10,a10))), % 119.03/119.03 inference(scs_inference,[],[775,23,312,2,16,49,55])). % 119.03/119.03 cnf(782,plain, % 119.03/119.03 (E(f7(a10,a10),f7(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[775,23,312,2,16,49,55,71])). % 119.03/119.03 cnf(784,plain, % 119.03/119.03 (E(f3(a1,f7(a10,a10)),f7(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[775,23,312,2,16,49,55,71,3])). % 119.03/119.03 cnf(785,plain, % 119.03/119.03 (P3(f3(a1,f7(a10,a10)),f7(a10,a10))), % 119.03/119.03 inference(scs_inference,[],[775,23,312,2,16,49,55,71,3,18])). % 119.03/119.03 cnf(786,plain, % 119.03/119.03 (P3(f7(a10,a10),f3(a1,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[775,23,312,2,16,49,55,71,3,18,17])). % 119.03/119.03 cnf(792,plain, % 119.03/119.03 (E(f7(f7(a10,a10),a1),f7(a10,a10))), % 119.03/119.03 inference(scs_inference,[],[782,2])). % 119.03/119.03 cnf(793,plain, % 119.03/119.03 (P1(f7(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[312,782,2,16])). % 119.03/119.03 cnf(796,plain, % 119.03/119.03 (P3(f7(f7(a10,a10),a1),f7(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[780,312,201,400,782,2,16,18,17,49])). % 119.03/119.03 cnf(798,plain, % 119.03/119.03 (P3(a1,f7(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[780,23,312,201,400,782,784,2,16,18,17,49,55])). % 119.03/119.03 cnf(800,plain, % 119.03/119.03 (E(f7(a10,a10),f7(f7(f7(a10,a10),a1),a1))), % 119.03/119.03 inference(scs_inference,[],[780,23,312,201,400,782,784,2,16,18,17,49,55,71])). % 119.03/119.03 cnf(807,plain, % 119.03/119.03 (E(f7(f7(a10,a10),a1),f3(a1,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[784,2])). % 119.03/119.03 cnf(810,plain, % 119.03/119.03 (P3(f7(a10,a10),f7(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[796,312,784,792,800,2,16,18,17])). % 119.03/119.03 cnf(817,plain, % 119.03/119.03 (P3(a1,f3(a1,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[798,807,800,2,18])). % 119.03/119.03 cnf(866,plain, % 119.03/119.03 (E(f4(a8,f7(a10,a10)),f7(a10,a10))), % 119.03/119.03 inference(scs_inference,[],[400,38,393])). % 119.03/119.03 cnf(867,plain, % 119.03/119.03 (E(f7(a10,a10),f4(a8,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[866,2])). % 119.03/119.03 cnf(868,plain, % 119.03/119.03 (E(f3(a1,f7(a10,a10)),f4(a8,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[775,866,2,3])). % 119.03/119.03 cnf(869,plain, % 119.03/119.03 (P1(f4(a8,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[775,866,312,2,3,16])). % 119.03/119.03 cnf(872,plain, % 119.03/119.03 (P2(a8,f7(a10,a10))), % 119.03/119.03 inference(scs_inference,[],[775,866,24,312,2,3,16,49,54])). % 119.03/119.03 cnf(874,plain, % 119.03/119.03 (P3(a1,f4(a8,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[775,866,24,23,312,2,3,16,49,54,55])). % 119.03/119.03 cnf(876,plain, % 119.03/119.03 (E(f7(a10,a10),f7(f4(a8,f7(a10,a10)),a1))), % 119.03/119.03 inference(scs_inference,[],[775,866,24,23,312,2,3,16,49,54,55,71])). % 119.03/119.03 cnf(880,plain, % 119.03/119.03 (P3(f4(a8,f7(a10,a10)),f7(a10,a10))), % 119.03/119.03 inference(scs_inference,[],[775,866,24,23,312,258,400,2,3,16,49,54,55,71,19,20,18])). % 119.03/119.03 cnf(881,plain, % 119.03/119.03 (P3(f7(a10,a10),f4(a8,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[775,866,24,23,312,258,400,2,3,16,49,54,55,71,19,20,18,17])). % 119.03/119.03 cnf(890,plain, % 119.03/119.03 (P2(a8,f3(a1,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[874,24,312,201,777,876,868,2,16,17,54])). % 119.03/119.03 cnf(968,plain, % 119.03/119.03 (E(f3(f7(a10,a10),a1),f7(a10,a10))), % 119.03/119.03 inference(scs_inference,[],[400,39,393])). % 119.03/119.03 cnf(969,plain, % 119.03/119.03 (E(f7(a10,a10),f3(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[968,2])). % 119.03/119.03 cnf(970,plain, % 119.03/119.03 (E(f3(a1,f7(a10,a10)),f3(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[775,968,2,3])). % 119.03/119.03 cnf(971,plain, % 119.03/119.03 (P1(f3(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[775,968,312,2,3,16])). % 119.03/119.03 cnf(974,plain, % 119.03/119.03 (P3(a1,f3(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[775,968,23,312,2,3,16,49,55])). % 119.03/119.03 cnf(976,plain, % 119.03/119.03 (E(a1,f7(f7(a10,a10),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[334,775,968,23,312,2,3,16,49,55,71])). % 119.03/119.03 cnf(978,plain, % 119.03/119.03 (P3(f7(f7(a10,a10),f7(a10,a10)),a1)), % 119.03/119.03 inference(scs_inference,[],[334,775,968,23,312,2,3,16,49,55,71,106])). % 119.03/119.03 cnf(979,plain, % 119.03/119.03 (P3(f3(f7(a10,a10),a1),f7(a10,a10))), % 119.03/119.03 inference(scs_inference,[],[334,775,968,23,312,2,3,16,49,55,71,106,18])). % 119.03/119.03 cnf(980,plain, % 119.03/119.03 (P3(f7(a10,a10),f3(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[334,775,968,23,312,2,3,16,49,55,71,106,18,17])). % 119.03/119.03 cnf(986,plain, % 119.03/119.03 (E(f3(f7(a10,a10),a1),f3(a1,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[970,2])). % 119.03/119.03 cnf(987,plain, % 119.03/119.03 (E(f7(a1,a1),f7(f7(a10,a10),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[113,970,976,2,3])). % 119.03/119.03 cnf(988,plain, % 119.03/119.03 (P3(f7(f7(a10,a10),f7(a10,a10)),f7(f7(a1,a1),f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[978,113,201,970,976,2,3,18])). % 119.03/119.03 cnf(990,plain, % 119.03/119.03 (E(f7(a10,a10),f7(f3(f7(a10,a10),a1),a1))), % 119.03/119.03 inference(scs_inference,[],[978,974,113,23,312,201,970,971,976,2,3,18,17,71])). % 119.03/119.03 cnf(995,plain, % 119.03/119.03 (E(f7(f7(a1,a1),f7(a1,a1)),f7(f7(a10,a10),f7(a10,a10)))+~P3(a1,f7(f7(a10,a10),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[206,978,974,113,23,312,201,180,338,970,971,976,2,3,18,17,71,16,56,69])). % 119.03/119.03 cnf(998,plain, % 119.03/119.03 (E(f7(f7(a10,a10),f7(a10,a10)),a1)), % 119.03/119.03 inference(scs_inference,[],[976,2])). % 119.03/119.03 cnf(999,plain, % 119.03/119.03 (E(f3(a1,f7(a1,a1)),f7(f7(a10,a10),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[249,976,987,2,3])). % 119.03/119.03 cnf(1000,plain, % 119.03/119.03 (P3(a1,f7(f7(a10,a10),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[357,249,976,987,2,3,17])). % 119.03/119.03 cnf(1001,plain, % 119.03/119.03 (E(a1,f7(f3(a1,f7(a10,a10)),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[357,786,23,312,249,777,976,987,986,2,3,17,71])). % 119.03/119.03 cnf(1004,plain, % 119.03/119.03 (P3(f7(f3(a1,f7(a10,a10)),f7(a10,a10)),a1)), % 119.03/119.03 inference(scs_inference,[],[357,786,23,312,249,777,976,987,986,2,3,17,71,995,106])). % 119.03/119.03 cnf(1005,plain, % 119.03/119.03 (P1(f7(f3(a1,f7(a10,a10)),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[357,786,23,312,249,777,976,987,986,2,3,17,71,995,106,16])). % 119.03/119.03 cnf(1006,plain, % 119.03/119.03 (P3(f7(f3(a1,f7(a10,a10)),f7(a10,a10)),f7(f7(a1,a1),f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[357,786,23,312,201,249,777,976,987,986,2,3,17,71,995,106,16,18])). % 119.03/119.03 cnf(1013,plain, % 119.03/119.03 (E(f7(a1,a1),f7(f3(a1,f7(a10,a10)),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[113,999,1001,2,3])). % 119.03/119.03 cnf(1019,plain, % 119.03/119.03 (P3(f7(f7(a10,a10),f7(a10,a10)),f3(a1,f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[988,1000,113,102,23,201,180,338,999,1001,2,3,17,56,71,497])). % 119.03/119.03 cnf(1020,plain, % 119.03/119.03 (P3(f3(a1,f7(a1,a1)),f7(f7(a10,a10),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[988,1000,113,102,23,201,180,338,999,1001,2,3,17,56,71,497,524])). % 119.03/119.03 cnf(1028,plain, % 119.03/119.03 (E(f3(a1,f7(a1,a1)),f7(f3(a1,f7(a10,a10)),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[249,1001,1013,2,3])). % 119.03/119.03 cnf(1030,plain, % 119.03/119.03 (P3(a1,f7(f3(a1,f7(a10,a10)),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[1020,102,23,249,1001,1013,1005,2,3,17,55])). % 119.03/119.03 cnf(1044,plain, % 119.03/119.03 (P3(f7(f7(a1,a1),f7(a1,a1)),f7(f3(a1,f7(a10,a10)),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[1030,201,990,2,17])). % 119.03/119.03 cnf(1053,plain, % 119.03/119.03 (P2(a8,a1)), % 119.03/119.03 inference(scs_inference,[],[23,1044,1006,180,24,312,685,872,1028,1005,2,56,70])). % 119.03/119.03 cnf(1056,plain, % 119.03/119.03 (P2(f3(a8,f7(a8,a8)),a1)), % 119.03/119.03 inference(scs_inference,[],[23,1044,1006,201,258,180,24,312,685,872,1028,1005,2,56,70,20,19])). % 119.03/119.03 cnf(1125,plain, % 119.03/119.03 (E(f7(f7(a10,a10),a1),f4(a8,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[866,782,3,2])). % 119.03/119.03 cnf(1126,plain, % 119.03/119.03 (P2(a8,f7(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[866,24,312,782,793,3,2,54])). % 119.03/119.03 cnf(1136,plain, % 119.03/119.03 (E(f3(f7(a10,a10),a1),f4(a8,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[866,258,969,1126,3,19,2])). % 119.03/119.03 cnf(1137,plain, % 119.03/119.03 (P2(a8,f3(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[866,258,24,312,971,969,1126,3,19,2,54])). % 119.03/119.03 cnf(1139,plain, % 119.03/119.03 (E(a1,f7(f4(a8,f7(a10,a10)),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[23,881,866,258,24,312,869,971,969,1126,3,19,2,54,71])). % 119.03/119.03 cnf(1146,plain, % 119.03/119.03 (P3(f7(f4(a8,f7(a10,a10)),f7(a10,a10)),a1)), % 119.03/119.03 inference(scs_inference,[],[1139,106])). % 119.03/119.03 cnf(1148,plain, % 119.03/119.03 (E(f7(a1,a1),f7(f4(a8,f7(a10,a10)),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[113,1139,106,2,3])). % 119.03/119.03 cnf(1151,plain, % 119.03/119.03 (P1(f7(f4(a8,f7(a10,a10)),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[23,113,201,258,1139,1137,106,2,3,18,19,16])). % 119.03/119.03 cnf(1158,plain, % 119.03/119.03 (E(f3(a1,f7(a1,a1)),f7(f4(a8,f7(a10,a10)),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[249,1148,2,3])). % 119.03/119.03 cnf(1159,plain, % 119.03/119.03 (P3(a1,f7(f4(a8,f7(a10,a10)),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[23,249,102,1148,1151,2,3,55])). % 119.03/119.03 cnf(1320,plain, % 119.03/119.03 (E(a8,a1)+E(f7(a10,a10),f2(f3(a1,f7(a10,a10)),a8))), % 119.03/119.03 inference(scs_inference,[],[24,312,777,868,890,72])). % 119.03/119.03 cnf(1327,plain, % 119.03/119.03 (E(a8,a1)+E(f7(a10,a10),f2(f7(a10,a10),a8))), % 119.03/119.03 inference(scs_inference,[],[24,312,867,872,72])). % 119.03/119.03 cnf(1334,plain, % 119.03/119.03 (E(a8,a1)+E(f7(a10,a10),f2(f3(f7(a10,a10),a1),a8))), % 119.03/119.03 inference(scs_inference,[],[24,312,971,1136,1137,72])). % 119.03/119.03 cnf(1341,plain, % 119.03/119.03 (E(a8,a1)+E(f7(a10,a10),f2(f7(f7(a10,a10),a1),a8))), % 119.03/119.03 inference(scs_inference,[],[24,312,793,1126,1125,72])). % 119.03/119.03 cnf(1380,plain, % 119.03/119.03 (E(f4(f7(a10,a10),a8),f7(a10,a10))), % 119.03/119.03 inference(scs_inference,[],[400,40,393])). % 119.03/119.03 cnf(1381,plain, % 119.03/119.03 (E(f7(a10,a10),f4(f7(a10,a10),a8))), % 119.03/119.03 inference(scs_inference,[],[1380,2])). % 119.03/119.03 cnf(1382,plain, % 119.03/119.03 (E(f3(a1,f7(a10,a10)),f4(f7(a10,a10),a8))), % 119.03/119.03 inference(scs_inference,[],[775,1380,2,3])). % 119.03/119.03 cnf(1383,plain, % 119.03/119.03 (P1(f4(f7(a10,a10),a8))), % 119.03/119.03 inference(scs_inference,[],[775,1380,312,2,3,16])). % 119.03/119.03 cnf(1386,plain, % 119.03/119.03 (P2(f7(a10,a10),f7(a10,a10))), % 119.03/119.03 inference(scs_inference,[],[775,1380,24,312,2,3,16,49,54])). % 119.03/119.03 cnf(1388,plain, % 119.03/119.03 (P3(a1,f4(f7(a10,a10),a8))), % 119.03/119.03 inference(scs_inference,[],[23,775,1380,24,312,2,3,16,49,54,55])). % 119.03/119.03 cnf(1390,plain, % 119.03/119.03 (E(f7(a10,a10),f7(f4(f7(a10,a10),a8),a1))), % 119.03/119.03 inference(scs_inference,[],[23,775,1380,24,312,2,3,16,49,54,55,71])). % 119.03/119.03 cnf(1392,plain, % 119.03/119.03 (P2(f3(f7(a10,a10),f7(f7(a10,a10),f7(a10,a10))),f7(a10,a10))), % 119.03/119.03 inference(scs_inference,[],[23,775,1380,24,312,400,2,3,16,49,54,55,71,19])). % 119.03/119.03 cnf(1393,plain, % 119.03/119.03 (P3(f7(a10,a10),f4(f7(a10,a10),a8))), % 119.03/119.03 inference(scs_inference,[],[23,775,1380,24,312,400,2,3,16,49,54,55,71,19,17])). % 119.03/119.03 cnf(1394,plain, % 119.03/119.03 (P3(f4(f7(a10,a10),a8),f7(a10,a10))), % 119.03/119.03 inference(scs_inference,[],[23,775,1380,24,312,400,2,3,16,49,54,55,71,19,17,18])). % 119.03/119.03 cnf(1410,plain, % 119.03/119.03 (P2(f7(a10,a10),f3(a1,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[1388,24,312,201,777,1390,1382,2,17,16,54])). % 119.03/119.03 cnf(1422,plain, % 119.03/119.03 (E(a1,f7(f7(f7(a10,a10),a1),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[23,810,968,312,793,782,3,71])). % 119.03/119.03 cnf(1424,plain, % 119.03/119.03 (P3(f7(f7(f7(a10,a10),a1),f7(a10,a10)),a1)), % 119.03/119.03 inference(scs_inference,[],[23,810,968,312,793,782,3,71,106])). % 119.03/119.03 cnf(1427,plain, % 119.03/119.03 (P3(f7(f7(f7(a10,a10),a1),f7(a10,a10)),f7(f7(a1,a1),f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[23,810,968,312,201,793,782,3,71,106,2,17,18])). % 119.03/119.03 cnf(1428,plain, % 119.03/119.03 (P1(f7(f7(f7(a10,a10),a1),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[23,810,968,312,201,793,782,3,71,106,2,17,18,16])). % 119.03/119.03 cnf(1441,plain, % 119.03/119.03 (E(f3(f7(a10,a10),a1),f4(f7(a10,a10),a8))), % 119.03/119.03 inference(scs_inference,[],[968,1381,1422,2,3])). % 119.03/119.03 cnf(1442,plain, % 119.03/119.03 (P2(f7(a10,a10),f3(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[968,24,312,971,1381,1422,2,3,54])). % 119.03/119.03 cnf(1444,plain, % 119.03/119.03 (E(a1,f7(f4(f7(a10,a10),a8),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[23,1393,968,24,312,971,1383,1381,1422,2,3,54,71])). % 119.03/119.03 cnf(1446,plain, % 119.03/119.03 (P3(f7(f4(f7(a10,a10),a8),f7(a10,a10)),a1)), % 119.03/119.03 inference(scs_inference,[],[23,1393,968,24,312,971,1383,1381,1422,2,3,54,71,106])). % 119.03/119.03 cnf(1449,plain, % 119.03/119.03 (P1(f7(f4(f7(a10,a10),a8),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[23,1393,968,24,312,201,971,1383,1381,1422,2,3,54,71,106,17,18,16])). % 119.03/119.03 cnf(1462,plain, % 119.03/119.03 (E(f7(a1,a1),f7(f7(f7(a10,a10),a1),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[113,1422,1441,2,3])). % 119.03/119.03 cnf(1469,plain, % 119.03/119.03 (E(f7(a1,a1),f7(f4(f7(a10,a10),a8),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[113,1444,2,3])). % 119.03/119.03 cnf(1476,plain, % 119.03/119.03 (E(f3(a1,f7(a1,a1)),f7(f7(f7(a10,a10),a1),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[249,1462,2,3])). % 119.03/119.03 cnf(1477,plain, % 119.03/119.03 (P3(a1,f7(f7(f7(a10,a10),a1),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[23,102,249,1462,1428,2,3,55])). % 119.03/119.03 cnf(1479,plain, % 119.03/119.03 (P3(f7(f7(a1,a1),f7(a1,a1)),f7(f7(f7(a10,a10),a1),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[23,102,201,249,1462,1428,2,3,55,17])). % 119.03/119.03 cnf(1491,plain, % 119.03/119.03 (E(f7(f4(f7(a10,a10),a8),f7(a10,a10)),f7(a1,a1))), % 119.03/119.03 inference(scs_inference,[],[1469,2])). % 119.03/119.03 cnf(1492,plain, % 119.03/119.03 (E(f3(a1,f7(a1,a1)),f7(f4(f7(a10,a10),a8),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[249,1469,2,3])). % 119.03/119.03 cnf(1495,plain, % 119.03/119.03 (E(f7(f7(f7(a10,a10),a1),f7(a10,a10)),f7(f7(a1,a1),f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[23,1427,1479,102,249,180,1469,1449,1428,2,3,55,56])). % 119.03/119.03 cnf(1542,plain, % 119.03/119.03 (P3(f7(f7(a1,a1),a1),f7(a10,a10))), % 119.03/119.03 inference(scs_inference,[],[780,440,17])). % 119.03/119.03 cnf(1545,plain, % 119.03/119.03 (P2(f7(f7(a1,a1),a1),f7(a1,a1))), % 119.03/119.03 inference(scs_inference,[],[780,160,440,604,593,17,18,20,19])). % 119.03/119.03 cnf(1552,plain, % 119.03/119.03 (P3(f7(a1,f7(a1,a1)),f7(f7(a1,a1),a1))), % 119.03/119.03 inference(scs_inference,[],[817,238,440,17,18])). % 119.03/119.03 cnf(1553,plain, % 119.03/119.03 (P2(f7(f7(a1,a1),a1),f3(a1,f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[817,238,440,617,17,18,19])). % 119.03/119.03 cnf(1554,plain, % 119.03/119.03 (P2(a1,f7(f7(a1,a1),a1))), % 119.03/119.03 inference(scs_inference,[],[817,238,440,617,590,17,18,19,20])). % 119.03/119.03 cnf(1561,plain, % 119.03/119.03 (P3(f4(a1,f7(a10,a10)),f7(f7(a1,a1),a1))), % 119.03/119.03 inference(scs_inference,[],[798,592,440,17,18])). % 119.03/119.03 cnf(1562,plain, % 119.03/119.03 (P2(f7(a10,a10),f7(f7(a1,a1),a1))), % 119.03/119.03 inference(scs_inference,[],[798,592,440,685,17,18,20])). % 119.03/119.03 cnf(1563,plain, % 119.03/119.03 (P2(f7(f7(a1,a1),a1),a1)), % 119.03/119.03 inference(scs_inference,[],[798,592,440,590,685,17,18,20,19])). % 119.03/119.03 cnf(1568,plain, % 119.03/119.03 (P3(f4(f7(a10,a10),a1),f7(f7(a1,a1),a1))), % 119.03/119.03 inference(scs_inference,[],[874,687,440,17,18])). % 119.03/119.03 cnf(1569,plain, % 119.03/119.03 (P2(f7(f7(a1,a1),a1),f7(f7(a1,a1),f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[874,687,440,594,17,18,19])). % 119.03/119.03 cnf(1577,plain, % 119.03/119.03 (P3(f7(f7(a10,a10),f7(a10,a10)),f7(f7(a1,a1),a1))), % 119.03/119.03 inference(scs_inference,[],[974,978,440,17,18])). % 119.03/119.03 cnf(1578,plain, % 119.03/119.03 (P2(f3(a8,f7(a8,a8)),f7(f7(a1,a1),a1))), % 119.03/119.03 inference(scs_inference,[],[974,978,440,1056,17,18,20])). % 119.03/119.03 cnf(1579,plain, % 119.03/119.03 (P2(f7(a1,a1),f7(a1,a1))), % 119.03/119.03 inference(scs_inference,[],[974,978,440,408,1056,1545,17,18,20,19])). % 119.03/119.03 cnf(1586,plain, % 119.03/119.03 (P2(f7(a1,a1),f3(a1,f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[203,440,408,1553,17,19])). % 119.03/119.03 cnf(1587,plain, % 119.03/119.03 (P3(f7(f3(a1,f7(a10,a10)),f7(a10,a10)),f7(f7(a1,a1),a1))), % 119.03/119.03 inference(scs_inference,[],[203,1004,440,408,1553,17,19,18])). % 119.03/119.03 cnf(1588,plain, % 119.03/119.03 (P2(f7(a1,a1),a1)), % 119.03/119.03 inference(scs_inference,[],[203,1004,113,440,408,1579,1553,17,19,18,20])). % 119.03/119.03 cnf(1593,plain, % 119.03/119.03 (P2(f3(a8,f7(a8,a8)),f7(a1,a1))), % 119.03/119.03 inference(scs_inference,[],[307,440,408,1578,17,20])). % 119.03/119.03 cnf(1594,plain, % 119.03/119.03 (P3(f7(f4(a8,f7(a10,a10)),f7(a10,a10)),f7(f7(a1,a1),a1))), % 119.03/119.03 inference(scs_inference,[],[307,1146,440,408,1578,17,20,18])). % 119.03/119.03 cnf(1596,plain, % 119.03/119.03 (E(f7(f7(a1,a1),a1),f7(a1,f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[307,1146,1552,440,187,260,408,1569,1578,17,20,18,19,56])). % 119.03/119.03 cnf(1603,plain, % 119.03/119.03 (P3(f7(f7(a1,a1),a1),f4(a1,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[596,440,17])). % 119.03/119.03 cnf(1604,plain, % 119.03/119.03 (P2(a8,f7(a1,a1))), % 119.03/119.03 inference(scs_inference,[],[596,440,154,1593,17,19])). % 119.03/119.03 cnf(1606,plain, % 119.03/119.03 (P3(f7(f7(f7(a10,a10),a1),f7(a10,a10)),f7(f7(a1,a1),a1))), % 119.03/119.03 inference(scs_inference,[],[596,1424,440,154,1593,1563,17,19,20,18])). % 119.03/119.03 cnf(1607,plain, % 119.03/119.03 (E(f7(f7(a1,a1),a1),f4(a1,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[596,1424,1561,440,260,154,587,1593,1563,17,19,20,18,56])). % 119.03/119.03 cnf(1615,plain, % 119.03/119.03 (P3(f7(f4(f7(a10,a10),a8),f7(a10,a10)),f7(f7(a1,a1),a1))), % 119.03/119.03 inference(scs_inference,[],[691,1446,440,17,18])). % 119.03/119.03 cnf(1617,plain, % 119.03/119.03 (E(f7(f7(a1,a1),a1),f4(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[691,1446,1568,440,260,682,1588,17,18,20,56])). % 119.03/119.03 cnf(1634,plain, % 119.03/119.03 (E(f7(f7(a1,a1),a1),f7(f3(a1,f7(a10,a10)),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[1030,1594,1587,440,260,408,1005,17,18,56])). % 119.03/119.03 cnf(1646,plain, % 119.03/119.03 (E(f7(f7(a10,a10),f7(a10,a10)),f7(f7(a1,a1),a1))), % 119.03/119.03 inference(scs_inference,[],[1000,1606,1577,440,260,338,408,17,18,56,2])). % 119.03/119.03 cnf(1654,plain, % 119.03/119.03 (E(f7(f7(a1,a1),a1),f7(f4(a8,f7(a10,a10)),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[1159,1615,1594,440,260,408,1151,17,18,56])). % 119.03/119.03 cnf(1662,plain, % 119.03/119.03 (P3(f7(a1,a1),f7(a10,a10))), % 119.03/119.03 inference(scs_inference,[],[1542,408,17])). % 119.03/119.03 cnf(1677,plain, % 119.03/119.03 (P3(f4(a1,f7(a10,a10)),f7(a1,a1))), % 119.03/119.03 inference(scs_inference,[],[1477,1561,440,408,17,18])). % 119.03/119.03 cnf(1678,plain, % 119.03/119.03 (E(f7(f7(a1,a1),a1),f7(f7(f7(a10,a10),a1),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[1477,1606,1561,440,260,408,1428,17,18,56])). % 119.03/119.03 cnf(1720,plain, % 119.03/119.03 (P3(f7(a1,a1),f4(a1,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[1603,408,17])). % 119.03/119.03 cnf(2156,plain, % 119.03/119.03 (P3(f7(f7(f7(a10,a10),a1),f7(a10,a10)),f3(a1,f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[203,1422,17])). % 119.03/119.03 cnf(2161,plain, % 119.03/119.03 (E(f7(f3(a1,f7(a10,a10)),f7(a10,a10)),f4(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[160,203,719,604,617,1028,1422,17,19,3,18,20,2])). % 119.03/119.03 cnf(2162,plain, % 119.03/119.03 (P2(f7(a10,a10),f7(f3(a1,f7(a10,a10)),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[160,203,719,604,617,1028,1422,23,312,1005,17,19,3,18,20,2,54])). % 119.03/119.03 cnf(2173,plain, % 119.03/119.03 (E(f7(a1,f7(a1,a1)),f7(f7(f7(a10,a10),a1),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[238,307,623,617,1028,1422,1491,987,187,1428,17,19,3,18,20,56])). % 119.03/119.03 cnf(2182,plain, % 119.03/119.03 (E(f7(f7(f7(a10,a10),a1),f7(a10,a10)),f7(a1,f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[2173,2])). % 119.03/119.03 cnf(2184,plain, % 119.03/119.03 (E(f4(f7(a10,a10),a1),f7(f4(a8,f7(a10,a10)),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[1388,719,1422,1158,2173,2,17,3])). % 119.03/119.03 cnf(2185,plain, % 119.03/119.03 (P3(f3(a1,f7(a1,a1)),f7(f3(a1,f7(a10,a10)),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[1388,193,719,1028,1422,1158,2173,2,17,3,18])). % 119.03/119.03 cnf(2186,plain, % 119.03/119.03 (P2(f7(f7(a10,a10),a1),f7(a1,a1))), % 119.03/119.03 inference(scs_inference,[],[1388,193,782,719,698,1028,1422,1158,2173,2,17,3,18,19])). % 119.03/119.03 cnf(2195,plain, % 119.03/119.03 (P3(f7(a1,f7(a1,a1)),f3(a1,f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[193,213,429,1028,2184,2,17,18])). % 119.03/119.03 cnf(2196,plain, % 119.03/119.03 (E(f4(a8,f7(a10,a10)),f4(f7(a10,a10),a8))), % 119.03/119.03 inference(scs_inference,[],[193,213,866,429,1028,1381,2184,2,17,18,3])). % 119.03/119.03 cnf(2197,plain, % 119.03/119.03 (P2(f7(f7(f7(a10,a10),a1),f7(a10,a10)),a1)), % 119.03/119.03 inference(scs_inference,[],[193,213,866,429,1028,1422,590,1381,2184,2,17,18,3,19])). % 119.03/119.03 cnf(2199,plain, % 119.03/119.03 (P2(f7(a10,a10),f7(f4(a8,f7(a10,a10)),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[193,213,866,429,1028,1422,590,23,312,1381,2184,1151,2,17,18,3,19,20,54])). % 119.03/119.03 cnf(2205,plain, % 119.03/119.03 (E(f4(f7(a10,a10),a1),f7(f7(f7(a10,a10),a1),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[719,1476,2196,2,3])). % 119.03/119.03 cnf(2206,plain, % 119.03/119.03 (P3(f4(a1,f7(a10,a10)),f7(f7(f7(a10,a10),a1),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[592,719,1422,1476,2196,2,3,18])). % 119.03/119.03 cnf(2215,plain, % 119.03/119.03 (E(f7(f7(f7(a10,a10),a1),f7(a10,a10)),f4(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[2205,2])). % 119.03/119.03 cnf(2217,plain, % 119.03/119.03 (P3(f3(a1,f7(a1,a1)),f7(a1,f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[213,687,429,1422,2205,2,18,17])). % 119.03/119.03 cnf(2218,plain, % 119.03/119.03 (P2(f7(f7(a10,a10),a1),a1)), % 119.03/119.03 inference(scs_inference,[],[213,687,782,429,1422,685,2205,2,18,17,19])). % 119.03/119.03 cnf(2219,plain, % 119.03/119.03 (E(f4(f7(a10,a10),a1),f7(f4(f7(a10,a10),a8),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[213,687,782,719,429,1422,685,1492,2205,2,18,17,19,3])). % 119.03/119.03 cnf(2231,plain, % 119.03/119.03 (E(f4(f7(a10,a10),a1),f7(a1,f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[817,782,719,1422,424,712,2219,2,17,19,3])). % 119.03/119.03 cnf(2232,plain, % 119.03/119.03 (P3(f3(a1,f7(a10,a10)),f7(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[817,785,782,719,1422,424,712,2219,2,17,19,3,18])). % 119.03/119.03 cnf(2234,plain, % 119.03/119.03 (P2(f7(a10,a10),f7(f4(f7(a10,a10),a8),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[817,785,782,719,1422,23,312,424,1056,712,2219,1449,2,17,19,3,18,20,54])). % 119.03/119.03 cnf(2241,plain, % 119.03/119.03 (E(f7(a1,f7(a1,a1)),f4(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[2231,2])). % 119.03/119.03 cnf(2242,plain, % 119.03/119.03 (P2(f7(f7(a10,a10),a1),f7(a10,a10))), % 119.03/119.03 inference(scs_inference,[],[782,1386,2231,2,19])). % 119.03/119.03 cnf(2243,plain, % 119.03/119.03 (E(f7(f7(a10,a10),f7(a10,a10)),f7(a1,f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[1646,782,1596,1386,2231,2,19,3])). % 119.03/119.03 cnf(2247,plain, % 119.03/119.03 (P2(f7(a10,a10),f7(a1,f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[798,880,1646,782,1422,23,312,1596,1386,187,2231,2,19,3,18,17,20,54])). % 119.03/119.03 cnf(2259,plain, % 119.03/119.03 (P3(f7(f7(f7(a10,a10),a1),f7(a10,a10)),f4(a1,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[596,979,1646,782,1422,1607,2243,2,3,18,17])). % 119.03/119.03 cnf(2262,plain, % 119.03/119.03 (E(f7(f7(f7(a10,a10),a1),f7(a10,a10)),f4(a1,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[596,979,2206,1646,782,1422,1028,1607,1554,1586,587,2243,1428,2,3,18,17,19,20,56])). % 119.03/119.03 cnf(2273,plain, % 119.03/119.03 (P3(f7(f7(a10,a10),f7(a10,a10)),f7(f7(f7(a10,a10),a1),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[978,1422,2262,2,18])). % 119.03/119.03 cnf(2275,plain, % 119.03/119.03 (P2(f7(f7(a10,a10),a1),f7(f7(a1,a1),f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[691,978,782,1422,689,2262,2,18,17,19])). % 119.03/119.03 cnf(2276,plain, % 119.03/119.03 (E(f7(f7(a10,a10),f7(a10,a10)),f4(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[691,978,1646,782,1422,1617,689,2262,2,18,17,19,3])). % 119.03/119.03 cnf(2293,plain, % 119.03/119.03 (E(f7(f7(a10,a10),f7(a10,a10)),f7(f3(a1,f7(a10,a10)),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[874,1019,1646,782,1422,1028,1634,1410,2276,2,17,19,18,3])). % 119.03/119.03 cnf(2296,plain, % 119.03/119.03 (~P3(f7(f7(f7(a10,a10),a1),f7(a10,a10)),f7(f7(a10,a10),f7(a10,a10)))+E(f7(f7(f7(a10,a10),a1),f7(a10,a10)),f7(f7(a10,a10),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[874,1019,2273,1646,782,1422,1028,1634,338,1553,1410,2276,1428,2,17,19,18,3,20,524,56])). % 119.03/119.03 cnf(2301,plain, % 119.03/119.03 (P3(f7(f7(a10,a10),a1),f3(a1,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[786,782,1442,2293,2,19,17])). % 119.03/119.03 cnf(2302,plain, % 119.03/119.03 (P3(f4(f7(a10,a10),a8),f7(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[786,1394,782,1442,2293,2,19,17,18])). % 119.03/119.03 cnf(2303,plain, % 119.03/119.03 (E(f7(f7(a10,a10),f7(a10,a10)),f7(f4(a8,f7(a10,a10)),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[786,1394,1646,782,1654,1442,2293,2,19,17,18,3])). % 119.03/119.03 cnf(2318,plain, % 119.03/119.03 (P3(f7(f7(f7(a10,a10),a1),f7(a10,a10)),f7(f7(a10,a10),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[881,2195,1646,782,1028,1678,1562,2242,2303,2,17,18,19,3,20,524])). % 119.03/119.03 cnf(2324,plain, % 119.03/119.03 (E(f7(f7(f7(a10,a10),a1),f7(a10,a10)),f7(f7(a10,a10),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[2318,2296])). % 119.03/119.03 cnf(2327,plain, % 119.03/119.03 (E(f4(f7(a10,a10),a1),f4(a1,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[980,782,719,602,2162,19,17,3])). % 119.03/119.03 cnf(2329,plain, % 119.03/119.03 (P2(a1,f4(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[980,782,719,1422,23,312,602,682,2162,2218,19,17,3,20,54])). % 119.03/119.03 cnf(2331,plain, % 119.03/119.03 (E(f4(a1,f7(a10,a10)),f4(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[980,782,719,1422,23,312,602,682,2162,2218,19,17,3,20,54,2])). % 119.03/119.03 cnf(2340,plain, % 119.03/119.03 (E(f7(a1,f7(a1,a1)),f7(f4(f7(a10,a10),a8),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[974,782,1422,1491,23,312,283,587,2199,2331,19,3,17,54,2])). % 119.03/119.03 cnf(2346,plain, % 119.03/119.03 (P3(f7(f7(a10,a10),a1),f4(f7(a10,a10),a8))), % 119.03/119.03 inference(scs_inference,[],[1393,782,17])). % 119.03/119.03 cnf(2348,plain, % 119.03/119.03 (E(f7(f4(f7(a10,a10),a8),f7(a10,a10)),f4(a1,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[1393,782,1491,586,2234,17,19,3])). % 119.03/119.03 cnf(2349,plain, % 119.03/119.03 (E(f7(f7(a10,a10),a1),f4(f7(a10,a10),a8))), % 119.03/119.03 inference(scs_inference,[],[1393,2302,782,1491,1383,586,793,2234,17,19,3,56])). % 119.03/119.03 cnf(2351,plain, % 119.03/119.03 (P2(a1,f7(f4(f7(a10,a10),a8),f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[1393,2302,782,1491,23,312,1383,586,793,2234,1449,17,19,3,56,54])). % 119.03/119.03 cnf(2361,plain, % 119.03/119.03 (P2(f7(f7(a10,a10),a1),f7(a1,f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[2217,782,1028,2247,2349,2,17,19])). % 119.03/119.03 cnf(2396,plain, % 119.03/119.03 (P2(f7(f7(f7(a10,a10),a1),f7(a10,a10)),f4(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[1422,2329,19])). % 119.03/119.03 cnf(2418,plain, % 119.03/119.03 (P2(f7(f7(a1,a1),f7(a1,a1)),f4(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[1495,2396,19])). % 119.03/119.03 cnf(2592,plain, % 119.03/119.03 (P2(f4(a8,f7(a10,a10)),f7(a1,a1))), % 119.03/119.03 inference(scs_inference,[],[2232,2301,1125,2186,18,17,19])). % 119.03/119.03 cnf(2607,plain, % 119.03/119.03 (P2(f4(a8,f7(a10,a10)),a1)), % 119.03/119.03 inference(scs_inference,[],[2302,2346,113,1125,2275,2592,18,17,19,20])). % 119.03/119.03 cnf(2648,plain, % 119.03/119.03 (P2(f4(a8,f7(a10,a10)),f7(a1,f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[1125,2361,19])). % 119.03/119.03 cnf(2805,plain, % 119.03/119.03 (~E(f3(a10,a11),a10)), % 119.03/119.03 inference(scs_inference,[],[401,695,407,1449,41,37,38,39,40,35,36,4,5,6,8,9,10,11,12,13,14,15,7,2])). % 119.03/119.03 cnf(2812,plain, % 119.03/119.03 (P2(f7(f7(a10,a10),f7(a10,a10)),a1)), % 119.03/119.03 inference(scs_inference,[],[34,401,202,2197,2324,695,219,407,308,1449,41,37,38,39,40,35,36,4,5,6,8,9,10,11,12,13,14,15,7,2,51,50,3,17,19])). % 119.03/119.03 cnf(2820,plain, % 119.03/119.03 (E(f3(f7(a1,a1),f5(f7(a1,a1),f7(a1,a1))),f7(a1,a1))), % 119.03/119.03 inference(scs_inference,[],[34,401,202,2351,2197,2418,2327,2324,695,219,1604,115,407,308,411,1449,102,24,23,41,37,38,39,40,35,36,4,5,6,8,9,10,11,12,13,14,15,7,2,51,50,3,17,19,20,59,60,67,68])). % 119.03/119.03 cnf(2830,plain, % 119.03/119.03 (P2(a1,f4(a1,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[34,401,202,2351,2197,2418,2327,2324,695,219,1604,115,407,308,411,1449,587,27,102,312,24,23,41,37,38,39,40,35,36,4,5,6,8,9,10,11,12,13,14,15,7,2,51,50,3,17,19,20,59,60,67,68,77,78,84,85,87])). % 119.03/119.03 cnf(2836,plain, % 119.03/119.03 (~P1(f3(a10,a11))), % 119.03/119.03 inference(scs_inference,[],[34,401,202,2351,2197,2418,2327,2324,695,418,219,1604,115,407,308,411,402,1449,587,27,102,26,312,24,23,41,37,38,39,40,35,36,4,5,6,8,9,10,11,12,13,14,15,7,2,51,50,3,17,19,20,59,60,67,68,77,78,84,85,87,43,89,88])). % 119.03/119.03 cnf(2857,plain, % 119.03/119.03 (E(f4(f7(a9,a9),a8),f7(a9,a9))), % 119.03/119.03 inference(scs_inference,[],[224,37,40])). % 119.03/119.03 cnf(2861,plain, % 119.03/119.03 (E(f3(f7(a9,a9),a1),f7(a9,a9))), % 119.03/119.03 inference(scs_inference,[],[291,224,37,40,36,39])). % 119.03/119.03 cnf(2869,plain, % 119.03/119.03 (E(f6(f7(f7(a10,a10),f7(a10,a10)),x28691),f6(a1,x28691))), % 119.03/119.03 inference(scs_inference,[],[998,291,224,37,40,36,39,8,35,5,12,4,14])). % 119.03/119.03 cnf(2871,plain, % 119.03/119.03 (E(f4(a8,f7(a9,a9)),f7(a9,a9))), % 119.03/119.03 inference(scs_inference,[],[998,291,224,37,40,36,39,8,35,5,12,4,14,15,38])). % 119.03/119.03 cnf(2879,plain, % 119.03/119.03 (E(f3(x28791,f7(f7(a10,a10),f7(a10,a10))),f3(x28791,a1))), % 119.03/119.03 inference(scs_inference,[],[998,291,224,37,40,36,39,8,35,5,12,4,14,15,38,11,6,13,117,9,10,7])). % 119.03/119.03 cnf(2880,plain, % 119.03/119.03 (~E(f3(a9,f7(a9,a9)),a1)), % 119.03/119.03 inference(scs_inference,[],[259,998,291,224,37,40,36,39,8,35,5,12,4,14,15,38,11,6,13,117,9,10,7,2])). % 119.03/119.03 cnf(2881,plain, % 119.03/119.03 (P1(f4(f7(a9,a9),f7(a9,a9)))), % 119.03/119.03 inference(scs_inference,[],[259,998,291,224,37,40,36,39,8,35,5,12,4,14,15,38,11,6,13,117,9,10,7,2,51])). % 119.03/119.03 cnf(2883,plain, % 119.03/119.03 (P1(f3(f7(a9,a9),f7(a9,a9)))), % 119.03/119.03 inference(scs_inference,[],[259,998,291,224,37,40,36,39,8,35,5,12,4,14,15,38,11,6,13,117,9,10,7,2,51,50])). % 119.03/119.03 cnf(2885,plain, % 119.03/119.03 (E(f7(a1,f7(a1,a1)),f4(a1,f7(a10,a10)))), % 119.03/119.03 inference(scs_inference,[],[259,2340,2348,998,291,224,37,40,36,39,8,35,5,12,4,14,15,38,11,6,13,117,9,10,7,2,51,50,3])). % 119.03/119.03 cnf(2886,plain, % 119.03/119.03 (~E(f7(f7(a11,a11),f7(a11,a11)),f3(a10,a11))), % 119.03/119.03 inference(scs_inference,[],[2836,259,2340,2348,998,291,224,37,40,36,39,8,35,5,12,4,14,15,38,11,6,13,117,9,10,7,2,51,50,3,16])). % 119.03/119.03 cnf(2898,plain, % 119.03/119.03 (P1(f6(f7(a1,a1),f7(a1,a1)))), % 119.03/119.03 inference(scs_inference,[],[2836,259,2156,2340,2215,2348,998,1579,273,291,245,285,224,102,26,24,37,40,36,39,8,35,5,12,4,14,15,38,11,6,13,117,9,10,7,2,51,50,3,16,17,68,85,77,59,67,60])). % 119.03/119.03 cnf(2920,plain, % 119.03/119.03 (P2(f7(a10,a10),f4(f7(a10,a10),a1))), % 119.03/119.03 inference(scs_inference,[],[2836,259,454,2820,2156,2340,2215,711,2348,998,1579,1662,273,115,291,245,682,332,285,224,305,102,26,312,24,23,37,40,36,39,8,35,5,12,4,14,15,38,11,6,13,117,9,10,7,2,51,50,3,16,17,68,85,77,59,67,60,78,84,95,61,62,65,57,41,53,43,87])). % 119.03/119.03 cnf(2932,plain, % 119.03/119.03 (P2(f7(a1,a1),f3(f7(a1,a1),f7(a1,a1)))), % 119.03/119.04 inference(scs_inference,[],[2836,259,454,2820,2156,1720,2340,2215,711,2348,998,333,1579,1662,273,316,115,291,245,144,682,332,285,224,587,305,180,102,26,312,142,24,23,37,40,36,39,8,35,5,12,4,14,15,38,11,6,13,117,9,10,7,2,51,50,3,16,17,68,85,77,59,67,60,78,84,95,61,62,65,57,41,53,43,87,88,89,90,97,58,79])). % 119.03/119.04 cnf(2935,plain, % 119.03/119.04 (P3(f7(a9,a9),f3(f7(a9,a9),f7(a9,a9)))), % 119.03/119.04 inference(scs_inference,[],[2883,319])). % 119.03/119.04 cnf(2940,plain, % 119.03/119.04 (E(f3(a1,f7(a11,a11)),f7(a11,a11))), % 119.03/119.04 inference(scs_inference,[],[267,40,37])). % 119.03/119.04 cnf(2942,plain, % 119.03/119.04 (E(f3(f7(a11,a11),a1),f7(a11,a11))), % 119.03/119.04 inference(scs_inference,[],[267,40,37,39])). % 119.03/119.04 cnf(2966,plain, % 119.03/119.04 (P1(f4(f7(a11,a11),f7(a11,a11)))), % 119.03/119.04 inference(scs_inference,[],[2886,2881,2883,314,267,40,37,39,41,8,35,36,5,4,15,12,13,38,14,6,9,117,10,11,7,2,51])). % 119.03/119.04 cnf(2968,plain, % 119.03/119.04 (P1(f3(f7(a11,a11),f7(a11,a11)))), % 119.03/119.04 inference(scs_inference,[],[2886,2881,2883,314,267,40,37,39,41,8,35,36,5,4,15,12,13,38,14,6,9,117,10,11,7,2,51,50])). % 119.03/119.04 cnf(2971,plain, % 119.03/119.04 (~E(f4(f7(a9,a9),f7(a9,a9)),f3(a10,a11))), % 119.03/119.04 inference(scs_inference,[],[2805,2886,2881,2883,314,2836,308,267,40,37,39,41,8,35,36,5,4,15,12,13,38,14,6,9,117,10,11,7,2,51,50,3,16])). % 119.03/119.04 cnf(2972,plain, % 119.03/119.04 (E(f3(a11,f5(a11,a11)),a11)), % 119.03/119.04 inference(scs_inference,[],[2805,2886,2881,2883,314,2836,233,308,267,27,40,37,39,41,8,35,36,5,4,15,12,13,38,14,6,9,117,10,11,7,2,51,50,3,16,68])). % 119.03/119.04 cnf(2976,plain, % 119.03/119.04 (P1(f6(f7(f7(a10,a10),f7(a10,a10)),a1))), % 119.03/119.04 inference(scs_inference,[],[2805,2886,2881,2883,2812,314,2836,233,308,267,338,27,24,23,40,37,39,41,8,35,36,5,4,15,12,13,38,14,6,9,117,10,11,7,2,51,50,3,16,68,85,60])). % 119.03/119.04 cnf(2990,plain, % 119.03/119.04 (~E(f3(a10,a11),f7(f3(f7(a9,a9),f7(a9,a9)),f7(a9,a9)))), % 119.03/119.04 inference(scs_inference,[],[2805,2886,2881,2883,2935,2812,615,453,314,2836,115,233,308,267,338,224,27,102,312,24,23,40,37,39,41,8,35,36,5,4,15,12,13,38,14,6,9,117,10,11,7,2,51,50,3,16,68,85,60,77,59,78,84,62,65,57])). % 119.03/119.04 cnf(2992,plain, % 119.03/119.04 (E(f7(a9,a9),f7(f3(f7(a9,a9),f7(a9,a9)),f7(a9,a9)))), % 119.03/119.04 inference(scs_inference,[],[2805,2886,2881,2883,2935,2812,615,453,314,2836,115,233,308,267,338,224,27,102,312,24,23,40,37,39,41,8,35,36,5,4,15,12,13,38,14,6,9,117,10,11,7,2,51,50,3,16,68,85,60,77,59,78,84,62,65,57,97])). % 119.03/119.04 cnf(2996,plain, % 119.03/119.04 (E(f7(a11,a11),f7(f3(f7(a11,a11),f7(a11,a11)),f7(a11,a11)))), % 119.03/119.04 inference(scs_inference,[],[2805,2886,2881,2883,2935,2920,2812,615,453,314,2836,115,233,1386,308,682,267,338,224,27,102,312,24,23,40,37,39,41,8,35,36,5,4,15,12,13,38,14,6,9,117,10,11,7,2,51,50,3,16,68,85,60,77,59,78,84,62,65,57,97,79,350])). % 119.03/119.04 cnf(3002,plain, % 119.03/119.04 (P3(f7(a11,a11),f3(f7(a11,a11),f7(a11,a11)))), % 119.03/119.04 inference(scs_inference,[],[2968,344])). % 119.03/119.04 cnf(3003,plain, % 119.03/119.04 (P2(f7(a11,a11),f4(f7(a11,a11),f7(a11,a11)))), % 119.03/119.04 inference(scs_inference,[],[2966,348])). % 119.03/119.04 cnf(3004,plain, % 119.03/119.04 (E(f3(a1,a11),a11)), % 119.03/119.04 inference(scs_inference,[],[27,37])). % 119.03/119.04 cnf(3006,plain, % 119.03/119.04 (E(f4(a11,a8),a11)), % 119.03/119.04 inference(scs_inference,[],[27,37,40])). % 119.03/119.04 cnf(3015,plain, % 119.03/119.04 (E(f3(a11,a1),a11)), % 119.03/119.04 inference(scs_inference,[],[2898,2972,27,37,40,41,36,8,35,39])). % 119.03/119.04 cnf(3021,plain, % 119.03/119.04 (E(f4(a8,a11),a11)), % 119.03/119.04 inference(scs_inference,[],[2898,2972,27,37,40,41,36,8,35,39,12,4,5,15,38])). % 119.03/119.04 cnf(3029,plain, % 119.03/119.04 (E(f3(x30291,f3(a11,f5(a11,a11))),f3(x30291,a11))), % 119.03/119.04 inference(scs_inference,[],[2898,2972,27,37,40,41,36,8,35,39,12,4,5,15,38,6,14,13,11,9,10,7])). % 119.03/119.04 cnf(3031,plain, % 119.03/119.04 (P1(f4(a11,a11))), % 119.03/119.04 inference(scs_inference,[],[2971,2898,2972,27,37,40,41,36,8,35,39,12,4,5,15,38,6,14,13,11,9,10,7,2,51])). % 119.03/119.04 cnf(3033,plain, % 119.03/119.04 (P1(f3(a11,a11))), % 119.03/119.04 inference(scs_inference,[],[2971,2898,2972,27,37,40,41,36,8,35,39,12,4,5,15,38,6,14,13,11,9,10,7,2,51,50])). % 119.03/119.04 cnf(3035,plain, % 119.03/119.04 (E(f4(f7(a9,a9),a8),f7(f3(f7(a9,a9),f7(a9,a9)),f7(a9,a9)))), % 119.03/119.04 inference(scs_inference,[],[2971,2857,2898,2972,2992,27,37,40,41,36,8,35,39,12,4,5,15,38,6,14,13,11,9,10,7,2,51,50,3])). % 119.03/119.04 cnf(3036,plain, % 119.03/119.04 (~E(f6(f7(a1,a1),f7(a1,a1)),f3(a10,a11))), % 119.03/119.04 inference(scs_inference,[],[2971,2857,2898,2972,2992,2836,27,37,40,41,36,8,35,39,12,4,5,15,38,6,14,13,11,9,10,7,2,51,50,3,16])). % 119.03/119.04 cnf(3038,plain, % 119.03/119.04 (P1(f5(f7(a11,a11),f7(a11,a11)))), % 119.03/119.04 inference(scs_inference,[],[34,2971,2857,2898,2972,2992,2836,287,267,27,37,40,41,36,8,35,39,12,4,5,15,38,6,14,13,11,9,10,7,2,51,50,3,16,18,59])). % 119.03/119.04 cnf(3069,plain, % 119.03/119.04 (P2(a11,f4(a11,a11))), % 119.03/119.04 inference(scs_inference,[],[3031,415])). % 119.03/119.04 cnf(3070,plain, % 119.03/119.04 (P3(a11,f3(a11,a11))), % 119.03/119.04 inference(scs_inference,[],[3033,431])). % 119.03/119.04 cnf(3071,plain, % 119.03/119.04 (E(f4(f4(a11,a11),a8),f4(a11,a11))), % 119.03/119.04 inference(scs_inference,[],[3031,40])). % 119.03/119.04 cnf(3073,plain, % 119.03/119.04 (E(f3(a1,f4(a11,a11)),f4(a11,a11))), % 119.03/119.04 inference(scs_inference,[],[3031,40,37])). % 119.03/119.04 cnf(3079,plain, % 119.03/119.04 (P3(f4(a11,a11),f4(a11,a11))), % 119.03/119.04 inference(scs_inference,[],[3031,40,37,36,35,41])). % 119.03/119.04 cnf(3098,plain, % 119.03/119.04 (P1(f4(f4(a11,a11),f4(a11,a11)))), % 119.03/119.04 inference(scs_inference,[],[3031,3004,3036,40,37,36,35,41,39,8,4,12,15,6,14,38,5,9,10,13,11,7,2,51])). % 119.03/119.04 cnf(3100,plain, % 119.03/119.04 (P1(f3(f4(a11,a11),f4(a11,a11)))), % 119.03/119.04 inference(scs_inference,[],[3031,3004,3036,40,37,36,35,41,39,8,4,12,15,6,14,38,5,9,10,13,11,7,2,51,50])). % 119.03/119.04 cnf(3103,plain, % 119.03/119.04 (~E(f4(a11,a11),f3(a10,a11))), % 119.03/119.04 inference(scs_inference,[],[3031,3004,3036,2990,3035,2836,40,37,36,35,41,39,8,4,12,15,6,14,38,5,9,10,13,11,7,2,51,50,3,16])). % 119.03/119.04 cnf(3113,plain, % 119.03/119.04 (P1(f5(f4(a11,a11),f4(a11,a11)))), % 119.03/119.04 inference(scs_inference,[],[3031,3004,3036,3003,2990,2996,3035,2648,2185,2241,2161,2880,1588,2836,305,102,23,40,37,36,35,41,39,8,4,12,15,6,14,38,5,9,10,13,11,7,2,51,50,3,16,18,19,20,53,67,85,59])). % 119.03/119.04 cnf(3115,plain, % 119.03/119.04 (E(f3(f4(a11,a11),f5(f4(a11,a11),f4(a11,a11))),f4(a11,a11))), % 119.03/119.04 inference(scs_inference,[],[3031,3004,3036,3003,2990,2996,3035,2648,2185,2241,2161,2880,1588,2836,305,102,23,40,37,36,35,41,39,8,4,12,15,6,14,38,5,9,10,13,11,7,2,51,50,3,16,18,19,20,53,67,85,59,68])). % 119.03/119.04 cnf(3119,plain, % 119.03/119.04 (P1(f6(f7(a10,a10),f7(a10,a10)))), % 119.03/119.04 inference(scs_inference,[],[3031,3004,3036,3003,2990,2996,3035,2648,2185,2241,2161,2880,1588,2836,1386,305,102,312,23,40,37,36,35,41,39,8,4,12,15,6,14,38,5,9,10,13,11,7,2,51,50,3,16,18,19,20,53,67,85,59,68,77,60])). % 119.03/119.04 cnf(3125,plain, % 119.03/119.04 (~E(f3(a1,f4(a11,a11)),f3(a9,f4(a11,a11)))), % 119.03/119.04 inference(scs_inference,[],[3031,3004,3036,3003,2990,2996,3035,2648,2185,2241,2161,33,2880,1588,2836,1386,305,102,312,25,23,40,37,36,35,41,39,8,4,12,15,6,14,38,5,9,10,13,11,7,2,51,50,3,16,18,19,20,53,67,85,59,68,77,60,78,84,62])). % 119.03/119.04 cnf(3133,plain, % 119.03/119.04 (E(f3(f3(a1,a11),f7(a11,a11)),a11)), % 119.03/119.04 inference(scs_inference,[],[3031,3004,3036,2861,2968,3002,3003,2990,2996,3035,2648,2185,2241,2161,33,2592,2880,1588,2836,1386,869,267,305,222,102,312,25,23,40,37,36,35,41,39,8,4,12,15,6,14,38,5,9,10,13,11,7,2,51,50,3,16,18,19,20,53,67,85,59,68,77,60,78,84,62,57,65,79,318])). % 119.03/119.04 cnf(3145,plain, % 119.03/119.04 (E(f3(a1,f3(a11,a11)),f3(a11,a11))), % 119.03/119.04 inference(scs_inference,[],[3033,37])). % 119.03/119.04 cnf(3153,plain, % 119.03/119.04 (P3(f3(a11,a11),f3(a11,a11))), % 119.03/119.04 inference(scs_inference,[],[3033,37,40,35,36,41])). % 119.03/119.04 cnf(3170,plain, % 119.03/119.04 (E(f3(x31701,f4(a11,a8)),f3(x31701,a11))), % 119.03/119.04 inference(scs_inference,[],[3033,3006,37,40,35,36,41,39,12,4,38,8,6,5,15,14,13,9,11,10,7])). % 119.03/119.04 cnf(3171,plain, % 119.03/119.04 (~E(f3(a10,a11),f4(a11,a11))), % 119.03/119.04 inference(scs_inference,[],[3033,3103,3006,37,40,35,36,41,39,12,4,38,8,6,5,15,14,13,9,11,10,7,2])). % 119.03/119.04 cnf(3172,plain, % 119.03/119.04 (P1(f4(f3(a11,a11),f3(a11,a11)))), % 119.03/119.04 inference(scs_inference,[],[3033,3103,3006,37,40,35,36,41,39,12,4,38,8,6,5,15,14,13,9,11,10,7,2,51])). % 119.03/119.04 cnf(3174,plain, % 119.03/119.04 (P1(f3(f3(a11,a11),f3(a11,a11)))), % 119.03/119.04 inference(scs_inference,[],[3033,3103,3006,37,40,35,36,41,39,12,4,38,8,6,5,15,14,13,9,11,10,7,2,51,50])). % 119.03/119.04 cnf(3177,plain, % 119.03/119.04 (~E(f3(a11,a11),f3(a10,a11))), % 119.03/119.04 inference(scs_inference,[],[3033,3103,3006,330,2836,37,40,35,36,41,39,12,4,38,8,6,5,15,14,13,9,11,10,7,2,51,50,3,16])). % 119.03/119.04 cnf(3202,plain, % 119.03/119.04 (E(f4(f7(a1,a1),a8),f7(a1,a1))), % 119.03/119.04 inference(scs_inference,[],[102,40])). % 119.03/119.04 cnf(3204,plain, % 119.03/119.04 (E(f3(a1,a10),a10)), % 119.03/119.04 inference(scs_inference,[],[102,26,40,37])). % 119.03/119.04 cnf(3227,plain, % 119.03/119.04 (E(f3(x32271,f3(a11,a1)),f3(x32271,a11))), % 119.03/119.04 inference(scs_inference,[],[3015,3038,102,26,40,37,36,35,39,41,38,4,12,6,8,15,14,5,11,10,13,9,7])). % 119.03/119.04 cnf(3228,plain, % 119.03/119.04 (~E(f3(a10,a11),f3(a11,a11))), % 119.03/119.04 inference(scs_inference,[],[3177,3015,3038,102,26,40,37,36,35,39,41,38,4,12,6,8,15,14,5,11,10,13,9,7,2])). % 119.03/119.04 cnf(3229,plain, % 119.03/119.04 (P1(f4(f7(a1,a1),f7(a1,a1)))), % 119.03/119.04 inference(scs_inference,[],[3177,3015,3038,102,26,40,37,36,35,39,41,38,4,12,6,8,15,14,5,11,10,13,9,7,2,51])). % 119.03/119.04 cnf(3231,plain, % 119.03/119.04 (P1(f3(f7(a1,a1),f7(a1,a1)))), % 119.03/119.04 inference(scs_inference,[],[3177,3015,3038,102,26,40,37,36,35,39,41,38,4,12,6,8,15,14,5,11,10,13,9,7,2,51,50])). % 119.03/119.04 cnf(3234,plain, % 119.03/119.04 (~E(f5(f7(a11,a11),f7(a11,a11)),f3(a10,a11))), % 119.03/119.04 inference(scs_inference,[],[3171,3177,3015,3071,3038,2836,102,26,40,37,36,35,39,41,38,4,12,6,8,15,14,5,11,10,13,9,7,2,51,50,3,16])). % 119.03/119.04 cnf(3237,plain, % 119.03/119.04 (P3(f7(a1,f7(a1,a1)),f4(a1,f7(a10,a10)))), % 119.03/119.04 inference(scs_inference,[],[34,3171,3177,3015,3071,3170,3038,2259,2182,2836,102,26,40,37,36,35,39,41,38,4,12,6,8,15,14,5,11,10,13,9,7,2,51,50,3,16,18,17])). % 119.03/119.04 cnf(3238,plain, % 119.03/119.04 (P2(f3(f7(a10,a10),a1),f7(a10,a10))), % 119.03/119.04 inference(scs_inference,[],[34,3171,3177,3015,3071,3170,3038,2879,2259,2182,1392,2836,102,26,40,37,36,35,39,41,38,4,12,6,8,15,14,5,11,10,13,9,7,2,51,50,3,16,18,17,19])). % 119.03/119.04 cnf(3240,plain, % 119.03/119.04 (P1(f5(f3(a11,a11),f3(a11,a11)))), % 119.03/119.04 inference(scs_inference,[],[34,3153,3171,3177,3015,3071,3170,3038,2879,2259,2182,1392,2836,3033,102,26,40,37,36,35,39,41,38,4,12,6,8,15,14,5,11,10,13,9,7,2,51,50,3,16,18,17,19,59])). % 119.03/119.04 cnf(3256,plain, % 119.03/119.04 (P2(f3(a11,a11),f4(f3(a11,a11),f3(a11,a11)))), % 119.03/119.04 inference(scs_inference,[],[34,3069,3153,3171,3177,3015,2940,3071,3170,2932,3038,3172,2879,2259,2182,1392,3070,1579,233,2836,3033,3031,27,102,26,40,37,36,35,39,41,38,4,12,6,8,15,14,5,11,10,13,9,7,2,51,50,3,16,18,17,19,59,67,68,60,57,65,79,318,20,87])). % 119.03/119.04 cnf(3258,plain, % 119.03/119.04 (P3(f3(a11,a11),f3(f3(a11,a11),f3(a11,a11)))), % 119.03/119.04 inference(scs_inference,[],[34,3069,3153,3171,3177,3015,2940,3071,3170,2932,3038,3172,3174,2879,2259,2182,1392,3070,1579,233,2836,3033,3031,27,102,26,40,37,36,35,39,41,38,4,12,6,8,15,14,5,11,10,13,9,7,2,51,50,3,16,18,17,19,59,67,68,60,57,65,79,318,20,87,88])). % 119.03/119.04 cnf(3265,plain, % 119.03/119.04 (P3(f7(a1,a1),f3(f7(a1,a1),f7(a1,a1)))), % 119.03/119.04 inference(scs_inference,[],[3231,274])). % 119.03/119.04 cnf(3267,plain, % 119.03/119.04 (E(f4(a10,a8),a10)), % 119.03/119.04 inference(scs_inference,[],[26,40])). % 119.03/119.04 cnf(3277,plain, % 119.03/119.04 (E(f3(a10,a1),a10)), % 119.03/119.04 inference(scs_inference,[],[3098,26,142,40,37,41,35,36,39])). % 119.03/119.04 cnf(3279,plain, % 119.03/119.04 (E(f4(a8,a10),a10)), % 119.03/119.04 inference(scs_inference,[],[3098,26,142,40,37,41,35,36,39,38])). % 119.03/119.04 cnf(3284,plain, % 119.03/119.04 (E(f7(x32841,f4(a8,a11)),f7(x32841,a11))), % 119.03/119.04 inference(scs_inference,[],[3021,3098,26,142,40,37,41,35,36,39,38,12,4,6,11])). % 119.03/119.04 cnf(3291,plain, % 119.03/119.04 (E(f3(x32911,f4(a8,a11)),f3(x32911,a11))), % 119.03/119.04 inference(scs_inference,[],[3021,3098,26,142,40,37,41,35,36,39,38,12,4,6,11,8,5,14,15,10,13,7])). % 119.03/119.04 cnf(3294,plain, % 119.03/119.04 (P1(f4(a10,a10))), % 119.03/119.04 inference(scs_inference,[],[3021,3234,3098,26,142,40,37,41,35,36,39,38,12,4,6,11,8,5,14,15,10,13,7,9,2,51])). % 119.03/119.04 cnf(3296,plain, % 119.03/119.04 (P1(f3(a10,a10))), % 119.03/119.04 inference(scs_inference,[],[3021,3234,3098,26,142,40,37,41,35,36,39,38,12,4,6,11,8,5,14,15,10,13,7,9,2,51,50])). % 119.03/119.04 cnf(3299,plain, % 119.03/119.04 (~E(f4(f4(a11,a11),f4(a11,a11)),f3(a10,a11))), % 119.03/119.04 inference(scs_inference,[],[3021,3234,3098,330,2836,26,142,40,37,41,35,36,39,38,12,4,6,11,8,5,14,15,10,13,7,9,2,51,50,3,16])). % 119.03/119.04 cnf(3302,plain, % 119.03/119.04 (~P3(f3(a1,a10),f3(a10,a11))), % 119.03/119.04 inference(scs_inference,[],[34,3021,3204,3234,3227,3098,330,2836,26,142,40,37,41,35,36,39,38,12,4,6,11,8,5,14,15,10,13,7,9,2,51,50,3,16,18,17])). % 119.03/119.04 cnf(3309,plain, % 119.03/119.04 (P1(f6(a1,a1))), % 119.03/119.04 inference(scs_inference,[],[34,3021,3204,3234,3227,3098,1677,330,1053,287,590,2836,587,267,102,26,142,24,23,40,37,41,35,36,39,38,12,4,6,11,8,5,14,15,10,13,7,9,2,51,50,3,16,18,17,59,67,68,60])). % 119.03/119.04 cnf(3329,plain, % 119.03/119.04 (P3(f4(a11,a11),f3(f4(a11,a11),f4(a11,a11)))), % 119.03/119.04 inference(scs_inference,[],[34,3079,3021,3204,3234,3238,2942,3227,3098,3100,3113,3258,3115,2869,2976,1677,2968,3002,3174,330,1053,287,233,590,2836,587,3033,3031,971,267,27,102,26,312,142,24,23,40,37,41,35,36,39,38,12,4,6,11,8,5,14,15,10,13,7,9,2,51,50,3,16,18,17,59,67,68,60,43,89,57,65,79,71,318,44,87,88])). % 119.03/119.04 cnf(3331,plain, % 119.03/119.04 (E(f3(a11,a11),f7(f3(f3(a11,a11),f3(a11,a11)),f3(a11,a11)))), % 119.03/119.04 inference(scs_inference,[],[34,3079,3021,3204,3234,3238,2942,3227,3098,3100,3113,3258,3115,2869,2976,1677,2968,3002,3174,330,1053,287,233,590,2836,587,3033,3031,971,267,27,102,26,312,142,24,23,40,37,41,35,36,39,38,12,4,6,11,8,5,14,15,10,13,7,9,2,51,50,3,16,18,17,59,67,68,60,43,89,57,65,79,71,318,44,87,88,97])). % 119.03/119.04 cnf(3334,plain, % 119.03/119.04 (P2(a10,f4(a10,a10))), % 119.03/119.04 inference(scs_inference,[],[3294,215])). % 119.03/119.04 cnf(3335,plain, % 119.03/119.04 (P3(a10,f3(a10,a10))), % 119.03/119.04 inference(scs_inference,[],[3296,413])). % 119.03/119.04 cnf(3336,plain, % 119.03/119.04 (E(f4(f4(a10,a10),a8),f4(a10,a10))), % 119.03/119.04 inference(scs_inference,[],[3294,40])). % 119.03/119.04 cnf(3342,plain, % 119.03/119.04 (P3(f4(a10,a10),f4(a10,a10))), % 119.03/119.04 inference(scs_inference,[],[3294,40,37,39,41])). % 119.03/119.04 cnf(3353,plain, % 119.03/119.04 (E(f3(f4(a10,a8),x33531),f3(a10,x33531))), % 119.03/119.04 inference(scs_inference,[],[3294,3267,40,37,39,41,35,38,36,4,12,15,6])). % 119.03/119.04 cnf(3354,plain, % 119.03/119.04 (E(f7(x33541,f4(a10,a8)),f7(x33541,a10))), % 119.03/119.04 inference(scs_inference,[],[3294,3267,40,37,39,41,35,38,36,4,12,15,6,11])). % 119.03/119.04 cnf(3358,plain, % 119.03/119.04 (E(f4(f4(a10,a8),x33581),f4(a10,x33581))), % 119.03/119.04 inference(scs_inference,[],[3294,3267,40,37,39,41,35,38,36,4,12,15,6,11,14,5,10,8])). % 119.03/119.04 cnf(3361,plain, % 119.03/119.04 (E(f3(x33611,f4(a10,a8)),f3(x33611,a10))), % 119.03/119.04 inference(scs_inference,[],[3294,3267,40,37,39,41,35,38,36,4,12,15,6,11,14,5,10,8,13,9,7])). % 119.03/119.04 cnf(3363,plain, % 119.03/119.04 (P1(f4(f4(a10,a10),f4(a10,a10)))), % 119.03/119.04 inference(scs_inference,[],[3294,3267,3299,40,37,39,41,35,38,36,4,12,15,6,11,14,5,10,8,13,9,7,2,51])). % 119.03/119.04 cnf(3365,plain, % 119.03/119.04 (P1(f3(f4(a10,a10),f4(a10,a10)))), % 119.03/119.04 inference(scs_inference,[],[3294,3267,3299,40,37,39,41,35,38,36,4,12,15,6,11,14,5,10,8,13,9,7,2,51,50])). % 119.03/119.04 cnf(3368,plain, % 119.03/119.04 (~E(f4(a10,a10),f3(a10,a11))), % 119.03/119.04 inference(scs_inference,[],[3294,3228,3267,3299,3145,2836,40,37,39,41,35,38,36,4,12,15,6,11,14,5,10,8,13,9,7,2,51,50,3,16])). % 119.03/119.04 cnf(3371,plain, % 119.03/119.04 (~P3(f4(a10,a8),f3(a10,a11))), % 119.03/119.04 inference(scs_inference,[],[34,3294,3228,3267,3299,3145,3291,2836,40,37,39,41,35,38,36,4,12,15,6,11,14,5,10,8,13,9,7,2,51,50,3,16,18,17])). % 119.03/119.04 cnf(3386,plain, % 119.03/119.04 (E(f4(a1,f7(a10,a10)),f7(a1,f7(a1,a1)))), % 119.03/119.04 inference(scs_inference,[],[34,3294,3228,3267,3299,3145,3291,3231,3256,3265,2885,3237,3172,2880,590,2836,587,3033,187,305,102,23,40,37,39,41,35,38,36,4,12,15,6,11,14,5,10,8,13,9,7,2,51,50,3,16,18,17,59,53,67,68,60,43,89,56])). % 119.03/119.04 cnf(3394,plain, % 119.03/119.04 (E(f3(f4(a10,a8),f7(a10,a10)),a10)), % 119.03/119.04 inference(scs_inference,[],[34,3294,3228,3267,3299,2871,3145,3291,3231,3256,3265,2885,3237,3172,2607,2880,590,2836,587,869,3033,187,305,222,102,25,23,40,37,39,41,35,38,36,4,12,15,6,11,14,5,10,8,13,9,7,2,51,50,3,16,18,17,59,53,67,68,60,43,89,56,57,65,79,370])). % 119.03/119.04 cnf(3405,plain, % 119.03/119.04 (E(f4(f6(a1,a1),a8),f6(a1,a1))), % 119.03/119.04 inference(scs_inference,[],[3309,40])). % 119.03/119.04 cnf(3411,plain, % 119.03/119.04 (P3(f6(a1,a1),f6(a1,a1))), % 119.03/119.04 inference(scs_inference,[],[3309,40,37,39,41])). % 119.03/119.04 cnf(3419,plain, % 119.03/119.04 (E(f2(f3(a10,a1),x34191),f2(a10,x34191))), % 119.03/119.04 inference(scs_inference,[],[3309,3277,3119,40,37,39,41,36,35,38,4])). % 119.03/119.04 cnf(3431,plain, % 119.03/119.04 (~E(f3(a10,a11),f4(a10,a10))), % 119.03/119.04 inference(scs_inference,[],[3368,3309,3277,3119,40,37,39,41,36,35,38,4,6,5,12,15,14,10,11,8,13,9,7,2])). % 119.03/119.04 cnf(3432,plain, % 119.03/119.04 (P1(f4(f6(a1,a1),f6(a1,a1)))), % 119.03/119.04 inference(scs_inference,[],[3368,3309,3277,3119,40,37,39,41,36,35,38,4,6,5,12,15,14,10,11,8,13,9,7,2,51])). % 119.03/119.04 cnf(3434,plain, % 119.03/119.04 (P1(f3(f6(a1,a1),f6(a1,a1)))), % 119.03/119.04 inference(scs_inference,[],[3368,3309,3277,3119,40,37,39,41,36,35,38,4,6,5,12,15,14,10,11,8,13,9,7,2,51,50])). % 119.03/119.04 cnf(3437,plain, % 119.03/119.04 (~E(f6(a1,a1),f3(a10,a11))), % 119.03/119.04 inference(scs_inference,[],[3368,3309,3277,3119,380,2836,40,37,39,41,36,35,38,4,6,5,12,15,14,10,11,8,13,9,7,2,51,50,3,16])). % 119.03/119.04 cnf(3456,plain, % 119.03/119.04 (E(a10,f7(f3(a10,a10),a10))), % 119.03/119.04 inference(scs_inference,[],[34,3334,3335,3368,3309,3277,3353,3354,3119,3296,454,380,3294,332,2836,26,312,40,37,39,41,36,35,38,4,6,5,12,15,14,10,11,8,13,9,7,2,51,50,3,16,18,17,59,67,68,60,62,57,65,97])). % 119.03/119.04 cnf(3478,plain, % 119.03/119.04 (E(f3(f4(a8,a10),x34781),f3(a10,x34781))), % 119.03/119.04 inference(scs_inference,[],[3279,3229,3296,40,39,37,38,41,36,35,4,12,6])). % 119.03/119.04 cnf(3488,plain, % 119.03/119.04 (~E(f3(a10,a11),f6(a1,a1))), % 119.03/119.04 inference(scs_inference,[],[3437,3279,3229,3296,40,39,37,38,41,36,35,4,12,6,10,5,14,15,8,11,13,9,7,2])). % 119.03/119.04 cnf(3491,plain, % 119.03/119.04 (P1(f3(f3(a10,a10),f3(a10,a10)))), % 119.03/119.04 inference(scs_inference,[],[3437,3279,3229,3296,40,39,37,38,41,36,35,4,12,6,10,5,14,15,8,11,13,9,7,2,51,50])). % 119.03/119.04 cnf(3494,plain, % 119.03/119.04 (~E(f4(f7(a1,a1),f7(a1,a1)),f3(a10,a11))), % 119.03/119.04 inference(scs_inference,[],[3431,3437,3279,3336,3229,3296,2836,40,39,37,38,41,36,35,4,12,6,10,5,14,15,8,11,13,9,7,2,51,50,3,16])). % 119.03/119.04 cnf(3522,plain, % 119.03/119.04 (E(f3(a1,a8),a8)), % 119.03/119.04 inference(scs_inference,[],[142,24,40,39,37])). % 119.03/119.04 cnf(3545,plain, % 119.03/119.04 (P1(f4(f7(a10,a10),f7(a10,a10)))), % 119.03/119.04 inference(scs_inference,[],[3494,3240,3133,312,142,24,40,39,37,41,38,35,36,4,12,5,14,10,6,11,15,13,8,9,7,2,51])). % 119.03/119.04 cnf(3547,plain, % 119.03/119.04 (P1(f3(f7(a10,a10),f7(a10,a10)))), % 119.03/119.04 inference(scs_inference,[],[3494,3240,3133,312,142,24,40,39,37,41,38,35,36,4,12,5,14,10,6,11,15,13,8,9,7,2,51,50])). % 119.03/119.04 cnf(3550,plain, % 119.03/119.04 (~E(f5(f3(a11,a11),f3(a11,a11)),f3(a10,a11))), % 119.03/119.04 inference(scs_inference,[],[3494,3073,3240,3133,3125,2836,312,142,24,40,39,37,41,38,35,36,4,12,5,14,10,6,11,15,13,8,9,7,2,51,50,3,16])). % 119.03/119.04 cnf(3563,plain, % 119.03/119.04 (P2(f7(a10,a10),f3(f7(a10,a10),f7(a10,a10)))), % 119.03/119.04 inference(scs_inference,[],[34,3342,3411,3494,3073,3284,3478,3240,3329,3133,3394,3125,3100,3070,1386,3309,3294,2836,3031,3033,27,312,142,24,40,39,37,41,38,35,36,4,12,5,14,10,6,11,15,13,8,9,7,2,51,50,3,16,18,17,59,68,57,65,79])). % 119.03/119.04 cnf(3574,plain, % 119.03/119.04 (E(f7(a8,a8),f7(f3(f7(a8,a8),f7(a8,a8)),f7(a8,a8)))+~P1(f3(f7(a8,a8),f7(a8,a8)))), % 119.03/119.04 inference(scs_inference,[],[3545,406])). % 119.03/119.04 cnf(3576,plain, % 119.03/119.04 (E(f4(a8,a8),a8)), % 119.03/119.04 inference(scs_inference,[],[24,40])). % 119.03/119.04 cnf(3578,plain, % 119.03/119.04 (E(f3(a8,a1),a8)), % 119.03/119.04 inference(scs_inference,[],[24,40,39])). % 119.03/119.04 cnf(3582,plain, % 119.03/119.04 (E(f4(a8,a9),a9)), % 119.03/119.04 inference(scs_inference,[],[3363,24,25,40,39,41,38])). % 119.03/119.04 cnf(3610,plain, % 119.03/119.04 (~P3(f4(f4(a10,a8),a8),f3(a10,a11))), % 119.03/119.04 inference(scs_inference,[],[3488,3371,3522,3550,3405,3358,3363,3456,403,2836,142,24,25,40,39,41,38,37,35,36,4,5,10,6,12,15,14,11,8,13,9,7,2,51,50,3,16,18,17])). % 119.03/119.04 cnf(3618,plain, % 119.03/119.04 (~E(f3(a8,a1),f3(a8,a8))), % 119.03/119.04 inference(scs_inference,[],[3488,3371,3522,3550,3405,3358,3363,3547,3563,3456,119,403,32,245,2836,224,102,312,142,24,25,23,40,39,41,38,37,35,36,4,5,10,6,12,15,14,11,8,13,9,7,2,51,50,3,16,18,17,59,60,68,61])). % 119.03/119.04 cnf(3630,plain, % 119.03/119.04 (E(f7(a8,a8),f7(f3(f7(a8,a8),f7(a8,a8)),f7(a8,a8)))), % 119.03/119.04 inference(scs_inference,[],[3488,3371,3522,3550,3202,3405,3358,3363,3547,3563,3432,3434,3456,119,403,32,245,1386,3309,2836,100,224,102,312,142,24,25,23,40,39,41,38,37,35,36,4,5,10,6,12,15,14,11,8,13,9,7,2,51,50,3,16,18,17,59,60,68,61,65,79,45,87,88,3574])). % 119.03/119.04 cnf(3639,plain, % 119.03/119.04 (E(f3(a1,a1),a1)), % 119.03/119.04 inference(scs_inference,[],[25,23,40,38,37])). % 119.03/119.04 cnf(3657,plain, % 119.03/119.04 (E(f4(x36571,f4(a8,a8)),f4(x36571,a8))), % 119.03/119.04 inference(scs_inference,[],[3576,3365,25,23,40,38,37,39,35,41,36,4,10,12,15,5,6,11,14,9])). % 119.03/119.04 cnf(3661,plain, % 119.03/119.04 (~E(f3(a8,a8),f3(a8,a1))), % 119.03/119.04 inference(scs_inference,[],[3618,3576,3365,25,23,40,38,37,39,35,41,36,4,10,12,15,5,6,11,14,9,13,8,7,2])). % 119.03/119.04 cnf(3662,plain, % 119.03/119.04 (P1(f4(a8,a8))), % 119.03/119.04 inference(scs_inference,[],[3618,3576,3365,24,25,23,40,38,37,39,35,41,36,4,10,12,15,5,6,11,14,9,13,8,7,2,51])). % 119.03/119.04 cnf(3664,plain, % 119.03/119.04 (P1(f3(a8,a8))), % 119.03/119.04 inference(scs_inference,[],[3618,3576,3365,24,25,23,40,38,37,39,35,41,36,4,10,12,15,5,6,11,14,9,13,8,7,2,51,50])). % 119.03/119.04 cnf(3666,plain, % 119.03/119.04 (E(f4(a8,a8),f3(a8,f7(a8,a8)))), % 119.03/119.04 inference(scs_inference,[],[3618,3576,3365,258,24,25,23,40,38,37,39,35,41,36,4,10,12,15,5,6,11,14,9,13,8,7,2,51,50,3])). % 119.03/119.04 cnf(3667,plain, % 119.03/119.04 (~E(f3(f4(a10,a10),f4(a10,a10)),f3(a10,a11))), % 119.03/119.04 inference(scs_inference,[],[3618,3576,3365,2836,258,24,25,23,40,38,37,39,35,41,36,4,10,12,15,5,6,11,14,9,13,8,7,2,51,50,3,16])). % 119.03/119.04 cnf(3692,plain, % 119.03/119.04 (P3(a8,f3(a8,a8))), % 119.03/119.04 inference(scs_inference,[],[3664,231])). % 119.03/119.04 cnf(3693,plain, % 119.03/119.04 (P2(a8,f4(a8,a8))), % 119.03/119.04 inference(scs_inference,[],[3662,235])). % 119.03/119.04 cnf(3735,plain, % 119.03/119.04 (~E(f4(a8,a8),f3(a10,a11))), % 119.03/119.04 inference(scs_inference,[],[3662,3664,3578,3667,3657,3610,3666,2836,10,15,5,14,13,6,8,40,11,9,39,2,38,35,37,4,41,7,36,12,17,18,16])). % 119.03/119.04 cnf(3788,plain, % 119.03/119.04 (E(f4(a1,a1),a1)), % 119.03/119.04 inference(scs_inference,[],[23,3582,15,5,14,10,6,13,11,8,40,35])). % 119.03/119.04 cnf(3809,plain, % 119.03/119.04 (P1(f4(a1,a1))), % 119.03/119.04 inference(scs_inference,[],[23,3735,3302,3582,3361,3491,2830,3386,3029,3664,2836,15,5,14,10,6,13,11,8,40,35,39,9,37,2,41,4,7,36,12,17,20,16,18,51])). % 119.03/119.04 cnf(3811,plain, % 119.03/119.04 (P1(f3(a1,a1))), % 119.03/119.04 inference(scs_inference,[],[23,3735,3302,3582,3361,3491,2830,3386,3029,3664,2836,15,5,14,10,6,13,11,8,40,35,39,9,37,2,41,4,7,36,12,17,20,16,18,51,50])). % 119.03/119.04 cnf(3826,plain, % 119.03/119.04 (~E(f3(a10,a11),f7(a1,a1))), % 119.03/119.04 inference(scs_inference,[],[23,3692,3693,3735,3302,3582,3639,3361,3491,2830,3386,3029,3664,3662,587,2836,100,303,24,15,5,14,10,6,13,11,8,40,35,39,9,37,2,41,4,7,36,12,17,20,16,18,51,50,3,60,67,68,59,43,89,57])). % 119.03/119.04 cnf(3842,plain, % 119.03/119.04 (E(a1,f7(f3(a1,a1),a1))), % 119.03/119.04 inference(scs_inference,[],[3811,301])). % 119.03/119.04 cnf(3872,plain, % 119.03/119.04 (P3(f4(a1,a1),a1)), % 119.03/119.04 inference(scs_inference,[],[3809,3811,3826,3788,15,5,14,10,6,11,13,8,40,35,39,9,37,2,117,41,4,38,7,36,12,17,18])). % 119.03/119.04 cnf(5113,plain, % 119.03/119.04 ($false), % 119.03/119.04 inference(scs_inference,[],[26,28,2836,27,201,782,3033,2880,3277,409,3872,3331,3069,2812,330,3826,3842,3177,3661,3419,3630,3456,117,106,6,370,192,7,2,342,190,1320,1327,1334,1341,146,191,18,17,16,20,3,19,50]), % 119.03/119.04 ['proof']). % 119.03/119.04 % SZS output end Proof % 119.03/119.04 % Total time :118.500000s %------------------------------------------------------------------------------