%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM505+3 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n026.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:41 EDT 2024 % Result : Theorem 59.97s 60.03s % Output : CNFRefutation 59.97s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.13/0.15 % Problem : NUM505+3 : TPTP v8.2.0. Released v4.0.0. % 0.13/0.15 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.15/0.38 % Computer : n026.cluster.edu % 0.15/0.38 % Model : x86_64 x86_64 % 0.15/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.38 % Memory : 8042.1875MB % 0.15/0.38 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.38 % CPULimit : 300 % 0.15/0.38 % WCLimit : 300 % 0.15/0.38 % DateTime : Sun Jun 23 02:31:24 EDT 2024 % 0.15/0.38 % CPUTime : % 0.51/0.63 start to proof:theBenchmark % 59.88/60.00 %------------------------------------------- % 59.88/60.00 % File :CSE---1.7 % 59.88/60.00 % Problem :theBenchmark % 59.88/60.00 % Transform :cnf % 59.88/60.00 % Format :tptp:raw % 59.88/60.00 % Command :java -jar mcs_scs.jar %d %s % 59.88/60.00 % 59.88/60.00 % Result :Theorem 58.720000s % 59.88/60.00 % Output :CNFRefutation 58.720000s % 59.88/60.00 %------------------------------------------- % 59.88/60.01 %------------------------------------------------------------------------------ % 59.88/60.01 % File : NUM505+3 : TPTP v8.2.0. Released v4.0.0. % 59.88/60.01 % Domain : Number Theory % 59.88/60.01 % Problem : Square root of a prime is irrational 14_03_03_03_03, 02 expansion % 59.88/60.01 % Version : Especial. % 59.88/60.01 % English : % 59.88/60.01 % 59.88/60.01 % Refs : [LPV06] Lyaletski et al. (2006), SAD as a Mathematical Assista % 59.88/60.01 % : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 59.88/60.01 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 59.88/60.01 % Source : [Pas08] % 59.88/60.01 % Names : primes_14_03_03_03_03.02 [Pas08] % 59.88/60.01 % 59.88/60.01 % Status : Theorem % 59.88/60.01 % Rating : 0.14 v7.5.0, 0.16 v7.4.0, 0.13 v7.3.0, 0.14 v7.2.0, 0.10 v7.1.0, 0.17 v7.0.0, 0.13 v6.4.0, 0.19 v6.3.0, 0.17 v6.2.0, 0.16 v6.1.0, 0.13 v6.0.0, 0.17 v5.5.0, 0.22 v5.4.0, 0.25 v5.3.0, 0.30 v5.2.0, 0.20 v5.1.0, 0.33 v5.0.0, 0.38 v4.1.0, 0.39 v4.0.1, 0.74 v4.0.0 % 59.88/60.01 % Syntax : Number of formulae : 50 ( 1 unt; 5 def) % 59.88/60.01 % Number of atoms : 266 ( 93 equ) % 59.88/60.01 % Maximal formula atoms : 22 ( 5 avg) % 59.88/60.01 % Number of connectives : 251 ( 35 ~; 20 |; 125 &) % 59.88/60.01 % ( 5 <=>; 66 =>; 0 <=; 0 <~>) % 59.88/60.01 % Maximal formula depth : 16 ( 6 avg) % 59.88/60.01 % Maximal term depth : 3 ( 1 avg) % 59.88/60.01 % Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty) % 59.88/60.01 % Number of functors : 11 ( 11 usr; 7 con; 0-2 aty) % 59.88/60.01 % Number of variables : 104 ( 85 !; 19 ?) % 59.88/60.01 % SPC : FOF_THM_RFO_SEQ % 59.88/60.01 % 59.88/60.01 % Comments : Problem generated by the SAD system [VLP07] % 59.88/60.01 %------------------------------------------------------------------------------ % 59.88/60.01 fof(mNatSort,axiom, % 59.88/60.01 ! [W0] : % 59.88/60.01 ( aNaturalNumber0(W0) % 59.88/60.01 => $true ) ). % 59.88/60.01 % 59.88/60.01 fof(mSortsC,axiom, % 59.88/60.01 aNaturalNumber0(sz00) ). % 59.88/60.01 % 59.88/60.01 fof(mSortsC_01,axiom, % 59.88/60.01 ( aNaturalNumber0(sz10) % 59.88/60.01 & sz10 != sz00 ) ). % 59.88/60.01 % 59.88/60.01 fof(mSortsB,axiom, % 59.88/60.01 ! [W0,W1] : % 59.88/60.01 ( ( aNaturalNumber0(W0) % 59.88/60.01 & aNaturalNumber0(W1) ) % 59.88/60.01 => aNaturalNumber0(sdtpldt0(W0,W1)) ) ). % 59.88/60.01 % 59.88/60.01 fof(mSortsB_02,axiom, % 59.88/60.01 ! [W0,W1] : % 59.88/60.01 ( ( aNaturalNumber0(W0) % 59.88/60.01 & aNaturalNumber0(W1) ) % 59.88/60.01 => aNaturalNumber0(sdtasdt0(W0,W1)) ) ). % 59.88/60.01 % 59.88/60.01 fof(mAddComm,axiom, % 59.88/60.01 ! [W0,W1] : % 59.88/60.01 ( ( aNaturalNumber0(W0) % 59.88/60.01 & aNaturalNumber0(W1) ) % 59.88/60.01 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 59.88/60.01 % 59.88/60.01 fof(mAddAsso,axiom, % 59.88/60.01 ! [W0,W1,W2] : % 59.88/60.01 ( ( aNaturalNumber0(W0) % 59.88/60.01 & aNaturalNumber0(W1) % 59.88/60.01 & aNaturalNumber0(W2) ) % 59.88/60.01 => sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) ). % 59.88/60.01 % 59.88/60.01 fof(m_AddZero,axiom, % 59.88/60.01 ! [W0] : % 59.88/60.01 ( aNaturalNumber0(W0) % 59.88/60.01 => ( sdtpldt0(W0,sz00) = W0 % 59.88/60.01 & W0 = sdtpldt0(sz00,W0) ) ) ). % 59.88/60.01 % 59.88/60.01 fof(mMulComm,axiom, % 59.88/60.01 ! [W0,W1] : % 59.88/60.01 ( ( aNaturalNumber0(W0) % 59.88/60.01 & aNaturalNumber0(W1) ) % 59.88/60.01 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 59.88/60.01 % 59.88/60.01 fof(mMulAsso,axiom, % 59.88/60.01 ! [W0,W1,W2] : % 59.88/60.01 ( ( aNaturalNumber0(W0) % 59.88/60.01 & aNaturalNumber0(W1) % 59.88/60.01 & aNaturalNumber0(W2) ) % 59.88/60.01 => sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) ). % 59.88/60.01 % 59.88/60.01 fof(m_MulUnit,axiom, % 59.88/60.02 ! [W0] : % 59.88/60.02 ( aNaturalNumber0(W0) % 59.88/60.02 => ( sdtasdt0(W0,sz10) = W0 % 59.88/60.02 & W0 = sdtasdt0(sz10,W0) ) ) ). % 59.88/60.02 % 59.88/60.02 fof(m_MulZero,axiom, % 59.88/60.02 ! [W0] : % 59.88/60.02 ( aNaturalNumber0(W0) % 59.88/60.02 => ( sdtasdt0(W0,sz00) = sz00 % 59.88/60.02 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 59.88/60.02 % 59.88/60.02 fof(mAMDistr,axiom, % 59.88/60.02 ! [W0,W1,W2] : % 59.88/60.02 ( ( aNaturalNumber0(W0) % 59.88/60.02 & aNaturalNumber0(W1) % 59.88/60.02 & aNaturalNumber0(W2) ) % 59.88/60.02 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 59.88/60.02 & sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ). % 59.88/60.02 % 59.88/60.02 fof(mAddCanc,axiom, % 59.88/60.02 ! [W0,W1,W2] : % 59.88/60.02 ( ( aNaturalNumber0(W0) % 59.88/60.02 & aNaturalNumber0(W1) % 59.88/60.02 & aNaturalNumber0(W2) ) % 59.88/60.02 => ( ( sdtpldt0(W0,W1) = sdtpldt0(W0,W2) % 59.88/60.02 | sdtpldt0(W1,W0) = sdtpldt0(W2,W0) ) % 59.88/60.02 => W1 = W2 ) ) ). % 59.88/60.02 % 59.88/60.02 fof(mMulCanc,axiom, % 59.88/60.02 ! [W0] : % 59.88/60.02 ( aNaturalNumber0(W0) % 59.88/60.02 => ( W0 != sz00 % 59.88/60.02 => ! [W1,W2] : % 59.88/60.02 ( ( aNaturalNumber0(W1) % 59.88/60.02 & aNaturalNumber0(W2) ) % 59.88/60.02 => ( ( sdtasdt0(W0,W1) = sdtasdt0(W0,W2) % 59.88/60.02 | sdtasdt0(W1,W0) = sdtasdt0(W2,W0) ) % 59.88/60.02 => W1 = W2 ) ) ) ) ). % 59.88/60.02 % 59.88/60.02 fof(mZeroAdd,axiom, % 59.88/60.02 ! [W0,W1] : % 59.88/60.02 ( ( aNaturalNumber0(W0) % 59.88/60.02 & aNaturalNumber0(W1) ) % 59.88/60.02 => ( sdtpldt0(W0,W1) = sz00 % 59.88/60.02 => ( W0 = sz00 % 59.88/60.02 & W1 = sz00 ) ) ) ). % 59.88/60.02 % 59.88/60.02 fof(mZeroMul,axiom, % 59.88/60.02 ! [W0,W1] : % 59.88/60.02 ( ( aNaturalNumber0(W0) % 59.88/60.02 & aNaturalNumber0(W1) ) % 59.88/60.02 => ( sdtasdt0(W0,W1) = sz00 % 59.88/60.02 => ( W0 = sz00 % 59.88/60.02 | W1 = sz00 ) ) ) ). % 59.88/60.02 % 59.88/60.02 fof(mDefLE,definition, % 59.88/60.02 ! [W0,W1] : % 59.88/60.02 ( ( aNaturalNumber0(W0) % 59.88/60.02 & aNaturalNumber0(W1) ) % 59.88/60.02 => ( sdtlseqdt0(W0,W1) % 59.88/60.02 <=> ? [W2] : % 59.88/60.02 ( aNaturalNumber0(W2) % 59.88/60.02 & sdtpldt0(W0,W2) = W1 ) ) ) ). % 59.88/60.02 % 59.88/60.02 fof(mDefDiff,definition, % 59.88/60.02 ! [W0,W1] : % 59.88/60.02 ( ( aNaturalNumber0(W0) % 59.88/60.02 & aNaturalNumber0(W1) ) % 59.88/60.02 => ( sdtlseqdt0(W0,W1) % 59.88/60.02 => ! [W2] : % 59.88/60.02 ( W2 = sdtmndt0(W1,W0) % 59.88/60.02 <=> ( aNaturalNumber0(W2) % 59.88/60.02 & sdtpldt0(W0,W2) = W1 ) ) ) ) ). % 59.88/60.02 % 59.88/60.02 fof(mLERefl,axiom, % 59.88/60.02 ! [W0] : % 59.88/60.02 ( aNaturalNumber0(W0) % 59.88/60.02 => sdtlseqdt0(W0,W0) ) ). % 59.88/60.02 % 59.88/60.02 fof(mLEAsym,axiom, % 59.88/60.02 ! [W0,W1] : % 59.88/60.02 ( ( aNaturalNumber0(W0) % 59.88/60.02 & aNaturalNumber0(W1) ) % 59.88/60.02 => ( ( sdtlseqdt0(W0,W1) % 59.88/60.02 & sdtlseqdt0(W1,W0) ) % 59.88/60.02 => W0 = W1 ) ) ). % 59.88/60.02 % 59.88/60.02 fof(mLETran,axiom, % 59.88/60.02 ! [W0,W1,W2] : % 59.88/60.02 ( ( aNaturalNumber0(W0) % 59.88/60.02 & aNaturalNumber0(W1) % 59.88/60.02 & aNaturalNumber0(W2) ) % 59.88/60.02 => ( ( sdtlseqdt0(W0,W1) % 59.88/60.02 & sdtlseqdt0(W1,W2) ) % 59.88/60.02 => sdtlseqdt0(W0,W2) ) ) ). % 59.88/60.02 % 59.88/60.02 fof(mLETotal,axiom, % 59.88/60.02 ! [W0,W1] : % 59.88/60.02 ( ( aNaturalNumber0(W0) % 59.88/60.02 & aNaturalNumber0(W1) ) % 59.88/60.02 => ( sdtlseqdt0(W0,W1) % 59.88/60.02 | ( W1 != W0 % 59.88/60.02 & sdtlseqdt0(W1,W0) ) ) ) ). % 59.88/60.02 % 59.88/60.02 fof(mMonAdd,axiom, % 59.88/60.02 ! [W0,W1] : % 59.88/60.02 ( ( aNaturalNumber0(W0) % 59.88/60.02 & aNaturalNumber0(W1) ) % 59.88/60.02 => ( ( W0 != W1 % 59.88/60.02 & sdtlseqdt0(W0,W1) ) % 59.88/60.02 => ! [W2] : % 59.88/60.02 ( aNaturalNumber0(W2) % 59.88/60.02 => ( sdtpldt0(W2,W0) != sdtpldt0(W2,W1) % 59.88/60.02 & sdtlseqdt0(sdtpldt0(W2,W0),sdtpldt0(W2,W1)) % 59.88/60.02 & sdtpldt0(W0,W2) != sdtpldt0(W1,W2) % 59.88/60.02 & sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W2)) ) ) ) ) ). % 59.88/60.02 % 59.88/60.02 fof(mMonMul,axiom, % 59.88/60.02 ! [W0,W1,W2] : % 59.88/60.02 ( ( aNaturalNumber0(W0) % 59.88/60.02 & aNaturalNumber0(W1) % 59.88/60.02 & aNaturalNumber0(W2) ) % 59.88/60.02 => ( ( W0 != sz00 % 59.88/60.02 & W1 != W2 % 59.88/60.02 & sdtlseqdt0(W1,W2) ) % 59.88/60.02 => ( sdtasdt0(W0,W1) != sdtasdt0(W0,W2) % 59.88/60.02 & sdtlseqdt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 59.88/60.02 & sdtasdt0(W1,W0) != sdtasdt0(W2,W0) % 59.88/60.02 & sdtlseqdt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ) ). % 59.88/60.02 % 59.88/60.02 fof(mLENTr,axiom, % 59.88/60.02 ! [W0] : % 59.88/60.02 ( aNaturalNumber0(W0) % 59.88/60.02 => ( W0 = sz00 % 59.88/60.02 | W0 = sz10 % 59.88/60.02 | ( sz10 != W0 % 59.88/60.02 & sdtlseqdt0(sz10,W0) ) ) ) ). % 59.88/60.02 % 59.88/60.02 fof(mMonMul2,axiom, % 59.88/60.02 ! [W0,W1] : % 59.88/60.02 ( ( aNaturalNumber0(W0) % 59.88/60.02 & aNaturalNumber0(W1) ) % 59.88/60.02 => ( W0 != sz00 % 59.88/60.02 => sdtlseqdt0(W1,sdtasdt0(W1,W0)) ) ) ). % 59.88/60.02 % 59.88/60.02 fof(mIH,axiom, % 59.88/60.02 ! [W0,W1] : % 59.88/60.02 ( ( aNaturalNumber0(W0) % 59.88/60.02 & aNaturalNumber0(W1) ) % 59.88/60.02 => ( iLess0(W0,W1) % 59.88/60.02 => $true ) ) ). % 59.88/60.02 % 59.88/60.02 fof(mIH_03,axiom, % 59.88/60.02 ! [W0,W1] : % 59.88/60.02 ( ( aNaturalNumber0(W0) % 59.88/60.02 & aNaturalNumber0(W1) ) % 59.88/60.02 => ( ( W0 != W1 % 59.88/60.02 & sdtlseqdt0(W0,W1) ) % 59.88/60.02 => iLess0(W0,W1) ) ) ). % 59.88/60.02 % 59.88/60.02 fof(mDefDiv,definition, % 59.88/60.02 ! [W0,W1] : % 59.88/60.02 ( ( aNaturalNumber0(W0) % 59.88/60.02 & aNaturalNumber0(W1) ) % 59.88/60.02 => ( doDivides0(W0,W1) % 59.88/60.02 <=> ? [W2] : % 59.88/60.02 ( aNaturalNumber0(W2) % 59.88/60.02 & W1 = sdtasdt0(W0,W2) ) ) ) ). % 59.88/60.02 % 59.88/60.02 fof(mDefQuot,definition, % 59.97/60.02 ! [W0,W1] : % 59.97/60.02 ( ( aNaturalNumber0(W0) % 59.97/60.02 & aNaturalNumber0(W1) ) % 59.97/60.02 => ( ( W0 != sz00 % 59.97/60.02 & doDivides0(W0,W1) ) % 59.97/60.02 => ! [W2] : % 59.97/60.02 ( W2 = sdtsldt0(W1,W0) % 59.97/60.02 <=> ( aNaturalNumber0(W2) % 59.97/60.02 & W1 = sdtasdt0(W0,W2) ) ) ) ) ). % 59.97/60.02 % 59.97/60.02 fof(mDivTrans,axiom, % 59.97/60.02 ! [W0,W1,W2] : % 59.97/60.02 ( ( aNaturalNumber0(W0) % 59.97/60.02 & aNaturalNumber0(W1) % 59.97/60.02 & aNaturalNumber0(W2) ) % 59.97/60.02 => ( ( doDivides0(W0,W1) % 59.97/60.02 & doDivides0(W1,W2) ) % 59.97/60.02 => doDivides0(W0,W2) ) ) ). % 59.97/60.02 % 59.97/60.02 fof(mDivSum,axiom, % 59.97/60.02 ! [W0,W1,W2] : % 59.97/60.02 ( ( aNaturalNumber0(W0) % 59.97/60.02 & aNaturalNumber0(W1) % 59.97/60.02 & aNaturalNumber0(W2) ) % 59.97/60.02 => ( ( doDivides0(W0,W1) % 59.97/60.02 & doDivides0(W0,W2) ) % 59.97/60.02 => doDivides0(W0,sdtpldt0(W1,W2)) ) ) ). % 59.97/60.02 % 59.97/60.02 fof(mDivMin,axiom, % 59.97/60.02 ! [W0,W1,W2] : % 59.97/60.02 ( ( aNaturalNumber0(W0) % 59.97/60.02 & aNaturalNumber0(W1) % 59.97/60.02 & aNaturalNumber0(W2) ) % 59.97/60.02 => ( ( doDivides0(W0,W1) % 59.97/60.02 & doDivides0(W0,sdtpldt0(W1,W2)) ) % 59.97/60.02 => doDivides0(W0,W2) ) ) ). % 59.97/60.02 % 59.97/60.02 fof(mDivLE,axiom, % 59.97/60.02 ! [W0,W1] : % 59.97/60.02 ( ( aNaturalNumber0(W0) % 59.97/60.02 & aNaturalNumber0(W1) ) % 59.97/60.02 => ( ( doDivides0(W0,W1) % 59.97/60.02 & W1 != sz00 ) % 59.97/60.02 => sdtlseqdt0(W0,W1) ) ) ). % 59.97/60.02 % 59.97/60.02 fof(mDivAsso,axiom, % 59.97/60.02 ! [W0,W1] : % 59.97/60.02 ( ( aNaturalNumber0(W0) % 59.97/60.02 & aNaturalNumber0(W1) ) % 59.97/60.02 => ( ( W0 != sz00 % 59.97/60.02 & doDivides0(W0,W1) ) % 59.97/60.02 => ! [W2] : % 59.97/60.02 ( aNaturalNumber0(W2) % 59.97/60.02 => sdtasdt0(W2,sdtsldt0(W1,W0)) = sdtsldt0(sdtasdt0(W2,W1),W0) ) ) ) ). % 59.97/60.02 % 59.97/60.02 fof(mDefPrime,definition, % 59.97/60.02 ! [W0] : % 59.97/60.02 ( aNaturalNumber0(W0) % 59.97/60.02 => ( isPrime0(W0) % 59.97/60.02 <=> ( W0 != sz00 % 59.97/60.02 & W0 != sz10 % 59.97/60.02 & ! [W1] : % 59.97/60.02 ( ( aNaturalNumber0(W1) % 59.97/60.02 & doDivides0(W1,W0) ) % 59.97/60.02 => ( W1 = sz10 % 59.97/60.02 | W1 = W0 ) ) ) ) ) ). % 59.97/60.02 % 59.97/60.02 fof(mPrimDiv,axiom, % 59.97/60.02 ! [W0] : % 59.97/60.02 ( ( aNaturalNumber0(W0) % 59.97/60.02 & W0 != sz00 % 59.97/60.03 & W0 != sz10 ) % 59.97/60.03 => ? [W1] : % 59.97/60.03 ( aNaturalNumber0(W1) % 59.97/60.03 & doDivides0(W1,W0) % 59.97/60.03 & isPrime0(W1) ) ) ). % 59.97/60.03 % 59.97/60.03 fof(m__1837,hypothesis, % 59.97/60.03 ( aNaturalNumber0(xn) % 59.97/60.03 & aNaturalNumber0(xm) % 59.97/60.03 & aNaturalNumber0(xp) ) ). % 59.97/60.03 % 59.97/60.03 fof(m__1799,hypothesis, % 59.97/60.03 ! [W0,W1,W2] : % 59.97/60.03 ( ( aNaturalNumber0(W0) % 59.97/60.03 & aNaturalNumber0(W1) % 59.97/60.03 & aNaturalNumber0(W2) ) % 59.97/60.03 => ( ( ( ( W2 != sz00 % 59.97/60.03 & W2 != sz10 % 59.97/60.03 & ! [W3] : % 59.97/60.03 ( ( aNaturalNumber0(W3) % 59.97/60.03 & ? [W4] : % 59.97/60.03 ( aNaturalNumber0(W4) % 59.97/60.03 & W2 = sdtasdt0(W3,W4) ) % 59.97/60.03 & doDivides0(W3,W2) ) % 59.97/60.03 => ( W3 = sz10 % 59.97/60.03 | W3 = W2 ) ) ) % 59.97/60.03 | isPrime0(W2) ) % 59.97/60.03 & ( ? [W3] : % 59.97/60.03 ( aNaturalNumber0(W3) % 59.97/60.03 & sdtasdt0(W0,W1) = sdtasdt0(W2,W3) ) % 59.97/60.03 | doDivides0(W2,sdtasdt0(W0,W1)) ) ) % 59.97/60.03 => ( iLess0(sdtpldt0(sdtpldt0(W0,W1),W2),sdtpldt0(sdtpldt0(xn,xm),xp)) % 59.97/60.03 => ( ( ? [W3] : % 59.97/60.03 ( aNaturalNumber0(W3) % 59.97/60.03 & W0 = sdtasdt0(W2,W3) ) % 59.97/60.03 & doDivides0(W2,W0) ) % 59.97/60.03 | ( ? [W3] : % 59.97/60.03 ( aNaturalNumber0(W3) % 59.97/60.03 & W1 = sdtasdt0(W2,W3) ) % 59.97/60.03 & doDivides0(W2,W1) ) ) ) ) ) ). % 59.97/60.03 % 59.97/60.03 fof(m__1860,hypothesis, % 59.97/60.03 ( xp != sz00 % 59.97/60.03 & xp != sz10 % 59.97/60.03 & ! [W0] : % 59.97/60.03 ( ( aNaturalNumber0(W0) % 59.97/60.03 & ( ? [W1] : % 59.97/60.03 ( aNaturalNumber0(W1) % 59.97/60.03 & xp = sdtasdt0(W0,W1) ) % 59.97/60.03 | doDivides0(W0,xp) ) ) % 59.97/60.03 => ( W0 = sz10 % 59.97/60.03 | W0 = xp ) ) % 59.97/60.03 & isPrime0(xp) % 59.97/60.03 & ? [W0] : % 59.97/60.03 ( aNaturalNumber0(W0) % 59.97/60.03 & sdtasdt0(xn,xm) = sdtasdt0(xp,W0) ) % 59.97/60.03 & doDivides0(xp,sdtasdt0(xn,xm)) ) ). % 59.97/60.03 % 59.97/60.03 fof(m__1870,hypothesis, % 59.97/60.03 ~ ( ? [W0] : % 59.97/60.03 ( aNaturalNumber0(W0) % 59.97/60.03 & sdtpldt0(xp,W0) = xn ) % 59.97/60.03 | sdtlseqdt0(xp,xn) ) ). % 59.97/60.03 % 59.97/60.03 fof(m__2075,hypothesis, % 59.97/60.03 ~ ( ? [W0] : % 59.97/60.03 ( aNaturalNumber0(W0) % 59.97/60.03 & sdtpldt0(xp,W0) = xm ) % 59.97/60.03 | sdtlseqdt0(xp,xm) ) ). % 59.97/60.03 % 59.97/60.03 fof(m__2287,hypothesis, % 59.97/60.03 ( xn != xp % 59.97/60.03 & ? [W0] : % 59.97/60.03 ( aNaturalNumber0(W0) % 59.97/60.03 & sdtpldt0(xn,W0) = xp ) % 59.97/60.03 & sdtlseqdt0(xn,xp) % 59.97/60.03 & xm != xp % 59.97/60.03 & ? [W0] : % 59.97/60.03 ( aNaturalNumber0(W0) % 59.97/60.03 & sdtpldt0(xm,W0) = xp ) % 59.97/60.03 & sdtlseqdt0(xm,xp) ) ). % 59.97/60.03 % 59.97/60.03 fof(m__2306,hypothesis, % 59.97/60.03 ( aNaturalNumber0(xk) % 59.97/60.03 & sdtasdt0(xn,xm) = sdtasdt0(xp,xk) % 59.97/60.03 & xk = sdtsldt0(sdtasdt0(xn,xm),xp) ) ). % 59.97/60.03 % 59.97/60.03 fof(m__2315,hypothesis, % 59.97/60.03 ~ ( xk = sz00 % 59.97/60.03 | xk = sz10 ) ). % 59.97/60.03 % 59.97/60.03 fof(m__2327,hypothesis, % 59.97/60.03 ( xk != sz00 % 59.97/60.03 & xk != sz10 ) ). % 59.97/60.03 % 59.97/60.03 fof(m__2342,hypothesis, % 59.97/60.03 ( aNaturalNumber0(xr) % 59.97/60.03 & ? [W0] : % 59.97/60.03 ( aNaturalNumber0(W0) % 59.97/60.03 & xk = sdtasdt0(xr,W0) ) % 59.97/60.03 & doDivides0(xr,xk) % 59.97/60.03 & xr != sz00 % 59.97/60.03 & xr != sz10 % 59.97/60.03 & ! [W0] : % 59.97/60.03 ( ( aNaturalNumber0(W0) % 59.97/60.03 & ( ? [W1] : % 59.97/60.03 ( aNaturalNumber0(W1) % 59.97/60.03 & xr = sdtasdt0(W0,W1) ) % 59.97/60.03 | doDivides0(W0,xr) ) ) % 59.97/60.03 => ( W0 = sz10 % 59.97/60.03 | W0 = xr ) ) % 59.97/60.03 & isPrime0(xr) ) ). % 59.97/60.03 % 59.97/60.03 fof(m__2362,hypothesis, % 59.97/60.03 ( ? [W0] : % 59.97/60.03 ( aNaturalNumber0(W0) % 59.97/60.03 & sdtpldt0(xr,W0) = xk ) % 59.97/60.03 & ? [W0] : % 59.97/60.03 ( aNaturalNumber0(W0) % 59.97/60.03 & sdtasdt0(xn,xm) = sdtasdt0(xr,W0) ) % 59.97/60.03 & doDivides0(xr,sdtasdt0(xn,xm)) ) ). % 59.97/60.03 % 59.97/60.03 fof(m__,conjecture, % 59.97/60.03 ( ~ ( ? [W0] : % 59.97/60.03 ( aNaturalNumber0(W0) % 59.97/60.03 & sdtpldt0(xp,W0) = xk ) % 59.97/60.03 | sdtlseqdt0(xp,xk) ) % 59.97/60.03 => ( xk != xp % 59.97/60.03 & ( ? [W0] : % 59.97/60.03 ( aNaturalNumber0(W0) % 59.97/60.03 & sdtpldt0(xk,W0) = xp ) % 59.97/60.03 | sdtlseqdt0(xk,xp) ) ) ) ). % 59.97/60.03 % 59.97/60.03 %------------------------------------------------------------------------------ % 59.97/60.03 %------------------------------------------- % 59.97/60.03 % Proof found % 59.97/60.03 % SZS status Theorem for theBenchmark % 59.97/60.03 % SZS output start Proof % 59.97/60.03 %ClaNum:278(EqnAxiom:37) % 59.97/60.03 %VarNum:3220(SingletonVarNum:579) % 59.97/60.03 %MaxLitNum:11 % 59.97/60.03 %MaxfuncDepth:2 % 59.97/60.03 %SharedTerms:66 % 59.97/60.03 %goalClause: 79 82 98 99 % 59.97/60.03 %singleGoalClaCount:1 % 59.97/60.03 [38]P1(a1) % 59.97/60.03 [39]P1(a20) % 59.97/60.03 [40]P1(a21) % 59.97/60.03 [41]P1(a22) % 59.97/60.03 [42]P1(a24) % 59.97/60.03 [43]P1(a23) % 59.97/60.03 [44]P1(a25) % 59.97/60.03 [45]P1(a2) % 59.97/60.03 [46]P1(a3) % 59.97/60.03 [47]P1(a4) % 59.97/60.03 [48]P1(a5) % 59.97/60.03 [49]P1(a6) % 59.97/60.03 [50]P1(a7) % 59.97/60.03 [51]P2(a24) % 59.97/60.03 [52]P2(a25) % 59.97/60.03 [57]P5(a21,a24) % 59.97/60.03 [58]P5(a22,a24) % 59.97/60.03 [59]P3(a25,a23) % 59.97/60.03 [66]~E(a1,a20) % 59.97/60.03 [67]~E(a1,a24) % 59.97/60.03 [68]~E(a24,a20) % 59.97/60.03 [69]~E(a24,a21) % 59.97/60.03 [70]~E(a24,a22) % 59.97/60.03 [72]~E(a1,a23) % 59.97/60.03 [74]~E(a23,a20) % 59.97/60.03 [75]~E(a1,a25) % 59.97/60.03 [76]~E(a25,a20) % 59.97/60.03 [77]~P5(a24,a21) % 59.97/60.03 [78]~P5(a24,a22) % 59.97/60.03 [79]~P5(a24,a23) % 59.97/60.03 [53]E(f16(a25,a5),a23) % 59.97/60.03 [54]E(f17(a21,a3),a24) % 59.97/60.03 [55]E(f17(a22,a4),a24) % 59.97/60.03 [56]E(f17(a25,a6),a23) % 59.97/60.03 [60]E(f16(a24,a23),f16(a21,a22)) % 59.97/60.03 [61]E(f16(a24,a2),f16(a21,a22)) % 59.97/60.03 [62]E(f16(a25,a7),f16(a21,a22)) % 59.97/60.03 [64]P3(a24,f16(a21,a22)) % 59.97/60.03 [65]P3(a25,f16(a21,a22)) % 59.97/60.03 [63]E(f19(f16(a21,a22),a24),a23) % 59.97/60.03 [82]E(a23,a24)+~P5(a23,a24) % 59.97/60.03 [91]~P1(x911)+P5(x911,x911) % 59.97/60.03 [83]~P1(x831)+E(f16(a1,x831),a1) % 59.97/60.03 [84]~P1(x841)+E(f16(x841,a1),a1) % 59.97/60.03 [85]~P1(x851)+E(f17(a1,x851),x851) % 59.97/60.03 [86]~P1(x861)+E(f16(a20,x861),x861) % 59.97/60.03 [87]~P1(x871)+E(f17(x871,a1),x871) % 59.97/60.03 [88]~P1(x881)+E(f16(x881,a20),x881) % 59.97/60.03 [96]~P1(x961)+~E(f17(a24,x961),a21) % 59.97/60.03 [97]~P1(x971)+~E(f17(a24,x971),a22) % 59.97/60.03 [98]~P1(x981)+~E(f17(a24,x981),a23) % 59.97/60.03 [80]~P1(x801)+~P2(x801)+~E(x801,a1) % 59.97/60.03 [81]~P1(x811)+~P2(x811)+~E(x811,a20) % 59.97/60.03 [99]~P1(x991)+E(a23,a24)+~E(f17(a23,x991),a24) % 59.97/60.03 [110]~P1(x1102)+~P1(x1101)+E(f17(x1101,x1102),f17(x1102,x1101)) % 59.97/60.03 [111]~P1(x1112)+~P1(x1111)+E(f16(x1111,x1112),f16(x1112,x1111)) % 59.97/60.03 [113]~P1(x1132)+~P1(x1131)+P1(f17(x1131,x1132)) % 59.97/60.03 [114]~P1(x1142)+~P1(x1141)+P1(f16(x1141,x1142)) % 59.97/60.03 [93]~P1(x931)+E(x931,a20)+P5(a20,x931)+E(x931,a1) % 59.97/60.03 [100]~P1(x1001)+E(x1001,a24)+~P3(x1001,a24)+E(x1001,a20) % 59.97/60.03 [101]~P1(x1011)+E(x1011,a25)+~P3(x1011,a25)+E(x1011,a20) % 59.97/60.03 [89]~P1(x891)+E(x891,a20)+E(x891,a1)+P1(f8(x891)) % 59.97/60.03 [90]~P1(x901)+E(x901,a20)+E(x901,a1)+P2(f8(x901)) % 59.97/60.03 [102]~P1(x1021)+E(x1021,a20)+P3(f8(x1021),x1021)+E(x1021,a1) % 59.97/60.03 [103]~E(x1032,x1031)+~P1(x1031)+~P1(x1032)+P5(x1031,x1032) % 59.97/60.03 [112]P5(x1122,x1121)+~P1(x1121)+~P1(x1122)+P5(x1121,x1122) % 59.97/60.03 [105]~P1(x1052)+~P1(x1051)+E(x1051,a1)+~E(f17(x1052,x1051),a1) % 59.97/60.03 [106]~P1(x1062)+~P1(x1061)+E(x1061,a1)+~E(f17(x1061,x1062),a1) % 59.97/60.03 [118]~P1(x1182)+~P1(x1181)+P5(x1182,f16(x1182,x1181))+E(x1181,a1) % 59.97/60.03 [124]~P1(x1242)+~P1(x1241)+~P5(x1241,x1242)+P1(f10(x1241,x1242)) % 59.97/60.03 [125]~P1(x1252)+~P1(x1251)+~P3(x1251,x1252)+P1(f11(x1251,x1252)) % 59.97/60.03 [132]~P1(x1321)+~P1(x1322)+~P3(x1321,x1322)+E(f16(x1321,f11(x1321,x1322)),x1322) % 59.97/60.03 [133]~P1(x1332)+~P1(x1331)+~P5(x1331,x1332)+E(f17(x1331,f10(x1331,x1332)),x1332) % 59.97/60.03 [142]~P1(x1423)+~P1(x1422)+~P1(x1421)+E(f17(f17(x1421,x1422),x1423),f17(x1421,f17(x1422,x1423))) % 59.97/60.03 [143]~P1(x1433)+~P1(x1432)+~P1(x1431)+E(f16(f16(x1431,x1432),x1433),f16(x1431,f16(x1432,x1433))) % 59.97/60.03 [151]~P1(x1513)+~P1(x1512)+~P1(x1511)+E(f17(f16(x1511,x1512),f16(x1511,x1513)),f16(x1511,f17(x1512,x1513))) % 59.97/60.03 [152]~P1(x1522)+~P1(x1523)+~P1(x1521)+E(f17(f16(x1521,x1522),f16(x1523,x1522)),f16(f17(x1521,x1523),x1522)) % 59.97/60.03 [92]P2(x921)+~P1(x921)+E(x921,a20)+E(x921,a1)+~E(f9(x921),a20) % 59.97/60.03 [94]P2(x941)+~P1(x941)+E(x941,a20)+~E(f9(x941),x941)+E(x941,a1) % 59.97/60.03 [95]P2(x951)+~P1(x951)+E(x951,a20)+E(x951,a1)+P1(f9(x951)) % 59.97/60.03 [104]P2(x1041)+~P1(x1041)+E(x1041,a20)+P3(f9(x1041),x1041)+E(x1041,a1) % 59.97/60.03 [116]~P1(x1161)+~P1(x1162)+~P3(x1162,x1161)+P5(x1162,x1161)+E(x1161,a1) % 59.97/60.03 [117]P4(x1171,x1172)+~P1(x1172)+~P1(x1171)+~P5(x1171,x1172)+E(x1171,x1172) % 59.97/60.03 [121]~P1(x1212)+~P1(x1211)+~P5(x1212,x1211)+~P5(x1211,x1212)+E(x1211,x1212) % 59.97/60.03 [107]~P1(x1071)+~P1(x1072)+E(x1071,a24)+E(x1071,a20)+~E(f16(x1071,x1072),a24) % 59.97/60.03 [108]~P1(x1081)+~P1(x1082)+E(x1081,a25)+E(x1081,a20)+~E(f16(x1081,x1082),a25) % 59.97/60.03 [109]~P1(x1091)+~P1(x1092)+E(x1091,a1)+E(x1092,a1)+~E(f16(x1092,x1091),a1) % 59.97/60.03 [119]~P1(x1191)+~P1(x1192)+~P1(x1193)+P3(x1191,x1192)+~E(x1192,f16(x1191,x1193)) % 59.97/60.03 [120]~P1(x1202)+~P1(x1201)+~P1(x1203)+P5(x1201,x1202)+~E(f17(x1201,x1203),x1202) % 59.97/60.03 [122]~P1(x1223)+~P1(x1222)+~P5(x1223,x1222)+P1(x1221)+~E(x1221,f18(x1222,x1223)) % 59.97/60.03 [126]~P1(x1262)+~P1(x1261)+~P1(x1263)+E(x1261,x1262)+~E(f17(x1263,x1261),f17(x1263,x1262)) % 59.97/60.03 [127]~P1(x1272)+~P1(x1273)+~P1(x1271)+E(x1271,x1272)+~E(f17(x1271,x1273),f17(x1272,x1273)) % 59.97/60.03 [130]~P1(x1303)+~P1(x1301)+~P5(x1301,x1303)+~E(x1302,f18(x1303,x1301))+E(f17(x1301,x1302),x1303) % 59.97/60.03 [115]~P1(x1152)+~P1(x1151)+~P2(x1152)+~P3(x1151,x1152)+E(x1151,x1152)+E(x1151,a20) % 59.97/60.03 [134]~P1(x1342)+~P1(x1341)+~P5(x1343,x1342)+~P5(x1341,x1343)+P5(x1341,x1342)+~P1(x1343) % 59.97/60.03 [135]~P1(x1352)+~P1(x1351)+~P3(x1353,x1352)+~P3(x1351,x1353)+P3(x1351,x1352)+~P1(x1353) % 59.97/60.03 [123]~P1(x1231)+~P1(x1233)+~P3(x1231,x1233)+P1(x1232)+E(x1231,a1)+~E(x1232,f19(x1233,x1231)) % 59.97/60.03 [128]~P1(x1282)+~P1(x1281)+~P1(x1283)+E(x1281,x1282)+~E(f16(x1283,x1281),f16(x1283,x1282))+E(x1283,a1) % 59.97/60.03 [129]~P1(x1292)+~P1(x1293)+~P1(x1291)+E(x1291,x1292)+~E(f16(x1291,x1293),f16(x1292,x1293))+E(x1293,a1) % 59.97/60.03 [131]~P1(x1311)+~P1(x1312)+~P3(x1311,x1312)+~E(x1313,f19(x1312,x1311))+E(x1311,a1)+E(x1312,f16(x1311,x1313)) % 59.97/60.03 [136]~P1(x1362)+~P1(x1363)+~P1(x1361)+~P5(x1363,x1362)+~E(f17(x1363,x1361),x1362)+E(x1361,f18(x1362,x1363)) % 59.97/60.03 [144]~P1(x1443)+~P1(x1442)+~P1(x1441)+~P3(x1441,x1443)+~P3(x1441,x1442)+P3(x1441,f17(x1442,x1443)) % 59.97/60.03 [145]~P1(x1452)+~P1(x1451)+~P1(x1453)+~P5(x1451,x1452)+E(x1451,x1452)+P5(f17(x1453,x1451),f17(x1453,x1452)) % 59.97/60.03 [146]~P1(x1462)+~P1(x1463)+~P1(x1461)+~P5(x1461,x1462)+E(x1461,x1462)+P5(f17(x1461,x1463),f17(x1462,x1463)) % 59.97/60.03 [149]~P1(x1492)+~P1(x1491)+~P3(x1491,x1493)+P3(x1491,x1492)+~P1(x1493)+~P3(x1491,f17(x1493,x1492)) % 59.97/60.03 [150]~P1(x1502)+~P1(x1503)+~P1(x1501)+~P3(x1501,x1503)+E(x1501,a1)+E(f19(f16(x1502,x1503),x1501),f16(x1502,f19(x1503,x1501))) % 59.97/60.03 [137]~P1(x1371)+~P1(x1373)+~P1(x1372)+~P3(x1371,x1373)+~E(x1373,f16(x1371,x1372))+E(x1371,a1)+E(x1372,f19(x1373,x1371)) % 59.97/60.03 [147]~P1(x1472)+~P1(x1471)+~P1(x1473)+~P5(x1471,x1472)+E(x1471,x1472)+P5(f16(x1473,x1471),f16(x1473,x1472))+E(x1473,a1) % 59.97/60.03 [148]~P1(x1482)+~P1(x1483)+~P1(x1481)+~P5(x1481,x1482)+E(x1481,x1482)+P5(f16(x1481,x1483),f16(x1482,x1483))+E(x1483,a1) % 59.97/60.03 [154]~P1(x1542)+~P1(x1543)+~P1(x1541)+~P2(x1541)+P3(x1541,x1542)+P3(x1541,x1543)+~P3(x1541,f16(x1542,x1543))+~P4(f17(f17(x1542,x1543),x1541),f17(f17(a21,a22),a24)) % 59.97/60.03 [165]~P1(x1651)+~P1(x1653)+~P1(x1652)+~P2(x1651)+P3(x1651,x1652)+~P3(x1651,f16(x1652,x1653))+P1(f13(x1652,x1653,x1651))+~P4(f17(f17(x1652,x1653),x1651),f17(f17(a21,a22),a24)) % 59.97/60.03 [166]~P1(x1663)+~P1(x1662)+~P1(x1661)+~P2(x1661)+P3(x1661,x1662)+~P3(x1661,f16(x1663,x1662))+P1(f14(x1663,x1662,x1661))+~P4(f17(f17(x1663,x1662),x1661),f17(f17(a21,a22),a24)) % 59.97/60.03 [170]P3(x1701,x1703)+~P1(x1702)+~P1(x1703)+~P1(x1701)+~P2(x1701)+~P3(x1701,f16(x1702,x1703))+E(f16(x1701,f14(x1702,x1703,x1701)),x1702)+~P4(f17(f17(x1702,x1703),x1701),f17(f17(a21,a22),a24)) % 59.97/60.03 [171]P3(x1711,x1712)+~P1(x1712)+~P1(x1711)+~P1(x1713)+~P2(x1711)+~P3(x1711,f16(x1712,x1713))+E(f16(x1711,f13(x1712,x1713,x1711)),x1713)+~P4(f17(f17(x1712,x1713),x1711),f17(f17(a21,a22),a24)) % 59.97/60.03 [196]~P1(x1963)+~P1(x1962)+~P1(x1961)+~P2(x1963)+~P3(x1963,f16(x1961,x1962))+P1(f13(x1961,x1962,x1963))+~P4(f17(f17(x1961,x1962),x1963),f17(f17(a21,a22),a24))+P1(f14(x1961,x1962,x1963)) % 59.97/60.03 [208]~P1(x2081)+~P1(x2083)+~P1(x2082)+~P2(x2081)+~P3(x2081,f16(x2082,x2083))+P1(f13(x2082,x2083,x2081))+~P4(f17(f17(x2082,x2083),x2081),f17(f17(a21,a22),a24))+E(f16(x2081,f14(x2082,x2083,x2081)),x2082) % 59.97/60.03 [209]~P1(x2092)+~P1(x2091)+~P1(x2093)+~P2(x2091)+~P3(x2091,f16(x2092,x2093))+P1(f14(x2092,x2093,x2091))+~P4(f17(f17(x2092,x2093),x2091),f17(f17(a21,a22),a24))+E(f16(x2091,f13(x2092,x2093,x2091)),x2093) % 59.97/60.03 [219]~P1(x2192)+~P1(x2191)+~P1(x2193)+~P2(x2191)+~P3(x2191,f16(x2192,x2193))+E(f16(x2191,f13(x2192,x2193,x2191)),x2193)+~P4(f17(f17(x2192,x2193),x2191),f17(f17(a21,a22),a24))+E(f16(x2191,f14(x2192,x2193,x2191)),x2192) % 59.97/60.03 [153]~P1(x1534)+~P1(x1532)+~P1(x1533)+~P1(x1531)+~P2(x1531)+P3(x1531,x1532)+P3(x1531,x1533)+~E(f16(x1531,x1534),f16(x1532,x1533))+~P4(f17(f17(x1532,x1533),x1531),f17(f17(a21,a22),a24)) % 59.97/60.03 [159]~P1(x1594)+~P1(x1591)+~P1(x1593)+~P1(x1592)+~P2(x1591)+P3(x1591,x1592)+~E(f16(x1592,x1593),f16(x1591,x1594))+P1(f13(x1592,x1593,x1591))+~P4(f17(f17(x1592,x1593),x1591),f17(f17(a21,a22),a24)) % 59.97/60.03 [160]~P1(x1604)+~P1(x1603)+~P1(x1602)+~P1(x1601)+~P2(x1601)+P3(x1601,x1602)+~E(f16(x1601,x1604),f16(x1603,x1602))+P1(f14(x1603,x1602,x1601))+~P4(f17(f17(x1603,x1602),x1601),f17(f17(a21,a22),a24)) % 59.97/60.03 [163]P3(x1631,x1633)+~P1(x1634)+~P1(x1632)+~P1(x1633)+~P1(x1631)+~P2(x1631)+~E(f16(x1631,x1634),f16(x1632,x1633))+E(f16(x1631,f14(x1632,x1633,x1631)),x1632)+~P4(f17(f17(x1632,x1633),x1631),f17(f17(a21,a22),a24)) % 59.97/60.03 [164]P3(x1641,x1642)+~P1(x1644)+~P1(x1642)+~P1(x1641)+~P1(x1643)+~P2(x1641)+~E(f16(x1641,x1644),f16(x1642,x1643))+E(f16(x1641,f13(x1642,x1643,x1641)),x1643)+~P4(f17(f17(x1642,x1643),x1641),f17(f17(a21,a22),a24)) % 59.97/60.03 [185]~P1(x1854)+~P1(x1853)+~P1(x1852)+~P1(x1851)+~P2(x1853)+~E(f16(x1851,x1852),f16(x1853,x1854))+P1(f13(x1851,x1852,x1853))+~P4(f17(f17(x1851,x1852),x1853),f17(f17(a21,a22),a24))+P1(f14(x1851,x1852,x1853)) % 59.97/60.03 [194]~P1(x1944)+~P1(x1941)+~P1(x1943)+~P1(x1942)+~P2(x1941)+~E(f16(x1942,x1943),f16(x1941,x1944))+P1(f13(x1942,x1943,x1941))+~P4(f17(f17(x1942,x1943),x1941),f17(f17(a21,a22),a24))+E(f16(x1941,f14(x1942,x1943,x1941)),x1942) % 59.97/60.03 [195]~P1(x1954)+~P1(x1952)+~P1(x1951)+~P1(x1953)+~P2(x1951)+~E(f16(x1951,x1954),f16(x1952,x1953))+P1(f14(x1952,x1953,x1951))+~P4(f17(f17(x1952,x1953),x1951),f17(f17(a21,a22),a24))+E(f16(x1951,f13(x1952,x1953,x1951)),x1953) % 59.97/60.03 [203]~P1(x2034)+~P1(x2032)+~P1(x2031)+~P1(x2033)+~P2(x2031)+~E(f16(x2031,x2034),f16(x2032,x2033))+E(f16(x2031,f13(x2032,x2033,x2031)),x2033)+~P4(f17(f17(x2032,x2033),x2031),f17(f17(a21,a22),a24))+E(f16(x2031,f14(x2032,x2033,x2031)),x2032) % 59.97/60.03 [157]~P1(x1572)+~P1(x1573)+~P1(x1571)+P3(x1571,x1572)+P3(x1571,x1573)+E(x1571,a20)+~P3(x1571,f16(x1572,x1573))+E(x1571,a1)+~E(f12(x1572,x1573,x1571),a20)+~P4(f17(f17(x1572,x1573),x1571),f17(f17(a21,a22),a24)) % 59.97/60.03 [158]~P1(x1582)+~P1(x1583)+~P1(x1581)+P3(x1581,x1582)+P3(x1581,x1583)+E(x1581,a20)+~E(f12(x1582,x1583,x1581),x1581)+~P3(x1581,f16(x1582,x1583))+E(x1581,a1)+~P4(f17(f17(x1582,x1583),x1581),f17(f17(a21,a22),a24)) % 59.97/60.03 [168]~P1(x1682)+~P1(x1683)+~P1(x1681)+P3(x1681,x1682)+P3(x1681,x1683)+E(x1681,a20)+~P3(x1681,f16(x1682,x1683))+E(x1681,a1)+P1(f12(x1682,x1683,x1681))+~P4(f17(f17(x1682,x1683),x1681),f17(f17(a21,a22),a24)) % 59.97/60.03 [169]~P1(x1692)+~P1(x1693)+~P1(x1691)+P3(x1691,x1692)+P3(x1691,x1693)+E(x1691,a20)+~P3(x1691,f16(x1692,x1693))+E(x1691,a1)+P1(f15(x1692,x1693,x1691))+~P4(f17(f17(x1692,x1693),x1691),f17(f17(a21,a22),a24)) % 59.97/60.03 [172]~P1(x1722)+~P1(x1723)+~P1(x1721)+P3(x1721,x1722)+P3(x1721,x1723)+E(x1721,a20)+P3(f12(x1722,x1723,x1721),x1721)+~P3(x1721,f16(x1722,x1723))+E(x1721,a1)+~P4(f17(f17(x1722,x1723),x1721),f17(f17(a21,a22),a24)) % 59.97/60.03 [181]~P1(x1811)+~P1(x1813)+~P1(x1812)+P3(x1811,x1812)+E(x1811,a20)+~P3(x1811,f16(x1812,x1813))+E(x1811,a1)+~E(f12(x1812,x1813,x1811),a20)+~P4(f17(f17(x1812,x1813),x1811),f17(f17(a21,a22),a24))+P1(f13(x1812,x1813,x1811)) % 59.97/60.03 [182]~P1(x1823)+~P1(x1822)+~P1(x1821)+P3(x1821,x1822)+E(x1821,a20)+~P3(x1821,f16(x1823,x1822))+E(x1821,a1)+~E(f12(x1823,x1822,x1821),a20)+~P4(f17(f17(x1823,x1822),x1821),f17(f17(a21,a22),a24))+P1(f14(x1823,x1822,x1821)) % 59.97/60.03 [183]~P1(x1831)+~P1(x1833)+~P1(x1832)+P3(x1831,x1832)+E(x1831,a20)+~E(f12(x1832,x1833,x1831),x1831)+~P3(x1831,f16(x1832,x1833))+E(x1831,a1)+~P4(f17(f17(x1832,x1833),x1831),f17(f17(a21,a22),a24))+P1(f13(x1832,x1833,x1831)) % 59.97/60.03 [184]~P1(x1843)+~P1(x1842)+~P1(x1841)+P3(x1841,x1842)+E(x1841,a20)+~E(f12(x1843,x1842,x1841),x1841)+~P3(x1841,f16(x1843,x1842))+E(x1841,a1)+~P4(f17(f17(x1843,x1842),x1841),f17(f17(a21,a22),a24))+P1(f14(x1843,x1842,x1841)) % 59.97/60.03 [186]P3(x1861,x1862)+~P1(x1862)+~P1(x1861)+~P1(x1863)+E(x1861,a20)+~P3(x1861,f16(x1862,x1863))+E(x1861,a1)+~E(f12(x1862,x1863,x1861),a20)+~P4(f17(f17(x1862,x1863),x1861),f17(f17(a21,a22),a24))+E(f16(x1861,f13(x1862,x1863,x1861)),x1863) % 59.97/60.03 [187]P3(x1871,x1873)+~P1(x1872)+~P1(x1873)+~P1(x1871)+E(x1871,a20)+~P3(x1871,f16(x1872,x1873))+E(x1871,a1)+~E(f12(x1872,x1873,x1871),a20)+~P4(f17(f17(x1872,x1873),x1871),f17(f17(a21,a22),a24))+E(f16(x1871,f14(x1872,x1873,x1871)),x1872) % 59.97/60.03 [188]P3(x1881,x1882)+~P1(x1882)+~P1(x1881)+~P1(x1883)+E(x1881,a20)+~E(f12(x1882,x1883,x1881),x1881)+~P3(x1881,f16(x1882,x1883))+E(x1881,a1)+~P4(f17(f17(x1882,x1883),x1881),f17(f17(a21,a22),a24))+E(f16(x1881,f13(x1882,x1883,x1881)),x1883) % 59.97/60.03 [189]P3(x1891,x1893)+~P1(x1892)+~P1(x1893)+~P1(x1891)+E(x1891,a20)+~E(f12(x1892,x1893,x1891),x1891)+~P3(x1891,f16(x1892,x1893))+E(x1891,a1)+~P4(f17(f17(x1892,x1893),x1891),f17(f17(a21,a22),a24))+E(f16(x1891,f14(x1892,x1893,x1891)),x1892) % 59.97/60.03 [204]~P1(x2041)+~P1(x2043)+~P1(x2042)+P3(x2041,x2042)+E(x2041,a20)+~P3(x2041,f16(x2042,x2043))+E(x2041,a1)+P1(f13(x2042,x2043,x2041))+~P4(f17(f17(x2042,x2043),x2041),f17(f17(a21,a22),a24))+P1(f12(x2042,x2043,x2041)) % 59.97/60.03 [205]~P1(x2051)+~P1(x2053)+~P1(x2052)+P3(x2051,x2052)+E(x2051,a20)+~P3(x2051,f16(x2052,x2053))+E(x2051,a1)+P1(f13(x2052,x2053,x2051))+~P4(f17(f17(x2052,x2053),x2051),f17(f17(a21,a22),a24))+P1(f15(x2052,x2053,x2051)) % 59.97/60.03 [206]~P1(x2063)+~P1(x2062)+~P1(x2061)+P3(x2061,x2062)+E(x2061,a20)+~P3(x2061,f16(x2063,x2062))+E(x2061,a1)+P1(f14(x2063,x2062,x2061))+~P4(f17(f17(x2063,x2062),x2061),f17(f17(a21,a22),a24))+P1(f12(x2063,x2062,x2061)) % 59.97/60.03 [207]~P1(x2073)+~P1(x2072)+~P1(x2071)+P3(x2071,x2072)+E(x2071,a20)+~P3(x2071,f16(x2073,x2072))+E(x2071,a1)+P1(f14(x2073,x2072,x2071))+~P4(f17(f17(x2073,x2072),x2071),f17(f17(a21,a22),a24))+P1(f15(x2073,x2072,x2071)) % 59.97/60.03 [213]~P1(x2131)+~P1(x2133)+~P1(x2132)+P3(x2131,x2132)+E(x2131,a20)+P3(f12(x2132,x2133,x2131),x2131)+~P3(x2131,f16(x2132,x2133))+E(x2131,a1)+~P4(f17(f17(x2132,x2133),x2131),f17(f17(a21,a22),a24))+P1(f13(x2132,x2133,x2131)) % 59.97/60.03 [214]~P1(x2143)+~P1(x2142)+~P1(x2141)+P3(x2141,x2142)+E(x2141,a20)+P3(f12(x2143,x2142,x2141),x2141)+~P3(x2141,f16(x2143,x2142))+E(x2141,a1)+~P4(f17(f17(x2143,x2142),x2141),f17(f17(a21,a22),a24))+P1(f14(x2143,x2142,x2141)) % 59.97/60.03 [215]P3(x2151,x2152)+~P1(x2152)+~P1(x2151)+~P1(x2153)+E(x2151,a20)+~P3(x2151,f16(x2152,x2153))+E(x2151,a1)+P1(f12(x2152,x2153,x2151))+~P4(f17(f17(x2152,x2153),x2151),f17(f17(a21,a22),a24))+E(f16(x2151,f13(x2152,x2153,x2151)),x2153) % 59.97/60.03 [216]P3(x2161,x2162)+~P1(x2162)+~P1(x2161)+~P1(x2163)+E(x2161,a20)+~P3(x2161,f16(x2162,x2163))+E(x2161,a1)+P1(f15(x2162,x2163,x2161))+~P4(f17(f17(x2162,x2163),x2161),f17(f17(a21,a22),a24))+E(f16(x2161,f13(x2162,x2163,x2161)),x2163) % 59.97/60.03 [217]P3(x2171,x2173)+~P1(x2172)+~P1(x2173)+~P1(x2171)+E(x2171,a20)+~P3(x2171,f16(x2172,x2173))+E(x2171,a1)+P1(f12(x2172,x2173,x2171))+~P4(f17(f17(x2172,x2173),x2171),f17(f17(a21,a22),a24))+E(f16(x2171,f14(x2172,x2173,x2171)),x2172) % 59.97/60.03 [218]P3(x2181,x2183)+~P1(x2182)+~P1(x2183)+~P1(x2181)+E(x2181,a20)+~P3(x2181,f16(x2182,x2183))+E(x2181,a1)+P1(f15(x2182,x2183,x2181))+~P4(f17(f17(x2182,x2183),x2181),f17(f17(a21,a22),a24))+E(f16(x2181,f14(x2182,x2183,x2181)),x2182) % 59.97/60.03 [220]P3(x2201,x2202)+~P1(x2202)+~P1(x2201)+~P1(x2203)+E(x2201,a20)+P3(f12(x2202,x2203,x2201),x2201)+~P3(x2201,f16(x2202,x2203))+E(x2201,a1)+~P4(f17(f17(x2202,x2203),x2201),f17(f17(a21,a22),a24))+E(f16(x2201,f13(x2202,x2203,x2201)),x2203) % 59.97/60.03 [221]P3(x2211,x2213)+~P1(x2212)+~P1(x2213)+~P1(x2211)+E(x2211,a20)+P3(f12(x2212,x2213,x2211),x2211)+~P3(x2211,f16(x2212,x2213))+E(x2211,a1)+~P4(f17(f17(x2212,x2213),x2211),f17(f17(a21,a22),a24))+E(f16(x2211,f14(x2212,x2213,x2211)),x2212) % 59.97/60.03 [222]P3(x2221,x2222)+P3(x2221,x2223)+~P1(x2222)+~P1(x2223)+~P1(x2221)+E(x2221,a20)+~P3(x2221,f16(x2222,x2223))+E(x2221,a1)+~P4(f17(f17(x2222,x2223),x2221),f17(f17(a21,a22),a24))+E(f16(f12(x2222,x2223,x2221),f15(x2222,x2223,x2221)),x2221) % 59.97/60.03 [229]~P1(x2291)+~P1(x2293)+~P1(x2292)+E(x2291,a20)+~P3(x2291,f16(x2292,x2293))+E(x2291,a1)+P1(f13(x2292,x2293,x2291))+~E(f12(x2292,x2293,x2291),a20)+~P4(f17(f17(x2292,x2293),x2291),f17(f17(a21,a22),a24))+P1(f14(x2292,x2293,x2291)) % 59.97/60.03 [230]~P1(x2301)+~P1(x2303)+~P1(x2302)+E(x2301,a20)+~E(f12(x2302,x2303,x2301),x2301)+~P3(x2301,f16(x2302,x2303))+E(x2301,a1)+P1(f13(x2302,x2303,x2301))+~P4(f17(f17(x2302,x2303),x2301),f17(f17(a21,a22),a24))+P1(f14(x2302,x2303,x2301)) % 59.97/60.03 [233]~P1(x2331)+~P1(x2333)+~P1(x2332)+E(x2331,a20)+~P3(x2331,f16(x2332,x2333))+E(x2331,a1)+P1(f13(x2332,x2333,x2331))+~E(f12(x2332,x2333,x2331),a20)+~P4(f17(f17(x2332,x2333),x2331),f17(f17(a21,a22),a24))+E(f16(x2331,f14(x2332,x2333,x2331)),x2332) % 59.97/60.03 [234]~P1(x2342)+~P1(x2341)+~P1(x2343)+E(x2341,a20)+~P3(x2341,f16(x2342,x2343))+E(x2341,a1)+P1(f14(x2342,x2343,x2341))+~E(f12(x2342,x2343,x2341),a20)+~P4(f17(f17(x2342,x2343),x2341),f17(f17(a21,a22),a24))+E(f16(x2341,f13(x2342,x2343,x2341)),x2343) % 59.97/60.03 [235]~P1(x2351)+~P1(x2353)+~P1(x2352)+E(x2351,a20)+~E(f12(x2352,x2353,x2351),x2351)+~P3(x2351,f16(x2352,x2353))+E(x2351,a1)+P1(f13(x2352,x2353,x2351))+~P4(f17(f17(x2352,x2353),x2351),f17(f17(a21,a22),a24))+E(f16(x2351,f14(x2352,x2353,x2351)),x2352) % 59.97/60.03 [236]~P1(x2362)+~P1(x2361)+~P1(x2363)+E(x2361,a20)+~E(f12(x2362,x2363,x2361),x2361)+~P3(x2361,f16(x2362,x2363))+E(x2361,a1)+P1(f14(x2362,x2363,x2361))+~P4(f17(f17(x2362,x2363),x2361),f17(f17(a21,a22),a24))+E(f16(x2361,f13(x2362,x2363,x2361)),x2363) % 59.97/60.03 [239]~P1(x2392)+~P1(x2391)+~P1(x2393)+E(x2391,a20)+~P3(x2391,f16(x2392,x2393))+E(x2391,a1)+E(f16(x2391,f13(x2392,x2393,x2391)),x2393)+~E(f12(x2392,x2393,x2391),a20)+~P4(f17(f17(x2392,x2393),x2391),f17(f17(a21,a22),a24))+E(f16(x2391,f14(x2392,x2393,x2391)),x2392) % 59.97/60.03 [240]~P1(x2402)+~P1(x2401)+~P1(x2403)+E(x2401,a20)+~E(f12(x2402,x2403,x2401),x2401)+~P3(x2401,f16(x2402,x2403))+E(x2401,a1)+E(f16(x2401,f13(x2402,x2403,x2401)),x2403)+~P4(f17(f17(x2402,x2403),x2401),f17(f17(a21,a22),a24))+E(f16(x2401,f14(x2402,x2403,x2401)),x2402) % 59.97/60.03 [246]~P1(x2461)+~P1(x2463)+~P1(x2462)+E(x2461,a20)+~P3(x2461,f16(x2462,x2463))+E(x2461,a1)+P1(f14(x2462,x2463,x2461))+P1(f13(x2462,x2463,x2461))+~P4(f17(f17(x2462,x2463),x2461),f17(f17(a21,a22),a24))+P1(f12(x2462,x2463,x2461)) % 59.97/60.03 [247]~P1(x2471)+~P1(x2473)+~P1(x2472)+E(x2471,a20)+~P3(x2471,f16(x2472,x2473))+E(x2471,a1)+P1(f14(x2472,x2473,x2471))+P1(f13(x2472,x2473,x2471))+~P4(f17(f17(x2472,x2473),x2471),f17(f17(a21,a22),a24))+P1(f15(x2472,x2473,x2471)) % 59.97/60.03 [254]~P1(x2541)+~P1(x2543)+~P1(x2542)+E(x2541,a20)+P3(f12(x2542,x2543,x2541),x2541)+~P3(x2541,f16(x2542,x2543))+E(x2541,a1)+P1(f13(x2542,x2543,x2541))+~P4(f17(f17(x2542,x2543),x2541),f17(f17(a21,a22),a24))+P1(f14(x2542,x2543,x2541)) % 59.97/60.03 [255]~P1(x2551)+~P1(x2553)+~P1(x2552)+E(x2551,a20)+~P3(x2551,f16(x2552,x2553))+E(x2551,a1)+P1(f12(x2552,x2553,x2551))+P1(f13(x2552,x2553,x2551))+~P4(f17(f17(x2552,x2553),x2551),f17(f17(a21,a22),a24))+E(f16(x2551,f14(x2552,x2553,x2551)),x2552) % 59.97/60.03 [256]~P1(x2561)+~P1(x2563)+~P1(x2562)+E(x2561,a20)+~P3(x2561,f16(x2562,x2563))+E(x2561,a1)+P1(f15(x2562,x2563,x2561))+P1(f13(x2562,x2563,x2561))+~P4(f17(f17(x2562,x2563),x2561),f17(f17(a21,a22),a24))+E(f16(x2561,f14(x2562,x2563,x2561)),x2562) % 59.97/60.03 [257]~P1(x2572)+~P1(x2571)+~P1(x2573)+E(x2571,a20)+~P3(x2571,f16(x2572,x2573))+E(x2571,a1)+P1(f12(x2572,x2573,x2571))+P1(f14(x2572,x2573,x2571))+~P4(f17(f17(x2572,x2573),x2571),f17(f17(a21,a22),a24))+E(f16(x2571,f13(x2572,x2573,x2571)),x2573) % 59.97/60.03 [258]~P1(x2582)+~P1(x2581)+~P1(x2583)+E(x2581,a20)+~P3(x2581,f16(x2582,x2583))+E(x2581,a1)+P1(f15(x2582,x2583,x2581))+P1(f14(x2582,x2583,x2581))+~P4(f17(f17(x2582,x2583),x2581),f17(f17(a21,a22),a24))+E(f16(x2581,f13(x2582,x2583,x2581)),x2583) % 59.97/60.03 [262]~P1(x2621)+~P1(x2623)+~P1(x2622)+E(x2621,a20)+P3(f12(x2622,x2623,x2621),x2621)+~P3(x2621,f16(x2622,x2623))+E(x2621,a1)+P1(f13(x2622,x2623,x2621))+~P4(f17(f17(x2622,x2623),x2621),f17(f17(a21,a22),a24))+E(f16(x2621,f14(x2622,x2623,x2621)),x2622) % 59.97/60.03 [263]~P1(x2632)+~P1(x2631)+~P1(x2633)+E(x2631,a20)+P3(f12(x2632,x2633,x2631),x2631)+~P3(x2631,f16(x2632,x2633))+E(x2631,a1)+P1(f14(x2632,x2633,x2631))+~P4(f17(f17(x2632,x2633),x2631),f17(f17(a21,a22),a24))+E(f16(x2631,f13(x2632,x2633,x2631)),x2633) % 59.97/60.03 [264]P3(x2641,x2642)+~P1(x2641)+~P1(x2643)+~P1(x2642)+E(x2641,a20)+~P3(x2641,f16(x2642,x2643))+E(x2641,a1)+P1(f13(x2642,x2643,x2641))+~P4(f17(f17(x2642,x2643),x2641),f17(f17(a21,a22),a24))+E(f16(f12(x2642,x2643,x2641),f15(x2642,x2643,x2641)),x2641) % 59.97/60.03 [265]P3(x2651,x2653)+~P1(x2652)+~P1(x2653)+~P1(x2651)+E(x2651,a20)+~P3(x2651,f16(x2652,x2653))+E(x2651,a1)+P1(f14(x2652,x2653,x2651))+~P4(f17(f17(x2652,x2653),x2651),f17(f17(a21,a22),a24))+E(f16(f12(x2652,x2653,x2651),f15(x2652,x2653,x2651)),x2651) % 59.97/60.03 [266]~P1(x2662)+~P1(x2661)+~P1(x2663)+E(x2661,a20)+~P3(x2661,f16(x2662,x2663))+E(x2661,a1)+E(f16(x2661,f13(x2662,x2663,x2661)),x2663)+P1(f12(x2662,x2663,x2661))+~P4(f17(f17(x2662,x2663),x2661),f17(f17(a21,a22),a24))+E(f16(x2661,f14(x2662,x2663,x2661)),x2662) % 59.97/60.03 [267]~P1(x2672)+~P1(x2671)+~P1(x2673)+E(x2671,a20)+~P3(x2671,f16(x2672,x2673))+E(x2671,a1)+E(f16(x2671,f13(x2672,x2673,x2671)),x2673)+P1(f15(x2672,x2673,x2671))+~P4(f17(f17(x2672,x2673),x2671),f17(f17(a21,a22),a24))+E(f16(x2671,f14(x2672,x2673,x2671)),x2672) % 59.97/60.03 [268]~P1(x2682)+~P1(x2681)+~P1(x2683)+E(x2681,a20)+P3(f12(x2682,x2683,x2681),x2681)+~P3(x2681,f16(x2682,x2683))+E(x2681,a1)+E(f16(x2681,f13(x2682,x2683,x2681)),x2683)+~P4(f17(f17(x2682,x2683),x2681),f17(f17(a21,a22),a24))+E(f16(x2681,f14(x2682,x2683,x2681)),x2682) % 59.97/60.03 [269]P3(x2691,x2692)+~P1(x2692)+~P1(x2691)+~P1(x2693)+E(x2691,a20)+~P3(x2691,f16(x2692,x2693))+E(x2691,a1)+E(f16(f12(x2692,x2693,x2691),f15(x2692,x2693,x2691)),x2691)+~P4(f17(f17(x2692,x2693),x2691),f17(f17(a21,a22),a24))+E(f16(x2691,f13(x2692,x2693,x2691)),x2693) % 59.97/60.03 [270]P3(x2701,x2703)+~P1(x2702)+~P1(x2703)+~P1(x2701)+E(x2701,a20)+~P3(x2701,f16(x2702,x2703))+E(x2701,a1)+E(f16(f12(x2702,x2703,x2701),f15(x2702,x2703,x2701)),x2701)+~P4(f17(f17(x2702,x2703),x2701),f17(f17(a21,a22),a24))+E(f16(x2701,f14(x2702,x2703,x2701)),x2702) % 59.97/60.03 [274]~P1(x2741)+~P1(x2743)+~P1(x2742)+E(x2741,a20)+~P3(x2741,f16(x2742,x2743))+E(x2741,a1)+P1(f14(x2742,x2743,x2741))+P1(f13(x2742,x2743,x2741))+~P4(f17(f17(x2742,x2743),x2741),f17(f17(a21,a22),a24))+E(f16(f12(x2742,x2743,x2741),f15(x2742,x2743,x2741)),x2741) % 59.97/60.03 [276]~P1(x2761)+~P1(x2763)+~P1(x2762)+E(x2761,a20)+~P3(x2761,f16(x2762,x2763))+E(x2761,a1)+E(f16(f12(x2762,x2763,x2761),f15(x2762,x2763,x2761)),x2761)+P1(f13(x2762,x2763,x2761))+~P4(f17(f17(x2762,x2763),x2761),f17(f17(a21,a22),a24))+E(f16(x2761,f14(x2762,x2763,x2761)),x2762) % 59.97/60.03 [277]~P1(x2772)+~P1(x2771)+~P1(x2773)+E(x2771,a20)+~P3(x2771,f16(x2772,x2773))+E(x2771,a1)+E(f16(f12(x2772,x2773,x2771),f15(x2772,x2773,x2771)),x2771)+P1(f14(x2772,x2773,x2771))+~P4(f17(f17(x2772,x2773),x2771),f17(f17(a21,a22),a24))+E(f16(x2771,f13(x2772,x2773,x2771)),x2773) % 59.97/60.03 [278]~P1(x2782)+~P1(x2781)+~P1(x2783)+E(x2781,a20)+~P3(x2781,f16(x2782,x2783))+E(x2781,a1)+E(f16(x2781,f13(x2782,x2783,x2781)),x2783)+E(f16(f12(x2782,x2783,x2781),f15(x2782,x2783,x2781)),x2781)+~P4(f17(f17(x2782,x2783),x2781),f17(f17(a21,a22),a24))+E(f16(x2781,f14(x2782,x2783,x2781)),x2782) % 59.97/60.03 [155]~P1(x1554)+~P1(x1552)+~P1(x1553)+~P1(x1551)+P3(x1551,x1552)+P3(x1551,x1553)+E(x1551,a20)+E(x1551,a1)+~E(f16(x1551,x1554),f16(x1552,x1553))+~E(f12(x1552,x1553,x1551),a20)+~P4(f17(f17(x1552,x1553),x1551),f17(f17(a21,a22),a24)) % 59.97/60.03 [156]~P1(x1564)+~P1(x1562)+~P1(x1563)+~P1(x1561)+P3(x1561,x1562)+P3(x1561,x1563)+E(x1561,a20)+~E(f12(x1562,x1563,x1561),x1561)+E(x1561,a1)+~E(f16(x1561,x1564),f16(x1562,x1563))+~P4(f17(f17(x1562,x1563),x1561),f17(f17(a21,a22),a24)) % 59.97/60.03 [161]~P1(x1614)+~P1(x1612)+~P1(x1613)+~P1(x1611)+P3(x1611,x1612)+P3(x1611,x1613)+E(x1611,a20)+E(x1611,a1)+~E(f16(x1611,x1614),f16(x1612,x1613))+P1(f12(x1612,x1613,x1611))+~P4(f17(f17(x1612,x1613),x1611),f17(f17(a21,a22),a24)) % 59.97/60.03 [162]~P1(x1624)+~P1(x1622)+~P1(x1623)+~P1(x1621)+P3(x1621,x1622)+P3(x1621,x1623)+E(x1621,a20)+E(x1621,a1)+~E(f16(x1621,x1624),f16(x1622,x1623))+P1(f15(x1622,x1623,x1621))+~P4(f17(f17(x1622,x1623),x1621),f17(f17(a21,a22),a24)) % 59.97/60.03 [167]~P1(x1674)+~P1(x1672)+~P1(x1673)+~P1(x1671)+P3(x1671,x1672)+P3(x1671,x1673)+E(x1671,a20)+P3(f12(x1672,x1673,x1671),x1671)+E(x1671,a1)+~E(f16(x1671,x1674),f16(x1672,x1673))+~P4(f17(f17(x1672,x1673),x1671),f17(f17(a21,a22),a24)) % 59.97/60.03 [173]~P1(x1734)+~P1(x1731)+~P1(x1733)+~P1(x1732)+P3(x1731,x1732)+E(x1731,a20)+E(x1731,a1)+~E(f16(x1732,x1733),f16(x1731,x1734))+~E(f12(x1732,x1733,x1731),a20)+P1(f13(x1732,x1733,x1731))+~P4(f17(f17(x1732,x1733),x1731),f17(f17(a21,a22),a24)) % 59.97/60.03 [174]~P1(x1744)+~P1(x1743)+~P1(x1742)+~P1(x1741)+P3(x1741,x1742)+E(x1741,a20)+E(x1741,a1)+~E(f16(x1741,x1744),f16(x1743,x1742))+~E(f12(x1743,x1742,x1741),a20)+P1(f14(x1743,x1742,x1741))+~P4(f17(f17(x1743,x1742),x1741),f17(f17(a21,a22),a24)) % 59.97/60.03 [175]~P1(x1754)+~P1(x1751)+~P1(x1753)+~P1(x1752)+P3(x1751,x1752)+E(x1751,a20)+~E(f12(x1752,x1753,x1751),x1751)+E(x1751,a1)+~E(f16(x1752,x1753),f16(x1751,x1754))+~P4(f17(f17(x1752,x1753),x1751),f17(f17(a21,a22),a24))+P1(f13(x1752,x1753,x1751)) % 59.97/60.03 [176]~P1(x1764)+~P1(x1763)+~P1(x1762)+~P1(x1761)+P3(x1761,x1762)+E(x1761,a20)+~E(f12(x1763,x1762,x1761),x1761)+E(x1761,a1)+~E(f16(x1761,x1764),f16(x1763,x1762))+~P4(f17(f17(x1763,x1762),x1761),f17(f17(a21,a22),a24))+P1(f14(x1763,x1762,x1761)) % 59.97/60.03 [177]P3(x1771,x1772)+~P1(x1774)+~P1(x1772)+~P1(x1771)+~P1(x1773)+E(x1771,a20)+E(x1771,a1)+~E(f16(x1771,x1774),f16(x1772,x1773))+~E(f12(x1772,x1773,x1771),a20)+~P4(f17(f17(x1772,x1773),x1771),f17(f17(a21,a22),a24))+E(f16(x1771,f13(x1772,x1773,x1771)),x1773) % 59.97/60.03 [178]P3(x1781,x1783)+~P1(x1784)+~P1(x1782)+~P1(x1783)+~P1(x1781)+E(x1781,a20)+E(x1781,a1)+~E(f16(x1781,x1784),f16(x1782,x1783))+~E(f12(x1782,x1783,x1781),a20)+~P4(f17(f17(x1782,x1783),x1781),f17(f17(a21,a22),a24))+E(f16(x1781,f14(x1782,x1783,x1781)),x1782) % 59.97/60.03 [179]P3(x1791,x1792)+~P1(x1794)+~P1(x1792)+~P1(x1791)+~P1(x1793)+E(x1791,a20)+~E(f12(x1792,x1793,x1791),x1791)+E(x1791,a1)+~E(f16(x1791,x1794),f16(x1792,x1793))+~P4(f17(f17(x1792,x1793),x1791),f17(f17(a21,a22),a24))+E(f16(x1791,f13(x1792,x1793,x1791)),x1793) % 59.97/60.03 [180]P3(x1801,x1803)+~P1(x1804)+~P1(x1802)+~P1(x1803)+~P1(x1801)+E(x1801,a20)+~E(f12(x1802,x1803,x1801),x1801)+E(x1801,a1)+~E(f16(x1801,x1804),f16(x1802,x1803))+~P4(f17(f17(x1802,x1803),x1801),f17(f17(a21,a22),a24))+E(f16(x1801,f14(x1802,x1803,x1801)),x1802) % 59.97/60.03 [190]~P1(x1904)+~P1(x1901)+~P1(x1903)+~P1(x1902)+P3(x1901,x1902)+E(x1901,a20)+E(x1901,a1)+~E(f16(x1902,x1903),f16(x1901,x1904))+P1(f13(x1902,x1903,x1901))+~P4(f17(f17(x1902,x1903),x1901),f17(f17(a21,a22),a24))+P1(f12(x1902,x1903,x1901)) % 59.97/60.03 [191]~P1(x1914)+~P1(x1911)+~P1(x1913)+~P1(x1912)+P3(x1911,x1912)+E(x1911,a20)+E(x1911,a1)+~E(f16(x1912,x1913),f16(x1911,x1914))+P1(f13(x1912,x1913,x1911))+~P4(f17(f17(x1912,x1913),x1911),f17(f17(a21,a22),a24))+P1(f15(x1912,x1913,x1911)) % 59.97/60.03 [192]~P1(x1924)+~P1(x1923)+~P1(x1922)+~P1(x1921)+P3(x1921,x1922)+E(x1921,a20)+E(x1921,a1)+~E(f16(x1921,x1924),f16(x1923,x1922))+P1(f14(x1923,x1922,x1921))+~P4(f17(f17(x1923,x1922),x1921),f17(f17(a21,a22),a24))+P1(f12(x1923,x1922,x1921)) % 59.97/60.03 [193]~P1(x1934)+~P1(x1933)+~P1(x1932)+~P1(x1931)+P3(x1931,x1932)+E(x1931,a20)+E(x1931,a1)+~E(f16(x1931,x1934),f16(x1933,x1932))+P1(f14(x1933,x1932,x1931))+~P4(f17(f17(x1933,x1932),x1931),f17(f17(a21,a22),a24))+P1(f15(x1933,x1932,x1931)) % 59.97/60.03 [197]~P1(x1974)+~P1(x1971)+~P1(x1973)+~P1(x1972)+P3(x1971,x1972)+E(x1971,a20)+P3(f12(x1972,x1973,x1971),x1971)+E(x1971,a1)+~E(f16(x1972,x1973),f16(x1971,x1974))+~P4(f17(f17(x1972,x1973),x1971),f17(f17(a21,a22),a24))+P1(f13(x1972,x1973,x1971)) % 59.97/60.03 [198]~P1(x1984)+~P1(x1983)+~P1(x1982)+~P1(x1981)+P3(x1981,x1982)+E(x1981,a20)+P3(f12(x1983,x1982,x1981),x1981)+E(x1981,a1)+~E(f16(x1981,x1984),f16(x1983,x1982))+~P4(f17(f17(x1983,x1982),x1981),f17(f17(a21,a22),a24))+P1(f14(x1983,x1982,x1981)) % 59.97/60.03 [199]P3(x1991,x1992)+~P1(x1994)+~P1(x1992)+~P1(x1991)+~P1(x1993)+E(x1991,a20)+E(x1991,a1)+~E(f16(x1991,x1994),f16(x1992,x1993))+P1(f12(x1992,x1993,x1991))+~P4(f17(f17(x1992,x1993),x1991),f17(f17(a21,a22),a24))+E(f16(x1991,f13(x1992,x1993,x1991)),x1993) % 59.97/60.03 [200]P3(x2001,x2002)+~P1(x2004)+~P1(x2002)+~P1(x2001)+~P1(x2003)+E(x2001,a20)+E(x2001,a1)+~E(f16(x2001,x2004),f16(x2002,x2003))+P1(f15(x2002,x2003,x2001))+~P4(f17(f17(x2002,x2003),x2001),f17(f17(a21,a22),a24))+E(f16(x2001,f13(x2002,x2003,x2001)),x2003) % 59.97/60.03 [201]P3(x2011,x2013)+~P1(x2014)+~P1(x2012)+~P1(x2013)+~P1(x2011)+E(x2011,a20)+E(x2011,a1)+~E(f16(x2011,x2014),f16(x2012,x2013))+P1(f12(x2012,x2013,x2011))+~P4(f17(f17(x2012,x2013),x2011),f17(f17(a21,a22),a24))+E(f16(x2011,f14(x2012,x2013,x2011)),x2012) % 59.97/60.03 [202]P3(x2021,x2023)+~P1(x2024)+~P1(x2022)+~P1(x2023)+~P1(x2021)+E(x2021,a20)+E(x2021,a1)+~E(f16(x2021,x2024),f16(x2022,x2023))+P1(f15(x2022,x2023,x2021))+~P4(f17(f17(x2022,x2023),x2021),f17(f17(a21,a22),a24))+E(f16(x2021,f14(x2022,x2023,x2021)),x2022) % 59.97/60.03 [210]P3(x2101,x2102)+~P1(x2104)+~P1(x2102)+~P1(x2101)+~P1(x2103)+E(x2101,a20)+P3(f12(x2102,x2103,x2101),x2101)+E(x2101,a1)+~E(f16(x2101,x2104),f16(x2102,x2103))+~P4(f17(f17(x2102,x2103),x2101),f17(f17(a21,a22),a24))+E(f16(x2101,f13(x2102,x2103,x2101)),x2103) % 59.97/60.03 [211]P3(x2111,x2113)+~P1(x2114)+~P1(x2112)+~P1(x2113)+~P1(x2111)+E(x2111,a20)+P3(f12(x2112,x2113,x2111),x2111)+E(x2111,a1)+~E(f16(x2111,x2114),f16(x2112,x2113))+~P4(f17(f17(x2112,x2113),x2111),f17(f17(a21,a22),a24))+E(f16(x2111,f14(x2112,x2113,x2111)),x2112) % 59.97/60.03 [212]P3(x2121,x2122)+P3(x2121,x2123)+~P1(x2124)+~P1(x2122)+~P1(x2123)+~P1(x2121)+E(x2121,a20)+E(x2121,a1)+~E(f16(x2121,x2124),f16(x2122,x2123))+~P4(f17(f17(x2122,x2123),x2121),f17(f17(a21,a22),a24))+E(f16(f12(x2122,x2123,x2121),f15(x2122,x2123,x2121)),x2121) % 59.97/60.03 [223]~P1(x2234)+~P1(x2231)+~P1(x2233)+~P1(x2232)+E(x2231,a20)+E(x2231,a1)+~E(f16(x2232,x2233),f16(x2231,x2234))+P1(f13(x2232,x2233,x2231))+~E(f12(x2232,x2233,x2231),a20)+~P4(f17(f17(x2232,x2233),x2231),f17(f17(a21,a22),a24))+P1(f14(x2232,x2233,x2231)) % 59.97/60.03 [224]~P1(x2244)+~P1(x2241)+~P1(x2243)+~P1(x2242)+E(x2241,a20)+~E(f12(x2242,x2243,x2241),x2241)+E(x2241,a1)+~E(f16(x2242,x2243),f16(x2241,x2244))+P1(f13(x2242,x2243,x2241))+~P4(f17(f17(x2242,x2243),x2241),f17(f17(a21,a22),a24))+P1(f14(x2242,x2243,x2241)) % 59.97/60.03 [225]~P1(x2254)+~P1(x2251)+~P1(x2253)+~P1(x2252)+E(x2251,a20)+E(x2251,a1)+~E(f16(x2252,x2253),f16(x2251,x2254))+P1(f13(x2252,x2253,x2251))+~E(f12(x2252,x2253,x2251),a20)+~P4(f17(f17(x2252,x2253),x2251),f17(f17(a21,a22),a24))+E(f16(x2251,f14(x2252,x2253,x2251)),x2252) % 59.97/60.03 [226]~P1(x2264)+~P1(x2262)+~P1(x2261)+~P1(x2263)+E(x2261,a20)+E(x2261,a1)+~E(f16(x2261,x2264),f16(x2262,x2263))+P1(f14(x2262,x2263,x2261))+~E(f12(x2262,x2263,x2261),a20)+~P4(f17(f17(x2262,x2263),x2261),f17(f17(a21,a22),a24))+E(f16(x2261,f13(x2262,x2263,x2261)),x2263) % 59.97/60.03 [227]~P1(x2274)+~P1(x2271)+~P1(x2273)+~P1(x2272)+E(x2271,a20)+~E(f12(x2272,x2273,x2271),x2271)+E(x2271,a1)+~E(f16(x2272,x2273),f16(x2271,x2274))+P1(f13(x2272,x2273,x2271))+~P4(f17(f17(x2272,x2273),x2271),f17(f17(a21,a22),a24))+E(f16(x2271,f14(x2272,x2273,x2271)),x2272) % 59.97/60.03 [228]~P1(x2284)+~P1(x2282)+~P1(x2281)+~P1(x2283)+E(x2281,a20)+~E(f12(x2282,x2283,x2281),x2281)+E(x2281,a1)+~E(f16(x2281,x2284),f16(x2282,x2283))+P1(f14(x2282,x2283,x2281))+~P4(f17(f17(x2282,x2283),x2281),f17(f17(a21,a22),a24))+E(f16(x2281,f13(x2282,x2283,x2281)),x2283) % 59.97/60.03 [231]~P1(x2314)+~P1(x2312)+~P1(x2311)+~P1(x2313)+E(x2311,a20)+E(x2311,a1)+~E(f16(x2311,x2314),f16(x2312,x2313))+E(f16(x2311,f13(x2312,x2313,x2311)),x2313)+~E(f12(x2312,x2313,x2311),a20)+~P4(f17(f17(x2312,x2313),x2311),f17(f17(a21,a22),a24))+E(f16(x2311,f14(x2312,x2313,x2311)),x2312) % 59.97/60.03 [232]~P1(x2324)+~P1(x2322)+~P1(x2321)+~P1(x2323)+E(x2321,a20)+~E(f12(x2322,x2323,x2321),x2321)+E(x2321,a1)+~E(f16(x2321,x2324),f16(x2322,x2323))+E(f16(x2321,f13(x2322,x2323,x2321)),x2323)+~P4(f17(f17(x2322,x2323),x2321),f17(f17(a21,a22),a24))+E(f16(x2321,f14(x2322,x2323,x2321)),x2322) % 59.97/60.03 [237]~P1(x2374)+~P1(x2371)+~P1(x2373)+~P1(x2372)+E(x2371,a20)+E(x2371,a1)+~E(f16(x2372,x2373),f16(x2371,x2374))+P1(f14(x2372,x2373,x2371))+P1(f13(x2372,x2373,x2371))+~P4(f17(f17(x2372,x2373),x2371),f17(f17(a21,a22),a24))+P1(f12(x2372,x2373,x2371)) % 59.97/60.03 [238]~P1(x2384)+~P1(x2381)+~P1(x2383)+~P1(x2382)+E(x2381,a20)+E(x2381,a1)+~E(f16(x2382,x2383),f16(x2381,x2384))+P1(f14(x2382,x2383,x2381))+P1(f13(x2382,x2383,x2381))+~P4(f17(f17(x2382,x2383),x2381),f17(f17(a21,a22),a24))+P1(f15(x2382,x2383,x2381)) % 59.97/60.03 [241]~P1(x2414)+~P1(x2411)+~P1(x2413)+~P1(x2412)+E(x2411,a20)+P3(f12(x2412,x2413,x2411),x2411)+E(x2411,a1)+~E(f16(x2412,x2413),f16(x2411,x2414))+P1(f13(x2412,x2413,x2411))+~P4(f17(f17(x2412,x2413),x2411),f17(f17(a21,a22),a24))+P1(f14(x2412,x2413,x2411)) % 59.97/60.03 [242]~P1(x2424)+~P1(x2421)+~P1(x2423)+~P1(x2422)+E(x2421,a20)+E(x2421,a1)+~E(f16(x2422,x2423),f16(x2421,x2424))+P1(f12(x2422,x2423,x2421))+P1(f13(x2422,x2423,x2421))+~P4(f17(f17(x2422,x2423),x2421),f17(f17(a21,a22),a24))+E(f16(x2421,f14(x2422,x2423,x2421)),x2422) % 59.97/60.03 [243]~P1(x2434)+~P1(x2431)+~P1(x2433)+~P1(x2432)+E(x2431,a20)+E(x2431,a1)+~E(f16(x2432,x2433),f16(x2431,x2434))+P1(f15(x2432,x2433,x2431))+P1(f13(x2432,x2433,x2431))+~P4(f17(f17(x2432,x2433),x2431),f17(f17(a21,a22),a24))+E(f16(x2431,f14(x2432,x2433,x2431)),x2432) % 59.97/60.03 [244]~P1(x2444)+~P1(x2442)+~P1(x2441)+~P1(x2443)+E(x2441,a20)+E(x2441,a1)+~E(f16(x2441,x2444),f16(x2442,x2443))+P1(f12(x2442,x2443,x2441))+P1(f14(x2442,x2443,x2441))+~P4(f17(f17(x2442,x2443),x2441),f17(f17(a21,a22),a24))+E(f16(x2441,f13(x2442,x2443,x2441)),x2443) % 59.97/60.03 [245]~P1(x2454)+~P1(x2452)+~P1(x2451)+~P1(x2453)+E(x2451,a20)+E(x2451,a1)+~E(f16(x2451,x2454),f16(x2452,x2453))+P1(f15(x2452,x2453,x2451))+P1(f14(x2452,x2453,x2451))+~P4(f17(f17(x2452,x2453),x2451),f17(f17(a21,a22),a24))+E(f16(x2451,f13(x2452,x2453,x2451)),x2453) % 59.97/60.03 [248]~P1(x2484)+~P1(x2481)+~P1(x2483)+~P1(x2482)+E(x2481,a20)+P3(f12(x2482,x2483,x2481),x2481)+E(x2481,a1)+~E(f16(x2482,x2483),f16(x2481,x2484))+P1(f13(x2482,x2483,x2481))+~P4(f17(f17(x2482,x2483),x2481),f17(f17(a21,a22),a24))+E(f16(x2481,f14(x2482,x2483,x2481)),x2482) % 59.97/60.03 [249]~P1(x2494)+~P1(x2492)+~P1(x2491)+~P1(x2493)+E(x2491,a20)+P3(f12(x2492,x2493,x2491),x2491)+E(x2491,a1)+~E(f16(x2491,x2494),f16(x2492,x2493))+P1(f14(x2492,x2493,x2491))+~P4(f17(f17(x2492,x2493),x2491),f17(f17(a21,a22),a24))+E(f16(x2491,f13(x2492,x2493,x2491)),x2493) % 59.97/60.03 [250]P3(x2501,x2502)+~P1(x2504)+~P1(x2501)+~P1(x2503)+~P1(x2502)+E(x2501,a20)+E(x2501,a1)+~E(f16(x2502,x2503),f16(x2501,x2504))+P1(f13(x2502,x2503,x2501))+~P4(f17(f17(x2502,x2503),x2501),f17(f17(a21,a22),a24))+E(f16(f12(x2502,x2503,x2501),f15(x2502,x2503,x2501)),x2501) % 59.97/60.03 [251]P3(x2511,x2513)+~P1(x2514)+~P1(x2512)+~P1(x2513)+~P1(x2511)+E(x2511,a20)+E(x2511,a1)+~E(f16(x2511,x2514),f16(x2512,x2513))+P1(f14(x2512,x2513,x2511))+~P4(f17(f17(x2512,x2513),x2511),f17(f17(a21,a22),a24))+E(f16(f12(x2512,x2513,x2511),f15(x2512,x2513,x2511)),x2511) % 59.97/60.03 [252]~P1(x2524)+~P1(x2522)+~P1(x2521)+~P1(x2523)+E(x2521,a20)+E(x2521,a1)+~E(f16(x2521,x2524),f16(x2522,x2523))+E(f16(x2521,f13(x2522,x2523,x2521)),x2523)+P1(f12(x2522,x2523,x2521))+~P4(f17(f17(x2522,x2523),x2521),f17(f17(a21,a22),a24))+E(f16(x2521,f14(x2522,x2523,x2521)),x2522) % 59.97/60.03 [253]~P1(x2534)+~P1(x2532)+~P1(x2531)+~P1(x2533)+E(x2531,a20)+E(x2531,a1)+~E(f16(x2531,x2534),f16(x2532,x2533))+E(f16(x2531,f13(x2532,x2533,x2531)),x2533)+P1(f15(x2532,x2533,x2531))+~P4(f17(f17(x2532,x2533),x2531),f17(f17(a21,a22),a24))+E(f16(x2531,f14(x2532,x2533,x2531)),x2532) % 59.97/60.03 [259]~P1(x2594)+~P1(x2592)+~P1(x2591)+~P1(x2593)+E(x2591,a20)+P3(f12(x2592,x2593,x2591),x2591)+E(x2591,a1)+~E(f16(x2591,x2594),f16(x2592,x2593))+E(f16(x2591,f13(x2592,x2593,x2591)),x2593)+~P4(f17(f17(x2592,x2593),x2591),f17(f17(a21,a22),a24))+E(f16(x2591,f14(x2592,x2593,x2591)),x2592) % 59.97/60.03 [260]P3(x2601,x2602)+~P1(x2604)+~P1(x2602)+~P1(x2601)+~P1(x2603)+E(x2601,a20)+E(x2601,a1)+~E(f16(x2601,x2604),f16(x2602,x2603))+E(f16(f12(x2602,x2603,x2601),f15(x2602,x2603,x2601)),x2601)+~P4(f17(f17(x2602,x2603),x2601),f17(f17(a21,a22),a24))+E(f16(x2601,f13(x2602,x2603,x2601)),x2603) % 59.97/60.03 [261]P3(x2611,x2613)+~P1(x2614)+~P1(x2612)+~P1(x2613)+~P1(x2611)+E(x2611,a20)+E(x2611,a1)+~E(f16(x2611,x2614),f16(x2612,x2613))+E(f16(f12(x2612,x2613,x2611),f15(x2612,x2613,x2611)),x2611)+~P4(f17(f17(x2612,x2613),x2611),f17(f17(a21,a22),a24))+E(f16(x2611,f14(x2612,x2613,x2611)),x2612) % 59.97/60.03 [271]~P1(x2714)+~P1(x2711)+~P1(x2713)+~P1(x2712)+E(x2711,a20)+E(x2711,a1)+~E(f16(x2712,x2713),f16(x2711,x2714))+P1(f14(x2712,x2713,x2711))+P1(f13(x2712,x2713,x2711))+~P4(f17(f17(x2712,x2713),x2711),f17(f17(a21,a22),a24))+E(f16(f12(x2712,x2713,x2711),f15(x2712,x2713,x2711)),x2711) % 59.97/60.03 [272]~P1(x2724)+~P1(x2721)+~P1(x2723)+~P1(x2722)+E(x2721,a20)+E(x2721,a1)+~E(f16(x2722,x2723),f16(x2721,x2724))+E(f16(f12(x2722,x2723,x2721),f15(x2722,x2723,x2721)),x2721)+P1(f13(x2722,x2723,x2721))+~P4(f17(f17(x2722,x2723),x2721),f17(f17(a21,a22),a24))+E(f16(x2721,f14(x2722,x2723,x2721)),x2722) % 59.97/60.03 [273]~P1(x2734)+~P1(x2732)+~P1(x2731)+~P1(x2733)+E(x2731,a20)+E(x2731,a1)+~E(f16(x2731,x2734),f16(x2732,x2733))+E(f16(f12(x2732,x2733,x2731),f15(x2732,x2733,x2731)),x2731)+P1(f14(x2732,x2733,x2731))+~P4(f17(f17(x2732,x2733),x2731),f17(f17(a21,a22),a24))+E(f16(x2731,f13(x2732,x2733,x2731)),x2733) % 59.97/60.03 [275]~P1(x2754)+~P1(x2752)+~P1(x2751)+~P1(x2753)+E(x2751,a20)+E(x2751,a1)+~E(f16(x2751,x2754),f16(x2752,x2753))+E(f16(x2751,f13(x2752,x2753,x2751)),x2753)+E(f16(f12(x2752,x2753,x2751),f15(x2752,x2753,x2751)),x2751)+~P4(f17(f17(x2752,x2753),x2751),f17(f17(a21,a22),a24))+E(f16(x2751,f14(x2752,x2753,x2751)),x2752) % 59.97/60.03 %EqnAxiom % 59.97/60.03 [1]E(x11,x11) % 59.97/60.03 [2]E(x22,x21)+~E(x21,x22) % 59.97/60.03 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 59.97/60.03 [4]~E(x41,x42)+E(f16(x41,x43),f16(x42,x43)) % 59.97/60.03 [5]~E(x51,x52)+E(f16(x53,x51),f16(x53,x52)) % 59.97/60.03 [6]~E(x61,x62)+E(f17(x61,x63),f17(x62,x63)) % 59.97/60.03 [7]~E(x71,x72)+E(f17(x73,x71),f17(x73,x72)) % 59.97/60.03 [8]~E(x81,x82)+E(f14(x81,x83,x84),f14(x82,x83,x84)) % 59.97/60.03 [9]~E(x91,x92)+E(f14(x93,x91,x94),f14(x93,x92,x94)) % 59.97/60.03 [10]~E(x101,x102)+E(f14(x103,x104,x101),f14(x103,x104,x102)) % 59.97/60.03 [11]~E(x111,x112)+E(f15(x111,x113,x114),f15(x112,x113,x114)) % 59.97/60.03 [12]~E(x121,x122)+E(f15(x123,x121,x124),f15(x123,x122,x124)) % 59.97/60.03 [13]~E(x131,x132)+E(f15(x133,x134,x131),f15(x133,x134,x132)) % 59.97/60.03 [14]~E(x141,x142)+E(f13(x141,x143,x144),f13(x142,x143,x144)) % 59.97/60.03 [15]~E(x151,x152)+E(f13(x153,x151,x154),f13(x153,x152,x154)) % 59.97/60.03 [16]~E(x161,x162)+E(f13(x163,x164,x161),f13(x163,x164,x162)) % 59.97/60.03 [17]~E(x171,x172)+E(f12(x171,x173,x174),f12(x172,x173,x174)) % 59.97/60.03 [18]~E(x181,x182)+E(f12(x183,x181,x184),f12(x183,x182,x184)) % 59.97/60.03 [19]~E(x191,x192)+E(f12(x193,x194,x191),f12(x193,x194,x192)) % 59.97/60.03 [20]~E(x201,x202)+E(f19(x201,x203),f19(x202,x203)) % 59.97/60.03 [21]~E(x211,x212)+E(f19(x213,x211),f19(x213,x212)) % 59.97/60.03 [22]~E(x221,x222)+E(f8(x221),f8(x222)) % 59.97/60.03 [23]~E(x231,x232)+E(f9(x231),f9(x232)) % 59.97/60.03 [24]~E(x241,x242)+E(f18(x241,x243),f18(x242,x243)) % 59.97/60.03 [25]~E(x251,x252)+E(f18(x253,x251),f18(x253,x252)) % 59.97/60.03 [26]~E(x261,x262)+E(f10(x261,x263),f10(x262,x263)) % 59.97/60.03 [27]~E(x271,x272)+E(f10(x273,x271),f10(x273,x272)) % 59.97/60.03 [28]~E(x281,x282)+E(f11(x281,x283),f11(x282,x283)) % 59.97/60.03 [29]~E(x291,x292)+E(f11(x293,x291),f11(x293,x292)) % 59.97/60.03 [30]~P1(x301)+P1(x302)+~E(x301,x302) % 59.97/60.03 [31]P4(x312,x313)+~E(x311,x312)+~P4(x311,x313) % 59.97/60.03 [32]P4(x323,x322)+~E(x321,x322)+~P4(x323,x321) % 59.97/60.03 [33]P3(x332,x333)+~E(x331,x332)+~P3(x331,x333) % 59.97/60.03 [34]P3(x343,x342)+~E(x341,x342)+~P3(x343,x341) % 59.97/60.03 [35]~P2(x351)+P2(x352)+~E(x351,x352) % 59.97/60.03 [36]P5(x362,x363)+~E(x361,x362)+~P5(x361,x363) % 59.97/60.03 [37]P5(x373,x372)+~E(x371,x372)+~P5(x373,x371) % 59.97/60.03 % 59.97/60.03 %------------------------------------------- % 59.97/60.03 cnf(279,plain, % 59.97/60.03 (~P2(a1)+~P1(a1)), % 59.97/60.03 inference(equality_inference,[],[80])). % 59.97/60.03 cnf(280,plain, % 59.97/60.03 (~P2(a20)+~P1(a20)), % 59.97/60.03 inference(equality_inference,[],[81])). % 59.97/60.03 cnf(282,plain, % 59.97/60.03 (P3(x2821,f16(x2821,x2822))+~P1(x2821)+~P1(f16(x2821,x2822))+~P1(x2822)), % 59.97/60.03 inference(equality_inference,[],[119])). % 59.97/60.03 cnf(283,plain, % 59.97/60.03 (P5(x2831,f17(x2831,x2832))+~P1(f17(x2831,x2832))+~P1(x2831)+~P1(x2832)), % 59.97/60.03 inference(equality_inference,[],[120])). % 59.97/60.03 cnf(284,plain, % 59.97/60.03 (~P5(x2841,x2842)+~P1(x2841)+~P1(x2842)+P1(f18(x2842,x2841))), % 59.97/60.03 inference(equality_inference,[],[122])). % 59.97/60.03 cnf(290,plain, % 59.97/60.03 (~P5(x2901,x2902)+~P1(x2902)+~P1(x2901)+E(f17(x2901,f18(x2902,x2901)),x2902)), % 59.97/60.03 inference(equality_inference,[],[130])). % 59.97/60.03 cnf(339,plain, % 59.97/60.03 (~P2(a1)), % 59.97/60.03 inference(scs_inference,[],[38,279])). % 59.97/60.03 cnf(340,plain, % 59.97/60.03 (~P2(a20)), % 59.97/60.03 inference(scs_inference,[],[39,280])). % 59.97/60.03 cnf(341,plain, % 59.97/60.03 (E(f16(a21,a22),f16(a25,a7))), % 59.97/60.03 inference(scs_inference,[],[62,2])). % 59.97/60.03 cnf(342,plain, % 59.97/60.03 (~E(a1,f16(a25,a5))), % 59.97/60.03 inference(scs_inference,[],[62,72,53,2,3])). % 59.97/60.03 cnf(343,plain, % 59.97/60.03 (P3(a25,f16(a25,a7))), % 59.97/60.03 inference(scs_inference,[],[62,72,65,53,2,3,34])). % 59.97/60.03 cnf(344,plain, % 59.97/60.03 (P5(a1,a1)), % 59.97/60.03 inference(scs_inference,[],[62,38,72,65,53,2,3,34,112])). % 59.97/60.03 cnf(346,plain, % 59.97/60.03 (P1(f18(a1,a1))), % 59.97/60.03 inference(scs_inference,[],[62,38,72,65,53,2,3,34,112,284])). % 59.97/60.03 cnf(348,plain, % 59.97/60.03 (E(f17(a1,f18(a1,a1)),a1)), % 59.97/60.03 inference(scs_inference,[],[62,38,72,65,53,2,3,34,112,284,290])). % 59.97/60.03 cnf(350,plain, % 59.97/60.03 (~P3(a1,a24)), % 59.97/60.03 inference(scs_inference,[],[62,38,66,67,72,65,53,2,3,34,112,284,290,100])). % 59.97/60.03 cnf(354,plain, % 59.97/60.03 (E(f18(a1,a1),a1)), % 59.97/60.03 inference(scs_inference,[],[62,38,66,67,72,75,65,53,2,3,34,112,284,290,100,101,105])). % 59.97/60.03 cnf(356,plain, % 59.97/60.03 (P5(a25,a23)), % 59.97/60.03 inference(scs_inference,[],[62,38,43,44,49,66,67,72,75,65,53,56,2,3,34,112,284,290,100,101,105,120])). % 59.97/60.03 cnf(358,plain, % 59.97/60.03 (E(a3,f18(a24,a21))), % 59.97/60.03 inference(scs_inference,[],[62,38,40,42,43,44,46,49,57,66,67,72,75,65,53,54,56,2,3,34,112,284,290,100,101,105,120,136])). % 59.97/60.03 cnf(361,plain, % 59.97/60.03 (~E(a25,a24)), % 59.97/60.03 inference(scs_inference,[],[79,62,38,40,42,43,44,46,49,57,66,67,72,75,65,53,54,56,2,3,34,112,284,290,100,101,105,120,136,30,36])). % 59.97/60.03 cnf(362,plain, % 59.97/60.03 (~P2(f18(a1,a1))), % 59.97/60.03 inference(scs_inference,[],[79,62,38,40,42,43,44,46,49,57,66,67,72,75,65,53,54,56,2,3,34,112,284,290,100,101,105,120,136,30,36,80])). % 59.97/60.03 cnf(369,plain, % 59.97/60.04 (E(a1,f17(a1,f18(a1,a1)))), % 59.97/60.04 inference(scs_inference,[],[348,2])). % 59.97/60.04 cnf(370,plain, % 59.97/60.04 (P3(a24,f16(a25,a7))), % 59.97/60.04 inference(scs_inference,[],[341,348,64,2,34])). % 59.97/60.04 cnf(372,plain, % 59.97/60.04 (E(f16(a24,a2),f16(a25,a7))), % 59.97/60.04 inference(scs_inference,[],[344,341,348,61,64,2,34,37,3])). % 59.97/60.04 cnf(373,plain, % 59.97/60.04 (P5(f17(a1,f18(a1,a1)),a1)), % 59.97/60.04 inference(scs_inference,[],[344,341,348,61,64,2,34,37,3,36])). % 59.97/60.04 cnf(375,plain, % 59.97/60.04 (P1(f18(a24,a21))), % 59.97/60.04 inference(scs_inference,[],[344,341,348,358,61,339,64,46,2,34,37,3,36,35,30])). % 59.97/60.04 cnf(376,plain, % 59.97/60.04 (~P3(a25,a24)), % 59.97/60.04 inference(scs_inference,[],[344,341,348,361,358,61,339,64,46,76,44,2,34,37,3,36,35,30,100])). % 59.97/60.04 cnf(378,plain, % 59.97/60.04 (P5(f18(a1,a1),f18(a1,a1))), % 59.97/60.04 inference(scs_inference,[],[344,341,346,348,361,358,61,339,64,46,76,44,2,34,37,3,36,35,30,100,112])). % 59.97/60.04 cnf(380,plain, % 59.97/60.04 (P1(f18(f18(a1,a1),f18(a1,a1)))), % 59.97/60.04 inference(scs_inference,[],[344,341,346,348,361,358,61,339,64,46,76,44,2,34,37,3,36,35,30,100,112,284])). % 59.97/60.04 cnf(382,plain, % 59.97/60.04 (E(f17(f18(a1,a1),f18(f18(a1,a1),f18(a1,a1))),f18(a1,a1))), % 59.97/60.04 inference(scs_inference,[],[344,341,346,348,361,358,61,339,64,46,76,44,2,34,37,3,36,35,30,100,112,284,290])). % 59.97/60.04 cnf(384,plain, % 59.97/60.04 (P1(f17(f18(a1,a1),f18(f18(a1,a1),f18(a1,a1))))), % 59.97/60.04 inference(scs_inference,[],[344,341,346,348,361,358,61,339,64,46,76,44,38,2,34,37,3,36,35,30,100,112,284,290,122])). % 59.97/60.04 cnf(386,plain, % 59.97/60.04 (~P3(a23,a24)), % 59.97/60.04 inference(scs_inference,[],[344,341,346,348,361,358,61,339,64,46,76,43,59,42,44,38,2,34,37,3,36,35,30,100,112,284,290,122,135])). % 59.97/60.04 cnf(388,plain, % 59.97/60.04 (E(a4,f18(a24,a22))), % 59.97/60.04 inference(scs_inference,[],[344,341,346,348,361,58,358,61,41,47,339,64,55,46,76,43,59,42,44,38,2,34,37,3,36,35,30,100,112,284,290,122,135,136])). % 59.97/60.04 cnf(391,plain, % 59.97/60.04 (P5(a20,a24)+E(a24,a1)), % 59.97/60.04 inference(scs_inference,[],[344,341,346,348,343,361,58,358,61,41,47,68,339,64,55,46,76,43,59,42,44,38,2,34,37,3,36,35,30,100,112,284,290,122,135,136,33,93])). % 59.97/60.04 cnf(399,plain, % 59.97/60.04 (P5(a20,a20)), % 59.97/60.04 inference(scs_inference,[],[344,341,346,348,343,361,58,358,61,39,41,47,68,339,64,55,46,76,43,59,42,44,38,2,34,37,3,36,35,30,100,112,284,290,122,135,136,33,93,102,282,283,103])). % 59.97/60.04 cnf(402,plain, % 59.97/60.04 (E(f18(a1,a1),f17(f18(a1,a1),f18(f18(a1,a1),f18(a1,a1))))), % 59.97/60.04 inference(scs_inference,[],[382,2])). % 59.97/60.04 cnf(403,plain, % 59.97/60.04 (P5(f18(a1,a1),a1)), % 59.97/60.04 inference(scs_inference,[],[378,382,354,2,37])). % 59.97/60.04 cnf(404,plain, % 59.97/60.04 (E(f16(a24,a23),f16(a25,a7))), % 59.97/60.04 inference(scs_inference,[],[378,382,341,354,60,2,37,3])). % 59.97/60.04 cnf(405,plain, % 59.97/60.04 (~E(f16(a25,a7),a24)), % 59.97/60.04 inference(scs_inference,[],[378,382,343,341,354,376,60,2,37,3,34])). % 59.97/60.04 cnf(406,plain, % 59.97/60.04 (P5(a1,f18(a1,a1))), % 59.97/60.04 inference(scs_inference,[],[378,382,343,341,354,376,60,2,37,3,34,36])). % 59.97/60.04 cnf(407,plain, % 59.97/60.04 (P1(f17(a1,f18(a1,a1)))), % 59.97/60.04 inference(scs_inference,[],[378,382,369,343,341,354,376,60,38,2,37,3,34,36,30])). % 59.97/60.04 cnf(409,plain, % 59.97/60.04 (P5(f18(f18(a1,a1),f18(a1,a1)),f18(f18(a1,a1),f18(a1,a1)))), % 59.97/60.04 inference(scs_inference,[],[378,380,382,369,343,341,354,362,376,60,38,2,37,3,34,36,30,35,112])). % 59.97/60.04 cnf(411,plain, % 59.97/60.04 (P1(f18(a20,a20))), % 59.97/60.04 inference(scs_inference,[],[378,380,382,399,369,343,341,354,362,376,60,39,38,2,37,3,34,36,30,35,112,284])). % 59.97/60.04 cnf(413,plain, % 59.97/60.04 (E(f17(a20,f18(a20,a20)),a20)), % 59.97/60.04 inference(scs_inference,[],[378,380,382,399,369,343,341,354,362,376,60,39,38,2,37,3,34,36,30,35,112,284,290])). % 59.97/60.04 cnf(415,plain, % 59.97/60.04 (E(a1,f18(a1,a1))), % 59.97/60.04 inference(scs_inference,[],[346,378,380,382,399,369,343,341,354,362,376,60,39,38,2,37,3,34,36,30,35,112,284,290,121])). % 59.97/60.04 cnf(417,plain, % 59.97/60.04 (P5(f17(a1,f18(a1,a1)),f18(a1,a1))), % 59.97/60.04 inference(scs_inference,[],[346,378,380,382,399,369,373,343,341,354,362,376,60,39,38,2,37,3,34,36,30,35,112,284,290,121,134])). % 59.97/60.04 cnf(419,plain, % 59.97/60.04 (E(a6,f18(a23,a25))), % 59.97/60.04 inference(scs_inference,[],[346,378,380,382,356,399,369,373,343,341,354,56,362,376,60,39,49,43,44,38,2,37,3,34,36,30,35,112,284,290,121,134,136])). % 59.97/60.04 cnf(423,plain, % 59.97/60.04 (P3(x4231,f16(a25,a7))+~E(a24,x4231)), % 59.97/60.04 inference(scs_inference,[],[346,378,380,382,356,399,369,373,370,343,341,354,56,362,376,60,39,49,43,44,38,2,37,3,34,36,30,35,112,284,290,121,134,136,81,33])). % 59.97/60.04 cnf(425,plain, % 59.97/60.04 (P5(a20,a23)+E(a23,a1)), % 59.97/60.04 inference(scs_inference,[],[346,378,380,382,356,399,369,373,370,343,341,354,56,362,376,74,60,39,49,43,44,38,2,37,3,34,36,30,35,112,284,290,121,134,136,81,33,100,93])). % 59.97/60.04 cnf(430,plain, % 59.97/60.04 (E(f16(a25,a7),f16(a24,a2))), % 59.97/60.04 inference(scs_inference,[],[372,2])). % 59.97/60.04 cnf(431,plain, % 59.97/60.04 (~E(a1,f17(a20,f18(a20,a20)))), % 59.97/60.04 inference(scs_inference,[],[372,413,66,2,3])). % 59.97/60.04 cnf(432,plain, % 59.97/60.04 (~E(a23,a24)), % 59.97/60.04 inference(scs_inference,[],[372,413,66,59,376,2,3,34])). % 59.97/60.04 cnf(433,plain, % 59.97/60.04 (P5(f17(f18(a1,a1),f18(f18(a1,a1),f18(a1,a1))),a1)), % 59.97/60.04 inference(scs_inference,[],[402,372,403,413,66,59,376,2,3,34,36])). % 59.97/60.04 cnf(434,plain, % 59.97/60.04 (P5(f18(a1,a1),f17(a1,f18(a1,a1)))), % 59.97/60.04 inference(scs_inference,[],[402,372,403,413,369,66,59,376,2,3,34,36,37])). % 59.97/60.04 cnf(436,plain, % 59.97/60.04 (P1(f18(a24,a22))), % 59.97/60.04 inference(scs_inference,[],[402,372,403,413,369,66,388,59,340,376,47,2,3,34,36,37,35,30])). % 59.97/60.04 cnf(439,plain, % 59.97/60.04 (E(f18(a1,a1),f17(a1,f18(a1,a1)))), % 59.97/60.04 inference(scs_inference,[],[346,402,417,407,372,403,413,369,66,388,59,340,376,47,2,3,34,36,37,35,30,112,121])). % 59.97/60.04 cnf(443,plain, % 59.97/60.04 (P3(x4431,a23)+~E(a25,x4431)), % 59.97/60.04 inference(scs_inference,[],[346,384,402,417,407,372,403,406,413,369,66,388,59,340,376,47,38,2,3,34,36,37,35,30,112,121,134,33])). % 59.97/60.04 cnf(448,plain, % 59.97/60.04 (~P5(a23,a24)), % 59.97/60.04 inference(scs_inference,[],[432,82])). % 59.97/60.04 cnf(449,plain, % 59.97/60.04 (~P1(x4491)+~E(f17(a23,x4491),a24)), % 59.97/60.04 inference(scs_inference,[],[432,99])). % 59.97/60.04 cnf(450,plain, % 59.97/60.04 (E(a20,f17(a20,f18(a20,a20)))), % 59.97/60.04 inference(scs_inference,[],[413,2])). % 59.97/60.04 cnf(451,plain, % 59.97/60.04 (P3(a24,f16(a24,a2))), % 59.97/60.04 inference(scs_inference,[],[413,370,430,2,34])). % 59.97/60.04 cnf(452,plain, % 59.97/60.04 (P5(f17(a20,f18(a20,a20)),a20)), % 59.97/60.04 inference(scs_inference,[],[413,370,430,399,2,34,36])). % 59.97/60.04 cnf(453,plain, % 59.97/60.04 (P5(a1,f17(f18(a1,a1),f18(f18(a1,a1),f18(a1,a1))))), % 59.97/60.04 inference(scs_inference,[],[413,370,430,402,406,399,2,34,36,37])). % 59.97/60.04 cnf(454,plain, % 59.97/60.04 (E(f16(a24,a23),f16(a24,a2))), % 59.97/60.04 inference(scs_inference,[],[413,370,404,430,402,406,399,2,34,36,37,3])). % 59.97/60.04 cnf(455,plain, % 59.97/60.04 (P1(f18(a23,a25))), % 59.97/60.04 inference(scs_inference,[],[413,370,404,430,402,406,399,419,49,2,34,36,37,3,30])). % 59.97/60.04 cnf(456,plain, % 59.97/60.04 (P5(f18(a24,a22),f18(a24,a22))), % 59.97/60.04 inference(scs_inference,[],[413,370,436,404,430,402,406,399,419,49,2,34,36,37,3,30,112])). % 59.97/60.04 cnf(458,plain, % 59.97/60.04 (P1(f18(f18(a24,a22),f18(a24,a22)))), % 59.97/60.04 inference(scs_inference,[],[413,370,436,404,430,402,406,399,419,49,2,34,36,37,3,30,112,284])). % 59.97/60.04 cnf(460,plain, % 59.97/60.04 (E(f17(f18(a24,a22),f18(f18(a24,a22),f18(a24,a22))),f18(a24,a22))), % 59.97/60.04 inference(scs_inference,[],[413,370,436,404,430,402,406,399,419,49,2,34,36,37,3,30,112,284,290])). % 59.97/60.04 cnf(462,plain, % 59.97/60.04 (P1(f17(f18(a24,a22),f18(f18(a24,a22),f18(a24,a22))))), % 59.97/60.04 inference(scs_inference,[],[413,370,436,404,430,402,406,399,58,419,41,49,42,2,34,36,37,3,30,112,284,290,122])). % 59.97/60.04 cnf(466,plain, % 59.97/60.04 (E(f18(a1,a1),f18(f18(a1,a1),a1))), % 59.97/60.04 inference(scs_inference,[],[346,413,370,434,436,404,430,402,406,417,399,407,58,38,419,41,49,42,2,34,36,37,3,30,112,284,290,122,121,136])). % 59.97/60.04 cnf(469,plain, % 59.97/60.04 (P3(x4691,f16(a21,a22))+~E(a24,x4691)), % 59.97/60.04 inference(scs_inference,[],[346,413,370,434,436,404,430,402,406,417,399,407,58,38,419,64,41,49,42,2,34,36,37,3,30,112,284,290,122,121,136,35,33])). % 59.97/60.04 cnf(472,plain, % 59.97/60.04 (P5(a20,a25)+E(a25,a1)), % 59.97/60.04 inference(scs_inference,[],[346,413,370,434,436,404,430,402,406,417,399,407,58,38,419,64,41,49,76,42,44,2,34,36,37,3,30,112,284,290,122,121,136,35,33,283,93])). % 59.97/60.04 cnf(476,plain, % 59.97/60.04 (E(f18(a24,a22),f17(f18(a24,a22),f18(f18(a24,a22),f18(a24,a22))))), % 59.97/60.04 inference(scs_inference,[],[460,2])). % 59.97/60.04 cnf(479,plain, % 59.97/60.04 (~E(f16(a21,a22),a24)), % 59.97/60.04 inference(scs_inference,[],[378,456,460,402,65,376,2,36,37,34])). % 59.97/60.04 cnf(480,plain, % 59.97/60.04 (~E(a25,f17(a21,a3))), % 59.97/60.04 inference(scs_inference,[],[361,378,456,460,402,54,65,376,2,36,37,34,3])). % 59.97/60.04 cnf(482,plain, % 59.97/60.04 (P5(f18(f18(a24,a22),f18(a24,a22)),f18(f18(a24,a22),f18(a24,a22)))), % 59.97/60.04 inference(scs_inference,[],[361,378,456,458,460,450,402,54,39,65,376,2,36,37,34,3,30,112])). % 59.97/60.04 cnf(487,plain, % 59.97/60.04 (P3(x4871,f16(a24,a2))+~E(a24,x4871)), % 59.97/60.04 inference(scs_inference,[],[361,433,378,456,458,460,453,450,451,384,402,54,39,38,65,376,2,36,37,34,3,30,112,121,35,33])). % 59.97/60.04 cnf(490,plain, % 59.97/60.04 (P5(f18(a23,a25),f18(a23,a25))), % 59.97/60.04 inference(scs_inference,[],[361,433,378,456,458,460,455,453,450,451,384,402,54,39,38,65,376,76,44,2,36,37,34,3,30,112,121,35,33,102,103])). % 59.97/60.04 cnf(497,plain, % 59.97/60.04 (E(f16(a24,a2),f16(a24,a23))), % 59.97/60.04 inference(scs_inference,[],[454,2])). % 59.97/60.04 cnf(498,plain, % 59.97/60.04 (P5(f17(a20,f18(a20,a20)),f17(a20,f18(a20,a20)))), % 59.97/60.04 inference(scs_inference,[],[454,452,450,2,37])). % 59.97/60.04 cnf(499,plain, % 59.97/60.04 (~E(a25,f17(a22,a4))), % 59.97/60.04 inference(scs_inference,[],[361,454,452,450,55,2,37,3])). % 59.97/60.04 cnf(500,plain, % 59.97/60.04 (~E(a21,a23)), % 59.97/60.04 inference(scs_inference,[],[448,361,454,452,450,55,57,2,37,3,36])). % 59.97/60.04 cnf(501,plain, % 59.97/60.04 (P1(f18(f18(a1,a1),a1))), % 59.97/60.04 inference(scs_inference,[],[448,346,361,454,452,450,55,57,466,2,37,3,36,30])). % 59.97/60.04 cnf(502,plain, % 59.97/60.04 (P5(f18(a24,a21),f18(a24,a21))), % 59.97/60.04 inference(scs_inference,[],[448,346,361,375,454,452,450,55,57,466,2,37,3,36,30,112])). % 59.97/60.04 cnf(504,plain, % 59.97/60.04 (P1(f18(f18(a24,a21),f18(a24,a21)))), % 59.97/60.04 inference(scs_inference,[],[448,346,361,375,454,452,450,55,57,466,2,37,3,36,30,112,284])). % 59.97/60.04 cnf(506,plain, % 59.97/60.04 (E(f17(f18(a24,a21),f18(f18(a24,a21),f18(a24,a21))),f18(a24,a21))), % 59.97/60.04 inference(scs_inference,[],[448,346,361,375,454,452,450,55,57,466,2,37,3,36,30,112,284,290])). % 59.97/60.04 cnf(508,plain, % 59.97/60.04 (P1(f17(f18(a24,a21),f18(f18(a24,a21),f18(a24,a21))))), % 59.97/60.04 inference(scs_inference,[],[448,346,361,375,454,452,450,55,57,466,40,42,2,37,3,36,30,112,284,290,122])). % 59.97/60.04 cnf(512,plain, % 59.97/60.04 (E(f18(f18(a1,a1),f18(a1,a1)),f18(a1,f18(a1,a1)))), % 59.97/60.04 inference(scs_inference,[],[448,346,361,433,403,453,375,454,452,380,450,384,55,38,57,466,40,42,2,37,3,36,30,112,284,290,122,121,136])). % 59.97/60.04 cnf(515,plain, % 59.97/60.04 (E(f18(f18(a1,a1),f18(a1,a1)),a1)), % 59.97/60.04 inference(scs_inference,[],[448,346,361,433,403,453,476,375,454,452,380,450,384,55,38,57,466,40,42,2,37,3,36,30,112,284,290,122,121,136,35,105])). % 59.97/60.04 cnf(521,plain, % 59.97/60.04 (E(f18(a24,a21),f17(f18(a24,a21),f18(f18(a24,a21),f18(a24,a21))))), % 59.97/60.04 inference(scs_inference,[],[506,2])). % 59.97/60.04 cnf(525,plain, % 59.97/60.04 (~E(a21,f17(a25,a6))), % 59.97/60.04 inference(scs_inference,[],[451,506,497,500,380,56,515,2,80,34,3])). % 59.97/60.04 cnf(527,plain, % 59.97/60.04 (P5(f18(a24,a21),f17(f18(a24,a21),f18(f18(a24,a21),f18(a24,a21))))), % 59.97/60.04 inference(scs_inference,[],[451,502,506,497,500,380,56,515,2,80,34,3,36,37])). % 59.97/60.04 cnf(528,plain, % 59.97/60.04 (P1(f18(a1,f18(a1,a1)))), % 59.97/60.04 inference(scs_inference,[],[451,502,506,497,500,380,56,512,515,2,80,34,3,36,37,30])). % 59.97/60.04 cnf(529,plain, % 59.97/60.04 (P1(f18(f18(a23,a25),f18(a23,a25)))), % 59.97/60.04 inference(scs_inference,[],[451,502,506,490,497,500,455,380,56,512,515,2,80,34,3,36,37,30,284])). % 59.97/60.04 cnf(531,plain, % 59.97/60.04 (P5(f18(f18(a24,a21),f18(a24,a21)),f18(f18(a24,a21),f18(a24,a21)))), % 59.97/60.04 inference(scs_inference,[],[451,502,504,506,490,497,500,455,380,56,512,515,2,80,34,3,36,37,30,284,112])). % 59.97/60.04 cnf(533,plain, % 59.97/60.04 (E(f17(f18(a23,a25),f18(f18(a23,a25),f18(a23,a25))),f18(a23,a25))), % 59.97/60.04 inference(scs_inference,[],[451,502,504,506,490,497,500,455,380,56,512,515,2,80,34,3,36,37,30,284,112,290])). % 59.97/60.04 cnf(537,plain, % 59.97/60.04 (P3(x5371,f16(a21,a22))+~E(a25,x5371)), % 59.97/60.04 inference(scs_inference,[],[451,502,504,506,490,497,500,356,455,380,56,65,512,515,43,44,2,80,34,3,36,37,30,284,112,290,122,33])). % 59.97/60.04 cnf(539,plain, % 59.97/60.04 (P5(f18(f18(a1,a1),a1),f18(f18(a1,a1),a1))), % 59.97/60.04 inference(scs_inference,[],[451,502,504,506,490,501,497,500,356,455,380,56,65,512,515,43,44,2,80,34,3,36,37,30,284,112,290,122,33,35,103])). % 59.97/60.04 cnf(545,plain, % 59.97/60.04 (E(f18(a23,a25),f17(f18(a23,a25),f18(f18(a23,a25),f18(a23,a25))))), % 59.97/60.04 inference(scs_inference,[],[533,2])). % 59.97/60.04 cnf(548,plain, % 59.97/60.04 (P5(f18(f18(a1,a1),f18(a1,a1)),a1)), % 59.97/60.04 inference(scs_inference,[],[413,498,533,409,500,515,63,2,3,36,37])). % 59.97/60.04 cnf(549,plain, % 59.97/60.04 (P5(f18(f18(a23,a25),f18(a23,a25)),f18(f18(a23,a25),f18(a23,a25)))), % 59.97/60.04 inference(scs_inference,[],[413,498,529,533,409,500,515,63,2,3,36,37,112])). % 59.97/60.04 cnf(556,plain, % 59.97/60.04 (E(f16(a25,a7),f16(a24,a23))), % 59.97/60.04 inference(scs_inference,[],[404,2])). % 59.97/60.04 cnf(557,plain, % 59.97/60.04 (P5(a1,f18(f18(a1,a1),f18(a1,a1)))), % 59.97/60.04 inference(scs_inference,[],[409,404,515,2,36])). % 59.97/60.04 cnf(558,plain, % 59.97/60.04 (~E(a21,f16(a25,a5))), % 59.97/60.04 inference(scs_inference,[],[409,404,500,515,53,2,36,3])). % 59.97/60.04 cnf(559,plain, % 59.97/60.04 (P5(f18(f18(a1,a1),f18(a1,a1)),f17(a1,f18(a1,a1)))), % 59.97/60.04 inference(scs_inference,[],[369,548,409,404,500,515,53,2,36,3,37])). % 59.97/60.04 cnf(560,plain, % 59.97/60.04 (P5(f18(a1,f18(a1,a1)),f18(a1,f18(a1,a1)))), % 59.97/60.04 inference(scs_inference,[],[369,528,548,409,404,500,515,53,2,36,3,37,112])). % 59.97/60.04 cnf(562,plain, % 59.97/60.04 (E(a1,f18(f18(a1,a1),f18(a1,a1)))), % 59.97/60.04 inference(scs_inference,[],[369,528,548,409,404,500,380,38,515,53,2,36,3,37,112,121])). % 59.97/60.04 cnf(567,plain, % 59.97/60.04 (E(a24,f17(a21,a3))), % 59.97/60.04 inference(scs_inference,[],[54,2])). % 59.97/60.04 cnf(568,plain, % 59.97/60.04 (E(a1,f18(a1,f18(a1,a1)))), % 59.97/60.04 inference(scs_inference,[],[54,512,562,2,3])). % 59.97/60.04 cnf(569,plain, % 59.97/60.04 (P5(f17(a1,f18(a1,a1)),f18(f18(a1,a1),f18(a1,a1)))), % 59.97/60.04 inference(scs_inference,[],[369,557,54,512,562,2,3,36])). % 59.97/60.04 cnf(570,plain, % 59.97/60.04 (P1(f17(a21,a3))), % 59.97/60.04 inference(scs_inference,[],[369,557,54,512,562,42,2,3,36,30])). % 59.97/60.04 cnf(572,plain, % 59.97/60.04 (P2(f17(a21,a3))), % 59.97/60.04 inference(scs_inference,[],[369,557,456,476,54,512,562,51,42,2,3,36,30,37,35])). % 59.97/60.04 cnf(573,plain, % 59.97/60.04 (P3(f17(a21,a3),f16(a25,a7))), % 59.97/60.04 inference(scs_inference,[],[370,369,557,456,476,54,512,562,51,42,2,3,36,30,37,35,33])). % 59.97/60.04 cnf(574,plain, % 59.97/60.04 (P5(f18(a20,a20),f18(a20,a20))), % 59.97/60.04 inference(scs_inference,[],[370,369,557,456,476,411,54,512,562,51,42,2,3,36,30,37,35,33,112])). % 59.97/60.04 cnf(576,plain, % 59.97/60.04 (E(f17(f18(a20,a20),f18(f18(a20,a20),f18(a20,a20))),f18(a20,a20))), % 59.97/60.04 inference(scs_inference,[],[370,369,557,456,476,411,54,512,562,51,42,2,3,36,30,37,35,33,112,290])). % 59.97/60.04 cnf(582,plain, % 59.97/60.04 (E(f18(a1,a1),f18(f18(f18(a1,a1),f18(a1,a1)),a1))), % 59.97/60.04 inference(scs_inference,[],[346,370,369,559,557,456,476,411,399,407,380,54,39,38,512,562,51,42,2,3,36,30,37,35,33,112,290,122,121,136])). % 59.97/60.04 cnf(584,plain, % 59.97/60.04 (P3(f17(a21,a3),f16(a21,a22))), % 59.97/60.04 inference(scs_inference,[],[346,370,369,559,557,456,476,411,399,407,380,54,39,38,512,562,51,42,2,3,36,30,37,35,33,112,290,122,121,136,469])). % 59.97/60.04 cnf(587,plain, % 59.97/60.04 (P1(f18(f18(a20,a20),f18(a20,a20)))), % 59.97/60.04 inference(scs_inference,[],[346,370,369,559,556,557,456,476,411,399,407,380,54,39,38,512,562,51,42,2,3,36,30,37,35,33,112,290,122,121,136,469,487,34,284])). % 59.97/60.04 cnf(589,plain, % 59.97/60.04 (P5(a5,a5)), % 59.97/60.04 inference(scs_inference,[],[346,370,369,559,556,557,456,476,411,399,407,380,54,39,38,512,562,48,51,42,2,3,36,30,37,35,33,112,290,122,121,136,469,487,34,284,103])). % 59.97/60.04 cnf(601,plain, % 59.97/60.04 (E(f17(a1,f18(a1,a1)),f18(a1,f18(a1,a1)))), % 59.97/60.04 inference(scs_inference,[],[348,346,574,576,568,582,2,36,30,37,3])). % 59.97/60.04 cnf(602,plain, % 59.97/60.04 (P1(f18(a5,a5))), % 59.97/60.04 inference(scs_inference,[],[348,346,574,576,568,589,582,48,2,36,30,37,3,284])). % 59.97/60.04 cnf(606,plain, % 59.97/60.04 (E(f17(a5,f18(a5,a5)),a5)), % 59.97/60.04 inference(scs_inference,[],[348,346,587,574,576,568,589,582,48,2,36,30,37,3,284,112,290])). % 59.97/60.04 cnf(612,plain, % 59.97/60.04 (~P3(a25,f17(a21,a3))), % 59.97/60.04 inference(scs_inference,[],[348,346,559,528,407,380,587,574,576,569,480,570,572,568,589,38,76,582,48,44,2,36,30,37,3,284,112,290,120,121,115])). % 59.97/60.04 cnf(614,plain, % 59.97/60.04 (E(f18(a1,a1),f18(f18(a1,f18(a1,a1)),a1))), % 59.97/60.04 inference(scs_inference,[],[348,346,559,528,407,380,587,574,576,569,480,570,572,568,589,38,76,582,48,44,2,36,30,37,3,284,112,290,120,121,115,136])). % 59.97/60.04 cnf(617,plain, % 59.97/60.04 (P5(f17(a21,a3),f17(a21,a3))), % 59.97/60.04 inference(scs_inference,[],[348,346,533,559,528,407,380,587,574,576,569,480,570,572,568,589,38,76,582,48,44,2,36,30,37,3,284,112,290,120,121,115,136,35,103])). % 59.97/60.04 cnf(623,plain, % 59.97/60.04 (P1(f10(f18(a1,a1),f18(a1,a1)))), % 59.97/60.04 inference(scs_inference,[],[346,91,124])). % 59.97/60.04 cnf(624,plain, % 59.97/60.04 (E(f18(a1,f18(a1,a1)),a1)), % 59.97/60.04 inference(scs_inference,[],[568,2])). % 59.97/60.04 cnf(630,plain, % 59.97/60.04 (P5(a24,f17(a21,a3))), % 59.97/60.04 inference(scs_inference,[],[346,343,528,568,560,617,54,614,612,2,80,34,30,37,36])). % 59.97/60.04 cnf(635,plain, % 59.97/60.04 (E(f17(f17(a21,a3),f18(f17(a21,a3),f17(a21,a3))),f17(a21,a3))), % 59.97/60.04 inference(scs_inference,[],[346,343,528,568,623,560,617,570,54,614,612,2,80,34,30,37,36,284,112,290])). % 59.97/60.04 cnf(639,plain, % 59.97/60.04 (P5(f18(a1,f18(a1,a1)),f18(a1,a1))), % 59.97/60.04 inference(scs_inference,[],[346,343,406,528,568,623,560,617,570,59,54,38,614,612,43,44,2,80,34,30,37,36,284,112,290,135,134])). % 59.97/60.04 cnf(650,plain, % 59.97/60.04 (~E(a23,f17(a21,a3))), % 59.97/60.04 inference(scs_inference,[],[601,59,612,2,34])). % 59.97/60.04 cnf(662,plain, % 59.97/60.04 (P1(f17(a5,f18(a5,a5)))), % 59.97/60.04 inference(scs_inference,[],[606,48,2,30])). % 59.97/60.04 cnf(664,plain, % 59.97/60.04 (P5(f18(a1,f18(a1,a1)),f18(f18(a1,a1),f18(a1,a1)))), % 59.97/60.04 inference(scs_inference,[],[403,568,557,606,48,2,30,37,36])). % 59.97/60.04 cnf(665,plain, % 59.97/60.04 (~E(a23,f17(f17(a21,a3),f18(f17(a21,a3),f17(a21,a3))))), % 59.97/60.04 inference(scs_inference,[],[403,568,557,606,635,650,48,2,30,37,36,3])). % 59.97/60.04 cnf(666,plain, % 59.97/60.04 (P5(f18(a5,a5),f18(a5,a5))), % 59.97/60.04 inference(scs_inference,[],[403,568,557,606,635,602,650,48,2,30,37,36,3,112])). % 59.97/60.04 cnf(668,plain, % 59.97/60.04 (E(f17(f18(a5,a5),f18(f18(a5,a5),f18(a5,a5))),f18(a5,a5))), % 59.97/60.04 inference(scs_inference,[],[403,568,557,606,635,602,650,48,2,30,37,36,3,112,290])). % 59.97/60.04 cnf(675,plain, % 59.97/60.04 (P1(f18(f18(a5,a5),f18(a5,a5)))), % 59.97/60.04 inference(scs_inference,[],[346,403,576,568,557,606,528,635,639,602,650,589,48,2,30,37,36,3,112,290,122,121,35,284])). % 59.97/60.04 cnf(679,plain, % 59.97/60.04 (P5(a21,a21)), % 59.97/60.04 inference(scs_inference,[],[346,403,411,576,568,557,606,528,635,639,602,650,589,48,40,2,30,37,36,3,112,290,122,121,35,284,282,103])). % 59.97/60.04 cnf(684,plain, % 59.97/60.04 (E(f17(a21,a3),f17(f17(a21,a3),f18(f17(a21,a3),f17(a21,a3))))), % 59.97/60.04 inference(scs_inference,[],[635,2])). % 59.97/60.04 cnf(685,plain, % 59.97/60.04 (P5(f18(f18(a1,a1),f18(a1,a1)),f18(a1,f18(a1,a1)))), % 59.97/60.04 inference(scs_inference,[],[548,568,635,2,37])). % 59.97/60.04 cnf(686,plain, % 59.97/60.04 (P1(f17(f17(a21,a3),f18(f17(a21,a3),f17(a21,a3))))), % 59.97/60.04 inference(scs_inference,[],[548,568,570,635,2,37,30])). % 59.97/60.04 cnf(687,plain, % 59.97/60.04 (~E(a21,a24)), % 59.97/60.04 inference(scs_inference,[],[548,568,570,635,679,77,2,37,30,36])). % 59.97/60.04 cnf(689,plain, % 59.97/60.04 (P2(f17(f17(a21,a3),f18(f17(a21,a3),f17(a21,a3))))), % 59.97/60.04 inference(scs_inference,[],[413,548,568,570,635,679,572,74,77,2,37,30,36,3,35])). % 59.97/60.04 cnf(692,plain, % 59.97/60.04 (P1(f18(a21,a21))), % 59.97/60.04 inference(scs_inference,[],[413,548,568,570,635,675,679,572,74,77,40,2,37,30,36,3,35,112,284])). % 59.97/60.04 cnf(694,plain, % 59.97/60.04 (E(f17(a21,f18(a21,a21)),a21)), % 59.97/60.04 inference(scs_inference,[],[413,548,568,570,635,675,679,572,74,77,40,2,37,30,36,3,35,112,284,290])). % 59.97/60.04 cnf(696,plain, % 59.97/60.04 (P5(a21,f17(f17(a21,a3),f18(f17(a21,a3),f17(a21,a3))))), % 59.97/60.04 inference(scs_inference,[],[413,548,568,570,635,675,679,572,74,77,46,40,2,37,30,36,3,35,112,284,290,120])). % 59.97/60.04 cnf(703,plain, % 59.97/60.04 (E(f18(a5,a5),f17(f18(a5,a5),f18(f18(a5,a5),f18(a5,a5))))), % 59.97/60.04 inference(scs_inference,[],[668,2])). % 59.97/60.04 cnf(704,plain, % 59.97/60.04 (~E(f17(a21,a3),a23)), % 59.97/60.04 inference(scs_inference,[],[79,630,668,2,37])). % 59.97/60.04 cnf(705,plain, % 59.97/60.04 (~E(a25,f17(f17(a21,a3),f18(f17(a21,a3),f17(a21,a3))))), % 59.97/60.04 inference(scs_inference,[],[79,630,635,668,480,2,37,3])). % 59.97/60.04 cnf(708,plain, % 59.97/60.04 (P5(f17(a5,f18(a5,a5)),f17(a5,f18(a5,a5)))), % 59.97/60.04 inference(scs_inference,[],[79,573,630,617,635,668,662,684,480,2,37,3,36,33,112])). % 59.97/60.04 cnf(714,plain, % 59.97/60.04 (P3(f17(f17(a21,a3),f18(f17(a21,a3),f17(a21,a3))),f16(a24,a23))), % 59.97/60.04 inference(scs_inference,[],[79,573,528,380,630,617,635,664,668,556,685,686,689,662,684,665,480,74,43,2,37,3,36,33,112,121,115,34])). % 59.97/60.04 cnf(718,plain, % 59.97/60.04 (E(a21,f17(a21,f18(a21,a21)))), % 59.97/60.04 inference(scs_inference,[],[694,2])). % 59.97/60.04 cnf(721,plain, % 59.97/60.04 (P1(f17(a21,f18(a21,a21)))), % 59.97/60.04 inference(scs_inference,[],[694,666,703,714,454,40,2,34,37,30])). % 59.97/60.04 cnf(725,plain, % 59.97/60.04 (P5(f18(a21,a21),f18(a21,a21))), % 59.97/60.04 inference(scs_inference,[],[584,684,694,666,703,714,692,454,40,69,2,34,37,30,3,36,33,112])). % 59.97/60.04 cnf(727,plain, % 59.97/60.04 (~P3(a25,f17(f17(a21,a3),f18(f17(a21,a3),f17(a21,a3))))), % 59.97/60.04 inference(scs_inference,[],[584,684,694,666,703,714,692,705,686,689,454,76,40,69,44,2,34,37,30,3,36,33,112,115])). % 59.97/60.04 cnf(730,plain, % 59.97/60.04 (P1(f18(f18(a21,a21),f18(a21,a21)))), % 59.97/60.04 inference(scs_inference,[],[584,606,684,694,666,703,714,692,705,686,689,454,76,40,69,44,2,34,37,30,3,36,33,112,115,35,284])). % 59.97/60.04 cnf(732,plain, % 59.97/60.04 (E(f17(f18(a21,a21),f18(f18(a21,a21),f18(a21,a21))),f18(a21,a21))), % 59.97/60.04 inference(scs_inference,[],[584,606,684,694,666,703,714,692,705,686,689,454,76,40,69,44,2,34,37,30,3,36,33,112,115,35,284,290])). % 59.97/60.04 cnf(740,plain, % 59.97/60.04 (P5(a22,a22)), % 59.97/60.04 inference(scs_inference,[],[584,606,684,694,666,703,714,692,705,686,689,687,454,679,76,40,69,41,44,2,34,37,30,3,36,33,112,115,35,284,290,122,283,100,103])). % 59.97/60.04 cnf(747,plain, % 59.97/60.04 (~E(f16(a21,a22),f17(f17(a21,a3),f18(f17(a21,a3),f17(a21,a3))))), % 59.97/60.04 inference(scs_inference,[],[732,65,727,2,34])). % 59.97/60.04 cnf(749,plain, % 59.97/60.04 (~E(f17(a21,a3),f17(a25,a6))), % 59.97/60.04 inference(scs_inference,[],[725,732,704,56,65,727,2,34,37,3])). % 59.97/60.04 cnf(751,plain, % 59.97/60.04 (P1(f18(a22,a22))), % 59.97/60.04 inference(scs_inference,[],[725,732,740,704,56,65,727,41,2,34,37,3,36,284])). % 59.97/60.04 cnf(755,plain, % 59.97/60.04 (E(f17(a22,f18(a22,a22)),a22)), % 59.97/60.04 inference(scs_inference,[],[725,730,732,740,704,56,65,727,41,2,34,37,3,36,284,112,290])). % 59.97/60.04 cnf(760,plain, % 59.97/60.04 (E(a22,f17(a22,f18(a22,a22)))), % 59.97/60.04 inference(scs_inference,[],[755,2])). % 59.97/60.04 cnf(761,plain, % 59.97/60.04 (P5(a21,f17(a21,a3))), % 59.97/60.04 inference(scs_inference,[],[635,696,755,2,37])). % 59.97/60.04 cnf(762,plain, % 59.97/60.04 (P1(f17(a22,f18(a22,a22)))), % 59.97/60.04 inference(scs_inference,[],[635,696,755,41,2,37,30])). % 59.97/60.04 cnf(765,plain, % 59.97/60.04 (P5(f17(a21,f18(a21,a21)),f17(a21,f18(a21,a21)))), % 59.97/60.04 inference(scs_inference,[],[635,606,684,696,747,708,721,755,41,2,37,30,3,36,112])). % 59.97/60.04 cnf(771,plain, % 59.97/60.04 (P5(f18(a22,a22),f18(a22,a22))), % 59.97/60.04 inference(scs_inference,[],[668,635,606,684,696,747,708,721,751,755,405,41,2,37,30,3,36,112,35,100,283,103])). % 59.97/60.04 cnf(776,plain, % 59.97/60.04 (P5(f17(a21,f18(a21,a21)),a21)), % 59.97/60.04 inference(scs_inference,[],[694,765,55,2,37])). % 59.97/60.04 cnf(777,plain, % 59.97/60.04 (P1(f17(a22,a4))), % 59.97/60.04 inference(scs_inference,[],[694,765,55,42,2,37,30])). % 59.97/60.04 cnf(780,plain, % 59.97/60.04 (P2(f17(a22,a4))), % 59.97/60.04 inference(scs_inference,[],[694,755,765,55,70,51,42,2,37,30,36,3,35])). % 59.97/60.04 cnf(781,plain, % 59.97/60.04 (P1(f18(f18(a22,a22),f18(a22,a22)))), % 59.97/60.04 inference(scs_inference,[],[694,755,765,771,751,55,70,51,42,2,37,30,36,3,35,284])). % 59.97/60.04 cnf(783,plain, % 59.97/60.04 (E(f17(f18(a22,a22),f18(f18(a22,a22),f18(a22,a22))),f18(a22,a22))), % 59.97/60.04 inference(scs_inference,[],[694,755,765,771,751,55,70,51,42,2,37,30,36,3,35,284,290])). % 59.97/60.04 cnf(785,plain, % 59.97/60.04 (P5(f17(a22,f18(a22,a22)),f17(a22,f18(a22,a22)))), % 59.97/60.04 inference(scs_inference,[],[694,755,765,771,762,751,55,70,51,42,2,37,30,36,3,35,284,290,112])). % 59.97/60.04 cnf(789,plain, % 59.97/60.04 (P3(f17(a22,a4),f16(a25,a7))), % 59.97/60.04 inference(scs_inference,[],[694,755,765,771,762,740,751,55,41,70,51,42,2,37,30,36,3,35,284,290,112,122,423])). % 59.97/60.04 cnf(790,plain, % 59.97/60.04 (P3(f17(a22,a4),f16(a21,a22))), % 59.97/60.04 inference(scs_inference,[],[694,755,765,771,762,740,751,55,41,70,51,42,2,37,30,36,3,35,284,290,112,122,423,469])). % 59.97/60.04 cnf(795,plain, % 59.97/60.04 (P5(a2,a2)), % 59.97/60.04 inference(scs_inference,[],[694,556,755,765,771,762,740,751,479,55,39,41,70,45,51,42,2,37,30,36,3,35,284,290,112,122,423,469,487,34,283,100,103])). % 59.97/60.04 cnf(801,plain, % 59.97/60.04 (E(f18(a22,a22),f17(f18(a22,a22),f18(f18(a22,a22),f18(a22,a22))))), % 59.97/60.04 inference(scs_inference,[],[783,2])). % 59.97/60.04 cnf(802,plain, % 59.97/60.04 (P5(f17(a22,f18(a22,a22)),a22)), % 59.97/60.04 inference(scs_inference,[],[755,783,785,2,37])). % 59.97/60.04 cnf(805,plain, % 59.97/60.04 (P1(f18(a2,a2))), % 59.97/60.04 inference(scs_inference,[],[755,783,785,795,704,63,45,2,37,3,36,284])). % 59.97/60.04 cnf(807,plain, % 59.97/60.04 (E(f17(a2,f18(a2,a2)),a2)), % 59.97/60.04 inference(scs_inference,[],[755,783,785,795,704,63,45,2,37,3,36,284,290])). % 59.97/60.04 cnf(811,plain, % 59.97/60.04 (~P3(a25,f17(a22,a4))), % 59.97/60.04 inference(scs_inference,[],[755,781,783,499,785,777,780,795,704,76,63,45,44,2,37,3,36,284,290,112,115])). % 59.97/60.04 cnf(817,plain, % 59.97/60.04 (~E(f16(a25,a7),f17(a22,a4))), % 59.97/60.04 inference(scs_inference,[],[343,807,811,2,34])). % 59.97/60.04 cnf(819,plain, % 59.97/60.04 (P1(f17(a2,f18(a2,a2)))), % 59.97/60.04 inference(scs_inference,[],[343,606,807,708,811,45,2,34,37,30])). % 59.97/60.04 cnf(821,plain, % 59.97/60.04 (~E(f17(a21,f18(a21,a21)),a24)), % 59.97/60.04 inference(scs_inference,[],[343,606,776,807,708,704,811,77,53,45,2,34,37,30,3,36])). % 59.97/60.04 cnf(822,plain, % 59.97/60.04 (P5(f18(a2,a2),f18(a2,a2))), % 59.97/60.04 inference(scs_inference,[],[343,606,776,805,807,708,704,811,77,53,45,2,34,37,30,3,36,112])). % 59.97/60.04 cnf(824,plain, % 59.97/60.04 (E(f17(f18(a2,a2),f18(f18(a2,a2),f18(a2,a2))),f18(a2,a2))), % 59.97/60.04 inference(scs_inference,[],[343,606,776,805,807,708,704,811,77,53,45,2,34,37,30,3,36,112,290])). % 59.97/60.04 cnf(826,plain, % 59.97/60.04 (~E(f18(a21,a21),f18(a24,a21))), % 59.97/60.04 inference(scs_inference,[],[343,606,776,805,807,708,704,57,40,811,77,53,45,42,2,34,37,30,3,36,112,290,130])). % 59.97/60.04 cnf(833,plain, % 59.97/60.04 (P1(f18(f18(a2,a2),f18(a2,a2)))), % 59.97/60.04 inference(scs_inference,[],[343,606,732,776,805,807,708,777,795,704,59,57,40,811,77,53,45,42,44,43,2,34,37,30,3,36,112,290,130,122,135,35,284])). % 59.97/60.04 cnf(837,plain, % 59.97/60.04 (P5(f17(a22,a4),f17(a22,a4))), % 59.97/60.04 inference(scs_inference,[],[343,606,732,776,805,807,708,777,795,704,405,59,57,40,811,77,53,45,42,44,43,2,34,37,30,3,36,112,290,130,122,135,35,284,283,100,103])). % 59.97/60.04 cnf(844,plain, % 59.97/60.04 (~E(f17(a22,f18(a22,a22)),a24)), % 59.97/60.04 inference(scs_inference,[],[413,802,822,824,76,78,2,37,3,36])). % 59.97/60.04 cnf(845,plain, % 59.97/60.04 (P1(f18(f17(a22,a4),f17(a22,a4)))), % 59.97/60.04 inference(scs_inference,[],[413,802,822,824,837,777,76,78,2,37,3,36,284])). % 59.97/60.04 cnf(849,plain, % 59.97/60.04 (E(f17(f17(a22,a4),f18(f17(a22,a4),f17(a22,a4))),f17(a22,a4))), % 59.97/60.04 inference(scs_inference,[],[413,802,833,822,824,837,777,76,78,2,37,3,36,284,112,290])). % 59.97/60.04 cnf(851,plain, % 59.97/60.04 (~E(f18(a22,a22),f18(a24,a22))), % 59.97/60.04 inference(scs_inference,[],[413,802,833,822,824,837,777,76,58,41,78,42,2,37,3,36,284,112,290,130])). % 59.97/60.04 cnf(853,plain, % 59.97/60.04 (~E(a22,a24)), % 59.97/60.04 inference(scs_inference,[],[413,802,833,822,824,837,777,76,58,41,78,42,2,37,3,36,284,112,290,130,24])). % 59.97/60.04 cnf(857,plain, % 59.97/60.04 (E(f17(a22,a4),f17(f17(a22,a4),f18(f17(a22,a4),f17(a22,a4))))), % 59.97/60.04 inference(scs_inference,[],[849,2])). % 59.97/60.04 cnf(858,plain, % 59.97/60.04 (P5(f18(a23,a25),f17(f18(a23,a25),f18(f18(a23,a25),f18(a23,a25))))), % 59.97/60.04 inference(scs_inference,[],[545,849,490,2,37])). % 59.97/60.04 cnf(860,plain, % 59.97/60.04 (P1(f17(f17(a22,a4),f18(f17(a22,a4),f17(a22,a4))))), % 59.97/60.04 inference(scs_inference,[],[460,545,849,490,777,851,2,37,3,30])). % 59.97/60.04 cnf(862,plain, % 59.97/60.04 (P2(f17(f17(a22,a4),f18(f17(a22,a4),f17(a22,a4))))), % 59.97/60.04 inference(scs_inference,[],[460,545,718,849,761,780,490,777,851,2,37,3,30,36,35])). % 59.97/60.04 cnf(865,plain, % 59.97/60.04 (P5(a22,f17(f17(a22,a4),f18(f17(a22,a4),f17(a22,a4))))), % 59.97/60.04 inference(scs_inference,[],[460,545,718,845,849,761,780,490,777,41,851,47,2,37,3,30,36,35,112,120])). % 59.97/60.04 cnf(871,plain, % 59.97/60.04 (P5(f17(a2,f18(a2,a2)),f17(a2,f18(a2,a2)))), % 59.97/60.04 inference(scs_inference,[],[460,721,545,718,845,821,819,849,761,780,490,777,41,851,47,2,37,3,30,36,35,112,120,283,100,103])). % 59.97/60.04 cnf(873,plain, % 59.97/60.04 (P1(f18(a4,a4))+~P5(a4,a4)), % 59.97/60.04 inference(scs_inference,[],[460,721,545,718,845,821,819,849,761,780,490,777,41,851,47,2,37,3,30,36,35,112,120,283,100,103,284])). % 59.97/60.04 cnf(877,plain, % 59.97/60.04 (E(f17(a4,f18(a4,a4)),a4)+~P5(a4,a4)), % 59.97/60.04 inference(scs_inference,[],[460,721,545,718,845,821,819,849,761,780,490,777,41,851,47,2,37,3,30,36,35,112,120,283,100,103,284,282,290])). % 59.97/60.04 cnf(879,plain, % 59.97/60.04 (E(a23,f17(a25,a6))), % 59.97/60.04 inference(scs_inference,[],[56,2])). % 59.97/60.04 cnf(883,plain, % 59.97/60.04 (P1(f17(a25,a6))), % 59.97/60.04 inference(scs_inference,[],[506,789,807,871,857,56,826,43,2,37,33,3,30])). % 59.97/60.04 cnf(885,plain, % 59.97/60.04 (P5(a3,a3)), % 59.97/60.04 inference(scs_inference,[],[506,789,807,871,857,56,826,46,43,2,37,33,3,30,36,112])). % 59.97/60.04 cnf(887,plain, % 59.97/60.04 (E(f17(a3,f18(a3,a3)),a3)), % 59.97/60.04 inference(scs_inference,[],[506,789,807,871,857,56,826,46,43,2,37,33,3,30,36,112,290])). % 59.97/60.04 cnf(889,plain, % 59.97/60.04 (P3(f17(f17(a22,a4),f18(f17(a22,a4),f17(a22,a4))),f16(a24,a23))), % 59.97/60.04 inference(scs_inference,[],[506,789,556,807,871,857,56,826,46,43,2,37,33,3,30,36,112,290,34])). % 59.97/60.04 cnf(891,plain, % 59.97/60.04 (P1(f18(a3,a3))), % 59.97/60.04 inference(scs_inference,[],[506,694,789,556,807,871,857,56,826,46,43,2,37,33,3,30,36,112,290,34,35,284])). % 59.97/60.04 cnf(897,plain, % 59.97/60.04 (P5(a6,a6)), % 59.97/60.04 inference(scs_inference,[],[506,694,789,556,762,807,844,871,857,56,38,826,46,49,43,2,37,33,3,30,36,112,290,34,35,284,283,100,103])). % 59.97/60.04 cnf(903,plain, % 59.97/60.04 (E(a3,f17(a3,f18(a3,a3)))), % 59.97/60.04 inference(scs_inference,[],[887,2])). % 59.97/60.04 cnf(905,plain, % 59.97/60.04 (P5(a22,f17(a22,a4))), % 59.97/60.04 inference(scs_inference,[],[454,849,865,889,887,2,34,37])). % 59.97/60.04 cnf(908,plain, % 59.97/60.04 (P5(f18(a24,a21),a3)), % 59.97/60.04 inference(scs_inference,[],[790,454,849,857,865,885,889,817,887,358,2,34,37,33,3,36])). % 59.97/60.04 cnf(909,plain, % 59.97/60.04 (P1(f17(a3,f18(a3,a3)))), % 59.97/60.04 inference(scs_inference,[],[790,454,849,857,865,885,889,817,887,358,46,2,34,37,33,3,36,30])). % 59.97/60.04 cnf(910,plain, % 59.97/60.04 (P1(f18(a6,a6))), % 59.97/60.04 inference(scs_inference,[],[790,454,849,857,865,885,889,817,887,897,358,46,49,2,34,37,33,3,36,30,284])). % 59.97/60.04 cnf(912,plain, % 59.97/60.04 (P5(f18(a3,a3),f18(a3,a3))), % 59.97/60.04 inference(scs_inference,[],[790,454,849,857,865,885,891,889,817,887,897,358,46,49,2,34,37,33,3,36,30,284,112])). % 59.97/60.04 cnf(914,plain, % 59.97/60.04 (E(f17(f18(a3,a3),f18(f18(a3,a3),f18(a3,a3))),f18(a3,a3))), % 59.97/60.04 inference(scs_inference,[],[790,454,849,857,865,885,891,889,817,887,897,358,46,49,2,34,37,33,3,36,30,284,112,290])). % 59.97/60.04 cnf(923,plain, % 59.97/60.04 (P5(f17(a25,a6),f17(a25,a6))), % 59.97/60.04 inference(scs_inference,[],[783,790,454,849,857,853,865,885,891,889,817,883,887,897,358,41,46,49,2,34,37,33,3,36,30,284,112,290,122,35,283,100,103])). % 59.97/60.04 cnf(929,plain, % 59.97/60.04 (P5(a20,a24)), % 59.97/60.04 inference(scs_inference,[],[67,391,2])). % 59.97/60.04 cnf(934,plain, % 59.97/60.04 (P1(f18(f18(a3,a3),f18(a3,a3)))), % 59.97/60.04 inference(scs_inference,[],[849,891,912,914,499,2,37,36,3,284])). % 59.97/60.04 cnf(936,plain, % 59.97/60.04 (E(f17(f17(a25,a6),f18(f17(a25,a6),f17(a25,a6))),f17(a25,a6))), % 59.97/60.04 inference(scs_inference,[],[849,891,912,914,923,499,883,2,37,36,3,284,290])). % 59.97/60.04 cnf(938,plain, % 59.97/60.04 (P5(f17(a3,f18(a3,a3)),f17(a3,f18(a3,a3)))), % 59.97/60.04 inference(scs_inference,[],[849,891,912,914,909,923,499,883,2,37,36,3,284,290,112])). % 59.97/60.04 cnf(940,plain, % 59.97/60.04 (~P5(a24,a20)), % 59.97/60.04 inference(scs_inference,[],[849,891,912,914,909,923,499,883,68,39,929,42,2,37,36,3,284,290,112,121])). % 59.97/60.04 cnf(942,plain, % 59.97/60.04 (~P3(a25,f17(f17(a22,a4),f18(f17(a22,a4),f17(a22,a4))))), % 59.97/60.04 inference(scs_inference,[],[849,891,912,914,860,862,909,923,499,883,76,68,39,929,42,44,2,37,36,3,284,290,112,121,115])). % 59.97/60.04 cnf(947,plain, % 59.97/60.04 (E(f17(a25,a6),f17(f17(a25,a6),f18(f17(a25,a6),f17(a25,a6))))), % 59.97/60.04 inference(scs_inference,[],[936,2])). % 59.97/60.04 cnf(953,plain, % 59.97/60.04 (E(f17(a6,f18(a6,a6)),a6)), % 59.97/60.04 inference(scs_inference,[],[452,887,525,936,938,897,883,59,942,940,49,2,34,37,36,3,30,290])). % 59.97/60.04 cnf(955,plain, % 59.97/60.04 (P1(f18(f17(a25,a6),f17(a25,a6)))), % 59.97/60.04 inference(scs_inference,[],[452,887,525,936,938,923,897,883,59,942,940,49,2,34,37,36,3,30,290,284])). % 59.97/60.04 cnf(961,plain, % 59.97/60.04 (P5(a25,f17(f17(a25,a6),f18(f17(a25,a6),f17(a25,a6))))), % 59.97/60.04 inference(scs_inference,[],[452,887,934,525,936,938,923,897,883,59,39,942,940,929,49,42,44,2,34,37,36,3,30,290,284,112,130,120])). % 59.97/60.04 cnf(968,plain, % 59.97/60.04 (P5(f18(a6,a6),f18(a6,a6))), % 59.97/60.04 inference(scs_inference,[],[452,824,887,934,525,936,938,910,860,862,923,897,883,479,59,74,39,942,940,929,49,42,44,43,2,34,37,36,3,30,290,284,112,130,120,115,24,35,100,103])). % 59.97/60.04 cnf(974,plain, % 59.97/60.04 (E(a6,f17(a6,f18(a6,a6)))), % 59.97/60.04 inference(scs_inference,[],[953,2])). % 59.97/60.04 cnf(975,plain, % 59.97/60.04 (P5(f18(a24,a21),f17(a3,f18(a3,a3)))), % 59.97/60.04 inference(scs_inference,[],[903,908,953,2,37])). % 59.97/60.04 cnf(976,plain, % 59.97/60.04 (P5(f17(f18(a24,a21),f18(f18(a24,a21),f18(a24,a21))),a3)), % 59.97/60.04 inference(scs_inference,[],[521,903,908,953,2,37,36])). % 59.97/60.04 cnf(977,plain, % 59.97/60.04 (P1(f17(a6,f18(a6,a6)))), % 59.97/60.04 inference(scs_inference,[],[521,903,908,953,49,2,37,36,30])). % 59.97/60.04 cnf(979,plain, % 59.97/60.04 (E(f17(f18(a6,a6),f18(f18(a6,a6),f18(a6,a6))),f18(a6,a6))), % 59.97/60.04 inference(scs_inference,[],[521,749,903,968,908,953,936,910,49,2,37,36,30,3,290])). % 59.97/60.04 cnf(991,plain, % 59.97/60.04 (P5(a4,a4)), % 59.97/60.04 inference(scs_inference,[],[755,521,955,749,903,968,908,953,936,897,910,883,405,47,49,2,37,36,30,3,290,284,112,122,35,100,283,103])). % 59.97/60.04 cnf(995,plain, % 59.97/60.04 (P1(f18(a4,a4))), % 59.97/60.04 inference(scs_inference,[],[991,873])). % 59.97/60.04 cnf(996,plain, % 59.97/60.04 (E(f17(a4,f18(a4,a4)),a4)), % 59.97/60.04 inference(scs_inference,[],[991,877])). % 59.97/60.04 cnf(1000,plain, % 59.97/60.04 (~E(f18(a22,a22),a4)), % 59.97/60.04 inference(scs_inference,[],[936,760,961,979,905,388,851,2,37,36,3])). % 59.97/60.04 cnf(1006,plain, % 59.97/60.04 (E(a4,f17(a4,f18(a4,a4)))), % 59.97/60.04 inference(scs_inference,[],[996,2])). % 59.97/60.04 cnf(1007,plain, % 59.97/60.04 (P5(a4,f18(a24,a22))), % 59.97/60.04 inference(scs_inference,[],[996,991,388,2,37])). % 59.97/60.04 cnf(1008,plain, % 59.97/60.04 (P1(f17(a4,f18(a4,a4)))), % 59.97/60.04 inference(scs_inference,[],[996,991,388,47,2,37,30])). % 59.97/60.04 cnf(1009,plain, % 59.97/60.04 (P5(f18(a24,a22),a4)), % 59.97/60.04 inference(scs_inference,[],[996,991,388,47,2,37,30,36])). % 59.97/60.04 cnf(1011,plain, % 59.97/60.04 (P5(f17(a6,f18(a6,a6)),f17(a6,f18(a6,a6)))), % 59.97/60.04 inference(scs_inference,[],[996,977,1000,991,388,47,2,37,30,36,3,112])). % 59.97/60.04 cnf(1018,plain, % 59.97/60.04 (P5(f18(a4,a4),f18(a4,a4))), % 59.97/60.04 inference(scs_inference,[],[436,497,996,977,995,1000,991,388,47,2,37,30,36,3,112,121,35,283,103])). % 59.97/60.04 cnf(1022,plain, % 59.97/60.04 (E(f17(f18(a4,a4),f18(f18(a4,a4),f18(a4,a4))),f18(a4,a4))), % 59.97/60.04 inference(scs_inference,[],[436,497,996,977,995,1000,991,388,47,2,37,30,36,3,112,121,35,283,103,282,290])). % 59.97/60.04 cnf(1029,plain, % 59.97/60.04 (~E(f18(a21,a21),a3)), % 59.97/60.04 inference(scs_inference,[],[1022,1018,995,358,826,2,37,30,36,3])). % 59.97/60.04 cnf(1030,plain, % 59.97/60.04 (P1(f18(f18(a4,a4),f18(a4,a4)))), % 59.97/60.04 inference(scs_inference,[],[1022,1018,995,358,826,2,37,30,36,3,284])). % 59.97/60.04 cnf(1032,plain, % 59.97/60.04 (P5(f17(a4,f18(a4,a4)),f17(a4,f18(a4,a4)))), % 59.97/60.04 inference(scs_inference,[],[1022,1018,1008,995,358,826,2,37,30,36,3,284,112])). % 59.97/60.04 cnf(1035,plain, % 59.97/60.04 (P5(a7,a7)), % 59.97/60.04 inference(scs_inference,[],[914,1022,1018,1008,995,358,826,50,2,37,30,36,3,284,112,35,103])). % 59.97/60.04 cnf(1039,plain, % 59.97/60.04 (E(f17(a7,f18(a7,a7)),a7)), % 59.97/60.04 inference(scs_inference,[],[914,1022,1018,1008,995,479,358,48,826,50,2,37,30,36,3,284,112,35,103,283,100,290])). % 59.97/60.04 cnf(1043,plain, % 59.97/60.04 (P5(a4,f17(f18(a24,a22),f18(f18(a24,a22),f18(a24,a22))))), % 59.97/60.04 inference(scs_inference,[],[1007,1039,476,2,37])). % 59.97/60.04 cnf(1044,plain, % 59.97/60.04 (P1(f17(a7,f18(a7,a7)))), % 59.97/60.04 inference(scs_inference,[],[1007,1039,476,50,2,37,30])). % 59.97/60.04 cnf(1045,plain, % 59.97/60.04 (P5(f17(a4,f18(a4,a4)),f18(a24,a22))), % 59.97/60.04 inference(scs_inference,[],[1007,1006,1039,476,50,2,37,30,36])). % 59.97/60.04 cnf(1047,plain, % 59.97/60.04 (P1(f18(a7,a7))), % 59.97/60.04 inference(scs_inference,[],[887,1007,1006,1029,1039,1035,476,50,2,37,30,36,3,284])). % 59.97/60.04 cnf(1054,plain, % 59.97/60.04 (P5(a24,a24)), % 59.97/60.04 inference(scs_inference,[],[807,887,1007,1030,1006,1029,1039,1035,476,40,50,42,2,37,30,36,3,284,112,35,283,103])). % 59.97/60.04 cnf(1059,plain, % 59.97/60.04 (E(f18(a24,a21),a3)), % 59.97/60.04 inference(scs_inference,[],[358,2])). % 59.97/60.04 cnf(1060,plain, % 59.97/60.04 (P5(f18(a24,a22),f17(a4,f18(a4,a4)))), % 59.97/60.04 inference(scs_inference,[],[1009,1006,358,2,37])). % 59.97/60.04 cnf(1061,plain, % 59.97/60.04 (P5(f17(f18(a24,a22),f18(f18(a24,a22),f18(a24,a22))),a4)), % 59.97/60.04 inference(scs_inference,[],[1009,1006,476,358,2,37,36])). % 59.97/60.04 cnf(1062,plain, % 59.97/60.04 (E(f17(a6,f18(a6,a6)),f18(a23,a25))), % 59.97/60.04 inference(scs_inference,[],[953,1009,1006,476,358,419,2,37,36,3])). % 59.97/60.04 cnf(1063,plain, % 59.97/60.04 (E(f17(a24,f18(a24,a24)),a24)), % 59.97/60.04 inference(scs_inference,[],[953,1009,1054,1006,476,358,419,42,2,37,36,3,290])). % 59.97/60.04 cnf(1065,plain, % 59.97/60.04 (P1(f18(a24,a24))), % 59.97/60.04 inference(scs_inference,[],[953,1009,1054,1006,476,358,419,42,2,37,36,3,290,284])). % 59.97/60.04 cnf(1067,plain, % 59.97/60.04 (P5(f18(a7,a7),f18(a7,a7))), % 59.97/60.04 inference(scs_inference,[],[953,1009,1047,1054,1006,476,358,419,42,2,37,36,3,290,284,112])). % 59.97/60.04 cnf(1069,plain, % 59.97/60.04 (P5(a6,f18(a23,a25))), % 59.97/60.04 inference(scs_inference,[],[455,910,953,1009,1047,1054,1006,476,358,419,49,42,2,37,36,3,290,284,112,120])). % 59.97/60.04 cnf(1073,plain, % 59.97/60.04 (E(f18(a6,a6),f18(f18(a23,a25),a6))), % 59.97/60.04 inference(scs_inference,[],[436,455,910,953,1009,1008,1045,1047,1054,1006,476,358,419,49,42,2,37,36,3,290,284,112,120,121,136])). % 59.97/60.04 cnf(1075,plain, % 59.97/60.04 (P1(f18(f18(a23,a25),a6))), % 59.97/60.04 inference(scs_inference,[],[436,455,910,953,1009,1008,1045,1047,1054,1006,476,358,419,49,42,2,37,36,3,290,284,112,120,121,136,30])). % 59.97/60.04 cnf(1077,plain, % 59.97/60.04 (P5(f17(a7,f18(a7,a7)),f17(a7,f18(a7,a7)))), % 59.97/60.04 inference(scs_inference,[],[436,455,910,979,953,1009,1008,1045,1047,1044,1054,1006,476,358,419,49,42,2,37,36,3,290,284,112,120,121,136,30,35,103])). % 59.97/60.04 cnf(1083,plain, % 59.97/60.04 (E(f18(a23,a25),f17(a6,f18(a6,a6)))), % 59.97/60.04 inference(scs_inference,[],[1062,2])). % 59.97/60.04 cnf(1084,plain, % 59.97/60.04 (~E(a24,a23)), % 59.97/60.04 inference(scs_inference,[],[79,1054,1062,2,37])). % 59.97/60.04 cnf(1085,plain, % 59.97/60.04 (P5(a3,f17(f18(a24,a21),f18(f18(a24,a21),f18(a24,a21))))), % 59.97/60.04 inference(scs_inference,[],[79,527,1054,1062,1059,2,37,36])). % 59.97/60.04 cnf(1086,plain, % 59.97/60.04 (~E(a25,f17(a24,f18(a24,a24)))), % 59.97/60.04 inference(scs_inference,[],[79,361,527,1054,1062,1059,1063,2,37,36,3])). % 59.97/60.04 cnf(1087,plain, % 59.97/60.04 (E(f17(f18(a7,a7),f18(f18(a7,a7),f18(a7,a7))),f18(a7,a7))), % 59.97/60.04 inference(scs_inference,[],[79,361,527,1054,1047,1062,1067,1059,1063,2,37,36,3,290])). % 59.97/60.04 cnf(1091,plain, % 59.97/60.04 (P1(f18(f18(a7,a7),f18(a7,a7)))), % 59.97/60.04 inference(scs_inference,[],[79,361,527,1054,1047,1062,1067,1075,1059,1063,2,37,36,3,290,112,284])). % 59.97/60.04 cnf(1097,plain, % 59.97/60.04 (E(f18(a4,a4),f18(f18(a24,a22),a4))), % 59.97/60.04 inference(scs_inference,[],[79,436,361,527,995,1008,1007,1054,1047,1060,1062,1067,1075,1059,1063,1045,1035,47,50,2,37,36,3,290,112,284,122,121,136])). % 59.97/60.04 cnf(1099,plain, % 59.97/60.04 (P1(f18(f18(a24,a22),a4))), % 59.97/60.04 inference(scs_inference,[],[79,436,361,527,995,1008,1007,1054,1047,1060,1062,1067,1075,1059,1063,1045,1035,47,50,2,37,36,3,290,112,284,122,121,136,30])). % 59.97/60.04 cnf(1101,plain, % 59.97/60.04 (P5(f18(a24,a24),f18(a24,a24))), % 59.97/60.04 inference(scs_inference,[],[79,436,361,527,995,556,1008,1007,1054,1047,1060,1062,1067,1075,1065,1059,1063,1045,1035,47,50,2,37,36,3,290,112,284,122,121,136,30,35,103])). % 59.97/60.04 cnf(1110,plain, % 59.97/60.04 (P1(f17(a24,f18(a24,a24)))), % 59.97/60.04 inference(scs_inference,[],[996,1063,1032,42,2,37,36,30])). % 59.97/60.04 cnf(1111,plain, % 59.97/60.04 (E(f18(a23,a25),a6)), % 59.97/60.04 inference(scs_inference,[],[953,996,1063,1032,1083,42,2,37,36,30,3])). % 59.97/60.04 cnf(1112,plain, % 59.97/60.04 (P2(f17(a24,f18(a24,a24)))), % 59.97/60.04 inference(scs_inference,[],[953,996,1063,1032,1083,51,42,2,37,36,30,3,35])). % 59.97/60.04 cnf(1113,plain, % 59.97/60.04 (E(f17(f18(a24,a24),f18(f18(a24,a24),f18(a24,a24))),f18(a24,a24))), % 59.97/60.04 inference(scs_inference,[],[953,996,1063,1032,1083,1101,1065,51,42,2,37,36,30,3,35,290])). % 59.97/60.04 cnf(1115,plain, % 59.97/60.04 (P1(f18(f18(a24,a24),f18(a24,a24)))), % 59.97/60.04 inference(scs_inference,[],[953,996,1063,1032,1083,1101,1065,51,42,2,37,36,30,3,35,290,284])). % 59.97/60.04 cnf(1127,plain, % 59.97/60.04 (P5(f18(f18(a24,a22),a4),f18(f18(a24,a22),a4))), % 59.97/60.04 inference(scs_inference,[],[556,953,996,1063,1054,1032,1083,1091,1101,1099,976,1085,508,1065,46,51,42,2,37,36,30,3,35,290,284,112,122,121,423,487,469,34,103])). % 59.97/60.04 cnf(1138,plain, % 59.97/60.04 (E(f17(f18(a23,a25),f18(f18(a23,a25),f18(a23,a25))),a6)), % 59.97/60.04 inference(scs_inference,[],[533,953,1087,858,1011,1111,2,37,36,3])). % 59.97/60.04 cnf(1143,plain, % 59.97/60.04 (E(f17(f18(a24,a22),f18(f18(a24,a22),f18(a24,a22))),a4)), % 59.97/60.04 inference(scs_inference,[],[455,533,529,953,1087,858,1011,462,1115,1043,1061,1111,47,49,2,37,36,3,112,120,121])). % 59.97/60.04 cnf(1145,plain, % 59.97/60.04 (~P3(a25,f17(a24,f18(a24,a24)))), % 59.97/60.04 inference(scs_inference,[],[455,533,529,953,1087,858,1011,462,1115,1043,1110,1112,1061,1111,1086,76,47,49,44,2,37,36,3,112,120,121,115])). % 59.97/60.04 cnf(1147,plain, % 59.97/60.04 (E(f18(f18(a23,a25),f18(a23,a25)),f18(a6,f18(a23,a25)))), % 59.97/60.04 inference(scs_inference,[],[455,533,529,953,1087,858,1011,462,1115,1043,1110,1112,1061,1111,1086,76,47,49,44,2,37,36,3,112,120,121,115,136])). % 59.97/60.04 cnf(1149,plain, % 59.97/60.04 (P1(f18(a6,f18(a23,a25)))), % 59.97/60.04 inference(scs_inference,[],[455,533,529,953,1087,858,1011,462,1115,1043,1110,1112,1061,1111,1086,76,47,49,44,2,37,36,3,112,120,121,115,136,30])). % 59.97/60.04 cnf(1151,plain, % 59.97/60.04 (P5(f17(a24,f18(a24,a24)),f17(a24,f18(a24,a24)))), % 59.97/60.04 inference(scs_inference,[],[455,533,529,887,953,1087,858,1011,462,1115,1043,1110,1112,1061,1111,1086,76,47,49,44,2,37,36,3,112,120,121,115,136,30,35,103])). % 59.97/60.04 cnf(1160,plain, % 59.97/60.04 (P5(f18(f18(a23,a25),f18(a23,a25)),f18(a6,f18(a23,a25)))), % 59.97/60.04 inference(scs_inference,[],[343,1113,549,1147,1145,2,34,37])). % 59.97/60.04 cnf(1161,plain, % 59.97/60.04 (P5(f18(a6,f18(a23,a25)),f18(f18(a23,a25),f18(a23,a25)))), % 59.97/60.04 inference(scs_inference,[],[343,1113,549,1147,1145,2,34,37,36])). % 59.97/60.04 cnf(1162,plain, % 59.97/60.04 (~E(a24,f17(a25,a6))), % 59.97/60.04 inference(scs_inference,[],[343,1113,549,1084,56,1147,1145,2,34,37,36,3])). % 59.97/60.04 cnf(1169,plain, % 59.97/60.04 (E(f18(f18(a24,a22),f18(a24,a22)),f18(a4,f18(a24,a22)))), % 59.97/60.04 inference(scs_inference,[],[436,343,458,1009,1113,549,1084,1149,462,1043,1061,1110,59,56,47,1147,1143,1145,44,43,2,34,37,36,3,112,121,135,136])). % 59.97/60.04 cnf(1171,plain, % 59.97/60.04 (P1(f18(a4,f18(a24,a22)))), % 59.97/60.04 inference(scs_inference,[],[436,343,458,1009,1113,549,1084,1149,462,1043,1061,1110,59,56,47,1147,1143,1145,44,43,2,34,37,36,3,112,121,135,136,30])). % 59.97/60.04 cnf(1173,plain, % 59.97/60.04 (P5(a25,a25)), % 59.97/60.04 inference(scs_inference,[],[436,343,458,1022,1009,1113,549,1084,1149,462,1043,1061,1110,59,56,47,1147,1143,1145,44,43,2,34,37,36,3,112,121,135,136,30,35,103])). % 59.97/60.04 cnf(1175,plain, % 59.97/60.04 (E(f17(a25,f18(a25,a25)),a25)), % 59.97/60.04 inference(scs_inference,[],[436,343,458,1022,1009,1113,549,1084,1149,462,1043,1061,1110,59,56,47,1147,1143,1145,44,43,2,34,37,36,3,112,121,135,136,30,35,103,290])). % 59.97/60.04 cnf(1179,plain, % 59.97/60.04 (P5(f18(f18(a24,a22),f18(a24,a22)),f18(a4,f18(a24,a22)))), % 59.97/60.04 inference(scs_inference,[],[1138,482,1169,2,37])). % 59.97/60.04 cnf(1180,plain, % 59.97/60.04 (P5(f18(a4,f18(a24,a22)),f18(f18(a24,a22),f18(a24,a22)))), % 59.97/60.04 inference(scs_inference,[],[1138,482,1169,2,37,36])). % 59.97/60.04 cnf(1182,plain, % 59.97/60.04 (P1(f18(a25,a25))), % 59.97/60.04 inference(scs_inference,[],[936,1138,482,1162,1173,1169,44,2,37,36,3,284])). % 59.97/60.04 cnf(1189,plain, % 59.97/60.04 (E(f17(a23,f18(a23,a23)),a23)+~P5(a23,a23)), % 59.97/60.04 inference(scs_inference,[],[529,372,936,1138,1149,482,1160,1161,1171,1162,1173,1169,44,43,2,37,36,3,284,112,121,35,290])). % 59.97/60.04 cnf(1191,plain, % 59.97/60.04 (P5(a23,a23)), % 59.97/60.04 inference(scs_inference,[],[529,372,936,1138,1149,482,1160,1161,1171,1162,1173,1169,44,43,2,37,36,3,284,112,121,35,290,103])). % 59.97/60.04 cnf(1194,plain, % 59.97/60.04 (P5(a20,a23)), % 59.97/60.04 inference(scs_inference,[],[72,425,2])). % 59.97/60.04 cnf(1195,plain, % 59.97/60.04 (E(f17(a23,f18(a23,a23)),a23)), % 59.97/60.04 inference(scs_inference,[],[1191,1189])). % 59.97/60.04 cnf(1196,plain, % 59.97/60.04 (E(a25,f17(a25,f18(a25,a25)))), % 59.97/60.04 inference(scs_inference,[],[1175,2])). % 59.97/60.04 cnf(1199,plain, % 59.97/60.04 (P1(f17(a25,f18(a25,a25)))), % 59.97/60.04 inference(scs_inference,[],[343,1039,1175,1077,44,2,33,37,30])). % 59.97/60.04 cnf(1201,plain, % 59.97/60.04 (~E(a1,f17(a25,f18(a25,a25)))), % 59.97/60.04 inference(scs_inference,[],[343,1039,1175,974,1069,1077,75,44,2,33,37,30,36,3])). % 59.97/60.04 cnf(1202,plain, % 59.97/60.04 (P2(f17(a25,f18(a25,a25)))), % 59.97/60.04 inference(scs_inference,[],[343,1039,1175,974,1069,1077,75,44,52,2,33,37,30,36,3,35])). % 59.97/60.04 cnf(1203,plain, % 59.97/60.04 (P1(f18(a23,a23))), % 59.97/60.04 inference(scs_inference,[],[343,1039,1175,974,1069,1077,1191,75,44,52,43,2,33,37,30,36,3,35,284])). % 59.97/60.04 cnf(1205,plain, % 59.97/60.04 (P5(f18(a25,a25),f18(a25,a25))), % 59.97/60.04 inference(scs_inference,[],[343,1039,1175,974,1069,1077,1182,1191,75,44,52,43,2,33,37,30,36,3,35,284,112])). % 59.97/60.04 cnf(1210,plain, % 59.97/60.04 (P3(f17(a25,f18(a25,a25)),a23)), % 59.97/60.04 inference(scs_inference,[],[343,458,1039,1175,974,1171,1069,1077,1182,1179,1180,1191,75,44,52,43,2,33,37,30,36,3,35,284,112,121,537,443])). % 59.97/60.04 cnf(1211,plain, % 59.97/60.04 (P3(f17(a25,f18(a25,a25)),f16(a24,a23))), % 59.97/60.04 inference(scs_inference,[],[343,458,556,1039,1175,974,1171,1069,1077,1182,1179,1180,1191,75,44,52,43,2,33,37,30,36,3,35,284,112,121,537,443,34])). % 59.97/60.04 cnf(1212,plain, % 59.97/60.04 (E(f17(f18(a25,a25),f18(f18(a25,a25),f18(a25,a25))),f18(a25,a25))), % 59.97/60.04 inference(scs_inference,[],[343,458,556,1039,1175,974,1171,1069,1077,1182,1179,1180,1191,75,44,52,43,2,33,37,30,36,3,35,284,112,121,537,443,34,290])). % 59.97/60.04 cnf(1214,plain, % 59.97/60.04 (P5(f17(a25,f18(a25,a25)),f17(a25,f18(a25,a25)))), % 59.97/60.04 inference(scs_inference,[],[343,458,556,1039,1175,974,1171,1069,1077,1182,1179,1180,1191,75,44,52,43,2,33,37,30,36,3,35,284,112,121,537,443,34,290,103])). % 59.97/60.04 cnf(1225,plain, % 59.97/60.04 (P3(f17(a25,f18(a25,a25)),f16(a24,a2))), % 59.97/60.04 inference(scs_inference,[],[454,1212,1211,2,34])). % 59.97/60.04 cnf(1226,plain, % 59.97/60.04 (P3(a25,f16(a24,a23))), % 59.97/60.04 inference(scs_inference,[],[454,1175,1212,1211,2,34,33])). % 59.97/60.04 cnf(1228,plain, % 59.97/60.04 (P5(a24,f17(a24,f18(a24,a24)))), % 59.97/60.04 inference(scs_inference,[],[454,1063,1175,1151,1212,1211,2,34,33,37,36])). % 59.97/60.04 cnf(1230,plain, % 59.97/60.04 (P1(f18(f18(a25,a25),f18(a25,a25)))), % 59.97/60.04 inference(scs_inference,[],[454,1063,1175,1182,1151,1205,1212,1211,1195,1084,2,34,33,37,36,3,284])). % 59.97/60.04 cnf(1232,plain, % 59.97/60.04 (P5(f18(a23,a23),f18(a23,a23))), % 59.97/60.04 inference(scs_inference,[],[454,1063,1175,1182,1151,1205,1212,1203,1211,1195,1084,2,34,33,37,36,3,284,112])). % 59.97/60.04 cnf(1240,plain, % 59.97/60.04 (E(f18(f18(a24,a21),f18(a24,a21)),f18(a3,f18(a24,a21)))), % 59.97/60.04 inference(scs_inference,[],[79,375,504,454,1063,1175,1110,1182,1151,1205,1212,1199,1202,1203,1211,1195,1201,1084,976,1085,508,908,38,46,66,42,43,2,34,33,37,36,3,284,112,121,134,115,136])). % 59.97/60.04 cnf(1242,plain, % 59.97/60.04 (P1(f18(a3,f18(a24,a21)))), % 59.97/60.04 inference(scs_inference,[],[79,375,504,454,1063,1175,1110,1182,1151,1205,1212,1199,1202,1203,1211,1195,1201,1084,976,1085,508,908,38,46,66,42,43,2,34,33,37,36,3,284,112,121,134,115,136,30])). % 59.97/60.04 cnf(1244,plain, % 59.97/60.04 (E(f17(f18(a23,a23),f18(f18(a23,a23),f18(a23,a23))),f18(a23,a23))), % 59.97/60.04 inference(scs_inference,[],[79,375,504,1062,454,1063,1175,1110,1182,1151,1205,1212,1199,1202,1203,1211,1195,1201,1084,976,1085,508,908,38,46,66,42,43,2,34,33,37,36,3,284,112,121,134,115,136,30,35,290])). % 59.97/60.04 cnf(1255,plain, % 59.97/60.04 (P3(f17(a25,f18(a25,a25)),f17(a25,a6))), % 59.97/60.04 inference(scs_inference,[],[1195,879,1210,2,34])). % 59.97/60.04 cnf(1256,plain, % 59.97/60.04 (P3(a25,f16(a24,a2))), % 59.97/60.04 inference(scs_inference,[],[1175,1195,879,1210,1225,2,34,33])). % 59.97/60.04 cnf(1265,plain, % 59.97/60.04 (~P5(a23,a20)), % 59.97/60.04 inference(scs_inference,[],[1175,1195,879,1203,531,1232,1210,1242,1225,1084,74,39,63,43,1194,1240,2,34,33,37,30,36,3,284,112,121])). % 59.97/60.04 cnf(1268,plain, % 59.97/60.04 (P5(f17(a23,f18(a23,a23)),f17(a23,f18(a23,a23)))), % 59.97/60.04 inference(scs_inference,[],[947,1175,1195,879,1203,531,1232,1210,1242,1225,1084,74,39,63,43,1194,1240,2,34,33,37,30,36,3,284,112,121,35,103])). % 59.97/60.04 cnf(1276,plain, % 59.97/60.04 (P3(a25,f17(a25,a6))), % 59.97/60.04 inference(scs_inference,[],[1175,1244,1256,1255,727,2,34,33])). % 59.97/60.04 cnf(1278,plain, % 59.97/60.04 (~E(f17(a20,f18(a20,a20)),a23)), % 59.97/60.04 inference(scs_inference,[],[79,452,1175,1244,1228,1256,1255,1265,727,2,34,33,37,36])). % 59.97/60.04 cnf(1301,plain, % 59.97/60.04 (~P2(f18(f18(a1,a1),a1))), % 59.97/60.04 inference(scs_inference,[],[567,1195,1228,539,1226,1278,466,362,942,2,34,37,36,3,35])). % 59.97/60.04 cnf(1337,plain, % 59.97/60.04 (P5(a3,f18(a24,a21))), % 59.97/60.04 inference(scs_inference,[],[506,1256,1085,1073,376,2,34,37])). % 59.97/60.04 cnf(1351,plain, % 59.97/60.04 (P5(f18(f18(a24,a22),a4),f18(a4,a4))), % 59.97/60.04 inference(scs_inference,[],[1226,1127,1097,727,2,34,37])). % 59.97/60.04 cnf(1369,plain, % 59.97/60.04 (E(f18(a3,a3),f18(f18(a24,a21),a3))), % 59.97/60.04 inference(scs_inference,[],[375,570,891,883,909,1175,903,1276,1337,1214,975,46,44,60,612,2,34,37,36,121,135,136])). % 59.97/60.04 cnf(1374,plain, % 59.97/60.04 (E(f16(a21,a22),f16(a24,a2))), % 59.97/60.04 inference(scs_inference,[],[61,2])). % 59.97/60.04 cnf(1376,plain, % 59.97/60.04 (P1(f18(f18(a24,a21),a3))), % 59.97/60.04 inference(scs_inference,[],[891,1276,61,1369,942,2,34,30])). % 59.97/60.04 cnf(1378,plain, % 59.97/60.04 (P5(a23,f17(a23,f18(a23,a23)))), % 59.97/60.04 inference(scs_inference,[],[891,1195,1276,1268,61,1369,942,2,34,30,37,36])). % 59.97/60.04 cnf(1379,plain, % 59.97/60.04 (P5(f18(f18(a24,a21),a3),f18(f18(a24,a21),a3))), % 59.97/60.04 inference(scs_inference,[],[891,1195,1276,1268,61,1369,942,2,34,30,37,36,112])). % 59.97/60.04 cnf(1389,plain, % 59.97/60.04 (E(a23,f19(f16(a21,a22),a24))), % 59.97/60.04 inference(scs_inference,[],[63,2])). % 59.97/60.04 cnf(1391,plain, % 59.97/60.04 (P1(f19(f16(a21,a22),a24))), % 59.97/60.04 inference(scs_inference,[],[1276,43,63,727,2,34,30])). % 59.97/60.04 cnf(1394,plain, % 59.97/60.04 (P5(f19(f16(a21,a22),a24),f19(f16(a21,a22),a24))), % 59.97/60.04 inference(scs_inference,[],[448,879,1276,1378,43,63,727,2,34,30,37,36,112])). % 59.97/60.04 cnf(1400,plain, % 59.97/60.04 (E(a23,f16(a25,a5))), % 59.97/60.04 inference(scs_inference,[],[53,2])). % 59.97/60.04 cnf(1402,plain, % 59.97/60.04 (P1(f16(a25,a5))), % 59.97/60.04 inference(scs_inference,[],[1276,43,53,1145,2,34,30])). % 59.97/60.04 cnf(1405,plain, % 59.97/60.04 (P5(f16(a25,a5),f16(a25,a5))), % 59.97/60.04 inference(scs_inference,[],[1276,1394,43,53,63,1145,2,34,30,37,36,112])). % 59.97/60.04 cnf(1410,plain, % 59.97/60.04 (E(f17(f16(a25,a5),f18(f16(a25,a5),f16(a25,a5))),f16(a25,a5))), % 59.97/60.04 inference(scs_inference,[],[448,1212,1276,1394,1391,42,43,53,63,1145,2,34,30,37,36,112,134,35,290])). % 59.97/60.04 cnf(1412,plain, % 59.97/60.04 (P1(f18(f16(a25,a5),f16(a25,a5)))), % 59.97/60.04 inference(scs_inference,[],[448,1212,1276,1394,1391,42,43,53,63,1145,2,34,30,37,36,112,134,35,290,284])). % 59.97/60.04 cnf(1424,plain, % 59.97/60.04 (E(f16(a25,a5),f17(f16(a25,a5),f18(f16(a25,a5),f16(a25,a5))))), % 59.97/60.04 inference(scs_inference,[],[1410,2])). % 59.97/60.04 cnf(1426,plain, % 59.97/60.04 (P5(f16(a25,a5),a23)), % 59.97/60.04 inference(scs_inference,[],[1276,1405,1410,53,811,2,34,37])). % 59.97/60.04 cnf(1429,plain, % 59.97/60.04 (P3(a25,f17(f16(a25,a5),f18(f16(a25,a5),f16(a25,a5))))), % 59.97/60.04 inference(scs_inference,[],[1276,1405,1410,1402,48,44,53,811,2,34,37,30,36,119])). % 59.97/60.04 cnf(1431,plain, % 59.97/60.04 (~P5(f16(a25,a5),a24)), % 59.97/60.04 inference(scs_inference,[],[448,1276,1405,1410,1402,48,42,44,43,53,811,2,34,37,30,36,119,134])). % 59.97/60.04 cnf(1503,plain, % 59.97/60.04 (P5(a25,f17(a25,f18(a25,a25)))), % 59.97/60.04 inference(scs_inference,[],[1175,1410,801,558,1214,771,3,37,36])). % 59.97/60.04 cnf(1515,plain, % 59.97/60.04 (P3(f17(a25,f18(a25,a25)),f16(a25,a5))), % 59.97/60.04 inference(scs_inference,[],[1400,1210,34])). % 59.97/60.04 cnf(1519,plain, % 59.97/60.04 (P3(a25,f16(a25,a5))), % 59.97/60.04 inference(scs_inference,[],[947,1175,1410,1400,1210,1378,342,923,34,3,37,36,33])). % 59.97/60.04 cnf(1521,plain, % 59.97/60.04 (P3(a25,f18(f16(a25,a5),f16(a25,a5)))), % 59.97/60.04 inference(scs_inference,[],[1402,947,1175,1410,1374,1400,1412,1210,1378,342,923,44,1429,34,3,37,36,33,35,149])). % 59.97/60.04 cnf(1557,plain, % 59.97/60.04 (P5(a25,f16(a25,a5))), % 59.97/60.04 inference(scs_inference,[],[1400,1519,356,727,34,37])). % 59.97/60.04 cnf(1563,plain, % 59.97/60.04 (P5(a20,a25)), % 59.97/60.04 inference(scs_inference,[],[75,472,2])). % 59.97/60.04 cnf(1564,plain, % 59.97/60.04 (~E(f16(a24,a2),f17(a22,a4))), % 59.97/60.04 inference(scs_inference,[],[1256,811,34])). % 59.97/60.04 cnf(1567,plain, % 59.97/60.04 (~P5(a25,a20)), % 59.97/60.04 inference(scs_inference,[],[1196,1256,1424,1557,39,44,76,1563,811,34,37,36,121])). % 59.97/60.04 cnf(1578,plain, % 59.97/60.04 (~E(f17(a25,f18(a25,a25)),a20)), % 59.97/60.04 inference(scs_inference,[],[1503,1521,1567,376,34,37])). % 59.97/60.04 cnf(1704,plain, % 59.97/60.04 (~E(a22,a23)), % 59.97/60.04 inference(scs_inference,[],[448,58,36])). % 59.97/60.04 cnf(2021,plain, % 59.97/60.04 (~P3(f18(f16(a25,a5),f16(a25,a5)),f17(a21,a3))), % 59.97/60.04 inference(scs_inference,[],[570,1519,1412,44,1521,612,34,135])). % 59.97/60.04 cnf(2249,plain, % 59.97/60.04 (P1(f8(f17(a25,f18(a25,a25))))), % 59.97/60.04 inference(scs_inference,[],[79,350,1704,1301,1515,439,1376,624,1202,1112,1389,1379,1210,623,760,55,1578,1195,1110,1199,1402,85,86,87,88,83,84,96,97,98,449,22,23,4,5,6,20,21,25,26,27,28,29,8,9,10,11,12,13,14,15,16,17,18,19,7,2,24,113,114,81,80,33,3,30,34,36,37,35,124,125,89])). % 59.97/60.04 cnf(2251,plain, % 59.97/60.04 (P2(f8(f17(a25,f18(a25,a25))))), % 59.97/60.04 inference(scs_inference,[],[79,350,1704,1301,1515,439,1376,624,1202,1112,1389,1379,1210,623,760,55,1578,1195,1110,1199,1402,85,86,87,88,83,84,96,97,98,449,22,23,4,5,6,20,21,25,26,27,28,29,8,9,10,11,12,13,14,15,16,17,18,19,7,2,24,113,114,81,80,33,3,30,34,36,37,35,124,125,89,90])). % 59.97/60.04 cnf(2253,plain, % 59.97/60.04 (E(f16(a25,f11(a25,f16(a25,a5))),f16(a25,a5))), % 59.97/60.04 inference(scs_inference,[],[79,350,1704,1301,1515,439,1376,624,1202,1112,1389,1379,1210,623,760,55,1578,1195,1519,1110,1199,1402,44,85,86,87,88,83,84,96,97,98,449,22,23,4,5,6,20,21,25,26,27,28,29,8,9,10,11,12,13,14,15,16,17,18,19,7,2,24,113,114,81,80,33,3,30,34,36,37,35,124,125,89,90,132])). % 59.97/60.04 cnf(2255,plain, % 59.97/60.04 (E(f17(f16(a25,a5),f10(f16(a25,a5),a23)),a23)), % 59.97/60.04 inference(scs_inference,[],[79,350,1704,1301,1515,439,1376,1426,624,1202,1112,1389,1379,1210,623,760,55,1578,1195,1519,1110,1199,1402,43,44,85,86,87,88,83,84,96,97,98,449,22,23,4,5,6,20,21,25,26,27,28,29,8,9,10,11,12,13,14,15,16,17,18,19,7,2,24,113,114,81,80,33,3,30,34,36,37,35,124,125,89,90,132,133])). % 59.97/60.04 cnf(2375,plain, % 59.97/60.04 ($false), % 59.97/60.04 inference(scs_inference,[],[79,386,1431,1564,2021,431,2253,2249,2251,2255,1351,415,1230,1099,567,362,771,751,995,448,50,42,43,98,97,96,84,86,28,10,27,20,4,88,83,23,449,26,85,19,18,17,87,22,6,16,8,5,14,12,11,13,9,25,21,29,7,15,2,24,113,114,81,80,33,3,34,36,37,35,124,143,133,152,142,151,112]), % 59.97/60.04 ['proof']). % 59.97/60.04 % SZS output end Proof % 59.97/60.04 % Total time :58.720000s %------------------------------------------------------------------------------