%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM443+4 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n023.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 12:24:17 EDT 2024 % Result : Theorem 58.71s 58.76s % Output : CNFRefutation 58.71s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.14 % Problem : NUM443+4 : TPTP v8.2.0. Released v4.0.0. % 0.08/0.14 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.35 % Computer : n023.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.36 % WCLimit : 300 % 0.13/0.36 % DateTime : Sun Jun 23 04:09:39 EDT 2024 % 0.13/0.36 % CPUTime : % 0.22/0.59 start to proof:theBenchmark % 58.68/58.73 %------------------------------------------- % 58.68/58.73 % File :CSE---1.7 % 58.68/58.73 % Problem :theBenchmark % 58.68/58.73 % Transform :cnf % 58.68/58.73 % Format :tptp:raw % 58.68/58.73 % Command :java -jar mcs_scs.jar %d %s % 58.68/58.73 % 58.68/58.73 % Result :Theorem 58.060000s % 58.68/58.73 % Output :CNFRefutation 58.060000s % 58.68/58.73 %------------------------------------------- % 58.71/58.74 %------------------------------------------------------------------------------ % 58.71/58.74 % File : NUM443+4 : TPTP v8.2.0. Released v4.0.0. % 58.71/58.74 % Domain : Number Theory % 58.71/58.74 % Problem : Fuerstenberg's infinitude of primes 10_01, 03 expansion % 58.71/58.74 % Version : Especial. % 58.71/58.74 % English : % 58.71/58.74 % 58.71/58.74 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 58.71/58.74 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 58.71/58.74 % Source : [Pas08] % 58.71/58.74 % Names : fuerst_10_01.03 [Pas08] % 58.71/58.74 % 58.71/58.74 % Status : Theorem % 58.71/58.74 % Rating : 0.19 v8.1.0, 0.11 v7.5.0, 0.09 v7.4.0, 0.13 v7.3.0, 0.14 v7.2.0, 0.10 v7.1.0, 0.09 v7.0.0, 0.07 v6.4.0, 0.15 v6.3.0, 0.08 v6.1.0, 0.20 v6.0.0, 0.26 v5.4.0, 0.32 v5.3.0, 0.37 v5.2.0, 0.20 v5.1.0, 0.33 v5.0.0, 0.42 v4.1.0, 0.52 v4.0.1, 0.83 v4.0.0 % 58.71/58.74 % Syntax : Number of formulae : 43 ( 2 unt; 10 def) % 58.71/58.74 % Number of atoms : 220 ( 43 equ) % 58.71/58.74 % Maximal formula atoms : 34 ( 5 avg) % 58.71/58.74 % Number of connectives : 193 ( 16 ~; 7 |; 98 &) % 58.71/58.74 % ( 16 <=>; 56 =>; 0 <=; 0 <~>) % 58.71/58.74 % Maximal formula depth : 12 ( 6 avg) % 58.71/58.74 % Maximal term depth : 3 ( 1 avg) % 58.71/58.74 % Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty) % 58.71/58.74 % Number of functors : 15 ( 15 usr; 7 con; 0-2 aty) % 58.71/58.74 % Number of variables : 94 ( 85 !; 9 ?) % 58.71/58.74 % SPC : FOF_THM_RFO_SEQ % 58.71/58.74 % 58.71/58.74 % Comments : Problem generated by the SAD system [VLP07] % 58.71/58.74 %------------------------------------------------------------------------------ % 58.71/58.74 fof(mIntegers,axiom, % 58.71/58.74 ! [W0] : % 58.71/58.74 ( aInteger0(W0) % 58.71/58.74 => $true ) ). % 58.71/58.74 % 58.71/58.74 fof(mIntZero,axiom, % 58.71/58.74 aInteger0(sz00) ). % 58.71/58.74 % 58.71/58.74 fof(mIntOne,axiom, % 58.71/58.74 aInteger0(sz10) ). % 58.71/58.74 % 58.71/58.74 fof(mIntNeg,axiom, % 58.71/58.74 ! [W0] : % 58.71/58.74 ( aInteger0(W0) % 58.71/58.74 => aInteger0(smndt0(W0)) ) ). % 58.71/58.74 % 58.71/58.74 fof(mIntPlus,axiom, % 58.71/58.74 ! [W0,W1] : % 58.71/58.74 ( ( aInteger0(W0) % 58.71/58.74 & aInteger0(W1) ) % 58.71/58.74 => aInteger0(sdtpldt0(W0,W1)) ) ). % 58.71/58.74 % 58.71/58.74 fof(mIntMult,axiom, % 58.71/58.75 ! [W0,W1] : % 58.71/58.75 ( ( aInteger0(W0) % 58.71/58.75 & aInteger0(W1) ) % 58.71/58.75 => aInteger0(sdtasdt0(W0,W1)) ) ). % 58.71/58.75 % 58.71/58.75 fof(mAddAsso,axiom, % 58.71/58.75 ! [W0,W1,W2] : % 58.71/58.75 ( ( aInteger0(W0) % 58.71/58.75 & aInteger0(W1) % 58.71/58.75 & aInteger0(W2) ) % 58.71/58.75 => sdtpldt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtpldt0(W0,W1),W2) ) ). % 58.71/58.75 % 58.71/58.75 fof(mAddComm,axiom, % 58.71/58.75 ! [W0,W1] : % 58.71/58.75 ( ( aInteger0(W0) % 58.71/58.75 & aInteger0(W1) ) % 58.71/58.75 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 58.71/58.75 % 58.71/58.75 fof(mAddZero,axiom, % 58.71/58.75 ! [W0] : % 58.71/58.75 ( aInteger0(W0) % 58.71/58.75 => ( sdtpldt0(W0,sz00) = W0 % 58.71/58.75 & W0 = sdtpldt0(sz00,W0) ) ) ). % 58.71/58.75 % 58.71/58.75 fof(mAddNeg,axiom, % 58.71/58.75 ! [W0] : % 58.71/58.75 ( aInteger0(W0) % 58.71/58.75 => ( sdtpldt0(W0,smndt0(W0)) = sz00 % 58.71/58.75 & sz00 = sdtpldt0(smndt0(W0),W0) ) ) ). % 58.71/58.75 % 58.71/58.75 fof(mMulAsso,axiom, % 58.71/58.75 ! [W0,W1,W2] : % 58.71/58.75 ( ( aInteger0(W0) % 58.71/58.75 & aInteger0(W1) % 58.71/58.75 & aInteger0(W2) ) % 58.71/58.75 => sdtasdt0(W0,sdtasdt0(W1,W2)) = sdtasdt0(sdtasdt0(W0,W1),W2) ) ). % 58.71/58.75 % 58.71/58.75 fof(mMulComm,axiom, % 58.71/58.75 ! [W0,W1] : % 58.71/58.75 ( ( aInteger0(W0) % 58.71/58.75 & aInteger0(W1) ) % 58.71/58.75 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 58.71/58.75 % 58.71/58.75 fof(mMulOne,axiom, % 58.71/58.75 ! [W0] : % 58.71/58.75 ( aInteger0(W0) % 58.71/58.75 => ( sdtasdt0(W0,sz10) = W0 % 58.71/58.75 & W0 = sdtasdt0(sz10,W0) ) ) ). % 58.71/58.75 % 58.71/58.75 fof(mDistrib,axiom, % 58.71/58.75 ! [W0,W1,W2] : % 58.71/58.75 ( ( aInteger0(W0) % 58.71/58.75 & aInteger0(W1) % 58.71/58.75 & aInteger0(W2) ) % 58.71/58.75 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 58.71/58.75 & sdtasdt0(sdtpldt0(W0,W1),W2) = sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W1,W2)) ) ) ). % 58.71/58.75 % 58.71/58.75 fof(mMulZero,axiom, % 58.71/58.75 ! [W0] : % 58.71/58.75 ( aInteger0(W0) % 58.71/58.75 => ( sdtasdt0(W0,sz00) = sz00 % 58.71/58.75 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 58.71/58.75 % 58.71/58.75 fof(mMulMinOne,axiom, % 58.71/58.75 ! [W0] : % 58.71/58.75 ( aInteger0(W0) % 58.71/58.75 => ( sdtasdt0(smndt0(sz10),W0) = smndt0(W0) % 58.71/58.75 & smndt0(W0) = sdtasdt0(W0,smndt0(sz10)) ) ) ). % 58.71/58.75 % 58.71/58.75 fof(mZeroDiv,axiom, % 58.71/58.75 ! [W0,W1] : % 58.71/58.75 ( ( aInteger0(W0) % 58.71/58.75 & aInteger0(W1) ) % 58.71/58.75 => ( sdtasdt0(W0,W1) = sz00 % 58.71/58.75 => ( W0 = sz00 % 58.71/58.75 | W1 = sz00 ) ) ) ). % 58.71/58.75 % 58.71/58.75 fof(mDivisor,definition, % 58.71/58.75 ! [W0] : % 58.71/58.75 ( aInteger0(W0) % 58.71/58.75 => ! [W1] : % 58.71/58.75 ( aDivisorOf0(W1,W0) % 58.71/58.75 <=> ( aInteger0(W1) % 58.71/58.75 & W1 != sz00 % 58.71/58.75 & ? [W2] : % 58.71/58.75 ( aInteger0(W2) % 58.71/58.75 & sdtasdt0(W1,W2) = W0 ) ) ) ) ). % 58.71/58.75 % 58.71/58.75 fof(mEquMod,definition, % 58.71/58.75 ! [W0,W1,W2] : % 58.71/58.75 ( ( aInteger0(W0) % 58.71/58.75 & aInteger0(W1) % 58.71/58.75 & aInteger0(W2) % 58.71/58.75 & W2 != sz00 ) % 58.71/58.75 => ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 58.71/58.75 <=> aDivisorOf0(W2,sdtpldt0(W0,smndt0(W1))) ) ) ). % 58.71/58.75 % 58.71/58.75 fof(mEquModRef,axiom, % 58.71/58.75 ! [W0,W1] : % 58.71/58.75 ( ( aInteger0(W0) % 58.71/58.75 & aInteger0(W1) % 58.71/58.75 & W1 != sz00 ) % 58.71/58.75 => sdteqdtlpzmzozddtrp0(W0,W0,W1) ) ). % 58.71/58.75 % 58.71/58.75 fof(mEquModSym,axiom, % 58.71/58.75 ! [W0,W1,W2] : % 58.71/58.75 ( ( aInteger0(W0) % 58.71/58.75 & aInteger0(W1) % 58.71/58.75 & aInteger0(W2) % 58.71/58.75 & W2 != sz00 ) % 58.71/58.75 => ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 58.71/58.75 => sdteqdtlpzmzozddtrp0(W1,W0,W2) ) ) ). % 58.71/58.75 % 58.71/58.75 fof(mEquModTrn,axiom, % 58.71/58.75 ! [W0,W1,W2,W3] : % 58.71/58.75 ( ( aInteger0(W0) % 58.71/58.75 & aInteger0(W1) % 58.71/58.75 & aInteger0(W2) % 58.71/58.75 & W2 != sz00 % 58.71/58.75 & aInteger0(W3) ) % 58.71/58.75 => ( ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 58.71/58.75 & sdteqdtlpzmzozddtrp0(W1,W3,W2) ) % 58.71/58.75 => sdteqdtlpzmzozddtrp0(W0,W3,W2) ) ) ). % 58.71/58.75 % 58.71/58.75 fof(mEquModMul,axiom, % 58.71/58.75 ! [W0,W1,W2,W3] : % 58.71/58.75 ( ( aInteger0(W0) % 58.71/58.75 & aInteger0(W1) % 58.71/58.75 & aInteger0(W2) % 58.71/58.75 & W2 != sz00 % 58.71/58.75 & aInteger0(W3) % 58.71/58.75 & W3 != sz00 ) % 58.71/58.75 => ( sdteqdtlpzmzozddtrp0(W0,W1,sdtasdt0(W2,W3)) % 58.71/58.75 => ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 58.71/58.75 & sdteqdtlpzmzozddtrp0(W0,W1,W3) ) ) ) ). % 58.71/58.75 % 58.71/58.75 fof(mPrime,axiom, % 58.71/58.75 ! [W0] : % 58.71/58.75 ( ( aInteger0(W0) % 58.71/58.75 & W0 != sz00 ) % 58.71/58.75 => ( isPrime0(W0) % 58.71/58.75 => $true ) ) ). % 58.71/58.75 % 58.71/58.75 fof(mPrimeDivisor,axiom, % 58.71/58.75 ! [W0] : % 58.71/58.75 ( aInteger0(W0) % 58.71/58.75 => ( ? [W1] : % 58.71/58.75 ( aDivisorOf0(W1,W0) % 58.71/58.75 & isPrime0(W1) ) % 58.71/58.75 <=> ( W0 != sz10 % 58.71/58.75 & W0 != smndt0(sz10) ) ) ) ). % 58.71/58.75 % 58.71/58.75 fof(mSets,axiom, % 58.71/58.75 ! [W0] : % 58.71/58.75 ( aSet0(W0) % 58.71/58.75 => $true ) ). % 58.71/58.75 % 58.71/58.75 fof(mElements,axiom, % 58.71/58.75 ! [W0] : % 58.71/58.75 ( aSet0(W0) % 58.71/58.75 => ! [W1] : % 58.71/58.75 ( aElementOf0(W1,W0) % 58.71/58.75 => $true ) ) ). % 58.71/58.75 % 58.71/58.75 fof(mSubset,definition, % 58.71/58.75 ! [W0] : % 58.71/58.75 ( aSet0(W0) % 58.71/58.75 => ! [W1] : % 58.71/58.75 ( aSubsetOf0(W1,W0) % 58.71/58.75 <=> ( aSet0(W1) % 58.71/58.75 & ! [W2] : % 58.71/58.75 ( aElementOf0(W2,W1) % 58.71/58.75 => aElementOf0(W2,W0) ) ) ) ) ). % 58.71/58.75 % 58.71/58.75 fof(mFinSet,axiom, % 58.71/58.75 ! [W0] : % 58.71/58.75 ( aSet0(W0) % 58.71/58.75 => ( isFinite0(W0) % 58.71/58.75 => $true ) ) ). % 58.71/58.75 % 58.71/58.75 fof(mUnion,definition, % 58.71/58.75 ! [W0,W1] : % 58.71/58.75 ( ( aSubsetOf0(W0,cS1395) % 58.71/58.75 & aSubsetOf0(W1,cS1395) ) % 58.71/58.75 => ! [W2] : % 58.71/58.75 ( W2 = sdtbsmnsldt0(W0,W1) % 58.71/58.75 <=> ( aSet0(W2) % 58.71/58.75 & ! [W3] : % 58.71/58.75 ( aElementOf0(W3,W2) % 58.71/58.75 <=> ( aInteger0(W3) % 58.71/58.75 & ( aElementOf0(W3,W0) % 58.71/58.75 | aElementOf0(W3,W1) ) ) ) ) ) ) ). % 58.71/58.75 % 58.71/58.75 fof(mIntersection,definition, % 58.71/58.75 ! [W0,W1] : % 58.71/58.75 ( ( aSubsetOf0(W0,cS1395) % 58.71/58.75 & aSubsetOf0(W1,cS1395) ) % 58.71/58.75 => ! [W2] : % 58.71/58.75 ( W2 = sdtslmnbsdt0(W0,W1) % 58.71/58.75 <=> ( aSet0(W2) % 58.71/58.75 & ! [W3] : % 58.71/58.75 ( aElementOf0(W3,W2) % 58.71/58.75 <=> ( aInteger0(W3) % 58.71/58.75 & aElementOf0(W3,W0) % 58.71/58.75 & aElementOf0(W3,W1) ) ) ) ) ) ). % 58.71/58.75 % 58.71/58.75 fof(mUnionSet,definition, % 58.71/58.75 ! [W0] : % 58.71/58.75 ( ( aSet0(W0) % 58.71/58.75 & ! [W1] : % 58.71/58.75 ( aElementOf0(W1,W0) % 58.71/58.75 => aSubsetOf0(W1,cS1395) ) ) % 58.71/58.75 => ! [W1] : % 58.71/58.75 ( W1 = sbsmnsldt0(W0) % 58.71/58.75 <=> ( aSet0(W1) % 58.71/58.75 & ! [W2] : % 58.71/58.75 ( aElementOf0(W2,W1) % 58.71/58.75 <=> ( aInteger0(W2) % 58.71/58.75 & ? [W3] : % 58.71/58.75 ( aElementOf0(W3,W0) % 58.71/58.75 & aElementOf0(W2,W3) ) ) ) ) ) ) ). % 58.71/58.75 % 58.71/58.75 fof(mComplement,definition, % 58.71/58.75 ! [W0] : % 58.71/58.75 ( aSubsetOf0(W0,cS1395) % 58.71/58.75 => ! [W1] : % 58.71/58.75 ( W1 = stldt0(W0) % 58.71/58.75 <=> ( aSet0(W1) % 58.71/58.75 & ! [W2] : % 58.71/58.75 ( aElementOf0(W2,W1) % 58.71/58.75 <=> ( aInteger0(W2) % 58.71/58.75 & ~ aElementOf0(W2,W0) ) ) ) ) ) ). % 58.71/58.75 % 58.71/58.75 fof(mArSeq,definition, % 58.71/58.75 ! [W0,W1] : % 58.71/58.75 ( ( aInteger0(W0) % 58.71/58.75 & aInteger0(W1) % 58.71/58.75 & W1 != sz00 ) % 58.71/58.75 => ! [W2] : % 58.71/58.75 ( W2 = szAzrzSzezqlpdtcmdtrp0(W0,W1) % 58.71/58.75 <=> ( aSet0(W2) % 58.71/58.75 & ! [W3] : % 58.71/58.75 ( aElementOf0(W3,W2) % 58.71/58.75 <=> ( aInteger0(W3) % 58.71/58.75 & sdteqdtlpzmzozddtrp0(W3,W0,W1) ) ) ) ) ) ). % 58.71/58.75 % 58.71/58.76 fof(mOpen,definition, % 58.71/58.76 ! [W0] : % 58.71/58.76 ( aSubsetOf0(W0,cS1395) % 58.71/58.76 => ( isOpen0(W0) % 58.71/58.76 <=> ! [W1] : % 58.71/58.76 ( aElementOf0(W1,W0) % 58.71/58.76 => ? [W2] : % 58.71/58.76 ( aInteger0(W2) % 58.71/58.76 & W2 != sz00 % 58.71/58.76 & aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W1,W2),W0) ) ) ) ) ). % 58.71/58.76 % 58.71/58.76 fof(mClosed,definition, % 58.71/58.76 ! [W0] : % 58.71/58.76 ( aSubsetOf0(W0,cS1395) % 58.71/58.76 => ( isClosed0(W0) % 58.71/58.76 <=> isOpen0(stldt0(W0)) ) ) ). % 58.71/58.76 % 58.71/58.76 fof(mUnionOpen,axiom, % 58.71/58.76 ! [W0] : % 58.71/58.76 ( ( aSet0(W0) % 58.71/58.76 & ! [W1] : % 58.71/58.76 ( aElementOf0(W1,W0) % 58.71/58.76 => ( aSubsetOf0(W1,cS1395) % 58.71/58.76 & isOpen0(W1) ) ) ) % 58.71/58.76 => isOpen0(sbsmnsldt0(W0)) ) ). % 58.71/58.76 % 58.71/58.76 fof(mInterOpen,axiom, % 58.71/58.76 ! [W0,W1] : % 58.71/58.76 ( ( aSubsetOf0(W0,cS1395) % 58.71/58.76 & aSubsetOf0(W1,cS1395) % 58.71/58.76 & isOpen0(W0) % 58.71/58.76 & isOpen0(W1) ) % 58.71/58.76 => isOpen0(sdtslmnbsdt0(W0,W1)) ) ). % 58.71/58.76 % 58.71/58.76 fof(mUnionClosed,axiom, % 58.71/58.76 ! [W0,W1] : % 58.71/58.76 ( ( aSubsetOf0(W0,cS1395) % 58.71/58.76 & aSubsetOf0(W1,cS1395) % 58.71/58.76 & isClosed0(W0) % 58.71/58.76 & isClosed0(W1) ) % 58.71/58.76 => isClosed0(sdtbsmnsldt0(W0,W1)) ) ). % 58.71/58.76 % 58.71/58.76 fof(mUnionSClosed,axiom, % 58.71/58.76 ! [W0] : % 58.71/58.76 ( ( aSet0(W0) % 58.71/58.76 & isFinite0(W0) % 58.71/58.76 & ! [W1] : % 58.71/58.76 ( aElementOf0(W1,W0) % 58.71/58.76 => ( aSubsetOf0(W1,cS1395) % 58.71/58.76 & isClosed0(W1) ) ) ) % 58.71/58.76 => isClosed0(sbsmnsldt0(W0)) ) ). % 58.71/58.76 % 58.71/58.76 fof(m__1962,hypothesis, % 58.71/58.76 ( aInteger0(xa) % 58.71/58.76 & aInteger0(xq) % 58.71/58.76 & xq != sz00 ) ). % 58.71/58.76 % 58.71/58.76 fof(m__2010,hypothesis, % 58.71/58.76 ( aInteger0(xb) % 58.71/58.76 & aInteger0(xc) ) ). % 58.71/58.76 % 58.71/58.76 fof(m__,conjecture, % 58.71/58.76 ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) % 58.71/58.76 & ! [W0] : % 58.71/58.76 ( ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) % 58.71/58.76 => ( aInteger0(W0) % 58.71/58.76 & ? [W1] : % 58.71/58.76 ( aInteger0(W1) % 58.71/58.76 & sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa)) ) % 58.71/58.76 & aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa))) % 58.71/58.76 & sdteqdtlpzmzozddtrp0(W0,xa,xq) ) ) % 58.71/58.76 & ( ( aInteger0(W0) % 58.71/58.76 & ( ? [W1] : % 58.71/58.76 ( aInteger0(W1) % 58.71/58.76 & sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa)) ) % 58.71/58.76 | aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa))) % 58.71/58.76 | sdteqdtlpzmzozddtrp0(W0,xa,xq) ) ) % 58.71/58.76 => aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ) % 58.71/58.76 & ~ aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq)) % 58.71/58.76 & aElementOf0(xb,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) % 58.71/58.76 & ? [W0] : % 58.71/58.76 ( aInteger0(W0) % 58.71/58.76 & sdtasdt0(xq,W0) = sdtpldt0(xc,smndt0(xb)) ) % 58.71/58.76 & aDivisorOf0(xq,sdtpldt0(xc,smndt0(xb))) % 58.71/58.76 & sdteqdtlpzmzozddtrp0(xc,xb,xq) ) % 58.71/58.76 => ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) % 58.71/58.76 & ! [W0] : % 58.71/58.76 ( ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) % 58.71/58.76 => ( aInteger0(W0) % 58.71/58.76 & ? [W1] : % 58.71/58.76 ( aInteger0(W1) % 58.71/58.76 & sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa)) ) % 58.71/58.76 & aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa))) % 58.71/58.76 & sdteqdtlpzmzozddtrp0(W0,xa,xq) ) ) % 58.71/58.76 & ( ( aInteger0(W0) % 58.71/58.76 & ( ? [W1] : % 58.71/58.76 ( aInteger0(W1) % 58.71/58.76 & sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa)) ) % 58.71/58.76 | aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa))) % 58.71/58.76 | sdteqdtlpzmzozddtrp0(W0,xa,xq) ) ) % 58.71/58.76 => aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ) ) % 58.71/58.76 => ( ~ aElementOf0(xc,szAzrzSzezqlpdtcmdtrp0(xa,xq)) % 58.71/58.76 | aElementOf0(xc,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ) ) ) ). % 58.71/58.76 % 58.71/58.76 %------------------------------------------------------------------------------ % 58.71/58.76 %------------------------------------------- % 58.71/58.76 % Proof found % 58.71/58.76 % SZS status Theorem for theBenchmark % 58.71/58.76 % SZS output start Proof % 58.71/58.76 %ClaNum:198(EqnAxiom:62) % 58.71/58.76 %VarNum:888(SingletonVarNum:263) % 58.71/58.76 %MaxLitNum:8 % 58.71/58.76 %MaxfuncDepth:2 % 58.71/58.76 %SharedTerms:31 % 58.71/58.76 %goalClause: 69 71 72 73 74 75 76 78 79 114 118 119 136 137 142 144 152 157 165 % 58.71/58.76 %singleGoalClaCount:9 % 58.71/58.76 [63]P1(a1) % 58.71/58.76 [64]P1(a28) % 58.71/58.76 [65]P1(a29) % 58.71/58.76 [66]P1(a31) % 58.71/58.76 [67]P1(a32) % 58.71/58.76 [68]P1(a33) % 58.71/58.76 [69]P1(a2) % 58.71/58.76 [75]P5(a33,a32,a31) % 58.71/58.76 [77]~E(a1,a31) % 58.71/58.76 [71]P4(f30(a29,a31)) % 58.71/58.76 [73]P2(a33,f30(a29,a31)) % 58.71/58.76 [78]~P2(a32,f30(a29,a31)) % 58.71/58.76 [72]E(f12(a33,f11(a32)),f13(a31,a2)) % 58.71/58.76 [74]P3(a31,f12(a33,f11(a32))) % 58.71/58.76 [76]P2(a32,f27(f30(a29,a31))) % 58.71/58.76 [79]~P2(a33,f27(f30(a29,a31))) % 58.71/58.76 [80]~P1(x801)+P1(f11(x801)) % 58.71/58.76 [81]~P1(x811)+E(f13(a1,x811),a1) % 58.71/58.76 [82]~P1(x821)+E(f13(x821,a1),a1) % 58.71/58.76 [83]~P1(x831)+E(f12(a1,x831),x831) % 58.71/58.76 [84]~P1(x841)+E(f13(a28,x841),x841) % 58.71/58.76 [85]~P1(x851)+E(f12(x851,a1),x851) % 58.71/58.76 [86]~P1(x861)+E(f13(x861,a28),x861) % 58.71/58.76 [114]P1(x1141)+~P2(x1141,f30(a29,a31)) % 58.71/58.76 [118]~P2(x1181,f30(a29,a31))+P1(f10(x1181)) % 58.71/58.76 [119]~P2(x1191,f30(a29,a31))+P1(f16(x1191)) % 58.71/58.76 [152]~P2(x1521,f30(a29,a31))+P5(x1521,a29,a31) % 58.71/58.76 [88]~P1(x881)+E(f12(f11(x881),x881),a1) % 58.71/58.76 [89]~P1(x891)+E(f12(x891,f11(x891)),a1) % 58.71/58.76 [90]~P1(x901)+E(f13(x901,f11(a28)),f11(x901)) % 58.71/58.76 [91]~P1(x911)+E(f13(f11(a28),x911),f11(x911)) % 58.71/58.76 [136]~P2(x1361,f30(a29,a31))+E(f12(x1361,f11(a29)),f13(a31,f10(x1361))) % 58.71/58.76 [137]~P2(x1371,f30(a29,a31))+E(f12(x1371,f11(a29)),f13(a31,f16(x1371))) % 58.71/58.76 [144]~P2(x1441,f30(a29,a31))+P3(a31,f12(x1441,f11(a29))) % 58.71/58.76 [97]~P9(x971)+~P7(x971,a3)+P8(f27(x971)) % 58.71/58.76 [98]~P4(x981)+P2(f4(x981),x981)+P8(f17(x981)) % 58.71/58.76 [102]P9(x1021)+~P7(x1021,a3)+~P8(f27(x1021)) % 58.71/58.76 [109]P8(x1091)+P2(f5(x1091),x1091)+~P7(x1091,a3) % 58.71/58.76 [165]~P1(x1651)+P2(x1651,f30(a29,a31))+~P5(x1651,a29,a31) % 58.71/58.76 [157]~P1(x1571)+P2(x1571,f30(a29,a31))+~P3(a31,f12(x1571,f11(a29))) % 58.71/58.76 [92]~P3(x921,x922)+~P1(x922)+~E(x921,a1) % 58.71/58.76 [95]~P3(x951,x952)+P1(x951)+~P1(x952) % 58.71/58.76 [96]~P7(x961,x962)+P4(x961)+~P4(x962) % 58.71/58.76 [94]P4(x941)+~P7(x942,a3)+~E(x941,f27(x942)) % 58.71/58.76 [103]~P1(x1032)+~P1(x1031)+E(f12(x1031,x1032),f12(x1032,x1031)) % 58.71/58.76 [104]~P1(x1042)+~P1(x1041)+E(f13(x1041,x1042),f13(x1042,x1041)) % 58.71/58.76 [107]~P1(x1072)+~P1(x1071)+P1(f12(x1071,x1072)) % 58.71/58.76 [108]~P1(x1082)+~P1(x1081)+P1(f13(x1081,x1082)) % 58.71/58.76 [115]~P1(x1151)+~P3(x1152,x1151)+P1(f15(x1151,x1152)) % 58.71/58.76 [128]~P1(x1282)+~P3(x1281,x1282)+E(f13(x1281,f15(x1282,x1281)),x1282) % 58.71/58.76 [87]~P1(x871)+E(x871,a28)+E(x871,f11(a28))+P6(f14(x871)) % 58.71/58.76 [93]~P1(x931)+P3(f14(x931),x931)+E(x931,a28)+E(x931,f11(a28)) % 58.71/58.76 [110]~P4(x1101)+~P10(x1101)+P2(f9(x1101),x1101)+P9(f17(x1101)) % 58.71/58.76 [120]~P4(x1201)+~P8(f4(x1201))+~P7(f4(x1201),a3)+P8(f17(x1201)) % 58.71/58.76 [99]~P1(x991)+~P3(x992,x991)+~P6(x992)+~E(x991,a28) % 58.71/58.76 [127]~P1(x1271)+~P1(x1272)+P5(x1272,x1272,x1271)+E(x1271,a1) % 58.71/58.76 [101]~P4(x1012)+P4(x1011)+~E(x1011,f17(x1012))+P2(f18(x1012),x1012) % 58.71/58.76 [105]~P1(x1051)+~P3(x1052,x1051)+~P6(x1052)+~E(x1051,f11(a28)) % 58.71/58.76 [111]~P4(x1112)+P4(x1111)+~E(x1111,f17(x1112))+~P7(f18(x1112),a3) % 58.71/58.76 [124]~P4(x1241)+~P4(x1242)+P7(x1241,x1242)+P2(f19(x1242,x1241),x1241) % 58.71/58.76 [131]~P8(x1311)+~P2(x1312,x1311)+~P7(x1311,a3)+~E(f6(x1311,x1312),a1) % 58.71/58.76 [133]~P8(x1331)+~P2(x1332,x1331)+~P7(x1331,a3)+P1(f6(x1331,x1332)) % 58.71/58.76 [140]~P4(x1401)+~P4(x1402)+P7(x1401,x1402)+~P2(f19(x1402,x1401),x1402) % 58.71/58.76 [142]~P1(x1421)+~P1(x1422)+P2(x1421,f30(a29,a31))+~E(f13(a31,x1422),f12(x1421,f11(a29))) % 58.71/58.76 [171]~P8(x1712)+~P2(x1711,x1712)+~P7(x1712,a3)+P7(f30(x1711,f6(x1712,x1711)),x1712) % 58.71/58.76 [122]~P4(x1222)+~P7(x1223,x1222)+P2(x1221,x1222)+~P2(x1221,x1223) % 58.71/58.76 [112]~P2(x1121,x1122)+P1(x1121)+~P7(x1123,a3)+~E(x1122,f27(x1123)) % 58.71/58.76 [125]P4(x1251)+~P7(x1253,a3)+~P7(x1252,a3)+~E(x1251,f25(x1252,x1253)) % 58.71/58.76 [126]P4(x1261)+~P7(x1263,a3)+~P7(x1262,a3)+~E(x1261,f26(x1262,x1263)) % 58.71/58.76 [132]~P2(x1323,x1322)+~P2(x1323,x1321)+~P7(x1322,a3)+~E(x1321,f27(x1322)) % 58.71/58.76 [145]~P1(x1453)+~P1(x1452)+~P1(x1451)+E(f12(f12(x1451,x1452),x1453),f12(x1451,f12(x1452,x1453))) % 58.71/58.76 [146]~P1(x1463)+~P1(x1462)+~P1(x1461)+E(f13(f13(x1461,x1462),x1463),f13(x1461,f13(x1462,x1463))) % 58.71/58.76 [166]~P1(x1663)+~P1(x1662)+~P1(x1661)+E(f12(f13(x1661,x1662),f13(x1661,x1663)),f13(x1661,f12(x1662,x1663))) % 58.71/58.76 [167]~P1(x1672)+~P1(x1673)+~P1(x1671)+E(f12(f13(x1671,x1672),f13(x1673,x1672)),f13(f12(x1671,x1673),x1672)) % 58.71/58.76 [129]~P4(x1291)+~P10(x1291)+~P9(f9(x1291))+~P7(f9(x1291),a3)+P9(f17(x1291)) % 58.71/58.76 [100]~P1(x1001)+~P1(x1002)+E(x1001,a1)+E(x1002,a1)+~E(f13(x1002,x1001),a1) % 58.71/58.76 [134]~P8(x1342)+~P8(x1341)+~P7(x1342,a3)+~P7(x1341,a3)+P8(f26(x1341,x1342)) % 58.71/58.76 [135]~P9(x1352)+~P9(x1351)+~P7(x1352,a3)+~P7(x1351,a3)+P9(f25(x1351,x1352)) % 58.71/58.76 [150]~P4(x1501)+P2(f7(x1502,x1501),x1501)+~P7(x1502,a3)+E(x1501,f27(x1502))+P1(f7(x1502,x1501)) % 58.71/58.76 [170]~P4(x1701)+P2(f7(x1702,x1701),x1701)+~P7(x1702,a3)+~P2(f7(x1702,x1701),x1702)+E(x1701,f27(x1702)) % 58.71/58.76 [159]~P1(x1591)+P8(x1592)+~P7(x1592,a3)+E(x1591,a1)+~P7(f30(f5(x1592),x1591),x1592) % 58.71/58.76 [106]~P1(x1061)+~P1(x1063)+P4(x1062)+E(x1061,a1)+~E(x1062,f30(x1063,x1061)) % 58.71/58.76 [117]~P4(x1172)+~P2(x1171,x1173)+P1(x1171)+P2(f18(x1172),x1172)+~E(x1173,f17(x1172)) % 58.71/58.76 [121]~P1(x1211)+P2(x1211,x1212)+P2(x1211,x1213)+~E(x1212,f27(x1213))+~P7(x1213,a3) % 58.71/58.76 [130]~P4(x1303)+~P2(x1301,x1302)+P1(x1301)+~E(x1302,f17(x1303))+~P7(f18(x1303),a3) % 58.71/58.76 [178]~P4(x1781)+~P2(x1782,x1783)+~E(x1783,f17(x1781))+P2(f18(x1781),x1781)+P2(x1782,f23(x1781,x1783,x1782)) % 58.71/58.76 [179]~P4(x1791)+~P2(x1793,x1792)+~E(x1792,f17(x1791))+P2(f18(x1791),x1791)+P2(f23(x1791,x1792,x1793),x1791) % 58.71/58.76 [181]~P4(x1812)+~P2(x1811,x1813)+~E(x1813,f17(x1812))+P2(x1811,f23(x1812,x1813,x1811))+~P7(f18(x1812),a3) % 58.71/58.76 [182]~P4(x1821)+~P2(x1823,x1822)+~E(x1822,f17(x1821))+P2(f23(x1821,x1822,x1823),x1821)+~P7(f18(x1821),a3) % 58.71/58.76 [138]~P2(x1381,x1382)+P1(x1381)+~P7(x1384,a3)+~P7(x1383,a3)+~E(x1382,f25(x1383,x1384)) % 58.71/58.76 [139]~P2(x1391,x1392)+P1(x1391)+~P7(x1394,a3)+~P7(x1393,a3)+~E(x1392,f26(x1393,x1394)) % 58.71/58.76 [147]~P2(x1471,x1473)+P2(x1471,x1472)+~P7(x1474,a3)+~P7(x1472,a3)+~E(x1473,f26(x1474,x1472)) % 58.71/58.76 [148]~P2(x1481,x1483)+P2(x1481,x1482)+~P7(x1484,a3)+~P7(x1482,a3)+~E(x1483,f26(x1482,x1484)) % 58.71/58.76 [155]~P4(x1551)+~P4(x1552)+P2(f18(x1552),x1552)+P2(f22(x1552,x1551),x1551)+E(x1551,f17(x1552))+P1(f22(x1552,x1551)) % 58.71/58.76 [162]~P4(x1621)+~P4(x1622)+P2(f22(x1622,x1621),x1621)+E(x1621,f17(x1622))+P1(f22(x1622,x1621))+~P7(f18(x1622),a3) % 58.71/58.76 [163]~P4(x1631)+~P4(x1632)+P2(f18(x1632),x1632)+P2(f22(x1632,x1631),x1631)+P2(f24(x1632,x1631),x1632)+E(x1631,f17(x1632)) % 58.71/58.76 [168]~P4(x1681)+~P4(x1682)+P2(f22(x1682,x1681),x1681)+P2(f24(x1682,x1681),x1682)+E(x1681,f17(x1682))+~P7(f18(x1682),a3) % 58.71/58.76 [172]~P4(x1721)+~P4(x1722)+P2(f18(x1722),x1722)+P2(f22(x1722,x1721),x1721)+P2(f22(x1722,x1721),f24(x1722,x1721))+E(x1721,f17(x1722)) % 58.71/58.76 [174]~P4(x1741)+~P4(x1742)+P2(f22(x1742,x1741),x1741)+P2(f22(x1742,x1741),f24(x1742,x1741))+E(x1741,f17(x1742))+~P7(f18(x1742),a3) % 58.71/58.76 [180]~P4(x1801)+P2(f7(x1802,x1801),x1802)+~P7(x1802,a3)+~P2(f7(x1802,x1801),x1801)+E(x1801,f27(x1802))+~P1(f7(x1802,x1801)) % 58.71/58.76 [177]~P1(x1771)+~P1(x1772)+~P1(x1773)+~P5(x1773,x1772,x1771)+P5(x1772,x1773,x1771)+E(x1771,a1) % 58.71/58.76 [116]~P1(x1162)+~P1(x1163)+~P1(x1161)+P3(x1161,x1162)+E(x1161,a1)+~E(f13(x1161,x1163),x1162) % 58.71/58.76 [189]~P4(x1891)+P2(f20(x1892,x1893,x1891),x1891)+~P7(x1893,a3)+~P7(x1892,a3)+E(x1891,f25(x1892,x1893))+P1(f20(x1892,x1893,x1891)) % 58.71/58.76 [190]~P4(x1901)+P2(f21(x1902,x1903,x1901),x1901)+~P7(x1903,a3)+~P7(x1902,a3)+E(x1901,f26(x1902,x1903))+P1(f21(x1902,x1903,x1901)) % 58.71/58.76 [191]~P4(x1911)+P2(f21(x1912,x1913,x1911),x1911)+P2(f21(x1912,x1913,x1911),x1913)+~P7(x1913,a3)+~P7(x1912,a3)+E(x1911,f26(x1912,x1913)) % 58.71/58.76 [192]~P4(x1921)+P2(f21(x1922,x1923,x1921),x1921)+P2(f21(x1922,x1923,x1921),x1922)+~P7(x1923,a3)+~P7(x1922,a3)+E(x1921,f26(x1922,x1923)) % 58.71/58.76 [175]~P1(x1753)+~P1(x1752)+~P1(x1751)+P5(x1752,x1753,x1751)+E(x1751,a1)+~P3(x1751,f12(x1752,f11(x1753))) % 58.71/58.76 [176]~P1(x1761)+~P1(x1763)+~P1(x1762)+~P5(x1762,x1763,x1761)+E(x1761,a1)+P3(x1761,f12(x1762,f11(x1763))) % 58.71/58.76 [123]~P1(x1231)+~P1(x1234)+~P2(x1232,x1233)+P1(x1232)+E(x1231,a1)+~E(x1233,f30(x1234,x1231)) % 58.71/58.76 [153]~P1(x1531)+~P2(x1531,x1534)+P2(x1531,x1532)+~P7(x1533,a3)+~P7(x1534,a3)+~E(x1532,f25(x1533,x1534)) % 58.71/58.76 [154]~P1(x1541)+~P2(x1541,x1543)+P2(x1541,x1542)+~P7(x1544,a3)+~P7(x1543,a3)+~E(x1542,f25(x1543,x1544)) % 58.71/58.76 [160]~P2(x1601,x1604)+P2(x1601,x1602)+P2(x1601,x1603)+~P7(x1602,a3)+~P7(x1603,a3)+~E(x1604,f25(x1603,x1602)) % 58.71/58.76 [161]~P1(x1611)+~P1(x1613)+~P2(x1612,x1614)+P5(x1612,x1613,x1611)+E(x1611,a1)+~E(x1614,f30(x1613,x1611)) % 58.71/58.76 [188]~P1(x1881)+~P1(x1883)+~P4(x1882)+P2(f8(x1883,x1881,x1882),x1882)+E(x1881,a1)+E(x1882,f30(x1883,x1881))+P1(f8(x1883,x1881,x1882)) % 58.71/58.76 [193]~P1(x1931)+~P1(x1933)+~P4(x1932)+P5(f8(x1933,x1931,x1932),x1933,x1931)+P2(f8(x1933,x1931,x1932),x1932)+E(x1931,a1)+E(x1932,f30(x1933,x1931)) % 58.71/58.76 [194]~P4(x1941)+P2(f20(x1942,x1943,x1941),x1941)+P2(f20(x1942,x1943,x1941),x1943)+P2(f20(x1942,x1943,x1941),x1942)+~P7(x1943,a3)+~P7(x1942,a3)+E(x1941,f25(x1942,x1943)) % 58.71/58.76 [195]~P4(x1951)+~P7(x1953,a3)+~P7(x1952,a3)+~P2(f20(x1952,x1953,x1951),x1951)+~P2(f20(x1952,x1953,x1951),x1953)+E(x1951,f25(x1952,x1953))+~P1(f20(x1952,x1953,x1951)) % 58.71/58.76 [196]~P4(x1961)+~P7(x1963,a3)+~P7(x1962,a3)+~P2(f20(x1962,x1963,x1961),x1961)+~P2(f20(x1962,x1963,x1961),x1962)+E(x1961,f25(x1962,x1963))+~P1(f20(x1962,x1963,x1961)) % 58.71/58.76 [149]~P1(x1491)+~P4(x1493)+~P2(x1491,x1494)+P2(x1491,x1492)+~P2(x1494,x1493)+~E(x1492,f17(x1493))+P2(f18(x1493),x1493) % 58.71/58.76 [158]~P1(x1581)+~P4(x1583)+~P2(x1581,x1584)+P2(x1581,x1582)+~P2(x1584,x1583)+~E(x1582,f17(x1583))+~P7(f18(x1583),a3) % 58.71/58.76 [169]~P1(x1691)+~P2(x1691,x1694)+~P2(x1691,x1693)+P2(x1691,x1692)+~P7(x1694,a3)+~P7(x1693,a3)+~E(x1692,f26(x1693,x1694)) % 58.71/58.76 [173]~P1(x1731)+~P1(x1734)+~P1(x1732)+~P5(x1732,x1734,x1731)+P2(x1732,x1733)+E(x1731,a1)+~E(x1733,f30(x1734,x1731)) % 58.71/58.76 [185]~P4(x1851)+~P4(x1852)+~P2(x1853,x1852)+P2(f18(x1852),x1852)+~P2(f22(x1852,x1851),x1853)+~P2(f22(x1852,x1851),x1851)+E(x1851,f17(x1852))+~P1(f22(x1852,x1851)) % 58.71/58.76 [186]~P4(x1861)+~P4(x1862)+~P2(x1863,x1862)+~P2(f22(x1862,x1861),x1863)+~P2(f22(x1862,x1861),x1861)+E(x1861,f17(x1862))+~P1(f22(x1862,x1861))+~P7(f18(x1862),a3) % 58.71/58.76 [197]~P1(x1971)+~P1(x1973)+~P4(x1972)+~P5(f8(x1973,x1971,x1972),x1973,x1971)+~P2(f8(x1973,x1971,x1972),x1972)+E(x1971,a1)+E(x1972,f30(x1973,x1971))+~P1(f8(x1973,x1971,x1972)) % 58.71/58.76 [198]~P4(x1981)+~P7(x1983,a3)+~P7(x1982,a3)+~P2(f21(x1982,x1983,x1981),x1981)+~P2(f21(x1982,x1983,x1981),x1983)+~P2(f21(x1982,x1983,x1981),x1982)+E(x1981,f26(x1982,x1983))+~P1(f21(x1982,x1983,x1981)) % 58.71/58.76 [187]~P1(x1873)+~P1(x1871)+~P1(x1872)+~P5(x1874,x1873,x1871)+~P5(x1872,x1874,x1871)+P5(x1872,x1873,x1871)+~P1(x1874)+E(x1871,a1) % 58.71/58.76 [183]~P1(x1831)+~P1(x1832)+~P1(x1834)+~P1(x1833)+P5(x1833,x1834,x1832)+~P5(x1833,x1834,f13(x1831,x1832))+E(x1831,a1)+E(x1832,a1) % 58.71/58.76 [184]~P1(x1841)+~P1(x1842)+~P1(x1844)+~P1(x1843)+P5(x1843,x1844,x1842)+~P5(x1843,x1844,f13(x1842,x1841))+E(x1841,a1)+E(x1842,a1) % 58.71/58.76 %EqnAxiom % 58.71/58.76 [1]E(x11,x11) % 58.71/58.76 [2]E(x22,x21)+~E(x21,x22) % 58.71/58.76 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.71/58.76 [4]~E(x41,x42)+E(f30(x41,x43),f30(x42,x43)) % 58.71/58.76 [5]~E(x51,x52)+E(f30(x53,x51),f30(x53,x52)) % 58.71/58.76 [6]~E(x61,x62)+E(f21(x61,x63,x64),f21(x62,x63,x64)) % 58.71/58.76 [7]~E(x71,x72)+E(f21(x73,x71,x74),f21(x73,x72,x74)) % 58.71/58.76 [8]~E(x81,x82)+E(f21(x83,x84,x81),f21(x83,x84,x82)) % 58.71/58.76 [9]~E(x91,x92)+E(f11(x91),f11(x92)) % 58.71/58.76 [10]~E(x101,x102)+E(f12(x101,x103),f12(x102,x103)) % 58.71/58.76 [11]~E(x111,x112)+E(f12(x113,x111),f12(x113,x112)) % 58.71/58.76 [12]~E(x121,x122)+E(f13(x121,x123),f13(x122,x123)) % 58.71/58.76 [13]~E(x131,x132)+E(f13(x133,x131),f13(x133,x132)) % 58.71/58.76 [14]~E(x141,x142)+E(f26(x141,x143),f26(x142,x143)) % 58.71/58.76 [15]~E(x151,x152)+E(f26(x153,x151),f26(x153,x152)) % 58.71/58.76 [16]~E(x161,x162)+E(f22(x161,x163),f22(x162,x163)) % 58.71/58.76 [17]~E(x171,x172)+E(f22(x173,x171),f22(x173,x172)) % 58.71/58.76 [18]~E(x181,x182)+E(f27(x181),f27(x182)) % 58.71/58.76 [19]~E(x191,x192)+E(f20(x191,x193,x194),f20(x192,x193,x194)) % 58.71/58.76 [20]~E(x201,x202)+E(f20(x203,x201,x204),f20(x203,x202,x204)) % 58.71/58.76 [21]~E(x211,x212)+E(f20(x213,x214,x211),f20(x213,x214,x212)) % 58.71/58.76 [22]~E(x221,x222)+E(f18(x221),f18(x222)) % 58.71/58.76 [23]~E(x231,x232)+E(f17(x231),f17(x232)) % 58.71/58.76 [24]~E(x241,x242)+E(f8(x241,x243,x244),f8(x242,x243,x244)) % 58.71/58.76 [25]~E(x251,x252)+E(f8(x253,x251,x254),f8(x253,x252,x254)) % 58.71/58.76 [26]~E(x261,x262)+E(f8(x263,x264,x261),f8(x263,x264,x262)) % 58.71/58.76 [27]~E(x271,x272)+E(f25(x271,x273),f25(x272,x273)) % 58.71/58.76 [28]~E(x281,x282)+E(f25(x283,x281),f25(x283,x282)) % 58.71/58.76 [29]~E(x291,x292)+E(f15(x291,x293),f15(x292,x293)) % 58.71/58.76 [30]~E(x301,x302)+E(f15(x303,x301),f15(x303,x302)) % 58.71/58.76 [31]~E(x311,x312)+E(f7(x311,x313),f7(x312,x313)) % 58.71/58.76 [32]~E(x321,x322)+E(f7(x323,x321),f7(x323,x322)) % 58.71/58.76 [33]~E(x331,x332)+E(f5(x331),f5(x332)) % 58.71/58.76 [34]~E(x341,x342)+E(f6(x341,x343),f6(x342,x343)) % 58.71/58.76 [35]~E(x351,x352)+E(f6(x353,x351),f6(x353,x352)) % 58.71/58.76 [36]~E(x361,x362)+E(f23(x361,x363,x364),f23(x362,x363,x364)) % 58.71/58.76 [37]~E(x371,x372)+E(f23(x373,x371,x374),f23(x373,x372,x374)) % 58.71/58.76 [38]~E(x381,x382)+E(f23(x383,x384,x381),f23(x383,x384,x382)) % 58.71/58.76 [39]~E(x391,x392)+E(f16(x391),f16(x392)) % 58.71/58.76 [40]~E(x401,x402)+E(f24(x401,x403),f24(x402,x403)) % 58.71/58.76 [41]~E(x411,x412)+E(f24(x413,x411),f24(x413,x412)) % 58.71/58.76 [42]~E(x421,x422)+E(f14(x421),f14(x422)) % 58.71/58.76 [43]~E(x431,x432)+E(f4(x431),f4(x432)) % 58.71/58.76 [44]~E(x441,x442)+E(f19(x441,x443),f19(x442,x443)) % 58.71/58.76 [45]~E(x451,x452)+E(f19(x453,x451),f19(x453,x452)) % 58.71/58.76 [46]~E(x461,x462)+E(f9(x461),f9(x462)) % 58.71/58.76 [47]~E(x471,x472)+E(f10(x471),f10(x472)) % 58.71/58.76 [48]~P1(x481)+P1(x482)+~E(x481,x482) % 58.71/58.76 [49]P2(x492,x493)+~E(x491,x492)+~P2(x491,x493) % 58.71/58.76 [50]P2(x503,x502)+~E(x501,x502)+~P2(x503,x501) % 58.71/58.76 [51]~P4(x511)+P4(x512)+~E(x511,x512) % 58.71/58.76 [52]P5(x522,x523,x524)+~E(x521,x522)+~P5(x521,x523,x524) % 58.71/58.76 [53]P5(x533,x532,x534)+~E(x531,x532)+~P5(x533,x531,x534) % 58.71/58.76 [54]P5(x543,x544,x542)+~E(x541,x542)+~P5(x543,x544,x541) % 58.71/58.76 [55]P7(x552,x553)+~E(x551,x552)+~P7(x551,x553) % 58.71/58.76 [56]P7(x563,x562)+~E(x561,x562)+~P7(x563,x561) % 58.71/58.76 [57]~P8(x571)+P8(x572)+~E(x571,x572) % 58.71/58.76 [58]~P6(x581)+P6(x582)+~E(x581,x582) % 58.71/58.76 [59]P3(x592,x593)+~E(x591,x592)+~P3(x591,x593) % 58.71/58.76 [60]P3(x603,x602)+~E(x601,x602)+~P3(x603,x601) % 58.71/58.76 [61]~P9(x611)+P9(x612)+~E(x611,x612) % 58.71/58.76 [62]~P10(x621)+P10(x622)+~E(x621,x622) % 58.71/58.76 % 58.71/58.76 %------------------------------------------- % 58.71/58.76 cnf(199,plain, % 58.71/58.76 (~P1(x1991)+~P3(a1,x1991)), % 58.71/58.76 inference(equality_inference,[],[92])). % 58.71/58.76 cnf(204,plain, % 58.71/58.76 (~P1(x2041)+~P1(x2042)+P4(f30(x2042,x2041))+E(x2041,a1)), % 58.71/58.76 inference(equality_inference,[],[106])). % 58.71/58.76 cnf(226,plain, % 58.71/58.76 (~P5(x2261,x2262,x2263)+~P1(x2263)+~P1(x2262)+P2(x2261,f30(x2262,x2263))+~P1(x2261)+E(x2263,a1)), % 58.71/58.76 inference(equality_inference,[],[173])). % 58.71/58.76 cnf(235,plain, % 58.71/58.76 (P3(a31,f13(a31,a2))), % 58.71/58.76 inference(scs_inference,[],[78,73,72,79,74,2,49,50,60])). % 58.71/58.76 cnf(241,plain, % 58.71/58.76 (~P1(f11(a32))+P1(f13(a31,a2))), % 58.71/58.76 inference(scs_inference,[],[69,78,73,72,71,76,79,74,68,2,49,50,60,122,48,95,107])). % 58.71/58.76 cnf(245,plain, % 58.71/58.76 (~E(a32,a33)), % 58.71/58.77 inference(scs_inference,[],[76,79,78,50,49])). % 58.71/58.77 cnf(347,plain, % 58.71/58.77 (E(f13(a1,f16(a33)),a1)), % 58.71/58.77 inference(scs_inference,[],[73,81,119])). % 58.71/58.77 cnf(348,plain, % 58.71/58.77 (E(a1,f13(a1,f16(a33)))), % 58.71/58.77 inference(scs_inference,[],[347,2])). % 58.71/58.77 cnf(383,plain, % 58.71/58.77 (E(f13(f11(a2),a1),a1)), % 58.71/58.77 inference(scs_inference,[],[69,82,80])). % 58.71/58.77 cnf(431,plain, % 58.71/58.77 (E(f12(a1,a33),a33)), % 58.71/58.77 inference(scs_inference,[],[73,83,114])). % 58.71/58.77 cnf(432,plain, % 58.71/58.77 (E(a33,f12(a1,a33))), % 58.71/58.77 inference(scs_inference,[],[431,2])). % 58.71/58.77 cnf(435,plain, % 58.71/58.77 (P1(f12(a1,a33))), % 58.71/58.77 inference(scs_inference,[],[75,431,245,68,2,3,52,48])). % 58.71/58.77 cnf(609,plain, % 58.71/58.77 (E(f13(a28,f11(a2)),f11(a2))), % 58.71/58.77 inference(scs_inference,[],[69,84,80])). % 58.71/58.77 cnf(610,plain, % 58.71/58.77 (E(f11(a2),f13(a28,f11(a2)))), % 58.71/58.77 inference(scs_inference,[],[609,2])). % 58.71/58.77 cnf(718,plain, % 58.71/58.77 (E(f13(a33,a28),a33)), % 58.71/58.77 inference(scs_inference,[],[73,86,114])). % 58.71/58.77 cnf(719,plain, % 58.71/58.77 (E(a33,f13(a33,a28))), % 58.71/58.77 inference(scs_inference,[],[718,2])). % 58.71/58.77 cnf(721,plain, % 58.71/58.77 (P1(f13(a33,a28))), % 58.71/58.77 inference(scs_inference,[],[718,245,68,2,3,48])). % 58.71/58.77 cnf(843,plain, % 58.71/58.77 (P1(f13(a31,a2))), % 58.71/58.77 inference(scs_inference,[],[67,241,80])). % 58.71/58.77 cnf(1288,plain, % 58.71/58.77 (E(f12(f11(f11(a2)),f11(a2)),a1)), % 58.71/58.77 inference(scs_inference,[],[69,88,80])). % 58.71/58.77 cnf(1289,plain, % 58.71/58.77 (E(a1,f12(f11(f11(a2)),f11(a2)))), % 58.71/58.77 inference(scs_inference,[],[1288,2])). % 58.71/58.77 cnf(1337,plain, % 58.71/58.77 (E(f12(a33,f11(a33)),a1)), % 58.71/58.77 inference(scs_inference,[],[73,89,114])). % 58.71/58.77 cnf(1569,plain, % 58.71/58.77 (E(f12(f11(f11(a2)),f11(a2)),f13(f11(a2),a1))), % 58.71/58.77 inference(scs_inference,[],[63,383,1289,92,3,2])). % 58.71/58.77 cnf(2085,plain, % 58.71/58.77 (E(f13(f11(a28),a33),f11(a33))), % 58.71/58.77 inference(scs_inference,[],[73,91,114])). % 58.71/58.77 cnf(2086,plain, % 58.71/58.77 (E(f11(a33),f13(f11(a28),a33))), % 58.71/58.77 inference(scs_inference,[],[2085,2])). % 58.71/58.77 cnf(2261,plain, % 58.71/58.77 (~P3(f13(f11(a2),a1),a33)), % 58.71/58.77 inference(scs_inference,[],[68,383,92])). % 58.71/58.77 cnf(2275,plain, % 58.71/58.77 (P5(f13(a33,a28),a29,a31)), % 58.71/58.77 inference(scs_inference,[],[73,719,152,49])). % 58.71/58.77 cnf(2279,plain, % 58.71/58.77 (P5(a33,a29,a31)), % 58.71/58.77 inference(scs_inference,[],[78,718,721,2275,165,49,52])). % 58.71/58.77 cnf(2402,plain, % 58.71/58.77 (P5(f12(a1,a33),a29,a31)), % 58.71/58.77 inference(scs_inference,[],[432,2279,52])). % 58.71/58.77 cnf(2404,plain, % 58.71/58.77 (P2(f12(a1,a33),f30(a29,a31))), % 58.71/58.77 inference(scs_inference,[],[432,435,2279,52,53,165])). % 58.71/58.77 cnf(2717,plain, % 58.71/58.77 (E(f26(f13(a31,a2),x27171),f26(f12(a33,f11(a32)),x27171))), % 58.71/58.77 inference(scs_inference,[],[72,14,2])). % 58.71/58.77 cnf(4161,plain, % 58.71/58.77 (~E(a31,a1)), % 58.71/58.77 inference(scs_inference,[],[1569,718,2261,77,60,59,2])). % 58.71/58.77 cnf(4169,plain, % 58.71/58.77 (P5(a32,a33,a31)), % 58.71/58.77 inference(scs_inference,[],[383,75,69,1569,718,2261,77,66,67,68,60,59,2,3,127,204,106,177])). % 58.71/58.77 cnf(4173,plain, % 58.71/58.77 (~E(f27(f30(a29,a31)),f30(a32,a31))), % 58.71/58.77 inference(scs_inference,[],[383,75,79,69,1569,718,2261,77,66,67,68,60,59,2,3,127,204,106,177,226,173])). % 58.71/58.77 cnf(4180,plain, % 58.71/58.77 (P5(a32,f13(a33,a28),a31)), % 58.71/58.77 inference(scs_inference,[],[719,4173,4169,2,53])). % 58.71/58.77 cnf(4360,plain, % 58.71/58.77 ($false), % 58.71/58.77 inference(scs_inference,[],[69,2717,4180,2404,2402,435,721,843,235,2275,65,2086,348,610,431,4161,79,78,1337,66,67,199,83,84,85,86,81,82,9,18,22,23,33,39,42,43,46,47,88,89,118,119,4,5,10,11,12,13,14,15,16,17,27,28,29,30,31,32,34,35,40,41,44,45,90,91,6,7,8,19,20,21,24,25,26,36,37,38,144,136,137,80,2,115,128,157,107,108,165,92,3,48,53,49,60,145,146,166,167,142,100,177,176,187]), % 58.71/58.77 ['proof']). % 58.71/58.77 % SZS output end Proof % 58.71/58.77 % Total time :58.060000s %------------------------------------------------------------------------------