%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM523+3 : 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 : n001.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 73.74s 73.76s % Output : CNFRefutation 73.82s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.14 % Problem : NUM523+3 : TPTP v8.2.0. Released v4.0.0. % 0.09/0.14 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.14/0.36 % Computer : n001.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 300 % 0.14/0.36 % DateTime : Sat Jun 22 18:57:09 EDT 2024 % 0.14/0.36 % CPUTime : % 0.54/0.62 start to proof:theBenchmark % 73.67/73.74 %------------------------------------------- % 73.67/73.74 % File :CSE---1.7 % 73.67/73.74 % Problem :theBenchmark % 73.67/73.74 % Transform :cnf % 73.67/73.74 % Format :tptp:raw % 73.67/73.74 % Command :java -jar mcs_scs.jar %d %s % 73.67/73.74 % 73.67/73.74 % Result :Theorem 73.040000s % 73.67/73.74 % Output :CNFRefutation 73.040000s % 73.67/73.74 %------------------------------------------- % 73.74/73.75 %------------------------------------------------------------------------------ % 73.74/73.75 % File : NUM523+3 : TPTP v8.2.0. Released v4.0.0. % 73.74/73.75 % Domain : Number Theory % 73.74/73.75 % Problem : Square root of a prime is irrational 15_01, 02 expansion % 73.74/73.75 % Version : Especial. % 73.74/73.75 % English : % 73.74/73.75 % 73.74/73.75 % Refs : [LPV06] Lyaletski et al. (2006), SAD as a Mathematical Assista % 73.74/73.75 % : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 73.74/73.75 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 73.74/73.75 % Source : [Pas08] % 73.74/73.75 % Names : primes_15_01.02 [Pas08] % 73.74/73.75 % 73.74/73.75 % Status : Theorem % 73.74/73.75 % Rating : 0.36 v8.2.0, 0.39 v8.1.0, 0.36 v7.5.0, 0.38 v7.4.0, 0.33 v7.3.0, 0.34 v7.2.0, 0.28 v7.1.0, 0.30 v6.4.0, 0.38 v6.3.0, 0.29 v6.2.0, 0.44 v6.1.0, 0.53 v6.0.0, 0.43 v5.5.0, 0.56 v5.4.0, 0.57 v5.3.0, 0.59 v5.2.0, 0.50 v5.1.0, 0.52 v5.0.0, 0.54 v4.1.0, 0.57 v4.0.1, 0.78 v4.0.0 % 73.74/73.75 % Syntax : Number of formulae : 44 ( 2 unt; 5 def) % 73.74/73.75 % Number of atoms : 227 ( 74 equ) % 73.74/73.75 % Maximal formula atoms : 16 ( 5 avg) % 73.74/73.75 % Number of connectives : 212 ( 29 ~; 14 |; 98 &) % 73.74/73.75 % ( 5 <=>; 66 =>; 0 <=; 0 <~>) % 73.74/73.75 % Maximal formula depth : 16 ( 6 avg) % 73.74/73.75 % Maximal term depth : 3 ( 1 avg) % 73.74/73.75 % Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty) % 73.74/73.75 % Number of functors : 9 ( 9 usr; 5 con; 0-2 aty) % 73.74/73.75 % Number of variables : 94 ( 87 !; 7 ?) % 73.74/73.75 % SPC : FOF_THM_RFO_SEQ % 73.74/73.75 % 73.74/73.75 % Comments : Problem generated by the SAD system [VLP07] % 73.74/73.75 %------------------------------------------------------------------------------ % 73.74/73.75 fof(mNatSort,axiom, % 73.74/73.75 ! [W0] : % 73.74/73.75 ( aNaturalNumber0(W0) % 73.74/73.75 => $true ) ). % 73.74/73.75 % 73.74/73.75 fof(mSortsC,axiom, % 73.74/73.75 aNaturalNumber0(sz00) ). % 73.74/73.75 % 73.74/73.75 fof(mSortsC_01,axiom, % 73.74/73.75 ( aNaturalNumber0(sz10) % 73.74/73.75 & sz10 != sz00 ) ). % 73.74/73.75 % 73.74/73.75 fof(mSortsB,axiom, % 73.74/73.75 ! [W0,W1] : % 73.74/73.75 ( ( aNaturalNumber0(W0) % 73.74/73.75 & aNaturalNumber0(W1) ) % 73.74/73.75 => aNaturalNumber0(sdtpldt0(W0,W1)) ) ). % 73.74/73.75 % 73.74/73.75 fof(mSortsB_02,axiom, % 73.74/73.75 ! [W0,W1] : % 73.74/73.75 ( ( aNaturalNumber0(W0) % 73.74/73.75 & aNaturalNumber0(W1) ) % 73.74/73.75 => aNaturalNumber0(sdtasdt0(W0,W1)) ) ). % 73.74/73.75 % 73.74/73.75 fof(mAddComm,axiom, % 73.74/73.75 ! [W0,W1] : % 73.74/73.75 ( ( aNaturalNumber0(W0) % 73.74/73.75 & aNaturalNumber0(W1) ) % 73.74/73.75 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 73.74/73.75 % 73.74/73.75 fof(mAddAsso,axiom, % 73.74/73.75 ! [W0,W1,W2] : % 73.74/73.75 ( ( aNaturalNumber0(W0) % 73.74/73.75 & aNaturalNumber0(W1) % 73.74/73.75 & aNaturalNumber0(W2) ) % 73.74/73.75 => sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) ). % 73.74/73.75 % 73.74/73.75 fof(m_AddZero,axiom, % 73.74/73.75 ! [W0] : % 73.74/73.75 ( aNaturalNumber0(W0) % 73.74/73.75 => ( sdtpldt0(W0,sz00) = W0 % 73.74/73.75 & W0 = sdtpldt0(sz00,W0) ) ) ). % 73.74/73.75 % 73.74/73.75 fof(mMulComm,axiom, % 73.74/73.75 ! [W0,W1] : % 73.74/73.75 ( ( aNaturalNumber0(W0) % 73.74/73.75 & aNaturalNumber0(W1) ) % 73.74/73.75 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 73.74/73.75 % 73.74/73.75 fof(mMulAsso,axiom, % 73.74/73.75 ! [W0,W1,W2] : % 73.74/73.75 ( ( aNaturalNumber0(W0) % 73.74/73.75 & aNaturalNumber0(W1) % 73.74/73.75 & aNaturalNumber0(W2) ) % 73.74/73.75 => sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) ). % 73.74/73.75 % 73.74/73.75 fof(m_MulUnit,axiom, % 73.74/73.75 ! [W0] : % 73.74/73.75 ( aNaturalNumber0(W0) % 73.74/73.75 => ( sdtasdt0(W0,sz10) = W0 % 73.74/73.75 & W0 = sdtasdt0(sz10,W0) ) ) ). % 73.74/73.75 % 73.74/73.75 fof(m_MulZero,axiom, % 73.74/73.75 ! [W0] : % 73.74/73.75 ( aNaturalNumber0(W0) % 73.74/73.75 => ( sdtasdt0(W0,sz00) = sz00 % 73.74/73.75 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 73.74/73.75 % 73.74/73.75 fof(mAMDistr,axiom, % 73.74/73.75 ! [W0,W1,W2] : % 73.74/73.75 ( ( aNaturalNumber0(W0) % 73.74/73.75 & aNaturalNumber0(W1) % 73.74/73.75 & aNaturalNumber0(W2) ) % 73.74/73.75 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 73.74/73.75 & sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ). % 73.74/73.75 % 73.74/73.75 fof(mAddCanc,axiom, % 73.74/73.75 ! [W0,W1,W2] : % 73.74/73.75 ( ( aNaturalNumber0(W0) % 73.74/73.75 & aNaturalNumber0(W1) % 73.74/73.75 & aNaturalNumber0(W2) ) % 73.74/73.75 => ( ( sdtpldt0(W0,W1) = sdtpldt0(W0,W2) % 73.74/73.75 | sdtpldt0(W1,W0) = sdtpldt0(W2,W0) ) % 73.74/73.75 => W1 = W2 ) ) ). % 73.74/73.75 % 73.74/73.75 fof(mMulCanc,axiom, % 73.74/73.75 ! [W0] : % 73.74/73.75 ( aNaturalNumber0(W0) % 73.74/73.75 => ( W0 != sz00 % 73.74/73.75 => ! [W1,W2] : % 73.74/73.75 ( ( aNaturalNumber0(W1) % 73.74/73.75 & aNaturalNumber0(W2) ) % 73.74/73.75 => ( ( sdtasdt0(W0,W1) = sdtasdt0(W0,W2) % 73.74/73.75 | sdtasdt0(W1,W0) = sdtasdt0(W2,W0) ) % 73.74/73.75 => W1 = W2 ) ) ) ) ). % 73.74/73.75 % 73.74/73.75 fof(mZeroAdd,axiom, % 73.74/73.75 ! [W0,W1] : % 73.74/73.75 ( ( aNaturalNumber0(W0) % 73.74/73.75 & aNaturalNumber0(W1) ) % 73.74/73.75 => ( sdtpldt0(W0,W1) = sz00 % 73.74/73.75 => ( W0 = sz00 % 73.74/73.76 & W1 = sz00 ) ) ) ). % 73.74/73.76 % 73.74/73.76 fof(mZeroMul,axiom, % 73.74/73.76 ! [W0,W1] : % 73.74/73.76 ( ( aNaturalNumber0(W0) % 73.74/73.76 & aNaturalNumber0(W1) ) % 73.74/73.76 => ( sdtasdt0(W0,W1) = sz00 % 73.74/73.76 => ( W0 = sz00 % 73.74/73.76 | W1 = sz00 ) ) ) ). % 73.74/73.76 % 73.74/73.76 fof(mDefLE,definition, % 73.74/73.76 ! [W0,W1] : % 73.74/73.76 ( ( aNaturalNumber0(W0) % 73.74/73.76 & aNaturalNumber0(W1) ) % 73.74/73.76 => ( sdtlseqdt0(W0,W1) % 73.74/73.76 <=> ? [W2] : % 73.74/73.76 ( aNaturalNumber0(W2) % 73.74/73.76 & sdtpldt0(W0,W2) = W1 ) ) ) ). % 73.74/73.76 % 73.74/73.76 fof(mDefDiff,definition, % 73.74/73.76 ! [W0,W1] : % 73.74/73.76 ( ( aNaturalNumber0(W0) % 73.74/73.76 & aNaturalNumber0(W1) ) % 73.74/73.76 => ( sdtlseqdt0(W0,W1) % 73.74/73.76 => ! [W2] : % 73.74/73.76 ( W2 = sdtmndt0(W1,W0) % 73.74/73.76 <=> ( aNaturalNumber0(W2) % 73.74/73.76 & sdtpldt0(W0,W2) = W1 ) ) ) ) ). % 73.74/73.76 % 73.74/73.76 fof(mLERefl,axiom, % 73.74/73.76 ! [W0] : % 73.74/73.76 ( aNaturalNumber0(W0) % 73.74/73.76 => sdtlseqdt0(W0,W0) ) ). % 73.74/73.76 % 73.74/73.76 fof(mLEAsym,axiom, % 73.74/73.76 ! [W0,W1] : % 73.74/73.76 ( ( aNaturalNumber0(W0) % 73.74/73.76 & aNaturalNumber0(W1) ) % 73.74/73.76 => ( ( sdtlseqdt0(W0,W1) % 73.74/73.76 & sdtlseqdt0(W1,W0) ) % 73.74/73.76 => W0 = W1 ) ) ). % 73.74/73.76 % 73.74/73.76 fof(mLETran,axiom, % 73.74/73.76 ! [W0,W1,W2] : % 73.74/73.76 ( ( aNaturalNumber0(W0) % 73.74/73.76 & aNaturalNumber0(W1) % 73.74/73.76 & aNaturalNumber0(W2) ) % 73.74/73.76 => ( ( sdtlseqdt0(W0,W1) % 73.74/73.76 & sdtlseqdt0(W1,W2) ) % 73.74/73.76 => sdtlseqdt0(W0,W2) ) ) ). % 73.74/73.76 % 73.74/73.76 fof(mLETotal,axiom, % 73.74/73.76 ! [W0,W1] : % 73.74/73.76 ( ( aNaturalNumber0(W0) % 73.74/73.76 & aNaturalNumber0(W1) ) % 73.74/73.76 => ( sdtlseqdt0(W0,W1) % 73.74/73.76 | ( W1 != W0 % 73.74/73.76 & sdtlseqdt0(W1,W0) ) ) ) ). % 73.74/73.76 % 73.74/73.76 fof(mMonAdd,axiom, % 73.74/73.76 ! [W0,W1] : % 73.74/73.76 ( ( aNaturalNumber0(W0) % 73.74/73.76 & aNaturalNumber0(W1) ) % 73.74/73.76 => ( ( W0 != W1 % 73.74/73.76 & sdtlseqdt0(W0,W1) ) % 73.74/73.76 => ! [W2] : % 73.74/73.76 ( aNaturalNumber0(W2) % 73.74/73.76 => ( sdtpldt0(W2,W0) != sdtpldt0(W2,W1) % 73.74/73.76 & sdtlseqdt0(sdtpldt0(W2,W0),sdtpldt0(W2,W1)) % 73.74/73.76 & sdtpldt0(W0,W2) != sdtpldt0(W1,W2) % 73.74/73.76 & sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W2)) ) ) ) ) ). % 73.74/73.76 % 73.74/73.76 fof(mMonMul,axiom, % 73.74/73.76 ! [W0,W1,W2] : % 73.74/73.76 ( ( aNaturalNumber0(W0) % 73.74/73.76 & aNaturalNumber0(W1) % 73.74/73.76 & aNaturalNumber0(W2) ) % 73.74/73.76 => ( ( W0 != sz00 % 73.74/73.76 & W1 != W2 % 73.74/73.76 & sdtlseqdt0(W1,W2) ) % 73.74/73.76 => ( sdtasdt0(W0,W1) != sdtasdt0(W0,W2) % 73.74/73.76 & sdtlseqdt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 73.74/73.76 & sdtasdt0(W1,W0) != sdtasdt0(W2,W0) % 73.74/73.76 & sdtlseqdt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ) ). % 73.74/73.76 % 73.74/73.76 fof(mLENTr,axiom, % 73.74/73.76 ! [W0] : % 73.74/73.76 ( aNaturalNumber0(W0) % 73.74/73.76 => ( W0 = sz00 % 73.74/73.76 | W0 = sz10 % 73.74/73.76 | ( sz10 != W0 % 73.74/73.76 & sdtlseqdt0(sz10,W0) ) ) ) ). % 73.74/73.76 % 73.74/73.76 fof(mMonMul2,axiom, % 73.74/73.76 ! [W0,W1] : % 73.74/73.76 ( ( aNaturalNumber0(W0) % 73.74/73.76 & aNaturalNumber0(W1) ) % 73.74/73.76 => ( W0 != sz00 % 73.74/73.76 => sdtlseqdt0(W1,sdtasdt0(W1,W0)) ) ) ). % 73.74/73.76 % 73.74/73.76 fof(mIH,axiom, % 73.74/73.76 ! [W0,W1] : % 73.74/73.76 ( ( aNaturalNumber0(W0) % 73.74/73.76 & aNaturalNumber0(W1) ) % 73.74/73.76 => ( iLess0(W0,W1) % 73.74/73.76 => $true ) ) ). % 73.74/73.76 % 73.74/73.76 fof(mIH_03,axiom, % 73.74/73.76 ! [W0,W1] : % 73.74/73.76 ( ( aNaturalNumber0(W0) % 73.74/73.76 & aNaturalNumber0(W1) ) % 73.74/73.76 => ( ( W0 != W1 % 73.74/73.76 & sdtlseqdt0(W0,W1) ) % 73.74/73.76 => iLess0(W0,W1) ) ) ). % 73.74/73.76 % 73.74/73.76 fof(mDefDiv,definition, % 73.74/73.76 ! [W0,W1] : % 73.74/73.76 ( ( aNaturalNumber0(W0) % 73.74/73.76 & aNaturalNumber0(W1) ) % 73.74/73.76 => ( doDivides0(W0,W1) % 73.74/73.76 <=> ? [W2] : % 73.74/73.76 ( aNaturalNumber0(W2) % 73.74/73.76 & W1 = sdtasdt0(W0,W2) ) ) ) ). % 73.74/73.76 % 73.74/73.76 fof(mDefQuot,definition, % 73.74/73.76 ! [W0,W1] : % 73.74/73.76 ( ( aNaturalNumber0(W0) % 73.74/73.76 & aNaturalNumber0(W1) ) % 73.74/73.76 => ( ( W0 != sz00 % 73.74/73.76 & doDivides0(W0,W1) ) % 73.74/73.76 => ! [W2] : % 73.74/73.76 ( W2 = sdtsldt0(W1,W0) % 73.74/73.76 <=> ( aNaturalNumber0(W2) % 73.74/73.76 & W1 = sdtasdt0(W0,W2) ) ) ) ) ). % 73.74/73.76 % 73.74/73.76 fof(mDivTrans,axiom, % 73.74/73.76 ! [W0,W1,W2] : % 73.74/73.76 ( ( aNaturalNumber0(W0) % 73.74/73.76 & aNaturalNumber0(W1) % 73.74/73.76 & aNaturalNumber0(W2) ) % 73.74/73.76 => ( ( doDivides0(W0,W1) % 73.74/73.76 & doDivides0(W1,W2) ) % 73.74/73.76 => doDivides0(W0,W2) ) ) ). % 73.74/73.76 % 73.74/73.76 fof(mDivSum,axiom, % 73.74/73.76 ! [W0,W1,W2] : % 73.74/73.76 ( ( aNaturalNumber0(W0) % 73.74/73.76 & aNaturalNumber0(W1) % 73.74/73.76 & aNaturalNumber0(W2) ) % 73.74/73.76 => ( ( doDivides0(W0,W1) % 73.74/73.76 & doDivides0(W0,W2) ) % 73.74/73.76 => doDivides0(W0,sdtpldt0(W1,W2)) ) ) ). % 73.74/73.76 % 73.74/73.76 fof(mDivMin,axiom, % 73.74/73.76 ! [W0,W1,W2] : % 73.74/73.76 ( ( aNaturalNumber0(W0) % 73.74/73.76 & aNaturalNumber0(W1) % 73.74/73.76 & aNaturalNumber0(W2) ) % 73.74/73.76 => ( ( doDivides0(W0,W1) % 73.74/73.76 & doDivides0(W0,sdtpldt0(W1,W2)) ) % 73.74/73.76 => doDivides0(W0,W2) ) ) ). % 73.74/73.76 % 73.74/73.76 fof(mDivLE,axiom, % 73.74/73.76 ! [W0,W1] : % 73.74/73.76 ( ( aNaturalNumber0(W0) % 73.74/73.76 & aNaturalNumber0(W1) ) % 73.74/73.76 => ( ( doDivides0(W0,W1) % 73.74/73.76 & W1 != sz00 ) % 73.74/73.76 => sdtlseqdt0(W0,W1) ) ) ). % 73.74/73.76 % 73.74/73.76 fof(mDivAsso,axiom, % 73.74/73.76 ! [W0,W1] : % 73.74/73.76 ( ( aNaturalNumber0(W0) % 73.74/73.76 & aNaturalNumber0(W1) ) % 73.74/73.76 => ( ( W0 != sz00 % 73.74/73.76 & doDivides0(W0,W1) ) % 73.74/73.76 => ! [W2] : % 73.74/73.76 ( aNaturalNumber0(W2) % 73.74/73.76 => sdtasdt0(W2,sdtsldt0(W1,W0)) = sdtsldt0(sdtasdt0(W2,W1),W0) ) ) ) ). % 73.74/73.76 % 73.74/73.76 fof(mDefPrime,definition, % 73.74/73.76 ! [W0] : % 73.74/73.76 ( aNaturalNumber0(W0) % 73.74/73.76 => ( isPrime0(W0) % 73.74/73.76 <=> ( W0 != sz00 % 73.74/73.76 & W0 != sz10 % 73.74/73.76 & ! [W1] : % 73.74/73.76 ( ( aNaturalNumber0(W1) % 73.74/73.76 & doDivides0(W1,W0) ) % 73.74/73.76 => ( W1 = sz10 % 73.74/73.76 | W1 = W0 ) ) ) ) ) ). % 73.74/73.76 % 73.74/73.76 fof(mPrimDiv,axiom, % 73.74/73.76 ! [W0] : % 73.74/73.76 ( ( aNaturalNumber0(W0) % 73.74/73.76 & W0 != sz00 % 73.74/73.76 & W0 != sz10 ) % 73.74/73.76 => ? [W1] : % 73.74/73.76 ( aNaturalNumber0(W1) % 73.74/73.76 & doDivides0(W1,W0) % 73.74/73.76 & isPrime0(W1) ) ) ). % 73.74/73.76 % 73.74/73.76 fof(mPDP,axiom, % 73.74/73.76 ! [W0,W1,W2] : % 73.74/73.76 ( ( aNaturalNumber0(W0) % 73.74/73.76 & aNaturalNumber0(W1) % 73.74/73.76 & aNaturalNumber0(W2) ) % 73.74/73.76 => ( ( isPrime0(W2) % 73.74/73.76 & doDivides0(W2,sdtasdt0(W0,W1)) ) % 73.74/73.76 => ( doDivides0(W2,W0) % 73.74/73.76 | doDivides0(W2,W1) ) ) ) ). % 73.74/73.76 % 73.74/73.76 fof(m__2987,hypothesis, % 73.74/73.76 ( aNaturalNumber0(xn) % 73.74/73.76 & aNaturalNumber0(xm) % 73.74/73.76 & aNaturalNumber0(xp) % 73.74/73.76 & xn != sz00 % 73.74/73.76 & xm != sz00 % 73.74/73.76 & xp != sz00 ) ). % 73.74/73.76 % 73.74/73.76 fof(m__2963,hypothesis, % 73.74/73.76 ! [W0,W1,W2] : % 73.74/73.76 ( ( aNaturalNumber0(W0) % 73.74/73.76 & aNaturalNumber0(W1) % 73.74/73.76 & aNaturalNumber0(W2) % 73.74/73.76 & W0 != sz00 % 73.74/73.76 & W1 != sz00 % 73.74/73.76 & W2 != sz00 ) % 73.74/73.76 => ( sdtasdt0(W2,sdtasdt0(W1,W1)) = sdtasdt0(W0,W0) % 73.74/73.76 => ( iLess0(W0,xn) % 73.74/73.76 => ~ ( ( W2 != sz10 % 73.74/73.76 & ! [W3] : % 73.74/73.76 ( ( aNaturalNumber0(W3) % 73.74/73.76 & ? [W4] : % 73.74/73.76 ( aNaturalNumber0(W4) % 73.74/73.76 & W2 = sdtasdt0(W3,W4) ) % 73.74/73.76 & doDivides0(W3,W2) ) % 73.74/73.76 => ( W3 = sz10 % 73.74/73.76 | W3 = W2 ) ) ) % 73.74/73.76 | isPrime0(W2) ) ) ) ) ). % 73.74/73.76 % 73.74/73.76 fof(m__3014,hypothesis, % 73.74/73.76 sdtasdt0(xp,sdtasdt0(xm,xm)) = sdtasdt0(xn,xn) ). % 73.74/73.76 % 73.74/73.76 fof(m__3025,hypothesis, % 73.74/73.76 ( xp != sz10 % 73.74/73.76 & ! [W0] : % 73.74/73.76 ( ( aNaturalNumber0(W0) % 73.74/73.76 & ( ? [W1] : % 73.74/73.76 ( aNaturalNumber0(W1) % 73.74/73.76 & xp = sdtasdt0(W0,W1) ) % 73.74/73.76 | doDivides0(W0,xp) ) ) % 73.74/73.76 => ( W0 = sz10 % 73.74/73.76 | W0 = xp ) ) % 73.74/73.76 & isPrime0(xp) ) ). % 73.74/73.76 % 73.74/73.76 fof(m__,conjecture, % 73.74/73.76 ( ( ? [W0] : % 73.74/73.76 ( aNaturalNumber0(W0) % 73.74/73.76 & sdtasdt0(xn,xn) = sdtasdt0(xp,W0) ) % 73.74/73.76 | doDivides0(xp,sdtasdt0(xn,xn)) ) % 73.74/73.76 & ( ? [W0] : % 73.74/73.76 ( aNaturalNumber0(W0) % 73.74/73.76 & xn = sdtasdt0(xp,W0) ) % 73.74/73.76 | doDivides0(xp,xn) ) ) ). % 73.74/73.76 % 73.74/73.76 %------------------------------------------------------------------------------ % 73.74/73.76 %------------------------------------------- % 73.74/73.76 % Proof found % 73.74/73.76 % SZS status Theorem for theBenchmark % 73.74/73.76 % SZS output start Proof % 73.74/73.76 %ClaNum:121(EqnAxiom:31) % 73.74/73.76 %VarNum:570(SingletonVarNum:159) % 73.74/73.76 %MaxLitNum:10 % 73.74/73.76 %MaxfuncDepth:2 % 73.74/73.76 %SharedTerms:22 % 73.74/73.76 %goalClause: 79 86 89 94 % 73.74/73.76 [32]P1(a1) % 73.74/73.76 [33]P1(a12) % 73.74/73.76 [34]P1(a13) % 73.74/73.76 [35]P1(a14) % 73.74/73.76 [36]P1(a15) % 73.74/73.76 [37]P2(a15) % 73.74/73.76 [39]~E(a1,a12) % 73.74/73.76 [40]~E(a1,a13) % 73.74/73.76 [41]~E(a1,a14) % 73.74/73.76 [42]~E(a1,a15) % 73.74/73.76 [43]~E(a15,a12) % 73.74/73.76 [38]E(f2(a15,f2(a14,a14)),f2(a13,a13)) % 73.74/73.76 [86]~P3(a15,a13)+~P3(a15,f2(a13,a13)) % 73.74/73.76 [54]~P1(x541)+P5(x541,x541) % 73.74/73.76 [46]~P1(x461)+E(f2(a1,x461),a1) % 73.74/73.76 [47]~P1(x471)+E(f2(x471,a1),a1) % 73.74/73.76 [48]~P1(x481)+E(f9(a1,x481),x481) % 73.74/73.76 [49]~P1(x491)+E(f2(a12,x491),x491) % 73.74/73.76 [50]~P1(x501)+E(f9(x501,a1),x501) % 73.74/73.76 [51]~P1(x511)+E(f2(x511,a12),x511) % 73.74/73.76 [44]~P1(x441)+~P2(x441)+~E(x441,a1) % 73.74/73.76 [45]~P1(x451)+~P2(x451)+~E(x451,a12) % 73.74/73.76 [79]~P1(x791)+~E(f2(a15,x791),f2(a13,a13))+~P3(a15,a13) % 73.74/73.76 [94]~P1(x941)+~P3(a15,f2(a13,a13))+~E(f2(a15,x941),a13) % 73.74/73.76 [67]~P1(x672)+~P1(x671)+E(f9(x671,x672),f9(x672,x671)) % 73.74/73.76 [68]~P1(x682)+~P1(x681)+E(f2(x681,x682),f2(x682,x681)) % 73.74/73.76 [70]~P1(x702)+~P1(x701)+P1(f9(x701,x702)) % 73.74/73.76 [71]~P1(x712)+~P1(x711)+P1(f2(x711,x712)) % 73.74/73.76 [56]~P1(x561)+E(x561,a12)+P5(a12,x561)+E(x561,a1) % 73.74/73.76 [59]~P1(x591)+E(x591,a15)+~P3(x591,a15)+E(x591,a12) % 73.74/73.76 [52]~P1(x521)+E(x521,a12)+E(x521,a1)+P1(f3(x521)) % 73.74/73.76 [53]~P1(x531)+E(x531,a12)+E(x531,a1)+P2(f3(x531)) % 73.74/73.76 [60]~P1(x601)+E(x601,a12)+P3(f3(x601),x601)+E(x601,a1) % 73.74/73.76 [61]~E(x612,x611)+~P1(x611)+~P1(x612)+P5(x611,x612) % 73.74/73.76 [69]P5(x692,x691)+~P1(x691)+~P1(x692)+P5(x691,x692) % 73.74/73.76 [63]~P1(x632)+~P1(x631)+E(x631,a1)+~E(f9(x632,x631),a1) % 73.74/73.76 [64]~P1(x642)+~P1(x641)+E(x641,a1)+~E(f9(x641,x642),a1) % 73.74/73.76 [75]~P1(x752)+~P1(x751)+P5(x752,f2(x752,x751))+E(x751,a1) % 73.74/73.76 [82]~P1(x822)+~P1(x821)+~P5(x821,x822)+P1(f5(x821,x822)) % 73.74/73.76 [83]~P1(x832)+~P1(x831)+~P3(x831,x832)+P1(f6(x831,x832)) % 73.74/73.76 [89]~P1(x892)+~P1(x891)+~E(f2(a15,x892),f2(a13,a13))+~E(f2(a15,x891),a13) % 73.74/73.76 [92]~P1(x921)+~P1(x922)+~P3(x921,x922)+E(f2(x921,f6(x921,x922)),x922) % 73.74/73.76 [93]~P1(x932)+~P1(x931)+~P5(x931,x932)+E(f9(x931,f5(x931,x932)),x932) % 73.74/73.76 [103]~P1(x1033)+~P1(x1032)+~P1(x1031)+E(f9(f9(x1031,x1032),x1033),f9(x1031,f9(x1032,x1033))) % 73.74/73.76 [104]~P1(x1043)+~P1(x1042)+~P1(x1041)+E(f2(f2(x1041,x1042),x1043),f2(x1041,f2(x1042,x1043))) % 73.74/73.76 [113]~P1(x1133)+~P1(x1132)+~P1(x1131)+E(f9(f2(x1131,x1132),f2(x1131,x1133)),f2(x1131,f9(x1132,x1133))) % 73.74/73.76 [114]~P1(x1142)+~P1(x1143)+~P1(x1141)+E(f9(f2(x1141,x1142),f2(x1143,x1142)),f2(f9(x1141,x1143),x1142)) % 73.74/73.76 [55]P2(x551)+~P1(x551)+E(x551,a12)+E(x551,a1)+~E(f4(x551),a12) % 73.74/73.76 [57]P2(x571)+~P1(x571)+E(x571,a12)+~E(f4(x571),x571)+E(x571,a1) % 73.74/73.76 [58]P2(x581)+~P1(x581)+E(x581,a12)+E(x581,a1)+P1(f4(x581)) % 73.74/73.76 [62]P2(x621)+~P1(x621)+E(x621,a12)+P3(f4(x621),x621)+E(x621,a1) % 73.74/73.76 [73]~P1(x731)+~P1(x732)+~P3(x732,x731)+P5(x732,x731)+E(x731,a1) % 73.74/73.76 [74]P4(x741,x742)+~P1(x742)+~P1(x741)+~P5(x741,x742)+E(x741,x742) % 73.74/73.76 [78]~P1(x782)+~P1(x781)+~P5(x782,x781)+~P5(x781,x782)+E(x781,x782) % 73.74/73.76 [65]~P1(x651)+~P1(x652)+E(x651,a15)+E(x651,a12)+~E(f2(x651,x652),a15) % 73.74/73.76 [66]~P1(x661)+~P1(x662)+E(x661,a1)+E(x662,a1)+~E(f2(x662,x661),a1) % 73.74/73.76 [76]~P1(x761)+~P1(x762)+~P1(x763)+P3(x761,x762)+~E(x762,f2(x761,x763)) % 73.74/73.76 [77]~P1(x772)+~P1(x771)+~P1(x773)+P5(x771,x772)+~E(f9(x771,x773),x772) % 73.74/73.76 [80]~P1(x803)+~P1(x802)+~P5(x803,x802)+P1(x801)+~E(x801,f10(x802,x803)) % 73.74/73.76 [84]~P1(x842)+~P1(x841)+~P1(x843)+E(x841,x842)+~E(f9(x843,x841),f9(x843,x842)) % 73.74/73.76 [85]~P1(x852)+~P1(x853)+~P1(x851)+E(x851,x852)+~E(f9(x851,x853),f9(x852,x853)) % 73.74/73.76 [90]~P1(x903)+~P1(x901)+~P5(x901,x903)+~E(x902,f10(x903,x901))+E(f9(x901,x902),x903) % 73.74/73.76 [72]~P1(x722)+~P1(x721)+~P2(x722)+~P3(x721,x722)+E(x721,x722)+E(x721,a12) % 73.74/73.76 [95]~P1(x952)+~P1(x951)+~P5(x953,x952)+~P5(x951,x953)+P5(x951,x952)+~P1(x953) % 73.74/73.76 [96]~P1(x962)+~P1(x961)+~P3(x963,x962)+~P3(x961,x963)+P3(x961,x962)+~P1(x963) % 73.74/73.76 [81]~P1(x811)+~P1(x813)+~P3(x811,x813)+P1(x812)+E(x811,a1)+~E(x812,f11(x813,x811)) % 73.74/73.76 [87]~P1(x872)+~P1(x871)+~P1(x873)+E(x871,x872)+~E(f2(x873,x871),f2(x873,x872))+E(x873,a1) % 73.74/73.76 [88]~P1(x882)+~P1(x883)+~P1(x881)+E(x881,x882)+~E(f2(x881,x883),f2(x882,x883))+E(x883,a1) % 73.74/73.76 [91]~P1(x911)+~P1(x912)+~P3(x911,x912)+~E(x913,f11(x912,x911))+E(x911,a1)+E(x912,f2(x911,x913)) % 73.74/73.76 [97]~P1(x972)+~P1(x973)+~P1(x971)+~P5(x973,x972)+~E(f9(x973,x971),x972)+E(x971,f10(x972,x973)) % 73.74/73.76 [105]~P1(x1053)+~P1(x1052)+~P1(x1051)+~P3(x1051,x1053)+~P3(x1051,x1052)+P3(x1051,f9(x1052,x1053)) % 73.74/73.76 [106]~P1(x1062)+~P1(x1061)+~P1(x1063)+~P5(x1061,x1062)+E(x1061,x1062)+P5(f9(x1063,x1061),f9(x1063,x1062)) % 73.74/73.76 [107]~P1(x1072)+~P1(x1073)+~P1(x1071)+~P5(x1071,x1072)+E(x1071,x1072)+P5(f9(x1071,x1073),f9(x1072,x1073)) % 73.74/73.76 [111]~P1(x1112)+~P1(x1111)+~P3(x1111,x1113)+P3(x1111,x1112)+~P1(x1113)+~P3(x1111,f9(x1113,x1112)) % 73.74/73.76 [112]~P1(x1122)+~P1(x1123)+~P1(x1121)+~P3(x1121,x1123)+E(x1121,a1)+E(f11(f2(x1122,x1123),x1121),f2(x1122,f11(x1123,x1121))) % 73.74/73.76 [98]~P1(x981)+~P1(x983)+~P1(x982)+~P3(x981,x983)+~E(x983,f2(x981,x982))+E(x981,a1)+E(x982,f11(x983,x981)) % 73.74/73.76 [108]~P1(x1082)+~P1(x1081)+~P1(x1083)+~P5(x1081,x1082)+E(x1081,x1082)+P5(f2(x1083,x1081),f2(x1083,x1082))+E(x1083,a1) % 73.74/73.76 [109]~P1(x1092)+~P1(x1093)+~P1(x1091)+~P5(x1091,x1092)+E(x1091,x1092)+P5(f2(x1091,x1093),f2(x1092,x1093))+E(x1093,a1) % 73.74/73.76 [110]~P1(x1101)+~P1(x1102)+~P1(x1103)+~P2(x1101)+P3(x1101,x1102)+P3(x1101,x1103)+~P3(x1101,f2(x1103,x1102)) % 73.74/73.76 [115]~P1(x1151)+~P1(x1152)+~P1(x1153)+~P2(x1153)+~P4(x1152,a13)+E(x1151,a1)+E(x1152,a1)+E(x1153,a1)+~E(f2(x1153,f2(x1151,x1151)),f2(x1152,x1152)) % 73.74/73.76 [116]~P1(x1161)+~P1(x1162)+~P1(x1163)+E(x1161,a12)+~P4(x1163,a13)+E(x1161,a1)+E(x1162,a1)+E(x1163,a1)+~E(f7(x1163,x1162,x1161),a12)+~E(f2(x1161,f2(x1162,x1162)),f2(x1163,x1163)) % 73.74/73.76 [117]~P1(x1171)+~P1(x1172)+~P1(x1173)+E(x1171,a12)+~E(f7(x1173,x1172,x1171),x1171)+~P4(x1173,a13)+E(x1171,a1)+E(x1172,a1)+E(x1173,a1)+~E(f2(x1171,f2(x1172,x1172)),f2(x1173,x1173)) % 73.74/73.76 [118]~P1(x1181)+~P1(x1182)+~P1(x1183)+E(x1181,a12)+~P4(x1183,a13)+E(x1181,a1)+E(x1182,a1)+E(x1183,a1)+P1(f7(x1183,x1182,x1181))+~E(f2(x1181,f2(x1182,x1182)),f2(x1183,x1183)) % 73.74/73.76 [119]~P1(x1191)+~P1(x1192)+~P1(x1193)+E(x1191,a12)+~P4(x1193,a13)+E(x1191,a1)+E(x1192,a1)+E(x1193,a1)+P1(f8(x1193,x1192,x1191))+~E(f2(x1191,f2(x1192,x1192)),f2(x1193,x1193)) % 73.74/73.76 [120]~P1(x1201)+~P1(x1202)+~P1(x1203)+E(x1201,a12)+P3(f7(x1203,x1202,x1201),x1201)+~P4(x1203,a13)+E(x1201,a1)+E(x1202,a1)+E(x1203,a1)+~E(f2(x1201,f2(x1202,x1202)),f2(x1203,x1203)) % 73.74/73.76 [121]~P1(x1211)+~P1(x1212)+~P1(x1213)+E(x1213,a12)+~P4(x1212,a13)+E(x1211,a1)+E(x1212,a1)+E(x1213,a1)+E(f2(f7(x1212,x1211,x1213),f8(x1212,x1211,x1213)),x1213)+~E(f2(x1213,f2(x1211,x1211)),f2(x1212,x1212)) % 73.74/73.76 %EqnAxiom % 73.74/73.76 [1]E(x11,x11) % 73.74/73.76 [2]E(x22,x21)+~E(x21,x22) % 73.74/73.76 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 73.74/73.76 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 73.74/73.76 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 73.74/73.76 [6]~E(x61,x62)+E(f8(x61,x63,x64),f8(x62,x63,x64)) % 73.74/73.76 [7]~E(x71,x72)+E(f8(x73,x71,x74),f8(x73,x72,x74)) % 73.74/73.76 [8]~E(x81,x82)+E(f8(x83,x84,x81),f8(x83,x84,x82)) % 73.74/73.76 [9]~E(x91,x92)+E(f7(x91,x93,x94),f7(x92,x93,x94)) % 73.74/73.76 [10]~E(x101,x102)+E(f7(x103,x101,x104),f7(x103,x102,x104)) % 73.74/73.76 [11]~E(x111,x112)+E(f7(x113,x114,x111),f7(x113,x114,x112)) % 73.74/73.76 [12]~E(x121,x122)+E(f9(x121,x123),f9(x122,x123)) % 73.74/73.76 [13]~E(x131,x132)+E(f9(x133,x131),f9(x133,x132)) % 73.74/73.76 [14]~E(x141,x142)+E(f11(x141,x143),f11(x142,x143)) % 73.74/73.76 [15]~E(x151,x152)+E(f11(x153,x151),f11(x153,x152)) % 73.74/73.76 [16]~E(x161,x162)+E(f5(x161,x163),f5(x162,x163)) % 73.74/73.76 [17]~E(x171,x172)+E(f5(x173,x171),f5(x173,x172)) % 73.74/73.76 [18]~E(x181,x182)+E(f10(x181,x183),f10(x182,x183)) % 73.74/73.76 [19]~E(x191,x192)+E(f10(x193,x191),f10(x193,x192)) % 73.74/73.76 [20]~E(x201,x202)+E(f6(x201,x203),f6(x202,x203)) % 73.74/73.76 [21]~E(x211,x212)+E(f6(x213,x211),f6(x213,x212)) % 73.74/73.76 [22]~E(x221,x222)+E(f4(x221),f4(x222)) % 73.74/73.76 [23]~E(x231,x232)+E(f3(x231),f3(x232)) % 73.74/73.76 [24]~P1(x241)+P1(x242)+~E(x241,x242) % 73.74/73.76 [25]P4(x252,x253)+~E(x251,x252)+~P4(x251,x253) % 73.74/73.77 [26]P4(x263,x262)+~E(x261,x262)+~P4(x263,x261) % 73.74/73.77 [27]P5(x272,x273)+~E(x271,x272)+~P5(x271,x273) % 73.74/73.77 [28]P5(x283,x282)+~E(x281,x282)+~P5(x283,x281) % 73.74/73.77 [29]P3(x292,x293)+~E(x291,x292)+~P3(x291,x293) % 73.74/73.77 [30]P3(x303,x302)+~E(x301,x302)+~P3(x303,x301) % 73.74/73.77 [31]~P2(x311)+P2(x312)+~E(x311,x312) % 73.74/73.77 % 73.74/73.77 %------------------------------------------- % 73.74/73.78 cnf(122,plain, % 73.74/73.78 (~P2(a1)+~P1(a1)), % 73.74/73.78 inference(equality_inference,[],[44])). % 73.74/73.78 cnf(123,plain, % 73.74/73.78 (~P2(a12)+~P1(a12)), % 73.74/73.78 inference(equality_inference,[],[45])). % 73.74/73.78 cnf(125,plain, % 73.74/73.78 (P3(x1251,f2(x1251,x1252))+~P1(x1251)+~P1(f2(x1251,x1252))+~P1(x1252)), % 73.74/73.78 inference(equality_inference,[],[76])). % 73.74/73.78 cnf(126,plain, % 73.74/73.78 (P5(x1261,f9(x1261,x1262))+~P1(f9(x1261,x1262))+~P1(x1261)+~P1(x1262)), % 73.74/73.78 inference(equality_inference,[],[77])). % 73.74/73.78 cnf(127,plain, % 73.74/73.78 (~P5(x1271,x1272)+~P1(x1271)+~P1(x1272)+P1(f10(x1272,x1271))), % 73.74/73.78 inference(equality_inference,[],[80])). % 73.74/73.78 cnf(128,plain, % 73.74/73.78 (~P3(x1281,x1282)+~P1(x1281)+~P1(x1282)+P1(f11(x1282,x1281))+E(x1281,a1)), % 73.74/73.78 inference(equality_inference,[],[81])). % 73.74/73.78 cnf(133,plain, % 73.74/73.78 (~P5(x1331,x1332)+~P1(x1332)+~P1(x1331)+E(f9(x1331,f10(x1332,x1331)),x1332)), % 73.74/73.78 inference(equality_inference,[],[90])). % 73.74/73.78 cnf(134,plain, % 73.74/73.78 (~P3(x1341,x1342)+~P1(x1341)+~P1(x1342)+E(x1341,a1)+E(x1342,f2(x1341,f11(x1342,x1341)))), % 73.74/73.78 inference(equality_inference,[],[91])). % 73.74/73.78 cnf(135,plain, % 73.74/73.78 (~P5(x1351,f9(x1351,x1352))+~P1(f9(x1351,x1352))+~P1(x1351)+~P1(x1352)+E(x1352,f10(f9(x1351,x1352),x1351))), % 73.74/73.78 inference(equality_inference,[],[97])). % 73.74/73.78 cnf(136,plain, % 73.74/73.78 (~P3(x1361,f2(x1361,x1362))+~P1(x1361)+~P1(f2(x1361,x1362))+~P1(x1362)+E(x1361,a1)+E(x1362,f11(f2(x1361,x1362),x1361))), % 73.74/73.78 inference(equality_inference,[],[98])). % 73.74/73.78 cnf(142,plain, % 73.74/73.78 (~P2(a1)), % 73.74/73.78 inference(scs_inference,[],[32,122])). % 73.74/73.78 cnf(143,plain, % 73.74/73.78 (~P2(a12)), % 73.74/73.78 inference(scs_inference,[],[33,123])). % 73.74/73.78 cnf(144,plain, % 73.74/73.78 (E(f2(a13,a13),f2(a15,f2(a14,a14)))), % 73.74/73.78 inference(scs_inference,[],[38,2])). % 73.74/73.78 cnf(145,plain, % 73.74/73.78 (~P3(a1,a15)), % 73.74/73.78 inference(scs_inference,[],[32,38,39,42,2,59])). % 73.74/73.78 cnf(147,plain, % 73.74/73.78 (P5(a1,a1)), % 73.74/73.78 inference(scs_inference,[],[32,38,39,42,2,59,69])). % 73.74/73.78 cnf(149,plain, % 73.74/73.78 (E(f9(a1,f10(a1,a1)),a1)), % 73.74/73.78 inference(scs_inference,[],[32,38,39,42,2,59,69,133])). % 73.74/73.78 cnf(151,plain, % 73.74/73.78 (~P1(f2(a14,a14))+~P3(a15,a13)), % 73.74/73.78 inference(scs_inference,[],[32,38,39,42,2,59,69,133,79])). % 73.74/73.78 cnf(153,plain, % 73.74/73.78 (P1(f10(a1,a1))), % 73.74/73.78 inference(scs_inference,[],[32,38,39,42,2,59,69,133,79,127])). % 73.74/73.78 cnf(155,plain, % 73.74/73.78 (E(f10(a1,a1),a1)), % 73.74/73.78 inference(scs_inference,[],[32,38,39,42,2,59,69,133,79,127,63])). % 73.74/73.78 cnf(160,plain, % 73.74/73.78 (E(x1601,a1)+~E(x1601,f9(a1,f10(a1,a1)))), % 73.74/73.78 inference(scs_inference,[],[32,38,39,42,2,59,69,133,79,127,63,24,44,3])). % 73.74/73.78 cnf(162,plain, % 73.74/73.78 (E(a15,a1)+P5(a12,a15)), % 73.74/73.78 inference(scs_inference,[],[32,36,38,39,42,43,2,59,69,133,79,127,63,24,44,3,31,56])). % 73.74/73.78 cnf(165,plain, % 73.74/73.78 (E(a1,f9(a1,f10(a1,a1)))), % 73.74/73.78 inference(scs_inference,[],[149,2])). % 73.74/73.78 cnf(166,plain, % 73.74/73.78 (P5(f9(a1,f10(a1,a1)),a1)), % 73.74/73.78 inference(scs_inference,[],[147,149,2,27])). % 73.74/73.78 cnf(167,plain, % 73.74/73.78 (P5(a1,f9(a1,f10(a1,a1)))), % 73.74/73.78 inference(scs_inference,[],[147,149,2,27,28])). % 73.74/73.78 cnf(168,plain, % 73.74/73.78 (~P2(f10(a1,a1))), % 73.74/73.78 inference(scs_inference,[],[153,147,149,155,2,27,28,44])). % 73.74/73.78 cnf(170,plain, % 73.74/73.78 (P1(f9(a1,f10(a1,a1)))), % 73.74/73.78 inference(scs_inference,[],[32,153,147,149,155,2,27,28,44,24])). % 73.74/73.78 cnf(171,plain, % 73.74/73.78 (~P2(f9(a1,f10(a1,a1)))), % 73.74/73.78 inference(scs_inference,[],[32,153,147,149,155,142,2,27,28,44,24,31])). % 73.74/73.78 cnf(172,plain, % 73.74/73.78 (P5(f10(a1,a1),f10(a1,a1))), % 73.74/73.78 inference(scs_inference,[],[32,153,147,149,155,142,2,27,28,44,24,31,69])). % 73.74/73.78 cnf(174,plain, % 73.74/73.78 (P1(f10(f10(a1,a1),f10(a1,a1)))), % 73.74/73.78 inference(scs_inference,[],[32,153,147,149,155,142,2,27,28,44,24,31,69,127])). % 73.74/73.78 cnf(176,plain, % 73.74/73.78 (E(f9(f10(a1,a1),f10(f10(a1,a1),f10(a1,a1))),f10(a1,a1))), % 73.74/73.78 inference(scs_inference,[],[32,153,147,149,155,142,2,27,28,44,24,31,69,127,133])). % 73.74/73.78 cnf(178,plain, % 73.74/73.78 (P1(f9(f10(a1,a1),f10(f10(a1,a1),f10(a1,a1))))), % 73.74/73.78 inference(scs_inference,[],[32,153,147,149,155,142,2,27,28,44,24,31,69,127,133,80])). % 73.74/73.78 cnf(180,plain, % 73.74/73.78 (E(f9(f10(a1,a1),f10(f10(a1,a1),f10(a1,a1))),a1)), % 73.74/73.78 inference(scs_inference,[],[32,153,147,149,155,142,2,27,28,44,24,31,69,127,133,80,3])). % 73.74/73.78 cnf(181,plain, % 73.74/73.78 (P3(f3(a15),a15)+E(a15,a1)), % 73.74/73.78 inference(scs_inference,[],[32,153,36,147,149,155,142,43,2,27,28,44,24,31,69,127,133,80,3,60])). % 73.74/73.78 cnf(183,plain, % 73.74/73.78 (E(f10(f10(a1,a1),f10(a1,a1)),a1)), % 73.74/73.78 inference(scs_inference,[],[32,153,36,147,149,155,142,43,2,27,28,44,24,31,69,127,133,80,3,60,63])). % 73.74/73.78 cnf(185,plain, % 73.74/73.78 (P5(f10(a1,a1),a1)), % 73.74/73.78 inference(scs_inference,[],[32,153,36,147,149,155,142,43,2,27,28,44,24,31,69,127,133,80,3,60,63,77])). % 73.74/73.78 cnf(187,plain, % 73.74/73.78 (E(f10(f10(a1,a1),f10(a1,a1)),f10(a1,f10(a1,a1)))), % 73.74/73.78 inference(scs_inference,[],[32,153,36,147,149,155,142,43,2,27,28,44,24,31,69,127,133,80,3,60,63,77,97])). % 73.74/73.78 cnf(189,plain, % 73.74/73.78 (~E(f3(a15),a1)+E(a15,a1)), % 73.74/73.78 inference(scs_inference,[],[32,153,36,147,149,145,155,142,43,2,27,28,44,24,31,69,127,133,80,3,60,63,77,97,29])). % 73.74/73.78 cnf(192,plain, % 73.74/73.78 (E(f10(a1,a1),f9(f10(a1,a1),f10(f10(a1,a1),f10(a1,a1))))), % 73.74/73.78 inference(scs_inference,[],[176,2])). % 73.74/73.78 cnf(193,plain, % 73.74/73.78 (P5(f10(a1,a1),f9(a1,f10(a1,a1)))), % 73.74/73.78 inference(scs_inference,[],[176,185,165,2,28])). % 73.74/73.78 cnf(194,plain, % 73.74/73.78 (P5(a1,f10(a1,a1))), % 73.74/73.78 inference(scs_inference,[],[176,172,185,165,155,2,28,27])). % 73.74/73.78 cnf(195,plain, % 73.74/73.78 (~P2(f10(f10(a1,a1),f10(a1,a1)))), % 73.74/73.78 inference(scs_inference,[],[174,176,172,185,165,183,155,2,28,27,44])). % 73.74/73.78 cnf(198,plain, % 73.74/73.78 (P1(f10(a1,f10(a1,a1)))), % 73.74/73.78 inference(scs_inference,[],[174,176,172,168,185,187,165,183,155,2,28,27,44,31,24])). % 73.74/73.78 cnf(199,plain, % 73.74/73.78 (P5(f10(f10(a1,a1),f10(a1,a1)),f10(f10(a1,a1),f10(a1,a1)))), % 73.74/73.78 inference(scs_inference,[],[174,176,172,168,185,187,165,183,155,2,28,27,44,31,24,69])). % 73.74/73.78 cnf(201,plain, % 73.74/73.78 (E(a1,f10(a1,a1))), % 73.74/73.78 inference(scs_inference,[],[32,174,153,176,172,168,185,187,165,183,155,2,28,27,44,31,24,69,78])). % 73.74/73.78 cnf(208,plain, % 73.74/73.78 (E(a1,f9(f10(a1,a1),f10(f10(a1,a1),f10(a1,a1))))), % 73.74/73.78 inference(scs_inference,[],[180,2])). % 73.74/73.78 cnf(210,plain, % 73.74/73.78 (P5(f9(a1,f10(a1,a1)),f10(a1,a1))), % 73.74/73.78 inference(scs_inference,[],[201,180,166,172,192,2,27,28])). % 73.74/73.78 cnf(213,plain, % 73.74/73.78 (E(f9(a1,f10(a1,a1)),f10(a1,a1))), % 73.74/73.78 inference(scs_inference,[],[153,170,201,180,166,172,192,193,2,27,28,69,78])). % 73.74/73.78 cnf(217,plain, % 73.74/73.78 (E(f10(a1,a1),f10(f10(a1,a1),a1))), % 73.74/73.78 inference(scs_inference,[],[32,153,178,170,201,180,166,172,185,192,193,194,2,27,28,69,78,95,97])). % 73.74/73.78 cnf(219,plain, % 73.74/73.78 (~P1(f2(a13,a13))+P1(f2(a15,f2(a14,a14)))), % 73.74/73.78 inference(scs_inference,[],[32,153,178,170,201,180,166,172,185,192,193,144,194,2,27,28,69,78,95,97,24])). % 73.74/73.78 cnf(220,plain, % 73.74/73.78 (E(a1,f10(f10(a1,a1),a1))), % 73.74/73.78 inference(scs_inference,[],[32,153,178,170,201,180,166,172,185,192,193,144,194,2,27,28,69,78,95,97,24,3])). % 73.74/73.78 cnf(225,plain, % 73.74/73.78 (P5(a1,f10(f10(a1,a1),f10(a1,a1)))), % 73.74/73.78 inference(scs_inference,[],[213,192,183,172,199,2,28,27])). % 73.74/73.78 cnf(226,plain, % 73.74/73.78 (P1(f10(f10(a1,a1),a1))), % 73.74/73.78 inference(scs_inference,[],[153,213,192,183,172,199,217,2,28,27,24])). % 73.74/73.78 cnf(227,plain, % 73.74/73.78 (P5(f10(a1,f10(a1,a1)),f10(a1,f10(a1,a1)))), % 73.74/73.78 inference(scs_inference,[],[153,213,198,192,183,172,199,217,2,28,27,24,69])). % 73.74/73.78 cnf(230,plain, % 73.74/73.78 (E(x2301,a1)+~E(x2301,f10(f10(a1,a1),f10(a1,a1)))), % 73.74/73.78 inference(scs_inference,[],[153,213,198,192,183,172,199,217,144,2,28,27,24,69,31,3])). % 73.74/73.78 cnf(233,plain, % 73.74/73.78 (P1(f10(a12,a12))+~P5(a12,a12)), % 73.74/73.78 inference(scs_inference,[],[32,153,213,198,33,192,183,172,199,217,144,2,28,27,24,69,31,3,126,127])). % 73.74/73.78 cnf(235,plain, % 73.74/73.78 (P3(a1,f2(a1,a1))+~P1(f2(a1,a1))), % 73.74/73.78 inference(scs_inference,[],[32,153,213,198,33,192,183,172,199,217,144,2,28,27,24,69,31,3,126,127,125])). % 73.74/73.78 cnf(237,plain, % 73.74/73.78 (P5(a12,a12)), % 73.74/73.78 inference(scs_inference,[],[32,153,213,198,33,192,183,172,199,217,144,2,28,27,24,69,31,3,126,127,125,61])). % 73.74/73.78 cnf(240,plain, % 73.74/73.78 (P1(f10(a12,a12))), % 73.74/73.78 inference(scs_inference,[],[237,233])). % 73.74/73.78 cnf(241,plain, % 73.74/73.78 (E(f10(a1,f10(a1,a1)),f10(f10(a1,a1),f10(a1,a1)))), % 73.74/73.78 inference(scs_inference,[],[187,237,233,2])). % 73.74/73.78 cnf(243,plain, % 73.74/73.78 (P5(f10(f10(a1,a1),f10(a1,a1)),f10(a1,f10(a1,a1)))), % 73.74/73.78 inference(scs_inference,[],[192,187,194,227,237,233,2,28,27])). % 73.74/73.78 cnf(244,plain, % 73.74/73.78 (~P2(f10(a1,f10(a1,a1)))), % 73.74/73.78 inference(scs_inference,[],[192,187,194,195,227,237,233,2,28,27,31])). % 73.74/73.78 cnf(245,plain, % 73.74/73.78 (E(f10(a1,f10(a1,a1)),a1)), % 73.74/73.78 inference(scs_inference,[],[192,187,183,194,195,227,237,233,2,28,27,31,3])). % 73.74/73.78 cnf(246,plain, % 73.74/73.78 (E(f9(a12,f10(a12,a12)),a12)), % 73.74/73.78 inference(scs_inference,[],[33,192,187,183,194,195,227,237,233,2,28,27,31,3,133])). % 73.74/73.78 cnf(248,plain, % 73.74/73.78 (P5(f10(f10(a1,a1),a1),f10(f10(a1,a1),a1))), % 73.74/73.78 inference(scs_inference,[],[226,33,192,187,183,194,195,227,237,233,2,28,27,31,3,133,69])). % 73.74/73.78 cnf(254,plain, % 73.74/73.78 (P1(f10(a14,a14))+~P5(a14,a14)), % 73.74/73.78 inference(scs_inference,[],[153,226,35,33,192,187,183,194,195,227,237,233,2,28,27,31,3,133,69,45,126,127])). % 73.74/73.78 cnf(256,plain, % 73.74/73.78 (P3(f10(a1,a1),f2(f10(a1,a1),f10(a1,a1)))+~P1(f2(f10(a1,a1),f10(a1,a1)))), % 73.74/73.78 inference(scs_inference,[],[153,226,35,33,192,187,183,194,195,227,237,233,2,28,27,31,3,133,69,45,126,127,125])). % 73.74/73.78 cnf(258,plain, % 73.74/73.78 (P5(a14,a14)), % 73.74/73.78 inference(scs_inference,[],[153,226,35,33,192,187,183,194,195,227,237,233,2,28,27,31,3,133,69,45,126,127,125,61])). % 73.74/73.78 cnf(261,plain, % 73.74/73.78 (P1(f10(a14,a14))), % 73.74/73.78 inference(scs_inference,[],[258,254])). % 73.74/73.78 cnf(263,plain, % 73.74/73.78 (P5(a1,f10(a1,f10(a1,a1)))), % 73.74/73.78 inference(scs_inference,[],[187,183,225,258,254,2,28])). % 73.74/73.78 cnf(264,plain, % 73.74/73.78 (P5(f10(a1,a1),f10(f10(a1,a1),f10(a1,a1)))), % 73.74/73.78 inference(scs_inference,[],[201,187,183,225,258,254,2,28,27])). % 73.74/73.78 cnf(265,plain, % 73.74/73.78 (~P2(f9(a12,f10(a12,a12)))), % 73.74/73.78 inference(scs_inference,[],[201,187,183,225,246,143,258,254,2,28,27,31])). % 73.74/73.78 cnf(266,plain, % 73.74/73.78 (E(f9(a1,f10(a1,a1)),f10(f10(a1,a1),a1))), % 73.74/73.78 inference(scs_inference,[],[213,201,187,183,217,225,246,143,258,254,2,28,27,31,3])). % 73.74/73.78 cnf(267,plain, % 73.74/73.78 (E(f9(a14,f10(a14,a14)),a14)), % 73.74/73.78 inference(scs_inference,[],[213,201,35,187,183,217,225,246,143,258,254,2,28,27,31,3,133])). % 73.74/73.78 cnf(269,plain, % 73.74/73.78 (P5(f10(a12,a12),f10(a12,a12))), % 73.74/73.78 inference(scs_inference,[],[213,201,240,35,187,183,217,225,246,143,258,254,2,28,27,31,3,133,69])). % 73.74/73.78 cnf(271,plain, % 73.74/73.78 (P5(a1,f10(f10(a1,a1),a1))), % 73.74/73.78 inference(scs_inference,[],[32,153,213,201,226,240,35,187,183,217,225,246,143,258,254,2,28,27,31,3,133,69,77])). % 73.74/73.78 cnf(273,plain, % 73.74/73.78 (E(f10(a1,a1),f10(f10(f10(a1,a1),a1),a1))), % 73.74/73.78 inference(scs_inference,[],[32,153,213,201,226,240,35,187,183,217,225,246,143,258,254,2,28,27,31,3,133,69,77,97])). % 73.74/73.78 cnf(276,plain, % 73.74/73.78 (P5(a12,f9(a12,a12))+~P1(f9(a12,a12))), % 73.74/73.78 inference(scs_inference,[],[32,153,213,201,226,33,240,35,187,183,217,225,246,143,258,254,2,28,27,31,3,133,69,77,97,24,126])). % 73.74/73.78 cnf(278,plain, % 73.74/73.78 (P1(f10(f10(a12,a12),f10(a12,a12)))), % 73.82/73.78 inference(scs_inference,[],[32,153,213,201,226,33,240,35,187,183,217,225,246,143,258,254,2,28,27,31,3,133,69,77,97,24,126,127])). % 73.82/73.78 cnf(282,plain, % 73.82/73.78 (P5(a13,a13)), % 73.82/73.78 inference(scs_inference,[],[32,153,213,201,226,33,240,34,35,187,183,217,225,246,143,258,254,2,28,27,31,3,133,69,77,97,24,126,127,125,61])). % 73.82/73.78 cnf(286,plain, % 73.82/73.78 (E(f10(f10(a1,a1),a1),f10(a1,a1))), % 73.82/73.78 inference(scs_inference,[],[217,2])). % 73.82/73.78 cnf(287,plain, % 73.82/73.78 (P5(f10(a1,a1),f10(a1,f10(a1,a1)))), % 73.82/73.78 inference(scs_inference,[],[187,217,264,2,28])). % 73.82/73.78 cnf(288,plain, % 73.82/73.78 (P5(f10(a1,a1),f10(f10(a1,a1),a1))), % 73.82/73.78 inference(scs_inference,[],[187,217,264,248,2,28,27])). % 73.82/73.78 cnf(289,plain, % 73.82/73.78 (~P2(f10(f10(a1,a1),a1))), % 73.82/73.78 inference(scs_inference,[],[187,217,264,248,168,2,28,27,31])). % 73.82/73.78 cnf(291,plain, % 73.82/73.78 (E(f9(f10(a12,a12),f10(f10(a12,a12),f10(a12,a12))),f10(a12,a12))), % 73.82/73.78 inference(scs_inference,[],[240,187,39,217,246,264,269,248,168,2,28,27,31,3,133])). % 73.82/73.78 cnf(293,plain, % 73.82/73.78 (P5(f10(f10(a12,a12),f10(a12,a12)),f10(f10(a12,a12),f10(a12,a12)))), % 73.82/73.78 inference(scs_inference,[],[240,278,187,39,217,246,264,269,248,168,2,28,27,31,3,133,69])). % 73.82/73.78 cnf(295,plain, % 73.82/73.78 (P1(f10(a13,a13))), % 73.82/73.78 inference(scs_inference,[],[240,278,34,187,39,217,246,264,269,248,282,168,2,28,27,31,3,133,69,127])). % 73.82/73.78 cnf(297,plain, % 73.82/73.78 (P1(f9(f10(a12,a12),f10(f10(a12,a12),f10(a12,a12))))), % 73.82/73.78 inference(scs_inference,[],[33,240,278,34,187,39,217,246,264,269,248,282,168,237,2,28,27,31,3,133,69,127,80])). % 73.82/73.78 cnf(302,plain, % 73.82/73.78 (E(a12,f9(a12,f10(a12,a12)))), % 73.82/73.78 inference(scs_inference,[],[246,2])). % 73.82/73.78 cnf(303,plain, % 73.82/73.78 (P5(f10(f10(a1,a1),f10(a1,a1)),a1)), % 73.82/73.78 inference(scs_inference,[],[246,245,243,2,28])). % 73.82/73.78 cnf(304,plain, % 73.82/73.78 (P5(f9(a12,f10(a12,a12)),a12)), % 73.82/73.78 inference(scs_inference,[],[246,245,243,237,2,28,27])). % 73.82/73.78 cnf(305,plain, % 73.82/73.78 (P1(f9(a12,f10(a12,a12)))), % 73.82/73.78 inference(scs_inference,[],[33,246,245,243,237,2,28,27,24])). % 73.82/73.78 cnf(306,plain, % 73.82/73.78 (~E(a15,f9(a12,f10(a12,a12)))), % 73.82/73.78 inference(scs_inference,[],[33,43,246,245,243,237,2,28,27,24,3])). % 73.82/73.78 cnf(307,plain, % 73.82/73.78 (E(f9(a13,f10(a13,a13)),a13)), % 73.82/73.78 inference(scs_inference,[],[33,34,43,246,245,243,282,237,2,28,27,24,3,133])). % 73.82/73.78 cnf(309,plain, % 73.82/73.78 (P5(f10(a14,a14),f10(a14,a14))), % 73.82/73.79 inference(scs_inference,[],[33,261,34,43,246,245,243,282,237,2,28,27,24,3,133,69])). % 73.82/73.79 cnf(311,plain, % 73.82/73.79 (P1(f10(f10(a14,a14),f10(a14,a14)))), % 73.82/73.79 inference(scs_inference,[],[33,261,34,43,246,245,243,282,237,2,28,27,24,3,133,69,127])). % 73.82/73.79 cnf(318,plain, % 73.82/73.79 (P5(f10(a13,a13),f10(a13,a13))), % 73.82/73.79 inference(scs_inference,[],[33,240,261,295,34,43,246,245,267,243,282,237,2,28,27,24,3,133,69,127,31,126,125,61])). % 73.82/73.79 cnf(322,plain, % 73.82/73.79 (P5(f10(f10(a1,a1),f10(a1,a1)),f10(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[201,220,303,2,28])). % 73.82/73.79 cnf(323,plain, % 73.82/73.79 (~E(a1,f9(a14,f10(a14,a14)))), % 73.82/73.79 inference(scs_inference,[],[201,220,267,303,41,2,28,3])). % 73.82/73.79 cnf(324,plain, % 73.82/73.79 (E(f9(f10(a14,a14),f10(f10(a14,a14),f10(a14,a14))),f10(a14,a14))), % 73.82/73.79 inference(scs_inference,[],[201,261,220,267,309,303,41,2,28,3,133])). % 73.82/73.79 cnf(326,plain, % 73.82/73.79 (P5(f9(a12,f10(a12,a12)),f9(a12,f10(a12,a12)))), % 73.82/73.79 inference(scs_inference,[],[201,261,305,220,267,309,303,41,2,28,3,133,69])). % 73.82/73.79 cnf(328,plain, % 73.82/73.79 (P1(f10(f10(a13,a13),f10(a13,a13)))), % 73.82/73.79 inference(scs_inference,[],[201,261,305,295,220,267,309,303,318,41,2,28,3,133,69,127])). % 73.82/73.79 cnf(330,plain, % 73.82/73.79 (E(f10(f10(a1,a1),f10(a1,a1)),f10(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[153,201,261,305,295,174,220,267,264,309,303,318,41,2,28,3,133,69,127,78])). % 73.82/73.79 cnf(338,plain, % 73.82/73.79 (P5(f10(f10(a14,a14),f10(a14,a14)),f10(f10(a14,a14),f10(a14,a14)))), % 73.82/73.79 inference(scs_inference,[],[153,201,261,305,311,295,174,35,220,267,291,264,293,309,303,318,41,258,2,28,3,133,69,127,78,80,27,31,126,61])). % 73.82/73.79 cnf(340,plain, % 73.82/73.79 (P3(f10(a13,a13),f2(f10(a13,a13),f10(a13,a13)))+~P1(f2(f10(a13,a13),f10(a13,a13)))), % 73.82/73.79 inference(scs_inference,[],[153,201,261,305,311,295,174,35,220,267,291,264,293,309,303,318,41,258,2,28,3,133,69,127,78,80,27,31,126,61,125])). % 73.82/73.79 cnf(342,plain, % 73.82/73.79 (E(f10(a14,a14),f10(f9(f10(a14,a14),f10(a14,a14)),f10(a14,a14)))+~P1(f9(f10(a14,a14),f10(a14,a14)))), % 73.82/73.79 inference(scs_inference,[],[153,201,261,305,311,295,174,35,220,267,291,264,293,309,303,318,41,258,2,28,3,133,69,127,78,80,27,31,126,61,125,135])). % 73.82/73.79 cnf(346,plain, % 73.82/73.79 (P5(f10(a1,f10(a1,a1)),a1)), % 73.82/73.79 inference(scs_inference,[],[330,245,227,2,28])). % 73.82/73.79 cnf(347,plain, % 73.82/73.79 (P5(a12,f9(a12,f10(a12,a12)))), % 73.82/73.79 inference(scs_inference,[],[330,246,245,326,227,2,28,27])). % 73.82/73.79 cnf(349,plain, % 73.82/73.79 (E(f9(f10(a13,a13),f10(f10(a13,a13),f10(a13,a13))),f10(a13,a13))), % 73.82/73.79 inference(scs_inference,[],[330,295,246,245,241,326,227,318,2,28,27,3,133])). % 73.82/73.79 cnf(358,plain, % 73.82/73.79 (P5(a15,a15)), % 73.82/73.79 inference(scs_inference,[],[32,198,330,328,295,34,36,246,245,241,307,326,263,227,318,282,2,28,27,3,133,69,78,80,31,61])). % 73.82/73.79 cnf(360,plain, % 73.82/73.79 (P5(f10(a13,a13),f9(f10(a13,a13),f10(a13,a13)))+~P1(f9(f10(a13,a13),f10(a13,a13)))), % 73.82/73.79 inference(scs_inference,[],[32,198,330,328,295,34,36,246,245,241,307,326,263,227,318,282,2,28,27,3,133,69,78,80,31,61,126])). % 73.82/73.79 cnf(362,plain, % 73.82/73.79 (P1(f10(a15,a15))), % 73.82/73.79 inference(scs_inference,[],[32,198,330,328,295,34,36,246,245,241,307,326,263,227,318,282,2,28,27,3,133,69,78,80,31,61,126,127])). % 73.82/73.79 cnf(367,plain, % 73.82/73.79 (~E(a1,f9(a13,f10(a13,a13)))), % 73.82/73.79 inference(scs_inference,[],[201,266,307,346,40,2,28,3])). % 73.82/73.79 cnf(368,plain, % 73.82/73.79 (E(f9(a15,f10(a15,a15)),a15)), % 73.82/73.79 inference(scs_inference,[],[201,36,266,307,346,40,358,2,28,3,133])). % 73.82/73.79 cnf(370,plain, % 73.82/73.79 (P5(f10(a15,a15),f10(a15,a15))), % 73.82/73.79 inference(scs_inference,[],[201,362,36,266,307,346,40,358,2,28,3,133,69])). % 73.82/73.79 cnf(372,plain, % 73.82/73.79 (E(f10(a1,a1),f10(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[153,201,198,362,36,266,307,287,346,40,358,2,28,3,133,69,78])). % 73.82/73.79 cnf(375,plain, % 73.82/73.79 (P1(f10(f10(a15,a15),f10(a15,a15)))), % 73.82/73.79 inference(scs_inference,[],[153,201,198,362,36,266,307,287,338,346,40,358,2,28,3,133,69,78,27,127])). % 73.82/73.79 cnf(378,plain, % 73.82/73.79 (P5(f10(f10(a15,a15),f10(a15,a15)),f10(f10(a15,a15),f10(a15,a15)))), % 73.82/73.79 inference(scs_inference,[],[153,201,198,362,36,266,307,324,287,338,346,40,358,2,28,3,133,69,78,27,127,31,61])). % 73.82/73.79 cnf(388,plain, % 73.82/73.79 (P1(f9(a14,f10(a14,a14)))), % 73.82/73.79 inference(scs_inference,[],[35,267,2,24])). % 73.82/73.79 cnf(392,plain, % 73.82/73.79 (E(f9(f10(a15,a15),f10(f10(a15,a15),f10(a15,a15))),f10(a15,a15))), % 73.82/73.79 inference(scs_inference,[],[213,35,362,372,267,210,193,370,2,24,27,28,3,133])). % 73.82/73.79 cnf(394,plain, % 73.82/73.79 (P5(f9(a14,f10(a14,a14)),f9(a14,f10(a14,a14)))), % 73.82/73.79 inference(scs_inference,[],[213,35,362,372,267,210,193,370,2,24,27,28,3,133,69])). % 73.82/73.79 cnf(396,plain, % 73.82/73.79 (E(f10(a1,f10(a1,a1)),f9(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[213,198,35,170,362,372,267,210,193,370,2,24,27,28,3,133,69,78])). % 73.82/73.79 cnf(400,plain, % 73.82/73.79 (E(f10(a1,a1),f10(f10(a1,f10(a1,a1)),a1))), % 73.82/73.79 inference(scs_inference,[],[32,213,153,198,35,170,362,36,372,267,210,193,263,370,358,2,24,27,28,3,133,69,78,80,97])). % 73.82/73.79 cnf(405,plain, % 73.82/73.79 (P5(a13,f9(a13,a13))+~P1(f9(a13,a13))), % 73.82/73.79 inference(scs_inference,[],[32,213,153,198,34,35,170,362,36,372,267,210,193,349,263,370,358,2,24,27,28,3,133,69,78,80,97,31,125,126])). % 73.82/73.79 cnf(409,plain, % 73.82/73.79 (E(f10(a12,a12),f9(f10(a12,a12),f10(f10(a12,a12),f10(a12,a12))))), % 73.82/73.79 inference(scs_inference,[],[291,2])). % 73.82/73.79 cnf(411,plain, % 73.82/73.79 (P5(f10(a1,f10(a1,a1)),f10(f10(a1,a1),f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[153,372,291,264,400,2,24,27])). % 73.82/73.79 cnf(412,plain, % 73.82/73.79 (P5(f10(f10(a1,a1),f10(a1,a1)),f9(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[153,396,372,291,264,243,400,2,24,27,28])). % 73.82/73.79 cnf(419,plain, % 73.82/73.79 (E(f10(a15,a15),f10(f9(f10(a15,a15),f10(a15,a15)),f10(a15,a15)))+~P1(f9(f10(a15,a15),f10(a15,a15)))), % 73.82/73.79 inference(scs_inference,[],[153,362,36,396,372,266,291,144,264,243,392,400,2,24,27,28,3,31,125,126,76,135])). % 73.82/73.79 cnf(421,plain, % 73.82/73.79 (P1(f5(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[32,54,82])). % 73.82/73.79 cnf(422,plain, % 73.82/73.79 (E(a13,f9(a13,f10(a13,a13)))), % 73.82/73.79 inference(scs_inference,[],[307,2])). % 73.82/73.79 cnf(423,plain, % 73.82/73.79 (P1(f9(a13,f10(a13,a13)))), % 73.82/73.79 inference(scs_inference,[],[34,307,2,24])). % 73.82/73.79 cnf(426,plain, % 73.82/73.79 (~E(a1,f9(a15,f10(a15,a15)))), % 73.82/73.79 inference(scs_inference,[],[34,396,42,267,307,368,411,394,2,24,27,28,3])). % 73.82/73.79 cnf(427,plain, % 73.82/73.79 (P5(f5(a1,a1),f5(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[34,421,396,42,267,307,368,411,394,2,24,27,28,3,69])). % 73.82/73.79 cnf(429,plain, % 73.82/73.79 (E(f9(a1,f10(a1,a1)),f10(f10(a1,a1),f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[34,170,174,421,396,42,267,307,368,412,411,394,2,24,27,28,3,69,78])). % 73.82/73.79 cnf(431,plain, % 73.82/73.79 (E(f10(a1,a1),f10(f10(f10(a1,a1),f10(a1,a1)),a1))), % 73.82/73.79 inference(scs_inference,[],[32,153,34,170,174,421,396,42,267,307,225,368,412,411,394,2,24,27,28,3,69,78,97])). % 73.82/73.79 cnf(434,plain, % 73.82/73.79 (E(f9(f5(a1,a1),f10(f5(a1,a1),f5(a1,a1))),f5(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[32,153,34,170,174,421,396,42,267,307,225,368,412,411,409,394,2,24,27,28,3,69,78,97,31,133])). % 73.82/73.79 cnf(438,plain, % 73.82/73.79 (P5(f9(a13,f10(a13,a13)),f9(a13,f10(a13,a13)))), % 73.82/73.79 inference(scs_inference,[],[32,153,34,170,174,421,396,42,267,307,225,368,412,411,409,394,2,24,27,28,3,69,78,97,31,133,127,61])). % 73.82/73.79 cnf(446,plain, % 73.82/73.79 (P5(f10(a1,f10(a1,a1)),f10(f10(a1,a1),a1))), % 73.82/73.79 inference(scs_inference,[],[372,429,288,2,27])). % 73.82/73.79 cnf(448,plain, % 73.82/73.79 (P5(f9(a13,f10(a13,a13)),a13)), % 73.82/73.79 inference(scs_inference,[],[153,372,429,307,288,438,431,2,27,24,28])). % 73.82/73.79 cnf(458,plain, % 73.82/73.79 (P5(f10(a12,a12),f9(f10(a12,a12),f10(f10(a12,a12),f10(a12,a12))))), % 73.82/73.79 inference(scs_inference,[],[396,324,446,269,409,2,27,28])). % 73.82/73.79 cnf(474,plain, % 73.82/73.79 (P5(f10(f10(a1,a1),a1),f10(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[267,286,273,248,394,2,27,28])). % 73.82/73.79 cnf(476,plain, % 73.82/73.79 (P5(f10(f10(a1,a1),a1),a1)), % 73.82/73.79 inference(scs_inference,[],[32,153,226,267,185,286,273,248,394,168,2,27,28,31,95])). % 73.82/73.79 cnf(487,plain, % 73.82/73.79 (P5(f10(f10(a1,a1),a1),f10(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[372,392,474,370,2,27,28])). % 73.82/73.79 cnf(488,plain, % 73.82/73.79 (E(f10(f10(a1,a1),a1),f10(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[198,226,372,392,474,370,446,2,27,28,78])). % 73.82/73.79 cnf(493,plain, % 73.82/73.79 (P5(f5(a1,a1),f9(f5(a1,a1),f5(a1,a1)))+~P1(f9(f5(a1,a1),f5(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[421,198,226,372,392,434,474,370,446,2,27,28,78,31,125,126])). % 73.82/73.79 cnf(495,plain, % 73.82/73.79 (E(f5(a1,a1),f10(f9(f5(a1,a1),f5(a1,a1)),f5(a1,a1)))+~P1(f9(f5(a1,a1),f5(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[36,421,198,226,372,43,392,434,474,370,446,2,27,28,78,31,125,126,57,135])). % 73.82/73.79 cnf(497,plain, % 73.82/73.79 (E(a15,f9(a15,f10(a15,a15)))), % 73.82/73.79 inference(scs_inference,[],[368,2])). % 73.82/73.79 cnf(498,plain, % 73.82/73.79 (P1(f9(a15,f10(a15,a15)))), % 73.82/73.79 inference(scs_inference,[],[36,368,2,24])). % 73.82/73.79 cnf(499,plain, % 73.82/73.79 (P5(a13,f9(a13,f10(a13,a13)))), % 73.82/73.79 inference(scs_inference,[],[36,307,368,438,2,24,27])). % 73.82/73.79 cnf(501,plain, % 73.82/73.79 (P2(f9(a15,f10(a15,a15)))), % 73.82/73.79 inference(scs_inference,[],[36,396,307,368,487,438,37,2,24,27,28,31])). % 73.82/73.79 cnf(502,plain, % 73.82/73.79 (P5(f9(a15,f10(a15,a15)),f9(a15,f10(a15,a15)))), % 73.82/73.79 inference(scs_inference,[],[36,396,307,368,487,438,37,2,24,27,28,31,69])). % 73.82/73.79 cnf(511,plain, % 73.82/73.79 (~P3(a1,f9(a15,f10(a15,a15)))), % 73.82/73.79 inference(scs_inference,[],[32,421,498,39,434,427,501,426,2,24,27,28,72])). % 73.82/73.79 cnf(518,plain, % 73.82/73.79 (P5(a15,f9(a15,f10(a15,a15)))), % 73.82/73.79 inference(scs_inference,[],[368,400,502,2,27])). % 73.82/73.79 cnf(519,plain, % 73.82/73.79 (P5(f9(a15,f10(a15,a15)),a15)), % 73.82/73.79 inference(scs_inference,[],[368,400,502,2,27,28])). % 73.82/73.79 cnf(526,plain, % 73.82/73.79 (E(f10(f10(f10(a1,a1),f10(a1,a1)),a1),f10(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[431,2])). % 73.82/73.79 cnf(564,plain, % 73.82/73.79 (P5(a12,a15)), % 73.82/73.79 inference(scs_inference,[],[42,162,2])). % 73.82/73.79 cnf(565,plain, % 73.82/73.79 (P5(f9(a12,f10(a12,a12)),a15)), % 73.82/73.79 inference(scs_inference,[],[302,564,27])). % 73.82/73.79 cnf(566,plain, % 73.82/73.79 (P5(a12,f9(a15,f10(a15,a15)))), % 73.82/73.79 inference(scs_inference,[],[302,497,564,27,28])). % 73.82/73.79 cnf(567,plain, % 73.82/73.79 (~P5(a15,a12)), % 73.82/73.79 inference(scs_inference,[],[33,36,43,302,497,564,27,28,78])). % 73.82/73.79 cnf(569,plain, % 73.82/73.79 (~P5(f9(a15,f10(a15,a15)),a12)), % 73.82/73.79 inference(scs_inference,[],[33,36,498,43,302,497,518,564,27,28,78,95])). % 73.82/73.79 cnf(578,plain, % 73.82/73.79 (~E(f9(a12,f10(a12,a12)),a15)), % 73.82/73.79 inference(scs_inference,[],[567,304,27])). % 73.82/73.79 cnf(579,plain, % 73.82/73.79 (~E(f9(a15,f10(a15,a15)),a12)), % 73.82/73.79 inference(scs_inference,[],[567,304,518,27,28])). % 73.82/73.79 cnf(582,plain, % 73.82/73.79 (~P5(a15,f9(a12,f10(a12,a12)))), % 73.82/73.79 inference(scs_inference,[],[33,36,305,567,304,518,306,565,564,27,28,90,78])). % 73.82/73.79 cnf(584,plain, % 73.82/73.79 (~E(a12,a15)), % 73.82/73.79 inference(scs_inference,[],[33,36,305,567,304,518,306,565,564,27,28,90,78,18])). % 73.82/73.79 cnf(588,plain, % 73.82/73.79 (P5(f9(a12,f10(a12,a12)),f9(a15,f10(a15,a15)))), % 73.82/73.79 inference(scs_inference,[],[302,566,27])). % 73.82/73.79 cnf(590,plain, % 73.82/73.79 (~P5(f9(a15,f10(a15,a15)),f9(a12,f10(a12,a12)))), % 73.82/73.79 inference(scs_inference,[],[305,498,582,302,518,566,27,28,78])). % 73.82/73.79 cnf(595,plain, % 73.82/73.79 (~E(a12,f9(a15,f10(a15,a15)))), % 73.82/73.79 inference(scs_inference,[],[590,347,27])). % 73.82/73.79 cnf(601,plain, % 73.82/73.79 (~E(f9(a12,f10(a12,a12)),f9(a15,f10(a15,a15)))), % 73.82/73.79 inference(scs_inference,[],[590,326,27])). % 73.82/73.79 cnf(649,plain, % 73.82/73.79 (E(f2(a1,f10(a1,a1)),a1)), % 73.82/73.79 inference(scs_inference,[],[213,170,46,24])). % 73.82/73.79 cnf(650,plain, % 73.82/73.79 (E(a1,f2(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[649,2])). % 73.82/73.79 cnf(651,plain, % 73.82/73.79 (P1(f2(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[32,649,2,24])). % 73.82/73.79 cnf(652,plain, % 73.82/73.79 (~P2(f2(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[32,649,142,2,24,31])). % 73.82/73.79 cnf(655,plain, % 73.82/73.79 (P3(a1,a1)), % 73.82/73.79 inference(scs_inference,[],[32,153,649,142,2,24,31,69,76])). % 73.82/73.79 cnf(657,plain, % 73.82/73.79 (P3(f10(a1,a1),a1)), % 73.82/73.79 inference(scs_inference,[],[32,153,201,649,142,2,24,31,69,76,29])). % 73.82/73.79 cnf(658,plain, % 73.82/73.79 (P3(f10(a1,a1),f10(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[32,153,201,649,142,2,24,31,69,76,29,30])). % 73.82/73.79 cnf(659,plain, % 73.82/73.79 (P5(a1,f2(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[32,153,201,649,142,2,24,31,69,76,29,30,27])). % 73.82/73.79 cnf(660,plain, % 73.82/73.79 (P5(f2(a1,f10(a1,a1)),a1)), % 73.82/73.79 inference(scs_inference,[],[32,153,201,649,142,2,24,31,69,76,29,30,27,28])). % 73.82/73.79 cnf(664,plain, % 73.82/73.79 (P3(f10(a1,f10(a1,a1)),f10(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[372,658,29])). % 73.82/73.79 cnf(666,plain, % 73.82/73.79 (P5(f2(a1,f10(a1,a1)),f10(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[201,372,658,660,29,30,28])). % 73.82/73.79 cnf(667,plain, % 73.82/73.79 (P5(f10(a1,a1),f2(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[201,372,658,659,660,29,30,28,27])). % 73.82/73.79 cnf(668,plain, % 73.82/73.79 (E(f10(a1,a1),f2(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[153,201,372,651,658,659,660,29,30,28,27,78])). % 73.82/73.79 cnf(670,plain, % 73.82/73.79 (P3(f10(a1,f10(a1,a1)),a1)), % 73.82/73.79 inference(scs_inference,[],[32,153,201,372,198,651,658,657,659,660,29,30,28,27,78,96])). % 73.82/73.79 cnf(673,plain, % 73.82/73.79 (E(f9(a1,f10(a1,a1)),f2(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[32,153,213,201,372,198,651,658,657,659,660,29,30,28,27,78,96,2,3])). % 73.82/73.79 cnf(674,plain, % 73.82/73.79 (P3(a1,f10(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[32,153,213,201,372,198,651,658,657,659,660,29,30,28,27,78,96,2,3,76])). % 73.82/73.79 cnf(676,plain, % 73.82/73.79 (E(f10(a1,a1),f10(f2(a1,f10(a1,a1)),a1))), % 73.82/73.79 inference(scs_inference,[],[32,153,213,201,372,198,651,658,657,659,660,29,30,28,27,78,96,2,3,76,97])). % 73.82/73.79 cnf(682,plain, % 73.82/73.79 (P3(f9(a1,f10(a1,a1)),f10(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[396,664,673,2,29])). % 73.82/73.79 cnf(683,plain, % 73.82/73.79 (P3(f10(a1,f10(a1,a1)),f10(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[372,396,664,673,2,29,30])). % 73.82/73.79 cnf(684,plain, % 73.82/73.79 (E(f10(a1,f10(a1,a1)),f2(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[372,396,664,673,2,29,30,3])). % 73.82/73.79 cnf(685,plain, % 73.82/73.79 (P1(f10(f2(a1,f10(a1,a1)),a1))), % 73.82/73.79 inference(scs_inference,[],[153,372,396,664,673,676,2,29,30,3,24])). % 73.82/73.79 cnf(686,plain, % 73.82/73.79 (P5(f2(a1,f10(a1,a1)),f10(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[153,372,396,664,666,673,676,2,29,30,3,24,28])). % 73.82/73.79 cnf(687,plain, % 73.82/73.79 (P5(f10(a1,f10(a1,a1)),f2(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[153,372,396,664,666,667,673,676,2,29,30,3,24,28,27])). % 73.82/73.79 cnf(688,plain, % 73.82/73.79 (P3(a1,f9(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[32,153,372,396,170,664,666,667,673,676,2,29,30,3,24,28,27,76])). % 73.82/73.79 cnf(692,plain, % 73.82/73.79 (~P3(f10(a1,a1),f9(a15,f10(a15,a15)))), % 73.82/73.79 inference(scs_inference,[],[32,153,372,396,198,170,498,511,651,664,666,667,673,676,674,2,29,30,3,24,28,27,76,78,96])). % 73.82/73.79 cnf(698,plain, % 73.82/73.79 (E(f10(f2(a1,f10(a1,a1)),a1),f10(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[676,2])). % 73.82/73.79 cnf(700,plain, % 73.82/73.79 (P3(f10(a1,f10(a1,a1)),f9(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[396,676,683,2,29,30])). % 73.82/73.79 cnf(706,plain, % 73.82/73.79 (P3(f9(a1,f10(a1,a1)),a1)), % 73.82/73.79 inference(scs_inference,[],[32,153,396,198,170,676,682,683,684,686,687,657,168,2,29,30,27,28,31,76,96])). % 73.82/73.79 cnf(719,plain, % 73.82/73.79 (P3(f10(a1,a1),f9(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[201,688,29])). % 73.82/73.79 cnf(851,plain, % 73.82/73.79 (E(f2(f10(a1,a1),a1),a1)), % 73.82/73.79 inference(scs_inference,[],[213,170,47,24])). % 73.82/73.79 cnf(852,plain, % 73.82/73.79 (E(a1,f2(f10(a1,a1),a1))), % 73.82/73.79 inference(scs_inference,[],[851,2])). % 73.82/73.79 cnf(853,plain, % 73.82/73.79 (~P2(f2(f10(a1,a1),a1))), % 73.82/73.79 inference(scs_inference,[],[851,142,2,31])). % 73.82/73.79 cnf(854,plain, % 73.82/73.79 (P1(f2(f10(a1,a1),a1))), % 73.82/73.79 inference(scs_inference,[],[32,851,142,2,31,24])). % 73.82/73.79 cnf(857,plain, % 73.82/73.79 (P5(a1,f2(f10(a1,a1),a1))), % 73.82/73.79 inference(scs_inference,[],[32,851,142,2,31,24,69,27])). % 73.82/73.79 cnf(858,plain, % 73.82/73.79 (P5(f2(f10(a1,a1),a1),a1)), % 73.82/73.79 inference(scs_inference,[],[32,851,142,2,31,24,69,27,28])). % 73.82/73.79 cnf(862,plain, % 73.82/73.79 (P5(f10(a1,a1),f2(f10(a1,a1),a1))), % 73.82/73.79 inference(scs_inference,[],[201,857,27])). % 73.82/73.79 cnf(863,plain, % 73.82/73.79 (P5(f2(f10(a1,a1),a1),f10(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[201,857,858,27,28])). % 73.82/73.79 cnf(867,plain, % 73.82/73.79 (E(f9(a1,f10(a1,a1)),f2(f10(a1,a1),a1))), % 73.82/73.79 inference(scs_inference,[],[213,201,153,854,857,858,27,28,78,2,3])). % 73.82/73.79 cnf(870,plain, % 73.82/73.79 (E(f10(a1,a1),f10(f2(f10(a1,a1),a1),a1))), % 73.82/73.79 inference(scs_inference,[],[33,32,213,423,201,153,34,854,499,857,858,27,28,78,2,3,95,97])). % 73.82/73.79 cnf(877,plain, % 73.82/73.79 (P5(f10(a1,f10(a1,a1)),f2(f10(a1,a1),a1))), % 73.82/73.79 inference(scs_inference,[],[372,396,862,867,2,3,27])). % 73.82/73.79 cnf(878,plain, % 73.82/73.79 (P5(f2(f10(a1,a1),a1),f10(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[372,396,863,862,867,2,3,27,28])). % 73.82/73.79 cnf(883,plain, % 73.82/73.79 (P3(a15,a13)+~P1(f2(a13,a13))+~P1(f2(a14,a14))), % 73.82/73.79 inference(scs_inference,[],[33,198,372,240,396,34,36,854,297,144,458,863,862,867,37,2,3,27,28,78,76,110])). % 73.82/73.79 cnf(884,plain, % 73.82/73.79 (E(f10(f2(f10(a1,a1),a1),a1),f10(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[870,2])). % 73.82/73.79 cnf(946,plain, % 73.82/73.79 (E(f9(a1,f9(a12,a12)),f9(a12,a12))), % 73.82/73.79 inference(scs_inference,[],[33,48,70])). % 73.82/73.79 cnf(947,plain, % 73.82/73.79 (E(f9(a12,a12),f9(a1,f9(a12,a12)))), % 73.82/73.79 inference(scs_inference,[],[946,2])). % 73.82/73.79 cnf(956,plain, % 73.82/73.79 (P5(f9(a1,f9(a12,a12)),f9(a1,f9(a12,a12)))+~P1(f9(a12,a12))), % 73.82/73.79 inference(scs_inference,[],[947,31,24,127,69])). % 73.82/73.79 cnf(964,plain, % 73.82/73.79 (P5(a1,f9(a12,a12))+~P1(f9(a12,a12))), % 73.82/73.79 inference(scs_inference,[],[32,946,77])). % 73.82/73.79 cnf(966,plain, % 73.82/73.79 (P5(f10(a1,a1),f9(a12,a12))+~P1(f9(a12,a12))), % 73.82/73.79 inference(scs_inference,[],[32,201,946,77,27])). % 73.82/73.79 cnf(1022,plain, % 73.82/73.79 (E(f2(a12,f2(a12,a12)),f2(a12,a12))), % 73.82/73.79 inference(scs_inference,[],[33,49,71])). % 73.82/73.79 cnf(1023,plain, % 73.82/73.79 (E(f2(a12,a12),f2(a12,f2(a12,a12)))), % 73.82/73.79 inference(scs_inference,[],[1022,2])). % 73.82/73.79 cnf(1031,plain, % 73.82/73.79 (~P1(f2(a12,a12))+P1(f2(a12,f2(a12,a12)))), % 73.82/73.79 inference(scs_inference,[],[1023,31,24])). % 73.82/73.79 cnf(1093,plain, % 73.82/73.79 (E(f9(f9(a12,a12),a1),f9(a12,a12))), % 73.82/73.79 inference(scs_inference,[],[33,50,70])). % 73.82/73.79 cnf(1094,plain, % 73.82/73.79 (E(f9(a12,a12),f9(f9(a12,a12),a1))), % 73.82/73.79 inference(scs_inference,[],[1093,2])). % 73.82/73.79 cnf(1095,plain, % 73.82/73.79 (E(f9(a1,f9(a12,a12)),f9(f9(a12,a12),a1))), % 73.82/73.79 inference(scs_inference,[],[946,1093,2,3])). % 73.82/73.79 cnf(1098,plain, % 73.82/73.79 (P5(a12,f9(a12,a12))+~P1(f9(f9(a12,a12),a1))), % 73.82/73.79 inference(scs_inference,[],[33,946,1093,2,3,31,24,126])). % 73.82/73.79 cnf(1103,plain, % 73.82/73.79 (E(f9(f9(a12,a12),a1),f9(a1,f9(a12,a12)))), % 73.82/73.79 inference(scs_inference,[],[1095,2])). % 73.82/73.79 cnf(1105,plain, % 73.82/73.79 (~P1(f9(a12,a12))+P1(f9(f9(a12,a12),a1))), % 73.82/73.79 inference(scs_inference,[],[1094,1095,2,31,24])). % 73.82/73.79 cnf(1296,plain, % 73.82/73.79 (E(f2(f10(a1,a1),a12),f10(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[201,32,51,24])). % 73.82/73.79 cnf(1297,plain, % 73.82/73.79 (E(f10(a1,a1),f2(f10(a1,a1),a12))), % 73.82/73.79 inference(scs_inference,[],[1296,2])). % 73.82/73.79 cnf(1298,plain, % 73.82/73.79 (~P2(f2(f10(a1,a1),a12))), % 73.82/73.79 inference(scs_inference,[],[1296,168,2,31])). % 73.82/73.79 cnf(1299,plain, % 73.82/73.79 (P1(f2(f10(a1,a1),a12))), % 73.82/73.79 inference(scs_inference,[],[153,1296,168,2,31,24])). % 73.82/73.79 cnf(1300,plain, % 73.82/73.79 (E(a1,f10(f10(f10(a1,a1),a1),a1))), % 73.82/73.79 inference(scs_inference,[],[201,153,273,1296,168,2,31,24,3])). % 73.82/73.79 cnf(1301,plain, % 73.82/73.79 (P5(f2(f10(a1,a1),a12),f2(f10(a1,a1),a12))), % 73.82/73.79 inference(scs_inference,[],[201,153,273,1296,168,2,31,24,3,69])). % 73.82/73.79 cnf(1303,plain, % 73.82/73.79 (P5(f2(f10(a1,a1),a12),f10(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[201,153,273,1296,168,2,31,24,3,69,28])). % 73.82/73.79 cnf(1304,plain, % 73.82/73.79 (P5(f10(a1,a1),f2(f10(a1,a1),a12))), % 73.82/73.79 inference(scs_inference,[],[201,153,273,1296,168,2,31,24,3,69,28,27])). % 73.82/73.79 cnf(1309,plain, % 73.82/73.79 (P5(f2(f10(a1,a1),a12),f10(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[372,1303,1300,2,28])). % 73.82/73.79 cnf(1310,plain, % 73.82/73.79 (P5(f10(a1,f10(a1,a1)),f2(f10(a1,a1),a12))), % 73.82/73.79 inference(scs_inference,[],[372,1303,1304,1300,2,28,27])). % 73.82/73.79 cnf(1311,plain, % 73.82/73.79 (E(a1,f10(f10(a1,f10(a1,a1)),a1))), % 73.82/73.79 inference(scs_inference,[],[201,372,400,1303,1304,1300,2,28,27,3])). % 73.82/73.79 cnf(1312,plain, % 73.82/73.79 (E(f10(a1,f10(a1,a1)),f2(f10(a1,a1),a12))), % 73.82/73.79 inference(scs_inference,[],[201,372,198,1299,400,1303,1304,1300,2,28,27,3,78])). % 73.82/73.79 cnf(1320,plain, % 73.82/73.79 (E(a1,f10(f10(f10(a1,a1),f10(a1,a1)),a1))), % 73.82/73.79 inference(scs_inference,[],[201,396,1312,431,1309,1310,2,28,27,3])). % 73.82/73.79 cnf(1321,plain, % 73.82/73.79 (E(f9(a1,f10(a1,a1)),f2(f10(a1,a1),a12))), % 73.82/73.79 inference(scs_inference,[],[201,396,170,1299,1312,431,1309,1310,2,28,27,3,78])). % 73.82/73.79 cnf(1325,plain, % 73.82/73.79 (E(f10(a1,a1),f10(f2(f10(a1,a1),a12),a1))), % 73.82/73.79 inference(scs_inference,[],[32,201,396,170,153,1299,1312,431,1309,1310,2,28,27,3,78,77,97])). % 73.82/73.79 cnf(1333,plain, % 73.82/73.79 (E(a1,f10(f2(a1,f10(a1,a1)),a1))), % 73.82/73.79 inference(scs_inference,[],[201,1321,676,2,3])). % 73.82/73.79 cnf(1338,plain, % 73.82/73.79 (E(a1,f10(f2(f10(a1,a1),a1),a1))), % 73.82/73.79 inference(scs_inference,[],[201,870,1311,2,3])). % 73.82/73.79 cnf(1346,plain, % 73.82/73.79 (E(a1,f2(f10(a1,a1),a12))), % 73.82/73.79 inference(scs_inference,[],[201,1297,1325,168,2,31,3])). % 73.82/73.79 cnf(1353,plain, % 73.82/73.79 (E(a1,f10(f2(f10(a1,a1),a12),a1))), % 73.82/73.79 inference(scs_inference,[],[201,1325,1320,2,3])). % 73.82/73.79 cnf(1359,plain, % 73.82/73.79 (E(f10(f2(a1,f10(a1,a1)),a1),a1)), % 73.82/73.79 inference(scs_inference,[],[1333,2])). % 73.82/73.79 cnf(1365,plain, % 73.82/73.79 (E(f10(f2(f10(a1,a1),a1),a1),a1)), % 73.82/73.79 inference(scs_inference,[],[1338,2])). % 73.82/73.79 cnf(1372,plain, % 73.82/73.79 (E(f2(f10(a1,a1),a12),a1)), % 73.82/73.79 inference(scs_inference,[],[1346,2])). % 73.82/73.79 cnf(1378,plain, % 73.82/73.79 (E(f10(f2(f10(a1,a1),a12),a1),a1)), % 73.82/73.79 inference(scs_inference,[],[1353,2])). % 73.82/73.79 cnf(1412,plain, % 73.82/73.79 (P5(f2(f10(a1,a1),a12),a1)), % 73.82/73.79 inference(scs_inference,[],[1372,1301,28])). % 73.82/73.79 cnf(1469,plain, % 73.82/73.79 (~P3(a15,a13)), % 73.82/73.79 inference(scs_inference,[],[35,151,71])). % 73.82/73.79 cnf(1470,plain, % 73.82/73.79 (~P1(f2(a13,a13))+~P1(f2(a14,a14))), % 73.82/73.79 inference(scs_inference,[],[1469,883])). % 73.82/73.79 cnf(1725,plain, % 73.82/73.79 (E(a15,a1)+P3(f3(a15),f9(a15,f10(a15,a15)))), % 73.82/73.79 inference(scs_inference,[],[497,181,30])). % 73.82/73.79 cnf(1741,plain, % 73.82/73.79 (~E(f3(a15),a1)), % 73.82/73.79 inference(scs_inference,[],[42,189,2])). % 73.82/73.79 cnf(1742,plain, % 73.82/73.79 (~E(f3(a15),f9(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[1741,160])). % 73.82/73.79 cnf(1743,plain, % 73.82/73.79 (~E(f3(a15),f10(f10(a1,a1),f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[1741,160,230])). % 73.82/73.79 cnf(1744,plain, % 73.82/73.79 (~E(f3(a15),f10(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[396,1741,160,230,3])). % 73.82/73.79 cnf(1747,plain, % 73.82/73.79 (~E(f3(a15),f10(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[372,1744,3])). % 73.82/73.79 cnf(1750,plain, % 73.82/73.79 (~E(f3(a15),f10(f10(a1,a1),a1))), % 73.82/73.79 inference(scs_inference,[],[488,1744,3])). % 73.82/73.79 cnf(1768,plain, % 73.82/73.79 (P5(f10(f10(a1,a1),a1),f2(f10(a1,a1),a12))), % 73.82/73.79 inference(scs_inference,[],[1312,487,28])). % 73.82/73.79 cnf(1769,plain, % 73.82/73.79 (P5(f2(f10(a1,a1),a12),f10(f10(a1,a1),f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[1312,411,487,28,27])). % 73.82/73.79 cnf(1770,plain, % 73.82/73.79 (P3(f2(f10(a1,a1),a12),f9(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[1312,411,700,487,28,27,29])). % 73.82/73.79 cnf(1772,plain, % 73.82/73.79 (P3(f2(f10(a1,a1),a12),f10(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[213,1312,411,526,700,487,1747,28,27,29,3,30])). % 73.82/73.79 cnf(1776,plain, % 73.82/73.79 (P3(f2(f10(a1,a1),a12),f10(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[372,1772,30])). % 73.82/73.79 cnf(1777,plain, % 73.82/73.79 (P5(f2(a1,f10(a1,a1)),f2(f10(a1,a1),a12))), % 73.82/73.79 inference(scs_inference,[],[1312,372,686,1772,30,28])). % 73.82/73.79 cnf(1779,plain, % 73.82/73.79 (P3(f2(f10(a1,a1),a12),a1)), % 73.82/73.79 inference(scs_inference,[],[1312,372,446,670,686,1772,30,28,27,29])). % 73.82/73.79 cnf(1781,plain, % 73.82/73.79 (E(f2(f10(a1,a1),a12),f10(f10(a1,a1),a1))), % 73.82/73.79 inference(scs_inference,[],[1312,1299,372,226,1372,446,670,686,1741,1772,1768,30,28,27,29,3,78])). % 73.82/73.79 cnf(1784,plain, % 73.82/73.79 (P3(f10(a1,a1),f10(f10(a1,a1),a1))), % 73.82/73.79 inference(scs_inference,[],[1312,1299,372,153,33,226,1372,446,670,686,1741,1772,1768,30,28,27,29,3,78,2,76])). % 73.82/73.79 cnf(1793,plain, % 73.82/73.79 (P5(f2(f10(a1,a1),a1),f2(f10(a1,a1),a12))), % 73.82/73.79 inference(scs_inference,[],[1312,692,878,1784,30,28])). % 73.82/73.79 cnf(1794,plain, % 73.82/73.79 (P5(f2(f10(a1,a1),a12),f2(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[1312,687,692,878,1784,30,28,27])). % 73.82/73.79 cnf(1795,plain, % 73.82/73.79 (P3(f10(f10(a1,a1),a1),f9(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[1312,1781,687,692,878,1770,1784,30,28,27,29])). % 73.82/73.79 cnf(1799,plain, % 73.82/73.79 (P3(a1,f2(f10(a1,a1),a12))), % 73.82/73.79 inference(scs_inference,[],[32,1312,1299,153,651,1781,698,687,692,878,1770,1784,1777,1747,30,28,27,29,3,78,76])). % 73.82/73.79 cnf(1803,plain, % 73.82/73.79 (E(f2(a1,f10(a1,a1)),f2(f10(a1,a1),a12))), % 73.82/73.79 inference(scs_inference,[],[32,1312,511,1299,153,498,651,1781,698,687,692,878,1770,1784,1777,1747,30,28,27,29,3,78,76,96,2])). % 73.82/73.79 cnf(1809,plain, % 73.82/73.79 (P5(f10(f10(a1,a1),f10(a1,a1)),f2(f10(a1,a1),a12))), % 73.82/73.79 inference(scs_inference,[],[1312,511,243,1799,30,28])). % 73.82/73.79 cnf(1810,plain, % 73.82/73.79 (P5(f2(f10(a1,a1),a12),f2(f10(a1,a1),a1))), % 73.82/73.79 inference(scs_inference,[],[1312,511,877,243,1799,30,28,27])). % 73.82/73.79 cnf(1813,plain, % 73.82/73.79 (P3(f10(a1,a1),f2(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[1312,511,153,33,651,1781,884,877,243,1776,1803,1799,1747,30,28,27,29,3,76])). % 73.82/73.79 cnf(1815,plain, % 73.82/73.79 (E(f10(f10(a1,a1),f10(a1,a1)),f2(f10(a1,a1),a12))), % 73.82/73.79 inference(scs_inference,[],[1312,511,1299,153,33,174,651,1781,884,877,243,1769,1776,1803,1799,1747,30,28,27,29,3,76,78])). % 73.82/73.79 cnf(1825,plain, % 73.82/73.79 (P5(f2(f10(a1,a1),a1),f10(f10(a1,a1),a1))), % 73.82/73.79 inference(scs_inference,[],[1781,692,1793,1813,30,28])). % 73.82/73.79 cnf(1827,plain, % 73.82/73.79 (P3(f10(a1,f10(a1,a1)),f2(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[372,1781,692,1793,1794,1813,30,28,27,29])). % 73.82/73.79 cnf(1829,plain, % 73.82/73.79 (E(f2(f10(a1,a1),a12),f2(f10(a1,a1),a1))), % 73.82/73.79 inference(scs_inference,[],[854,1299,372,1781,1378,692,1741,1793,1794,1813,1810,30,28,27,29,3,78])). % 73.82/73.79 cnf(1831,plain, % 73.82/73.79 (P3(f10(a1,a1),f10(f10(a1,a1),f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[854,153,33,1299,372,174,1781,1815,1378,692,1741,1793,1794,1813,1810,30,28,27,29,3,78,76])). % 73.82/73.79 cnf(1835,plain, % 73.82/73.79 (E(f2(f10(a1,a1),a1),f2(f10(a1,a1),a12))), % 73.82/73.79 inference(scs_inference,[],[854,153,33,1299,372,174,498,1781,1815,1378,692,1741,1793,1794,1813,1810,30,28,27,29,3,78,76,96,2])). % 73.82/73.79 cnf(1847,plain, % 73.82/73.79 (E(f10(f10(a1,a1),a1),f10(f10(a1,a1),f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[32,153,1299,372,226,174,1781,1829,692,1831,1809,1769,30,27,28,29,76,78,2])). % 73.82/73.79 cnf(1856,plain, % 73.82/73.79 (P3(f10(a1,a1),f2(f10(a1,a1),a1))), % 73.82/73.79 inference(scs_inference,[],[854,153,33,226,1781,1835,1779,1825,1777,1810,28,27,29,78,76])). % 73.82/73.79 cnf(1860,plain, % 73.82/73.79 (~P3(f2(f10(a1,a1),a1),f9(a15,f10(a15,a15)))), % 73.82/73.79 inference(scs_inference,[],[32,854,153,33,226,498,1781,692,1795,1835,1779,1825,1777,1810,28,27,29,78,76,111,96])). % 73.82/73.79 cnf(1879,plain, % 73.82/73.79 (P3(f10(a1,f10(a1,a1)),f10(f10(a1,a1),a1))), % 73.82/73.79 inference(scs_inference,[],[372,1784,29])). % 73.82/73.79 cnf(1897,plain, % 73.82/73.79 (P3(f10(a1,f10(a1,a1)),f2(f10(a1,a1),a1))), % 73.82/73.79 inference(scs_inference,[],[372,1856,29])). % 73.82/73.79 cnf(1941,plain, % 73.82/73.79 (P3(f2(f10(a1,a1),a1),a1)), % 73.82/73.79 inference(scs_inference,[],[1829,1779,29])). % 73.82/73.79 cnf(1959,plain, % 73.82/73.79 (P3(f2(f10(a1,a1),a12),f2(f10(a1,a1),a1))), % 73.82/73.79 inference(scs_inference,[],[1312,1897,29])). % 73.82/73.79 cnf(1972,plain, % 73.82/73.79 (P3(f2(f10(a1,a1),a1),f2(f10(a1,a1),a1))), % 73.82/73.79 inference(scs_inference,[],[1829,1959,29])). % 73.82/73.79 cnf(2817,plain, % 73.82/73.79 (P5(f9(a12,a12),f9(a1,f9(a12,a12)))+~P1(f9(a1,f9(a12,a12)))+~P1(f9(a12,a12))), % 73.82/73.79 inference(scs_inference,[],[36,32,1103,1741,77])). % 73.82/73.79 cnf(2818,plain, % 73.82/73.79 (~P3(a15,f3(a15))+P5(a15,f3(a15))+~P1(f3(a15))), % 73.82/73.79 inference(scs_inference,[],[36,1741,73])). % 73.82/73.79 cnf(2820,plain, % 73.82/73.79 (~P1(f3(a15))+E(a15,f2(f3(a15),f11(a15,f3(a15))))+~P3(f3(a15),a15)), % 73.82/73.79 inference(scs_inference,[],[36,1741,43,134])). % 73.82/73.79 cnf(2829,plain, % 73.82/73.79 (P5(f10(f10(a1,a1),f10(a1,a1)),f2(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[668,396,264,322,1827,27,29,28])). % 73.82/73.79 cnf(2832,plain, % 73.82/73.79 (E(f2(a1,f10(a1,a1)),f10(f10(a1,a1),f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[651,668,396,174,264,322,1827,27,29,28,78,2])). % 73.82/73.79 cnf(2833,plain, % 73.82/73.79 (P3(a1,f10(f10(a1,a1),f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[32,651,668,153,396,174,264,322,1827,27,29,28,78,2,76])). % 73.82/73.79 cnf(2854,plain, % 73.82/73.79 (P3(f9(a1,f10(a1,a1)),f10(f10(a1,a1),a1))), % 73.82/73.79 inference(scs_inference,[],[396,1879,29])). % 73.82/73.79 cnf(2864,plain, % 73.82/73.79 (P3(f2(a1,f10(a1,a1)),f9(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[668,719,29])). % 73.82/73.79 cnf(2868,plain, % 73.82/73.79 (P3(f2(a1,f10(a1,a1)),a1)), % 73.82/73.79 inference(scs_inference,[],[668,657,29])). % 73.82/73.79 cnf(2869,plain, % 73.82/73.79 (P3(f2(a1,f10(a1,a1)),f10(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[32,651,153,668,657,2864,29,111])). % 73.82/73.79 cnf(2919,plain, % 73.82/73.79 (E(f9(a1,a1),a1)), % 73.82/73.79 inference(scs_inference,[],[32,48])). % 73.82/73.79 cnf(2921,plain, % 73.82/73.79 (E(f2(a12,a1),a1)), % 73.82/73.79 inference(scs_inference,[],[32,48,49])). % 73.82/73.79 cnf(2925,plain, % 73.82/73.79 (E(f2(a1,a12),a1)), % 73.82/73.79 inference(scs_inference,[],[32,375,48,49,50,51])). % 73.82/73.79 cnf(2927,plain, % 73.82/73.79 (E(f2(a1,a1),a1)), % 73.82/73.79 inference(scs_inference,[],[32,375,48,49,50,51,46])). % 73.82/73.79 cnf(2933,plain, % 73.82/73.79 (E(f2(a1,x29331),f2(f2(a1,f10(a1,a1)),x29331))), % 73.82/73.79 inference(scs_inference,[],[32,650,375,48,49,50,51,46,47,22,23,4])). % 73.82/73.79 cnf(2936,plain, % 73.82/73.79 (E(f9(x29361,a1),f9(x29361,f2(a1,f10(a1,a1))))), % 73.82/73.79 inference(scs_inference,[],[32,650,375,48,49,50,51,46,47,22,23,4,5,12,13])). % 73.82/73.79 cnf(2942,plain, % 73.82/73.79 (E(f6(a1,x29421),f6(f2(a1,f10(a1,a1)),x29421))), % 73.82/73.79 inference(scs_inference,[],[32,650,375,48,49,50,51,46,47,22,23,4,5,12,13,14,15,16,17,19,20])). % 73.82/73.79 cnf(2951,plain, % 73.82/73.79 (~E(f9(a14,f10(a14,a14)),a1)), % 73.82/73.79 inference(scs_inference,[],[32,323,650,375,48,49,50,51,46,47,22,23,4,5,12,13,14,15,16,17,19,20,21,6,7,8,9,10,11,18,2])). % 73.82/73.79 cnf(2952,plain, % 73.82/73.79 (P1(f9(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[32,323,650,375,48,49,50,51,46,47,22,23,4,5,12,13,14,15,16,17,19,20,21,6,7,8,9,10,11,18,2,70])). % 73.82/73.79 cnf(2954,plain, % 73.82/73.79 (~P3(f2(f10(a1,a1),a1),a15)), % 73.82/73.79 inference(scs_inference,[],[32,323,650,1860,375,497,48,49,50,51,46,47,22,23,4,5,12,13,14,15,16,17,19,20,21,6,7,8,9,10,11,18,2,70,30])). % 73.82/73.79 cnf(2955,plain, % 73.82/73.79 (P1(f2(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[32,323,650,1860,375,497,48,49,50,51,46,47,22,23,4,5,12,13,14,15,16,17,19,20,21,6,7,8,9,10,11,18,2,70,30,71])). % 73.82/73.79 cnf(2958,plain, % 73.82/73.79 (~E(f9(a15,f10(a15,a15)),a1)), % 73.82/73.79 inference(scs_inference,[],[32,323,289,650,1860,501,375,497,498,48,49,50,51,46,47,22,23,4,5,12,13,14,15,16,17,19,20,21,6,7,8,9,10,11,18,2,70,30,71,31,44])). % 73.82/73.79 cnf(2967,plain, % 73.82/73.79 (P1(f3(f9(a15,f10(a15,a15))))), % 73.82/73.79 inference(scs_inference,[],[32,2869,323,289,650,208,1365,1860,145,167,501,375,378,651,497,579,498,153,48,49,50,51,46,47,22,23,4,5,12,13,14,15,16,17,19,20,21,6,7,8,9,10,11,18,2,70,30,71,31,44,27,3,29,82,83,52])). % 73.82/73.79 cnf(2971,plain, % 73.82/73.79 (E(f2(a1,f6(a1,a1)),a1)), % 73.82/73.79 inference(scs_inference,[],[32,2869,323,289,650,208,1365,1860,655,145,167,501,375,378,388,651,497,579,498,153,48,49,50,51,46,47,22,23,4,5,12,13,14,15,16,17,19,20,21,6,7,8,9,10,11,18,2,70,30,71,31,44,27,3,29,82,83,52,75,92])). % 73.82/73.79 cnf(2973,plain, % 73.82/73.79 (E(f9(a1,f5(a1,a1)),a1)), % 73.82/73.79 inference(scs_inference,[],[32,2869,323,289,650,208,1365,1860,655,145,167,501,375,378,147,388,651,497,579,498,153,48,49,50,51,46,47,22,23,4,5,12,13,14,15,16,17,19,20,21,6,7,8,9,10,11,18,2,70,30,71,31,44,27,3,29,82,83,52,75,92,93])). % 73.82/73.79 cnf(2987,plain, % 73.82/73.79 (P3(a1,f2(a1,f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[32,2869,323,289,650,208,1365,1359,1860,655,145,167,501,375,378,147,388,685,651,497,579,498,153,48,49,50,51,46,47,22,23,4,5,12,13,14,15,16,17,19,20,21,6,7,8,9,10,11,18,2,70,30,71,31,44,27,3,29,82,83,52,75,92,93,103,104,113,114,64,61,125])). % 73.82/73.79 cnf(2989,plain, % 73.82/73.79 (P2(f3(f9(a15,f10(a15,a15))))), % 73.82/73.79 inference(scs_inference,[],[32,2869,323,289,650,208,1365,1359,1860,655,145,167,501,375,378,147,388,685,651,497,579,498,153,48,49,50,51,46,47,22,23,4,5,12,13,14,15,16,17,19,20,21,6,7,8,9,10,11,18,2,70,30,71,31,44,27,3,29,82,83,52,75,92,93,103,104,113,114,64,61,125,53])). % 73.82/73.79 cnf(2993,plain, % 73.82/73.79 (P5(a1,f9(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[32,2869,323,289,650,208,1365,1359,1860,655,145,167,501,375,378,147,388,685,651,497,579,498,153,48,49,50,51,46,47,22,23,4,5,12,13,14,15,16,17,19,20,21,6,7,8,9,10,11,18,2,70,30,71,31,44,27,3,29,82,83,52,75,92,93,103,104,113,114,64,61,125,53,63,126])). % 73.82/73.79 cnf(2999,plain, % 73.82/73.79 (~E(f9(a1,a12),f9(a1,a15))), % 73.82/73.79 inference(scs_inference,[],[32,584,2869,323,289,601,650,208,1365,1359,1860,655,145,588,476,167,501,375,378,147,388,685,651,497,226,305,579,498,153,33,36,48,49,50,51,46,47,22,23,4,5,12,13,14,15,16,17,19,20,21,6,7,8,9,10,11,18,2,70,30,71,31,44,27,3,29,82,83,52,75,92,93,103,104,113,114,64,61,125,53,63,126,127,74,84])). % 73.82/73.79 cnf(3001,plain, % 73.82/73.79 (~E(f9(a12,a1),f9(a15,a1))), % 73.82/73.79 inference(scs_inference,[],[32,584,2869,323,289,601,650,208,1365,1359,1860,655,145,588,476,167,501,375,378,147,388,685,651,497,226,305,579,498,153,33,36,48,49,50,51,46,47,22,23,4,5,12,13,14,15,16,17,19,20,21,6,7,8,9,10,11,18,2,70,30,71,31,44,27,3,29,82,83,52,75,92,93,103,104,113,114,64,61,125,53,63,126,127,74,84,85])). % 73.82/73.79 cnf(3003,plain, % 73.82/73.79 (~E(f2(a1,a1),a15)), % 73.82/73.79 inference(scs_inference,[],[32,584,2869,323,289,601,650,208,1365,1359,1860,655,145,588,476,167,39,501,42,375,378,147,388,685,651,497,226,305,579,498,153,33,36,48,49,50,51,46,47,22,23,4,5,12,13,14,15,16,17,19,20,21,6,7,8,9,10,11,18,2,70,30,71,31,44,27,3,29,82,83,52,75,92,93,103,104,113,114,64,61,125,53,63,126,127,74,84,85,65])). % 73.82/73.79 cnf(3007,plain, % 73.82/73.79 (E(f9(f10(a1,a1),f2(a1,f10(a1,a1))),f10(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[32,584,2869,323,289,2832,601,650,208,1365,1359,1860,655,145,588,476,167,39,501,42,375,172,378,147,388,685,651,497,226,305,579,498,153,33,36,48,49,50,51,46,47,22,23,4,5,12,13,14,15,16,17,19,20,21,6,7,8,9,10,11,18,2,70,30,71,31,44,27,3,29,82,83,52,75,92,93,103,104,113,114,64,61,125,53,63,126,127,74,84,85,65,66,90])). % 73.82/73.79 cnf(3011,plain, % 73.82/73.79 (E(a1,f10(f9(a1,a1),a1))), % 73.82/73.79 inference(scs_inference,[],[32,584,2869,323,289,2829,2832,601,650,208,1365,1359,1860,655,145,588,476,167,39,501,42,375,172,378,147,388,685,651,497,226,305,174,579,498,153,33,36,48,49,50,51,46,47,22,23,4,5,12,13,14,15,16,17,19,20,21,6,7,8,9,10,11,18,2,70,30,71,31,44,27,3,29,82,83,52,75,92,93,103,104,113,114,64,61,125,53,63,126,127,74,84,85,65,66,90,80,135])). % 73.82/73.79 cnf(3027,plain, % 73.82/73.79 (~P3(a15,f2(a13,a13))), % 73.82/73.79 inference(scs_inference,[],[32,584,2869,323,569,595,289,2829,2832,601,650,208,1365,1359,1860,655,1941,145,1469,566,588,476,167,39,501,194,42,375,172,378,37,147,388,685,854,651,497,226,305,174,579,498,153,33,34,36,48,49,50,51,46,47,22,23,4,5,12,13,14,15,16,17,19,20,21,6,7,8,9,10,11,18,2,70,30,71,31,44,27,3,29,82,83,52,75,92,93,103,104,113,114,64,61,125,53,63,126,127,74,84,85,65,66,90,80,135,77,76,106,107,97,111,105,110])). % 73.82/73.79 cnf(3029,plain, % 73.82/73.79 (P5(f9(a1,a1),f9(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[32,584,2869,323,569,595,289,2829,2832,601,650,208,1365,1359,1860,655,1941,145,1469,566,588,476,167,39,501,194,42,375,172,378,37,147,388,685,854,651,497,226,305,174,579,498,153,33,34,36,48,49,50,51,46,47,22,23,4,5,12,13,14,15,16,17,19,20,21,6,7,8,9,10,11,18,2,70,30,71,31,44,27,3,29,82,83,52,75,92,93,103,104,113,114,64,61,125,53,63,126,127,74,84,85,65,66,90,80,135,77,76,106,107,97,111,105,110,54])). % 73.82/73.79 cnf(3042,plain, % 73.82/73.79 (P3(a1,f2(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[2955,235])). % 73.82/73.79 cnf(3070,plain, % 73.82/73.79 (E(f7(f9(a1,a1),x30701,x30702),f7(a1,x30701,x30702))), % 73.82/73.79 inference(scs_inference,[],[2952,2919,47,50,48,9])). % 73.82/73.79 cnf(3071,plain, % 73.82/73.79 (E(f2(x30711,f9(a1,a1)),f2(x30711,a1))), % 73.82/73.79 inference(scs_inference,[],[2952,2919,47,50,48,9,5])). % 73.82/73.79 cnf(3072,plain, % 73.82/73.79 (E(f9(f9(a1,a1),x30721),f9(a1,x30721))), % 73.82/73.79 inference(scs_inference,[],[2952,2919,47,50,48,9,5,12])). % 73.82/73.79 cnf(3075,plain, % 73.82/73.79 (E(f8(x30751,f9(a1,a1),x30752),f8(x30751,a1,x30752))), % 73.82/73.79 inference(scs_inference,[],[2952,2919,47,50,48,9,5,12,21,15,7])). % 73.82/73.79 cnf(3076,plain, % 73.82/73.79 (E(f9(x30761,f9(a1,a1)),f9(x30761,a1))), % 73.82/73.79 inference(scs_inference,[],[2952,2919,47,50,48,9,5,12,21,15,7,13])). % 73.82/73.79 cnf(3077,plain, % 73.82/73.79 (E(f2(a1,f9(a1,a1)),a1)), % 73.82/73.79 inference(scs_inference,[],[2952,2919,47,50,48,9,5,12,21,15,7,13,46])). % 73.82/73.79 cnf(3079,plain, % 73.82/73.79 (E(f5(x30791,f9(a1,a1)),f5(x30791,a1))), % 73.82/73.79 inference(scs_inference,[],[2952,2919,47,50,48,9,5,12,21,15,7,13,46,17])). % 73.82/73.79 cnf(3080,plain, % 73.82/73.79 (E(f9(f9(a1,a1),f10(a1,a1)),a1)), % 73.82/73.79 inference(scs_inference,[],[2952,2919,47,50,48,9,5,12,21,15,7,13,46,17,160])). % 73.82/73.79 cnf(3082,plain, % 73.82/73.79 (E(f5(f9(a1,a1),x30821),f5(a1,x30821))), % 73.82/73.79 inference(scs_inference,[],[2952,2919,47,50,48,9,5,12,21,15,7,13,46,17,160,14,16])). % 73.82/73.79 cnf(3083,plain, % 73.82/73.79 (E(f2(a12,f9(a1,a1)),f9(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[2952,2919,47,50,48,9,5,12,21,15,7,13,46,17,160,14,16,49])). % 73.82/73.79 cnf(3085,plain, % 73.82/73.79 (E(f2(f9(a1,a1),x30851),f2(a1,x30851))), % 73.82/73.79 inference(scs_inference,[],[2952,2919,47,50,48,9,5,12,21,15,7,13,46,17,160,14,16,49,4])). % 73.82/73.79 cnf(3086,plain, % 73.82/73.79 (E(f7(x30861,x30862,f9(a1,a1)),f7(x30861,x30862,a1))), % 73.82/73.79 inference(scs_inference,[],[2952,2919,47,50,48,9,5,12,21,15,7,13,46,17,160,14,16,49,4,11])). % 73.82/73.79 cnf(3087,plain, % 73.82/73.79 (E(f2(f9(a1,a1),a12),f9(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[2952,2919,47,50,48,9,5,12,21,15,7,13,46,17,160,14,16,49,4,11,51])). % 73.82/73.79 cnf(3090,plain, % 73.82/73.79 (P5(f2(a1,a1),f2(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[2952,2955,2919,47,50,48,9,5,12,21,15,7,13,46,17,160,14,16,49,4,11,51,23,54])). % 73.82/73.79 cnf(3095,plain, % 73.82/73.79 (E(f8(x30951,x30952,f9(a1,a1)),f8(x30951,x30952,a1))), % 73.82/73.79 inference(scs_inference,[],[2952,2955,2919,47,50,48,9,5,12,21,15,7,13,46,17,160,14,16,49,4,11,51,23,54,10,20,22,8])). % 73.82/73.79 cnf(3097,plain, % 73.82/73.79 (E(f10(x30971,f9(a1,a1)),f10(x30971,a1))), % 73.82/73.79 inference(scs_inference,[],[2952,2955,2919,47,50,48,9,5,12,21,15,7,13,46,17,160,14,16,49,4,11,51,23,54,10,20,22,8,6,19])). % 73.82/73.79 cnf(3098,plain, % 73.82/73.79 (E(f10(f9(a1,a1),x30981),f10(a1,x30981))), % 73.82/73.79 inference(scs_inference,[],[2952,2955,2919,47,50,48,9,5,12,21,15,7,13,46,17,160,14,16,49,4,11,51,23,54,10,20,22,8,6,19,18])). % 73.82/73.79 cnf(3099,plain, % 73.82/73.79 (~E(f9(a1,a15),f9(a1,a12))), % 73.82/73.79 inference(scs_inference,[],[2952,2955,2919,2999,47,50,48,9,5,12,21,15,7,13,46,17,160,14,16,49,4,11,51,23,54,10,20,22,8,6,19,18,2])). % 73.82/73.79 cnf(3100,plain, % 73.82/73.79 (P1(f9(f9(a1,a1),f9(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[2952,2955,2919,2999,47,50,48,9,5,12,21,15,7,13,46,17,160,14,16,49,4,11,51,23,54,10,20,22,8,6,19,18,2,70])). % 73.82/73.79 cnf(3104,plain, % 73.82/73.79 (P1(f2(f9(a1,a1),f9(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[2952,2955,2919,2999,2967,2989,47,50,48,9,5,12,21,15,7,13,46,17,160,14,16,49,4,11,51,23,54,10,20,22,8,6,19,18,2,70,45,71])). % 73.82/73.79 cnf(3107,plain, % 73.82/73.79 (~P2(f9(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[2952,2955,2919,2999,2868,3011,2967,2989,47,50,48,9,5,12,21,15,7,13,46,17,160,14,16,49,4,11,51,23,54,10,20,22,8,6,19,18,2,70,45,71,30,44])). % 73.82/73.79 cnf(3110,plain, % 73.82/73.79 (E(f9(a1,a1),f10(f9(a1,a1),a1))), % 73.82/73.79 inference(scs_inference,[],[2952,2955,2919,2999,2868,3011,2967,2989,142,47,50,48,9,5,12,21,15,7,13,46,17,160,14,16,49,4,11,51,23,54,10,20,22,8,6,19,18,2,70,45,71,30,44,31,3])). % 73.82/73.79 cnf(3111,plain, % 73.82/73.79 (~P3(f9(a1,a1),a15)), % 73.82/73.79 inference(scs_inference,[],[2952,2955,2919,2999,2868,3011,2967,2989,145,142,47,50,48,9,5,12,21,15,7,13,46,17,160,14,16,49,4,11,51,23,54,10,20,22,8,6,19,18,2,70,45,71,30,44,31,3,29])). % 73.82/73.79 cnf(3124,plain, % 73.82/73.79 (P1(f5(a1,f9(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[32,2952,2955,2993,2919,2999,2868,3011,2967,2989,145,658,142,153,33,47,50,48,9,5,12,21,15,7,13,46,17,160,14,16,49,4,11,51,23,54,10,20,22,8,6,19,18,2,70,45,71,30,44,31,3,29,103,114,104,92,93,113,82])). % 73.82/73.79 cnf(3126,plain, % 73.82/73.79 (P1(f6(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[32,2952,2955,2993,2919,2999,2868,3011,2967,2989,655,145,658,142,153,33,47,50,48,9,5,12,21,15,7,13,46,17,160,14,16,49,4,11,51,23,54,10,20,22,8,6,19,18,2,70,45,71,30,44,31,3,29,103,114,104,92,93,113,82,83])). % 73.82/73.79 cnf(3130,plain, % 73.82/73.79 (P5(a12,f3(f9(a15,f10(a15,a15))))), % 73.82/73.79 inference(scs_inference,[],[32,2952,2955,2993,2919,2999,2868,3011,2967,2989,655,145,658,142,153,33,47,50,48,9,5,12,21,15,7,13,46,17,160,14,16,49,4,11,51,23,54,10,20,22,8,6,19,18,2,70,45,71,30,44,31,3,29,103,114,104,92,93,113,82,83,133,56])). % 73.82/73.79 cnf(3134,plain, % 73.82/73.79 (E(f9(a1,a1),f10(f10(a1,a1),a1))), % 73.82/73.79 inference(scs_inference,[],[32,2952,2955,2993,2919,2999,2868,3011,2967,2989,655,1300,145,658,142,271,565,226,578,305,153,33,36,47,50,48,9,5,12,21,15,7,13,46,17,160,14,16,49,4,11,51,23,54,10,20,22,8,6,19,18,2,70,45,71,30,44,31,3,29,103,114,104,92,93,113,82,83,133,56,74,90])). % 73.82/73.79 cnf(3136,plain, % 73.82/73.79 (P1(f9(f10(a1,a1),f2(a1,f10(a1,a1))))), % 73.82/73.79 inference(scs_inference,[],[32,2952,2955,2993,2919,2999,2868,3011,3007,2967,2989,655,1300,145,658,142,271,565,147,226,578,305,153,33,36,47,50,48,9,5,12,21,15,7,13,46,17,160,14,16,49,4,11,51,23,54,10,20,22,8,6,19,18,2,70,45,71,30,44,31,3,29,103,114,104,92,93,113,82,83,133,56,74,90,80])). % 73.82/73.79 cnf(3138,plain, % 73.82/73.79 (P5(f9(a12,a1),f9(a15,a1))), % 73.82/73.79 inference(scs_inference,[],[32,2952,2955,2993,2919,2999,2868,3011,3007,2967,2989,655,1300,145,584,658,142,271,565,564,147,226,578,305,153,33,36,47,50,48,9,5,12,21,15,7,13,46,17,160,14,16,49,4,11,51,23,54,10,20,22,8,6,19,18,2,70,45,71,30,44,31,3,29,103,114,104,92,93,113,82,83,133,56,74,90,80,107])). % 73.82/73.79 cnf(3140,plain, % 73.82/73.79 (P5(f9(a1,a12),f9(a1,a15))), % 73.82/73.79 inference(scs_inference,[],[32,2952,2955,2993,2919,2999,2868,3011,3007,2967,2989,655,1300,145,584,658,142,271,565,564,147,226,578,305,153,33,36,47,50,48,9,5,12,21,15,7,13,46,17,160,14,16,49,4,11,51,23,54,10,20,22,8,6,19,18,2,70,45,71,30,44,31,3,29,103,114,104,92,93,113,82,83,133,56,74,90,80,107,106])). % 73.82/73.79 cnf(3144,plain, % 73.82/73.79 (P3(f2(a1,f10(a1,a1)),f9(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[32,2952,2955,2993,2919,2999,2868,3011,3007,2967,2989,2854,655,1795,1300,145,584,658,142,271,565,564,147,651,226,578,305,170,153,33,36,47,50,48,9,5,12,21,15,7,13,46,17,160,14,16,49,4,11,51,23,54,10,20,22,8,6,19,18,2,70,45,71,30,44,31,3,29,103,114,104,92,93,113,82,83,133,56,74,90,80,107,106,96,105])). % 73.82/73.79 cnf(3148,plain, % 73.82/73.79 (P5(a1,f2(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[32,2952,2955,2993,2919,2927,2999,2868,3011,3007,2967,2989,2854,655,1795,1300,145,584,658,142,271,565,564,147,651,226,578,305,170,153,33,36,38,47,50,48,9,5,12,21,15,7,13,46,17,160,14,16,49,4,11,51,23,54,10,20,22,8,6,19,18,2,70,45,71,30,44,31,3,29,103,114,104,92,93,113,82,83,133,56,74,90,80,107,106,96,105,89,61])). % 73.82/73.79 cnf(3150,plain, % 73.82/73.79 (P3(f9(a1,a1),f2(f9(a1,a1),f9(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[32,2952,2955,2993,2919,2927,2999,2868,3011,3007,2967,2989,2854,655,1795,1300,145,584,658,142,271,565,564,147,651,226,578,305,170,153,33,36,38,47,50,48,9,5,12,21,15,7,13,46,17,160,14,16,49,4,11,51,23,54,10,20,22,8,6,19,18,2,70,45,71,30,44,31,3,29,103,114,104,92,93,113,82,83,133,56,74,90,80,107,106,96,105,89,61,125])). % 73.82/73.79 cnf(3152,plain, % 73.82/73.79 (P5(f9(a1,a1),f9(f9(a1,a1),f9(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[32,2952,2955,2993,2919,2927,2999,2868,3011,3007,2967,2989,2854,655,1795,1300,145,584,658,142,271,565,564,147,651,226,578,305,170,153,33,36,38,47,50,48,9,5,12,21,15,7,13,46,17,160,14,16,49,4,11,51,23,54,10,20,22,8,6,19,18,2,70,45,71,30,44,31,3,29,103,114,104,92,93,113,82,83,133,56,74,90,80,107,106,96,105,89,61,125,126])). % 73.82/73.79 cnf(3154,plain, % 73.82/73.79 (P1(f10(f9(a1,a1),a1))), % 73.82/73.79 inference(scs_inference,[],[32,2952,2955,2993,2919,2927,2999,2868,3011,3007,2967,2989,2854,655,1795,1300,145,584,658,142,271,565,564,147,651,226,578,305,170,153,33,36,38,47,50,48,9,5,12,21,15,7,13,46,17,160,14,16,49,4,11,51,23,54,10,20,22,8,6,19,18,2,70,45,71,30,44,31,3,29,103,114,104,92,93,113,82,83,133,56,74,90,80,107,106,96,105,89,61,125,126,127])). % 73.82/73.79 cnf(3156,plain, % 73.82/73.79 (~P5(f3(f9(a15,f10(a15,a15))),a12)), % 73.82/73.79 inference(scs_inference,[],[32,2952,2955,2993,2919,2927,2999,2868,3011,3007,2967,2989,2854,655,1795,1300,145,584,658,142,271,565,564,147,651,226,578,305,170,153,33,36,38,47,50,48,9,5,12,21,15,7,13,46,17,160,14,16,49,4,11,51,23,54,10,20,22,8,6,19,18,2,70,45,71,30,44,31,3,29,103,114,104,92,93,113,82,83,133,56,74,90,80,107,106,96,105,89,61,125,126,127,78])). % 73.82/73.79 cnf(3175,plain, % 73.82/73.79 (E(f9(f6(a1,a1),a1),f6(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[3126,3100,47,48,46,49,51,50])). % 73.82/73.79 cnf(3177,plain, % 73.82/73.79 (P5(f6(a1,a1),f6(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[3126,3100,47,48,46,49,51,50,54])). % 73.82/73.79 cnf(3179,plain, % 73.82/73.79 (E(f9(x31791,f2(a1,a12)),f9(x31791,a1))), % 73.82/73.79 inference(scs_inference,[],[2925,3126,3100,47,48,46,49,51,50,54,13])). % 73.82/73.79 cnf(3183,plain, % 73.82/73.79 (E(f9(f2(a1,a12),f10(a1,a1)),a1)), % 73.82/73.79 inference(scs_inference,[],[2925,3126,3100,47,48,46,49,51,50,54,13,14,17,12,160])). % 73.82/73.79 cnf(3197,plain, % 73.82/73.79 (E(f10(x31971,f2(a1,a12)),f10(x31971,a1))), % 73.82/73.79 inference(scs_inference,[],[2925,3126,3100,47,48,46,49,51,50,54,13,14,17,12,160,7,16,15,20,5,21,9,11,4,8,22,23,10,19])). % 73.82/73.79 cnf(3199,plain, % 73.82/73.79 (E(f10(f2(a1,a12),x31991),f10(a1,x31991))), % 73.82/73.79 inference(scs_inference,[],[2925,3126,3100,47,48,46,49,51,50,54,13,14,17,12,160,7,16,15,20,5,21,9,11,4,8,22,23,10,19,6,18])). % 73.82/73.79 cnf(3200,plain, % 73.82/73.79 (~E(a15,f2(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[2925,3126,3003,3100,47,48,46,49,51,50,54,13,14,17,12,160,7,16,15,20,5,21,9,11,4,8,22,23,10,19,6,18,2])). % 73.82/73.79 cnf(3201,plain, % 73.82/73.79 (P1(f9(f6(a1,a1),f6(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[2925,3126,3003,3100,47,48,46,49,51,50,54,13,14,17,12,160,7,16,15,20,5,21,9,11,4,8,22,23,10,19,6,18,2,70])). % 73.82/73.79 cnf(3203,plain, % 73.82/73.79 (P1(f2(f6(a1,a1),f6(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[2925,3126,3003,3100,47,48,46,49,51,50,54,13,14,17,12,160,7,16,15,20,5,21,9,11,4,8,22,23,10,19,6,18,2,70,71])). % 73.82/73.79 cnf(3206,plain, % 73.82/73.79 (~E(a15,a1)), % 73.82/73.79 inference(scs_inference,[],[2925,3126,3003,3027,3100,37,36,38,47,48,46,49,51,50,54,13,14,17,12,160,7,16,15,20,5,21,9,11,4,8,22,23,10,19,6,18,2,70,71,30,44])). % 73.82/73.79 cnf(3213,plain, % 73.82/73.79 (~P3(f9(a15,f10(a15,a15)),f2(a13,a13))), % 73.82/73.79 inference(scs_inference,[],[3107,2925,3126,3003,3027,3100,2933,2942,2989,368,37,36,38,47,48,46,49,51,50,54,13,14,17,12,160,7,16,15,20,5,21,9,11,4,8,22,23,10,19,6,18,2,70,71,30,44,31,24,3,29])). % 73.82/73.79 cnf(3220,plain, % 73.82/73.79 (~E(f9(a15,a15),a1)), % 73.82/73.79 inference(scs_inference,[],[3090,3107,2925,3126,3003,3027,3100,2933,2942,2989,2955,368,37,34,36,38,47,48,46,49,51,50,54,13,14,17,12,160,7,16,15,20,5,21,9,11,4,8,22,23,10,19,6,18,2,70,71,30,44,31,24,3,29,75,114,93,64])). % 73.82/73.79 cnf(3222,plain, % 73.82/73.79 (P1(f3(a15))), % 73.82/73.79 inference(scs_inference,[],[3090,3107,2925,3126,3003,3027,3100,2933,2942,2989,2955,368,37,34,36,43,38,47,48,46,49,51,50,54,13,14,17,12,160,7,16,15,20,5,21,9,11,4,8,22,23,10,19,6,18,2,70,71,30,44,31,24,3,29,75,114,93,64,52])). % 73.82/73.79 cnf(3232,plain, % 73.82/73.79 (P3(f3(a15),a15)), % 73.82/73.79 inference(scs_inference,[],[32,3042,3090,3107,2925,3126,3003,3027,3100,2933,2942,2989,2955,368,37,34,36,43,38,47,48,46,49,51,50,54,13,14,17,12,160,7,16,15,20,5,21,9,11,4,8,22,23,10,19,6,18,2,70,71,30,44,31,24,3,29,75,114,93,64,52,103,104,92,113,60])). % 73.82/73.79 cnf(3234,plain, % 73.82/73.79 (P1(f5(f2(a1,a1),f2(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[32,3042,3090,3107,2925,3126,3003,3027,3100,2933,2942,2989,2955,368,37,34,36,43,38,47,48,46,49,51,50,54,13,14,17,12,160,7,16,15,20,5,21,9,11,4,8,22,23,10,19,6,18,2,70,71,30,44,31,24,3,29,75,114,93,64,52,103,104,92,113,60,82])). % 73.82/73.79 cnf(3238,plain, % 73.82/73.79 (P2(f3(a15))), % 73.82/73.79 inference(scs_inference,[],[32,3042,3090,3107,2925,3126,3003,3027,3100,2933,2942,2989,2955,368,37,34,36,43,38,47,48,46,49,51,50,54,13,14,17,12,160,7,16,15,20,5,21,9,11,4,8,22,23,10,19,6,18,2,70,71,30,44,31,24,3,29,75,114,93,64,52,103,104,92,113,60,82,83,53])). % 73.82/73.79 cnf(3240,plain, % 73.82/73.79 (~E(a12,f3(f9(a15,f10(a15,a15))))), % 73.82/73.79 inference(scs_inference,[],[32,3042,3090,3107,2925,3126,3003,3027,3100,2933,2942,3156,2989,2955,2967,368,37,33,34,36,43,38,47,48,46,49,51,50,54,13,14,17,12,160,7,16,15,20,5,21,9,11,4,8,22,23,10,19,6,18,2,70,71,30,44,31,24,3,29,75,114,93,64,52,103,104,92,113,60,82,83,53,61])). % 73.82/73.79 cnf(3242,plain, % 73.82/73.79 (~E(f9(f3(a15),f3(a15)),a1)), % 73.82/73.79 inference(scs_inference,[],[32,3042,3090,3107,2925,3126,3003,3027,3100,2933,2942,3156,2989,2955,2967,368,37,1741,33,34,36,43,38,47,48,46,49,51,50,54,13,14,17,12,160,7,16,15,20,5,21,9,11,4,8,22,23,10,19,6,18,2,70,71,30,44,31,24,3,29,75,114,93,64,52,103,104,92,113,60,82,83,53,61,63])). % 73.82/73.79 cnf(3244,plain, % 73.82/73.79 (~E(f2(a15,a15),a1)), % 73.82/73.79 inference(scs_inference,[],[32,3042,3090,3107,2925,3126,3003,3027,3100,2933,2942,3156,2989,2955,2967,368,37,1741,33,34,36,43,38,47,48,46,49,51,50,54,13,14,17,12,160,7,16,15,20,5,21,9,11,4,8,22,23,10,19,6,18,2,70,71,30,44,31,24,3,29,75,114,93,64,52,103,104,92,113,60,82,83,53,61,63,66])). % 73.82/73.79 cnf(3254,plain, % 73.82/73.79 (E(f9(a1,a1),f10(f9(f9(a1,a1),f9(a1,a1)),f9(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[32,3042,3090,3107,2925,3126,3003,3027,3097,3098,3100,3152,2933,2942,3156,2989,2955,595,2967,1412,368,566,37,147,2952,1299,1741,498,33,34,36,43,38,47,48,46,49,51,50,54,13,14,17,12,160,7,16,15,20,5,21,9,11,4,8,22,23,10,19,6,18,2,70,71,30,44,31,24,3,29,75,114,93,64,52,103,104,92,113,60,82,83,53,61,63,66,74,90,80,135])). % 73.82/73.79 cnf(3258,plain, % 73.82/73.79 (P3(a1,f9(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[32,3042,3090,3107,2925,3126,3003,3027,3144,3097,3098,3100,3152,2987,2933,2942,3156,2989,2955,595,2967,1412,368,566,37,147,2952,1299,651,1741,498,33,34,36,43,38,47,48,46,49,51,50,54,13,14,17,12,160,7,16,15,20,5,21,9,11,4,8,22,23,10,19,6,18,2,70,71,30,44,31,24,3,29,75,114,93,64,52,103,104,92,113,60,82,83,53,61,63,66,74,90,80,135,87,96])). % 73.82/73.79 cnf(3260,plain, % 73.82/73.79 (E(f5(f2(a1,a1),f2(a1,a1)),f10(f2(a1,a1),f2(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[32,3042,3090,3107,2925,3126,3003,3027,3144,3097,3098,3100,3152,2987,2933,2942,3156,2989,2955,595,2967,1412,368,566,37,147,2952,1299,651,1741,498,33,34,36,43,38,47,48,46,49,51,50,54,13,14,17,12,160,7,16,15,20,5,21,9,11,4,8,22,23,10,19,6,18,2,70,71,30,44,31,24,3,29,75,114,93,64,52,103,104,92,113,60,82,83,53,61,63,66,74,90,80,135,87,96,97])). % 73.82/73.79 cnf(3262,plain, % 73.82/73.79 (P3(f10(a1,a1),f9(f10(a1,a1),f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[32,3042,3090,3107,2925,3126,3003,3027,3144,3097,3098,3100,3152,2987,2933,2942,3156,2989,2955,595,2967,658,1412,368,566,37,147,2952,1299,651,1741,498,153,33,34,36,43,38,47,48,46,49,51,50,54,13,14,17,12,160,7,16,15,20,5,21,9,11,4,8,22,23,10,19,6,18,2,70,71,30,44,31,24,3,29,75,114,93,64,52,103,104,92,113,60,82,83,53,61,63,66,74,90,80,135,87,96,97,105])). % 73.82/73.79 cnf(3264,plain, % 73.82/73.79 (P3(f3(a15),f9(a15,f10(a15,a15)))), % 73.82/73.79 inference(scs_inference,[],[32,3042,3090,3107,2925,3126,3003,3027,3144,3097,3098,3100,3152,2987,2933,2942,3156,2989,2955,595,2967,658,1412,368,566,37,147,2952,1299,651,1741,498,153,33,34,36,43,38,47,48,46,49,51,50,54,13,14,17,12,160,7,16,15,20,5,21,9,11,4,8,22,23,10,19,6,18,2,70,71,30,44,31,24,3,29,75,114,93,64,52,103,104,92,113,60,82,83,53,61,63,66,74,90,80,135,87,96,97,105,1725])). % 73.82/73.79 cnf(3267,plain, % 73.82/73.79 (~E(f3(a15),a12)), % 73.82/73.79 inference(scs_inference,[],[32,3042,3090,3107,2925,3126,3003,3027,3144,3097,3098,3100,3152,2987,2933,2942,3156,2989,2955,595,2967,658,1412,368,566,37,147,2952,1299,651,1741,498,153,33,34,36,43,38,47,48,46,49,51,50,54,13,14,17,12,160,7,16,15,20,5,21,9,11,4,8,22,23,10,19,6,18,2,70,71,30,44,31,24,3,29,75,114,93,64,52,103,104,92,113,60,82,83,53,61,63,66,74,90,80,135,87,96,97,105,1725,2818,2820,45])). % 73.82/73.79 cnf(3271,plain, % 73.82/73.79 (E(f3(a15),a15)), % 73.82/73.79 inference(scs_inference,[],[32,3042,3090,3107,2925,3126,3003,3148,3027,3144,3097,3098,3100,3152,2987,2933,2942,3156,2989,2955,595,2967,658,1412,368,566,37,147,2952,1299,651,1741,498,153,33,34,36,43,38,47,48,46,49,51,50,54,13,14,17,12,160,7,16,15,20,5,21,9,11,4,8,22,23,10,19,6,18,2,70,71,30,44,31,24,3,29,75,114,93,64,52,103,104,92,113,60,82,83,53,61,63,66,74,90,80,135,87,96,97,105,1725,2818,2820,45,133,59])). % 73.82/73.79 cnf(3273,plain, % 73.82/73.79 (P5(f3(a15),a15)), % 73.82/73.79 inference(scs_inference,[],[32,3042,3090,3107,2925,3126,3003,3148,3027,3144,3097,3098,3100,3152,2987,2933,2942,3156,2989,2955,595,2967,658,1412,368,566,37,147,2952,1299,651,1741,498,153,33,34,36,43,38,47,48,46,49,51,50,54,13,14,17,12,160,7,16,15,20,5,21,9,11,4,8,22,23,10,19,6,18,2,70,71,30,44,31,24,3,29,75,114,93,64,52,103,104,92,113,60,82,83,53,61,63,66,74,90,80,135,87,96,97,105,1725,2818,2820,45,133,59,73])). % 73.82/73.79 cnf(3289,plain, % 73.82/73.79 (E(f9(f3(a15),a1),f3(a15))), % 73.82/73.79 inference(scs_inference,[],[3222,47,46,50])). % 73.82/73.79 cnf(3291,plain, % 73.82/73.79 (E(f9(a1,f3(a15)),f3(a15))), % 73.82/73.79 inference(scs_inference,[],[3222,47,46,50,48])). % 73.82/73.79 cnf(3293,plain, % 73.82/73.79 (E(f2(f3(a15),a12),f3(a15))), % 73.82/73.79 inference(scs_inference,[],[3222,47,46,50,48,51])). % 73.82/73.79 cnf(3295,plain, % 73.82/73.79 (P5(f3(a15),f3(a15))), % 73.82/73.79 inference(scs_inference,[],[3222,47,46,50,48,51,54])). % 73.82/73.79 cnf(3299,plain, % 73.82/73.79 (E(f2(a12,f3(a15)),f3(a15))), % 73.82/73.79 inference(scs_inference,[],[2921,3222,47,46,50,48,51,54,17,12,49])). % 73.82/73.79 cnf(3301,plain, % 73.82/73.79 (E(f9(f2(a12,a1),f10(a1,a1)),a1)), % 73.82/73.79 inference(scs_inference,[],[2921,3222,47,46,50,48,51,54,17,12,49,160])). % 73.82/73.79 cnf(3303,plain, % 73.82/73.79 (E(f9(x33031,f2(a12,a1)),f9(x33031,a1))), % 73.82/73.79 inference(scs_inference,[],[2921,3222,47,46,50,48,51,54,17,12,49,160,16,13])). % 73.82/73.79 cnf(3317,plain, % 73.82/73.79 (E(f10(f2(a12,a1),x33171),f10(a1,x33171))), % 73.82/73.79 inference(scs_inference,[],[2921,3222,47,46,50,48,51,54,17,12,49,160,16,13,14,7,20,15,9,22,4,21,5,10,11,23,8,18])). % 73.82/73.79 cnf(3319,plain, % 73.82/73.79 (E(f10(x33191,f2(a12,a1)),f10(x33191,a1))), % 73.82/73.79 inference(scs_inference,[],[2921,3222,47,46,50,48,51,54,17,12,49,160,16,13,14,7,20,15,9,22,4,21,5,10,11,23,8,18,6,19])). % 73.82/73.79 cnf(3321,plain, % 73.82/73.79 (P1(f9(f3(a15),f3(a15)))), % 73.82/73.79 inference(scs_inference,[],[2921,3220,3222,47,46,50,48,51,54,17,12,49,160,16,13,14,7,20,15,9,22,4,21,5,10,11,23,8,18,6,19,2,70])). % 73.82/73.79 cnf(3323,plain, % 73.82/73.79 (P1(f2(f3(a15),f3(a15)))), % 73.82/73.79 inference(scs_inference,[],[2921,3220,3222,47,46,50,48,51,54,17,12,49,160,16,13,14,7,20,15,9,22,4,21,5,10,11,23,8,18,6,19,2,70,71])). % 73.82/73.79 cnf(3325,plain, % 73.82/73.79 (~P3(f9(a1,a1),f3(a15))), % 73.82/73.79 inference(scs_inference,[],[2921,3220,3111,3222,3271,47,46,50,48,51,54,17,12,49,160,16,13,14,7,20,15,9,22,4,21,5,10,11,23,8,18,6,19,2,70,71,30])). % 73.82/73.79 cnf(3326,plain, % 73.82/73.79 (~P2(f2(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[2921,3220,3111,3222,3271,2927,2955,47,46,50,48,51,54,17,12,49,160,16,13,14,7,20,15,9,22,4,21,5,10,11,23,8,18,6,19,2,70,71,30,44])). % 73.82/73.79 cnf(3329,plain, % 73.82/73.79 (~P5(f3(a15),f9(a12,f10(a12,a12)))), % 73.82/73.79 inference(scs_inference,[],[2921,3220,3111,3222,3238,3271,265,2927,582,2955,47,46,50,48,51,54,17,12,49,160,16,13,14,7,20,15,9,22,4,21,5,10,11,23,8,18,6,19,2,70,71,30,44,31,27])). % 73.82/73.79 cnf(3330,plain, % 73.82/73.79 (~P5(f3(a15),a12)), % 73.82/73.79 inference(scs_inference,[],[2921,3220,3111,3222,3238,3271,265,2927,582,2955,302,47,46,50,48,51,54,17,12,49,160,16,13,14,7,20,15,9,22,4,21,5,10,11,23,8,18,6,19,2,70,71,30,44,31,27,28])). % 73.82/73.79 cnf(3332,plain, % 73.82/73.79 (~P3(f2(a12,a1),a15)), % 73.82/73.79 inference(scs_inference,[],[2921,3220,3111,3222,3238,3271,265,852,2927,582,145,2955,302,47,46,50,48,51,54,17,12,49,160,16,13,14,7,20,15,9,22,4,21,5,10,11,23,8,18,6,19,2,70,71,30,44,31,27,28,3,29])). % 73.82/73.79 cnf(3335,plain, % 73.82/73.79 (P1(f3(f3(a15)))), % 73.82/73.79 inference(scs_inference,[],[2921,3220,3111,3222,3238,3267,3271,265,852,2927,582,145,2955,302,1741,35,47,46,50,48,51,54,17,12,49,160,16,13,14,7,20,15,9,22,4,21,5,10,11,23,8,18,6,19,2,70,71,30,44,31,27,28,3,29,114,52])). % 73.82/73.79 cnf(3341,plain, % 73.82/73.79 (P5(f9(a12,f10(a12,a12)),f3(a15))), % 73.82/73.79 inference(scs_inference,[],[32,3206,2921,3220,3111,3222,3238,3267,3271,265,852,2927,582,145,2955,302,305,1741,35,36,47,46,50,48,51,54,17,12,49,160,16,13,14,7,20,15,9,22,4,21,5,10,11,23,8,18,6,19,2,70,71,30,44,31,27,28,3,29,114,52,75,93,69])). % 73.82/73.79 cnf(3343,plain, % 73.82/73.79 (E(f2(f3(a15),f6(f3(a15),a15)),a15)), % 73.82/73.79 inference(scs_inference,[],[32,3206,3232,2921,3220,3111,3222,3238,3267,3271,265,852,2927,582,145,2955,302,305,1741,35,36,47,46,50,48,51,54,17,12,49,160,16,13,14,7,20,15,9,22,4,21,5,10,11,23,8,18,6,19,2,70,71,30,44,31,27,28,3,29,114,52,75,93,69,92])). % 73.82/73.79 cnf(3353,plain, % 73.82/73.79 (P2(f3(f3(a15)))), % 73.82/73.79 inference(scs_inference,[],[32,3206,3232,2921,3220,3111,3222,3238,3267,3271,265,852,2927,582,145,2955,302,305,1741,35,36,47,46,50,48,51,54,17,12,49,160,16,13,14,7,20,15,9,22,4,21,5,10,11,23,8,18,6,19,2,70,71,30,44,31,27,28,3,29,114,52,75,93,69,92,103,104,113,82,53])). % 73.82/73.79 cnf(3355,plain, % 73.82/73.79 (P5(a15,f3(a15))), % 73.82/73.79 inference(scs_inference,[],[32,3206,3232,2921,3220,3111,3222,3238,3267,3271,265,852,2927,582,145,2955,302,305,1741,35,36,47,46,50,48,51,54,17,12,49,160,16,13,14,7,20,15,9,22,4,21,5,10,11,23,8,18,6,19,2,70,71,30,44,31,27,28,3,29,114,52,75,93,69,92,103,104,113,82,53,61])). % 73.82/73.79 cnf(3364,plain, % 73.82/73.79 (~E(f2(a15,a15),f2(a15,a1))), % 73.82/73.79 inference(scs_inference,[],[32,3206,3232,2921,3220,3111,3222,3238,3267,3271,3199,265,852,2927,582,145,185,2955,302,305,1741,153,35,36,47,46,50,48,51,54,17,12,49,160,16,13,14,7,20,15,9,22,4,21,5,10,11,23,8,18,6,19,2,70,71,30,44,31,27,28,3,29,114,52,75,93,69,92,103,104,113,82,53,61,83,90,128,87])). % 73.82/73.79 cnf(3366,plain, % 73.82/73.79 (E(a1,f10(f6(a1,a1),f6(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[32,3206,3232,2921,3177,3220,3111,3222,3238,3267,3271,3199,3175,265,852,2927,582,145,185,3126,2955,302,305,1741,153,35,36,47,46,50,48,51,54,17,12,49,160,16,13,14,7,20,15,9,22,4,21,5,10,11,23,8,18,6,19,2,70,71,30,44,31,27,28,3,29,114,52,75,93,69,92,103,104,113,82,53,61,83,90,128,87,97])). % 73.82/73.79 cnf(3372,plain, % 73.82/73.79 (P5(a12,f3(a15))), % 73.82/73.79 inference(scs_inference,[],[32,3206,3232,2921,3177,3258,3220,3111,3222,3238,3267,3271,3199,3175,3104,265,852,2927,582,655,145,185,3126,2955,302,2952,305,1741,153,35,36,47,46,50,48,51,54,17,12,49,160,16,13,14,7,20,15,9,22,4,21,5,10,11,23,8,18,6,19,2,70,71,30,44,31,27,28,3,29,114,52,75,93,69,92,103,104,113,82,53,61,83,90,128,87,97,105,45,56])). % 73.82/73.79 cnf(3376,plain, % 73.82/73.79 (E(a15,f3(a15))), % 73.82/73.79 inference(scs_inference,[],[32,3206,3232,2921,3177,3258,3220,3111,3222,3238,3267,3271,3273,3199,3175,3104,265,852,2927,582,655,145,185,3126,2955,302,2952,305,1741,153,35,36,47,46,50,48,51,54,17,12,49,160,16,13,14,7,20,15,9,22,4,21,5,10,11,23,8,18,6,19,2,70,71,30,44,31,27,28,3,29,114,52,75,93,69,92,103,104,113,82,53,61,83,90,128,87,97,105,45,56,66,78])). % 73.82/73.79 cnf(3380,plain, % 73.82/73.79 (P3(f3(a15),f10(a15,a15))), % 73.82/73.79 inference(scs_inference,[],[32,3206,3232,2921,3177,3258,3220,3111,3222,3238,3267,3271,3273,3199,3175,3104,3150,265,3264,852,2927,582,655,145,185,3126,2955,302,2952,362,305,1741,153,35,36,47,46,50,48,51,54,17,12,49,160,16,13,14,7,20,15,9,22,4,21,5,10,11,23,8,18,6,19,2,70,71,30,44,31,27,28,3,29,114,52,75,93,69,92,103,104,113,82,53,61,83,90,128,87,97,105,45,56,66,78,96,111])). % 73.82/73.79 cnf(3392,plain, % 73.82/73.79 (P5(f5(f2(a1,a1),f2(a1,a1)),f5(f2(a1,a1),f2(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[3234,2955,46,48,47,50,54])). % 73.82/73.79 cnf(3399,plain, % 73.82/73.79 (E(f9(a15,x33991),f9(f3(a15),x33991))), % 73.82/73.79 inference(scs_inference,[],[3376,3234,2955,46,48,47,50,54,49,17,51,12])). % 73.82/73.79 cnf(3401,plain, % 73.82/73.79 (E(f11(a15,x34011),f11(f3(a15),x34011))), % 73.82/73.79 inference(scs_inference,[],[3376,3234,2955,46,48,47,50,54,49,17,51,12,20,14])). % 73.82/73.79 cnf(3403,plain, % 73.82/73.79 (E(f2(a15,x34031),f2(f3(a15),x34031))), % 73.82/73.79 inference(scs_inference,[],[3376,3234,2955,46,48,47,50,54,49,17,51,12,20,14,7,4])). % 73.82/73.79 cnf(3404,plain, % 73.82/73.79 (E(f9(x34041,a15),f9(x34041,f3(a15)))), % 73.82/73.79 inference(scs_inference,[],[3376,3234,2955,46,48,47,50,54,49,17,51,12,20,14,7,4,13])). % 73.82/73.79 cnf(3407,plain, % 73.82/73.79 (E(f11(x34071,a15),f11(x34071,f3(a15)))), % 73.82/73.79 inference(scs_inference,[],[3376,3234,2955,46,48,47,50,54,49,17,51,12,20,14,7,4,13,16,9,15])). % 73.82/73.79 cnf(3411,plain, % 73.82/73.79 (E(f3(a15),f3(f3(a15)))), % 73.82/73.79 inference(scs_inference,[],[3376,3234,2955,46,48,47,50,54,49,17,51,12,20,14,7,4,13,16,9,15,22,5,21,23])). % 73.82/73.79 cnf(3412,plain, % 73.82/73.79 (E(f10(a15,x34121),f10(f3(a15),x34121))), % 73.82/73.79 inference(scs_inference,[],[3376,3234,2955,46,48,47,50,54,49,17,51,12,20,14,7,4,13,16,9,15,22,5,21,23,18])). % 73.82/73.79 cnf(3417,plain, % 73.82/73.79 (E(f10(x34171,a15),f10(x34171,f3(a15)))), % 73.82/73.79 inference(scs_inference,[],[3376,3234,2955,46,48,47,50,54,49,17,51,12,20,14,7,4,13,16,9,15,22,5,21,23,18,10,6,11,8,19])). % 73.82/73.79 cnf(3418,plain, % 73.82/73.79 (~E(f2(a15,a1),f2(a15,a15))), % 73.82/73.79 inference(scs_inference,[],[3364,3376,3234,2955,46,48,47,50,54,49,17,51,12,20,14,7,4,13,16,9,15,22,5,21,23,18,10,6,11,8,19,2])). % 73.82/73.79 cnf(3419,plain, % 73.82/73.79 (P1(f9(f2(a1,a1),f2(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[3364,3376,3234,2955,46,48,47,50,54,49,17,51,12,20,14,7,4,13,16,9,15,22,5,21,23,18,10,6,11,8,19,2,70])). % 73.82/73.79 cnf(3421,plain, % 73.82/73.79 (P1(f2(f2(a1,a1),f2(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[3364,3376,3234,2955,46,48,47,50,54,49,17,51,12,20,14,7,4,13,16,9,15,22,5,21,23,18,10,6,11,8,19,2,70,71])). % 73.82/73.79 cnf(3423,plain, % 73.82/73.79 (~E(f3(f3(a15)),a12)), % 73.82/73.79 inference(scs_inference,[],[3364,3376,3234,3335,3353,2955,46,48,47,50,54,49,17,51,12,20,14,7,4,13,16,9,15,22,5,21,23,18,10,6,11,8,19,2,70,71,45])). % 73.82/73.79 cnf(3426,plain, % 73.82/73.79 (~E(f3(f3(a15)),a1)), % 73.82/73.79 inference(scs_inference,[],[3364,3332,3376,3234,3335,3353,3343,2955,46,48,47,50,54,49,17,51,12,20,14,7,4,13,16,9,15,22,5,21,23,18,10,6,11,8,19,2,70,71,45,30,44])). % 73.82/73.79 cnf(3428,plain, % 73.82/73.79 (~E(f3(f3(a15)),f2(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[3326,3364,3332,3376,3234,3335,3353,3343,2955,46,48,47,50,54,49,17,51,12,20,14,7,4,13,16,9,15,22,5,21,23,18,10,6,11,8,19,2,70,71,45,30,44,31])). % 73.82/73.79 cnf(3429,plain, % 73.82/73.79 (~P5(f9(f3(a15),a1),a12)), % 73.82/73.79 inference(scs_inference,[],[3326,3364,3332,3330,3376,3289,3234,3335,3353,3343,2955,46,48,47,50,54,49,17,51,12,20,14,7,4,13,16,9,15,22,5,21,23,18,10,6,11,8,19,2,70,71,45,30,44,31,27])). % 73.82/73.79 cnf(3430,plain, % 73.82/73.79 (P5(f9(a15,f10(a15,a15)),f3(a15))), % 73.82/73.79 inference(scs_inference,[],[3326,3364,3332,3330,3376,3289,3234,3335,3353,3343,519,2955,46,48,47,50,54,49,17,51,12,20,14,7,4,13,16,9,15,22,5,21,23,18,10,6,11,8,19,2,70,71,45,30,44,31,27,28])). % 73.82/73.79 cnf(3431,plain, % 73.82/73.79 (~E(f2(f3(a15),a15),f2(a15,a1))), % 73.82/73.79 inference(scs_inference,[],[3326,3364,3332,3330,3376,3289,3234,3335,3353,3343,519,2955,46,48,47,50,54,49,17,51,12,20,14,7,4,13,16,9,15,22,5,21,23,18,10,6,11,8,19,2,70,71,45,30,44,31,27,28,3])). % 73.82/73.79 cnf(3432,plain, % 73.82/73.79 (~P3(f9(f9(a1,a1),a1),f3(a15))), % 73.82/73.79 inference(scs_inference,[],[3326,3364,3325,3332,3330,3376,3072,3289,3234,3335,3353,3343,519,2955,46,48,47,50,54,49,17,51,12,20,14,7,4,13,16,9,15,22,5,21,23,18,10,6,11,8,19,2,70,71,45,30,44,31,27,28,3,29])). % 73.82/73.79 cnf(3436,plain, % 73.82/73.79 (P1(f3(f3(f3(a15))))), % 73.82/73.79 inference(scs_inference,[],[32,3326,3364,3325,3332,3330,3376,3072,3289,3234,3242,3321,3335,3353,3343,519,2955,46,48,47,50,54,49,17,51,12,20,14,7,4,13,16,9,15,22,5,21,23,18,10,6,11,8,19,2,70,71,45,30,44,31,27,28,3,29,64,52])). % 73.82/73.79 cnf(3450,plain, % 73.82/73.79 (P1(f6(f10(a1,a1),f10(a1,a1)))), % 73.82/73.79 inference(scs_inference,[],[32,3326,3364,3325,3332,3330,3376,3072,3289,3234,3242,3321,3335,3353,3343,519,3177,658,2955,3126,3222,1741,153,36,46,48,47,50,54,49,17,51,12,20,14,7,4,13,16,9,15,22,5,21,23,18,10,6,11,8,19,2,70,71,45,30,44,31,27,28,3,29,64,52,103,114,75,104,93,113,83])). % 73.82/73.79 cnf(3452,plain, % 73.82/73.79 (P2(f3(f3(f3(a15))))), % 73.82/73.79 inference(scs_inference,[],[32,3326,3364,3325,3332,3330,3376,3072,3289,3234,3242,3321,3335,3353,3343,519,3177,658,2955,3126,3222,1741,153,36,46,48,47,50,54,49,17,51,12,20,14,7,4,13,16,9,15,22,5,21,23,18,10,6,11,8,19,2,70,71,45,30,44,31,27,28,3,29,64,52,103,114,75,104,93,113,83,53])). % 73.82/73.79 cnf(3459,plain, % 73.82/73.79 (~E(f2(f3(a15),f3(a15)),a1)), % 73.82/73.79 inference(scs_inference,[],[32,3326,3364,3325,3332,3330,3376,3072,3079,3289,3234,3242,3124,3321,3335,3353,3343,519,3177,658,2955,3126,3222,421,1741,153,36,46,48,47,50,54,49,17,51,12,20,14,7,4,13,16,9,15,22,5,21,23,18,10,6,11,8,19,2,70,71,45,30,44,31,27,28,3,29,64,52,103,114,75,104,93,113,83,53,61,82,66])). % 73.82/73.79 cnf(3461,plain, % 73.82/73.79 (E(f9(a1,f9(a1,a1)),f10(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[32,3326,3364,3325,3332,3330,3376,3072,3079,3289,3134,3234,3242,3124,3321,3335,3353,3343,519,3177,658,194,2955,3126,3222,421,1741,153,36,46,48,47,50,54,49,17,51,12,20,14,7,4,13,16,9,15,22,5,21,23,18,10,6,11,8,19,2,70,71,45,30,44,31,27,28,3,29,64,52,103,114,75,104,93,113,83,53,61,82,66,90])). % 73.82/73.79 cnf(3467,plain, % 73.82/73.79 (~P3(f2(f10(a1,a1),a1),f3(a15))), % 73.82/73.79 inference(scs_inference,[],[32,3326,3364,3325,3380,3332,3330,3376,3072,3079,3289,1742,2954,3134,3234,3242,3124,3321,3335,3353,3343,519,3177,3232,658,194,2955,3126,3222,421,362,854,1741,170,153,36,46,48,47,50,54,49,17,51,12,20,14,7,4,13,16,9,15,22,5,21,23,18,10,6,11,8,19,2,70,71,45,30,44,31,27,28,3,29,64,52,103,114,75,104,93,113,83,53,61,82,66,90,128,88,96])). % 73.82/73.79 cnf(3471,plain, % 73.82/73.79 (~E(f9(f10(a1,a1),f3(a15)),f10(a1,a1))), % 73.82/73.79 inference(scs_inference,[],[32,3326,3364,3325,3380,3332,3330,3376,3072,3079,3289,1742,1743,2954,3134,3234,3242,3124,3321,3335,3353,3343,2833,519,3177,145,3232,658,194,172,2955,3126,3222,421,362,854,174,1741,170,153,36,46,48,47,50,54,49,17,51,12,20,14,7,4,13,16,9,15,22,5,21,23,18,10,6,11,8,19,2,70,71,45,30,44,31,27,28,3,29,64,52,103,114,75,104,93,113,83,53,61,82,66,90,128,88,96,111,97])). % 73.82/73.79 cnf(3473,plain, % 73.82/73.79 (P3(f3(a15),f9(f10(a15,a15),f10(a15,a15)))), % 73.82/73.80 inference(scs_inference,[],[32,3326,3364,3325,3380,3332,3330,3376,3072,3079,3289,1742,1743,2954,3134,3234,3242,3124,3321,3335,3353,3343,2833,519,3177,145,3232,658,194,172,2955,3126,3222,421,362,854,174,1741,170,153,36,46,48,47,50,54,49,17,51,12,20,14,7,4,13,16,9,15,22,5,21,23,18,10,6,11,8,19,2,70,71,45,30,44,31,27,28,3,29,64,52,103,114,75,104,93,113,83,53,61,82,66,90,128,88,96,111,97,105])). % 73.82/73.80 cnf(3481,plain, % 73.82/73.80 (E(f9(f10(a13,a13),a1),f10(a13,a13))), % 73.82/73.80 inference(scs_inference,[],[295,50])). % 73.82/73.80 cnf(3516,plain, % 73.82/73.80 (P1(f9(f10(a13,a13),f10(a13,a13)))), % 73.82/73.80 inference(scs_inference,[],[3244,3419,2971,295,50,47,48,46,49,54,51,17,20,12,16,5,4,13,7,15,14,23,22,21,9,6,18,8,10,19,11,2,70])). % 73.82/73.80 cnf(3518,plain, % 73.82/73.80 (P1(f2(f10(a13,a13),f10(a13,a13)))), % 73.82/73.80 inference(scs_inference,[],[3244,3419,2971,295,50,47,48,46,49,54,51,17,20,12,16,5,4,13,7,15,14,23,22,21,9,6,18,8,10,19,11,2,70,71])). % 73.82/73.80 cnf(3520,plain, % 73.82/73.80 (~E(f3(f3(f3(a15))),a12)), % 73.82/73.80 inference(scs_inference,[],[3244,3419,2971,3436,3452,295,50,47,48,46,49,54,51,17,20,12,16,5,4,13,7,15,14,23,22,21,9,6,18,8,10,19,11,2,70,71,45])). % 73.82/73.80 cnf(3522,plain, % 73.82/73.80 (P3(f9(a1,a1),f2(f9(a1,a1),a1))), % 73.82/73.80 inference(scs_inference,[],[3244,3071,3419,2971,3436,3452,3150,295,50,47,48,46,49,54,51,17,20,12,16,5,4,13,7,15,14,23,22,21,9,6,18,8,10,19,11,2,70,71,45,30])). % 73.82/73.80 cnf(3524,plain, % 73.82/73.80 (~E(f3(f3(f3(a15))),a1)), % 73.82/73.80 inference(scs_inference,[],[3244,3071,3419,2971,3436,3452,3150,295,50,47,48,46,49,54,51,17,20,12,16,5,4,13,7,15,14,23,22,21,9,6,18,8,10,19,11,2,70,71,45,30,44])). % 73.82/73.80 cnf(3528,plain, % 73.82/73.80 (~P5(f9(f3(a15),f9(a1,a1)),a12)), % 73.82/73.80 inference(scs_inference,[],[32,3244,3071,3076,3419,2971,3366,3429,3436,3452,3107,3150,295,50,47,48,46,49,54,51,17,20,12,16,5,4,13,7,15,14,23,22,21,9,6,18,8,10,19,11,2,70,71,45,30,44,24,31,27])). % 73.82/73.80 cnf(3530,plain, % 73.82/73.80 (~P5(f9(f3(a15),a1),f9(a12,f10(a12,a12)))), % 73.82/73.80 inference(scs_inference,[],[32,3244,3071,3076,3419,2971,3366,3429,3436,3452,3107,3150,246,295,50,47,48,46,49,54,51,17,20,12,16,5,4,13,7,15,14,23,22,21,9,6,18,8,10,19,11,2,70,71,45,30,44,24,31,27,28])). % 73.82/73.80 cnf(3545,plain, % 73.82/73.80 (E(f9(a12,f10(a15,a12)),f3(a15))), % 73.82/73.80 inference(scs_inference,[],[32,3372,3244,3461,3070,3086,3071,3076,3419,2971,3412,3366,3429,3436,3452,3329,3107,3258,3150,3104,246,692,295,2952,3222,305,33,50,47,48,46,49,54,51,17,20,12,16,5,4,13,7,15,14,23,22,21,9,6,18,8,10,19,11,2,70,71,45,30,44,24,31,27,28,3,29,92,93,83,61,82,90])). % 73.82/73.80 cnf(3552,plain, % 73.82/73.80 (P3(f9(a1,f10(a1,a1)),f9(a1,a1))), % 73.82/73.80 inference(scs_inference,[],[32,3372,3244,3200,3461,3070,3086,3071,3076,3467,3419,2971,3412,3366,3429,3436,3452,3329,706,1972,3107,3258,3150,3104,3206,246,692,2955,295,2952,3222,854,305,170,33,36,50,47,48,46,49,54,51,17,20,12,16,5,4,13,7,15,14,23,22,21,9,6,18,8,10,19,11,2,70,71,45,30,44,24,31,27,28,3,29,92,93,83,61,82,90,87,111,105])). % 73.82/73.80 cnf(3562,plain, % 73.82/73.80 (P3(f10(a13,a13),f2(f10(a13,a13),f10(a13,a13)))), % 73.82/73.80 inference(scs_inference,[],[3518,340])). % 73.82/73.80 cnf(3563,plain, % 73.82/73.80 (P5(f10(a13,a13),f9(f10(a13,a13),f10(a13,a13)))), % 73.82/73.80 inference(scs_inference,[],[3516,360])). % 73.82/73.80 cnf(3564,plain, % 73.82/73.80 (E(f9(a1,f10(a12,a12)),f10(a12,a12))), % 73.82/73.80 inference(scs_inference,[],[240,48])). % 73.82/73.80 cnf(3579,plain, % 73.82/73.80 (E(f9(f9(f9(a1,a1),f10(a1,a1)),x35791),f9(a1,x35791))), % 73.82/73.80 inference(scs_inference,[],[3421,3080,240,48,46,54,47,50,51,49,17,12])). % 73.82/73.80 cnf(3598,plain, % 73.82/73.80 (~E(f9(a15,a1),f9(a12,a1))), % 73.82/73.80 inference(scs_inference,[],[3001,3421,3080,240,48,46,54,47,50,51,49,17,12,20,7,22,4,13,5,9,16,14,23,21,15,8,6,19,11,18,10,2])). % 73.82/73.80 cnf(3604,plain, % 73.82/73.80 (~E(f3(f3(a15)),f10(a1,f10(a1,a1)))), % 73.82/73.80 inference(scs_inference,[],[3001,3213,3421,3080,244,3353,240,38,48,46,54,47,50,51,49,17,12,20,7,22,4,13,5,9,16,14,23,21,15,8,6,19,11,18,10,2,70,71,30,31])). % 73.82/73.80 cnf(3606,plain, % 73.82/73.80 (E(f9(x36061,f2(a12,a1)),f9(x36061,a1))), % 73.82/73.80 inference(rename_variables,[],[3303])). % 73.82/73.80 cnf(3607,plain, % 73.82/73.80 (P5(f9(a1,a1),f10(f9(a1,a1),a1))), % 73.82/73.80 inference(scs_inference,[],[3001,3213,3303,3421,3110,3080,244,3530,3029,3353,240,38,48,46,54,47,50,51,49,17,12,20,7,22,4,13,5,9,16,14,23,21,15,8,6,19,11,18,10,2,70,71,30,31,27,28])). % 73.82/73.80 cnf(3608,plain, % 73.82/73.80 (~E(f2(f3(a15),a1),f2(a15,a15))), % 73.82/73.80 inference(scs_inference,[],[3418,3001,3213,3303,3421,3110,3080,244,3403,3530,3029,3353,240,38,48,46,54,47,50,51,49,17,12,20,7,22,4,13,5,9,16,14,23,21,15,8,6,19,11,18,10,2,70,71,30,31,27,28,3])). % 73.82/73.80 cnf(3610,plain, % 73.82/73.80 (~P3(f9(f9(a1,a1),f2(a12,a1)),f3(a15))), % 73.82/73.80 inference(scs_inference,[],[3418,3001,3213,3303,3606,3432,3421,3110,3080,244,3403,3530,3029,3353,240,38,48,46,54,47,50,51,49,17,12,20,7,22,4,13,5,9,16,14,23,21,15,8,6,19,11,18,10,2,70,71,30,31,27,28,3,29])). % 73.82/73.80 cnf(3616,plain, % 73.82/73.80 (P1(f5(f10(a12,a12),f10(a12,a12)))), % 73.82/73.80 inference(scs_inference,[],[32,3418,3001,3213,3303,3606,3432,3421,3110,3080,244,3403,3530,3029,674,3353,269,240,153,38,48,46,54,47,50,51,49,17,12,20,7,22,4,13,5,9,16,14,23,21,15,8,6,19,11,18,10,2,70,71,30,31,27,28,3,29,92,93,82])). % 73.82/73.80 cnf(3635,plain, % 73.82/73.80 (P5(f6(a1,a1),f9(f6(a1,a1),f6(a1,a1)))), % 73.82/73.80 inference(scs_inference,[],[32,3418,3001,3213,3552,3303,3606,3317,3432,3421,3110,3080,244,3201,3203,3403,3407,3530,3136,3029,3007,674,706,3353,3380,269,3126,147,240,2952,362,3222,1741,170,153,38,48,46,54,47,50,51,49,17,12,20,7,22,4,13,5,9,16,14,23,21,15,8,6,19,11,18,10,2,70,71,30,31,27,28,3,29,92,93,82,83,61,90,91,105,160,44,125,126])). % 73.82/73.80 cnf(3676,plain, % 73.82/73.80 (P1(f9(f10(a14,a14),f10(a14,a14)))), % 73.82/73.80 inference(scs_inference,[],[3471,3450,3183,261,54,48,47,50,51,46,49,17,12,20,4,5,13,22,23,7,21,15,16,9,14,8,11,6,19,18,10,2,70])). % 73.82/73.80 cnf(3678,plain, % 73.82/73.80 (P1(f2(f10(a14,a14),f10(a14,a14)))), % 73.82/73.80 inference(scs_inference,[],[3471,3450,3183,261,54,48,47,50,51,46,49,17,12,20,4,5,13,22,23,7,21,15,16,9,14,8,11,6,19,18,10,2,70,71])). % 73.82/73.80 cnf(3680,plain, % 73.82/73.80 (P3(f9(a1,a1),f2(a1,a1))), % 73.82/73.80 inference(scs_inference,[],[3471,3085,3450,3522,3183,261,54,48,47,50,51,46,49,17,12,20,4,5,13,22,23,7,21,15,16,9,14,8,11,6,19,18,10,2,70,71,30])). % 73.82/73.80 cnf(3682,plain, % 73.82/73.80 (~E(f3(a15),f2(a1,a1))), % 73.82/73.80 inference(scs_inference,[],[3471,3085,3450,3522,3183,3326,3238,261,54,48,47,50,51,46,49,17,12,20,4,5,13,22,23,7,21,15,16,9,14,8,11,6,19,18,10,2,70,71,30,31])). % 73.82/73.80 cnf(3685,plain, % 73.82/73.80 (~P5(f9(f3(a15),f9(a1,a1)),f9(a12,f10(a12,a12)))), % 73.82/73.80 inference(scs_inference,[],[3471,3085,3450,3522,3183,3399,3528,3326,3238,246,261,54,48,47,50,51,46,49,17,12,20,4,5,13,22,23,7,21,15,16,9,14,8,11,6,19,18,10,2,70,71,30,31,27,28])). % 73.82/73.80 cnf(3689,plain, % 73.82/73.80 (~P3(f2(a12,f9(a1,a1)),f3(a15))), % 73.82/73.80 inference(scs_inference,[],[3471,3075,3095,3083,3085,3450,3522,3183,3399,3528,3326,3325,3238,246,261,54,48,47,50,51,46,49,17,12,20,4,5,13,22,23,7,21,15,16,9,14,8,11,6,19,18,10,2,70,71,30,31,27,28,3,29])). % 73.82/73.80 cnf(3692,plain, % 73.82/73.80 (P5(f3(f3(a15)),f3(a15))), % 73.82/73.80 inference(scs_inference,[],[3471,3075,3095,3083,3085,3450,3522,3183,3399,3411,3528,3326,3325,3238,3335,448,246,423,261,3222,34,54,48,47,50,51,46,49,17,12,20,4,5,13,22,23,7,21,15,16,9,14,8,11,6,19,18,10,2,70,71,30,31,27,28,3,29,82,61])). % 73.82/73.80 cnf(3707,plain, % 73.82/73.80 (P3(f3(f3(a15)),f3(a15))), % 73.82/73.80 inference(scs_inference,[],[32,3295,3471,3075,3095,3083,3085,3450,3516,3563,3522,3183,3323,3399,3417,3459,3411,3528,3604,3326,3325,3238,3267,3335,448,185,246,423,261,295,3222,1741,153,34,54,48,47,50,51,46,49,17,12,20,4,5,13,22,23,7,21,15,16,9,14,8,11,6,19,18,10,2,70,71,30,31,27,28,3,29,82,61,127,66,90,97,342,160,52,60])). % 73.82/73.80 cnf(3709,plain, % 73.82/73.80 (P3(f3(a15),f2(f3(a15),f3(a15)))), % 73.82/73.80 inference(scs_inference,[],[32,3295,3471,3075,3095,3083,3085,3450,3516,3563,3522,3183,3323,3399,3417,3459,3411,3528,3604,3326,3325,3238,3267,3335,448,185,246,423,261,295,3222,1741,153,34,54,48,47,50,51,46,49,17,12,20,4,5,13,22,23,7,21,15,16,9,14,8,11,6,19,18,10,2,70,71,30,31,27,28,3,29,82,61,127,66,90,97,342,160,52,60,125])). % 73.82/73.80 cnf(3721,plain, % 73.82/73.80 (E(f3(a15),f11(f2(f3(a15),f3(a15)),f3(a15)))), % 73.82/73.80 inference(scs_inference,[],[32,3295,3355,3471,3075,3095,3083,3085,3450,3516,3563,3522,3635,3183,3323,3399,3417,3459,3411,3528,3604,3326,3325,3238,3201,3321,3267,3335,448,185,246,423,3126,261,295,3222,1741,153,34,36,54,48,47,50,51,46,49,17,12,20,4,5,13,22,23,7,21,15,16,9,14,8,11,6,19,18,10,2,70,71,30,31,27,28,3,29,82,61,127,66,90,97,342,160,52,60,125,93,133,63,126,135,136])). % 73.82/73.80 cnf(3731,plain, % 73.82/73.80 (E(f9(a1,f5(a1,a1)),f5(a1,a1))), % 73.82/73.80 inference(scs_inference,[],[3616,421,54,47,48])). % 73.82/73.80 cnf(3761,plain, % 73.82/73.80 (~E(f2(a1,a1),f3(a15))), % 73.82/73.80 inference(scs_inference,[],[3682,3616,3301,421,54,47,48,50,49,46,51,17,20,7,23,12,5,15,4,9,13,16,21,14,8,22,6,11,19,18,10,2])). % 73.82/73.80 cnf(3762,plain, % 73.82/73.80 (P1(f9(f5(a1,a1),f5(a1,a1)))), % 73.82/73.80 inference(scs_inference,[],[3682,3616,3301,421,54,47,48,50,49,46,51,17,20,7,23,12,5,15,4,9,13,16,21,14,8,22,6,11,19,18,10,2,70])). % 73.82/73.80 cnf(3764,plain, % 73.82/73.80 (P1(f2(f5(a1,a1),f5(a1,a1)))), % 73.82/73.80 inference(scs_inference,[],[3682,3616,3301,421,54,47,48,50,49,46,51,17,20,7,23,12,5,15,4,9,13,16,21,14,8,22,6,11,19,18,10,2,70,71])). % 73.82/73.80 cnf(3767,plain, % 73.82/73.80 (~P5(f9(f3(a15),f2(a1,a12)),f9(a12,f10(a12,a12)))), % 73.82/73.80 inference(scs_inference,[],[3682,3179,3610,3545,3616,3301,3530,421,54,47,48,50,49,46,51,17,20,7,23,12,5,15,4,9,13,16,21,14,8,22,6,11,19,18,10,2,70,71,30,27])). % 73.82/73.80 cnf(3770,plain, % 73.82/73.80 (P5(f9(a1,a12),f9(a1,f3(a15)))), % 73.82/73.80 inference(scs_inference,[],[3140,3682,3179,3610,3545,3616,3301,171,3404,3530,3353,421,54,47,48,50,49,46,51,17,20,7,23,12,5,15,4,9,13,16,21,14,8,22,6,11,19,18,10,2,70,71,30,27,31,28])). % 73.82/73.80 cnf(3779,plain, % 73.82/73.80 (~E(a12,f3(a15))), % 73.82/73.80 inference(scs_inference,[],[3140,3598,3682,3341,3179,3610,3545,3707,3616,3301,171,3404,2936,3530,3330,3353,427,421,3222,305,33,54,47,48,50,49,46,51,17,20,7,23,12,5,15,4,9,13,16,21,14,8,22,6,11,19,18,10,2,70,71,30,27,31,28,3,29,93,82,61])). % 73.82/73.80 cnf(3787,plain, % 73.82/73.80 (~P5(f3(f3(f3(a15))),a12)), % 73.82/73.80 inference(scs_inference,[],[3140,3598,3682,3341,3179,3610,3545,3707,3616,3301,171,3404,3520,3524,2936,3240,3130,3530,3330,3436,3353,2967,427,421,3222,305,33,54,47,48,50,49,46,51,17,20,7,23,12,5,15,4,9,13,16,21,14,8,22,6,11,19,18,10,2,70,71,30,27,31,28,3,29,93,82,61,56,127,74,78])). % 73.82/73.80 cnf(3794,plain, % 73.82/73.80 (~E(f9(a1,f3(a15)),f10(a1,a1))), % 73.82/73.80 inference(scs_inference,[],[32,3140,3598,3682,3341,3481,3179,3610,3545,3707,1750,3616,3301,171,3404,3520,3524,2936,3240,3130,3412,3530,3330,3436,3353,2967,427,194,421,282,3222,305,153,33,34,54,47,48,50,49,46,51,17,20,7,23,12,5,15,4,9,13,16,21,14,8,22,6,11,19,18,10,2,70,71,30,27,31,28,3,29,93,82,61,56,127,74,78,80,90,97])). % 73.82/73.80 cnf(3796,plain, % 73.82/73.80 (E(f3(f3(a15)),f3(a15))), % 73.82/73.80 inference(scs_inference,[],[32,3140,3598,3682,3341,3481,3179,3610,3545,3707,1750,3616,3301,3423,171,3404,3520,3524,2936,3240,3130,3412,3530,3330,3436,3238,3353,2967,3335,427,194,421,282,3222,305,153,33,34,54,47,48,50,49,46,51,17,20,7,23,12,5,15,4,9,13,16,21,14,8,22,6,11,19,18,10,2,70,71,30,27,31,28,3,29,93,82,61,56,127,74,78,80,90,97,72])). % 73.82/73.80 cnf(3798,plain, % 73.82/73.80 (E(f5(a1,a1),f10(f9(f5(a1,a1),f5(a1,a1)),f5(a1,a1)))), % 73.82/73.80 inference(scs_inference,[],[32,3140,3598,3682,3341,3481,3179,3610,3545,3707,1750,3616,3301,3423,171,3404,3520,3524,2936,3240,3130,3412,3530,3330,3436,3238,3353,2967,3335,427,194,421,282,3222,305,153,33,34,54,47,48,50,49,46,51,17,20,7,23,12,5,15,4,9,13,16,21,14,8,22,6,11,19,18,10,2,70,71,30,27,31,28,3,29,93,82,61,56,127,74,78,80,90,97,72,495])). % 73.82/73.80 cnf(3808,plain, % 73.82/73.80 (P5(f5(a1,a1),f9(f5(a1,a1),f5(a1,a1)))), % 73.82/73.80 inference(scs_inference,[],[3762,493])). % 73.82/73.80 cnf(3844,plain, % 73.82/73.80 (P1(f9(f10(a15,a15),f10(a15,a15)))), % 73.82/73.80 inference(scs_inference,[],[3794,3676,2973,362,54,48,47,50,49,46,51,20,17,12,5,23,7,16,14,15,21,8,6,4,9,13,22,11,19,18,10,2,70])). % 73.82/73.80 cnf(3846,plain, % 73.82/73.80 (P1(f2(f10(a15,a15),f10(a15,a15)))), % 73.82/73.80 inference(scs_inference,[],[3794,3676,2973,362,54,48,47,50,49,46,51,20,17,12,5,23,7,16,14,15,21,8,6,4,9,13,22,11,19,18,10,2,70,71])). % 73.82/73.80 cnf(3849,plain, % 73.82/73.80 (~E(f3(a15),f9(a1,a1))), % 73.82/73.80 inference(scs_inference,[],[3794,3689,3796,3676,2973,3107,3238,362,54,48,47,50,49,46,51,20,17,12,5,23,7,16,14,15,21,8,6,4,9,13,22,11,19,18,10,2,70,71,30,31])). % 73.82/73.80 cnf(3852,plain, % 73.82/73.80 (~P5(f9(f3(a15),f2(a1,a12)),a12)), % 73.82/73.80 inference(scs_inference,[],[3794,3689,3796,3676,2973,3685,3767,3399,3107,3238,302,362,54,48,47,50,49,46,51,20,17,12,5,23,7,16,14,15,21,8,6,4,9,13,22,11,19,18,10,2,70,71,30,31,27,28])). % 73.82/73.80 cnf(3853,plain, % 73.82/73.80 (E(f9(a1,f5(a1,a1)),f10(f9(f5(a1,a1),f5(a1,a1)),f5(a1,a1)))), % 73.82/73.80 inference(scs_inference,[],[3731,3794,3689,3796,3676,2973,3685,3767,3798,3399,3107,3238,302,362,54,48,47,50,49,46,51,20,17,12,5,23,7,16,14,15,21,8,6,4,9,13,22,11,19,18,10,2,70,71,30,31,27,28,3])). % 73.82/73.80 cnf(3854,plain, % 73.82/73.80 (~P3(f2(f9(a1,a1),a12),f3(a15))), % 73.82/73.80 inference(scs_inference,[],[3731,3794,3087,3689,3796,3676,2973,3685,3767,3798,3399,3107,3325,3238,302,362,54,48,47,50,49,46,51,20,17,12,5,23,7,16,14,15,21,8,6,4,9,13,22,11,19,18,10,2,70,71,30,31,27,28,3,29])). % 73.82/73.80 cnf(3857,plain, % 73.82/73.80 (P1(f5(f9(a1,a1),f9(a1,a1)))), % 73.82/73.80 inference(scs_inference,[],[32,3731,3794,3087,3689,3796,3676,2973,3685,3767,3798,3148,3399,3029,3107,3325,3238,302,2955,2952,362,54,48,47,50,49,46,51,20,17,12,5,23,7,16,14,15,21,8,6,4,9,13,22,11,19,18,10,2,70,71,30,31,27,28,3,29,93,82])). % 73.82/73.80 cnf(3866,plain, % 73.82/73.80 (E(f10(x38661,f2(a12,a1)),f10(x38661,a1))), % 73.82/73.80 inference(rename_variables,[],[3319])). % 73.82/73.80 cnf(3881,plain, % 73.82/73.80 (E(a1,f10(f9(a1,a1),f9(a1,a1)))), % 73.82/73.80 inference(scs_inference,[],[32,3761,3779,3731,3794,3087,3319,3866,3689,3796,3676,2973,2951,3685,3767,3798,3426,3148,3072,3563,3399,3029,3516,3107,3325,3372,3238,3335,302,147,388,2955,2952,295,362,3222,1741,33,54,48,47,50,49,46,51,20,17,12,5,23,7,16,14,15,21,8,6,4,9,13,22,11,19,18,10,2,70,71,30,31,27,28,3,29,93,82,61,74,66,80,90,135,419,160,64,75,87,97])). % 73.82/73.80 cnf(3884,plain, % 73.82/73.80 (P3(f3(a15),f3(a15))), % 73.82/73.80 inference(scs_inference,[],[32,3761,3779,3731,3794,3087,3319,3866,3689,3796,3676,2973,3709,2951,3685,3767,3798,3426,3148,3072,3563,3399,3029,3516,3107,3325,3372,3238,3335,302,147,388,2955,2952,295,362,3222,1741,33,54,48,47,50,49,46,51,20,17,12,5,23,7,16,14,15,21,8,6,4,9,13,22,11,19,18,10,2,70,71,30,31,27,28,3,29,93,82,61,74,66,80,90,135,419,160,64,75,87,97,110])). % 73.82/73.80 cnf(3891,plain, % 73.82/73.80 (E(f9(a1,a12),a12)), % 73.82/73.80 inference(scs_inference,[],[33,48])). % 73.82/73.80 cnf(3897,plain, % 73.82/73.80 (E(f2(a12,f10(a1,a1)),f10(a1,a1))), % 73.82/73.80 inference(scs_inference,[],[3678,153,33,48,54,47,49])). % 73.82/73.80 cnf(3899,plain, % 73.82/73.80 (E(f2(a12,a12),a12)), % 73.82/73.80 inference(scs_inference,[],[3678,153,33,48,54,47,49,51])). % 73.82/73.80 cnf(3908,plain, % 73.82/73.80 (E(f9(a1,x39081),f9(f10(f9(a1,a1),f9(a1,a1)),x39081))), % 73.82/73.80 inference(scs_inference,[],[3678,3881,153,33,48,54,47,49,51,50,46,17,5,20,12])). % 73.82/73.80 cnf(3925,plain, % 73.82/73.80 (~E(f9(a1,a1),f3(a15))), % 73.82/73.80 inference(scs_inference,[],[3849,3678,3881,153,33,48,54,47,49,51,50,46,17,5,20,12,23,16,7,21,4,9,11,15,22,6,8,14,13,18,19,10,2])). % 73.82/73.80 cnf(3928,plain, % 73.82/73.80 (P1(f2(f10(a1,a1),f10(a1,a1)))), % 73.82/73.80 inference(scs_inference,[],[3849,3678,3881,153,33,48,54,47,49,51,50,46,17,5,20,12,23,16,7,21,4,9,11,15,22,6,8,14,13,18,19,10,2,70,71])). % 73.82/73.80 cnf(3930,plain, % 73.82/73.80 (~P3(f2(f9(a1,a1),a12),f9(a1,f3(a15)))), % 73.82/73.80 inference(scs_inference,[],[3849,3854,3291,3678,3881,153,33,48,54,47,49,51,50,46,17,5,20,12,23,16,7,21,4,9,11,15,22,6,8,14,13,18,19,10,2,70,71,30])). % 73.82/73.80 cnf(3932,plain, % 73.82/73.80 (~P5(f9(a1,f3(a15)),f9(a12,f10(a12,a12)))), % 73.82/73.80 inference(scs_inference,[],[3849,3854,3291,3678,652,3881,3329,3353,153,33,48,54,47,49,51,50,46,17,5,20,12,23,16,7,21,4,9,11,15,22,6,8,14,13,18,19,10,2,70,71,30,31,27])). % 73.82/73.80 cnf(3938,plain, % 73.82/73.80 (E(f9(f3(a15),f5(f3(a15),a15)),a15)), % 73.82/73.80 inference(scs_inference,[],[3849,3884,3854,3291,3678,3770,652,3881,3721,3273,3329,3353,3222,153,33,36,48,54,47,49,51,50,46,17,5,20,12,23,16,7,21,4,9,11,15,22,6,8,14,13,18,19,10,2,70,71,30,31,27,28,3,29,92,93])). % 73.82/73.80 cnf(3952,plain, % 73.82/73.80 (P1(f9(a1,f5(a1,a1)))), % 73.82/73.80 inference(scs_inference,[],[32,3849,3884,3082,3197,3854,3692,3291,3678,3762,3808,3857,3770,652,3881,3853,3721,3423,3124,3273,3426,3329,3353,3335,147,421,3222,153,33,36,48,54,47,49,51,50,46,17,5,20,12,23,16,7,21,4,9,11,15,22,6,8,14,13,18,19,10,2,70,71,30,31,27,28,3,29,92,93,83,82,61,56,90,80])). % 73.82/73.80 cnf(3958,plain, % 73.82/73.80 (P3(f3(a15),f9(f3(a15),f3(a15)))), % 73.82/73.80 inference(scs_inference,[],[32,3849,3884,3082,3197,3854,3692,3291,3262,3678,3762,3808,3857,3770,652,3881,3853,3721,3423,3124,3273,3426,3329,674,3353,3335,147,421,3222,1741,153,33,36,48,54,47,49,51,50,46,17,5,20,12,23,16,7,21,4,9,11,15,22,6,8,14,13,18,19,10,2,70,71,30,31,27,28,3,29,92,93,83,82,61,56,90,80,134,96,105])). % 73.82/73.80 cnf(3969,plain, % 73.82/73.80 (P3(f10(a1,a1),f2(f10(a1,a1),f10(a1,a1)))), % 73.82/73.80 inference(scs_inference,[],[3928,256])). % 73.82/73.80 cnf(3970,plain, % 73.82/73.80 (E(f9(a1,a13),a13)), % 73.82/73.80 inference(scs_inference,[],[34,48])). % 73.82/73.80 cnf(3976,plain, % 73.82/73.80 (E(f9(a12,a1),a12)), % 73.82/73.80 inference(scs_inference,[],[3764,33,34,48,54,47,50])). % 73.82/73.80 cnf(3978,plain, % 73.82/73.80 (E(f2(a13,a12),a13)), % 73.82/73.80 inference(scs_inference,[],[3764,33,34,48,54,47,50,51])). % 73.82/73.80 cnf(3980,plain, % 73.82/73.80 (E(f2(a12,a13),a13)), % 73.82/73.80 inference(scs_inference,[],[3764,33,34,48,54,47,50,51,49])). % 73.82/73.80 cnf(3986,plain, % 73.82/73.80 (E(f9(f2(a12,a12),x39861),f9(a12,x39861))), % 73.82/73.80 inference(scs_inference,[],[3899,3764,33,34,48,54,47,50,51,49,46,20,17,12])). % 73.82/73.80 cnf(3988,plain, % 73.82/73.80 (E(f2(x39881,f2(a12,a12)),f2(x39881,a12))), % 73.82/73.80 inference(scs_inference,[],[3899,3764,33,34,48,54,47,50,51,49,46,20,17,12,16,5])). % 73.82/73.80 cnf(3990,plain, % 73.82/73.80 (E(f2(f2(a12,a12),x39901),f2(a12,x39901))), % 73.82/73.80 inference(scs_inference,[],[3899,3764,33,34,48,54,47,50,51,49,46,20,17,12,16,5,23,4])). % 73.82/73.80 cnf(4000,plain, % 73.82/73.80 (E(f10(x40001,f2(a12,a12)),f10(x40001,a12))), % 73.82/73.80 inference(scs_inference,[],[3899,3764,33,34,48,54,47,50,51,49,46,20,17,12,16,5,23,4,9,11,15,6,7,21,8,14,22,19])). % 73.82/73.80 cnf(4005,plain, % 73.82/73.80 (P1(f9(a12,a12))), % 73.82/73.80 inference(scs_inference,[],[3899,3608,3764,33,34,48,54,47,50,51,49,46,20,17,12,16,5,23,4,9,11,15,6,7,21,8,14,22,19,10,13,18,2,70])). % 73.82/73.80 cnf(4007,plain, % 73.82/73.80 (P1(f2(a12,a12))), % 73.82/73.80 inference(scs_inference,[],[3899,3608,3764,33,34,48,54,47,50,51,49,46,20,17,12,16,5,23,4,9,11,15,6,7,21,8,14,22,19,10,13,18,2,70,71])). % 73.82/73.80 cnf(4011,plain, % 73.82/73.80 (~P5(f9(a15,f2(a1,a12)),a12)), % 73.82/73.80 inference(scs_inference,[],[3899,3608,3293,3764,3852,3432,3326,3399,3452,33,34,48,54,47,50,51,49,46,20,17,12,16,5,23,4,9,11,15,6,7,21,8,14,22,19,10,13,18,2,70,71,30,31,27])). % 73.82/73.80 cnf(4013,plain, % 73.82/73.80 (~P5(f9(f3(a15),f2(a1,a12)),f2(a12,a12))), % 73.82/73.80 inference(scs_inference,[],[3899,3608,3293,3764,3852,3432,3326,3399,3452,33,34,48,54,47,50,51,49,46,20,17,12,16,5,23,4,9,11,15,6,7,21,8,14,22,19,10,13,18,2,70,71,30,31,27,28])). % 73.82/73.80 cnf(4037,plain, % 73.82/73.80 (~P3(a1,f3(a15))), % 73.82/73.80 inference(scs_inference,[],[32,3680,3899,3608,3897,3293,3430,3764,3844,3401,3473,3852,3787,2958,3432,3326,3707,3467,3399,1941,3029,3452,3436,3884,3335,692,302,147,2955,2952,854,3222,1741,498,33,34,48,54,47,50,51,49,46,20,17,12,16,5,23,4,9,11,15,6,7,21,8,14,22,19,10,13,18,2,70,71,30,31,27,28,3,29,92,93,83,82,61,90,91,105,956,2817,64,96])). % 73.82/73.80 cnf(4042,plain, % 73.82/73.80 (P5(a12,f9(a12,a12))), % 73.82/73.80 inference(scs_inference,[],[4005,276])). % 73.82/73.80 cnf(4045,plain, % 73.82/73.80 (P5(a1,f9(a12,a12))), % 73.82/73.80 inference(scs_inference,[],[4005,964])). % 73.82/73.80 cnf(4046,plain, % 73.82/73.80 (P5(f10(a1,a1),f9(a12,a12))), % 73.82/73.80 inference(scs_inference,[],[4005,966])). % 73.82/73.80 cnf(4047,plain, % 73.82/73.80 (P1(f2(a12,f2(a12,a12)))), % 73.82/73.80 inference(scs_inference,[],[4007,1031])). % 73.82/73.80 cnf(4048,plain, % 73.82/73.80 (P1(f9(f9(a12,a12),a1))), % 73.82/73.80 inference(scs_inference,[],[4005,1105])). % 73.82/73.80 cnf(4050,plain, % 73.82/73.80 (E(f9(a1,f2(a12,a12)),f2(a12,a12))), % 73.82/73.80 inference(scs_inference,[],[4007,48])). % 73.82/73.80 cnf(4058,plain, % 73.82/73.80 (E(f9(f2(a12,a12),a1),f2(a12,a12))), % 73.82/73.80 inference(scs_inference,[],[4005,4007,48,54,47,49,50])). % 73.82/73.80 cnf(4101,plain, % 73.82/73.80 (P1(f5(f9(a12,a12),f9(a12,a12)))), % 73.82/73.80 inference(scs_inference,[],[32,4005,4007,4037,3138,3925,3891,3976,3431,3299,3562,853,3077,4011,3254,3518,657,3353,295,153,48,54,47,49,50,51,46,17,16,23,20,5,11,15,12,4,9,7,14,8,21,6,22,10,19,18,13,2,70,71,30,31,27,3,28,29,92,93,83,82])). % 73.82/73.80 cnf(4125,plain, % 73.82/73.80 (P5(a12,f9(a12,a12))), % 73.82/73.80 inference(scs_inference,[],[4048,1098])). % 73.82/73.80 cnf(4133,plain, % 73.82/73.80 (E(f9(a1,a14),a14)), % 73.82/73.80 inference(scs_inference,[],[35,48])). % 73.82/73.80 cnf(4139,plain, % 73.82/73.80 (E(f2(a12,a14),a14)), % 73.82/73.80 inference(scs_inference,[],[3846,35,48,47,54,49])). % 73.82/73.80 cnf(4166,plain, % 73.82/73.80 (E(f9(x41661,f9(a1,a13)),f9(x41661,a13))), % 73.82/73.80 inference(scs_inference,[],[3970,3846,34,35,48,47,54,49,50,51,46,23,17,20,16,11,4,12,14,5,15,9,21,7,10,6,8,18,22,19,13])). % 73.82/73.80 cnf(4167,plain, % 73.82/73.80 (~E(f2(a1,a1),f3(f3(a15)))), % 73.82/73.80 inference(scs_inference,[],[3970,3428,3846,34,35,48,47,54,49,50,51,46,23,17,20,16,11,4,12,14,5,15,9,21,7,10,6,8,18,22,19,13,2])). % 73.82/73.80 cnf(4170,plain, % 73.82/73.80 (P1(f2(f2(a12,a12),f2(a12,a12)))), % 73.82/73.80 inference(scs_inference,[],[3970,3428,3846,4007,34,35,48,47,54,49,50,51,46,23,17,20,16,11,4,12,14,5,15,9,21,7,10,6,8,18,22,19,13,2,70,71])). % 73.82/73.80 cnf(4172,plain, % 73.82/73.80 (~P3(a15,f9(a1,a13))), % 73.82/73.80 inference(scs_inference,[],[3970,3428,3846,4007,1469,34,35,48,47,54,49,50,51,46,23,17,20,16,11,4,12,14,5,15,9,21,7,10,6,8,18,22,19,13,2,70,71,30])). % 73.82/73.80 cnf(4173,plain, % 73.82/73.80 (~P5(f9(a15,f2(a1,a12)),f2(a12,a12))), % 73.82/73.80 inference(scs_inference,[],[3970,4013,3428,3846,4007,3399,1469,34,35,48,47,54,49,50,51,46,23,17,20,16,11,4,12,14,5,15,9,21,7,10,6,8,18,22,19,13,2,70,71,30,27])). % 73.82/73.80 cnf(4177,plain, % 73.82/73.80 (E(f2(x41771,f2(a12,a12)),f2(x41771,a12))), % 73.82/73.80 inference(rename_variables,[],[3988])). % 73.82/73.80 cnf(4180,plain, % 73.82/73.80 (E(f2(x41801,f2(a12,a12)),f2(x41801,a12))), % 73.82/73.80 inference(rename_variables,[],[3988])). % 73.82/73.80 cnf(4185,plain, % 73.82/73.80 (P5(f2(a12,a12),f2(a12,f2(a12,a12)))), % 73.82/73.80 inference(scs_inference,[],[32,4042,4045,3970,4013,3428,3988,4177,4180,3846,4047,3930,3326,4007,3399,1469,2989,4005,422,33,34,35,48,47,54,49,50,51,46,23,17,20,16,11,4,12,14,5,15,9,21,7,10,6,8,18,22,19,13,2,70,71,30,27,31,28,3,29,93,82,61])). % 73.82/73.80 cnf(4193,plain, % 73.82/73.80 (~E(f2(f3(a15),f3(a15)),f2(f3(a15),a1))), % 73.82/73.80 inference(scs_inference,[],[32,4042,4045,3970,4013,3428,3988,4177,4180,4000,3846,3958,4047,3930,3326,4007,3321,3399,1469,2989,4005,422,3222,1741,33,34,35,48,47,54,49,50,51,46,23,17,20,16,11,4,12,14,5,15,9,21,7,10,6,8,18,22,19,13,2,70,71,30,27,31,28,3,29,93,82,61,90,128,87])). % 73.82/73.80 cnf(4208,plain, % 73.82/73.80 (E(f9(a1,a15),a15)), % 73.82/73.80 inference(scs_inference,[],[36,48])). % 73.82/73.80 cnf(4214,plain, % 73.82/73.80 (E(f2(a12,a15),a15)), % 73.82/73.80 inference(scs_inference,[],[4101,36,48,47,54,49])). % 73.82/73.80 cnf(4243,plain, % 73.82/73.80 (P1(f9(a13,a13))), % 73.82/73.80 inference(scs_inference,[],[3978,367,4101,34,35,36,48,47,54,49,50,51,46,23,17,20,16,12,14,4,11,7,5,15,6,21,8,9,10,22,19,18,13,2,70])). % 73.82/73.80 cnf(4245,plain, % 73.82/73.80 (P1(f2(a13,a13))), % 73.82/73.80 inference(scs_inference,[],[3978,367,4101,34,35,36,48,47,54,49,50,51,46,23,17,20,16,12,14,4,11,7,5,15,6,21,8,9,10,22,19,18,13,2,70,71])). % 73.82/73.80 cnf(4247,plain, % 73.82/73.80 (~P3(a15,f9(a1,f9(a1,a13)))), % 73.82/73.80 inference(scs_inference,[],[3978,4172,4166,367,4101,34,35,36,48,47,54,49,50,51,46,23,17,20,16,12,14,4,11,7,5,15,6,21,8,9,10,22,19,18,13,2,70,71,30])). % 73.82/73.80 cnf(4259,plain, % 73.82/73.80 (P1(f5(f10(a1,a1),f9(a12,a12)))), % 73.82/73.80 inference(scs_inference,[],[4046,3099,3978,4172,4050,4173,4166,367,4101,3607,3154,1298,3260,3392,3908,3938,3353,309,4005,261,2952,153,34,35,36,48,47,54,49,50,51,46,23,17,20,16,12,14,4,11,7,5,15,6,21,8,9,10,22,19,18,13,2,70,71,30,27,31,28,3,29,127,93,82])). % 73.82/73.80 cnf(4271,plain, % 73.82/73.80 (~P1(f2(a14,a14))), % 73.82/73.80 inference(scs_inference,[],[32,4046,3099,3978,4172,4050,4173,4166,367,3969,4101,3607,3154,1298,3260,3392,4193,3908,3938,3928,1847,3213,3709,657,3323,3353,501,172,309,4005,261,2952,3222,1741,498,153,34,35,36,48,47,54,49,50,51,46,23,17,20,16,12,14,4,11,7,5,15,6,21,8,9,10,22,19,18,13,2,70,71,30,27,31,28,3,29,127,93,82,90,128,91,105,110,1470])). % 73.82/73.80 cnf(4273,plain, % 73.82/73.80 (~E(a1,f2(a14,a14))), % 73.82/73.80 inference(scs_inference,[],[32,4046,3099,3978,4172,4050,4173,4166,367,3969,4101,3607,3154,1298,3260,3392,4193,3908,3938,3928,1847,3213,3709,657,3323,3353,501,172,309,4005,261,2952,3222,1741,498,153,34,35,36,48,47,54,49,50,51,46,23,17,20,16,12,14,4,11,7,5,15,6,21,8,9,10,22,19,18,13,2,70,71,30,27,31,28,3,29,127,93,82,90,128,91,105,110,1470,219,24])). % 73.82/73.80 cnf(4289,plain, % 73.82/73.80 (P5(a13,f9(a13,a13))), % 73.82/73.80 inference(scs_inference,[],[4243,405])). % 73.82/73.80 cnf(4341,plain, % 73.82/73.80 (~E(f9(a13,a13),f2(a14,a14))), % 73.82/73.80 inference(scs_inference,[],[4243,3980,4273,4271,48,47,54,50,49,51,46,23,17,12,16,4,20,5,14,7,11,15,21,6,22,8,9,10,18,13,19,2,70,24])). % 73.82/73.80 cnf(4344,plain, % 73.82/73.80 (~P3(a15,f2(a12,a13))), % 73.82/73.80 inference(scs_inference,[],[4243,3980,4273,4271,1469,48,47,54,50,49,51,46,23,17,12,16,4,20,5,14,7,11,15,21,6,22,8,9,10,18,13,19,2,70,24,71,30])). % 73.82/73.80 cnf(4372,plain, % 73.82/73.80 (~P2(f9(a1,f5(a1,a1)))), % 73.82/73.80 inference(scs_inference,[],[4125,4243,4245,3980,4273,4271,4208,3564,3986,4167,4247,3932,3579,3952,3027,3925,3330,1469,3452,168,3335,4005,2973,2955,2952,422,237,3222,33,36,48,47,54,50,49,51,46,23,17,12,16,4,20,5,14,7,11,15,21,6,22,8,9,10,18,13,19,2,70,24,71,30,31,27,28,3,29,127,93,82,85,84,80,90,77,76,45,44])). % 73.82/73.80 cnf(4374,plain, % 73.82/73.80 (P1(f3(f9(f3(a15),f3(a15))))), % 73.82/73.80 inference(scs_inference,[],[4125,4243,4245,3980,4273,4271,4208,3564,3986,4167,4247,3932,3579,3952,3027,3925,3242,3330,3321,1469,3452,168,3335,4005,2973,2955,2952,422,237,3222,33,36,48,47,54,50,49,51,46,23,17,12,16,4,20,5,14,7,11,15,21,6,22,8,9,10,18,13,19,2,70,24,71,30,31,27,28,3,29,127,93,82,85,84,80,90,77,76,45,44,52])). % 73.82/73.80 cnf(4376,plain, % 73.82/73.80 (P2(f3(f9(f3(a15),f3(a15))))), % 73.82/73.80 inference(scs_inference,[],[4125,4243,4245,3980,4273,4271,4208,3564,3986,4167,4247,3932,3579,3952,3027,3925,3242,3330,3321,1469,3452,168,3335,4005,2973,2955,2952,422,237,3222,33,36,48,47,54,50,49,51,46,23,17,12,16,4,20,5,14,7,11,15,21,6,22,8,9,10,18,13,19,2,70,24,71,30,31,27,28,3,29,127,93,82,85,84,80,90,77,76,45,44,52,53])). % 73.82/73.80 cnf(4442,plain, % 73.82/73.80 (~E(f2(a14,a14),f10(a1,a1))), % 73.82/73.80 inference(scs_inference,[],[32,4289,4341,4133,4344,4214,4058,3990,4170,4185,4372,4374,4376,3761,4173,4047,4245,4271,582,3238,4007,4243,147,2955,3222,34,48,47,54,50,49,51,46,23,17,16,12,20,5,14,4,11,15,7,9,6,18,10,21,8,22,19,13,2,45,70,44,71,30,31,27,28,3,29,56,93,82,85,80])). % 73.82/73.80 cnf(4493,plain, % 73.82/73.80 ($false), % 73.82/73.80 inference(scs_inference,[],[4442,4139,4259,4271,4007,3899,35,36,47,54,50,46,23,17,16,4,20,12,5,14,11,10,9,18,21,15,7,8,22,6,19,13,2,45,70,71]), % 73.82/73.80 ['proof']). % 73.82/73.80 % SZS output end Proof % 73.82/73.80 % Total time :73.040000s %------------------------------------------------------------------------------