%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : RNG069+1 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n004.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:56 EDT 2024 % Result : Theorem 117.57s 117.60s % Output : CNFRefutation 117.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.10 % Problem : RNG069+1 : TPTP v8.2.0. Released v4.0.0. % 0.03/0.10 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.10/0.30 % Computer : n004.cluster.edu % 0.10/0.30 % Model : x86_64 x86_64 % 0.10/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.30 % Memory : 8042.1875MB % 0.10/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.30 % CPULimit : 300 % 0.10/0.30 % WCLimit : 300 % 0.10/0.30 % DateTime : Tue Jun 18 13:34:09 EDT 2024 % 0.10/0.30 % CPUTime : % 0.16/0.47 start to proof:theBenchmark % 117.45/117.58 %------------------------------------------- % 117.45/117.58 % File :CSE---1.7 % 117.45/117.58 % Problem :theBenchmark % 117.45/117.58 % Transform :cnf % 117.45/117.58 % Format :tptp:raw % 117.45/117.58 % Command :java -jar mcs_scs.jar %d %s % 117.45/117.58 % 117.45/117.58 % Result :Theorem 117.020000s % 117.45/117.58 % Output :CNFRefutation 117.020000s % 117.45/117.58 %------------------------------------------- % 117.45/117.59 %------------------------------------------------------------------------------ % 117.45/117.59 % File : RNG069+1 : TPTP v8.2.0. Released v4.0.0. % 117.45/117.59 % Domain : Ring Theory % 117.45/117.59 % Problem : Cauchy-Bouniakowsky-Schwarz inequality 05_16_03_04, 00 expansion % 117.45/117.59 % Version : Especial. % 117.45/117.59 % English : % 117.45/117.59 % 117.45/117.59 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 117.45/117.59 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 117.45/117.59 % Source : [Pas08] % 117.45/117.59 % Names : cauchy_05_16_03_04.00 [Pas08] % 117.45/117.59 % 117.45/117.59 % Status : Theorem % 117.45/117.59 % Rating : 0.31 v8.2.0, 0.33 v8.1.0, 0.39 v7.5.0, 0.44 v7.4.0, 0.33 v7.3.0, 0.24 v7.1.0, 0.30 v7.0.0, 0.40 v6.4.0, 0.35 v6.3.0, 0.29 v6.2.0, 0.36 v6.1.0, 0.50 v6.0.0, 0.43 v5.5.0, 0.52 v5.4.0, 0.61 v5.3.0, 0.67 v5.2.0, 0.55 v5.1.0, 0.62 v5.0.0, 0.71 v4.1.0, 0.74 v4.0.1, 0.91 v4.0.0 % 117.45/117.59 % Syntax : Number of formulae : 62 ( 11 unt; 1 def) % 117.45/117.59 % Number of atoms : 193 ( 58 equ) % 117.45/117.59 % Maximal formula atoms : 9 ( 3 avg) % 117.45/117.59 % Number of connectives : 137 ( 6 ~; 1 |; 76 &) % 117.45/117.59 % ( 1 <=>; 53 =>; 0 <=; 0 <~>) % 117.45/117.59 % Maximal formula depth : 10 ( 4 avg) % 117.45/117.59 % Maximal term depth : 5 ( 1 avg) % 117.45/117.59 % Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty) % 117.45/117.59 % Number of functors : 26 ( 26 usr; 18 con; 0-2 aty) % 117.45/117.59 % Number of variables : 71 ( 70 !; 1 ?) % 117.45/117.59 % SPC : FOF_THM_RFO_SEQ % 117.45/117.59 % 117.45/117.59 % Comments : Problem generated by the SAD system [VLP07] % 117.45/117.59 %------------------------------------------------------------------------------ % 117.45/117.59 fof(mNatSort,axiom, % 117.45/117.59 ! [W0] : % 117.45/117.59 ( aNaturalNumber0(W0) % 117.45/117.59 => $true ) ). % 117.45/117.59 % 117.45/117.59 fof(mZeroNat,axiom, % 117.45/117.59 aNaturalNumber0(sz00) ). % 117.45/117.59 % 117.45/117.59 fof(mSuccNat,axiom, % 117.45/117.59 ! [W0] : % 117.45/117.59 ( aNaturalNumber0(W0) % 117.45/117.59 => ( aNaturalNumber0(szszuzczcdt0(W0)) % 117.45/117.59 & szszuzczcdt0(W0) != sz00 ) ) ). % 117.45/117.59 % 117.45/117.59 fof(mNatExtr,axiom, % 117.45/117.59 ! [W0] : % 117.45/117.59 ( ( aNaturalNumber0(W0) % 117.45/117.59 & W0 != sz00 ) % 117.45/117.59 => ? [W1] : % 117.45/117.59 ( aNaturalNumber0(W1) % 117.45/117.59 & W0 = szszuzczcdt0(W1) ) ) ). % 117.45/117.59 % 117.45/117.59 fof(mSuccEqu,axiom, % 117.45/117.59 ! [W0,W1] : % 117.45/117.59 ( ( aNaturalNumber0(W0) % 117.45/117.59 & aNaturalNumber0(W1) ) % 117.45/117.59 => ( szszuzczcdt0(W0) = szszuzczcdt0(W1) % 117.45/117.59 => W0 = W1 ) ) ). % 117.45/117.59 % 117.45/117.59 fof(mIHOrd,axiom, % 117.45/117.59 ! [W0,W1] : % 117.45/117.59 ( ( aNaturalNumber0(W0) % 117.45/117.59 & aNaturalNumber0(W1) ) % 117.45/117.59 => ( iLess0(W0,W1) % 117.45/117.59 => $true ) ) ). % 117.45/117.59 % 117.45/117.59 fof(mIH,axiom, % 117.45/117.59 ! [W0] : % 117.45/117.59 ( aNaturalNumber0(W0) % 117.45/117.59 => iLess0(W0,szszuzczcdt0(W0)) ) ). % 117.45/117.59 % 117.45/117.59 fof(mScSort,axiom, % 117.45/117.59 ! [W0] : % 117.45/117.59 ( aScalar0(W0) % 117.45/117.59 => $true ) ). % 117.45/117.59 % 117.45/117.59 fof(mSZeroSc,axiom, % 117.45/117.59 aScalar0(sz0z00) ). % 117.45/117.59 % 117.45/117.59 fof(mSumSc,axiom, % 117.45/117.59 ! [W0,W1] : % 117.45/117.59 ( ( aScalar0(W0) % 117.45/117.59 & aScalar0(W1) ) % 117.45/117.59 => aScalar0(sdtpldt0(W0,W1)) ) ). % 117.45/117.59 % 117.45/117.59 fof(mMulSc,axiom, % 117.45/117.59 ! [W0,W1] : % 117.45/117.59 ( ( aScalar0(W0) % 117.45/117.59 & aScalar0(W1) ) % 117.45/117.59 => aScalar0(sdtasdt0(W0,W1)) ) ). % 117.45/117.59 % 117.45/117.59 fof(mNegSc,axiom, % 117.45/117.59 ! [W0] : % 117.45/117.59 ( aScalar0(W0) % 117.45/117.59 => aScalar0(smndt0(W0)) ) ). % 117.45/117.59 % 117.45/117.59 fof(mScZero,axiom, % 117.45/117.59 ! [W0] : % 117.45/117.59 ( aScalar0(W0) % 117.45/117.59 => ( sdtpldt0(W0,sz0z00) = W0 % 117.45/117.59 & sdtpldt0(sz0z00,W0) = W0 % 117.45/117.59 & sdtasdt0(W0,sz0z00) = sz0z00 % 117.45/117.59 & sdtasdt0(sz0z00,W0) = sz0z00 % 117.45/117.59 & sdtpldt0(W0,smndt0(W0)) = sz0z00 % 117.45/117.59 & sdtpldt0(smndt0(W0),W0) = sz0z00 % 117.45/117.59 & smndt0(smndt0(W0)) = W0 % 117.45/117.59 & smndt0(sz0z00) = sz0z00 ) ) ). % 117.45/117.59 % 117.45/117.59 fof(mArith,axiom, % 117.45/117.59 ! [W0,W1,W2] : % 117.45/117.59 ( ( aScalar0(W0) % 117.45/117.59 & aScalar0(W1) % 117.45/117.59 & aScalar0(W2) ) % 117.45/117.59 => ( sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) % 117.45/117.59 & sdtpldt0(W0,W1) = sdtpldt0(W1,W0) % 117.45/117.59 & sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) % 117.45/117.59 & sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ) ). % 117.45/117.59 % 117.45/117.59 fof(mDistr,axiom, % 117.45/117.59 ! [W0,W1,W2] : % 117.45/117.59 ( ( aScalar0(W0) % 117.45/117.59 & aScalar0(W1) % 117.45/117.59 & aScalar0(W2) ) % 117.45/117.59 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 117.45/117.59 & sdtasdt0(sdtpldt0(W0,W1),W2) = sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W1,W2)) ) ) ). % 117.45/117.59 % 117.45/117.59 fof(mDistr2,axiom, % 117.45/117.59 ! [W0,W1,W2,W3] : % 117.45/117.59 ( ( aScalar0(W0) % 117.45/117.59 & aScalar0(W1) % 117.45/117.59 & aScalar0(W2) % 117.45/117.59 & aScalar0(W3) ) % 117.45/117.59 => sdtasdt0(sdtpldt0(W0,W1),sdtpldt0(W2,W3)) = sdtpldt0(sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W0,W3)),sdtpldt0(sdtasdt0(W1,W2),sdtasdt0(W1,W3))) ) ). % 117.45/117.59 % 117.45/117.59 fof(mMNeg,axiom, % 117.45/117.59 ! [W0,W1] : % 117.45/117.59 ( ( aScalar0(W0) % 117.45/117.59 & aScalar0(W1) ) % 117.45/117.59 => ( sdtasdt0(W0,smndt0(W1)) = smndt0(sdtasdt0(W0,W1)) % 117.45/117.59 & sdtasdt0(smndt0(W0),W1) = smndt0(sdtasdt0(W0,W1)) ) ) ). % 117.45/117.59 % 117.45/117.59 fof(mMDNeg,axiom, % 117.45/117.59 ! [W0,W1] : % 117.45/117.59 ( ( aScalar0(W0) % 117.45/117.59 & aScalar0(W1) ) % 117.45/117.59 => sdtasdt0(smndt0(W0),smndt0(W1)) = sdtasdt0(W0,W1) ) ). % 117.45/117.59 % 117.45/117.59 fof(mLess,axiom, % 117.45/117.59 ! [W0,W1] : % 117.45/117.59 ( ( aScalar0(W0) % 117.45/117.59 & aScalar0(W1) ) % 117.45/117.59 => ( sdtlseqdt0(W0,W1) % 117.45/117.59 => $true ) ) ). % 117.45/117.59 % 117.45/117.59 fof(mLERef,axiom, % 117.45/117.59 ! [W0] : % 117.45/117.59 ( aScalar0(W0) % 117.45/117.59 => sdtlseqdt0(W0,W0) ) ). % 117.45/117.59 % 117.45/117.59 fof(mLEASm,axiom, % 117.45/117.59 ! [W0,W1] : % 117.45/117.59 ( ( aScalar0(W0) % 117.45/117.59 & aScalar0(W1) ) % 117.45/117.59 => ( ( sdtlseqdt0(W0,W1) % 117.45/117.59 & sdtlseqdt0(W1,W0) ) % 117.45/117.59 => W0 = W1 ) ) ). % 117.45/117.59 % 117.45/117.59 fof(mLETrn,axiom, % 117.45/117.59 ! [W0,W1,W2] : % 117.45/117.59 ( ( aScalar0(W0) % 117.45/117.59 & aScalar0(W1) % 117.45/117.59 & aScalar0(W2) ) % 117.45/117.59 => ( ( sdtlseqdt0(W0,W1) % 117.45/117.59 & sdtlseqdt0(W1,W2) ) % 117.45/117.59 => sdtlseqdt0(W0,W2) ) ) ). % 117.45/117.59 % 117.45/117.59 fof(mLEMon,axiom, % 117.45/117.59 ! [W0,W1,W2,W3] : % 117.45/117.59 ( ( aScalar0(W0) % 117.45/117.59 & aScalar0(W1) % 117.45/117.59 & aScalar0(W2) % 117.45/117.59 & aScalar0(W3) ) % 117.45/117.59 => ( ( sdtlseqdt0(W0,W1) % 117.45/117.59 & sdtlseqdt0(W2,W3) ) % 117.45/117.59 => sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W3)) ) ) ). % 117.45/117.59 % 117.45/117.59 fof(mLEMonM,axiom, % 117.45/117.59 ! [W0,W1,W2,W3] : % 117.45/117.59 ( ( aScalar0(W0) % 117.45/117.59 & aScalar0(W1) % 117.45/117.59 & aScalar0(W2) % 117.45/117.59 & aScalar0(W3) ) % 117.45/117.59 => ( ( sdtlseqdt0(W0,W1) % 117.45/117.59 & sdtlseqdt0(sz0z00,W2) % 117.45/117.59 & sdtlseqdt0(W2,W3) ) % 117.45/117.59 => sdtlseqdt0(sdtasdt0(W0,W2),sdtasdt0(W1,W3)) ) ) ). % 117.45/117.59 % 117.45/117.59 fof(mLETot,axiom, % 117.45/117.59 ! [W0,W1] : % 117.45/117.59 ( ( aScalar0(W0) % 117.45/117.59 & aScalar0(W1) ) % 117.45/117.59 => ( sdtlseqdt0(W0,W1) % 117.45/117.59 | sdtlseqdt0(W1,W0) ) ) ). % 117.45/117.59 % 117.45/117.59 fof(mPosMon,axiom, % 117.45/117.59 ! [W0,W1] : % 117.45/117.59 ( ( aScalar0(W0) % 117.45/117.59 & aScalar0(W1) ) % 117.45/117.59 => ( ( sdtlseqdt0(sz0z00,W0) % 117.45/117.59 & sdtlseqdt0(sz0z00,W1) ) % 117.45/117.59 => ( sdtlseqdt0(sz0z00,sdtpldt0(W0,W1)) % 117.45/117.59 & sdtlseqdt0(sz0z00,sdtasdt0(W0,W1)) ) ) ) ). % 117.45/117.59 % 117.45/117.59 fof(mSqPos,axiom, % 117.45/117.59 ! [W0] : % 117.45/117.59 ( aScalar0(W0) % 117.45/117.59 => sdtlseqdt0(sz0z00,sdtasdt0(W0,W0)) ) ). % 117.45/117.59 % 117.45/117.59 fof(mSqrt,axiom, % 117.45/117.59 ! [W0,W1] : % 117.45/117.59 ( ( aScalar0(W0) % 117.45/117.59 & aScalar0(W1) ) % 117.45/117.59 => ( ( sdtlseqdt0(sz0z00,W0) % 117.45/117.59 & sdtlseqdt0(sz0z00,W1) % 117.45/117.59 & sdtasdt0(W0,W0) = sdtasdt0(W1,W1) ) % 117.45/117.59 => W0 = W1 ) ) ). % 117.45/117.59 % 117.45/117.59 fof(mVcSort,axiom, % 117.45/117.59 ! [W0] : % 117.45/117.59 ( aVector0(W0) % 117.45/117.59 => $true ) ). % 117.45/117.59 % 117.45/117.59 fof(mDimNat,axiom, % 117.45/117.59 ! [W0] : % 117.45/117.59 ( aVector0(W0) % 117.45/117.59 => aNaturalNumber0(aDimensionOf0(W0)) ) ). % 117.45/117.59 % 117.45/117.59 fof(mElmSc,axiom, % 117.45/117.59 ! [W0,W1] : % 117.45/117.59 ( ( aVector0(W0) % 117.45/117.59 & aNaturalNumber0(W1) ) % 117.45/117.59 => aScalar0(sdtlbdtrb0(W0,W1)) ) ). % 117.45/117.59 % 117.45/117.59 fof(mDefInit,definition, % 117.45/117.59 ! [W0] : % 117.45/117.59 ( aVector0(W0) % 117.45/117.59 => ( aDimensionOf0(W0) != sz00 % 117.45/117.59 => ! [W1] : % 117.45/117.59 ( W1 = sziznziztdt0(W0) % 117.45/117.59 <=> ( aVector0(W1) % 117.45/117.59 & szszuzczcdt0(aDimensionOf0(W1)) = aDimensionOf0(W0) % 117.45/117.59 & ! [W2] : % 117.45/117.59 ( aNaturalNumber0(W2) % 117.45/117.59 => sdtlbdtrb0(W1,W2) = sdtlbdtrb0(W0,W2) ) ) ) ) ) ). % 117.45/117.59 % 117.45/117.59 fof(mEqInit,axiom, % 117.45/117.59 ! [W0,W1] : % 117.45/117.59 ( ( aVector0(W0) % 117.45/117.59 & aVector0(W1) ) % 117.45/117.59 => ( ( aDimensionOf0(W0) = aDimensionOf0(W1) % 117.45/117.59 & aDimensionOf0(W1) != sz00 ) % 117.45/117.59 => aDimensionOf0(sziznziztdt0(W0)) = aDimensionOf0(sziznziztdt0(W1)) ) ) ). % 117.45/117.59 % 117.45/117.59 fof(mScPr,axiom, % 117.45/117.59 ! [W0,W1] : % 117.45/117.59 ( ( aVector0(W0) % 117.45/117.59 & aVector0(W1) ) % 117.45/117.59 => ( aDimensionOf0(W0) = aDimensionOf0(W1) % 117.45/117.59 => aScalar0(sdtasasdt0(W0,W1)) ) ) ). % 117.45/117.59 % 117.45/117.59 fof(mDefSPZ,axiom, % 117.45/117.59 ! [W0,W1] : % 117.45/117.59 ( ( aVector0(W0) % 117.45/117.59 & aVector0(W1) ) % 117.45/117.59 => ( ( aDimensionOf0(W0) = aDimensionOf0(W1) % 117.45/117.59 & aDimensionOf0(W1) = sz00 ) % 117.45/117.59 => sdtasasdt0(W0,W1) = sz0z00 ) ) ). % 117.45/117.59 % 117.45/117.60 fof(mDefSPN,axiom, % 117.45/117.60 ! [W0,W1] : % 117.45/117.60 ( ( aVector0(W0) % 117.45/117.60 & aVector0(W1) ) % 117.45/117.60 => ( ( aDimensionOf0(W0) = aDimensionOf0(W1) % 117.45/117.60 & aDimensionOf0(W1) != sz00 ) % 117.45/117.60 => sdtasasdt0(W0,W1) = sdtpldt0(sdtasasdt0(sziznziztdt0(W0),sziznziztdt0(W1)),sdtasdt0(sdtlbdtrb0(W0,aDimensionOf0(W0)),sdtlbdtrb0(W1,aDimensionOf0(W1)))) ) ) ). % 117.45/117.60 % 117.45/117.60 fof(mScSqPos,axiom, % 117.45/117.60 ! [W0] : % 117.45/117.60 ( aVector0(W0) % 117.45/117.60 => sdtlseqdt0(sz0z00,sdtasasdt0(W0,W0)) ) ). % 117.45/117.60 % 117.57/117.60 fof(m__1678,hypothesis, % 117.57/117.60 ( aVector0(xs) % 117.57/117.60 & aVector0(xt) ) ). % 117.57/117.60 % 117.57/117.60 fof(m__1652,hypothesis, % 117.57/117.60 ! [W0,W1] : % 117.57/117.60 ( ( aVector0(W0) % 117.57/117.60 & aVector0(W1) ) % 117.57/117.60 => ( aDimensionOf0(W0) = aDimensionOf0(W1) % 117.57/117.60 => ( iLess0(aDimensionOf0(W0),aDimensionOf0(xs)) % 117.57/117.60 => sdtlseqdt0(sdtasdt0(sdtasasdt0(W0,W1),sdtasasdt0(W0,W1)),sdtasdt0(sdtasasdt0(W0,W0),sdtasasdt0(W1,W1))) ) ) ) ). % 117.57/117.60 % 117.57/117.60 fof(m__1678_01,hypothesis, % 117.57/117.60 aDimensionOf0(xs) = aDimensionOf0(xt) ). % 117.57/117.60 % 117.57/117.60 fof(m__1692,hypothesis, % 117.57/117.60 aDimensionOf0(xs) != sz00 ). % 117.57/117.60 % 117.57/117.60 fof(m__1709,hypothesis, % 117.57/117.60 ( aVector0(xp) % 117.57/117.60 & xp = sziznziztdt0(xs) ) ). % 117.57/117.60 % 117.57/117.60 fof(m__1726,hypothesis, % 117.57/117.60 ( aVector0(xq) % 117.57/117.60 & xq = sziznziztdt0(xt) ) ). % 117.57/117.60 % 117.57/117.60 fof(m__1746,hypothesis, % 117.57/117.60 ( aScalar0(xA) % 117.57/117.60 & xA = sdtlbdtrb0(xs,aDimensionOf0(xs)) ) ). % 117.57/117.60 % 117.57/117.60 fof(m__1766,hypothesis, % 117.57/117.60 ( aScalar0(xB) % 117.57/117.60 & xB = sdtlbdtrb0(xt,aDimensionOf0(xt)) ) ). % 117.57/117.60 % 117.57/117.60 fof(m__1783,hypothesis, % 117.57/117.60 ( aScalar0(xC) % 117.57/117.60 & xC = sdtasasdt0(xp,xp) ) ). % 117.57/117.60 % 117.57/117.60 fof(m__1800,hypothesis, % 117.57/117.60 ( aScalar0(xD) % 117.57/117.60 & xD = sdtasasdt0(xq,xq) ) ). % 117.57/117.60 % 117.57/117.60 fof(m__1820,hypothesis, % 117.57/117.60 ( aScalar0(xE) % 117.57/117.60 & xE = sdtasasdt0(xp,xq) ) ). % 117.57/117.60 % 117.57/117.60 fof(m__1837,hypothesis, % 117.57/117.60 ( aScalar0(xF) % 117.57/117.60 & xF = sdtasdt0(xA,xA) ) ). % 117.57/117.60 % 117.57/117.60 fof(m__1854,hypothesis, % 117.57/117.60 ( aScalar0(xG) % 117.57/117.60 & xG = sdtasdt0(xB,xB) ) ). % 117.57/117.60 % 117.57/117.60 fof(m__1873,hypothesis, % 117.57/117.60 ( aScalar0(xH) % 117.57/117.60 & xH = sdtasdt0(xA,xB) ) ). % 117.57/117.60 % 117.57/117.60 fof(m__1892,hypothesis, % 117.57/117.60 ( aScalar0(xR) % 117.57/117.60 & xR = sdtasdt0(xC,xG) ) ). % 117.57/117.60 % 117.57/117.60 fof(m__1911,hypothesis, % 117.57/117.60 ( aScalar0(xP) % 117.57/117.60 & xP = sdtasdt0(xE,xH) ) ). % 117.57/117.60 % 117.57/117.60 fof(m__1930,hypothesis, % 117.57/117.60 ( aScalar0(xS) % 117.57/117.60 & xS = sdtasdt0(xF,xD) ) ). % 117.57/117.60 % 117.57/117.60 fof(m__1949,hypothesis, % 117.57/117.60 ( aScalar0(xN) % 117.57/117.60 & xN = sdtasdt0(xR,xS) ) ). % 117.57/117.60 % 117.57/117.60 fof(m__1967,hypothesis, % 117.57/117.60 sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)) ). % 117.57/117.60 % 117.57/117.60 fof(m__2004,hypothesis, % 117.57/117.60 sdtlseqdt0(sdtasdt0(xP,xP),xN) ). % 117.57/117.60 % 117.57/117.60 fof(m__2104,hypothesis, % 117.57/117.60 sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS))) ). % 117.57/117.60 % 117.57/117.60 fof(m__2463,hypothesis, % 117.57/117.60 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)) ). % 117.57/117.60 % 117.57/117.60 fof(m__2510,hypothesis, % 117.57/117.60 sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),xN),sdtasdt0(xS,xS)),xN) = sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),xN),sdtpldt0(sdtasdt0(xS,xS),xN)) ). % 117.57/117.60 % 117.57/117.60 fof(m__2580,hypothesis, % 117.57/117.60 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)))) ). % 117.57/117.60 % 117.57/117.60 fof(m__,conjecture, % 117.57/117.60 sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS))) ). % 117.57/117.60 % 117.57/117.60 %------------------------------------------------------------------------------ % 117.57/117.60 %------------------------------------------- % 117.57/117.60 % Proof found % 117.57/117.60 % SZS status Theorem for theBenchmark % 117.57/117.60 % SZS output start Proof % 117.57/117.60 %ClaNum:116(EqnAxiom:25) % 117.57/117.60 %VarNum:309(SingletonVarNum:96) % 117.57/117.60 %MaxLitNum:8 % 117.57/117.60 %MaxfuncDepth:4 % 117.57/117.60 %SharedTerms:102 % 117.57/117.60 %goalClause: 66 % 117.57/117.60 %singleGoalClaCount:1 % 117.57/117.60 [28]P1(a3) % 117.57/117.60 [29]P2(a12) % 117.57/117.60 [30]P2(a14) % 117.57/117.60 [31]P2(a16) % 117.57/117.60 [32]P2(a17) % 117.57/117.60 [33]P2(a18) % 117.57/117.60 [34]P2(a19) % 117.57/117.60 [35]P2(a20) % 117.57/117.60 [36]P2(a21) % 117.57/117.60 [37]P2(a22) % 117.57/117.60 [38]P2(a23) % 117.57/117.60 [39]P2(a24) % 117.57/117.60 [40]P2(a26) % 117.57/117.60 [41]P2(a25) % 117.57/117.60 [42]P3(a1) % 117.57/117.60 [43]P3(a28) % 117.57/117.60 [44]P3(a13) % 117.57/117.60 [45]P3(a27) % 117.57/117.60 [26]E(f2(a1),a13) % 117.57/117.60 [27]E(f2(a28),a27) % 117.57/117.60 [46]E(f4(a28),f4(a1)) % 117.57/117.60 [47]E(f5(a13,a13),a17) % 117.57/117.60 [48]E(f5(a27,a27),a18) % 117.57/117.60 [49]E(f5(a13,a27),a19) % 117.57/117.60 [50]E(f8(a14,a14),a20) % 117.57/117.60 [51]E(f8(a16,a16),a21) % 117.57/117.60 [52]E(f8(a14,a16),a22) % 117.57/117.60 [53]E(f8(a17,a21),a23) % 117.57/117.60 [54]E(f8(a19,a22),a24) % 117.57/117.60 [55]E(f8(a20,a18),a26) % 117.57/117.60 [56]E(f8(a23,a26),a25) % 117.57/117.60 [59]P4(f8(a24,a24),a25) % 117.57/117.60 [60]P4(f8(a19,a19),f8(a17,a18)) % 117.57/117.60 [65]~E(f4(a1),a3) % 117.57/117.60 [57]E(f9(a1,f4(a1)),a14) % 117.57/117.60 [58]E(f9(a28,f4(a28)),a16) % 117.57/117.60 [61]P4(f10(f8(a24,a24),f8(a24,a24)),f10(f8(a23,a23),f8(a26,a26))) % 117.57/117.60 [66]~P4(f8(f10(a24,a24),f10(a24,a24)),f8(f10(a23,a26),f10(a23,a26))) % 117.57/117.60 [62]E(f10(f10(f10(f8(a23,a23),a25),f8(a26,a26)),a25),f10(f10(f8(a23,a23),a25),f10(f8(a26,a26),a25))) % 117.57/117.60 [63]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)))) % 117.57/117.60 [64]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)) % 117.57/117.60 [79]~P2(x791)+P4(x791,x791) % 117.57/117.60 [67]~P2(x671)+E(f11(a12),a12) % 117.57/117.60 [68]~P1(x681)+~E(f15(x681),a3) % 117.57/117.60 [69]~P1(x691)+P1(f15(x691)) % 117.57/117.60 [70]~P3(x701)+P1(f4(x701)) % 117.57/117.60 [71]~P2(x711)+P2(f11(x711)) % 117.57/117.60 [74]~P2(x741)+E(f8(x741,a12),a12) % 117.57/117.60 [75]~P2(x751)+E(f8(a12,x751),a12) % 117.57/117.60 [77]~P2(x771)+E(f10(x771,a12),x771) % 117.57/117.60 [78]~P2(x781)+E(f10(a12,x781),x781) % 117.57/117.60 [83]~P1(x831)+P5(x831,f15(x831)) % 117.57/117.60 [90]~P2(x901)+P4(a12,f8(x901,x901)) % 117.57/117.60 [91]~P3(x911)+P4(a12,f5(x911,x911)) % 117.57/117.60 [72]~P2(x721)+E(f11(f11(x721)),x721) % 117.57/117.60 [81]~P2(x811)+E(f10(x811,f11(x811)),a12) % 117.57/117.60 [82]~P2(x821)+E(f10(f11(x821),x821),a12) % 117.57/117.60 [73]~P1(x731)+E(x731,a3)+P1(f6(x731)) % 117.57/117.60 [76]~P1(x761)+E(x761,a3)+E(f15(f6(x761)),x761) % 117.57/117.60 [87]~P2(x872)+~P2(x871)+P2(f10(x871,x872)) % 117.57/117.60 [88]~P2(x882)+~P2(x881)+P2(f8(x881,x882)) % 117.57/117.60 [89]~P1(x892)+~P3(x891)+P2(f9(x891,x892)) % 117.57/117.60 [96]~P2(x962)+~P2(x961)+E(f8(f11(x961),f11(x962)),f8(x961,x962)) % 117.57/117.60 [100]~P2(x1002)+~P2(x1001)+E(f11(f8(x1001,x1002)),f8(x1001,f11(x1002))) % 117.57/117.60 [101]~P2(x1012)+~P2(x1011)+E(f11(f8(x1011,x1012)),f8(f11(x1011),x1012)) % 117.57/117.60 [86]P4(x862,x861)+~P2(x861)+~P2(x862)+P4(x861,x862) % 117.57/117.60 [80]~P3(x801)+P3(x802)+~E(x802,f2(x801))+E(f4(x801),a3) % 117.57/117.60 [84]~P1(x842)+~P1(x841)+E(x841,x842)+~E(f15(x841),f15(x842)) % 117.57/117.60 [98]~P3(x982)+~P3(x981)+~E(f4(x981),f4(x982))+P2(f5(x981,x982)) % 117.57/117.60 [85]~P3(x851)+~E(x852,f2(x851))+E(f4(x851),a3)+E(f15(f4(x852)),f4(x851)) % 117.57/117.60 [93]~P2(x932)+~P2(x931)+~P2(x933)+E(f10(x931,x932),f10(x932,x931)) % 117.57/117.60 [94]~P2(x942)+~P2(x941)+~P2(x943)+E(f8(x941,x942),f8(x942,x941)) % 117.57/117.60 [106]~P2(x1063)+~P2(x1062)+~P2(x1061)+E(f10(f10(x1061,x1062),x1063),f10(x1061,f10(x1062,x1063))) % 117.57/117.60 [107]~P2(x1073)+~P2(x1072)+~P2(x1071)+E(f8(f8(x1071,x1072),x1073),f8(x1071,f8(x1072,x1073))) % 117.57/117.60 [109]~P2(x1093)+~P2(x1092)+~P2(x1091)+E(f10(f8(x1091,x1092),f8(x1091,x1093)),f8(x1091,f10(x1092,x1093))) % 117.57/117.60 [110]~P2(x1102)+~P2(x1103)+~P2(x1101)+E(f10(f8(x1101,x1102),f8(x1103,x1102)),f8(f10(x1101,x1103),x1102)) % 117.57/117.60 [99]~P2(x992)+~P2(x991)+~P4(x992,x991)+~P4(x991,x992)+E(x991,x992) % 117.57/117.60 [92]~P3(x922)+~P3(x921)+~E(f4(x921),f4(x922))+~E(f4(x922),a3)+E(f5(x921,x922),a12) % 117.57/117.60 [104]~P2(x1042)+~P2(x1041)+~P4(a12,x1042)+~P4(a12,x1041)+P4(a12,f10(x1041,x1042)) % 117.57/117.60 [105]~P2(x1052)+~P2(x1051)+~P4(a12,x1052)+~P4(a12,x1051)+P4(a12,f8(x1051,x1052)) % 117.57/117.60 [95]~P3(x951)+~P3(x952)+~E(f4(x952),f4(x951))+E(f4(x951),a3)+E(f4(f2(x952)),f4(f2(x951))) % 117.57/117.60 [115]~P3(x1152)+~P3(x1151)+~E(f4(x1151),f4(x1152))+~P5(f4(x1151),f4(a1))+P4(f8(f5(x1151,x1152),f5(x1151,x1152)),f8(f5(x1151,x1151),f5(x1152,x1152))) % 117.57/117.60 [114]~P3(x1141)+~P3(x1142)+~E(f4(x1142),f4(x1141))+E(f4(x1141),a3)+E(f10(f5(f2(x1142),f2(x1141)),f8(f9(x1142,f4(x1142)),f9(x1141,f4(x1141)))),f5(x1142,x1141)) % 117.57/117.60 [97]~P1(x973)+~P3(x971)+~E(x972,f2(x971))+E(f9(x972,x973),f9(x971,x973))+E(f4(x971),a3) % 117.57/117.60 [116]~P2(x1163)+~P2(x1162)+~P2(x1164)+~P2(x1161)+E(f10(f10(f8(x1161,x1162),f8(x1161,x1163)),f10(f8(x1164,x1162),f8(x1164,x1163))),f8(f10(x1161,x1164),f10(x1162,x1163))) % 117.57/117.60 [108]~P2(x1082)+~P2(x1081)+E(x1081,x1082)+~E(f8(x1081,x1081),f8(x1082,x1082))+~P4(a12,x1082)+~P4(a12,x1081) % 117.57/117.60 [102]~P3(x1021)+~P3(x1022)+E(x1021,f2(x1022))+E(f4(x1022),a3)+P1(f7(x1022,x1021))+~E(f15(f4(x1021)),f4(x1022)) % 117.57/117.60 [113]~P3(x1132)+~P3(x1131)+E(x1131,f2(x1132))+E(f4(x1132),a3)+~E(f15(f4(x1131)),f4(x1132))+~E(f9(x1131,f7(x1132,x1131)),f9(x1132,f7(x1132,x1131))) % 117.57/117.60 [103]~P2(x1032)+~P2(x1031)+~P4(x1033,x1032)+~P4(x1031,x1033)+P4(x1031,x1032)+~P2(x1033) % 117.57/117.60 [111]~P2(x1114)+~P2(x1112)+~P2(x1113)+~P2(x1111)+~P4(x1112,x1114)+~P4(x1111,x1113)+P4(f10(x1111,x1112),f10(x1113,x1114)) % 117.57/117.60 [112]~P2(x1124)+~P2(x1122)+~P2(x1123)+~P2(x1121)+~P4(x1122,x1124)+~P4(x1121,x1123)+~P4(a12,x1122)+P4(f8(x1121,x1122),f8(x1123,x1124)) % 117.57/117.60 %EqnAxiom % 117.57/117.60 [1]E(x11,x11) % 117.57/117.60 [2]E(x22,x21)+~E(x21,x22) % 117.57/117.60 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 117.57/117.60 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 117.57/117.60 [5]~E(x51,x52)+E(f8(x51,x53),f8(x52,x53)) % 117.57/117.60 [6]~E(x61,x62)+E(f8(x63,x61),f8(x63,x62)) % 117.57/117.60 [7]~E(x71,x72)+E(f4(x71),f4(x72)) % 117.57/117.60 [8]~E(x81,x82)+E(f11(x81),f11(x82)) % 117.57/117.60 [9]~E(x91,x92)+E(f5(x91,x93),f5(x92,x93)) % 117.57/117.60 [10]~E(x101,x102)+E(f5(x103,x101),f5(x103,x102)) % 117.57/117.60 [11]~E(x111,x112)+E(f10(x111,x113),f10(x112,x113)) % 117.57/117.60 [12]~E(x121,x122)+E(f10(x123,x121),f10(x123,x122)) % 117.57/117.60 [13]~E(x131,x132)+E(f15(x131),f15(x132)) % 117.57/117.60 [14]~E(x141,x142)+E(f9(x141,x143),f9(x142,x143)) % 117.57/117.60 [15]~E(x151,x152)+E(f9(x153,x151),f9(x153,x152)) % 117.57/117.60 [16]~E(x161,x162)+E(f7(x161,x163),f7(x162,x163)) % 117.57/117.60 [17]~E(x171,x172)+E(f7(x173,x171),f7(x173,x172)) % 117.57/117.60 [18]~E(x181,x182)+E(f6(x181),f6(x182)) % 117.57/117.60 [19]~P1(x191)+P1(x192)+~E(x191,x192) % 117.57/117.60 [20]~P2(x201)+P2(x202)+~E(x201,x202) % 117.57/117.60 [21]P4(x212,x213)+~E(x211,x212)+~P4(x211,x213) % 117.57/117.60 [22]P4(x223,x222)+~E(x221,x222)+~P4(x223,x221) % 117.57/117.60 [23]~P3(x231)+P3(x232)+~E(x231,x232) % 117.57/117.60 [24]P5(x242,x243)+~E(x241,x242)+~P5(x241,x243) % 117.57/117.60 [25]P5(x253,x252)+~E(x251,x252)+~P5(x253,x251) % 117.57/117.60 % 117.57/117.60 %------------------------------------------- % 117.57/117.62 cnf(117,plain, % 117.57/117.62 (~P3(x1171)+P3(f2(x1171))+E(f4(x1171),a3)), % 117.57/117.62 inference(equality_inference,[],[80])). % 117.57/117.62 cnf(119,plain, % 117.57/117.62 (~P3(x1191)+E(f4(x1191),a3)+E(f15(f4(f2(x1191))),f4(x1191))), % 117.57/117.62 inference(equality_inference,[],[85])). % 117.57/117.62 cnf(121,plain, % 117.57/117.62 (~P1(x1211)+~P3(x1212)+E(f9(f2(x1212),x1211),f9(x1212,x1211))+E(f4(x1212),a3)), % 117.57/117.62 inference(equality_inference,[],[97])). % 117.57/117.62 cnf(122,plain, % 117.57/117.62 (~P3(x1221)+~P3(x1221)+P2(f5(x1221,x1221))), % 117.57/117.62 inference(equality_inference,[],[98])). % 117.57/117.62 cnf(124,plain, % 117.57/117.62 (~P3(x1241)+~P3(x1241)+E(f4(x1241),a3)+E(f10(f5(f2(x1241),f2(x1241)),f8(f9(x1241,f4(x1241)),f9(x1241,f4(x1241)))),f5(x1241,x1241))), % 117.57/117.62 inference(equality_inference,[],[114])). % 117.57/117.62 cnf(125,plain, % 117.57/117.62 (~P3(x1251)+~P3(x1251)+~P5(f4(x1251),f4(a1))+P4(f8(f5(x1251,x1251),f5(x1251,x1251)),f8(f5(x1251,x1251),f5(x1251,x1251)))), % 117.57/117.62 inference(equality_inference,[],[115])). % 117.57/117.62 cnf(126,plain, % 117.57/117.62 (E(f4(a1),f4(a28))), % 117.57/117.62 inference(scs_inference,[],[46,2])). % 117.57/117.62 cnf(127,plain, % 117.57/117.62 (P3(f2(a1))), % 117.57/117.62 inference(scs_inference,[],[46,42,65,2,117])). % 117.57/117.62 cnf(129,plain, % 117.57/117.62 (E(f15(f4(f2(a1))),f4(a1))), % 117.57/117.62 inference(scs_inference,[],[46,42,65,2,117,119])). % 117.57/117.62 cnf(131,plain, % 117.57/117.62 (P4(a12,a12)), % 117.57/117.62 inference(scs_inference,[],[29,46,42,65,2,117,119,86])). % 117.57/117.62 cnf(133,plain, % 117.57/117.62 (E(f9(f2(a1),a3),f9(a1,a3))), % 117.57/117.62 inference(scs_inference,[],[29,46,28,42,65,2,117,119,86,121])). % 117.57/117.62 cnf(135,plain, % 117.57/117.62 (E(f10(f5(f2(a1),f2(a1)),f8(f9(a1,f4(a1)),f9(a1,f4(a1)))),f5(a1,a1))), % 117.57/117.62 inference(scs_inference,[],[29,46,28,42,65,2,117,119,86,121,124])). % 117.57/117.62 cnf(137,plain, % 117.57/117.62 (E(f4(f2(a28)),f4(f2(a1)))), % 117.57/117.62 inference(scs_inference,[],[29,46,28,42,43,65,2,117,119,86,121,124,95])). % 117.57/117.62 cnf(139,plain, % 117.57/117.62 (P4(f8(a12,a12),f8(a12,a12))), % 117.57/117.62 inference(scs_inference,[],[29,46,28,42,43,65,2,117,119,86,121,124,95,112])). % 117.57/117.62 cnf(146,plain, % 117.57/117.62 (E(f11(a12),a12)), % 117.57/117.62 inference(scs_inference,[],[30,67])). % 117.57/117.62 cnf(149,plain, % 117.57/117.62 (E(a13,f2(a1))), % 117.57/117.62 inference(scs_inference,[],[26,2])). % 117.57/117.62 cnf(150,plain, % 117.57/117.62 (E(f15(f4(a13)),f4(a1))), % 117.57/117.62 inference(scs_inference,[],[26,42,65,2,85])). % 117.57/117.62 cnf(152,plain, % 117.57/117.62 (P4(a14,a14)), % 117.57/117.62 inference(scs_inference,[],[26,30,42,65,2,85,86])). % 117.57/117.62 cnf(154,plain, % 117.57/117.62 (E(f9(a13,a3),f9(a1,a3))), % 117.57/117.62 inference(scs_inference,[],[26,30,28,42,65,2,85,86,97])). % 117.57/117.62 cnf(164,plain, % 117.57/117.62 (P2(f5(a13,a13))), % 117.57/117.62 inference(scs_inference,[],[32,47,2,20])). % 117.57/117.62 cnf(173,plain, % 117.57/117.62 (P2(f5(a13,a27))), % 117.57/117.62 inference(scs_inference,[],[34,49,2,20])). % 117.57/117.62 cnf(174,plain, % 117.57/117.62 (P4(f5(a13,a13),f5(a13,a13))), % 117.57/117.62 inference(scs_inference,[],[164,34,49,2,20,86])). % 117.57/117.62 cnf(177,plain, % 117.57/117.62 (P4(a17,f5(a13,a13))), % 117.57/117.62 inference(scs_inference,[],[131,164,34,49,47,2,20,86,22,21])). % 117.57/117.62 cnf(186,plain, % 117.57/117.62 (P2(f8(a16,a16))), % 117.57/117.62 inference(scs_inference,[],[36,51,2,20])). % 117.57/117.62 cnf(188,plain, % 117.57/117.62 (P4(f5(a13,a27),f5(a13,a27))), % 117.57/117.62 inference(scs_inference,[],[174,173,36,51,47,2,20,22,86])). % 117.57/117.62 cnf(190,plain, % 117.57/117.62 (P4(x1901,a14)+~E(a14,x1901)), % 117.57/117.62 inference(scs_inference,[],[174,152,173,36,51,47,2,20,22,86,21])). % 117.57/117.62 cnf(196,plain, % 117.57/117.62 (P2(f8(a17,a21))), % 117.57/117.62 inference(scs_inference,[],[38,53,2,20])). % 117.57/117.62 cnf(198,plain, % 117.57/117.62 (P4(f5(a13,a27),a19)), % 117.57/117.62 inference(scs_inference,[],[188,38,53,49,2,20,21,22])). % 117.57/117.62 cnf(199,plain, % 117.57/117.62 (P4(f8(a16,a16),f8(a16,a16))), % 117.57/117.62 inference(scs_inference,[],[188,186,38,53,49,2,20,21,22,86])). % 117.57/117.62 cnf(207,plain, % 117.57/117.62 (P2(f8(a20,a18))), % 117.57/117.62 inference(scs_inference,[],[40,55,2,20])). % 117.57/117.62 cnf(208,plain, % 117.57/117.62 (P4(a21,f8(a16,a16))), % 117.57/117.62 inference(scs_inference,[],[199,40,55,51,2,20,21])). % 117.57/117.62 cnf(210,plain, % 117.57/117.62 (P4(f8(a17,a21),f8(a17,a21))), % 117.57/117.62 inference(scs_inference,[],[199,196,40,55,51,2,20,21,22,86])). % 117.57/117.62 cnf(218,plain, % 117.57/117.62 (E(a12,f11(a12))), % 117.57/117.62 inference(scs_inference,[],[146,2])). % 117.57/117.62 cnf(219,plain, % 117.57/117.62 (P2(f11(a12))), % 117.57/117.62 inference(scs_inference,[],[146,29,2,20])). % 117.57/117.62 cnf(220,plain, % 117.57/117.62 (P4(f11(a12),a12)), % 117.57/117.62 inference(scs_inference,[],[131,146,29,2,20,21])). % 117.57/117.62 cnf(221,plain, % 117.57/117.62 (P4(a12,f11(a12))), % 117.57/117.62 inference(scs_inference,[],[131,146,29,2,20,21,22])). % 117.57/117.62 cnf(222,plain, % 117.57/117.62 (P4(f8(a20,a18),f8(a20,a18))), % 117.57/117.62 inference(scs_inference,[],[131,207,146,29,2,20,21,22,86])). % 117.57/117.62 cnf(233,plain, % 117.57/117.62 (P2(f9(a28,f4(a28)))), % 117.57/117.62 inference(scs_inference,[],[210,58,31,53,2,21,20])). % 117.57/117.62 cnf(235,plain, % 117.57/117.62 (P4(f11(a12),f11(a12))), % 117.57/117.62 inference(scs_inference,[],[210,219,58,31,53,2,21,20,22,86])). % 117.57/117.62 cnf(243,plain, % 117.57/117.62 (P2(f8(a14,a14))), % 117.57/117.62 inference(scs_inference,[],[35,50,2,20])). % 117.57/117.62 cnf(246,plain, % 117.57/117.62 (P4(f9(a28,f4(a28)),f9(a28,f4(a28)))), % 117.57/117.62 inference(scs_inference,[],[222,233,35,50,55,2,20,21,22,86])). % 117.57/117.62 cnf(248,plain, % 117.57/117.62 (P4(f8(a12,f11(a12)),f8(f11(a12),f11(a12)))), % 117.57/117.62 inference(scs_inference,[],[235,222,221,233,35,50,219,55,29,2,20,21,22,86,112])). % 117.57/117.62 cnf(257,plain, % 117.57/117.62 (P2(f8(a19,a22))), % 117.57/117.62 inference(scs_inference,[],[246,54,39,58,2,21,20])). % 117.57/117.62 cnf(259,plain, % 117.57/117.62 (P4(f8(a14,a14),f8(a14,a14))), % 117.57/117.62 inference(scs_inference,[],[246,54,243,39,58,2,21,20,22,86])). % 117.57/117.62 cnf(267,plain, % 117.57/117.62 (P2(f8(a23,a26))), % 117.57/117.62 inference(scs_inference,[],[56,41,2,20])). % 117.57/117.62 cnf(270,plain, % 117.57/117.62 (P4(f8(a19,a22),f8(a19,a22))), % 117.57/117.62 inference(scs_inference,[],[259,56,257,50,41,2,20,21,22,86])). % 117.57/117.62 cnf(278,plain, % 117.57/117.62 (E(a14,f9(a1,f4(a1)))), % 117.57/117.62 inference(scs_inference,[],[57,2])). % 117.57/117.62 cnf(280,plain, % 117.57/117.62 (P2(f9(a1,f4(a1)))), % 117.57/117.62 inference(scs_inference,[],[270,57,54,30,2,21,20])). % 117.57/117.62 cnf(282,plain, % 117.57/117.62 (P4(f8(a23,a26),f8(a23,a26))), % 117.57/117.62 inference(scs_inference,[],[270,57,54,267,30,2,21,20,22,86])). % 117.57/117.62 cnf(290,plain, % 117.57/117.62 (P1(f15(f4(a27)))), % 117.57/117.62 inference(scs_inference,[],[45,69,70])). % 117.57/117.62 cnf(296,plain, % 117.57/117.62 (P4(f9(a1,f4(a1)),f9(a1,f4(a1)))), % 117.57/117.62 inference(scs_inference,[],[282,62,56,280,65,290,42,2,21,22,121,86])). % 117.57/117.62 cnf(304,plain, % 117.57/117.62 (E(a18,f5(a27,a27))), % 117.57/117.62 inference(scs_inference,[],[48,2])). % 117.57/117.62 cnf(306,plain, % 117.57/117.62 (P2(f5(a27,a27))), % 117.57/117.62 inference(scs_inference,[],[296,57,48,33,2,21,20])). % 117.57/117.62 cnf(308,plain, % 117.57/117.62 (P4(a18,a18)), % 117.57/117.62 inference(scs_inference,[],[296,177,57,48,33,47,2,21,20,22,86])). % 117.57/117.62 cnf(316,plain, % 117.57/117.62 (P2(f8(a14,a16))), % 117.57/117.62 inference(scs_inference,[],[52,37,2,20])). % 117.57/117.62 cnf(319,plain, % 117.57/117.62 (P4(f5(a27,a27),f5(a27,a27))), % 117.57/117.62 inference(scs_inference,[],[308,52,306,37,304,2,20,21,22,86])). % 117.57/117.62 cnf(326,plain, % 117.57/117.62 (E(a27,f2(a28))), % 117.57/117.62 inference(scs_inference,[],[27,2])). % 117.57/117.62 cnf(329,plain, % 117.57/117.62 (P3(f2(a28))), % 117.57/117.62 inference(scs_inference,[],[198,208,27,49,51,45,2,21,22,23])). % 117.57/117.62 cnf(350,plain, % 117.57/117.62 (E(f5(a1,a1),f10(f5(f2(a1),f2(a1)),f8(f9(a1,f4(a1)),f9(a1,f4(a1)))))), % 117.57/117.62 inference(scs_inference,[],[135,2])). % 117.57/117.62 cnf(378,plain, % 117.57/117.62 (E(f4(f2(a1)),f4(f2(a28)))), % 117.57/117.62 inference(scs_inference,[],[137,2])). % 117.57/117.62 cnf(384,plain, % 117.57/117.62 (E(f9(a1,a3),f9(a13,a3))), % 117.57/117.62 inference(scs_inference,[],[154,2])). % 117.57/117.62 cnf(390,plain, % 117.57/117.62 (E(f4(a1),f15(f4(a13)))), % 117.57/117.62 inference(scs_inference,[],[150,2])). % 117.57/117.62 cnf(391,plain, % 117.57/117.62 (E(f9(f2(a1),a3),f9(a13,a3))), % 117.57/117.62 inference(scs_inference,[],[384,150,133,2,3])). % 117.57/117.62 cnf(398,plain, % 117.57/117.62 (E(f4(a28),f15(f4(a13)))), % 117.57/117.62 inference(scs_inference,[],[46,391,390,2,3])). % 117.57/117.62 cnf(404,plain, % 117.57/117.62 (E(f15(f4(a13)),f4(a28))), % 117.57/117.62 inference(scs_inference,[],[398,2])). % 117.57/117.62 cnf(405,plain, % 117.57/117.62 (P4(x4051,f10(f8(a23,a23),f8(a26,a26)))+~E(f10(f8(a24,a24),f8(a24,a24)),x4051)), % 117.57/117.62 inference(scs_inference,[],[61,398,2,21])). % 117.57/117.62 cnf(411,plain, % 117.57/117.62 (P4(x4111,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))),x4111)), % 117.57/117.62 inference(scs_inference,[],[63,133,2,21])). % 117.57/117.62 cnf(417,plain, % 117.57/117.62 (E(f4(a28),f15(f4(f2(a1))))), % 117.57/117.62 inference(scs_inference,[],[46,129,2,3])). % 117.57/117.62 cnf(423,plain, % 117.57/117.62 (P2(f11(f10(a17,a17)))), % 117.57/117.62 inference(scs_inference,[],[32,71,87])). % 117.57/117.62 cnf(424,plain, % 117.57/117.62 (E(f15(f4(f2(a1))),f4(a28))), % 117.57/117.62 inference(scs_inference,[],[417,2])). % 117.57/117.62 cnf(425,plain, % 117.57/117.62 (E(f15(f4(a13)),f15(f4(f2(a1))))), % 117.57/117.62 inference(scs_inference,[],[404,417,2,3])). % 117.57/117.62 cnf(426,plain, % 117.57/117.62 (P4(f11(f10(a17,a17)),f11(f10(a17,a17)))), % 117.57/117.62 inference(scs_inference,[],[423,404,417,2,3,86])). % 117.57/117.62 cnf(433,plain, % 117.57/117.62 (E(f15(f4(f2(a1))),f15(f4(a13)))), % 117.57/117.62 inference(scs_inference,[],[425,2])). % 117.57/117.62 cnf(449,plain, % 117.57/117.62 (E(f4(a13),f4(f2(a1)))+~P1(f4(f2(a1)))+~P1(f4(a13))), % 117.57/117.62 inference(scs_inference,[],[426,52,390,425,84])). % 117.57/117.62 cnf(459,plain, % 117.57/117.62 (~P1(f4(a28))+P1(f4(a1))), % 117.57/117.62 inference(scs_inference,[],[139,46,398,20,22,19])). % 117.57/117.62 cnf(478,plain, % 117.57/117.62 (P4(f8(a12,f11(a12)),x4781)+~E(f8(f11(a12),f11(a12)),x4781)), % 117.57/117.62 inference(scs_inference,[],[248,424,20,22])). % 117.57/117.62 cnf(502,plain, % 117.57/117.62 (P4(a12,f10(a12,a12))), % 117.57/117.62 inference(scs_inference,[],[29,79,104])). % 117.57/117.62 cnf(505,plain, % 117.57/117.62 (P4(f10(f10(f8(a24,a24),f8(a24,a24)),f10(f8(a24,a24),f8(a24,a24))),x5051)+~E(f10(f10(f8(a23,a23),f8(a23,a26)),f10(f8(a26,a23),f8(a26,a26))),x5051)), % 117.57/117.62 inference(scs_inference,[],[63,502,218,433,21,20,22])). % 117.57/117.62 cnf(543,plain, % 117.57/117.62 (P2(f10(f5(f2(a1),f2(a1)),f8(f9(a1,f4(a1)),f9(a1,f4(a1)))))), % 117.57/117.62 inference(scs_inference,[],[350,42,20,98])). % 117.57/117.62 cnf(546,plain, % 117.57/117.62 (P2(f5(a1,a1))), % 117.57/117.62 inference(scs_inference,[],[543,135,20])). % 117.57/117.62 cnf(596,plain, % 117.57/117.62 (~P1(f4(a1))+P1(f15(f4(a13)))), % 117.57/117.62 inference(scs_inference,[],[390,19])). % 117.57/117.62 cnf(627,plain, % 117.57/117.62 (~P1(f4(f2(a1)))+P1(f4(a28))), % 117.57/117.62 inference(scs_inference,[],[424,19,69])). % 117.57/117.62 cnf(643,plain, % 117.57/117.62 (~P1(f15(f4(a13)))+P1(f4(a28))), % 117.57/117.62 inference(scs_inference,[],[404,19])). % 117.57/117.62 cnf(644,plain, % 117.57/117.62 (~P1(f4(a13))+P1(f4(a28))), % 117.57/117.62 inference(scs_inference,[],[404,19,69])). % 117.57/117.62 cnf(648,plain, % 117.57/117.62 (~P1(f4(a13))+P1(f15(f4(f2(a1))))), % 117.57/117.62 inference(scs_inference,[],[425,19,69])). % 117.57/117.62 cnf(653,plain, % 117.57/117.62 (~P1(f4(f2(a1)))+P1(f15(f4(a13)))), % 117.57/117.62 inference(scs_inference,[],[433,19,69])). % 117.57/117.62 cnf(688,plain, % 117.57/117.62 (~P1(f4(a1))+P1(f4(a28))), % 117.57/117.62 inference(scs_inference,[],[126,19])). % 117.57/117.62 cnf(697,plain, % 117.57/117.62 (~P1(f4(f2(a1)))+P1(f4(f2(a28)))), % 117.57/117.62 inference(scs_inference,[],[378,19])). % 117.57/117.62 cnf(930,plain, % 117.57/117.62 (~P4(a12,f5(a27,a27))+P4(f8(a12,f5(a27,a27)),f8(f5(a27,a27),f5(a27,a27)))), % 117.57/117.62 inference(scs_inference,[],[131,319,306,29,103,112])). % 117.57/117.62 cnf(1073,plain, % 117.57/117.62 (~E(f15(f15(f15(f4(a27)))),a3)), % 117.57/117.62 inference(scs_inference,[],[290,68,69])). % 117.57/117.62 cnf(1119,plain, % 117.57/117.62 (P5(f4(f2(a28)),f15(f4(f2(a28))))), % 117.57/117.62 inference(scs_inference,[],[329,83,70])). % 117.57/117.62 cnf(1120,plain, % 117.57/117.62 (P5(f4(f2(a1)),f15(f4(f2(a28))))), % 117.57/117.62 inference(scs_inference,[],[137,1119,24])). % 117.57/117.62 cnf(1121,plain, % 117.57/117.62 (P5(f4(f2(a28)),x11211)+~E(f15(f4(f2(a28))),x11211)), % 117.57/117.62 inference(scs_inference,[],[137,1119,24,25])). % 117.57/117.62 cnf(1126,plain, % 117.57/117.62 (P5(f4(f2(a1)),x11261)+~E(f15(f4(f2(a28))),x11261)), % 117.57/117.62 inference(scs_inference,[],[1120,25])). % 117.57/117.62 cnf(1306,plain, % 117.57/117.62 (P1(f4(a1))), % 117.57/117.62 inference(scs_inference,[],[43,459,70])). % 117.57/117.62 cnf(1307,plain, % 117.57/117.62 (P1(f15(f4(a13)))), % 117.57/117.62 inference(scs_inference,[],[1306,596])). % 117.57/117.62 cnf(1309,plain, % 117.57/117.62 (P1(f4(a28))), % 117.57/117.62 inference(scs_inference,[],[1306,688])). % 117.57/117.62 cnf(1310,plain, % 117.57/117.62 (E(f9(f2(a1),f4(a1)),f9(a1,f4(a1)))), % 117.57/117.62 inference(scs_inference,[],[65,1306,42,121])). % 117.57/117.62 cnf(1312,plain, % 117.57/117.62 (E(f9(a13,f4(a1)),f9(a1,f4(a1)))), % 117.57/117.62 inference(scs_inference,[],[149,65,1306,42,121,97])). % 117.57/117.62 cnf(1314,plain, % 117.57/117.62 (E(f9(a1,f4(a1)),f9(f2(a1),f4(a1)))), % 117.57/117.62 inference(scs_inference,[],[149,65,1306,42,121,97,2])). % 117.57/117.62 cnf(1325,plain, % 117.57/117.62 (P1(f4(a28))), % 117.57/117.62 inference(scs_inference,[],[1307,643])). % 117.57/117.62 cnf(1330,plain, % 117.57/117.62 (E(f9(a1,f4(a1)),f9(a13,f4(a1)))), % 117.57/117.62 inference(scs_inference,[],[1312,2])). % 117.57/117.62 cnf(1331,plain, % 117.57/117.62 (E(a14,f9(f2(a1),f4(a1)))), % 117.57/117.62 inference(scs_inference,[],[278,1314,1312,2,3])). % 117.57/117.62 cnf(1332,plain, % 117.57/117.62 (P2(f9(f2(a1),f4(a1)))), % 117.57/117.62 inference(scs_inference,[],[280,278,1314,1312,2,3,20])). % 117.57/117.62 cnf(1335,plain, % 117.57/117.62 (P4(f9(f2(a1),f4(a1)),a14)), % 117.57/117.62 inference(scs_inference,[],[280,278,1314,1312,2,3,20,86,190])). % 117.57/117.62 cnf(1336,plain, % 117.57/117.62 (P4(f9(a1,f4(a1)),f9(f2(a1),f4(a1)))), % 117.57/117.62 inference(scs_inference,[],[280,278,1314,1312,1310,2,3,20,86,190,21])). % 117.57/117.62 cnf(1343,plain, % 117.57/117.62 (E(a14,f9(a13,f4(a1)))), % 117.57/117.62 inference(scs_inference,[],[278,1330,1331,2,3])). % 117.57/117.62 cnf(1344,plain, % 117.57/117.62 (P4(a14,f9(f2(a1),f4(a1)))), % 117.57/117.62 inference(scs_inference,[],[1336,57,278,1330,1331,2,3,21])). % 117.57/117.62 cnf(1345,plain, % 117.57/117.62 (P2(f9(a13,f4(a1)))), % 117.57/117.62 inference(scs_inference,[],[1336,280,57,278,1330,1331,2,3,21,20])). % 117.57/117.62 cnf(1346,plain, % 117.57/117.62 (P4(f9(a13,f4(a1)),f9(a13,f4(a1)))), % 117.57/117.62 inference(scs_inference,[],[1336,280,57,278,1330,1331,2,3,21,20,86])). % 117.57/117.62 cnf(1355,plain, % 117.57/117.62 (P4(f9(a1,f4(a1)),f9(a13,f4(a1)))), % 117.57/117.62 inference(scs_inference,[],[1346,1343,1312,2,21])). % 117.57/117.62 cnf(1360,plain, % 117.57/117.62 (P4(a14,f9(a13,f4(a1)))), % 117.57/117.62 inference(scs_inference,[],[1355,57,21])). % 117.57/117.62 cnf(1439,plain, % 117.57/117.62 (E(f9(a13,f4(a28)),f9(a1,f4(a28)))), % 117.57/117.62 inference(scs_inference,[],[65,149,1309,42,121,97])). % 117.57/117.62 cnf(1441,plain, % 117.57/117.62 (E(f9(a1,f4(a28)),f9(f2(a1),f4(a28)))), % 117.57/117.62 inference(scs_inference,[],[65,149,1309,42,121,97,2])). % 117.57/117.62 cnf(1442,plain, % 117.57/117.62 (E(x14421,f9(a1,f4(a28)))+~E(x14421,f9(a13,f4(a28)))), % 117.57/117.62 inference(scs_inference,[],[65,149,1309,42,121,97,2,3])). % 117.57/117.62 cnf(1448,plain, % 117.57/117.62 (E(f9(a13,f4(a28)),f9(f2(a1),f4(a28)))), % 117.57/117.62 inference(scs_inference,[],[1441,1439,2,3])). % 117.57/117.62 cnf(1455,plain, % 117.57/117.62 (E(f9(f2(a1),f4(a28)),f9(a13,f4(a28)))), % 117.57/117.62 inference(scs_inference,[],[1448,2])). % 117.57/117.62 cnf(1485,plain, % 117.57/117.62 (~P2(f9(a13,f4(a28)))+P2(f9(f2(a1),f4(a28)))), % 117.57/117.62 inference(scs_inference,[],[1448,1439,19,20])). % 117.57/117.62 cnf(1490,plain, % 117.57/117.62 (~P2(f9(f2(a1),f4(a28)))+P2(f9(a13,f4(a28)))), % 117.57/117.62 inference(scs_inference,[],[1455,20])). % 117.57/117.62 cnf(1491,plain, % 117.57/117.62 (~P2(f9(a13,f4(a28)))+P2(f9(a13,f4(a28)))), % 117.57/117.62 inference(scs_inference,[],[1455,20,1485])). % 117.57/117.62 cnf(1497,plain, % 117.57/117.62 (~P2(f9(a13,f4(a28)))+P2(f9(a1,f4(a28)))), % 117.57/117.62 inference(scs_inference,[],[1439,20])). % 117.57/117.62 cnf(1663,plain, % 117.57/117.62 (E(f9(f2(a1),f4(a1)),f9(a13,f4(a1)))), % 117.57/117.62 inference(scs_inference,[],[1335,1344,1343,1310,1330,22,21,3])). % 117.57/117.62 cnf(3271,plain, % 117.57/117.62 (P4(f11(a12),a18)+~P4(a12,a18)), % 117.57/117.62 inference(scs_inference,[],[33,220,219,29,103])). % 117.57/117.62 cnf(3540,plain, % 117.57/117.62 (~E(f15(f4(a28)),a3)), % 117.57/117.62 inference(scs_inference,[],[1325,423,71,83,68])). % 117.57/117.62 cnf(3550,plain, % 117.57/117.62 (P4(a12,f5(a27,a27))), % 117.57/117.62 inference(scs_inference,[],[45,1325,423,71,83,68,72,77,78,90,91])). % 117.57/117.62 cnf(3577,plain, % 117.57/117.62 (P1(f15(f4(a28)))), % 117.57/117.62 inference(scs_inference,[],[1073,1663,45,1325,423,71,83,68,72,77,78,90,91,74,75,4,7,8,13,18,81,82,5,6,9,10,11,12,14,15,16,17,930,2,69])). % 117.57/117.62 cnf(3579,plain, % 117.57/117.62 (P1(f4(a27))), % 117.57/117.62 inference(scs_inference,[],[1073,1663,45,1325,423,71,83,68,72,77,78,90,91,74,75,4,7,8,13,18,81,82,5,6,9,10,11,12,14,15,16,17,930,2,69,70])). % 117.57/117.62 cnf(3583,plain, % 117.57/117.62 (P1(f6(f4(a1)))), % 117.57/117.62 inference(scs_inference,[],[1073,1663,45,1325,1306,423,65,71,83,68,72,77,78,90,91,74,75,4,7,8,13,18,81,82,5,6,9,10,11,12,14,15,16,17,930,2,69,70,88,73])). % 117.57/117.62 cnf(3593,plain, % 117.57/117.62 (~E(f4(a28),a3)), % 117.57/117.62 inference(scs_inference,[],[1073,1663,45,126,1325,1306,423,65,71,83,68,72,77,78,90,91,74,75,4,7,8,13,18,81,82,5,6,9,10,11,12,14,15,16,17,930,2,69,70,88,73,76,96,100,101,3])). % 117.57/117.62 cnf(3594,plain, % 117.57/117.62 (P2(f5(a28,a28))), % 117.57/117.62 inference(scs_inference,[],[1073,1663,45,126,1325,1306,423,43,65,71,83,68,72,77,78,90,91,74,75,4,7,8,13,18,81,82,5,6,9,10,11,12,14,15,16,17,930,2,69,70,88,73,76,96,100,101,3,122])). % 117.57/117.62 cnf(3598,plain, % 117.57/117.62 (P2(f9(a27,f4(a28)))), % 117.57/117.62 inference(scs_inference,[],[1073,1663,45,126,1325,1306,423,43,65,71,83,68,72,77,78,90,91,74,75,4,7,8,13,18,81,82,5,6,9,10,11,12,14,15,16,17,930,2,69,70,88,73,76,96,100,101,3,122,87,89])). % 117.57/117.62 cnf(3608,plain, % 117.57/117.62 (P2(f5(a1,a28))), % 117.57/117.62 inference(scs_inference,[],[1073,1663,45,126,1325,1306,423,43,546,65,42,71,83,68,72,77,78,90,91,74,75,4,7,8,13,18,81,82,5,6,9,10,11,12,14,15,16,17,930,2,69,70,88,73,76,96,100,101,3,122,87,89,106,107,109,110,98])). % 117.57/117.62 cnf(3610,plain, % 117.57/117.62 (~E(f15(f4(a1)),f15(a3))), % 117.57/117.62 inference(scs_inference,[],[1073,1663,45,126,1325,1306,423,28,43,546,65,42,71,83,68,72,77,78,90,91,74,75,4,7,8,13,18,81,82,5,6,9,10,11,12,14,15,16,17,930,2,69,70,88,73,76,96,100,101,3,122,87,89,106,107,109,110,98,84])). % 117.57/117.62 cnf(3625,plain, % 117.57/117.62 (E(f15(f4(a27)),f4(a28))), % 117.57/117.62 inference(scs_inference,[],[1073,1663,45,1360,326,126,398,1325,1306,423,28,43,1345,546,30,221,219,46,65,42,71,83,68,72,77,78,90,91,74,75,4,7,8,13,18,81,82,5,6,9,10,11,12,14,15,16,17,930,2,69,70,88,73,76,96,100,101,3,122,87,89,106,107,109,110,98,84,105,114,116,111,79,119,24,85])). % 117.57/117.62 cnf(3627,plain, % 117.57/117.62 (E(f9(f2(a28),f4(a28)),f9(a28,f4(a28)))), % 117.57/117.62 inference(scs_inference,[],[1073,1663,45,1360,326,126,398,1325,1306,423,28,43,1345,546,30,221,219,46,65,42,71,83,68,72,77,78,90,91,74,75,4,7,8,13,18,81,82,5,6,9,10,11,12,14,15,16,17,930,2,69,70,88,73,76,96,100,101,3,122,87,89,106,107,109,110,98,84,105,114,116,111,79,119,24,85,121])). % 117.57/117.62 cnf(3633,plain, % 117.57/117.62 (E(f9(a27,f4(a28)),f9(a28,f4(a28)))), % 117.57/117.62 inference(scs_inference,[],[1073,1663,45,1360,326,126,398,1325,1306,423,28,43,1345,546,306,30,221,219,46,65,42,71,83,68,72,77,78,90,91,74,75,4,7,8,13,18,81,82,5,6,9,10,11,12,14,15,16,17,930,2,69,70,88,73,76,96,100,101,3,122,87,89,106,107,109,110,98,84,105,114,116,111,79,119,24,85,121,124,104,97])). % 117.57/117.62 cnf(3639,plain, % 117.57/117.62 (E(f8(a12,f5(a28,a28)),a12)), % 117.57/117.62 inference(scs_inference,[],[3594,75])). % 117.57/117.62 cnf(3641,plain, % 117.57/117.62 (E(f8(f5(a28,a28),a12),a12)), % 117.57/117.62 inference(scs_inference,[],[3594,75,74])). % 117.57/117.62 cnf(3643,plain, % 117.57/117.62 (E(f10(f5(a28,a28),a12),f5(a28,a28))), % 117.57/117.62 inference(scs_inference,[],[3594,75,74,77])). % 117.57/117.62 cnf(3647,plain, % 117.57/117.62 (E(f15(f15(f4(a27))),f15(f4(a28)))), % 117.57/117.62 inference(scs_inference,[],[3579,3594,3625,75,74,77,83,13])). % 117.57/117.62 cnf(3651,plain, % 117.57/117.62 (E(f6(f15(f4(a27))),f6(f4(a28)))), % 117.57/117.62 inference(scs_inference,[],[3579,3594,3625,75,74,77,83,13,9,10,12,18])). % 117.57/117.62 cnf(3652,plain, % 117.57/117.62 (~E(f15(f4(a27)),a3)), % 117.57/117.62 inference(scs_inference,[],[3579,3594,3625,75,74,77,83,13,9,10,12,18,68])). % 117.57/117.62 cnf(3654,plain, % 117.57/117.62 (E(f10(a12,f5(a28,a28)),f5(a28,a28))), % 117.57/117.62 inference(scs_inference,[],[3579,3594,3625,75,74,77,83,13,9,10,12,18,68,78])). % 117.57/117.62 cnf(3660,plain, % 117.57/117.62 (P2(f11(f5(a28,a28)))), % 117.57/117.62 inference(scs_inference,[],[3579,3594,3625,75,74,77,83,13,9,10,12,18,68,78,81,72,71])). % 117.57/117.62 cnf(3662,plain, % 117.57/117.62 (P4(a12,f5(a28,a28))), % 117.57/117.62 inference(scs_inference,[],[3579,3594,3625,43,75,74,77,83,13,9,10,12,18,68,78,81,72,71,91])). % 117.57/117.62 cnf(3665,plain, % 117.57/117.62 (P4(a12,f8(f5(a28,a28),f5(a28,a28)))), % 117.57/117.62 inference(scs_inference,[],[3579,3594,3625,43,75,74,77,83,13,9,10,12,18,68,78,81,72,71,91,5,90])). % 117.57/117.62 cnf(3667,plain, % 117.57/117.62 (P4(f5(a28,a28),f5(a28,a28))), % 117.57/117.62 inference(scs_inference,[],[3579,3594,3625,43,75,74,77,83,13,9,10,12,18,68,78,81,72,71,91,5,90,79])). % 117.57/117.62 cnf(3669,plain, % 117.57/117.62 (E(f10(f11(f5(a28,a28)),f5(a28,a28)),a12)), % 117.57/117.62 inference(scs_inference,[],[3579,3594,3625,43,75,74,77,83,13,9,10,12,18,68,78,81,72,71,91,5,90,79,82])). % 117.57/117.62 cnf(3680,plain, % 117.57/117.62 (~E(a3,f4(a28))), % 117.57/117.62 inference(scs_inference,[],[3579,3594,3593,3625,43,75,74,77,83,13,9,10,12,18,68,78,81,72,71,91,5,90,79,82,17,7,16,11,15,4,6,8,14,2])). % 117.57/117.62 cnf(3681,plain, % 117.57/117.62 (P1(f15(f15(f4(a28))))), % 117.57/117.62 inference(scs_inference,[],[3579,3594,3593,3625,3577,43,75,74,77,83,13,9,10,12,18,68,78,81,72,71,91,5,90,79,82,17,7,16,11,15,4,6,8,14,2,69])). % 117.57/117.62 cnf(3683,plain, % 117.57/117.62 (P1(f4(f2(a1)))), % 117.57/117.62 inference(scs_inference,[],[3579,3594,3593,3625,3577,43,127,75,74,77,83,13,9,10,12,18,68,78,81,72,71,91,5,90,79,82,17,7,16,11,15,4,6,8,14,2,69,70])). % 117.57/117.62 cnf(3685,plain, % 117.57/117.62 (E(f11(f8(f5(a28,a28),f5(a28,a28))),f8(f11(f5(a28,a28)),f5(a28,a28)))), % 117.57/117.62 inference(scs_inference,[],[3579,3594,3593,3625,3577,43,127,75,74,77,83,13,9,10,12,18,68,78,81,72,71,91,5,90,79,82,17,7,16,11,15,4,6,8,14,2,69,70,101])). % 117.57/117.62 cnf(3689,plain, % 117.57/117.62 (P1(f6(f15(f4(a28))))), % 117.57/117.62 inference(scs_inference,[],[3579,3594,3593,3625,3577,3540,43,127,75,74,77,83,13,9,10,12,18,68,78,81,72,71,91,5,90,79,82,17,7,16,11,15,4,6,8,14,2,69,70,101,100,73])). % 117.57/117.62 cnf(3693,plain, % 117.57/117.62 (E(f15(f6(f15(f4(a28)))),f15(f4(a28)))), % 117.57/117.62 inference(scs_inference,[],[3579,3594,3593,3625,3577,3540,43,127,75,74,77,83,13,9,10,12,18,68,78,81,72,71,91,5,90,79,82,17,7,16,11,15,4,6,8,14,2,69,70,101,100,73,96,76])). % 117.57/117.62 cnf(3695,plain, % 117.57/117.62 (P2(f8(f5(a28,a28),f5(a28,a28)))), % 117.57/117.62 inference(scs_inference,[],[3579,3594,3593,3625,3577,3540,43,127,75,74,77,83,13,9,10,12,18,68,78,81,72,71,91,5,90,79,82,17,7,16,11,15,4,6,8,14,2,69,70,101,100,73,96,76,88])). % 117.57/117.62 cnf(3697,plain, % 117.57/117.62 (P2(f10(f5(a28,a28),f5(a28,a28)))), % 117.57/117.62 inference(scs_inference,[],[3579,3594,3593,3625,3577,3540,43,127,75,74,77,83,13,9,10,12,18,68,78,81,72,71,91,5,90,79,82,17,7,16,11,15,4,6,8,14,2,69,70,101,100,73,96,76,88,87])). % 117.57/117.62 cnf(3699,plain, % 117.57/117.62 (P2(f9(a27,f4(a27)))), % 117.57/117.62 inference(scs_inference,[],[3579,3594,3593,3625,3577,3540,45,43,127,75,74,77,83,13,9,10,12,18,68,78,81,72,71,91,5,90,79,82,17,7,16,11,15,4,6,8,14,2,69,70,101,100,73,96,76,88,87,89])). % 117.57/117.62 cnf(3701,plain, % 117.57/117.62 (E(f9(a27,f4(a28)),a16)), % 117.57/117.62 inference(scs_inference,[],[3579,3594,3593,3625,3577,3540,3633,58,45,43,127,75,74,77,83,13,9,10,12,18,68,78,81,72,71,91,5,90,79,82,17,7,16,11,15,4,6,8,14,2,69,70,101,100,73,96,76,88,87,89,3])). % 117.57/117.62 cnf(3702,plain, % 117.57/117.62 (P2(f5(f2(a1),f2(a1)))), % 117.57/117.62 inference(scs_inference,[],[3579,3594,3593,3625,3577,3540,3633,58,45,43,127,75,74,77,83,13,9,10,12,18,68,78,81,72,71,91,5,90,79,82,17,7,16,11,15,4,6,8,14,2,69,70,101,100,73,96,76,88,87,89,3,122])). % 117.57/117.62 cnf(3708,plain, % 117.57/117.62 (E(f10(f8(f5(a28,a28),f5(a28,a28)),f8(f5(a28,a28),f5(a28,a28))),f8(f10(f5(a28,a28),f5(a28,a28)),f5(a28,a28)))), % 117.57/117.62 inference(scs_inference,[],[3579,3594,3593,3625,3577,3540,3633,58,45,43,127,75,74,77,83,13,9,10,12,18,68,78,81,72,71,91,5,90,79,82,17,7,16,11,15,4,6,8,14,2,69,70,101,100,73,96,76,88,87,89,3,122,109,106,110])). % 117.57/117.62 cnf(3720,plain, % 117.57/117.62 (P4(f10(a12,f5(a28,a28)),f10(f5(a27,a27),f5(a28,a28)))), % 117.57/117.62 inference(scs_inference,[],[3550,3579,3594,3593,3625,3577,3540,3633,58,45,126,43,306,127,42,29,75,74,77,83,13,9,10,12,18,68,78,81,72,71,91,5,90,79,82,17,7,16,11,15,4,6,8,14,2,69,70,101,100,73,96,76,88,87,89,3,122,109,106,110,107,104,105,114,116,111])). % 117.57/117.62 cnf(3722,plain, % 117.57/117.62 (P4(f8(a12,f5(a28,a28)),f8(f5(a27,a27),f5(a28,a28)))), % 117.57/117.62 inference(scs_inference,[],[3550,3579,3594,3593,3625,3577,3540,3633,58,45,126,43,306,127,42,29,75,74,77,83,13,9,10,12,18,68,78,81,72,71,91,5,90,79,82,17,7,16,11,15,4,6,8,14,2,69,70,101,100,73,96,76,88,87,89,3,122,109,106,110,107,104,105,114,116,111,112])). % 117.57/117.62 cnf(3724,plain, % 117.57/117.62 (E(f4(a13),f4(f2(a1)))+~P1(f4(a13))), % 117.57/117.62 inference(scs_inference,[],[3550,3579,3594,3593,3625,3577,3540,3633,58,45,126,43,306,127,42,29,75,74,77,83,13,9,10,12,18,68,78,81,72,71,91,5,90,79,82,17,7,16,11,15,4,6,8,14,2,69,70,101,100,73,96,76,88,87,89,3,122,109,106,110,107,104,105,114,116,111,112,449])). % 117.57/117.62 cnf(3727,plain, % 117.57/117.62 (P4(a12,a18)), % 117.57/117.62 inference(scs_inference,[],[3550,3579,3594,3593,3625,3577,3540,3633,58,48,45,126,218,43,306,127,42,29,75,74,77,83,13,9,10,12,18,68,78,81,72,71,91,5,90,79,82,17,7,16,11,15,4,6,8,14,2,69,70,101,100,73,96,76,88,87,89,3,122,109,106,110,107,104,105,114,116,111,112,449,21,25,22])). % 117.57/117.62 cnf(3728,plain, % 117.57/117.62 (E(f9(a27,f4(a27)),f9(a28,f4(a27)))), % 117.57/117.62 inference(scs_inference,[],[3550,3579,3594,3593,3625,3577,3540,3633,326,58,48,45,126,218,43,306,127,42,29,75,74,77,83,13,9,10,12,18,68,78,81,72,71,91,5,90,79,82,17,7,16,11,15,4,6,8,14,2,69,70,101,100,73,96,76,88,87,89,3,122,109,106,110,107,104,105,114,116,111,112,449,21,25,22,97])). % 117.57/117.62 cnf(3730,plain, % 117.57/117.62 (P4(f11(a12),a18)), % 117.57/117.62 inference(scs_inference,[],[3550,3579,3594,3593,3625,3577,3540,3633,326,58,48,45,126,218,43,306,127,42,29,75,74,77,83,13,9,10,12,18,68,78,81,72,71,91,5,90,79,82,17,7,16,11,15,4,6,8,14,2,69,70,101,100,73,96,76,88,87,89,3,122,109,106,110,107,104,105,114,116,111,112,449,21,25,22,97,3271])). % 117.57/117.62 cnf(3734,plain, % 117.57/117.62 (P1(f4(a28))), % 117.57/117.62 inference(scs_inference,[],[3683,627])). % 117.57/117.62 cnf(3735,plain, % 117.57/117.62 (P1(f15(f4(a13)))), % 117.57/117.62 inference(scs_inference,[],[3683,653])). % 117.57/117.62 cnf(3736,plain, % 117.57/117.62 (P1(f4(f2(a28)))), % 117.57/117.62 inference(scs_inference,[],[3683,697])). % 117.57/117.62 cnf(3737,plain, % 117.57/117.62 (E(f8(f5(a1,a28),a12),a12)), % 117.57/117.62 inference(scs_inference,[],[3608,74])). % 117.57/117.62 cnf(3739,plain, % 117.57/117.62 (~E(f15(f6(f4(a1))),a3)), % 117.57/117.62 inference(scs_inference,[],[3608,3583,74,68])). % 117.57/117.62 cnf(3741,plain, % 117.57/117.62 (P2(f11(f5(a1,a28)))), % 117.57/117.62 inference(scs_inference,[],[3608,3583,74,68,71])). % 117.57/117.62 cnf(3743,plain, % 117.57/117.62 (E(f8(a12,f5(a1,a28)),a12)), % 117.57/117.62 inference(scs_inference,[],[3608,3583,74,68,71,75])). % 117.57/117.62 cnf(3745,plain, % 117.57/117.62 (E(f10(f5(a1,a28),a12),f5(a1,a28))), % 117.57/117.62 inference(scs_inference,[],[3608,3583,74,68,71,75,77])). % 117.57/117.62 cnf(3747,plain, % 117.57/117.62 (P4(a12,f5(f2(a1),f2(a1)))), % 117.57/117.62 inference(scs_inference,[],[3608,3583,127,74,68,71,75,77,91])). % 117.57/117.62 cnf(3757,plain, % 117.57/117.62 (E(f10(a12,f5(a1,a28)),f5(a1,a28))), % 117.57/117.62 inference(scs_inference,[],[3608,3643,3583,127,74,68,71,75,77,91,83,13,18,81,79,78])). % 117.57/117.62 cnf(3765,plain, % 117.57/117.62 (P4(a12,f8(f5(a1,a28),f5(a1,a28)))), % 117.57/117.62 inference(scs_inference,[],[3608,3643,3583,127,74,68,71,75,77,91,83,13,18,81,79,78,72,17,7,11,9,90])). % 117.57/117.62 cnf(3773,plain, % 117.57/117.62 (~E(f15(a3),f15(f4(a1)))), % 117.57/117.62 inference(scs_inference,[],[3608,3643,3610,3583,127,74,68,71,75,77,91,83,13,18,81,79,78,72,17,7,11,9,90,12,82,10,5,16,2])). % 117.57/117.62 cnf(3778,plain, % 117.57/117.62 (P1(f15(f6(f4(a1))))), % 117.57/117.62 inference(scs_inference,[],[3608,3643,3610,3583,127,74,68,71,75,77,91,83,13,18,81,79,78,72,17,7,11,9,90,12,82,10,5,16,2,6,8,4,15,69])). % 117.57/117.62 cnf(3781,plain, % 117.57/117.62 (P1(f4(a13))), % 117.57/117.62 inference(scs_inference,[],[3608,3643,3610,3583,127,44,74,68,71,75,77,91,83,13,18,81,79,78,72,17,7,11,9,90,12,82,10,5,16,2,6,8,4,15,69,14,70])). % 117.57/117.62 cnf(3787,plain, % 117.57/117.62 (E(f15(f6(f15(f4(a27)))),f15(f4(a27)))), % 117.57/117.62 inference(scs_inference,[],[3608,3643,3610,3583,3652,290,127,44,74,68,71,75,77,91,83,13,18,81,79,78,72,17,7,11,9,90,12,82,10,5,16,2,6,8,4,15,69,14,70,100,96,76])). % 117.57/117.62 cnf(3789,plain, % 117.57/117.62 (P1(f6(f15(f4(a27))))), % 117.57/117.62 inference(scs_inference,[],[3608,3643,3610,3583,3652,290,127,44,74,68,71,75,77,91,83,13,18,81,79,78,72,17,7,11,9,90,12,82,10,5,16,2,6,8,4,15,69,14,70,100,96,76,73])). % 117.57/117.62 cnf(3791,plain, % 117.57/117.62 (P2(f8(f5(a1,a28),f5(a1,a28)))), % 117.57/117.62 inference(scs_inference,[],[3608,3643,3610,3583,3652,290,127,44,74,68,71,75,77,91,83,13,18,81,79,78,72,17,7,11,9,90,12,82,10,5,16,2,6,8,4,15,69,14,70,100,96,76,73,88])). % 117.57/117.62 cnf(3795,plain, % 117.57/117.62 (P2(f10(f5(a1,a28),f5(a1,a28)))), % 117.57/117.62 inference(scs_inference,[],[3608,3643,3610,3583,3652,290,127,44,74,68,71,75,77,91,83,13,18,81,79,78,72,17,7,11,9,90,12,82,10,5,16,2,6,8,4,15,69,14,70,100,96,76,73,88,101,87])). % 117.57/117.62 cnf(3797,plain, % 117.57/117.62 (P2(f5(f2(a28),f2(a28)))), % 117.57/117.62 inference(scs_inference,[],[3608,3643,3610,3583,3652,290,127,44,329,74,68,71,75,77,91,83,13,18,81,79,78,72,17,7,11,9,90,12,82,10,5,16,2,6,8,4,15,69,14,70,100,96,76,73,88,101,87,122])). % 117.57/117.62 cnf(3799,plain, % 117.57/117.62 (~E(a3,f15(f4(f2(a1))))), % 117.57/117.62 inference(scs_inference,[],[3680,3608,3643,3610,3583,3652,424,290,127,44,329,74,68,71,75,77,91,83,13,18,81,79,78,72,17,7,11,9,90,12,82,10,5,16,2,6,8,4,15,69,14,70,100,96,76,73,88,101,87,122,3])). % 117.57/117.62 cnf(3802,plain, % 117.57/117.62 (P2(f9(a28,f4(a27)))), % 117.57/117.62 inference(scs_inference,[],[3680,3608,3643,3610,3583,3699,3652,3728,424,45,290,127,44,329,74,68,71,75,77,91,83,13,18,81,79,78,72,17,7,11,9,90,12,82,10,5,16,2,6,8,4,15,69,14,70,100,96,76,73,88,101,87,122,3,89,20])). % 117.57/117.62 cnf(3819,plain, % 117.57/117.62 (P4(f8(f5(a28,a28),f5(a28,a28)),f8(f5(a28,a28),f5(a28,a28)))), % 117.57/117.62 inference(scs_inference,[],[3727,3667,3680,3608,3662,3643,3610,3702,3583,3699,3652,3728,424,45,290,3594,127,44,329,33,74,68,71,75,77,91,83,13,18,81,79,78,72,17,7,11,9,90,12,82,10,5,16,2,6,8,4,15,69,14,70,100,96,76,73,88,101,87,122,3,89,20,109,110,106,107,104,105,116,111,112])). % 117.57/117.62 cnf(3821,plain, % 117.57/117.62 (~P4(x38211,f8(f10(a23,a26),f10(a23,a26)))+~E(x38211,f8(f10(a24,a24),f10(a24,a24)))), % 117.57/117.62 inference(scs_inference,[],[66,3727,3667,3680,3608,3662,3643,3610,3702,3583,3699,3652,3728,424,45,290,3594,127,44,329,33,74,68,71,75,77,91,83,13,18,81,79,78,72,17,7,11,9,90,12,82,10,5,16,2,6,8,4,15,69,14,70,100,96,76,73,88,101,87,122,3,89,20,109,110,106,107,104,105,116,111,112,21])). % 117.57/117.62 cnf(3826,plain, % 117.57/117.62 (P1(f4(a28))), % 117.57/117.62 inference(scs_inference,[],[3781,644])). % 117.57/117.62 cnf(3827,plain, % 117.57/117.62 (P1(f15(f4(f2(a1))))), % 117.57/117.62 inference(scs_inference,[],[3781,648])). % 117.57/117.62 cnf(3828,plain, % 117.57/117.62 (E(f4(a13),f4(f2(a1)))), % 117.57/117.62 inference(scs_inference,[],[3781,3724])). % 117.57/117.62 cnf(3831,plain, % 117.57/117.62 (~E(f15(f4(a13)),a3)), % 117.57/117.62 inference(scs_inference,[],[3781,3695,77,68])). % 117.57/117.62 cnf(3837,plain, % 117.57/117.62 (P2(f11(f8(f5(a28,a28),f5(a28,a28))))), % 117.57/117.62 inference(scs_inference,[],[3781,3695,77,68,74,81,71])). % 117.57/117.62 cnf(3841,plain, % 117.57/117.62 (P4(a12,f5(a13,a13))), % 117.57/117.62 inference(scs_inference,[],[3781,3695,44,77,68,74,81,71,75,91])). % 117.57/117.62 cnf(3846,plain, % 117.57/117.62 (P5(f4(a13),f15(f4(a13)))), % 117.57/117.62 inference(scs_inference,[],[3781,3654,3695,44,77,68,74,81,71,75,91,18,82,83])). % 117.57/117.62 cnf(3862,plain, % 117.57/117.62 (P1(f15(f15(f4(a13))))), % 117.57/117.62 inference(scs_inference,[],[3781,3654,3695,3797,3735,44,77,68,74,81,71,75,91,18,82,83,78,79,90,17,7,13,10,72,16,11,69])). % 117.57/117.62 cnf(3871,plain, % 117.57/117.62 (~E(f15(f4(f2(a1))),a3)), % 117.57/117.62 inference(scs_inference,[],[3781,3654,3695,3797,3735,3799,44,77,68,74,81,71,75,91,18,82,83,78,79,90,17,7,13,10,72,16,11,69,5,12,9,14,8,4,6,2])). % 117.57/117.62 cnf(3879,plain, % 117.57/117.62 (P1(f6(f4(a28)))), % 117.57/117.62 inference(scs_inference,[],[3734,3781,3654,3695,3797,3735,3799,3593,44,77,68,74,81,71,75,91,18,82,83,78,79,90,17,7,13,10,72,16,11,69,5,12,9,14,8,4,6,2,15,96,101,88,73])). % 117.57/117.62 cnf(3883,plain, % 117.57/117.62 (P2(f10(f8(f5(a28,a28),f5(a28,a28)),f8(f5(a28,a28),f5(a28,a28))))), % 117.57/117.62 inference(scs_inference,[],[3734,3781,3654,3695,3797,3735,3799,3593,44,77,68,74,81,71,75,91,18,82,83,78,79,90,17,7,13,10,72,16,11,69,5,12,9,14,8,4,6,2,15,96,101,88,73,100,87])). % 117.57/117.62 cnf(3885,plain, % 117.57/117.63 (E(f15(f6(f4(a28))),f4(a28))), % 117.57/117.63 inference(scs_inference,[],[3734,3781,3654,3695,3797,3735,3799,3593,44,77,68,74,81,71,75,91,18,82,83,78,79,90,17,7,13,10,72,16,11,69,5,12,9,14,8,4,6,2,15,96,101,88,73,100,87,76])). % 117.57/117.63 cnf(3887,plain, % 117.57/117.63 (P2(f9(f2(a1),f4(a28)))), % 117.57/117.63 inference(scs_inference,[],[3734,3781,3654,3695,3797,3735,3799,3593,127,44,77,68,74,81,71,75,91,18,82,83,78,79,90,17,7,13,10,72,16,11,69,5,12,9,14,8,4,6,2,15,96,101,88,73,100,87,76,89])). % 117.57/117.63 cnf(3889,plain, % 117.57/117.63 (E(f8(a12,f5(a28,a28)),f11(a12))), % 117.57/117.63 inference(scs_inference,[],[3734,3781,3654,3695,3797,3735,3639,3799,3593,218,127,44,77,68,74,81,71,75,91,18,82,83,78,79,90,17,7,13,10,72,16,11,69,5,12,9,14,8,4,6,2,15,96,101,88,73,100,87,76,89,3])). % 117.57/117.63 cnf(3893,plain, % 117.57/117.63 (E(f10(f8(a23,a23),f8(a23,a23)),f8(a23,f10(a23,a23)))), % 117.57/117.63 inference(scs_inference,[],[3734,3781,3654,3695,3797,3735,3639,3720,3799,3593,218,546,38,127,44,77,68,74,81,71,75,91,18,82,83,78,79,90,17,7,13,10,72,16,11,69,5,12,9,14,8,4,6,2,15,96,101,88,73,100,87,76,89,3,21,110,109])). % 117.57/117.63 cnf(3903,plain, % 117.57/117.63 (P4(f10(f8(f5(a28,a28),f5(a28,a28)),f8(f5(a28,a28),f5(a28,a28))),f10(f8(f5(a28,a28),f5(a28,a28)),f8(f5(a28,a28),f5(a28,a28))))), % 117.57/117.63 inference(scs_inference,[],[3734,3781,3654,3695,3797,3735,3747,3665,3639,3819,3720,3799,3702,3593,218,546,38,127,44,77,68,74,81,71,75,91,18,82,83,78,79,90,17,7,13,10,72,16,11,69,5,12,9,14,8,4,6,2,15,96,101,88,73,100,87,76,89,3,21,110,109,106,107,104,116,111])). % 117.57/117.63 cnf(3911,plain, % 117.57/117.63 (P2(f9(a13,f4(a28)))), % 117.57/117.63 inference(scs_inference,[],[3887,1490])). % 117.57/117.63 cnf(3912,plain, % 117.57/117.63 (P2(f11(f9(f2(a1),f4(a28))))), % 117.57/117.63 inference(scs_inference,[],[3887,71])). % 117.57/117.63 cnf(3916,plain, % 117.57/117.63 (~E(f15(f4(f2(a28))),a3)), % 117.57/117.63 inference(scs_inference,[],[3887,3736,71,77,68])). % 117.57/117.63 cnf(3939,plain, % 117.57/117.63 (P4(a12,f8(f9(f2(a1),f4(a28)),f9(f2(a1),f4(a28))))), % 117.57/117.63 inference(scs_inference,[],[3745,3887,3683,3736,329,71,77,68,74,82,81,83,75,91,79,17,72,7,78,18,90])). % 117.57/117.63 cnf(3941,plain, % 117.57/117.63 (P1(f15(f4(f2(a28))))), % 117.57/117.63 inference(scs_inference,[],[3745,3887,3683,3736,329,71,77,68,74,82,81,83,75,91,79,17,72,7,78,18,90,69])). % 117.57/117.63 cnf(3954,plain, % 117.57/117.63 (~E(a3,f15(f4(a13)))), % 117.57/117.63 inference(scs_inference,[],[3745,3887,3683,3736,3831,329,71,77,68,74,82,81,83,75,91,79,17,72,7,78,18,90,69,11,13,12,10,16,5,14,15,4,8,9,2])). % 117.57/117.63 cnf(3960,plain, % 117.57/117.63 (E(f15(f6(f15(f4(a13)))),f15(f4(a13)))), % 117.57/117.63 inference(scs_inference,[],[3745,3887,3683,3736,3831,3735,329,71,77,68,74,82,81,83,75,91,79,17,72,7,78,18,90,69,11,13,12,10,16,5,14,15,4,8,9,2,6,96,88,76])). % 117.57/117.63 cnf(3962,plain, % 117.57/117.63 (P2(f10(f9(f2(a1),f4(a28)),f9(f2(a1),f4(a28))))), % 117.57/117.63 inference(scs_inference,[],[3745,3887,3683,3736,3831,3735,329,71,77,68,74,82,81,83,75,91,79,17,72,7,78,18,90,69,11,13,12,10,16,5,14,15,4,8,9,2,6,96,88,76,87])). % 117.57/117.63 cnf(3966,plain, % 117.57/117.63 (P1(f6(f15(f4(a13))))), % 117.57/117.63 inference(scs_inference,[],[3745,3887,3683,3736,3831,3735,329,71,77,68,74,82,81,83,75,91,79,17,72,7,78,18,90,69,11,13,12,10,16,5,14,15,4,8,9,2,6,96,88,76,87,100,73])). % 117.57/117.63 cnf(3970,plain, % 117.57/117.63 (P2(f9(a27,f4(f2(a1))))), % 117.57/117.63 inference(scs_inference,[],[3745,3887,3683,3736,3831,3735,45,329,71,77,68,74,82,81,83,75,91,79,17,72,7,78,18,90,69,11,13,12,10,16,5,14,15,4,8,9,2,6,96,88,76,87,100,73,101,89])). % 117.57/117.63 cnf(3972,plain, % 117.57/117.63 (~E(a3,f15(f6(f4(a28))))), % 117.57/117.63 inference(scs_inference,[],[3745,3887,3683,3736,3831,3885,3680,3735,45,329,71,77,68,74,82,81,83,75,91,79,17,72,7,78,18,90,69,11,13,12,10,16,5,14,15,4,8,9,2,6,96,88,76,87,100,73,101,89,3])). % 117.57/117.63 cnf(3975,plain, % 117.57/117.63 (E(f10(f8(a24,a24),f8(a24,a24)),f8(a24,f10(a24,a24)))), % 117.57/117.63 inference(scs_inference,[],[3745,3887,3683,3736,3831,3885,3680,3735,45,39,329,71,77,68,74,82,81,83,75,91,79,17,72,7,78,18,90,69,11,13,12,10,16,5,14,15,4,8,9,2,6,96,88,76,87,100,73,101,89,3,110,109])). % 117.57/117.63 cnf(3994,plain, % 117.57/117.63 (~E(f10(f10(f8(a23,a23),f8(a23,a26)),f10(f8(a26,a23),f8(a26,a26))),f8(f10(a23,a26),f10(a23,a26)))), % 117.57/117.63 inference(scs_inference,[],[3730,3841,3745,3887,3791,3683,3736,3765,3831,3885,3680,3735,45,39,164,329,33,221,219,71,77,68,74,82,81,83,75,91,79,17,72,7,78,18,90,69,11,13,12,10,16,5,14,15,4,8,9,2,6,96,88,76,87,100,73,101,89,3,110,109,107,106,105,104,116,111,112,405,3821,411,505])). % 117.57/117.63 cnf(4003,plain, % 117.57/117.63 (P2(f9(a13,f4(a28)))), % 117.57/117.63 inference(scs_inference,[],[3911,1491])). % 117.57/117.63 cnf(4004,plain, % 117.57/117.63 (P2(f9(a1,f4(a28)))), % 117.57/117.63 inference(scs_inference,[],[3911,1497])). % 117.57/117.63 cnf(4006,plain, % 117.57/117.63 (P2(f11(f9(a13,f4(a28))))), % 117.57/117.63 inference(scs_inference,[],[3911,3975,405,71])). % 117.57/117.63 cnf(4008,plain, % 117.57/117.63 (E(f10(f9(a13,f4(a28)),a12),f9(a13,f4(a28)))), % 117.57/117.63 inference(scs_inference,[],[3911,3975,405,71,77])). % 117.57/117.63 cnf(4014,plain, % 117.57/117.63 (~E(f15(f6(f4(a28))),a3)), % 117.57/117.63 inference(scs_inference,[],[3911,3879,3975,405,71,77,83,82,68])). % 117.57/117.63 cnf(4020,plain, % 117.57/117.63 (P4(a12,f5(a1,a1))), % 117.57/117.63 inference(scs_inference,[],[3911,3879,3975,42,405,71,77,83,82,68,81,74,91])). % 117.57/117.63 cnf(4024,plain, % 117.57/117.63 (P4(f9(a13,f4(a28)),f9(a13,f4(a28)))), % 117.57/117.63 inference(scs_inference,[],[3911,3879,3975,42,405,71,77,83,82,68,81,74,91,75,79])). % 117.57/117.63 cnf(4028,plain, % 117.57/117.63 (P4(a12,f8(f9(a13,f4(a28)),f9(a13,f4(a28))))), % 117.57/117.63 inference(scs_inference,[],[3911,3879,3975,42,405,71,77,83,82,68,81,74,91,75,79,72,90])). % 117.57/117.63 cnf(4034,plain, % 117.57/117.63 (P1(f15(f6(f4(a28))))), % 117.57/117.63 inference(scs_inference,[],[3757,3911,3879,3975,42,405,71,77,83,82,68,81,74,91,75,79,72,90,78,7,18,69])). % 117.57/117.63 cnf(4049,plain, % 117.57/117.63 (~E(a3,f15(f6(f4(a1))))), % 117.57/117.63 inference(scs_inference,[],[3757,3911,3879,3975,3739,42,405,71,77,83,82,68,81,74,91,75,79,72,90,78,7,18,69,17,13,11,12,10,4,14,16,5,15,8,9,6,2])). % 117.57/117.63 cnf(4050,plain, % 117.57/117.63 (P2(f8(f9(a13,f4(a28)),f9(a13,f4(a28))))), % 117.57/117.63 inference(scs_inference,[],[3757,3911,3879,3975,3739,42,405,71,77,83,82,68,81,74,91,75,79,72,90,78,7,18,69,17,13,11,12,10,4,14,16,5,15,8,9,6,2,88])). % 117.57/117.63 cnf(4056,plain, % 117.57/117.63 (E(f15(f6(f15(f6(f4(a1))))),f15(f6(f4(a1))))), % 117.57/117.63 inference(scs_inference,[],[3757,3911,3879,3975,3778,3739,42,405,71,77,83,82,68,81,74,91,75,79,72,90,78,7,18,69,17,13,11,12,10,4,14,16,5,15,8,9,6,2,88,96,101,76])). % 117.57/117.63 cnf(4061,plain, % 117.57/117.63 (P2(f9(f2(a28),f4(a28)))), % 117.57/117.63 inference(scs_inference,[],[3826,3757,3911,3828,3879,3846,3975,3778,3739,329,42,405,71,77,83,82,68,81,74,91,75,79,72,90,78,7,18,69,17,13,11,12,10,4,14,16,5,15,8,9,6,2,88,96,101,76,87,24,89])). % 117.57/117.63 cnf(4065,plain, % 117.57/117.63 (P1(f6(f15(f6(f4(a1)))))), % 117.57/117.63 inference(scs_inference,[],[3826,3757,3911,3828,3879,3846,3975,3778,3739,329,42,405,71,77,83,82,68,81,74,91,75,79,72,90,78,7,18,69,17,13,11,12,10,4,14,16,5,15,8,9,6,2,88,96,101,76,87,24,89,100,73])). % 117.57/117.63 cnf(4067,plain, % 117.57/117.63 (E(f4(a13),f4(f2(a28)))), % 117.57/117.63 inference(scs_inference,[],[3826,3757,3911,3828,3879,3846,3975,3778,3739,378,329,42,405,71,77,83,82,68,81,74,91,75,79,72,90,78,7,18,69,17,13,11,12,10,4,14,16,5,15,8,9,6,2,88,96,101,76,87,24,89,100,73,3])). % 117.57/117.63 cnf(4074,plain, % 117.57/117.63 (E(f10(f8(a26,a26),f8(a26,a26)),f8(a26,f10(a26,a26)))), % 117.57/117.63 inference(scs_inference,[],[3826,3757,3889,3911,3828,3879,3846,3722,3975,3778,3739,3708,3903,378,40,329,42,405,71,77,83,82,68,81,74,91,75,79,72,90,78,7,18,69,17,13,11,12,10,4,14,16,5,15,8,9,6,2,88,96,101,76,87,24,89,100,73,3,21,22,110,107,109])). % 117.57/117.63 cnf(4098,plain, % 117.57/117.63 (~E(f15(f15(f15(f4(a28)))),a3)), % 117.57/117.63 inference(scs_inference,[],[4004,3681,71,82,77,81,68])). % 117.57/117.63 cnf(4116,plain, % 117.57/117.63 (P1(f15(f15(f15(f4(a28)))))), % 117.57/117.63 inference(scs_inference,[],[4004,3697,4067,3681,71,82,77,81,68,83,75,72,74,90,79,78,7,13,69])). % 117.57/117.63 cnf(4131,plain, % 117.57/117.63 (~E(a3,f15(f4(f2(a28))))), % 117.57/117.63 inference(scs_inference,[],[4004,3697,4067,3681,3916,71,82,77,81,68,83,75,72,74,90,79,78,7,13,69,18,17,11,12,10,5,14,16,4,15,8,6,9,2])). % 117.57/117.63 cnf(4142,plain, % 117.57/117.63 (E(f15(f6(f15(f4(f2(a1))))),f15(f4(f2(a1))))), % 117.57/117.63 inference(scs_inference,[],[4004,3697,4067,3681,3827,3871,3916,45,71,82,77,81,68,83,75,72,74,90,79,78,7,13,69,18,17,11,12,10,5,14,16,4,15,8,6,9,2,88,96,89,101,87,76])). % 117.57/117.63 cnf(4146,plain, % 117.57/117.63 (P1(f6(f15(f4(f2(a1)))))), % 117.57/117.63 inference(scs_inference,[],[4004,3697,4067,3681,3827,3871,3916,45,71,82,77,81,68,83,75,72,74,90,79,78,7,13,69,18,17,11,12,10,5,14,16,4,15,8,6,9,2,88,96,89,101,87,76,100,73])). % 117.57/117.63 cnf(4148,plain, % 117.57/117.63 (~E(a3,f15(f6(f15(f4(a13)))))), % 117.57/117.63 inference(scs_inference,[],[4004,3697,4067,3954,3681,3827,3871,3916,3960,45,71,82,77,81,68,83,75,72,74,90,79,78,7,13,69,18,17,11,12,10,5,14,16,4,15,8,6,9,2,88,96,89,101,87,76,100,73,3])). % 117.57/117.63 cnf(4149,plain, % 117.57/117.63 (E(f10(f8(a25,a25),f8(a25,a25)),f8(f10(a25,a25),a25))), % 117.57/117.63 inference(scs_inference,[],[4004,3697,4067,3954,3681,3827,3871,3916,3960,45,41,71,82,77,81,68,83,75,72,74,90,79,78,7,13,69,18,17,11,12,10,5,14,16,4,15,8,6,9,2,88,96,89,101,87,76,100,73,3,110])). % 117.57/117.63 cnf(4177,plain, % 117.57/117.63 (~E(f15(f6(f15(f4(a28)))),a3)), % 117.57/117.63 inference(scs_inference,[],[3660,3689,71,82,68])). % 117.57/117.63 cnf(4183,plain, % 117.57/117.63 (P5(f6(f15(f4(a28))),f15(f6(f15(f4(a28)))))), % 117.57/117.63 inference(scs_inference,[],[3660,3689,71,82,68,77,81,83])). % 117.57/117.63 cnf(4197,plain, % 117.57/117.63 (P1(f15(f6(f15(f4(a28)))))), % 117.57/117.63 inference(scs_inference,[],[3660,3689,71,82,68,77,81,83,75,74,90,72,79,78,69])). % 117.57/117.63 cnf(4200,plain, % 117.57/117.63 (E(f10(x42001,f9(a27,f4(a28))),f10(x42001,a16))), % 117.57/117.63 inference(scs_inference,[],[3660,3701,3689,71,82,68,77,81,83,75,74,90,72,79,78,69,7,12])). % 117.57/117.63 cnf(4202,plain, % 117.57/117.63 (E(f10(f9(a27,f4(a28)),x42021),f10(a16,x42021))), % 117.57/117.63 inference(scs_inference,[],[3660,3701,3689,71,82,68,77,81,83,75,74,90,72,79,78,69,7,12,18,11])). % 117.57/117.63 cnf(4204,plain, % 117.57/117.63 (E(f7(x42041,f9(a27,f4(a28))),f7(x42041,a16))), % 117.57/117.63 inference(scs_inference,[],[3660,3701,3689,71,82,68,77,81,83,75,74,90,72,79,78,69,7,12,18,11,13,17])). % 117.57/117.63 cnf(4209,plain, % 117.57/117.63 (E(f11(f9(a27,f4(a28))),f11(a16))), % 117.57/117.63 inference(scs_inference,[],[3660,3701,3689,71,82,68,77,81,83,75,74,90,72,79,78,69,7,12,18,11,13,17,10,5,4,14,8])). % 117.57/117.63 cnf(4211,plain, % 117.57/117.63 (E(f7(f9(a27,f4(a28)),x42111),f7(a16,x42111))), % 117.57/117.63 inference(scs_inference,[],[3660,3701,3689,71,82,68,77,81,83,75,74,90,72,79,78,69,7,12,18,11,13,17,10,5,4,14,8,15,16])). % 117.57/117.63 cnf(4223,plain, % 117.57/117.63 (P1(f6(f15(f4(f2(a28)))))), % 117.57/117.63 inference(scs_inference,[],[3660,3701,3689,3941,3994,3916,45,71,82,68,77,81,83,75,74,90,72,79,78,69,7,12,18,11,13,17,10,5,4,14,8,15,16,6,9,2,88,89,101,96,73])). % 117.57/117.63 cnf(4231,plain, % 117.57/117.63 (E(f8(f5(a28,a28),a12),f11(a12))), % 117.57/117.63 inference(scs_inference,[],[3660,3701,3641,3689,3941,3994,3916,45,218,71,82,68,77,81,83,75,74,90,72,79,78,69,7,12,18,11,13,17,10,5,4,14,8,15,16,6,9,2,88,89,101,96,73,87,76,100,3])). % 117.57/117.63 cnf(4232,plain, % 117.57/117.63 (E(f10(f8(a22,a22),f8(a22,a22)),f8(f10(a22,a22),a22))), % 117.57/117.63 inference(scs_inference,[],[3660,3701,3641,3689,3941,3994,3916,45,218,37,71,82,68,77,81,83,75,74,90,72,79,78,69,7,12,18,11,13,17,10,5,4,14,8,15,16,6,9,2,88,89,101,96,73,87,76,100,3,110])). % 117.57/117.63 cnf(4242,plain, % 117.57/117.63 (P4(f10(f9(a13,f4(a28)),a12),f10(f9(a13,f4(a28)),f5(a1,a1)))), % 117.57/117.63 inference(scs_inference,[],[4020,4003,3660,3701,3641,3689,3941,3994,4024,3916,45,218,546,37,29,71,82,68,77,81,83,75,74,90,72,79,78,69,7,12,18,11,13,17,10,5,4,14,8,15,16,6,9,2,88,89,101,96,73,87,76,100,3,110,109,107,106,116,111])). % 117.57/117.63 cnf(4250,plain, % 117.57/117.63 (P2(f11(f11(f5(a1,a28))))), % 117.57/117.63 inference(scs_inference,[],[3741,71])). % 117.57/117.63 cnf(4258,plain, % 117.57/117.63 (P5(f6(f15(f4(a27))),f15(f6(f15(f4(a27)))))), % 117.57/117.63 inference(scs_inference,[],[3741,3789,71,82,81,75,83])). % 117.57/117.63 cnf(4260,plain, % 117.57/117.63 (~E(f15(f6(f15(f4(a27)))),a3)), % 117.57/117.63 inference(scs_inference,[],[3741,3789,71,82,81,75,83,68])). % 117.57/117.63 cnf(4272,plain, % 117.57/117.63 (P1(f15(f6(f15(f4(a27)))))), % 117.57/117.63 inference(scs_inference,[],[3741,3789,71,82,81,75,83,68,77,90,72,74,78,69])). % 117.57/117.63 cnf(4291,plain, % 117.57/117.63 (~E(a3,f15(f15(f15(f4(a28)))))), % 117.57/117.63 inference(scs_inference,[],[4231,3741,3789,4098,71,82,81,75,83,68,77,90,72,74,78,69,79,12,18,17,7,13,10,11,5,8,16,4,14,15,6,9,2])). % 117.57/117.63 cnf(4300,plain, % 117.57/117.63 (P1(f6(f15(f6(f4(a28)))))), % 117.57/117.63 inference(scs_inference,[],[4231,3741,3789,4034,4014,4098,45,71,82,81,75,83,68,77,90,72,74,78,69,79,12,18,17,7,13,10,11,5,8,16,4,14,15,6,9,2,88,101,89,96,73])). % 117.57/117.63 cnf(4306,plain, % 117.57/117.63 (E(f15(f6(f15(f6(f4(a28))))),f15(f6(f4(a28))))), % 117.57/117.63 inference(scs_inference,[],[4231,3741,3789,4034,4014,4098,45,71,82,81,75,83,68,77,90,72,74,78,69,79,12,18,17,7,13,10,11,5,8,16,4,14,15,6,9,2,88,101,89,96,73,100,87,76])). % 117.57/117.63 cnf(4327,plain, % 117.57/117.63 (P5(f4(f2(a1)),f4(a28))), % 117.57/117.63 inference(scs_inference,[],[4231,3741,3789,4034,3972,4014,4008,4242,4098,3593,45,164,43,71,82,81,75,83,68,77,90,72,74,78,69,79,12,18,17,7,13,10,11,5,8,16,4,14,15,6,9,2,88,101,89,96,73,100,87,76,3,21,110,109,107,106,116,111,119,121,1121,1126])). % 117.57/117.63 cnf(4330,plain, % 117.57/117.63 (P2(f11(f9(f2(a28),f4(a28))))), % 117.57/117.63 inference(scs_inference,[],[4061,71])). % 117.57/117.63 cnf(4336,plain, % 117.57/117.63 (~E(f15(f15(f15(f4(a13)))),a3)), % 117.57/117.63 inference(scs_inference,[],[4061,3862,71,82,75,68])). % 117.57/117.63 cnf(4350,plain, % 117.57/117.63 (P1(f15(f15(f15(f4(a13)))))), % 117.57/117.63 inference(scs_inference,[],[4061,3862,71,82,75,68,81,83,77,90,74,72,69])). % 117.57/117.63 cnf(4354,plain, % 117.57/117.63 (P4(f9(f2(a28),f4(a28)),f9(f2(a28),f4(a28)))), % 117.57/117.63 inference(scs_inference,[],[4061,3862,71,82,75,68,81,83,77,90,74,72,69,78,79])). % 117.57/117.63 cnf(4371,plain, % 117.57/117.63 (~E(f15(f6(f15(f4(a13)))),a3)), % 117.57/117.63 inference(scs_inference,[],[4061,3737,3862,4148,71,82,75,68,81,83,77,90,74,72,69,78,79,12,18,17,13,7,10,11,5,4,16,8,6,15,14,9,2])). % 117.57/117.63 cnf(4382,plain, % 117.57/117.63 (P1(f6(f15(f15(f15(f4(a28))))))), % 117.57/117.63 inference(scs_inference,[],[4061,3737,3862,4116,4148,4098,45,71,82,75,68,81,83,77,90,74,72,69,78,79,12,18,17,13,7,10,11,5,4,16,8,6,15,14,9,2,101,88,89,96,100,73])). % 117.57/117.63 cnf(4386,plain, % 117.57/117.63 (E(f8(f5(a1,a28),a12),f11(a12))), % 117.57/117.63 inference(scs_inference,[],[4061,3737,3862,4116,4148,4098,45,218,71,82,75,68,81,83,77,90,74,72,69,78,79,12,18,17,13,7,10,11,5,4,16,8,6,15,14,9,2,101,88,89,96,100,73,87,3])). % 117.57/117.63 cnf(4409,plain, % 117.57/117.63 (P2(f11(f9(a27,f4(a28))))), % 117.57/117.63 inference(scs_inference,[],[3598,71])). % 117.57/117.63 cnf(4431,plain, % 117.57/117.63 (P1(f15(f6(f15(f4(a13)))))), % 117.57/117.63 inference(scs_inference,[],[3598,3966,4065,71,82,68,83,75,77,81,72,74,90,78,69])). % 117.57/117.63 cnf(4433,plain, % 117.57/117.63 (P4(f9(a27,f4(a28)),f9(a27,f4(a28)))), % 117.57/117.63 inference(scs_inference,[],[3598,3966,4065,71,82,68,83,75,77,81,72,74,90,78,69,79])). % 117.57/117.63 cnf(4457,plain, % 117.57/117.63 (P1(f6(f15(f6(f15(f4(a28))))))), % 117.57/117.63 inference(scs_inference,[],[4386,3598,3966,4065,4197,4177,45,71,82,68,83,75,77,81,72,74,90,78,69,79,12,17,10,18,7,13,11,8,5,16,14,4,15,6,9,2,88,101,89,73])). % 117.57/117.63 cnf(4459,plain, % 117.57/117.63 (P2(f10(f9(a27,f4(a28)),f9(a27,f4(a28))))), % 117.57/117.63 inference(scs_inference,[],[4386,3598,3966,4065,4197,4177,45,71,82,68,83,75,77,81,72,74,90,78,69,79,12,17,10,18,7,13,11,8,5,16,14,4,15,6,9,2,88,101,89,73,87])). % 117.57/117.63 cnf(4466,plain, % 117.57/117.63 (P2(f5(f2(a1),f2(a28)))), % 117.57/117.63 inference(scs_inference,[],[4386,3598,3966,4049,4065,4197,4177,4056,45,378,127,329,71,82,68,83,75,77,81,72,74,90,78,69,79,12,17,10,18,7,13,11,8,5,16,14,4,15,6,9,2,88,101,89,73,87,96,100,3,98])). % 117.57/117.63 cnf(4479,plain, % 117.57/117.63 (~E(f15(f15(f6(f15(f4(a28))))),f15(a3))), % 117.57/117.63 inference(scs_inference,[],[4386,3598,3966,4049,4065,4197,4177,4056,45,28,378,207,127,329,71,82,68,83,75,77,81,72,74,90,78,69,79,12,17,10,18,7,13,11,8,5,16,14,4,15,6,9,2,88,101,89,73,87,96,100,3,98,110,107,109,106,116,22,84])). % 117.57/117.63 cnf(4494,plain, % 117.57/117.63 (~E(f15(f6(f15(f4(f2(a1))))),a3)), % 117.57/117.63 inference(scs_inference,[],[4466,4146,82,71,83,77,68])). % 117.57/117.63 cnf(4506,plain, % 117.57/117.63 (P1(f15(f6(f15(f4(f2(a1))))))), % 117.57/117.63 inference(scs_inference,[],[4466,4146,82,71,83,77,68,75,90,81,74,72,69])). % 117.57/117.63 cnf(4538,plain, % 117.57/117.63 (P1(f6(f15(f6(f15(f4(a27))))))), % 117.57/117.63 inference(scs_inference,[],[4466,3743,4146,4272,4260,45,82,71,83,77,68,75,90,81,74,72,69,78,79,12,13,10,17,11,18,7,14,6,16,4,8,5,15,9,2,101,88,89,100,96,73])). % 117.57/117.63 cnf(4542,plain, % 117.57/117.63 (E(f8(a12,f5(a1,a28)),f11(a12))), % 117.57/117.63 inference(scs_inference,[],[4466,3743,4146,4272,4260,45,218,82,71,83,77,68,75,90,81,74,72,69,78,79,12,13,10,17,11,18,7,14,6,16,4,8,5,15,9,2,101,88,89,100,96,73,87,3])). % 117.57/117.63 cnf(4544,plain, % 117.57/117.63 (P2(f5(a13,f2(a1)))), % 117.57/117.63 inference(scs_inference,[],[4466,3743,4354,3627,4146,4272,4260,3828,45,218,127,44,82,71,83,77,68,75,90,81,74,72,69,78,79,12,13,10,17,11,18,7,14,6,16,4,8,5,15,9,2,101,88,89,100,96,73,87,3,21,98])). % 117.57/117.63 cnf(4554,plain, % 117.57/117.63 (~E(f15(a3),f15(f15(f4(f2(a28)))))), % 117.57/117.63 inference(scs_inference,[],[4466,3743,4354,3627,4131,4146,4272,4260,3828,3941,45,28,218,257,127,44,82,71,83,77,68,75,90,81,74,72,69,78,79,12,13,10,17,11,18,7,14,6,16,4,8,5,15,9,2,101,88,89,100,96,73,87,3,21,98,107,110,109,106,84])). % 117.57/117.63 cnf(4573,plain, % 117.57/117.63 (~E(f15(f6(f15(f4(f2(a28))))),a3)), % 117.57/117.63 inference(scs_inference,[],[3802,4223,82,71,77,83,68])). % 117.57/117.63 cnf(4579,plain, % 117.57/117.63 (P4(a12,f8(f9(a28,f4(a27)),f9(a28,f4(a27))))), % 117.57/117.63 inference(scs_inference,[],[3802,4223,82,71,77,83,68,75,72,90])). % 117.57/117.63 cnf(4583,plain, % 117.57/117.63 (E(f8(f9(a28,f4(a27)),a12),a12)), % 117.57/117.63 inference(scs_inference,[],[3802,4223,82,71,77,83,68,75,72,90,81,74])). % 117.57/117.63 cnf(4585,plain, % 117.57/117.63 (P1(f15(f6(f15(f4(f2(a28))))))), % 117.57/117.63 inference(scs_inference,[],[3802,4223,82,71,77,83,68,75,72,90,81,74,69])). % 117.57/117.63 cnf(4609,plain, % 117.57/117.63 (P2(f8(f9(a28,f4(a27)),f9(a28,f4(a27))))), % 117.57/117.63 inference(scs_inference,[],[4542,3802,4223,4554,82,71,77,83,68,75,72,90,81,74,69,78,79,12,17,11,10,13,18,7,14,8,4,16,6,5,15,9,2,101,88])). % 117.57/117.63 cnf(4617,plain, % 117.57/117.63 (P1(f6(f15(f6(f15(f4(a13))))))), % 117.57/117.63 inference(scs_inference,[],[4542,3802,4223,4431,4371,4554,45,82,71,77,83,68,75,72,90,81,74,69,78,79,12,17,11,10,13,18,7,14,8,4,16,6,5,15,9,2,101,88,89,96,100,73])). % 117.57/117.63 cnf(4634,plain, % 117.57/117.63 (P4(f8(f9(a28,f4(a27)),a12),f8(f9(a28,f4(a27)),f8(f9(a13,f4(a28)),f9(a13,f4(a28)))))), % 117.57/117.63 inference(scs_inference,[],[4542,3802,4050,4028,4223,4431,4371,4554,4142,3799,45,316,131,29,82,71,77,83,68,75,72,90,81,74,69,78,79,12,17,11,10,13,18,7,14,8,4,16,6,5,15,9,2,101,88,89,96,100,73,87,3,107,109,110,106,104,116,112])). % 117.57/117.63 cnf(4644,plain, % 117.57/117.63 (P5(f6(f15(f6(f4(a28)))),f15(f6(f15(f6(f4(a28))))))), % 117.57/117.63 inference(scs_inference,[],[4544,4300,82,71,83])). % 117.57/117.63 cnf(4650,plain, % 117.57/117.63 (~E(f15(f6(f15(f6(f4(a28))))),a3)), % 117.57/117.63 inference(scs_inference,[],[4544,4300,82,71,83,77,75,68])). % 117.57/117.63 cnf(4660,plain, % 117.57/117.63 (P1(f15(f6(f15(f6(f4(a28))))))), % 117.57/117.63 inference(scs_inference,[],[4544,4300,82,71,83,77,75,68,72,74,90,81,69])). % 117.57/117.63 cnf(4692,plain, % 117.57/117.63 (P1(f6(f15(f15(f15(f4(a13))))))), % 117.57/117.63 inference(scs_inference,[],[4544,4074,4300,4350,4336,45,82,71,83,77,75,68,72,74,90,81,69,78,79,12,10,11,13,17,18,7,14,16,6,4,5,8,15,2,9,101,88,100,96,89,73])). % 117.57/117.63 cnf(4696,plain, % 117.57/117.63 (E(f10(f11(f5(a28,a28)),f5(a28,a28)),f11(a12))), % 117.57/117.63 inference(scs_inference,[],[4544,4074,3669,4300,4350,4336,45,218,82,71,83,77,75,68,72,74,90,81,69,78,79,12,10,11,13,17,18,7,14,16,6,4,5,8,15,2,9,101,88,100,96,89,73,87,3])). % 117.57/117.63 cnf(4697,plain, % 117.57/117.63 (P2(f11(a16))), % 117.57/117.63 inference(scs_inference,[],[4544,4074,3669,4209,4409,4300,4350,4336,45,218,82,71,83,77,75,68,72,74,90,81,69,78,79,12,10,11,13,17,18,7,14,16,6,4,5,8,15,2,9,101,88,100,96,89,73,87,3,20])). % 117.57/117.63 cnf(4700,plain, % 117.57/117.63 (E(f10(f8(a21,a21),f8(a21,a21)),f8(a21,f10(a21,a21)))), % 117.57/117.63 inference(scs_inference,[],[4544,4074,3669,4209,4409,4300,4350,4336,45,218,36,82,71,83,77,75,68,72,74,90,81,69,78,79,12,10,11,13,17,18,7,14,16,6,4,5,8,15,2,9,101,88,100,96,89,73,87,3,20,107,109])). % 117.57/117.63 cnf(4724,plain, % 117.57/117.63 (P2(f11(f11(a16)))), % 117.57/117.63 inference(scs_inference,[],[4697,82,71])). % 117.57/117.63 cnf(4726,plain, % 117.57/117.63 (E(f10(f11(a16),a12),f11(a16))), % 117.57/117.63 inference(scs_inference,[],[4697,82,71,77])). % 117.57/117.63 cnf(4730,plain, % 117.57/117.63 (~E(f15(f6(f15(f15(f15(f4(a28)))))),a3)), % 117.57/117.63 inference(scs_inference,[],[4697,4382,4065,82,71,77,83,68])). % 117.57/117.63 cnf(4732,plain, % 117.57/117.63 (E(f8(a12,f11(a16)),a12)), % 117.57/117.63 inference(scs_inference,[],[4697,4382,4065,82,71,77,83,68,75])). % 117.57/117.63 cnf(4736,plain, % 117.57/117.63 (E(f8(f11(a16),a12),a12)), % 117.57/117.63 inference(scs_inference,[],[4697,4382,4065,82,71,77,83,68,75,81,74])). % 117.57/117.63 cnf(4744,plain, % 117.57/117.63 (P4(f11(a16),f11(a16))), % 117.57/117.63 inference(scs_inference,[],[4697,4382,4065,82,71,77,83,68,75,81,74,72,90,69,79])). % 117.57/117.63 cnf(4746,plain, % 117.57/117.63 (E(f10(a12,f11(a16)),f11(a16))), % 117.57/117.63 inference(scs_inference,[],[4697,4382,4065,82,71,77,83,68,75,81,74,72,90,69,79,78])). % 117.57/117.63 cnf(4764,plain, % 117.57/117.63 (E(f11(f8(f11(a16),f11(a16))),f8(f11(f11(a16)),f11(a16)))), % 117.57/117.63 inference(scs_inference,[],[4697,4696,4479,4382,4065,82,71,77,83,68,75,81,74,72,90,69,79,78,12,13,17,11,10,18,7,14,4,5,6,16,8,15,9,2,101])). % 117.57/117.63 cnf(4766,plain, % 117.57/117.63 (P2(f8(f11(a16),f11(a16)))), % 117.57/117.63 inference(scs_inference,[],[4697,4696,4479,4382,4065,82,71,77,83,68,75,81,74,72,90,69,79,78,12,13,17,11,10,18,7,14,4,5,6,16,8,15,9,2,101,88])). % 117.57/117.63 cnf(4776,plain, % 117.57/117.63 (P2(f10(f11(a16),f11(a16)))), % 117.57/117.63 inference(scs_inference,[],[4697,4696,4479,4382,4506,4494,4065,45,82,71,77,83,68,75,81,74,72,90,69,79,78,12,13,17,11,10,18,7,14,4,5,6,16,8,15,9,2,101,88,89,96,100,73,87])). % 117.57/117.63 cnf(4798,plain, % 117.57/117.63 (P2(f11(f8(f11(a16),f11(a16))))), % 117.57/117.63 inference(scs_inference,[],[4766,82,71])). % 117.57/117.63 cnf(4806,plain, % 117.57/117.63 (~E(f15(f6(f15(f6(f15(f4(a28)))))),a3)), % 117.57/117.63 inference(scs_inference,[],[4766,4457,4116,82,71,77,83,75,68])). % 117.57/117.63 cnf(4855,plain, % 117.57/117.63 (E(f10(f8(a20,a20),f8(a20,a20)),f8(a20,f10(a20,a20)))), % 117.57/117.63 inference(scs_inference,[],[4726,4766,4732,4457,4585,4573,4730,4116,45,218,35,82,71,77,83,75,68,74,90,72,69,81,79,78,12,13,11,10,17,7,14,18,5,4,16,8,6,15,2,9,101,89,88,96,100,73,87,3,107,109])). % 117.57/117.63 cnf(4857,plain, % 117.57/117.63 (E(f10(f8(a23,a23),f8(a23,a23)),f8(f10(a23,a23),a23))), % 117.57/117.63 inference(scs_inference,[],[4726,4766,4732,4457,4585,4573,4730,4116,45,218,38,35,82,71,77,83,75,68,74,90,72,69,81,79,78,12,13,11,10,17,7,14,18,5,4,16,8,6,15,2,9,101,89,88,96,100,73,87,3,107,109,110])). % 117.57/117.63 cnf(4874,plain, % 117.57/117.63 (~E(f15(f6(f15(f6(f15(f4(a27)))))),a3)), % 117.57/117.63 inference(scs_inference,[],[4724,4538,82,71,68])). % 117.57/117.63 cnf(4880,plain, % 117.57/117.63 (P5(f15(f6(f15(f4(a27)))),f15(f15(f6(f15(f4(a27))))))), % 117.57/117.63 inference(scs_inference,[],[4724,4538,4272,82,71,68,77,75,83])). % 117.57/117.63 cnf(4942,plain, % 117.57/117.63 (E(f8(f11(a16),a12),f11(a12))), % 117.57/117.63 inference(scs_inference,[],[4744,4746,4724,4736,4609,4579,4538,4660,4650,4806,4272,4697,45,218,196,44,82,71,68,77,75,83,90,81,74,69,72,79,78,12,13,10,11,17,14,7,18,4,5,8,6,16,9,15,2,101,88,89,73,96,100,87,107,109,110,106,104,116,111,119,3])). % 117.57/117.63 cnf(4951,plain, % 117.57/117.63 (P2(f11(f10(f11(a16),f11(a16))))), % 117.57/117.63 inference(scs_inference,[],[4776,82,71])). % 117.57/117.63 cnf(5003,plain, % 117.57/117.63 (P2(f5(a28,a1))), % 117.57/117.63 inference(scs_inference,[],[4942,4776,4617,4874,4350,45,43,46,42,82,71,77,75,68,83,90,81,74,72,69,79,78,12,13,11,17,10,18,14,7,4,5,16,2,15,6,8,9,101,88,89,96,100,87,98])). % 117.57/117.63 cnf(5013,plain, % 117.57/117.63 (~E(f15(f15(f15(f15(f4(a13))))),f15(a3))), % 117.57/117.63 inference(scs_inference,[],[4942,4776,4617,4874,4350,4336,45,28,243,43,46,42,82,71,77,75,68,83,90,81,74,72,69,79,78,12,13,11,17,10,18,14,7,4,5,16,2,15,6,8,9,101,88,89,96,100,87,98,109,107,106,110,84])). % 117.57/117.63 cnf(5023,plain, % 117.57/117.63 (E(f10(f11(f5(a28,a1)),f5(a28,a1)),a12)), % 117.57/117.63 inference(scs_inference,[],[5003,82])). % 117.57/117.63 cnf(5027,plain, % 117.57/117.63 (E(f8(a12,f5(a28,a1)),a12)), % 117.57/117.63 inference(scs_inference,[],[5003,4692,82,68,75])). % 117.57/117.63 cnf(5029,plain, % 117.57/117.63 (P2(f11(f5(a28,a1)))), % 117.57/117.63 inference(scs_inference,[],[5003,4692,82,68,75,71])). % 117.57/117.63 cnf(5031,plain, % 117.57/117.63 (E(f10(f5(a28,a1),a12),f5(a28,a1))), % 117.57/117.63 inference(scs_inference,[],[5003,4692,82,68,75,71,77])). % 117.57/117.63 cnf(5039,plain, % 117.57/117.63 (E(f8(f5(a28,a1),a12),a12)), % 117.57/117.63 inference(scs_inference,[],[5003,4692,4431,82,68,75,71,77,90,83,81,74])). % 117.57/117.63 cnf(5065,plain, % 117.57/117.63 (P2(f8(f5(a28,a1),f5(a28,a1)))), % 117.57/117.63 inference(scs_inference,[],[5003,3893,5013,4692,4431,82,68,75,71,77,90,83,81,74,69,72,79,78,12,13,10,17,11,7,18,14,4,5,15,8,16,9,2,6,88])). % 117.57/117.63 cnf(5067,plain, % 117.57/117.63 (E(f11(f8(f5(a28,a1),f5(a28,a1))),f8(f11(f5(a28,a1)),f5(a28,a1)))), % 117.57/117.63 inference(scs_inference,[],[5003,3893,5013,4692,4431,82,68,75,71,77,90,83,81,74,69,72,79,78,12,13,10,17,11,7,18,14,4,5,15,8,16,9,2,6,88,101])). % 117.57/117.63 cnf(5075,plain, % 117.57/117.63 (P2(f10(f5(a28,a1),f5(a28,a1)))), % 117.57/117.63 inference(scs_inference,[],[5003,3893,5013,4692,4431,45,82,68,75,71,77,90,83,81,74,69,72,79,78,12,13,10,17,11,7,18,14,4,5,15,8,16,9,2,6,88,101,96,89,100,87])). % 117.57/117.63 cnf(5077,plain, % 117.57/117.63 (P2(f5(a13,f2(a28)))), % 117.57/117.63 inference(scs_inference,[],[5003,3893,5013,4692,4431,4067,45,44,329,82,68,75,71,77,90,83,81,74,69,72,79,78,12,13,10,17,11,7,18,14,4,5,15,8,16,9,2,6,88,101,96,89,100,87,98])). % 117.57/117.63 cnf(5087,plain, % 117.57/117.63 (~E(f15(a3),f15(f15(f15(f15(f4(a28))))))), % 117.57/117.63 inference(scs_inference,[],[5003,3893,4291,5013,4692,4431,4116,4067,45,28,44,329,82,68,75,71,77,90,83,81,74,69,72,79,78,12,13,10,17,11,7,18,14,4,5,15,8,16,9,2,6,88,101,96,89,100,87,98,107,109,110,106,84])). % 117.57/117.63 cnf(5093,plain, % 117.57/117.63 (P2(f8(f11(f5(a28,a28)),f5(a28,a28)))), % 117.57/117.63 inference(scs_inference,[],[5003,3893,3837,3685,4291,5013,4692,4431,4116,4067,45,28,44,329,82,68,75,71,77,90,83,81,74,69,72,79,78,12,13,10,17,11,7,18,14,4,5,15,8,16,9,2,6,88,101,96,89,100,87,98,107,109,110,106,84,116,73,20])). % 117.57/117.63 cnf(5099,plain, % 117.57/117.63 (~E(f15(f15(f6(f15(f4(f2(a1)))))),a3)), % 117.57/117.63 inference(scs_inference,[],[5065,4506,82,68])). % 117.57/117.63 cnf(5105,plain, % 117.57/117.63 (P2(f11(f8(f5(a28,a1),f5(a28,a1))))), % 117.57/117.63 inference(scs_inference,[],[5065,4506,82,68,75,77,71])). % 117.57/117.63 cnf(5156,plain, % 117.57/117.63 (E(f10(f8(a20,a20),f8(a20,a20)),f8(f10(a20,a20),a20))), % 117.57/117.63 inference(scs_inference,[],[5031,5065,5027,5087,4506,4197,218,35,306,82,68,75,77,71,90,83,72,69,81,74,79,78,12,13,10,7,11,17,18,5,4,14,15,2,9,16,6,8,101,88,96,100,87,3,107,109,106,110])). % 117.57/117.63 cnf(5175,plain, % 117.57/117.63 (~E(f15(f15(f6(f15(f4(f2(a28)))))),a3)), % 117.57/117.63 inference(scs_inference,[],[5029,4585,82,77,75,68])). % 117.57/117.63 cnf(5177,plain, % 117.57/117.63 (P2(f11(f11(f5(a28,a1))))), % 117.57/117.63 inference(scs_inference,[],[5029,4585,82,77,75,68,71])). % 117.57/117.63 cnf(5249,plain, % 117.57/117.63 (P2(f11(f5(a13,f2(a28))))), % 117.57/117.63 inference(scs_inference,[],[5077,4660,3827,82,68,75,77,83,71])). % 117.57/117.63 cnf(5310,plain, % 117.57/117.63 (~E(f15(f15(f6(f15(f4(a27))))),a3)), % 117.57/117.63 inference(scs_inference,[],[5093,4272,82,68])). % 117.57/117.63 cnf(5324,plain, % 117.57/117.63 (P1(f15(f15(f6(f15(f4(a27))))))), % 117.57/117.63 inference(scs_inference,[],[5093,4272,4034,82,68,75,77,71,83,72,90,69])). % 117.57/117.63 cnf(5370,plain, % 117.57/117.63 (E(f10(f8(a19,a19),f8(a19,a19)),f8(f10(a19,a19),a19))), % 117.57/117.63 inference(scs_inference,[],[5039,5093,4583,3693,4183,4634,5099,5075,4272,4034,34,82,68,75,77,71,83,72,90,69,81,74,79,78,12,13,7,10,17,11,4,18,15,14,5,16,6,2,9,8,73,88,101,96,100,87,25,21,109,106,107,110])). % 117.57/117.63 cnf(5387,plain, % 117.57/117.63 (~E(f15(f15(f15(f6(f15(f4(a27)))))),a3)), % 117.57/117.63 inference(scs_inference,[],[3912,5324,82,77,75,68])). % 117.57/117.63 cnf(5435,plain, % 117.57/117.63 (E(f10(f11(f5(a28,a1)),f5(a28,a1)),f11(a12))), % 117.57/117.63 inference(scs_inference,[],[4857,5023,3912,5324,5310,3795,3577,45,218,82,77,75,68,71,72,83,90,69,74,81,79,78,12,13,7,10,11,4,17,14,15,18,16,6,5,2,9,8,89,88,101,96,100,87,3])). % 117.57/117.63 cnf(5436,plain, % 117.57/117.63 (E(f10(f8(a18,a18),f8(a18,a18)),f8(a18,f10(a18,a18)))), % 117.57/117.63 inference(scs_inference,[],[4857,5023,3912,5324,5310,3795,3577,45,218,33,82,77,75,68,71,72,83,90,69,74,81,79,78,12,13,7,10,11,4,17,14,15,18,16,6,5,2,9,8,89,88,101,96,100,87,3,109])). % 117.57/117.63 cnf(5442,plain, % 117.57/117.63 (E(f10(f8(a17,a17),f8(a17,a17)),f8(f10(a17,a17),a17))), % 117.57/117.63 inference(scs_inference,[],[4857,5023,3912,5324,5310,3795,3577,45,218,32,33,82,77,75,68,71,72,83,90,69,74,81,79,78,12,13,7,10,11,4,17,14,15,18,16,6,5,2,9,8,89,88,101,96,100,87,3,109,106,107,110])). % 117.57/117.63 cnf(5472,plain, % 117.57/117.63 (P1(f15(f15(f6(f15(f4(a13))))))), % 117.57/117.63 inference(scs_inference,[],[4006,4431,3735,82,68,75,77,71,83,72,69])). % 117.57/117.63 cnf(5513,plain, % 117.57/117.63 (P2(f5(f2(a28),f2(a1)))), % 117.57/117.63 inference(scs_inference,[],[5435,4006,5105,5067,5175,3699,4431,3735,137,127,329,82,68,75,77,71,83,72,69,90,81,74,79,78,12,13,7,10,4,17,11,18,14,15,5,6,16,2,9,8,73,88,101,96,100,87,20,98])). % 117.57/117.63 cnf(5515,plain, % 117.57/117.63 (E(f10(f8(a16,a16),f8(a16,a16)),f8(a16,f10(a16,a16)))), % 117.57/117.63 inference(scs_inference,[],[5435,4006,5105,5067,5175,3699,4431,3735,137,127,329,31,82,68,75,77,71,83,72,69,90,81,74,79,78,12,13,7,10,4,17,11,18,14,15,5,6,16,2,9,8,73,88,101,96,100,87,20,98,109])). % 117.57/117.63 cnf(5535,plain, % 117.57/117.63 (~E(f15(f15(f15(f6(f15(f4(a13)))))),a3)), % 117.57/117.63 inference(scs_inference,[],[5513,5472,82,68])). % 117.57/117.63 cnf(5543,plain, % 117.57/117.63 (P2(f11(f5(f2(a28),f2(a1))))), % 117.57/117.63 inference(scs_inference,[],[5513,5472,3941,82,68,77,75,83,71])). % 117.57/117.63 cnf(5752,plain, % 117.57/117.63 (~E(f15(f15(f6(f15(f4(a28))))),a3)), % 117.57/117.63 inference(scs_inference,[],[5543,4197,82,77,75,68])). % 117.57/117.63 cnf(5758,plain, % 117.57/117.63 (P1(f15(f15(f6(f15(f4(a28))))))), % 117.57/117.63 inference(scs_inference,[],[5543,4197,28,82,77,75,68,83,71,69])). % 117.57/117.63 cnf(5788,plain, % 117.57/117.63 (P2(f9(a27,f4(f2(a28))))), % 117.57/117.63 inference(scs_inference,[],[4232,5543,5387,3736,4197,28,45,82,77,75,68,83,71,69,74,72,81,90,79,78,12,13,7,4,10,17,11,18,2,14,5,9,6,16,15,8,89])). % 117.57/117.63 cnf(5821,plain, % 117.57/117.63 (~E(f15(f15(f15(f6(f15(f4(a28)))))),a3)), % 117.57/117.63 inference(scs_inference,[],[4951,5758,82,75,68])). % 117.57/117.63 cnf(5869,plain, % 117.57/117.63 (E(f10(f9(a27,f4(a28)),f9(a27,f4(a28))),f10(a16,a16))), % 117.57/117.63 inference(scs_inference,[],[4149,4200,4202,4951,5758,5752,5075,3797,45,82,75,68,77,71,69,74,72,90,81,79,78,12,13,7,4,17,10,11,18,2,14,16,5,6,9,15,8,89,101,88,96,100,87,3])). % 117.57/117.63 cnf(5886,plain, % 117.57/117.63 (~E(f15(f15(f15(f15(f4(a13))))),a3)), % 117.57/117.63 inference(scs_inference,[],[5177,4350,82,68])). % 117.57/117.63 cnf(5894,plain, % 117.57/117.63 (P1(f15(f15(f15(f15(f4(a13))))))), % 117.57/117.63 inference(scs_inference,[],[5177,4350,82,68,75,77,71,69])). % 117.57/117.63 cnf(5939,plain, % 117.57/117.63 (P2(f8(f11(f11(a16)),f11(a16)))), % 117.57/117.63 inference(scs_inference,[],[4855,5177,4798,4764,3787,5535,4880,4506,4350,3697,1332,45,82,68,75,77,71,69,72,74,81,90,79,78,12,13,7,4,11,17,10,18,2,14,5,9,6,16,15,8,24,73,89,101,88,96,87,100,20])). % 117.57/117.63 cnf(6014,plain, % 117.57/117.63 (~E(f15(f15(f15(f15(f15(f4(a13)))))),f15(a3))), % 117.57/117.63 inference(scs_inference,[],[4700,5939,4204,4211,5894,5886,28,1345,45,82,68,75,77,71,74,72,69,81,90,79,78,12,13,7,17,4,11,10,18,2,14,6,5,16,9,15,8,89,101,88,96,100,87,3,106,107,84])). % 117.57/117.63 cnf(6070,plain, % 117.57/117.63 (P1(f6(f15(f15(f6(f4(a1))))))), % 117.57/117.63 inference(scs_inference,[],[5156,4330,6014,4585,3778,45,82,68,75,77,71,74,72,69,81,90,79,78,12,13,7,17,4,11,10,18,14,2,6,15,5,9,16,8,89,73])). % 117.57/117.63 cnf(6174,plain, % 117.57/117.63 (~E(f15(f6(f15(f15(f6(f4(a1)))))),a3)), % 117.57/117.63 inference(scs_inference,[],[4250,6070,82,77,68])). % 117.57/117.63 cnf(6300,plain, % 117.57/117.63 (~E(f15(f15(f4(f2(a1)))),a3)), % 117.57/117.63 inference(scs_inference,[],[5249,3827,82,77,68])). % 117.57/117.63 cnf(6308,plain, % 117.57/117.63 (P1(f15(f15(f4(f2(a1)))))), % 117.57/117.63 inference(scs_inference,[],[5249,3827,82,77,68,75,71,72,69])). % 117.57/117.63 cnf(6338,plain, % 117.57/117.63 (P1(f6(f15(f15(f4(f2(a1))))))), % 117.57/117.63 inference(scs_inference,[],[5436,5249,5821,4660,3827,45,82,77,68,75,71,72,69,90,74,81,79,78,12,17,4,13,7,10,11,18,6,2,16,14,5,15,9,8,89,73])). % 117.57/117.63 cnf(6346,plain, % 117.57/117.63 (E(f8(f11(a26),f11(a26)),f8(a26,a26))), % 117.57/117.63 inference(scs_inference,[],[5436,5249,5821,4660,3827,45,40,82,77,68,75,71,72,69,90,74,81,79,78,12,17,4,13,7,10,11,18,6,2,16,14,5,15,9,8,89,73,101,88,87,96])). % 117.57/117.63 cnf(6348,plain, % 117.57/117.63 (P2(f10(a16,a16))), % 117.57/117.63 inference(scs_inference,[],[5436,5249,5869,4459,5821,4660,3827,45,40,82,77,68,75,71,72,69,90,74,81,79,78,12,17,4,13,7,10,11,18,6,2,16,14,5,15,9,8,89,73,101,88,87,96,20])). % 117.57/117.63 cnf(6367,plain, % 117.57/117.63 (E(f10(f11(f10(a16,a16)),f10(a16,a16)),a12)), % 117.57/117.63 inference(scs_inference,[],[6348,82])). % 117.57/117.63 cnf(6369,plain, % 117.57/117.63 (E(f10(f10(a16,a16),a12),f10(a16,a16))), % 117.57/117.63 inference(scs_inference,[],[6348,82,77])). % 117.57/117.63 cnf(6371,plain, % 117.57/117.63 (~E(f15(f15(f15(f4(f2(a1))))),a3)), % 117.57/117.63 inference(scs_inference,[],[6348,6308,82,77,68])). % 117.57/117.63 cnf(6375,plain, % 117.57/117.63 (P2(f11(f10(a16,a16)))), % 117.57/117.63 inference(scs_inference,[],[6348,6308,82,77,68,75,71])). % 117.57/117.63 cnf(6379,plain, % 117.57/117.63 (E(f8(f10(a16,a16),a12),a12)), % 117.57/117.63 inference(scs_inference,[],[6348,6308,82,77,68,75,71,72,74])). % 117.57/117.63 cnf(6381,plain, % 117.57/117.63 (P1(f15(f15(f15(f4(f2(a1))))))), % 117.57/117.63 inference(scs_inference,[],[6348,6308,82,77,68,75,71,72,74,69])). % 117.57/117.63 cnf(6387,plain, % 117.57/117.63 (E(f10(a12,f10(a16,a16)),f10(a16,a16))), % 117.57/117.63 inference(scs_inference,[],[6348,6308,82,77,68,75,71,72,74,69,90,81,78])). % 117.57/117.63 cnf(6415,plain, % 117.57/117.63 (P2(f10(f10(a16,a16),f10(a16,a16)))), % 117.57/117.63 inference(scs_inference,[],[6348,6346,6308,6300,45,82,77,68,75,71,72,74,69,90,81,78,79,12,4,17,7,13,10,11,18,6,2,5,16,15,9,14,8,89,73,88,101,87])). % 117.57/117.63 cnf(6440,plain, % 117.57/117.63 (P2(f11(f10(f10(a16,a16),f10(a16,a16))))), % 117.57/117.63 inference(scs_inference,[],[6415,6338,82,77,68,75,71])). % 117.57/117.63 cnf(6488,plain, % 117.57/117.63 (~E(f15(f15(f15(f15(f4(f2(a1)))))),f15(a3))), % 117.57/117.63 inference(scs_inference,[],[6369,6415,6338,6381,6371,28,45,82,77,68,75,71,74,72,69,90,81,78,79,12,17,4,13,7,10,18,11,6,5,2,9,16,14,15,8,89,101,88,87,96,100,106,107,84])). % 117.57/117.63 cnf(6507,plain, % 117.57/117.63 (P2(f11(f11(f10(a16,a16))))), % 117.57/117.63 inference(scs_inference,[],[6375,6381,82,68,77,75,71])). % 117.57/117.63 cnf(6543,plain, % 117.57/117.63 (P2(f10(f11(f10(a16,a16)),f11(f10(a16,a16))))), % 117.57/117.63 inference(scs_inference,[],[6387,6375,6488,6381,82,68,77,75,71,74,72,69,81,90,79,78,12,17,13,4,10,7,18,6,11,5,9,2,16,15,8,14,101,88,87])). % 117.57/117.63 cnf(6566,plain, % 117.57/117.63 (~E(f15(f15(f6(f4(a28)))),a3)), % 117.57/117.63 inference(scs_inference,[],[6440,4034,82,77,68])). % 117.57/117.63 cnf(6574,plain, % 117.57/117.63 (P1(f15(f15(f6(f4(a28)))))), % 117.57/117.63 inference(scs_inference,[],[6440,4034,82,77,68,75,71,74,69])). % 117.57/117.63 cnf(6654,plain, % 117.57/117.63 (E(f10(x66541,f8(f10(a16,a16),a12)),f10(x66541,a12))), % 117.57/117.63 inference(scs_inference,[],[6379,6507,6574,82,77,68,75,71,74,69,72,90,81,78,79,12])). % 117.57/117.63 cnf(6661,plain, % 117.57/117.63 (E(f10(f8(f10(a16,a16),a12),x66611),f10(a12,x66611))), % 117.57/117.63 inference(scs_inference,[],[6379,6507,6574,82,77,68,75,71,74,69,72,90,81,78,79,12,17,4,13,18,7,10,11])). % 117.57/117.63 cnf(6684,plain, % 117.57/117.63 (E(f8(f10(a16,a16),a12),f11(a12))), % 117.57/117.63 inference(scs_inference,[],[6379,6507,6574,6566,218,41,45,82,77,68,75,71,74,69,72,90,81,78,79,12,17,4,13,18,7,10,11,6,5,2,15,9,8,16,14,89,73,101,88,87,96,100,3])). % 117.57/117.63 cnf(6833,plain, % 117.57/117.63 (~E(f15(f15(f4(a28))),a3)), % 117.57/117.63 inference(scs_inference,[],[3970,3577,82,77,75,68])). % 117.57/117.63 cnf(6843,plain, % 117.57/117.63 (P1(f15(f15(f15(f15(f4(a28))))))), % 117.57/117.63 inference(scs_inference,[],[3970,4116,3577,82,77,75,68,71,72,74,90,69])). % 117.57/117.63 cnf(6867,plain, % 117.57/117.63 (E(f15(f6(f15(f15(f4(a28))))),f15(f15(f4(a28))))), % 117.57/117.63 inference(scs_inference,[],[6684,3970,6174,4116,3577,3681,82,77,75,68,71,72,74,90,69,81,78,79,12,17,13,18,4,7,10,6,5,11,15,2,8,9,16,14,76])). % 117.57/117.63 cnf(6929,plain, % 117.57/117.63 (~E(a3,f15(f15(f4(a28))))), % 117.57/117.63 inference(scs_inference,[],[5442,5788,6833,6843,82,77,75,68,71,72,74,90,69,81,78,79,12,17,13,4,18,7,10,6,5,11,15,2])). % 117.57/117.63 cnf(6936,plain, % 117.57/117.63 (P1(f6(f15(f15(f4(a28)))))), % 117.57/117.63 inference(scs_inference,[],[5442,5788,6833,6843,3681,45,82,77,75,68,71,72,74,90,69,81,78,79,12,17,13,4,18,7,10,6,5,11,15,2,8,16,9,14,89,73])). % 117.57/117.63 cnf(6953,plain, % 117.57/117.63 (~E(f15(f4(a28)),f15(a3))), % 117.57/117.63 inference(scs_inference,[],[5442,5788,6833,6843,6867,3826,3681,3593,28,257,45,82,77,75,68,71,72,74,90,69,81,78,79,12,17,13,4,18,7,10,6,5,11,15,2,8,16,9,14,89,73,101,88,87,96,100,3,106,107,84])). % 117.57/117.63 cnf(6976,plain, % 117.57/117.63 (P1(f15(f6(f15(f15(f4(a28))))))), % 117.57/117.63 inference(scs_inference,[],[3962,6936,82,77,75,68,71,72,69])). % 117.57/117.63 cnf(6999,plain, % 117.57/117.63 (~E(f15(a3),f15(f4(a28)))), % 117.57/117.63 inference(scs_inference,[],[6953,5370,3962,6936,82,77,75,68,71,72,69,74,90,81,78,79,12,13,4,17,18,7,6,10,5,11,15,2])). % 117.57/117.63 cnf(7012,plain, % 117.57/117.63 (P2(f8(f10(f5(a28,a28),f5(a28,a28)),f5(a28,a28)))), % 117.57/117.63 inference(scs_inference,[],[6953,5370,3962,6936,3883,3708,316,43,82,77,75,68,71,72,69,74,90,81,78,79,12,13,4,17,18,7,6,10,5,11,15,2,8,9,16,14,89,73,101,88,20])). % 117.57/117.63 cnf(7019,plain, % 117.57/117.63 (E(f10(f11(f10(a16,a16)),f10(a16,a16)),f11(a12))), % 117.57/117.63 inference(scs_inference,[],[6953,5370,6367,3962,6936,3883,3708,218,316,43,82,77,75,68,71,72,69,74,90,81,78,79,12,13,4,17,18,7,6,10,5,11,15,2,8,9,16,14,89,73,101,88,20,87,96,100,3])). % 117.57/117.63 cnf(7024,plain, % 117.57/117.63 (~E(f15(a3),f15(f15(f15(f4(a28)))))), % 117.57/117.63 inference(scs_inference,[],[6953,5370,6367,6929,3962,6936,3883,3708,3681,218,28,316,43,82,77,75,68,71,72,69,74,90,81,78,79,12,13,4,17,18,7,6,10,5,11,15,2,8,9,16,14,89,73,101,88,20,87,96,100,3,106,107,84])). % 117.57/117.63 cnf(7040,plain, % 117.57/117.63 (P2(f11(f8(f10(f5(a28,a28),f5(a28,a28)),f5(a28,a28))))), % 117.57/117.63 inference(scs_inference,[],[7012,6976,82,77,75,68,71])). % 117.57/117.63 cnf(7084,plain, % 117.57/117.63 (~E(f15(a3),f15(f15(f4(a27))))), % 117.57/117.63 inference(scs_inference,[],[6999,7019,7012,7024,6976,3647,164,43,82,77,75,68,71,72,69,90,74,81,78,79,12,4,13,17,18,7,10,6,5,11,8,15,2,9,16,14,89,101,88,87,96,100,3])). % 117.57/117.63 cnf(7099,plain, % 117.57/117.63 (~E(f15(f15(f4(a13))),a3)), % 117.57/117.63 inference(scs_inference,[],[3735,68])). % 117.57/117.63 cnf(7135,plain, % 117.57/117.63 (P1(f15(f15(f4(f2(a28)))))), % 117.57/117.63 inference(scs_inference,[],[5515,7084,6543,3735,3941,68,2,9,17,13,74,16,18,14,82,81,78,12,10,7,6,71,72,11,79,8,5,15,90,77,4,69])). % 117.57/117.63 cnf(7148,plain, % 117.57/117.63 (P1(f6(f15(f15(f4(a13)))))), % 117.57/117.63 inference(scs_inference,[],[5515,6654,6661,7084,6543,6381,3735,3941,3862,546,45,68,2,9,17,13,74,16,18,14,82,81,78,12,10,7,6,71,72,11,79,8,5,15,90,77,4,69,75,89,88,101,3,73])). % 117.57/117.63 cnf(7227,plain, % 117.57/117.63 (E(f8(f11(a12),f11(a12)),f8(a12,a12))), % 117.57/117.63 inference(scs_inference,[],[26,4433,7099,7040,7135,7148,4306,4644,6999,3633,3693,29,45,68,74,13,16,2,82,9,18,17,81,14,78,10,12,7,71,72,6,79,11,83,90,77,4,8,69,5,15,75,89,88,101,21,73,3,87,25,100,96])). % 117.57/117.63 cnf(7943,plain, % 117.57/117.63 ($false), % 117.57/117.63 inference(scs_inference,[],[46,43,127,38,40,28,218,4067,3625,7227,3593,1325,47,3689,3939,3841,3693,4258,3994,3773,4200,4008,3651,4459,4327,2,13,1442,478,25,3,22,21,20,24,125,84,121,116]), % 117.57/117.63 ['proof']). % 117.57/117.63 % SZS output end Proof % 117.57/117.63 % Total time :117.020000s %------------------------------------------------------------------------------