%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : RNG102+1 : 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 : n007.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 14:01:05 EDT 2024 % Result : Theorem 50.93s 51.00s % Output : CNFRefutation 50.93s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : RNG102+1 : TPTP v8.2.0. Released v4.0.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n007.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 : Tue Jun 18 13:57:38 EDT 2024 % 0.12/0.34 % CPUTime : % 0.52/0.60 start to proof:theBenchmark % 50.93/50.97 %------------------------------------------- % 50.93/50.97 % File :CSE---1.7 % 50.93/50.97 % Problem :theBenchmark % 50.93/50.97 % Transform :cnf % 50.93/50.97 % Format :tptp:raw % 50.93/50.97 % Command :java -jar mcs_scs.jar %d %s % 50.93/50.97 % 50.93/50.97 % Result :Theorem 50.300000s % 50.93/50.97 % Output :CNFRefutation 50.300000s % 50.93/50.97 %------------------------------------------- % 50.93/50.98 %------------------------------------------------------------------------------ % 50.93/50.98 % File : RNG102+1 : TPTP v8.2.0. Released v4.0.0. % 50.93/50.98 % Domain : Ring Theory % 50.93/50.98 % Problem : Chinese remainder theorem in a ring 06_02, 00 expansion % 50.93/50.98 % Version : Especial. % 50.93/50.98 % English : % 50.93/50.98 % 50.93/50.98 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 50.93/50.98 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 50.93/50.98 % Source : [Pas08] % 50.93/50.98 % Names : chines_06_02.00 [Pas08] % 50.93/50.98 % 50.93/50.98 % Status : Theorem % 50.93/50.98 % Rating : 0.33 v8.1.0, 0.36 v7.5.0, 0.38 v7.4.0, 0.30 v7.3.0, 0.38 v7.1.0, 0.35 v7.0.0, 0.37 v6.4.0, 0.42 v6.3.0, 0.38 v6.2.0, 0.48 v6.1.0, 0.57 v6.0.0, 0.43 v5.5.0, 0.52 v5.4.0, 0.54 v5.3.0, 0.59 v5.2.0, 0.45 v5.1.0, 0.52 v5.0.0, 0.67 v4.1.0, 0.70 v4.0.1, 0.83 v4.0.0 % 50.93/50.98 % Syntax : Number of formulae : 41 ( 4 unt; 9 def) % 50.93/50.98 % Number of atoms : 158 ( 33 equ) % 50.93/50.98 % Maximal formula atoms : 9 ( 3 avg) % 50.93/50.98 % Number of connectives : 121 ( 4 ~; 1 |; 57 &) % 50.93/50.98 % ( 12 <=>; 47 =>; 0 <=; 0 <~>) % 50.93/50.98 % Maximal formula depth : 13 ( 5 avg) % 50.93/50.98 % Maximal term depth : 3 ( 1 avg) % 50.93/50.98 % Number of predicates : 13 ( 11 usr; 1 prp; 0-3 aty) % 50.93/50.98 % Number of functors : 14 ( 14 usr; 7 con; 0-2 aty) % 50.93/50.98 % Number of variables : 84 ( 76 !; 8 ?) % 50.93/50.98 % SPC : FOF_THM_RFO_SEQ % 50.93/50.98 % 50.93/50.98 % Comments : Problem generated by the SAD system [VLP07] % 50.93/50.98 %------------------------------------------------------------------------------ % 50.93/50.98 fof(mElmSort,axiom, % 50.93/50.98 ! [W0] : % 50.93/50.98 ( aElement0(W0) % 50.93/50.98 => $true ) ). % 50.93/50.98 % 50.93/50.98 fof(mSortsC,axiom, % 50.93/50.98 aElement0(sz00) ). % 50.93/50.98 % 50.93/50.98 fof(mSortsC_01,axiom, % 50.93/50.98 aElement0(sz10) ). % 50.93/50.98 % 50.93/50.98 fof(mSortsU,axiom, % 50.93/50.98 ! [W0] : % 50.93/50.98 ( aElement0(W0) % 50.93/50.98 => aElement0(smndt0(W0)) ) ). % 50.93/50.98 % 50.93/50.98 fof(mSortsB,axiom, % 50.93/50.98 ! [W0,W1] : % 50.93/50.98 ( ( aElement0(W0) % 50.93/50.98 & aElement0(W1) ) % 50.93/50.98 => aElement0(sdtpldt0(W0,W1)) ) ). % 50.93/50.98 % 50.93/50.98 fof(mSortsB_02,axiom, % 50.93/50.98 ! [W0,W1] : % 50.93/50.98 ( ( aElement0(W0) % 50.93/50.98 & aElement0(W1) ) % 50.93/50.98 => aElement0(sdtasdt0(W0,W1)) ) ). % 50.93/50.98 % 50.93/50.98 fof(mAddComm,axiom, % 50.93/50.98 ! [W0,W1] : % 50.93/50.98 ( ( aElement0(W0) % 50.93/50.98 & aElement0(W1) ) % 50.93/50.98 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 50.93/50.98 % 50.93/50.98 fof(mAddAsso,axiom, % 50.93/50.98 ! [W0,W1,W2] : % 50.93/50.98 ( ( aElement0(W0) % 50.93/50.98 & aElement0(W1) % 50.93/50.98 & aElement0(W2) ) % 50.93/50.98 => sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) ). % 50.93/50.98 % 50.93/50.98 fof(mAddZero,axiom, % 50.93/50.98 ! [W0] : % 50.93/50.98 ( aElement0(W0) % 50.93/50.98 => ( sdtpldt0(W0,sz00) = W0 % 50.93/50.98 & W0 = sdtpldt0(sz00,W0) ) ) ). % 50.93/50.98 % 50.93/50.98 fof(mAddInvr,axiom, % 50.93/50.98 ! [W0] : % 50.93/50.98 ( aElement0(W0) % 50.93/50.98 => ( sdtpldt0(W0,smndt0(W0)) = sz00 % 50.93/50.98 & sz00 = sdtpldt0(smndt0(W0),W0) ) ) ). % 50.93/50.98 % 50.93/50.98 fof(mMulComm,axiom, % 50.93/50.98 ! [W0,W1] : % 50.93/50.98 ( ( aElement0(W0) % 50.93/50.98 & aElement0(W1) ) % 50.93/50.98 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 50.93/50.98 % 50.93/50.98 fof(mMulAsso,axiom, % 50.93/50.98 ! [W0,W1,W2] : % 50.93/50.98 ( ( aElement0(W0) % 50.93/50.99 & aElement0(W1) % 50.93/50.99 & aElement0(W2) ) % 50.93/50.99 => sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) ). % 50.93/50.99 % 50.93/50.99 fof(mMulUnit,axiom, % 50.93/50.99 ! [W0] : % 50.93/50.99 ( aElement0(W0) % 50.93/50.99 => ( sdtasdt0(W0,sz10) = W0 % 50.93/50.99 & W0 = sdtasdt0(sz10,W0) ) ) ). % 50.93/50.99 % 50.93/50.99 fof(mAMDistr,axiom, % 50.93/50.99 ! [W0,W1,W2] : % 50.93/50.99 ( ( aElement0(W0) % 50.93/50.99 & aElement0(W1) % 50.93/50.99 & aElement0(W2) ) % 50.93/50.99 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 50.93/50.99 & sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ). % 50.93/50.99 % 50.93/50.99 fof(mMulMnOne,axiom, % 50.93/50.99 ! [W0] : % 50.93/50.99 ( aElement0(W0) % 50.93/50.99 => ( sdtasdt0(smndt0(sz10),W0) = smndt0(W0) % 50.93/50.99 & smndt0(W0) = sdtasdt0(W0,smndt0(sz10)) ) ) ). % 50.93/50.99 % 50.93/50.99 fof(mMulZero,axiom, % 50.93/50.99 ! [W0] : % 50.93/50.99 ( aElement0(W0) % 50.93/50.99 => ( sdtasdt0(W0,sz00) = sz00 % 50.93/50.99 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 50.93/50.99 % 50.93/50.99 fof(mCancel,axiom, % 50.93/50.99 ! [W0,W1] : % 50.93/50.99 ( ( aElement0(W0) % 50.93/50.99 & aElement0(W1) ) % 50.93/50.99 => ( sdtasdt0(W0,W1) = sz00 % 50.93/50.99 => ( W0 = sz00 % 50.93/50.99 | W1 = sz00 ) ) ) ). % 50.93/50.99 % 50.93/50.99 fof(mUnNeZr,axiom, % 50.93/50.99 sz10 != sz00 ). % 50.93/50.99 % 50.93/50.99 fof(mSetSort,axiom, % 50.93/50.99 ! [W0] : % 50.93/50.99 ( aSet0(W0) % 50.93/50.99 => $true ) ). % 50.93/50.99 % 50.93/50.99 fof(mEOfElem,axiom, % 50.93/50.99 ! [W0] : % 50.93/50.99 ( aSet0(W0) % 50.93/50.99 => ! [W1] : % 50.93/50.99 ( aElementOf0(W1,W0) % 50.93/50.99 => aElement0(W1) ) ) ). % 50.93/50.99 % 50.93/50.99 fof(mSetEq,axiom, % 50.93/50.99 ! [W0,W1] : % 50.93/50.99 ( ( aSet0(W0) % 50.93/50.99 & aSet0(W1) ) % 50.93/50.99 => ( ( ! [W2] : % 50.93/50.99 ( aElementOf0(W2,W0) % 50.93/50.99 => aElementOf0(W2,W1) ) % 50.93/50.99 & ! [W2] : % 50.93/50.99 ( aElementOf0(W2,W1) % 50.93/50.99 => aElementOf0(W2,W0) ) ) % 50.93/50.99 => W0 = W1 ) ) ). % 50.93/50.99 % 50.93/50.99 fof(mDefSSum,definition, % 50.93/50.99 ! [W0,W1] : % 50.93/50.99 ( ( aSet0(W0) % 50.93/50.99 & aSet0(W1) ) % 50.93/50.99 => ! [W2] : % 50.93/50.99 ( W2 = sdtpldt1(W0,W1) % 50.93/50.99 <=> ( aSet0(W2) % 50.93/50.99 & ! [W3] : % 50.93/50.99 ( aElementOf0(W3,W2) % 50.93/50.99 <=> ? [W4,W5] : % 50.93/50.99 ( aElementOf0(W4,W0) % 50.93/50.99 & aElementOf0(W5,W1) % 50.93/50.99 & sdtpldt0(W4,W5) = W3 ) ) ) ) ) ). % 50.93/50.99 % 50.93/50.99 fof(mDefSInt,definition, % 50.93/50.99 ! [W0,W1] : % 50.93/50.99 ( ( aSet0(W0) % 50.93/50.99 & aSet0(W1) ) % 50.93/50.99 => ! [W2] : % 50.93/50.99 ( W2 = sdtasasdt0(W0,W1) % 50.93/50.99 <=> ( aSet0(W2) % 50.93/50.99 & ! [W3] : % 50.93/50.99 ( aElementOf0(W3,W2) % 50.93/50.99 <=> ( aElementOf0(W3,W0) % 50.93/50.99 & aElementOf0(W3,W1) ) ) ) ) ) ). % 50.93/50.99 % 50.93/50.99 fof(mDefIdeal,definition, % 50.93/50.99 ! [W0] : % 50.93/50.99 ( aIdeal0(W0) % 50.93/50.99 <=> ( aSet0(W0) % 50.93/50.99 & ! [W1] : % 50.93/50.99 ( aElementOf0(W1,W0) % 50.93/50.99 => ( ! [W2] : % 50.93/50.99 ( aElementOf0(W2,W0) % 50.93/50.99 => aElementOf0(sdtpldt0(W1,W2),W0) ) % 50.93/50.99 & ! [W2] : % 50.93/50.99 ( aElement0(W2) % 50.93/50.99 => aElementOf0(sdtasdt0(W2,W1),W0) ) ) ) ) ) ). % 50.93/50.99 % 50.93/50.99 fof(mIdeSum,axiom, % 50.93/50.99 ! [W0,W1] : % 50.93/50.99 ( ( aIdeal0(W0) % 50.93/50.99 & aIdeal0(W1) ) % 50.93/50.99 => aIdeal0(sdtpldt1(W0,W1)) ) ). % 50.93/50.99 % 50.93/50.99 fof(mIdeInt,axiom, % 50.93/50.99 ! [W0,W1] : % 50.93/50.99 ( ( aIdeal0(W0) % 50.93/50.99 & aIdeal0(W1) ) % 50.93/50.99 => aIdeal0(sdtasasdt0(W0,W1)) ) ). % 50.93/50.99 % 50.93/50.99 fof(mDefMod,definition, % 50.93/50.99 ! [W0,W1,W2] : % 50.93/50.99 ( ( aElement0(W0) % 50.93/50.99 & aElement0(W1) % 50.93/50.99 & aIdeal0(W2) ) % 50.93/50.99 => ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 50.93/50.99 <=> aElementOf0(sdtpldt0(W0,smndt0(W1)),W2) ) ) ). % 50.93/50.99 % 50.93/50.99 fof(mChineseRemainder,axiom, % 50.93/50.99 ! [W0,W1] : % 50.93/50.99 ( ( aIdeal0(W0) % 50.93/50.99 & aIdeal0(W1) ) % 50.93/50.99 => ( ! [W2] : % 50.93/50.99 ( aElement0(W2) % 50.93/50.99 => aElementOf0(W2,sdtpldt1(W0,W1)) ) % 50.93/50.99 => ! [W2,W3] : % 50.93/50.99 ( ( aElement0(W2) % 50.93/50.99 & aElement0(W3) ) % 50.93/50.99 => ? [W4] : % 50.93/50.99 ( aElement0(W4) % 50.93/50.99 & sdteqdtlpzmzozddtrp0(W4,W2,W0) % 50.93/50.99 & sdteqdtlpzmzozddtrp0(W4,W3,W1) ) ) ) ) ). % 50.93/50.99 % 50.93/50.99 fof(mNatSort,axiom, % 50.93/50.99 ! [W0] : % 50.93/50.99 ( aNaturalNumber0(W0) % 50.93/50.99 => $true ) ). % 50.93/50.99 % 50.93/50.99 fof(mEucSort,axiom, % 50.93/50.99 ! [W0] : % 50.93/50.99 ( ( aElement0(W0) % 50.93/50.99 & W0 != sz00 ) % 50.93/50.99 => aNaturalNumber0(sbrdtbr0(W0)) ) ). % 50.93/50.99 % 50.93/50.99 fof(mNatLess,axiom, % 50.93/50.99 ! [W0,W1] : % 50.93/50.99 ( ( aNaturalNumber0(W0) % 50.93/50.99 & aNaturalNumber0(W1) ) % 50.93/50.99 => ( iLess0(W0,W1) % 50.93/50.99 => $true ) ) ). % 50.93/50.99 % 50.93/50.99 fof(mDivision,axiom, % 50.93/50.99 ! [W0,W1] : % 50.93/50.99 ( ( aElement0(W0) % 50.93/50.99 & aElement0(W1) % 50.93/50.99 & W1 != sz00 ) % 50.93/50.99 => ? [W2,W3] : % 50.93/50.99 ( aElement0(W2) % 50.93/50.99 & aElement0(W3) % 50.93/50.99 & W0 = sdtpldt0(sdtasdt0(W2,W1),W3) % 50.93/50.99 & ( W3 != sz00 % 50.93/50.99 => iLess0(sbrdtbr0(W3),sbrdtbr0(W1)) ) ) ) ). % 50.93/50.99 % 50.93/50.99 fof(mDefDiv,definition, % 50.93/50.99 ! [W0,W1] : % 50.93/50.99 ( ( aElement0(W0) % 50.93/50.99 & aElement0(W1) ) % 50.93/50.99 => ( doDivides0(W0,W1) % 50.93/50.99 <=> ? [W2] : % 50.93/50.99 ( aElement0(W2) % 50.93/50.99 & sdtasdt0(W0,W2) = W1 ) ) ) ). % 50.93/50.99 % 50.93/50.99 fof(mDefDvs,definition, % 50.93/50.99 ! [W0] : % 50.93/50.99 ( aElement0(W0) % 50.93/50.99 => ! [W1] : % 50.93/50.99 ( aDivisorOf0(W1,W0) % 50.93/50.99 <=> ( aElement0(W1) % 50.93/50.99 & doDivides0(W1,W0) ) ) ) ). % 50.93/50.99 % 50.93/50.99 fof(mDefGCD,definition, % 50.93/50.99 ! [W0,W1] : % 50.93/50.99 ( ( aElement0(W0) % 50.93/50.99 & aElement0(W1) ) % 50.93/50.99 => ! [W2] : % 50.93/50.99 ( aGcdOfAnd0(W2,W0,W1) % 50.93/50.99 <=> ( aDivisorOf0(W2,W0) % 50.93/50.99 & aDivisorOf0(W2,W1) % 50.93/50.99 & ! [W3] : % 50.93/50.99 ( ( aDivisorOf0(W3,W0) % 50.93/50.99 & aDivisorOf0(W3,W1) ) % 50.93/50.99 => doDivides0(W3,W2) ) ) ) ) ). % 50.93/50.99 % 50.93/50.99 fof(mDefRel,definition, % 50.93/50.99 ! [W0,W1] : % 50.93/50.99 ( ( aElement0(W0) % 50.93/50.99 & aElement0(W1) ) % 50.93/50.99 => ( misRelativelyPrime0(W0,W1) % 50.93/50.99 <=> aGcdOfAnd0(sz10,W0,W1) ) ) ). % 50.93/50.99 % 50.93/50.99 fof(mDefPrIdeal,definition, % 50.93/50.99 ! [W0] : % 50.93/50.99 ( aElement0(W0) % 50.93/50.99 => ! [W1] : % 50.93/50.99 ( W1 = slsdtgt0(W0) % 50.93/50.99 <=> ( aSet0(W1) % 50.93/50.99 & ! [W2] : % 50.93/50.99 ( aElementOf0(W2,W1) % 50.93/50.99 <=> ? [W3] : % 50.93/50.99 ( aElement0(W3) % 50.93/50.99 & sdtasdt0(W0,W3) = W2 ) ) ) ) ) ). % 50.93/50.99 % 50.93/50.99 fof(m__1905,hypothesis, % 50.93/50.99 aElement0(xc) ). % 50.93/50.99 % 50.93/50.99 fof(m__1933,hypothesis, % 50.93/50.99 ( aElementOf0(xx,slsdtgt0(xc)) % 50.93/50.99 & aElementOf0(xy,slsdtgt0(xc)) % 50.93/50.99 & aElement0(xz) ) ). % 50.93/50.99 % 50.93/50.99 fof(m__1956,hypothesis, % 50.93/50.99 ( aElement0(xu) % 50.93/50.99 & sdtasdt0(xc,xu) = xx ) ). % 50.93/50.99 % 50.93/51.00 fof(m__,conjecture, % 50.93/51.00 ? [W0] : % 50.93/51.00 ( aElement0(W0) % 50.93/51.00 & sdtasdt0(xc,W0) = xy ) ). % 50.93/51.00 % 50.93/51.00 %------------------------------------------------------------------------------ % 50.93/51.00 %------------------------------------------- % 50.93/51.00 % Proof found % 50.93/51.00 % SZS status Theorem for theBenchmark % 50.93/51.00 % SZS output start Proof % 50.93/51.00 %ClaNum:178(EqnAxiom:83) % 50.93/51.00 %VarNum:701(SingletonVarNum:213) % 50.93/51.00 %MaxLitNum:8 % 50.93/51.00 %MaxfuncDepth:2 % 50.93/51.00 %SharedTerms:19 % 50.93/51.00 %goalClause: 103 % 50.93/51.00 [84]P1(a1) % 50.93/51.00 [85]P1(a29) % 50.93/51.00 [86]P1(a30) % 50.93/51.00 [87]P1(a31) % 50.93/51.00 [88]P1(a32) % 50.93/51.00 [92]~E(a1,a29) % 50.93/51.00 [89]E(f2(a30,a32),a33) % 50.93/51.00 [90]P3(a33,f25(a30)) % 50.93/51.00 [91]P3(a34,f25(a30)) % 50.93/51.00 [93]~P5(x931)+P4(x931) % 50.93/51.00 [94]~P1(x941)+P1(f28(x941)) % 50.93/51.00 [96]~P1(x961)+E(f2(a1,x961),a1) % 50.93/51.00 [97]~P1(x971)+E(f2(x971,a1),a1) % 50.93/51.00 [99]~P1(x991)+E(f26(a1,x991),x991) % 50.93/51.00 [100]~P1(x1001)+E(f2(a29,x1001),x1001) % 50.93/51.00 [101]~P1(x1011)+E(f26(x1011,a1),x1011) % 50.93/51.00 [102]~P1(x1021)+E(f2(x1021,a29),x1021) % 50.93/51.00 [103]~P1(x1031)+~E(f2(a30,x1031),a34) % 50.93/51.00 [104]~P1(x1041)+E(f26(f28(x1041),x1041),a1) % 50.93/51.00 [105]~P1(x1051)+E(f26(x1051,f28(x1051)),a1) % 50.93/51.00 [106]~P1(x1061)+E(f2(x1061,f28(a29)),f28(x1061)) % 50.93/51.00 [107]~P1(x1071)+E(f2(f28(a29),x1071),f28(x1071)) % 50.93/51.00 [95]~P1(x951)+E(x951,a1)+P7(f3(x951)) % 50.93/51.00 [108]~P4(x1081)+P5(x1081)+P3(f4(x1081),x1081) % 50.93/51.00 [109]~P3(x1091,x1092)+P1(x1091)+~P4(x1092) % 50.93/51.00 [110]~P2(x1101,x1102)+P1(x1101)+~P1(x1102) % 50.93/51.00 [117]~P1(x1172)+~P2(x1171,x1172)+P8(x1171,x1172) % 50.93/51.00 [98]~P1(x982)+P4(x981)+~E(x981,f25(x982)) % 50.93/51.00 [112]~P1(x1122)+~P1(x1121)+E(f26(x1121,x1122),f26(x1122,x1121)) % 50.93/51.00 [113]~P1(x1132)+~P1(x1131)+E(f2(x1131,x1132),f2(x1132,x1131)) % 50.93/51.00 [118]~P1(x1182)+~P1(x1181)+P1(f26(x1181,x1182)) % 50.93/51.00 [119]~P1(x1192)+~P1(x1191)+P1(f2(x1191,x1192)) % 50.93/51.00 [120]~P5(x1202)+~P5(x1201)+P5(f27(x1201,x1202)) % 50.93/51.00 [121]~P5(x1212)+~P5(x1211)+P5(f24(x1211,x1212)) % 50.93/51.00 [116]~P4(x1161)+P5(x1161)+P3(f6(x1161),x1161)+P1(f5(x1161)) % 50.93/51.00 [147]~P4(x1471)+P5(x1471)+P1(f5(x1471))+~P3(f26(f4(x1471),f6(x1471)),x1471) % 50.93/51.00 [150]~P4(x1501)+P5(x1501)+P3(f6(x1501),x1501)+~P3(f2(f5(x1501),f4(x1501)),x1501) % 50.93/51.00 [159]~P4(x1591)+P5(x1591)+~P3(f26(f4(x1591),f6(x1591)),x1591)+~P3(f2(f5(x1591),f4(x1591)),x1591) % 50.93/51.00 [124]~P1(x1242)+~P1(x1241)+~P8(x1241,x1242)+P2(x1241,x1242) % 50.93/51.00 [132]~P1(x1322)+~P1(x1321)+~P9(x1321,x1322)+P6(a29,x1321,x1322) % 50.93/51.00 [140]~P1(x1402)+~P1(x1401)+P9(x1401,x1402)+~P6(a29,x1401,x1402) % 50.93/51.00 [122]~P1(x1221)+~P1(x1222)+E(x1221,a1)+P1(f7(x1222,x1221)) % 50.93/51.00 [123]~P1(x1231)+~P1(x1232)+E(x1231,a1)+P1(f10(x1232,x1231)) % 50.93/51.00 [127]~P1(x1272)+~P1(x1271)+~P8(x1271,x1272)+P1(f11(x1271,x1272)) % 50.93/51.00 [131]~P1(x1312)+~P1(x1311)+~P8(x1311,x1312)+E(f2(x1311,f11(x1311,x1312)),x1312) % 50.93/51.00 [152]~P1(x1521)+~P1(x1522)+E(x1521,a1)+E(f26(f2(f7(x1522,x1521),x1521),f10(x1522,x1521)),x1522) % 50.93/51.00 [142]~P1(x1422)+~P6(x1421,x1423,x1422)+P2(x1421,x1422)+~P1(x1423) % 50.93/51.00 [143]~P1(x1432)+~P6(x1431,x1432,x1433)+P2(x1431,x1432)+~P1(x1433) % 50.93/51.00 [114]~P4(x1143)+~P4(x1142)+P4(x1141)+~E(x1141,f27(x1142,x1143)) % 50.93/51.00 [115]~P4(x1153)+~P4(x1152)+P4(x1151)+~E(x1151,f24(x1152,x1153)) % 50.93/51.00 [130]~P1(x1301)+~P5(x1303)+~P3(x1302,x1303)+P3(f2(x1301,x1302),x1303) % 50.93/51.00 [134]~P5(x1343)+~P3(x1341,x1343)+~P3(x1342,x1343)+P3(f26(x1341,x1342),x1343) % 50.93/51.00 [154]~P1(x1541)+~P3(x1543,x1542)+~E(x1542,f25(x1541))+P1(f14(x1541,x1542,x1543)) % 50.93/51.00 [137]~P1(x1373)+~P1(x1372)+~P1(x1371)+E(f26(f26(x1371,x1372),x1373),f26(x1371,f26(x1372,x1373))) % 50.93/51.00 [138]~P1(x1383)+~P1(x1382)+~P1(x1381)+E(f2(f2(x1381,x1382),x1383),f2(x1381,f2(x1382,x1383))) % 50.93/51.00 [148]~P1(x1483)+~P1(x1482)+~P1(x1481)+E(f26(f2(x1481,x1482),f2(x1481,x1483)),f2(x1481,f26(x1482,x1483))) % 50.93/51.00 [149]~P1(x1492)+~P1(x1493)+~P1(x1491)+E(f26(f2(x1491,x1492),f2(x1493,x1492)),f2(f26(x1491,x1493),x1492)) % 50.93/51.00 [156]~P1(x1561)+~P3(x1563,x1562)+~E(x1562,f25(x1561))+E(f2(x1561,f14(x1561,x1562,x1563)),x1563) % 50.93/51.00 [111]~P1(x1111)+~P1(x1112)+E(x1111,a1)+E(x1112,a1)+~E(f2(x1112,x1111),a1) % 50.93/51.00 [133]~P1(x1332)+~P4(x1331)+P3(f13(x1332,x1331),x1331)+E(x1331,f25(x1332))+P1(f12(x1332,x1331)) % 50.93/51.00 [135]~P4(x1352)+~P4(x1351)+E(x1351,x1352)+P3(f16(x1351,x1352),x1351)+P3(f17(x1351,x1352),x1352) % 50.93/51.00 [144]~P4(x1442)+~P4(x1441)+E(x1441,x1442)+P3(f16(x1441,x1442),x1441)+~P3(f17(x1441,x1442),x1441) % 50.93/51.00 [145]~P4(x1452)+~P4(x1451)+E(x1451,x1452)+P3(f17(x1451,x1452),x1452)+~P3(f16(x1451,x1452),x1452) % 50.93/51.00 [153]~P4(x1532)+~P4(x1531)+E(x1531,x1532)+~P3(f16(x1531,x1532),x1532)+~P3(f17(x1531,x1532),x1531) % 50.93/51.00 [139]~P1(x1391)+~P1(x1392)+E(x1391,a1)+P10(f3(f10(x1392,x1391)),f3(x1391))+E(f10(x1392,x1391),a1) % 50.93/51.00 [141]~P1(x1412)+~P4(x1411)+P3(f13(x1412,x1411),x1411)+E(x1411,f25(x1412))+E(f2(x1412,f12(x1412,x1411)),f13(x1412,x1411)) % 50.93/51.00 [125]~P1(x1252)+~P1(x1251)+~P1(x1253)+P8(x1251,x1252)+~E(f2(x1251,x1253),x1252) % 50.93/51.00 [155]~P1(x1552)+~P1(x1551)+~P5(x1553)+P11(x1551,x1552,x1553)+~P3(f26(x1551,f28(x1552)),x1553) % 50.93/51.00 [157]~P1(x1572)+~P1(x1571)+~P5(x1573)+~P11(x1571,x1572,x1573)+P3(f26(x1571,f28(x1572)),x1573) % 50.93/51.00 [126]~P1(x1263)+~P1(x1264)+P3(x1261,x1262)+~E(f2(x1263,x1264),x1261)+~E(x1262,f25(x1263)) % 50.93/51.00 [128]~P4(x1284)+~P4(x1282)+~P3(x1281,x1283)+P3(x1281,x1282)+~E(x1283,f24(x1284,x1282)) % 50.93/51.00 [129]~P4(x1294)+~P4(x1292)+~P3(x1291,x1293)+P3(x1291,x1292)+~E(x1293,f24(x1292,x1294)) % 50.93/51.00 [170]~P4(x1702)+~P4(x1701)+~P3(x1704,x1703)+~E(x1703,f27(x1701,x1702))+P3(f19(x1701,x1702,x1703,x1704),x1701) % 50.93/51.00 [171]~P4(x1712)+~P4(x1711)+~P3(x1714,x1713)+~E(x1713,f27(x1711,x1712))+P3(f20(x1711,x1712,x1713,x1714),x1712) % 50.93/51.00 [178]~P4(x1782)+~P4(x1781)+~P3(x1784,x1783)+~E(x1783,f27(x1781,x1782))+E(f26(f19(x1781,x1782,x1783,x1784),f20(x1781,x1782,x1783,x1784)),x1784) % 50.93/51.00 [151]~P1(x1513)+~P1(x1512)+~P4(x1511)+~P3(f13(x1512,x1511),x1511)+~E(f13(x1512,x1511),f2(x1512,x1513))+E(x1511,f25(x1512)) % 50.93/51.00 [160]~P1(x1603)+~P1(x1602)+~P2(x1601,x1603)+~P2(x1601,x1602)+P6(x1601,x1602,x1603)+P2(f15(x1602,x1603,x1601),x1603) % 50.93/51.00 [161]~P1(x1613)+~P1(x1612)+~P2(x1611,x1613)+~P2(x1611,x1612)+P6(x1611,x1612,x1613)+P2(f15(x1612,x1613,x1611),x1612) % 50.93/51.00 [162]~P4(x1621)+~P4(x1623)+~P4(x1622)+P3(f18(x1622,x1623,x1621),x1621)+P3(f21(x1622,x1623,x1621),x1622)+E(x1621,f27(x1622,x1623)) % 50.93/51.00 [163]~P4(x1631)+~P4(x1633)+~P4(x1632)+P3(f18(x1632,x1633,x1631),x1631)+P3(f22(x1632,x1633,x1631),x1633)+E(x1631,f27(x1632,x1633)) % 50.93/51.00 [164]~P4(x1641)+~P4(x1643)+~P4(x1642)+P3(f23(x1642,x1643,x1641),x1641)+P3(f23(x1642,x1643,x1641),x1643)+E(x1641,f24(x1642,x1643)) % 50.93/51.00 [165]~P4(x1651)+~P4(x1653)+~P4(x1652)+P3(f23(x1652,x1653,x1651),x1651)+P3(f23(x1652,x1653,x1651),x1652)+E(x1651,f24(x1652,x1653)) % 50.93/51.00 [166]~P1(x1663)+~P1(x1662)+~P2(x1661,x1663)+~P2(x1661,x1662)+P6(x1661,x1662,x1663)+~P8(f15(x1662,x1663,x1661),x1661) % 50.93/51.00 [168]~P4(x1681)+~P4(x1683)+~P4(x1682)+P3(f18(x1682,x1683,x1681),x1681)+E(x1681,f27(x1682,x1683))+E(f26(f21(x1682,x1683,x1681),f22(x1682,x1683,x1681)),f18(x1682,x1683,x1681)) % 50.93/51.00 [158]~P2(x1581,x1583)+~P2(x1581,x1584)+~P6(x1582,x1584,x1583)+P8(x1581,x1582)+~P1(x1583)+~P1(x1584) % 50.93/51.00 [136]~P4(x1364)+~P4(x1363)+~P3(x1361,x1364)+~P3(x1361,x1363)+P3(x1361,x1362)+~E(x1362,f24(x1363,x1364)) % 50.93/51.00 [169]~P1(x1694)+~P1(x1693)+~P5(x1692)+~P5(x1691)+P1(f8(x1691,x1692))+P1(f9(x1691,x1692,x1693,x1694)) % 50.93/51.00 [172]~P1(x1724)+~P1(x1723)+~P5(x1722)+~P5(x1721)+P11(f9(x1721,x1722,x1723,x1724),x1724,x1722)+P1(f8(x1721,x1722)) % 50.93/51.00 [173]~P1(x1734)+~P1(x1733)+~P5(x1732)+~P5(x1731)+P11(f9(x1731,x1732,x1733,x1734),x1733,x1731)+P1(f8(x1731,x1732)) % 50.93/51.00 [175]~P1(x1754)+~P1(x1753)+~P5(x1752)+~P5(x1751)+~P3(f8(x1751,x1752),f27(x1751,x1752))+P1(f9(x1751,x1752,x1753,x1754)) % 50.93/51.00 [176]~P1(x1764)+~P1(x1763)+~P5(x1762)+~P5(x1761)+P11(f9(x1761,x1762,x1763,x1764),x1764,x1762)+~P3(f8(x1761,x1762),f27(x1761,x1762)) % 50.93/51.00 [177]~P1(x1774)+~P1(x1773)+~P5(x1772)+~P5(x1771)+P11(f9(x1771,x1772,x1773,x1774),x1773,x1771)+~P3(f8(x1771,x1772),f27(x1771,x1772)) % 50.93/51.00 [174]~P4(x1741)+~P4(x1743)+~P4(x1742)+~P3(f23(x1742,x1743,x1741),x1741)+~P3(f23(x1742,x1743,x1741),x1743)+~P3(f23(x1742,x1743,x1741),x1742)+E(x1741,f24(x1742,x1743)) % 50.93/51.00 [146]~P4(x1464)+~P4(x1463)+~P3(x1466,x1464)+~P3(x1465,x1463)+P3(x1461,x1462)+~E(x1462,f27(x1463,x1464))+~E(f26(x1465,x1466),x1461) % 50.93/51.00 [167]~P4(x1671)+~P4(x1673)+~P4(x1672)+~P3(x1675,x1673)+~P3(x1674,x1672)+~P3(f18(x1672,x1673,x1671),x1671)+E(x1671,f27(x1672,x1673))+~E(f26(x1674,x1675),f18(x1672,x1673,x1671)) % 50.93/51.00 %EqnAxiom % 50.93/51.00 [1]E(x11,x11) % 50.93/51.00 [2]E(x22,x21)+~E(x21,x22) % 50.93/51.00 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 50.93/51.00 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 50.93/51.00 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 50.93/51.00 [6]~E(x61,x62)+E(f25(x61),f25(x62)) % 50.93/51.00 [7]~E(x71,x72)+E(f21(x71,x73,x74),f21(x72,x73,x74)) % 50.93/51.00 [8]~E(x81,x82)+E(f21(x83,x81,x84),f21(x83,x82,x84)) % 50.93/51.00 [9]~E(x91,x92)+E(f21(x93,x94,x91),f21(x93,x94,x92)) % 50.93/51.00 [10]~E(x101,x102)+E(f28(x101),f28(x102)) % 50.93/51.00 [11]~E(x111,x112)+E(f3(x111),f3(x112)) % 50.93/51.00 [12]~E(x121,x122)+E(f27(x121,x123),f27(x122,x123)) % 50.93/51.00 [13]~E(x131,x132)+E(f27(x133,x131),f27(x133,x132)) % 50.93/51.00 [14]~E(x141,x142)+E(f26(x141,x143),f26(x142,x143)) % 50.93/51.00 [15]~E(x151,x152)+E(f26(x153,x151),f26(x153,x152)) % 50.93/51.00 [16]~E(x161,x162)+E(f15(x161,x163,x164),f15(x162,x163,x164)) % 50.93/51.00 [17]~E(x171,x172)+E(f15(x173,x171,x174),f15(x173,x172,x174)) % 50.93/51.00 [18]~E(x181,x182)+E(f15(x183,x184,x181),f15(x183,x184,x182)) % 50.93/51.00 [19]~E(x191,x192)+E(f14(x191,x193,x194),f14(x192,x193,x194)) % 50.93/51.00 [20]~E(x201,x202)+E(f14(x203,x201,x204),f14(x203,x202,x204)) % 50.93/51.00 [21]~E(x211,x212)+E(f14(x213,x214,x211),f14(x213,x214,x212)) % 50.93/51.00 [22]~E(x221,x222)+E(f20(x221,x223,x224,x225),f20(x222,x223,x224,x225)) % 50.93/51.00 [23]~E(x231,x232)+E(f20(x233,x231,x234,x235),f20(x233,x232,x234,x235)) % 50.93/51.00 [24]~E(x241,x242)+E(f20(x243,x244,x241,x245),f20(x243,x244,x242,x245)) % 50.93/51.00 [25]~E(x251,x252)+E(f20(x253,x254,x255,x251),f20(x253,x254,x255,x252)) % 50.93/51.00 [26]~E(x261,x262)+E(f9(x261,x263,x264,x265),f9(x262,x263,x264,x265)) % 50.93/51.00 [27]~E(x271,x272)+E(f9(x273,x271,x274,x275),f9(x273,x272,x274,x275)) % 50.93/51.00 [28]~E(x281,x282)+E(f9(x283,x284,x281,x285),f9(x283,x284,x282,x285)) % 50.93/51.00 [29]~E(x291,x292)+E(f9(x293,x294,x295,x291),f9(x293,x294,x295,x292)) % 50.93/51.00 [30]~E(x301,x302)+E(f19(x301,x303,x304,x305),f19(x302,x303,x304,x305)) % 50.93/51.00 [31]~E(x311,x312)+E(f19(x313,x311,x314,x315),f19(x313,x312,x314,x315)) % 50.93/51.00 [32]~E(x321,x322)+E(f19(x323,x324,x321,x325),f19(x323,x324,x322,x325)) % 50.93/51.00 [33]~E(x331,x332)+E(f19(x333,x334,x335,x331),f19(x333,x334,x335,x332)) % 50.93/51.00 [34]~E(x341,x342)+E(f23(x341,x343,x344),f23(x342,x343,x344)) % 50.93/51.00 [35]~E(x351,x352)+E(f23(x353,x351,x354),f23(x353,x352,x354)) % 50.93/51.00 [36]~E(x361,x362)+E(f23(x363,x364,x361),f23(x363,x364,x362)) % 50.93/51.00 [37]~E(x371,x372)+E(f24(x371,x373),f24(x372,x373)) % 50.93/51.00 [38]~E(x381,x382)+E(f24(x383,x381),f24(x383,x382)) % 50.93/51.00 [39]~E(x391,x392)+E(f5(x391),f5(x392)) % 50.93/51.00 [40]~E(x401,x402)+E(f4(x401),f4(x402)) % 50.93/51.00 [41]~E(x411,x412)+E(f17(x411,x413),f17(x412,x413)) % 50.93/51.00 [42]~E(x421,x422)+E(f17(x423,x421),f17(x423,x422)) % 50.93/51.00 [43]~E(x431,x432)+E(f16(x431,x433),f16(x432,x433)) % 50.93/51.00 [44]~E(x441,x442)+E(f16(x443,x441),f16(x443,x442)) % 50.93/51.00 [45]~E(x451,x452)+E(f8(x451,x453),f8(x452,x453)) % 50.93/51.00 [46]~E(x461,x462)+E(f8(x463,x461),f8(x463,x462)) % 50.93/51.00 [47]~E(x471,x472)+E(f13(x471,x473),f13(x472,x473)) % 50.93/51.00 [48]~E(x481,x482)+E(f13(x483,x481),f13(x483,x482)) % 50.93/51.00 [49]~E(x491,x492)+E(f22(x491,x493,x494),f22(x492,x493,x494)) % 50.93/51.00 [50]~E(x501,x502)+E(f22(x503,x501,x504),f22(x503,x502,x504)) % 50.93/51.00 [51]~E(x511,x512)+E(f22(x513,x514,x511),f22(x513,x514,x512)) % 50.93/51.00 [52]~E(x521,x522)+E(f6(x521),f6(x522)) % 50.93/51.00 [53]~E(x531,x532)+E(f18(x531,x533,x534),f18(x532,x533,x534)) % 50.93/51.00 [54]~E(x541,x542)+E(f18(x543,x541,x544),f18(x543,x542,x544)) % 50.93/51.00 [55]~E(x551,x552)+E(f18(x553,x554,x551),f18(x553,x554,x552)) % 50.93/51.00 [56]~E(x561,x562)+E(f10(x561,x563),f10(x562,x563)) % 50.93/51.00 [57]~E(x571,x572)+E(f10(x573,x571),f10(x573,x572)) % 50.93/51.00 [58]~E(x581,x582)+E(f7(x581,x583),f7(x582,x583)) % 50.93/51.00 [59]~E(x591,x592)+E(f7(x593,x591),f7(x593,x592)) % 50.93/51.00 [60]~E(x601,x602)+E(f12(x601,x603),f12(x602,x603)) % 50.93/51.00 [61]~E(x611,x612)+E(f12(x613,x611),f12(x613,x612)) % 50.93/51.00 [62]~E(x621,x622)+E(f11(x621,x623),f11(x622,x623)) % 50.93/51.00 [63]~E(x631,x632)+E(f11(x633,x631),f11(x633,x632)) % 50.93/51.00 [64]~P1(x641)+P1(x642)+~E(x641,x642) % 50.93/51.00 [65]P3(x652,x653)+~E(x651,x652)+~P3(x651,x653) % 50.93/51.00 [66]P3(x663,x662)+~E(x661,x662)+~P3(x663,x661) % 50.93/51.00 [67]~P4(x671)+P4(x672)+~E(x671,x672) % 50.93/51.00 [68]P10(x682,x683)+~E(x681,x682)+~P10(x681,x683) % 50.93/51.00 [69]P10(x693,x692)+~E(x691,x692)+~P10(x693,x691) % 50.93/51.00 [70]~P5(x701)+P5(x702)+~E(x701,x702) % 50.93/51.00 [71]P2(x712,x713)+~E(x711,x712)+~P2(x711,x713) % 50.93/51.00 [72]P2(x723,x722)+~E(x721,x722)+~P2(x723,x721) % 50.93/51.00 [73]P11(x732,x733,x734)+~E(x731,x732)+~P11(x731,x733,x734) % 50.93/51.00 [74]P11(x743,x742,x744)+~E(x741,x742)+~P11(x743,x741,x744) % 50.93/51.00 [75]P11(x753,x754,x752)+~E(x751,x752)+~P11(x753,x754,x751) % 50.93/51.00 [76]P9(x762,x763)+~E(x761,x762)+~P9(x761,x763) % 50.93/51.00 [77]P9(x773,x772)+~E(x771,x772)+~P9(x773,x771) % 50.93/51.00 [78]P6(x782,x783,x784)+~E(x781,x782)+~P6(x781,x783,x784) % 50.93/51.00 [79]P6(x793,x792,x794)+~E(x791,x792)+~P6(x793,x791,x794) % 50.93/51.00 [80]P6(x803,x804,x802)+~E(x801,x802)+~P6(x803,x804,x801) % 50.93/51.00 [81]P8(x812,x813)+~E(x811,x812)+~P8(x811,x813) % 50.93/51.00 [82]P8(x823,x822)+~E(x821,x822)+~P8(x823,x821) % 50.93/51.00 [83]~P7(x831)+P7(x832)+~E(x831,x832) % 50.93/51.00 % 50.93/51.00 %------------------------------------------- % 50.93/51.00 cnf(186,plain, % 50.93/51.00 (~P1(x1861)+~P3(x1862,f25(x1861))+P1(f14(x1861,f25(x1861),x1862))), % 50.93/51.00 inference(equality_inference,[],[154])). % 50.93/51.00 cnf(187,plain, % 50.93/51.00 (~P1(x1871)+~P3(x1872,f25(x1871))+E(f2(x1871,f14(x1871,f25(x1871),x1872)),x1872)), % 50.93/51.00 inference(equality_inference,[],[156])). % 50.93/51.00 cnf(4241,plain, % 50.93/51.00 (P1(f14(a30,f25(a30),a34))), % 50.93/51.00 inference(scs_inference,[],[86,91,186])). % 50.93/51.00 cnf(4258,plain, % 50.93/51.00 ($false), % 50.93/51.00 inference(scs_inference,[],[86,4241,91,90,186,187,103]), % 50.93/51.00 ['proof']). % 50.93/51.00 % SZS output end Proof % 50.93/51.00 % Total time :50.300000s %------------------------------------------------------------------------------