%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : RNG105+2 : 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 : n005.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:06 EDT 2024 % Result : Theorem 13.58s 13.64s % Output : CNFRefutation 13.58s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : RNG105+2 : TPTP v8.2.0. Released v4.0.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n005.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:30:08 EDT 2024 % 0.19/0.33 % CPUTime : % 0.20/0.55 start to proof:theBenchmark % 13.58/13.62 %------------------------------------------- % 13.58/13.62 % File :CSE---1.7 % 13.58/13.62 % Problem :theBenchmark % 13.58/13.62 % Transform :cnf % 13.58/13.62 % Format :tptp:raw % 13.58/13.62 % Command :java -jar mcs_scs.jar %d %s % 13.58/13.62 % 13.58/13.62 % Result :Theorem 13.010000s % 13.58/13.62 % Output :CNFRefutation 13.010000s % 13.58/13.62 %------------------------------------------- % 13.58/13.63 %------------------------------------------------------------------------------ % 13.58/13.63 % File : RNG105+2 : TPTP v8.2.0. Released v4.0.0. % 13.58/13.63 % Domain : Ring Theory % 13.58/13.63 % Problem : Chinese remainder theorem in a ring 06_05, 01 expansion % 13.58/13.63 % Version : Especial. % 13.58/13.63 % English : % 13.58/13.63 % 13.58/13.63 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 13.58/13.63 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 13.58/13.63 % Source : [Pas08] % 13.58/13.63 % Names : chines_06_05.01 [Pas08] % 13.58/13.63 % 13.58/13.63 % Status : Theorem % 13.58/13.63 % Rating : 0.25 v8.2.0, 0.22 v8.1.0, 0.17 v7.5.0, 0.19 v7.4.0, 0.17 v7.3.0, 0.21 v7.2.0, 0.17 v7.1.0, 0.22 v7.0.0, 0.17 v6.4.0, 0.23 v6.3.0, 0.25 v6.2.0, 0.24 v6.1.0, 0.30 v5.5.0, 0.37 v5.4.0, 0.43 v5.3.0, 0.44 v5.2.0, 0.35 v5.1.0, 0.48 v5.0.0, 0.54 v4.1.0, 0.57 v4.0.1, 0.83 v4.0.0 % 13.58/13.63 % Syntax : Number of formulae : 44 ( 6 unt; 9 def) % 13.58/13.63 % Number of atoms : 170 ( 39 equ) % 13.58/13.63 % Maximal formula atoms : 9 ( 3 avg) % 13.58/13.63 % Number of connectives : 130 ( 4 ~; 3 |; 64 &) % 13.58/13.63 % ( 12 <=>; 47 =>; 0 <=; 0 <~>) % 13.58/13.63 % Maximal formula depth : 13 ( 5 avg) % 13.58/13.63 % Maximal term depth : 3 ( 1 avg) % 13.58/13.63 % Number of predicates : 13 ( 11 usr; 1 prp; 0-3 aty) % 13.58/13.63 % Number of functors : 15 ( 15 usr; 8 con; 0-2 aty) % 13.58/13.63 % Number of variables : 87 ( 76 !; 11 ?) % 13.58/13.63 % SPC : FOF_THM_RFO_SEQ % 13.58/13.63 % 13.58/13.63 % Comments : Problem generated by the SAD system [VLP07] % 13.58/13.63 %------------------------------------------------------------------------------ % 13.58/13.63 fof(mElmSort,axiom, % 13.58/13.63 ! [W0] : % 13.58/13.63 ( aElement0(W0) % 13.58/13.63 => $true ) ). % 13.58/13.63 % 13.58/13.63 fof(mSortsC,axiom, % 13.58/13.63 aElement0(sz00) ). % 13.58/13.63 % 13.58/13.63 fof(mSortsC_01,axiom, % 13.58/13.63 aElement0(sz10) ). % 13.58/13.63 % 13.58/13.63 fof(mSortsU,axiom, % 13.58/13.63 ! [W0] : % 13.58/13.63 ( aElement0(W0) % 13.58/13.63 => aElement0(smndt0(W0)) ) ). % 13.58/13.63 % 13.58/13.63 fof(mSortsB,axiom, % 13.58/13.63 ! [W0,W1] : % 13.58/13.63 ( ( aElement0(W0) % 13.58/13.63 & aElement0(W1) ) % 13.58/13.63 => aElement0(sdtpldt0(W0,W1)) ) ). % 13.58/13.63 % 13.58/13.63 fof(mSortsB_02,axiom, % 13.58/13.63 ! [W0,W1] : % 13.58/13.63 ( ( aElement0(W0) % 13.58/13.63 & aElement0(W1) ) % 13.58/13.63 => aElement0(sdtasdt0(W0,W1)) ) ). % 13.58/13.63 % 13.58/13.63 fof(mAddComm,axiom, % 13.58/13.63 ! [W0,W1] : % 13.58/13.63 ( ( aElement0(W0) % 13.58/13.63 & aElement0(W1) ) % 13.58/13.63 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 13.58/13.63 % 13.58/13.63 fof(mAddAsso,axiom, % 13.58/13.63 ! [W0,W1,W2] : % 13.58/13.63 ( ( aElement0(W0) % 13.58/13.63 & aElement0(W1) % 13.58/13.63 & aElement0(W2) ) % 13.58/13.63 => sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) ). % 13.58/13.63 % 13.58/13.63 fof(mAddZero,axiom, % 13.58/13.63 ! [W0] : % 13.58/13.63 ( aElement0(W0) % 13.58/13.63 => ( sdtpldt0(W0,sz00) = W0 % 13.58/13.63 & W0 = sdtpldt0(sz00,W0) ) ) ). % 13.58/13.63 % 13.58/13.63 fof(mAddInvr,axiom, % 13.58/13.63 ! [W0] : % 13.58/13.63 ( aElement0(W0) % 13.58/13.63 => ( sdtpldt0(W0,smndt0(W0)) = sz00 % 13.58/13.63 & sz00 = sdtpldt0(smndt0(W0),W0) ) ) ). % 13.58/13.63 % 13.58/13.63 fof(mMulComm,axiom, % 13.58/13.63 ! [W0,W1] : % 13.58/13.63 ( ( aElement0(W0) % 13.58/13.63 & aElement0(W1) ) % 13.58/13.63 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 13.58/13.63 % 13.58/13.63 fof(mMulAsso,axiom, % 13.58/13.63 ! [W0,W1,W2] : % 13.58/13.63 ( ( aElement0(W0) % 13.58/13.63 & aElement0(W1) % 13.58/13.63 & aElement0(W2) ) % 13.58/13.63 => sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) ). % 13.58/13.63 % 13.58/13.63 fof(mMulUnit,axiom, % 13.58/13.63 ! [W0] : % 13.58/13.63 ( aElement0(W0) % 13.58/13.63 => ( sdtasdt0(W0,sz10) = W0 % 13.58/13.63 & W0 = sdtasdt0(sz10,W0) ) ) ). % 13.58/13.63 % 13.58/13.63 fof(mAMDistr,axiom, % 13.58/13.63 ! [W0,W1,W2] : % 13.58/13.63 ( ( aElement0(W0) % 13.58/13.63 & aElement0(W1) % 13.58/13.63 & aElement0(W2) ) % 13.58/13.63 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 13.58/13.63 & sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ). % 13.58/13.63 % 13.58/13.63 fof(mMulMnOne,axiom, % 13.58/13.63 ! [W0] : % 13.58/13.63 ( aElement0(W0) % 13.58/13.64 => ( sdtasdt0(smndt0(sz10),W0) = smndt0(W0) % 13.58/13.64 & smndt0(W0) = sdtasdt0(W0,smndt0(sz10)) ) ) ). % 13.58/13.64 % 13.58/13.64 fof(mMulZero,axiom, % 13.58/13.64 ! [W0] : % 13.58/13.64 ( aElement0(W0) % 13.58/13.64 => ( sdtasdt0(W0,sz00) = sz00 % 13.58/13.64 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 13.58/13.64 % 13.58/13.64 fof(mCancel,axiom, % 13.58/13.64 ! [W0,W1] : % 13.58/13.64 ( ( aElement0(W0) % 13.58/13.64 & aElement0(W1) ) % 13.58/13.64 => ( sdtasdt0(W0,W1) = sz00 % 13.58/13.64 => ( W0 = sz00 % 13.58/13.64 | W1 = sz00 ) ) ) ). % 13.58/13.64 % 13.58/13.64 fof(mUnNeZr,axiom, % 13.58/13.64 sz10 != sz00 ). % 13.58/13.64 % 13.58/13.64 fof(mSetSort,axiom, % 13.58/13.64 ! [W0] : % 13.58/13.64 ( aSet0(W0) % 13.58/13.64 => $true ) ). % 13.58/13.64 % 13.58/13.64 fof(mEOfElem,axiom, % 13.58/13.64 ! [W0] : % 13.58/13.64 ( aSet0(W0) % 13.58/13.64 => ! [W1] : % 13.58/13.64 ( aElementOf0(W1,W0) % 13.58/13.64 => aElement0(W1) ) ) ). % 13.58/13.64 % 13.58/13.64 fof(mSetEq,axiom, % 13.58/13.64 ! [W0,W1] : % 13.58/13.64 ( ( aSet0(W0) % 13.58/13.64 & aSet0(W1) ) % 13.58/13.64 => ( ( ! [W2] : % 13.58/13.64 ( aElementOf0(W2,W0) % 13.58/13.64 => aElementOf0(W2,W1) ) % 13.58/13.64 & ! [W2] : % 13.58/13.64 ( aElementOf0(W2,W1) % 13.58/13.64 => aElementOf0(W2,W0) ) ) % 13.58/13.64 => W0 = W1 ) ) ). % 13.58/13.64 % 13.58/13.64 fof(mDefSSum,definition, % 13.58/13.64 ! [W0,W1] : % 13.58/13.64 ( ( aSet0(W0) % 13.58/13.64 & aSet0(W1) ) % 13.58/13.64 => ! [W2] : % 13.58/13.64 ( W2 = sdtpldt1(W0,W1) % 13.58/13.64 <=> ( aSet0(W2) % 13.58/13.64 & ! [W3] : % 13.58/13.64 ( aElementOf0(W3,W2) % 13.58/13.64 <=> ? [W4,W5] : % 13.58/13.64 ( aElementOf0(W4,W0) % 13.58/13.64 & aElementOf0(W5,W1) % 13.58/13.64 & sdtpldt0(W4,W5) = W3 ) ) ) ) ) ). % 13.58/13.64 % 13.58/13.64 fof(mDefSInt,definition, % 13.58/13.64 ! [W0,W1] : % 13.58/13.64 ( ( aSet0(W0) % 13.58/13.64 & aSet0(W1) ) % 13.58/13.64 => ! [W2] : % 13.58/13.64 ( W2 = sdtasasdt0(W0,W1) % 13.58/13.64 <=> ( aSet0(W2) % 13.58/13.64 & ! [W3] : % 13.58/13.64 ( aElementOf0(W3,W2) % 13.58/13.64 <=> ( aElementOf0(W3,W0) % 13.58/13.64 & aElementOf0(W3,W1) ) ) ) ) ) ). % 13.58/13.64 % 13.58/13.64 fof(mDefIdeal,definition, % 13.58/13.64 ! [W0] : % 13.58/13.64 ( aIdeal0(W0) % 13.58/13.64 <=> ( aSet0(W0) % 13.58/13.64 & ! [W1] : % 13.58/13.64 ( aElementOf0(W1,W0) % 13.58/13.64 => ( ! [W2] : % 13.58/13.64 ( aElementOf0(W2,W0) % 13.58/13.64 => aElementOf0(sdtpldt0(W1,W2),W0) ) % 13.58/13.64 & ! [W2] : % 13.58/13.64 ( aElement0(W2) % 13.58/13.64 => aElementOf0(sdtasdt0(W2,W1),W0) ) ) ) ) ) ). % 13.58/13.64 % 13.58/13.64 fof(mIdeSum,axiom, % 13.58/13.64 ! [W0,W1] : % 13.58/13.64 ( ( aIdeal0(W0) % 13.58/13.64 & aIdeal0(W1) ) % 13.58/13.64 => aIdeal0(sdtpldt1(W0,W1)) ) ). % 13.58/13.64 % 13.58/13.64 fof(mIdeInt,axiom, % 13.58/13.64 ! [W0,W1] : % 13.58/13.64 ( ( aIdeal0(W0) % 13.58/13.64 & aIdeal0(W1) ) % 13.58/13.64 => aIdeal0(sdtasasdt0(W0,W1)) ) ). % 13.58/13.64 % 13.58/13.64 fof(mDefMod,definition, % 13.58/13.64 ! [W0,W1,W2] : % 13.58/13.64 ( ( aElement0(W0) % 13.58/13.64 & aElement0(W1) % 13.58/13.64 & aIdeal0(W2) ) % 13.58/13.64 => ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 13.58/13.64 <=> aElementOf0(sdtpldt0(W0,smndt0(W1)),W2) ) ) ). % 13.58/13.64 % 13.58/13.64 fof(mChineseRemainder,axiom, % 13.58/13.64 ! [W0,W1] : % 13.58/13.64 ( ( aIdeal0(W0) % 13.58/13.64 & aIdeal0(W1) ) % 13.58/13.64 => ( ! [W2] : % 13.58/13.64 ( aElement0(W2) % 13.58/13.64 => aElementOf0(W2,sdtpldt1(W0,W1)) ) % 13.58/13.64 => ! [W2,W3] : % 13.58/13.64 ( ( aElement0(W2) % 13.58/13.64 & aElement0(W3) ) % 13.58/13.64 => ? [W4] : % 13.58/13.64 ( aElement0(W4) % 13.58/13.64 & sdteqdtlpzmzozddtrp0(W4,W2,W0) % 13.58/13.64 & sdteqdtlpzmzozddtrp0(W4,W3,W1) ) ) ) ) ). % 13.58/13.64 % 13.58/13.64 fof(mNatSort,axiom, % 13.58/13.64 ! [W0] : % 13.58/13.64 ( aNaturalNumber0(W0) % 13.58/13.64 => $true ) ). % 13.58/13.64 % 13.58/13.64 fof(mEucSort,axiom, % 13.58/13.64 ! [W0] : % 13.58/13.64 ( ( aElement0(W0) % 13.58/13.64 & W0 != sz00 ) % 13.58/13.64 => aNaturalNumber0(sbrdtbr0(W0)) ) ). % 13.58/13.64 % 13.58/13.64 fof(mNatLess,axiom, % 13.58/13.64 ! [W0,W1] : % 13.58/13.64 ( ( aNaturalNumber0(W0) % 13.58/13.64 & aNaturalNumber0(W1) ) % 13.58/13.64 => ( iLess0(W0,W1) % 13.58/13.64 => $true ) ) ). % 13.58/13.64 % 13.58/13.64 fof(mDivision,axiom, % 13.58/13.64 ! [W0,W1] : % 13.58/13.64 ( ( aElement0(W0) % 13.58/13.64 & aElement0(W1) % 13.58/13.64 & W1 != sz00 ) % 13.58/13.64 => ? [W2,W3] : % 13.58/13.64 ( aElement0(W2) % 13.58/13.64 & aElement0(W3) % 13.58/13.64 & W0 = sdtpldt0(sdtasdt0(W2,W1),W3) % 13.58/13.64 & ( W3 != sz00 % 13.58/13.64 => iLess0(sbrdtbr0(W3),sbrdtbr0(W1)) ) ) ) ). % 13.58/13.64 % 13.58/13.64 fof(mDefDiv,definition, % 13.58/13.64 ! [W0,W1] : % 13.58/13.64 ( ( aElement0(W0) % 13.58/13.64 & aElement0(W1) ) % 13.58/13.64 => ( doDivides0(W0,W1) % 13.58/13.64 <=> ? [W2] : % 13.58/13.64 ( aElement0(W2) % 13.58/13.64 & sdtasdt0(W0,W2) = W1 ) ) ) ). % 13.58/13.64 % 13.58/13.64 fof(mDefDvs,definition, % 13.58/13.64 ! [W0] : % 13.58/13.64 ( aElement0(W0) % 13.58/13.64 => ! [W1] : % 13.58/13.64 ( aDivisorOf0(W1,W0) % 13.58/13.64 <=> ( aElement0(W1) % 13.58/13.64 & doDivides0(W1,W0) ) ) ) ). % 13.58/13.64 % 13.58/13.64 fof(mDefGCD,definition, % 13.58/13.64 ! [W0,W1] : % 13.58/13.64 ( ( aElement0(W0) % 13.58/13.64 & aElement0(W1) ) % 13.58/13.64 => ! [W2] : % 13.58/13.64 ( aGcdOfAnd0(W2,W0,W1) % 13.58/13.64 <=> ( aDivisorOf0(W2,W0) % 13.58/13.64 & aDivisorOf0(W2,W1) % 13.58/13.64 & ! [W3] : % 13.58/13.64 ( ( aDivisorOf0(W3,W0) % 13.58/13.64 & aDivisorOf0(W3,W1) ) % 13.58/13.64 => doDivides0(W3,W2) ) ) ) ) ). % 13.58/13.64 % 13.58/13.64 fof(mDefRel,definition, % 13.58/13.64 ! [W0,W1] : % 13.58/13.64 ( ( aElement0(W0) % 13.58/13.64 & aElement0(W1) ) % 13.58/13.64 => ( misRelativelyPrime0(W0,W1) % 13.58/13.64 <=> aGcdOfAnd0(sz10,W0,W1) ) ) ). % 13.58/13.64 % 13.58/13.64 fof(mDefPrIdeal,definition, % 13.58/13.64 ! [W0] : % 13.58/13.64 ( aElement0(W0) % 13.58/13.64 => ! [W1] : % 13.58/13.64 ( W1 = slsdtgt0(W0) % 13.58/13.64 <=> ( aSet0(W1) % 13.58/13.64 & ! [W2] : % 13.58/13.64 ( aElementOf0(W2,W1) % 13.58/13.64 <=> ? [W3] : % 13.58/13.64 ( aElement0(W3) % 13.58/13.64 & sdtasdt0(W0,W3) = W2 ) ) ) ) ) ). % 13.58/13.64 % 13.58/13.64 fof(m__1905,hypothesis, % 13.58/13.64 aElement0(xc) ). % 13.58/13.64 % 13.58/13.64 fof(m__1933,hypothesis, % 13.58/13.64 ( ? [W0] : % 13.58/13.64 ( aElement0(W0) % 13.58/13.64 & sdtasdt0(xc,W0) = xx ) % 13.58/13.64 & aElementOf0(xx,slsdtgt0(xc)) % 13.58/13.64 & ? [W0] : % 13.58/13.64 ( aElement0(W0) % 13.58/13.64 & sdtasdt0(xc,W0) = xy ) % 13.58/13.64 & aElementOf0(xy,slsdtgt0(xc)) % 13.58/13.64 & aElement0(xz) ) ). % 13.58/13.64 % 13.58/13.64 fof(m__1956,hypothesis, % 13.58/13.64 ( aElement0(xu) % 13.58/13.64 & sdtasdt0(xc,xu) = xx ) ). % 13.58/13.64 % 13.58/13.64 fof(m__1979,hypothesis, % 13.58/13.64 ( aElement0(xv) % 13.58/13.64 & sdtasdt0(xc,xv) = xy ) ). % 13.58/13.64 % 13.58/13.64 fof(m__2010,hypothesis, % 13.58/13.64 sdtpldt0(xx,xy) = sdtasdt0(xc,sdtpldt0(xu,xv)) ). % 13.58/13.64 % 13.58/13.64 fof(m__2043,hypothesis, % 13.58/13.64 sdtasdt0(xz,xx) = sdtasdt0(xc,sdtasdt0(xu,xz)) ). % 13.58/13.64 % 13.58/13.64 fof(m__,conjecture, % 13.58/13.64 ( ( ? [W0] : % 13.58/13.64 ( aElement0(W0) % 13.58/13.64 & sdtasdt0(xc,W0) = sdtpldt0(xx,xy) ) % 13.58/13.64 | aElementOf0(sdtpldt0(xx,xy),slsdtgt0(xc)) ) % 13.58/13.64 & ( ? [W0] : % 13.58/13.64 ( aElement0(W0) % 13.58/13.64 & sdtasdt0(xc,W0) = sdtasdt0(xz,xx) ) % 13.58/13.64 | aElementOf0(sdtasdt0(xz,xx),slsdtgt0(xc)) ) ) ). % 13.58/13.64 % 13.58/13.64 %------------------------------------------------------------------------------ % 13.58/13.64 %------------------------------------------- % 13.58/13.64 % Proof found % 13.58/13.64 % SZS status Theorem for theBenchmark % 13.58/13.64 % SZS output start Proof % 13.58/13.64 %ClaNum:189(EqnAxiom:83) % 13.58/13.64 %VarNum:707(SingletonVarNum:216) % 13.58/13.64 %MaxLitNum:8 % 13.58/13.64 %MaxfuncDepth:2 % 13.58/13.64 %SharedTerms:41 % 13.58/13.64 %goalClause: 139 147 148 154 % 13.58/13.64 [84]P1(a1) % 13.58/13.64 [85]P1(a31) % 13.58/13.64 [86]P1(a32) % 13.58/13.64 [87]P1(a33) % 13.58/13.64 [88]P1(a34) % 13.58/13.64 [89]P1(a35) % 13.58/13.64 [90]P1(a2) % 13.58/13.64 [91]P1(a15) % 13.58/13.64 [100]~E(a1,a31) % 13.58/13.64 [92]E(f16(a32,a34),a36) % 13.58/13.64 [93]E(f16(a32,a35),a37) % 13.58/13.64 [94]E(f16(a32,a2),a36) % 13.58/13.64 [95]E(f16(a32,a15),a37) % 13.58/13.64 [96]P3(a36,f27(a32)) % 13.58/13.64 [97]P3(a37,f27(a32)) % 13.58/13.64 [98]E(f16(a32,f28(a34,a35)),f28(a36,a37)) % 13.58/13.64 [99]E(f16(a32,f16(a34,a33)),f16(a33,a36)) % 13.58/13.65 [154]~P3(f28(a36,a37),f27(a32))+~P3(f16(a33,a36),f27(a32)) % 13.58/13.65 [101]~P5(x1011)+P4(x1011) % 13.58/13.65 [102]~P1(x1021)+P1(f30(x1021)) % 13.58/13.65 [104]~P1(x1041)+E(f16(a1,x1041),a1) % 13.58/13.65 [105]~P1(x1051)+E(f16(x1051,a1),a1) % 13.58/13.65 [107]~P1(x1071)+E(f28(a1,x1071),x1071) % 13.58/13.65 [108]~P1(x1081)+E(f16(a31,x1081),x1081) % 13.58/13.65 [109]~P1(x1091)+E(f28(x1091,a1),x1091) % 13.58/13.65 [110]~P1(x1101)+E(f16(x1101,a31),x1101) % 13.58/13.65 [111]~P1(x1111)+E(f28(f30(x1111),x1111),a1) % 13.58/13.65 [112]~P1(x1121)+E(f28(x1121,f30(x1121)),a1) % 13.58/13.65 [113]~P1(x1131)+E(f16(x1131,f30(a31)),f30(x1131)) % 13.58/13.65 [114]~P1(x1141)+E(f16(f30(a31),x1141),f30(x1141)) % 13.58/13.65 [103]~P1(x1031)+E(x1031,a1)+P7(f17(x1031)) % 13.58/13.65 [115]~P4(x1151)+P5(x1151)+P3(f18(x1151),x1151) % 13.58/13.65 [147]~P1(x1471)+~E(f16(a32,x1471),f28(a36,a37))+~P3(f16(a33,a36),f27(a32)) % 13.58/13.65 [148]~P1(x1481)+~E(f16(a32,x1481),f16(a33,a36))+~P3(f28(a36,a37),f27(a32)) % 13.58/13.65 [116]~P3(x1161,x1162)+P1(x1161)+~P4(x1162) % 13.58/13.65 [117]~P2(x1171,x1172)+P1(x1171)+~P1(x1172) % 13.58/13.65 [124]~P1(x1242)+~P2(x1241,x1242)+P8(x1241,x1242) % 13.58/13.65 [106]~P1(x1062)+P4(x1061)+~E(x1061,f27(x1062)) % 13.58/13.65 [119]~P1(x1192)+~P1(x1191)+E(f28(x1191,x1192),f28(x1192,x1191)) % 13.58/13.65 [120]~P1(x1202)+~P1(x1201)+E(f16(x1201,x1202),f16(x1202,x1201)) % 13.58/13.65 [125]~P1(x1252)+~P1(x1251)+P1(f28(x1251,x1252)) % 13.58/13.65 [126]~P1(x1262)+~P1(x1261)+P1(f16(x1261,x1262)) % 13.58/13.65 [127]~P5(x1272)+~P5(x1271)+P5(f29(x1271,x1272)) % 13.58/13.65 [128]~P5(x1282)+~P5(x1281)+P5(f26(x1281,x1282)) % 13.58/13.65 [123]~P4(x1231)+P5(x1231)+P3(f4(x1231),x1231)+P1(f3(x1231)) % 13.58/13.65 [158]~P4(x1581)+P5(x1581)+P1(f3(x1581))+~P3(f28(f18(x1581),f4(x1581)),x1581) % 13.58/13.65 [161]~P4(x1611)+P5(x1611)+P3(f4(x1611),x1611)+~P3(f16(f3(x1611),f18(x1611)),x1611) % 13.58/13.65 [170]~P4(x1701)+P5(x1701)+~P3(f28(f18(x1701),f4(x1701)),x1701)+~P3(f16(f3(x1701),f18(x1701)),x1701) % 13.58/13.65 [131]~P1(x1312)+~P1(x1311)+~P8(x1311,x1312)+P2(x1311,x1312) % 13.58/13.65 [140]~P1(x1402)+~P1(x1401)+~P9(x1401,x1402)+P6(a31,x1401,x1402) % 13.58/13.65 [150]~P1(x1502)+~P1(x1501)+P9(x1501,x1502)+~P6(a31,x1501,x1502) % 13.58/13.65 [129]~P1(x1291)+~P1(x1292)+E(x1291,a1)+P1(f5(x1292,x1291)) % 13.58/13.65 [130]~P1(x1301)+~P1(x1302)+E(x1301,a1)+P1(f8(x1302,x1301)) % 13.58/13.65 [134]~P1(x1342)+~P1(x1341)+~P8(x1341,x1342)+P1(f9(x1341,x1342)) % 13.58/13.65 [139]~P1(x1391)+~P1(x1392)+~E(f16(a32,x1391),f28(a36,a37))+~E(f16(a32,x1392),f16(a33,a36)) % 13.58/13.65 [138]~P1(x1382)+~P1(x1381)+~P8(x1381,x1382)+E(f16(x1381,f9(x1381,x1382)),x1382) % 13.58/13.65 [163]~P1(x1631)+~P1(x1632)+E(x1631,a1)+E(f28(f16(f5(x1632,x1631),x1631),f8(x1632,x1631)),x1632) % 13.58/13.65 [152]~P1(x1522)+~P6(x1521,x1523,x1522)+P2(x1521,x1522)+~P1(x1523) % 13.58/13.65 [153]~P1(x1532)+~P6(x1531,x1532,x1533)+P2(x1531,x1532)+~P1(x1533) % 13.58/13.65 [121]~P4(x1213)+~P4(x1212)+P4(x1211)+~E(x1211,f29(x1212,x1213)) % 13.58/13.65 [122]~P4(x1223)+~P4(x1222)+P4(x1221)+~E(x1221,f26(x1222,x1223)) % 13.58/13.65 [137]~P1(x1371)+~P5(x1373)+~P3(x1372,x1373)+P3(f16(x1371,x1372),x1373) % 13.58/13.65 [142]~P5(x1423)+~P3(x1421,x1423)+~P3(x1422,x1423)+P3(f28(x1421,x1422),x1423) % 13.58/13.65 [165]~P1(x1651)+~P3(x1653,x1652)+~E(x1652,f27(x1651))+P1(f12(x1651,x1652,x1653)) % 13.58/13.65 [145]~P1(x1453)+~P1(x1452)+~P1(x1451)+E(f28(f28(x1451,x1452),x1453),f28(x1451,f28(x1452,x1453))) % 13.58/13.65 [146]~P1(x1463)+~P1(x1462)+~P1(x1461)+E(f16(f16(x1461,x1462),x1463),f16(x1461,f16(x1462,x1463))) % 13.58/13.65 [159]~P1(x1593)+~P1(x1592)+~P1(x1591)+E(f28(f16(x1591,x1592),f16(x1591,x1593)),f16(x1591,f28(x1592,x1593))) % 13.58/13.65 [160]~P1(x1602)+~P1(x1603)+~P1(x1601)+E(f28(f16(x1601,x1602),f16(x1603,x1602)),f16(f28(x1601,x1603),x1602)) % 13.58/13.65 [167]~P1(x1671)+~P3(x1673,x1672)+~E(x1672,f27(x1671))+E(f16(x1671,f12(x1671,x1672,x1673)),x1673) % 13.58/13.65 [118]~P1(x1181)+~P1(x1182)+E(x1181,a1)+E(x1182,a1)+~E(f16(x1182,x1181),a1) % 13.58/13.65 [141]~P1(x1412)+~P4(x1411)+P3(f11(x1412,x1411),x1411)+E(x1411,f27(x1412))+P1(f10(x1412,x1411)) % 13.58/13.65 [143]~P4(x1432)+~P4(x1431)+E(x1431,x1432)+P3(f14(x1431,x1432),x1431)+P3(f19(x1431,x1432),x1432) % 13.58/13.65 [155]~P4(x1552)+~P4(x1551)+E(x1551,x1552)+P3(f14(x1551,x1552),x1551)+~P3(f19(x1551,x1552),x1551) % 13.58/13.65 [156]~P4(x1562)+~P4(x1561)+E(x1561,x1562)+P3(f19(x1561,x1562),x1562)+~P3(f14(x1561,x1562),x1562) % 13.58/13.65 [164]~P4(x1642)+~P4(x1641)+E(x1641,x1642)+~P3(f14(x1641,x1642),x1642)+~P3(f19(x1641,x1642),x1641) % 13.58/13.65 [149]~P1(x1491)+~P1(x1492)+E(x1491,a1)+P10(f17(f8(x1492,x1491)),f17(x1491))+E(f8(x1492,x1491),a1) % 13.58/13.65 [151]~P1(x1512)+~P4(x1511)+P3(f11(x1512,x1511),x1511)+E(x1511,f27(x1512))+E(f16(x1512,f10(x1512,x1511)),f11(x1512,x1511)) % 13.58/13.65 [132]~P1(x1322)+~P1(x1321)+~P1(x1323)+P8(x1321,x1322)+~E(f16(x1321,x1323),x1322) % 13.58/13.65 [166]~P1(x1662)+~P1(x1661)+~P5(x1663)+P11(x1661,x1662,x1663)+~P3(f28(x1661,f30(x1662)),x1663) % 13.58/13.65 [168]~P1(x1682)+~P1(x1681)+~P5(x1683)+~P11(x1681,x1682,x1683)+P3(f28(x1681,f30(x1682)),x1683) % 13.58/13.65 [133]~P1(x1333)+~P1(x1334)+P3(x1331,x1332)+~E(f16(x1333,x1334),x1331)+~E(x1332,f27(x1333)) % 13.58/13.65 [135]~P4(x1354)+~P4(x1352)+~P3(x1351,x1353)+P3(x1351,x1352)+~E(x1353,f26(x1354,x1352)) % 13.58/13.65 [136]~P4(x1364)+~P4(x1362)+~P3(x1361,x1363)+P3(x1361,x1362)+~E(x1363,f26(x1362,x1364)) % 13.58/13.65 [181]~P4(x1812)+~P4(x1811)+~P3(x1814,x1813)+~E(x1813,f29(x1811,x1812))+P3(f21(x1811,x1812,x1813,x1814),x1811) % 13.58/13.65 [182]~P4(x1822)+~P4(x1821)+~P3(x1824,x1823)+~E(x1823,f29(x1821,x1822))+P3(f22(x1821,x1822,x1823,x1824),x1822) % 13.58/13.65 [189]~P4(x1892)+~P4(x1891)+~P3(x1894,x1893)+~E(x1893,f29(x1891,x1892))+E(f28(f21(x1891,x1892,x1893,x1894),f22(x1891,x1892,x1893,x1894)),x1894) % 13.58/13.65 [162]~P1(x1623)+~P1(x1622)+~P4(x1621)+~P3(f11(x1622,x1621),x1621)+~E(f11(x1622,x1621),f16(x1622,x1623))+E(x1621,f27(x1622)) % 13.58/13.65 [171]~P1(x1713)+~P1(x1712)+~P2(x1711,x1713)+~P2(x1711,x1712)+P6(x1711,x1712,x1713)+P2(f13(x1712,x1713,x1711),x1713) % 13.58/13.65 [172]~P1(x1723)+~P1(x1722)+~P2(x1721,x1723)+~P2(x1721,x1722)+P6(x1721,x1722,x1723)+P2(f13(x1722,x1723,x1721),x1722) % 13.58/13.65 [173]~P4(x1731)+~P4(x1733)+~P4(x1732)+P3(f20(x1732,x1733,x1731),x1731)+P3(f23(x1732,x1733,x1731),x1732)+E(x1731,f29(x1732,x1733)) % 13.58/13.65 [174]~P4(x1741)+~P4(x1743)+~P4(x1742)+P3(f20(x1742,x1743,x1741),x1741)+P3(f24(x1742,x1743,x1741),x1743)+E(x1741,f29(x1742,x1743)) % 13.58/13.65 [175]~P4(x1751)+~P4(x1753)+~P4(x1752)+P3(f25(x1752,x1753,x1751),x1751)+P3(f25(x1752,x1753,x1751),x1753)+E(x1751,f26(x1752,x1753)) % 13.58/13.65 [176]~P4(x1761)+~P4(x1763)+~P4(x1762)+P3(f25(x1762,x1763,x1761),x1761)+P3(f25(x1762,x1763,x1761),x1762)+E(x1761,f26(x1762,x1763)) % 13.58/13.65 [177]~P1(x1773)+~P1(x1772)+~P2(x1771,x1773)+~P2(x1771,x1772)+P6(x1771,x1772,x1773)+~P8(f13(x1772,x1773,x1771),x1771) % 13.58/13.65 [179]~P4(x1791)+~P4(x1793)+~P4(x1792)+P3(f20(x1792,x1793,x1791),x1791)+E(x1791,f29(x1792,x1793))+E(f28(f23(x1792,x1793,x1791),f24(x1792,x1793,x1791)),f20(x1792,x1793,x1791)) % 13.58/13.65 [169]~P2(x1691,x1693)+~P2(x1691,x1694)+~P6(x1692,x1694,x1693)+P8(x1691,x1692)+~P1(x1693)+~P1(x1694) % 13.58/13.65 [144]~P4(x1444)+~P4(x1443)+~P3(x1441,x1444)+~P3(x1441,x1443)+P3(x1441,x1442)+~E(x1442,f26(x1443,x1444)) % 13.58/13.65 [180]~P1(x1804)+~P1(x1803)+~P5(x1802)+~P5(x1801)+P1(f6(x1801,x1802))+P1(f7(x1801,x1802,x1803,x1804)) % 13.58/13.65 [183]~P1(x1834)+~P1(x1833)+~P5(x1832)+~P5(x1831)+P11(f7(x1831,x1832,x1833,x1834),x1834,x1832)+P1(f6(x1831,x1832)) % 13.58/13.65 [184]~P1(x1844)+~P1(x1843)+~P5(x1842)+~P5(x1841)+P11(f7(x1841,x1842,x1843,x1844),x1843,x1841)+P1(f6(x1841,x1842)) % 13.58/13.65 [186]~P1(x1864)+~P1(x1863)+~P5(x1862)+~P5(x1861)+~P3(f6(x1861,x1862),f29(x1861,x1862))+P1(f7(x1861,x1862,x1863,x1864)) % 13.58/13.65 [187]~P1(x1874)+~P1(x1873)+~P5(x1872)+~P5(x1871)+P11(f7(x1871,x1872,x1873,x1874),x1874,x1872)+~P3(f6(x1871,x1872),f29(x1871,x1872)) % 13.58/13.65 [188]~P1(x1884)+~P1(x1883)+~P5(x1882)+~P5(x1881)+P11(f7(x1881,x1882,x1883,x1884),x1883,x1881)+~P3(f6(x1881,x1882),f29(x1881,x1882)) % 13.58/13.65 [185]~P4(x1851)+~P4(x1853)+~P4(x1852)+~P3(f25(x1852,x1853,x1851),x1851)+~P3(f25(x1852,x1853,x1851),x1853)+~P3(f25(x1852,x1853,x1851),x1852)+E(x1851,f26(x1852,x1853)) % 13.58/13.65 [157]~P4(x1574)+~P4(x1573)+~P3(x1576,x1574)+~P3(x1575,x1573)+P3(x1571,x1572)+~E(x1572,f29(x1573,x1574))+~E(f28(x1575,x1576),x1571) % 13.58/13.65 [178]~P4(x1781)+~P4(x1783)+~P4(x1782)+~P3(x1785,x1783)+~P3(x1784,x1782)+~P3(f20(x1782,x1783,x1781),x1781)+E(x1781,f29(x1782,x1783))+~E(f28(x1784,x1785),f20(x1782,x1783,x1781)) % 13.58/13.65 %EqnAxiom % 13.58/13.65 [1]E(x11,x11) % 13.58/13.65 [2]E(x22,x21)+~E(x21,x22) % 13.58/13.65 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 13.58/13.65 [4]~E(x41,x42)+E(f16(x41,x43),f16(x42,x43)) % 13.58/13.65 [5]~E(x51,x52)+E(f16(x53,x51),f16(x53,x52)) % 13.58/13.65 [6]~E(x61,x62)+E(f29(x61,x63),f29(x62,x63)) % 13.58/13.65 [7]~E(x71,x72)+E(f29(x73,x71),f29(x73,x72)) % 13.58/13.65 [8]~E(x81,x82)+E(f28(x81,x83),f28(x82,x83)) % 13.58/13.65 [9]~E(x91,x92)+E(f28(x93,x91),f28(x93,x92)) % 13.58/13.65 [10]~E(x101,x102)+E(f22(x101,x103,x104,x105),f22(x102,x103,x104,x105)) % 13.58/13.65 [11]~E(x111,x112)+E(f22(x113,x111,x114,x115),f22(x113,x112,x114,x115)) % 13.58/13.65 [12]~E(x121,x122)+E(f22(x123,x124,x121,x125),f22(x123,x124,x122,x125)) % 13.58/13.65 [13]~E(x131,x132)+E(f22(x133,x134,x135,x131),f22(x133,x134,x135,x132)) % 13.58/13.65 [14]~E(x141,x142)+E(f27(x141),f27(x142)) % 13.58/13.65 [15]~E(x151,x152)+E(f13(x151,x153,x154),f13(x152,x153,x154)) % 13.58/13.65 [16]~E(x161,x162)+E(f13(x163,x161,x164),f13(x163,x162,x164)) % 13.58/13.65 [17]~E(x171,x172)+E(f13(x173,x174,x171),f13(x173,x174,x172)) % 13.58/13.65 [18]~E(x181,x182)+E(f18(x181),f18(x182)) % 13.58/13.65 [19]~E(x191,x192)+E(f21(x191,x193,x194,x195),f21(x192,x193,x194,x195)) % 13.58/13.65 [20]~E(x201,x202)+E(f21(x203,x201,x204,x205),f21(x203,x202,x204,x205)) % 13.58/13.65 [21]~E(x211,x212)+E(f21(x213,x214,x211,x215),f21(x213,x214,x212,x215)) % 13.58/13.65 [22]~E(x221,x222)+E(f21(x223,x224,x225,x221),f21(x223,x224,x225,x222)) % 13.58/13.65 [23]~E(x231,x232)+E(f30(x231),f30(x232)) % 13.58/13.65 [24]~E(x241,x242)+E(f20(x241,x243,x244),f20(x242,x243,x244)) % 13.58/13.65 [25]~E(x251,x252)+E(f20(x253,x251,x254),f20(x253,x252,x254)) % 13.58/13.65 [26]~E(x261,x262)+E(f20(x263,x264,x261),f20(x263,x264,x262)) % 13.58/13.65 [27]~E(x271,x272)+E(f6(x271,x273),f6(x272,x273)) % 13.58/13.65 [28]~E(x281,x282)+E(f6(x283,x281),f6(x283,x282)) % 13.58/13.65 [29]~E(x291,x292)+E(f7(x291,x293,x294,x295),f7(x292,x293,x294,x295)) % 13.58/13.65 [30]~E(x301,x302)+E(f7(x303,x301,x304,x305),f7(x303,x302,x304,x305)) % 13.58/13.65 [31]~E(x311,x312)+E(f7(x313,x314,x311,x315),f7(x313,x314,x312,x315)) % 13.58/13.65 [32]~E(x321,x322)+E(f7(x323,x324,x325,x321),f7(x323,x324,x325,x322)) % 13.58/13.65 [33]~E(x331,x332)+E(f3(x331),f3(x332)) % 13.58/13.65 [34]~E(x341,x342)+E(f17(x341),f17(x342)) % 13.58/13.65 [35]~E(x351,x352)+E(f23(x351,x353,x354),f23(x352,x353,x354)) % 13.58/13.65 [36]~E(x361,x362)+E(f23(x363,x361,x364),f23(x363,x362,x364)) % 13.58/13.65 [37]~E(x371,x372)+E(f23(x373,x374,x371),f23(x373,x374,x372)) % 13.58/13.65 [38]~E(x381,x382)+E(f11(x381,x383),f11(x382,x383)) % 13.58/13.65 [39]~E(x391,x392)+E(f11(x393,x391),f11(x393,x392)) % 13.58/13.65 [40]~E(x401,x402)+E(f25(x401,x403,x404),f25(x402,x403,x404)) % 13.58/13.65 [41]~E(x411,x412)+E(f25(x413,x411,x414),f25(x413,x412,x414)) % 13.58/13.65 [42]~E(x421,x422)+E(f25(x423,x424,x421),f25(x423,x424,x422)) % 13.58/13.65 [43]~E(x431,x432)+E(f26(x431,x433),f26(x432,x433)) % 13.58/13.65 [44]~E(x441,x442)+E(f26(x443,x441),f26(x443,x442)) % 13.58/13.65 [45]~E(x451,x452)+E(f19(x451,x453),f19(x452,x453)) % 13.58/13.65 [46]~E(x461,x462)+E(f19(x463,x461),f19(x463,x462)) % 13.58/13.65 [47]~E(x471,x472)+E(f9(x471,x473),f9(x472,x473)) % 13.58/13.65 [48]~E(x481,x482)+E(f9(x483,x481),f9(x483,x482)) % 13.58/13.65 [49]~E(x491,x492)+E(f10(x491,x493),f10(x492,x493)) % 13.58/13.65 [50]~E(x501,x502)+E(f10(x503,x501),f10(x503,x502)) % 13.58/13.65 [51]~E(x511,x512)+E(f14(x511,x513),f14(x512,x513)) % 13.58/13.65 [52]~E(x521,x522)+E(f14(x523,x521),f14(x523,x522)) % 13.58/13.65 [53]~E(x531,x532)+E(f12(x531,x533,x534),f12(x532,x533,x534)) % 13.58/13.65 [54]~E(x541,x542)+E(f12(x543,x541,x544),f12(x543,x542,x544)) % 13.58/13.65 [55]~E(x551,x552)+E(f12(x553,x554,x551),f12(x553,x554,x552)) % 13.58/13.65 [56]~E(x561,x562)+E(f8(x561,x563),f8(x562,x563)) % 13.58/13.65 [57]~E(x571,x572)+E(f8(x573,x571),f8(x573,x572)) % 13.58/13.65 [58]~E(x581,x582)+E(f4(x581),f4(x582)) % 13.58/13.65 [59]~E(x591,x592)+E(f24(x591,x593,x594),f24(x592,x593,x594)) % 13.58/13.65 [60]~E(x601,x602)+E(f24(x603,x601,x604),f24(x603,x602,x604)) % 13.58/13.65 [61]~E(x611,x612)+E(f24(x613,x614,x611),f24(x613,x614,x612)) % 13.58/13.65 [62]~E(x621,x622)+E(f5(x621,x623),f5(x622,x623)) % 13.58/13.65 [63]~E(x631,x632)+E(f5(x633,x631),f5(x633,x632)) % 13.58/13.65 [64]~P1(x641)+P1(x642)+~E(x641,x642) % 13.58/13.65 [65]P3(x652,x653)+~E(x651,x652)+~P3(x651,x653) % 13.58/13.65 [66]P3(x663,x662)+~E(x661,x662)+~P3(x663,x661) % 13.58/13.65 [67]~P4(x671)+P4(x672)+~E(x671,x672) % 13.58/13.65 [68]P2(x682,x683)+~E(x681,x682)+~P2(x681,x683) % 13.58/13.65 [69]P2(x693,x692)+~E(x691,x692)+~P2(x693,x691) % 13.58/13.65 [70]P11(x702,x703,x704)+~E(x701,x702)+~P11(x701,x703,x704) % 13.58/13.65 [71]P11(x713,x712,x714)+~E(x711,x712)+~P11(x713,x711,x714) % 13.58/13.65 [72]P11(x723,x724,x722)+~E(x721,x722)+~P11(x723,x724,x721) % 13.58/13.65 [73]~P5(x731)+P5(x732)+~E(x731,x732) % 13.58/13.65 [74]P6(x742,x743,x744)+~E(x741,x742)+~P6(x741,x743,x744) % 13.58/13.65 [75]P6(x753,x752,x754)+~E(x751,x752)+~P6(x753,x751,x754) % 13.58/13.65 [76]P6(x763,x764,x762)+~E(x761,x762)+~P6(x763,x764,x761) % 13.58/13.65 [77]P9(x772,x773)+~E(x771,x772)+~P9(x771,x773) % 13.58/13.65 [78]P9(x783,x782)+~E(x781,x782)+~P9(x783,x781) % 13.58/13.65 [79]P8(x792,x793)+~E(x791,x792)+~P8(x791,x793) % 13.58/13.65 [80]P8(x803,x802)+~E(x801,x802)+~P8(x803,x801) % 13.58/13.65 [81]P10(x812,x813)+~E(x811,x812)+~P10(x811,x813) % 13.58/13.65 [82]P10(x823,x822)+~E(x821,x822)+~P10(x823,x821) % 13.58/13.65 [83]~P7(x831)+P7(x832)+~E(x831,x832) % 13.58/13.65 % 13.58/13.65 %------------------------------------------- % 13.58/13.65 cnf(190,plain, % 13.58/13.65 (~P1(x1901)+P4(f27(x1901))), % 13.58/13.65 inference(equality_inference,[],[106])). % 13.58/13.65 cnf(202,plain, % 13.58/13.65 (E(f28(a36,a37),f16(a32,f28(a34,a35)))), % 13.58/13.65 inference(scs_inference,[],[98,2])). % 13.58/13.65 cnf(210,plain, % 13.58/13.65 (E(a37,f16(a32,a35))), % 13.58/13.65 inference(scs_inference,[],[93,2])). % 13.58/13.65 cnf(216,plain, % 13.58/13.65 (E(a37,f16(a32,a15))), % 13.58/13.65 inference(scs_inference,[],[95,2])). % 13.58/13.65 cnf(222,plain, % 13.58/13.65 (P3(x2221,f27(a32))+~E(a36,x2221)), % 13.58/13.65 inference(scs_inference,[],[98,202,210,95,96,2,3,73,67,64,83,65])). % 13.58/13.65 cnf(237,plain, % 13.58/13.65 (E(a36,f16(a32,a2))), % 13.58/13.65 inference(scs_inference,[],[94,2])). % 13.58/13.65 cnf(248,plain, % 13.58/13.65 (E(f16(a32,a34),f16(a32,a2))), % 13.58/13.65 inference(scs_inference,[],[237,92,2,3])). % 13.58/13.65 cnf(249,plain, % 13.58/13.65 (P3(f16(a32,a34),f27(a32))), % 13.58/13.65 inference(scs_inference,[],[237,92,2,3,222])). % 13.58/13.65 cnf(256,plain, % 13.58/13.65 (E(f16(a32,a2),f16(a32,a34))), % 13.58/13.65 inference(scs_inference,[],[248,2])). % 13.58/13.65 cnf(264,plain, % 13.58/13.65 (~P1(f28(a34,a35))+~E(f27(a32),x2641)+~P1(f16(a34,a33))), % 13.58/13.65 inference(scs_inference,[],[98,249,216,248,99,2,66,65,139])). % 13.58/13.65 cnf(268,plain, % 13.58/13.65 (~P1(f28(a34,a35))+~P1(f16(a34,a33))), % 13.58/13.65 inference(equality_inference,[],[264])). % 13.58/13.65 cnf(299,plain, % 13.58/13.65 (~P1(a36)+P1(f16(a32,a2))), % 13.58/13.65 inference(scs_inference,[],[237,256,73,64])). % 13.58/13.65 cnf(330,plain, % 13.58/13.65 (~P1(f16(a32,a2))+P1(f16(a32,a34))), % 13.58/13.65 inference(scs_inference,[],[256,202,73,64])). % 13.58/13.65 cnf(367,plain, % 13.58/13.65 (~P4(f27(a32))+P1(a36)), % 13.58/13.65 inference(scs_inference,[],[249,88,86,92,64,126,116])). % 13.58/13.65 cnf(498,plain, % 13.58/13.65 (P1(a36)), % 13.58/13.65 inference(scs_inference,[],[86,367,190])). % 13.58/13.65 cnf(500,plain, % 13.58/13.65 (P1(f16(a32,a2))), % 13.58/13.65 inference(scs_inference,[],[498,299])). % 13.58/13.65 cnf(507,plain, % 13.58/13.65 (P1(f16(a32,a34))), % 13.58/13.65 inference(scs_inference,[],[500,330])). % 13.58/13.65 cnf(1603,plain, % 13.58/13.65 (E(f27(a36),f27(f16(a32,a34)))), % 13.58/13.65 inference(scs_inference,[],[92,14,2])). % 13.58/13.65 cnf(1605,plain, % 13.58/13.65 (P4(f27(a36))), % 13.58/13.65 inference(scs_inference,[],[507,1603,2,106])). % 13.58/13.65 cnf(1868,plain, % 13.58/13.65 (~P1(f16(a34,a33))), % 13.58/13.65 inference(scs_inference,[],[89,88,268,125])). % 13.58/13.65 cnf(1871,plain, % 13.58/13.65 ($false), % 13.58/13.65 inference(scs_inference,[],[1868,87,88,1605,116,126]), % 13.58/13.65 ['proof']). % 13.58/13.65 % SZS output end Proof % 13.58/13.65 % Total time :13.010000s %------------------------------------------------------------------------------