%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM521+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 : n023.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:48 EDT 2024 % Result : Theorem 65.01s 65.15s % Output : CNFRefutation 65.01s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : NUM521+3 : TPTP v8.2.0. Released v4.0.0. % 0.03/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.35 % Computer : n023.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Sun Jun 23 03:18:24 EDT 2024 % 0.13/0.35 % CPUTime : % 0.52/0.57 start to proof:theBenchmark % 65.01/65.13 %------------------------------------------- % 65.01/65.13 % File :CSE---1.7 % 65.01/65.13 % Problem :theBenchmark % 65.01/65.13 % Transform :cnf % 65.01/65.13 % Format :tptp:raw % 65.01/65.13 % Command :java -jar mcs_scs.jar %d %s % 65.01/65.13 % 65.01/65.13 % Result :Theorem 63.770000s % 65.01/65.13 % Output :CNFRefutation 63.770000s % 65.01/65.13 %------------------------------------------- % 65.01/65.13 %------------------------------------------------------------------------------ % 65.01/65.13 % File : NUM521+3 : TPTP v8.2.0. Released v4.0.0. % 65.01/65.13 % Domain : Number Theory % 65.01/65.13 % Problem : Square root of a prime is irrational 14_04, 02 expansion % 65.01/65.13 % Version : Especial. % 65.01/65.13 % English : % 65.01/65.14 % 65.01/65.14 % Refs : [LPV06] Lyaletski et al. (2006), SAD as a Mathematical Assista % 65.01/65.14 % : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 65.01/65.14 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 65.01/65.14 % Source : [Pas08] % 65.01/65.14 % Names : primes_14_04.02 [Pas08] % 65.01/65.14 % 65.01/65.14 % Status : ContradictoryAxioms % 65.01/65.14 % Rating : 0.22 v8.2.0, 0.19 v8.1.0, 0.22 v7.5.0, 0.25 v7.4.0, 0.14 v7.3.0, 0.00 v7.0.0, 0.13 v6.4.0, 0.19 v6.3.0, 0.12 v6.2.0, 0.16 v6.1.0, 0.23 v6.0.0, 0.26 v5.5.0, 0.33 v5.4.0, 0.39 v5.3.0, 0.44 v5.2.0, 0.30 v5.1.0, 0.43 v5.0.0, 0.46 v4.1.0, 0.48 v4.0.1, 0.78 v4.0.0 % 65.01/65.14 % Syntax : Number of formulae : 45 ( 1 unt; 5 def) % 65.01/65.14 % Number of atoms : 240 ( 78 equ) % 65.01/65.14 % Maximal formula atoms : 22 ( 5 avg) % 65.01/65.14 % Number of connectives : 224 ( 29 ~; 20 |; 106 &) % 65.01/65.14 % ( 5 <=>; 64 =>; 0 <=; 0 <~>) % 65.01/65.14 % Maximal formula depth : 16 ( 6 avg) % 65.01/65.14 % Maximal term depth : 3 ( 1 avg) % 65.01/65.14 % Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty) % 65.01/65.14 % Number of functors : 9 ( 9 usr; 5 con; 0-2 aty) % 65.01/65.14 % Number of variables : 99 ( 84 !; 15 ?) % 65.01/65.14 % SPC : FOF_CAX_RFO_SEQ % 65.01/65.14 % 65.01/65.14 % Comments : Problem generated by the SAD system [VLP07] % 65.01/65.14 %------------------------------------------------------------------------------ % 65.01/65.14 fof(mNatSort,axiom, % 65.01/65.14 ! [W0] : % 65.01/65.14 ( aNaturalNumber0(W0) % 65.01/65.14 => $true ) ). % 65.01/65.14 % 65.01/65.14 fof(mSortsC,axiom, % 65.01/65.14 aNaturalNumber0(sz00) ). % 65.01/65.14 % 65.01/65.14 fof(mSortsC_01,axiom, % 65.01/65.14 ( aNaturalNumber0(sz10) % 65.01/65.14 & sz10 != sz00 ) ). % 65.01/65.14 % 65.01/65.14 fof(mSortsB,axiom, % 65.01/65.14 ! [W0,W1] : % 65.01/65.14 ( ( aNaturalNumber0(W0) % 65.01/65.14 & aNaturalNumber0(W1) ) % 65.01/65.14 => aNaturalNumber0(sdtpldt0(W0,W1)) ) ). % 65.01/65.14 % 65.01/65.14 fof(mSortsB_02,axiom, % 65.01/65.14 ! [W0,W1] : % 65.01/65.14 ( ( aNaturalNumber0(W0) % 65.01/65.14 & aNaturalNumber0(W1) ) % 65.01/65.14 => aNaturalNumber0(sdtasdt0(W0,W1)) ) ). % 65.01/65.14 % 65.01/65.14 fof(mAddComm,axiom, % 65.01/65.14 ! [W0,W1] : % 65.01/65.14 ( ( aNaturalNumber0(W0) % 65.01/65.14 & aNaturalNumber0(W1) ) % 65.01/65.14 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 65.01/65.14 % 65.01/65.14 fof(mAddAsso,axiom, % 65.01/65.14 ! [W0,W1,W2] : % 65.01/65.14 ( ( aNaturalNumber0(W0) % 65.01/65.14 & aNaturalNumber0(W1) % 65.01/65.14 & aNaturalNumber0(W2) ) % 65.01/65.14 => sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) ). % 65.01/65.14 % 65.01/65.14 fof(m_AddZero,axiom, % 65.01/65.14 ! [W0] : % 65.01/65.14 ( aNaturalNumber0(W0) % 65.01/65.14 => ( sdtpldt0(W0,sz00) = W0 % 65.01/65.14 & W0 = sdtpldt0(sz00,W0) ) ) ). % 65.01/65.14 % 65.01/65.14 fof(mMulComm,axiom, % 65.01/65.14 ! [W0,W1] : % 65.01/65.14 ( ( aNaturalNumber0(W0) % 65.01/65.14 & aNaturalNumber0(W1) ) % 65.01/65.14 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 65.01/65.14 % 65.01/65.14 fof(mMulAsso,axiom, % 65.01/65.14 ! [W0,W1,W2] : % 65.01/65.14 ( ( aNaturalNumber0(W0) % 65.01/65.14 & aNaturalNumber0(W1) % 65.01/65.14 & aNaturalNumber0(W2) ) % 65.01/65.14 => sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) ). % 65.01/65.14 % 65.01/65.14 fof(m_MulUnit,axiom, % 65.01/65.14 ! [W0] : % 65.01/65.14 ( aNaturalNumber0(W0) % 65.01/65.14 => ( sdtasdt0(W0,sz10) = W0 % 65.01/65.14 & W0 = sdtasdt0(sz10,W0) ) ) ). % 65.01/65.14 % 65.01/65.14 fof(m_MulZero,axiom, % 65.01/65.14 ! [W0] : % 65.01/65.14 ( aNaturalNumber0(W0) % 65.01/65.14 => ( sdtasdt0(W0,sz00) = sz00 % 65.01/65.14 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 65.01/65.14 % 65.01/65.14 fof(mAMDistr,axiom, % 65.01/65.14 ! [W0,W1,W2] : % 65.01/65.14 ( ( aNaturalNumber0(W0) % 65.01/65.14 & aNaturalNumber0(W1) % 65.01/65.14 & aNaturalNumber0(W2) ) % 65.01/65.14 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 65.01/65.14 & sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ). % 65.01/65.14 % 65.01/65.14 fof(mAddCanc,axiom, % 65.01/65.14 ! [W0,W1,W2] : % 65.01/65.14 ( ( aNaturalNumber0(W0) % 65.01/65.14 & aNaturalNumber0(W1) % 65.01/65.14 & aNaturalNumber0(W2) ) % 65.01/65.14 => ( ( sdtpldt0(W0,W1) = sdtpldt0(W0,W2) % 65.01/65.14 | sdtpldt0(W1,W0) = sdtpldt0(W2,W0) ) % 65.01/65.14 => W1 = W2 ) ) ). % 65.01/65.14 % 65.01/65.14 fof(mMulCanc,axiom, % 65.01/65.14 ! [W0] : % 65.01/65.14 ( aNaturalNumber0(W0) % 65.01/65.14 => ( W0 != sz00 % 65.01/65.14 => ! [W1,W2] : % 65.01/65.14 ( ( aNaturalNumber0(W1) % 65.01/65.14 & aNaturalNumber0(W2) ) % 65.01/65.14 => ( ( sdtasdt0(W0,W1) = sdtasdt0(W0,W2) % 65.01/65.14 | sdtasdt0(W1,W0) = sdtasdt0(W2,W0) ) % 65.01/65.14 => W1 = W2 ) ) ) ) ). % 65.01/65.14 % 65.01/65.14 fof(mZeroAdd,axiom, % 65.01/65.14 ! [W0,W1] : % 65.01/65.14 ( ( aNaturalNumber0(W0) % 65.01/65.14 & aNaturalNumber0(W1) ) % 65.01/65.14 => ( sdtpldt0(W0,W1) = sz00 % 65.01/65.14 => ( W0 = sz00 % 65.01/65.14 & W1 = sz00 ) ) ) ). % 65.01/65.14 % 65.01/65.14 fof(mZeroMul,axiom, % 65.01/65.14 ! [W0,W1] : % 65.01/65.14 ( ( aNaturalNumber0(W0) % 65.01/65.14 & aNaturalNumber0(W1) ) % 65.01/65.14 => ( sdtasdt0(W0,W1) = sz00 % 65.01/65.14 => ( W0 = sz00 % 65.01/65.14 | W1 = sz00 ) ) ) ). % 65.01/65.14 % 65.01/65.14 fof(mDefLE,definition, % 65.01/65.14 ! [W0,W1] : % 65.01/65.14 ( ( aNaturalNumber0(W0) % 65.01/65.14 & aNaturalNumber0(W1) ) % 65.01/65.14 => ( sdtlseqdt0(W0,W1) % 65.01/65.14 <=> ? [W2] : % 65.01/65.14 ( aNaturalNumber0(W2) % 65.01/65.14 & sdtpldt0(W0,W2) = W1 ) ) ) ). % 65.01/65.14 % 65.01/65.14 fof(mDefDiff,definition, % 65.01/65.14 ! [W0,W1] : % 65.01/65.14 ( ( aNaturalNumber0(W0) % 65.01/65.14 & aNaturalNumber0(W1) ) % 65.01/65.14 => ( sdtlseqdt0(W0,W1) % 65.01/65.14 => ! [W2] : % 65.01/65.14 ( W2 = sdtmndt0(W1,W0) % 65.01/65.14 <=> ( aNaturalNumber0(W2) % 65.01/65.14 & sdtpldt0(W0,W2) = W1 ) ) ) ) ). % 65.01/65.14 % 65.01/65.14 fof(mLERefl,axiom, % 65.01/65.14 ! [W0] : % 65.01/65.14 ( aNaturalNumber0(W0) % 65.01/65.14 => sdtlseqdt0(W0,W0) ) ). % 65.01/65.14 % 65.01/65.14 fof(mLEAsym,axiom, % 65.01/65.14 ! [W0,W1] : % 65.01/65.14 ( ( aNaturalNumber0(W0) % 65.01/65.14 & aNaturalNumber0(W1) ) % 65.01/65.14 => ( ( sdtlseqdt0(W0,W1) % 65.01/65.14 & sdtlseqdt0(W1,W0) ) % 65.01/65.14 => W0 = W1 ) ) ). % 65.01/65.14 % 65.01/65.14 fof(mLETran,axiom, % 65.01/65.14 ! [W0,W1,W2] : % 65.01/65.14 ( ( aNaturalNumber0(W0) % 65.01/65.14 & aNaturalNumber0(W1) % 65.01/65.14 & aNaturalNumber0(W2) ) % 65.01/65.14 => ( ( sdtlseqdt0(W0,W1) % 65.01/65.14 & sdtlseqdt0(W1,W2) ) % 65.01/65.14 => sdtlseqdt0(W0,W2) ) ) ). % 65.01/65.14 % 65.01/65.14 fof(mLETotal,axiom, % 65.01/65.14 ! [W0,W1] : % 65.01/65.14 ( ( aNaturalNumber0(W0) % 65.01/65.14 & aNaturalNumber0(W1) ) % 65.01/65.14 => ( sdtlseqdt0(W0,W1) % 65.01/65.14 | ( W1 != W0 % 65.01/65.14 & sdtlseqdt0(W1,W0) ) ) ) ). % 65.01/65.14 % 65.01/65.14 fof(mMonAdd,axiom, % 65.01/65.14 ! [W0,W1] : % 65.01/65.14 ( ( aNaturalNumber0(W0) % 65.01/65.14 & aNaturalNumber0(W1) ) % 65.01/65.14 => ( ( W0 != W1 % 65.01/65.14 & sdtlseqdt0(W0,W1) ) % 65.01/65.14 => ! [W2] : % 65.01/65.14 ( aNaturalNumber0(W2) % 65.01/65.14 => ( sdtpldt0(W2,W0) != sdtpldt0(W2,W1) % 65.01/65.14 & sdtlseqdt0(sdtpldt0(W2,W0),sdtpldt0(W2,W1)) % 65.01/65.14 & sdtpldt0(W0,W2) != sdtpldt0(W1,W2) % 65.01/65.14 & sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W2)) ) ) ) ) ). % 65.01/65.14 % 65.01/65.14 fof(mMonMul,axiom, % 65.01/65.14 ! [W0,W1,W2] : % 65.01/65.14 ( ( aNaturalNumber0(W0) % 65.01/65.14 & aNaturalNumber0(W1) % 65.01/65.14 & aNaturalNumber0(W2) ) % 65.01/65.14 => ( ( W0 != sz00 % 65.01/65.14 & W1 != W2 % 65.01/65.14 & sdtlseqdt0(W1,W2) ) % 65.01/65.14 => ( sdtasdt0(W0,W1) != sdtasdt0(W0,W2) % 65.01/65.14 & sdtlseqdt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 65.01/65.14 & sdtasdt0(W1,W0) != sdtasdt0(W2,W0) % 65.01/65.14 & sdtlseqdt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ) ). % 65.01/65.14 % 65.01/65.14 fof(mLENTr,axiom, % 65.01/65.14 ! [W0] : % 65.01/65.14 ( aNaturalNumber0(W0) % 65.01/65.14 => ( W0 = sz00 % 65.01/65.14 | W0 = sz10 % 65.01/65.14 | ( sz10 != W0 % 65.01/65.14 & sdtlseqdt0(sz10,W0) ) ) ) ). % 65.01/65.14 % 65.01/65.14 fof(mMonMul2,axiom, % 65.01/65.14 ! [W0,W1] : % 65.01/65.14 ( ( aNaturalNumber0(W0) % 65.01/65.14 & aNaturalNumber0(W1) ) % 65.01/65.14 => ( W0 != sz00 % 65.01/65.14 => sdtlseqdt0(W1,sdtasdt0(W1,W0)) ) ) ). % 65.01/65.14 % 65.01/65.14 fof(mIH,axiom, % 65.01/65.14 ! [W0,W1] : % 65.01/65.14 ( ( aNaturalNumber0(W0) % 65.01/65.14 & aNaturalNumber0(W1) ) % 65.01/65.14 => ( iLess0(W0,W1) % 65.01/65.15 => $true ) ) ). % 65.01/65.15 % 65.01/65.15 fof(mIH_03,axiom, % 65.01/65.15 ! [W0,W1] : % 65.01/65.15 ( ( aNaturalNumber0(W0) % 65.01/65.15 & aNaturalNumber0(W1) ) % 65.01/65.15 => ( ( W0 != W1 % 65.01/65.15 & sdtlseqdt0(W0,W1) ) % 65.01/65.15 => iLess0(W0,W1) ) ) ). % 65.01/65.15 % 65.01/65.15 fof(mDefDiv,definition, % 65.01/65.15 ! [W0,W1] : % 65.01/65.15 ( ( aNaturalNumber0(W0) % 65.01/65.15 & aNaturalNumber0(W1) ) % 65.01/65.15 => ( doDivides0(W0,W1) % 65.01/65.15 <=> ? [W2] : % 65.01/65.15 ( aNaturalNumber0(W2) % 65.01/65.15 & W1 = sdtasdt0(W0,W2) ) ) ) ). % 65.01/65.15 % 65.01/65.15 fof(mDefQuot,definition, % 65.01/65.15 ! [W0,W1] : % 65.01/65.15 ( ( aNaturalNumber0(W0) % 65.01/65.15 & aNaturalNumber0(W1) ) % 65.01/65.15 => ( ( W0 != sz00 % 65.01/65.15 & doDivides0(W0,W1) ) % 65.01/65.15 => ! [W2] : % 65.01/65.15 ( W2 = sdtsldt0(W1,W0) % 65.01/65.15 <=> ( aNaturalNumber0(W2) % 65.01/65.15 & W1 = sdtasdt0(W0,W2) ) ) ) ) ). % 65.01/65.15 % 65.01/65.15 fof(mDivTrans,axiom, % 65.01/65.15 ! [W0,W1,W2] : % 65.01/65.15 ( ( aNaturalNumber0(W0) % 65.01/65.15 & aNaturalNumber0(W1) % 65.01/65.15 & aNaturalNumber0(W2) ) % 65.01/65.15 => ( ( doDivides0(W0,W1) % 65.01/65.15 & doDivides0(W1,W2) ) % 65.01/65.15 => doDivides0(W0,W2) ) ) ). % 65.01/65.15 % 65.01/65.15 fof(mDivSum,axiom, % 65.01/65.15 ! [W0,W1,W2] : % 65.01/65.15 ( ( aNaturalNumber0(W0) % 65.01/65.15 & aNaturalNumber0(W1) % 65.01/65.15 & aNaturalNumber0(W2) ) % 65.01/65.15 => ( ( doDivides0(W0,W1) % 65.01/65.15 & doDivides0(W0,W2) ) % 65.01/65.15 => doDivides0(W0,sdtpldt0(W1,W2)) ) ) ). % 65.01/65.15 % 65.01/65.15 fof(mDivMin,axiom, % 65.01/65.15 ! [W0,W1,W2] : % 65.01/65.15 ( ( aNaturalNumber0(W0) % 65.01/65.15 & aNaturalNumber0(W1) % 65.01/65.15 & aNaturalNumber0(W2) ) % 65.01/65.15 => ( ( doDivides0(W0,W1) % 65.01/65.15 & doDivides0(W0,sdtpldt0(W1,W2)) ) % 65.01/65.15 => doDivides0(W0,W2) ) ) ). % 65.01/65.15 % 65.01/65.15 fof(mDivLE,axiom, % 65.01/65.15 ! [W0,W1] : % 65.01/65.15 ( ( aNaturalNumber0(W0) % 65.01/65.15 & aNaturalNumber0(W1) ) % 65.01/65.15 => ( ( doDivides0(W0,W1) % 65.01/65.15 & W1 != sz00 ) % 65.01/65.15 => sdtlseqdt0(W0,W1) ) ) ). % 65.01/65.15 % 65.01/65.15 fof(mDivAsso,axiom, % 65.01/65.15 ! [W0,W1] : % 65.01/65.15 ( ( aNaturalNumber0(W0) % 65.01/65.15 & aNaturalNumber0(W1) ) % 65.01/65.15 => ( ( W0 != sz00 % 65.01/65.15 & doDivides0(W0,W1) ) % 65.01/65.15 => ! [W2] : % 65.01/65.15 ( aNaturalNumber0(W2) % 65.01/65.15 => sdtasdt0(W2,sdtsldt0(W1,W0)) = sdtsldt0(sdtasdt0(W2,W1),W0) ) ) ) ). % 65.01/65.15 % 65.01/65.15 fof(mDefPrime,definition, % 65.01/65.15 ! [W0] : % 65.01/65.15 ( aNaturalNumber0(W0) % 65.01/65.15 => ( isPrime0(W0) % 65.01/65.15 <=> ( W0 != sz00 % 65.01/65.15 & W0 != sz10 % 65.01/65.15 & ! [W1] : % 65.01/65.15 ( ( aNaturalNumber0(W1) % 65.01/65.15 & doDivides0(W1,W0) ) % 65.01/65.15 => ( W1 = sz10 % 65.01/65.15 | W1 = W0 ) ) ) ) ) ). % 65.01/65.15 % 65.01/65.15 fof(mPrimDiv,axiom, % 65.01/65.15 ! [W0] : % 65.01/65.15 ( ( aNaturalNumber0(W0) % 65.01/65.15 & W0 != sz00 % 65.01/65.15 & W0 != sz10 ) % 65.01/65.15 => ? [W1] : % 65.01/65.15 ( aNaturalNumber0(W1) % 65.01/65.15 & doDivides0(W1,W0) % 65.01/65.15 & isPrime0(W1) ) ) ). % 65.01/65.15 % 65.01/65.15 fof(m__1837,hypothesis, % 65.01/65.15 ( aNaturalNumber0(xn) % 65.01/65.15 & aNaturalNumber0(xm) % 65.01/65.15 & aNaturalNumber0(xp) ) ). % 65.01/65.15 % 65.01/65.15 fof(m__1799,hypothesis, % 65.01/65.15 ! [W0,W1,W2] : % 65.01/65.15 ( ( aNaturalNumber0(W0) % 65.01/65.15 & aNaturalNumber0(W1) % 65.01/65.15 & aNaturalNumber0(W2) ) % 65.01/65.15 => ( ( ( ( W2 != sz00 % 65.01/65.15 & W2 != sz10 % 65.01/65.15 & ! [W3] : % 65.01/65.15 ( ( aNaturalNumber0(W3) % 65.01/65.15 & ? [W4] : % 65.01/65.15 ( aNaturalNumber0(W4) % 65.01/65.15 & W2 = sdtasdt0(W3,W4) ) % 65.01/65.15 & doDivides0(W3,W2) ) % 65.01/65.15 => ( W3 = sz10 % 65.01/65.15 | W3 = W2 ) ) ) % 65.01/65.15 | isPrime0(W2) ) % 65.01/65.15 & ( ? [W3] : % 65.01/65.15 ( aNaturalNumber0(W3) % 65.01/65.15 & sdtasdt0(W0,W1) = sdtasdt0(W2,W3) ) % 65.01/65.15 | doDivides0(W2,sdtasdt0(W0,W1)) ) ) % 65.01/65.15 => ( iLess0(sdtpldt0(sdtpldt0(W0,W1),W2),sdtpldt0(sdtpldt0(xn,xm),xp)) % 65.01/65.15 => ( ( ? [W3] : % 65.01/65.15 ( aNaturalNumber0(W3) % 65.01/65.15 & W0 = sdtasdt0(W2,W3) ) % 65.01/65.15 & doDivides0(W2,W0) ) % 65.01/65.15 | ( ? [W3] : % 65.01/65.15 ( aNaturalNumber0(W3) % 65.01/65.15 & W1 = sdtasdt0(W2,W3) ) % 65.01/65.15 & doDivides0(W2,W1) ) ) ) ) ) ). % 65.01/65.15 % 65.01/65.15 fof(m__1860,hypothesis, % 65.01/65.15 ( xp != sz00 % 65.01/65.15 & xp != sz10 % 65.01/65.15 & ! [W0] : % 65.01/65.15 ( ( aNaturalNumber0(W0) % 65.01/65.15 & ( ? [W1] : % 65.01/65.15 ( aNaturalNumber0(W1) % 65.01/65.15 & xp = sdtasdt0(W0,W1) ) % 65.01/65.15 | doDivides0(W0,xp) ) ) % 65.01/65.15 => ( W0 = sz10 % 65.01/65.15 | W0 = xp ) ) % 65.01/65.15 & isPrime0(xp) % 65.01/65.15 & ? [W0] : % 65.01/65.15 ( aNaturalNumber0(W0) % 65.01/65.15 & sdtasdt0(xn,xm) = sdtasdt0(xp,W0) ) % 65.01/65.15 & doDivides0(xp,sdtasdt0(xn,xm)) ) ). % 65.01/65.15 % 65.01/65.15 fof(m__1870,hypothesis, % 65.01/65.15 ~ ( ? [W0] : % 65.01/65.15 ( aNaturalNumber0(W0) % 65.01/65.15 & sdtpldt0(xp,W0) = xn ) % 65.01/65.15 | sdtlseqdt0(xp,xn) ) ). % 65.01/65.15 % 65.01/65.15 fof(m__2075,hypothesis, % 65.01/65.15 ~ ( ? [W0] : % 65.01/65.15 ( aNaturalNumber0(W0) % 65.01/65.15 & sdtpldt0(xp,W0) = xm ) % 65.01/65.15 | sdtlseqdt0(xp,xm) ) ). % 65.01/65.15 % 65.01/65.15 fof(m__2287,hypothesis, % 65.01/65.15 ~ ( xn != xp % 65.01/65.15 & ( ? [W0] : % 65.01/65.15 ( aNaturalNumber0(W0) % 65.01/65.15 & sdtpldt0(xn,W0) = xp ) % 65.01/65.15 | sdtlseqdt0(xn,xp) ) % 65.01/65.15 & xm != xp % 65.01/65.15 & ( ? [W0] : % 65.01/65.15 ( aNaturalNumber0(W0) % 65.01/65.15 & sdtpldt0(xm,W0) = xp ) % 65.01/65.15 | sdtlseqdt0(xm,xp) ) ) ). % 65.01/65.15 % 65.01/65.15 fof(m__,conjecture, % 65.01/65.15 ( ? [W0] : % 65.01/65.15 ( aNaturalNumber0(W0) % 65.01/65.15 & xn = sdtasdt0(xp,W0) ) % 65.01/65.15 | doDivides0(xp,xn) % 65.01/65.15 | ? [W0] : % 65.01/65.15 ( aNaturalNumber0(W0) % 65.01/65.15 & xm = sdtasdt0(xp,W0) ) % 65.01/65.15 | doDivides0(xp,xm) ) ). % 65.01/65.15 % 65.01/65.15 %------------------------------------------------------------------------------ % 65.01/65.15 %------------------------------------------- % 65.01/65.15 % Proof found % 65.01/65.15 % SZS status Theorem for theBenchmark % 65.01/65.15 % SZS output start Proof % 65.01/65.15 %ClaNum:253(EqnAxiom:37) % 65.01/65.15 %VarNum:3218(SingletonVarNum:580) % 65.01/65.15 %MaxLitNum:11 % 65.01/65.15 %MaxfuncDepth:2 % 65.01/65.15 %SharedTerms:30 % 65.01/65.15 %goalClause: 52 53 69 70 % 65.01/65.15 %singleGoalClaCount:2 % 65.01/65.15 [38]P1(a1) % 65.01/65.15 [39]P1(a15) % 65.01/65.15 [40]P1(a16) % 65.01/65.15 [41]P1(a17) % 65.01/65.15 [42]P1(a18) % 65.01/65.15 [43]P1(a2) % 65.01/65.15 [44]P2(a18) % 65.01/65.15 [47]~E(a1,a15) % 65.01/65.15 [48]~E(a1,a18) % 65.01/65.15 [49]~E(a18,a15) % 65.01/65.15 [50]~P5(a18,a16) % 65.01/65.15 [51]~P5(a18,a17) % 65.01/65.15 [52]~P3(a18,a16) % 65.01/65.15 [53]~P3(a18,a17) % 65.01/65.15 [45]E(f11(a18,a2),f11(a16,a17)) % 65.01/65.15 [46]P3(a18,f11(a16,a17)) % 65.01/65.15 [64]~P1(x641)+P5(x641,x641) % 65.01/65.15 [56]~P1(x561)+E(f11(a1,x561),a1) % 65.01/65.15 [57]~P1(x571)+E(f11(x571,a1),a1) % 65.01/65.15 [58]~P1(x581)+E(f12(a1,x581),x581) % 65.01/65.15 [59]~P1(x591)+E(f11(a15,x591),x591) % 65.01/65.15 [60]~P1(x601)+E(f12(x601,a1),x601) % 65.01/65.15 [61]~P1(x611)+E(f11(x611,a15),x611) % 65.01/65.15 [69]~P1(x691)+~E(f11(a18,x691),a16) % 65.01/65.15 [70]~P1(x701)+~E(f11(a18,x701),a17) % 65.01/65.15 [71]~P1(x711)+~E(f12(a18,x711),a16) % 65.01/65.15 [72]~P1(x721)+~E(f12(a18,x721),a17) % 65.01/65.15 [54]~P1(x541)+~P2(x541)+~E(x541,a1) % 65.01/65.15 [55]~P1(x551)+~P2(x551)+~E(x551,a15) % 65.01/65.15 [82]~P1(x822)+~P1(x821)+E(f12(x821,x822),f12(x822,x821)) % 65.01/65.15 [83]~P1(x832)+~P1(x831)+E(f11(x831,x832),f11(x832,x831)) % 65.01/65.15 [85]~P1(x852)+~P1(x851)+P1(f12(x851,x852)) % 65.01/65.15 [86]~P1(x862)+~P1(x861)+P1(f11(x861,x862)) % 65.01/65.15 [77]E(a18,a16)+E(a18,a17)+~P5(a16,a18)+~P5(a17,a18) % 65.01/65.15 [66]~P1(x661)+E(x661,a15)+P5(a15,x661)+E(x661,a1) % 65.01/65.15 [73]~P1(x731)+E(x731,a18)+~P3(x731,a18)+E(x731,a15) % 65.01/65.15 [62]~P1(x621)+E(x621,a15)+E(x621,a1)+P1(f3(x621)) % 65.01/65.15 [63]~P1(x631)+E(x631,a15)+E(x631,a1)+P2(f3(x631)) % 65.01/65.15 [74]~P1(x741)+E(x741,a15)+P3(f3(x741),x741)+E(x741,a1) % 65.01/65.15 [75]~E(x752,x751)+~P1(x751)+~P1(x752)+P5(x751,x752) % 65.01/65.15 [84]P5(x842,x841)+~P1(x841)+~P1(x842)+P5(x841,x842) % 65.01/65.15 [78]~P1(x782)+~P1(x781)+E(x781,a1)+~E(f12(x782,x781),a1) % 65.01/65.15 [79]~P1(x792)+~P1(x791)+E(x791,a1)+~E(f12(x791,x792),a1) % 65.01/65.15 [92]~P1(x922)+~P1(x921)+P5(x922,f11(x922,x921))+E(x921,a1) % 65.01/65.15 [99]~P1(x992)+~P1(x991)+~P5(x991,x992)+P1(f5(x991,x992)) % 65.01/65.15 [100]~P1(x1002)+~P1(x1001)+~P3(x1001,x1002)+P1(f6(x1001,x1002)) % 65.01/65.15 [107]~P1(x1071)+~P1(x1072)+~P3(x1071,x1072)+E(f11(x1071,f6(x1071,x1072)),x1072) % 65.01/65.15 [108]~P1(x1082)+~P1(x1081)+~P5(x1081,x1082)+E(f12(x1081,f5(x1081,x1082)),x1082) % 65.01/65.15 [117]~P1(x1173)+~P1(x1172)+~P1(x1171)+E(f12(f12(x1171,x1172),x1173),f12(x1171,f12(x1172,x1173))) % 65.01/65.15 [118]~P1(x1183)+~P1(x1182)+~P1(x1181)+E(f11(f11(x1181,x1182),x1183),f11(x1181,f11(x1182,x1183))) % 65.01/65.15 [126]~P1(x1263)+~P1(x1262)+~P1(x1261)+E(f12(f11(x1261,x1262),f11(x1261,x1263)),f11(x1261,f12(x1262,x1263))) % 65.01/65.15 [127]~P1(x1272)+~P1(x1273)+~P1(x1271)+E(f12(f11(x1271,x1272),f11(x1273,x1272)),f11(f12(x1271,x1273),x1272)) % 65.01/65.15 [65]P2(x651)+~P1(x651)+E(x651,a15)+E(x651,a1)+~E(f4(x651),a15) % 65.01/65.15 [67]P2(x671)+~P1(x671)+E(x671,a15)+~E(f4(x671),x671)+E(x671,a1) % 65.01/65.15 [68]P2(x681)+~P1(x681)+E(x681,a15)+E(x681,a1)+P1(f4(x681)) % 65.01/65.15 [76]P2(x761)+~P1(x761)+E(x761,a15)+P3(f4(x761),x761)+E(x761,a1) % 65.01/65.15 [87]~P1(x871)+E(a18,a16)+E(a18,a17)+~P5(a17,a18)+~E(f12(a16,x871),a18) % 65.01/65.15 [88]~P1(x881)+E(a18,a16)+E(a18,a17)+~P5(a16,a18)+~E(f12(a17,x881),a18) % 65.01/65.15 [90]~P1(x901)+~P1(x902)+~P3(x902,x901)+P5(x902,x901)+E(x901,a1) % 65.01/65.15 [91]P4(x911,x912)+~P1(x912)+~P1(x911)+~P5(x911,x912)+E(x911,x912) % 65.01/65.15 [96]~P1(x962)+~P1(x961)+~P5(x962,x961)+~P5(x961,x962)+E(x961,x962) % 65.01/65.15 [80]~P1(x801)+~P1(x802)+E(x801,a18)+E(x801,a15)+~E(f11(x801,x802),a18) % 65.01/65.15 [81]~P1(x811)+~P1(x812)+E(x811,a1)+E(x812,a1)+~E(f11(x812,x811),a1) % 65.01/65.15 [94]~P1(x941)+~P1(x942)+~P1(x943)+P3(x941,x942)+~E(x942,f11(x941,x943)) % 65.01/65.15 [95]~P1(x952)+~P1(x951)+~P1(x953)+P5(x951,x952)+~E(f12(x951,x953),x952) % 65.01/65.15 [97]~P1(x973)+~P1(x972)+~P5(x973,x972)+P1(x971)+~E(x971,f13(x972,x973)) % 65.01/65.15 [101]~P1(x1012)+~P1(x1011)+~P1(x1013)+E(x1011,x1012)+~E(f12(x1013,x1011),f12(x1013,x1012)) % 65.01/65.15 [102]~P1(x1022)+~P1(x1023)+~P1(x1021)+E(x1021,x1022)+~E(f12(x1021,x1023),f12(x1022,x1023)) % 65.01/65.15 [105]~P1(x1053)+~P1(x1051)+~P5(x1051,x1053)+~E(x1052,f13(x1053,x1051))+E(f12(x1051,x1052),x1053) % 65.01/65.15 [89]~P1(x892)+~P1(x891)+~P2(x892)+~P3(x891,x892)+E(x891,x892)+E(x891,a15) % 65.01/65.15 [93]~P1(x931)+~P1(x932)+E(a18,a16)+E(a18,a17)+~E(f12(a16,x931),a18)+~E(f12(a17,x932),a18) % 65.01/65.15 [109]~P1(x1092)+~P1(x1091)+~P5(x1093,x1092)+~P5(x1091,x1093)+P5(x1091,x1092)+~P1(x1093) % 65.01/65.15 [110]~P1(x1102)+~P1(x1101)+~P3(x1103,x1102)+~P3(x1101,x1103)+P3(x1101,x1102)+~P1(x1103) % 65.01/65.15 [98]~P1(x981)+~P1(x983)+~P3(x981,x983)+P1(x982)+E(x981,a1)+~E(x982,f14(x983,x981)) % 65.01/65.15 [103]~P1(x1032)+~P1(x1031)+~P1(x1033)+E(x1031,x1032)+~E(f11(x1033,x1031),f11(x1033,x1032))+E(x1033,a1) % 65.01/65.15 [104]~P1(x1042)+~P1(x1043)+~P1(x1041)+E(x1041,x1042)+~E(f11(x1041,x1043),f11(x1042,x1043))+E(x1043,a1) % 65.01/65.15 [106]~P1(x1061)+~P1(x1062)+~P3(x1061,x1062)+~E(x1063,f14(x1062,x1061))+E(x1061,a1)+E(x1062,f11(x1061,x1063)) % 65.01/65.15 [111]~P1(x1112)+~P1(x1113)+~P1(x1111)+~P5(x1113,x1112)+~E(f12(x1113,x1111),x1112)+E(x1111,f13(x1112,x1113)) % 65.01/65.15 [119]~P1(x1193)+~P1(x1192)+~P1(x1191)+~P3(x1191,x1193)+~P3(x1191,x1192)+P3(x1191,f12(x1192,x1193)) % 65.01/65.15 [120]~P1(x1202)+~P1(x1201)+~P1(x1203)+~P5(x1201,x1202)+E(x1201,x1202)+P5(f12(x1203,x1201),f12(x1203,x1202)) % 65.01/65.15 [121]~P1(x1212)+~P1(x1213)+~P1(x1211)+~P5(x1211,x1212)+E(x1211,x1212)+P5(f12(x1211,x1213),f12(x1212,x1213)) % 65.01/65.15 [124]~P1(x1242)+~P1(x1241)+~P3(x1241,x1243)+P3(x1241,x1242)+~P1(x1243)+~P3(x1241,f12(x1243,x1242)) % 65.01/65.15 [125]~P1(x1252)+~P1(x1253)+~P1(x1251)+~P3(x1251,x1253)+E(x1251,a1)+E(f14(f11(x1252,x1253),x1251),f11(x1252,f14(x1253,x1251))) % 65.01/65.15 [112]~P1(x1121)+~P1(x1123)+~P1(x1122)+~P3(x1121,x1123)+~E(x1123,f11(x1121,x1122))+E(x1121,a1)+E(x1122,f14(x1123,x1121)) % 65.01/65.15 [122]~P1(x1222)+~P1(x1221)+~P1(x1223)+~P5(x1221,x1222)+E(x1221,x1222)+P5(f11(x1223,x1221),f11(x1223,x1222))+E(x1223,a1) % 65.01/65.15 [123]~P1(x1232)+~P1(x1233)+~P1(x1231)+~P5(x1231,x1232)+E(x1231,x1232)+P5(f11(x1231,x1233),f11(x1232,x1233))+E(x1233,a1) % 65.01/65.15 [129]~P1(x1292)+~P1(x1293)+~P1(x1291)+~P2(x1291)+P3(x1291,x1292)+P3(x1291,x1293)+~P3(x1291,f11(x1292,x1293))+~P4(f12(f12(x1292,x1293),x1291),f12(f12(a16,a17),a18)) % 65.01/65.15 [140]~P1(x1401)+~P1(x1403)+~P1(x1402)+~P2(x1401)+P3(x1401,x1402)+~P3(x1401,f11(x1402,x1403))+P1(f8(x1402,x1403,x1401))+~P4(f12(f12(x1402,x1403),x1401),f12(f12(a16,a17),a18)) % 65.01/65.15 [141]~P1(x1413)+~P1(x1412)+~P1(x1411)+~P2(x1411)+P3(x1411,x1412)+~P3(x1411,f11(x1413,x1412))+P1(f9(x1413,x1412,x1411))+~P4(f12(f12(x1413,x1412),x1411),f12(f12(a16,a17),a18)) % 65.01/65.15 [145]P3(x1451,x1453)+~P1(x1452)+~P1(x1453)+~P1(x1451)+~P2(x1451)+~P3(x1451,f11(x1452,x1453))+E(f11(x1451,f9(x1452,x1453,x1451)),x1452)+~P4(f12(f12(x1452,x1453),x1451),f12(f12(a16,a17),a18)) % 65.01/65.15 [146]P3(x1461,x1462)+~P1(x1462)+~P1(x1461)+~P1(x1463)+~P2(x1461)+~P3(x1461,f11(x1462,x1463))+E(f11(x1461,f8(x1462,x1463,x1461)),x1463)+~P4(f12(f12(x1462,x1463),x1461),f12(f12(a16,a17),a18)) % 65.01/65.15 [171]~P1(x1713)+~P1(x1712)+~P1(x1711)+~P2(x1713)+~P3(x1713,f11(x1711,x1712))+P1(f8(x1711,x1712,x1713))+~P4(f12(f12(x1711,x1712),x1713),f12(f12(a16,a17),a18))+P1(f9(x1711,x1712,x1713)) % 65.01/65.15 [183]~P1(x1831)+~P1(x1833)+~P1(x1832)+~P2(x1831)+~P3(x1831,f11(x1832,x1833))+P1(f8(x1832,x1833,x1831))+~P4(f12(f12(x1832,x1833),x1831),f12(f12(a16,a17),a18))+E(f11(x1831,f9(x1832,x1833,x1831)),x1832) % 65.01/65.15 [184]~P1(x1842)+~P1(x1841)+~P1(x1843)+~P2(x1841)+~P3(x1841,f11(x1842,x1843))+P1(f9(x1842,x1843,x1841))+~P4(f12(f12(x1842,x1843),x1841),f12(f12(a16,a17),a18))+E(f11(x1841,f8(x1842,x1843,x1841)),x1843) % 65.01/65.15 [194]~P1(x1942)+~P1(x1941)+~P1(x1943)+~P2(x1941)+~P3(x1941,f11(x1942,x1943))+E(f11(x1941,f8(x1942,x1943,x1941)),x1943)+~P4(f12(f12(x1942,x1943),x1941),f12(f12(a16,a17),a18))+E(f11(x1941,f9(x1942,x1943,x1941)),x1942) % 65.01/65.15 [128]~P1(x1284)+~P1(x1282)+~P1(x1283)+~P1(x1281)+~P2(x1281)+P3(x1281,x1282)+P3(x1281,x1283)+~E(f11(x1281,x1284),f11(x1282,x1283))+~P4(f12(f12(x1282,x1283),x1281),f12(f12(a16,a17),a18)) % 65.01/65.15 [134]~P1(x1344)+~P1(x1341)+~P1(x1343)+~P1(x1342)+~P2(x1341)+P3(x1341,x1342)+~E(f11(x1342,x1343),f11(x1341,x1344))+P1(f8(x1342,x1343,x1341))+~P4(f12(f12(x1342,x1343),x1341),f12(f12(a16,a17),a18)) % 65.01/65.15 [135]~P1(x1354)+~P1(x1353)+~P1(x1352)+~P1(x1351)+~P2(x1351)+P3(x1351,x1352)+~E(f11(x1351,x1354),f11(x1353,x1352))+P1(f9(x1353,x1352,x1351))+~P4(f12(f12(x1353,x1352),x1351),f12(f12(a16,a17),a18)) % 65.01/65.15 [138]P3(x1381,x1383)+~P1(x1384)+~P1(x1382)+~P1(x1383)+~P1(x1381)+~P2(x1381)+~E(f11(x1381,x1384),f11(x1382,x1383))+E(f11(x1381,f9(x1382,x1383,x1381)),x1382)+~P4(f12(f12(x1382,x1383),x1381),f12(f12(a16,a17),a18)) % 65.01/65.15 [139]P3(x1391,x1392)+~P1(x1394)+~P1(x1392)+~P1(x1391)+~P1(x1393)+~P2(x1391)+~E(f11(x1391,x1394),f11(x1392,x1393))+E(f11(x1391,f8(x1392,x1393,x1391)),x1393)+~P4(f12(f12(x1392,x1393),x1391),f12(f12(a16,a17),a18)) % 65.01/65.15 [160]~P1(x1604)+~P1(x1603)+~P1(x1602)+~P1(x1601)+~P2(x1603)+~E(f11(x1601,x1602),f11(x1603,x1604))+P1(f8(x1601,x1602,x1603))+~P4(f12(f12(x1601,x1602),x1603),f12(f12(a16,a17),a18))+P1(f9(x1601,x1602,x1603)) % 65.01/65.15 [169]~P1(x1694)+~P1(x1691)+~P1(x1693)+~P1(x1692)+~P2(x1691)+~E(f11(x1692,x1693),f11(x1691,x1694))+P1(f8(x1692,x1693,x1691))+~P4(f12(f12(x1692,x1693),x1691),f12(f12(a16,a17),a18))+E(f11(x1691,f9(x1692,x1693,x1691)),x1692) % 65.01/65.15 [170]~P1(x1704)+~P1(x1702)+~P1(x1701)+~P1(x1703)+~P2(x1701)+~E(f11(x1701,x1704),f11(x1702,x1703))+P1(f9(x1702,x1703,x1701))+~P4(f12(f12(x1702,x1703),x1701),f12(f12(a16,a17),a18))+E(f11(x1701,f8(x1702,x1703,x1701)),x1703) % 65.01/65.15 [178]~P1(x1784)+~P1(x1782)+~P1(x1781)+~P1(x1783)+~P2(x1781)+~E(f11(x1781,x1784),f11(x1782,x1783))+E(f11(x1781,f8(x1782,x1783,x1781)),x1783)+~P4(f12(f12(x1782,x1783),x1781),f12(f12(a16,a17),a18))+E(f11(x1781,f9(x1782,x1783,x1781)),x1782) % 65.01/65.15 [132]~P1(x1322)+~P1(x1323)+~P1(x1321)+P3(x1321,x1322)+P3(x1321,x1323)+E(x1321,a15)+~P3(x1321,f11(x1322,x1323))+E(x1321,a1)+~E(f7(x1322,x1323,x1321),a15)+~P4(f12(f12(x1322,x1323),x1321),f12(f12(a16,a17),a18)) % 65.01/65.15 [133]~P1(x1332)+~P1(x1333)+~P1(x1331)+P3(x1331,x1332)+P3(x1331,x1333)+E(x1331,a15)+~E(f7(x1332,x1333,x1331),x1331)+~P3(x1331,f11(x1332,x1333))+E(x1331,a1)+~P4(f12(f12(x1332,x1333),x1331),f12(f12(a16,a17),a18)) % 65.01/65.15 [143]~P1(x1432)+~P1(x1433)+~P1(x1431)+P3(x1431,x1432)+P3(x1431,x1433)+E(x1431,a15)+~P3(x1431,f11(x1432,x1433))+E(x1431,a1)+P1(f7(x1432,x1433,x1431))+~P4(f12(f12(x1432,x1433),x1431),f12(f12(a16,a17),a18)) % 65.01/65.15 [144]~P1(x1442)+~P1(x1443)+~P1(x1441)+P3(x1441,x1442)+P3(x1441,x1443)+E(x1441,a15)+~P3(x1441,f11(x1442,x1443))+E(x1441,a1)+P1(f10(x1442,x1443,x1441))+~P4(f12(f12(x1442,x1443),x1441),f12(f12(a16,a17),a18)) % 65.01/65.15 [147]~P1(x1472)+~P1(x1473)+~P1(x1471)+P3(x1471,x1472)+P3(x1471,x1473)+E(x1471,a15)+P3(f7(x1472,x1473,x1471),x1471)+~P3(x1471,f11(x1472,x1473))+E(x1471,a1)+~P4(f12(f12(x1472,x1473),x1471),f12(f12(a16,a17),a18)) % 65.01/65.15 [156]~P1(x1561)+~P1(x1563)+~P1(x1562)+P3(x1561,x1562)+E(x1561,a15)+~P3(x1561,f11(x1562,x1563))+E(x1561,a1)+~E(f7(x1562,x1563,x1561),a15)+~P4(f12(f12(x1562,x1563),x1561),f12(f12(a16,a17),a18))+P1(f8(x1562,x1563,x1561)) % 65.01/65.15 [157]~P1(x1573)+~P1(x1572)+~P1(x1571)+P3(x1571,x1572)+E(x1571,a15)+~P3(x1571,f11(x1573,x1572))+E(x1571,a1)+~E(f7(x1573,x1572,x1571),a15)+~P4(f12(f12(x1573,x1572),x1571),f12(f12(a16,a17),a18))+P1(f9(x1573,x1572,x1571)) % 65.01/65.15 [158]~P1(x1581)+~P1(x1583)+~P1(x1582)+P3(x1581,x1582)+E(x1581,a15)+~E(f7(x1582,x1583,x1581),x1581)+~P3(x1581,f11(x1582,x1583))+E(x1581,a1)+~P4(f12(f12(x1582,x1583),x1581),f12(f12(a16,a17),a18))+P1(f8(x1582,x1583,x1581)) % 65.01/65.15 [159]~P1(x1593)+~P1(x1592)+~P1(x1591)+P3(x1591,x1592)+E(x1591,a15)+~E(f7(x1593,x1592,x1591),x1591)+~P3(x1591,f11(x1593,x1592))+E(x1591,a1)+~P4(f12(f12(x1593,x1592),x1591),f12(f12(a16,a17),a18))+P1(f9(x1593,x1592,x1591)) % 65.01/65.15 [161]P3(x1611,x1612)+~P1(x1612)+~P1(x1611)+~P1(x1613)+E(x1611,a15)+~P3(x1611,f11(x1612,x1613))+E(x1611,a1)+~E(f7(x1612,x1613,x1611),a15)+~P4(f12(f12(x1612,x1613),x1611),f12(f12(a16,a17),a18))+E(f11(x1611,f8(x1612,x1613,x1611)),x1613) % 65.01/65.15 [162]P3(x1621,x1623)+~P1(x1622)+~P1(x1623)+~P1(x1621)+E(x1621,a15)+~P3(x1621,f11(x1622,x1623))+E(x1621,a1)+~E(f7(x1622,x1623,x1621),a15)+~P4(f12(f12(x1622,x1623),x1621),f12(f12(a16,a17),a18))+E(f11(x1621,f9(x1622,x1623,x1621)),x1622) % 65.01/65.15 [163]P3(x1631,x1632)+~P1(x1632)+~P1(x1631)+~P1(x1633)+E(x1631,a15)+~E(f7(x1632,x1633,x1631),x1631)+~P3(x1631,f11(x1632,x1633))+E(x1631,a1)+~P4(f12(f12(x1632,x1633),x1631),f12(f12(a16,a17),a18))+E(f11(x1631,f8(x1632,x1633,x1631)),x1633) % 65.01/65.15 [164]P3(x1641,x1643)+~P1(x1642)+~P1(x1643)+~P1(x1641)+E(x1641,a15)+~E(f7(x1642,x1643,x1641),x1641)+~P3(x1641,f11(x1642,x1643))+E(x1641,a1)+~P4(f12(f12(x1642,x1643),x1641),f12(f12(a16,a17),a18))+E(f11(x1641,f9(x1642,x1643,x1641)),x1642) % 65.01/65.15 [179]~P1(x1791)+~P1(x1793)+~P1(x1792)+P3(x1791,x1792)+E(x1791,a15)+~P3(x1791,f11(x1792,x1793))+E(x1791,a1)+P1(f8(x1792,x1793,x1791))+~P4(f12(f12(x1792,x1793),x1791),f12(f12(a16,a17),a18))+P1(f7(x1792,x1793,x1791)) % 65.01/65.15 [180]~P1(x1801)+~P1(x1803)+~P1(x1802)+P3(x1801,x1802)+E(x1801,a15)+~P3(x1801,f11(x1802,x1803))+E(x1801,a1)+P1(f8(x1802,x1803,x1801))+~P4(f12(f12(x1802,x1803),x1801),f12(f12(a16,a17),a18))+P1(f10(x1802,x1803,x1801)) % 65.01/65.15 [181]~P1(x1813)+~P1(x1812)+~P1(x1811)+P3(x1811,x1812)+E(x1811,a15)+~P3(x1811,f11(x1813,x1812))+E(x1811,a1)+P1(f9(x1813,x1812,x1811))+~P4(f12(f12(x1813,x1812),x1811),f12(f12(a16,a17),a18))+P1(f7(x1813,x1812,x1811)) % 65.01/65.16 [182]~P1(x1823)+~P1(x1822)+~P1(x1821)+P3(x1821,x1822)+E(x1821,a15)+~P3(x1821,f11(x1823,x1822))+E(x1821,a1)+P1(f9(x1823,x1822,x1821))+~P4(f12(f12(x1823,x1822),x1821),f12(f12(a16,a17),a18))+P1(f10(x1823,x1822,x1821)) % 65.01/65.16 [188]~P1(x1881)+~P1(x1883)+~P1(x1882)+P3(x1881,x1882)+E(x1881,a15)+P3(f7(x1882,x1883,x1881),x1881)+~P3(x1881,f11(x1882,x1883))+E(x1881,a1)+~P4(f12(f12(x1882,x1883),x1881),f12(f12(a16,a17),a18))+P1(f8(x1882,x1883,x1881)) % 65.01/65.16 [189]~P1(x1893)+~P1(x1892)+~P1(x1891)+P3(x1891,x1892)+E(x1891,a15)+P3(f7(x1893,x1892,x1891),x1891)+~P3(x1891,f11(x1893,x1892))+E(x1891,a1)+~P4(f12(f12(x1893,x1892),x1891),f12(f12(a16,a17),a18))+P1(f9(x1893,x1892,x1891)) % 65.01/65.16 [190]P3(x1901,x1902)+~P1(x1902)+~P1(x1901)+~P1(x1903)+E(x1901,a15)+~P3(x1901,f11(x1902,x1903))+E(x1901,a1)+P1(f7(x1902,x1903,x1901))+~P4(f12(f12(x1902,x1903),x1901),f12(f12(a16,a17),a18))+E(f11(x1901,f8(x1902,x1903,x1901)),x1903) % 65.01/65.16 [191]P3(x1911,x1912)+~P1(x1912)+~P1(x1911)+~P1(x1913)+E(x1911,a15)+~P3(x1911,f11(x1912,x1913))+E(x1911,a1)+P1(f10(x1912,x1913,x1911))+~P4(f12(f12(x1912,x1913),x1911),f12(f12(a16,a17),a18))+E(f11(x1911,f8(x1912,x1913,x1911)),x1913) % 65.01/65.16 [192]P3(x1921,x1923)+~P1(x1922)+~P1(x1923)+~P1(x1921)+E(x1921,a15)+~P3(x1921,f11(x1922,x1923))+E(x1921,a1)+P1(f7(x1922,x1923,x1921))+~P4(f12(f12(x1922,x1923),x1921),f12(f12(a16,a17),a18))+E(f11(x1921,f9(x1922,x1923,x1921)),x1922) % 65.01/65.16 [193]P3(x1931,x1933)+~P1(x1932)+~P1(x1933)+~P1(x1931)+E(x1931,a15)+~P3(x1931,f11(x1932,x1933))+E(x1931,a1)+P1(f10(x1932,x1933,x1931))+~P4(f12(f12(x1932,x1933),x1931),f12(f12(a16,a17),a18))+E(f11(x1931,f9(x1932,x1933,x1931)),x1932) % 65.01/65.16 [195]P3(x1951,x1952)+~P1(x1952)+~P1(x1951)+~P1(x1953)+E(x1951,a15)+P3(f7(x1952,x1953,x1951),x1951)+~P3(x1951,f11(x1952,x1953))+E(x1951,a1)+~P4(f12(f12(x1952,x1953),x1951),f12(f12(a16,a17),a18))+E(f11(x1951,f8(x1952,x1953,x1951)),x1953) % 65.01/65.16 [196]P3(x1961,x1963)+~P1(x1962)+~P1(x1963)+~P1(x1961)+E(x1961,a15)+P3(f7(x1962,x1963,x1961),x1961)+~P3(x1961,f11(x1962,x1963))+E(x1961,a1)+~P4(f12(f12(x1962,x1963),x1961),f12(f12(a16,a17),a18))+E(f11(x1961,f9(x1962,x1963,x1961)),x1962) % 65.01/65.16 [197]P3(x1971,x1972)+P3(x1971,x1973)+~P1(x1972)+~P1(x1973)+~P1(x1971)+E(x1971,a15)+~P3(x1971,f11(x1972,x1973))+E(x1971,a1)+~P4(f12(f12(x1972,x1973),x1971),f12(f12(a16,a17),a18))+E(f11(f7(x1972,x1973,x1971),f10(x1972,x1973,x1971)),x1971) % 65.01/65.16 [204]~P1(x2041)+~P1(x2043)+~P1(x2042)+E(x2041,a15)+~P3(x2041,f11(x2042,x2043))+E(x2041,a1)+P1(f8(x2042,x2043,x2041))+~E(f7(x2042,x2043,x2041),a15)+~P4(f12(f12(x2042,x2043),x2041),f12(f12(a16,a17),a18))+P1(f9(x2042,x2043,x2041)) % 65.01/65.16 [205]~P1(x2051)+~P1(x2053)+~P1(x2052)+E(x2051,a15)+~E(f7(x2052,x2053,x2051),x2051)+~P3(x2051,f11(x2052,x2053))+E(x2051,a1)+P1(f8(x2052,x2053,x2051))+~P4(f12(f12(x2052,x2053),x2051),f12(f12(a16,a17),a18))+P1(f9(x2052,x2053,x2051)) % 65.01/65.16 [208]~P1(x2081)+~P1(x2083)+~P1(x2082)+E(x2081,a15)+~P3(x2081,f11(x2082,x2083))+E(x2081,a1)+P1(f8(x2082,x2083,x2081))+~E(f7(x2082,x2083,x2081),a15)+~P4(f12(f12(x2082,x2083),x2081),f12(f12(a16,a17),a18))+E(f11(x2081,f9(x2082,x2083,x2081)),x2082) % 65.01/65.16 [209]~P1(x2092)+~P1(x2091)+~P1(x2093)+E(x2091,a15)+~P3(x2091,f11(x2092,x2093))+E(x2091,a1)+P1(f9(x2092,x2093,x2091))+~E(f7(x2092,x2093,x2091),a15)+~P4(f12(f12(x2092,x2093),x2091),f12(f12(a16,a17),a18))+E(f11(x2091,f8(x2092,x2093,x2091)),x2093) % 65.01/65.16 [210]~P1(x2101)+~P1(x2103)+~P1(x2102)+E(x2101,a15)+~E(f7(x2102,x2103,x2101),x2101)+~P3(x2101,f11(x2102,x2103))+E(x2101,a1)+P1(f8(x2102,x2103,x2101))+~P4(f12(f12(x2102,x2103),x2101),f12(f12(a16,a17),a18))+E(f11(x2101,f9(x2102,x2103,x2101)),x2102) % 65.01/65.16 [211]~P1(x2112)+~P1(x2111)+~P1(x2113)+E(x2111,a15)+~E(f7(x2112,x2113,x2111),x2111)+~P3(x2111,f11(x2112,x2113))+E(x2111,a1)+P1(f9(x2112,x2113,x2111))+~P4(f12(f12(x2112,x2113),x2111),f12(f12(a16,a17),a18))+E(f11(x2111,f8(x2112,x2113,x2111)),x2113) % 65.01/65.16 [214]~P1(x2142)+~P1(x2141)+~P1(x2143)+E(x2141,a15)+~P3(x2141,f11(x2142,x2143))+E(x2141,a1)+E(f11(x2141,f8(x2142,x2143,x2141)),x2143)+~E(f7(x2142,x2143,x2141),a15)+~P4(f12(f12(x2142,x2143),x2141),f12(f12(a16,a17),a18))+E(f11(x2141,f9(x2142,x2143,x2141)),x2142) % 65.01/65.16 [215]~P1(x2152)+~P1(x2151)+~P1(x2153)+E(x2151,a15)+~E(f7(x2152,x2153,x2151),x2151)+~P3(x2151,f11(x2152,x2153))+E(x2151,a1)+E(f11(x2151,f8(x2152,x2153,x2151)),x2153)+~P4(f12(f12(x2152,x2153),x2151),f12(f12(a16,a17),a18))+E(f11(x2151,f9(x2152,x2153,x2151)),x2152) % 65.01/65.16 [221]~P1(x2211)+~P1(x2213)+~P1(x2212)+E(x2211,a15)+~P3(x2211,f11(x2212,x2213))+E(x2211,a1)+P1(f9(x2212,x2213,x2211))+P1(f8(x2212,x2213,x2211))+~P4(f12(f12(x2212,x2213),x2211),f12(f12(a16,a17),a18))+P1(f7(x2212,x2213,x2211)) % 65.01/65.16 [222]~P1(x2221)+~P1(x2223)+~P1(x2222)+E(x2221,a15)+~P3(x2221,f11(x2222,x2223))+E(x2221,a1)+P1(f9(x2222,x2223,x2221))+P1(f8(x2222,x2223,x2221))+~P4(f12(f12(x2222,x2223),x2221),f12(f12(a16,a17),a18))+P1(f10(x2222,x2223,x2221)) % 65.01/65.16 [229]~P1(x2291)+~P1(x2293)+~P1(x2292)+E(x2291,a15)+P3(f7(x2292,x2293,x2291),x2291)+~P3(x2291,f11(x2292,x2293))+E(x2291,a1)+P1(f8(x2292,x2293,x2291))+~P4(f12(f12(x2292,x2293),x2291),f12(f12(a16,a17),a18))+P1(f9(x2292,x2293,x2291)) % 65.01/65.16 [230]~P1(x2301)+~P1(x2303)+~P1(x2302)+E(x2301,a15)+~P3(x2301,f11(x2302,x2303))+E(x2301,a1)+P1(f7(x2302,x2303,x2301))+P1(f8(x2302,x2303,x2301))+~P4(f12(f12(x2302,x2303),x2301),f12(f12(a16,a17),a18))+E(f11(x2301,f9(x2302,x2303,x2301)),x2302) % 65.01/65.16 [231]~P1(x2311)+~P1(x2313)+~P1(x2312)+E(x2311,a15)+~P3(x2311,f11(x2312,x2313))+E(x2311,a1)+P1(f10(x2312,x2313,x2311))+P1(f8(x2312,x2313,x2311))+~P4(f12(f12(x2312,x2313),x2311),f12(f12(a16,a17),a18))+E(f11(x2311,f9(x2312,x2313,x2311)),x2312) % 65.01/65.16 [232]~P1(x2322)+~P1(x2321)+~P1(x2323)+E(x2321,a15)+~P3(x2321,f11(x2322,x2323))+E(x2321,a1)+P1(f7(x2322,x2323,x2321))+P1(f9(x2322,x2323,x2321))+~P4(f12(f12(x2322,x2323),x2321),f12(f12(a16,a17),a18))+E(f11(x2321,f8(x2322,x2323,x2321)),x2323) % 65.01/65.16 [233]~P1(x2332)+~P1(x2331)+~P1(x2333)+E(x2331,a15)+~P3(x2331,f11(x2332,x2333))+E(x2331,a1)+P1(f10(x2332,x2333,x2331))+P1(f9(x2332,x2333,x2331))+~P4(f12(f12(x2332,x2333),x2331),f12(f12(a16,a17),a18))+E(f11(x2331,f8(x2332,x2333,x2331)),x2333) % 65.01/65.16 [237]~P1(x2371)+~P1(x2373)+~P1(x2372)+E(x2371,a15)+P3(f7(x2372,x2373,x2371),x2371)+~P3(x2371,f11(x2372,x2373))+E(x2371,a1)+P1(f8(x2372,x2373,x2371))+~P4(f12(f12(x2372,x2373),x2371),f12(f12(a16,a17),a18))+E(f11(x2371,f9(x2372,x2373,x2371)),x2372) % 65.01/65.16 [238]~P1(x2382)+~P1(x2381)+~P1(x2383)+E(x2381,a15)+P3(f7(x2382,x2383,x2381),x2381)+~P3(x2381,f11(x2382,x2383))+E(x2381,a1)+P1(f9(x2382,x2383,x2381))+~P4(f12(f12(x2382,x2383),x2381),f12(f12(a16,a17),a18))+E(f11(x2381,f8(x2382,x2383,x2381)),x2383) % 65.01/65.16 [239]P3(x2391,x2392)+~P1(x2391)+~P1(x2393)+~P1(x2392)+E(x2391,a15)+~P3(x2391,f11(x2392,x2393))+E(x2391,a1)+P1(f8(x2392,x2393,x2391))+~P4(f12(f12(x2392,x2393),x2391),f12(f12(a16,a17),a18))+E(f11(f7(x2392,x2393,x2391),f10(x2392,x2393,x2391)),x2391) % 65.01/65.16 [240]P3(x2401,x2403)+~P1(x2402)+~P1(x2403)+~P1(x2401)+E(x2401,a15)+~P3(x2401,f11(x2402,x2403))+E(x2401,a1)+P1(f9(x2402,x2403,x2401))+~P4(f12(f12(x2402,x2403),x2401),f12(f12(a16,a17),a18))+E(f11(f7(x2402,x2403,x2401),f10(x2402,x2403,x2401)),x2401) % 65.01/65.16 [241]~P1(x2412)+~P1(x2411)+~P1(x2413)+E(x2411,a15)+~P3(x2411,f11(x2412,x2413))+E(x2411,a1)+E(f11(x2411,f8(x2412,x2413,x2411)),x2413)+P1(f7(x2412,x2413,x2411))+~P4(f12(f12(x2412,x2413),x2411),f12(f12(a16,a17),a18))+E(f11(x2411,f9(x2412,x2413,x2411)),x2412) % 65.01/65.16 [242]~P1(x2422)+~P1(x2421)+~P1(x2423)+E(x2421,a15)+~P3(x2421,f11(x2422,x2423))+E(x2421,a1)+E(f11(x2421,f8(x2422,x2423,x2421)),x2423)+P1(f10(x2422,x2423,x2421))+~P4(f12(f12(x2422,x2423),x2421),f12(f12(a16,a17),a18))+E(f11(x2421,f9(x2422,x2423,x2421)),x2422) % 65.01/65.16 [243]~P1(x2432)+~P1(x2431)+~P1(x2433)+E(x2431,a15)+P3(f7(x2432,x2433,x2431),x2431)+~P3(x2431,f11(x2432,x2433))+E(x2431,a1)+E(f11(x2431,f8(x2432,x2433,x2431)),x2433)+~P4(f12(f12(x2432,x2433),x2431),f12(f12(a16,a17),a18))+E(f11(x2431,f9(x2432,x2433,x2431)),x2432) % 65.01/65.16 [244]P3(x2441,x2442)+~P1(x2442)+~P1(x2441)+~P1(x2443)+E(x2441,a15)+~P3(x2441,f11(x2442,x2443))+E(x2441,a1)+E(f11(f7(x2442,x2443,x2441),f10(x2442,x2443,x2441)),x2441)+~P4(f12(f12(x2442,x2443),x2441),f12(f12(a16,a17),a18))+E(f11(x2441,f8(x2442,x2443,x2441)),x2443) % 65.01/65.16 [245]P3(x2451,x2453)+~P1(x2452)+~P1(x2453)+~P1(x2451)+E(x2451,a15)+~P3(x2451,f11(x2452,x2453))+E(x2451,a1)+E(f11(f7(x2452,x2453,x2451),f10(x2452,x2453,x2451)),x2451)+~P4(f12(f12(x2452,x2453),x2451),f12(f12(a16,a17),a18))+E(f11(x2451,f9(x2452,x2453,x2451)),x2452) % 65.01/65.16 [249]~P1(x2491)+~P1(x2493)+~P1(x2492)+E(x2491,a15)+~P3(x2491,f11(x2492,x2493))+E(x2491,a1)+P1(f9(x2492,x2493,x2491))+P1(f8(x2492,x2493,x2491))+~P4(f12(f12(x2492,x2493),x2491),f12(f12(a16,a17),a18))+E(f11(f7(x2492,x2493,x2491),f10(x2492,x2493,x2491)),x2491) % 65.01/65.16 [251]~P1(x2511)+~P1(x2513)+~P1(x2512)+E(x2511,a15)+~P3(x2511,f11(x2512,x2513))+E(x2511,a1)+E(f11(f7(x2512,x2513,x2511),f10(x2512,x2513,x2511)),x2511)+P1(f8(x2512,x2513,x2511))+~P4(f12(f12(x2512,x2513),x2511),f12(f12(a16,a17),a18))+E(f11(x2511,f9(x2512,x2513,x2511)),x2512) % 65.01/65.16 [252]~P1(x2522)+~P1(x2521)+~P1(x2523)+E(x2521,a15)+~P3(x2521,f11(x2522,x2523))+E(x2521,a1)+E(f11(f7(x2522,x2523,x2521),f10(x2522,x2523,x2521)),x2521)+P1(f9(x2522,x2523,x2521))+~P4(f12(f12(x2522,x2523),x2521),f12(f12(a16,a17),a18))+E(f11(x2521,f8(x2522,x2523,x2521)),x2523) % 65.01/65.16 [253]~P1(x2532)+~P1(x2531)+~P1(x2533)+E(x2531,a15)+~P3(x2531,f11(x2532,x2533))+E(x2531,a1)+E(f11(x2531,f8(x2532,x2533,x2531)),x2533)+E(f11(f7(x2532,x2533,x2531),f10(x2532,x2533,x2531)),x2531)+~P4(f12(f12(x2532,x2533),x2531),f12(f12(a16,a17),a18))+E(f11(x2531,f9(x2532,x2533,x2531)),x2532) % 65.01/65.16 [130]~P1(x1304)+~P1(x1302)+~P1(x1303)+~P1(x1301)+P3(x1301,x1302)+P3(x1301,x1303)+E(x1301,a15)+E(x1301,a1)+~E(f11(x1301,x1304),f11(x1302,x1303))+~E(f7(x1302,x1303,x1301),a15)+~P4(f12(f12(x1302,x1303),x1301),f12(f12(a16,a17),a18)) % 65.01/65.16 [131]~P1(x1314)+~P1(x1312)+~P1(x1313)+~P1(x1311)+P3(x1311,x1312)+P3(x1311,x1313)+E(x1311,a15)+~E(f7(x1312,x1313,x1311),x1311)+E(x1311,a1)+~E(f11(x1311,x1314),f11(x1312,x1313))+~P4(f12(f12(x1312,x1313),x1311),f12(f12(a16,a17),a18)) % 65.01/65.16 [136]~P1(x1364)+~P1(x1362)+~P1(x1363)+~P1(x1361)+P3(x1361,x1362)+P3(x1361,x1363)+E(x1361,a15)+E(x1361,a1)+~E(f11(x1361,x1364),f11(x1362,x1363))+P1(f7(x1362,x1363,x1361))+~P4(f12(f12(x1362,x1363),x1361),f12(f12(a16,a17),a18)) % 65.01/65.16 [137]~P1(x1374)+~P1(x1372)+~P1(x1373)+~P1(x1371)+P3(x1371,x1372)+P3(x1371,x1373)+E(x1371,a15)+E(x1371,a1)+~E(f11(x1371,x1374),f11(x1372,x1373))+P1(f10(x1372,x1373,x1371))+~P4(f12(f12(x1372,x1373),x1371),f12(f12(a16,a17),a18)) % 65.01/65.16 [142]~P1(x1424)+~P1(x1422)+~P1(x1423)+~P1(x1421)+P3(x1421,x1422)+P3(x1421,x1423)+E(x1421,a15)+P3(f7(x1422,x1423,x1421),x1421)+E(x1421,a1)+~E(f11(x1421,x1424),f11(x1422,x1423))+~P4(f12(f12(x1422,x1423),x1421),f12(f12(a16,a17),a18)) % 65.01/65.16 [148]~P1(x1484)+~P1(x1481)+~P1(x1483)+~P1(x1482)+P3(x1481,x1482)+E(x1481,a15)+E(x1481,a1)+~E(f11(x1482,x1483),f11(x1481,x1484))+~E(f7(x1482,x1483,x1481),a15)+P1(f8(x1482,x1483,x1481))+~P4(f12(f12(x1482,x1483),x1481),f12(f12(a16,a17),a18)) % 65.01/65.16 [149]~P1(x1494)+~P1(x1493)+~P1(x1492)+~P1(x1491)+P3(x1491,x1492)+E(x1491,a15)+E(x1491,a1)+~E(f11(x1491,x1494),f11(x1493,x1492))+~E(f7(x1493,x1492,x1491),a15)+P1(f9(x1493,x1492,x1491))+~P4(f12(f12(x1493,x1492),x1491),f12(f12(a16,a17),a18)) % 65.01/65.16 [150]~P1(x1504)+~P1(x1501)+~P1(x1503)+~P1(x1502)+P3(x1501,x1502)+E(x1501,a15)+~E(f7(x1502,x1503,x1501),x1501)+E(x1501,a1)+~E(f11(x1502,x1503),f11(x1501,x1504))+~P4(f12(f12(x1502,x1503),x1501),f12(f12(a16,a17),a18))+P1(f8(x1502,x1503,x1501)) % 65.01/65.16 [151]~P1(x1514)+~P1(x1513)+~P1(x1512)+~P1(x1511)+P3(x1511,x1512)+E(x1511,a15)+~E(f7(x1513,x1512,x1511),x1511)+E(x1511,a1)+~E(f11(x1511,x1514),f11(x1513,x1512))+~P4(f12(f12(x1513,x1512),x1511),f12(f12(a16,a17),a18))+P1(f9(x1513,x1512,x1511)) % 65.01/65.16 [152]P3(x1521,x1522)+~P1(x1524)+~P1(x1522)+~P1(x1521)+~P1(x1523)+E(x1521,a15)+E(x1521,a1)+~E(f11(x1521,x1524),f11(x1522,x1523))+~E(f7(x1522,x1523,x1521),a15)+~P4(f12(f12(x1522,x1523),x1521),f12(f12(a16,a17),a18))+E(f11(x1521,f8(x1522,x1523,x1521)),x1523) % 65.01/65.16 [153]P3(x1531,x1533)+~P1(x1534)+~P1(x1532)+~P1(x1533)+~P1(x1531)+E(x1531,a15)+E(x1531,a1)+~E(f11(x1531,x1534),f11(x1532,x1533))+~E(f7(x1532,x1533,x1531),a15)+~P4(f12(f12(x1532,x1533),x1531),f12(f12(a16,a17),a18))+E(f11(x1531,f9(x1532,x1533,x1531)),x1532) % 65.01/65.16 [154]P3(x1541,x1542)+~P1(x1544)+~P1(x1542)+~P1(x1541)+~P1(x1543)+E(x1541,a15)+~E(f7(x1542,x1543,x1541),x1541)+E(x1541,a1)+~E(f11(x1541,x1544),f11(x1542,x1543))+~P4(f12(f12(x1542,x1543),x1541),f12(f12(a16,a17),a18))+E(f11(x1541,f8(x1542,x1543,x1541)),x1543) % 65.01/65.16 [155]P3(x1551,x1553)+~P1(x1554)+~P1(x1552)+~P1(x1553)+~P1(x1551)+E(x1551,a15)+~E(f7(x1552,x1553,x1551),x1551)+E(x1551,a1)+~E(f11(x1551,x1554),f11(x1552,x1553))+~P4(f12(f12(x1552,x1553),x1551),f12(f12(a16,a17),a18))+E(f11(x1551,f9(x1552,x1553,x1551)),x1552) % 65.01/65.16 [165]~P1(x1654)+~P1(x1651)+~P1(x1653)+~P1(x1652)+P3(x1651,x1652)+E(x1651,a15)+E(x1651,a1)+~E(f11(x1652,x1653),f11(x1651,x1654))+P1(f8(x1652,x1653,x1651))+~P4(f12(f12(x1652,x1653),x1651),f12(f12(a16,a17),a18))+P1(f7(x1652,x1653,x1651)) % 65.01/65.16 [166]~P1(x1664)+~P1(x1661)+~P1(x1663)+~P1(x1662)+P3(x1661,x1662)+E(x1661,a15)+E(x1661,a1)+~E(f11(x1662,x1663),f11(x1661,x1664))+P1(f8(x1662,x1663,x1661))+~P4(f12(f12(x1662,x1663),x1661),f12(f12(a16,a17),a18))+P1(f10(x1662,x1663,x1661)) % 65.01/65.16 [167]~P1(x1674)+~P1(x1673)+~P1(x1672)+~P1(x1671)+P3(x1671,x1672)+E(x1671,a15)+E(x1671,a1)+~E(f11(x1671,x1674),f11(x1673,x1672))+P1(f9(x1673,x1672,x1671))+~P4(f12(f12(x1673,x1672),x1671),f12(f12(a16,a17),a18))+P1(f7(x1673,x1672,x1671)) % 65.01/65.16 [168]~P1(x1684)+~P1(x1683)+~P1(x1682)+~P1(x1681)+P3(x1681,x1682)+E(x1681,a15)+E(x1681,a1)+~E(f11(x1681,x1684),f11(x1683,x1682))+P1(f9(x1683,x1682,x1681))+~P4(f12(f12(x1683,x1682),x1681),f12(f12(a16,a17),a18))+P1(f10(x1683,x1682,x1681)) % 65.01/65.16 [172]~P1(x1724)+~P1(x1721)+~P1(x1723)+~P1(x1722)+P3(x1721,x1722)+E(x1721,a15)+P3(f7(x1722,x1723,x1721),x1721)+E(x1721,a1)+~E(f11(x1722,x1723),f11(x1721,x1724))+~P4(f12(f12(x1722,x1723),x1721),f12(f12(a16,a17),a18))+P1(f8(x1722,x1723,x1721)) % 65.01/65.16 [173]~P1(x1734)+~P1(x1733)+~P1(x1732)+~P1(x1731)+P3(x1731,x1732)+E(x1731,a15)+P3(f7(x1733,x1732,x1731),x1731)+E(x1731,a1)+~E(f11(x1731,x1734),f11(x1733,x1732))+~P4(f12(f12(x1733,x1732),x1731),f12(f12(a16,a17),a18))+P1(f9(x1733,x1732,x1731)) % 65.01/65.16 [174]P3(x1741,x1742)+~P1(x1744)+~P1(x1742)+~P1(x1741)+~P1(x1743)+E(x1741,a15)+E(x1741,a1)+~E(f11(x1741,x1744),f11(x1742,x1743))+P1(f7(x1742,x1743,x1741))+~P4(f12(f12(x1742,x1743),x1741),f12(f12(a16,a17),a18))+E(f11(x1741,f8(x1742,x1743,x1741)),x1743) % 65.01/65.16 [175]P3(x1751,x1752)+~P1(x1754)+~P1(x1752)+~P1(x1751)+~P1(x1753)+E(x1751,a15)+E(x1751,a1)+~E(f11(x1751,x1754),f11(x1752,x1753))+P1(f10(x1752,x1753,x1751))+~P4(f12(f12(x1752,x1753),x1751),f12(f12(a16,a17),a18))+E(f11(x1751,f8(x1752,x1753,x1751)),x1753) % 65.01/65.16 [176]P3(x1761,x1763)+~P1(x1764)+~P1(x1762)+~P1(x1763)+~P1(x1761)+E(x1761,a15)+E(x1761,a1)+~E(f11(x1761,x1764),f11(x1762,x1763))+P1(f7(x1762,x1763,x1761))+~P4(f12(f12(x1762,x1763),x1761),f12(f12(a16,a17),a18))+E(f11(x1761,f9(x1762,x1763,x1761)),x1762) % 65.01/65.16 [177]P3(x1771,x1773)+~P1(x1774)+~P1(x1772)+~P1(x1773)+~P1(x1771)+E(x1771,a15)+E(x1771,a1)+~E(f11(x1771,x1774),f11(x1772,x1773))+P1(f10(x1772,x1773,x1771))+~P4(f12(f12(x1772,x1773),x1771),f12(f12(a16,a17),a18))+E(f11(x1771,f9(x1772,x1773,x1771)),x1772) % 65.01/65.16 [185]P3(x1851,x1852)+~P1(x1854)+~P1(x1852)+~P1(x1851)+~P1(x1853)+E(x1851,a15)+P3(f7(x1852,x1853,x1851),x1851)+E(x1851,a1)+~E(f11(x1851,x1854),f11(x1852,x1853))+~P4(f12(f12(x1852,x1853),x1851),f12(f12(a16,a17),a18))+E(f11(x1851,f8(x1852,x1853,x1851)),x1853) % 65.01/65.16 [186]P3(x1861,x1863)+~P1(x1864)+~P1(x1862)+~P1(x1863)+~P1(x1861)+E(x1861,a15)+P3(f7(x1862,x1863,x1861),x1861)+E(x1861,a1)+~E(f11(x1861,x1864),f11(x1862,x1863))+~P4(f12(f12(x1862,x1863),x1861),f12(f12(a16,a17),a18))+E(f11(x1861,f9(x1862,x1863,x1861)),x1862) % 65.01/65.16 [187]P3(x1871,x1872)+P3(x1871,x1873)+~P1(x1874)+~P1(x1872)+~P1(x1873)+~P1(x1871)+E(x1871,a15)+E(x1871,a1)+~E(f11(x1871,x1874),f11(x1872,x1873))+~P4(f12(f12(x1872,x1873),x1871),f12(f12(a16,a17),a18))+E(f11(f7(x1872,x1873,x1871),f10(x1872,x1873,x1871)),x1871) % 65.01/65.16 [198]~P1(x1984)+~P1(x1981)+~P1(x1983)+~P1(x1982)+E(x1981,a15)+E(x1981,a1)+~E(f11(x1982,x1983),f11(x1981,x1984))+P1(f8(x1982,x1983,x1981))+~E(f7(x1982,x1983,x1981),a15)+~P4(f12(f12(x1982,x1983),x1981),f12(f12(a16,a17),a18))+P1(f9(x1982,x1983,x1981)) % 65.01/65.16 [199]~P1(x1994)+~P1(x1991)+~P1(x1993)+~P1(x1992)+E(x1991,a15)+~E(f7(x1992,x1993,x1991),x1991)+E(x1991,a1)+~E(f11(x1992,x1993),f11(x1991,x1994))+P1(f8(x1992,x1993,x1991))+~P4(f12(f12(x1992,x1993),x1991),f12(f12(a16,a17),a18))+P1(f9(x1992,x1993,x1991)) % 65.01/65.16 [200]~P1(x2004)+~P1(x2001)+~P1(x2003)+~P1(x2002)+E(x2001,a15)+E(x2001,a1)+~E(f11(x2002,x2003),f11(x2001,x2004))+P1(f8(x2002,x2003,x2001))+~E(f7(x2002,x2003,x2001),a15)+~P4(f12(f12(x2002,x2003),x2001),f12(f12(a16,a17),a18))+E(f11(x2001,f9(x2002,x2003,x2001)),x2002) % 65.01/65.16 [201]~P1(x2014)+~P1(x2012)+~P1(x2011)+~P1(x2013)+E(x2011,a15)+E(x2011,a1)+~E(f11(x2011,x2014),f11(x2012,x2013))+P1(f9(x2012,x2013,x2011))+~E(f7(x2012,x2013,x2011),a15)+~P4(f12(f12(x2012,x2013),x2011),f12(f12(a16,a17),a18))+E(f11(x2011,f8(x2012,x2013,x2011)),x2013) % 65.01/65.16 [202]~P1(x2024)+~P1(x2021)+~P1(x2023)+~P1(x2022)+E(x2021,a15)+~E(f7(x2022,x2023,x2021),x2021)+E(x2021,a1)+~E(f11(x2022,x2023),f11(x2021,x2024))+P1(f8(x2022,x2023,x2021))+~P4(f12(f12(x2022,x2023),x2021),f12(f12(a16,a17),a18))+E(f11(x2021,f9(x2022,x2023,x2021)),x2022) % 65.01/65.16 [203]~P1(x2034)+~P1(x2032)+~P1(x2031)+~P1(x2033)+E(x2031,a15)+~E(f7(x2032,x2033,x2031),x2031)+E(x2031,a1)+~E(f11(x2031,x2034),f11(x2032,x2033))+P1(f9(x2032,x2033,x2031))+~P4(f12(f12(x2032,x2033),x2031),f12(f12(a16,a17),a18))+E(f11(x2031,f8(x2032,x2033,x2031)),x2033) % 65.01/65.16 [206]~P1(x2064)+~P1(x2062)+~P1(x2061)+~P1(x2063)+E(x2061,a15)+E(x2061,a1)+~E(f11(x2061,x2064),f11(x2062,x2063))+E(f11(x2061,f8(x2062,x2063,x2061)),x2063)+~E(f7(x2062,x2063,x2061),a15)+~P4(f12(f12(x2062,x2063),x2061),f12(f12(a16,a17),a18))+E(f11(x2061,f9(x2062,x2063,x2061)),x2062) % 65.01/65.16 [207]~P1(x2074)+~P1(x2072)+~P1(x2071)+~P1(x2073)+E(x2071,a15)+~E(f7(x2072,x2073,x2071),x2071)+E(x2071,a1)+~E(f11(x2071,x2074),f11(x2072,x2073))+E(f11(x2071,f8(x2072,x2073,x2071)),x2073)+~P4(f12(f12(x2072,x2073),x2071),f12(f12(a16,a17),a18))+E(f11(x2071,f9(x2072,x2073,x2071)),x2072) % 65.01/65.16 [212]~P1(x2124)+~P1(x2121)+~P1(x2123)+~P1(x2122)+E(x2121,a15)+E(x2121,a1)+~E(f11(x2122,x2123),f11(x2121,x2124))+P1(f9(x2122,x2123,x2121))+P1(f8(x2122,x2123,x2121))+~P4(f12(f12(x2122,x2123),x2121),f12(f12(a16,a17),a18))+P1(f7(x2122,x2123,x2121)) % 65.01/65.16 [213]~P1(x2134)+~P1(x2131)+~P1(x2133)+~P1(x2132)+E(x2131,a15)+E(x2131,a1)+~E(f11(x2132,x2133),f11(x2131,x2134))+P1(f9(x2132,x2133,x2131))+P1(f8(x2132,x2133,x2131))+~P4(f12(f12(x2132,x2133),x2131),f12(f12(a16,a17),a18))+P1(f10(x2132,x2133,x2131)) % 65.01/65.16 [216]~P1(x2164)+~P1(x2161)+~P1(x2163)+~P1(x2162)+E(x2161,a15)+P3(f7(x2162,x2163,x2161),x2161)+E(x2161,a1)+~E(f11(x2162,x2163),f11(x2161,x2164))+P1(f8(x2162,x2163,x2161))+~P4(f12(f12(x2162,x2163),x2161),f12(f12(a16,a17),a18))+P1(f9(x2162,x2163,x2161)) % 65.01/65.16 [217]~P1(x2174)+~P1(x2171)+~P1(x2173)+~P1(x2172)+E(x2171,a15)+E(x2171,a1)+~E(f11(x2172,x2173),f11(x2171,x2174))+P1(f7(x2172,x2173,x2171))+P1(f8(x2172,x2173,x2171))+~P4(f12(f12(x2172,x2173),x2171),f12(f12(a16,a17),a18))+E(f11(x2171,f9(x2172,x2173,x2171)),x2172) % 65.01/65.16 [218]~P1(x2184)+~P1(x2181)+~P1(x2183)+~P1(x2182)+E(x2181,a15)+E(x2181,a1)+~E(f11(x2182,x2183),f11(x2181,x2184))+P1(f10(x2182,x2183,x2181))+P1(f8(x2182,x2183,x2181))+~P4(f12(f12(x2182,x2183),x2181),f12(f12(a16,a17),a18))+E(f11(x2181,f9(x2182,x2183,x2181)),x2182) % 65.01/65.16 [219]~P1(x2194)+~P1(x2192)+~P1(x2191)+~P1(x2193)+E(x2191,a15)+E(x2191,a1)+~E(f11(x2191,x2194),f11(x2192,x2193))+P1(f7(x2192,x2193,x2191))+P1(f9(x2192,x2193,x2191))+~P4(f12(f12(x2192,x2193),x2191),f12(f12(a16,a17),a18))+E(f11(x2191,f8(x2192,x2193,x2191)),x2193) % 65.01/65.16 [220]~P1(x2204)+~P1(x2202)+~P1(x2201)+~P1(x2203)+E(x2201,a15)+E(x2201,a1)+~E(f11(x2201,x2204),f11(x2202,x2203))+P1(f10(x2202,x2203,x2201))+P1(f9(x2202,x2203,x2201))+~P4(f12(f12(x2202,x2203),x2201),f12(f12(a16,a17),a18))+E(f11(x2201,f8(x2202,x2203,x2201)),x2203) % 65.01/65.16 [223]~P1(x2234)+~P1(x2231)+~P1(x2233)+~P1(x2232)+E(x2231,a15)+P3(f7(x2232,x2233,x2231),x2231)+E(x2231,a1)+~E(f11(x2232,x2233),f11(x2231,x2234))+P1(f8(x2232,x2233,x2231))+~P4(f12(f12(x2232,x2233),x2231),f12(f12(a16,a17),a18))+E(f11(x2231,f9(x2232,x2233,x2231)),x2232) % 65.01/65.16 [224]~P1(x2244)+~P1(x2242)+~P1(x2241)+~P1(x2243)+E(x2241,a15)+P3(f7(x2242,x2243,x2241),x2241)+E(x2241,a1)+~E(f11(x2241,x2244),f11(x2242,x2243))+P1(f9(x2242,x2243,x2241))+~P4(f12(f12(x2242,x2243),x2241),f12(f12(a16,a17),a18))+E(f11(x2241,f8(x2242,x2243,x2241)),x2243) % 65.01/65.16 [225]P3(x2251,x2252)+~P1(x2254)+~P1(x2251)+~P1(x2253)+~P1(x2252)+E(x2251,a15)+E(x2251,a1)+~E(f11(x2252,x2253),f11(x2251,x2254))+P1(f8(x2252,x2253,x2251))+~P4(f12(f12(x2252,x2253),x2251),f12(f12(a16,a17),a18))+E(f11(f7(x2252,x2253,x2251),f10(x2252,x2253,x2251)),x2251) % 65.01/65.16 [226]P3(x2261,x2263)+~P1(x2264)+~P1(x2262)+~P1(x2263)+~P1(x2261)+E(x2261,a15)+E(x2261,a1)+~E(f11(x2261,x2264),f11(x2262,x2263))+P1(f9(x2262,x2263,x2261))+~P4(f12(f12(x2262,x2263),x2261),f12(f12(a16,a17),a18))+E(f11(f7(x2262,x2263,x2261),f10(x2262,x2263,x2261)),x2261) % 65.01/65.16 [227]~P1(x2274)+~P1(x2272)+~P1(x2271)+~P1(x2273)+E(x2271,a15)+E(x2271,a1)+~E(f11(x2271,x2274),f11(x2272,x2273))+E(f11(x2271,f8(x2272,x2273,x2271)),x2273)+P1(f7(x2272,x2273,x2271))+~P4(f12(f12(x2272,x2273),x2271),f12(f12(a16,a17),a18))+E(f11(x2271,f9(x2272,x2273,x2271)),x2272) % 65.01/65.16 [228]~P1(x2284)+~P1(x2282)+~P1(x2281)+~P1(x2283)+E(x2281,a15)+E(x2281,a1)+~E(f11(x2281,x2284),f11(x2282,x2283))+E(f11(x2281,f8(x2282,x2283,x2281)),x2283)+P1(f10(x2282,x2283,x2281))+~P4(f12(f12(x2282,x2283),x2281),f12(f12(a16,a17),a18))+E(f11(x2281,f9(x2282,x2283,x2281)),x2282) % 65.01/65.16 [234]~P1(x2344)+~P1(x2342)+~P1(x2341)+~P1(x2343)+E(x2341,a15)+P3(f7(x2342,x2343,x2341),x2341)+E(x2341,a1)+~E(f11(x2341,x2344),f11(x2342,x2343))+E(f11(x2341,f8(x2342,x2343,x2341)),x2343)+~P4(f12(f12(x2342,x2343),x2341),f12(f12(a16,a17),a18))+E(f11(x2341,f9(x2342,x2343,x2341)),x2342) % 65.01/65.16 [235]P3(x2351,x2352)+~P1(x2354)+~P1(x2352)+~P1(x2351)+~P1(x2353)+E(x2351,a15)+E(x2351,a1)+~E(f11(x2351,x2354),f11(x2352,x2353))+E(f11(f7(x2352,x2353,x2351),f10(x2352,x2353,x2351)),x2351)+~P4(f12(f12(x2352,x2353),x2351),f12(f12(a16,a17),a18))+E(f11(x2351,f8(x2352,x2353,x2351)),x2353) % 65.01/65.16 [236]P3(x2361,x2363)+~P1(x2364)+~P1(x2362)+~P1(x2363)+~P1(x2361)+E(x2361,a15)+E(x2361,a1)+~E(f11(x2361,x2364),f11(x2362,x2363))+E(f11(f7(x2362,x2363,x2361),f10(x2362,x2363,x2361)),x2361)+~P4(f12(f12(x2362,x2363),x2361),f12(f12(a16,a17),a18))+E(f11(x2361,f9(x2362,x2363,x2361)),x2362) % 65.01/65.16 [246]~P1(x2464)+~P1(x2461)+~P1(x2463)+~P1(x2462)+E(x2461,a15)+E(x2461,a1)+~E(f11(x2462,x2463),f11(x2461,x2464))+P1(f9(x2462,x2463,x2461))+P1(f8(x2462,x2463,x2461))+~P4(f12(f12(x2462,x2463),x2461),f12(f12(a16,a17),a18))+E(f11(f7(x2462,x2463,x2461),f10(x2462,x2463,x2461)),x2461) % 65.01/65.16 [247]~P1(x2474)+~P1(x2471)+~P1(x2473)+~P1(x2472)+E(x2471,a15)+E(x2471,a1)+~E(f11(x2472,x2473),f11(x2471,x2474))+E(f11(f7(x2472,x2473,x2471),f10(x2472,x2473,x2471)),x2471)+P1(f8(x2472,x2473,x2471))+~P4(f12(f12(x2472,x2473),x2471),f12(f12(a16,a17),a18))+E(f11(x2471,f9(x2472,x2473,x2471)),x2472) % 65.01/65.16 [248]~P1(x2484)+~P1(x2482)+~P1(x2481)+~P1(x2483)+E(x2481,a15)+E(x2481,a1)+~E(f11(x2481,x2484),f11(x2482,x2483))+E(f11(f7(x2482,x2483,x2481),f10(x2482,x2483,x2481)),x2481)+P1(f9(x2482,x2483,x2481))+~P4(f12(f12(x2482,x2483),x2481),f12(f12(a16,a17),a18))+E(f11(x2481,f8(x2482,x2483,x2481)),x2483) % 65.01/65.16 [250]~P1(x2504)+~P1(x2502)+~P1(x2501)+~P1(x2503)+E(x2501,a15)+E(x2501,a1)+~E(f11(x2501,x2504),f11(x2502,x2503))+E(f11(x2501,f8(x2502,x2503,x2501)),x2503)+E(f11(f7(x2502,x2503,x2501),f10(x2502,x2503,x2501)),x2501)+~P4(f12(f12(x2502,x2503),x2501),f12(f12(a16,a17),a18))+E(f11(x2501,f9(x2502,x2503,x2501)),x2502) % 65.01/65.16 %EqnAxiom % 65.01/65.16 [1]E(x11,x11) % 65.01/65.16 [2]E(x22,x21)+~E(x21,x22) % 65.01/65.16 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 65.01/65.16 [4]~E(x41,x42)+E(f11(x41,x43),f11(x42,x43)) % 65.01/65.16 [5]~E(x51,x52)+E(f11(x53,x51),f11(x53,x52)) % 65.01/65.16 [6]~E(x61,x62)+E(f12(x61,x63),f12(x62,x63)) % 65.01/65.16 [7]~E(x71,x72)+E(f12(x73,x71),f12(x73,x72)) % 65.01/65.16 [8]~E(x81,x82)+E(f7(x81,x83,x84),f7(x82,x83,x84)) % 65.01/65.16 [9]~E(x91,x92)+E(f7(x93,x91,x94),f7(x93,x92,x94)) % 65.01/65.16 [10]~E(x101,x102)+E(f7(x103,x104,x101),f7(x103,x104,x102)) % 65.01/65.16 [11]~E(x111,x112)+E(f9(x111,x113,x114),f9(x112,x113,x114)) % 65.01/65.16 [12]~E(x121,x122)+E(f9(x123,x121,x124),f9(x123,x122,x124)) % 65.01/65.16 [13]~E(x131,x132)+E(f9(x133,x134,x131),f9(x133,x134,x132)) % 65.01/65.16 [14]~E(x141,x142)+E(f10(x141,x143,x144),f10(x142,x143,x144)) % 65.01/65.16 [15]~E(x151,x152)+E(f10(x153,x151,x154),f10(x153,x152,x154)) % 65.01/65.16 [16]~E(x161,x162)+E(f10(x163,x164,x161),f10(x163,x164,x162)) % 65.01/65.16 [17]~E(x171,x172)+E(f8(x171,x173,x174),f8(x172,x173,x174)) % 65.01/65.16 [18]~E(x181,x182)+E(f8(x183,x181,x184),f8(x183,x182,x184)) % 65.01/65.16 [19]~E(x191,x192)+E(f8(x193,x194,x191),f8(x193,x194,x192)) % 65.01/65.16 [20]~E(x201,x202)+E(f14(x201,x203),f14(x202,x203)) % 65.01/65.16 [21]~E(x211,x212)+E(f14(x213,x211),f14(x213,x212)) % 65.01/65.16 [22]~E(x221,x222)+E(f13(x221,x223),f13(x222,x223)) % 65.01/65.16 [23]~E(x231,x232)+E(f13(x233,x231),f13(x233,x232)) % 65.01/65.16 [24]~E(x241,x242)+E(f5(x241,x243),f5(x242,x243)) % 65.01/65.16 [25]~E(x251,x252)+E(f5(x253,x251),f5(x253,x252)) % 65.01/65.16 [26]~E(x261,x262)+E(f3(x261),f3(x262)) % 65.01/65.16 [27]~E(x271,x272)+E(f6(x271,x273),f6(x272,x273)) % 65.01/65.16 [28]~E(x281,x282)+E(f6(x283,x281),f6(x283,x282)) % 65.01/65.16 [29]~E(x291,x292)+E(f4(x291),f4(x292)) % 65.01/65.16 [30]~P1(x301)+P1(x302)+~E(x301,x302) % 65.01/65.16 [31]P4(x312,x313)+~E(x311,x312)+~P4(x311,x313) % 65.01/65.16 [32]P4(x323,x322)+~E(x321,x322)+~P4(x323,x321) % 65.01/65.16 [33]P3(x332,x333)+~E(x331,x332)+~P3(x331,x333) % 65.01/65.16 [34]P3(x343,x342)+~E(x341,x342)+~P3(x343,x341) % 65.01/65.16 [35]~P2(x351)+P2(x352)+~E(x351,x352) % 65.01/65.16 [36]P5(x362,x363)+~E(x361,x362)+~P5(x361,x363) % 65.01/65.16 [37]P5(x373,x372)+~E(x371,x372)+~P5(x373,x371) % 65.01/65.16 % 65.01/65.16 %------------------------------------------- % 65.01/65.16 cnf(254,plain, % 65.01/65.16 (~P2(a1)+~P1(a1)), % 65.01/65.16 inference(equality_inference,[],[54])). % 65.01/65.16 cnf(255,plain, % 65.01/65.16 (~P2(a15)+~P1(a15)), % 65.01/65.16 inference(equality_inference,[],[55])). % 65.01/65.16 cnf(257,plain, % 65.01/65.16 (P3(x2571,f11(x2571,x2572))+~P1(x2571)+~P1(f11(x2571,x2572))+~P1(x2572)), % 65.01/65.16 inference(equality_inference,[],[94])). % 65.01/65.16 cnf(258,plain, % 65.01/65.16 (P5(x2581,f12(x2581,x2582))+~P1(f12(x2581,x2582))+~P1(x2581)+~P1(x2582)), % 65.01/65.16 inference(equality_inference,[],[95])). % 65.01/65.16 cnf(259,plain, % 65.01/65.16 (~P5(x2591,x2592)+~P1(x2591)+~P1(x2592)+P1(f13(x2592,x2591))), % 65.01/65.16 inference(equality_inference,[],[97])). % 65.01/65.16 cnf(265,plain, % 65.01/65.16 (~P5(x2651,x2652)+~P1(x2652)+~P1(x2651)+E(f12(x2651,f13(x2652,x2651)),x2652)), % 65.01/65.16 inference(equality_inference,[],[105])). % 65.01/65.16 cnf(267,plain, % 65.01/65.16 (~P5(x2671,f12(x2671,x2672))+~P1(f12(x2671,x2672))+~P1(x2671)+~P1(x2672)+E(x2672,f13(f12(x2671,x2672),x2671))), % 65.01/65.16 inference(equality_inference,[],[111])). % 65.01/65.16 cnf(268,plain, % 65.01/65.16 (~P3(x2681,f11(x2681,x2682))+~P1(x2681)+~P1(f11(x2681,x2682))+~P1(x2682)+E(x2681,a1)+E(x2682,f14(f11(x2681,x2682),x2681))), % 65.01/65.16 inference(equality_inference,[],[112])). % 65.01/65.16 cnf(314,plain, % 65.01/65.16 (~P2(a1)), % 65.01/65.16 inference(scs_inference,[],[38,254])). % 65.01/65.16 cnf(315,plain, % 65.01/65.16 (~P2(a15)), % 65.01/65.16 inference(scs_inference,[],[39,255])). % 65.01/65.16 cnf(316,plain, % 65.01/65.16 (E(f11(a16,a17),f11(a18,a2))), % 65.01/65.16 inference(scs_inference,[],[45,2])). % 65.01/65.16 cnf(317,plain, % 65.01/65.16 (~E(f11(a16,a17),a16)), % 65.01/65.16 inference(scs_inference,[],[52,45,46,2,34])). % 65.01/65.16 cnf(318,plain, % 65.01/65.16 (~P3(a1,a18)), % 65.01/65.16 inference(scs_inference,[],[52,38,47,48,45,46,2,34,73])). % 65.01/65.16 cnf(320,plain, % 65.01/65.16 (P5(a1,a1)), % 65.01/65.16 inference(scs_inference,[],[52,38,47,48,45,46,2,34,73,84])). % 65.01/65.16 cnf(322,plain, % 65.01/65.16 (E(f12(a1,f13(a1,a1)),a1)), % 65.01/65.16 inference(scs_inference,[],[52,38,47,48,45,46,2,34,73,84,265])). % 65.01/65.16 cnf(324,plain, % 65.01/65.16 (E(x3241,a1)+~E(x3241,f12(a1,f13(a1,a1)))), % 65.01/65.16 inference(scs_inference,[],[52,38,47,48,45,46,2,34,73,84,265,3])). % 65.01/65.16 cnf(327,plain, % 65.01/65.16 (~E(a18,f12(a1,f13(a1,a1)))+P2(a1)), % 65.01/65.16 inference(scs_inference,[],[52,38,42,44,47,48,45,46,2,34,73,84,265,3,33,54,35])). % 65.01/65.16 cnf(334,plain, % 65.01/65.16 (~E(a18,f12(a1,f13(a1,a1)))), % 65.01/65.16 inference(scs_inference,[],[314,327])). % 65.01/65.16 cnf(335,plain, % 65.01/65.16 (E(a1,f12(a1,f13(a1,a1)))), % 65.01/65.16 inference(scs_inference,[],[322,314,327,2])). % 65.01/65.16 cnf(336,plain, % 65.01/65.16 (P1(f12(a1,f13(a1,a1)))), % 65.01/65.16 inference(scs_inference,[],[38,322,314,327,2,30])). % 65.01/65.16 cnf(337,plain, % 65.01/65.16 (P5(a1,f12(a1,f13(a1,a1)))), % 65.01/65.16 inference(scs_inference,[],[38,320,322,314,327,2,30,37])). % 65.01/65.16 cnf(338,plain, % 65.01/65.16 (~E(a18,a1)), % 65.01/65.16 inference(scs_inference,[],[38,320,322,314,327,2,30,37,3])). % 65.01/65.16 cnf(339,plain, % 65.01/65.16 (~P2(f12(a1,f13(a1,a1)))), % 65.01/65.16 inference(scs_inference,[],[38,320,322,314,327,2,30,37,3,35])). % 65.01/65.16 cnf(340,plain, % 65.01/65.16 (P5(f12(a1,f13(a1,a1)),a1)), % 65.01/65.16 inference(scs_inference,[],[38,320,322,314,327,2,30,37,3,35,36])). % 65.01/65.16 cnf(341,plain, % 65.01/65.16 (P3(f3(a18),a18)), % 65.01/65.16 inference(scs_inference,[],[42,38,320,322,314,49,327,2,30,37,3,35,36,74])). % 65.01/65.16 cnf(343,plain, % 65.01/65.16 (P5(a15,a18)), % 65.01/65.16 inference(scs_inference,[],[42,38,320,322,314,49,327,2,30,37,3,35,36,74,66])). % 65.01/65.16 cnf(345,plain, % 65.01/65.16 (P5(a15,a15)), % 65.01/65.16 inference(scs_inference,[],[39,42,38,320,322,314,49,327,2,30,37,3,35,36,74,66,84])). % 65.01/65.16 cnf(347,plain, % 65.01/65.16 (P1(f13(a15,a15))), % 65.01/65.16 inference(scs_inference,[],[39,42,38,320,322,314,49,327,2,30,37,3,35,36,74,66,84,259])). % 65.01/65.16 cnf(349,plain, % 65.01/65.16 (E(f12(a15,f13(a15,a15)),a15)), % 65.01/65.16 inference(scs_inference,[],[39,42,38,320,322,314,49,327,2,30,37,3,35,36,74,66,84,259,265])). % 65.01/65.16 cnf(351,plain, % 65.01/65.16 (~P5(a18,a15)), % 65.01/65.16 inference(scs_inference,[],[39,42,38,320,322,314,49,327,2,30,37,3,35,36,74,66,84,259,265,96])). % 65.01/65.16 cnf(355,plain, % 65.01/65.16 (~E(f3(a18),a1)), % 65.01/65.16 inference(scs_inference,[],[39,42,38,318,320,322,314,49,327,2,30,37,3,35,36,74,66,84,259,265,96,55,33])). % 65.01/65.16 cnf(356,plain, % 65.01/65.16 (~E(f3(a18),f12(a1,f13(a1,a1)))), % 65.01/65.16 inference(scs_inference,[],[39,42,38,318,320,322,314,49,327,2,30,37,3,35,36,74,66,84,259,265,96,55,33,324])). % 65.01/65.16 cnf(357,plain, % 65.01/65.16 (P3(f3(a18),x3571)+~E(a18,x3571)), % 65.01/65.16 inference(scs_inference,[],[39,42,38,318,320,322,314,49,327,2,30,37,3,35,36,74,66,84,259,265,96,55,33,324,34])). % 65.01/65.16 cnf(358,plain, % 65.01/65.16 (P5(a16,a16)), % 65.01/65.16 inference(scs_inference,[],[39,40,42,38,318,320,322,314,49,327,2,30,37,3,35,36,74,66,84,259,265,96,55,33,324,34,75])). % 65.01/65.16 cnf(367,plain, % 65.01/65.16 (E(a15,f12(a15,f13(a15,a15)))), % 65.01/65.16 inference(scs_inference,[],[349,2])). % 65.01/65.16 cnf(368,plain, % 65.01/65.16 (~P2(f12(a15,f13(a15,a15)))), % 65.01/65.16 inference(scs_inference,[],[349,315,2,35])). % 65.01/65.16 cnf(369,plain, % 65.01/65.16 (P1(f12(a15,f13(a15,a15)))), % 65.01/65.16 inference(scs_inference,[],[39,349,315,2,35,30])). % 65.01/65.16 cnf(371,plain, % 65.01/65.16 (~E(a1,f12(a15,f13(a15,a15)))), % 65.01/65.16 inference(scs_inference,[],[39,47,345,349,315,2,35,30,37,3])). % 65.01/65.16 cnf(372,plain, % 65.01/65.16 (~E(a15,a18)), % 65.01/65.16 inference(scs_inference,[],[39,351,47,345,349,315,2,35,30,37,3,36])). % 65.01/65.16 cnf(373,plain, % 65.01/65.16 (E(f12(a16,f13(a16,a16)),a16)), % 65.01/65.16 inference(scs_inference,[],[39,351,40,47,345,349,315,358,2,35,30,37,3,36,265])). % 65.01/65.16 cnf(377,plain, % 65.01/65.16 (P1(f13(a16,a16))), % 65.01/65.16 inference(scs_inference,[],[39,336,351,40,47,345,349,315,358,2,35,30,37,3,36,265,84,259])). % 65.01/65.16 cnf(380,plain, % 65.01/65.16 (P5(f13(a15,a15),f13(a15,a15))), % 65.01/65.16 inference(scs_inference,[],[39,336,347,351,40,47,46,345,349,315,358,2,35,30,37,3,36,265,84,259,33,75])). % 65.01/65.16 cnf(391,plain, % 65.01/65.16 (E(a16,f12(a16,f13(a16,a16)))), % 65.01/65.16 inference(scs_inference,[],[373,2])). % 65.01/65.16 cnf(392,plain, % 65.01/65.16 (P1(f12(a16,f13(a16,a16)))), % 65.01/65.16 inference(scs_inference,[],[40,373,2,30])). % 65.01/65.16 cnf(393,plain, % 65.01/65.16 (P5(a16,f12(a16,f13(a16,a16)))), % 65.01/65.16 inference(scs_inference,[],[40,373,358,2,30,37])). % 65.01/65.16 cnf(394,plain, % 65.01/65.16 (P5(f12(a15,f13(a15,a15)),a18)), % 65.01/65.16 inference(scs_inference,[],[367,40,343,373,358,2,30,37,36])). % 65.01/65.16 cnf(396,plain, % 65.01/65.16 (E(f12(f13(a15,a15),f13(f13(a15,a15),f13(a15,a15))),f13(a15,a15))), % 65.01/65.16 inference(scs_inference,[],[367,347,40,49,349,343,380,373,358,2,30,37,36,3,265])). % 65.01/65.16 cnf(400,plain, % 65.01/65.16 (P5(f12(a15,f13(a15,a15)),f12(a15,f13(a15,a15)))), % 65.01/65.16 inference(scs_inference,[],[369,367,347,40,49,349,343,380,373,358,2,30,37,36,3,265,259,84])). % 65.01/65.16 cnf(404,plain, % 65.01/65.16 (~P5(a18,f12(a15,f13(a15,a15)))), % 65.01/65.16 inference(scs_inference,[],[39,369,367,347,40,42,49,349,343,345,380,373,358,2,30,37,36,3,265,259,84,97,96])). % 65.01/65.16 cnf(409,plain, % 65.01/65.16 (P5(f13(a16,a16),f13(a16,a16))), % 65.01/65.16 inference(scs_inference,[],[39,316,369,377,367,347,40,42,49,349,343,345,380,373,358,2,30,37,36,3,265,259,84,97,96,35,258,75])). % 65.01/65.16 cnf(414,plain, % 65.01/65.16 (E(f13(a15,a15),f12(f13(a15,a15),f13(f13(a15,a15),f13(a15,a15))))), % 65.01/65.16 inference(scs_inference,[],[396,2])). % 65.01/65.16 cnf(416,plain, % 65.01/65.16 (~E(f12(a15,f13(a15,a15)),a18)), % 65.01/65.16 inference(scs_inference,[],[404,349,396,400,2,37,36])). % 65.01/65.16 cnf(418,plain, % 65.01/65.16 (E(f12(f13(a16,a16),f13(f13(a16,a16),f13(a16,a16))),f13(a16,a16))), % 65.01/65.16 inference(scs_inference,[],[317,404,377,349,373,396,400,409,2,37,36,3,265])). % 65.01/65.16 cnf(420,plain, % 65.01/65.16 (P1(f13(f13(a16,a16),f13(a16,a16)))), % 65.01/65.16 inference(scs_inference,[],[317,404,377,349,373,396,400,409,2,37,36,3,265,259])). % 65.01/65.16 cnf(431,plain, % 65.01/65.16 (E(f13(a16,a16),f12(f13(a16,a16),f13(f13(a16,a16),f13(a16,a16))))), % 65.01/65.16 inference(scs_inference,[],[418,2])). % 65.01/65.16 cnf(433,plain, % 65.01/65.16 (P5(f12(a16,f13(a16,a16)),f12(a16,f13(a16,a16)))), % 65.01/65.16 inference(scs_inference,[],[414,391,418,393,380,2,37,36])). % 65.01/65.16 cnf(434,plain, % 65.01/65.16 (P1(f13(a1,a1))), % 65.01/65.16 inference(scs_inference,[],[414,391,38,418,393,380,320,2,37,36,259])). % 65.01/65.16 cnf(439,plain, % 65.01/65.16 (E(f13(a1,a1),a1)), % 65.01/65.16 inference(scs_inference,[],[414,420,391,38,322,418,393,380,320,2,37,36,259,84,35,78])). % 65.01/65.16 cnf(441,plain, % 65.01/65.16 (~P2(f13(a1,a1))), % 65.01/65.16 inference(scs_inference,[],[414,420,391,38,322,418,393,380,320,2,37,36,259,84,35,78,54])). % 65.01/65.16 cnf(444,plain, % 65.01/65.16 (~E(f3(a18),f13(a1,a1))), % 65.01/65.16 inference(scs_inference,[],[355,414,420,391,38,322,418,393,380,320,45,2,37,36,259,84,35,78,54,30,3])). % 65.01/65.16 cnf(447,plain, % 65.01/65.16 (P5(a2,a2)), % 65.01/65.16 inference(scs_inference,[],[355,414,420,391,43,38,322,418,393,380,320,45,2,37,36,259,84,35,78,54,30,3,258,75])). % 65.01/65.16 cnf(451,plain, % 65.01/65.16 (E(f12(a2,f13(a2,a2)),a2)), % 65.01/65.16 inference(scs_inference,[],[355,414,420,391,43,38,322,418,393,380,320,45,2,37,36,259,84,35,78,54,30,3,258,75,257,265])). % 65.01/65.16 cnf(454,plain, % 65.01/65.16 (E(a1,f13(a1,a1))), % 65.01/65.16 inference(scs_inference,[],[439,2])). % 65.01/65.16 cnf(455,plain, % 65.01/65.16 (P5(f12(a16,f13(a16,a16)),a16)), % 65.01/65.16 inference(scs_inference,[],[373,439,433,2,37])). % 65.01/65.16 cnf(457,plain, % 65.01/65.16 (P1(f13(a2,a2))), % 65.01/65.16 inference(scs_inference,[],[431,43,373,439,433,447,409,2,37,36,259])). % 65.01/65.16 cnf(459,plain, % 65.01/65.16 (P5(f13(a1,a1),f13(a1,a1))), % 65.01/65.16 inference(scs_inference,[],[434,431,43,373,439,433,447,409,2,37,36,259,84])). % 65.01/65.16 cnf(462,plain, % 65.01/65.16 (E(f12(f13(a1,a1),f13(f13(a1,a1),f13(a1,a1))),f13(a1,a1))), % 65.01/65.16 inference(scs_inference,[],[391,434,431,43,373,439,433,447,409,2,37,36,259,84,35,265])). % 65.01/65.16 cnf(464,plain, % 65.01/65.16 (P1(f12(f13(a1,a1),f13(f13(a1,a1),f13(a1,a1))))), % 65.01/65.16 inference(scs_inference,[],[391,38,434,431,43,373,439,433,447,409,320,2,37,36,259,84,35,265,97])). % 65.01/65.16 cnf(469,plain, % 65.01/65.16 (P5(a17,a17)), % 65.01/65.16 inference(scs_inference,[],[391,40,38,434,431,41,43,373,439,433,451,447,409,320,2,37,36,259,84,35,265,97,3,258,75])). % 65.01/65.16 cnf(476,plain, % 65.01/65.16 (E(a2,f12(a2,f13(a2,a2)))), % 65.01/65.16 inference(scs_inference,[],[451,2])). % 65.01/65.16 cnf(477,plain, % 65.01/65.16 (P1(f12(a2,f13(a2,a2)))), % 65.01/65.16 inference(scs_inference,[],[43,451,2,30])). % 65.01/65.16 cnf(479,plain, % 65.01/65.16 (P5(f13(a1,a1),a1)), % 65.01/65.16 inference(scs_inference,[],[43,439,451,462,459,441,2,30,35,37])). % 65.01/65.16 cnf(480,plain, % 65.01/65.16 (P5(a1,f13(a1,a1))), % 65.01/65.16 inference(scs_inference,[],[43,439,451,462,459,441,2,30,35,37,36])). % 65.01/65.16 cnf(482,plain, % 65.01/65.16 (E(f12(a17,f13(a17,a17)),a17)), % 65.01/65.16 inference(scs_inference,[],[444,41,43,439,451,462,459,441,469,2,30,35,37,36,3,265])). % 65.01/65.16 cnf(484,plain, % 65.01/65.16 (P1(f13(f13(a1,a1),f13(a1,a1)))), % 65.01/65.16 inference(scs_inference,[],[434,444,41,43,439,451,462,459,441,469,2,30,35,37,36,3,265,259])). % 65.01/65.16 cnf(486,plain, % 65.01/65.16 (P5(f13(a2,a2),f13(a2,a2))), % 65.01/65.16 inference(scs_inference,[],[434,444,457,41,43,439,451,462,459,441,469,2,30,35,37,36,3,265,259,84])). % 65.01/65.16 cnf(488,plain, % 65.01/65.16 (P5(a18,a18)), % 65.01/65.16 inference(scs_inference,[],[434,444,457,41,43,42,439,451,462,459,441,469,2,30,35,37,36,3,265,259,84,75])). % 65.01/65.16 cnf(494,plain, % 65.01/65.16 (P5(f3(a18),a18)+~P1(f3(a18))), % 65.01/65.16 inference(scs_inference,[],[39,338,38,434,444,457,41,43,42,341,439,451,462,459,441,469,2,30,35,37,36,3,265,259,84,75,258,257,267,90])). % 65.01/65.16 cnf(496,plain, % 65.01/65.16 (E(f13(a1,a1),f12(f13(a1,a1),f13(f13(a1,a1),f13(a1,a1))))), % 65.01/65.16 inference(scs_inference,[],[462,2])). % 65.01/65.16 cnf(497,plain, % 65.01/65.16 (P5(f13(a1,a1),f12(a1,f13(a1,a1)))), % 65.01/65.16 inference(scs_inference,[],[335,462,479,2,37])). % 65.01/65.16 cnf(498,plain, % 65.01/65.16 (~E(f12(a16,f13(a16,a16)),a18)), % 65.01/65.16 inference(scs_inference,[],[335,462,455,479,50,2,37,36])). % 65.01/65.16 cnf(499,plain, % 65.01/65.16 (~E(a18,f13(a1,a1))), % 65.01/65.16 inference(scs_inference,[],[335,338,439,462,455,479,50,2,37,36,3])). % 65.01/65.16 cnf(500,plain, % 65.01/65.16 (E(f12(f13(a2,a2),f13(f13(a2,a2),f13(a2,a2))),f13(a2,a2))), % 65.01/65.16 inference(scs_inference,[],[335,338,457,439,462,455,486,479,50,2,37,36,3,265])). % 65.01/65.16 cnf(502,plain, % 65.01/65.16 (P1(f13(f13(a2,a2),f13(a2,a2)))), % 65.01/65.16 inference(scs_inference,[],[335,338,457,439,462,455,486,479,50,2,37,36,3,265,259])). % 65.01/65.16 cnf(504,plain, % 65.01/65.16 (P5(f13(f13(a1,a1),f13(a1,a1)),f13(f13(a1,a1),f13(a1,a1)))), % 65.01/65.16 inference(scs_inference,[],[335,338,457,484,439,462,455,486,479,50,2,37,36,3,265,259,84])). % 65.01/65.16 cnf(513,plain, % 65.01/65.16 (P5(f12(a2,f13(a2,a2)),f12(a2,f13(a2,a2)))), % 65.01/65.16 inference(scs_inference,[],[335,338,392,431,434,457,43,484,477,439,462,455,486,479,50,447,2,37,36,3,265,259,84,97,35,73,258,75])). % 65.01/65.16 cnf(519,plain, % 65.01/65.16 (E(a17,f12(a17,f13(a17,a17)))), % 65.01/65.16 inference(scs_inference,[],[482,2])). % 65.01/65.16 cnf(520,plain, % 65.01/65.16 (P1(f12(a17,f13(a17,a17)))), % 65.01/65.16 inference(scs_inference,[],[41,482,2,30])). % 65.01/65.16 cnf(521,plain, % 65.01/65.16 (P5(a1,f12(f13(a1,a1),f13(f13(a1,a1),f13(a1,a1))))), % 65.01/65.16 inference(scs_inference,[],[41,496,482,480,2,30,37])). % 65.01/65.16 cnf(522,plain, % 65.01/65.16 (P5(f12(a1,f13(a1,a1)),f13(a1,a1))), % 65.01/65.16 inference(scs_inference,[],[335,41,496,482,480,2,30,37,36])). % 65.01/65.16 cnf(524,plain, % 65.01/65.16 (E(f12(a18,f13(a18,a18)),a18)), % 65.01/65.16 inference(scs_inference,[],[335,41,496,499,42,462,482,480,488,2,30,37,36,3,265])). % 65.01/65.16 cnf(526,plain, % 65.01/65.16 (P1(f13(a17,a17))), % 65.01/65.16 inference(scs_inference,[],[335,41,496,499,42,462,482,480,488,469,2,30,37,36,3,265,259])). % 65.01/65.16 cnf(530,plain, % 65.01/65.16 (E(f12(a1,f13(a1,a1)),f13(a1,a1))), % 65.01/65.16 inference(scs_inference,[],[335,336,434,41,496,502,499,42,462,482,480,488,497,469,2,30,37,36,3,265,259,84,96])). % 65.01/65.16 cnf(532,plain, % 65.01/65.16 (E(f13(a1,a1),f13(f13(a1,a1),a1))), % 65.01/65.16 inference(scs_inference,[],[335,38,336,434,41,496,502,499,42,462,482,480,488,497,469,2,30,37,36,3,265,259,84,96,111])). % 65.01/65.16 cnf(535,plain, % 65.01/65.16 (P5(f12(a17,f13(a17,a17)),f12(a17,f13(a17,a17)))), % 65.01/65.16 inference(scs_inference,[],[335,38,336,434,41,476,496,502,499,42,462,482,480,488,497,469,2,30,37,36,3,265,259,84,96,111,35,75])). % 65.01/65.16 cnf(542,plain, % 65.01/65.16 (E(f13(a1,a1),f12(a1,f13(a1,a1)))), % 65.01/65.16 inference(scs_inference,[],[530,2])). % 65.01/65.16 cnf(543,plain, % 65.01/65.16 (P1(f13(f13(a1,a1),a1))), % 65.01/65.16 inference(scs_inference,[],[434,530,532,2,30])). % 65.01/65.16 cnf(546,plain, % 65.01/65.16 (E(a1,f13(f13(a1,a1),a1))), % 65.01/65.16 inference(scs_inference,[],[434,454,530,496,451,479,513,532,2,30,37,36,3])). % 65.01/65.16 cnf(547,plain, % 65.01/65.16 (P1(f13(a18,a18))), % 65.01/65.16 inference(scs_inference,[],[434,454,42,530,496,451,488,479,513,532,2,30,37,36,3,259])). % 65.01/65.16 cnf(549,plain, % 65.01/65.16 (P5(f13(a17,a17),f13(a17,a17))), % 65.01/65.16 inference(scs_inference,[],[434,454,42,530,526,496,451,488,479,513,532,2,30,37,36,3,259,84])). % 65.01/65.16 cnf(551,plain, % 65.01/65.16 (E(f12(f13(a1,a1),f13(f13(a1,a1),f13(a1,a1))),a1)), % 65.01/65.16 inference(scs_inference,[],[38,434,454,42,464,530,526,496,451,488,479,513,532,521,2,30,37,36,3,259,84,96])). % 65.01/65.16 cnf(553,plain, % 65.01/65.16 (E(f13(f13(a1,a1),f13(a1,a1)),f13(a1,f13(a1,a1)))), % 65.01/65.16 inference(scs_inference,[],[38,434,454,484,42,464,530,526,496,451,488,479,513,532,521,2,30,37,36,3,259,84,96,111])). % 65.01/65.16 cnf(556,plain, % 65.01/65.16 (E(f13(f13(a1,a1),f13(a1,a1)),a1)), % 65.01/65.16 inference(scs_inference,[],[38,434,454,484,42,464,530,526,519,496,451,488,479,513,532,521,2,30,37,36,3,259,84,96,111,35,78])). % 65.01/65.16 cnf(558,plain, % 65.01/65.16 (E(f12(f13(a17,a17),f13(f13(a17,a17),f13(a17,a17))),f13(a17,a17))), % 65.01/65.16 inference(scs_inference,[],[38,434,454,484,42,464,530,526,519,496,451,488,479,513,532,521,2,30,37,36,3,259,84,96,111,35,78,265])). % 65.01/65.16 cnf(562,plain, % 65.01/65.16 (~P2(f13(f13(a1,a1),f13(a1,a1)))), % 65.01/65.16 inference(scs_inference,[],[38,434,454,41,484,42,464,530,526,519,496,451,488,479,513,532,521,469,2,30,37,36,3,259,84,96,111,35,78,265,97,54])). % 65.01/65.16 cnf(564,plain, % 65.01/65.16 (P5(f13(f13(a1,a1),a1),f13(f13(a1,a1),a1))), % 65.01/65.16 inference(scs_inference,[],[38,434,454,41,484,42,464,530,526,519,496,451,488,479,513,532,521,469,2,30,37,36,3,259,84,96,111,35,78,265,97,54,75])). % 65.01/65.16 cnf(572,plain, % 65.01/65.16 (P1(f13(a1,f13(a1,a1)))), % 65.01/65.16 inference(scs_inference,[],[484,551,553,2,30])). % 65.01/65.16 cnf(573,plain, % 65.01/65.16 (P5(f13(f13(a1,a1),f13(a1,a1)),f13(a1,f13(a1,a1)))), % 65.01/65.16 inference(scs_inference,[],[484,551,504,553,2,30,37])). % 65.01/65.16 cnf(574,plain, % 65.01/65.16 (P5(f13(a1,f13(a1,a1)),f13(f13(a1,a1),f13(a1,a1)))), % 65.01/65.16 inference(scs_inference,[],[484,551,504,553,2,30,37,36])). % 65.01/65.16 cnf(575,plain, % 65.01/65.16 (~E(a1,f12(a18,f13(a18,a18)))), % 65.01/65.16 inference(scs_inference,[],[484,551,48,524,504,553,2,30,37,36,3])). % 65.01/65.16 cnf(576,plain, % 65.01/65.16 (P1(f13(f13(a17,a17),f13(a17,a17)))), % 65.01/65.16 inference(scs_inference,[],[484,526,551,48,524,504,549,553,2,30,37,36,3,259])). % 65.01/65.16 cnf(578,plain, % 65.01/65.16 (P5(f13(a18,a18),f13(a18,a18))), % 65.01/65.16 inference(scs_inference,[],[484,526,547,551,48,524,504,549,553,2,30,37,36,3,259,84])). % 65.01/65.16 cnf(580,plain, % 65.01/65.16 (E(f13(a1,f13(a1,a1)),f13(f13(a1,a1),f13(a1,a1)))), % 65.01/65.16 inference(scs_inference,[],[484,526,547,551,48,524,504,549,553,2,30,37,36,3,259,84,96])). % 65.01/65.16 cnf(583,plain, % 65.01/65.16 (E(f12(f13(a18,a18),f13(f13(a18,a18),f13(a18,a18))),f13(a18,a18))), % 65.01/65.16 inference(scs_inference,[],[484,526,547,551,396,48,524,504,549,553,2,30,37,36,3,259,84,96,35,265])). % 65.01/65.16 cnf(590,plain, % 65.01/65.16 (E(f13(f13(a1,a1),a1),a1)), % 65.01/65.16 inference(scs_inference,[],[546,2])). % 65.01/65.16 cnf(593,plain, % 65.01/65.16 (~P2(f13(a1,f13(a1,a1)))), % 65.01/65.16 inference(scs_inference,[],[546,580,543,562,2,54,35])). % 65.01/65.16 cnf(594,plain, % 65.01/65.16 (P5(f12(a17,f13(a17,a17)),a17)), % 65.01/65.16 inference(scs_inference,[],[546,580,543,482,562,535,2,54,35,37])). % 65.01/65.16 cnf(596,plain, % 65.01/65.16 (E(f12(a1,f13(a1,a1)),f13(f13(a1,a1),a1))), % 65.01/65.16 inference(scs_inference,[],[530,546,580,543,482,532,562,535,2,54,35,37,36,3])). % 65.01/65.16 cnf(597,plain, % 65.01/65.16 (P1(f13(f13(a18,a18),f13(a18,a18)))), % 65.01/65.16 inference(scs_inference,[],[530,546,580,543,547,482,532,562,578,535,2,54,35,37,36,3,259])). % 65.01/65.16 cnf(601,plain, % 65.01/65.16 (P5(a1,f13(f13(a1,a1),a1))), % 65.01/65.16 inference(scs_inference,[],[38,434,530,546,576,580,543,547,482,532,562,578,535,2,54,35,37,36,3,259,84,95])). % 65.01/65.16 cnf(603,plain, % 65.01/65.16 (E(f13(a1,a1),f13(f13(f13(a1,a1),a1),a1))), % 65.01/65.16 inference(scs_inference,[],[38,434,530,546,576,580,543,547,482,532,562,578,535,2,54,35,37,36,3,259,84,95,111])). % 65.01/65.16 cnf(612,plain, % 65.01/65.17 (~P5(a16,a18)+~E(f13(a16,a16),f13(a18,a16))), % 65.01/65.17 inference(scs_inference,[],[40,38,434,530,42,546,576,580,543,572,547,482,498,532,562,578,535,2,54,35,37,36,3,259,84,95,111,30,75,257,258,105])). % 65.01/65.17 cnf(615,plain, % 65.01/65.17 (E(f13(f13(a1,a1),a1),f12(a1,f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[596,2])). % 65.01/65.17 cnf(616,plain, % 65.01/65.17 (P5(f13(f13(a1,a1),a1),a1)), % 65.01/65.17 inference(scs_inference,[],[596,590,564,2,37])). % 65.01/65.17 cnf(617,plain, % 65.01/65.17 (~E(f12(a17,f13(a17,a17)),a18)), % 65.01/65.17 inference(scs_inference,[],[596,590,564,594,51,2,37,36])). % 65.01/65.17 cnf(618,plain, % 65.01/65.17 (~E(a18,f13(f13(a1,a1),a1))), % 65.01/65.17 inference(scs_inference,[],[338,596,590,564,594,51,2,37,36,3])). % 65.01/65.17 cnf(625,plain, % 65.01/65.17 (P1(f5(a15,a15))), % 65.01/65.17 inference(scs_inference,[],[39,64,99])). % 65.01/65.17 cnf(626,plain, % 65.01/65.17 (E(f13(a2,a2),f12(f13(a2,a2),f13(f13(a2,a2),f13(a2,a2))))), % 65.01/65.17 inference(scs_inference,[],[500,2])). % 65.01/65.17 cnf(628,plain, % 65.01/65.17 (P5(f12(a1,f13(a1,a1)),f13(f13(a1,a1),a1))), % 65.01/65.17 inference(scs_inference,[],[335,500,601,616,2,37,36])). % 65.01/65.17 cnf(629,plain, % 65.01/65.17 (~E(f3(a18),f13(f13(a1,a1),a1))), % 65.01/65.17 inference(scs_inference,[],[335,356,615,500,601,616,2,37,36,3])). % 65.01/65.17 cnf(635,plain, % 65.01/65.17 (P1(f13(f5(a15,a15),f5(a15,a15)))), % 65.01/65.17 inference(scs_inference,[],[335,356,615,625,373,500,601,616,2,37,36,3,84,35,265,259])). % 65.01/65.17 cnf(641,plain, % 65.01/65.17 (P5(f13(f5(a15,a15),f5(a15,a15)),f13(f5(a15,a15),f5(a15,a15)))), % 65.01/65.17 inference(scs_inference,[],[335,526,520,356,615,625,373,500,601,617,616,2,37,36,3,84,35,265,259,73,258,75])). % 65.01/65.17 cnf(645,plain, % 65.01/65.17 (E(f13(a17,a17),f13(f12(f13(a17,a17),f13(a17,a17)),f13(a17,a17)))+~P1(f12(f13(a17,a17),f13(a17,a17)))), % 65.01/65.17 inference(scs_inference,[],[335,526,520,356,615,625,373,500,601,617,616,2,37,36,3,84,35,265,259,73,258,75,257,267])). % 65.01/65.17 cnf(647,plain, % 65.01/65.17 (E(a18,f12(a18,f13(a18,a18)))), % 65.01/65.17 inference(scs_inference,[],[524,2])). % 65.01/65.17 cnf(648,plain, % 65.01/65.17 (P3(f3(a18),f12(a18,f13(a18,a18)))), % 65.01/65.17 inference(scs_inference,[],[341,524,2,34])). % 65.01/65.17 cnf(649,plain, % 65.01/65.17 (P3(f12(a18,f13(a18,a18)),f11(a16,a17))), % 65.01/65.17 inference(scs_inference,[],[341,46,524,2,34,33])). % 65.01/65.17 cnf(650,plain, % 65.01/65.17 (P1(f12(a18,f13(a18,a18)))), % 65.01/65.17 inference(scs_inference,[],[42,341,46,524,2,34,33,30])). % 65.01/65.17 cnf(651,plain, % 65.01/65.17 (P2(f12(a18,f13(a18,a18)))), % 65.01/65.17 inference(scs_inference,[],[42,341,46,524,44,2,34,33,30,35])). % 65.01/65.17 cnf(652,plain, % 65.01/65.17 (P5(a15,f12(a18,f13(a18,a18)))), % 65.01/65.17 inference(scs_inference,[],[42,341,46,524,343,44,2,34,33,30,35,37])). % 65.01/65.17 cnf(654,plain, % 65.01/65.17 (~E(a18,f13(f13(a1,a1),f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[338,42,341,46,524,343,488,556,44,2,34,33,30,35,37,36,3])). % 65.01/65.17 cnf(655,plain, % 65.01/65.17 (P5(f12(a18,f13(a18,a18)),f12(a18,f13(a18,a18)))), % 65.01/65.17 inference(scs_inference,[],[338,42,341,46,524,343,488,556,44,2,34,33,30,35,37,36,3,84])). % 65.01/65.17 cnf(662,plain, % 65.01/65.17 (E(f13(a17,a17),f12(f13(a17,a17),f13(f13(a17,a17),f13(a17,a17))))), % 65.01/65.17 inference(scs_inference,[],[558,2])). % 65.01/65.17 cnf(664,plain, % 65.01/65.17 (P3(a18,f11(a18,a2))), % 65.01/65.17 inference(scs_inference,[],[316,649,558,524,2,34,33])). % 65.01/65.17 cnf(665,plain, % 65.01/65.17 (P5(f12(a15,f13(a15,a15)),f12(a18,f13(a18,a18)))), % 65.01/65.17 inference(scs_inference,[],[316,649,647,558,524,394,2,34,33,37])). % 65.01/65.17 cnf(666,plain, % 65.01/65.17 (P5(f13(a1,a1),f13(f13(a1,a1),a1))), % 65.01/65.17 inference(scs_inference,[],[316,530,649,647,558,524,394,628,2,34,33,37,36])). % 65.01/65.17 cnf(667,plain, % 65.01/65.17 (~E(a18,f13(a1,f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[316,530,580,649,654,647,558,524,394,628,2,34,33,37,36,3])). % 65.01/65.17 cnf(668,plain, % 65.01/65.17 (~P3(a1,f12(a18,f13(a18,a18)))), % 65.01/65.17 inference(scs_inference,[],[38,316,530,580,650,649,575,654,647,47,558,524,394,628,651,2,34,33,37,36,3,89])). % 65.01/65.17 cnf(675,plain, % 65.01/65.17 (~P5(a17,a18)+~E(f13(a17,a17),f13(a18,a17))), % 65.01/65.17 inference(scs_inference,[],[39,38,41,316,42,530,355,625,580,626,650,649,575,654,647,47,558,524,394,617,628,651,2,34,33,37,36,3,89,35,257,258,90,105])). % 65.01/65.17 cnf(677,plain, % 65.01/65.17 (E(f13(a18,a18),f12(f13(a18,a18),f13(f13(a18,a18),f13(a18,a18))))), % 65.01/65.17 inference(scs_inference,[],[583,2])). % 65.01/65.17 cnf(678,plain, % 65.01/65.17 (~E(f11(a18,a2),a16)), % 65.01/65.17 inference(scs_inference,[],[52,664,583,2,34])). % 65.01/65.17 cnf(688,plain, % 65.01/65.17 (P5(f13(f13(a1,a1),a1),f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[454,532,616,2,37])). % 65.01/65.17 cnf(689,plain, % 65.01/65.17 (P5(a18,f12(a18,f13(a18,a18)))), % 65.01/65.17 inference(scs_inference,[],[454,524,532,616,655,2,37,36])). % 65.01/65.17 cnf(691,plain, % 65.01/65.17 (~P5(f12(a18,f13(a18,a18)),a15)), % 65.01/65.17 inference(scs_inference,[],[39,42,454,650,678,351,373,524,532,616,655,2,37,36,3,109])). % 65.01/65.17 cnf(707,plain, % 65.01/65.17 (E(a1,f13(f13(a1,a1),f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[556,2])). % 65.01/65.17 cnf(708,plain, % 65.01/65.17 (~E(f12(a18,f13(a18,a18)),a15)), % 65.01/65.17 inference(scs_inference,[],[351,556,689,2,37])). % 65.01/65.17 cnf(719,plain, % 65.01/65.17 (P3(f3(a18),f13(a18,a18))+~P1(f3(a18))), % 65.01/65.17 inference(scs_inference,[],[42,547,648,677,499,404,341,603,689,578,441,2,37,35,3,36,124])). % 65.01/65.17 cnf(721,plain, % 65.01/65.17 (P3(f3(a18),f12(f13(a18,a18),f13(f13(a18,a18),f13(a18,a18))))+~P1(f3(a18))), % 65.01/65.17 inference(scs_inference,[],[42,547,648,677,499,404,341,603,689,578,441,2,37,35,3,36,124,34])). % 65.01/65.17 cnf(724,plain, % 65.01/65.17 (P5(a2,f12(a2,f13(a2,a2)))), % 65.01/65.17 inference(scs_inference,[],[476,447,37])). % 65.01/65.17 cnf(738,plain, % 65.01/65.17 (~E(a17,a18)), % 65.01/65.17 inference(scs_inference,[],[677,51,578,469,37,36])). % 65.01/65.17 cnf(744,plain, % 65.01/65.17 (~E(a16,a18)), % 65.01/65.17 inference(scs_inference,[],[431,50,409,358,37,36])). % 65.01/65.17 cnf(837,plain, % 65.01/65.17 (P5(f13(a1,f13(a1,a1)),a1)), % 65.01/65.17 inference(scs_inference,[],[556,574,37])). % 65.01/65.17 cnf(838,plain, % 65.01/65.17 (P5(a1,f13(a1,f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[556,573,574,37,36])). % 65.01/65.17 cnf(839,plain, % 65.01/65.17 (E(a1,f13(a1,f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[38,572,556,573,574,37,36,96])). % 65.01/65.17 cnf(845,plain, % 65.01/65.17 (~E(f12(a15,f13(a15,a15)),f12(a18,f13(a18,a18)))), % 65.01/65.17 inference(scs_inference,[],[524,416,3])). % 65.01/65.17 cnf(846,plain, % 65.01/65.17 (P5(f13(a1,f13(a1,a1)),f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[454,524,416,837,3,37])). % 65.01/65.17 cnf(847,plain, % 65.01/65.17 (P5(f13(f13(a1,a1),f13(a1,a1)),a1)), % 65.01/65.17 inference(scs_inference,[],[454,580,524,416,837,3,37,36])). % 65.01/65.17 cnf(850,plain, % 65.01/65.17 (~E(a15,f12(a18,f13(a18,a18)))), % 65.01/65.17 inference(scs_inference,[],[39,454,580,650,524,416,652,837,3,37,36,105,22])). % 65.01/65.17 cnf(855,plain, % 65.01/65.17 (P5(f13(a1,f13(a1,a1)),f12(a1,f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[542,846,37])). % 65.01/65.17 cnf(856,plain, % 65.01/65.17 (P5(a1,f13(f13(a1,a1),f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[542,556,504,846,37,36])). % 65.01/65.17 cnf(860,plain, % 65.01/65.17 (P5(f13(f13(a1,a1),f13(a1,a1)),f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[454,847,37])). % 65.01/65.17 cnf(861,plain, % 65.01/65.17 (P5(f13(f13(a1,a1),f13(a1,a1)),f12(a1,f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[454,580,855,847,37,36])). % 65.01/65.17 cnf(865,plain, % 65.01/65.17 (P5(f13(a1,a1),f13(f13(a1,a1),f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[454,856,36])). % 65.01/65.17 cnf(868,plain, % 65.01/65.17 (E(f13(f13(a1,a1),f13(a1,a1)),f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[434,454,484,860,856,36,96,2])). % 65.01/65.17 cnf(874,plain, % 65.01/65.17 (P5(f13(a1,a1),f13(a1,f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[868,573,36])). % 65.01/65.17 cnf(886,plain, % 65.01/65.17 (E(f13(a1,a1),f13(f13(f13(a1,a1),f13(a1,a1)),a1))), % 65.01/65.17 inference(scs_inference,[],[38,434,542,336,484,861,856,865,36,96,111])). % 65.01/65.17 cnf(888,plain, % 65.01/65.17 (E(f13(f13(a1,a1),f13(a1,a1)),f12(a1,f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[38,434,542,336,484,861,856,865,36,96,111,2])). % 65.01/65.17 cnf(899,plain, % 65.01/65.17 (E(f12(a1,f13(a1,a1)),f13(a1,f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[542,336,572,499,855,874,886,441,2,3,35,36,96])). % 65.01/65.17 cnf(901,plain, % 65.01/65.17 (E(f13(a1,a1),f13(f13(a1,f13(a1,a1)),a1))), % 65.01/65.17 inference(scs_inference,[],[38,434,542,336,572,499,855,838,874,886,441,2,3,35,36,96,111])). % 65.01/65.17 cnf(914,plain, % 65.01/65.17 (E(f13(f13(a1,f13(a1,a1)),a1),f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[901,2])). % 65.01/65.17 cnf(959,plain, % 65.01/65.17 (E(f11(a1,a1),a1)), % 65.01/65.17 inference(scs_inference,[],[551,464,56,30])). % 65.01/65.17 cnf(960,plain, % 65.01/65.17 (E(a1,f11(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[959,2])). % 65.01/65.17 cnf(961,plain, % 65.01/65.17 (~E(a18,f11(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[338,959,2,3])). % 65.01/65.17 cnf(962,plain, % 65.01/65.17 (P1(f11(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[38,338,959,2,3,30])). % 65.01/65.17 cnf(963,plain, % 65.01/65.17 (~P2(f11(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[38,338,959,314,2,3,30,35])). % 65.01/65.17 cnf(964,plain, % 65.01/65.17 (P5(f11(a1,a1),f11(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[38,338,959,314,2,3,30,35,84])). % 65.01/65.17 cnf(966,plain, % 65.01/65.17 (P1(f13(f11(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[38,338,959,314,2,3,30,35,84,259])). % 65.01/65.17 cnf(968,plain, % 65.01/65.17 (P3(a1,f11(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[38,338,959,314,2,3,30,35,84,259,257])). % 65.01/65.17 cnf(970,plain, % 65.01/65.17 (P3(a1,a1)), % 65.01/65.17 inference(scs_inference,[],[38,338,959,314,2,3,30,35,84,259,257,94])). % 65.01/65.17 cnf(975,plain, % 65.01/65.17 (P3(f13(a1,a1),f11(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[38,338,454,650,668,959,314,2,3,30,35,84,259,257,94,110,34,33])). % 65.01/65.17 cnf(976,plain, % 65.01/65.17 (P5(f11(a1,a1),a1)), % 65.01/65.17 inference(scs_inference,[],[38,338,454,650,668,959,314,2,3,30,35,84,259,257,94,110,34,33,37])). % 65.01/65.17 cnf(977,plain, % 65.01/65.17 (P5(a1,f11(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[38,338,454,650,668,959,314,2,3,30,35,84,259,257,94,110,34,33,37,36])). % 65.01/65.17 cnf(978,plain, % 65.01/65.17 (E(f12(f11(a1,a1),f13(f11(a1,a1),f11(a1,a1))),f11(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[38,338,454,650,668,959,314,2,3,30,35,84,259,257,94,110,34,33,37,36,265])). % 65.01/65.17 cnf(980,plain, % 65.01/65.17 (P5(f13(f11(a1,a1),f11(a1,a1)),f13(f11(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[38,338,454,650,668,959,314,2,3,30,35,84,259,257,94,110,34,33,37,36,265,75])). % 65.01/65.17 cnf(985,plain, % 65.01/65.17 (E(f11(a1,a1),f12(f11(a1,a1),f13(f11(a1,a1),f11(a1,a1))))), % 65.01/65.17 inference(scs_inference,[],[978,2])). % 65.01/65.17 cnf(986,plain, % 65.01/65.17 (P3(f13(a1,a1),a1)), % 65.01/65.17 inference(scs_inference,[],[975,959,978,2,34])). % 65.01/65.17 cnf(989,plain, % 65.01/65.17 (P1(f12(f11(a1,a1),f13(f11(a1,a1),f11(a1,a1))))), % 65.01/65.17 inference(scs_inference,[],[496,975,962,961,959,978,2,34,33,3,30])). % 65.01/65.17 cnf(991,plain, % 65.01/65.17 (P5(f11(a1,a1),f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[454,496,975,962,961,959,978,963,976,2,34,33,3,30,35,37])). % 65.01/65.17 cnf(992,plain, % 65.01/65.17 (P5(f13(a1,a1),f11(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[454,496,975,962,961,959,978,963,976,977,2,34,33,3,30,35,37,36])). % 65.01/65.17 cnf(993,plain, % 65.01/65.17 (P3(a1,f12(f11(a1,a1),f13(f11(a1,a1),f11(a1,a1))))), % 65.01/65.17 inference(scs_inference,[],[38,454,496,975,962,961,959,978,963,976,977,2,34,33,3,30,35,37,36,94])). % 65.01/65.17 cnf(995,plain, % 65.01/65.17 (E(f13(a1,a1),f11(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[38,434,454,496,975,962,961,959,978,963,976,977,2,34,33,3,30,35,37,36,94,96])). % 65.01/65.17 cnf(997,plain, % 65.01/65.17 (P3(a1,f13(f11(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[38,434,454,496,975,966,962,968,961,959,978,963,976,977,2,34,33,3,30,35,37,36,94,96,124])). % 65.01/65.17 cnf(1005,plain, % 65.01/65.17 (E(f11(a1,a1),f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[995,2])). % 65.01/65.17 cnf(1006,plain, % 65.01/65.17 (P3(f13(a1,a1),f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[454,995,986,2,34])). % 65.01/65.17 cnf(1007,plain, % 65.01/65.17 (P3(f12(a1,f13(a1,a1)),a1)), % 65.01/65.17 inference(scs_inference,[],[454,542,995,986,2,34,33])). % 65.01/65.17 cnf(1010,plain, % 65.01/65.17 (P3(a1,f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[38,434,454,542,995,985,986,964,2,34,33,37,36,94])). % 65.01/65.17 cnf(1012,plain, % 65.01/65.17 (~P3(f13(a1,a1),f12(a18,f13(a18,a18)))), % 65.01/65.17 inference(scs_inference,[],[38,434,454,542,650,668,995,985,986,964,2,34,33,37,36,94,110])). % 65.01/65.17 cnf(1020,plain, % 65.01/65.17 (P5(f11(a1,a1),f12(f13(a1,a1),f13(f13(a1,a1),f13(a1,a1))))), % 65.01/65.17 inference(scs_inference,[],[454,496,993,1006,1012,991,34,33,37])). % 65.01/65.17 cnf(1021,plain, % 65.01/65.17 (P5(f12(f11(a1,a1),f13(f11(a1,a1),f11(a1,a1))),f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[454,496,985,993,1006,1012,991,34,33,37,36])). % 65.01/65.17 cnf(1022,plain, % 65.01/65.17 (P3(f13(a1,a1),f13(f11(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[434,454,496,962,966,985,993,1006,1012,975,991,34,33,37,36,124])). % 65.01/65.17 cnf(1028,plain, % 65.01/65.17 (P3(f12(a1,f13(a1,a1)),f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[542,668,997,1006,34,33])). % 65.01/65.17 cnf(1029,plain, % 65.01/65.17 (P5(f13(a1,a1),f12(f11(a1,a1),f13(f11(a1,a1),f11(a1,a1))))), % 65.01/65.17 inference(scs_inference,[],[542,668,985,997,1006,992,34,33,37])). % 65.01/65.17 cnf(1030,plain, % 65.01/65.17 (P5(f12(a1,f13(a1,a1)),f11(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[542,668,985,997,1006,992,34,33,37,36])). % 65.01/65.17 cnf(1036,plain, % 65.01/65.17 (E(f13(f11(a1,a1),f11(a1,a1)),f13(f13(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[434,42,547,542,668,962,966,985,997,1006,989,1012,992,991,1021,34,33,37,36,96,2,119,111])). % 65.01/65.17 cnf(1038,plain, % 65.01/65.17 (E(x10381,f13(f13(a1,a1),f11(a1,a1)))+~E(x10381,f13(f11(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[434,42,547,542,668,962,966,985,997,1006,989,1012,992,991,1021,34,33,37,36,96,2,119,111,3])). % 65.01/65.17 cnf(1039,plain, % 65.01/65.17 (P1(f13(f13(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[434,42,547,542,668,962,966,985,997,1006,989,1012,992,991,1021,34,33,37,36,96,2,119,111,3,30])). % 65.01/65.17 cnf(1041,plain, % 65.01/65.17 (P5(f13(f13(a1,a1),f11(a1,a1)),f13(f13(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[434,42,547,542,668,962,966,985,997,1006,989,1012,992,991,1021,34,33,37,36,96,2,119,111,3,30,35,84])). % 65.01/65.17 cnf(1047,plain, % 65.01/65.17 (E(f13(f13(a1,a1),f11(a1,a1)),f13(f11(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[1036,2])). % 65.01/65.17 cnf(1048,plain, % 65.01/65.17 (P3(f12(f13(a1,a1),f13(f13(a1,a1),f13(a1,a1))),f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[496,1006,1036,2,33])). % 65.01/65.17 cnf(1050,plain, % 65.01/65.17 (P5(f12(f11(a1,a1),f13(f11(a1,a1),f11(a1,a1))),a1)), % 65.01/65.17 inference(scs_inference,[],[496,985,1006,976,977,1036,2,33,37,36])). % 65.01/65.17 cnf(1051,plain, % 65.01/65.17 (E(f12(f11(a1,a1),f13(f11(a1,a1),f11(a1,a1))),a1)), % 65.01/65.17 inference(scs_inference,[],[38,496,985,1006,989,976,977,1036,2,33,37,36,96])). % 65.01/65.17 cnf(1053,plain, % 65.01/65.17 (E(f13(f11(a1,a1),f11(a1,a1)),f13(a1,f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[38,496,962,966,985,1006,989,976,977,1036,2,33,37,36,96,111])). % 65.01/65.17 cnf(1055,plain, % 65.01/65.17 (E(f13(f13(a1,a1),f11(a1,a1)),f13(a1,f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[38,496,962,966,985,1006,989,976,977,1036,2,33,37,36,96,111,3])). % 65.01/65.17 cnf(1056,plain, % 65.01/65.17 (P1(f13(a1,f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[38,496,962,966,985,1006,989,976,977,1036,2,33,37,36,96,111,3,30])). % 65.01/65.17 cnf(1058,plain, % 65.01/65.17 (E(f13(f11(a1,a1),f11(a1,a1)),a1)), % 65.01/65.17 inference(scs_inference,[],[38,496,962,966,985,1006,989,976,977,1036,2,33,37,36,96,111,3,30,35,78])). % 65.01/65.17 cnf(1060,plain, % 65.01/65.17 (P5(f13(a1,f11(a1,a1)),f13(a1,f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[38,496,962,966,985,1006,989,976,977,1036,2,33,37,36,96,111,3,30,35,78,84])). % 65.01/65.17 cnf(1065,plain, % 65.01/65.17 (E(f13(a1,f11(a1,a1)),f13(f13(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[1055,2])). % 65.01/65.17 cnf(1066,plain, % 65.01/65.17 (~P2(f13(f11(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[966,1055,1058,2,54])). % 65.01/65.17 cnf(1069,plain, % 65.01/65.17 (~E(a18,f13(f11(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[338,496,966,986,1055,1058,2,54,33,3])). % 65.01/65.17 cnf(1070,plain, % 65.01/65.17 (~P2(f13(f13(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[338,496,966,986,1047,1055,1058,2,54,33,3,35])). % 65.01/65.17 cnf(1071,plain, % 65.01/65.17 (P5(f13(f13(a1,a1),f11(a1,a1)),f13(f11(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[338,496,966,986,1047,1055,1041,1058,2,54,33,3,35,37])). % 65.01/65.17 cnf(1075,plain, % 65.01/65.17 (E(f13(f13(a1,a1),f13(a1,a1)),f13(f11(a1,a1),f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[434,338,496,484,962,966,986,1047,1055,464,992,1041,1020,1058,2,54,33,3,35,37,36,96,111])). % 65.01/65.17 cnf(1077,plain, % 65.01/65.17 (P1(f13(f11(a1,a1),f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[434,338,496,484,962,966,986,1047,1055,464,992,1041,1020,1058,2,54,33,3,35,37,36,96,111,30])). % 65.01/65.17 cnf(1078,plain, % 65.01/65.17 (P5(f13(f11(a1,a1),f13(a1,a1)),f13(f11(a1,a1),f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[434,338,496,484,962,966,986,1047,1055,464,992,1041,1020,1058,2,54,33,3,35,37,36,96,111,30,84])). % 65.01/65.17 cnf(1080,plain, % 65.01/65.17 (P3(a1,f12(f13(a1,a1),f13(f13(a1,a1),f13(a1,a1))))), % 65.01/65.17 inference(scs_inference,[],[38,434,338,496,484,962,966,986,1047,1055,464,992,1041,1020,1058,2,54,33,3,35,37,36,96,111,30,84,94])). % 65.01/65.17 cnf(1082,plain, % 65.01/65.17 (P3(a1,f13(f13(a1,a1),f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[38,434,338,496,484,962,966,1010,986,1047,1055,464,992,1041,1020,1058,2,54,33,3,35,37,36,96,111,30,84,94,124])). % 65.01/65.17 cnf(1091,plain, % 65.01/65.17 (P3(f12(a1,f13(a1,a1)),f12(a1,f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[542,975,1051,1028,2,33,34])). % 65.01/65.17 cnf(1092,plain, % 65.01/65.17 (~E(a18,f13(f13(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[542,975,1051,1047,1028,1069,2,33,34,3])). % 65.01/65.17 cnf(1094,plain, % 65.01/65.17 (P5(f11(a1,a1),f12(a1,f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[542,975,1051,1047,1028,1065,1069,991,1070,2,33,34,3,35,37])). % 65.01/65.17 cnf(1095,plain, % 65.01/65.17 (P5(f13(a1,f11(a1,a1)),f13(f11(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[542,975,1051,1055,1047,1028,1065,1069,991,1070,1071,2,33,34,3,35,37,36])). % 65.01/65.17 cnf(1103,plain, % 65.01/65.17 (E(f13(a1,f11(a1,a1)),f13(f11(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[1053,2])). % 65.01/65.17 cnf(1106,plain, % 65.01/65.17 (P5(f13(f11(a1,a1),f11(a1,a1)),f13(f13(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[454,1065,1080,1092,1036,1053,980,2,33,3,37])). % 65.01/65.17 cnf(1108,plain, % 65.01/65.17 (E(f12(a1,f13(a1,a1)),f11(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[454,336,962,1065,1080,1092,1036,1053,980,1094,1030,1060,2,33,3,37,36,96])). % 65.01/65.17 cnf(1112,plain, % 65.01/65.17 (E(f13(a1,a1),f13(f11(a1,a1),a1))), % 65.01/65.17 inference(scs_inference,[],[434,38,454,336,484,962,1006,1065,1080,1092,1036,1053,977,980,1094,1030,1060,2,33,3,37,36,96,124,111])). % 65.01/65.17 cnf(1114,plain, % 65.01/65.17 (P1(f13(f11(a1,a1),a1))), % 65.01/65.17 inference(scs_inference,[],[434,38,454,336,484,962,1006,1065,1080,1092,1036,1053,977,980,1094,1030,1060,2,33,3,37,36,96,124,111,30])). % 65.01/65.17 cnf(1115,plain, % 65.01/65.17 (P5(f13(f11(a1,a1),a1),f13(f11(a1,a1),a1))), % 65.01/65.17 inference(scs_inference,[],[434,38,454,336,484,962,1006,1065,1080,1092,1036,1053,977,980,1094,1030,1060,2,33,3,37,36,96,124,111,30,84])). % 65.01/65.17 cnf(1117,plain, % 65.01/65.17 (P3(a1,f12(a1,f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[434,38,454,336,484,962,1006,1065,1080,1092,1036,1053,977,980,1094,1030,1060,2,33,3,37,36,96,124,111,30,84,94])). % 65.01/65.17 cnf(1121,plain, % 65.01/65.17 (~E(f12(a1,f13(a1,a1)),f12(a18,f13(a18,a18)))), % 65.01/65.17 inference(scs_inference,[],[39,434,38,454,336,484,962,668,1006,1065,1080,1048,1092,464,1036,1053,977,980,1094,1030,1060,2,33,3,37,36,96,124,111,30,84,94,110,34])). % 65.01/65.17 cnf(1125,plain, % 65.01/65.17 (E(f11(a1,a1),f12(a1,f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[1108,2])). % 65.01/65.17 cnf(1126,plain, % 65.01/65.17 (P3(f13(a1,a1),f12(a1,f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[530,1091,1108,2,33])). % 65.01/65.17 cnf(1127,plain, % 65.01/65.17 (E(f13(a1,f13(a1,a1)),f13(f11(a1,a1),f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[530,580,1091,1108,1075,2,33,3])). % 65.01/65.17 cnf(1128,plain, % 65.01/65.17 (P5(f13(f11(a1,a1),f11(a1,a1)),f13(a1,f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[530,580,1055,1091,1108,1075,1106,2,33,3,37])). % 65.01/65.17 cnf(1135,plain, % 65.01/65.17 (E(f13(f11(a1,a1),f13(a1,a1)),f13(a1,f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[1127,2])). % 65.01/65.17 cnf(1136,plain, % 65.01/65.17 (E(f12(a1,f13(a1,a1)),f13(f11(a1,a1),f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[899,1127,2,3])). % 65.01/65.17 cnf(1137,plain, % 65.01/65.17 (~P2(f13(f11(a1,a1),f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[899,1127,593,2,3,35])). % 65.01/65.17 cnf(1138,plain, % 65.01/65.17 (P5(f13(f11(a1,a1),f13(a1,a1)),f13(a1,f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[899,1127,1078,593,2,3,35,37])). % 65.01/65.17 cnf(1139,plain, % 65.01/65.17 (P5(f13(a1,f13(a1,a1)),f13(f11(a1,a1),f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[899,1127,1078,593,2,3,35,37,36])). % 65.01/65.17 cnf(1140,plain, % 65.01/65.17 (P5(a1,f13(f11(a1,a1),f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[434,38,899,1077,1127,1078,593,2,3,35,37,36,95])). % 65.01/65.17 cnf(1142,plain, % 65.01/65.17 (E(f13(a1,a1),f13(f13(f11(a1,a1),f13(a1,a1)),a1))), % 65.01/65.17 inference(scs_inference,[],[434,38,899,1077,1127,1078,593,2,3,35,37,36,95,111])). % 65.01/65.17 cnf(1148,plain, % 65.01/65.17 (E(f13(f11(a1,a1),f13(a1,a1)),f12(a1,f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[1136,2])). % 65.01/65.17 cnf(1149,plain, % 65.01/65.17 (E(a1,f13(f11(a1,a1),f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[335,1136,2,3])). % 65.01/65.17 cnf(1152,plain, % 65.01/65.17 (E(f13(f11(a1,a1),f13(a1,a1)),f13(f13(a1,a1),f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[580,335,484,1077,1136,1138,1139,2,3,37,36,96])). % 65.01/65.17 cnf(1159,plain, % 65.01/65.17 (E(f13(f11(a1,a1),f13(a1,a1)),a1)), % 65.01/65.17 inference(scs_inference,[],[1149,2])). % 65.01/65.17 cnf(1161,plain, % 65.01/65.17 (P5(f13(f11(a1,a1),f13(a1,a1)),f12(a1,f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[334,1148,1149,1078,2,3,37])). % 65.01/65.17 cnf(1168,plain, % 65.01/65.17 (E(a1,f13(f11(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[1058,2])). % 65.01/65.17 cnf(1169,plain, % 65.01/65.17 (E(f12(a1,f13(a1,a1)),f13(f11(a1,a1),a1))), % 65.01/65.17 inference(scs_inference,[],[530,1058,1112,2,3])). % 65.01/65.17 cnf(1170,plain, % 65.01/65.17 (P5(f13(a1,f11(a1,a1)),a1)), % 65.01/65.17 inference(scs_inference,[],[530,1058,1112,1095,2,3,37])). % 65.01/65.17 cnf(1171,plain, % 65.01/65.17 (P5(f13(a1,a1),f13(f11(a1,a1),f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[530,454,1058,1112,1095,1140,2,3,37,36])). % 65.01/65.17 cnf(1172,plain, % 65.01/65.17 (P5(a1,f13(f11(a1,a1),a1))), % 65.01/65.17 inference(scs_inference,[],[434,38,530,454,1114,1058,1112,1095,1140,2,3,37,36,95])). % 65.01/65.17 cnf(1174,plain, % 65.01/65.17 (E(f13(a1,a1),f13(f13(f11(a1,a1),a1),a1))), % 65.01/65.17 inference(scs_inference,[],[434,38,530,454,1114,1058,1112,1095,1140,2,3,37,36,95,111])). % 65.01/65.17 cnf(1182,plain, % 65.01/65.17 (E(f13(f11(a1,a1),a1),f12(a1,f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[1169,2])). % 65.01/65.17 cnf(1183,plain, % 65.01/65.17 (E(a1,f13(f11(a1,a1),a1))), % 65.01/65.17 inference(scs_inference,[],[335,1169,2,3])). % 65.01/65.17 cnf(1185,plain, % 65.01/65.17 (P5(f13(f13(a1,a1),f11(a1,a1)),a1)), % 65.01/65.17 inference(scs_inference,[],[335,1169,1058,1071,339,2,3,35,37])). % 65.01/65.17 cnf(1186,plain, % 65.01/65.17 (P5(a1,f13(f13(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[335,1169,1058,1106,1071,339,2,3,35,37,36])). % 65.01/65.17 cnf(1187,plain, % 65.01/65.17 (E(a1,f13(f13(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[38,335,1039,1169,1058,1106,1071,339,2,3,35,37,36,96])). % 65.01/65.17 cnf(1192,plain, % 65.01/65.17 (E(f13(f11(a1,a1),a1),a1)), % 65.01/65.17 inference(scs_inference,[],[1183,2])). % 65.01/65.17 cnf(1194,plain, % 65.01/65.17 (P5(f13(f11(a1,a1),f13(a1,a1)),a1)), % 65.01/65.17 inference(scs_inference,[],[1159,1182,1183,334,1078,2,3,37])). % 65.01/65.17 cnf(1195,plain, % 65.01/65.17 (P5(f12(a1,f13(a1,a1)),f13(f11(a1,a1),a1))), % 65.01/65.17 inference(scs_inference,[],[1159,1182,1183,334,1078,1115,2,3,37,36])). % 65.01/65.17 cnf(1201,plain, % 65.01/65.17 (E(f13(f11(a1,a1),a1),f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[1112,2])). % 65.01/65.17 cnf(1202,plain, % 65.01/65.17 (~E(f3(a18),f11(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[1125,356,1112,2,3])). % 65.01/65.17 cnf(1205,plain, % 65.01/65.17 (E(f13(f11(a1,a1),f13(a1,a1)),f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[434,530,1077,1125,356,1112,1161,1171,1195,2,3,37,36,96])). % 65.01/65.17 cnf(1212,plain, % 65.01/65.17 (P5(f13(a1,f11(a1,a1)),f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[454,1205,1202,978,1170,2,3,37])). % 65.01/65.17 cnf(1213,plain, % 65.01/65.17 (P5(a1,f13(a1,f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[454,1205,1202,978,1058,1128,1170,2,3,37,36])). % 65.01/65.17 cnf(1214,plain, % 65.01/65.17 (E(a1,f13(a1,f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[38,454,1056,1205,1202,978,1058,1128,1170,2,3,37,36,96])). % 65.01/65.17 cnf(1220,plain, % 65.01/65.17 (P5(f13(f11(a1,a1),f11(a1,a1)),a1)), % 65.01/65.17 inference(scs_inference,[],[1214,1058,980,2,37])). % 65.01/65.17 cnf(1221,plain, % 65.01/65.17 (P5(f13(f13(a1,a1),f11(a1,a1)),f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[1065,1214,1058,1212,980,2,37,36])). % 65.01/65.17 cnf(1225,plain, % 65.01/65.17 (E(f13(f13(f11(a1,a1),f13(a1,a1)),a1),f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[1142,2])). % 65.01/65.17 cnf(1228,plain, % 65.01/65.17 (P5(f13(f11(a1,a1),f11(a1,a1)),f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[454,499,1142,1220,441,2,3,35,37])). % 65.01/65.17 cnf(1229,plain, % 65.01/65.17 (P5(f13(a1,a1),f13(f13(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[454,499,1142,1220,1186,441,2,3,35,37,36])). % 65.01/65.17 cnf(1230,plain, % 65.01/65.17 (E(f13(a1,a1),f13(f13(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[434,454,1039,499,1142,1221,1220,1186,441,2,3,35,37,36,96])). % 65.01/65.17 cnf(1235,plain, % 65.01/65.17 (E(f13(f13(a1,a1),f11(a1,a1)),f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[1230,2])). % 65.01/65.17 cnf(1238,plain, % 65.01/65.17 (P5(f13(a1,a1),f13(a1,f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[647,454,1121,1047,1230,1229,1213,2,3,37,36])). % 65.01/65.17 cnf(1239,plain, % 65.01/65.17 (E(f13(a1,a1),f13(f11(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[434,647,454,966,1121,1047,1230,1228,1229,1213,2,3,37,36,96])). % 65.01/65.17 cnf(1247,plain, % 65.01/65.17 (E(f13(f11(a1,a1),f11(a1,a1)),f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[1239,2])). % 65.01/65.17 cnf(1249,plain, % 65.01/65.17 (P5(f13(f11(a1,a1),a1),a1)), % 65.01/65.17 inference(scs_inference,[],[914,1192,1239,444,1115,2,3,37])). % 65.01/65.17 cnf(1250,plain, % 65.01/65.17 (P5(a1,f13(f11(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[914,1192,1239,444,1058,1115,980,2,3,37,36])). % 65.01/65.17 cnf(1256,plain, % 65.01/65.17 (E(f13(f13(f11(a1,a1),a1),a1),f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[1174,2])). % 65.01/65.17 cnf(1297,plain, % 65.01/65.17 (E(f11(f12(a15,a15),a1),a1)), % 65.01/65.17 inference(scs_inference,[],[39,57,85])). % 65.01/65.17 cnf(1300,plain, % 65.01/65.17 (P1(f11(f12(a15,a15),a1))), % 65.01/65.17 inference(scs_inference,[],[38,338,1297,2,3,30])). % 65.01/65.17 cnf(1304,plain, % 65.01/65.17 (P5(f11(f12(a15,a15),a1),a1)), % 65.01/65.17 inference(scs_inference,[],[38,338,1297,314,2,3,30,35,84,37])). % 65.01/65.17 cnf(1305,plain, % 65.01/65.17 (P5(a1,f11(f12(a15,a15),a1))), % 65.01/65.17 inference(scs_inference,[],[38,338,1297,314,2,3,30,35,84,37,36])). % 65.01/65.17 cnf(1311,plain, % 65.01/65.17 (P5(f11(f12(a15,a15),a1),f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[454,1304,37])). % 65.01/65.17 cnf(1313,plain, % 65.01/65.17 (E(f13(a1,a1),f11(f12(a15,a15),a1))), % 65.01/65.17 inference(scs_inference,[],[434,454,1300,1304,1305,37,36,96])). % 65.01/65.17 cnf(1391,plain, % 65.01/65.17 (~E(f11(a18,a2),a17)), % 65.01/65.17 inference(scs_inference,[],[53,664,34])). % 65.01/65.17 cnf(1398,plain, % 65.01/65.17 (~E(f11(a16,a17),a17)), % 65.01/65.17 inference(scs_inference,[],[53,46,34])). % 65.01/65.17 cnf(1555,plain, % 65.01/65.17 (E(f12(a1,f12(a18,f13(a18,a18))),f12(a18,f13(a18,a18)))), % 65.01/65.17 inference(scs_inference,[],[647,42,58,30])). % 65.01/65.17 cnf(1793,plain, % 65.01/65.17 (E(f13(a1,a1),f13(f11(f12(a15,a15),a1),a1))), % 65.01/65.17 inference(scs_inference,[],[38,434,1313,336,986,1300,522,497,1305,33,36,37,96,111])). % 65.01/65.17 cnf(1796,plain, % 65.01/65.17 (P3(f11(f12(a15,a15),a1),f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[38,434,454,1313,336,986,1300,522,497,1305,33,36,37,96,111,2,34])). % 65.01/65.17 cnf(1808,plain, % 65.01/65.17 (E(f13(f13(a1,a1),a1),f11(f12(a15,a15),a1))), % 65.01/65.17 inference(scs_inference,[],[1313,543,975,1300,1796,499,688,666,1793,441,2,3,34,33,35,36,37,96])). % 65.01/65.17 cnf(1818,plain, % 65.01/65.17 (E(f11(a1,a1),f11(f12(a15,a15),a1))), % 65.01/65.17 inference(scs_inference,[],[962,1313,1205,1300,1126,1808,444,992,991,2,3,33,36,37,96])). % 65.01/65.17 cnf(1828,plain, % 65.01/65.17 (P3(a1,f11(f12(a15,a15),a1))), % 65.01/65.17 inference(scs_inference,[],[38,1313,1300,1022,1818,846,865,2,33,36,37,94])). % 65.01/65.17 cnf(1901,plain, % 65.01/65.17 (~E(f11(a18,f11(a1,a1)),a17)), % 65.01/65.17 inference(scs_inference,[],[38,70,86])). % 65.01/65.17 cnf(1903,plain, % 65.01/65.17 (P3(f11(a1,a1),f12(a1,f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[1901,960,1117,482,3,33])). % 65.01/65.17 cnf(1909,plain, % 65.01/65.17 (P3(a1,f13(f13(a1,a1),a1))), % 65.01/65.17 inference(scs_inference,[],[38,1901,960,962,543,1117,601,616,482,3,33,37,36,96,2,94])). % 65.01/65.17 cnf(1921,plain, % 65.01/65.17 (P5(f11(a1,a1),f13(a1,f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[960,970,668,1909,847,838,34,33,37,36])). % 65.01/65.17 cnf(1922,plain, % 65.01/65.17 (P3(f11(a1,a1),f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[38,960,962,970,434,668,1903,1909,847,838,34,33,37,36,124])). % 65.01/65.17 cnf(1927,plain, % 65.01/65.17 (P3(f11(a1,a1),f11(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[960,968,33])). % 65.01/65.17 cnf(1928,plain, % 65.01/65.17 (P5(f13(a1,f13(a1,a1)),f11(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[960,968,837,33,37])). % 65.01/65.17 cnf(1939,plain, % 65.01/65.17 (P5(f13(f11(a1,a1),f13(a1,a1)),f11(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[960,997,1194,33,37])). % 65.01/65.17 cnf(1940,plain, % 65.01/65.17 (P5(f11(a1,a1),f13(f11(a1,a1),f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[960,997,1140,1194,33,37,36])). % 65.01/65.17 cnf(1943,plain, % 65.01/65.17 (P3(a1,f13(a1,f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[38,960,962,572,997,1140,1194,1921,1928,33,37,36,96,94])). % 65.01/65.17 cnf(1955,plain, % 65.01/65.17 (P5(f11(a1,a1),f13(f11(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[960,1082,1250,1185,33,37,36])). % 65.01/65.17 cnf(1959,plain, % 65.01/65.17 (P3(a1,f13(f11(a1,a1),f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[38,960,962,1082,1077,1250,1185,1939,1940,33,37,36,96,2,94])). % 65.01/65.17 cnf(1974,plain, % 65.01/65.17 (E(f13(a1,a1),f13(f13(f11(a1,a1),f11(a1,a1)),a1))), % 65.01/65.17 inference(scs_inference,[],[38,1168,336,1117,966,434,340,337,1250,33,37,36,96,2,111])). % 65.01/65.17 cnf(1978,plain, % 65.01/65.17 (P1(f13(f13(f11(a1,a1),f11(a1,a1)),a1))), % 65.01/65.17 inference(scs_inference,[],[38,1168,336,369,1117,966,434,42,340,337,394,1250,33,37,36,96,2,111,109,30])). % 65.01/65.17 cnf(1982,plain, % 65.01/65.17 (E(f13(f13(f11(a1,a1),f11(a1,a1)),a1),f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[1974,2])). % 65.01/65.17 cnf(1988,plain, % 65.01/65.17 (E(f13(f13(a1,a1),f11(a1,a1)),f12(a1,f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[1187,336,1117,1039,499,340,337,1974,441,2,3,35,33,37,36,96])). % 65.01/65.17 cnf(1990,plain, % 65.01/65.17 (P3(f13(f13(a1,a1),f11(a1,a1)),a1)), % 65.01/65.17 inference(scs_inference,[],[38,1187,336,1117,1039,1007,499,340,337,1974,441,2,3,35,33,37,36,96,110])). % 65.01/65.17 cnf(1992,plain, % 65.01/65.17 (P3(f13(f13(a1,a1),f11(a1,a1)),f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[38,1187,336,1117,1039,1007,434,499,340,337,1974,441,2,3,35,33,37,36,96,110,124])). % 65.01/65.17 cnf(2002,plain, % 65.01/65.17 (P3(f13(f11(a1,a1),f13(a1,a1)),f12(a1,f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[1149,995,1225,1117,1992,1988,444,2,3,34,33])). % 65.01/65.17 cnf(2003,plain, % 65.01/65.17 (P5(f13(f13(a1,a1),a1),f13(f11(a1,a1),f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[1149,995,1225,1117,1992,1988,444,616,2,3,34,33,37])). % 65.01/65.17 cnf(2004,plain, % 65.01/65.17 (P5(f13(f11(a1,a1),f13(a1,a1)),f13(f13(a1,a1),a1))), % 65.01/65.17 inference(scs_inference,[],[1149,995,1225,1117,1992,1988,444,601,616,2,3,34,33,37,36])). % 65.01/65.17 cnf(2005,plain, % 65.01/65.17 (E(f13(f11(a1,a1),f13(a1,a1)),f13(f13(a1,a1),a1))), % 65.01/65.17 inference(scs_inference,[],[1149,995,1225,543,1117,1077,1992,1988,444,601,616,2,3,34,33,37,36,96])). % 65.01/65.17 cnf(2007,plain, % 65.01/65.17 (E(f13(a1,a1),f13(f13(f13(a1,a1),f11(a1,a1)),a1))), % 65.01/65.17 inference(scs_inference,[],[38,1149,995,1225,543,1117,1039,1077,434,1992,1988,444,601,616,1186,2,3,34,33,37,36,96,111])). % 65.01/65.17 cnf(2018,plain, % 65.01/65.17 (P3(f13(f11(a1,a1),a1),a1)), % 65.01/65.17 inference(scs_inference,[],[38,1183,336,1117,1007,1114,2005,1990,337,616,2,34,33,37,36,110])). % 65.01/65.17 cnf(2020,plain, % 65.01/65.17 (P3(f13(f11(a1,a1),a1),f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[38,1183,336,1117,1007,1114,434,2005,1990,337,616,2,34,33,37,36,110,124])). % 65.01/65.17 cnf(2032,plain, % 65.01/65.17 (E(f13(f11(a1,a1),f11(a1,a1)),f13(f13(a1,a1),a1))), % 65.01/65.17 inference(scs_inference,[],[1168,995,543,966,970,2020,499,601,616,2007,441,2,3,35,34,33,37,36,96])). % 65.01/65.17 cnf(2041,plain, % 65.01/65.17 (P3(f13(f11(a1,a1),a1),f13(f11(a1,a1),f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[1149,1235,2032,2018,444,2,3,34])). % 65.01/65.17 cnf(2045,plain, % 65.01/65.17 (E(f13(f11(a1,a1),f13(a1,a1)),f13(f11(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[1149,1235,966,1077,1010,2032,2018,444,1250,1220,2,3,34,33,37,36,96])). % 65.01/65.17 cnf(2047,plain, % 65.01/65.17 (~E(f3(a18),f13(f11(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[1149,1235,966,1077,1010,2032,2018,444,1250,1220,2,3,34,33,37,36,96,1038])). % 65.01/65.17 cnf(2058,plain, % 65.01/65.17 (E(f13(f13(a1,a1),f11(a1,a1)),f13(f13(a1,a1),a1))), % 65.01/65.17 inference(scs_inference,[],[1103,1187,543,1039,997,2018,2045,2047,601,616,2,3,34,33,37,36,96])). % 65.01/65.17 cnf(2064,plain, % 65.01/65.17 (P3(f13(f11(a1,a1),a1),f13(a1,f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[1135,2041,2058,2,34])). % 65.01/65.17 cnf(2142,plain, % 65.01/65.17 (P5(f13(a1,f11(a1,a1)),f13(f11(a1,a1),f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[1149,968,1170,33,37])). % 65.01/65.17 cnf(2143,plain, % 65.01/65.17 (P5(f13(f11(a1,a1),f13(a1,a1)),f13(a1,f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[1149,968,1213,1170,33,37,36])). % 65.01/65.17 cnf(2151,plain, % 65.01/65.17 (P5(f13(f11(a1,a1),a1),f13(f11(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[1168,1082,1249,33,37])). % 65.01/65.17 cnf(2155,plain, % 65.01/65.17 (E(f11(a1,a1),f13(f11(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[962,1168,966,1082,977,1249,1955,33,37,36,96,2])). % 65.01/65.17 cnf(2161,plain, % 65.01/65.17 (P5(f13(f11(a1,a1),a1),f11(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[1183,1828,977,1185,33,37,36])). % 65.01/65.17 cnf(2189,plain, % 65.01/65.17 (P3(f13(f11(a1,a1),f13(a1,a1)),f13(f11(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[1149,997,33])). % 65.01/65.17 cnf(2190,plain, % 65.01/65.17 (P5(f13(a1,f11(a1,a1)),f11(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[1149,995,997,1212,33,37])). % 65.01/65.17 cnf(2203,plain, % 65.01/65.17 (E(f13(f11(a1,a1),a1),f13(f11(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[1152,1168,966,1114,1828,1172,2003,2151,33,37,36,96,2])). % 65.01/65.17 cnf(2218,plain, % 65.01/65.17 (P5(f11(a1,a1),f13(a1,f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[1152,1187,995,2002,1249,1238,33,37,36])). % 65.01/65.17 cnf(2230,plain, % 65.01/65.17 (E(f13(a1,f11(a1,a1)),f11(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[962,1135,1149,1056,1082,2004,2003,2190,2218,33,37,36,96,2])). % 65.01/65.17 cnf(2233,plain, % 65.01/65.17 (~P3(f13(a1,f11(a1,a1)),f12(a18,f13(a18,a18)))), % 65.01/65.17 inference(scs_inference,[],[38,962,1135,1149,650,1056,1082,668,2004,2003,2190,2218,33,37,36,96,2,94,110])). % 65.01/65.17 cnf(2241,plain, % 65.01/65.17 (P3(f13(f11(a1,a1),f11(a1,a1)),f13(f13(a1,a1),a1))), % 65.01/65.17 inference(scs_inference,[],[1168,1909,33])). % 65.01/65.17 cnf(2242,plain, % 65.01/65.17 (P5(f13(a1,f11(a1,a1)),f13(f13(a1,a1),f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[1152,1168,1909,2142,33,37])). % 65.01/65.17 cnf(2243,plain, % 65.01/65.17 (P5(f13(f13(a1,a1),f13(a1,a1)),f13(f13(a1,a1),a1))), % 65.01/65.17 inference(scs_inference,[],[1152,1168,1909,2004,2142,33,37,36])). % 65.01/65.17 cnf(2260,plain, % 65.01/65.17 (P5(f13(a1,f11(a1,a1)),f12(a1,f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[1149,888,1828,2242,33,37])). % 65.01/65.17 cnf(2261,plain, % 65.01/65.17 (P5(f13(f13(a1,a1),f13(a1,a1)),f13(a1,f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[1152,1149,888,1828,2143,2242,33,37,36])). % 65.01/65.17 cnf(2269,plain, % 65.01/65.17 (P5(f12(a1,f13(a1,a1)),f13(a1,f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[888,985,1922,2261,33,36])). % 65.01/65.17 cnf(2279,plain, % 65.01/65.17 (P3(f13(a1,a1),f13(a1,f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[1201,2064,33])). % 65.01/65.17 cnf(2282,plain, % 65.01/65.17 (E(f13(a1,a1),f13(f13(a1,f11(a1,a1)),a1))), % 65.01/65.17 inference(scs_inference,[],[38,1201,336,434,1056,2064,1213,2260,2269,33,96,111])). % 65.01/65.17 cnf(2289,plain, % 65.01/65.17 (E(f13(f13(a1,f11(a1,a1)),a1),f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[2282,2])). % 65.01/65.17 cnf(2293,plain, % 65.01/65.17 (E(f13(f13(a1,a1),f13(a1,a1)),f13(a1,f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[1168,484,1056,1943,499,2282,2242,2261,441,2,3,35,33,96])). % 65.01/65.17 cnf(2298,plain, % 65.01/65.17 (E(f13(a1,f11(a1,a1)),f13(f13(a1,a1),f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[2293,2])). % 65.01/65.17 cnf(2299,plain, % 65.01/65.17 (~E(f3(a18),f13(f13(f11(a1,a1),a1),a1))), % 65.01/65.17 inference(scs_inference,[],[1256,2293,444,2,3])). % 65.01/65.17 cnf(2370,plain, % 65.01/65.17 (P3(f13(f11(a1,a1),f11(a1,a1)),f13(f11(a1,a1),f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[1168,1959,33])). % 65.01/65.17 cnf(2379,plain, % 65.01/65.17 (P3(f13(a1,a1),f13(f13(a1,a1),a1))), % 65.01/65.17 inference(scs_inference,[],[1247,2241,33])). % 65.01/65.17 cnf(2388,plain, % 65.01/65.17 (P3(f11(a1,a1),f13(a1,f13(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[995,2279,33])). % 65.01/65.17 cnf(2449,plain, % 65.01/65.17 (~E(f12(a18,f13(a18,a18)),a1)), % 65.01/65.17 inference(scs_inference,[],[1391,2230,651,635,650,58,59,60,61,56,57,69,70,71,72,26,29,4,5,6,7,20,21,23,24,25,27,28,8,9,10,11,12,13,14,15,16,17,18,19,1038,22,2,85,86,54])). % 65.01/65.17 cnf(2461,plain, % 65.01/65.17 (P1(f3(a18))), % 65.01/65.17 inference(scs_inference,[],[1391,618,691,2379,1137,1555,2233,2289,2230,839,1050,1012,651,647,635,641,543,49,338,434,42,650,58,59,60,61,56,57,69,70,71,72,26,29,4,5,6,7,20,21,23,24,25,27,28,8,9,10,11,12,13,14,15,16,17,18,19,1038,22,2,85,86,54,3,35,34,36,37,33,99,100,62])). % 65.01/65.17 cnf(2463,plain, % 65.01/65.17 (P2(f3(a18))), % 65.01/65.17 inference(scs_inference,[],[1391,618,691,2379,1137,1555,2233,2289,2230,839,1050,1012,651,647,635,641,543,49,338,434,42,650,58,59,60,61,56,57,69,70,71,72,26,29,4,5,6,7,20,21,23,24,25,27,28,8,9,10,11,12,13,14,15,16,17,18,19,1038,22,2,85,86,54,3,35,34,36,37,33,99,100,62,63])). % 65.01/65.17 cnf(2483,plain, % 65.01/65.17 (P5(a17,a18)), % 65.01/65.17 inference(scs_inference,[],[1391,618,691,2379,1137,1555,2233,1927,2289,2230,1982,839,1978,1050,51,1012,964,651,647,635,641,43,41,543,49,338,962,434,355,42,650,58,59,60,61,56,57,69,70,71,72,26,29,4,5,6,7,20,21,23,24,25,27,28,8,9,10,11,12,13,14,15,16,17,18,19,1038,22,2,85,86,54,3,35,34,36,37,33,99,100,62,63,107,108,117,118,126,127,78,75,259,84])). % 65.01/65.17 cnf(2489,plain, % 65.01/65.17 (E(f12(f13(a1,a1),f13(a1,f11(a1,a1))),f13(a1,a1))), % 65.01/65.17 inference(scs_inference,[],[1391,618,691,2379,1137,1555,2233,1927,2298,2289,2230,845,1982,839,1978,1050,51,1012,665,964,651,459,647,635,641,43,41,543,369,49,338,962,434,355,42,650,58,59,60,61,56,57,69,70,71,72,26,29,4,5,6,7,20,21,23,24,25,27,28,8,9,10,11,12,13,14,15,16,17,18,19,1038,22,2,85,86,54,3,35,34,36,37,33,99,100,62,63,107,108,117,118,126,127,78,75,259,84,91,81,105])). % 65.01/65.17 cnf(2507,plain, % 65.01/65.17 (P5(f3(a18),f3(a18))), % 65.01/65.17 inference(scs_inference,[],[52,1391,618,691,2379,1137,1555,2161,2233,1927,2298,2289,2230,845,1982,839,1978,648,1050,51,1012,665,44,964,724,53,651,459,647,635,641,480,477,46,457,43,41,40,1114,543,369,49,338,962,434,355,42,650,38,58,59,60,61,56,57,69,70,71,72,26,29,4,5,6,7,20,21,23,24,25,27,28,8,9,10,11,12,13,14,15,16,17,18,19,1038,22,2,85,86,54,3,35,34,36,37,33,99,100,62,63,107,108,117,118,126,127,78,75,259,84,91,81,105,97,90,267,103,104,111,119,129,64])). % 65.01/65.17 cnf(2533,plain, % 65.01/65.17 (~P5(a16,a18)+E(a18,a17)+E(a18,a16)), % 65.01/65.17 inference(scs_inference,[],[2483,77])). % 65.01/65.17 cnf(2536,plain, % 65.01/65.17 (P5(f3(a18),a18)), % 65.01/65.17 inference(scs_inference,[],[2461,494])). % 65.01/65.17 cnf(2539,plain, % 65.01/65.17 (~E(f13(a17,a17),f13(a18,a17))), % 65.01/65.17 inference(scs_inference,[],[2483,675])). % 65.01/65.17 cnf(2540,plain, % 65.01/65.17 (P3(f3(a18),f13(a18,a18))), % 65.01/65.17 inference(scs_inference,[],[2461,719])). % 65.01/65.17 cnf(2541,plain, % 65.01/65.17 (P3(f3(a18),f12(f13(a18,a18),f13(f13(a18,a18),f13(a18,a18))))), % 65.01/65.17 inference(scs_inference,[],[2461,721])). % 65.01/65.17 cnf(2574,plain, % 65.01/65.17 (E(f12(f11(a1,a1),x25741),f12(f13(a1,a1),x25741))), % 65.01/65.17 inference(scs_inference,[],[2461,1005,71,72,70,57,24,12,56,5,13,60,25,26,6])). % 65.01/65.17 cnf(2601,plain, % 65.01/65.17 (E(f13(f11(a1,a1),x26011),f13(f13(a1,a1),x26011))), % 65.01/65.17 inference(scs_inference,[],[2461,1005,71,72,70,57,24,12,56,5,13,60,25,26,6,69,15,29,59,20,58,17,23,61,11,18,28,10,8,4,9,7,21,14,19,27,16,22])). % 65.01/65.17 cnf(2603,plain, % 65.01/65.17 (P1(f12(f3(a18),f3(a18)))), % 65.01/65.17 inference(scs_inference,[],[1398,2461,1005,71,72,70,57,24,12,56,5,13,60,25,26,6,69,15,29,59,20,58,17,23,61,11,18,28,10,8,4,9,7,21,14,19,27,16,22,2,85])). % 65.01/65.17 cnf(2605,plain, % 65.01/65.17 (~E(f3(a18),a15)), % 65.01/65.17 inference(scs_inference,[],[1398,2461,2463,1005,71,72,70,57,24,12,56,5,13,60,25,26,6,69,15,29,59,20,58,17,23,61,11,18,28,10,8,4,9,7,21,14,19,27,16,22,2,85,55])). % 65.01/65.17 cnf(2607,plain, % 65.01/65.17 (P1(f11(f3(a18),f3(a18)))), % 65.01/65.17 inference(scs_inference,[],[1398,2461,2463,1005,71,72,70,57,24,12,56,5,13,60,25,26,6,69,15,29,59,20,58,17,23,61,11,18,28,10,8,4,9,7,21,14,19,27,16,22,2,85,55,86])). % 65.01/65.17 cnf(2613,plain, % 65.01/65.17 (~P5(a18,f12(a16,f13(a16,a16)))), % 65.01/65.17 inference(scs_inference,[],[52,1398,2461,2463,368,371,2243,1005,707,2293,50,373,71,72,70,57,24,12,56,5,13,60,25,26,6,69,15,29,59,20,58,17,23,61,11,18,28,10,8,4,9,7,21,14,19,27,16,22,2,85,55,86,3,35,34,36,37])). % 65.01/65.17 cnf(2615,plain, % 65.01/65.17 (P1(f6(f11(a1,a1),f11(a1,a1)))), % 65.01/65.17 inference(scs_inference,[],[52,1398,2461,2463,368,371,2243,1005,707,1927,2293,50,524,373,962,71,72,70,57,24,12,56,5,13,60,25,26,6,69,15,29,59,20,58,17,23,61,11,18,28,10,8,4,9,7,21,14,19,27,16,22,2,85,55,86,3,35,34,36,37,33,100])). % 65.01/65.17 cnf(2625,plain, % 65.01/65.17 (P2(f3(f12(a18,f13(a18,a18))))), % 65.01/65.17 inference(scs_inference,[],[52,1398,2507,2461,2463,368,2449,371,2243,1005,707,1927,2293,50,1006,524,373,40,962,434,708,650,71,72,70,57,24,12,56,5,13,60,25,26,6,69,15,29,59,20,58,17,23,61,11,18,28,10,8,4,9,7,21,14,19,27,16,22,2,85,55,86,3,35,34,36,37,33,100,126,107,108,127,63])). % 65.01/65.17 cnf(2627,plain, % 65.01/65.17 (P1(f3(f12(a18,f13(a18,a18))))), % 65.01/65.17 inference(scs_inference,[],[52,1398,2507,2461,2463,368,2449,371,2243,1005,707,1927,2293,50,1006,524,373,40,962,434,708,650,71,72,70,57,24,12,56,5,13,60,25,26,6,69,15,29,59,20,58,17,23,61,11,18,28,10,8,4,9,7,21,14,19,27,16,22,2,85,55,86,3,35,34,36,37,33,100,126,107,108,127,63,62])). % 65.01/65.17 cnf(2641,plain, % 65.01/65.17 (P5(f3(a18),f12(f3(a18),f3(a18)))), % 65.01/65.17 inference(scs_inference,[],[52,1398,2536,2507,2461,2463,368,2449,371,2243,1005,707,1927,2293,50,1006,524,373,40,338,962,434,355,42,708,650,71,72,70,57,24,12,56,5,13,60,25,26,6,69,15,29,59,20,58,17,23,61,11,18,28,10,8,4,9,7,21,14,19,27,16,22,2,85,55,86,3,35,34,36,37,33,100,126,107,108,127,63,62,99,118,92,117,78,79,258])). % 65.01/65.17 cnf(2643,plain, % 65.01/65.17 (E(f3(a18),a18)), % 65.01/65.17 inference(scs_inference,[],[52,1398,2536,2507,2461,2463,368,2449,371,2243,1005,707,1927,2293,50,1006,524,373,341,40,338,962,434,355,42,708,650,71,72,70,57,24,12,56,5,13,60,25,26,6,69,15,29,59,20,58,17,23,61,11,18,28,10,8,4,9,7,21,14,19,27,16,22,2,85,55,86,3,35,34,36,37,33,100,126,107,108,127,63,62,99,118,92,117,78,79,258,73])). % 65.01/65.17 cnf(2645,plain, % 65.01/65.17 (P3(f3(a18),f11(f3(a18),f3(a18)))), % 65.01/65.17 inference(scs_inference,[],[52,1398,2536,2507,2461,2463,368,2449,371,2243,1005,707,1927,2293,50,1006,524,373,341,40,338,962,434,355,42,708,650,71,72,70,57,24,12,56,5,13,60,25,26,6,69,15,29,59,20,58,17,23,61,11,18,28,10,8,4,9,7,21,14,19,27,16,22,2,85,55,86,3,35,34,36,37,33,100,126,107,108,127,63,62,99,118,92,117,78,79,258,73,257])). % 65.01/65.17 cnf(2653,plain, % 65.01/65.17 (P5(a16,a18)), % 65.01/65.17 inference(scs_inference,[],[52,2483,1398,2536,2507,2461,2463,368,2449,371,2243,1005,707,1927,2293,50,1006,524,373,341,40,41,338,962,434,355,42,708,650,71,72,70,57,24,12,56,5,13,60,25,26,6,69,15,29,59,20,58,17,23,61,11,18,28,10,8,4,9,7,21,14,19,27,16,22,2,85,55,86,3,35,34,36,37,33,100,126,107,108,127,63,62,99,118,92,117,78,79,258,73,257,265,66,74,84])). % 65.01/65.17 cnf(2663,plain, % 65.01/65.17 (P4(a17,a18)), % 65.01/65.17 inference(scs_inference,[],[52,2483,1398,2536,2507,2461,2463,629,368,2449,371,2243,1005,707,1927,2293,744,738,50,48,47,1006,524,373,341,40,41,543,338,962,434,355,42,708,650,38,71,72,70,57,24,12,56,5,13,60,25,26,6,69,15,29,59,20,58,17,23,61,11,18,28,10,8,4,9,7,21,14,19,27,16,22,2,85,55,86,3,35,34,36,37,33,100,126,107,108,127,63,62,99,118,92,117,78,79,258,73,257,265,66,74,84,101,102,80,81,91])). % 65.01/65.17 cnf(2669,plain, % 65.01/65.17 (P1(f12(f13(a1,a1),f13(a1,f11(a1,a1))))), % 65.01/65.17 inference(scs_inference,[],[52,2483,1398,2536,2507,2461,2463,629,368,2449,371,2489,2243,2203,1005,707,1927,2293,744,738,50,48,47,964,1006,524,373,320,341,40,41,543,338,962,434,355,42,708,650,38,71,72,70,57,24,12,56,5,13,60,25,26,6,69,15,29,59,20,58,17,23,61,11,18,28,10,8,4,9,7,21,14,19,27,16,22,2,85,55,86,3,35,34,36,37,33,100,126,107,108,127,63,62,99,118,92,117,78,79,258,73,257,265,66,74,84,101,102,80,81,91,95,105,97])). % 65.01/65.17 cnf(2681,plain, % 65.01/65.17 (P3(f3(a18),f13(f13(a18,a18),f13(a18,a18)))), % 65.01/65.17 inference(scs_inference,[],[52,2483,1398,2536,2540,2507,2461,2463,667,629,368,2449,371,2370,2489,2299,2541,372,2243,2203,1005,707,1927,2293,744,738,50,2189,48,1172,47,964,1006,524,373,597,320,341,40,41,1114,547,1077,543,572,966,338,962,434,355,42,708,650,39,38,71,72,70,57,24,12,56,5,13,60,25,26,6,69,15,29,59,20,58,17,23,61,11,18,28,10,8,4,9,7,21,14,19,27,16,22,2,85,55,86,3,35,34,36,37,33,100,126,107,108,127,63,62,99,118,92,117,78,79,258,73,257,265,66,74,84,101,102,80,81,91,95,105,97,94,104,103,110,111,124])). % 65.01/65.17 cnf(2687,plain, % 65.01/65.17 (~E(f13(a16,a16),f13(a18,a16))), % 65.01/65.17 inference(scs_inference,[],[52,2483,1398,2536,2540,2507,2461,2463,667,629,368,2449,371,2370,2489,2299,2541,372,2243,2203,1005,707,1927,2293,744,738,50,2189,48,1172,47,964,1006,343,524,373,597,320,341,40,41,1114,547,1077,543,572,966,338,962,434,355,42,708,650,39,38,71,72,70,57,24,12,56,5,13,60,25,26,6,69,15,29,59,20,58,17,23,61,11,18,28,10,8,4,9,7,21,14,19,27,16,22,2,85,55,86,3,35,34,36,37,33,100,126,107,108,127,63,62,99,118,92,117,78,79,258,73,257,265,66,74,84,101,102,80,81,91,95,105,97,94,104,103,110,111,124,122,123,612])). % 65.01/65.17 cnf(2690,plain, % 65.01/65.17 (E(f12(a1,f11(a1,a1)),a1)), % 65.01/65.17 inference(scs_inference,[],[52,2483,1398,2536,2540,2507,2461,2463,667,629,368,2449,371,2370,2489,2299,2541,372,2243,2203,1005,707,1927,2293,744,738,50,2189,48,1172,47,964,1006,343,524,373,597,320,341,40,41,1114,547,1077,543,572,966,338,962,434,355,42,708,650,39,38,71,72,70,57,24,12,56,5,13,60,25,26,6,69,15,29,59,20,58,17,23,61,11,18,28,10,8,4,9,7,21,14,19,27,16,22,2,85,55,86,3,35,34,36,37,33,100,126,107,108,127,63,62,99,118,92,117,78,79,258,73,257,265,66,74,84,101,102,80,81,91,95,105,97,94,104,103,110,111,124,122,123,612,64,324])). % 65.01/65.17 cnf(2716,plain, % 65.01/65.17 (E(a18,a16)+E(a18,a17)), % 65.01/65.17 inference(scs_inference,[],[2653,2533])). % 65.01/65.17 cnf(2765,plain, % 65.01/65.17 (~E(f13(a18,a17),f13(a17,a17))), % 65.01/65.17 inference(scs_inference,[],[2539,2643,2615,526,69,71,60,70,13,64,59,56,72,25,58,15,26,17,5,57,12,24,23,4,9,6,61,21,29,20,11,8,18,28,19,10,27,7,14,16,22,2])). % 65.01/65.17 cnf(2803,plain, % 65.01/65.17 (P1(f5(a16,a18))), % 65.01/65.17 inference(scs_inference,[],[52,2653,2663,2539,2605,2643,2615,1066,2681,2613,2574,2625,2627,1029,318,519,2483,2540,662,647,651,597,526,41,547,2461,40,355,42,69,71,60,70,13,64,59,56,72,25,58,15,26,17,5,57,12,24,23,4,9,6,61,21,29,20,11,8,18,28,19,10,27,7,14,16,22,2,85,86,55,31,32,54,3,35,34,36,37,33,107,100,63,126,92,108,62,127,118,117,99])). % 65.01/65.17 cnf(2838,plain, % 65.01/65.17 (~P3(f3(a18),f12(f13(f13(a18,a18),f13(a18,a18)),a16))), % 65.01/65.17 inference(scs_inference,[],[52,2653,2663,2539,2605,2643,2388,2615,1066,2641,2603,2607,2681,2645,2613,2574,2601,2669,2625,2627,850,2155,1029,1311,318,519,2483,2540,1927,652,662,964,647,651,597,392,526,1300,1056,41,547,2461,40,572,338,962,434,355,42,650,39,69,71,60,70,13,64,59,56,72,25,58,15,26,17,5,57,12,24,23,4,9,6,61,21,29,20,11,8,18,28,19,10,27,7,14,16,22,2,85,86,55,31,32,54,3,35,34,36,37,33,107,100,63,126,92,108,62,127,118,117,99,258,79,257,75,84,102,81,91,95,105,97,94,267,121,268,119,124])). % 65.01/65.17 cnf(2841,plain, % 65.01/65.17 (~E(a18,a16)), % 65.01/65.17 inference(scs_inference,[],[52,2653,2663,2539,2605,2643,2388,2615,1066,2641,2603,2607,2681,2645,2613,2574,2601,2669,2625,2627,850,2155,1029,1311,318,519,2483,2540,1927,652,662,964,647,651,597,392,526,1300,1056,41,547,2461,40,572,338,962,434,355,42,650,39,69,71,60,70,13,64,59,56,72,25,58,15,26,17,5,57,12,24,23,4,9,6,61,21,29,20,11,8,18,28,19,10,27,7,14,16,22,2,85,86,55,31,32,54,3,35,34,36,37,33,107,100,63,126,92,108,62,127,118,117,99,258,79,257,75,84,102,81,91,95,105,97,94,267,121,268,119,124,645,357])). % 65.01/65.17 cnf(2857,plain, % 65.01/65.17 (E(a18,a17)), % 65.01/65.17 inference(scs_inference,[],[2841,2716])). % 65.01/65.17 cnf(2908,plain, % 65.01/65.17 (P1(f12(f5(a16,a18),f5(a16,a18)))), % 65.01/65.17 inference(scs_inference,[],[2841,2687,2803,2690,2838,2716,357,69,71,59,70,58,25,56,72,60,26,64,23,13,12,61,57,15,29,4,6,24,5,17,20,18,21,10,9,8,11,28,7,19,16,27,22,14,2,85])). % 65.01/65.17 cnf(3026,plain, % 65.01/65.17 ($false), % 65.01/65.17 inference(scs_inference,[],[2857,2765,2908,457,70,71,59,69,56,60,58,72,64,57,61,25,13,26,23,12,17,10,15,24,8,9,11,7,29,6,4,5,16,27,20,18,22]), % 65.01/65.17 ['proof']). % 65.01/65.17 % SZS output end Proof % 65.01/65.17 % Total time :63.770000s %------------------------------------------------------------------------------