%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM491+1 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n023.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 12:24:32 EDT 2024 % Result : Theorem 117.15s 117.20s % Output : CNFRefutation 117.25s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM491+1 : TPTP v8.2.0. Released v4.0.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n023.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Sun Jun 23 00:14:39 EDT 2024 % 0.12/0.33 % CPUTime : % 0.50/0.58 start to proof:theBenchmark % 117.15/117.17 %------------------------------------------- % 117.15/117.17 % File :CSE---1.7 % 117.15/117.17 % Problem :theBenchmark % 117.15/117.17 % Transform :cnf % 117.15/117.17 % Format :tptp:raw % 117.15/117.17 % Command :java -jar mcs_scs.jar %d %s % 117.15/117.17 % 117.15/117.17 % Result :Theorem 116.530000s % 117.15/117.17 % Output :CNFRefutation 116.530000s % 117.15/117.17 %------------------------------------------- % 117.15/117.18 %------------------------------------------------------------------------------ % 117.15/117.18 % File : NUM491+1 : TPTP v8.2.0. Released v4.0.0. % 117.15/117.18 % Domain : Number Theory % 117.15/117.18 % Problem : Square root of a prime is irrational 14_01_03_04, 00 expansion % 117.15/117.18 % Version : Especial. % 117.15/117.18 % English : % 117.15/117.18 % 117.15/117.18 % Refs : [LPV06] Lyaletski et al. (2006), SAD as a Mathematical Assista % 117.15/117.18 % : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 117.15/117.18 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 117.15/117.18 % Source : [Pas08] % 117.15/117.18 % Names : primes_14_01_03_04.00 [Pas08] % 117.15/117.18 % 117.15/117.18 % Status : Theorem % 117.15/117.18 % Rating : 0.17 v8.2.0, 0.19 v8.1.0, 0.11 v7.5.0, 0.06 v7.4.0, 0.13 v7.3.0, 0.10 v7.1.0, 0.09 v7.0.0, 0.13 v6.4.0, 0.19 v6.3.0, 0.08 v6.2.0, 0.16 v6.1.0, 0.17 v6.0.0, 0.09 v5.5.0, 0.26 v5.4.0, 0.32 v5.3.0, 0.37 v5.2.0, 0.25 v5.1.0, 0.38 v5.0.0, 0.42 v4.1.0, 0.52 v4.0.1, 0.70 v4.0.0 % 117.15/117.18 % Syntax : Number of formulae : 48 ( 7 unt; 5 def) % 117.15/117.18 % Number of atoms : 204 ( 61 equ) % 117.15/117.18 % Maximal formula atoms : 10 ( 4 avg) % 117.15/117.18 % Number of connectives : 177 ( 21 ~; 8 |; 81 &) % 117.15/117.18 % ( 5 <=>; 62 =>; 0 <=; 0 <~>) % 117.15/117.18 % Maximal formula depth : 11 ( 5 avg) % 117.15/117.18 % Maximal term depth : 3 ( 1 avg) % 117.15/117.18 % Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty) % 117.15/117.18 % Number of functors : 10 ( 10 usr; 6 con; 0-2 aty) % 117.15/117.18 % Number of variables : 85 ( 82 !; 3 ?) % 117.15/117.18 % SPC : FOF_THM_RFO_SEQ % 117.15/117.18 % 117.15/117.18 % Comments : Problem generated by the SAD system [VLP07] % 117.15/117.18 %------------------------------------------------------------------------------ % 117.15/117.18 fof(mNatSort,axiom, % 117.15/117.18 ! [W0] : % 117.15/117.18 ( aNaturalNumber0(W0) % 117.15/117.18 => $true ) ). % 117.15/117.18 % 117.15/117.18 fof(mSortsC,axiom, % 117.15/117.18 aNaturalNumber0(sz00) ). % 117.15/117.18 % 117.15/117.18 fof(mSortsC_01,axiom, % 117.15/117.18 ( aNaturalNumber0(sz10) % 117.15/117.18 & sz10 != sz00 ) ). % 117.15/117.18 % 117.15/117.18 fof(mSortsB,axiom, % 117.15/117.18 ! [W0,W1] : % 117.15/117.18 ( ( aNaturalNumber0(W0) % 117.15/117.18 & aNaturalNumber0(W1) ) % 117.15/117.18 => aNaturalNumber0(sdtpldt0(W0,W1)) ) ). % 117.15/117.18 % 117.15/117.18 fof(mSortsB_02,axiom, % 117.15/117.18 ! [W0,W1] : % 117.15/117.18 ( ( aNaturalNumber0(W0) % 117.15/117.18 & aNaturalNumber0(W1) ) % 117.15/117.18 => aNaturalNumber0(sdtasdt0(W0,W1)) ) ). % 117.15/117.18 % 117.15/117.18 fof(mAddComm,axiom, % 117.15/117.18 ! [W0,W1] : % 117.15/117.18 ( ( aNaturalNumber0(W0) % 117.15/117.18 & aNaturalNumber0(W1) ) % 117.15/117.18 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 117.15/117.18 % 117.15/117.18 fof(mAddAsso,axiom, % 117.15/117.18 ! [W0,W1,W2] : % 117.15/117.18 ( ( aNaturalNumber0(W0) % 117.15/117.18 & aNaturalNumber0(W1) % 117.15/117.18 & aNaturalNumber0(W2) ) % 117.15/117.18 => sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) ). % 117.15/117.18 % 117.15/117.18 fof(m_AddZero,axiom, % 117.15/117.18 ! [W0] : % 117.15/117.18 ( aNaturalNumber0(W0) % 117.15/117.18 => ( sdtpldt0(W0,sz00) = W0 % 117.15/117.18 & W0 = sdtpldt0(sz00,W0) ) ) ). % 117.15/117.18 % 117.15/117.19 fof(mMulComm,axiom, % 117.15/117.19 ! [W0,W1] : % 117.15/117.19 ( ( aNaturalNumber0(W0) % 117.15/117.19 & aNaturalNumber0(W1) ) % 117.15/117.19 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 117.15/117.19 % 117.15/117.19 fof(mMulAsso,axiom, % 117.15/117.19 ! [W0,W1,W2] : % 117.15/117.19 ( ( aNaturalNumber0(W0) % 117.15/117.19 & aNaturalNumber0(W1) % 117.15/117.19 & aNaturalNumber0(W2) ) % 117.15/117.19 => sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) ). % 117.15/117.19 % 117.15/117.19 fof(m_MulUnit,axiom, % 117.15/117.19 ! [W0] : % 117.15/117.19 ( aNaturalNumber0(W0) % 117.15/117.19 => ( sdtasdt0(W0,sz10) = W0 % 117.15/117.19 & W0 = sdtasdt0(sz10,W0) ) ) ). % 117.15/117.19 % 117.15/117.19 fof(m_MulZero,axiom, % 117.15/117.19 ! [W0] : % 117.15/117.19 ( aNaturalNumber0(W0) % 117.15/117.19 => ( sdtasdt0(W0,sz00) = sz00 % 117.15/117.19 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 117.15/117.19 % 117.15/117.19 fof(mAMDistr,axiom, % 117.15/117.19 ! [W0,W1,W2] : % 117.15/117.19 ( ( aNaturalNumber0(W0) % 117.15/117.19 & aNaturalNumber0(W1) % 117.15/117.19 & aNaturalNumber0(W2) ) % 117.15/117.19 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 117.15/117.19 & sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ). % 117.15/117.19 % 117.15/117.19 fof(mAddCanc,axiom, % 117.15/117.19 ! [W0,W1,W2] : % 117.15/117.19 ( ( aNaturalNumber0(W0) % 117.15/117.19 & aNaturalNumber0(W1) % 117.15/117.19 & aNaturalNumber0(W2) ) % 117.15/117.19 => ( ( sdtpldt0(W0,W1) = sdtpldt0(W0,W2) % 117.15/117.19 | sdtpldt0(W1,W0) = sdtpldt0(W2,W0) ) % 117.15/117.19 => W1 = W2 ) ) ). % 117.15/117.19 % 117.15/117.19 fof(mMulCanc,axiom, % 117.15/117.19 ! [W0] : % 117.15/117.19 ( aNaturalNumber0(W0) % 117.15/117.19 => ( W0 != sz00 % 117.15/117.19 => ! [W1,W2] : % 117.15/117.19 ( ( aNaturalNumber0(W1) % 117.15/117.19 & aNaturalNumber0(W2) ) % 117.15/117.19 => ( ( sdtasdt0(W0,W1) = sdtasdt0(W0,W2) % 117.15/117.19 | sdtasdt0(W1,W0) = sdtasdt0(W2,W0) ) % 117.15/117.19 => W1 = W2 ) ) ) ) ). % 117.15/117.19 % 117.15/117.19 fof(mZeroAdd,axiom, % 117.15/117.19 ! [W0,W1] : % 117.15/117.19 ( ( aNaturalNumber0(W0) % 117.15/117.19 & aNaturalNumber0(W1) ) % 117.15/117.19 => ( sdtpldt0(W0,W1) = sz00 % 117.15/117.19 => ( W0 = sz00 % 117.15/117.19 & W1 = sz00 ) ) ) ). % 117.15/117.19 % 117.15/117.19 fof(mZeroMul,axiom, % 117.15/117.19 ! [W0,W1] : % 117.15/117.19 ( ( aNaturalNumber0(W0) % 117.15/117.19 & aNaturalNumber0(W1) ) % 117.15/117.19 => ( sdtasdt0(W0,W1) = sz00 % 117.15/117.19 => ( W0 = sz00 % 117.15/117.19 | W1 = sz00 ) ) ) ). % 117.15/117.19 % 117.15/117.19 fof(mDefLE,definition, % 117.15/117.19 ! [W0,W1] : % 117.15/117.19 ( ( aNaturalNumber0(W0) % 117.15/117.19 & aNaturalNumber0(W1) ) % 117.15/117.19 => ( sdtlseqdt0(W0,W1) % 117.15/117.19 <=> ? [W2] : % 117.15/117.19 ( aNaturalNumber0(W2) % 117.15/117.19 & sdtpldt0(W0,W2) = W1 ) ) ) ). % 117.15/117.19 % 117.15/117.19 fof(mDefDiff,definition, % 117.15/117.19 ! [W0,W1] : % 117.15/117.19 ( ( aNaturalNumber0(W0) % 117.15/117.19 & aNaturalNumber0(W1) ) % 117.15/117.19 => ( sdtlseqdt0(W0,W1) % 117.15/117.19 => ! [W2] : % 117.15/117.19 ( W2 = sdtmndt0(W1,W0) % 117.15/117.19 <=> ( aNaturalNumber0(W2) % 117.15/117.19 & sdtpldt0(W0,W2) = W1 ) ) ) ) ). % 117.15/117.19 % 117.15/117.19 fof(mLERefl,axiom, % 117.15/117.19 ! [W0] : % 117.15/117.19 ( aNaturalNumber0(W0) % 117.15/117.19 => sdtlseqdt0(W0,W0) ) ). % 117.15/117.19 % 117.15/117.19 fof(mLEAsym,axiom, % 117.15/117.19 ! [W0,W1] : % 117.15/117.19 ( ( aNaturalNumber0(W0) % 117.15/117.19 & aNaturalNumber0(W1) ) % 117.15/117.19 => ( ( sdtlseqdt0(W0,W1) % 117.15/117.19 & sdtlseqdt0(W1,W0) ) % 117.15/117.19 => W0 = W1 ) ) ). % 117.15/117.19 % 117.15/117.19 fof(mLETran,axiom, % 117.15/117.19 ! [W0,W1,W2] : % 117.15/117.19 ( ( aNaturalNumber0(W0) % 117.15/117.19 & aNaturalNumber0(W1) % 117.15/117.19 & aNaturalNumber0(W2) ) % 117.15/117.19 => ( ( sdtlseqdt0(W0,W1) % 117.15/117.19 & sdtlseqdt0(W1,W2) ) % 117.15/117.19 => sdtlseqdt0(W0,W2) ) ) ). % 117.15/117.19 % 117.15/117.19 fof(mLETotal,axiom, % 117.15/117.19 ! [W0,W1] : % 117.15/117.19 ( ( aNaturalNumber0(W0) % 117.15/117.19 & aNaturalNumber0(W1) ) % 117.15/117.19 => ( sdtlseqdt0(W0,W1) % 117.15/117.19 | ( W1 != W0 % 117.15/117.19 & sdtlseqdt0(W1,W0) ) ) ) ). % 117.15/117.19 % 117.15/117.19 fof(mMonAdd,axiom, % 117.15/117.19 ! [W0,W1] : % 117.15/117.19 ( ( aNaturalNumber0(W0) % 117.15/117.19 & aNaturalNumber0(W1) ) % 117.15/117.19 => ( ( W0 != W1 % 117.15/117.19 & sdtlseqdt0(W0,W1) ) % 117.15/117.19 => ! [W2] : % 117.15/117.19 ( aNaturalNumber0(W2) % 117.15/117.19 => ( sdtpldt0(W2,W0) != sdtpldt0(W2,W1) % 117.15/117.19 & sdtlseqdt0(sdtpldt0(W2,W0),sdtpldt0(W2,W1)) % 117.15/117.19 & sdtpldt0(W0,W2) != sdtpldt0(W1,W2) % 117.15/117.19 & sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W2)) ) ) ) ) ). % 117.15/117.19 % 117.15/117.19 fof(mMonMul,axiom, % 117.15/117.19 ! [W0,W1,W2] : % 117.15/117.19 ( ( aNaturalNumber0(W0) % 117.15/117.19 & aNaturalNumber0(W1) % 117.15/117.19 & aNaturalNumber0(W2) ) % 117.15/117.19 => ( ( W0 != sz00 % 117.15/117.19 & W1 != W2 % 117.15/117.19 & sdtlseqdt0(W1,W2) ) % 117.15/117.19 => ( sdtasdt0(W0,W1) != sdtasdt0(W0,W2) % 117.15/117.19 & sdtlseqdt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 117.15/117.19 & sdtasdt0(W1,W0) != sdtasdt0(W2,W0) % 117.15/117.19 & sdtlseqdt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ) ). % 117.15/117.19 % 117.15/117.19 fof(mLENTr,axiom, % 117.15/117.19 ! [W0] : % 117.15/117.19 ( aNaturalNumber0(W0) % 117.15/117.19 => ( W0 = sz00 % 117.15/117.19 | W0 = sz10 % 117.15/117.19 | ( sz10 != W0 % 117.15/117.19 & sdtlseqdt0(sz10,W0) ) ) ) ). % 117.15/117.19 % 117.15/117.19 fof(mMonMul2,axiom, % 117.15/117.19 ! [W0,W1] : % 117.15/117.19 ( ( aNaturalNumber0(W0) % 117.15/117.19 & aNaturalNumber0(W1) ) % 117.15/117.19 => ( W0 != sz00 % 117.15/117.19 => sdtlseqdt0(W1,sdtasdt0(W1,W0)) ) ) ). % 117.15/117.19 % 117.15/117.19 fof(mIH,axiom, % 117.15/117.19 ! [W0,W1] : % 117.15/117.19 ( ( aNaturalNumber0(W0) % 117.15/117.19 & aNaturalNumber0(W1) ) % 117.15/117.19 => ( iLess0(W0,W1) % 117.15/117.19 => $true ) ) ). % 117.15/117.19 % 117.15/117.19 fof(mIH_03,axiom, % 117.15/117.19 ! [W0,W1] : % 117.15/117.19 ( ( aNaturalNumber0(W0) % 117.15/117.19 & aNaturalNumber0(W1) ) % 117.15/117.19 => ( ( W0 != W1 % 117.15/117.19 & sdtlseqdt0(W0,W1) ) % 117.15/117.19 => iLess0(W0,W1) ) ) ). % 117.15/117.19 % 117.15/117.19 fof(mDefDiv,definition, % 117.15/117.19 ! [W0,W1] : % 117.15/117.19 ( ( aNaturalNumber0(W0) % 117.15/117.19 & aNaturalNumber0(W1) ) % 117.15/117.19 => ( doDivides0(W0,W1) % 117.15/117.19 <=> ? [W2] : % 117.15/117.19 ( aNaturalNumber0(W2) % 117.15/117.19 & W1 = sdtasdt0(W0,W2) ) ) ) ). % 117.15/117.19 % 117.15/117.19 fof(mDefQuot,definition, % 117.15/117.19 ! [W0,W1] : % 117.15/117.19 ( ( aNaturalNumber0(W0) % 117.15/117.19 & aNaturalNumber0(W1) ) % 117.15/117.19 => ( ( W0 != sz00 % 117.15/117.19 & doDivides0(W0,W1) ) % 117.15/117.19 => ! [W2] : % 117.15/117.19 ( W2 = sdtsldt0(W1,W0) % 117.15/117.19 <=> ( aNaturalNumber0(W2) % 117.15/117.19 & W1 = sdtasdt0(W0,W2) ) ) ) ) ). % 117.15/117.19 % 117.15/117.19 fof(mDivTrans,axiom, % 117.15/117.19 ! [W0,W1,W2] : % 117.15/117.19 ( ( aNaturalNumber0(W0) % 117.15/117.19 & aNaturalNumber0(W1) % 117.15/117.19 & aNaturalNumber0(W2) ) % 117.15/117.19 => ( ( doDivides0(W0,W1) % 117.15/117.19 & doDivides0(W1,W2) ) % 117.15/117.19 => doDivides0(W0,W2) ) ) ). % 117.15/117.19 % 117.15/117.19 fof(mDivSum,axiom, % 117.15/117.19 ! [W0,W1,W2] : % 117.15/117.19 ( ( aNaturalNumber0(W0) % 117.15/117.19 & aNaturalNumber0(W1) % 117.15/117.19 & aNaturalNumber0(W2) ) % 117.15/117.19 => ( ( doDivides0(W0,W1) % 117.15/117.19 & doDivides0(W0,W2) ) % 117.15/117.19 => doDivides0(W0,sdtpldt0(W1,W2)) ) ) ). % 117.15/117.19 % 117.15/117.19 fof(mDivMin,axiom, % 117.15/117.19 ! [W0,W1,W2] : % 117.15/117.19 ( ( aNaturalNumber0(W0) % 117.15/117.19 & aNaturalNumber0(W1) % 117.15/117.19 & aNaturalNumber0(W2) ) % 117.15/117.19 => ( ( doDivides0(W0,W1) % 117.15/117.19 & doDivides0(W0,sdtpldt0(W1,W2)) ) % 117.15/117.19 => doDivides0(W0,W2) ) ) ). % 117.15/117.19 % 117.15/117.19 fof(mDivLE,axiom, % 117.15/117.19 ! [W0,W1] : % 117.15/117.19 ( ( aNaturalNumber0(W0) % 117.15/117.19 & aNaturalNumber0(W1) ) % 117.15/117.19 => ( ( doDivides0(W0,W1) % 117.15/117.19 & W1 != sz00 ) % 117.15/117.19 => sdtlseqdt0(W0,W1) ) ) ). % 117.15/117.19 % 117.15/117.19 fof(mDivAsso,axiom, % 117.15/117.19 ! [W0,W1] : % 117.15/117.19 ( ( aNaturalNumber0(W0) % 117.15/117.19 & aNaturalNumber0(W1) ) % 117.15/117.19 => ( ( W0 != sz00 % 117.15/117.19 & doDivides0(W0,W1) ) % 117.15/117.19 => ! [W2] : % 117.15/117.19 ( aNaturalNumber0(W2) % 117.15/117.19 => sdtasdt0(W2,sdtsldt0(W1,W0)) = sdtsldt0(sdtasdt0(W2,W1),W0) ) ) ) ). % 117.15/117.20 % 117.15/117.20 fof(mDefPrime,definition, % 117.15/117.20 ! [W0] : % 117.15/117.20 ( aNaturalNumber0(W0) % 117.15/117.20 => ( isPrime0(W0) % 117.15/117.20 <=> ( W0 != sz00 % 117.15/117.20 & W0 != sz10 % 117.15/117.20 & ! [W1] : % 117.15/117.20 ( ( aNaturalNumber0(W1) % 117.15/117.20 & doDivides0(W1,W0) ) % 117.15/117.20 => ( W1 = sz10 % 117.15/117.20 | W1 = W0 ) ) ) ) ) ). % 117.15/117.20 % 117.15/117.20 fof(mPrimDiv,axiom, % 117.15/117.20 ! [W0] : % 117.15/117.20 ( ( aNaturalNumber0(W0) % 117.15/117.20 & W0 != sz00 % 117.15/117.20 & W0 != sz10 ) % 117.15/117.20 => ? [W1] : % 117.15/117.20 ( aNaturalNumber0(W1) % 117.15/117.20 & doDivides0(W1,W0) % 117.15/117.20 & isPrime0(W1) ) ) ). % 117.15/117.20 % 117.15/117.20 fof(m__1837,hypothesis, % 117.15/117.20 ( aNaturalNumber0(xn) % 117.15/117.20 & aNaturalNumber0(xm) % 117.15/117.20 & aNaturalNumber0(xp) ) ). % 117.15/117.20 % 117.15/117.20 fof(m__1799,hypothesis, % 117.15/117.20 ! [W0,W1,W2] : % 117.15/117.20 ( ( aNaturalNumber0(W0) % 117.15/117.20 & aNaturalNumber0(W1) % 117.15/117.20 & aNaturalNumber0(W2) ) % 117.15/117.20 => ( ( isPrime0(W2) % 117.15/117.20 & doDivides0(W2,sdtasdt0(W0,W1)) ) % 117.15/117.20 => ( iLess0(sdtpldt0(sdtpldt0(W0,W1),W2),sdtpldt0(sdtpldt0(xn,xm),xp)) % 117.15/117.20 => ( doDivides0(W2,W0) % 117.15/117.20 | doDivides0(W2,W1) ) ) ) ) ). % 117.15/117.20 % 117.15/117.20 fof(m__1860,hypothesis, % 117.15/117.20 ( isPrime0(xp) % 117.15/117.20 & doDivides0(xp,sdtasdt0(xn,xm)) ) ). % 117.15/117.20 % 117.15/117.20 fof(m__1870,hypothesis, % 117.15/117.20 sdtlseqdt0(xp,xn) ). % 117.15/117.20 % 117.15/117.20 fof(m__1883,hypothesis, % 117.15/117.20 xr = sdtmndt0(xn,xp) ). % 117.15/117.20 % 117.15/117.20 fof(m__1894,hypothesis, % 117.15/117.20 ( xr != xn % 117.15/117.20 & sdtlseqdt0(xr,xn) ) ). % 117.15/117.20 % 117.15/117.20 fof(m__1924,hypothesis, % 117.15/117.20 xn = sdtpldt0(xp,xr) ). % 117.15/117.20 % 117.15/117.20 fof(m__1951,hypothesis, % 117.15/117.20 sdtasdt0(xn,xm) = sdtpldt0(sdtasdt0(xp,xm),sdtasdt0(xr,xm)) ). % 117.15/117.20 % 117.15/117.20 fof(m__1978,hypothesis, % 117.15/117.20 sdtasdt0(xr,xm) = sdtmndt0(sdtasdt0(xn,xm),sdtasdt0(xp,xm)) ). % 117.15/117.20 % 117.15/117.20 fof(m__,conjecture, % 117.15/117.20 doDivides0(xp,sdtasdt0(xp,xm)) ). % 117.15/117.20 % 117.15/117.20 %------------------------------------------------------------------------------ % 117.15/117.20 %------------------------------------------- % 117.15/117.20 % Proof found % 117.15/117.20 % SZS status Theorem for theBenchmark % 117.15/117.20 % SZS output start Proof % 117.15/117.20 %ClaNum:106(EqnAxiom:25) % 117.15/117.20 %VarNum:440(SingletonVarNum:131) % 117.15/117.20 %MaxLitNum:8 % 117.15/117.20 %MaxfuncDepth:2 % 117.15/117.20 %SharedTerms:31 % 117.15/117.20 %goalClause: 41 % 117.15/117.20 %singleGoalClaCount:1 % 117.15/117.20 [26]P1(a1) % 117.15/117.20 [27]P1(a10) % 117.15/117.20 [28]P1(a11) % 117.15/117.20 [29]P1(a12) % 117.15/117.20 [30]P1(a13) % 117.15/117.20 [31]P2(a13) % 117.15/117.20 [34]P5(a13,a11) % 117.15/117.20 [35]P5(a14,a11) % 117.15/117.20 [39]~E(a1,a10) % 117.15/117.20 [40]~E(a14,a11) % 117.15/117.20 [32]E(f2(a13,a14),a11) % 117.15/117.20 [33]E(f3(a11,a13),a14) % 117.15/117.20 [36]P3(a13,f4(a11,a12)) % 117.15/117.20 [41]~P3(a13,f4(a13,a12)) % 117.15/117.20 [37]E(f2(f4(a13,a12),f4(a14,a12)),f4(a11,a12)) % 117.15/117.20 [38]E(f3(f4(a11,a12),f4(a13,a12)),f4(a14,a12)) % 117.15/117.20 [52]~P1(x521)+P5(x521,x521) % 117.15/117.20 [44]~P1(x441)+E(f4(a1,x441),a1) % 117.15/117.20 [45]~P1(x451)+E(f4(x451,a1),a1) % 117.15/117.20 [46]~P1(x461)+E(f2(a1,x461),x461) % 117.15/117.20 [47]~P1(x471)+E(f4(a10,x471),x471) % 117.15/117.20 [48]~P1(x481)+E(f2(x481,a1),x481) % 117.15/117.20 [49]~P1(x491)+E(f4(x491,a10),x491) % 117.15/117.20 [42]~P1(x421)+~P2(x421)+~E(x421,a1) % 117.15/117.20 [43]~P1(x431)+~P2(x431)+~E(x431,a10) % 117.15/117.20 [63]~P1(x632)+~P1(x631)+E(f2(x631,x632),f2(x632,x631)) % 117.15/117.20 [64]~P1(x642)+~P1(x641)+E(f4(x641,x642),f4(x642,x641)) % 117.15/117.20 [66]~P1(x662)+~P1(x661)+P1(f2(x661,x662)) % 117.25/117.20 [67]~P1(x672)+~P1(x671)+P1(f4(x671,x672)) % 117.25/117.20 [54]~P1(x541)+E(x541,a10)+P5(a10,x541)+E(x541,a1) % 117.25/117.20 [50]~P1(x501)+E(x501,a10)+E(x501,a1)+P1(f5(x501)) % 117.25/117.20 [51]~P1(x511)+E(x511,a10)+E(x511,a1)+P2(f5(x511)) % 117.25/117.20 [57]~P1(x571)+E(x571,a10)+P3(f5(x571),x571)+E(x571,a1) % 117.25/117.20 [58]~E(x582,x581)+~P1(x581)+~P1(x582)+P5(x581,x582) % 117.25/117.20 [65]P5(x652,x651)+~P1(x651)+~P1(x652)+P5(x651,x652) % 117.25/117.20 [60]~P1(x602)+~P1(x601)+E(x601,a1)+~E(f2(x602,x601),a1) % 117.25/117.20 [61]~P1(x612)+~P1(x611)+E(x611,a1)+~E(f2(x611,x612),a1) % 117.25/117.20 [71]~P1(x712)+~P1(x711)+P5(x712,f4(x712,x711))+E(x711,a1) % 117.25/117.20 [77]~P1(x772)+~P1(x771)+~P5(x771,x772)+P1(f7(x771,x772)) % 117.25/117.20 [78]~P1(x782)+~P1(x781)+~P3(x781,x782)+P1(f8(x781,x782)) % 117.25/117.20 [85]~P1(x851)+~P1(x852)+~P3(x851,x852)+E(f4(x851,f8(x851,x852)),x852) % 117.25/117.20 [86]~P1(x862)+~P1(x861)+~P5(x861,x862)+E(f2(x861,f7(x861,x862)),x862) % 117.25/117.20 [95]~P1(x953)+~P1(x952)+~P1(x951)+E(f2(f2(x951,x952),x953),f2(x951,f2(x952,x953))) % 117.25/117.20 [96]~P1(x963)+~P1(x962)+~P1(x961)+E(f4(f4(x961,x962),x963),f4(x961,f4(x962,x963))) % 117.25/117.20 [104]~P1(x1043)+~P1(x1042)+~P1(x1041)+E(f2(f4(x1041,x1042),f4(x1041,x1043)),f4(x1041,f2(x1042,x1043))) % 117.25/117.20 [105]~P1(x1052)+~P1(x1053)+~P1(x1051)+E(f2(f4(x1051,x1052),f4(x1053,x1052)),f4(f2(x1051,x1053),x1052)) % 117.25/117.20 [53]P2(x531)+~P1(x531)+E(x531,a10)+E(x531,a1)+~E(f6(x531),a10) % 117.25/117.20 [55]P2(x551)+~P1(x551)+E(x551,a10)+~E(f6(x551),x551)+E(x551,a1) % 117.25/117.20 [56]P2(x561)+~P1(x561)+E(x561,a10)+E(x561,a1)+P1(f6(x561)) % 117.25/117.20 [59]P2(x591)+~P1(x591)+E(x591,a10)+P3(f6(x591),x591)+E(x591,a1) % 117.25/117.20 [69]~P1(x691)+~P1(x692)+~P3(x692,x691)+P5(x692,x691)+E(x691,a1) % 117.25/117.20 [70]P4(x701,x702)+~P1(x702)+~P1(x701)+~P5(x701,x702)+E(x701,x702) % 117.25/117.20 [74]~P1(x742)+~P1(x741)+~P5(x742,x741)+~P5(x741,x742)+E(x741,x742) % 117.25/117.20 [62]~P1(x621)+~P1(x622)+E(x621,a1)+E(x622,a1)+~E(f4(x622,x621),a1) % 117.25/117.20 [72]~P1(x721)+~P1(x722)+~P1(x723)+P3(x721,x722)+~E(x722,f4(x721,x723)) % 117.25/117.20 [73]~P1(x732)+~P1(x731)+~P1(x733)+P5(x731,x732)+~E(f2(x731,x733),x732) % 117.25/117.20 [75]~P1(x753)+~P1(x752)+~P5(x753,x752)+P1(x751)+~E(x751,f3(x752,x753)) % 117.25/117.20 [79]~P1(x792)+~P1(x791)+~P1(x793)+E(x791,x792)+~E(f2(x793,x791),f2(x793,x792)) % 117.25/117.20 [80]~P1(x802)+~P1(x803)+~P1(x801)+E(x801,x802)+~E(f2(x801,x803),f2(x802,x803)) % 117.25/117.20 [83]~P1(x833)+~P1(x831)+~P5(x831,x833)+~E(x832,f3(x833,x831))+E(f2(x831,x832),x833) % 117.25/117.20 [68]~P1(x682)+~P1(x681)+~P2(x682)+~P3(x681,x682)+E(x681,x682)+E(x681,a10) % 117.25/117.20 [87]~P1(x872)+~P1(x871)+~P5(x873,x872)+~P5(x871,x873)+P5(x871,x872)+~P1(x873) % 117.25/117.20 [88]~P1(x882)+~P1(x881)+~P3(x883,x882)+~P3(x881,x883)+P3(x881,x882)+~P1(x883) % 117.25/117.20 [76]~P1(x761)+~P1(x763)+~P3(x761,x763)+P1(x762)+E(x761,a1)+~E(x762,f9(x763,x761)) % 117.25/117.20 [81]~P1(x812)+~P1(x811)+~P1(x813)+E(x811,x812)+~E(f4(x813,x811),f4(x813,x812))+E(x813,a1) % 117.25/117.20 [82]~P1(x822)+~P1(x823)+~P1(x821)+E(x821,x822)+~E(f4(x821,x823),f4(x822,x823))+E(x823,a1) % 117.25/117.20 [84]~P1(x841)+~P1(x842)+~P3(x841,x842)+~E(x843,f9(x842,x841))+E(x841,a1)+E(x842,f4(x841,x843)) % 117.25/117.20 [89]~P1(x892)+~P1(x893)+~P1(x891)+~P5(x893,x892)+~E(f2(x893,x891),x892)+E(x891,f3(x892,x893)) % 117.25/117.20 [97]~P1(x973)+~P1(x972)+~P1(x971)+~P3(x971,x973)+~P3(x971,x972)+P3(x971,f2(x972,x973)) % 117.25/117.20 [98]~P1(x982)+~P1(x981)+~P1(x983)+~P5(x981,x982)+E(x981,x982)+P5(f2(x983,x981),f2(x983,x982)) % 117.25/117.20 [99]~P1(x992)+~P1(x993)+~P1(x991)+~P5(x991,x992)+E(x991,x992)+P5(f2(x991,x993),f2(x992,x993)) % 117.25/117.20 [102]~P1(x1022)+~P1(x1021)+~P3(x1021,x1023)+P3(x1021,x1022)+~P1(x1023)+~P3(x1021,f2(x1023,x1022)) % 117.25/117.20 [103]~P1(x1032)+~P1(x1033)+~P1(x1031)+~P3(x1031,x1033)+E(x1031,a1)+E(f9(f4(x1032,x1033),x1031),f4(x1032,f9(x1033,x1031))) % 117.25/117.20 [90]~P1(x901)+~P1(x903)+~P1(x902)+~P3(x901,x903)+~E(x903,f4(x901,x902))+E(x901,a1)+E(x902,f9(x903,x901)) % 117.25/117.20 [100]~P1(x1002)+~P1(x1001)+~P1(x1003)+~P5(x1001,x1002)+E(x1001,x1002)+P5(f4(x1003,x1001),f4(x1003,x1002))+E(x1003,a1) % 117.25/117.20 [101]~P1(x1012)+~P1(x1013)+~P1(x1011)+~P5(x1011,x1012)+E(x1011,x1012)+P5(f4(x1011,x1013),f4(x1012,x1013))+E(x1013,a1) % 117.25/117.20 [106]~P1(x1061)+~P1(x1062)+~P1(x1063)+~P2(x1061)+P3(x1061,x1062)+P3(x1061,x1063)+~P3(x1061,f4(x1063,x1062))+~P4(f2(f2(x1063,x1062),x1061),f2(f2(a11,a12),a13)) % 117.25/117.20 %EqnAxiom % 117.25/117.20 [1]E(x11,x11) % 117.25/117.20 [2]E(x22,x21)+~E(x21,x22) % 117.25/117.20 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 117.25/117.20 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 117.25/117.20 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 117.25/117.20 [6]~E(x61,x62)+E(f3(x61,x63),f3(x62,x63)) % 117.25/117.20 [7]~E(x71,x72)+E(f3(x73,x71),f3(x73,x72)) % 117.25/117.20 [8]~E(x81,x82)+E(f4(x81,x83),f4(x82,x83)) % 117.25/117.20 [9]~E(x91,x92)+E(f4(x93,x91),f4(x93,x92)) % 117.25/117.20 [10]~E(x101,x102)+E(f9(x101,x103),f9(x102,x103)) % 117.25/117.20 [11]~E(x111,x112)+E(f9(x113,x111),f9(x113,x112)) % 117.25/117.20 [12]~E(x121,x122)+E(f7(x121,x123),f7(x122,x123)) % 117.25/117.20 [13]~E(x131,x132)+E(f7(x133,x131),f7(x133,x132)) % 117.25/117.20 [14]~E(x141,x142)+E(f8(x141,x143),f8(x142,x143)) % 117.25/117.20 [15]~E(x151,x152)+E(f8(x153,x151),f8(x153,x152)) % 117.25/117.20 [16]~E(x161,x162)+E(f5(x161),f5(x162)) % 117.25/117.20 [17]~E(x171,x172)+E(f6(x171),f6(x172)) % 117.25/117.20 [18]~P1(x181)+P1(x182)+~E(x181,x182) % 117.25/117.20 [19]P4(x192,x193)+~E(x191,x192)+~P4(x191,x193) % 117.25/117.20 [20]P4(x203,x202)+~E(x201,x202)+~P4(x203,x201) % 117.25/117.20 [21]P3(x212,x213)+~E(x211,x212)+~P3(x211,x213) % 117.25/117.20 [22]P3(x223,x222)+~E(x221,x222)+~P3(x223,x221) % 117.25/117.20 [23]~P2(x231)+P2(x232)+~E(x231,x232) % 117.25/117.20 [24]P5(x242,x243)+~E(x241,x242)+~P5(x241,x243) % 117.25/117.20 [25]P5(x253,x252)+~E(x251,x252)+~P5(x253,x251) % 117.25/117.20 % 117.25/117.20 %------------------------------------------- % 117.25/117.20 cnf(107,plain, % 117.25/117.20 (~P2(a1)+~P1(a1)), % 117.25/117.20 inference(equality_inference,[],[42])). % 117.25/117.20 cnf(108,plain, % 117.25/117.20 (~P2(a10)+~P1(a10)), % 117.25/117.20 inference(equality_inference,[],[43])). % 117.25/117.20 cnf(110,plain, % 117.25/117.20 (P3(x1101,f4(x1101,x1102))+~P1(x1101)+~P1(f4(x1101,x1102))+~P1(x1102)), % 117.25/117.20 inference(equality_inference,[],[72])). % 117.25/117.20 cnf(111,plain, % 117.25/117.20 (P5(x1111,f2(x1111,x1112))+~P1(f2(x1111,x1112))+~P1(x1111)+~P1(x1112)), % 117.25/117.20 inference(equality_inference,[],[73])). % 117.25/117.20 cnf(112,plain, % 117.25/117.20 (~P5(x1121,x1122)+~P1(x1121)+~P1(x1122)+P1(f3(x1122,x1121))), % 117.25/117.20 inference(equality_inference,[],[75])). % 117.25/117.20 cnf(113,plain, % 117.25/117.20 (~P3(x1131,x1132)+~P1(x1131)+~P1(x1132)+P1(f9(x1132,x1131))+E(x1131,a1)), % 117.25/117.20 inference(equality_inference,[],[76])). % 117.25/117.20 cnf(118,plain, % 117.25/117.20 (~P5(x1181,x1182)+~P1(x1182)+~P1(x1181)+E(f2(x1181,f3(x1182,x1181)),x1182)), % 117.25/117.20 inference(equality_inference,[],[83])). % 117.25/117.20 cnf(119,plain, % 117.25/117.20 (~P3(x1191,x1192)+~P1(x1191)+~P1(x1192)+E(x1191,a1)+E(x1192,f4(x1191,f9(x1192,x1191)))), % 117.25/117.20 inference(equality_inference,[],[84])). % 117.25/117.20 cnf(120,plain, % 117.25/117.20 (~P5(x1201,f2(x1201,x1202))+~P1(f2(x1201,x1202))+~P1(x1201)+~P1(x1202)+E(x1202,f3(f2(x1201,x1202),x1201))), % 117.25/117.20 inference(equality_inference,[],[89])). % 117.25/117.20 cnf(121,plain, % 117.25/117.20 (~P3(x1211,f4(x1211,x1212))+~P1(x1211)+~P1(f4(x1211,x1212))+~P1(x1212)+E(x1211,a1)+E(x1212,f9(f4(x1211,x1212),x1211))), % 117.25/117.20 inference(equality_inference,[],[90])). % 117.25/117.20 cnf(122,plain, % 117.25/117.20 (~P2(a1)), % 117.25/117.20 inference(scs_inference,[],[26,107])). % 117.25/117.21 cnf(123,plain, % 117.25/117.21 (~P2(a10)), % 117.25/117.21 inference(scs_inference,[],[27,108])). % 117.25/117.21 cnf(124,plain, % 117.25/117.21 (E(f4(a14,a12),f3(f4(a11,a12),f4(a13,a12)))), % 117.25/117.21 inference(scs_inference,[],[38,2])). % 117.25/117.21 cnf(126,plain, % 117.25/117.21 (~E(a14,f2(a13,a14))), % 117.25/117.21 inference(scs_inference,[],[41,40,38,32,36,2,22,3])). % 117.25/117.21 cnf(127,plain, % 117.25/117.21 (P5(a1,a1)), % 117.25/117.21 inference(scs_inference,[],[41,26,40,38,32,36,2,22,3,65])). % 117.25/117.21 cnf(129,plain, % 117.25/117.21 (E(f2(a1,f3(a1,a1)),a1)), % 117.25/117.21 inference(scs_inference,[],[41,26,40,38,32,36,2,22,3,65,118])). % 117.25/117.21 cnf(131,plain, % 117.25/117.21 (~E(a11,a13)), % 117.25/117.21 inference(scs_inference,[],[41,26,40,38,32,36,2,22,3,65,118,8])). % 117.25/117.21 cnf(132,plain, % 117.25/117.21 (P3(x1321,f4(a11,a12))+~E(a13,x1321)), % 117.25/117.21 inference(scs_inference,[],[41,26,40,38,32,36,2,22,3,65,118,8,21])). % 117.25/117.21 cnf(133,plain, % 117.25/117.21 (P1(f3(a1,a1))), % 117.25/117.21 inference(scs_inference,[],[41,26,40,38,32,36,2,22,3,65,118,8,21,112])). % 117.25/117.21 cnf(135,plain, % 117.25/117.21 (E(f3(a1,a1),a1)), % 117.25/117.21 inference(scs_inference,[],[41,26,40,38,32,36,2,22,3,65,118,8,21,112,60])). % 117.25/117.21 cnf(137,plain, % 117.25/117.21 (~P5(a11,a13)), % 117.25/117.21 inference(scs_inference,[],[41,26,28,30,34,40,38,32,36,2,22,3,65,118,8,21,112,60,74])). % 117.25/117.21 cnf(143,plain, % 117.25/117.21 (P5(x1431,a11)+~E(a13,x1431)), % 117.25/117.21 inference(scs_inference,[],[41,26,28,30,34,40,38,32,36,2,22,3,65,118,8,21,112,60,74,18,42,23,24])). % 117.25/117.21 cnf(144,plain, % 117.25/117.21 (P5(a13,x1441)+~E(a11,x1441)), % 117.25/117.21 inference(scs_inference,[],[41,26,28,30,34,40,38,32,36,2,22,3,65,118,8,21,112,60,74,18,42,23,24,25])). % 117.25/117.21 cnf(148,plain, % 117.25/117.21 (E(a1,f3(a1,a1))), % 117.25/117.21 inference(scs_inference,[],[135,2])). % 117.25/117.21 cnf(149,plain, % 117.25/117.21 (~P2(f3(a1,a1))), % 117.25/117.21 inference(scs_inference,[],[133,135,2,42])). % 117.25/117.21 cnf(151,plain, % 117.25/117.21 (~P2(f2(a1,f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[133,135,129,122,2,42,23])). % 117.25/117.21 cnf(152,plain, % 117.25/117.21 (P5(f3(a1,a1),a1)), % 117.25/117.21 inference(scs_inference,[],[133,127,135,129,122,2,42,23,24])). % 117.25/117.21 cnf(153,plain, % 117.25/117.21 (P5(a1,f3(a1,a1))), % 117.25/117.21 inference(scs_inference,[],[133,127,135,129,122,2,42,23,24,25])). % 117.25/117.21 cnf(154,plain, % 117.25/117.21 (P5(f3(a1,a1),f3(a1,a1))), % 117.25/117.21 inference(scs_inference,[],[133,127,135,129,122,2,42,23,24,25,65])). % 117.25/117.21 cnf(156,plain, % 117.25/117.21 (E(f2(f3(a1,a1),f3(f3(a1,a1),f3(a1,a1))),f3(a1,a1))), % 117.25/117.21 inference(scs_inference,[],[133,127,135,129,122,2,42,23,24,25,65,118])). % 117.25/117.21 cnf(158,plain, % 117.25/117.21 (P1(f3(f3(a1,a1),f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[133,127,135,129,122,2,42,23,24,25,65,118,112])). % 117.25/117.21 cnf(160,plain, % 117.25/117.21 (P1(f2(f3(a1,a1),f3(f3(a1,a1),f3(a1,a1))))), % 117.25/117.21 inference(scs_inference,[],[26,133,127,135,129,122,2,42,23,24,25,65,118,112,75])). % 117.25/117.21 cnf(162,plain, % 117.25/117.21 (E(x1621,a1)+~E(x1621,f2(a1,f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[26,133,127,135,129,122,2,42,23,24,25,65,118,112,75,3])). % 117.25/117.21 cnf(168,plain, % 117.25/117.21 (E(a1,f2(a1,f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[129,2])). % 117.25/117.21 cnf(169,plain, % 117.25/117.21 (~P2(f2(f3(a1,a1),f3(f3(a1,a1),f3(a1,a1))))), % 117.25/117.21 inference(scs_inference,[],[129,156,149,2,23])). % 117.25/117.21 cnf(170,plain, % 117.25/117.21 (E(f2(f3(a1,a1),f3(f3(a1,a1),f3(a1,a1))),a1)), % 117.25/117.21 inference(scs_inference,[],[129,135,156,149,2,23,3])). % 117.25/117.21 cnf(171,plain, % 117.25/117.21 (P1(f2(a1,f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[26,129,135,156,149,2,23,3,18])). % 117.25/117.21 cnf(172,plain, % 117.25/117.21 (P5(f3(f3(a1,a1),f3(a1,a1)),f3(f3(a1,a1),f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[26,158,129,135,156,149,2,23,3,18,65])). % 117.25/117.21 cnf(174,plain, % 117.25/117.21 (E(f3(f3(a1,a1),f3(a1,a1)),a1)), % 117.25/117.21 inference(scs_inference,[],[26,158,133,129,135,156,149,2,23,3,18,65,60])). % 117.25/117.21 cnf(176,plain, % 117.25/117.21 (E(f3(f3(a1,a1),f3(a1,a1)),f3(a1,f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[26,158,133,129,135,156,149,152,2,23,3,18,65,60,89])). % 117.25/117.21 cnf(178,plain, % 117.25/117.21 (~P2(f3(f3(a1,a1),f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[26,158,133,129,135,156,149,152,2,23,3,18,65,60,89,42])). % 117.25/117.21 cnf(180,plain, % 117.25/117.21 (P5(x1801,a11)+~E(a14,x1801)), % 117.25/117.21 inference(scs_inference,[],[26,158,133,129,135,156,149,152,35,2,23,3,18,65,60,89,42,24])). % 117.25/117.21 cnf(181,plain, % 117.25/117.21 (P5(f3(f3(a1,a1),f3(a1,a1)),a1)), % 117.25/117.21 inference(scs_inference,[],[26,158,133,129,135,156,149,152,35,2,23,3,18,65,60,89,42,24,25])). % 117.25/117.21 cnf(182,plain, % 117.25/117.21 (E(f2(a10,f3(a10,a10)),a10)+~P5(a10,a10)), % 117.25/117.21 inference(scs_inference,[],[26,158,27,133,129,135,156,149,152,35,2,23,3,18,65,60,89,42,24,25,118])). % 117.25/117.21 cnf(188,plain, % 117.25/117.21 (P5(a10,a10)), % 117.25/117.21 inference(scs_inference,[],[26,158,27,133,129,135,156,149,152,35,2,23,3,18,65,60,89,42,24,25,118,110,111,58])). % 117.25/117.21 cnf(192,plain, % 117.25/117.21 (E(f2(a10,f3(a10,a10)),a10)), % 117.25/117.21 inference(scs_inference,[],[188,182])). % 117.25/117.21 cnf(193,plain, % 117.25/117.21 (E(f3(a1,a1),f2(f3(a1,a1),f3(f3(a1,a1),f3(a1,a1))))), % 117.25/117.21 inference(scs_inference,[],[156,188,182,2])). % 117.25/117.21 cnf(194,plain, % 117.25/117.21 (~P2(f2(a10,f3(a10,a10)))), % 117.25/117.21 inference(scs_inference,[],[156,123,188,182,2,23])). % 117.25/117.21 cnf(195,plain, % 117.25/117.21 (E(f2(a1,f3(a1,a1)),f3(a1,a1))), % 117.25/117.21 inference(scs_inference,[],[129,156,148,123,188,182,2,23,3])). % 117.25/117.21 cnf(197,plain, % 117.25/117.21 (P5(f3(f3(a1,a1),f3(a1,a1)),f3(a1,f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[129,156,148,172,176,123,188,182,2,23,3,24,25])). % 117.25/117.21 cnf(198,plain, % 117.25/117.21 (P1(f3(a1,f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[158,129,156,148,172,176,123,188,182,2,23,3,24,25,18])). % 117.25/117.21 cnf(199,plain, % 117.25/117.21 (P5(a11,a11)), % 117.25/117.21 inference(scs_inference,[],[28,158,129,156,148,172,176,123,188,182,2,23,3,24,25,18,65])). % 117.25/117.21 cnf(201,plain, % 117.25/117.21 (E(f2(a11,f3(a11,a11)),a11)), % 117.25/117.21 inference(scs_inference,[],[28,158,129,156,148,172,176,123,188,182,2,23,3,24,25,18,65,118])). % 117.25/117.21 cnf(203,plain, % 117.25/117.21 (P1(f3(a11,a11))), % 117.25/117.21 inference(scs_inference,[],[28,158,129,156,148,172,176,123,188,182,2,23,3,24,25,18,65,118,112])). % 117.25/117.21 cnf(205,plain, % 117.25/117.21 (E(f3(a1,f3(a1,a1)),f3(f3(a1,a1),f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[28,158,129,156,148,172,176,123,188,182,2,23,3,24,25,18,65,118,112,74])). % 117.25/117.21 cnf(207,plain, % 117.25/117.21 (P5(f3(a1,f3(a1,a1)),a1)), % 117.25/117.21 inference(scs_inference,[],[26,28,158,129,156,148,172,181,176,123,188,182,2,23,3,24,25,18,65,118,112,74,87])). % 117.25/117.21 cnf(209,plain, % 117.25/117.21 (E(f3(a1,a1),f3(f3(a1,a1),a1))), % 117.25/117.21 inference(scs_inference,[],[26,28,133,158,153,129,156,148,172,181,176,123,188,182,2,23,3,24,25,18,65,118,112,74,87,89])). % 117.25/117.21 cnf(211,plain, % 117.25/117.21 (P3(a11,f4(a11,a11))+~P1(f4(a11,a11))), % 117.25/117.21 inference(scs_inference,[],[26,28,133,158,153,129,156,148,172,181,176,123,188,182,2,23,3,24,25,18,65,118,112,74,87,89,110])). % 117.25/117.21 cnf(214,plain, % 117.25/117.21 (E(a1,f2(f3(a1,a1),f3(f3(a1,a1),f3(a1,a1))))), % 117.25/117.21 inference(scs_inference,[],[170,2])). % 117.25/117.21 cnf(215,plain, % 117.25/117.21 (~P2(f3(a1,f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[170,178,205,2,23])). % 117.25/117.21 cnf(217,plain, % 117.25/117.21 (P5(a1,f3(a1,f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[170,174,178,197,205,2,23,3,24])). % 117.25/117.21 cnf(218,plain, % 117.25/117.21 (P5(f3(a1,f3(a1,a1)),f3(a1,a1))), % 117.25/117.21 inference(scs_inference,[],[170,148,174,178,197,205,207,2,23,3,24,25])). % 117.25/117.21 cnf(219,plain, % 117.25/117.21 (P1(f3(f3(a1,a1),a1))), % 117.25/117.21 inference(scs_inference,[],[133,170,148,174,178,209,197,205,207,2,23,3,24,25,18])). % 117.25/117.21 cnf(220,plain, % 117.25/117.21 (P5(f2(a1,f3(a1,a1)),f2(a1,f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[133,171,170,148,174,178,209,197,205,207,2,23,3,24,25,18,65])). % 117.25/117.21 cnf(222,plain, % 117.25/117.21 (P1(f3(a10,a10))), % 117.25/117.21 inference(scs_inference,[],[133,171,27,170,148,174,178,209,197,205,207,188,2,23,3,24,25,18,65,112])). % 117.25/117.21 cnf(224,plain, % 117.25/117.21 (E(a1,f3(a1,f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[26,133,171,198,27,170,148,174,178,209,197,205,207,188,2,23,3,24,25,18,65,112,74])). % 117.25/117.21 cnf(230,plain, % 117.25/117.21 (~E(a1,f2(a10,f3(a10,a10)))), % 117.25/117.21 inference(scs_inference,[],[195,192,39,2,3])). % 117.25/117.21 cnf(231,plain, % 117.25/117.21 (P5(a1,f3(f3(a1,a1),f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[195,192,174,172,39,2,3,24])). % 117.25/117.21 cnf(232,plain, % 117.25/117.21 (P5(f3(f3(a1,a1),f3(a1,a1)),f3(a1,a1))), % 117.25/117.21 inference(scs_inference,[],[195,192,148,174,181,172,39,2,3,24,25])). % 117.25/117.21 cnf(233,plain, % 117.25/117.21 (P5(f3(a10,a10),f3(a10,a10))), % 117.25/117.21 inference(scs_inference,[],[222,195,192,148,174,181,172,39,2,3,24,25,65])). % 117.25/117.21 cnf(235,plain, % 117.25/117.21 (E(f2(f3(a10,a10),f3(f3(a10,a10),f3(a10,a10))),f3(a10,a10))), % 117.25/117.21 inference(scs_inference,[],[222,195,192,148,174,181,172,39,2,3,24,25,65,118])). % 117.25/117.21 cnf(237,plain, % 117.25/117.21 (P1(f3(f3(a10,a10),f3(a10,a10)))), % 117.25/117.21 inference(scs_inference,[],[222,195,192,148,174,181,172,39,2,3,24,25,65,118,112])). % 117.25/117.21 cnf(239,plain, % 117.25/117.21 (P1(f2(f3(a10,a10),f3(f3(a10,a10),f3(a10,a10))))), % 117.25/117.21 inference(scs_inference,[],[27,222,195,192,148,174,181,172,39,188,2,3,24,25,65,118,112,75])). % 117.25/117.21 cnf(241,plain, % 117.25/117.21 (E(a1,f3(f3(a1,a1),f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[26,27,158,222,195,192,148,174,181,172,39,188,2,3,24,25,65,118,112,75,74])). % 117.25/117.21 cnf(247,plain, % 117.25/117.21 (P5(a11,f2(a11,a11))+~P1(f2(a11,a11))), % 117.25/117.21 inference(scs_inference,[],[26,28,27,158,222,195,192,148,174,201,181,172,39,33,188,2,3,24,25,65,118,112,75,74,23,18,110,111])). % 117.25/117.21 cnf(249,plain, % 117.25/117.21 (P5(f3(f3(a1,a1),a1),f3(f3(a1,a1),a1))), % 117.25/117.21 inference(scs_inference,[],[26,28,27,158,222,219,195,192,148,174,201,181,172,39,33,188,2,3,24,25,65,118,112,75,74,23,18,110,111,58])). % 117.25/117.21 cnf(251,plain, % 117.25/117.21 (E(a11,f3(f2(a11,a11),a11))+~P1(f2(a11,a11))), % 117.25/117.21 inference(scs_inference,[],[26,28,27,158,222,219,195,192,148,174,201,181,172,39,33,188,2,3,24,25,65,118,112,75,74,23,18,110,111,58,120])). % 117.25/117.21 cnf(253,plain, % 117.25/117.21 (E(a10,f2(a10,f3(a10,a10)))), % 117.25/117.21 inference(scs_inference,[],[192,2])). % 117.25/117.21 cnf(254,plain, % 117.25/117.21 (~E(a14,f2(a11,f3(a11,a11)))), % 117.25/117.21 inference(scs_inference,[],[192,201,40,2,3])). % 117.25/117.21 cnf(255,plain, % 117.25/117.21 (P5(f3(a1,a1),f3(a1,f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[192,148,201,217,40,2,3,24])). % 117.25/117.21 cnf(256,plain, % 117.25/117.21 (P5(f2(a1,f3(a1,a1)),a1)), % 117.25/117.21 inference(scs_inference,[],[129,192,148,201,217,220,40,2,3,24,25])). % 117.25/117.21 cnf(257,plain, % 117.25/117.21 (P1(f2(a10,f3(a10,a10)))), % 117.25/117.21 inference(scs_inference,[],[27,129,192,148,201,217,220,40,2,3,24,25,18])). % 117.25/117.21 cnf(260,plain, % 117.25/117.21 (E(f3(a1,a1),f3(a1,f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[133,27,237,198,129,192,148,201,218,217,220,40,2,3,24,25,18,65,74])). % 117.25/117.21 cnf(263,plain, % 117.25/117.21 (E(f2(f3(a11,a11),f3(f3(a11,a11),f3(a11,a11))),f3(a11,a11))+~P5(f3(a11,a11),f3(a11,a11))), % 117.25/117.21 inference(scs_inference,[],[133,27,237,203,198,129,192,148,201,218,217,220,235,40,2,3,24,25,18,65,74,23,118])). % 117.25/117.21 cnf(265,plain, % 117.25/117.21 (P3(f3(a10,a10),f4(f3(a10,a10),f3(a10,a10)))+~P1(f4(f3(a10,a10),f3(a10,a10)))), % 117.25/117.21 inference(scs_inference,[],[133,27,222,237,203,198,129,192,148,201,218,217,220,235,40,2,3,24,25,18,65,74,23,118,110])). % 117.25/117.21 cnf(267,plain, % 117.25/117.21 (P5(f3(a1,a1),f2(f3(a1,a1),f3(a1,a1)))+~P1(f2(f3(a1,a1),f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[133,27,222,237,203,198,129,192,148,201,218,217,220,235,40,2,3,24,25,18,65,74,23,118,110,111])). % 117.25/117.21 cnf(269,plain, % 117.25/117.21 (P5(f3(a11,a11),f3(a11,a11))), % 117.25/117.21 inference(scs_inference,[],[133,27,222,237,203,198,129,192,148,201,218,217,220,235,40,2,3,24,25,18,65,74,23,118,110,111,58])). % 117.25/117.21 cnf(272,plain, % 117.25/117.21 (E(f2(f3(a11,a11),f3(f3(a11,a11),f3(a11,a11))),f3(a11,a11))), % 117.25/117.21 inference(scs_inference,[],[269,263])). % 117.25/117.21 cnf(273,plain, % 117.25/117.21 (E(f3(f3(a1,a1),a1),f3(a1,a1))), % 117.25/117.21 inference(scs_inference,[],[209,269,263,2])). % 117.25/117.21 cnf(274,plain, % 117.25/117.21 (~P2(f3(f3(a1,a1),a1))), % 117.25/117.21 inference(scs_inference,[],[209,269,149,263,2,23])). % 117.25/117.21 cnf(275,plain, % 117.25/117.21 (P5(f3(a1,a1),f3(f3(a1,a1),f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[148,209,231,269,149,263,2,23,24])). % 117.25/117.21 cnf(277,plain, % 117.25/117.21 (P5(f2(a10,f3(a10,a10)),f2(a10,f3(a10,a10)))), % 117.25/117.21 inference(scs_inference,[],[257,148,209,231,269,249,149,263,2,23,24,25,65])). % 117.25/117.21 cnf(279,plain, % 117.25/117.21 (P1(f3(f3(a11,a11),f3(a11,a11)))), % 117.25/117.21 inference(scs_inference,[],[257,203,148,209,231,269,249,149,263,2,23,24,25,65,112])). % 117.25/117.21 cnf(283,plain, % 117.25/117.21 (E(f3(a1,a1),f3(f3(a1,a1),f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[28,133,158,257,203,148,209,199,232,231,269,249,149,263,2,23,24,25,65,112,75,74])). % 117.25/117.21 cnf(285,plain, % 117.25/117.21 (P5(f3(f3(a1,a1),a1),a1)), % 117.25/117.21 inference(scs_inference,[],[26,28,133,158,257,219,203,152,148,209,199,232,231,269,249,149,263,2,23,24,25,65,112,75,74,87])). % 117.25/117.21 cnf(294,plain, % 117.25/117.21 (E(a11,f2(a11,f3(a11,a11)))), % 117.25/117.21 inference(scs_inference,[],[201,2])). % 117.25/117.21 cnf(295,plain, % 117.25/117.21 (E(f2(a1,f3(a1,a1)),f3(f3(a1,a1),a1))), % 117.25/117.21 inference(scs_inference,[],[195,209,201,2,3])). % 117.25/117.21 cnf(297,plain, % 117.25/117.21 (P5(a13,f2(a11,f3(a11,a11)))), % 117.25/117.21 inference(scs_inference,[],[195,209,201,199,34,2,3,24,25])). % 117.25/117.21 cnf(298,plain, % 117.25/117.21 (P1(f2(a11,f3(a11,a11)))), % 117.25/117.21 inference(scs_inference,[],[28,195,209,201,199,34,2,3,24,25,18])). % 117.25/117.21 cnf(299,plain, % 117.25/117.21 (P5(f3(f3(a11,a11),f3(a11,a11)),f3(f3(a11,a11),f3(a11,a11)))), % 117.25/117.21 inference(scs_inference,[],[28,279,195,209,201,199,34,2,3,24,25,18,65])). % 117.25/117.21 cnf(301,plain, % 117.25/117.21 (P5(a1,f3(f3(a1,a1),a1))), % 117.25/117.21 inference(scs_inference,[],[26,28,133,279,219,195,209,201,199,34,2,3,24,25,18,65,73])). % 117.25/117.21 cnf(305,plain, % 117.25/117.21 (E(f3(a1,a1),f3(f3(f3(a1,a1),a1),a1))), % 117.25/117.21 inference(scs_inference,[],[26,28,133,158,279,219,195,209,201,199,34,232,275,2,3,24,25,18,65,73,74,89])). % 117.25/117.21 cnf(308,plain, % 117.25/117.21 (E(f2(a12,f3(a12,a12)),a12)+~P5(a12,a12)), % 117.25/117.21 inference(scs_inference,[],[26,28,133,158,279,29,219,195,209,201,199,34,232,275,272,2,3,24,25,18,65,73,74,89,23,118])). % 117.25/117.21 cnf(312,plain, % 117.25/117.21 (P5(a12,a12)), % 117.25/117.21 inference(scs_inference,[],[26,28,133,158,203,279,29,219,195,209,201,199,34,232,275,272,2,3,24,25,18,65,73,74,89,23,118,110,58])). % 117.25/117.21 cnf(315,plain, % 117.25/117.21 (E(f2(a12,f3(a12,a12)),a12)), % 117.25/117.21 inference(scs_inference,[],[312,308])). % 117.25/117.21 cnf(316,plain, % 117.25/117.21 (E(f3(a10,a10),f2(f3(a10,a10),f3(f3(a10,a10),f3(a10,a10))))), % 117.25/117.21 inference(scs_inference,[],[235,312,308,2])). % 117.25/117.21 cnf(317,plain, % 117.25/117.21 (E(f2(a1,f3(a1,a1)),f3(a1,f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[195,235,260,312,308,2,3])). % 117.25/117.21 cnf(318,plain, % 117.25/117.21 (P5(a1,f2(a1,f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[129,195,235,260,220,312,308,2,3,24])). % 117.25/117.21 cnf(319,plain, % 117.25/117.21 (P5(f2(a1,f3(a1,a1)),f3(a1,a1))), % 117.25/117.21 inference(scs_inference,[],[129,195,148,235,260,220,256,312,308,2,3,24,25])). % 117.25/117.21 cnf(320,plain, % 117.25/117.21 (P1(f3(f3(f3(a1,a1),a1),a1))), % 117.25/117.21 inference(scs_inference,[],[133,129,195,148,235,260,220,256,305,312,308,2,3,24,25,18])). % 117.25/117.21 cnf(321,plain, % 117.25/117.21 (P5(f2(a11,f3(a11,a11)),f2(a11,f3(a11,a11)))), % 117.25/117.21 inference(scs_inference,[],[133,298,129,195,148,235,260,220,256,305,312,308,2,3,24,25,18,65])). % 117.25/117.21 cnf(323,plain, % 117.25/117.21 (P1(f3(a12,a12))), % 117.25/117.21 inference(scs_inference,[],[133,298,29,129,195,148,235,260,220,256,305,312,308,2,3,24,25,18,65,112])). % 117.25/117.21 cnf(327,plain, % 117.25/117.21 (E(f3(a1,a1),f3(f3(a1,f3(a1,a1)),a1))), % 117.25/117.21 inference(scs_inference,[],[26,133,298,198,29,129,195,148,235,218,217,260,220,256,255,305,312,308,2,3,24,25,18,65,112,74,89])). % 117.25/117.21 cnf(333,plain, % 117.25/117.21 (E(f3(a11,a11),f2(f3(a11,a11),f3(f3(a11,a11),f3(a11,a11))))), % 117.25/117.21 inference(scs_inference,[],[272,2])). % 117.25/117.21 cnf(334,plain, % 117.25/117.21 (E(a1,f3(f3(a1,a1),a1))), % 117.25/117.21 inference(scs_inference,[],[272,168,295,2,3])). % 117.25/117.21 cnf(337,plain, % 117.25/117.21 (P1(f3(f3(a1,f3(a1,a1)),a1))), % 117.25/117.21 inference(scs_inference,[],[133,272,168,295,273,249,233,316,327,2,3,24,25,18])). % 117.25/117.21 cnf(338,plain, % 117.25/117.21 (P5(f3(a12,a12),f3(a12,a12))), % 117.25/117.21 inference(scs_inference,[],[133,323,272,168,295,273,249,233,316,327,2,3,24,25,18,65])). % 117.25/117.21 cnf(340,plain, % 117.25/117.21 (E(f2(f3(a12,a12),f3(f3(a12,a12),f3(a12,a12))),f3(a12,a12))), % 117.25/117.21 inference(scs_inference,[],[133,323,272,168,295,273,249,233,316,327,2,3,24,25,18,65,118])). % 117.25/117.21 cnf(342,plain, % 117.25/117.21 (P1(f3(f3(a12,a12),f3(a12,a12)))), % 117.25/117.21 inference(scs_inference,[],[133,323,272,168,295,273,249,233,316,327,2,3,24,25,18,65,118,112])). % 117.25/117.21 cnf(354,plain, % 117.25/117.21 (P5(f3(a1,a1),f2(a1,f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[195,148,295,283,318,2,3,24])). % 117.25/117.21 cnf(355,plain, % 117.25/117.21 (P5(f2(a10,f3(a10,a10)),a10)), % 117.25/117.21 inference(scs_inference,[],[195,192,148,295,283,318,277,2,3,24,25])). % 117.25/117.21 cnf(358,plain, % 117.25/117.21 (E(f3(a1,a1),f3(f3(f3(a1,a1),f3(a1,a1)),a1))), % 117.25/117.21 inference(scs_inference,[],[26,133,158,342,195,192,148,295,231,283,318,277,2,3,24,25,65,89])). % 117.25/117.21 cnf(362,plain, % 117.25/117.21 (E(f2(a13,f3(a13,a13)),a13)+~P5(a13,a13)), % 117.25/117.21 inference(scs_inference,[],[26,133,158,342,30,195,192,148,295,231,283,315,318,277,2,3,24,25,65,89,23,18,118])). % 117.25/117.21 cnf(364,plain, % 117.25/117.21 (P3(a12,f4(a12,a12))+~P1(f4(a12,a12))), % 117.25/117.21 inference(scs_inference,[],[26,133,158,29,342,30,195,192,148,295,231,283,315,318,277,2,3,24,25,65,89,23,18,118,110])). % 117.25/117.21 cnf(366,plain, % 117.25/117.21 (P5(a13,a13)), % 117.25/117.21 inference(scs_inference,[],[26,133,158,29,342,30,195,192,148,295,231,283,315,318,277,2,3,24,25,65,89,23,18,118,110,58])). % 117.25/117.21 cnf(369,plain, % 117.25/117.21 (E(f2(a13,f3(a13,a13)),a13)), % 117.25/117.21 inference(scs_inference,[],[366,362])). % 117.25/117.21 cnf(370,plain, % 117.25/117.21 (E(f3(a1,f3(a1,a1)),f2(a1,f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[317,366,362,2])). % 117.25/117.21 cnf(371,plain, % 117.25/117.21 (~E(a11,f2(a13,f3(a13,a13)))), % 117.25/117.21 inference(scs_inference,[],[317,131,366,362,2,3])). % 117.25/117.21 cnf(372,plain, % 117.25/117.21 (P5(a11,f2(a11,f3(a11,a11)))), % 117.25/117.21 inference(scs_inference,[],[201,317,131,321,366,362,2,3,24])). % 117.25/117.21 cnf(373,plain, % 117.25/117.21 (P5(a14,f2(a11,f3(a11,a11)))), % 117.25/117.21 inference(scs_inference,[],[201,317,294,131,321,366,35,362,2,3,24,25])). % 117.25/117.21 cnf(374,plain, % 117.25/117.21 (P5(f3(a1,f3(a1,a1)),f3(a1,f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[198,201,317,294,131,321,366,35,362,2,3,24,25,65])). % 117.25/117.21 cnf(376,plain, % 117.25/117.21 (P1(f3(a13,a13))), % 117.25/117.21 inference(scs_inference,[],[198,30,201,317,294,131,321,366,35,362,2,3,24,25,65,112])). % 117.25/117.21 cnf(378,plain, % 117.25/117.21 (~P5(f2(a11,f3(a11,a11)),a13)), % 117.25/117.21 inference(scs_inference,[],[28,298,198,30,201,317,294,131,137,321,366,35,362,2,3,24,25,65,112,87])). % 117.25/117.21 cnf(386,plain, % 117.25/117.21 (P5(f3(a13,a13),f3(a13,a13))), % 117.25/117.21 inference(scs_inference,[],[28,323,298,198,30,201,317,294,340,131,137,321,366,124,35,362,2,3,24,25,65,112,87,23,18,118,110,58])). % 117.25/117.21 cnf(390,plain, % 117.25/117.21 (E(f3(f3(a1,a1),f3(a1,a1)),f2(a1,f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[176,305,370,2,3])). % 117.25/117.21 cnf(391,plain, % 117.25/117.21 (P5(f2(f3(a10,a10),f3(f3(a10,a10),f3(a10,a10))),f3(a10,a10))), % 117.25/117.21 inference(scs_inference,[],[176,305,316,370,233,2,3,24])). % 117.25/117.21 cnf(392,plain, % 117.25/117.21 (~E(f2(a11,f3(a11,a11)),a13)), % 117.25/117.21 inference(scs_inference,[],[176,305,316,370,372,233,137,2,3,24,25])). % 117.25/117.21 cnf(394,plain, % 117.25/117.21 (E(f2(f3(a13,a13),f3(f3(a13,a13),f3(a13,a13))),f3(a13,a13))), % 117.25/117.21 inference(scs_inference,[],[376,176,305,316,370,386,372,233,137,149,2,3,24,25,23,118])). % 117.25/117.21 cnf(396,plain, % 117.25/117.21 (P1(f3(f3(a13,a13),f3(a13,a13)))), % 117.25/117.21 inference(scs_inference,[],[376,176,305,316,370,386,372,233,137,149,2,3,24,25,23,118,112])). % 117.25/117.21 cnf(398,plain, % 117.25/117.21 (P1(f2(f3(a13,a13),f3(f3(a13,a13),f3(a13,a13))))), % 117.25/117.21 inference(scs_inference,[],[30,376,176,305,316,370,386,372,233,137,149,366,2,3,24,25,23,118,112,75])). % 117.25/117.21 cnf(404,plain, % 117.25/117.21 (P1(f7(a1,a1))), % 117.25/117.21 inference(scs_inference,[],[26,52,77])). % 117.25/117.21 cnf(406,plain, % 117.25/117.21 (~E(f2(a11,f3(a11,a11)),f2(a13,f3(a13,a13)))), % 117.25/117.21 inference(scs_inference,[],[340,369,392,2,3])). % 117.25/117.21 cnf(409,plain, % 117.25/117.21 (P5(f7(a1,a1),f7(a1,a1))), % 117.25/117.21 inference(scs_inference,[],[404,340,369,338,392,2,3,24,25,65])). % 117.25/117.21 cnf(411,plain, % 117.25/117.21 (E(f2(f7(a1,a1),f3(f7(a1,a1),f7(a1,a1))),f7(a1,a1))), % 117.25/117.21 inference(scs_inference,[],[404,340,369,338,392,2,3,24,25,65,118])). % 117.25/117.21 cnf(416,plain, % 117.25/117.21 (P3(a13,f4(a13,a13))+~P1(f4(a13,a13))), % 117.25/117.21 inference(scs_inference,[],[30,404,340,333,369,338,392,2,3,24,25,65,118,112,23,110])). % 117.25/117.21 cnf(423,plain, % 117.25/117.21 (E(a12,f2(a12,f3(a12,a12)))), % 117.25/117.21 inference(scs_inference,[],[315,2])). % 117.25/117.21 cnf(424,plain, % 117.25/117.21 (P5(a10,f2(a10,f3(a10,a10)))), % 117.25/117.21 inference(scs_inference,[],[192,315,277,2,24])). % 117.25/117.21 cnf(426,plain, % 117.25/117.21 (P1(f2(a12,f3(a12,a12)))), % 117.25/117.21 inference(scs_inference,[],[29,192,315,333,277,269,2,24,25,18])). % 117.25/117.21 cnf(427,plain, % 117.25/117.21 (P5(f2(a12,f3(a12,a12)),f2(a12,f3(a12,a12)))), % 117.25/117.21 inference(scs_inference,[],[29,192,315,333,277,269,2,24,25,18,65])). % 117.25/117.21 cnf(429,plain, % 117.25/117.21 (E(x4291,f3(a13,a13))+~E(x4291,f2(f3(a13,a13),f3(f3(a13,a13),f3(a13,a13))))), % 117.25/117.21 inference(scs_inference,[],[29,192,315,333,394,277,269,2,24,25,18,65,3])). % 117.25/117.21 cnf(437,plain, % 117.25/117.21 (P5(a12,f2(a12,f3(a12,a12)))), % 117.25/117.21 inference(scs_inference,[],[315,327,427,2,24])). % 117.25/117.21 cnf(439,plain, % 117.25/117.21 (~P2(f3(f3(a1,f3(a1,a1)),a1))), % 117.25/117.21 inference(scs_inference,[],[315,327,427,149,2,24,25,23])). % 117.25/117.21 cnf(448,plain, % 117.25/117.21 (P5(f2(f3(a13,a13),f3(f3(a13,a13),f3(a13,a13))),f3(a13,a13))), % 117.25/117.21 inference(scs_inference,[],[394,386,2,24])). % 117.25/117.21 cnf(450,plain, % 117.25/117.21 (E(x4501,a14)+~E(x4501,f3(a11,a13))), % 117.25/117.21 inference(scs_inference,[],[394,33,386,2,24,25,3])). % 117.25/117.21 cnf(478,plain, % 117.25/117.21 (P3(a11,a13)+~E(a13,f2(f4(a13,a12),f4(a14,a12)))), % 117.25/117.21 inference(scs_inference,[],[28,29,30,36,358,333,37,269,366,149,2,24,23,3,21,25,18,65,118,112,72])). % 117.25/117.21 cnf(484,plain, % 117.25/117.21 (E(a13,f2(a13,f3(a13,a13)))), % 117.25/117.21 inference(scs_inference,[],[369,2])). % 117.25/117.21 cnf(485,plain, % 117.25/117.21 (P3(f2(a13,f3(a13,a13)),f4(a11,a12))), % 117.25/117.21 inference(scs_inference,[],[36,369,2,21])). % 117.25/117.21 cnf(486,plain, % 117.25/117.21 (P5(f2(a13,f3(a13,a13)),a11)), % 117.25/117.21 inference(scs_inference,[],[36,34,369,2,21,24])). % 117.25/117.21 cnf(487,plain, % 117.25/117.21 (P5(a13,f2(a13,f3(a13,a13)))), % 117.25/117.21 inference(scs_inference,[],[36,34,369,366,2,21,24,25])). % 117.25/117.21 cnf(488,plain, % 117.25/117.21 (P2(f2(a13,f3(a13,a13)))), % 117.25/117.21 inference(scs_inference,[],[36,34,369,31,366,2,21,24,25,23])). % 117.25/117.21 cnf(489,plain, % 117.25/117.21 (P1(f2(a13,f3(a13,a13)))), % 117.25/117.21 inference(scs_inference,[],[30,36,34,369,31,366,2,21,24,25,23,18])). % 117.25/117.21 cnf(490,plain, % 117.25/117.21 (P5(f2(a13,f3(a13,a13)),f2(a13,f3(a13,a13)))), % 117.25/117.21 inference(scs_inference,[],[30,36,34,369,31,366,2,21,24,25,23,18,65])). % 117.25/117.21 cnf(492,plain, % 117.25/117.21 (~P5(a11,f2(a13,f3(a13,a13)))), % 117.25/117.21 inference(scs_inference,[],[28,30,36,34,369,371,31,366,2,21,24,25,23,18,65,74])). % 117.25/117.21 cnf(497,plain, % 117.25/117.21 (P5(f3(a10,a10),f2(f3(a10,a10),f3(a10,a10)))+~P1(f2(f3(a10,a10),f3(a10,a10)))), % 117.25/117.21 inference(scs_inference,[],[28,222,30,376,36,34,369,371,31,366,2,21,24,25,23,18,65,74,22,110,111])). % 117.25/117.21 cnf(499,plain, % 117.25/117.21 (E(f3(a10,a10),f3(f2(f3(a10,a10),f3(a10,a10)),f3(a10,a10)))+~P1(f2(f3(a10,a10),f3(a10,a10)))), % 117.25/117.21 inference(scs_inference,[],[28,222,29,30,376,36,34,369,38,371,31,366,2,21,24,25,23,18,65,74,22,110,111,72,120])). % 117.25/117.21 cnf(502,plain, % 117.25/117.21 (E(f7(a1,a1),f2(f7(a1,a1),f3(f7(a1,a1),f7(a1,a1))))), % 117.25/117.21 inference(scs_inference,[],[411,2])). % 117.25/117.21 cnf(506,plain, % 117.25/117.21 (~P5(f2(a11,f3(a11,a11)),f2(a13,f3(a13,a13)))), % 117.25/117.21 inference(scs_inference,[],[404,298,489,411,297,406,409,484,2,24,25,18,74])). % 117.25/117.21 cnf(511,plain, % 117.25/117.21 (P5(f3(a11,a11),f2(f3(a11,a11),f3(a11,a11)))+~P1(f2(f3(a11,a11),f3(a11,a11)))), % 117.25/117.21 inference(scs_inference,[],[203,404,298,489,394,411,297,406,409,484,2,24,25,18,74,23,110,111])). % 117.25/117.21 cnf(516,plain, % 117.25/117.21 (E(a11,f2(a13,a14))), % 117.25/117.21 inference(scs_inference,[],[32,2])). % 117.25/117.21 cnf(517,plain, % 117.25/117.21 (~E(f2(a13,f3(a13,a13)),f2(a11,f3(a11,a11)))), % 117.25/117.21 inference(scs_inference,[],[32,506,490,2,24])). % 117.25/117.21 cnf(518,plain, % 117.25/117.21 (P5(f2(a13,f3(a13,a13)),a13)), % 117.25/117.21 inference(scs_inference,[],[369,32,506,490,2,24,25])). % 117.25/117.21 cnf(519,plain, % 117.25/117.21 (P1(f2(a13,a14))), % 117.25/117.21 inference(scs_inference,[],[28,369,32,506,490,2,24,25,18])). % 117.25/117.21 cnf(520,plain, % 117.25/117.21 (P5(f2(a13,a14),f2(a13,a14))), % 117.25/117.21 inference(scs_inference,[],[28,369,32,506,490,2,24,25,18,65])). % 117.25/117.21 cnf(522,plain, % 117.25/117.21 (E(f2(f2(a13,a14),f3(f2(a13,a14),f2(a13,a14))),f2(a13,a14))), % 117.25/117.21 inference(scs_inference,[],[28,369,32,506,490,2,24,25,18,65,118])). % 117.25/117.21 cnf(524,plain, % 117.25/117.21 (P1(f3(f2(a13,a14),f2(a13,a14)))), % 117.25/117.21 inference(scs_inference,[],[28,369,32,506,490,2,24,25,18,65,118,112])). % 117.25/117.21 cnf(528,plain, % 117.25/117.21 (~E(a13,f2(a11,f3(a11,a11)))), % 117.25/117.21 inference(scs_inference,[],[28,30,298,369,297,32,506,490,2,24,25,18,65,118,112,83,6])). % 117.25/117.21 cnf(529,plain, % 117.25/117.21 (P5(a13,f2(a13,a14))), % 117.25/117.21 inference(scs_inference,[],[28,30,298,369,297,32,506,490,2,24,25,18,65,118,112,83,6,144])). % 117.25/117.21 cnf(536,plain, % 117.25/117.21 (P5(a12,f2(a12,a12))+~P1(f2(a12,a12))), % 117.25/117.21 inference(scs_inference,[],[28,29,30,298,369,411,297,32,506,490,126,2,24,25,18,65,118,112,83,6,144,3,23,110,58,111])). % 117.25/117.21 cnf(539,plain, % 117.25/117.21 (E(a14,f3(a11,a13))), % 117.25/117.21 inference(scs_inference,[],[33,2])). % 117.25/117.21 cnf(541,plain, % 117.25/117.21 (P5(f2(a13,a14),a11)), % 117.25/117.21 inference(scs_inference,[],[32,33,373,520,2,24,25])). % 117.25/117.21 cnf(542,plain, % 117.25/117.21 (P1(a14)), % 117.25/117.21 inference(scs_inference,[],[28,30,34,32,33,373,520,2,24,25,75])). % 117.25/117.21 cnf(556,plain, % 117.25/117.21 (E(f4(a11,a12),f2(f4(a13,a12),f4(a14,a12)))), % 117.25/117.21 inference(scs_inference,[],[37,2])). % 117.25/117.21 cnf(558,plain, % 117.25/117.21 (~E(f2(a13,f3(a13,a13)),a11)), % 117.25/117.21 inference(scs_inference,[],[485,294,37,517,2,22,3])). % 117.25/117.21 cnf(559,plain, % 117.25/117.21 (P3(a13,f2(f4(a13,a12),f4(a14,a12)))), % 117.25/117.21 inference(scs_inference,[],[485,294,369,37,517,2,22,3,21])). % 117.25/117.21 cnf(560,plain, % 117.25/117.21 (~E(a13,a11)), % 117.25/117.21 inference(scs_inference,[],[485,294,369,37,487,517,492,2,22,3,21,24])). % 117.25/117.21 cnf(561,plain, % 117.25/117.21 (P5(f2(a13,a14),f2(a11,f3(a11,a11)))), % 117.25/117.21 inference(scs_inference,[],[485,294,369,37,487,517,492,541,2,22,3,21,24,25])). % 117.25/117.21 cnf(562,plain, % 117.25/117.21 (P1(f3(a11,a13))), % 117.25/117.21 inference(scs_inference,[],[485,542,294,369,37,487,517,492,539,541,2,22,3,21,24,25,18])). % 117.25/117.21 cnf(563,plain, % 117.25/117.21 (P5(a14,a14)), % 117.25/117.21 inference(scs_inference,[],[485,542,294,369,37,487,517,492,539,541,2,22,3,21,24,25,18,65])). % 117.25/117.21 cnf(565,plain, % 117.25/117.21 (E(f2(a14,f3(a14,a14)),a14)), % 117.25/117.21 inference(scs_inference,[],[485,542,294,369,37,487,517,492,539,541,2,22,3,21,24,25,18,65,118])). % 117.25/117.21 cnf(567,plain, % 117.25/117.21 (P1(f3(a14,a14))), % 117.25/117.21 inference(scs_inference,[],[485,542,294,369,37,487,517,492,539,541,2,22,3,21,24,25,18,65,118,112])). % 117.25/117.21 cnf(569,plain, % 117.25/117.21 (~E(f3(a13,a13),f3(a11,a13))), % 117.25/117.21 inference(scs_inference,[],[485,28,30,542,294,369,34,37,487,517,492,539,541,2,22,3,21,24,25,18,65,118,112,83])). % 117.25/117.21 cnf(572,plain, % 117.25/117.21 (P3(a14,f4(a14,a14))+~P1(f4(a14,a14))), % 117.25/117.21 inference(scs_inference,[],[485,28,30,542,294,369,34,32,37,487,517,492,539,541,2,22,3,21,24,25,18,65,118,112,83,23,110])). % 117.25/117.21 cnf(574,plain, % 117.25/117.21 (P5(f3(a11,a13),f3(a11,a13))), % 117.25/117.21 inference(scs_inference,[],[485,28,30,542,294,369,34,32,37,487,517,492,539,541,2,22,3,21,24,25,18,65,118,112,83,23,110,58])). % 117.25/117.21 cnf(579,plain, % 117.25/117.21 (E(f2(a13,a14),f2(f2(a13,a14),f3(f2(a13,a14),f2(a13,a14))))), % 117.25/117.21 inference(scs_inference,[],[522,2])). % 117.25/117.21 cnf(581,plain, % 117.25/117.21 (~E(a13,f2(a13,a14))), % 117.25/117.21 inference(scs_inference,[],[41,559,32,522,560,2,22,3])). % 117.25/117.21 cnf(582,plain, % 117.25/117.21 (P5(a14,f3(a11,a13))), % 117.25/117.21 inference(scs_inference,[],[41,559,32,33,522,574,560,2,22,3,24])). % 117.25/117.21 cnf(583,plain, % 117.25/117.21 (P5(f3(a11,a13),a14)), % 117.25/117.21 inference(scs_inference,[],[41,559,32,33,522,574,560,2,22,3,24,25])). % 117.25/117.21 cnf(584,plain, % 117.25/117.21 (P1(f2(f2(a13,a14),f3(f2(a13,a14),f2(a13,a14))))), % 117.25/117.21 inference(scs_inference,[],[41,559,519,32,33,522,574,560,2,22,3,24,25,18])). % 117.25/117.21 cnf(585,plain, % 117.25/117.21 (P5(f3(a14,a14),f3(a14,a14))), % 117.25/117.21 inference(scs_inference,[],[41,559,519,567,32,33,522,574,560,2,22,3,24,25,18,65])). % 117.25/117.21 cnf(587,plain, % 117.25/117.21 (E(f2(f3(a11,a13),f3(f3(a11,a13),f3(a11,a13))),f3(a11,a13))), % 117.25/117.21 inference(scs_inference,[],[41,559,519,562,567,32,33,522,574,560,2,22,3,24,25,18,65,118])). % 117.25/117.21 cnf(589,plain, % 117.25/117.21 (P1(f3(f3(a11,a13),f3(a11,a13)))), % 117.25/117.21 inference(scs_inference,[],[41,559,519,562,567,32,33,522,574,560,2,22,3,24,25,18,65,118,112])). % 117.25/117.21 cnf(591,plain, % 117.25/117.21 (P5(a13,f2(f2(a13,a14),f3(f2(a13,a14),f2(a13,a14))))), % 117.25/117.21 inference(scs_inference,[],[41,559,30,519,542,562,567,32,33,522,574,560,2,22,3,24,25,18,65,118,112,73])). % 117.25/117.21 cnf(593,plain, % 117.25/117.21 (P1(f2(f3(a11,a13),f3(f3(a11,a13),f3(a11,a13))))), % 117.25/117.21 inference(scs_inference,[],[41,559,28,30,519,542,562,567,32,34,33,522,574,560,2,22,3,24,25,18,65,118,112,73,75])). % 117.25/117.21 cnf(600,plain, % 117.25/117.21 (P5(a13,f2(a13,a13))+~P1(f2(a13,a13))), % 117.25/117.21 inference(scs_inference,[],[41,559,28,30,519,542,562,567,32,34,33,522,574,560,2,22,3,24,25,18,65,118,112,73,75,23,110,58,111])). % 117.25/117.21 cnf(603,plain, % 117.25/117.21 (E(f3(a11,a13),f2(f3(a11,a13),f3(f3(a11,a13),f3(a11,a13))))), % 117.25/117.21 inference(scs_inference,[],[587,2])). % 117.25/117.21 cnf(605,plain, % 117.25/117.21 (P5(f2(a13,f3(a13,a13)),f2(a13,a14))), % 117.25/117.21 inference(scs_inference,[],[32,484,558,587,529,2,3,24])). % 117.25/117.21 cnf(606,plain, % 117.25/117.21 (E(f2(f3(a14,a14),f3(f3(a14,a14),f3(a14,a14))),f3(a14,a14))), % 117.25/117.21 inference(scs_inference,[],[567,32,484,558,587,529,585,2,3,24,118])). % 117.25/117.21 cnf(614,plain, % 117.25/117.21 (~E(f3(a13,a13),a14)), % 117.25/117.21 inference(scs_inference,[],[30,519,542,567,32,484,558,563,587,529,585,2,3,24,118,112,83,75,5])). % 117.25/117.21 cnf(622,plain, % 117.25/117.21 (P5(f3(a13,a13),f2(f3(a13,a13),f3(a13,a13)))+~P1(f2(f3(a13,a13),f3(a13,a13)))), % 117.25/117.21 inference(scs_inference,[],[30,376,519,542,567,32,484,37,558,556,299,563,587,529,585,2,3,24,118,112,83,75,5,25,65,18,23,110,111])). % 117.25/117.21 cnf(628,plain, % 117.25/117.21 (~E(a13,f2(f2(a13,a14),f3(f2(a13,a14),f2(a13,a14))))), % 117.25/117.21 inference(scs_inference,[],[522,565,581,2,3])). % 117.25/117.21 cnf(630,plain, % 117.25/117.21 (P1(f2(a14,f3(a14,a14)))), % 117.25/117.21 inference(scs_inference,[],[542,522,502,565,581,409,2,3,24,18])). % 117.25/117.21 cnf(631,plain, % 117.25/117.21 (P5(f2(a14,f3(a14,a14)),f2(a14,f3(a14,a14)))), % 117.25/117.21 inference(scs_inference,[],[542,522,502,565,581,409,2,3,24,18,65])). % 117.25/117.21 cnf(633,plain, % 117.25/117.21 (P5(f2(a14,f3(a14,a14)),a11)), % 117.25/117.21 inference(scs_inference,[],[542,522,502,565,581,409,2,3,24,18,65,180])). % 117.25/117.21 cnf(640,plain, % 117.25/117.21 (E(f3(a14,a14),f2(f3(a14,a14),f3(f3(a14,a14),f3(a14,a14))))), % 117.25/117.21 inference(scs_inference,[],[606,2])). % 117.25/117.21 cnf(642,plain, % 117.25/117.21 (P5(a14,f2(a14,f3(a14,a14)))), % 117.25/117.21 inference(scs_inference,[],[587,569,565,606,631,2,3,24])). % 117.25/117.21 cnf(643,plain, % 117.25/117.21 (P5(f2(a14,f3(a14,a14)),a14)), % 117.25/117.21 inference(scs_inference,[],[587,569,565,606,631,2,3,24,25])). % 117.25/117.21 cnf(645,plain, % 117.25/117.21 (P5(f2(a13,a14),f2(f2(a13,a14),f2(a13,a14)))+~P1(f2(f2(a13,a14),f2(a13,a14)))), % 117.25/117.21 inference(scs_inference,[],[519,522,587,569,565,606,631,2,3,24,25,23,111])). % 117.25/117.21 cnf(648,plain, % 117.25/117.21 (~E(f3(a13,a13),f2(a14,f3(a14,a14)))), % 117.25/117.21 inference(scs_inference,[],[565,614,3])). % 117.25/117.21 cnf(649,plain, % 117.25/117.21 (P5(f3(a11,a13),f2(a14,f3(a14,a14)))), % 117.25/117.21 inference(scs_inference,[],[539,565,614,642,3,24])). % 117.25/117.21 cnf(650,plain, % 117.25/117.21 (P5(f2(a14,f3(a14,a14)),f2(a11,f3(a11,a11)))), % 117.25/117.21 inference(scs_inference,[],[294,539,565,614,633,642,3,24,25])). % 117.25/117.21 cnf(657,plain, % 117.25/117.21 (P5(a11,f2(a13,a14))), % 117.25/117.21 inference(scs_inference,[],[32,520,24])). % 117.25/117.21 cnf(661,plain, % 117.25/117.21 (~P5(f2(a13,a14),f2(a13,f3(a13,a13)))), % 117.25/117.21 inference(scs_inference,[],[28,519,562,489,630,32,539,643,649,520,492,24,25,74,87])). % 117.25/117.21 cnf(663,plain, % 117.25/117.21 (E(f3(a14,a14),f3(f3(a11,a13),a14))), % 117.25/117.21 inference(scs_inference,[],[28,519,542,562,567,489,630,32,539,582,643,649,520,492,24,25,74,87,89])). % 117.25/117.21 cnf(668,plain, % 117.25/117.21 (P5(f3(f3(a11,a13),a14),f3(f3(a11,a13),a14))), % 117.25/117.21 inference(scs_inference,[],[28,519,542,562,567,489,630,32,539,587,582,643,649,520,492,24,25,74,87,89,2,18,23,65])). % 117.25/117.21 cnf(670,plain, % 117.25/117.21 (P5(a14,f2(a14,a14))+~P1(f2(a14,a14))), % 117.25/117.21 inference(scs_inference,[],[28,519,542,562,567,489,630,32,539,587,582,643,649,520,492,24,25,74,87,89,2,18,23,65,111])). % 117.25/117.21 cnf(672,plain, % 117.25/117.21 (E(a14,f3(f2(a14,a14),a14))+~P1(f2(a14,a14))), % 117.25/117.21 inference(scs_inference,[],[28,519,542,562,567,489,630,32,539,587,37,582,643,649,520,492,24,25,74,87,89,2,18,23,65,111,73,120])). % 117.25/117.21 cnf(677,plain, % 117.25/117.21 (~P5(f2(a13,a14),a13)), % 117.25/117.21 inference(scs_inference,[],[28,30,519,668,663,657,137,2,24,25,87])). % 117.25/117.21 cnf(683,plain, % 117.25/117.21 (P5(f2(a11,f3(a11,a11)),f2(a13,a14))), % 117.25/117.21 inference(scs_inference,[],[294,657,24])). % 117.25/117.21 cnf(684,plain, % 117.25/117.21 (~E(f2(a13,a14),f2(a13,f3(a13,a13)))), % 117.25/117.21 inference(scs_inference,[],[294,657,492,24,25])). % 117.25/117.21 cnf(689,plain, % 117.25/117.21 (E(f3(a11,a11),f3(f2(a13,a14),a11))), % 117.25/117.21 inference(scs_inference,[],[28,203,30,519,298,489,294,487,657,561,492,24,25,83,74,89])). % 117.25/117.21 cnf(692,plain, % 117.25/117.21 (E(f2(a13,a14),f2(a11,f3(a11,a11)))), % 117.25/117.21 inference(scs_inference,[],[28,203,30,519,298,489,294,487,657,561,492,24,25,83,74,89,5,2])). % 117.25/117.21 cnf(694,plain, % 117.25/117.21 (P1(f3(f2(a13,a14),a11))), % 117.25/117.21 inference(scs_inference,[],[28,203,30,519,298,489,394,294,487,657,561,492,24,25,83,74,89,5,2,3,18])). % 117.25/117.21 cnf(696,plain, % 117.25/117.21 (P5(f3(f2(a13,a14),a11),f3(f2(a13,a14),a11))), % 117.25/117.21 inference(scs_inference,[],[28,203,30,519,298,489,394,294,606,487,657,561,492,24,25,83,74,89,5,2,3,18,23,65])). % 117.25/117.21 cnf(698,plain, % 117.25/117.21 (~P5(a14,f3(a13,a13))), % 117.25/117.21 inference(scs_inference,[],[28,203,30,376,519,542,298,489,394,294,606,487,657,561,661,492,24,25,83,74,89,5,2,3,18,23,65,98])). % 117.25/117.21 cnf(700,plain, % 117.25/117.21 (~P5(f3(a11,a13),f3(a13,a13))), % 117.25/117.21 inference(scs_inference,[],[28,203,30,376,519,542,562,298,489,394,294,606,487,582,657,561,661,492,24,25,83,74,89,5,2,3,18,23,65,98,87])). % 117.25/117.21 cnf(702,plain, % 117.25/117.21 (P5(f3(a11,a13),f2(f3(a11,a13),f3(a11,a13)))+~P1(f2(f3(a11,a13),f3(a11,a13)))), % 117.25/117.21 inference(scs_inference,[],[28,203,30,376,519,542,562,298,489,394,294,606,487,582,657,561,661,492,24,25,83,74,89,5,2,3,18,23,65,98,87,111])). % 117.25/117.21 cnf(704,plain, % 117.25/117.21 (E(f3(a11,a13),f3(f2(f3(a11,a13),f3(a11,a13)),f3(a11,a13)))+~P1(f2(f3(a11,a13),f3(a11,a13)))), % 117.25/117.21 inference(scs_inference,[],[28,203,30,376,519,542,562,298,489,394,294,37,606,487,582,657,561,661,492,24,25,83,74,89,5,2,3,18,23,65,98,87,111,73,120])). % 117.25/117.21 cnf(706,plain, % 117.25/117.21 (E(f3(f2(a13,a14),a11),f3(a11,a11))), % 117.25/117.21 inference(scs_inference,[],[689,2])). % 117.25/117.21 cnf(708,plain, % 117.25/117.21 (~E(f3(a11,a13),f3(a13,a13))), % 117.25/117.21 inference(scs_inference,[],[448,582,700,689,698,2,24,25])). % 117.25/117.21 cnf(709,plain, % 117.25/117.21 (~P5(f2(a14,f3(a14,a14)),f3(a13,a13))), % 117.25/117.21 inference(scs_inference,[],[376,542,630,448,582,642,700,689,698,2,24,25,87])). % 117.25/117.21 cnf(711,plain, % 117.25/117.21 (E(a14,f3(f2(a11,f3(a11,a11)),a13))), % 117.25/117.21 inference(scs_inference,[],[30,376,542,298,630,297,448,582,642,700,689,692,698,2,24,25,87,89])). % 117.25/117.21 cnf(714,plain, % 117.25/117.21 (P1(f3(f2(a11,f3(a11,a11)),a13))), % 117.25/117.21 inference(scs_inference,[],[30,376,542,298,630,297,448,582,642,700,689,692,698,2,24,25,87,89,180,18])). % 117.25/117.21 cnf(718,plain, % 117.25/117.21 (E(f3(a14,a14),f3(f2(f3(a14,a14),f3(a14,a14)),f3(a14,a14)))+~P1(f2(f3(a14,a14),f3(a14,a14)))), % 117.25/117.21 inference(scs_inference,[],[30,376,542,567,298,630,37,297,556,448,582,642,700,689,692,698,2,24,25,87,89,180,18,23,111,73,120])). % 117.25/117.21 cnf(720,plain, % 117.25/117.21 (E(f3(f2(a11,f3(a11,a11)),a13),a14)), % 117.25/117.21 inference(scs_inference,[],[711,2])). % 117.25/117.21 cnf(724,plain, % 117.25/117.21 (~P5(f2(a11,f3(a11,a11)),f3(a13,a13))), % 117.25/117.21 inference(scs_inference,[],[376,542,298,394,642,373,708,706,696,711,698,2,3,24,25,87])). % 117.25/117.21 cnf(729,plain, % 117.25/117.21 (~E(f2(a13,a14),a13)), % 117.25/117.21 inference(scs_inference,[],[484,684,3])). % 117.25/117.21 cnf(730,plain, % 117.25/117.21 (~E(f3(a13,a13),f2(a11,f3(a11,a11)))), % 117.25/117.21 inference(scs_inference,[],[484,684,724,386,3,24])). % 117.25/117.21 cnf(731,plain, % 117.25/117.21 (~E(a11,f3(a13,a13))), % 117.25/117.21 inference(scs_inference,[],[484,684,35,724,386,698,3,24,25])). % 117.25/117.21 cnf(732,plain, % 117.25/117.21 (~P5(a11,f3(a13,a13))), % 117.25/117.21 inference(scs_inference,[],[28,376,542,484,684,35,724,386,698,3,24,25,87])). % 117.25/117.21 cnf(738,plain, % 117.25/117.21 (~P5(f2(a13,a14),f3(a13,a13))), % 117.25/117.21 inference(scs_inference,[],[28,376,519,372,657,732,25,87])). % 117.25/117.21 cnf(745,plain, % 117.25/117.21 (~E(f2(a13,a14),f3(a13,a13))), % 117.25/117.21 inference(scs_inference,[],[657,732,25])). % 117.25/117.21 cnf(751,plain, % 117.25/117.21 (P5(f3(f2(a13,a14),a11),f3(a11,a11))), % 117.25/117.21 inference(scs_inference,[],[706,696,25])). % 117.25/117.21 cnf(1112,plain, % 117.25/117.21 (~P3(a1,a13)+E(a1,a13)), % 117.25/117.21 inference(scs_inference,[],[26,30,39,31,68])). % 117.25/117.21 cnf(1133,plain, % 117.25/117.21 (~P3(f2(f3(a1,a1),f3(f3(a1,a1),f3(a1,a1))),a13)+E(a1,a13)), % 117.25/117.21 inference(scs_inference,[],[170,1112,21])). % 117.25/117.21 cnf(1142,plain, % 117.25/117.21 (P5(f3(a1,f3(a1,a1)),f3(f3(a1,a1),a1))), % 117.25/117.21 inference(scs_inference,[],[209,218,25])). % 117.25/117.21 cnf(1143,plain, % 117.25/117.21 (P5(f3(f3(a1,a1),a1),f3(a1,f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[209,218,255,25,24])). % 117.25/117.21 cnf(1147,plain, % 117.25/117.21 (E(f3(f3(a1,a1),f3(a1,a1)),f3(f3(a1,a1),a1))), % 117.25/117.21 inference(scs_inference,[],[219,198,209,176,218,255,25,24,74,2,3])). % 117.25/117.21 cnf(1151,plain, % 117.25/117.21 (P5(f3(f3(a1,a1),f3(a1,a1)),f3(f3(a1,a1),a1))), % 117.25/117.21 inference(scs_inference,[],[209,232,1147,2,25])). % 117.25/117.21 cnf(1152,plain, % 117.25/117.21 (P5(f3(f3(a1,a1),a1),f3(f3(a1,a1),f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[209,232,275,1147,2,25,24])). % 117.25/117.21 cnf(1155,plain, % 117.25/117.21 (P5(f2(a1,f3(a1,a1)),f3(f3(a1,a1),a1))), % 117.25/117.21 inference(scs_inference,[],[209,319,25])). % 117.25/117.21 cnf(1156,plain, % 117.25/117.21 (P5(f3(f3(a1,a1),a1),f2(a1,f3(a1,a1)))), % 117.25/117.21 inference(scs_inference,[],[209,319,354,25,24])). % 117.25/117.21 cnf(1163,plain, % 117.25/117.21 (E(f4(a1,f2(a1,a1)),a1)), % 117.25/117.21 inference(scs_inference,[],[26,44,66])). % 117.25/117.22 cnf(1164,plain, % 117.25/117.22 (E(a1,f4(a1,f2(a1,a1)))), % 117.25/117.22 inference(scs_inference,[],[1163,2])). % 117.25/117.22 cnf(1165,plain, % 117.25/117.22 (~P2(f4(a1,f2(a1,a1)))), % 117.25/117.22 inference(scs_inference,[],[1163,122,2,23])). % 117.25/117.22 cnf(1166,plain, % 117.25/117.22 (P1(f4(a1,f2(a1,a1)))), % 117.25/117.22 inference(scs_inference,[],[26,1163,122,2,23,18])). % 117.25/117.22 cnf(1169,plain, % 117.25/117.22 (P5(f4(a1,f2(a1,a1)),a1)), % 117.25/117.22 inference(scs_inference,[],[26,1163,122,2,23,18,65,25])). % 117.25/117.22 cnf(1170,plain, % 117.25/117.22 (P5(a1,f4(a1,f2(a1,a1)))), % 117.25/117.22 inference(scs_inference,[],[26,1163,122,2,23,18,65,25,24])). % 117.25/117.22 cnf(1177,plain, % 117.25/117.22 (P5(f4(a1,f2(a1,a1)),f3(a1,a1))), % 117.25/117.22 inference(scs_inference,[],[148,1169,25])). % 117.25/117.22 cnf(1178,plain, % 117.25/117.22 (P5(f3(a1,a1),f4(a1,f2(a1,a1)))), % 117.25/117.22 inference(scs_inference,[],[148,1169,1170,25,24])). % 117.25/117.22 cnf(1186,plain, % 117.25/117.22 (E(f3(f3(a1,a1),a1),f4(a1,f2(a1,a1)))), % 117.25/117.22 inference(scs_inference,[],[219,1166,209,1177,1178,25,24,74])). % 117.25/117.22 cnf(1207,plain, % 117.25/117.22 (E(f4(f4(a1,a1),a1),a1)), % 117.25/117.22 inference(scs_inference,[],[26,45,67])). % 117.25/117.22 cnf(1208,plain, % 117.25/117.22 (E(a1,f4(f4(a1,a1),a1))), % 117.25/117.22 inference(scs_inference,[],[1207,2])). % 117.25/117.22 cnf(1209,plain, % 117.25/117.22 (~P2(f4(f4(a1,a1),a1))), % 117.25/117.22 inference(scs_inference,[],[1207,122,2,23])). % 117.25/117.22 cnf(1210,plain, % 117.25/117.22 (P1(f4(f4(a1,a1),a1))), % 117.25/117.22 inference(scs_inference,[],[26,1207,122,2,23,18])). % 117.25/117.22 cnf(1213,plain, % 117.25/117.22 (P5(f4(f4(a1,a1),a1),a1)), % 117.25/117.22 inference(scs_inference,[],[26,1207,122,2,23,18,65,25])). % 117.25/117.22 cnf(1214,plain, % 117.25/117.22 (P5(a1,f4(f4(a1,a1),a1))), % 117.25/117.22 inference(scs_inference,[],[26,1207,122,2,23,18,65,25,24])). % 117.25/117.22 cnf(1255,plain, % 117.25/117.22 (~P5(a14,f2(f3(a11,a13),f3(f3(a11,a13),f3(a11,a13))))+E(a14,f2(f3(a11,a13),f3(f3(a11,a13),f3(a11,a13))))), % 117.25/117.22 inference(scs_inference,[],[542,593,603,583,539,24,25,74])). % 117.25/117.22 cnf(1261,plain, % 117.25/117.22 (P5(a13,f2(a10,f3(a10,a10)))+~P5(f2(f2(a13,a14),f3(f2(a13,a14),f2(a13,a14))),a10)), % 117.25/117.22 inference(scs_inference,[],[27,30,584,591,640,253,585,24,87,25])). % 117.25/117.22 cnf(1264,plain, % 117.25/117.22 (P5(a13,a10)+~P5(a11,a10)), % 117.25/117.22 inference(scs_inference,[],[27,28,30,34,87])). % 117.25/117.22 cnf(1314,plain, % 117.25/117.22 (P5(f2(a13,f3(a13,a13)),a10)+~P5(a13,a10)), % 117.25/117.22 inference(scs_inference,[],[27,489,30,518,87])). % 117.25/117.22 cnf(1319,plain, % 117.25/117.22 (P5(f2(a13,f3(a13,a13)),a10)+~P5(f2(a13,a14),a10)), % 117.25/117.22 inference(scs_inference,[],[27,489,519,605,87])). % 117.25/117.22 cnf(1619,plain, % 117.25/117.22 (E(f4(a10,f2(a13,f3(a13,a13))),f2(a13,f3(a13,a13)))), % 117.25/117.22 inference(scs_inference,[],[484,30,47,18])). % 117.25/117.22 cnf(1635,plain, % 117.25/117.22 (E(f2(f2(a10,a10),a1),f2(a10,a10))), % 117.25/117.22 inference(scs_inference,[],[27,48,66])). % 117.25/117.22 cnf(1636,plain, % 117.25/117.22 (E(f2(a10,a10),f2(f2(a10,a10),a1))), % 117.25/117.22 inference(scs_inference,[],[1635,2])). % 117.25/117.22 cnf(1637,plain, % 117.25/117.22 (~P1(f2(f2(a10,a10),a1))+P1(f2(a10,a10))), % 117.25/117.22 inference(scs_inference,[],[1635,2,18])). % 117.25/117.22 cnf(1640,plain, % 117.25/117.22 (P1(f3(f2(a10,a10),f2(a10,a10)))+~P1(f2(f2(a10,a10),a1))), % 117.25/117.22 inference(scs_inference,[],[1635,2,18,65,112])). % 117.25/117.22 cnf(1642,plain, % 117.25/117.22 (E(f2(f2(a10,a10),f3(f2(a10,a10),f2(a10,a10))),f2(a10,a10))+~P1(f2(f2(a10,a10),a1))), % 117.25/117.22 inference(scs_inference,[],[1635,2,18,65,112,118])). % 117.25/117.22 cnf(1646,plain, % 117.25/117.22 (E(a10,f3(f2(a10,a10),a10))+~P1(f2(f2(a10,a10),a1))), % 117.25/117.22 inference(scs_inference,[],[27,1635,2,18,65,112,118,111,120])). % 117.25/117.22 cnf(1661,plain, % 117.25/117.22 (~P1(f2(a10,a10))+E(a10,f3(f2(a10,a10),a10))), % 117.25/117.22 inference(scs_inference,[],[27,1636,18,65,73,89,1637,1640,1642,1646])). % 117.25/117.22 cnf(1681,plain, % 117.25/117.22 (E(f3(a1,a1),f3(f4(a1,f2(a1,a1)),a1))), % 117.25/117.22 inference(scs_inference,[],[26,133,1166,305,154,129,1164,1170,24,3,25,89])). % 117.25/117.22 cnf(1684,plain, % 117.25/117.22 (P1(f3(f4(a1,f2(a1,a1)),a1))), % 117.25/117.22 inference(scs_inference,[],[26,133,1166,305,154,129,1164,1170,24,3,25,89,2,18])). % 117.25/117.22 cnf(1690,plain, % 117.25/117.22 (E(f3(f4(a1,f2(a1,a1)),a1),f3(a1,a1))), % 117.25/117.22 inference(scs_inference,[],[1681,2])). % 117.25/117.22 cnf(1692,plain, % 117.25/117.22 (~P2(f3(f4(a1,f2(a1,a1)),a1))), % 117.25/117.22 inference(scs_inference,[],[172,390,1681,149,2,24,23])). % 117.25/117.22 cnf(1695,plain, % 117.25/117.22 (E(f3(a1,a1),f3(f4(f4(a1,a1),a1),a1))), % 117.25/117.22 inference(scs_inference,[],[26,133,1210,172,129,390,1208,1214,1681,149,2,24,23,3,25,89])). % 117.25/117.22 cnf(1697,plain, % 117.25/117.22 (P1(f3(f4(f4(a1,a1),a1),a1))), % 117.25/117.22 inference(scs_inference,[],[26,133,1210,172,129,390,1208,1214,1681,149,2,24,23,3,25,89,18])). % 117.25/117.22 cnf(1707,plain, % 117.25/117.22 (E(f3(f4(f4(a1,a1),a1),a1),f3(a1,a1))), % 117.25/117.22 inference(scs_inference,[],[1695,2])). % 117.25/117.22 cnf(1708,plain, % 117.25/117.22 (~P2(f3(f4(f4(a1,a1),a1),a1))), % 117.25/117.22 inference(scs_inference,[],[1695,149,2,23])). % 117.25/117.22 cnf(1710,plain, % 117.25/117.22 (P5(f3(a1,f3(a1,a1)),f4(a1,f2(a1,a1)))), % 117.25/117.22 inference(scs_inference,[],[374,1186,370,1142,1695,149,2,23,24,25])). % 117.25/117.22 cnf(1715,plain, % 117.25/117.22 (P5(f3(f3(a1,a1),f3(a1,a1)),f4(a1,f2(a1,a1)))), % 117.25/117.22 inference(scs_inference,[],[579,1186,520,1151,24,25])). % 117.25/117.22 cnf(1719,plain, % 117.25/117.22 (P5(f4(a1,f2(a1,a1)),f3(a1,f3(a1,a1)))), % 117.25/117.22 inference(scs_inference,[],[1186,1143,24])). % 117.25/117.22 cnf(1720,plain, % 117.25/117.22 (P5(f2(a1,f3(a1,a1)),f4(a1,f2(a1,a1)))), % 117.25/117.22 inference(scs_inference,[],[1186,1143,1155,24,25])). % 117.25/117.22 cnf(1729,plain, % 117.25/117.22 (P5(f4(a1,f2(a1,a1)),f3(f3(a1,a1),f3(a1,a1)))), % 117.25/117.22 inference(scs_inference,[],[1186,1152,24])). % 117.25/117.22 cnf(1730,plain, % 117.25/117.22 (P5(f4(f4(a1,a1),a1),f4(a1,f2(a1,a1)))), % 117.25/117.22 inference(scs_inference,[],[1164,1186,1152,1213,24,25])). % 117.25/117.22 cnf(1739,plain, % 117.25/117.22 (P5(f4(a1,f2(a1,a1)),f2(a1,f3(a1,a1)))), % 117.25/117.22 inference(scs_inference,[],[1186,1156,24])). % 117.25/117.22 cnf(1740,plain, % 117.25/117.22 (P5(a1,f3(f3(f3(a1,a1),a1),a1))), % 117.25/117.22 inference(scs_inference,[],[305,1186,1156,153,24,25])). % 117.25/117.22 cnf(1744,plain, % 117.25/117.22 (E(f4(f4(a11,a11),a10),f4(a11,a11))), % 117.25/117.22 inference(scs_inference,[],[28,49,67])). % 117.25/117.22 cnf(1745,plain, % 117.25/117.22 (E(f4(a11,a11),f4(f4(a11,a11),a10))), % 117.25/117.22 inference(scs_inference,[],[1744,2])). % 117.25/117.22 cnf(1747,plain, % 117.25/117.22 (E(f4(a1,f2(a1,a1)),f4(f4(a1,a1),a1))), % 117.25/117.22 inference(scs_inference,[],[1166,1210,1164,1214,1744,1730,2,24,74])). % 117.25/117.22 cnf(1753,plain, % 117.25/117.22 (P3(a11,f4(a11,a11))+~P1(f4(f4(a11,a11),a10))), % 117.25/117.22 inference(scs_inference,[],[28,1166,1210,1164,1214,1744,1730,2,24,74,23,18,65,58,110])). % 117.25/117.22 cnf(1758,plain, % 117.25/117.22 (E(f3(f3(f3(a1,a1),a1),a1),a1)), % 117.25/117.22 inference(scs_inference,[],[26,320,305,152,1740,1747,2,24,74])). % 117.25/117.22 cnf(1761,plain, % 117.25/117.22 (~P1(f4(a11,a11))+P1(f4(f4(a11,a11),a10))), % 117.25/117.22 inference(scs_inference,[],[26,320,305,152,1740,1747,1745,2,24,74,23,18])). % 117.25/117.22 cnf(1765,plain, % 117.25/117.22 (E(a1,f3(f3(f3(a1,a1),a1),a1))), % 117.25/117.22 inference(scs_inference,[],[1758,2])). % 117.25/117.22 cnf(1769,plain, % 117.25/117.22 (P3(f4(a11,a11),f4(a11,a11))+~P1(f4(a11,a11))), % 117.25/117.22 inference(scs_inference,[],[27,1745,72])). % 117.25/117.22 cnf(1771,plain, % 117.25/117.22 (P3(f4(a11,a11),f4(f4(a11,a11),a10))+~P1(f4(a11,a11))), % 117.25/117.22 inference(scs_inference,[],[27,1745,72,22])). % 117.25/117.22 cnf(1772,plain, % 117.25/117.22 (P3(f4(f4(a11,a11),a10),f4(a11,a11))+~P1(f4(a11,a11))), % 117.25/117.22 inference(scs_inference,[],[27,1745,72,22,21])). % 117.25/117.22 cnf(1908,plain, % 117.25/117.22 (P5(f2(f3(a13,a13),f3(f3(a13,a13),f3(a13,a13))),a11)+~P5(f3(a13,a13),a11)), % 117.25/117.22 inference(scs_inference,[],[28,376,398,448,87])). % 117.25/117.22 cnf(2230,plain, % 117.25/117.22 (E(f3(a1,f3(a1,a1)),f4(f4(a1,a1),a1))), % 117.25/117.22 inference(scs_inference,[],[1210,198,148,1747,1681,1710,1719,24,3,25,74])). % 117.25/117.22 cnf(2239,plain, % 117.25/117.22 (E(a1,f3(f4(f4(a1,a1),a1),a1))), % 117.25/117.22 inference(scs_inference,[],[148,1747,1695,1729,2230,2,24,3])). % 117.25/117.22 cnf(2240,plain, % 117.25/117.22 (P5(f2(a1,f3(a1,a1)),f4(f4(a1,a1),a1))), % 117.25/117.22 inference(scs_inference,[],[148,1747,1695,1720,1729,2230,2,24,3,25])). % 117.25/117.22 cnf(2245,plain, % 117.25/117.22 (P5(f4(f4(a1,a1),a1),f2(a1,f3(a1,a1)))), % 117.25/117.22 inference(scs_inference,[],[1747,1739,2239,2,24])). % 117.25/117.22 cnf(2247,plain, % 117.25/117.22 (E(a1,f3(f3(a1,f3(a1,a1)),a1))), % 117.25/117.22 inference(scs_inference,[],[148,1747,327,1739,1715,2239,2,24,25,3])). % 117.25/117.22 cnf(2260,plain, % 117.25/117.22 (E(f3(f3(a1,f3(a1,a1)),a1),a1)), % 117.25/117.22 inference(scs_inference,[],[2247,2])). % 117.25/117.22 cnf(2449,plain, % 117.25/117.22 (E(a12,f3(f2(a12,a12),a12))+~P5(a12,f2(a12,a12))+~P1(f2(a12,a12))), % 117.25/117.22 inference(scs_inference,[],[29,222,239,124,391,120])). % 117.25/117.22 cnf(2733,plain, % 117.25/117.22 (P5(a1,f2(f3(a1,a1),f3(f3(a1,a1),f3(a1,a1))))), % 117.25/117.22 inference(scs_inference,[],[127,214,25])). % 117.25/117.22 cnf(2738,plain, % 117.25/117.22 (P5(f3(a1,a1),f2(f3(a1,a1),f3(f3(a1,a1),f3(a1,a1))))), % 117.25/117.22 inference(scs_inference,[],[154,193,25])). % 117.25/117.22 cnf(2803,plain, % 117.25/117.22 (P5(f2(a10,f3(a10,a10)),a13)+~P5(a10,a13)), % 117.25/117.22 inference(scs_inference,[],[30,27,257,355,87])). % 117.25/117.22 cnf(2822,plain, % 117.25/117.22 (E(f2(a1,x28221),f2(f3(f3(a1,a1),a1),x28221))), % 117.25/117.22 inference(scs_inference,[],[334,630,46,47,48,49,44,45,16,17,4])). % 117.25/117.22 cnf(2823,plain, % 117.25/117.22 (E(f3(x28231,a1),f3(x28231,f3(f3(a1,a1),a1)))), % 117.25/117.22 inference(scs_inference,[],[334,630,46,47,48,49,44,45,16,17,4,7])). % 117.25/117.22 cnf(2824,plain, % 117.25/117.22 (E(f4(x28241,a1),f4(x28241,f3(f3(a1,a1),a1)))), % 117.25/117.22 inference(scs_inference,[],[334,630,46,47,48,49,44,45,16,17,4,7,9])). % 117.25/117.22 cnf(2831,plain, % 117.25/117.22 (~E(a11,f2(f3(a13,a13),f3(f3(a13,a13),f3(a13,a13))))), % 117.25/117.22 inference(scs_inference,[],[731,334,630,46,47,48,49,44,45,16,17,4,7,9,10,11,12,13,14,15,429])). % 117.25/117.22 cnf(2832,plain, % 117.25/117.22 (E(f2(f3(a11,a13),f3(f3(a11,a13),f3(a11,a13))),a14)), % 117.25/117.22 inference(scs_inference,[],[731,334,630,587,46,47,48,49,44,45,16,17,4,7,9,10,11,12,13,14,15,429,450])). % 117.25/117.22 cnf(2833,plain, % 117.25/117.22 (E(f4(a1,x28331),f4(f3(f3(a1,a1),a1),x28331))), % 117.25/117.22 inference(scs_inference,[],[731,334,630,587,46,47,48,49,44,45,16,17,4,7,9,10,11,12,13,14,15,429,450,8])). % 117.25/117.22 cnf(2836,plain, % 117.25/117.22 (~E(f3(a13,a13),a11)), % 117.25/117.22 inference(scs_inference,[],[731,334,630,587,46,47,48,49,44,45,16,17,4,7,9,10,11,12,13,14,15,429,450,8,6,5,2])). % 117.25/117.22 cnf(2842,plain, % 117.25/117.22 (~E(a13,a10)), % 117.25/117.22 inference(scs_inference,[],[731,230,1765,334,31,630,587,30,46,47,48,49,44,45,16,17,4,7,9,10,11,12,13,14,15,429,450,8,6,5,2,3,67,66,43])). % 117.25/117.22 cnf(2844,plain, % 117.25/117.22 (~P3(f2(a13,f3(a13,a13)),f4(a13,a12))), % 117.25/117.22 inference(scs_inference,[],[41,731,230,1765,334,31,630,587,369,30,46,47,48,49,44,45,16,17,4,7,9,10,11,12,13,14,15,429,450,8,6,5,2,3,67,66,43,21])). % 117.25/117.22 cnf(2845,plain, % 117.25/117.22 (~E(f2(a13,f3(a13,a13)),a1)), % 117.25/117.22 inference(scs_inference,[],[41,731,230,1765,334,31,630,488,587,369,489,30,46,47,48,49,44,45,16,17,4,7,9,10,11,12,13,14,15,429,450,8,6,5,2,3,67,66,43,21,42])). % 117.25/117.22 cnf(2852,plain, % 117.25/117.22 (E(f2(a14,f7(a14,a14)),a14)), % 117.25/117.22 inference(scs_inference,[],[41,731,230,274,1619,2733,1765,334,506,563,631,31,630,488,587,369,489,542,30,46,47,48,49,44,45,16,17,4,7,9,10,11,12,13,14,15,429,450,8,6,5,2,3,67,66,43,21,42,23,24,25,77,86])). % 117.25/117.22 cnf(2858,plain, % 117.25/117.22 (E(f2(f4(a12,a12),f4(a12,a12)),f4(a12,f2(a12,a12)))), % 117.25/117.22 inference(scs_inference,[],[41,731,230,274,1619,2733,1765,334,506,563,631,31,630,488,587,369,489,29,542,30,46,47,48,49,44,45,16,17,4,7,9,10,11,12,13,14,15,429,450,8,6,5,2,3,67,66,43,21,42,23,24,25,77,86,95,96,104])). % 117.25/117.22 cnf(2866,plain, % 117.25/117.22 (P5(f3(a13,a13),f2(a14,f3(a14,a14)))), % 117.25/117.22 inference(scs_inference,[],[41,731,709,230,274,1619,2733,1765,334,506,563,631,31,630,488,587,369,489,29,376,542,30,46,47,48,49,44,45,16,17,4,7,9,10,11,12,13,14,15,429,450,8,6,5,2,3,67,66,43,21,42,23,24,25,77,86,95,96,104,105,60,61,65])). % 117.25/117.22 cnf(2874,plain, % 117.25/117.22 (~P1(f4(a13,a12))), % 117.25/117.22 inference(scs_inference,[],[41,731,709,230,274,1619,2733,1765,1707,334,506,563,631,31,630,589,488,587,369,1697,562,593,489,29,376,542,133,30,46,47,48,49,44,45,16,17,4,7,9,10,11,12,13,14,15,429,450,8,6,5,2,3,67,66,43,21,42,23,24,25,77,86,95,96,104,105,60,61,65,112,111,58,110])). % 117.25/117.22 cnf(2886,plain, % 117.25/117.22 (E(f2(a1,a1),f3(f3(a1,a1),a1))), % 117.25/117.22 inference(scs_inference,[],[41,731,738,709,230,274,1619,2733,1765,1707,334,486,506,745,558,563,631,301,437,31,630,589,488,587,369,426,1697,323,562,593,489,519,29,376,219,542,28,133,30,26,46,47,48,49,44,45,16,17,4,7,9,10,11,12,13,14,15,429,450,8,6,5,2,3,67,66,43,21,42,23,24,25,77,86,95,96,104,105,60,61,65,112,111,58,110,70,79,62,120,73,83])). % 117.25/117.22 cnf(2888,plain, % 117.25/117.22 (~P5(f2(f2(a13,a14),f3(f2(a13,a14),f2(a13,a14))),a13)), % 117.25/117.22 inference(scs_inference,[],[41,731,738,709,230,274,628,1619,2733,1765,1707,334,486,506,745,558,563,631,301,437,31,630,589,591,488,587,369,426,1697,323,584,562,593,489,519,29,376,219,542,28,133,30,26,46,47,48,49,44,45,16,17,4,7,9,10,11,12,13,14,15,429,450,8,6,5,2,3,67,66,43,21,42,23,24,25,77,86,95,96,104,105,60,61,65,112,111,58,110,70,79,62,120,73,83,74])). % 117.25/117.22 cnf(2892,plain, % 117.25/117.22 (~E(f2(a13,a11),a13)), % 117.25/117.22 inference(scs_inference,[],[41,731,738,709,230,274,628,1619,2738,2733,1765,1707,334,486,506,745,558,563,631,301,437,31,630,589,591,488,587,369,426,1697,160,323,584,562,593,366,489,519,29,376,219,542,28,133,30,26,46,47,48,49,44,45,16,17,4,7,9,10,11,12,13,14,15,429,450,8,6,5,2,3,67,66,43,21,42,23,24,25,77,86,95,96,104,105,60,61,65,112,111,58,110,70,79,62,120,73,83,74,75,89])). % 117.25/117.22 cnf(2904,plain, % 117.25/117.22 (E(f4(f3(a12,a12),a10),f3(a12,a12))), % 117.25/117.22 inference(scs_inference,[],[396,323,45,49])). % 117.25/117.22 cnf(2906,plain, % 117.25/117.22 (E(f2(f3(a12,a12),a1),f3(a12,a12))), % 117.25/117.22 inference(scs_inference,[],[396,323,45,49,48])). % 117.25/117.22 cnf(2908,plain, % 117.25/117.22 (E(f2(a1,f3(a12,a12)),f3(a12,a12))), % 117.25/117.22 inference(scs_inference,[],[396,323,45,49,48,46])). % 117.25/117.22 cnf(2919,plain, % 117.25/117.22 (E(f2(f2(a14,f7(a14,a14)),x29191),f2(a14,x29191))), % 117.25/117.22 inference(scs_inference,[],[2852,745,396,323,45,49,48,46,429,47,12,15,9,44,11,4])). % 117.25/117.22 cnf(2928,plain, % 117.25/117.22 (E(f2(x29281,f2(a14,f7(a14,a14))),f2(x29281,a14))), % 117.25/117.22 inference(scs_inference,[],[2852,745,396,323,45,49,48,46,429,47,12,15,9,44,11,4,7,17,10,16,14,13,8,6,5])). % 117.25/117.22 cnf(2929,plain, % 117.25/117.22 (~E(a10,a13)), % 117.25/117.22 inference(scs_inference,[],[2842,2852,745,396,323,45,49,48,46,429,47,12,15,9,44,11,4,7,17,10,16,14,13,8,6,5,2])). % 117.25/117.22 cnf(2930,plain, % 117.25/117.22 (P1(f2(f3(a12,a12),f3(a12,a12)))), % 117.25/117.22 inference(scs_inference,[],[2842,2852,745,396,323,45,49,48,46,429,47,12,15,9,44,11,4,7,17,10,16,14,13,8,6,5,2,66])). % 117.25/117.22 cnf(2932,plain, % 117.25/117.22 (P1(f4(f3(a12,a12),f3(a12,a12)))), % 117.25/117.22 inference(scs_inference,[],[2842,2852,745,396,323,45,49,48,46,429,47,12,15,9,44,11,4,7,17,10,16,14,13,8,6,5,2,66,67])). % 117.25/117.22 cnf(2935,plain, % 117.25/117.22 (E(f3(x29351,a1),f3(x29351,f3(f3(a1,a1),a1)))), % 117.25/117.22 inference(rename_variables,[],[2823])). % 117.25/117.22 cnf(2936,plain, % 117.25/117.22 (~E(f2(a13,f3(a13,a13)),a10)), % 117.25/117.22 inference(scs_inference,[],[2842,2886,2852,2823,745,396,488,323,489,45,49,48,46,429,47,12,15,9,44,11,4,7,17,10,16,14,13,8,6,5,2,66,67,3,43])). % 117.25/117.22 cnf(2938,plain, % 117.25/117.22 (~E(a13,a1)), % 117.25/117.22 inference(scs_inference,[],[2842,2886,2852,2823,745,396,31,488,323,489,30,45,49,48,46,429,47,12,15,9,44,11,4,7,17,10,16,14,13,8,6,5,2,66,67,3,43,42])). % 117.25/117.22 cnf(2941,plain, % 117.25/117.22 (~P5(f2(a14,f7(a14,a14)),f3(a13,a13))), % 117.25/117.22 inference(scs_inference,[],[2842,2886,215,2852,2823,745,396,698,31,488,323,489,30,45,49,48,46,429,47,12,15,9,44,11,4,7,17,10,16,14,13,8,6,5,2,66,67,3,43,42,23,24])). % 117.25/117.22 cnf(2942,plain, % 117.25/117.22 (~P5(f3(a11,a13),f2(f3(a13,a13),f3(f3(a13,a13),f3(a13,a13))))), % 117.25/117.22 inference(scs_inference,[],[2842,2886,215,2852,2823,700,745,396,698,31,488,323,489,394,30,45,49,48,46,429,47,12,15,9,44,11,4,7,17,10,16,14,13,8,6,5,2,66,67,3,43,42,23,24,25])). % 117.25/117.22 cnf(2943,plain, % 117.25/117.22 (~E(f3(f3(a13,a13),f3(a13,a13)),f4(a13,a12))), % 117.25/117.22 inference(scs_inference,[],[2842,2874,2886,215,2852,2823,700,745,396,698,31,488,323,489,394,30,45,49,48,46,429,47,12,15,9,44,11,4,7,17,10,16,14,13,8,6,5,2,66,67,3,43,42,23,24,25,18])). % 117.25/117.22 cnf(2944,plain, % 117.25/117.22 (P1(f5(f2(a13,f3(a13,a13))))), % 117.25/117.22 inference(scs_inference,[],[2842,2874,2886,215,2845,2852,2823,700,745,396,698,31,488,323,489,394,30,45,49,48,46,429,47,12,15,9,44,11,4,7,17,10,16,14,13,8,6,5,2,66,67,3,43,42,23,24,25,18,50])). % 117.25/117.22 cnf(2946,plain, % 117.25/117.22 (P5(a10,f2(a13,f3(a13,a13)))), % 117.25/117.22 inference(scs_inference,[],[2842,2874,2886,215,2845,2852,2823,700,745,396,698,31,488,323,489,394,30,45,49,48,46,429,47,12,15,9,44,11,4,7,17,10,16,14,13,8,6,5,2,66,67,3,43,42,23,24,25,18,50,54])). % 117.25/117.22 cnf(2948,plain, % 117.25/117.22 (P5(a13,f4(a13,a13))), % 117.25/117.22 inference(scs_inference,[],[2842,2874,2886,215,2845,2852,2823,700,745,396,698,31,488,323,489,394,30,45,49,48,46,429,47,12,15,9,44,11,4,7,17,10,16,14,13,8,6,5,2,66,67,3,43,42,23,24,25,18,50,54,71])). % 117.25/117.22 cnf(2950,plain, % 117.25/117.22 (P3(f5(a13),a13)), % 117.25/117.22 inference(scs_inference,[],[2842,2874,2886,215,2845,2852,2823,700,745,396,698,31,488,323,489,394,30,45,49,48,46,429,47,12,15,9,44,11,4,7,17,10,16,14,13,8,6,5,2,66,67,3,43,42,23,24,25,18,50,54,71,57])). % 117.25/117.22 cnf(2960,plain, % 117.25/117.22 (~E(f2(a13,a13),a1)), % 117.25/117.22 inference(scs_inference,[],[2842,2874,2886,215,2845,2852,2823,700,745,751,338,396,698,31,488,694,323,203,489,394,542,30,45,49,48,46,429,47,12,15,9,44,11,4,7,17,10,16,14,13,8,6,5,2,66,67,3,43,42,23,24,25,18,50,54,71,57,96,105,77,86,60])). % 117.25/117.22 cnf(2962,plain, % 117.25/117.22 (E(f2(f4(a14,a14),f4(a14,a14)),f4(a14,f2(a14,a14)))), % 117.25/117.22 inference(scs_inference,[],[2842,2874,2886,215,2845,2852,2823,700,745,751,338,396,698,31,488,694,323,203,489,394,542,30,45,49,48,46,429,47,12,15,9,44,11,4,7,17,10,16,14,13,8,6,5,2,66,67,3,43,42,23,24,25,18,50,54,71,57,96,105,77,86,60,104])). % 117.25/117.22 cnf(2966,plain, % 117.25/117.22 (P2(f5(f2(a13,f3(a13,a13))))), % 117.25/117.22 inference(scs_inference,[],[2842,2874,2886,215,2845,2852,2823,700,745,751,338,396,698,31,488,694,323,203,489,394,542,30,45,49,48,46,429,47,12,15,9,44,11,4,7,17,10,16,14,13,8,6,5,2,66,67,3,43,42,23,24,25,18,50,54,71,57,96,105,77,86,60,104,95,51])). % 117.25/117.22 cnf(2968,plain, % 117.25/117.22 (E(f2(f2(a13,a14),f3(a11,f2(a13,a14))),a11)), % 117.25/117.22 inference(scs_inference,[],[2842,2874,2886,215,2845,2852,2823,700,745,541,751,338,396,698,31,488,694,323,203,519,489,394,542,28,30,45,49,48,46,429,47,12,15,9,44,11,4,7,17,10,16,14,13,8,6,5,2,66,67,3,43,42,23,24,25,18,50,54,71,57,96,105,77,86,60,104,95,51,118])). % 117.25/117.22 cnf(2970,plain, % 117.25/117.22 (P5(f3(a13,a13),f3(a11,a13))), % 117.25/117.22 inference(scs_inference,[],[2842,2874,2886,215,2845,2852,2823,700,745,541,751,338,396,698,31,488,694,323,562,203,519,489,376,394,542,28,30,45,49,48,46,429,47,12,15,9,44,11,4,7,17,10,16,14,13,8,6,5,2,66,67,3,43,42,23,24,25,18,50,54,71,57,96,105,77,86,60,104,95,51,118,65])). % 117.25/117.22 cnf(2972,plain, % 117.25/117.22 (~E(f3(a13,a13),f2(a13,a14))), % 117.25/117.22 inference(scs_inference,[],[2842,2874,2886,215,2845,2852,2823,700,738,745,541,751,338,396,698,31,488,694,323,562,203,519,489,376,394,542,28,30,45,49,48,46,429,47,12,15,9,44,11,4,7,17,10,16,14,13,8,6,5,2,66,67,3,43,42,23,24,25,18,50,54,71,57,96,105,77,86,60,104,95,51,118,65,58])). % 117.25/117.22 cnf(2978,plain, % 117.25/117.22 (E(f2(f3(f3(a1,a1),a1),f3(a1,a1)),a1)), % 117.25/117.22 inference(scs_inference,[],[2842,2874,648,2866,2886,215,2845,2852,2823,2935,729,700,738,745,541,751,285,338,396,698,31,488,694,323,562,630,203,519,489,376,394,219,542,28,30,26,45,49,48,46,429,47,12,15,9,44,11,4,7,17,10,16,14,13,8,6,5,2,66,67,3,43,42,23,24,25,18,50,54,71,57,96,105,77,86,60,104,95,51,118,65,58,80,70,83])). % 117.25/117.22 cnf(2981,plain, % 117.25/117.22 (~P5(f2(a11,f3(a11,a11)),a14)), % 117.25/117.22 inference(scs_inference,[],[2842,2874,648,2866,2886,254,215,2845,2852,2823,2935,729,700,738,745,541,751,285,338,396,698,31,488,373,694,323,298,562,630,203,519,489,376,394,219,542,28,30,26,45,49,48,46,429,47,12,15,9,44,11,4,7,17,10,16,14,13,8,6,5,2,66,67,3,43,42,23,24,25,18,50,54,71,57,96,105,77,86,60,104,95,51,118,65,58,80,70,83,74])). % 117.25/117.22 cnf(2990,plain, % 117.25/117.22 (P3(f3(a12,a12),f4(f3(a12,a12),f3(a12,a12)))), % 117.25/117.22 inference(scs_inference,[],[2842,2874,648,2866,2886,254,215,2845,2852,2823,2935,729,700,738,745,541,751,285,338,396,698,524,31,488,373,694,323,584,298,562,630,203,519,489,376,394,219,542,28,30,26,45,49,48,46,429,47,12,15,9,44,11,4,7,17,10,16,14,13,8,6,5,2,66,67,3,43,42,23,24,25,18,50,54,71,57,96,105,77,86,60,104,95,51,118,65,58,80,70,83,74,75,52,22,111,110])). % 117.25/117.22 cnf(2994,plain, % 117.25/117.22 (~E(f4(a13,a13),a1)), % 117.25/117.22 inference(scs_inference,[],[2842,2874,648,2866,2886,254,215,2845,2852,2823,2935,729,700,738,745,541,751,285,338,396,698,524,31,488,373,694,323,584,298,562,630,203,519,489,376,394,219,542,28,30,26,45,49,48,46,429,47,12,15,9,44,11,4,7,17,10,16,14,13,8,6,5,2,66,67,3,43,42,23,24,25,18,50,54,71,57,96,105,77,86,60,104,95,51,118,65,58,80,70,83,74,75,52,22,111,110,112,62])). % 117.25/117.22 cnf(3000,plain, % 117.25/117.22 (~E(f4(a13,a13),f4(a13,a10))), % 117.25/117.22 inference(scs_inference,[],[2842,2874,648,2866,2886,254,215,2845,2852,2823,2935,729,700,738,745,541,642,751,285,338,396,698,524,31,488,373,694,323,584,298,562,630,203,519,489,567,376,394,219,542,28,30,27,26,45,49,48,46,429,47,12,15,9,44,11,4,7,17,10,16,14,13,8,6,5,2,66,67,3,43,42,23,24,25,18,50,54,71,57,96,105,77,86,60,104,95,51,118,65,58,80,70,83,74,75,52,22,111,110,112,62,120,99,81])). % 117.25/117.22 cnf(3002,plain, % 117.25/117.22 (~E(f4(a13,a13),f4(a10,a13))), % 117.25/117.22 inference(scs_inference,[],[2842,2874,648,2866,2886,254,215,2845,2852,2823,2935,729,700,738,745,541,642,751,285,338,396,698,524,31,488,373,694,323,584,298,562,630,203,519,489,567,376,394,219,542,28,30,27,26,45,49,48,46,429,47,12,15,9,44,11,4,7,17,10,16,14,13,8,6,5,2,66,67,3,43,42,23,24,25,18,50,54,71,57,96,105,77,86,60,104,95,51,118,65,58,80,70,83,74,75,52,22,111,110,112,62,120,99,81,82])). % 117.25/117.22 cnf(3037,plain, % 117.25/117.22 (E(f2(x30371,a1),f2(x30371,f3(f3(a1,a1),f3(a1,a1))))), % 117.25/117.22 inference(scs_inference,[],[2930,2932,241,404,52,48,45,47,46,49,44,11,17,9,15,7,12,13,14,4,8,10,16,6,5])). % 117.25/117.22 cnf(3038,plain, % 117.25/117.22 (~E(a1,a13)), % 117.25/117.22 inference(scs_inference,[],[2938,2930,2932,241,404,52,48,45,47,46,49,44,11,17,9,15,7,12,13,14,4,8,10,16,6,5,2])). % 117.25/117.22 cnf(3039,plain, % 117.25/117.22 (P1(f2(f7(a1,a1),f7(a1,a1)))), % 117.25/117.22 inference(scs_inference,[],[2938,2930,2932,241,404,52,48,45,47,46,49,44,11,17,9,15,7,12,13,14,4,8,10,16,6,5,2,66])). % 117.25/117.22 cnf(3041,plain, % 117.25/117.22 (P1(f4(f7(a1,a1),f7(a1,a1)))), % 117.25/117.22 inference(scs_inference,[],[2938,2930,2932,241,404,52,48,45,47,46,49,44,11,17,9,15,7,12,13,14,4,8,10,16,6,5,2,66,67])). % 117.25/117.22 cnf(3043,plain, % 117.25/117.22 (~E(f5(f2(a13,f3(a13,a13))),a10)), % 117.25/117.22 inference(scs_inference,[],[2938,2930,2932,2944,2966,241,404,52,48,45,47,46,49,44,11,17,9,15,7,12,13,14,4,8,10,16,6,5,2,66,67,43])). % 117.25/117.22 cnf(3045,plain, % 117.25/117.22 (~E(f2(a10,f3(a10,a10)),a13)), % 117.25/117.22 inference(scs_inference,[],[2929,2938,2930,2932,2944,2966,241,404,253,52,48,45,47,46,49,44,11,17,9,15,7,12,13,14,4,8,10,16,6,5,2,66,67,43,3])). % 117.25/117.22 cnf(3046,plain, % 117.25/117.22 (~E(f5(f2(a13,f3(a13,a13))),a1)), % 117.25/117.22 inference(scs_inference,[],[2929,2938,2930,2932,2944,2966,241,404,253,52,48,45,47,46,49,44,11,17,9,15,7,12,13,14,4,8,10,16,6,5,2,66,67,43,3,42])). % 117.25/117.22 cnf(3049,plain, % 117.25/117.22 (~P5(f2(f2(a14,f7(a14,a14)),f7(a14,a14)),f3(a13,a13))), % 117.25/117.22 inference(scs_inference,[],[2929,2938,2941,2930,2932,151,2919,2944,2966,241,488,404,253,52,48,45,47,46,49,44,11,17,9,15,7,12,13,14,4,8,10,16,6,5,2,66,67,43,3,42,23,24])). % 117.25/117.22 cnf(3053,plain, % 117.25/117.22 (~E(f2(f3(a12,a12),f3(a12,a12)),f4(a13,a12))), % 117.25/117.22 inference(scs_inference,[],[2929,2938,2941,2930,2932,151,2919,2944,2966,2822,241,2245,2874,488,404,253,52,48,45,47,46,49,44,11,17,9,15,7,12,13,14,4,8,10,16,6,5,2,66,67,43,3,42,23,24,25,18])). % 117.25/117.22 cnf(3054,plain, % 117.25/117.22 (P1(f5(a13))), % 117.25/117.22 inference(scs_inference,[],[2929,2938,2941,2930,2932,151,2919,2944,2966,2822,241,2245,2874,2842,488,404,253,30,52,48,45,47,46,49,44,11,17,9,15,7,12,13,14,4,8,10,16,6,5,2,66,67,43,3,42,23,24,25,18,50])). % 117.25/117.22 cnf(3058,plain, % 117.25/117.22 (P5(a10,a13)), % 117.25/117.22 inference(scs_inference,[],[2929,2938,2950,2941,2930,2932,151,2919,2944,2966,2822,241,2245,2874,2842,488,404,253,30,52,48,45,47,46,49,44,11,17,9,15,7,12,13,14,4,8,10,16,6,5,2,66,67,43,3,42,23,24,25,18,50,78,54])). % 117.25/117.22 cnf(3064,plain, % 117.25/117.22 (P1(f7(f3(a13,a13),f3(a11,a13)))), % 117.25/117.22 inference(scs_inference,[],[2929,2938,2970,2950,2941,2930,2932,151,2919,2944,2966,2822,241,2245,2874,2842,488,404,562,253,376,28,30,52,48,45,47,46,49,44,11,17,9,15,7,12,13,14,4,8,10,16,6,5,2,66,67,43,3,42,23,24,25,18,50,78,54,96,104,77])). % 117.25/117.22 cnf(3066,plain, % 117.25/117.22 (P2(f5(a13))), % 117.25/117.22 inference(scs_inference,[],[2929,2938,2970,2950,2941,2930,2932,151,2919,2944,2966,2822,241,2245,2874,2842,488,404,562,253,376,28,30,52,48,45,47,46,49,44,11,17,9,15,7,12,13,14,4,8,10,16,6,5,2,66,67,43,3,42,23,24,25,18,50,78,54,96,104,77,51])). % 117.25/117.22 cnf(3076,plain, % 117.25/117.22 (P5(a14,f2(f3(a11,a13),f3(f3(a11,a13),f3(a11,a13))))), % 117.25/117.22 inference(scs_inference,[],[2929,2938,2970,2950,2941,2930,2932,151,2919,2942,2944,2966,2832,2822,241,2245,2874,2842,233,488,398,404,222,562,593,253,376,542,28,30,52,48,45,47,46,49,44,11,17,9,15,7,12,13,14,4,8,10,16,6,5,2,66,67,43,3,42,23,24,25,18,50,78,54,96,104,77,51,105,86,95,65,58])). % 117.25/117.22 cnf(3080,plain, % 117.25/117.22 (P5(f5(a13),a13)), % 117.25/117.22 inference(scs_inference,[],[2929,2938,2970,2972,2950,2941,2930,2932,151,2919,2942,2944,2966,2832,2822,241,2245,2874,2842,233,488,398,404,222,562,593,253,519,376,542,28,30,52,48,45,47,46,49,44,11,17,9,15,7,12,13,14,4,8,10,16,6,5,2,66,67,43,3,42,23,24,25,18,50,78,54,96,104,77,51,105,86,95,65,58,80,69])). % 117.25/117.22 cnf(3092,plain, % 117.25/117.22 (P3(f5(a13),f2(a13,a13))), % 117.25/117.22 inference(scs_inference,[],[2929,2938,2970,2972,2950,2904,2941,2930,2932,151,2919,2942,2944,2966,2832,2822,241,2245,2874,2845,424,2842,233,488,257,398,404,222,562,593,253,519,489,29,376,542,312,28,30,27,52,48,45,47,46,49,44,11,17,9,15,7,12,13,14,4,8,10,16,6,5,2,66,67,43,3,42,23,24,25,18,50,78,54,96,104,77,51,105,86,95,65,58,80,69,62,70,120,83,75,97])). % 117.25/117.22 cnf(3098,plain, % 117.25/117.22 (~E(f4(a13,a10),f4(a13,a13))), % 117.25/117.22 inference(scs_inference,[],[2929,2938,2970,2972,2950,2904,2941,2930,2932,151,2919,2942,2944,2966,2832,2822,241,2245,2874,2845,424,2842,233,488,257,398,404,222,562,593,253,519,489,29,376,542,312,28,30,27,52,48,45,47,46,49,44,11,17,9,15,7,12,13,14,4,8,10,16,6,5,2,66,67,43,3,42,23,24,25,18,50,78,54,96,104,77,51,105,86,95,65,58,80,69,62,70,120,83,75,97,99,82,81])). % 117.25/117.22 cnf(3102,plain, % 117.25/117.22 (~P3(a1,a13)), % 117.25/117.22 inference(scs_inference,[],[2929,2938,2970,2972,2950,2904,2941,2930,2932,151,2919,2942,2944,2966,2832,2822,241,2245,2874,2845,424,2842,233,488,257,398,404,222,562,593,253,519,489,29,376,542,312,28,30,27,52,48,45,47,46,49,44,11,17,9,15,7,12,13,14,4,8,10,16,6,5,2,66,67,43,3,42,23,24,25,18,50,78,54,96,104,77,51,105,86,95,65,58,80,69,62,70,120,83,75,97,99,82,81,98,1112])). % 117.25/117.22 cnf(3103,plain, % 117.25/117.22 (P5(f2(a10,f3(a10,a10)),a13)), % 117.25/117.22 inference(scs_inference,[],[2929,2938,2970,2972,2950,2904,2941,2930,2932,151,2919,2942,2944,2966,2832,2822,241,2245,2874,2845,424,2842,233,488,257,398,404,222,562,593,253,519,489,29,376,542,312,28,30,27,52,48,45,47,46,49,44,11,17,9,15,7,12,13,14,4,8,10,16,6,5,2,66,67,43,3,42,23,24,25,18,50,78,54,96,104,77,51,105,86,95,65,58,80,69,62,70,120,83,75,97,99,82,81,98,1112,2803])). % 117.25/117.22 cnf(3104,plain, % 117.25/117.22 (~P3(f2(f3(a1,a1),f3(f3(a1,a1),f3(a1,a1))),a13)), % 117.25/117.22 inference(scs_inference,[],[2929,2938,2970,2972,2950,2904,2941,2930,2932,151,2919,2942,2944,2966,2832,2822,241,2245,2874,2845,424,2842,233,488,257,398,404,222,562,593,253,519,489,29,376,542,312,28,30,27,52,48,45,47,46,49,44,11,17,9,15,7,12,13,14,4,8,10,16,6,5,2,66,67,43,3,42,23,24,25,18,50,78,54,96,104,77,51,105,86,95,65,58,80,69,62,70,120,83,75,97,99,82,81,98,1112,2803,1133])). % 117.25/117.22 cnf(3106,plain, % 117.25/117.22 (~P3(a1,f2(a13,f3(a13,a13)))), % 117.25/117.22 inference(scs_inference,[],[2929,2938,2970,2972,2950,2904,2941,2930,2932,151,2978,2919,2942,2944,2966,2832,2822,241,2245,2874,2845,424,2842,233,488,369,257,398,404,222,562,593,253,519,489,29,376,542,312,28,30,27,52,48,45,47,46,49,44,11,17,9,15,7,12,13,14,4,8,10,16,6,5,2,66,67,43,3,42,23,24,25,18,50,78,54,96,104,77,51,105,86,95,65,58,80,69,62,70,120,83,75,97,99,82,81,98,1112,2803,1133,21,22])). % 117.25/117.22 cnf(3107,plain, % 117.25/117.22 (E(f4(f5(a13),f8(f5(a13),a13)),a13)), % 117.25/117.22 inference(scs_inference,[],[2929,2938,2970,2972,2950,2904,2941,2930,2932,151,2978,2919,2942,2944,2966,2832,2822,241,2245,2874,2845,424,2842,233,488,369,257,398,404,222,562,593,253,519,489,29,376,542,312,28,30,27,52,48,45,47,46,49,44,11,17,9,15,7,12,13,14,4,8,10,16,6,5,2,66,67,43,3,42,23,24,25,18,50,78,54,96,104,77,51,105,86,95,65,58,80,69,62,70,120,83,75,97,99,82,81,98,1112,2803,1133,21,22,85])). % 117.25/117.22 cnf(3124,plain, % 117.25/117.22 (E(a14,f2(f3(a11,a13),f3(f3(a11,a13),f3(a11,a13))))), % 117.25/117.22 inference(scs_inference,[],[3076,1255])). % 117.25/117.22 cnf(3126,plain, % 117.25/117.22 (P5(f5(a13),f5(a13))), % 117.25/117.22 inference(scs_inference,[],[3054,52])). % 117.25/117.22 cnf(3128,plain, % 117.25/117.22 (E(f4(f5(a13),a1),a1)), % 117.25/117.22 inference(scs_inference,[],[3054,52,45])). % 117.25/117.22 cnf(3130,plain, % 117.25/117.22 (E(f4(a10,f5(a13)),f5(a13))), % 117.25/117.22 inference(scs_inference,[],[3054,52,45,47])). % 117.25/117.22 cnf(3132,plain, % 117.25/117.22 (E(f4(f5(a13),a10),f5(a13))), % 117.25/117.22 inference(scs_inference,[],[3054,52,45,47,49])). % 117.25/117.22 cnf(3134,plain, % 117.25/117.22 (E(f2(f5(a13),a1),f5(a13))), % 117.25/117.22 inference(scs_inference,[],[3054,52,45,47,49,48])). % 117.25/117.22 cnf(3136,plain, % 117.25/117.22 (E(f2(a1,f5(a13)),f5(a13))), % 117.25/117.22 inference(scs_inference,[],[3054,52,45,47,49,48,46])). % 117.25/117.22 cnf(3154,plain, % 117.25/117.22 (~E(a1,f2(a13,a13))), % 117.25/117.22 inference(scs_inference,[],[2960,3054,224,52,45,47,49,48,46,44,15,17,11,13,9,12,7,10,8,14,4,16,6,5,2])). % 117.25/117.22 cnf(3155,plain, % 117.25/117.22 (P1(f2(f5(a13),f5(a13)))), % 117.25/117.22 inference(scs_inference,[],[2960,3054,224,52,45,47,49,48,46,44,15,17,11,13,9,12,7,10,8,14,4,16,6,5,2,66])). % 117.25/117.22 cnf(3157,plain, % 117.25/117.22 (~P3(f2(f3(a1,a1),a1),a13)), % 117.25/117.22 inference(scs_inference,[],[2960,3054,3037,3104,224,52,45,47,49,48,46,44,15,17,11,13,9,12,7,10,8,14,4,16,6,5,2,66,21])). % 117.25/117.22 cnf(3159,plain, % 117.25/117.22 (P1(f4(f5(a13),f5(a13)))), % 117.25/117.22 inference(scs_inference,[],[2960,3054,3037,3104,224,52,45,47,49,48,46,44,15,17,11,13,9,12,7,10,8,14,4,16,6,5,2,66,21,67])). % 117.25/117.22 cnf(3161,plain, % 117.25/117.22 (~E(f5(a13),a10)), % 117.25/117.22 inference(scs_inference,[],[2960,3054,3066,3037,3104,224,52,45,47,49,48,46,44,15,17,11,13,9,12,7,10,8,14,4,16,6,5,2,66,21,67,43])). % 117.25/117.22 cnf(3164,plain, % 117.25/117.22 (~E(f5(a13),a1)), % 117.25/117.22 inference(scs_inference,[],[2960,3054,3066,3037,3104,2968,224,516,52,45,47,49,48,46,44,15,17,11,13,9,12,7,10,8,14,4,16,6,5,2,66,21,67,43,3,42])). % 117.25/117.22 cnf(3168,plain, % 117.25/117.22 (~P5(f2(a13,a14),a14)), % 117.25/117.22 inference(scs_inference,[],[3102,2960,3054,3066,2981,1165,3037,3104,3107,2968,224,516,692,52,45,47,49,48,46,44,15,17,11,13,9,12,7,10,8,14,4,16,6,5,2,66,21,67,43,3,42,22,23,24])). % 117.25/117.22 cnf(3170,plain, % 117.25/117.22 (~E(f5(a13),f4(a13,a12))), % 117.25/117.22 inference(scs_inference,[],[3102,2960,3054,3066,2981,1165,3037,3104,3107,2968,224,677,516,692,2874,52,45,47,49,48,46,44,15,17,11,13,9,12,7,10,8,14,4,16,6,5,2,66,21,67,43,3,42,22,23,24,25,18])). % 117.25/117.22 cnf(3173,plain, % 117.25/117.22 (P3(f5(f5(a13)),f5(a13))), % 117.25/117.22 inference(scs_inference,[],[3102,2960,3054,3066,2981,1165,3037,3104,3107,2968,224,677,516,692,2874,2845,489,52,45,47,49,48,46,44,15,17,11,13,9,12,7,10,8,14,4,16,6,5,2,66,21,67,43,3,42,22,23,24,25,18,71,57])). % 117.25/117.22 cnf(3175,plain, % 117.25/117.22 (P1(f5(f5(a13)))), % 117.25/117.22 inference(scs_inference,[],[3102,2960,3054,3066,2981,1165,3037,3104,3107,2968,224,677,516,692,2874,2845,489,52,45,47,49,48,46,44,15,17,11,13,9,12,7,10,8,14,4,16,6,5,2,66,21,67,43,3,42,22,23,24,25,18,71,57,50])). % 117.25/117.22 cnf(3185,plain, % 117.25/117.22 (E(f2(a10,f7(a10,a13)),a13)), % 117.25/117.22 inference(scs_inference,[],[3102,3058,2960,3054,3066,2981,1165,3037,3104,3107,2968,224,677,516,692,2874,2845,489,30,27,52,45,47,49,48,46,44,15,17,11,13,9,12,7,10,8,14,4,16,6,5,2,66,21,67,43,3,42,22,23,24,25,18,71,57,50,104,60,96,95,86])). % 117.25/117.22 cnf(3187,plain, % 117.25/117.22 (P2(f5(f5(a13)))), % 117.25/117.22 inference(scs_inference,[],[3102,3058,2960,3054,3066,2981,1165,3037,3104,3107,2968,224,677,516,692,2874,2845,489,30,27,52,45,47,49,48,46,44,15,17,11,13,9,12,7,10,8,14,4,16,6,5,2,66,21,67,43,3,42,22,23,24,25,18,71,57,50,104,60,96,95,86,51])). % 117.25/117.22 cnf(3189,plain, % 117.25/117.22 (P1(f7(f5(a13),f5(a13)))), % 117.25/117.22 inference(scs_inference,[],[3102,3058,2960,3054,3066,2981,1165,3037,3104,3107,2968,224,677,516,692,2874,2845,489,30,27,52,45,47,49,48,46,44,15,17,11,13,9,12,7,10,8,14,4,16,6,5,2,66,21,67,43,3,42,22,23,24,25,18,71,57,50,104,60,96,95,86,51,77])). % 117.25/117.22 cnf(3193,plain, % 117.25/117.22 (~E(f2(f5(a13),f5(a13)),a1)), % 117.25/117.22 inference(scs_inference,[],[3102,3058,2960,3054,3066,2981,1165,3037,3104,3107,2968,224,677,516,692,2874,2845,489,30,27,52,45,47,49,48,46,44,15,17,11,13,9,12,7,10,8,14,4,16,6,5,2,66,21,67,43,3,42,22,23,24,25,18,71,57,50,104,60,96,95,86,51,77,105,61])). % 117.25/117.22 cnf(3195,plain, % 117.25/117.22 (P5(f3(a13,a13),f2(a11,f3(a11,a11)))), % 117.25/117.22 inference(scs_inference,[],[3102,3058,2960,3054,3066,2981,1165,3037,3104,3107,2968,224,677,724,516,692,2874,2845,298,489,376,30,27,52,45,47,49,48,46,44,15,17,11,13,9,12,7,10,8,14,4,16,6,5,2,66,21,67,43,3,42,22,23,24,25,18,71,57,50,104,60,96,95,86,51,77,105,61,65])). % 117.25/117.22 cnf(3199,plain, % 117.25/117.22 (~E(a13,f4(a1,a13))), % 117.25/117.22 inference(scs_inference,[],[3102,3038,3058,2960,3054,3066,2981,1165,3037,3104,3107,2968,224,677,724,516,692,2874,2845,298,489,376,30,27,26,52,45,47,49,48,46,44,15,17,11,13,9,12,7,10,8,14,4,16,6,5,2,66,21,67,43,3,42,22,23,24,25,18,71,57,50,104,60,96,95,86,51,77,105,61,65,80,72])). % 117.25/117.22 cnf(3201,plain, % 117.25/117.22 (~E(f4(f5(a13),f5(a13)),a1)), % 117.25/117.22 inference(scs_inference,[],[3102,3038,3058,2960,3054,3066,2981,1165,3037,3104,3107,2968,224,677,724,516,692,2874,2845,298,489,376,30,27,26,52,45,47,49,48,46,44,15,17,11,13,9,12,7,10,8,14,4,16,6,5,2,66,21,67,43,3,42,22,23,24,25,18,71,57,50,104,60,96,95,86,51,77,105,61,65,80,72,62])). % 117.25/117.22 cnf(3205,plain, % 117.25/117.22 (~E(f4(a13,a12),f3(a13,a10))), % 117.25/117.22 inference(scs_inference,[],[3102,3038,3058,2960,3054,3066,2906,2981,1165,3037,3104,3107,2968,224,677,724,516,692,2874,2845,298,489,29,376,312,30,27,26,52,45,47,49,48,46,44,15,17,11,13,9,12,7,10,8,14,4,16,6,5,2,66,21,67,43,3,42,22,23,24,25,18,71,57,50,104,60,96,95,86,51,77,105,61,65,80,72,62,83,75])). % 117.25/117.22 cnf(3207,plain, % 117.25/117.22 (~P3(a1,f5(a13))), % 117.25/117.22 inference(scs_inference,[],[3102,3038,3058,2960,3054,3066,2906,2981,1165,3037,3104,3107,2968,224,677,724,516,692,2874,2845,2950,298,489,29,376,312,30,27,26,52,45,47,49,48,46,44,15,17,11,13,9,12,7,10,8,14,4,16,6,5,2,66,21,67,43,3,42,22,23,24,25,18,71,57,50,104,60,96,95,86,51,77,105,61,65,80,72,62,83,75,88])). % 117.25/117.22 cnf(3211,plain, % 117.25/117.22 (P3(f5(f5(a13)),f2(f5(a13),f5(a13)))), % 117.25/117.22 inference(scs_inference,[],[3102,3038,3058,2960,3054,3066,2906,2981,1165,3037,3104,3107,2968,224,677,724,516,692,2874,2845,2950,298,489,29,376,312,30,27,26,52,45,47,49,48,46,44,15,17,11,13,9,12,7,10,8,14,4,16,6,5,2,66,21,67,43,3,42,22,23,24,25,18,71,57,50,104,60,96,95,86,51,77,105,61,65,80,72,62,83,75,88,76,97])). % 117.25/117.22 cnf(3213,plain, % 117.25/117.22 (~E(f4(a13,a13),f4(a13,a1))), % 117.25/117.22 inference(scs_inference,[],[3102,3038,3058,2960,3054,3066,2906,2981,1165,3037,3104,3107,2968,224,677,724,516,692,2874,2845,2950,2938,298,489,29,376,312,30,27,26,52,45,47,49,48,46,44,15,17,11,13,9,12,7,10,8,14,4,16,6,5,2,66,21,67,43,3,42,22,23,24,25,18,71,57,50,104,60,96,95,86,51,77,105,61,65,80,72,62,83,75,88,76,97,81])). % 117.25/117.22 cnf(3217,plain, % 117.25/117.22 (~E(f4(a13,a13),f4(a1,a13))), % 117.25/117.22 inference(scs_inference,[],[3102,3038,3058,2960,3054,3066,2906,528,2981,1165,3037,3104,3107,2968,224,677,724,516,692,2874,2845,2950,297,2938,298,489,29,376,312,30,27,26,52,45,47,49,48,46,44,15,17,11,13,9,12,7,10,8,14,4,16,6,5,2,66,21,67,43,3,42,22,23,24,25,18,71,57,50,104,60,96,95,86,51,77,105,61,65,80,72,62,83,75,88,76,97,81,99,82])). % 117.25/117.22 cnf(3219,plain, % 117.25/117.22 (E(f5(a13),a13)), % 117.25/117.22 inference(scs_inference,[],[3102,3038,3058,2960,3054,3066,2906,528,2981,1165,3037,3104,3107,2968,224,677,724,516,692,2874,2845,2950,297,31,2938,298,489,29,376,312,30,27,26,52,45,47,49,48,46,44,15,17,11,13,9,12,7,10,8,14,4,16,6,5,2,66,21,67,43,3,42,22,23,24,25,18,71,57,50,104,60,96,95,86,51,77,105,61,65,80,72,62,83,75,88,76,97,81,99,82,68])). % 117.25/117.22 cnf(3223,plain, % 117.25/117.22 (~P5(f2(a11,f3(a11,a11)),f2(a14,f3(a14,a14)))), % 117.25/117.22 inference(scs_inference,[],[3102,3038,3058,2960,3054,3066,2906,528,2981,1165,3037,3104,3107,2968,224,581,677,724,643,516,692,2874,2845,2950,297,31,2938,529,298,630,519,489,29,376,542,312,30,27,26,52,45,47,49,48,46,44,15,17,11,13,9,12,7,10,8,14,4,16,6,5,2,66,21,67,43,3,42,22,23,24,25,18,71,57,50,104,60,96,95,86,51,77,105,61,65,80,72,62,83,75,88,76,97,81,99,82,68,98,87])). % 117.25/117.22 cnf(3227,plain, % 117.25/117.22 (P5(a13,f5(a13))), % 117.25/117.22 inference(scs_inference,[],[3102,3038,3058,2960,3054,3066,2906,528,2981,1165,3037,3104,3107,2968,224,581,677,724,643,516,692,2874,2845,2950,297,31,2938,529,298,630,519,489,29,376,542,312,30,27,26,52,45,47,49,48,46,44,15,17,11,13,9,12,7,10,8,14,4,16,6,5,2,66,21,67,43,3,42,22,23,24,25,18,71,57,50,104,60,96,95,86,51,77,105,61,65,80,72,62,83,75,88,76,97,81,99,82,68,98,87,85,58])). % 117.25/117.22 cnf(3233,plain, % 117.25/117.22 (P5(f4(a13,f5(a13)),f4(f2(a11,f3(a11,a11)),f5(a13)))), % 117.25/117.22 inference(scs_inference,[],[3102,3038,3058,2960,3054,3066,2906,528,2981,1165,3037,3104,3107,2968,224,581,677,724,643,516,692,2874,2845,2950,297,31,2938,529,298,630,519,489,29,376,542,312,30,27,26,52,45,47,49,48,46,44,15,17,11,13,9,12,7,10,8,14,4,16,6,5,2,66,21,67,43,3,42,22,23,24,25,18,71,57,50,104,60,96,95,86,51,77,105,61,65,80,72,62,83,75,88,76,97,81,99,82,68,98,87,85,58,113,119,101])). % 117.25/117.22 cnf(3237,plain, % 117.25/117.22 (E(f4(a10,f3(a10,a10)),f3(a10,a10))), % 117.25/117.22 inference(scs_inference,[],[222,47])). % 117.25/117.22 cnf(3241,plain, % 117.25/117.22 (E(f4(f3(a10,a10),a10),f3(a10,a10))), % 117.25/117.22 inference(scs_inference,[],[3039,222,47,45,49])). % 117.25/117.22 cnf(3247,plain, % 117.25/117.22 (E(f2(a1,f3(a10,a10)),f3(a10,a10))), % 117.25/117.22 inference(scs_inference,[],[3039,222,47,45,49,48,52,46])). % 117.25/117.22 cnf(3254,plain, % 117.25/117.22 (E(f3(x32541,f5(a13)),f3(x32541,a13))), % 117.25/117.22 inference(scs_inference,[],[3219,3039,222,47,45,49,48,52,46,44,11,17,15,7])). % 117.25/117.22 cnf(3255,plain, % 117.25/117.22 (E(f4(x32551,f5(a13)),f4(x32551,a13))), % 117.25/117.22 inference(scs_inference,[],[3219,3039,222,47,45,49,48,52,46,44,11,17,15,7,9])). % 117.25/117.22 cnf(3256,plain, % 117.25/117.22 (E(f7(f5(a13),x32561),f7(a13,x32561))), % 117.25/117.22 inference(scs_inference,[],[3219,3039,222,47,45,49,48,52,46,44,11,17,15,7,9,12])). % 117.25/117.22 cnf(3257,plain, % 117.25/117.22 (E(f7(x32571,f5(a13)),f7(x32571,a13))), % 117.25/117.22 inference(scs_inference,[],[3219,3039,222,47,45,49,48,52,46,44,11,17,15,7,9,12,13])). % 117.25/117.22 cnf(3258,plain, % 117.25/117.22 (E(f4(f5(a13),x32581),f4(a13,x32581))), % 117.25/117.22 inference(scs_inference,[],[3219,3039,222,47,45,49,48,52,46,44,11,17,15,7,9,12,13,8])). % 117.25/117.22 cnf(3260,plain, % 117.25/117.22 (E(f2(f5(a13),x32601),f2(a13,x32601))), % 117.25/117.22 inference(scs_inference,[],[3219,3039,222,47,45,49,48,52,46,44,11,17,15,7,9,12,13,8,10,4])). % 117.25/117.22 cnf(3262,plain, % 117.25/117.22 (E(f5(f5(a13)),f5(a13))), % 117.25/117.22 inference(scs_inference,[],[3219,3039,222,47,45,49,48,52,46,44,11,17,15,7,9,12,13,8,10,4,14,16])). % 117.25/117.22 cnf(3263,plain, % 117.25/117.22 (E(f3(f5(a13),x32631),f3(a13,x32631))), % 117.25/117.22 inference(scs_inference,[],[3219,3039,222,47,45,49,48,52,46,44,11,17,15,7,9,12,13,8,10,4,14,16,6])). % 117.25/117.22 cnf(3264,plain, % 117.25/117.22 (E(f2(x32641,f5(a13)),f2(x32641,a13))), % 117.25/117.22 inference(scs_inference,[],[3219,3039,222,47,45,49,48,52,46,44,11,17,15,7,9,12,13,8,10,4,14,16,6,5])). % 117.25/117.22 cnf(3265,plain, % 117.25/117.22 (~E(f4(a1,a13),f4(a13,a13))), % 117.25/117.22 inference(scs_inference,[],[3217,3219,3039,222,47,45,49,48,52,46,44,11,17,15,7,9,12,13,8,10,4,14,16,6,5,2])). % 117.25/117.22 cnf(3266,plain, % 117.25/117.22 (P1(f2(f3(a10,a10),f3(a10,a10)))), % 117.25/117.22 inference(scs_inference,[],[3217,3219,3039,222,47,45,49,48,52,46,44,11,17,15,7,9,12,13,8,10,4,14,16,6,5,2,66])). % 117.25/117.22 cnf(3268,plain, % 117.25/117.22 (~P3(f5(a13),f4(a13,a12))), % 117.25/117.22 inference(scs_inference,[],[41,3217,3219,3039,222,47,45,49,48,52,46,44,11,17,15,7,9,12,13,8,10,4,14,16,6,5,2,66,21])). % 117.25/117.22 cnf(3269,plain, % 117.25/117.22 (P1(f4(f3(a10,a10),f3(a10,a10)))), % 117.25/117.22 inference(scs_inference,[],[41,3217,3219,3039,222,47,45,49,48,52,46,44,11,17,15,7,9,12,13,8,10,4,14,16,6,5,2,66,21,67])). % 117.25/117.22 cnf(3271,plain, % 117.25/117.22 (~E(f5(f5(a13)),a10)), % 117.25/117.22 inference(scs_inference,[],[41,3217,3219,3039,3175,3187,222,47,45,49,48,52,46,44,11,17,15,7,9,12,13,8,10,4,14,16,6,5,2,66,21,67,43])). % 117.25/117.22 cnf(3273,plain, % 117.25/117.22 (~E(f5(f5(a13)),a1)), % 117.25/117.22 inference(scs_inference,[],[41,3217,3219,3039,3175,3187,222,47,45,49,48,52,46,44,11,17,15,7,9,12,13,8,10,4,14,16,6,5,2,66,21,67,43,42])). % 117.25/117.22 cnf(3276,plain, % 117.25/117.22 (~P3(a13,f4(f5(a13),a12))), % 117.25/117.22 inference(scs_inference,[],[41,3098,3217,3219,3039,3175,3187,222,47,45,49,48,52,46,44,11,17,15,7,9,12,13,8,10,4,14,16,6,5,2,66,21,67,43,42,3,22])). % 117.25/117.22 cnf(3278,plain, % 117.25/117.22 (~P5(f2(a13,f2(a14,f7(a14,a14))),a14)), % 117.25/117.22 inference(scs_inference,[],[41,3098,3217,3168,3219,3039,1209,3175,3187,2928,222,47,45,49,48,52,46,44,11,17,15,7,9,12,13,8,10,4,14,16,6,5,2,66,21,67,43,42,3,22,23,24])). % 117.25/117.22 cnf(3280,plain, % 117.25/117.22 (~P5(f2(f2(a13,a14),f3(f2(a13,a14),f2(a13,a14))),f5(a13))), % 117.25/117.22 inference(scs_inference,[],[41,3098,3217,3168,3219,3039,1209,3175,3187,2928,2888,222,47,45,49,48,52,46,44,11,17,15,7,9,12,13,8,10,4,14,16,6,5,2,66,21,67,43,42,3,22,23,24,25])). % 117.25/117.22 cnf(3281,plain, % 117.25/117.22 (~E(f2(f7(a1,a1),f7(a1,a1)),f4(a13,a12))), % 117.25/117.22 inference(scs_inference,[],[41,3098,3217,3168,3219,3039,1209,3175,3187,2928,2888,2874,222,47,45,49,48,52,46,44,11,17,15,7,9,12,13,8,10,4,14,16,6,5,2,66,21,67,43,42,3,22,23,24,25,18])). % 117.25/117.22 cnf(3284,plain, % 117.25/117.22 (P5(f5(a13),f4(f5(a13),f5(a13)))), % 117.25/117.22 inference(scs_inference,[],[41,3098,3217,3164,3168,3219,3039,1209,3175,3187,2928,2888,2874,222,3054,27,47,45,49,48,52,46,44,11,17,15,7,9,12,13,8,10,4,14,16,6,5,2,66,21,67,43,42,3,22,23,24,25,18,104,71])). % 117.25/117.22 cnf(3290,plain, % 117.25/117.22 (P1(f5(f5(f5(a13))))), % 117.25/117.22 inference(scs_inference,[],[41,3098,3217,3164,3168,3219,3039,1209,3175,3187,2928,2888,2874,222,3054,27,47,45,49,48,52,46,44,11,17,15,7,9,12,13,8,10,4,14,16,6,5,2,66,21,67,43,42,3,22,23,24,25,18,104,71,96,95,50])). % 117.25/117.22 cnf(3292,plain, % 117.25/117.22 (E(f2(f3(a11,a13),f7(f3(a11,a13),f3(a11,a13))),f3(a11,a13))), % 117.25/117.22 inference(scs_inference,[],[41,3098,3217,3164,3168,3219,3039,1209,3175,3187,2928,2888,574,2874,222,562,3054,27,47,45,49,48,52,46,44,11,17,15,7,9,12,13,8,10,4,14,16,6,5,2,66,21,67,43,42,3,22,23,24,25,18,104,71,96,95,50,86])). % 117.25/117.22 cnf(3296,plain, % 117.25/117.22 (P2(f5(f5(f5(a13))))), % 117.25/117.22 inference(scs_inference,[],[41,3098,3217,3164,3168,3219,3173,3039,1209,3175,3187,2928,2888,574,2874,222,562,3054,27,47,45,49,48,52,46,44,11,17,15,7,9,12,13,8,10,4,14,16,6,5,2,66,21,67,43,42,3,22,23,24,25,18,104,71,96,95,50,86,78,51])). % 117.25/117.22 cnf(3312,plain, % 117.25/117.22 (E(f3(a10,a10),f3(f2(f3(a10,a10),f3(a10,a10)),f3(a10,a10)))), % 117.25/117.22 inference(scs_inference,[],[41,3098,3217,3126,3164,3168,3219,2908,3173,3039,1209,3175,3187,3103,2928,2888,1690,574,2874,1684,257,584,222,562,3054,29,312,133,30,27,47,45,49,48,52,46,44,11,17,15,7,9,12,13,8,10,4,14,16,6,5,2,66,21,67,43,42,3,22,23,24,25,18,104,71,96,95,50,86,78,51,77,105,61,65,58,83,75,499])). % 117.25/117.22 cnf(3313,plain, % 117.25/117.22 (E(f3(a11,f5(a13)),a14)), % 117.25/117.22 inference(scs_inference,[],[41,3098,3217,3126,3164,3168,3219,2908,3173,3039,1209,3175,3187,3103,2928,2888,1690,574,2874,1684,257,584,222,562,3054,29,312,133,30,27,47,45,49,48,52,46,44,11,17,15,7,9,12,13,8,10,4,14,16,6,5,2,66,21,67,43,42,3,22,23,24,25,18,104,71,96,95,50,86,78,51,77,105,61,65,58,83,75,499,450])). % 117.25/117.22 cnf(3319,plain, % 117.25/117.22 (P3(f3(a10,a10),f4(f3(a10,a10),f3(a10,a10)))), % 117.25/117.22 inference(scs_inference,[],[3269,265])). % 117.25/117.22 cnf(3320,plain, % 117.25/117.22 (P5(f3(a10,a10),f2(f3(a10,a10),f3(a10,a10)))), % 117.25/117.22 inference(scs_inference,[],[3266,497])). % 117.25/117.22 cnf(3321,plain, % 117.25/117.22 (E(f4(f3(a11,a13),a10),f3(a11,a13))), % 117.25/117.22 inference(scs_inference,[],[562,49])). % 117.25/117.22 cnf(3325,plain, % 117.25/117.22 (E(f4(a10,f3(a11,a13)),f3(a11,a13))), % 117.25/117.22 inference(scs_inference,[],[3041,562,49,45,47])). % 117.25/117.22 cnf(3327,plain, % 117.25/117.22 (E(f2(f3(a11,a13),a1),f3(a11,a13))), % 117.25/117.22 inference(scs_inference,[],[3041,562,49,45,47,48])). % 117.25/117.22 cnf(3331,plain, % 117.25/117.22 (E(f2(a1,f3(a11,a13)),f3(a11,a13))), % 117.25/117.22 inference(scs_inference,[],[3041,562,49,45,47,48,52,46])). % 117.25/117.22 cnf(3346,plain, % 117.25/117.22 (E(f2(f4(f5(a13),a1),x33461),f2(a1,x33461))), % 117.25/117.22 inference(scs_inference,[],[3041,3128,3292,562,49,45,47,48,52,46,450,15,11,44,17,13,9,12,7,10,8,14,4])). % 117.25/117.22 cnf(3349,plain, % 117.25/117.22 (E(f2(x33491,f4(f5(a13),a1)),f2(x33491,a1))), % 117.25/117.22 inference(scs_inference,[],[3041,3128,3292,562,49,45,47,48,52,46,450,15,11,44,17,13,9,12,7,10,8,14,4,6,16,5])). % 117.25/117.22 cnf(3351,plain, % 117.25/117.22 (P1(f2(f3(a11,a13),f3(a11,a13)))), % 117.25/117.22 inference(scs_inference,[],[2994,3041,3128,3292,562,49,45,47,48,52,46,450,15,11,44,17,13,9,12,7,10,8,14,4,6,16,5,2,66])). % 117.25/117.22 cnf(3353,plain, % 117.25/117.22 (~P3(f2(f5(a13),f3(a13,a13)),f4(a13,a12))), % 117.25/117.22 inference(scs_inference,[],[2994,3260,3041,3128,3292,2844,562,49,45,47,48,52,46,450,15,11,44,17,13,9,12,7,10,8,14,4,6,16,5,2,66,21])). % 117.25/117.22 cnf(3354,plain, % 117.25/117.22 (E(f2(f5(a13),x33541),f2(a13,x33541))), % 117.25/117.22 inference(rename_variables,[],[3260])). % 117.25/117.22 cnf(3355,plain, % 117.25/117.22 (~E(f5(f5(f5(a13))),a1)), % 117.25/117.22 inference(scs_inference,[],[2994,3260,3041,3128,3292,3290,3296,2844,562,49,45,47,48,52,46,450,15,11,44,17,13,9,12,7,10,8,14,4,6,16,5,2,66,21,42])). % 117.25/117.22 cnf(3357,plain, % 117.25/117.22 (P1(f4(f3(a11,a13),f3(a11,a13)))), % 117.25/117.22 inference(scs_inference,[],[2994,3260,3041,3128,3292,3290,3296,2844,562,49,45,47,48,52,46,450,15,11,44,17,13,9,12,7,10,8,14,4,6,16,5,2,66,21,42,67])). % 117.25/117.22 cnf(3359,plain, % 117.25/117.22 (~E(f5(f5(f5(a13))),a10)), % 117.25/117.22 inference(scs_inference,[],[2994,3260,3041,3128,3292,3290,3296,2844,562,49,45,47,48,52,46,450,15,11,44,17,13,9,12,7,10,8,14,4,6,16,5,2,66,21,42,67,43])). % 117.25/117.22 cnf(3362,plain, % 117.25/117.22 (~P3(a1,f2(f5(a13),f3(a13,a13)))), % 117.25/117.22 inference(scs_inference,[],[2994,3237,3260,3354,3041,3106,3128,3312,3292,3290,3296,2844,562,49,45,47,48,52,46,450,15,11,44,17,13,9,12,7,10,8,14,4,6,16,5,2,66,21,42,67,43,3,22])). % 117.25/117.22 cnf(3365,plain, % 117.25/117.22 (~P5(f2(a13,a14),f2(a14,f3(a14,a14)))), % 117.25/117.22 inference(scs_inference,[],[2994,3237,3260,3354,3041,3106,3128,3223,3312,3292,3290,3296,2844,692,149,562,49,45,47,48,52,46,450,15,11,44,17,13,9,12,7,10,8,14,4,6,16,5,2,66,21,42,67,43,3,22,23,24])). % 117.25/117.22 cnf(3366,plain, % 117.25/117.22 (~P5(f2(f2(a14,f7(a14,a14)),f7(a14,a14)),f3(a13,f5(a13)))), % 117.25/117.22 inference(scs_inference,[],[2994,3237,3254,3260,3354,3041,3106,3128,3049,3223,3312,3292,3290,3296,2844,692,149,562,49,45,47,48,52,46,450,15,11,44,17,13,9,12,7,10,8,14,4,6,16,5,2,66,21,42,67,43,3,22,23,24,25])). % 117.25/117.22 cnf(3367,plain, % 117.25/117.22 (E(f3(x33671,f5(a13)),f3(x33671,a13))), % 117.25/117.22 inference(rename_variables,[],[3254])). % 117.25/117.22 cnf(3368,plain, % 117.25/117.22 (~E(f4(f7(a1,a1),f7(a1,a1)),f4(a13,a12))), % 117.25/117.22 inference(scs_inference,[],[2994,3237,3254,3260,3354,3041,3106,3128,3049,3223,3312,3292,3290,3296,2844,692,149,2874,562,49,45,47,48,52,46,450,15,11,44,17,13,9,12,7,10,8,14,4,6,16,5,2,66,21,42,67,43,3,22,23,24,25,18])). % 117.25/117.22 cnf(3373,plain, % 117.25/117.22 (E(f2(f5(a13),f7(f5(a13),a13)),a13)), % 117.25/117.22 inference(scs_inference,[],[2994,3080,3237,3254,3260,3354,3041,3106,3128,3049,3223,3312,3292,3290,3296,2844,692,149,2874,562,3054,30,26,49,45,47,48,52,46,450,15,11,44,17,13,9,12,7,10,8,14,4,6,16,5,2,66,21,42,67,43,3,22,23,24,25,18,104,95,86])). % 117.25/117.22 cnf(3377,plain, % 117.25/117.22 (E(f4(f4(a1,a1),a1),f4(a1,f4(a1,a1)))), % 117.25/117.22 inference(scs_inference,[],[2994,3080,3237,3254,3260,3354,2990,3041,3106,3128,3049,3223,3312,3292,3290,3296,2844,2932,692,149,2874,562,323,3054,30,26,49,45,47,48,52,46,450,15,11,44,17,13,9,12,7,10,8,14,4,6,16,5,2,66,21,42,67,43,3,22,23,24,25,18,104,95,86,78,96])). % 117.25/117.22 cnf(3379,plain, % 117.25/117.22 (P1(f7(a13,f5(a13)))), % 117.25/117.22 inference(scs_inference,[],[2994,3227,3080,3237,3254,3260,3354,2990,3041,3106,3128,3049,3223,3312,3292,3290,3296,2844,2932,692,149,2874,562,323,3054,30,26,49,45,47,48,52,46,450,15,11,44,17,13,9,12,7,10,8,14,4,6,16,5,2,66,21,42,67,43,3,22,23,24,25,18,104,95,86,78,96,77])). % 117.25/117.22 cnf(3383,plain, % 117.25/117.22 (P5(a14,f2(a13,a14))), % 117.25/117.22 inference(scs_inference,[],[2994,3227,3080,3237,3254,3260,3354,2990,3041,3106,3128,3049,3223,3312,3292,3290,3296,2844,3168,2932,692,149,2874,562,323,519,3054,542,30,26,49,45,47,48,52,46,450,15,11,44,17,13,9,12,7,10,8,14,4,6,16,5,2,66,21,42,67,43,3,22,23,24,25,18,104,95,86,78,96,77,105,65])). % 117.25/117.22 cnf(3385,plain, % 117.25/117.22 (~E(f2(a14,f3(a14,a14)),f2(a11,f3(a11,a11)))), % 117.25/117.22 inference(scs_inference,[],[2994,3227,3080,3237,3254,3260,3354,2990,3041,3106,3128,3049,3223,3312,3292,3290,3296,2844,3168,2932,692,149,2874,562,630,298,323,519,3054,542,30,26,49,45,47,48,52,46,450,15,11,44,17,13,9,12,7,10,8,14,4,6,16,5,2,66,21,42,67,43,3,22,23,24,25,18,104,95,86,78,96,77,105,65,58])). % 117.25/117.22 cnf(3389,plain, % 117.25/117.22 (E(f2(a13,f3(f5(a13),f5(a13))),f5(a13))), % 117.25/117.22 inference(scs_inference,[],[2994,3227,3080,3237,3254,3367,3260,3354,2990,3041,3106,3128,3049,3223,3312,3292,3290,3296,2844,3168,2932,692,574,149,2874,562,630,298,323,519,3054,542,30,26,49,45,47,48,52,46,450,15,11,44,17,13,9,12,7,10,8,14,4,6,16,5,2,66,21,42,67,43,3,22,23,24,25,18,104,95,86,78,96,77,105,65,58,75,83])). % 117.25/117.22 cnf(3392,plain, % 117.25/117.22 (E(f3(a11,a13),f3(f2(f3(a11,a13),f3(a11,a13)),f3(a11,a13)))), % 117.25/117.22 inference(scs_inference,[],[2994,3227,3080,3237,3254,3367,3260,3354,2990,3041,3106,3128,3049,3223,3312,3292,3290,3296,2844,3168,2932,692,574,149,2874,562,630,298,323,519,3054,542,30,26,49,45,47,48,52,46,450,15,11,44,17,13,9,12,7,10,8,14,4,6,16,5,2,66,21,42,67,43,3,22,23,24,25,18,104,95,86,78,96,77,105,65,58,75,83,704])). % 117.25/117.22 cnf(3405,plain, % 117.25/117.22 (P5(f3(a11,a13),f2(f3(a11,a13),f3(a11,a13)))), % 117.25/117.22 inference(scs_inference,[],[3351,702])). % 117.25/117.22 cnf(3410,plain, % 117.25/117.22 (E(f4(f3(a11,a11),a10),f3(a11,a11))), % 117.25/117.22 inference(scs_inference,[],[3064,203,45,47,49])). % 117.25/117.22 cnf(3420,plain, % 117.25/117.22 (E(f4(f3(a11,a13),a10),a14)), % 117.25/117.22 inference(scs_inference,[],[3321,3064,203,45,47,49,48,52,46,44,450])). % 117.25/117.22 cnf(3435,plain, % 117.25/117.22 (~E(f4(a10,a13),f4(a13,a13))), % 117.25/117.22 inference(scs_inference,[],[3002,3321,3064,3313,203,45,47,49,48,52,46,44,450,11,15,17,12,13,10,9,7,8,16,4,14,6,5,2])). % 117.25/117.22 cnf(3436,plain, % 117.25/117.22 (P1(f2(f3(a11,a11),f3(a11,a11)))), % 117.25/117.22 inference(scs_inference,[],[3002,3321,3064,3313,203,45,47,49,48,52,46,44,450,11,15,17,12,13,10,9,7,8,16,4,14,6,5,2,66])). % 117.25/117.22 cnf(3438,plain, % 117.25/117.22 (P1(f4(f3(a11,a11),f3(a11,a11)))), % 117.25/117.22 inference(scs_inference,[],[3002,3321,3064,3313,203,45,47,49,48,52,46,44,450,11,15,17,12,13,10,9,7,8,16,4,14,6,5,2,66,67])). % 117.25/117.22 cnf(3440,plain, % 117.25/117.22 (~P3(f2(a10,f7(a10,a13)),f4(a13,a12))), % 117.25/117.22 inference(scs_inference,[],[41,3002,3321,3064,3313,3185,203,45,47,49,48,52,46,44,450,11,15,17,12,13,10,9,7,8,16,4,14,6,5,2,66,67,21])). % 117.25/117.22 cnf(3442,plain, % 117.25/117.22 (E(f4(f5(a13),x34421),f4(a13,x34421))), % 117.25/117.22 inference(rename_variables,[],[3258])). % 117.25/117.22 cnf(3443,plain, % 117.25/117.22 (~P3(f5(a13),f4(f5(a13),a12))), % 117.25/117.22 inference(scs_inference,[],[41,3000,3002,3268,3321,3258,3442,3064,3313,3185,203,45,47,49,48,52,46,44,450,11,15,17,12,13,10,9,7,8,16,4,14,6,5,2,66,67,21,3,22])). % 117.25/117.22 cnf(3447,plain, % 117.25/117.22 (E(f4(x34471,f5(a13)),f4(x34471,a13))), % 117.25/117.22 inference(rename_variables,[],[3255])). % 117.25/117.22 cnf(3450,plain, % 117.25/117.22 (~E(f7(f3(a13,a13),f3(a11,a13)),f4(a13,a12))), % 117.25/117.22 inference(scs_inference,[],[41,3000,3002,3268,3321,3255,3447,3258,3442,3064,3284,3313,194,3185,3233,3066,2874,203,45,47,49,48,52,46,44,450,11,15,17,12,13,10,9,7,8,16,4,14,6,5,2,66,67,21,3,22,23,24,25,18])). % 117.25/117.22 cnf(3457,plain, % 117.25/117.22 (~P1(f4(f5(a13),a12))), % 117.25/117.22 inference(scs_inference,[],[41,3000,3002,3268,3383,3321,3255,3447,3258,3442,3064,3193,3155,3284,3313,194,3185,3233,3066,409,2874,404,203,519,29,3054,542,45,47,49,48,52,46,44,450,11,15,17,12,13,10,9,7,8,16,4,14,6,5,2,66,67,21,3,22,23,24,25,18,60,86,77,110])). % 117.25/117.22 cnf(3459,plain, % 117.25/117.22 (P5(f2(a14,f3(a14,a14)),f2(a13,a14))), % 117.25/117.22 inference(scs_inference,[],[41,3000,3002,3268,3383,3321,3255,3447,3258,3442,3064,3193,3155,3365,3284,3313,194,3185,3233,3066,409,2874,630,404,203,519,29,3054,542,45,47,49,48,52,46,44,450,11,15,17,12,13,10,9,7,8,16,4,14,6,5,2,66,67,21,3,22,23,24,25,18,60,86,77,110,65])). % 117.25/117.22 cnf(3461,plain, % 117.25/117.22 (P5(f7(a13,f5(a13)),f7(f5(a13),f5(a13)))), % 117.25/117.22 inference(scs_inference,[],[41,3000,3002,3268,3383,3321,3255,3447,3256,3258,3442,3064,3193,3155,3189,3365,3284,3313,194,3379,3185,3233,3066,409,2874,630,404,203,519,29,3054,542,45,47,49,48,52,46,44,450,11,15,17,12,13,10,9,7,8,16,4,14,6,5,2,66,67,21,3,22,23,24,25,18,60,86,77,110,65,58])). % 117.25/117.22 cnf(3482,plain, % 117.25/117.22 (P5(f3(a11,a11),f2(f3(a11,a11),f3(a11,a11)))), % 117.25/117.22 inference(scs_inference,[],[3436,511])). % 117.25/117.22 cnf(3487,plain, % 117.25/117.22 (E(f4(f3(a14,a14),a10),f3(a14,a14))), % 117.25/117.22 inference(scs_inference,[],[3269,567,45,47,49])). % 117.25/117.22 cnf(3497,plain, % 117.25/117.22 (E(f4(a10,f3(a11,a13)),a14)), % 117.25/117.22 inference(scs_inference,[],[3325,3269,567,45,47,49,48,52,46,44,450])). % 117.25/117.22 cnf(3512,plain, % 117.25/117.22 (~E(f4(a13,a1),f4(a13,a13))), % 117.25/117.22 inference(scs_inference,[],[3213,3325,3269,3420,567,45,47,49,48,52,46,44,450,11,17,12,13,15,8,9,10,16,7,14,6,4,5,2])). % 117.25/117.22 cnf(3513,plain, % 117.25/117.22 (P1(f2(f3(a14,a14),f3(a14,a14)))), % 117.25/117.22 inference(scs_inference,[],[3213,3325,3269,3420,567,45,47,49,48,52,46,44,450,11,17,12,13,15,8,9,10,16,7,14,6,4,5,2,66])). % 117.25/117.22 cnf(3522,plain, % 117.25/117.22 (~P5(f2(a13,a14),f5(a13))), % 117.25/117.22 inference(scs_inference,[],[3213,3325,3264,3262,3269,3443,3420,3392,3211,3280,2966,149,567,579,45,47,49,48,52,46,44,450,11,17,12,13,15,8,9,10,16,7,14,6,4,5,2,66,67,21,3,22,23,24])). % 117.25/117.22 cnf(3524,plain, % 117.25/117.22 (E(f3(f5(a13),x35241),f3(a13,x35241))), % 117.25/117.22 inference(rename_variables,[],[3263])). % 117.25/117.22 cnf(3536,plain, % 117.25/117.22 (P5(f3(a13,a13),f2(a13,a14))), % 117.25/117.22 inference(scs_inference,[],[3213,3325,3263,3264,3262,3269,3351,3405,3457,3443,3420,3392,3211,3280,3366,683,738,2966,3164,409,149,298,404,562,567,519,3054,376,579,45,47,49,48,52,46,44,450,11,17,12,13,15,8,9,10,16,7,14,6,4,5,2,66,67,21,3,22,23,24,25,18,60,86,77,112,110,65])). % 117.25/117.22 cnf(3538,plain, % 117.25/117.22 (P5(f5(a13),f5(f5(a13)))), % 117.25/117.22 inference(scs_inference,[],[3213,3325,3263,3264,3262,3269,3351,3405,3457,3443,3420,3392,3211,3280,3366,683,738,2966,3175,3164,409,149,298,404,562,567,519,3054,376,579,45,47,49,48,52,46,44,450,11,17,12,13,15,8,9,10,16,7,14,6,4,5,2,66,67,21,3,22,23,24,25,18,60,86,77,112,110,65,58])). % 117.25/117.22 cnf(3542,plain, % 117.25/117.22 (E(f2(f5(a13),f3(f5(a13),f5(a13))),a13)), % 117.25/117.22 inference(scs_inference,[],[3213,3325,3263,3524,3264,3262,3269,3351,3405,3457,3201,3159,3443,3420,3392,3211,3280,3366,683,3080,738,2966,3175,3164,409,149,298,404,562,567,519,3054,376,579,30,45,47,49,48,52,46,44,450,11,17,12,13,15,8,9,10,16,7,14,6,4,5,2,66,67,21,3,22,23,24,25,18,60,86,77,112,110,65,58,62,83])). % 117.25/117.22 cnf(3552,plain, % 117.25/117.22 (P5(f3(a14,a14),f2(f3(a14,a14),f3(a14,a14)))), % 117.25/117.22 inference(scs_inference,[],[3092,3213,3325,3263,3524,3264,3262,3269,3351,3405,3457,3201,3159,3443,3420,3392,3211,3280,3366,3046,3043,683,3126,3080,738,2944,2966,3175,3164,409,149,298,404,562,567,519,3054,376,579,30,45,47,49,48,52,46,44,450,11,17,12,13,15,8,9,10,16,7,14,6,4,5,2,66,67,21,3,22,23,24,25,18,60,86,77,112,110,65,58,62,83,718,85,54,118,111])). % 117.25/117.22 cnf(3560,plain, % 117.25/117.22 (E(f4(a10,f2(a13,a14)),f2(a13,a14))), % 117.25/117.22 inference(scs_inference,[],[3357,519,45,47])). % 117.25/117.22 cnf(3570,plain, % 117.25/117.22 (E(f2(f3(a11,a13),a1),a14)), % 117.25/117.22 inference(scs_inference,[],[3327,3357,519,45,47,49,52,48,46,450])). % 117.25/117.22 cnf(3587,plain, % 117.25/117.22 (~E(f3(a13,a10),f4(a13,a12))), % 117.25/117.22 inference(scs_inference,[],[3205,3327,3357,3497,519,45,47,49,52,48,46,450,44,11,12,13,15,17,16,7,8,9,10,6,14,4,5,2])). % 117.25/117.22 cnf(3588,plain, % 117.25/117.22 (P1(f2(f2(a13,a14),f2(a13,a14)))), % 117.25/117.22 inference(scs_inference,[],[3205,3327,3357,3497,519,45,47,49,52,48,46,450,44,11,12,13,15,17,16,7,8,9,10,6,14,4,5,2,66])). % 117.25/117.22 cnf(3597,plain, % 117.25/117.22 (~E(f5(a13),f3(f4(a1,f2(a1,a1)),a1))), % 117.25/117.22 inference(scs_inference,[],[41,3265,3205,3353,3327,3357,3497,1692,2833,3542,3258,3066,519,45,47,49,52,48,46,450,44,11,12,13,15,17,16,7,8,9,10,6,14,4,5,2,66,67,21,3,22,23])). % 117.25/117.22 cnf(3599,plain, % 117.25/117.22 (E(f7(x35991,f5(a13)),f7(x35991,a13))), % 117.25/117.22 inference(rename_variables,[],[3257])). % 117.25/117.22 cnf(3607,plain, % 117.25/117.22 (P3(f5(a13),f4(f5(a13),f5(a13)))), % 117.25/117.22 inference(scs_inference,[],[41,3265,3536,3205,3353,3327,3257,3599,3357,3497,3461,1692,2833,3542,3258,3457,3159,3066,519,3054,376,45,47,49,52,48,46,450,44,11,12,13,15,17,16,7,8,9,10,6,14,4,5,2,66,67,21,3,22,23,24,25,18,86,77,110])). % 117.25/117.22 cnf(3611,plain, % 117.25/117.22 (P5(f5(a13),f2(a13,a14))), % 117.25/117.22 inference(scs_inference,[],[41,3265,3536,3205,3522,3353,3327,3257,3599,3357,3497,3461,1692,2833,3542,3258,3457,3159,3066,519,3054,376,45,47,49,52,48,46,450,44,11,12,13,15,17,16,7,8,9,10,6,14,4,5,2,66,67,21,3,22,23,24,25,18,86,77,110,112,65])). % 117.25/117.22 cnf(3613,plain, % 117.25/117.22 (~E(f5(a13),f2(a13,a14))), % 117.25/117.22 inference(scs_inference,[],[41,3265,3536,3205,3522,3353,3327,3257,3599,3357,3497,3461,1692,2833,3542,3258,3457,3159,3066,519,3054,376,45,47,49,52,48,46,450,44,11,12,13,15,17,16,7,8,9,10,6,14,4,5,2,66,67,21,3,22,23,24,25,18,86,77,110,112,65,58])). % 117.25/117.22 cnf(3619,plain, % 117.25/117.22 (E(f5(a13),f9(f4(f5(a13),f5(a13)),f5(a13)))), % 117.25/117.22 inference(scs_inference,[],[41,3265,3536,3205,3522,3353,3241,3327,3257,3599,3195,3357,730,3497,3461,1692,2833,3542,3258,3457,3159,3066,3164,298,519,3054,376,188,27,45,47,49,52,48,46,450,44,11,12,13,15,17,16,7,8,9,10,6,14,4,5,2,66,67,21,3,22,23,24,25,18,86,77,110,112,65,58,70,83,121])). % 117.25/117.22 cnf(3631,plain, % 117.25/117.22 (P5(f2(a13,a14),f2(f2(a13,a14),f2(a13,a14)))), % 117.25/117.22 inference(scs_inference,[],[3588,645])). % 117.25/117.22 cnf(3634,plain, % 117.25/117.22 (E(f4(a10,a12),a12)), % 117.25/117.22 inference(scs_inference,[],[3438,29,45,47])). % 117.25/117.22 cnf(3638,plain, % 117.25/117.22 (E(f4(a12,a10),a12)), % 117.25/117.22 inference(scs_inference,[],[3438,29,45,47,52,49])). % 117.25/117.22 cnf(3640,plain, % 117.25/117.22 (E(f2(a12,a1),a12)), % 117.25/117.22 inference(scs_inference,[],[3438,29,45,47,52,49,48])). % 117.25/117.22 cnf(3642,plain, % 117.25/117.22 (E(f2(a1,a12),a12)), % 117.25/117.22 inference(scs_inference,[],[3438,29,45,47,52,49,48,46])). % 117.25/117.22 cnf(3646,plain, % 117.25/117.22 (E(f2(a1,f3(a11,a13)),a14)), % 117.25/117.22 inference(scs_inference,[],[3331,3438,29,45,47,52,49,48,46,44,450])). % 117.25/117.22 cnf(3661,plain, % 117.25/117.22 (~E(f4(a13,a12),f5(a13))), % 117.25/117.22 inference(scs_inference,[],[3170,3331,3438,3570,29,45,47,52,49,48,46,44,450,11,15,12,13,17,7,9,16,8,6,10,14,4,5,2])). % 117.25/117.22 cnf(3662,plain, % 117.25/117.22 (P1(f2(a12,a12))), % 117.25/117.22 inference(scs_inference,[],[3170,3331,3438,3570,29,45,47,52,49,48,46,44,450,11,15,12,13,17,7,9,16,8,6,10,14,4,5,2,66])). % 117.25/117.22 cnf(3664,plain, % 117.25/117.22 (P1(f4(a12,a12))), % 117.25/117.22 inference(scs_inference,[],[3170,3331,3438,3570,29,45,47,52,49,48,46,44,450,11,15,12,13,17,7,9,16,8,6,10,14,4,5,2,66,67])). % 117.25/117.22 cnf(3666,plain, % 117.25/117.22 (~P3(f4(a10,f5(a13)),f4(a13,a12))), % 117.25/117.22 inference(scs_inference,[],[3170,3331,3130,3438,3570,3268,29,45,47,52,49,48,46,44,450,11,15,12,13,17,7,9,16,8,6,10,14,4,5,2,66,67,21])). % 117.25/117.22 cnf(3669,plain, % 117.25/117.22 (~E(f5(f5(a13)),f3(f3(a1,a1),f3(a1,a1)))), % 117.25/117.22 inference(scs_inference,[],[3170,3331,3130,3438,3570,3268,3207,178,3392,3187,29,45,47,52,49,48,46,44,450,11,15,12,13,17,7,9,16,8,6,10,14,4,5,2,66,67,21,3,22,23])). % 117.25/117.22 cnf(3670,plain, % 117.25/117.22 (~P5(f2(f5(a13),f2(a14,f7(a14,a14))),a14)), % 117.25/117.22 inference(scs_inference,[],[3170,3331,3130,3438,3570,3278,3268,3207,3260,178,3392,3187,29,45,47,52,49,48,46,44,450,11,15,12,13,17,7,9,16,8,6,10,14,4,5,2,66,67,21,3,22,23,24])). % 117.25/117.22 cnf(3679,plain, % 117.25/117.22 (P1(f7(f3(a12,a12),f3(a12,a12)))), % 117.25/117.22 inference(scs_inference,[],[3170,3611,3331,3130,3438,3570,3278,3268,3207,709,3254,3260,178,3392,3457,3187,338,3164,323,29,519,3054,45,47,52,49,48,46,44,450,11,15,12,13,17,7,9,16,8,6,10,14,4,5,2,66,67,21,3,22,23,24,25,18,71,86,77])). % 117.25/117.22 cnf(3691,plain, % 117.25/117.22 (E(f2(a10,f3(f5(a13),a10)),a13)), % 117.25/117.22 inference(scs_inference,[],[2836,3170,3611,3613,3331,3130,3438,3482,3570,3278,3436,3268,3207,709,3254,3260,3263,178,3392,3058,3457,732,3187,720,338,3164,714,323,203,29,519,3054,376,542,28,30,27,45,47,52,49,48,46,44,450,11,15,12,13,17,7,9,16,8,6,10,14,4,5,2,66,67,21,3,22,23,24,25,18,71,86,77,65,58,80,70,120,83])). % 117.25/117.22 cnf(3694,plain, % 117.25/117.22 (P5(f2(f3(a13,a13),f3(f3(a13,a13),f3(a13,a13))),a11)), % 117.25/117.22 inference(scs_inference,[],[2836,3170,3611,3613,3331,3130,3438,3482,3570,3278,3436,3268,3207,709,3254,3260,3263,178,3392,3058,3457,732,3187,720,338,3164,714,323,203,29,519,3054,376,542,28,30,27,45,47,52,49,48,46,44,450,11,15,12,13,17,7,9,16,8,6,10,14,4,5,2,66,67,21,3,22,23,24,25,18,71,86,77,65,58,80,70,120,83,1908])). % 117.25/117.22 cnf(3700,plain, % 117.25/117.22 (P3(a12,f4(a12,a12))), % 117.25/117.22 inference(scs_inference,[],[3664,364])). % 117.25/117.22 cnf(3701,plain, % 117.25/117.22 (P5(a12,f2(a12,a12))), % 117.25/117.22 inference(scs_inference,[],[3662,536])). % 117.25/117.22 cnf(3704,plain, % 117.25/117.22 (E(a12,f3(f2(a12,a12),a12))+~P5(a12,f2(a12,a12))), % 117.25/117.22 inference(scs_inference,[],[3662,2449])). % 117.25/117.22 cnf(3712,plain, % 117.25/117.22 (E(f4(f2(a12,a12),a1),a1)), % 117.25/117.22 inference(scs_inference,[],[3662,47,45])). % 117.25/117.22 cnf(3729,plain, % 117.25/117.22 (E(f4(x37291,f4(a10,a12)),f4(x37291,a12))), % 117.25/117.22 inference(scs_inference,[],[3662,3634,47,45,49,52,48,46,44,15,13,12,17,11,9])). % 117.25/117.22 cnf(3730,plain, % 117.25/117.22 (E(f3(x37301,f4(a10,a12)),f3(x37301,a12))), % 117.25/117.22 inference(scs_inference,[],[3662,3634,47,45,49,52,48,46,44,15,13,12,17,11,9,7])). % 117.25/117.22 cnf(3734,plain, % 117.25/117.22 (E(f3(f4(a10,a12),x37341),f3(a12,x37341))), % 117.25/117.22 inference(scs_inference,[],[3662,3634,47,45,49,52,48,46,44,15,13,12,17,11,9,7,8,16,10,6])). % 117.25/117.22 cnf(3739,plain, % 117.25/117.22 (P1(f2(f2(a12,a12),f2(a12,a12)))), % 117.25/117.22 inference(scs_inference,[],[3662,2892,3634,47,45,49,52,48,46,44,15,13,12,17,11,9,7,8,16,10,6,14,4,5,2,66])). % 117.25/117.22 cnf(3741,plain, % 117.25/117.22 (P1(f4(f2(a12,a12),f2(a12,a12)))), % 117.25/117.22 inference(scs_inference,[],[3662,2892,3634,47,45,49,52,48,46,44,15,13,12,17,11,9,7,8,16,10,6,14,4,5,2,66,67])). % 117.25/117.22 cnf(3749,plain, % 117.25/117.22 (~P5(f2(a1,f3(a11,a13)),f3(a13,a13))), % 117.25/117.22 inference(scs_inference,[],[41,3662,3435,2892,3634,3666,3646,1708,3373,3255,3258,3066,698,47,45,49,52,48,46,44,15,13,12,17,11,9,7,8,16,10,6,14,4,5,2,66,67,21,3,22,23,24])). % 117.25/117.22 cnf(3756,plain, % 117.25/117.22 (P5(f3(a13,a13),a14)), % 117.25/117.22 inference(scs_inference,[],[41,3662,3435,2892,3634,3666,3646,3377,1708,3373,3255,2240,3258,3457,3066,698,376,542,47,45,49,52,48,46,44,15,13,12,17,11,9,7,8,16,10,6,14,4,5,2,66,67,21,3,22,23,24,25,18,77,86,65])). % 117.25/117.22 cnf(3785,plain, % 117.25/117.22 (E(a12,f3(f2(a12,a12),a12))), % 117.25/117.22 inference(scs_inference,[],[3701,3704])). % 117.25/117.22 cnf(3806,plain, % 117.25/117.22 (E(f4(x38061,f4(a12,a10)),f4(x38061,a12))), % 117.25/117.22 inference(scs_inference,[],[3638,3513,3664,47,52,45,49,48,46,44,15,12,17,11,13,8,9])). % 117.25/117.22 cnf(3838,plain, % 117.25/117.22 (~E(f2(a14,f3(a14,a14)),f2(a13,a14))), % 117.25/117.22 inference(scs_inference,[],[41,3700,3701,3199,3638,3749,3729,3132,3513,3346,3664,3365,3443,3263,3457,3662,630,29,423,519,47,52,45,49,48,46,44,15,12,17,11,13,8,9,7,10,16,14,6,4,5,2,67,66,3,21,22,24,25,18,85,78,77,86,110,58])). % 117.25/117.22 cnf(3847,plain, % 117.25/117.22 (P3(a12,f2(f4(a12,a12),f4(a12,a12)))), % 117.25/117.22 inference(scs_inference,[],[41,3700,3701,3199,3638,3749,3729,3730,3132,3513,3346,3664,3365,3443,3263,3102,3457,3662,630,29,423,519,30,26,47,52,45,49,48,46,44,15,12,17,11,13,8,9,7,10,16,14,6,4,5,2,67,66,3,21,22,24,25,18,85,78,77,86,110,58,72,75,83,97])). % 117.25/117.22 cnf(3853,plain, % 117.25/117.22 (~P3(f2(f2(a13,a14),f3(f2(a13,a14),f2(a13,a14))),f5(a13))), % 117.25/117.22 inference(scs_inference,[],[41,3700,3701,3199,3638,3749,3729,3730,3132,3513,3346,3664,3365,3443,3280,3263,3193,3102,3058,3155,3457,2929,3164,3662,584,630,29,423,519,3054,30,27,26,47,52,45,49,48,46,44,15,12,17,11,13,8,9,7,10,16,14,6,4,5,2,67,66,3,21,22,24,25,18,85,78,77,86,110,58,72,75,83,97,98,50,69])). % 117.25/117.22 cnf(3857,plain, % 117.25/117.22 (~P5(a13,f2(a10,f3(a10,a10)))), % 117.25/117.22 inference(scs_inference,[],[41,3700,3701,3199,3638,3749,3729,3730,3132,3513,3045,3346,3664,3365,3443,3103,3280,569,3263,3193,3102,3058,3155,3457,2929,3164,3662,257,584,630,562,29,423,519,3054,376,30,27,26,47,52,45,49,48,46,44,15,12,17,11,13,8,9,7,10,16,14,6,4,5,2,67,66,3,21,22,24,25,18,85,78,77,86,110,58,72,75,83,97,98,50,69,80,74])). % 117.25/117.22 cnf(3861,plain, % 117.25/117.22 (~E(a11,f2(a10,f3(a10,a10)))), % 117.25/117.22 inference(scs_inference,[],[41,3700,3701,3199,3638,3749,3729,3730,3132,3513,3045,3346,3664,3365,3443,3103,3280,569,3263,3193,3102,3058,3155,3457,2929,3164,2938,3662,257,584,630,562,29,423,519,3054,376,30,27,26,47,52,45,49,48,46,44,15,12,17,11,13,8,9,7,10,16,14,6,4,5,2,67,66,3,21,22,24,25,18,85,78,77,86,110,58,72,75,83,97,98,50,69,80,74,81,144])). % 117.25/117.22 cnf(3864,plain, % 117.25/117.22 (~P5(f2(f2(a13,a14),f3(f2(a13,a14),f2(a13,a14))),a10)), % 117.25/117.22 inference(scs_inference,[],[3857,1261])). % 117.25/117.22 cnf(3867,plain, % 117.25/117.22 (E(f4(a10,f3(a13,a13)),f3(a13,a13))), % 117.25/117.22 inference(scs_inference,[],[3588,376,52,47])). % 117.25/117.22 cnf(3869,plain, % 117.25/117.22 (E(f4(f3(a13,a13),a10),f3(a13,a13))), % 117.25/117.22 inference(scs_inference,[],[3588,376,52,47,49])). % 117.25/117.22 cnf(3871,plain, % 117.25/117.22 (E(f2(f3(a13,a13),a1),f3(a13,a13))), % 117.25/117.22 inference(scs_inference,[],[3588,376,52,47,49,48])). % 117.25/117.22 cnf(3875,plain, % 117.25/117.22 (E(f2(a1,f3(a13,a13)),f3(a13,a13))), % 117.25/117.22 inference(scs_inference,[],[3588,376,52,47,49,48,45,46])). % 117.25/117.22 cnf(3885,plain, % 117.25/117.22 (E(f3(x38851,f2(a12,a1)),f3(x38851,a12))), % 117.25/117.22 inference(scs_inference,[],[3640,3588,376,52,47,49,48,45,46,44,15,11,12,13,17,8,7])). % 117.25/117.22 cnf(3886,plain, % 117.25/117.22 (E(f4(x38861,f2(a12,a1)),f4(x38861,a12))), % 117.25/117.22 inference(scs_inference,[],[3640,3588,376,52,47,49,48,45,46,44,15,11,12,13,17,8,7,9])). % 117.25/117.22 cnf(3894,plain, % 117.25/117.22 (P1(f2(f3(a13,a13),f3(a13,a13)))), % 117.25/117.22 inference(scs_inference,[],[3640,3450,3588,376,52,47,49,48,45,46,44,15,11,12,13,17,8,7,9,10,4,6,14,16,5,2,66])). % 117.25/117.22 cnf(3896,plain, % 117.25/117.22 (P1(f4(f3(a13,a13),f3(a13,a13)))), % 117.25/117.22 inference(scs_inference,[],[3640,3450,3588,376,52,47,49,48,45,46,44,15,11,12,13,17,8,7,9,10,4,6,14,16,5,2,66,67])). % 117.25/117.22 cnf(3898,plain, % 117.25/117.22 (~E(f4(a13,f3(f3(a1,a1),a1)),f4(a13,a13))), % 117.25/117.22 inference(scs_inference,[],[3512,3640,3450,3588,2824,376,52,47,49,48,45,46,44,15,11,12,13,17,8,7,9,10,4,6,14,16,5,2,66,67,3])). % 117.25/117.22 cnf(3904,plain, % 117.25/117.22 (~P5(f2(a13,a14),f2(f5(a13),a1))), % 117.25/117.22 inference(scs_inference,[],[41,3512,3640,3450,3806,3134,3588,3785,2824,3691,3522,3701,376,52,47,49,48,45,46,44,15,11,12,13,17,8,7,9,10,4,6,14,16,5,2,66,67,3,21,22,24,25])). % 117.25/117.22 cnf(3908,plain, % 117.25/117.22 (P1(f7(f3(a10,a10),f3(a10,a10)))), % 117.25/117.22 inference(scs_inference,[],[41,3756,3512,3640,3450,3806,3134,3588,3785,2824,3691,3522,3701,233,3457,222,376,542,52,47,49,48,45,46,44,15,11,12,13,17,8,7,9,10,4,6,14,16,5,2,66,67,3,21,22,24,25,18,86,77])). % 117.25/117.22 cnf(3910,plain, % 117.25/117.22 (~P3(f2(a11,f3(a11,a11)),a13)), % 117.25/117.22 inference(scs_inference,[],[41,3756,3512,3640,3450,3806,3134,3588,3785,2824,3691,378,3522,3701,233,3457,2938,298,222,376,542,30,52,47,49,48,45,46,44,15,11,12,13,17,8,7,9,10,4,6,14,16,5,2,66,67,3,21,22,24,25,18,86,77,69])). % 117.25/117.22 cnf(3912,plain, % 117.25/117.22 (~P5(a11,f2(f3(a13,a13),f3(f3(a13,a13),f3(a13,a13))))), % 117.25/117.22 inference(scs_inference,[],[41,3756,3512,3640,3450,3806,3134,3588,3785,3694,2831,2824,3691,378,3522,3701,233,3457,2938,398,298,222,376,542,28,30,52,47,49,48,45,46,44,15,11,12,13,17,8,7,9,10,4,6,14,16,5,2,66,67,3,21,22,24,25,18,86,77,69,74])). % 117.25/117.22 cnf(3931,plain, % 117.25/117.22 (P5(f3(a13,a13),f2(f3(a13,a13),f3(a13,a13)))), % 117.25/117.22 inference(scs_inference,[],[3894,622])). % 117.25/117.22 cnf(3932,plain, % 117.25/117.22 (E(f4(a10,a14),a14)), % 117.25/117.22 inference(scs_inference,[],[542,47])). % 117.25/117.22 cnf(3938,plain, % 117.25/117.22 (E(f2(a14,a1),a14)), % 117.25/117.22 inference(scs_inference,[],[3679,542,47,52,45,48])). % 117.25/117.22 cnf(3940,plain, % 117.25/117.22 (E(f4(a14,a10),a14)), % 117.25/117.22 inference(scs_inference,[],[3679,542,47,52,45,48,49])). % 117.25/117.22 cnf(3942,plain, % 117.25/117.22 (E(f2(a1,a14),a14)), % 117.25/117.22 inference(scs_inference,[],[3679,542,47,52,45,48,49,46])). % 117.25/117.22 cnf(3952,plain, % 117.25/117.22 (E(f4(x39521,f2(a1,a12)),f4(x39521,a12))), % 117.25/117.22 inference(scs_inference,[],[3642,3679,542,47,52,45,48,49,46,44,15,13,11,17,8,12,9])). % 117.25/117.22 cnf(3953,plain, % 117.25/117.22 (E(f3(x39531,f2(a1,a12)),f3(x39531,a12))), % 117.25/117.22 inference(scs_inference,[],[3642,3679,542,47,52,45,48,49,46,44,15,13,11,17,8,12,9,7])). % 117.25/117.22 cnf(3957,plain, % 117.25/117.22 (E(f3(f2(a1,a12),x39571),f3(a12,x39571))), % 117.25/117.22 inference(scs_inference,[],[3642,3679,542,47,52,45,48,49,46,44,15,13,11,17,8,12,9,7,16,10,14,6])). % 117.25/117.22 cnf(3961,plain, % 117.25/117.22 (P1(f4(a14,a14))), % 117.25/117.22 inference(scs_inference,[],[3642,3368,3679,542,47,52,45,48,49,46,44,15,13,11,17,8,12,9,7,16,10,14,6,4,5,2,67])). % 117.25/117.22 cnf(3963,plain, % 117.25/117.22 (P1(f2(a14,a14))), % 117.25/117.23 inference(scs_inference,[],[3642,3368,3679,542,47,52,45,48,49,46,44,15,13,11,17,8,12,9,7,16,10,14,6,4,5,2,67,66])). % 117.25/117.23 cnf(3966,plain, % 117.25/117.23 (~P3(f2(a1,f5(a13)),f4(a13,a12))), % 117.25/117.23 inference(scs_inference,[],[3642,3368,3136,3679,3785,3268,542,47,52,45,48,49,46,44,15,13,11,17,8,12,9,7,16,10,14,6,4,5,2,67,66,3,21])). % 117.25/117.23 cnf(3967,plain, % 117.25/117.23 (~P3(a13,f4(a13,f2(a12,a1)))), % 117.25/117.23 inference(scs_inference,[],[41,3642,3368,3886,3136,3679,3785,3268,542,47,52,45,48,49,46,44,15,13,11,17,8,12,9,7,16,10,14,6,4,5,2,67,66,3,21,22])). % 117.25/117.23 cnf(3987,plain, % 117.25/117.23 (E(a13,f5(a13))), % 117.25/117.23 inference(scs_inference,[],[41,3642,3368,3459,3560,3886,3136,3679,3904,3349,3864,3912,3785,3211,3359,3355,3227,3268,3080,3193,3290,3155,269,3175,3457,3164,398,584,630,203,519,3054,542,28,30,27,47,52,45,48,49,46,44,15,13,11,17,8,12,9,7,16,10,14,6,4,5,2,67,66,3,21,22,24,25,18,54,86,61,77,65,58,69,74])). % 117.25/117.23 cnf(3995,plain, % 117.25/117.23 (E(a14,f3(f2(a14,a14),a14))), % 117.25/117.23 inference(scs_inference,[],[41,3642,3368,3459,3487,3560,3886,3136,3679,3904,3349,3864,3597,3912,3320,3785,3211,3359,3355,3266,3227,3268,3080,3193,3290,563,3155,1170,269,3175,3457,3164,398,584,630,222,203,1166,519,3054,542,28,30,27,26,47,52,45,48,49,46,44,15,13,11,17,8,12,9,7,16,10,14,6,4,5,2,67,66,3,21,22,24,25,18,54,86,61,77,65,58,69,74,75,83,89,672])). % 117.25/117.23 cnf(4000,plain, % 117.25/117.23 (P5(f2(a12,a12),f2(f2(a12,a12),f2(a12,a12)))), % 117.25/117.23 inference(scs_inference,[],[41,3642,3368,3459,3487,3560,3886,3136,3679,3739,3904,3349,3864,3597,3912,3756,3320,3785,3211,3359,3355,3266,3227,3268,3080,3201,3193,3290,563,3155,3159,1170,269,3175,3457,3164,398,584,3662,630,222,203,1166,519,3054,376,542,28,30,27,26,47,52,45,48,49,46,44,15,13,11,17,8,12,9,7,16,10,14,6,4,5,2,67,66,3,21,22,24,25,18,54,86,61,77,65,58,69,74,75,83,89,672,51,118,111])). % 117.25/117.23 cnf(4004,plain, % 117.25/117.23 (P3(a14,f4(a14,a14))), % 117.25/117.23 inference(scs_inference,[],[3961,572])). % 117.25/117.23 cnf(4005,plain, % 117.25/117.23 (P5(a14,f2(a14,a14))), % 117.25/117.23 inference(scs_inference,[],[3963,670])). % 117.25/117.23 cnf(4008,plain, % 117.25/117.23 (P5(f4(a14,a14),f4(a14,a14))), % 117.25/117.23 inference(scs_inference,[],[3961,47,52])). % 117.25/117.23 cnf(4027,plain, % 117.25/117.23 (E(f4(x40271,f4(a10,a14)),f4(x40271,a14))), % 117.25/117.23 inference(scs_inference,[],[3961,3932,47,52,45,48,49,46,44,15,11,13,8,12,17,7,9])). % 117.25/117.23 cnf(4040,plain, % 117.25/117.23 (E(f4(x40401,f2(a1,a12)),f4(x40401,a12))), % 117.25/117.23 inference(rename_variables,[],[3952])). % 117.25/117.23 cnf(4043,plain, % 117.25/117.23 (~P3(a13,f4(a13,f2(a1,a12)))), % 117.25/117.23 inference(scs_inference,[],[41,3961,3587,3932,3281,3966,3952,4040,3346,47,52,45,48,49,46,44,15,11,13,8,12,17,7,9,10,4,16,14,6,5,2,67,66,3,21,22])). % 117.25/117.23 cnf(4046,plain, % 117.25/117.23 (~P5(f4(a10,a14),f3(a13,a13))), % 117.25/117.23 inference(scs_inference,[],[41,3961,3587,3932,3281,3966,3952,4040,3670,3346,698,47,52,45,48,49,46,44,15,11,13,8,12,17,7,9,10,4,16,14,6,5,2,67,66,3,21,22,25,24])). % 117.25/117.23 cnf(4052,plain, % 117.25/117.23 (P1(f3(f4(a14,a14),f4(a14,a14)))), % 117.25/117.23 inference(scs_inference,[],[41,3961,3587,3932,3281,3966,3952,4040,3552,3670,3346,3513,698,3457,567,47,52,45,48,49,46,44,15,11,13,8,12,17,7,9,10,4,16,14,6,5,2,67,66,3,21,22,25,24,18,86,77,112])). % 117.25/117.23 cnf(4063,plain, % 117.25/117.23 (~E(f4(f5(a13),f5(a13)),f4(f5(a13),a1))), % 117.25/117.23 inference(scs_inference,[],[41,3961,3587,3932,3281,3966,3838,3952,4040,3953,3552,3670,3346,3864,3173,3513,3175,698,3457,3164,584,630,567,29,519,3054,312,27,26,47,52,45,48,49,46,44,15,11,13,8,12,17,7,9,10,4,16,14,6,5,2,67,66,3,21,22,25,24,18,86,77,112,58,69,80,83,81])). % 117.25/117.23 cnf(4075,plain, % 117.25/117.23 (E(f2(a12,a12),f3(f2(f2(a12,a12),f2(a12,a12)),f2(a12,a12)))), % 117.25/117.23 inference(scs_inference,[],[41,3961,3587,3932,3281,3966,3838,3952,4040,3953,3552,4000,3538,3669,3670,3273,3271,3739,3346,3864,3173,3513,3175,154,698,3457,3164,584,3662,630,567,29,519,3054,312,133,27,26,47,52,45,48,49,46,44,15,11,13,8,12,17,7,9,10,4,16,14,6,5,2,67,66,3,21,22,25,24,18,86,77,112,58,69,80,83,81,89,87,71,54,118,120])). % 117.25/117.23 cnf(4086,plain, % 117.25/117.23 (P5(f2(a14,a14),f2(a14,a14))), % 117.25/117.23 inference(scs_inference,[],[3963,47,52])). % 117.25/117.23 cnf(4113,plain, % 117.25/117.23 (P1(f4(f2(a14,a14),f2(a14,a14)))), % 117.25/117.23 inference(scs_inference,[],[3963,3938,3053,47,52,45,48,49,46,44,15,13,11,17,12,8,7,9,4,10,6,16,14,5,2,67])). % 117.25/117.23 cnf(4115,plain, % 117.25/117.23 (P1(f2(f2(a14,a14),f2(a14,a14)))), % 117.25/117.23 inference(scs_inference,[],[3963,3938,3053,47,52,45,48,49,46,44,15,13,11,17,12,8,7,9,4,10,6,16,14,5,2,67,66])). % 117.25/117.23 cnf(4118,plain, % 117.25/117.23 (P3(f3(f2(a14,a14),a14),f4(a14,a14))), % 117.25/117.23 inference(scs_inference,[],[3963,4004,3938,3053,3995,47,52,45,48,49,46,44,15,13,11,17,12,8,7,9,4,10,6,16,14,5,2,67,66,3,21])). % 117.25/117.23 cnf(4121,plain, % 117.25/117.23 (~P5(f4(a10,f4(a10,a14)),f3(a13,a13))), % 117.25/117.23 inference(scs_inference,[],[3963,4004,4046,3938,3987,3053,3867,4027,3995,3853,47,52,45,48,49,46,44,15,13,11,17,12,8,7,9,4,10,6,16,14,5,2,67,66,3,21,22,25,24])). % 117.25/117.23 cnf(4130,plain, % 117.25/117.23 (P1(f3(f2(a14,a14),a14))), % 117.25/117.23 inference(scs_inference,[],[3963,4004,4005,4046,3938,3987,3053,3867,4027,3995,3853,3457,3961,542,47,52,45,48,49,46,44,15,13,11,17,12,8,7,9,4,10,6,16,14,5,2,67,66,3,21,22,25,24,18,85,86,77,112])). % 117.25/117.23 cnf(4132,plain, % 117.25/117.23 (P5(f3(f2(a14,a14),a14),a14)), % 117.25/117.23 inference(scs_inference,[],[3963,4004,4005,4046,3938,3987,3053,3867,4027,3995,3853,3457,3961,542,47,52,45,48,49,46,44,15,13,11,17,12,8,7,9,4,10,6,16,14,5,2,67,66,3,21,22,25,24,18,85,86,77,112,58])). % 117.25/117.23 cnf(4136,plain, % 117.25/117.23 (~E(f2(a14,a14),f3(a13,a13))), % 117.25/117.23 inference(scs_inference,[],[3963,4004,4005,4046,3938,3987,3053,3867,4027,3861,3995,3853,698,3457,3961,257,376,542,28,47,52,45,48,49,46,44,15,13,11,17,12,8,7,9,4,10,6,16,14,5,2,67,66,3,21,22,25,24,18,85,86,77,112,58,79,73])). % 117.25/117.23 cnf(4147,plain, % 117.25/117.23 (P3(a14,f2(f4(a14,a14),f4(a14,a14)))), % 117.25/117.23 inference(scs_inference,[],[3963,4004,4005,4046,3938,3987,3053,3867,3957,4027,3861,3995,4063,3853,3607,3159,698,3457,3164,3961,257,29,3054,376,312,542,28,26,47,52,45,48,49,46,44,15,13,11,17,12,8,7,9,4,10,6,16,14,5,2,67,66,3,21,22,25,24,18,85,86,77,112,58,79,73,75,83,82,84,97])). % 117.25/117.23 cnf(4166,plain, % 117.25/117.23 (E(f4(a10,a11),a11)), % 117.25/117.23 inference(scs_inference,[],[28,47])). % 117.25/117.23 cnf(4172,plain, % 117.25/117.23 (E(f2(a11,a1),a11)), % 117.25/117.23 inference(scs_inference,[],[3741,28,47,45,52,48])). % 117.25/117.23 cnf(4174,plain, % 117.25/117.23 (E(f4(a11,a10),a11)), % 117.25/117.23 inference(scs_inference,[],[3741,28,47,45,52,48,49])). % 117.25/117.23 cnf(4176,plain, % 117.25/117.23 (E(f2(a1,a11),a11)), % 117.25/117.23 inference(scs_inference,[],[3741,28,47,45,52,48,49,46])). % 117.25/117.23 cnf(4186,plain, % 117.25/117.23 (E(f4(f4(a14,a10),x41861),f4(a14,x41861))), % 117.25/117.23 inference(scs_inference,[],[3940,3741,28,47,45,52,48,49,46,44,15,13,17,11,7,12,8])). % 117.25/117.23 cnf(4195,plain, % 117.25/117.23 (P1(f4(a11,a11))), % 117.25/117.23 inference(scs_inference,[],[4136,3940,3741,28,47,45,52,48,49,46,44,15,13,17,11,7,12,8,9,6,4,10,14,16,5,2,67])). % 117.25/117.23 cnf(4197,plain, % 117.25/117.23 (P1(f2(a11,a11))), % 117.25/117.23 inference(scs_inference,[],[4136,3940,3741,28,47,45,52,48,49,46,44,15,13,17,11,7,12,8,9,6,4,10,14,16,5,2,67,66])). % 117.25/117.23 cnf(4205,plain, % 117.25/117.23 (~P5(f4(a14,a10),f3(a13,a13))), % 117.25/117.23 inference(scs_inference,[],[4136,3940,3869,3440,3741,3276,439,3952,3185,3670,3066,698,28,47,45,52,48,49,46,44,15,13,17,11,7,12,8,9,6,4,10,14,16,5,2,67,66,21,3,22,23,25,24])). % 117.25/117.23 cnf(4206,plain, % 117.25/117.23 (~E(f4(f2(a12,a12),f2(a12,a12)),f4(a13,a12))), % 117.25/117.23 inference(scs_inference,[],[4136,3940,3869,3440,3741,3276,439,3952,3185,3670,3066,698,2874,28,47,45,52,48,49,46,44,15,13,17,11,7,12,8,9,6,4,10,14,16,5,2,67,66,21,3,22,23,25,24,18])). % 117.25/117.23 cnf(4219,plain, % 117.25/117.23 (~E(f4(a13,a12),f3(f4(a14,a14),f4(a14,a14)))), % 117.25/117.23 inference(scs_inference,[],[4008,4086,4136,3940,3869,3440,3741,3276,4130,4132,439,3952,3631,3185,3670,3103,3045,3280,3588,3066,698,3664,2874,3963,3961,257,584,519,3054,376,542,28,30,47,45,52,48,49,46,44,15,13,17,11,7,12,8,9,6,4,10,14,16,5,2,67,66,21,3,22,23,25,24,18,86,77,58,79,70,120,75])). % 117.25/117.23 cnf(4229,plain, % 117.25/117.23 (E(a11,f3(f2(a11,a11),a11))), % 117.25/117.23 inference(scs_inference,[],[4008,4086,4136,3940,3247,3869,4118,3440,3741,3276,4130,4132,439,3952,3631,3185,3670,3103,3045,3280,3588,3066,698,3664,2874,3164,3963,3961,257,366,584,519,3054,376,542,188,28,30,27,47,45,52,48,49,46,44,15,13,17,11,7,12,8,9,6,4,10,14,16,5,2,67,66,21,3,22,23,25,24,18,86,77,58,79,70,120,75,83,81,97,89,251])). % 117.25/117.23 cnf(4238,plain, % 117.25/117.23 (P3(a11,f4(a11,a11))), % 117.25/117.23 inference(scs_inference,[],[4195,211])). % 117.25/117.23 cnf(4239,plain, % 117.25/117.23 (P5(a11,f2(a11,a11))), % 117.25/117.23 inference(scs_inference,[],[4197,247])). % 117.25/117.23 cnf(4240,plain, % 117.25/117.23 (P1(f4(f4(a11,a11),a10))), % 117.25/117.23 inference(scs_inference,[],[4195,1761])). % 117.25/117.23 cnf(4241,plain, % 117.25/117.23 (P3(f4(a11,a11),f4(a11,a11))), % 117.25/117.23 inference(scs_inference,[],[4195,1769])). % 117.25/117.23 cnf(4242,plain, % 117.25/117.23 (P3(f4(a11,a11),f4(f4(a11,a11),a10))), % 117.25/117.23 inference(scs_inference,[],[4195,1771])). % 117.25/117.23 cnf(4243,plain, % 117.25/117.23 (P3(f4(f4(a11,a11),a10),f4(a11,a11))), % 117.25/117.23 inference(scs_inference,[],[4195,1772])). % 117.25/117.23 cnf(4252,plain, % 117.25/117.23 (P5(f4(a11,a11),f4(a11,a11))), % 117.25/117.23 inference(scs_inference,[],[4195,4197,47,45,48,49,52])). % 117.25/117.23 cnf(4264,plain, % 117.25/117.23 (E(f4(f2(a1,a14),x42641),f4(a14,x42641))), % 117.25/117.23 inference(scs_inference,[],[4195,4197,3942,47,45,48,49,52,46,44,15,13,17,11,7,12,8])). % 117.25/117.23 cnf(4280,plain, % 117.25/117.23 (~P5(f4(a14,a10),f2(f3(a13,a13),a1))), % 117.25/117.23 inference(scs_inference,[],[4195,4197,4205,3942,4206,3871,3362,3712,2858,3124,3847,47,45,48,49,52,46,44,15,13,17,11,7,12,8,9,4,6,10,14,16,5,2,67,66,21,3,22,25])). % 117.25/117.23 cnf(4281,plain, % 117.25/117.23 (~P5(f4(f4(a14,a10),a10),f3(a13,a13))), % 117.25/117.23 inference(scs_inference,[],[4195,4197,4205,3942,4206,3871,4186,3362,3712,2858,3124,3847,47,45,48,49,52,46,44,15,13,17,11,7,12,8,9,4,6,10,14,16,5,2,67,66,21,3,22,25,24])). % 117.25/117.23 cnf(4308,plain, % 117.25/117.23 (P3(a11,f4(a11,a11))), % 117.25/117.23 inference(scs_inference,[],[4240,1753])). % 117.25/117.23 cnf(4335,plain, % 117.25/117.23 (E(f2(f4(a10,a11),x43351),f2(a11,x43351))), % 117.25/117.23 inference(scs_inference,[],[4166,3894,4197,133,47,48,45,49,52,46,44,15,17,11,13,7,12,8,9,10,6,4])). % 117.25/117.23 cnf(4340,plain, % 117.25/117.23 (P1(f4(f2(a11,a11),f2(a11,a11)))), % 117.25/117.23 inference(scs_inference,[],[4166,2943,3894,4197,133,47,48,45,49,52,46,44,15,17,11,13,7,12,8,9,10,6,4,14,16,5,2,67])). % 117.25/117.23 cnf(4342,plain, % 117.25/117.23 (P1(f2(f2(a11,a11),f2(a11,a11)))), % 117.25/117.23 inference(scs_inference,[],[4166,2943,3894,4197,133,47,48,45,49,52,46,44,15,17,11,13,7,12,8,9,10,6,4,14,16,5,2,67,66])). % 117.25/117.23 cnf(4351,plain, % 117.25/117.23 (~E(f2(f3(a13,a13),f3(a13,a13)),f4(a13,a12))), % 117.25/117.23 inference(scs_inference,[],[3661,4166,2943,3875,4281,3894,4043,3157,3389,4197,3349,3912,3258,2874,133,47,48,45,49,52,46,44,15,17,11,13,7,12,8,9,10,6,4,14,16,5,2,67,66,21,3,22,25,24,18])). % 117.25/117.23 cnf(4360,plain, % 117.25/117.23 (P3(f2(a11,a11),f4(f2(a11,a11),f2(a11,a11)))), % 117.25/117.23 inference(scs_inference,[],[4238,4239,4241,4252,3661,4166,2943,3875,4281,3894,4043,3157,3389,4197,3349,3912,3258,4195,2874,28,133,47,48,45,49,52,46,44,15,17,11,13,7,12,8,9,10,6,4,14,16,5,2,67,66,21,3,22,25,24,18,85,78,77,86,110])). % 117.25/117.23 cnf(4376,plain, % 117.25/117.23 (P5(f2(a11,a11),f2(f2(a11,a11),f2(a11,a11)))), % 117.25/117.23 inference(scs_inference,[],[4238,4239,4241,4252,3661,4166,2943,3875,4243,3885,4281,3894,3931,4242,4240,4043,3157,3385,3389,4197,3349,3912,650,3258,1744,4195,2874,630,298,29,376,312,28,133,47,48,45,49,52,46,44,15,17,11,13,7,12,8,9,10,6,4,14,16,5,2,67,66,21,3,22,25,24,18,85,78,77,86,110,58,70,75,83,88,450,42,111])). % 117.25/117.23 cnf(4390,plain, % 117.25/117.23 (E(f4(a13,a10),a13)), % 117.25/117.23 inference(scs_inference,[],[3896,133,30,47,45,48,52,49])). % 117.25/117.23 cnf(4392,plain, % 117.25/117.23 (E(f2(a1,a13),a13)), % 117.25/117.23 inference(scs_inference,[],[3896,133,30,47,45,48,52,49,46])). % 117.25/117.23 cnf(4400,plain, % 117.25/117.23 (E(f3(x44001,f4(a11,a10)),f3(x44001,a11))), % 117.25/117.23 inference(scs_inference,[],[4174,3896,133,30,47,45,48,52,49,46,44,15,17,11,13,7])). % 117.25/117.23 cnf(4413,plain, % 117.25/117.23 (P1(f2(f3(a1,a1),f3(a1,a1)))), % 117.25/117.23 inference(scs_inference,[],[4174,4351,3896,133,30,47,45,48,52,49,46,44,15,17,11,13,7,8,12,9,10,6,14,4,16,5,2,67,66])). % 117.25/117.23 cnf(4415,plain, % 117.25/117.23 (~P3(f2(f4(a10,a11),f3(a11,a11)),a13)), % 117.25/117.23 inference(scs_inference,[],[4174,4351,4335,3896,3910,133,30,47,45,48,52,49,46,44,15,17,11,13,7,8,12,9,10,6,14,4,16,5,2,67,66,21])). % 117.25/117.23 cnf(4423,plain, % 117.25/117.23 (P5(a10,f5(a13))), % 117.25/117.23 inference(scs_inference,[],[4174,4351,4264,4121,4335,3896,4229,4280,4147,2962,3161,3869,3910,3457,3164,3054,133,30,47,45,48,52,49,46,44,15,17,11,13,7,8,12,9,10,6,14,4,16,5,2,67,66,21,3,22,25,24,18,54])). % 117.25/117.23 cnf(4435,plain, % 117.25/117.23 (P1(f9(f4(f5(a13),f5(a13)),f5(a13)))), % 117.25/117.23 inference(scs_inference,[],[4308,4174,4351,4264,4121,4335,3896,4342,4376,4229,4280,4147,2962,3161,2260,4241,3869,3910,3607,585,3159,4197,337,3457,4195,3164,567,3054,28,133,30,26,47,45,48,52,49,46,44,15,17,11,13,7,8,12,9,10,6,14,4,16,5,2,67,66,21,3,22,25,24,18,54,85,78,86,77,58,113])). % 117.25/117.23 cnf(4454,plain, % 117.25/117.23 (P5(f3(a1,a1),f2(f3(a1,a1),f3(a1,a1)))), % 117.25/117.23 inference(scs_inference,[],[4413,267])). % 117.25/117.23 cnf(4455,plain, % 117.25/117.23 (E(f4(a10,a13),a13)), % 117.25/117.23 inference(scs_inference,[],[30,47])). % 117.25/117.23 cnf(4459,plain, % 117.25/117.23 (E(f2(a13,a1),a13)), % 117.25/117.23 inference(scs_inference,[],[3908,30,47,45,48])). % 117.25/117.23 cnf(4461,plain, % 117.25/117.23 (E(f4(a10,a10),a10)), % 117.25/117.23 inference(scs_inference,[],[3908,30,27,47,45,48,49])). % 117.25/117.23 cnf(4484,plain, % 117.25/117.23 (P1(f4(a13,a13))), % 117.25/117.23 inference(scs_inference,[],[4172,3908,4219,30,27,47,45,48,49,52,46,44,15,17,11,13,7,8,12,10,14,9,6,4,16,5,2,67])). % 117.25/117.23 cnf(4486,plain, % 117.25/117.23 (P1(f2(a13,a13))), % 117.25/117.23 inference(scs_inference,[],[4172,3908,4219,30,27,47,45,48,49,52,46,44,15,17,11,13,7,8,12,10,14,9,6,4,16,5,2,67,66])). % 117.25/117.23 cnf(4488,plain, % 117.25/117.23 (~P3(f4(a13,a10),f4(a13,a12))), % 117.25/117.23 inference(scs_inference,[],[41,4172,4390,3908,4219,30,27,47,45,48,49,52,46,44,15,17,11,13,7,8,12,10,14,9,6,4,16,5,2,67,66,21])). % 117.25/117.23 cnf(4500,plain, % 117.25/117.23 (~E(f2(f4(a13,a13),f4(a13,a13)),a1)), % 117.25/117.23 inference(scs_inference,[],[41,4172,3154,4390,3908,4219,3967,169,2960,2994,3092,2888,1208,3912,3258,3066,2874,3054,30,27,47,45,48,49,52,46,44,15,17,11,13,7,8,12,10,14,9,6,4,16,5,2,67,66,21,3,22,23,25,24,18,85,71,60])). % 117.25/117.23 cnf(4502,plain, % 117.25/117.23 (~E(f2(f2(a13,a13),f2(a13,a13)),a1)), % 117.25/117.23 inference(scs_inference,[],[41,4172,3154,4390,3908,4219,3967,169,2960,2994,3092,2888,1208,3912,3258,3066,2874,3054,30,27,47,45,48,49,52,46,44,15,17,11,13,7,8,12,10,14,9,6,4,16,5,2,67,66,21,3,22,23,25,24,18,85,71,60,61])). % 117.25/117.23 cnf(4512,plain, % 117.25/117.23 (P5(f5(a13),f2(a13,a13))), % 117.25/117.23 inference(scs_inference,[],[41,2948,4172,3154,4390,3908,4340,4360,4219,3967,169,2960,2994,3092,2888,1208,3912,3258,3066,4197,2874,3164,3054,30,27,47,45,48,49,52,46,44,15,17,11,13,7,8,12,10,14,9,6,4,16,5,2,67,66,21,3,22,23,25,24,18,85,71,60,61,78,86,77,119,69])). % 117.25/117.23 cnf(4524,plain, % 117.25/117.23 (~P5(a13,a10)), % 117.25/117.23 inference(scs_inference,[],[41,2948,4172,3154,4390,3410,3908,4340,4360,4219,2946,3967,169,2936,2960,2994,3092,2888,1208,3912,3258,3066,4197,2874,3164,489,199,3054,28,30,27,26,47,45,48,49,52,46,44,15,17,11,13,7,8,12,10,14,9,6,4,16,5,2,67,66,21,3,22,23,25,24,18,85,71,60,61,78,86,77,119,69,62,74,75,83,81,1314])). % 117.25/117.23 cnf(4525,plain, % 117.25/117.23 (~P5(f2(a13,a14),a10)), % 117.25/117.23 inference(scs_inference,[],[41,2948,4172,3154,4390,3410,3908,4340,4360,4219,2946,3967,169,2936,2960,2994,3092,2888,1208,3912,3258,3066,4197,2874,3164,489,199,3054,28,30,27,26,47,45,48,49,52,46,44,15,17,11,13,7,8,12,10,14,9,6,4,16,5,2,67,66,21,3,22,23,25,24,18,85,71,60,61,78,86,77,119,69,62,74,75,83,81,1314,1319])). % 117.25/117.23 cnf(4526,plain, % 117.25/117.23 (~E(a11,a10)), % 117.25/117.23 inference(scs_inference,[],[41,2948,4172,3154,4390,3410,3908,4340,4360,4219,2946,3967,169,2936,2960,2994,3092,2888,1208,3912,3258,3066,4197,2874,3164,489,199,3054,28,30,27,26,47,45,48,49,52,46,44,15,17,11,13,7,8,12,10,14,9,6,4,16,5,2,67,66,21,3,22,23,25,24,18,85,71,60,61,78,86,77,119,69,62,74,75,83,81,1314,1319,144])). % 117.25/117.23 cnf(4539,plain, % 117.25/117.23 (P3(a13,f4(a13,a13))), % 117.25/117.23 inference(scs_inference,[],[4484,416])). % 117.25/117.23 cnf(4540,plain, % 117.25/117.23 (P5(a13,f2(a13,a13))), % 117.25/117.23 inference(scs_inference,[],[4486,600])). % 117.25/117.23 cnf(4542,plain, % 117.25/117.23 (~P5(a11,a10)), % 117.25/117.23 inference(scs_inference,[],[4524,1264])). % 117.25/117.23 cnf(4553,plain, % 117.25/117.23 (P5(f4(a13,a13),f4(a13,a13))), % 117.25/117.23 inference(scs_inference,[],[4484,47,48,45,52])). % 117.25/117.23 cnf(4575,plain, % 117.25/117.23 (~E(a10,a11)), % 117.25/117.23 inference(scs_inference,[],[4526,4484,4176,47,48,45,52,49,46,44,15,17,11,13,8,7,12,10,9,14,16,6,4,5,2])). % 117.25/117.23 cnf(4583,plain, % 117.25/117.23 (~P5(a13,f4(a10,a10))), % 117.25/117.23 inference(scs_inference,[],[41,4524,4526,4484,4176,4392,4461,4415,4229,47,48,45,52,49,46,44,15,17,11,13,8,7,12,10,9,14,16,6,4,5,2,67,66,21,3,22,25])). % 117.25/117.23 cnf(4600,plain, % 117.25/117.23 (P5(f4(f4(a11,a11),a10),f4(a11,a11))), % 117.25/117.23 inference(scs_inference,[],[41,4524,4526,4484,4486,4525,4423,4176,4512,4392,4461,3319,4500,4415,4229,2994,4240,3269,1745,3457,4195,222,519,3054,27,47,48,45,52,49,46,44,15,17,11,13,8,7,12,10,9,14,16,6,4,5,2,67,66,21,3,22,25,24,18,71,60,78,112,86,77,65,58])). % 117.25/117.23 cnf(4615,plain, % 117.25/117.23 (~E(a11,f4(a10,a10))), % 117.25/117.23 inference(scs_inference,[],[41,4524,4526,4484,4486,4525,4423,4176,4512,4392,4461,4400,3319,4500,4415,4239,4229,40,2970,2994,4240,569,3269,1745,35,2960,4197,3457,4195,222,562,519,376,3054,542,28,27,26,47,48,45,52,49,46,44,15,17,11,13,8,7,12,10,9,14,16,6,4,5,2,67,66,21,3,22,25,24,18,71,60,78,112,86,77,65,58,62,83,75,82,98,100,144])). % 117.25/117.23 cnf(4664,plain, % 117.25/117.23 (~E(f4(f2(a14,a14),f2(a14,a14)),f4(a13,a12))), % 117.25/117.23 inference(scs_inference,[],[41,4575,4488,4583,4615,4455,4052,4113,3886,4486,378,2874,253,47,48,45,49,52,46,44,15,17,11,13,7,8,12,10,6,4,16,9,14,5,2,67,66,21,3,22,25,24,18])). % 117.25/117.23 cnf(4688,plain, % 117.25/117.23 (~P3(a11,a13)), % 117.25/117.23 inference(scs_inference,[],[41,4542,4575,4539,4540,4553,4488,4583,4615,4455,4600,3734,4052,4113,4413,4454,4502,4435,3619,131,3213,3886,4526,4486,378,4240,2994,31,2938,2874,4484,4195,253,29,3054,312,28,133,30,27,47,48,45,49,52,46,44,15,17,11,13,7,8,12,10,6,4,16,9,14,5,2,67,66,21,3,22,25,24,18,71,86,112,77,65,58,62,75,83,121,84,68])). % 117.25/117.23 cnf(4714,plain, % 117.25/117.23 (~E(a13,f2(f4(a13,a12),f4(a14,a12)))), % 117.25/117.23 inference(scs_inference,[],[4688,478])). % 117.25/117.23 cnf(4725,plain, % 117.25/117.23 (E(f2(a1,a1),a1)), % 117.25/117.23 inference(scs_inference,[],[4115,27,26,47,45,48,49,52,46])). % 117.25/117.23 cnf(4746,plain, % 117.25/117.23 (P1(f2(a10,a10))), % 117.25/117.23 inference(scs_inference,[],[4459,4664,4115,27,26,47,45,48,49,52,46,44,15,11,17,13,7,8,12,10,6,4,16,9,14,5,2,67,66])). % 117.25/117.23 cnf(4807,plain, % 117.25/117.23 (E(a10,f3(f2(a10,a10),a10))), % 117.25/117.23 inference(scs_inference,[],[4746,1661])). % 117.25/117.23 cnf(5723,plain, % 117.25/117.23 ($false), % 117.25/117.23 inference(scs_inference,[],[27,30,556,29,423,2874,3164,3940,4725,2950,484,4807,4539,3701,3995,3268,122,4075,4229,4714,3987,3898,2,9,162,180,144,132,143,18,24,25,22,3,21,23,67]), % 117.25/117.23 ['proof']). % 117.25/117.23 % SZS output end Proof % 117.25/117.23 % Total time :116.530000s %------------------------------------------------------------------------------