%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM441+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 : n029.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:16 EDT 2024 % Result : Theorem 0.56s 0.72s % Output : CNFRefutation 0.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NUM441+6 : TPTP v8.2.0. Released v4.0.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n029.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sun Jun 23 01:43:39 EDT 2024 % 0.13/0.34 % CPUTime : % 0.54/0.59 start to proof:theBenchmark % 0.56/0.70 %------------------------------------------- % 0.56/0.70 % File :CSE---1.7 % 0.56/0.70 % Problem :theBenchmark % 0.56/0.70 % Transform :cnf % 0.56/0.70 % Format :tptp:raw % 0.56/0.70 % Command :java -jar mcs_scs.jar %d %s % 0.56/0.70 % 0.56/0.70 % Result :Theorem 0.020000s % 0.56/0.70 % Output :CNFRefutation 0.020000s % 0.56/0.70 %------------------------------------------- % 0.56/0.70 %------------------------------------------------------------------------------ % 0.56/0.70 % File : NUM441+6 : TPTP v8.2.0. Released v4.0.0. % 0.56/0.70 % Domain : Number Theory % 0.56/0.70 % Problem : Fuerstenberg's infinitude of primes 09_02, 05 expansion % 0.56/0.70 % Version : Especial. % 0.56/0.70 % English : % 0.56/0.70 % 0.56/0.70 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 0.56/0.70 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 0.56/0.70 % Source : [Pas08] % 0.56/0.70 % Names : fuerst_09_02.05 [Pas08] % 0.56/0.70 % 0.56/0.70 % Status : Theorem % 0.56/0.70 % Rating : 0.25 v8.1.0, 0.19 v7.5.0, 0.25 v7.4.0, 0.10 v7.3.0, 0.14 v7.1.0, 0.22 v7.0.0, 0.20 v6.4.0, 0.23 v6.3.0, 0.17 v6.2.0, 0.20 v6.1.0, 0.37 v6.0.0, 0.30 v5.5.0, 0.37 v5.4.0, 0.43 v5.3.0, 0.52 v5.2.0, 0.30 v5.1.0, 0.43 v5.0.0, 0.50 v4.1.0, 0.57 v4.0.1, 0.87 v4.0.0 % 0.56/0.70 % Syntax : Number of formulae : 41 ( 2 unt; 10 def) % 0.56/0.70 % Number of atoms : 304 ( 47 equ) % 0.56/0.70 % Maximal formula atoms : 64 ( 7 avg) % 0.56/0.70 % Number of connectives : 287 ( 24 ~; 13 |; 153 &) % 0.56/0.70 % ( 31 <=>; 66 =>; 0 <=; 0 <~>) % 0.56/0.70 % Maximal formula depth : 33 ( 8 avg) % 0.56/0.70 % Maximal term depth : 3 ( 1 avg) % 0.56/0.70 % Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty) % 0.56/0.70 % Number of functors : 13 ( 13 usr; 5 con; 0-2 aty) % 0.56/0.70 % Number of variables : 120 ( 107 !; 13 ?) % 0.56/0.70 % SPC : FOF_THM_RFO_SEQ % 0.56/0.70 % 0.56/0.70 % Comments : Problem generated by the SAD system [VLP07] % 0.56/0.70 %------------------------------------------------------------------------------ % 0.56/0.70 fof(mIntegers,axiom, % 0.56/0.70 ! [W0] : % 0.56/0.70 ( aInteger0(W0) % 0.56/0.70 => $true ) ). % 0.56/0.70 % 0.56/0.70 fof(mIntZero,axiom, % 0.56/0.70 aInteger0(sz00) ). % 0.56/0.70 % 0.56/0.70 fof(mIntOne,axiom, % 0.56/0.70 aInteger0(sz10) ). % 0.56/0.70 % 0.56/0.70 fof(mIntNeg,axiom, % 0.56/0.70 ! [W0] : % 0.56/0.70 ( aInteger0(W0) % 0.56/0.70 => aInteger0(smndt0(W0)) ) ). % 0.56/0.70 % 0.56/0.70 fof(mIntPlus,axiom, % 0.56/0.70 ! [W0,W1] : % 0.56/0.70 ( ( aInteger0(W0) % 0.56/0.70 & aInteger0(W1) ) % 0.56/0.70 => aInteger0(sdtpldt0(W0,W1)) ) ). % 0.56/0.70 % 0.56/0.71 fof(mIntMult,axiom, % 0.56/0.71 ! [W0,W1] : % 0.56/0.71 ( ( aInteger0(W0) % 0.56/0.71 & aInteger0(W1) ) % 0.56/0.71 => aInteger0(sdtasdt0(W0,W1)) ) ). % 0.56/0.71 % 0.56/0.71 fof(mAddAsso,axiom, % 0.56/0.71 ! [W0,W1,W2] : % 0.56/0.71 ( ( aInteger0(W0) % 0.56/0.71 & aInteger0(W1) % 0.56/0.71 & aInteger0(W2) ) % 0.56/0.71 => sdtpldt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtpldt0(W0,W1),W2) ) ). % 0.56/0.71 % 0.56/0.71 fof(mAddComm,axiom, % 0.56/0.71 ! [W0,W1] : % 0.56/0.71 ( ( aInteger0(W0) % 0.56/0.71 & aInteger0(W1) ) % 0.56/0.71 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 0.56/0.71 % 0.56/0.71 fof(mAddZero,axiom, % 0.56/0.71 ! [W0] : % 0.56/0.71 ( aInteger0(W0) % 0.56/0.71 => ( sdtpldt0(W0,sz00) = W0 % 0.56/0.71 & W0 = sdtpldt0(sz00,W0) ) ) ). % 0.56/0.71 % 0.56/0.71 fof(mAddNeg,axiom, % 0.56/0.71 ! [W0] : % 0.56/0.71 ( aInteger0(W0) % 0.56/0.71 => ( sdtpldt0(W0,smndt0(W0)) = sz00 % 0.56/0.71 & sz00 = sdtpldt0(smndt0(W0),W0) ) ) ). % 0.56/0.71 % 0.56/0.71 fof(mMulAsso,axiom, % 0.56/0.71 ! [W0,W1,W2] : % 0.56/0.71 ( ( aInteger0(W0) % 0.56/0.71 & aInteger0(W1) % 0.56/0.71 & aInteger0(W2) ) % 0.56/0.71 => sdtasdt0(W0,sdtasdt0(W1,W2)) = sdtasdt0(sdtasdt0(W0,W1),W2) ) ). % 0.56/0.71 % 0.56/0.71 fof(mMulComm,axiom, % 0.56/0.71 ! [W0,W1] : % 0.56/0.71 ( ( aInteger0(W0) % 0.56/0.71 & aInteger0(W1) ) % 0.56/0.71 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 0.56/0.71 % 0.56/0.71 fof(mMulOne,axiom, % 0.56/0.71 ! [W0] : % 0.56/0.71 ( aInteger0(W0) % 0.56/0.71 => ( sdtasdt0(W0,sz10) = W0 % 0.56/0.71 & W0 = sdtasdt0(sz10,W0) ) ) ). % 0.56/0.71 % 0.56/0.71 fof(mDistrib,axiom, % 0.56/0.71 ! [W0,W1,W2] : % 0.56/0.71 ( ( aInteger0(W0) % 0.56/0.71 & aInteger0(W1) % 0.56/0.71 & aInteger0(W2) ) % 0.56/0.71 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 0.56/0.71 & sdtasdt0(sdtpldt0(W0,W1),W2) = sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W1,W2)) ) ) ). % 0.56/0.71 % 0.56/0.71 fof(mMulZero,axiom, % 0.56/0.71 ! [W0] : % 0.56/0.71 ( aInteger0(W0) % 0.56/0.71 => ( sdtasdt0(W0,sz00) = sz00 % 0.56/0.71 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 0.56/0.71 % 0.56/0.71 fof(mMulMinOne,axiom, % 0.56/0.71 ! [W0] : % 0.56/0.71 ( aInteger0(W0) % 0.56/0.71 => ( sdtasdt0(smndt0(sz10),W0) = smndt0(W0) % 0.56/0.71 & smndt0(W0) = sdtasdt0(W0,smndt0(sz10)) ) ) ). % 0.56/0.71 % 0.56/0.71 fof(mZeroDiv,axiom, % 0.56/0.71 ! [W0,W1] : % 0.56/0.71 ( ( aInteger0(W0) % 0.56/0.71 & aInteger0(W1) ) % 0.56/0.71 => ( sdtasdt0(W0,W1) = sz00 % 0.56/0.71 => ( W0 = sz00 % 0.56/0.71 | W1 = sz00 ) ) ) ). % 0.56/0.71 % 0.56/0.71 fof(mDivisor,definition, % 0.56/0.71 ! [W0] : % 0.56/0.71 ( aInteger0(W0) % 0.56/0.71 => ! [W1] : % 0.56/0.71 ( aDivisorOf0(W1,W0) % 0.56/0.71 <=> ( aInteger0(W1) % 0.56/0.71 & W1 != sz00 % 0.56/0.71 & ? [W2] : % 0.56/0.71 ( aInteger0(W2) % 0.56/0.71 & sdtasdt0(W1,W2) = W0 ) ) ) ) ). % 0.56/0.71 % 0.56/0.71 fof(mEquMod,definition, % 0.56/0.71 ! [W0,W1,W2] : % 0.56/0.71 ( ( aInteger0(W0) % 0.56/0.71 & aInteger0(W1) % 0.56/0.71 & aInteger0(W2) % 0.56/0.71 & W2 != sz00 ) % 0.56/0.71 => ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 0.56/0.71 <=> aDivisorOf0(W2,sdtpldt0(W0,smndt0(W1))) ) ) ). % 0.56/0.71 % 0.56/0.71 fof(mEquModRef,axiom, % 0.56/0.71 ! [W0,W1] : % 0.56/0.71 ( ( aInteger0(W0) % 0.56/0.71 & aInteger0(W1) % 0.56/0.71 & W1 != sz00 ) % 0.56/0.71 => sdteqdtlpzmzozddtrp0(W0,W0,W1) ) ). % 0.56/0.71 % 0.56/0.71 fof(mEquModSym,axiom, % 0.56/0.71 ! [W0,W1,W2] : % 0.56/0.71 ( ( aInteger0(W0) % 0.56/0.71 & aInteger0(W1) % 0.56/0.71 & aInteger0(W2) % 0.56/0.71 & W2 != sz00 ) % 0.56/0.71 => ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 0.56/0.71 => sdteqdtlpzmzozddtrp0(W1,W0,W2) ) ) ). % 0.56/0.71 % 0.56/0.71 fof(mEquModTrn,axiom, % 0.56/0.71 ! [W0,W1,W2,W3] : % 0.56/0.71 ( ( aInteger0(W0) % 0.56/0.71 & aInteger0(W1) % 0.56/0.71 & aInteger0(W2) % 0.56/0.71 & W2 != sz00 % 0.56/0.71 & aInteger0(W3) ) % 0.56/0.71 => ( ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 0.56/0.71 & sdteqdtlpzmzozddtrp0(W1,W3,W2) ) % 0.56/0.71 => sdteqdtlpzmzozddtrp0(W0,W3,W2) ) ) ). % 0.56/0.71 % 0.56/0.71 fof(mEquModMul,axiom, % 0.56/0.71 ! [W0,W1,W2,W3] : % 0.56/0.71 ( ( aInteger0(W0) % 0.56/0.71 & aInteger0(W1) % 0.56/0.71 & aInteger0(W2) % 0.56/0.71 & W2 != sz00 % 0.56/0.71 & aInteger0(W3) % 0.56/0.71 & W3 != sz00 ) % 0.56/0.71 => ( sdteqdtlpzmzozddtrp0(W0,W1,sdtasdt0(W2,W3)) % 0.56/0.71 => ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 0.56/0.71 & sdteqdtlpzmzozddtrp0(W0,W1,W3) ) ) ) ). % 0.56/0.71 % 0.56/0.71 fof(mPrime,axiom, % 0.56/0.71 ! [W0] : % 0.56/0.71 ( ( aInteger0(W0) % 0.56/0.71 & W0 != sz00 ) % 0.56/0.71 => ( isPrime0(W0) % 0.56/0.71 => $true ) ) ). % 0.56/0.71 % 0.56/0.71 fof(mPrimeDivisor,axiom, % 0.56/0.71 ! [W0] : % 0.56/0.71 ( aInteger0(W0) % 0.56/0.71 => ( ? [W1] : % 0.56/0.71 ( aDivisorOf0(W1,W0) % 0.56/0.71 & isPrime0(W1) ) % 0.56/0.71 <=> ( W0 != sz10 % 0.56/0.71 & W0 != smndt0(sz10) ) ) ) ). % 0.56/0.71 % 0.56/0.71 fof(mSets,axiom, % 0.56/0.71 ! [W0] : % 0.56/0.71 ( aSet0(W0) % 0.56/0.71 => $true ) ). % 0.56/0.71 % 0.56/0.71 fof(mElements,axiom, % 0.56/0.71 ! [W0] : % 0.56/0.71 ( aSet0(W0) % 0.56/0.71 => ! [W1] : % 0.56/0.71 ( aElementOf0(W1,W0) % 0.56/0.71 => $true ) ) ). % 0.56/0.71 % 0.56/0.71 fof(mSubset,definition, % 0.56/0.71 ! [W0] : % 0.56/0.71 ( aSet0(W0) % 0.56/0.71 => ! [W1] : % 0.56/0.71 ( aSubsetOf0(W1,W0) % 0.56/0.71 <=> ( aSet0(W1) % 0.56/0.71 & ! [W2] : % 0.56/0.71 ( aElementOf0(W2,W1) % 0.56/0.71 => aElementOf0(W2,W0) ) ) ) ) ). % 0.56/0.71 % 0.56/0.71 fof(mFinSet,axiom, % 0.56/0.71 ! [W0] : % 0.56/0.71 ( aSet0(W0) % 0.56/0.71 => ( isFinite0(W0) % 0.56/0.71 => $true ) ) ). % 0.56/0.71 % 0.56/0.71 fof(mUnion,definition, % 0.56/0.71 ! [W0,W1] : % 0.56/0.71 ( ( aSubsetOf0(W0,cS1395) % 0.56/0.71 & aSubsetOf0(W1,cS1395) ) % 0.56/0.71 => ! [W2] : % 0.56/0.71 ( W2 = sdtbsmnsldt0(W0,W1) % 0.56/0.71 <=> ( aSet0(W2) % 0.56/0.71 & ! [W3] : % 0.56/0.71 ( aElementOf0(W3,W2) % 0.56/0.71 <=> ( aInteger0(W3) % 0.56/0.71 & ( aElementOf0(W3,W0) % 0.56/0.71 | aElementOf0(W3,W1) ) ) ) ) ) ) ). % 0.56/0.71 % 0.56/0.71 fof(mIntersection,definition, % 0.56/0.71 ! [W0,W1] : % 0.56/0.71 ( ( aSubsetOf0(W0,cS1395) % 0.56/0.71 & aSubsetOf0(W1,cS1395) ) % 0.56/0.71 => ! [W2] : % 0.56/0.71 ( W2 = sdtslmnbsdt0(W0,W1) % 0.56/0.71 <=> ( aSet0(W2) % 0.56/0.71 & ! [W3] : % 0.56/0.71 ( aElementOf0(W3,W2) % 0.56/0.71 <=> ( aInteger0(W3) % 0.56/0.71 & aElementOf0(W3,W0) % 0.56/0.71 & aElementOf0(W3,W1) ) ) ) ) ) ). % 0.56/0.71 % 0.56/0.71 fof(mUnionSet,definition, % 0.56/0.71 ! [W0] : % 0.56/0.71 ( ( aSet0(W0) % 0.56/0.71 & ! [W1] : % 0.56/0.71 ( aElementOf0(W1,W0) % 0.56/0.71 => aSubsetOf0(W1,cS1395) ) ) % 0.56/0.71 => ! [W1] : % 0.56/0.71 ( W1 = sbsmnsldt0(W0) % 0.56/0.71 <=> ( aSet0(W1) % 0.56/0.71 & ! [W2] : % 0.56/0.71 ( aElementOf0(W2,W1) % 0.56/0.71 <=> ( aInteger0(W2) % 0.56/0.71 & ? [W3] : % 0.56/0.71 ( aElementOf0(W3,W0) % 0.56/0.71 & aElementOf0(W2,W3) ) ) ) ) ) ) ). % 0.56/0.71 % 0.56/0.71 fof(mComplement,definition, % 0.56/0.71 ! [W0] : % 0.56/0.71 ( aSubsetOf0(W0,cS1395) % 0.56/0.71 => ! [W1] : % 0.56/0.71 ( W1 = stldt0(W0) % 0.56/0.71 <=> ( aSet0(W1) % 0.56/0.71 & ! [W2] : % 0.56/0.71 ( aElementOf0(W2,W1) % 0.56/0.71 <=> ( aInteger0(W2) % 0.56/0.71 & ~ aElementOf0(W2,W0) ) ) ) ) ) ). % 0.56/0.71 % 0.56/0.71 fof(mArSeq,definition, % 0.56/0.71 ! [W0,W1] : % 0.56/0.71 ( ( aInteger0(W0) % 0.56/0.71 & aInteger0(W1) % 0.56/0.71 & W1 != sz00 ) % 0.56/0.71 => ! [W2] : % 0.56/0.71 ( W2 = szAzrzSzezqlpdtcmdtrp0(W0,W1) % 0.56/0.71 <=> ( aSet0(W2) % 0.56/0.71 & ! [W3] : % 0.56/0.71 ( aElementOf0(W3,W2) % 0.56/0.72 <=> ( aInteger0(W3) % 0.56/0.72 & sdteqdtlpzmzozddtrp0(W3,W0,W1) ) ) ) ) ) ). % 0.56/0.72 % 0.56/0.72 fof(mOpen,definition, % 0.56/0.72 ! [W0] : % 0.56/0.72 ( aSubsetOf0(W0,cS1395) % 0.56/0.72 => ( isOpen0(W0) % 0.56/0.72 <=> ! [W1] : % 0.56/0.72 ( aElementOf0(W1,W0) % 0.56/0.72 => ? [W2] : % 0.56/0.72 ( aInteger0(W2) % 0.56/0.72 & W2 != sz00 % 0.56/0.72 & aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W1,W2),W0) ) ) ) ) ). % 0.56/0.72 % 0.56/0.72 fof(mClosed,definition, % 0.56/0.72 ! [W0] : % 0.56/0.72 ( aSubsetOf0(W0,cS1395) % 0.56/0.72 => ( isClosed0(W0) % 0.56/0.72 <=> isOpen0(stldt0(W0)) ) ) ). % 0.56/0.72 % 0.56/0.72 fof(mUnionOpen,axiom, % 0.56/0.72 ! [W0] : % 0.56/0.72 ( ( aSet0(W0) % 0.56/0.72 & ! [W1] : % 0.56/0.72 ( aElementOf0(W1,W0) % 0.56/0.72 => ( aSubsetOf0(W1,cS1395) % 0.56/0.72 & isOpen0(W1) ) ) ) % 0.56/0.72 => isOpen0(sbsmnsldt0(W0)) ) ). % 0.56/0.72 % 0.56/0.72 fof(mInterOpen,axiom, % 0.56/0.72 ! [W0,W1] : % 0.56/0.72 ( ( aSubsetOf0(W0,cS1395) % 0.56/0.72 & aSubsetOf0(W1,cS1395) % 0.56/0.72 & isOpen0(W0) % 0.56/0.72 & isOpen0(W1) ) % 0.56/0.72 => isOpen0(sdtslmnbsdt0(W0,W1)) ) ). % 0.56/0.72 % 0.56/0.72 fof(m__1826,hypothesis, % 0.56/0.72 ( aSet0(cS1395) % 0.56/0.72 & ! [W0] : % 0.56/0.72 ( aElementOf0(W0,cS1395) % 0.56/0.72 <=> aInteger0(W0) ) % 0.56/0.72 & aSet0(xA) % 0.56/0.72 & ! [W0] : % 0.56/0.72 ( aElementOf0(W0,xA) % 0.56/0.72 => aElementOf0(W0,cS1395) ) % 0.56/0.72 & aSubsetOf0(xA,cS1395) % 0.56/0.72 & aSet0(cS1395) % 0.56/0.72 & ! [W0] : % 0.56/0.72 ( aElementOf0(W0,cS1395) % 0.56/0.72 <=> aInteger0(W0) ) % 0.56/0.72 & aSet0(xB) % 0.56/0.72 & ! [W0] : % 0.56/0.72 ( aElementOf0(W0,xB) % 0.56/0.72 => aElementOf0(W0,cS1395) ) % 0.56/0.72 & aSubsetOf0(xB,cS1395) % 0.56/0.72 & aSet0(stldt0(xA)) % 0.56/0.72 & ! [W0] : % 0.56/0.72 ( aElementOf0(W0,stldt0(xA)) % 0.56/0.72 <=> ( aInteger0(W0) % 0.56/0.72 & ~ aElementOf0(W0,xA) ) ) % 0.56/0.72 & ! [W0] : % 0.56/0.72 ( aElementOf0(W0,stldt0(xA)) % 0.56/0.72 => ? [W1] : % 0.56/0.72 ( aInteger0(W1) % 0.56/0.72 & W1 != sz00 % 0.56/0.72 & aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)) % 0.56/0.72 & ! [W2] : % 0.56/0.72 ( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) % 0.56/0.72 => ( aInteger0(W2) % 0.56/0.72 & ? [W3] : % 0.56/0.72 ( aInteger0(W3) % 0.56/0.72 & sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0)) ) % 0.56/0.72 & aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))) % 0.56/0.72 & sdteqdtlpzmzozddtrp0(W2,W0,W1) ) ) % 0.56/0.72 & ( ( aInteger0(W2) % 0.56/0.72 & ( ? [W3] : % 0.56/0.72 ( aInteger0(W3) % 0.56/0.72 & sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0)) ) % 0.56/0.72 | aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))) % 0.56/0.72 | sdteqdtlpzmzozddtrp0(W2,W0,W1) ) ) % 0.56/0.72 => aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) ) ) % 0.56/0.72 & ! [W2] : % 0.56/0.72 ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) % 0.56/0.72 => aElementOf0(W2,stldt0(xA)) ) % 0.56/0.72 & aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(xA)) ) ) % 0.56/0.72 & isOpen0(stldt0(xA)) % 0.56/0.72 & isClosed0(xA) % 0.56/0.72 & aSet0(stldt0(xB)) % 0.56/0.72 & ! [W0] : % 0.56/0.72 ( aElementOf0(W0,stldt0(xB)) % 0.56/0.72 <=> ( aInteger0(W0) % 0.56/0.72 & ~ aElementOf0(W0,xB) ) ) % 0.56/0.72 & ! [W0] : % 0.56/0.72 ( aElementOf0(W0,stldt0(xB)) % 0.56/0.72 => ? [W1] : % 0.56/0.72 ( aInteger0(W1) % 0.56/0.72 & W1 != sz00 % 0.56/0.72 & aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)) % 0.56/0.72 & ! [W2] : % 0.56/0.72 ( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) % 0.56/0.72 => ( aInteger0(W2) % 0.56/0.72 & ? [W3] : % 0.56/0.72 ( aInteger0(W3) % 0.56/0.72 & sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0)) ) % 0.56/0.72 & aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))) % 0.56/0.72 & sdteqdtlpzmzozddtrp0(W2,W0,W1) ) ) % 0.56/0.72 & ( ( aInteger0(W2) % 0.56/0.72 & ( ? [W3] : % 0.56/0.72 ( aInteger0(W3) % 0.56/0.72 & sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0)) ) % 0.56/0.72 | aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))) % 0.56/0.72 | sdteqdtlpzmzozddtrp0(W2,W0,W1) ) ) % 0.56/0.72 => aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) ) ) % 0.56/0.72 & ! [W2] : % 0.56/0.72 ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) % 0.56/0.72 => aElementOf0(W2,stldt0(xB)) ) % 0.56/0.72 & aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(xB)) ) ) % 0.56/0.72 & isOpen0(stldt0(xB)) % 0.56/0.72 & isClosed0(xB) ) ). % 0.56/0.72 % 0.56/0.72 fof(m__1883,hypothesis, % 0.56/0.72 ( aSet0(stldt0(xA)) % 0.56/0.72 & ! [W0] : % 0.56/0.72 ( aElementOf0(W0,stldt0(xA)) % 0.56/0.72 <=> ( aInteger0(W0) % 0.56/0.72 & ~ aElementOf0(W0,xA) ) ) % 0.56/0.72 & aSet0(cS1395) % 0.56/0.72 & ! [W0] : % 0.56/0.72 ( aElementOf0(W0,cS1395) % 0.56/0.72 <=> aInteger0(W0) ) % 0.56/0.72 & ! [W0] : % 0.56/0.72 ( aElementOf0(W0,stldt0(xA)) % 0.56/0.72 => aElementOf0(W0,cS1395) ) % 0.56/0.72 & aSubsetOf0(stldt0(xA),cS1395) % 0.56/0.72 & aSet0(stldt0(xB)) % 0.56/0.72 & ! [W0] : % 0.56/0.72 ( aElementOf0(W0,stldt0(xB)) % 0.56/0.72 <=> ( aInteger0(W0) % 0.56/0.72 & ~ aElementOf0(W0,xB) ) ) % 0.56/0.72 & aSet0(cS1395) % 0.56/0.72 & ! [W0] : % 0.56/0.72 ( aElementOf0(W0,cS1395) % 0.56/0.72 <=> aInteger0(W0) ) % 0.56/0.72 & ! [W0] : % 0.56/0.72 ( aElementOf0(W0,stldt0(xB)) % 0.56/0.72 => aElementOf0(W0,cS1395) ) % 0.56/0.72 & aSubsetOf0(stldt0(xB),cS1395) % 0.56/0.72 & aSet0(sdtbsmnsldt0(xA,xB)) % 0.56/0.72 & ! [W0] : % 0.56/0.72 ( aElementOf0(W0,sdtbsmnsldt0(xA,xB)) % 0.56/0.72 <=> ( aInteger0(W0) % 0.56/0.72 & ( aElementOf0(W0,xA) % 0.56/0.72 | aElementOf0(W0,xB) ) ) ) % 0.56/0.72 & aSet0(stldt0(sdtbsmnsldt0(xA,xB))) % 0.56/0.72 & ! [W0] : % 0.56/0.72 ( aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB))) % 0.56/0.72 <=> ( aInteger0(W0) % 0.56/0.72 & ~ aElementOf0(W0,sdtbsmnsldt0(xA,xB)) ) ) % 0.56/0.72 & ! [W0] : % 0.56/0.72 ( aElementOf0(W0,stldt0(xA)) % 0.56/0.72 <=> ( aInteger0(W0) % 0.56/0.72 & ~ aElementOf0(W0,xA) ) ) % 0.56/0.72 & ! [W0] : % 0.56/0.72 ( aElementOf0(W0,stldt0(xB)) % 0.56/0.72 <=> ( aInteger0(W0) % 0.56/0.72 & ~ aElementOf0(W0,xB) ) ) % 0.56/0.72 & ! [W0] : % 0.56/0.72 ( aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB))) % 0.56/0.72 <=> ( aInteger0(W0) % 0.56/0.72 & aElementOf0(W0,stldt0(xA)) % 0.56/0.72 & aElementOf0(W0,stldt0(xB)) ) ) % 0.56/0.72 & stldt0(sdtbsmnsldt0(xA,xB)) = sdtslmnbsdt0(stldt0(xA),stldt0(xB)) ) ). % 0.56/0.72 % 0.56/0.72 fof(m__,conjecture, % 0.56/0.72 ( ( aSet0(sdtbsmnsldt0(xA,xB)) % 0.56/0.72 & ! [W0] : % 0.56/0.72 ( aElementOf0(W0,sdtbsmnsldt0(xA,xB)) % 0.56/0.72 <=> ( aInteger0(W0) % 0.56/0.72 & ( aElementOf0(W0,xA) % 0.56/0.72 | aElementOf0(W0,xB) ) ) ) ) % 0.56/0.72 => ( ( ( aSet0(stldt0(sdtbsmnsldt0(xA,xB))) % 0.56/0.72 & ! [W0] : % 0.56/0.72 ( aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB))) % 0.56/0.72 <=> ( aInteger0(W0) % 0.56/0.72 & ~ aElementOf0(W0,sdtbsmnsldt0(xA,xB)) ) ) ) % 0.56/0.72 => ( ! [W0] : % 0.56/0.72 ( aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB))) % 0.56/0.72 => ? [W1] : % 0.56/0.72 ( aInteger0(W1) % 0.56/0.72 & W1 != sz00 % 0.56/0.72 & ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)) % 0.56/0.72 & ! [W2] : % 0.56/0.72 ( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) % 0.56/0.72 => ( aInteger0(W2) % 0.56/0.72 & ? [W3] : % 0.56/0.72 ( aInteger0(W3) % 0.56/0.72 & sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0)) ) % 0.56/0.72 & aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))) % 0.56/0.72 & sdteqdtlpzmzozddtrp0(W2,W0,W1) ) ) % 0.56/0.72 & ( ( aInteger0(W2) % 0.56/0.72 & ( ? [W3] : % 0.56/0.72 ( aInteger0(W3) % 0.56/0.72 & sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0)) ) % 0.56/0.72 | aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))) % 0.56/0.72 | sdteqdtlpzmzozddtrp0(W2,W0,W1) ) ) % 0.56/0.72 => aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) ) ) ) % 0.56/0.72 => ( ! [W2] : % 0.56/0.72 ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) % 0.56/0.72 => aElementOf0(W2,stldt0(sdtbsmnsldt0(xA,xB))) ) % 0.56/0.72 | aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sdtbsmnsldt0(xA,xB))) ) ) ) ) % 0.56/0.72 | isOpen0(stldt0(sdtbsmnsldt0(xA,xB))) ) ) % 0.56/0.72 | isClosed0(sdtbsmnsldt0(xA,xB)) ) ) ). % 0.56/0.72 % 0.56/0.72 %------------------------------------------------------------------------------ % 0.56/0.72 %------------------------------------------- % 0.56/0.72 % Proof found % 0.56/0.72 % SZS status Theorem for theBenchmark % 0.56/0.72 % SZS output start Proof % 0.56/0.72 %ClaNum:281(EqnAxiom:67) % 0.56/0.72 %VarNum:1114(SingletonVarNum:337) % 0.56/0.72 %MaxLitNum:8 % 0.56/0.72 %MaxfuncDepth:2 % 0.56/0.72 %SharedTerms:34 % 0.56/0.72 %goalClause: 89 92 93 94 95 131 162 165 169 171 184 189 197 200 204 211 216 217 224 227 228 236 237 244 % 0.56/0.72 %singleGoalClaCount:5 % 0.56/0.72 [68]P1(a1) % 0.56/0.72 [69]P1(a31) % 0.56/0.72 [73]P4(a2) % 0.56/0.72 [74]P4(a32) % 0.56/0.72 [75]P4(a34) % 0.56/0.72 [76]P5(a32) % 0.56/0.72 [77]P5(a34) % 0.56/0.72 [84]P6(a32,a2) % 0.56/0.72 [85]P6(a34,a2) % 0.56/0.72 [79]P4(f3(a32)) % 0.56/0.72 [81]P4(f3(a34)) % 0.56/0.72 [82]P7(f3(a32)) % 0.56/0.72 [83]P7(f3(a34)) % 0.56/0.72 [86]P6(f3(a32),a2) % 0.56/0.72 [87]P6(f3(a34),a2) % 0.56/0.72 [89]P4(f4(a32,a34)) % 0.56/0.72 [94]~P5(f4(a32,a34)) % 0.56/0.72 [90]E(f28(f3(a32),f3(a34)),f3(f4(a32,a34))) % 0.56/0.72 [92]P4(f3(f4(a32,a34))) % 0.56/0.72 [93]P2(a5,f3(f4(a32,a34))) % 0.56/0.72 [95]~P7(f3(f4(a32,a34))) % 0.56/0.72 [102]~P1(x1021)+P2(x1021,a2) % 0.56/0.72 [111]P1(x1111)+~P2(x1111,a2) % 0.56/0.72 [124]~P2(x1241,a32)+P2(x1241,a2) % 0.56/0.72 [125]~P2(x1251,a34)+P2(x1251,a2) % 0.56/0.72 [96]~P1(x961)+P1(f30(x961)) % 0.56/0.72 [97]~P1(x971)+E(f15(a1,x971),a1) % 0.56/0.72 [98]~P1(x981)+E(f15(x981,a1),a1) % 0.56/0.72 [103]~P1(x1031)+E(f29(a1,x1031),x1031) % 0.56/0.72 [104]~P1(x1041)+E(f15(a31,x1041),x1041) % 0.56/0.72 [105]~P1(x1051)+E(f29(x1051,a1),x1051) % 0.56/0.72 [106]~P1(x1061)+E(f15(x1061,a31),x1061) % 0.56/0.72 [118]P1(x1181)+~P2(x1181,f3(a32)) % 0.56/0.72 [121]P1(x1211)+~P2(x1211,f3(a34)) % 0.56/0.72 [129]~P2(x1291,f3(a32))+~E(f6(x1291),a1) % 0.56/0.72 [130]~P2(x1301,f3(a34))+~E(f12(x1301),a1) % 0.56/0.72 [138]~P2(x1381,f3(a32))+P1(f6(x1381)) % 0.56/0.72 [139]~P2(x1391,f3(a34))+P1(f12(x1391)) % 0.56/0.72 [144]P2(x1441,a2)+~P2(x1441,f3(a32)) % 0.56/0.72 [145]P2(x1451,a2)+~P2(x1451,f3(a34)) % 0.56/0.72 [157]~P2(x1571,a32)+~P2(x1571,f3(a32)) % 0.56/0.72 [160]~P2(x1601,a34)+~P2(x1601,f3(a34)) % 0.56/0.72 [165]P1(x1651)+~P2(x1651,f4(a32,a34)) % 0.56/0.72 [112]~P1(x1121)+E(f29(f30(x1121),x1121),a1) % 0.56/0.72 [113]~P1(x1131)+E(f29(x1131,f30(x1131)),a1) % 0.56/0.72 [114]~P1(x1141)+E(f15(x1141,f30(a31)),f30(x1141)) % 0.56/0.72 [115]~P1(x1151)+E(f15(f30(a31),x1151),f30(x1151)) % 0.56/0.72 [180]~P2(x1801,f3(a32))+P4(f33(x1801,f6(x1801))) % 0.56/0.72 [181]~P2(x1811,f3(a34))+P4(f33(x1811,f12(x1811))) % 0.56/0.72 [191]~P2(x1911,f3(a32))+P6(f33(x1911,f6(x1911)),f3(a32)) % 0.56/0.72 [192]~P2(x1921,f3(a34))+P6(f33(x1921,f12(x1921)),f3(a34)) % 0.56/0.72 [200]P1(x2001)+~P2(x2001,f3(f4(a32,a34))) % 0.56/0.72 [213]P2(x2131,f3(a32))+~P2(x2131,f3(f4(a32,a34))) % 0.56/0.72 [214]P2(x2141,f3(a34))+~P2(x2141,f3(f4(a32,a34))) % 0.56/0.72 [244]~P2(x2441,f4(a32,a34))+~P2(x2441,f3(f4(a32,a34))) % 0.56/0.72 [131]~P1(x1311)+E(x1311,a1)+P4(f33(a5,x1311)) % 0.56/0.72 [134]~P1(x1341)+P2(x1341,a32)+P2(x1341,f3(a32)) % 0.56/0.72 [137]~P1(x1371)+P2(x1371,a34)+P2(x1371,f3(a34)) % 0.56/0.72 [140]~P5(x1401)+~P6(x1401,a2)+P7(f3(x1401)) % 0.56/0.72 [141]~P4(x1411)+P2(f7(x1411),x1411)+P7(f20(x1411)) % 0.56/0.72 [147]P5(x1471)+~P6(x1471,a2)+~P7(f3(x1471)) % 0.56/0.72 [154]P7(x1541)+P2(f8(x1541),x1541)+~P6(x1541,a2) % 0.56/0.72 [162]~P1(x1621)+E(x1621,a1)+P2(f17(x1621),f33(a5,x1621)) % 0.56/0.72 [169]~P1(x1691)+~P2(x1691,a32)+P2(x1691,f4(a32,a34)) % 0.56/0.72 [171]~P1(x1711)+~P2(x1711,a34)+P2(x1711,f4(a32,a34)) % 0.56/0.72 [189]P2(x1891,a34)+P2(x1891,a32)+~P2(x1891,f4(a32,a34)) % 0.56/0.72 [204]~P1(x2041)+P2(x2041,f4(a32,a34))+P2(x2041,f3(f4(a32,a34))) % 0.56/0.72 [216]~P1(x2161)+E(x2161,a1)+~P2(f17(x2161),f3(f4(a32,a34))) % 0.56/0.72 [237]~P1(x2371)+E(x2371,a1)+~P6(f33(a5,x2371),f3(f4(a32,a34))) % 0.56/0.72 [122]~P3(x1221,x1222)+~P1(x1222)+~E(x1221,a1) % 0.56/0.72 [127]~P3(x1271,x1272)+P1(x1271)+~P1(x1272) % 0.56/0.72 [128]~P6(x1281,x1282)+P4(x1281)+~P4(x1282) % 0.56/0.72 [126]P4(x1261)+~P6(x1262,a2)+~E(x1261,f3(x1262)) % 0.56/0.72 [148]~P1(x1482)+~P1(x1481)+E(f29(x1481,x1482),f29(x1482,x1481)) % 0.56/0.72 [149]~P1(x1492)+~P1(x1491)+E(f15(x1491,x1492),f15(x1492,x1491)) % 0.56/0.72 [152]~P1(x1522)+~P1(x1521)+P1(f29(x1521,x1522)) % 0.56/0.72 [153]~P1(x1532)+~P1(x1531)+P1(f15(x1531,x1532)) % 0.56/0.72 [166]~P1(x1661)+~P3(x1662,x1661)+P1(f18(x1661,x1662)) % 0.56/0.72 [183]~P1(x1832)+~P3(x1831,x1832)+E(f15(x1831,f18(x1832,x1831)),x1832) % 0.56/0.72 [218]P1(x2181)+~P2(x2182,f3(a32))+~P2(x2181,f33(x2182,f6(x2182))) % 0.56/0.72 [219]P1(x2191)+~P2(x2192,f3(a34))+~P2(x2191,f33(x2192,f12(x2192))) % 0.56/0.72 [231]P2(x2311,f3(a32))+~P2(x2312,f3(a32))+~P2(x2311,f33(x2312,f6(x2312))) % 0.56/0.72 [232]P2(x2321,f3(a34))+~P2(x2322,f3(a34))+~P2(x2321,f33(x2322,f12(x2322))) % 0.56/0.72 [238]~P2(x2381,f3(a32))+~P2(x2382,f33(x2381,f6(x2381)))+P1(f13(x2381,x2382)) % 0.56/0.72 [239]~P2(x2391,f3(a34))+~P2(x2392,f33(x2391,f12(x2391)))+P1(f14(x2391,x2392)) % 0.56/0.72 [251]~P2(x2511,f3(a32))+~P2(x2512,f33(x2511,f6(x2511)))+P3(f6(x2511),f29(x2512,f30(x2511))) % 0.56/0.72 [252]~P2(x2521,f3(a34))+~P2(x2522,f33(x2521,f12(x2521)))+P3(f12(x2521),f29(x2522,f30(x2521))) % 0.56/0.72 [253]P9(x2531,x2532,f6(x2532))+~P2(x2532,f3(a32))+~P2(x2531,f33(x2532,f6(x2532))) % 0.56/0.72 [254]P9(x2541,x2542,f12(x2542))+~P2(x2542,f3(a34))+~P2(x2541,f33(x2542,f12(x2542))) % 0.56/0.72 [255]~P2(x2551,f3(a32))+~P2(x2552,f33(x2551,f6(x2551)))+E(f15(f6(x2551),f13(x2551,x2552)),f29(x2552,f30(x2551))) % 0.56/0.72 [256]~P2(x2561,f3(a34))+~P2(x2562,f33(x2561,f12(x2561)))+E(f15(f12(x2561),f14(x2561,x2562)),f29(x2562,f30(x2561))) % 0.56/0.72 [107]~P1(x1071)+E(x1071,a31)+E(x1071,f30(a31))+P8(f16(x1071)) % 0.56/0.72 [123]~P1(x1231)+P3(f16(x1231),x1231)+E(x1231,a31)+E(x1231,f30(a31)) % 0.56/0.72 [173]~P4(x1731)+~P7(f7(x1731))+~P6(f7(x1731),a2)+P7(f20(x1731)) % 0.56/0.72 [226]~P1(x2261)+~P2(x2261,f3(a32))+~P2(x2261,f3(a34))+P2(x2261,f3(f4(a32,a34))) % 0.56/0.72 [142]~P1(x1421)+~P3(x1422,x1421)+~P8(x1422)+~E(x1421,a31) % 0.56/0.72 [182]~P1(x1821)+~P1(x1822)+P9(x1822,x1822,x1821)+E(x1821,a1) % 0.56/0.72 [146]~P4(x1462)+P4(x1461)+~E(x1461,f20(x1462))+P2(f21(x1462),x1462) % 0.56/0.72 [150]~P1(x1501)+~P3(x1502,x1501)+~P8(x1502)+~E(x1501,f30(a31)) % 0.56/0.72 [161]~P4(x1612)+P4(x1611)+~E(x1611,f20(x1612))+~P6(f21(x1612),a2) % 0.56/0.72 [177]~P4(x1771)+~P4(x1772)+P6(x1771,x1772)+P2(f22(x1772,x1771),x1771) % 0.56/0.72 [184]~P1(x1841)+P1(x1842)+E(x1841,a1)+~P2(x1842,f33(a5,x1841)) % 0.56/0.72 [186]~P7(x1861)+~P2(x1862,x1861)+~P6(x1861,a2)+~E(f9(x1861,x1862),a1) % 0.56/0.72 [190]~P7(x1901)+~P2(x1902,x1901)+~P6(x1901,a2)+P1(f9(x1901,x1902)) % 0.56/0.72 [196]~P4(x1961)+~P4(x1962)+P6(x1961,x1962)+~P2(f22(x1962,x1961),x1962) % 0.56/0.72 [197]~P1(x1971)+E(x1971,a1)+~P2(x1972,f33(a5,x1971))+P1(f19(x1971,x1972)) % 0.56/0.72 [224]~P1(x2241)+P9(x2242,a5,x2241)+E(x2241,a1)+~P2(x2242,f33(a5,x2241)) % 0.56/0.72 [217]~P1(x2171)+E(x2171,a1)+~P2(x2172,f33(a5,x2171))+P3(x2171,f29(x2172,f30(a5))) % 0.56/0.72 [227]~P1(x2271)+E(x2271,a1)+~P2(x2272,f33(a5,x2271))+E(f15(x2271,f19(x2271,x2272)),f29(x2272,f30(a5))) % 0.56/0.72 [240]~P7(x2402)+~P2(x2401,x2402)+~P6(x2402,a2)+P6(f33(x2401,f9(x2402,x2401)),x2402) % 0.56/0.72 [257]~P1(x2571)+~P2(x2572,f3(a32))+~P3(f6(x2572),f29(x2571,f30(x2572)))+P2(x2571,f33(x2572,f6(x2572))) % 0.56/0.72 [258]~P1(x2581)+~P2(x2582,f3(a34))+~P3(f12(x2582),f29(x2581,f30(x2582)))+P2(x2581,f33(x2582,f12(x2582))) % 0.56/0.72 [261]~P1(x2611)+~P9(x2611,x2612,f6(x2612))+~P2(x2612,f3(a32))+P2(x2611,f33(x2612,f6(x2612))) % 0.56/0.72 [262]~P1(x2621)+~P9(x2621,x2622,f12(x2622))+~P2(x2622,f3(a34))+P2(x2621,f33(x2622,f12(x2622))) % 0.56/0.72 [175]~P4(x1752)+~P6(x1753,x1752)+P2(x1751,x1752)+~P2(x1751,x1753) % 0.56/0.72 [163]~P2(x1631,x1632)+P1(x1631)+~P6(x1633,a2)+~E(x1632,f3(x1633)) % 0.56/0.72 [178]P4(x1781)+~P6(x1783,a2)+~P6(x1782,a2)+~E(x1781,f4(x1782,x1783)) % 0.56/0.72 [179]P4(x1791)+~P6(x1793,a2)+~P6(x1792,a2)+~E(x1791,f28(x1792,x1793)) % 0.56/0.72 [187]~P2(x1873,x1872)+~P2(x1873,x1871)+~P6(x1872,a2)+~E(x1871,f3(x1872)) % 0.56/0.72 [201]~P1(x2013)+~P1(x2012)+~P1(x2011)+E(f29(f29(x2011,x2012),x2013),f29(x2011,f29(x2012,x2013))) % 0.56/0.72 [202]~P1(x2023)+~P1(x2022)+~P1(x2021)+E(f15(f15(x2021,x2022),x2023),f15(x2021,f15(x2022,x2023))) % 0.56/0.72 [229]~P1(x2293)+~P1(x2292)+~P1(x2291)+E(f29(f15(x2291,x2292),f15(x2291,x2293)),f15(x2291,f29(x2292,x2293))) % 0.56/0.72 [230]~P1(x2302)+~P1(x2303)+~P1(x2301)+E(f29(f15(x2301,x2302),f15(x2303,x2302)),f15(f29(x2301,x2303),x2302)) % 0.56/0.72 [143]~P1(x1431)+~P1(x1432)+E(x1431,a1)+E(x1432,a1)+~E(f15(x1432,x1431),a1) % 0.56/0.72 [193]~P7(x1932)+~P7(x1931)+~P6(x1932,a2)+~P6(x1931,a2)+P7(f28(x1931,x1932)) % 0.56/0.72 [208]~P4(x2081)+P2(f10(x2082,x2081),x2081)+~P6(x2082,a2)+E(x2081,f3(x2082))+P1(f10(x2082,x2081)) % 0.56/0.72 [235]~P4(x2351)+P2(f10(x2352,x2351),x2351)+~P6(x2352,a2)+~P2(f10(x2352,x2351),x2352)+E(x2351,f3(x2352)) % 0.56/0.72 [236]~P1(x2361)+~P1(x2362)+~P9(x2362,a5,x2361)+E(x2361,a1)+P2(x2362,f33(a5,x2361)) % 0.56/0.72 [220]~P1(x2201)+P7(x2202)+~P6(x2202,a2)+E(x2201,a1)+~P6(f33(f8(x2202),x2201),x2202) % 0.56/0.72 [228]~P1(x2282)+~P1(x2281)+E(x2281,a1)+P2(x2282,f33(a5,x2281))+~P3(x2281,f29(x2282,f30(a5))) % 0.56/0.72 [151]~P1(x1511)+~P1(x1513)+P4(x1512)+E(x1511,a1)+~E(x1512,f33(x1513,x1511)) % 0.56/0.72 [172]~P4(x1722)+~P2(x1721,x1723)+P1(x1721)+P2(f21(x1722),x1722)+~E(x1723,f20(x1722)) % 0.56/0.72 [174]~P1(x1741)+P2(x1741,x1742)+P2(x1741,x1743)+~E(x1742,f3(x1743))+~P6(x1743,a2) % 0.56/0.73 [185]~P4(x1853)+~P2(x1851,x1852)+P1(x1851)+~E(x1852,f20(x1853))+~P6(f21(x1853),a2) % 0.56/0.73 [259]~P4(x2591)+~P2(x2592,x2593)+~E(x2593,f20(x2591))+P2(f21(x2591),x2591)+P2(x2592,f26(x2591,x2593,x2592)) % 0.56/0.73 [260]~P4(x2601)+~P2(x2603,x2602)+~E(x2602,f20(x2601))+P2(f21(x2601),x2601)+P2(f26(x2601,x2602,x2603),x2601) % 0.56/0.73 [264]~P4(x2642)+~P2(x2641,x2643)+~E(x2643,f20(x2642))+P2(x2641,f26(x2642,x2643,x2641))+~P6(f21(x2642),a2) % 0.56/0.73 [265]~P4(x2651)+~P2(x2653,x2652)+~E(x2652,f20(x2651))+P2(f26(x2651,x2652,x2653),x2651)+~P6(f21(x2651),a2) % 0.56/0.73 [246]~P1(x2461)+~P1(x2463)+~P2(x2462,f3(a32))+P2(x2461,f33(x2462,f6(x2462)))+~E(f15(f6(x2462),x2463),f29(x2461,f30(x2462))) % 0.56/0.73 [247]~P1(x2471)+~P1(x2473)+~P2(x2472,f3(a34))+P2(x2471,f33(x2472,f12(x2472)))+~E(f15(f12(x2472),x2473),f29(x2471,f30(x2472))) % 0.56/0.73 [194]~P2(x1941,x1942)+P1(x1941)+~P6(x1944,a2)+~P6(x1943,a2)+~E(x1942,f4(x1943,x1944)) % 0.56/0.73 [195]~P2(x1951,x1952)+P1(x1951)+~P6(x1954,a2)+~P6(x1953,a2)+~E(x1952,f28(x1953,x1954)) % 0.56/0.73 [205]~P2(x2051,x2053)+P2(x2051,x2052)+~P6(x2054,a2)+~P6(x2052,a2)+~E(x2053,f28(x2054,x2052)) % 0.56/0.73 [206]~P2(x2061,x2063)+P2(x2061,x2062)+~P6(x2064,a2)+~P6(x2062,a2)+~E(x2063,f28(x2062,x2064)) % 0.56/0.73 [212]~P4(x2121)+~P4(x2122)+P2(f21(x2122),x2122)+P2(f25(x2122,x2121),x2121)+E(x2121,f20(x2122))+P1(f25(x2122,x2121)) % 0.56/0.73 [223]~P4(x2231)+~P4(x2232)+P2(f25(x2232,x2231),x2231)+E(x2231,f20(x2232))+P1(f25(x2232,x2231))+~P6(f21(x2232),a2) % 0.56/0.73 [225]~P4(x2251)+~P4(x2252)+P2(f21(x2252),x2252)+P2(f25(x2252,x2251),x2251)+P2(f27(x2252,x2251),x2252)+E(x2251,f20(x2252)) % 0.56/0.73 [233]~P4(x2331)+~P4(x2332)+P2(f25(x2332,x2331),x2331)+P2(f27(x2332,x2331),x2332)+E(x2331,f20(x2332))+~P6(f21(x2332),a2) % 0.56/0.73 [241]~P4(x2411)+~P4(x2412)+P2(f21(x2412),x2412)+P2(f25(x2412,x2411),x2411)+P2(f25(x2412,x2411),f27(x2412,x2411))+E(x2411,f20(x2412)) % 0.56/0.73 [245]~P4(x2451)+~P4(x2452)+P2(f25(x2452,x2451),x2451)+P2(f25(x2452,x2451),f27(x2452,x2451))+E(x2451,f20(x2452))+~P6(f21(x2452),a2) % 0.56/0.73 [263]~P4(x2631)+P2(f10(x2632,x2631),x2632)+~P6(x2632,a2)+~P2(f10(x2632,x2631),x2631)+E(x2631,f3(x2632))+~P1(f10(x2632,x2631)) % 0.56/0.73 [250]~P1(x2501)+~P1(x2502)+~P1(x2503)+~P9(x2503,x2502,x2501)+P9(x2502,x2503,x2501)+E(x2501,a1) % 0.56/0.73 [167]~P1(x1672)+~P1(x1673)+~P1(x1671)+P3(x1671,x1672)+E(x1671,a1)+~E(f15(x1671,x1673),x1672) % 0.56/0.73 [272]~P4(x2721)+P2(f23(x2722,x2723,x2721),x2721)+~P6(x2723,a2)+~P6(x2722,a2)+E(x2721,f4(x2722,x2723))+P1(f23(x2722,x2723,x2721)) % 0.56/0.73 [273]~P4(x2731)+P2(f24(x2732,x2733,x2731),x2731)+~P6(x2733,a2)+~P6(x2732,a2)+E(x2731,f28(x2732,x2733))+P1(f24(x2732,x2733,x2731)) % 0.56/0.73 [274]~P4(x2741)+P2(f24(x2742,x2743,x2741),x2741)+P2(f24(x2742,x2743,x2741),x2743)+~P6(x2743,a2)+~P6(x2742,a2)+E(x2741,f28(x2742,x2743)) % 0.56/0.73 [275]~P4(x2751)+P2(f24(x2752,x2753,x2751),x2751)+P2(f24(x2752,x2753,x2751),x2752)+~P6(x2753,a2)+~P6(x2752,a2)+E(x2751,f28(x2752,x2753)) % 0.56/0.73 [211]~P1(x2112)+~P1(x2111)+~P1(x2113)+E(x2111,a1)+P2(x2112,f33(a5,x2111))+~E(f15(x2111,x2113),f29(x2112,f30(a5))) % 0.56/0.73 [248]~P1(x2483)+~P1(x2482)+~P1(x2481)+P9(x2482,x2483,x2481)+E(x2481,a1)+~P3(x2481,f29(x2482,f30(x2483))) % 0.56/0.73 [249]~P1(x2491)+~P1(x2493)+~P1(x2492)+~P9(x2492,x2493,x2491)+E(x2491,a1)+P3(x2491,f29(x2492,f30(x2493))) % 0.56/0.73 [176]~P1(x1761)+~P1(x1764)+~P2(x1762,x1763)+P1(x1762)+E(x1761,a1)+~E(x1763,f33(x1764,x1761)) % 0.56/0.73 [209]~P1(x2091)+~P2(x2091,x2094)+P2(x2091,x2092)+~P6(x2093,a2)+~P6(x2094,a2)+~E(x2092,f4(x2093,x2094)) % 0.56/0.73 [210]~P1(x2101)+~P2(x2101,x2103)+P2(x2101,x2102)+~P6(x2104,a2)+~P6(x2103,a2)+~E(x2102,f4(x2103,x2104)) % 0.56/0.73 [221]~P2(x2211,x2214)+P2(x2211,x2212)+P2(x2211,x2213)+~P6(x2212,a2)+~P6(x2213,a2)+~E(x2214,f4(x2213,x2212)) % 0.56/0.73 [222]~P1(x2221)+~P1(x2223)+~P2(x2222,x2224)+P9(x2222,x2223,x2221)+E(x2221,a1)+~E(x2224,f33(x2223,x2221)) % 0.56/0.73 [271]~P1(x2711)+~P1(x2713)+~P4(x2712)+P2(f11(x2713,x2711,x2712),x2712)+E(x2711,a1)+E(x2712,f33(x2713,x2711))+P1(f11(x2713,x2711,x2712)) % 0.56/0.73 [276]~P1(x2761)+~P1(x2763)+~P4(x2762)+P9(f11(x2763,x2761,x2762),x2763,x2761)+P2(f11(x2763,x2761,x2762),x2762)+E(x2761,a1)+E(x2762,f33(x2763,x2761)) % 0.56/0.73 [277]~P4(x2771)+P2(f23(x2772,x2773,x2771),x2771)+P2(f23(x2772,x2773,x2771),x2773)+P2(f23(x2772,x2773,x2771),x2772)+~P6(x2773,a2)+~P6(x2772,a2)+E(x2771,f4(x2772,x2773)) % 0.56/0.73 [278]~P4(x2781)+~P6(x2783,a2)+~P6(x2782,a2)+~P2(f23(x2782,x2783,x2781),x2781)+~P2(f23(x2782,x2783,x2781),x2783)+E(x2781,f4(x2782,x2783))+~P1(f23(x2782,x2783,x2781)) % 0.56/0.73 [279]~P4(x2791)+~P6(x2793,a2)+~P6(x2792,a2)+~P2(f23(x2792,x2793,x2791),x2791)+~P2(f23(x2792,x2793,x2791),x2792)+E(x2791,f4(x2792,x2793))+~P1(f23(x2792,x2793,x2791)) % 0.56/0.73 [207]~P1(x2071)+~P4(x2073)+~P2(x2071,x2074)+P2(x2071,x2072)+~P2(x2074,x2073)+~E(x2072,f20(x2073))+P2(f21(x2073),x2073) % 0.56/0.73 [215]~P1(x2151)+~P4(x2153)+~P2(x2151,x2154)+P2(x2151,x2152)+~P2(x2154,x2153)+~E(x2152,f20(x2153))+~P6(f21(x2153),a2) % 0.56/0.73 [234]~P1(x2341)+~P2(x2341,x2344)+~P2(x2341,x2343)+P2(x2341,x2342)+~P6(x2344,a2)+~P6(x2343,a2)+~E(x2342,f28(x2343,x2344)) % 0.56/0.73 [242]~P1(x2421)+~P1(x2424)+~P1(x2422)+~P9(x2422,x2424,x2421)+P2(x2422,x2423)+E(x2421,a1)+~E(x2423,f33(x2424,x2421)) % 0.56/0.73 [268]~P4(x2681)+~P4(x2682)+~P2(x2683,x2682)+P2(f21(x2682),x2682)+~P2(f25(x2682,x2681),x2683)+~P2(f25(x2682,x2681),x2681)+E(x2681,f20(x2682))+~P1(f25(x2682,x2681)) % 0.56/0.73 [269]~P4(x2691)+~P4(x2692)+~P2(x2693,x2692)+~P2(f25(x2692,x2691),x2693)+~P2(f25(x2692,x2691),x2691)+E(x2691,f20(x2692))+~P1(f25(x2692,x2691))+~P6(f21(x2692),a2) % 0.56/0.73 [280]~P1(x2801)+~P1(x2803)+~P4(x2802)+~P9(f11(x2803,x2801,x2802),x2803,x2801)+~P2(f11(x2803,x2801,x2802),x2802)+E(x2801,a1)+E(x2802,f33(x2803,x2801))+~P1(f11(x2803,x2801,x2802)) % 0.56/0.73 [281]~P4(x2811)+~P6(x2813,a2)+~P6(x2812,a2)+~P2(f24(x2812,x2813,x2811),x2811)+~P2(f24(x2812,x2813,x2811),x2813)+~P2(f24(x2812,x2813,x2811),x2812)+E(x2811,f28(x2812,x2813))+~P1(f24(x2812,x2813,x2811)) % 0.56/0.73 [270]~P1(x2703)+~P1(x2701)+~P1(x2702)+~P9(x2704,x2703,x2701)+~P9(x2702,x2704,x2701)+P9(x2702,x2703,x2701)+~P1(x2704)+E(x2701,a1) % 0.56/0.73 [266]~P1(x2661)+~P1(x2662)+~P1(x2664)+~P1(x2663)+P9(x2663,x2664,x2662)+~P9(x2663,x2664,f15(x2661,x2662))+E(x2661,a1)+E(x2662,a1) % 0.56/0.73 [267]~P1(x2671)+~P1(x2672)+~P1(x2674)+~P1(x2673)+P9(x2673,x2674,x2672)+~P9(x2673,x2674,f15(x2672,x2671))+E(x2671,a1)+E(x2672,a1) % 0.56/0.73 %EqnAxiom % 0.56/0.73 [1]E(x11,x11) % 0.56/0.73 [2]E(x22,x21)+~E(x21,x22) % 0.56/0.73 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.56/0.73 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 0.56/0.73 [5]~E(x51,x52)+E(f24(x51,x53,x54),f24(x52,x53,x54)) % 0.56/0.73 [6]~E(x61,x62)+E(f24(x63,x61,x64),f24(x63,x62,x64)) % 0.56/0.73 [7]~E(x71,x72)+E(f24(x73,x74,x71),f24(x73,x74,x72)) % 0.56/0.73 [8]~E(x81,x82)+E(f12(x81),f12(x82)) % 0.56/0.73 [9]~E(x91,x92)+E(f29(x91,x93),f29(x92,x93)) % 0.56/0.73 [10]~E(x101,x102)+E(f29(x103,x101),f29(x103,x102)) % 0.56/0.73 [11]~E(x111,x112)+E(f30(x111),f30(x112)) % 0.56/0.73 [12]~E(x121,x122)+E(f28(x121,x123),f28(x122,x123)) % 0.56/0.73 [13]~E(x131,x132)+E(f28(x133,x131),f28(x133,x132)) % 0.56/0.73 [14]~E(x141,x142)+E(f11(x141,x143,x144),f11(x142,x143,x144)) % 0.56/0.73 [15]~E(x151,x152)+E(f11(x153,x151,x154),f11(x153,x152,x154)) % 0.56/0.73 [16]~E(x161,x162)+E(f11(x163,x164,x161),f11(x163,x164,x162)) % 0.56/0.73 [17]~E(x171,x172)+E(f27(x171,x173),f27(x172,x173)) % 0.56/0.73 [18]~E(x181,x182)+E(f27(x183,x181),f27(x183,x182)) % 0.56/0.73 [19]~E(x191,x192)+E(f4(x191,x193),f4(x192,x193)) % 0.56/0.73 [20]~E(x201,x202)+E(f4(x203,x201),f4(x203,x202)) % 0.56/0.73 [21]~E(x211,x212)+E(f26(x211,x213,x214),f26(x212,x213,x214)) % 0.56/0.73 [22]~E(x221,x222)+E(f26(x223,x221,x224),f26(x223,x222,x224)) % 0.56/0.73 [23]~E(x231,x232)+E(f26(x233,x234,x231),f26(x233,x234,x232)) % 0.56/0.73 [24]~E(x241,x242)+E(f25(x241,x243),f25(x242,x243)) % 0.56/0.73 [25]~E(x251,x252)+E(f25(x253,x251),f25(x253,x252)) % 0.56/0.73 [26]~E(x261,x262)+E(f33(x261,x263),f33(x262,x263)) % 0.56/0.73 [27]~E(x271,x272)+E(f33(x273,x271),f33(x273,x272)) % 0.56/0.73 [28]~E(x281,x282)+E(f13(x281,x283),f13(x282,x283)) % 0.56/0.73 [29]~E(x291,x292)+E(f13(x293,x291),f13(x293,x292)) % 0.56/0.73 [30]~E(x301,x302)+E(f20(x301),f20(x302)) % 0.56/0.73 [31]~E(x311,x312)+E(f23(x311,x313,x314),f23(x312,x313,x314)) % 0.56/0.73 [32]~E(x321,x322)+E(f23(x323,x321,x324),f23(x323,x322,x324)) % 0.56/0.73 [33]~E(x331,x332)+E(f23(x333,x334,x331),f23(x333,x334,x332)) % 0.56/0.73 [34]~E(x341,x342)+E(f15(x341,x343),f15(x342,x343)) % 0.56/0.73 [35]~E(x351,x352)+E(f15(x353,x351),f15(x353,x352)) % 0.56/0.73 [36]~E(x361,x362)+E(f7(x361),f7(x362)) % 0.56/0.73 [37]~E(x371,x372)+E(f6(x371),f6(x372)) % 0.56/0.73 [38]~E(x381,x382)+E(f10(x381,x383),f10(x382,x383)) % 0.56/0.73 [39]~E(x391,x392)+E(f10(x393,x391),f10(x393,x392)) % 0.56/0.73 [40]~E(x401,x402)+E(f21(x401),f21(x402)) % 0.56/0.73 [41]~E(x411,x412)+E(f9(x411,x413),f9(x412,x413)) % 0.56/0.73 [42]~E(x421,x422)+E(f9(x423,x421),f9(x423,x422)) % 0.56/0.73 [43]~E(x431,x432)+E(f14(x431,x433),f14(x432,x433)) % 0.56/0.73 [44]~E(x441,x442)+E(f14(x443,x441),f14(x443,x442)) % 0.56/0.73 [45]~E(x451,x452)+E(f19(x451,x453),f19(x452,x453)) % 0.56/0.73 [46]~E(x461,x462)+E(f19(x463,x461),f19(x463,x462)) % 0.56/0.73 [47]~E(x471,x472)+E(f18(x471,x473),f18(x472,x473)) % 0.56/0.73 [48]~E(x481,x482)+E(f18(x483,x481),f18(x483,x482)) % 0.56/0.73 [49]~E(x491,x492)+E(f16(x491),f16(x492)) % 0.56/0.73 [50]~E(x501,x502)+E(f22(x501,x503),f22(x502,x503)) % 0.56/0.73 [51]~E(x511,x512)+E(f22(x513,x511),f22(x513,x512)) % 0.56/0.73 [52]~E(x521,x522)+E(f17(x521),f17(x522)) % 0.56/0.73 [53]~E(x531,x532)+E(f8(x531),f8(x532)) % 0.56/0.73 [54]~P1(x541)+P1(x542)+~E(x541,x542) % 0.56/0.73 [55]P2(x552,x553)+~E(x551,x552)+~P2(x551,x553) % 0.56/0.73 [56]P2(x563,x562)+~E(x561,x562)+~P2(x563,x561) % 0.56/0.73 [57]~P4(x571)+P4(x572)+~E(x571,x572) % 0.56/0.73 [58]P6(x582,x583)+~E(x581,x582)+~P6(x581,x583) % 0.56/0.73 [59]P6(x593,x592)+~E(x591,x592)+~P6(x593,x591) % 0.56/0.73 [60]P9(x602,x603,x604)+~E(x601,x602)+~P9(x601,x603,x604) % 0.56/0.73 [61]P9(x613,x612,x614)+~E(x611,x612)+~P9(x613,x611,x614) % 0.56/0.73 [62]P9(x623,x624,x622)+~E(x621,x622)+~P9(x623,x624,x621) % 0.56/0.73 [63]P3(x632,x633)+~E(x631,x632)+~P3(x631,x633) % 0.56/0.73 [64]P3(x643,x642)+~E(x641,x642)+~P3(x643,x641) % 0.56/0.73 [65]~P8(x651)+P8(x652)+~E(x651,x652) % 0.56/0.73 [66]~P7(x661)+P7(x662)+~E(x661,x662) % 0.56/0.73 [67]~P5(x671)+P5(x672)+~E(x671,x672) % 0.56/0.73 % 0.56/0.73 %------------------------------------------- % 0.56/0.73 cnf(283,plain, % 0.56/0.73 (P4(f3(x2831))+~P6(x2831,a2)), % 0.56/0.73 inference(equality_inference,[],[126])). % 0.56/0.73 cnf(294,plain, % 0.56/0.73 (P4(f4(x2941,x2942))+~P6(x2942,a2)+~P6(x2941,a2)), % 0.56/0.73 inference(equality_inference,[],[178])). % 0.56/0.73 cnf(295,plain, % 0.56/0.73 (P4(f28(x2951,x2952))+~P6(x2952,a2)+~P6(x2951,a2)), % 0.56/0.73 inference(equality_inference,[],[179])). % 0.56/0.73 cnf(297,plain, % 0.56/0.73 (~P2(x2971,x2972)+~P2(x2971,f3(x2972))+~P6(x2972,a2)), % 0.56/0.73 inference(equality_inference,[],[187])). % 0.56/0.73 cnf(300,plain, % 0.56/0.73 (~P2(x3001,f28(x3002,x3003))+P2(x3001,x3003)+~P6(x3003,a2)+~P6(x3002,a2)), % 0.56/0.73 inference(equality_inference,[],[205])). % 0.56/0.73 cnf(301,plain, % 0.56/0.73 (~P2(x3011,f28(x3012,x3013))+P2(x3011,x3012)+~P6(x3012,a2)+~P6(x3013,a2)), % 0.56/0.73 inference(equality_inference,[],[206])). % 0.56/0.73 cnf(306,plain, % 0.56/0.73 (~P2(x3061,f4(x3062,x3063))+P2(x3061,x3063)+P2(x3061,x3062)+~P6(x3063,a2)+~P6(x3062,a2)), % 0.56/0.73 inference(equality_inference,[],[221])). % 0.56/0.73 cnf(355,plain, % 0.56/0.73 ($false), % 0.56/0.73 inference(scs_inference,[],[89,93,92,95,84,85,90,86,87,82,83,200,244,213,214,144,157,160,283,2,297,56,57,294,295,66,175,187,300,301,205,206,306,193]), % 0.56/0.73 ['proof']). % 0.56/0.73 % SZS output end Proof % 0.56/0.73 % Total time :0.020000s %------------------------------------------------------------------------------