%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : RNG049+2 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n018.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 14:00:51 EDT 2024 % Result : Theorem 122.98s 123.00s % Output : CNFRefutation 122.98s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : RNG049+2 : TPTP v8.2.0. Released v4.0.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.11/0.33 % Computer : n018.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Tue Jun 18 13:43:53 EDT 2024 % 0.11/0.33 % CPUTime : % 0.19/0.55 start to proof:theBenchmark % 122.88/122.98 %------------------------------------------- % 122.88/122.98 % File :CSE---1.7 % 122.88/122.98 % Problem :theBenchmark % 122.88/122.98 % Transform :cnf % 122.88/122.98 % Format :tptp:raw % 122.88/122.98 % Command :java -jar mcs_scs.jar %d %s % 122.88/122.98 % 122.88/122.98 % Result :Theorem 122.350000s % 122.88/122.98 % Output :CNFRefutation 122.350000s % 122.88/122.98 %------------------------------------------- % 122.88/122.99 %------------------------------------------------------------------------------ % 122.88/122.99 % File : RNG049+2 : TPTP v8.2.0. Released v4.0.0. % 122.88/122.99 % Domain : Ring Theory % 122.88/122.99 % Problem : Cauchy-Bouniakowsky-Schwarz inequality 04_03, 01 expansion % 122.88/122.99 % Version : Especial. % 122.88/122.99 % English : % 122.88/122.99 % 122.88/122.99 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 122.88/122.99 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 122.88/122.99 % Source : [Pas08] % 122.88/122.99 % Names : cauchy_04_03.01 [Pas08] % 122.88/122.99 % 122.88/122.99 % Status : Theorem % 122.88/122.99 % Rating : 0.44 v8.2.0, 0.50 v8.1.0, 0.39 v7.5.0, 0.44 v7.4.0, 0.37 v7.3.0, 0.41 v7.2.0, 0.38 v7.1.0, 0.35 v7.0.0, 0.43 v6.4.0, 0.50 v6.3.0, 0.42 v6.2.0, 0.48 v6.1.0, 0.57 v6.0.0, 0.52 v5.5.0, 0.67 v5.4.0, 0.71 v5.3.0, 0.78 v5.2.0, 0.75 v5.1.0, 0.76 v5.0.0, 0.83 v4.1.0, 0.91 v4.0.1, 1.00 v4.0.0 % 122.88/122.99 % Syntax : Number of formulae : 42 ( 5 unt; 1 def) % 122.88/122.99 % Number of atoms : 170 ( 49 equ) % 122.88/122.99 % Maximal formula atoms : 9 ( 4 avg) % 122.88/122.99 % Number of connectives : 134 ( 6 ~; 1 |; 71 &) % 122.88/122.99 % ( 1 <=>; 55 =>; 0 <=; 0 <~>) % 122.88/122.99 % Maximal formula depth : 10 ( 5 avg) % 122.88/122.99 % Maximal term depth : 5 ( 1 avg) % 122.88/122.99 % Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty) % 122.88/122.99 % Number of functors : 11 ( 11 usr; 3 con; 0-2 aty) % 122.88/122.99 % Number of variables : 73 ( 72 !; 1 ?) % 122.88/122.99 % SPC : FOF_THM_RFO_SEQ % 122.88/122.99 % 122.88/122.99 % Comments : Problem generated by the SAD system [VLP07] % 122.88/122.99 %------------------------------------------------------------------------------ % 122.88/122.99 fof(mNatSort,axiom, % 122.88/122.99 ! [W0] : % 122.88/122.99 ( aNaturalNumber0(W0) % 122.88/122.99 => $true ) ). % 122.88/122.99 % 122.88/122.99 fof(mZeroNat,axiom, % 122.88/122.99 aNaturalNumber0(sz00) ). % 122.88/122.99 % 122.88/122.99 fof(mSuccNat,axiom, % 122.88/122.99 ! [W0] : % 122.88/122.99 ( aNaturalNumber0(W0) % 122.88/122.99 => ( aNaturalNumber0(szszuzczcdt0(W0)) % 122.88/122.99 & szszuzczcdt0(W0) != sz00 ) ) ). % 122.88/122.99 % 122.88/122.99 fof(mNatExtr,axiom, % 122.88/122.99 ! [W0] : % 122.88/122.99 ( ( aNaturalNumber0(W0) % 122.88/122.99 & W0 != sz00 ) % 122.88/122.99 => ? [W1] : % 122.88/122.99 ( aNaturalNumber0(W1) % 122.88/122.99 & W0 = szszuzczcdt0(W1) ) ) ). % 122.88/122.99 % 122.88/122.99 fof(mSuccEqu,axiom, % 122.88/122.99 ! [W0,W1] : % 122.88/122.99 ( ( aNaturalNumber0(W0) % 122.88/122.99 & aNaturalNumber0(W1) ) % 122.88/122.99 => ( szszuzczcdt0(W0) = szszuzczcdt0(W1) % 122.88/122.99 => W0 = W1 ) ) ). % 122.88/122.99 % 122.88/122.99 fof(mIHOrd,axiom, % 122.88/122.99 ! [W0,W1] : % 122.88/122.99 ( ( aNaturalNumber0(W0) % 122.88/122.99 & aNaturalNumber0(W1) ) % 122.88/122.99 => ( iLess0(W0,W1) % 122.88/122.99 => $true ) ) ). % 122.88/122.99 % 122.88/122.99 fof(mIH,axiom, % 122.88/122.99 ! [W0] : % 122.88/122.99 ( aNaturalNumber0(W0) % 122.88/122.99 => iLess0(W0,szszuzczcdt0(W0)) ) ). % 122.88/122.99 % 122.88/122.99 fof(mScSort,axiom, % 122.88/122.99 ! [W0] : % 122.88/122.99 ( aScalar0(W0) % 122.88/122.99 => $true ) ). % 122.88/122.99 % 122.88/122.99 fof(mSZeroSc,axiom, % 122.88/122.99 aScalar0(sz0z00) ). % 122.88/122.99 % 122.88/122.99 fof(mSumSc,axiom, % 122.88/122.99 ! [W0,W1] : % 122.88/122.99 ( ( aScalar0(W0) % 122.88/122.99 & aScalar0(W1) ) % 122.88/122.99 => aScalar0(sdtpldt0(W0,W1)) ) ). % 122.88/122.99 % 122.88/122.99 fof(mMulSc,axiom, % 122.88/122.99 ! [W0,W1] : % 122.88/122.99 ( ( aScalar0(W0) % 122.88/122.99 & aScalar0(W1) ) % 122.88/122.99 => aScalar0(sdtasdt0(W0,W1)) ) ). % 122.88/122.99 % 122.88/122.99 fof(mNegSc,axiom, % 122.88/122.99 ! [W0] : % 122.88/122.99 ( aScalar0(W0) % 122.88/122.99 => aScalar0(smndt0(W0)) ) ). % 122.88/122.99 % 122.88/122.99 fof(mScZero,axiom, % 122.88/122.99 ! [W0] : % 122.88/122.99 ( aScalar0(W0) % 122.88/122.99 => ( sdtpldt0(W0,sz0z00) = W0 % 122.88/122.99 & sdtpldt0(sz0z00,W0) = W0 % 122.88/122.99 & sdtasdt0(W0,sz0z00) = sz0z00 % 122.88/122.99 & sdtasdt0(sz0z00,W0) = sz0z00 % 122.88/122.99 & sdtpldt0(W0,smndt0(W0)) = sz0z00 % 122.88/122.99 & sdtpldt0(smndt0(W0),W0) = sz0z00 % 122.88/122.99 & smndt0(smndt0(W0)) = W0 % 122.88/122.99 & smndt0(sz0z00) = sz0z00 ) ) ). % 122.88/122.99 % 122.88/122.99 fof(mArith,axiom, % 122.88/122.99 ! [W0,W1,W2] : % 122.88/122.99 ( ( aScalar0(W0) % 122.88/122.99 & aScalar0(W1) % 122.88/122.99 & aScalar0(W2) ) % 122.88/122.99 => ( sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) % 122.88/122.99 & sdtpldt0(W0,W1) = sdtpldt0(W1,W0) % 122.88/122.99 & sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) % 122.88/122.99 & sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ) ). % 122.88/122.99 % 122.88/122.99 fof(mDistr,axiom, % 122.88/122.99 ! [W0,W1,W2] : % 122.88/122.99 ( ( aScalar0(W0) % 122.88/122.99 & aScalar0(W1) % 122.88/122.99 & aScalar0(W2) ) % 122.88/122.99 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 122.88/122.99 & sdtasdt0(sdtpldt0(W0,W1),W2) = sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W1,W2)) ) ) ). % 122.88/122.99 % 122.88/122.99 fof(mDistr2,axiom, % 122.88/122.99 ! [W0,W1,W2,W3] : % 122.88/122.99 ( ( aScalar0(W0) % 122.88/122.99 & aScalar0(W1) % 122.88/122.99 & aScalar0(W2) % 122.88/122.99 & aScalar0(W3) ) % 122.88/122.99 => sdtasdt0(sdtpldt0(W0,W1),sdtpldt0(W2,W3)) = sdtpldt0(sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W0,W3)),sdtpldt0(sdtasdt0(W1,W2),sdtasdt0(W1,W3))) ) ). % 122.88/122.99 % 122.88/122.99 fof(mMNeg,axiom, % 122.88/122.99 ! [W0,W1] : % 122.88/122.99 ( ( aScalar0(W0) % 122.88/122.99 & aScalar0(W1) ) % 122.88/122.99 => ( sdtasdt0(W0,smndt0(W1)) = smndt0(sdtasdt0(W0,W1)) % 122.88/122.99 & sdtasdt0(smndt0(W0),W1) = smndt0(sdtasdt0(W0,W1)) ) ) ). % 122.88/122.99 % 122.88/122.99 fof(mMDNeg,axiom, % 122.88/122.99 ! [W0,W1] : % 122.88/122.99 ( ( aScalar0(W0) % 122.88/122.99 & aScalar0(W1) ) % 122.88/122.99 => sdtasdt0(smndt0(W0),smndt0(W1)) = sdtasdt0(W0,W1) ) ). % 122.88/122.99 % 122.88/122.99 fof(mLess,axiom, % 122.88/122.99 ! [W0,W1] : % 122.88/122.99 ( ( aScalar0(W0) % 122.88/122.99 & aScalar0(W1) ) % 122.88/122.99 => ( sdtlseqdt0(W0,W1) % 122.88/122.99 => $true ) ) ). % 122.88/122.99 % 122.88/122.99 fof(mLERef,axiom, % 122.88/122.99 ! [W0] : % 122.88/122.99 ( aScalar0(W0) % 122.88/122.99 => sdtlseqdt0(W0,W0) ) ). % 122.88/122.99 % 122.88/122.99 fof(mLEASm,axiom, % 122.88/122.99 ! [W0,W1] : % 122.88/122.99 ( ( aScalar0(W0) % 122.88/122.99 & aScalar0(W1) ) % 122.88/122.99 => ( ( sdtlseqdt0(W0,W1) % 122.88/122.99 & sdtlseqdt0(W1,W0) ) % 122.88/122.99 => W0 = W1 ) ) ). % 122.88/122.99 % 122.88/122.99 fof(mLETrn,axiom, % 122.88/122.99 ! [W0,W1,W2] : % 122.88/122.99 ( ( aScalar0(W0) % 122.88/122.99 & aScalar0(W1) % 122.88/122.99 & aScalar0(W2) ) % 122.88/122.99 => ( ( sdtlseqdt0(W0,W1) % 122.88/122.99 & sdtlseqdt0(W1,W2) ) % 122.88/122.99 => sdtlseqdt0(W0,W2) ) ) ). % 122.88/122.99 % 122.88/122.99 fof(mLEMon,axiom, % 122.88/122.99 ! [W0,W1,W2,W3] : % 122.88/122.99 ( ( aScalar0(W0) % 122.88/122.99 & aScalar0(W1) % 122.88/122.99 & aScalar0(W2) % 122.88/122.99 & aScalar0(W3) ) % 122.88/122.99 => ( ( sdtlseqdt0(W0,W1) % 122.88/122.99 & sdtlseqdt0(W2,W3) ) % 122.88/122.99 => sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W3)) ) ) ). % 122.88/122.99 % 122.88/122.99 fof(mLEMonM,axiom, % 122.88/122.99 ! [W0,W1,W2,W3] : % 122.88/122.99 ( ( aScalar0(W0) % 122.88/122.99 & aScalar0(W1) % 122.88/122.99 & aScalar0(W2) % 122.88/122.99 & aScalar0(W3) ) % 122.88/122.99 => ( ( sdtlseqdt0(W0,W1) % 122.88/122.99 & sdtlseqdt0(sz0z00,W2) % 122.88/122.99 & sdtlseqdt0(W2,W3) ) % 122.88/122.99 => sdtlseqdt0(sdtasdt0(W0,W2),sdtasdt0(W1,W3)) ) ) ). % 122.88/123.00 % 122.88/123.00 fof(mLETot,axiom, % 122.88/123.00 ! [W0,W1] : % 122.88/123.00 ( ( aScalar0(W0) % 122.88/123.00 & aScalar0(W1) ) % 122.88/123.00 => ( sdtlseqdt0(W0,W1) % 122.88/123.00 | sdtlseqdt0(W1,W0) ) ) ). % 122.88/123.00 % 122.88/123.00 fof(mPosMon,axiom, % 122.88/123.00 ! [W0,W1] : % 122.88/123.00 ( ( aScalar0(W0) % 122.88/123.00 & aScalar0(W1) ) % 122.88/123.00 => ( ( sdtlseqdt0(sz0z00,W0) % 122.88/123.00 & sdtlseqdt0(sz0z00,W1) ) % 122.88/123.00 => ( sdtlseqdt0(sz0z00,sdtpldt0(W0,W1)) % 122.88/123.00 & sdtlseqdt0(sz0z00,sdtasdt0(W0,W1)) ) ) ) ). % 122.88/123.00 % 122.88/123.00 fof(mSqPos,axiom, % 122.88/123.00 ! [W0] : % 122.88/123.00 ( aScalar0(W0) % 122.88/123.00 => sdtlseqdt0(sz0z00,sdtasdt0(W0,W0)) ) ). % 122.88/123.00 % 122.88/123.00 fof(mSqrt,axiom, % 122.88/123.00 ! [W0,W1] : % 122.88/123.00 ( ( aScalar0(W0) % 122.88/123.00 & aScalar0(W1) ) % 122.88/123.00 => ( ( sdtlseqdt0(sz0z00,W0) % 122.88/123.00 & sdtlseqdt0(sz0z00,W1) % 122.88/123.00 & sdtasdt0(W0,W0) = sdtasdt0(W1,W1) ) % 122.88/123.00 => W0 = W1 ) ) ). % 122.88/123.00 % 122.88/123.00 fof(mVcSort,axiom, % 122.88/123.00 ! [W0] : % 122.88/123.00 ( aVector0(W0) % 122.88/123.00 => $true ) ). % 122.88/123.00 % 122.88/123.00 fof(mDimNat,axiom, % 122.88/123.00 ! [W0] : % 122.88/123.00 ( aVector0(W0) % 122.88/123.00 => aNaturalNumber0(aDimensionOf0(W0)) ) ). % 122.88/123.00 % 122.88/123.00 fof(mElmSc,axiom, % 122.88/123.00 ! [W0,W1] : % 122.88/123.00 ( ( aVector0(W0) % 122.88/123.00 & aNaturalNumber0(W1) ) % 122.88/123.00 => aScalar0(sdtlbdtrb0(W0,W1)) ) ). % 122.88/123.00 % 122.88/123.00 fof(mDefInit,definition, % 122.88/123.00 ! [W0] : % 122.88/123.00 ( aVector0(W0) % 122.88/123.00 => ( aDimensionOf0(W0) != sz00 % 122.88/123.00 => ! [W1] : % 122.88/123.00 ( W1 = sziznziztdt0(W0) % 122.88/123.00 <=> ( aVector0(W1) % 122.88/123.00 & szszuzczcdt0(aDimensionOf0(W1)) = aDimensionOf0(W0) % 122.88/123.00 & ! [W2] : % 122.88/123.00 ( aNaturalNumber0(W2) % 122.88/123.00 => sdtlbdtrb0(W1,W2) = sdtlbdtrb0(W0,W2) ) ) ) ) ) ). % 122.88/123.00 % 122.88/123.00 fof(mEqInit,axiom, % 122.98/123.00 ! [W0,W1] : % 122.98/123.00 ( ( aVector0(W0) % 122.98/123.00 & aVector0(W1) ) % 122.98/123.00 => ( ( aDimensionOf0(W0) = aDimensionOf0(W1) % 122.98/123.00 & aDimensionOf0(W1) != sz00 ) % 122.98/123.00 => aDimensionOf0(sziznziztdt0(W0)) = aDimensionOf0(sziznziztdt0(W1)) ) ) ). % 122.98/123.00 % 122.98/123.00 fof(mScPr,axiom, % 122.98/123.00 ! [W0,W1] : % 122.98/123.00 ( ( aVector0(W0) % 122.98/123.00 & aVector0(W1) ) % 122.98/123.00 => ( aDimensionOf0(W0) = aDimensionOf0(W1) % 122.98/123.00 => aScalar0(sdtasasdt0(W0,W1)) ) ) ). % 122.98/123.00 % 122.98/123.00 fof(mDefSPZ,axiom, % 122.98/123.00 ! [W0,W1] : % 122.98/123.00 ( ( aVector0(W0) % 122.98/123.00 & aVector0(W1) ) % 122.98/123.00 => ( ( aDimensionOf0(W0) = aDimensionOf0(W1) % 122.98/123.00 & aDimensionOf0(W1) = sz00 ) % 122.98/123.00 => sdtasasdt0(W0,W1) = sz0z00 ) ) ). % 122.98/123.00 % 122.98/123.00 fof(mDefSPN,axiom, % 122.98/123.00 ! [W0,W1] : % 122.98/123.00 ( ( aVector0(W0) % 122.98/123.00 & aVector0(W1) ) % 122.98/123.00 => ( ( aDimensionOf0(W0) = aDimensionOf0(W1) % 122.98/123.00 & aDimensionOf0(W1) != sz00 ) % 122.98/123.00 => sdtasasdt0(W0,W1) = sdtpldt0(sdtasasdt0(sziznziztdt0(W0),sziznziztdt0(W1)),sdtasdt0(sdtlbdtrb0(W0,aDimensionOf0(W0)),sdtlbdtrb0(W1,aDimensionOf0(W1)))) ) ) ). % 122.98/123.00 % 122.98/123.00 fof(m__1542,hypothesis, % 122.98/123.00 aVector0(xs) ). % 122.98/123.00 % 122.98/123.00 fof(m__1516,hypothesis, % 122.98/123.00 ! [W0] : % 122.98/123.00 ( aVector0(W0) % 122.98/123.00 => ( iLess0(aDimensionOf0(W0),aDimensionOf0(xs)) % 122.98/123.00 => sdtlseqdt0(sz0z00,sdtasasdt0(W0,W0)) ) ) ). % 122.98/123.00 % 122.98/123.00 fof(m__1542_01,hypothesis, % 122.98/123.00 aDimensionOf0(xs) != sz00 ). % 122.98/123.00 % 122.98/123.00 fof(m__1568,hypothesis, % 122.98/123.00 ( aVector0(sziznziztdt0(xs)) % 122.98/123.00 & szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs) % 122.98/123.00 & ! [W0] : % 122.98/123.00 ( aNaturalNumber0(W0) % 122.98/123.00 => sdtlbdtrb0(sziznziztdt0(xs),W0) = sdtlbdtrb0(xs,W0) ) % 122.98/123.00 & aVector0(sziznziztdt0(xs)) % 122.98/123.00 & szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs) % 122.98/123.00 & ! [W0] : % 122.98/123.00 ( aNaturalNumber0(W0) % 122.98/123.00 => sdtlbdtrb0(sziznziztdt0(xs),W0) = sdtlbdtrb0(xs,W0) ) ) ). % 122.98/123.00 % 122.98/123.00 fof(m__1590,hypothesis, % 122.98/123.00 ( aVector0(sziznziztdt0(xs)) % 122.98/123.00 & szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs) % 122.98/123.00 & ! [W0] : % 122.98/123.00 ( aNaturalNumber0(W0) % 122.98/123.00 => sdtlbdtrb0(sziznziztdt0(xs),W0) = sdtlbdtrb0(xs,W0) ) % 122.98/123.00 & aVector0(sziznziztdt0(xs)) % 122.98/123.00 & szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs) % 122.98/123.00 & ! [W0] : % 122.98/123.00 ( aNaturalNumber0(W0) % 122.98/123.00 => sdtlbdtrb0(sziznziztdt0(xs),W0) = sdtlbdtrb0(xs,W0) ) % 122.98/123.00 & sdtlseqdt0(sz0z00,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))) ) ). % 122.98/123.00 % 122.98/123.00 fof(m__,conjecture, % 122.98/123.00 sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)) ). % 122.98/123.00 % 122.98/123.00 %------------------------------------------------------------------------------ % 122.98/123.00 %------------------------------------------- % 122.98/123.00 % Proof found % 122.98/123.00 % SZS status Theorem for theBenchmark % 122.98/123.00 % SZS output start Proof % 122.98/123.00 %ClaNum:92(EqnAxiom:25) % 122.98/123.00 %VarNum:300(SingletonVarNum:95) % 122.98/123.00 %MaxLitNum:8 % 122.98/123.00 %MaxfuncDepth:4 % 122.98/123.00 %SharedTerms:20 % 122.98/123.00 %goalClause: 39 % 122.98/123.00 %singleGoalClaCount:1 % 122.98/123.00 [26]P1(a1) % 122.98/123.00 [27]P2(a10) % 122.98/123.00 [28]P3(a11) % 122.98/123.00 [32]P3(f12(a11)) % 122.98/123.00 [38]~E(f2(a11),a1) % 122.98/123.00 [39]~P4(a10,f5(a11,a11)) % 122.98/123.00 [36]E(f13(f2(f12(a11))),f2(a11)) % 122.98/123.00 [37]P4(a10,f4(f3(a11,f2(a11)),f3(a11,f2(a11)))) % 122.98/123.00 [52]~P2(x521)+P4(x521,x521) % 122.98/123.00 [40]~P2(x401)+E(f8(a10),a10) % 122.98/123.00 [41]~P1(x411)+~E(f13(x411),a1) % 122.98/123.00 [42]~P1(x421)+P1(f13(x421)) % 122.98/123.00 [43]~P3(x431)+P1(f2(x431)) % 122.98/123.00 [44]~P2(x441)+P2(f8(x441)) % 122.98/123.00 [47]~P2(x471)+E(f4(x471,a10),a10) % 122.98/123.00 [48]~P2(x481)+E(f4(a10,x481),a10) % 122.98/123.00 [50]~P2(x501)+E(f9(x501,a10),x501) % 122.98/123.00 [51]~P2(x511)+E(f9(a10,x511),x511) % 122.98/123.00 [56]~P1(x561)+P5(x561,f13(x561)) % 122.98/123.00 [67]~P2(x671)+P4(a10,f4(x671,x671)) % 122.98/123.00 [45]~P2(x451)+E(f8(f8(x451)),x451) % 122.98/123.00 [54]~P2(x541)+E(f9(x541,f8(x541)),a10) % 122.98/123.00 [55]~P2(x551)+E(f9(f8(x551),x551),a10) % 122.98/123.00 [62]~P1(x621)+E(f3(f12(a11),x621),f3(a11,x621)) % 122.98/123.00 [46]~P1(x461)+E(x461,a1)+P1(f6(x461)) % 122.98/123.00 [80]~P3(x801)+~P5(f2(x801),f2(a11))+P4(a10,f5(x801,x801)) % 122.98/123.00 [49]~P1(x491)+E(x491,a1)+E(f13(f6(x491)),x491) % 122.98/123.00 [64]~P2(x642)+~P2(x641)+P2(f9(x641,x642)) % 122.98/123.00 [65]~P2(x652)+~P2(x651)+P2(f4(x651,x652)) % 122.98/123.00 [66]~P1(x662)+~P3(x661)+P2(f3(x661,x662)) % 122.98/123.00 [72]~P2(x722)+~P2(x721)+E(f4(f8(x721),f8(x722)),f4(x721,x722)) % 122.98/123.00 [76]~P2(x762)+~P2(x761)+E(f8(f4(x761,x762)),f4(x761,f8(x762))) % 122.98/123.00 [77]~P2(x772)+~P2(x771)+E(f8(f4(x771,x772)),f4(f8(x771),x772)) % 122.98/123.00 [63]P4(x632,x631)+~P2(x631)+~P2(x632)+P4(x631,x632) % 122.98/123.00 [53]~P3(x531)+P3(x532)+~E(x532,f12(x531))+E(f2(x531),a1) % 122.98/123.00 [57]~P1(x572)+~P1(x571)+E(x571,x572)+~E(f13(x571),f13(x572)) % 122.98/123.00 [74]~P3(x742)+~P3(x741)+~E(f2(x741),f2(x742))+P2(f5(x741,x742)) % 122.98/123.00 [58]~P3(x581)+~E(x582,f12(x581))+E(f2(x581),a1)+E(f13(f2(x582)),f2(x581)) % 122.98/123.00 [69]~P2(x692)+~P2(x691)+~P2(x693)+E(f9(x691,x692),f9(x692,x691)) % 122.98/123.00 [70]~P2(x702)+~P2(x701)+~P2(x703)+E(f4(x701,x702),f4(x702,x701)) % 122.98/123.00 [83]~P2(x833)+~P2(x832)+~P2(x831)+E(f9(f9(x831,x832),x833),f9(x831,f9(x832,x833))) % 122.98/123.00 [84]~P2(x843)+~P2(x842)+~P2(x841)+E(f4(f4(x841,x842),x843),f4(x841,f4(x842,x843))) % 122.98/123.00 [86]~P2(x863)+~P2(x862)+~P2(x861)+E(f9(f4(x861,x862),f4(x861,x863)),f4(x861,f9(x862,x863))) % 122.98/123.00 [87]~P2(x872)+~P2(x873)+~P2(x871)+E(f9(f4(x871,x872),f4(x873,x872)),f4(f9(x871,x873),x872)) % 122.98/123.00 [75]~P2(x752)+~P2(x751)+~P4(x752,x751)+~P4(x751,x752)+E(x751,x752) % 122.98/123.00 [68]~P3(x682)+~P3(x681)+~E(f2(x681),f2(x682))+~E(f2(x682),a1)+E(f5(x681,x682),a10) % 122.98/123.00 [81]~P2(x812)+~P2(x811)+~P4(a10,x812)+~P4(a10,x811)+P4(a10,f9(x811,x812)) % 122.98/123.00 [82]~P2(x822)+~P2(x821)+~P4(a10,x822)+~P4(a10,x821)+P4(a10,f4(x821,x822)) % 122.98/123.00 [71]~P3(x711)+~P3(x712)+~E(f2(x712),f2(x711))+E(f2(x711),a1)+E(f2(f12(x712)),f2(f12(x711))) % 122.98/123.00 [91]~P3(x911)+~P3(x912)+~E(f2(x912),f2(x911))+E(f2(x911),a1)+E(f9(f5(f12(x912),f12(x911)),f4(f3(x912,f2(x912)),f3(x911,f2(x911)))),f5(x912,x911)) % 122.98/123.00 [73]~P1(x733)+~P3(x731)+~E(x732,f12(x731))+E(f3(x732,x733),f3(x731,x733))+E(f2(x731),a1) % 122.98/123.00 [92]~P2(x923)+~P2(x922)+~P2(x924)+~P2(x921)+E(f9(f9(f4(x921,x922),f4(x921,x923)),f9(f4(x924,x922),f4(x924,x923))),f4(f9(x921,x924),f9(x922,x923))) % 122.98/123.00 [85]~P2(x852)+~P2(x851)+E(x851,x852)+~E(f4(x851,x851),f4(x852,x852))+~P4(a10,x852)+~P4(a10,x851) % 122.98/123.00 [78]~P3(x781)+~P3(x782)+E(x781,f12(x782))+E(f2(x782),a1)+P1(f7(x782,x781))+~E(f13(f2(x781)),f2(x782)) % 122.98/123.00 [90]~P3(x902)+~P3(x901)+E(x901,f12(x902))+E(f2(x902),a1)+~E(f13(f2(x901)),f2(x902))+~E(f3(x901,f7(x902,x901)),f3(x902,f7(x902,x901))) % 122.98/123.00 [79]~P2(x792)+~P2(x791)+~P4(x793,x792)+~P4(x791,x793)+P4(x791,x792)+~P2(x793) % 122.98/123.00 [88]~P2(x884)+~P2(x882)+~P2(x883)+~P2(x881)+~P4(x882,x884)+~P4(x881,x883)+P4(f9(x881,x882),f9(x883,x884)) % 122.98/123.00 [89]~P2(x894)+~P2(x892)+~P2(x893)+~P2(x891)+~P4(x892,x894)+~P4(x891,x893)+~P4(a10,x892)+P4(f4(x891,x892),f4(x893,x894)) % 122.98/123.00 %EqnAxiom % 122.98/123.00 [1]E(x11,x11) % 122.98/123.00 [2]E(x22,x21)+~E(x21,x22) % 122.98/123.00 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 122.98/123.00 [4]~E(x41,x42)+E(f12(x41),f12(x42)) % 122.98/123.00 [5]~E(x51,x52)+E(f4(x51,x53),f4(x52,x53)) % 122.98/123.00 [6]~E(x61,x62)+E(f4(x63,x61),f4(x63,x62)) % 122.98/123.00 [7]~E(x71,x72)+E(f9(x71,x73),f9(x72,x73)) % 122.98/123.00 [8]~E(x81,x82)+E(f9(x83,x81),f9(x83,x82)) % 122.98/123.00 [9]~E(x91,x92)+E(f2(x91),f2(x92)) % 122.98/123.00 [10]~E(x101,x102)+E(f5(x101,x103),f5(x102,x103)) % 122.98/123.00 [11]~E(x111,x112)+E(f5(x113,x111),f5(x113,x112)) % 122.98/123.00 [12]~E(x121,x122)+E(f3(x121,x123),f3(x122,x123)) % 122.98/123.00 [13]~E(x131,x132)+E(f3(x133,x131),f3(x133,x132)) % 122.98/123.00 [14]~E(x141,x142)+E(f13(x141),f13(x142)) % 122.98/123.00 [15]~E(x151,x152)+E(f7(x151,x153),f7(x152,x153)) % 122.98/123.00 [16]~E(x161,x162)+E(f7(x163,x161),f7(x163,x162)) % 122.98/123.00 [17]~E(x171,x172)+E(f6(x171),f6(x172)) % 122.98/123.00 [18]~E(x181,x182)+E(f8(x181),f8(x182)) % 122.98/123.00 [19]~P1(x191)+P1(x192)+~E(x191,x192) % 122.98/123.00 [20]~P2(x201)+P2(x202)+~E(x201,x202) % 122.98/123.00 [21]~P3(x211)+P3(x212)+~E(x211,x212) % 122.98/123.00 [22]P4(x222,x223)+~E(x221,x222)+~P4(x221,x223) % 122.98/123.00 [23]P4(x233,x232)+~E(x231,x232)+~P4(x233,x231) % 122.98/123.00 [24]P5(x242,x243)+~E(x241,x242)+~P5(x241,x243) % 122.98/123.00 [25]P5(x253,x252)+~E(x251,x252)+~P5(x253,x251) % 122.98/123.00 % 122.98/123.00 %------------------------------------------- % 122.98/123.01 cnf(95,plain, % 122.98/123.01 (~P3(x951)+E(f2(x951),a1)+E(f13(f2(f12(x951))),f2(x951))), % 122.98/123.01 inference(equality_inference,[],[58])). % 122.98/123.01 cnf(97,plain, % 122.98/123.01 (~P1(x971)+~P3(x972)+E(f3(f12(x972),x971),f3(x972,x971))+E(f2(x972),a1)), % 122.98/123.01 inference(equality_inference,[],[73])). % 122.98/123.01 cnf(98,plain, % 122.98/123.01 (~P3(x981)+~P3(x981)+P2(f5(x981,x981))), % 122.98/123.01 inference(equality_inference,[],[74])). % 122.98/123.01 cnf(100,plain, % 122.98/123.01 (~P3(x1001)+~P3(x1001)+E(f2(x1001),a1)+E(f9(f5(f12(x1001),f12(x1001)),f4(f3(x1001,f2(x1001)),f3(x1001,f2(x1001)))),f5(x1001,x1001))), % 122.98/123.01 inference(equality_inference,[],[91])). % 122.98/123.01 cnf(101,plain, % 122.98/123.01 (E(f2(a11),f13(f2(f12(a11))))), % 122.98/123.01 inference(scs_inference,[],[36,2])). % 122.98/123.01 cnf(102,plain, % 122.98/123.01 (~P5(f2(a11),f2(a11))), % 122.98/123.01 inference(scs_inference,[],[39,28,36,2,80])). % 122.98/123.01 cnf(105,plain, % 122.98/123.01 (P4(a10,a10)), % 122.98/123.01 inference(scs_inference,[],[39,28,27,36,37,2,80,23,63])). % 122.98/123.01 cnf(107,plain, % 122.98/123.01 (E(f3(f12(a11),a1),f3(a11,a1))), % 122.98/123.01 inference(scs_inference,[],[39,28,27,26,38,36,37,2,80,23,63,97])). % 122.98/123.01 cnf(109,plain, % 122.98/123.01 (E(f9(f5(f12(a11),f12(a11)),f4(f3(a11,f2(a11)),f3(a11,f2(a11)))),f5(a11,a11))), % 122.98/123.01 inference(scs_inference,[],[39,28,27,26,38,36,37,2,80,23,63,97,100])). % 122.98/123.01 cnf(111,plain, % 122.98/123.01 (P4(f4(a10,a10),f4(a10,a10))), % 122.98/123.01 inference(scs_inference,[],[39,28,27,26,38,36,37,2,80,23,63,97,100,89])). % 122.98/123.01 cnf(113,plain, % 122.98/123.01 (P4(x1131,f4(f3(a11,f2(a11)),f3(a11,f2(a11))))+~E(a10,x1131)), % 122.98/123.01 inference(scs_inference,[],[39,28,27,26,38,36,37,2,80,23,63,97,100,89,22])). % 122.98/123.01 cnf(115,plain, % 122.98/123.01 (E(x1151,f3(a11,a1))+~E(x1151,f3(f12(a11),a1))), % 122.98/123.01 inference(scs_inference,[],[39,28,27,26,38,36,37,2,80,23,63,97,100,89,22,21,3])). % 122.98/123.01 cnf(124,plain, % 122.98/123.01 (E(f8(a10),a10)), % 122.98/123.01 inference(scs_inference,[],[27,40])). % 122.98/123.01 cnf(127,plain, % 122.98/123.01 (E(f5(a11,a11),f9(f5(f12(a11),f12(a11)),f4(f3(a11,f2(a11)),f3(a11,f2(a11)))))), % 122.98/123.01 inference(scs_inference,[],[109,2])). % 122.98/123.01 cnf(129,plain, % 122.98/123.01 (~P2(f9(f5(f12(a11),f12(a11)),f4(f3(a11,f2(a11)),f3(a11,f2(a11)))))+P2(f5(a11,a11))), % 122.98/123.01 inference(scs_inference,[],[39,105,109,2,23,20])). % 122.98/123.01 cnf(133,plain, % 122.98/123.01 (E(f3(a11,a1),f3(f12(a11),a1))), % 122.98/123.01 inference(scs_inference,[],[107,2])). % 122.98/123.01 cnf(139,plain, % 122.98/123.01 (E(a10,f8(a10))), % 122.98/123.01 inference(scs_inference,[],[124,2])). % 122.98/123.01 cnf(140,plain, % 122.98/123.01 (P2(f8(a10))), % 122.98/123.01 inference(scs_inference,[],[27,124,2,20])). % 122.98/123.01 cnf(141,plain, % 122.98/123.01 (P4(f8(a10),a10)), % 122.98/123.01 inference(scs_inference,[],[105,27,124,2,20,22])). % 122.98/123.01 cnf(142,plain, % 122.98/123.01 (P4(f8(a10),f8(a10))), % 122.98/123.01 inference(scs_inference,[],[105,27,124,2,20,22,63])). % 122.98/123.01 cnf(144,plain, % 122.98/123.01 (P4(f8(a10),f4(f3(a11,f2(a11)),f3(a11,f2(a11))))), % 122.98/123.01 inference(scs_inference,[],[105,27,124,2,20,22,63,113])). % 122.98/123.01 cnf(145,plain, % 122.98/123.01 (P4(f4(a10,a10),x1451)+~E(f4(a10,a10),x1451)), % 122.98/123.01 inference(scs_inference,[],[105,27,111,124,2,20,22,63,113,23])). % 122.98/123.01 cnf(152,plain, % 122.98/123.01 (P4(a10,f8(a10))), % 122.98/123.01 inference(scs_inference,[],[142,124,22])). % 122.98/123.01 cnf(154,plain, % 122.98/123.01 (P4(f4(a10,f8(a10)),f4(f8(a10),a10))), % 122.98/123.01 inference(scs_inference,[],[39,141,142,27,140,124,22,23,89])). % 122.98/123.01 cnf(157,plain, % 122.98/123.01 (P2(f9(f5(f12(a11),f12(a11)),f4(f3(a11,f2(a11)),f3(a11,f2(a11)))))), % 122.98/123.01 inference(scs_inference,[],[39,141,142,28,27,127,140,124,22,23,89,20,74])). % 122.98/123.01 cnf(160,plain, % 122.98/123.01 (P2(f5(a11,a11))), % 122.98/123.01 inference(scs_inference,[],[157,129])). % 122.98/123.01 cnf(167,plain, % 122.98/123.01 (P4(f5(a11,a11),f5(a11,a11))), % 122.98/123.01 inference(scs_inference,[],[160,63])). % 122.98/123.01 cnf(169,plain, % 122.98/123.01 (~P4(f8(a10),f5(a11,a11))), % 122.98/123.01 inference(scs_inference,[],[39,152,27,140,160,63,79])). % 122.98/123.01 cnf(172,plain, % 122.98/123.01 (~E(f5(a11,a11),a10)), % 122.98/123.01 inference(scs_inference,[],[39,152,27,140,101,160,63,79,20,22])). % 122.98/123.01 cnf(173,plain, % 122.98/123.01 (P4(f5(a11,a11),f9(f5(f12(a11),f12(a11)),f4(f3(a11,f2(a11)),f3(a11,f2(a11)))))), % 122.98/123.01 inference(scs_inference,[],[39,152,27,127,140,101,160,63,79,20,22,23])). % 122.98/123.01 cnf(178,plain, % 122.98/123.01 (~E(f5(a11,a11),f8(a10))), % 122.98/123.01 inference(scs_inference,[],[172,124,3])). % 122.98/123.01 cnf(179,plain, % 122.98/123.01 (P4(x1791,f4(f8(a10),a10))+~E(f4(a10,f8(a10)),x1791)), % 122.98/123.01 inference(scs_inference,[],[172,154,124,3,22])). % 122.98/123.01 cnf(184,plain, % 122.98/123.01 (P4(x1841,f4(a10,a10))+~E(f4(a10,a10),x1841)), % 122.98/123.01 inference(scs_inference,[],[111,22])). % 122.98/123.01 cnf(206,plain, % 122.98/123.01 (P1(f13(f2(a11)))), % 122.98/123.01 inference(scs_inference,[],[28,42,43])). % 122.98/123.01 cnf(210,plain, % 122.98/123.01 (~P2(f3(f12(a11),f13(f2(a11))))+P2(f3(a11,f13(f2(a11))))), % 122.98/123.01 inference(scs_inference,[],[28,38,206,97,2,20])). % 122.98/123.01 cnf(245,plain, % 122.98/123.01 (P4(f4(a10,f8(a10)),x2451)+~E(f4(f8(a10),a10),x2451)), % 122.98/123.01 inference(scs_inference,[],[154,23])). % 122.98/123.01 cnf(270,plain, % 122.98/123.01 (~P1(f2(a11))+P1(f13(f2(f12(a11))))), % 122.98/123.01 inference(scs_inference,[],[101,19])). % 122.98/123.01 cnf(277,plain, % 122.98/123.01 (P4(f5(a11,a11),a10)+~P4(f9(f5(f12(a11),f12(a11)),f4(f3(a11,f2(a11)),f3(a11,f2(a11)))),a10)), % 122.98/123.01 inference(scs_inference,[],[144,173,27,124,140,160,157,19,75,79])). % 122.98/123.01 cnf(286,plain, % 122.98/123.01 (P2(f8(f8(a10)))), % 122.98/123.01 inference(scs_inference,[],[139,27,44,20])). % 122.98/123.01 cnf(287,plain, % 122.98/123.01 (P4(f8(f8(a10)),f8(f8(a10)))), % 122.98/123.01 inference(scs_inference,[],[286,63])). % 122.98/123.01 cnf(289,plain, % 122.98/123.01 (P4(x2891,f8(f8(a10)))+~E(f8(f8(a10)),x2891)), % 122.98/123.01 inference(scs_inference,[],[286,63,22])). % 122.98/123.01 cnf(290,plain, % 122.98/123.01 (~E(f8(f8(a10)),f5(a11,a11))+~E(f8(f8(a10)),a10)), % 122.98/123.01 inference(scs_inference,[],[39,286,63,22,23])). % 122.98/123.01 cnf(291,plain, % 122.98/123.01 (~P4(f8(f8(a10)),f5(a11,a11))+~E(f8(f8(a10)),a10)), % 122.98/123.01 inference(scs_inference,[],[39,27,286,160,63,22,23,79])). % 122.98/123.01 cnf(293,plain, % 122.98/123.01 (~E(f8(f8(a10)),a10)+P4(f4(a10,f8(f8(a10))),f4(f8(f8(a10)),f8(f8(a10))))), % 122.98/123.01 inference(scs_inference,[],[39,27,286,160,63,22,23,79,89])). % 122.98/123.01 cnf(297,plain, % 122.98/123.01 (P4(f8(f8(a10)),x2971)+~E(f8(f8(a10)),x2971)), % 122.98/123.01 inference(scs_inference,[],[287,23])). % 122.98/123.01 cnf(316,plain, % 122.98/123.01 (P4(a10,f9(a10,a10))), % 122.98/123.01 inference(scs_inference,[],[27,52,81])). % 122.98/123.01 cnf(317,plain, % 122.98/123.01 (P4(f8(a10),f9(a10,a10))), % 122.98/123.01 inference(scs_inference,[],[316,139,22])). % 122.98/123.01 cnf(318,plain, % 122.98/123.01 (~E(f9(a10,a10),f5(a11,a11))), % 122.98/123.01 inference(scs_inference,[],[39,316,139,22,23])). % 122.98/123.01 cnf(319,plain, % 122.98/123.01 (~P2(f9(a10,a10))+~P4(f9(a10,a10),f5(a11,a11))), % 122.98/123.01 inference(scs_inference,[],[39,27,316,139,160,22,23,79])). % 122.98/123.01 cnf(322,plain, % 122.98/123.01 (~E(f9(a10,a10),f9(f5(f12(a11),f12(a11)),f4(f3(a11,f2(a11)),f3(a11,f2(a11)))))), % 122.98/123.01 inference(scs_inference,[],[318,109,3])). % 122.98/123.01 cnf(447,plain, % 122.98/123.01 (E(f8(f8(f8(a10))),f8(a10))), % 122.98/123.01 inference(scs_inference,[],[27,45,44])). % 122.98/123.01 cnf(449,plain, % 122.98/123.01 (P2(f8(f8(f8(a10))))), % 122.98/123.01 inference(scs_inference,[],[140,447,2,20])). % 122.98/123.01 cnf(450,plain, % 122.98/123.01 (~E(f5(a11,a11),f8(f8(f8(a10))))), % 122.98/123.01 inference(scs_inference,[],[140,178,447,2,20,3])). % 122.98/123.01 cnf(454,plain, % 122.98/123.01 (P4(f8(a10),f8(f8(f8(a10))))), % 122.98/123.01 inference(scs_inference,[],[140,178,447,2,20,3,63,21,22])). % 122.98/123.01 cnf(455,plain, % 122.98/123.01 (P4(f8(f8(f8(a10))),f8(a10))), % 122.98/123.01 inference(scs_inference,[],[140,178,447,2,20,3,63,21,22,23])). % 122.98/123.01 cnf(461,plain, % 122.98/123.01 (P4(a10,f8(f8(f8(a10))))), % 122.98/123.01 inference(scs_inference,[],[454,124,22])). % 122.98/123.01 cnf(463,plain, % 122.98/123.01 (E(f8(f8(f8(a10))),a10)), % 122.98/123.01 inference(scs_inference,[],[455,454,27,124,449,22,23,75])). % 122.98/123.01 cnf(504,plain, % 122.98/123.01 (E(f4(f8(a10),a10),a10)), % 122.98/123.01 inference(scs_inference,[],[27,47,44])). % 122.98/123.01 cnf(505,plain, % 122.98/123.01 (P4(f4(a10,f8(a10)),a10)), % 122.98/123.01 inference(scs_inference,[],[504,245])). % 122.98/123.01 cnf(506,plain, % 122.98/123.01 (E(a10,f4(f8(a10),a10))), % 122.98/123.01 inference(scs_inference,[],[504,245,2])). % 122.98/123.01 cnf(507,plain, % 122.98/123.01 (~E(f5(a11,a11),f4(f8(a10),a10))), % 122.98/123.01 inference(scs_inference,[],[172,504,245,2,3])). % 122.98/123.01 cnf(508,plain, % 122.98/123.01 (P2(f4(f8(a10),a10))), % 122.98/123.01 inference(scs_inference,[],[172,27,504,245,2,3,20])). % 122.98/123.01 cnf(509,plain, % 122.98/123.01 (P4(f4(a10,f8(a10)),f8(a10))), % 122.98/123.01 inference(scs_inference,[],[172,27,139,504,245,2,3,20,23])). % 122.98/123.01 cnf(510,plain, % 122.98/123.01 (P4(f4(f8(a10),a10),f4(f8(a10),a10))), % 122.98/123.01 inference(scs_inference,[],[172,27,139,504,245,2,3,20,23,63])). % 122.98/123.01 cnf(514,plain, % 122.98/123.01 (P4(a10,f4(f8(a10),a10))), % 122.98/123.01 inference(scs_inference,[],[172,27,139,504,245,2,3,20,23,63,113,21,22])). % 122.98/123.01 cnf(522,plain, % 122.98/123.01 (P4(f4(f8(a10),a10),a10)), % 122.98/123.01 inference(scs_inference,[],[510,504,23])). % 122.98/123.01 cnf(523,plain, % 122.98/123.01 (P4(f8(a10),f4(f8(a10),a10))), % 122.98/123.01 inference(scs_inference,[],[510,514,139,504,23,22])). % 122.98/123.01 cnf(524,plain, % 122.98/123.01 (~P4(f4(f8(a10),a10),f5(a11,a11))), % 122.98/123.01 inference(scs_inference,[],[39,510,514,27,139,160,508,504,23,22,79])). % 122.98/123.01 cnf(526,plain, % 122.98/123.01 (P4(f4(a10,f4(f8(a10),a10)),f4(f4(f8(a10),a10),f4(f8(a10),a10)))), % 122.98/123.01 inference(scs_inference,[],[39,510,514,27,139,160,508,504,23,22,79,89])). % 122.98/123.01 cnf(544,plain, % 122.98/123.01 (P4(f4(a10,f4(f8(a10),a10)),f4(f4(f8(a10),a10),a10))), % 122.98/123.01 inference(scs_inference,[],[514,522,27,508,89])). % 122.98/123.01 cnf(546,plain, % 122.98/123.01 (P4(x5461,f8(a10))+~E(f4(a10,f8(a10)),x5461)), % 122.98/123.01 inference(scs_inference,[],[514,522,509,27,508,89,22])). % 122.98/123.01 cnf(552,plain, % 122.98/123.01 (P4(x5521,f4(f4(f8(a10),a10),f4(f8(a10),a10)))+~E(f4(a10,f4(f8(a10),a10)),x5521)), % 122.98/123.01 inference(scs_inference,[],[526,22])). % 122.98/123.01 cnf(560,plain, % 122.98/123.01 (P4(f4(a10,f4(f8(a10),a10)),x5601)+~E(f4(f4(f8(a10),a10),a10),x5601)), % 122.98/123.01 inference(scs_inference,[],[544,23])). % 122.98/123.01 cnf(579,plain, % 122.98/123.01 (E(f4(a10,f8(a10)),a10)), % 122.98/123.01 inference(scs_inference,[],[27,48,44])). % 122.98/123.01 cnf(580,plain, % 122.98/123.01 (E(a10,f4(a10,f8(a10)))), % 122.98/123.01 inference(scs_inference,[],[579,2])). % 122.98/123.01 cnf(581,plain, % 122.98/123.01 (~E(f5(a11,a11),f4(a10,f8(a10)))), % 122.98/123.01 inference(scs_inference,[],[172,579,2,3])). % 122.98/123.01 cnf(582,plain, % 122.98/123.01 (P2(f4(a10,f8(a10)))), % 122.98/123.01 inference(scs_inference,[],[172,27,579,2,3,20])). % 122.98/123.01 cnf(583,plain, % 122.98/123.01 (P4(f4(a10,f8(a10)),f4(a10,f8(a10)))), % 122.98/123.01 inference(scs_inference,[],[172,27,579,2,3,20,63])). % 122.98/123.01 cnf(587,plain, % 122.98/123.01 (P4(a10,f4(a10,f8(a10)))), % 122.98/123.01 inference(scs_inference,[],[172,27,579,2,3,20,63,113,21,22])). % 122.98/123.01 cnf(596,plain, % 122.98/123.01 (P4(f8(a10),f4(a10,f8(a10)))), % 122.98/123.01 inference(scs_inference,[],[587,139,22])). % 122.98/123.01 cnf(597,plain, % 122.98/123.01 (E(f8(a10),f4(a10,f8(a10)))), % 122.98/123.01 inference(scs_inference,[],[509,587,139,140,582,22,75])). % 122.98/123.01 cnf(599,plain, % 122.98/123.01 (~P4(f4(a10,f8(a10)),f5(a11,a11))), % 122.98/123.01 inference(scs_inference,[],[39,509,587,27,139,140,160,582,22,75,79])). % 122.98/123.01 cnf(601,plain, % 122.98/123.01 (P4(f4(a10,f4(a10,f8(a10))),f4(f4(a10,f8(a10)),a10))), % 122.98/123.01 inference(scs_inference,[],[39,505,509,587,27,139,140,160,582,22,75,79,89])). % 122.98/123.01 cnf(620,plain, % 122.98/123.01 (P4(f4(a10,f8(a10)),f8(f8(f8(a10))))), % 122.98/123.01 inference(scs_inference,[],[454,597,22])). % 122.98/123.01 cnf(621,plain, % 122.98/123.01 (P4(f4(a10,f4(a10,f8(a10))),x6211)+~E(f4(f4(a10,f8(a10)),a10),x6211)), % 122.98/123.01 inference(scs_inference,[],[454,597,601,22,23])). % 122.98/123.01 cnf(626,plain, % 122.98/123.01 (P4(x6261,f4(f4(a10,f8(a10)),a10))+~E(f4(a10,f4(a10,f8(a10))),x6261)), % 122.98/123.01 inference(scs_inference,[],[601,22])). % 122.98/123.01 cnf(652,plain, % 122.98/123.01 (E(f9(f8(a10),a10),f8(a10))), % 122.98/123.01 inference(scs_inference,[],[27,50,44])). % 122.98/123.01 cnf(654,plain, % 122.98/123.01 (~E(f5(a11,a11),f9(f8(a10),a10))), % 122.98/123.01 inference(scs_inference,[],[652,178,2,3])). % 122.98/123.01 cnf(655,plain, % 122.98/123.01 (P2(f9(f8(a10),a10))), % 122.98/123.01 inference(scs_inference,[],[140,652,178,2,3,20])). % 122.98/123.01 cnf(659,plain, % 122.98/123.01 (P4(f9(f8(a10),a10),f8(a10))), % 122.98/123.01 inference(scs_inference,[],[140,652,178,2,3,20,63,21,23])). % 122.98/123.01 cnf(660,plain, % 122.98/123.01 (P4(f8(a10),f9(f8(a10),a10))), % 122.98/123.01 inference(scs_inference,[],[140,652,178,2,3,20,63,21,23,22])). % 122.98/123.01 cnf(666,plain, % 122.98/123.01 (P4(f9(f8(a10),a10),f4(a10,f8(a10)))), % 122.98/123.01 inference(scs_inference,[],[659,597,23])). % 122.98/123.01 cnf(667,plain, % 122.98/123.01 (P4(f4(a10,f8(a10)),f9(f8(a10),a10))), % 122.98/123.01 inference(scs_inference,[],[659,660,597,23,22])). % 122.98/123.01 cnf(668,plain, % 122.98/123.01 (E(f4(a10,f8(a10)),f9(f8(a10),a10))), % 122.98/123.01 inference(scs_inference,[],[659,660,597,582,655,23,22,75])). % 122.98/123.01 cnf(672,plain, % 122.98/123.01 (P4(f9(f8(a10),a10),f4(f8(a10),a10))), % 122.98/123.01 inference(scs_inference,[],[141,659,660,27,597,140,582,655,23,22,75,79,179])). % 122.98/123.01 cnf(687,plain, % 122.98/123.01 (~P4(f9(f8(a10),a10),f5(a11,a11))), % 122.98/123.01 inference(scs_inference,[],[620,599,667,668,160,582,655,22,23,79])). % 122.98/123.01 cnf(709,plain, % 122.98/123.01 (E(f4(f8(a10),a10),f9(f8(a10),a10))+~E(f8(a10),f4(f8(a10),a10))), % 122.98/123.01 inference(scs_inference,[],[660,672,508,655,75,22])). % 122.98/123.01 cnf(723,plain, % 122.98/123.01 (E(f9(a10,f8(a10)),f8(a10))), % 122.98/123.01 inference(scs_inference,[],[27,51,44])). % 122.98/123.01 cnf(726,plain, % 122.98/123.01 (P2(f9(a10,f8(a10)))), % 122.98/123.01 inference(scs_inference,[],[140,723,178,2,3,20])). % 122.98/123.01 cnf(727,plain, % 122.98/123.01 (P4(f9(a10,f8(a10)),f9(a10,f8(a10)))), % 122.98/123.01 inference(scs_inference,[],[140,723,178,2,3,20,63])). % 122.98/123.01 cnf(730,plain, % 122.98/123.01 (P4(f9(a10,f8(a10)),f8(a10))), % 122.98/123.01 inference(scs_inference,[],[140,723,178,2,3,20,63,21,23])). % 122.98/123.01 cnf(731,plain, % 122.98/123.01 (P4(f8(a10),f9(a10,f8(a10)))), % 122.98/123.01 inference(scs_inference,[],[140,723,178,2,3,20,63,21,23,22])). % 122.98/123.01 cnf(737,plain, % 122.98/123.01 (P4(f9(a10,f8(a10)),f4(a10,f8(a10)))), % 122.98/123.01 inference(scs_inference,[],[730,597,23])). % 122.98/123.01 cnf(738,plain, % 122.98/123.01 (P4(f4(a10,f8(a10)),f9(a10,f8(a10)))), % 122.98/123.01 inference(scs_inference,[],[730,731,597,23,22])). % 122.98/123.01 cnf(739,plain, % 122.98/123.01 (E(f4(a10,f8(a10)),f9(a10,f8(a10)))), % 122.98/123.01 inference(scs_inference,[],[730,731,597,582,726,23,22,75])). % 122.98/123.01 cnf(743,plain, % 122.98/123.01 (P4(f9(a10,f8(a10)),f4(f8(a10),a10))), % 122.98/123.01 inference(scs_inference,[],[141,730,731,597,27,140,582,726,23,22,75,79,179])). % 122.98/123.01 cnf(758,plain, % 122.98/123.01 (P4(f9(a10,f8(a10)),f9(f8(a10),a10))), % 122.98/123.01 inference(scs_inference,[],[737,668,23])). % 122.98/123.01 cnf(759,plain, % 122.98/123.01 (P4(f9(f8(a10),a10),f9(a10,f8(a10)))), % 122.98/123.01 inference(scs_inference,[],[737,738,668,23,22])). % 122.98/123.01 cnf(762,plain, % 122.98/123.01 (~P4(f9(a10,f8(a10)),f5(a11,a11))), % 122.98/123.01 inference(scs_inference,[],[737,738,599,668,160,582,655,726,23,22,75,79])). % 122.98/123.01 cnf(797,plain, % 122.98/123.01 (E(f4(f8(a10),a10),f9(a10,f8(a10)))+~E(f9(f8(a10),a10),f4(f8(a10),a10))), % 122.98/123.01 inference(scs_inference,[],[759,743,508,726,75,22])). % 122.98/123.01 cnf(810,plain, % 122.98/123.01 (P4(a10,f4(f8(a10),f8(a10)))), % 122.98/123.01 inference(scs_inference,[],[27,67,44])). % 122.98/123.01 cnf(811,plain, % 122.98/123.01 (~E(f4(f8(a10),f8(a10)),f5(a11,a11))), % 122.98/123.01 inference(scs_inference,[],[39,810,23])). % 122.98/123.01 cnf(813,plain, % 122.98/123.01 (~P2(f4(f8(a10),f8(a10)))+~P4(f4(f8(a10),f8(a10)),f5(a11,a11))), % 122.98/123.01 inference(scs_inference,[],[39,27,139,160,810,23,22,79])). % 122.98/123.01 cnf(1000,plain, % 122.98/123.01 (~E(f4(f8(a10),f4(f8(a10),a10)),f5(a11,a11))), % 122.98/123.01 inference(scs_inference,[],[523,152,599,27,140,508,89,23])). % 122.98/123.01 cnf(1001,plain, % 122.98/123.01 (P4(f9(f8(a10),a10),f4(f8(a10),f4(f8(a10),a10)))), % 122.98/123.01 inference(scs_inference,[],[523,152,599,668,27,140,508,89,23,22])). % 122.98/123.01 cnf(1038,plain, % 122.98/123.01 (E(f12(f4(f8(f8(f8(a10))),x10381)),f12(f4(a10,x10381)))), % 122.98/123.01 inference(scs_inference,[],[463,4,5])). % 122.98/123.01 cnf(1111,plain, % 122.98/123.01 (E(f9(f8(a10),f8(f8(a10))),a10)), % 122.98/123.01 inference(scs_inference,[],[27,54,44])). % 122.98/123.01 cnf(1112,plain, % 122.98/123.01 (E(a10,f9(f8(a10),f8(f8(a10))))), % 122.98/123.01 inference(scs_inference,[],[1111,2])). % 122.98/123.01 cnf(1113,plain, % 122.98/123.01 (~E(f5(a11,a11),f9(f8(a10),f8(f8(a10))))), % 122.98/123.01 inference(scs_inference,[],[172,1111,2,3])). % 122.98/123.01 cnf(1114,plain, % 122.98/123.01 (P2(f9(f8(a10),f8(f8(a10))))), % 122.98/123.01 inference(scs_inference,[],[172,27,1111,2,3,20])). % 122.98/123.01 cnf(1119,plain, % 122.98/123.01 (P4(a10,f9(f8(a10),f8(f8(a10))))), % 122.98/123.01 inference(scs_inference,[],[172,27,1111,2,3,20,63,113,19,22])). % 122.98/123.01 cnf(1127,plain, % 122.98/123.01 (P4(f8(a10),f9(f8(a10),f8(f8(a10))))), % 122.98/123.01 inference(scs_inference,[],[1119,139,22])). % 122.98/123.01 cnf(1139,plain, % 122.98/123.01 (P4(f4(a10,f8(a10)),f9(f8(a10),f8(f8(a10))))), % 122.98/123.01 inference(scs_inference,[],[1127,597,22])). % 122.98/123.01 cnf(1157,plain, % 122.98/123.01 (~E(f4(a10,f8(a10)),f9(f8(a10),f8(f8(a10))))+E(f9(f8(a10),f8(f8(a10))),f8(a10))), % 122.98/123.01 inference(scs_inference,[],[1127,1139,739,140,1114,22,75,546])). % 122.98/123.01 cnf(1179,plain, % 122.98/123.01 (E(f9(f8(f8(a10)),f8(a10)),a10)), % 122.98/123.01 inference(scs_inference,[],[27,55,44])). % 122.98/123.01 cnf(1180,plain, % 122.98/123.01 (E(a10,f9(f8(f8(a10)),f8(a10)))), % 122.98/123.01 inference(scs_inference,[],[1179,2])). % 122.98/123.01 cnf(1181,plain, % 122.98/123.01 (~E(f5(a11,a11),f9(f8(f8(a10)),f8(a10)))), % 122.98/123.01 inference(scs_inference,[],[172,1179,2,3])). % 122.98/123.01 cnf(1182,plain, % 122.98/123.01 (P2(f9(f8(f8(a10)),f8(a10)))), % 122.98/123.01 inference(scs_inference,[],[172,27,1179,2,3,20])). % 122.98/123.01 cnf(1183,plain, % 122.98/123.01 (P4(f9(f8(f8(a10)),f8(a10)),f9(f8(f8(a10)),f8(a10)))), % 122.98/123.01 inference(scs_inference,[],[172,27,1179,2,3,20,63])). % 122.98/123.01 cnf(1187,plain, % 122.98/123.01 (P4(a10,f9(f8(f8(a10)),f8(a10)))), % 122.98/123.01 inference(scs_inference,[],[172,27,1179,2,3,20,63,113,19,22])). % 122.98/123.01 cnf(1195,plain, % 122.98/123.01 (P4(f8(a10),f9(f8(f8(a10)),f8(a10)))), % 122.98/123.01 inference(scs_inference,[],[1187,139,22])). % 122.98/123.01 cnf(1206,plain, % 122.98/123.01 (P4(f4(a10,f8(a10)),f9(f8(f8(a10)),f8(a10)))), % 122.98/123.01 inference(scs_inference,[],[1195,597,22])). % 122.98/123.01 cnf(1219,plain, % 122.98/123.01 (~E(f4(a10,f8(a10)),f9(f8(f8(a10)),f8(a10)))+E(f9(f8(f8(a10)),f8(a10)),f8(a10))), % 122.98/123.01 inference(scs_inference,[],[1195,1206,739,140,1182,22,75,546])). % 122.98/123.01 cnf(1290,plain, % 122.98/123.01 (E(f3(f12(a11),f13(f2(f12(a11)))),f3(a11,f13(f2(f12(a11)))))+~P1(f2(a11))), % 122.98/123.01 inference(scs_inference,[],[38,28,270,97])). % 122.98/123.01 cnf(1299,plain, % 122.98/123.01 (P4(f4(a10,f4(a10,f8(a10))),f4(f4(a10,f8(a10)),f4(a10,f8(a10))))), % 122.98/123.01 inference(scs_inference,[],[583,587,27,582,89])). % 122.98/123.01 cnf(1301,plain, % 122.98/123.01 (P4(f4(a10,f4(a10,f8(a10))),x13011)+~E(f4(f4(a10,f8(a10)),f4(a10,f8(a10))),x13011)), % 122.98/123.01 inference(scs_inference,[],[583,587,27,582,89,23])). % 122.98/123.01 cnf(1306,plain, % 122.98/123.01 (P4(x13061,f4(f4(a10,f8(a10)),f4(a10,f8(a10))))+~E(f4(a10,f4(a10,f8(a10))),x13061)), % 122.98/123.01 inference(scs_inference,[],[1299,22])). % 122.98/123.01 cnf(1312,plain, % 122.98/123.01 (~P2(f9(a10,a10))+~E(f4(f8(a10),f9(a10,a10)),f5(a11,a11))), % 122.98/123.01 inference(scs_inference,[],[317,152,599,27,140,89,23])). % 122.98/123.01 cnf(1440,plain, % 122.98/123.01 (~E(f4(f8(a10),f9(f8(a10),f8(f8(a10)))),f5(a11,a11))), % 122.98/123.01 inference(scs_inference,[],[152,1127,599,739,27,140,1114,89,22,23])). % 122.98/123.01 cnf(1815,plain, % 122.98/123.01 (~E(f4(f8(a10),f8(f8(f8(a10)))),f5(a11,a11))), % 122.98/123.01 inference(scs_inference,[],[461,454,152,599,27,506,140,449,22,89,23])). % 122.98/123.01 cnf(1822,plain, % 122.98/123.01 (E(f8(a10),f4(f8(a10),a10))), % 122.98/123.02 inference(scs_inference,[],[152,523,506,140,508,22,75,2])). % 122.98/123.02 cnf(1828,plain, % 122.98/123.02 (E(f4(f8(a10),a10),f9(f8(a10),a10))), % 122.98/123.02 inference(scs_inference,[],[1822,709])). % 122.98/123.02 cnf(1829,plain, % 122.98/123.02 (P4(f4(f8(a10),a10),f9(f8(f8(a10)),f8(a10)))), % 122.98/123.02 inference(scs_inference,[],[1187,506,22])). % 122.98/123.02 cnf(1834,plain, % 122.98/123.02 (P4(f4(f8(a10),a10),f4(a10,f8(a10)))), % 122.98/123.02 inference(scs_inference,[],[587,1828,506,2,22])). % 122.98/123.02 cnf(1835,plain, % 122.98/123.02 (E(f4(f8(a10),a10),f4(a10,f8(a10)))), % 122.98/123.02 inference(scs_inference,[],[587,154,1828,506,508,582,2,22,75])). % 122.98/123.02 cnf(1837,plain, % 122.98/123.02 (E(f4(f8(a10),a10),f9(a10,f8(a10)))), % 122.98/123.02 inference(scs_inference,[],[587,154,1828,506,508,582,2,22,75,797])). % 122.98/123.02 cnf(1842,plain, % 122.98/123.02 (E(f4(a10,f8(a10)),f4(f8(a10),a10))), % 122.98/123.02 inference(scs_inference,[],[1835,2])). % 122.98/123.02 cnf(1848,plain, % 122.98/123.02 (E(f9(a10,f8(a10)),f4(f8(a10),a10))), % 122.98/123.02 inference(scs_inference,[],[1837,2])). % 122.98/123.02 cnf(1994,plain, % 122.98/123.02 (P4(f4(f8(a10),a10),f9(f8(a10),a10))), % 122.98/123.02 inference(scs_inference,[],[758,1848,22])). % 122.98/123.02 cnf(1995,plain, % 122.98/123.02 (P4(f4(a10,f4(a10,f8(a10))),f4(f4(a10,f8(a10)),f9(a10,f8(a10))))), % 122.98/123.02 inference(scs_inference,[],[758,738,587,27,1848,582,726,22,89])). % 122.98/123.02 cnf(1997,plain, % 122.98/123.02 (P4(f4(a10,f4(a10,f8(a10))),x19971)+~E(f4(f4(a10,f8(a10)),f9(a10,f8(a10))),x19971)), % 122.98/123.02 inference(scs_inference,[],[758,738,587,27,1848,582,726,22,89,23])). % 122.98/123.02 cnf(2003,plain, % 122.98/123.02 (P4(f4(f8(a10),a10),f9(a10,f8(a10)))), % 122.98/123.02 inference(scs_inference,[],[727,1848,22])). % 122.98/123.02 cnf(2006,plain, % 122.98/123.02 (~E(f4(f8(a10),f9(a10,f8(a10))),f5(a11,a11))), % 122.98/123.02 inference(scs_inference,[],[731,727,152,599,27,1848,140,726,22,89,23])). % 122.98/123.02 cnf(2060,plain, % 122.98/123.02 (P4(x20601,f4(f4(a10,f8(a10)),f9(a10,f8(a10))))+~E(f4(a10,f4(a10,f8(a10))),x20601)), % 122.98/123.02 inference(scs_inference,[],[1995,22])). % 122.98/123.02 cnf(2169,plain, % 122.98/123.02 (P4(f4(a10,f4(f8(a10),a10)),f4(f4(f8(a10),a10),f9(f8(f8(a10)),f8(a10))))), % 122.98/123.02 inference(scs_inference,[],[514,1829,27,508,1182,89])). % 122.98/123.02 cnf(2176,plain, % 122.98/123.02 (P4(x21761,f4(f4(f8(a10),a10),f9(f8(f8(a10)),f8(a10))))+~E(f4(a10,f4(f8(a10),a10)),x21761)), % 122.98/123.02 inference(scs_inference,[],[2169,22])). % 122.98/123.02 cnf(2299,plain, % 122.98/123.02 (P4(f9(f8(f8(a10)),f8(a10)),f4(f8(a10),a10))), % 122.98/123.02 inference(scs_inference,[],[587,1206,1180,582,1182,22,75,2,179])). % 122.98/123.02 cnf(2301,plain, % 122.98/123.02 (E(f9(f8(f8(a10)),f8(a10)),f8(a10))), % 122.98/123.02 inference(scs_inference,[],[587,1206,1180,582,1182,22,75,2,179,19,1219])). % 122.98/123.02 cnf(2307,plain, % 122.98/123.02 (E(f4(f8(a10),a10),f9(f8(f8(a10)),f8(a10)))), % 122.98/123.02 inference(scs_inference,[],[1119,1829,2299,2301,1180,508,1182,2,22,75])). % 122.98/123.02 cnf(2490,plain, % 122.98/123.02 (P4(f9(f8(f8(a10)),f8(a10)),f9(f8(a10),a10))), % 122.98/123.02 inference(scs_inference,[],[1994,2307,22])). % 122.98/123.02 cnf(2497,plain, % 122.98/123.02 (P4(f9(f8(f8(a10)),f8(a10)),f9(a10,f8(a10)))), % 122.98/123.02 inference(scs_inference,[],[2003,2307,22])). % 122.98/123.02 cnf(2506,plain, % 122.98/123.02 (P4(f9(f8(a10),f8(f8(a10))),f4(f8(a10),a10))), % 122.98/123.02 inference(scs_inference,[],[514,1112,22])). % 122.98/123.02 cnf(2536,plain, % 122.98/123.02 (E(f4(a10,f8(a10)),f9(f8(a10),f8(f8(a10))))), % 122.98/123.02 inference(scs_inference,[],[1139,587,1112,582,1114,22,75,2])). % 122.98/123.02 cnf(2544,plain, % 122.98/123.02 (E(f9(f8(a10),f8(f8(a10))),f8(a10))), % 122.98/123.02 inference(scs_inference,[],[2536,1157])). % 122.98/123.02 cnf(2546,plain, % 122.98/123.02 (E(f8(a10),f9(f8(a10),f8(f8(a10))))), % 122.98/123.02 inference(scs_inference,[],[2544,2])). % 122.98/123.02 cnf(2777,plain, % 122.98/123.02 (P1(f13(a1))), % 122.98/123.02 inference(scs_inference,[],[157,26,52,42])). % 122.98/123.02 cnf(2783,plain, % 122.98/123.02 (~E(f13(a1),a1)), % 122.98/123.02 inference(scs_inference,[],[157,26,52,42,44,56,41])). % 122.98/123.02 cnf(2801,plain, % 122.98/123.02 (E(f9(f8(f9(f8(a10),f8(f8(a10)))),f9(f8(a10),f8(f8(a10)))),a10)), % 122.98/123.02 inference(scs_inference,[],[1842,157,1114,26,52,42,44,56,41,45,50,51,67,47,4,9,17,18,54,55])). % 122.98/123.02 cnf(2803,plain, % 122.98/123.02 (E(f4(f4(a10,f8(a10)),x28031),f4(f4(f8(a10),a10),x28031))), % 122.98/123.02 inference(scs_inference,[],[1842,157,1114,26,52,42,44,56,41,45,50,51,67,47,4,9,17,18,54,55,5])). % 122.98/123.02 cnf(2804,plain, % 122.98/123.02 (E(f4(x28041,f4(a10,f8(a10))),f4(x28041,f4(f8(a10),a10)))), % 122.98/123.02 inference(scs_inference,[],[1842,157,1114,26,52,42,44,56,41,45,50,51,67,47,4,9,17,18,54,55,5,6])). % 122.98/123.02 cnf(2805,plain, % 122.98/123.02 (E(f9(f4(a10,f8(a10)),x28051),f9(f4(f8(a10),a10),x28051))), % 122.98/123.02 inference(scs_inference,[],[1842,157,1114,26,52,42,44,56,41,45,50,51,67,47,4,9,17,18,54,55,5,6,7])). % 122.98/123.02 cnf(2813,plain, % 122.98/123.02 (E(f3(f12(a11),f13(a1)),f3(a11,f13(a1)))), % 122.98/123.02 inference(scs_inference,[],[1842,157,1114,26,52,42,44,56,41,45,50,51,67,47,4,9,17,18,54,55,5,6,7,8,10,11,12,13,15,16,62])). % 122.98/123.02 cnf(2818,plain, % 122.98/123.02 (P1(f2(f12(a11)))), % 122.98/123.02 inference(scs_inference,[],[1842,32,157,1114,26,52,42,44,56,41,45,50,51,67,47,4,9,17,18,54,55,5,6,7,8,10,11,12,13,15,16,62,2060,48,43])). % 122.98/123.02 cnf(2821,plain, % 122.98/123.02 (~E(f5(a11,a11),f4(f8(a10),f8(a10)))), % 122.98/123.02 inference(scs_inference,[],[811,1842,32,157,1114,26,52,42,44,56,41,45,50,51,67,47,4,9,17,18,54,55,5,6,7,8,10,11,12,13,15,16,62,2060,48,43,14,2])). % 122.98/123.02 cnf(2822,plain, % 122.98/123.02 (P1(f6(f13(a1)))), % 122.98/123.02 inference(scs_inference,[],[811,1842,32,157,1114,26,52,42,44,56,41,45,50,51,67,47,4,9,17,18,54,55,5,6,7,8,10,11,12,13,15,16,62,2060,48,43,14,2,46])). % 122.98/123.02 cnf(2824,plain, % 122.98/123.02 (E(f13(f6(f13(a1))),f13(a1))), % 122.98/123.02 inference(scs_inference,[],[811,1842,32,157,1114,26,52,42,44,56,41,45,50,51,67,47,4,9,17,18,54,55,5,6,7,8,10,11,12,13,15,16,62,2060,48,43,14,2,46,49])). % 122.98/123.02 cnf(2834,plain, % 122.98/123.02 (P2(f5(f12(a11),f12(a11)))), % 122.98/123.02 inference(scs_inference,[],[811,1842,32,157,1114,726,26,52,42,44,56,41,45,50,51,67,47,4,9,17,18,54,55,5,6,7,8,10,11,12,13,15,16,62,2060,48,43,14,2,46,49,72,76,77,64,98])). % 122.98/123.02 cnf(2836,plain, % 122.98/123.02 (P2(f3(f12(a11),a1))), % 122.98/123.02 inference(scs_inference,[],[811,1842,32,157,1114,726,26,52,42,44,56,41,45,50,51,67,47,4,9,17,18,54,55,5,6,7,8,10,11,12,13,15,16,62,2060,48,43,14,2,46,49,72,76,77,64,98,66])). % 122.98/123.02 cnf(2840,plain, % 122.98/123.02 (~P5(f13(f2(f12(a11))),f2(a11))), % 122.98/123.02 inference(scs_inference,[],[811,1842,102,32,157,36,1114,726,26,52,42,44,56,41,45,50,51,67,47,4,9,17,18,54,55,5,6,7,8,10,11,12,13,15,16,62,2060,48,43,14,2,46,49,72,76,77,64,98,66,65,24])). % 122.98/123.02 cnf(2843,plain, % 122.98/123.02 (P2(f3(a11,a1))), % 122.98/123.02 inference(scs_inference,[],[811,1038,1842,102,32,157,36,1114,726,26,107,52,42,44,56,41,45,50,51,67,47,4,9,17,18,54,55,5,6,7,8,10,11,12,13,15,16,62,2060,48,43,14,2,46,49,72,76,77,64,98,66,65,24,3,20])). % 122.98/123.02 cnf(2844,plain, % 122.98/123.02 (~P5(f2(a11),f13(f2(f12(a11))))), % 122.98/123.02 inference(scs_inference,[],[811,1038,1842,102,32,157,36,1114,726,26,107,52,42,44,56,41,45,50,51,67,47,4,9,17,18,54,55,5,6,7,8,10,11,12,13,15,16,62,2060,48,43,14,2,46,49,72,76,77,64,98,66,65,24,3,20,25])). % 122.98/123.02 cnf(2845,plain, % 122.98/123.02 (~P4(a10,f9(f5(f12(a11),f12(a11)),f4(f3(a11,f2(a11)),f3(a11,f2(a11)))))), % 122.98/123.02 inference(scs_inference,[],[39,811,1038,1842,102,32,157,36,1114,726,26,109,107,52,42,44,56,41,45,50,51,67,47,4,9,17,18,54,55,5,6,7,8,10,11,12,13,15,16,62,2060,48,43,14,2,46,49,72,76,77,64,98,66,65,24,3,20,25,23])). % 122.98/123.02 cnf(2846,plain, % 122.98/123.02 (~E(f13(f13(a1)),f13(a1))), % 122.98/123.02 inference(scs_inference,[],[39,811,1038,1842,102,32,157,36,1114,726,26,109,107,52,42,44,56,41,45,50,51,67,47,4,9,17,18,54,55,5,6,7,8,10,11,12,13,15,16,62,2060,48,43,14,2,46,49,72,76,77,64,98,66,65,24,3,20,25,23,57])). % 122.98/123.02 cnf(2856,plain, % 122.98/123.02 (P4(f9(f5(f12(a11),f12(a11)),f4(f3(a11,f2(a11)),f3(a11,f2(a11)))),a10)), % 122.98/123.02 inference(scs_inference,[],[39,811,1038,1842,102,32,157,36,1114,726,26,109,160,107,27,52,42,44,56,41,45,50,51,67,47,4,9,17,18,54,55,5,6,7,8,10,11,12,13,15,16,62,2060,48,43,14,2,46,49,72,76,77,64,98,66,65,24,3,20,25,23,57,83,84,86,87,63])). % 122.98/123.02 cnf(2862,plain, % 122.98/123.02 (P4(f9(f9(f8(a10),a10),f9(f8(a10),a10)),f9(f4(a10,f8(a10)),f4(a10,f8(a10))))), % 122.98/123.02 inference(scs_inference,[],[39,811,1038,666,1842,102,461,32,157,36,1114,726,26,109,160,107,449,582,655,27,52,42,44,56,41,45,50,51,67,47,4,9,17,18,54,55,5,6,7,8,10,11,12,13,15,16,62,2060,48,43,14,2,46,49,72,76,77,64,98,66,65,24,3,20,25,23,57,83,84,86,87,63,82,92,88])). % 122.98/123.02 cnf(2866,plain, % 122.98/123.02 (P4(f9(f5(f12(a11),f12(a11)),f4(f3(a11,f2(a11)),f3(a11,f2(a11)))),f5(a11,a11))), % 122.98/123.02 inference(scs_inference,[],[39,811,1038,666,1842,102,167,461,32,157,36,1114,726,127,26,109,160,107,449,582,655,27,52,42,44,56,41,45,50,51,67,47,4,9,17,18,54,55,5,6,7,8,10,11,12,13,15,16,62,2060,48,43,14,2,46,49,72,76,77,64,98,66,65,24,3,20,25,23,57,83,84,86,87,63,82,92,88,95,22])). % 122.98/123.02 cnf(2869,plain, % 122.98/123.02 (P4(f4(f8(a10),f8(a10)),f4(f4(a10,f8(a10)),f4(a10,f8(a10))))), % 122.98/123.02 inference(scs_inference,[],[39,811,1038,666,596,1842,102,167,1119,461,32,157,36,1114,726,127,26,109,160,107,449,582,140,655,152,27,52,42,44,56,41,45,50,51,67,47,4,9,17,18,54,55,5,6,7,8,10,11,12,13,15,16,62,2060,48,43,14,2,46,49,72,76,77,64,98,66,65,24,3,20,25,23,57,83,84,86,87,63,82,92,88,95,22,81,89])). % 122.98/123.02 cnf(2873,plain, % 122.98/123.02 (P4(f5(a11,a11),a10)), % 122.98/123.02 inference(scs_inference,[],[2856,277])). % 122.98/123.02 cnf(2875,plain, % 122.98/123.02 (E(f9(f3(a11,a1),f8(f3(a11,a1))),a10)), % 122.98/123.02 inference(scs_inference,[],[2843,54])). % 122.98/123.02 cnf(2879,plain, % 122.98/123.02 (E(f9(a10,f3(a11,a1)),f3(a11,a1))), % 122.98/123.02 inference(scs_inference,[],[2843,54,45,51])). % 122.98/123.02 cnf(2881,plain, % 122.98/123.02 (E(f4(f3(a11,a1),a10),a10)), % 122.98/123.02 inference(scs_inference,[],[2843,54,45,51,47])). % 122.98/123.02 cnf(2883,plain, % 122.98/123.02 (P4(a10,f4(f3(a11,a1),f3(a11,a1)))), % 122.98/123.02 inference(scs_inference,[],[2843,54,45,51,47,67])). % 122.98/123.02 cnf(2885,plain, % 122.98/123.02 (E(f9(f3(a11,a1),a10),f3(a11,a1))), % 122.98/123.02 inference(scs_inference,[],[2843,54,45,51,47,67,50])). % 122.98/123.02 cnf(2887,plain, % 122.98/123.02 (E(f9(f8(f3(a11,a1)),f3(a11,a1)),a10)), % 122.98/123.02 inference(scs_inference,[],[2843,54,45,51,47,67,50,55])). % 122.98/123.02 cnf(2889,plain, % 122.98/123.02 (~E(f13(f13(a1)),a1)), % 122.98/123.02 inference(scs_inference,[],[2843,2777,54,45,51,47,67,50,55,41])). % 122.98/123.02 cnf(2891,plain, % 122.98/123.02 (P1(f13(f13(a1)))), % 122.98/123.02 inference(scs_inference,[],[2843,2777,54,45,51,47,67,50,55,41,42])). % 122.98/123.02 cnf(2896,plain, % 122.98/123.02 (E(f3(f12(a11),f2(f12(a11))),f3(a11,f2(f12(a11))))), % 122.98/123.02 inference(scs_inference,[],[2843,2777,2818,2813,54,45,51,47,67,50,55,41,42,10,13,4,62])). % 122.98/123.02 cnf(2900,plain, % 122.98/123.02 (P4(f3(a11,a1),f3(a11,a1))), % 122.98/123.02 inference(scs_inference,[],[2843,2777,2818,2813,54,45,51,47,67,50,55,41,42,10,13,4,62,15,9,52])). % 122.98/123.02 cnf(2902,plain, % 122.98/123.02 (P5(f2(f12(a11)),f13(f2(f12(a11))))), % 122.98/123.02 inference(scs_inference,[],[2843,2777,2818,2813,54,45,51,47,67,50,55,41,42,10,13,4,62,15,9,52,56])). % 122.98/123.02 cnf(2905,plain, % 122.98/123.02 (P2(f8(f3(a11,a1)))), % 122.98/123.02 inference(scs_inference,[],[2843,2777,2818,2813,54,45,51,47,67,50,55,41,42,10,13,4,62,15,9,52,56,11,44])). % 122.98/123.02 cnf(2907,plain, % 122.98/123.02 (E(f4(a10,f3(a11,a1)),a10)), % 122.98/123.02 inference(scs_inference,[],[2843,2777,2818,2813,54,45,51,47,67,50,55,41,42,10,13,4,62,15,9,52,56,11,44,48])). % 122.98/123.02 cnf(2910,plain, % 122.98/123.02 (E(f8(f3(f12(a11),f13(a1))),f8(f3(a11,f13(a1))))), % 122.98/123.02 inference(scs_inference,[],[2843,2777,2818,2813,54,45,51,47,67,50,55,41,42,10,13,4,62,15,9,52,56,11,44,48,8,18])). % 122.98/123.02 cnf(2911,plain, % 122.98/123.02 (P1(f2(a11))), % 122.98/123.02 inference(scs_inference,[],[2843,2777,2818,2813,28,54,45,51,47,67,50,55,41,42,10,13,4,62,15,9,52,56,11,44,48,8,18,43])). % 122.98/123.02 cnf(2915,plain, % 122.98/123.02 (E(f4(x29151,f3(f12(a11),f13(a1))),f4(x29151,f3(a11,f13(a1))))), % 122.98/123.02 inference(scs_inference,[],[2843,2777,2818,2813,28,54,45,51,47,67,50,55,41,42,10,13,4,62,15,9,52,56,11,44,48,8,18,43,16,12,6])). % 122.98/123.02 cnf(2917,plain, % 122.98/123.02 (E(f4(f3(f12(a11),f13(a1)),x29171),f4(f3(a11,f13(a1)),x29171))), % 122.98/123.02 inference(scs_inference,[],[2843,2777,2818,2813,28,54,45,51,47,67,50,55,41,42,10,13,4,62,15,9,52,56,11,44,48,8,18,43,16,12,6,7,5])). % 122.98/123.02 cnf(2920,plain, % 122.98/123.02 (~E(a1,f13(a1))), % 122.98/123.02 inference(scs_inference,[],[2843,2777,2783,2818,2813,28,54,45,51,47,67,50,55,41,42,10,13,4,62,15,9,52,56,11,44,48,8,18,43,16,12,6,7,5,17,14,2])). % 122.98/123.02 cnf(2927,plain, % 122.98/123.02 (E(f13(f6(f13(f13(a1)))),f13(f13(a1)))), % 122.98/123.02 inference(scs_inference,[],[2843,2777,2783,2818,2813,28,54,45,51,47,67,50,55,41,42,10,13,4,62,15,9,52,56,11,44,48,8,18,43,16,12,6,7,5,17,14,2,76,77,72,49])). % 122.98/123.02 cnf(2929,plain, % 122.98/123.02 (P1(f6(f13(f13(a1))))), % 122.98/123.02 inference(scs_inference,[],[2843,2777,2783,2818,2813,28,54,45,51,47,67,50,55,41,42,10,13,4,62,15,9,52,56,11,44,48,8,18,43,16,12,6,7,5,17,14,2,76,77,72,49,46])). % 122.98/123.02 cnf(2931,plain, % 122.98/123.02 (P2(f9(f3(a11,a1),f3(a11,a1)))), % 122.98/123.02 inference(scs_inference,[],[2843,2777,2783,2818,2813,28,54,45,51,47,67,50,55,41,42,10,13,4,62,15,9,52,56,11,44,48,8,18,43,16,12,6,7,5,17,14,2,76,77,72,49,46,64])). % 122.98/123.02 cnf(2933,plain, % 122.98/123.02 (P2(f3(f12(a11),f13(a1)))), % 122.98/123.02 inference(scs_inference,[],[2843,2777,2783,2818,2813,32,28,54,45,51,47,67,50,55,41,42,10,13,4,62,15,9,52,56,11,44,48,8,18,43,16,12,6,7,5,17,14,2,76,77,72,49,46,64,66])). % 122.98/123.02 cnf(2935,plain, % 122.98/123.02 (P2(f4(f3(a11,a1),f3(a11,a1)))), % 122.98/123.02 inference(scs_inference,[],[2843,2777,2783,2818,2813,32,28,54,45,51,47,67,50,55,41,42,10,13,4,62,15,9,52,56,11,44,48,8,18,43,16,12,6,7,5,17,14,2,76,77,72,49,46,64,66,65])). % 122.98/123.02 cnf(2937,plain, % 122.98/123.02 (~P5(f13(f2(f12(a11))),f13(f2(f12(a11))))), % 122.98/123.02 inference(scs_inference,[],[2843,2777,2783,2818,2813,2844,32,36,28,54,45,51,47,67,50,55,41,42,10,13,4,62,15,9,52,56,11,44,48,8,18,43,16,12,6,7,5,17,14,2,76,77,72,49,46,64,66,65,24])). % 122.98/123.02 cnf(2938,plain, % 122.98/123.02 (~E(f13(f13(a1)),f13(f6(f13(a1))))), % 122.98/123.02 inference(scs_inference,[],[2843,2777,2783,2846,2818,2813,2824,2844,32,36,28,54,45,51,47,67,50,55,41,42,10,13,4,62,15,9,52,56,11,44,48,8,18,43,16,12,6,7,5,17,14,2,76,77,72,49,46,64,66,65,24,3])). % 122.98/123.02 cnf(2939,plain, % 122.98/123.02 (P1(f13(f2(f12(a11))))), % 122.98/123.02 inference(scs_inference,[],[2843,2777,2783,2846,2818,2813,2824,2844,101,32,36,28,54,45,51,47,67,50,55,41,42,10,13,4,62,15,9,52,56,11,44,48,8,18,43,16,12,6,7,5,17,14,2,76,77,72,49,46,64,66,65,24,3,19])). % 122.98/123.02 cnf(2941,plain, % 122.98/123.02 (P4(f4(f8(a10),f8(a10)),f4(f4(f8(a10),a10),f4(a10,f8(a10))))), % 122.98/123.02 inference(scs_inference,[],[39,2843,2777,2783,2846,2818,2813,2824,2844,2869,2803,2801,101,32,36,28,54,45,51,47,67,50,55,41,42,10,13,4,62,15,9,52,56,11,44,48,8,18,43,16,12,6,7,5,17,14,2,76,77,72,49,46,64,66,65,24,3,19,22,23])). % 122.98/123.02 cnf(2947,plain, % 122.98/123.02 (E(f9(f4(f3(a11,a1),f3(a11,a1)),f4(f3(a11,a1),f3(a11,a1))),f4(f9(f3(a11,a1),f3(a11,a1)),f3(a11,a1)))), % 122.98/123.02 inference(scs_inference,[],[39,2843,2777,2783,2846,2818,2813,2824,2844,2869,2803,2801,101,32,36,28,54,45,51,47,67,50,55,41,42,10,13,4,62,15,9,52,56,11,44,48,8,18,43,16,12,6,7,5,17,14,2,76,77,72,49,46,64,66,65,24,3,19,22,23,84,86,87])). % 122.98/123.02 cnf(2951,plain, % 122.98/123.02 (P4(f5(a11,a11),f4(f8(a10),a10))), % 122.98/123.02 inference(scs_inference,[],[39,2843,2777,2783,524,2846,2818,2813,2824,2844,2869,2803,2801,101,32,36,160,28,508,54,45,51,47,67,50,55,41,42,10,13,4,62,15,9,52,56,11,44,48,8,18,43,16,12,6,7,5,17,14,2,76,77,72,49,46,64,66,65,24,3,19,22,23,84,86,87,83,63])). % 122.98/123.02 cnf(2967,plain, % 122.98/123.02 (E(f3(f12(a11),f13(f2(f12(a11)))),f3(a11,f13(f2(f12(a11)))))), % 122.98/123.02 inference(scs_inference,[],[2911,1290])). % 122.98/123.02 cnf(2970,plain, % 122.98/123.02 (E(f9(f8(f5(f12(a11),f12(a11))),f5(f12(a11),f12(a11))),a10)), % 122.98/123.02 inference(scs_inference,[],[2834,50,55])). % 122.98/123.02 cnf(2972,plain, % 122.98/123.02 (~E(f13(f2(a11)),a1)), % 122.98/123.02 inference(scs_inference,[],[2911,2834,50,55,41])). % 122.98/123.02 cnf(2976,plain, % 122.98/123.02 (P4(a10,f4(f5(f12(a11),f12(a11)),f5(f12(a11),f12(a11))))), % 122.98/123.02 inference(scs_inference,[],[2911,2834,50,55,41,45,67])). % 122.98/123.02 cnf(2978,plain, % 122.98/123.02 (P1(f13(f6(f13(a1))))), % 122.98/123.02 inference(scs_inference,[],[2911,2834,2822,50,55,41,45,67,42])). % 122.98/123.02 cnf(2998,plain, % 122.98/123.02 (P5(f2(a11),f13(f2(a11)))), % 122.98/123.02 inference(scs_inference,[],[2911,2879,2834,2822,50,55,41,45,67,42,54,52,51,47,13,10,9,4,62,8,48,16,56])). % 122.98/123.02 cnf(3000,plain, % 122.98/123.02 (P2(f8(f5(f12(a11),f12(a11))))), % 122.98/123.02 inference(scs_inference,[],[2911,2879,2834,2822,50,55,41,45,67,42,54,52,51,47,13,10,9,4,62,8,48,16,56,44])). % 122.98/123.02 cnf(3005,plain, % 122.98/123.02 (E(f5(x30051,f9(a10,f3(a11,a1))),f5(x30051,f3(a11,a1)))), % 122.98/123.02 inference(scs_inference,[],[2911,2879,2834,2822,50,55,41,45,67,42,54,52,51,47,13,10,9,4,62,8,48,16,56,44,15,12,18,11])). % 122.98/123.02 cnf(3011,plain, % 122.98/123.02 (~E(a1,f13(f13(a1)))), % 122.98/123.02 inference(scs_inference,[],[2911,2879,2834,2822,2889,50,55,41,45,67,42,54,52,51,47,13,10,9,4,62,8,48,16,56,44,15,12,18,11,7,17,6,14,5,2])). % 122.98/123.02 cnf(3016,plain, % 122.98/123.02 (E(f13(f6(f2(a11))),f2(a11))), % 122.98/123.02 inference(scs_inference,[],[2911,2879,2834,2822,2889,160,38,50,55,41,45,67,42,54,52,51,47,13,10,9,4,62,8,48,16,56,44,15,12,18,11,7,17,6,14,5,2,76,72,49])). % 122.98/123.02 cnf(3018,plain, % 122.98/123.02 (P1(f6(f2(a11)))), % 122.98/123.02 inference(scs_inference,[],[2911,2879,2834,2822,2889,160,38,50,55,41,45,67,42,54,52,51,47,13,10,9,4,62,8,48,16,56,44,15,12,18,11,7,17,6,14,5,2,76,72,49,46])). % 122.98/123.02 cnf(3022,plain, % 122.98/123.02 (P2(f9(f5(f12(a11),f12(a11)),f5(f12(a11),f12(a11))))), % 122.98/123.02 inference(scs_inference,[],[2911,2879,2834,2822,2889,160,38,50,55,41,45,67,42,54,52,51,47,13,10,9,4,62,8,48,16,56,44,15,12,18,11,7,17,6,14,5,2,76,72,49,46,77,64])). % 122.98/123.02 cnf(3024,plain, % 122.98/123.02 (P2(f4(f5(f12(a11),f12(a11)),f5(f12(a11),f12(a11))))), % 122.98/123.02 inference(scs_inference,[],[2911,2879,2834,2822,2889,160,38,50,55,41,45,67,42,54,52,51,47,13,10,9,4,62,8,48,16,56,44,15,12,18,11,7,17,6,14,5,2,76,72,49,46,77,64,65])). % 122.98/123.02 cnf(3026,plain, % 122.98/123.02 (P2(f3(f12(a11),f2(a11)))), % 122.98/123.02 inference(scs_inference,[],[2911,2879,2834,2822,2889,32,160,38,50,55,41,45,67,42,54,52,51,47,13,10,9,4,62,8,48,16,56,44,15,12,18,11,7,17,6,14,5,2,76,72,49,46,77,64,65,66])). % 122.98/123.02 cnf(3029,plain, % 122.98/123.02 (~P4(f4(f3(a11,a1),a10),f5(a11,a11))), % 122.98/123.02 inference(scs_inference,[],[39,2911,2879,2834,2822,2881,2889,133,32,160,38,50,55,41,45,67,42,54,52,51,47,13,10,9,4,62,8,48,16,56,44,15,12,18,11,7,17,6,14,5,2,76,72,49,46,77,64,65,66,3,22])). % 122.98/123.02 cnf(3041,plain, % 122.98/123.02 (P4(a10,f4(f4(f3(a11,a1),f3(a11,a1)),f4(f3(a11,a1),f3(a11,a1))))), % 122.98/123.02 inference(scs_inference,[],[39,2911,2879,2834,2935,2822,2883,2881,2889,524,762,133,32,726,109,160,38,140,50,55,41,45,67,42,54,52,51,47,13,10,9,4,62,8,48,16,56,44,15,12,18,11,7,17,6,14,5,2,76,72,49,46,77,64,65,66,3,22,23,86,87,84,83,63,82])). % 122.98/123.02 cnf(3043,plain, % 122.98/123.02 (P4(a10,f9(f4(f3(a11,a1),f3(a11,a1)),f4(f3(a11,a1),f3(a11,a1))))), % 122.98/123.02 inference(scs_inference,[],[39,2911,2879,2834,2935,2822,2883,2881,2889,524,762,133,32,726,109,160,38,140,50,55,41,45,67,42,54,52,51,47,13,10,9,4,62,8,48,16,56,44,15,12,18,11,7,17,6,14,5,2,76,72,49,46,77,64,65,66,3,22,23,86,87,84,83,63,82,81])). % 122.98/123.02 cnf(3050,plain, % 122.98/123.02 (~P4(f4(f3(a11,a1),f3(a11,a1)),f5(a11,a11))), % 122.98/123.02 inference(scs_inference,[],[39,2911,2879,2834,2935,2822,2883,2881,2889,2497,524,762,1183,133,1187,32,1182,726,109,160,38,140,27,50,55,41,45,67,42,54,52,51,47,13,10,9,4,62,8,48,16,56,44,15,12,18,11,7,17,6,14,5,2,76,72,49,46,77,64,65,66,3,22,23,86,87,84,83,63,82,81,88,89,24,79])). % 122.98/123.02 cnf(3052,plain, % 122.98/123.02 (~P5(f2(f12(a11)),f2(a11))+P4(a10,f5(f12(a11),f12(a11)))), % 122.98/123.02 inference(scs_inference,[],[39,2911,2879,2834,2935,2822,2883,2881,2889,2497,524,762,1183,133,1187,32,1182,726,109,160,38,140,27,50,55,41,45,67,42,54,52,51,47,13,10,9,4,62,8,48,16,56,44,15,12,18,11,7,17,6,14,5,2,76,72,49,46,77,64,65,66,3,22,23,86,87,84,83,63,82,81,88,89,24,79,80])). % 122.98/123.02 cnf(3054,plain, % 122.98/123.02 (P1(f13(f13(f13(a1))))), % 122.98/123.02 inference(scs_inference,[],[2891,42])). % 122.98/123.02 cnf(3058,plain, % 122.98/123.02 (P4(a10,f4(f8(f3(a11,a1)),f8(f3(a11,a1))))), % 122.98/123.02 inference(scs_inference,[],[2905,2891,42,55,67])). % 122.98/123.02 cnf(3066,plain, % 122.98/123.02 (E(f4(f8(f3(a11,a1)),a10),a10)), % 122.98/123.02 inference(scs_inference,[],[2905,2891,42,55,67,54,50,52,47])). % 122.98/123.02 cnf(3072,plain, % 122.98/123.02 (~E(f13(f13(f13(a1))),a1)), % 122.98/123.02 inference(scs_inference,[],[2905,2891,42,55,67,54,50,52,47,51,45,41])). % 122.98/123.02 cnf(3081,plain, % 122.98/123.02 (P2(f8(f8(f3(a11,a1))))), % 122.98/123.02 inference(scs_inference,[],[2885,2905,2891,42,55,67,54,50,52,47,51,45,41,62,13,10,8,15,4,44])). % 122.98/123.02 cnf(3084,plain, % 122.98/123.02 (E(f4(a10,f8(f3(a11,a1))),a10)), % 122.98/123.02 inference(scs_inference,[],[2885,2905,2891,42,55,67,54,50,52,47,51,45,41,62,13,10,8,15,4,44,9,48])). % 122.98/123.02 cnf(3097,plain, % 122.98/123.02 (~E(a1,f13(f2(a11)))), % 122.98/123.02 inference(scs_inference,[],[2885,2905,2891,2972,42,55,67,54,50,52,47,51,45,41,62,13,10,8,15,4,44,9,48,56,11,12,16,7,18,6,17,5,14,2])). % 122.98/123.02 cnf(3102,plain, % 122.98/123.02 (P1(f6(f13(f2(a11))))), % 122.98/123.02 inference(scs_inference,[],[2885,2905,2891,2972,206,140,42,55,67,54,50,52,47,51,45,41,62,13,10,8,15,4,44,9,48,56,11,12,16,7,18,6,17,5,14,2,76,72,46])). % 122.98/123.02 cnf(3104,plain, % 122.98/123.02 (P2(f9(f8(f3(a11,a1)),f8(f3(a11,a1))))), % 122.98/123.02 inference(scs_inference,[],[2885,2905,2891,2972,206,140,42,55,67,54,50,52,47,51,45,41,62,13,10,8,15,4,44,9,48,56,11,12,16,7,18,6,17,5,14,2,76,72,46,64])). % 122.98/123.02 cnf(3108,plain, % 122.98/123.02 (E(f13(f6(f13(f2(a11)))),f13(f2(a11)))), % 122.98/123.02 inference(scs_inference,[],[2885,2905,2891,2972,206,140,42,55,67,54,50,52,47,51,45,41,62,13,10,8,15,4,44,9,48,56,11,12,16,7,18,6,17,5,14,2,76,72,46,64,77,49])). % 122.98/123.02 cnf(3110,plain, % 122.98/123.02 (P2(f4(f8(f3(a11,a1)),f8(f3(a11,a1))))), % 122.98/123.02 inference(scs_inference,[],[2885,2905,2891,2972,206,140,42,55,67,54,50,52,47,51,45,41,62,13,10,8,15,4,44,9,48,56,11,12,16,7,18,6,17,5,14,2,76,72,46,64,77,49,65])). % 122.98/123.02 cnf(3112,plain, % 122.98/123.02 (P2(f3(f12(a11),f13(f13(a1))))), % 122.98/123.02 inference(scs_inference,[],[2885,2905,2891,2972,32,206,140,42,55,67,54,50,52,47,51,45,41,62,13,10,8,15,4,44,9,48,56,11,12,16,7,18,6,17,5,14,2,76,72,46,64,77,49,65,66])). % 122.98/123.02 cnf(3114,plain, % 122.98/123.02 (~P5(f13(f6(f2(a11))),f13(f2(f12(a11))))), % 122.98/123.02 inference(scs_inference,[],[2885,2905,2891,2972,3016,2844,32,206,140,42,55,67,54,50,52,47,51,45,41,62,13,10,8,15,4,44,9,48,56,11,12,16,7,18,6,17,5,14,2,76,72,46,64,77,49,65,66,24])). % 122.98/123.02 cnf(3115,plain, % 122.98/123.02 (~E(a1,f13(f6(f13(a1))))), % 122.98/123.02 inference(scs_inference,[],[2920,2885,2905,2891,2972,3016,2824,2844,32,206,140,42,55,67,54,50,52,47,51,45,41,62,13,10,8,15,4,44,9,48,56,11,12,16,7,18,6,17,5,14,2,76,72,46,64,77,49,65,66,24,3])). % 122.98/123.02 cnf(3116,plain, % 122.98/123.02 (~P5(f13(f2(f12(a11))),f13(f6(f2(a11))))), % 122.98/123.02 inference(scs_inference,[],[2920,2885,2905,2891,2972,3016,2840,2824,2844,32,206,140,42,55,67,54,50,52,47,51,45,41,62,13,10,8,15,4,44,9,48,56,11,12,16,7,18,6,17,5,14,2,76,72,46,64,77,49,65,66,24,3,25])). % 122.98/123.02 cnf(3119,plain, % 122.98/123.02 (E(f9(f4(a10,a10),f4(a10,a10)),f4(a10,f9(a10,a10)))), % 122.98/123.02 inference(scs_inference,[],[39,2920,2885,2905,2891,2907,2972,3016,3043,2947,2840,2824,2844,32,206,140,27,42,55,67,54,50,52,47,51,45,41,62,13,10,8,15,4,44,9,48,56,11,12,16,7,18,6,17,5,14,2,76,72,46,64,77,49,65,66,24,3,25,22,23,86])). % 122.98/123.02 cnf(3121,plain, % 122.98/123.02 (E(f9(f4(a10,a10),f4(a10,a10)),f4(f9(a10,a10),a10))), % 122.98/123.02 inference(scs_inference,[],[39,2920,2885,2905,2891,2907,2972,3016,3043,2947,2840,2824,2844,32,206,140,27,42,55,67,54,50,52,47,51,45,41,62,13,10,8,15,4,44,9,48,56,11,12,16,7,18,6,17,5,14,2,76,72,46,64,77,49,65,66,24,3,25,22,23,86,87])). % 122.98/123.02 cnf(3131,plain, % 122.98/123.02 (~P4(f4(f3(a11,a1),f3(a11,a1)),f9(f5(f12(a11),f12(a11)),f4(f3(a11,f2(a11)),f3(a11,f2(a11)))))), % 122.98/123.02 inference(scs_inference,[],[39,2920,3050,2885,2905,2891,2907,2972,3016,3024,2976,3043,2947,2840,2824,2844,2866,2935,157,32,206,160,140,27,42,55,67,54,50,52,47,51,45,41,62,13,10,8,15,4,44,9,48,56,11,12,16,7,18,6,17,5,14,2,76,72,46,64,77,49,65,66,24,3,25,22,23,86,87,84,83,63,82,79])). % 122.98/123.02 cnf(3141,plain, % 122.98/123.02 (E(f9(f8(f9(f3(a11,a1),f3(a11,a1))),f9(f3(a11,a1),f3(a11,a1))),a10)), % 122.98/123.02 inference(scs_inference,[],[2931,52,55])). % 122.98/123.02 cnf(3147,plain, % 122.98/123.02 (E(f4(f9(f3(a11,a1),f3(a11,a1)),a10),a10)), % 122.98/123.02 inference(scs_inference,[],[2931,52,55,51,50,47])). % 122.98/123.02 cnf(3149,plain, % 122.98/123.02 (P1(f13(f6(f2(a11))))), % 122.98/123.02 inference(scs_inference,[],[2931,3018,52,55,51,50,47,42])). % 122.98/123.02 cnf(3151,plain, % 122.98/123.02 (~E(f13(f6(f2(a11))),a1)), % 122.98/123.02 inference(scs_inference,[],[2931,3018,52,55,51,50,47,42,41])). % 122.98/123.02 cnf(3155,plain, % 122.98/123.02 (E(f3(f12(a11),f6(f2(a11))),f3(a11,f6(f2(a11))))), % 122.98/123.02 inference(scs_inference,[],[2931,3018,52,55,51,50,47,42,41,45,62])). % 122.98/123.02 cnf(3157,plain, % 122.98/123.02 (P4(a10,f4(f9(f3(a11,a1),f3(a11,a1)),f9(f3(a11,a1),f3(a11,a1))))), % 122.98/123.02 inference(scs_inference,[],[2931,3018,52,55,51,50,47,42,41,45,62,67])). % 122.98/123.02 cnf(3166,plain, % 122.98/123.02 (P5(f6(f2(a11)),f13(f6(f2(a11))))), % 122.98/123.02 inference(scs_inference,[],[2931,3018,3119,52,55,51,50,47,42,41,45,62,67,54,13,15,4,10,11,56])). % 122.98/123.02 cnf(3168,plain, % 122.98/123.02 (P2(f8(f9(f3(a11,a1),f3(a11,a1))))), % 122.98/123.02 inference(scs_inference,[],[2931,3018,3119,52,55,51,50,47,42,41,45,62,67,54,13,15,4,10,11,56,44])). % 122.98/123.02 cnf(3170,plain, % 122.98/123.02 (E(f4(a10,f9(f3(a11,a1),f3(a11,a1))),a10)), % 122.98/123.02 inference(scs_inference,[],[2931,3018,3119,52,55,51,50,47,42,41,45,62,67,54,13,15,4,10,11,56,44,48])). % 122.98/123.02 cnf(3182,plain, % 122.98/123.02 (~E(f5(a11,a11),f4(f8(a10),f4(f8(a10),a10)))), % 122.98/123.02 inference(scs_inference,[],[2931,3018,3119,1000,52,55,51,50,47,42,41,45,62,67,54,13,15,4,10,11,56,44,48,8,7,12,9,18,16,17,6,14,5,2])). % 122.98/123.02 cnf(3183,plain, % 122.98/123.02 (E(f8(f4(a10,a10)),f4(a10,f8(a10)))), % 122.98/123.02 inference(scs_inference,[],[2931,3018,3119,1000,27,52,55,51,50,47,42,41,45,62,67,54,13,15,4,10,11,56,44,48,8,7,12,9,18,16,17,6,14,5,2,76])). % 122.98/123.02 cnf(3189,plain, % 122.98/123.02 (P2(f9(f9(f3(a11,a1),f3(a11,a1)),f9(f3(a11,a1),f3(a11,a1))))), % 122.98/123.02 inference(scs_inference,[],[2931,3018,3119,1000,3054,3072,27,52,55,51,50,47,42,41,45,62,67,54,13,15,4,10,11,56,44,48,8,7,12,9,18,16,17,6,14,5,2,76,49,72,64])). % 122.98/123.02 cnf(3193,plain, % 122.98/123.02 (P1(f6(f13(f13(f13(a1)))))), % 122.98/123.02 inference(scs_inference,[],[2931,3018,3119,1000,3054,3072,27,52,55,51,50,47,42,41,45,62,67,54,13,15,4,10,11,56,44,48,8,7,12,9,18,16,17,6,14,5,2,76,49,72,64,77,46])). % 122.98/123.02 cnf(3195,plain, % 122.98/123.02 (P2(f4(f9(f3(a11,a1),f3(a11,a1)),f9(f3(a11,a1),f3(a11,a1))))), % 122.98/123.02 inference(scs_inference,[],[2931,3018,3119,1000,3054,3072,27,52,55,51,50,47,42,41,45,62,67,54,13,15,4,10,11,56,44,48,8,7,12,9,18,16,17,6,14,5,2,76,49,72,64,77,46,65])). % 122.98/123.02 cnf(3197,plain, % 122.98/123.02 (P2(f3(f12(a11),f6(f2(a11))))), % 122.98/123.02 inference(scs_inference,[],[2931,3018,3119,1000,3054,3072,32,27,52,55,51,50,47,42,41,45,62,67,54,13,15,4,10,11,56,44,48,8,7,12,9,18,16,17,6,14,5,2,76,49,72,64,77,46,65,66])). % 122.98/123.02 cnf(3199,plain, % 122.98/123.02 (~P5(f2(a11),f13(f6(f2(a11))))), % 122.98/123.02 inference(scs_inference,[],[2931,3018,3119,1000,3054,3072,3116,101,32,27,52,55,51,50,47,42,41,45,62,67,54,13,15,4,10,11,56,44,48,8,7,12,9,18,16,17,6,14,5,2,76,49,72,64,77,46,65,66,24])). % 122.98/123.02 cnf(3201,plain, % 122.98/123.02 (~P5(f13(f6(f2(a11))),f2(a11))), % 122.98/123.02 inference(scs_inference,[],[2931,3018,3119,2887,1000,3054,3072,3114,3116,580,101,32,27,52,55,51,50,47,42,41,45,62,67,54,13,15,4,10,11,56,44,48,8,7,12,9,18,16,17,6,14,5,2,76,49,72,64,77,46,65,66,24,3,25])). % 122.98/123.02 cnf(3203,plain, % 122.98/123.02 (~P4(f4(f3(a11,a1),a10),f9(f5(f12(a11),f12(a11)),f4(f3(a11,f2(a11)),f3(a11,f2(a11)))))), % 122.98/123.02 inference(scs_inference,[],[39,3029,2931,3018,3119,2887,1000,3054,3072,3114,3116,580,101,32,109,27,52,55,51,50,47,42,41,45,62,67,54,13,15,4,10,11,56,44,48,8,7,12,9,18,16,17,6,14,5,2,76,49,72,64,77,46,65,66,24,3,25,22,23])). % 122.98/123.02 cnf(3204,plain, % 122.98/123.02 (E(f4(f4(a10,a10),a10),f4(a10,f4(a10,a10)))), % 122.98/123.02 inference(scs_inference,[],[39,3029,2931,3018,3119,2887,1000,3054,3072,3114,3116,580,101,32,109,27,52,55,51,50,47,42,41,45,62,67,54,13,15,4,10,11,56,44,48,8,7,12,9,18,16,17,6,14,5,2,76,49,72,64,77,46,65,66,24,3,25,22,23,84])). % 122.98/123.02 cnf(3206,plain, % 122.98/123.02 (E(f9(f9(a10,a10),a10),f9(a10,f9(a10,a10)))), % 122.98/123.02 inference(scs_inference,[],[39,3029,2931,3018,3119,2887,1000,3054,3072,3114,3116,580,101,32,109,27,52,55,51,50,47,42,41,45,62,67,54,13,15,4,10,11,56,44,48,8,7,12,9,18,16,17,6,14,5,2,76,49,72,64,77,46,65,66,24,3,25,22,23,84,83])). % 122.98/123.02 cnf(3216,plain, % 122.98/123.02 (~E(f9(f3(a11,a1),f3(a11,a1)),x32161)+P2(x32161)), % 122.98/123.02 inference(scs_inference,[],[39,2900,3029,2931,2836,3018,3119,2887,1000,3054,3072,3110,3058,3114,3116,3131,580,2935,101,157,32,2843,109,105,27,52,55,51,50,47,42,41,45,62,67,54,13,15,4,10,11,56,44,48,8,7,12,9,18,16,17,6,14,5,2,76,49,72,64,77,46,65,66,24,3,25,22,23,84,83,63,88,82,89,20])). % 122.98/123.02 cnf(3218,plain, % 122.98/123.02 (P1(f13(f6(f13(f13(a1)))))), % 122.98/123.02 inference(scs_inference,[],[2929,42])). % 122.98/123.02 cnf(3220,plain, % 122.98/123.02 (E(f9(f8(f3(f12(a11),f13(a1))),f3(f12(a11),f13(a1))),a10)), % 122.98/123.02 inference(scs_inference,[],[2933,2929,42,55])). % 122.98/123.02 cnf(3224,plain, % 122.98/123.02 (~E(f13(f6(f13(f13(a1)))),a1)), % 122.98/123.02 inference(scs_inference,[],[2933,2929,42,55,45,41])). % 122.98/123.02 cnf(3226,plain, % 122.98/123.02 (E(f4(f3(f12(a11),f13(a1)),a10),a10)), % 122.98/123.02 inference(scs_inference,[],[2933,2929,42,55,45,41,47])). % 122.98/123.02 cnf(3230,plain, % 122.98/123.02 (P4(f3(f12(a11),f13(a1)),f3(f12(a11),f13(a1)))), % 122.98/123.02 inference(scs_inference,[],[2933,2929,42,55,45,41,47,62,52])). % 122.98/123.02 cnf(3232,plain, % 122.98/123.02 (P4(a10,f4(f3(f12(a11),f13(a1)),f3(f12(a11),f13(a1))))), % 122.98/123.02 inference(scs_inference,[],[2933,2929,42,55,45,41,47,62,52,67])). % 122.98/123.02 cnf(3236,plain, % 122.98/123.02 (E(f9(a10,f3(f12(a11),f13(a1))),f3(f12(a11),f13(a1)))), % 122.98/123.02 inference(scs_inference,[],[2933,2929,42,55,45,41,47,62,52,67,54,51])). % 122.98/123.02 cnf(3245,plain, % 122.98/123.02 (P2(f8(f3(f12(a11),f13(a1))))), % 122.98/123.02 inference(scs_inference,[],[2933,3183,2929,42,55,45,41,47,62,52,67,54,51,50,13,10,11,7,15,44])). % 122.98/123.02 cnf(3250,plain, % 122.98/123.02 (E(f4(a10,f3(f12(a11),f13(a1))),a10)), % 122.98/123.02 inference(scs_inference,[],[2933,3183,2929,42,55,45,41,47,62,52,67,54,51,50,13,10,11,7,15,44,56,4,48])). % 122.98/123.02 cnf(3261,plain, % 122.98/123.02 (~E(f5(a11,a11),f4(f8(a10),f9(a10,f8(a10))))), % 122.98/123.02 inference(scs_inference,[],[2933,3183,2006,2929,42,55,45,41,47,62,52,67,54,51,50,13,10,11,7,15,44,56,4,48,18,8,12,16,9,6,17,5,14,2])). % 122.98/123.02 cnf(3262,plain, % 122.98/123.02 (E(f13(f6(f13(f6(f2(a11))))),f13(f6(f2(a11))))), % 122.98/123.02 inference(scs_inference,[],[2933,3183,2006,2929,3149,3151,42,55,45,41,47,62,52,67,54,51,50,13,10,11,7,15,44,56,4,48,18,8,12,16,9,6,17,5,14,2,49])). % 122.98/123.02 cnf(3264,plain, % 122.98/123.02 (P2(f9(f3(f12(a11),f13(a1)),f3(f12(a11),f13(a1))))), % 122.98/123.02 inference(scs_inference,[],[2933,3183,2006,2929,3149,3151,42,55,45,41,47,62,52,67,54,51,50,13,10,11,7,15,44,56,4,48,18,8,12,16,9,6,17,5,14,2,49,64])). % 122.98/123.02 cnf(3266,plain, % 122.98/123.02 (P1(f6(f13(f6(f2(a11)))))), % 122.98/123.02 inference(scs_inference,[],[2933,3183,2006,2929,3149,3151,42,55,45,41,47,62,52,67,54,51,50,13,10,11,7,15,44,56,4,48,18,8,12,16,9,6,17,5,14,2,49,64,46])). % 122.98/123.02 cnf(3272,plain, % 122.98/123.02 (P2(f4(f3(f12(a11),f13(a1)),f3(f12(a11),f13(a1))))), % 122.98/123.02 inference(scs_inference,[],[2933,3183,2006,2929,3149,3151,42,55,45,41,47,62,52,67,54,51,50,13,10,11,7,15,44,56,4,48,18,8,12,16,9,6,17,5,14,2,49,64,46,77,72,65])). % 122.98/123.02 cnf(3279,plain, % 122.98/123.02 (~P4(f9(f3(a11,a1),f8(f3(a11,a1))),f5(a11,a11))), % 122.98/123.02 inference(scs_inference,[],[39,581,2933,3183,2006,3201,2929,3149,2875,3151,2927,127,32,42,55,45,41,47,62,52,67,54,51,50,13,10,11,7,15,44,56,4,48,18,8,12,16,9,6,17,5,14,2,49,64,46,77,72,65,66,24,3,25,22])). % 122.98/123.02 cnf(3292,plain, % 122.98/123.02 (E(f3(f12(a11),f13(f6(f13(a1)))),f3(a11,f13(f6(f13(a1)))))), % 122.98/123.02 inference(scs_inference,[],[2978,62])). % 122.98/123.02 cnf(3300,plain, % 122.98/123.02 (E(f4(f3(f12(a11),f2(a11)),a10),a10)), % 122.98/123.02 inference(scs_inference,[],[3026,2978,62,55,67,52,47])). % 122.98/123.02 cnf(3304,plain, % 122.98/123.02 (P1(f13(f13(f2(f12(a11)))))), % 122.98/123.02 inference(scs_inference,[],[3026,2939,2978,62,55,67,52,47,54,42])). % 122.98/123.02 cnf(3312,plain, % 122.98/123.02 (~E(f13(f13(f2(f12(a11)))),a1)), % 122.98/123.02 inference(scs_inference,[],[3026,2939,2978,62,55,67,52,47,54,42,51,50,45,41])). % 122.98/123.02 cnf(3324,plain, % 122.98/123.02 (P2(f8(f3(f12(a11),f2(a11))))), % 122.98/123.02 inference(scs_inference,[],[3026,3121,2939,2978,62,55,67,52,47,54,42,51,50,45,41,13,7,15,10,11,18,48,56,44])). % 122.98/123.02 cnf(3335,plain, % 122.98/123.02 (~E(f13(f6(f13(a1))),a1)), % 122.98/123.02 inference(scs_inference,[],[3026,3121,2939,2978,3115,62,55,67,52,47,54,42,51,50,45,41,13,7,15,10,11,18,48,56,44,16,8,4,9,12,17,6,14,5,2])). % 122.98/123.02 cnf(3338,plain, % 122.98/123.02 (P2(f9(f3(f12(a11),f2(a11)),f3(f12(a11),f2(a11))))), % 122.98/123.02 inference(scs_inference,[],[3026,3121,2939,2978,3115,62,55,67,52,47,54,42,51,50,45,41,13,7,15,10,11,18,48,56,44,16,8,4,9,12,17,6,14,5,2,49,64])). % 122.98/123.02 cnf(3346,plain, % 122.98/123.02 (P2(f4(f3(f12(a11),f2(a11)),f3(f12(a11),f2(a11))))), % 122.98/123.02 inference(scs_inference,[],[3026,3121,2939,2978,3115,3218,3224,62,55,67,52,47,54,42,51,50,45,41,13,7,15,10,11,18,48,56,44,16,8,4,9,12,17,6,14,5,2,49,64,77,72,46,65])). % 122.98/123.02 cnf(3348,plain, % 122.98/123.02 (P2(f3(f12(a11),f13(f2(f12(a11)))))), % 122.98/123.02 inference(scs_inference,[],[3026,3121,2939,2978,3115,3218,3224,32,62,55,67,52,47,54,42,51,50,45,41,13,7,15,10,11,18,48,56,44,16,8,4,9,12,17,6,14,5,2,49,64,77,72,46,65,66])). % 122.98/123.02 cnf(3350,plain, % 122.98/123.02 (~P5(f13(f6(f2(a11))),f13(f6(f2(a11))))), % 122.98/123.02 inference(scs_inference,[],[3026,3121,2939,2978,3199,3115,3218,3224,3016,32,62,55,67,52,47,54,42,51,50,45,41,13,7,15,10,11,18,48,56,44,16,8,4,9,12,17,6,14,5,2,49,64,77,72,46,65,66,24])). % 122.98/123.02 cnf(3380,plain, % 122.98/123.02 (E(f3(f12(a11),f6(f13(a1))),f3(a11,f6(f13(a1))))), % 122.98/123.02 inference(scs_inference,[],[3000,3193,2822,54,55,42,51,47,50,62])). % 122.98/123.02 cnf(3388,plain, % 122.98/123.02 (P4(a10,f4(f8(f5(f12(a11),f12(a11))),f8(f5(f12(a11),f12(a11)))))), % 122.98/123.02 inference(scs_inference,[],[3000,3193,2822,54,55,42,51,47,50,62,45,41,52,67])). % 122.98/123.02 cnf(3393,plain, % 122.98/123.02 (P2(f8(f8(f5(f12(a11),f12(a11)))))), % 122.98/123.02 inference(scs_inference,[],[3204,3000,3193,2822,54,55,42,51,47,50,62,45,41,52,67,13,10,11,44])). % 122.98/123.02 cnf(3399,plain, % 122.98/123.02 (P5(f6(f13(a1)),f13(f6(f13(a1))))), % 122.98/123.02 inference(scs_inference,[],[3204,3000,3193,2822,54,55,42,51,47,50,62,45,41,52,67,13,10,11,44,7,48,16,56])). % 122.98/123.02 cnf(3411,plain, % 122.98/123.02 (~E(f13(f6(f13(a1))),f13(f13(a1)))), % 122.98/123.02 inference(scs_inference,[],[3204,3000,2938,3193,2822,54,55,42,51,47,50,62,45,41,52,67,13,10,11,44,7,48,16,56,15,9,18,8,12,4,6,17,5,14,2])). % 122.98/123.02 cnf(3416,plain, % 122.98/123.02 (P1(f6(f13(f13(f2(f12(a11))))))), % 122.98/123.02 inference(scs_inference,[],[3204,3000,2938,3193,3304,3312,2836,2822,54,55,42,51,47,50,62,45,41,52,67,13,10,11,44,7,48,16,56,15,9,18,8,12,4,6,17,5,14,2,64,72,46])). % 122.98/123.02 cnf(3420,plain, % 122.98/123.02 (P2(f4(f8(f5(f12(a11),f12(a11))),f8(f5(f12(a11),f12(a11)))))), % 122.98/123.02 inference(scs_inference,[],[3204,3000,2938,3193,3304,3312,2836,2822,54,55,42,51,47,50,62,45,41,52,67,13,10,11,44,7,48,16,56,15,9,18,8,12,4,6,17,5,14,2,64,72,46,77,65])). % 122.98/123.02 cnf(3424,plain, % 122.98/123.02 (~P5(f13(f6(f13(f6(f2(a11))))),f13(f6(f2(a11))))), % 122.98/123.02 inference(scs_inference,[],[3204,3000,2938,3350,3193,3304,3312,2836,2822,3262,32,54,55,42,51,47,50,62,45,41,52,67,13,10,11,44,7,48,16,56,15,9,18,8,12,4,6,17,5,14,2,64,72,46,77,65,66,24])). % 122.98/123.02 cnf(3425,plain, % 122.98/123.02 (~E(f9(f5(f12(a11),f12(a11)),f4(f3(a11,f2(a11)),f3(a11,f2(a11)))),f9(f8(a10),a10))), % 122.98/123.02 inference(scs_inference,[],[654,3204,3000,2938,3350,3193,3304,3312,2836,2822,3262,127,32,54,55,42,51,47,50,62,45,41,52,67,13,10,11,44,7,48,16,56,15,9,18,8,12,4,6,17,5,14,2,64,72,46,77,65,66,24,3])). % 122.98/123.02 cnf(3447,plain, % 122.98/123.02 (~E(f13(f6(f13(f6(f2(a11))))),a1)), % 122.98/123.02 inference(scs_inference,[],[3081,3266,3102,50,45,55,47,62,41])). % 122.98/123.02 cnf(3460,plain, % 122.98/123.02 (P2(f8(f8(f8(f3(a11,a1)))))), % 122.98/123.02 inference(scs_inference,[],[3206,3081,3266,3102,50,45,55,47,62,41,54,67,52,51,42,13,44])). % 122.98/123.02 cnf(3468,plain, % 122.98/123.02 (P5(f6(f13(f2(a11))),f13(f6(f13(f2(a11)))))), % 122.98/123.02 inference(scs_inference,[],[3206,3081,3266,3102,50,45,55,47,62,41,54,67,52,51,42,13,44,7,9,48,10,11,56])). % 122.98/123.02 cnf(3489,plain, % 122.98/123.02 (P1(f6(f13(f6(f13(a1)))))), % 122.98/123.02 inference(scs_inference,[],[3206,3081,3335,1440,3266,3102,2978,2935,50,45,55,47,62,41,54,67,52,51,42,13,44,7,9,48,10,11,56,12,15,16,18,4,8,17,6,14,5,2,64,72,77,65,46])). % 122.98/123.02 cnf(3508,plain, % 122.98/123.02 (~E(f13(f6(f13(f6(f13(a1))))),a1)), % 122.98/123.02 inference(scs_inference,[],[3489,41])). % 122.98/123.02 cnf(3531,plain, % 122.98/123.02 (P2(f8(f8(f9(f3(a11,a1),f3(a11,a1)))))), % 122.98/123.02 inference(scs_inference,[],[3168,3066,3489,3054,41,67,54,45,62,52,50,42,51,47,55,13,44])). % 122.98/123.02 cnf(3537,plain, % 122.98/123.02 (E(f9(f4(f8(f3(a11,a1)),a10),x35371),f9(a10,x35371))), % 122.98/123.02 inference(scs_inference,[],[3168,3066,3489,3054,41,67,54,45,62,52,50,42,51,47,55,13,44,48,9,15,7])). % 122.98/123.02 cnf(3545,plain, % 122.98/123.02 (E(f9(x35451,f4(f8(f3(a11,a1)),a10)),f9(x35451,a10))), % 122.98/123.02 inference(scs_inference,[],[3168,3066,3489,3054,41,67,54,45,62,52,50,42,51,47,55,13,44,48,9,15,7,56,4,10,16,11,12,8])). % 122.98/123.02 cnf(3563,plain, % 122.98/123.02 (~E(f9(f5(f12(a11),f12(a11)),f4(f3(a11,f2(a11)),f3(a11,f2(a11)))),f4(f8(a10),f8(a10)))), % 122.98/123.02 inference(scs_inference,[],[2821,3168,3066,3166,1815,3489,3424,3054,286,127,32,41,67,54,45,62,52,50,42,51,47,55,13,44,48,9,15,7,56,4,10,16,11,12,8,18,6,17,2,5,14,64,72,65,77,66,24,3])). % 122.98/123.02 cnf(3565,plain, % 122.98/123.02 (~P4(f4(f8(f3(a11,a1)),a10),f5(a11,a11))), % 122.98/123.02 inference(scs_inference,[],[39,2821,3168,3066,3166,1815,3489,3108,3468,3424,3054,286,127,32,41,67,54,45,62,52,50,42,51,47,55,13,44,48,9,15,7,56,4,10,16,11,12,8,18,6,17,2,5,14,64,72,65,77,66,24,3,25,22])). % 122.98/123.02 cnf(3568,plain, % 122.98/123.02 (P4(f5(a11,a11),f9(f8(a10),a10))), % 122.98/123.02 inference(scs_inference,[],[39,2821,3168,3066,3166,1815,2805,3489,3108,2862,3468,3424,3054,687,286,127,32,160,655,41,67,54,45,62,52,50,42,51,47,55,13,44,48,9,15,7,56,4,10,16,11,12,8,18,6,17,2,5,14,64,72,65,77,66,24,3,25,22,23,63])). % 122.98/123.02 cnf(3576,plain, % 122.98/123.02 (P2(f8(f3(a11,f13(a1))))), % 122.98/123.02 inference(scs_inference,[],[39,2821,3230,3168,3245,3066,3166,1815,2805,2910,3489,3108,2862,3468,3424,3058,3054,3110,687,2933,286,127,32,160,655,41,67,54,45,62,52,50,42,51,47,55,13,44,48,9,15,7,56,4,10,16,11,12,8,18,6,17,2,5,14,64,72,65,77,66,24,3,25,22,23,63,82,88,46,20])). % 122.98/123.02 cnf(3577,plain, % 122.98/123.02 (~E(f13(f13(f6(f13(f13(a1))))),f13(a1))), % 122.98/123.02 inference(scs_inference,[],[39,2821,3230,3168,3245,3066,3166,1815,2805,2910,3489,3108,2862,3468,3424,3058,3218,3224,3054,3110,687,2933,286,127,26,32,160,655,41,67,54,45,62,52,50,42,51,47,55,13,44,48,9,15,7,56,4,10,16,11,12,8,18,6,17,2,5,14,64,72,65,77,66,24,3,25,22,23,63,82,88,46,20,57])). % 122.98/123.02 cnf(3585,plain, % 122.98/123.02 (~E(f13(f13(f13(f2(f12(a11))))),a1)), % 122.98/123.02 inference(scs_inference,[],[3324,3304,45,41])). % 122.98/123.02 cnf(3606,plain, % 122.98/123.02 (P2(f8(f8(f3(f12(a11),f2(a11)))))), % 122.98/123.02 inference(scs_inference,[],[3324,3084,3304,3149,45,41,42,67,47,52,62,55,51,54,50,13,44])). % 122.98/123.02 cnf(3613,plain, % 122.98/123.02 (E(f9(f4(a10,f8(f3(a11,a1))),x36131),f9(a10,x36131))), % 122.98/123.02 inference(scs_inference,[],[3324,3084,3304,3149,45,41,42,67,47,52,62,55,51,54,50,13,44,48,9,56,7])). % 122.98/123.02 cnf(3619,plain, % 122.98/123.02 (E(f9(x36191,f4(a10,f8(f3(a11,a1)))),f9(x36191,a10))), % 122.98/123.02 inference(scs_inference,[],[3324,3084,3304,3149,45,41,42,67,47,52,62,55,51,54,50,13,44,48,9,56,7,4,10,11,15,16,8])). % 122.98/123.02 cnf(3624,plain, % 122.98/123.02 (~E(f9(f5(f12(a11),f12(a11)),f4(f3(a11,f2(a11)),f3(a11,f2(a11)))),f9(a10,a10))), % 122.98/123.02 inference(scs_inference,[],[3324,3084,322,3304,3149,45,41,42,67,47,52,62,55,51,54,50,13,44,48,9,56,7,4,10,11,15,16,8,18,12,6,17,2])). % 122.98/123.02 cnf(3640,plain, % 122.98/123.02 (~E(f13(a1),f13(f13(f13(a1))))), % 122.98/123.02 inference(scs_inference,[],[39,3011,3279,3324,3084,322,3304,3149,580,2891,109,26,32,160,45,41,42,67,47,52,62,55,51,54,50,13,44,48,9,56,7,4,10,11,15,16,8,18,12,6,17,2,14,5,64,72,65,66,77,3,22,23,57])). % 122.98/123.02 cnf(3644,plain, % 122.98/123.02 (P4(f9(f8(f3(f12(a11),f2(a11))),f5(a11,a11)),f9(f8(f3(f12(a11),f2(a11))),f9(f8(a10),a10)))), % 122.98/123.02 inference(scs_inference,[],[39,3568,3011,3279,3324,3084,322,3304,3149,580,2891,599,109,26,32,160,582,655,45,41,42,67,47,52,62,55,51,54,50,13,44,48,9,56,7,4,10,11,15,16,8,18,12,6,17,2,14,5,64,72,65,66,77,3,22,23,57,63,88])). % 122.98/123.02 cnf(3656,plain, % 122.98/123.02 (~E(f13(f13(f6(f13(f13(a1))))),a1)), % 122.98/123.02 inference(scs_inference,[],[3112,3218,67,45,41])). % 122.98/123.02 cnf(3666,plain, % 122.98/123.02 (P1(f13(f13(f6(f13(f13(a1))))))), % 122.98/123.02 inference(scs_inference,[],[3112,3218,67,45,41,55,54,50,52,42])). % 122.98/123.02 cnf(3680,plain, % 122.98/123.02 (E(f9(f4(f9(f3(a11,a1),f3(a11,a1)),a10),x36801),f9(a10,x36801))), % 122.98/123.02 inference(scs_inference,[],[3112,3147,3218,2978,67,45,41,55,54,50,52,42,47,51,13,48,44,9,56,7])). % 122.98/123.02 cnf(3689,plain, % 122.98/123.02 (~E(f13(f13(f13(a1))),f13(a1))), % 122.98/123.02 inference(scs_inference,[],[3112,3640,3147,3218,2978,67,45,41,55,54,50,52,42,47,51,13,48,44,9,56,7,4,10,11,16,15,18,8,12,2])). % 122.98/123.02 cnf(3703,plain, % 122.98/123.02 (~E(a1,f13(f6(f13(f2(a11)))))), % 122.98/123.02 inference(scs_inference,[],[3097,3112,3640,3147,3108,2824,3218,2978,582,67,45,41,55,54,50,52,42,47,51,13,48,44,9,56,7,4,10,11,16,15,18,8,12,2,6,17,5,14,72,64,77,65,24,3])). % 122.98/123.02 cnf(3721,plain, % 122.98/123.02 (P1(f13(f13(f6(f13(a1)))))), % 122.98/123.02 inference(scs_inference,[],[3197,2978,55,67,45,42])). % 122.98/123.02 cnf(3725,plain, % 122.98/123.02 (~E(f13(f2(f12(a11))),a1)), % 122.98/123.02 inference(scs_inference,[],[3197,2818,2978,55,67,45,42,51,41])). % 122.98/123.02 cnf(3733,plain, % 122.98/123.02 (P4(f3(f12(a11),f6(f2(a11))),f3(f12(a11),f6(f2(a11))))), % 122.98/123.02 inference(scs_inference,[],[3197,2818,2978,55,67,45,42,51,41,54,50,47,52])). % 122.98/123.02 cnf(3738,plain, % 122.98/123.02 (P2(f8(f3(f12(a11),f6(f2(a11)))))), % 122.98/123.02 inference(scs_inference,[],[3197,3170,2818,2978,55,67,45,42,51,41,54,50,47,52,13,48,44])). % 122.98/123.02 cnf(3752,plain, % 122.98/123.02 (~E(f13(f6(f13(f2(a11)))),a1)), % 122.98/123.02 inference(scs_inference,[],[3197,3170,3703,2818,2978,206,55,67,45,42,51,41,54,50,47,52,13,48,44,56,9,10,11,4,7,16,15,18,12,8,2])). % 122.98/123.02 cnf(3757,plain, % 122.98/123.02 (E(f13(f6(f13(f2(f12(a11))))),f13(f2(f12(a11))))), % 122.98/123.02 inference(scs_inference,[],[3197,3170,3703,2818,2939,2978,206,55,67,45,42,51,41,54,50,47,52,13,48,44,56,9,10,11,4,7,16,15,18,12,8,2,6,17,5,14,49])). % 122.98/123.02 cnf(3759,plain, % 122.98/123.02 (E(f4(f8(f8(a10)),f8(f8(a10))),f4(f8(a10),f8(a10)))), % 122.98/123.02 inference(scs_inference,[],[3197,3170,3703,2818,2939,2978,206,140,55,67,45,42,51,41,54,50,47,52,13,48,44,56,9,10,11,4,7,16,15,18,12,8,2,6,17,5,14,49,72])). % 122.98/123.02 cnf(3763,plain, % 122.98/123.02 (E(f8(f4(f8(a10),f8(a10))),f4(f8(f8(a10)),f8(a10)))), % 122.98/123.02 inference(scs_inference,[],[3197,3170,3703,2818,2939,2978,206,140,55,67,45,42,51,41,54,50,47,52,13,48,44,56,9,10,11,4,7,16,15,18,12,8,2,6,17,5,14,49,72,64,77])). % 122.98/123.02 cnf(3767,plain, % 122.98/123.02 (P1(f6(f13(f2(f12(a11)))))), % 122.98/123.02 inference(scs_inference,[],[3197,3170,3703,2818,2939,2978,206,140,55,67,45,42,51,41,54,50,47,52,13,48,44,56,9,10,11,4,7,16,15,18,12,8,2,6,17,5,14,49,72,64,77,65,46])). % 122.98/123.02 cnf(3770,plain, % 122.98/123.02 (~P5(f13(f6(f13(f6(f2(a11))))),f13(f2(f12(a11))))), % 122.98/123.02 inference(scs_inference,[],[3197,3170,3703,3114,3262,2818,2939,2978,580,206,140,55,67,45,42,51,41,54,50,47,52,13,48,44,56,9,10,11,4,7,16,15,18,12,8,2,6,17,5,14,49,72,64,77,65,46,3,24])). % 122.98/123.02 cnf(3771,plain, % 122.98/123.02 (~P4(f4(a10,f9(f3(a11,a1),f3(a11,a1))),f5(a11,a11))), % 122.98/123.02 inference(scs_inference,[],[39,3197,3170,3703,3114,3262,2818,2939,2978,580,206,140,55,67,45,42,51,41,54,50,47,52,13,48,44,56,9,10,11,4,7,16,15,18,12,8,2,6,17,5,14,49,72,64,77,65,46,3,24,22])). % 122.98/123.02 cnf(3793,plain, % 122.98/123.02 (~E(f13(f13(f13(f6(f13(a1))))),a1)), % 122.98/123.02 inference(scs_inference,[],[3576,3721,67,42,55,50,45,52,41])). % 122.98/123.02 cnf(3804,plain, % 122.98/123.02 (P2(f8(f8(f3(a11,f13(a1)))))), % 122.98/123.02 inference(scs_inference,[],[3576,3226,3721,67,42,55,50,45,52,41,51,47,54,13,48,44])). % 122.98/123.02 cnf(3817,plain, % 122.98/123.02 (~E(a1,f13(f2(f12(a11))))), % 122.98/123.02 inference(scs_inference,[],[3576,3725,3226,3721,67,42,55,50,45,52,41,51,47,54,13,48,44,9,4,11,7,16,10,18,15,8,12,6,2])). % 122.98/123.02 cnf(3832,plain, % 122.98/123.02 (~E(f13(f13(f13(a1))),f13(f6(f13(a1))))), % 122.98/123.02 inference(scs_inference,[],[3689,3576,3725,3226,3721,3757,2937,2824,32,508,67,42,55,50,45,52,41,51,47,54,13,48,44,9,4,11,7,16,10,18,15,8,12,6,2,5,17,14,66,72,64,77,65,25,3])). % 122.98/123.02 cnf(3860,plain, % 122.98/123.02 (~E(f13(f6(f13(f2(f12(a11))))),a1)), % 122.98/123.02 inference(scs_inference,[],[3189,3767,3245,42,50,67,51,55,45,54,52,41])). % 122.98/123.02 cnf(3867,plain, % 122.98/123.02 (P2(f8(f9(f9(f3(a11,a1),f3(a11,a1)),f9(f3(a11,a1),f3(a11,a1)))))), % 122.98/123.02 inference(scs_inference,[],[3250,3189,3767,3245,42,50,67,51,55,45,54,52,41,47,48,13,44])). % 122.98/123.02 cnf(3894,plain, % 122.98/123.02 (P2(f3(a11,f13(f2(f12(a11)))))), % 122.98/123.02 inference(scs_inference,[],[3250,3189,3832,3348,3767,2967,3245,32,655,42,50,67,51,55,45,54,52,41,47,48,13,44,9,4,7,16,10,11,18,15,8,12,6,2,5,17,14,72,66,64,77,65,20])). % 122.98/123.02 cnf(3898,plain, % 122.98/123.02 (~P4(f4(a10,f3(f12(a11),f13(a1))),f5(a11,a11))), % 122.98/123.02 inference(scs_inference,[],[39,3250,3189,3399,3832,3348,3767,2967,3770,3245,2902,2824,580,32,655,42,50,67,51,55,45,54,52,41,47,48,13,44,9,4,7,16,10,11,18,15,8,12,6,2,5,17,14,72,66,64,77,65,20,25,24,3,22])). % 122.98/123.02 cnf(3906,plain, % 122.98/123.02 (P1(f13(f6(f13(f2(a11)))))), % 122.98/123.02 inference(scs_inference,[],[3102,42])). % 122.98/123.02 cnf(3910,plain, % 122.98/123.02 (E(f9(f8(f3(f12(a11),a1)),f3(f12(a11),a1)),a10)), % 122.98/123.02 inference(scs_inference,[],[3264,2836,3102,42,50,55])). % 122.98/123.02 cnf(3922,plain, % 122.98/123.02 (~E(f13(f13(f13(f13(a1)))),a1)), % 122.98/123.02 inference(scs_inference,[],[3393,3264,2836,3102,3054,42,50,55,67,45,52,51,54,41])). % 122.98/123.02 cnf(3944,plain, % 122.98/123.02 (~E(f4(f8(a10),f8(a10)),f9(f5(f12(a11),f12(a11)),f4(f3(a11,f2(a11)),f3(a11,f2(a11)))))), % 122.98/123.02 inference(scs_inference,[],[3300,3393,3563,3264,2836,3102,3054,42,50,55,67,45,52,51,54,41,47,48,13,44,4,16,9,18,7,10,11,15,8,12,6,5,17,2])). % 122.98/123.02 cnf(3946,plain, % 122.98/123.02 (E(f4(f8(a10),f8(a10)),f4(a10,a10))), % 122.98/123.02 inference(scs_inference,[],[3300,3393,3563,3264,2836,3102,3054,27,42,50,55,67,45,52,51,54,41,47,48,13,44,4,16,9,18,7,10,11,15,8,12,6,5,17,2,14,72])). % 122.98/123.02 cnf(3950,plain, % 122.98/123.02 (E(f8(f4(a10,a10)),f4(f8(a10),a10))), % 122.98/123.02 inference(scs_inference,[],[3300,3393,3563,3264,2836,3102,3054,27,42,50,55,67,45,52,51,54,41,47,48,13,44,4,16,9,18,7,10,11,15,8,12,6,5,17,2,14,72,64,77])). % 122.98/123.02 cnf(3957,plain, % 122.98/123.02 (~E(f9(f5(f12(a11),f12(a11)),f4(f3(a11,f2(a11)),f3(a11,f2(a11)))),f4(f8(a10),f4(f8(a10),a10)))), % 122.98/123.02 inference(scs_inference,[],[3182,3300,3393,3752,3563,3264,3757,3114,2836,3102,3054,127,27,42,50,55,67,45,52,51,54,41,47,48,13,44,4,16,9,18,7,10,11,15,8,12,6,5,17,2,14,72,64,77,46,65,25,3])). % 122.98/123.02 cnf(3966,plain, % 122.98/123.02 (~E(f13(f13(a1)),f13(f13(f13(f13(a1)))))), % 122.98/123.02 inference(scs_inference,[],[39,3182,3300,3155,3733,3393,3752,3563,3264,2490,3640,3757,3114,2836,3110,3058,2777,1183,3102,3054,127,1182,655,27,42,50,55,67,45,52,51,54,41,47,48,13,44,4,16,9,18,7,10,11,15,8,12,6,5,17,2,14,72,64,77,46,65,25,3,22,23,81,88,115,24,57])). % 122.98/123.02 cnf(3987,plain, % 122.98/123.02 (~E(f13(f13(f6(f13(f2(a11))))),a1)), % 122.98/123.02 inference(scs_inference,[],[3460,3906,3338,2935,42,50,45,55,52,67,54,51,41])). % 122.98/123.02 cnf(3993,plain, % 122.98/123.02 (E(f3(x39931,f4(f8(a10),f8(a10))),f3(x39931,f4(a10,a10)))), % 122.98/123.02 inference(scs_inference,[],[3946,3460,3906,3338,2935,42,50,45,55,52,67,54,51,41,47,48,13])). % 122.98/123.02 cnf(3996,plain, % 122.98/123.02 (E(f7(x39961,f4(f8(a10),f8(a10))),f7(x39961,f4(a10,a10)))), % 122.98/123.02 inference(scs_inference,[],[3946,3460,3906,3338,2935,42,50,45,55,52,67,54,51,41,47,48,13,44,16])). % 122.98/123.02 cnf(3997,plain, % 122.98/123.02 (E(f12(f4(f8(a10),f8(a10))),f12(f4(a10,a10)))), % 122.98/123.02 inference(scs_inference,[],[3946,3460,3906,3338,2935,42,50,45,55,52,67,54,51,41,47,48,13,44,16,4])). % 122.98/123.02 cnf(3998,plain, % 122.98/123.02 (E(f8(f4(f8(a10),f8(a10))),f8(f4(a10,a10)))), % 122.98/123.02 inference(scs_inference,[],[3946,3460,3906,3338,2935,42,50,45,55,52,67,54,51,41,47,48,13,44,16,4,18])). % 122.98/123.02 cnf(3999,plain, % 122.98/123.02 (E(f5(x39991,f4(f8(a10),f8(a10))),f5(x39991,f4(a10,a10)))), % 122.98/123.02 inference(scs_inference,[],[3946,3460,3906,3338,2935,42,50,45,55,52,67,54,51,41,47,48,13,44,16,4,18,11])). % 122.98/123.02 cnf(4001,plain, % 122.98/123.02 (E(f9(f4(f8(a10),f8(a10)),x40011),f9(f4(a10,a10),x40011))), % 122.98/123.02 inference(scs_inference,[],[3946,3460,3906,3338,2935,42,50,45,55,52,67,54,51,41,47,48,13,44,16,4,18,11,9,7])). % 122.98/123.02 cnf(4002,plain, % 122.98/123.02 (E(f7(f4(f8(a10),f8(a10)),x40021),f7(f4(a10,a10),x40021))), % 122.98/123.02 inference(scs_inference,[],[3946,3460,3906,3338,2935,42,50,45,55,52,67,54,51,41,47,48,13,44,16,4,18,11,9,7,15])). % 122.98/123.02 cnf(4003,plain, % 122.98/123.02 (E(f5(f4(f8(a10),f8(a10)),x40031),f5(f4(a10,a10),x40031))), % 122.98/123.02 inference(scs_inference,[],[3946,3460,3906,3338,2935,42,50,45,55,52,67,54,51,41,47,48,13,44,16,4,18,11,9,7,15,10])). % 122.98/123.02 cnf(4004,plain, % 122.98/123.02 (E(f9(x40041,f4(f8(a10),f8(a10))),f9(x40041,f4(a10,a10)))), % 122.98/123.02 inference(scs_inference,[],[3946,3460,3906,3338,2935,42,50,45,55,52,67,54,51,41,47,48,13,44,16,4,18,11,9,7,15,10,8])). % 122.98/123.02 cnf(4008,plain, % 122.98/123.02 (E(f4(f4(f8(a10),f8(a10)),x40081),f4(f4(a10,a10),x40081))), % 122.98/123.02 inference(scs_inference,[],[3946,3460,3906,3338,2935,42,50,45,55,52,67,54,51,41,47,48,13,44,16,4,18,11,9,7,15,10,8,6,17,12,5])). % 122.98/123.02 cnf(4009,plain, % 122.98/123.02 (~E(a1,f13(f13(f13(f13(a1)))))), % 122.98/123.02 inference(scs_inference,[],[3946,3460,3906,3922,3338,2935,42,50,45,55,52,67,54,51,41,47,48,13,44,16,4,18,11,9,7,15,10,8,6,17,12,5,2])). % 122.98/123.02 cnf(4017,plain, % 122.98/123.02 (~E(f4(a10,a10),f9(f5(f12(a11),f12(a11)),f4(f3(a11,f2(a11)),f3(a11,f2(a11)))))), % 122.98/123.02 inference(scs_inference,[],[3946,3460,3906,3922,3944,3338,2935,32,42,50,45,55,52,67,54,51,41,47,48,13,44,16,4,18,11,9,7,15,10,8,6,17,12,5,2,14,66,64,65,3])). % 122.98/123.02 cnf(4021,plain, % 122.98/123.02 (~E(f13(a1),f13(f13(f2(f12(a11)))))), % 122.98/123.02 inference(scs_inference,[],[3946,3565,3817,2941,3460,3906,3922,3944,3338,3116,3757,2939,2935,26,109,32,42,50,45,55,52,67,54,51,41,47,48,13,44,16,4,18,11,9,7,15,10,8,6,17,12,5,2,14,66,64,65,3,24,22,23,57])). % 122.98/123.02 cnf(4033,plain, % 122.98/123.02 (P1(f13(f13(f6(f2(a11)))))), % 122.98/123.02 inference(scs_inference,[],[3149,42])). % 122.98/123.02 cnf(4049,plain, % 122.98/123.02 (~E(f13(f13(f6(f2(a11)))),a1)), % 122.98/123.02 inference(scs_inference,[],[3531,3022,3149,286,42,50,52,45,67,55,51,54,41])). % 122.98/123.02 cnf(4070,plain, % 122.98/123.02 (~E(f13(f13(f2(f12(a11)))),f13(a1))), % 122.98/123.02 inference(scs_inference,[],[3950,3531,4021,3022,3149,286,42,50,52,45,67,55,51,54,41,47,48,44,13,4,16,11,15,18,10,9,7,8,5,17,6,2])). % 122.98/123.02 cnf(4081,plain, % 122.98/123.02 (~E(f9(f5(f12(a11),f12(a11)),f4(f3(a11,f2(a11)),f3(a11,f2(a11)))),f4(f8(a10),f9(a10,f8(a10))))), % 122.98/123.02 inference(scs_inference,[],[3950,3261,3531,4021,3022,3218,3149,286,127,32,42,50,52,45,67,55,51,54,41,47,48,44,13,4,16,11,15,18,10,9,7,8,5,17,6,2,12,14,66,64,46,65,3])). % 122.98/123.02 cnf(4107,plain, % 122.98/123.02 (~E(f13(f13(f13(f6(f2(a11))))),a1)), % 122.98/123.02 inference(scs_inference,[],[3894,4033,3104,1182,42,50,67,52,55,45,54,51,41])). % 122.98/123.02 cnf(4137,plain, % 122.98/123.02 (~P5(f2(a11),f13(f6(f13(f2(f12(a11))))))), % 122.98/123.02 inference(scs_inference,[],[3993,3894,4033,4049,3104,2844,3757,1182,32,42,50,67,52,55,45,54,51,41,47,48,44,13,16,4,15,9,11,18,7,10,17,8,2,12,5,6,14,66,64,65,25])). % 122.98/123.02 cnf(4151,plain, % 122.98/123.02 (P1(f13(f13(f13(f13(a1)))))), % 122.98/123.02 inference(scs_inference,[],[3054,42])). % 122.98/123.02 cnf(4167,plain, % 122.98/123.02 (~E(f13(f13(f6(f13(a1)))),a1)), % 122.98/123.02 inference(scs_inference,[],[3606,3024,3245,2978,3054,726,42,50,67,52,45,55,51,54,41])). % 122.98/123.02 cnf(4187,plain, % 122.98/123.02 (~E(f13(f13(f13(f13(a1)))),f13(f13(a1)))), % 122.98/123.02 inference(scs_inference,[],[3996,3606,3966,3024,3245,2978,3054,726,42,50,67,52,45,55,51,54,41,47,48,44,13,16,4,15,11,9,7,18,10,17,12,5,2])). % 122.98/123.02 cnf(4191,plain, % 122.98/123.02 (P2(f3(f12(a11),f2(f12(a11))))), % 122.98/123.02 inference(scs_inference,[],[3996,3606,3966,3024,3245,2818,2978,3054,726,32,42,50,67,52,45,55,51,54,41,47,48,44,13,16,4,15,11,9,7,18,10,17,12,5,2,8,6,14,66])). % 122.98/123.02 cnf(4199,plain, % 122.98/123.02 (~E(f13(a1),f13(f13(a1)))), % 122.98/123.02 inference(scs_inference,[],[3996,3411,3606,3966,3024,3721,3245,2824,2818,2978,3054,726,32,42,50,67,52,45,55,51,54,41,47,48,44,13,16,4,15,11,9,7,18,10,17,12,5,2,8,6,14,66,46,64,65,3])). % 122.98/123.02 cnf(4201,plain, % 122.98/123.02 (P4(a10,f4(f3(f12(a11),f13(a1)),f3(a11,f13(a1))))), % 122.98/123.02 inference(scs_inference,[],[39,3996,3411,2915,3910,3606,3966,3024,3721,3245,3232,2824,2818,2978,3054,726,32,42,50,67,52,45,55,51,54,41,47,48,44,13,16,4,15,11,9,7,18,10,17,12,5,2,8,6,14,66,46,64,65,3,22,23])). % 122.98/123.02 cnf(4221,plain, % 122.98/123.02 (P4(f3(f12(a11),f2(f12(a11))),f3(f12(a11),f2(f12(a11))))), % 122.98/123.02 inference(scs_inference,[],[4191,4151,42,67,50,52])). % 122.98/123.02 cnf(4231,plain, % 122.98/123.02 (~E(f13(f13(f13(f13(f13(a1))))),a1)), % 122.98/123.02 inference(scs_inference,[],[4191,4151,42,67,50,52,55,45,54,51,41])). % 122.98/123.02 cnf(4237,plain, % 122.98/123.02 (P2(f8(f3(f12(a11),f2(f12(a11)))))), % 122.98/123.02 inference(scs_inference,[],[4191,4151,42,67,50,52,55,45,54,51,41,47,48,44])). % 122.98/123.02 cnf(4248,plain, % 122.98/123.02 (~E(a1,f13(f13(f6(f13(a1)))))), % 122.98/123.02 inference(scs_inference,[],[4191,3997,4151,4167,42,67,50,52,55,45,54,51,41,47,48,44,13,16,4,15,9,11,18,7,10,2])). % 122.98/123.02 cnf(4261,plain, % 122.98/123.02 (E(f8(f4(f8(a10),f8(a10))),f4(a10,f8(a10)))), % 122.98/123.02 inference(scs_inference,[],[4191,3997,3998,4151,4167,3183,32,42,67,50,52,55,45,54,51,41,47,48,44,13,16,4,15,9,11,18,7,10,2,8,5,17,12,6,14,66,64,65,3])). % 122.98/123.02 cnf(4274,plain, % 122.98/123.02 (P1(f13(f13(f2(a11))))), % 122.98/123.02 inference(scs_inference,[],[206,42])). % 122.98/123.02 cnf(4278,plain, % 122.98/123.02 (P4(a10,f4(f3(f12(a11),a1),f3(f12(a11),a1)))), % 122.98/123.02 inference(scs_inference,[],[3195,2836,206,42,50,67])). % 122.98/123.02 cnf(4280,plain, % 122.98/123.02 (E(f9(f8(f5(a11,a11)),f5(a11,a11)),a10)), % 122.98/123.02 inference(scs_inference,[],[3195,2836,206,160,42,50,67,55])). % 122.98/123.02 cnf(4284,plain, % 122.98/123.02 (E(f8(f8(f5(a11,a11))),f5(a11,a11))), % 122.98/123.02 inference(scs_inference,[],[4237,3195,2836,206,160,42,50,67,55,52,45])). % 122.98/123.02 cnf(4286,plain, % 122.98/123.02 (E(f9(f5(a11,a11),f8(f5(a11,a11))),a10)), % 122.98/123.02 inference(scs_inference,[],[4237,3195,2836,206,160,42,50,67,55,52,45,54])). % 122.98/123.02 cnf(4288,plain, % 122.98/123.02 (~E(f13(f13(f2(a11))),a1)), % 122.98/123.02 inference(scs_inference,[],[4237,3195,2836,206,160,42,50,67,55,52,45,54,41])). % 122.98/123.02 cnf(4309,plain, % 122.98/123.02 (~E(f9(f5(f12(a11),f12(a11)),f4(f3(a11,f2(a11)),f3(a11,f2(a11)))),f4(a10,a10))), % 122.98/123.02 inference(scs_inference,[],[3999,4237,4017,3195,2836,206,160,42,50,67,55,52,45,54,41,56,51,47,48,44,13,4,16,11,15,9,7,18,10,2])). % 122.98/123.02 cnf(4316,plain, % 122.98/123.02 (E(f13(f6(f13(f13(f2(a11))))),f13(f13(f2(a11))))), % 122.98/123.02 inference(scs_inference,[],[3999,4237,4017,3195,2836,206,160,42,50,67,55,52,45,54,41,56,51,47,48,44,13,4,16,11,15,9,7,18,10,2,5,17,12,8,6,14,49])). % 122.98/123.02 cnf(4318,plain, % 122.98/123.02 (P2(f3(f12(a11),f6(f13(a1))))), % 122.98/123.02 inference(scs_inference,[],[3999,4237,4017,3195,2822,2836,206,32,160,42,50,67,55,52,45,54,41,56,51,47,48,44,13,4,16,11,15,9,7,18,10,2,5,17,12,8,6,14,49,66])). % 122.98/123.02 cnf(4320,plain, % 122.98/123.02 (P1(f6(f13(f13(f2(a11)))))), % 122.98/123.02 inference(scs_inference,[],[3999,4237,4017,3195,2822,2836,206,32,160,42,50,67,55,52,45,54,41,56,51,47,48,44,13,4,16,11,15,9,7,18,10,2,5,17,12,8,6,14,49,66,46])). % 122.98/123.02 cnf(4327,plain, % 122.98/123.02 (~P5(f13(f6(f13(f2(f12(a11))))),f2(a11))), % 122.98/123.02 inference(scs_inference,[],[3999,4237,4017,4137,2998,2840,3195,3757,2822,2836,206,32,160,42,50,67,55,52,45,54,41,56,51,47,48,44,13,4,16,11,15,9,7,18,10,2,5,17,12,8,6,14,49,66,46,64,65,25,24])). % 122.98/123.02 cnf(4328,plain, % 122.98/123.02 (~E(f13(a1),f13(f6(f13(f13(a1)))))), % 122.98/123.02 inference(scs_inference,[],[4199,3999,4237,4017,4137,2998,2927,2840,3195,3757,2822,2836,206,32,160,42,50,67,55,52,45,54,41,56,51,47,48,44,13,4,16,11,15,9,7,18,10,2,5,17,12,8,6,14,49,66,46,64,65,25,24,3])). % 122.98/123.02 cnf(4331,plain, % 122.98/123.02 (E(f3(f12(a11),f13(f13(f2(a11)))),f3(a11,f13(f13(f2(a11)))))), % 122.98/123.02 inference(scs_inference,[],[39,4199,3999,4221,2896,2970,4237,4017,4137,2998,2927,2840,3195,3757,2822,2836,206,32,160,42,50,67,55,52,45,54,41,56,51,47,48,44,13,4,16,11,15,9,7,18,10,2,5,17,12,8,6,14,49,66,46,64,65,25,24,3,22,23,62])). % 122.98/123.02 cnf(4336,plain, % 122.98/123.02 (P4(a10,f4(f4(a10,f8(a10)),f4(a10,f8(a10))))), % 122.98/123.02 inference(scs_inference,[],[39,4199,3999,4221,2896,2970,4237,4187,4017,3416,4137,2998,2927,2840,4151,3195,3757,2822,2836,2891,587,206,32,160,582,42,50,67,55,52,45,54,41,56,51,47,48,44,13,4,16,11,15,9,7,18,10,2,5,17,12,8,6,14,49,66,46,64,65,25,24,3,22,23,62,19,57,82])). % 122.98/123.02 cnf(4338,plain, % 122.98/123.02 (~P4(f4(f8(f5(f12(a11),f12(a11))),f8(f5(f12(a11),f12(a11)))),f5(a11,a11))), % 122.98/123.02 inference(scs_inference,[],[39,4199,3999,4221,2896,2970,4237,4187,4017,3420,3388,3416,4137,2998,2927,2840,4151,3195,3757,2822,2836,2891,587,206,32,160,582,27,42,50,67,55,52,45,54,41,56,51,47,48,44,13,4,16,11,15,9,7,18,10,2,5,17,12,8,6,14,49,66,46,64,65,25,24,3,22,23,62,19,57,82,79])). % 122.98/123.02 cnf(4350,plain, % 122.98/123.02 (P1(f13(f13(f13(f2(a11)))))), % 122.98/123.02 inference(scs_inference,[],[4274,42])). % 122.98/123.02 cnf(4358,plain, % 122.98/123.02 (P4(f3(f12(a11),f6(f13(a1))),f3(f12(a11),f6(f13(a1))))), % 122.98/123.02 inference(scs_inference,[],[4318,4274,42,67,50,54,52])). % 122.98/123.02 cnf(4366,plain, % 122.98/123.02 (~E(f13(f13(f13(f2(a11)))),a1)), % 122.98/123.02 inference(scs_inference,[],[4318,4274,42,67,50,54,52,55,45,51,41])). % 122.98/123.02 cnf(4372,plain, % 122.98/123.02 (P2(f8(f3(f12(a11),f6(f13(a1)))))), % 122.98/123.02 inference(scs_inference,[],[4318,4274,42,67,50,54,52,55,45,51,41,47,48,44])). % 122.98/123.02 cnf(4374,plain, % 122.98/123.02 (E(f3(x43741,f9(f8(f5(a11,a11)),f5(a11,a11))),f3(x43741,a10))), % 122.98/123.02 inference(scs_inference,[],[4280,4318,4274,42,67,50,54,52,55,45,51,41,47,48,44,13])). % 122.98/123.02 cnf(4375,plain, % 122.98/123.02 (E(f7(f9(f8(f5(a11,a11)),f5(a11,a11)),x43751),f7(a10,x43751))), % 122.98/123.02 inference(scs_inference,[],[4280,4318,4274,42,67,50,54,52,55,45,51,41,47,48,44,13,15])). % 122.98/123.02 cnf(4376,plain, % 122.98/123.02 (E(f7(x43761,f9(f8(f5(a11,a11)),f5(a11,a11))),f7(x43761,a10))), % 122.98/123.02 inference(scs_inference,[],[4280,4318,4274,42,67,50,54,52,55,45,51,41,47,48,44,13,15,16])). % 122.98/123.02 cnf(4378,plain, % 122.98/123.02 (E(f5(x43781,f9(f8(f5(a11,a11)),f5(a11,a11))),f5(x43781,a10))), % 122.98/123.02 inference(scs_inference,[],[4280,4318,4274,42,67,50,54,52,55,45,51,41,47,48,44,13,15,16,4,11])). % 122.98/123.02 cnf(4380,plain, % 122.98/123.02 (E(f9(f9(f8(f5(a11,a11)),f5(a11,a11)),x43801),f9(a10,x43801))), % 122.98/123.02 inference(scs_inference,[],[4280,4318,4274,42,67,50,54,52,55,45,51,41,47,48,44,13,15,16,4,11,9,7])). % 122.98/123.02 cnf(4381,plain, % 122.98/123.02 (E(f8(f9(f8(f5(a11,a11)),f5(a11,a11))),f8(a10))), % 122.98/123.02 inference(scs_inference,[],[4280,4318,4274,42,67,50,54,52,55,45,51,41,47,48,44,13,15,16,4,11,9,7,18])). % 122.98/123.02 cnf(4382,plain, % 122.98/123.02 (E(f5(f9(f8(f5(a11,a11)),f5(a11,a11)),x43821),f5(a10,x43821))), % 122.98/123.02 inference(scs_inference,[],[4280,4318,4274,42,67,50,54,52,55,45,51,41,47,48,44,13,15,16,4,11,9,7,18,10])). % 122.98/123.02 cnf(4383,plain, % 122.98/123.02 (E(f4(f9(f8(f5(a11,a11)),f5(a11,a11)),x43831),f4(a10,x43831))), % 122.98/123.02 inference(scs_inference,[],[4280,4318,4274,42,67,50,54,52,55,45,51,41,47,48,44,13,15,16,4,11,9,7,18,10,5])). % 122.98/123.02 cnf(4385,plain, % 122.98/123.02 (~E(a1,f13(f13(f2(a11))))), % 122.98/123.02 inference(scs_inference,[],[4280,4318,4274,4288,42,67,50,54,52,55,45,51,41,47,48,44,13,15,16,4,11,9,7,18,10,5,17,2])). % 122.98/123.02 cnf(4386,plain, % 122.98/123.02 (E(f3(f9(f8(f5(a11,a11)),f5(a11,a11)),x43861),f3(a10,x43861))), % 122.98/123.02 inference(scs_inference,[],[4280,4318,4274,4288,42,67,50,54,52,55,45,51,41,47,48,44,13,15,16,4,11,9,7,18,10,5,17,2,12])). % 122.98/123.02 cnf(4387,plain, % 122.98/123.02 (E(f9(x43871,f9(f8(f5(a11,a11)),f5(a11,a11))),f9(x43871,a10))), % 122.98/123.02 inference(scs_inference,[],[4280,4318,4274,4288,42,67,50,54,52,55,45,51,41,47,48,44,13,15,16,4,11,9,7,18,10,5,17,2,12,8])). % 122.98/123.02 cnf(4388,plain, % 122.98/123.02 (E(f4(x43881,f9(f8(f5(a11,a11)),f5(a11,a11))),f4(x43881,a10))), % 122.98/123.02 inference(scs_inference,[],[4280,4318,4274,4288,42,67,50,54,52,55,45,51,41,47,48,44,13,15,16,4,11,9,7,18,10,5,17,2,12,8,6])). % 122.98/123.02 cnf(4390,plain, % 122.98/123.02 (P2(f3(f12(a11),f13(f13(f2(a11)))))), % 122.98/123.02 inference(scs_inference,[],[4280,4318,4274,4288,32,42,67,50,54,52,55,45,51,41,47,48,44,13,15,16,4,11,9,7,18,10,5,17,2,12,8,6,14,66])). % 122.98/123.02 cnf(4398,plain, % 122.98/123.02 (~P5(f13(f6(f13(f2(f12(a11))))),f13(f2(f12(a11))))), % 122.98/123.03 inference(scs_inference,[],[4280,4318,4274,4288,4327,36,32,42,67,50,54,52,55,45,51,41,47,48,44,13,15,16,4,11,9,7,18,10,5,17,2,12,8,6,14,66,46,64,65,25])). % 122.98/123.03 cnf(4399,plain, % 122.98/123.03 (E(f9(f8(f5(a11,a11)),f5(a11,a11)),f4(a10,f8(a10)))), % 122.98/123.03 inference(scs_inference,[],[4280,4318,4274,4288,4327,580,36,32,42,67,50,54,52,55,45,51,41,47,48,44,13,15,16,4,11,9,7,18,10,5,17,2,12,8,6,14,66,46,64,65,25,3])). % 122.98/123.03 cnf(4400,plain, % 122.98/123.03 (~P4(f9(f8(f5(a11,a11)),f5(a11,a11)),f5(a11,a11))), % 122.98/123.03 inference(scs_inference,[],[39,4280,4318,4274,4288,4327,580,36,32,42,67,50,54,52,55,45,51,41,47,48,44,13,15,16,4,11,9,7,18,10,5,17,2,12,8,6,14,66,46,64,65,25,3,22])). % 122.98/123.03 cnf(4402,plain, % 122.98/123.03 (~E(f13(f13(f13(f2(a11)))),f13(a1))), % 122.98/123.03 inference(scs_inference,[],[39,4280,4284,4318,4274,4288,4327,580,36,26,32,42,67,50,54,52,55,45,51,41,47,48,44,13,15,16,4,11,9,7,18,10,5,17,2,12,8,6,14,66,46,64,65,25,3,22,23,57])). % 122.98/123.03 cnf(4404,plain, % 122.98/123.03 (P4(f5(a11,a11),f4(f8(f5(f12(a11),f12(a11))),f8(f5(f12(a11),f12(a11)))))), % 122.98/123.03 inference(scs_inference,[],[39,4280,4284,4318,4274,4288,4338,4327,3420,580,36,26,32,160,42,67,50,54,52,55,45,51,41,47,48,44,13,15,16,4,11,9,7,18,10,5,17,2,12,8,6,14,66,46,64,65,25,3,22,23,57,63])). % 122.98/123.03 cnf(4406,plain, % 122.98/123.03 (~P4(f9(a10,f8(a10)),f9(f5(f12(a11),f12(a11)),f4(f3(a11,f2(a11)),f3(a11,f2(a11)))))), % 122.98/123.03 inference(scs_inference,[],[39,4280,4284,4318,4274,4288,4338,4327,3420,762,2866,580,36,157,726,26,32,160,42,67,50,54,52,55,45,51,41,47,48,44,13,15,16,4,11,9,7,18,10,5,17,2,12,8,6,14,66,46,64,65,25,3,22,23,57,63,79])). % 122.98/123.03 cnf(4418,plain, % 122.98/123.03 (P4(a10,f4(f8(f8(a10)),f8(f8(a10))))), % 122.98/123.03 inference(scs_inference,[],[4320,286,42,67])). % 122.98/123.03 cnf(4474,plain, % 122.98/123.03 (P4(f4(f8(a10),f8(a10)),f4(f8(a10),f8(a10)))), % 122.98/123.03 inference(scs_inference,[],[39,4399,4286,4385,4402,4358,3380,4372,4320,4406,4316,4398,2902,3157,3346,1183,461,3195,157,286,1182,726,32,449,142,140,152,42,67,50,55,45,54,52,51,41,47,48,44,13,15,16,4,11,9,18,10,7,5,17,12,2,8,14,6,66,64,65,3,24,22,23,63,81,88,82,89])). % 122.98/123.03 cnf(4480,plain, % 122.98/123.03 (P4(a10,f4(f9(a10,f8(a10)),f9(a10,f8(a10))))), % 122.98/123.03 inference(scs_inference,[],[4350,726,42,67])). % 122.98/123.03 cnf(4490,plain, % 122.98/123.03 (E(f9(f8(f4(a10,f8(a10))),f4(a10,f8(a10))),a10)), % 122.98/123.03 inference(scs_inference,[],[4390,4350,3272,726,582,42,67,54,52,45,50,55])). % 122.98/123.03 cnf(4496,plain, % 122.98/123.03 (~E(f13(f13(f13(f13(f2(a11))))),a1)), % 122.98/123.03 inference(scs_inference,[],[4390,4350,3272,726,582,42,67,54,52,45,50,55,51,47,41])). % 122.98/123.03 cnf(4512,plain, % 122.98/123.03 (~E(f13(f6(f13(f13(a1)))),f13(a1))), % 122.98/123.03 inference(scs_inference,[],[4374,4390,4350,4328,3272,726,582,42,67,54,52,45,50,55,51,47,41,48,44,13,15,16,4,10,9,11,18,7,5,2])). % 122.98/123.03 cnf(4522,plain, % 122.98/123.03 (P2(f3(a11,f13(f13(f2(a11)))))), % 122.98/123.03 inference(scs_inference,[],[4374,4390,4350,4328,4331,3272,726,32,582,42,67,54,52,45,50,55,51,47,41,48,44,13,15,16,4,10,9,11,18,7,5,2,17,12,8,6,14,66,64,20])). % 122.98/123.03 cnf(4526,plain, % 122.98/123.03 (E(f3(x45261,f9(f8(f5(a11,a11)),f5(a11,a11))),f3(x45261,a10))), % 122.98/123.03 inference(rename_variables,[],[4374])). % 122.98/123.03 cnf(4530,plain, % 122.98/123.03 (~P4(f9(f8(f5(a11,a11)),f5(a11,a11)),f8(f8(f5(a11,a11))))), % 122.98/123.03 inference(scs_inference,[],[4400,4374,4380,4386,4390,4350,4328,4331,4284,4406,3272,726,32,582,42,67,54,52,45,50,55,51,47,41,48,44,13,15,16,4,10,9,11,18,7,5,2,17,12,8,6,14,66,64,20,65,3,22,23])). % 122.98/123.03 cnf(4536,plain, % 122.98/123.03 (P4(a10,f9(f9(f8(f8(a10)),f8(a10)),f9(f8(f8(a10)),f8(a10))))), % 122.98/123.03 inference(scs_inference,[],[4400,4374,4526,4380,4386,4390,4350,4328,4404,4331,4284,4406,3420,167,3272,1187,1182,726,32,160,514,582,508,42,67,54,52,45,50,55,51,47,41,48,44,13,15,16,4,10,9,11,18,7,5,2,17,12,8,6,14,66,64,20,65,3,22,23,82,88,24,81])). % 122.98/123.03 cnf(4541,plain, % 122.98/123.03 (P4(a10,f4(f5(a11,a11),f5(a11,a11)))), % 122.98/123.03 inference(scs_inference,[],[160,67])). % 122.98/123.03 cnf(4551,plain, % 122.98/123.03 (E(f9(f8(f4(f8(a10),a10)),f4(f8(a10),a10)),a10)), % 122.98/123.03 inference(scs_inference,[],[4522,3110,160,508,67,54,45,50,52,55])). % 122.98/123.03 cnf(4579,plain, % 122.98/123.03 (P2(f3(f12(a11),f6(f13(f2(a11)))))), % 122.98/123.03 inference(scs_inference,[],[4375,4522,3425,3110,3102,32,160,508,67,54,45,50,52,55,51,47,48,44,13,15,4,9,11,18,10,16,7,2,5,12,17,8,6,14,64,66])). % 122.98/123.03 cnf(4583,plain, % 122.98/123.03 (~E(f13(f13(f2(f12(a11)))),f13(f6(f13(a1))))), % 122.98/123.03 inference(scs_inference,[],[4375,4070,4522,3425,3110,3102,2824,32,160,508,67,54,45,50,52,55,51,47,48,44,13,15,4,9,11,18,10,16,7,2,5,12,17,8,6,14,64,66,65,3])). % 122.98/123.03 cnf(4599,plain, % 122.98/123.03 (E(f9(f8(f9(f8(a10),a10)),f9(f8(a10),a10)),a10)), % 122.98/123.03 inference(scs_inference,[],[4579,655,67,45,52,54,55])). % 122.98/123.03 cnf(4636,plain, % 122.98/123.03 (~P4(f4(a10,f9(f3(a11,a1),f3(a11,a1))),f8(f8(f5(a11,a11))))), % 122.98/123.03 inference(scs_inference,[],[3771,4376,4383,4002,4579,4583,4284,3245,655,67,45,52,54,55,50,51,47,48,44,13,4,15,9,18,16,10,11,7,2,17,12,5,8,6,14,64,65,3,22,23])). % 122.98/123.03 cnf(4642,plain, % 122.98/123.03 (P4(a10,f4(a10,a10))), % 122.98/123.03 inference(scs_inference,[],[27,67])). % 122.98/123.03 cnf(4648,plain, % 122.98/123.03 (E(f8(f8(a10)),a10)), % 122.98/123.03 inference(scs_inference,[],[3738,2836,27,67,52,50,45])). % 122.98/123.03 cnf(4650,plain, % 122.98/123.03 (E(f9(f8(a10),a10),a10)), % 122.98/123.03 inference(scs_inference,[],[3738,2836,27,67,52,50,45,55])). % 122.98/123.03 cnf(4652,plain, % 122.98/123.03 (E(f9(a10,f8(a10)),a10)), % 122.98/123.03 inference(scs_inference,[],[3738,2836,27,67,52,50,45,55,54])). % 122.98/123.03 cnf(4654,plain, % 122.98/123.03 (E(f9(a10,f3(f12(a11),a1)),f3(f12(a11),a1))), % 122.98/123.03 inference(scs_inference,[],[3738,2836,27,67,52,50,45,55,54,51])). % 122.98/123.03 cnf(4678,plain, % 122.98/123.03 (P2(f9(f3(f12(a11),a1),f3(f12(a11),a1)))), % 122.98/123.03 inference(scs_inference,[],[4378,3738,3577,2836,27,67,52,50,45,55,54,51,47,48,44,13,15,4,9,10,18,16,7,11,2,17,6,14,5,8,12,64])). % 122.98/123.03 cnf(4680,plain, % 122.98/123.03 (P2(f3(f12(a11),f13(f6(f13(a1)))))), % 122.98/123.03 inference(scs_inference,[],[4378,3738,3577,2978,2836,32,27,67,52,50,45,55,54,51,47,48,44,13,15,4,9,10,18,16,7,11,2,17,6,14,5,8,12,64,66])). % 122.98/123.03 cnf(4682,plain, % 122.98/123.03 (P2(f4(f3(f12(a11),a1),f3(f12(a11),a1)))), % 122.98/123.03 inference(scs_inference,[],[4378,3738,3577,2978,2836,32,27,67,52,50,45,55,54,51,47,48,44,13,15,4,9,10,18,16,7,11,2,17,6,14,5,8,12,64,66,65])). % 122.98/123.03 cnf(4684,plain, % 122.98/123.03 (~E(f5(a11,a11),f4(a10,a10))), % 122.98/123.03 inference(scs_inference,[],[4378,3738,4309,3577,2978,2836,109,32,27,67,52,50,45,55,54,51,47,48,44,13,15,4,9,10,18,16,7,11,2,17,6,14,5,8,12,64,66,65,3])). % 122.98/123.03 cnf(4690,plain, % 122.98/123.03 (~E(f8(f8(a10)),f5(a11,a11))), % 122.98/123.03 inference(scs_inference,[],[39,4378,4278,4201,3141,2917,3738,4309,3577,2978,2836,109,32,27,67,52,50,45,55,54,51,47,48,44,13,15,4,9,10,18,16,7,11,2,17,6,14,5,8,12,64,66,65,3,22,23,82,290])). % 122.98/123.03 cnf(4691,plain, % 122.98/123.03 (~P4(f8(f8(a10)),f5(a11,a11))), % 122.98/123.03 inference(scs_inference,[],[39,4378,4278,4201,3141,2917,3738,4309,3577,2978,2836,109,32,27,67,52,50,45,55,54,51,47,48,44,13,15,4,9,10,18,16,7,11,2,17,6,14,5,8,12,64,66,65,3,22,23,82,290,291])). % 122.98/123.03 cnf(4693,plain, % 122.98/123.03 (E(f9(f3(f12(a11),a1),a10),f3(a11,a1))), % 122.98/123.03 inference(scs_inference,[],[39,4378,4278,4201,3141,2917,3738,4309,3577,2978,2836,109,32,27,67,52,50,45,55,54,51,47,48,44,13,15,4,9,10,18,16,7,11,2,17,6,14,5,8,12,64,66,65,3,22,23,82,290,291,293,115])). % 122.98/123.03 cnf(4694,plain, % 122.98/123.03 (~E(f13(f13(f13(f13(f2(a11))))),f13(a1))), % 122.98/123.03 inference(scs_inference,[],[39,4378,4278,4201,3141,2917,3738,4309,3577,4366,4350,2978,2836,26,109,32,27,67,52,50,45,55,54,51,47,48,44,13,15,4,9,10,18,16,7,11,2,17,6,14,5,8,12,64,66,65,3,22,23,82,290,291,293,115,57])). % 122.98/123.03 cnf(4702,plain, % 122.98/123.03 (E(f9(a10,f3(f12(a11),a1)),f3(a11,a1))), % 122.98/123.03 inference(scs_inference,[],[4654,115])). % 122.98/123.03 cnf(4715,plain, % 122.98/123.03 (P2(f8(f9(f3(f12(a11),a1),f3(f12(a11),a1))))), % 122.98/123.03 inference(scs_inference,[],[4654,4678,115,67,52,50,51,47,48,44])). % 122.98/123.03 cnf(4717,plain, % 122.98/123.03 (E(f3(x47171,f9(f8(a10),a10)),f3(x47171,a10))), % 122.98/123.03 inference(scs_inference,[],[4650,4654,4678,115,67,52,50,51,47,48,44,13])). % 122.98/123.03 cnf(4718,plain, % 122.98/123.03 (E(f7(f9(f8(a10),a10),x47181),f7(a10,x47181))), % 122.98/123.03 inference(scs_inference,[],[4650,4654,4678,115,67,52,50,51,47,48,44,13,15])). % 122.98/123.03 cnf(4719,plain, % 122.98/123.03 (E(f12(f9(f8(a10),a10)),f12(a10))), % 122.98/123.03 inference(scs_inference,[],[4650,4654,4678,115,67,52,50,51,47,48,44,13,15,4])). % 122.98/123.03 cnf(4720,plain, % 122.98/123.03 (E(f5(f9(f8(a10),a10),x47201),f5(a10,x47201))), % 122.98/123.03 inference(scs_inference,[],[4650,4654,4678,115,67,52,50,51,47,48,44,13,15,4,10])). % 122.98/123.03 cnf(4721,plain, % 122.98/123.03 (E(f8(f9(f8(a10),a10)),f8(a10))), % 122.98/123.03 inference(scs_inference,[],[4650,4654,4678,115,67,52,50,51,47,48,44,13,15,4,10,18])). % 122.98/123.03 cnf(4722,plain, % 122.98/123.03 (E(f2(f9(f8(a10),a10)),f2(a10))), % 122.98/123.03 inference(scs_inference,[],[4650,4654,4678,115,67,52,50,51,47,48,44,13,15,4,10,18,9])). % 122.98/123.03 cnf(4723,plain, % 122.98/123.03 (E(f7(x47231,f9(f8(a10),a10)),f7(x47231,a10))), % 122.98/123.03 inference(scs_inference,[],[4650,4654,4678,115,67,52,50,51,47,48,44,13,15,4,10,18,9,16])). % 122.98/123.03 cnf(4724,plain, % 122.98/123.03 (E(f5(x47241,f9(f8(a10),a10)),f5(x47241,a10))), % 122.98/123.03 inference(scs_inference,[],[4650,4654,4678,115,67,52,50,51,47,48,44,13,15,4,10,18,9,16,11])). % 122.98/123.03 cnf(4725,plain, % 122.98/123.03 (E(f9(f9(f8(a10),a10),x47251),f9(a10,x47251))), % 122.98/123.03 inference(scs_inference,[],[4650,4654,4678,115,67,52,50,51,47,48,44,13,15,4,10,18,9,16,11,7])). % 122.98/123.03 cnf(4726,plain, % 122.98/123.03 (~E(f4(a10,a10),f5(a11,a11))), % 122.98/123.03 inference(scs_inference,[],[4684,4650,4654,4678,115,67,52,50,51,47,48,44,13,15,4,10,18,9,16,11,7,2])). % 122.98/123.03 cnf(4727,plain, % 122.98/123.03 (E(f6(f9(f8(a10),a10)),f6(a10))), % 122.98/123.03 inference(scs_inference,[],[4684,4650,4654,4678,115,67,52,50,51,47,48,44,13,15,4,10,18,9,16,11,7,2,17])). % 122.98/123.03 cnf(4728,plain, % 122.98/123.03 (E(f4(f9(f8(a10),a10),x47281),f4(a10,x47281))), % 122.98/123.03 inference(scs_inference,[],[4684,4650,4654,4678,115,67,52,50,51,47,48,44,13,15,4,10,18,9,16,11,7,2,17,5])). % 122.98/123.03 cnf(4729,plain, % 122.98/123.03 (E(f13(f9(f8(a10),a10)),f13(a10))), % 122.98/123.03 inference(scs_inference,[],[4684,4650,4654,4678,115,67,52,50,51,47,48,44,13,15,4,10,18,9,16,11,7,2,17,5,14])). % 122.98/123.03 cnf(4730,plain, % 122.98/123.03 (E(f3(f9(f8(a10),a10),x47301),f3(a10,x47301))), % 122.98/123.03 inference(scs_inference,[],[4684,4650,4654,4678,115,67,52,50,51,47,48,44,13,15,4,10,18,9,16,11,7,2,17,5,14,12])). % 122.98/123.03 cnf(4731,plain, % 122.98/123.03 (E(f4(x47311,f9(f8(a10),a10)),f4(x47311,a10))), % 122.98/123.03 inference(scs_inference,[],[4684,4650,4654,4678,115,67,52,50,51,47,48,44,13,15,4,10,18,9,16,11,7,2,17,5,14,12,6])). % 122.98/123.03 cnf(4732,plain, % 122.98/123.03 (E(f9(x47321,f9(f8(a10),a10)),f9(x47321,a10))), % 122.98/123.03 inference(scs_inference,[],[4684,4650,4654,4678,115,67,52,50,51,47,48,44,13,15,4,10,18,9,16,11,7,2,17,5,14,12,6,8])). % 122.98/123.03 cnf(4740,plain, % 122.98/123.03 (~P4(f9(f8(a10),f9(f8(f5(a11,a11)),f5(a11,a11))),f5(a11,a11))), % 122.98/123.03 inference(scs_inference,[],[4684,4650,4382,4387,3005,4654,4678,687,115,67,52,50,51,47,48,44,13,15,4,10,18,9,16,11,7,2,17,5,14,12,6,8,64,65,3,22])). % 122.98/123.03 cnf(4742,plain, % 122.98/123.03 (~P4(f8(f8(a10)),f8(f8(f5(a11,a11))))), % 122.98/123.03 inference(scs_inference,[],[4684,4691,4650,4382,4387,3005,4654,4678,4284,687,115,67,52,50,51,47,48,44,13,15,4,10,18,9,16,11,7,2,17,5,14,12,6,8,64,65,3,22,23])). % 122.98/123.03 cnf(4743,plain, % 122.98/123.03 (~E(f13(f13(f6(f13(f13(a1))))),f13(f13(a1)))), % 122.98/123.03 inference(scs_inference,[],[4684,4691,4650,4382,4387,3005,4654,4678,4512,4284,687,2777,3218,115,67,52,50,51,47,48,44,13,15,4,10,18,9,16,11,7,2,17,5,14,12,6,8,64,65,3,22,23,57])). % 122.98/123.03 cnf(4749,plain, % 122.98/123.03 (~E(f8(f8(a10)),f8(f8(f5(a11,a11))))), % 122.98/123.03 inference(scs_inference,[],[4684,4691,4650,4382,4387,3005,4654,4678,4512,2873,4284,687,2777,167,3218,286,160,27,115,67,52,50,51,47,48,44,13,15,4,10,18,9,16,11,7,2,17,5,14,12,6,8,64,65,3,22,23,57,63,88,297])). % 122.98/123.03 cnf(4766,plain, % 122.98/123.03 (E(f3(x47661,f9(a10,f8(a10))),f3(x47661,a10))), % 122.98/123.03 inference(scs_inference,[],[4652,4680,4682,50,52,51,47,48,44,13])). % 122.98/123.03 cnf(4767,plain, % 122.98/123.03 (E(f12(f9(a10,f8(a10))),f12(a10))), % 122.98/123.03 inference(scs_inference,[],[4652,4680,4682,50,52,51,47,48,44,13,4])). % 122.98/123.03 cnf(4768,plain, % 122.98/123.03 (E(f7(f9(a10,f8(a10)),x47681),f7(a10,x47681))), % 122.98/123.03 inference(scs_inference,[],[4652,4680,4682,50,52,51,47,48,44,13,4,15])). % 122.98/123.03 cnf(4769,plain, % 122.98/123.03 (E(f5(f9(a10,f8(a10)),x47691),f5(a10,x47691))), % 122.98/123.03 inference(scs_inference,[],[4652,4680,4682,50,52,51,47,48,44,13,4,15,10])). % 122.98/123.03 cnf(4771,plain, % 122.98/123.03 (E(f8(f9(a10,f8(a10))),f8(a10))), % 122.98/123.03 inference(scs_inference,[],[4652,4680,4682,50,52,51,47,48,44,13,4,15,10,11,18])). % 122.98/123.03 cnf(4773,plain, % 122.98/123.03 (E(f2(f9(a10,f8(a10))),f2(a10))), % 122.98/123.03 inference(scs_inference,[],[4652,4680,4682,50,52,51,47,48,44,13,4,15,10,11,18,16,9])). % 122.98/123.03 cnf(4775,plain, % 122.98/123.03 (E(f6(f9(a10,f8(a10))),f6(a10))), % 122.98/123.03 inference(scs_inference,[],[4652,4680,4682,50,52,51,47,48,44,13,4,15,10,11,18,16,9,7,17])). % 122.98/123.03 cnf(4776,plain, % 122.98/123.03 (~E(f5(a11,a11),f8(f8(a10)))), % 122.98/123.03 inference(scs_inference,[],[4690,4652,4680,4682,50,52,51,47,48,44,13,4,15,10,11,18,16,9,7,17,2])). % 122.98/123.03 cnf(4778,plain, % 122.98/123.03 (E(f13(f9(a10,f8(a10))),f13(a10))), % 122.98/123.03 inference(scs_inference,[],[4690,4652,4680,4682,50,52,51,47,48,44,13,4,15,10,11,18,16,9,7,17,2,5,14])). % 122.98/123.03 cnf(4784,plain, % 122.98/123.03 (P2(f3(a11,f13(f6(f13(a1)))))), % 122.98/123.03 inference(scs_inference,[],[4690,4652,4680,3292,4682,50,52,51,47,48,44,13,4,15,10,11,18,16,9,7,17,2,5,14,8,6,12,64,20])). % 122.98/123.03 cnf(4787,plain, % 122.98/123.03 (~E(f4(a10,a10),f8(f8(f5(a11,a11))))), % 122.98/123.03 inference(scs_inference,[],[4726,4690,4652,4680,3292,4682,4284,50,52,51,47,48,44,13,4,15,10,11,18,16,9,7,17,2,5,14,8,6,12,64,20,65,3])). % 122.98/123.03 cnf(4788,plain, % 122.98/123.03 (~P4(f4(f9(f8(a10),a10),f3(f12(a11),f13(a1))),f5(a11,a11))), % 122.98/123.03 inference(scs_inference,[],[4726,4690,4652,3898,4728,4680,3292,4682,4284,50,52,51,47,48,44,13,4,15,10,11,18,16,9,7,17,2,5,14,8,6,12,64,20,65,3,22])). % 122.98/123.03 cnf(4800,plain, % 122.98/123.03 (E(f9(f4(f3(a11,a1),f3(a11,a1)),a10),f4(f3(a11,a1),f3(a11,a1)))), % 122.98/123.03 inference(scs_inference,[],[2935,50])). % 122.98/123.03 cnf(4804,plain, % 122.98/123.03 (E(f9(a10,f4(f3(a11,a1),f3(a11,a1))),f4(f3(a11,a1),f3(a11,a1)))), % 122.98/123.03 inference(scs_inference,[],[4784,2935,50,52,51])). % 122.98/123.03 cnf(4812,plain, % 122.98/123.03 (E(f3(x48121,f8(f8(a10))),f3(x48121,a10))), % 122.98/123.03 inference(scs_inference,[],[4648,4784,2935,50,52,51,47,48,44,13])). % 122.98/123.03 cnf(4813,plain, % 122.98/123.03 (E(f7(f8(f8(a10)),x48131),f7(a10,x48131))), % 122.98/123.03 inference(scs_inference,[],[4648,4784,2935,50,52,51,47,48,44,13,15])). % 122.98/123.03 cnf(4814,plain, % 122.98/123.03 (E(f12(f8(f8(a10))),f12(a10))), % 122.98/123.03 inference(scs_inference,[],[4648,4784,2935,50,52,51,47,48,44,13,15,4])). % 122.98/123.03 cnf(4815,plain, % 122.98/123.03 (E(f5(f8(f8(a10)),x48151),f5(a10,x48151))), % 122.98/123.03 inference(scs_inference,[],[4648,4784,2935,50,52,51,47,48,44,13,15,4,10])). % 122.98/123.03 cnf(4816,plain, % 122.98/123.03 (E(f5(x48161,f8(f8(a10))),f5(x48161,a10))), % 122.98/123.03 inference(scs_inference,[],[4648,4784,2935,50,52,51,47,48,44,13,15,4,10,11])). % 122.98/123.03 cnf(4817,plain, % 122.98/123.03 (E(f7(x48171,f8(f8(a10))),f7(x48171,a10))), % 122.98/123.03 inference(scs_inference,[],[4648,4784,2935,50,52,51,47,48,44,13,15,4,10,11,16])). % 122.98/123.03 cnf(4818,plain, % 122.98/123.03 (E(f2(f8(f8(a10))),f2(a10))), % 122.98/123.03 inference(scs_inference,[],[4648,4784,2935,50,52,51,47,48,44,13,15,4,10,11,16,9])). % 122.98/123.03 cnf(4820,plain, % 122.98/123.03 (E(f9(f8(f8(a10)),x48201),f9(a10,x48201))), % 122.98/123.03 inference(scs_inference,[],[4648,4693,4784,2935,50,52,51,47,48,44,13,15,4,10,11,16,9,18,7])). % 122.98/123.03 cnf(4822,plain, % 122.98/123.03 (E(f6(f8(f8(a10))),f6(a10))), % 122.98/123.03 inference(scs_inference,[],[4648,4693,4787,4784,2935,50,52,51,47,48,44,13,15,4,10,11,16,9,18,7,2,17])). % 122.98/123.03 cnf(4826,plain, % 122.98/123.03 (E(f13(f8(f8(a10))),f13(a10))), % 122.98/123.03 inference(scs_inference,[],[4648,4693,4787,4784,2935,50,52,51,47,48,44,13,15,4,10,11,16,9,18,7,2,17,6,5,8,14])). % 122.98/123.03 cnf(4827,plain, % 122.98/123.03 (E(f3(f8(f8(a10)),x48271),f3(a10,x48271))), % 122.98/123.03 inference(scs_inference,[],[4648,4693,4787,4784,2935,50,52,51,47,48,44,13,15,4,10,11,16,9,18,7,2,17,6,5,8,14,12])). % 122.98/123.03 cnf(4828,plain, % 122.98/123.03 (P2(f9(f4(f3(a11,a1),f3(a11,a1)),f4(f3(a11,a1),f3(a11,a1))))), % 122.98/123.03 inference(scs_inference,[],[4648,4693,4787,4784,2935,50,52,51,47,48,44,13,15,4,10,11,16,9,18,7,2,17,6,5,8,14,12,64])). % 122.98/123.03 cnf(4830,plain, % 122.98/123.03 (P2(f4(f4(f3(a11,a1),f3(a11,a1)),f4(f3(a11,a1),f3(a11,a1))))), % 122.98/123.03 inference(scs_inference,[],[4648,4693,4787,4784,2935,50,52,51,47,48,44,13,15,4,10,11,16,9,18,7,2,17,6,5,8,14,12,64,65])). % 122.98/123.03 cnf(4832,plain, % 122.98/123.03 (~E(a10,f8(f8(f5(a11,a11))))), % 122.98/123.03 inference(scs_inference,[],[4648,4693,4787,4749,4784,2935,50,52,51,47,48,44,13,15,4,10,11,16,9,18,7,2,17,6,5,8,14,12,64,65,3])). % 122.98/123.03 cnf(4854,plain, % 122.98/123.03 (P2(f8(f9(f4(f3(a11,a1),f3(a11,a1)),f4(f3(a11,a1),f3(a11,a1)))))), % 122.98/123.03 inference(scs_inference,[],[4828,50,52,51,47,48,44])). % 122.98/123.03 cnf(4876,plain, % 122.98/123.03 (~E(f9(f5(f12(a11),f12(a11)),f4(f3(a11,f2(a11)),f3(a11,f2(a11)))),f8(f8(a10)))), % 122.98/123.03 inference(scs_inference,[],[4776,4702,4832,4828,127,50,52,51,47,48,44,13,15,4,16,9,10,11,18,7,2,17,6,5,8,14,12,64,65,3])). % 122.98/123.03 cnf(4917,plain, % 122.98/123.03 (P2(f3(f12(a11),f13(f6(f2(a11)))))), % 122.98/123.03 inference(scs_inference,[],[4766,3804,4876,4830,3149,32,50,52,51,47,48,44,13,4,15,16,9,10,18,11,17,7,2,5,8,6,14,12,66])). % 122.98/123.03 cnf(4935,plain, % 122.98/123.03 (E(f9(f8(f8(a10)),a10),f8(f8(a10)))), % 122.98/123.03 inference(scs_inference,[],[286,50])). % 122.98/123.03 cnf(4939,plain, % 122.98/123.03 (E(f9(a10,f8(f8(a10))),f8(f8(a10)))), % 122.98/123.03 inference(scs_inference,[],[4917,286,50,52,51])). % 122.98/123.03 cnf(4963,plain, % 122.98/123.03 (P2(f9(f8(f8(a10)),f8(f8(a10))))), % 122.98/123.03 inference(scs_inference,[],[4768,4917,4694,286,50,52,51,47,48,44,13,4,16,15,10,11,9,18,17,7,8,6,2,5,12,14,64])). % 122.98/123.03 cnf(4965,plain, % 122.98/123.03 (P2(f4(f8(f8(a10)),f8(f8(a10))))), % 122.98/123.03 inference(scs_inference,[],[4768,4917,4694,286,50,52,51,47,48,44,13,4,16,15,10,11,9,18,17,7,8,6,2,5,12,14,64,65])). % 122.98/123.03 cnf(4978,plain, % 122.98/123.03 (~E(f13(f13(f13(f6(f2(a11))))),f13(a1))), % 122.98/123.03 inference(scs_inference,[],[39,4768,4732,4418,3220,4917,3624,4694,3644,3666,2951,4049,4033,167,286,26,109,160,508,50,52,51,47,48,44,13,4,16,15,10,11,9,18,17,7,8,6,2,5,12,14,64,65,3,22,23,82,88,67,19,57])). % 122.98/123.03 cnf(5000,plain, % 122.98/123.03 (P4(f4(f8(f8(a10)),f8(f8(a10))),f4(f8(f8(a10)),f8(f8(a10))))), % 122.98/123.03 inference(scs_inference,[],[4963,4965,50,52])). % 122.98/123.03 cnf(5008,plain, % 122.98/123.03 (P2(f8(f9(f8(f8(a10)),f8(f8(a10)))))), % 122.98/123.03 inference(scs_inference,[],[4963,4965,50,52,51,47,48,44])). % 122.98/123.03 cnf(5026,plain, % 122.98/123.03 (P2(f9(a10,f8(f8(a10))))), % 122.98/123.03 inference(scs_inference,[],[4769,4820,4963,4965,4978,50,52,51,47,48,44,13,4,16,11,10,9,15,17,18,7,8,2,6,12,14,5,20])). % 122.98/123.03 cnf(5054,plain, % 122.98/123.03 (P4(f9(a10,f8(f8(a10))),f9(a10,f8(f8(a10))))), % 122.98/123.03 inference(scs_inference,[],[5026,50,52])). % 122.98/123.03 cnf(5062,plain, % 122.98/123.03 (P2(f8(f9(a10,f8(f8(a10)))))), % 122.98/123.03 inference(scs_inference,[],[5026,50,52,51,47,48,44])). % 122.98/123.03 cnf(5134,plain, % 122.98/123.03 (P2(f3(f12(a11),f13(f13(f13(a1)))))), % 122.98/123.03 inference(scs_inference,[],[4717,4725,4730,4788,5062,3447,4965,4406,4284,3054,32,142,140,50,52,51,48,47,44,13,4,16,10,11,9,15,17,18,7,8,2,14,12,6,5,64,65,3,22,23,88,66])). % 122.98/123.03 cnf(5168,plain, % 122.98/123.03 (P2(f9(f9(f8(f8(a10)),f8(a10)),f9(f8(f8(a10)),f8(a10))))), % 122.98/123.03 inference(scs_inference,[],[4718,5134,3508,1182,50,52,51,47,48,44,13,4,16,10,9,17,11,15,18,7,8,2,14,12,6,5,64])). % 122.98/123.03 cnf(5170,plain, % 122.98/123.03 (P2(f4(f9(f8(f8(a10)),f8(a10)),f9(f8(f8(a10)),f8(a10))))), % 122.98/123.03 inference(scs_inference,[],[4718,5134,3508,1182,50,52,51,47,48,44,13,4,16,10,9,17,11,15,18,7,8,2,14,12,6,5,64,65])). % 122.98/123.03 cnf(5172,plain, % 122.98/123.03 (~E(f9(f5(f12(a11),f12(a11)),f4(f3(a11,f2(a11)),f3(a11,f2(a11)))),f9(f8(f8(a10)),f8(a10)))), % 122.98/123.03 inference(scs_inference,[],[4718,5134,3508,1181,127,1182,50,52,51,47,48,44,13,4,16,10,9,17,11,15,18,7,8,2,14,12,6,5,64,65,3])). % 122.98/123.03 cnf(5222,plain, % 122.98/123.03 (~E(f9(f8(f8(a10)),f8(a10)),f9(f5(f12(a11),f12(a11)),f4(f3(a11,f2(a11)),f3(a11,f2(a11)))))), % 122.98/123.03 inference(scs_inference,[],[4720,5168,5172,3348,726,50,52,51,48,47,44,13,4,16,9,10,15,11,17,18,7,2])). % 122.98/123.03 cnf(5228,plain, % 122.98/123.03 (P2(f9(f9(a10,f8(a10)),f9(a10,f8(a10))))), % 122.98/123.03 inference(scs_inference,[],[4720,5168,5172,3348,726,50,52,51,48,47,44,13,4,16,9,10,15,11,17,18,7,2,8,14,12,6,5,64])). % 122.98/123.03 cnf(5230,plain, % 122.98/123.03 (P2(f4(f9(a10,f8(a10)),f9(a10,f8(a10))))), % 122.98/123.03 inference(scs_inference,[],[4720,5168,5172,3348,726,50,52,51,48,47,44,13,4,16,9,10,15,11,17,18,7,2,8,14,12,6,5,64,65])). % 122.98/123.03 cnf(5248,plain, % 122.98/123.03 (P4(f5(a11,a11),f9(f9(f8(f8(a10)),f8(a10)),f9(f8(f8(a10)),f8(a10))))), % 122.98/123.03 inference(scs_inference,[],[39,4720,4724,4731,4740,5168,4536,3203,5172,2506,4480,3348,3018,1119,4284,1114,726,160,508,27,50,52,51,48,47,44,13,4,16,9,10,15,11,17,18,7,2,8,14,12,6,5,64,65,3,22,23,81,79,89,67,46,63])). % 122.98/123.03 cnf(5252,plain, % 122.98/123.03 (~E(f9(f9(f8(f8(a10)),f8(a10)),f9(f8(f8(a10)),f8(a10))),x52521)+P2(x52521)), % 122.98/123.03 inference(scs_inference,[],[39,4720,4724,4731,4740,5168,4536,3203,5172,2506,4480,3348,3018,1119,4284,1114,726,160,508,27,50,52,51,48,47,44,13,4,16,9,10,15,11,17,18,7,2,8,14,12,6,5,64,65,3,22,23,81,79,89,67,46,63,82,20])). % 122.98/123.03 cnf(5264,plain, % 122.98/123.03 (P2(f8(f9(f9(a10,f8(a10)),f9(a10,f8(a10)))))), % 122.98/123.03 inference(scs_inference,[],[5228,5230,50,52,51,48,47,44])). % 122.98/123.03 cnf(5286,plain, % 122.98/123.03 (~E(f9(a10,f8(a10)),f9(f5(f12(a11),f12(a11)),f4(f3(a11,f2(a11)),f3(a11,f2(a11)))))), % 122.98/123.03 inference(scs_inference,[],[4723,5228,5230,5222,3793,4820,50,52,51,48,47,44,13,4,10,16,9,15,17,18,11,7,8,2,14,12,6,5,64,65,3])). % 122.98/123.03 cnf(5337,plain, % 122.98/123.03 (~P4(f8(f9(f8(a10),a10)),f5(a11,a11))), % 122.98/123.03 inference(scs_inference,[],[4812,4827,4721,5170,5286,5230,169,4830,50,52,51,48,47,44,13,9,4,16,10,15,18,17,7,11,8,12,2,14,6,5,64,65,3,22])). % 122.98/123.03 cnf(5355,plain, % 122.98/123.03 (E(f9(f5(a11,a11),a10),f5(a11,a11))), % 122.98/123.03 inference(scs_inference,[],[4682,160,52,50])). % 122.98/123.03 cnf(5357,plain, % 122.98/123.03 (E(f9(a10,f5(a11,a11)),f5(a11,a11))), % 122.98/123.03 inference(scs_inference,[],[4682,160,52,50,51])). % 122.98/123.03 cnf(5381,plain, % 122.98/123.03 (P2(f9(f5(a11,a11),f5(a11,a11)))), % 122.98/123.03 inference(scs_inference,[],[4813,3867,3585,4682,160,52,50,51,48,47,44,13,4,10,9,16,18,17,15,7,11,8,2,12,14,6,5,64])). % 122.98/123.03 cnf(5383,plain, % 122.98/123.03 (P2(f4(f5(a11,a11),f5(a11,a11)))), % 122.98/123.03 inference(scs_inference,[],[4813,3867,3585,4682,160,52,50,51,48,47,44,13,4,10,9,16,18,17,15,7,11,8,2,12,14,6,5,64,65])). % 122.98/123.03 cnf(5396,plain, % 122.98/123.03 (E(f9(f8(f9(f5(a11,a11),f5(a11,a11))),f9(f5(a11,a11),f5(a11,a11))),a10)), % 122.98/123.03 inference(scs_inference,[],[39,4541,4813,4939,5248,4490,3867,3585,450,5054,3041,4682,5168,167,4830,127,160,52,50,51,48,47,44,13,4,10,9,16,18,17,15,7,11,8,2,12,14,6,5,64,65,3,22,23,82,81,88,45,55])). % 122.98/123.03 cnf(5406,plain, % 122.98/123.03 (P2(f3(f12(a11),f13(f2(a11))))), % 122.98/123.03 inference(scs_inference,[],[39,4541,4813,4939,5248,4490,3867,3585,450,5054,3041,4682,5168,167,4830,127,206,32,160,52,50,51,48,47,44,13,4,10,9,16,18,17,15,7,11,8,2,12,14,6,5,64,65,3,22,23,82,81,88,45,55,54,67,72,77,66])). % 122.98/123.03 cnf(5412,plain, % 122.98/123.03 (P2(f3(a11,f13(f2(a11))))), % 122.98/123.03 inference(scs_inference,[],[39,4541,4813,4939,5248,4490,3867,3585,450,1834,5054,3041,583,4682,3024,5168,167,4830,127,206,32,160,514,582,508,52,50,51,48,47,44,13,4,10,9,16,18,17,15,7,11,8,2,12,14,6,5,64,65,3,22,23,82,81,88,45,55,54,67,72,77,66,63,89,210])). % 122.98/123.03 cnf(5416,plain, % 122.98/123.03 (E(f9(f8(f4(f5(a11,a11),f5(a11,a11))),f4(f5(a11,a11),f5(a11,a11))),a10)), % 122.98/123.03 inference(scs_inference,[],[5383,45,55])). % 122.98/123.03 cnf(5428,plain, % 122.98/123.03 (E(f4(a10,f9(f5(a11,a11),f5(a11,a11))),a10)), % 122.98/123.03 inference(scs_inference,[],[5381,5383,5406,45,55,54,67,52,50,51,48])). % 122.98/123.03 cnf(5430,plain, % 122.98/123.03 (E(f4(f9(f5(a11,a11),f5(a11,a11)),a10),a10)), % 122.98/123.03 inference(scs_inference,[],[5381,5383,5406,45,55,54,67,52,50,51,48,47])). % 122.98/123.03 cnf(5432,plain, % 122.98/123.03 (P2(f8(f9(f5(a11,a11),f5(a11,a11))))), % 122.98/123.03 inference(scs_inference,[],[5381,5383,5406,45,55,54,67,52,50,51,48,47,44])). % 122.98/123.03 cnf(5442,plain, % 122.98/123.03 (E(f9(f9(f5(a11,a11),a10),x54421),f9(f5(a11,a11),x54421))), % 122.98/123.03 inference(scs_inference,[],[5355,5381,5383,5406,45,55,54,67,52,50,51,48,47,44,13,4,10,16,9,17,18,15,7])). % 122.98/123.03 cnf(5443,plain, % 122.98/123.03 (E(f5(x54431,f9(f5(a11,a11),a10)),f5(x54431,f5(a11,a11)))), % 122.98/123.03 inference(scs_inference,[],[5355,5381,5383,5406,45,55,54,67,52,50,51,48,47,44,13,4,10,16,9,17,18,15,7,11])). % 122.98/123.03 cnf(5445,plain, % 122.98/123.03 (E(f9(x54451,f9(f5(a11,a11),a10)),f9(x54451,f5(a11,a11)))), % 122.98/123.03 inference(scs_inference,[],[5355,5381,5383,5406,3656,45,55,54,67,52,50,51,48,47,44,13,4,10,16,9,17,18,15,7,11,2,8])). % 122.98/123.03 cnf(5454,plain, % 122.98/123.03 (P2(f9(f9(f5(a11,a11),f5(a11,a11)),f9(f5(a11,a11),f5(a11,a11))))), % 122.98/123.03 inference(scs_inference,[],[5355,5381,5383,5406,3656,45,55,54,67,52,50,51,48,47,44,13,4,10,16,9,17,18,15,7,11,2,8,12,14,6,5,72,77,64])). % 122.98/123.03 cnf(5456,plain, % 122.98/123.03 (P2(f4(f9(f5(a11,a11),f5(a11,a11)),f9(f5(a11,a11),f5(a11,a11))))), % 122.98/123.03 inference(scs_inference,[],[5355,5381,5383,5406,3656,45,55,54,67,52,50,51,48,47,44,13,4,10,16,9,17,18,15,7,11,2,8,12,14,6,5,72,77,64,65])). % 122.98/123.03 cnf(5460,plain, % 122.98/123.03 (~P4(a10,f9(f5(a11,a11),a10))), % 122.98/123.03 inference(scs_inference,[],[39,5355,5381,5383,4771,5406,3656,169,127,45,55,54,67,52,50,51,48,47,44,13,4,10,16,9,17,18,15,7,11,2,8,12,14,6,5,72,77,64,65,3,22,23])). % 122.98/123.03 cnf(5498,plain, % 122.98/123.03 (P2(f8(f8(f9(f5(a11,a11),f5(a11,a11)))))), % 122.98/123.03 inference(scs_inference,[],[5432,45,55,54,67,50,52,51,47,48,44])). % 122.98/123.03 cnf(5509,plain, % 122.98/123.03 (E(f9(f9(a10,f5(a11,a11)),x55091),f9(f5(a11,a11),x55091))), % 122.98/123.03 inference(scs_inference,[],[5357,5432,45,55,54,67,50,52,51,47,48,44,13,10,4,9,17,16,18,15,11,7])). % 122.98/123.03 cnf(5511,plain, % 122.98/123.03 (E(f9(x55111,f9(a10,f5(a11,a11))),f9(x55111,f5(a11,a11)))), % 122.98/123.03 inference(scs_inference,[],[5357,5432,3860,45,55,54,67,50,52,51,47,48,44,13,10,4,9,17,16,18,15,11,7,2,8])). % 122.98/123.03 cnf(5521,plain, % 122.98/123.03 (~P4(f4(a10,f9(f5(a11,a11),f5(a11,a11))),f5(a11,a11))), % 122.98/123.03 inference(scs_inference,[],[39,5357,5432,5428,3860,1113,127,45,55,54,67,50,52,51,47,48,44,13,10,4,9,17,16,18,15,11,7,2,8,14,12,6,5,64,65,3,22])). % 122.98/123.03 cnf(5522,plain, % 122.98/123.03 (~P4(a10,f9(a10,f5(a11,a11)))), % 122.98/123.03 inference(scs_inference,[],[39,5357,5432,5428,3860,1113,127,45,55,54,67,50,52,51,47,48,44,13,10,4,9,17,16,18,15,11,7,2,8,14,12,6,5,64,65,3,22,23])). % 122.98/123.03 cnf(5550,plain, % 122.98/123.03 (P2(f8(f4(f9(f5(a11,a11),f5(a11,a11)),f9(f5(a11,a11),f5(a11,a11)))))), % 122.98/123.03 inference(scs_inference,[],[5456,5412,45,55,54,67,50,52,51,47,48,44])). % 122.98/123.03 cnf(5575,plain, % 122.98/123.03 (~P4(f4(f9(f5(a11,a11),f5(a11,a11)),a10),f5(a11,a11))), % 122.98/123.03 inference(scs_inference,[],[39,4815,4816,5430,5456,3987,5412,45,55,54,67,50,52,51,47,48,44,13,10,4,17,9,11,16,18,15,7,14,2,8,12,6,5,64,65,3,22])). % 122.98/123.03 cnf(5576,plain, % 122.98/123.03 (~P4(a10,f9(a10,f9(f5(a11,a11),a10)))), % 122.98/123.03 inference(scs_inference,[],[39,5522,4815,4816,5430,5445,5456,3987,5412,45,55,54,67,50,52,51,47,48,44,13,10,4,17,9,11,16,18,15,7,14,2,8,12,6,5,64,65,3,22,23])). % 122.98/123.03 cnf(5633,plain, % 122.98/123.03 (~P4(a10,f9(f9(f5(a11,a11),a10),a10))), % 122.98/123.03 inference(scs_inference,[],[39,4817,5442,4551,5498,4107,5454,507,5460,5406,127,45,55,54,67,50,52,51,48,47,44,13,10,4,11,17,18,9,16,7,15,14,8,2,12,6,5,64,65,3,22,23])). % 122.98/123.03 cnf(5637,plain, % 122.98/123.03 (~E(f13(f13(f6(f13(f2(a11))))),f13(a1))), % 122.98/123.03 inference(scs_inference,[],[39,4817,5442,4551,5498,4107,5454,507,5460,5406,3752,4541,3906,5383,127,26,45,55,54,67,50,52,51,48,47,44,13,10,4,11,17,18,9,16,7,15,14,8,2,12,6,5,64,65,3,22,23,81,57])). % 122.98/123.03 cnf(5677,plain, % 122.98/123.03 (E(f4(x56771,f9(f8(f5(a11,a11)),f5(a11,a11))),f4(x56771,a10))), % 122.98/123.03 inference(rename_variables,[],[4388])). % 122.98/123.03 cnf(5679,plain, % 122.98/123.03 (~P4(f4(f9(f5(a11,a11),f5(a11,a11)),f9(f8(f5(a11,a11)),f5(a11,a11))),f5(a11,a11))), % 122.98/123.03 inference(scs_inference,[],[5575,4767,4388,5677,4008,4715,5637,5412,67,50,52,51,48,47,44,13,10,4,17,18,9,11,16,7,15,14,12,2,8,6,5,64,65,3,22])). % 122.98/123.03 cnf(5682,plain, % 122.98/123.03 (~E(f13(a1),f13(f13(f13(f13(f13(a1))))))), % 122.98/123.03 inference(scs_inference,[],[5337,5575,4767,4388,5677,4008,4009,4715,5637,5412,4151,4284,26,67,50,52,51,48,47,44,13,10,4,17,18,9,11,16,7,15,14,12,2,8,6,5,64,65,3,22,23,57])). % 122.98/123.03 cnf(5716,plain, % 122.98/123.03 (~E(f9(a10,a10),f8(f8(f5(a11,a11))))), % 122.98/123.03 inference(scs_inference,[],[39,4775,4599,4854,4231,318,5406,4284,4,9,17,16,6,18,50,13,51,11,52,7,5,15,44,14,48,47,12,2,8,10,22,3])). % 122.98/123.03 cnf(5717,plain, % 122.98/123.03 (~P4(a10,f9(f9(a10,f5(a11,a11)),a10))), % 122.98/123.03 inference(scs_inference,[],[39,4775,5509,4599,4854,4231,318,5460,5406,4284,4,9,17,16,6,18,50,13,51,11,52,7,5,15,44,14,48,47,12,2,8,10,22,3,23])). % 122.98/123.03 cnf(5757,plain, % 122.98/123.03 (P2(f4(f4(f5(a11,a11),f5(a11,a11)),f4(f5(a11,a11),f5(a11,a11))))), % 122.98/123.03 inference(scs_inference,[],[4719,5716,4381,5008,2546,169,3346,5383,4,6,50,9,17,16,52,13,51,11,18,7,44,48,14,15,5,8,47,12,10,2,22,3,65])). % 122.98/123.03 cnf(5760,plain, % 122.98/123.03 (P2(f9(f4(f5(a11,a11),f5(a11,a11)),f4(f5(a11,a11),f5(a11,a11))))), % 122.98/123.03 inference(scs_inference,[],[5521,4719,5716,4381,5008,2546,169,3346,5383,4284,4,6,50,9,17,16,52,13,51,11,18,7,44,48,14,15,5,8,47,12,10,2,22,3,65,23,64])). % 122.98/123.03 cnf(5764,plain, % 122.98/123.03 (~E(f8(f9(f8(f8(a10)),f8(f8(a10)))),x57641)+P2(x57641)), % 122.98/123.03 inference(scs_inference,[],[5521,4719,5716,4381,5008,2546,169,3346,5383,4284,4,6,50,9,17,16,52,13,51,11,18,7,44,48,14,15,5,8,47,12,10,2,22,3,65,23,64,67,20])). % 122.98/123.03 cnf(5792,plain, % 122.98/123.03 (P2(f8(f4(f4(f5(a11,a11),f5(a11,a11)),f4(f5(a11,a11),f5(a11,a11)))))), % 122.98/123.03 inference(scs_inference,[],[4727,5757,3272,4,6,50,17,9,16,52,51,13,11,18,7,44])). % 122.98/123.03 cnf(5811,plain, % 122.98/123.03 (~P4(a10,f9(a10,f9(a10,f5(a11,a11))))), % 122.98/123.03 inference(scs_inference,[],[4727,5576,5511,5757,5760,5396,4496,3011,5522,2927,3272,4,6,50,17,9,16,52,51,13,11,18,7,44,48,14,5,15,67,47,8,12,10,2,22,3,65,23])). % 122.98/123.03 cnf(5851,plain, % 122.98/123.03 (~P4(f8(f4(f8(a10),f8(a10))),f5(a11,a11))), % 122.98/123.03 inference(scs_inference,[],[4814,4261,5264,5682,5760,3110,599,4,6,50,17,16,9,52,51,13,11,18,7,44,48,14,15,5,47,8,12,10,2,22])). % 122.98/123.03 cnf(5852,plain, % 122.98/123.03 (E(f9(f4(f8(a10),f8(a10)),f4(f8(a10),f8(a10))),f9(f4(a10,a10),f4(a10,a10)))), % 122.98/123.03 inference(scs_inference,[],[4814,4001,4004,4261,5264,5682,5760,3110,599,4,6,50,17,16,9,52,51,13,11,18,7,44,48,14,15,5,47,8,12,10,2,22,3])). % 122.98/123.03 cnf(5857,plain, % 122.98/123.03 (~P4(a10,f9(f9(f5(a11,a11),a10),f4(f8(f3(a11,a1)),a10)))), % 122.98/123.03 inference(scs_inference,[],[4814,5633,4001,4004,4261,3545,5264,5682,5760,3110,599,4,6,50,17,16,9,52,51,13,11,18,7,44,48,14,15,5,47,8,12,10,2,22,3,65,23])). % 122.98/123.03 cnf(5897,plain, % 122.98/123.03 (~E(f9(f5(f12(a11),f12(a11)),f4(f3(a11,f2(a11)),f3(a11,f2(a11)))),f8(f4(f8(a10),f8(a10))))), % 122.98/123.03 inference(scs_inference,[],[5851,4818,5550,4743,2866,3195,449,4,50,6,17,9,16,52,51,13,11,18,7,44,48,14,5,15,47,8,12,10,2,22])). % 122.98/123.03 cnf(5940,plain, % 122.98/123.03 (P2(f4(f4(a10,f8(a10)),f4(a10,f8(a10))))), % 122.98/123.03 inference(scs_inference,[],[4822,4003,4800,5443,5792,3957,3131,3245,582,4,50,6,17,16,52,9,51,11,13,18,7,44,48,14,5,15,47,8,12,10,2,22,3,65])). % 122.98/123.03 cnf(5942,plain, % 122.98/123.03 (~P4(a10,f9(f9(a10,f5(a11,a11)),f4(a10,f8(f3(a11,a1)))))), % 122.98/123.03 inference(scs_inference,[],[4822,5717,4003,4800,5443,3619,5792,3957,3131,3245,582,4,50,6,17,16,52,9,51,11,13,18,7,44,48,14,5,15,47,8,12,10,2,22,3,65,23])). % 122.98/123.03 cnf(5944,plain, % 122.98/123.03 (P2(f9(f4(a10,f8(a10)),f4(a10,f8(a10))))), % 122.98/123.03 inference(scs_inference,[],[4822,5717,4003,4800,5443,3619,5792,3957,3131,3245,582,4,50,6,17,16,52,9,51,11,13,18,7,44,48,14,5,15,47,8,12,10,2,22,3,65,23,64])). % 122.98/123.03 cnf(5946,plain, % 122.98/123.03 (~E(f13(f13(f13(f2(f12(a11))))),f13(f13(a1)))), % 122.98/123.03 inference(scs_inference,[],[4822,5717,4003,4800,5443,3619,5792,3957,4070,3131,3304,2777,3245,582,4,50,6,17,16,52,9,51,11,13,18,7,44,48,14,5,15,47,8,12,10,2,22,3,65,23,64,57])). % 122.98/123.03 cnf(5969,plain, % 122.98/123.03 (P2(f8(f4(f4(a10,f8(a10)),f4(a10,f8(a10)))))), % 122.98/123.03 inference(scs_inference,[],[4826,5940,2836,4,50,6,17,16,52,9,51,11,13,18,7,44])). % 122.98/123.03 cnf(5984,plain, % 122.98/123.03 (~P4(f9(f8(f4(f5(a11,a11),f5(a11,a11))),f4(f5(a11,a11),f5(a11,a11))),f9(a10,f9(a10,f5(a11,a11))))), % 122.98/123.03 inference(scs_inference,[],[4826,5811,5940,5944,5416,5946,2836,4,50,6,17,16,52,9,51,11,13,18,7,44,48,14,67,15,5,47,8,12,10,2,22])). % 122.98/123.03 cnf(5985,plain, % 122.98/123.03 (~E(f5(a11,a11),f8(f4(f8(a10),f8(a10))))), % 122.98/123.03 inference(scs_inference,[],[4826,5811,5940,5944,5416,5946,5897,2836,109,4,50,6,17,16,52,9,51,11,13,18,7,44,48,14,67,15,5,47,8,12,10,2,22,3])). % 122.98/123.03 cnf(5991,plain, % 122.98/123.03 (~E(f13(a1),f13(f13(f13(f6(f13(a1))))))), % 122.98/123.03 inference(scs_inference,[],[26,4826,5811,5940,5944,3759,5416,4248,5000,5946,5897,3721,2836,109,4,50,6,17,16,52,9,51,11,13,18,7,44,48,14,67,15,5,47,8,12,10,2,22,3,65,23,64,57])). % 122.98/123.03 cnf(5995,plain, % 122.98/123.03 (P2(f4(f4(a10,f8(a10)),f4(f8(a10),a10)))), % 122.98/123.03 inference(scs_inference,[],[26,4826,5811,5940,5944,3759,5416,4248,5000,5946,5897,4336,2804,3721,2836,109,4,50,6,17,16,52,9,51,11,13,18,7,44,48,14,67,15,5,47,8,12,10,2,22,3,65,23,64,57,81,20])). % 122.98/123.03 cnf(6028,plain, % 122.98/123.03 (P2(f8(f4(f4(a10,f8(a10)),f4(f8(a10),a10))))), % 122.98/123.03 inference(scs_inference,[],[4722,5995,4,50,6,17,16,52,9,51,11,13,18,7,44])). % 122.98/123.03 cnf(6042,plain, % 122.98/123.03 (~E(f8(f4(f8(a10),f8(a10))),f5(a11,a11))), % 122.98/123.03 inference(scs_inference,[],[4722,5985,5995,4,50,6,17,16,52,9,51,11,13,18,7,44,48,14,67,15,5,47,8,12,10,2])). % 122.98/123.03 cnf(6043,plain, % 122.98/123.03 (~P4(f9(a10,f4(f3(a11,a1),f3(a11,a1))),f5(a11,a11))), % 122.98/123.03 inference(scs_inference,[],[4722,5985,4804,5995,3050,4,50,6,17,16,52,9,51,11,13,18,7,44,48,14,67,15,5,47,8,12,10,2,22])). % 122.98/123.03 cnf(6088,plain, % 122.98/123.03 (~E(f4(f8(f8(a10)),f8(a10)),f5(a11,a11))), % 122.98/123.03 inference(scs_inference,[],[6042,6043,4729,3763,3537,5969,5991,5944,2935,4,50,6,17,52,16,9,51,11,13,18,44,7,48,14,15,5,47,8,12,10,2,22,3])). % 122.98/123.03 cnf(6124,plain, % 122.98/123.03 (~E(f5(a11,a11),f4(f8(f8(a10)),f8(a10)))), % 122.98/123.03 inference(scs_inference,[],[6088,4773,6028,508,4,50,6,17,16,9,51,11,13,44,18,7,48,14,15,5,47,8,12,10,2])). % 122.98/123.03 cnf(6127,plain, % 122.98/123.03 (P2(f4(f8(a10),f8(a10)))), % 122.98/123.03 inference(scs_inference,[],[6088,4773,3236,4935,6028,4742,2813,140,508,4,50,6,17,16,9,51,11,13,44,18,7,48,14,15,5,47,8,12,10,2,22,3,65])). % 122.98/123.03 cnf(6129,plain, % 122.98/123.03 (P2(f9(f8(a10),f8(a10)))), % 122.98/123.03 inference(scs_inference,[],[6088,4773,3236,4935,6028,4742,2813,140,508,4,50,6,17,16,9,51,11,13,44,18,7,48,14,15,5,47,8,12,10,2,22,3,65,64])). % 122.98/123.03 cnf(6132,plain, % 122.98/123.03 (P4(a10,f4(f4(f8(a10),f8(a10)),f4(f8(a10),f8(a10))))), % 122.98/123.03 inference(scs_inference,[],[6088,4773,3236,4935,5679,6028,4742,810,4284,2813,140,508,4,50,6,17,16,9,51,11,13,44,18,7,48,14,15,5,47,8,12,10,2,22,3,65,64,23,82])). % 122.98/123.03 cnf(6151,plain, % 122.98/123.03 (~P4(f4(f8(a10),f8(a10)),f5(a11,a11))), % 122.98/123.03 inference(scs_inference,[],[6127,813])). % 122.98/123.03 cnf(6163,plain, % 122.98/123.03 (E(f9(f4(f8(a10),f8(a10)),a10),f4(f8(a10),f8(a10)))), % 122.98/123.03 inference(scs_inference,[],[6127,6129,4778,45,55,4,54,50])). % 122.98/123.03 cnf(6177,plain, % 122.98/123.03 (E(f4(a10,f4(f8(a10),f8(a10))),a10)), % 122.98/123.03 inference(scs_inference,[],[6127,6129,4778,45,55,4,54,50,6,17,16,51,9,11,13,44,18,7,48])). % 122.98/123.03 cnf(6194,plain, % 122.98/123.03 (~E(f9(f5(f12(a11),f12(a11)),f4(f3(a11,f2(a11)),f3(a11,f2(a11)))),f4(f8(f8(a10)),f8(a10)))), % 122.98/123.03 inference(scs_inference,[],[6127,6129,6124,4778,4530,4081,5445,127,45,55,4,54,50,6,17,16,51,9,11,13,44,18,7,48,67,14,15,47,5,8,12,10,2,77,22,3])). % 122.98/123.03 cnf(6207,plain, % 122.98/123.03 (P4(f9(f4(f8(a10),f8(a10)),f4(f8(a10),f8(a10))),f9(f4(f8(a10),f8(a10)),f4(f8(a10),f8(a10))))), % 122.98/123.03 inference(scs_inference,[],[6127,6129,4474,6124,4778,6132,4530,3613,5984,4081,5851,5445,810,127,160,45,55,4,54,50,6,17,16,51,9,11,13,44,18,7,48,67,14,15,47,5,8,12,10,2,77,22,3,72,65,64,23,63,81,88])). % 122.98/123.03 cnf(6214,plain, % 122.98/123.03 (P2(f4(a10,a10))), % 122.98/123.03 inference(scs_inference,[],[6127,6129,4474,6124,4778,6132,4530,3613,5984,4081,5851,5445,810,3946,127,160,45,55,4,54,50,6,17,16,51,9,11,13,44,18,7,48,67,14,15,47,5,8,12,10,2,77,22,3,72,65,64,23,63,81,88,89,52,24,20])). % 122.98/123.03 cnf(6228,plain, % 122.98/123.03 (P4(a10,f4(f4(a10,a10),f4(a10,a10)))), % 122.98/123.03 inference(scs_inference,[],[6214,67])). % 122.98/123.03 cnf(6246,plain, % 122.98/123.03 (E(f9(f4(a10,a10),a10),f4(a10,a10))), % 122.98/123.03 inference(scs_inference,[],[6214,6177,6194,67,14,15,47,5,8,12,10,2,45,55,4,54,50])). % 122.98/123.03 cnf(6252,plain, % 122.98/123.03 (E(f9(a10,f4(a10,a10)),f4(a10,a10))), % 122.98/123.03 inference(scs_inference,[],[6214,6177,6194,67,14,15,47,5,8,12,10,2,45,55,4,54,50,6,17,16,9,51])). % 122.98/123.03 cnf(6256,plain, % 122.98/123.03 (P2(f8(f4(a10,a10)))), % 122.98/123.03 inference(scs_inference,[],[6214,6177,6194,67,14,15,47,5,8,12,10,2,45,55,4,54,50,6,17,16,9,51,11,13,44])). % 122.98/123.03 cnf(6264,plain, % 122.98/123.03 (P2(f9(f4(a10,a10),f4(a10,a10)))), % 122.98/123.03 inference(scs_inference,[],[6214,6177,6194,67,14,15,47,5,8,12,10,2,45,55,4,54,50,6,17,16,9,51,11,13,44,7,48,18,77,64])). % 122.98/123.03 cnf(6266,plain, % 122.98/123.03 (~P4(f4(f8(a10),f8(a10)),f9(a10,f5(a11,a11)))), % 122.98/123.03 inference(scs_inference,[],[6214,6151,6177,6194,5357,67,14,15,47,5,8,12,10,2,45,55,4,54,50,6,17,16,9,51,11,13,44,7,48,18,77,64,23])). % 122.98/123.03 cnf(6273,plain, % 122.98/123.03 (P2(f4(f4(a10,a10),f4(a10,a10)))), % 122.98/123.03 inference(scs_inference,[],[6214,6151,6177,5942,6194,580,5357,67,14,15,47,5,8,12,10,2,45,55,4,54,50,6,17,16,9,51,11,13,44,7,48,18,77,64,23,76,22,3,72,65])). % 122.98/123.03 cnf(6275,plain, % 122.98/123.03 (~E(f13(f2(a11)),f13(a1))), % 122.98/123.03 inference(scs_inference,[],[26,6214,6151,6177,5942,6194,2911,580,5357,38,67,14,15,47,5,8,12,10,2,45,55,4,54,50,6,17,16,9,51,11,13,44,7,48,18,77,64,23,76,22,3,72,65,57])). % 122.98/123.03 cnf(6277,plain, % 122.98/123.03 (P4(f5(a11,a11),f4(f8(a10),f8(a10)))), % 122.98/123.03 inference(scs_inference,[],[26,6214,6151,6177,5942,6194,2911,580,6127,5357,160,38,67,14,15,47,5,8,12,10,2,45,55,4,54,50,6,17,16,9,51,11,13,44,7,48,18,77,64,23,76,22,3,72,65,57,63])). % 122.98/123.03 cnf(6279,plain, % 122.98/123.03 (P4(a10,f9(f4(a10,a10),f4(a10,a10)))), % 122.98/123.03 inference(scs_inference,[],[26,6214,6151,6177,5942,6194,4642,2911,580,6127,5357,160,38,67,14,15,47,5,8,12,10,2,45,55,4,54,50,6,17,16,9,51,11,13,44,7,48,18,77,64,23,76,22,3,72,65,57,63,81])). % 122.98/123.03 cnf(6313,plain, % 122.98/123.03 (E(f4(a10,a10),a10)), % 122.98/123.03 inference(scs_inference,[],[27,6246,6256,67,14,15,47])). % 122.98/123.03 cnf(6319,plain, % 122.98/123.03 (~E(f13(a1),f13(f2(a11)))), % 122.98/123.03 inference(scs_inference,[],[27,6246,6275,6256,67,14,15,47,5,8,12,10,2])). % 122.98/123.03 cnf(6327,plain, % 122.98/123.03 (E(f9(a10,a10),a10)), % 122.98/123.03 inference(scs_inference,[],[27,6246,6275,6256,67,14,15,47,5,8,12,10,2,45,55,4,54,50])). % 122.98/123.03 cnf(6345,plain, % 122.98/123.03 (P2(f9(a10,a10))), % 122.98/123.03 inference(scs_inference,[],[27,6246,6275,6256,6264,67,14,15,47,5,8,12,10,2,45,55,4,54,50,6,52,17,16,51,9,11,13,44,48,7,18,64])). % 122.98/123.03 cnf(6352,plain, % 122.98/123.03 (~P4(f9(f4(f8(a10),f8(a10)),a10),f9(a10,f5(a11,a11)))), % 122.98/123.03 inference(scs_inference,[],[27,6246,6275,6256,6264,6266,6163,5852,6207,67,14,15,47,5,8,12,10,2,45,55,4,54,50,6,52,17,16,51,9,11,13,44,48,7,18,64,77,23,76,22])). % 122.98/123.03 cnf(6353,plain, % 122.98/123.03 (~E(f13(f2(a11)),f13(f6(f13(a1))))), % 122.98/123.03 inference(scs_inference,[],[27,6246,6275,6256,6264,6266,6163,5852,6207,2824,67,14,15,47,5,8,12,10,2,45,55,4,54,50,6,52,17,16,51,9,11,13,44,48,7,18,64,77,23,76,22,3])). % 122.98/123.03 cnf(6360,plain, % 122.98/123.03 (~E(f13(f13(f2(a11))),f13(f13(a1)))), % 122.98/123.03 inference(scs_inference,[],[27,6246,6275,6256,6264,6266,6163,5852,6207,2824,2777,206,67,14,15,47,5,8,12,10,2,45,55,4,54,50,6,52,17,16,51,9,11,13,44,48,7,18,64,77,23,76,22,3,72,65,86,57])). % 122.98/123.03 cnf(6378,plain, % 122.98/123.03 (~P4(f4(f8(a10),f8(a10)),f9(f5(f12(a11),f12(a11)),f4(f3(a11,f2(a11)),f3(a11,f2(a11)))))), % 122.98/123.03 inference(scs_inference,[],[27,6246,6275,6256,6264,6273,6277,6228,6279,6266,6163,5852,6207,6151,2866,2824,2777,6127,157,206,160,105,67,14,15,47,5,8,12,10,2,45,55,4,54,50,6,52,17,16,51,9,11,13,44,48,7,18,64,77,23,76,22,3,72,65,86,57,87,84,83,81,82,88,89,63,79])). % 122.98/123.03 cnf(6381,plain, % 122.98/123.03 (~P4(f9(a10,a10),f5(a11,a11))), % 122.98/123.03 inference(scs_inference,[],[6345,319])). % 122.98/123.03 cnf(6384,plain, % 122.98/123.03 (~E(f4(f8(a10),f9(a10,a10)),f5(a11,a11))), % 122.98/123.03 inference(scs_inference,[],[6345,1312])). % 122.98/123.03 cnf(6388,plain, % 122.98/123.03 (E(f7(f4(a10,a10),x63881),f7(a10,x63881))), % 122.98/123.03 inference(scs_inference,[],[6345,6313,67,15])). % 122.98/123.03 cnf(6392,plain, % 122.98/123.03 (E(f4(f4(a10,a10),x63921),f4(a10,x63921))), % 122.98/123.03 inference(scs_inference,[],[6345,6313,67,15,14,47,5])). % 122.98/123.03 cnf(6393,plain, % 122.98/123.03 (E(f9(x63931,f4(a10,a10)),f9(x63931,a10))), % 122.98/123.03 inference(scs_inference,[],[6345,6313,67,15,14,47,5,8])). % 122.98/123.03 cnf(6407,plain, % 122.98/123.03 (P4(f9(a10,a10),f9(a10,a10))), % 122.98/123.03 inference(scs_inference,[],[6345,6313,6360,67,15,14,47,5,8,12,10,2,45,55,54,4,50,6,52])). % 122.98/123.03 cnf(6410,plain, % 122.98/123.03 (E(f9(a10,f9(a10,a10)),f9(a10,a10))), % 122.98/123.03 inference(scs_inference,[],[6345,6313,6360,67,15,14,47,5,8,12,10,2,45,55,54,4,50,6,52,17,51])). % 122.98/123.03 cnf(6412,plain, % 122.98/123.03 (E(f7(x64121,f4(a10,a10)),f7(x64121,a10))), % 122.98/123.03 inference(scs_inference,[],[6345,6313,6360,67,15,14,47,5,8,12,10,2,45,55,54,4,50,6,52,17,51,16])). % 122.98/123.03 cnf(6416,plain, % 122.98/123.03 (P2(f8(f9(a10,a10)))), % 122.98/123.03 inference(scs_inference,[],[6345,6313,6360,67,15,14,47,5,8,12,10,2,45,55,54,4,50,6,52,17,51,16,9,11,13,44])). % 122.98/123.03 cnf(6422,plain, % 122.98/123.03 (P2(f9(f9(a10,a10),f9(a10,a10)))), % 122.98/123.03 inference(scs_inference,[],[6345,6313,6360,67,15,14,47,5,8,12,10,2,45,55,54,4,50,6,52,17,51,16,9,11,13,44,48,7,18,64])). % 122.98/123.03 cnf(6436,plain, % 122.98/123.03 (P4(a10,f9(f9(a10,a10),f9(a10,a10)))), % 122.98/123.03 inference(scs_inference,[],[6345,6313,6252,6352,6360,3680,5857,6378,316,6127,157,67,15,14,47,5,8,12,10,2,45,55,54,4,50,6,52,17,51,16,9,11,13,44,48,7,18,64,77,23,22,3,72,65,63,81])). % 122.98/123.03 cnf(6451,plain, % 122.98/123.03 (P4(a10,f4(f8(f9(a10,a10)),f8(f9(a10,a10))))), % 122.98/123.03 inference(scs_inference,[],[6416,67])). % 122.98/123.03 cnf(6458,plain, % 122.98/123.03 (E(f9(x64581,f9(a10,a10)),f9(x64581,a10))), % 122.98/123.03 inference(scs_inference,[],[6327,6416,67,47,14,15,5,8])). % 122.98/123.03 cnf(6491,plain, % 122.98/123.03 (P4(f9(a10,a10),a10)), % 122.98/123.03 inference(scs_inference,[],[6407,6327,6384,6416,67,47,14,15,5,8,12,10,2,45,55,54,4,50,6,52,17,51,16,9,11,13,44,48,7,18,64,77,23])). % 122.98/123.03 cnf(6492,plain, % 122.98/123.03 (~P4(f9(a10,f9(a10,a10)),f5(a11,a11))), % 122.98/123.03 inference(scs_inference,[],[6381,6407,6327,6410,6384,6416,67,47,14,15,5,8,12,10,2,45,55,54,4,50,6,52,17,51,16,9,11,13,44,48,7,18,64,77,23,22])). % 122.98/123.03 cnf(6493,plain, % 122.98/123.03 (~E(f13(a1),f13(f6(f13(f2(a11)))))), % 122.98/123.03 inference(scs_inference,[],[6381,6407,6327,6410,6384,6416,6319,3108,67,47,14,15,5,8,12,10,2,45,55,54,4,50,6,52,17,51,16,9,11,13,44,48,7,18,64,77,23,22,3])). % 122.98/123.03 cnf(6496,plain, % 122.98/123.03 (P2(f4(f8(f9(a10,a10)),f8(f9(a10,a10))))), % 122.98/123.03 inference(scs_inference,[],[6381,6407,6327,6410,6384,6416,6319,3108,67,47,14,15,5,8,12,10,2,45,55,54,4,50,6,52,17,51,16,9,11,13,44,48,7,18,64,77,23,22,3,72,65])). % 122.98/123.03 cnf(6561,plain, % 122.98/123.03 (P2(f9(f9(a10,a10),a10))), % 122.98/123.03 inference(scs_inference,[],[6492,6388,6392,6412,6458,6422,6353,4636,4284,67,47,15,14,5,8,12,10,2,45,55,54,4,50,6,52,17,51,16,9,11,13,44,48,7,18,64,77,23,22,3,72,20])). % 122.98/123.03 cnf(6573,plain, % 122.98/123.03 (E(a10,f9(a10,a10))), % 122.98/123.03 inference(scs_inference,[],[27,6491,6492,6388,6392,6412,6458,6422,6436,6496,6353,6451,4636,316,4284,6345,160,105,67,47,15,14,5,8,12,10,2,45,55,54,4,50,6,52,17,51,16,9,11,13,44,48,7,18,64,77,23,22,3,72,20,65,81,82,88,63,75])). % 122.98/123.03 cnf(6582,plain, % 122.98/123.03 (E(f4(a10,x65821),f4(f9(a10,a10),x65821))), % 122.98/123.03 inference(scs_inference,[],[6573,6561,67,47,15,14,5])). % 122.98/123.03 cnf(6589,plain, % 122.98/123.03 (~E(f13(f6(f13(f2(a11)))),f13(a1))), % 122.98/123.03 inference(scs_inference,[],[6573,6561,6493,67,47,15,14,5,2060,8,12,10,45,2])). % 122.98/123.03 cnf(6599,plain, % 122.98/123.03 (E(f4(x65991,a10),f4(x65991,f9(a10,a10)))), % 122.98/123.03 inference(scs_inference,[],[6573,6561,6493,67,47,15,14,5,2060,8,12,10,45,2,55,54,4,50,52,6])). % 122.98/123.03 cnf(6888,plain, % 122.98/123.03 (E(f4(a10,x68881),f4(f9(a10,a10),x68881))), % 122.98/123.03 inference(rename_variables,[],[6582])). % 122.98/123.03 cnf(6889,plain, % 122.98/123.03 (E(f4(a10,a10),f4(f8(a10),f8(a10)))), % 122.98/123.03 inference(scs_inference,[],[3946,4749,6582,18,179,2])). % 122.98/123.03 cnf(6895,plain, % 122.98/123.03 (E(f4(a10,x68951),f4(f9(a10,a10),x68951))), % 122.98/123.03 inference(rename_variables,[],[6582])). % 122.98/123.03 cnf(6897,plain, % 122.98/123.03 (E(f4(f4(a10,f8(a10)),x68971),f4(f4(f8(a10),a10),x68971))), % 122.98/123.03 inference(rename_variables,[],[2803])). % 122.98/123.03 cnf(6899,plain, % 122.98/123.03 (E(f4(f4(a10,f8(a10)),x68991),f4(f4(f8(a10),a10),x68991))), % 122.98/123.03 inference(rename_variables,[],[2803])). % 122.98/123.03 cnf(6901,plain, % 122.98/123.03 (E(f4(a10,x69011),f4(f9(a10,a10),x69011))), % 122.98/123.03 inference(rename_variables,[],[6582])). % 122.98/123.03 cnf(6905,plain, % 122.98/123.03 (E(f4(a10,x69051),f4(f9(a10,a10),x69051))), % 122.98/123.03 inference(rename_variables,[],[6582])). % 122.98/123.03 cnf(6907,plain, % 122.98/123.03 (E(f4(a10,x69071),f4(f9(a10,a10),x69071))), % 122.98/123.03 inference(rename_variables,[],[6582])). % 122.98/123.03 cnf(6918,plain, % 122.98/123.03 (P5(f2(f12(a11)),f2(a11))), % 122.98/123.03 inference(scs_inference,[],[39,1001,3946,6313,5355,2813,6573,2933,36,4650,4648,3041,2902,3114,318,4512,4749,2803,6897,6899,6582,6888,6895,6901,6905,6907,6599,18,179,2,113,14,297,145,2176,1997,1301,1306,621,626,552,560,289,184,3,20,22,24,23,25])). % 122.98/123.03 cnf(6919,plain, % 122.98/123.03 (E(f6(f13(a1)),a1)), % 122.98/123.03 inference(scs_inference,[],[39,1001,26,3946,6313,5355,2813,6573,2933,36,4650,4648,2824,2822,3041,2902,3114,318,4512,4749,2803,6897,6899,6582,6888,6895,6901,6905,6907,6599,18,179,2,113,14,297,145,2176,1997,1301,1306,621,626,552,560,289,184,3,20,22,24,23,25,57])). % 122.98/123.03 cnf(6921,plain, % 122.98/123.03 (E(a10,f8(f8(a10)))), % 122.98/123.03 inference(scs_inference,[],[39,27,1001,26,286,3946,6313,5355,2813,6573,2933,36,4650,4648,2824,2822,3041,2902,3114,318,4512,4749,2803,6897,6899,6582,6888,6895,6901,6905,6907,6599,18,179,2,113,14,297,145,2176,1997,1301,1306,621,626,552,560,289,184,3,20,22,24,23,25,57,75])). % 122.98/123.03 cnf(6925,plain, % 122.98/123.03 (E(f8(f8(a10)),f8(a10))), % 122.98/123.03 inference(scs_inference,[],[39,27,152,140,1001,160,26,286,3946,6313,5355,2813,6573,2933,36,4650,4648,4830,2824,2822,3041,2902,3114,318,4512,4749,3759,2803,6897,6899,6582,6888,6895,6901,6905,6907,6599,18,179,2,113,14,297,145,2176,1997,1301,1306,621,626,552,560,289,184,3,20,22,24,23,25,57,75,79,85])). % 122.98/123.03 cnf(6937,plain, % 122.98/123.03 (P4(a10,f5(f12(a11),f12(a11)))), % 122.98/123.03 inference(scs_inference,[],[6918,3052])). % 122.98/123.03 cnf(6940,plain, % 122.98/123.03 (E(a10,f4(a10,a10))), % 122.98/123.03 inference(scs_inference,[],[6313,2])). % 122.98/123.03 cnf(6947,plain, % 122.98/123.03 (E(f4(x69471,f4(a10,f8(a10))),f4(x69471,f4(f8(a10),a10)))), % 122.98/123.03 inference(rename_variables,[],[2804])). % 122.98/123.03 cnf(6949,plain, % 122.98/123.03 (E(f4(x69491,f4(a10,f8(a10))),f4(x69491,f4(f8(a10),a10)))), % 122.98/123.03 inference(rename_variables,[],[2804])). % 122.98/123.03 cnf(6951,plain, % 122.98/123.03 (E(f4(x69511,a10),f4(x69511,f9(a10,a10)))), % 122.98/123.03 inference(rename_variables,[],[6599])). % 122.98/123.03 cnf(6970,plain, % 122.98/123.03 (~P4(f4(f3(f12(a11),f13(a1)),f3(f12(a11),f13(a1))),f5(a11,a11))), % 122.98/123.03 inference(scs_inference,[],[39,27,140,28,38,160,139,286,6313,5357,6393,101,3041,3272,2818,2883,3232,3757,6264,3767,318,102,2998,6582,6589,6599,6951,2804,6947,6949,6925,6921,2,113,14,297,145,1301,1306,621,289,184,626,3,20,22,24,23,25,57,58,75,79])). % 122.98/123.03 cnf(6995,plain, % 122.98/123.03 (P5(f6(f2(a11)),f2(a11))), % 122.98/123.03 inference(scs_inference,[],[39,139,5355,4280,3119,2883,3232,6264,172,3016,6599,3166,3350,3411,6940,6889,2,113,14,145,184,3,20,22,24,23,25])). % 122.98/123.03 cnf(7010,plain, % 122.98/123.03 (~P2(f3(a11,f2(a11)))), % 122.98/123.03 inference(scs_inference,[],[27,37,160,39,139,5355,4280,6127,2834,3119,5383,810,3272,2883,3232,3018,6264,4541,172,3266,3262,4474,3016,6599,3166,3350,3411,6970,6940,6889,6937,2845,2,113,14,145,184,3,20,22,24,23,25,57,63,81,79,89,3216,5252,5764,21,65])). % 122.98/123.03 cnf(7028,plain, % 122.98/123.03 ($false), % 122.98/123.03 inference(scs_inference,[],[28,39,139,5357,2879,3121,101,2911,3232,6264,4541,4820,6319,3399,6889,7010,6995,6919,3216,5252,5764,14,2,145,3,23,20,22,24,25,66]), % 122.98/123.03 ['proof']). % 122.98/123.03 % SZS output end Proof % 122.98/123.03 % Total time :122.350000s %------------------------------------------------------------------------------