%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM523+1 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : 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:49 EDT 2024 % Result : Theorem 81.54s 81.60s % Output : CNFRefutation 81.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM523+1 : TPTP v8.2.0. Released v4.0.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n019.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Sat Jun 22 23:37:39 EDT 2024 % 0.13/0.34 % CPUTime : % 0.52/0.57 start to proof:theBenchmark % 81.54/81.58 %------------------------------------------- % 81.54/81.58 % File :CSE---1.7 % 81.54/81.58 % Problem :theBenchmark % 81.54/81.58 % Transform :cnf % 81.54/81.58 % Format :tptp:raw % 81.54/81.58 % Command :java -jar mcs_scs.jar %d %s % 81.54/81.58 % 81.54/81.58 % Result :Theorem 80.940000s % 81.54/81.58 % Output :CNFRefutation 80.940000s % 81.54/81.58 %------------------------------------------- % 81.54/81.59 %------------------------------------------------------------------------------ % 81.54/81.59 % File : NUM523+1 : TPTP v8.2.0. Released v4.0.0. % 81.54/81.59 % Domain : Number Theory % 81.54/81.59 % Problem : Square root of a prime is irrational 15_01, 00 expansion % 81.54/81.59 % Version : Especial. % 81.54/81.59 % English : % 81.54/81.59 % 81.54/81.59 % Refs : [LPV06] Lyaletski et al. (2006), SAD as a Mathematical Assista % 81.54/81.59 % : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 81.54/81.59 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 81.54/81.59 % Source : [Pas08] % 81.54/81.59 % Names : primes_15_01.00 [Pas08] % 81.54/81.59 % 81.54/81.59 % Status : Theorem % 81.54/81.59 % Rating : 0.36 v8.2.0, 0.39 v8.1.0, 0.33 v7.5.0, 0.34 v7.4.0, 0.30 v7.3.0, 0.34 v7.2.0, 0.31 v7.1.0, 0.30 v6.4.0, 0.35 v6.3.0, 0.29 v6.2.0, 0.44 v6.1.0, 0.50 v6.0.0, 0.39 v5.5.0, 0.59 v5.4.0, 0.57 v5.3.0, 0.59 v5.2.0, 0.50 v5.1.0, 0.52 v5.0.0, 0.50 v4.1.0, 0.57 v4.0.1, 0.78 v4.0.0 % 81.54/81.59 % Syntax : Number of formulae : 44 ( 3 unt; 5 def) % 81.54/81.59 % Number of atoms : 209 ( 64 equ) % 81.54/81.59 % Maximal formula atoms : 10 ( 4 avg) % 81.54/81.59 % Number of connectives : 192 ( 27 ~; 8 |; 88 &) % 81.54/81.59 % ( 5 <=>; 64 =>; 0 <=; 0 <~>) % 81.54/81.59 % Maximal formula depth : 11 ( 6 avg) % 81.54/81.59 % Maximal term depth : 3 ( 1 avg) % 81.54/81.59 % Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty) % 81.54/81.59 % Number of functors : 9 ( 9 usr; 5 con; 0-2 aty) % 81.54/81.59 % Number of variables : 88 ( 85 !; 3 ?) % 81.54/81.59 % SPC : FOF_THM_RFO_SEQ % 81.54/81.59 % 81.54/81.59 % Comments : Problem generated by the SAD system [VLP07] % 81.54/81.59 %------------------------------------------------------------------------------ % 81.54/81.59 fof(mNatSort,axiom, % 81.54/81.59 ! [W0] : % 81.54/81.59 ( aNaturalNumber0(W0) % 81.54/81.59 => $true ) ). % 81.54/81.59 % 81.54/81.59 fof(mSortsC,axiom, % 81.54/81.59 aNaturalNumber0(sz00) ). % 81.54/81.59 % 81.54/81.59 fof(mSortsC_01,axiom, % 81.54/81.59 ( aNaturalNumber0(sz10) % 81.54/81.59 & sz10 != sz00 ) ). % 81.54/81.59 % 81.54/81.59 fof(mSortsB,axiom, % 81.54/81.59 ! [W0,W1] : % 81.54/81.59 ( ( aNaturalNumber0(W0) % 81.54/81.59 & aNaturalNumber0(W1) ) % 81.54/81.59 => aNaturalNumber0(sdtpldt0(W0,W1)) ) ). % 81.54/81.59 % 81.54/81.59 fof(mSortsB_02,axiom, % 81.54/81.59 ! [W0,W1] : % 81.54/81.59 ( ( aNaturalNumber0(W0) % 81.54/81.59 & aNaturalNumber0(W1) ) % 81.54/81.59 => aNaturalNumber0(sdtasdt0(W0,W1)) ) ). % 81.54/81.59 % 81.54/81.59 fof(mAddComm,axiom, % 81.54/81.59 ! [W0,W1] : % 81.54/81.59 ( ( aNaturalNumber0(W0) % 81.54/81.59 & aNaturalNumber0(W1) ) % 81.54/81.59 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 81.54/81.59 % 81.54/81.59 fof(mAddAsso,axiom, % 81.54/81.59 ! [W0,W1,W2] : % 81.54/81.59 ( ( aNaturalNumber0(W0) % 81.54/81.59 & aNaturalNumber0(W1) % 81.54/81.59 & aNaturalNumber0(W2) ) % 81.54/81.59 => sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) ). % 81.54/81.59 % 81.54/81.59 fof(m_AddZero,axiom, % 81.54/81.59 ! [W0] : % 81.54/81.59 ( aNaturalNumber0(W0) % 81.54/81.59 => ( sdtpldt0(W0,sz00) = W0 % 81.54/81.59 & W0 = sdtpldt0(sz00,W0) ) ) ). % 81.54/81.59 % 81.54/81.59 fof(mMulComm,axiom, % 81.54/81.59 ! [W0,W1] : % 81.54/81.59 ( ( aNaturalNumber0(W0) % 81.54/81.59 & aNaturalNumber0(W1) ) % 81.54/81.59 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 81.54/81.59 % 81.54/81.59 fof(mMulAsso,axiom, % 81.54/81.59 ! [W0,W1,W2] : % 81.54/81.59 ( ( aNaturalNumber0(W0) % 81.54/81.59 & aNaturalNumber0(W1) % 81.54/81.59 & aNaturalNumber0(W2) ) % 81.54/81.59 => sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) ). % 81.54/81.59 % 81.54/81.59 fof(m_MulUnit,axiom, % 81.54/81.59 ! [W0] : % 81.54/81.59 ( aNaturalNumber0(W0) % 81.54/81.59 => ( sdtasdt0(W0,sz10) = W0 % 81.54/81.59 & W0 = sdtasdt0(sz10,W0) ) ) ). % 81.54/81.59 % 81.54/81.59 fof(m_MulZero,axiom, % 81.54/81.59 ! [W0] : % 81.54/81.59 ( aNaturalNumber0(W0) % 81.54/81.59 => ( sdtasdt0(W0,sz00) = sz00 % 81.54/81.59 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 81.54/81.59 % 81.54/81.59 fof(mAMDistr,axiom, % 81.54/81.59 ! [W0,W1,W2] : % 81.54/81.59 ( ( aNaturalNumber0(W0) % 81.54/81.59 & aNaturalNumber0(W1) % 81.54/81.59 & aNaturalNumber0(W2) ) % 81.54/81.59 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 81.54/81.59 & sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ). % 81.54/81.59 % 81.54/81.59 fof(mAddCanc,axiom, % 81.54/81.59 ! [W0,W1,W2] : % 81.54/81.59 ( ( aNaturalNumber0(W0) % 81.54/81.59 & aNaturalNumber0(W1) % 81.54/81.59 & aNaturalNumber0(W2) ) % 81.54/81.59 => ( ( sdtpldt0(W0,W1) = sdtpldt0(W0,W2) % 81.54/81.59 | sdtpldt0(W1,W0) = sdtpldt0(W2,W0) ) % 81.54/81.59 => W1 = W2 ) ) ). % 81.54/81.59 % 81.54/81.59 fof(mMulCanc,axiom, % 81.54/81.59 ! [W0] : % 81.54/81.59 ( aNaturalNumber0(W0) % 81.54/81.59 => ( W0 != sz00 % 81.54/81.59 => ! [W1,W2] : % 81.54/81.59 ( ( aNaturalNumber0(W1) % 81.54/81.59 & aNaturalNumber0(W2) ) % 81.54/81.59 => ( ( sdtasdt0(W0,W1) = sdtasdt0(W0,W2) % 81.54/81.59 | sdtasdt0(W1,W0) = sdtasdt0(W2,W0) ) % 81.54/81.59 => W1 = W2 ) ) ) ) ). % 81.54/81.59 % 81.54/81.59 fof(mZeroAdd,axiom, % 81.54/81.59 ! [W0,W1] : % 81.54/81.59 ( ( aNaturalNumber0(W0) % 81.54/81.59 & aNaturalNumber0(W1) ) % 81.54/81.59 => ( sdtpldt0(W0,W1) = sz00 % 81.54/81.59 => ( W0 = sz00 % 81.54/81.59 & W1 = sz00 ) ) ) ). % 81.54/81.59 % 81.54/81.59 fof(mZeroMul,axiom, % 81.54/81.59 ! [W0,W1] : % 81.54/81.60 ( ( aNaturalNumber0(W0) % 81.54/81.60 & aNaturalNumber0(W1) ) % 81.54/81.60 => ( sdtasdt0(W0,W1) = sz00 % 81.54/81.60 => ( W0 = sz00 % 81.54/81.60 | W1 = sz00 ) ) ) ). % 81.54/81.60 % 81.54/81.60 fof(mDefLE,definition, % 81.54/81.60 ! [W0,W1] : % 81.54/81.60 ( ( aNaturalNumber0(W0) % 81.54/81.60 & aNaturalNumber0(W1) ) % 81.54/81.60 => ( sdtlseqdt0(W0,W1) % 81.54/81.60 <=> ? [W2] : % 81.54/81.60 ( aNaturalNumber0(W2) % 81.54/81.60 & sdtpldt0(W0,W2) = W1 ) ) ) ). % 81.54/81.60 % 81.54/81.60 fof(mDefDiff,definition, % 81.54/81.60 ! [W0,W1] : % 81.54/81.60 ( ( aNaturalNumber0(W0) % 81.54/81.60 & aNaturalNumber0(W1) ) % 81.54/81.60 => ( sdtlseqdt0(W0,W1) % 81.54/81.60 => ! [W2] : % 81.54/81.60 ( W2 = sdtmndt0(W1,W0) % 81.54/81.60 <=> ( aNaturalNumber0(W2) % 81.54/81.60 & sdtpldt0(W0,W2) = W1 ) ) ) ) ). % 81.54/81.60 % 81.54/81.60 fof(mLERefl,axiom, % 81.54/81.60 ! [W0] : % 81.54/81.60 ( aNaturalNumber0(W0) % 81.54/81.60 => sdtlseqdt0(W0,W0) ) ). % 81.54/81.60 % 81.54/81.60 fof(mLEAsym,axiom, % 81.54/81.60 ! [W0,W1] : % 81.54/81.60 ( ( aNaturalNumber0(W0) % 81.54/81.60 & aNaturalNumber0(W1) ) % 81.54/81.60 => ( ( sdtlseqdt0(W0,W1) % 81.54/81.60 & sdtlseqdt0(W1,W0) ) % 81.54/81.60 => W0 = W1 ) ) ). % 81.54/81.60 % 81.54/81.60 fof(mLETran,axiom, % 81.54/81.60 ! [W0,W1,W2] : % 81.54/81.60 ( ( aNaturalNumber0(W0) % 81.54/81.60 & aNaturalNumber0(W1) % 81.54/81.60 & aNaturalNumber0(W2) ) % 81.54/81.60 => ( ( sdtlseqdt0(W0,W1) % 81.54/81.60 & sdtlseqdt0(W1,W2) ) % 81.54/81.60 => sdtlseqdt0(W0,W2) ) ) ). % 81.54/81.60 % 81.54/81.60 fof(mLETotal,axiom, % 81.54/81.60 ! [W0,W1] : % 81.54/81.60 ( ( aNaturalNumber0(W0) % 81.54/81.60 & aNaturalNumber0(W1) ) % 81.54/81.60 => ( sdtlseqdt0(W0,W1) % 81.54/81.60 | ( W1 != W0 % 81.54/81.60 & sdtlseqdt0(W1,W0) ) ) ) ). % 81.54/81.60 % 81.54/81.60 fof(mMonAdd,axiom, % 81.54/81.60 ! [W0,W1] : % 81.54/81.60 ( ( aNaturalNumber0(W0) % 81.54/81.60 & aNaturalNumber0(W1) ) % 81.54/81.60 => ( ( W0 != W1 % 81.54/81.60 & sdtlseqdt0(W0,W1) ) % 81.54/81.60 => ! [W2] : % 81.54/81.60 ( aNaturalNumber0(W2) % 81.54/81.60 => ( sdtpldt0(W2,W0) != sdtpldt0(W2,W1) % 81.54/81.60 & sdtlseqdt0(sdtpldt0(W2,W0),sdtpldt0(W2,W1)) % 81.54/81.60 & sdtpldt0(W0,W2) != sdtpldt0(W1,W2) % 81.54/81.60 & sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W2)) ) ) ) ) ). % 81.54/81.60 % 81.54/81.60 fof(mMonMul,axiom, % 81.54/81.60 ! [W0,W1,W2] : % 81.54/81.60 ( ( aNaturalNumber0(W0) % 81.54/81.60 & aNaturalNumber0(W1) % 81.54/81.60 & aNaturalNumber0(W2) ) % 81.54/81.60 => ( ( W0 != sz00 % 81.54/81.60 & W1 != W2 % 81.54/81.60 & sdtlseqdt0(W1,W2) ) % 81.54/81.60 => ( sdtasdt0(W0,W1) != sdtasdt0(W0,W2) % 81.54/81.60 & sdtlseqdt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 81.54/81.60 & sdtasdt0(W1,W0) != sdtasdt0(W2,W0) % 81.54/81.60 & sdtlseqdt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ) ). % 81.54/81.60 % 81.54/81.60 fof(mLENTr,axiom, % 81.54/81.60 ! [W0] : % 81.54/81.60 ( aNaturalNumber0(W0) % 81.54/81.60 => ( W0 = sz00 % 81.54/81.60 | W0 = sz10 % 81.54/81.60 | ( sz10 != W0 % 81.54/81.60 & sdtlseqdt0(sz10,W0) ) ) ) ). % 81.54/81.60 % 81.54/81.60 fof(mMonMul2,axiom, % 81.54/81.60 ! [W0,W1] : % 81.54/81.60 ( ( aNaturalNumber0(W0) % 81.54/81.60 & aNaturalNumber0(W1) ) % 81.54/81.60 => ( W0 != sz00 % 81.54/81.60 => sdtlseqdt0(W1,sdtasdt0(W1,W0)) ) ) ). % 81.54/81.60 % 81.54/81.60 fof(mIH,axiom, % 81.54/81.60 ! [W0,W1] : % 81.54/81.60 ( ( aNaturalNumber0(W0) % 81.54/81.60 & aNaturalNumber0(W1) ) % 81.54/81.60 => ( iLess0(W0,W1) % 81.54/81.60 => $true ) ) ). % 81.54/81.60 % 81.54/81.60 fof(mIH_03,axiom, % 81.54/81.60 ! [W0,W1] : % 81.54/81.60 ( ( aNaturalNumber0(W0) % 81.54/81.60 & aNaturalNumber0(W1) ) % 81.54/81.60 => ( ( W0 != W1 % 81.54/81.60 & sdtlseqdt0(W0,W1) ) % 81.54/81.60 => iLess0(W0,W1) ) ) ). % 81.54/81.60 % 81.54/81.60 fof(mDefDiv,definition, % 81.54/81.60 ! [W0,W1] : % 81.54/81.60 ( ( aNaturalNumber0(W0) % 81.54/81.60 & aNaturalNumber0(W1) ) % 81.54/81.60 => ( doDivides0(W0,W1) % 81.54/81.60 <=> ? [W2] : % 81.54/81.60 ( aNaturalNumber0(W2) % 81.54/81.60 & W1 = sdtasdt0(W0,W2) ) ) ) ). % 81.54/81.60 % 81.54/81.60 fof(mDefQuot,definition, % 81.54/81.60 ! [W0,W1] : % 81.54/81.60 ( ( aNaturalNumber0(W0) % 81.54/81.60 & aNaturalNumber0(W1) ) % 81.54/81.60 => ( ( W0 != sz00 % 81.54/81.60 & doDivides0(W0,W1) ) % 81.54/81.60 => ! [W2] : % 81.54/81.60 ( W2 = sdtsldt0(W1,W0) % 81.54/81.60 <=> ( aNaturalNumber0(W2) % 81.54/81.60 & W1 = sdtasdt0(W0,W2) ) ) ) ) ). % 81.54/81.60 % 81.54/81.60 fof(mDivTrans,axiom, % 81.54/81.60 ! [W0,W1,W2] : % 81.54/81.60 ( ( aNaturalNumber0(W0) % 81.54/81.60 & aNaturalNumber0(W1) % 81.54/81.60 & aNaturalNumber0(W2) ) % 81.54/81.60 => ( ( doDivides0(W0,W1) % 81.54/81.60 & doDivides0(W1,W2) ) % 81.54/81.60 => doDivides0(W0,W2) ) ) ). % 81.54/81.60 % 81.54/81.60 fof(mDivSum,axiom, % 81.54/81.60 ! [W0,W1,W2] : % 81.54/81.60 ( ( aNaturalNumber0(W0) % 81.54/81.60 & aNaturalNumber0(W1) % 81.54/81.60 & aNaturalNumber0(W2) ) % 81.54/81.60 => ( ( doDivides0(W0,W1) % 81.54/81.60 & doDivides0(W0,W2) ) % 81.54/81.60 => doDivides0(W0,sdtpldt0(W1,W2)) ) ) ). % 81.54/81.60 % 81.54/81.60 fof(mDivMin,axiom, % 81.54/81.60 ! [W0,W1,W2] : % 81.54/81.60 ( ( aNaturalNumber0(W0) % 81.54/81.60 & aNaturalNumber0(W1) % 81.54/81.60 & aNaturalNumber0(W2) ) % 81.54/81.60 => ( ( doDivides0(W0,W1) % 81.54/81.60 & doDivides0(W0,sdtpldt0(W1,W2)) ) % 81.54/81.60 => doDivides0(W0,W2) ) ) ). % 81.54/81.60 % 81.54/81.60 fof(mDivLE,axiom, % 81.54/81.60 ! [W0,W1] : % 81.54/81.60 ( ( aNaturalNumber0(W0) % 81.54/81.60 & aNaturalNumber0(W1) ) % 81.54/81.60 => ( ( doDivides0(W0,W1) % 81.54/81.60 & W1 != sz00 ) % 81.54/81.60 => sdtlseqdt0(W0,W1) ) ) ). % 81.54/81.60 % 81.54/81.60 fof(mDivAsso,axiom, % 81.54/81.60 ! [W0,W1] : % 81.54/81.60 ( ( aNaturalNumber0(W0) % 81.54/81.60 & aNaturalNumber0(W1) ) % 81.54/81.60 => ( ( W0 != sz00 % 81.54/81.60 & doDivides0(W0,W1) ) % 81.54/81.60 => ! [W2] : % 81.54/81.60 ( aNaturalNumber0(W2) % 81.54/81.60 => sdtasdt0(W2,sdtsldt0(W1,W0)) = sdtsldt0(sdtasdt0(W2,W1),W0) ) ) ) ). % 81.54/81.60 % 81.54/81.60 fof(mDefPrime,definition, % 81.54/81.60 ! [W0] : % 81.54/81.60 ( aNaturalNumber0(W0) % 81.54/81.60 => ( isPrime0(W0) % 81.54/81.60 <=> ( W0 != sz00 % 81.54/81.60 & W0 != sz10 % 81.54/81.60 & ! [W1] : % 81.54/81.60 ( ( aNaturalNumber0(W1) % 81.54/81.60 & doDivides0(W1,W0) ) % 81.54/81.60 => ( W1 = sz10 % 81.54/81.60 | W1 = W0 ) ) ) ) ) ). % 81.54/81.60 % 81.54/81.60 fof(mPrimDiv,axiom, % 81.54/81.60 ! [W0] : % 81.54/81.60 ( ( aNaturalNumber0(W0) % 81.54/81.60 & W0 != sz00 % 81.54/81.60 & W0 != sz10 ) % 81.54/81.60 => ? [W1] : % 81.54/81.60 ( aNaturalNumber0(W1) % 81.54/81.60 & doDivides0(W1,W0) % 81.54/81.60 & isPrime0(W1) ) ) ). % 81.54/81.60 % 81.54/81.60 fof(mPDP,axiom, % 81.54/81.60 ! [W0,W1,W2] : % 81.54/81.60 ( ( aNaturalNumber0(W0) % 81.54/81.60 & aNaturalNumber0(W1) % 81.54/81.60 & aNaturalNumber0(W2) ) % 81.54/81.60 => ( ( isPrime0(W2) % 81.54/81.60 & doDivides0(W2,sdtasdt0(W0,W1)) ) % 81.54/81.60 => ( doDivides0(W2,W0) % 81.54/81.60 | doDivides0(W2,W1) ) ) ) ). % 81.54/81.60 % 81.54/81.60 fof(m__2987,hypothesis, % 81.54/81.60 ( aNaturalNumber0(xn) % 81.54/81.60 & aNaturalNumber0(xm) % 81.54/81.60 & aNaturalNumber0(xp) % 81.54/81.60 & xn != sz00 % 81.54/81.60 & xm != sz00 % 81.54/81.60 & xp != sz00 ) ). % 81.54/81.60 % 81.54/81.60 fof(m__2963,hypothesis, % 81.54/81.60 ! [W0,W1,W2] : % 81.54/81.60 ( ( aNaturalNumber0(W0) % 81.54/81.60 & aNaturalNumber0(W1) % 81.54/81.60 & aNaturalNumber0(W2) % 81.54/81.60 & W0 != sz00 % 81.54/81.60 & W1 != sz00 % 81.54/81.60 & W2 != sz00 ) % 81.54/81.60 => ( sdtasdt0(W2,sdtasdt0(W1,W1)) = sdtasdt0(W0,W0) % 81.54/81.60 => ( iLess0(W0,xn) % 81.54/81.60 => ~ isPrime0(W2) ) ) ) ). % 81.54/81.60 % 81.54/81.60 fof(m__3014,hypothesis, % 81.54/81.60 sdtasdt0(xp,sdtasdt0(xm,xm)) = sdtasdt0(xn,xn) ). % 81.54/81.60 % 81.54/81.60 fof(m__3025,hypothesis, % 81.54/81.60 isPrime0(xp) ). % 81.54/81.60 % 81.54/81.60 fof(m__,conjecture, % 81.54/81.60 ( doDivides0(xp,sdtasdt0(xn,xn)) % 81.54/81.60 & doDivides0(xp,xn) ) ). % 81.54/81.60 % 81.54/81.60 %------------------------------------------------------------------------------ % 81.54/81.60 %------------------------------------------- % 81.54/81.60 % Proof found % 81.54/81.60 % SZS status Theorem for theBenchmark % 81.54/81.60 % SZS output start Proof % 81.54/81.60 %ClaNum:103(EqnAxiom:25) % 81.54/81.60 %VarNum:450(SingletonVarNum:134) % 81.54/81.60 %MaxLitNum:9 % 81.54/81.60 %MaxfuncDepth:2 % 81.54/81.60 %SharedTerms:21 % 81.54/81.60 %goalClause: 76 % 81.54/81.60 [26]P1(a1) % 81.54/81.60 [27]P1(a10) % 81.54/81.60 [28]P1(a11) % 81.54/81.60 [29]P1(a12) % 81.54/81.60 [30]P1(a13) % 81.54/81.60 [31]P2(a13) % 81.54/81.60 [33]~E(a1,a10) % 81.54/81.60 [34]~E(a1,a11) % 81.54/81.60 [35]~E(a1,a12) % 81.54/81.60 [36]~E(a1,a13) % 81.54/81.60 [32]E(f2(a13,f2(a12,a12)),f2(a11,a11)) % 81.54/81.60 [76]~P3(a13,a11)+~P3(a13,f2(a11,a11)) % 81.54/81.60 [47]~P1(x471)+P5(x471,x471) % 81.54/81.60 [39]~P1(x391)+E(f2(a1,x391),a1) % 81.54/81.60 [40]~P1(x401)+E(f2(x401,a1),a1) % 81.54/81.60 [41]~P1(x411)+E(f7(a1,x411),x411) % 81.54/81.60 [42]~P1(x421)+E(f2(a10,x421),x421) % 81.54/81.60 [43]~P1(x431)+E(f7(x431,a1),x431) % 81.54/81.60 [44]~P1(x441)+E(f2(x441,a10),x441) % 81.54/81.60 [37]~P1(x371)+~P2(x371)+~E(x371,a1) % 81.54/81.60 [38]~P1(x381)+~P2(x381)+~E(x381,a10) % 81.54/81.60 [58]~P1(x582)+~P1(x581)+E(f7(x581,x582),f7(x582,x581)) % 81.54/81.60 [59]~P1(x592)+~P1(x591)+E(f2(x591,x592),f2(x592,x591)) % 81.54/81.60 [61]~P1(x612)+~P1(x611)+P1(f7(x611,x612)) % 81.54/81.60 [62]~P1(x622)+~P1(x621)+P1(f2(x621,x622)) % 81.54/81.60 [49]~P1(x491)+E(x491,a10)+P5(a10,x491)+E(x491,a1) % 81.54/81.60 [45]~P1(x451)+E(x451,a10)+E(x451,a1)+P1(f3(x451)) % 81.54/81.60 [46]~P1(x461)+E(x461,a10)+E(x461,a1)+P2(f3(x461)) % 81.54/81.60 [52]~P1(x521)+E(x521,a10)+P3(f3(x521),x521)+E(x521,a1) % 81.54/81.60 [53]~E(x532,x531)+~P1(x531)+~P1(x532)+P5(x531,x532) % 81.54/81.60 [60]P5(x602,x601)+~P1(x601)+~P1(x602)+P5(x601,x602) % 81.54/81.60 [55]~P1(x552)+~P1(x551)+E(x551,a1)+~E(f7(x552,x551),a1) % 81.54/81.60 [56]~P1(x562)+~P1(x561)+E(x561,a1)+~E(f7(x561,x562),a1) % 81.54/81.60 [66]~P1(x662)+~P1(x661)+P5(x662,f2(x662,x661))+E(x661,a1) % 81.54/81.60 [72]~P1(x722)+~P1(x721)+~P5(x721,x722)+P1(f5(x721,x722)) % 81.54/81.60 [73]~P1(x732)+~P1(x731)+~P3(x731,x732)+P1(f6(x731,x732)) % 81.54/81.60 [81]~P1(x811)+~P1(x812)+~P3(x811,x812)+E(f2(x811,f6(x811,x812)),x812) % 81.54/81.60 [82]~P1(x822)+~P1(x821)+~P5(x821,x822)+E(f7(x821,f5(x821,x822)),x822) % 81.54/81.60 [91]~P1(x913)+~P1(x912)+~P1(x911)+E(f7(f7(x911,x912),x913),f7(x911,f7(x912,x913))) % 81.54/81.60 [92]~P1(x923)+~P1(x922)+~P1(x921)+E(f2(f2(x921,x922),x923),f2(x921,f2(x922,x923))) % 81.54/81.60 [101]~P1(x1013)+~P1(x1012)+~P1(x1011)+E(f7(f2(x1011,x1012),f2(x1011,x1013)),f2(x1011,f7(x1012,x1013))) % 81.54/81.60 [102]~P1(x1022)+~P1(x1023)+~P1(x1021)+E(f7(f2(x1021,x1022),f2(x1023,x1022)),f2(f7(x1021,x1023),x1022)) % 81.54/81.60 [48]P2(x481)+~P1(x481)+E(x481,a10)+E(x481,a1)+~E(f4(x481),a10) % 81.54/81.60 [50]P2(x501)+~P1(x501)+E(x501,a10)+~E(f4(x501),x501)+E(x501,a1) % 81.54/81.60 [51]P2(x511)+~P1(x511)+E(x511,a10)+E(x511,a1)+P1(f4(x511)) % 81.54/81.60 [54]P2(x541)+~P1(x541)+E(x541,a10)+P3(f4(x541),x541)+E(x541,a1) % 81.54/81.60 [64]~P1(x641)+~P1(x642)+~P3(x642,x641)+P5(x642,x641)+E(x641,a1) % 81.54/81.61 [65]P4(x651,x652)+~P1(x652)+~P1(x651)+~P5(x651,x652)+E(x651,x652) % 81.54/81.61 [69]~P1(x692)+~P1(x691)+~P5(x692,x691)+~P5(x691,x692)+E(x691,x692) % 81.54/81.61 [57]~P1(x571)+~P1(x572)+E(x571,a1)+E(x572,a1)+~E(f2(x572,x571),a1) % 81.54/81.61 [67]~P1(x671)+~P1(x672)+~P1(x673)+P3(x671,x672)+~E(x672,f2(x671,x673)) % 81.54/81.61 [68]~P1(x682)+~P1(x681)+~P1(x683)+P5(x681,x682)+~E(f7(x681,x683),x682) % 81.54/81.61 [70]~P1(x703)+~P1(x702)+~P5(x703,x702)+P1(x701)+~E(x701,f8(x702,x703)) % 81.54/81.61 [74]~P1(x742)+~P1(x741)+~P1(x743)+E(x741,x742)+~E(f7(x743,x741),f7(x743,x742)) % 81.54/81.61 [75]~P1(x752)+~P1(x753)+~P1(x751)+E(x751,x752)+~E(f7(x751,x753),f7(x752,x753)) % 81.54/81.61 [79]~P1(x793)+~P1(x791)+~P5(x791,x793)+~E(x792,f8(x793,x791))+E(f7(x791,x792),x793) % 81.54/81.61 [63]~P1(x632)+~P1(x631)+~P2(x632)+~P3(x631,x632)+E(x631,x632)+E(x631,a10) % 81.54/81.61 [83]~P1(x832)+~P1(x831)+~P5(x833,x832)+~P5(x831,x833)+P5(x831,x832)+~P1(x833) % 81.54/81.61 [84]~P1(x842)+~P1(x841)+~P3(x843,x842)+~P3(x841,x843)+P3(x841,x842)+~P1(x843) % 81.54/81.61 [71]~P1(x711)+~P1(x713)+~P3(x711,x713)+P1(x712)+E(x711,a1)+~E(x712,f9(x713,x711)) % 81.54/81.61 [77]~P1(x772)+~P1(x771)+~P1(x773)+E(x771,x772)+~E(f2(x773,x771),f2(x773,x772))+E(x773,a1) % 81.54/81.61 [78]~P1(x782)+~P1(x783)+~P1(x781)+E(x781,x782)+~E(f2(x781,x783),f2(x782,x783))+E(x783,a1) % 81.54/81.61 [80]~P1(x801)+~P1(x802)+~P3(x801,x802)+~E(x803,f9(x802,x801))+E(x801,a1)+E(x802,f2(x801,x803)) % 81.54/81.61 [85]~P1(x852)+~P1(x853)+~P1(x851)+~P5(x853,x852)+~E(f7(x853,x851),x852)+E(x851,f8(x852,x853)) % 81.54/81.61 [93]~P1(x933)+~P1(x932)+~P1(x931)+~P3(x931,x933)+~P3(x931,x932)+P3(x931,f7(x932,x933)) % 81.54/81.61 [94]~P1(x942)+~P1(x941)+~P1(x943)+~P5(x941,x942)+E(x941,x942)+P5(f7(x943,x941),f7(x943,x942)) % 81.54/81.61 [95]~P1(x952)+~P1(x953)+~P1(x951)+~P5(x951,x952)+E(x951,x952)+P5(f7(x951,x953),f7(x952,x953)) % 81.54/81.61 [99]~P1(x992)+~P1(x991)+~P3(x991,x993)+P3(x991,x992)+~P1(x993)+~P3(x991,f7(x993,x992)) % 81.54/81.61 [100]~P1(x1002)+~P1(x1003)+~P1(x1001)+~P3(x1001,x1003)+E(x1001,a1)+E(f9(f2(x1002,x1003),x1001),f2(x1002,f9(x1003,x1001))) % 81.54/81.61 [86]~P1(x861)+~P1(x863)+~P1(x862)+~P3(x861,x863)+~E(x863,f2(x861,x862))+E(x861,a1)+E(x862,f9(x863,x861)) % 81.54/81.61 [96]~P1(x962)+~P1(x961)+~P1(x963)+~P5(x961,x962)+E(x961,x962)+P5(f2(x963,x961),f2(x963,x962))+E(x963,a1) % 81.54/81.61 [97]~P1(x972)+~P1(x973)+~P1(x971)+~P5(x971,x972)+E(x971,x972)+P5(f2(x971,x973),f2(x972,x973))+E(x973,a1) % 81.54/81.61 [98]~P1(x981)+~P1(x982)+~P1(x983)+~P2(x981)+P3(x981,x982)+P3(x981,x983)+~P3(x981,f2(x983,x982)) % 81.54/81.61 [103]~P1(x1031)+~P1(x1032)+~P1(x1033)+~P2(x1031)+~P4(x1033,a11)+E(x1031,a1)+E(x1032,a1)+E(x1033,a1)+~E(f2(x1031,f2(x1032,x1032)),f2(x1033,x1033)) % 81.54/81.61 %EqnAxiom % 81.54/81.61 [1]E(x11,x11) % 81.54/81.61 [2]E(x22,x21)+~E(x21,x22) % 81.54/81.61 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 81.54/81.61 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 81.54/81.61 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 81.54/81.61 [6]~E(x61,x62)+E(f7(x61,x63),f7(x62,x63)) % 81.54/81.61 [7]~E(x71,x72)+E(f7(x73,x71),f7(x73,x72)) % 81.54/81.61 [8]~E(x81,x82)+E(f9(x81,x83),f9(x82,x83)) % 81.54/81.61 [9]~E(x91,x92)+E(f9(x93,x91),f9(x93,x92)) % 81.54/81.61 [10]~E(x101,x102)+E(f8(x101,x103),f8(x102,x103)) % 81.54/81.61 [11]~E(x111,x112)+E(f8(x113,x111),f8(x113,x112)) % 81.54/81.61 [12]~E(x121,x122)+E(f5(x121,x123),f5(x122,x123)) % 81.54/81.61 [13]~E(x131,x132)+E(f5(x133,x131),f5(x133,x132)) % 81.54/81.61 [14]~E(x141,x142)+E(f6(x141,x143),f6(x142,x143)) % 81.54/81.61 [15]~E(x151,x152)+E(f6(x153,x151),f6(x153,x152)) % 81.54/81.61 [16]~E(x161,x162)+E(f4(x161),f4(x162)) % 81.54/81.61 [17]~E(x171,x172)+E(f3(x171),f3(x172)) % 81.54/81.61 [18]~P1(x181)+P1(x182)+~E(x181,x182) % 81.54/81.61 [19]P4(x192,x193)+~E(x191,x192)+~P4(x191,x193) % 81.54/81.61 [20]P4(x203,x202)+~E(x201,x202)+~P4(x203,x201) % 81.54/81.61 [21]~P2(x211)+P2(x212)+~E(x211,x212) % 81.54/81.61 [22]P3(x222,x223)+~E(x221,x222)+~P3(x221,x223) % 81.54/81.61 [23]P3(x233,x232)+~E(x231,x232)+~P3(x233,x231) % 81.54/81.61 [24]P5(x242,x243)+~E(x241,x242)+~P5(x241,x243) % 81.54/81.61 [25]P5(x253,x252)+~E(x251,x252)+~P5(x253,x251) % 81.54/81.61 % 81.54/81.61 %------------------------------------------- % 81.62/81.62 cnf(104,plain, % 81.62/81.62 (~P2(a1)+~P1(a1)), % 81.62/81.62 inference(equality_inference,[],[37])). % 81.62/81.62 cnf(105,plain, % 81.62/81.62 (~P2(a10)+~P1(a10)), % 81.62/81.62 inference(equality_inference,[],[38])). % 81.62/81.62 cnf(107,plain, % 81.62/81.62 (P3(x1071,f2(x1071,x1072))+~P1(x1071)+~P1(f2(x1071,x1072))+~P1(x1072)), % 81.62/81.62 inference(equality_inference,[],[67])). % 81.62/81.62 cnf(108,plain, % 81.62/81.62 (P5(x1081,f7(x1081,x1082))+~P1(f7(x1081,x1082))+~P1(x1081)+~P1(x1082)), % 81.62/81.62 inference(equality_inference,[],[68])). % 81.62/81.62 cnf(109,plain, % 81.62/81.62 (~P5(x1091,x1092)+~P1(x1091)+~P1(x1092)+P1(f8(x1092,x1091))), % 81.62/81.62 inference(equality_inference,[],[70])). % 81.62/81.62 cnf(110,plain, % 81.62/81.62 (~P3(x1101,x1102)+~P1(x1101)+~P1(x1102)+P1(f9(x1102,x1101))+E(x1101,a1)), % 81.62/81.62 inference(equality_inference,[],[71])). % 81.62/81.62 cnf(115,plain, % 81.62/81.62 (~P5(x1151,x1152)+~P1(x1152)+~P1(x1151)+E(f7(x1151,f8(x1152,x1151)),x1152)), % 81.62/81.62 inference(equality_inference,[],[79])). % 81.62/81.62 cnf(116,plain, % 81.62/81.62 (~P3(x1161,x1162)+~P1(x1161)+~P1(x1162)+E(x1161,a1)+E(x1162,f2(x1161,f9(x1162,x1161)))), % 81.62/81.62 inference(equality_inference,[],[80])). % 81.62/81.62 cnf(117,plain, % 81.62/81.62 (~P5(x1171,f7(x1171,x1172))+~P1(f7(x1171,x1172))+~P1(x1171)+~P1(x1172)+E(x1172,f8(f7(x1171,x1172),x1171))), % 81.62/81.62 inference(equality_inference,[],[85])). % 81.62/81.62 cnf(120,plain, % 81.62/81.62 (~P2(a1)), % 81.62/81.62 inference(scs_inference,[],[26,104])). % 81.62/81.62 cnf(121,plain, % 81.62/81.62 (~P2(a10)), % 81.62/81.62 inference(scs_inference,[],[27,105])). % 81.62/81.62 cnf(122,plain, % 81.62/81.62 (E(f2(a11,a11),f2(a13,f2(a12,a12)))), % 81.62/81.62 inference(scs_inference,[],[32,2])). % 81.62/81.62 cnf(123,plain, % 81.62/81.62 (P5(a1,a1)), % 81.62/81.62 inference(scs_inference,[],[26,32,2,60])). % 81.62/81.62 cnf(125,plain, % 81.62/81.62 (E(f7(a1,f8(a1,a1)),a1)), % 81.62/81.62 inference(scs_inference,[],[26,32,2,60,115])). % 81.62/81.62 cnf(127,plain, % 81.62/81.62 (~P3(a1,a13)), % 81.62/81.62 inference(scs_inference,[],[26,30,31,33,36,32,2,60,115,63])). % 81.62/81.62 cnf(130,plain, % 81.62/81.62 (P1(f8(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[26,30,31,33,36,32,2,60,115,63,18,109])). % 81.62/81.62 cnf(132,plain, % 81.62/81.62 (E(f8(a1,a1),a1)), % 81.62/81.62 inference(scs_inference,[],[26,30,31,33,36,32,2,60,115,63,18,109,55])). % 81.62/81.62 cnf(134,plain, % 81.62/81.62 (~P1(f2(a12,a12))+P1(f2(a11,a11))), % 81.62/81.62 inference(scs_inference,[],[26,30,31,33,36,32,2,60,115,63,18,109,55,62])). % 81.62/81.62 cnf(137,plain, % 81.62/81.62 (E(a1,f7(a1,f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[125,2])). % 81.62/81.62 cnf(138,plain, % 81.62/81.62 (~P2(f8(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[130,125,132,2,37])). % 81.62/81.62 cnf(140,plain, % 81.62/81.62 (P5(f7(a1,f8(a1,a1)),a1)), % 81.62/81.62 inference(scs_inference,[],[130,123,125,132,2,37,24])). % 81.62/81.62 cnf(141,plain, % 81.62/81.62 (P5(a1,f7(a1,f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[130,123,125,132,2,37,24,25])). % 81.62/81.62 cnf(142,plain, % 81.62/81.62 (~P2(f7(a1,f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[130,123,125,132,120,2,37,24,25,21])). % 81.62/81.62 cnf(143,plain, % 81.62/81.62 (P1(f7(a1,f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[26,130,123,125,132,120,2,37,24,25,21,18])). % 81.62/81.62 cnf(144,plain, % 81.62/81.62 (P5(f8(a1,a1),f8(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[26,130,123,125,132,120,2,37,24,25,21,18,60])). % 81.62/81.62 cnf(146,plain, % 81.62/81.62 (E(x1461,a1)+~E(x1461,f8(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[26,130,123,125,132,120,2,37,24,25,21,18,60,3])). % 81.62/81.62 cnf(147,plain, % 81.62/81.62 (P1(f8(f8(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[26,130,123,125,132,120,2,37,24,25,21,18,60,3,109])). % 81.62/81.62 cnf(149,plain, % 81.62/81.62 (E(f7(f8(a1,a1),f8(f8(a1,a1),f8(a1,a1))),f8(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[26,130,123,125,132,120,2,37,24,25,21,18,60,3,109,115])). % 81.62/81.62 cnf(151,plain, % 81.62/81.62 (P1(f7(f8(a1,a1),f8(f8(a1,a1),f8(a1,a1))))), % 81.62/81.62 inference(scs_inference,[],[26,130,123,125,132,120,2,37,24,25,21,18,60,3,109,115,70])). % 81.62/81.62 cnf(158,plain, % 81.62/81.62 (E(f8(a1,a1),f7(f8(a1,a1),f8(f8(a1,a1),f8(a1,a1))))), % 81.62/81.62 inference(scs_inference,[],[149,2])). % 81.62/81.62 cnf(160,plain, % 81.62/81.62 (P5(f8(a1,a1),a1)), % 81.62/81.62 inference(scs_inference,[],[149,144,138,132,2,21,25])). % 81.62/81.62 cnf(161,plain, % 81.62/81.62 (E(f7(f8(a1,a1),f8(f8(a1,a1),f8(a1,a1))),a1)), % 81.62/81.62 inference(scs_inference,[],[149,144,138,132,2,21,25,3])). % 81.62/81.62 cnf(162,plain, % 81.62/81.62 (P5(a1,f8(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[149,144,138,132,2,21,25,3,24])). % 81.62/81.62 cnf(163,plain, % 81.62/81.62 (E(f8(f8(a1,a1),f8(a1,a1)),a1)), % 81.62/81.62 inference(scs_inference,[],[147,130,149,144,138,132,2,21,25,3,24,55])). % 81.62/81.62 cnf(165,plain, % 81.62/81.62 (P5(f8(f8(a1,a1),f8(a1,a1)),f8(f8(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[147,130,149,144,138,132,2,21,25,3,24,55,60])). % 81.62/81.62 cnf(167,plain, % 81.62/81.62 (E(a1,f8(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[26,147,130,149,144,138,132,2,21,25,3,24,55,60,69])). % 81.62/81.62 cnf(169,plain, % 81.62/81.62 (E(f8(f8(a1,a1),f8(a1,a1)),f8(a1,f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[26,147,130,149,144,138,132,2,21,25,3,24,55,60,69,85])). % 81.62/81.62 cnf(172,plain, % 81.62/81.62 (~P2(f8(f8(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[26,147,130,149,144,138,122,132,2,21,25,3,24,55,60,69,85,18,37])). % 81.62/81.62 cnf(175,plain, % 81.62/81.62 (E(f8(a1,f8(a1,a1)),f8(f8(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[169,2])). % 81.62/81.62 cnf(176,plain, % 81.62/81.62 (P1(f8(a1,f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[147,169,2,18])). % 81.62/81.62 cnf(177,plain, % 81.62/81.62 (P5(f7(a1,f8(a1,a1)),f7(a1,f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[147,141,137,169,2,18,24])). % 81.62/81.62 cnf(178,plain, % 81.62/81.62 (E(f7(a1,f8(a1,a1)),f8(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[147,125,141,137,169,167,2,18,24,3])). % 81.62/81.62 cnf(180,plain, % 81.62/81.62 (P5(f8(f8(a1,a1),f8(a1,a1)),f8(a1,f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[147,125,141,165,172,137,169,167,2,18,24,3,21,25])). % 81.62/81.62 cnf(181,plain, % 81.62/81.62 (P5(a10,a10)), % 81.62/81.62 inference(scs_inference,[],[27,147,125,141,165,172,137,169,167,2,18,24,3,21,25,60])). % 81.62/81.62 cnf(183,plain, % 81.62/81.62 (E(f8(a1,a1),f8(f8(a1,a1),a1))), % 81.62/81.62 inference(scs_inference,[],[26,130,27,147,125,141,165,172,137,169,167,162,2,18,24,3,21,25,60,85])). % 81.62/81.62 cnf(185,plain, % 81.62/81.62 (P1(f8(a10,a10))), % 81.62/81.62 inference(scs_inference,[],[26,130,27,147,125,141,165,172,137,169,167,162,2,18,24,3,21,25,60,85,109])). % 81.62/81.62 cnf(189,plain, % 81.62/81.62 (E(f7(a10,f8(a10,a10)),a10)), % 81.62/81.62 inference(scs_inference,[],[26,130,27,147,125,141,165,172,137,169,167,162,2,18,24,3,21,25,60,85,109,108,115])). % 81.62/81.62 cnf(193,plain, % 81.62/81.62 (P5(a12,a12)), % 81.62/81.62 inference(scs_inference,[],[26,130,27,29,147,125,141,165,172,137,169,167,162,2,18,24,3,21,25,60,85,109,108,115,38,53])). % 81.62/81.62 cnf(200,plain, % 81.62/81.62 (P1(f8(f8(a1,a1),a1))), % 81.62/81.62 inference(scs_inference,[],[130,161,140,167,183,2,25,18])). % 81.62/81.62 cnf(202,plain, % 81.62/81.62 (E(f8(a1,f8(a1,a1)),a1)), % 81.62/81.62 inference(scs_inference,[],[130,161,140,163,167,175,183,189,121,2,25,18,21,3])). % 81.62/81.62 cnf(204,plain, % 81.62/81.62 (P1(f8(a12,a12))), % 81.62/81.62 inference(scs_inference,[],[130,29,161,140,141,163,167,175,183,189,121,193,2,25,18,21,3,24,109])). % 81.62/81.62 cnf(206,plain, % 81.62/81.62 (E(f7(a12,f8(a12,a12)),a12)), % 81.62/81.62 inference(scs_inference,[],[130,29,161,140,141,163,167,175,183,189,121,193,2,25,18,21,3,24,109,115])). % 81.62/81.62 cnf(208,plain, % 81.62/81.62 (P5(f8(a1,f8(a1,a1)),f8(a1,f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[130,176,29,161,140,141,163,167,175,183,189,121,193,2,25,18,21,3,24,109,115,60])). % 81.62/81.62 cnf(210,plain, % 81.62/81.62 (E(f8(a1,a1),f7(a1,f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[130,143,176,29,161,140,141,163,167,175,183,189,121,193,2,25,18,21,3,24,109,115,60,69])). % 81.62/81.62 cnf(214,plain, % 81.62/81.62 (P5(f8(a10,a10),f8(a10,a10))), % 81.62/81.62 inference(scs_inference,[],[130,143,176,185,29,161,140,141,163,167,175,183,189,121,193,2,25,18,21,3,24,109,115,60,69,108,53])). % 81.62/81.62 cnf(220,plain, % 81.62/81.62 (E(a10,f7(a10,f8(a10,a10)))), % 81.62/81.62 inference(scs_inference,[],[189,2])). % 81.62/81.62 cnf(222,plain, % 81.62/81.62 (~E(a1,f7(a10,f8(a10,a10)))), % 81.62/81.62 inference(scs_inference,[],[189,33,181,2,24,3])). % 81.62/81.62 cnf(223,plain, % 81.62/81.62 (P5(a10,f7(a10,f8(a10,a10)))), % 81.62/81.62 inference(scs_inference,[],[189,33,181,2,24,3,25])). % 81.62/81.62 cnf(224,plain, % 81.62/81.62 (P1(f7(a10,f8(a10,a10)))), % 81.62/81.62 inference(scs_inference,[],[27,189,33,181,2,24,3,25,18])). % 81.62/81.62 cnf(225,plain, % 81.62/81.62 (P1(f8(f8(a10,a10),f8(a10,a10)))), % 81.62/81.62 inference(scs_inference,[],[27,185,189,33,181,214,2,24,3,25,18,109])). % 81.62/81.62 cnf(227,plain, % 81.62/81.62 (E(f7(f8(a10,a10),f8(f8(a10,a10),f8(a10,a10))),f8(a10,a10))), % 81.62/81.62 inference(scs_inference,[],[27,185,189,33,181,214,2,24,3,25,18,109,115])). % 81.62/81.62 cnf(229,plain, % 81.62/81.62 (P5(f8(f8(a1,a1),a1),f8(f8(a1,a1),a1))), % 81.62/81.62 inference(scs_inference,[],[27,200,185,189,33,181,214,2,24,3,25,18,109,115,60])). % 81.62/81.62 cnf(234,plain, % 81.62/81.62 (P5(f8(a12,a12),f8(a12,a12))), % 81.62/81.62 inference(scs_inference,[],[27,200,204,185,189,33,181,214,206,2,24,3,25,18,109,115,60,70,21,53])). % 81.62/81.62 cnf(241,plain, % 81.62/81.62 (E(a1,f8(f8(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[163,2])). % 81.62/81.62 cnf(242,plain, % 81.62/81.62 (P5(a1,f8(a1,f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[163,180,2,24])). % 81.62/81.62 cnf(243,plain, % 81.62/81.62 (P5(f8(a1,f8(a1,a1)),f8(f8(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[163,175,208,180,2,24,25])). % 81.62/81.62 cnf(244,plain, % 81.62/81.62 (~E(a1,f7(a12,f8(a12,a12)))), % 81.62/81.62 inference(scs_inference,[],[163,175,206,208,180,35,2,24,25,3])). % 81.62/81.62 cnf(245,plain, % 81.62/81.62 (P1(f8(f8(a12,a12),f8(a12,a12)))), % 81.62/81.62 inference(scs_inference,[],[204,163,175,206,208,180,234,35,2,24,25,3,109])). % 81.62/81.62 cnf(247,plain, % 81.62/81.62 (E(f7(f8(a12,a12),f8(f8(a12,a12),f8(a12,a12))),f8(a12,a12))), % 81.62/81.62 inference(scs_inference,[],[204,163,175,206,208,180,234,35,2,24,25,3,109,115])). % 81.62/81.62 cnf(260,plain, % 81.62/81.62 (P3(a13,f2(a11,a11))+~P1(f2(a11,a11))+~P1(f2(a12,a12))), % 81.62/81.62 inference(scs_inference,[],[225,224,204,29,30,163,175,206,227,208,180,234,35,193,122,2,24,25,3,109,115,60,70,67])). % 81.62/81.62 cnf(261,plain, % 81.62/81.62 (E(a12,f7(a12,f8(a12,a12)))), % 81.62/81.62 inference(scs_inference,[],[206,2])). % 81.62/81.62 cnf(262,plain, % 81.62/81.62 (P1(f7(a12,f8(a12,a12)))), % 81.62/81.62 inference(scs_inference,[],[29,206,2,18])). % 81.62/81.62 cnf(263,plain, % 81.62/81.62 (P5(a1,f8(f8(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[29,206,202,243,2,18,24])). % 81.62/81.62 cnf(264,plain, % 81.62/81.62 (P5(f8(f8(a1,a1),f8(a1,a1)),a1)), % 81.62/81.62 inference(scs_inference,[],[29,206,202,180,243,2,18,24,25])). % 81.62/81.62 cnf(265,plain, % 81.62/81.62 (P5(f8(f8(a12,a12),f8(a12,a12)),f8(f8(a12,a12),f8(a12,a12)))), % 81.62/81.62 inference(scs_inference,[],[245,29,206,202,180,243,2,18,24,25,60])). % 81.62/81.62 cnf(267,plain, % 81.62/81.62 (P5(f8(a1,f8(a1,a1)),a1)), % 81.62/81.62 inference(scs_inference,[],[26,176,245,29,147,206,202,180,243,2,18,24,25,60,83])). % 81.62/81.62 cnf(270,plain, % 81.62/81.62 (E(a1,f8(a1,f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[26,176,245,29,147,206,202,32,180,243,242,2,18,24,25,60,83,21,69])). % 81.62/81.62 cnf(273,plain, % 81.62/81.62 (P1(f8(a11,a11))+~P5(a11,a11)), % 81.62/81.62 inference(scs_inference,[],[26,176,245,28,29,147,206,202,227,32,180,243,242,2,18,24,25,60,83,21,69,3,109])). % 81.62/81.62 cnf(275,plain, % 81.62/81.62 (P5(a11,a11)), % 81.62/81.62 inference(scs_inference,[],[26,176,245,28,29,147,206,202,227,32,180,243,242,2,18,24,25,60,83,21,69,3,109,53])). % 81.62/81.62 cnf(279,plain, % 81.62/81.62 (P1(f8(a11,a11))), % 81.62/81.62 inference(scs_inference,[],[275,273])). % 81.62/81.62 cnf(280,plain, % 81.62/81.62 (E(f8(f8(a1,a1),a1),f8(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[183,275,273,2])). % 81.62/81.62 cnf(283,plain, % 81.62/81.62 (P5(f8(a1,a1),f8(a1,f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[183,167,242,229,275,138,273,2,25,21,24])). % 81.62/81.62 cnf(284,plain, % 81.62/81.62 (E(f7(a11,f8(a11,a11)),a11)), % 81.62/81.62 inference(scs_inference,[],[28,183,167,242,229,275,138,273,2,25,21,24,115])). % 81.62/81.62 cnf(286,plain, % 81.62/81.62 (P5(f7(a12,f8(a12,a12)),f7(a12,f8(a12,a12)))), % 81.62/81.62 inference(scs_inference,[],[262,28,183,167,242,229,275,138,273,2,25,21,24,115,60])). % 81.62/81.62 cnf(288,plain, % 81.62/81.62 (P5(f8(f8(a1,a1),a1),a1)), % 81.62/81.62 inference(scs_inference,[],[26,130,200,262,28,160,183,167,242,229,275,138,273,2,25,21,24,115,60,83])). % 81.62/81.62 cnf(302,plain, % 81.62/81.62 (E(f8(a10,a10),f7(f8(a10,a10),f8(f8(a10,a10),f8(a10,a10))))), % 81.62/81.62 inference(scs_inference,[],[227,2])). % 81.62/81.62 cnf(303,plain, % 81.62/81.62 (P5(f8(a1,a1),f8(f8(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[227,167,263,2,24])). % 81.62/81.62 cnf(304,plain, % 81.62/81.62 (E(f7(a1,f8(a1,a1)),f8(f8(a1,a1),a1))), % 81.62/81.62 inference(scs_inference,[],[178,227,183,167,263,2,24,3])). % 81.62/81.62 cnf(305,plain, % 81.62/81.62 (P5(f8(f8(a1,a1),f8(a1,a1)),f8(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[178,227,183,167,264,263,2,24,3,25])). % 81.62/81.62 cnf(306,plain, % 81.62/81.62 (P5(f8(a11,a11),f8(a11,a11))), % 81.62/81.62 inference(scs_inference,[],[279,178,227,183,167,264,263,2,24,3,25,60])). % 81.62/81.62 cnf(308,plain, % 81.62/81.62 (P5(a1,f8(f8(a1,a1),a1))), % 81.62/81.62 inference(scs_inference,[],[26,130,200,279,178,227,183,167,264,263,2,24,3,25,60,68])). % 81.62/81.62 cnf(316,plain, % 81.62/81.62 (E(f7(f8(a11,a11),f8(f8(a11,a11),f8(a11,a11))),f8(a11,a11))), % 81.62/81.62 inference(scs_inference,[],[26,130,200,279,178,227,183,167,247,264,263,288,2,24,3,25,60,68,69,85,18,21,115])). % 81.62/81.62 cnf(318,plain, % 81.62/81.62 (P1(f8(f8(a11,a11),f8(a11,a11)))), % 81.62/81.62 inference(scs_inference,[],[26,130,200,279,178,227,183,167,247,264,263,288,2,24,3,25,60,68,69,85,18,21,115,109])). % 81.62/81.62 cnf(322,plain, % 81.62/81.62 (P5(a13,a13)), % 81.62/81.62 inference(scs_inference,[],[26,130,200,28,279,30,178,227,183,167,247,264,263,288,275,2,24,3,25,60,68,69,85,18,21,115,109,70,53])). % 81.62/81.62 cnf(324,plain, % 81.62/81.62 (P5(f8(a10,a10),f7(f8(a10,a10),f8(a10,a10)))+~P1(f7(f8(a10,a10),f8(a10,a10)))), % 81.62/81.62 inference(scs_inference,[],[26,130,185,200,28,279,30,178,227,183,167,247,264,263,288,275,2,24,3,25,60,68,69,85,18,21,115,109,70,53,108])). % 81.62/81.62 cnf(330,plain, % 81.62/81.62 (E(f8(a10,a10),f8(f7(f8(a10,a10),f8(a10,a10)),f8(a10,a10)))+~P1(f7(f8(a10,a10),f8(a10,a10)))), % 81.62/81.62 inference(scs_inference,[],[26,130,185,200,28,279,30,178,227,183,167,247,32,264,263,288,275,2,24,3,25,60,68,69,85,18,21,115,109,70,53,108,107,67,117])). % 81.62/81.62 cnf(334,plain, % 81.62/81.62 (P5(f8(a1,f8(a1,a1)),f8(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[167,247,267,280,229,2,24,25])). % 81.62/81.62 cnf(335,plain, % 81.62/81.62 (~E(a1,f7(a11,f8(a11,a11)))), % 81.62/81.62 inference(scs_inference,[],[167,247,267,280,284,229,34,2,24,25,3])). % 81.62/81.62 cnf(336,plain, % 81.62/81.62 (E(f7(a13,f8(a13,a13)),a13)), % 81.62/81.62 inference(scs_inference,[],[30,167,247,267,280,284,229,34,322,2,24,25,3,115])). % 81.62/81.62 cnf(338,plain, % 81.62/81.62 (P1(f8(a13,a13))), % 81.62/81.62 inference(scs_inference,[],[30,167,247,267,280,284,229,34,322,2,24,25,3,115,109])). % 81.62/81.62 cnf(342,plain, % 81.62/81.62 (E(f8(a1,f8(a1,a1)),f8(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[130,176,318,30,167,247,267,283,280,284,229,34,322,2,24,25,3,115,109,60,69])). % 81.62/81.62 cnf(345,plain, % 81.62/81.62 (P5(f8(a13,a13),f8(a13,a13))), % 81.62/81.62 inference(scs_inference,[],[130,176,318,30,167,247,122,267,283,280,284,229,34,322,2,24,25,3,115,109,60,69,21,53])). % 81.62/81.62 cnf(347,plain, % 81.62/81.62 (P5(a12,f7(a12,a12))+~P1(f7(a12,a12))), % 81.62/81.62 inference(scs_inference,[],[130,29,176,318,30,167,247,122,267,283,280,284,229,34,322,2,24,25,3,115,109,60,69,21,53,108])). % 81.62/81.62 cnf(355,plain, % 81.62/81.62 (P5(a12,f7(a12,f8(a12,a12)))), % 81.62/81.62 inference(scs_inference,[],[206,169,304,342,286,2,3,25,24])). % 81.62/81.62 cnf(356,plain, % 81.62/81.62 (E(f7(f8(a13,a13),f8(f8(a13,a13),f8(a13,a13))),f8(a13,a13))), % 81.62/81.62 inference(scs_inference,[],[338,206,169,304,342,286,345,2,3,25,24,115])). % 81.62/81.62 cnf(364,plain, % 81.62/81.62 (E(f8(a1,a1),f8(f8(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[130,147,30,338,206,169,304,303,305,342,286,345,322,2,3,25,24,115,109,60,70,69])). % 81.62/81.62 cnf(374,plain, % 81.62/81.62 (P1(f7(a11,f8(a11,a11)))), % 81.62/81.62 inference(scs_inference,[],[28,284,2,18])). % 81.62/81.62 cnf(376,plain, % 81.62/81.62 (~E(a1,f7(a13,f8(a13,a13)))), % 81.62/81.62 inference(scs_inference,[],[28,284,336,302,36,214,2,18,24,3])). % 81.62/81.62 cnf(378,plain, % 81.62/81.62 (P5(f7(a11,f8(a11,a11)),f7(a11,f8(a11,a11)))), % 81.62/81.62 inference(scs_inference,[],[28,284,336,302,36,214,2,18,24,3,25,60])). % 81.62/81.62 cnf(383,plain, % 81.62/81.62 (P5(f8(a11,a11),f7(f8(a11,a11),f8(a11,a11)))+~P1(f7(f8(a11,a11),f8(a11,a11)))), % 81.62/81.62 inference(scs_inference,[],[26,200,28,279,284,316,336,288,302,308,36,214,2,18,24,3,25,60,69,21,108])). % 81.62/81.62 cnf(385,plain, % 81.62/81.62 (P3(f8(a11,a11),f2(f8(a11,a11),f8(a11,a11)))+~P1(f2(f8(a11,a11),f8(a11,a11)))), % 81.62/81.62 inference(scs_inference,[],[26,200,28,279,284,316,336,288,302,308,36,214,2,18,24,3,25,60,69,21,108,107])). % 81.62/81.62 cnf(387,plain, % 81.62/81.62 (E(f8(a11,a11),f8(f7(f8(a11,a11),f8(a11,a11)),f8(a11,a11)))+~P1(f7(f8(a11,a11),f8(a11,a11)))), % 81.62/81.62 inference(scs_inference,[],[26,200,28,279,30,284,122,316,336,288,302,308,36,214,2,18,24,3,25,60,69,21,108,107,67,117])). % 81.62/81.62 cnf(389,plain, % 81.62/81.62 (P1(f5(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[26,47,72])). % 81.62/81.62 cnf(392,plain, % 81.62/81.62 (E(f7(a1,f8(a1,a1)),f8(f8(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[178,316,364,306,2,25,3])). % 81.62/81.62 cnf(394,plain, % 81.62/81.62 (P5(f5(a1,a1),f5(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[389,178,316,364,306,2,25,3,24,60])). % 81.62/81.62 cnf(396,plain, % 81.62/81.62 (E(f8(a1,a1),f8(a1,f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[130,176,389,178,316,283,364,334,306,2,25,3,24,60,69])). % 81.62/81.62 cnf(398,plain, % 81.62/81.62 (E(f8(a1,a1),f8(f8(f8(a1,a1),f8(a1,a1)),a1))), % 81.62/81.62 inference(scs_inference,[],[26,130,176,147,389,178,316,263,283,364,334,306,2,25,3,24,60,69,85])). % 81.62/81.62 cnf(404,plain, % 81.62/81.62 (E(f7(f5(a1,a1),f8(f5(a1,a1),f5(a1,a1))),f5(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[26,130,176,147,389,178,316,263,356,283,364,334,306,2,25,3,24,60,69,85,18,21,109,115])). % 81.62/81.62 cnf(413,plain, % 81.62/81.62 (E(a13,f7(a13,f8(a13,a13)))), % 81.62/81.62 inference(scs_inference,[],[336,2])). % 81.62/81.62 cnf(414,plain, % 81.62/81.62 (P1(f7(a13,f8(a13,a13)))), % 81.62/81.62 inference(scs_inference,[],[30,336,2,18])). % 81.62/81.62 cnf(415,plain, % 81.62/81.62 (P2(f7(a13,f8(a13,a13)))), % 81.62/81.62 inference(scs_inference,[],[30,336,31,2,18,21])). % 81.62/81.62 cnf(416,plain, % 81.62/81.62 (P5(f7(a11,f8(a11,a11)),a11)), % 81.62/81.62 inference(scs_inference,[],[30,284,336,378,31,2,18,21,25])). % 81.62/81.62 cnf(417,plain, % 81.62/81.62 (P5(a11,f7(a11,f8(a11,a11)))), % 81.62/81.62 inference(scs_inference,[],[30,284,336,378,31,2,18,21,25,24])). % 81.62/81.62 cnf(418,plain, % 81.62/81.62 (E(f7(a1,f8(a1,a1)),f8(a1,f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[30,178,284,336,396,378,31,2,18,21,25,24,3])). % 81.62/81.62 cnf(419,plain, % 81.62/81.62 (P5(f7(a13,f8(a13,a13)),f7(a13,f8(a13,a13)))), % 81.62/81.62 inference(scs_inference,[],[30,178,284,336,396,378,31,2,18,21,25,24,3,60])). % 81.62/81.62 cnf(421,plain, % 81.62/81.62 (E(f8(a1,a1),f8(f8(a1,f8(a1,a1)),a1))), % 81.62/81.62 inference(scs_inference,[],[26,130,30,176,178,284,336,242,396,378,31,2,18,21,25,24,3,60,85])). % 81.62/81.62 cnf(426,plain, % 81.62/81.62 (E(f8(a13,a13),f7(f8(a13,a13),f8(f8(a13,a13),f8(a13,a13))))), % 81.62/81.62 inference(scs_inference,[],[356,2])). % 81.62/81.62 cnf(428,plain, % 81.62/81.62 (P5(a13,f7(a13,f8(a13,a13)))), % 81.62/81.62 inference(scs_inference,[],[130,336,356,419,421,2,18,24])). % 81.62/81.62 cnf(430,plain, % 81.62/81.62 (~P3(a1,f7(a13,f8(a13,a13)))), % 81.62/81.62 inference(scs_inference,[],[26,130,414,33,336,356,419,415,421,376,2,18,24,25,63])). % 81.62/81.62 cnf(448,plain, % 81.62/81.62 (E(f8(a1,f8(a1,a1)),f7(a1,f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[175,392,2,3])). % 81.62/81.62 cnf(454,plain, % 81.62/81.62 (P5(f8(a13,a13),f7(f8(a13,a13),f8(a13,a13)))+~P1(f7(f8(a13,a13),f8(a13,a13)))), % 81.62/81.62 inference(scs_inference,[],[338,389,175,392,404,426,345,2,3,24,25,21,107,108])). % 81.62/81.62 cnf(458,plain, % 81.62/81.62 (E(f5(a1,a1),f7(f5(a1,a1),f8(f5(a1,a1),f5(a1,a1))))), % 81.62/81.62 inference(scs_inference,[],[404,2])). % 81.62/81.62 cnf(470,plain, % 81.62/81.62 (P5(f5(a1,a1),f7(f5(a1,a1),f5(a1,a1)))+~P1(f7(f5(a1,a1),f5(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[389,398,394,458,138,2,21,24,25,108])). % 81.62/81.62 cnf(524,plain, % 81.62/81.62 (E(f2(a1,a1),a1)), % 81.62/81.62 inference(scs_inference,[],[161,151,39,18])). % 81.62/81.62 cnf(526,plain, % 81.62/81.62 (E(f7(f8(a1,a1),f8(f8(a1,a1),f8(a1,a1))),f2(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[161,524,2,3])). % 81.62/81.62 cnf(527,plain, % 81.62/81.62 (P1(f2(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[26,161,524,2,3,18])). % 81.62/81.62 cnf(528,plain, % 81.62/81.62 (~P2(f2(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[26,161,524,120,2,3,18,21])). % 81.62/81.62 cnf(529,plain, % 81.62/81.62 (P5(f2(a1,a1),f2(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[26,161,524,120,2,3,18,21,60])). % 81.62/81.62 cnf(531,plain, % 81.62/81.62 (P3(a1,f2(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[26,161,524,120,2,3,18,21,60,107])). % 81.62/81.62 cnf(533,plain, % 81.62/81.62 (P5(f8(a1,a1),f2(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[26,130,147,161,524,120,2,3,18,21,60,107,68])). % 81.62/81.62 cnf(535,plain, % 81.62/81.62 (P3(a1,a1)), % 81.62/81.62 inference(scs_inference,[],[26,130,147,161,524,120,2,3,18,21,60,107,68,67])). % 81.62/81.62 cnf(539,plain, % 81.62/81.62 (E(f8(f8(a1,a1),f8(a1,a1)),f8(f2(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[26,130,147,414,430,161,524,120,2,3,18,21,60,107,68,67,84,85])). % 81.62/81.62 cnf(541,plain, % 81.62/81.62 (~E(f2(a1,a1),f7(a13,f8(a13,a13)))), % 81.62/81.62 inference(scs_inference,[],[26,130,147,414,430,161,524,120,2,3,18,21,60,107,68,67,84,85,23])). % 81.62/81.62 cnf(542,plain, % 81.62/81.62 (P3(f8(a1,a1),f2(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[26,130,147,414,430,161,167,524,120,2,3,18,21,60,107,68,67,84,85,23,22])). % 81.62/81.62 cnf(544,plain, % 81.62/81.62 (P5(f2(a1,a1),a1)), % 81.62/81.62 inference(scs_inference,[],[26,130,147,414,430,161,167,524,120,265,2,3,18,21,60,107,68,67,84,85,23,22,24,25])). % 81.62/81.62 cnf(545,plain, % 81.62/81.62 (E(f7(f2(a1,a1),f8(f2(a1,a1),f2(a1,a1))),f2(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[26,130,147,414,430,161,167,524,120,265,2,3,18,21,60,107,68,67,84,85,23,22,24,25,115])). % 81.62/81.62 cnf(547,plain, % 81.62/81.62 (P1(f8(f2(a1,a1),f2(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[26,130,147,414,430,161,167,524,120,265,2,3,18,21,60,107,68,67,84,85,23,22,24,25,115,109])). % 81.62/81.62 cnf(549,plain, % 81.62/81.62 (P5(f8(f2(a1,a1),f2(a1,a1)),f8(f2(a1,a1),f2(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[26,130,147,414,430,161,167,524,120,265,2,3,18,21,60,107,68,67,84,85,23,22,24,25,115,109,53])). % 81.62/81.62 cnf(557,plain, % 81.62/81.62 (E(f8(f2(a1,a1),f8(a1,a1)),f8(f8(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[539,2])). % 81.62/81.62 cnf(559,plain, % 81.62/81.62 (P3(f8(a1,a1),a1)), % 81.62/81.62 inference(scs_inference,[],[542,183,524,539,2,22,23])). % 81.62/81.62 cnf(560,plain, % 81.62/81.62 (~E(f2(a1,a1),a13)), % 81.62/81.62 inference(scs_inference,[],[542,541,183,413,524,539,2,22,23,3])). % 81.62/81.62 cnf(561,plain, % 81.62/81.62 (P1(f8(f2(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[542,541,147,183,413,524,539,2,22,23,3,18])). % 81.62/81.62 cnf(563,plain, % 81.62/81.62 (P5(f2(a1,a1),f8(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[542,541,147,167,183,413,524,539,545,528,544,2,22,23,3,18,21,25])). % 81.62/81.62 cnf(565,plain, % 81.62/81.62 (P5(f8(f2(a1,a1),f8(a1,a1)),f8(f2(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[542,541,147,167,183,413,524,539,545,533,528,544,2,22,23,3,18,21,25,24,60])). % 81.62/81.62 cnf(569,plain, % 81.62/81.62 (P3(a1,f7(f8(a1,a1),f8(f8(a1,a1),f8(a1,a1))))), % 81.62/81.62 inference(scs_inference,[],[26,542,541,130,147,527,151,167,183,413,524,539,545,533,526,528,544,2,22,23,3,18,21,25,24,60,69,67])). % 81.62/81.62 cnf(581,plain, % 81.62/81.62 (P3(f8(a1,a1),f8(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[559,167,183,526,2,22,23])). % 81.62/81.62 cnf(582,plain, % 81.62/81.62 (E(f8(a1,a1),f2(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[559,167,183,158,526,2,22,23,3])). % 81.62/81.62 cnf(583,plain, % 81.62/81.62 (~P2(f8(f2(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[559,167,183,158,526,557,172,2,22,23,3,21])). % 81.62/81.62 cnf(584,plain, % 81.62/81.62 (P5(f8(f2(a1,a1),f8(a1,a1)),f8(f8(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[559,167,183,158,526,565,557,172,2,22,23,3,21,25])). % 81.62/81.62 cnf(585,plain, % 81.62/81.62 (P5(a1,f2(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[559,167,183,158,526,524,529,565,557,172,2,22,23,3,21,25,24])). % 81.62/81.62 cnf(588,plain, % 81.62/81.62 (P3(a1,f8(f8(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[26,559,569,130,147,167,183,158,526,524,529,565,557,172,2,22,23,3,21,25,24,67,99])). % 81.62/81.62 cnf(590,plain, % 81.62/81.62 (~P3(f8(a1,a1),f7(a13,f8(a13,a13)))), % 81.62/81.62 inference(scs_inference,[],[26,559,569,130,147,414,430,167,183,158,526,524,529,565,557,172,2,22,23,3,21,25,24,67,99,84])). % 81.62/81.62 cnf(592,plain, % 81.62/81.62 (P5(f8(f2(a1,a1),f8(a1,a1)),a1)), % 81.62/81.62 inference(scs_inference,[],[26,559,569,130,147,414,430,561,167,183,264,158,526,524,529,565,557,172,2,22,23,3,21,25,24,67,99,84,83])). % 81.62/81.62 cnf(599,plain, % 81.62/81.62 (P3(f8(f8(a1,a1),a1),f8(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[581,183,545,2,22])). % 81.62/81.62 cnf(600,plain, % 81.62/81.62 (~E(f8(a1,a1),f7(a13,f8(a13,a13)))), % 81.62/81.62 inference(scs_inference,[],[581,590,183,545,2,22,23])). % 81.62/81.62 cnf(601,plain, % 81.62/81.62 (P1(f7(f2(a1,a1),f8(f2(a1,a1),f2(a1,a1))))), % 81.62/81.62 inference(scs_inference,[],[581,590,527,183,545,2,22,23,18])). % 81.62/81.62 cnf(602,plain, % 81.62/81.62 (E(f7(a1,f8(a1,a1)),f8(f2(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[581,590,527,392,183,545,539,2,22,23,18,3])). % 81.62/81.62 cnf(603,plain, % 81.62/81.62 (P5(f8(f2(a1,a1),f8(a1,a1)),f8(a1,f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[581,590,527,392,183,169,545,539,584,2,22,23,18,3,25])). % 81.62/81.62 cnf(604,plain, % 81.62/81.62 (P5(f8(f8(a1,a1),f8(a1,a1)),f8(f2(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[581,590,527,392,183,169,545,539,557,584,565,2,22,23,18,3,25,24])). % 81.62/81.62 cnf(605,plain, % 81.62/81.62 (P5(a1,f8(f2(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[26,581,590,130,527,561,392,183,169,545,539,557,584,565,2,22,23,18,3,25,24,68])). % 81.62/81.62 cnf(607,plain, % 81.62/81.62 (E(a1,f8(f2(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[26,581,590,130,527,561,392,183,169,545,539,557,584,592,565,2,22,23,18,3,25,24,68,69])). % 81.62/81.62 cnf(609,plain, % 81.62/81.62 (P3(a1,f7(f2(a1,a1),f8(f2(a1,a1),f2(a1,a1))))), % 81.62/81.62 inference(scs_inference,[],[26,581,590,130,527,561,392,183,169,545,539,557,584,592,565,2,22,23,18,3,25,24,68,69,67])). % 81.62/81.62 cnf(613,plain, % 81.62/81.62 (P3(a1,f8(f2(a1,a1),f2(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[26,531,581,590,588,130,147,414,527,547,561,430,392,183,169,545,539,557,584,592,565,2,22,23,18,3,25,24,68,69,67,84,99])). % 81.62/81.62 cnf(615,plain, % 81.62/81.62 (E(f8(a1,a1),f8(f8(f2(a1,a1),f8(a1,a1)),a1))), % 81.62/81.62 inference(scs_inference,[],[26,531,581,590,588,130,147,414,527,547,561,430,392,183,169,545,539,557,584,592,565,2,22,23,18,3,25,24,68,69,67,84,99,85])). % 81.62/81.62 cnf(621,plain, % 81.62/81.62 (E(f8(f2(a1,a1),f8(a1,a1)),f7(a1,f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[602,2])). % 81.62/81.62 cnf(622,plain, % 81.62/81.62 (P3(f8(a1,a1),f8(f2(a1,a1),f2(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[613,167,602,2,22])). % 81.62/81.62 cnf(623,plain, % 81.62/81.62 (P3(f8(f8(a1,a1),a1),f8(f8(a1,a1),a1))), % 81.62/81.62 inference(scs_inference,[],[599,613,167,183,602,2,22,23])). % 81.62/81.62 cnf(624,plain, % 81.62/81.62 (~E(f8(a1,a1),a13)), % 81.62/81.62 inference(scs_inference,[],[600,599,613,167,183,413,602,2,22,23,3])). % 81.62/81.62 cnf(626,plain, % 81.62/81.62 (P5(f8(a1,f8(a1,a1)),f8(f2(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[600,599,613,130,167,183,169,413,602,604,615,2,22,23,3,18,24])). % 81.62/81.62 cnf(638,plain, % 81.62/81.62 (~E(f8(f2(a1,a1),f2(a1,a1)),f7(a13,f8(a13,a13)))), % 81.62/81.62 inference(scs_inference,[],[609,590,622,167,615,2,22,23])). % 81.62/81.62 cnf(639,plain, % 81.62/81.62 (E(f8(a1,a1),f8(f2(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[609,590,622,167,210,602,615,2,22,23,3])). % 81.62/81.62 cnf(641,plain, % 81.62/81.62 (P5(f8(f2(a1,a1),f8(a1,a1)),f8(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[609,590,622,167,210,602,615,592,138,2,22,23,3,21,25])). % 81.62/81.62 cnf(642,plain, % 81.62/81.62 (P5(f8(a1,a1),f8(f2(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[609,590,622,167,210,602,615,592,605,138,2,22,23,3,21,25,24])). % 81.62/81.62 cnf(643,plain, % 81.62/81.62 (E(f8(a1,f8(a1,a1)),f8(f2(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[609,590,622,176,561,167,210,602,615,592,603,605,626,138,2,22,23,3,21,25,24,69])). % 81.62/81.62 cnf(652,plain, % 81.62/81.62 (~E(f8(f8(a1,a1),f8(a1,a1)),f7(a13,f8(a13,a13)))), % 81.62/81.62 inference(scs_inference,[],[569,588,430,167,607,2,22,23])). % 81.62/81.62 cnf(654,plain, % 81.62/81.62 (P5(f8(f8(a1,a1),a1),f8(f2(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[569,638,588,430,167,183,413,607,642,2,22,23,3,24])). % 81.62/81.62 cnf(655,plain, % 81.62/81.62 (P5(f8(f2(a1,a1),f8(a1,a1)),f8(f8(a1,a1),a1))), % 81.62/81.62 inference(scs_inference,[],[569,638,588,430,167,183,413,607,641,642,2,22,23,3,24,25])). % 81.62/81.62 cnf(658,plain, % 81.62/81.62 (P3(f8(a1,a1),f8(f8(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[569,638,588,581,130,147,561,430,167,183,413,607,641,642,2,22,23,3,24,25,69,99])). % 81.62/81.62 cnf(662,plain, % 81.62/81.62 (P3(a13,a11)+~P1(f2(a11,a11))+~P1(f2(a12,a12))), % 81.62/81.62 inference(scs_inference,[],[26,569,638,588,581,130,28,30,147,414,561,430,167,183,122,428,413,607,641,642,31,2,22,23,3,24,25,69,99,67,98])). % 81.62/81.62 cnf(664,plain, % 81.62/81.62 (P3(f8(a1,a1),f8(f8(a1,a1),a1))), % 81.62/81.62 inference(scs_inference,[],[623,280,643,2,22])). % 81.62/81.62 cnf(671,plain, % 81.62/81.62 (P5(x6711,f8(f2(a1,a1),f2(a1,a1)))+~E(f8(f2(a1,a1),f2(a1,a1)),x6711)), % 81.62/81.62 inference(scs_inference,[],[590,623,652,130,200,414,561,280,413,643,549,654,655,2,22,23,3,69,84,24])). % 81.62/81.62 cnf(672,plain, % 81.62/81.62 (P5(f8(f2(a1,a1),f2(a1,a1)),x6721)+~E(f8(f2(a1,a1),f2(a1,a1)),x6721)), % 81.62/81.62 inference(scs_inference,[],[590,623,652,130,200,414,561,280,413,643,549,654,655,2,22,23,3,69,84,24,25])). % 81.62/81.62 cnf(694,plain, % 81.62/81.62 (E(f7(a1,f8(a1,a1)),f2(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[658,178,183,582,22,3])). % 81.62/81.62 cnf(695,plain, % 81.62/81.62 (P3(a1,f7(a1,f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[26,658,143,178,183,582,22,3,67])). % 81.62/81.62 cnf(699,plain, % 81.62/81.62 (E(f8(a1,a1),f8(f2(a1,a1),a1))), % 81.62/81.62 inference(scs_inference,[],[26,658,130,527,143,414,430,178,183,582,585,22,3,67,84,85])). % 81.62/81.62 cnf(702,plain, % 81.62/81.62 (~E(f7(a1,f8(a1,a1)),f7(a13,f8(a13,a13)))), % 81.62/81.62 inference(scs_inference,[],[26,658,130,527,143,414,430,178,183,582,585,22,3,67,84,85,2,23])). % 81.62/81.62 cnf(703,plain, % 81.62/81.62 (P1(f8(f2(a1,a1),a1))), % 81.62/81.62 inference(scs_inference,[],[26,658,130,527,143,414,430,178,183,582,585,22,3,67,84,85,2,23,18])). % 81.62/81.62 cnf(705,plain, % 81.62/81.62 (P5(f8(f2(a1,a1),a1),f8(f2(a1,a1),a1))), % 81.62/81.62 inference(scs_inference,[],[26,658,130,527,143,414,430,178,183,582,585,265,22,3,67,84,85,2,23,18,25,60])). % 81.62/81.62 cnf(710,plain, % 81.62/81.62 (P3(f8(a1,a1),f7(a1,f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[695,167,699,2,22])). % 81.62/81.62 cnf(712,plain, % 81.62/81.62 (~P2(f8(f2(a1,a1),a1))), % 81.62/81.62 inference(scs_inference,[],[702,695,167,413,699,138,2,22,3,21])). % 81.62/81.62 cnf(713,plain, % 81.62/81.62 (P5(f8(a1,a1),f8(f2(a1,a1),a1))), % 81.62/81.62 inference(scs_inference,[],[702,695,167,413,705,699,138,2,22,3,21,24])). % 81.62/81.62 cnf(714,plain, % 81.62/81.62 (P5(f8(f2(a1,a1),a1),f8(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[702,695,167,413,705,699,138,2,22,3,21,24,25])). % 81.62/81.62 cnf(715,plain, % 81.62/81.62 (P5(f8(f2(a1,a1),a1),a1)), % 81.62/81.62 inference(scs_inference,[],[26,702,695,130,703,167,160,413,705,699,138,2,22,3,21,24,25,83])). % 81.62/81.62 cnf(723,plain, % 81.62/81.62 (E(f8(a1,f8(a1,a1)),f2(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[710,183,448,694,22,3])). % 81.62/81.62 cnf(726,plain, % 81.62/81.62 (E(f8(f2(a1,a1),a1),f8(f8(a1,a1),a1))), % 81.62/81.62 inference(scs_inference,[],[710,200,703,183,448,694,714,713,22,3,24,25,69])). % 81.62/81.62 cnf(728,plain, % 81.62/81.62 (P3(a1,f8(a1,f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[26,710,176,200,703,183,448,694,714,713,22,3,24,25,69,67])). % 81.62/81.62 cnf(741,plain, % 81.62/81.62 (P3(f8(a1,a1),f8(a1,f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[728,167,726,2,22])). % 81.62/81.62 cnf(742,plain, % 81.62/81.62 (E(f7(a1,f8(a1,a1)),f8(f2(a1,a1),a1))), % 81.62/81.62 inference(scs_inference,[],[728,178,167,699,726,2,22,3])). % 81.62/81.62 cnf(743,plain, % 81.62/81.62 (P5(a1,f8(f2(a1,a1),a1))), % 81.62/81.62 inference(scs_inference,[],[26,728,130,703,178,167,699,726,2,22,3,68])). % 81.62/81.62 cnf(754,plain, % 81.62/81.62 (E(f8(f2(a1,a1),a1),f7(a1,f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[742,2])). % 81.62/81.62 cnf(770,plain, % 81.62/81.62 (E(f2(f7(a1,a1),a1),a1)), % 81.62/81.62 inference(scs_inference,[],[26,40,61])). % 81.62/81.62 cnf(771,plain, % 81.62/81.62 (E(a1,f2(f7(a1,a1),a1))), % 81.62/81.62 inference(scs_inference,[],[770,2])). % 81.62/81.62 cnf(772,plain, % 81.62/81.62 (P1(f2(f7(a1,a1),a1))), % 81.62/81.62 inference(scs_inference,[],[26,770,2,18])). % 81.62/81.62 cnf(774,plain, % 81.62/81.62 (P5(f2(f7(a1,a1),a1),f2(f7(a1,a1),a1))), % 81.62/81.62 inference(scs_inference,[],[26,770,120,2,18,21,60])). % 81.62/81.62 cnf(776,plain, % 81.62/81.62 (P5(a1,f2(f7(a1,a1),a1))), % 81.62/81.62 inference(scs_inference,[],[26,770,120,2,18,21,60,24])). % 81.62/81.62 cnf(777,plain, % 81.62/81.62 (P5(f2(f7(a1,a1),a1),a1)), % 81.62/81.62 inference(scs_inference,[],[26,770,120,2,18,21,60,24,25])). % 81.62/81.62 cnf(778,plain, % 81.62/81.62 (P3(f7(a1,a1),a1)+~P1(f7(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[26,770,120,2,18,21,60,24,25,67])). % 81.62/81.62 cnf(780,plain, % 81.62/81.62 (P3(f7(a1,a1),f8(a1,a1))+~P1(f7(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[26,167,770,120,2,18,21,60,24,25,67,22,23])). % 81.62/81.62 cnf(783,plain, % 81.62/81.62 (P5(f8(a1,a1),f2(f7(a1,a1),a1))), % 81.62/81.62 inference(scs_inference,[],[167,776,24])). % 81.62/81.62 cnf(784,plain, % 81.62/81.62 (P5(f2(f7(a1,a1),a1),f8(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[167,777,776,24,25])). % 81.62/81.62 cnf(788,plain, % 81.62/81.62 (E(f7(a1,f8(a1,a1)),f2(f7(a1,a1),a1))), % 81.62/81.62 inference(scs_inference,[],[130,772,178,167,777,776,24,25,69,2,3])). % 81.62/81.62 cnf(791,plain, % 81.62/81.62 (E(f8(a1,a1),f8(f2(f7(a1,a1),a1),a1))), % 81.62/81.62 inference(scs_inference,[],[26,130,143,772,178,167,777,776,24,25,69,2,3,67,85])). % 81.62/81.62 cnf(796,plain, % 81.62/81.62 (P5(f8(f8(a1,a1),a1),f2(f7(a1,a1),a1))), % 81.62/81.62 inference(scs_inference,[],[130,183,783,788,791,2,18,24])). % 81.62/81.62 cnf(797,plain, % 81.62/81.62 (P5(f2(f7(a1,a1),a1),f8(f8(a1,a1),a1))), % 81.62/81.62 inference(scs_inference,[],[130,183,784,783,788,791,2,18,24,25])). % 81.62/81.62 cnf(807,plain, % 81.62/81.62 (P3(f7(a1,a1),f8(f8(a1,a1),a1))+~P1(f7(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[26,200,772,791,796,797,138,2,21,69,67])). % 81.62/81.62 cnf(947,plain, % 81.62/81.62 (E(f7(a1,a1),a1)), % 81.62/81.62 inference(scs_inference,[],[161,151,41,18])). % 81.62/81.62 cnf(949,plain, % 81.62/81.62 (E(f7(f8(a1,a1),f8(f8(a1,a1),f8(a1,a1))),f7(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[161,947,2,3])). % 81.62/81.62 cnf(950,plain, % 81.62/81.62 (~P2(f7(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[161,947,120,2,3,21])). % 81.62/81.62 cnf(951,plain, % 81.62/81.62 (P1(f7(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[26,161,947,120,2,3,21,18])). % 81.62/81.62 cnf(952,plain, % 81.62/81.62 (P5(a1,f7(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[26,161,947,120,2,3,21,18,108])). % 81.62/81.62 cnf(954,plain, % 81.62/81.62 (P5(f7(a1,a1),f7(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[26,161,947,120,2,3,21,18,108,60])). % 81.62/81.62 cnf(956,plain, % 81.62/81.62 (P5(f8(a1,a1),f7(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[26,147,130,161,947,120,2,3,21,18,108,60,68])). % 81.62/81.62 cnf(958,plain, % 81.62/81.62 (P3(f7(a1,a1),f7(a1,f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[26,143,147,130,161,788,947,120,2,3,21,18,108,60,68,67])). % 81.62/81.62 cnf(960,plain, % 81.62/81.62 (E(a1,f8(f7(a1,a1),a1))), % 81.62/81.62 inference(scs_inference,[],[26,143,147,130,161,788,947,120,2,3,21,18,108,60,68,67,117])). % 81.62/81.62 cnf(962,plain, % 81.62/81.62 (E(f8(f8(a1,a1),f8(a1,a1)),f8(f7(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[26,143,147,130,161,788,947,120,2,3,21,18,108,60,68,67,117,85])). % 81.62/81.62 cnf(964,plain, % 81.62/81.62 (P3(f7(a1,a1),a1)), % 81.62/81.62 inference(scs_inference,[],[26,143,147,130,161,788,947,120,2,3,21,18,108,60,68,67,117,85,778])). % 81.62/81.62 cnf(967,plain, % 81.62/81.62 (P5(f7(a1,a1),a1)), % 81.62/81.62 inference(scs_inference,[],[26,143,147,130,161,788,947,120,2,3,21,18,108,60,68,67,117,85,778,780,807,25])). % 81.62/81.62 cnf(968,plain, % 81.62/81.62 (E(f7(f7(a1,a1),f8(f7(a1,a1),f7(a1,a1))),f7(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[26,143,147,130,161,788,947,120,2,3,21,18,108,60,68,67,117,85,778,780,807,25,115])). % 81.62/81.62 cnf(970,plain, % 81.62/81.62 (P1(f8(f7(a1,a1),f7(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[26,143,147,130,161,788,947,120,2,3,21,18,108,60,68,67,117,85,778,780,807,25,115,109])). % 81.62/81.62 cnf(978,plain, % 81.62/81.62 (E(f7(a1,f8(a1,a1)),f8(f7(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[392,949,962,2,3])). % 81.62/81.62 cnf(979,plain, % 81.62/81.62 (P5(f7(a1,a1),f8(a1,a1))), % 81.62/81.62 inference(scs_inference,[],[392,167,949,962,967,2,3,25])). % 81.62/81.62 cnf(981,plain, % 81.62/81.62 (P1(f8(f7(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[147,392,167,949,950,968,962,967,2,3,25,21,18])). % 81.62/81.62 cnf(986,plain, % 81.62/81.62 (P5(a1,f7(f8(a1,a1),f8(f8(a1,a1),f8(a1,a1))))), % 81.62/81.62 inference(scs_inference,[],[26,147,130,970,951,151,392,167,949,950,956,968,962,967,2,3,25,21,18,60,69,68])). % 81.62/81.62 cnf(991,plain, % 81.62/81.62 (P5(f8(f7(a1,a1),f8(a1,a1)),f8(f7(a1,a1),f8(a1,a1)))), % 81.62/81.62 inference(scs_inference,[],[26,147,130,970,951,151,392,167,949,950,956,968,962,967,2,3,25,21,18,60,69,68,24,108,53])). % 81.62/81.62 cnf(996,plain, % 81.62/81.62 (E(f8(f7(a1,a1),a1),a1)), % 81.62/81.62 inference(scs_inference,[],[960,2])). % 81.62/81.62 cnf(999,plain, % 81.62/81.62 (~P2(f8(f7(a1,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[167,137,960,978,986,120,2,3,24,21])). % 81.62/81.63 cnf(1000,plain, % 81.62/81.63 (P1(f8(f7(a1,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[26,167,137,960,978,986,120,2,3,24,21,18])). % 81.62/81.63 cnf(1001,plain, % 81.62/81.63 (P5(f8(f7(a1,a1),a1),f8(f7(a1,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[26,167,137,960,978,986,120,2,3,24,21,18,60])). % 81.62/81.63 cnf(1003,plain, % 81.62/81.63 (E(f8(a1,a1),f7(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[26,130,951,167,137,960,979,978,986,956,120,2,3,24,21,18,60,69])). % 81.62/81.63 cnf(1005,plain, % 81.62/81.63 (P5(a1,f8(f7(a1,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,130,951,981,167,137,960,979,978,986,956,120,2,3,24,21,18,60,69,68])). % 81.62/81.63 cnf(1007,plain, % 81.62/81.63 (E(f8(a1,a1),f8(f8(f7(a1,a1),f8(a1,a1)),a1))), % 81.62/81.63 inference(scs_inference,[],[26,130,951,981,167,137,960,979,978,986,956,120,2,3,24,21,18,60,69,68,85])). % 81.62/81.63 cnf(1014,plain, % 81.62/81.63 (E(f8(f7(a1,a1),f8(a1,a1)),f8(f8(a1,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[962,2])). % 81.62/81.63 cnf(1015,plain, % 81.62/81.63 (E(f8(a1,f8(a1,a1)),f2(f7(a1,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[788,448,962,2,3])). % 81.62/81.63 cnf(1017,plain, % 81.62/81.63 (P5(f8(f7(a1,a1),f8(a1,a1)),f8(f8(a1,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[788,448,962,991,2,3,24,25])). % 81.62/81.63 cnf(1019,plain, % 81.62/81.63 (~P2(f8(f7(a1,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[130,788,448,962,991,1007,172,2,3,24,25,18,21])). % 81.62/81.63 cnf(1026,plain, % 81.62/81.63 (E(f7(a1,f8(a1,a1)),f7(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[178,978,1003,2,3])). % 81.62/81.63 cnf(1027,plain, % 81.62/81.63 (P5(a1,f8(f7(a1,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[178,978,996,1003,1001,2,3,24])). % 81.62/81.63 cnf(1028,plain, % 81.62/81.63 (P5(f8(f7(a1,a1),f8(a1,a1)),a1)), % 81.62/81.63 inference(scs_inference,[],[178,163,978,996,1003,1017,1001,2,3,24,25])). % 81.62/81.63 cnf(1031,plain, % 81.62/81.63 (E(f8(a1,a1),f8(f7(a1,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[26,130,951,981,178,163,978,996,952,1003,1017,1001,1005,2,3,24,25,69,85])). % 81.62/81.63 cnf(1041,plain, % 81.62/81.63 (P5(f8(a1,a1),f8(f7(a1,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[178,167,968,1031,1027,2,3,24])). % 81.62/81.63 cnf(1042,plain, % 81.62/81.63 (P5(f8(f7(a1,a1),f8(a1,a1)),f8(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[178,167,968,1031,1028,1027,2,3,24,25])). % 81.62/81.63 cnf(1043,plain, % 81.62/81.63 (P1(f7(f7(a1,a1),f8(f7(a1,a1),f7(a1,a1))))), % 81.62/81.63 inference(scs_inference,[],[951,178,167,968,1031,1028,1027,2,3,24,25,18])). % 81.62/81.63 cnf(1044,plain, % 81.62/81.63 (P5(a1,f7(f7(a1,a1),f8(f7(a1,a1),f7(a1,a1))))), % 81.62/81.63 inference(scs_inference,[],[26,951,178,167,968,1031,1028,1027,2,3,24,25,18,68])). % 81.62/81.63 cnf(1046,plain, % 81.62/81.63 (E(f8(a1,a1),f8(f8(f7(a1,a1),a1),a1))), % 81.62/81.63 inference(scs_inference,[],[26,130,951,1000,178,167,968,1031,1028,1027,2,3,24,25,18,68,85])). % 81.62/81.63 cnf(1054,plain, % 81.62/81.63 (P5(f8(f7(a1,a1),a1),a1)), % 81.62/81.63 inference(scs_inference,[],[167,1007,996,1001,1044,2,24,25])). % 81.62/81.63 cnf(1057,plain, % 81.62/81.63 (~P5(f8(a1,a1),f8(f7(a1,a1),f8(a1,a1)))+E(f8(a1,a1),f8(f7(a1,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[130,981,167,1007,996,1001,1042,1046,1044,138,2,24,25,21,18,69])). % 81.62/81.63 cnf(1060,plain, % 81.62/81.63 (E(f7(a1,a1),f7(a1,f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[1026,2])). % 81.62/81.63 cnf(1062,plain, % 81.62/81.63 (P5(f8(f7(a1,a1),a1),f8(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[167,1026,1054,1005,2,24,25])). % 81.62/81.63 cnf(1063,plain, % 81.62/81.63 (E(f8(f7(a1,a1),a1),f8(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[130,1000,167,1026,1041,1054,1005,2,24,25,69])). % 81.62/81.63 cnf(1065,plain, % 81.62/81.63 (E(a1,f8(f7(a1,f8(a1,a1)),a1))), % 81.62/81.63 inference(scs_inference,[],[26,143,130,1000,167,141,1026,1041,1054,1005,2,24,25,69,85])). % 81.62/81.63 cnf(1067,plain, % 81.62/81.63 (E(f8(a1,a1),f8(f7(a1,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,143,130,1000,167,141,1026,1041,1054,1005,2,24,25,69,85,1057])). % 81.62/81.63 cnf(1068,plain, % 81.62/81.63 (P1(f8(f7(a1,f8(a1,a1)),a1))), % 81.62/81.63 inference(scs_inference,[],[26,143,130,1000,167,141,1026,1041,1054,1005,2,24,25,69,85,1057,18])). % 81.62/81.63 cnf(1075,plain, % 81.62/81.63 (E(f2(f7(a1,a1),a1),f8(a1,f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[1015,2])). % 81.62/81.63 cnf(1096,plain, % 81.62/81.63 (E(f8(f7(a1,f8(a1,a1)),a1),a1)), % 81.62/81.63 inference(scs_inference,[],[1065,2])). % 81.62/81.63 cnf(1387,plain, % 81.62/81.63 (E(f2(a10,a1),a1)), % 81.62/81.63 inference(scs_inference,[],[161,151,42,18])). % 81.62/81.63 cnf(1388,plain, % 81.62/81.63 (E(a1,f2(a10,a1))), % 81.62/81.63 inference(scs_inference,[],[1387,2])). % 81.62/81.63 cnf(1389,plain, % 81.62/81.63 (E(f7(f8(a1,a1),f8(f8(a1,a1),f8(a1,a1))),f2(a10,a1))), % 81.62/81.63 inference(scs_inference,[],[161,1387,2,3])). % 81.62/81.63 cnf(1390,plain, % 81.62/81.63 (P1(f2(a10,a1))), % 81.62/81.63 inference(scs_inference,[],[26,161,1387,2,3,18])). % 81.62/81.63 cnf(1391,plain, % 81.62/81.63 (~P2(f2(a10,a1))), % 81.62/81.63 inference(scs_inference,[],[26,161,1387,120,2,3,18,21])). % 81.62/81.63 cnf(1392,plain, % 81.62/81.63 (P5(f2(a10,a1),f2(a10,a1))), % 81.62/81.63 inference(scs_inference,[],[26,161,1387,120,2,3,18,21,60])). % 81.62/81.63 cnf(1394,plain, % 81.62/81.63 (P1(f8(f2(a10,a1),f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,161,1387,120,2,3,18,21,60,109])). % 81.62/81.63 cnf(1396,plain, % 81.62/81.63 (E(f7(f2(a10,a1),f8(f2(a10,a1),f2(a10,a1))),f2(a10,a1))), % 81.62/81.63 inference(scs_inference,[],[26,161,1387,120,2,3,18,21,60,109,115])). % 81.62/81.63 cnf(1398,plain, % 81.62/81.63 (P5(f8(a1,a1),f2(a10,a1))), % 81.62/81.63 inference(scs_inference,[],[26,130,147,161,1387,120,2,3,18,21,60,109,115,68])). % 81.62/81.63 cnf(1402,plain, % 81.62/81.63 (E(f8(f8(a1,a1),f8(a1,a1)),f8(f2(a10,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[27,26,130,147,161,1387,120,2,3,18,21,60,109,115,68,67,85])). % 81.62/81.63 cnf(1404,plain, % 81.62/81.63 (P3(f7(a10,f8(a10,a10)),a1)), % 81.62/81.63 inference(scs_inference,[],[27,26,130,147,161,220,1387,120,2,3,18,21,60,109,115,68,67,85,22])). % 81.62/81.63 cnf(1405,plain, % 81.62/81.63 (P3(a10,f8(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[27,26,130,147,161,167,220,1387,120,2,3,18,21,60,109,115,68,67,85,22,23])). % 81.62/81.63 cnf(1406,plain, % 81.62/81.63 (P5(a1,f2(a10,a1))), % 81.62/81.63 inference(scs_inference,[],[27,26,130,147,161,167,220,1387,120,2,3,18,21,60,109,115,68,67,85,22,23,24])). % 81.62/81.63 cnf(1407,plain, % 81.62/81.63 (P5(f2(a10,a1),a1)), % 81.62/81.63 inference(scs_inference,[],[27,26,130,147,161,167,220,1387,120,2,3,18,21,60,109,115,68,67,85,22,23,24,25])). % 81.62/81.63 cnf(1412,plain, % 81.62/81.63 (P5(f8(f2(a10,a1),f2(a10,a1)),f8(f2(a10,a1),f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[27,26,130,147,161,167,220,1387,120,2,3,18,21,60,109,115,68,67,85,22,23,24,25,107,108,53])). % 81.62/81.63 cnf(1416,plain, % 81.62/81.63 (E(f8(f2(a10,a1),f8(a1,a1)),f8(f8(a1,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[1402,2])). % 81.62/81.63 cnf(1417,plain, % 81.62/81.63 (P3(f7(a10,f8(a10,a10)),f8(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[1404,167,1402,2,23])). % 81.62/81.63 cnf(1418,plain, % 81.62/81.63 (E(f7(a1,f8(a1,a1)),f8(f2(a10,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[1404,392,167,1402,2,23,3])). % 81.62/81.63 cnf(1419,plain, % 81.62/81.63 (P5(f2(a10,a1),f8(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[1404,392,167,1402,1407,2,23,3,25])). % 81.62/81.63 cnf(1420,plain, % 81.62/81.63 (P1(f8(f2(a10,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[1404,147,392,167,1402,1407,2,23,3,25,18])). % 81.62/81.63 cnf(1422,plain, % 81.62/81.63 (P5(f8(f2(a10,a1),f8(a1,a1)),f8(f2(a10,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[1404,147,392,167,1402,1396,1391,1407,2,23,3,25,18,21,60])). % 81.62/81.63 cnf(1424,plain, % 81.62/81.63 (P5(a1,f8(f2(a10,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,1404,130,147,392,167,1402,1396,1391,1407,2,23,3,25,18,21,60,68])). % 81.62/81.63 cnf(1428,plain, % 81.62/81.63 (E(f2(a10,a1),f8(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[27,26,1404,130,147,1390,151,392,167,1402,1389,1398,1396,1391,1407,2,23,3,25,18,21,60,68,67,69])). % 81.62/81.63 cnf(1430,plain, % 81.62/81.63 (P3(a10,f8(f8(a1,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[27,26,1405,1404,130,147,1390,151,392,167,1402,1389,1398,1396,1391,1407,2,23,3,25,18,21,60,68,67,69,99])). % 81.62/81.63 cnf(1432,plain, % 81.62/81.63 (E(f8(a1,a1),f8(f8(f2(a10,a1),f8(a1,a1)),a1))), % 81.62/81.63 inference(scs_inference,[],[27,26,1405,1404,130,147,1390,151,392,167,1402,1389,1398,1396,1391,1407,2,23,3,25,18,21,60,68,67,69,99,85])). % 81.62/81.63 cnf(1435,plain, % 81.62/81.63 (P5(x14351,f8(f2(a10,a1),f2(a10,a1)))+~E(f8(f2(a10,a1),f2(a10,a1)),x14351)), % 81.62/81.63 inference(scs_inference,[],[27,26,1405,1404,130,147,1390,151,392,167,220,1412,1402,1389,1398,1396,1391,1407,2,23,3,25,18,21,60,68,67,69,99,85,22,24])). % 81.62/81.63 cnf(1444,plain, % 81.62/81.63 (E(f8(a1,a1),f2(a10,a1))), % 81.62/81.63 inference(scs_inference,[],[1428,2])). % 81.62/81.63 cnf(1445,plain, % 81.62/81.63 (E(f7(f2(a10,a1),f8(f2(a10,a1),f2(a10,a1))),a1)), % 81.62/81.63 inference(scs_inference,[],[1387,1428,1396,2,3])). % 81.62/81.63 cnf(1446,plain, % 81.62/81.63 (P5(f8(f8(a1,a1),f8(a1,a1)),f8(f2(a10,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[1387,1428,1416,1422,1396,2,3,24])). % 81.62/81.63 cnf(1447,plain, % 81.62/81.63 (P5(f8(f2(a10,a1),f8(a1,a1)),f8(f8(a1,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[1387,1428,1416,1422,1396,2,3,24,25])). % 81.62/81.63 cnf(1449,plain, % 81.62/81.63 (~P2(f8(f2(a10,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[130,1387,1428,1416,1422,1432,1396,172,2,3,24,25,18,21])). % 81.62/81.63 cnf(1450,plain, % 81.62/81.63 (E(f8(f2(a10,a1),f2(a10,a1)),a1)), % 81.62/81.63 inference(scs_inference,[],[130,1390,1394,1387,1428,1416,1422,1432,1396,172,2,3,24,25,18,21,55])). % 81.62/81.63 cnf(1452,plain, % 81.62/81.63 (E(f8(f2(a10,a1),f2(a10,a1)),f8(a1,f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,130,1390,1394,1387,1428,1416,1422,1432,1396,1407,172,2,3,24,25,18,21,55,85])). % 81.62/81.63 cnf(1454,plain, % 81.62/81.63 (P5(a1,f8(f2(a10,a1),f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,130,1390,1394,1387,1428,1416,1422,1432,1396,1407,172,2,3,24,25,18,21,55,85,1435])). % 81.62/81.63 cnf(1455,plain, % 81.62/81.63 (~P2(f8(f2(a10,a1),f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,130,1390,1394,1387,1428,1416,1422,1432,1396,1407,172,2,3,24,25,18,21,55,85,1435,37])). % 81.62/81.63 cnf(1459,plain, % 81.62/81.63 (P3(a10,f2(a10,a1))+~P1(f7(f2(a10,a1),f8(f2(a10,a1),f2(a10,a1))))), % 81.62/81.63 inference(scs_inference,[],[27,26,130,1390,1394,1387,1428,1416,1422,1432,1396,1407,172,2,3,24,25,18,21,55,85,1435,37,67,23])). % 81.62/81.63 cnf(1463,plain, % 81.62/81.63 (P5(f8(a1,f2(a10,a1)),f8(f2(a10,a1),f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[1452,1435])). % 81.62/81.63 cnf(1464,plain, % 81.62/81.63 (E(f8(f2(a10,a1),f8(a1,a1)),f7(a1,f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[1418,1452,1435,2])). % 81.62/81.63 cnf(1466,plain, % 81.62/81.63 (P5(f8(a1,a1),f8(f2(a10,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[167,137,1418,1424,1452,1435,2,3,24])). % 81.62/81.63 cnf(1467,plain, % 81.62/81.63 (P5(f8(f2(a10,a1),f8(a1,a1)),a1)), % 81.62/81.63 inference(scs_inference,[],[163,167,137,1418,1447,1424,1452,1435,2,3,24,25])). % 81.62/81.63 cnf(1468,plain, % 81.62/81.63 (P1(f8(a1,f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[1394,163,167,137,1418,1447,1424,1452,1435,2,3,24,25,18])). % 81.62/81.63 cnf(1469,plain, % 81.62/81.63 (P5(f8(a1,f2(a10,a1)),f8(a1,f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[1394,163,167,137,1418,1447,1424,1452,1435,2,3,24,25,18,60])). % 81.62/81.63 cnf(1479,plain, % 81.62/81.63 (E(a1,f7(f2(a10,a1),f8(f2(a10,a1),f2(a10,a1))))), % 81.62/81.63 inference(scs_inference,[],[1445,2])). % 81.62/81.63 cnf(1480,plain, % 81.62/81.63 (E(f8(a1,a1),f8(f2(a10,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[210,1445,1418,2,3])). % 81.62/81.63 cnf(1481,plain, % 81.62/81.63 (P5(f8(a1,a1),f8(f2(a10,a1),f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[167,210,1445,1418,1454,2,3,24])). % 81.62/81.63 cnf(1482,plain, % 81.62/81.63 (P5(f8(f8(a1,a1),f8(a1,a1)),f7(a1,f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[167,210,1445,1418,1464,1446,1454,2,3,24,25])). % 81.62/81.63 cnf(1483,plain, % 81.62/81.63 (P1(f7(f2(a10,a1),f8(f2(a10,a1),f2(a10,a1))))), % 81.62/81.63 inference(scs_inference,[],[26,167,210,1445,1418,1464,1446,1454,2,3,24,25,18])). % 81.62/81.63 cnf(1484,plain, % 81.62/81.63 (P3(a10,f7(f2(a10,a1),f8(f2(a10,a1),f2(a10,a1))))), % 81.62/81.63 inference(scs_inference,[],[27,26,167,210,1445,1418,1396,1464,1446,1454,2,3,24,25,18,67])). % 81.62/81.63 cnf(1489,plain, % 81.62/81.63 (P3(a10,f2(a10,a1))), % 81.62/81.63 inference(scs_inference,[],[1483,1459])). % 81.62/81.63 cnf(1491,plain, % 81.62/81.63 (E(a1,f8(f2(a10,a1),f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[1450,2])). % 81.62/81.63 cnf(1493,plain, % 81.62/81.63 (P5(f8(a1,f2(a10,a1)),a1)), % 81.62/81.63 inference(scs_inference,[],[742,448,1450,1463,2,3,25])). % 81.62/81.63 cnf(1494,plain, % 81.62/81.63 (P5(x14941,f8(a1,f2(a10,a1)))+~E(f8(a1,f2(a10,a1)),x14941)), % 81.62/81.63 inference(scs_inference,[],[742,448,1450,1469,1463,2,3,25,24])). % 81.62/81.63 cnf(1501,plain, % 81.62/81.63 (P5(f8(f2(a10,a1),f8(a1,a1)),f8(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[167,1389,1452,1467,1491,2,3,25])). % 81.62/81.63 cnf(1507,plain, % 81.62/81.63 (P5(x15071,f8(f2(a10,a1),f2(a10,a1)))+~E(f8(a1,f2(a10,a1)),x15071)), % 81.62/81.63 inference(scs_inference,[],[27,1484,1489,130,1390,1394,1420,167,220,1389,1452,1463,1467,1491,1466,2,3,25,69,99,22,24])). % 81.62/81.63 cnf(1512,plain, % 81.62/81.63 (E(f8(a1,f2(a10,a1)),f8(f2(a10,a1),f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[1452,2])). % 81.62/81.63 cnf(1513,plain, % 81.62/81.63 (E(f7(a1,f8(a1,a1)),f2(a10,a1))), % 81.62/81.63 inference(scs_inference,[],[178,1452,1444,2,3])). % 81.62/81.63 cnf(1514,plain, % 81.62/81.63 (P5(f8(f2(a10,a1),f2(a10,a1)),a1)), % 81.62/81.63 inference(scs_inference,[],[178,1452,1444,1493,2,3,24])). % 81.62/81.63 cnf(1515,plain, % 81.62/81.63 (P5(f8(a1,f2(a10,a1)),f8(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[178,167,1452,1444,1493,2,3,24,25])). % 81.62/81.63 cnf(1516,plain, % 81.62/81.63 (~P2(f8(a1,f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[178,167,1452,1444,1455,1493,2,3,24,25,21])). % 81.62/81.63 cnf(1519,plain, % 81.62/81.63 (E(f8(a1,a1),f8(f2(a10,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[27,26,130,143,1390,178,167,1452,1444,1406,1455,1493,2,3,24,25,21,67,85])). % 81.62/81.63 cnf(1521,plain, % 81.62/81.63 (P5(f8(f2(a10,a1),f2(a10,a1)),f8(a1,f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[27,26,130,143,1390,178,167,1452,1444,1406,1455,1493,2,3,24,25,21,67,85,1494])). % 81.62/81.63 cnf(1522,plain, % 81.62/81.63 (P3(f7(a10,f8(a10,a10)),f7(a1,f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[27,26,130,143,1390,178,167,220,1452,1444,1406,1455,1493,2,3,24,25,21,67,85,1494,22])). % 81.62/81.63 cnf(1523,plain, % 81.62/81.63 (P1(f8(f2(a10,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[27,26,130,143,1390,178,167,220,1452,1444,1406,1455,1493,2,3,24,25,21,67,85,1494,22,18])). % 81.62/81.63 cnf(1524,plain, % 81.62/81.63 (P5(f8(f2(a10,a1),a1),f8(f2(a10,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[27,26,130,143,1390,178,167,220,1452,1444,1406,1455,1493,2,3,24,25,21,67,85,1494,22,18,60])). % 81.62/81.63 cnf(1528,plain, % 81.62/81.63 (E(f8(a1,a1),f8(a1,f2(a10,a1)))+~P5(a1,f8(a1,f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[27,26,130,143,1390,1468,178,167,160,220,1452,1444,1406,1455,1493,2,3,24,25,21,67,85,1494,22,18,60,69,83])). % 81.62/81.63 cnf(1532,plain, % 81.62/81.63 (E(f7(a1,f8(a1,a1)),f8(f2(a10,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[178,1396,1519,2,3])). % 81.62/81.63 cnf(1534,plain, % 81.62/81.63 (P5(f8(f2(a10,a1),f2(a10,a1)),f8(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[178,167,1450,1396,1521,1519,1514,2,3,24,25])). % 81.62/81.63 cnf(1535,plain, % 81.62/81.63 (P5(a1,f8(f2(a10,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[26,130,1523,178,167,1450,1396,1521,1519,1514,2,3,24,25,68])). % 81.62/81.63 cnf(1541,plain, % 81.62/81.63 (E(f8(a1,a1),f8(a1,f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,130,1394,1523,178,167,1450,1396,1481,1521,1519,1514,2,3,24,25,68,69,85,1528])). % 81.62/81.63 cnf(1550,plain, % 81.62/81.63 (E(f7(a1,f8(a1,a1)),f8(a1,f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[178,1432,1541,2,3])). % 81.62/81.63 cnf(1553,plain, % 81.62/81.63 (E(f8(a1,a1),f8(f2(a10,a1),f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[130,1394,178,167,1432,1481,1541,1534,1535,138,2,3,24,21,69])). % 81.62/81.63 cnf(1587,plain, % 81.62/81.63 (E(f8(f2(a10,a1),a1),f7(a1,f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[1532,2])). % 81.62/81.63 cnf(1588,plain, % 81.62/81.63 (E(f7(a1,f8(a1,a1)),f8(f2(a10,a1),f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[178,1532,1553,2,3])). % 81.62/81.63 cnf(1589,plain, % 81.62/81.63 (P5(f7(a1,f8(a1,a1)),f8(f2(a10,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[178,1532,1553,1524,2,3,24])). % 81.62/81.63 cnf(1590,plain, % 81.62/81.63 (P5(f8(f2(a10,a1),a1),f7(a1,f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[178,1532,1553,1524,2,3,24,25])). % 81.62/81.63 cnf(1591,plain, % 81.62/81.63 (~P2(f8(f2(a10,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[178,1532,1553,1524,142,2,3,24,25,21])). % 81.62/81.63 cnf(1599,plain, % 81.62/81.63 (E(f8(a1,f2(a10,a1)),f7(a1,f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[1550,2])). % 81.62/81.63 cnf(1604,plain, % 81.62/81.63 (P5(f7(a1,f8(a1,a1)),f8(f2(a10,a1),f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,1523,125,1452,1550,1590,1535,2,3,25,69,1507])). % 81.62/81.63 cnf(1605,plain, % 81.62/81.63 (P5(f7(a1,f8(a1,a1)),f8(a1,f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,1523,125,1452,1550,1590,1535,2,3,25,69,1507,1494])). % 81.62/81.63 cnf(1742,plain, % 81.62/81.63 (E(f8(f8(a1,a1),f8(a1,a1)),f2(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[788,169,723,177,24,25,3])). % 81.62/81.63 cnf(1743,plain, % 81.62/81.63 (P3(f7(a1,a1),f2(f7(a1,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[958,788,169,723,177,24,25,3,23])). % 81.62/81.63 cnf(1745,plain, % 81.62/81.63 (P3(a1,f2(f7(a1,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[958,788,169,947,723,177,24,25,3,23,2,22])). % 81.62/81.63 cnf(1750,plain, % 81.62/81.63 (P3(f8(a1,a1),f2(f7(a1,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[1745,167,22])). % 81.62/81.63 cnf(1753,plain, % 81.62/81.63 (E(f8(a1,f8(a1,a1)),f8(f7(a1,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[1745,788,167,175,962,1482,1604,22,24,25,3])). % 81.62/81.63 cnf(1754,plain, % 81.62/81.63 (P3(f7(a10,f8(a10,a10)),f2(f7(a1,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[1522,1745,788,167,175,962,1482,1604,22,24,25,3,23])). % 81.62/81.63 cnf(1761,plain, % 81.62/81.63 (P3(a10,f2(f7(a1,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[1754,189,22])). % 81.62/81.63 cnf(1763,plain, % 81.62/81.63 (P5(f8(f2(a10,a1),a1),f2(f7(a1,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[1754,788,189,1605,1590,22,24,25])). % 81.62/81.63 cnf(1766,plain, % 81.62/81.63 (P3(f7(a1,a1),f7(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[26,590,1750,1754,951,788,1060,189,1605,1590,22,24,25,3,23,67])). % 81.62/81.63 cnf(1768,plain, % 81.62/81.63 (E(a1,f8(f2(f7(a1,a1),a1),a1))), % 81.62/81.63 inference(scs_inference,[],[26,590,1750,1754,951,772,788,1060,776,189,1605,1590,22,24,25,3,23,67,85])). % 81.62/81.63 cnf(1775,plain, % 81.62/81.63 (P3(a1,f7(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[1766,947,1768,2,22])). % 81.62/81.63 cnf(1776,plain, % 81.62/81.63 (P5(f2(f7(a1,a1),a1),f8(f2(a10,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[1766,788,947,1589,1768,2,22,24])). % 81.62/81.63 cnf(1777,plain, % 81.62/81.63 (E(f7(a1,a1),f8(f2(a1,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[1766,788,602,947,1060,1589,1768,2,22,24,3])). % 81.62/81.63 cnf(1781,plain, % 81.62/81.63 (E(a1,f8(f8(f2(a1,a1),f8(a1,a1)),a1))), % 81.62/81.63 inference(scs_inference,[],[26,1766,561,772,430,1523,788,602,947,1060,605,1589,1763,1768,2,22,24,3,23,69,85])). % 81.62/81.63 cnf(1783,plain, % 81.62/81.63 (~P3(f7(a1,a1),f7(a13,f8(a13,a13)))), % 81.62/81.63 inference(scs_inference,[],[26,1766,951,414,561,772,430,1523,788,602,947,1060,605,1589,1763,1768,2,22,24,3,23,69,85,84])). % 81.62/81.63 cnf(1791,plain, % 81.62/81.63 (E(f7(a1,a1),f8(f2(a1,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[1775,167,742,1060,1777,2,22,3])). % 81.62/81.63 cnf(1794,plain, % 81.62/81.63 (E(a1,f8(f8(f2(a1,a1),a1),a1))), % 81.62/81.63 inference(scs_inference,[],[26,1775,703,772,1523,167,742,1060,743,1763,1777,1776,2,22,3,69,85])). % 81.62/81.63 cnf(1796,plain, % 81.62/81.63 (P3(f7(a1,a1),f8(f2(a10,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[26,1775,951,703,772,1523,167,742,1060,743,1763,1777,1776,2,22,3,69,85,67])). % 81.62/81.63 cnf(1808,plain, % 81.62/81.63 (P3(a1,f8(f2(a10,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[1796,947,1781,2,22])). % 81.62/81.63 cnf(1809,plain, % 81.62/81.63 (E(f7(a1,a1),f2(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[1796,694,947,1060,1781,2,22,3])). % 81.62/81.63 cnf(1817,plain, % 81.62/81.63 (E(f7(a1,a1),f8(f7(a1,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[1808,167,978,1060,1791,2,22,3])). % 81.62/81.63 cnf(1818,plain, % 81.62/81.63 (E(a1,f8(f8(f7(a1,a1),f8(a1,a1)),a1))), % 81.62/81.63 inference(scs_inference,[],[26,1808,981,167,978,1060,1005,1791,2,22,3,85])). % 81.62/81.63 cnf(1824,plain, % 81.62/81.63 (E(f2(a1,a1),f7(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[1809,2])). % 81.62/81.63 cnf(1835,plain, % 81.62/81.63 (P3(f7(a1,a1),f8(f8(a1,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,951,147,169,1015,1794,2,3,67])). % 81.62/81.63 cnf(1843,plain, % 81.62/81.63 (E(f8(a1,a1),f8(f7(a1,f8(a1,a1)),a1))), % 81.62/81.63 inference(scs_inference,[],[132,1065,1817,2,3])). % 81.62/81.63 cnf(1850,plain, % 81.62/81.63 (E(f7(a1,a1),f8(f2(a10,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[1060,1418,1818,2,3])). % 81.62/81.63 cnf(1851,plain, % 81.62/81.63 (E(a1,f8(f8(f2(a10,a1),f8(a1,a1)),a1))), % 81.62/81.63 inference(scs_inference,[],[26,1420,1060,1418,1424,1818,2,3,85])). % 81.62/81.63 cnf(1897,plain, % 81.62/81.63 (P3(a10,f7(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[26,951,27,1060,1513,1850,2,3,67])). % 81.62/81.63 cnf(1915,plain, % 81.62/81.63 (E(f8(a1,f8(a1,a1)),f8(f2(a10,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[175,1402,1843,2,3])). % 81.62/81.63 cnf(1957,plain, % 81.62/81.63 (E(f8(a1,a1),f7(f2(a10,a1),f8(f2(a10,a1),f2(a10,a1))))), % 81.62/81.63 inference(scs_inference,[],[132,1479,1851,2,3])). % 81.62/81.63 cnf(2051,plain, % 81.62/81.63 (E(f8(f2(a10,a1),f2(a10,a1)),f8(f8(a1,a1),f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[1390,130,1394,1419,1957,2,85])). % 81.62/81.63 cnf(2054,plain, % 81.62/81.63 (P1(f8(f8(a1,a1),f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[1390,130,1394,1419,1957,2,85,1435,18])). % 81.62/81.63 cnf(2055,plain, % 81.62/81.63 (E(f8(a1,f2(a10,a1)),f8(f8(a1,a1),f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[1390,130,1394,1512,1419,1957,2,85,1435,18,3])). % 81.62/81.63 cnf(2056,plain, % 81.62/81.63 (P5(f8(f8(a1,a1),f2(a10,a1)),a1)), % 81.62/81.63 inference(scs_inference,[],[1390,130,1394,1450,1512,1419,1957,2,85,1435,18,3,25])). % 81.62/81.63 cnf(2058,plain, % 81.62/81.63 (P5(f8(f8(a1,a1),f2(a10,a1)),f8(f8(a1,a1),f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[1390,130,1394,1450,1512,1419,1957,2,85,1435,18,3,25,24,60])). % 81.62/81.63 cnf(2067,plain, % 81.62/81.63 (E(f7(a1,f8(a1,a1)),f8(f8(a1,a1),f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[1550,2055,2,3])). % 81.62/81.63 cnf(2068,plain, % 81.62/81.63 (P5(f8(f8(a1,a1),f2(a10,a1)),f8(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[167,1550,2055,2056,2,3,25])). % 81.62/81.63 cnf(2070,plain, % 81.62/81.63 (~P2(f8(f8(a1,a1),f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[167,1550,2058,1516,2055,2056,2,3,25,24,21])). % 81.62/81.63 cnf(2071,plain, % 81.62/81.63 (P5(a1,f8(f8(a1,a1),f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,130,2054,167,1550,2058,1516,2055,2056,2,3,25,24,21,68])). % 81.62/81.63 cnf(2073,plain, % 81.62/81.63 (E(a1,f8(f8(a1,a1),f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,130,2054,167,1550,2058,1516,2055,2056,2,3,25,24,21,68,69])). % 81.62/81.63 cnf(2085,plain, % 81.62/81.63 (E(f8(a1,a1),f8(f8(a1,a1),f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[130,2054,167,1060,2051,2068,2067,2071,2,3,24,69])). % 81.62/81.63 cnf(2266,plain, % 81.62/81.63 (E(f8(f2(a10,a1),a1),f8(f2(a10,a1),f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[1587,1588,3])). % 81.62/81.63 cnf(2530,plain, % 81.62/81.63 (P5(f8(f2(a1,a1),f8(a1,a1)),f2(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[639,771,1599,1418,544,533,25,3,24])). % 81.62/81.63 cnf(2536,plain, % 81.62/81.63 (~P5(f2(f7(a1,a1),a1),f2(a1,a1))+E(f2(f7(a1,a1),a1),f2(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[1417,1750,527,772,639,771,1599,1418,544,533,25,3,24,22,23,1507,2,1494,69])). % 81.62/81.63 cnf(2539,plain, % 81.62/81.63 (P5(f2(a1,a1),f8(f2(a1,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[639,563,25])). % 81.62/81.63 cnf(2546,plain, % 81.62/81.63 (E(f2(f7(a1,a1),a1),f2(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[1430,1745,527,561,639,771,962,1063,1067,563,585,2530,25,3,22,23,24,69,2536])). % 81.62/81.63 cnf(2555,plain, % 81.62/81.63 (E(f8(a1,f2(a10,a1)),f8(f8(a1,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[962,1599,304,584,2546,2,25,3])). % 81.62/81.63 cnf(2559,plain, % 81.62/81.63 (P3(f7(a1,a1),f2(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[26,1405,1743,951,527,639,962,1599,1060,304,584,621,2546,2,25,3,23,24,22,67])). % 81.62/81.63 cnf(2561,plain, % 81.62/81.63 (E(f8(f2(a1,a1),f8(a1,a1)),f2(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[26,1405,1743,951,527,561,639,962,1599,1060,304,584,621,2546,2539,2530,2,25,3,23,24,22,67,69])). % 81.62/81.63 cnf(2573,plain, % 81.62/81.63 (E(f8(a1,f2(a10,a1)),f2(a10,a1))), % 81.62/81.63 inference(scs_inference,[],[1754,771,1075,1599,1513,592,605,2555,2,25,23,24,3])). % 81.62/81.63 cnf(2575,plain, % 81.62/81.63 (P3(a1,f8(f2(a1,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,1754,1796,561,771,1075,1599,1060,1513,592,605,2561,2555,2,25,23,24,3,22,67])). % 81.62/81.63 cnf(2577,plain, % 81.62/81.63 (E(f2(f7(a1,a1),a1),f8(f2(a1,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,1754,1796,561,772,771,1075,1599,1060,1513,592,605,2561,2555,2,25,23,24,3,22,67,69])). % 81.62/81.63 cnf(2582,plain, % 81.62/81.63 (P5(f2(a10,a1),f8(a1,f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,1754,1796,430,414,561,772,771,1075,1599,1060,1513,592,605,2561,2555,2,25,23,24,3,22,67,69,84,1507,1494])). % 81.62/81.63 cnf(2592,plain, % 81.62/81.63 (E(f8(a1,f2(a10,a1)),f8(f8(a1,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[1761,1808,771,962,1075,1599,392,621,604,626,2577,2,25,24,23,22,3])). % 81.62/81.63 cnf(2604,plain, % 81.62/81.63 (P5(f8(f2(a1,a1),a1),f8(f2(a1,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[639,714,2573,2,25])). % 81.62/81.63 cnf(2607,plain, % 81.62/81.63 (E(f8(a1,f2(a10,a1)),f8(a1,f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[2575,430,639,1599,418,621,603,714,2573,2,25,23,24,3])). % 81.62/81.63 cnf(2619,plain, % 81.62/81.63 (P5(f8(f2(a1,a1),a1),f2(f7(a1,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[771,715,2592,2,25])). % 81.62/81.63 cnf(2621,plain, % 81.62/81.63 (P3(f2(f7(a1,a1),a1),f7(a1,f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[695,639,771,713,715,2592,2,25,24,22])). % 81.62/81.63 cnf(2622,plain, % 81.62/81.63 (E(f7(f2(a1,a1),f8(f2(a1,a1),f2(a1,a1))),a1)), % 81.62/81.63 inference(scs_inference,[],[695,639,771,545,524,713,715,2592,2,25,24,22,3])). % 81.62/81.63 cnf(2627,plain, % 81.62/81.63 (E(f8(f2(a1,a1),f2(a1,a1)),f8(a1,f2(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,695,527,547,561,703,639,771,545,524,544,713,715,2592,2604,2,25,24,22,3,55,69,85])). % 81.62/81.63 cnf(2629,plain, % 81.62/81.63 (P5(a1,f8(f2(a1,a1),f2(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,695,527,547,561,703,639,771,545,524,544,713,715,2592,2604,2,25,24,22,3,55,69,85,671])). % 81.62/81.63 cnf(2630,plain, % 81.62/81.63 (P5(f8(f2(a1,a1),f2(a1,a1)),a1)), % 81.62/81.63 inference(scs_inference,[],[26,695,527,547,561,703,639,771,545,524,544,713,715,2592,2604,2,25,24,22,3,55,69,85,671,672])). % 81.62/81.63 cnf(2631,plain, % 81.62/81.63 (~P2(f8(f2(a1,a1),f2(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,695,527,547,561,703,639,771,545,524,544,713,715,2592,2604,2,25,24,22,3,55,69,85,671,672,37])). % 81.62/81.63 cnf(2633,plain, % 81.62/81.63 (P1(f8(a1,f2(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,695,527,547,561,703,639,771,545,524,544,713,715,2592,2604,2,25,24,22,3,55,69,85,671,672,37,18])). % 81.62/81.63 cnf(2641,plain, % 81.62/81.63 (P5(f8(f2(a1,a1),f2(a1,a1)),f8(a1,f2(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[2627,671,672])). % 81.62/81.63 cnf(2644,plain, % 81.62/81.63 (P5(f2(f7(a1,a1),a1),f8(f2(a1,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[639,771,743,1062,2607,2627,671,672,2,25,24])). % 81.62/81.63 cnf(2645,plain, % 81.62/81.63 (P3(f8(f2(a1,a1),f8(a1,a1)),f7(a1,f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[710,639,771,743,1062,2607,2627,671,672,2,25,24,22])). % 81.62/81.63 cnf(2646,plain, % 81.62/81.63 (E(f8(a1,f2(a10,a1)),f8(f2(a1,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[710,639,771,1599,602,743,1062,2607,2627,671,672,2,25,24,22,3])). % 81.62/81.63 cnf(2655,plain, % 81.62/81.63 (E(a1,f7(f2(a1,a1),f8(f2(a1,a1),f2(a1,a1))))), % 81.62/81.63 inference(scs_inference,[],[2622,2])). % 81.62/81.63 cnf(2659,plain, % 81.62/81.63 (E(f8(a1,f2(a10,a1)),f2(f7(a1,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[1835,771,962,1599,1060,788,1482,967,2622,2,25,24,22,3])). % 81.62/81.63 cnf(2662,plain, % 81.62/81.63 (E(a1,f8(f2(a1,a1),f2(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,1835,1468,951,547,771,962,1599,1060,788,1482,967,2622,2630,2629,2,25,24,22,3,67,69])). % 81.62/81.63 cnf(2672,plain, % 81.62/81.63 (~P2(f8(a1,f2(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[2627,2631,2,21])). % 81.62/81.63 cnf(2674,plain, % 81.62/81.63 (P5(f2(f7(a1,a1),a1),f8(f7(a1,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[639,771,1027,979,2627,2631,2,21,25,24])). % 81.62/81.63 cnf(2676,plain, % 81.62/81.63 (E(f8(f7(a1,a1),f8(a1,a1)),f8(f2(a10,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[531,639,771,1014,1402,1027,979,2627,2631,2,21,25,24,22,3])). % 81.62/81.63 cnf(2685,plain, % 81.62/81.63 (P5(f8(f7(a1,a1),f8(a1,a1)),f2(f7(a1,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[771,1028,2646,2,25])). % 81.62/81.63 cnf(2687,plain, % 81.62/81.63 (P3(f8(f2(a1,a1),f8(a1,a1)),f2(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[542,639,771,952,1028,2646,2,25,24,22])). % 81.62/81.63 cnf(2688,plain, % 81.62/81.63 (E(f8(f7(a1,f8(a1,a1)),a1),f2(a10,a1))), % 81.62/81.63 inference(scs_inference,[],[542,639,771,1096,1388,952,1028,2646,2,25,24,22,3])). % 81.62/81.63 cnf(2691,plain, % 81.62/81.63 (E(f8(f2(a1,a1),a1),f2(f7(a1,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[26,542,27,703,772,1068,639,771,1096,1388,952,1028,2646,2619,2644,2,25,24,22,3,67,69])). % 81.62/81.63 cnf(2700,plain, % 81.62/81.63 (P5(f8(f7(a1,a1),a1),f2(f7(a1,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[639,771,1041,1054,2659,2,24,25])). % 81.62/81.63 cnf(2701,plain, % 81.62/81.63 (P3(f7(a1,f8(a1,a1)),f7(a1,f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[958,639,771,1060,1041,1054,2659,2,24,25,22])). % 81.62/81.63 cnf(2702,plain, % 81.62/81.63 (E(f8(f7(a1,a1),a1),f2(a10,a1))), % 81.62/81.63 inference(scs_inference,[],[958,639,771,1063,1060,1444,1041,1054,2659,2,24,25,22,3])). % 81.62/81.63 cnf(2705,plain, % 81.62/81.63 (E(f8(f7(a1,a1),a1),f2(f7(a1,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[26,958,1000,951,703,772,639,771,1063,1060,1444,1041,1054,2659,2674,2691,2,24,25,22,3,67,69])). % 81.62/81.63 cnf(2707,plain, % 81.62/81.63 (~P3(f8(f2(a1,a1),a1),f7(a13,f8(a13,a13)))), % 81.62/81.63 inference(scs_inference,[],[26,958,1783,1000,951,414,703,772,639,771,1063,1060,1444,1041,1054,2659,2674,2691,2,24,25,22,3,67,69,84])). % 81.62/81.63 cnf(2716,plain, % 81.62/81.63 (P5(f8(f2(a1,a1),f8(a1,a1)),f7(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[639,621,956,565,2676,2,25,24])). % 81.62/81.63 cnf(2723,plain, % 81.62/81.63 (~P3(f8(f7(a1,a1),a1),f7(a13,f8(a13,a13)))), % 81.62/81.63 inference(scs_inference,[],[26,535,1783,1000,951,414,772,639,771,1075,621,1753,956,565,2676,2700,2705,2674,2,25,24,22,3,67,69,84])). % 81.62/81.63 cnf(2725,plain, % 81.62/81.63 (P3(f2(f7(a1,a1),a1),f8(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[26,535,1783,2621,1000,130,951,414,772,639,771,1075,621,1753,956,565,2676,2700,2705,2674,2,25,24,22,3,67,69,84,99])). % 81.62/81.63 cnf(2737,plain, % 81.62/81.63 (E(f8(f7(a1,a1),a1),f8(f2(a10,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[559,639,771,1063,754,1480,1005,705,2688,2,24,25,22,3])). % 81.62/81.63 cnf(2742,plain, % 81.62/81.63 (P3(f8(f2(a1,a1),f8(a1,a1)),f8(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[26,559,2645,981,1000,27,130,561,772,639,771,1063,754,1480,1005,705,2688,2702,2685,2,24,25,22,3,67,69,99])). % 81.62/81.63 cnf(2753,plain, % 81.62/81.63 (E(f8(f7(a1,a1),a1),f8(a1,f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[588,771,1063,1075,621,1541,565,774,2702,2,25,24,22,3])). % 81.62/81.63 cnf(2765,plain, % 81.62/81.63 (E(f8(f7(a1,a1),a1),f8(f2(a10,a1),f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[1063,1060,754,1553,705,954,2737,2,24,25,3])). % 81.62/81.63 cnf(2771,plain, % 81.62/81.63 (P5(f2(a10,a1),f8(f2(a1,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[639,1419,2753,2,25])). % 81.62/81.63 cnf(2774,plain, % 81.62/81.63 (E(f8(a1,f2(a10,a1)),f8(f2(a1,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[622,639,1075,1599,742,774,1419,2753,2,25,24,22,3])). % 81.62/81.63 cnf(2786,plain, % 81.62/81.63 (P5(f2(a10,a1),f2(f7(a1,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[771,1407,2765,2774,1507,1494,2,25])). % 81.62/81.63 cnf(2789,plain, % 81.62/81.63 (E(f2(f7(a1,a1),a1),f8(f2(a10,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[664,639,771,1075,1060,1915,954,1407,2765,2774,1507,1494,2,25,24,22,3])). % 81.62/81.63 cnf(2796,plain, % 81.62/81.63 (E(f8(f7(a1,a1),f8(a1,a1)),f2(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[639,962,1014,1742,1398,1447,2789,2,25,24,3])). % 81.62/81.63 cnf(2798,plain, % 81.62/81.63 (P3(f7(a1,a1),f8(f2(a10,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,658,1420,951,639,962,1014,1742,1398,1447,2789,2,25,24,3,22,67])). % 81.62/81.63 cnf(2800,plain, % 81.62/81.63 (E(f8(f2(a1,a1),f8(a1,a1)),f2(a10,a1))), % 81.62/81.63 inference(scs_inference,[],[26,658,1390,1420,951,561,639,962,1014,1742,1398,1447,2789,2771,2,25,24,3,22,67,69])). % 81.62/81.63 cnf(2811,plain, % 81.62/81.63 (P5(f2(f7(a1,a1),a1),f2(a10,a1))), % 81.62/81.63 inference(scs_inference,[],[771,1406,1467,2774,2,25,24])). % 81.62/81.63 cnf(2825,plain, % 81.62/81.63 (E(f8(a1,f2(a10,a1)),f2(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[771,962,1599,694,1446,1493,2800,2,25,24,3])). % 81.62/81.63 cnf(2827,plain, % 81.62/81.63 (P3(a1,f8(a1,f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,728,1468,771,962,1599,694,1446,1493,2800,2,25,24,3,22,67])). % 81.62/81.63 cnf(2829,plain, % 81.62/81.63 (E(f2(a10,a1),f2(f7(a1,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[26,728,1390,1468,772,771,962,1599,694,1446,1493,2800,2811,2786,2,25,24,3,22,67,69])). % 81.62/81.63 cnf(2838,plain, % 81.62/81.63 (E(f2(a1,a1),f8(f7(a1,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[2796,2])). % 81.62/81.63 cnf(2840,plain, % 81.62/81.63 (P5(f8(f2(a10,a1),f8(a1,a1)),f8(f2(a1,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[639,771,1424,1501,2796,2,24,25])). % 81.62/81.63 cnf(2841,plain, % 81.62/81.63 (E(f7(f2(a1,a1),f8(f2(a1,a1),f2(a1,a1))),f7(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[639,771,545,1824,1424,1501,2796,2,24,25,3])). % 81.62/81.63 cnf(2843,plain, % 81.62/81.63 (P5(f2(a1,a1),f7(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[741,951,527,547,639,771,545,1824,1424,1501,2796,2,24,25,3,22,68])). % 81.62/81.63 cnf(2845,plain, % 81.62/81.63 (P3(f7(a1,a1),f2(a10,a1))), % 81.62/81.63 inference(scs_inference,[],[26,741,1390,951,527,547,639,771,545,1824,1424,1501,2796,2829,2,24,25,3,22,68,67])). % 81.62/81.63 cnf(2849,plain, % 81.62/81.63 (~P3(f2(a10,a1),f7(a13,f8(a13,a13)))), % 81.62/81.63 inference(scs_inference,[],[26,741,1783,1390,951,527,414,547,639,771,545,1824,1424,1501,2796,2829,2,24,25,3,22,68,67,85,84])). % 81.62/81.63 cnf(2851,plain, % 81.62/81.63 (P5(f8(f7(a1,a1),f2(a1,a1)),f8(f2(a1,a1),f2(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,741,1783,1390,951,527,414,547,639,771,545,1824,1424,1501,2796,2829,2,24,25,3,22,68,67,85,84,671])). % 81.62/81.63 cnf(2852,plain, % 81.62/81.63 (P5(f8(f2(a1,a1),f2(a1,a1)),f8(f7(a1,a1),f2(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,741,1783,1390,951,527,414,547,639,771,545,1824,1424,1501,2796,2829,2,24,25,3,22,68,67,85,84,671,672])). % 81.62/81.63 cnf(2853,plain, % 81.62/81.63 (P1(f8(f7(a1,a1),f2(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,741,1783,1390,951,527,414,547,639,771,545,1824,1424,1501,2796,2829,2,24,25,3,22,68,67,85,84,671,672,18])). % 81.62/81.63 cnf(2854,plain, % 81.62/81.63 (~E(f2(a10,a1),f7(a13,f8(a13,a13)))), % 81.62/81.63 inference(scs_inference,[],[26,741,1783,1390,951,527,414,547,639,771,545,1824,1424,1501,2796,2829,2,24,25,3,22,68,67,85,84,671,672,18,23])). % 81.62/81.63 cnf(2855,plain, % 81.62/81.63 (P5(f8(f7(a1,a1),f2(a1,a1)),f8(f7(a1,a1),f2(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,741,1783,1390,951,527,414,547,639,771,545,1824,1424,1501,2796,2829,2,24,25,3,22,68,67,85,84,671,672,18,23,60])). % 81.62/81.63 cnf(2860,plain, % 81.62/81.63 (E(f2(a1,a1),f8(a1,f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[2825,2])). % 81.62/81.63 cnf(2864,plain, % 81.62/81.63 (P5(f8(f2(a1,a1),f8(a1,a1)),f8(f2(a10,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[964,639,1063,1060,1515,1466,2085,2825,2,3,25,22,24])). % 81.62/81.63 cnf(2867,plain, % 81.62/81.63 (P3(f7(a1,f8(a1,a1)),f8(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[26,964,2701,130,1420,143,561,639,1063,1060,1515,1466,2085,2825,2840,2,3,25,22,24,69,99])). % 81.62/81.63 cnf(2879,plain, % 81.62/81.63 (E(f2(a1,a10),a1)), % 81.62/81.63 inference(scs_inference,[],[26,2853,41,42,43,44])). % 81.62/81.63 cnf(2899,plain, % 81.62/81.63 (~E(a13,f2(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[26,560,2860,2853,41,42,43,44,39,40,16,17,4,5,6,7,8,9,10,11,12,13,14,15,2])). % 81.62/81.63 cnf(2917,plain, % 81.62/81.63 (P1(f3(f7(a13,f8(a13,a13))))), % 81.62/81.63 inference(scs_inference,[],[26,560,2867,1019,2860,2855,2853,2841,2687,415,1783,143,414,130,41,42,43,44,39,40,16,17,4,5,6,7,8,9,10,11,12,13,14,15,2,61,38,62,37,21,18,23,3,22,72,73,45])). % 81.62/81.63 cnf(2919,plain, % 81.62/81.63 (P2(f3(f7(a13,f8(a13,a13))))), % 81.62/81.63 inference(scs_inference,[],[26,560,2867,1019,2860,2855,2853,2841,2687,415,1783,143,414,130,41,42,43,44,39,40,16,17,4,5,6,7,8,9,10,11,12,13,14,15,2,61,38,62,37,21,18,23,3,22,72,73,45,46])). % 81.62/81.63 cnf(2927,plain, % 81.62/81.63 (E(f7(f7(a1,a1),a1),f7(a1,f7(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,2843,560,2867,1019,2860,2855,2845,2853,2841,2687,415,1783,1390,951,143,527,414,130,41,42,43,44,39,40,16,17,4,5,6,7,8,9,10,11,12,13,14,15,2,61,38,62,37,21,18,23,3,22,72,73,45,46,66,81,82,91])). % 81.62/81.63 cnf(2933,plain, % 81.62/81.63 (E(f7(f2(a1,a1),f2(a1,a1)),f2(f7(a1,a1),a1))), % 81.62/81.63 inference(scs_inference,[],[26,2843,560,2867,1019,2860,2855,2845,2853,2841,2687,415,1783,1390,951,143,527,414,130,41,42,43,44,39,40,16,17,4,5,6,7,8,9,10,11,12,13,14,15,2,61,38,62,37,21,18,23,3,22,72,73,45,46,66,81,82,91,92,101,102])). % 81.62/81.63 cnf(2947,plain, % 81.62/81.63 (~E(f7(f2(a1,a1),a1),f7(a13,a1))), % 81.62/81.63 inference(scs_inference,[],[26,2843,560,2867,1019,2860,2855,2845,2853,2841,2687,2655,2630,415,970,601,1043,547,1783,1390,951,143,527,414,30,130,41,42,43,44,39,40,16,17,4,5,6,7,8,9,10,11,12,13,14,15,2,61,38,62,37,21,18,23,3,22,72,73,45,46,66,81,82,91,92,101,102,55,56,109,115,108,53,75])). % 81.62/81.63 cnf(2951,plain, % 81.62/81.63 (~E(f7(a1,f2(a1,a1)),f7(a1,a13))), % 81.62/81.63 inference(scs_inference,[],[26,2843,560,2867,1019,2860,2855,2845,2853,2841,2687,2655,2630,415,970,601,1043,547,1783,1390,951,143,527,414,30,130,41,42,43,44,39,40,16,17,4,5,6,7,8,9,10,11,12,13,14,15,2,61,38,62,37,21,18,23,3,22,72,73,45,46,66,81,82,91,92,101,102,55,56,109,115,108,53,75,57,74])). % 81.62/81.63 cnf(2953,plain, % 81.62/81.63 (P1(f8(f2(a1,a1),f2(a10,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,2843,560,2867,1019,2860,2582,2855,2845,2853,2841,2687,2655,2630,415,970,601,1043,1468,547,1783,1390,951,143,527,414,30,130,41,42,43,44,39,40,16,17,4,5,6,7,8,9,10,11,12,13,14,15,2,61,38,62,37,21,18,23,3,22,72,73,45,46,66,81,82,91,92,101,102,55,56,109,115,108,53,75,57,74,70])). % 81.62/81.63 cnf(2955,plain, % 81.62/81.63 (E(f7(f2(a10,a1),f2(a1,a1)),a1)), % 81.62/81.63 inference(scs_inference,[],[26,2843,560,2867,1019,2860,2582,2855,2845,2853,2841,2687,2655,2630,415,1407,970,601,1043,1468,547,1783,1390,951,143,527,414,30,130,41,42,43,44,39,40,16,17,4,5,6,7,8,9,10,11,12,13,14,15,2,61,38,62,37,21,18,23,3,22,72,73,45,46,66,81,82,91,92,101,102,55,56,109,115,108,53,75,57,74,70,79])). % 81.62/81.63 cnf(2965,plain, % 81.62/81.63 (~P3(a1,f7(a1,a13))), % 81.62/81.63 inference(scs_inference,[],[26,127,2843,560,2867,1019,2860,2582,2851,2852,2855,2845,2853,2723,2841,2687,2655,2630,535,415,417,1407,970,601,374,1043,1000,1468,279,547,1783,1390,951,143,527,414,30,130,28,41,42,43,44,39,40,16,17,4,5,6,7,8,9,10,11,12,13,14,15,2,61,38,62,37,21,18,23,3,22,72,73,45,46,66,81,82,91,92,101,102,55,56,109,115,108,53,75,57,74,70,79,67,117,69,93,99])). % 81.62/81.63 cnf(2980,plain, % 81.62/81.63 (E(f7(f8(a10,a10),a1),f8(a10,a10))), % 81.62/81.63 inference(scs_inference,[],[185,43])). % 81.62/81.63 cnf(2984,plain, % 81.62/81.63 (E(f7(a1,f8(a10,a10)),f8(a10,a10))), % 81.62/81.63 inference(scs_inference,[],[185,43,42,41])). % 81.62/81.63 cnf(2986,plain, % 81.62/81.63 (E(f2(f8(a10,a10),a10),f8(a10,a10))), % 81.62/81.63 inference(scs_inference,[],[185,43,42,41,44])). % 81.62/81.63 cnf(2992,plain, % 81.62/81.63 (E(f2(x29921,f2(a1,a10)),f2(x29921,a1))), % 81.62/81.63 inference(scs_inference,[],[2879,2953,185,43,42,41,44,39,16,17,5])). % 81.62/81.63 cnf(2993,plain, % 81.62/81.63 (E(f6(x29931,f2(a1,a10)),f6(x29931,a1))), % 81.62/81.63 inference(scs_inference,[],[2879,2953,185,43,42,41,44,39,16,17,5,15])). % 81.62/81.63 cnf(2994,plain, % 81.62/81.63 (E(f7(f2(a1,a10),x29941),f7(a1,x29941))), % 81.62/81.63 inference(scs_inference,[],[2879,2953,185,43,42,41,44,39,16,17,5,15,6])). % 81.62/81.63 cnf(3000,plain, % 81.62/81.63 (E(f6(f2(a1,a10),x30001),f6(a1,x30001))), % 81.62/81.63 inference(scs_inference,[],[2879,2953,185,43,42,41,44,39,16,17,5,15,6,12,47,40,14])). % 81.62/81.63 cnf(3002,plain, % 81.62/81.63 (E(f7(x30021,f2(a1,a10)),f7(x30021,a1))), % 81.62/81.63 inference(scs_inference,[],[2879,2953,185,43,42,41,44,39,16,17,5,15,6,12,47,40,14,9,7])). % 81.62/81.63 cnf(3004,plain, % 81.62/81.63 (E(f2(f2(a1,a10),x30041),f2(a1,x30041))), % 81.62/81.63 inference(scs_inference,[],[2879,2953,185,43,42,41,44,39,16,17,5,15,6,12,47,40,14,9,7,13,4])). % 81.62/81.63 cnf(3005,plain, % 81.62/81.63 (E(f8(x30051,f2(a1,a10)),f8(x30051,a1))), % 81.62/81.63 inference(scs_inference,[],[2879,2953,185,43,42,41,44,39,16,17,5,15,6,12,47,40,14,9,7,13,4,11])). % 81.62/81.63 cnf(3007,plain, % 81.62/81.63 (E(f8(f2(a1,a10),x30071),f8(a1,x30071))), % 81.62/81.63 inference(scs_inference,[],[2879,2953,185,43,42,41,44,39,16,17,5,15,6,12,47,40,14,9,7,13,4,11,8,10])). % 81.62/81.63 cnf(3011,plain, % 81.62/81.63 (P1(f7(f8(a10,a10),f8(a10,a10)))), % 81.62/81.63 inference(scs_inference,[],[624,2879,2953,2917,2919,185,43,42,41,44,39,16,17,5,15,6,12,47,40,14,9,7,13,4,11,8,10,2,38,61])). % 81.62/81.63 cnf(3013,plain, % 81.62/81.63 (P1(f2(f8(a10,a10),f8(a10,a10)))), % 81.62/81.63 inference(scs_inference,[],[624,2879,2953,2917,2919,185,43,42,41,44,39,16,17,5,15,6,12,47,40,14,9,7,13,4,11,8,10,2,38,61,62])). % 81.62/81.63 cnf(3018,plain, % 81.62/81.63 (~P3(a1,f7(f2(a1,a10),a13))), % 81.62/81.63 inference(scs_inference,[],[624,2965,2879,2953,2917,2919,950,185,43,42,41,44,39,16,17,5,15,6,12,47,40,14,9,7,13,4,11,8,10,2,38,61,62,37,21,23])). % 81.62/81.63 cnf(3019,plain, % 81.62/81.63 (E(f2(a1,a10),f8(f2(a1,a1),f2(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[624,2965,2879,2953,2917,2919,2662,950,185,43,42,41,44,39,16,17,5,15,6,12,47,40,14,9,7,13,4,11,8,10,2,38,61,62,37,21,23,3])). % 81.62/81.63 cnf(3020,plain, % 81.62/81.63 (~P3(f2(a1,a10),f7(a1,a13))), % 81.62/81.63 inference(scs_inference,[],[624,2965,2879,2953,2917,2919,2662,950,185,43,42,41,44,39,16,17,5,15,6,12,47,40,14,9,7,13,4,11,8,10,2,38,61,62,37,21,23,3,22])). % 81.62/81.63 cnf(3023,plain, % 81.62/81.63 (E(f2(a1,f6(a1,a1)),a1)), % 81.62/81.63 inference(scs_inference,[],[26,624,2965,2879,2953,2917,2919,2662,950,535,185,29,43,42,41,44,39,16,17,5,15,6,12,47,40,14,9,7,13,4,11,8,10,2,38,61,62,37,21,23,3,22,102,81])). % 81.62/81.63 cnf(3027,plain, % 81.62/81.63 (P5(a10,f3(f7(a13,f8(a13,a13))))), % 81.62/81.63 inference(scs_inference,[],[26,624,2965,2879,2953,2917,2919,2662,950,535,185,29,43,42,41,44,39,16,17,5,15,6,12,47,40,14,9,7,13,4,11,8,10,2,38,61,62,37,21,23,3,22,102,81,92,49])). % 81.62/81.63 cnf(3031,plain, % 81.62/81.63 (P1(f6(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[26,624,2965,2879,2953,2917,2919,2662,950,535,185,29,43,42,41,44,39,16,17,5,15,6,12,47,40,14,9,7,13,4,11,8,10,2,38,61,62,37,21,23,3,22,102,81,92,49,101,73])). % 81.62/81.63 cnf(3033,plain, % 81.62/81.63 (E(f7(a1,f5(a1,a1)),a1)), % 81.62/81.63 inference(scs_inference,[],[26,624,2965,2879,2953,2917,2919,2662,950,535,185,123,29,43,42,41,44,39,16,17,5,15,6,12,47,40,14,9,7,13,4,11,8,10,2,38,61,62,37,21,23,3,22,102,81,92,49,101,73,82])). % 81.62/81.63 cnf(3039,plain, % 81.62/81.63 (P3(f8(a10,a10),f2(f8(a10,a10),f8(a10,a10)))), % 81.62/81.63 inference(scs_inference,[],[26,624,2965,2879,2953,2917,2919,2662,950,416,535,374,185,123,29,28,43,42,41,44,39,16,17,5,15,6,12,47,40,14,9,7,13,4,11,8,10,2,38,61,62,37,21,23,3,22,102,81,92,49,101,73,82,91,72,107])). % 81.62/81.63 cnf(3043,plain, % 81.62/81.63 (~P5(f3(f7(a13,f8(a13,a13))),a10)), % 81.62/81.63 inference(scs_inference,[],[26,624,2965,2879,2953,2917,2919,2662,1392,2266,950,416,535,374,185,1390,123,29,27,28,43,42,41,44,39,16,17,5,15,6,12,47,40,14,9,7,13,4,11,8,10,2,38,61,62,37,21,23,3,22,102,81,92,49,101,73,82,91,72,107,79,69])). % 81.62/81.63 cnf(3047,plain, % 81.62/81.63 (E(a1,f8(f8(a10,a10),f8(a10,a10)))), % 81.62/81.63 inference(scs_inference,[],[26,624,2965,2879,2953,2917,2919,2827,2662,1392,2266,950,416,535,374,214,185,1468,1390,123,29,27,28,43,42,41,44,39,16,17,5,15,6,12,47,40,14,9,7,13,4,11,8,10,2,38,61,62,37,21,23,3,22,102,81,92,49,101,73,82,91,72,107,79,69,93,85])). % 81.62/81.63 cnf(3049,plain, % 81.62/81.63 (E(f8(a10,a10),f8(f7(f8(a10,a10),f8(a10,a10)),f8(a10,a10)))), % 81.62/81.63 inference(scs_inference,[],[26,624,2965,2879,2953,2917,2919,2827,2662,1392,2266,950,416,535,374,214,185,1468,1390,123,29,27,28,43,42,41,44,39,16,17,5,15,6,12,47,40,14,9,7,13,4,11,8,10,2,38,61,62,37,21,23,3,22,102,81,92,49,101,73,82,91,72,107,79,69,93,85,330])). % 81.62/81.63 cnf(3050,plain, % 81.62/81.63 (E(f8(a1,f2(a1,a10)),a1)), % 81.62/81.63 inference(scs_inference,[],[26,624,2965,2879,2953,2917,2919,2827,2662,1392,2266,950,416,535,374,214,185,1468,1390,123,29,27,28,43,42,41,44,39,16,17,5,15,6,12,47,40,14,9,7,13,4,11,8,10,2,38,61,62,37,21,23,3,22,102,81,92,49,101,73,82,91,72,107,79,69,93,85,330,146])). % 81.62/81.63 cnf(3059,plain, % 81.62/81.63 (P5(f8(f7(a1,a1),f8(a1,a1)),f2(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[26,624,2965,2879,2716,2953,2917,2919,2827,2838,2662,1392,2266,950,416,535,1398,1483,374,214,185,1468,981,1390,1394,561,951,527,123,29,130,27,28,43,42,41,44,39,16,17,5,15,6,12,47,40,14,9,7,13,4,11,8,10,2,38,61,62,37,21,23,3,22,102,81,92,49,101,73,82,91,72,107,79,69,93,85,330,146,66,109,115,108,53])). % 81.62/81.63 cnf(3063,plain, % 81.62/81.63 (P3(a1,f8(f2(a10,a1),f8(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,624,2965,2879,2716,2953,2917,2919,2827,2838,2798,2662,1392,2266,950,416,223,535,1398,1775,1483,374,214,1420,185,1468,981,224,1390,1394,561,951,527,123,29,130,27,28,43,42,41,44,39,16,17,5,15,6,12,47,40,14,9,7,13,4,11,8,10,2,38,61,62,37,21,23,3,22,102,81,92,49,101,73,82,91,72,107,79,69,93,85,330,146,66,109,115,108,53,117,84])). % 81.62/81.63 cnf(3065,plain, % 81.62/81.63 (P5(a1,f8(a1,f2(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,624,2965,2879,2716,2953,2641,2917,2919,2827,2838,2798,2662,2633,1392,2266,950,2629,416,223,535,1398,1775,1483,374,214,1420,185,1468,981,547,224,1390,1394,561,951,527,123,29,130,27,28,43,42,41,44,39,16,17,5,15,6,12,47,40,14,9,7,13,4,11,8,10,2,38,61,62,37,21,23,3,22,102,81,92,49,101,73,82,91,72,107,79,69,93,85,330,146,66,109,115,108,53,117,84,83])). % 81.62/81.63 cnf(3069,plain, % 81.62/81.63 (P5(f8(a10,a10),f7(f8(a10,a10),f8(a10,a10)))), % 81.62/81.63 inference(scs_inference,[],[3011,324])). % 81.62/81.63 cnf(3080,plain, % 81.62/81.63 (E(f2(f6(a1,a1),a1),a1)), % 81.62/81.63 inference(scs_inference,[],[3031,3011,43,44,39,41,42,40])). % 81.62/81.63 cnf(3083,plain, % 81.62/81.63 (E(f8(f2(a1,a10),a1),a1)), % 81.62/81.63 inference(scs_inference,[],[3031,3007,3011,3033,43,44,39,41,42,40,12,146])). % 81.62/81.63 cnf(3098,plain, % 81.62/81.63 (E(f8(x30981,f7(a1,f5(a1,a1))),f8(x30981,a1))), % 81.62/81.63 inference(scs_inference,[],[3031,3007,3011,3033,43,44,39,41,42,40,12,146,16,15,17,47,14,5,8,6,4,7,9,13,11])). % 81.62/81.63 cnf(3101,plain, % 81.62/81.63 (~E(a13,a10)), % 81.62/81.63 inference(scs_inference,[],[3031,3007,2947,3011,3033,31,30,43,44,39,41,42,40,12,146,16,15,17,47,14,5,8,6,4,7,9,13,11,10,2,38])). % 81.62/81.63 cnf(3105,plain, % 81.62/81.63 (P1(f2(f6(a1,a1),f6(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[3031,3007,2947,3011,3033,31,30,43,44,39,41,42,40,12,146,16,15,17,47,14,5,8,6,4,7,9,13,11,10,2,38,61,62])). % 81.62/81.63 cnf(3107,plain, % 81.62/81.63 (~E(a13,a1)), % 81.62/81.63 inference(scs_inference,[],[3031,3007,2947,3011,3033,31,30,43,44,39,41,42,40,12,146,16,15,17,47,14,5,8,6,4,7,9,13,11,10,2,38,61,62,37])). % 81.62/81.63 cnf(3110,plain, % 81.62/81.63 (~P3(f2(a1,a10),f7(f2(a1,a10),a13))), % 81.62/81.63 inference(scs_inference,[],[3020,3031,2994,3007,2947,3011,583,3033,31,30,43,44,39,41,42,40,12,146,16,15,17,47,14,5,8,6,4,7,9,13,11,10,2,38,61,62,37,21,23])). % 81.62/81.63 cnf(3112,plain, % 81.62/81.63 (~P3(f2(a10,f2(a1,a10)),f7(a13,f8(a13,a13)))), % 81.62/81.63 inference(scs_inference,[],[3020,3031,2992,2994,3007,2947,3011,583,3033,2849,31,30,43,44,39,41,42,40,12,146,16,15,17,47,14,5,8,6,4,7,9,13,11,10,2,38,61,62,37,21,23,22])). % 81.62/81.63 cnf(3114,plain, % 81.62/81.63 (~E(f7(a13,f8(a13,a13)),f2(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[3020,2899,3031,2992,2994,3007,2947,3011,583,3033,2849,31,413,30,43,44,39,41,42,40,12,146,16,15,17,47,14,5,8,6,4,7,9,13,11,10,2,38,61,62,37,21,23,22,3])). % 81.62/81.63 cnf(3115,plain, % 81.62/81.63 (P2(f3(a13))), % 81.62/81.63 inference(scs_inference,[],[3020,2899,3031,2992,2994,3007,2947,3011,583,3033,2849,31,413,30,43,44,39,41,42,40,12,146,16,15,17,47,14,5,8,6,4,7,9,13,11,10,2,38,61,62,37,21,23,22,3,46])). % 81.62/81.63 cnf(3117,plain, % 81.62/81.63 (P1(f3(a13))), % 81.62/81.63 inference(scs_inference,[],[3020,2899,3031,2992,2994,3007,2947,3011,583,3033,2849,31,413,30,43,44,39,41,42,40,12,146,16,15,17,47,14,5,8,6,4,7,9,13,11,10,2,38,61,62,37,21,23,22,3,46,45])). % 81.62/81.63 cnf(3135,plain, % 81.62/81.63 (~E(f7(a13,a13),a1)), % 81.62/81.63 inference(scs_inference,[],[26,3020,2899,3031,3059,2992,2994,3007,2947,3011,583,3033,3063,1897,2849,31,413,1420,981,527,951,30,27,43,44,39,41,42,40,12,146,16,15,17,47,14,5,8,6,4,7,9,13,11,10,2,38,61,62,37,21,23,22,3,46,45,81,102,73,101,82,92,91,72,55])). % 81.62/81.63 cnf(3139,plain, % 81.62/81.63 (~E(f2(a13,a13),a1)), % 81.62/81.63 inference(scs_inference,[],[26,3020,2899,3031,3059,2992,2994,3007,2947,3011,583,3033,3063,3043,1897,2849,31,2917,413,1420,981,527,951,30,27,43,44,39,41,42,40,12,146,16,15,17,47,14,5,8,6,4,7,9,13,11,10,2,38,61,62,37,21,23,22,3,46,45,81,102,73,101,82,92,91,72,55,53,57])). % 81.62/81.63 cnf(3144,plain, % 81.62/81.63 (E(f8(x31441,f2(a1,a10)),f8(x31441,a1))), % 81.62/81.63 inference(rename_variables,[],[3005])). % 81.62/81.63 cnf(3152,plain, % 81.62/81.63 (P3(f3(a13),a13)), % 81.62/81.63 inference(scs_inference,[],[26,3020,2899,3031,3059,2992,2994,3005,3007,2947,3011,583,3033,3063,3027,3043,1897,2849,1766,31,2917,413,355,1420,262,204,981,527,951,123,29,30,27,43,44,39,41,42,40,12,146,16,15,17,47,14,5,8,6,4,7,9,13,11,10,2,38,61,62,37,21,23,22,3,46,45,81,102,73,101,82,92,91,72,55,53,57,65,79,117,77,93,52])). % 81.62/81.63 cnf(3156,plain, % 81.62/81.63 (P3(f6(a1,a1),f2(f6(a1,a1),f6(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[26,3020,2899,3031,3059,2992,2994,3005,3007,2947,3011,583,3033,3063,3027,3043,1897,2849,1766,31,2917,413,355,1420,262,204,981,527,951,123,29,30,27,43,44,39,41,42,40,12,146,16,15,17,47,14,5,8,6,4,7,9,13,11,10,2,38,61,62,37,21,23,22,3,46,45,81,102,73,101,82,92,91,72,55,53,57,65,79,117,77,93,52,56,107])). % 81.62/81.63 cnf(3158,plain, % 81.62/81.63 (P5(f3(a13),a13)), % 81.62/81.63 inference(scs_inference,[],[26,3020,2899,3031,3059,2992,2994,3005,3007,2947,3011,583,3033,3063,3027,3043,1897,2849,1766,31,2917,413,355,1420,262,204,981,527,951,123,29,30,27,43,44,39,41,42,40,12,146,16,15,17,47,14,5,8,6,4,7,9,13,11,10,2,38,61,62,37,21,23,22,3,46,45,81,102,73,101,82,92,91,72,55,53,57,65,79,117,77,93,52,56,107,64])). % 81.62/81.63 cnf(3160,plain, % 81.62/81.63 (P1(f8(a1,f2(a1,a10)))), % 81.62/81.63 inference(scs_inference,[],[26,3020,2899,3031,3059,2992,2994,3005,3144,3007,2947,3011,583,3033,3063,3027,3043,1897,2849,1766,31,2917,413,355,1420,262,204,981,527,951,123,29,30,27,43,44,39,41,42,40,12,146,16,15,17,47,14,5,8,6,4,7,9,13,11,10,2,38,61,62,37,21,23,22,3,46,45,81,102,73,101,82,92,91,72,55,53,57,65,79,117,77,93,52,56,107,64,70])). % 81.62/81.63 cnf(3163,plain, % 81.62/81.63 (~E(f2(a13,a13),f2(a1,a13))), % 81.62/81.63 inference(scs_inference,[],[26,3020,2899,3031,3059,2992,2994,3005,3144,3007,2947,3011,583,3033,3063,3027,3043,1897,2849,1766,31,2917,413,355,1420,262,204,981,527,951,123,29,30,27,43,44,39,41,42,40,12,146,16,15,17,47,14,5,8,6,4,7,9,13,11,10,2,38,61,62,37,21,23,22,3,46,45,81,102,73,101,82,92,91,72,55,53,57,65,79,117,77,93,52,56,107,64,70,78])). % 81.62/81.63 cnf(3167,plain, % 81.62/81.63 (E(f7(f3(a13),a1),f3(a13))), % 81.62/81.63 inference(scs_inference,[],[3117,43])). % 81.62/81.63 cnf(3171,plain, % 81.62/81.63 (E(f2(a10,f3(a13)),f3(a13))), % 81.62/81.63 inference(scs_inference,[],[3117,43,41,42])). % 81.62/81.63 cnf(3175,plain, % 81.62/81.63 (E(f2(f3(a13),a10),f3(a13))), % 81.62/81.63 inference(scs_inference,[],[3117,43,41,42,39,44])). % 81.62/81.63 cnf(3177,plain, % 81.62/81.63 (E(f2(f3(a13),a1),a1)), % 81.62/81.63 inference(scs_inference,[],[3117,43,41,42,39,44,40])). % 81.62/81.63 cnf(3183,plain, % 81.62/81.63 (P5(f3(a13),f3(a13))), % 81.62/81.63 inference(scs_inference,[],[3117,3050,43,41,42,39,44,40,17,16,12,14,47])). % 81.62/81.63 cnf(3187,plain, % 81.62/81.63 (E(f2(x31871,f8(a1,f2(a1,a10))),f2(x31871,a1))), % 81.62/81.63 inference(scs_inference,[],[3117,3050,3098,43,41,42,39,44,40,17,16,12,14,47,146,5])). % 81.62/81.63 cnf(3193,plain, % 81.62/81.63 (E(f2(f8(a1,f2(a1,a10)),x31931),f2(a1,x31931))), % 81.62/81.63 inference(scs_inference,[],[3117,3050,3098,43,41,42,39,44,40,17,16,12,14,47,146,5,15,13,7,6,8,4])). % 81.62/81.63 cnf(3195,plain, % 81.62/81.63 (E(f8(x31951,f8(a1,f2(a1,a10))),f8(x31951,a1))), % 81.62/81.63 inference(scs_inference,[],[3117,3050,3098,43,41,42,39,44,40,17,16,12,14,47,146,5,15,13,7,6,8,4,9,11])). % 81.62/81.63 cnf(3196,plain, % 81.62/81.63 (E(f8(f8(a1,f2(a1,a10)),x31961),f8(a1,x31961))), % 81.62/81.63 inference(scs_inference,[],[3117,3050,3098,43,41,42,39,44,40,17,16,12,14,47,146,5,15,13,7,6,8,4,9,11,10])). % 81.62/81.63 cnf(3197,plain, % 81.62/81.63 (~E(a10,a13)), % 81.62/81.63 inference(scs_inference,[],[3101,3117,3050,3098,43,41,42,39,44,40,17,16,12,14,47,146,5,15,13,7,6,8,4,9,11,10,2])). % 81.62/81.63 cnf(3198,plain, % 81.62/81.63 (~E(f3(a13),a10)), % 81.62/81.63 inference(scs_inference,[],[3101,3115,3117,3050,3098,43,41,42,39,44,40,17,16,12,14,47,146,5,15,13,7,6,8,4,9,11,10,2,38])). % 81.62/81.63 cnf(3202,plain, % 81.62/81.63 (P1(f2(f3(a13),f3(a13)))), % 81.62/81.63 inference(scs_inference,[],[3101,3115,3117,3050,3098,43,41,42,39,44,40,17,16,12,14,47,146,5,15,13,7,6,8,4,9,11,10,2,38,61,62])). % 81.62/81.63 cnf(3204,plain, % 81.62/81.63 (~E(f3(a13),a1)), % 81.62/81.63 inference(scs_inference,[],[3101,3115,3117,3050,3098,43,41,42,39,44,40,17,16,12,14,47,146,5,15,13,7,6,8,4,9,11,10,2,38,61,62,37])). % 81.62/81.63 cnf(3207,plain, % 81.62/81.63 (~P3(f2(a10,f2(a1,a10)),a13)), % 81.62/81.63 inference(scs_inference,[],[3101,3115,3117,2672,3050,3112,3098,413,43,41,42,39,44,40,17,16,12,14,47,146,5,15,13,7,6,8,4,9,11,10,2,38,61,62,37,21,23])). % 81.62/81.63 cnf(3210,plain, % 81.62/81.63 (E(f7(f8(a10,a10),a1),f8(f7(f8(a10,a10),f8(a10,a10)),f8(a10,a10)))), % 81.62/81.63 inference(scs_inference,[],[3101,3115,3117,2980,3004,2672,3110,3050,3049,3112,3098,413,43,41,42,39,44,40,17,16,12,14,47,146,5,15,13,7,6,8,4,9,11,10,2,38,61,62,37,21,23,22,3])). % 81.62/81.63 cnf(3211,plain, % 81.62/81.63 (P2(f3(f3(a13)))), % 81.62/81.63 inference(scs_inference,[],[3101,3115,3117,2980,3004,2672,3110,3050,3049,3112,3098,413,43,41,42,39,44,40,17,16,12,14,47,146,5,15,13,7,6,8,4,9,11,10,2,38,61,62,37,21,23,22,3,46])). % 81.62/81.63 cnf(3219,plain, % 81.62/81.63 (P1(f3(f3(a13)))), % 81.62/81.63 inference(scs_inference,[],[3101,3115,3117,3152,2980,3004,2672,3110,3050,3049,3112,3098,413,30,27,43,41,42,39,44,40,17,16,12,14,47,146,5,15,13,7,6,8,4,9,11,10,2,38,61,62,37,21,23,22,3,46,81,102,73,45])). % 81.62/81.63 cnf(3227,plain, % 81.62/81.63 (P1(f5(f3(a13),f3(a13)))), % 81.62/81.63 inference(scs_inference,[],[26,3101,3107,3115,3117,3152,3158,2980,3004,2672,3110,3050,3049,3112,3098,413,30,27,43,41,42,39,44,40,17,16,12,14,47,146,5,15,13,7,6,8,4,9,11,10,2,38,61,62,37,21,23,22,3,46,81,102,73,45,101,66,82,72])). % 81.62/81.63 cnf(3235,plain, % 81.62/81.63 (~E(f7(a13,a1),a1)), % 81.62/81.63 inference(scs_inference,[],[26,3101,3107,3115,3117,3152,3158,2980,3004,2672,3110,3050,3049,3112,3098,413,30,27,43,41,42,39,44,40,17,16,12,14,47,146,5,15,13,7,6,8,4,9,11,10,2,38,61,62,37,21,23,22,3,46,81,102,73,45,101,66,82,72,92,91,55,56])). % 81.62/81.63 cnf(3237,plain, % 81.62/81.63 (P5(f8(f8(a10,a10),f8(a10,a10)),a1)), % 81.62/81.63 inference(scs_inference,[],[26,3101,3107,3115,3117,3152,3158,2980,3004,2672,3110,3050,3047,3049,3112,3098,225,413,30,27,43,41,42,39,44,40,17,16,12,14,47,146,5,15,13,7,6,8,4,9,11,10,2,38,61,62,37,21,23,22,3,46,81,102,73,45,101,66,82,72,92,91,55,56,53])). % 81.62/81.63 cnf(3245,plain, % 81.62/81.63 (~E(f2(a13,a13),f2(a13,a1))), % 81.62/81.63 inference(scs_inference,[],[26,3101,3107,3115,3117,3152,3158,2980,3004,2672,3019,3110,3050,3047,3049,3112,3098,529,225,413,527,30,27,43,41,42,39,44,40,17,16,12,14,47,146,5,15,13,7,6,8,4,9,11,10,2,38,61,62,37,21,23,22,3,46,81,102,73,45,101,66,82,72,92,91,55,56,53,116,110,79,77])). % 81.62/81.63 cnf(3247,plain, % 81.62/81.63 (E(f3(a13),a13)), % 81.62/81.63 inference(scs_inference,[],[26,3101,3107,3115,3117,3152,3158,2980,3004,2672,3019,3110,3050,3047,3049,3112,3098,529,225,31,413,527,30,27,43,41,42,39,44,40,17,16,12,14,47,146,5,15,13,7,6,8,4,9,11,10,2,38,61,62,37,21,23,22,3,46,81,102,73,45,101,66,82,72,92,91,55,56,53,116,110,79,77,63])). % 81.62/81.63 cnf(3258,plain, % 81.62/81.63 (E(f7(a1,f5(a1,a1)),f5(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[389,43,41])). % 81.62/81.63 cnf(3260,plain, % 81.62/81.63 (E(f2(f5(a1,a1),a10),f5(a1,a1))), % 81.62/81.63 inference(scs_inference,[],[389,43,41,44])). % 81.62/81.63 cnf(3270,plain, % 81.62/81.63 (E(f2(x32701,f3(a13)),f2(x32701,a13))), % 81.62/81.63 inference(scs_inference,[],[3247,3160,389,43,41,44,39,40,42,47,5])). % 81.62/81.63 cnf(3273,plain, % 81.62/81.63 (E(f3(f3(a13)),f3(a13))), % 81.62/81.63 inference(scs_inference,[],[3247,3160,389,43,41,44,39,40,42,47,5,16,14,17])). % 81.62/81.63 cnf(3274,plain, % 81.62/81.63 (E(f5(x32741,f3(a13)),f5(x32741,a13))), % 81.62/81.63 inference(scs_inference,[],[3247,3160,389,43,41,44,39,40,42,47,5,16,14,17,13])). % 81.62/81.63 cnf(3278,plain, % 81.62/81.63 (E(f7(f3(a13),x32781),f7(a13,x32781))), % 81.62/81.63 inference(scs_inference,[],[3247,3160,3195,389,43,41,44,39,40,42,47,5,16,14,17,13,146,12,6])). % 81.62/81.63 cnf(3279,plain, % 81.62/81.63 (E(f2(f3(a13),x32791),f2(a13,x32791))), % 81.62/81.63 inference(scs_inference,[],[3247,3160,3195,389,43,41,44,39,40,42,47,5,16,14,17,13,146,12,6,4])). % 81.62/81.63 cnf(3281,plain, % 81.62/81.63 (E(f7(x32811,f3(a13)),f7(x32811,a13))), % 81.62/81.63 inference(scs_inference,[],[3247,3160,3195,389,43,41,44,39,40,42,47,5,16,14,17,13,146,12,6,4,15,7])). % 81.62/81.63 cnf(3282,plain, % 81.62/81.63 (E(f9(f3(a13),x32821),f9(a13,x32821))), % 81.62/81.63 inference(scs_inference,[],[3247,3160,3195,389,43,41,44,39,40,42,47,5,16,14,17,13,146,12,6,4,15,7,8])). % 81.62/81.63 cnf(3287,plain, % 81.62/81.63 (~E(f3(f3(a13)),a10)), % 81.62/81.63 inference(scs_inference,[],[3135,3247,3160,3211,3219,3195,389,43,41,44,39,40,42,47,5,16,14,17,13,146,12,6,4,15,7,8,11,9,10,2,38])). % 81.62/81.63 cnf(3289,plain, % 81.62/81.63 (P1(f7(f5(a1,a1),f5(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[3135,3247,3160,3211,3219,3195,389,43,41,44,39,40,42,47,5,16,14,17,13,146,12,6,4,15,7,8,11,9,10,2,38,61])). % 81.62/81.63 cnf(3291,plain, % 81.62/81.63 (P1(f2(f5(a1,a1),f5(a1,a1)))), % 81.62/81.63 inference(scs_inference,[],[3135,3247,3160,3211,3219,3195,389,43,41,44,39,40,42,47,5,16,14,17,13,146,12,6,4,15,7,8,11,9,10,2,38,61,62])). % 81.62/81.63 cnf(3293,plain, % 81.62/81.63 (~E(f3(f3(a13)),a1)), % 81.62/81.63 inference(scs_inference,[],[3135,3247,3160,3211,3219,3195,389,43,41,44,39,40,42,47,5,16,14,17,13,146,12,6,4,15,7,8,11,9,10,2,38,61,62,37])). % 81.62/81.63 cnf(3296,plain, % 81.62/81.63 (~P3(f2(a10,f2(a1,a10)),f3(a13))), % 81.62/81.63 inference(scs_inference,[],[3135,3247,2070,3160,3211,3219,3207,3195,389,43,41,44,39,40,42,47,5,16,14,17,13,146,12,6,4,15,7,8,11,9,10,2,38,61,62,37,21,23])). % 81.62/81.63 cnf(3297,plain, % 81.62/81.63 (P3(a13,a13)), % 81.62/81.63 inference(scs_inference,[],[3135,3247,2070,3160,3211,3219,3207,3195,3152,389,43,41,44,39,40,42,47,5,16,14,17,13,146,12,6,4,15,7,8,11,9,10,2,38,61,62,37,21,23,22])). % 81.62/81.63 cnf(3301,plain, % 81.62/81.63 (P2(f3(f3(f3(a13))))), % 81.62/81.63 inference(scs_inference,[],[3197,3135,3247,2070,3160,3211,3219,3207,3195,1766,3152,389,220,951,43,41,44,39,40,42,47,5,16,14,17,13,146,12,6,4,15,7,8,11,9,10,2,38,61,62,37,21,23,22,3,81,46])). % 81.62/81.63 cnf(3305,plain, % 81.62/81.63 (P1(f3(f3(f3(a13))))), % 81.62/81.63 inference(scs_inference,[],[3197,3135,3247,2070,3160,3211,3219,3207,3195,1766,3152,389,220,951,28,43,41,44,39,40,42,47,5,16,14,17,13,146,12,6,4,15,7,8,11,9,10,2,38,61,62,37,21,23,22,3,81,46,102,45])). % 81.62/81.63 cnf(3307,plain, % 81.62/81.63 (P1(f6(f7(a1,a1),f7(a1,a1)))), % 81.62/81.64 inference(scs_inference,[],[3197,3135,3247,2070,3160,3211,3219,3207,3195,1766,3152,389,220,951,28,43,41,44,39,40,42,47,5,16,14,17,13,146,12,6,4,15,7,8,11,9,10,2,38,61,62,37,21,23,22,3,81,46,102,45,73])). % 81.62/81.64 cnf(3323,plain, % 81.62/81.64 (P5(a13,f3(a13))), % 81.62/81.64 inference(scs_inference,[],[26,3197,3135,3204,3247,3237,2070,3160,3211,3219,3207,3195,1766,3152,394,225,389,3117,220,951,30,28,43,41,44,39,40,42,47,5,16,14,17,13,146,12,6,4,15,7,8,11,9,10,2,38,61,62,37,21,23,22,3,81,46,102,45,73,101,66,91,72,82,92,55,53])). % 81.62/81.64 cnf(3325,plain, % 81.62/81.64 (E(a13,f2(a13,f9(a13,a13)))), % 81.62/81.64 inference(scs_inference,[],[26,3197,3135,3204,3247,3237,2070,3160,3211,3219,3207,3195,1766,3107,3152,394,225,389,3117,220,951,30,28,43,41,44,39,40,42,47,5,16,14,17,13,146,12,6,4,15,7,8,11,9,10,2,38,61,62,37,21,23,22,3,81,46,102,45,73,101,66,91,72,82,92,55,53,116])). % 81.62/81.64 cnf(3327,plain, % 81.62/81.64 (P1(f9(a13,a13))), % 81.62/81.64 inference(scs_inference,[],[26,3197,3135,3204,3247,3237,2070,3160,3211,3219,3207,3195,1766,3107,3152,394,225,389,3117,220,951,30,28,43,41,44,39,40,42,47,5,16,14,17,13,146,12,6,4,15,7,8,11,9,10,2,38,61,62,37,21,23,22,3,81,46,102,45,73,101,66,91,72,82,92,55,53,116,110])). % 81.62/81.64 cnf(3331,plain, % 81.62/81.64 (~E(f2(f3(a13),f3(a13)),a1)), % 81.62/81.64 inference(scs_inference,[],[26,3197,3135,3204,3247,3114,3237,2070,3160,3211,3219,3207,3195,1766,3107,3152,394,225,389,3117,220,951,527,414,30,28,43,41,44,39,40,42,47,5,16,14,17,13,146,12,6,4,15,7,8,11,9,10,2,38,61,62,37,21,23,22,3,81,46,102,45,73,101,66,91,72,82,92,55,53,116,110,75,57])). % 81.62/81.64 cnf(3333,plain, % 81.62/81.64 (P1(f7(f8(a10,a10),a1))), % 81.62/81.64 inference(scs_inference,[],[26,3197,3135,3204,3247,3114,3069,3237,2070,3160,3211,3219,3207,3195,3210,3011,1766,3107,3152,394,225,389,3117,185,220,951,527,414,30,28,43,41,44,39,40,42,47,5,16,14,17,13,146,12,6,4,15,7,8,11,9,10,2,38,61,62,37,21,23,22,3,81,46,102,45,73,101,66,91,72,82,92,55,53,116,110,75,57,70])). % 81.62/81.64 cnf(3349,plain, % 81.62/81.64 (P5(f5(a1,a1),f7(f5(a1,a1),f5(a1,a1)))), % 81.62/81.64 inference(scs_inference,[],[3289,470])). % 81.62/81.64 cnf(3350,plain, % 81.62/81.64 (E(f7(a1,f9(a13,a13)),f9(a13,a13))), % 81.62/81.64 inference(scs_inference,[],[3327,41])). % 81.62/81.64 cnf(3356,plain, % 81.62/81.64 (E(f2(f9(a13,a13),a10),f9(a13,a13))), % 81.62/81.64 inference(scs_inference,[],[3327,41,43,40,44])). % 81.62/81.64 cnf(3360,plain, % 81.62/81.64 (E(f2(a1,f9(a13,a13)),a1)), % 81.62/81.64 inference(scs_inference,[],[3327,41,43,40,44,42,39])). % 81.62/81.64 cnf(3362,plain, % 81.62/81.64 (P5(f9(a13,a13),f9(a13,a13))), % 81.62/81.64 inference(scs_inference,[],[3327,41,43,40,44,42,39,47])). % 81.62/81.64 cnf(3378,plain, % 81.62/81.64 (E(f8(x33781,f2(a1,f6(a1,a1))),f8(x33781,a1))), % 81.62/81.64 inference(scs_inference,[],[3327,3023,3196,41,43,40,44,42,39,47,146,5,14,17,13,16,6,15,8,12,9,4,7,11])). % 81.62/81.64 cnf(3379,plain, % 81.62/81.64 (E(f8(f2(a1,f6(a1,a1)),x33791),f8(a1,x33791))), % 81.62/81.64 inference(scs_inference,[],[3327,3023,3196,41,43,40,44,42,39,47,146,5,14,17,13,16,6,15,8,12,9,4,7,11,10])). % 81.62/81.64 cnf(3380,plain, % 81.62/81.64 (~E(f2(a1,a13),f2(a13,a13))), % 81.62/81.64 inference(scs_inference,[],[3163,3327,3023,3196,41,43,40,44,42,39,47,146,5,14,17,13,16,6,15,8,12,9,4,7,11,10,2])). % 81.62/81.64 cnf(3381,plain, % 81.62/81.64 (~E(f3(f3(f3(a13))),a10)), % 81.62/81.64 inference(scs_inference,[],[3163,3327,3023,3196,3301,3305,41,43,40,44,42,39,47,146,5,14,17,13,16,6,15,8,12,9,4,7,11,10,2,38])). % 81.62/81.64 cnf(3385,plain, % 81.62/81.64 (P1(f2(f9(a13,a13),f9(a13,a13)))), % 81.62/81.64 inference(scs_inference,[],[3163,3327,3023,3196,3301,3305,41,43,40,44,42,39,47,146,5,14,17,13,16,6,15,8,12,9,4,7,11,10,2,38,61,62])). % 81.62/81.64 cnf(3387,plain, % 81.62/81.64 (~E(f3(f3(f3(a13))),a1)), % 81.62/81.64 inference(scs_inference,[],[3163,3327,3023,3196,3301,3305,41,43,40,44,42,39,47,146,5,14,17,13,16,6,15,8,12,9,4,7,11,10,2,38,61,62,37])). % 81.62/81.64 cnf(3395,plain, % 81.62/81.64 (~P3(f2(a1,f6(a1,a1)),f7(f2(a1,a10),a13))), % 81.62/81.64 inference(scs_inference,[],[3163,3327,3323,2993,3000,3273,3296,3023,3018,3325,3196,3301,3305,528,41,43,40,44,42,39,47,146,5,14,17,13,16,6,15,8,12,9,4,7,11,10,2,38,61,62,37,21,23,24,3,22])). % 81.62/81.64 cnf(3396,plain, % 81.62/81.64 (E(f2(a13,f6(a13,a13)),a13)), % 81.62/81.64 inference(scs_inference,[],[3297,3163,3327,3323,2993,3000,3273,3296,3023,3018,3325,3196,3301,3305,528,30,41,43,40,44,42,39,47,146,5,14,17,13,16,6,15,8,12,9,4,7,11,10,2,38,61,62,37,21,23,24,3,22,81])). % 81.62/81.64 cnf(3400,plain, % 81.62/81.64 (P5(f3(a13),f2(f3(a13),f3(a13)))), % 81.62/81.64 inference(scs_inference,[],[3297,3163,3327,3323,2993,3000,3273,3296,3023,3105,3156,3018,3325,3196,3301,3305,528,3204,3031,3117,30,41,43,40,44,42,39,47,146,5,14,17,13,16,6,15,8,12,9,4,7,11,10,2,38,61,62,37,21,23,24,3,22,81,73,66])). % 81.62/81.64 cnf(3425,plain, % 81.62/81.64 (E(f7(f8(a11,a11),a1),f8(a11,a11))), % 81.62/81.64 inference(scs_inference,[],[279,43])). % 81.62/81.64 cnf(3453,plain, % 81.62/81.64 (E(f8(x34531,f7(f2(a10,a1),f2(a1,a1))),f8(x34531,a1))), % 81.62/81.64 inference(scs_inference,[],[3289,2955,3378,279,43,41,40,39,44,42,47,13,5,16,14,146,17,6,15,8,12,4,9,7,11])). % 81.62/81.64 cnf(3454,plain, % 81.62/81.64 (E(f8(f7(f2(a10,a1),f2(a1,a1)),x34541),f8(a1,x34541))), % 81.62/81.64 inference(scs_inference,[],[3289,2955,3378,279,43,41,40,39,44,42,47,13,5,16,14,146,17,6,15,8,12,4,9,7,11,10])). % 81.62/81.64 cnf(3455,plain, % 81.62/81.64 (~E(f2(a13,a1),f2(a13,a13))), % 81.62/81.64 inference(scs_inference,[],[3245,3289,2955,3378,279,43,41,40,39,44,42,47,13,5,16,14,146,17,6,15,8,12,4,9,7,11,10,2])). % 81.62/81.64 cnf(3456,plain, % 81.62/81.64 (P1(f7(f8(a11,a11),f8(a11,a11)))), % 81.62/81.64 inference(scs_inference,[],[3245,3289,2955,3378,279,43,41,40,39,44,42,47,13,5,16,14,146,17,6,15,8,12,4,9,7,11,10,2,61])). % 81.62/81.64 cnf(3458,plain, % 81.62/81.64 (P1(f2(f8(a11,a11),f8(a11,a11)))), % 81.62/81.64 inference(scs_inference,[],[3245,3289,2955,3378,279,43,41,40,39,44,42,47,13,5,16,14,146,17,6,15,8,12,4,9,7,11,10,2,61,62])). % 81.62/81.64 cnf(3463,plain, % 81.62/81.64 (~P3(f7(a1,f2(a1,a10)),f7(a13,f8(a13,a13)))), % 81.62/81.64 inference(scs_inference,[],[3245,3002,3278,3289,1591,2955,3378,2707,3115,279,1783,43,41,40,39,44,42,47,13,5,16,14,146,17,6,15,8,12,4,9,7,11,10,2,61,62,21,23,22])). % 81.62/81.64 cnf(3467,plain, % 81.62/81.64 (P5(a10,f3(f3(f3(a13))))), % 81.62/81.64 inference(scs_inference,[],[3380,3245,3002,3270,3278,3289,1591,2955,3378,3381,3387,2707,3305,3115,279,1783,43,41,40,39,44,42,47,13,5,16,14,146,17,6,15,8,12,4,9,7,11,10,2,61,62,21,23,22,3,49])). % 81.62/81.64 cnf(3488,plain, % 81.62/81.64 (E(f8(a11,a11),f8(f7(f8(a11,a11),f8(a11,a11)),f8(a11,a11)))), % 81.62/81.64 inference(scs_inference,[],[26,3183,3362,3380,3245,3002,3270,3278,3350,3039,3289,1591,3333,2955,3378,3381,3387,3013,2707,2742,2559,3282,2765,1392,3305,3297,3115,3204,3152,3327,3107,279,1783,185,1390,3117,561,527,951,30,130,43,41,40,39,44,42,47,13,5,16,14,146,17,6,15,8,12,4,9,7,11,10,2,61,62,21,23,22,3,49,81,73,72,82,108,79,71,80,93,387])). % 81.62/81.64 cnf(3491,plain, % 81.62/81.64 (~P2(f8(a1,f2(a1,a10)))), % 81.62/81.64 inference(scs_inference,[],[26,3183,3362,3380,3245,3002,3270,3278,3350,3039,3289,1591,3333,2955,3378,3381,3387,3013,2707,2742,2559,3282,2765,1392,3305,3297,3115,3160,3204,3152,3327,3107,3050,279,1783,185,1390,3117,561,527,951,30,130,43,41,40,39,44,42,47,13,5,16,14,146,17,6,15,8,12,4,9,7,11,10,2,61,62,21,23,22,3,49,81,73,72,82,108,79,71,80,93,387,38,37])). % 81.62/81.64 cnf(3493,plain, % 81.62/81.64 (P3(f3(f3(a13)),f3(a13))), % 81.62/81.64 inference(scs_inference,[],[26,3183,3362,3380,3245,3002,3270,3278,3350,3039,3289,1591,3333,2955,3378,3381,3387,3013,2707,2742,2559,3198,3282,2765,1392,3305,3297,3115,3160,3204,3152,3327,3107,3050,279,1783,185,1390,3117,561,527,951,30,130,43,41,40,39,44,42,47,13,5,16,14,146,17,6,15,8,12,4,9,7,11,10,2,61,62,21,23,22,3,49,81,73,72,82,108,79,71,80,93,387,38,37,52])). % 81.62/81.64 cnf(3503,plain, % 81.62/81.64 (P5(f8(a11,a11),f7(f8(a11,a11),f8(a11,a11)))), % 81.62/81.64 inference(scs_inference,[],[3456,383])). % 81.62/81.64 cnf(3504,plain, % 81.62/81.64 (P3(f8(a11,a11),f2(f8(a11,a11),f8(a11,a11)))), % 81.62/81.64 inference(scs_inference,[],[3458,385])). % 81.62/81.64 cnf(3511,plain, % 81.62/81.64 (E(f7(a1,f8(a12,a12)),f8(a12,a12))), % 81.62/81.64 inference(scs_inference,[],[3291,204,43,39,40,41])). % 81.62/81.64 cnf(3535,plain, % 81.62/81.64 (~E(a1,f2(a13,a13))), % 81.62/81.64 inference(scs_inference,[],[3139,3291,3083,3453,204,43,39,40,41,44,42,47,13,5,17,16,14,146,12,6,15,4,8,9,11,7,10,2])). % 81.62/81.64 cnf(3548,plain, % 81.62/81.64 (E(f2(f8(a1,a1),f6(f8(a1,a1),f8(a1,a1))),f8(a1,a1))), % 81.62/81.64 inference(scs_inference,[],[3139,3425,3281,3291,999,3287,3083,3488,3395,3193,3453,3293,3211,581,3219,204,130,43,39,40,41,44,42,47,13,5,17,16,14,146,12,6,15,4,8,9,11,7,10,2,62,61,21,23,22,3,49,81])). % 81.62/81.64 cnf(3550,plain, % 81.62/81.64 (P1(f6(a13,a13))), % 81.62/81.64 inference(scs_inference,[],[3139,3425,3281,3291,999,3287,3083,3488,3395,3193,3453,3293,3211,581,3297,3219,204,30,130,43,39,40,41,44,42,47,13,5,17,16,14,146,12,6,15,4,8,9,11,7,10,2,62,61,21,23,22,3,49,81,73])). % 81.62/81.64 cnf(3599,plain, % 81.62/81.64 (E(f2(f6(a13,a13),a1),a1)), % 81.62/81.64 inference(scs_inference,[],[3550,43,40])). % 81.62/81.64 cnf(3601,plain, % 81.62/81.64 (E(f2(a1,f6(a13,a13)),a1)), % 81.62/81.64 inference(scs_inference,[],[3550,43,40,39])). % 81.62/81.64 cnf(3616,plain, % 81.62/81.64 (E(f7(f2(a13,f6(a13,a13)),x36161),f7(a13,x36161))), % 81.62/81.64 inference(scs_inference,[],[3550,3396,43,40,39,44,42,41,47,17,13,14,16,5,6])). % 81.62/81.64 cnf(3621,plain, % 81.62/81.64 (E(f9(f2(a13,f6(a13,a13)),x36211),f9(a13,x36211))), % 81.62/81.64 inference(scs_inference,[],[3550,3396,3548,43,40,39,44,42,41,47,17,13,14,16,5,6,12,146,15,9,8])). % 81.62/81.64 cnf(3626,plain, % 81.62/81.64 (~E(a1,f7(a13,a1))), % 81.62/81.64 inference(scs_inference,[],[3550,3235,3396,3548,43,40,39,44,42,41,47,17,13,14,16,5,6,12,146,15,9,8,4,11,7,10,2])). % 81.62/81.64 cnf(3633,plain, % 81.62/81.64 (~P3(f2(f6(a1,a1),a1),a13)), % 81.62/81.64 inference(scs_inference,[],[3550,3235,3167,712,3396,3080,3548,127,3296,3115,43,40,39,44,42,41,47,17,13,14,16,5,6,12,146,15,9,8,4,11,7,10,2,62,61,21,23,22])). % 81.62/81.64 cnf(3635,plain, % 81.62/81.64 (E(f2(f3(a13),x36351),f2(a13,x36351))), % 81.62/81.64 inference(rename_variables,[],[3279])). % 81.62/81.64 cnf(3657,plain, % 81.62/81.64 (E(f5(a1,a1),f8(f7(f5(a1,a1),f5(a1,a1)),f5(a1,a1)))), % 81.62/81.64 inference(scs_inference,[],[26,3550,3455,3235,3258,3356,2984,3279,3635,3493,3167,222,3503,712,3400,3396,3080,3548,3456,127,3296,3349,3385,3293,3115,581,3289,3219,3297,3327,3107,279,389,224,3117,181,30,130,27,43,40,39,44,42,41,47,17,13,14,16,5,6,12,146,15,9,8,4,11,7,10,2,62,61,21,23,22,3,66,73,72,82,75,79,71,93,19,25,107,117])). % 81.62/81.64 cnf(3666,plain, % 81.62/81.64 (E(f2(f2(a10,a1),a10),f2(a10,a1))), % 81.62/81.64 inference(scs_inference,[],[3307,1390,40,43,44])). % 81.62/81.64 cnf(3689,plain, % 81.62/81.64 (E(f8(x36891,f2(f6(a13,a13),a1)),f8(x36891,a1))), % 81.62/81.64 inference(scs_inference,[],[3307,3599,3454,1390,40,43,44,39,41,42,47,13,5,16,12,17,14,146,6,15,9,8,4,11])). % 81.62/81.64 cnf(3693,plain, % 81.62/81.64 (P1(f2(f2(a10,a1),f2(a10,a1)))), % 81.62/81.64 inference(scs_inference,[],[2951,3307,3599,3454,1390,40,43,44,39,41,42,47,13,5,16,12,17,14,146,6,15,9,8,4,11,7,10,2,62])). % 81.62/81.64 cnf(3695,plain, % 81.62/81.64 (P1(f7(f2(a10,a1),f2(a10,a1)))), % 81.62/81.64 inference(scs_inference,[],[2951,3307,3599,3454,1390,40,43,44,39,41,42,47,13,5,16,12,17,14,146,6,15,9,8,4,11,7,10,2,62,61])). % 81.62/81.64 cnf(3700,plain, % 81.62/81.64 (~P3(f2(f6(a1,a1),f8(a1,f2(a1,a10))),a13)), % 81.62/81.64 inference(scs_inference,[],[2951,3307,3599,3633,3463,3187,3454,3616,1391,2919,1390,40,43,44,39,41,42,47,13,5,16,12,17,14,146,6,15,9,8,4,11,7,10,2,62,61,21,23,22])). % 81.62/81.64 cnf(3753,plain, % 81.62/81.64 (P1(f2(f8(a13,a13),f8(a13,a13)))), % 81.62/81.64 inference(scs_inference,[],[244,3693,3601,3379,338,40,39,43,44,41,42,47,13,16,12,5,146,17,14,6,15,8,9,11,4,7,10,2,62])). % 81.62/81.64 cnf(3755,plain, % 81.62/81.64 (P1(f7(f8(a13,a13),f8(a13,a13)))), % 81.62/81.64 inference(scs_inference,[],[244,3693,3601,3379,338,40,39,43,44,41,42,47,13,16,12,5,146,17,14,6,15,8,9,11,4,7,10,2,62,61])). % 81.62/81.64 cnf(3786,plain, % 81.62/81.64 (P5(f8(a13,a13),f7(f8(a13,a13),f8(a13,a13)))), % 81.62/81.64 inference(scs_inference,[],[3755,454])). % 81.62/81.64 cnf(3793,plain, % 81.62/81.64 (E(f7(a1,f7(a1,a1)),f7(a1,a1))), % 81.62/81.64 inference(scs_inference,[],[3695,951,40,39,44,41])). % 81.62/81.64 cnf(3893,plain, % 81.62/81.64 (E(f8(x38931,f2(a1,f9(a13,a13))),f8(x38931,a1))), % 81.62/81.64 inference(scs_inference,[],[3753,3360,3689,527,40,41,43,39,44,42,47,16,5,13,12,146,6,17,14,11])). % 81.62/81.64 cnf(3899,plain, % 81.62/81.64 (E(f8(f2(a1,f9(a13,a13)),x38991),f8(a1,x38991))), % 81.62/81.64 inference(scs_inference,[],[3753,3360,3689,527,40,41,43,39,44,42,47,16,5,13,12,146,6,17,14,11,9,8,15,4,7,10])). % 81.62/81.64 cnf(3903,plain, % 81.62/81.64 (P1(f7(f2(a1,a1),f2(a1,a1)))), % 81.62/81.64 inference(scs_inference,[],[335,3753,3360,3689,527,40,41,43,39,44,42,47,16,5,13,12,146,6,17,14,11,9,8,15,4,7,10,2,62,61])). % 81.62/81.64 cnf(3907,plain, % 81.62/81.64 (~P3(f7(a1,f7(a1,a1)),f7(a13,f8(a13,a13)))), % 81.62/81.64 inference(scs_inference,[],[3793,3171,335,3753,3491,3360,3689,3296,3115,1783,527,40,41,43,39,44,42,47,16,5,13,12,146,6,17,14,11,9,8,15,4,7,10,2,62,61,21,23,22])). % 81.62/81.64 cnf(3908,plain, % 81.62/81.64 (~E(f8(a1,f8(a1,a1)),f2(a13,a13))), % 81.62/81.64 inference(scs_inference,[],[3535,3793,3171,335,3753,3491,3360,3689,270,3296,3115,1783,527,40,41,43,39,44,42,47,16,5,13,12,146,6,17,14,11,9,8,15,4,7,10,2,62,61,21,23,22,3])). % 81.62/81.64 cnf(3909,plain, % 81.62/81.64 (P5(a10,f3(a13))), % 81.62/81.64 inference(scs_inference,[],[3535,3793,3171,335,3753,3491,3360,3689,270,3198,3296,3115,3204,1783,3117,527,40,41,43,39,44,42,47,16,5,13,12,146,6,17,14,11,9,8,15,4,7,10,2,62,61,21,23,22,3,49])). % 81.62/81.64 cnf(3921,plain, % 81.62/81.64 (~P5(f3(f3(f3(a13))),a10)), % 81.62/81.64 inference(scs_inference,[],[26,3535,3793,2986,3171,335,3504,3753,3491,3360,3689,3467,3458,270,3381,3198,1406,3296,3202,3331,3305,3115,306,3204,1783,279,1390,3117,527,181,27,40,41,43,39,44,42,47,16,5,13,12,146,6,17,14,11,9,8,15,4,7,10,2,62,61,21,23,22,3,49,66,73,82,72,79,69])). % 81.62/81.64 cnf(3940,plain, % 81.62/81.64 (E(f2(a12,a10),a12)), % 81.62/81.64 inference(scs_inference,[],[3755,29,40,44])). % 81.62/81.64 cnf(3942,plain, % 81.62/81.64 (E(f7(a1,a12),a12)), % 81.62/81.64 inference(scs_inference,[],[3755,29,40,44,41])). % 81.62/81.64 cnf(3969,plain, % 81.62/81.64 (P1(f2(a12,a12))), % 81.62/81.64 inference(scs_inference,[],[3908,3755,3177,3893,29,40,44,41,43,39,42,47,5,16,12,146,13,17,9,6,11,15,14,4,8,7,10,2,62])). % 81.62/81.64 cnf(3971,plain, % 81.62/81.64 (P1(f7(a12,a12))), % 81.62/81.64 inference(scs_inference,[],[3908,3755,3177,3893,29,40,44,41,43,39,42,47,5,16,12,146,13,17,9,6,11,15,14,4,8,7,10,2,62,61])). % 81.62/81.64 cnf(3976,plain, % 81.62/81.64 (~P3(f7(f7(a1,a1),a1),f7(a13,f8(a13,a13)))), % 81.62/81.64 inference(scs_inference,[],[3908,3755,3177,2927,3907,3893,3616,528,2919,29,40,44,41,43,39,42,47,5,16,12,146,13,17,9,6,11,15,14,4,8,7,10,2,62,61,21,23,22])). % 81.62/81.64 cnf(3988,plain, % 81.62/81.64 (E(f7(f2(a10,a1),a1),f8(a1,a1))), % 81.62/81.64 inference(scs_inference,[],[26,3909,3908,3260,3755,3786,3903,3065,3177,2933,2927,3907,3893,2073,3657,3616,2633,528,1419,2919,214,185,772,338,1390,3117,29,130,27,40,44,41,43,39,42,47,5,16,12,146,13,17,9,6,11,15,14,4,8,7,10,2,62,61,21,23,22,3,82,72,115,109,53,79])). % 81.62/81.64 cnf(3994,plain, % 81.62/81.64 (~P1(f2(a11,a11))+P3(a13,a11)), % 81.62/81.64 inference(scs_inference,[],[26,3909,3908,3260,3755,3786,3903,3065,3177,2933,2927,3907,3893,2864,2725,2073,2840,3657,3616,2633,528,1419,2919,214,1420,185,772,338,1390,3117,561,29,130,27,40,44,41,43,39,42,47,5,16,12,146,13,17,9,6,11,15,14,4,8,7,10,2,62,61,21,23,22,3,82,72,115,109,53,79,69,93,662])). % 81.62/81.64 cnf(4006,plain, % 81.62/81.64 (P1(f2(a11,a11))), % 81.62/81.64 inference(scs_inference,[],[3969,134])). % 81.62/81.64 cnf(4007,plain, % 81.62/81.64 (P3(a13,f2(a11,a11))+~P1(f2(a11,a11))), % 81.62/81.64 inference(scs_inference,[],[3969,260])). % 81.62/81.64 cnf(4008,plain, % 81.62/81.64 (P5(a12,f7(a12,a12))), % 81.62/81.64 inference(scs_inference,[],[3971,347])). % 81.62/81.64 cnf(4051,plain, % 81.62/81.64 (~E(f8(f8(a1,a1),f8(a1,a1)),f7(a13,a1))), % 81.62/81.64 inference(scs_inference,[],[3969,3626,3940,3988,3666,3175,3274,2854,1449,3227,241,2849,3296,415,40,43,44,39,41,42,47,16,12,5,17,13,146,9,6,11,14,15,4,8,7,10,2,62,61,18,21,23,22,3])). % 81.62/81.64 cnf(4096,plain, % 81.62/81.64 (P3(a13,a11)), % 81.62/81.64 inference(scs_inference,[],[4006,3994])). % 81.62/81.64 cnf(4150,plain, % 81.62/81.64 (P3(a13,f2(a11,a11))), % 81.62/81.64 inference(scs_inference,[],[26,3971,4008,4006,3942,3511,4051,3976,3899,3621,3700,3921,34,1391,3278,3301,3305,261,3152,3204,193,3117,29,30,27,28,40,42,44,43,41,39,47,16,12,5,13,17,6,146,9,4,15,14,8,11,7,10,2,62,61,21,23,22,3,82,72,53,74,79,71,4007])). % 81.62/81.64 cnf(4197,plain, % 81.62/81.64 ($false), % 81.62/81.64 inference(scs_inference,[],[4096,4150,76]), % 81.62/81.64 ['proof']). % 81.62/81.64 % SZS output end Proof % 81.62/81.64 % Total time :80.940000s %------------------------------------------------------------------------------