%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM450+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 : n022.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.86s 58.96s % Output : CNFRefutation 58.86s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NUM450+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.33 % Computer : n022.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:11:08 EDT 2024 % 0.12/0.33 % CPUTime : % 0.48/0.58 start to proof:theBenchmark % 58.86/58.93 %------------------------------------------- % 58.86/58.93 % File :CSE---1.7 % 58.86/58.93 % Problem :theBenchmark % 58.86/58.93 % Transform :cnf % 58.86/58.93 % Format :tptp:raw % 58.86/58.93 % Command :java -jar mcs_scs.jar %d %s % 58.86/58.93 % 58.86/58.93 % Result :Theorem 58.230000s % 58.86/58.93 % Output :CNFRefutation 58.230000s % 58.86/58.93 %------------------------------------------- % 58.86/58.94 %------------------------------------------------------------------------------ % 58.86/58.94 % File : NUM450+6 : TPTP v8.2.0. Released v4.0.0. % 58.86/58.94 % Domain : Number Theory % 58.86/58.94 % Problem : Fuerstenberg's infinitude of primes 11_03, 05 expansion % 58.86/58.94 % Version : Especial. % 58.86/58.94 % English : % 58.86/58.94 % 58.86/58.94 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 58.86/58.94 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 58.86/58.94 % Source : [Pas08] % 58.86/58.94 % Names : fuerst_11_03.05 [Pas08] % 58.86/58.94 % 58.86/58.94 % Status : Theorem % 58.86/58.94 % Rating : 0.11 v8.1.0, 0.03 v7.3.0, 0.10 v7.1.0, 0.13 v7.0.0, 0.17 v6.4.0, 0.19 v6.3.0, 0.12 v6.2.0, 0.20 v6.1.0, 0.27 v6.0.0, 0.26 v5.5.0, 0.30 v5.4.0, 0.36 v5.3.0, 0.37 v5.2.0, 0.30 v5.1.0, 0.38 v5.0.0, 0.42 v4.1.0, 0.48 v4.0.1, 0.74 v4.0.0 % 58.86/58.94 % Syntax : Number of formulae : 46 ( 3 unt; 10 def) % 58.86/58.94 % Number of atoms : 320 ( 59 equ) % 58.86/58.94 % Maximal formula atoms : 56 ( 6 avg) % 58.86/58.94 % Number of connectives : 297 ( 23 ~; 14 |; 163 &) % 58.86/58.94 % ( 25 <=>; 72 =>; 0 <=; 0 <~>) % 58.86/58.94 % Maximal formula depth : 24 ( 7 avg) % 58.86/58.94 % Maximal term depth : 3 ( 1 avg) % 58.86/58.94 % Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty) % 58.86/58.94 % Number of functors : 14 ( 14 usr; 6 con; 0-2 aty) % 58.86/58.94 % Number of variables : 128 ( 105 !; 23 ?) % 58.86/58.94 % SPC : FOF_THM_RFO_SEQ % 58.86/58.94 % 58.86/58.94 % Comments : Problem generated by the SAD system [VLP07] % 58.86/58.94 %------------------------------------------------------------------------------ % 58.86/58.94 fof(mIntegers,axiom, % 58.86/58.94 ! [W0] : % 58.86/58.94 ( aInteger0(W0) % 58.86/58.94 => $true ) ). % 58.86/58.94 % 58.86/58.94 fof(mIntZero,axiom, % 58.86/58.94 aInteger0(sz00) ). % 58.86/58.94 % 58.86/58.94 fof(mIntOne,axiom, % 58.86/58.94 aInteger0(sz10) ). % 58.86/58.94 % 58.86/58.94 fof(mIntNeg,axiom, % 58.86/58.94 ! [W0] : % 58.86/58.94 ( aInteger0(W0) % 58.86/58.94 => aInteger0(smndt0(W0)) ) ). % 58.86/58.94 % 58.86/58.94 fof(mIntPlus,axiom, % 58.86/58.94 ! [W0,W1] : % 58.86/58.94 ( ( aInteger0(W0) % 58.86/58.94 & aInteger0(W1) ) % 58.86/58.94 => aInteger0(sdtpldt0(W0,W1)) ) ). % 58.86/58.94 % 58.86/58.94 fof(mIntMult,axiom, % 58.86/58.94 ! [W0,W1] : % 58.86/58.94 ( ( aInteger0(W0) % 58.86/58.94 & aInteger0(W1) ) % 58.86/58.94 => aInteger0(sdtasdt0(W0,W1)) ) ). % 58.86/58.94 % 58.86/58.94 fof(mAddAsso,axiom, % 58.86/58.94 ! [W0,W1,W2] : % 58.86/58.94 ( ( aInteger0(W0) % 58.86/58.94 & aInteger0(W1) % 58.86/58.94 & aInteger0(W2) ) % 58.86/58.94 => sdtpldt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtpldt0(W0,W1),W2) ) ). % 58.86/58.94 % 58.86/58.94 fof(mAddComm,axiom, % 58.86/58.94 ! [W0,W1] : % 58.86/58.94 ( ( aInteger0(W0) % 58.86/58.94 & aInteger0(W1) ) % 58.86/58.94 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 58.86/58.94 % 58.86/58.94 fof(mAddZero,axiom, % 58.86/58.94 ! [W0] : % 58.86/58.94 ( aInteger0(W0) % 58.86/58.94 => ( sdtpldt0(W0,sz00) = W0 % 58.86/58.94 & W0 = sdtpldt0(sz00,W0) ) ) ). % 58.86/58.94 % 58.86/58.94 fof(mAddNeg,axiom, % 58.86/58.94 ! [W0] : % 58.86/58.94 ( aInteger0(W0) % 58.86/58.94 => ( sdtpldt0(W0,smndt0(W0)) = sz00 % 58.86/58.94 & sz00 = sdtpldt0(smndt0(W0),W0) ) ) ). % 58.86/58.94 % 58.86/58.94 fof(mMulAsso,axiom, % 58.86/58.94 ! [W0,W1,W2] : % 58.86/58.94 ( ( aInteger0(W0) % 58.86/58.94 & aInteger0(W1) % 58.86/58.94 & aInteger0(W2) ) % 58.86/58.94 => sdtasdt0(W0,sdtasdt0(W1,W2)) = sdtasdt0(sdtasdt0(W0,W1),W2) ) ). % 58.86/58.94 % 58.86/58.94 fof(mMulComm,axiom, % 58.86/58.94 ! [W0,W1] : % 58.86/58.94 ( ( aInteger0(W0) % 58.86/58.94 & aInteger0(W1) ) % 58.86/58.94 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 58.86/58.94 % 58.86/58.94 fof(mMulOne,axiom, % 58.86/58.94 ! [W0] : % 58.86/58.94 ( aInteger0(W0) % 58.86/58.94 => ( sdtasdt0(W0,sz10) = W0 % 58.86/58.94 & W0 = sdtasdt0(sz10,W0) ) ) ). % 58.86/58.94 % 58.86/58.94 fof(mDistrib,axiom, % 58.86/58.94 ! [W0,W1,W2] : % 58.86/58.94 ( ( aInteger0(W0) % 58.86/58.94 & aInteger0(W1) % 58.86/58.94 & aInteger0(W2) ) % 58.86/58.94 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 58.86/58.94 & sdtasdt0(sdtpldt0(W0,W1),W2) = sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W1,W2)) ) ) ). % 58.86/58.94 % 58.86/58.94 fof(mMulZero,axiom, % 58.86/58.94 ! [W0] : % 58.86/58.94 ( aInteger0(W0) % 58.86/58.94 => ( sdtasdt0(W0,sz00) = sz00 % 58.86/58.94 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 58.86/58.94 % 58.86/58.94 fof(mMulMinOne,axiom, % 58.86/58.94 ! [W0] : % 58.86/58.94 ( aInteger0(W0) % 58.86/58.94 => ( sdtasdt0(smndt0(sz10),W0) = smndt0(W0) % 58.86/58.94 & smndt0(W0) = sdtasdt0(W0,smndt0(sz10)) ) ) ). % 58.86/58.94 % 58.86/58.94 fof(mZeroDiv,axiom, % 58.86/58.94 ! [W0,W1] : % 58.86/58.94 ( ( aInteger0(W0) % 58.86/58.94 & aInteger0(W1) ) % 58.86/58.94 => ( sdtasdt0(W0,W1) = sz00 % 58.86/58.94 => ( W0 = sz00 % 58.86/58.94 | W1 = sz00 ) ) ) ). % 58.86/58.94 % 58.86/58.94 fof(mDivisor,definition, % 58.86/58.94 ! [W0] : % 58.86/58.94 ( aInteger0(W0) % 58.86/58.94 => ! [W1] : % 58.86/58.94 ( aDivisorOf0(W1,W0) % 58.86/58.94 <=> ( aInteger0(W1) % 58.86/58.94 & W1 != sz00 % 58.86/58.94 & ? [W2] : % 58.86/58.94 ( aInteger0(W2) % 58.86/58.94 & sdtasdt0(W1,W2) = W0 ) ) ) ) ). % 58.86/58.94 % 58.86/58.94 fof(mEquMod,definition, % 58.86/58.94 ! [W0,W1,W2] : % 58.86/58.94 ( ( aInteger0(W0) % 58.86/58.94 & aInteger0(W1) % 58.86/58.94 & aInteger0(W2) % 58.86/58.94 & W2 != sz00 ) % 58.86/58.94 => ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 58.86/58.94 <=> aDivisorOf0(W2,sdtpldt0(W0,smndt0(W1))) ) ) ). % 58.86/58.94 % 58.86/58.94 fof(mEquModRef,axiom, % 58.86/58.94 ! [W0,W1] : % 58.86/58.94 ( ( aInteger0(W0) % 58.86/58.94 & aInteger0(W1) % 58.86/58.94 & W1 != sz00 ) % 58.86/58.94 => sdteqdtlpzmzozddtrp0(W0,W0,W1) ) ). % 58.86/58.94 % 58.86/58.94 fof(mEquModSym,axiom, % 58.86/58.94 ! [W0,W1,W2] : % 58.86/58.94 ( ( aInteger0(W0) % 58.86/58.94 & aInteger0(W1) % 58.86/58.94 & aInteger0(W2) % 58.86/58.94 & W2 != sz00 ) % 58.86/58.94 => ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 58.86/58.94 => sdteqdtlpzmzozddtrp0(W1,W0,W2) ) ) ). % 58.86/58.94 % 58.86/58.95 fof(mEquModTrn,axiom, % 58.86/58.95 ! [W0,W1,W2,W3] : % 58.86/58.95 ( ( aInteger0(W0) % 58.86/58.95 & aInteger0(W1) % 58.86/58.95 & aInteger0(W2) % 58.86/58.95 & W2 != sz00 % 58.86/58.95 & aInteger0(W3) ) % 58.86/58.95 => ( ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 58.86/58.95 & sdteqdtlpzmzozddtrp0(W1,W3,W2) ) % 58.86/58.95 => sdteqdtlpzmzozddtrp0(W0,W3,W2) ) ) ). % 58.86/58.95 % 58.86/58.95 fof(mEquModMul,axiom, % 58.86/58.95 ! [W0,W1,W2,W3] : % 58.86/58.95 ( ( aInteger0(W0) % 58.86/58.95 & aInteger0(W1) % 58.86/58.95 & aInteger0(W2) % 58.86/58.95 & W2 != sz00 % 58.86/58.95 & aInteger0(W3) % 58.86/58.95 & W3 != sz00 ) % 58.86/58.95 => ( sdteqdtlpzmzozddtrp0(W0,W1,sdtasdt0(W2,W3)) % 58.86/58.95 => ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 58.86/58.95 & sdteqdtlpzmzozddtrp0(W0,W1,W3) ) ) ) ). % 58.86/58.95 % 58.86/58.95 fof(mPrime,axiom, % 58.86/58.95 ! [W0] : % 58.86/58.95 ( ( aInteger0(W0) % 58.86/58.95 & W0 != sz00 ) % 58.86/58.95 => ( isPrime0(W0) % 58.86/58.95 => $true ) ) ). % 58.86/58.95 % 58.86/58.95 fof(mPrimeDivisor,axiom, % 58.86/58.95 ! [W0] : % 58.86/58.95 ( aInteger0(W0) % 58.86/58.95 => ( ? [W1] : % 58.86/58.95 ( aDivisorOf0(W1,W0) % 58.86/58.95 & isPrime0(W1) ) % 58.86/58.95 <=> ( W0 != sz10 % 58.86/58.95 & W0 != smndt0(sz10) ) ) ) ). % 58.86/58.95 % 58.86/58.95 fof(mSets,axiom, % 58.86/58.95 ! [W0] : % 58.86/58.95 ( aSet0(W0) % 58.86/58.95 => $true ) ). % 58.86/58.95 % 58.86/58.95 fof(mElements,axiom, % 58.86/58.95 ! [W0] : % 58.86/58.95 ( aSet0(W0) % 58.86/58.95 => ! [W1] : % 58.86/58.95 ( aElementOf0(W1,W0) % 58.86/58.95 => $true ) ) ). % 58.86/58.95 % 58.86/58.95 fof(mSubset,definition, % 58.86/58.95 ! [W0] : % 58.86/58.95 ( aSet0(W0) % 58.86/58.95 => ! [W1] : % 58.86/58.95 ( aSubsetOf0(W1,W0) % 58.86/58.95 <=> ( aSet0(W1) % 58.86/58.95 & ! [W2] : % 58.86/58.95 ( aElementOf0(W2,W1) % 58.86/58.95 => aElementOf0(W2,W0) ) ) ) ) ). % 58.86/58.95 % 58.86/58.95 fof(mFinSet,axiom, % 58.86/58.95 ! [W0] : % 58.86/58.95 ( aSet0(W0) % 58.86/58.95 => ( isFinite0(W0) % 58.86/58.95 => $true ) ) ). % 58.86/58.95 % 58.86/58.95 fof(mUnion,definition, % 58.86/58.95 ! [W0,W1] : % 58.86/58.95 ( ( aSubsetOf0(W0,cS1395) % 58.86/58.95 & aSubsetOf0(W1,cS1395) ) % 58.86/58.95 => ! [W2] : % 58.86/58.95 ( W2 = sdtbsmnsldt0(W0,W1) % 58.86/58.95 <=> ( aSet0(W2) % 58.86/58.95 & ! [W3] : % 58.86/58.95 ( aElementOf0(W3,W2) % 58.86/58.95 <=> ( aInteger0(W3) % 58.86/58.95 & ( aElementOf0(W3,W0) % 58.86/58.95 | aElementOf0(W3,W1) ) ) ) ) ) ) ). % 58.86/58.95 % 58.86/58.95 fof(mIntersection,definition, % 58.86/58.95 ! [W0,W1] : % 58.86/58.95 ( ( aSubsetOf0(W0,cS1395) % 58.86/58.95 & aSubsetOf0(W1,cS1395) ) % 58.86/58.95 => ! [W2] : % 58.86/58.95 ( W2 = sdtslmnbsdt0(W0,W1) % 58.86/58.95 <=> ( aSet0(W2) % 58.86/58.95 & ! [W3] : % 58.86/58.95 ( aElementOf0(W3,W2) % 58.86/58.95 <=> ( aInteger0(W3) % 58.86/58.95 & aElementOf0(W3,W0) % 58.86/58.95 & aElementOf0(W3,W1) ) ) ) ) ) ). % 58.86/58.95 % 58.86/58.95 fof(mUnionSet,definition, % 58.86/58.95 ! [W0] : % 58.86/58.95 ( ( aSet0(W0) % 58.86/58.95 & ! [W1] : % 58.86/58.95 ( aElementOf0(W1,W0) % 58.86/58.95 => aSubsetOf0(W1,cS1395) ) ) % 58.86/58.95 => ! [W1] : % 58.86/58.95 ( W1 = sbsmnsldt0(W0) % 58.86/58.95 <=> ( aSet0(W1) % 58.86/58.95 & ! [W2] : % 58.86/58.95 ( aElementOf0(W2,W1) % 58.86/58.95 <=> ( aInteger0(W2) % 58.86/58.95 & ? [W3] : % 58.86/58.95 ( aElementOf0(W3,W0) % 58.86/58.95 & aElementOf0(W2,W3) ) ) ) ) ) ) ). % 58.86/58.95 % 58.86/58.95 fof(mComplement,definition, % 58.86/58.95 ! [W0] : % 58.86/58.95 ( aSubsetOf0(W0,cS1395) % 58.86/58.95 => ! [W1] : % 58.86/58.95 ( W1 = stldt0(W0) % 58.86/58.95 <=> ( aSet0(W1) % 58.86/58.95 & ! [W2] : % 58.86/58.95 ( aElementOf0(W2,W1) % 58.86/58.95 <=> ( aInteger0(W2) % 58.86/58.95 & ~ aElementOf0(W2,W0) ) ) ) ) ) ). % 58.86/58.95 % 58.86/58.95 fof(mArSeq,definition, % 58.86/58.95 ! [W0,W1] : % 58.86/58.95 ( ( aInteger0(W0) % 58.86/58.95 & aInteger0(W1) % 58.86/58.95 & W1 != sz00 ) % 58.86/58.95 => ! [W2] : % 58.86/58.95 ( W2 = szAzrzSzezqlpdtcmdtrp0(W0,W1) % 58.86/58.95 <=> ( aSet0(W2) % 58.86/58.95 & ! [W3] : % 58.86/58.95 ( aElementOf0(W3,W2) % 58.86/58.95 <=> ( aInteger0(W3) % 58.86/58.95 & sdteqdtlpzmzozddtrp0(W3,W0,W1) ) ) ) ) ) ). % 58.86/58.95 % 58.86/58.95 fof(mOpen,definition, % 58.86/58.95 ! [W0] : % 58.86/58.95 ( aSubsetOf0(W0,cS1395) % 58.86/58.95 => ( isOpen0(W0) % 58.86/58.95 <=> ! [W1] : % 58.86/58.95 ( aElementOf0(W1,W0) % 58.86/58.95 => ? [W2] : % 58.86/58.95 ( aInteger0(W2) % 58.86/58.95 & W2 != sz00 % 58.86/58.95 & aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W1,W2),W0) ) ) ) ) ). % 58.86/58.95 % 58.86/58.95 fof(mClosed,definition, % 58.86/58.95 ! [W0] : % 58.86/58.95 ( aSubsetOf0(W0,cS1395) % 58.86/58.95 => ( isClosed0(W0) % 58.86/58.95 <=> isOpen0(stldt0(W0)) ) ) ). % 58.86/58.95 % 58.86/58.95 fof(mUnionOpen,axiom, % 58.86/58.95 ! [W0] : % 58.86/58.95 ( ( aSet0(W0) % 58.86/58.95 & ! [W1] : % 58.86/58.95 ( aElementOf0(W1,W0) % 58.86/58.95 => ( aSubsetOf0(W1,cS1395) % 58.86/58.95 & isOpen0(W1) ) ) ) % 58.86/58.95 => isOpen0(sbsmnsldt0(W0)) ) ). % 58.86/58.95 % 58.86/58.95 fof(mInterOpen,axiom, % 58.86/58.95 ! [W0,W1] : % 58.86/58.95 ( ( aSubsetOf0(W0,cS1395) % 58.86/58.95 & aSubsetOf0(W1,cS1395) % 58.86/58.95 & isOpen0(W0) % 58.86/58.95 & isOpen0(W1) ) % 58.86/58.95 => isOpen0(sdtslmnbsdt0(W0,W1)) ) ). % 58.86/58.95 % 58.86/58.95 fof(mUnionClosed,axiom, % 58.86/58.95 ! [W0,W1] : % 58.86/58.95 ( ( aSubsetOf0(W0,cS1395) % 58.86/58.95 & aSubsetOf0(W1,cS1395) % 58.86/58.95 & isClosed0(W0) % 58.86/58.95 & isClosed0(W1) ) % 58.86/58.95 => isClosed0(sdtbsmnsldt0(W0,W1)) ) ). % 58.86/58.95 % 58.86/58.95 fof(mUnionSClosed,axiom, % 58.86/58.95 ! [W0] : % 58.86/58.95 ( ( aSet0(W0) % 58.86/58.95 & isFinite0(W0) % 58.86/58.95 & ! [W1] : % 58.86/58.95 ( aElementOf0(W1,W0) % 58.86/58.95 => ( aSubsetOf0(W1,cS1395) % 58.86/58.95 & isClosed0(W1) ) ) ) % 58.86/58.95 => isClosed0(sbsmnsldt0(W0)) ) ). % 58.86/58.95 % 58.86/58.95 fof(mArSeqClosed,axiom, % 58.86/58.95 ! [W0,W1] : % 58.86/58.95 ( ( aInteger0(W0) % 58.86/58.95 & aInteger0(W1) % 58.86/58.95 & W1 != sz00 ) % 58.86/58.95 => ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),cS1395) % 58.86/58.95 & isClosed0(szAzrzSzezqlpdtcmdtrp0(W0,W1)) ) ) ). % 58.86/58.95 % 58.86/58.95 fof(m__2046,hypothesis, % 58.86/58.95 ( aSet0(xS) % 58.86/58.95 & ! [W0] : % 58.86/58.95 ( ( aElementOf0(W0,xS) % 58.86/58.95 => ? [W1] : % 58.86/58.95 ( aInteger0(W1) % 58.86/58.95 & W1 != sz00 % 58.86/58.95 & isPrime0(W1) % 58.86/58.95 & aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,W1)) % 58.86/58.95 & ! [W2] : % 58.86/58.95 ( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1)) % 58.86/58.95 => ( aInteger0(W2) % 58.86/58.95 & ? [W3] : % 58.86/58.95 ( aInteger0(W3) % 58.86/58.95 & sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00)) ) % 58.86/58.95 & aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00))) % 58.86/58.95 & sdteqdtlpzmzozddtrp0(W2,sz00,W1) ) ) % 58.86/58.95 & ( ( aInteger0(W2) % 58.86/58.95 & ( ? [W3] : % 58.86/58.95 ( aInteger0(W3) % 58.86/58.95 & sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00)) ) % 58.86/58.95 | aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00))) % 58.86/58.95 | sdteqdtlpzmzozddtrp0(W2,sz00,W1) ) ) % 58.86/58.95 => aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1)) ) ) % 58.86/58.95 & szAzrzSzezqlpdtcmdtrp0(sz00,W1) = W0 ) ) % 58.86/58.95 & ( ? [W1] : % 58.86/58.95 ( aInteger0(W1) % 58.86/58.95 & W1 != sz00 % 58.86/58.95 & isPrime0(W1) % 58.86/58.95 & ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,W1)) % 58.86/58.95 & ! [W2] : % 58.86/58.95 ( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1)) % 58.86/58.95 => ( aInteger0(W2) % 58.86/58.95 & ? [W3] : % 58.86/58.95 ( aInteger0(W3) % 58.86/58.95 & sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00)) ) % 58.86/58.95 & aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00))) % 58.86/58.95 & sdteqdtlpzmzozddtrp0(W2,sz00,W1) ) ) % 58.86/58.95 & ( ( aInteger0(W2) % 58.86/58.95 & ( ? [W3] : % 58.86/58.95 ( aInteger0(W3) % 58.86/58.95 & sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00)) ) % 58.86/58.95 | aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00))) % 58.86/58.95 | sdteqdtlpzmzozddtrp0(W2,sz00,W1) ) ) % 58.86/58.95 => aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1)) ) ) ) % 58.86/58.95 => szAzrzSzezqlpdtcmdtrp0(sz00,W1) = W0 ) ) % 58.86/58.95 => aElementOf0(W0,xS) ) ) % 58.86/58.95 & xS = cS2043 ) ). % 58.86/58.95 % 58.86/58.95 fof(m__2079,hypothesis, % 58.86/58.95 ( aSet0(sbsmnsldt0(xS)) % 58.86/58.95 & ! [W0] : % 58.86/58.95 ( aElementOf0(W0,sbsmnsldt0(xS)) % 58.86/58.95 <=> ( aInteger0(W0) % 58.86/58.95 & ? [W1] : % 58.86/58.95 ( aElementOf0(W1,xS) % 58.86/58.95 & aElementOf0(W0,W1) ) ) ) % 58.86/58.95 & aSet0(stldt0(sbsmnsldt0(xS))) % 58.86/58.95 & ! [W0] : % 58.86/58.95 ( aElementOf0(W0,stldt0(sbsmnsldt0(xS))) % 58.86/58.95 <=> ( aInteger0(W0) % 58.86/58.95 & ~ aElementOf0(W0,sbsmnsldt0(xS)) ) ) % 58.86/58.95 & ! [W0] : % 58.86/58.95 ( aElementOf0(W0,stldt0(sbsmnsldt0(xS))) % 58.86/58.95 <=> ( W0 = sz10 % 58.86/58.95 | W0 = smndt0(sz10) ) ) % 58.86/58.95 & stldt0(sbsmnsldt0(xS)) = cS2076 ) ). % 58.86/58.95 % 58.86/58.95 fof(m__2117,hypothesis, % 58.86/58.95 isFinite0(xS) ). % 58.86/58.95 % 58.86/58.95 fof(m__2144,hypothesis, % 58.86/58.95 ( aSet0(sbsmnsldt0(xS)) % 58.86/58.95 & ! [W0] : % 58.86/58.95 ( aElementOf0(W0,sbsmnsldt0(xS)) % 58.86/58.95 <=> ( aInteger0(W0) % 58.86/58.95 & ? [W1] : % 58.86/58.95 ( aElementOf0(W1,xS) % 58.86/58.95 & aElementOf0(W0,W1) ) ) ) % 58.86/58.95 & ! [W0] : % 58.86/58.95 ( aElementOf0(W0,stldt0(sbsmnsldt0(xS))) % 58.86/58.95 <=> ( aInteger0(W0) % 58.86/58.95 & ~ aElementOf0(W0,sbsmnsldt0(xS)) ) ) % 58.86/58.95 & ! [W0] : % 58.86/58.95 ( aElementOf0(W0,stldt0(sbsmnsldt0(xS))) % 58.86/58.95 => ? [W1] : % 58.86/58.95 ( aInteger0(W1) % 58.86/58.95 & W1 != sz00 % 58.86/58.95 & aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)) % 58.86/58.95 & ! [W2] : % 58.86/58.95 ( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) % 58.86/58.95 => ( aInteger0(W2) % 58.86/58.95 & ? [W3] : % 58.86/58.95 ( aInteger0(W3) % 58.86/58.95 & sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0)) ) % 58.86/58.95 & aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))) % 58.86/58.95 & sdteqdtlpzmzozddtrp0(W2,W0,W1) ) ) % 58.86/58.95 & ( ( aInteger0(W2) % 58.86/58.95 & ( ? [W3] : % 58.86/58.95 ( aInteger0(W3) % 58.86/58.95 & sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0)) ) % 58.86/58.95 | aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))) % 58.86/58.95 | sdteqdtlpzmzozddtrp0(W2,W0,W1) ) ) % 58.86/58.95 => aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) ) ) % 58.86/58.95 & ! [W2] : % 58.86/58.95 ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) % 58.86/58.95 => aElementOf0(W2,stldt0(sbsmnsldt0(xS))) ) % 58.86/58.95 & aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS))) ) ) % 58.86/58.95 & isOpen0(stldt0(sbsmnsldt0(xS))) % 58.86/58.95 & isClosed0(sbsmnsldt0(xS)) % 58.86/58.96 & aSet0(sbsmnsldt0(xS)) % 58.86/58.96 & ! [W0] : % 58.86/58.96 ( aElementOf0(W0,sbsmnsldt0(xS)) % 58.86/58.96 <=> ( aInteger0(W0) % 58.86/58.96 & ? [W1] : % 58.86/58.96 ( aElementOf0(W1,xS) % 58.86/58.96 & aElementOf0(W0,W1) ) ) ) % 58.86/58.96 & ! [W0] : % 58.86/58.96 ( aElementOf0(W0,stldt0(sbsmnsldt0(xS))) % 58.86/58.96 <=> ( aInteger0(W0) % 58.86/58.96 & ~ aElementOf0(W0,sbsmnsldt0(xS)) ) ) % 58.86/58.96 & ! [W0] : % 58.86/58.96 ( aElementOf0(W0,stldt0(sbsmnsldt0(xS))) % 58.86/58.96 => ? [W1] : % 58.86/58.96 ( aInteger0(W1) % 58.86/58.96 & W1 != sz00 % 58.86/58.96 & aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)) % 58.86/58.96 & ! [W2] : % 58.86/58.96 ( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) % 58.86/58.96 => ( aInteger0(W2) % 58.86/58.96 & ? [W3] : % 58.86/58.96 ( aInteger0(W3) % 58.86/58.96 & sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0)) ) % 58.86/58.96 & aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))) % 58.86/58.96 & sdteqdtlpzmzozddtrp0(W2,W0,W1) ) ) % 58.86/58.96 & ( ( aInteger0(W2) % 58.86/58.96 & ( ? [W3] : % 58.86/58.96 ( aInteger0(W3) % 58.86/58.96 & sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0)) ) % 58.86/58.96 | aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))) % 58.86/58.96 | sdteqdtlpzmzozddtrp0(W2,W0,W1) ) ) % 58.86/58.96 => aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) ) ) % 58.86/58.96 & ! [W2] : % 58.86/58.96 ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) % 58.86/58.96 => aElementOf0(W2,stldt0(sbsmnsldt0(xS))) ) % 58.86/58.96 & aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS))) ) ) ) ). % 58.86/58.96 % 58.86/58.96 fof(m__,conjecture, % 58.86/58.96 ? [W0] : % 58.86/58.96 ( aInteger0(W0) % 58.86/58.96 & W0 != sz00 % 58.86/58.96 & ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,W0)) % 58.86/58.96 & ! [W1] : % 58.86/58.96 ( ( aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0)) % 58.86/58.96 => ( aInteger0(W1) % 58.86/58.96 & ? [W2] : % 58.86/58.96 ( aInteger0(W2) % 58.86/58.96 & sdtasdt0(W0,W2) = sdtpldt0(W1,smndt0(sz10)) ) % 58.86/58.96 & aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10))) % 58.86/58.96 & sdteqdtlpzmzozddtrp0(W1,sz10,W0) ) ) % 58.86/58.96 & ( ( aInteger0(W1) % 58.86/58.96 & ( ? [W2] : % 58.86/58.96 ( aInteger0(W2) % 58.86/58.96 & sdtasdt0(W0,W2) = sdtpldt0(W1,smndt0(sz10)) ) % 58.86/58.96 | aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10))) % 58.86/58.96 | sdteqdtlpzmzozddtrp0(W1,sz10,W0) ) ) % 58.86/58.96 => aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0)) ) ) ) % 58.86/58.96 => ( ( aSet0(sbsmnsldt0(xS)) % 58.86/58.96 & ! [W1] : % 58.86/58.96 ( aElementOf0(W1,sbsmnsldt0(xS)) % 58.86/58.96 <=> ( aInteger0(W1) % 58.86/58.96 & ? [W2] : % 58.86/58.96 ( aElementOf0(W2,xS) % 58.86/58.96 & aElementOf0(W1,W2) ) ) ) ) % 58.86/58.96 => ( ! [W1] : % 58.86/58.96 ( aElementOf0(W1,stldt0(sbsmnsldt0(xS))) % 58.86/58.96 <=> ( aInteger0(W1) % 58.86/58.96 & ~ aElementOf0(W1,sbsmnsldt0(xS)) ) ) % 58.86/58.96 => ( ! [W1] : % 58.86/58.96 ( aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0)) % 58.86/58.96 => aElementOf0(W1,stldt0(sbsmnsldt0(xS))) ) % 58.86/58.96 | aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,W0),stldt0(sbsmnsldt0(xS))) ) ) ) ) ) ). % 58.86/58.96 % 58.86/58.96 %------------------------------------------------------------------------------ % 58.86/58.96 %------------------------------------------- % 58.86/58.96 % Proof found % 58.86/58.96 % SZS status Theorem for theBenchmark % 58.86/58.96 % SZS output start Proof % 58.86/58.96 %ClaNum:290(EqnAxiom:80) % 58.86/58.96 %VarNum:1275(SingletonVarNum:393) % 58.86/58.96 %MaxLitNum:8 % 58.86/58.96 %MaxfuncDepth:2 % 58.86/58.96 %SharedTerms:20 % 58.86/58.96 %goalClause: 119 154 163 183 187 189 196 201 213 216 221 223 224 235 % 58.86/58.96 [81]E(a1,a2) % 58.86/58.96 [82]P1(a4) % 58.86/58.96 [83]P1(a41) % 58.86/58.96 [84]P4(a1) % 58.86/58.96 [85]P5(a1) % 58.86/58.96 [89]P4(f5(a1)) % 58.86/58.96 [90]P6(f5(a1)) % 58.86/58.96 [86]E(f35(f5(a1)),a6) % 58.86/58.96 [91]P4(f35(f5(a1))) % 58.86/58.96 [92]P8(f35(f5(a1))) % 58.86/58.96 [94]~P1(x941)+P1(f36(x941)) % 58.86/58.96 [95]~P1(x951)+E(f37(a4,x951),a4) % 58.86/58.96 [96]~P1(x961)+E(f37(x961,a4),a4) % 58.86/58.96 [97]~P1(x971)+E(f38(a4,x971),x971) % 58.86/58.96 [98]~P1(x981)+E(f37(a41,x981),x981) % 58.86/58.96 [99]~P1(x991)+E(f38(x991,a4),x991) % 58.86/58.96 [100]~P1(x1001)+E(f37(x1001,a41),x1001) % 58.86/58.96 [102]~P2(x1021,a1)+~E(f8(x1021),a4) % 58.86/58.96 [108]~P2(x1081,a1)+P1(f8(x1081)) % 58.86/58.96 [109]~P2(x1091,a1)+P9(f8(x1091)) % 58.86/58.96 [112]P1(x1121)+~P2(x1121,f5(a1)) % 58.86/58.96 [140]~P2(x1401,f5(a1))+P2(f15(x1401),a1) % 58.86/58.96 [141]~P2(x1411,f5(a1))+P2(f18(x1411),a1) % 58.86/58.96 [142]~P2(x1421,f5(a1))+P2(f20(x1421),a1) % 58.86/58.96 [144]P2(x1441,f15(x1441))+~P2(x1441,f5(a1)) % 58.86/58.96 [145]P2(x1451,f18(x1451))+~P2(x1451,f5(a1)) % 58.86/58.96 [146]P2(x1461,f20(x1461))+~P2(x1461,f5(a1)) % 58.86/58.96 [103]~P1(x1031)+E(f38(f36(x1031),x1031),a4) % 58.86/58.96 [104]~P1(x1041)+E(f38(x1041,f36(x1041)),a4) % 58.86/58.96 [105]~P1(x1051)+E(f37(x1051,f36(a41)),f36(x1051)) % 58.86/58.96 [106]~P1(x1061)+E(f37(f36(a41),x1061),f36(x1061)) % 58.86/58.96 [107]~E(x1071,a41)+P2(x1071,f35(f5(a1))) % 58.86/58.96 [114]~E(x1141,f36(a41))+P2(x1141,f35(f5(a1))) % 58.86/58.96 [123]~P2(x1231,a1)+E(f42(a4,f8(x1231)),x1231) % 58.86/58.96 [139]P1(x1391)+~P2(x1391,f35(f5(a1))) % 58.86/58.96 [147]~E(f21(x1471),a4)+~P2(x1471,f35(f5(a1))) % 58.86/58.96 [148]~E(f23(x1481),a4)+~P2(x1481,f35(f5(a1))) % 58.86/58.96 [155]P1(f21(x1551))+~P2(x1551,f35(f5(a1))) % 58.86/58.96 [156]P1(f23(x1561))+~P2(x1561,f35(f5(a1))) % 58.86/58.96 [161]~P2(x1611,a1)+P4(f42(a4,f8(x1611))) % 58.86/58.96 [179]~P2(x1791,f5(a1))+~P2(x1791,f35(f5(a1))) % 58.86/58.96 [192]~P2(x1921,f35(f5(a1)))+P4(f42(x1921,f21(x1921))) % 58.86/58.96 [193]~P2(x1931,f35(f5(a1)))+P4(f42(x1931,f23(x1931))) % 58.86/58.96 [209]~P2(x2091,f35(f5(a1)))+P7(f42(x2091,f21(x2091)),f35(f5(a1))) % 58.86/58.96 [210]~P2(x2101,f35(f5(a1)))+P7(f42(x2101,f23(x2101)),f35(f5(a1))) % 58.86/58.96 [119]~P1(x1191)+E(x1191,a4)+P4(f42(a41,x1191)) % 58.86/58.96 [120]~P6(x1201)+~P7(x1201,a3)+P8(f35(x1201)) % 58.86/58.96 [121]~P4(x1211)+P2(f9(x1211),x1211)+P8(f5(x1211)) % 58.86/58.96 [127]P6(x1271)+~P7(x1271,a3)+~P8(f35(x1271)) % 58.86/58.96 [134]P8(x1341)+P2(f10(x1341),x1341)+~P7(x1341,a3) % 58.86/58.96 [154]~P1(x1541)+E(x1541,a4)+P2(f24(x1541),f42(a41,x1541)) % 58.86/58.96 [143]E(x1431,a41)+E(x1431,f36(a41))+~P2(x1431,f35(f5(a1))) % 58.86/58.96 [153]~P1(x1531)+P2(x1531,f5(a1))+P2(x1531,f35(f5(a1))) % 58.86/58.96 [163]~P1(x1631)+E(x1631,a4)+~P2(f24(x1631),f35(f5(a1))) % 58.86/58.96 [196]~P1(x1961)+E(x1961,a4)+~P7(f42(a41,x1961),f35(f5(a1))) % 58.86/58.96 [113]~P3(x1131,x1132)+~P1(x1132)+~E(x1131,a4) % 58.86/58.96 [117]~P3(x1171,x1172)+P1(x1171)+~P1(x1172) % 58.86/58.96 [118]~P7(x1181,x1182)+P4(x1181)+~P4(x1182) % 58.86/58.96 [116]P4(x1161)+~P7(x1162,a3)+~E(x1161,f35(x1162)) % 58.86/58.96 [128]~P1(x1282)+~P1(x1281)+E(f38(x1281,x1282),f38(x1282,x1281)) % 58.86/58.96 [129]~P1(x1292)+~P1(x1291)+E(f37(x1291,x1292),f37(x1292,x1291)) % 58.86/58.96 [132]~P1(x1322)+~P1(x1321)+P1(f38(x1321,x1322)) % 58.86/58.96 [133]~P1(x1332)+~P1(x1331)+P1(f37(x1331,x1332)) % 58.86/58.96 [164]~P1(x1641)+~P3(x1642,x1641)+P1(f19(x1641,x1642)) % 58.86/58.96 [181]~P1(x1812)+~P3(x1811,x1812)+E(f37(x1811,f19(x1812,x1811)),x1812) % 58.86/58.96 [206]P1(x2061)+~P2(x2062,a1)+~P2(x2061,f42(a4,f8(x2062))) % 58.86/58.96 [227]~P2(x2271,a1)+P1(f16(x2271,x2272))+~P2(x2272,f42(a4,f8(x2271))) % 58.86/58.96 [228]P1(x2281)+~P2(x2281,f42(x2282,f21(x2282)))+~P2(x2282,f35(f5(a1))) % 58.86/58.96 [229]P1(x2291)+~P2(x2291,f42(x2292,f23(x2292)))+~P2(x2292,f35(f5(a1))) % 58.86/58.96 [242]~P2(x2421,a1)+P3(f8(x2421),f38(x2422,f36(a4)))+~P2(x2422,f42(a4,f8(x2421))) % 58.86/58.96 [243]~P2(x2431,f42(x2432,f21(x2432)))+P2(x2431,f35(f5(a1)))+~P2(x2432,f35(f5(a1))) % 58.86/58.96 [244]~P2(x2441,f42(x2442,f23(x2442)))+P2(x2441,f35(f5(a1)))+~P2(x2442,f35(f5(a1))) % 58.86/58.96 [245]~P2(x2452,f42(x2451,f21(x2451)))+P1(f22(x2451,x2452))+~P2(x2451,f35(f5(a1))) % 58.86/58.96 [246]~P2(x2462,f42(x2461,f23(x2461)))+P1(f27(x2461,x2462))+~P2(x2461,f35(f5(a1))) % 58.86/58.96 [249]~P2(x2492,a1)+P10(x2491,a4,f8(x2492))+~P2(x2491,f42(a4,f8(x2492))) % 58.86/58.96 [252]~P2(x2521,a1)+E(f37(f8(x2521),f16(x2521,x2522)),f38(x2522,f36(a4)))+~P2(x2522,f42(a4,f8(x2521))) % 58.86/58.96 [260]~P2(x2602,f42(x2601,f21(x2601)))+P3(f21(x2601),f38(x2602,f36(x2601)))+~P2(x2601,f35(f5(a1))) % 58.86/58.96 [261]~P2(x2612,f42(x2611,f23(x2611)))+P3(f23(x2611),f38(x2612,f36(x2611)))+~P2(x2611,f35(f5(a1))) % 58.86/58.96 [263]P10(x2631,x2632,f21(x2632))+~P2(x2631,f42(x2632,f21(x2632)))+~P2(x2632,f35(f5(a1))) % 58.86/58.96 [264]P10(x2641,x2642,f23(x2642))+~P2(x2641,f42(x2642,f23(x2642)))+~P2(x2642,f35(f5(a1))) % 58.86/58.96 [267]~P2(x2672,f42(x2671,f21(x2671)))+E(f37(f21(x2671),f22(x2671,x2672)),f38(x2672,f36(x2671)))+~P2(x2671,f35(f5(a1))) % 58.86/58.96 [268]~P2(x2682,f42(x2681,f23(x2681)))+E(f37(f23(x2681),f27(x2681,x2682)),f38(x2682,f36(x2681)))+~P2(x2681,f35(f5(a1))) % 58.86/58.96 [101]~P1(x1011)+E(x1011,a41)+E(x1011,f36(a41))+P9(f7(x1011)) % 58.86/58.96 [115]~P1(x1151)+P3(f7(x1151),x1151)+E(x1151,a41)+E(x1151,f36(a41)) % 58.86/58.96 [135]~P4(x1351)+~P5(x1351)+P2(f14(x1351),x1351)+P6(f5(x1351)) % 58.86/58.96 [167]~P4(x1671)+~P8(f9(x1671))+~P7(f9(x1671),a3)+P8(f5(x1671)) % 58.86/58.96 [122]~P1(x1221)+~P3(x1222,x1221)+~P9(x1222)+~E(x1221,a41) % 58.86/58.96 [180]~P1(x1801)+~P1(x1802)+P10(x1802,x1802,x1801)+E(x1801,a4) % 58.86/58.96 [125]~P4(x1252)+P4(x1251)+~E(x1251,f5(x1252))+P2(f28(x1252),x1252) % 58.86/58.96 [130]~P1(x1301)+~P3(x1302,x1301)+~P9(x1302)+~E(x1301,f36(a41)) % 58.86/58.96 [136]~P1(x1361)+~P1(x1362)+E(x1361,a4)+P6(f42(x1362,x1361)) % 58.86/58.96 [149]~P4(x1492)+P4(x1491)+~E(x1491,f5(x1492))+~P7(f28(x1492),a3) % 58.86/58.96 [157]~P1(x1571)+~P1(x1572)+E(x1571,a4)+P7(f42(x1572,x1571),a3) % 58.86/58.96 [173]~P1(x1731)+~P2(x1731,x1732)+~P2(x1732,a1)+P2(x1731,f5(a1)) % 58.86/58.96 [174]~P4(x1741)+~P4(x1742)+P7(x1741,x1742)+P2(f29(x1742,x1741),x1741) % 58.86/58.96 [183]~P1(x1831)+P1(x1832)+E(x1831,a4)+~P2(x1832,f42(a41,x1831)) % 58.86/58.96 [185]~P8(x1851)+~P2(x1852,x1851)+~P7(x1851,a3)+~E(f11(x1851,x1852),a4) % 58.86/58.96 [187]~P1(x1871)+E(x1871,a4)+~P2(x1872,f5(a1))+P2(f25(x1871,x1872),a1) % 58.86/58.96 [189]~P1(x1891)+P2(x1892,f25(x1891,x1892))+E(x1891,a4)+~P2(x1892,f5(a1)) % 58.86/58.96 [191]~P8(x1911)+~P2(x1912,x1911)+~P7(x1911,a3)+P1(f11(x1911,x1912)) % 58.86/58.96 [200]~P4(x2001)+~P4(x2002)+P7(x2001,x2002)+~P2(f29(x2002,x2001),x2002) % 58.86/58.96 [201]~P1(x2011)+E(x2011,a4)+~P2(x2012,f42(a41,x2011))+P1(f26(x2011,x2012)) % 58.86/58.96 [221]~P1(x2211)+P10(x2212,a41,x2211)+E(x2211,a4)+~P2(x2212,f42(a41,x2211)) % 58.86/58.96 [216]~P1(x2161)+E(x2161,a4)+~P2(x2162,f42(a41,x2161))+P3(x2161,f38(x2162,f36(a41))) % 58.86/58.96 [223]~P1(x2231)+E(x2231,a4)+~P2(x2232,f42(a41,x2231))+E(f37(x2231,f26(x2231,x2232)),f38(x2232,f36(a41))) % 58.86/58.96 [237]~P8(x2372)+~P2(x2371,x2372)+~P7(x2372,a3)+P7(f42(x2371,f11(x2372,x2371)),x2372) % 58.86/58.96 [250]~P1(x2501)+~P2(x2502,a1)+~P3(f8(x2502),f38(x2501,f36(a4)))+P2(x2501,f42(a4,f8(x2502))) % 58.86/58.96 [255]~P1(x2551)+~P2(x2552,a1)+~P10(x2551,a4,f8(x2552))+P2(x2551,f42(a4,f8(x2552))) % 58.86/58.96 [269]~P1(x2691)+~P3(f21(x2692),f38(x2691,f36(x2692)))+P2(x2691,f42(x2692,f21(x2692)))+~P2(x2692,f35(f5(a1))) % 58.86/58.96 [270]~P1(x2701)+~P3(f23(x2702),f38(x2701,f36(x2702)))+P2(x2701,f42(x2702,f23(x2702)))+~P2(x2702,f35(f5(a1))) % 58.86/58.96 [271]~P1(x2711)+~P10(x2711,x2712,f21(x2712))+P2(x2711,f42(x2712,f21(x2712)))+~P2(x2712,f35(f5(a1))) % 58.86/58.96 [272]~P1(x2721)+~P10(x2721,x2722,f23(x2722))+P2(x2721,f42(x2722,f23(x2722)))+~P2(x2722,f35(f5(a1))) % 58.86/58.96 [169]~P4(x1692)+~P7(x1693,x1692)+P2(x1691,x1692)+~P2(x1691,x1693) % 58.86/58.96 [159]~P2(x1591,x1592)+P1(x1591)+~P7(x1593,a3)+~E(x1592,f35(x1593)) % 58.86/58.96 [175]P4(x1751)+~P7(x1753,a3)+~P7(x1752,a3)+~E(x1751,f39(x1752,x1753)) % 58.86/58.96 [176]P4(x1761)+~P7(x1763,a3)+~P7(x1762,a3)+~E(x1761,f40(x1762,x1763)) % 58.86/58.96 [186]~P2(x1863,x1862)+~P2(x1863,x1861)+~P7(x1862,a3)+~E(x1861,f35(x1862)) % 58.86/58.96 [202]~P1(x2023)+~P1(x2022)+~P1(x2021)+E(f38(f38(x2021,x2022),x2023),f38(x2021,f38(x2022,x2023))) % 58.86/58.96 [203]~P1(x2033)+~P1(x2032)+~P1(x2031)+E(f37(f37(x2031,x2032),x2033),f37(x2031,f37(x2032,x2033))) % 58.86/58.96 [225]~P1(x2253)+~P1(x2252)+~P1(x2251)+E(f38(f37(x2251,x2252),f37(x2251,x2253)),f37(x2251,f38(x2252,x2253))) % 58.86/58.96 [226]~P1(x2262)+~P1(x2263)+~P1(x2261)+E(f38(f37(x2261,x2262),f37(x2263,x2262)),f37(f38(x2261,x2263),x2262)) % 58.86/58.96 [182]~P4(x1821)+~P5(x1821)+~P6(f14(x1821))+~P7(f14(x1821),a3)+P6(f5(x1821)) % 58.86/58.96 [124]~P1(x1241)+~P1(x1242)+E(x1241,a4)+E(x1242,a4)+~E(f37(x1242,x1241),a4) % 58.86/58.96 [150]~P1(x1501)+~P9(x1501)+E(x1501,a4)+P2(x1502,a1)+~E(f42(a4,x1501),x1502) % 58.86/58.96 [160]~P1(x1601)+~P9(x1601)+E(x1601,a4)+P2(x1602,a1)+P4(f42(a4,x1601)) % 58.86/58.96 [194]~P8(x1942)+~P8(x1941)+~P7(x1942,a3)+~P7(x1941,a3)+P8(f40(x1941,x1942)) % 58.86/58.96 [195]~P6(x1952)+~P6(x1951)+~P7(x1952,a3)+~P7(x1951,a3)+P6(f39(x1951,x1952)) % 58.86/58.96 [208]~P4(x2081)+P2(f12(x2082,x2081),x2081)+~P7(x2082,a3)+E(x2081,f35(x2082))+P1(f12(x2082,x2081)) % 58.86/58.96 [234]~P4(x2341)+P2(f12(x2342,x2341),x2341)+~P7(x2342,a3)+~P2(f12(x2342,x2341),x2342)+E(x2341,f35(x2342)) % 58.86/58.96 [235]~P1(x2351)+~P1(x2352)+~P10(x2352,a41,x2351)+E(x2351,a4)+P2(x2352,f42(a41,x2351)) % 58.86/58.96 [217]~P1(x2171)+P8(x2172)+~P7(x2172,a3)+E(x2171,a4)+~P7(f42(f10(x2172),x2171),x2172) % 58.86/58.96 [224]~P1(x2242)+~P1(x2241)+E(x2241,a4)+P2(x2242,f42(a41,x2241))+~P3(x2241,f38(x2242,f36(a41))) % 58.86/58.96 [131]~P1(x1311)+~P1(x1313)+P4(x1312)+E(x1311,a4)+~E(x1312,f42(x1313,x1311)) % 58.86/58.96 [166]~P4(x1662)+~P2(x1661,x1663)+P1(x1661)+P2(f28(x1662),x1662)+~E(x1663,f5(x1662)) % 58.86/58.96 [168]~P1(x1681)+P2(x1681,x1682)+P2(x1681,x1683)+~E(x1682,f35(x1683))+~P7(x1683,a3) % 58.86/58.96 [184]~P4(x1843)+~P2(x1841,x1842)+P1(x1841)+~E(x1842,f5(x1843))+~P7(f28(x1843),a3) % 58.86/58.96 [258]~P4(x2581)+~P2(x2582,x2583)+~E(x2583,f5(x2581))+P2(f28(x2581),x2581)+P2(x2582,f33(x2581,x2583,x2582)) % 58.86/58.96 [259]~P4(x2591)+~P2(x2593,x2592)+~E(x2592,f5(x2591))+P2(f28(x2591),x2591)+P2(f33(x2591,x2592,x2593),x2591) % 58.86/58.96 [265]~P4(x2652)+~P2(x2651,x2653)+~E(x2653,f5(x2652))+P2(x2651,f33(x2652,x2653,x2651))+~P7(f28(x2652),a3) % 58.86/58.96 [266]~P4(x2661)+~P2(x2663,x2662)+~E(x2662,f5(x2661))+P2(f33(x2661,x2662,x2663),x2661)+~P7(f28(x2661),a3) % 58.86/58.96 [238]~P1(x2381)+~P1(x2383)+~P2(x2382,a1)+~E(f37(f8(x2382),x2383),f38(x2381,f36(a4)))+P2(x2381,f42(a4,f8(x2382))) % 58.86/58.96 [256]~P1(x2561)+~P1(x2563)+P2(x2561,f42(x2562,f21(x2562)))+~E(f37(f21(x2562),x2563),f38(x2561,f36(x2562)))+~P2(x2562,f35(f5(a1))) % 58.86/58.96 [257]~P1(x2571)+~P1(x2573)+P2(x2571,f42(x2572,f23(x2572)))+~E(f37(f23(x2572),x2573),f38(x2571,f36(x2572)))+~P2(x2572,f35(f5(a1))) % 58.86/58.96 [197]~P2(x1971,x1972)+P1(x1971)+~P7(x1974,a3)+~P7(x1973,a3)+~E(x1972,f39(x1973,x1974)) % 58.86/58.96 [198]~P2(x1981,x1982)+P1(x1981)+~P7(x1984,a3)+~P7(x1983,a3)+~E(x1982,f40(x1983,x1984)) % 58.86/58.96 [204]~P2(x2041,x2043)+P2(x2041,x2042)+~P7(x2044,a3)+~P7(x2042,a3)+~E(x2043,f40(x2044,x2042)) % 58.86/58.96 [205]~P2(x2051,x2053)+P2(x2051,x2052)+~P7(x2054,a3)+~P7(x2052,a3)+~E(x2053,f40(x2052,x2054)) % 58.86/58.96 [214]~P4(x2141)+~P4(x2142)+P2(f28(x2142),x2142)+P2(f32(x2142,x2141),x2141)+E(x2141,f5(x2142))+P1(f32(x2142,x2141)) % 58.86/58.96 [220]~P4(x2201)+~P4(x2202)+P2(f32(x2202,x2201),x2201)+E(x2201,f5(x2202))+P1(f32(x2202,x2201))+~P7(f28(x2202),a3) % 58.86/58.96 [222]~P4(x2221)+~P4(x2222)+P2(f28(x2222),x2222)+P2(f32(x2222,x2221),x2221)+P2(f34(x2222,x2221),x2222)+E(x2221,f5(x2222)) % 58.86/58.96 [231]~P4(x2311)+~P4(x2312)+P2(f32(x2312,x2311),x2311)+P2(f34(x2312,x2311),x2312)+E(x2311,f5(x2312))+~P7(f28(x2312),a3) % 58.86/58.96 [240]~P4(x2401)+~P4(x2402)+P2(f28(x2402),x2402)+P2(f32(x2402,x2401),x2401)+P2(f32(x2402,x2401),f34(x2402,x2401))+E(x2401,f5(x2402)) % 58.86/58.96 [247]~P4(x2471)+~P4(x2472)+P2(f32(x2472,x2471),x2471)+P2(f32(x2472,x2471),f34(x2472,x2471))+E(x2471,f5(x2472))+~P7(f28(x2472),a3) % 58.86/58.96 [262]~P4(x2621)+P2(f12(x2622,x2621),x2622)+~P7(x2622,a3)+~P2(f12(x2622,x2621),x2621)+E(x2621,f35(x2622))+~P1(f12(x2622,x2621)) % 58.86/58.96 [254]~P1(x2541)+~P1(x2542)+~P1(x2543)+~P10(x2543,x2542,x2541)+P10(x2542,x2543,x2541)+E(x2541,a4) % 58.86/58.96 [165]~P1(x1652)+~P1(x1653)+~P1(x1651)+P3(x1651,x1652)+E(x1651,a4)+~E(f37(x1651,x1653),x1652) % 58.86/58.96 [199]~P1(x1991)+~P9(x1991)+P1(x1992)+E(x1991,a4)+P2(x1993,a1)+~P2(x1992,f42(a4,x1991)) % 58.86/58.96 [236]~P1(x2361)+~P9(x2361)+P10(x2363,a4,x2361)+E(x2361,a4)+P2(x2362,a1)+~P2(x2363,f42(a4,x2361)) % 58.86/58.96 [273]~P1(x2731)+~P9(x2731)+E(x2731,a4)+P2(x2732,a1)+~P2(x2733,f42(a4,x2731))+P1(f17(x2732,x2731,x2733)) % 58.86/58.96 [281]~P4(x2811)+P2(f30(x2812,x2813,x2811),x2811)+~P7(x2813,a3)+~P7(x2812,a3)+E(x2811,f39(x2812,x2813))+P1(f30(x2812,x2813,x2811)) % 58.86/58.96 [282]~P4(x2821)+P2(f31(x2822,x2823,x2821),x2821)+~P7(x2823,a3)+~P7(x2822,a3)+E(x2821,f40(x2822,x2823))+P1(f31(x2822,x2823,x2821)) % 58.86/58.96 [283]~P4(x2831)+P2(f31(x2832,x2833,x2831),x2831)+P2(f31(x2832,x2833,x2831),x2833)+~P7(x2833,a3)+~P7(x2832,a3)+E(x2831,f40(x2832,x2833)) % 58.86/58.96 [284]~P4(x2841)+P2(f31(x2842,x2843,x2841),x2841)+P2(f31(x2842,x2843,x2841),x2842)+~P7(x2843,a3)+~P7(x2842,a3)+E(x2841,f40(x2842,x2843)) % 58.86/58.96 [213]~P1(x2132)+~P1(x2131)+~P1(x2133)+E(x2131,a4)+P2(x2132,f42(a41,x2131))+~E(f37(x2131,x2133),f38(x2132,f36(a41))) % 58.86/58.96 [233]~P1(x2331)+~P9(x2331)+E(x2331,a4)+P2(x2332,a1)+~P2(x2333,f42(a4,x2331))+P3(x2331,f38(x2333,f36(a4))) % 58.86/58.96 [251]~P1(x2513)+~P1(x2512)+~P1(x2511)+P10(x2512,x2513,x2511)+E(x2511,a4)+~P3(x2511,f38(x2512,f36(x2513))) % 58.86/58.96 [253]~P1(x2531)+~P1(x2533)+~P1(x2532)+~P10(x2532,x2533,x2531)+E(x2531,a4)+P3(x2531,f38(x2532,f36(x2533))) % 58.86/58.96 [276]~P1(x2761)+~P9(x2761)+P2(x2762,a1)+E(x2761,a4)+~P2(x2763,f42(a4,x2761))+E(f37(x2761,f17(x2762,x2761,x2763)),f38(x2763,f36(a4))) % 58.86/58.96 [170]~P1(x1701)+~P1(x1704)+~P2(x1702,x1703)+P1(x1702)+E(x1701,a4)+~E(x1703,f42(x1704,x1701)) % 58.86/58.96 [211]~P1(x2111)+~P2(x2111,x2114)+P2(x2111,x2112)+~P7(x2113,a3)+~P7(x2114,a3)+~E(x2112,f39(x2113,x2114)) % 58.86/58.96 [212]~P1(x2121)+~P2(x2121,x2123)+P2(x2121,x2122)+~P7(x2124,a3)+~P7(x2123,a3)+~E(x2122,f39(x2123,x2124)) % 58.86/58.96 [218]~P2(x2181,x2184)+P2(x2181,x2182)+P2(x2181,x2183)+~P7(x2182,a3)+~P7(x2183,a3)+~E(x2184,f39(x2183,x2182)) % 58.86/58.96 [219]~P1(x2191)+~P1(x2193)+~P2(x2192,x2194)+P10(x2192,x2193,x2191)+E(x2191,a4)+~E(x2194,f42(x2193,x2191)) % 58.86/58.96 [248]~P1(x2481)+~P1(x2483)+~P9(x2481)+~P10(x2483,a4,x2481)+E(x2481,a4)+P2(x2482,a1)+P2(x2483,f42(a4,x2481)) % 58.86/58.96 [280]~P1(x2801)+~P1(x2803)+~P4(x2802)+P2(f13(x2803,x2801,x2802),x2802)+E(x2801,a4)+E(x2802,f42(x2803,x2801))+P1(f13(x2803,x2801,x2802)) % 58.86/58.96 [285]~P1(x2851)+~P1(x2853)+~P4(x2852)+P10(f13(x2853,x2851,x2852),x2853,x2851)+P2(f13(x2853,x2851,x2852),x2852)+E(x2851,a4)+E(x2852,f42(x2853,x2851)) % 58.86/58.96 [286]~P4(x2861)+P2(f30(x2862,x2863,x2861),x2861)+P2(f30(x2862,x2863,x2861),x2863)+P2(f30(x2862,x2863,x2861),x2862)+~P7(x2863,a3)+~P7(x2862,a3)+E(x2861,f39(x2862,x2863)) % 58.86/58.96 [287]~P4(x2871)+~P7(x2873,a3)+~P7(x2872,a3)+~P2(f30(x2872,x2873,x2871),x2871)+~P2(f30(x2872,x2873,x2871),x2873)+E(x2871,f39(x2872,x2873))+~P1(f30(x2872,x2873,x2871)) % 58.86/58.96 [288]~P4(x2881)+~P7(x2883,a3)+~P7(x2882,a3)+~P2(f30(x2882,x2883,x2881),x2881)+~P2(f30(x2882,x2883,x2881),x2882)+E(x2881,f39(x2882,x2883))+~P1(f30(x2882,x2883,x2881)) % 58.86/58.96 [239]~P1(x2393)+~P1(x2391)+~P9(x2391)+E(x2391,a4)+P2(x2392,a1)+P2(x2393,f42(a4,x2391))+~P3(x2391,f38(x2393,f36(a4))) % 58.86/58.96 [207]~P1(x2071)+~P4(x2073)+~P2(x2071,x2074)+P2(x2071,x2072)+~P2(x2074,x2073)+~E(x2072,f5(x2073))+P2(f28(x2073),x2073) % 58.86/58.96 [215]~P1(x2151)+~P4(x2153)+~P2(x2151,x2154)+P2(x2151,x2152)+~P2(x2154,x2153)+~E(x2152,f5(x2153))+~P7(f28(x2153),a3) % 58.86/58.96 [232]~P1(x2321)+~P2(x2321,x2324)+~P2(x2321,x2323)+P2(x2321,x2322)+~P7(x2324,a3)+~P7(x2323,a3)+~E(x2322,f40(x2323,x2324)) % 58.86/58.96 [241]~P1(x2411)+~P1(x2414)+~P1(x2412)+~P10(x2412,x2414,x2411)+P2(x2412,x2413)+E(x2411,a4)+~E(x2413,f42(x2414,x2411)) % 58.86/58.96 [277]~P4(x2771)+~P4(x2772)+~P2(x2773,x2772)+P2(f28(x2772),x2772)+~P2(f32(x2772,x2771),x2773)+~P2(f32(x2772,x2771),x2771)+E(x2771,f5(x2772))+~P1(f32(x2772,x2771)) % 58.86/58.96 [278]~P4(x2781)+~P4(x2782)+~P2(x2783,x2782)+~P2(f32(x2782,x2781),x2783)+~P2(f32(x2782,x2781),x2781)+E(x2781,f5(x2782))+~P1(f32(x2782,x2781))+~P7(f28(x2782),a3) % 58.86/58.96 [289]~P1(x2891)+~P1(x2893)+~P4(x2892)+~P10(f13(x2893,x2891,x2892),x2893,x2891)+~P2(f13(x2893,x2891,x2892),x2892)+E(x2891,a4)+E(x2892,f42(x2893,x2891))+~P1(f13(x2893,x2891,x2892)) % 58.86/58.96 [290]~P4(x2901)+~P7(x2903,a3)+~P7(x2902,a3)+~P2(f31(x2902,x2903,x2901),x2901)+~P2(f31(x2902,x2903,x2901),x2903)+~P2(f31(x2902,x2903,x2901),x2902)+E(x2901,f40(x2902,x2903))+~P1(f31(x2902,x2903,x2901)) % 58.86/58.96 [279]~P1(x2793)+~P1(x2791)+~P1(x2792)+~P10(x2794,x2793,x2791)+~P10(x2792,x2794,x2791)+P10(x2792,x2793,x2791)+~P1(x2794)+E(x2791,a4) % 58.86/58.96 [274]~P1(x2741)+~P1(x2742)+~P1(x2744)+~P1(x2743)+P10(x2743,x2744,x2742)+~P10(x2743,x2744,f37(x2741,x2742))+E(x2741,a4)+E(x2742,a4) % 58.86/58.96 [275]~P1(x2751)+~P1(x2752)+~P1(x2754)+~P1(x2753)+P10(x2753,x2754,x2752)+~P10(x2753,x2754,f37(x2752,x2751))+E(x2751,a4)+E(x2752,a4) % 58.86/58.96 [230]~P1(x2303)+~P1(x2301)+~P1(x2304)+~P9(x2301)+E(x2301,a4)+P2(x2302,a1)+P2(x2303,f42(a4,x2301))+~E(f37(x2301,x2304),f38(x2303,f36(a4))) % 58.86/58.96 %EqnAxiom % 58.86/58.96 [1]E(x11,x11) % 58.86/58.96 [2]E(x22,x21)+~E(x21,x22) % 58.86/58.96 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.86/58.96 [4]~E(x41,x42)+E(f5(x41),f5(x42)) % 58.86/58.96 [5]~E(x51,x52)+E(f35(x51),f35(x52)) % 58.86/58.96 [6]~E(x61,x62)+E(f31(x61,x63,x64),f31(x62,x63,x64)) % 58.86/58.96 [7]~E(x71,x72)+E(f31(x73,x71,x74),f31(x73,x72,x74)) % 58.86/58.96 [8]~E(x81,x82)+E(f31(x83,x84,x81),f31(x83,x84,x82)) % 58.86/58.96 [9]~E(x91,x92)+E(f8(x91),f8(x92)) % 58.86/58.96 [10]~E(x101,x102)+E(f38(x101,x103),f38(x102,x103)) % 58.86/58.96 [11]~E(x111,x112)+E(f38(x113,x111),f38(x113,x112)) % 58.86/58.96 [12]~E(x121,x122)+E(f36(x121),f36(x122)) % 58.86/58.96 [13]~E(x131,x132)+E(f40(x131,x133),f40(x132,x133)) % 58.86/58.96 [14]~E(x141,x142)+E(f40(x143,x141),f40(x143,x142)) % 58.86/58.96 [15]~E(x151,x152)+E(f28(x151),f28(x152)) % 58.86/58.96 [16]~E(x161,x162)+E(f13(x161,x163,x164),f13(x162,x163,x164)) % 58.86/58.96 [17]~E(x171,x172)+E(f13(x173,x171,x174),f13(x173,x172,x174)) % 58.86/58.96 [18]~E(x181,x182)+E(f13(x183,x184,x181),f13(x183,x184,x182)) % 58.86/58.96 [19]~E(x191,x192)+E(f21(x191),f21(x192)) % 58.86/58.96 [20]~E(x201,x202)+E(f32(x201,x203),f32(x202,x203)) % 58.86/58.96 [21]~E(x211,x212)+E(f32(x213,x211),f32(x213,x212)) % 58.86/58.96 [22]~E(x221,x222)+E(f37(x221,x223),f37(x222,x223)) % 58.86/58.96 [23]~E(x231,x232)+E(f37(x233,x231),f37(x233,x232)) % 58.86/58.96 [24]~E(x241,x242)+E(f42(x241,x243),f42(x242,x243)) % 58.86/58.96 [25]~E(x251,x252)+E(f42(x253,x251),f42(x253,x252)) % 58.86/58.96 [26]~E(x261,x262)+E(f23(x261),f23(x262)) % 58.86/58.96 [27]~E(x271,x272)+E(f30(x271,x273,x274),f30(x272,x273,x274)) % 58.86/58.96 [28]~E(x281,x282)+E(f30(x283,x281,x284),f30(x283,x282,x284)) % 58.86/58.96 [29]~E(x291,x292)+E(f30(x293,x294,x291),f30(x293,x294,x292)) % 58.86/58.96 [30]~E(x301,x302)+E(f34(x301,x303),f34(x302,x303)) % 58.86/58.96 [31]~E(x311,x312)+E(f34(x313,x311),f34(x313,x312)) % 58.86/58.96 [32]~E(x321,x322)+E(f20(x321),f20(x322)) % 58.86/58.96 [33]~E(x331,x332)+E(f25(x331,x333),f25(x332,x333)) % 58.86/58.96 [34]~E(x341,x342)+E(f25(x343,x341),f25(x343,x342)) % 58.86/58.96 [35]~E(x351,x352)+E(f12(x351,x353),f12(x352,x353)) % 58.86/58.96 [36]~E(x361,x362)+E(f12(x363,x361),f12(x363,x362)) % 58.86/58.96 [37]~E(x371,x372)+E(f7(x371),f7(x372)) % 58.86/58.96 [38]~E(x381,x382)+E(f17(x381,x383,x384),f17(x382,x383,x384)) % 58.86/58.96 [39]~E(x391,x392)+E(f17(x393,x391,x394),f17(x393,x392,x394)) % 58.86/58.96 [40]~E(x401,x402)+E(f17(x403,x404,x401),f17(x403,x404,x402)) % 58.86/58.96 [41]~E(x411,x412)+E(f39(x411,x413),f39(x412,x413)) % 58.86/58.96 [42]~E(x421,x422)+E(f39(x423,x421),f39(x423,x422)) % 58.86/58.96 [43]~E(x431,x432)+E(f27(x431,x433),f27(x432,x433)) % 58.86/58.96 [44]~E(x441,x442)+E(f27(x443,x441),f27(x443,x442)) % 58.86/58.96 [45]~E(x451,x452)+E(f9(x451),f9(x452)) % 58.86/58.96 [46]~E(x461,x462)+E(f11(x461,x463),f11(x462,x463)) % 58.86/58.96 [47]~E(x471,x472)+E(f11(x473,x471),f11(x473,x472)) % 58.86/58.96 [48]~E(x481,x482)+E(f29(x481,x483),f29(x482,x483)) % 58.86/58.96 [49]~E(x491,x492)+E(f29(x493,x491),f29(x493,x492)) % 58.86/58.96 [50]~E(x501,x502)+E(f10(x501),f10(x502)) % 58.86/58.96 [51]~E(x511,x512)+E(f26(x511,x513),f26(x512,x513)) % 58.86/58.96 [52]~E(x521,x522)+E(f26(x523,x521),f26(x523,x522)) % 58.86/58.96 [53]~E(x531,x532)+E(f14(x531),f14(x532)) % 58.86/58.96 [54]~E(x541,x542)+E(f22(x541,x543),f22(x542,x543)) % 58.86/58.96 [55]~E(x551,x552)+E(f22(x553,x551),f22(x553,x552)) % 58.86/58.96 [56]~E(x561,x562)+E(f33(x561,x563,x564),f33(x562,x563,x564)) % 58.86/58.96 [57]~E(x571,x572)+E(f33(x573,x571,x574),f33(x573,x572,x574)) % 58.86/58.96 [58]~E(x581,x582)+E(f33(x583,x584,x581),f33(x583,x584,x582)) % 58.86/58.96 [59]~E(x591,x592)+E(f15(x591),f15(x592)) % 58.86/58.96 [60]~E(x601,x602)+E(f16(x601,x603),f16(x602,x603)) % 58.86/58.96 [61]~E(x611,x612)+E(f16(x613,x611),f16(x613,x612)) % 58.86/58.96 [62]~E(x621,x622)+E(f19(x621,x623),f19(x622,x623)) % 58.86/58.96 [63]~E(x631,x632)+E(f19(x633,x631),f19(x633,x632)) % 58.86/58.96 [64]~E(x641,x642)+E(f24(x641),f24(x642)) % 58.86/58.96 [65]~E(x651,x652)+E(f18(x651),f18(x652)) % 58.86/58.96 [66]~P1(x661)+P1(x662)+~E(x661,x662) % 58.86/58.96 [67]P2(x672,x673)+~E(x671,x672)+~P2(x671,x673) % 58.86/58.96 [68]P2(x683,x682)+~E(x681,x682)+~P2(x683,x681) % 58.86/58.96 [69]~P4(x691)+P4(x692)+~E(x691,x692) % 58.86/58.96 [70]~P5(x701)+P5(x702)+~E(x701,x702) % 58.86/58.96 [71]P7(x712,x713)+~E(x711,x712)+~P7(x711,x713) % 58.86/58.96 [72]P7(x723,x722)+~E(x721,x722)+~P7(x723,x721) % 58.86/58.96 [73]~P8(x731)+P8(x732)+~E(x731,x732) % 58.86/58.96 [74]P3(x742,x743)+~E(x741,x742)+~P3(x741,x743) % 58.86/58.96 [75]P3(x753,x752)+~E(x751,x752)+~P3(x753,x751) % 58.86/58.96 [76]~P6(x761)+P6(x762)+~E(x761,x762) % 58.86/58.96 [77]P10(x772,x773,x774)+~E(x771,x772)+~P10(x771,x773,x774) % 58.86/58.96 [78]P10(x783,x782,x784)+~E(x781,x782)+~P10(x783,x781,x784) % 58.86/58.96 [79]P10(x793,x794,x792)+~E(x791,x792)+~P10(x793,x794,x791) % 58.86/58.96 [80]~P9(x801)+P9(x802)+~E(x801,x802) % 58.86/58.96 % 58.86/58.96 %------------------------------------------- % 58.86/58.96 cnf(291,plain, % 58.86/58.96 (P2(a41,f35(f5(a1)))), % 58.86/58.96 inference(equality_inference,[],[107])). % 58.86/58.96 cnf(292,plain, % 58.86/58.96 (~P1(x2921)+~P3(a4,x2921)), % 58.86/58.96 inference(equality_inference,[],[113])). % 58.86/58.96 cnf(293,plain, % 58.86/58.96 (P2(f36(a41),f35(f5(a1)))), % 58.86/58.96 inference(equality_inference,[],[114])). % 58.86/58.96 cnf(298,plain, % 58.86/58.96 (~P1(x2981)+~P1(x2982)+P4(f42(x2982,x2981))+E(x2981,a4)), % 58.86/58.96 inference(equality_inference,[],[131])). % 58.86/58.96 cnf(321,plain, % 58.86/58.96 (~P10(x3211,x3212,x3213)+~P1(x3213)+~P1(x3212)+P2(x3211,f42(x3212,x3213))+~P1(x3211)+E(x3213,a4)), % 58.86/58.96 inference(equality_inference,[],[241])). % 58.86/58.96 cnf(327,plain, % 58.86/58.96 (P1(f36(a41))), % 58.86/58.96 inference(scs_inference,[],[293,139])). % 58.86/58.96 cnf(329,plain, % 58.86/58.96 (~E(f21(f36(a41)),a4)), % 58.86/58.96 inference(scs_inference,[],[293,139,147])). % 58.86/58.96 cnf(331,plain, % 58.86/58.96 (~E(f23(f36(a41)),a4)), % 58.86/58.96 inference(scs_inference,[],[293,139,147,148])). % 58.86/58.96 cnf(333,plain, % 58.86/58.96 (P1(f21(f36(a41)))), % 58.86/58.96 inference(scs_inference,[],[293,139,147,148,155])). % 58.86/58.96 cnf(335,plain, % 58.86/58.96 (P1(f23(f36(a41)))), % 58.86/58.96 inference(scs_inference,[],[293,139,147,148,155,156])). % 58.86/58.96 cnf(337,plain, % 58.86/58.96 (E(a2,a1)), % 58.86/58.96 inference(scs_inference,[],[81,293,139,147,148,155,156,2])). % 58.86/58.96 cnf(338,plain, % 58.86/58.96 (~P2(f36(a41),f5(a1))), % 58.86/58.96 inference(scs_inference,[],[81,293,139,147,148,155,156,2,179])). % 58.86/58.96 cnf(348,plain, % 58.86/58.96 (P10(a4,a4,f21(f36(a41)))), % 58.86/58.96 inference(scs_inference,[],[81,82,293,84,85,86,92,139,147,148,155,156,2,179,68,69,70,73,298,173,180])). % 58.86/58.96 cnf(350,plain, % 58.86/58.96 (P2(a4,f42(a4,f21(f36(a41))))), % 58.86/58.96 inference(scs_inference,[],[81,82,293,84,85,86,92,139,147,148,155,156,2,179,68,69,70,73,298,173,180,321])). % 58.86/58.96 cnf(365,plain, % 58.86/58.96 (P1(f21(a41))), % 58.86/58.96 inference(scs_inference,[],[291,155])). % 58.86/58.96 cnf(367,plain, % 58.86/58.96 (P1(f23(a41))), % 58.86/58.96 inference(scs_inference,[],[291,155,156])). % 58.86/58.96 cnf(369,plain, % 58.86/58.96 (~E(f23(a41),a4)), % 58.86/58.96 inference(scs_inference,[],[291,155,156,148])). % 58.86/58.96 cnf(371,plain, % 58.86/58.96 (~E(f21(a41),a4)), % 58.86/58.96 inference(scs_inference,[],[291,155,156,148,147])). % 58.86/58.96 cnf(373,plain, % 58.86/58.96 (~P2(a41,f5(a1))), % 58.86/58.96 inference(scs_inference,[],[291,155,156,148,147,179])). % 58.86/58.96 cnf(375,plain, % 58.86/58.96 (E(a6,f35(f5(a1)))), % 58.86/58.96 inference(scs_inference,[],[291,86,155,156,148,147,179,2])). % 58.86/58.96 cnf(377,plain, % 58.86/58.96 (P10(a4,a4,f23(f36(a41)))), % 58.86/58.96 inference(scs_inference,[],[82,335,331,291,91,86,155,156,148,147,179,2,69,180])). % 58.86/58.96 cnf(381,plain, % 58.86/58.96 (P2(a4,f42(a4,f23(f36(a41))))), % 58.86/58.96 inference(scs_inference,[],[82,335,331,291,91,86,155,156,148,147,179,2,69,180,298,321])). % 58.86/58.96 cnf(383,plain, % 58.86/58.96 (P2(x3831,f42(a4,f21(f36(a41))))+~E(a4,x3831)), % 58.86/58.96 inference(scs_inference,[],[82,335,350,331,291,91,86,155,156,148,147,179,2,69,180,298,321,67])). % 58.86/58.96 cnf(389,plain, % 58.86/58.96 (P10(a4,a4,f23(a41))), % 58.86/58.96 inference(scs_inference,[],[82,367,369,180])). % 58.86/58.96 cnf(393,plain, % 58.86/58.96 (P2(a4,f42(a4,f23(a41)))), % 58.86/58.96 inference(scs_inference,[],[82,367,369,180,298,321])). % 58.86/58.96 cnf(412,plain, % 58.86/58.96 (P10(a4,a4,f21(a41))), % 58.86/58.96 inference(scs_inference,[],[82,371,365,180])). % 58.86/58.96 cnf(416,plain, % 58.86/58.96 (P2(a4,f42(a4,f21(a41)))), % 58.86/58.96 inference(scs_inference,[],[82,371,365,180,298,321])). % 58.86/58.96 cnf(461,plain, % 58.86/58.96 (P1(x4611)+~P2(x4611,f42(a41,f21(a41)))), % 58.86/58.96 inference(scs_inference,[],[293,291,246,245,228])). % 58.86/58.96 cnf(463,plain, % 58.86/58.96 (P2(x4631,f42(a4,f23(f36(a41))))+~E(a4,x4631)), % 58.86/58.96 inference(scs_inference,[],[381,293,291,246,245,228,67])). % 58.86/58.96 cnf(472,plain, % 58.86/58.96 (P10(a4,x4721,f23(f36(a41)))+~E(a4,x4721)), % 58.86/58.96 inference(scs_inference,[],[375,291,377,246,70,260,78])). % 58.86/58.96 cnf(473,plain, % 58.86/58.96 (P1(x4731)+~P2(x4731,f42(a41,f23(a41)))), % 58.86/58.96 inference(scs_inference,[],[375,291,377,246,70,260,78,229])). % 58.86/58.96 cnf(483,plain, % 58.86/58.96 (P2(x4831,f42(a4,f21(a41)))+~E(a4,x4831)), % 58.86/58.96 inference(scs_inference,[],[416,67])). % 58.86/58.96 cnf(490,plain, % 58.86/58.96 (P10(a4,x4901,f21(a41))+~E(a4,x4901)), % 58.86/58.96 inference(scs_inference,[],[375,337,412,80,73,78])). % 58.86/58.96 cnf(491,plain, % 58.86/58.96 (P10(x4911,a4,f21(a41))+~E(a4,x4911)), % 58.86/58.96 inference(scs_inference,[],[375,337,412,80,73,78,77])). % 58.86/58.96 cnf(493,plain, % 58.86/58.96 (P2(x4931,f42(a4,f23(a41)))+~E(a4,x4931)), % 58.86/58.96 inference(scs_inference,[],[375,337,393,412,80,73,78,77,76,67])). % 58.86/58.96 cnf(498,plain, % 58.86/58.96 (P10(x4981,a4,f21(f36(a41)))+~E(a4,x4981)), % 58.86/58.96 inference(scs_inference,[],[337,348,80,77])). % 58.86/58.96 cnf(502,plain, % 58.86/58.96 (P10(a4,x5021,f21(f36(a41)))+~E(a4,x5021)), % 58.86/58.96 inference(scs_inference,[],[337,86,348,80,77,70,76,79,78])). % 58.86/58.96 cnf(511,plain, % 58.86/58.96 (P10(x5111,a4,f23(a41))+~E(a4,x5111)), % 58.86/58.96 inference(scs_inference,[],[81,291,86,389,80,67,76,79,66,77])). % 58.86/58.96 cnf(515,plain, % 58.86/58.96 (P10(a4,x5151,f23(a41))+~E(a4,x5151)), % 58.86/58.96 inference(scs_inference,[],[389,78])). % 58.86/58.96 cnf(528,plain, % 58.86/58.96 (P10(x5281,a4,f23(f36(a41)))+~E(a4,x5281)), % 58.86/58.96 inference(scs_inference,[],[377,77])). % 58.86/58.96 cnf(812,plain, % 58.86/58.96 (P1(f36(f21(a41)))), % 58.86/58.96 inference(scs_inference,[],[291,94,155])). % 58.86/58.96 cnf(914,plain, % 58.86/58.96 (P2(a41,f42(a41,f23(a41)))), % 58.86/58.96 inference(scs_inference,[],[83,369,367,291,180,298,272])). % 58.86/58.96 cnf(919,plain, % 58.86/58.96 (P3(f23(a41),f38(a41,f36(a41)))), % 58.86/58.96 inference(scs_inference,[],[83,369,367,291,373,180,298,272,246,68,261])). % 58.86/58.96 cnf(924,plain, % 58.86/58.96 (E(f38(a41,f36(a41)),f37(f23(a41),f27(a41,a41)))), % 58.86/58.96 inference(scs_inference,[],[83,369,367,291,373,180,298,272,246,68,261,268,73,2])). % 58.86/58.96 cnf(936,plain, % 58.86/58.96 (P2(a41,f42(a41,f21(a41)))), % 58.86/58.96 inference(scs_inference,[],[83,371,914,924,919,365,291,373,75,173,180,271])). % 58.86/58.96 cnf(942,plain, % 58.86/58.96 (P1(f22(a41,a41))), % 58.86/58.96 inference(scs_inference,[],[83,371,914,924,919,365,291,373,75,173,180,271,298,267,245])). % 58.86/58.96 cnf(1468,plain, % 58.86/58.96 (E(f38(a4,f36(a41)),f36(a41))), % 58.86/58.96 inference(scs_inference,[],[293,97,139])). % 58.86/58.96 cnf(1469,plain, % 58.86/58.96 (E(f36(a41),f38(a4,f36(a41)))), % 58.86/58.96 inference(scs_inference,[],[1468,2])). % 58.86/58.96 cnf(2439,plain, % 58.86/58.96 (E(f37(a4,a41),a4)), % 58.86/58.96 inference(scs_inference,[],[936,461,95])). % 58.86/58.96 cnf(2442,plain, % 58.86/58.96 (~E(f21(a41),f37(a4,a41))), % 58.86/58.96 inference(scs_inference,[],[82,371,2439,2,66,3])). % 58.86/58.96 cnf(2760,plain, % 58.86/58.96 (E(f37(a41,a4),a4)), % 58.86/58.96 inference(scs_inference,[],[914,473,96])). % 58.86/58.96 cnf(2774,plain, % 58.86/58.96 (P1(f37(a41,a4))), % 58.86/58.96 inference(scs_inference,[],[82,2760,2,383,463,491,490,483,515,498,472,511,502,493,528,66])). % 58.86/58.96 cnf(3171,plain, % 58.86/58.96 (P10(f36(a41),f38(a4,f36(a41)),f23(f36(a41)))), % 58.86/58.96 inference(scs_inference,[],[327,1469,331,329,333,335,338,293,2439,113,298,180,321,241,246,77,68,78])). % 58.86/58.96 cnf(3182,plain, % 58.86/58.96 (P10(f36(a41),f36(a41),f23(a41))), % 58.86/58.96 inference(scs_inference,[],[327,1469,369,367,3171,77,180])). % 58.86/58.96 cnf(3204,plain, % 58.86/58.96 (P1(f22(f36(a41),f36(a41)))), % 58.86/58.96 inference(scs_inference,[],[327,1469,329,333,338,293,3182,77,78,180,321,241,245])). % 58.86/58.96 cnf(3775,plain, % 58.86/58.96 (E(f31(a1,x37751,x37752),f31(a2,x37751,x37752))), % 58.86/58.96 inference(scs_inference,[],[81,3204,2774,94,292,98,99,100,95,4,5,9,12,15,19,32,37,45,50,53,59,64,65,103,104,10,11,13,14,20,21,22,23,30,31,33,34,35,36,41,42,43,44,46,47,48,49,51,52,54,55,60,61,62,63,105,106,6])). % 58.86/58.96 cnf(3792,plain, % 58.86/58.96 (P7(f42(a41,f23(a41)),f35(f5(a1)))), % 58.86/58.96 inference(scs_inference,[],[81,3204,2774,291,94,292,98,99,100,95,4,5,9,12,15,19,32,37,45,50,53,59,64,65,103,104,10,11,13,14,20,21,22,23,30,31,33,34,35,36,41,42,43,44,46,47,48,49,51,52,54,55,60,61,62,63,105,106,6,7,8,16,17,18,27,28,29,38,39,40,56,57,58,209,210])). % 58.86/58.96 cnf(3978,plain, % 58.86/58.96 ($false), % 58.86/58.96 inference(scs_inference,[],[2442,3775,812,3792,2774,942,369,367,365,371,100,106,19,41,98,99,31,29,39,57,16,58,60,36,105,15,18,11,12,103,7,94,4,21,34,49,97,50,17,104,292,22,51,54,20,95,52,14,35,62,56,53,44,40,42,38,48,13,64,5,32,33,9,30,46,65,47,37,43,63,23,59,6,45,27,55,8,10,61,28,26,2,24,25,96,154,196]), % 58.86/58.96 ['proof']). % 58.86/58.96 % SZS output end Proof % 58.86/58.96 % Total time :58.230000s %------------------------------------------------------------------------------