%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LAT388+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 10:19:19 EDT 2024 % Result : Theorem 0.59s 0.64s % Output : CNFRefutation 0.59s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : LAT388+4 : 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.12/0.33 % Computer : n023.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 : Fri Jun 21 21:45:24 EDT 2024 % 0.12/0.33 % CPUTime : % 0.20/0.57 start to proof:theBenchmark % 0.59/0.63 %------------------------------------------- % 0.59/0.63 % File :CSE---1.7 % 0.59/0.63 % Problem :theBenchmark % 0.59/0.63 % Transform :cnf % 0.59/0.63 % Format :tptp:raw % 0.59/0.63 % Command :java -jar mcs_scs.jar %d %s % 0.59/0.63 % 0.59/0.63 % Result :Theorem 0.000000s % 0.59/0.63 % Output :CNFRefutation 0.000000s % 0.59/0.63 %------------------------------------------- % 0.59/0.63 %------------------------------------------------------------------------------ % 0.59/0.63 % File : LAT388+4 : TPTP v8.2.0. Released v4.0.0. % 0.59/0.63 % Domain : Lattice Theory % 0.59/0.63 % Problem : Tarski-Knaster fixed point theorem 03_01_05, 03 expansion % 0.59/0.63 % Version : Especial. % 0.59/0.63 % English : % 0.59/0.63 % 0.59/0.63 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 0.59/0.63 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 0.59/0.63 % : [VL+08] Verchinine et al. (2008), On Correctness of Mathematic % 0.59/0.63 % Source : [Pas08] % 0.59/0.63 % Names : tarski_03_01_05.03 [Pas08] % 0.59/0.63 % 0.59/0.63 % Status : Theorem % 0.59/0.63 % Rating : 0.03 v8.1.0, 0.00 v6.1.0, 0.03 v6.0.0, 0.04 v5.4.0, 0.07 v5.3.0, 0.11 v5.2.0, 0.00 v5.1.0, 0.10 v5.0.0, 0.17 v4.1.0, 0.22 v4.0.1, 0.61 v4.0.0 % 0.59/0.63 % Syntax : Number of formulae : 31 ( 0 unt; 10 def) % 0.59/0.63 % Number of atoms : 202 ( 13 equ) % 0.59/0.63 % Maximal formula atoms : 37 ( 6 avg) % 0.59/0.63 % Number of connectives : 172 ( 1 ~; 9 |; 81 &) % 0.59/0.63 % ( 10 <=>; 71 =>; 0 <=; 0 <~>) % 0.59/0.63 % Maximal formula depth : 24 ( 8 avg) % 0.59/0.63 % Maximal term depth : 2 ( 1 avg) % 0.59/0.63 % Number of predicates : 17 ( 15 usr; 1 prp; 0-3 aty) % 0.59/0.63 % Number of functors : 11 ( 11 usr; 6 con; 0-3 aty) % 0.59/0.63 % Number of variables : 86 ( 80 !; 6 ?) % 0.59/0.63 % SPC : FOF_THM_RFO_SEQ % 0.59/0.63 % 0.59/0.63 % Comments : Problem generated by the SAD system [VLP07] % 0.59/0.63 %------------------------------------------------------------------------------ % 0.59/0.63 fof(mSetSort,axiom, % 0.59/0.63 ! [W0] : % 0.59/0.63 ( aSet0(W0) % 0.59/0.63 => $true ) ). % 0.59/0.63 % 0.59/0.63 fof(mElmSort,axiom, % 0.59/0.63 ! [W0] : % 0.59/0.63 ( aElement0(W0) % 0.59/0.63 => $true ) ). % 0.59/0.63 % 0.59/0.63 fof(mEOfElem,axiom, % 0.59/0.63 ! [W0] : % 0.59/0.63 ( aSet0(W0) % 0.59/0.63 => ! [W1] : % 0.59/0.63 ( aElementOf0(W1,W0) % 0.59/0.63 => aElement0(W1) ) ) ). % 0.59/0.63 % 0.59/0.63 fof(mDefEmpty,definition, % 0.59/0.63 ! [W0] : % 0.59/0.63 ( aSet0(W0) % 0.59/0.63 => ( isEmpty0(W0) % 0.59/0.63 <=> ~ ? [W1] : aElementOf0(W1,W0) ) ) ). % 0.59/0.63 % 0.59/0.63 fof(mDefSub,definition, % 0.59/0.63 ! [W0] : % 0.59/0.63 ( aSet0(W0) % 0.59/0.63 => ! [W1] : % 0.59/0.63 ( aSubsetOf0(W1,W0) % 0.59/0.63 <=> ( aSet0(W1) % 0.59/0.63 & ! [W2] : % 0.59/0.64 ( aElementOf0(W2,W1) % 0.59/0.64 => aElementOf0(W2,W0) ) ) ) ) ). % 0.59/0.64 % 0.59/0.64 fof(mLessRel,axiom, % 0.59/0.64 ! [W0,W1] : % 0.59/0.64 ( ( aElement0(W0) % 0.59/0.64 & aElement0(W1) ) % 0.59/0.64 => ( sdtlseqdt0(W0,W1) % 0.59/0.64 => $true ) ) ). % 0.59/0.64 % 0.59/0.64 fof(mARefl,axiom, % 0.59/0.64 ! [W0] : % 0.59/0.64 ( aElement0(W0) % 0.59/0.64 => sdtlseqdt0(W0,W0) ) ). % 0.59/0.64 % 0.59/0.64 fof(mASymm,axiom, % 0.59/0.64 ! [W0,W1] : % 0.59/0.64 ( ( aElement0(W0) % 0.59/0.64 & aElement0(W1) ) % 0.59/0.64 => ( ( sdtlseqdt0(W0,W1) % 0.59/0.64 & sdtlseqdt0(W1,W0) ) % 0.59/0.64 => W0 = W1 ) ) ). % 0.59/0.64 % 0.59/0.64 fof(mTrans,axiom, % 0.59/0.64 ! [W0,W1,W2] : % 0.59/0.64 ( ( aElement0(W0) % 0.59/0.64 & aElement0(W1) % 0.59/0.64 & aElement0(W2) ) % 0.59/0.64 => ( ( sdtlseqdt0(W0,W1) % 0.59/0.64 & sdtlseqdt0(W1,W2) ) % 0.59/0.64 => sdtlseqdt0(W0,W2) ) ) ). % 0.59/0.64 % 0.59/0.64 fof(mDefLB,definition, % 0.59/0.64 ! [W0] : % 0.59/0.64 ( aSet0(W0) % 0.59/0.64 => ! [W1] : % 0.59/0.64 ( aSubsetOf0(W1,W0) % 0.59/0.64 => ! [W2] : % 0.59/0.64 ( aLowerBoundOfIn0(W2,W1,W0) % 0.59/0.64 <=> ( aElementOf0(W2,W0) % 0.59/0.64 & ! [W3] : % 0.59/0.64 ( aElementOf0(W3,W1) % 0.59/0.64 => sdtlseqdt0(W2,W3) ) ) ) ) ) ). % 0.59/0.64 % 0.59/0.64 fof(mDefUB,definition, % 0.59/0.64 ! [W0] : % 0.59/0.64 ( aSet0(W0) % 0.59/0.64 => ! [W1] : % 0.59/0.64 ( aSubsetOf0(W1,W0) % 0.59/0.64 => ! [W2] : % 0.59/0.64 ( aUpperBoundOfIn0(W2,W1,W0) % 0.59/0.64 <=> ( aElementOf0(W2,W0) % 0.59/0.64 & ! [W3] : % 0.59/0.64 ( aElementOf0(W3,W1) % 0.59/0.64 => sdtlseqdt0(W3,W2) ) ) ) ) ) ). % 0.59/0.64 % 0.59/0.64 fof(mDefInf,definition, % 0.59/0.64 ! [W0] : % 0.59/0.64 ( aSet0(W0) % 0.59/0.64 => ! [W1] : % 0.59/0.64 ( aSubsetOf0(W1,W0) % 0.59/0.64 => ! [W2] : % 0.59/0.64 ( aInfimumOfIn0(W2,W1,W0) % 0.59/0.64 <=> ( aElementOf0(W2,W0) % 0.59/0.64 & aLowerBoundOfIn0(W2,W1,W0) % 0.59/0.64 & ! [W3] : % 0.59/0.64 ( aLowerBoundOfIn0(W3,W1,W0) % 0.59/0.64 => sdtlseqdt0(W3,W2) ) ) ) ) ) ). % 0.59/0.64 % 0.59/0.64 fof(mDefSup,definition, % 0.59/0.64 ! [W0] : % 0.59/0.64 ( aSet0(W0) % 0.59/0.64 => ! [W1] : % 0.59/0.64 ( aSubsetOf0(W1,W0) % 0.59/0.64 => ! [W2] : % 0.59/0.64 ( aSupremumOfIn0(W2,W1,W0) % 0.59/0.64 <=> ( aElementOf0(W2,W0) % 0.59/0.64 & aUpperBoundOfIn0(W2,W1,W0) % 0.59/0.64 & ! [W3] : % 0.59/0.64 ( aUpperBoundOfIn0(W3,W1,W0) % 0.59/0.64 => sdtlseqdt0(W2,W3) ) ) ) ) ) ). % 0.59/0.64 % 0.59/0.64 fof(mSupUn,axiom, % 0.59/0.64 ! [W0] : % 0.59/0.64 ( aSet0(W0) % 0.59/0.64 => ! [W1] : % 0.59/0.64 ( aSubsetOf0(W1,W0) % 0.59/0.64 => ! [W2,W3] : % 0.59/0.64 ( ( aSupremumOfIn0(W2,W1,W0) % 0.59/0.64 & aSupremumOfIn0(W3,W1,W0) ) % 0.59/0.64 => W2 = W3 ) ) ) ). % 0.59/0.64 % 0.59/0.64 fof(mInfUn,axiom, % 0.59/0.64 ! [W0] : % 0.59/0.64 ( aSet0(W0) % 0.59/0.64 => ! [W1] : % 0.59/0.64 ( aSubsetOf0(W1,W0) % 0.59/0.64 => ! [W2,W3] : % 0.59/0.64 ( ( aInfimumOfIn0(W2,W1,W0) % 0.59/0.64 & aInfimumOfIn0(W3,W1,W0) ) % 0.59/0.64 => W2 = W3 ) ) ) ). % 0.59/0.64 % 0.59/0.64 fof(mDefCLat,definition, % 0.59/0.64 ! [W0] : % 0.59/0.64 ( aCompleteLattice0(W0) % 0.59/0.64 <=> ( aSet0(W0) % 0.59/0.64 & ! [W1] : % 0.59/0.64 ( aSubsetOf0(W1,W0) % 0.59/0.64 => ? [W2] : % 0.59/0.64 ( aInfimumOfIn0(W2,W1,W0) % 0.59/0.64 & ? [W3] : aSupremumOfIn0(W3,W1,W0) ) ) ) ) ). % 0.59/0.64 % 0.59/0.64 fof(mConMap,axiom, % 0.59/0.64 ! [W0] : % 0.59/0.64 ( aFunction0(W0) % 0.59/0.64 => $true ) ). % 0.59/0.64 % 0.59/0.64 fof(mDomSort,axiom, % 0.59/0.64 ! [W0] : % 0.59/0.64 ( aFunction0(W0) % 0.59/0.64 => aSet0(szDzozmdt0(W0)) ) ). % 0.59/0.64 % 0.59/0.64 fof(mRanSort,axiom, % 0.59/0.64 ! [W0] : % 0.59/0.64 ( aFunction0(W0) % 0.59/0.64 => aSet0(szRzazndt0(W0)) ) ). % 0.59/0.64 % 0.59/0.64 fof(mDefDom,definition, % 0.59/0.64 ! [W0,W1] : % 0.59/0.64 ( ( aFunction0(W0) % 0.59/0.64 & aSet0(W1) ) % 0.59/0.64 => ( isOn0(W0,W1) % 0.59/0.64 <=> ( szDzozmdt0(W0) = szRzazndt0(W0) % 0.59/0.64 & szRzazndt0(W0) = W1 ) ) ) ). % 0.59/0.64 % 0.59/0.64 fof(mImgSort,axiom, % 0.59/0.64 ! [W0] : % 0.59/0.64 ( aFunction0(W0) % 0.59/0.64 => ! [W1] : % 0.59/0.64 ( aElementOf0(W1,szDzozmdt0(W0)) % 0.59/0.64 => aElementOf0(sdtlpdtrp0(W0,W1),szRzazndt0(W0)) ) ) ). % 0.59/0.64 % 0.59/0.64 fof(mDefFix,definition, % 0.59/0.64 ! [W0] : % 0.59/0.64 ( aFunction0(W0) % 0.59/0.64 => ! [W1] : % 0.59/0.64 ( aFixedPointOf0(W1,W0) % 0.59/0.64 <=> ( aElementOf0(W1,szDzozmdt0(W0)) % 0.59/0.64 & sdtlpdtrp0(W0,W1) = W1 ) ) ) ). % 0.59/0.64 % 0.59/0.64 fof(mDefMonot,definition, % 0.59/0.64 ! [W0] : % 0.59/0.64 ( aFunction0(W0) % 0.59/0.64 => ( isMonotone0(W0) % 0.59/0.64 <=> ! [W1,W2] : % 0.59/0.64 ( ( aElementOf0(W1,szDzozmdt0(W0)) % 0.59/0.64 & aElementOf0(W2,szDzozmdt0(W0)) ) % 0.59/0.64 => ( sdtlseqdt0(W1,W2) % 0.59/0.64 => sdtlseqdt0(sdtlpdtrp0(W0,W1),sdtlpdtrp0(W0,W2)) ) ) ) ) ). % 0.59/0.64 % 0.59/0.64 fof(m__1123,hypothesis, % 0.59/0.64 ( aSet0(xU) % 0.59/0.64 & ! [W0] : % 0.59/0.64 ( ( ( aSet0(W0) % 0.59/0.64 & ! [W1] : % 0.59/0.64 ( aElementOf0(W1,W0) % 0.59/0.64 => aElementOf0(W1,xU) ) ) % 0.59/0.64 | aSubsetOf0(W0,xU) ) % 0.59/0.64 => ? [W1] : % 0.59/0.64 ( aElementOf0(W1,xU) % 0.59/0.64 & aElementOf0(W1,xU) % 0.59/0.64 & ! [W2] : % 0.59/0.64 ( aElementOf0(W2,W0) % 0.59/0.64 => sdtlseqdt0(W1,W2) ) % 0.59/0.64 & aLowerBoundOfIn0(W1,W0,xU) % 0.59/0.64 & ! [W2] : % 0.59/0.64 ( ( ( aElementOf0(W2,xU) % 0.59/0.64 & ! [W3] : % 0.59/0.64 ( aElementOf0(W3,W0) % 0.59/0.64 => sdtlseqdt0(W2,W3) ) ) % 0.59/0.64 | aLowerBoundOfIn0(W2,W0,xU) ) % 0.59/0.64 => sdtlseqdt0(W2,W1) ) % 0.59/0.64 & aInfimumOfIn0(W1,W0,xU) % 0.59/0.64 & ? [W2] : % 0.59/0.64 ( aElementOf0(W2,xU) % 0.59/0.64 & aElementOf0(W2,xU) % 0.59/0.64 & ! [W3] : % 0.59/0.64 ( aElementOf0(W3,W0) % 0.59/0.64 => sdtlseqdt0(W3,W2) ) % 0.59/0.64 & aUpperBoundOfIn0(W2,W0,xU) % 0.59/0.64 & ! [W3] : % 0.59/0.64 ( ( ( aElementOf0(W3,xU) % 0.59/0.64 & ! [W4] : % 0.59/0.64 ( aElementOf0(W4,W0) % 0.59/0.64 => sdtlseqdt0(W4,W3) ) ) % 0.59/0.64 | aUpperBoundOfIn0(W3,W0,xU) ) % 0.59/0.64 => sdtlseqdt0(W2,W3) ) % 0.59/0.64 & aSupremumOfIn0(W2,W0,xU) ) ) ) % 0.59/0.64 & aCompleteLattice0(xU) % 0.59/0.64 & aFunction0(xf) % 0.59/0.64 & ! [W0,W1] : % 0.59/0.64 ( ( aElementOf0(W0,szDzozmdt0(xf)) % 0.59/0.64 & aElementOf0(W1,szDzozmdt0(xf)) ) % 0.59/0.64 => ( sdtlseqdt0(W0,W1) % 0.59/0.64 => sdtlseqdt0(sdtlpdtrp0(xf,W0),sdtlpdtrp0(xf,W1)) ) ) % 0.59/0.64 & isMonotone0(xf) % 0.59/0.64 & szDzozmdt0(xf) = szRzazndt0(xf) % 0.59/0.64 & szRzazndt0(xf) = xU % 0.59/0.64 & isOn0(xf,xU) ) ). % 0.59/0.64 % 0.59/0.64 fof(m__1144,hypothesis, % 0.59/0.64 ( aSet0(xS) % 0.59/0.64 & ! [W0] : % 0.59/0.64 ( ( aElementOf0(W0,xS) % 0.59/0.64 => ( aElementOf0(W0,szDzozmdt0(xf)) % 0.59/0.64 & sdtlpdtrp0(xf,W0) = W0 % 0.59/0.64 & aFixedPointOf0(W0,xf) ) ) % 0.59/0.64 & ( ( ( aElementOf0(W0,szDzozmdt0(xf)) % 0.59/0.64 & sdtlpdtrp0(xf,W0) = W0 ) % 0.59/0.64 | aFixedPointOf0(W0,xf) ) % 0.59/0.64 => aElementOf0(W0,xS) ) ) % 0.59/0.64 & xS = cS1142(xf) ) ). % 0.59/0.64 % 0.59/0.64 fof(m__1173,hypothesis, % 0.59/0.64 ( aSet0(xT) % 0.59/0.64 & ! [W0] : % 0.59/0.64 ( aElementOf0(W0,xT) % 0.59/0.64 => aElementOf0(W0,xS) ) % 0.59/0.64 & aSubsetOf0(xT,xS) ) ). % 0.59/0.64 % 0.59/0.64 fof(m__1244,hypothesis, % 0.59/0.64 ( aSet0(xP) % 0.59/0.64 & ! [W0] : % 0.59/0.64 ( ( aElementOf0(W0,xP) % 0.59/0.64 => ( aElementOf0(W0,xU) % 0.59/0.64 & sdtlseqdt0(sdtlpdtrp0(xf,W0),W0) % 0.59/0.64 & ! [W1] : % 0.59/0.64 ( aElementOf0(W1,xT) % 0.59/0.64 => sdtlseqdt0(W1,W0) ) % 0.59/0.64 & aUpperBoundOfIn0(W0,xT,xU) ) ) % 0.59/0.64 & ( ( aElementOf0(W0,xU) % 0.59/0.64 & sdtlseqdt0(sdtlpdtrp0(xf,W0),W0) % 0.59/0.64 & ( ! [W1] : % 0.59/0.64 ( aElementOf0(W1,xT) % 0.59/0.64 => sdtlseqdt0(W1,W0) ) % 0.59/0.64 | aUpperBoundOfIn0(W0,xT,xU) ) ) % 0.59/0.64 => aElementOf0(W0,xP) ) ) % 0.59/0.64 & xP = cS1241(xU,xf,xT) ) ). % 0.59/0.64 % 0.59/0.64 fof(m__1261,hypothesis, % 0.59/0.64 ( aElementOf0(xp,xU) % 0.59/0.64 & aElementOf0(xp,xU) % 0.59/0.64 & ! [W0] : % 0.59/0.64 ( aElementOf0(W0,xP) % 0.59/0.64 => sdtlseqdt0(xp,W0) ) % 0.59/0.64 & aLowerBoundOfIn0(xp,xP,xU) % 0.59/0.64 & ! [W0] : % 0.59/0.64 ( ( ( aElementOf0(W0,xU) % 0.59/0.64 & ! [W1] : % 0.59/0.64 ( aElementOf0(W1,xP) % 0.59/0.64 => sdtlseqdt0(W0,W1) ) ) % 0.59/0.64 | aLowerBoundOfIn0(W0,xP,xU) ) % 0.59/0.64 => sdtlseqdt0(W0,xp) ) % 0.59/0.64 & aInfimumOfIn0(xp,xP,xU) ) ). % 0.59/0.64 % 0.59/0.64 fof(m__1299,hypothesis, % 0.59/0.64 ( ! [W0] : % 0.59/0.64 ( aElementOf0(W0,xP) % 0.59/0.64 => sdtlseqdt0(sdtlpdtrp0(xf,xp),W0) ) % 0.59/0.64 & aLowerBoundOfIn0(sdtlpdtrp0(xf,xp),xP,xU) % 0.59/0.64 & ! [W0] : % 0.59/0.64 ( aElementOf0(W0,xT) % 0.59/0.64 => sdtlseqdt0(W0,sdtlpdtrp0(xf,xp)) ) % 0.59/0.64 & aUpperBoundOfIn0(sdtlpdtrp0(xf,xp),xT,xU) ) ). % 0.59/0.64 % 0.59/0.64 fof(m__1330,hypothesis, % 0.59/0.64 ( aElementOf0(xp,szDzozmdt0(xf)) % 0.59/0.64 & sdtlpdtrp0(xf,xp) = xp % 0.59/0.64 & aFixedPointOf0(xp,xf) % 0.59/0.64 & ! [W0] : % 0.59/0.64 ( aElementOf0(W0,xT) % 0.59/0.64 => sdtlseqdt0(W0,xp) ) % 0.59/0.64 & aUpperBoundOfIn0(xp,xT,xS) % 0.59/0.64 & ! [W0] : % 0.59/0.64 ( ( ( aElementOf0(W0,xS) % 0.59/0.64 & ! [W1] : % 0.59/0.64 ( aElementOf0(W1,xT) % 0.59/0.64 => sdtlseqdt0(W1,W0) ) ) % 0.59/0.64 | aUpperBoundOfIn0(W0,xT,xS) ) % 0.59/0.64 => sdtlseqdt0(xp,W0) ) % 0.59/0.64 & aSupremumOfIn0(xp,xT,xS) ) ). % 0.59/0.64 % 0.59/0.64 fof(m__,conjecture, % 0.59/0.64 ? [W0] : % 0.59/0.64 ( ( aElementOf0(W0,xS) % 0.59/0.64 & ( ( aElementOf0(W0,xS) % 0.59/0.64 & ! [W1] : % 0.59/0.64 ( aElementOf0(W1,xT) % 0.59/0.64 => sdtlseqdt0(W1,W0) ) ) % 0.59/0.64 | aUpperBoundOfIn0(W0,xT,xS) ) % 0.59/0.64 & ! [W1] : % 0.59/0.64 ( ( aElementOf0(W1,xS) % 0.59/0.64 & ! [W2] : % 0.59/0.64 ( aElementOf0(W2,xT) % 0.59/0.64 => sdtlseqdt0(W2,W1) ) % 0.59/0.64 & aUpperBoundOfIn0(W1,xT,xS) ) % 0.59/0.64 => sdtlseqdt0(W0,W1) ) ) % 0.59/0.64 | aSupremumOfIn0(W0,xT,xS) ) ). % 0.59/0.64 % 0.59/0.64 %------------------------------------------------------------------------------ % 0.59/0.64 %------------------------------------------- % 0.59/0.64 % Proof found % 0.59/0.64 % SZS status Theorem for theBenchmark % 0.59/0.64 % SZS output start Proof % 0.59/0.64 %ClaNum:200(EqnAxiom:74) % 0.59/0.64 %VarNum:585(SingletonVarNum:185) % 0.59/0.64 %MaxLitNum:6 % 0.59/0.64 %MaxfuncDepth:2 % 0.59/0.64 %SharedTerms:34 % 0.59/0.64 %goalClause: 98 137 148 149 152 154 159 162 163 171 177 179 183 % 0.59/0.64 %singleGoalClaCount:1 % 0.59/0.64 [77]P1(a30) % 0.59/0.64 [78]P1(a3) % 0.59/0.64 [79]P1(a31) % 0.59/0.64 [80]P1(a29) % 0.59/0.64 [81]P2(a30) % 0.59/0.64 [82]P3(a1) % 0.59/0.64 [83]P9(a1) % 0.59/0.64 [86]P4(a32,a30) % 0.59/0.64 [87]P10(a31,a3) % 0.59/0.64 [88]P15(a1,a30) % 0.59/0.64 [89]P6(a32,a1) % 0.59/0.64 [92]P7(a32,a29,a30) % 0.59/0.64 [93]P11(a32,a31,a3) % 0.59/0.64 [94]P8(a32,a29,a30) % 0.59/0.64 [95]P12(a32,a31,a3) % 0.59/0.64 [75]E(f2(a1),a3) % 0.59/0.64 [76]E(f4(a1),a30) % 0.59/0.64 [84]E(f5(a1),f4(a1)) % 0.59/0.64 [85]E(f6(a1,a32),a32) % 0.59/0.64 [90]P4(a32,f5(a1)) % 0.59/0.64 [91]E(f7(a30,a1,a31),a29) % 0.59/0.64 [96]P7(f6(a1,a32),a29,a30) % 0.59/0.64 [97]P11(f6(a1,a32),a31,a30) % 0.59/0.64 [98]~P12(x981,a31,a3) % 0.59/0.64 [99]~P2(x991)+P1(x991) % 0.59/0.64 [102]~P5(x1021)+P16(x1021,x1021) % 0.59/0.64 [103]P13(x1031)+~P10(x1031,a30) % 0.59/0.64 [109]~P4(x1091,a29)+P4(x1091,a30) % 0.59/0.64 [110]~P4(x1101,a31)+P4(x1101,a3) % 0.59/0.64 [111]~P6(x1111,a1)+P4(x1111,a3) % 0.59/0.64 [112]~P4(x1121,a31)+P16(x1121,a32) % 0.59/0.64 [113]~P4(x1131,a3)+P6(x1131,a1) % 0.59/0.64 [114]~P4(x1141,a29)+P16(a32,x1141) % 0.59/0.64 [150]~P4(x1501,a29)+P11(x1501,a31,a30) % 0.59/0.64 [160]P16(x1601,a32)+~P7(x1601,a29,a30) % 0.59/0.64 [161]P16(a32,x1611)+~P11(x1611,a31,a3) % 0.59/0.64 [100]~P3(x1001)+P1(f5(x1001)) % 0.59/0.64 [101]~P3(x1011)+P1(f4(x1011)) % 0.59/0.64 [104]~P13(x1041)+P4(f8(x1041),a30) % 0.59/0.64 [105]~P13(x1051)+P4(f17(x1051),a30) % 0.59/0.64 [115]~P4(x1151,a3)+E(f6(a1,x1151),x1151) % 0.59/0.64 [119]~P4(x1191,a3)+P4(x1191,f5(a1)) % 0.59/0.64 [133]~P4(x1331,a31)+P16(x1331,f6(a1,a32)) % 0.59/0.64 [134]~P4(x1341,a29)+P16(f6(a1,a32),x1341) % 0.59/0.64 [136]~P4(x1361,a29)+P16(f6(a1,x1361),x1361) % 0.59/0.64 [142]~P13(x1421)+P7(f8(x1421),x1421,a30) % 0.59/0.64 [143]~P13(x1431)+P11(f17(x1431),x1431,a30) % 0.59/0.64 [144]~P13(x1441)+P8(f8(x1441),x1441,a30) % 0.59/0.64 [145]~P13(x1451)+P12(f17(x1451),x1451,a30) % 0.59/0.64 [106]~P1(x1061)+P14(x1061)+P4(f18(x1061),x1061) % 0.59/0.64 [107]~P1(x1071)+P2(x1071)+P10(f20(x1071),x1071) % 0.59/0.64 [108]~P1(x1081)+P13(x1081)+P4(f9(x1081),x1081) % 0.59/0.64 [120]~P3(x1201)+P9(x1201)+P4(f10(x1201),f5(x1201)) % 0.59/0.64 [121]~P3(x1211)+P9(x1211)+P4(f11(x1211),f5(x1211)) % 0.59/0.64 [122]~P3(x1221)+P9(x1221)+P16(f10(x1221),f11(x1221)) % 0.59/0.64 [123]~P1(x1231)+P13(x1231)+~P4(f9(x1231),a30) % 0.59/0.64 [131]~P4(x1311,a30)+P16(x1311,a32)+P4(f12(x1311),a29) % 0.59/0.64 [132]~P4(x1321,a3)+P16(a32,x1321)+P4(f14(x1321),a31) % 0.59/0.65 [137]~P4(x1371,a3)+P4(f16(x1371),a3)+P4(f15(x1371),a31) % 0.59/0.65 [138]P4(x1381,a3)+~E(f6(a1,x1381),x1381)+~P4(x1381,f5(a1)) % 0.59/0.65 [140]~P4(x1401,a30)+~P16(x1401,f12(x1401))+P16(x1401,a32) % 0.59/0.65 [141]~P4(x1411,a3)+~P16(f14(x1411),x1411)+P16(a32,x1411) % 0.59/0.65 [148]~P4(x1481,a3)+~P16(x1481,f16(x1481))+P4(f15(x1481),a31) % 0.59/0.65 [149]~P4(x1491,a3)+~P16(f15(x1491),x1491)+P4(f16(x1491),a3) % 0.59/0.65 [154]~P16(x1541,f16(x1541))+~P16(f15(x1541),x1541)+~P4(x1541,a3) % 0.59/0.65 [162]~P4(x1621,a3)+P11(f16(x1621),a31,a3)+P4(f15(x1621),a31) % 0.59/0.65 [163]~P4(x1631,a3)+~P16(f15(x1631),x1631)+P11(f16(x1631),a31,a3) % 0.59/0.65 [171]~P4(x1711,a3)+~P11(x1711,a31,a3)+P4(f16(x1711),a3) % 0.59/0.65 [177]~P16(x1771,f16(x1771))+~P4(x1771,a3)+~P11(x1771,a31,a3) % 0.59/0.65 [183]~P4(x1831,a3)+~P11(x1831,a31,a3)+P11(f16(x1831),a31,a3) % 0.59/0.65 [182]~P3(x1821)+P9(x1821)+~P16(f6(x1821,f10(x1821)),f6(x1821,f11(x1821))) % 0.59/0.65 [116]~P10(x1161,x1162)+P1(x1161)+~P1(x1162) % 0.59/0.65 [117]~P4(x1171,x1172)+P5(x1171)+~P1(x1172) % 0.59/0.65 [118]~P14(x1181)+~P1(x1181)+~P4(x1182,x1181) % 0.59/0.65 [135]P16(x1351,x1352)+~P4(x1352,a29)+~P4(x1351,a31) % 0.59/0.65 [125]~P3(x1251)+~P6(x1252,x1251)+E(f6(x1251,x1252),x1252) % 0.59/0.65 [128]~P3(x1282)+~P6(x1281,x1282)+P4(x1281,f5(x1282)) % 0.59/0.65 [129]~P13(x1292)+~P4(x1291,x1292)+P16(x1291,f17(x1292)) % 0.59/0.65 [130]~P13(x1301)+~P4(x1302,x1301)+P16(f8(x1301),x1302) % 0.59/0.65 [155]~P3(x1551)+~P4(x1552,f5(x1551))+P4(f6(x1551,x1552),f4(x1551)) % 0.59/0.65 [164]~P2(x1641)+~P10(x1642,x1641)+P8(f23(x1641,x1642),x1642,x1641) % 0.59/0.65 [165]~P2(x1651)+~P10(x1652,x1651)+P12(f28(x1651,x1652),x1652,x1651) % 0.59/0.65 [167]~P13(x1672)+~P7(x1671,x1672,a30)+P16(x1671,f8(x1672)) % 0.59/0.65 [168]~P13(x1681)+~P11(x1682,x1681,a30)+P16(f17(x1681),x1682) % 0.59/0.65 [166]~P4(x1661,a30)+P4(x1661,a29)+~P16(f6(a1,x1661),x1661)+P4(f13(x1661),a31) % 0.59/0.65 [172]~P4(x1721,a30)+~P16(f13(x1721),x1721)+P4(x1721,a29)+~P16(f6(a1,x1721),x1721) % 0.59/0.65 [187]~P4(x1871,a30)+P4(x1871,a29)+~P16(f6(a1,x1871),x1871)+~P11(x1871,a31,a30) % 0.59/0.65 [124]~P1(x1242)+~P3(x1241)+~P15(x1241,x1242)+E(f4(x1241),x1242) % 0.59/0.65 [126]~P3(x1261)+~P15(x1261,x1262)+~P1(x1262)+E(f5(x1261),f4(x1261)) % 0.59/0.65 [147]~P1(x1471)+~P1(x1472)+P10(x1471,x1472)+P4(f21(x1472,x1471),x1471) % 0.59/0.65 [151]~P3(x1512)+P6(x1511,x1512)+~E(f6(x1512,x1511),x1511)+~P4(x1511,f5(x1512)) % 0.59/0.65 [152]~P4(x1522,a3)+~P4(x1521,a31)+P16(x1521,f16(x1522))+P4(f15(x1522),a31) % 0.59/0.65 [156]~P13(x1562)+P4(f19(x1562,x1561),x1562)+~P4(x1561,a30)+P16(x1561,f8(x1562)) % 0.59/0.65 [157]~P13(x1571)+P4(f22(x1571,x1572),x1571)+~P4(x1572,a30)+P16(f17(x1571),x1572) % 0.59/0.65 [158]~P1(x1581)+~P1(x1582)+P10(x1581,x1582)+~P4(f21(x1582,x1581),x1582) % 0.59/0.65 [159]~P4(x1592,a3)+~P4(x1591,a31)+~P16(f15(x1592),x1592)+P16(x1591,f16(x1592)) % 0.59/0.65 [169]~P13(x1692)+~P4(x1691,a30)+~P16(x1691,f19(x1692,x1691))+P16(x1691,f8(x1692)) % 0.59/0.65 [170]~P13(x1701)+~P4(x1702,a30)+~P16(f22(x1701,x1702),x1702)+P16(f17(x1701),x1702) % 0.59/0.65 [178]~P16(x1781,x1782)+~P4(x1782,f5(a1))+~P4(x1781,f5(a1))+P16(f6(a1,x1781),f6(a1,x1782)) % 0.59/0.65 [179]~P4(x1792,a3)+~P4(x1791,a31)+P16(x1791,f16(x1792))+~P11(x1792,a31,a3) % 0.59/0.65 [146]~P1(x1462)+~P10(x1463,x1462)+P4(x1461,x1462)+~P4(x1461,x1463) % 0.59/0.65 [173]~P1(x1732)+~P7(x1731,x1733,x1732)+P4(x1731,x1732)+~P10(x1733,x1732) % 0.59/0.65 [174]~P1(x1742)+~P11(x1741,x1743,x1742)+P4(x1741,x1742)+~P10(x1743,x1742) % 0.59/0.65 [175]~P1(x1752)+~P8(x1751,x1753,x1752)+P4(x1751,x1752)+~P10(x1753,x1752) % 0.59/0.65 [176]~P1(x1762)+~P12(x1761,x1763,x1762)+P4(x1761,x1762)+~P10(x1763,x1762) % 0.59/0.65 [185]~P1(x1853)+~P10(x1852,x1853)+~P8(x1851,x1852,x1853)+P7(x1851,x1852,x1853) % 0.59/0.65 [186]~P1(x1863)+~P10(x1862,x1863)+~P12(x1861,x1862,x1863)+P11(x1861,x1862,x1863) % 0.59/0.65 [188]~P1(x1881)+P2(x1881)+~P8(x1882,f20(x1881),x1881)+~P12(x1883,f20(x1881),x1881) % 0.59/0.65 [139]~P5(x1392)+~P5(x1391)+~P16(x1392,x1391)+~P16(x1391,x1392)+E(x1391,x1392) % 0.59/0.65 [127]~P1(x1272)+~P3(x1271)+P15(x1271,x1272)+~E(f4(x1271),x1272)+~E(f5(x1271),f4(x1271)) % 0.59/0.65 [193]~P1(x1933)+~P4(x1931,x1933)+~P10(x1932,x1933)+P7(x1931,x1932,x1933)+P4(f24(x1933,x1932,x1931),x1932) % 0.59/0.65 [194]~P1(x1943)+~P4(x1941,x1943)+~P10(x1942,x1943)+P11(x1941,x1942,x1943)+P4(f25(x1943,x1942,x1941),x1942) % 0.59/0.65 [195]~P1(x1953)+~P4(x1951,x1953)+~P10(x1952,x1953)+P7(x1951,x1952,x1953)+~P16(x1951,f24(x1953,x1952,x1951)) % 0.59/0.65 [196]~P1(x1963)+~P4(x1961,x1963)+~P10(x1962,x1963)+P11(x1961,x1962,x1963)+~P16(f25(x1963,x1962,x1961),x1961) % 0.59/0.65 [180]~P10(x1804,x1803)+~P7(x1801,x1804,x1803)+P16(x1801,x1802)+~P4(x1802,x1804)+~P1(x1803) % 0.59/0.65 [181]~P10(x1814,x1813)+~P11(x1812,x1814,x1813)+P16(x1811,x1812)+~P4(x1811,x1814)+~P1(x1813) % 0.59/0.65 [189]~P8(x1892,x1894,x1893)+~P8(x1891,x1894,x1893)+E(x1891,x1892)+~P10(x1894,x1893)+~P1(x1893) % 0.59/0.65 [190]~P12(x1902,x1904,x1903)+~P12(x1901,x1904,x1903)+E(x1901,x1902)+~P10(x1904,x1903)+~P1(x1903) % 0.59/0.65 [191]~P11(x1912,x1914,x1913)+~P12(x1911,x1914,x1913)+P16(x1911,x1912)+~P10(x1914,x1913)+~P1(x1913) % 0.59/0.65 [192]~P7(x1921,x1924,x1923)+~P8(x1922,x1924,x1923)+P16(x1921,x1922)+~P10(x1924,x1923)+~P1(x1923) % 0.59/0.65 [153]~P5(x1532)+~P5(x1531)+~P16(x1533,x1532)+~P16(x1531,x1533)+P16(x1531,x1532)+~P5(x1533) % 0.59/0.65 [184]~P3(x1841)+~P9(x1841)+~P16(x1842,x1843)+~P4(x1843,f5(x1841))+~P4(x1842,f5(x1841))+P16(f6(x1841,x1842),f6(x1841,x1843)) % 0.59/0.65 [197]~P1(x1973)+~P4(x1971,x1973)+~P10(x1972,x1973)+~P7(x1971,x1972,x1973)+P8(x1971,x1972,x1973)+P7(f26(x1973,x1972,x1971),x1972,x1973) % 0.59/0.65 [198]~P1(x1983)+~P4(x1981,x1983)+~P10(x1982,x1983)+~P11(x1981,x1982,x1983)+P12(x1981,x1982,x1983)+P11(f27(x1983,x1982,x1981),x1982,x1983) % 0.59/0.65 [199]~P1(x1993)+~P4(x1991,x1993)+~P10(x1992,x1993)+~P11(x1991,x1992,x1993)+P12(x1991,x1992,x1993)+~P16(x1991,f27(x1993,x1992,x1991)) % 0.59/0.65 [200]~P1(x2003)+~P4(x2001,x2003)+~P10(x2002,x2003)+~P7(x2001,x2002,x2003)+P8(x2001,x2002,x2003)+~P16(f26(x2003,x2002,x2001),x2001) % 0.59/0.65 %EqnAxiom % 0.59/0.65 [1]E(x11,x11) % 0.59/0.65 [2]E(x22,x21)+~E(x21,x22) % 0.59/0.65 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.59/0.65 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 0.59/0.65 [5]~E(x51,x52)+E(f4(x51),f4(x52)) % 0.59/0.65 [6]~E(x61,x62)+E(f5(x61),f5(x62)) % 0.59/0.65 [7]~E(x71,x72)+E(f26(x71,x73,x74),f26(x72,x73,x74)) % 0.59/0.65 [8]~E(x81,x82)+E(f26(x83,x81,x84),f26(x83,x82,x84)) % 0.59/0.65 [9]~E(x91,x92)+E(f26(x93,x94,x91),f26(x93,x94,x92)) % 0.59/0.65 [10]~E(x101,x102)+E(f6(x101,x103),f6(x102,x103)) % 0.59/0.65 [11]~E(x111,x112)+E(f6(x113,x111),f6(x113,x112)) % 0.59/0.65 [12]~E(x121,x122)+E(f24(x121,x123,x124),f24(x122,x123,x124)) % 0.59/0.65 [13]~E(x131,x132)+E(f24(x133,x131,x134),f24(x133,x132,x134)) % 0.59/0.65 [14]~E(x141,x142)+E(f24(x143,x144,x141),f24(x143,x144,x142)) % 0.59/0.65 [15]~E(x151,x152)+E(f7(x151,x153,x154),f7(x152,x153,x154)) % 0.59/0.65 [16]~E(x161,x162)+E(f7(x163,x161,x164),f7(x163,x162,x164)) % 0.59/0.65 [17]~E(x171,x172)+E(f7(x173,x174,x171),f7(x173,x174,x172)) % 0.59/0.65 [18]~E(x181,x182)+E(f16(x181),f16(x182)) % 0.59/0.65 [19]~E(x191,x192)+E(f13(x191),f13(x192)) % 0.59/0.65 [20]~E(x201,x202)+E(f20(x201),f20(x202)) % 0.59/0.65 [21]~E(x211,x212)+E(f27(x211,x213,x214),f27(x212,x213,x214)) % 0.59/0.65 [22]~E(x221,x222)+E(f27(x223,x221,x224),f27(x223,x222,x224)) % 0.59/0.65 [23]~E(x231,x232)+E(f27(x233,x234,x231),f27(x233,x234,x232)) % 0.59/0.65 [24]~E(x241,x242)+E(f8(x241),f8(x242)) % 0.59/0.65 [25]~E(x251,x252)+E(f17(x251),f17(x252)) % 0.59/0.65 [26]~E(x261,x262)+E(f18(x261),f18(x262)) % 0.59/0.65 [27]~E(x271,x272)+E(f15(x271),f15(x272)) % 0.59/0.65 [28]~E(x281,x282)+E(f9(x281),f9(x282)) % 0.59/0.65 [29]~E(x291,x292)+E(f11(x291),f11(x292)) % 0.59/0.65 [30]~E(x301,x302)+E(f25(x301,x303,x304),f25(x302,x303,x304)) % 0.59/0.65 [31]~E(x311,x312)+E(f25(x313,x311,x314),f25(x313,x312,x314)) % 0.59/0.65 [32]~E(x321,x322)+E(f25(x323,x324,x321),f25(x323,x324,x322)) % 0.59/0.65 [33]~E(x331,x332)+E(f10(x331),f10(x332)) % 0.59/0.65 [34]~E(x341,x342)+E(f22(x341,x343),f22(x342,x343)) % 0.59/0.65 [35]~E(x351,x352)+E(f22(x353,x351),f22(x353,x352)) % 0.59/0.65 [36]~E(x361,x362)+E(f12(x361),f12(x362)) % 0.59/0.65 [37]~E(x371,x372)+E(f21(x371,x373),f21(x372,x373)) % 0.59/0.65 [38]~E(x381,x382)+E(f21(x383,x381),f21(x383,x382)) % 0.59/0.65 [39]~E(x391,x392)+E(f28(x391,x393),f28(x392,x393)) % 0.59/0.65 [40]~E(x401,x402)+E(f28(x403,x401),f28(x403,x402)) % 0.59/0.65 [41]~E(x411,x412)+E(f19(x411,x413),f19(x412,x413)) % 0.59/0.65 [42]~E(x421,x422)+E(f19(x423,x421),f19(x423,x422)) % 0.59/0.65 [43]~E(x431,x432)+E(f14(x431),f14(x432)) % 0.59/0.65 [44]~E(x441,x442)+E(f23(x441,x443),f23(x442,x443)) % 0.59/0.65 [45]~E(x451,x452)+E(f23(x453,x451),f23(x453,x452)) % 0.59/0.65 [46]~P1(x461)+P1(x462)+~E(x461,x462) % 0.59/0.65 [47]P16(x472,x473)+~E(x471,x472)+~P16(x471,x473) % 0.59/0.65 [48]P16(x483,x482)+~E(x481,x482)+~P16(x483,x481) % 0.59/0.65 [49]P7(x492,x493,x494)+~E(x491,x492)+~P7(x491,x493,x494) % 0.59/0.65 [50]P7(x503,x502,x504)+~E(x501,x502)+~P7(x503,x501,x504) % 0.59/0.65 [51]P7(x513,x514,x512)+~E(x511,x512)+~P7(x513,x514,x511) % 0.59/0.65 [52]P10(x522,x523)+~E(x521,x522)+~P10(x521,x523) % 0.59/0.65 [53]P10(x533,x532)+~E(x531,x532)+~P10(x533,x531) % 0.59/0.65 [54]~P2(x541)+P2(x542)+~E(x541,x542) % 0.59/0.65 [55]~P3(x551)+P3(x552)+~E(x551,x552) % 0.59/0.65 [56]~P9(x561)+P9(x562)+~E(x561,x562) % 0.59/0.65 [57]P4(x572,x573)+~E(x571,x572)+~P4(x571,x573) % 0.59/0.65 [58]P4(x583,x582)+~E(x581,x582)+~P4(x583,x581) % 0.59/0.65 [59]P11(x592,x593,x594)+~E(x591,x592)+~P11(x591,x593,x594) % 0.59/0.65 [60]P11(x603,x602,x604)+~E(x601,x602)+~P11(x603,x601,x604) % 0.59/0.65 [61]P11(x613,x614,x612)+~E(x611,x612)+~P11(x613,x614,x611) % 0.59/0.65 [62]P15(x622,x623)+~E(x621,x622)+~P15(x621,x623) % 0.59/0.65 [63]P15(x633,x632)+~E(x631,x632)+~P15(x633,x631) % 0.59/0.65 [64]P6(x642,x643)+~E(x641,x642)+~P6(x641,x643) % 0.59/0.65 [65]P6(x653,x652)+~E(x651,x652)+~P6(x653,x651) % 0.59/0.65 [66]~P13(x661)+P13(x662)+~E(x661,x662) % 0.59/0.65 [67]P12(x672,x673,x674)+~E(x671,x672)+~P12(x671,x673,x674) % 0.59/0.65 [68]P12(x683,x682,x684)+~E(x681,x682)+~P12(x683,x681,x684) % 0.59/0.65 [69]P12(x693,x694,x692)+~E(x691,x692)+~P12(x693,x694,x691) % 0.59/0.65 [70]~P5(x701)+P5(x702)+~E(x701,x702) % 0.59/0.65 [71]P8(x712,x713,x714)+~E(x711,x712)+~P8(x711,x713,x714) % 0.59/0.65 [72]P8(x723,x722,x724)+~E(x721,x722)+~P8(x723,x721,x724) % 0.59/0.65 [73]P8(x733,x734,x732)+~E(x731,x732)+~P8(x733,x734,x731) % 0.59/0.65 [74]~P14(x741)+P14(x742)+~E(x741,x742) % 0.59/0.65 % 0.59/0.65 %------------------------------------------- % 0.59/0.65 cnf(201,plain, % 0.59/0.65 ($false), % 0.59/0.65 inference(scs_inference,[],[98,95]), % 0.59/0.65 ['proof']). % 0.59/0.65 % SZS output end Proof % 0.59/0.65 % Total time :0.000000s %------------------------------------------------------------------------------