%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM455+6 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n021.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:21 EDT 2024 % Result : Theorem 0.55s 0.77s % Output : CNFRefutation 0.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : NUM455+6 : TPTP v8.2.0. Released v4.0.0. % 0.04/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n021.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 : Sat Jun 22 23:35:53 EDT 2024 % 0.12/0.33 % CPUTime : % 0.53/0.57 start to proof:theBenchmark % 0.55/0.75 %------------------------------------------- % 0.55/0.75 % File :CSE---1.7 % 0.55/0.75 % Problem :theBenchmark % 0.55/0.75 % Transform :cnf % 0.55/0.75 % Format :tptp:raw % 0.55/0.75 % Command :java -jar mcs_scs.jar %d %s % 0.55/0.75 % 0.55/0.75 % Result :Theorem 0.100000s % 0.55/0.75 % Output :CNFRefutation 0.100000s % 0.55/0.75 %------------------------------------------- % 0.55/0.75 %------------------------------------------------------------------------------ % 0.55/0.75 % File : NUM455+6 : TPTP v8.2.0. Released v4.0.0. % 0.55/0.75 % Domain : Number Theory % 0.55/0.75 % Problem : Fuerstenberg's infinitude of primes 11_04_04, 05 expansion % 0.55/0.75 % Version : Especial. % 0.55/0.75 % English : % 0.55/0.75 % 0.55/0.75 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 0.55/0.75 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 0.55/0.75 % Source : [Pas08] % 0.55/0.75 % Names : fuerst_11_04_04.05 [Pas08] % 0.55/0.75 % 0.55/0.75 % Status : ContradictoryAxioms % 0.55/0.75 % Rating : 0.25 v8.2.0, 0.22 v8.1.0, 0.19 v7.5.0, 0.22 v7.4.0, 0.14 v7.3.0, 0.00 v7.0.0, 0.13 v6.4.0, 0.15 v6.3.0, 0.12 v6.2.0, 0.16 v6.1.0, 0.33 v6.0.0, 0.22 v5.5.0, 0.33 v5.4.0, 0.39 v5.3.0, 0.44 v5.2.0, 0.30 v5.1.0, 0.48 v5.0.0, 0.54 v4.1.0, 0.57 v4.0.1, 0.83 v4.0.0 % 0.55/0.75 % Syntax : Number of formulae : 50 ( 3 unt; 10 def) % 0.55/0.75 % Number of atoms : 343 ( 68 equ) % 0.55/0.75 % Maximal formula atoms : 56 ( 6 avg) % 0.55/0.75 % Number of connectives : 321 ( 28 ~; 18 |; 181 &) % 0.55/0.75 % ( 25 <=>; 69 =>; 0 <=; 0 <~>) % 0.55/0.75 % Maximal formula depth : 24 ( 7 avg) % 0.55/0.75 % Maximal term depth : 4 ( 1 avg) % 0.55/0.75 % Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty) % 0.55/0.75 % Number of functors : 16 ( 16 usr; 8 con; 0-2 aty) % 0.55/0.75 % Number of variables : 131 ( 105 !; 26 ?) % 0.55/0.75 % SPC : FOF_CAX_RFO_SEQ % 0.55/0.75 % 0.55/0.75 % Comments : Problem generated by the SAD system [VLP07] % 0.55/0.75 %------------------------------------------------------------------------------ % 0.55/0.75 fof(mIntegers,axiom, % 0.55/0.75 ! [W0] : % 0.55/0.75 ( aInteger0(W0) % 0.55/0.75 => $true ) ). % 0.55/0.75 % 0.55/0.75 fof(mIntZero,axiom, % 0.55/0.75 aInteger0(sz00) ). % 0.55/0.75 % 0.55/0.75 fof(mIntOne,axiom, % 0.55/0.75 aInteger0(sz10) ). % 0.55/0.75 % 0.55/0.75 fof(mIntNeg,axiom, % 0.55/0.75 ! [W0] : % 0.55/0.76 ( aInteger0(W0) % 0.55/0.76 => aInteger0(smndt0(W0)) ) ). % 0.55/0.76 % 0.55/0.76 fof(mIntPlus,axiom, % 0.55/0.76 ! [W0,W1] : % 0.55/0.76 ( ( aInteger0(W0) % 0.55/0.76 & aInteger0(W1) ) % 0.55/0.76 => aInteger0(sdtpldt0(W0,W1)) ) ). % 0.55/0.76 % 0.55/0.76 fof(mIntMult,axiom, % 0.55/0.76 ! [W0,W1] : % 0.55/0.76 ( ( aInteger0(W0) % 0.55/0.76 & aInteger0(W1) ) % 0.55/0.76 => aInteger0(sdtasdt0(W0,W1)) ) ). % 0.55/0.76 % 0.55/0.76 fof(mAddAsso,axiom, % 0.55/0.76 ! [W0,W1,W2] : % 0.55/0.76 ( ( aInteger0(W0) % 0.55/0.76 & aInteger0(W1) % 0.55/0.76 & aInteger0(W2) ) % 0.55/0.76 => sdtpldt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtpldt0(W0,W1),W2) ) ). % 0.55/0.76 % 0.55/0.76 fof(mAddComm,axiom, % 0.55/0.76 ! [W0,W1] : % 0.55/0.76 ( ( aInteger0(W0) % 0.55/0.76 & aInteger0(W1) ) % 0.55/0.76 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 0.55/0.76 % 0.55/0.76 fof(mAddZero,axiom, % 0.55/0.76 ! [W0] : % 0.55/0.76 ( aInteger0(W0) % 0.55/0.76 => ( sdtpldt0(W0,sz00) = W0 % 0.55/0.76 & W0 = sdtpldt0(sz00,W0) ) ) ). % 0.55/0.76 % 0.55/0.76 fof(mAddNeg,axiom, % 0.55/0.76 ! [W0] : % 0.55/0.76 ( aInteger0(W0) % 0.55/0.76 => ( sdtpldt0(W0,smndt0(W0)) = sz00 % 0.55/0.76 & sz00 = sdtpldt0(smndt0(W0),W0) ) ) ). % 0.55/0.76 % 0.55/0.76 fof(mMulAsso,axiom, % 0.55/0.76 ! [W0,W1,W2] : % 0.55/0.76 ( ( aInteger0(W0) % 0.55/0.76 & aInteger0(W1) % 0.55/0.76 & aInteger0(W2) ) % 0.55/0.76 => sdtasdt0(W0,sdtasdt0(W1,W2)) = sdtasdt0(sdtasdt0(W0,W1),W2) ) ). % 0.55/0.76 % 0.55/0.76 fof(mMulComm,axiom, % 0.55/0.76 ! [W0,W1] : % 0.55/0.76 ( ( aInteger0(W0) % 0.55/0.76 & aInteger0(W1) ) % 0.55/0.76 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 0.55/0.76 % 0.55/0.76 fof(mMulOne,axiom, % 0.55/0.76 ! [W0] : % 0.55/0.76 ( aInteger0(W0) % 0.55/0.76 => ( sdtasdt0(W0,sz10) = W0 % 0.55/0.76 & W0 = sdtasdt0(sz10,W0) ) ) ). % 0.55/0.76 % 0.55/0.76 fof(mDistrib,axiom, % 0.55/0.76 ! [W0,W1,W2] : % 0.55/0.76 ( ( aInteger0(W0) % 0.55/0.76 & aInteger0(W1) % 0.55/0.76 & aInteger0(W2) ) % 0.55/0.76 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 0.55/0.76 & sdtasdt0(sdtpldt0(W0,W1),W2) = sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W1,W2)) ) ) ). % 0.55/0.76 % 0.55/0.76 fof(mMulZero,axiom, % 0.55/0.76 ! [W0] : % 0.55/0.76 ( aInteger0(W0) % 0.55/0.76 => ( sdtasdt0(W0,sz00) = sz00 % 0.55/0.76 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 0.55/0.76 % 0.55/0.76 fof(mMulMinOne,axiom, % 0.55/0.76 ! [W0] : % 0.55/0.76 ( aInteger0(W0) % 0.55/0.76 => ( sdtasdt0(smndt0(sz10),W0) = smndt0(W0) % 0.55/0.76 & smndt0(W0) = sdtasdt0(W0,smndt0(sz10)) ) ) ). % 0.55/0.76 % 0.55/0.76 fof(mZeroDiv,axiom, % 0.55/0.76 ! [W0,W1] : % 0.55/0.76 ( ( aInteger0(W0) % 0.55/0.76 & aInteger0(W1) ) % 0.55/0.76 => ( sdtasdt0(W0,W1) = sz00 % 0.55/0.76 => ( W0 = sz00 % 0.55/0.76 | W1 = sz00 ) ) ) ). % 0.55/0.76 % 0.55/0.76 fof(mDivisor,definition, % 0.55/0.76 ! [W0] : % 0.55/0.76 ( aInteger0(W0) % 0.55/0.76 => ! [W1] : % 0.55/0.76 ( aDivisorOf0(W1,W0) % 0.55/0.76 <=> ( aInteger0(W1) % 0.55/0.76 & W1 != sz00 % 0.55/0.76 & ? [W2] : % 0.55/0.76 ( aInteger0(W2) % 0.55/0.76 & sdtasdt0(W1,W2) = W0 ) ) ) ) ). % 0.55/0.76 % 0.55/0.76 fof(mEquMod,definition, % 0.55/0.76 ! [W0,W1,W2] : % 0.55/0.76 ( ( aInteger0(W0) % 0.55/0.76 & aInteger0(W1) % 0.55/0.76 & aInteger0(W2) % 0.55/0.76 & W2 != sz00 ) % 0.55/0.76 => ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 0.55/0.76 <=> aDivisorOf0(W2,sdtpldt0(W0,smndt0(W1))) ) ) ). % 0.55/0.76 % 0.55/0.76 fof(mEquModRef,axiom, % 0.55/0.76 ! [W0,W1] : % 0.55/0.76 ( ( aInteger0(W0) % 0.55/0.76 & aInteger0(W1) % 0.55/0.76 & W1 != sz00 ) % 0.55/0.76 => sdteqdtlpzmzozddtrp0(W0,W0,W1) ) ). % 0.55/0.76 % 0.55/0.76 fof(mEquModSym,axiom, % 0.55/0.76 ! [W0,W1,W2] : % 0.55/0.76 ( ( aInteger0(W0) % 0.55/0.76 & aInteger0(W1) % 0.55/0.76 & aInteger0(W2) % 0.55/0.76 & W2 != sz00 ) % 0.55/0.76 => ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 0.55/0.76 => sdteqdtlpzmzozddtrp0(W1,W0,W2) ) ) ). % 0.55/0.76 % 0.55/0.76 fof(mEquModTrn,axiom, % 0.55/0.76 ! [W0,W1,W2,W3] : % 0.55/0.76 ( ( aInteger0(W0) % 0.55/0.76 & aInteger0(W1) % 0.55/0.76 & aInteger0(W2) % 0.55/0.76 & W2 != sz00 % 0.55/0.76 & aInteger0(W3) ) % 0.55/0.76 => ( ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 0.55/0.76 & sdteqdtlpzmzozddtrp0(W1,W3,W2) ) % 0.55/0.76 => sdteqdtlpzmzozddtrp0(W0,W3,W2) ) ) ). % 0.55/0.76 % 0.55/0.76 fof(mEquModMul,axiom, % 0.55/0.76 ! [W0,W1,W2,W3] : % 0.55/0.76 ( ( aInteger0(W0) % 0.55/0.76 & aInteger0(W1) % 0.55/0.76 & aInteger0(W2) % 0.55/0.76 & W2 != sz00 % 0.55/0.76 & aInteger0(W3) % 0.55/0.76 & W3 != sz00 ) % 0.55/0.76 => ( sdteqdtlpzmzozddtrp0(W0,W1,sdtasdt0(W2,W3)) % 0.55/0.76 => ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 0.55/0.76 & sdteqdtlpzmzozddtrp0(W0,W1,W3) ) ) ) ). % 0.55/0.76 % 0.55/0.76 fof(mPrime,axiom, % 0.55/0.76 ! [W0] : % 0.55/0.76 ( ( aInteger0(W0) % 0.55/0.76 & W0 != sz00 ) % 0.55/0.76 => ( isPrime0(W0) % 0.55/0.76 => $true ) ) ). % 0.55/0.76 % 0.55/0.76 fof(mPrimeDivisor,axiom, % 0.55/0.76 ! [W0] : % 0.55/0.76 ( aInteger0(W0) % 0.55/0.76 => ( ? [W1] : % 0.55/0.76 ( aDivisorOf0(W1,W0) % 0.55/0.76 & isPrime0(W1) ) % 0.55/0.76 <=> ( W0 != sz10 % 0.55/0.76 & W0 != smndt0(sz10) ) ) ) ). % 0.55/0.76 % 0.55/0.76 fof(mSets,axiom, % 0.55/0.76 ! [W0] : % 0.55/0.76 ( aSet0(W0) % 0.55/0.76 => $true ) ). % 0.55/0.76 % 0.55/0.76 fof(mElements,axiom, % 0.55/0.76 ! [W0] : % 0.55/0.76 ( aSet0(W0) % 0.55/0.76 => ! [W1] : % 0.55/0.76 ( aElementOf0(W1,W0) % 0.55/0.76 => $true ) ) ). % 0.55/0.76 % 0.55/0.76 fof(mSubset,definition, % 0.55/0.76 ! [W0] : % 0.55/0.76 ( aSet0(W0) % 0.55/0.76 => ! [W1] : % 0.55/0.76 ( aSubsetOf0(W1,W0) % 0.55/0.76 <=> ( aSet0(W1) % 0.55/0.76 & ! [W2] : % 0.55/0.76 ( aElementOf0(W2,W1) % 0.55/0.76 => aElementOf0(W2,W0) ) ) ) ) ). % 0.55/0.76 % 0.55/0.76 fof(mFinSet,axiom, % 0.55/0.76 ! [W0] : % 0.55/0.76 ( aSet0(W0) % 0.55/0.76 => ( isFinite0(W0) % 0.55/0.76 => $true ) ) ). % 0.55/0.76 % 0.55/0.76 fof(mUnion,definition, % 0.55/0.76 ! [W0,W1] : % 0.55/0.76 ( ( aSubsetOf0(W0,cS1395) % 0.55/0.76 & aSubsetOf0(W1,cS1395) ) % 0.55/0.76 => ! [W2] : % 0.55/0.76 ( W2 = sdtbsmnsldt0(W0,W1) % 0.55/0.76 <=> ( aSet0(W2) % 0.55/0.76 & ! [W3] : % 0.55/0.76 ( aElementOf0(W3,W2) % 0.55/0.76 <=> ( aInteger0(W3) % 0.55/0.76 & ( aElementOf0(W3,W0) % 0.55/0.76 | aElementOf0(W3,W1) ) ) ) ) ) ) ). % 0.55/0.76 % 0.55/0.76 fof(mIntersection,definition, % 0.55/0.76 ! [W0,W1] : % 0.55/0.76 ( ( aSubsetOf0(W0,cS1395) % 0.55/0.76 & aSubsetOf0(W1,cS1395) ) % 0.55/0.76 => ! [W2] : % 0.55/0.76 ( W2 = sdtslmnbsdt0(W0,W1) % 0.55/0.76 <=> ( aSet0(W2) % 0.55/0.76 & ! [W3] : % 0.55/0.76 ( aElementOf0(W3,W2) % 0.55/0.76 <=> ( aInteger0(W3) % 0.55/0.76 & aElementOf0(W3,W0) % 0.55/0.76 & aElementOf0(W3,W1) ) ) ) ) ) ). % 0.55/0.76 % 0.55/0.76 fof(mUnionSet,definition, % 0.55/0.76 ! [W0] : % 0.55/0.76 ( ( aSet0(W0) % 0.55/0.76 & ! [W1] : % 0.55/0.76 ( aElementOf0(W1,W0) % 0.55/0.76 => aSubsetOf0(W1,cS1395) ) ) % 0.55/0.76 => ! [W1] : % 0.55/0.76 ( W1 = sbsmnsldt0(W0) % 0.55/0.76 <=> ( aSet0(W1) % 0.55/0.76 & ! [W2] : % 0.55/0.76 ( aElementOf0(W2,W1) % 0.55/0.76 <=> ( aInteger0(W2) % 0.55/0.76 & ? [W3] : % 0.55/0.76 ( aElementOf0(W3,W0) % 0.55/0.76 & aElementOf0(W2,W3) ) ) ) ) ) ) ). % 0.55/0.76 % 0.55/0.76 fof(mComplement,definition, % 0.55/0.76 ! [W0] : % 0.55/0.76 ( aSubsetOf0(W0,cS1395) % 0.55/0.76 => ! [W1] : % 0.55/0.76 ( W1 = stldt0(W0) % 0.55/0.76 <=> ( aSet0(W1) % 0.55/0.76 & ! [W2] : % 0.55/0.77 ( aElementOf0(W2,W1) % 0.55/0.77 <=> ( aInteger0(W2) % 0.55/0.77 & ~ aElementOf0(W2,W0) ) ) ) ) ) ). % 0.55/0.77 % 0.55/0.77 fof(mArSeq,definition, % 0.55/0.77 ! [W0,W1] : % 0.55/0.77 ( ( aInteger0(W0) % 0.55/0.77 & aInteger0(W1) % 0.55/0.77 & W1 != sz00 ) % 0.55/0.77 => ! [W2] : % 0.55/0.77 ( W2 = szAzrzSzezqlpdtcmdtrp0(W0,W1) % 0.55/0.77 <=> ( aSet0(W2) % 0.55/0.77 & ! [W3] : % 0.55/0.77 ( aElementOf0(W3,W2) % 0.55/0.77 <=> ( aInteger0(W3) % 0.55/0.77 & sdteqdtlpzmzozddtrp0(W3,W0,W1) ) ) ) ) ) ). % 0.55/0.77 % 0.55/0.77 fof(mOpen,definition, % 0.55/0.77 ! [W0] : % 0.55/0.77 ( aSubsetOf0(W0,cS1395) % 0.55/0.77 => ( isOpen0(W0) % 0.55/0.77 <=> ! [W1] : % 0.55/0.77 ( aElementOf0(W1,W0) % 0.55/0.77 => ? [W2] : % 0.55/0.77 ( aInteger0(W2) % 0.55/0.77 & W2 != sz00 % 0.55/0.77 & aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W1,W2),W0) ) ) ) ) ). % 0.55/0.77 % 0.55/0.77 fof(mClosed,definition, % 0.55/0.77 ! [W0] : % 0.55/0.77 ( aSubsetOf0(W0,cS1395) % 0.55/0.77 => ( isClosed0(W0) % 0.55/0.77 <=> isOpen0(stldt0(W0)) ) ) ). % 0.55/0.77 % 0.55/0.77 fof(mUnionOpen,axiom, % 0.55/0.77 ! [W0] : % 0.55/0.77 ( ( aSet0(W0) % 0.55/0.77 & ! [W1] : % 0.55/0.77 ( aElementOf0(W1,W0) % 0.55/0.77 => ( aSubsetOf0(W1,cS1395) % 0.55/0.77 & isOpen0(W1) ) ) ) % 0.55/0.77 => isOpen0(sbsmnsldt0(W0)) ) ). % 0.55/0.77 % 0.55/0.77 fof(mInterOpen,axiom, % 0.55/0.77 ! [W0,W1] : % 0.55/0.77 ( ( aSubsetOf0(W0,cS1395) % 0.55/0.77 & aSubsetOf0(W1,cS1395) % 0.55/0.77 & isOpen0(W0) % 0.55/0.77 & isOpen0(W1) ) % 0.55/0.77 => isOpen0(sdtslmnbsdt0(W0,W1)) ) ). % 0.55/0.77 % 0.55/0.77 fof(mUnionClosed,axiom, % 0.55/0.77 ! [W0,W1] : % 0.55/0.77 ( ( aSubsetOf0(W0,cS1395) % 0.55/0.77 & aSubsetOf0(W1,cS1395) % 0.55/0.77 & isClosed0(W0) % 0.55/0.77 & isClosed0(W1) ) % 0.55/0.77 => isClosed0(sdtbsmnsldt0(W0,W1)) ) ). % 0.55/0.77 % 0.55/0.77 fof(mUnionSClosed,axiom, % 0.55/0.77 ! [W0] : % 0.55/0.77 ( ( aSet0(W0) % 0.55/0.77 & isFinite0(W0) % 0.55/0.77 & ! [W1] : % 0.55/0.77 ( aElementOf0(W1,W0) % 0.55/0.77 => ( aSubsetOf0(W1,cS1395) % 0.55/0.77 & isClosed0(W1) ) ) ) % 0.55/0.77 => isClosed0(sbsmnsldt0(W0)) ) ). % 0.55/0.77 % 0.55/0.77 fof(mArSeqClosed,axiom, % 0.55/0.77 ! [W0,W1] : % 0.55/0.77 ( ( aInteger0(W0) % 0.55/0.77 & aInteger0(W1) % 0.55/0.77 & W1 != sz00 ) % 0.55/0.77 => ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),cS1395) % 0.55/0.77 & isClosed0(szAzrzSzezqlpdtcmdtrp0(W0,W1)) ) ) ). % 0.55/0.77 % 0.55/0.77 fof(m__2046,hypothesis, % 0.55/0.77 ( aSet0(xS) % 0.55/0.77 & ! [W0] : % 0.55/0.77 ( ( aElementOf0(W0,xS) % 0.55/0.77 => ? [W1] : % 0.55/0.77 ( aInteger0(W1) % 0.55/0.77 & W1 != sz00 % 0.55/0.77 & isPrime0(W1) % 0.55/0.77 & aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,W1)) % 0.55/0.77 & ! [W2] : % 0.55/0.77 ( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1)) % 0.55/0.77 => ( aInteger0(W2) % 0.55/0.77 & ? [W3] : % 0.55/0.77 ( aInteger0(W3) % 0.55/0.77 & sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00)) ) % 0.55/0.77 & aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00))) % 0.55/0.77 & sdteqdtlpzmzozddtrp0(W2,sz00,W1) ) ) % 0.55/0.77 & ( ( aInteger0(W2) % 0.55/0.77 & ( ? [W3] : % 0.55/0.77 ( aInteger0(W3) % 0.55/0.77 & sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00)) ) % 0.55/0.77 | aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00))) % 0.55/0.77 | sdteqdtlpzmzozddtrp0(W2,sz00,W1) ) ) % 0.55/0.77 => aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1)) ) ) % 0.55/0.77 & szAzrzSzezqlpdtcmdtrp0(sz00,W1) = W0 ) ) % 0.55/0.77 & ( ? [W1] : % 0.55/0.77 ( aInteger0(W1) % 0.55/0.77 & W1 != sz00 % 0.55/0.77 & isPrime0(W1) % 0.55/0.77 & ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,W1)) % 0.55/0.77 & ! [W2] : % 0.55/0.77 ( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1)) % 0.55/0.77 => ( aInteger0(W2) % 0.55/0.77 & ? [W3] : % 0.55/0.77 ( aInteger0(W3) % 0.55/0.77 & sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00)) ) % 0.55/0.77 & aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00))) % 0.55/0.77 & sdteqdtlpzmzozddtrp0(W2,sz00,W1) ) ) % 0.55/0.77 & ( ( aInteger0(W2) % 0.55/0.77 & ( ? [W3] : % 0.55/0.77 ( aInteger0(W3) % 0.55/0.77 & sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00)) ) % 0.55/0.77 | aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00))) % 0.55/0.77 | sdteqdtlpzmzozddtrp0(W2,sz00,W1) ) ) % 0.55/0.77 => aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1)) ) ) ) % 0.55/0.77 => szAzrzSzezqlpdtcmdtrp0(sz00,W1) = W0 ) ) % 0.55/0.77 => aElementOf0(W0,xS) ) ) % 0.55/0.77 & xS = cS2043 ) ). % 0.55/0.77 % 0.55/0.77 fof(m__2079,hypothesis, % 0.55/0.77 ( aSet0(sbsmnsldt0(xS)) % 0.55/0.77 & ! [W0] : % 0.55/0.77 ( aElementOf0(W0,sbsmnsldt0(xS)) % 0.55/0.77 <=> ( aInteger0(W0) % 0.55/0.77 & ? [W1] : % 0.55/0.77 ( aElementOf0(W1,xS) % 0.55/0.77 & aElementOf0(W0,W1) ) ) ) % 0.55/0.77 & aSet0(stldt0(sbsmnsldt0(xS))) % 0.55/0.77 & ! [W0] : % 0.55/0.77 ( aElementOf0(W0,stldt0(sbsmnsldt0(xS))) % 0.55/0.77 <=> ( aInteger0(W0) % 0.55/0.77 & ~ aElementOf0(W0,sbsmnsldt0(xS)) ) ) % 0.55/0.77 & ! [W0] : % 0.55/0.77 ( aElementOf0(W0,stldt0(sbsmnsldt0(xS))) % 0.55/0.77 <=> ( W0 = sz10 % 0.55/0.77 | W0 = smndt0(sz10) ) ) % 0.55/0.77 & stldt0(sbsmnsldt0(xS)) = cS2076 ) ). % 0.55/0.77 % 0.55/0.77 fof(m__2117,hypothesis, % 0.55/0.77 isFinite0(xS) ). % 0.55/0.77 % 0.55/0.77 fof(m__2144,hypothesis, % 0.55/0.77 ( aSet0(sbsmnsldt0(xS)) % 0.55/0.77 & ! [W0] : % 0.55/0.77 ( aElementOf0(W0,sbsmnsldt0(xS)) % 0.55/0.77 <=> ( aInteger0(W0) % 0.55/0.77 & ? [W1] : % 0.55/0.77 ( aElementOf0(W1,xS) % 0.55/0.77 & aElementOf0(W0,W1) ) ) ) % 0.55/0.77 & ! [W0] : % 0.55/0.77 ( aElementOf0(W0,stldt0(sbsmnsldt0(xS))) % 0.55/0.77 <=> ( aInteger0(W0) % 0.55/0.77 & ~ aElementOf0(W0,sbsmnsldt0(xS)) ) ) % 0.55/0.77 & ! [W0] : % 0.55/0.77 ( aElementOf0(W0,stldt0(sbsmnsldt0(xS))) % 0.55/0.77 => ? [W1] : % 0.55/0.77 ( aInteger0(W1) % 0.55/0.77 & W1 != sz00 % 0.55/0.77 & aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)) % 0.55/0.77 & ! [W2] : % 0.55/0.77 ( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) % 0.55/0.77 => ( aInteger0(W2) % 0.55/0.77 & ? [W3] : % 0.55/0.77 ( aInteger0(W3) % 0.55/0.77 & sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0)) ) % 0.55/0.77 & aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))) % 0.55/0.77 & sdteqdtlpzmzozddtrp0(W2,W0,W1) ) ) % 0.55/0.77 & ( ( aInteger0(W2) % 0.55/0.77 & ( ? [W3] : % 0.55/0.77 ( aInteger0(W3) % 0.55/0.77 & sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0)) ) % 0.55/0.77 | aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))) % 0.55/0.77 | sdteqdtlpzmzozddtrp0(W2,W0,W1) ) ) % 0.55/0.77 => aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) ) ) % 0.55/0.77 & ! [W2] : % 0.55/0.77 ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) % 0.55/0.77 => aElementOf0(W2,stldt0(sbsmnsldt0(xS))) ) % 0.55/0.77 & aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS))) ) ) % 0.55/0.77 & isOpen0(stldt0(sbsmnsldt0(xS))) % 0.55/0.77 & isClosed0(sbsmnsldt0(xS)) % 0.55/0.77 & aSet0(sbsmnsldt0(xS)) % 0.55/0.77 & ! [W0] : % 0.55/0.77 ( aElementOf0(W0,sbsmnsldt0(xS)) % 0.55/0.77 <=> ( aInteger0(W0) % 0.55/0.77 & ? [W1] : % 0.55/0.77 ( aElementOf0(W1,xS) % 0.55/0.77 & aElementOf0(W0,W1) ) ) ) % 0.55/0.77 & ! [W0] : % 0.55/0.77 ( aElementOf0(W0,stldt0(sbsmnsldt0(xS))) % 0.55/0.77 <=> ( aInteger0(W0) % 0.55/0.77 & ~ aElementOf0(W0,sbsmnsldt0(xS)) ) ) % 0.55/0.77 & ! [W0] : % 0.55/0.77 ( aElementOf0(W0,stldt0(sbsmnsldt0(xS))) % 0.55/0.77 => ? [W1] : % 0.55/0.77 ( aInteger0(W1) % 0.55/0.77 & W1 != sz00 % 0.55/0.77 & aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)) % 0.55/0.77 & ! [W2] : % 0.55/0.77 ( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) % 0.55/0.77 => ( aInteger0(W2) % 0.55/0.77 & ? [W3] : % 0.55/0.77 ( aInteger0(W3) % 0.55/0.77 & sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0)) ) % 0.55/0.77 & aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))) % 0.55/0.77 & sdteqdtlpzmzozddtrp0(W2,W0,W1) ) ) % 0.55/0.77 & ( ( aInteger0(W2) % 0.55/0.77 & ( ? [W3] : % 0.55/0.77 ( aInteger0(W3) % 0.55/0.77 & sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0)) ) % 0.55/0.77 | aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))) % 0.55/0.77 | sdteqdtlpzmzozddtrp0(W2,W0,W1) ) ) % 0.55/0.77 => aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) ) ) % 0.55/0.77 & ! [W2] : % 0.55/0.77 ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) % 0.55/0.77 => aElementOf0(W2,stldt0(sbsmnsldt0(xS))) ) % 0.55/0.77 & aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS))) ) ) ) ). % 0.55/0.77 % 0.55/0.77 fof(m__2171,hypothesis, % 0.55/0.77 ( aInteger0(xp) % 0.55/0.77 & xp != sz00 % 0.55/0.77 & aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp)) % 0.55/0.77 & ! [W0] : % 0.55/0.77 ( ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) % 0.55/0.77 => ( aInteger0(W0) % 0.55/0.77 & ? [W1] : % 0.55/0.77 ( aInteger0(W1) % 0.55/0.77 & sdtasdt0(xp,W1) = sdtpldt0(W0,smndt0(sz10)) ) % 0.55/0.77 & aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10))) % 0.55/0.77 & sdteqdtlpzmzozddtrp0(W0,sz10,xp) ) ) % 0.55/0.77 & ( ( aInteger0(W0) % 0.55/0.77 & ( ? [W1] : % 0.55/0.77 ( aInteger0(W1) % 0.55/0.77 & sdtasdt0(xp,W1) = sdtpldt0(W0,smndt0(sz10)) ) % 0.55/0.77 | aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10))) % 0.55/0.77 | sdteqdtlpzmzozddtrp0(W0,sz10,xp) ) ) % 0.55/0.77 => aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) ) ) % 0.55/0.77 & aSet0(sbsmnsldt0(xS)) % 0.55/0.77 & ! [W0] : % 0.55/0.77 ( aElementOf0(W0,sbsmnsldt0(xS)) % 0.55/0.77 <=> ( aInteger0(W0) % 0.55/0.77 & ? [W1] : % 0.55/0.77 ( aElementOf0(W1,xS) % 0.55/0.77 & aElementOf0(W0,W1) ) ) ) % 0.55/0.77 & ! [W0] : % 0.55/0.77 ( aElementOf0(W0,stldt0(sbsmnsldt0(xS))) % 0.55/0.77 <=> ( aInteger0(W0) % 0.55/0.77 & ~ aElementOf0(W0,sbsmnsldt0(xS)) ) ) % 0.55/0.77 & ! [W0] : % 0.55/0.77 ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) % 0.55/0.77 => aElementOf0(W0,stldt0(sbsmnsldt0(xS))) ) % 0.55/0.77 & aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS))) ) ). % 0.55/0.77 % 0.55/0.77 fof(m__2232,hypothesis, % 0.55/0.77 ( ? [W0] : % 0.55/0.77 ( aInteger0(W0) % 0.55/0.77 & sdtasdt0(xp,W0) = sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)) ) % 0.55/0.77 & aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))) % 0.55/0.77 & sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp) % 0.55/0.77 & aElementOf0(sdtpldt0(sz10,xp),szAzrzSzezqlpdtcmdtrp0(sz10,xp)) % 0.55/0.77 & ? [W0] : % 0.55/0.77 ( aInteger0(W0) % 0.55/0.77 & sdtasdt0(xp,W0) = sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)) ) % 0.55/0.77 & aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10))) % 0.55/0.77 & sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,smndt0(xp)),sz10,xp) % 0.55/0.77 & aElementOf0(sdtpldt0(sz10,smndt0(xp)),szAzrzSzezqlpdtcmdtrp0(sz10,xp)) ) ). % 0.55/0.77 % 0.55/0.77 fof(m__2258,hypothesis, % 0.55/0.77 ( sdtpldt0(sz10,xp) != sz10 % 0.55/0.77 & sdtpldt0(sz10,smndt0(xp)) != sz10 ) ). % 0.55/0.77 % 0.55/0.77 fof(m__2286,hypothesis, % 0.55/0.77 ( sdtpldt0(sz10,xp) != smndt0(sz10) % 0.55/0.77 | sdtpldt0(sz10,smndt0(xp)) != smndt0(sz10) ) ). % 0.55/0.77 % 0.55/0.77 fof(m__,conjecture, % 0.55/0.77 ? [W0] : % 0.55/0.77 ( ( ( aInteger0(W0) % 0.55/0.77 & ( ? [W1] : % 0.55/0.77 ( aInteger0(W1) % 0.55/0.77 & sdtasdt0(xp,W1) = sdtpldt0(W0,smndt0(sz10)) ) % 0.55/0.77 | aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10))) % 0.55/0.77 | sdteqdtlpzmzozddtrp0(W0,sz10,xp) ) ) % 0.55/0.77 | aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) ) % 0.55/0.77 & ~ ( ( W0 = sz10 % 0.55/0.77 | W0 = smndt0(sz10) ) % 0.55/0.77 & aElementOf0(W0,cS2200) ) ) ). % 0.55/0.77 % 0.55/0.77 %------------------------------------------------------------------------------ % 0.55/0.77 %------------------------------------------- % 0.55/0.77 % Proof found % 0.55/0.77 % SZS status Theorem for theBenchmark % 0.55/0.77 % SZS output start Proof % 0.55/0.77 %ClaNum:309(EqnAxiom:77) % 0.55/0.77 %VarNum:1256(SingletonVarNum:390) % 0.55/0.77 %MaxLitNum:8 % 0.55/0.77 %MaxfuncDepth:2 % 0.55/0.77 %SharedTerms:50 % 0.55/0.77 %goalClause: 177 185 186 205 209 215 220 223 % 0.55/0.77 [78]E(a1,a2) % 0.55/0.77 [79]P1(a4) % 0.55/0.77 [80]P1(a43) % 0.55/0.77 [81]P1(a45) % 0.55/0.77 [82]P1(a5) % 0.55/0.77 [83]P1(a27) % 0.55/0.77 [84]P4(a1) % 0.55/0.77 [85]P5(a1) % 0.55/0.77 [104]~E(a45,a4) % 0.55/0.77 [90]P4(f28(a1)) % 0.55/0.77 [91]P6(f28(a1)) % 0.55/0.77 [94]P4(f44(a43,a45)) % 0.55/0.77 [97]P2(f38(a43,a45),f44(a43,a45)) % 0.55/0.77 [100]P9(f38(a43,a45),a43,a45) % 0.55/0.77 [105]~E(f38(a43,a45),a43) % 0.55/0.77 [86]E(f37(f28(a1)),a6) % 0.55/0.77 [92]P4(f37(f28(a1))) % 0.55/0.77 [93]P8(f37(f28(a1))) % 0.55/0.77 [95]P7(f44(a43,a45),f37(f28(a1))) % 0.55/0.77 [96]E(f38(f38(a43,a45),f41(a43)),f39(a45,a5)) % 0.55/0.77 [98]E(f38(f38(a43,f41(a45)),f41(a43)),f39(a45,a27)) % 0.55/0.77 [99]P2(f38(a43,f41(a45)),f44(a43,a45)) % 0.55/0.77 [101]P9(f38(a43,f41(a45)),a43,a45) % 0.55/0.77 [102]P3(a45,f38(f38(a43,a45),f41(a43))) % 0.55/0.77 [103]P3(a45,f38(f38(a43,f41(a45)),f41(a43))) % 0.55/0.77 [106]~E(f38(a43,f41(a45)),a43) % 0.55/0.77 [165]~E(f38(a43,a45),f41(a43))+~E(f38(a43,f41(a45)),f41(a43)) % 0.55/0.77 [107]~P1(x1071)+P1(f41(x1071)) % 0.55/0.77 [108]~P1(x1081)+E(f39(a4,x1081),a4) % 0.55/0.77 [109]~P1(x1091)+E(f39(x1091,a4),a4) % 0.55/0.77 [110]~P1(x1101)+E(f38(a4,x1101),x1101) % 0.55/0.77 [111]~P1(x1111)+E(f39(a43,x1111),x1111) % 0.55/0.77 [112]~P1(x1121)+E(f38(x1121,a4),x1121) % 0.55/0.77 [113]~P1(x1131)+E(f39(x1131,a43),x1131) % 0.55/0.78 [115]~P2(x1151,a1)+~E(f7(x1151),a4) % 0.55/0.78 [121]~P2(x1211,a1)+P1(f7(x1211)) % 0.55/0.78 [122]~P2(x1221,a1)+P10(f7(x1221)) % 0.55/0.78 [126]P1(x1261)+~P2(x1261,f28(a1)) % 0.55/0.78 [153]~P2(x1531,f28(a1))+P2(f15(x1531),a1) % 0.55/0.78 [154]~P2(x1541,f28(a1))+P2(f18(x1541),a1) % 0.55/0.78 [155]~P2(x1551,f28(a1))+P2(f20(x1551),a1) % 0.55/0.78 [156]~P2(x1561,f28(a1))+P2(f23(x1561),a1) % 0.55/0.78 [158]P2(x1581,f15(x1581))+~P2(x1581,f28(a1)) % 0.55/0.78 [159]P2(x1591,f18(x1591))+~P2(x1591,f28(a1)) % 0.55/0.78 [160]P2(x1601,f20(x1601))+~P2(x1601,f28(a1)) % 0.55/0.78 [161]P2(x1611,f23(x1611))+~P2(x1611,f28(a1)) % 0.55/0.78 [176]P1(x1761)+~P2(x1761,f44(a43,a45)) % 0.55/0.78 [182]~P2(x1821,f44(a43,a45))+P1(f25(x1821)) % 0.55/0.78 [186]P2(x1861,a10)+~P2(x1861,f44(a43,a45)) % 0.55/0.78 [231]~P2(x2311,f44(a43,a45))+P9(x2311,a43,a45) % 0.55/0.78 [116]~P1(x1161)+E(f38(f41(x1161),x1161),a4) % 0.55/0.78 [117]~P1(x1171)+E(f38(x1171,f41(x1171)),a4) % 0.55/0.78 [118]~P1(x1181)+E(f39(x1181,f41(a43)),f41(x1181)) % 0.55/0.78 [119]~P1(x1191)+E(f39(f41(a43),x1191),f41(x1191)) % 0.55/0.78 [120]~E(x1201,a43)+P2(x1201,f37(f28(a1))) % 0.55/0.78 [128]~E(x1281,f41(a43))+P2(x1281,f37(f28(a1))) % 0.55/0.78 [136]~P2(x1361,a1)+E(f44(a4,f7(x1361)),x1361) % 0.55/0.78 [152]P1(x1521)+~P2(x1521,f37(f28(a1))) % 0.55/0.78 [162]~E(f21(x1621),a4)+~P2(x1621,f37(f28(a1))) % 0.55/0.78 [163]~E(f24(x1631),a4)+~P2(x1631,f37(f28(a1))) % 0.55/0.78 [171]P1(f21(x1711))+~P2(x1711,f37(f28(a1))) % 0.55/0.78 [172]P1(f24(x1721))+~P2(x1721,f37(f28(a1))) % 0.55/0.78 [178]~P2(x1781,a1)+P4(f44(a4,f7(x1781))) % 0.55/0.78 [199]~P2(x1991,f28(a1))+~P2(x1991,f37(f28(a1))) % 0.55/0.78 [207]~P2(x2071,f44(a43,a45))+P2(x2071,f37(f28(a1))) % 0.55/0.78 [210]~P2(x2101,f37(f28(a1)))+P4(f44(x2101,f21(x2101))) % 0.55/0.78 [211]~P2(x2111,f37(f28(a1)))+P4(f44(x2111,f24(x2111))) % 0.55/0.78 [214]~P2(x2141,f44(a43,a45))+E(f39(a45,f25(x2141)),f38(x2141,f41(a43))) % 0.55/0.78 [222]~P2(x2221,f44(a43,a45))+P3(a45,f38(x2221,f41(a43))) % 0.55/0.78 [232]~P2(x2321,f37(f28(a1)))+P7(f44(x2321,f21(x2321)),f37(f28(a1))) % 0.55/0.78 [233]~P2(x2331,f37(f28(a1)))+P7(f44(x2331,f24(x2331)),f37(f28(a1))) % 0.55/0.78 [223]~P1(x2231)+P2(x2231,a10)+~P9(x2231,a43,a45) % 0.55/0.78 [133]~P6(x1331)+~P7(x1331,a3)+P8(f37(x1331)) % 0.55/0.78 [134]~P4(x1341)+P2(f8(x1341),x1341)+P8(f28(x1341)) % 0.55/0.78 [139]P6(x1391)+~P7(x1391,a3)+~P8(f37(x1391)) % 0.55/0.78 [146]P8(x1461)+P2(f9(x1461),x1461)+~P7(x1461,a3) % 0.55/0.78 [177]E(x1771,a43)+~P2(x1771,f44(a43,a45))+E(x1771,f41(a43)) % 0.55/0.78 [244]~P1(x2441)+P2(x2441,f44(a43,a45))+~P9(x2441,a43,a45) % 0.55/0.78 [157]E(x1571,a43)+E(x1571,f41(a43))+~P2(x1571,f37(f28(a1))) % 0.55/0.78 [170]~P1(x1701)+P2(x1701,f28(a1))+P2(x1701,f37(f28(a1))) % 0.55/0.78 [215]~P1(x2151)+P2(x2151,a10)+~P3(a45,f38(x2151,f41(a43))) % 0.55/0.78 [237]~P1(x2371)+P2(x2371,f44(a43,a45))+~P3(a45,f38(x2371,f41(a43))) % 0.55/0.78 [127]~P3(x1271,x1272)+~P1(x1272)+~E(x1271,a4) % 0.55/0.78 [131]~P3(x1311,x1312)+P1(x1311)+~P1(x1312) % 0.55/0.78 [132]~P7(x1321,x1322)+P4(x1321)+~P4(x1322) % 0.55/0.78 [130]P4(x1301)+~P7(x1302,a3)+~E(x1301,f37(x1302)) % 0.55/0.78 [140]~P1(x1402)+~P1(x1401)+E(f38(x1401,x1402),f38(x1402,x1401)) % 0.55/0.78 [141]~P1(x1412)+~P1(x1411)+E(f39(x1411,x1412),f39(x1412,x1411)) % 0.55/0.78 [144]~P1(x1442)+~P1(x1441)+P1(f38(x1441,x1442)) % 0.55/0.78 [145]~P1(x1452)+~P1(x1451)+P1(f39(x1451,x1452)) % 0.55/0.78 [179]~P1(x1791)+~P3(x1792,x1791)+P1(f19(x1791,x1792)) % 0.55/0.78 [201]~P1(x2012)+~P3(x2011,x2012)+E(f39(x2011,f19(x2012,x2011)),x2012) % 0.55/0.78 [228]P1(x2281)+~P2(x2282,a1)+~P2(x2281,f44(a4,f7(x2282))) % 0.55/0.78 [247]~P2(x2471,a1)+P1(f16(x2471,x2472))+~P2(x2472,f44(a4,f7(x2471))) % 0.55/0.78 [248]P1(x2481)+~P2(x2481,f44(x2482,f21(x2482)))+~P2(x2482,f37(f28(a1))) % 0.55/0.78 [249]P1(x2491)+~P2(x2491,f44(x2492,f24(x2492)))+~P2(x2492,f37(f28(a1))) % 0.55/0.78 [261]~P2(x2611,a1)+P3(f7(x2611),f38(x2612,f41(a4)))+~P2(x2612,f44(a4,f7(x2611))) % 0.55/0.78 [262]~P2(x2621,f44(x2622,f21(x2622)))+P2(x2621,f37(f28(a1)))+~P2(x2622,f37(f28(a1))) % 0.55/0.78 [263]~P2(x2631,f44(x2632,f24(x2632)))+P2(x2631,f37(f28(a1)))+~P2(x2632,f37(f28(a1))) % 0.55/0.78 [264]~P2(x2642,f44(x2641,f21(x2641)))+P1(f22(x2641,x2642))+~P2(x2641,f37(f28(a1))) % 0.55/0.78 [265]~P2(x2652,f44(x2651,f24(x2651)))+P1(f26(x2651,x2652))+~P2(x2651,f37(f28(a1))) % 0.55/0.78 [268]~P2(x2682,a1)+P9(x2681,a4,f7(x2682))+~P2(x2681,f44(a4,f7(x2682))) % 0.55/0.78 [271]~P2(x2711,a1)+E(f39(f7(x2711),f16(x2711,x2712)),f38(x2712,f41(a4)))+~P2(x2712,f44(a4,f7(x2711))) % 0.55/0.78 [279]~P2(x2792,f44(x2791,f21(x2791)))+P3(f21(x2791),f38(x2792,f41(x2791)))+~P2(x2791,f37(f28(a1))) % 0.55/0.78 [280]~P2(x2802,f44(x2801,f24(x2801)))+P3(f24(x2801),f38(x2802,f41(x2801)))+~P2(x2801,f37(f28(a1))) % 0.55/0.78 [282]P9(x2821,x2822,f21(x2822))+~P2(x2821,f44(x2822,f21(x2822)))+~P2(x2822,f37(f28(a1))) % 0.55/0.78 [283]P9(x2831,x2832,f24(x2832))+~P2(x2831,f44(x2832,f24(x2832)))+~P2(x2832,f37(f28(a1))) % 0.55/0.78 [286]~P2(x2862,f44(x2861,f21(x2861)))+E(f39(f21(x2861),f22(x2861,x2862)),f38(x2862,f41(x2861)))+~P2(x2861,f37(f28(a1))) % 0.55/0.78 [287]~P2(x2872,f44(x2871,f24(x2871)))+E(f39(f24(x2871),f26(x2871,x2872)),f38(x2872,f41(x2871)))+~P2(x2871,f37(f28(a1))) % 0.55/0.78 [114]~P1(x1141)+E(x1141,a43)+E(x1141,f41(a43))+P10(f29(x1141)) % 0.55/0.78 [129]~P1(x1291)+P3(f29(x1291),x1291)+E(x1291,a43)+E(x1291,f41(a43)) % 0.55/0.78 [147]~P4(x1471)+~P5(x1471)+P2(f14(x1471),x1471)+P6(f28(x1471)) % 0.55/0.78 [183]~P4(x1831)+~P8(f8(x1831))+~P7(f8(x1831),a3)+P8(f28(x1831)) % 0.55/0.78 [220]~P1(x2201)+E(x2201,a43)+~P9(x2201,a43,a45)+E(x2201,f41(a43)) % 0.55/0.78 [209]~P1(x2091)+E(x2091,a43)+E(x2091,f41(a43))+~P3(a45,f38(x2091,f41(a43))) % 0.55/0.78 [135]~P1(x1351)+~P3(x1352,x1351)+~P10(x1352)+~E(x1351,a43) % 0.55/0.78 [200]~P1(x2001)+~P1(x2002)+P9(x2002,x2002,x2001)+E(x2001,a4) % 0.55/0.78 [138]~P4(x1382)+P4(x1381)+~E(x1381,f28(x1382))+P2(f30(x1382),x1382) % 0.55/0.78 [142]~P1(x1421)+~P3(x1422,x1421)+~P10(x1422)+~E(x1421,f41(a43)) % 0.55/0.78 [148]~P1(x1481)+~P1(x1482)+E(x1481,a4)+P6(f44(x1482,x1481)) % 0.55/0.78 [164]~P4(x1642)+P4(x1641)+~E(x1641,f28(x1642))+~P7(f30(x1642),a3) % 0.55/0.78 [173]~P1(x1731)+~P1(x1732)+E(x1731,a4)+P7(f44(x1732,x1731),a3) % 0.55/0.78 [192]~P1(x1921)+~P2(x1921,x1922)+~P2(x1922,a1)+P2(x1921,f28(a1)) % 0.55/0.78 [193]~P4(x1931)+~P4(x1932)+P7(x1931,x1932)+P2(f31(x1932,x1931),x1931) % 0.55/0.78 [204]~P8(x2041)+~P2(x2042,x2041)+~P7(x2041,a3)+~E(f11(x2041,x2042),a4) % 0.55/0.78 [208]~P8(x2081)+~P2(x2082,x2081)+~P7(x2081,a3)+P1(f11(x2081,x2082)) % 0.55/0.78 [219]~P4(x2191)+~P4(x2192)+P7(x2191,x2192)+~P2(f31(x2192,x2191),x2192) % 0.55/0.78 [205]~P1(x2052)+~P1(x2051)+P2(x2051,a10)+~E(f39(a45,x2052),f38(x2051,f41(a43))) % 0.55/0.78 [221]~P1(x2211)+~P1(x2212)+P2(x2211,f44(a43,a45))+~E(f39(a45,x2212),f38(x2211,f41(a43))) % 0.55/0.78 [256]~P8(x2562)+~P2(x2561,x2562)+~P7(x2562,a3)+P7(f44(x2561,f11(x2562,x2561)),x2562) % 0.55/0.78 [269]~P1(x2691)+~P2(x2692,a1)+~P3(f7(x2692),f38(x2691,f41(a4)))+P2(x2691,f44(a4,f7(x2692))) % 0.55/0.78 [274]~P1(x2741)+~P2(x2742,a1)+~P9(x2741,a4,f7(x2742))+P2(x2741,f44(a4,f7(x2742))) % 0.55/0.78 [288]~P1(x2881)+~P3(f21(x2882),f38(x2881,f41(x2882)))+P2(x2881,f44(x2882,f21(x2882)))+~P2(x2882,f37(f28(a1))) % 0.55/0.78 [289]~P1(x2891)+~P3(f24(x2892),f38(x2891,f41(x2892)))+P2(x2891,f44(x2892,f24(x2892)))+~P2(x2892,f37(f28(a1))) % 0.55/0.78 [290]~P1(x2901)+~P9(x2901,x2902,f21(x2902))+P2(x2901,f44(x2902,f21(x2902)))+~P2(x2902,f37(f28(a1))) % 0.55/0.78 [291]~P1(x2911)+~P9(x2911,x2912,f24(x2912))+P2(x2911,f44(x2912,f24(x2912)))+~P2(x2912,f37(f28(a1))) % 0.55/0.78 [187]~P4(x1872)+~P7(x1873,x1872)+P2(x1871,x1872)+~P2(x1871,x1873) % 0.55/0.78 [174]~P2(x1741,x1742)+P1(x1741)+~P7(x1743,a3)+~E(x1742,f37(x1743)) % 0.55/0.78 [194]P4(x1941)+~P7(x1943,a3)+~P7(x1942,a3)+~E(x1941,f40(x1942,x1943)) % 0.55/0.78 [195]P4(x1951)+~P7(x1953,a3)+~P7(x1952,a3)+~E(x1951,f42(x1952,x1953)) % 0.55/0.78 [206]~P2(x2063,x2062)+~P2(x2063,x2061)+~P7(x2062,a3)+~E(x2061,f37(x2062)) % 0.55/0.78 [224]~P1(x2243)+~P1(x2242)+~P1(x2241)+E(f38(f38(x2241,x2242),x2243),f38(x2241,f38(x2242,x2243))) % 0.55/0.78 [225]~P1(x2253)+~P1(x2252)+~P1(x2251)+E(f39(f39(x2251,x2252),x2253),f39(x2251,f39(x2252,x2253))) % 0.55/0.78 [245]~P1(x2453)+~P1(x2452)+~P1(x2451)+E(f38(f39(x2451,x2452),f39(x2451,x2453)),f39(x2451,f38(x2452,x2453))) % 0.55/0.78 [246]~P1(x2462)+~P1(x2463)+~P1(x2461)+E(f38(f39(x2461,x2462),f39(x2463,x2462)),f39(f38(x2461,x2463),x2462)) % 0.55/0.78 [202]~P4(x2021)+~P5(x2021)+~P6(f14(x2021))+~P7(f14(x2021),a3)+P6(f28(x2021)) % 0.55/0.78 [137]~P1(x1371)+~P1(x1372)+E(x1371,a4)+E(x1372,a4)+~E(f39(x1372,x1371),a4) % 0.55/0.78 [166]~P1(x1661)+~P10(x1661)+E(x1661,a4)+P2(x1662,a1)+~E(f44(a4,x1661),x1662) % 0.55/0.78 [175]~P1(x1751)+~P10(x1751)+E(x1751,a4)+P2(x1752,a1)+P4(f44(a4,x1751)) % 0.55/0.78 [212]~P8(x2122)+~P8(x2121)+~P7(x2122,a3)+~P7(x2121,a3)+P8(f42(x2121,x2122)) % 0.55/0.78 [213]~P6(x2132)+~P6(x2131)+~P7(x2132,a3)+~P7(x2131,a3)+P6(f40(x2131,x2132)) % 0.55/0.78 [230]~P4(x2301)+P2(f12(x2302,x2301),x2301)+~P7(x2302,a3)+E(x2301,f37(x2302))+P1(f12(x2302,x2301)) % 0.55/0.78 [254]~P4(x2541)+P2(f12(x2542,x2541),x2541)+~P7(x2542,a3)+~P2(f12(x2542,x2541),x2542)+E(x2541,f37(x2542)) % 0.55/0.78 [185]~P1(x1852)+~P1(x1851)+E(x1851,a43)+E(x1851,f41(a43))+~E(f39(a45,x1852),f38(x1851,f41(a43))) % 0.55/0.78 [239]~P1(x2391)+P8(x2392)+~P7(x2392,a3)+E(x2391,a4)+~P7(f44(f9(x2392),x2391),x2392) % 0.55/0.78 [143]~P1(x1431)+~P1(x1433)+P4(x1432)+E(x1431,a4)+~E(x1432,f44(x1433,x1431)) % 0.55/0.78 [181]~P4(x1812)+~P2(x1811,x1813)+P1(x1811)+P2(f30(x1812),x1812)+~E(x1813,f28(x1812)) % 0.55/0.78 [184]~P1(x1841)+P2(x1841,x1842)+P2(x1841,x1843)+~E(x1842,f37(x1843))+~P7(x1843,a3) % 0.55/0.78 [203]~P4(x2033)+~P2(x2031,x2032)+P1(x2031)+~E(x2032,f28(x2033))+~P7(f30(x2033),a3) % 0.55/0.78 [277]~P4(x2771)+~P2(x2772,x2773)+~E(x2773,f28(x2771))+P2(f30(x2771),x2771)+P2(x2772,f35(x2771,x2773,x2772)) % 0.55/0.78 [278]~P4(x2781)+~P2(x2783,x2782)+~E(x2782,f28(x2781))+P2(f30(x2781),x2781)+P2(f35(x2781,x2782,x2783),x2781) % 0.55/0.78 [284]~P4(x2842)+~P2(x2841,x2843)+~E(x2843,f28(x2842))+P2(x2841,f35(x2842,x2843,x2841))+~P7(f30(x2842),a3) % 0.55/0.78 [285]~P4(x2851)+~P2(x2853,x2852)+~E(x2852,f28(x2851))+P2(f35(x2851,x2852,x2853),x2851)+~P7(f30(x2851),a3) % 0.55/0.78 [257]~P1(x2571)+~P1(x2573)+~P2(x2572,a1)+~E(f39(f7(x2572),x2573),f38(x2571,f41(a4)))+P2(x2571,f44(a4,f7(x2572))) % 0.55/0.78 [275]~P1(x2751)+~P1(x2753)+P2(x2751,f44(x2752,f21(x2752)))+~E(f39(f21(x2752),x2753),f38(x2751,f41(x2752)))+~P2(x2752,f37(f28(a1))) % 0.55/0.78 [276]~P1(x2761)+~P1(x2763)+P2(x2761,f44(x2762,f24(x2762)))+~E(f39(f24(x2762),x2763),f38(x2761,f41(x2762)))+~P2(x2762,f37(f28(a1))) % 0.55/0.78 [216]~P2(x2161,x2162)+P1(x2161)+~P7(x2164,a3)+~P7(x2163,a3)+~E(x2162,f40(x2163,x2164)) % 0.55/0.78 [217]~P2(x2171,x2172)+P1(x2171)+~P7(x2174,a3)+~P7(x2173,a3)+~E(x2172,f42(x2173,x2174)) % 0.55/0.78 [226]~P2(x2261,x2263)+P2(x2261,x2262)+~P7(x2264,a3)+~P7(x2262,a3)+~E(x2263,f42(x2264,x2262)) % 0.55/0.78 [227]~P2(x2271,x2273)+P2(x2271,x2272)+~P7(x2274,a3)+~P7(x2272,a3)+~E(x2273,f42(x2272,x2274)) % 0.55/0.78 [236]~P4(x2361)+~P4(x2362)+P2(f30(x2362),x2362)+P2(f34(x2362,x2361),x2361)+E(x2361,f28(x2362))+P1(f34(x2362,x2361)) % 0.55/0.78 [242]~P4(x2421)+~P4(x2422)+P2(f34(x2422,x2421),x2421)+E(x2421,f28(x2422))+P1(f34(x2422,x2421))+~P7(f30(x2422),a3) % 0.55/0.78 [243]~P4(x2431)+~P4(x2432)+P2(f30(x2432),x2432)+P2(f34(x2432,x2431),x2431)+P2(f36(x2432,x2431),x2432)+E(x2431,f28(x2432)) % 0.55/0.78 [251]~P4(x2511)+~P4(x2512)+P2(f34(x2512,x2511),x2511)+P2(f36(x2512,x2511),x2512)+E(x2511,f28(x2512))+~P7(f30(x2512),a3) % 0.55/0.78 [259]~P4(x2591)+~P4(x2592)+P2(f30(x2592),x2592)+P2(f34(x2592,x2591),x2591)+P2(f34(x2592,x2591),f36(x2592,x2591))+E(x2591,f28(x2592)) % 0.55/0.78 [266]~P4(x2661)+~P4(x2662)+P2(f34(x2662,x2661),x2661)+P2(f34(x2662,x2661),f36(x2662,x2661))+E(x2661,f28(x2662))+~P7(f30(x2662),a3) % 0.55/0.78 [281]~P4(x2811)+P2(f12(x2812,x2811),x2812)+~P7(x2812,a3)+~P2(f12(x2812,x2811),x2811)+E(x2811,f37(x2812))+~P1(f12(x2812,x2811)) % 0.55/0.78 [273]~P1(x2731)+~P1(x2732)+~P1(x2733)+~P9(x2733,x2732,x2731)+P9(x2732,x2733,x2731)+E(x2731,a4) % 0.55/0.78 [180]~P1(x1802)+~P1(x1803)+~P1(x1801)+P3(x1801,x1802)+E(x1801,a4)+~E(f39(x1801,x1803),x1802) % 0.55/0.78 [218]~P1(x2181)+~P10(x2181)+P1(x2182)+E(x2181,a4)+P2(x2183,a1)+~P2(x2182,f44(a4,x2181)) % 0.55/0.78 [255]~P1(x2551)+~P10(x2551)+P9(x2553,a4,x2551)+E(x2551,a4)+P2(x2552,a1)+~P2(x2553,f44(a4,x2551)) % 0.55/0.78 [292]~P1(x2921)+~P10(x2921)+E(x2921,a4)+P2(x2922,a1)+~P2(x2923,f44(a4,x2921))+P1(f17(x2922,x2921,x2923)) % 0.55/0.78 [300]~P4(x3001)+P2(f32(x3002,x3003,x3001),x3001)+~P7(x3003,a3)+~P7(x3002,a3)+E(x3001,f40(x3002,x3003))+P1(f32(x3002,x3003,x3001)) % 0.55/0.78 [301]~P4(x3011)+P2(f33(x3012,x3013,x3011),x3011)+~P7(x3013,a3)+~P7(x3012,a3)+E(x3011,f42(x3012,x3013))+P1(f33(x3012,x3013,x3011)) % 0.55/0.78 [302]~P4(x3021)+P2(f33(x3022,x3023,x3021),x3021)+P2(f33(x3022,x3023,x3021),x3023)+~P7(x3023,a3)+~P7(x3022,a3)+E(x3021,f42(x3022,x3023)) % 0.55/0.78 [303]~P4(x3031)+P2(f33(x3032,x3033,x3031),x3031)+P2(f33(x3032,x3033,x3031),x3032)+~P7(x3033,a3)+~P7(x3032,a3)+E(x3031,f42(x3032,x3033)) % 0.55/0.78 [253]~P1(x2531)+~P10(x2531)+E(x2531,a4)+P2(x2532,a1)+~P2(x2533,f44(a4,x2531))+P3(x2531,f38(x2533,f41(a4))) % 0.55/0.78 [270]~P1(x2703)+~P1(x2702)+~P1(x2701)+P9(x2702,x2703,x2701)+E(x2701,a4)+~P3(x2701,f38(x2702,f41(x2703))) % 0.55/0.78 [272]~P1(x2721)+~P1(x2723)+~P1(x2722)+~P9(x2722,x2723,x2721)+E(x2721,a4)+P3(x2721,f38(x2722,f41(x2723))) % 0.55/0.78 [295]~P1(x2951)+~P10(x2951)+P2(x2952,a1)+E(x2951,a4)+~P2(x2953,f44(a4,x2951))+E(f39(x2951,f17(x2952,x2951,x2953)),f38(x2953,f41(a4))) % 0.55/0.78 [188]~P1(x1881)+~P1(x1884)+~P2(x1882,x1883)+P1(x1882)+E(x1881,a4)+~E(x1883,f44(x1884,x1881)) % 0.55/0.78 [234]~P1(x2341)+~P2(x2341,x2344)+P2(x2341,x2342)+~P7(x2343,a3)+~P7(x2344,a3)+~E(x2342,f40(x2343,x2344)) % 0.55/0.78 [235]~P1(x2351)+~P2(x2351,x2353)+P2(x2351,x2352)+~P7(x2354,a3)+~P7(x2353,a3)+~E(x2352,f40(x2353,x2354)) % 0.55/0.78 [240]~P2(x2401,x2404)+P2(x2401,x2402)+P2(x2401,x2403)+~P7(x2402,a3)+~P7(x2403,a3)+~E(x2404,f40(x2403,x2402)) % 0.55/0.78 [241]~P1(x2411)+~P1(x2413)+~P2(x2412,x2414)+P9(x2412,x2413,x2411)+E(x2411,a4)+~E(x2414,f44(x2413,x2411)) % 0.55/0.78 [267]~P1(x2671)+~P1(x2673)+~P10(x2671)+~P9(x2673,a4,x2671)+E(x2671,a4)+P2(x2672,a1)+P2(x2673,f44(a4,x2671)) % 0.55/0.78 [299]~P1(x2991)+~P1(x2993)+~P4(x2992)+P2(f13(x2993,x2991,x2992),x2992)+E(x2991,a4)+E(x2992,f44(x2993,x2991))+P1(f13(x2993,x2991,x2992)) % 0.55/0.78 [304]~P1(x3041)+~P1(x3043)+~P4(x3042)+P9(f13(x3043,x3041,x3042),x3043,x3041)+P2(f13(x3043,x3041,x3042),x3042)+E(x3041,a4)+E(x3042,f44(x3043,x3041)) % 0.55/0.78 [305]~P4(x3051)+P2(f32(x3052,x3053,x3051),x3051)+P2(f32(x3052,x3053,x3051),x3053)+P2(f32(x3052,x3053,x3051),x3052)+~P7(x3053,a3)+~P7(x3052,a3)+E(x3051,f40(x3052,x3053)) % 0.55/0.78 [306]~P4(x3061)+~P7(x3063,a3)+~P7(x3062,a3)+~P2(f32(x3062,x3063,x3061),x3061)+~P2(f32(x3062,x3063,x3061),x3063)+E(x3061,f40(x3062,x3063))+~P1(f32(x3062,x3063,x3061)) % 0.55/0.78 [307]~P4(x3071)+~P7(x3073,a3)+~P7(x3072,a3)+~P2(f32(x3072,x3073,x3071),x3071)+~P2(f32(x3072,x3073,x3071),x3072)+E(x3071,f40(x3072,x3073))+~P1(f32(x3072,x3073,x3071)) % 0.55/0.78 [258]~P1(x2583)+~P1(x2581)+~P10(x2581)+E(x2581,a4)+P2(x2582,a1)+P2(x2583,f44(a4,x2581))+~P3(x2581,f38(x2583,f41(a4))) % 0.55/0.78 [229]~P1(x2291)+~P4(x2293)+~P2(x2291,x2294)+P2(x2291,x2292)+~P2(x2294,x2293)+~E(x2292,f28(x2293))+P2(f30(x2293),x2293) % 0.55/0.78 [238]~P1(x2381)+~P4(x2383)+~P2(x2381,x2384)+P2(x2381,x2382)+~P2(x2384,x2383)+~E(x2382,f28(x2383))+~P7(f30(x2383),a3) % 0.55/0.78 [252]~P1(x2521)+~P2(x2521,x2524)+~P2(x2521,x2523)+P2(x2521,x2522)+~P7(x2524,a3)+~P7(x2523,a3)+~E(x2522,f42(x2523,x2524)) % 0.55/0.78 [260]~P1(x2601)+~P1(x2604)+~P1(x2602)+~P9(x2602,x2604,x2601)+P2(x2602,x2603)+E(x2601,a4)+~E(x2603,f44(x2604,x2601)) % 0.55/0.78 [296]~P4(x2961)+~P4(x2962)+~P2(x2963,x2962)+P2(f30(x2962),x2962)+~P2(f34(x2962,x2961),x2963)+~P2(f34(x2962,x2961),x2961)+E(x2961,f28(x2962))+~P1(f34(x2962,x2961)) % 0.55/0.78 [297]~P4(x2971)+~P4(x2972)+~P2(x2973,x2972)+~P2(f34(x2972,x2971),x2973)+~P2(f34(x2972,x2971),x2971)+E(x2971,f28(x2972))+~P1(f34(x2972,x2971))+~P7(f30(x2972),a3) % 0.55/0.78 [308]~P1(x3081)+~P1(x3083)+~P4(x3082)+~P9(f13(x3083,x3081,x3082),x3083,x3081)+~P2(f13(x3083,x3081,x3082),x3082)+E(x3081,a4)+E(x3082,f44(x3083,x3081))+~P1(f13(x3083,x3081,x3082)) % 0.55/0.78 [309]~P4(x3091)+~P7(x3093,a3)+~P7(x3092,a3)+~P2(f33(x3092,x3093,x3091),x3091)+~P2(f33(x3092,x3093,x3091),x3093)+~P2(f33(x3092,x3093,x3091),x3092)+E(x3091,f42(x3092,x3093))+~P1(f33(x3092,x3093,x3091)) % 0.55/0.78 [298]~P1(x2983)+~P1(x2981)+~P1(x2982)+~P9(x2984,x2983,x2981)+~P9(x2982,x2984,x2981)+P9(x2982,x2983,x2981)+~P1(x2984)+E(x2981,a4) % 0.55/0.78 [293]~P1(x2931)+~P1(x2932)+~P1(x2934)+~P1(x2933)+P9(x2933,x2934,x2932)+~P9(x2933,x2934,f39(x2931,x2932))+E(x2931,a4)+E(x2932,a4) % 0.55/0.78 [294]~P1(x2941)+~P1(x2942)+~P1(x2944)+~P1(x2943)+P9(x2943,x2944,x2942)+~P9(x2943,x2944,f39(x2942,x2941))+E(x2941,a4)+E(x2942,a4) % 0.55/0.78 [250]~P1(x2503)+~P1(x2501)+~P1(x2504)+~P10(x2501)+E(x2501,a4)+P2(x2502,a1)+P2(x2503,f44(a4,x2501))+~E(f39(x2501,x2504),f38(x2503,f41(a4))) % 0.55/0.78 %EqnAxiom % 0.55/0.78 [1]E(x11,x11) % 0.55/0.78 [2]E(x22,x21)+~E(x21,x22) % 0.55/0.78 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.55/0.78 [4]~E(x41,x42)+E(f28(x41),f28(x42)) % 0.55/0.78 [5]~E(x51,x52)+E(f37(x51),f37(x52)) % 0.55/0.78 [6]~E(x61,x62)+E(f33(x61,x63,x64),f33(x62,x63,x64)) % 0.55/0.78 [7]~E(x71,x72)+E(f33(x73,x71,x74),f33(x73,x72,x74)) % 0.55/0.78 [8]~E(x81,x82)+E(f33(x83,x84,x81),f33(x83,x84,x82)) % 0.55/0.78 [9]~E(x91,x92)+E(f7(x91),f7(x92)) % 0.55/0.78 [10]~E(x101,x102)+E(f38(x101,x103),f38(x102,x103)) % 0.55/0.78 [11]~E(x111,x112)+E(f38(x113,x111),f38(x113,x112)) % 0.55/0.78 [12]~E(x121,x122)+E(f41(x121),f41(x122)) % 0.55/0.78 [13]~E(x131,x132)+E(f42(x131,x133),f42(x132,x133)) % 0.55/0.78 [14]~E(x141,x142)+E(f42(x143,x141),f42(x143,x142)) % 0.55/0.78 [15]~E(x151,x152)+E(f13(x151,x153,x154),f13(x152,x153,x154)) % 0.55/0.78 [16]~E(x161,x162)+E(f13(x163,x161,x164),f13(x163,x162,x164)) % 0.55/0.78 [17]~E(x171,x172)+E(f13(x173,x174,x171),f13(x173,x174,x172)) % 0.55/0.78 [18]~E(x181,x182)+E(f30(x181),f30(x182)) % 0.55/0.78 [19]~E(x191,x192)+E(f12(x191,x193),f12(x192,x193)) % 0.55/0.78 [20]~E(x201,x202)+E(f12(x203,x201),f12(x203,x202)) % 0.55/0.78 [21]~E(x211,x212)+E(f21(x211),f21(x212)) % 0.55/0.78 [22]~E(x221,x222)+E(f44(x221,x223),f44(x222,x223)) % 0.55/0.78 [23]~E(x231,x232)+E(f44(x233,x231),f44(x233,x232)) % 0.55/0.78 [24]~E(x241,x242)+E(f39(x241,x243),f39(x242,x243)) % 0.55/0.78 [25]~E(x251,x252)+E(f39(x253,x251),f39(x253,x252)) % 0.55/0.78 [26]~E(x261,x262)+E(f34(x261,x263),f34(x262,x263)) % 0.55/0.78 [27]~E(x271,x272)+E(f34(x273,x271),f34(x273,x272)) % 0.55/0.78 [28]~E(x281,x282)+E(f35(x281,x283,x284),f35(x282,x283,x284)) % 0.55/0.78 [29]~E(x291,x292)+E(f35(x293,x291,x294),f35(x293,x292,x294)) % 0.55/0.78 [30]~E(x301,x302)+E(f35(x303,x304,x301),f35(x303,x304,x302)) % 0.55/0.78 [31]~E(x311,x312)+E(f24(x311),f24(x312)) % 0.55/0.78 [32]~E(x321,x322)+E(f23(x321),f23(x322)) % 0.55/0.78 [33]~E(x331,x332)+E(f11(x331,x333),f11(x332,x333)) % 0.55/0.78 [34]~E(x341,x342)+E(f11(x343,x341),f11(x343,x342)) % 0.55/0.78 [35]~E(x351,x352)+E(f9(x351),f9(x352)) % 0.55/0.78 [36]~E(x361,x362)+E(f36(x361,x363),f36(x362,x363)) % 0.55/0.78 [37]~E(x371,x372)+E(f36(x373,x371),f36(x373,x372)) % 0.55/0.78 [38]~E(x381,x382)+E(f32(x381,x383,x384),f32(x382,x383,x384)) % 0.55/0.78 [39]~E(x391,x392)+E(f32(x393,x391,x394),f32(x393,x392,x394)) % 0.55/0.78 [40]~E(x401,x402)+E(f32(x403,x404,x401),f32(x403,x404,x402)) % 0.55/0.78 [41]~E(x411,x412)+E(f8(x411),f8(x412)) % 0.55/0.78 [42]~E(x421,x422)+E(f26(x421,x423),f26(x422,x423)) % 0.55/0.78 [43]~E(x431,x432)+E(f26(x433,x431),f26(x433,x432)) % 0.55/0.78 [44]~E(x441,x442)+E(f40(x441,x443),f40(x442,x443)) % 0.55/0.78 [45]~E(x451,x452)+E(f40(x453,x451),f40(x453,x452)) % 0.55/0.78 [46]~E(x461,x462)+E(f20(x461),f20(x462)) % 0.55/0.78 [47]~E(x471,x472)+E(f14(x471),f14(x472)) % 0.55/0.78 [48]~E(x481,x482)+E(f22(x481,x483),f22(x482,x483)) % 0.55/0.78 [49]~E(x491,x492)+E(f22(x493,x491),f22(x493,x492)) % 0.55/0.78 [50]~E(x501,x502)+E(f31(x501,x503),f31(x502,x503)) % 0.55/0.78 [51]~E(x511,x512)+E(f31(x513,x511),f31(x513,x512)) % 0.55/0.78 [52]~E(x521,x522)+E(f15(x521),f15(x522)) % 0.55/0.78 [53]~E(x531,x532)+E(f29(x531),f29(x532)) % 0.55/0.78 [54]~E(x541,x542)+E(f25(x541),f25(x542)) % 0.55/0.78 [55]~E(x551,x552)+E(f16(x551,x553),f16(x552,x553)) % 0.55/0.78 [56]~E(x561,x562)+E(f16(x563,x561),f16(x563,x562)) % 0.55/0.78 [57]~E(x571,x572)+E(f17(x571,x573,x574),f17(x572,x573,x574)) % 0.55/0.78 [58]~E(x581,x582)+E(f17(x583,x581,x584),f17(x583,x582,x584)) % 0.55/0.78 [59]~E(x591,x592)+E(f17(x593,x594,x591),f17(x593,x594,x592)) % 0.55/0.78 [60]~E(x601,x602)+E(f19(x601,x603),f19(x602,x603)) % 0.55/0.78 [61]~E(x611,x612)+E(f19(x613,x611),f19(x613,x612)) % 0.55/0.78 [62]~E(x621,x622)+E(f18(x621),f18(x622)) % 0.55/0.78 [63]~P1(x631)+P1(x632)+~E(x631,x632) % 0.55/0.78 [64]P2(x642,x643)+~E(x641,x642)+~P2(x641,x643) % 0.55/0.78 [65]P2(x653,x652)+~E(x651,x652)+~P2(x653,x651) % 0.55/0.78 [66]P9(x662,x663,x664)+~E(x661,x662)+~P9(x661,x663,x664) % 0.55/0.78 [67]P9(x673,x672,x674)+~E(x671,x672)+~P9(x673,x671,x674) % 0.55/0.78 [68]P9(x683,x684,x682)+~E(x681,x682)+~P9(x683,x684,x681) % 0.55/0.78 [69]P3(x692,x693)+~E(x691,x692)+~P3(x691,x693) % 0.55/0.78 [70]P3(x703,x702)+~E(x701,x702)+~P3(x703,x701) % 0.55/0.78 [71]P7(x712,x713)+~E(x711,x712)+~P7(x711,x713) % 0.55/0.78 [72]P7(x723,x722)+~E(x721,x722)+~P7(x723,x721) % 0.55/0.78 [73]~P4(x731)+P4(x732)+~E(x731,x732) % 0.55/0.78 [74]~P5(x741)+P5(x742)+~E(x741,x742) % 0.55/0.78 [75]~P10(x751)+P10(x752)+~E(x751,x752) % 0.55/0.78 [76]~P6(x761)+P6(x762)+~E(x761,x762) % 0.55/0.78 [77]~P8(x771)+P8(x772)+~E(x771,x772) % 0.55/0.78 % 0.55/0.78 %------------------------------------------- % 0.55/0.78 cnf(310,plain, % 0.55/0.78 (P2(a43,f37(f28(a1)))), % 0.55/0.78 inference(equality_inference,[],[120])). % 0.55/0.78 cnf(312,plain, % 0.55/0.78 (P2(f41(a43),f37(f28(a1)))), % 0.55/0.78 inference(equality_inference,[],[128])). % 0.55/0.78 cnf(317,plain, % 0.55/0.78 (~P1(x3171)+~P1(x3172)+P4(f44(x3172,x3171))+E(x3171,a4)), % 0.55/0.78 inference(equality_inference,[],[143])). % 0.55/0.78 cnf(340,plain, % 0.55/0.78 (~P9(x3401,x3402,x3403)+~P1(x3403)+~P1(x3402)+P2(x3401,f44(x3402,x3403))+~P1(x3401)+E(x3403,a4)), % 0.55/0.78 inference(equality_inference,[],[260])). % 0.55/0.78 cnf(349,plain, % 0.55/0.78 (P1(f41(a43))), % 0.55/0.78 inference(scs_inference,[],[78,312,97,186,2,152])). % 0.55/0.78 cnf(359,plain, % 0.55/0.78 (P1(f38(a43,a45))), % 0.55/0.78 inference(scs_inference,[],[78,310,312,97,186,2,152,162,163,171,172,176])). % 0.55/0.78 cnf(369,plain, % 0.55/0.78 (E(f38(a43,a45),f41(a43))), % 0.55/0.78 inference(scs_inference,[],[78,105,310,312,97,84,85,95,96,102,86,93,186,2,152,162,163,171,172,176,199,65,70,72,73,74,77,209])). % 0.55/0.78 cnf(386,plain, % 0.55/0.78 (P2(f41(a43),a10)), % 0.55/0.78 inference(scs_inference,[],[78,105,310,312,97,79,80,81,84,85,104,100,95,96,102,103,86,93,186,2,152,162,163,171,172,176,199,65,70,72,73,74,77,209,192,200,317,340,273,215,64,66,67,223])). % 0.55/0.78 cnf(394,plain, % 0.55/0.78 (~E(f38(a43,f41(a45)),f41(a43))), % 0.55/0.78 inference(scs_inference,[],[369,165])). % 0.55/0.78 cnf(427,plain, % 0.55/0.78 (E(f38(a43,f41(a45)),f41(a43))), % 0.55/0.78 inference(scs_inference,[],[369,386,359,349,106,104,99,98,92,312,103,86,81,163,172,176,199,186,171,162,2,70,64,73,65,200,192,317,209])). % 0.55/0.78 cnf(442,plain, % 0.55/0.78 ($false), % 0.55/0.78 inference(scs_inference,[],[427,394]), % 0.55/0.78 ['proof']). % 0.55/0.78 % SZS output end Proof % 0.55/0.78 % Total time :0.100000s %------------------------------------------------------------------------------