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