%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : RNG112+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 : n023.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:07 EDT 2024 % Result : Theorem 59.01s 59.53s % Output : CNFRefutation 59.15s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.10 % Problem : RNG112+1 : TPTP v8.2.0. Released v4.0.0. % 0.03/0.10 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.09/0.30 % Computer : n023.cluster.edu % 0.09/0.30 % Model : x86_64 x86_64 % 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.30 % Memory : 8042.1875MB % 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.30 % CPULimit : 300 % 0.09/0.30 % WCLimit : 300 % 0.09/0.30 % DateTime : Tue Jun 18 13:40:53 EDT 2024 % 0.09/0.30 % CPUTime : % 0.15/0.54 start to proof:theBenchmark % 59.01/59.51 %------------------------------------------- % 59.01/59.51 % File :CSE---1.7 % 59.01/59.51 % Problem :theBenchmark % 59.01/59.51 % Transform :cnf % 59.01/59.51 % Format :tptp:raw % 59.01/59.51 % Command :java -jar mcs_scs.jar %d %s % 59.01/59.51 % 59.01/59.51 % Result :Theorem 58.530000s % 59.01/59.51 % Output :CNFRefutation 58.530000s % 59.01/59.51 %------------------------------------------- % 59.01/59.52 %------------------------------------------------------------------------------ % 59.01/59.52 % File : RNG112+1 : TPTP v8.2.0. Released v4.0.0. % 59.01/59.52 % Domain : Ring Theory % 59.01/59.52 % Problem : Chinese remainder theorem in a ring 07_04_02, 00 expansion % 59.01/59.52 % Version : Especial. % 59.01/59.52 % English : % 59.01/59.52 % 59.01/59.52 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 59.01/59.52 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 59.01/59.52 % Source : [Pas08] % 59.01/59.52 % Names : chines_07_04_02.00 [Pas08] % 59.01/59.52 % 59.01/59.52 % Status : Theorem % 59.01/59.52 % Rating : 0.31 v8.2.0, 0.28 v8.1.0, 0.25 v7.5.0, 0.28 v7.4.0, 0.17 v7.3.0, 0.21 v7.2.0, 0.17 v7.1.0, 0.26 v7.0.0, 0.27 v6.4.0, 0.31 v6.3.0, 0.21 v6.2.0, 0.28 v6.1.0, 0.47 v6.0.0, 0.43 v5.5.0, 0.56 v5.4.0, 0.57 v5.3.0, 0.59 v5.2.0, 0.50 v5.1.0, 0.57 v5.0.0, 0.71 v4.1.0, 0.74 v4.0.1, 0.83 v4.0.0 % 59.01/59.52 % Syntax : Number of formulae : 46 ( 4 unt; 9 def) % 59.01/59.52 % Number of atoms : 177 ( 40 equ) % 59.01/59.52 % Maximal formula atoms : 9 ( 3 avg) % 59.01/59.52 % Number of connectives : 145 ( 14 ~; 2 |; 66 &) % 59.01/59.52 % ( 12 <=>; 51 =>; 0 <=; 0 <~>) % 59.01/59.52 % Maximal formula depth : 13 ( 6 avg) % 59.01/59.52 % Maximal term depth : 3 ( 1 avg) % 59.01/59.52 % Number of predicates : 13 ( 11 usr; 1 prp; 0-3 aty) % 59.01/59.52 % Number of functors : 13 ( 13 usr; 6 con; 0-2 aty) % 59.01/59.52 % Number of variables : 90 ( 80 !; 10 ?) % 59.01/59.52 % SPC : FOF_THM_RFO_SEQ % 59.01/59.52 % 59.01/59.52 % Comments : Problem generated by the SAD system [VLP07] % 59.01/59.52 %------------------------------------------------------------------------------ % 59.01/59.52 fof(mElmSort,axiom, % 59.01/59.52 ! [W0] : % 59.01/59.52 ( aElement0(W0) % 59.01/59.52 => $true ) ). % 59.01/59.52 % 59.01/59.52 fof(mSortsC,axiom, % 59.01/59.52 aElement0(sz00) ). % 59.01/59.52 % 59.01/59.52 fof(mSortsC_01,axiom, % 59.01/59.52 aElement0(sz10) ). % 59.01/59.52 % 59.01/59.52 fof(mSortsU,axiom, % 59.01/59.52 ! [W0] : % 59.01/59.52 ( aElement0(W0) % 59.01/59.52 => aElement0(smndt0(W0)) ) ). % 59.01/59.52 % 59.01/59.52 fof(mSortsB,axiom, % 59.01/59.52 ! [W0,W1] : % 59.01/59.52 ( ( aElement0(W0) % 59.01/59.52 & aElement0(W1) ) % 59.01/59.52 => aElement0(sdtpldt0(W0,W1)) ) ). % 59.01/59.52 % 59.01/59.52 fof(mSortsB_02,axiom, % 59.01/59.52 ! [W0,W1] : % 59.01/59.52 ( ( aElement0(W0) % 59.01/59.52 & aElement0(W1) ) % 59.01/59.52 => aElement0(sdtasdt0(W0,W1)) ) ). % 59.01/59.52 % 59.01/59.52 fof(mAddComm,axiom, % 59.01/59.52 ! [W0,W1] : % 59.01/59.52 ( ( aElement0(W0) % 59.01/59.52 & aElement0(W1) ) % 59.01/59.52 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 59.01/59.52 % 59.01/59.52 fof(mAddAsso,axiom, % 59.01/59.52 ! [W0,W1,W2] : % 59.01/59.52 ( ( aElement0(W0) % 59.01/59.52 & aElement0(W1) % 59.01/59.52 & aElement0(W2) ) % 59.01/59.52 => sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) ). % 59.01/59.52 % 59.01/59.52 fof(mAddZero,axiom, % 59.01/59.52 ! [W0] : % 59.01/59.52 ( aElement0(W0) % 59.01/59.52 => ( sdtpldt0(W0,sz00) = W0 % 59.01/59.52 & W0 = sdtpldt0(sz00,W0) ) ) ). % 59.01/59.52 % 59.01/59.52 fof(mAddInvr,axiom, % 59.01/59.52 ! [W0] : % 59.01/59.52 ( aElement0(W0) % 59.01/59.52 => ( sdtpldt0(W0,smndt0(W0)) = sz00 % 59.01/59.52 & sz00 = sdtpldt0(smndt0(W0),W0) ) ) ). % 59.01/59.52 % 59.01/59.52 fof(mMulComm,axiom, % 59.01/59.52 ! [W0,W1] : % 59.01/59.52 ( ( aElement0(W0) % 59.01/59.52 & aElement0(W1) ) % 59.01/59.52 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 59.01/59.52 % 59.01/59.52 fof(mMulAsso,axiom, % 59.01/59.52 ! [W0,W1,W2] : % 59.01/59.52 ( ( aElement0(W0) % 59.01/59.52 & aElement0(W1) % 59.01/59.53 & aElement0(W2) ) % 59.01/59.53 => sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) ). % 59.01/59.53 % 59.01/59.53 fof(mMulUnit,axiom, % 59.01/59.53 ! [W0] : % 59.01/59.53 ( aElement0(W0) % 59.01/59.53 => ( sdtasdt0(W0,sz10) = W0 % 59.01/59.53 & W0 = sdtasdt0(sz10,W0) ) ) ). % 59.01/59.53 % 59.01/59.53 fof(mAMDistr,axiom, % 59.01/59.53 ! [W0,W1,W2] : % 59.01/59.53 ( ( aElement0(W0) % 59.01/59.53 & aElement0(W1) % 59.01/59.53 & aElement0(W2) ) % 59.01/59.53 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 59.01/59.53 & sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ). % 59.01/59.53 % 59.01/59.53 fof(mMulMnOne,axiom, % 59.01/59.53 ! [W0] : % 59.01/59.53 ( aElement0(W0) % 59.01/59.53 => ( sdtasdt0(smndt0(sz10),W0) = smndt0(W0) % 59.01/59.53 & smndt0(W0) = sdtasdt0(W0,smndt0(sz10)) ) ) ). % 59.01/59.53 % 59.01/59.53 fof(mMulZero,axiom, % 59.01/59.53 ! [W0] : % 59.01/59.53 ( aElement0(W0) % 59.01/59.53 => ( sdtasdt0(W0,sz00) = sz00 % 59.01/59.53 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 59.01/59.53 % 59.01/59.53 fof(mCancel,axiom, % 59.01/59.53 ! [W0,W1] : % 59.01/59.53 ( ( aElement0(W0) % 59.01/59.53 & aElement0(W1) ) % 59.01/59.53 => ( sdtasdt0(W0,W1) = sz00 % 59.01/59.53 => ( W0 = sz00 % 59.01/59.53 | W1 = sz00 ) ) ) ). % 59.01/59.53 % 59.01/59.53 fof(mUnNeZr,axiom, % 59.01/59.53 sz10 != sz00 ). % 59.01/59.53 % 59.01/59.53 fof(mSetSort,axiom, % 59.01/59.53 ! [W0] : % 59.01/59.53 ( aSet0(W0) % 59.01/59.53 => $true ) ). % 59.01/59.53 % 59.01/59.53 fof(mEOfElem,axiom, % 59.01/59.53 ! [W0] : % 59.01/59.53 ( aSet0(W0) % 59.01/59.53 => ! [W1] : % 59.01/59.53 ( aElementOf0(W1,W0) % 59.01/59.53 => aElement0(W1) ) ) ). % 59.01/59.53 % 59.01/59.53 fof(mSetEq,axiom, % 59.01/59.53 ! [W0,W1] : % 59.01/59.53 ( ( aSet0(W0) % 59.01/59.53 & aSet0(W1) ) % 59.01/59.53 => ( ( ! [W2] : % 59.01/59.53 ( aElementOf0(W2,W0) % 59.01/59.53 => aElementOf0(W2,W1) ) % 59.01/59.53 & ! [W2] : % 59.01/59.53 ( aElementOf0(W2,W1) % 59.01/59.53 => aElementOf0(W2,W0) ) ) % 59.01/59.53 => W0 = W1 ) ) ). % 59.01/59.53 % 59.01/59.53 fof(mDefSSum,definition, % 59.01/59.53 ! [W0,W1] : % 59.01/59.53 ( ( aSet0(W0) % 59.01/59.53 & aSet0(W1) ) % 59.01/59.53 => ! [W2] : % 59.01/59.53 ( W2 = sdtpldt1(W0,W1) % 59.01/59.53 <=> ( aSet0(W2) % 59.01/59.53 & ! [W3] : % 59.01/59.53 ( aElementOf0(W3,W2) % 59.01/59.53 <=> ? [W4,W5] : % 59.01/59.53 ( aElementOf0(W4,W0) % 59.01/59.53 & aElementOf0(W5,W1) % 59.01/59.53 & sdtpldt0(W4,W5) = W3 ) ) ) ) ) ). % 59.01/59.53 % 59.01/59.53 fof(mDefSInt,definition, % 59.01/59.53 ! [W0,W1] : % 59.01/59.53 ( ( aSet0(W0) % 59.01/59.53 & aSet0(W1) ) % 59.01/59.53 => ! [W2] : % 59.01/59.53 ( W2 = sdtasasdt0(W0,W1) % 59.01/59.53 <=> ( aSet0(W2) % 59.01/59.53 & ! [W3] : % 59.01/59.53 ( aElementOf0(W3,W2) % 59.01/59.53 <=> ( aElementOf0(W3,W0) % 59.01/59.53 & aElementOf0(W3,W1) ) ) ) ) ) ). % 59.01/59.53 % 59.01/59.53 fof(mDefIdeal,definition, % 59.01/59.53 ! [W0] : % 59.01/59.53 ( aIdeal0(W0) % 59.01/59.53 <=> ( aSet0(W0) % 59.01/59.53 & ! [W1] : % 59.01/59.53 ( aElementOf0(W1,W0) % 59.01/59.53 => ( ! [W2] : % 59.01/59.53 ( aElementOf0(W2,W0) % 59.01/59.53 => aElementOf0(sdtpldt0(W1,W2),W0) ) % 59.01/59.53 & ! [W2] : % 59.01/59.53 ( aElement0(W2) % 59.01/59.53 => aElementOf0(sdtasdt0(W2,W1),W0) ) ) ) ) ) ). % 59.01/59.53 % 59.01/59.53 fof(mIdeSum,axiom, % 59.01/59.53 ! [W0,W1] : % 59.01/59.53 ( ( aIdeal0(W0) % 59.01/59.53 & aIdeal0(W1) ) % 59.01/59.53 => aIdeal0(sdtpldt1(W0,W1)) ) ). % 59.01/59.53 % 59.01/59.53 fof(mIdeInt,axiom, % 59.01/59.53 ! [W0,W1] : % 59.01/59.53 ( ( aIdeal0(W0) % 59.01/59.53 & aIdeal0(W1) ) % 59.01/59.53 => aIdeal0(sdtasasdt0(W0,W1)) ) ). % 59.01/59.53 % 59.01/59.53 fof(mDefMod,definition, % 59.01/59.53 ! [W0,W1,W2] : % 59.01/59.53 ( ( aElement0(W0) % 59.01/59.53 & aElement0(W1) % 59.01/59.53 & aIdeal0(W2) ) % 59.01/59.53 => ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 59.01/59.53 <=> aElementOf0(sdtpldt0(W0,smndt0(W1)),W2) ) ) ). % 59.01/59.53 % 59.01/59.53 fof(mChineseRemainder,axiom, % 59.01/59.53 ! [W0,W1] : % 59.01/59.53 ( ( aIdeal0(W0) % 59.01/59.53 & aIdeal0(W1) ) % 59.01/59.53 => ( ! [W2] : % 59.01/59.53 ( aElement0(W2) % 59.01/59.53 => aElementOf0(W2,sdtpldt1(W0,W1)) ) % 59.01/59.53 => ! [W2,W3] : % 59.01/59.53 ( ( aElement0(W2) % 59.01/59.53 & aElement0(W3) ) % 59.01/59.53 => ? [W4] : % 59.01/59.53 ( aElement0(W4) % 59.01/59.53 & sdteqdtlpzmzozddtrp0(W4,W2,W0) % 59.01/59.53 & sdteqdtlpzmzozddtrp0(W4,W3,W1) ) ) ) ) ). % 59.01/59.53 % 59.01/59.53 fof(mNatSort,axiom, % 59.01/59.53 ! [W0] : % 59.01/59.53 ( aNaturalNumber0(W0) % 59.01/59.53 => $true ) ). % 59.01/59.53 % 59.01/59.53 fof(mEucSort,axiom, % 59.01/59.53 ! [W0] : % 59.01/59.53 ( ( aElement0(W0) % 59.01/59.53 & W0 != sz00 ) % 59.01/59.53 => aNaturalNumber0(sbrdtbr0(W0)) ) ). % 59.01/59.53 % 59.01/59.53 fof(mNatLess,axiom, % 59.01/59.53 ! [W0,W1] : % 59.01/59.53 ( ( aNaturalNumber0(W0) % 59.01/59.53 & aNaturalNumber0(W1) ) % 59.01/59.53 => ( iLess0(W0,W1) % 59.01/59.53 => $true ) ) ). % 59.01/59.53 % 59.01/59.53 fof(mDivision,axiom, % 59.01/59.53 ! [W0,W1] : % 59.01/59.53 ( ( aElement0(W0) % 59.01/59.53 & aElement0(W1) % 59.01/59.53 & W1 != sz00 ) % 59.01/59.53 => ? [W2,W3] : % 59.01/59.53 ( aElement0(W2) % 59.01/59.53 & aElement0(W3) % 59.01/59.53 & W0 = sdtpldt0(sdtasdt0(W2,W1),W3) % 59.01/59.53 & ( W3 != sz00 % 59.01/59.53 => iLess0(sbrdtbr0(W3),sbrdtbr0(W1)) ) ) ) ). % 59.01/59.53 % 59.01/59.53 fof(mDefDiv,definition, % 59.01/59.53 ! [W0,W1] : % 59.01/59.53 ( ( aElement0(W0) % 59.01/59.53 & aElement0(W1) ) % 59.01/59.53 => ( doDivides0(W0,W1) % 59.01/59.53 <=> ? [W2] : % 59.01/59.53 ( aElement0(W2) % 59.01/59.53 & sdtasdt0(W0,W2) = W1 ) ) ) ). % 59.01/59.53 % 59.01/59.53 fof(mDefDvs,definition, % 59.01/59.53 ! [W0] : % 59.01/59.53 ( aElement0(W0) % 59.01/59.53 => ! [W1] : % 59.01/59.53 ( aDivisorOf0(W1,W0) % 59.01/59.53 <=> ( aElement0(W1) % 59.01/59.53 & doDivides0(W1,W0) ) ) ) ). % 59.01/59.53 % 59.01/59.53 fof(mDefGCD,definition, % 59.01/59.53 ! [W0,W1] : % 59.01/59.53 ( ( aElement0(W0) % 59.01/59.53 & aElement0(W1) ) % 59.01/59.53 => ! [W2] : % 59.01/59.53 ( aGcdOfAnd0(W2,W0,W1) % 59.01/59.53 <=> ( aDivisorOf0(W2,W0) % 59.01/59.53 & aDivisorOf0(W2,W1) % 59.01/59.53 & ! [W3] : % 59.01/59.53 ( ( aDivisorOf0(W3,W0) % 59.01/59.53 & aDivisorOf0(W3,W1) ) % 59.01/59.53 => doDivides0(W3,W2) ) ) ) ) ). % 59.01/59.53 % 59.01/59.53 fof(mDefRel,definition, % 59.01/59.53 ! [W0,W1] : % 59.01/59.53 ( ( aElement0(W0) % 59.01/59.53 & aElement0(W1) ) % 59.01/59.53 => ( misRelativelyPrime0(W0,W1) % 59.01/59.53 <=> aGcdOfAnd0(sz10,W0,W1) ) ) ). % 59.01/59.53 % 59.01/59.53 fof(mDefPrIdeal,definition, % 59.01/59.53 ! [W0] : % 59.01/59.53 ( aElement0(W0) % 59.01/59.53 => ! [W1] : % 59.01/59.53 ( W1 = slsdtgt0(W0) % 59.01/59.53 <=> ( aSet0(W1) % 59.01/59.53 & ! [W2] : % 59.01/59.53 ( aElementOf0(W2,W1) % 59.01/59.53 <=> ? [W3] : % 59.01/59.53 ( aElement0(W3) % 59.01/59.53 & sdtasdt0(W0,W3) = W2 ) ) ) ) ) ). % 59.01/59.53 % 59.01/59.53 fof(mPrIdeal,axiom, % 59.01/59.53 ! [W0] : % 59.01/59.53 ( aElement0(W0) % 59.01/59.53 => aIdeal0(slsdtgt0(W0)) ) ). % 59.01/59.53 % 59.01/59.53 fof(m__2091,hypothesis, % 59.01/59.53 ( aElement0(xa) % 59.01/59.53 & aElement0(xb) ) ). % 59.01/59.53 % 59.01/59.53 fof(m__2110,hypothesis, % 59.01/59.53 ( xa != sz00 % 59.01/59.53 | xb != sz00 ) ). % 59.01/59.53 % 59.01/59.53 fof(m__2129,hypothesis, % 59.01/59.53 aGcdOfAnd0(xc,xa,xb) ). % 59.01/59.53 % 59.01/59.53 fof(m__2174,hypothesis, % 59.01/59.53 ( aIdeal0(xI) % 59.01/59.53 & xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)) ) ). % 59.01/59.53 % 59.01/59.53 fof(m__2203,hypothesis, % 59.01/59.53 ( aElementOf0(sz00,slsdtgt0(xa)) % 59.01/59.53 & aElementOf0(xa,slsdtgt0(xa)) % 59.01/59.53 & aElementOf0(sz00,slsdtgt0(xb)) % 59.01/59.53 & aElementOf0(xb,slsdtgt0(xb)) ) ). % 59.01/59.53 % 59.01/59.53 fof(m__2228,hypothesis, % 59.01/59.53 ? [W0] : % 59.01/59.53 ( aElementOf0(W0,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))) % 59.01/59.53 & W0 != sz00 ) ). % 59.01/59.53 % 59.01/59.53 fof(m__2351,hypothesis, % 59.01/59.53 ! [W0] : % 59.01/59.53 ( ( aElementOf0(W0,xI) % 59.01/59.53 & W0 != sz00 ) % 59.01/59.53 => ? [W1] : % 59.01/59.53 ( aElementOf0(W1,xI) % 59.01/59.53 & W1 != sz00 % 59.01/59.53 & ! [W2] : % 59.01/59.53 ( ( aElementOf0(W2,xI) % 59.01/59.53 & W2 != sz00 ) % 59.01/59.53 => ~ iLess0(sbrdtbr0(W2),sbrdtbr0(W1)) ) ) ) ). % 59.01/59.53 % 59.01/59.53 fof(m__,conjecture, % 59.01/59.53 ? [W0] : % 59.01/59.53 ( aElementOf0(W0,xI) % 59.01/59.53 & W0 != sz00 % 59.01/59.53 & ! [W1] : % 59.01/59.53 ( ( aElementOf0(W1,xI) % 59.01/59.53 & W1 != sz00 ) % 59.01/59.53 => ~ iLess0(sbrdtbr0(W1),sbrdtbr0(W0)) ) ) ). % 59.01/59.53 % 59.01/59.53 %------------------------------------------------------------------------------ % 59.01/59.53 %------------------------------------------- % 59.01/59.53 % Proof found % 59.01/59.53 % SZS status Theorem for theBenchmark % 59.01/59.53 % SZS output start Proof % 59.01/59.53 %ClaNum:191(EqnAxiom:84) % 59.01/59.53 %VarNum:720(SingletonVarNum:220) % 59.01/59.53 %MaxLitNum:8 % 59.01/59.53 %MaxfuncDepth:2 % 59.01/59.53 %SharedTerms:31 % 59.01/59.53 %goalClause: 116 122 137 % 59.01/59.53 [85]P1(a1) % 59.01/59.53 [86]P1(a32) % 59.01/59.53 [87]P1(a33) % 59.01/59.53 [88]P1(a35) % 59.01/59.53 [89]P3(a34) % 59.01/59.53 [95]P5(a36,a33,a35) % 59.01/59.53 [97]~E(a1,a32) % 59.01/59.53 [98]~E(a4,a1) % 59.01/59.54 [90]P4(a1,f2(a33)) % 59.01/59.54 [91]P4(a1,f2(a35)) % 59.01/59.54 [92]P4(a33,f2(a33)) % 59.01/59.54 [93]P4(a35,f2(a35)) % 59.01/59.54 [94]E(f3(f2(a33),f2(a35)),a34) % 59.01/59.54 [96]P4(a4,f3(f2(a33),f2(a35))) % 59.01/59.54 [99]~E(a1,a33)+~E(a1,a35) % 59.01/59.54 [100]~P3(x1001)+P6(x1001) % 59.01/59.54 [101]~P1(x1011)+P1(f31(x1011)) % 59.01/59.54 [102]~P1(x1021)+P3(f2(x1021)) % 59.01/59.54 [104]~P1(x1041)+E(f28(a1,x1041),a1) % 59.01/59.54 [105]~P1(x1051)+E(f28(x1051,a1),a1) % 59.01/59.54 [107]~P1(x1071)+E(f30(a1,x1071),x1071) % 59.01/59.54 [108]~P1(x1081)+E(f28(a32,x1081),x1081) % 59.01/59.54 [109]~P1(x1091)+E(f30(x1091,a1),x1091) % 59.01/59.54 [110]~P1(x1101)+E(f28(x1101,a32),x1101) % 59.01/59.54 [112]~P1(x1121)+E(f30(f31(x1121),x1121),a1) % 59.01/59.54 [113]~P1(x1131)+E(f30(x1131,f31(x1131)),a1) % 59.01/59.54 [114]~P1(x1141)+E(f28(x1141,f31(a32)),f31(x1141)) % 59.01/59.54 [115]~P1(x1151)+E(f28(f31(a32),x1151),f31(x1151)) % 59.01/59.54 [111]~P4(x1111,a34)+E(x1111,a1)+~E(a18,a1) % 59.01/59.54 [118]~P4(x1181,a34)+E(x1181,a1)+P4(a18,a34) % 59.01/59.54 [103]~P1(x1031)+E(x1031,a1)+P7(f17(x1031)) % 59.01/59.54 [116]~P4(x1161,a34)+E(x1161,a1)+~E(f19(x1161),a1) % 59.01/59.54 [117]~P6(x1171)+P3(x1171)+P4(f20(x1171),x1171) % 59.01/59.54 [122]~P4(x1221,a34)+E(x1221,a1)+P4(f19(x1221),a34) % 59.01/59.54 [137]~P4(x1371,a34)+E(x1371,a1)+P9(f17(f19(x1371)),f17(x1371)) % 59.01/59.54 [119]~P4(x1191,x1192)+P1(x1191)+~P6(x1192) % 59.01/59.54 [120]~P2(x1201,x1202)+P1(x1201)+~P1(x1202) % 59.01/59.54 [128]~P1(x1282)+~P2(x1281,x1282)+P8(x1281,x1282) % 59.01/59.54 [106]~P1(x1062)+P6(x1061)+~E(x1061,f2(x1062)) % 59.01/59.54 [123]~P1(x1232)+~P1(x1231)+E(f30(x1231,x1232),f30(x1232,x1231)) % 59.01/59.54 [124]~P1(x1242)+~P1(x1241)+E(f28(x1241,x1242),f28(x1242,x1241)) % 59.01/59.54 [129]~P1(x1292)+~P1(x1291)+P1(f30(x1291,x1292)) % 59.01/59.54 [130]~P1(x1302)+~P1(x1301)+P1(f28(x1301,x1302)) % 59.01/59.54 [131]~P3(x1312)+~P3(x1311)+P3(f3(x1311,x1312)) % 59.01/59.54 [132]~P3(x1322)+~P3(x1321)+P3(f29(x1321,x1322)) % 59.01/59.54 [127]~P6(x1271)+P3(x1271)+P4(f6(x1271),x1271)+P1(f5(x1271)) % 59.01/59.54 [160]~P6(x1601)+P3(x1601)+P1(f5(x1601))+~P4(f30(f20(x1601),f6(x1601)),x1601) % 59.01/59.54 [163]~P6(x1631)+P3(x1631)+P4(f6(x1631),x1631)+~P4(f28(f5(x1631),f20(x1631)),x1631) % 59.01/59.54 [172]~P6(x1721)+P3(x1721)+~P4(f30(f20(x1721),f6(x1721)),x1721)+~P4(f28(f5(x1721),f20(x1721)),x1721) % 59.01/59.54 [135]~P1(x1352)+~P1(x1351)+~P8(x1351,x1352)+P2(x1351,x1352) % 59.01/59.54 [145]~P1(x1452)+~P1(x1451)+~P10(x1451,x1452)+P5(a32,x1451,x1452) % 59.01/59.54 [153]~P1(x1532)+~P1(x1531)+P10(x1531,x1532)+~P5(a32,x1531,x1532) % 59.01/59.54 [133]~P1(x1331)+~P1(x1332)+E(x1331,a1)+P1(f7(x1332,x1331)) % 59.01/59.54 [134]~P1(x1341)+~P1(x1342)+E(x1341,a1)+P1(f10(x1342,x1341)) % 59.01/59.54 [139]~P1(x1392)+~P1(x1391)+~P8(x1391,x1392)+P1(f11(x1391,x1392)) % 59.01/59.54 [143]~P1(x1432)+~P1(x1431)+~P8(x1431,x1432)+E(f28(x1431,f11(x1431,x1432)),x1432) % 59.01/59.54 [165]~P1(x1651)+~P1(x1652)+E(x1651,a1)+E(f30(f28(f7(x1652,x1651),x1651),f10(x1652,x1651)),x1652) % 59.01/59.54 [155]~P1(x1552)+~P5(x1551,x1553,x1552)+P2(x1551,x1552)+~P1(x1553) % 59.01/59.54 [156]~P1(x1562)+~P5(x1561,x1562,x1563)+P2(x1561,x1562)+~P1(x1563) % 59.01/59.54 [125]~P6(x1253)+~P6(x1252)+P6(x1251)+~E(x1251,f3(x1252,x1253)) % 59.01/59.54 [126]~P6(x1263)+~P6(x1262)+P6(x1261)+~E(x1261,f29(x1262,x1263)) % 59.01/59.54 [142]~P1(x1421)+~P3(x1423)+~P4(x1422,x1423)+P4(f28(x1421,x1422),x1423) % 59.01/59.54 [147]~P3(x1473)+~P4(x1471,x1473)+~P4(x1472,x1473)+P4(f30(x1471,x1472),x1473) % 59.01/59.54 [167]~P1(x1671)+~P4(x1673,x1672)+~E(x1672,f2(x1671))+P1(f14(x1671,x1672,x1673)) % 59.01/59.54 [150]~P1(x1503)+~P1(x1502)+~P1(x1501)+E(f30(f30(x1501,x1502),x1503),f30(x1501,f30(x1502,x1503))) % 59.01/59.54 [151]~P1(x1513)+~P1(x1512)+~P1(x1511)+E(f28(f28(x1511,x1512),x1513),f28(x1511,f28(x1512,x1513))) % 59.01/59.54 [161]~P1(x1613)+~P1(x1612)+~P1(x1611)+E(f30(f28(x1611,x1612),f28(x1611,x1613)),f28(x1611,f30(x1612,x1613))) % 59.01/59.54 [162]~P1(x1622)+~P1(x1623)+~P1(x1621)+E(f30(f28(x1621,x1622),f28(x1623,x1622)),f28(f30(x1621,x1623),x1622)) % 59.01/59.54 [169]~P1(x1691)+~P4(x1693,x1692)+~E(x1692,f2(x1691))+E(f28(x1691,f14(x1691,x1692,x1693)),x1693) % 59.01/59.54 [121]~P1(x1211)+~P1(x1212)+E(x1211,a1)+E(x1212,a1)+~E(f28(x1212,x1211),a1) % 59.01/59.54 [144]~P4(x1441,a34)+~P4(x1442,a34)+E(x1441,a1)+E(x1442,a1)+~P9(f17(x1442),f17(a18)) % 59.01/59.54 [146]~P1(x1462)+~P6(x1461)+P4(f13(x1462,x1461),x1461)+E(x1461,f2(x1462))+P1(f12(x1462,x1461)) % 59.01/59.54 [148]~P6(x1482)+~P6(x1481)+E(x1481,x1482)+P4(f16(x1481,x1482),x1481)+P4(f21(x1481,x1482),x1482) % 59.01/59.54 [157]~P6(x1572)+~P6(x1571)+E(x1571,x1572)+P4(f16(x1571,x1572),x1571)+~P4(f21(x1571,x1572),x1571) % 59.01/59.54 [158]~P6(x1582)+~P6(x1581)+E(x1581,x1582)+P4(f21(x1581,x1582),x1582)+~P4(f16(x1581,x1582),x1582) % 59.01/59.54 [166]~P6(x1662)+~P6(x1661)+E(x1661,x1662)+~P4(f16(x1661,x1662),x1662)+~P4(f21(x1661,x1662),x1661) % 59.01/59.54 [152]~P1(x1521)+~P1(x1522)+E(x1521,a1)+P9(f17(f10(x1522,x1521)),f17(x1521))+E(f10(x1522,x1521),a1) % 59.01/59.54 [154]~P1(x1542)+~P6(x1541)+P4(f13(x1542,x1541),x1541)+E(x1541,f2(x1542))+E(f28(x1542,f12(x1542,x1541)),f13(x1542,x1541)) % 59.01/59.54 [136]~P1(x1362)+~P1(x1361)+~P1(x1363)+P8(x1361,x1362)+~E(f28(x1361,x1363),x1362) % 59.01/59.54 [168]~P1(x1682)+~P1(x1681)+~P3(x1683)+P11(x1681,x1682,x1683)+~P4(f30(x1681,f31(x1682)),x1683) % 59.01/59.54 [170]~P1(x1702)+~P1(x1701)+~P3(x1703)+~P11(x1701,x1702,x1703)+P4(f30(x1701,f31(x1702)),x1703) % 59.01/59.54 [138]~P1(x1383)+~P1(x1384)+P4(x1381,x1382)+~E(f28(x1383,x1384),x1381)+~E(x1382,f2(x1383)) % 59.01/59.54 [140]~P6(x1404)+~P6(x1402)+~P4(x1401,x1403)+P4(x1401,x1402)+~E(x1403,f29(x1404,x1402)) % 59.01/59.54 [141]~P6(x1414)+~P6(x1412)+~P4(x1411,x1413)+P4(x1411,x1412)+~E(x1413,f29(x1412,x1414)) % 59.01/59.54 [183]~P6(x1832)+~P6(x1831)+~P4(x1834,x1833)+~E(x1833,f3(x1831,x1832))+P4(f23(x1831,x1832,x1833,x1834),x1831) % 59.01/59.54 [184]~P6(x1842)+~P6(x1841)+~P4(x1844,x1843)+~E(x1843,f3(x1841,x1842))+P4(f24(x1841,x1842,x1843,x1844),x1842) % 59.01/59.54 [191]~P6(x1912)+~P6(x1911)+~P4(x1914,x1913)+~E(x1913,f3(x1911,x1912))+E(f30(f23(x1911,x1912,x1913,x1914),f24(x1911,x1912,x1913,x1914)),x1914) % 59.01/59.54 [164]~P1(x1643)+~P1(x1642)+~P6(x1641)+~P4(f13(x1642,x1641),x1641)+~E(f13(x1642,x1641),f28(x1642,x1643))+E(x1641,f2(x1642)) % 59.01/59.54 [173]~P1(x1733)+~P1(x1732)+~P2(x1731,x1733)+~P2(x1731,x1732)+P5(x1731,x1732,x1733)+P2(f15(x1732,x1733,x1731),x1733) % 59.01/59.54 [174]~P1(x1743)+~P1(x1742)+~P2(x1741,x1743)+~P2(x1741,x1742)+P5(x1741,x1742,x1743)+P2(f15(x1742,x1743,x1741),x1742) % 59.01/59.54 [175]~P6(x1751)+~P6(x1753)+~P6(x1752)+P4(f22(x1752,x1753,x1751),x1751)+P4(f25(x1752,x1753,x1751),x1752)+E(x1751,f3(x1752,x1753)) % 59.01/59.54 [176]~P6(x1761)+~P6(x1763)+~P6(x1762)+P4(f22(x1762,x1763,x1761),x1761)+P4(f26(x1762,x1763,x1761),x1763)+E(x1761,f3(x1762,x1763)) % 59.01/59.54 [177]~P6(x1771)+~P6(x1773)+~P6(x1772)+P4(f27(x1772,x1773,x1771),x1771)+P4(f27(x1772,x1773,x1771),x1773)+E(x1771,f29(x1772,x1773)) % 59.01/59.54 [178]~P6(x1781)+~P6(x1783)+~P6(x1782)+P4(f27(x1782,x1783,x1781),x1781)+P4(f27(x1782,x1783,x1781),x1782)+E(x1781,f29(x1782,x1783)) % 59.01/59.54 [179]~P1(x1793)+~P1(x1792)+~P2(x1791,x1793)+~P2(x1791,x1792)+P5(x1791,x1792,x1793)+~P8(f15(x1792,x1793,x1791),x1791) % 59.01/59.54 [181]~P6(x1811)+~P6(x1813)+~P6(x1812)+P4(f22(x1812,x1813,x1811),x1811)+E(x1811,f3(x1812,x1813))+E(f30(f25(x1812,x1813,x1811),f26(x1812,x1813,x1811)),f22(x1812,x1813,x1811)) % 59.01/59.54 [171]~P2(x1711,x1713)+~P2(x1711,x1714)+~P5(x1712,x1714,x1713)+P8(x1711,x1712)+~P1(x1713)+~P1(x1714) % 59.01/59.54 [149]~P6(x1494)+~P6(x1493)+~P4(x1491,x1494)+~P4(x1491,x1493)+P4(x1491,x1492)+~E(x1492,f29(x1493,x1494)) % 59.01/59.54 [182]~P1(x1824)+~P1(x1823)+~P3(x1822)+~P3(x1821)+P1(f8(x1821,x1822))+P1(f9(x1821,x1822,x1823,x1824)) % 59.01/59.54 [185]~P1(x1854)+~P1(x1853)+~P3(x1852)+~P3(x1851)+P11(f9(x1851,x1852,x1853,x1854),x1854,x1852)+P1(f8(x1851,x1852)) % 59.01/59.54 [186]~P1(x1864)+~P1(x1863)+~P3(x1862)+~P3(x1861)+P11(f9(x1861,x1862,x1863,x1864),x1863,x1861)+P1(f8(x1861,x1862)) % 59.01/59.54 [188]~P1(x1884)+~P1(x1883)+~P3(x1882)+~P3(x1881)+~P4(f8(x1881,x1882),f3(x1881,x1882))+P1(f9(x1881,x1882,x1883,x1884)) % 59.01/59.54 [189]~P1(x1894)+~P1(x1893)+~P3(x1892)+~P3(x1891)+P11(f9(x1891,x1892,x1893,x1894),x1894,x1892)+~P4(f8(x1891,x1892),f3(x1891,x1892)) % 59.01/59.54 [190]~P1(x1904)+~P1(x1903)+~P3(x1902)+~P3(x1901)+P11(f9(x1901,x1902,x1903,x1904),x1903,x1901)+~P4(f8(x1901,x1902),f3(x1901,x1902)) % 59.01/59.54 [187]~P6(x1871)+~P6(x1873)+~P6(x1872)+~P4(f27(x1872,x1873,x1871),x1871)+~P4(f27(x1872,x1873,x1871),x1873)+~P4(f27(x1872,x1873,x1871),x1872)+E(x1871,f29(x1872,x1873)) % 59.01/59.54 [159]~P6(x1594)+~P6(x1593)+~P4(x1596,x1594)+~P4(x1595,x1593)+P4(x1591,x1592)+~E(x1592,f3(x1593,x1594))+~E(f30(x1595,x1596),x1591) % 59.01/59.54 [180]~P6(x1801)+~P6(x1803)+~P6(x1802)+~P4(x1805,x1803)+~P4(x1804,x1802)+~P4(f22(x1802,x1803,x1801),x1801)+E(x1801,f3(x1802,x1803))+~E(f30(x1804,x1805),f22(x1802,x1803,x1801)) % 59.01/59.54 %EqnAxiom % 59.01/59.54 [1]E(x11,x11) % 59.01/59.54 [2]E(x22,x21)+~E(x21,x22) % 59.01/59.54 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 59.01/59.54 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 59.01/59.54 [5]~E(x51,x52)+E(f3(x51,x53),f3(x52,x53)) % 59.01/59.54 [6]~E(x61,x62)+E(f3(x63,x61),f3(x63,x62)) % 59.01/59.54 [7]~E(x71,x72)+E(f30(x71,x73),f30(x72,x73)) % 59.01/59.54 [8]~E(x81,x82)+E(f30(x83,x81),f30(x83,x82)) % 59.01/59.54 [9]~E(x91,x92)+E(f24(x91,x93,x94,x95),f24(x92,x93,x94,x95)) % 59.01/59.54 [10]~E(x101,x102)+E(f24(x103,x101,x104,x105),f24(x103,x102,x104,x105)) % 59.01/59.54 [11]~E(x111,x112)+E(f24(x113,x114,x111,x115),f24(x113,x114,x112,x115)) % 59.01/59.54 [12]~E(x121,x122)+E(f24(x123,x124,x125,x121),f24(x123,x124,x125,x122)) % 59.01/59.54 [13]~E(x131,x132)+E(f23(x131,x133,x134,x135),f23(x132,x133,x134,x135)) % 59.01/59.54 [14]~E(x141,x142)+E(f23(x143,x141,x144,x145),f23(x143,x142,x144,x145)) % 59.01/59.54 [15]~E(x151,x152)+E(f23(x153,x154,x151,x155),f23(x153,x154,x152,x155)) % 59.01/59.54 [16]~E(x161,x162)+E(f23(x163,x164,x165,x161),f23(x163,x164,x165,x162)) % 59.01/59.54 [17]~E(x171,x172)+E(f27(x171,x173,x174),f27(x172,x173,x174)) % 59.01/59.54 [18]~E(x181,x182)+E(f27(x183,x181,x184),f27(x183,x182,x184)) % 59.01/59.54 [19]~E(x191,x192)+E(f27(x193,x194,x191),f27(x193,x194,x192)) % 59.01/59.54 [20]~E(x201,x202)+E(f29(x201,x203),f29(x202,x203)) % 59.01/59.54 [21]~E(x211,x212)+E(f29(x213,x211),f29(x213,x212)) % 59.01/59.54 [22]~E(x221,x222)+E(f8(x221,x223),f8(x222,x223)) % 59.01/59.54 [23]~E(x231,x232)+E(f8(x233,x231),f8(x233,x232)) % 59.01/59.54 [24]~E(x241,x242)+E(f9(x241,x243,x244,x245),f9(x242,x243,x244,x245)) % 59.01/59.54 [25]~E(x251,x252)+E(f9(x253,x251,x254,x255),f9(x253,x252,x254,x255)) % 59.01/59.54 [26]~E(x261,x262)+E(f9(x263,x264,x261,x265),f9(x263,x264,x262,x265)) % 59.01/59.54 [27]~E(x271,x272)+E(f9(x273,x274,x275,x271),f9(x273,x274,x275,x272)) % 59.01/59.54 [28]~E(x281,x282)+E(f13(x281,x283),f13(x282,x283)) % 59.01/59.54 [29]~E(x291,x292)+E(f13(x293,x291),f13(x293,x292)) % 59.01/59.54 [30]~E(x301,x302)+E(f31(x301),f31(x302)) % 59.01/59.54 [31]~E(x311,x312)+E(f16(x311,x313),f16(x312,x313)) % 59.01/59.54 [32]~E(x321,x322)+E(f16(x323,x321),f16(x323,x322)) % 59.01/59.54 [33]~E(x331,x332)+E(f17(x331),f17(x332)) % 59.01/59.54 [34]~E(x341,x342)+E(f28(x341,x343),f28(x342,x343)) % 59.01/59.54 [35]~E(x351,x352)+E(f28(x353,x351),f28(x353,x352)) % 59.01/59.54 [36]~E(x361,x362)+E(f21(x361,x363),f21(x362,x363)) % 59.01/59.54 [37]~E(x371,x372)+E(f21(x373,x371),f21(x373,x372)) % 59.01/59.54 [38]~E(x381,x382)+E(f26(x381,x383,x384),f26(x382,x383,x384)) % 59.01/59.54 [39]~E(x391,x392)+E(f26(x393,x391,x394),f26(x393,x392,x394)) % 59.01/59.54 [40]~E(x401,x402)+E(f26(x403,x404,x401),f26(x403,x404,x402)) % 59.01/59.54 [41]~E(x411,x412)+E(f15(x411,x413,x414),f15(x412,x413,x414)) % 59.01/59.54 [42]~E(x421,x422)+E(f15(x423,x421,x424),f15(x423,x422,x424)) % 59.01/59.54 [43]~E(x431,x432)+E(f15(x433,x434,x431),f15(x433,x434,x432)) % 59.01/59.54 [44]~E(x441,x442)+E(f6(x441),f6(x442)) % 59.01/59.54 [45]~E(x451,x452)+E(f25(x451,x453,x454),f25(x452,x453,x454)) % 59.01/59.54 [46]~E(x461,x462)+E(f25(x463,x461,x464),f25(x463,x462,x464)) % 59.15/59.55 [47]~E(x471,x472)+E(f25(x473,x474,x471),f25(x473,x474,x472)) % 59.15/59.55 [48]~E(x481,x482)+E(f12(x481,x483),f12(x482,x483)) % 59.15/59.55 [49]~E(x491,x492)+E(f12(x493,x491),f12(x493,x492)) % 59.15/59.55 [50]~E(x501,x502)+E(f22(x501,x503,x504),f22(x502,x503,x504)) % 59.15/59.55 [51]~E(x511,x512)+E(f22(x513,x511,x514),f22(x513,x512,x514)) % 59.15/59.55 [52]~E(x521,x522)+E(f22(x523,x524,x521),f22(x523,x524,x522)) % 59.15/59.55 [53]~E(x531,x532)+E(f10(x531,x533),f10(x532,x533)) % 59.15/59.55 [54]~E(x541,x542)+E(f10(x543,x541),f10(x543,x542)) % 59.15/59.55 [55]~E(x551,x552)+E(f19(x551),f19(x552)) % 59.15/59.55 [56]~E(x561,x562)+E(f7(x561,x563),f7(x562,x563)) % 59.15/59.55 [57]~E(x571,x572)+E(f7(x573,x571),f7(x573,x572)) % 59.15/59.55 [58]~E(x581,x582)+E(f11(x581,x583),f11(x582,x583)) % 59.15/59.55 [59]~E(x591,x592)+E(f11(x593,x591),f11(x593,x592)) % 59.15/59.55 [60]~E(x601,x602)+E(f20(x601),f20(x602)) % 59.15/59.55 [61]~E(x611,x612)+E(f5(x611),f5(x612)) % 59.15/59.55 [62]~E(x621,x622)+E(f14(x621,x623,x624),f14(x622,x623,x624)) % 59.15/59.55 [63]~E(x631,x632)+E(f14(x633,x631,x634),f14(x633,x632,x634)) % 59.15/59.55 [64]~E(x641,x642)+E(f14(x643,x644,x641),f14(x643,x644,x642)) % 59.15/59.55 [65]~P1(x651)+P1(x652)+~E(x651,x652) % 59.15/59.55 [66]P4(x662,x663)+~E(x661,x662)+~P4(x661,x663) % 59.15/59.55 [67]P4(x673,x672)+~E(x671,x672)+~P4(x673,x671) % 59.15/59.55 [68]~P6(x681)+P6(x682)+~E(x681,x682) % 59.15/59.55 [69]~P3(x691)+P3(x692)+~E(x691,x692) % 59.15/59.55 [70]P2(x702,x703)+~E(x701,x702)+~P2(x701,x703) % 59.15/59.55 [71]P2(x713,x712)+~E(x711,x712)+~P2(x713,x711) % 59.15/59.55 [72]P8(x722,x723)+~E(x721,x722)+~P8(x721,x723) % 59.15/59.55 [73]P8(x733,x732)+~E(x731,x732)+~P8(x733,x731) % 59.15/59.55 [74]P11(x742,x743,x744)+~E(x741,x742)+~P11(x741,x743,x744) % 59.15/59.55 [75]P11(x753,x752,x754)+~E(x751,x752)+~P11(x753,x751,x754) % 59.15/59.55 [76]P11(x763,x764,x762)+~E(x761,x762)+~P11(x763,x764,x761) % 59.15/59.55 [77]P5(x772,x773,x774)+~E(x771,x772)+~P5(x771,x773,x774) % 59.15/59.55 [78]P5(x783,x782,x784)+~E(x781,x782)+~P5(x783,x781,x784) % 59.15/59.55 [79]P5(x793,x794,x792)+~E(x791,x792)+~P5(x793,x794,x791) % 59.15/59.55 [80]P10(x802,x803)+~E(x801,x802)+~P10(x801,x803) % 59.15/59.55 [81]P10(x813,x812)+~E(x811,x812)+~P10(x813,x811) % 59.15/59.55 [82]P9(x822,x823)+~E(x821,x822)+~P9(x821,x823) % 59.15/59.55 [83]P9(x833,x832)+~E(x831,x832)+~P9(x833,x831) % 59.15/59.55 [84]~P7(x841)+P7(x842)+~E(x841,x842) % 59.15/59.55 % 59.15/59.55 %------------------------------------------- % 59.15/59.55 cnf(192,plain, % 59.15/59.55 (~P1(x1921)+P6(f2(x1921))), % 59.15/59.55 inference(equality_inference,[],[106])). % 59.15/59.55 cnf(193,plain, % 59.15/59.55 (~P6(x1931)+~P6(x1932)+P6(f3(x1932,x1931))), % 59.15/59.55 inference(equality_inference,[],[125])). % 59.15/59.55 cnf(194,plain, % 59.15/59.55 (~P6(x1941)+~P6(x1942)+P6(f29(x1942,x1941))), % 59.15/59.55 inference(equality_inference,[],[126])). % 59.15/59.55 cnf(195,plain, % 59.15/59.55 (P8(x1951,f28(x1951,x1952))+~P1(f28(x1951,x1952))+~P1(x1951)+~P1(x1952)), % 59.15/59.55 inference(equality_inference,[],[136])). % 59.15/59.55 cnf(198,plain, % 59.15/59.55 (~P4(x1981,x1982)+~P6(x1983)+~P4(x1981,x1983)+~P6(x1982)+P4(x1981,f29(x1982,x1983))), % 59.15/59.55 inference(equality_inference,[],[149])). % 59.15/59.55 cnf(199,plain, % 59.15/59.55 (~P1(x1991)+~P4(x1992,f2(x1991))+P1(f14(x1991,f2(x1991),x1992))), % 59.15/59.55 inference(equality_inference,[],[167])). % 59.15/59.55 cnf(204,plain, % 59.15/59.55 (E(a34,f3(f2(a33),f2(a35)))), % 59.15/59.55 inference(scs_inference,[],[94,2])). % 59.15/59.55 cnf(205,plain, % 59.15/59.55 (P4(a4,a34)), % 59.15/59.55 inference(scs_inference,[],[96,94,2,67])). % 59.15/59.55 cnf(206,plain, % 59.15/59.55 (P3(f3(f2(a33),f2(a35)))), % 59.15/59.55 inference(scs_inference,[],[89,96,94,2,67,69])). % 59.15/59.55 cnf(231,plain, % 59.15/59.55 (~P6(a34)+P6(f3(f2(a33),f2(a35)))), % 59.15/59.55 inference(scs_inference,[],[204,96,92,67,66,68])). % 59.15/59.55 cnf(242,plain, % 59.15/59.55 (~P6(f3(f2(a33),f2(a35)))+P6(a34)), % 59.15/59.55 inference(scs_inference,[],[94,93,67,68])). % 59.15/59.55 cnf(243,plain, % 59.15/59.55 (P4(x2431,f2(a35))+~E(a1,x2431)), % 59.15/59.55 inference(scs_inference,[],[94,91,93,67,68,66])). % 59.15/59.55 cnf(254,plain, % 59.15/59.55 (P4(x2541,f2(a33))+~E(a1,x2541)), % 59.15/59.55 inference(scs_inference,[],[90,66])). % 59.15/59.55 cnf(271,plain, % 59.15/59.55 (~P6(f2(a35))+P4(a1,f29(f2(a35),f2(a35)))), % 59.15/59.55 inference(scs_inference,[],[204,91,125,198])). % 59.15/59.55 cnf(280,plain, % 59.15/59.55 (P6(f3(f2(a33),f2(a35)))), % 59.15/59.55 inference(scs_inference,[],[89,100,231])). % 59.15/59.55 cnf(281,plain, % 59.15/59.55 (P6(a34)), % 59.15/59.55 inference(scs_inference,[],[280,242])). % 59.15/59.55 cnf(320,plain, % 59.15/59.55 (P1(f31(a4))), % 59.15/59.55 inference(scs_inference,[],[280,96,101,119])). % 59.15/59.55 cnf(338,plain, % 59.15/59.55 (P3(f2(f31(a1)))), % 59.15/59.55 inference(scs_inference,[],[85,102,101])). % 59.15/59.55 cnf(354,plain, % 59.15/59.55 (P4(a1,f29(f2(a35),f2(a35)))), % 59.15/59.55 inference(scs_inference,[],[88,192,271])). % 59.15/59.55 cnf(356,plain, % 59.15/59.55 (P4(x3561,f29(f2(a35),f2(a35)))+~E(a1,x3561)), % 59.15/59.55 inference(scs_inference,[],[354,67,66])). % 59.15/59.55 cnf(423,plain, % 59.15/59.55 (E(f28(a1,f31(a32)),a1)), % 59.15/59.55 inference(scs_inference,[],[86,104,101])). % 59.15/59.55 cnf(424,plain, % 59.15/59.55 (E(a1,f28(a1,f31(a32)))), % 59.15/59.55 inference(scs_inference,[],[423,2])). % 59.15/59.55 cnf(427,plain, % 59.15/59.55 (P1(f28(a1,f31(a32)))), % 59.15/59.55 inference(scs_inference,[],[354,98,85,423,2,3,66,65])). % 59.15/59.55 cnf(428,plain, % 59.15/59.55 (P4(f28(a1,f31(a32)),f2(a35))), % 59.15/59.55 inference(scs_inference,[],[354,98,85,423,2,3,66,65,243])). % 59.15/59.55 cnf(429,plain, % 59.15/59.55 (P4(f28(a1,f31(a32)),f2(a33))), % 59.15/59.55 inference(scs_inference,[],[354,98,85,423,2,3,66,65,243,254])). % 59.15/59.55 cnf(445,plain, % 59.15/59.55 (P8(a1,a1)+~P1(f31(a32))), % 59.15/59.55 inference(scs_inference,[],[204,428,85,423,84,69,67,125,136])). % 59.15/59.55 cnf(459,plain, % 59.15/59.55 (P4(a1,x4591)+~P1(f31(a32))+~E(x4591,f2(a1))), % 59.15/59.55 inference(scs_inference,[],[204,205,85,423,138])). % 59.15/59.55 cnf(460,plain, % 59.15/59.55 (P4(a1,f2(a1))+~P1(f31(a32))), % 59.15/59.55 inference(equality_inference,[],[459])). % 59.15/59.55 cnf(464,plain, % 59.15/59.55 (P8(f28(a1,f31(a32)),a1)+~P1(f31(a32))), % 59.15/59.55 inference(scs_inference,[],[424,445,72])). % 59.15/59.55 cnf(480,plain, % 59.15/59.55 (E(f28(f31(a32),a1),a1)), % 59.15/59.55 inference(scs_inference,[],[86,105,101])). % 59.15/59.55 cnf(481,plain, % 59.15/59.55 (E(a1,f28(f31(a32),a1))), % 59.15/59.55 inference(scs_inference,[],[480,2])). % 59.15/59.55 cnf(483,plain, % 59.15/59.55 (P1(f28(f31(a32),a1))), % 59.15/59.55 inference(scs_inference,[],[98,85,480,2,3,65])). % 59.15/59.55 cnf(484,plain, % 59.15/59.55 (P4(f28(f31(a32),a1),f29(f2(a35),f2(a35)))), % 59.15/59.55 inference(scs_inference,[],[98,85,480,2,3,65,356])). % 59.15/59.55 cnf(505,plain, % 59.15/59.55 (P8(f31(a32),a1)+~P1(f31(a32))), % 59.15/59.55 inference(scs_inference,[],[204,481,484,85,480,84,69,67,125,136])). % 59.15/59.55 cnf(526,plain, % 59.15/59.55 (E(f30(a1,f31(a32)),f31(a32))), % 59.15/59.55 inference(scs_inference,[],[86,107,101])). % 59.15/59.55 cnf(527,plain, % 59.15/59.55 (E(f31(a32),f30(a1,f31(a32)))), % 59.15/59.55 inference(scs_inference,[],[526,2])). % 59.15/59.55 cnf(563,plain, % 59.15/59.55 (E(f28(a32,f31(a32)),f31(a32))), % 59.15/59.55 inference(scs_inference,[],[86,108,101])). % 59.15/59.55 cnf(564,plain, % 59.15/59.55 (E(f31(a32),f28(a32,f31(a32)))), % 59.15/59.55 inference(scs_inference,[],[563,2])). % 59.15/59.55 cnf(565,plain, % 59.15/59.55 (E(f30(a1,f31(a32)),f28(a32,f31(a32)))), % 59.15/59.55 inference(scs_inference,[],[526,563,2,3])). % 59.15/59.55 cnf(623,plain, % 59.15/59.55 (E(f30(f31(a32),a1),f31(a32))), % 59.15/59.55 inference(scs_inference,[],[86,109,101])). % 59.15/59.55 cnf(624,plain, % 59.15/59.55 (E(f31(a32),f30(f31(a32),a1))), % 59.15/59.55 inference(scs_inference,[],[623,2])). % 59.15/59.55 cnf(789,plain, % 59.15/59.55 (E(f28(a32,f31(a32)),f30(f31(a32),a1))), % 59.15/59.55 inference(scs_inference,[],[624,563,3])). % 59.15/59.55 cnf(873,plain, % 59.15/59.55 (P4(a1,f2(a1))), % 59.15/59.55 inference(scs_inference,[],[86,460,101])). % 59.15/59.55 cnf(977,plain, % 59.15/59.55 (P8(f30(a1,f31(a32)),a1)+~P1(f31(a32))), % 59.15/59.55 inference(scs_inference,[],[527,505,72])). % 59.15/59.55 cnf(992,plain, % 59.15/59.55 (P4(f28(f31(a32),a1),f2(a1))), % 59.15/59.55 inference(scs_inference,[],[481,873,66])). % 59.15/59.55 cnf(1903,plain, % 59.15/59.55 (P8(f28(a1,f31(a32)),a1)), % 59.15/59.55 inference(scs_inference,[],[86,464,101])). % 59.15/59.55 cnf(1904,plain, % 59.15/59.55 (P8(a1,a1)), % 59.15/59.55 inference(scs_inference,[],[1903,423,72])). % 59.15/59.55 cnf(1906,plain, % 59.15/59.55 (P2(f28(a1,f31(a32)),a1)), % 59.15/59.55 inference(scs_inference,[],[424,1903,427,423,85,72,73,135])). % 59.15/59.55 cnf(1908,plain, % 59.15/59.55 (P2(a1,a1)), % 59.15/59.55 inference(scs_inference,[],[424,1903,427,423,85,72,73,135,70])). % 59.15/59.55 cnf(1909,plain, % 59.15/59.55 (P2(f28(a1,f31(a32)),f28(a1,f31(a32)))), % 59.15/59.55 inference(scs_inference,[],[424,1903,427,423,85,72,73,135,70,71])). % 59.15/59.55 cnf(1912,plain, % 59.15/59.55 (P2(a1,f28(a1,f31(a32)))), % 59.15/59.55 inference(scs_inference,[],[1909,423,70])). % 59.15/59.55 cnf(2010,plain, % 59.15/59.55 (P8(f30(a1,f31(a32)),a1)), % 59.15/59.55 inference(scs_inference,[],[86,977,101])). % 59.15/59.55 cnf(2011,plain, % 59.15/59.55 (P8(f28(a32,f31(a32)),a1)), % 59.15/59.55 inference(scs_inference,[],[565,2010,72])). % 59.15/59.55 cnf(2098,plain, % 59.15/59.55 (P8(f28(a32,f31(a32)),f28(f31(a32),a1))), % 59.15/59.55 inference(scs_inference,[],[481,2011,1908,1904,70,72,71,73])). % 59.15/59.55 cnf(2102,plain, % 59.15/59.55 (P2(f28(f31(a32),a1),f28(a1,f31(a32)))), % 59.15/59.55 inference(scs_inference,[],[481,1912,70])). % 59.15/59.55 cnf(2110,plain, % 59.15/59.55 (P2(f28(a1,f31(a32)),f28(f31(a32),a1))), % 59.15/59.55 inference(scs_inference,[],[481,789,2098,1906,72,71])). % 59.15/59.55 cnf(2111,plain, % 59.15/59.55 (P8(a1,f28(f31(a32),a1))), % 59.15/59.55 inference(scs_inference,[],[481,789,2098,1904,1906,72,71,73])). % 59.15/59.55 cnf(3787,plain, % 59.15/59.55 (P3(f2(a1))), % 59.15/59.55 inference(scs_inference,[],[85,102])). % 59.15/59.55 cnf(3791,plain, % 59.15/59.55 (E(f30(a1,a1),a1)), % 59.15/59.55 inference(scs_inference,[],[85,102,192,107])). % 59.15/59.55 cnf(3793,plain, % 59.15/59.55 (E(f28(a32,a1),a1)), % 59.15/59.55 inference(scs_inference,[],[85,102,192,107,108])). % 59.15/59.55 cnf(3799,plain, % 59.15/59.55 (E(f28(a1,a1),a1)), % 59.15/59.55 inference(scs_inference,[],[85,320,102,192,107,108,109,110,104])). % 59.15/59.55 cnf(3872,plain, % 59.15/59.55 (~E(a32,a1)), % 59.15/59.55 inference(scs_inference,[],[85,97,320,564,102,192,107,108,109,110,104,105,4,30,33,44,55,60,61,112,113,5,6,7,8,20,21,22,23,28,29,31,32,34,35,36,37,48,49,53,54,56,57,58,59,114,115,17,18,19,38,39,40,41,42,43,45,46,47,50,51,52,62,63,64,9,10,11,12,13,14,15,16,24,25,26,27,2])). % 59.15/59.55 cnf(3877,plain, % 59.15/59.55 (P1(f28(a1,a1))), % 59.15/59.55 inference(scs_inference,[],[85,97,338,320,564,102,192,107,108,109,110,104,105,4,30,33,44,55,60,61,112,113,5,6,7,8,20,21,22,23,28,29,31,32,34,35,36,37,48,49,53,54,56,57,58,59,114,115,17,18,19,38,39,40,41,42,43,45,46,47,50,51,52,62,63,64,9,10,11,12,13,14,15,16,24,25,26,27,2,101,100,130])). % 59.15/59.55 cnf(3883,plain, % 59.15/59.55 (P6(f29(a34,a34))), % 59.15/59.55 inference(scs_inference,[],[85,97,338,320,564,281,102,192,107,108,109,110,104,105,4,30,33,44,55,60,61,112,113,5,6,7,8,20,21,22,23,28,29,31,32,34,35,36,37,48,49,53,54,56,57,58,59,114,115,17,18,19,38,39,40,41,42,43,45,46,47,50,51,52,62,63,64,9,10,11,12,13,14,15,16,24,25,26,27,2,101,100,130,131,132,194])). % 59.15/59.55 cnf(3887,plain, % 59.15/59.55 (~E(a18,a1)), % 59.15/59.55 inference(scs_inference,[],[85,97,338,320,98,564,281,86,205,102,192,107,108,109,110,104,105,4,30,33,44,55,60,61,112,113,5,6,7,8,20,21,22,23,28,29,31,32,34,35,36,37,48,49,53,54,56,57,58,59,114,115,17,18,19,38,39,40,41,42,43,45,46,47,50,51,52,62,63,64,9,10,11,12,13,14,15,16,24,25,26,27,2,101,100,130,131,132,194,103,111])). % 59.15/59.55 cnf(3889,plain, % 59.15/59.55 (P4(a18,a34)), % 59.15/59.55 inference(scs_inference,[],[85,97,338,320,98,564,281,86,205,102,192,107,108,109,110,104,105,4,30,33,44,55,60,61,112,113,5,6,7,8,20,21,22,23,28,29,31,32,34,35,36,37,48,49,53,54,56,57,58,59,114,115,17,18,19,38,39,40,41,42,43,45,46,47,50,51,52,62,63,64,9,10,11,12,13,14,15,16,24,25,26,27,2,101,100,130,131,132,194,103,111,118])). % 59.15/59.55 cnf(3906,plain, % 59.15/59.55 (P1(a4)), % 59.15/59.55 inference(scs_inference,[],[85,97,338,2110,2102,992,320,98,564,481,281,86,205,102,192,107,108,109,110,104,105,4,30,33,44,55,60,61,112,113,5,6,7,8,20,21,22,23,28,29,31,32,34,35,36,37,48,49,53,54,56,57,58,59,114,115,17,18,19,38,39,40,41,42,43,45,46,47,50,51,52,62,63,64,9,10,11,12,13,14,15,16,24,25,26,27,2,101,100,130,131,132,194,103,111,118,116,122,199,137,193,129,71,3,70,119])). % 59.15/59.55 cnf(3914,plain, % 59.15/59.55 (P4(f30(a4,a4),f3(f2(a33),f2(a35)))), % 59.15/59.55 inference(scs_inference,[],[85,97,338,2110,2102,992,206,320,98,1904,564,481,281,86,96,205,102,192,107,108,109,110,104,105,4,30,33,44,55,60,61,112,113,5,6,7,8,20,21,22,23,28,29,31,32,34,35,36,37,48,49,53,54,56,57,58,59,114,115,17,18,19,38,39,40,41,42,43,45,46,47,50,51,52,62,63,64,9,10,11,12,13,14,15,16,24,25,26,27,2,101,100,130,131,132,194,103,111,118,116,122,199,137,193,129,71,3,70,119,139,133,134,147])). % 59.15/59.55 cnf(3930,plain, % 59.15/59.55 (~E(f28(a4,a4),a1)), % 59.15/59.55 inference(scs_inference,[],[85,97,338,2110,2102,992,206,320,98,1904,564,481,281,86,96,205,102,192,107,108,109,110,104,105,4,30,33,44,55,60,61,112,113,5,6,7,8,20,21,22,23,28,29,31,32,34,35,36,37,48,49,53,54,56,57,58,59,114,115,17,18,19,38,39,40,41,42,43,45,46,47,50,51,52,62,63,64,9,10,11,12,13,14,15,16,24,25,26,27,2,101,100,130,131,132,194,103,111,118,116,122,199,137,193,129,71,3,70,119,139,133,134,147,143,150,151,165,161,162,142,121])). % 59.15/59.55 cnf(3965,plain, % 59.15/59.55 (P3(f2(a4))), % 59.15/59.55 inference(scs_inference,[],[3906,108,110,102])). % 59.15/59.55 cnf(3990,plain, % 59.15/59.55 (P6(f2(a4))), % 59.15/59.55 inference(scs_inference,[],[3906,3799,108,110,102,113,104,112,9,105,28,57,34,115,44,61,25,41,114,18,62,11,192])). % 59.15/59.55 cnf(4049,plain, % 59.15/59.55 (P9(f17(f19(a18)),f17(a18))), % 59.15/59.55 inference(scs_inference,[],[3887,3889,3906,3877,3799,108,110,102,113,104,112,9,105,28,57,34,115,44,61,25,41,114,18,62,11,192,52,13,8,56,42,17,10,109,107,64,31,60,55,47,63,39,6,26,40,21,58,30,38,19,15,16,53,27,20,33,32,48,50,43,12,46,36,22,59,54,4,51,5,45,35,37,49,29,7,24,14,23,101,2,137])). % 59.15/59.55 cnf(4051,plain, % 59.15/59.55 (~E(f19(a18),a1)), % 59.15/59.55 inference(scs_inference,[],[3887,3889,3906,3877,3799,108,110,102,113,104,112,9,105,28,57,34,115,44,61,25,41,114,18,62,11,192,52,13,8,56,42,17,10,109,107,64,31,60,55,47,63,39,6,26,40,21,58,30,38,19,15,16,53,27,20,33,32,48,50,43,12,46,36,22,59,54,4,51,5,45,35,37,49,29,7,24,14,23,101,2,137,116])). % 59.15/59.55 cnf(4055,plain, % 59.15/59.55 (P1(f30(a4,a4))), % 59.15/59.55 inference(scs_inference,[],[3887,3889,3906,3877,3799,3787,108,110,102,113,104,112,9,105,28,57,34,115,44,61,25,41,114,18,62,11,192,52,13,8,56,42,17,10,109,107,64,31,60,55,47,63,39,6,26,40,21,58,30,38,19,15,16,53,27,20,33,32,48,50,43,12,46,36,22,59,54,4,51,5,45,35,37,49,29,7,24,14,23,101,2,137,116,131,129])). % 59.15/59.55 cnf(4057,plain, % 59.15/59.55 (P3(f29(f2(a1),f2(a1)))), % 59.15/59.55 inference(scs_inference,[],[3887,3889,3906,3877,3799,3787,108,110,102,113,104,112,9,105,28,57,34,115,44,61,25,41,114,18,62,11,192,52,13,8,56,42,17,10,109,107,64,31,60,55,47,63,39,6,26,40,21,58,30,38,19,15,16,53,27,20,33,32,48,50,43,12,46,36,22,59,54,4,51,5,45,35,37,49,29,7,24,14,23,101,2,137,116,131,129,132])). % 59.15/59.55 cnf(4061,plain, % 59.15/59.55 (P4(f19(a18),a34)), % 59.15/59.55 inference(scs_inference,[],[3887,3889,3906,3877,3799,3787,108,110,102,113,104,112,9,105,28,57,34,115,44,61,25,41,114,18,62,11,192,52,13,8,56,42,17,10,109,107,64,31,60,55,47,63,39,6,26,40,21,58,30,38,19,15,16,53,27,20,33,32,48,50,43,12,46,36,22,59,54,4,51,5,45,35,37,49,29,7,24,14,23,101,2,137,116,131,129,132,130,122])). % 59.15/59.55 cnf(4072,plain, % 59.15/59.55 (P1(a18)), % 59.15/59.55 inference(scs_inference,[],[3887,3889,3906,3877,3883,3799,3787,3930,88,424,428,281,108,110,102,113,104,112,9,105,28,57,34,115,44,61,25,41,114,18,62,11,192,52,13,8,56,42,17,10,109,107,64,31,60,55,47,63,39,6,26,40,21,58,30,38,19,15,16,53,27,20,33,32,48,50,43,12,46,36,22,59,54,4,51,5,45,35,37,49,29,7,24,14,23,101,2,137,116,131,129,132,130,122,193,103,194,199,3,119])). % 59.15/59.55 cnf(4110,plain, % 59.15/59.55 (P8(a36,a35)), % 59.15/59.55 inference(scs_inference,[],[85,3887,3889,3906,3877,3883,3799,3787,3930,2111,89,88,98,87,483,424,428,95,281,108,110,102,113,104,112,9,105,28,57,34,115,44,61,25,41,114,18,62,11,192,52,13,8,56,42,17,10,109,107,64,31,60,55,47,63,39,6,26,40,21,58,30,38,19,15,16,53,27,20,33,32,48,50,43,12,46,36,22,59,54,4,51,5,45,35,37,49,29,7,24,14,23,101,2,137,116,131,129,132,130,122,193,103,194,199,3,119,151,134,139,147,162,150,156,161,165,133,155,142,195,144,138,171,100,117,128])). % 59.15/59.55 cnf(4112,plain, % 59.15/59.55 (P1(a36)), % 59.15/59.55 inference(scs_inference,[],[85,3887,3889,3906,3877,3883,3799,3787,3930,2111,89,88,98,87,483,424,428,95,281,108,110,102,113,104,112,9,105,28,57,34,115,44,61,25,41,114,18,62,11,192,52,13,8,56,42,17,10,109,107,64,31,60,55,47,63,39,6,26,40,21,58,30,38,19,15,16,53,27,20,33,32,48,50,43,12,46,36,22,59,54,4,51,5,45,35,37,49,29,7,24,14,23,101,2,137,116,131,129,132,130,122,193,103,194,199,3,119,151,134,139,147,162,150,156,161,165,133,155,142,195,144,138,171,100,117,128,120])). % 59.15/59.55 cnf(4119,plain, % 59.15/59.55 (~E(f28(a32,a32),a1)), % 59.15/59.55 inference(scs_inference,[],[85,3872,3887,3889,3906,3877,3883,3799,3787,3930,3914,2111,89,88,94,98,87,483,424,428,95,281,86,108,110,102,113,104,112,9,105,28,57,34,115,44,61,25,41,114,18,62,11,192,52,13,8,56,42,17,10,109,107,64,31,60,55,47,63,39,6,26,40,21,58,30,38,19,15,16,53,27,20,33,32,48,50,43,12,46,36,22,59,54,4,51,5,45,35,37,49,29,7,24,14,23,101,2,137,116,131,129,132,130,122,193,103,194,199,3,119,151,134,139,147,162,150,156,161,165,133,155,142,195,144,138,171,100,117,128,120,67,167,143,121])). % 59.15/59.55 cnf(4141,plain, % 59.15/59.55 (P6(f2(a18))), % 59.15/59.55 inference(scs_inference,[],[4072,108,113,112,115,110,114,107,192])). % 59.15/59.55 cnf(4145,plain, % 59.15/59.55 (P3(f2(a18))), % 59.15/59.55 inference(scs_inference,[],[4072,108,113,112,115,110,114,107,192,105,102])). % 59.15/59.55 cnf(4217,plain, % 59.15/59.55 (P3(f3(f2(a4),f2(a4)))), % 59.15/59.55 inference(scs_inference,[],[4072,3791,3965,4119,4057,108,113,112,115,110,114,107,192,105,102,104,25,42,9,41,109,44,61,26,57,62,10,6,34,20,19,4,13,28,38,52,33,22,24,18,5,36,8,40,63,53,35,11,55,51,30,43,27,17,16,56,31,54,15,58,59,64,39,60,47,21,14,32,12,50,49,29,48,45,23,46,37,7,101,100,2,131])). % 59.15/59.55 cnf(4403,plain, % 59.15/59.55 ($false), % 59.15/59.55 inference(scs_inference,[],[85,4110,3793,4055,3990,4141,4145,4051,4061,4049,4217,4112,89,88,98,87,3906,424,429,281,108,115,114,113,107,112,192,110,102,25,105,104,109,41,44,9,42,19,62,38,26,40,13,6,51,16,8,14,61,10,55,60,56,28,39,34,57,12,27,63,4,58,5,46,11,24,20,32,17,21,43,33,49,30,47,52,35,22,36,53,18,31,59,15,54,64,48,101,45,50,37,29,7,23,100,2,116,131,129,193,122,103,132,130,199,194,3,119,134,151,162,147,161,150,133,143,144]), % 59.15/59.55 ['proof']). % 59.15/59.55 % SZS output end Proof % 59.15/59.55 % Total time :58.530000s %------------------------------------------------------------------------------