%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : RNG049+1 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n026.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 14:00:51 EDT 2024 % Result : Theorem 117.88s 118.51s % Output : CNFRefutation 117.98s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : RNG049+1 : TPTP v8.2.0. Released v4.0.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n026.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Tue Jun 18 14:15:24 EDT 2024 % 0.12/0.34 % CPUTime : % 0.19/0.57 start to proof:theBenchmark % 117.88/118.49 %------------------------------------------- % 117.88/118.49 % File :CSE---1.7 % 117.88/118.49 % Problem :theBenchmark % 117.88/118.49 % Transform :cnf % 117.88/118.49 % Format :tptp:raw % 117.88/118.49 % Command :java -jar mcs_scs.jar %d %s % 117.88/118.49 % 117.88/118.49 % Result :Theorem 117.290000s % 117.88/118.49 % Output :CNFRefutation 117.290000s % 117.88/118.49 %------------------------------------------- % 117.88/118.50 %------------------------------------------------------------------------------ % 117.88/118.50 % File : RNG049+1 : TPTP v8.2.0. Released v4.0.0. % 117.88/118.50 % Domain : Ring Theory % 117.88/118.50 % Problem : Cauchy-Bouniakowsky-Schwarz inequality 04_03, 00 expansion % 117.88/118.50 % Version : Especial. % 117.88/118.50 % English : % 117.88/118.50 % 117.88/118.50 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 117.88/118.50 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 117.88/118.50 % Source : [Pas08] % 117.88/118.50 % Names : cauchy_04_03.00 [Pas08] % 117.88/118.50 % 117.88/118.50 % Status : Theorem % 117.88/118.50 % Rating : 0.36 v8.1.0, 0.33 v7.5.0, 0.38 v7.4.0, 0.27 v7.3.0, 0.34 v7.2.0, 0.31 v7.1.0, 0.30 v6.4.0, 0.35 v6.3.0, 0.29 v6.2.0, 0.40 v6.1.0, 0.53 v6.0.0, 0.48 v5.5.0, 0.67 v5.4.0, 0.71 v5.3.0, 0.70 v5.2.0, 0.55 v5.1.0, 0.62 v5.0.0, 0.71 v4.1.0, 0.74 v4.0.1, 0.87 v4.0.0 % 117.88/118.50 % Syntax : Number of formulae : 42 ( 6 unt; 1 def) % 117.88/118.50 % Number of atoms : 156 ( 42 equ) % 117.88/118.50 % Maximal formula atoms : 9 ( 3 avg) % 117.88/118.50 % Number of connectives : 120 ( 6 ~; 1 |; 61 &) % 117.88/118.50 % ( 1 <=>; 51 =>; 0 <=; 0 <~>) % 117.88/118.50 % Maximal formula depth : 10 ( 5 avg) % 117.88/118.50 % Maximal term depth : 5 ( 1 avg) % 117.88/118.50 % Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty) % 117.88/118.50 % Number of functors : 11 ( 11 usr; 3 con; 0-2 aty) % 117.88/118.50 % Number of variables : 69 ( 68 !; 1 ?) % 117.88/118.50 % SPC : FOF_THM_RFO_SEQ % 117.88/118.50 % 117.88/118.50 % Comments : Problem generated by the SAD system [VLP07] % 117.88/118.50 %------------------------------------------------------------------------------ % 117.88/118.50 fof(mNatSort,axiom, % 117.88/118.50 ! [W0] : % 117.88/118.50 ( aNaturalNumber0(W0) % 117.88/118.50 => $true ) ). % 117.88/118.50 % 117.88/118.50 fof(mZeroNat,axiom, % 117.88/118.50 aNaturalNumber0(sz00) ). % 117.88/118.50 % 117.88/118.50 fof(mSuccNat,axiom, % 117.88/118.50 ! [W0] : % 117.88/118.50 ( aNaturalNumber0(W0) % 117.88/118.50 => ( aNaturalNumber0(szszuzczcdt0(W0)) % 117.88/118.50 & szszuzczcdt0(W0) != sz00 ) ) ). % 117.88/118.50 % 117.88/118.50 fof(mNatExtr,axiom, % 117.88/118.50 ! [W0] : % 117.88/118.50 ( ( aNaturalNumber0(W0) % 117.88/118.50 & W0 != sz00 ) % 117.88/118.50 => ? [W1] : % 117.88/118.50 ( aNaturalNumber0(W1) % 117.88/118.50 & W0 = szszuzczcdt0(W1) ) ) ). % 117.88/118.50 % 117.88/118.50 fof(mSuccEqu,axiom, % 117.88/118.50 ! [W0,W1] : % 117.88/118.50 ( ( aNaturalNumber0(W0) % 117.88/118.50 & aNaturalNumber0(W1) ) % 117.88/118.50 => ( szszuzczcdt0(W0) = szszuzczcdt0(W1) % 117.88/118.50 => W0 = W1 ) ) ). % 117.88/118.50 % 117.88/118.50 fof(mIHOrd,axiom, % 117.88/118.50 ! [W0,W1] : % 117.88/118.50 ( ( aNaturalNumber0(W0) % 117.88/118.50 & aNaturalNumber0(W1) ) % 117.88/118.50 => ( iLess0(W0,W1) % 117.88/118.50 => $true ) ) ). % 117.88/118.50 % 117.88/118.50 fof(mIH,axiom, % 117.88/118.50 ! [W0] : % 117.88/118.50 ( aNaturalNumber0(W0) % 117.88/118.50 => iLess0(W0,szszuzczcdt0(W0)) ) ). % 117.88/118.50 % 117.88/118.50 fof(mScSort,axiom, % 117.88/118.50 ! [W0] : % 117.88/118.50 ( aScalar0(W0) % 117.88/118.50 => $true ) ). % 117.88/118.50 % 117.88/118.50 fof(mSZeroSc,axiom, % 117.88/118.50 aScalar0(sz0z00) ). % 117.88/118.50 % 117.88/118.50 fof(mSumSc,axiom, % 117.88/118.50 ! [W0,W1] : % 117.88/118.50 ( ( aScalar0(W0) % 117.88/118.50 & aScalar0(W1) ) % 117.88/118.50 => aScalar0(sdtpldt0(W0,W1)) ) ). % 117.88/118.50 % 117.88/118.50 fof(mMulSc,axiom, % 117.88/118.50 ! [W0,W1] : % 117.88/118.50 ( ( aScalar0(W0) % 117.88/118.50 & aScalar0(W1) ) % 117.88/118.50 => aScalar0(sdtasdt0(W0,W1)) ) ). % 117.88/118.50 % 117.88/118.50 fof(mNegSc,axiom, % 117.88/118.50 ! [W0] : % 117.88/118.50 ( aScalar0(W0) % 117.88/118.50 => aScalar0(smndt0(W0)) ) ). % 117.88/118.50 % 117.88/118.50 fof(mScZero,axiom, % 117.88/118.50 ! [W0] : % 117.88/118.50 ( aScalar0(W0) % 117.88/118.50 => ( sdtpldt0(W0,sz0z00) = W0 % 117.88/118.50 & sdtpldt0(sz0z00,W0) = W0 % 117.88/118.50 & sdtasdt0(W0,sz0z00) = sz0z00 % 117.88/118.50 & sdtasdt0(sz0z00,W0) = sz0z00 % 117.88/118.50 & sdtpldt0(W0,smndt0(W0)) = sz0z00 % 117.88/118.50 & sdtpldt0(smndt0(W0),W0) = sz0z00 % 117.88/118.50 & smndt0(smndt0(W0)) = W0 % 117.88/118.50 & smndt0(sz0z00) = sz0z00 ) ) ). % 117.88/118.50 % 117.88/118.50 fof(mArith,axiom, % 117.88/118.50 ! [W0,W1,W2] : % 117.88/118.50 ( ( aScalar0(W0) % 117.88/118.50 & aScalar0(W1) % 117.88/118.50 & aScalar0(W2) ) % 117.88/118.50 => ( sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) % 117.88/118.50 & sdtpldt0(W0,W1) = sdtpldt0(W1,W0) % 117.88/118.50 & sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) % 117.88/118.50 & sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ) ). % 117.88/118.50 % 117.88/118.50 fof(mDistr,axiom, % 117.88/118.50 ! [W0,W1,W2] : % 117.88/118.50 ( ( aScalar0(W0) % 117.88/118.50 & aScalar0(W1) % 117.88/118.50 & aScalar0(W2) ) % 117.88/118.50 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 117.88/118.50 & sdtasdt0(sdtpldt0(W0,W1),W2) = sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W1,W2)) ) ) ). % 117.88/118.50 % 117.88/118.50 fof(mDistr2,axiom, % 117.88/118.50 ! [W0,W1,W2,W3] : % 117.88/118.50 ( ( aScalar0(W0) % 117.88/118.50 & aScalar0(W1) % 117.88/118.50 & aScalar0(W2) % 117.88/118.50 & aScalar0(W3) ) % 117.88/118.50 => sdtasdt0(sdtpldt0(W0,W1),sdtpldt0(W2,W3)) = sdtpldt0(sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W0,W3)),sdtpldt0(sdtasdt0(W1,W2),sdtasdt0(W1,W3))) ) ). % 117.88/118.50 % 117.88/118.50 fof(mMNeg,axiom, % 117.88/118.50 ! [W0,W1] : % 117.88/118.50 ( ( aScalar0(W0) % 117.88/118.50 & aScalar0(W1) ) % 117.88/118.50 => ( sdtasdt0(W0,smndt0(W1)) = smndt0(sdtasdt0(W0,W1)) % 117.88/118.50 & sdtasdt0(smndt0(W0),W1) = smndt0(sdtasdt0(W0,W1)) ) ) ). % 117.88/118.50 % 117.88/118.50 fof(mMDNeg,axiom, % 117.88/118.50 ! [W0,W1] : % 117.88/118.50 ( ( aScalar0(W0) % 117.88/118.50 & aScalar0(W1) ) % 117.88/118.50 => sdtasdt0(smndt0(W0),smndt0(W1)) = sdtasdt0(W0,W1) ) ). % 117.88/118.50 % 117.88/118.50 fof(mLess,axiom, % 117.88/118.50 ! [W0,W1] : % 117.88/118.50 ( ( aScalar0(W0) % 117.88/118.50 & aScalar0(W1) ) % 117.88/118.50 => ( sdtlseqdt0(W0,W1) % 117.88/118.50 => $true ) ) ). % 117.88/118.50 % 117.88/118.50 fof(mLERef,axiom, % 117.88/118.50 ! [W0] : % 117.88/118.50 ( aScalar0(W0) % 117.88/118.50 => sdtlseqdt0(W0,W0) ) ). % 117.88/118.50 % 117.88/118.50 fof(mLEASm,axiom, % 117.88/118.50 ! [W0,W1] : % 117.88/118.50 ( ( aScalar0(W0) % 117.88/118.50 & aScalar0(W1) ) % 117.88/118.50 => ( ( sdtlseqdt0(W0,W1) % 117.88/118.50 & sdtlseqdt0(W1,W0) ) % 117.88/118.50 => W0 = W1 ) ) ). % 117.88/118.50 % 117.88/118.50 fof(mLETrn,axiom, % 117.88/118.50 ! [W0,W1,W2] : % 117.88/118.50 ( ( aScalar0(W0) % 117.88/118.50 & aScalar0(W1) % 117.88/118.50 & aScalar0(W2) ) % 117.88/118.50 => ( ( sdtlseqdt0(W0,W1) % 117.88/118.50 & sdtlseqdt0(W1,W2) ) % 117.88/118.50 => sdtlseqdt0(W0,W2) ) ) ). % 117.88/118.50 % 117.88/118.50 fof(mLEMon,axiom, % 117.88/118.50 ! [W0,W1,W2,W3] : % 117.88/118.50 ( ( aScalar0(W0) % 117.88/118.50 & aScalar0(W1) % 117.88/118.50 & aScalar0(W2) % 117.88/118.50 & aScalar0(W3) ) % 117.88/118.50 => ( ( sdtlseqdt0(W0,W1) % 117.88/118.50 & sdtlseqdt0(W2,W3) ) % 117.88/118.50 => sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W3)) ) ) ). % 117.88/118.50 % 117.88/118.50 fof(mLEMonM,axiom, % 117.88/118.50 ! [W0,W1,W2,W3] : % 117.88/118.50 ( ( aScalar0(W0) % 117.88/118.50 & aScalar0(W1) % 117.88/118.50 & aScalar0(W2) % 117.88/118.50 & aScalar0(W3) ) % 117.88/118.50 => ( ( sdtlseqdt0(W0,W1) % 117.88/118.50 & sdtlseqdt0(sz0z00,W2) % 117.88/118.50 & sdtlseqdt0(W2,W3) ) % 117.88/118.50 => sdtlseqdt0(sdtasdt0(W0,W2),sdtasdt0(W1,W3)) ) ) ). % 117.88/118.50 % 117.88/118.50 fof(mLETot,axiom, % 117.88/118.50 ! [W0,W1] : % 117.88/118.50 ( ( aScalar0(W0) % 117.88/118.50 & aScalar0(W1) ) % 117.88/118.50 => ( sdtlseqdt0(W0,W1) % 117.88/118.50 | sdtlseqdt0(W1,W0) ) ) ). % 117.88/118.50 % 117.88/118.50 fof(mPosMon,axiom, % 117.88/118.50 ! [W0,W1] : % 117.88/118.50 ( ( aScalar0(W0) % 117.88/118.50 & aScalar0(W1) ) % 117.88/118.50 => ( ( sdtlseqdt0(sz0z00,W0) % 117.88/118.50 & sdtlseqdt0(sz0z00,W1) ) % 117.88/118.50 => ( sdtlseqdt0(sz0z00,sdtpldt0(W0,W1)) % 117.88/118.51 & sdtlseqdt0(sz0z00,sdtasdt0(W0,W1)) ) ) ) ). % 117.88/118.51 % 117.88/118.51 fof(mSqPos,axiom, % 117.88/118.51 ! [W0] : % 117.88/118.51 ( aScalar0(W0) % 117.88/118.51 => sdtlseqdt0(sz0z00,sdtasdt0(W0,W0)) ) ). % 117.88/118.51 % 117.88/118.51 fof(mSqrt,axiom, % 117.88/118.51 ! [W0,W1] : % 117.88/118.51 ( ( aScalar0(W0) % 117.88/118.51 & aScalar0(W1) ) % 117.88/118.51 => ( ( sdtlseqdt0(sz0z00,W0) % 117.88/118.51 & sdtlseqdt0(sz0z00,W1) % 117.88/118.51 & sdtasdt0(W0,W0) = sdtasdt0(W1,W1) ) % 117.88/118.51 => W0 = W1 ) ) ). % 117.88/118.51 % 117.88/118.51 fof(mVcSort,axiom, % 117.88/118.51 ! [W0] : % 117.88/118.51 ( aVector0(W0) % 117.88/118.51 => $true ) ). % 117.88/118.51 % 117.88/118.51 fof(mDimNat,axiom, % 117.88/118.51 ! [W0] : % 117.88/118.51 ( aVector0(W0) % 117.88/118.51 => aNaturalNumber0(aDimensionOf0(W0)) ) ). % 117.88/118.51 % 117.88/118.51 fof(mElmSc,axiom, % 117.88/118.51 ! [W0,W1] : % 117.88/118.51 ( ( aVector0(W0) % 117.88/118.51 & aNaturalNumber0(W1) ) % 117.88/118.51 => aScalar0(sdtlbdtrb0(W0,W1)) ) ). % 117.88/118.51 % 117.88/118.51 fof(mDefInit,definition, % 117.88/118.51 ! [W0] : % 117.88/118.51 ( aVector0(W0) % 117.88/118.51 => ( aDimensionOf0(W0) != sz00 % 117.88/118.51 => ! [W1] : % 117.88/118.51 ( W1 = sziznziztdt0(W0) % 117.88/118.51 <=> ( aVector0(W1) % 117.88/118.51 & szszuzczcdt0(aDimensionOf0(W1)) = aDimensionOf0(W0) % 117.88/118.51 & ! [W2] : % 117.88/118.51 ( aNaturalNumber0(W2) % 117.88/118.51 => sdtlbdtrb0(W1,W2) = sdtlbdtrb0(W0,W2) ) ) ) ) ) ). % 117.88/118.51 % 117.88/118.51 fof(mEqInit,axiom, % 117.88/118.51 ! [W0,W1] : % 117.88/118.51 ( ( aVector0(W0) % 117.88/118.51 & aVector0(W1) ) % 117.88/118.51 => ( ( aDimensionOf0(W0) = aDimensionOf0(W1) % 117.88/118.51 & aDimensionOf0(W1) != sz00 ) % 117.88/118.51 => aDimensionOf0(sziznziztdt0(W0)) = aDimensionOf0(sziznziztdt0(W1)) ) ) ). % 117.88/118.51 % 117.88/118.51 fof(mScPr,axiom, % 117.88/118.51 ! [W0,W1] : % 117.88/118.51 ( ( aVector0(W0) % 117.88/118.51 & aVector0(W1) ) % 117.88/118.51 => ( aDimensionOf0(W0) = aDimensionOf0(W1) % 117.88/118.51 => aScalar0(sdtasasdt0(W0,W1)) ) ) ). % 117.88/118.51 % 117.88/118.51 fof(mDefSPZ,axiom, % 117.88/118.51 ! [W0,W1] : % 117.88/118.51 ( ( aVector0(W0) % 117.88/118.51 & aVector0(W1) ) % 117.88/118.51 => ( ( aDimensionOf0(W0) = aDimensionOf0(W1) % 117.88/118.51 & aDimensionOf0(W1) = sz00 ) % 117.88/118.51 => sdtasasdt0(W0,W1) = sz0z00 ) ) ). % 117.88/118.51 % 117.88/118.51 fof(mDefSPN,axiom, % 117.88/118.51 ! [W0,W1] : % 117.88/118.51 ( ( aVector0(W0) % 117.88/118.51 & aVector0(W1) ) % 117.88/118.51 => ( ( aDimensionOf0(W0) = aDimensionOf0(W1) % 117.88/118.51 & aDimensionOf0(W1) != sz00 ) % 117.88/118.51 => sdtasasdt0(W0,W1) = sdtpldt0(sdtasasdt0(sziznziztdt0(W0),sziznziztdt0(W1)),sdtasdt0(sdtlbdtrb0(W0,aDimensionOf0(W0)),sdtlbdtrb0(W1,aDimensionOf0(W1)))) ) ) ). % 117.88/118.51 % 117.88/118.51 fof(m__1542,hypothesis, % 117.88/118.51 aVector0(xs) ). % 117.88/118.51 % 117.88/118.51 fof(m__1516,hypothesis, % 117.88/118.51 ! [W0] : % 117.88/118.51 ( aVector0(W0) % 117.88/118.51 => ( iLess0(aDimensionOf0(W0),aDimensionOf0(xs)) % 117.88/118.51 => sdtlseqdt0(sz0z00,sdtasasdt0(W0,W0)) ) ) ). % 117.88/118.51 % 117.88/118.51 fof(m__1542_01,hypothesis, % 117.88/118.51 aDimensionOf0(xs) != sz00 ). % 117.88/118.51 % 117.88/118.51 fof(m__1568,hypothesis, % 117.88/118.51 sdtasasdt0(xs,xs) = sdtpldt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))) ). % 117.88/118.51 % 117.88/118.51 fof(m__1590,hypothesis, % 117.88/118.51 ( sdtlseqdt0(sz0z00,sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs))) % 117.88/118.51 & sdtlseqdt0(sz0z00,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))) ) ). % 117.88/118.51 % 117.88/118.51 fof(m__,conjecture, % 117.88/118.51 sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)) ). % 117.88/118.51 % 117.88/118.51 %------------------------------------------------------------------------------ % 117.88/118.51 %------------------------------------------- % 117.88/118.51 % Proof found % 117.88/118.51 % SZS status Theorem for theBenchmark % 117.88/118.51 % SZS output start Proof % 117.88/118.51 %ClaNum:82(EqnAxiom:25) % 117.88/118.51 %VarNum:297(SingletonVarNum:94) % 117.88/118.51 %MaxLitNum:8 % 117.88/118.51 %MaxfuncDepth:4 % 117.88/118.51 %SharedTerms:20 % 117.88/118.51 %goalClause: 33 % 117.88/118.51 %singleGoalClaCount:1 % 117.88/118.51 [26]P1(a1) % 117.88/118.51 [27]P2(a10) % 117.88/118.51 [28]P3(a11) % 117.88/118.51 [32]~E(f3(a11),a1) % 117.88/118.51 [33]~P4(a10,f2(a11,a11)) % 117.88/118.51 [29]P4(a10,f2(f12(a11),f12(a11))) % 117.88/118.51 [30]P4(a10,f7(f6(a11,f3(a11)),f6(a11,f3(a11)))) % 117.88/118.51 [31]E(f8(f2(f12(a11),f12(a11)),f7(f6(a11,f3(a11)),f6(a11,f3(a11)))),f2(a11,a11)) % 117.88/118.51 [46]~P2(x461)+P4(x461,x461) % 117.88/118.51 [34]~P2(x341)+E(f9(a10),a10) % 117.88/118.51 [35]~P1(x351)+~E(f13(x351),a1) % 117.88/118.51 [36]~P1(x361)+P1(f13(x361)) % 117.88/118.51 [37]~P3(x371)+P1(f3(x371)) % 117.88/118.51 [38]~P2(x381)+P2(f9(x381)) % 117.88/118.51 [41]~P2(x411)+E(f7(x411,a10),a10) % 117.88/118.51 [42]~P2(x421)+E(f7(a10,x421),a10) % 117.88/118.51 [44]~P2(x441)+E(f8(x441,a10),x441) % 117.88/118.51 [45]~P2(x451)+E(f8(a10,x451),x451) % 117.88/118.51 [50]~P1(x501)+P5(x501,f13(x501)) % 117.88/118.51 [57]~P2(x571)+P4(a10,f7(x571,x571)) % 117.88/118.51 [39]~P2(x391)+E(f9(f9(x391)),x391) % 117.88/118.51 [48]~P2(x481)+E(f8(x481,f9(x481)),a10) % 117.88/118.51 [49]~P2(x491)+E(f8(f9(x491),x491),a10) % 117.88/118.51 [40]~P1(x401)+E(x401,a1)+P1(f4(x401)) % 117.88/118.51 [70]~P3(x701)+~P5(f3(x701),f3(a11))+P4(a10,f2(x701,x701)) % 117.88/118.51 [43]~P1(x431)+E(x431,a1)+E(f13(f4(x431)),x431) % 117.88/118.51 [54]~P2(x542)+~P2(x541)+P2(f8(x541,x542)) % 117.88/118.51 [55]~P2(x552)+~P2(x551)+P2(f7(x551,x552)) % 117.88/118.51 [56]~P1(x562)+~P3(x561)+P2(f6(x561,x562)) % 117.88/118.51 [62]~P2(x622)+~P2(x621)+E(f7(f9(x621),f9(x622)),f7(x621,x622)) % 117.88/118.51 [66]~P2(x662)+~P2(x661)+E(f9(f7(x661,x662)),f7(x661,f9(x662))) % 117.88/118.51 [67]~P2(x672)+~P2(x671)+E(f9(f7(x671,x672)),f7(f9(x671),x672)) % 117.88/118.51 [53]P4(x532,x531)+~P2(x531)+~P2(x532)+P4(x531,x532) % 117.88/118.51 [47]~P3(x471)+P3(x472)+~E(x472,f12(x471))+E(f3(x471),a1) % 117.88/118.51 [51]~P1(x512)+~P1(x511)+E(x511,x512)+~E(f13(x511),f13(x512)) % 117.88/118.51 [64]~P3(x642)+~P3(x641)+~E(f3(x641),f3(x642))+P2(f2(x641,x642)) % 117.88/118.51 [52]~P3(x521)+~E(x522,f12(x521))+E(f3(x521),a1)+E(f13(f3(x522)),f3(x521)) % 117.88/118.51 [59]~P2(x592)+~P2(x591)+~P2(x593)+E(f8(x591,x592),f8(x592,x591)) % 117.88/118.51 [60]~P2(x602)+~P2(x601)+~P2(x603)+E(f7(x601,x602),f7(x602,x601)) % 117.88/118.51 [73]~P2(x733)+~P2(x732)+~P2(x731)+E(f8(f8(x731,x732),x733),f8(x731,f8(x732,x733))) % 117.88/118.51 [74]~P2(x743)+~P2(x742)+~P2(x741)+E(f7(f7(x741,x742),x743),f7(x741,f7(x742,x743))) % 117.88/118.51 [76]~P2(x763)+~P2(x762)+~P2(x761)+E(f8(f7(x761,x762),f7(x761,x763)),f7(x761,f8(x762,x763))) % 117.88/118.51 [77]~P2(x772)+~P2(x773)+~P2(x771)+E(f8(f7(x771,x772),f7(x773,x772)),f7(f8(x771,x773),x772)) % 117.88/118.51 [65]~P2(x652)+~P2(x651)+~P4(x652,x651)+~P4(x651,x652)+E(x651,x652) % 117.88/118.51 [58]~P3(x582)+~P3(x581)+~E(f3(x581),f3(x582))+~E(f3(x582),a1)+E(f2(x581,x582),a10) % 117.88/118.51 [71]~P2(x712)+~P2(x711)+~P4(a10,x712)+~P4(a10,x711)+P4(a10,f8(x711,x712)) % 117.88/118.51 [72]~P2(x722)+~P2(x721)+~P4(a10,x722)+~P4(a10,x721)+P4(a10,f7(x721,x722)) % 117.88/118.51 [61]~P3(x611)+~P3(x612)+~E(f3(x612),f3(x611))+E(f3(x611),a1)+E(f3(f12(x612)),f3(f12(x611))) % 117.88/118.51 [81]~P3(x811)+~P3(x812)+~E(f3(x812),f3(x811))+E(f3(x811),a1)+E(f8(f2(f12(x812),f12(x811)),f7(f6(x812,f3(x812)),f6(x811,f3(x811)))),f2(x812,x811)) % 117.88/118.51 [63]~P1(x633)+~P3(x631)+~E(x632,f12(x631))+E(f6(x632,x633),f6(x631,x633))+E(f3(x631),a1) % 117.88/118.51 [82]~P2(x823)+~P2(x822)+~P2(x824)+~P2(x821)+E(f8(f8(f7(x821,x822),f7(x821,x823)),f8(f7(x824,x822),f7(x824,x823))),f7(f8(x821,x824),f8(x822,x823))) % 117.88/118.51 [75]~P2(x752)+~P2(x751)+E(x751,x752)+~E(f7(x751,x751),f7(x752,x752))+~P4(a10,x752)+~P4(a10,x751) % 117.88/118.51 [68]~P3(x681)+~P3(x682)+E(x681,f12(x682))+E(f3(x682),a1)+P1(f5(x682,x681))+~E(f13(f3(x681)),f3(x682)) % 117.88/118.51 [80]~P3(x802)+~P3(x801)+E(x801,f12(x802))+E(f3(x802),a1)+~E(f13(f3(x801)),f3(x802))+~E(f6(x801,f5(x802,x801)),f6(x802,f5(x802,x801))) % 117.88/118.51 [69]~P2(x692)+~P2(x691)+~P4(x693,x692)+~P4(x691,x693)+P4(x691,x692)+~P2(x693) % 117.88/118.51 [78]~P2(x784)+~P2(x782)+~P2(x783)+~P2(x781)+~P4(x782,x784)+~P4(x781,x783)+P4(f8(x781,x782),f8(x783,x784)) % 117.88/118.51 [79]~P2(x794)+~P2(x792)+~P2(x793)+~P2(x791)+~P4(x792,x794)+~P4(x791,x793)+~P4(a10,x792)+P4(f7(x791,x792),f7(x793,x794)) % 117.88/118.51 %EqnAxiom % 117.88/118.51 [1]E(x11,x11) % 117.88/118.51 [2]E(x22,x21)+~E(x21,x22) % 117.88/118.51 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 117.88/118.51 [4]~E(x41,x42)+E(f12(x41),f12(x42)) % 117.88/118.51 [5]~E(x51,x52)+E(f7(x51,x53),f7(x52,x53)) % 117.88/118.51 [6]~E(x61,x62)+E(f7(x63,x61),f7(x63,x62)) % 117.88/118.51 [7]~E(x71,x72)+E(f2(x71,x73),f2(x72,x73)) % 117.88/118.51 [8]~E(x81,x82)+E(f2(x83,x81),f2(x83,x82)) % 117.88/118.51 [9]~E(x91,x92)+E(f3(x91),f3(x92)) % 117.88/118.51 [10]~E(x101,x102)+E(f6(x101,x103),f6(x102,x103)) % 117.88/118.51 [11]~E(x111,x112)+E(f6(x113,x111),f6(x113,x112)) % 117.88/118.51 [12]~E(x121,x122)+E(f8(x121,x123),f8(x122,x123)) % 117.88/118.51 [13]~E(x131,x132)+E(f8(x133,x131),f8(x133,x132)) % 117.88/118.51 [14]~E(x141,x142)+E(f9(x141),f9(x142)) % 117.88/118.51 [15]~E(x151,x152)+E(f13(x151),f13(x152)) % 117.88/118.51 [16]~E(x161,x162)+E(f4(x161),f4(x162)) % 117.88/118.51 [17]~E(x171,x172)+E(f5(x171,x173),f5(x172,x173)) % 117.88/118.51 [18]~E(x181,x182)+E(f5(x183,x181),f5(x183,x182)) % 117.88/118.51 [19]~P1(x191)+P1(x192)+~E(x191,x192) % 117.88/118.51 [20]~P2(x201)+P2(x202)+~E(x201,x202) % 117.88/118.51 [21]~P3(x211)+P3(x212)+~E(x211,x212) % 117.88/118.51 [22]P4(x222,x223)+~E(x221,x222)+~P4(x221,x223) % 117.88/118.51 [23]P4(x233,x232)+~E(x231,x232)+~P4(x233,x231) % 117.88/118.51 [24]P5(x242,x243)+~E(x241,x242)+~P5(x241,x243) % 117.88/118.51 [25]P5(x253,x252)+~E(x251,x252)+~P5(x253,x251) % 117.88/118.51 % 117.88/118.51 %------------------------------------------- % 117.88/118.52 cnf(83,plain, % 117.88/118.52 (~P3(x831)+P3(f12(x831))+E(f3(x831),a1)), % 117.88/118.52 inference(equality_inference,[],[47])). % 117.88/118.52 cnf(85,plain, % 117.88/118.52 (~P3(x851)+E(f3(x851),a1)+E(f13(f3(f12(x851))),f3(x851))), % 117.88/118.52 inference(equality_inference,[],[52])). % 117.88/118.52 cnf(87,plain, % 117.88/118.52 (~P1(x871)+~P3(x872)+E(f6(f12(x872),x871),f6(x872,x871))+E(f3(x872),a1)), % 117.88/118.52 inference(equality_inference,[],[63])). % 117.88/118.52 cnf(88,plain, % 117.88/118.52 (~P3(x881)+~P3(x881)+P2(f2(x881,x881))), % 117.88/118.52 inference(equality_inference,[],[64])). % 117.88/118.52 cnf(91,plain, % 117.88/118.52 (E(f2(a11,a11),f8(f2(f12(a11),f12(a11)),f7(f6(a11,f3(a11)),f6(a11,f3(a11)))))), % 117.88/118.52 inference(scs_inference,[],[31,2])). % 117.88/118.52 cnf(92,plain, % 117.88/118.52 (~P5(f3(a11),f3(a11))), % 117.88/118.52 inference(scs_inference,[],[33,28,31,2,70])). % 117.88/118.52 cnf(94,plain, % 117.88/118.52 (~E(f2(f12(a11),f12(a11)),f2(a11,a11))), % 117.88/118.52 inference(scs_inference,[],[33,28,29,31,2,70,23])). % 117.88/118.52 cnf(95,plain, % 117.88/118.52 (P3(f12(a11))), % 117.88/118.52 inference(scs_inference,[],[33,28,32,29,31,2,70,23,83])). % 117.88/118.52 cnf(97,plain, % 117.88/118.52 (E(f13(f3(f12(a11))),f3(a11))), % 117.88/118.52 inference(scs_inference,[],[33,28,32,29,31,2,70,23,83,85])). % 117.88/118.52 cnf(100,plain, % 117.88/118.52 (P4(a10,a10)), % 117.88/118.52 inference(scs_inference,[],[33,28,27,32,29,31,2,70,23,83,85,3,53])). % 117.88/118.52 cnf(102,plain, % 117.88/118.52 (E(f6(f12(a11),a1),f6(a11,a1))), % 117.88/118.52 inference(scs_inference,[],[33,28,27,26,32,29,31,2,70,23,83,85,3,53,87])). % 117.88/118.52 cnf(104,plain, % 117.88/118.52 (P4(f7(a10,a10),f7(a10,a10))), % 117.88/118.52 inference(scs_inference,[],[33,28,27,26,32,29,31,2,70,23,83,85,3,53,87,79])). % 117.88/118.52 cnf(106,plain, % 117.88/118.52 (P4(x1061,f2(f12(a11),f12(a11)))+~E(a10,x1061)), % 117.88/118.52 inference(scs_inference,[],[33,28,27,26,32,29,31,2,70,23,83,85,3,53,87,79,22])). % 117.88/118.52 cnf(109,plain, % 117.88/118.52 (~P2(f8(f2(f12(a11),f12(a11)),f7(f6(a11,f3(a11)),f6(a11,f3(a11)))))+P2(f2(a11,a11))), % 117.88/118.52 inference(scs_inference,[],[33,28,27,26,32,29,31,2,70,23,83,85,3,53,87,79,22,21,19,20])). % 117.88/118.52 cnf(115,plain, % 117.88/118.52 (E(f9(a10),a10)), % 117.88/118.52 inference(scs_inference,[],[27,34])). % 117.88/118.52 cnf(118,plain, % 117.88/118.52 (E(f6(a11,a1),f6(f12(a11),a1))), % 117.88/118.52 inference(scs_inference,[],[102,2])). % 117.88/118.52 cnf(121,plain, % 117.88/118.52 (P2(f8(f2(f12(a11),f12(a11)),f7(f6(a11,f3(a11)),f6(a11,f3(a11)))))), % 117.88/118.52 inference(scs_inference,[],[33,100,28,91,102,2,23,20,64])). % 117.88/118.52 cnf(124,plain, % 117.88/118.52 (P2(f2(a11,a11))), % 117.88/118.52 inference(scs_inference,[],[121,109])). % 117.88/118.52 cnf(125,plain, % 117.88/118.52 (E(f3(a11),f13(f3(f12(a11))))), % 117.88/118.52 inference(scs_inference,[],[97,2])). % 117.88/118.52 cnf(127,plain, % 117.88/118.52 (E(x1271,a10)+~E(x1271,f9(a10))), % 117.88/118.52 inference(scs_inference,[],[33,97,115,30,2,23,3])). % 117.88/118.52 cnf(132,plain, % 117.88/118.52 (E(a10,f9(a10))), % 117.88/118.52 inference(scs_inference,[],[115,2])). % 117.88/118.52 cnf(133,plain, % 117.88/118.52 (P2(f9(a10))), % 117.88/118.52 inference(scs_inference,[],[27,115,2,20])). % 117.88/118.52 cnf(134,plain, % 117.88/118.52 (P4(f9(a10),a10)), % 117.88/118.52 inference(scs_inference,[],[100,27,115,2,20,22])). % 117.88/118.52 cnf(135,plain, % 117.88/118.52 (P4(f9(a10),f9(a10))), % 117.88/118.52 inference(scs_inference,[],[100,27,115,2,20,22,23])). % 117.88/118.52 cnf(136,plain, % 117.88/118.52 (P4(f2(a11,a11),f2(a11,a11))), % 117.88/118.52 inference(scs_inference,[],[100,27,124,115,2,20,22,23,53])). % 117.88/118.52 cnf(138,plain, % 117.88/118.52 (P4(f9(a10),f2(f12(a11),f12(a11)))), % 117.88/118.52 inference(scs_inference,[],[100,27,124,115,2,20,22,23,53,106])). % 117.88/118.52 cnf(143,plain, % 117.88/118.52 (~E(f2(a11,a11),a10)), % 117.88/118.52 inference(scs_inference,[],[33,136,22])). % 117.88/118.52 cnf(144,plain, % 117.88/118.52 (P4(f2(a11,a11),f8(f2(f12(a11),f12(a11)),f7(f6(a11,f3(a11)),f6(a11,f3(a11)))))), % 117.88/118.52 inference(scs_inference,[],[33,136,91,22,23])). % 117.88/118.52 cnf(145,plain, % 117.88/118.52 (~E(f2(a11,a11),f9(a10))), % 117.88/118.52 inference(scs_inference,[],[33,136,91,22,23,127])). % 117.88/118.52 cnf(146,plain, % 117.88/118.52 (~P1(f13(f3(f12(a11))))+P1(f3(a11))), % 117.88/118.52 inference(scs_inference,[],[33,136,91,97,22,23,127,19])). % 117.88/118.52 cnf(147,plain, % 117.88/118.52 (~P1(f3(f12(a11)))+P1(f3(a11))), % 117.88/118.52 inference(scs_inference,[],[33,136,91,97,22,23,127,19,36])). % 117.88/118.52 cnf(150,plain, % 117.88/118.52 (P4(a10,f9(a10))), % 117.88/118.52 inference(scs_inference,[],[135,115,22])). % 117.88/118.52 cnf(152,plain, % 117.88/118.52 (~P4(f9(a10),f2(a11,a11))), % 117.88/118.52 inference(scs_inference,[],[33,135,27,115,124,133,22,23,69])). % 117.88/118.52 cnf(154,plain, % 117.88/118.52 (P4(f7(a10,f9(a10)),f7(f9(a10),f9(a10)))), % 117.88/118.52 inference(scs_inference,[],[33,135,27,115,124,133,22,23,69,79])). % 117.88/118.52 cnf(161,plain, % 117.88/118.52 (P4(f7(a10,f9(a10)),f7(f9(a10),a10))), % 117.88/118.52 inference(scs_inference,[],[134,150,27,132,133,30,22,79])). % 117.88/118.52 cnf(176,plain, % 117.88/118.52 (~E(f7(f9(a10),f9(a10)),f2(a11,a11))+~E(f7(a10,f9(a10)),a10)), % 117.88/118.52 inference(scs_inference,[],[33,154,22,23])). % 117.88/118.52 cnf(194,plain, % 117.88/118.52 (P2(f9(f2(a11,a11)))), % 117.88/118.52 inference(scs_inference,[],[31,121,38,20])). % 117.88/118.52 cnf(195,plain, % 117.88/118.52 (P4(f9(f2(a11,a11)),f9(f2(a11,a11)))), % 117.88/118.52 inference(scs_inference,[],[194,53])). % 117.88/118.52 cnf(235,plain, % 117.88/118.52 (~P2(f6(a11,a1))+P2(f6(f12(a11),a1))), % 117.88/118.52 inference(scs_inference,[],[118,20])). % 117.88/118.52 cnf(245,plain, % 117.88/118.52 (~P2(f6(f12(a11),a1))+P2(f6(a11,a1))), % 117.88/118.52 inference(scs_inference,[],[102,20])). % 117.88/118.52 cnf(264,plain, % 117.88/118.52 (~P2(f2(f12(a11),f12(a11)))+~P4(f2(f12(a11),f12(a11)),f2(a11,a11))), % 117.88/118.52 inference(scs_inference,[],[138,152,28,104,32,118,124,133,26,19,23,63,65,69])). % 117.88/118.52 cnf(268,plain, % 117.88/118.52 (~P1(f3(a11))+P1(f13(f3(f12(a11))))), % 117.88/118.52 inference(scs_inference,[],[125,19])). % 117.88/118.52 cnf(269,plain, % 117.88/118.52 (P1(f13(f3(f12(a11))))+~P1(f13(f3(f12(a11))))), % 117.88/118.52 inference(scs_inference,[],[125,19,146])). % 117.88/118.52 cnf(276,plain, % 117.88/118.52 (P4(f7(a10,f9(a10)),x2761)+~E(f7(f9(a10),a10),x2761)), % 117.88/118.52 inference(scs_inference,[],[161,23])). % 117.88/118.52 cnf(278,plain, % 117.88/118.52 (P4(f2(a11,a11),a10)+~P4(f2(a11,a11),a10)), % 117.88/118.52 inference(scs_inference,[],[136,138,27,161,124,133,23,65,69])). % 117.88/118.52 cnf(288,plain, % 117.88/118.52 (P4(a10,f8(a10,a10))), % 117.88/118.52 inference(scs_inference,[],[27,46,71])). % 117.88/118.52 cnf(290,plain, % 117.88/118.52 (~E(f8(a10,a10),f2(a11,a11))), % 117.88/118.52 inference(scs_inference,[],[33,288,132,22,23])). % 117.88/118.52 cnf(291,plain, % 117.88/118.52 (P4(f2(a11,a11),a10)+~P4(f8(f2(f12(a11),f12(a11)),f7(f6(a11,f3(a11)),f6(a11,f3(a11)))),a10)), % 117.88/118.52 inference(scs_inference,[],[33,144,27,288,132,124,121,22,23,69])). % 117.88/118.52 cnf(448,plain, % 117.88/118.52 (E(f9(f9(f9(a10))),f9(a10))), % 117.88/118.52 inference(scs_inference,[],[27,39,38])). % 117.88/118.52 cnf(451,plain, % 117.88/118.52 (P2(f9(f9(f9(a10))))), % 117.88/118.52 inference(scs_inference,[],[133,145,448,2,3,20])). % 117.88/118.52 cnf(454,plain, % 117.88/118.52 (P4(f9(a10),f9(f9(f9(a10))))), % 117.88/118.52 inference(scs_inference,[],[133,145,448,2,3,20,53,22])). % 117.88/118.52 cnf(456,plain, % 117.88/118.52 (P4(f9(f9(f9(a10))),f9(a10))), % 117.88/118.52 inference(scs_inference,[],[133,145,448,2,3,20,53,22,21,23])). % 117.88/118.52 cnf(462,plain, % 117.88/118.52 (P4(a10,f9(f9(f9(a10))))), % 117.88/118.52 inference(scs_inference,[],[454,115,22])). % 117.88/118.52 cnf(464,plain, % 117.88/118.52 (E(f9(f9(f9(a10))),a10)), % 117.88/118.52 inference(scs_inference,[],[456,454,27,115,451,22,23,65])). % 117.88/118.52 cnf(466,plain, % 117.88/118.52 (~P4(f9(f9(f9(a10))),f2(a11,a11))), % 117.88/118.52 inference(scs_inference,[],[456,454,152,27,115,124,133,451,22,23,65,69])). % 117.88/118.52 cnf(505,plain, % 117.88/118.52 (E(f7(f9(a10),a10),a10)), % 117.88/118.52 inference(scs_inference,[],[27,41,38])). % 117.88/118.52 cnf(509,plain, % 117.88/118.52 (P4(f7(a10,f9(a10)),f9(a10))), % 117.88/118.52 inference(scs_inference,[],[143,132,505,276,2,3,23])). % 117.88/118.52 cnf(510,plain, % 117.88/118.52 (P2(f7(f9(a10),a10))), % 117.88/118.52 inference(scs_inference,[],[143,27,132,505,276,2,3,23,20])). % 117.88/118.52 cnf(511,plain, % 117.88/118.52 (P4(f7(f9(a10),a10),f7(f9(a10),a10))), % 117.88/118.52 inference(scs_inference,[],[143,27,132,505,276,2,3,23,20,53])). % 117.88/118.52 cnf(519,plain, % 117.88/118.52 (P4(a10,f7(f9(a10),a10))), % 117.88/118.52 inference(scs_inference,[],[511,505,22])). % 117.88/118.52 cnf(534,plain, % 117.88/118.52 (P4(f9(a10),f7(f9(a10),a10))), % 117.88/118.52 inference(scs_inference,[],[519,132,22])). % 117.88/118.52 cnf(578,plain, % 117.88/118.52 (E(f7(a10,f9(a10)),a10)), % 117.88/118.52 inference(scs_inference,[],[27,42,38])). % 117.88/118.52 cnf(579,plain, % 117.88/118.52 (~E(f7(f9(a10),f9(a10)),f2(a11,a11))), % 117.88/118.52 inference(scs_inference,[],[578,176])). % 117.88/118.52 cnf(580,plain, % 117.88/118.52 (E(a10,f7(a10,f9(a10)))), % 117.88/118.52 inference(scs_inference,[],[578,2])). % 117.88/118.52 cnf(581,plain, % 117.88/118.52 (~E(f2(a11,a11),f7(a10,f9(a10)))), % 117.88/118.52 inference(scs_inference,[],[143,578,2,3])). % 117.88/118.52 cnf(582,plain, % 117.88/118.52 (P4(a10,f7(f9(a10),f9(a10)))), % 117.88/118.52 inference(scs_inference,[],[143,154,578,2,3,22])). % 117.88/118.52 cnf(583,plain, % 117.88/118.52 (P2(f7(a10,f9(a10)))), % 117.88/118.52 inference(scs_inference,[],[143,154,27,578,2,3,22,20])). % 117.88/118.52 cnf(584,plain, % 117.88/118.52 (P4(f7(a10,f9(a10)),f7(a10,f9(a10)))), % 117.88/118.52 inference(scs_inference,[],[143,154,27,578,2,3,22,20,53])). % 117.88/118.52 cnf(591,plain, % 117.88/118.52 (P4(a10,f7(a10,f9(a10)))), % 117.88/118.52 inference(scs_inference,[],[584,578,22])). % 117.88/118.52 cnf(593,plain, % 117.88/118.52 (~P4(f7(a10,f9(a10)),f2(a11,a11))), % 117.88/118.52 inference(scs_inference,[],[33,584,27,124,583,578,22,23,69])). % 117.88/118.52 cnf(609,plain, % 117.88/118.52 (P4(f9(a10),f7(a10,f9(a10)))), % 117.88/118.52 inference(scs_inference,[],[591,132,22])). % 117.88/118.52 cnf(610,plain, % 117.88/118.52 (E(f9(a10),f7(a10,f9(a10)))), % 117.88/118.52 inference(scs_inference,[],[509,591,132,133,583,22,65])). % 117.88/118.52 cnf(612,plain, % 117.88/118.52 (E(f7(a10,f9(a10)),f9(a10))), % 117.88/118.52 inference(scs_inference,[],[509,591,132,133,583,22,65,2])). % 117.88/118.52 cnf(651,plain, % 117.88/118.52 (E(f8(f9(a10),a10),f9(a10))), % 117.88/118.52 inference(scs_inference,[],[27,44,38])). % 117.88/118.52 cnf(654,plain, % 117.88/118.52 (P2(f8(f9(a10),a10))), % 117.88/118.52 inference(scs_inference,[],[133,651,145,2,3,20])). % 117.88/118.52 cnf(655,plain, % 117.88/118.52 (P4(f8(f9(a10),a10),f8(f9(a10),a10))), % 117.88/118.52 inference(scs_inference,[],[133,651,145,2,3,20,53])). % 117.88/118.52 cnf(657,plain, % 117.88/118.52 (P4(f9(a10),f8(f9(a10),a10))), % 117.88/118.52 inference(scs_inference,[],[133,651,145,2,3,20,53,22])). % 117.88/118.52 cnf(659,plain, % 117.88/118.52 (P4(f8(f9(a10),a10),f9(a10))), % 117.88/118.52 inference(scs_inference,[],[133,651,145,2,3,20,53,22,21,23])). % 117.88/118.52 cnf(665,plain, % 117.88/118.52 (P4(f7(a10,f9(a10)),f8(f9(a10),a10))), % 117.88/118.52 inference(scs_inference,[],[657,610,22])). % 117.88/118.52 cnf(666,plain, % 117.88/118.52 (P4(f8(f9(a10),a10),f7(a10,f9(a10)))), % 117.88/118.52 inference(scs_inference,[],[659,657,610,22,23])). % 117.88/118.52 cnf(669,plain, % 117.88/118.52 (P4(f8(f9(a10),a10),a10)), % 117.88/118.52 inference(scs_inference,[],[134,659,657,27,610,133,583,654,22,23,65,69])). % 117.88/118.52 cnf(671,plain, % 117.88/118.52 (E(f7(a10,f9(a10)),f8(f9(a10),a10))), % 117.88/118.52 inference(scs_inference,[],[134,659,657,27,610,133,583,654,22,23,65,69,2])). % 117.88/118.52 cnf(684,plain, % 117.88/118.52 (P4(a10,f8(f9(a10),a10))), % 117.88/118.52 inference(scs_inference,[],[665,578,22])). % 117.88/118.52 cnf(686,plain, % 117.88/118.52 (E(a10,f8(f9(a10),a10))), % 117.88/118.52 inference(scs_inference,[],[593,665,669,27,578,654,22,23,65])). % 117.88/118.52 cnf(688,plain, % 117.88/118.52 (~P4(f8(f9(a10),a10),f2(a11,a11))), % 117.88/118.52 inference(scs_inference,[],[593,665,669,27,124,578,583,654,22,23,65,69])). % 117.88/118.52 cnf(690,plain, % 117.88/118.52 (P4(f7(a10,f8(f9(a10),a10)),f7(f8(f9(a10),a10),f8(f9(a10),a10)))), % 117.88/118.52 inference(scs_inference,[],[593,655,665,669,27,124,578,583,654,22,23,65,69,79])). % 117.88/118.52 cnf(699,plain, % 117.88/118.52 (P4(f7(a10,f8(f9(a10),a10)),f7(f8(f9(a10),a10),f7(a10,f9(a10))))), % 117.88/118.52 inference(scs_inference,[],[462,666,684,27,686,583,654,22,79])). % 117.88/118.52 cnf(705,plain, % 117.88/118.52 (P4(f8(f9(a10),a10),f7(f9(a10),a10))), % 117.88/118.52 inference(scs_inference,[],[519,686,22])). % 117.88/118.52 cnf(711,plain, % 117.88/118.52 (P4(f7(a10,f8(f9(a10),a10)),f7(f8(f9(a10),a10),a10))), % 117.88/118.52 inference(scs_inference,[],[582,684,669,27,686,654,22,79])). % 117.88/118.52 cnf(713,plain, % 117.88/118.52 (P4(f7(a10,f8(f9(a10),a10)),x7131)+~E(f7(f8(f9(a10),a10),f7(a10,f9(a10))),x7131)), % 117.88/118.52 inference(scs_inference,[],[582,684,669,27,686,699,654,22,79,23])). % 117.88/118.52 cnf(719,plain, % 117.88/118.52 (P4(f7(a10,f8(f9(a10),a10)),x7191)+~E(f7(f8(f9(a10),a10),a10),x7191)), % 117.88/118.52 inference(scs_inference,[],[288,686,711,22,23])). % 117.88/118.52 cnf(725,plain, % 117.88/118.52 (P4(f7(a10,f8(f9(a10),a10)),x7251)+~E(f7(f8(f9(a10),a10),f8(f9(a10),a10)),x7251)), % 117.88/118.52 inference(scs_inference,[],[686,690,30,22,23])). % 117.88/118.52 cnf(730,plain, % 117.88/118.52 (P4(x7301,f7(f8(f9(a10),a10),f7(a10,f9(a10))))+~E(f7(a10,f8(f9(a10),a10)),x7301)), % 117.88/118.52 inference(scs_inference,[],[699,22])). % 117.88/118.52 cnf(734,plain, % 117.88/118.52 (P4(x7341,f7(f8(f9(a10),a10),a10))+~E(f7(a10,f8(f9(a10),a10)),x7341)), % 117.88/118.52 inference(scs_inference,[],[711,22])). % 117.88/118.52 cnf(738,plain, % 117.88/118.52 (P4(x7381,f7(f8(f9(a10),a10),f8(f9(a10),a10)))+~E(f7(a10,f8(f9(a10),a10)),x7381)), % 117.88/118.52 inference(scs_inference,[],[690,22])). % 117.98/118.52 cnf(754,plain, % 117.98/118.52 (E(f8(a10,f9(a10)),f9(a10))), % 117.98/118.52 inference(scs_inference,[],[27,45,38])). % 117.98/118.52 cnf(755,plain, % 117.98/118.52 (E(f9(a10),f8(a10,f9(a10)))), % 117.98/118.52 inference(scs_inference,[],[754,2])). % 117.98/118.52 cnf(757,plain, % 117.98/118.52 (P2(f8(a10,f9(a10)))), % 117.98/118.52 inference(scs_inference,[],[133,754,145,2,3,20])). % 117.98/118.52 cnf(758,plain, % 117.98/118.52 (P4(f8(a10,f9(a10)),f8(a10,f9(a10)))), % 117.98/118.52 inference(scs_inference,[],[133,754,145,2,3,20,53])). % 117.98/118.52 cnf(760,plain, % 117.98/118.52 (P4(f9(a10),f8(a10,f9(a10)))), % 117.98/118.52 inference(scs_inference,[],[133,754,145,2,3,20,53,22])). % 117.98/118.52 cnf(762,plain, % 117.98/118.52 (P4(f8(a10,f9(a10)),f9(a10))), % 117.98/118.52 inference(scs_inference,[],[133,754,145,2,3,20,53,22,21,23])). % 117.98/118.52 cnf(768,plain, % 117.98/118.52 (P4(f7(a10,f9(a10)),f8(a10,f9(a10)))), % 117.98/118.52 inference(scs_inference,[],[760,610,22])). % 117.98/118.52 cnf(772,plain, % 117.98/118.52 (P4(f8(a10,f9(a10)),a10)), % 117.98/118.52 inference(scs_inference,[],[134,762,760,610,27,133,583,757,22,23,65,69])). % 117.98/118.52 cnf(790,plain, % 117.98/118.52 (P4(a10,f8(a10,f9(a10)))), % 117.98/118.52 inference(scs_inference,[],[768,593,578,23,22])). % 117.98/118.52 cnf(791,plain, % 117.98/118.52 (E(a10,f8(a10,f9(a10)))), % 117.98/118.52 inference(scs_inference,[],[768,772,593,27,578,757,23,22,65])). % 117.98/118.52 cnf(793,plain, % 117.98/118.52 (~P4(f8(a10,f9(a10)),f2(a11,a11))), % 117.98/118.52 inference(scs_inference,[],[768,772,593,27,578,124,583,757,23,22,65,69])). % 117.98/118.52 cnf(798,plain, % 117.98/118.52 (E(f8(a10,f9(a10)),a10)), % 117.98/118.52 inference(scs_inference,[],[758,768,772,593,27,578,124,583,757,23,22,65,69,79,106,2])). % 117.98/118.52 cnf(803,plain, % 117.98/118.52 (P4(f8(f9(a10),a10),f8(a10,f9(a10)))), % 117.98/118.52 inference(scs_inference,[],[790,686,22])). % 117.98/118.52 cnf(849,plain, % 117.98/118.52 (P4(a10,f7(a10,a10))), % 117.98/118.52 inference(scs_inference,[],[464,451,57,20])). % 117.98/118.52 cnf(850,plain, % 117.98/118.52 (~E(f7(a10,a10),f2(a11,a11))), % 117.98/118.52 inference(scs_inference,[],[33,849,23])). % 117.98/118.52 cnf(874,plain, % 117.98/118.52 (P1(f3(a11))), % 117.98/118.52 inference(scs_inference,[],[95,147,37])). % 117.98/118.52 cnf(875,plain, % 117.98/118.52 (P1(f13(f3(f12(a11))))), % 117.98/118.52 inference(scs_inference,[],[874,268])). % 117.98/118.52 cnf(876,plain, % 117.98/118.52 (E(f6(f12(a11),f3(a11)),f6(a11,f3(a11)))), % 117.98/118.52 inference(scs_inference,[],[28,32,874,87])). % 117.98/118.52 cnf(883,plain, % 117.98/118.52 (P1(f13(f3(f12(a11))))), % 117.98/118.52 inference(scs_inference,[],[875,269])). % 117.98/118.52 cnf(890,plain, % 117.98/118.52 (P4(f6(a11,f3(a11)),f6(a11,f3(a11)))+~P2(f6(f12(a11),f3(a11)))), % 117.98/118.52 inference(scs_inference,[],[876,19,20,53])). % 117.98/118.52 cnf(986,plain, % 117.98/118.52 (P4(f8(a10,f9(a10)),f7(f9(a10),a10))), % 117.98/118.52 inference(scs_inference,[],[519,791,22])). % 117.98/118.52 cnf(1007,plain, % 117.98/118.52 (E(f8(f9(a10),a10),f8(a10,f9(a10)))), % 117.98/118.52 inference(scs_inference,[],[803,684,791,654,757,22,65,2])). % 117.98/118.52 cnf(1086,plain, % 117.98/118.52 (P4(f7(a10,f9(a10)),f7(f9(a10),f7(f9(a10),a10)))), % 117.98/118.52 inference(scs_inference,[],[534,150,27,133,510,79])). % 117.98/118.52 cnf(1088,plain, % 117.98/118.52 (~E(f7(f9(a10),f7(f9(a10),a10)),f2(a11,a11))), % 117.98/118.52 inference(scs_inference,[],[534,150,593,27,133,510,79,23])). % 117.98/118.52 cnf(1138,plain, % 117.98/118.52 (P4(f7(a10,f8(f9(a10),a10)),f7(f8(f9(a10),a10),f7(f9(a10),a10)))), % 117.98/118.52 inference(scs_inference,[],[705,684,27,1086,671,510,654,22,79])). % 117.98/118.52 cnf(1140,plain, % 117.98/118.52 (P4(f7(a10,f8(f9(a10),a10)),x11401)+~E(f7(f8(f9(a10),a10),f7(f9(a10),a10)),x11401)), % 117.98/118.52 inference(scs_inference,[],[705,684,27,1086,671,510,654,22,79,23])). % 117.98/118.52 cnf(1144,plain, % 117.98/118.52 (P4(x11441,f7(f8(f9(a10),a10),f7(f9(a10),a10)))+~E(f7(a10,f8(f9(a10),a10)),x11441)), % 117.98/118.52 inference(scs_inference,[],[1138,22])). % 117.98/118.52 cnf(1308,plain, % 117.98/118.52 (E(f8(f9(a10),f9(f9(a10))),a10)), % 117.98/118.52 inference(scs_inference,[],[27,48,38])). % 117.98/118.52 cnf(1310,plain, % 117.98/118.52 (~E(f2(a11,a11),f8(f9(a10),f9(f9(a10))))), % 117.98/118.52 inference(scs_inference,[],[143,1308,2,3])). % 117.98/118.52 cnf(1311,plain, % 117.98/118.52 (P2(f8(f9(a10),f9(f9(a10))))), % 117.98/118.52 inference(scs_inference,[],[143,27,1308,2,3,20])). % 117.98/118.52 cnf(1374,plain, % 117.98/118.52 (E(f8(f9(f9(a10)),f9(a10)),a10)), % 117.98/118.52 inference(scs_inference,[],[27,49,38])). % 117.98/118.52 cnf(1375,plain, % 117.98/118.52 (E(a10,f8(f9(f9(a10)),f9(a10)))), % 117.98/118.52 inference(scs_inference,[],[1374,2])). % 117.98/118.52 cnf(1376,plain, % 117.98/118.52 (~E(f2(a11,a11),f8(f9(f9(a10)),f9(a10)))), % 117.98/118.52 inference(scs_inference,[],[143,1374,2,3])). % 117.98/118.52 cnf(1377,plain, % 117.98/118.52 (P2(f8(f9(f9(a10)),f9(a10)))), % 117.98/118.52 inference(scs_inference,[],[143,27,1374,2,3,20])). % 117.98/118.52 cnf(1378,plain, % 117.98/118.52 (P4(f8(f9(f9(a10)),f9(a10)),f8(f9(f9(a10)),f9(a10)))), % 117.98/118.52 inference(scs_inference,[],[143,27,1374,2,3,20,53])). % 117.98/118.52 cnf(1380,plain, % 117.98/118.52 (P4(f8(f9(f9(a10)),f9(a10)),f2(f12(a11),f12(a11)))), % 117.98/118.52 inference(scs_inference,[],[143,27,1374,2,3,20,53,106])). % 117.98/118.52 cnf(1383,plain, % 117.98/118.52 (P4(a10,f8(f9(f9(a10)),f9(a10)))), % 117.98/118.52 inference(scs_inference,[],[143,27,1374,2,3,20,53,106,23,19,22])). % 117.98/118.52 cnf(1384,plain, % 117.98/118.52 (~P4(f8(f9(f9(a10)),f9(a10)),f2(a11,a11))), % 117.98/118.52 inference(scs_inference,[],[33,143,27,124,1374,2,3,20,53,106,23,19,22,69])). % 117.98/118.52 cnf(1433,plain, % 117.98/118.52 (P4(f7(a10,f8(a10,f9(a10))),f7(f8(a10,f9(a10)),f7(f9(a10),a10)))), % 117.98/118.52 inference(scs_inference,[],[986,790,1086,27,578,510,757,22,79])). % 117.98/118.52 cnf(1439,plain, % 117.98/118.52 (P4(f7(a10,f9(a10)),f7(f9(a10),f8(f9(a10),a10)))), % 117.98/118.52 inference(scs_inference,[],[657,150,27,133,654,79])). % 117.98/118.52 cnf(1442,plain, % 117.98/118.52 (~E(f7(f9(a10),f8(f9(a10),a10)),f2(a11,a11))), % 117.98/118.52 inference(scs_inference,[],[657,150,593,27,1433,133,654,79,22,23])). % 117.98/118.52 cnf(1449,plain, % 117.98/118.52 (P4(f7(a10,f7(a10,f9(a10))),x14491)+~E(f7(f7(a10,f9(a10)),f8(f9(a10),a10)),x14491)), % 117.98/118.52 inference(scs_inference,[],[665,591,27,1439,578,583,654,22,79,23])). % 117.98/118.52 cnf(1826,plain, % 117.98/118.52 (P4(a10,f7(f9(a10),f9(f9(f9(a10)))))), % 117.98/118.52 inference(scs_inference,[],[454,150,27,578,133,451,79,22])). % 117.98/118.52 cnf(1827,plain, % 117.98/118.52 (~E(f7(f9(a10),f9(f9(f9(a10)))),f2(a11,a11))), % 117.98/118.52 inference(scs_inference,[],[454,150,593,27,578,133,451,79,22,23])). % 117.98/118.52 cnf(1832,plain, % 117.98/118.52 (P4(f7(a10,f8(f9(a10),a10)),f7(f8(f9(a10),a10),f8(a10,f9(a10))))), % 117.98/118.52 inference(scs_inference,[],[803,684,1826,686,27,654,757,22,79])). % 117.98/118.52 cnf(1834,plain, % 117.98/118.52 (P4(f7(a10,f8(f9(a10),a10)),x18341)+~E(f7(f8(f9(a10),a10),f8(a10,f9(a10))),x18341)), % 117.98/118.52 inference(scs_inference,[],[803,684,1826,686,27,654,757,22,79,23])). % 117.98/118.52 cnf(1838,plain, % 117.98/118.52 (P4(x18381,f7(f8(f9(a10),a10),f8(a10,f9(a10))))+~E(f7(a10,f8(f9(a10),a10)),x18381)), % 117.98/118.52 inference(scs_inference,[],[1832,22])). % 117.98/118.52 cnf(1932,plain, % 117.98/118.52 (P2(f6(f12(a11),a1))), % 117.98/118.52 inference(scs_inference,[],[26,28,235,56])). % 117.98/118.52 cnf(1933,plain, % 117.98/118.52 (P2(f6(a11,a1))), % 117.98/118.52 inference(scs_inference,[],[1932,245])). % 117.98/118.52 cnf(1976,plain, % 117.98/118.52 (~E(f7(f9(a10),f7(a10,f9(a10))),f2(a11,a11))), % 117.98/118.52 inference(scs_inference,[],[609,150,593,27,578,133,583,79,22,23])). % 117.98/118.52 cnf(2408,plain, % 117.98/118.52 (P2(f9(f6(a11,a1)))), % 117.98/118.52 inference(scs_inference,[],[1933,121,46,38])). % 117.98/118.52 cnf(2410,plain, % 117.98/118.52 (P5(f3(a11),f13(f3(a11)))), % 117.98/118.52 inference(scs_inference,[],[1933,121,874,46,38,50])). % 117.98/118.52 cnf(2412,plain, % 117.98/118.52 (~E(f13(f3(a11)),a1)), % 117.98/118.52 inference(scs_inference,[],[1933,121,874,46,38,50,35])). % 117.98/118.52 cnf(2414,plain, % 117.98/118.52 (E(f9(f9(f6(a11,a1))),f6(a11,a1))), % 117.98/118.52 inference(scs_inference,[],[1933,121,874,46,38,50,35,39])). % 117.98/118.52 cnf(2416,plain, % 117.98/118.52 (E(f8(f6(a11,a1),a10),f6(a11,a1))), % 117.98/118.52 inference(scs_inference,[],[1933,121,874,46,38,50,35,39,44])). % 117.98/118.52 cnf(2418,plain, % 117.98/118.52 (E(f8(a10,f6(a11,a1)),f6(a11,a1))), % 117.98/118.52 inference(scs_inference,[],[1933,121,874,46,38,50,35,39,44,45])). % 117.98/118.52 cnf(2420,plain, % 117.98/118.52 (P4(a10,f7(f6(a11,a1),f6(a11,a1)))), % 117.98/118.52 inference(scs_inference,[],[1933,121,874,46,38,50,35,39,44,45,57])). % 117.98/118.52 cnf(2422,plain, % 117.98/118.52 (E(f7(f6(a11,a1),a10),a10)), % 117.98/118.52 inference(scs_inference,[],[1933,121,874,46,38,50,35,39,44,45,57,41])). % 117.98/118.52 cnf(2424,plain, % 117.98/118.52 (E(f7(a10,f6(a11,a1)),a10)), % 117.98/118.52 inference(scs_inference,[],[1933,121,874,46,38,50,35,39,44,45,57,41,42])). % 117.98/118.52 cnf(2429,plain, % 117.98/118.52 (E(f8(f6(a11,a1),f9(f6(a11,a1))),a10)), % 117.98/118.52 inference(scs_inference,[],[1007,1933,121,874,46,38,50,35,39,44,45,57,41,42,9,14,16,48])). % 117.98/118.52 cnf(2431,plain, % 117.98/118.52 (E(f8(f9(f6(a11,a1)),f6(a11,a1)),a10)), % 117.98/118.52 inference(scs_inference,[],[1007,1933,121,874,46,38,50,35,39,44,45,57,41,42,9,14,16,48,49])). % 117.98/118.52 cnf(2433,plain, % 117.98/118.52 (E(f7(f8(f9(a10),a10),x24331),f7(f8(a10,f9(a10)),x24331))), % 117.98/118.52 inference(scs_inference,[],[1007,1933,121,874,46,38,50,35,39,44,45,57,41,42,9,14,16,48,49,5])). % 117.98/118.52 cnf(2434,plain, % 117.98/118.52 (E(f7(x24341,f8(f9(a10),a10)),f7(x24341,f8(a10,f9(a10))))), % 117.98/118.52 inference(scs_inference,[],[1007,1933,121,874,46,38,50,35,39,44,45,57,41,42,9,14,16,48,49,5,6])). % 117.98/118.52 cnf(2440,plain, % 117.98/118.52 (E(f8(x24401,f8(f9(a10),a10)),f8(x24401,f8(a10,f9(a10))))), % 117.98/118.52 inference(scs_inference,[],[1007,1933,121,874,46,38,50,35,39,44,45,57,41,42,9,14,16,48,49,5,6,7,8,10,11,12,13])). % 117.98/118.52 cnf(2443,plain, % 117.98/118.52 (P4(f7(a10,f8(a10,f9(a10))),f7(f8(f9(a10),a10),a10))), % 117.98/118.52 inference(scs_inference,[],[1007,1933,121,874,46,38,50,35,39,44,45,57,41,42,9,14,16,48,49,5,6,7,8,10,11,12,13,17,18,734])). % 117.98/118.52 cnf(2448,plain, % 117.98/118.52 (P1(f13(f3(a11)))), % 117.98/118.52 inference(scs_inference,[],[1007,1933,121,874,46,38,50,35,39,44,45,57,41,42,9,14,16,48,49,5,6,7,8,10,11,12,13,17,18,734,730,738,1144,1838,36])). % 117.98/118.52 cnf(2450,plain, % 117.98/118.52 (P1(f3(f12(a11)))), % 117.98/118.52 inference(scs_inference,[],[1007,1933,121,874,95,46,38,50,35,39,44,45,57,41,42,9,14,16,48,49,5,6,7,8,10,11,12,13,17,18,734,730,738,1144,1838,36,37])). % 117.98/118.52 cnf(2454,plain, % 117.98/118.52 (~E(f2(a11,a11),f8(a10,a10))), % 117.98/118.52 inference(scs_inference,[],[290,1007,1933,121,874,95,46,38,50,35,39,44,45,57,41,42,9,14,16,48,49,5,6,7,8,10,11,12,13,17,18,734,730,738,1144,1838,36,37,15,4,2])). % 117.98/118.52 cnf(2455,plain, % 117.98/118.52 (P2(f6(f12(a11),f3(a11)))), % 117.98/118.52 inference(scs_inference,[],[290,1007,1933,121,874,95,46,38,50,35,39,44,45,57,41,42,9,14,16,48,49,5,6,7,8,10,11,12,13,17,18,734,730,738,1144,1838,36,37,15,4,2,56])). % 117.98/118.52 cnf(2457,plain, % 117.98/118.52 (E(f13(f4(f3(a11))),f3(a11))), % 117.98/118.52 inference(scs_inference,[],[290,1007,1933,121,874,95,32,46,38,50,35,39,44,45,57,41,42,9,14,16,48,49,5,6,7,8,10,11,12,13,17,18,734,730,738,1144,1838,36,37,15,4,2,56,43])). % 117.98/118.52 cnf(2465,plain, % 117.98/118.52 (P1(f4(f3(a11)))), % 117.98/118.52 inference(scs_inference,[],[290,1007,1933,121,874,95,32,46,38,50,35,39,44,45,57,41,42,9,14,16,48,49,5,6,7,8,10,11,12,13,17,18,734,730,738,1144,1838,36,37,15,4,2,56,43,62,66,67,40])). % 117.98/118.52 cnf(2467,plain, % 117.98/118.52 (P2(f8(f6(a11,a1),f6(a11,a1)))), % 117.98/118.52 inference(scs_inference,[],[290,1007,1933,121,874,95,32,46,38,50,35,39,44,45,57,41,42,9,14,16,48,49,5,6,7,8,10,11,12,13,17,18,734,730,738,1144,1838,36,37,15,4,2,56,43,62,66,67,40,54])). % 117.98/118.52 cnf(2469,plain, % 117.98/118.52 (P2(f2(f12(a11),f12(a11)))), % 117.98/118.52 inference(scs_inference,[],[290,1007,1933,121,874,95,32,46,38,50,35,39,44,45,57,41,42,9,14,16,48,49,5,6,7,8,10,11,12,13,17,18,734,730,738,1144,1838,36,37,15,4,2,56,43,62,66,67,40,54,88])). % 117.98/118.52 cnf(2471,plain, % 117.98/118.52 (~P5(f13(f3(f12(a11))),f3(a11))), % 117.98/118.52 inference(scs_inference,[],[290,1007,92,1933,121,874,95,97,32,46,38,50,35,39,44,45,57,41,42,9,14,16,48,49,5,6,7,8,10,11,12,13,17,18,734,730,738,1144,1838,36,37,15,4,2,56,43,62,66,67,40,54,88,24])). % 117.98/118.52 cnf(2472,plain, % 117.98/118.52 (P2(f7(f6(a11,a1),f6(a11,a1)))), % 117.98/118.52 inference(scs_inference,[],[290,1007,92,1933,121,874,95,97,32,46,38,50,35,39,44,45,57,41,42,9,14,16,48,49,5,6,7,8,10,11,12,13,17,18,734,730,738,1144,1838,36,37,15,4,2,56,43,62,66,67,40,54,88,24,55])). % 117.98/118.52 cnf(2474,plain, % 117.98/118.52 (~P5(f3(a11),f13(f3(f12(a11))))), % 117.98/118.52 inference(scs_inference,[],[290,1007,92,1933,121,874,95,97,32,46,38,50,35,39,44,45,57,41,42,9,14,16,48,49,5,6,7,8,10,11,12,13,17,18,734,730,738,1144,1838,36,37,15,4,2,56,43,62,66,67,40,54,88,24,55,25])). % 117.98/118.52 cnf(2476,plain, % 117.98/118.52 (P2(f6(a11,f3(a11)))), % 117.98/118.52 inference(scs_inference,[],[290,1007,92,1933,876,121,874,95,31,97,32,46,38,50,35,39,44,45,57,41,42,9,14,16,48,49,5,6,7,8,10,11,12,13,17,18,734,730,738,1144,1838,36,37,15,4,2,56,43,62,66,67,40,54,88,24,55,25,3,20])). % 117.98/118.52 cnf(2477,plain, % 117.98/118.52 (~P4(a10,f8(f2(f12(a11),f12(a11)),f7(f6(a11,f3(a11)),f6(a11,f3(a11)))))), % 117.98/118.52 inference(scs_inference,[],[33,290,1007,92,1933,876,121,874,95,31,97,32,46,38,50,35,39,44,45,57,41,42,9,14,16,48,49,5,6,7,8,10,11,12,13,17,18,734,730,738,1144,1838,36,37,15,4,2,56,43,62,66,67,40,54,88,24,55,25,3,20,23])). % 117.98/118.52 cnf(2478,plain, % 117.98/118.52 (~P4(f8(a10,f9(a10)),f8(f2(f12(a11),f12(a11)),f7(f6(a11,f3(a11)),f6(a11,f3(a11)))))), % 117.98/118.52 inference(scs_inference,[],[33,290,1007,92,1933,798,876,121,874,95,31,97,32,46,38,50,35,39,44,45,57,41,42,9,14,16,48,49,5,6,7,8,10,11,12,13,17,18,734,730,738,1144,1838,36,37,15,4,2,56,43,62,66,67,40,54,88,24,55,25,3,20,23,22])). % 117.98/118.52 cnf(2479,plain, % 117.98/118.52 (~E(f13(f3(a11)),f13(a1))), % 117.98/118.52 inference(scs_inference,[],[33,290,1007,92,1933,798,876,121,874,95,26,31,97,32,46,38,50,35,39,44,45,57,41,42,9,14,16,48,49,5,6,7,8,10,11,12,13,17,18,734,730,738,1144,1838,36,37,15,4,2,56,43,62,66,67,40,54,88,24,55,25,3,20,23,22,51])). % 117.98/118.52 cnf(2487,plain, % 117.98/118.52 (E(f8(f7(f6(a11,a1),f6(a11,a1)),f7(f6(a11,a1),f6(a11,a1))),f7(f8(f6(a11,a1),f6(a11,a1)),f6(a11,a1)))), % 117.98/118.52 inference(scs_inference,[],[33,290,1007,92,1933,798,876,121,874,95,26,31,97,32,46,38,50,35,39,44,45,57,41,42,9,14,16,48,49,5,6,7,8,10,11,12,13,17,18,734,730,738,1144,1838,36,37,15,4,2,56,43,62,66,67,40,54,88,24,55,25,3,20,23,22,51,73,74,76,77])). % 117.98/118.52 cnf(2489,plain, % 117.98/118.52 (P4(f8(f2(f12(a11),f12(a11)),f7(f6(a11,f3(a11)),f6(a11,f3(a11)))),a10)), % 117.98/118.52 inference(scs_inference,[],[33,290,1007,92,1933,798,876,121,874,95,26,31,27,97,32,46,38,50,35,39,44,45,57,41,42,9,14,16,48,49,5,6,7,8,10,11,12,13,17,18,734,730,738,1144,1838,36,37,15,4,2,56,43,62,66,67,40,54,88,24,55,25,3,20,23,22,51,73,74,76,77,53])). % 117.98/118.52 cnf(2507,plain, % 117.98/118.52 (~P4(f2(f12(a11),f12(a11)),f2(a11,a11))), % 117.98/118.52 inference(scs_inference,[],[2469,264])). % 117.98/118.52 cnf(2509,plain, % 117.98/118.52 (P4(f2(a11,a11),a10)), % 117.98/118.52 inference(scs_inference,[],[2489,291])). % 117.98/118.52 cnf(2512,plain, % 117.98/118.52 (P4(f6(a11,f3(a11)),f6(a11,f3(a11)))), % 117.98/118.52 inference(scs_inference,[],[2455,890])). % 117.98/118.52 cnf(2527,plain, % 117.98/118.52 (E(f7(a10,f9(f6(a11,a1))),a10)), % 117.98/118.52 inference(scs_inference,[],[2408,49,44,42])). % 117.98/118.52 cnf(2529,plain, % 117.98/118.53 (E(f7(f9(f6(a11,a1)),a10),a10)), % 117.98/118.53 inference(scs_inference,[],[2408,49,44,42,41])). % 117.98/118.53 cnf(2541,plain, % 117.98/118.53 (P4(a10,f7(f9(f6(a11,a1)),f9(f6(a11,a1))))), % 117.98/118.53 inference(scs_inference,[],[2416,2408,2448,49,44,42,41,18,46,39,9,16,50,7,57])). % 117.98/118.53 cnf(2550,plain, % 117.98/118.53 (~E(f13(f13(f3(a11))),a1)), % 117.98/118.53 inference(scs_inference,[],[2416,2408,2448,49,44,42,41,18,46,39,9,16,50,7,57,11,45,6,14,48,35])). % 117.98/118.53 cnf(2552,plain, % 117.98/118.53 (P2(f9(f9(f6(a11,a1))))), % 117.98/118.53 inference(scs_inference,[],[2416,2408,2448,49,44,42,41,18,46,39,9,16,50,7,57,11,45,6,14,48,35,38])). % 117.98/118.53 cnf(2557,plain, % 117.98/118.53 (P1(f13(f13(f3(a11))))), % 117.98/118.53 inference(scs_inference,[],[2416,2408,2448,49,44,42,41,18,46,39,9,16,50,7,57,11,45,6,14,48,35,38,8,17,13,36])). % 117.98/118.53 cnf(2564,plain, % 117.98/118.53 (~E(f2(a11,a11),f7(a10,a10))), % 117.98/118.53 inference(scs_inference,[],[850,2416,2408,2448,49,44,42,41,18,46,39,9,16,50,7,57,11,45,6,14,48,35,38,8,17,13,36,5,10,12,4,15,2])). % 117.98/118.53 cnf(2569,plain, % 117.98/118.53 (P2(f6(f12(a11),f13(f3(a11))))), % 117.98/118.53 inference(scs_inference,[],[850,2416,2408,2448,95,49,44,42,41,18,46,39,9,16,50,7,57,11,45,6,14,48,35,38,8,17,13,36,5,10,12,4,15,2,62,67,56])). % 117.98/118.53 cnf(2571,plain, % 117.98/118.53 (E(f13(f4(f13(f3(a11)))),f13(f3(a11)))), % 117.98/118.53 inference(scs_inference,[],[850,2416,2408,2448,2412,95,49,44,42,41,18,46,39,9,16,50,7,57,11,45,6,14,48,35,38,8,17,13,36,5,10,12,4,15,2,62,67,56,43])). % 117.98/118.53 cnf(2575,plain, % 117.98/118.53 (P1(f4(f13(f3(a11))))), % 117.98/118.53 inference(scs_inference,[],[850,2416,2408,2448,2412,95,124,49,44,42,41,18,46,39,9,16,50,7,57,11,45,6,14,48,35,38,8,17,13,36,5,10,12,4,15,2,62,67,56,43,66,40])). % 117.98/118.53 cnf(2577,plain, % 117.98/118.53 (P2(f8(f9(f6(a11,a1)),f9(f6(a11,a1))))), % 117.98/118.53 inference(scs_inference,[],[850,2416,2408,2448,2412,95,124,49,44,42,41,18,46,39,9,16,50,7,57,11,45,6,14,48,35,38,8,17,13,36,5,10,12,4,15,2,62,67,56,43,66,40,54])). % 117.98/118.53 cnf(2579,plain, % 117.98/118.53 (~P5(f13(f4(f3(a11))),f13(f3(f12(a11))))), % 117.98/118.53 inference(scs_inference,[],[850,2416,2408,2448,2412,2457,2474,95,124,49,44,42,41,18,46,39,9,16,50,7,57,11,45,6,14,48,35,38,8,17,13,36,5,10,12,4,15,2,62,67,56,43,66,40,54,24])). % 117.98/118.53 cnf(2580,plain, % 117.98/118.53 (P2(f7(f9(f6(a11,a1)),f9(f6(a11,a1))))), % 117.98/118.53 inference(scs_inference,[],[850,2416,2408,2448,2412,2457,2474,95,124,49,44,42,41,18,46,39,9,16,50,7,57,11,45,6,14,48,35,38,8,17,13,36,5,10,12,4,15,2,62,67,56,43,66,40,54,24,55])). % 117.98/118.53 cnf(2582,plain, % 117.98/118.53 (E(f8(f6(a11,a1),a10),f6(f12(a11),a1))), % 117.98/118.53 inference(scs_inference,[],[850,2416,2408,2448,2412,2457,2474,118,95,124,49,44,42,41,18,46,39,9,16,50,7,57,11,45,6,14,48,35,38,8,17,13,36,5,10,12,4,15,2,62,67,56,43,66,40,54,24,55,3])). % 117.98/118.53 cnf(2583,plain, % 117.98/118.53 (~P5(f13(f3(f12(a11))),f13(f4(f3(a11))))), % 117.98/118.53 inference(scs_inference,[],[850,2416,2408,2448,2412,2457,2471,2474,118,95,124,49,44,42,41,18,46,39,9,16,50,7,57,11,45,6,14,48,35,38,8,17,13,36,5,10,12,4,15,2,62,67,56,43,66,40,54,24,55,3,25])). % 117.98/118.53 cnf(2586,plain, % 117.98/118.53 (~P4(f7(f6(a11,a1),a10),f2(a11,a11))), % 117.98/118.53 inference(scs_inference,[],[33,850,2416,2408,2448,2412,2422,2457,2471,2474,2433,2443,118,95,124,49,44,42,41,18,46,39,9,16,50,7,57,11,45,6,14,48,35,38,8,17,13,36,5,10,12,4,15,2,62,67,56,43,66,40,54,24,55,3,25,23,22])). % 117.98/118.53 cnf(2611,plain, % 117.98/118.53 (P4(f2(a11,a11),a10)), % 117.98/118.53 inference(scs_inference,[],[2509,278])). % 117.98/118.53 cnf(2614,plain, % 117.98/118.53 (P4(f8(f6(a11,a1),f6(a11,a1)),f8(f6(a11,a1),f6(a11,a1)))), % 117.98/118.53 inference(scs_inference,[],[2467,49,46])). % 117.98/118.53 cnf(2616,plain, % 117.98/118.53 (P5(f3(f12(a11)),f13(f3(f12(a11))))), % 117.98/118.53 inference(scs_inference,[],[2467,2450,49,46,50])). % 117.98/118.53 cnf(2620,plain, % 117.98/118.53 (P4(a10,f7(f8(f6(a11,a1),f6(a11,a1)),f8(f6(a11,a1),f6(a11,a1))))), % 117.98/118.53 inference(scs_inference,[],[2467,2450,49,46,50,42,57])). % 117.98/118.53 cnf(2622,plain, % 117.98/118.53 (~E(f13(f3(f12(a11))),a1)), % 117.98/118.53 inference(scs_inference,[],[2467,2450,49,46,50,42,57,35])). % 117.98/118.53 cnf(2630,plain, % 117.98/118.53 (E(f9(f9(f8(f6(a11,a1),f6(a11,a1)))),f8(f6(a11,a1),f6(a11,a1)))), % 117.98/118.53 inference(scs_inference,[],[2418,2467,2450,49,46,50,42,57,35,44,7,11,48,39])). % 117.98/118.53 cnf(2632,plain, % 117.98/118.53 (E(f7(f8(f6(a11,a1),f6(a11,a1)),a10),a10)), % 117.98/118.53 inference(scs_inference,[],[2418,2467,2450,49,46,50,42,57,35,44,7,11,48,39,41])). % 117.98/118.53 cnf(2635,plain, % 117.98/118.53 (P2(f9(f8(f6(a11,a1),f6(a11,a1))))), % 117.98/118.53 inference(scs_inference,[],[2418,2467,2450,49,46,50,42,57,35,44,7,11,48,39,41,6,38])). % 117.98/118.53 cnf(2644,plain, % 117.98/118.53 (P1(f13(f4(f3(a11))))), % 117.98/118.53 inference(scs_inference,[],[2418,2467,2450,2465,49,46,50,42,57,35,44,7,11,48,39,41,6,38,16,18,45,9,17,10,36])). % 117.98/118.53 cnf(2658,plain, % 117.98/118.53 (P2(f6(f12(a11),f3(f12(a11))))), % 117.98/118.53 inference(scs_inference,[],[94,2418,2467,2450,2465,95,49,46,50,42,57,35,44,7,11,48,39,41,6,38,16,18,45,9,17,10,36,14,8,5,13,12,4,15,2,67,62,56])). % 117.98/118.53 cnf(2660,plain, % 117.98/118.53 (E(f9(f7(a10,a10)),f7(a10,f9(a10)))), % 117.98/118.53 inference(scs_inference,[],[94,2418,2467,2450,2465,95,27,49,46,50,42,57,35,44,7,11,48,39,41,6,38,16,18,45,9,17,10,36,14,8,5,13,12,4,15,2,67,62,56,66])). % 117.98/118.53 cnf(2662,plain, % 117.98/118.53 (P1(f4(f13(f13(f3(a11)))))), % 117.98/118.53 inference(scs_inference,[],[94,2418,2467,2450,2465,2557,2550,95,27,49,46,50,42,57,35,44,7,11,48,39,41,6,38,16,18,45,9,17,10,36,14,8,5,13,12,4,15,2,67,62,56,66,40])). % 117.98/118.53 cnf(2666,plain, % 117.98/118.53 (P2(f8(f8(f6(a11,a1),f6(a11,a1)),f8(f6(a11,a1),f6(a11,a1))))), % 117.98/118.53 inference(scs_inference,[],[94,2418,2467,2450,2465,2557,2550,95,27,49,46,50,42,57,35,44,7,11,48,39,41,6,38,16,18,45,9,17,10,36,14,8,5,13,12,4,15,2,67,62,56,66,40,43,54])). % 117.98/118.53 cnf(2668,plain, % 117.98/118.53 (P2(f7(f8(f6(a11,a1),f6(a11,a1)),f8(f6(a11,a1),f6(a11,a1))))), % 117.98/118.53 inference(scs_inference,[],[94,2418,2467,2450,2465,2557,2550,95,27,49,46,50,42,57,35,44,7,11,48,39,41,6,38,16,18,45,9,17,10,36,14,8,5,13,12,4,15,2,67,62,56,66,40,43,54,55])). % 117.98/118.53 cnf(2670,plain, % 117.98/118.53 (~E(f3(f12(a11)),f13(f4(f3(a11))))), % 117.98/118.53 inference(scs_inference,[],[94,2418,2467,2450,2465,2557,2550,2579,95,27,49,46,50,42,57,35,44,7,11,48,39,41,6,38,16,18,45,9,17,10,36,14,8,5,13,12,4,15,2,67,62,56,66,40,43,54,55,24])). % 117.98/118.53 cnf(2671,plain, % 117.98/118.53 (~P5(f13(f4(f3(a11))),f3(a11))), % 117.98/118.53 inference(scs_inference,[],[94,2418,2467,2450,2465,2557,2550,2579,125,95,27,49,46,50,42,57,35,44,7,11,48,39,41,6,38,16,18,45,9,17,10,36,14,8,5,13,12,4,15,2,67,62,56,66,40,43,54,55,24,25])). % 117.98/118.53 cnf(2672,plain, % 117.98/118.53 (~E(f8(f2(f12(a11),f12(a11)),f7(f6(a11,f3(a11)),f6(a11,f3(a11)))),f7(a10,a10))), % 117.98/118.53 inference(scs_inference,[],[2564,94,2418,2467,2450,2465,2557,2550,2579,125,95,91,27,49,46,50,42,57,35,44,7,11,48,39,41,6,38,16,18,45,9,17,10,36,14,8,5,13,12,4,15,2,67,62,56,66,40,43,54,55,24,25,3])). % 117.98/118.53 cnf(2673,plain, % 117.98/118.53 (~P4(f8(f9(a10),a10),f8(f2(f12(a11),f12(a11)),f7(f6(a11,f3(a11)),f6(a11,f3(a11)))))), % 117.98/118.53 inference(scs_inference,[],[2564,94,688,2418,2467,2450,2465,2557,2550,2579,125,95,91,31,27,49,46,50,42,57,35,44,7,11,48,39,41,6,38,16,18,45,9,17,10,36,14,8,5,13,12,4,15,2,67,62,56,66,40,43,54,55,24,25,3,23])). % 117.98/118.53 cnf(2675,plain, % 117.98/118.53 (E(f8(f7(a10,a10),f7(a10,a10)),f7(a10,f8(a10,a10)))), % 117.98/118.53 inference(scs_inference,[],[33,2564,94,688,2418,2467,2450,2465,2424,2557,2550,2579,125,95,91,31,27,49,46,50,42,57,35,44,7,11,48,39,41,6,38,16,18,45,9,17,10,36,14,8,5,13,12,4,15,2,67,62,56,66,40,43,54,55,24,25,3,23,22,76])). % 117.98/118.53 cnf(2677,plain, % 117.98/118.53 (E(f8(f7(a10,a10),f7(a10,a10)),f7(f8(a10,a10),a10))), % 117.98/118.53 inference(scs_inference,[],[33,2564,94,688,2418,2467,2450,2465,2424,2557,2550,2579,125,95,91,31,27,49,46,50,42,57,35,44,7,11,48,39,41,6,38,16,18,45,9,17,10,36,14,8,5,13,12,4,15,2,67,62,56,66,40,43,54,55,24,25,3,23,22,76,77])). % 117.98/118.53 cnf(2681,plain, % 117.98/118.53 (E(f8(f8(a10,a10),a10),f8(a10,f8(a10,a10)))), % 117.98/118.53 inference(scs_inference,[],[33,2564,94,688,2418,2467,2450,2465,2424,2557,2550,2579,125,95,91,31,27,49,46,50,42,57,35,44,7,11,48,39,41,6,38,16,18,45,9,17,10,36,14,8,5,13,12,4,15,2,67,62,56,66,40,43,54,55,24,25,3,23,22,76,77,74,73])). % 117.98/118.53 cnf(2683,plain, % 117.98/118.53 (P4(f2(a11,a11),f8(f9(a10),a10))), % 117.98/118.53 inference(scs_inference,[],[33,2564,94,688,2418,2467,2450,2465,2424,2557,2550,2579,125,95,91,31,124,27,654,49,46,50,42,57,35,44,7,11,48,39,41,6,38,16,18,45,9,17,10,36,14,8,5,13,12,4,15,2,67,62,56,66,40,43,54,55,24,25,3,23,22,76,77,74,73,53])). % 117.98/118.53 cnf(2695,plain, % 117.98/118.53 (~P4(f7(f9(f6(a11,a1)),f9(f6(a11,a1))),f2(a11,a11))), % 117.98/118.53 inference(scs_inference,[],[33,2564,94,688,2418,2467,2450,2465,2424,2557,2550,2580,2541,2579,1380,2469,1378,1383,125,1377,95,91,31,124,27,654,49,46,50,42,57,35,44,7,11,48,39,41,6,38,16,18,45,9,17,10,36,14,8,5,13,12,4,15,2,67,62,56,66,40,43,54,55,24,25,3,23,22,76,77,74,73,53,72,71,78,79,65,69])). % 117.98/118.53 cnf(2701,plain, % 117.98/118.53 (~E(f13(f4(f13(f3(a11)))),a1)), % 117.98/118.53 inference(scs_inference,[],[2476,2575,49,35])). % 117.98/118.53 cnf(2703,plain, % 117.98/118.53 (E(f9(f9(f6(a11,f3(a11)))),f6(a11,f3(a11)))), % 117.98/118.53 inference(scs_inference,[],[2476,2575,49,35,39])). % 117.98/118.53 cnf(2709,plain, % 117.98/118.53 (P4(a10,f7(f6(f12(a11),f3(a11)),f6(f12(a11),f3(a11))))), % 117.98/118.53 inference(scs_inference,[],[2476,2455,2575,49,35,39,50,48,57])). % 117.98/118.53 cnf(2711,plain, % 117.98/118.53 (P4(f9(f9(f6(a11,a1))),f9(f9(f6(a11,a1))))), % 117.98/118.53 inference(scs_inference,[],[2476,2455,2552,2575,49,35,39,50,48,57,46])). % 117.98/118.53 cnf(2713,plain, % 117.98/118.53 (E(f7(f6(a11,f3(a11)),a10),a10)), % 117.98/118.53 inference(scs_inference,[],[2476,2455,2552,2575,49,35,39,50,48,57,46,41])). % 117.98/118.53 cnf(2717,plain, % 117.98/118.53 (E(f7(a10,f6(a11,f3(a11))),a10)), % 117.98/118.53 inference(scs_inference,[],[2476,2455,2552,2575,49,35,39,50,48,57,46,41,44,42])). % 117.98/118.53 cnf(2722,plain, % 117.98/118.53 (P1(f13(f4(f13(f3(a11)))))), % 117.98/118.53 inference(scs_inference,[],[2476,2455,2660,2552,2575,49,35,39,50,48,57,46,41,44,42,45,6,36])). % 117.98/118.53 cnf(2728,plain, % 117.98/118.53 (P2(f9(f6(a11,f3(a11))))), % 117.98/118.53 inference(scs_inference,[],[2476,2455,2660,2552,2575,49,35,39,50,48,57,46,41,44,42,45,6,36,16,11,9,7,38])). % 117.98/118.53 cnf(2740,plain, % 117.98/118.53 (~E(f2(a11,a11),f7(f9(a10),f9(a10)))), % 117.98/118.53 inference(scs_inference,[],[579,2476,2455,2660,2552,2575,49,35,39,50,48,57,46,41,44,42,45,6,36,16,11,9,7,38,17,18,13,10,8,5,14,4,12,15,2])). % 117.98/118.53 cnf(2745,plain, % 117.98/118.53 (P2(f6(f12(a11),f4(f13(f3(a11)))))), % 117.98/118.53 inference(scs_inference,[],[579,2476,2455,2660,2552,2575,95,49,35,39,50,48,57,46,41,44,42,45,6,36,16,11,9,7,38,17,18,13,10,8,5,14,4,12,15,2,62,67,56])). % 117.98/118.53 cnf(2747,plain, % 117.98/118.53 (P1(f4(f13(f3(f12(a11)))))), % 117.98/118.53 inference(scs_inference,[],[579,2476,2455,2660,2552,2575,2622,875,95,49,35,39,50,48,57,46,41,44,42,45,6,36,16,11,9,7,38,17,18,13,10,8,5,14,4,12,15,2,62,67,56,40])). % 117.98/118.53 cnf(2749,plain, % 117.98/118.53 (E(f13(f4(f13(f3(f12(a11))))),f13(f3(f12(a11))))), % 117.98/118.53 inference(scs_inference,[],[579,2476,2455,2660,2552,2575,2622,875,95,49,35,39,50,48,57,46,41,44,42,45,6,36,16,11,9,7,38,17,18,13,10,8,5,14,4,12,15,2,62,67,56,40,43])). % 117.98/118.53 cnf(2753,plain, % 117.98/118.53 (P2(f8(f6(a11,f3(a11)),f6(a11,f3(a11))))), % 117.98/118.53 inference(scs_inference,[],[579,2476,2455,2660,2552,2575,2622,875,95,133,49,35,39,50,48,57,46,41,44,42,45,6,36,16,11,9,7,38,17,18,13,10,8,5,14,4,12,15,2,62,67,56,40,43,66,54])). % 117.98/118.53 cnf(2755,plain, % 117.98/118.53 (P2(f7(f6(a11,f3(a11)),f6(a11,f3(a11))))), % 117.98/118.53 inference(scs_inference,[],[579,2476,2455,2660,2552,2575,2622,875,95,133,49,35,39,50,48,57,46,41,44,42,45,6,36,16,11,9,7,38,17,18,13,10,8,5,14,4,12,15,2,62,67,56,40,43,66,54,55])). % 117.98/118.53 cnf(2757,plain, % 117.98/118.53 (~P5(f3(a11),f13(f4(f3(a11))))), % 117.98/118.53 inference(scs_inference,[],[579,2476,2455,2660,2552,2575,2622,2583,875,125,95,133,49,35,39,50,48,57,46,41,44,42,45,6,36,16,11,9,7,38,17,18,13,10,8,5,14,4,12,15,2,62,67,56,40,43,66,54,55,24])). % 117.98/118.53 cnf(2758,plain, % 117.98/118.53 (E(f9(f7(a10,a10)),f9(a10))), % 117.98/118.53 inference(scs_inference,[],[579,2476,2455,2660,2552,2575,2622,2583,612,875,125,95,133,49,35,39,50,48,57,46,41,44,42,45,6,36,16,11,9,7,38,17,18,13,10,8,5,14,4,12,15,2,62,67,56,40,43,66,54,55,24,3])). % 117.98/118.53 cnf(2761,plain, % 117.98/118.53 (~P4(f9(f7(a10,a10)),f2(a11,a11))), % 117.98/118.53 inference(scs_inference,[],[579,2476,2455,2660,2414,2552,2575,2622,2583,2571,612,875,125,593,95,133,49,35,39,50,48,57,46,41,44,42,45,6,36,16,11,9,7,38,17,18,13,10,8,5,14,4,12,15,2,62,67,56,40,43,66,54,55,24,3,25,23,22])). % 117.98/118.53 cnf(2776,plain, % 117.98/118.53 (E(f9(f7(a10,a10)),a10)), % 117.98/118.53 inference(scs_inference,[],[579,793,2476,2455,2512,2660,2414,2552,2575,2622,2668,2620,2583,2571,612,875,125,593,95,124,133,757,49,35,39,50,48,57,46,41,44,42,45,6,36,16,11,9,7,38,17,18,13,10,8,5,14,4,12,15,2,62,67,56,40,43,66,54,55,24,3,25,23,22,77,76,74,73,53,72,78,127])). % 117.98/118.53 cnf(2790,plain, % 117.98/118.53 (P1(f13(f13(f4(f3(a11)))))), % 117.98/118.53 inference(scs_inference,[],[2635,2644,49,57,39,45,36])). % 117.98/118.53 cnf(2794,plain, % 117.98/118.53 (~E(f13(f13(f4(f3(a11)))),a1)), % 117.98/118.53 inference(scs_inference,[],[2635,2644,49,57,39,45,36,48,35])). % 117.98/118.53 cnf(2798,plain, % 117.98/118.53 (E(f8(f9(f8(f6(a11,a1),f6(a11,a1))),a10),f9(f8(f6(a11,a1),f6(a11,a1))))), % 117.98/118.53 inference(scs_inference,[],[2635,2644,49,57,39,45,36,48,35,42,44])). % 117.98/118.53 cnf(2804,plain, % 117.98/118.53 (P5(f13(f4(f3(a11))),f13(f13(f4(f3(a11)))))), % 117.98/118.53 inference(scs_inference,[],[2635,2644,49,57,39,45,36,48,35,42,44,41,46,50])). % 117.98/118.53 cnf(2806,plain, % 117.98/118.53 (P2(f9(f9(f8(f6(a11,a1),f6(a11,a1)))))), % 117.98/118.53 inference(scs_inference,[],[2635,2644,49,57,39,45,36,48,35,42,44,41,46,50,38])). % 117.98/118.53 cnf(2823,plain, % 117.98/118.53 (~E(f13(a1),f13(f3(a11)))), % 117.98/118.53 inference(scs_inference,[],[2758,2479,2635,2644,49,57,39,45,36,48,35,42,44,41,46,50,38,11,6,7,16,9,17,13,14,18,5,8,10,12,4,15,2])). % 117.98/118.53 cnf(2828,plain, % 117.98/118.53 (P2(f6(f12(a11),f13(f4(f3(a11)))))), % 117.98/118.53 inference(scs_inference,[],[2758,2479,2635,2644,2455,95,49,57,39,45,36,48,35,42,44,41,46,50,38,11,6,7,16,9,17,13,14,18,5,8,10,12,4,15,2,67,62,56])). % 117.98/118.53 cnf(2830,plain, % 117.98/118.53 (P2(f8(f9(f8(f6(a11,a1),f6(a11,a1))),f9(f8(f6(a11,a1),f6(a11,a1)))))), % 117.98/118.53 inference(scs_inference,[],[2758,2479,2635,2644,2455,95,49,57,39,45,36,48,35,42,44,41,46,50,38,11,6,7,16,9,17,13,14,18,5,8,10,12,4,15,2,67,62,56,54])). % 117.98/118.53 cnf(2836,plain, % 117.98/118.53 (~P5(f13(f4(f3(a11))),f13(f4(f3(a11))))), % 117.98/118.53 inference(scs_inference,[],[2758,2479,2635,2644,2757,2722,2701,2455,2457,95,49,57,39,45,36,48,35,42,44,41,46,50,38,11,6,7,16,9,17,13,14,18,5,8,10,12,4,15,2,67,62,56,54,40,55,24])). % 117.98/118.53 cnf(2837,plain, % 117.98/118.53 (~E(f13(f3(a11)),f13(f4(f3(a11))))), % 117.98/118.53 inference(scs_inference,[],[2758,2479,2410,2635,2644,2757,2722,2701,2455,2457,95,49,57,39,45,36,48,35,42,44,41,46,50,38,11,6,7,16,9,17,13,14,18,5,8,10,12,4,15,2,67,62,56,54,40,55,24,25])). % 117.98/118.53 cnf(2840,plain, % 117.98/118.53 (~E(f2(a11,a11),f9(f7(a10,a10)))), % 117.98/118.53 inference(scs_inference,[],[2454,2507,2761,2758,2479,2410,2635,2644,2757,2722,2701,2455,2457,136,91,95,31,49,57,39,45,36,48,35,42,44,41,46,50,38,11,6,7,16,9,17,13,14,18,5,8,10,12,4,15,2,67,62,56,54,40,55,24,25,3,23,22])). % 117.98/118.53 cnf(2843,plain, % 117.98/118.53 (P4(f8(f9(f8(f6(a11,a1),f6(a11,a1))),f2(a11,a11)),f8(f9(f8(f6(a11,a1),f6(a11,a1))),a10))), % 117.98/118.53 inference(scs_inference,[],[2509,2454,2507,2761,2758,2479,2410,2635,2644,2757,2722,2701,2455,2457,2469,136,91,95,31,124,27,49,57,39,45,36,48,35,42,44,41,46,50,38,11,6,7,16,9,17,13,14,18,5,8,10,12,4,15,2,67,62,56,54,40,55,24,25,3,23,22,53,78])). % 117.98/118.53 cnf(2859,plain, % 117.98/118.53 (P2(f9(f9(f6(a11,f3(a11)))))), % 117.98/118.53 inference(scs_inference,[],[2728,48,49,46,38])). % 117.98/118.53 cnf(2873,plain, % 117.98/118.53 (P5(f4(f3(a11)),f13(f4(f3(a11))))), % 117.98/118.53 inference(scs_inference,[],[2728,2662,2465,48,49,46,38,39,36,57,41,44,42,50])). % 117.98/118.53 cnf(2875,plain, % 117.98/118.53 (~E(f13(f4(f13(f13(f3(a11))))),a1)), % 117.98/118.53 inference(scs_inference,[],[2728,2662,2465,48,49,46,38,39,36,57,41,44,42,50,35])). % 117.98/118.53 cnf(2880,plain, % 117.98/118.53 (E(f3(f9(f7(a10,a10))),f3(a10))), % 117.98/118.53 inference(scs_inference,[],[2776,2728,2662,2465,48,49,46,38,39,36,57,41,44,42,50,35,45,6,9])). % 117.98/118.53 cnf(2881,plain, % 117.98/118.53 (E(f6(x28811,f9(f7(a10,a10))),f6(x28811,a10))), % 117.98/118.53 inference(scs_inference,[],[2776,2728,2662,2465,48,49,46,38,39,36,57,41,44,42,50,35,45,6,9,11])). % 117.98/118.53 cnf(2882,plain, % 117.98/118.53 (E(f4(f9(f7(a10,a10))),f4(a10))), % 117.98/118.53 inference(scs_inference,[],[2776,2728,2662,2465,48,49,46,38,39,36,57,41,44,42,50,35,45,6,9,11,16])). % 117.98/118.53 cnf(2883,plain, % 117.98/118.53 (E(f2(f9(f7(a10,a10)),x28831),f2(a10,x28831))), % 117.98/118.53 inference(scs_inference,[],[2776,2728,2662,2465,48,49,46,38,39,36,57,41,44,42,50,35,45,6,9,11,16,7])). % 117.98/118.53 cnf(2884,plain, % 117.98/118.53 (E(f5(f9(f7(a10,a10)),x28841),f5(a10,x28841))), % 117.98/118.53 inference(scs_inference,[],[2776,2728,2662,2465,48,49,46,38,39,36,57,41,44,42,50,35,45,6,9,11,16,7,17])). % 117.98/118.53 cnf(2886,plain, % 117.98/118.53 (E(f8(x28861,f9(f7(a10,a10))),f8(x28861,a10))), % 117.98/118.53 inference(scs_inference,[],[2776,2728,2662,2465,48,49,46,38,39,36,57,41,44,42,50,35,45,6,9,11,16,7,17,14,13])). % 117.98/118.53 cnf(2887,plain, % 117.98/118.53 (E(f6(f9(f7(a10,a10)),x28871),f6(a10,x28871))), % 117.98/118.53 inference(scs_inference,[],[2776,2728,2662,2465,48,49,46,38,39,36,57,41,44,42,50,35,45,6,9,11,16,7,17,14,13,10])). % 117.98/118.53 cnf(2888,plain, % 117.98/118.53 (E(f2(x28881,f9(f7(a10,a10))),f2(x28881,a10))), % 117.98/118.53 inference(scs_inference,[],[2776,2728,2662,2465,48,49,46,38,39,36,57,41,44,42,50,35,45,6,9,11,16,7,17,14,13,10,8])). % 117.98/118.53 cnf(2889,plain, % 117.98/118.53 (E(f5(x28891,f9(f7(a10,a10))),f5(x28891,a10))), % 117.98/118.53 inference(scs_inference,[],[2776,2728,2662,2465,48,49,46,38,39,36,57,41,44,42,50,35,45,6,9,11,16,7,17,14,13,10,8,18])). % 117.98/118.53 cnf(2890,plain, % 117.98/118.53 (E(f7(f9(f7(a10,a10)),x28901),f7(a10,x28901))), % 117.98/118.53 inference(scs_inference,[],[2776,2728,2662,2465,48,49,46,38,39,36,57,41,44,42,50,35,45,6,9,11,16,7,17,14,13,10,8,18,5])). % 117.98/118.53 cnf(2891,plain, % 117.98/118.53 (E(f12(f9(f7(a10,a10))),f12(a10))), % 117.98/118.53 inference(scs_inference,[],[2776,2728,2662,2465,48,49,46,38,39,36,57,41,44,42,50,35,45,6,9,11,16,7,17,14,13,10,8,18,5,4])). % 117.98/118.53 cnf(2892,plain, % 117.98/118.53 (E(f8(f9(f7(a10,a10)),x28921),f8(a10,x28921))), % 117.98/118.53 inference(scs_inference,[],[2776,2728,2662,2465,48,49,46,38,39,36,57,41,44,42,50,35,45,6,9,11,16,7,17,14,13,10,8,18,5,4,12])). % 117.98/118.53 cnf(2894,plain, % 117.98/118.53 (E(f13(f9(f7(a10,a10))),f13(a10))), % 117.98/118.53 inference(scs_inference,[],[2840,2776,2728,2662,2465,48,49,46,38,39,36,57,41,44,42,50,35,45,6,9,11,16,7,17,14,13,10,8,18,5,4,12,2,15])). % 117.98/118.53 cnf(2907,plain, % 117.98/118.53 (~P5(f13(f4(f13(f3(f12(a11))))),f3(a11))), % 117.98/118.53 inference(scs_inference,[],[2840,2776,2728,2662,2790,2794,2749,2465,2471,2472,95,48,49,46,38,39,36,57,41,44,42,50,35,45,6,9,11,16,7,17,14,13,10,8,18,5,4,12,2,15,62,67,56,54,40,55,24])). % 117.98/118.53 cnf(2908,plain, % 117.98/118.53 (E(f8(f9(f6(a11,a1)),f6(a11,a1)),f7(a10,f9(a10)))), % 117.98/118.53 inference(scs_inference,[],[2840,2776,2431,2728,2662,2790,2794,2749,2465,2471,2472,580,95,48,49,46,38,39,36,57,41,44,42,50,35,45,6,9,11,16,7,17,14,13,10,8,18,5,4,12,2,15,62,67,56,54,40,55,24,3])). % 117.98/118.53 cnf(2909,plain, % 117.98/118.53 (~P5(f3(a11),f13(f4(f13(f3(f12(a11))))))), % 117.98/118.53 inference(scs_inference,[],[2840,2776,2431,2728,2662,2790,2794,2749,2465,2471,2474,2472,580,95,48,49,46,38,39,36,57,41,44,42,50,35,45,6,9,11,16,7,17,14,13,10,8,18,5,4,12,2,15,62,67,56,54,40,55,24,3,25])). % 117.98/118.53 cnf(2911,plain, % 117.98/118.53 (~P4(f8(f9(f6(a11,a1)),f6(a11,a1)),f2(a11,a11))), % 117.98/118.53 inference(scs_inference,[],[33,2840,2776,2431,2728,2662,2790,2794,2798,2843,2749,2465,2471,2474,2472,580,95,48,49,46,38,39,36,57,41,44,42,50,35,45,6,9,11,16,7,17,14,13,10,8,18,5,4,12,2,15,62,67,56,54,40,55,24,3,25,23,22])). % 117.98/118.53 cnf(2916,plain, % 117.98/118.53 (E(f9(f9(f7(a10,a10))),a10)), % 117.98/118.53 inference(scs_inference,[],[33,2611,2840,2776,2431,2728,2695,2662,2790,2794,2798,2843,2749,2465,2471,2474,2472,580,2580,95,124,27,48,49,46,38,39,36,57,41,44,42,50,35,45,6,9,11,16,7,17,14,13,10,8,18,5,4,12,2,15,62,67,56,54,40,55,24,3,25,23,22,53,78,127])). % 117.98/118.53 cnf(2937,plain, % 117.98/118.53 (P2(f9(f6(f12(a11),f13(f3(a11)))))), % 117.98/118.53 inference(scs_inference,[],[2569,49,48,39,38])). % 117.98/118.53 cnf(2953,plain, % 117.98/118.53 (~E(f13(f4(f13(f3(f12(a11))))),a1)), % 117.98/118.53 inference(scs_inference,[],[2569,2747,2557,49,48,39,38,36,44,57,42,46,41,50,35])). % 117.98/118.53 cnf(2983,plain, % 117.98/118.53 (~E(f4(f3(a11)),f13(f4(f3(a11))))), % 117.98/118.53 inference(scs_inference,[],[2675,1088,2569,2873,2836,2747,2557,1932,95,49,48,39,38,36,44,57,42,46,41,50,35,45,11,9,6,7,16,13,17,14,18,8,10,4,5,12,2,15,62,67,56,54,55,24])). % 117.98/118.53 cnf(2984,plain, % 117.98/118.53 (~E(f8(f2(f12(a11),f12(a11)),f7(f6(a11,f3(a11)),f6(a11,f3(a11)))),f7(a10,f9(a10)))), % 117.98/118.53 inference(scs_inference,[],[581,2675,1088,2569,2873,2836,2747,2557,1932,91,95,49,48,39,38,36,44,57,42,46,41,50,35,45,11,9,6,7,16,13,17,14,18,8,10,4,5,12,2,15,62,67,56,54,55,24,3])). % 117.98/118.53 cnf(2985,plain, % 117.98/118.53 (~E(f13(f13(f4(f3(a11)))),f13(f4(f3(a11))))), % 117.98/118.53 inference(scs_inference,[],[581,2675,1088,2569,2873,2836,2747,2804,2557,1932,91,95,49,48,39,38,36,44,57,42,46,41,50,35,45,11,9,6,7,16,13,17,14,18,8,10,4,5,12,2,15,62,67,56,54,55,24,3,25])). % 117.98/118.53 cnf(2987,plain, % 117.98/118.53 (~P4(f8(f6(a11,a1),f9(f6(a11,a1))),f2(a11,a11))), % 117.98/118.53 inference(scs_inference,[],[33,2586,581,2675,1088,2569,2429,2873,2836,2747,2804,2557,1932,91,95,31,49,48,39,38,36,44,57,42,46,41,50,35,45,11,9,6,7,16,13,17,14,18,8,10,4,5,12,2,15,62,67,56,54,55,24,3,25,23,22])). % 117.98/118.53 cnf(3002,plain, % 117.98/118.53 (P2(f9(f6(f12(a11),f3(f12(a11)))))), % 117.98/118.53 inference(scs_inference,[],[2658,48,49,38])). % 117.98/118.53 cnf(3020,plain, % 117.98/118.53 (~E(f13(f13(f4(f13(f3(a11))))),a1)), % 117.98/118.53 inference(scs_inference,[],[2658,2722,883,48,49,38,36,44,57,46,39,41,42,50,35])). % 117.98/118.53 cnf(3038,plain, % 117.98/118.53 (~E(f2(a11,a11),f7(f9(a10),f8(f9(a10),a10)))), % 117.98/118.53 inference(scs_inference,[],[2677,1442,2658,2722,883,48,49,38,36,44,57,46,39,41,42,50,35,45,6,9,16,7,11,14,8,13,10,17,18,5,12,4,2])). % 117.98/118.53 cnf(3048,plain, % 117.98/118.53 (~P5(f13(f4(f13(f3(f12(a11))))),f13(f4(f3(a11))))), % 117.98/118.53 inference(scs_inference,[],[2677,1442,2658,2583,2722,2749,194,883,48,49,38,36,44,57,46,39,41,42,50,35,45,6,9,16,7,11,14,8,13,10,17,18,5,12,4,2,15,62,67,54,55,24])). % 117.98/118.53 cnf(3077,plain, % 117.98/118.53 (P2(f9(f8(f9(f6(a11,a1)),f9(f6(a11,a1)))))), % 117.98/118.53 inference(scs_inference,[],[2577,2790,2552,49,48,44,36,57,46,41,38])). % 117.98/118.53 cnf(3115,plain, % 117.98/118.53 (~E(f8(f2(f12(a11),f12(a11)),f7(f6(a11,f3(a11)),f6(a11,f3(a11)))),f7(f9(a10),f9(a10)))), % 117.98/118.53 inference(scs_inference,[],[2740,2681,1976,2577,2909,2410,2790,2552,2457,2469,91,26,49,48,44,36,57,46,41,38,42,39,45,35,50,9,16,11,6,7,13,17,14,18,8,10,12,5,4,2,15,62,67,54,55,24,25,3])). % 117.98/118.53 cnf(3116,plain, % 117.98/118.53 (~P4(f9(f9(f7(a10,a10))),f2(a11,a11))), % 117.98/118.53 inference(scs_inference,[],[33,2740,2681,1976,2916,2577,2909,2410,2790,2552,2457,2469,91,26,49,48,44,36,57,46,41,38,42,39,45,35,50,9,16,11,6,7,13,17,14,18,8,10,12,5,4,2,15,62,67,54,55,24,25,3,22])). % 117.98/118.53 cnf(3132,plain, % 117.98/118.53 (P1(f13(f13(f13(f3(a11)))))), % 117.98/118.53 inference(scs_inference,[],[2557,2455,48,49,36])). % 117.98/118.53 cnf(3148,plain, % 117.98/118.53 (~E(f13(f4(f3(a11))),a1)), % 117.98/118.53 inference(scs_inference,[],[2806,2753,2465,2557,2455,48,49,36,57,46,41,44,42,38,39,35])). % 117.98/118.53 cnf(3166,plain, % 117.98/118.53 (~E(f13(f4(f3(a11))),f3(f12(a11)))), % 117.98/118.53 inference(scs_inference,[],[2582,2670,2806,2753,2465,2557,2455,48,49,36,57,46,41,44,42,38,39,35,45,16,11,9,7,6,14,8,10,13,17,18,5,4,12,2])). % 117.98/118.53 cnf(3168,plain, % 117.98/118.53 (E(f13(f4(f13(f4(f3(a11))))),f13(f4(f3(a11))))), % 117.98/118.53 inference(scs_inference,[],[2582,2670,2806,2753,2465,2557,2455,2644,48,49,36,57,46,41,44,42,38,39,35,45,16,11,9,7,6,14,8,10,13,17,18,5,4,12,2,15,43])). % 117.98/118.53 cnf(3172,plain, % 117.98/118.53 (P1(f4(f13(f4(f3(a11)))))), % 117.98/118.53 inference(scs_inference,[],[2582,2670,2806,2753,2465,2557,2455,2644,510,48,49,36,57,46,41,44,42,38,39,35,45,16,11,9,7,6,14,8,10,13,17,18,5,4,12,2,15,43,62,40])). % 117.98/118.53 cnf(3180,plain, % 117.98/118.53 (~P5(f13(f3(f12(a11))),f13(f3(f12(a11))))), % 117.98/118.53 inference(scs_inference,[],[2582,2670,2806,2753,2474,2465,2557,2455,2644,510,97,48,49,36,57,46,41,44,42,38,39,35,45,16,11,9,7,6,14,8,10,13,17,18,5,4,12,2,15,43,62,40,67,54,55,24])). % 117.98/118.53 cnf(3181,plain, % 117.98/118.53 (E(f6(f9(f7(a10,a10)),f9(f7(a10,a10))),f6(a10,a10))), % 117.98/118.53 inference(scs_inference,[],[2582,2881,2887,2670,2806,2753,2474,2465,2557,2455,2644,510,97,48,49,36,57,46,41,44,42,38,39,35,45,16,11,9,7,6,14,8,10,13,17,18,5,4,12,2,15,43,62,40,67,54,55,24,3])). % 117.98/118.53 cnf(3186,plain, % 117.98/118.53 (P4(f9(f9(f8(f6(a11,a1),f6(a11,a1)))),f8(f6(a11,a1),f6(a11,a1)))), % 117.98/118.53 inference(scs_inference,[],[2582,2881,2886,2887,2670,2806,2630,2673,2753,2474,2465,2557,2455,2644,510,97,48,49,36,57,46,41,44,42,38,39,35,45,16,11,9,7,6,14,8,10,13,17,18,5,4,12,2,15,43,62,40,67,54,55,24,3,22,23])). % 117.98/118.53 cnf(3189,plain, % 117.98/118.53 (P4(a10,f7(f7(f9(a10),a10),f7(f9(a10),a10)))), % 117.98/118.53 inference(scs_inference,[],[2582,2881,2886,2887,2670,2806,2630,2673,2753,2474,2465,2557,2455,2644,519,121,510,97,654,48,49,36,57,46,41,44,42,38,39,35,45,16,11,9,7,6,14,8,10,13,17,18,5,4,12,2,15,43,62,40,67,54,55,24,3,22,23,53,72])). % 117.98/118.53 cnf(3204,plain, % 117.98/118.53 (P4(f9(f9(f6(a11,f3(a11)))),f9(f9(f6(a11,f3(a11)))))), % 117.98/118.53 inference(scs_inference,[],[2859,2666,2472,49,48,57,46])). % 117.98/118.53 cnf(3236,plain, % 117.98/118.53 (~E(a1,f13(f4(f3(a11))))), % 117.98/118.53 inference(scs_inference,[],[2883,3148,2859,3132,2666,2472,49,48,57,46,41,44,36,38,42,39,45,35,9,7,16,11,6,14,13,18,10,8,17,5,12,4,2])). % 117.98/118.53 cnf(3248,plain, % 117.98/118.53 (~P5(f13(f4(f13(f4(f3(a11))))),f3(a11))), % 117.98/118.53 inference(scs_inference,[],[2883,2671,3148,2859,3132,3168,2666,2472,95,583,49,48,57,46,41,44,36,38,42,39,45,35,9,7,16,11,6,14,13,18,10,8,17,5,12,4,2,15,62,56,67,54,55,24])). % 117.98/118.53 cnf(3250,plain, % 117.98/118.53 (~E(f13(a1),f13(f4(f13(f3(a11)))))), % 117.98/118.53 inference(scs_inference,[],[2823,2883,2671,3148,3180,2859,3132,3168,2666,2571,2749,2472,95,583,49,48,57,46,41,44,36,38,42,39,45,35,9,7,16,11,6,14,13,18,10,8,17,5,12,4,2,15,62,56,67,54,55,24,25,3])). % 117.98/118.53 cnf(3251,plain, % 117.98/118.53 (~P4(f7(a10,f9(f6(a11,a1))),f2(a11,a11))), % 117.98/118.53 inference(scs_inference,[],[33,2823,2883,2671,3148,2527,3180,2859,3132,3168,2666,2571,2749,2472,95,583,49,48,57,46,41,44,36,38,42,39,45,35,9,7,16,11,6,14,13,18,10,8,17,5,12,4,2,15,62,56,67,54,55,24,25,3,22])). % 117.98/118.53 cnf(3253,plain, % 117.98/118.53 (~E(f13(f13(f4(f13(f3(a11))))),f13(a1))), % 117.98/118.53 inference(scs_inference,[],[33,2823,2911,2883,2671,3148,2527,3180,2859,3132,3168,2666,2701,2571,2722,2749,2472,26,95,583,31,49,48,57,46,41,44,36,38,42,39,45,35,9,7,16,11,6,14,13,18,10,8,17,5,12,4,2,15,62,56,67,54,55,24,25,3,22,23,51])). % 117.98/118.53 cnf(3257,plain, % 117.98/118.53 (P4(a10,f8(f7(f6(a11,a1),f6(a11,a1)),f7(f6(a11,a1),f6(a11,a1))))), % 117.98/118.53 inference(scs_inference,[],[33,2823,2911,2883,2671,3148,2527,3180,2859,3132,3168,2666,1384,2701,2571,2420,2722,2749,2472,1377,26,95,583,31,124,49,48,57,46,41,44,36,38,42,39,45,35,9,7,16,11,6,14,13,18,10,8,17,5,12,4,2,15,62,56,67,54,55,24,25,3,22,23,51,53,71])). % 117.98/118.53 cnf(3303,plain, % 117.98/118.53 (~E(f13(f4(f3(a11))),f13(f3(a11)))), % 117.98/118.53 inference(scs_inference,[],[2884,2837,3172,3002,2668,2552,1932,48,49,46,41,44,36,57,42,38,39,35,45,16,11,9,7,14,6,10,13,5,17,18,8,4,12,2])). % 117.98/118.53 cnf(3315,plain, % 117.98/118.53 (~P5(f13(f4(f13(f3(f12(a11))))),f13(f3(f12(a11))))), % 117.98/118.53 inference(scs_inference,[],[2884,2837,3172,3002,2907,2668,2552,1932,95,124,97,48,49,46,41,44,36,57,42,38,39,35,45,16,11,9,7,14,6,10,13,5,17,18,8,4,12,2,15,62,56,67,54,55,25])). % 117.98/118.53 cnf(3316,plain, % 117.98/118.53 (E(f5(f9(f7(a10,a10)),f9(f7(a10,a10))),f5(a10,a10))), % 117.98/118.53 inference(scs_inference,[],[2884,2889,2837,3172,3002,2907,2668,2552,1932,95,124,97,48,49,46,41,44,36,57,42,38,39,35,45,16,11,9,7,14,6,10,13,5,17,18,8,4,12,2,15,62,56,67,54,55,25,3])). % 117.98/118.53 cnf(3322,plain, % 117.98/118.53 (~E(f13(a1),f13(f13(f4(f3(a11)))))), % 117.98/118.53 inference(scs_inference,[],[2884,2889,2890,3251,3236,2837,3257,2487,3172,3002,2907,2668,2552,1932,2644,26,95,124,97,48,49,46,41,44,36,57,42,38,39,35,45,16,11,9,7,14,6,10,13,5,17,18,8,4,12,2,15,62,56,67,54,55,25,3,22,23,51])). % 117.98/118.53 cnf(3326,plain, % 117.98/118.53 (P4(f8(f9(f9(f8(f6(a11,a1),f6(a11,a1)))),f2(a11,a11)),f8(f8(f6(a11,a1),f6(a11,a1)),f8(f9(a10),a10)))), % 117.98/118.53 inference(scs_inference,[],[2683,2884,2889,2890,3251,3236,2837,3257,2487,3172,3002,3186,2907,466,2668,2806,2552,1932,2644,2467,26,95,124,97,654,451,48,49,46,41,44,36,57,42,38,39,35,45,16,11,9,7,14,6,10,13,5,17,18,8,4,12,2,15,62,56,67,54,55,25,3,22,23,51,53,78])). % 117.98/118.53 cnf(3332,plain, % 117.98/118.53 (E(f8(f9(f9(f2(a11,a11))),f9(f2(a11,a11))),a10)), % 117.98/118.53 inference(scs_inference,[],[194,49])). % 117.98/118.53 cnf(3340,plain, % 117.98/118.53 (P1(f13(f13(f3(f12(a11)))))), % 117.98/118.53 inference(scs_inference,[],[2745,2755,194,883,49,48,41,44,36])). % 117.98/118.53 cnf(3354,plain, % 117.98/118.53 (~E(f13(f13(f13(f3(a11)))),a1)), % 117.98/118.53 inference(scs_inference,[],[2745,2755,2557,194,883,49,48,41,44,36,57,46,38,42,39,45,35])). % 117.98/118.53 cnf(3370,plain, % 117.98/118.53 (~E(f13(f4(f3(a11))),f4(f3(a11)))), % 117.98/118.53 inference(scs_inference,[],[2888,2983,2745,2755,2557,194,883,49,48,41,44,36,57,46,38,42,39,45,35,9,7,16,6,11,14,5,18,8,10,13,17,12,4,2])). % 117.98/118.53 cnf(3383,plain, % 117.98/118.53 (~P5(f13(f4(f13(f4(f3(a11))))),f13(f4(f3(a11))))), % 117.98/118.53 inference(scs_inference,[],[2888,2983,2745,3248,3048,2873,2755,3132,2457,2557,194,883,133,49,48,41,44,36,57,46,38,42,39,45,35,9,7,16,6,11,14,5,18,8,10,13,17,12,4,2,15,62,40,67,54,55,24,25])). % 117.98/118.53 cnf(3387,plain, % 117.98/118.53 (P4(f2(a11,a11),f7(a10,f9(a10)))), % 117.98/118.53 inference(scs_inference,[],[33,2987,2888,1310,2529,2983,2745,3248,3048,2873,2755,3132,2457,2557,194,883,593,91,583,31,124,133,49,48,41,44,36,57,46,38,42,39,45,35,9,7,16,6,11,14,5,18,8,10,13,17,12,4,2,15,62,40,67,54,55,24,25,3,22,23,53])). % 117.98/118.53 cnf(3438,plain, % 117.98/118.53 (E(f7(f9(a10),f9(a10)),f7(a10,a10))), % 117.98/118.53 inference(scs_inference,[],[2892,1827,3340,2828,2580,1932,2469,27,49,48,41,46,57,36,39,38,42,44,45,35,16,14,9,6,11,7,5,8,10,13,18,17,12,4,2,15,62])). % 117.98/118.53 cnf(3442,plain, % 117.98/118.53 (E(f9(f7(a10,a10)),f7(f9(a10),a10))), % 117.98/118.53 inference(scs_inference,[],[2892,1827,3340,2828,2580,1932,2469,95,27,49,48,41,46,57,36,39,38,42,44,45,35,16,14,9,6,11,7,5,8,10,13,18,17,12,4,2,15,62,56,67])). % 117.98/118.53 cnf(3476,plain, % 117.98/118.53 (P1(f13(a1))), % 117.98/118.53 inference(scs_inference,[],[3077,1377,26,49,48,41,39,42,36])). % 117.98/118.53 cnf(3505,plain, % 117.98/118.53 (~E(f13(f4(f13(f3(a11)))),f13(a1))), % 117.98/118.53 inference(scs_inference,[],[3438,3250,3077,2937,2552,875,1377,26,583,49,48,41,39,42,36,44,57,38,46,45,35,9,7,6,16,11,14,10,5,13,8,18,17,4,12,15,2])). % 117.98/118.53 cnf(3518,plain, % 117.98/118.53 (~P5(f3(a11),f13(f4(f13(f4(f3(a11))))))), % 117.98/118.53 inference(scs_inference,[],[3438,3250,3077,2937,3168,2757,2722,3340,2552,875,1377,26,583,95,654,49,48,41,39,42,36,44,57,38,46,45,35,9,7,6,16,11,14,10,5,13,8,18,17,4,12,15,2,62,40,56,67,54,55,25])). % 117.98/118.53 cnf(3543,plain, % 117.98/118.53 (P1(f13(f13(a1)))), % 117.98/118.53 inference(scs_inference,[],[3476,2830,2455,510,49,48,41,44,38,36])). % 117.98/118.53 cnf(3555,plain, % 117.98/118.53 (~E(f13(f13(a1)),a1)), % 117.98/118.53 inference(scs_inference,[],[3476,2830,2668,2455,510,757,49,48,41,44,38,36,46,57,42,39,45,35])). % 117.98/118.53 cnf(3573,plain, % 117.98/118.53 (E(f13(f4(f13(f13(a1)))),f13(f13(a1)))), % 117.98/118.53 inference(scs_inference,[],[3476,3442,3354,2830,2668,2455,510,757,49,48,41,44,38,36,46,57,42,39,45,35,6,14,16,9,7,11,13,10,8,18,5,12,17,4,2,15,43])). % 117.98/118.53 cnf(3577,plain, % 117.98/118.53 (P2(f6(f12(a11),f13(a1)))), % 117.98/118.53 inference(scs_inference,[],[3476,3442,3354,2830,2668,2455,510,95,757,49,48,41,44,38,36,46,57,42,39,45,35,6,14,16,9,7,11,13,10,8,18,5,12,17,4,2,15,43,62,56])). % 117.98/118.53 cnf(3579,plain, % 117.98/118.53 (P1(f4(f13(f13(a1))))), % 117.98/118.53 inference(scs_inference,[],[3476,3442,3354,2830,2668,2455,510,95,757,49,48,41,44,38,36,46,57,42,39,45,35,6,14,16,9,7,11,13,10,8,18,5,12,17,4,2,15,43,62,56,40])). % 117.98/118.53 cnf(3583,plain, % 117.98/118.53 (P2(f8(f6(f12(a11),f3(a11)),f6(f12(a11),f3(a11))))), % 117.98/118.53 inference(scs_inference,[],[3476,3442,3354,2830,2668,2455,510,95,757,49,48,41,44,38,36,46,57,42,39,45,35,6,14,16,9,7,11,13,10,8,18,5,12,17,4,2,15,43,62,56,40,67,54])). % 117.98/118.53 cnf(3585,plain, % 117.98/118.53 (P2(f7(f6(f12(a11),f3(a11)),f6(f12(a11),f3(a11))))), % 117.98/118.53 inference(scs_inference,[],[3476,3442,3354,2830,2668,2455,510,95,757,49,48,41,44,38,36,46,57,42,39,45,35,6,14,16,9,7,11,13,10,8,18,5,12,17,4,2,15,43,62,56,40,67,54,55])). % 117.98/118.53 cnf(3588,plain, % 117.98/118.53 (E(f8(f9(f6(a11,a1)),f6(a11,a1)),f9(a10))), % 117.98/118.53 inference(scs_inference,[],[3476,3442,2908,3354,2830,3518,612,2457,2668,2455,510,95,757,49,48,41,44,38,36,46,57,42,39,45,35,6,14,16,9,7,11,13,10,8,18,5,12,17,4,2,15,43,62,56,40,67,54,55,24,3])). % 117.98/118.53 cnf(3592,plain, % 117.98/118.53 (E(f6(f12(a11),f13(a1)),f6(a11,f13(a1)))), % 117.98/118.53 inference(scs_inference,[],[33,3476,3442,2908,2632,2440,3354,2830,3518,3326,612,2457,2668,2455,510,95,757,32,28,49,48,41,44,38,36,46,57,42,39,45,35,6,14,16,9,7,11,13,10,8,18,5,12,17,4,2,15,43,62,56,40,67,54,55,24,3,22,23,87])). % 117.98/118.53 cnf(3611,plain, % 117.98/118.53 (P1(f13(f13(f13(a1))))), % 117.98/118.53 inference(scs_inference,[],[3543,3577,3579,49,48,50,41,36])). % 117.98/118.53 cnf(3615,plain, % 117.98/118.53 (E(f7(a10,f6(f12(a11),f13(a1))),a10)), % 117.98/118.53 inference(scs_inference,[],[3543,3577,3579,49,48,50,41,36,44,42])). % 117.98/118.53 cnf(3617,plain, % 117.98/118.53 (P4(f6(f12(a11),f13(a1)),f6(f12(a11),f13(a1)))), % 117.98/118.53 inference(scs_inference,[],[3543,3577,3579,49,48,50,41,36,44,42,46])). % 117.98/118.53 cnf(3621,plain, % 117.98/118.53 (P4(a10,f7(f6(f12(a11),f13(a1)),f6(f12(a11),f13(a1))))), % 117.98/118.53 inference(scs_inference,[],[3543,3577,3579,49,48,50,41,36,44,42,46,39,57])). % 117.98/118.53 cnf(3623,plain, % 117.98/118.53 (P2(f9(f6(f12(a11),f13(a1))))), % 117.98/118.53 inference(scs_inference,[],[3543,3577,3579,49,48,50,41,36,44,42,46,39,57,38])). % 117.98/118.53 cnf(3643,plain, % 117.98/118.53 (~E(a1,f13(f13(a1)))), % 117.98/118.53 inference(scs_inference,[],[3543,3577,3555,3588,3579,49,48,50,41,36,44,42,46,39,57,38,45,35,6,16,11,7,14,9,18,10,13,5,8,12,17,4,2])). % 117.98/118.53 cnf(3645,plain, % 117.98/118.53 (E(f13(f4(f13(f13(f13(a1))))),f13(f13(f13(a1))))), % 117.98/118.53 inference(scs_inference,[],[3543,3577,3555,3588,3579,49,48,50,41,36,44,42,46,39,57,38,45,35,6,16,11,7,14,9,18,10,13,5,8,12,17,4,2,15,43])). % 117.98/118.53 cnf(3649,plain, % 117.98/118.53 (P2(f6(f12(a11),f13(f13(a1))))), % 117.98/118.53 inference(scs_inference,[],[3543,3577,3555,3588,3579,95,49,48,50,41,36,44,42,46,39,57,38,45,35,6,16,11,7,14,9,18,10,13,5,8,12,17,4,2,15,43,62,56])). % 117.98/118.53 cnf(3651,plain, % 117.98/118.53 (P1(f4(f13(f13(f13(a1)))))), % 117.98/118.53 inference(scs_inference,[],[3543,3577,3555,3588,3579,95,49,48,50,41,36,44,42,46,39,57,38,45,35,6,16,11,7,14,9,18,10,13,5,8,12,17,4,2,15,43,62,56,40])). % 117.98/118.53 cnf(3653,plain, % 117.98/118.53 (E(f9(f7(f6(f12(a11),f13(a1)),f6(f12(a11),f13(a1)))),f7(f9(f6(f12(a11),f13(a1))),f6(f12(a11),f13(a1))))), % 117.98/118.53 inference(scs_inference,[],[3543,3577,3555,3588,3579,95,49,48,50,41,36,44,42,46,39,57,38,45,35,6,16,11,7,14,9,18,10,13,5,8,12,17,4,2,15,43,62,56,40,67])). % 117.98/118.53 cnf(3655,plain, % 117.98/118.53 (P2(f8(f6(f12(a11),f13(a1)),f6(f12(a11),f13(a1))))), % 117.98/118.53 inference(scs_inference,[],[3543,3577,3555,3588,3579,95,49,48,50,41,36,44,42,46,39,57,38,45,35,6,16,11,7,14,9,18,10,13,5,8,12,17,4,2,15,43,62,56,40,67,54])). % 117.98/118.53 cnf(3657,plain, % 117.98/118.53 (P2(f7(f6(f12(a11),f13(a1)),f6(f12(a11),f13(a1))))), % 117.98/118.53 inference(scs_inference,[],[3543,3577,3555,3588,3579,95,49,48,50,41,36,44,42,46,39,57,38,45,35,6,16,11,7,14,9,18,10,13,5,8,12,17,4,2,15,43,62,56,40,67,54,55])). % 117.98/118.53 cnf(3662,plain, % 117.98/118.53 (~P4(f7(f6(a11,f3(a11)),a10),f2(a11,a11))), % 117.98/118.53 inference(scs_inference,[],[33,3543,3577,3555,3588,3038,3579,2713,3573,3518,91,95,97,49,48,50,41,36,44,42,46,39,57,38,45,35,6,16,11,7,14,9,18,10,13,5,8,12,17,4,2,15,43,62,56,40,67,54,55,24,25,3,22])). % 117.98/118.53 cnf(3669,plain, % 117.98/118.53 (~E(f13(f13(f13(a1))),f13(a1))), % 117.98/118.53 inference(scs_inference,[],[33,3387,3543,3577,3555,3588,3116,3038,3579,2713,3585,2709,3573,3518,91,26,583,31,95,124,97,49,48,50,41,36,44,42,46,39,57,38,45,35,6,16,11,7,14,9,18,10,13,5,8,12,17,4,2,15,43,62,56,40,67,54,55,24,25,3,22,23,71,78,19,51])). % 117.98/118.53 cnf(3692,plain, % 117.98/118.53 (P1(f13(f13(f13(f13(a1)))))), % 117.98/118.53 inference(scs_inference,[],[3623,3611,49,48,41,50,44,39,42,36])). % 117.98/118.53 cnf(3696,plain, % 117.98/118.53 (P4(f9(f6(f12(a11),f13(a1))),f9(f6(f12(a11),f13(a1))))), % 117.98/118.53 inference(scs_inference,[],[3623,3611,49,48,41,50,44,39,42,36,57,46])). % 117.98/118.53 cnf(3702,plain, % 117.98/118.53 (~E(f13(f13(f13(f13(a1)))),a1)), % 117.98/118.53 inference(scs_inference,[],[3623,3611,49,48,41,50,44,39,42,36,57,46,38,45,35])). % 117.98/118.53 cnf(3706,plain, % 117.98/118.53 (E(f9(f6(f12(a11),f13(a1))),f9(f6(a11,f13(a1))))), % 117.98/118.53 inference(scs_inference,[],[3592,3623,3611,49,48,41,50,44,39,42,36,57,46,38,45,35,16,7,14])). % 117.98/118.53 cnf(3707,plain, % 117.98/118.53 (E(f7(x37071,f6(f12(a11),f13(a1))),f7(x37071,f6(a11,f13(a1))))), % 117.98/118.53 inference(scs_inference,[],[3592,3623,3611,49,48,41,50,44,39,42,36,57,46,38,45,35,16,7,14,6])). % 117.98/118.53 cnf(3710,plain, % 117.98/118.53 (E(f8(x37101,f6(f12(a11),f13(a1))),f8(x37101,f6(a11,f13(a1))))), % 117.98/118.53 inference(scs_inference,[],[3592,3623,3611,49,48,41,50,44,39,42,36,57,46,38,45,35,16,7,14,6,11,9,13])). % 117.98/118.53 cnf(3714,plain, % 117.98/118.53 (E(f7(f6(f12(a11),f13(a1)),x37141),f7(f6(a11,f13(a1)),x37141))), % 117.98/118.53 inference(scs_inference,[],[3592,3623,3611,49,48,41,50,44,39,42,36,57,46,38,45,35,16,7,14,6,11,9,13,18,8,10,5])). % 117.98/118.53 cnf(3718,plain, % 117.98/118.53 (~E(f13(a1),f13(f13(f13(a1))))), % 117.98/118.53 inference(scs_inference,[],[3592,3669,3623,3611,49,48,41,50,44,39,42,36,57,46,38,45,35,16,7,14,6,11,9,13,18,8,10,5,12,4,17,2])). % 117.98/118.53 cnf(3720,plain, % 117.98/118.53 (P2(f6(f12(a11),f13(f13(f13(a1)))))), % 117.98/118.53 inference(scs_inference,[],[3592,3669,3623,3611,95,49,48,41,50,44,39,42,36,57,46,38,45,35,16,7,14,6,11,9,13,18,8,10,5,12,4,17,2,15,56])). % 117.98/118.53 cnf(3733,plain, % 117.98/118.53 (~E(f13(f13(f13(f13(a1)))),f13(f13(a1)))), % 117.98/118.53 inference(scs_inference,[],[3617,3592,3669,3623,3611,2717,3383,2410,2873,3518,580,3476,95,49,48,41,50,44,39,42,36,57,46,38,45,35,16,7,14,6,11,9,13,18,8,10,5,12,4,17,2,15,56,40,54,55,24,25,3,22,23,51])). % 117.98/118.53 cnf(3735,plain, % 117.98/118.53 (P4(f8(f6(f12(a11),f13(a1)),f6(f12(a11),f13(a1))),f8(f6(f12(a11),f13(a1)),f6(f12(a11),f13(a1))))), % 117.98/118.53 inference(scs_inference,[],[3617,3592,3669,3623,3611,2717,3383,2410,2873,3518,580,3476,3577,95,49,48,41,50,44,39,42,36,57,46,38,45,35,16,7,14,6,11,9,13,18,8,10,5,12,4,17,2,15,56,40,54,55,24,25,3,22,23,51,78])). % 117.98/118.53 cnf(3759,plain, % 117.98/118.53 (P2(f9(f6(f12(a11),f13(f13(a1)))))), % 117.98/118.53 inference(scs_inference,[],[3649,3651,49,48,39,41,44,57,42,36,46,38])). % 117.98/118.53 cnf(3787,plain, % 117.98/118.53 (~E(a1,f13(f4(f13(f13(a1)))))), % 117.98/118.53 inference(scs_inference,[],[3643,2880,3649,3651,3322,3573,95,49,48,39,41,44,57,42,36,46,38,35,45,7,6,11,16,14,13,8,9,5,18,10,12,17,4,2,15,56,54,55,3])). % 117.98/118.53 cnf(3811,plain, % 117.98/118.53 (P4(f7(f6(f12(a11),f13(a1)),f6(f12(a11),f13(a1))),f7(f6(f12(a11),f13(a1)),f6(f12(a11),f13(a1))))), % 117.98/118.53 inference(scs_inference,[],[3657,583,49,48,57,42,44,39,41,46])). % 117.98/118.53 cnf(3815,plain, % 117.98/118.53 (P2(f9(f7(f6(f12(a11),f13(a1)),f6(f12(a11),f13(a1)))))), % 117.98/118.53 inference(scs_inference,[],[3657,3692,583,49,48,57,42,44,39,41,46,36,38])). % 117.98/118.53 cnf(3836,plain, % 117.98/118.53 (~E(f13(f4(f13(f13(a1)))),a1)), % 117.98/118.53 inference(scs_inference,[],[2882,3657,3692,3787,583,49,48,57,42,44,39,41,46,36,38,45,35,7,11,6,16,14,18,9,5,13,10,8,12,17,4,15,2])). % 117.98/118.53 cnf(3845,plain, % 117.98/118.53 (~P4(f7(a10,f6(f12(a11),f13(a1))),f2(a11,a11))), % 117.98/118.53 inference(scs_inference,[],[33,2882,3615,2616,3657,3692,3787,3315,1375,583,95,49,48,57,42,44,39,41,46,36,38,45,35,7,11,6,16,14,18,9,5,13,10,8,12,17,4,15,2,56,54,55,24,3,22])). % 117.98/118.53 cnf(3847,plain, % 117.98/118.53 (E(f7(x38471,f6(f12(a11),f13(a1))),f7(x38471,f6(a11,f13(a1))))), % 117.98/118.53 inference(rename_variables,[],[3707])). % 117.98/118.53 cnf(3856,plain, % 117.98/118.53 (P2(f7(f6(f12(a11),f13(a1)),f6(a11,f13(a1))))), % 117.98/118.53 inference(scs_inference,[],[33,2882,3615,2616,3657,3621,3707,3847,3692,3787,3315,3579,511,1375,519,194,510,583,95,195,49,48,57,42,44,39,41,46,36,38,45,35,7,11,6,16,14,18,9,5,13,10,8,12,17,4,15,2,56,54,55,24,3,22,23,71,78,79,40,20])). % 117.98/118.53 cnf(3862,plain, % 117.98/118.53 (E(f8(f9(f2(a11,a11)),f2(a11,a11)),a10)), % 117.98/118.53 inference(scs_inference,[],[124,49])). % 117.98/118.53 cnf(3864,plain, % 117.98/118.53 (E(f8(f2(a11,a11),f9(f2(a11,a11))),a10)), % 117.98/118.53 inference(scs_inference,[],[124,49,48])). % 117.98/118.53 cnf(3868,plain, % 117.98/118.53 (E(f9(f9(f2(a11,a11))),f2(a11,a11))), % 117.98/118.53 inference(scs_inference,[],[3856,124,49,48,41,39])). % 117.98/118.53 cnf(3874,plain, % 117.98/118.53 (P1(f13(f4(f13(f13(a1)))))), % 117.98/118.53 inference(scs_inference,[],[3856,3579,124,49,48,41,39,57,44,36])). % 117.98/118.53 cnf(3880,plain, % 117.98/118.53 (P2(f9(f7(f6(f12(a11),f13(a1)),f6(a11,f13(a1)))))), % 117.98/118.53 inference(scs_inference,[],[3856,3579,124,49,48,41,39,57,44,36,42,46,38])). % 117.98/118.53 cnf(3882,plain, % 117.98/118.53 (~E(f13(a1),a1)), % 117.98/118.53 inference(scs_inference,[],[3856,3579,26,124,49,48,41,39,57,44,36,42,46,38,35])). % 117.98/118.53 cnf(3902,plain, % 117.98/118.53 (E(f13(f4(f13(a1))),f13(a1))), % 117.98/118.53 inference(scs_inference,[],[2891,3856,3733,3579,3476,26,124,49,48,41,39,57,44,36,42,46,38,35,45,7,6,11,10,16,5,13,14,18,8,9,12,4,17,2,15,43])). % 117.98/118.53 cnf(3904,plain, % 117.98/118.53 (P2(f6(f12(a11),f4(f13(f13(a1)))))), % 117.98/118.53 inference(scs_inference,[],[2891,3856,3733,3579,3476,26,95,124,49,48,41,39,57,44,36,42,46,38,35,45,7,6,11,10,16,5,13,14,18,8,9,12,4,17,2,15,43,56])). % 117.98/118.53 cnf(3938,plain, % 117.98/118.53 (E(f9(f9(a10)),a10)), % 117.98/118.53 inference(scs_inference,[],[3759,27,1311,49,48,41,39])). % 117.98/118.53 cnf(3957,plain, % 117.98/118.53 (E(f6(f8(f9(f2(a11,a11)),f2(a11,a11)),x39571),f6(a10,x39571))), % 117.98/118.53 inference(scs_inference,[],[3862,3874,3759,3655,27,1311,49,48,41,39,57,42,44,46,36,38,45,35,11,10])). % 117.98/118.53 cnf(3959,plain, % 117.98/118.53 (E(f7(x39591,f8(f9(f2(a11,a11)),f2(a11,a11))),f7(x39591,a10))), % 117.98/118.53 inference(scs_inference,[],[3862,3874,3759,3655,27,1311,49,48,41,39,57,42,44,46,36,38,45,35,11,10,5,6])). % 117.98/118.53 cnf(3961,plain, % 117.98/118.53 (E(f4(f8(f9(f2(a11,a11)),f2(a11,a11))),f4(a10))), % 117.98/118.53 inference(scs_inference,[],[3862,3874,3759,3655,27,1311,49,48,41,39,57,42,44,46,36,38,45,35,11,10,5,6,7,16])). % 117.98/118.53 cnf(3964,plain, % 117.98/118.53 (E(f3(f8(f9(f2(a11,a11)),f2(a11,a11))),f3(a10))), % 117.98/118.53 inference(scs_inference,[],[3862,3874,3759,3655,27,1311,49,48,41,39,57,42,44,46,36,38,45,35,11,10,5,6,7,16,8,14,9])). % 117.98/118.53 cnf(3965,plain, % 117.98/118.53 (E(f8(x39651,f8(f9(f2(a11,a11)),f2(a11,a11))),f8(x39651,a10))), % 117.98/118.53 inference(scs_inference,[],[3862,3874,3759,3655,27,1311,49,48,41,39,57,42,44,46,36,38,45,35,11,10,5,6,7,16,8,14,9,13])). % 117.98/118.53 cnf(3966,plain, % 117.98/118.53 (E(f5(x39661,f8(f9(f2(a11,a11)),f2(a11,a11))),f5(x39661,a10))), % 117.98/118.53 inference(scs_inference,[],[3862,3874,3759,3655,27,1311,49,48,41,39,57,42,44,46,36,38,45,35,11,10,5,6,7,16,8,14,9,13,18])). % 117.98/118.53 cnf(3968,plain, % 117.98/118.53 (E(f12(f8(f9(f2(a11,a11)),f2(a11,a11))),f12(a10))), % 117.98/118.53 inference(scs_inference,[],[3862,3874,3759,3655,27,1311,49,48,41,39,57,42,44,46,36,38,45,35,11,10,5,6,7,16,8,14,9,13,18,17,4])). % 117.98/118.53 cnf(3970,plain, % 117.98/118.53 (~E(a1,f13(a1))), % 117.98/118.53 inference(scs_inference,[],[3882,3862,3874,3759,3655,27,1311,49,48,41,39,57,42,44,46,36,38,45,35,11,10,5,6,7,16,8,14,9,13,18,17,4,12,2])). % 117.98/118.53 cnf(3974,plain, % 117.98/118.53 (P1(f4(f13(a1)))), % 117.98/118.53 inference(scs_inference,[],[3882,3862,3874,3759,3655,3476,95,27,1311,49,48,41,39,57,42,44,46,36,38,45,35,11,10,5,6,7,16,8,14,9,13,18,17,4,12,2,15,56,40])). % 117.98/118.53 cnf(3980,plain, % 117.98/118.53 (~P5(f13(f4(f13(f4(f3(a11))))),f13(f3(f12(a11))))), % 117.98/118.53 inference(scs_inference,[],[3882,3862,3874,3759,3655,3168,2579,3476,95,27,1311,49,48,41,39,57,42,44,46,36,38,45,35,11,10,5,6,7,16,8,14,9,13,18,17,4,12,2,15,56,40,54,55,24])). % 117.98/118.53 cnf(3981,plain, % 117.98/118.53 (E(f8(f9(f2(a11,a11)),f2(a11,a11)),f7(a10,f9(a10)))), % 117.98/118.53 inference(scs_inference,[],[3882,3862,3874,3759,3655,3168,2579,580,3476,95,27,1311,49,48,41,39,57,42,44,46,36,38,45,35,11,10,5,6,7,16,8,14,9,13,18,17,4,12,2,15,56,40,54,55,24,3])). % 117.98/118.53 cnf(3982,plain, % 117.98/118.53 (~P4(f8(f9(f2(a11,a11)),f2(a11,a11)),f2(a11,a11))), % 117.98/118.53 inference(scs_inference,[],[33,3882,3862,3874,3759,3655,3168,2579,580,3476,95,27,1311,49,48,41,39,57,42,44,46,36,38,45,35,11,10,5,6,7,16,8,14,9,13,18,17,4,12,2,15,56,40,54,55,24,3,22])). % 117.98/118.53 cnf(3983,plain, % 117.98/118.53 (~P4(a10,f9(f9(f2(a11,a11))))), % 117.98/118.53 inference(scs_inference,[],[33,3882,3862,3868,3874,3759,3655,3168,2579,580,3476,95,27,1311,49,48,41,39,57,42,44,46,36,38,45,35,11,10,5,6,7,16,8,14,9,13,18,17,4,12,2,15,56,40,54,55,24,3,22,23])). % 117.98/118.53 cnf(3986,plain, % 117.98/118.53 (E(f9(f8(f9(f2(a11,a11)),f2(a11,a11))),a10)), % 117.98/118.53 inference(scs_inference,[],[33,3882,2614,3862,3868,3874,3759,3655,2711,3168,2579,580,3476,2552,2467,95,27,1311,49,48,41,39,57,42,44,46,36,38,45,35,11,10,5,6,7,16,8,14,9,13,18,17,4,12,2,15,56,40,54,55,24,3,22,23,78,127])). % 117.98/118.53 cnf(3987,plain, % 117.98/118.53 (P5(f4(f13(a1)),f13(f4(f13(a1))))), % 117.98/118.53 inference(scs_inference,[],[33,3882,2614,3862,3868,3874,3759,3655,2711,3168,2579,580,3476,2552,2467,95,27,1311,49,48,41,39,57,42,44,46,36,38,45,35,11,10,5,6,7,16,8,14,9,13,18,17,4,12,2,15,56,40,54,55,24,3,22,23,78,127,50])). % 117.98/118.53 cnf(4008,plain, % 117.98/118.53 (P1(f13(f4(f13(a1))))), % 117.98/118.53 inference(scs_inference,[],[3974,3720,3583,1311,654,49,48,41,57,39,42,46,44,36])). % 117.98/118.53 cnf(4012,plain, % 117.98/118.53 (~E(f13(f4(f13(a1))),a1)), % 117.98/118.53 inference(scs_inference,[],[3974,3720,3583,1311,654,49,48,41,57,39,42,46,44,36,38,35])). % 117.98/118.53 cnf(4016,plain, % 117.98/118.53 (E(f7(f9(f9(a10)),x40161),f7(a10,x40161))), % 117.98/118.53 inference(scs_inference,[],[3974,3938,3720,3583,1311,654,49,48,41,57,39,42,46,44,36,38,35,45,5])). % 117.98/118.53 cnf(4017,plain, % 117.98/118.53 (E(f7(x40171,f9(f9(a10))),f7(x40171,a10))), % 117.98/118.53 inference(scs_inference,[],[3974,3938,3720,3583,1311,654,49,48,41,57,39,42,46,44,36,38,35,45,5,6])). % 117.98/118.53 cnf(4018,plain, % 117.98/118.53 (E(f4(f9(f9(a10))),f4(a10))), % 117.98/118.53 inference(scs_inference,[],[3974,3938,3720,3583,1311,654,49,48,41,57,39,42,46,44,36,38,35,45,5,6,16])). % 117.98/118.53 cnf(4019,plain, % 117.98/118.53 (E(f6(f9(f9(a10)),x40191),f6(a10,x40191))), % 117.98/118.53 inference(scs_inference,[],[3974,3938,3720,3583,1311,654,49,48,41,57,39,42,46,44,36,38,35,45,5,6,16,10])). % 117.98/118.53 cnf(4020,plain, % 117.98/118.53 (E(f6(x40201,f9(f9(a10))),f6(x40201,a10))), % 117.98/118.53 inference(scs_inference,[],[3974,3938,3720,3583,1311,654,49,48,41,57,39,42,46,44,36,38,35,45,5,6,16,10,11])). % 117.98/118.53 cnf(4021,plain, % 117.98/118.53 (E(f2(f9(f9(a10)),x40211),f2(a10,x40211))), % 117.98/118.53 inference(scs_inference,[],[3974,3938,3720,3583,1311,654,49,48,41,57,39,42,46,44,36,38,35,45,5,6,16,10,11,7])). % 117.98/118.53 cnf(4023,plain, % 117.98/118.53 (E(f8(x40231,f9(f9(a10))),f8(x40231,a10))), % 117.98/118.53 inference(scs_inference,[],[3974,3938,3902,3720,3583,1311,654,49,48,41,57,39,42,46,44,36,38,35,45,5,6,16,10,11,7,14,13])). % 117.98/118.53 cnf(4024,plain, % 117.98/118.53 (E(f5(x40241,f9(f9(a10))),f5(x40241,a10))), % 117.98/118.53 inference(scs_inference,[],[3974,3938,3902,3720,3583,1311,654,49,48,41,57,39,42,46,44,36,38,35,45,5,6,16,10,11,7,14,13,18])). % 117.98/118.53 cnf(4025,plain, % 117.98/118.53 (E(f2(x40251,f9(f9(a10))),f2(x40251,a10))), % 117.98/118.53 inference(scs_inference,[],[3974,3938,3902,3720,3583,1311,654,49,48,41,57,39,42,46,44,36,38,35,45,5,6,16,10,11,7,14,13,18,8])). % 117.98/118.53 cnf(4027,plain, % 117.98/118.53 (E(f8(f9(f9(a10)),x40271),f8(a10,x40271))), % 117.98/118.53 inference(scs_inference,[],[3974,3938,3902,3720,3583,1311,654,49,48,41,57,39,42,46,44,36,38,35,45,5,6,16,10,11,7,14,13,18,8,9,12])). % 117.98/118.53 cnf(4028,plain, % 117.98/118.53 (E(f5(f9(f9(a10)),x40281),f5(a10,x40281))), % 117.98/118.53 inference(scs_inference,[],[3974,3938,3902,3720,3583,1311,654,49,48,41,57,39,42,46,44,36,38,35,45,5,6,16,10,11,7,14,13,18,8,9,12,17])). % 117.98/118.53 cnf(4029,plain, % 117.98/118.53 (E(f12(f9(f9(a10))),f12(a10))), % 117.98/118.53 inference(scs_inference,[],[3974,3938,3902,3720,3583,1311,654,49,48,41,57,39,42,46,44,36,38,35,45,5,6,16,10,11,7,14,13,18,8,9,12,17,4])). % 117.98/118.53 cnf(4032,plain, % 117.98/118.53 (E(f13(f4(f13(f4(f13(a1))))),f13(f4(f13(a1))))), % 117.98/118.53 inference(scs_inference,[],[3974,3938,3902,3720,2672,3583,1311,654,49,48,41,57,39,42,46,44,36,38,35,45,5,6,16,10,11,7,14,13,18,8,9,12,17,4,2,15,43])). % 117.98/118.53 cnf(4034,plain, % 117.98/118.53 (P2(f6(f12(a11),f4(f13(a1))))), % 117.98/118.53 inference(scs_inference,[],[3974,3938,3902,3720,2672,3583,95,1311,654,49,48,41,57,39,42,46,44,36,38,35,45,5,6,16,10,11,7,14,13,18,8,9,12,17,4,2,15,43,56])). % 117.98/118.53 cnf(4036,plain, % 117.98/118.53 (P1(f4(f13(f4(f13(a1)))))), % 117.98/118.53 inference(scs_inference,[],[3974,3938,3902,3720,2672,3583,95,1311,654,49,48,41,57,39,42,46,44,36,38,35,45,5,6,16,10,11,7,14,13,18,8,9,12,17,4,2,15,43,56,40])). % 117.98/118.53 cnf(4042,plain, % 117.98/118.53 (~E(a1,f13(f4(f13(a1))))), % 117.98/118.53 inference(scs_inference,[],[3970,3974,3938,3902,3720,2672,3583,95,1311,654,49,48,41,57,39,42,46,44,36,38,35,45,5,6,16,10,11,7,14,13,18,8,9,12,17,4,2,15,43,56,40,54,55,3])). % 117.98/118.53 cnf(4045,plain, % 117.98/118.53 (P5(f13(f4(f13(a1))),f13(f13(f4(f13(a1)))))), % 117.98/118.53 inference(scs_inference,[],[33,3970,3974,3938,3982,3902,3720,2672,3583,3868,95,1311,654,49,48,41,57,39,42,46,44,36,38,35,45,5,6,16,10,11,7,14,13,18,8,9,12,17,4,2,15,43,56,40,54,55,3,22,23,50])). % 117.98/118.53 cnf(4048,plain, % 117.98/118.53 (~E(f13(f13(f13(f13(f13(a1))))),f13(a1))), % 117.98/118.53 inference(scs_inference,[],[33,3970,3974,3938,3982,3902,3720,2672,3702,3583,3868,3692,26,95,1311,654,49,48,41,57,39,42,46,44,36,38,35,45,5,6,16,10,11,7,14,13,18,8,9,12,17,4,2,15,43,56,40,54,55,3,22,23,50,24,51])). % 117.98/118.53 cnf(4050,plain, % 117.98/118.53 (E(f6(f12(a11),f4(f13(a1))),f6(a11,f4(f13(a1))))), % 117.98/118.53 inference(scs_inference,[],[33,3970,3974,3938,3982,3902,3720,2672,3702,3583,3868,3692,26,95,1311,654,32,28,49,48,41,57,39,42,46,44,36,38,35,45,5,6,16,10,11,7,14,13,18,8,9,12,17,4,2,15,43,56,40,54,55,3,22,23,50,24,51,87])). % 117.98/118.53 cnf(4075,plain, % 117.98/118.53 (P1(f13(f13(f4(f13(a1)))))), % 117.98/118.53 inference(scs_inference,[],[4008,4034,49,48,41,57,39,42,44,46,36])). % 117.98/118.53 cnf(4077,plain, % 117.98/118.53 (P2(f9(f6(f12(a11),f4(f13(a1)))))), % 117.98/118.53 inference(scs_inference,[],[4008,4034,49,48,41,57,39,42,44,46,36,38])). % 117.98/118.53 cnf(4081,plain, % 117.98/118.53 (~E(f13(f13(f4(f13(a1)))),a1)), % 117.98/118.53 inference(scs_inference,[],[4008,4034,49,48,41,57,39,42,44,46,36,38,45,35])). % 117.98/118.53 cnf(4099,plain, % 117.98/118.53 (P2(f6(f12(a11),f13(f4(f13(a1)))))), % 117.98/118.53 inference(scs_inference,[],[4016,4008,4034,2984,95,49,48,41,57,39,42,44,46,36,38,45,35,16,10,7,6,5,11,9,8,13,14,18,4,12,17,15,2,56])). % 117.98/118.53 cnf(4108,plain, % 117.98/118.53 (E(f7(f9(f9(a10)),f9(f9(a10))),f7(a10,a10))), % 117.98/118.53 inference(scs_inference,[],[4016,4017,4008,4034,2984,3980,2616,95,49,48,41,57,39,42,44,46,36,38,45,35,16,10,7,6,5,11,9,8,13,14,18,4,12,17,15,2,56,40,54,55,24,3])). % 117.98/118.53 cnf(4109,plain, % 117.98/118.53 (E(f7(f9(f9(a10)),x41091),f7(a10,x41091))), % 117.98/118.53 inference(rename_variables,[],[4016])). % 117.98/118.53 cnf(4115,plain, % 117.98/118.53 (~E(f13(f13(f4(f13(a1)))),f13(a1))), % 117.98/118.53 inference(scs_inference,[],[3845,4016,4109,4017,4008,4034,4012,3710,3735,2984,3980,2616,26,95,49,48,41,57,39,42,44,46,36,38,45,35,16,10,7,6,5,11,9,8,13,14,18,4,12,17,15,2,56,40,54,55,24,3,22,23,51])). % 117.98/118.53 cnf(4119,plain, % 117.98/118.53 (P2(f6(a11,f4(f13(a1))))), % 117.98/118.53 inference(scs_inference,[],[3845,4016,4109,4017,4008,4034,4012,3710,4050,3735,2984,3980,2616,3974,26,95,49,48,41,57,39,42,44,46,36,38,45,35,16,10,7,6,5,11,9,8,13,14,18,4,12,17,15,2,56,40,54,55,24,3,22,23,51,43,20])). % 117.98/118.53 cnf(4170,plain, % 117.98/118.53 (~P4(f8(f2(a11,a11),f9(f2(a11,a11))),f2(a11,a11))), % 117.98/118.53 inference(scs_inference,[],[33,4019,3864,3718,4119,4115,4036,4045,3645,3902,95,49,48,41,39,44,57,42,36,46,38,35,45,6,11,7,5,16,10,9,8,18,13,14,4,12,17,15,2,56,54,55,24,3,22])). % 117.98/118.53 cnf(4171,plain, % 117.98/118.53 (~P4(f7(f6(a11,f3(a11)),a10),f9(f9(f2(a11,a11))))), % 117.98/118.53 inference(scs_inference,[],[33,3662,4019,3864,3718,4119,4115,4036,4045,3645,3868,3902,95,49,48,41,39,44,57,42,36,46,38,35,45,6,11,7,5,16,10,9,8,18,13,14,4,12,17,15,2,56,54,55,24,3,22,23])). % 117.98/118.53 cnf(4230,plain, % 117.98/118.53 (~E(f13(f13(f13(f4(f13(a1))))),f13(a1))), % 117.98/118.53 inference(scs_inference,[],[4020,4027,3957,3714,4077,4075,3811,3115,4081,2478,3585,26,95,654,757,49,41,48,39,44,57,46,42,36,38,45,35,6,7,11,16,9,5,10,18,8,13,14,4,12,17,15,2,56,54,55,3,22,23,51])). % 117.98/118.53 cnf(4273,plain, % 117.98/118.53 (~E(f13(f4(f3(a11))),f13(f13(f4(f3(a11)))))), % 117.98/118.53 inference(scs_inference,[],[4021,3904,2985,2472,757,451,49,39,48,41,44,46,42,38,45,6,11,7,9,16,8,10,18,13,14,5,4,15,17,12,2])). % 117.98/118.53 cnf(4274,plain, % 117.98/118.53 (P2(f6(f12(a11),f4(f3(a11))))), % 117.98/118.53 inference(scs_inference,[],[4021,3904,2985,2465,2472,95,757,451,49,39,48,41,44,46,42,38,45,6,11,7,9,16,8,10,18,13,14,5,4,15,17,12,2,56])). % 117.98/118.53 cnf(4276,plain, % 117.98/118.53 (P2(f8(f7(f6(a11,a1),f6(a11,a1)),f7(f6(a11,a1),f6(a11,a1))))), % 117.98/118.53 inference(scs_inference,[],[4021,3904,2985,2465,2472,95,757,451,49,39,48,41,44,46,42,38,45,6,11,7,9,16,8,10,18,13,14,5,4,15,17,12,2,56,54])). % 117.98/118.53 cnf(4278,plain, % 117.98/118.53 (P2(f7(f7(f6(a11,a1),f6(a11,a1)),f7(f6(a11,a1),f6(a11,a1))))), % 117.98/118.53 inference(scs_inference,[],[4021,3904,2985,2465,2472,95,757,451,49,39,48,41,44,46,42,38,45,6,11,7,9,16,8,10,18,13,14,5,4,15,17,12,2,56,54,55])). % 117.98/118.53 cnf(4283,plain, % 117.98/118.53 (~E(f13(f13(f4(f3(a11)))),f13(f3(f12(a11))))), % 117.98/118.53 inference(scs_inference,[],[33,4170,4021,4042,3166,3986,3904,2985,4032,3868,2450,2465,2644,2472,95,757,451,49,39,48,41,44,46,42,38,45,6,11,7,9,16,8,10,18,13,14,5,4,15,17,12,2,56,54,55,3,22,23,51])). % 117.98/118.53 cnf(4313,plain, % 117.98/118.53 (P2(f9(f6(f12(a11),f4(f3(a11)))))), % 117.98/118.53 inference(scs_inference,[],[4274,4276,49,39,48,41,42,46,44,57,38])). % 117.98/118.53 cnf(4337,plain, % 117.98/118.53 (E(f5(f9(f9(a10)),f9(f9(a10))),f5(a10,a10))), % 117.98/118.53 inference(scs_inference,[],[4023,4024,4028,4274,4276,4283,49,39,48,41,42,46,44,57,38,45,7,6,11,10,9,14,16,13,18,8,5,4,15,12,17,2,54,55,3])). % 117.98/118.53 cnf(4387,plain, % 117.98/118.53 (P2(f7(f9(f6(f12(a11),f13(a1))),f6(f12(a11),f13(a1))))), % 117.98/118.53 inference(scs_inference,[],[4025,4313,3815,3253,3653,4278,451,39,44,46,41,42,38,45,6,7,11,14,18,13,16,10,9,8,5,4,12,15,2,17,20])). % 117.98/118.53 cnf(4392,plain, % 117.98/118.53 (~E(f3(a11),f13(f3(a11)))), % 117.98/118.53 inference(scs_inference,[],[4025,3303,4313,3815,3253,3653,4278,2457,451,39,44,46,41,42,38,45,6,7,11,14,18,13,16,10,9,8,5,4,12,15,2,17,20,54,55,3])). % 117.98/118.53 cnf(4433,plain, % 117.98/118.53 (E(f8(f9(f2(a11,a11)),f2(a11,a11)),f9(a10))), % 117.98/118.53 inference(scs_inference,[],[4392,2894,3981,4387,4276,612,44,46,42,41,38,45,6,7,18,14,11,13,16,10,9,5,8,4,15,12,2,17,54,55,3])). % 117.98/118.53 cnf(4440,plain, % 117.98/118.53 (~E(a11,f12(a11))), % 117.98/118.53 inference(scs_inference,[],[4392,2894,3981,3959,4387,3696,3706,4171,1380,4276,612,1378,2469,1377,32,28,44,46,42,41,38,45,6,7,18,14,11,13,16,10,9,5,8,4,15,12,2,17,54,55,3,22,23,78,24,52])). % 117.98/118.53 cnf(4475,plain, % 117.98/118.53 (P2(f8(f9(f2(a11,a11)),f9(f2(a11,a11))))), % 117.98/118.53 inference(scs_inference,[],[4440,4433,4099,194,46,42,44,38,41,45,6,7,18,13,11,14,16,10,9,5,8,4,15,12,2,17,54])). % 117.98/118.53 cnf(4477,plain, % 117.98/118.53 (P2(f7(f9(f2(a11,a11)),f9(f2(a11,a11))))), % 117.98/118.53 inference(scs_inference,[],[4440,4433,4099,194,46,42,44,38,41,45,6,7,18,13,11,14,16,10,9,5,8,4,15,12,2,17,54,55])). % 117.98/118.53 cnf(4482,plain, % 117.98/118.53 (~E(f7(f7(f9(a10),a10),f7(f9(a10),a10)),f9(f9(f2(a11,a11))))), % 117.98/118.53 inference(scs_inference,[],[33,4440,4433,3983,3987,3189,3332,4099,755,3902,194,46,42,44,38,41,45,6,7,18,13,11,14,16,10,9,5,8,4,15,12,2,17,54,55,25,3,22,23])). % 117.98/118.53 cnf(4499,plain, % 117.98/118.53 (P2(f9(f8(f9(f2(a11,a11)),f9(f2(a11,a11)))))), % 117.98/118.53 inference(scs_inference,[],[4475,4477,46,44,42,57,38])). % 117.98/118.53 cnf(4529,plain, % 117.98/118.53 (~E(f13(f13(f4(f13(f13(a1))))),f13(a1))), % 117.98/118.53 inference(scs_inference,[],[4018,3965,3370,4475,4477,2703,4482,3204,3836,688,3874,2457,26,46,44,42,57,38,41,45,6,7,18,13,10,14,11,8,9,16,4,5,15,2,12,17,54,55,3,22,23,51])). % 117.98/118.53 cnf(4619,plain, % 117.98/118.53 (P2(f7(f9(f6(f12(a11),f13(a1))),f6(a11,f13(a1))))), % 117.98/118.53 inference(scs_inference,[],[4029,4499,4048,3707,4387,4278,1932,46,42,44,38,45,41,6,13,7,10,18,9,11,4,16,14,8,15,5,2,12,17,20])). % 117.98/118.53 cnf(4621,plain, % 117.98/118.53 (P2(f8(f6(f12(a11),a1),f6(f12(a11),a1)))), % 117.98/118.53 inference(scs_inference,[],[4029,4499,4048,3707,4387,4278,1932,46,42,44,38,45,41,6,13,7,10,18,9,11,4,16,14,8,15,5,2,12,17,20,54])). % 117.98/118.53 cnf(4623,plain, % 117.98/118.53 (P2(f7(f6(f12(a11),a1),f6(f12(a11),a1)))), % 117.98/118.53 inference(scs_inference,[],[4029,4499,4048,3707,4387,4278,1932,46,42,44,38,45,41,6,13,7,10,18,9,11,4,16,14,8,15,5,2,12,17,20,54,55])). % 117.98/118.53 cnf(4641,plain, % 117.98/118.53 (P2(f9(f8(f6(f12(a11),a1),f6(f12(a11),a1))))), % 117.98/118.53 inference(scs_inference,[],[4621,4623,46,42,44,38])). % 117.98/118.53 cnf(4707,plain, % 117.98/118.53 (P2(f8(f6(f12(a11),f13(a1)),f6(a11,f13(a1))))), % 117.98/118.53 inference(scs_inference,[],[4108,4619,4230,3710,4623,3655,46,42,44,38,41,45,6,18,10,13,7,11,8,5,4,16,15,14,9,2,12,17,20])). % 117.98/118.53 cnf(4729,plain, % 117.98/118.53 (P2(f9(f8(f6(f12(a11),f13(a1)),f6(a11,f13(a1)))))), % 117.98/118.53 inference(scs_inference,[],[4707,46,42,44,38])). % 117.98/118.53 cnf(4796,plain, % 117.98/118.53 (P2(f8(f2(f12(a11),f12(a11)),f2(f12(a11),f12(a11))))), % 117.98/118.53 inference(scs_inference,[],[3966,4641,4529,2580,2469,46,42,44,38,45,41,6,18,13,7,10,11,14,5,4,8,9,16,15,2,12,17,54])). % 117.98/118.53 cnf(4798,plain, % 117.98/118.53 (P2(f7(f2(f12(a11),f12(a11)),f2(f12(a11),f12(a11))))), % 117.98/118.53 inference(scs_inference,[],[3966,4641,4529,2580,2469,46,42,44,38,45,41,6,18,13,7,10,11,14,5,4,8,9,16,15,2,12,17,54,55])). % 117.98/118.53 cnf(4821,plain, % 117.98/118.53 (P2(f9(f8(f2(f12(a11),f12(a11)),f2(f12(a11),f12(a11)))))), % 117.98/118.53 inference(scs_inference,[],[4796,4798,57,46,42,44,38])). % 117.98/118.53 cnf(4887,plain, % 117.98/118.53 (P2(f6(f12(a11),f13(f3(f12(a11)))))), % 117.98/118.53 inference(scs_inference,[],[4337,4821,2875,4798,875,95,46,42,38,41,44,45,6,18,7,13,10,11,14,4,15,8,5,9,16,12,2,17,56])). % 117.98/118.53 cnf(4893,plain, % 117.98/118.53 (~E(f3(a11),f13(f13(f4(f3(a11)))))), % 117.98/118.53 inference(scs_inference,[],[4337,4821,4273,2875,4798,2457,875,95,46,42,38,41,44,45,6,18,7,13,10,11,14,4,15,8,5,9,16,12,2,17,56,54,55,3])). % 117.98/118.53 cnf(4936,plain, % 117.98/118.53 (P2(f8(f8(f9(f9(a10)),f9(a10)),f8(f9(f9(a10)),f9(a10))))), % 117.98/118.53 inference(scs_inference,[],[3181,4887,4893,2755,1377,46,42,38,41,44,45,6,18,13,7,10,11,14,4,15,9,8,5,16,12,2,17,54])). % 117.98/118.53 cnf(4978,plain, % 117.98/118.53 (P2(f8(f7(f9(a10),a10),f7(f9(a10),a10)))), % 117.98/118.53 inference(scs_inference,[],[3316,4936,2953,3585,510,42,46,41,38,44,45,6,18,7,13,10,11,4,15,9,14,16,5,8,12,2,17,54])). % 117.98/118.53 cnf(4980,plain, % 117.98/118.53 (P2(f7(f7(f9(a10),a10),f7(f9(a10),a10)))), % 117.98/118.53 inference(scs_inference,[],[3316,4936,2953,3585,510,42,46,41,38,44,45,6,18,7,13,10,11,4,15,9,14,16,5,8,12,2,17,54,55])). % 117.98/118.53 cnf(4982,plain, % 117.98/118.53 (~E(f8(f2(f12(a11),f12(a11)),f7(f6(a11,f3(a11)),f6(a11,f3(a11)))),f8(f9(f9(a10)),f9(a10)))), % 117.98/118.53 inference(scs_inference,[],[3316,4936,2953,1376,3585,91,510,42,46,41,38,44,45,6,18,7,13,10,11,4,15,9,14,16,5,8,12,2,17,54,55,3])). % 117.98/118.53 cnf(5007,plain, % 117.98/118.53 (P2(f9(f8(f7(f9(a10),a10),f7(f9(a10),a10))))), % 117.98/118.53 inference(scs_inference,[],[4978,2472,42,46,41,44,38])). % 117.98/118.53 cnf(5025,plain, % 117.98/118.53 (~E(f8(f9(f9(a10)),f9(a10)),f8(f2(f12(a11),f12(a11)),f7(f6(a11,f3(a11)),f6(a11,f3(a11)))))), % 117.98/118.53 inference(scs_inference,[],[3961,4978,4982,2472,42,46,41,44,38,45,6,18,7,13,10,4,11,9,15,14,16,5,12,8,2])). % 117.98/118.53 cnf(5077,plain, % 117.98/118.53 (~E(f8(a10,f9(a10)),f8(f2(f12(a11),f12(a11)),f7(f6(a11,f3(a11)),f6(a11,f3(a11)))))), % 117.98/118.53 inference(scs_inference,[],[3964,5007,5025,3020,4027,4980,2469,46,42,41,44,38,45,6,18,13,7,11,4,10,9,14,15,16,5,12,2,8,17,54,55,3])). % 117.98/118.53 cnf(5112,plain, % 117.98/118.53 (~E(f8(f2(f12(a11),f12(a11)),f7(f6(a11,f3(a11)),f6(a11,f3(a11)))),f8(a10,f9(a10)))), % 117.98/118.53 inference(scs_inference,[],[3968,3880,5077,583,42,38,44,41,45,18,6,7,13,4,11,9,14,15,5,10,16,12,2])). % 117.98/118.53 cnf(5228,plain, % 117.98/118.53 (E(f8(a10,f2(a11,a11)),f2(a11,a11))), % 117.98/118.53 inference(scs_inference,[],[4729,124,42,41,38,45])). % 117.98/118.53 cnf(5676,plain, % 117.98/118.53 (E(f7(f8(f9(a10),a10),x56761),f7(f8(a10,f9(a10)),x56761))), % 117.98/118.53 inference(rename_variables,[],[2433])). % 117.98/118.53 cnf(5680,plain, % 117.98/118.53 (E(f7(f8(f9(a10),a10),x56801),f7(f8(a10,f9(a10)),x56801))), % 117.98/118.53 inference(rename_variables,[],[2433])). % 117.98/118.53 cnf(5682,plain, % 117.98/118.53 (E(f7(f8(f9(a10),a10),x56821),f7(f8(a10,f9(a10)),x56821))), % 117.98/118.53 inference(rename_variables,[],[2433])). % 117.98/118.53 cnf(5684,plain, % 117.98/118.53 (E(f7(f8(f9(a10),a10),x56841),f7(f8(a10,f9(a10)),x56841))), % 117.98/118.53 inference(rename_variables,[],[2433])). % 117.98/118.53 cnf(5697,plain, % 117.98/118.53 ($false), % 117.98/118.53 inference(scs_inference,[],[33,29,30,1826,791,26,2469,5228,3592,3577,2755,125,2457,2420,3974,3902,2410,2873,3505,2433,5676,5680,5682,5684,2434,5112,2477,2,15,1834,1449,1140,713,719,725,23,22,3,24,25,20,53,51,71]), % 117.98/118.53 ['proof']). % 117.98/118.53 % SZS output end Proof % 117.98/118.53 % Total time :117.290000s %------------------------------------------------------------------------------