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