%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : RNG069+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 : n016.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:57 EDT 2024 % Result : Theorem 118.63s 118.72s % Output : CNFRefutation 118.83s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.14 % Problem : RNG069+2 : TPTP v8.2.0. Released v4.0.0. % 0.04/0.14 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.14/0.36 % Computer : n016.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 300 % 0.14/0.36 % DateTime : Tue Jun 18 14:38:09 EDT 2024 % 0.14/0.36 % CPUTime : % 0.48/0.62 start to proof:theBenchmark % 118.63/118.69 %------------------------------------------- % 118.63/118.69 % File :CSE---1.7 % 118.63/118.69 % Problem :theBenchmark % 118.63/118.69 % Transform :cnf % 118.63/118.69 % Format :tptp:raw % 118.63/118.69 % Command :java -jar mcs_scs.jar %d %s % 118.63/118.69 % 118.63/118.69 % Result :Theorem 117.990000s % 118.63/118.69 % Output :CNFRefutation 117.990000s % 118.63/118.69 %------------------------------------------- % 118.63/118.70 %------------------------------------------------------------------------------ % 118.63/118.70 % File : RNG069+2 : TPTP v8.2.0. Released v4.0.0. % 118.63/118.70 % Domain : Ring Theory % 118.63/118.70 % Problem : Cauchy-Bouniakowsky-Schwarz inequality 05_16_03_04, 01 expansion % 118.63/118.70 % Version : Especial. % 118.63/118.70 % English : % 118.63/118.70 % 118.63/118.70 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 118.63/118.70 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 118.63/118.70 % Source : [Pas08] % 118.63/118.70 % Names : cauchy_05_16_03_04.01 [Pas08] % 118.63/118.70 % 118.63/118.70 % Status : Theorem % 118.63/118.70 % Rating : 0.33 v8.2.0, 0.36 v7.5.0, 0.41 v7.4.0, 0.30 v7.3.0, 0.24 v7.1.0, 0.30 v7.0.0, 0.37 v6.4.0, 0.35 v6.3.0, 0.29 v6.2.0, 0.36 v6.1.0, 0.53 v6.0.0, 0.48 v5.5.0, 0.56 v5.4.0, 0.61 v5.3.0, 0.67 v5.2.0, 0.60 v5.1.0, 0.67 v5.0.0, 0.75 v4.1.0, 0.78 v4.0.1, 0.91 v4.0.0 % 118.63/118.70 % Syntax : Number of formulae : 62 ( 11 unt; 1 def) % 118.63/118.70 % Number of atoms : 199 ( 62 equ) % 118.63/118.70 % Maximal formula atoms : 9 ( 3 avg) % 118.63/118.70 % Number of connectives : 143 ( 6 ~; 1 |; 80 &) % 118.63/118.70 % ( 1 <=>; 55 =>; 0 <=; 0 <~>) % 118.63/118.70 % Maximal formula depth : 10 ( 4 avg) % 118.63/118.70 % Maximal term depth : 5 ( 1 avg) % 118.63/118.70 % Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty) % 118.63/118.70 % Number of functors : 26 ( 26 usr; 18 con; 0-2 aty) % 118.63/118.70 % Number of variables : 73 ( 72 !; 1 ?) % 118.63/118.70 % SPC : FOF_THM_RFO_SEQ % 118.63/118.70 % 118.63/118.70 % Comments : Problem generated by the SAD system [VLP07] % 118.63/118.70 %------------------------------------------------------------------------------ % 118.63/118.70 fof(mNatSort,axiom, % 118.63/118.70 ! [W0] : % 118.63/118.70 ( aNaturalNumber0(W0) % 118.63/118.70 => $true ) ). % 118.63/118.70 % 118.63/118.70 fof(mZeroNat,axiom, % 118.63/118.70 aNaturalNumber0(sz00) ). % 118.63/118.70 % 118.63/118.70 fof(mSuccNat,axiom, % 118.63/118.70 ! [W0] : % 118.63/118.70 ( aNaturalNumber0(W0) % 118.63/118.70 => ( aNaturalNumber0(szszuzczcdt0(W0)) % 118.63/118.70 & szszuzczcdt0(W0) != sz00 ) ) ). % 118.63/118.70 % 118.63/118.70 fof(mNatExtr,axiom, % 118.63/118.70 ! [W0] : % 118.63/118.70 ( ( aNaturalNumber0(W0) % 118.63/118.70 & W0 != sz00 ) % 118.63/118.70 => ? [W1] : % 118.63/118.70 ( aNaturalNumber0(W1) % 118.63/118.70 & W0 = szszuzczcdt0(W1) ) ) ). % 118.63/118.70 % 118.63/118.70 fof(mSuccEqu,axiom, % 118.63/118.70 ! [W0,W1] : % 118.63/118.70 ( ( aNaturalNumber0(W0) % 118.63/118.71 & aNaturalNumber0(W1) ) % 118.63/118.71 => ( szszuzczcdt0(W0) = szszuzczcdt0(W1) % 118.63/118.71 => W0 = W1 ) ) ). % 118.63/118.71 % 118.63/118.71 fof(mIHOrd,axiom, % 118.63/118.71 ! [W0,W1] : % 118.63/118.71 ( ( aNaturalNumber0(W0) % 118.63/118.71 & aNaturalNumber0(W1) ) % 118.63/118.71 => ( iLess0(W0,W1) % 118.63/118.71 => $true ) ) ). % 118.63/118.71 % 118.63/118.71 fof(mIH,axiom, % 118.63/118.71 ! [W0] : % 118.63/118.71 ( aNaturalNumber0(W0) % 118.63/118.71 => iLess0(W0,szszuzczcdt0(W0)) ) ). % 118.63/118.71 % 118.63/118.71 fof(mScSort,axiom, % 118.63/118.71 ! [W0] : % 118.63/118.71 ( aScalar0(W0) % 118.63/118.71 => $true ) ). % 118.63/118.71 % 118.63/118.71 fof(mSZeroSc,axiom, % 118.63/118.71 aScalar0(sz0z00) ). % 118.63/118.71 % 118.63/118.71 fof(mSumSc,axiom, % 118.63/118.71 ! [W0,W1] : % 118.63/118.71 ( ( aScalar0(W0) % 118.63/118.71 & aScalar0(W1) ) % 118.63/118.71 => aScalar0(sdtpldt0(W0,W1)) ) ). % 118.63/118.71 % 118.63/118.71 fof(mMulSc,axiom, % 118.63/118.71 ! [W0,W1] : % 118.63/118.71 ( ( aScalar0(W0) % 118.63/118.71 & aScalar0(W1) ) % 118.63/118.71 => aScalar0(sdtasdt0(W0,W1)) ) ). % 118.63/118.71 % 118.63/118.71 fof(mNegSc,axiom, % 118.63/118.71 ! [W0] : % 118.63/118.71 ( aScalar0(W0) % 118.63/118.71 => aScalar0(smndt0(W0)) ) ). % 118.63/118.71 % 118.63/118.71 fof(mScZero,axiom, % 118.63/118.71 ! [W0] : % 118.63/118.71 ( aScalar0(W0) % 118.63/118.71 => ( sdtpldt0(W0,sz0z00) = W0 % 118.63/118.71 & sdtpldt0(sz0z00,W0) = W0 % 118.63/118.71 & sdtasdt0(W0,sz0z00) = sz0z00 % 118.63/118.71 & sdtasdt0(sz0z00,W0) = sz0z00 % 118.63/118.71 & sdtpldt0(W0,smndt0(W0)) = sz0z00 % 118.63/118.71 & sdtpldt0(smndt0(W0),W0) = sz0z00 % 118.63/118.71 & smndt0(smndt0(W0)) = W0 % 118.63/118.71 & smndt0(sz0z00) = sz0z00 ) ) ). % 118.63/118.71 % 118.63/118.71 fof(mArith,axiom, % 118.63/118.71 ! [W0,W1,W2] : % 118.63/118.71 ( ( aScalar0(W0) % 118.63/118.71 & aScalar0(W1) % 118.63/118.71 & aScalar0(W2) ) % 118.63/118.71 => ( sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) % 118.63/118.71 & sdtpldt0(W0,W1) = sdtpldt0(W1,W0) % 118.63/118.71 & sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) % 118.63/118.71 & sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ) ). % 118.63/118.71 % 118.63/118.71 fof(mDistr,axiom, % 118.63/118.71 ! [W0,W1,W2] : % 118.63/118.71 ( ( aScalar0(W0) % 118.63/118.71 & aScalar0(W1) % 118.63/118.71 & aScalar0(W2) ) % 118.63/118.71 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 118.63/118.71 & sdtasdt0(sdtpldt0(W0,W1),W2) = sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W1,W2)) ) ) ). % 118.63/118.71 % 118.63/118.71 fof(mDistr2,axiom, % 118.63/118.71 ! [W0,W1,W2,W3] : % 118.63/118.71 ( ( aScalar0(W0) % 118.63/118.71 & aScalar0(W1) % 118.63/118.71 & aScalar0(W2) % 118.63/118.71 & aScalar0(W3) ) % 118.63/118.71 => sdtasdt0(sdtpldt0(W0,W1),sdtpldt0(W2,W3)) = sdtpldt0(sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W0,W3)),sdtpldt0(sdtasdt0(W1,W2),sdtasdt0(W1,W3))) ) ). % 118.63/118.71 % 118.63/118.71 fof(mMNeg,axiom, % 118.63/118.71 ! [W0,W1] : % 118.63/118.71 ( ( aScalar0(W0) % 118.63/118.71 & aScalar0(W1) ) % 118.63/118.71 => ( sdtasdt0(W0,smndt0(W1)) = smndt0(sdtasdt0(W0,W1)) % 118.63/118.71 & sdtasdt0(smndt0(W0),W1) = smndt0(sdtasdt0(W0,W1)) ) ) ). % 118.63/118.71 % 118.63/118.71 fof(mMDNeg,axiom, % 118.63/118.71 ! [W0,W1] : % 118.63/118.71 ( ( aScalar0(W0) % 118.63/118.71 & aScalar0(W1) ) % 118.63/118.71 => sdtasdt0(smndt0(W0),smndt0(W1)) = sdtasdt0(W0,W1) ) ). % 118.63/118.71 % 118.63/118.71 fof(mLess,axiom, % 118.63/118.71 ! [W0,W1] : % 118.63/118.71 ( ( aScalar0(W0) % 118.63/118.71 & aScalar0(W1) ) % 118.63/118.71 => ( sdtlseqdt0(W0,W1) % 118.63/118.71 => $true ) ) ). % 118.63/118.71 % 118.63/118.71 fof(mLERef,axiom, % 118.63/118.71 ! [W0] : % 118.63/118.71 ( aScalar0(W0) % 118.63/118.71 => sdtlseqdt0(W0,W0) ) ). % 118.63/118.71 % 118.63/118.71 fof(mLEASm,axiom, % 118.63/118.71 ! [W0,W1] : % 118.63/118.71 ( ( aScalar0(W0) % 118.63/118.71 & aScalar0(W1) ) % 118.63/118.71 => ( ( sdtlseqdt0(W0,W1) % 118.63/118.71 & sdtlseqdt0(W1,W0) ) % 118.63/118.71 => W0 = W1 ) ) ). % 118.63/118.71 % 118.63/118.71 fof(mLETrn,axiom, % 118.63/118.71 ! [W0,W1,W2] : % 118.63/118.71 ( ( aScalar0(W0) % 118.63/118.71 & aScalar0(W1) % 118.63/118.71 & aScalar0(W2) ) % 118.63/118.71 => ( ( sdtlseqdt0(W0,W1) % 118.63/118.71 & sdtlseqdt0(W1,W2) ) % 118.63/118.71 => sdtlseqdt0(W0,W2) ) ) ). % 118.63/118.71 % 118.63/118.71 fof(mLEMon,axiom, % 118.63/118.71 ! [W0,W1,W2,W3] : % 118.63/118.71 ( ( aScalar0(W0) % 118.63/118.71 & aScalar0(W1) % 118.63/118.71 & aScalar0(W2) % 118.63/118.71 & aScalar0(W3) ) % 118.63/118.71 => ( ( sdtlseqdt0(W0,W1) % 118.63/118.71 & sdtlseqdt0(W2,W3) ) % 118.63/118.71 => sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W3)) ) ) ). % 118.63/118.71 % 118.63/118.71 fof(mLEMonM,axiom, % 118.63/118.71 ! [W0,W1,W2,W3] : % 118.63/118.71 ( ( aScalar0(W0) % 118.63/118.71 & aScalar0(W1) % 118.63/118.71 & aScalar0(W2) % 118.63/118.71 & aScalar0(W3) ) % 118.63/118.71 => ( ( sdtlseqdt0(W0,W1) % 118.63/118.71 & sdtlseqdt0(sz0z00,W2) % 118.63/118.71 & sdtlseqdt0(W2,W3) ) % 118.63/118.71 => sdtlseqdt0(sdtasdt0(W0,W2),sdtasdt0(W1,W3)) ) ) ). % 118.63/118.71 % 118.63/118.71 fof(mLETot,axiom, % 118.63/118.71 ! [W0,W1] : % 118.63/118.71 ( ( aScalar0(W0) % 118.63/118.71 & aScalar0(W1) ) % 118.63/118.71 => ( sdtlseqdt0(W0,W1) % 118.63/118.71 | sdtlseqdt0(W1,W0) ) ) ). % 118.63/118.71 % 118.63/118.71 fof(mPosMon,axiom, % 118.63/118.71 ! [W0,W1] : % 118.63/118.71 ( ( aScalar0(W0) % 118.63/118.71 & aScalar0(W1) ) % 118.63/118.71 => ( ( sdtlseqdt0(sz0z00,W0) % 118.63/118.71 & sdtlseqdt0(sz0z00,W1) ) % 118.63/118.71 => ( sdtlseqdt0(sz0z00,sdtpldt0(W0,W1)) % 118.63/118.71 & sdtlseqdt0(sz0z00,sdtasdt0(W0,W1)) ) ) ) ). % 118.63/118.71 % 118.63/118.71 fof(mSqPos,axiom, % 118.63/118.71 ! [W0] : % 118.63/118.71 ( aScalar0(W0) % 118.63/118.71 => sdtlseqdt0(sz0z00,sdtasdt0(W0,W0)) ) ). % 118.63/118.71 % 118.63/118.71 fof(mSqrt,axiom, % 118.63/118.71 ! [W0,W1] : % 118.63/118.71 ( ( aScalar0(W0) % 118.63/118.71 & aScalar0(W1) ) % 118.63/118.71 => ( ( sdtlseqdt0(sz0z00,W0) % 118.63/118.71 & sdtlseqdt0(sz0z00,W1) % 118.63/118.71 & sdtasdt0(W0,W0) = sdtasdt0(W1,W1) ) % 118.63/118.71 => W0 = W1 ) ) ). % 118.63/118.71 % 118.63/118.71 fof(mVcSort,axiom, % 118.63/118.71 ! [W0] : % 118.63/118.71 ( aVector0(W0) % 118.63/118.71 => $true ) ). % 118.63/118.71 % 118.63/118.71 fof(mDimNat,axiom, % 118.63/118.71 ! [W0] : % 118.63/118.71 ( aVector0(W0) % 118.63/118.71 => aNaturalNumber0(aDimensionOf0(W0)) ) ). % 118.63/118.71 % 118.63/118.71 fof(mElmSc,axiom, % 118.63/118.71 ! [W0,W1] : % 118.63/118.71 ( ( aVector0(W0) % 118.63/118.71 & aNaturalNumber0(W1) ) % 118.63/118.71 => aScalar0(sdtlbdtrb0(W0,W1)) ) ). % 118.63/118.71 % 118.63/118.71 fof(mDefInit,definition, % 118.63/118.71 ! [W0] : % 118.63/118.71 ( aVector0(W0) % 118.63/118.71 => ( aDimensionOf0(W0) != sz00 % 118.63/118.71 => ! [W1] : % 118.63/118.71 ( W1 = sziznziztdt0(W0) % 118.63/118.71 <=> ( aVector0(W1) % 118.63/118.71 & szszuzczcdt0(aDimensionOf0(W1)) = aDimensionOf0(W0) % 118.63/118.71 & ! [W2] : % 118.63/118.71 ( aNaturalNumber0(W2) % 118.63/118.71 => sdtlbdtrb0(W1,W2) = sdtlbdtrb0(W0,W2) ) ) ) ) ) ). % 118.63/118.71 % 118.63/118.71 fof(mEqInit,axiom, % 118.63/118.71 ! [W0,W1] : % 118.63/118.71 ( ( aVector0(W0) % 118.63/118.71 & aVector0(W1) ) % 118.63/118.71 => ( ( aDimensionOf0(W0) = aDimensionOf0(W1) % 118.63/118.71 & aDimensionOf0(W1) != sz00 ) % 118.63/118.71 => aDimensionOf0(sziznziztdt0(W0)) = aDimensionOf0(sziznziztdt0(W1)) ) ) ). % 118.63/118.71 % 118.63/118.71 fof(mScPr,axiom, % 118.63/118.71 ! [W0,W1] : % 118.63/118.71 ( ( aVector0(W0) % 118.63/118.71 & aVector0(W1) ) % 118.63/118.71 => ( aDimensionOf0(W0) = aDimensionOf0(W1) % 118.63/118.71 => aScalar0(sdtasasdt0(W0,W1)) ) ) ). % 118.63/118.71 % 118.63/118.71 fof(mDefSPZ,axiom, % 118.63/118.71 ! [W0,W1] : % 118.63/118.71 ( ( aVector0(W0) % 118.63/118.71 & aVector0(W1) ) % 118.63/118.71 => ( ( aDimensionOf0(W0) = aDimensionOf0(W1) % 118.63/118.71 & aDimensionOf0(W1) = sz00 ) % 118.63/118.71 => sdtasasdt0(W0,W1) = sz0z00 ) ) ). % 118.63/118.71 % 118.63/118.71 fof(mDefSPN,axiom, % 118.63/118.71 ! [W0,W1] : % 118.63/118.71 ( ( aVector0(W0) % 118.63/118.71 & aVector0(W1) ) % 118.63/118.71 => ( ( aDimensionOf0(W0) = aDimensionOf0(W1) % 118.63/118.71 & aDimensionOf0(W1) != sz00 ) % 118.63/118.71 => sdtasasdt0(W0,W1) = sdtpldt0(sdtasasdt0(sziznziztdt0(W0),sziznziztdt0(W1)),sdtasdt0(sdtlbdtrb0(W0,aDimensionOf0(W0)),sdtlbdtrb0(W1,aDimensionOf0(W1)))) ) ) ). % 118.63/118.71 % 118.63/118.71 fof(mScSqPos,axiom, % 118.63/118.71 ! [W0] : % 118.63/118.71 ( aVector0(W0) % 118.63/118.71 => sdtlseqdt0(sz0z00,sdtasasdt0(W0,W0)) ) ). % 118.63/118.71 % 118.63/118.71 fof(m__1678,hypothesis, % 118.63/118.72 ( aVector0(xs) % 118.63/118.72 & aVector0(xt) ) ). % 118.63/118.72 % 118.63/118.72 fof(m__1652,hypothesis, % 118.63/118.72 ! [W0,W1] : % 118.63/118.72 ( ( aVector0(W0) % 118.63/118.72 & aVector0(W1) ) % 118.63/118.72 => ( aDimensionOf0(W0) = aDimensionOf0(W1) % 118.63/118.72 => ( iLess0(aDimensionOf0(W0),aDimensionOf0(xs)) % 118.63/118.72 => sdtlseqdt0(sdtasdt0(sdtasasdt0(W0,W1),sdtasasdt0(W0,W1)),sdtasdt0(sdtasasdt0(W0,W0),sdtasasdt0(W1,W1))) ) ) ) ). % 118.63/118.72 % 118.63/118.72 fof(m__1678_01,hypothesis, % 118.63/118.72 aDimensionOf0(xs) = aDimensionOf0(xt) ). % 118.63/118.72 % 118.63/118.72 fof(m__1692,hypothesis, % 118.63/118.72 aDimensionOf0(xs) != sz00 ). % 118.63/118.72 % 118.63/118.72 fof(m__1709,hypothesis, % 118.63/118.72 ( aVector0(xp) % 118.63/118.72 & szszuzczcdt0(aDimensionOf0(xp)) = aDimensionOf0(xs) % 118.63/118.72 & ! [W0] : % 118.63/118.72 ( aNaturalNumber0(W0) % 118.63/118.72 => sdtlbdtrb0(xp,W0) = sdtlbdtrb0(xs,W0) ) % 118.63/118.72 & xp = sziznziztdt0(xs) ) ). % 118.63/118.72 % 118.63/118.72 fof(m__1726,hypothesis, % 118.63/118.72 ( aVector0(xq) % 118.63/118.72 & szszuzczcdt0(aDimensionOf0(xq)) = aDimensionOf0(xt) % 118.63/118.72 & ! [W0] : % 118.63/118.72 ( aNaturalNumber0(W0) % 118.63/118.72 => sdtlbdtrb0(xq,W0) = sdtlbdtrb0(xt,W0) ) % 118.63/118.72 & xq = sziznziztdt0(xt) ) ). % 118.63/118.72 % 118.63/118.72 fof(m__1746,hypothesis, % 118.63/118.72 ( aScalar0(xA) % 118.63/118.72 & xA = sdtlbdtrb0(xs,aDimensionOf0(xs)) ) ). % 118.63/118.72 % 118.63/118.72 fof(m__1766,hypothesis, % 118.63/118.72 ( aScalar0(xB) % 118.63/118.72 & xB = sdtlbdtrb0(xt,aDimensionOf0(xt)) ) ). % 118.63/118.72 % 118.63/118.72 fof(m__1783,hypothesis, % 118.63/118.72 ( aScalar0(xC) % 118.63/118.72 & xC = sdtasasdt0(xp,xp) ) ). % 118.63/118.72 % 118.63/118.72 fof(m__1800,hypothesis, % 118.63/118.72 ( aScalar0(xD) % 118.63/118.72 & xD = sdtasasdt0(xq,xq) ) ). % 118.63/118.72 % 118.63/118.72 fof(m__1820,hypothesis, % 118.63/118.72 ( aScalar0(xE) % 118.63/118.72 & xE = sdtasasdt0(xp,xq) ) ). % 118.63/118.72 % 118.63/118.72 fof(m__1837,hypothesis, % 118.63/118.72 ( aScalar0(xF) % 118.63/118.72 & xF = sdtasdt0(xA,xA) ) ). % 118.63/118.72 % 118.63/118.72 fof(m__1854,hypothesis, % 118.63/118.72 ( aScalar0(xG) % 118.63/118.72 & xG = sdtasdt0(xB,xB) ) ). % 118.63/118.72 % 118.63/118.72 fof(m__1873,hypothesis, % 118.63/118.72 ( aScalar0(xH) % 118.63/118.72 & xH = sdtasdt0(xA,xB) ) ). % 118.63/118.72 % 118.63/118.72 fof(m__1892,hypothesis, % 118.63/118.72 ( aScalar0(xR) % 118.63/118.72 & xR = sdtasdt0(xC,xG) ) ). % 118.63/118.72 % 118.63/118.72 fof(m__1911,hypothesis, % 118.63/118.72 ( aScalar0(xP) % 118.63/118.72 & xP = sdtasdt0(xE,xH) ) ). % 118.63/118.72 % 118.63/118.72 fof(m__1930,hypothesis, % 118.63/118.72 ( aScalar0(xS) % 118.63/118.72 & xS = sdtasdt0(xF,xD) ) ). % 118.63/118.72 % 118.63/118.72 fof(m__1949,hypothesis, % 118.63/118.72 ( aScalar0(xN) % 118.63/118.72 & xN = sdtasdt0(xR,xS) ) ). % 118.63/118.72 % 118.63/118.72 fof(m__1967,hypothesis, % 118.63/118.72 sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)) ). % 118.63/118.72 % 118.63/118.72 fof(m__2004,hypothesis, % 118.63/118.72 sdtlseqdt0(sdtasdt0(xP,xP),xN) ). % 118.63/118.72 % 118.63/118.72 fof(m__2104,hypothesis, % 118.63/118.72 sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS))) ). % 118.63/118.72 % 118.63/118.72 fof(m__2463,hypothesis, % 118.63/118.72 sdtlseqdt0(sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN),xN)) ). % 118.63/118.72 % 118.63/118.72 fof(m__2510,hypothesis, % 118.63/118.72 sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),xN),sdtasdt0(xS,xS)),xN) = sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),xN),sdtpldt0(sdtasdt0(xS,xS),xN)) ). % 118.63/118.72 % 118.63/118.72 fof(m__2580,hypothesis, % 118.63/118.72 sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP))),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xR,xS)),sdtpldt0(sdtasdt0(xS,xR),sdtasdt0(xS,xS)))) ). % 118.63/118.72 % 118.63/118.72 fof(m__,conjecture, % 118.63/118.72 sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS))) ). % 118.63/118.72 % 118.63/118.72 %------------------------------------------------------------------------------ % 118.63/118.72 %------------------------------------------- % 118.63/118.72 % Proof found % 118.63/118.72 % SZS status Theorem for theBenchmark % 118.63/118.72 % SZS output start Proof % 118.63/118.72 %ClaNum:120(EqnAxiom:25) % 118.63/118.72 %VarNum:315(SingletonVarNum:98) % 118.63/118.72 %MaxLitNum:8 % 118.63/118.72 %MaxfuncDepth:4 % 118.63/118.72 %SharedTerms:108 % 118.63/118.72 %goalClause: 68 % 118.63/118.72 %singleGoalClaCount:1 % 118.63/118.72 [28]P1(a3) % 118.63/118.72 [29]P2(a12) % 118.63/118.72 [30]P2(a14) % 118.63/118.72 [31]P2(a16) % 118.63/118.72 [32]P2(a17) % 118.63/118.72 [33]P2(a18) % 118.63/118.72 [34]P2(a19) % 118.63/118.72 [35]P2(a20) % 118.63/118.72 [36]P2(a21) % 118.63/118.72 [37]P2(a22) % 118.63/118.72 [38]P2(a23) % 118.63/118.72 [39]P2(a24) % 118.63/118.72 [40]P2(a26) % 118.63/118.72 [41]P2(a25) % 118.63/118.72 [42]P3(a1) % 118.63/118.72 [43]P3(a28) % 118.63/118.72 [44]P3(a13) % 118.63/118.72 [45]P3(a27) % 118.63/118.72 [26]E(f2(a1),a13) % 118.63/118.72 [27]E(f2(a28),a27) % 118.63/118.72 [46]E(f4(a28),f4(a1)) % 118.63/118.72 [49]E(f5(a13,a13),a17) % 118.63/118.72 [50]E(f5(a27,a27),a18) % 118.63/118.72 [51]E(f5(a13,a27),a19) % 118.63/118.72 [52]E(f8(a14,a14),a20) % 118.63/118.72 [53]E(f8(a16,a16),a21) % 118.63/118.72 [54]E(f8(a14,a16),a22) % 118.63/118.72 [55]E(f8(a17,a21),a23) % 118.63/118.72 [56]E(f8(a19,a22),a24) % 118.63/118.72 [57]E(f8(a20,a18),a26) % 118.63/118.72 [58]E(f8(a23,a26),a25) % 118.63/118.72 [61]P4(f8(a24,a24),a25) % 118.63/118.72 [62]P4(f8(a19,a19),f8(a17,a18)) % 118.63/118.72 [67]~E(f4(a1),a3) % 118.63/118.72 [47]E(f15(f4(a13)),f4(a1)) % 118.63/118.72 [48]E(f15(f4(a27)),f4(a28)) % 118.63/118.72 [59]E(f9(a1,f4(a1)),a14) % 118.63/118.72 [60]E(f9(a28,f4(a28)),a16) % 118.63/118.72 [63]P4(f10(f8(a24,a24),f8(a24,a24)),f10(f8(a23,a23),f8(a26,a26))) % 118.63/118.72 [68]~P4(f8(f10(a24,a24),f10(a24,a24)),f8(f10(a23,a26),f10(a23,a26))) % 118.63/118.72 [64]E(f10(f10(f10(f8(a23,a23),a25),f8(a26,a26)),a25),f10(f10(f8(a23,a23),a25),f10(f8(a26,a26),a25))) % 118.63/118.72 [65]P4(f10(f10(f8(a24,a24),f8(a24,a24)),f10(f8(a24,a24),f8(a24,a24))),f10(f10(f8(a23,a23),f8(a23,a26)),f10(f8(a26,a23),f8(a26,a26)))) % 118.63/118.72 [66]P4(f10(f10(f10(f8(a24,a24),f8(a24,a24)),f8(a24,a24)),f8(a24,a24)),f10(f10(f10(f8(a23,a23),f8(a26,a26)),a25),a25)) % 118.63/118.72 [81]~P2(x811)+P4(x811,x811) % 118.63/118.72 [69]~P2(x691)+E(f11(a12),a12) % 118.63/118.72 [70]~P1(x701)+~E(f15(x701),a3) % 118.63/118.72 [71]~P1(x711)+P1(f15(x711)) % 118.63/118.72 [72]~P3(x721)+P1(f4(x721)) % 118.63/118.72 [73]~P2(x731)+P2(f11(x731)) % 118.63/118.72 [76]~P2(x761)+E(f8(x761,a12),a12) % 118.63/118.72 [77]~P2(x771)+E(f8(a12,x771),a12) % 118.63/118.72 [79]~P2(x791)+E(f10(x791,a12),x791) % 118.63/118.72 [80]~P2(x801)+E(f10(a12,x801),x801) % 118.63/118.72 [85]~P1(x851)+P5(x851,f15(x851)) % 118.63/118.72 [87]~P1(x871)+E(f9(a13,x871),f9(a1,x871)) % 118.63/118.72 [88]~P1(x881)+E(f9(a28,x881),f9(a27,x881)) % 118.63/118.72 [94]~P2(x941)+P4(a12,f8(x941,x941)) % 118.63/118.72 [95]~P3(x951)+P4(a12,f5(x951,x951)) % 118.63/118.72 [74]~P2(x741)+E(f11(f11(x741)),x741) % 118.63/118.72 [83]~P2(x831)+E(f10(x831,f11(x831)),a12) % 118.63/118.72 [84]~P2(x841)+E(f10(f11(x841),x841),a12) % 118.63/118.72 [75]~P1(x751)+E(x751,a3)+P1(f6(x751)) % 118.63/118.72 [78]~P1(x781)+E(x781,a3)+E(f15(f6(x781)),x781) % 118.63/118.72 [91]~P2(x912)+~P2(x911)+P2(f10(x911,x912)) % 118.63/118.72 [92]~P2(x922)+~P2(x921)+P2(f8(x921,x922)) % 118.63/118.72 [93]~P1(x932)+~P3(x931)+P2(f9(x931,x932)) % 118.63/118.72 [100]~P2(x1002)+~P2(x1001)+E(f8(f11(x1001),f11(x1002)),f8(x1001,x1002)) % 118.63/118.72 [104]~P2(x1042)+~P2(x1041)+E(f11(f8(x1041,x1042)),f8(x1041,f11(x1042))) % 118.63/118.72 [105]~P2(x1052)+~P2(x1051)+E(f11(f8(x1051,x1052)),f8(f11(x1051),x1052)) % 118.63/118.72 [90]P4(x902,x901)+~P2(x901)+~P2(x902)+P4(x901,x902) % 118.63/118.72 [82]~P3(x821)+P3(x822)+~E(x822,f2(x821))+E(f4(x821),a3) % 118.63/118.72 [86]~P1(x862)+~P1(x861)+E(x861,x862)+~E(f15(x861),f15(x862)) % 118.63/118.72 [102]~P3(x1022)+~P3(x1021)+~E(f4(x1021),f4(x1022))+P2(f5(x1021,x1022)) % 118.63/118.72 [89]~P3(x891)+~E(x892,f2(x891))+E(f4(x891),a3)+E(f15(f4(x892)),f4(x891)) % 118.63/118.72 [97]~P2(x972)+~P2(x971)+~P2(x973)+E(f10(x971,x972),f10(x972,x971)) % 118.63/118.72 [98]~P2(x982)+~P2(x981)+~P2(x983)+E(f8(x981,x982),f8(x982,x981)) % 118.63/118.72 [110]~P2(x1103)+~P2(x1102)+~P2(x1101)+E(f10(f10(x1101,x1102),x1103),f10(x1101,f10(x1102,x1103))) % 118.63/118.72 [111]~P2(x1113)+~P2(x1112)+~P2(x1111)+E(f8(f8(x1111,x1112),x1113),f8(x1111,f8(x1112,x1113))) % 118.63/118.72 [113]~P2(x1133)+~P2(x1132)+~P2(x1131)+E(f10(f8(x1131,x1132),f8(x1131,x1133)),f8(x1131,f10(x1132,x1133))) % 118.63/118.72 [114]~P2(x1142)+~P2(x1143)+~P2(x1141)+E(f10(f8(x1141,x1142),f8(x1143,x1142)),f8(f10(x1141,x1143),x1142)) % 118.63/118.72 [103]~P2(x1032)+~P2(x1031)+~P4(x1032,x1031)+~P4(x1031,x1032)+E(x1031,x1032) % 118.63/118.72 [96]~P3(x962)+~P3(x961)+~E(f4(x961),f4(x962))+~E(f4(x962),a3)+E(f5(x961,x962),a12) % 118.63/118.72 [108]~P2(x1082)+~P2(x1081)+~P4(a12,x1082)+~P4(a12,x1081)+P4(a12,f10(x1081,x1082)) % 118.63/118.72 [109]~P2(x1092)+~P2(x1091)+~P4(a12,x1092)+~P4(a12,x1091)+P4(a12,f8(x1091,x1092)) % 118.63/118.72 [99]~P3(x991)+~P3(x992)+~E(f4(x992),f4(x991))+E(f4(x991),a3)+E(f4(f2(x992)),f4(f2(x991))) % 118.63/118.72 [119]~P3(x1192)+~P3(x1191)+~E(f4(x1191),f4(x1192))+~P5(f4(x1191),f4(a1))+P4(f8(f5(x1191,x1192),f5(x1191,x1192)),f8(f5(x1191,x1191),f5(x1192,x1192))) % 118.63/118.72 [118]~P3(x1181)+~P3(x1182)+~E(f4(x1182),f4(x1181))+E(f4(x1181),a3)+E(f10(f5(f2(x1182),f2(x1181)),f8(f9(x1182,f4(x1182)),f9(x1181,f4(x1181)))),f5(x1182,x1181)) % 118.63/118.72 [101]~P1(x1013)+~P3(x1011)+~E(x1012,f2(x1011))+E(f9(x1012,x1013),f9(x1011,x1013))+E(f4(x1011),a3) % 118.63/118.72 [120]~P2(x1203)+~P2(x1202)+~P2(x1204)+~P2(x1201)+E(f10(f10(f8(x1201,x1202),f8(x1201,x1203)),f10(f8(x1204,x1202),f8(x1204,x1203))),f8(f10(x1201,x1204),f10(x1202,x1203))) % 118.63/118.72 [112]~P2(x1122)+~P2(x1121)+E(x1121,x1122)+~E(f8(x1121,x1121),f8(x1122,x1122))+~P4(a12,x1122)+~P4(a12,x1121) % 118.63/118.72 [106]~P3(x1061)+~P3(x1062)+E(x1061,f2(x1062))+E(f4(x1062),a3)+P1(f7(x1062,x1061))+~E(f15(f4(x1061)),f4(x1062)) % 118.63/118.72 [117]~P3(x1172)+~P3(x1171)+E(x1171,f2(x1172))+E(f4(x1172),a3)+~E(f15(f4(x1171)),f4(x1172))+~E(f9(x1171,f7(x1172,x1171)),f9(x1172,f7(x1172,x1171))) % 118.63/118.72 [107]~P2(x1072)+~P2(x1071)+~P4(x1073,x1072)+~P4(x1071,x1073)+P4(x1071,x1072)+~P2(x1073) % 118.63/118.72 [115]~P2(x1154)+~P2(x1152)+~P2(x1153)+~P2(x1151)+~P4(x1152,x1154)+~P4(x1151,x1153)+P4(f10(x1151,x1152),f10(x1153,x1154)) % 118.63/118.72 [116]~P2(x1164)+~P2(x1162)+~P2(x1163)+~P2(x1161)+~P4(x1162,x1164)+~P4(x1161,x1163)+~P4(a12,x1162)+P4(f8(x1161,x1162),f8(x1163,x1164)) % 118.63/118.72 %EqnAxiom % 118.63/118.72 [1]E(x11,x11) % 118.63/118.72 [2]E(x22,x21)+~E(x21,x22) % 118.63/118.72 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 118.63/118.72 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 118.63/118.72 [5]~E(x51,x52)+E(f8(x51,x53),f8(x52,x53)) % 118.63/118.72 [6]~E(x61,x62)+E(f8(x63,x61),f8(x63,x62)) % 118.63/118.72 [7]~E(x71,x72)+E(f4(x71),f4(x72)) % 118.63/118.72 [8]~E(x81,x82)+E(f11(x81),f11(x82)) % 118.63/118.72 [9]~E(x91,x92)+E(f15(x91),f15(x92)) % 118.63/118.72 [10]~E(x101,x102)+E(f10(x101,x103),f10(x102,x103)) % 118.63/118.72 [11]~E(x111,x112)+E(f10(x113,x111),f10(x113,x112)) % 118.63/118.72 [12]~E(x121,x122)+E(f9(x121,x123),f9(x122,x123)) % 118.63/118.72 [13]~E(x131,x132)+E(f9(x133,x131),f9(x133,x132)) % 118.63/118.72 [14]~E(x141,x142)+E(f5(x141,x143),f5(x142,x143)) % 118.63/118.72 [15]~E(x151,x152)+E(f5(x153,x151),f5(x153,x152)) % 118.63/118.72 [16]~E(x161,x162)+E(f6(x161),f6(x162)) % 118.63/118.72 [17]~E(x171,x172)+E(f7(x171,x173),f7(x172,x173)) % 118.63/118.72 [18]~E(x181,x182)+E(f7(x183,x181),f7(x183,x182)) % 118.63/118.72 [19]~P1(x191)+P1(x192)+~E(x191,x192) % 118.63/118.72 [20]~P2(x201)+P2(x202)+~E(x201,x202) % 118.63/118.72 [21]P4(x212,x213)+~E(x211,x212)+~P4(x211,x213) % 118.63/118.72 [22]P4(x223,x222)+~E(x221,x222)+~P4(x223,x221) % 118.63/118.72 [23]~P3(x231)+P3(x232)+~E(x231,x232) % 118.63/118.72 [24]P5(x242,x243)+~E(x241,x242)+~P5(x241,x243) % 118.63/118.72 [25]P5(x253,x252)+~E(x251,x252)+~P5(x253,x251) % 118.63/118.72 % 118.63/118.72 %------------------------------------------- % 118.63/118.73 cnf(121,plain, % 118.63/118.73 (~P3(x1211)+P3(f2(x1211))+E(f4(x1211),a3)), % 118.63/118.73 inference(equality_inference,[],[82])). % 118.63/118.73 cnf(123,plain, % 118.63/118.73 (~P3(x1231)+E(f4(x1231),a3)+E(f15(f4(f2(x1231))),f4(x1231))), % 118.63/118.73 inference(equality_inference,[],[89])). % 118.63/118.73 cnf(125,plain, % 118.63/118.73 (~P1(x1251)+~P3(x1252)+E(f9(f2(x1252),x1251),f9(x1252,x1251))+E(f4(x1252),a3)), % 118.63/118.73 inference(equality_inference,[],[101])). % 118.63/118.73 cnf(126,plain, % 118.63/118.73 (~P3(x1261)+~P3(x1261)+P2(f5(x1261,x1261))), % 118.63/118.73 inference(equality_inference,[],[102])). % 118.63/118.73 cnf(128,plain, % 118.63/118.73 (~P3(x1281)+~P3(x1281)+E(f4(x1281),a3)+E(f10(f5(f2(x1281),f2(x1281)),f8(f9(x1281,f4(x1281)),f9(x1281,f4(x1281)))),f5(x1281,x1281))), % 118.63/118.73 inference(equality_inference,[],[118])). % 118.63/118.73 cnf(129,plain, % 118.63/118.73 (~P3(x1291)+~P3(x1291)+~P5(f4(x1291),f4(a1))+P4(f8(f5(x1291,x1291),f5(x1291,x1291)),f8(f5(x1291,x1291),f5(x1291,x1291)))), % 118.63/118.73 inference(equality_inference,[],[119])). % 118.63/118.73 cnf(130,plain, % 118.63/118.73 (E(f4(a1),f4(a28))), % 118.63/118.73 inference(scs_inference,[],[46,2])). % 118.63/118.73 cnf(131,plain, % 118.63/118.73 (P3(f2(a1))), % 118.63/118.73 inference(scs_inference,[],[46,42,67,2,121])). % 118.63/118.73 cnf(133,plain, % 118.63/118.73 (E(f15(f4(f2(a1))),f4(a1))), % 118.63/118.73 inference(scs_inference,[],[46,42,67,2,121,123])). % 118.63/118.73 cnf(135,plain, % 118.63/118.73 (E(f15(f4(a27)),f4(a1))), % 118.63/118.73 inference(scs_inference,[],[46,48,42,67,2,121,123,3])). % 118.63/118.73 cnf(136,plain, % 118.63/118.73 (P4(a12,a12)), % 118.63/118.73 inference(scs_inference,[],[29,46,48,42,67,2,121,123,3,90])). % 118.63/118.73 cnf(138,plain, % 118.63/118.73 (E(f9(f2(a1),a3),f9(a1,a3))), % 118.63/118.73 inference(scs_inference,[],[29,46,48,28,42,67,2,121,123,3,90,125])). % 118.63/118.73 cnf(140,plain, % 118.63/118.73 (E(f10(f5(f2(a1),f2(a1)),f8(f9(a1,f4(a1)),f9(a1,f4(a1)))),f5(a1,a1))), % 118.63/118.73 inference(scs_inference,[],[29,46,48,28,42,67,2,121,123,3,90,125,128])). % 118.63/118.73 cnf(142,plain, % 118.63/118.73 (E(f4(f2(a28)),f4(f2(a1)))), % 118.63/118.73 inference(scs_inference,[],[29,46,48,28,42,43,67,2,121,123,3,90,125,128,99])). % 118.63/118.73 cnf(144,plain, % 118.63/118.73 (P4(f8(a12,a12),f8(a12,a12))), % 118.63/118.73 inference(scs_inference,[],[29,46,48,28,42,43,67,2,121,123,3,90,125,128,99,116])). % 118.63/118.73 cnf(151,plain, % 118.63/118.73 (E(f11(a12),a12)), % 118.63/118.73 inference(scs_inference,[],[30,69])). % 118.63/118.73 cnf(154,plain, % 118.63/118.73 (E(a13,f2(a1))), % 118.63/118.73 inference(scs_inference,[],[26,2])). % 118.63/118.73 cnf(155,plain, % 118.63/118.73 (E(f15(f4(a13)),f4(a28))), % 118.63/118.73 inference(scs_inference,[],[26,47,130,2,3])). % 118.63/118.73 cnf(156,plain, % 118.63/118.73 (P4(a14,a14)), % 118.63/118.73 inference(scs_inference,[],[26,30,47,130,2,3,90])). % 118.63/118.73 cnf(158,plain, % 118.63/118.73 (E(f9(a13,a3),f9(a1,a3))), % 118.63/118.73 inference(scs_inference,[],[26,30,47,130,28,42,67,2,3,90,101])). % 118.63/118.73 cnf(169,plain, % 118.63/118.73 (E(a27,f2(a28))), % 118.63/118.73 inference(scs_inference,[],[27,2])). % 118.63/118.73 cnf(170,plain, % 118.63/118.73 (P3(f2(a28))), % 118.63/118.73 inference(scs_inference,[],[27,45,2,23])). % 118.63/118.73 cnf(174,plain, % 118.63/118.73 (P4(a14,x1741)+~E(a14,x1741)), % 118.63/118.73 inference(scs_inference,[],[156,27,31,45,2,23,90,19,22])). % 118.63/118.73 cnf(175,plain, % 118.63/118.73 (E(x1751,a18)+~E(x1751,f5(a27,a27))), % 118.63/118.73 inference(scs_inference,[],[156,27,31,50,45,2,23,90,19,22,3])). % 118.63/118.73 cnf(183,plain, % 118.63/118.73 (P2(f5(a13,a27))), % 118.63/118.73 inference(scs_inference,[],[34,51,2,20])). % 118.63/118.73 cnf(184,plain, % 118.63/118.73 (P4(a17,a17)), % 118.63/118.73 inference(scs_inference,[],[32,34,51,2,20,90])). % 118.63/118.73 cnf(186,plain, % 118.63/118.73 (~P1(f4(a28))+P1(f4(a1))), % 118.63/118.73 inference(scs_inference,[],[46,32,34,51,2,20,90,19])). % 118.63/118.73 cnf(190,plain, % 118.63/118.73 (P2(f8(a16,a16))), % 118.63/118.73 inference(scs_inference,[],[36,53,2,20])). % 118.63/118.73 cnf(195,plain, % 118.63/118.73 (P4(f5(a13,a27),a19)), % 118.63/118.73 inference(scs_inference,[],[183,36,53,51,2,20,90,19,21,22])). % 118.63/118.73 cnf(203,plain, % 118.63/118.73 (P2(f8(a17,a21))), % 118.63/118.73 inference(scs_inference,[],[195,38,55,51,2,21,20])). % 118.63/118.73 cnf(204,plain, % 118.63/118.73 (P4(f8(a16,a16),f8(a16,a16))), % 118.63/118.73 inference(scs_inference,[],[195,190,38,55,51,2,21,20,90])). % 118.63/118.73 cnf(215,plain, % 118.63/118.73 (P2(f8(a20,a18))), % 118.63/118.73 inference(scs_inference,[],[204,40,57,53,2,21,20])). % 118.63/118.73 cnf(216,plain, % 118.63/118.73 (P4(f8(a17,a21),f8(a17,a21))), % 118.63/118.73 inference(scs_inference,[],[204,203,40,57,53,2,21,20,90])). % 118.63/118.73 cnf(225,plain, % 118.63/118.73 (E(a12,f11(a12))), % 118.63/118.73 inference(scs_inference,[],[151,2])). % 118.63/118.73 cnf(226,plain, % 118.63/118.73 (P4(a12,f11(a12))), % 118.63/118.73 inference(scs_inference,[],[136,151,2,22])). % 118.63/118.73 cnf(228,plain, % 118.63/118.73 (P2(f11(a12))), % 118.63/118.73 inference(scs_inference,[],[136,151,29,2,22,21,20])). % 118.63/118.73 cnf(229,plain, % 118.63/118.73 (P4(f8(a20,a18),f8(a20,a18))), % 118.63/118.73 inference(scs_inference,[],[136,215,151,29,2,22,21,20,90])). % 118.63/118.73 cnf(241,plain, % 118.63/118.73 (P4(a23,f8(a17,a21))), % 118.63/118.73 inference(scs_inference,[],[216,60,55,2,22,21])). % 118.63/118.73 cnf(242,plain, % 118.63/118.73 (P2(f9(a28,f4(a28)))), % 118.63/118.73 inference(scs_inference,[],[216,60,31,55,2,22,21,20])). % 118.63/118.73 cnf(243,plain, % 118.63/118.73 (P4(f11(a12),f11(a12))), % 118.63/118.73 inference(scs_inference,[],[216,228,60,31,55,2,22,21,20,90])). % 118.63/118.73 cnf(251,plain, % 118.63/118.73 (E(a18,f5(a27,a27))), % 118.63/118.73 inference(scs_inference,[],[50,2])). % 118.63/118.73 cnf(252,plain, % 118.63/118.73 (P4(f8(a20,a18),a26)), % 118.63/118.73 inference(scs_inference,[],[229,50,57,2,22])). % 118.63/118.73 cnf(254,plain, % 118.63/118.73 (P2(f5(a27,a27))), % 118.63/118.73 inference(scs_inference,[],[229,33,50,57,2,22,21,20])). % 118.63/118.73 cnf(255,plain, % 118.63/118.73 (P4(f9(a28,f4(a28)),f9(a28,f4(a28)))), % 118.63/118.73 inference(scs_inference,[],[229,242,33,50,57,2,22,21,20,90])). % 118.63/118.73 cnf(257,plain, % 118.63/118.73 (P4(f8(a12,f11(a12)),f8(f11(a12),f11(a12)))), % 118.63/118.73 inference(scs_inference,[],[243,229,226,242,33,228,50,57,29,2,22,21,20,90,116])). % 118.63/118.73 cnf(260,plain, % 118.63/118.73 (E(x2601,a17)+~E(x2601,f5(a13,a13))), % 118.63/118.73 inference(scs_inference,[],[243,229,226,242,33,228,50,49,57,29,2,22,21,20,90,116,19,3])). % 118.63/118.73 cnf(267,plain, % 118.63/118.73 (P2(f8(a14,a16))), % 118.63/118.73 inference(scs_inference,[],[255,54,37,60,2,21,20])). % 118.63/118.73 cnf(268,plain, % 118.63/118.73 (P4(f9(a28,f4(a28)),a16)), % 118.63/118.73 inference(scs_inference,[],[255,54,37,60,2,21,20,22])). % 118.63/118.73 cnf(269,plain, % 118.63/118.73 (P4(f5(a27,a27),f5(a27,a27))), % 118.63/118.73 inference(scs_inference,[],[255,54,254,37,60,2,21,20,22,90])). % 118.63/118.73 cnf(278,plain, % 118.63/118.73 (P4(f5(a27,a27),a18)), % 118.63/118.73 inference(scs_inference,[],[269,56,50,2,22])). % 118.63/118.73 cnf(279,plain, % 118.63/118.73 (P2(f8(a19,a22))), % 118.63/118.73 inference(scs_inference,[],[269,56,39,50,2,22,20])). % 118.63/118.73 cnf(281,plain, % 118.63/118.73 (P4(f8(a14,a16),f8(a14,a16))), % 118.63/118.73 inference(scs_inference,[],[269,56,267,39,50,2,22,20,21,90])). % 118.63/118.73 cnf(285,plain, % 118.63/118.73 (E(x2851,f4(a28))+~E(x2851,f15(f4(a27)))), % 118.63/118.73 inference(scs_inference,[],[269,56,267,39,48,50,2,22,20,21,90,19,23,3])). % 118.63/118.73 cnf(290,plain, % 118.63/118.73 (P2(f8(a23,a26))), % 118.63/118.73 inference(scs_inference,[],[58,41,2,20])). % 118.63/118.73 cnf(291,plain, % 118.63/118.73 (P4(a22,f8(a14,a16))), % 118.63/118.73 inference(scs_inference,[],[281,58,54,41,2,20,21])). % 118.63/118.73 cnf(293,plain, % 118.63/118.73 (P4(f8(a19,a22),f8(a19,a22))), % 118.63/118.73 inference(scs_inference,[],[281,58,54,279,41,2,20,21,22,90])). % 118.63/118.73 cnf(301,plain, % 118.63/118.73 (P1(f15(f4(f2(a28))))), % 118.63/118.73 inference(scs_inference,[],[170,71,72])). % 118.63/118.73 cnf(302,plain, % 118.63/118.73 (E(a14,f9(a1,f4(a1)))), % 118.63/118.73 inference(scs_inference,[],[59,2])). % 118.63/118.73 cnf(303,plain, % 118.63/118.73 (P4(a24,f8(a19,a22))), % 118.63/118.73 inference(scs_inference,[],[293,59,56,2,21])). % 118.63/118.73 cnf(305,plain, % 118.63/118.73 (P2(f9(a1,f4(a1)))), % 118.63/118.73 inference(scs_inference,[],[293,59,56,30,2,21,22,20])). % 118.63/118.73 cnf(306,plain, % 118.63/118.73 (P4(f8(a23,a26),f8(a23,a26))), % 118.63/118.73 inference(scs_inference,[],[293,59,56,290,30,2,21,22,20,90])). % 118.63/118.73 cnf(311,plain, % 118.63/118.73 (E(x3111,f4(a1))+~E(x3111,f15(f4(f2(a1))))), % 118.63/118.73 inference(scs_inference,[],[293,59,56,290,30,133,2,21,22,20,90,174,19,23,3])). % 118.63/118.73 cnf(316,plain, % 118.63/118.73 (P4(f8(a23,a26),a25)), % 118.63/118.73 inference(scs_inference,[],[306,64,58,2,22])). % 118.63/118.73 cnf(327,plain, % 118.63/118.73 (E(a17,f5(a13,a13))), % 118.63/118.73 inference(scs_inference,[],[49,2])). % 118.63/118.73 cnf(328,plain, % 118.63/118.73 (P2(f5(a13,a13))), % 118.63/118.73 inference(scs_inference,[],[49,32,2,20])). % 118.63/118.73 cnf(331,plain, % 118.63/118.73 (P4(a20,a20)), % 118.63/118.73 inference(scs_inference,[],[156,184,49,35,32,302,2,20,21,22,90])). % 118.63/118.73 cnf(339,plain, % 118.63/118.73 (E(f4(a28),f15(f4(a27)))), % 118.63/118.73 inference(scs_inference,[],[48,2])). % 118.63/118.73 cnf(342,plain, % 118.63/118.73 (P4(f5(a13,a13),f5(a13,a13))), % 118.63/118.73 inference(scs_inference,[],[184,241,48,55,328,327,2,22,21,90])). % 118.63/118.73 cnf(344,plain, % 118.63/118.73 (~P1(f15(f4(a27)))+P1(f4(a28))), % 118.63/118.73 inference(scs_inference,[],[184,241,48,55,328,327,2,22,21,90,19])). % 118.63/118.73 cnf(345,plain, % 118.63/118.73 (~P1(f4(a27))+P1(f4(a28))), % 118.63/118.73 inference(scs_inference,[],[184,241,48,55,328,327,2,22,21,90,19,71])). % 118.63/118.73 cnf(349,plain, % 118.63/118.73 (P2(f8(a14,a14))), % 118.63/118.73 inference(scs_inference,[],[52,35,2,20])). % 118.63/118.73 cnf(356,plain, % 118.63/118.73 (E(x3561,f9(a1,a3))+~E(x3561,f9(f2(a1),a3))), % 118.63/118.73 inference(scs_inference,[],[331,52,47,33,35,138,2,20,21,22,90,19,23,3])). % 118.63/118.73 cnf(360,plain, % 118.63/118.73 (E(f4(a1),f15(f4(a13)))), % 118.63/118.73 inference(scs_inference,[],[47,2])). % 118.63/118.73 cnf(363,plain, % 118.63/118.73 (E(f4(a28),f15(f4(a13)))), % 118.63/118.73 inference(scs_inference,[],[252,291,46,47,54,57,2,21,22,3])). % 118.63/118.73 cnf(366,plain, % 118.63/118.73 (~P1(f15(f4(a13)))+P1(f4(a1))), % 118.63/118.73 inference(scs_inference,[],[252,291,46,47,54,57,349,2,21,22,3,90,19])). % 118.63/118.73 cnf(370,plain, % 118.63/118.73 (E(f4(a1),f15(f4(a27)))), % 118.63/118.73 inference(scs_inference,[],[135,2])). % 118.63/118.73 cnf(373,plain, % 118.63/118.73 (E(f15(f4(a27)),f15(f4(a13)))), % 118.63/118.73 inference(scs_inference,[],[303,316,58,56,48,135,363,2,22,21,3])). % 118.63/118.73 cnf(380,plain, % 118.63/118.73 (E(f9(a1,a3),f9(a13,a3))), % 118.63/118.73 inference(scs_inference,[],[158,2])). % 118.63/118.73 cnf(387,plain, % 118.63/118.73 (E(f9(f2(a1),a3),f9(a13,a3))), % 118.63/118.73 inference(scs_inference,[],[373,380,138,2,3])). % 118.63/118.73 cnf(400,plain, % 118.63/118.73 (E(f4(a1),f15(f4(f2(a1))))), % 118.63/118.73 inference(scs_inference,[],[133,2])). % 118.63/118.73 cnf(401,plain, % 118.63/118.73 (E(f4(a28),f15(f4(f2(a1))))), % 118.63/118.73 inference(scs_inference,[],[46,133,2,3])). % 118.63/118.73 cnf(406,plain, % 118.63/118.73 (E(f15(f4(f2(a1))),f4(a28))), % 118.63/118.73 inference(scs_inference,[],[401,2])). % 118.63/118.73 cnf(407,plain, % 118.63/118.73 (E(f15(f4(a27)),f15(f4(f2(a1))))), % 118.63/118.73 inference(scs_inference,[],[48,401,2,3])). % 118.63/118.73 cnf(412,plain, % 118.63/118.73 (E(f15(f4(f2(a1))),f15(f4(a27)))), % 118.63/118.73 inference(scs_inference,[],[407,2])). % 118.63/118.73 cnf(416,plain, % 118.63/118.73 (E(f4(f2(a1)),f4(f2(a28)))), % 118.63/118.73 inference(scs_inference,[],[142,2])). % 118.63/118.73 cnf(420,plain, % 118.63/118.73 (P2(f11(f10(f8(a23,a26),f8(a23,a26))))), % 118.63/118.73 inference(scs_inference,[],[290,73,91])). % 118.63/118.73 cnf(421,plain, % 118.63/118.73 (E(f5(a1,a1),f10(f5(f2(a1),f2(a1)),f8(f9(a1,f4(a1)),f9(a1,f4(a1)))))), % 118.63/118.73 inference(scs_inference,[],[140,2])). % 118.63/118.73 cnf(442,plain, % 118.63/118.73 (~P1(f4(a1))+P1(f15(f4(a27)))), % 118.63/118.73 inference(scs_inference,[],[370,19])). % 118.63/118.73 cnf(443,plain, % 118.63/118.73 (P1(f15(f4(a27)))+~P1(f15(f4(a13)))), % 118.63/118.73 inference(scs_inference,[],[370,19,366])). % 118.63/118.73 cnf(444,plain, % 118.63/118.73 (~P1(f4(a13))+P1(f15(f4(a27)))), % 118.63/118.73 inference(scs_inference,[],[370,19,366,71])). % 118.63/118.73 cnf(455,plain, % 118.63/118.73 (P4(x4551,f8(a12,a12))+~E(f8(a12,a12),x4551)), % 118.63/118.73 inference(scs_inference,[],[144,21])). % 118.63/118.73 cnf(461,plain, % 118.63/118.73 (~P1(f4(a13))+P1(f4(a28))), % 118.63/118.73 inference(scs_inference,[],[155,19,71])). % 118.63/118.73 cnf(485,plain, % 118.63/118.73 (~P1(f4(a27))+P1(f15(f4(a13)))), % 118.63/118.73 inference(scs_inference,[],[373,19,71])). % 118.63/118.73 cnf(496,plain, % 118.63/118.73 (P4(f8(a12,a12),x4961)+~E(f8(a12,a12),x4961)), % 118.63/118.73 inference(scs_inference,[],[144,61,155,363,20,21,19,22])). % 118.63/118.73 cnf(502,plain, % 118.63/118.73 (P4(a12,f10(a12,a12))), % 118.63/118.73 inference(scs_inference,[],[29,81,108])). % 118.63/118.73 cnf(506,plain, % 118.63/118.73 (P4(f8(a12,f11(a12)),x5061)+~E(f8(f11(a12),f11(a12)),x5061)), % 118.63/118.73 inference(scs_inference,[],[257,502,225,373,138,21,20,19,22])). % 118.63/118.73 cnf(509,plain, % 118.63/118.73 (E(f4(a27),f4(a13))+~P1(f4(a13))+~P1(f4(a27))), % 118.63/118.73 inference(scs_inference,[],[257,502,225,302,373,138,21,86])). % 118.63/118.73 cnf(512,plain, % 118.63/118.73 (P4(x5121,f10(f10(f8(a23,a23),f8(a23,a26)),f10(f8(a26,a23),f8(a26,a26))))+~E(f10(f10(f8(a24,a24),f8(a24,a24)),f10(f8(a24,a24),f8(a24,a24))),x5121)), % 118.63/118.73 inference(scs_inference,[],[65,363,20,21])). % 118.63/118.73 cnf(513,plain, % 118.63/118.73 (~P1(f4(a1))+P1(f15(f4(f2(a1))))), % 118.63/118.73 inference(scs_inference,[],[65,363,400,20,21,19])). % 118.63/118.73 cnf(525,plain, % 118.63/118.73 (P4(x5251,f10(f8(a23,a23),f8(a26,a26)))+~E(f10(f8(a24,a24),f8(a24,a24)),x5251)), % 118.63/118.73 inference(scs_inference,[],[63,21])). % 118.63/118.73 cnf(531,plain, % 118.63/118.73 (~P1(f4(f2(a1)))+P1(f4(a28))), % 118.63/118.73 inference(scs_inference,[],[406,19,71])). % 118.63/118.73 cnf(534,plain, % 118.63/118.73 (~P2(f9(f2(a1),a3))+P2(f9(a1,a3))), % 118.63/118.73 inference(scs_inference,[],[138,20])). % 118.63/118.73 cnf(543,plain, % 118.63/118.73 (~P1(f4(a27))+P1(f15(f4(f2(a1))))), % 118.63/118.73 inference(scs_inference,[],[407,19,443,71])). % 118.63/118.73 cnf(561,plain, % 118.63/118.73 (~P1(f4(f2(a1)))+P1(f15(f4(a27)))), % 118.63/118.73 inference(scs_inference,[],[412,19,71])). % 118.63/118.73 cnf(566,plain, % 118.63/118.73 (P4(f10(f10(f8(a24,a24),f8(a24,a24)),f10(f8(a24,a24),f8(a24,a24))),x5661)+~E(f10(f10(f8(a23,a23),f8(a23,a26)),f10(f8(a26,a23),f8(a26,a26))),x5661)), % 118.63/118.73 inference(scs_inference,[],[65,407,251,20,19,22])). % 118.63/118.73 cnf(619,plain, % 118.63/118.73 (~P1(f4(a1))+P1(f4(a28))), % 118.63/118.73 inference(scs_inference,[],[130,19])). % 118.63/118.73 cnf(630,plain, % 118.63/118.73 (P2(f10(f5(f2(a1),f2(a1)),f8(f9(a1,f4(a1)),f9(a1,f4(a1)))))), % 118.63/118.73 inference(scs_inference,[],[421,42,20,102])). % 118.63/118.73 cnf(633,plain, % 118.63/118.73 (P2(f5(a1,a1))), % 118.63/118.73 inference(scs_inference,[],[630,140,20])). % 118.63/118.73 cnf(645,plain, % 118.63/118.73 (~P2(f9(f2(a1),a3))+P2(f9(a13,a3))), % 118.63/118.73 inference(scs_inference,[],[387,20])). % 118.63/118.73 cnf(780,plain, % 118.63/118.73 (~P4(a12,f5(a13,a13))+P4(f8(a12,f5(a13,a13)),f8(f5(a13,a13),f5(a13,a13)))), % 118.63/118.73 inference(scs_inference,[],[136,342,328,29,107,116])). % 118.63/118.73 cnf(981,plain, % 118.63/118.73 (~E(f15(f15(f15(f4(f2(a28))))),a3)), % 118.63/118.73 inference(scs_inference,[],[301,70,71])). % 118.63/118.73 cnf(1027,plain, % 118.63/118.73 (P5(f4(f2(a28)),f15(f4(f2(a28))))), % 118.63/118.73 inference(scs_inference,[],[170,85,72])). % 118.63/118.73 cnf(1028,plain, % 118.63/118.73 (P5(f4(f2(a1)),f15(f4(f2(a28))))), % 118.63/118.73 inference(scs_inference,[],[142,1027,24])). % 118.63/118.73 cnf(1029,plain, % 118.63/118.73 (P5(f4(f2(a28)),x10291)+~E(f15(f4(f2(a28))),x10291)), % 118.63/118.73 inference(scs_inference,[],[142,1027,24,25])). % 118.63/118.73 cnf(1034,plain, % 118.63/118.73 (P5(f4(f2(a1)),x10341)+~E(f15(f4(f2(a28))),x10341)), % 118.63/118.73 inference(scs_inference,[],[1028,25])). % 118.63/118.73 cnf(1078,plain, % 118.63/118.73 (P1(f4(a1))), % 118.63/118.73 inference(scs_inference,[],[43,186,72])). % 118.63/118.73 cnf(1079,plain, % 118.63/118.73 (P1(f15(f4(a27)))), % 118.63/118.73 inference(scs_inference,[],[1078,442])). % 118.63/118.73 cnf(1081,plain, % 118.63/118.73 (P1(f15(f4(f2(a1))))), % 118.63/118.73 inference(scs_inference,[],[1078,513])). % 118.63/118.73 cnf(1082,plain, % 118.63/118.73 (P1(f4(a28))), % 118.63/118.73 inference(scs_inference,[],[1078,619])). % 118.63/118.73 cnf(1083,plain, % 118.63/118.73 (E(f9(f2(a1),f4(a1)),f9(a1,f4(a1)))), % 118.63/118.73 inference(scs_inference,[],[67,1078,42,125])). % 118.63/118.73 cnf(1085,plain, % 118.63/118.73 (E(f9(a13,f4(a1)),f9(a1,f4(a1)))), % 118.63/118.73 inference(scs_inference,[],[154,67,1078,42,125,101])). % 118.63/118.73 cnf(1087,plain, % 118.63/118.73 (E(f9(a1,f4(a1)),f9(f2(a1),f4(a1)))), % 118.63/118.73 inference(scs_inference,[],[154,67,1078,42,125,101,2])). % 118.63/118.73 cnf(1088,plain, % 118.63/118.73 (E(x10881,f9(a1,f4(a1)))+~E(x10881,f9(a13,f4(a1)))), % 118.63/118.73 inference(scs_inference,[],[154,67,1078,42,125,101,2,3])). % 118.63/118.73 cnf(1098,plain, % 118.63/118.73 (P1(f4(a28))), % 118.63/118.73 inference(scs_inference,[],[1079,344])). % 118.63/118.73 cnf(1111,plain, % 118.63/118.73 (E(f9(a1,f4(a1)),f9(a13,f4(a1)))), % 118.63/118.73 inference(scs_inference,[],[1085,2])). % 118.63/118.73 cnf(1112,plain, % 118.63/118.73 (E(a14,f9(f2(a1),f4(a1)))), % 118.63/118.73 inference(scs_inference,[],[302,1087,1085,2,3])). % 118.63/118.73 cnf(1113,plain, % 118.63/118.73 (P2(f9(f2(a1),f4(a1)))), % 118.63/118.73 inference(scs_inference,[],[305,302,1087,1085,2,3,20])). % 118.63/118.73 cnf(1116,plain, % 118.63/118.73 (P4(a14,f9(f2(a1),f4(a1)))), % 118.63/118.73 inference(scs_inference,[],[305,302,1087,1085,2,3,20,90,174])). % 118.63/118.73 cnf(1119,plain, % 118.63/118.73 (P4(f9(f2(a1),f4(a1)),f9(a1,f4(a1)))), % 118.63/118.73 inference(scs_inference,[],[305,302,1087,1085,1083,2,3,20,90,174,23,21,22])). % 118.63/118.73 cnf(1124,plain, % 118.63/118.73 (E(a14,f9(a13,f4(a1)))), % 118.63/118.73 inference(scs_inference,[],[302,1111,1112,2,3])). % 118.63/118.73 cnf(1125,plain, % 118.63/118.73 (P2(f9(a13,f4(a1)))), % 118.63/118.73 inference(scs_inference,[],[305,302,1111,1112,2,3,20])). % 118.63/118.73 cnf(1126,plain, % 118.63/118.73 (P4(f9(f2(a1),f4(a1)),a14)), % 118.63/118.73 inference(scs_inference,[],[1119,59,305,302,1111,1112,2,3,20,22])). % 118.63/118.73 cnf(1341,plain, % 118.63/118.73 (E(f9(f2(a1),f4(a28)),f9(a1,f4(a28)))), % 118.63/118.73 inference(scs_inference,[],[67,1082,42,125])). % 118.63/118.73 cnf(1343,plain, % 118.63/118.73 (E(f9(a13,f4(a28)),f9(a1,f4(a28)))), % 118.63/118.73 inference(scs_inference,[],[67,154,1082,42,125,101])). % 118.63/118.73 cnf(1345,plain, % 118.63/118.73 (E(f9(a1,f4(a28)),f9(f2(a1),f4(a28)))), % 118.63/118.73 inference(scs_inference,[],[67,154,1082,42,125,101,2])). % 118.63/118.73 cnf(1346,plain, % 118.63/118.73 (E(x13461,f9(a1,f4(a28)))+~E(x13461,f9(a13,f4(a28)))), % 118.63/118.73 inference(scs_inference,[],[67,154,1082,42,125,101,2,3])). % 118.63/118.73 cnf(1351,plain, % 118.63/118.73 (E(f9(a1,f4(a28)),f9(a13,f4(a28)))), % 118.63/118.73 inference(scs_inference,[],[1343,2])). % 118.63/118.73 cnf(1352,plain, % 118.63/118.73 (E(f9(a13,f4(a28)),f9(f2(a1),f4(a28)))), % 118.63/118.73 inference(scs_inference,[],[1345,1343,2,3])). % 118.63/118.73 cnf(1356,plain, % 118.63/118.73 (E(f9(f2(a1),f4(a28)),f9(a13,f4(a28)))), % 118.63/118.73 inference(scs_inference,[],[1352,2])). % 118.63/118.73 cnf(1371,plain, % 118.63/118.73 (~P2(f9(f2(a1),f4(a28)))+P2(f9(a1,f4(a28)))), % 118.63/118.73 inference(scs_inference,[],[1341,1343,23,20])). % 118.63/118.73 cnf(1377,plain, % 118.63/118.73 (~P2(f9(a1,f4(a28)))+P2(f9(a13,f4(a28)))), % 118.63/118.73 inference(scs_inference,[],[1351,1352,23,20])). % 118.63/118.73 cnf(1510,plain, % 118.63/118.73 (P4(f9(f2(a1),f4(a1)),f9(a13,f4(a1)))), % 118.63/118.73 inference(scs_inference,[],[1126,1124,22])). % 118.63/118.73 cnf(1512,plain, % 118.63/118.73 (E(f9(a13,f4(a1)),f9(f2(a1),f4(a1)))), % 118.63/118.73 inference(scs_inference,[],[1116,1126,1125,1113,1124,22,21,103])). % 118.63/118.73 cnf(1999,plain, % 118.63/118.73 (E(f15(f4(a13)),f15(f4(f2(a1))))), % 118.63/118.73 inference(scs_inference,[],[47,400,3])). % 118.63/118.73 cnf(2000,plain, % 118.63/118.73 (E(f15(f4(f2(a1))),f15(f4(a13)))), % 118.63/118.73 inference(scs_inference,[],[47,400,3,2])). % 118.63/118.73 cnf(3632,plain, % 118.63/118.73 (E(f9(f2(a1),f15(f4(f2(a1)))),f9(a1,f15(f4(f2(a1)))))), % 118.63/118.73 inference(scs_inference,[],[67,1081,42,125])). % 118.63/118.73 cnf(3634,plain, % 118.63/118.73 (E(f9(a13,f15(f4(f2(a1)))),f9(a1,f15(f4(f2(a1)))))), % 118.63/118.73 inference(scs_inference,[],[67,154,1081,42,125,101])). % 118.63/118.73 cnf(3648,plain, % 118.63/118.73 (E(f4(f2(a1)),f4(a13))+~P1(f4(a13))+~P1(f4(f2(a1)))), % 118.63/118.73 inference(scs_inference,[],[2000,3632,3634,2,3,86])). % 118.63/118.73 cnf(3653,plain, % 118.63/118.73 (~E(f15(f4(a28)),a3)), % 118.63/118.73 inference(scs_inference,[],[1098,420,73,85,70])). % 118.63/118.73 cnf(3663,plain, % 118.63/118.73 (P4(a12,f5(a27,a27))), % 118.63/118.73 inference(scs_inference,[],[45,1098,420,73,85,70,74,79,80,94,95])). % 118.63/118.73 cnf(3680,plain, % 118.63/118.73 (E(f10(f9(a13,f4(a1)),x36801),f10(f9(f2(a1),f4(a1)),x36801))), % 118.63/118.73 inference(scs_inference,[],[1512,45,1098,420,73,85,70,74,79,80,94,95,76,77,4,7,8,9,16,83,84,5,6,10])). % 118.63/118.73 cnf(3681,plain, % 118.63/118.73 (E(f10(x36811,f9(a13,f4(a1))),f10(x36811,f9(f2(a1),f4(a1))))), % 118.63/118.73 inference(scs_inference,[],[1512,45,1098,420,73,85,70,74,79,80,94,95,76,77,4,7,8,9,16,83,84,5,6,10,11])). % 118.63/118.73 cnf(3690,plain, % 118.63/118.73 (E(f9(a28,f4(a28)),f9(a27,f4(a28)))), % 118.63/118.73 inference(scs_inference,[],[1512,45,1098,301,420,73,85,70,74,79,80,94,95,76,77,4,7,8,9,16,83,84,5,6,10,11,12,13,14,15,17,18,87,88])). % 118.63/118.73 cnf(3692,plain, % 118.63/118.73 (P1(f15(f4(a28)))), % 118.63/118.73 inference(scs_inference,[],[1512,45,1098,301,420,73,85,70,74,79,80,94,95,76,77,4,7,8,9,16,83,84,5,6,10,11,12,13,14,15,17,18,87,88,71])). % 118.63/118.73 cnf(3694,plain, % 118.63/118.73 (P1(f4(a27))), % 118.63/118.73 inference(scs_inference,[],[1512,45,1098,301,420,73,85,70,74,79,80,94,95,76,77,4,7,8,9,16,83,84,5,6,10,11,12,13,14,15,17,18,87,88,71,72])). % 118.63/118.73 cnf(3701,plain, % 118.63/118.73 (P1(f6(f4(a1)))), % 118.63/118.73 inference(scs_inference,[],[981,1512,45,1098,1078,301,420,67,73,85,70,74,79,80,94,95,76,77,4,7,8,9,16,83,84,5,6,10,11,12,13,14,15,17,18,87,88,71,72,2,91,92,75])). % 118.63/118.73 cnf(3703,plain, % 118.63/118.73 (E(f15(f6(f4(a1))),f4(a1))), % 118.63/118.73 inference(scs_inference,[],[981,1512,45,1098,1078,301,420,67,73,85,70,74,79,80,94,95,76,77,4,7,8,9,16,83,84,5,6,10,11,12,13,14,15,17,18,87,88,71,72,2,91,92,75,78])). % 118.63/118.73 cnf(3711,plain, % 118.63/118.73 (P2(f9(a27,f4(a28)))), % 118.63/118.73 inference(scs_inference,[],[981,1512,45,1098,1078,301,420,633,67,73,85,70,74,79,80,94,95,76,77,4,7,8,9,16,83,84,5,6,10,11,12,13,14,15,17,18,87,88,71,72,2,91,92,75,78,100,104,105,93])). % 118.63/118.73 cnf(3713,plain, % 118.63/118.73 (P2(f5(f2(a1),f2(a1)))), % 118.63/118.73 inference(scs_inference,[],[981,1512,45,1098,1078,301,420,633,131,67,73,85,70,74,79,80,94,95,76,77,4,7,8,9,16,83,84,5,6,10,11,12,13,14,15,17,18,87,88,71,72,2,91,92,75,78,100,104,105,93,126])). % 118.63/118.73 cnf(3715,plain, % 118.63/118.73 (~E(f15(f4(a13)),a3)), % 118.63/118.73 inference(scs_inference,[],[981,1512,360,45,1098,1078,301,420,633,131,67,73,85,70,74,79,80,94,95,76,77,4,7,8,9,16,83,84,5,6,10,11,12,13,14,15,17,18,87,88,71,72,2,91,92,75,78,100,104,105,93,126,3])). % 118.63/118.73 cnf(3724,plain, % 118.63/118.73 (P2(f5(a1,a28))), % 118.63/118.73 inference(scs_inference,[],[981,1512,360,45,130,1098,1078,301,420,633,131,43,67,42,73,85,70,74,79,80,94,95,76,77,4,7,8,9,16,83,84,5,6,10,11,12,13,14,15,17,18,87,88,71,72,2,91,92,75,78,100,104,105,93,126,3,110,111,113,114,102])). % 118.63/118.73 cnf(3726,plain, % 118.63/118.73 (~E(f15(f4(a1)),f15(a3))), % 118.63/118.73 inference(scs_inference,[],[981,1512,360,45,130,1098,1078,301,28,420,633,131,43,67,42,73,85,70,74,79,80,94,95,76,77,4,7,8,9,16,83,84,5,6,10,11,12,13,14,15,17,18,87,88,71,72,2,91,92,75,78,100,104,105,93,126,3,110,111,113,114,102,86])). % 118.63/118.73 cnf(3734,plain, % 118.63/118.73 (P4(f10(f9(f2(a1),f4(a1)),f9(f2(a1),f4(a1))),f10(f9(a13,f4(a1)),f9(a13,f4(a1))))), % 118.63/118.73 inference(scs_inference,[],[981,1512,1510,360,45,130,1098,1078,301,28,420,633,131,1125,1113,43,226,228,46,67,42,73,85,70,74,79,80,94,95,76,77,4,7,8,9,16,83,84,5,6,10,11,12,13,14,15,17,18,87,88,71,72,2,91,92,75,78,100,104,105,93,126,3,110,111,113,114,102,86,109,120,118,115])). % 118.63/118.73 cnf(3747,plain, % 118.63/118.73 (E(f4(a27),f4(a13))+~P1(f4(a13))), % 118.63/118.73 inference(scs_inference,[],[981,1512,1510,360,339,45,268,278,130,1098,1078,301,28,420,633,131,1125,1113,254,43,33,226,228,46,67,42,73,85,70,74,79,80,94,95,76,77,4,7,8,9,16,83,84,5,6,10,11,12,13,14,15,17,18,87,88,71,72,2,91,92,75,78,100,104,105,93,126,3,110,111,113,114,102,86,109,120,118,115,81,123,22,24,21,108,116,509])). % 118.63/118.73 cnf(3748,plain, % 118.63/118.73 (P1(f4(a28))), % 118.63/118.73 inference(scs_inference,[],[3694,345])). % 118.63/118.73 cnf(3749,plain, % 118.63/118.73 (P1(f15(f4(a13)))), % 118.63/118.73 inference(scs_inference,[],[3694,485])). % 118.63/118.73 cnf(3750,plain, % 118.63/118.73 (P1(f15(f4(f2(a1))))), % 118.63/118.73 inference(scs_inference,[],[3694,543])). % 118.63/118.73 cnf(3754,plain, % 118.63/118.73 (E(f10(f5(a1,a28),a12),f5(a1,a28))), % 118.63/118.73 inference(scs_inference,[],[3724,81,79])). % 118.63/118.73 cnf(3756,plain, % 118.63/118.73 (E(f8(a12,f5(a1,a28)),a12)), % 118.63/118.73 inference(scs_inference,[],[3724,81,79,77])). % 118.63/118.73 cnf(3762,plain, % 118.63/118.73 (P4(a12,f5(f2(a1),f2(a1)))), % 118.63/118.73 inference(scs_inference,[],[3694,3724,131,81,79,77,85,94,95])). % 118.63/118.73 cnf(3766,plain, % 118.63/118.73 (E(f10(a12,f5(a1,a28)),f5(a1,a28))), % 118.63/118.73 inference(scs_inference,[],[3694,3724,3690,131,81,79,77,85,94,95,10,14,80])). % 118.63/118.73 cnf(3775,plain, % 118.63/118.73 (E(f9(a13,f4(a27)),f9(a1,f4(a27)))), % 118.63/118.73 inference(scs_inference,[],[3694,3724,3690,131,81,79,77,85,94,95,10,14,80,8,18,12,15,9,88,87])). % 118.63/118.73 cnf(3777,plain, % 118.63/118.73 (E(f8(f5(a1,a28),a12),a12)), % 118.63/118.73 inference(scs_inference,[],[3694,3724,3690,131,81,79,77,85,94,95,10,14,80,8,18,12,15,9,88,87,76])). % 118.63/118.73 cnf(3787,plain, % 118.63/118.73 (P2(f11(f5(a1,a28)))), % 118.63/118.73 inference(scs_inference,[],[3694,3724,3690,131,81,79,77,85,94,95,10,14,80,8,18,12,15,9,88,87,76,84,7,74,83,13,73])). % 118.63/118.73 cnf(3789,plain, % 118.63/118.73 (~E(f15(f4(a27)),a3)), % 118.63/118.73 inference(scs_inference,[],[3694,3724,3690,131,81,79,77,85,94,95,10,14,80,8,18,12,15,9,88,87,76,84,7,74,83,13,73,70])). % 118.63/118.73 cnf(3796,plain, % 118.63/118.73 (P1(f15(f15(f4(a28))))), % 118.63/118.73 inference(scs_inference,[],[3694,3724,3692,3690,131,81,79,77,85,94,95,10,14,80,8,18,12,15,9,88,87,76,84,7,74,83,13,73,70,4,5,6,16,11,71])). % 118.63/118.73 cnf(3799,plain, % 118.63/118.73 (P1(f4(f2(a1)))), % 118.63/118.73 inference(scs_inference,[],[3694,3724,3692,3690,131,81,79,77,85,94,95,10,14,80,8,18,12,15,9,88,87,76,84,7,74,83,13,73,70,4,5,6,16,11,71,17,72])). % 118.63/118.73 cnf(3804,plain, % 118.63/118.73 (P1(f6(f15(f4(a28))))), % 118.63/118.73 inference(scs_inference,[],[3694,3724,3726,3692,3653,3690,131,81,79,77,85,94,95,10,14,80,8,18,12,15,9,88,87,76,84,7,74,83,13,73,70,4,5,6,16,11,71,17,72,2,105,75])). % 118.63/118.73 cnf(3812,plain, % 118.63/118.73 (P2(f10(f5(a1,a28),f5(a1,a28)))), % 118.63/118.73 inference(scs_inference,[],[3694,3724,3726,3692,3653,3690,131,81,79,77,85,94,95,10,14,80,8,18,12,15,9,88,87,76,84,7,74,83,13,73,70,4,5,6,16,11,71,17,72,2,105,75,92,78,104,91])). % 118.63/118.73 cnf(3816,plain, % 118.63/118.73 (P2(f9(a27,f4(a27)))), % 118.63/118.73 inference(scs_inference,[],[3694,3724,3726,3692,3653,3690,45,131,81,79,77,85,94,95,10,14,80,8,18,12,15,9,88,87,76,84,7,74,83,13,73,70,4,5,6,16,11,71,17,72,2,105,75,92,78,104,91,100,93])). % 118.63/118.73 cnf(3818,plain, % 118.63/118.73 (P2(f5(f2(a28),f2(a28)))), % 118.63/118.73 inference(scs_inference,[],[3694,3724,3726,3692,3653,3690,45,131,170,81,79,77,85,94,95,10,14,80,8,18,12,15,9,88,87,76,84,7,74,83,13,73,70,4,5,6,16,11,71,17,72,2,105,75,92,78,104,91,100,93,126])). % 118.63/118.73 cnf(3820,plain, % 118.63/118.73 (E(f15(f6(f4(a1))),f15(f4(a27)))), % 118.63/118.73 inference(scs_inference,[],[3694,3724,3726,3692,3653,3690,3703,370,45,131,170,81,79,77,85,94,95,10,14,80,8,18,12,15,9,88,87,76,84,7,74,83,13,73,70,4,5,6,16,11,71,17,72,2,105,75,92,78,104,91,100,93,126,3])). % 118.63/118.73 cnf(3821,plain, % 118.63/118.73 (P1(f4(f2(a28)))), % 118.63/118.73 inference(scs_inference,[],[3694,3724,3726,3692,3653,3690,3703,370,45,416,131,170,81,79,77,85,94,95,10,14,80,8,18,12,15,9,88,87,76,84,7,74,83,13,73,70,4,5,6,16,11,71,17,72,2,105,75,92,78,104,91,100,93,126,3,19])). % 118.63/118.73 cnf(3834,plain, % 118.63/118.73 (P4(f10(a12,f5(a1,a28)),f10(f5(a27,a27),f5(a1,a28)))), % 118.63/118.73 inference(scs_inference,[],[3663,3694,3724,3726,3713,3692,3653,3690,3703,370,45,416,131,170,254,29,81,79,77,85,94,95,10,14,80,8,18,12,15,9,88,87,76,84,7,74,83,13,73,70,4,5,6,16,11,71,17,72,2,105,75,92,78,104,91,100,93,126,3,19,114,111,113,110,108,120,115])). % 118.63/118.73 cnf(3836,plain, % 118.63/118.73 (E(f15(f6(f4(a1))),f4(a28))), % 118.63/118.73 inference(scs_inference,[],[3663,3694,3724,3726,3713,3692,3653,3690,3703,370,45,416,131,170,254,29,81,79,77,85,94,95,10,14,80,8,18,12,15,9,88,87,76,84,7,74,83,13,73,70,4,5,6,16,11,71,17,72,2,105,75,92,78,104,91,100,93,126,3,19,114,111,113,110,108,120,115,285])). % 118.63/118.73 cnf(3839,plain, % 118.63/118.73 (P5(f4(a27),f4(a1))), % 118.63/118.73 inference(scs_inference,[],[3663,3694,3724,3726,3713,3692,3653,3690,3703,370,135,45,416,131,170,254,29,81,79,77,85,94,95,10,14,80,8,18,12,15,9,88,87,76,84,7,74,83,13,73,70,4,5,6,16,11,71,17,72,2,105,75,92,78,104,91,100,93,126,3,19,114,111,113,110,108,120,115,285,121,25])). % 118.63/118.73 cnf(3846,plain, % 118.63/118.73 (E(f4(f2(a1)),f4(a13))+~P1(f4(a13))), % 118.63/118.73 inference(scs_inference,[],[3663,3694,3724,3726,3713,3692,3653,3690,3703,370,135,45,269,416,131,170,254,67,42,29,81,79,77,85,94,95,10,14,80,8,18,12,15,9,88,87,76,84,7,74,83,13,73,70,4,5,6,16,11,71,17,72,2,105,75,92,78,104,91,100,93,126,3,19,114,111,113,110,108,120,115,285,121,25,125,109,116,3648])). % 118.63/118.73 cnf(3847,plain, % 118.63/118.73 (P1(f4(a28))), % 118.63/118.73 inference(scs_inference,[],[3799,531])). % 118.63/118.73 cnf(3848,plain, % 118.63/118.73 (P1(f15(f4(a27)))), % 118.63/118.73 inference(scs_inference,[],[3799,561])). % 118.63/118.73 cnf(3859,plain, % 118.63/118.73 (~E(f15(f6(f4(a1))),a3)), % 118.63/118.73 inference(scs_inference,[],[3818,3701,79,94,74,81,70])). % 118.63/118.73 cnf(3863,plain, % 118.63/118.73 (P4(a12,f5(f2(a28),f2(a28)))), % 118.63/118.73 inference(scs_inference,[],[3818,3701,170,79,94,74,81,70,77,95])). % 118.63/118.73 cnf(3868,plain, % 118.63/118.73 (P5(f6(f4(a1)),f15(f6(f4(a1))))), % 118.63/118.73 inference(scs_inference,[],[3754,3818,3701,170,79,94,74,81,70,77,95,15,8,9,85])). % 118.63/118.73 cnf(3876,plain, % 118.63/118.73 (P2(f11(f5(f2(a28),f2(a28))))), % 118.63/118.73 inference(scs_inference,[],[3754,3818,3701,170,79,94,74,81,70,77,95,15,8,9,85,88,80,84,73])). % 118.63/118.73 cnf(3890,plain, % 118.63/118.73 (P1(f15(f6(f4(a1))))), % 118.63/118.73 inference(scs_inference,[],[3754,3818,3701,170,79,94,74,81,70,77,95,15,8,9,85,88,80,84,73,12,76,10,13,83,87,18,4,14,71])). % 118.63/118.73 cnf(3898,plain, % 118.63/118.73 (P1(f4(a13))), % 118.63/118.73 inference(scs_inference,[],[3754,3818,3701,170,44,79,94,74,81,70,77,95,15,8,9,85,88,80,84,73,12,76,10,13,83,87,18,4,14,71,6,7,16,11,5,17,72])). % 118.63/118.73 cnf(3900,plain, % 118.63/118.73 (~E(a3,f15(f4(a13)))), % 118.63/118.73 inference(scs_inference,[],[3754,3818,3701,3715,170,44,79,94,74,81,70,77,95,15,8,9,85,88,80,84,73,12,76,10,13,83,87,18,4,14,71,6,7,16,11,5,17,72,2])). % 118.63/118.73 cnf(3903,plain, % 118.63/118.73 (P1(f6(f15(f4(a13))))), % 118.63/118.73 inference(scs_inference,[],[3754,3818,3701,3749,3715,170,44,79,94,74,81,70,77,95,15,8,9,85,88,80,84,73,12,76,10,13,83,87,18,4,14,71,6,7,16,11,5,17,72,2,105,75])). % 118.63/118.73 cnf(3911,plain, % 118.63/118.73 (E(f15(f6(f15(f4(a13)))),f15(f4(a13)))), % 118.63/118.73 inference(scs_inference,[],[3754,3818,3701,3749,3715,170,44,79,94,74,81,70,77,95,15,8,9,85,88,80,84,73,12,76,10,13,83,87,18,4,14,71,6,7,16,11,5,17,72,2,105,75,91,92,104,78])). % 118.63/118.73 cnf(3917,plain, % 118.63/118.73 (P2(f5(a28,a28))), % 118.63/118.73 inference(scs_inference,[],[3754,3818,3701,3749,3715,45,170,43,44,79,94,74,81,70,77,95,15,8,9,85,88,80,84,73,12,76,10,13,83,87,18,4,14,71,6,7,16,11,5,17,72,2,105,75,91,92,104,78,100,93,126])). % 118.63/118.73 cnf(3919,plain, % 118.63/118.73 (~E(f15(f4(f2(a1))),a3)), % 118.63/118.73 inference(scs_inference,[],[3754,3818,3701,3749,3715,3789,407,45,170,43,44,79,94,74,81,70,77,95,15,8,9,85,88,80,84,73,12,76,10,13,83,87,18,4,14,71,6,7,16,11,5,17,72,2,105,75,91,92,104,78,100,93,126,3])). % 118.63/118.73 cnf(3936,plain, % 118.63/118.73 (E(f4(a27),f4(a13))), % 118.63/118.73 inference(scs_inference,[],[3754,3818,3701,3749,3762,3715,3789,3713,407,45,170,328,43,44,79,94,74,81,70,77,95,15,8,9,85,88,80,84,73,12,76,10,13,83,87,18,4,14,71,6,7,16,11,5,17,72,2,105,75,91,92,104,78,100,93,126,3,111,114,113,110,108,120,115,116,3747])). % 118.63/118.73 cnf(3947,plain, % 118.63/118.73 (P1(f15(f4(a27)))), % 118.63/118.73 inference(scs_inference,[],[3898,444])). % 118.63/118.73 cnf(3948,plain, % 118.63/118.73 (P1(f4(a28))), % 118.63/118.73 inference(scs_inference,[],[3898,461])). % 118.63/118.73 cnf(3949,plain, % 118.63/118.73 (E(f4(f2(a1)),f4(a13))), % 118.63/118.73 inference(scs_inference,[],[3898,3846])). % 118.63/118.73 cnf(3950,plain, % 118.63/118.73 (P4(a12,f8(f5(a28,a28),f5(a28,a28)))), % 118.63/118.73 inference(scs_inference,[],[3917,94])). % 118.63/118.73 cnf(3952,plain, % 118.63/118.73 (~E(f15(f4(f2(a28))),a3)), % 118.63/118.73 inference(scs_inference,[],[3917,3821,94,70])). % 118.63/118.73 cnf(3954,plain, % 118.63/118.73 (E(f10(a12,f5(a28,a28)),f5(a28,a28))), % 118.63/118.73 inference(scs_inference,[],[3917,3821,94,70,80])). % 118.63/118.73 cnf(3958,plain, % 118.63/118.73 (E(f10(f5(a28,a28),a12),f5(a28,a28))), % 118.63/118.73 inference(scs_inference,[],[3917,3821,94,70,80,84,79])). % 118.63/118.73 cnf(3960,plain, % 118.63/118.73 (E(f9(a28,f4(a13)),f9(a27,f4(a13)))), % 118.63/118.73 inference(scs_inference,[],[3898,3917,3821,94,70,80,84,79,88])). % 118.63/118.73 cnf(3962,plain, % 118.63/118.73 (P4(a12,f5(a28,a28))), % 118.63/118.73 inference(scs_inference,[],[3898,3917,3821,43,94,70,80,84,79,88,95])). % 118.63/118.73 cnf(3968,plain, % 118.63/118.73 (P1(f15(f15(f4(a27))))), % 118.63/118.73 inference(scs_inference,[],[3898,3917,3821,3848,43,94,70,80,84,79,88,95,83,77,71])). % 118.63/118.73 cnf(3970,plain, % 118.63/118.73 (P4(f5(a28,a28),f5(a28,a28))), % 118.63/118.73 inference(scs_inference,[],[3898,3917,3821,3848,43,94,70,80,84,79,88,95,83,77,71,81])). % 118.63/118.73 cnf(3977,plain, % 118.63/118.73 (P2(f11(f5(a28,a28)))), % 118.63/118.73 inference(scs_inference,[],[3898,3917,3766,3821,3848,43,94,70,80,84,79,88,95,83,77,71,81,85,9,74,73])). % 118.63/118.73 cnf(3979,plain, % 118.63/118.73 (E(f7(x39791,f4(a27)),f7(x39791,f4(a13)))), % 118.63/118.73 inference(scs_inference,[],[3936,3898,3917,3766,3821,3848,43,94,70,80,84,79,88,95,83,77,71,81,85,9,74,73,18])). % 118.63/118.73 cnf(3980,plain, % 118.63/118.73 (E(f5(f4(a27),x39801),f5(f4(a13),x39801))), % 118.63/118.73 inference(scs_inference,[],[3936,3898,3917,3766,3821,3848,43,94,70,80,84,79,88,95,83,77,71,81,85,9,74,73,18,14])). % 118.63/118.73 cnf(3981,plain, % 118.63/118.73 (E(f9(a13,f4(a13)),f9(a1,f4(a13)))), % 118.63/118.73 inference(scs_inference,[],[3936,3898,3917,3766,3821,3848,43,94,70,80,84,79,88,95,83,77,71,81,85,9,74,73,18,14,87])). % 118.63/118.73 cnf(3983,plain, % 118.63/118.73 (E(f5(x39831,f4(a27)),f5(x39831,f4(a13)))), % 118.63/118.73 inference(scs_inference,[],[3936,3898,3917,3766,3821,3848,43,94,70,80,84,79,88,95,83,77,71,81,85,9,74,73,18,14,87,15])). % 118.63/118.73 cnf(3984,plain, % 118.63/118.73 (E(f8(f5(a28,a28),a12),a12)), % 118.63/118.73 inference(scs_inference,[],[3936,3898,3917,3766,3821,3848,43,94,70,80,84,79,88,95,83,77,71,81,85,9,74,73,18,14,87,15,76])). % 118.63/118.73 cnf(3989,plain, % 118.63/118.73 (E(f10(f4(a27),x39891),f10(f4(a13),x39891))), % 118.63/118.73 inference(scs_inference,[],[3936,3898,3917,3766,3821,3848,43,94,70,80,84,79,88,95,83,77,71,81,85,9,74,73,18,14,87,15,76,8,7,4,10])). % 118.63/118.73 cnf(3994,plain, % 118.63/118.73 (E(f7(f4(a27),x39941),f7(f4(a13),x39941))), % 118.63/118.73 inference(scs_inference,[],[3936,3898,3917,3766,3821,3848,43,94,70,80,84,79,88,95,83,77,71,81,85,9,74,73,18,14,87,15,76,8,7,4,10,13,12,6,5,17])). % 118.63/118.73 cnf(3995,plain, % 118.63/118.73 (E(f10(x39951,f4(a27)),f10(x39951,f4(a13)))), % 118.63/118.73 inference(scs_inference,[],[3936,3898,3917,3766,3821,3848,43,94,70,80,84,79,88,95,83,77,71,81,85,9,74,73,18,14,87,15,76,8,7,4,10,13,12,6,5,17,11])). % 118.63/118.73 cnf(3997,plain, % 118.63/118.73 (~E(a3,f15(f6(f4(a1))))), % 118.63/118.73 inference(scs_inference,[],[3936,3898,3917,3766,3821,3848,3859,43,94,70,80,84,79,88,95,83,77,71,81,85,9,74,73,18,14,87,15,76,8,7,4,10,13,12,6,5,17,11,16,2])). % 118.63/118.73 cnf(4000,plain, % 118.63/118.73 (P1(f6(f15(f4(a27))))), % 118.63/118.73 inference(scs_inference,[],[3936,3898,3917,3766,3821,3848,3859,3789,43,94,70,80,84,79,88,95,83,77,71,81,85,9,74,73,18,14,87,15,76,8,7,4,10,13,12,6,5,17,11,16,2,105,75])). % 118.63/118.73 cnf(4002,plain, % 118.63/118.73 (P2(f10(f5(a28,a28),f5(a28,a28)))), % 118.63/118.73 inference(scs_inference,[],[3936,3898,3917,3766,3821,3848,3859,3789,43,94,70,80,84,79,88,95,83,77,71,81,85,9,74,73,18,14,87,15,76,8,7,4,10,13,12,6,5,17,11,16,2,105,75,91])). % 118.63/118.73 cnf(4004,plain, % 118.63/118.73 (E(f15(f6(f15(f4(a27)))),f15(f4(a27)))), % 118.63/118.73 inference(scs_inference,[],[3936,3898,3917,3766,3821,3848,3859,3789,43,94,70,80,84,79,88,95,83,77,71,81,85,9,74,73,18,14,87,15,76,8,7,4,10,13,12,6,5,17,11,16,2,105,75,91,78])). % 118.63/118.73 cnf(4008,plain, % 118.63/118.73 (P2(f8(f5(a28,a28),f5(a28,a28)))), % 118.63/118.73 inference(scs_inference,[],[3936,3898,3917,3766,3821,3848,3859,3789,43,94,70,80,84,79,88,95,83,77,71,81,85,9,74,73,18,14,87,15,76,8,7,4,10,13,12,6,5,17,11,16,2,105,75,91,78,104,92])). % 118.63/118.73 cnf(4012,plain, % 118.63/118.73 (P2(f9(f2(a1),f4(a28)))), % 118.63/118.73 inference(scs_inference,[],[3936,3748,3898,3917,3766,3821,3848,3859,3789,131,43,94,70,80,84,79,88,95,83,77,71,81,85,9,74,73,18,14,87,15,76,8,7,4,10,13,12,6,5,17,11,16,2,105,75,91,78,104,92,100,93])). % 118.63/118.73 cnf(4014,plain, % 118.63/118.73 (E(f8(a12,f5(a1,a28)),f11(a12))), % 118.63/118.73 inference(scs_inference,[],[3936,3748,3898,3917,3766,3821,3848,3756,3859,3789,131,225,43,94,70,80,84,79,88,95,83,77,71,81,85,9,74,73,18,14,87,15,76,8,7,4,10,13,12,6,5,17,11,16,2,105,75,91,78,104,92,100,93,3])). % 118.63/118.73 cnf(4015,plain, % 118.63/118.73 (P4(f10(f9(f2(a1),f4(a1)),f9(f2(a1),f4(a1))),f10(f9(a13,f4(a1)),f9(f2(a1),f4(a1))))), % 118.63/118.73 inference(scs_inference,[],[3936,3748,3898,3917,3766,3821,3848,3756,3859,3681,3734,3789,131,225,43,94,70,80,84,79,88,95,83,77,71,81,85,9,74,73,18,14,87,15,76,8,7,4,10,13,12,6,5,17,11,16,2,105,75,91,78,104,92,100,93,3,22])). % 118.63/118.73 cnf(4017,plain, % 118.63/118.73 (P2(f9(a27,f4(a13)))), % 118.63/118.73 inference(scs_inference,[],[3936,3748,3898,3917,3766,3816,3821,3848,3756,3859,3681,3734,3789,131,225,43,94,70,80,84,79,88,95,83,77,71,81,85,9,74,73,18,14,87,15,76,8,7,4,10,13,12,6,5,17,11,16,2,105,75,91,78,104,92,100,93,3,22,20])). % 118.63/118.73 cnf(4019,plain, % 118.63/118.73 (E(f10(f8(f5(a28,a28),f5(a28,a28)),f8(f5(a28,a28),f5(a28,a28))),f8(f5(a28,a28),f10(f5(a28,a28),f5(a28,a28))))), % 118.63/118.73 inference(scs_inference,[],[3936,3748,3898,3917,3766,3816,3821,3848,3756,3834,3859,3681,3734,3789,131,225,43,94,70,80,84,79,88,95,83,77,71,81,85,9,74,73,18,14,87,15,76,8,7,4,10,13,12,6,5,17,11,16,2,105,75,91,78,104,92,100,93,3,22,20,21,113])). % 118.63/118.73 cnf(4021,plain, % 118.63/118.73 (E(f8(f8(f5(a28,a28),f5(a28,a28)),f5(a28,a28)),f8(f5(a28,a28),f8(f5(a28,a28),f5(a28,a28))))), % 118.63/118.73 inference(scs_inference,[],[3936,3748,3898,3917,3766,3816,3821,3848,3756,3834,3859,3681,3734,3789,131,225,43,94,70,80,84,79,88,95,83,77,71,81,85,9,74,73,18,14,87,15,76,8,7,4,10,13,12,6,5,17,11,16,2,105,75,91,78,104,92,100,93,3,22,20,21,113,111])). % 118.63/118.73 cnf(4027,plain, % 118.63/118.73 (P4(a12,f10(f5(a28,a28),f5(f2(a28),f2(a28))))), % 118.63/118.73 inference(scs_inference,[],[3936,3748,3898,3917,3766,3816,3821,3848,3863,3756,3834,3859,3681,3734,3789,3818,131,225,43,94,70,80,84,79,88,95,83,77,71,81,85,9,74,73,18,14,87,15,76,8,7,4,10,13,12,6,5,17,11,16,2,105,75,91,78,104,92,100,93,3,22,20,21,113,111,114,110,108])). % 118.63/118.73 cnf(4033,plain, % 118.63/118.73 (E(f15(f6(f15(f4(a27)))),f4(a28))), % 118.83/118.74 inference(scs_inference,[],[3936,3748,3898,3917,3766,3816,3821,3848,3863,3756,3834,3859,3681,3734,3789,3818,131,225,43,94,70,80,84,79,88,95,83,77,71,81,85,9,74,73,18,14,87,15,76,8,7,4,10,13,12,6,5,17,11,16,2,105,75,91,78,104,92,100,93,3,22,20,21,113,111,114,110,108,120,115,285])). % 118.83/118.74 cnf(4040,plain, % 118.83/118.74 (P2(f9(a1,f4(a28)))), % 118.83/118.74 inference(scs_inference,[],[4012,1371])). % 118.83/118.74 cnf(4045,plain, % 118.83/118.74 (~E(f15(f15(f4(a27))),a3)), % 118.83/118.74 inference(scs_inference,[],[4012,3947,79,70])). % 118.83/118.74 cnf(4049,plain, % 118.83/118.74 (P1(f15(f15(f4(f2(a1)))))), % 118.83/118.74 inference(scs_inference,[],[4012,3947,3750,79,70,94,71])). % 118.83/118.74 cnf(4063,plain, % 118.83/118.74 (P4(f9(f2(a1),f4(a28)),f9(f2(a1),f4(a28)))), % 118.83/118.74 inference(scs_inference,[],[4012,3799,3947,3750,44,79,70,94,71,74,95,85,88,83,84,81])). % 118.83/118.74 cnf(4072,plain, % 118.83/118.74 (P2(f11(f9(f2(a1),f4(a28))))), % 118.83/118.74 inference(scs_inference,[],[3954,4012,3799,3947,3750,44,79,70,94,71,74,95,85,88,83,84,81,76,80,77,9,73])). % 118.83/118.74 cnf(4091,plain, % 118.83/118.74 (P1(f6(f15(f4(f2(a1)))))), % 118.83/118.74 inference(scs_inference,[],[3949,3954,4012,3799,3947,3750,3919,44,79,70,94,71,74,95,85,88,83,84,81,76,80,77,9,73,87,7,10,13,15,4,14,18,8,6,12,11,5,16,17,2,75])). % 118.83/118.74 cnf(4107,plain, % 118.83/118.74 (~E(a3,f15(f6(f15(f4(a13)))))), % 118.83/118.74 inference(scs_inference,[],[3949,3954,4012,3799,3947,3900,3750,3919,3911,45,44,79,70,94,71,74,95,85,88,83,84,81,76,80,77,9,73,87,7,10,13,15,4,14,18,8,6,12,11,5,16,17,2,75,105,91,78,100,92,104,93,3])). % 118.83/118.74 cnf(4108,plain, % 118.83/118.74 (P2(f5(a27,a13))), % 118.83/118.74 inference(scs_inference,[],[3949,3954,4012,3799,3947,3900,3750,3919,3911,3936,45,44,79,70,94,71,74,95,85,88,83,84,81,76,80,77,9,73,87,7,10,13,15,4,14,18,8,6,12,11,5,16,17,2,75,105,91,78,100,92,104,93,3,102])). % 118.83/118.74 cnf(4114,plain, % 118.83/118.74 (E(f10(f8(a20,a20),f8(a20,a20)),f8(a20,f10(a20,a20)))), % 118.83/118.74 inference(scs_inference,[],[3949,3954,4012,3799,3947,3900,3750,3919,3911,3936,45,35,44,79,70,94,71,74,95,85,88,83,84,81,76,80,77,9,73,87,7,10,13,15,4,14,18,8,6,12,11,5,16,17,2,75,105,91,78,100,92,104,93,3,102,110,111,113])). % 118.83/118.74 cnf(4116,plain, % 118.83/118.74 (E(f10(f8(a20,a20),f8(a20,a20)),f8(f10(a20,a20),a20))), % 118.83/118.74 inference(scs_inference,[],[3949,3954,4012,3799,3947,3900,3750,3919,3911,3936,45,35,44,79,70,94,71,74,95,85,88,83,84,81,76,80,77,9,73,87,7,10,13,15,4,14,18,8,6,12,11,5,16,17,2,75,105,91,78,100,92,104,93,3,102,110,111,113,114])). % 118.83/118.74 cnf(4118,plain, % 118.83/118.74 (P4(a12,f8(f8(f5(a28,a28),f5(a28,a28)),f5(a28,a28)))), % 118.83/118.74 inference(scs_inference,[],[3962,3949,3954,4012,4008,3799,3947,3900,3950,3750,3919,3911,3936,45,3917,35,44,79,70,94,71,74,95,85,88,83,84,81,76,80,77,9,73,87,7,10,13,15,4,14,18,8,6,12,11,5,16,17,2,75,105,91,78,100,92,104,93,3,102,110,111,113,114,109])). % 118.83/118.74 cnf(4120,plain, % 118.83/118.74 (P4(a12,f10(f8(f5(a28,a28),f5(a28,a28)),f8(f5(a28,a28),f5(a28,a28))))), % 118.83/118.74 inference(scs_inference,[],[3962,3949,3954,4012,4008,3799,3947,3900,3950,3750,3919,3911,3936,45,3917,35,44,79,70,94,71,74,95,85,88,83,84,81,76,80,77,9,73,87,7,10,13,15,4,14,18,8,6,12,11,5,16,17,2,75,105,91,78,100,92,104,93,3,102,110,111,113,114,109,108])). % 118.83/118.74 cnf(4127,plain, % 118.83/118.74 (E(f15(f6(f15(f4(f2(a1))))),f4(a1))), % 118.83/118.74 inference(scs_inference,[],[3970,3962,3949,3954,4012,4008,3799,3947,3900,3950,3750,3919,3911,3936,45,3917,35,44,79,70,94,71,74,95,85,88,83,84,81,76,80,77,9,73,87,7,10,13,15,4,14,18,8,6,12,11,5,16,17,2,75,105,91,78,100,92,104,93,3,102,110,111,113,114,109,108,120,115,780,311])). % 118.83/118.74 cnf(4141,plain, % 118.83/118.74 (P2(f9(a13,f4(a28)))), % 118.83/118.74 inference(scs_inference,[],[4040,1377])). % 118.83/118.74 cnf(4143,plain, % 118.83/118.74 (~E(f15(f15(f15(f4(a28)))),a3)), % 118.83/118.74 inference(scs_inference,[],[3796,70])). % 118.83/118.74 cnf(4149,plain, % 118.83/118.74 (E(f10(f5(a27,a13),a12),f5(a27,a13))), % 118.83/118.74 inference(scs_inference,[],[4108,3796,70,74,84,79])). % 118.83/118.74 cnf(4151,plain, % 118.83/118.74 (E(f10(a12,f5(a27,a13)),f5(a27,a13))), % 118.83/118.74 inference(scs_inference,[],[4108,3796,70,74,84,79,80])). % 118.83/118.74 cnf(4153,plain, % 118.83/118.74 (E(f8(a12,f5(a27,a13)),a12)), % 118.83/118.74 inference(scs_inference,[],[4108,3796,70,74,84,79,80,77])). % 118.83/118.74 cnf(4157,plain, % 118.83/118.74 (P4(a12,f5(a1,a1))), % 118.83/118.74 inference(scs_inference,[],[4108,3796,42,70,74,84,79,80,77,85,95])). % 118.83/118.74 cnf(4161,plain, % 118.83/118.74 (P1(f15(f15(f15(f4(a28)))))), % 118.83/118.74 inference(scs_inference,[],[4108,3796,42,70,74,84,79,80,77,85,95,76,71])). % 118.83/118.74 cnf(4165,plain, % 118.83/118.74 (P4(f5(a27,a13),f5(a27,a13))), % 118.83/118.74 inference(scs_inference,[],[4108,3796,42,70,74,84,79,80,77,85,95,76,71,88,81])). % 118.83/118.74 cnf(4167,plain, % 118.83/118.74 (P4(a12,f8(f5(a27,a13),f5(a27,a13)))), % 118.83/118.74 inference(scs_inference,[],[4108,3796,42,70,74,84,79,80,77,85,95,76,71,88,81,94])). % 118.83/118.74 cnf(4171,plain, % 118.83/118.74 (P2(f11(f5(a27,a13)))), % 118.83/118.74 inference(scs_inference,[],[4108,3796,42,70,74,84,79,80,77,85,95,76,71,88,81,94,83,73])). % 118.83/118.74 cnf(4190,plain, % 118.83/118.74 (~E(a3,f15(f4(f2(a28))))), % 118.83/118.74 inference(scs_inference,[],[4108,3958,3796,3952,42,70,74,84,79,80,77,85,95,76,71,88,81,94,83,73,87,9,13,4,7,18,10,8,14,15,12,6,16,11,5,17,2])). % 118.83/118.74 cnf(4191,plain, % 118.83/118.74 (P2(f10(f5(a27,a13),f5(a27,a13)))), % 118.83/118.74 inference(scs_inference,[],[4108,3958,3796,3952,42,70,74,84,79,80,77,85,95,76,71,88,81,94,83,73,87,9,13,4,7,18,10,8,14,15,12,6,16,11,5,17,2,91])). % 118.83/118.74 cnf(4195,plain, % 118.83/118.74 (P1(f6(f15(f6(f4(a1)))))), % 118.83/118.74 inference(scs_inference,[],[4108,3958,3796,3890,3952,3859,42,70,74,84,79,80,77,85,95,76,71,88,81,94,83,73,87,9,13,4,7,18,10,8,14,15,12,6,16,11,5,17,2,91,105,75])). % 118.83/118.74 cnf(4197,plain, % 118.83/118.74 (E(f15(f6(f15(f6(f4(a1))))),f15(f6(f4(a1))))), % 118.83/118.74 inference(scs_inference,[],[4108,3958,3796,3890,3952,3859,42,70,74,84,79,80,77,85,95,76,71,88,81,94,83,73,87,9,13,4,7,18,10,8,14,15,12,6,16,11,5,17,2,91,105,75,78])). % 118.83/118.74 cnf(4201,plain, % 118.83/118.74 (P2(f8(f5(a27,a13),f5(a27,a13)))), % 118.83/118.74 inference(scs_inference,[],[4108,3958,3796,3890,3952,3859,42,70,74,84,79,80,77,85,95,76,71,88,81,94,83,73,87,9,13,4,7,18,10,8,14,15,12,6,16,11,5,17,2,91,105,75,78,104,92])). % 118.83/118.74 cnf(4205,plain, % 118.83/118.74 (P2(f9(f2(a28),f4(a28)))), % 118.83/118.74 inference(scs_inference,[],[4108,3847,3958,3796,3890,3952,3859,170,42,70,74,84,79,80,77,85,95,76,71,88,81,94,83,73,87,9,13,4,7,18,10,8,14,15,12,6,16,11,5,17,2,91,105,75,78,104,92,100,93])). % 118.83/118.74 cnf(4207,plain, % 118.83/118.74 (E(f8(f5(a28,a28),a12),f11(a12))), % 118.83/118.74 inference(scs_inference,[],[4108,3847,3958,3984,3796,3890,3952,3859,170,225,42,70,74,84,79,80,77,85,95,76,71,88,81,94,83,73,87,9,13,4,7,18,10,8,14,15,12,6,16,11,5,17,2,91,105,75,78,104,92,100,93,3])). % 118.83/118.74 cnf(4210,plain, % 118.83/118.74 (P2(f5(f2(a1),a13))), % 118.83/118.74 inference(scs_inference,[],[4108,3847,3958,3984,4063,4118,3796,3890,3952,4021,3859,1341,3949,170,131,225,44,42,70,74,84,79,80,77,85,95,76,71,88,81,94,83,73,87,9,13,4,7,18,10,8,14,15,12,6,16,11,5,17,2,91,105,75,78,104,92,100,93,3,22,21,102])). % 118.83/118.74 cnf(4240,plain, % 118.83/118.74 (E(f11(f11(f9(a13,f4(a28)))),f9(a13,f4(a28)))), % 118.83/118.74 inference(scs_inference,[],[4141,74])). % 118.83/118.74 cnf(4244,plain, % 118.83/118.74 (P1(f15(f6(f15(f4(a28)))))), % 118.83/118.74 inference(scs_inference,[],[4141,3804,74,80,71])). % 118.83/118.74 cnf(4246,plain, % 118.83/118.74 (~E(f15(f6(f15(f4(a28)))),a3)), % 118.83/118.74 inference(scs_inference,[],[4141,3804,74,80,71,70])). % 118.83/118.74 cnf(4266,plain, % 118.83/118.74 (P2(f11(f9(a13,f4(a28))))), % 118.83/118.74 inference(scs_inference,[],[4141,3804,74,80,71,70,94,85,83,77,81,79,88,84,76,73])). % 118.83/118.74 cnf(4285,plain, % 118.83/118.74 (~E(a3,f15(f15(f4(a27))))), % 118.83/118.74 inference(scs_inference,[],[4149,4141,3804,4045,74,80,71,70,94,85,83,77,81,79,88,84,76,73,87,7,13,10,9,14,4,8,15,18,6,12,5,16,11,17,2])). % 118.83/118.74 cnf(4286,plain, % 118.83/118.74 (P1(f6(f15(f15(f4(a27)))))), % 118.83/118.74 inference(scs_inference,[],[4149,4141,3804,3968,4045,74,80,71,70,94,85,83,77,81,79,88,84,76,73,87,7,13,10,9,14,4,8,15,18,6,12,5,16,11,17,2,75])). % 118.83/118.74 cnf(4292,plain, % 118.83/118.74 (E(f15(f6(f15(f15(f4(a27))))),f15(f15(f4(a27))))), % 118.83/118.74 inference(scs_inference,[],[4149,4141,3804,3968,4045,74,80,71,70,94,85,83,77,81,79,88,84,76,73,87,7,13,10,9,14,4,8,15,18,6,12,5,16,11,17,2,75,105,91,78])). % 118.83/118.74 cnf(4302,plain, % 118.83/118.74 (~E(a3,f15(f6(f15(f6(f4(a1))))))), % 118.83/118.74 inference(scs_inference,[],[4149,4141,3804,3968,3997,4045,4197,45,74,80,71,70,94,85,83,77,81,79,88,84,76,73,87,7,13,10,9,14,4,8,15,18,6,12,5,16,11,17,2,75,105,91,78,100,92,104,93,3])). % 118.83/118.74 cnf(4320,plain, % 118.83/118.74 (~P4(x43201,f8(f10(a23,a26),f10(a23,a26)))+~E(x43201,f8(f10(a24,a24),f10(a24,a24)))), % 118.83/118.74 inference(scs_inference,[],[68,4165,4157,4149,4141,4201,4167,3836,3804,3968,3997,4045,3868,4197,45,4108,633,349,74,80,71,70,94,85,83,77,81,79,88,84,76,73,87,7,13,10,9,14,4,8,15,18,6,12,5,16,11,17,2,75,105,91,78,100,92,104,93,3,25,111,110,114,113,109,108,120,115,21])). % 118.83/118.74 cnf(4345,plain, % 118.83/118.74 (~E(f15(f6(f15(f4(a13)))),a3)), % 118.83/118.74 inference(scs_inference,[],[4040,3903,80,94,79,74,83,76,85,84,77,88,70])). % 118.83/118.74 cnf(4347,plain, % 118.83/118.74 (P1(f15(f6(f15(f4(a13)))))), % 118.83/118.74 inference(scs_inference,[],[4040,3903,80,94,79,74,83,76,85,84,77,88,70,71])). % 118.83/118.74 cnf(4351,plain, % 118.83/118.74 (P2(f11(f9(a1,f4(a28))))), % 118.83/118.74 inference(scs_inference,[],[4040,3903,80,94,79,74,83,76,85,84,77,88,70,71,81,73])). % 118.83/118.74 cnf(4370,plain, % 118.83/118.74 (~E(a3,f15(f15(f15(f4(a28)))))), % 118.83/118.74 inference(scs_inference,[],[4151,4040,3903,4143,80,94,79,74,83,76,85,84,77,88,70,71,81,73,87,14,8,10,18,9,7,15,13,6,4,5,17,12,16,11,2])). % 118.83/118.74 cnf(4371,plain, % 118.83/118.74 (P1(f6(f15(f15(f15(f4(a28))))))), % 118.83/118.74 inference(scs_inference,[],[4151,4040,3903,4161,4143,80,94,79,74,83,76,85,84,77,88,70,71,81,73,87,14,8,10,18,9,7,15,13,6,4,5,17,12,16,11,2,75])). % 118.83/118.74 cnf(4377,plain, % 118.83/118.74 (E(f15(f6(f15(f4(f2(a28))))),f15(f4(f2(a28))))), % 118.83/118.74 inference(scs_inference,[],[4151,4040,3903,4161,4143,3952,301,80,94,79,74,83,76,85,84,77,88,70,71,81,73,87,14,8,10,18,9,7,15,13,6,4,5,17,12,16,11,2,75,91,105,78])). % 118.83/118.74 cnf(4385,plain, % 118.83/118.74 (E(f8(a12,f5(a27,a13)),f11(a12))), % 118.83/118.74 inference(scs_inference,[],[4151,4040,4153,3903,4161,4143,3952,301,225,80,94,79,74,83,76,85,84,77,88,70,71,81,73,87,14,8,10,18,9,7,15,13,6,4,5,17,12,16,11,2,75,91,105,78,100,104,92,3])). % 118.83/118.74 cnf(4425,plain, % 118.83/118.74 (P1(f15(f6(f15(f4(a27)))))), % 118.83/118.74 inference(scs_inference,[],[4171,4000,80,94,79,88,76,81,84,83,77,74,71])). % 118.83/118.74 cnf(4427,plain, % 118.83/118.74 (~E(f15(f6(f15(f4(a27)))),a3)), % 118.83/118.74 inference(scs_inference,[],[4171,4000,80,94,79,88,76,81,84,83,77,74,71,70])). % 118.83/118.74 cnf(4431,plain, % 118.83/118.74 (P2(f11(f11(f5(a27,a13))))), % 118.83/118.74 inference(scs_inference,[],[4171,4000,80,94,79,88,76,81,84,83,77,74,71,70,85,73])). % 118.83/118.74 cnf(4450,plain, % 118.83/118.74 (~E(a3,f15(f6(f15(f4(a28)))))), % 118.83/118.74 inference(scs_inference,[],[4385,4171,4000,4246,80,94,79,88,76,81,84,83,77,74,71,70,85,73,87,10,14,18,13,7,15,8,6,4,9,5,16,17,12,11,2])). % 118.83/118.74 cnf(4455,plain, % 118.83/118.74 (P1(f6(f15(f6(f15(f4(a13))))))), % 118.83/118.74 inference(scs_inference,[],[4385,4171,4000,4347,4345,4246,80,94,79,88,76,81,84,83,77,74,71,70,85,73,87,10,14,18,13,7,15,8,6,4,9,5,16,17,12,11,2,91,105,75])). % 118.83/118.74 cnf(4505,plain, % 118.83/118.74 (~E(f15(f15(f15(f4(f2(a1))))),a3)), % 118.83/118.74 inference(scs_inference,[],[4017,4049,3821,80,94,74,79,81,83,76,85,77,88,70])). % 118.83/118.74 cnf(4507,plain, % 118.83/118.74 (P1(f15(f15(f15(f4(f2(a1))))))), % 118.83/118.74 inference(scs_inference,[],[4017,4049,3821,80,94,74,79,81,83,76,85,77,88,70,71])). % 118.83/118.74 cnf(4511,plain, % 118.83/118.74 (P2(f11(f9(a27,f4(a13))))), % 118.83/118.74 inference(scs_inference,[],[4017,4049,3821,80,94,74,79,81,83,76,85,77,88,70,71,84,73])). % 118.83/118.74 cnf(4533,plain, % 118.83/118.74 (P1(f6(f15(f6(f15(f4(a28))))))), % 118.83/118.74 inference(scs_inference,[],[4207,4017,4049,4244,4427,3821,4246,80,94,74,79,81,83,76,85,77,88,70,71,84,73,87,18,13,10,15,6,8,14,4,7,9,5,12,17,16,11,2,105,75])). % 118.83/118.74 cnf(4545,plain, % 118.83/118.74 (E(f8(f5(a1,a28),a12),f11(a12))), % 118.83/118.74 inference(scs_inference,[],[4207,4017,3777,4049,4244,4427,3821,4246,45,225,80,94,74,79,81,83,76,85,77,88,70,71,84,73,87,18,13,10,15,6,8,14,4,7,9,5,12,17,16,11,2,105,75,91,93,104,100,92,3])). % 118.83/118.74 cnf(4579,plain, % 118.83/118.74 (P5(f6(f15(f4(f2(a1)))),f15(f6(f15(f4(f2(a1))))))), % 118.83/118.74 inference(scs_inference,[],[3787,4091,3947,80,88,74,83,94,81,85])). % 118.83/118.74 cnf(4587,plain, % 118.83/118.74 (P1(f15(f6(f15(f4(f2(a1))))))), % 118.83/118.74 inference(scs_inference,[],[3787,4091,3947,80,88,74,83,94,81,85,84,77,79,71])). % 118.83/118.74 cnf(4591,plain, % 118.83/118.74 (~E(f15(f6(f15(f4(f2(a1))))),a3)), % 118.83/118.74 inference(scs_inference,[],[3787,4091,3947,80,88,74,83,94,81,85,84,77,79,71,76,70])). % 118.83/118.74 cnf(4612,plain, % 118.83/118.74 (~E(f15(f6(f15(f6(f4(a1))))),a3)), % 118.83/118.74 inference(scs_inference,[],[4014,3787,4091,4302,3947,3890,80,88,74,83,94,81,85,84,77,79,71,76,70,73,87,10,18,15,8,14,13,4,7,6,9,5,16,12,17,11,2])). % 118.83/118.74 cnf(4627,plain, % 118.83/118.74 (~E(a3,f15(f6(f15(f4(f2(a28))))))), % 118.83/118.74 inference(scs_inference,[],[4014,3787,4190,4091,4507,4302,4505,4377,3947,3890,45,80,88,74,83,94,81,85,84,77,79,71,76,70,73,87,10,18,15,8,14,13,4,7,6,9,5,16,12,17,11,2,75,91,105,93,92,104,100,3])). % 118.83/118.74 cnf(4640,plain, % 118.83/118.74 (~E(f15(f15(f6(f15(f4(a27))))),f15(a3))), % 118.83/118.74 inference(scs_inference,[],[4014,3787,4190,4091,4425,4507,4302,4505,4377,4063,4427,3947,3890,1356,28,45,215,80,88,74,83,94,81,85,84,77,79,71,76,70,73,87,10,18,15,8,14,13,4,7,6,9,5,16,12,17,11,2,75,91,105,93,92,104,100,3,111,113,114,110,120,24,21,86])). % 118.83/118.74 cnf(4668,plain, % 118.83/118.74 (P1(f15(f6(f15(f6(f4(a1))))))), % 118.83/118.74 inference(scs_inference,[],[3812,4195,4286,3749,80,79,74,81,88,84,94,77,70,83,76,85,71])). % 118.83/118.74 cnf(4670,plain, % 118.83/118.74 (P2(f11(f10(f5(a1,a28),f5(a1,a28))))), % 118.83/118.74 inference(scs_inference,[],[3812,4195,4286,3749,80,79,74,81,88,84,94,77,70,83,76,85,71,73])). % 118.83/118.74 cnf(4715,plain, % 118.83/118.74 (~E(f15(a3),f15(f15(f15(f4(a27)))))), % 118.83/118.74 inference(scs_inference,[],[4545,3812,3979,3994,4285,4195,4286,4640,4587,4591,3749,3968,28,45,279,80,79,74,81,88,84,94,77,70,83,76,85,71,73,87,15,10,8,13,18,4,7,14,6,9,5,17,16,12,11,2,91,105,75,93,100,92,104,3,111,113,110,114,86])). % 118.83/118.74 cnf(4738,plain, % 118.83/118.74 (~E(f15(f6(f15(f15(f15(f4(a28)))))),a3)), % 118.83/118.74 inference(scs_inference,[],[3977,4371,3692,83,80,84,74,79,77,88,71,70])). % 118.83/118.74 cnf(4767,plain, % 118.83/118.74 (~E(f15(f15(f15(f4(a27)))),f15(a3))), % 118.83/118.74 inference(scs_inference,[],[3977,4116,4715,4371,4161,3692,83,80,84,74,79,77,88,71,70,81,85,94,76,73,87,15,8,13,4,10,7,14,18,6,9,5,12,17,16,11,2])). % 118.83/118.74 cnf(4783,plain, % 118.83/118.74 (P2(f5(f2(a28),f2(a1)))), % 118.83/118.74 inference(scs_inference,[],[3977,4116,4715,4371,4668,4612,4292,4285,4161,3692,45,142,170,131,83,80,84,74,79,77,88,71,70,81,85,94,76,73,87,15,8,13,4,10,7,14,18,6,9,5,12,17,16,11,2,105,75,91,93,104,100,92,3,102])). % 118.83/118.74 cnf(4805,plain, % 118.83/118.74 (~E(f15(f6(f15(f6(f15(f4(a13)))))),a3)), % 118.83/118.74 inference(scs_inference,[],[4783,4455,74,70])). % 118.83/118.74 cnf(4829,plain, % 118.83/118.74 (P2(f11(f5(f2(a28),f2(a1))))), % 118.83/118.74 inference(scs_inference,[],[4783,4455,4286,3750,74,70,80,88,79,83,77,84,71,81,76,85,94,73])). % 118.83/118.74 cnf(4846,plain, % 118.83/118.74 (~E(f15(f6(f15(f4(f2(a28))))),a3)), % 118.83/118.74 inference(scs_inference,[],[4783,4114,4455,4627,4286,3750,74,70,80,88,79,83,77,84,71,81,76,85,94,73,13,8,10,15,4,14,7,18,9,6,5,12,16,17,11,2])). % 118.83/118.74 cnf(4851,plain, % 118.83/118.74 (P1(f6(f15(f6(f15(f4(a27))))))), % 118.83/118.74 inference(scs_inference,[],[4783,4114,4455,4627,4286,4425,4427,3750,74,70,80,88,79,83,77,84,71,81,76,85,94,73,13,8,10,15,4,14,7,18,9,6,5,12,16,17,11,2,91,105,75])). % 118.83/118.74 cnf(4866,plain, % 118.83/118.74 (P2(f5(f2(a1),f2(a28)))), % 118.83/118.74 inference(scs_inference,[],[4783,4114,3980,3983,3680,4015,4455,4627,4286,4425,4427,3750,45,416,170,131,74,70,80,88,79,83,77,84,71,81,76,85,94,73,13,8,10,15,4,14,7,18,9,6,5,12,16,17,11,2,91,105,75,93,104,92,100,3,22,102])). % 118.83/118.74 cnf(4896,plain, % 118.83/118.74 (~E(f15(f6(f15(f6(f15(f4(a28)))))),a3)), % 118.83/118.74 inference(scs_inference,[],[4533,3890,88,70])). % 118.83/118.74 cnf(4920,plain, % 118.83/118.74 (P2(f11(f9(f2(a28),f4(a28))))), % 118.83/118.74 inference(scs_inference,[],[4205,4533,4244,3890,88,70,74,79,77,71,80,83,84,81,94,76,85,73])). % 118.83/118.74 cnf(4942,plain, % 118.83/118.74 (P1(f6(f15(f4(f2(a28)))))), % 118.83/118.74 inference(scs_inference,[],[4205,3775,4533,4738,4244,3952,3890,301,88,70,74,79,77,71,80,83,84,81,94,76,85,73,15,13,10,8,4,14,7,18,9,5,6,16,12,17,11,2,91,105,75])). % 118.83/118.74 cnf(4952,plain, % 118.83/118.74 (~E(f4(a28),a3)), % 118.83/118.74 inference(scs_inference,[],[4205,3775,4033,4533,4738,4244,3952,4427,3890,301,45,88,70,74,79,77,71,80,83,84,81,94,76,85,73,15,13,10,8,4,14,7,18,9,5,6,16,12,17,11,2,91,105,75,93,104,92,100,3])). % 118.83/118.74 cnf(4957,plain, % 118.83/118.74 (E(f10(f8(a24,a24),f8(a24,a24)),f8(f10(a24,a24),a24))), % 118.83/118.74 inference(scs_inference,[],[4205,3775,4033,4533,4738,4244,3952,4427,3890,301,45,39,88,70,74,79,77,71,80,83,84,81,94,76,85,73,15,13,10,8,4,14,7,18,9,5,6,16,12,17,11,2,91,105,75,93,104,92,100,3,111,113,114])). % 118.83/118.74 cnf(4966,plain, % 118.83/118.74 (~P4(f10(f10(f8(a24,a24),f8(a24,a24)),f10(f8(a24,a24),f8(a24,a24))),f8(f10(a23,a26),f10(a23,a26)))), % 118.83/118.74 inference(scs_inference,[],[4205,3775,4033,4533,4738,4244,3952,4427,3890,130,301,45,39,43,42,88,70,74,79,77,71,80,83,84,81,94,76,85,73,15,13,10,8,4,14,7,18,9,5,6,16,12,17,11,2,91,105,75,93,104,92,100,3,111,113,114,110,118,120,525,4320])). % 118.83/118.74 cnf(4968,plain, % 118.83/118.74 (~E(f10(f10(f8(a23,a23),f8(a23,a26)),f10(f8(a26,a23),f8(a26,a26))),f8(f10(a23,a26),f10(a23,a26)))), % 118.83/118.74 inference(scs_inference,[],[4205,3775,4033,4533,4738,4244,3952,4427,3890,130,301,45,39,43,42,88,70,74,79,77,71,80,83,84,81,94,76,85,73,15,13,10,8,4,14,7,18,9,5,6,16,12,17,11,2,91,105,75,93,104,92,100,3,111,113,114,110,118,120,525,4320,512,566])). % 118.83/118.74 cnf(4969,plain, % 118.83/118.74 (E(f15(f6(f4(a28))),f4(a28))), % 118.83/118.74 inference(scs_inference,[],[4205,3775,4033,4533,4738,4244,3748,3952,4427,3890,130,301,45,39,43,42,88,70,74,79,77,71,80,83,84,81,94,76,85,73,15,13,10,8,4,14,7,18,9,5,6,16,12,17,11,2,91,105,75,93,104,92,100,3,111,113,114,110,118,120,525,4320,512,566,78])). % 118.83/118.74 cnf(4998,plain, % 118.83/118.74 (~E(a3,f4(a28))), % 118.83/118.74 inference(scs_inference,[],[4952,4866,3981,4957,4942,85,94,76,7,18,6,9,525,2])). % 118.83/118.74 cnf(5003,plain, % 118.83/118.74 (~E(f15(f6(f15(f6(f15(f4(a27)))))),a3)), % 118.83/118.74 inference(scs_inference,[],[4952,4866,3981,4957,4942,4851,85,94,76,7,18,6,9,525,2,5,73,12,70])). % 118.83/118.74 cnf(5020,plain, % 118.83/118.74 (P1(f15(f6(f15(f4(f2(a28))))))), % 118.83/118.74 inference(scs_inference,[],[4952,4866,3981,4957,4942,4851,3968,85,94,76,7,18,6,9,525,2,5,73,12,70,79,88,80,16,77,74,8,15,84,71])). % 118.83/118.74 cnf(5030,plain, % 118.83/118.74 (P4(f5(f2(a1),f2(a28)),f5(f2(a1),f2(a28)))), % 118.83/118.74 inference(scs_inference,[],[4952,4866,3981,4957,4942,4851,3968,85,94,76,7,18,6,9,525,2,5,73,12,70,79,88,80,16,77,74,8,15,84,71,13,83,10,14,4,11,17,81])). % 118.83/118.74 cnf(5043,plain, % 118.83/118.74 (P1(f6(f4(a28)))), % 118.83/118.74 inference(scs_inference,[],[4952,4866,3981,3989,3995,4957,4942,4851,3847,3968,85,94,76,7,18,6,9,525,2,5,73,12,70,79,88,80,16,77,74,8,15,84,71,13,83,10,14,4,11,17,81,104,100,3,91,105,75])). % 118.83/118.74 cnf(5070,plain, % 118.83/118.74 (P4(a12,f8(f5(f2(a1),a13),f5(f2(a1),a13)))), % 118.83/118.74 inference(scs_inference,[],[4210,94])). % 118.83/118.74 cnf(5077,plain, % 118.83/118.74 (E(f7(x50771,f2(a1)),f7(x50771,a13))), % 118.83/118.74 inference(scs_inference,[],[26,5043,4210,3960,94,85,7,76,18])). % 118.83/118.74 cnf(5078,plain, % 118.83/118.74 (E(f15(f2(a1)),f15(a13))), % 118.83/118.74 inference(scs_inference,[],[26,5043,4210,3960,94,85,7,76,18,9])). % 118.83/118.74 cnf(5080,plain, % 118.83/118.74 (E(f8(x50801,f2(a1)),f8(x50801,a13))), % 118.83/118.74 inference(scs_inference,[],[26,5043,4210,3960,4968,94,85,7,76,18,9,2,6])). % 118.83/118.74 cnf(5083,plain, % 118.83/118.74 (E(f8(f2(a1),x50831),f8(a13,x50831))), % 118.83/118.74 inference(scs_inference,[],[26,5043,4210,3960,4968,94,85,7,76,18,9,2,6,77,5])). % 118.83/118.74 cnf(5088,plain, % 118.83/118.74 (~E(f15(f6(f4(a28))),a3)), % 118.83/118.74 inference(scs_inference,[],[26,5043,4210,3960,4968,94,85,7,76,18,9,2,6,77,5,88,73,70])). % 118.83/118.74 cnf(5096,plain, % 118.83/118.74 (E(f11(f2(a1)),f11(a13))), % 118.83/118.74 inference(scs_inference,[],[26,5043,4210,3960,4968,94,85,7,76,18,9,2,6,77,5,88,73,70,79,80,74,8])). % 118.83/118.74 cnf(5099,plain, % 118.83/118.74 (E(f6(f2(a1)),f6(a13))), % 118.83/118.74 inference(scs_inference,[],[26,5043,4210,3960,4968,94,85,7,76,18,9,2,6,77,5,88,73,70,79,80,74,8,84,16])). % 118.83/118.74 cnf(5103,plain, % 118.83/118.74 (P1(f15(f6(f4(a28))))), % 118.83/118.74 inference(scs_inference,[],[26,5043,4210,3960,4968,94,85,7,76,18,9,2,6,77,5,88,73,70,79,80,74,8,84,16,83,12,71])). % 118.83/118.74 cnf(5105,plain, % 118.83/118.74 (E(f5(f2(a1),x51051),f5(a13,x51051))), % 118.83/118.74 inference(scs_inference,[],[26,5043,4210,3960,4968,94,85,7,76,18,9,2,6,77,5,88,73,70,79,80,74,8,84,16,83,12,71,14])). % 118.83/118.74 cnf(5106,plain, % 118.83/118.74 (E(f5(x51061,f2(a1)),f5(x51061,a13))), % 118.83/118.74 inference(scs_inference,[],[26,5043,4210,3960,4968,94,85,7,76,18,9,2,6,77,5,88,73,70,79,80,74,8,84,16,83,12,71,14,15])). % 118.83/118.74 cnf(5107,plain, % 118.83/118.74 (E(f10(x51071,f2(a1)),f10(x51071,a13))), % 118.83/118.74 inference(scs_inference,[],[26,5043,4210,3960,4968,94,85,7,76,18,9,2,6,77,5,88,73,70,79,80,74,8,84,16,83,12,71,14,15,11])). % 118.83/118.74 cnf(5108,plain, % 118.83/118.74 (E(f9(x51081,f2(a1)),f9(x51081,a13))), % 118.83/118.74 inference(scs_inference,[],[26,5043,4210,3960,4968,94,85,7,76,18,9,2,6,77,5,88,73,70,79,80,74,8,84,16,83,12,71,14,15,11,13])). % 118.83/118.74 cnf(5109,plain, % 118.83/118.74 (E(f10(f2(a1),x51091),f10(a13,x51091))), % 118.83/118.74 inference(scs_inference,[],[26,5043,4210,3960,4968,94,85,7,76,18,9,2,6,77,5,88,73,70,79,80,74,8,84,16,83,12,71,14,15,11,13,10])). % 118.83/118.74 cnf(5111,plain, % 118.83/118.74 (P4(f5(f2(a1),a13),f5(f2(a1),a13))), % 118.83/118.74 inference(scs_inference,[],[26,5043,4210,3960,4968,94,85,7,76,18,9,2,6,77,5,88,73,70,79,80,74,8,84,16,83,12,71,14,15,11,13,10,4,81])). % 118.83/118.74 cnf(5113,plain, % 118.83/118.74 (E(f7(f2(a1),x51131),f7(a13,x51131))), % 118.83/118.74 inference(scs_inference,[],[26,5043,4210,3960,4968,94,85,7,76,18,9,2,6,77,5,88,73,70,79,80,74,8,84,16,83,12,71,14,15,11,13,10,4,81,17])). % 118.83/118.74 cnf(5116,plain, % 118.83/118.74 (E(f15(f6(f15(f6(f4(a28))))),f15(f6(f4(a28))))), % 118.83/118.74 inference(scs_inference,[],[26,5043,4210,3960,4968,94,85,7,76,18,9,2,6,77,5,88,73,70,79,80,74,8,84,16,83,12,71,14,15,11,13,10,4,81,17,104,78])). % 118.83/118.74 cnf(5120,plain, % 118.83/118.74 (~E(a3,f15(f6(f4(a28))))), % 118.83/118.74 inference(scs_inference,[],[26,4998,5043,4210,3960,4969,4968,94,85,7,76,18,9,2,6,77,5,88,73,70,79,80,74,8,84,16,83,12,71,14,15,11,13,10,4,81,17,104,78,100,3])). % 118.83/118.74 cnf(5126,plain, % 118.83/118.74 (P2(f9(a27,f6(f4(a28))))), % 118.83/118.74 inference(scs_inference,[],[26,4998,5043,4210,3960,4969,4968,45,94,85,7,76,18,9,2,6,77,5,88,73,70,79,80,74,8,84,16,83,12,71,14,15,11,13,10,4,81,17,104,78,100,3,25,105,91,93])). % 118.83/118.74 cnf(5130,plain, % 118.83/118.74 (P2(f8(f5(f2(a1),a13),f5(f2(a1),a13)))), % 118.83/118.74 inference(scs_inference,[],[26,4998,5043,4210,3960,4969,4968,5020,4846,45,94,85,7,76,18,9,2,6,77,5,88,73,70,79,80,74,8,84,16,83,12,71,14,15,11,13,10,4,81,17,104,78,100,3,25,105,91,93,75,92])). % 118.83/118.74 cnf(5146,plain, % 118.83/118.74 (E(f5(f2(a1),a13),a17)), % 118.83/118.74 inference(scs_inference,[],[26,4998,5043,4210,3960,4969,4968,5020,4846,3962,3970,4952,3917,45,254,43,94,85,7,76,18,9,2,6,77,5,88,73,70,79,80,74,8,84,16,83,12,71,14,15,11,13,10,4,81,17,104,78,100,3,25,105,91,93,75,92,125,110,111,114,113,120,116,260])). % 118.83/118.74 cnf(5150,plain, % 118.83/118.74 (E(f9(a27,f6(f4(a28))),f9(a28,f6(f4(a28))))), % 118.83/118.74 inference(scs_inference,[],[26,4998,5043,4210,3960,4969,4968,5020,4846,4966,3962,3970,4952,169,3917,45,254,43,94,85,7,76,18,9,2,6,77,5,88,73,70,79,80,74,8,84,16,83,12,71,14,15,11,13,10,4,81,17,104,78,100,3,25,105,91,93,75,92,125,110,111,114,113,120,116,260,87,21,101])). % 118.83/118.74 cnf(5176,plain, % 118.83/118.74 (~E(f15(f15(f6(f4(a28)))),a3)), % 118.83/118.74 inference(scs_inference,[],[5077,5106,4072,5103,4805,260,94,85,7,76,18,9,2,6,77,5,88,73,70])). % 118.83/118.74 cnf(5191,plain, % 118.83/118.74 (P1(f15(f15(f6(f4(a28)))))), % 118.83/118.74 inference(scs_inference,[],[5077,5106,4072,5103,4805,260,94,85,7,76,18,9,2,6,77,5,88,73,70,79,80,74,84,8,83,16,12,71])). % 118.83/118.74 cnf(5206,plain, % 118.83/118.74 (E(f7(f2(a1),f2(a1)),f7(a13,a13))), % 118.83/118.74 inference(scs_inference,[],[5077,5106,5113,4072,5103,4805,4191,260,94,85,7,76,18,9,2,6,77,5,88,73,70,79,80,74,84,8,83,16,12,71,14,15,11,13,10,81,4,17,104,100,3])). % 118.83/118.74 cnf(5215,plain, % 118.83/118.74 (P1(f6(f15(f6(f4(a28)))))), % 118.83/118.74 inference(scs_inference,[],[5077,5106,5113,4072,5103,5088,4805,4191,45,260,94,85,7,76,18,9,2,6,77,5,88,73,70,79,80,74,84,8,83,16,12,71,14,15,11,13,10,81,4,17,104,100,3,105,91,93,75])). % 118.83/118.74 cnf(5223,plain, % 118.83/118.74 (~E(f15(f15(f6(f4(a28)))),f15(a3))), % 118.83/118.74 inference(scs_inference,[],[5077,5105,5106,5113,5030,4072,5103,5088,4805,4191,28,45,260,94,85,7,76,18,9,2,6,77,5,88,73,70,79,80,74,84,8,83,16,12,71,14,15,11,13,10,81,4,17,104,100,3,105,91,93,75,92,21,110,86])). % 118.83/118.74 cnf(5261,plain, % 118.83/118.74 (~E(f15(f15(f15(f6(f4(a28))))),a3)), % 118.83/118.74 inference(scs_inference,[],[5078,4266,5223,5191,301,94,85,7,76,18,9,2,6,77,5,88,73,70])). % 118.83/118.74 cnf(5275,plain, % 118.83/118.74 (P1(f15(f15(f15(f6(f4(a28))))))), % 118.83/118.74 inference(scs_inference,[],[5078,4266,5223,5191,301,94,85,7,76,18,9,2,6,77,5,88,73,70,79,80,74,84,83,8,16,71])). % 118.83/118.74 cnf(5293,plain, % 118.83/118.74 (P2(f9(a28,f6(f4(a28))))), % 118.83/118.74 inference(scs_inference,[],[5078,5146,5111,4266,5126,5120,5223,5150,5191,5116,4002,301,94,85,7,76,18,9,2,6,77,5,88,73,70,79,80,74,84,83,8,16,71,12,14,15,11,13,81,10,4,17,104,100,3,22,20])). % 118.83/118.74 cnf(5300,plain, % 118.83/118.74 (P1(f6(f15(f15(f6(f4(a28))))))), % 118.83/118.74 inference(scs_inference,[],[5078,5146,5111,4266,5126,5120,5223,5150,5191,5176,5116,4002,301,45,94,85,7,76,18,9,2,6,77,5,88,73,70,79,80,74,84,83,8,16,71,12,14,15,11,13,81,10,4,17,104,100,3,22,20,105,91,93,75])). % 118.83/118.74 cnf(5306,plain, % 118.83/118.74 (~E(f15(a3),f15(f15(f6(f15(f4(a13))))))), % 118.83/118.74 inference(scs_inference,[],[5078,5146,5111,4266,5126,5120,5223,5150,5191,4107,5176,5116,4002,4347,301,28,45,94,85,7,76,18,9,2,6,77,5,88,73,70,79,80,74,84,83,8,16,71,12,14,15,11,13,81,10,4,17,104,100,3,22,20,105,91,93,75,92,110,86])). % 118.83/118.74 cnf(5328,plain, % 118.83/118.74 (~E(f15(f15(f6(f15(f4(a13))))),f15(a3))), % 118.83/118.74 inference(scs_inference,[],[5096,4351,5215,5306,94,85,7,76,18,9,2])). % 118.83/118.74 cnf(5337,plain, % 118.83/118.74 (~E(f15(f6(f15(f6(f4(a28))))),a3)), % 118.83/118.74 inference(scs_inference,[],[5096,4351,5215,5306,1078,94,85,7,76,18,9,2,6,77,5,88,73,70])). % 118.83/118.74 cnf(5351,plain, % 118.83/118.74 (P1(f15(f6(f15(f6(f4(a28))))))), % 118.83/118.74 inference(scs_inference,[],[5096,4351,5215,5306,1078,94,85,7,76,18,9,2,6,77,5,88,73,70,79,80,74,84,83,16,8,71])). % 118.83/118.74 cnf(5367,plain, % 118.83/118.74 (E(f8(f2(a1),f2(a1)),f8(a13,a13))), % 118.83/118.74 inference(scs_inference,[],[5096,5080,5083,4351,5215,5306,4201,1078,94,85,7,76,18,9,2,6,77,5,88,73,70,79,80,74,84,83,16,8,71,12,14,15,11,13,81,10,4,17,104,100,3])). % 118.83/118.74 cnf(5384,plain, % 118.83/118.74 (P2(f5(a28,a1))), % 118.83/118.74 inference(scs_inference,[],[5096,5080,5083,4351,5215,5275,5306,5261,4201,1078,45,43,46,42,94,85,7,76,18,9,2,6,77,5,88,73,70,79,80,74,84,83,16,8,71,12,14,15,11,13,81,10,4,17,104,100,3,105,91,93,75,92,110,111,102])). % 118.83/118.74 cnf(5398,plain, % 118.83/118.74 (P4(a12,f8(f5(a28,a1),f5(a28,a1)))), % 118.83/118.74 inference(scs_inference,[],[5384,94])). % 118.83/118.74 cnf(5402,plain, % 118.83/118.74 (E(f8(f5(a28,a1),a12),a12)), % 118.83/118.74 inference(scs_inference,[],[5384,4347,94,85,76])). % 118.83/118.74 cnf(5409,plain, % 118.83/118.74 (E(f8(a12,f5(a28,a1)),a12)), % 118.83/118.74 inference(scs_inference,[],[5384,5099,4896,4347,94,85,76,7,18,9,2,6,77])). % 118.83/118.74 cnf(5412,plain, % 118.83/118.74 (E(f9(a28,a3),f9(a27,a3))), % 118.83/118.74 inference(scs_inference,[],[5384,5099,4896,4347,28,94,85,76,7,18,9,2,6,77,5,88])). % 118.83/118.74 cnf(5414,plain, % 118.83/118.74 (P2(f11(f5(a28,a1)))), % 118.83/118.74 inference(scs_inference,[],[5384,5099,4896,4347,28,94,85,76,7,18,9,2,6,77,5,88,73])). % 118.83/118.74 cnf(5416,plain, % 118.83/118.74 (~E(f15(f6(f15(f15(f6(f4(a28)))))),a3)), % 118.83/118.74 inference(scs_inference,[],[5384,5099,5300,4896,4347,28,94,85,76,7,18,9,2,6,77,5,88,73,70])). % 118.83/118.74 cnf(5418,plain, % 118.83/118.74 (E(f10(f5(a28,a1),a12),f5(a28,a1))), % 118.83/118.74 inference(scs_inference,[],[5384,5099,5300,4896,4347,28,94,85,76,7,18,9,2,6,77,5,88,73,70,79])). % 118.83/118.74 cnf(5420,plain, % 118.83/118.74 (E(f10(a12,f5(a28,a1)),f5(a28,a1))), % 118.83/118.74 inference(scs_inference,[],[5384,5099,5300,4896,4347,28,94,85,76,7,18,9,2,6,77,5,88,73,70,79,80])). % 118.83/118.74 cnf(5422,plain, % 118.83/118.74 (E(f11(f11(f5(a28,a1))),f5(a28,a1))), % 118.83/118.74 inference(scs_inference,[],[5384,5099,5300,4896,4347,28,94,85,76,7,18,9,2,6,77,5,88,73,70,79,80,74])). % 118.83/118.74 cnf(5436,plain, % 118.83/118.74 (P4(f5(a28,a1),f5(a28,a1))), % 118.83/118.74 inference(scs_inference,[],[5384,5099,5300,4896,4347,28,94,85,76,7,18,9,2,6,77,5,88,73,70,79,80,74,84,83,16,71,8,12,14,15,11,81])). % 118.83/118.74 cnf(5448,plain, % 118.83/118.74 (P2(f10(f5(a28,a1),f5(a28,a1)))), % 118.83/118.74 inference(scs_inference,[],[5384,5099,5300,4896,4347,28,94,85,76,7,18,9,2,6,77,5,88,73,70,79,80,74,84,83,16,71,8,12,14,15,11,81,13,10,4,17,104,100,105,91])). % 118.83/118.74 cnf(5454,plain, % 118.83/118.74 (P2(f8(f5(a28,a1),f5(a28,a1)))), % 118.83/118.74 inference(scs_inference,[],[5384,5099,5300,5351,5337,4896,4347,28,45,94,85,76,7,18,9,2,6,77,5,88,73,70,79,80,74,84,83,16,71,8,12,14,15,11,81,13,10,4,17,104,100,105,91,93,75,92])). % 118.83/118.74 cnf(5460,plain, % 118.83/118.74 (E(f10(f8(f5(a28,a1),f5(a28,a1)),f8(f5(a28,a1),f5(a28,a1))),f8(f10(f5(a28,a1),f5(a28,a1)),f5(a28,a1)))), % 118.83/118.74 inference(scs_inference,[],[5384,5099,5300,5351,5337,4896,4347,28,45,94,85,76,7,18,9,2,6,77,5,88,73,70,79,80,74,84,83,16,71,8,12,14,15,11,81,13,10,4,17,104,100,105,91,93,75,92,110,111,114])). % 118.83/118.74 cnf(5477,plain, % 118.83/118.74 (P5(f15(f6(f15(f4(a27)))),f15(f15(f6(f15(f4(a27))))))), % 118.83/118.74 inference(scs_inference,[],[5454,4425,94,85])). % 118.83/118.74 cnf(5489,plain, % 118.83/118.74 (P2(f11(f8(f5(a28,a1),f5(a28,a1))))), % 118.83/118.74 inference(scs_inference,[],[5412,5454,5003,4425,94,85,76,7,18,9,2,6,77,5,73])). % 118.83/118.74 cnf(5491,plain, % 118.83/118.74 (~E(f15(f15(f15(f15(f4(f2(a1)))))),a3)), % 118.83/118.74 inference(scs_inference,[],[5412,5454,5003,4507,4425,94,85,76,7,18,9,2,6,77,5,73,70])). % 118.83/118.74 cnf(5507,plain, % 118.83/118.74 (E(f9(f9(a28,a3),x55071),f9(f9(a27,a3),x55071))), % 118.83/118.74 inference(scs_inference,[],[5412,5454,5003,4507,4425,94,85,76,7,18,9,2,6,77,5,73,70,79,80,74,84,83,16,71,8,12])). % 118.83/118.74 cnf(5510,plain, % 118.83/118.74 (E(f10(x55101,f9(a28,a3)),f10(x55101,f9(a27,a3)))), % 118.83/118.74 inference(scs_inference,[],[5412,5454,5003,4507,4425,94,85,76,7,18,9,2,6,77,5,73,70,79,80,74,84,83,16,71,8,12,14,15,11])). % 118.83/118.74 cnf(5538,plain, % 118.83/118.74 (P4(a12,f10(f8(f5(a28,a1),f5(a28,a1)),f8(f5(a28,a1),f5(a28,a1))))), % 118.83/118.74 inference(scs_inference,[],[5412,5454,5398,4019,5003,4120,4507,4425,45,29,94,85,76,7,18,9,2,6,77,5,73,70,79,80,74,84,83,16,71,8,12,14,15,11,81,10,13,4,17,104,100,22,105,91,93,92,110,111,114,113,108])). % 118.83/118.74 cnf(5546,plain, % 118.83/118.74 (E(f15(f4(f2(a28))),f4(a28))), % 118.83/118.74 inference(scs_inference,[],[5436,5412,5454,5398,5130,5070,4019,5003,4120,4507,4425,4952,5384,45,29,43,94,85,76,7,18,9,2,6,77,5,73,70,79,80,74,84,83,16,71,8,12,14,15,11,81,10,13,4,17,104,100,22,105,91,93,92,110,111,114,113,108,109,120,115,123])). % 118.83/118.74 cnf(5555,plain, % 118.83/118.74 (P5(f4(f2(a28)),f4(a28))), % 118.83/118.74 inference(scs_inference,[],[5546,1029])). % 118.83/118.74 cnf(5570,plain, % 118.83/118.74 (P2(f11(f11(f5(a28,a1))))), % 118.83/118.74 inference(scs_inference,[],[5418,5414,5546,5416,3947,1029,1034,94,85,76,7,18,9,2,6,77,73])). % 118.83/118.74 cnf(5573,plain, % 118.83/118.74 (~E(f15(f15(f6(f15(f4(f2(a28)))))),a3)), % 118.83/118.74 inference(scs_inference,[],[5418,5414,5546,5416,5020,3947,1029,1034,94,85,76,7,18,9,2,6,77,73,5,70])). % 118.83/118.74 cnf(5603,plain, % 118.83/118.74 (E(f10(f2(a1),f2(a1)),f10(a13,a13))), % 118.83/118.74 inference(scs_inference,[],[5418,5107,5109,5414,5546,5416,4851,5020,3947,1029,1034,94,85,76,7,18,9,2,6,77,73,5,70,79,80,74,84,83,71,16,8,12,14,15,11,81,10,13,4,17,104,100,3])). % 118.83/118.74 cnf(5646,plain, % 118.83/118.74 (P2(f11(f10(f5(a28,a1),f5(a28,a1))))), % 118.83/118.74 inference(scs_inference,[],[5420,5448,5491,3749,94,85,76,7,18,9,2,6,77,73])). % 118.83/118.74 cnf(5649,plain, % 118.83/118.74 (~E(f15(f15(f15(f15(f6(f4(a28)))))),a3)), % 118.83/118.74 inference(scs_inference,[],[5420,5448,5491,5275,3749,94,85,76,7,18,9,2,6,77,73,5,70])). % 118.83/118.74 cnf(5718,plain, % 118.83/118.74 (~E(f15(f15(f6(f15(f6(f4(a28)))))),a3)), % 118.83/118.74 inference(scs_inference,[],[5108,5646,5573,5351,3750,94,85,76,7,18,9,2,6,77,5,73,70])). % 118.83/118.74 cnf(5759,plain, % 118.83/118.74 (~E(f15(f15(f6(f15(f6(f4(a28)))))),f15(a3))), % 118.83/118.74 inference(scs_inference,[],[5108,5507,5646,5573,3711,5351,5337,3750,28,94,85,76,7,18,9,2,6,77,5,73,70,79,80,74,84,83,71,16,8,14,12,15,11,81,10,13,4,17,104,100,3,105,91,92,110,86])). % 118.83/118.74 cnf(5789,plain, % 118.83/118.74 (~E(f15(f15(f6(f15(f4(f2(a1)))))),a3)), % 118.83/118.74 inference(scs_inference,[],[5603,4670,5759,4587,3890,94,85,76,7,18,9,2,6,77,73,79,70])). % 118.83/118.74 cnf(5827,plain, % 118.83/118.74 (~E(f15(a3),f15(f15(f15(f15(f4(a28))))))), % 118.83/118.74 inference(scs_inference,[],[5603,4670,5538,5460,4370,5759,3816,4587,4161,3890,28,94,85,76,7,18,9,2,6,77,73,79,70,5,80,74,84,83,71,8,16,14,12,15,11,81,13,10,4,17,104,100,22,105,91,92,110,86])). % 118.83/118.74 cnf(5876,plain, % 118.83/118.74 (~E(f15(f15(f6(f15(f6(f4(a1)))))),a3)), % 118.83/118.74 inference(scs_inference,[],[5206,5489,5827,4668,3692,8,16,14,12,15,11,85,81,94,13,10,4,17,76,7,18,9,2,6,77,73,79,70])). % 118.83/118.74 cnf(5914,plain, % 118.83/118.74 (E(f6(f2(a28)),f6(a27))), % 118.83/118.74 inference(scs_inference,[],[27,16])). % 118.83/118.74 cnf(5915,plain, % 118.83/118.74 (E(f11(f2(a28)),f11(a27))), % 118.83/118.74 inference(scs_inference,[],[27,16,8])). % 118.83/118.74 cnf(5916,plain, % 118.83/118.74 (E(f5(f2(a28),x59161),f5(a27,x59161))), % 118.83/118.74 inference(scs_inference,[],[27,16,8,14])). % 118.83/118.74 cnf(5918,plain, % 118.83/118.74 (E(f5(x59181,f2(a28)),f5(x59181,a27))), % 118.83/118.74 inference(scs_inference,[],[27,16,8,14,12,15])). % 118.83/118.74 cnf(5919,plain, % 118.83/118.74 (E(f10(x59191,f2(a28)),f10(x59191,a27))), % 118.83/118.74 inference(scs_inference,[],[27,16,8,14,12,15,11])). % 118.83/118.74 cnf(5926,plain, % 118.83/118.74 (E(f5(f2(a28),a27),a18)), % 118.83/118.74 inference(scs_inference,[],[27,5570,3968,16,8,14,12,15,11,81,85,94,175])). % 118.83/118.74 cnf(5929,plain, % 118.83/118.74 (E(f2(f2(a28)),f2(a27))), % 118.83/118.74 inference(scs_inference,[],[27,5570,3968,16,8,14,12,15,11,81,85,94,175,10,13,4])). % 118.83/118.74 cnf(5930,plain, % 118.83/118.74 (E(f7(f2(a28),x59301),f7(a27,x59301))), % 118.83/118.74 inference(scs_inference,[],[27,5570,3968,16,8,14,12,15,11,81,85,94,175,10,13,4,17])). % 118.83/118.74 cnf(5933,plain, % 118.83/118.74 (E(f4(f2(a28)),f4(a27))), % 118.83/118.74 inference(scs_inference,[],[27,5570,3968,16,8,14,12,15,11,81,85,94,175,10,13,4,17,76,7])). % 118.83/118.74 cnf(5935,plain, % 118.83/118.74 (E(f15(f2(a28)),f15(a27))), % 118.83/118.74 inference(scs_inference,[],[27,5570,3968,16,8,14,12,15,11,81,85,94,175,10,13,4,17,76,7,18,9])). % 118.83/118.74 cnf(5937,plain, % 118.83/118.74 (E(f8(x59371,f2(a28)),f8(x59371,a27))), % 118.83/118.74 inference(scs_inference,[],[27,5570,5649,3968,16,8,14,12,15,11,81,85,94,175,10,13,4,17,76,7,18,9,2,6])). % 118.83/118.74 cnf(5944,plain, % 118.83/118.74 (~E(f15(f15(f6(f15(f4(a28))))),a3)), % 118.83/118.74 inference(scs_inference,[],[27,5570,5649,4244,3968,16,8,14,12,15,11,81,85,94,175,10,13,4,17,76,7,18,9,2,6,77,73,79,70])). % 118.83/118.74 cnf(5946,plain, % 118.83/118.74 (E(f8(f2(a28),x59461),f8(a27,x59461))), % 118.83/118.74 inference(scs_inference,[],[27,5570,5649,4244,3968,16,8,14,12,15,11,81,85,94,175,10,13,4,17,76,7,18,9,2,6,77,73,79,70,5])). % 118.83/118.74 cnf(5978,plain, % 118.83/118.74 (P2(f5(f2(a28),a27))), % 118.83/118.74 inference(scs_inference,[],[27,5402,5422,5570,5649,5477,4004,5020,4244,3713,3968,45,170,225,228,16,8,14,12,15,11,81,85,94,175,10,13,4,17,76,7,18,9,2,6,77,73,79,70,5,80,74,84,83,71,92,21,104,24,100,3,105,91,114,113,110,111,102])). % 118.83/118.74 cnf(5988,plain, % 118.83/118.74 (E(f11(f5(f2(a28),x59881)),f11(f5(a27,x59881)))), % 118.83/118.74 inference(scs_inference,[],[5916,16,8])). % 118.83/118.74 cnf(5992,plain, % 118.83/118.74 (E(f10(x59921,f5(f2(a28),x59922)),f10(x59921,f5(a27,x59922)))), % 118.83/118.74 inference(scs_inference,[],[5916,16,8,14,12,15,11])). % 118.83/118.74 cnf(5993,plain, % 118.83/118.74 (P4(f5(f2(a28),a27),f5(f2(a28),a27))), % 118.83/118.74 inference(scs_inference,[],[5916,5978,16,8,14,12,15,11,81])). % 118.83/118.74 cnf(6014,plain, % 118.83/118.74 (P2(f11(f5(f2(a28),a27)))), % 118.83/118.74 inference(scs_inference,[],[5916,5918,5978,5944,301,16,8,14,12,15,11,81,85,94,175,10,13,76,17,4,7,18,9,2,6,77,73])). % 118.83/118.74 cnf(6018,plain, % 118.83/118.74 (~E(f15(f15(f15(f15(f4(a28))))),a3)), % 118.83/118.74 inference(scs_inference,[],[5916,5918,5978,5944,4161,301,16,8,14,12,15,11,81,85,94,175,10,13,76,17,4,7,18,9,2,6,77,73,79,70])). % 118.83/118.74 cnf(6029,plain, % 118.83/118.74 (P1(f15(f6(f15(f15(f4(a27))))))), % 118.83/118.74 inference(scs_inference,[],[5916,5918,5978,5944,4286,4161,301,16,8,14,12,15,11,81,85,94,175,10,13,76,17,4,7,18,9,2,6,77,73,79,70,80,5,74,84,83,71])). % 118.83/118.74 cnf(6088,plain, % 118.83/118.74 (~E(f15(f15(f6(f15(f15(f4(a27)))))),a3)), % 118.83/118.74 inference(scs_inference,[],[5914,4829,6029,6018,1078,16,8,14,12,15,81,85,11,94,10,13,76,17,4,7,18,9,2,6,77,79,73,70])). % 118.83/118.74 cnf(6159,plain, % 118.83/118.74 (~E(f15(f15(f6(f15(f4(a13))))),a3)), % 118.83/118.74 inference(scs_inference,[],[5915,3876,5718,4347,28,16,8,14,12,81,15,85,11,94,10,13,76,17,4,7,18,9,2,77,6,79,73,70])). % 118.83/118.74 cnf(6170,plain, % 118.83/118.74 (P1(f15(f15(f6(f15(f4(a28))))))), % 118.83/118.74 inference(scs_inference,[],[5915,3876,5718,4244,4347,28,16,8,14,12,81,15,85,11,94,10,13,76,17,4,7,18,9,2,77,6,79,73,70,80,5,74,84,83,71])). % 118.83/118.74 cnf(6190,plain, % 118.83/118.74 (~E(x61901,f15(a3))+~E(f15(f15(f15(f4(a27)))),x61901)), % 118.83/118.74 inference(scs_inference,[],[5915,3876,4767,5718,5944,4851,4244,4347,28,1125,45,16,8,14,12,81,15,85,11,94,10,13,76,17,4,7,18,9,2,77,6,79,73,70,80,5,74,84,83,71,93,75,92,104,100,105,91,110,111,3])). % 118.83/118.74 cnf(6225,plain, % 118.83/118.74 (~E(f15(f15(f15(f6(f15(f4(a28)))))),a3)), % 118.83/118.74 inference(scs_inference,[],[5929,4920,6170,6159,16,8,14,12,81,15,11,94,10,13,76,17,4,7,18,9,2,77,6,79,73,70])). % 118.83/118.74 cnf(6247,plain, % 118.83/118.74 (E(f4(f2(a28)),f4(a13))), % 118.83/118.74 inference(scs_inference,[],[5929,5933,5926,5993,4920,6170,6159,3936,1113,45,16,8,14,12,81,15,11,94,10,13,76,17,4,7,18,9,2,77,6,79,73,70,80,5,74,84,83,71,93,92,104,100,22,3])). % 118.83/118.74 cnf(6254,plain, % 118.83/118.74 (~E(f15(f15(f15(f6(f15(f4(a28)))))),f15(a3))), % 118.83/118.74 inference(scs_inference,[],[5929,5933,5926,5993,4920,6170,6159,5944,3936,28,1113,45,16,8,14,12,81,15,11,94,10,13,76,17,4,7,18,9,2,77,6,79,73,70,80,5,74,84,83,71,93,92,104,100,22,3,105,91,110,86])). % 118.83/118.74 cnf(6292,plain, % 118.83/118.74 (~E(f15(f15(f6(f15(f4(a27))))),a3)), % 118.83/118.74 inference(scs_inference,[],[5935,4511,6254,4425,16,8,14,12,81,15,11,94,10,13,76,17,4,7,18,9,2,77,6,79,73,80,70])). % 118.83/118.74 cnf(6301,plain, % 118.83/118.74 (P1(f15(f15(f6(f15(f4(a27))))))), % 118.83/118.74 inference(scs_inference,[],[5935,4511,6254,4425,16,8,14,12,81,15,11,94,10,13,76,17,4,7,18,9,2,77,6,79,73,80,70,74,5,84,83,71])). % 118.83/118.74 cnf(6320,plain, % 118.83/118.74 (~E(f15(a3),f15(f15(f6(f15(f4(a28))))))), % 118.83/118.74 inference(scs_inference,[],[5935,4511,4450,4127,6254,4579,5020,4425,4244,28,45,242,16,8,14,12,81,15,11,94,10,13,76,17,4,7,18,9,2,77,6,79,73,80,70,74,5,84,83,71,93,75,92,104,25,100,105,91,110,86])). % 118.83/118.74 cnf(6375,plain, % 118.83/118.74 (E(f8(f11(a20),f11(a20)),f8(a20,a20))), % 118.83/118.74 inference(scs_inference,[],[5555,5919,6247,4431,6301,6320,45,35,16,8,14,12,81,15,11,94,10,13,76,17,4,7,18,9,2,77,6,79,73,70,80,74,5,84,83,71,93,92,24,104,100])). % 118.83/118.74 cnf(6423,plain, % 118.83/118.74 (~E(f15(f15(f4(a13))),a3)), % 118.83/118.74 inference(scs_inference,[],[6375,5293,6292,3749,16,8,12,14,81,15,94,11,10,13,76,17,4,7,18,9,2,77,6,79,73,80,70])). % 118.83/118.74 cnf(6432,plain, % 118.83/118.74 (P1(f15(f15(f15(f15(f4(a28))))))), % 118.83/118.74 inference(scs_inference,[],[6375,5293,6292,4161,3749,16,8,12,14,81,15,94,11,10,13,76,17,4,7,18,9,2,77,6,79,73,80,70,74,5,84,83,71])). % 118.83/118.74 cnf(6510,plain, % 118.83/118.74 (P2(f11(f5(a27,a27)))), % 118.83/118.74 inference(scs_inference,[],[5930,6014,6423,6432,5988,45,203,16,8,12,14,81,15,94,11,13,76,10,17,4,7,18,9,77,2,6,79,73,80,70,74,5,84,83,71,93,92,104,100,20])). % 118.83/118.74 cnf(6558,plain, % 118.83/118.74 (P2(f11(f11(f5(a27,a27))))), % 118.83/118.74 inference(scs_inference,[],[5937,6510,6088,16,8,12,81,14,15,94,11,13,76,10,17,4,7,18,9,77,2,6,79,73])). % 118.83/118.74 cnf(6562,plain, % 118.83/118.74 (~E(f15(f15(f4(f2(a1)))),a3)), % 118.83/118.74 inference(scs_inference,[],[5937,6510,6088,3750,16,8,12,81,14,15,94,11,13,76,10,17,4,7,18,9,77,2,6,79,73,80,70])). % 118.83/118.74 cnf(6569,plain, % 118.83/118.74 (P1(f15(f15(f6(f15(f4(a13))))))), % 118.83/118.74 inference(scs_inference,[],[5937,6510,6088,4347,3750,16,8,12,81,14,15,94,11,13,76,10,17,4,7,18,9,77,2,6,79,73,80,70,74,5,84,71])). % 118.83/118.74 cnf(6575,plain, % 118.83/118.74 (P1(f6(f15(f15(f4(f2(a1))))))), % 118.83/118.74 inference(scs_inference,[],[5937,6510,6088,4533,4347,4049,3750,131,16,8,12,81,14,15,94,11,13,76,10,17,4,7,18,9,77,2,6,79,73,80,70,74,5,84,71,83,93,75])). % 118.83/118.74 cnf(6663,plain, % 118.83/118.74 (P2(f5(f2(a28),a13))), % 118.83/118.74 inference(scs_inference,[],[5946,6558,4027,5992,6562,6569,6247,170,267,44,74,84,5,83,71,16,8,81,12,14,15,94,11,76,13,10,17,4,7,18,9,77,2,6,79,73,80,70,105,91,93,92,104,22,100,102])). % 118.83/118.74 cnf(6686,plain, % 118.83/118.74 (P1(f15(a3))), % 118.83/118.74 inference(scs_inference,[],[28,5367,6663,74,84,5,83,71])). % 118.83/118.74 cnf(6723,plain, % 118.83/118.74 (~E(f15(a3),a3)), % 118.83/118.74 inference(scs_inference,[],[28,5367,6663,5876,74,84,5,83,71,16,85,8,81,14,12,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,80,70])). % 118.83/118.74 cnf(6729,plain, % 118.83/118.74 (P2(f9(a27,a3))), % 118.83/118.74 inference(scs_inference,[],[28,5367,6663,5876,45,74,84,5,83,71,16,85,8,81,14,12,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,80,70,105,91,93])). % 118.83/118.74 cnf(6731,plain, % 118.83/118.74 (P1(f6(f15(a3)))), % 118.83/118.74 inference(scs_inference,[],[28,5367,6663,5876,45,74,84,5,83,71,16,85,8,81,14,12,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,80,70,105,91,93,75])). % 118.83/118.74 cnf(6733,plain, % 118.83/118.74 (E(f15(f6(f15(a3))),f15(a3))), % 118.83/118.74 inference(scs_inference,[],[28,5367,6663,5876,45,74,84,5,83,71,16,85,8,81,14,12,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,80,70,105,91,93,75,78])). % 118.83/118.74 cnf(6749,plain, % 118.83/118.74 (~E(f15(f4(a28)),f15(a3))), % 118.83/118.74 inference(scs_inference,[],[28,5367,6663,5409,5876,3820,3868,3948,4952,225,45,74,84,5,83,71,16,85,8,81,14,12,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,80,70,105,91,93,75,78,92,104,25,100,3,114,113,110,86])). % 118.83/118.74 cnf(6755,plain, % 118.83/118.74 (~E(f15(f15(f15(f4(a27)))),f15(f6(f15(a3))))), % 118.83/118.74 inference(scs_inference,[],[28,5367,6663,5409,5876,3820,3868,3948,4952,225,45,74,84,5,83,71,16,85,8,81,14,12,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,80,70,105,91,93,75,78,92,104,25,100,3,114,113,110,86,111,120,6190])). % 118.83/118.74 cnf(6758,plain, % 118.83/118.74 (E(f9(a27,a3),f9(a28,a3))), % 118.83/118.74 inference(scs_inference,[],[28,5367,6663,5409,5876,3820,3868,3948,169,4952,225,45,43,74,84,5,83,71,16,85,8,81,14,12,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,80,70,105,91,93,75,78,92,104,25,100,3,114,113,110,86,111,120,6190,125,101])). % 118.83/118.74 cnf(6767,plain, % 118.83/118.74 (E(f8(f9(a27,a3),x67671),f8(f9(a28,a3),x67671))), % 118.83/118.74 inference(scs_inference,[],[6758,6729,74,84,5])). % 118.83/118.74 cnf(6770,plain, % 118.83/118.74 (P1(f15(f15(a3)))), % 118.83/118.74 inference(scs_inference,[],[6758,6729,6686,74,84,5,83,71])). % 118.83/118.74 cnf(6776,plain, % 118.83/118.74 (P4(f9(a27,a3),f9(a27,a3))), % 118.83/118.74 inference(scs_inference,[],[6758,6729,6686,6731,74,84,5,83,71,16,85,8,81])). % 118.83/118.74 cnf(6780,plain, % 118.83/118.74 (P4(a12,f8(f9(a27,a3),f9(a27,a3)))), % 118.83/118.74 inference(scs_inference,[],[6758,6729,6686,6731,74,84,5,83,71,16,85,8,81,14,12,94])). % 118.83/118.74 cnf(6783,plain, % 118.83/118.74 (E(f10(x67831,f9(a27,a3)),f10(x67831,f9(a28,a3)))), % 118.83/118.74 inference(scs_inference,[],[6758,6729,6686,6731,74,84,5,83,71,16,85,8,81,14,12,94,15,11])). % 118.83/118.74 cnf(6799,plain, % 118.83/118.74 (~E(a3,f15(a3))), % 118.83/118.74 inference(scs_inference,[],[6758,6729,6686,6723,6731,74,84,5,83,71,16,85,8,81,14,12,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2])). % 118.83/118.74 cnf(6800,plain, % 118.83/118.74 (E(f10(f9(a27,a3),a12),f9(a27,a3))), % 118.83/118.74 inference(scs_inference,[],[6758,6729,6686,6723,6731,74,84,5,83,71,16,85,8,81,14,12,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79])). % 118.83/118.74 cnf(6804,plain, % 118.83/118.74 (E(f8(x68041,f9(a27,a3)),f8(x68041,f9(a28,a3)))), % 118.83/118.74 inference(scs_inference,[],[6758,6729,6686,6723,6731,74,84,5,83,71,16,85,8,81,14,12,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6])). % 118.83/118.74 cnf(6805,plain, % 118.83/118.74 (E(f10(a12,f9(a27,a3)),f9(a27,a3))), % 118.83/118.74 inference(scs_inference,[],[6758,6729,6686,6723,6731,74,84,5,83,71,16,85,8,81,14,12,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,80])). % 118.83/118.74 cnf(6807,plain, % 118.83/118.74 (~E(f15(f15(a3)),a3)), % 118.83/118.74 inference(scs_inference,[],[6758,6729,6686,6723,6731,74,84,5,83,71,16,85,8,81,14,12,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,80,70])). % 118.83/118.74 cnf(6811,plain, % 118.83/118.74 (P2(f10(f9(a27,a3),f9(a27,a3)))), % 118.83/118.74 inference(scs_inference,[],[6758,6729,6686,6723,6731,74,84,5,83,71,16,85,8,81,14,12,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,80,70,105,91])). % 118.83/118.74 cnf(6813,plain, % 118.83/118.74 (P2(f9(f2(a1),a3))), % 118.83/118.74 inference(scs_inference,[],[28,6758,6729,6686,6723,6731,131,74,84,5,83,71,16,85,8,81,14,12,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,80,70,105,91,93])). % 118.83/118.74 cnf(6815,plain, % 118.83/118.74 (P1(f6(f15(f15(a3))))), % 118.83/118.74 inference(scs_inference,[],[28,6758,6729,6686,6723,6731,131,74,84,5,83,71,16,85,8,81,14,12,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,80,70,105,91,93,75])). % 118.83/118.74 cnf(6817,plain, % 118.83/118.74 (E(f15(f6(f15(f15(a3)))),f15(f15(a3)))), % 118.83/118.74 inference(scs_inference,[],[28,6758,6729,6686,6723,6731,131,74,84,5,83,71,16,85,8,81,14,12,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,80,70,105,91,93,75,78])). % 118.83/118.74 cnf(6819,plain, % 118.83/118.74 (P2(f8(f9(a27,a3),f9(a27,a3)))), % 118.83/118.74 inference(scs_inference,[],[28,6758,6729,6686,6723,6731,131,74,84,5,83,71,16,85,8,81,14,12,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,80,70,105,91,93,75,78,92])). % 118.83/118.74 cnf(6825,plain, % 118.83/118.74 (~E(f15(f4(a28)),f15(f6(f15(a3))))), % 118.83/118.74 inference(scs_inference,[],[28,6758,6729,6686,6723,6749,6731,6733,131,74,84,5,83,71,16,85,8,81,14,12,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,80,70,105,91,93,75,78,92,104,100,3])). % 118.83/118.74 cnf(6828,plain, % 118.83/118.74 (~E(f15(f15(a3)),f15(a3))), % 118.83/118.74 inference(scs_inference,[],[28,6758,6729,6686,6723,6749,6731,6733,131,74,84,5,83,71,16,85,8,81,14,12,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,80,70,105,91,93,75,78,92,104,100,3,110,86])). % 118.83/118.74 cnf(6832,plain, % 118.83/118.74 (P2(f9(a13,a3))), % 118.83/118.74 inference(scs_inference,[],[28,6758,6729,6686,6723,6749,6731,6733,131,74,84,5,83,71,16,85,8,81,14,12,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,80,70,105,91,93,75,78,92,104,100,3,110,86,111,645])). % 118.83/118.74 cnf(6833,plain, % 118.83/118.74 (P4(f9(a28,a3),f9(a27,a3))), % 118.83/118.74 inference(scs_inference,[],[28,6758,6729,6686,6723,6749,6731,6733,131,74,84,5,83,71,16,85,8,81,14,12,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,80,70,105,91,93,75,78,92,104,100,3,110,86,111,645,21])). % 118.83/118.74 cnf(6844,plain, % 118.83/118.74 (P2(f9(a1,a3))), % 118.83/118.74 inference(scs_inference,[],[6813,534])). % 118.83/118.74 cnf(6853,plain, % 118.83/118.74 (P1(f15(f15(f15(a3))))), % 118.83/118.74 inference(scs_inference,[],[6832,6800,6770,74,84,5,83,71])). % 118.83/118.74 cnf(6882,plain, % 118.83/118.74 (~E(f15(a3),f15(f15(a3)))), % 118.83/118.74 inference(scs_inference,[],[6832,6800,6828,6770,74,84,5,83,71,85,16,81,8,12,14,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2])). % 118.83/118.74 cnf(6883,plain, % 118.83/118.74 (E(f10(f9(a13,a3),a12),f9(a13,a3))), % 118.83/118.74 inference(scs_inference,[],[6832,6800,6828,6770,74,84,5,83,71,85,16,81,8,12,14,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79])). % 118.83/118.74 cnf(6885,plain, % 118.83/118.74 (P2(f11(f9(a13,a3)))), % 118.83/118.74 inference(scs_inference,[],[6832,6800,6828,6770,74,84,5,83,71,85,16,81,8,12,14,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73])). % 118.83/118.74 cnf(6888,plain, % 118.83/118.74 (~E(f15(f15(f15(a3))),a3)), % 118.83/118.74 inference(scs_inference,[],[6832,6800,6828,6770,74,84,5,83,71,85,16,81,8,12,14,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,70])). % 118.83/118.74 cnf(6890,plain, % 118.83/118.74 (E(f10(a12,f9(a13,a3)),f9(a13,a3))), % 118.83/118.74 inference(scs_inference,[],[6832,6800,6828,6770,74,84,5,83,71,85,16,81,8,12,14,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,70,80])). % 118.83/118.74 cnf(6894,plain, % 118.83/118.74 (P2(f10(f9(a13,a3),f9(a13,a3)))), % 118.83/118.74 inference(scs_inference,[],[6832,6800,6828,6770,74,84,5,83,71,85,16,81,8,12,14,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,70,80,105,91])). % 118.83/118.74 cnf(6898,plain, % 118.83/118.74 (P1(f6(f15(f15(f15(a3)))))), % 118.83/118.74 inference(scs_inference,[],[28,6832,6800,6828,6770,170,74,84,5,83,71,85,16,81,8,12,14,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,70,80,105,91,93,75])). % 118.83/118.74 cnf(6900,plain, % 118.83/118.74 (E(f15(f6(f15(f15(f15(a3))))),f15(f15(f15(a3))))), % 118.83/118.74 inference(scs_inference,[],[28,6832,6800,6828,6770,170,74,84,5,83,71,85,16,81,8,12,14,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,70,80,105,91,93,75,78])). % 118.83/118.74 cnf(6908,plain, % 118.83/118.74 (E(f10(f9(a27,a3),a12),f9(a28,a3))), % 118.83/118.74 inference(scs_inference,[],[28,6832,6800,6828,6770,6758,170,74,84,5,83,71,85,16,81,8,12,14,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,70,80,105,91,93,75,78,92,104,100,3])). % 118.83/118.74 cnf(6913,plain, % 118.83/118.74 (P4(f10(f9(a13,a3),f9(a27,a3)),f10(f9(a13,a3),f9(a27,a3)))), % 118.83/118.74 inference(scs_inference,[],[28,6776,6832,6800,6828,6770,6758,6729,170,74,84,5,83,71,85,16,81,8,12,14,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,70,80,105,91,93,75,78,92,104,100,3,110,111,115])). % 118.83/118.74 cnf(6927,plain, % 118.83/118.74 (P1(f15(f6(f15(f15(a3)))))), % 118.83/118.74 inference(scs_inference,[],[6844,6805,6815,74,84,83,5,71])). % 118.83/118.74 cnf(6941,plain, % 118.83/118.74 (E(f8(f9(a1,a3),a12),a12)), % 118.83/118.74 inference(scs_inference,[],[6844,6805,6815,74,84,83,5,71,85,16,81,8,12,14,94,15,11,76])). % 118.83/118.74 cnf(6956,plain, % 118.83/118.74 (~E(a3,f15(f15(a3)))), % 118.83/118.74 inference(scs_inference,[],[6844,6805,6807,6815,74,84,83,5,71,85,16,81,8,12,14,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2])). % 118.83/118.74 cnf(6957,plain, % 118.83/118.74 (E(f10(f9(a1,a3),a12),f9(a1,a3))), % 118.83/118.74 inference(scs_inference,[],[6844,6805,6807,6815,74,84,83,5,71,85,16,81,8,12,14,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79])). % 118.83/118.74 cnf(6959,plain, % 118.83/118.74 (P2(f11(f9(a1,a3)))), % 118.83/118.74 inference(scs_inference,[],[6844,6805,6807,6815,74,84,83,5,71,85,16,81,8,12,14,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73])). % 118.83/118.74 cnf(6962,plain, % 118.83/118.74 (E(f10(a12,f9(a1,a3)),f9(a1,a3))), % 118.83/118.74 inference(scs_inference,[],[6844,6805,6807,6815,74,84,83,5,71,85,16,81,8,12,14,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,80])). % 118.83/118.74 cnf(6970,plain, % 118.83/118.74 (P2(f9(a28,a3))), % 118.83/118.74 inference(scs_inference,[],[28,6844,6805,6807,6815,43,74,84,83,5,71,85,16,81,8,12,14,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,80,70,105,91,93])). % 118.83/118.74 cnf(6972,plain, % 118.83/118.74 (P1(f6(f15(f6(f15(f15(a3))))))), % 118.83/118.74 inference(scs_inference,[],[28,6844,6805,6807,6815,43,74,84,83,5,71,85,16,81,8,12,14,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,80,70,105,91,93,75])). % 118.83/118.74 cnf(6980,plain, % 118.83/118.74 (P2(f8(f9(a27,a3),f9(a28,a3)))), % 118.83/118.74 inference(scs_inference,[],[28,6844,6805,6819,6807,6913,6804,6783,6815,43,74,84,83,5,71,85,16,81,8,12,14,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,80,70,105,91,93,75,21,92,104,20])). % 118.83/118.74 cnf(6984,plain, % 118.83/118.74 (~E(a3,f15(f6(f15(a3))))), % 118.83/118.74 inference(scs_inference,[],[28,6844,6799,6805,6819,6807,6913,6804,6783,6815,6733,43,74,84,83,5,71,85,16,81,8,12,14,94,15,11,76,13,10,17,4,7,88,18,87,9,77,2,79,73,6,80,70,105,91,93,75,21,92,104,20,100,3])). % 118.83/118.74 cnf(7010,plain, % 118.83/118.74 (P1(f15(f15(f15(f15(a3)))))), % 118.83/118.74 inference(scs_inference,[],[6970,6883,6853,74,84,83,5,71])). % 118.83/118.74 cnf(7039,plain, % 118.83/118.74 (~E(a3,f15(f15(f15(a3))))), % 118.83/118.74 inference(scs_inference,[],[6970,6883,6853,6888,74,84,83,5,71,85,16,81,8,14,12,94,15,11,76,13,10,17,4,7,88,18,87,77,9,2])). % 118.83/118.74 cnf(7040,plain, % 118.83/118.74 (E(f10(f9(a28,a3),a12),f9(a28,a3))), % 118.83/118.74 inference(scs_inference,[],[6970,6883,6853,6888,74,84,83,5,71,85,16,81,8,14,12,94,15,11,76,13,10,17,4,7,88,18,87,77,9,2,79])). % 118.83/118.74 cnf(7044,plain, % 118.83/118.74 (E(f10(a12,f9(a28,a3)),f9(a28,a3))), % 118.83/118.74 inference(scs_inference,[],[6970,6883,6853,6888,74,84,83,5,71,85,16,81,8,14,12,94,15,11,76,13,10,17,4,7,88,18,87,77,9,2,79,73,80])). % 118.83/118.74 cnf(7046,plain, % 118.83/118.74 (~E(f15(f15(f15(f15(a3)))),a3)), % 118.83/118.74 inference(scs_inference,[],[6970,6883,6853,6888,74,84,83,5,71,85,16,81,8,14,12,94,15,11,76,13,10,17,4,7,88,18,87,77,9,2,79,73,80,70])). % 118.83/118.74 cnf(7051,plain, % 118.83/118.74 (P2(f10(f9(a28,a3),f9(a28,a3)))), % 118.83/118.74 inference(scs_inference,[],[6970,6883,6853,6888,74,84,83,5,71,85,16,81,8,14,12,94,15,11,76,13,10,17,4,7,88,18,87,77,9,2,79,73,80,70,6,105,91])). % 118.83/118.74 cnf(7055,plain, % 118.83/118.74 (P1(f6(f15(f15(f15(f15(a3))))))), % 118.83/118.74 inference(scs_inference,[],[6970,6883,6853,6888,45,74,84,83,5,71,85,16,81,8,14,12,94,15,11,76,13,10,17,4,7,88,18,87,77,9,2,79,73,80,70,6,105,91,93,75])). % 118.83/118.74 cnf(7057,plain, % 118.83/118.74 (P2(f8(f9(a28,a3),f9(a28,a3)))), % 118.83/118.74 inference(scs_inference,[],[6970,6883,6853,6888,45,74,84,83,5,71,85,16,81,8,14,12,94,15,11,76,13,10,17,4,7,88,18,87,77,9,2,79,73,80,70,6,105,91,93,75,92])). % 118.83/118.74 cnf(7089,plain, % 118.83/118.74 (P1(f15(f6(f15(f15(f15(a3))))))), % 118.83/118.74 inference(scs_inference,[],[6957,6885,6898,74,84,83,5,71])). % 118.83/118.74 cnf(7114,plain, % 118.83/118.74 (~E(f15(f6(f15(a3))),a3)), % 118.83/118.74 inference(scs_inference,[],[6957,6885,6984,6898,74,84,83,5,71,85,81,16,8,14,12,94,15,11,76,13,10,17,4,7,18,77,9,2])). % 118.83/118.74 cnf(7115,plain, % 118.83/118.74 (P2(f11(f11(f9(a13,a3))))), % 118.83/118.74 inference(scs_inference,[],[6957,6885,6984,6898,74,84,83,5,71,85,81,16,8,14,12,94,15,11,76,13,10,17,4,7,18,77,9,2,73])). % 118.83/118.74 cnf(7137,plain, % 118.83/118.74 (~E(f15(a3),f15(f6(f15(f15(a3)))))), % 118.83/118.74 inference(scs_inference,[],[6957,6885,6882,6984,6898,6817,5555,5933,74,84,83,5,71,85,81,16,8,14,12,94,15,11,76,13,10,17,4,7,18,77,9,2,73,79,80,70,6,105,91,75,92,24,104,100,3])). % 118.83/118.74 cnf(7160,plain, % 118.83/118.74 (P1(f15(f15(f6(f15(f15(a3))))))), % 118.83/118.74 inference(scs_inference,[],[6962,6894,6927,74,84,83,5,71])). % 118.83/118.74 cnf(7185,plain, % 118.83/118.74 (~E(f15(f6(f15(a3))),f15(f4(a28)))), % 118.83/118.74 inference(scs_inference,[],[6962,6894,6825,6927,74,84,83,5,71,85,81,16,8,14,12,94,15,11,76,13,10,17,4,7,18,77,9,2])). % 118.83/118.74 cnf(7226,plain, % 118.83/118.74 (P1(f15(f15(f15(f15(f15(a3))))))), % 118.83/118.74 inference(scs_inference,[],[6959,7010,74,84,83,71])). % 118.83/118.74 cnf(7277,plain, % 118.83/118.74 (~E(f15(a3),f15(f15(f15(a3))))), % 118.83/118.74 inference(scs_inference,[],[28,6890,6959,6956,7010,7137,6817,6770,74,84,83,71,5,81,85,16,8,14,94,12,15,76,11,13,10,17,4,7,18,77,9,79,2,73,80,70,6,105,91,75,92,104,100,3,110,86])). % 118.83/118.74 cnf(7325,plain, % 118.83/118.74 (~E(f15(f15(f15(a3))),f15(a3))), % 118.83/118.74 inference(scs_inference,[],[6908,7051,7277,6972,74,84,83,71,5,81,16,8,94,14,12,15,76,11,13,17,10,4,7,18,77,9,79,73,2])). % 118.83/118.74 cnf(7341,plain, % 118.83/118.74 (E(f10(f9(a28,a3),a12),f9(a27,a3))), % 118.83/118.74 inference(scs_inference,[],[6908,7040,7051,7277,6972,5412,74,84,83,71,5,81,16,8,94,14,12,15,76,11,13,17,10,4,7,18,77,9,79,73,2,80,70,6,105,91,92,104,100,3])). % 118.83/118.74 cnf(7344,plain, % 118.83/118.74 (~E(f15(f15(a3)),f15(f15(f15(f15(a3)))))), % 118.83/118.74 inference(scs_inference,[],[6908,7040,7051,7277,6972,6686,6853,5412,74,84,83,71,5,81,16,8,94,14,12,15,76,11,13,17,10,4,7,18,77,9,79,73,2,80,70,6,105,91,92,104,100,3,110,86])). % 118.83/118.74 cnf(7352,plain, % 118.83/118.74 (P2(f10(f9(a28,a3),f9(a27,a3)))), % 118.83/118.74 inference(scs_inference,[],[6833,6908,7040,7051,7277,6972,5510,7114,6686,6853,5412,6729,6970,74,84,83,71,5,81,16,8,94,14,12,15,76,11,13,17,10,4,7,18,77,9,79,73,2,80,70,6,105,91,92,104,100,3,110,86,111,115,75,20])). % 118.83/118.74 cnf(7408,plain, % 118.83/118.74 (~E(f15(f15(f15(a3))),f15(f6(f15(a3))))), % 118.83/118.74 inference(scs_inference,[],[7044,7352,6767,7325,7046,7055,6780,6733,74,84,83,71,5,81,16,8,94,14,12,15,76,11,13,17,10,4,7,18,77,9,73,79,2,80,70,6,105,91,92,104,22,100,3])). % 118.83/118.74 cnf(7462,plain, % 118.83/118.74 (E(f8(f9(a1,a3),a12),f11(a12))), % 118.83/118.74 inference(scs_inference,[],[7341,6980,6941,7408,7089,225,77,9,73,79,2,80,70,74,6,84,83,71,5,81,16,8,94,12,14,15,76,11,13,17,10,4,7,18,105,91,3])). % 118.83/118.74 cnf(7477,plain, % 118.83/118.74 (E(f8(a12,a12),a12)), % 118.83/118.74 inference(scs_inference,[],[29,77])). % 118.83/118.74 cnf(7480,plain, % 118.83/118.74 (P2(f11(f10(f9(a27,a3),f9(a27,a3))))), % 118.83/118.74 inference(scs_inference,[],[29,7462,6811,77,9,73])). % 118.83/118.74 cnf(7519,plain, % 118.83/118.74 (P2(f10(a12,a12))), % 118.83/118.74 inference(scs_inference,[],[29,7462,6811,7344,7160,77,9,73,80,79,2,70,74,84,6,83,71,5,81,16,94,8,14,12,15,76,11,13,17,10,4,7,18,105,91])). % 118.83/118.74 cnf(7528,plain, % 118.83/118.74 (E(f8(f11(a12),f11(a12)),f8(a12,a12))), % 118.83/118.74 inference(scs_inference,[],[29,7462,6811,7039,7344,7160,6900,170,77,9,73,80,79,2,70,74,84,6,83,71,5,81,16,94,8,14,12,15,76,11,13,17,10,4,7,18,105,91,3,93,92,104,100])). % 118.83/118.74 cnf(7562,plain, % 118.83/118.74 (E(f10(a12,f10(a12,a12)),f10(a12,a12))), % 118.83/118.74 inference(scs_inference,[],[7519,7477,77,9,80])). % 118.83/118.74 cnf(7564,plain, % 118.83/118.74 (P2(f11(f10(a12,a12)))), % 118.83/118.74 inference(scs_inference,[],[7519,7477,77,9,80,73])). % 118.83/118.74 cnf(7589,plain, % 118.83/118.74 (E(f5(x75891,f8(a12,a12)),f5(x75891,a12))), % 118.83/118.74 inference(scs_inference,[],[7519,7477,6755,7226,77,9,80,73,79,2,70,74,84,6,83,71,5,81,16,94,8,14,12,15])). % 118.83/118.74 cnf(7592,plain, % 118.83/118.74 (E(f10(x75921,f8(a12,a12)),f10(x75921,a12))), % 118.83/118.74 inference(scs_inference,[],[7519,7477,6755,7226,77,9,80,73,79,2,70,74,84,6,83,71,5,81,16,94,8,14,12,15,76,11])). % 118.83/118.74 cnf(7594,plain, % 118.83/118.74 (E(f10(f8(a12,a12),x75941),f10(a12,x75941))), % 118.83/118.74 inference(scs_inference,[],[7519,7477,6755,7226,77,9,80,73,79,2,70,74,84,6,83,71,5,81,16,94,8,14,12,15,76,11,13,10])). % 118.83/118.74 cnf(7601,plain, % 118.83/118.74 (P2(f10(f10(a12,a12),f10(a12,a12)))), % 118.83/118.74 inference(scs_inference,[],[7519,7477,6755,7226,77,9,80,73,79,2,70,74,84,6,83,71,5,81,16,94,8,14,12,15,76,11,13,10,17,4,7,18,105,91])). % 118.83/118.74 cnf(7603,plain, % 118.83/118.74 (E(f8(a12,a12),f11(a12))), % 118.83/118.74 inference(scs_inference,[],[7519,7477,6755,7226,225,77,9,80,73,79,2,70,74,84,6,83,71,5,81,16,94,8,14,12,15,76,11,13,10,17,4,7,18,105,91,3])). % 118.83/118.74 cnf(7653,plain, % 118.83/118.74 (E(f8(x76531,f8(a12,a12)),f8(x76531,f11(a12)))), % 118.83/118.74 inference(scs_inference,[],[7603,7564,5789,6575,77,9,79,80,73,2,74,70,84,6])). % 118.83/118.74 cnf(7718,plain, % 118.83/118.74 (P2(f11(f10(f10(a12,a12),f10(a12,a12))))), % 118.83/118.74 inference(scs_inference,[],[7528,7601,77,9,80,79,73])). % 118.83/118.74 cnf(7721,plain, % 118.83/118.74 (~E(f15(f15(f6(f4(a1)))),a3)), % 118.83/118.74 inference(scs_inference,[],[7528,7601,6225,3890,77,9,80,79,73,2,70])). % 118.83/118.74 cnf(7730,plain, % 118.83/118.74 (P1(f15(f6(f15(a3))))), % 118.83/118.74 inference(scs_inference,[],[7528,7601,6225,6731,3890,77,9,80,79,73,2,70,74,84,6,83,71])). % 118.83/118.74 cnf(7762,plain, % 118.83/118.74 (P1(f6(f15(f6(f15(a3)))))), % 118.83/118.74 inference(scs_inference,[],[7528,7601,6225,7114,6731,3890,7603,77,9,80,79,73,2,70,74,84,6,83,71,5,85,81,16,94,8,14,12,76,15,11,88,13,87,17,10,4,7,18,105,91,3,75])). % 118.83/118.74 cnf(7803,plain, % 118.83/118.74 (E(f11(f11(f9(f2(a1),a3))),f9(f2(a1),a3))), % 118.83/118.74 inference(scs_inference,[],[7562,6813,7730,7721,77,9,80,79,73,2,70,74])). % 118.83/118.74 cnf(8088,plain, % 118.83/118.74 (~E(f15(f6(f15(f6(f15(a3))))),a3)), % 118.83/118.74 inference(scs_inference,[],[7115,7762,77,79,80,73,70])). % 118.83/118.74 cnf(8237,plain, % 118.83/118.74 (~E(f15(f15(f15(f4(a27)))),a3)), % 118.83/118.74 inference(scs_inference,[],[7589,7718,3968,10,17,4,7,77,18,79,80,70])). % 118.83/118.74 cnf(8247,plain, % 118.83/118.74 (P1(f15(f15(f4(a13))))), % 118.83/118.74 inference(scs_inference,[],[7589,7718,8088,3749,3968,10,17,4,7,77,18,79,80,70,73,74,9,2,84,71])). % 118.83/118.74 cnf(8283,plain, % 118.83/118.74 (P1(f6(f15(f15(f4(a13)))))), % 118.83/118.74 inference(scs_inference,[],[7589,7718,5328,8088,7057,6569,6733,6423,3749,3968,131,10,17,4,7,77,18,79,80,70,73,74,9,2,84,71,83,6,85,81,5,94,16,8,14,76,12,88,87,15,11,13,100,105,91,93,3,78,75])). % 118.83/118.74 cnf(8310,plain, % 118.83/118.74 (E(f10(a12,a14),a14)), % 118.83/118.74 inference(scs_inference,[],[30,7592,10,17,4,7,77,18,80])). % 118.83/118.74 cnf(8314,plain, % 118.83/118.74 (P2(f11(a14))), % 118.83/118.74 inference(scs_inference,[],[30,7592,10,17,4,7,77,18,80,79,73])). % 118.83/118.74 cnf(8316,plain, % 118.83/118.74 (~E(f15(f15(f15(f4(a13)))),a3)), % 118.83/118.74 inference(scs_inference,[],[30,7592,8247,10,17,4,7,77,18,80,79,73,70])). % 118.83/118.74 cnf(8356,plain, % 118.83/118.74 (P1(f6(f15(f15(f15(f4(a13))))))), % 118.83/118.74 inference(scs_inference,[],[30,7592,7594,7480,8247,8283,8237,170,10,17,4,7,77,18,80,79,73,70,74,9,84,2,71,83,6,85,81,5,94,16,8,14,76,12,15,11,13,100,105,91,93,3,75])). % 118.83/118.74 cnf(8518,plain, % 118.83/118.74 (E(f10(a12,a14),f9(a13,f4(a1)))), % 118.83/118.74 inference(scs_inference,[],[8310,8314,8316,8356,1124,131,10,17,4,77,7,18,80,73,74,79,70,9,84,2,71,83,6,81,5,94,16,76,8,14,12,15,11,13,100,105,91,93,3])). % 118.83/118.74 cnf(8638,plain, % 118.83/118.74 ($false), % 118.83/118.74 inference(scs_inference,[],[46,44,1999,43,38,40,28,3818,3936,7528,7477,7603,3690,5916,255,4952,3799,3898,5555,3839,4968,7185,7653,4998,4240,7803,8518,2,9,285,356,496,506,455,1346,1088,20,22,25,21,3,24,86,129,125,120]), % 118.83/118.74 ['proof']). % 118.83/118.74 % SZS output end Proof % 118.83/118.74 % Total time :117.990000s %------------------------------------------------------------------------------