%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM449+6 : 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 : n025.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:19 EDT 2024 % Result : Theorem 58.89s 59.08s % Output : CNFRefutation 58.89s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NUM449+6 : TPTP v8.2.0. Released v4.0.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n025.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Sun Jun 23 04:02:09 EDT 2024 % 0.12/0.34 % CPUTime : % 0.21/0.57 start to proof:theBenchmark % 58.89/59.05 %------------------------------------------- % 58.89/59.05 % File :CSE---1.7 % 58.89/59.05 % Problem :theBenchmark % 58.89/59.05 % Transform :cnf % 58.89/59.05 % Format :tptp:raw % 58.89/59.05 % Command :java -jar mcs_scs.jar %d %s % 58.89/59.05 % 58.89/59.05 % Result :Theorem 58.290000s % 58.89/59.05 % Output :CNFRefutation 58.290000s % 58.89/59.05 %------------------------------------------- % 58.89/59.06 %------------------------------------------------------------------------------ % 58.89/59.06 % File : NUM449+6 : TPTP v8.2.0. Released v4.0.0. % 58.89/59.06 % Domain : Number Theory % 58.89/59.06 % Problem : Fuerstenberg's infinitude of primes 11_02, 05 expansion % 58.89/59.06 % Version : Especial. % 58.89/59.06 % English : % 58.89/59.06 % 58.89/59.06 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 58.89/59.06 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 58.89/59.07 % Source : [Pas08] % 58.89/59.07 % Names : fuerst_11_02.05 [Pas08] % 58.89/59.07 % 58.89/59.07 % Status : Theorem % 58.89/59.07 % Rating : 0.44 v8.2.0, 0.39 v8.1.0, 0.33 v7.5.0, 0.44 v7.4.0, 0.27 v7.3.0, 0.31 v7.2.0, 0.28 v7.1.0, 0.30 v7.0.0, 0.37 v6.4.0, 0.38 v6.3.0, 0.33 v6.2.0, 0.40 v6.1.0, 0.50 v6.0.0, 0.43 v5.5.0, 0.63 v5.4.0, 0.68 v5.3.0, 0.70 v5.2.0, 0.65 v5.1.0, 0.76 v5.0.0, 0.79 v4.1.0, 0.83 v4.0.1, 0.87 v4.0.0 % 58.89/59.07 % Syntax : Number of formulae : 45 ( 3 unt; 10 def) % 58.89/59.07 % Number of atoms : 267 ( 53 equ) % 58.89/59.07 % Maximal formula atoms : 38 ( 5 avg) % 58.89/59.07 % Number of connectives : 241 ( 19 ~; 12 |; 124 &) % 58.89/59.07 % ( 21 <=>; 65 =>; 0 <=; 0 <~>) % 58.89/59.07 % Maximal formula depth : 19 ( 7 avg) % 58.89/59.07 % Maximal term depth : 3 ( 1 avg) % 58.89/59.07 % Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty) % 58.89/59.07 % Number of functors : 14 ( 14 usr; 6 con; 0-2 aty) % 58.89/59.07 % Number of variables : 111 ( 96 !; 15 ?) % 58.89/59.07 % SPC : FOF_THM_RFO_SEQ % 58.89/59.07 % 58.89/59.07 % Comments : Problem generated by the SAD system [VLP07] % 58.89/59.07 %------------------------------------------------------------------------------ % 58.89/59.07 fof(mIntegers,axiom, % 58.89/59.07 ! [W0] : % 58.89/59.07 ( aInteger0(W0) % 58.89/59.07 => $true ) ). % 58.89/59.07 % 58.89/59.07 fof(mIntZero,axiom, % 58.89/59.07 aInteger0(sz00) ). % 58.89/59.07 % 58.89/59.07 fof(mIntOne,axiom, % 58.89/59.07 aInteger0(sz10) ). % 58.89/59.07 % 58.89/59.07 fof(mIntNeg,axiom, % 58.89/59.07 ! [W0] : % 58.89/59.07 ( aInteger0(W0) % 58.89/59.07 => aInteger0(smndt0(W0)) ) ). % 58.89/59.07 % 58.89/59.07 fof(mIntPlus,axiom, % 58.89/59.07 ! [W0,W1] : % 58.89/59.07 ( ( aInteger0(W0) % 58.89/59.07 & aInteger0(W1) ) % 58.89/59.07 => aInteger0(sdtpldt0(W0,W1)) ) ). % 58.89/59.07 % 58.89/59.07 fof(mIntMult,axiom, % 58.89/59.07 ! [W0,W1] : % 58.89/59.07 ( ( aInteger0(W0) % 58.89/59.07 & aInteger0(W1) ) % 58.89/59.07 => aInteger0(sdtasdt0(W0,W1)) ) ). % 58.89/59.07 % 58.89/59.07 fof(mAddAsso,axiom, % 58.89/59.07 ! [W0,W1,W2] : % 58.89/59.07 ( ( aInteger0(W0) % 58.89/59.07 & aInteger0(W1) % 58.89/59.07 & aInteger0(W2) ) % 58.89/59.07 => sdtpldt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtpldt0(W0,W1),W2) ) ). % 58.89/59.07 % 58.89/59.07 fof(mAddComm,axiom, % 58.89/59.07 ! [W0,W1] : % 58.89/59.07 ( ( aInteger0(W0) % 58.89/59.07 & aInteger0(W1) ) % 58.89/59.07 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 58.89/59.07 % 58.89/59.07 fof(mAddZero,axiom, % 58.89/59.07 ! [W0] : % 58.89/59.07 ( aInteger0(W0) % 58.89/59.07 => ( sdtpldt0(W0,sz00) = W0 % 58.89/59.07 & W0 = sdtpldt0(sz00,W0) ) ) ). % 58.89/59.07 % 58.89/59.07 fof(mAddNeg,axiom, % 58.89/59.07 ! [W0] : % 58.89/59.07 ( aInteger0(W0) % 58.89/59.07 => ( sdtpldt0(W0,smndt0(W0)) = sz00 % 58.89/59.07 & sz00 = sdtpldt0(smndt0(W0),W0) ) ) ). % 58.89/59.07 % 58.89/59.07 fof(mMulAsso,axiom, % 58.89/59.07 ! [W0,W1,W2] : % 58.89/59.07 ( ( aInteger0(W0) % 58.89/59.07 & aInteger0(W1) % 58.89/59.07 & aInteger0(W2) ) % 58.89/59.07 => sdtasdt0(W0,sdtasdt0(W1,W2)) = sdtasdt0(sdtasdt0(W0,W1),W2) ) ). % 58.89/59.07 % 58.89/59.07 fof(mMulComm,axiom, % 58.89/59.07 ! [W0,W1] : % 58.89/59.07 ( ( aInteger0(W0) % 58.89/59.07 & aInteger0(W1) ) % 58.89/59.07 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 58.89/59.07 % 58.89/59.07 fof(mMulOne,axiom, % 58.89/59.07 ! [W0] : % 58.89/59.07 ( aInteger0(W0) % 58.89/59.07 => ( sdtasdt0(W0,sz10) = W0 % 58.89/59.07 & W0 = sdtasdt0(sz10,W0) ) ) ). % 58.89/59.07 % 58.89/59.07 fof(mDistrib,axiom, % 58.89/59.07 ! [W0,W1,W2] : % 58.89/59.07 ( ( aInteger0(W0) % 58.89/59.07 & aInteger0(W1) % 58.89/59.07 & aInteger0(W2) ) % 58.89/59.07 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 58.89/59.07 & sdtasdt0(sdtpldt0(W0,W1),W2) = sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W1,W2)) ) ) ). % 58.89/59.07 % 58.89/59.07 fof(mMulZero,axiom, % 58.89/59.07 ! [W0] : % 58.89/59.07 ( aInteger0(W0) % 58.89/59.07 => ( sdtasdt0(W0,sz00) = sz00 % 58.89/59.07 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 58.89/59.07 % 58.89/59.07 fof(mMulMinOne,axiom, % 58.89/59.07 ! [W0] : % 58.89/59.07 ( aInteger0(W0) % 58.89/59.07 => ( sdtasdt0(smndt0(sz10),W0) = smndt0(W0) % 58.89/59.07 & smndt0(W0) = sdtasdt0(W0,smndt0(sz10)) ) ) ). % 58.89/59.07 % 58.89/59.07 fof(mZeroDiv,axiom, % 58.89/59.07 ! [W0,W1] : % 58.89/59.07 ( ( aInteger0(W0) % 58.89/59.07 & aInteger0(W1) ) % 58.89/59.07 => ( sdtasdt0(W0,W1) = sz00 % 58.89/59.07 => ( W0 = sz00 % 58.89/59.07 | W1 = sz00 ) ) ) ). % 58.89/59.07 % 58.89/59.07 fof(mDivisor,definition, % 58.89/59.07 ! [W0] : % 58.89/59.07 ( aInteger0(W0) % 58.89/59.07 => ! [W1] : % 58.89/59.07 ( aDivisorOf0(W1,W0) % 58.89/59.07 <=> ( aInteger0(W1) % 58.89/59.07 & W1 != sz00 % 58.89/59.07 & ? [W2] : % 58.89/59.07 ( aInteger0(W2) % 58.89/59.07 & sdtasdt0(W1,W2) = W0 ) ) ) ) ). % 58.89/59.07 % 58.89/59.07 fof(mEquMod,definition, % 58.89/59.07 ! [W0,W1,W2] : % 58.89/59.07 ( ( aInteger0(W0) % 58.89/59.07 & aInteger0(W1) % 58.89/59.07 & aInteger0(W2) % 58.89/59.07 & W2 != sz00 ) % 58.89/59.07 => ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 58.89/59.07 <=> aDivisorOf0(W2,sdtpldt0(W0,smndt0(W1))) ) ) ). % 58.89/59.07 % 58.89/59.07 fof(mEquModRef,axiom, % 58.89/59.07 ! [W0,W1] : % 58.89/59.07 ( ( aInteger0(W0) % 58.89/59.07 & aInteger0(W1) % 58.89/59.07 & W1 != sz00 ) % 58.89/59.07 => sdteqdtlpzmzozddtrp0(W0,W0,W1) ) ). % 58.89/59.07 % 58.89/59.07 fof(mEquModSym,axiom, % 58.89/59.07 ! [W0,W1,W2] : % 58.89/59.07 ( ( aInteger0(W0) % 58.89/59.07 & aInteger0(W1) % 58.89/59.07 & aInteger0(W2) % 58.89/59.07 & W2 != sz00 ) % 58.89/59.07 => ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 58.89/59.07 => sdteqdtlpzmzozddtrp0(W1,W0,W2) ) ) ). % 58.89/59.07 % 58.89/59.07 fof(mEquModTrn,axiom, % 58.89/59.07 ! [W0,W1,W2,W3] : % 58.89/59.07 ( ( aInteger0(W0) % 58.89/59.07 & aInteger0(W1) % 58.89/59.07 & aInteger0(W2) % 58.89/59.07 & W2 != sz00 % 58.89/59.07 & aInteger0(W3) ) % 58.89/59.07 => ( ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 58.89/59.07 & sdteqdtlpzmzozddtrp0(W1,W3,W2) ) % 58.89/59.07 => sdteqdtlpzmzozddtrp0(W0,W3,W2) ) ) ). % 58.89/59.07 % 58.89/59.07 fof(mEquModMul,axiom, % 58.89/59.07 ! [W0,W1,W2,W3] : % 58.89/59.07 ( ( aInteger0(W0) % 58.89/59.07 & aInteger0(W1) % 58.89/59.07 & aInteger0(W2) % 58.89/59.07 & W2 != sz00 % 58.89/59.07 & aInteger0(W3) % 58.89/59.07 & W3 != sz00 ) % 58.89/59.07 => ( sdteqdtlpzmzozddtrp0(W0,W1,sdtasdt0(W2,W3)) % 58.89/59.07 => ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 58.89/59.07 & sdteqdtlpzmzozddtrp0(W0,W1,W3) ) ) ) ). % 58.89/59.07 % 58.89/59.07 fof(mPrime,axiom, % 58.89/59.07 ! [W0] : % 58.89/59.07 ( ( aInteger0(W0) % 58.89/59.07 & W0 != sz00 ) % 58.89/59.07 => ( isPrime0(W0) % 58.89/59.07 => $true ) ) ). % 58.89/59.07 % 58.89/59.07 fof(mPrimeDivisor,axiom, % 58.89/59.07 ! [W0] : % 58.89/59.07 ( aInteger0(W0) % 58.89/59.07 => ( ? [W1] : % 58.89/59.07 ( aDivisorOf0(W1,W0) % 58.89/59.07 & isPrime0(W1) ) % 58.89/59.07 <=> ( W0 != sz10 % 58.89/59.07 & W0 != smndt0(sz10) ) ) ) ). % 58.89/59.07 % 58.89/59.07 fof(mSets,axiom, % 58.89/59.07 ! [W0] : % 58.89/59.07 ( aSet0(W0) % 58.89/59.07 => $true ) ). % 58.89/59.07 % 58.89/59.07 fof(mElements,axiom, % 58.89/59.07 ! [W0] : % 58.89/59.07 ( aSet0(W0) % 58.89/59.07 => ! [W1] : % 58.89/59.07 ( aElementOf0(W1,W0) % 58.89/59.07 => $true ) ) ). % 58.89/59.07 % 58.89/59.07 fof(mSubset,definition, % 58.89/59.07 ! [W0] : % 58.89/59.07 ( aSet0(W0) % 58.89/59.07 => ! [W1] : % 58.89/59.07 ( aSubsetOf0(W1,W0) % 58.89/59.07 <=> ( aSet0(W1) % 58.89/59.07 & ! [W2] : % 58.89/59.07 ( aElementOf0(W2,W1) % 58.89/59.07 => aElementOf0(W2,W0) ) ) ) ) ). % 58.89/59.07 % 58.89/59.07 fof(mFinSet,axiom, % 58.89/59.07 ! [W0] : % 58.89/59.07 ( aSet0(W0) % 58.89/59.07 => ( isFinite0(W0) % 58.89/59.07 => $true ) ) ). % 58.89/59.07 % 58.89/59.07 fof(mUnion,definition, % 58.89/59.07 ! [W0,W1] : % 58.89/59.07 ( ( aSubsetOf0(W0,cS1395) % 58.89/59.07 & aSubsetOf0(W1,cS1395) ) % 58.89/59.07 => ! [W2] : % 58.89/59.07 ( W2 = sdtbsmnsldt0(W0,W1) % 58.89/59.07 <=> ( aSet0(W2) % 58.89/59.07 & ! [W3] : % 58.89/59.07 ( aElementOf0(W3,W2) % 58.89/59.07 <=> ( aInteger0(W3) % 58.89/59.07 & ( aElementOf0(W3,W0) % 58.89/59.07 | aElementOf0(W3,W1) ) ) ) ) ) ) ). % 58.89/59.07 % 58.89/59.07 fof(mIntersection,definition, % 58.89/59.07 ! [W0,W1] : % 58.89/59.07 ( ( aSubsetOf0(W0,cS1395) % 58.89/59.08 & aSubsetOf0(W1,cS1395) ) % 58.89/59.08 => ! [W2] : % 58.89/59.08 ( W2 = sdtslmnbsdt0(W0,W1) % 58.89/59.08 <=> ( aSet0(W2) % 58.89/59.08 & ! [W3] : % 58.89/59.08 ( aElementOf0(W3,W2) % 58.89/59.08 <=> ( aInteger0(W3) % 58.89/59.08 & aElementOf0(W3,W0) % 58.89/59.08 & aElementOf0(W3,W1) ) ) ) ) ) ). % 58.89/59.08 % 58.89/59.08 fof(mUnionSet,definition, % 58.89/59.08 ! [W0] : % 58.89/59.08 ( ( aSet0(W0) % 58.89/59.08 & ! [W1] : % 58.89/59.08 ( aElementOf0(W1,W0) % 58.89/59.08 => aSubsetOf0(W1,cS1395) ) ) % 58.89/59.08 => ! [W1] : % 58.89/59.08 ( W1 = sbsmnsldt0(W0) % 58.89/59.08 <=> ( aSet0(W1) % 58.89/59.08 & ! [W2] : % 58.89/59.08 ( aElementOf0(W2,W1) % 58.89/59.08 <=> ( aInteger0(W2) % 58.89/59.08 & ? [W3] : % 58.89/59.08 ( aElementOf0(W3,W0) % 58.89/59.08 & aElementOf0(W2,W3) ) ) ) ) ) ) ). % 58.89/59.08 % 58.89/59.08 fof(mComplement,definition, % 58.89/59.08 ! [W0] : % 58.89/59.08 ( aSubsetOf0(W0,cS1395) % 58.89/59.08 => ! [W1] : % 58.89/59.08 ( W1 = stldt0(W0) % 58.89/59.08 <=> ( aSet0(W1) % 58.89/59.08 & ! [W2] : % 58.89/59.08 ( aElementOf0(W2,W1) % 58.89/59.08 <=> ( aInteger0(W2) % 58.89/59.08 & ~ aElementOf0(W2,W0) ) ) ) ) ) ). % 58.89/59.08 % 58.89/59.08 fof(mArSeq,definition, % 58.89/59.08 ! [W0,W1] : % 58.89/59.08 ( ( aInteger0(W0) % 58.89/59.08 & aInteger0(W1) % 58.89/59.08 & W1 != sz00 ) % 58.89/59.08 => ! [W2] : % 58.89/59.08 ( W2 = szAzrzSzezqlpdtcmdtrp0(W0,W1) % 58.89/59.08 <=> ( aSet0(W2) % 58.89/59.08 & ! [W3] : % 58.89/59.08 ( aElementOf0(W3,W2) % 58.89/59.08 <=> ( aInteger0(W3) % 58.89/59.08 & sdteqdtlpzmzozddtrp0(W3,W0,W1) ) ) ) ) ) ). % 58.89/59.08 % 58.89/59.08 fof(mOpen,definition, % 58.89/59.08 ! [W0] : % 58.89/59.08 ( aSubsetOf0(W0,cS1395) % 58.89/59.08 => ( isOpen0(W0) % 58.89/59.08 <=> ! [W1] : % 58.89/59.08 ( aElementOf0(W1,W0) % 58.89/59.08 => ? [W2] : % 58.89/59.08 ( aInteger0(W2) % 58.89/59.08 & W2 != sz00 % 58.89/59.08 & aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W1,W2),W0) ) ) ) ) ). % 58.89/59.08 % 58.89/59.08 fof(mClosed,definition, % 58.89/59.08 ! [W0] : % 58.89/59.08 ( aSubsetOf0(W0,cS1395) % 58.89/59.08 => ( isClosed0(W0) % 58.89/59.08 <=> isOpen0(stldt0(W0)) ) ) ). % 58.89/59.08 % 58.89/59.08 fof(mUnionOpen,axiom, % 58.89/59.08 ! [W0] : % 58.89/59.08 ( ( aSet0(W0) % 58.89/59.08 & ! [W1] : % 58.89/59.08 ( aElementOf0(W1,W0) % 58.89/59.08 => ( aSubsetOf0(W1,cS1395) % 58.89/59.08 & isOpen0(W1) ) ) ) % 58.89/59.08 => isOpen0(sbsmnsldt0(W0)) ) ). % 58.89/59.08 % 58.89/59.08 fof(mInterOpen,axiom, % 58.89/59.08 ! [W0,W1] : % 58.89/59.08 ( ( aSubsetOf0(W0,cS1395) % 58.89/59.08 & aSubsetOf0(W1,cS1395) % 58.89/59.08 & isOpen0(W0) % 58.89/59.08 & isOpen0(W1) ) % 58.89/59.08 => isOpen0(sdtslmnbsdt0(W0,W1)) ) ). % 58.89/59.08 % 58.89/59.08 fof(mUnionClosed,axiom, % 58.89/59.08 ! [W0,W1] : % 58.89/59.08 ( ( aSubsetOf0(W0,cS1395) % 58.89/59.08 & aSubsetOf0(W1,cS1395) % 58.89/59.08 & isClosed0(W0) % 58.89/59.08 & isClosed0(W1) ) % 58.89/59.08 => isClosed0(sdtbsmnsldt0(W0,W1)) ) ). % 58.89/59.08 % 58.89/59.08 fof(mUnionSClosed,axiom, % 58.89/59.08 ! [W0] : % 58.89/59.08 ( ( aSet0(W0) % 58.89/59.08 & isFinite0(W0) % 58.89/59.08 & ! [W1] : % 58.89/59.08 ( aElementOf0(W1,W0) % 58.89/59.08 => ( aSubsetOf0(W1,cS1395) % 58.89/59.08 & isClosed0(W1) ) ) ) % 58.89/59.08 => isClosed0(sbsmnsldt0(W0)) ) ). % 58.89/59.08 % 58.89/59.08 fof(mArSeqClosed,axiom, % 58.89/59.08 ! [W0,W1] : % 58.89/59.08 ( ( aInteger0(W0) % 58.89/59.08 & aInteger0(W1) % 58.89/59.08 & W1 != sz00 ) % 58.89/59.08 => ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),cS1395) % 58.89/59.08 & isClosed0(szAzrzSzezqlpdtcmdtrp0(W0,W1)) ) ) ). % 58.89/59.08 % 58.89/59.08 fof(m__2046,hypothesis, % 58.89/59.08 ( aSet0(xS) % 58.89/59.08 & ! [W0] : % 58.89/59.08 ( ( aElementOf0(W0,xS) % 58.89/59.08 => ? [W1] : % 58.89/59.08 ( aInteger0(W1) % 58.89/59.08 & W1 != sz00 % 58.89/59.08 & isPrime0(W1) % 58.89/59.08 & aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,W1)) % 58.89/59.08 & ! [W2] : % 58.89/59.08 ( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1)) % 58.89/59.08 => ( aInteger0(W2) % 58.89/59.08 & ? [W3] : % 58.89/59.08 ( aInteger0(W3) % 58.89/59.08 & sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00)) ) % 58.89/59.08 & aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00))) % 58.89/59.08 & sdteqdtlpzmzozddtrp0(W2,sz00,W1) ) ) % 58.89/59.08 & ( ( aInteger0(W2) % 58.89/59.08 & ( ? [W3] : % 58.89/59.08 ( aInteger0(W3) % 58.89/59.08 & sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00)) ) % 58.89/59.08 | aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00))) % 58.89/59.08 | sdteqdtlpzmzozddtrp0(W2,sz00,W1) ) ) % 58.89/59.08 => aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1)) ) ) % 58.89/59.08 & szAzrzSzezqlpdtcmdtrp0(sz00,W1) = W0 ) ) % 58.89/59.08 & ( ? [W1] : % 58.89/59.08 ( aInteger0(W1) % 58.89/59.08 & W1 != sz00 % 58.89/59.08 & isPrime0(W1) % 58.89/59.08 & ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,W1)) % 58.89/59.08 & ! [W2] : % 58.89/59.08 ( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1)) % 58.89/59.08 => ( aInteger0(W2) % 58.89/59.08 & ? [W3] : % 58.89/59.08 ( aInteger0(W3) % 58.89/59.08 & sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00)) ) % 58.89/59.08 & aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00))) % 58.89/59.08 & sdteqdtlpzmzozddtrp0(W2,sz00,W1) ) ) % 58.89/59.08 & ( ( aInteger0(W2) % 58.89/59.08 & ( ? [W3] : % 58.89/59.08 ( aInteger0(W3) % 58.89/59.08 & sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00)) ) % 58.89/59.08 | aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00))) % 58.89/59.08 | sdteqdtlpzmzozddtrp0(W2,sz00,W1) ) ) % 58.89/59.08 => aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1)) ) ) ) % 58.89/59.08 => szAzrzSzezqlpdtcmdtrp0(sz00,W1) = W0 ) ) % 58.89/59.08 => aElementOf0(W0,xS) ) ) % 58.89/59.08 & xS = cS2043 ) ). % 58.89/59.08 % 58.89/59.08 fof(m__2079,hypothesis, % 58.89/59.08 ( aSet0(sbsmnsldt0(xS)) % 58.89/59.08 & ! [W0] : % 58.89/59.08 ( aElementOf0(W0,sbsmnsldt0(xS)) % 58.89/59.08 <=> ( aInteger0(W0) % 58.89/59.08 & ? [W1] : % 58.89/59.08 ( aElementOf0(W1,xS) % 58.89/59.08 & aElementOf0(W0,W1) ) ) ) % 58.89/59.08 & aSet0(stldt0(sbsmnsldt0(xS))) % 58.89/59.08 & ! [W0] : % 58.89/59.08 ( aElementOf0(W0,stldt0(sbsmnsldt0(xS))) % 58.89/59.08 <=> ( aInteger0(W0) % 58.89/59.08 & ~ aElementOf0(W0,sbsmnsldt0(xS)) ) ) % 58.89/59.08 & ! [W0] : % 58.89/59.08 ( aElementOf0(W0,stldt0(sbsmnsldt0(xS))) % 58.89/59.08 <=> ( W0 = sz10 % 58.89/59.08 | W0 = smndt0(sz10) ) ) % 58.89/59.08 & stldt0(sbsmnsldt0(xS)) = cS2076 ) ). % 58.89/59.08 % 58.89/59.08 fof(m__2117,hypothesis, % 58.89/59.08 isFinite0(xS) ). % 58.89/59.08 % 58.89/59.08 fof(m__,conjecture, % 58.89/59.08 ( ( aSet0(sbsmnsldt0(xS)) % 58.89/59.08 & ! [W0] : % 58.89/59.08 ( aElementOf0(W0,sbsmnsldt0(xS)) % 58.89/59.08 <=> ( aInteger0(W0) % 58.89/59.08 & ? [W1] : % 58.89/59.08 ( aElementOf0(W1,xS) % 58.89/59.08 & aElementOf0(W0,W1) ) ) ) ) % 58.89/59.08 => ( ( ! [W0] : % 58.89/59.08 ( aElementOf0(W0,stldt0(sbsmnsldt0(xS))) % 58.89/59.08 <=> ( aInteger0(W0) % 58.89/59.08 & ~ aElementOf0(W0,sbsmnsldt0(xS)) ) ) % 58.89/59.08 => ( ! [W0] : % 58.89/59.08 ( aElementOf0(W0,stldt0(sbsmnsldt0(xS))) % 58.89/59.08 => ? [W1] : % 58.89/59.08 ( aInteger0(W1) % 58.89/59.08 & W1 != sz00 % 58.89/59.08 & ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)) % 58.89/59.08 & ! [W2] : % 58.89/59.08 ( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) % 58.89/59.08 => ( aInteger0(W2) % 58.89/59.08 & ? [W3] : % 58.89/59.08 ( aInteger0(W3) % 58.89/59.08 & sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0)) ) % 58.89/59.08 & aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))) % 58.89/59.08 & sdteqdtlpzmzozddtrp0(W2,W0,W1) ) ) % 58.89/59.08 & ( ( aInteger0(W2) % 58.89/59.08 & ( ? [W3] : % 58.89/59.08 ( aInteger0(W3) % 58.89/59.08 & sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0)) ) % 58.89/59.08 | aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))) % 58.89/59.08 | sdteqdtlpzmzozddtrp0(W2,W0,W1) ) ) % 58.89/59.08 => aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) ) ) ) % 58.89/59.08 => ( ! [W2] : % 58.89/59.08 ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) % 58.89/59.08 => aElementOf0(W2,stldt0(sbsmnsldt0(xS))) ) % 58.89/59.08 | aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS))) ) ) ) ) % 58.89/59.08 | isOpen0(stldt0(sbsmnsldt0(xS))) ) ) % 58.89/59.08 | isClosed0(sbsmnsldt0(xS)) ) ) ). % 58.89/59.08 % 58.89/59.08 %------------------------------------------------------------------------------ % 58.89/59.08 %------------------------------------------- % 58.89/59.08 % Proof found % 58.89/59.08 % SZS status Theorem for theBenchmark % 58.89/59.08 % SZS output start Proof % 58.89/59.08 %ClaNum:240(EqnAxiom:71) % 58.89/59.08 %VarNum:1109(SingletonVarNum:341) % 58.89/59.08 %MaxLitNum:8 % 58.89/59.08 %MaxfuncDepth:2 % 58.89/59.08 %SharedTerms:23 % 58.89/59.08 %goalClause: 79 81 82 83 101 108 126 128 131 135 136 141 150 155 159 166 171 181 184 189 191 192 201 % 58.89/59.08 %singleGoalClaCount:4 % 58.89/59.08 [72]E(a1,a2) % 58.89/59.08 [73]P1(a4) % 58.89/59.08 [74]P1(a36) % 58.89/59.08 [75]P4(a1) % 58.89/59.08 [76]P5(a1) % 58.89/59.08 [79]P4(f5(a1)) % 58.89/59.08 [82]~P6(f5(a1)) % 58.89/59.08 [77]E(f30(f5(a1)),a6) % 58.89/59.08 [80]P4(f30(f5(a1))) % 58.89/59.08 [81]P2(a7,f30(f5(a1))) % 58.89/59.08 [83]~P8(f30(f5(a1))) % 58.89/59.08 [84]~P1(x841)+P1(f31(x841)) % 58.89/59.08 [85]~P1(x851)+E(f32(a4,x851),a4) % 58.89/59.08 [86]~P1(x861)+E(f32(x861,a4),a4) % 58.89/59.08 [87]~P1(x871)+E(f33(a4,x871),x871) % 58.89/59.08 [88]~P1(x881)+E(f32(a36,x881),x881) % 58.89/59.08 [89]~P1(x891)+E(f33(x891,a4),x891) % 58.89/59.08 [90]~P1(x901)+E(f32(x901,a36),x901) % 58.89/59.08 [92]~P2(x921,a1)+~E(f8(x921),a4) % 58.89/59.08 [98]~P2(x981,a1)+P1(f8(x981)) % 58.89/59.08 [99]~P2(x991,a1)+P9(f8(x991)) % 58.89/59.08 [101]P1(x1011)+~P2(x1011,f5(a1)) % 58.89/59.08 [127]~P2(x1271,f5(a1))+P2(f15(x1271),a1) % 58.89/59.08 [128]~P2(x1281,f5(a1))+P2(f18(x1281),a1) % 58.89/59.08 [130]P2(x1301,f15(x1301))+~P2(x1301,f5(a1)) % 58.89/59.08 [131]P2(x1311,f18(x1311))+~P2(x1311,f5(a1)) % 58.89/59.08 [93]~P1(x931)+E(f33(f31(x931),x931),a4) % 58.89/59.08 [94]~P1(x941)+E(f33(x941,f31(x941)),a4) % 58.89/59.08 [95]~P1(x951)+E(f32(x951,f31(a36)),f31(x951)) % 58.89/59.08 [96]~P1(x961)+E(f32(f31(a36),x961),f31(x961)) % 58.89/59.08 [97]~E(x971,a36)+P2(x971,f30(f5(a1))) % 58.89/59.08 [103]~E(x1031,f31(a36))+P2(x1031,f30(f5(a1))) % 58.89/59.08 [112]~P2(x1121,a1)+E(f37(a4,f8(x1121)),x1121) % 58.89/59.08 [126]P1(x1261)+~P2(x1261,f30(f5(a1))) % 58.89/59.08 [140]~P2(x1401,a1)+P4(f37(a4,f8(x1401))) % 58.89/59.08 [155]~P2(x1551,f5(a1))+~P2(x1551,f30(f5(a1))) % 58.89/59.08 [108]~P1(x1081)+E(x1081,a4)+P4(f37(a7,x1081)) % 58.89/59.08 [109]~P6(x1091)+~P7(x1091,a3)+P8(f30(x1091)) % 58.89/59.08 [110]~P4(x1101)+P2(f9(x1101),x1101)+P8(f5(x1101)) % 58.89/59.08 [115]P6(x1151)+~P7(x1151,a3)+~P8(f30(x1151)) % 58.89/59.08 [122]P8(x1221)+P2(f10(x1221),x1221)+~P7(x1221,a3) % 58.89/59.08 [136]~P1(x1361)+E(x1361,a4)+P2(f21(x1361),f37(a7,x1361)) % 58.89/59.08 [129]E(x1291,a36)+E(x1291,f31(a36))+~P2(x1291,f30(f5(a1))) % 58.89/59.08 [135]~P1(x1351)+P2(x1351,f5(a1))+P2(x1351,f30(f5(a1))) % 58.89/59.08 [141]~P1(x1411)+E(x1411,a4)+~P2(f21(x1411),f30(f5(a1))) % 58.89/59.08 [166]~P1(x1661)+E(x1661,a4)+~P7(f37(a7,x1661),f30(f5(a1))) % 58.89/59.08 [102]~P3(x1021,x1022)+~P1(x1022)+~E(x1021,a4) % 58.89/59.08 [106]~P3(x1061,x1062)+P1(x1061)+~P1(x1062) % 58.89/59.08 [107]~P7(x1071,x1072)+P4(x1071)+~P4(x1072) % 58.89/59.08 [105]P4(x1051)+~P7(x1052,a3)+~E(x1051,f30(x1052)) % 58.89/59.08 [116]~P1(x1162)+~P1(x1161)+E(f33(x1161,x1162),f33(x1162,x1161)) % 58.89/59.08 [117]~P1(x1172)+~P1(x1171)+E(f32(x1171,x1172),f32(x1172,x1171)) % 58.89/59.08 [120]~P1(x1202)+~P1(x1201)+P1(f33(x1201,x1202)) % 58.89/59.08 [121]~P1(x1212)+~P1(x1211)+P1(f32(x1211,x1212)) % 58.89/59.08 [142]~P1(x1421)+~P3(x1422,x1421)+P1(f19(x1421,x1422)) % 58.89/59.08 [157]~P1(x1572)+~P3(x1571,x1572)+E(f32(x1571,f19(x1572,x1571)),x1572) % 58.89/59.08 [176]P1(x1761)+~P2(x1762,a1)+~P2(x1761,f37(a4,f8(x1762))) % 58.89/59.08 [195]~P2(x1951,a1)+P1(f16(x1951,x1952))+~P2(x1952,f37(a4,f8(x1951))) % 58.89/59.08 [208]~P2(x2081,a1)+P3(f8(x2081),f33(x2082,f31(a4)))+~P2(x2082,f37(a4,f8(x2081))) % 58.89/59.08 [211]~P2(x2112,a1)+P10(x2111,a4,f8(x2112))+~P2(x2111,f37(a4,f8(x2112))) % 58.89/59.08 [214]~P2(x2141,a1)+E(f32(f8(x2141),f16(x2141,x2142)),f33(x2142,f31(a4)))+~P2(x2142,f37(a4,f8(x2141))) % 58.89/59.08 [91]~P1(x911)+E(x911,a36)+E(x911,f31(a36))+P9(f20(x911)) % 58.89/59.08 [104]~P1(x1041)+P3(f20(x1041),x1041)+E(x1041,a36)+E(x1041,f31(a36)) % 58.89/59.08 [123]~P4(x1231)+~P5(x1231)+P2(f14(x1231),x1231)+P6(f5(x1231)) % 58.89/59.08 [145]~P4(x1451)+~P8(f9(x1451))+~P7(f9(x1451),a3)+P8(f5(x1451)) % 58.89/59.08 [111]~P1(x1111)+~P3(x1112,x1111)+~P9(x1112)+~E(x1111,a36) % 58.89/59.08 [156]~P1(x1561)+~P1(x1562)+P10(x1562,x1562,x1561)+E(x1561,a4) % 58.89/59.08 [114]~P4(x1142)+P4(x1141)+~E(x1141,f5(x1142))+P2(f23(x1142),x1142) % 58.89/59.08 [118]~P1(x1181)+~P3(x1182,x1181)+~P9(x1182)+~E(x1181,f31(a36)) % 58.89/59.08 [124]~P1(x1241)+~P1(x1242)+E(x1241,a4)+P6(f37(x1242,x1241)) % 58.89/59.08 [132]~P4(x1322)+P4(x1321)+~E(x1321,f5(x1322))+~P7(f23(x1322),a3) % 58.89/59.08 [137]~P1(x1371)+~P1(x1372)+E(x1371,a4)+P7(f37(x1372,x1371),a3) % 58.89/59.08 [150]~P1(x1501)+~P2(x1501,x1502)+~P2(x1502,a1)+P2(x1501,f5(a1)) % 58.89/59.08 [151]~P4(x1511)+~P4(x1512)+P7(x1511,x1512)+P2(f24(x1512,x1511),x1511) % 58.89/59.08 [159]~P1(x1591)+P1(x1592)+E(x1591,a4)+~P2(x1592,f37(a7,x1591)) % 58.89/59.08 [161]~P8(x1611)+~P2(x1612,x1611)+~P7(x1611,a3)+~E(f11(x1611,x1612),a4) % 58.89/59.08 [163]~P8(x1631)+~P2(x1632,x1631)+~P7(x1631,a3)+P1(f11(x1631,x1632)) % 58.89/59.08 [170]~P4(x1701)+~P4(x1702)+P7(x1701,x1702)+~P2(f24(x1702,x1701),x1702) % 58.89/59.08 [171]~P1(x1711)+E(x1711,a4)+~P2(x1712,f37(a7,x1711))+P1(f22(x1711,x1712)) % 58.89/59.08 [189]~P1(x1891)+P10(x1892,a7,x1891)+E(x1891,a4)+~P2(x1892,f37(a7,x1891)) % 58.89/59.08 [184]~P1(x1841)+E(x1841,a4)+~P2(x1842,f37(a7,x1841))+P3(x1841,f33(x1842,f31(a7))) % 58.89/59.08 [191]~P1(x1911)+E(x1911,a4)+~P2(x1912,f37(a7,x1911))+E(f32(x1911,f22(x1911,x1912)),f33(x1912,f31(a7))) % 58.89/59.08 [203]~P8(x2032)+~P2(x2031,x2032)+~P7(x2032,a3)+P7(f37(x2031,f11(x2032,x2031)),x2032) % 58.89/59.08 [212]~P1(x2121)+~P2(x2122,a1)+~P3(f8(x2122),f33(x2121,f31(a4)))+P2(x2121,f37(a4,f8(x2122))) % 58.89/59.08 [217]~P1(x2171)+~P2(x2172,a1)+~P10(x2171,a4,f8(x2172))+P2(x2171,f37(a4,f8(x2172))) % 58.89/59.08 [147]~P4(x1472)+~P7(x1473,x1472)+P2(x1471,x1472)+~P2(x1471,x1473) % 58.89/59.08 [138]~P2(x1381,x1382)+P1(x1381)+~P7(x1383,a3)+~E(x1382,f30(x1383)) % 58.89/59.08 [152]P4(x1521)+~P7(x1523,a3)+~P7(x1522,a3)+~E(x1521,f34(x1522,x1523)) % 58.89/59.08 [153]P4(x1531)+~P7(x1533,a3)+~P7(x1532,a3)+~E(x1531,f35(x1532,x1533)) % 58.89/59.08 [162]~P2(x1623,x1622)+~P2(x1623,x1621)+~P7(x1622,a3)+~E(x1621,f30(x1622)) % 58.89/59.08 [172]~P1(x1723)+~P1(x1722)+~P1(x1721)+E(f33(f33(x1721,x1722),x1723),f33(x1721,f33(x1722,x1723))) % 58.89/59.08 [173]~P1(x1733)+~P1(x1732)+~P1(x1731)+E(f32(f32(x1731,x1732),x1733),f32(x1731,f32(x1732,x1733))) % 58.89/59.08 [193]~P1(x1933)+~P1(x1932)+~P1(x1931)+E(f33(f32(x1931,x1932),f32(x1931,x1933)),f32(x1931,f33(x1932,x1933))) % 58.89/59.08 [194]~P1(x1942)+~P1(x1943)+~P1(x1941)+E(f33(f32(x1941,x1942),f32(x1943,x1942)),f32(f33(x1941,x1943),x1942)) % 58.89/59.08 [158]~P4(x1581)+~P5(x1581)+~P6(f14(x1581))+~P7(f14(x1581),a3)+P6(f5(x1581)) % 58.89/59.08 [113]~P1(x1131)+~P1(x1132)+E(x1131,a4)+E(x1132,a4)+~E(f32(x1132,x1131),a4) % 58.89/59.08 [133]~P1(x1331)+~P9(x1331)+E(x1331,a4)+P2(x1332,a1)+~E(f37(a4,x1331),x1332) % 58.89/59.08 [139]~P1(x1391)+~P9(x1391)+E(x1391,a4)+P2(x1392,a1)+P4(f37(a4,x1391)) % 58.89/59.08 [164]~P8(x1642)+~P8(x1641)+~P7(x1642,a3)+~P7(x1641,a3)+P8(f35(x1641,x1642)) % 58.89/59.08 [165]~P6(x1652)+~P6(x1651)+~P7(x1652,a3)+~P7(x1651,a3)+P6(f34(x1651,x1652)) % 58.89/59.08 [178]~P4(x1781)+P2(f12(x1782,x1781),x1781)+~P7(x1782,a3)+E(x1781,f30(x1782))+P1(f12(x1782,x1781)) % 58.89/59.08 [200]~P4(x2001)+P2(f12(x2002,x2001),x2001)+~P7(x2002,a3)+~P2(f12(x2002,x2001),x2002)+E(x2001,f30(x2002)) % 58.89/59.08 [201]~P1(x2011)+~P1(x2012)+~P10(x2012,a7,x2011)+E(x2011,a4)+P2(x2012,f37(a7,x2011)) % 58.89/59.08 [185]~P1(x1851)+P8(x1852)+~P7(x1852,a3)+E(x1851,a4)+~P7(f37(f10(x1852),x1851),x1852) % 58.89/59.08 [192]~P1(x1922)+~P1(x1921)+E(x1921,a4)+P2(x1922,f37(a7,x1921))+~P3(x1921,f33(x1922,f31(a7))) % 58.89/59.08 [119]~P1(x1191)+~P1(x1193)+P4(x1192)+E(x1191,a4)+~E(x1192,f37(x1193,x1191)) % 58.89/59.08 [144]~P4(x1442)+~P2(x1441,x1443)+P1(x1441)+P2(f23(x1442),x1442)+~E(x1443,f5(x1442)) % 58.89/59.08 [146]~P1(x1461)+P2(x1461,x1462)+P2(x1461,x1463)+~E(x1462,f30(x1463))+~P7(x1463,a3) % 58.89/59.08 [160]~P4(x1603)+~P2(x1601,x1602)+P1(x1601)+~E(x1602,f5(x1603))+~P7(f23(x1603),a3) % 58.89/59.08 [218]~P4(x2181)+~P2(x2182,x2183)+~E(x2183,f5(x2181))+P2(f23(x2181),x2181)+P2(x2182,f28(x2181,x2183,x2182)) % 58.89/59.08 [219]~P4(x2191)+~P2(x2193,x2192)+~E(x2192,f5(x2191))+P2(f23(x2191),x2191)+P2(f28(x2191,x2192,x2193),x2191) % 58.89/59.08 [221]~P4(x2212)+~P2(x2211,x2213)+~E(x2213,f5(x2212))+P2(x2211,f28(x2212,x2213,x2211))+~P7(f23(x2212),a3) % 58.89/59.08 [222]~P4(x2221)+~P2(x2223,x2222)+~E(x2222,f5(x2221))+P2(f28(x2221,x2222,x2223),x2221)+~P7(f23(x2221),a3) % 58.89/59.08 [204]~P1(x2041)+~P1(x2043)+~P2(x2042,a1)+~E(f32(f8(x2042),x2043),f33(x2041,f31(a4)))+P2(x2041,f37(a4,f8(x2042))) % 58.89/59.08 [167]~P2(x1671,x1672)+P1(x1671)+~P7(x1674,a3)+~P7(x1673,a3)+~E(x1672,f34(x1673,x1674)) % 58.89/59.08 [168]~P2(x1681,x1682)+P1(x1681)+~P7(x1684,a3)+~P7(x1683,a3)+~E(x1682,f35(x1683,x1684)) % 58.89/59.08 [174]~P2(x1741,x1743)+P2(x1741,x1742)+~P7(x1744,a3)+~P7(x1742,a3)+~E(x1743,f35(x1744,x1742)) % 58.89/59.08 [175]~P2(x1751,x1753)+P2(x1751,x1752)+~P7(x1754,a3)+~P7(x1752,a3)+~E(x1753,f35(x1752,x1754)) % 58.89/59.08 [182]~P4(x1821)+~P4(x1822)+P2(f23(x1822),x1822)+P2(f27(x1822,x1821),x1821)+E(x1821,f5(x1822))+P1(f27(x1822,x1821)) % 58.89/59.08 [188]~P4(x1881)+~P4(x1882)+P2(f27(x1882,x1881),x1881)+E(x1881,f5(x1882))+P1(f27(x1882,x1881))+~P7(f23(x1882),a3) % 58.89/59.08 [190]~P4(x1901)+~P4(x1902)+P2(f23(x1902),x1902)+P2(f27(x1902,x1901),x1901)+P2(f29(x1902,x1901),x1902)+E(x1901,f5(x1902)) % 58.89/59.08 [197]~P4(x1971)+~P4(x1972)+P2(f27(x1972,x1971),x1971)+P2(f29(x1972,x1971),x1972)+E(x1971,f5(x1972))+~P7(f23(x1972),a3) % 58.89/59.08 [206]~P4(x2061)+~P4(x2062)+P2(f23(x2062),x2062)+P2(f27(x2062,x2061),x2061)+P2(f27(x2062,x2061),f29(x2062,x2061))+E(x2061,f5(x2062)) % 58.89/59.08 [209]~P4(x2091)+~P4(x2092)+P2(f27(x2092,x2091),x2091)+P2(f27(x2092,x2091),f29(x2092,x2091))+E(x2091,f5(x2092))+~P7(f23(x2092),a3) % 58.89/59.08 [220]~P4(x2201)+P2(f12(x2202,x2201),x2202)+~P7(x2202,a3)+~P2(f12(x2202,x2201),x2201)+E(x2201,f30(x2202))+~P1(f12(x2202,x2201)) % 58.89/59.08 [216]~P1(x2161)+~P1(x2162)+~P1(x2163)+~P10(x2163,x2162,x2161)+P10(x2162,x2163,x2161)+E(x2161,a4) % 58.89/59.08 [143]~P1(x1432)+~P1(x1433)+~P1(x1431)+P3(x1431,x1432)+E(x1431,a4)+~E(f32(x1431,x1433),x1432) % 58.89/59.08 [169]~P1(x1691)+~P9(x1691)+P1(x1692)+E(x1691,a4)+P2(x1693,a1)+~P2(x1692,f37(a4,x1691)) % 58.89/59.08 [202]~P1(x2021)+~P9(x2021)+P10(x2023,a4,x2021)+E(x2021,a4)+P2(x2022,a1)+~P2(x2023,f37(a4,x2021)) % 58.89/59.08 [223]~P1(x2231)+~P9(x2231)+E(x2231,a4)+P2(x2232,a1)+~P2(x2233,f37(a4,x2231))+P1(f17(x2232,x2231,x2233)) % 58.89/59.08 [231]~P4(x2311)+P2(f25(x2312,x2313,x2311),x2311)+~P7(x2313,a3)+~P7(x2312,a3)+E(x2311,f34(x2312,x2313))+P1(f25(x2312,x2313,x2311)) % 58.89/59.08 [232]~P4(x2321)+P2(f26(x2322,x2323,x2321),x2321)+~P7(x2323,a3)+~P7(x2322,a3)+E(x2321,f35(x2322,x2323))+P1(f26(x2322,x2323,x2321)) % 58.89/59.08 [233]~P4(x2331)+P2(f26(x2332,x2333,x2331),x2331)+P2(f26(x2332,x2333,x2331),x2333)+~P7(x2333,a3)+~P7(x2332,a3)+E(x2331,f35(x2332,x2333)) % 58.89/59.08 [234]~P4(x2341)+P2(f26(x2342,x2343,x2341),x2341)+P2(f26(x2342,x2343,x2341),x2342)+~P7(x2343,a3)+~P7(x2342,a3)+E(x2341,f35(x2342,x2343)) % 58.89/59.08 [181]~P1(x1812)+~P1(x1811)+~P1(x1813)+E(x1811,a4)+P2(x1812,f37(a7,x1811))+~E(f32(x1811,x1813),f33(x1812,f31(a7))) % 58.89/59.08 [199]~P1(x1991)+~P9(x1991)+E(x1991,a4)+P2(x1992,a1)+~P2(x1993,f37(a4,x1991))+P3(x1991,f33(x1993,f31(a4))) % 58.89/59.08 [213]~P1(x2133)+~P1(x2132)+~P1(x2131)+P10(x2132,x2133,x2131)+E(x2131,a4)+~P3(x2131,f33(x2132,f31(x2133))) % 58.89/59.08 [215]~P1(x2151)+~P1(x2153)+~P1(x2152)+~P10(x2152,x2153,x2151)+E(x2151,a4)+P3(x2151,f33(x2152,f31(x2153))) % 58.89/59.08 [226]~P1(x2261)+~P9(x2261)+P2(x2262,a1)+E(x2261,a4)+~P2(x2263,f37(a4,x2261))+E(f32(x2261,f17(x2262,x2261,x2263)),f33(x2263,f31(a4))) % 58.89/59.08 [148]~P1(x1481)+~P1(x1484)+~P2(x1482,x1483)+P1(x1482)+E(x1481,a4)+~E(x1483,f37(x1484,x1481)) % 58.89/59.09 [179]~P1(x1791)+~P2(x1791,x1794)+P2(x1791,x1792)+~P7(x1793,a3)+~P7(x1794,a3)+~E(x1792,f34(x1793,x1794)) % 58.89/59.09 [180]~P1(x1801)+~P2(x1801,x1803)+P2(x1801,x1802)+~P7(x1804,a3)+~P7(x1803,a3)+~E(x1802,f34(x1803,x1804)) % 58.89/59.09 [186]~P2(x1861,x1864)+P2(x1861,x1862)+P2(x1861,x1863)+~P7(x1862,a3)+~P7(x1863,a3)+~E(x1864,f34(x1863,x1862)) % 58.89/59.09 [187]~P1(x1871)+~P1(x1873)+~P2(x1872,x1874)+P10(x1872,x1873,x1871)+E(x1871,a4)+~E(x1874,f37(x1873,x1871)) % 58.89/59.09 [210]~P1(x2101)+~P1(x2103)+~P9(x2101)+~P10(x2103,a4,x2101)+E(x2101,a4)+P2(x2102,a1)+P2(x2103,f37(a4,x2101)) % 58.89/59.09 [230]~P1(x2301)+~P1(x2303)+~P4(x2302)+P2(f13(x2303,x2301,x2302),x2302)+E(x2301,a4)+E(x2302,f37(x2303,x2301))+P1(f13(x2303,x2301,x2302)) % 58.89/59.09 [235]~P1(x2351)+~P1(x2353)+~P4(x2352)+P10(f13(x2353,x2351,x2352),x2353,x2351)+P2(f13(x2353,x2351,x2352),x2352)+E(x2351,a4)+E(x2352,f37(x2353,x2351)) % 58.89/59.09 [236]~P4(x2361)+P2(f25(x2362,x2363,x2361),x2361)+P2(f25(x2362,x2363,x2361),x2363)+P2(f25(x2362,x2363,x2361),x2362)+~P7(x2363,a3)+~P7(x2362,a3)+E(x2361,f34(x2362,x2363)) % 58.89/59.09 [237]~P4(x2371)+~P7(x2373,a3)+~P7(x2372,a3)+~P2(f25(x2372,x2373,x2371),x2371)+~P2(f25(x2372,x2373,x2371),x2373)+E(x2371,f34(x2372,x2373))+~P1(f25(x2372,x2373,x2371)) % 58.89/59.09 [238]~P4(x2381)+~P7(x2383,a3)+~P7(x2382,a3)+~P2(f25(x2382,x2383,x2381),x2381)+~P2(f25(x2382,x2383,x2381),x2382)+E(x2381,f34(x2382,x2383))+~P1(f25(x2382,x2383,x2381)) % 58.89/59.09 [205]~P1(x2053)+~P1(x2051)+~P9(x2051)+E(x2051,a4)+P2(x2052,a1)+P2(x2053,f37(a4,x2051))+~P3(x2051,f33(x2053,f31(a4))) % 58.89/59.09 [177]~P1(x1771)+~P4(x1773)+~P2(x1771,x1774)+P2(x1771,x1772)+~P2(x1774,x1773)+~E(x1772,f5(x1773))+P2(f23(x1773),x1773) % 58.89/59.09 [183]~P1(x1831)+~P4(x1833)+~P2(x1831,x1834)+P2(x1831,x1832)+~P2(x1834,x1833)+~E(x1832,f5(x1833))+~P7(f23(x1833),a3) % 58.89/59.09 [198]~P1(x1981)+~P2(x1981,x1984)+~P2(x1981,x1983)+P2(x1981,x1982)+~P7(x1984,a3)+~P7(x1983,a3)+~E(x1982,f35(x1983,x1984)) % 58.89/59.09 [207]~P1(x2071)+~P1(x2074)+~P1(x2072)+~P10(x2072,x2074,x2071)+P2(x2072,x2073)+E(x2071,a4)+~E(x2073,f37(x2074,x2071)) % 58.89/59.09 [227]~P4(x2271)+~P4(x2272)+~P2(x2273,x2272)+P2(f23(x2272),x2272)+~P2(f27(x2272,x2271),x2273)+~P2(f27(x2272,x2271),x2271)+E(x2271,f5(x2272))+~P1(f27(x2272,x2271)) % 58.89/59.09 [228]~P4(x2281)+~P4(x2282)+~P2(x2283,x2282)+~P2(f27(x2282,x2281),x2283)+~P2(f27(x2282,x2281),x2281)+E(x2281,f5(x2282))+~P1(f27(x2282,x2281))+~P7(f23(x2282),a3) % 58.89/59.09 [239]~P1(x2391)+~P1(x2393)+~P4(x2392)+~P10(f13(x2393,x2391,x2392),x2393,x2391)+~P2(f13(x2393,x2391,x2392),x2392)+E(x2391,a4)+E(x2392,f37(x2393,x2391))+~P1(f13(x2393,x2391,x2392)) % 58.89/59.09 [240]~P4(x2401)+~P7(x2403,a3)+~P7(x2402,a3)+~P2(f26(x2402,x2403,x2401),x2401)+~P2(f26(x2402,x2403,x2401),x2403)+~P2(f26(x2402,x2403,x2401),x2402)+E(x2401,f35(x2402,x2403))+~P1(f26(x2402,x2403,x2401)) % 58.89/59.09 [229]~P1(x2293)+~P1(x2291)+~P1(x2292)+~P10(x2294,x2293,x2291)+~P10(x2292,x2294,x2291)+P10(x2292,x2293,x2291)+~P1(x2294)+E(x2291,a4) % 58.89/59.09 [224]~P1(x2241)+~P1(x2242)+~P1(x2244)+~P1(x2243)+P10(x2243,x2244,x2242)+~P10(x2243,x2244,f32(x2241,x2242))+E(x2241,a4)+E(x2242,a4) % 58.89/59.09 [225]~P1(x2251)+~P1(x2252)+~P1(x2254)+~P1(x2253)+P10(x2253,x2254,x2252)+~P10(x2253,x2254,f32(x2252,x2251))+E(x2251,a4)+E(x2252,a4) % 58.89/59.09 [196]~P1(x1963)+~P1(x1961)+~P1(x1964)+~P9(x1961)+E(x1961,a4)+P2(x1962,a1)+P2(x1963,f37(a4,x1961))+~E(f32(x1961,x1964),f33(x1963,f31(a4))) % 58.89/59.09 %EqnAxiom % 58.89/59.09 [1]E(x11,x11) % 58.89/59.09 [2]E(x22,x21)+~E(x21,x22) % 58.89/59.09 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.89/59.09 [4]~E(x41,x42)+E(f5(x41),f5(x42)) % 58.89/59.09 [5]~E(x51,x52)+E(f30(x51),f30(x52)) % 58.89/59.09 [6]~E(x61,x62)+E(f26(x61,x63,x64),f26(x62,x63,x64)) % 58.89/59.09 [7]~E(x71,x72)+E(f26(x73,x71,x74),f26(x73,x72,x74)) % 58.89/59.09 [8]~E(x81,x82)+E(f26(x83,x84,x81),f26(x83,x84,x82)) % 58.89/59.09 [9]~E(x91,x92)+E(f8(x91),f8(x92)) % 58.89/59.09 [10]~E(x101,x102)+E(f37(x101,x103),f37(x102,x103)) % 58.89/59.09 [11]~E(x111,x112)+E(f37(x113,x111),f37(x113,x112)) % 58.89/59.09 [12]~E(x121,x122)+E(f31(x121),f31(x122)) % 58.89/59.09 [13]~E(x131,x132)+E(f32(x131,x133),f32(x132,x133)) % 58.89/59.09 [14]~E(x141,x142)+E(f32(x143,x141),f32(x143,x142)) % 58.89/59.09 [15]~E(x151,x152)+E(f23(x151),f23(x152)) % 58.89/59.09 [16]~E(x161,x162)+E(f35(x161,x163),f35(x162,x163)) % 58.89/59.09 [17]~E(x171,x172)+E(f35(x173,x171),f35(x173,x172)) % 58.89/59.09 [18]~E(x181,x182)+E(f13(x181,x183,x184),f13(x182,x183,x184)) % 58.89/59.09 [19]~E(x191,x192)+E(f13(x193,x191,x194),f13(x193,x192,x194)) % 58.89/59.09 [20]~E(x201,x202)+E(f13(x203,x204,x201),f13(x203,x204,x202)) % 58.89/59.09 [21]~E(x211,x212)+E(f17(x211,x213,x214),f17(x212,x213,x214)) % 58.89/59.09 [22]~E(x221,x222)+E(f17(x223,x221,x224),f17(x223,x222,x224)) % 58.89/59.09 [23]~E(x231,x232)+E(f17(x233,x234,x231),f17(x233,x234,x232)) % 58.89/59.09 [24]~E(x241,x242)+E(f27(x241,x243),f27(x242,x243)) % 58.89/59.09 [25]~E(x251,x252)+E(f27(x253,x251),f27(x253,x252)) % 58.89/59.09 [26]~E(x261,x262)+E(f28(x261,x263,x264),f28(x262,x263,x264)) % 58.89/59.09 [27]~E(x271,x272)+E(f28(x273,x271,x274),f28(x273,x272,x274)) % 58.89/59.09 [28]~E(x281,x282)+E(f28(x283,x284,x281),f28(x283,x284,x282)) % 58.89/59.09 [29]~E(x291,x292)+E(f25(x291,x293,x294),f25(x292,x293,x294)) % 58.89/59.09 [30]~E(x301,x302)+E(f25(x303,x301,x304),f25(x303,x302,x304)) % 58.89/59.09 [31]~E(x311,x312)+E(f25(x313,x314,x311),f25(x313,x314,x312)) % 58.89/59.09 [32]~E(x321,x322)+E(f33(x321,x323),f33(x322,x323)) % 58.89/59.09 [33]~E(x331,x332)+E(f33(x333,x331),f33(x333,x332)) % 58.89/59.09 [34]~E(x341,x342)+E(f11(x341,x343),f11(x342,x343)) % 58.89/59.09 [35]~E(x351,x352)+E(f11(x353,x351),f11(x353,x352)) % 58.89/59.09 [36]~E(x361,x362)+E(f9(x361),f9(x362)) % 58.89/59.09 [37]~E(x371,x372)+E(f34(x371,x373),f34(x372,x373)) % 58.89/59.09 [38]~E(x381,x382)+E(f34(x383,x381),f34(x383,x382)) % 58.89/59.09 [39]~E(x391,x392)+E(f16(x391,x393),f16(x392,x393)) % 58.89/59.09 [40]~E(x401,x402)+E(f16(x403,x401),f16(x403,x402)) % 58.89/59.09 [41]~E(x411,x412)+E(f20(x411),f20(x412)) % 58.89/59.09 [42]~E(x421,x422)+E(f10(x421),f10(x422)) % 58.89/59.09 [43]~E(x431,x432)+E(f29(x431,x433),f29(x432,x433)) % 58.89/59.09 [44]~E(x441,x442)+E(f29(x443,x441),f29(x443,x442)) % 58.89/59.09 [45]~E(x451,x452)+E(f21(x451),f21(x452)) % 58.89/59.09 [46]~E(x461,x462)+E(f22(x461,x463),f22(x462,x463)) % 58.89/59.09 [47]~E(x471,x472)+E(f22(x473,x471),f22(x473,x472)) % 58.89/59.09 [48]~E(x481,x482)+E(f12(x481,x483),f12(x482,x483)) % 58.89/59.09 [49]~E(x491,x492)+E(f12(x493,x491),f12(x493,x492)) % 58.89/59.09 [50]~E(x501,x502)+E(f14(x501),f14(x502)) % 58.89/59.09 [51]~E(x511,x512)+E(f15(x511),f15(x512)) % 58.89/59.09 [52]~E(x521,x522)+E(f24(x521,x523),f24(x522,x523)) % 58.89/59.09 [53]~E(x531,x532)+E(f24(x533,x531),f24(x533,x532)) % 58.89/59.09 [54]~E(x541,x542)+E(f19(x541,x543),f19(x542,x543)) % 58.89/59.09 [55]~E(x551,x552)+E(f19(x553,x551),f19(x553,x552)) % 58.89/59.09 [56]~E(x561,x562)+E(f18(x561),f18(x562)) % 58.89/59.09 [57]~P1(x571)+P1(x572)+~E(x571,x572) % 58.89/59.09 [58]P2(x582,x583)+~E(x581,x582)+~P2(x581,x583) % 58.89/59.09 [59]P2(x593,x592)+~E(x591,x592)+~P2(x593,x591) % 58.89/59.09 [60]~P4(x601)+P4(x602)+~E(x601,x602) % 58.89/59.09 [61]~P5(x611)+P5(x612)+~E(x611,x612) % 58.89/59.09 [62]~P6(x621)+P6(x622)+~E(x621,x622) % 58.89/59.09 [63]P7(x632,x633)+~E(x631,x632)+~P7(x631,x633) % 58.89/59.09 [64]P7(x643,x642)+~E(x641,x642)+~P7(x643,x641) % 58.89/59.09 [65]P3(x652,x653)+~E(x651,x652)+~P3(x651,x653) % 58.89/59.09 [66]P3(x663,x662)+~E(x661,x662)+~P3(x663,x661) % 58.89/59.09 [67]P10(x672,x673,x674)+~E(x671,x672)+~P10(x671,x673,x674) % 58.89/59.09 [68]P10(x683,x682,x684)+~E(x681,x682)+~P10(x683,x681,x684) % 58.89/59.09 [69]P10(x693,x694,x692)+~E(x691,x692)+~P10(x693,x694,x691) % 58.89/59.09 [70]~P9(x701)+P9(x702)+~E(x701,x702) % 58.89/59.09 [71]~P8(x711)+P8(x712)+~E(x711,x712) % 58.89/59.09 % 58.89/59.09 %------------------------------------------- % 58.89/59.09 cnf(241,plain, % 58.89/59.09 (P2(a36,f30(f5(a1)))), % 58.89/59.09 inference(equality_inference,[],[97])). % 58.89/59.09 cnf(242,plain, % 58.89/59.09 (~P1(x2421)+~P3(a4,x2421)), % 58.89/59.09 inference(equality_inference,[],[102])). % 58.89/59.09 cnf(243,plain, % 58.89/59.09 (P2(f31(a36),f30(f5(a1)))), % 58.89/59.09 inference(equality_inference,[],[103])). % 58.89/59.09 cnf(245,plain, % 58.89/59.09 (~P9(x2451)+~P1(a36)+~P3(x2451,a36)), % 58.89/59.09 inference(equality_inference,[],[111])). % 58.89/59.09 cnf(247,plain, % 58.89/59.09 (~P9(x2471)+~P1(f31(a36))+~P3(x2471,f31(a36))), % 58.89/59.09 inference(equality_inference,[],[118])). % 58.89/59.09 cnf(248,plain, % 58.89/59.09 (~P1(x2481)+~P1(x2482)+P4(f37(x2482,x2481))+E(x2481,a4)), % 58.89/59.09 inference(equality_inference,[],[119])). % 58.89/59.09 cnf(255,plain, % 58.89/59.09 (P1(x2551)+~P1(x2552)+~P1(x2553)+~P2(x2551,f37(x2553,x2552))+E(x2552,a4)), % 58.89/59.09 inference(equality_inference,[],[148])). % 58.89/59.09 cnf(268,plain, % 58.89/59.09 (~P2(x2681,f34(x2682,x2683))+P2(x2681,x2683)+P2(x2681,x2682)+~P7(x2683,a3)+~P7(x2682,a3)), % 58.89/59.09 inference(equality_inference,[],[186])). % 58.89/59.09 cnf(269,plain, % 58.89/59.09 (P10(x2691,x2692,x2693)+~P1(x2693)+~P1(x2692)+~P2(x2691,f37(x2692,x2693))+E(x2693,a4)), % 58.89/59.09 inference(equality_inference,[],[187])). % 58.89/59.09 cnf(271,plain, % 58.89/59.09 (~P10(x2711,x2712,x2713)+~P1(x2713)+~P1(x2712)+P2(x2711,f37(x2712,x2713))+~P1(x2711)+E(x2713,a4)), % 58.89/59.09 inference(equality_inference,[],[207])). % 58.89/59.09 cnf(276,plain, % 58.89/59.09 (~P9(x2761)+~P3(x2761,a36)), % 58.89/59.09 inference(scs_inference,[],[74,245])). % 58.89/59.09 cnf(277,plain, % 58.89/59.09 (P1(a7)), % 58.89/59.09 inference(scs_inference,[],[81,126])). % 58.89/59.09 cnf(279,plain, % 58.89/59.09 (~P2(a7,f5(a1))), % 58.89/59.09 inference(scs_inference,[],[81,126,155])). % 58.89/59.09 cnf(281,plain, % 58.89/59.09 (E(a2,a1)), % 58.89/59.09 inference(scs_inference,[],[81,72,126,155,2])). % 58.89/59.09 cnf(283,plain, % 58.89/59.09 (~E(f30(f5(a1)),f5(a1))), % 58.89/59.09 inference(scs_inference,[],[81,72,75,126,155,2,60,59])). % 58.89/59.09 cnf(285,plain, % 58.89/59.09 (~P2(f30(f5(a1)),a1)), % 58.89/59.09 inference(scs_inference,[],[81,72,75,76,126,155,2,60,59,61,150])). % 58.89/59.09 cnf(287,plain, % 58.89/59.09 (P2(f14(a1),a1)), % 58.89/59.09 inference(scs_inference,[],[82,81,72,75,76,126,155,2,60,59,61,150,123])). % 58.89/59.09 cnf(297,plain, % 58.89/59.09 (~P9(x2971)+~P1(x2971)+E(x2971,a4)+P4(f37(a4,x2971))), % 58.89/59.09 inference(scs_inference,[],[285,139])). % 58.89/59.09 cnf(299,plain, % 58.89/59.09 (~P9(x2991)+~P1(x2992)+~P1(x2991)+~P1(x2993)+E(x2991,a4)+P2(x2992,f37(a4,x2991))+~E(f32(x2991,x2993),f33(x2992,f31(a4)))), % 58.89/59.09 inference(scs_inference,[],[285,196])). % 58.89/59.09 cnf(301,plain, % 58.89/59.09 (~P9(x3011)+~P1(x3011)+P10(x3012,a4,x3011)+E(x3011,a4)+~P2(x3012,f37(a4,x3011))), % 58.89/59.09 inference(scs_inference,[],[285,202])). % 58.89/59.09 cnf(304,plain, % 58.89/59.09 (P1(f31(a36))), % 58.89/59.09 inference(scs_inference,[],[243,126])). % 58.89/59.09 cnf(306,plain, % 58.89/59.09 (~P2(f31(a36),f5(a1))), % 58.89/59.09 inference(scs_inference,[],[243,126,155])). % 58.89/59.09 cnf(308,plain, % 58.89/59.09 (E(a6,f30(f5(a1)))), % 58.89/59.09 inference(scs_inference,[],[243,77,126,155,2])). % 58.89/59.09 cnf(311,plain, % 58.89/59.09 (P2(a36,a6)), % 58.89/59.09 inference(scs_inference,[],[285,83,243,241,287,77,126,155,2,71,58,59])). % 58.89/59.09 cnf(313,plain, % 58.89/59.09 (~P2(a7,f14(a1))), % 58.89/59.09 inference(scs_inference,[],[285,83,243,241,279,287,277,80,77,126,155,2,71,58,59,60,150])). % 58.89/59.09 cnf(315,plain, % 58.89/59.09 (~P9(x3151)+~P3(x3151,f31(a36))), % 58.89/59.09 inference(scs_inference,[],[285,83,243,241,279,287,277,80,77,126,155,2,71,58,59,60,150,247])). % 58.89/59.09 cnf(323,plain, % 58.89/59.09 (~P2(a36,f5(a1))), % 58.89/59.09 inference(scs_inference,[],[241,155])). % 58.89/59.09 cnf(334,plain, % 58.89/59.09 (P2(x3341,f30(f5(a1)))+~E(a7,x3341)), % 58.89/59.09 inference(scs_inference,[],[79,81,313,304,306,311,241,287,281,72,155,59,147,150,71,70,62,57,58])). % 58.89/59.09 cnf(337,plain, % 58.89/59.09 (P2(f14(a1),a2)), % 58.89/59.09 inference(scs_inference,[],[287,72,59])). % 58.89/59.09 cnf(338,plain, % 58.89/59.09 (~P2(a36,f14(a1))), % 58.89/59.09 inference(scs_inference,[],[287,323,72,74,59,150])). % 58.89/59.09 cnf(342,plain, % 58.89/59.09 (P2(x3421,f30(f5(a1)))+~E(f31(a36),x3421)), % 58.89/59.09 inference(scs_inference,[],[243,287,323,308,72,74,59,150,71,62,58])). % 58.89/59.09 cnf(352,plain, % 58.89/59.09 (P2(x3521,f30(f5(a1)))+~E(a36,x3521)), % 58.89/59.09 inference(scs_inference,[],[338,241,311,77,59,62,70,58])). % 58.89/59.09 cnf(499,plain, % 58.89/59.09 (P1(f31(f8(f14(a1))))), % 58.89/59.09 inference(scs_inference,[],[287,84,98])). % 58.89/59.09 cnf(531,plain, % 58.89/59.09 (~P3(f8(f14(a1)),a36)), % 58.89/59.09 inference(scs_inference,[],[287,276,99])). % 58.89/59.09 cnf(563,plain, % 58.89/59.09 (~P3(f8(f14(a1)),f31(a36))), % 58.89/59.09 inference(scs_inference,[],[287,315,99])). % 58.89/59.09 cnf(736,plain, % 58.89/59.09 (E(f32(a4,f31(f31(a36))),a4)), % 58.89/59.09 inference(scs_inference,[],[304,85,84])). % 58.89/59.09 cnf(737,plain, % 58.89/59.09 (E(a4,f32(a4,f31(f31(a36))))), % 58.89/59.09 inference(scs_inference,[],[736,2])). % 58.89/59.09 cnf(738,plain, % 58.89/59.09 (P1(f32(a4,f31(f31(a36))))), % 58.89/59.09 inference(scs_inference,[],[736,73,2,57])). % 58.89/59.09 cnf(776,plain, % 58.89/59.09 (E(f32(f8(f14(a1)),a4),a4)), % 58.89/59.09 inference(scs_inference,[],[287,86,98])). % 58.89/59.09 cnf(777,plain, % 58.89/59.09 (E(a4,f32(f8(f14(a1)),a4))), % 58.89/59.09 inference(scs_inference,[],[776,2])). % 58.89/59.09 cnf(780,plain, % 58.89/59.09 (P1(f32(f8(f14(a1)),a4))), % 58.89/59.09 inference(scs_inference,[],[304,776,73,2,102,57])). % 58.89/59.09 cnf(821,plain, % 58.89/59.09 (E(f33(a4,a7),a7)), % 58.89/59.09 inference(scs_inference,[],[81,87,126])). % 58.89/59.09 cnf(822,plain, % 58.89/59.09 (E(a7,f33(a4,a7))), % 58.89/59.09 inference(scs_inference,[],[821,2])). % 58.89/59.09 cnf(823,plain, % 58.89/59.09 (P1(f33(a4,a7))), % 58.89/59.09 inference(scs_inference,[],[277,821,2,57])). % 58.89/59.09 cnf(825,plain, % 58.89/59.09 (~P2(f33(a4,a7),f5(a1))), % 58.89/59.09 inference(scs_inference,[],[81,277,821,2,57,58,155])). % 58.89/59.09 cnf(828,plain, % 58.89/59.09 (~P2(f33(a4,a7),f14(a1))), % 58.89/59.09 inference(scs_inference,[],[81,287,277,821,2,57,58,155,70,150])). % 58.89/59.09 cnf(1012,plain, % 58.89/59.09 (E(f32(a36,f31(f33(a4,a7))),f31(f33(a4,a7)))), % 58.89/59.09 inference(scs_inference,[],[823,88,84])). % 58.89/59.09 cnf(1028,plain, % 58.89/59.09 (E(f33(f8(f14(a1)),a4),f8(f14(a1)))), % 58.89/59.09 inference(scs_inference,[],[287,89,98])). % 58.89/59.09 cnf(1041,plain, % 58.89/59.09 (~P3(f32(a4,f31(f31(a36))),a4)), % 58.89/59.09 inference(scs_inference,[],[73,736,102])). % 58.89/59.09 cnf(1044,plain, % 58.89/59.09 (~P3(f32(f8(f14(a1)),a4),a4)), % 58.89/59.09 inference(scs_inference,[],[73,776,102])). % 58.89/59.09 cnf(1048,plain, % 58.89/59.09 (E(f32(a7,a36),a7)), % 58.89/59.09 inference(scs_inference,[],[81,90,126])). % 58.89/59.09 cnf(1049,plain, % 58.89/59.09 (E(a7,f32(a7,a36))), % 58.89/59.09 inference(scs_inference,[],[1048,2])). % 58.89/59.09 cnf(1050,plain, % 58.89/59.09 (E(f33(a4,a7),f32(a7,a36))), % 58.89/59.09 inference(scs_inference,[],[821,1048,2,3])). % 58.89/59.09 cnf(1051,plain, % 58.89/59.09 (P1(f32(a7,a36))), % 58.89/59.09 inference(scs_inference,[],[277,821,1048,2,3,57])). % 58.89/59.09 cnf(1053,plain, % 58.89/59.09 (~P2(f32(a7,a36),f5(a1))), % 58.89/59.09 inference(scs_inference,[],[277,821,1048,2,3,57,334,155])). % 58.89/59.09 cnf(1261,plain, % 58.89/59.09 (~E(f8(f14(a1)),a4)), % 58.89/59.09 inference(scs_inference,[],[82,76,75,92,123])). % 58.89/59.09 cnf(1262,plain, % 58.89/59.09 (P4(f37(a36,f8(f14(a1))))+~P1(f8(f14(a1)))), % 58.89/59.09 inference(scs_inference,[],[74,1261,248])). % 58.89/59.09 cnf(1269,plain, % 58.89/59.09 (~E(a4,f31(a36))+~P1(f8(f14(a1)))), % 58.89/59.09 inference(scs_inference,[],[1261,776,563,73,143,66])). % 58.89/59.09 cnf(1277,plain, % 58.89/59.09 (~P1(f8(f14(a1)))+~P2(x12771,f37(a36,f8(f14(a1))))+P10(x12771,a36,f8(f14(a1)))), % 58.89/59.09 inference(scs_inference,[],[74,1261,269])). % 58.89/59.09 cnf(1400,plain, % 58.89/59.09 (~P1(f8(f14(a1)))+~P9(f8(f14(a1)))+~P2(x14001,f37(a4,f8(f14(a1))))+P10(x14001,a4,f8(f14(a1)))), % 58.89/59.09 inference(scs_inference,[],[1261,304,301])). % 58.89/59.09 cnf(1630,plain, % 58.89/59.09 (~P4(f14(a1))+~P7(a6,f14(a1))), % 58.89/59.09 inference(scs_inference,[],[338,311,147])). % 58.89/59.09 cnf(1793,plain, % 58.89/59.09 (~P1(f8(f14(a1)))+P4(x17931)+~E(x17931,f37(f32(a7,a36),f8(f14(a1))))), % 58.89/59.09 inference(scs_inference,[],[1261,1051,119])). % 58.89/59.09 cnf(2020,plain, % 58.89/59.09 (P4(f37(a4,f8(f14(a1))))), % 58.89/59.09 inference(scs_inference,[],[82,76,75,140,123])). % 58.89/59.09 cnf(2145,plain, % 58.89/59.09 (P10(f32(a7,a36),a7,f8(f14(a1)))+~P1(f8(f14(a1)))), % 58.89/59.09 inference(scs_inference,[],[277,1261,1049,736,102,156,69,67])). % 58.89/59.09 cnf(2146,plain, % 58.89/59.09 (P10(a7,f32(a7,a36),f8(f14(a1)))+~P1(f8(f14(a1)))), % 58.89/59.09 inference(scs_inference,[],[277,1261,1049,736,102,156,69,67,68])). % 58.89/59.09 cnf(2659,plain, % 58.89/59.09 (~E(a4,f31(a36))), % 58.89/59.09 inference(scs_inference,[],[287,1269,98])). % 58.89/59.09 cnf(2660,plain, % 58.89/59.09 (P3(f20(a4),a4)+E(a4,a36)), % 58.89/59.09 inference(scs_inference,[],[2659,73,104])). % 58.89/59.09 cnf(2663,plain, % 58.89/59.09 (P3(f20(a4),f32(a4,f31(f31(a36))))+E(a4,a36)), % 58.89/59.09 inference(scs_inference,[],[1049,737,1041,2659,73,104,65,70,66])). % 58.89/59.09 cnf(3016,plain, % 58.89/59.09 (E(f37(a4,f8(f14(a1))),f14(a1))), % 58.89/59.09 inference(scs_inference,[],[82,76,75,112,123])). % 58.89/59.09 cnf(3024,plain, % 58.89/59.09 (P2(f37(a4,f8(f14(a1))),a1)), % 58.89/59.09 inference(scs_inference,[],[81,313,337,281,2020,3016,2,60,58,147,1630,70,59])). % 58.89/59.09 cnf(3029,plain, % 58.89/59.09 (~P1(f8(f14(a1)))+P6(f14(a1))), % 58.89/59.09 inference(scs_inference,[],[81,313,337,1261,281,2020,3016,73,2,60,58,147,1630,70,59,71,57,61,62,124])). % 58.89/59.09 cnf(3266,plain, % 58.89/59.09 (~P2(a36,f37(a4,f8(f14(a1))))), % 58.89/59.09 inference(scs_inference,[],[3024,323,74,150])). % 58.89/59.09 cnf(3268,plain, % 58.89/59.09 (~E(f32(f8(f14(a1)),f31(a36)),f33(a36,f31(a4)))), % 58.89/59.09 inference(scs_inference,[],[304,3024,287,323,74,150,204])). % 58.89/59.09 cnf(3272,plain, % 58.89/59.09 (~P10(a36,a4,f8(f14(a1)))), % 58.89/59.09 inference(scs_inference,[],[304,3024,287,323,74,150,204,212,217])). % 58.89/59.09 cnf(3276,plain, % 58.89/59.09 (~P2(a4,f37(a36,f8(f14(a1))))+~P1(f8(f14(a1)))), % 58.89/59.09 inference(scs_inference,[],[304,3024,1261,287,323,73,74,150,204,212,217,216,1277])). % 58.89/59.09 cnf(3282,plain, % 58.89/59.09 (~P2(f31(a36),f37(a4,f8(f14(a1))))), % 58.89/59.09 inference(scs_inference,[],[304,3266,3024,311,306,2020,59,147,150])). % 58.89/59.09 cnf(3284,plain, % 58.89/59.09 (~E(f32(f8(f14(a1)),f31(a36)),f33(f31(a36),f31(a4)))), % 58.89/59.09 inference(scs_inference,[],[304,3266,3024,311,287,306,2020,59,147,150,204])). % 58.89/59.09 cnf(3286,plain, % 58.89/59.09 (~P10(f31(a36),a4,f8(f14(a1)))), % 58.89/59.09 inference(scs_inference,[],[304,3266,3024,311,287,306,2020,59,147,150,204,217])). % 58.89/59.09 cnf(3295,plain, % 58.89/59.09 (~P10(a7,a4,f8(f14(a1)))), % 58.89/59.09 inference(scs_inference,[],[304,3024,287,279,277,150,204,217])). % 58.89/59.09 cnf(3303,plain, % 58.89/59.09 (~P2(f33(a4,a7),f37(a4,f8(f14(a1))))), % 58.89/59.09 inference(scs_inference,[],[3024,825,823,150])). % 58.89/59.09 cnf(3309,plain, % 58.89/59.09 (~P10(f33(a4,a7),a4,f8(f14(a1)))), % 58.89/59.09 inference(scs_inference,[],[304,3024,287,825,823,150,204,212,217])). % 58.89/59.09 cnf(3320,plain, % 58.89/59.09 (~P3(f8(f14(a1)),f33(f32(a7,a36),f31(a4)))), % 58.89/59.09 inference(scs_inference,[],[304,3024,287,1053,1051,150,204,217,212])). % 58.89/59.09 cnf(4292,plain, % 58.89/59.09 (~E(f31(a36),a4)), % 58.89/59.09 inference(scs_inference,[],[2659,2])). % 58.89/59.09 cnf(4297,plain, % 58.89/59.09 (P2(f33(a4,a7),f37(f33(a4,a7),f31(a36)))), % 58.89/59.09 inference(scs_inference,[],[823,304,2659,2,156,248,271])). % 58.89/59.09 cnf(4300,plain, % 58.89/59.09 (P10(f33(a4,a7),a7,f31(a36))), % 58.89/59.09 inference(scs_inference,[],[823,304,821,2659,2,156,248,271,69,68])). % 58.89/59.09 cnf(4307,plain, % 58.89/59.09 (~E(f5(a1),f30(f5(a1)))), % 58.89/59.09 inference(scs_inference,[],[283,2])). % 58.89/59.09 cnf(4309,plain, % 58.89/59.09 (P10(a7,a7,f31(a36))), % 58.89/59.09 inference(scs_inference,[],[4300,821,1049,283,2,68,67])). % 58.89/59.09 cnf(4318,plain, % 58.89/59.09 (P10(f32(a7,a36),a7,f31(a36))), % 58.89/59.09 inference(scs_inference,[],[4309,308,1049,3268,4307,2,3,68,67])). % 58.89/59.09 cnf(4326,plain, % 58.89/59.09 (P10(f32(a7,a36),f32(a7,a36),f31(a36))), % 58.89/59.09 inference(scs_inference,[],[4318,1049,3284,2,68])). % 58.89/59.09 cnf(4422,plain, % 58.89/59.09 (~P3(a4,a4)), % 58.89/59.09 inference(scs_inference,[],[777,1044,65])). % 58.89/59.09 cnf(4457,plain, % 58.89/59.09 (~P3(x44571,a36)+~E(x44571,f8(f14(a1)))), % 58.89/59.09 inference(scs_inference,[],[531,65])). % 58.89/59.09 cnf(4464,plain, % 58.89/59.09 (~P3(x44641,f31(a36))+~E(x44641,f8(f14(a1)))), % 58.89/59.09 inference(scs_inference,[],[563,65])). % 58.89/59.09 cnf(4471,plain, % 58.89/59.09 (~P3(f8(f14(a1)),x44711)+~E(x44711,a36)), % 58.89/59.09 inference(scs_inference,[],[531,66])). % 58.89/59.09 cnf(4472,plain, % 58.89/59.09 (~E(a4,a36)+~P1(f8(f14(a1)))), % 58.89/59.09 inference(scs_inference,[],[1261,776,531,73,66,143])). % 58.89/59.09 cnf(4501,plain, % 58.89/59.09 (P3(f20(a4),a4)+~P1(f8(f14(a1)))), % 58.89/59.09 inference(scs_inference,[],[4472,2660])). % 58.89/59.09 cnf(4573,plain, % 58.89/59.09 (~E(f20(a4),a4)+~P1(f8(f14(a1)))), % 58.89/59.09 inference(scs_inference,[],[4422,4501,65])). % 58.89/59.09 cnf(4605,plain, % 58.89/59.09 (~E(f20(a4),a4)), % 58.89/59.09 inference(scs_inference,[],[287,4573,98])). % 58.89/59.09 cnf(5135,plain, % 58.89/59.09 (P4(x51351)+~P9(f8(f14(a1)))+~P1(f8(f14(a1)))+~E(x51351,f37(f31(f8(f14(a1))),f31(a36)))), % 58.89/59.09 inference(scs_inference,[],[3303,4292,1261,287,499,823,304,3016,3309,1400,212,133,119])). % 58.89/59.09 cnf(5136,plain, % 58.89/59.09 (P4(f37(f31(f8(f14(a1))),f31(a36)))+~P9(f8(f14(a1)))+~P1(f8(f14(a1)))), % 58.89/59.09 inference(equality_inference,[],[5135])). % 58.89/59.09 cnf(5145,plain, % 58.89/59.09 (P4(x51451)+~P9(f8(f14(a1)))+~P1(f8(f14(a1)))+~E(x51451,f37(f32(a4,f31(f31(a36))),f31(a36)))), % 58.89/59.09 inference(scs_inference,[],[3282,4292,287,738,304,308,3286,1400,212,119])). % 58.89/59.09 cnf(5146,plain, % 58.89/59.09 (P4(f37(f32(a4,f31(f31(a36))),f31(a36)))+~P9(f8(f14(a1)))+~P1(f8(f14(a1)))), % 58.89/59.09 inference(equality_inference,[],[5145])). % 58.89/59.09 cnf(5165,plain, % 58.89/59.09 (P4(x51651)+~P9(f8(f14(a1)))+~P1(f8(f14(a1)))+~E(x51651,f37(f32(f8(f14(a1)),a4),f31(a36)))), % 58.89/59.09 inference(scs_inference,[],[3266,4292,287,780,304,74,3272,1400,212,119])). % 58.89/59.09 cnf(5166,plain, % 58.89/59.09 (P4(f37(f32(f8(f14(a1)),a4),f31(a36)))+~P9(f8(f14(a1)))+~P1(f8(f14(a1)))), % 58.89/59.09 inference(equality_inference,[],[5165])). % 58.89/59.09 cnf(5191,plain, % 58.89/59.09 (P2(a7,f37(a7,f31(a36)))), % 58.89/59.09 inference(scs_inference,[],[4309,4292,277,304,248,271])). % 58.89/59.09 cnf(5499,plain, % 58.89/59.09 (E(f33(a4,a4),a4)), % 58.89/59.09 inference(scs_inference,[],[73,287,499,84,242,99,88,89])). % 58.89/59.09 cnf(5524,plain, % 58.89/59.09 (E(f37(f33(a4,a7),x55241),f37(f32(a7,a36),x55241))), % 58.89/59.09 inference(scs_inference,[],[1028,1050,73,277,287,499,84,242,99,88,89,90,85,86,4,5,9,12,15,36,41,42,45,50,51,56,93,94,4457,10])). % 58.89/59.09 cnf(5572,plain, % 58.89/59.09 (P1(f8(f14(a1)))), % 58.89/59.09 inference(scs_inference,[],[1028,1050,73,277,74,287,499,84,242,99,88,89,90,85,86,4,5,9,12,15,36,41,42,45,50,51,56,93,94,4457,10,11,13,14,16,17,24,25,32,33,34,35,37,38,39,40,43,44,46,47,48,49,52,53,54,55,95,96,4464,6,7,8,18,19,20,21,22,23,26,27,28,29,30,31,87,98])). % 58.89/59.09 cnf(5575,plain, % 58.89/59.09 (P1(f33(a4,a4))), % 58.89/59.09 inference(scs_inference,[],[1012,1028,1050,73,277,74,287,499,84,242,99,88,89,90,85,86,4,5,9,12,15,36,41,42,45,50,51,56,93,94,4457,10,11,13,14,16,17,24,25,32,33,34,35,37,38,39,40,43,44,46,47,48,49,52,53,54,55,95,96,4464,6,7,8,18,19,20,21,22,23,26,27,28,29,30,31,87,98,2,120])). % 58.89/59.09 cnf(5577,plain, % 58.89/59.09 (P1(f32(a4,a4))), % 58.89/59.09 inference(scs_inference,[],[1012,1028,1050,73,277,74,287,499,84,242,99,88,89,90,85,86,4,5,9,12,15,36,41,42,45,50,51,56,93,94,4457,10,11,13,14,16,17,24,25,32,33,34,35,37,38,39,40,43,44,46,47,48,49,52,53,54,55,95,96,4464,6,7,8,18,19,20,21,22,23,26,27,28,29,30,31,87,98,2,120,121])). % 58.89/59.09 cnf(5593,plain, % 58.89/59.09 (~P10(a7,a4,f33(f8(f14(a1)),a4))), % 58.89/59.09 inference(scs_inference,[],[1012,1028,1050,1261,736,4292,73,277,74,304,287,3295,499,84,242,99,88,89,90,85,86,4,5,9,12,15,36,41,42,45,50,51,56,93,94,4457,10,11,13,14,16,17,24,25,32,33,34,35,37,38,39,40,43,44,46,47,48,49,52,53,54,55,95,96,4464,6,7,8,18,19,20,21,22,23,26,27,28,29,30,31,87,98,2,120,121,108,136,141,166,1793,5136,5146,5166,68,69])). % 58.89/59.09 cnf(5595,plain, % 58.89/59.09 (~P10(f33(a4,a36),a4,f8(f14(a1)))), % 58.89/59.09 inference(scs_inference,[],[1012,1028,1050,1261,736,4292,73,277,74,304,287,3295,3272,499,84,242,99,88,89,90,85,86,4,5,9,12,15,36,41,42,45,50,51,56,93,94,4457,10,11,13,14,16,17,24,25,32,33,34,35,37,38,39,40,43,44,46,47,48,49,52,53,54,55,95,96,4464,6,7,8,18,19,20,21,22,23,26,27,28,29,30,31,87,98,2,120,121,108,136,141,166,1793,5136,5146,5166,68,69,60,67])). % 58.89/59.09 cnf(5596,plain, % 58.89/59.09 (P2(f33(a4,a7),f37(a7,f31(a36)))), % 58.89/59.09 inference(scs_inference,[],[1012,1028,1050,5191,822,1261,736,4292,73,277,74,304,287,3295,3272,499,84,242,99,88,89,90,85,86,4,5,9,12,15,36,41,42,45,50,51,56,93,94,4457,10,11,13,14,16,17,24,25,32,33,34,35,37,38,39,40,43,44,46,47,48,49,52,53,54,55,95,96,4464,6,7,8,18,19,20,21,22,23,26,27,28,29,30,31,87,98,2,120,121,108,136,141,166,1793,5136,5146,5166,68,69,60,67,58])). % 58.89/59.09 cnf(5618,plain, % 58.89/59.09 (P7(f37(a4,f8(f14(a1))),a3)), % 58.89/59.09 inference(scs_inference,[],[1012,1028,828,3320,1050,5191,822,1261,4297,736,4292,73,277,74,304,287,3295,3272,499,84,242,99,88,89,90,85,86,4,5,9,12,15,36,41,42,45,50,51,56,93,94,4457,10,11,13,14,16,17,24,25,32,33,34,35,37,38,39,40,43,44,46,47,48,49,52,53,54,55,95,96,4464,6,7,8,18,19,20,21,22,23,26,27,28,29,30,31,87,98,2,120,121,108,136,141,166,1793,5136,5146,5166,68,69,60,67,58,65,3,102,59,171,172,173,193,194,191,124,184,137])). % 58.89/59.09 cnf(5632,plain, % 58.89/59.09 (P3(f8(f14(a1)),a4)), % 58.89/59.09 inference(scs_inference,[],[1012,1028,4326,828,3320,285,1050,4318,5191,822,1261,4297,736,4292,776,73,277,74,304,287,3295,3272,499,1051,84,242,99,88,89,90,85,86,4,5,9,12,15,36,41,42,45,50,51,56,93,94,4457,10,11,13,14,16,17,24,25,32,33,34,35,37,38,39,40,43,44,46,47,48,49,52,53,54,55,95,96,4464,6,7,8,18,19,20,21,22,23,26,27,28,29,30,31,87,98,2,120,121,108,136,141,166,1793,5136,5146,5166,68,69,60,67,58,65,3,102,59,171,172,173,193,194,191,124,184,137,113,201,133,255,301,215,143])). % 58.89/59.09 cnf(5639,plain, % 58.89/59.09 (~E(a4,a36)), % 58.89/59.09 inference(scs_inference,[],[1012,1028,4326,828,3320,285,1050,3303,4318,5191,822,1261,4297,736,4292,776,73,277,74,304,287,3295,3272,499,823,1051,84,242,99,88,89,90,85,86,4,5,9,12,15,36,41,42,45,50,51,56,93,94,4457,10,11,13,14,16,17,24,25,32,33,34,35,37,38,39,40,43,44,46,47,48,49,52,53,54,55,95,96,4464,6,7,8,18,19,20,21,22,23,26,27,28,29,30,31,87,98,2,120,121,108,136,141,166,1793,5136,5146,5166,68,69,60,67,58,65,3,102,59,171,172,173,193,194,191,124,184,137,113,201,133,255,301,215,143,299,97,352,4471])). % 58.89/59.09 cnf(5642,plain, % 58.89/59.09 (P3(f20(a4),f32(a4,f31(f31(a36))))), % 58.89/59.09 inference(scs_inference,[],[1012,1028,4326,828,3320,285,1050,3303,4318,5191,822,1261,4297,736,4292,776,73,277,74,304,287,3295,3272,499,823,1051,84,242,99,88,89,90,85,86,4,5,9,12,15,36,41,42,45,50,51,56,93,94,4457,10,11,13,14,16,17,24,25,32,33,34,35,37,38,39,40,43,44,46,47,48,49,52,53,54,55,95,96,4464,6,7,8,18,19,20,21,22,23,26,27,28,29,30,31,87,98,2,120,121,108,136,141,166,1793,5136,5146,5166,68,69,60,67,58,65,3,102,59,171,172,173,193,194,191,124,184,137,113,201,133,255,301,215,143,299,97,352,4471,342,1262,2663])). % 58.89/59.09 cnf(5643,plain, % 58.89/59.09 (~P2(a4,f37(a36,f8(f14(a1))))), % 58.89/59.09 inference(scs_inference,[],[1012,1028,4326,828,3320,285,1050,3303,4318,5191,822,1261,4297,736,4292,776,73,277,74,304,287,3295,3272,499,823,1051,84,242,99,88,89,90,85,86,4,5,9,12,15,36,41,42,45,50,51,56,93,94,4457,10,11,13,14,16,17,24,25,32,33,34,35,37,38,39,40,43,44,46,47,48,49,52,53,54,55,95,96,4464,6,7,8,18,19,20,21,22,23,26,27,28,29,30,31,87,98,2,120,121,108,136,141,166,1793,5136,5146,5166,68,69,60,67,58,65,3,102,59,171,172,173,193,194,191,124,184,137,113,201,133,255,301,215,143,299,97,352,4471,342,1262,2663,3276])). % 58.89/59.09 cnf(5644,plain, % 58.89/59.09 (P10(f32(a7,a36),a7,f8(f14(a1)))), % 58.89/59.09 inference(scs_inference,[],[1012,1028,4326,828,3320,285,1050,3303,4318,5191,822,1261,4297,736,4292,776,73,277,74,304,287,3295,3272,499,823,1051,84,242,99,88,89,90,85,86,4,5,9,12,15,36,41,42,45,50,51,56,93,94,4457,10,11,13,14,16,17,24,25,32,33,34,35,37,38,39,40,43,44,46,47,48,49,52,53,54,55,95,96,4464,6,7,8,18,19,20,21,22,23,26,27,28,29,30,31,87,98,2,120,121,108,136,141,166,1793,5136,5146,5166,68,69,60,67,58,65,3,102,59,171,172,173,193,194,191,124,184,137,113,201,133,255,301,215,143,299,97,352,4471,342,1262,2663,3276,2145])). % 58.89/59.09 cnf(5646,plain, % 58.89/59.09 (P6(f14(a1))), % 58.89/59.09 inference(scs_inference,[],[1012,1028,4326,828,3320,285,1050,3303,4318,5191,822,1261,4297,736,4292,776,73,277,74,304,287,3295,3272,499,823,1051,84,242,99,88,89,90,85,86,4,5,9,12,15,36,41,42,45,50,51,56,93,94,4457,10,11,13,14,16,17,24,25,32,33,34,35,37,38,39,40,43,44,46,47,48,49,52,53,54,55,95,96,4464,6,7,8,18,19,20,21,22,23,26,27,28,29,30,31,87,98,2,120,121,108,136,141,166,1793,5136,5146,5166,68,69,60,67,58,65,3,102,59,171,172,173,193,194,191,124,184,137,113,201,133,255,301,215,143,299,97,352,4471,342,1262,2663,3276,2145,2146,3029])). % 58.89/59.09 cnf(5908,plain, % 58.89/59.09 ($false), % 58.89/59.09 inference(scs_inference,[],[5639,5575,5577,5499,5646,5632,5596,5572,5595,5644,5524,5643,5642,5618,5593,828,1048,737,4297,76,82,2659,1261,75,4292,4605,277,73,3016,304,738,823,1051,85,242,84,90,89,46,96,95,51,40,21,19,93,33,34,9,16,54,38,27,15,24,41,88,42,39,86,5,45,31,6,35,47,44,30,37,48,52,10,13,94,53,50,56,4,11,17,7,87,22,20,32,12,43,25,29,26,8,23,36,49,55,18,28,14,2,166,141,142,120,121,129,57,63,67,58,106,68,62,3,59,171,173,91,172,193,124,194,184,137,156,248,297,165,268,146,201,158]), % 58.89/59.09 ['proof']). % 58.89/59.09 % SZS output end Proof % 58.89/59.09 % Total time :58.290000s %------------------------------------------------------------------------------