%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM475+2 : 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 : n019.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:27 EDT 2024 % Result : Theorem 19.78s 19.87s % Output : CNFRefutation 19.78s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : NUM475+2 : TPTP v8.2.0. Released v4.0.0. % 0.10/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n019.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Sun Jun 23 01:40:39 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.57 start to proof:theBenchmark % 19.78/19.86 %------------------------------------------- % 19.78/19.86 % File :CSE---1.7 % 19.78/19.86 % Problem :theBenchmark % 19.78/19.86 % Transform :cnf % 19.78/19.86 % Format :tptp:raw % 19.78/19.86 % Command :java -jar mcs_scs.jar %d %s % 19.78/19.86 % 19.78/19.86 % Result :Theorem 19.230000s % 19.78/19.86 % Output :CNFRefutation 19.230000s % 19.78/19.86 %------------------------------------------- % 19.78/19.86 %------------------------------------------------------------------------------ % 19.78/19.86 % File : NUM475+2 : TPTP v8.2.0. Released v4.0.0. % 19.78/19.86 % Domain : Number Theory % 19.78/19.86 % Problem : Square root of a prime is irrational 10_06, 01 expansion % 19.78/19.86 % Version : Especial. % 19.78/19.86 % English : % 19.78/19.86 % 19.78/19.86 % Refs : [LPV06] Lyaletski et al. (2006), SAD as a Mathematical Assista % 19.78/19.86 % : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 19.78/19.86 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 19.78/19.86 % Source : [Pas08] % 19.78/19.86 % Names : primes_10_06.01 [Pas08] % 19.78/19.86 % 19.78/19.86 % Status : Theorem % 19.78/19.86 % Rating : 0.22 v8.2.0, 0.25 v8.1.0, 0.31 v7.5.0, 0.28 v7.4.0, 0.23 v7.3.0, 0.21 v7.1.0, 0.26 v7.0.0, 0.27 v6.4.0, 0.31 v6.3.0, 0.29 v6.2.0, 0.28 v6.1.0, 0.40 v6.0.0, 0.43 v5.5.0, 0.52 v5.4.0, 0.54 v5.3.0, 0.56 v5.2.0, 0.35 v5.1.0, 0.48 v5.0.0, 0.58 v4.1.0, 0.61 v4.0.1, 0.74 v4.0.0 % 19.78/19.86 % Syntax : Number of formulae : 42 ( 4 unt; 4 def) % 19.78/19.86 % Number of atoms : 176 ( 59 equ) % 19.78/19.86 % Maximal formula atoms : 10 ( 4 avg) % 19.78/19.86 % Number of connectives : 149 ( 15 ~; 6 |; 75 &) % 19.78/19.86 % ( 4 <=>; 49 =>; 0 <=; 0 <~>) % 19.78/19.86 % Maximal formula depth : 11 ( 5 avg) % 19.78/19.86 % Maximal term depth : 3 ( 1 avg) % 19.78/19.86 % Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty) % 19.78/19.86 % Number of functors : 12 ( 12 usr; 8 con; 0-2 aty) % 19.78/19.86 % Number of variables : 73 ( 68 !; 5 ?) % 19.78/19.86 % SPC : FOF_THM_RFO_SEQ % 19.78/19.86 % 19.78/19.86 % Comments : Problem generated by the SAD system [VLP07] % 19.78/19.86 %------------------------------------------------------------------------------ % 19.78/19.86 fof(mNatSort,axiom, % 19.78/19.86 ! [W0] : % 19.78/19.86 ( aNaturalNumber0(W0) % 19.78/19.86 => $true ) ). % 19.78/19.86 % 19.78/19.86 fof(mSortsC,axiom, % 19.78/19.86 aNaturalNumber0(sz00) ). % 19.78/19.86 % 19.78/19.86 fof(mSortsC_01,axiom, % 19.78/19.86 ( aNaturalNumber0(sz10) % 19.78/19.86 & sz10 != sz00 ) ). % 19.78/19.86 % 19.78/19.86 fof(mSortsB,axiom, % 19.78/19.86 ! [W0,W1] : % 19.78/19.86 ( ( aNaturalNumber0(W0) % 19.78/19.86 & aNaturalNumber0(W1) ) % 19.78/19.86 => aNaturalNumber0(sdtpldt0(W0,W1)) ) ). % 19.78/19.86 % 19.78/19.86 fof(mSortsB_02,axiom, % 19.78/19.86 ! [W0,W1] : % 19.78/19.86 ( ( aNaturalNumber0(W0) % 19.78/19.86 & aNaturalNumber0(W1) ) % 19.78/19.86 => aNaturalNumber0(sdtasdt0(W0,W1)) ) ). % 19.78/19.86 % 19.78/19.86 fof(mAddComm,axiom, % 19.78/19.86 ! [W0,W1] : % 19.78/19.86 ( ( aNaturalNumber0(W0) % 19.78/19.86 & aNaturalNumber0(W1) ) % 19.78/19.86 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 19.78/19.86 % 19.78/19.86 fof(mAddAsso,axiom, % 19.78/19.86 ! [W0,W1,W2] : % 19.78/19.86 ( ( aNaturalNumber0(W0) % 19.78/19.86 & aNaturalNumber0(W1) % 19.78/19.86 & aNaturalNumber0(W2) ) % 19.78/19.86 => sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) ). % 19.78/19.86 % 19.78/19.86 fof(m_AddZero,axiom, % 19.78/19.86 ! [W0] : % 19.78/19.86 ( aNaturalNumber0(W0) % 19.78/19.86 => ( sdtpldt0(W0,sz00) = W0 % 19.78/19.86 & W0 = sdtpldt0(sz00,W0) ) ) ). % 19.78/19.86 % 19.78/19.86 fof(mMulComm,axiom, % 19.78/19.86 ! [W0,W1] : % 19.78/19.86 ( ( aNaturalNumber0(W0) % 19.78/19.86 & aNaturalNumber0(W1) ) % 19.78/19.86 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 19.78/19.86 % 19.78/19.86 fof(mMulAsso,axiom, % 19.78/19.86 ! [W0,W1,W2] : % 19.78/19.86 ( ( aNaturalNumber0(W0) % 19.78/19.86 & aNaturalNumber0(W1) % 19.78/19.86 & aNaturalNumber0(W2) ) % 19.78/19.86 => sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) ). % 19.78/19.86 % 19.78/19.86 fof(m_MulUnit,axiom, % 19.78/19.86 ! [W0] : % 19.78/19.86 ( aNaturalNumber0(W0) % 19.78/19.86 => ( sdtasdt0(W0,sz10) = W0 % 19.78/19.86 & W0 = sdtasdt0(sz10,W0) ) ) ). % 19.78/19.86 % 19.78/19.86 fof(m_MulZero,axiom, % 19.78/19.86 ! [W0] : % 19.78/19.86 ( aNaturalNumber0(W0) % 19.78/19.86 => ( sdtasdt0(W0,sz00) = sz00 % 19.78/19.86 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 19.78/19.86 % 19.78/19.86 fof(mAMDistr,axiom, % 19.78/19.86 ! [W0,W1,W2] : % 19.78/19.86 ( ( aNaturalNumber0(W0) % 19.78/19.86 & aNaturalNumber0(W1) % 19.78/19.86 & aNaturalNumber0(W2) ) % 19.78/19.87 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 19.78/19.87 & sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ). % 19.78/19.87 % 19.78/19.87 fof(mAddCanc,axiom, % 19.78/19.87 ! [W0,W1,W2] : % 19.78/19.87 ( ( aNaturalNumber0(W0) % 19.78/19.87 & aNaturalNumber0(W1) % 19.78/19.87 & aNaturalNumber0(W2) ) % 19.78/19.87 => ( ( sdtpldt0(W0,W1) = sdtpldt0(W0,W2) % 19.78/19.87 | sdtpldt0(W1,W0) = sdtpldt0(W2,W0) ) % 19.78/19.87 => W1 = W2 ) ) ). % 19.78/19.87 % 19.78/19.87 fof(mMulCanc,axiom, % 19.78/19.87 ! [W0] : % 19.78/19.87 ( aNaturalNumber0(W0) % 19.78/19.87 => ( W0 != sz00 % 19.78/19.87 => ! [W1,W2] : % 19.78/19.87 ( ( aNaturalNumber0(W1) % 19.78/19.87 & aNaturalNumber0(W2) ) % 19.78/19.87 => ( ( sdtasdt0(W0,W1) = sdtasdt0(W0,W2) % 19.78/19.87 | sdtasdt0(W1,W0) = sdtasdt0(W2,W0) ) % 19.78/19.87 => W1 = W2 ) ) ) ) ). % 19.78/19.87 % 19.78/19.87 fof(mZeroAdd,axiom, % 19.78/19.87 ! [W0,W1] : % 19.78/19.87 ( ( aNaturalNumber0(W0) % 19.78/19.87 & aNaturalNumber0(W1) ) % 19.78/19.87 => ( sdtpldt0(W0,W1) = sz00 % 19.78/19.87 => ( W0 = sz00 % 19.78/19.87 & W1 = sz00 ) ) ) ). % 19.78/19.87 % 19.78/19.87 fof(mZeroMul,axiom, % 19.78/19.87 ! [W0,W1] : % 19.78/19.87 ( ( aNaturalNumber0(W0) % 19.78/19.87 & aNaturalNumber0(W1) ) % 19.78/19.87 => ( sdtasdt0(W0,W1) = sz00 % 19.78/19.87 => ( W0 = sz00 % 19.78/19.87 | W1 = sz00 ) ) ) ). % 19.78/19.87 % 19.78/19.87 fof(mDefLE,definition, % 19.78/19.87 ! [W0,W1] : % 19.78/19.87 ( ( aNaturalNumber0(W0) % 19.78/19.87 & aNaturalNumber0(W1) ) % 19.78/19.87 => ( sdtlseqdt0(W0,W1) % 19.78/19.87 <=> ? [W2] : % 19.78/19.87 ( aNaturalNumber0(W2) % 19.78/19.87 & sdtpldt0(W0,W2) = W1 ) ) ) ). % 19.78/19.87 % 19.78/19.87 fof(mDefDiff,definition, % 19.78/19.87 ! [W0,W1] : % 19.78/19.87 ( ( aNaturalNumber0(W0) % 19.78/19.87 & aNaturalNumber0(W1) ) % 19.78/19.87 => ( sdtlseqdt0(W0,W1) % 19.78/19.87 => ! [W2] : % 19.78/19.87 ( W2 = sdtmndt0(W1,W0) % 19.78/19.87 <=> ( aNaturalNumber0(W2) % 19.78/19.87 & sdtpldt0(W0,W2) = W1 ) ) ) ) ). % 19.78/19.87 % 19.78/19.87 fof(mLERefl,axiom, % 19.78/19.87 ! [W0] : % 19.78/19.87 ( aNaturalNumber0(W0) % 19.78/19.87 => sdtlseqdt0(W0,W0) ) ). % 19.78/19.87 % 19.78/19.87 fof(mLEAsym,axiom, % 19.78/19.87 ! [W0,W1] : % 19.78/19.87 ( ( aNaturalNumber0(W0) % 19.78/19.87 & aNaturalNumber0(W1) ) % 19.78/19.87 => ( ( sdtlseqdt0(W0,W1) % 19.78/19.87 & sdtlseqdt0(W1,W0) ) % 19.78/19.87 => W0 = W1 ) ) ). % 19.78/19.87 % 19.78/19.87 fof(mLETran,axiom, % 19.78/19.87 ! [W0,W1,W2] : % 19.78/19.87 ( ( aNaturalNumber0(W0) % 19.78/19.87 & aNaturalNumber0(W1) % 19.78/19.87 & aNaturalNumber0(W2) ) % 19.78/19.87 => ( ( sdtlseqdt0(W0,W1) % 19.78/19.87 & sdtlseqdt0(W1,W2) ) % 19.78/19.87 => sdtlseqdt0(W0,W2) ) ) ). % 19.78/19.87 % 19.78/19.87 fof(mLETotal,axiom, % 19.78/19.87 ! [W0,W1] : % 19.78/19.87 ( ( aNaturalNumber0(W0) % 19.78/19.87 & aNaturalNumber0(W1) ) % 19.78/19.87 => ( sdtlseqdt0(W0,W1) % 19.78/19.87 | ( W1 != W0 % 19.78/19.87 & sdtlseqdt0(W1,W0) ) ) ) ). % 19.78/19.87 % 19.78/19.87 fof(mMonAdd,axiom, % 19.78/19.87 ! [W0,W1] : % 19.78/19.87 ( ( aNaturalNumber0(W0) % 19.78/19.87 & aNaturalNumber0(W1) ) % 19.78/19.87 => ( ( W0 != W1 % 19.78/19.87 & sdtlseqdt0(W0,W1) ) % 19.78/19.87 => ! [W2] : % 19.78/19.87 ( aNaturalNumber0(W2) % 19.78/19.87 => ( sdtpldt0(W2,W0) != sdtpldt0(W2,W1) % 19.78/19.87 & sdtlseqdt0(sdtpldt0(W2,W0),sdtpldt0(W2,W1)) % 19.78/19.87 & sdtpldt0(W0,W2) != sdtpldt0(W1,W2) % 19.78/19.87 & sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W2)) ) ) ) ) ). % 19.78/19.87 % 19.78/19.87 fof(mMonMul,axiom, % 19.78/19.87 ! [W0,W1,W2] : % 19.78/19.87 ( ( aNaturalNumber0(W0) % 19.78/19.87 & aNaturalNumber0(W1) % 19.78/19.87 & aNaturalNumber0(W2) ) % 19.78/19.87 => ( ( W0 != sz00 % 19.78/19.87 & W1 != W2 % 19.78/19.87 & sdtlseqdt0(W1,W2) ) % 19.78/19.87 => ( sdtasdt0(W0,W1) != sdtasdt0(W0,W2) % 19.78/19.87 & sdtlseqdt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 19.78/19.87 & sdtasdt0(W1,W0) != sdtasdt0(W2,W0) % 19.78/19.87 & sdtlseqdt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ) ). % 19.78/19.87 % 19.78/19.87 fof(mLENTr,axiom, % 19.78/19.87 ! [W0] : % 19.78/19.87 ( aNaturalNumber0(W0) % 19.78/19.87 => ( W0 = sz00 % 19.78/19.87 | W0 = sz10 % 19.78/19.87 | ( sz10 != W0 % 19.78/19.87 & sdtlseqdt0(sz10,W0) ) ) ) ). % 19.78/19.87 % 19.78/19.87 fof(mMonMul2,axiom, % 19.78/19.87 ! [W0,W1] : % 19.78/19.87 ( ( aNaturalNumber0(W0) % 19.78/19.87 & aNaturalNumber0(W1) ) % 19.78/19.87 => ( W0 != sz00 % 19.78/19.87 => sdtlseqdt0(W1,sdtasdt0(W1,W0)) ) ) ). % 19.78/19.87 % 19.78/19.87 fof(mIH,axiom, % 19.78/19.87 ! [W0,W1] : % 19.78/19.87 ( ( aNaturalNumber0(W0) % 19.78/19.87 & aNaturalNumber0(W1) ) % 19.78/19.87 => ( iLess0(W0,W1) % 19.78/19.87 => $true ) ) ). % 19.78/19.87 % 19.78/19.87 fof(mIH_03,axiom, % 19.78/19.87 ! [W0,W1] : % 19.78/19.87 ( ( aNaturalNumber0(W0) % 19.78/19.87 & aNaturalNumber0(W1) ) % 19.78/19.87 => ( ( W0 != W1 % 19.78/19.87 & sdtlseqdt0(W0,W1) ) % 19.78/19.87 => iLess0(W0,W1) ) ) ). % 19.78/19.87 % 19.78/19.87 fof(mDefDiv,definition, % 19.78/19.87 ! [W0,W1] : % 19.78/19.87 ( ( aNaturalNumber0(W0) % 19.78/19.87 & aNaturalNumber0(W1) ) % 19.78/19.87 => ( doDivides0(W0,W1) % 19.78/19.87 <=> ? [W2] : % 19.78/19.87 ( aNaturalNumber0(W2) % 19.78/19.87 & W1 = sdtasdt0(W0,W2) ) ) ) ). % 19.78/19.87 % 19.78/19.87 fof(mDefQuot,definition, % 19.78/19.87 ! [W0,W1] : % 19.78/19.87 ( ( aNaturalNumber0(W0) % 19.78/19.87 & aNaturalNumber0(W1) ) % 19.78/19.87 => ( ( W0 != sz00 % 19.78/19.87 & doDivides0(W0,W1) ) % 19.78/19.87 => ! [W2] : % 19.78/19.87 ( W2 = sdtsldt0(W1,W0) % 19.78/19.87 <=> ( aNaturalNumber0(W2) % 19.78/19.87 & W1 = sdtasdt0(W0,W2) ) ) ) ) ). % 19.78/19.87 % 19.78/19.87 fof(mDivTrans,axiom, % 19.78/19.87 ! [W0,W1,W2] : % 19.78/19.87 ( ( aNaturalNumber0(W0) % 19.78/19.87 & aNaturalNumber0(W1) % 19.78/19.87 & aNaturalNumber0(W2) ) % 19.78/19.87 => ( ( doDivides0(W0,W1) % 19.78/19.87 & doDivides0(W1,W2) ) % 19.78/19.87 => doDivides0(W0,W2) ) ) ). % 19.78/19.87 % 19.78/19.87 fof(mDivSum,axiom, % 19.78/19.87 ! [W0,W1,W2] : % 19.78/19.87 ( ( aNaturalNumber0(W0) % 19.78/19.87 & aNaturalNumber0(W1) % 19.78/19.87 & aNaturalNumber0(W2) ) % 19.78/19.87 => ( ( doDivides0(W0,W1) % 19.78/19.87 & doDivides0(W0,W2) ) % 19.78/19.87 => doDivides0(W0,sdtpldt0(W1,W2)) ) ) ). % 19.78/19.87 % 19.78/19.87 fof(m__1324,hypothesis, % 19.78/19.87 ( aNaturalNumber0(xl) % 19.78/19.87 & aNaturalNumber0(xm) % 19.78/19.87 & aNaturalNumber0(xn) ) ). % 19.78/19.87 % 19.78/19.87 fof(m__1324_04,hypothesis, % 19.78/19.87 ( ? [W0] : % 19.78/19.87 ( aNaturalNumber0(W0) % 19.78/19.87 & xm = sdtasdt0(xl,W0) ) % 19.78/19.87 & doDivides0(xl,xm) % 19.78/19.87 & ? [W0] : % 19.78/19.87 ( aNaturalNumber0(W0) % 19.78/19.87 & sdtpldt0(xm,xn) = sdtasdt0(xl,W0) ) % 19.78/19.87 & doDivides0(xl,sdtpldt0(xm,xn)) ) ). % 19.78/19.87 % 19.78/19.87 fof(m__1347,hypothesis, % 19.78/19.87 xl != sz00 ). % 19.78/19.87 % 19.78/19.87 fof(m__1360,hypothesis, % 19.78/19.87 ( aNaturalNumber0(xp) % 19.78/19.87 & xm = sdtasdt0(xl,xp) % 19.78/19.87 & xp = sdtsldt0(xm,xl) ) ). % 19.78/19.87 % 19.78/19.87 fof(m__1379,hypothesis, % 19.78/19.87 ( aNaturalNumber0(xq) % 19.78/19.87 & sdtpldt0(xm,xn) = sdtasdt0(xl,xq) % 19.78/19.87 & xq = sdtsldt0(sdtpldt0(xm,xn),xl) ) ). % 19.78/19.87 % 19.78/19.87 fof(m__1395,hypothesis, % 19.78/19.87 ( ? [W0] : % 19.78/19.87 ( aNaturalNumber0(W0) % 19.78/19.87 & sdtpldt0(xp,W0) = xq ) % 19.78/19.87 & sdtlseqdt0(xp,xq) ) ). % 19.78/19.87 % 19.78/19.87 fof(m__1422,hypothesis, % 19.78/19.87 ( aNaturalNumber0(xr) % 19.78/19.87 & sdtpldt0(xp,xr) = xq % 19.78/19.87 & xr = sdtmndt0(xq,xp) ) ). % 19.78/19.87 % 19.78/19.87 fof(m__1459,hypothesis, % 19.78/19.87 sdtpldt0(sdtasdt0(xl,xp),sdtasdt0(xl,xr)) = sdtpldt0(sdtasdt0(xl,xp),xn) ). % 19.78/19.87 % 19.78/19.87 fof(m__,conjecture, % 19.78/19.87 xn = sdtasdt0(xl,xr) ). % 19.78/19.87 % 19.78/19.87 %------------------------------------------------------------------------------ % 19.78/19.87 %------------------------------------------- % 19.78/19.87 % Proof found % 19.78/19.87 % SZS status Theorem for theBenchmark % 19.78/19.87 % SZS output start Proof % 19.78/19.87 %ClaNum:100(EqnAxiom:22) % 19.78/19.87 %VarNum:348(SingletonVarNum:109) % 19.78/19.87 %MaxLitNum:7 % 19.78/19.87 %MaxfuncDepth:2 % 19.78/19.87 %SharedTerms:51 % 19.78/19.87 %goalClause: 49 % 19.78/19.87 %singleGoalClaCount:1 % 19.78/19.87 [23]P1(a1) % 19.78/19.87 [24]P1(a11) % 19.78/19.87 [25]P1(a12) % 19.78/19.87 [26]P1(a13) % 19.78/19.87 [27]P1(a14) % 19.78/19.87 [28]P1(a15) % 19.78/19.87 [29]P1(a16) % 19.78/19.87 [30]P1(a17) % 19.78/19.87 [31]P1(a2) % 19.78/19.87 [32]P1(a5) % 19.78/19.87 [33]P1(a6) % 19.78/19.87 [40]P2(a15,a16) % 19.78/19.87 [41]P3(a12,a13) % 19.78/19.87 [47]~E(a1,a11) % 19.78/19.87 [48]~E(a1,a12) % 19.78/19.87 [34]E(f7(a12,a15),a13) % 19.78/19.87 [35]E(f7(a12,a2),a13) % 19.78/19.87 [36]E(f8(a13,a12),a15) % 19.78/19.87 [37]E(f9(a16,a15),a17) % 19.78/19.87 [38]E(f10(a15,a17),a16) % 19.78/19.87 [39]E(f10(a15,a6),a16) % 19.78/19.87 [42]E(f10(a13,a14),f7(a12,a16)) % 19.78/19.87 [43]E(f10(a13,a14),f7(a12,a5)) % 19.78/19.87 [45]P3(a12,f10(a13,a14)) % 19.78/19.87 [49]~E(f7(a12,a17),a14) % 19.78/19.87 [44]E(f8(f10(a13,a14),a12),a16) % 19.78/19.87 [46]E(f10(f7(a12,a15),f7(a12,a17)),f10(f7(a12,a15),a14)) % 19.78/19.88 [56]~P1(x561)+P2(x561,x561) % 19.78/19.88 [50]~P1(x501)+E(f7(a1,x501),a1) % 19.78/19.88 [51]~P1(x511)+E(f7(x511,a1),a1) % 19.78/19.88 [52]~P1(x521)+E(f10(a1,x521),x521) % 19.78/19.88 [53]~P1(x531)+E(f7(a11,x531),x531) % 19.78/19.88 [54]~P1(x541)+E(f10(x541,a1),x541) % 19.78/19.88 [55]~P1(x551)+E(f7(x551,a11),x551) % 19.78/19.88 [62]~P1(x622)+~P1(x621)+E(f10(x621,x622),f10(x622,x621)) % 19.78/19.88 [63]~P1(x632)+~P1(x631)+E(f7(x631,x632),f7(x632,x631)) % 19.78/19.88 [65]~P1(x652)+~P1(x651)+P1(f10(x651,x652)) % 19.78/19.88 [66]~P1(x662)+~P1(x661)+P1(f7(x661,x662)) % 19.78/19.88 [57]~P1(x571)+E(x571,a11)+P2(a11,x571)+E(x571,a1) % 19.78/19.88 [58]~E(x582,x581)+~P1(x581)+~P1(x582)+P2(x581,x582) % 19.78/19.88 [64]P2(x642,x641)+~P1(x641)+~P1(x642)+P2(x641,x642) % 19.78/19.88 [59]~P1(x592)+~P1(x591)+E(x591,a1)+~E(f10(x592,x591),a1) % 19.78/19.88 [60]~P1(x602)+~P1(x601)+E(x601,a1)+~E(f10(x601,x602),a1) % 19.78/19.88 [68]~P1(x682)+~P1(x681)+P2(x682,f7(x682,x681))+E(x681,a1) % 19.78/19.88 [74]~P1(x742)+~P1(x741)+~P2(x741,x742)+P1(f3(x741,x742)) % 19.78/19.88 [75]~P1(x752)+~P1(x751)+~P3(x751,x752)+P1(f4(x751,x752)) % 19.78/19.88 [82]~P1(x821)+~P1(x822)+~P3(x821,x822)+E(f7(x821,f4(x821,x822)),x822) % 19.78/19.88 [83]~P1(x832)+~P1(x831)+~P2(x831,x832)+E(f10(x831,f3(x831,x832)),x832) % 19.78/19.88 [92]~P1(x923)+~P1(x922)+~P1(x921)+E(f10(f10(x921,x922),x923),f10(x921,f10(x922,x923))) % 19.78/19.88 [93]~P1(x933)+~P1(x932)+~P1(x931)+E(f7(f7(x931,x932),x933),f7(x931,f7(x932,x933))) % 19.78/19.88 [99]~P1(x993)+~P1(x992)+~P1(x991)+E(f10(f7(x991,x992),f7(x991,x993)),f7(x991,f10(x992,x993))) % 19.78/19.88 [100]~P1(x1002)+~P1(x1003)+~P1(x1001)+E(f10(f7(x1001,x1002),f7(x1003,x1002)),f7(f10(x1001,x1003),x1002)) % 19.78/19.88 [67]P4(x671,x672)+~P1(x672)+~P1(x671)+~P2(x671,x672)+E(x671,x672) % 19.78/19.88 [71]~P1(x712)+~P1(x711)+~P2(x712,x711)+~P2(x711,x712)+E(x711,x712) % 19.78/19.88 [61]~P1(x611)+~P1(x612)+E(x611,a1)+E(x612,a1)+~E(f7(x612,x611),a1) % 19.78/19.88 [69]~P1(x691)+~P1(x692)+~P1(x693)+P3(x691,x692)+~E(x692,f7(x691,x693)) % 19.78/19.88 [70]~P1(x702)+~P1(x701)+~P1(x703)+P2(x701,x702)+~E(f10(x701,x703),x702) % 19.78/19.88 [72]~P1(x723)+~P1(x722)+~P2(x723,x722)+P1(x721)+~E(x721,f9(x722,x723)) % 19.78/19.88 [76]~P1(x762)+~P1(x761)+~P1(x763)+E(x761,x762)+~E(f10(x763,x761),f10(x763,x762)) % 19.78/19.88 [77]~P1(x772)+~P1(x773)+~P1(x771)+E(x771,x772)+~E(f10(x771,x773),f10(x772,x773)) % 19.78/19.88 [80]~P1(x803)+~P1(x801)+~P2(x801,x803)+~E(x802,f9(x803,x801))+E(f10(x801,x802),x803) % 19.78/19.88 [84]~P1(x842)+~P1(x841)+~P2(x843,x842)+~P2(x841,x843)+P2(x841,x842)+~P1(x843) % 19.78/19.88 [85]~P1(x852)+~P1(x851)+~P3(x853,x852)+~P3(x851,x853)+P3(x851,x852)+~P1(x853) % 19.78/19.88 [73]~P1(x731)+~P1(x733)+~P3(x731,x733)+P1(x732)+E(x731,a1)+~E(x732,f8(x733,x731)) % 19.78/19.88 [78]~P1(x782)+~P1(x781)+~P1(x783)+E(x781,x782)+~E(f7(x783,x781),f7(x783,x782))+E(x783,a1) % 19.78/19.88 [79]~P1(x792)+~P1(x793)+~P1(x791)+E(x791,x792)+~E(f7(x791,x793),f7(x792,x793))+E(x793,a1) % 19.78/19.88 [81]~P1(x811)+~P1(x812)+~P3(x811,x812)+~E(x813,f8(x812,x811))+E(x811,a1)+E(x812,f7(x811,x813)) % 19.78/19.88 [86]~P1(x862)+~P1(x863)+~P1(x861)+~P2(x863,x862)+~E(f10(x863,x861),x862)+E(x861,f9(x862,x863)) % 19.78/19.88 [94]~P1(x943)+~P1(x942)+~P1(x941)+~P3(x941,x943)+~P3(x941,x942)+P3(x941,f10(x942,x943)) % 19.78/19.88 [95]~P1(x952)+~P1(x951)+~P1(x953)+~P2(x951,x952)+E(x951,x952)+P2(f10(x953,x951),f10(x953,x952)) % 19.78/19.88 [96]~P1(x962)+~P1(x963)+~P1(x961)+~P2(x961,x962)+E(x961,x962)+P2(f10(x961,x963),f10(x962,x963)) % 19.78/19.88 [87]~P1(x871)+~P1(x873)+~P1(x872)+~P3(x871,x873)+~E(x873,f7(x871,x872))+E(x871,a1)+E(x872,f8(x873,x871)) % 19.78/19.88 [97]~P1(x972)+~P1(x971)+~P1(x973)+~P2(x971,x972)+E(x971,x972)+P2(f7(x973,x971),f7(x973,x972))+E(x973,a1) % 19.78/19.88 [98]~P1(x982)+~P1(x983)+~P1(x981)+~P2(x981,x982)+E(x981,x982)+P2(f7(x981,x983),f7(x982,x983))+E(x983,a1) % 19.78/19.88 %EqnAxiom % 19.78/19.88 [1]E(x11,x11) % 19.78/19.88 [2]E(x22,x21)+~E(x21,x22) % 19.78/19.88 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 19.78/19.88 [4]~E(x41,x42)+E(f7(x41,x43),f7(x42,x43)) % 19.78/19.88 [5]~E(x51,x52)+E(f7(x53,x51),f7(x53,x52)) % 19.78/19.88 [6]~E(x61,x62)+E(f10(x61,x63),f10(x62,x63)) % 19.78/19.88 [7]~E(x71,x72)+E(f10(x73,x71),f10(x73,x72)) % 19.78/19.88 [8]~E(x81,x82)+E(f8(x81,x83),f8(x82,x83)) % 19.78/19.88 [9]~E(x91,x92)+E(f8(x93,x91),f8(x93,x92)) % 19.78/19.88 [10]~E(x101,x102)+E(f9(x101,x103),f9(x102,x103)) % 19.78/19.88 [11]~E(x111,x112)+E(f9(x113,x111),f9(x113,x112)) % 19.78/19.88 [12]~E(x121,x122)+E(f4(x121,x123),f4(x122,x123)) % 19.78/19.88 [13]~E(x131,x132)+E(f4(x133,x131),f4(x133,x132)) % 19.78/19.88 [14]~E(x141,x142)+E(f3(x141,x143),f3(x142,x143)) % 19.78/19.88 [15]~E(x151,x152)+E(f3(x153,x151),f3(x153,x152)) % 19.78/19.88 [16]~P1(x161)+P1(x162)+~E(x161,x162) % 19.78/19.88 [17]P2(x172,x173)+~E(x171,x172)+~P2(x171,x173) % 19.78/19.88 [18]P2(x183,x182)+~E(x181,x182)+~P2(x183,x181) % 19.78/19.88 [19]P4(x192,x193)+~E(x191,x192)+~P4(x191,x193) % 19.78/19.88 [20]P4(x203,x202)+~E(x201,x202)+~P4(x203,x201) % 19.78/19.88 [21]P3(x212,x213)+~E(x211,x212)+~P3(x211,x213) % 19.78/19.88 [22]P3(x223,x222)+~E(x221,x222)+~P3(x223,x221) % 19.78/19.88 % 19.78/19.88 %------------------------------------------- % 19.78/19.88 cnf(102,plain, % 19.78/19.88 (P3(x1021,f7(x1021,x1022))+~P1(x1021)+~P1(f7(x1021,x1022))+~P1(x1022)), % 19.78/19.88 inference(equality_inference,[],[69])). % 19.78/19.88 cnf(103,plain, % 19.78/19.88 (P2(x1031,f10(x1031,x1032))+~P1(f10(x1031,x1032))+~P1(x1031)+~P1(x1032)), % 19.78/19.88 inference(equality_inference,[],[70])). % 19.78/19.88 cnf(104,plain, % 19.78/19.88 (~P2(x1041,x1042)+~P1(x1041)+~P1(x1042)+P1(f9(x1042,x1041))), % 19.78/19.88 inference(equality_inference,[],[72])). % 19.78/19.88 cnf(110,plain, % 19.78/19.88 (~P2(x1101,x1102)+~P1(x1102)+~P1(x1101)+E(f10(x1101,f9(x1102,x1101)),x1102)), % 19.78/19.88 inference(equality_inference,[],[80])). % 19.78/19.88 cnf(112,plain, % 19.78/19.88 (~P2(x1121,f10(x1121,x1122))+~P1(f10(x1121,x1122))+~P1(x1121)+~P1(x1122)+E(x1122,f9(f10(x1121,x1122),x1121))), % 19.78/19.88 inference(equality_inference,[],[86])). % 19.78/19.88 cnf(114,plain, % 19.78/19.88 (E(f7(a12,a5),f10(a13,a14))), % 19.78/19.88 inference(scs_inference,[],[43,2])). % 19.78/19.88 cnf(115,plain, % 19.78/19.88 (E(f7(a12,a5),f7(a12,a16))), % 19.78/19.88 inference(scs_inference,[],[43,42,2,3])). % 19.78/19.88 cnf(116,plain, % 19.78/19.88 (P3(a12,f7(a12,a5))), % 19.78/19.88 inference(scs_inference,[],[43,42,45,2,3,22])). % 19.78/19.88 cnf(117,plain, % 19.78/19.88 (P2(a1,a1)), % 19.78/19.88 inference(scs_inference,[],[23,43,42,45,2,3,22,64])). % 19.78/19.88 cnf(119,plain, % 19.78/19.88 (P1(f9(a1,a1))), % 19.78/19.88 inference(scs_inference,[],[23,43,42,45,2,3,22,64,104])). % 19.78/19.88 cnf(121,plain, % 19.78/19.88 (E(f10(a1,f9(a1,a1)),a1)), % 19.78/19.88 inference(scs_inference,[],[23,43,42,45,2,3,22,64,104,110])). % 19.78/19.88 cnf(123,plain, % 19.78/19.88 (E(a17,f9(a16,a15))), % 19.78/19.88 inference(scs_inference,[],[23,28,29,30,43,40,42,45,38,2,3,22,64,104,110,86])). % 19.78/19.88 cnf(126,plain, % 19.78/19.88 (E(f9(a1,a1),a1)), % 19.78/19.88 inference(scs_inference,[],[23,28,29,30,43,40,42,45,38,2,3,22,64,104,110,86,16,59])). % 19.78/19.88 cnf(129,plain, % 19.78/19.88 (E(f7(a12,a16),f7(a12,a5))), % 19.78/19.88 inference(scs_inference,[],[115,2])). % 19.78/19.88 cnf(130,plain, % 19.78/19.88 (P1(f9(a16,a15))), % 19.78/19.88 inference(scs_inference,[],[115,30,123,2,16])). % 19.78/19.88 cnf(131,plain, % 19.78/19.88 (P3(a12,f7(a12,a16))), % 19.78/19.88 inference(scs_inference,[],[115,30,123,42,45,2,16,22])). % 19.78/19.88 cnf(132,plain, % 19.78/19.88 (P2(a11,a11)), % 19.78/19.88 inference(scs_inference,[],[115,24,30,123,42,45,2,16,22,64])). % 19.78/19.88 cnf(134,plain, % 19.78/19.88 (E(a6,f9(a16,a15))), % 19.78/19.88 inference(scs_inference,[],[115,24,33,28,29,30,39,123,42,45,40,2,16,22,64,86])). % 19.78/19.88 cnf(136,plain, % 19.78/19.88 (P2(x1361,a1)+~E(a1,x1361)), % 19.78/19.88 inference(scs_inference,[],[115,24,33,28,29,30,39,117,123,42,45,40,2,16,22,64,86,17])). % 19.78/19.88 cnf(137,plain, % 19.78/19.88 (P1(f9(a11,a11))), % 19.78/19.88 inference(scs_inference,[],[115,24,33,28,29,30,39,117,123,42,45,40,2,16,22,64,86,17,104])). % 19.78/19.88 cnf(139,plain, % 19.78/19.88 (E(f10(a11,f9(a11,a11)),a11)), % 19.78/19.88 inference(scs_inference,[],[115,24,33,28,29,30,39,117,123,42,45,40,2,16,22,64,86,17,104,110])). % 19.78/19.88 cnf(147,plain, % 19.78/19.88 (E(a1,f10(a1,f9(a1,a1)))), % 19.78/19.88 inference(scs_inference,[],[121,2])). % 19.78/19.88 cnf(148,plain, % 19.78/19.88 (P1(f10(a1,f9(a1,a1)))), % 19.78/19.88 inference(scs_inference,[],[23,121,2,16])). % 19.78/19.88 cnf(150,plain, % 19.78/19.88 (P2(f10(a1,f9(a1,a1)),a1)), % 19.78/19.88 inference(scs_inference,[],[114,129,23,121,117,2,16,3,17])). % 19.78/19.88 cnf(152,plain, % 19.78/19.88 (P2(a12,a12)), % 19.78/19.88 inference(scs_inference,[],[114,129,25,23,121,117,2,16,3,17,18,64])). % 19.78/19.88 cnf(154,plain, % 19.78/19.88 (P3(a12,x1541)+~E(a13,x1541)), % 19.78/19.88 inference(scs_inference,[],[114,129,25,23,121,41,117,2,16,3,17,18,64,22])). % 19.78/19.88 cnf(155,plain, % 19.78/19.88 (E(f10(a12,f9(a12,a12)),a12)), % 19.78/19.88 inference(scs_inference,[],[114,129,25,23,121,41,117,2,16,3,17,18,64,22,110])). % 19.78/19.88 cnf(157,plain, % 19.78/19.88 (P1(f9(a12,a12))), % 19.78/19.88 inference(scs_inference,[],[114,129,25,23,121,41,117,2,16,3,17,18,64,22,110,104])). % 19.78/19.88 cnf(159,plain, % 19.78/19.88 (P3(x1591,f7(a12,a16))+~E(a12,x1591)), % 19.78/19.88 inference(scs_inference,[],[114,129,25,23,121,131,41,117,2,16,3,17,18,64,22,110,104,21])). % 19.78/19.88 cnf(164,plain, % 19.78/19.88 (P2(a2,a2)), % 19.78/19.88 inference(scs_inference,[],[114,129,25,31,23,121,131,41,117,2,16,3,17,18,64,22,110,104,21,102,103,58])). % 19.78/19.88 cnf(170,plain, % 19.78/19.88 (E(a16,f10(a15,a17))), % 19.78/19.88 inference(scs_inference,[],[38,2])). % 19.78/19.88 cnf(172,plain, % 19.78/19.88 (P1(f10(a15,a17))), % 19.78/19.88 inference(scs_inference,[],[29,38,139,47,2,3,16])). % 19.78/19.88 cnf(174,plain, % 19.78/19.88 (E(f10(a2,f9(a2,a2)),a2)), % 19.78/19.88 inference(scs_inference,[],[147,31,29,38,139,150,47,164,2,3,16,18,110])). % 19.78/19.88 cnf(176,plain, % 19.78/19.88 (P1(f9(a2,a2))), % 19.78/19.88 inference(scs_inference,[],[147,31,29,38,139,150,47,164,2,3,16,18,110,104])). % 19.78/19.88 cnf(178,plain, % 19.78/19.88 (P2(a5,a5)), % 19.78/19.88 inference(scs_inference,[],[147,32,31,29,38,139,150,47,164,2,3,16,18,110,104,64])). % 19.78/19.88 cnf(181,plain, % 19.78/19.88 (P3(x1811,f7(a12,a5))+~E(a12,x1811)), % 19.78/19.88 inference(scs_inference,[],[147,32,31,29,38,139,132,150,47,164,116,2,3,16,18,110,104,64,17,21])). % 19.78/19.88 cnf(186,plain, % 19.78/19.88 (P2(a13,a13)), % 19.78/19.88 inference(scs_inference,[],[147,32,26,31,29,38,139,132,150,47,164,116,2,3,16,18,110,104,64,17,21,102,103,58])). % 19.78/19.88 cnf(188,plain, % 19.78/19.88 (~P1(f7(a12,a17))+~P1(f7(a12,a15))), % 19.78/19.88 inference(scs_inference,[],[49,147,32,26,27,31,29,38,139,132,150,47,164,46,116,2,3,16,18,110,104,64,17,21,102,103,58,76])). % 19.78/19.88 cnf(192,plain, % 19.78/19.88 (E(a16,f10(a15,a6))), % 19.78/19.88 inference(scs_inference,[],[39,2])). % 19.78/19.88 cnf(193,plain, % 19.78/19.88 (P1(f10(a15,a6))), % 19.78/19.88 inference(scs_inference,[],[29,39,2,16])). % 19.78/19.88 cnf(194,plain, % 19.78/19.88 (E(f10(a15,a6),f10(a15,a17))), % 19.78/19.88 inference(scs_inference,[],[170,29,39,2,16,3])). % 19.78/19.88 cnf(195,plain, % 19.78/19.88 (P2(a15,f10(a15,a17))), % 19.78/19.88 inference(scs_inference,[],[170,29,39,40,2,16,3,18])). % 19.78/19.88 cnf(196,plain, % 19.78/19.88 (E(f10(a5,f9(a5,a5)),a5)), % 19.78/19.88 inference(scs_inference,[],[170,32,29,39,178,40,2,16,3,18,110])). % 19.78/19.88 cnf(198,plain, % 19.78/19.88 (P1(f9(a5,a5))), % 19.78/19.88 inference(scs_inference,[],[170,32,29,39,178,40,2,16,3,18,110,104])). % 19.78/19.88 cnf(200,plain, % 19.78/19.88 (P2(a6,a6)), % 19.78/19.88 inference(scs_inference,[],[170,32,33,29,39,178,40,2,16,3,18,110,104,64])). % 19.78/19.88 cnf(202,plain, % 19.78/19.88 (E(a6,a17)), % 19.78/19.88 inference(scs_inference,[],[170,32,33,30,28,29,39,178,40,2,16,3,18,110,104,64,76])). % 19.78/19.88 cnf(204,plain, % 19.78/19.88 (E(a6,f9(f10(a15,a17),a15))), % 19.78/19.88 inference(scs_inference,[],[170,32,33,30,28,29,39,178,172,40,2,16,3,18,110,104,64,76,86])). % 19.78/19.88 cnf(211,plain, % 19.78/19.88 (E(f10(a15,a17),f10(a15,a6))), % 19.78/19.88 inference(scs_inference,[],[194,2])). % 19.78/19.88 cnf(213,plain, % 19.78/19.88 (P1(f9(f10(a15,a17),a15))), % 19.78/19.88 inference(scs_inference,[],[194,33,155,204,48,2,3,16])). % 19.78/19.88 cnf(214,plain, % 19.78/19.88 (P2(a17,a6)), % 19.78/19.88 inference(scs_inference,[],[194,202,33,155,204,48,200,2,3,16,17])). % 19.78/19.88 cnf(215,plain, % 19.78/19.88 (P2(a6,a17)), % 19.78/19.88 inference(scs_inference,[],[194,202,33,155,204,48,200,2,3,16,17,18])). % 19.78/19.88 cnf(216,plain, % 19.78/19.88 (E(f10(a13,f9(a13,a13)),a13)), % 19.78/19.88 inference(scs_inference,[],[194,202,26,33,155,204,48,186,200,2,3,16,17,18,110])). % 19.78/19.88 cnf(218,plain, % 19.78/19.88 (P1(f9(a13,a13))), % 19.78/19.88 inference(scs_inference,[],[194,202,26,33,155,204,48,186,200,2,3,16,17,18,110,104])). % 19.78/19.88 cnf(220,plain, % 19.78/19.88 (P2(a14,a14)), % 19.78/19.88 inference(scs_inference,[],[194,202,26,27,33,155,204,48,186,200,2,3,16,17,18,110,104,64])). % 19.78/19.88 cnf(222,plain, % 19.78/19.88 (P2(a15,f10(a15,a6))), % 19.78/19.88 inference(scs_inference,[],[194,202,26,27,30,33,28,155,193,204,48,186,200,2,3,16,17,18,110,104,64,70])). % 19.78/19.88 cnf(224,plain, % 19.78/19.88 (E(a17,a6)), % 19.78/19.88 inference(scs_inference,[],[194,202,26,27,30,33,28,155,193,204,48,186,200,2,3,16,17,18,110,104,64,70,71])). % 19.78/19.88 cnf(226,plain, % 19.78/19.88 (E(a17,f9(f10(a15,a6),a15))), % 19.78/19.88 inference(scs_inference,[],[194,202,26,27,30,33,28,155,193,204,48,186,200,2,3,16,17,18,110,104,64,70,71,86])). % 19.78/19.88 cnf(232,plain, % 19.78/19.88 (E(f9(a16,a15),a6)), % 19.78/19.88 inference(scs_inference,[],[134,2])). % 19.78/19.88 cnf(233,plain, % 19.78/19.88 (P1(f9(f10(a15,a6),a15))), % 19.78/19.88 inference(scs_inference,[],[30,134,226,2,16])). % 19.78/19.88 cnf(234,plain, % 19.78/19.88 (E(a17,f9(f10(a15,a17),a15))), % 19.78/19.88 inference(scs_inference,[],[224,30,134,204,226,2,16,3])). % 19.78/19.88 cnf(235,plain, % 19.78/19.88 (P2(a17,a17)), % 19.78/19.88 inference(scs_inference,[],[224,202,30,134,204,226,215,2,16,3,17])). % 19.78/19.88 cnf(236,plain, % 19.78/19.88 (E(f10(a14,f9(a14,a14)),a14)), % 19.78/19.88 inference(scs_inference,[],[224,202,27,30,134,204,226,215,220,2,16,3,17,110])). % 19.78/19.88 cnf(238,plain, % 19.78/19.88 (P1(f9(a14,a14))), % 19.78/19.88 inference(scs_inference,[],[224,202,27,30,134,204,226,215,220,2,16,3,17,110,104])). % 19.78/19.88 cnf(240,plain, % 19.78/19.88 (P2(a16,a16)), % 19.78/19.88 inference(scs_inference,[],[224,202,27,29,30,134,204,226,215,220,2,16,3,17,110,104,64])). % 19.78/19.88 cnf(243,plain, % 19.78/19.88 (P3(x2431,f10(a13,a14))+~E(a12,x2431)), % 19.78/19.88 inference(scs_inference,[],[224,202,27,29,30,134,152,45,204,226,215,220,2,16,3,17,110,104,64,18,21])). % 19.78/19.88 cnf(248,plain, % 19.78/19.88 (P2(a15,a15)), % 19.78/19.88 inference(scs_inference,[],[224,202,27,29,30,28,134,152,45,204,226,215,220,2,16,3,17,110,104,64,18,21,102,103,58])). % 19.78/19.88 cnf(253,plain, % 19.78/19.88 (E(f9(f10(a15,a17),a15),a17)), % 19.78/19.88 inference(scs_inference,[],[234,2])). % 19.78/19.88 cnf(254,plain, % 19.78/19.88 (E(f9(a16,a15),f9(f10(a15,a17),a15))), % 19.78/19.88 inference(scs_inference,[],[232,234,204,2,3])). % 19.78/19.88 cnf(255,plain, % 19.78/19.88 (P2(a6,f9(f10(a15,a17),a15))), % 19.78/19.88 inference(scs_inference,[],[232,234,204,215,2,3,18])). % 19.78/19.88 cnf(256,plain, % 19.78/19.88 (P2(f9(f10(a15,a17),a15),a6)), % 19.78/19.88 inference(scs_inference,[],[232,234,204,214,215,2,3,18,17])). % 19.78/19.88 cnf(257,plain, % 19.78/19.88 (E(f10(a6,f9(a6,a6)),a6)), % 19.78/19.88 inference(scs_inference,[],[232,234,33,204,214,215,200,2,3,18,17,110])). % 19.78/19.88 cnf(259,plain, % 19.78/19.88 (P1(f9(a6,a6))), % 19.78/19.88 inference(scs_inference,[],[232,234,33,204,214,215,200,2,3,18,17,110,104])). % 19.78/19.88 cnf(261,plain, % 19.78/19.88 (P2(f9(a16,a15),f9(a16,a15))), % 19.78/19.88 inference(scs_inference,[],[232,234,33,204,214,215,130,200,2,3,18,17,110,104,64])). % 19.78/19.88 cnf(263,plain, % 19.78/19.88 (E(f9(f10(a15,a17),a15),a6)), % 19.78/19.88 inference(scs_inference,[],[232,234,33,204,214,215,130,213,200,2,3,18,17,110,104,64,71])). % 19.78/19.88 cnf(269,plain, % 19.78/19.88 (E(f9(f10(a15,a17),a15),f9(a16,a15))), % 19.78/19.88 inference(scs_inference,[],[254,2])). % 19.78/19.88 cnf(270,plain, % 19.78/19.88 (E(f9(f10(a15,a17),a15),f9(f10(a15,a6),a15))), % 19.78/19.88 inference(scs_inference,[],[254,253,226,2,3])). % 19.78/19.88 cnf(271,plain, % 19.78/19.88 (P2(f9(a16,a15),f9(f10(a15,a17),a15))), % 19.78/19.88 inference(scs_inference,[],[254,253,226,261,2,3,18])). % 19.78/19.88 cnf(272,plain, % 19.78/19.88 (P2(f9(f10(a15,a17),a15),f9(a16,a15))), % 19.78/19.88 inference(scs_inference,[],[254,253,226,261,2,3,18,17])). % 19.78/19.88 cnf(273,plain, % 19.78/19.88 (E(f10(a16,f9(a16,a16)),a16)), % 19.78/19.88 inference(scs_inference,[],[254,253,29,226,261,240,2,3,18,17,110])). % 19.78/19.88 cnf(275,plain, % 19.78/19.88 (P1(f9(a16,a16))), % 19.78/19.88 inference(scs_inference,[],[254,253,29,226,261,240,2,3,18,17,110,104])). % 19.78/19.88 cnf(277,plain, % 19.78/19.88 (P2(f9(a12,a12),f9(a12,a12))), % 19.78/19.88 inference(scs_inference,[],[254,253,29,226,261,240,157,2,3,18,17,110,104,64])). % 19.78/19.88 cnf(284,plain, % 19.78/19.88 (P2(a6,f9(a16,a15))), % 19.78/19.88 inference(scs_inference,[],[269,270,255,2,18])). % 19.78/19.88 cnf(286,plain, % 19.78/19.88 (P2(a17,f9(f10(a15,a17),a15))), % 19.78/19.88 inference(scs_inference,[],[49,269,270,202,236,255,2,18,3,17])). % 19.78/19.88 cnf(287,plain, % 19.78/19.88 (E(f10(a17,f9(a17,a17)),a17)), % 19.78/19.88 inference(scs_inference,[],[49,269,270,202,30,236,255,235,2,18,3,17,110])). % 19.78/19.88 cnf(289,plain, % 19.78/19.88 (P1(f9(a17,a17))), % 19.78/19.88 inference(scs_inference,[],[49,269,270,202,30,236,255,235,2,18,3,17,110,104])). % 19.78/19.88 cnf(291,plain, % 19.78/19.88 (P2(f9(a2,a2),f9(a2,a2))), % 19.78/19.88 inference(scs_inference,[],[49,269,270,202,30,236,255,235,176,2,18,3,17,110,104,64])). % 19.78/19.88 cnf(297,plain, % 19.78/19.88 (P1(f10(a11,f9(a11,a11)))), % 19.78/19.88 inference(scs_inference,[],[24,139,2,16])). % 19.78/19.88 cnf(298,plain, % 19.78/19.88 (P2(f9(f10(a15,a17),a15),a17)), % 19.78/19.88 inference(scs_inference,[],[202,24,139,256,2,16,18])). % 19.78/19.88 cnf(300,plain, % 19.78/19.88 (E(f10(a15,f9(a15,a15)),a15)), % 19.78/19.88 inference(scs_inference,[],[269,202,24,28,139,256,248,2,16,18,17,110])). % 19.78/19.88 cnf(302,plain, % 19.78/19.88 (P1(f9(a15,a15))), % 19.78/19.88 inference(scs_inference,[],[269,202,24,28,139,256,248,2,16,18,17,110,104])). % 19.78/19.88 cnf(304,plain, % 19.78/19.88 (P2(f9(a5,a5),f9(a5,a5))), % 19.78/19.88 inference(scs_inference,[],[269,202,24,28,139,256,248,198,2,16,18,17,110,104,64])). % 19.78/19.88 cnf(317,plain, % 19.78/19.88 (E(a12,f10(a12,f9(a12,a12)))), % 19.78/19.88 inference(scs_inference,[],[155,2])). % 19.78/19.88 cnf(321,plain, % 19.78/19.88 (P2(f10(a12,f9(a12,a12)),a12)), % 19.78/19.88 inference(scs_inference,[],[25,41,155,152,2,16,18,21,17])). % 19.78/19.88 cnf(322,plain, % 19.78/19.88 (E(f10(f9(a16,a15),f9(f9(a16,a15),f9(a16,a15))),f9(a16,a15))), % 19.78/19.88 inference(scs_inference,[],[25,41,155,152,130,261,2,16,18,21,17,110])). % 19.78/19.88 cnf(326,plain, % 19.78/19.88 (P2(f10(a11,f9(a11,a11)),f10(a11,f9(a11,a11)))), % 19.78/19.88 inference(scs_inference,[],[25,41,155,152,297,130,261,2,16,18,21,17,110,104,64])). % 19.78/19.88 cnf(333,plain, % 19.78/19.88 (P3(f10(a12,f9(a12,a12)),x3331)+~E(a13,x3331)), % 19.78/19.88 inference(scs_inference,[],[25,29,28,41,155,152,297,130,261,40,2,16,18,21,17,110,104,64,72,243,159,181,22])). % 19.78/19.88 cnf(339,plain, % 19.78/19.88 (P2(f9(a13,a13),f9(a13,a13))), % 19.78/19.88 inference(scs_inference,[],[25,31,29,28,41,155,152,196,297,218,130,261,40,2,16,18,21,17,110,104,64,72,243,159,181,22,3,102,103,58])). % 19.78/19.88 cnf(346,plain, % 19.78/19.88 (E(a6,f9(f10(a15,a6),a15))), % 19.78/19.88 inference(scs_inference,[],[202,174,226,2,3])). % 19.78/19.88 cnf(347,plain, % 19.78/19.88 (P1(f10(a2,f9(a2,a2)))), % 19.78/19.88 inference(scs_inference,[],[202,31,174,226,2,3,16])). % 19.78/19.88 cnf(348,plain, % 19.78/19.88 (P2(a6,f9(f10(a15,a6),a15))), % 19.78/19.88 inference(scs_inference,[],[270,202,31,174,226,255,2,3,16,18])). % 19.78/19.88 cnf(349,plain, % 19.78/19.88 (P2(f9(f10(a15,a6),a15),a6)), % 19.78/19.88 inference(scs_inference,[],[270,202,31,174,226,255,256,2,3,16,18,17])). % 19.78/19.88 cnf(350,plain, % 19.78/19.88 (E(f10(f9(a12,a12),f9(f9(a12,a12),f9(a12,a12))),f9(a12,a12))), % 19.78/19.88 inference(scs_inference,[],[270,202,31,174,226,255,256,277,157,2,3,16,18,17,110])). % 19.78/19.88 cnf(366,plain, % 19.78/19.88 (P1(f10(a13,f9(a13,a13)))), % 19.78/19.88 inference(scs_inference,[],[26,216,2,16])). % 19.78/19.88 cnf(369,plain, % 19.78/19.88 (P2(a17,f9(a16,a15))), % 19.78/19.88 inference(scs_inference,[],[254,202,26,41,216,272,284,2,16,18,22,17])). % 19.78/19.88 cnf(371,plain, % 19.78/19.88 (E(f10(f9(a2,a2),f9(f9(a2,a2),f9(a2,a2))),f9(a2,a2))), % 19.78/19.88 inference(scs_inference,[],[317,254,202,26,41,216,272,284,291,176,2,16,18,22,17,21,110])). % 19.78/19.88 cnf(393,plain, % 19.78/19.88 (E(a5,f10(a5,f9(a5,a5)))), % 19.78/19.88 inference(scs_inference,[],[196,2])). % 19.78/19.88 cnf(394,plain, % 19.78/19.88 (P1(f10(a5,f9(a5,a5)))), % 19.78/19.88 inference(scs_inference,[],[32,196,2,16])). % 19.78/19.88 cnf(397,plain, % 19.78/19.88 (E(f10(f9(a5,a5),f9(f9(a5,a5),f9(a5,a5))),f9(a5,a5))), % 19.78/19.88 inference(scs_inference,[],[317,269,32,196,321,298,304,198,2,16,18,17,110])). % 19.78/19.88 cnf(399,plain, % 19.78/19.88 (P1(f9(f9(a5,a5),f9(a5,a5)))), % 19.78/19.88 inference(scs_inference,[],[317,269,32,196,321,298,304,198,2,16,18,17,110,104])). % 19.78/19.88 cnf(421,plain, % 19.78/19.88 (P2(f9(f10(a15,a6),a15),a17)), % 19.78/19.88 inference(scs_inference,[],[202,236,349,2,18])). % 19.78/19.88 cnf(422,plain, % 19.78/19.88 (P1(f10(a14,f9(a14,a14)))), % 19.78/19.88 inference(scs_inference,[],[202,27,236,349,2,18,16])). % 19.78/19.88 cnf(423,plain, % 19.78/19.88 (P2(a17,f9(f10(a15,a6),a15))), % 19.78/19.88 inference(scs_inference,[],[202,27,236,348,349,2,18,16,17])). % 19.78/19.88 cnf(424,plain, % 19.78/19.88 (E(f10(f9(a13,a13),f9(f9(a13,a13),f9(a13,a13))),f9(a13,a13))), % 19.78/19.88 inference(scs_inference,[],[202,27,236,348,349,339,218,2,18,16,17,110])). % 19.78/19.88 cnf(426,plain, % 19.78/19.88 (P1(f9(f9(a13,a13),f9(a13,a13)))), % 19.78/19.88 inference(scs_inference,[],[202,27,236,348,349,339,218,2,18,16,17,110,104])). % 19.78/19.88 cnf(428,plain, % 19.78/19.88 (P2(f9(f9(a5,a5),f9(a5,a5)),f9(f9(a5,a5),f9(a5,a5)))), % 19.78/19.88 inference(scs_inference,[],[202,27,236,348,349,399,339,218,2,18,16,17,110,104,64])). % 19.78/19.88 cnf(449,plain, % 19.78/19.88 (P1(f3(a12,a12))), % 19.78/19.88 inference(scs_inference,[],[25,56,74])). % 19.78/19.88 cnf(450,plain, % 19.78/19.88 (E(a6,f10(a6,f9(a6,a6)))), % 19.78/19.88 inference(scs_inference,[],[257,2])). % 19.78/19.88 cnf(451,plain, % 19.78/19.88 (P1(f10(a6,f9(a6,a6)))), % 19.78/19.88 inference(scs_inference,[],[33,257,2,16])). % 19.78/19.88 cnf(453,plain, % 19.78/19.88 (E(f9(f10(a15,a17),a15),f10(a6,f9(a6,a6)))), % 19.78/19.88 inference(scs_inference,[],[234,263,33,257,421,2,16,18,3])). % 19.78/19.89 cnf(465,plain, % 19.78/19.89 (P2(f9(f9(a13,a13),f9(a13,a13)),f9(f9(a13,a13),f9(a13,a13)))), % 19.78/19.89 inference(scs_inference,[],[234,263,30,33,449,139,257,426,326,421,2,16,18,3,17,64,110,103,104,102,58])). % 19.78/19.89 cnf(469,plain, % 19.78/19.89 (E(f10(a6,f9(a6,a6)),f9(f10(a15,a17),a15))), % 19.78/19.89 inference(scs_inference,[],[453,2])). % 19.78/19.89 cnf(471,plain, % 19.78/19.89 (E(a17,f10(a6,f9(a6,a6)))), % 19.78/19.89 inference(scs_inference,[],[234,346,453,256,2,18,3])). % 19.78/19.89 cnf(472,plain, % 19.78/19.89 (P2(f9(f10(a15,a6),a15),f9(a16,a15))), % 19.78/19.89 inference(scs_inference,[],[234,346,453,256,284,2,18,3,17])). % 19.78/19.89 cnf(473,plain, % 19.78/19.89 (P2(f10(a5,f9(a5,a5)),f10(a5,f9(a5,a5)))), % 19.78/19.89 inference(scs_inference,[],[234,346,453,256,284,394,2,18,3,17,64])). % 19.78/19.89 cnf(475,plain, % 19.78/19.89 (E(f9(a6,a6),f9(f9(f10(a15,a17),a15),a6))), % 19.78/19.89 inference(scs_inference,[],[234,346,453,33,255,256,284,394,259,213,2,18,3,17,64,86])). % 19.78/19.89 cnf(480,plain, % 19.78/19.89 (E(f10(a6,f9(a6,a6)),a17)), % 19.78/19.89 inference(scs_inference,[],[471,2])). % 19.78/19.89 cnf(482,plain, % 19.78/19.89 (P1(f9(f9(f10(a15,a17),a15),a6))), % 19.78/19.89 inference(scs_inference,[],[270,471,271,475,259,2,18,16])). % 19.78/19.89 cnf(484,plain, % 19.78/19.89 (P2(f10(a6,f9(a6,a6)),f10(a6,f9(a6,a6)))), % 19.78/19.89 inference(scs_inference,[],[270,346,471,271,348,451,475,259,2,18,16,17,64])). % 19.78/19.89 cnf(486,plain, % 19.78/19.89 (E(f9(a16,a15),f9(f10(a15,a6),a15))), % 19.78/19.89 inference(scs_inference,[],[270,346,471,271,348,130,472,451,475,259,233,2,18,16,17,64,71])). % 19.78/19.89 cnf(488,plain, % 19.78/19.89 (E(f9(a6,a6),f9(a17,a6))), % 19.78/19.89 inference(scs_inference,[],[270,346,471,30,33,215,271,348,130,472,451,475,259,233,2,18,16,17,64,71,86])). % 19.78/19.89 cnf(493,plain, % 19.78/19.89 (~E(f7(a12,a17),f10(f9(a16,a15),f9(f9(a16,a15),f9(a16,a15))))+~P1(f7(a12,a15))), % 19.78/19.89 inference(scs_inference,[],[49,270,346,471,30,33,29,27,28,215,322,271,348,130,472,451,475,259,233,46,40,2,18,16,17,64,71,86,3,72,76])). % 19.78/19.89 cnf(499,plain, % 19.78/19.89 (P1(f9(a17,a6))), % 19.78/19.89 inference(scs_inference,[],[486,488,259,2,16])). % 19.78/19.89 cnf(500,plain, % 19.78/19.89 (P2(f10(a5,f9(a5,a5)),a5)), % 19.78/19.89 inference(scs_inference,[],[486,196,473,488,259,2,16,18])). % 19.78/19.89 cnf(501,plain, % 19.78/19.89 (P2(a5,f10(a5,f9(a5,a5)))), % 19.78/19.89 inference(scs_inference,[],[486,196,473,488,259,2,16,18,17])). % 19.78/19.89 cnf(502,plain, % 19.78/19.89 (P2(f10(a14,f9(a14,a14)),f10(a14,f9(a14,a14)))), % 19.78/19.89 inference(scs_inference,[],[486,196,473,422,488,259,2,16,18,17,64])). % 19.78/19.89 cnf(507,plain, % 19.78/19.89 (~E(f7(a12,a17),f10(f9(a12,a12),f9(f9(a12,a12),f9(a12,a12))))+~P1(f7(a12,a15))), % 19.78/19.89 inference(scs_inference,[],[49,486,25,27,196,152,350,473,422,488,259,46,2,16,18,17,64,3,72,76])). % 19.78/19.89 cnf(512,plain, % 19.78/19.89 (E(a16,f10(a16,f9(a16,a16)))), % 19.78/19.89 inference(scs_inference,[],[273,2])). % 19.78/19.89 cnf(513,plain, % 19.78/19.89 (E(f10(a6,f9(a6,a6)),f9(a16,a15))), % 19.78/19.89 inference(scs_inference,[],[480,123,273,2,3])). % 19.78/19.89 cnf(515,plain, % 19.78/19.89 (P1(f10(a16,f9(a16,a16)))), % 19.78/19.89 inference(scs_inference,[],[480,29,123,273,236,502,2,3,18,16])). % 19.78/19.89 cnf(517,plain, % 19.78/19.89 (P2(f9(a14,a14),f9(a14,a14))), % 19.78/19.89 inference(scs_inference,[],[480,29,123,273,236,502,238,2,3,18,16,17,64])). % 19.78/19.89 cnf(519,plain, % 19.78/19.89 (E(f9(a6,a6),f9(f9(a16,a15),a6))), % 19.78/19.89 inference(scs_inference,[],[480,33,29,123,273,236,130,284,502,238,259,2,3,18,16,17,64,86])). % 19.78/19.89 cnf(523,plain, % 19.78/19.89 (E(f10(f9(a14,a14),f9(f9(a14,a14),f9(a14,a14))),f9(a14,a14))), % 19.78/19.89 inference(scs_inference,[],[480,33,29,123,273,236,130,284,502,238,259,2,3,18,16,17,64,86,103,110])). % 19.78/19.89 cnf(525,plain, % 19.78/19.89 (P1(f9(f9(a14,a14),f9(a14,a14)))), % 19.78/19.89 inference(scs_inference,[],[480,33,29,123,273,236,130,284,502,238,259,2,3,18,16,17,64,86,103,110,104])). % 19.78/19.89 cnf(531,plain, % 19.78/19.89 (P2(f9(a16,a16),f9(a16,a16))), % 19.78/19.89 inference(scs_inference,[],[480,33,29,27,123,273,236,130,284,502,238,275,220,259,2,3,18,16,17,64,86,103,110,104,72,102,58])). % 19.78/19.89 cnf(535,plain, % 19.78/19.89 (E(f9(a16,a15),f10(a6,f9(a6,a6)))), % 19.78/19.89 inference(scs_inference,[],[513,2])). % 19.78/19.89 cnf(536,plain, % 19.78/19.89 (P2(f10(a6,f9(a6,a6)),f9(f10(a15,a17),a15))), % 19.78/19.89 inference(scs_inference,[],[469,513,484,2,18])). % 19.78/19.89 cnf(537,plain, % 19.78/19.89 (E(f10(a15,a17),f10(a16,f9(a16,a16)))), % 19.78/19.89 inference(scs_inference,[],[469,513,512,38,484,2,18,3])). % 19.78/19.89 cnf(538,plain, % 19.78/19.89 (P1(f9(f9(a16,a15),a6))), % 19.78/19.89 inference(scs_inference,[],[469,513,512,38,484,519,259,2,18,3,16])). % 19.78/19.89 cnf(539,plain, % 19.78/19.89 (P2(f9(f10(a15,a17),a15),f10(a6,f9(a6,a6)))), % 19.78/19.89 inference(scs_inference,[],[469,513,512,38,484,519,259,2,18,3,16,17])). % 19.78/19.89 cnf(540,plain, % 19.78/19.89 (E(f10(f9(a16,a16),f9(f9(a16,a16),f9(a16,a16))),f9(a16,a16))), % 19.78/19.89 inference(scs_inference,[],[469,513,512,38,531,484,519,275,259,2,18,3,16,17,110])). % 19.78/19.89 cnf(542,plain, % 19.78/19.89 (P1(f9(f9(a16,a16),f9(a16,a16)))), % 19.78/19.89 inference(scs_inference,[],[469,513,512,38,531,484,519,275,259,2,18,3,16,17,110,104])). % 19.78/19.89 cnf(548,plain, % 19.78/19.89 (P2(a15,f10(a16,f9(a16,a16)))), % 19.78/19.89 inference(scs_inference,[],[469,513,512,30,29,28,38,525,531,515,484,519,275,240,259,2,18,3,16,17,110,104,64,72,70])). % 19.78/19.89 cnf(550,plain, % 19.78/19.89 (E(a17,f9(f10(a16,f9(a16,a16)),a15))), % 19.78/19.89 inference(scs_inference,[],[469,513,512,30,29,28,38,525,531,515,484,519,275,240,259,2,18,3,16,17,110,104,64,72,70,86])). % 19.78/19.89 cnf(556,plain, % 19.78/19.89 (P2(f10(a16,f9(a16,a16)),f10(a16,f9(a16,a16)))), % 19.78/19.89 inference(scs_inference,[],[469,513,512,30,29,28,38,525,531,515,484,519,275,240,259,2,18,3,16,17,110,104,64,72,70,86,103,102,58])). % 19.78/19.89 cnf(560,plain, % 19.78/19.89 (E(f10(a16,f9(a16,a16)),f10(a15,a17))), % 19.78/19.89 inference(scs_inference,[],[537,2])). % 19.78/19.89 cnf(561,plain, % 19.78/19.89 (E(f10(a15,a6),f10(a16,f9(a16,a16)))), % 19.78/19.89 inference(scs_inference,[],[194,537,2,3])). % 19.78/19.89 cnf(562,plain, % 19.78/19.89 (P2(f10(a16,f9(a16,a16)),a16)), % 19.78/19.89 inference(scs_inference,[],[194,537,273,556,2,3,18])). % 19.78/19.89 cnf(564,plain, % 19.78/19.89 (P2(a16,f10(a16,f9(a16,a16)))), % 19.78/19.89 inference(scs_inference,[],[194,537,30,273,556,550,2,3,18,16,17])). % 19.78/19.89 cnf(565,plain, % 19.78/19.89 (P2(f9(f9(a16,a16),f9(a16,a16)),f9(f9(a16,a16),f9(a16,a16)))), % 19.78/19.89 inference(scs_inference,[],[194,537,30,273,542,556,550,2,3,18,16,17,64])). % 19.78/19.89 cnf(569,plain, % 19.78/19.89 (E(f9(a16,a16),f9(f10(a15,a17),a16))), % 19.78/19.89 inference(scs_inference,[],[194,537,30,29,273,542,556,550,172,275,2,3,18,16,17,64,70,86])). % 19.78/19.89 cnf(573,plain, % 19.78/19.89 (E(f10(f9(a17,a17),f9(f9(a17,a17),f9(a17,a17))),f9(a17,a17))+~P2(f9(a17,a17),f9(a17,a17))), % 19.78/19.89 inference(scs_inference,[],[194,537,30,29,24,273,542,556,289,550,172,275,2,3,18,16,17,64,70,86,103,110])). % 19.78/19.89 cnf(575,plain, % 19.78/19.89 (P2(f9(a17,a17),f9(a17,a17))), % 19.78/19.89 inference(scs_inference,[],[194,537,30,29,24,273,542,556,289,550,172,275,2,3,18,16,17,64,70,86,103,110,58])). % 19.78/19.89 cnf(578,plain, % 19.78/19.89 (E(f10(f9(a17,a17),f9(f9(a17,a17),f9(a17,a17))),f9(a17,a17))), % 19.78/19.89 inference(scs_inference,[],[575,573])). % 19.78/19.89 cnf(579,plain, % 19.78/19.89 (E(f10(a16,f9(a16,a16)),f10(a15,a6))), % 19.78/19.89 inference(scs_inference,[],[561,575,573,2])). % 19.78/19.89 cnf(581,plain, % 19.78/19.89 (E(f10(a6,f9(a6,a6)),f9(f10(a15,a6),a15))), % 19.78/19.89 inference(scs_inference,[],[269,480,561,226,536,575,573,2,18,3])). % 19.78/19.89 cnf(582,plain, % 19.78/19.89 (P1(f9(f10(a15,a17),a16))), % 19.78/19.89 inference(scs_inference,[],[269,480,561,226,275,536,575,569,573,2,18,3,16])). % 19.78/19.89 cnf(584,plain, % 19.78/19.89 (P2(f9(a15,a15),f9(a15,a15))), % 19.78/19.89 inference(scs_inference,[],[269,480,561,226,275,536,539,575,569,302,573,2,18,3,16,17,64])). % 19.78/19.89 cnf(586,plain, % 19.78/19.89 (P1(f9(f9(a15,a15),f9(a15,a15)))), % 19.78/19.89 inference(scs_inference,[],[269,480,561,226,275,536,539,575,569,302,573,2,18,3,16,17,64,104])). % 19.78/19.89 cnf(590,plain, % 19.78/19.89 (P2(a16,f10(a15,a6))), % 19.78/19.89 inference(scs_inference,[],[269,480,561,30,29,226,275,536,539,575,569,302,235,193,573,2,18,3,16,17,64,104,72,70])). % 19.78/19.89 cnf(592,plain, % 19.78/19.89 (E(a6,f9(f10(a16,f9(a16,a16)),a15))), % 19.78/19.89 inference(scs_inference,[],[269,480,561,30,33,29,28,226,275,536,539,575,569,302,548,235,193,515,573,2,18,3,16,17,64,104,72,70,86])). % 19.78/19.89 cnf(596,plain, % 19.78/19.89 (E(f10(f9(a15,a15),f9(f9(a15,a15),f9(a15,a15))),f9(a15,a15))), % 19.78/19.89 inference(scs_inference,[],[269,480,561,30,33,29,26,28,226,275,536,539,575,569,302,548,235,193,515,573,2,18,3,16,17,64,104,72,70,86,103,110])). % 19.78/19.89 cnf(598,plain, % 19.78/19.89 (P2(f9(f9(a16,a15),a6),f9(f9(a16,a15),a6))), % 19.78/19.89 inference(scs_inference,[],[269,480,561,30,33,29,26,28,226,275,536,539,575,569,302,538,548,235,193,515,573,2,18,3,16,17,64,104,72,70,86,103,110,58])). % 19.78/19.89 cnf(602,plain, % 19.78/19.89 (E(a5,a16)+E(a12,a1)), % 19.78/19.89 inference(scs_inference,[],[269,115,480,561,25,32,30,33,29,26,28,226,275,536,539,575,569,302,538,548,235,193,515,573,2,18,3,16,17,64,104,72,70,86,103,110,58,102,112,78])). % 19.78/19.89 cnf(609,plain, % 19.78/19.89 (P1(f9(f9(a17,a17),f9(a17,a17)))), % 19.78/19.89 inference(scs_inference,[],[270,581,536,539,586,575,289,2,18,17,64,104])). % 19.78/19.89 cnf(622,plain, % 19.78/19.89 (P2(f10(a16,f9(a16,a16)),f10(a15,a6))), % 19.78/19.89 inference(scs_inference,[],[192,322,562,2,18])). % 19.78/19.89 cnf(623,plain, % 19.78/19.89 (P2(f10(a15,a6),a16)), % 19.78/19.89 inference(scs_inference,[],[192,579,322,562,2,18,17])). % 19.78/19.89 cnf(624,plain, % 19.78/19.89 (P2(f9(f9(a17,a17),f9(a17,a17)),f9(f9(a17,a17),f9(a17,a17)))), % 19.78/19.89 inference(scs_inference,[],[192,579,322,562,609,2,18,17,64])). % 19.78/19.89 cnf(626,plain, % 19.78/19.89 (E(f9(a16,a16),f9(f10(a15,a6),a16))), % 19.78/19.89 inference(scs_inference,[],[192,579,29,322,275,562,609,590,193,2,18,17,64,86])). % 19.78/19.89 cnf(628,plain, % 19.78/19.89 (E(x6281,f9(a5,a5))+~E(x6281,f10(f9(a5,a5),f9(f9(a5,a5),f9(a5,a5))))), % 19.78/19.89 inference(scs_inference,[],[192,579,29,322,397,275,562,609,590,193,2,18,17,64,86,3])). % 19.78/19.89 cnf(640,plain, % 19.78/19.89 (E(f9(a12,a12),f10(f9(a12,a12),f9(f9(a12,a12),f9(a12,a12))))), % 19.78/19.89 inference(scs_inference,[],[350,2])). % 19.78/19.89 cnf(642,plain, % 19.78/19.89 (P2(f10(a15,a6),f10(a16,f9(a16,a16)))), % 19.78/19.89 inference(scs_inference,[],[194,192,350,564,622,2,18,17])). % 19.78/19.89 cnf(658,plain, % 19.78/19.89 (E(f9(a2,a2),f10(f9(a2,a2),f9(f9(a2,a2),f9(a2,a2))))), % 19.78/19.89 inference(scs_inference,[],[371,2])). % 19.78/19.89 cnf(661,plain, % 19.78/19.89 (E(f10(f10(a15,a6),f9(f10(a15,a6),f10(a15,a6))),f10(a15,a6))), % 19.78/19.89 inference(scs_inference,[],[560,192,371,562,623,193,2,18,17,110])). % 19.78/19.89 cnf(663,plain, % 19.78/19.89 (P1(f9(f10(a15,a6),f10(a15,a6)))), % 19.78/19.89 inference(scs_inference,[],[560,192,371,562,623,193,2,18,17,110,104])). % 19.78/19.89 cnf(665,plain, % 19.78/19.89 (P2(f9(a11,a11),f9(a11,a11))), % 19.78/19.89 inference(scs_inference,[],[560,192,371,562,623,137,193,2,18,17,110,104,64])). % 19.78/19.89 cnf(682,plain, % 19.78/19.89 (E(f9(a5,a5),f10(f9(a5,a5),f9(f9(a5,a5),f9(a5,a5))))), % 19.78/19.89 inference(scs_inference,[],[397,2])). % 19.78/19.89 cnf(683,plain, % 19.78/19.89 (P2(f10(a15,a6),f10(a15,a17))), % 19.78/19.89 inference(scs_inference,[],[560,397,642,2,18])). % 19.78/19.89 cnf(684,plain, % 19.78/19.89 (P2(f10(a15,a17),f10(a15,a6))), % 19.78/19.89 inference(scs_inference,[],[560,397,622,642,2,18,17])). % 19.78/19.89 cnf(685,plain, % 19.78/19.89 (E(f10(f9(a11,a11),f9(f9(a11,a11),f9(a11,a11))),f9(a11,a11))), % 19.78/19.89 inference(scs_inference,[],[560,397,622,642,665,137,2,18,17,110])). % 19.78/19.89 cnf(698,plain, % 19.78/19.89 (E(f9(a13,a13),f10(f9(a13,a13),f9(f9(a13,a13),f9(a13,a13))))), % 19.78/19.89 inference(scs_inference,[],[424,2])). % 19.78/19.89 cnf(701,plain, % 19.78/19.89 (E(f10(f10(a15,a17),f9(f10(a15,a17),f10(a15,a17))),f10(a15,a17))), % 19.78/19.89 inference(scs_inference,[],[194,424,642,684,172,2,18,17,110])). % 19.78/19.89 cnf(703,plain, % 19.78/19.89 (P1(f9(f10(a15,a17),f10(a15,a17)))), % 19.78/19.89 inference(scs_inference,[],[194,424,642,684,172,2,18,17,110,104])). % 19.78/19.89 cnf(722,plain, % 19.78/19.89 (E(f10(a6,f9(a6,a6)),f10(a17,f9(a17,a17)))), % 19.78/19.89 inference(scs_inference,[],[480,640,287,277,2,18,3])). % 19.78/19.89 cnf(724,plain, % 19.78/19.89 (P1(f10(a17,f9(a17,a17)))), % 19.78/19.89 inference(scs_inference,[],[480,640,30,287,277,2,18,3,17,16])). % 19.78/19.89 cnf(727,plain, % 19.78/19.89 (P2(a6,f10(a17,f9(a17,a17)))), % 19.78/19.89 inference(scs_inference,[],[480,640,30,33,287,703,277,259,2,18,3,17,16,64,70])). % 19.78/19.89 cnf(729,plain, % 19.78/19.89 (E(f9(a6,a6),f9(f10(a17,f9(a17,a17)),a6))), % 19.78/19.89 inference(scs_inference,[],[480,640,30,33,287,703,277,259,2,18,3,17,16,64,70,86])). % 19.78/19.89 cnf(733,plain, % 19.78/19.89 (E(f10(f9(a17,a6),f9(f9(a17,a6),f9(a17,a6))),f9(a17,a6))+~P2(f9(a17,a6),f9(a17,a6))), % 19.78/19.89 inference(scs_inference,[],[480,640,30,33,28,287,703,499,277,259,2,18,3,17,16,64,70,86,103,110])). % 19.78/19.89 cnf(735,plain, % 19.78/19.89 (P1(f9(f9(a17,a6),f9(a17,a6)))+~P2(f9(a17,a6),f9(a17,a6))), % 19.78/19.89 inference(scs_inference,[],[480,640,30,33,28,287,703,499,277,259,2,18,3,17,16,64,70,86,103,110,104])). % 19.78/19.89 cnf(737,plain, % 19.78/19.89 (P2(f9(a17,a6),f9(a17,a6))), % 19.78/19.89 inference(scs_inference,[],[480,640,30,33,28,287,703,499,277,259,2,18,3,17,16,64,70,86,103,110,104,58])). % 19.78/19.89 cnf(743,plain, % 19.78/19.89 (E(f10(f9(a17,a6),f9(f9(a17,a6),f9(a17,a6))),f9(a17,a6))), % 19.78/19.89 inference(scs_inference,[],[737,733])). % 19.78/19.89 cnf(744,plain, % 19.78/19.89 (P1(f9(f9(a17,a6),f9(a17,a6)))), % 19.78/19.89 inference(scs_inference,[],[737,735])). % 19.78/19.89 cnf(745,plain, % 19.78/19.89 (E(f10(a17,f9(a17,a17)),f10(a6,f9(a6,a6)))), % 19.78/19.89 inference(scs_inference,[],[722,2])). % 19.78/19.89 cnf(747,plain, % 19.78/19.89 (E(f9(a16,a15),f10(a17,f9(a17,a17)))), % 19.78/19.89 inference(scs_inference,[],[535,682,722,304,2,18,3])). % 19.78/19.89 cnf(750,plain, % 19.78/19.89 (P2(f10(a17,f9(a17,a17)),f10(a17,f9(a17,a17)))), % 19.78/19.89 inference(scs_inference,[],[346,535,682,722,724,729,727,304,259,2,18,3,17,16,64])). % 19.78/19.89 cnf(754,plain, % 19.78/19.89 (E(f9(a17,a17),f9(f10(a6,f9(a6,a6)),a17))), % 19.78/19.89 inference(scs_inference,[],[346,535,682,722,30,289,724,729,727,451,304,259,2,18,3,17,16,64,70,86])). % 19.78/19.89 cnf(762,plain, % 19.78/19.89 (P2(f10(a13,f9(a13,a13)),f10(a13,f9(a13,a13)))), % 19.78/19.89 inference(scs_inference,[],[346,535,682,722,30,23,289,724,729,727,366,451,119,304,259,2,18,3,17,16,64,70,86,103,110,104,58])). % 19.78/19.89 cnf(768,plain, % 19.78/19.89 (E(f10(a17,f9(a17,a17)),f9(a16,a15))), % 19.78/19.89 inference(scs_inference,[],[747,2])). % 19.78/19.89 cnf(770,plain, % 19.78/19.89 (E(f9(f10(a15,a17),a15),f10(a17,f9(a17,a17)))), % 19.78/19.89 inference(scs_inference,[],[269,747,216,762,2,18,3])). % 19.78/19.89 cnf(772,plain, % 19.78/19.89 (P1(f9(f10(a6,f9(a6,a6)),a17))), % 19.78/19.89 inference(scs_inference,[],[269,747,216,289,762,754,2,18,3,17,16])). % 19.78/19.89 cnf(777,plain, % 19.78/19.89 (E(f9(a17,a17),f9(f9(a16,a15),a17))), % 19.78/19.89 inference(scs_inference,[],[269,747,30,33,130,216,215,369,289,762,743,744,754,2,18,3,17,16,64,72,86])). % 19.78/19.89 cnf(785,plain, % 19.78/19.89 (P2(f10(a2,f9(a2,a2)),f10(a2,f9(a2,a2)))), % 19.78/19.89 inference(scs_inference,[],[269,747,30,33,449,130,216,215,369,289,762,743,744,754,347,259,2,18,3,17,16,64,72,86,103,110,104,58])). % 19.78/19.89 cnf(793,plain, % 19.78/19.89 (E(a6,f10(a17,f9(a17,a17)))), % 19.78/19.89 inference(scs_inference,[],[450,722,770,174,785,2,18,3])). % 19.78/19.89 cnf(795,plain, % 19.78/19.89 (P1(f9(f9(a16,a15),a17))), % 19.78/19.89 inference(scs_inference,[],[450,722,770,174,289,785,777,2,18,3,17,16])). % 19.78/19.89 cnf(796,plain, % 19.78/19.89 (P2(f9(a1,a1),f9(a1,a1))), % 19.78/19.89 inference(scs_inference,[],[450,722,770,174,289,119,785,777,2,18,3,17,16,64])). % 19.78/19.89 cnf(798,plain, % 19.78/19.89 (E(f9(a17,a17),f9(f9(f10(a15,a17),a15),a17))), % 19.78/19.89 inference(scs_inference,[],[450,722,770,30,174,286,289,119,785,777,213,2,18,3,17,16,64,86])). % 19.78/19.89 cnf(802,plain, % 19.78/19.89 (P1(f9(f9(a1,a1),f9(a1,a1)))), % 19.78/19.89 inference(scs_inference,[],[450,722,770,30,157,174,286,289,119,785,777,213,2,18,3,17,16,64,86,103,104])). % 19.78/19.89 cnf(804,plain, % 19.78/19.89 (E(f10(f9(a1,a1),f9(f9(a1,a1),f9(a1,a1))),f9(a1,a1))), % 19.78/19.89 inference(scs_inference,[],[450,722,770,30,157,174,286,289,119,785,777,213,2,18,3,17,16,64,86,103,104,110])). % 19.78/19.89 cnf(815,plain, % 19.78/19.89 (E(f10(a17,f9(a17,a17)),a6)), % 19.78/19.89 inference(scs_inference,[],[793,2])). % 19.78/19.89 cnf(816,plain, % 19.78/19.89 (P2(f9(a1,a1),a1)), % 19.78/19.89 inference(scs_inference,[],[793,126,796,2,18])). % 19.78/19.89 cnf(817,plain, % 19.78/19.89 (E(f10(f9(a1,a1),f9(f9(a1,a1),f9(a1,a1))),a1)), % 19.78/19.89 inference(scs_inference,[],[793,126,796,804,2,18,3])). % 19.78/19.89 cnf(818,plain, % 19.78/19.89 (P2(a1,f9(a1,a1))), % 19.78/19.89 inference(scs_inference,[],[793,126,796,804,2,18,3,17])). % 19.78/19.89 cnf(820,plain, % 19.78/19.89 (E(f9(f9(a1,a1),f9(a1,a1)),a1)), % 19.78/19.89 inference(scs_inference,[],[793,289,126,119,796,804,802,798,2,18,3,17,16,59])). % 19.78/19.89 cnf(822,plain, % 19.78/19.89 (P2(f9(f9(a1,a1),f9(a1,a1)),f9(f9(a1,a1),f9(a1,a1)))), % 19.78/19.89 inference(scs_inference,[],[793,289,126,119,796,804,802,798,2,18,3,17,16,59,64])). % 19.78/19.89 cnf(824,plain, % 19.78/19.89 (E(a1,f9(a1,a1))), % 19.78/19.89 inference(scs_inference,[],[793,23,289,126,119,796,804,802,798,2,18,3,17,16,59,64,71])). % 19.78/19.89 cnf(826,plain, % 19.78/19.89 (E(f9(a17,a17),f9(a6,a17))), % 19.78/19.89 inference(scs_inference,[],[793,30,33,23,214,289,126,119,796,804,802,798,2,18,3,17,16,59,64,71,86])). % 19.78/19.89 cnf(837,plain, % 19.78/19.89 (P2(f9(f9(a1,a1),f9(a1,a1)),a1)), % 19.78/19.89 inference(scs_inference,[],[817,822,820,2,18])). % 19.78/19.89 cnf(838,plain, % 19.78/19.89 (E(f10(f9(a17,a17),f9(f9(a17,a17),f9(a17,a17))),f9(a6,a17))), % 19.78/19.89 inference(scs_inference,[],[817,578,822,826,820,2,18,3])). % 19.78/19.89 cnf(839,plain, % 19.78/19.89 (P2(a1,f9(f9(a1,a1),f9(a1,a1)))), % 19.78/19.89 inference(scs_inference,[],[817,578,822,826,820,2,18,3,17])). % 19.78/19.89 cnf(840,plain, % 19.78/19.89 (P1(f9(a6,a17))), % 19.78/19.89 inference(scs_inference,[],[817,289,578,822,826,820,2,18,3,17,16])). % 19.78/19.89 cnf(841,plain, % 19.78/19.89 (P2(f9(a6,a6),f9(a6,a6))), % 19.78/19.89 inference(scs_inference,[],[817,289,578,259,822,826,820,2,18,3,17,16,64])). % 19.78/19.89 cnf(845,plain, % 19.78/19.89 (P2(f9(a17,a17),f9(a6,a17))), % 19.78/19.89 inference(scs_inference,[],[817,23,289,578,609,259,802,822,826,820,2,18,3,17,16,64,71,70])). % 19.78/19.89 cnf(847,plain, % 19.78/19.89 (E(f9(f9(a1,a1),f9(a1,a1)),f9(a1,f9(a1,a1)))), % 19.78/19.89 inference(scs_inference,[],[817,23,289,578,119,609,259,802,822,816,826,820,2,18,3,17,16,64,71,70,86])). % 19.78/19.89 cnf(849,plain, % 19.78/19.89 (P2(f10(f9(a1,a1),f9(f9(a1,a1),f9(a1,a1))),a1)), % 19.78/19.89 inference(scs_inference,[],[817,23,289,578,119,609,259,802,822,816,826,820,2,18,3,17,16,64,71,70,86,136])). % 19.78/19.89 cnf(852,plain, % 19.78/19.89 (P1(f9(f9(a6,a6),f9(a6,a6)))), % 19.78/19.89 inference(scs_inference,[],[817,23,218,289,578,119,609,259,802,822,816,826,820,2,18,3,17,16,64,71,70,86,136,103,104])). % 19.78/19.89 cnf(854,plain, % 19.78/19.89 (E(f10(f9(a6,a6),f9(f9(a6,a6),f9(a6,a6))),f9(a6,a6))), % 19.78/19.89 inference(scs_inference,[],[817,23,218,289,578,119,609,259,802,822,816,826,820,2,18,3,17,16,64,71,70,86,136,103,104,110])). % 19.78/19.89 cnf(856,plain, % 19.78/19.89 (P1(f10(f9(a6,a6),f9(f9(a6,a6),f9(a6,a6))))), % 19.78/19.89 inference(scs_inference,[],[817,33,23,218,289,578,119,609,259,802,822,816,826,820,200,2,18,3,17,16,64,71,70,86,136,103,104,110,72])). % 19.78/19.89 cnf(858,plain, % 19.78/19.89 (P2(f9(f10(a15,a17),a16),f9(f10(a15,a17),a16))), % 19.78/19.89 inference(scs_inference,[],[817,33,23,218,289,578,119,609,259,802,822,816,826,820,582,200,2,18,3,17,16,64,71,70,86,136,103,104,110,72,58])). % 19.78/19.89 cnf(865,plain, % 19.78/19.89 (P2(f9(a6,a6),f9(f9(f10(a15,a17),a15),a6))), % 19.78/19.89 inference(scs_inference,[],[838,475,841,2,18])). % 19.78/19.89 cnf(866,plain, % 19.78/19.89 (E(f9(a6,a17),f9(a17,a17))), % 19.78/19.89 inference(scs_inference,[],[838,578,475,841,2,18,3])). % 19.78/19.89 cnf(867,plain, % 19.78/19.89 (P2(f9(f9(f10(a15,a17),a15),a6),f9(a6,a6))), % 19.78/19.89 inference(scs_inference,[],[838,578,475,841,2,18,3,17])). % 19.78/19.89 cnf(868,plain, % 19.78/19.89 (P1(f9(a1,f9(a1,a1)))), % 19.78/19.89 inference(scs_inference,[],[838,578,475,802,841,847,2,18,3,17,16])). % 19.78/19.89 cnf(869,plain, % 19.78/19.89 (P2(f9(f9(a6,a6),f9(a6,a6)),f9(f9(a6,a6),f9(a6,a6)))), % 19.78/19.89 inference(scs_inference,[],[838,578,475,802,841,852,847,2,18,3,17,16,64])). % 19.78/19.89 cnf(871,plain, % 19.78/19.89 (E(f9(f9(f10(a15,a17),a15),a6),f9(a6,a6))), % 19.78/19.89 inference(scs_inference,[],[838,578,475,259,802,841,852,847,482,2,18,3,17,16,64,71])). % 19.78/19.89 cnf(873,plain, % 19.78/19.89 (E(f9(f9(a17,a17),f9(a17,a17)),f9(f9(a6,a17),f9(a17,a17)))), % 19.78/19.89 inference(scs_inference,[],[838,289,578,475,609,259,802,841,852,847,845,840,482,2,18,3,17,16,64,71,86])). % 19.78/19.89 cnf(877,plain, % 19.78/19.89 (P1(f9(f9(a6,a17),f9(a6,a17)))+~P2(f9(a6,a17),f9(a6,a17))), % 19.78/19.89 inference(scs_inference,[],[838,176,289,578,475,609,259,802,841,852,847,845,840,482,2,18,3,17,16,64,71,86,103,104])). % 19.78/19.89 cnf(879,plain, % 19.78/19.89 (P2(f9(a6,a17),f9(a6,a17))), % 19.78/19.89 inference(scs_inference,[],[838,176,289,578,475,609,259,802,841,852,847,845,840,482,2,18,3,17,16,64,71,86,103,104,58])). % 19.78/19.89 cnf(881,plain, % 19.78/19.89 (E(f10(f9(a6,a17),f9(f9(a6,a17),f9(a6,a17))),f9(a6,a17))), % 19.78/19.89 inference(scs_inference,[],[838,176,289,578,475,609,259,802,841,852,847,845,840,482,2,18,3,17,16,64,71,86,103,104,58,110])). % 19.78/19.89 cnf(887,plain, % 19.78/19.89 (E(f9(f9(f10(a15,a17),a15),a6),f9(a17,a6))), % 19.78/19.89 inference(scs_inference,[],[871,540,488,624,873,879,877,2,18,3])). % 19.78/19.89 cnf(889,plain, % 19.78/19.89 (P1(f9(f9(a6,a17),f9(a17,a17)))), % 19.78/19.89 inference(scs_inference,[],[871,540,488,609,624,873,879,877,2,18,3,17,16])). % 19.78/19.89 cnf(904,plain, % 19.78/19.89 (E(f9(a17,a6),f9(f9(f10(a15,a17),a15),a6))), % 19.78/19.89 inference(scs_inference,[],[887,2])). % 19.78/19.89 cnf(905,plain, % 19.78/19.89 (P2(f10(a17,f9(a17,a17)),f9(a16,a15))), % 19.78/19.89 inference(scs_inference,[],[768,887,750,2,18])). % 19.78/19.89 cnf(906,plain, % 19.78/19.89 (E(f10(a17,f9(a17,a17)),f9(f10(a15,a6),a15))), % 19.78/19.89 inference(scs_inference,[],[581,768,745,887,750,2,18,3])). % 19.78/19.89 cnf(910,plain, % 19.78/19.89 (E(f9(a17,a17),f9(f9(f10(a15,a6),a15),a17))), % 19.78/19.89 inference(scs_inference,[],[581,768,745,887,30,289,423,233,750,889,2,18,3,17,64,86])). % 19.78/19.89 cnf(912,plain, % 19.78/19.89 (~P1(f10(f7(a12,a15),f7(a12,a17)))+P1(f10(f7(a12,a15),a14))), % 19.78/19.89 inference(scs_inference,[],[581,768,745,887,30,289,423,46,233,750,889,2,18,3,17,64,86,16])). % 19.78/19.89 cnf(916,plain, % 19.78/19.89 (P2(f9(f9(a1,a1),f9(a1,a1)),f10(a1,f9(a1,a1)))), % 19.78/19.89 inference(scs_inference,[],[147,906,837,2,18])). % 19.78/19.89 cnf(918,plain, % 19.78/19.89 (P2(f9(a1,f9(a1,a1)),a1)), % 19.78/19.89 inference(scs_inference,[],[147,871,906,904,847,837,2,18,3,17])). % 19.78/19.89 cnf(927,plain, % 19.78/19.89 (E(f9(a14,a14),f10(f9(a14,a14),f9(f9(a14,a14),f9(a14,a14))))), % 19.78/19.89 inference(scs_inference,[],[523,2])). % 19.78/19.89 cnf(928,plain, % 19.78/19.89 (P2(f9(a6,a6),f9(a17,a6))), % 19.78/19.89 inference(scs_inference,[],[887,523,865,2,18])). % 19.78/19.89 cnf(929,plain, % 19.78/19.89 (P2(f9(a17,a6),f9(a6,a6))), % 19.78/19.89 inference(scs_inference,[],[887,523,867,865,2,18,17])). % 19.78/19.89 cnf(930,plain, % 19.78/19.89 (E(f9(a6,a17),f9(f10(a6,f9(a6,a6)),a17))), % 19.78/19.89 inference(scs_inference,[],[866,887,523,754,867,865,2,18,17,3])). % 19.78/19.89 cnf(935,plain, % 19.78/19.89 (~P2(a1,f9(a1,f9(a1,a1)))+E(a1,f9(a1,f9(a1,a1)))), % 19.78/19.89 inference(scs_inference,[],[866,887,23,130,275,523,754,868,867,865,918,2,18,17,3,103,102,71])). % 19.78/19.89 cnf(939,plain, % 19.78/19.89 (E(f9(f10(a6,f9(a6,a6)),a17),f9(a6,a17))), % 19.78/19.89 inference(scs_inference,[],[930,2])). % 19.78/19.89 cnf(941,plain, % 19.78/19.89 (E(f9(a6,a17),f9(f9(a16,a15),a17))), % 19.78/19.89 inference(scs_inference,[],[147,866,930,777,816,2,18,3])). % 19.78/19.89 cnf(943,plain, % 19.78/19.89 (E(f10(a1,f9(a1,a1)),f9(a1,a1))), % 19.78/19.89 inference(scs_inference,[],[147,866,930,119,777,148,818,816,2,18,3,17,71])). % 19.78/19.89 cnf(945,plain, % 19.78/19.89 (E(f9(a1,a1),f9(f9(a1,a1),a1))), % 19.78/19.89 inference(scs_inference,[],[147,866,930,23,119,777,148,818,816,2,18,3,17,71,86])). % 19.78/19.89 cnf(947,plain, % 19.78/19.89 (P1(f9(f9(a1,a1),a1))), % 19.78/19.89 inference(scs_inference,[],[147,866,930,23,119,777,148,818,816,2,18,3,17,71,86,16])). % 19.78/19.89 cnf(950,plain, % 19.78/19.89 (P2(f9(f9(a1,a1),a1),f9(f9(a1,a1),a1))), % 19.78/19.89 inference(scs_inference,[],[147,866,930,23,302,119,777,148,818,816,2,18,3,17,71,86,16,103,64])). % 19.78/19.89 cnf(955,plain, % 19.78/19.89 (E(a5,a16)), % 19.78/19.89 inference(scs_inference,[],[48,602,2])). % 19.78/19.89 cnf(957,plain, % 19.78/19.89 (P2(a1,f9(a1,f9(a1,a1)))), % 19.78/19.89 inference(scs_inference,[],[943,847,839,2,18])). % 19.78/19.89 cnf(958,plain, % 19.78/19.89 (P2(f10(a1,f9(a1,a1)),f9(f9(a1,a1),f9(a1,a1)))), % 19.78/19.89 inference(scs_inference,[],[147,943,847,839,2,18,17])). % 19.78/19.89 cnf(959,plain, % 19.78/19.89 (E(a5,f10(a15,a6))), % 19.78/19.89 inference(scs_inference,[],[147,192,943,955,847,839,2,18,17,3])). % 19.78/19.89 cnf(962,plain, % 19.78/19.89 (E(f9(a1,a1),f9(f9(f9(a1,a1),f9(a1,a1)),a1))), % 19.78/19.89 inference(scs_inference,[],[147,192,943,955,23,119,802,148,847,839,916,2,18,17,3,71,86])). % 19.78/19.89 cnf(964,plain, % 19.78/19.89 (E(a1,f9(a1,f9(a1,a1)))), % 19.78/19.89 inference(scs_inference,[],[147,192,943,955,23,119,802,148,847,839,916,2,18,17,3,71,86,935])). % 19.78/19.89 cnf(972,plain, % 19.78/19.89 (P2(f10(a17,f9(a17,a17)),f9(f10(a15,a17),a15))), % 19.78/19.89 inference(scs_inference,[],[254,941,905,2,18])). % 19.78/19.89 cnf(973,plain, % 19.78/19.89 (E(a5,f10(a16,f9(a16,a16)))), % 19.78/19.89 inference(scs_inference,[],[254,512,941,955,905,2,18,3])). % 19.78/19.89 cnf(983,plain, % 19.78/19.89 (P2(f9(f9(a1,a1),f9(a1,a1)),f9(a1,a1))), % 19.78/19.89 inference(scs_inference,[],[943,964,916,2,18])). % 19.78/19.89 cnf(984,plain, % 19.78/19.89 (P2(f9(f10(a6,f9(a6,a6)),a17),f9(a6,a17))), % 19.78/19.89 inference(scs_inference,[],[943,964,754,845,916,2,18,17])). % 19.78/19.89 cnf(985,plain, % 19.78/19.89 (E(a5,f10(a15,a17))), % 19.78/19.89 inference(scs_inference,[],[170,943,964,955,754,845,916,2,18,17,3])). % 19.78/19.89 cnf(994,plain, % 19.78/19.89 (E(f10(a15,a6),a5)), % 19.78/19.89 inference(scs_inference,[],[959,2])). % 19.78/19.89 cnf(996,plain, % 19.78/19.89 (E(f10(a5,f9(a5,a5)),f10(a15,a6))), % 19.78/19.89 inference(scs_inference,[],[270,959,196,972,2,18,3])). % 19.78/19.89 cnf(997,plain, % 19.78/19.89 (P2(f9(f9(a16,a15),a17),f9(a6,a17))), % 19.78/19.89 inference(scs_inference,[],[270,959,196,777,845,972,2,18,3,17])). % 19.78/19.89 cnf(998,plain, % 19.78/19.89 (P2(a15,a5)), % 19.78/19.89 inference(scs_inference,[],[270,959,32,33,28,196,777,845,972,2,18,3,17,70])). % 19.78/19.89 cnf(1000,plain, % 19.78/19.89 (E(a6,f9(a5,a15))), % 19.78/19.89 inference(scs_inference,[],[270,959,32,33,28,196,777,845,972,2,18,3,17,70,86])). % 19.78/19.89 cnf(1002,plain, % 19.78/19.89 (P1(f9(a5,a15))), % 19.78/19.89 inference(scs_inference,[],[270,959,32,33,28,196,777,845,972,2,18,3,17,70,86,16])). % 19.78/19.89 cnf(1005,plain, % 19.78/19.89 (P2(f9(a5,a15),f9(a5,a15))), % 19.78/19.89 inference(scs_inference,[],[270,959,32,33,28,196,777,845,972,2,18,3,17,70,86,16,104,64])). % 19.78/19.89 cnf(1009,plain, % 19.78/19.89 (E(f10(f9(a5,a15),f9(f9(a5,a15),f9(a5,a15))),f9(a5,a15))), % 19.78/19.89 inference(scs_inference,[],[270,959,32,33,28,193,196,777,845,972,2,18,3,17,70,86,16,104,64,103,110])). % 19.78/19.89 cnf(1012,plain, % 19.78/19.89 (E(a16,a5)), % 19.78/19.89 inference(scs_inference,[],[955,2])). % 19.78/19.89 cnf(1013,plain, % 19.78/19.89 (P2(a5,f10(a15,a6))), % 19.78/19.89 inference(scs_inference,[],[955,996,501,2,18])). % 19.78/19.89 cnf(1014,plain, % 19.78/19.89 (P2(f10(a15,a6),a5)), % 19.78/19.89 inference(scs_inference,[],[955,996,500,501,2,18,17])). % 19.78/19.89 cnf(1015,plain, % 19.78/19.89 (E(f10(a15,a6),f10(a5,f9(a5,a5)))), % 19.78/19.89 inference(scs_inference,[],[393,955,996,994,500,501,2,18,17,3])). % 19.78/19.89 cnf(1022,plain, % 19.78/19.89 (P2(a15,f10(a5,f9(a5,a5)))), % 19.78/19.89 inference(scs_inference,[],[393,955,996,994,32,33,28,500,501,394,1005,1009,1002,998,2,18,17,3,104,64,72,70])). % 19.78/19.89 cnf(1024,plain, % 19.78/19.89 (E(f9(a5,a5),f9(f10(a15,a6),a5))), % 19.78/19.89 inference(scs_inference,[],[393,955,996,994,32,33,28,198,193,500,501,394,1005,1009,1002,998,2,18,17,3,104,64,72,70,86])). % 19.78/19.89 cnf(1029,plain, % 19.78/19.89 (P2(f9(f10(a15,a6),a5),f9(f10(a15,a6),a5))), % 19.78/19.89 inference(scs_inference,[],[393,955,996,994,32,33,28,198,193,499,500,501,394,1005,1009,1002,998,2,18,17,3,104,64,72,70,86,16,103,58])). % 19.78/19.89 cnf(1036,plain, % 19.78/19.89 (E(f10(a16,f9(a16,a16)),a5)), % 19.78/19.89 inference(scs_inference,[],[973,2])). % 19.78/19.89 cnf(1038,plain, % 19.78/19.89 (E(a16,f10(a5,f9(a5,a5)))), % 19.78/19.89 inference(scs_inference,[],[393,973,1012,475,929,2,18,3])). % 19.78/19.89 cnf(1040,plain, % 19.78/19.89 (P2(a16,a5)), % 19.78/19.89 inference(scs_inference,[],[393,973,1012,32,29,275,475,928,929,2,18,3,17,70])). % 19.78/19.89 cnf(1053,plain, % 19.78/19.89 (E(f10(a15,a17),a5)), % 19.78/19.89 inference(scs_inference,[],[985,2])). % 19.78/19.89 cnf(1054,plain, % 19.78/19.89 (P2(f9(a1,f9(a1,a1)),f10(a1,f9(a1,a1)))), % 19.78/19.89 inference(scs_inference,[],[147,985,918,2,18])). % 19.78/19.89 cnf(1055,plain, % 19.78/19.89 (P2(f10(a1,f9(a1,a1)),f9(a1,f9(a1,a1)))), % 19.78/19.89 inference(scs_inference,[],[147,985,957,918,2,18,17])). % 19.78/19.89 cnf(1056,plain, % 19.78/19.89 (E(f10(a16,f9(a16,a16)),f10(a5,f9(a5,a5)))), % 19.78/19.89 inference(scs_inference,[],[147,393,985,1036,957,918,2,18,17,3])). % 19.78/19.89 cnf(1057,plain, % 19.78/19.89 (E(f10(a1,f9(a1,a1)),f9(a1,f9(a1,a1)))), % 19.78/19.89 inference(scs_inference,[],[147,393,985,1036,148,868,957,918,2,18,17,3,71])). % 19.78/19.89 cnf(1061,plain, % 19.78/19.89 (E(f9(a16,a16),f9(a5,a16))), % 19.78/19.89 inference(scs_inference,[],[147,393,985,1036,32,29,275,394,148,868,957,918,1040,2,18,17,3,71,70,86])). % 19.78/19.89 cnf(1063,plain, % 19.78/19.89 (P1(f9(a5,a16))), % 19.78/19.89 inference(scs_inference,[],[147,393,985,1036,32,29,275,394,148,868,957,918,1040,2,18,17,3,71,70,86,16])). % 19.78/19.89 cnf(1066,plain, % 19.78/19.89 (P2(f9(a5,a16),f9(a5,a16))), % 19.78/19.89 inference(scs_inference,[],[147,393,985,1036,32,29,275,394,148,868,957,918,1040,2,18,17,3,71,70,86,16,104,64])). % 19.78/19.89 cnf(1068,plain, % 19.78/19.89 (E(f10(f9(a5,a16),f9(f9(a5,a16),f9(a5,a16))),f9(a5,a16))), % 19.78/19.89 inference(scs_inference,[],[147,393,985,1036,32,29,275,394,148,868,957,918,1040,2,18,17,3,71,70,86,16,104,64,110])). % 19.78/19.89 cnf(1073,plain, % 19.78/19.89 (E(f10(a5,f9(a5,a5)),f10(a16,f9(a16,a16)))), % 19.78/19.89 inference(scs_inference,[],[1056,2])). % 19.78/19.89 cnf(1074,plain, % 19.78/19.89 (P2(f9(f9(a16,a15),a17),f9(a17,a17))), % 19.78/19.89 inference(scs_inference,[],[866,1056,997,2,18])). % 19.78/19.89 cnf(1075,plain, % 19.78/19.89 (E(f10(a15,a17),f10(a5,f9(a5,a5)))), % 19.78/19.89 inference(scs_inference,[],[866,393,1056,1053,997,2,18,3])). % 19.78/19.89 cnf(1083,plain, % 19.78/19.89 (E(f9(a1,a1),f9(f9(a1,a1),f9(a1,a1)))), % 19.78/19.89 inference(scs_inference,[],[866,943,393,1056,1053,32,29,119,802,958,983,997,1066,1068,1063,1040,2,18,3,17,104,64,72,71])). % 19.78/19.89 cnf(1085,plain, % 19.78/19.89 (P2(a5,f10(a16,f9(a16,a16)))), % 19.78/19.89 inference(scs_inference,[],[866,943,393,1056,1053,32,29,198,119,802,515,958,983,997,1066,1068,1063,1040,2,18,3,17,104,64,72,71,70])). % 19.78/19.89 cnf(1097,plain, % 19.78/19.89 (P2(f9(f10(a6,f9(a6,a6)),a17),f9(a17,a17))), % 19.78/19.89 inference(scs_inference,[],[866,1083,984,2,18])). % 19.78/19.89 cnf(1098,plain, % 19.78/19.89 (P2(f10(a16,f9(a16,a16)),a5)), % 19.78/19.89 inference(scs_inference,[],[866,1083,1073,500,984,2,18,17])). % 19.78/19.89 cnf(1099,plain, % 19.78/19.89 (E(f9(a6,a17),f9(f9(f10(a15,a17),a15),a17))), % 19.78/19.89 inference(scs_inference,[],[866,1083,1073,500,798,984,2,18,17,3])). % 19.78/19.89 cnf(1102,plain, % 19.78/19.89 (E(f9(a5,a5),f9(f10(a16,f9(a16,a16)),a5))), % 19.78/19.89 inference(scs_inference,[],[866,1083,1073,32,198,500,148,868,515,798,984,1054,1055,1085,2,18,17,3,71,86])). % 19.78/19.89 cnf(1111,plain, % 19.78/19.89 (E(f10(a5,f9(a5,a5)),f10(a15,a17))), % 19.78/19.89 inference(scs_inference,[],[1075,2])). % 19.78/19.89 cnf(1112,plain, % 19.78/19.89 (P2(a5,f10(a15,a17))), % 19.78/19.89 inference(scs_inference,[],[194,1075,1013,2,18])). % 19.78/19.89 cnf(1113,plain, % 19.78/19.89 (E(f9(a6,a17),f9(f9(f10(a15,a6),a15),a17))), % 19.78/19.89 inference(scs_inference,[],[194,866,1075,910,1013,2,18,3])). % 19.78/19.89 cnf(1114,plain, % 19.78/19.89 (P2(f10(a5,f9(a5,a5)),f10(a15,a6))), % 19.78/19.89 inference(scs_inference,[],[194,866,393,1075,910,1013,2,18,3,17])). % 19.78/19.89 cnf(1115,plain, % 19.78/19.89 (E(f9(a1,a1),f9(f9(a1,f9(a1,a1)),a1))), % 19.78/19.89 inference(scs_inference,[],[194,866,393,1057,1075,23,119,868,910,957,1013,2,18,3,17,86])). % 19.78/19.89 cnf(1127,plain, % 19.78/19.89 (E(a1,f9(f9(a1,a1),a1))), % 19.78/19.89 inference(scs_inference,[],[824,393,1099,945,1014,2,18,3])). % 19.78/19.89 cnf(1128,plain, % 19.78/19.89 (P2(f10(a15,a17),a5)), % 19.78/19.89 inference(scs_inference,[],[194,824,393,1099,945,1014,2,18,3,17])). % 19.78/19.89 cnf(1131,plain, % 19.78/19.89 (P2(f9(f9(a1,a1),a1),a1)), % 19.78/19.89 inference(scs_inference,[],[194,824,393,1075,1099,30,28,394,945,1014,1022,2,18,3,17,86,136])). % 19.78/19.89 cnf(1138,plain, % 19.78/19.89 (E(a1,f9(f9(f9(a1,a1),f9(a1,a1)),a1))), % 19.78/19.89 inference(scs_inference,[],[824,393,1113,962,1098,2,18,3])). % 19.78/19.89 cnf(1139,plain, % 19.78/19.89 (P2(f9(a1,a1),f9(a1,f9(a1,a1)))), % 19.78/19.89 inference(scs_inference,[],[824,943,393,1113,962,1098,1055,2,18,3,17])). % 19.78/19.89 cnf(1142,plain, % 19.78/19.89 (P2(f9(f9(f9(a1,a1),f9(a1,a1)),a1),a1)), % 19.78/19.89 inference(scs_inference,[],[824,943,393,1053,1113,32,30,28,962,1098,1055,998,2,18,3,17,86,136])). % 19.78/19.89 cnf(1148,plain, % 19.78/19.89 (E(f9(f9(a1,a1),a1),a1)), % 19.78/19.89 inference(scs_inference,[],[1127,2])). % 19.78/19.89 cnf(1149,plain, % 19.78/19.89 (P2(f9(a1,f9(a1,a1)),f9(a1,a1))), % 19.78/19.89 inference(scs_inference,[],[943,1127,1054,2,18])). % 19.78/19.89 cnf(1150,plain, % 19.78/19.89 (E(f10(a17,f9(a17,a17)),f9(a5,a15))), % 19.78/19.89 inference(scs_inference,[],[943,815,1127,1000,1054,2,18,3])). % 19.78/19.89 cnf(1154,plain, % 19.78/19.89 (P2(a17,f9(a5,a15))), % 19.78/19.89 inference(scs_inference,[],[943,815,393,1127,30,289,119,868,1002,1000,1054,1085,1139,2,18,3,17,71,70])). % 19.78/19.89 cnf(1156,plain, % 19.78/19.89 (E(f9(a5,a5),f9(f10(a15,a17),a5))), % 19.78/19.89 inference(scs_inference,[],[943,815,393,1111,1127,32,30,198,289,172,119,868,1002,1000,1054,1085,1112,1139,2,18,3,17,71,70,86])). % 19.78/19.89 cnf(1159,plain, % 19.78/19.89 (P2(f9(f10(a15,a17),a5),f9(f10(a15,a17),a5))), % 19.78/19.89 inference(scs_inference,[],[943,815,393,1111,1127,32,30,198,289,172,119,868,1002,1000,1054,1085,1112,1139,2,18,3,17,71,70,86,16,58])). % 19.78/19.89 cnf(1166,plain, % 19.78/19.89 (E(f10(a6,f9(a6,a6)),f9(a5,a15))), % 19.78/19.89 inference(scs_inference,[],[194,722,1138,1150,1114,2,18,3])). % 19.78/19.89 cnf(1167,plain, % 19.78/19.89 (P2(f9(a6,a17),f9(a17,a17))), % 19.78/19.89 inference(scs_inference,[],[194,722,939,1138,1150,1114,1097,2,18,3,17])). % 19.78/19.89 cnf(1172,plain, % 19.78/19.89 (E(f9(a17,a17),f9(f9(a5,a15),a17))), % 19.78/19.89 inference(scs_inference,[],[194,722,939,1138,1150,30,33,289,119,259,868,1002,1114,1097,1149,1154,1139,2,18,3,17,71,70,86])). % 19.78/19.89 cnf(1181,plain, % 19.78/19.89 (E(f9(a5,a15),f10(a17,f9(a17,a17)))), % 19.78/19.89 inference(scs_inference,[],[1150,2])). % 19.78/19.89 cnf(1183,plain, % 19.78/19.89 (E(f10(f9(a16,a16),f9(f9(a16,a16),f9(a16,a16))),f9(a5,a16))), % 19.78/19.89 inference(scs_inference,[],[393,1150,540,1061,1128,2,18,3])). % 19.78/19.89 cnf(1185,plain, % 19.78/19.89 (P2(f9(a16,a16),f9(a5,a16))), % 19.78/19.89 inference(scs_inference,[],[927,393,1150,275,540,542,1063,1061,1128,517,2,18,3,17,70])). % 19.78/19.89 cnf(1196,plain, % 19.78/19.89 (E(f9(a5,a15),f10(a6,f9(a6,a6)))), % 19.78/19.89 inference(scs_inference,[],[1166,2])). % 19.78/19.89 cnf(1197,plain, % 19.78/19.89 (P2(f9(a6,a17),f9(f10(a6,f9(a6,a6)),a17))), % 19.78/19.89 inference(scs_inference,[],[1166,754,1167,2,18])). % 19.78/19.89 cnf(1198,plain, % 19.78/19.89 (E(a1,f9(f9(a1,f9(a1,a1)),a1))), % 19.78/19.89 inference(scs_inference,[],[824,1166,754,1115,1167,2,18,3])). % 19.78/19.89 cnf(1199,plain, % 19.78/19.89 (P2(f9(f9(a1,a1),f9(a1,a1)),f9(a1,f9(a1,a1)))), % 19.78/19.89 inference(scs_inference,[],[824,1083,1166,754,1115,1167,1139,2,18,3,17])). % 19.78/19.89 cnf(1200,plain, % 19.78/19.89 (E(f9(f9(a16,a16),f9(a16,a16)),f9(f9(a5,a16),f9(a16,a16)))), % 19.78/19.89 inference(scs_inference,[],[824,1083,1166,1183,275,542,1063,754,1115,1167,1139,1185,2,18,3,17,86])). % 19.78/19.89 cnf(1202,plain, % 19.78/19.89 (P2(f9(f9(a1,f9(a1,a1)),a1),a1)), % 19.78/19.89 inference(scs_inference,[],[824,1083,1166,1183,275,542,1063,754,1115,1167,1139,1185,2,18,3,17,86,136])). % 19.78/19.89 cnf(1203,plain, % 19.78/19.89 (P1(f9(f9(a5,a16),f9(a16,a16)))), % 19.78/19.89 inference(scs_inference,[],[824,1083,1166,1183,275,542,1063,754,1115,1167,1139,1185,2,18,3,17,86,136,16])). % 19.78/19.89 cnf(1210,plain, % 19.78/19.89 (E(f9(a5,a16),f10(f9(a16,a16),f9(f9(a16,a16),f9(a16,a16))))), % 19.78/19.89 inference(scs_inference,[],[1183,2])). % 19.78/19.89 cnf(1211,plain, % 19.78/19.89 (P2(f9(a6,a17),f9(f9(a16,a15),a17))), % 19.78/19.89 inference(scs_inference,[],[1183,777,1167,2,18])). % 19.78/19.89 cnf(1212,plain, % 19.78/19.89 (E(f9(a6,a17),f9(f9(a5,a15),a17))), % 19.78/19.89 inference(scs_inference,[],[866,1183,777,1172,1167,2,18,3])). % 19.78/19.89 cnf(1213,plain, % 19.78/19.89 (P2(f9(f9(a5,a16),f9(a16,a16)),f9(f9(a16,a16),f9(a16,a16)))), % 19.78/19.89 inference(scs_inference,[],[866,1183,777,1172,1167,565,1200,2,18,3,17])). % 19.78/19.89 cnf(1218,plain, % 19.78/19.89 (P2(f9(f9(a1,a1),a1),f10(a1,f9(a1,a1)))), % 19.78/19.89 inference(scs_inference,[],[147,1198,1131,2,18])). % 19.78/19.89 cnf(1219,plain, % 19.78/19.89 (P2(a1,f9(f9(a1,a1),a1))), % 19.78/19.89 inference(scs_inference,[],[147,1198,1148,1131,950,2,18,17])). % 19.78/19.89 cnf(1235,plain, % 19.78/19.89 (P2(f9(a17,a17),f9(f9(a16,a15),a17))), % 19.78/19.89 inference(scs_inference,[],[866,1083,1212,1149,1211,2,18,17])). % 19.78/19.89 cnf(1239,plain, % 19.78/19.89 (~E(x12391,f10(f9(a11,a11),f9(f9(a11,a11),f9(a11,a11))))+P1(x12391)), % 19.78/19.89 inference(scs_inference,[],[866,1083,1212,24,685,802,868,1149,1211,1199,132,2,18,17,71,3,72])). % 19.78/19.89 cnf(1251,plain, % 19.78/19.89 (E(f10(a5,f9(a5,a5)),a16)), % 19.78/19.89 inference(scs_inference,[],[1038,2])). % 19.78/19.89 cnf(1252,plain, % 19.78/19.89 (P2(f9(f9(a1,a1),a1),f9(a1,a1))), % 19.78/19.89 inference(scs_inference,[],[943,1038,1218,2,18])). % 19.78/19.89 cnf(1253,plain, % 19.78/19.89 (P2(f9(a17,a17),f9(f10(a6,f9(a6,a6)),a17))), % 19.78/19.89 inference(scs_inference,[],[943,866,1038,1197,1218,2,18,17])). % 19.78/19.89 cnf(1254,plain, % 19.78/19.89 (P2(a5,a16)), % 19.78/19.89 inference(scs_inference,[],[943,866,1038,32,29,198,1197,1218,2,18,17,70])). % 19.78/19.89 cnf(1258,plain, % 19.78/19.89 (E(f9(a5,a5),f9(a16,a5))), % 19.78/19.89 inference(scs_inference,[],[943,866,1038,32,29,198,289,795,1074,1197,1235,1218,2,18,17,70,71,86])). % 19.78/19.89 cnf(1261,plain, % 19.78/19.89 (P1(f9(a16,a5))), % 19.78/19.89 inference(scs_inference,[],[943,866,1038,32,29,198,289,743,795,1074,1197,1235,1218,2,18,17,70,71,86,3,16])). % 19.78/19.89 cnf(1262,plain, % 19.78/19.89 (P2(f9(a16,a5),f9(a16,a5))), % 19.78/19.89 inference(scs_inference,[],[943,866,1038,32,29,198,289,743,795,1074,1197,1235,1218,2,18,17,70,71,86,3,16,64])). % 19.78/19.89 cnf(1266,plain, % 19.78/19.89 (~E(f7(a12,a17),f10(f9(a17,a6),f9(f9(a17,a6),f9(a17,a6))))+~P1(f7(a12,a15))), % 19.78/19.89 inference(scs_inference,[],[943,866,1038,32,30,33,29,198,289,743,795,215,1074,1197,1235,1218,2,18,17,70,71,86,3,16,64,72,188])). % 19.78/19.89 cnf(1276,plain, % 19.78/19.89 (E(f10(f9(a5,a5),f9(f9(a5,a5),f9(a5,a5))),f9(a16,a5))), % 19.78/19.89 inference(scs_inference,[],[397,596,584,1258,2,18,3])). % 19.78/19.89 cnf(1290,plain, % 19.78/19.89 (E(f9(f9(a5,a5),f9(a5,a5)),f9(f9(a16,a5),f9(a5,a5)))), % 19.78/19.89 inference(scs_inference,[],[32,29,198,289,397,596,399,1097,584,1253,1262,1258,1261,772,1254,2,18,3,17,110,104,64,72,70,71,86])). % 19.78/19.89 cnf(1292,plain, % 19.78/19.89 (P1(f9(f9(a16,a5),f9(a5,a5)))), % 19.78/19.89 inference(scs_inference,[],[32,29,198,289,397,596,399,1097,584,1253,1262,1258,1261,772,1254,2,18,3,17,110,104,64,72,70,71,86,16])). % 19.78/19.89 cnf(1306,plain, % 19.78/19.89 (E(f9(a16,a5),f9(a5,a5))), % 19.78/19.89 inference(scs_inference,[],[1276,399,428,1290,1292,2,18,17,71,628])). % 19.78/19.89 cnf(1308,plain, % 19.78/19.89 (~E(x13081,f10(f9(a6,a6),f9(f9(a6,a6),f9(a6,a6))))+P1(x13081)), % 19.78/19.89 inference(scs_inference,[],[1276,33,854,399,428,1290,1292,200,2,18,17,71,628,3,72])). % 19.78/19.89 cnf(1320,plain, % 19.78/19.89 (E(f9(a17,a17),f10(f9(a17,a17),f9(f9(a17,a17),f9(a17,a17))))), % 19.78/19.89 inference(scs_inference,[],[578,2])). % 19.78/19.89 cnf(1321,plain, % 19.78/19.89 (P2(f9(f9(a1,a1),a1),f9(f9(a1,a1),f9(a1,a1)))), % 19.78/19.89 inference(scs_inference,[],[1083,578,1252,2,18])). % 19.78/19.89 cnf(1322,plain, % 19.78/19.89 (E(f9(a16,a5),f9(f10(a15,a6),a5))), % 19.78/19.89 inference(scs_inference,[],[1083,1306,578,1024,1252,2,18,3])). % 19.78/19.89 cnf(1327,plain, % 19.78/19.89 (E(f9(f10(a15,a6),a5),f9(a16,a5))), % 19.78/19.89 inference(scs_inference,[],[1322,2])). % 19.78/19.89 cnf(1329,plain, % 19.78/19.89 (E(f9(a16,a5),f9(f10(a16,f9(a16,a16)),a5))), % 19.78/19.89 inference(scs_inference,[],[1320,1322,1306,1102,1167,2,18,3])). % 19.78/19.89 cnf(1336,plain, % 19.78/19.89 (E(f9(a16,a5),f9(f10(a15,a17),a5))), % 19.78/19.89 inference(scs_inference,[],[1329,1327,1306,1156,1029,2,18,3])). % 19.78/19.89 cnf(1341,plain, % 19.78/19.89 (E(f9(f10(a15,a17),a5),f9(a16,a5))), % 19.78/19.89 inference(scs_inference,[],[1336,2])). % 19.78/19.89 cnf(1342,plain, % 19.78/19.89 (P2(f9(a5,a15),f10(a6,f9(a6,a6)))), % 19.78/19.89 inference(scs_inference,[],[1196,1336,1005,2,18])). % 19.78/19.89 cnf(1357,plain, % 19.78/19.89 (E(f9(a11,a11),f10(f9(a11,a11),f9(f9(a11,a11),f9(a11,a11))))), % 19.78/19.89 inference(scs_inference,[],[685,2])). % 19.78/19.89 cnf(1376,plain, % 19.78/19.89 (P2(f9(a5,a15),f10(a17,f9(a17,a17)))), % 19.78/19.89 inference(scs_inference,[],[1181,743,1005,2,18])). % 19.78/19.89 cnf(1379,plain, % 19.78/19.89 (~E(a12,f10(f7(a12,a15),f7(a12,a17)))+P1(f10(f7(a12,a15),a14))), % 19.78/19.89 inference(scs_inference,[],[393,1181,25,743,46,1254,1005,2,18,17,3,16])). % 19.78/19.89 cnf(1392,plain, % 19.78/19.89 (E(a15,f10(a15,f9(a15,a15)))), % 19.78/19.89 inference(scs_inference,[],[300,2])). % 19.78/19.89 cnf(1393,plain, % 19.78/19.89 (P2(f9(a5,a15),f9(a16,a15))), % 19.78/19.89 inference(scs_inference,[],[768,300,1376,2,18])). % 19.78/19.89 cnf(1396,plain, % 19.78/19.89 (P2(f10(a15,f9(a15,a15)),f10(a15,f9(a15,a15)))), % 19.78/19.89 inference(scs_inference,[],[768,28,300,222,1376,2,18,16,17,64])). % 19.78/19.89 cnf(1418,plain, % 19.78/19.89 (P2(f10(a15,f9(a15,a15)),f10(a15,a17))), % 19.78/19.89 inference(scs_inference,[],[1392,804,300,195,1396,2,18,17])). % 19.78/19.89 cnf(1438,plain, % 19.78/19.89 (E(f9(a6,a6),f10(f9(a6,a6),f9(f9(a6,a6),f9(a6,a6))))), % 19.78/19.89 inference(scs_inference,[],[854,2])). % 19.78/19.89 cnf(1439,plain, % 19.78/19.89 (P2(f9(a5,a15),f9(f10(a15,a17),a15))), % 19.78/19.89 inference(scs_inference,[],[254,854,1393,2,18])). % 19.78/19.89 cnf(1457,plain, % 19.78/19.89 (E(f10(f9(a6,a6),f9(f9(a6,a6),f9(a6,a6))),f9(a17,a6))), % 19.78/19.89 inference(scs_inference,[],[1438,499,881,929,928,856,2,18,17,71])). % 19.78/19.89 cnf(1459,plain, % 19.78/19.89 (E(f9(f9(a6,a6),f9(a6,a6)),f9(f9(a17,a6),f9(a6,a6)))), % 19.78/19.89 inference(scs_inference,[],[1438,499,259,881,852,929,928,856,2,18,17,71,86])). % 19.78/19.89 cnf(1477,plain, % 19.78/19.89 (P2(f10(a15,f9(a15,a15)),f10(a16,f9(a16,a16)))), % 19.78/19.89 inference(scs_inference,[],[824,1392,1457,548,849,2,18,17])). % 19.78/19.89 cnf(1495,plain, % 19.78/19.89 (P2(f9(a1,a1),f9(f9(a1,a1),a1))), % 19.78/19.89 inference(scs_inference,[],[824,550,1219,1142,2,18,17])). % 19.78/19.89 cnf(1513,plain, % 19.78/19.89 (E(f9(f9(a16,a15),a6),f9(a6,a6))), % 19.78/19.89 inference(scs_inference,[],[519,2])). % 19.78/19.89 cnf(1515,plain, % 19.78/19.89 (P2(f10(a6,f9(a6,a6)),f9(a5,a15))), % 19.78/19.89 inference(scs_inference,[],[824,1196,519,1202,1005,2,18,17])). % 19.78/19.89 cnf(1533,plain, % 19.78/19.89 (~E(x15331,f9(f9(a16,a16),f9(a16,a16)))+P1(x15331)), % 19.78/19.89 inference(scs_inference,[],[1181,275,1063,592,1200,1459,1342,869,1185,2,18,17,3,72])). % 19.78/19.89 cnf(1545,plain, % 19.78/19.89 (E(f9(f10(a15,a17),a16),f9(a16,a16))), % 19.78/19.89 inference(scs_inference,[],[569,2])). % 19.78/19.89 cnf(1548,plain, % 19.78/19.89 (E(f9(f9(a1,a1),f9(a1,a1)),f9(f9(a1,a1),a1))), % 19.78/19.89 inference(scs_inference,[],[1083,569,802,947,1495,1321,858,2,18,17,71])). % 19.78/19.89 cnf(1568,plain, % 19.78/19.89 (P2(f9(f10(a15,a17),a15),f9(a5,a15))), % 19.78/19.89 inference(scs_inference,[],[469,1513,1548,1545,626,1515,598,2,18,3,17])). % 19.78/19.89 cnf(1569,plain, % 19.78/19.89 (E(f9(f10(a15,a17),a15),f9(a5,a15))), % 19.78/19.89 inference(scs_inference,[],[469,1513,1548,1545,1002,626,213,1515,598,1439,2,18,3,17,71])). % 19.78/19.89 cnf(1578,plain, % 19.78/19.89 (E(f9(f10(a15,a17),a16),f9(a5,a16))), % 19.78/19.89 inference(scs_inference,[],[1341,1569,1545,1061,1159,2,18,3])). % 19.78/19.89 cnf(1611,plain, % 19.78/19.89 (~E(x16111,f9(f9(a6,a6),f9(a6,a6)))+P1(x16111)), % 19.78/19.89 inference(scs_inference,[],[270,1578,499,259,1002,233,928,1459,1568,1439,2,18,17,71,3,72])). % 19.78/19.89 cnf(1684,plain, % 19.78/19.89 (P2(f9(f9(a16,a16),f9(a16,a16)),f9(f9(a5,a16),f9(a16,a16)))), % 19.78/19.89 inference(scs_inference,[],[661,1200,565,2,18])). % 19.78/19.89 cnf(1685,plain, % 19.78/19.89 (E(f10(a15,a17),f10(f10(a15,a6),f9(f10(a15,a6),f10(a15,a6))))), % 19.78/19.89 inference(scs_inference,[],[211,661,1200,565,2,18,3])). % 19.78/19.89 cnf(1706,plain, % 19.78/19.89 (~E(x17061,f9(f10(a15,a6),f10(a15,a6)))+P1(x17061)), % 19.78/19.89 inference(scs_inference,[],[1327,658,1685,172,193,542,663,1203,683,1213,1684,1029,291,2,18,17,71,86,3,16,64,72])). % 19.78/19.89 cnf(1736,plain, % 19.78/19.89 (~P1(f7(a12,a15))+P1(f10(f7(a12,a15),f7(a12,a17)))), % 19.78/19.89 inference(scs_inference,[],[698,27,300,46,1396,339,2,18,17,16,1379,1533,1611,1706,912,65])). % 19.78/19.89 cnf(1743,plain, % 19.78/19.89 (E(f10(a15,a6),f10(f10(a15,a17),f9(f10(a15,a17),f10(a15,a17))))), % 19.78/19.89 inference(scs_inference,[],[194,1210,701,1185,2,18,3])). % 19.78/19.89 cnf(1762,plain, % 19.78/19.89 (~E(x17621,f9(f10(a15,a17),f10(a15,a17)))+P1(x17621)), % 19.78/19.89 inference(scs_inference,[],[1341,1357,1743,172,193,703,684,1159,665,2,18,17,86,3,16,64,72])). % 19.78/19.89 cnf(1801,plain, % 19.78/19.89 (P2(f10(a15,f9(a15,a15)),f10(a5,f9(a5,a5)))), % 19.78/19.89 inference(scs_inference,[],[1392,962,1022,2,17])). % 19.78/19.89 cnf(1808,plain, % 19.78/19.89 (P2(f10(a15,f9(a15,a15)),a5)), % 19.78/19.89 inference(scs_inference,[],[1392,1000,998,2,17])). % 19.78/19.89 cnf(1921,plain, % 19.78/19.89 (E(f10(a15,f9(a15,a15)),f8(a13,a12))), % 19.78/19.89 inference(scs_inference,[],[300,36,2,3])). % 19.78/19.89 cnf(1932,plain, % 19.78/19.89 (P2(f8(a13,a12),a15)), % 19.78/19.89 inference(scs_inference,[],[28,300,36,302,465,2,3,16,64,104,70,86,17,18])). % 19.78/19.89 cnf(1959,plain, % 19.78/19.89 (E(f10(a5,f9(a5,a5)),f8(f10(a13,a14),a12))), % 19.78/19.89 inference(scs_inference,[],[1251,44,2,3])). % 19.78/19.89 cnf(1960,plain, % 19.78/19.89 (P1(f8(f10(a13,a14),a12))), % 19.78/19.89 inference(scs_inference,[],[1251,29,44,2,3,16])). % 19.78/19.89 cnf(1963,plain, % 19.78/19.89 (P2(f8(f10(a13,a14),a12),f8(f10(a13,a14),a12))), % 19.78/19.89 inference(scs_inference,[],[1251,1392,1921,29,44,1477,1932,2,3,16,17,18,64])). % 19.78/19.89 cnf(1967,plain, % 19.78/19.89 (E(f9(a5,a5),f9(f8(f10(a13,a14),a12),a5))), % 19.78/19.89 inference(scs_inference,[],[1251,1392,1921,32,29,44,198,1477,1932,2,3,16,17,18,64,70,86])). % 19.78/19.89 cnf(1974,plain, % 19.78/19.89 (E(f8(f10(a13,a14),a12),f10(a5,f9(a5,a5)))), % 19.78/19.89 inference(scs_inference,[],[1959,2])). % 19.78/19.89 cnf(1975,plain, % 19.78/19.89 (E(f10(a15,a6),f8(f10(a13,a14),a12))), % 19.78/19.89 inference(scs_inference,[],[1015,1959,2,3])). % 19.78/19.89 cnf(1979,plain, % 19.78/19.89 (P2(a15,f8(f10(a13,a14),a12))), % 19.78/19.89 inference(scs_inference,[],[1015,1921,1959,33,28,44,198,1418,1963,1967,1960,2,3,17,16,18,70])). % 19.78/19.89 cnf(1989,plain, % 19.78/19.89 (E(f10(a15,a17),f8(f10(a13,a14),a12))), % 19.78/19.89 inference(scs_inference,[],[211,1975,2,3])). % 19.78/19.89 cnf(2000,plain, % 19.78/19.89 (E(f9(a16,a5),f9(f8(f10(a13,a14),a12),a5))), % 19.78/19.89 inference(scs_inference,[],[1306,1921,1989,1801,1967,2,17,3])). % 19.78/19.89 cnf(2009,plain, % 19.78/19.89 (P2(f8(f10(a13,a14),a12),f10(a5,f9(a5,a5)))), % 19.78/19.89 inference(scs_inference,[],[1921,2000,1974,1808,1963,2,17,18])). % 19.78/19.89 cnf(2056,plain, % 19.78/19.89 ($false), % 19.78/19.89 inference(scs_inference,[],[49,1073,1392,25,30,26,27,216,46,34,218,2009,1979,2,16,3,17,18,64,104,76,70,86,493,507,1266,1308,1762,1736,1533,1611,1706,1239,333,154,66]), % 19.78/19.89 ['proof']). % 19.78/19.89 % SZS output end Proof % 19.78/19.89 % Total time :19.230000s %------------------------------------------------------------------------------