%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LAT385+4 : 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 : 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 10:19:18 EDT 2024 % Result : Theorem 1.12s 1.14s % Output : CNFRefutation 1.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : LAT385+4 : TPTP v8.2.0. Released v4.0.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n029.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Fri Jun 21 22:28:24 EDT 2024 % 0.13/0.34 % CPUTime : % 0.52/0.56 start to proof:theBenchmark % 1.03/1.12 %------------------------------------------- % 1.03/1.12 % File :CSE---1.7 % 1.03/1.12 % Problem :theBenchmark % 1.03/1.12 % Transform :cnf % 1.03/1.12 % Format :tptp:raw % 1.03/1.12 % Command :java -jar mcs_scs.jar %d %s % 1.03/1.12 % 1.03/1.12 % Result :Theorem 0.500000s % 1.03/1.12 % Output :CNFRefutation 0.500000s % 1.03/1.12 %------------------------------------------- % 1.03/1.12 %------------------------------------------------------------------------------ % 1.03/1.12 % File : LAT385+4 : TPTP v8.2.0. Released v4.0.0. % 1.03/1.12 % Domain : Lattice Theory % 1.03/1.12 % Problem : Tarski-Knaster fixed point theorem 03_01_02, 03 expansion % 1.03/1.12 % Version : Especial. % 1.03/1.12 % English : % 1.03/1.12 % 1.03/1.12 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 1.03/1.12 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 1.03/1.12 % : [VL+08] Verchinine et al. (2008), On Correctness of Mathematic % 1.03/1.12 % Source : [Pas08] % 1.03/1.12 % Names : tarski_03_01_02.03 [Pas08] % 1.03/1.12 % 1.03/1.12 % Status : Theorem % 1.03/1.12 % Rating : 0.17 v8.2.0, 0.14 v8.1.0, 0.17 v7.5.0, 0.19 v7.4.0, 0.10 v7.2.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.13 v6.4.0, 0.15 v6.3.0, 0.12 v6.2.0, 0.16 v6.1.0, 0.13 v5.5.0, 0.11 v5.3.0, 0.15 v5.2.0, 0.10 v5.1.0, 0.19 v5.0.0, 0.25 v4.1.0, 0.30 v4.0.1, 0.70 v4.0.0 % 1.03/1.12 % Syntax : Number of formulae : 28 ( 0 unt; 10 def) % 1.03/1.12 % Number of atoms : 173 ( 12 equ) % 1.03/1.12 % Maximal formula atoms : 37 ( 6 avg) % 1.03/1.12 % Number of connectives : 146 ( 1 ~; 7 |; 65 &) % 1.03/1.12 % ( 10 <=>; 63 =>; 0 <=; 0 <~>) % 1.03/1.12 % Maximal formula depth : 24 ( 7 avg) % 1.03/1.12 % Maximal term depth : 2 ( 1 avg) % 1.03/1.13 % Number of predicates : 17 ( 15 usr; 1 prp; 0-3 aty) % 1.03/1.13 % Number of functors : 10 ( 10 usr; 5 con; 0-3 aty) % 1.03/1.13 % Number of variables : 78 ( 72 !; 6 ?) % 1.03/1.13 % SPC : FOF_THM_RFO_SEQ % 1.03/1.13 % 1.03/1.13 % Comments : Problem generated by the SAD system [VLP07] % 1.03/1.13 %------------------------------------------------------------------------------ % 1.03/1.13 fof(mSetSort,axiom, % 1.03/1.13 ! [W0] : % 1.03/1.13 ( aSet0(W0) % 1.03/1.13 => $true ) ). % 1.03/1.13 % 1.03/1.13 fof(mElmSort,axiom, % 1.03/1.13 ! [W0] : % 1.03/1.13 ( aElement0(W0) % 1.03/1.13 => $true ) ). % 1.03/1.13 % 1.03/1.13 fof(mEOfElem,axiom, % 1.03/1.13 ! [W0] : % 1.03/1.13 ( aSet0(W0) % 1.03/1.13 => ! [W1] : % 1.03/1.13 ( aElementOf0(W1,W0) % 1.03/1.13 => aElement0(W1) ) ) ). % 1.03/1.13 % 1.03/1.13 fof(mDefEmpty,definition, % 1.03/1.13 ! [W0] : % 1.03/1.13 ( aSet0(W0) % 1.03/1.13 => ( isEmpty0(W0) % 1.03/1.13 <=> ~ ? [W1] : aElementOf0(W1,W0) ) ) ). % 1.03/1.13 % 1.03/1.13 fof(mDefSub,definition, % 1.03/1.13 ! [W0] : % 1.03/1.13 ( aSet0(W0) % 1.03/1.13 => ! [W1] : % 1.03/1.13 ( aSubsetOf0(W1,W0) % 1.03/1.13 <=> ( aSet0(W1) % 1.03/1.13 & ! [W2] : % 1.03/1.13 ( aElementOf0(W2,W1) % 1.03/1.13 => aElementOf0(W2,W0) ) ) ) ) ). % 1.03/1.13 % 1.03/1.13 fof(mLessRel,axiom, % 1.03/1.13 ! [W0,W1] : % 1.03/1.13 ( ( aElement0(W0) % 1.03/1.13 & aElement0(W1) ) % 1.03/1.13 => ( sdtlseqdt0(W0,W1) % 1.03/1.13 => $true ) ) ). % 1.03/1.13 % 1.03/1.13 fof(mARefl,axiom, % 1.03/1.13 ! [W0] : % 1.03/1.13 ( aElement0(W0) % 1.03/1.13 => sdtlseqdt0(W0,W0) ) ). % 1.03/1.13 % 1.03/1.13 fof(mASymm,axiom, % 1.03/1.13 ! [W0,W1] : % 1.03/1.13 ( ( aElement0(W0) % 1.03/1.13 & aElement0(W1) ) % 1.03/1.13 => ( ( sdtlseqdt0(W0,W1) % 1.03/1.13 & sdtlseqdt0(W1,W0) ) % 1.03/1.13 => W0 = W1 ) ) ). % 1.03/1.13 % 1.03/1.13 fof(mTrans,axiom, % 1.03/1.13 ! [W0,W1,W2] : % 1.03/1.13 ( ( aElement0(W0) % 1.03/1.13 & aElement0(W1) % 1.03/1.13 & aElement0(W2) ) % 1.03/1.13 => ( ( sdtlseqdt0(W0,W1) % 1.03/1.13 & sdtlseqdt0(W1,W2) ) % 1.03/1.13 => sdtlseqdt0(W0,W2) ) ) ). % 1.03/1.13 % 1.03/1.13 fof(mDefLB,definition, % 1.03/1.13 ! [W0] : % 1.03/1.13 ( aSet0(W0) % 1.03/1.13 => ! [W1] : % 1.03/1.13 ( aSubsetOf0(W1,W0) % 1.03/1.13 => ! [W2] : % 1.03/1.13 ( aLowerBoundOfIn0(W2,W1,W0) % 1.03/1.13 <=> ( aElementOf0(W2,W0) % 1.03/1.13 & ! [W3] : % 1.03/1.13 ( aElementOf0(W3,W1) % 1.03/1.13 => sdtlseqdt0(W2,W3) ) ) ) ) ) ). % 1.03/1.13 % 1.03/1.13 fof(mDefUB,definition, % 1.03/1.13 ! [W0] : % 1.03/1.13 ( aSet0(W0) % 1.03/1.13 => ! [W1] : % 1.03/1.13 ( aSubsetOf0(W1,W0) % 1.03/1.13 => ! [W2] : % 1.03/1.13 ( aUpperBoundOfIn0(W2,W1,W0) % 1.03/1.13 <=> ( aElementOf0(W2,W0) % 1.03/1.13 & ! [W3] : % 1.03/1.13 ( aElementOf0(W3,W1) % 1.03/1.13 => sdtlseqdt0(W3,W2) ) ) ) ) ) ). % 1.03/1.13 % 1.03/1.13 fof(mDefInf,definition, % 1.03/1.13 ! [W0] : % 1.03/1.13 ( aSet0(W0) % 1.03/1.13 => ! [W1] : % 1.03/1.13 ( aSubsetOf0(W1,W0) % 1.03/1.13 => ! [W2] : % 1.03/1.13 ( aInfimumOfIn0(W2,W1,W0) % 1.03/1.13 <=> ( aElementOf0(W2,W0) % 1.03/1.13 & aLowerBoundOfIn0(W2,W1,W0) % 1.03/1.13 & ! [W3] : % 1.03/1.13 ( aLowerBoundOfIn0(W3,W1,W0) % 1.03/1.13 => sdtlseqdt0(W3,W2) ) ) ) ) ) ). % 1.03/1.13 % 1.03/1.13 fof(mDefSup,definition, % 1.03/1.13 ! [W0] : % 1.03/1.13 ( aSet0(W0) % 1.03/1.13 => ! [W1] : % 1.03/1.13 ( aSubsetOf0(W1,W0) % 1.03/1.13 => ! [W2] : % 1.03/1.13 ( aSupremumOfIn0(W2,W1,W0) % 1.03/1.13 <=> ( aElementOf0(W2,W0) % 1.03/1.13 & aUpperBoundOfIn0(W2,W1,W0) % 1.03/1.13 & ! [W3] : % 1.03/1.13 ( aUpperBoundOfIn0(W3,W1,W0) % 1.03/1.13 => sdtlseqdt0(W2,W3) ) ) ) ) ) ). % 1.03/1.13 % 1.03/1.13 fof(mSupUn,axiom, % 1.03/1.13 ! [W0] : % 1.03/1.13 ( aSet0(W0) % 1.03/1.13 => ! [W1] : % 1.03/1.13 ( aSubsetOf0(W1,W0) % 1.03/1.13 => ! [W2,W3] : % 1.03/1.13 ( ( aSupremumOfIn0(W2,W1,W0) % 1.03/1.13 & aSupremumOfIn0(W3,W1,W0) ) % 1.03/1.13 => W2 = W3 ) ) ) ). % 1.03/1.13 % 1.03/1.13 fof(mInfUn,axiom, % 1.03/1.13 ! [W0] : % 1.03/1.13 ( aSet0(W0) % 1.03/1.13 => ! [W1] : % 1.03/1.13 ( aSubsetOf0(W1,W0) % 1.03/1.13 => ! [W2,W3] : % 1.03/1.13 ( ( aInfimumOfIn0(W2,W1,W0) % 1.03/1.13 & aInfimumOfIn0(W3,W1,W0) ) % 1.03/1.13 => W2 = W3 ) ) ) ). % 1.03/1.13 % 1.03/1.13 fof(mDefCLat,definition, % 1.03/1.13 ! [W0] : % 1.03/1.13 ( aCompleteLattice0(W0) % 1.03/1.13 <=> ( aSet0(W0) % 1.03/1.13 & ! [W1] : % 1.03/1.13 ( aSubsetOf0(W1,W0) % 1.03/1.13 => ? [W2] : % 1.03/1.13 ( aInfimumOfIn0(W2,W1,W0) % 1.03/1.13 & ? [W3] : aSupremumOfIn0(W3,W1,W0) ) ) ) ) ). % 1.03/1.13 % 1.03/1.13 fof(mConMap,axiom, % 1.03/1.13 ! [W0] : % 1.03/1.13 ( aFunction0(W0) % 1.03/1.13 => $true ) ). % 1.03/1.13 % 1.03/1.13 fof(mDomSort,axiom, % 1.03/1.13 ! [W0] : % 1.03/1.13 ( aFunction0(W0) % 1.03/1.13 => aSet0(szDzozmdt0(W0)) ) ). % 1.03/1.13 % 1.03/1.13 fof(mRanSort,axiom, % 1.03/1.13 ! [W0] : % 1.03/1.13 ( aFunction0(W0) % 1.03/1.13 => aSet0(szRzazndt0(W0)) ) ). % 1.03/1.13 % 1.03/1.13 fof(mDefDom,definition, % 1.03/1.13 ! [W0,W1] : % 1.03/1.13 ( ( aFunction0(W0) % 1.03/1.13 & aSet0(W1) ) % 1.03/1.13 => ( isOn0(W0,W1) % 1.03/1.13 <=> ( szDzozmdt0(W0) = szRzazndt0(W0) % 1.03/1.13 & szRzazndt0(W0) = W1 ) ) ) ). % 1.03/1.13 % 1.03/1.13 fof(mImgSort,axiom, % 1.03/1.13 ! [W0] : % 1.03/1.13 ( aFunction0(W0) % 1.03/1.13 => ! [W1] : % 1.03/1.13 ( aElementOf0(W1,szDzozmdt0(W0)) % 1.03/1.13 => aElementOf0(sdtlpdtrp0(W0,W1),szRzazndt0(W0)) ) ) ). % 1.03/1.13 % 1.03/1.13 fof(mDefFix,definition, % 1.03/1.13 ! [W0] : % 1.03/1.13 ( aFunction0(W0) % 1.03/1.13 => ! [W1] : % 1.03/1.13 ( aFixedPointOf0(W1,W0) % 1.03/1.13 <=> ( aElementOf0(W1,szDzozmdt0(W0)) % 1.03/1.13 & sdtlpdtrp0(W0,W1) = W1 ) ) ) ). % 1.03/1.13 % 1.03/1.13 fof(mDefMonot,definition, % 1.03/1.13 ! [W0] : % 1.03/1.13 ( aFunction0(W0) % 1.03/1.13 => ( isMonotone0(W0) % 1.03/1.13 <=> ! [W1,W2] : % 1.03/1.13 ( ( aElementOf0(W1,szDzozmdt0(W0)) % 1.03/1.13 & aElementOf0(W2,szDzozmdt0(W0)) ) % 1.03/1.13 => ( sdtlseqdt0(W1,W2) % 1.03/1.13 => sdtlseqdt0(sdtlpdtrp0(W0,W1),sdtlpdtrp0(W0,W2)) ) ) ) ) ). % 1.03/1.13 % 1.03/1.13 fof(m__1123,hypothesis, % 1.03/1.13 ( aSet0(xU) % 1.03/1.13 & ! [W0] : % 1.03/1.13 ( ( ( aSet0(W0) % 1.03/1.13 & ! [W1] : % 1.03/1.13 ( aElementOf0(W1,W0) % 1.03/1.13 => aElementOf0(W1,xU) ) ) % 1.03/1.13 | aSubsetOf0(W0,xU) ) % 1.03/1.13 => ? [W1] : % 1.03/1.13 ( aElementOf0(W1,xU) % 1.03/1.13 & aElementOf0(W1,xU) % 1.03/1.13 & ! [W2] : % 1.03/1.13 ( aElementOf0(W2,W0) % 1.03/1.13 => sdtlseqdt0(W1,W2) ) % 1.03/1.13 & aLowerBoundOfIn0(W1,W0,xU) % 1.03/1.13 & ! [W2] : % 1.03/1.13 ( ( ( aElementOf0(W2,xU) % 1.03/1.13 & ! [W3] : % 1.03/1.13 ( aElementOf0(W3,W0) % 1.03/1.13 => sdtlseqdt0(W2,W3) ) ) % 1.03/1.13 | aLowerBoundOfIn0(W2,W0,xU) ) % 1.03/1.13 => sdtlseqdt0(W2,W1) ) % 1.03/1.13 & aInfimumOfIn0(W1,W0,xU) % 1.03/1.13 & ? [W2] : % 1.03/1.13 ( aElementOf0(W2,xU) % 1.03/1.13 & aElementOf0(W2,xU) % 1.03/1.13 & ! [W3] : % 1.03/1.13 ( aElementOf0(W3,W0) % 1.03/1.13 => sdtlseqdt0(W3,W2) ) % 1.03/1.13 & aUpperBoundOfIn0(W2,W0,xU) % 1.03/1.13 & ! [W3] : % 1.03/1.13 ( ( ( aElementOf0(W3,xU) % 1.03/1.13 & ! [W4] : % 1.03/1.13 ( aElementOf0(W4,W0) % 1.03/1.13 => sdtlseqdt0(W4,W3) ) ) % 1.03/1.13 | aUpperBoundOfIn0(W3,W0,xU) ) % 1.03/1.13 => sdtlseqdt0(W2,W3) ) % 1.03/1.13 & aSupremumOfIn0(W2,W0,xU) ) ) ) % 1.03/1.13 & aCompleteLattice0(xU) % 1.03/1.13 & aFunction0(xf) % 1.03/1.13 & ! [W0,W1] : % 1.03/1.13 ( ( aElementOf0(W0,szDzozmdt0(xf)) % 1.03/1.13 & aElementOf0(W1,szDzozmdt0(xf)) ) % 1.03/1.13 => ( sdtlseqdt0(W0,W1) % 1.03/1.13 => sdtlseqdt0(sdtlpdtrp0(xf,W0),sdtlpdtrp0(xf,W1)) ) ) % 1.03/1.13 & isMonotone0(xf) % 1.03/1.13 & szDzozmdt0(xf) = szRzazndt0(xf) % 1.03/1.13 & szRzazndt0(xf) = xU % 1.03/1.13 & isOn0(xf,xU) ) ). % 1.03/1.13 % 1.03/1.13 fof(m__1144,hypothesis, % 1.03/1.13 ( aSet0(xS) % 1.03/1.14 & ! [W0] : % 1.03/1.14 ( ( aElementOf0(W0,xS) % 1.03/1.14 => ( aElementOf0(W0,szDzozmdt0(xf)) % 1.03/1.14 & sdtlpdtrp0(xf,W0) = W0 % 1.03/1.14 & aFixedPointOf0(W0,xf) ) ) % 1.03/1.14 & ( ( ( aElementOf0(W0,szDzozmdt0(xf)) % 1.03/1.14 & sdtlpdtrp0(xf,W0) = W0 ) % 1.12/1.14 | aFixedPointOf0(W0,xf) ) % 1.12/1.14 => aElementOf0(W0,xS) ) ) % 1.12/1.14 & xS = cS1142(xf) ) ). % 1.12/1.14 % 1.12/1.14 fof(m__1173,hypothesis, % 1.12/1.14 ( aSet0(xT) % 1.12/1.14 & ! [W0] : % 1.12/1.14 ( aElementOf0(W0,xT) % 1.12/1.14 => aElementOf0(W0,xS) ) % 1.12/1.14 & aSubsetOf0(xT,xS) ) ). % 1.12/1.14 % 1.12/1.14 fof(m__1244,hypothesis, % 1.12/1.14 ( aSet0(xP) % 1.12/1.14 & ! [W0] : % 1.12/1.14 ( ( aElementOf0(W0,xP) % 1.12/1.14 => ( aElementOf0(W0,xU) % 1.12/1.14 & sdtlseqdt0(sdtlpdtrp0(xf,W0),W0) % 1.12/1.14 & ! [W1] : % 1.12/1.14 ( aElementOf0(W1,xT) % 1.12/1.14 => sdtlseqdt0(W1,W0) ) % 1.12/1.14 & aUpperBoundOfIn0(W0,xT,xU) ) ) % 1.12/1.14 & ( ( aElementOf0(W0,xU) % 1.12/1.14 & sdtlseqdt0(sdtlpdtrp0(xf,W0),W0) % 1.12/1.14 & ( ! [W1] : % 1.12/1.14 ( aElementOf0(W1,xT) % 1.12/1.14 => sdtlseqdt0(W1,W0) ) % 1.12/1.14 | aUpperBoundOfIn0(W0,xT,xU) ) ) % 1.12/1.14 => aElementOf0(W0,xP) ) ) % 1.12/1.14 & xP = cS1241(xU,xf,xT) ) ). % 1.12/1.14 % 1.12/1.14 fof(m__,conjecture, % 1.12/1.14 ? [W0] : % 1.12/1.14 ( ( aElementOf0(W0,xU) % 1.12/1.14 & ( ( aElementOf0(W0,xU) % 1.12/1.14 & ! [W1] : % 1.12/1.14 ( aElementOf0(W1,xP) % 1.12/1.14 => sdtlseqdt0(W0,W1) ) ) % 1.12/1.14 | aLowerBoundOfIn0(W0,xP,xU) ) % 1.12/1.14 & ! [W1] : % 1.12/1.14 ( ( aElementOf0(W1,xU) % 1.12/1.14 & ! [W2] : % 1.12/1.14 ( aElementOf0(W2,xP) % 1.12/1.14 => sdtlseqdt0(W1,W2) ) % 1.12/1.14 & aLowerBoundOfIn0(W1,xP,xU) ) % 1.12/1.14 => sdtlseqdt0(W1,W0) ) ) % 1.12/1.14 | aInfimumOfIn0(W0,xP,xU) ) ). % 1.12/1.14 % 1.12/1.14 %------------------------------------------------------------------------------ % 1.12/1.14 %------------------------------------------- % 1.12/1.14 % Proof found % 1.12/1.14 % SZS status Theorem for theBenchmark % 1.12/1.14 % SZS output start Proof % 1.12/1.14 %ClaNum:178(EqnAxiom:72) % 1.12/1.14 %VarNum:559(SingletonVarNum:175) % 1.12/1.14 %MaxLitNum:6 % 1.12/1.14 %MaxfuncDepth:2 % 1.12/1.14 %SharedTerms:22 % 1.12/1.14 %goalClause: 86 119 128 129 132 134 139 140 141 149 155 157 161 % 1.12/1.14 %singleGoalClaCount:1 % 1.12/1.14 [75]P1(a28) % 1.12/1.14 [76]P1(a3) % 1.12/1.14 [77]P1(a29) % 1.12/1.14 [78]P1(a27) % 1.12/1.14 [79]P2(a28) % 1.12/1.14 [80]P3(a1) % 1.12/1.14 [81]P9(a1) % 1.12/1.14 [83]P10(a29,a3) % 1.12/1.14 [84]P15(a1,a28) % 1.12/1.14 [73]E(f2(a1),a3) % 1.12/1.14 [74]E(f4(a1),a28) % 1.12/1.14 [82]E(f5(a1),f4(a1)) % 1.12/1.14 [85]E(f6(a28,a1,a29),a27) % 1.12/1.14 [86]~P7(x861,a27,a28) % 1.12/1.14 [87]~P2(x871)+P1(x871) % 1.12/1.14 [90]~P4(x901)+P16(x901,x901) % 1.12/1.14 [91]P11(x911)+~P10(x911,a28) % 1.12/1.14 [97]~P5(x971,a27)+P5(x971,a28) % 1.12/1.14 [98]~P5(x981,a29)+P5(x981,a3) % 1.12/1.14 [99]~P6(x991,a1)+P5(x991,a3) % 1.12/1.14 [100]~P5(x1001,a3)+P6(x1001,a1) % 1.12/1.14 [130]~P5(x1301,a27)+P12(x1301,a29,a28) % 1.12/1.14 [88]~P3(x881)+P1(f5(x881)) % 1.12/1.14 [89]~P3(x891)+P1(f4(x891)) % 1.12/1.14 [92]~P11(x921)+P5(f7(x921),a28) % 1.12/1.14 [93]~P11(x931)+P5(f14(x931),a28) % 1.12/1.14 [101]~P5(x1011,a3)+E(f26(a1,x1011),x1011) % 1.12/1.14 [105]~P5(x1051,a3)+P5(x1051,f5(a1)) % 1.12/1.14 [118]~P5(x1181,a27)+P16(f26(a1,x1181),x1181) % 1.12/1.14 [122]~P11(x1221)+P8(f7(x1221),x1221,a28) % 1.12/1.14 [123]~P11(x1231)+P12(f14(x1231),x1231,a28) % 1.12/1.14 [124]~P11(x1241)+P7(f7(x1241),x1241,a28) % 1.12/1.14 [125]~P11(x1251)+P13(f14(x1251),x1251,a28) % 1.12/1.14 [94]~P1(x941)+P14(x941)+P5(f16(x941),x941) % 1.12/1.14 [95]~P1(x951)+P2(x951)+P10(f18(x951),x951) % 1.12/1.14 [96]~P1(x961)+P11(x961)+P5(f8(x961),x961) % 1.12/1.14 [106]~P3(x1061)+P9(x1061)+P5(f9(x1061),f5(x1061)) % 1.12/1.14 [107]~P3(x1071)+P9(x1071)+P5(f10(x1071),f5(x1071)) % 1.12/1.14 [108]~P3(x1081)+P9(x1081)+P16(f9(x1081),f10(x1081)) % 1.12/1.14 [109]~P1(x1091)+P11(x1091)+~P5(f8(x1091),a28) % 1.12/1.14 [119]~P5(x1191,a28)+P5(f13(x1191),a28)+P5(f11(x1191),a27) % 1.12/1.14 [120]P5(x1201,a3)+~E(f26(a1,x1201),x1201)+~P5(x1201,f5(a1)) % 1.12/1.14 [128]~P5(x1281,a28)+~P16(x1281,f11(x1281))+P5(f13(x1281),a28) % 1.12/1.14 [129]~P5(x1291,a28)+~P16(f13(x1291),x1291)+P5(f11(x1291),a27) % 1.12/1.14 [134]~P16(x1341,f11(x1341))+~P16(f13(x1341),x1341)+~P5(x1341,a28) % 1.12/1.14 [140]~P5(x1401,a28)+P8(f13(x1401),a27,a28)+P5(f11(x1401),a27) % 1.12/1.14 [141]~P5(x1411,a28)+~P16(x1411,f11(x1411))+P8(f13(x1411),a27,a28) % 1.12/1.14 [149]~P5(x1491,a28)+~P8(x1491,a27,a28)+P5(f13(x1491),a28) % 1.12/1.14 [155]~P16(f13(x1551),x1551)+~P5(x1551,a28)+~P8(x1551,a27,a28) % 1.12/1.14 [161]~P5(x1611,a28)+~P8(x1611,a27,a28)+P8(f13(x1611),a27,a28) % 1.12/1.14 [160]~P3(x1601)+P9(x1601)+~P16(f26(x1601,f9(x1601)),f26(x1601,f10(x1601))) % 1.12/1.14 [102]~P10(x1021,x1022)+P1(x1021)+~P1(x1022) % 1.12/1.14 [103]~P5(x1031,x1032)+P4(x1031)+~P1(x1032) % 1.12/1.14 [104]~P14(x1041)+~P1(x1041)+~P5(x1042,x1041) % 1.12/1.14 [117]P16(x1171,x1172)+~P5(x1172,a27)+~P5(x1171,a29) % 1.12/1.14 [111]~P3(x1111)+~P6(x1112,x1111)+E(f26(x1111,x1112),x1112) % 1.12/1.14 [114]~P3(x1142)+~P6(x1141,x1142)+P5(x1141,f5(x1142)) % 1.12/1.14 [115]~P11(x1152)+~P5(x1151,x1152)+P16(x1151,f14(x1152)) % 1.12/1.14 [116]~P11(x1161)+~P5(x1162,x1161)+P16(f7(x1161),x1162) % 1.12/1.14 [135]~P3(x1351)+~P5(x1352,f5(x1351))+P5(f26(x1351,x1352),f4(x1351)) % 1.12/1.14 [142]~P2(x1421)+~P10(x1422,x1421)+P7(f20(x1421,x1422),x1422,x1421) % 1.12/1.14 [143]~P2(x1431)+~P10(x1432,x1431)+P13(f25(x1431,x1432),x1432,x1431) % 1.12/1.14 [145]~P11(x1452)+~P8(x1451,x1452,a28)+P16(x1451,f7(x1452)) % 1.12/1.14 [146]~P11(x1461)+~P12(x1462,x1461,a28)+P16(f14(x1461),x1462) % 1.12/1.14 [144]~P5(x1441,a28)+P5(x1441,a27)+~P16(f26(a1,x1441),x1441)+P5(f12(x1441),a29) % 1.12/1.14 [150]~P5(x1501,a28)+~P16(f12(x1501),x1501)+P5(x1501,a27)+~P16(f26(a1,x1501),x1501) % 1.12/1.14 [165]~P5(x1651,a28)+P5(x1651,a27)+~P16(f26(a1,x1651),x1651)+~P12(x1651,a29,a28) % 1.12/1.14 [110]~P1(x1102)+~P3(x1101)+~P15(x1101,x1102)+E(f4(x1101),x1102) % 1.12/1.14 [112]~P3(x1121)+~P15(x1121,x1122)+~P1(x1122)+E(f5(x1121),f4(x1121)) % 1.12/1.14 [127]~P1(x1271)+~P1(x1272)+P10(x1271,x1272)+P5(f19(x1272,x1271),x1271) % 1.12/1.14 [131]~P3(x1312)+P6(x1311,x1312)+~E(f26(x1312,x1311),x1311)+~P5(x1311,f5(x1312)) % 1.12/1.14 [132]~P5(x1321,a28)+~P5(x1322,a27)+P16(f13(x1321),x1322)+P5(f11(x1321),a27) % 1.12/1.14 [136]~P11(x1362)+P5(f15(x1362,x1361),x1362)+~P5(x1361,a28)+P16(x1361,f7(x1362)) % 1.12/1.14 [137]~P11(x1371)+P5(f17(x1371,x1372),x1371)+~P5(x1372,a28)+P16(f14(x1371),x1372) % 1.12/1.14 [138]~P1(x1381)+~P1(x1382)+P10(x1381,x1382)+~P5(f19(x1382,x1381),x1382) % 1.12/1.14 [139]~P5(x1391,a28)+~P5(x1392,a27)+~P16(x1391,f11(x1391))+P16(f13(x1391),x1392) % 1.12/1.14 [147]~P11(x1472)+~P5(x1471,a28)+~P16(x1471,f15(x1472,x1471))+P16(x1471,f7(x1472)) % 1.12/1.14 [148]~P11(x1481)+~P5(x1482,a28)+~P16(f17(x1481,x1482),x1482)+P16(f14(x1481),x1482) % 1.12/1.14 [156]~P16(x1561,x1562)+~P5(x1562,f5(a1))+~P5(x1561,f5(a1))+P16(f26(a1,x1561),f26(a1,x1562)) % 1.12/1.14 [157]~P5(x1571,a28)+~P5(x1572,a27)+P16(f13(x1571),x1572)+~P8(x1571,a27,a28) % 1.12/1.14 [126]~P1(x1262)+~P10(x1263,x1262)+P5(x1261,x1262)+~P5(x1261,x1263) % 1.12/1.14 [151]~P1(x1512)+~P8(x1511,x1513,x1512)+P5(x1511,x1512)+~P10(x1513,x1512) % 1.12/1.14 [152]~P1(x1522)+~P12(x1521,x1523,x1522)+P5(x1521,x1522)+~P10(x1523,x1522) % 1.12/1.14 [153]~P1(x1532)+~P7(x1531,x1533,x1532)+P5(x1531,x1532)+~P10(x1533,x1532) % 1.12/1.14 [154]~P1(x1542)+~P13(x1541,x1543,x1542)+P5(x1541,x1542)+~P10(x1543,x1542) % 1.12/1.14 [163]~P1(x1633)+~P10(x1632,x1633)+~P7(x1631,x1632,x1633)+P8(x1631,x1632,x1633) % 1.12/1.14 [164]~P1(x1643)+~P10(x1642,x1643)+~P13(x1641,x1642,x1643)+P12(x1641,x1642,x1643) % 1.12/1.14 [166]~P1(x1661)+P2(x1661)+~P7(x1662,f18(x1661),x1661)+~P13(x1663,f18(x1661),x1661) % 1.12/1.14 [121]~P4(x1212)+~P4(x1211)+~P16(x1212,x1211)+~P16(x1211,x1212)+E(x1211,x1212) % 1.12/1.14 [113]~P1(x1132)+~P3(x1131)+P15(x1131,x1132)+~E(f4(x1131),x1132)+~E(f5(x1131),f4(x1131)) % 1.12/1.14 [171]~P1(x1713)+~P5(x1711,x1713)+~P10(x1712,x1713)+P8(x1711,x1712,x1713)+P5(f21(x1713,x1712,x1711),x1712) % 1.12/1.14 [172]~P1(x1723)+~P5(x1721,x1723)+~P10(x1722,x1723)+P12(x1721,x1722,x1723)+P5(f22(x1723,x1722,x1721),x1722) % 1.12/1.14 [173]~P1(x1733)+~P5(x1731,x1733)+~P10(x1732,x1733)+P8(x1731,x1732,x1733)+~P16(x1731,f21(x1733,x1732,x1731)) % 1.12/1.14 [174]~P1(x1743)+~P5(x1741,x1743)+~P10(x1742,x1743)+P12(x1741,x1742,x1743)+~P16(f22(x1743,x1742,x1741),x1741) % 1.12/1.14 [158]~P10(x1584,x1583)+~P8(x1581,x1584,x1583)+P16(x1581,x1582)+~P5(x1582,x1584)+~P1(x1583) % 1.12/1.14 [159]~P10(x1594,x1593)+~P12(x1592,x1594,x1593)+P16(x1591,x1592)+~P5(x1591,x1594)+~P1(x1593) % 1.12/1.14 [167]~P7(x1672,x1674,x1673)+~P7(x1671,x1674,x1673)+E(x1671,x1672)+~P10(x1674,x1673)+~P1(x1673) % 1.12/1.14 [168]~P13(x1682,x1684,x1683)+~P13(x1681,x1684,x1683)+E(x1681,x1682)+~P10(x1684,x1683)+~P1(x1683) % 1.12/1.14 [169]~P12(x1692,x1694,x1693)+~P13(x1691,x1694,x1693)+P16(x1691,x1692)+~P10(x1694,x1693)+~P1(x1693) % 1.12/1.14 [170]~P8(x1701,x1704,x1703)+~P7(x1702,x1704,x1703)+P16(x1701,x1702)+~P10(x1704,x1703)+~P1(x1703) % 1.12/1.14 [133]~P4(x1332)+~P4(x1331)+~P16(x1333,x1332)+~P16(x1331,x1333)+P16(x1331,x1332)+~P4(x1333) % 1.12/1.14 [162]~P3(x1621)+~P9(x1621)+~P16(x1622,x1623)+~P5(x1623,f5(x1621))+~P5(x1622,f5(x1621))+P16(f26(x1621,x1622),f26(x1621,x1623)) % 1.12/1.14 [175]~P1(x1753)+~P5(x1751,x1753)+~P10(x1752,x1753)+~P8(x1751,x1752,x1753)+P7(x1751,x1752,x1753)+P8(f23(x1753,x1752,x1751),x1752,x1753) % 1.12/1.14 [176]~P1(x1763)+~P5(x1761,x1763)+~P10(x1762,x1763)+~P12(x1761,x1762,x1763)+P13(x1761,x1762,x1763)+P12(f24(x1763,x1762,x1761),x1762,x1763) % 1.12/1.14 [177]~P1(x1773)+~P5(x1771,x1773)+~P10(x1772,x1773)+~P12(x1771,x1772,x1773)+P13(x1771,x1772,x1773)+~P16(x1771,f24(x1773,x1772,x1771)) % 1.12/1.14 [178]~P1(x1783)+~P5(x1781,x1783)+~P10(x1782,x1783)+~P8(x1781,x1782,x1783)+P7(x1781,x1782,x1783)+~P16(f23(x1783,x1782,x1781),x1781) % 1.12/1.14 %EqnAxiom % 1.12/1.14 [1]E(x11,x11) % 1.12/1.14 [2]E(x22,x21)+~E(x21,x22) % 1.12/1.14 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 1.12/1.14 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 1.12/1.14 [5]~E(x51,x52)+E(f4(x51),f4(x52)) % 1.12/1.14 [6]~E(x61,x62)+E(f5(x61),f5(x62)) % 1.12/1.14 [7]~E(x71,x72)+E(f23(x71,x73,x74),f23(x72,x73,x74)) % 1.12/1.14 [8]~E(x81,x82)+E(f23(x83,x81,x84),f23(x83,x82,x84)) % 1.12/1.14 [9]~E(x91,x92)+E(f23(x93,x94,x91),f23(x93,x94,x92)) % 1.12/1.14 [10]~E(x101,x102)+E(f6(x101,x103,x104),f6(x102,x103,x104)) % 1.12/1.14 [11]~E(x111,x112)+E(f6(x113,x111,x114),f6(x113,x112,x114)) % 1.12/1.14 [12]~E(x121,x122)+E(f6(x123,x124,x121),f6(x123,x124,x122)) % 1.12/1.14 [13]~E(x131,x132)+E(f21(x131,x133,x134),f21(x132,x133,x134)) % 1.12/1.14 [14]~E(x141,x142)+E(f21(x143,x141,x144),f21(x143,x142,x144)) % 1.12/1.14 [15]~E(x151,x152)+E(f21(x153,x154,x151),f21(x153,x154,x152)) % 1.12/1.14 [16]~E(x161,x162)+E(f24(x161,x163,x164),f24(x162,x163,x164)) % 1.12/1.14 [17]~E(x171,x172)+E(f24(x173,x171,x174),f24(x173,x172,x174)) % 1.12/1.14 [18]~E(x181,x182)+E(f24(x183,x184,x181),f24(x183,x184,x182)) % 1.12/1.14 [19]~E(x191,x192)+E(f7(x191),f7(x192)) % 1.12/1.14 [20]~E(x201,x202)+E(f14(x201),f14(x202)) % 1.12/1.14 [21]~E(x211,x212)+E(f16(x211),f16(x212)) % 1.12/1.14 [22]~E(x221,x222)+E(f18(x221),f18(x222)) % 1.12/1.14 [23]~E(x231,x232)+E(f8(x231),f8(x232)) % 1.12/1.14 [24]~E(x241,x242)+E(f26(x241,x243),f26(x242,x243)) % 1.12/1.14 [25]~E(x251,x252)+E(f26(x253,x251),f26(x253,x252)) % 1.12/1.14 [26]~E(x261,x262)+E(f12(x261),f12(x262)) % 1.12/1.14 [27]~E(x271,x272)+E(f9(x271),f9(x272)) % 1.12/1.14 [28]~E(x281,x282)+E(f25(x281,x283),f25(x282,x283)) % 1.12/1.14 [29]~E(x291,x292)+E(f25(x293,x291),f25(x293,x292)) % 1.12/1.14 [30]~E(x301,x302)+E(f10(x301),f10(x302)) % 1.12/1.14 [31]~E(x311,x312)+E(f11(x311),f11(x312)) % 1.12/1.14 [32]~E(x321,x322)+E(f22(x321,x323,x324),f22(x322,x323,x324)) % 1.12/1.14 [33]~E(x331,x332)+E(f22(x333,x331,x334),f22(x333,x332,x334)) % 1.12/1.14 [34]~E(x341,x342)+E(f22(x343,x344,x341),f22(x343,x344,x342)) % 1.12/1.14 [35]~E(x351,x352)+E(f13(x351),f13(x352)) % 1.12/1.14 [36]~E(x361,x362)+E(f20(x361,x363),f20(x362,x363)) % 1.12/1.14 [37]~E(x371,x372)+E(f20(x373,x371),f20(x373,x372)) % 1.12/1.14 [38]~E(x381,x382)+E(f17(x381,x383),f17(x382,x383)) % 1.12/1.14 [39]~E(x391,x392)+E(f17(x393,x391),f17(x393,x392)) % 1.12/1.14 [40]~E(x401,x402)+E(f15(x401,x403),f15(x402,x403)) % 1.12/1.14 [41]~E(x411,x412)+E(f15(x413,x411),f15(x413,x412)) % 1.12/1.14 [42]~E(x421,x422)+E(f19(x421,x423),f19(x422,x423)) % 1.12/1.14 [43]~E(x431,x432)+E(f19(x433,x431),f19(x433,x432)) % 1.12/1.14 [44]~P1(x441)+P1(x442)+~E(x441,x442) % 1.12/1.14 [45]P16(x452,x453)+~E(x451,x452)+~P16(x451,x453) % 1.12/1.14 [46]P16(x463,x462)+~E(x461,x462)+~P16(x463,x461) % 1.12/1.14 [47]P8(x472,x473,x474)+~E(x471,x472)+~P8(x471,x473,x474) % 1.12/1.14 [48]P8(x483,x482,x484)+~E(x481,x482)+~P8(x483,x481,x484) % 1.12/1.14 [49]P8(x493,x494,x492)+~E(x491,x492)+~P8(x493,x494,x491) % 1.12/1.14 [50]P10(x502,x503)+~E(x501,x502)+~P10(x501,x503) % 1.12/1.14 [51]P10(x513,x512)+~E(x511,x512)+~P10(x513,x511) % 1.12/1.14 [52]~P2(x521)+P2(x522)+~E(x521,x522) % 1.12/1.14 [53]~P3(x531)+P3(x532)+~E(x531,x532) % 1.12/1.14 [54]~P9(x541)+P9(x542)+~E(x541,x542) % 1.12/1.14 [55]P5(x552,x553)+~E(x551,x552)+~P5(x551,x553) % 1.12/1.14 [56]P5(x563,x562)+~E(x561,x562)+~P5(x563,x561) % 1.12/1.14 [57]P15(x572,x573)+~E(x571,x572)+~P15(x571,x573) % 1.12/1.14 [58]P15(x583,x582)+~E(x581,x582)+~P15(x583,x581) % 1.12/1.14 [59]P7(x592,x593,x594)+~E(x591,x592)+~P7(x591,x593,x594) % 1.12/1.14 [60]P7(x603,x602,x604)+~E(x601,x602)+~P7(x603,x601,x604) % 1.12/1.14 [61]P7(x613,x614,x612)+~E(x611,x612)+~P7(x613,x614,x611) % 1.12/1.14 [62]P13(x622,x623,x624)+~E(x621,x622)+~P13(x621,x623,x624) % 1.12/1.14 [63]P13(x633,x632,x634)+~E(x631,x632)+~P13(x633,x631,x634) % 1.12/1.14 [64]P13(x643,x644,x642)+~E(x641,x642)+~P13(x643,x644,x641) % 1.12/1.14 [65]P12(x652,x653,x654)+~E(x651,x652)+~P12(x651,x653,x654) % 1.12/1.14 [66]P12(x663,x662,x664)+~E(x661,x662)+~P12(x663,x661,x664) % 1.12/1.14 [67]P12(x673,x674,x672)+~E(x671,x672)+~P12(x673,x674,x671) % 1.12/1.14 [68]~P11(x681)+P11(x682)+~E(x681,x682) % 1.12/1.14 [69]~P4(x691)+P4(x692)+~E(x691,x692) % 1.12/1.14 [70]P6(x702,x703)+~E(x701,x702)+~P6(x701,x703) % 1.12/1.14 [71]P6(x713,x712)+~E(x711,x712)+~P6(x713,x711) % 1.12/1.14 [72]~P14(x721)+P14(x722)+~E(x721,x722) % 1.12/1.14 % 1.12/1.14 %------------------------------------------- % 1.12/1.14 cnf(179,plain, % 1.12/1.14 (~P11(a27)), % 1.12/1.15 inference(scs_inference,[],[86,124])). % 1.12/1.15 cnf(356,plain, % 1.12/1.15 (~P5(f8(a27),a27)), % 1.12/1.15 inference(scs_inference,[],[179,78,97,109])). % 1.12/1.15 cnf(357,plain, % 1.12/1.15 ($false), % 1.12/1.15 inference(scs_inference,[],[179,356,78,96]), % 1.12/1.15 ['proof']). % 1.12/1.15 % SZS output end Proof % 1.12/1.15 % Total time :0.500000s %------------------------------------------------------------------------------