%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : RNG101+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 : n002.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:04 EDT 2024 % Result : Theorem 121.53s 122.49s % Output : CNFRefutation 121.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : RNG101+1 : TPTP v8.2.0. Released v4.0.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n002.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Tue Jun 18 13:26:09 EDT 2024 % 0.12/0.34 % CPUTime : % 0.50/0.57 start to proof:theBenchmark % 121.50/122.47 %------------------------------------------- % 121.50/122.47 % File :CSE---1.7 % 121.50/122.47 % Problem :theBenchmark % 121.50/122.47 % Transform :cnf % 121.50/122.47 % Format :tptp:raw % 121.50/122.47 % Command :java -jar mcs_scs.jar %d %s % 121.50/122.47 % 121.50/122.47 % Result :Theorem 120.860000s % 121.50/122.47 % Output :CNFRefutation 120.860000s % 121.50/122.47 %------------------------------------------- % 121.50/122.48 %------------------------------------------------------------------------------ % 121.50/122.48 % File : RNG101+1 : TPTP v8.2.0. Released v4.0.0. % 121.50/122.48 % Domain : Ring Theory % 121.50/122.48 % Problem : Chinese remainder theorem in a ring 06_01, 00 expansion % 121.50/122.48 % Version : Especial. % 121.50/122.48 % English : % 121.50/122.48 % 121.50/122.48 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 121.50/122.48 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 121.50/122.48 % Source : [Pas08] % 121.50/122.48 % Names : chines_06_01.00 [Pas08] % 121.50/122.48 % 121.50/122.48 % Status : Theorem % 121.50/122.48 % Rating : 0.31 v8.2.0, 0.33 v8.1.0, 0.31 v7.4.0, 0.30 v7.3.0, 0.38 v7.1.0, 0.30 v7.0.0, 0.33 v6.4.0, 0.35 v6.3.0, 0.38 v6.2.0, 0.48 v6.1.0, 0.53 v6.0.0, 0.43 v5.5.0, 0.52 v5.4.0, 0.54 v5.3.0, 0.59 v5.2.0, 0.45 v5.1.0, 0.52 v5.0.0, 0.67 v4.1.0, 0.70 v4.0.1, 0.87 v4.0.0 % 121.50/122.48 % Syntax : Number of formulae : 40 ( 4 unt; 9 def) % 121.50/122.48 % Number of atoms : 156 ( 32 equ) % 121.50/122.48 % Maximal formula atoms : 9 ( 3 avg) % 121.50/122.48 % Number of connectives : 120 ( 4 ~; 1 |; 56 &) % 121.50/122.48 % ( 12 <=>; 47 =>; 0 <=; 0 <~>) % 121.50/122.48 % Maximal formula depth : 13 ( 6 avg) % 121.50/122.48 % Maximal term depth : 3 ( 1 avg) % 121.50/122.48 % Number of predicates : 13 ( 11 usr; 1 prp; 0-3 aty) % 121.50/122.48 % Number of functors : 13 ( 13 usr; 6 con; 0-2 aty) % 121.50/122.48 % Number of variables : 84 ( 76 !; 8 ?) % 121.50/122.48 % SPC : FOF_THM_RFO_SEQ % 121.50/122.48 % 121.50/122.48 % Comments : Problem generated by the SAD system [VLP07] % 121.50/122.48 %------------------------------------------------------------------------------ % 121.50/122.48 fof(mElmSort,axiom, % 121.50/122.48 ! [W0] : % 121.50/122.48 ( aElement0(W0) % 121.50/122.48 => $true ) ). % 121.50/122.48 % 121.50/122.48 fof(mSortsC,axiom, % 121.50/122.48 aElement0(sz00) ). % 121.50/122.48 % 121.50/122.48 fof(mSortsC_01,axiom, % 121.50/122.48 aElement0(sz10) ). % 121.50/122.48 % 121.50/122.48 fof(mSortsU,axiom, % 121.50/122.48 ! [W0] : % 121.50/122.48 ( aElement0(W0) % 121.50/122.48 => aElement0(smndt0(W0)) ) ). % 121.50/122.48 % 121.50/122.48 fof(mSortsB,axiom, % 121.50/122.48 ! [W0,W1] : % 121.50/122.48 ( ( aElement0(W0) % 121.50/122.48 & aElement0(W1) ) % 121.50/122.48 => aElement0(sdtpldt0(W0,W1)) ) ). % 121.50/122.48 % 121.50/122.48 fof(mSortsB_02,axiom, % 121.50/122.48 ! [W0,W1] : % 121.50/122.48 ( ( aElement0(W0) % 121.50/122.48 & aElement0(W1) ) % 121.50/122.48 => aElement0(sdtasdt0(W0,W1)) ) ). % 121.50/122.48 % 121.50/122.48 fof(mAddComm,axiom, % 121.50/122.48 ! [W0,W1] : % 121.53/122.48 ( ( aElement0(W0) % 121.53/122.48 & aElement0(W1) ) % 121.53/122.48 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 121.53/122.48 % 121.53/122.48 fof(mAddAsso,axiom, % 121.53/122.48 ! [W0,W1,W2] : % 121.53/122.48 ( ( aElement0(W0) % 121.53/122.48 & aElement0(W1) % 121.53/122.48 & aElement0(W2) ) % 121.53/122.48 => sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) ). % 121.53/122.48 % 121.53/122.48 fof(mAddZero,axiom, % 121.53/122.48 ! [W0] : % 121.53/122.48 ( aElement0(W0) % 121.53/122.48 => ( sdtpldt0(W0,sz00) = W0 % 121.53/122.48 & W0 = sdtpldt0(sz00,W0) ) ) ). % 121.53/122.48 % 121.53/122.48 fof(mAddInvr,axiom, % 121.53/122.48 ! [W0] : % 121.53/122.48 ( aElement0(W0) % 121.53/122.48 => ( sdtpldt0(W0,smndt0(W0)) = sz00 % 121.53/122.48 & sz00 = sdtpldt0(smndt0(W0),W0) ) ) ). % 121.53/122.48 % 121.53/122.48 fof(mMulComm,axiom, % 121.53/122.48 ! [W0,W1] : % 121.53/122.48 ( ( aElement0(W0) % 121.53/122.48 & aElement0(W1) ) % 121.53/122.48 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 121.53/122.48 % 121.53/122.48 fof(mMulAsso,axiom, % 121.53/122.48 ! [W0,W1,W2] : % 121.53/122.48 ( ( aElement0(W0) % 121.53/122.48 & aElement0(W1) % 121.53/122.48 & aElement0(W2) ) % 121.53/122.48 => sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) ). % 121.53/122.48 % 121.53/122.48 fof(mMulUnit,axiom, % 121.53/122.48 ! [W0] : % 121.53/122.48 ( aElement0(W0) % 121.53/122.48 => ( sdtasdt0(W0,sz10) = W0 % 121.53/122.48 & W0 = sdtasdt0(sz10,W0) ) ) ). % 121.53/122.48 % 121.53/122.48 fof(mAMDistr,axiom, % 121.53/122.48 ! [W0,W1,W2] : % 121.53/122.48 ( ( aElement0(W0) % 121.53/122.48 & aElement0(W1) % 121.53/122.48 & aElement0(W2) ) % 121.53/122.48 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 121.53/122.48 & sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ). % 121.53/122.48 % 121.53/122.48 fof(mMulMnOne,axiom, % 121.53/122.48 ! [W0] : % 121.53/122.48 ( aElement0(W0) % 121.53/122.48 => ( sdtasdt0(smndt0(sz10),W0) = smndt0(W0) % 121.53/122.48 & smndt0(W0) = sdtasdt0(W0,smndt0(sz10)) ) ) ). % 121.53/122.48 % 121.53/122.48 fof(mMulZero,axiom, % 121.53/122.48 ! [W0] : % 121.53/122.48 ( aElement0(W0) % 121.53/122.48 => ( sdtasdt0(W0,sz00) = sz00 % 121.53/122.48 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 121.53/122.48 % 121.53/122.48 fof(mCancel,axiom, % 121.53/122.48 ! [W0,W1] : % 121.53/122.48 ( ( aElement0(W0) % 121.53/122.48 & aElement0(W1) ) % 121.53/122.48 => ( sdtasdt0(W0,W1) = sz00 % 121.53/122.48 => ( W0 = sz00 % 121.53/122.48 | W1 = sz00 ) ) ) ). % 121.53/122.48 % 121.53/122.48 fof(mUnNeZr,axiom, % 121.53/122.48 sz10 != sz00 ). % 121.53/122.48 % 121.53/122.48 fof(mSetSort,axiom, % 121.53/122.48 ! [W0] : % 121.53/122.48 ( aSet0(W0) % 121.53/122.48 => $true ) ). % 121.53/122.48 % 121.53/122.48 fof(mEOfElem,axiom, % 121.53/122.48 ! [W0] : % 121.53/122.48 ( aSet0(W0) % 121.53/122.48 => ! [W1] : % 121.53/122.48 ( aElementOf0(W1,W0) % 121.53/122.48 => aElement0(W1) ) ) ). % 121.53/122.48 % 121.53/122.48 fof(mSetEq,axiom, % 121.53/122.48 ! [W0,W1] : % 121.53/122.48 ( ( aSet0(W0) % 121.53/122.48 & aSet0(W1) ) % 121.53/122.48 => ( ( ! [W2] : % 121.53/122.48 ( aElementOf0(W2,W0) % 121.53/122.48 => aElementOf0(W2,W1) ) % 121.53/122.48 & ! [W2] : % 121.53/122.48 ( aElementOf0(W2,W1) % 121.53/122.48 => aElementOf0(W2,W0) ) ) % 121.53/122.48 => W0 = W1 ) ) ). % 121.53/122.48 % 121.53/122.48 fof(mDefSSum,definition, % 121.53/122.48 ! [W0,W1] : % 121.53/122.48 ( ( aSet0(W0) % 121.53/122.48 & aSet0(W1) ) % 121.53/122.48 => ! [W2] : % 121.53/122.48 ( W2 = sdtpldt1(W0,W1) % 121.53/122.48 <=> ( aSet0(W2) % 121.53/122.48 & ! [W3] : % 121.53/122.48 ( aElementOf0(W3,W2) % 121.53/122.48 <=> ? [W4,W5] : % 121.53/122.48 ( aElementOf0(W4,W0) % 121.53/122.48 & aElementOf0(W5,W1) % 121.53/122.48 & sdtpldt0(W4,W5) = W3 ) ) ) ) ) ). % 121.53/122.48 % 121.53/122.48 fof(mDefSInt,definition, % 121.53/122.48 ! [W0,W1] : % 121.53/122.48 ( ( aSet0(W0) % 121.53/122.48 & aSet0(W1) ) % 121.53/122.48 => ! [W2] : % 121.53/122.48 ( W2 = sdtasasdt0(W0,W1) % 121.53/122.48 <=> ( aSet0(W2) % 121.53/122.48 & ! [W3] : % 121.53/122.48 ( aElementOf0(W3,W2) % 121.53/122.48 <=> ( aElementOf0(W3,W0) % 121.53/122.48 & aElementOf0(W3,W1) ) ) ) ) ) ). % 121.53/122.49 % 121.53/122.49 fof(mDefIdeal,definition, % 121.53/122.49 ! [W0] : % 121.53/122.49 ( aIdeal0(W0) % 121.53/122.49 <=> ( aSet0(W0) % 121.53/122.49 & ! [W1] : % 121.53/122.49 ( aElementOf0(W1,W0) % 121.53/122.49 => ( ! [W2] : % 121.53/122.49 ( aElementOf0(W2,W0) % 121.53/122.49 => aElementOf0(sdtpldt0(W1,W2),W0) ) % 121.53/122.49 & ! [W2] : % 121.53/122.49 ( aElement0(W2) % 121.53/122.49 => aElementOf0(sdtasdt0(W2,W1),W0) ) ) ) ) ) ). % 121.53/122.49 % 121.53/122.49 fof(mIdeSum,axiom, % 121.53/122.49 ! [W0,W1] : % 121.53/122.49 ( ( aIdeal0(W0) % 121.53/122.49 & aIdeal0(W1) ) % 121.53/122.49 => aIdeal0(sdtpldt1(W0,W1)) ) ). % 121.53/122.49 % 121.53/122.49 fof(mIdeInt,axiom, % 121.53/122.49 ! [W0,W1] : % 121.53/122.49 ( ( aIdeal0(W0) % 121.53/122.49 & aIdeal0(W1) ) % 121.53/122.49 => aIdeal0(sdtasasdt0(W0,W1)) ) ). % 121.53/122.49 % 121.53/122.49 fof(mDefMod,definition, % 121.53/122.49 ! [W0,W1,W2] : % 121.53/122.49 ( ( aElement0(W0) % 121.53/122.49 & aElement0(W1) % 121.53/122.49 & aIdeal0(W2) ) % 121.53/122.49 => ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 121.53/122.49 <=> aElementOf0(sdtpldt0(W0,smndt0(W1)),W2) ) ) ). % 121.53/122.49 % 121.53/122.49 fof(mChineseRemainder,axiom, % 121.53/122.49 ! [W0,W1] : % 121.53/122.49 ( ( aIdeal0(W0) % 121.53/122.49 & aIdeal0(W1) ) % 121.53/122.49 => ( ! [W2] : % 121.53/122.49 ( aElement0(W2) % 121.53/122.49 => aElementOf0(W2,sdtpldt1(W0,W1)) ) % 121.53/122.49 => ! [W2,W3] : % 121.53/122.49 ( ( aElement0(W2) % 121.53/122.49 & aElement0(W3) ) % 121.53/122.49 => ? [W4] : % 121.53/122.49 ( aElement0(W4) % 121.53/122.49 & sdteqdtlpzmzozddtrp0(W4,W2,W0) % 121.53/122.49 & sdteqdtlpzmzozddtrp0(W4,W3,W1) ) ) ) ) ). % 121.53/122.49 % 121.53/122.49 fof(mNatSort,axiom, % 121.53/122.49 ! [W0] : % 121.53/122.49 ( aNaturalNumber0(W0) % 121.53/122.49 => $true ) ). % 121.53/122.49 % 121.53/122.49 fof(mEucSort,axiom, % 121.53/122.49 ! [W0] : % 121.53/122.49 ( ( aElement0(W0) % 121.53/122.49 & W0 != sz00 ) % 121.53/122.49 => aNaturalNumber0(sbrdtbr0(W0)) ) ). % 121.53/122.49 % 121.53/122.49 fof(mNatLess,axiom, % 121.53/122.49 ! [W0,W1] : % 121.53/122.49 ( ( aNaturalNumber0(W0) % 121.53/122.49 & aNaturalNumber0(W1) ) % 121.53/122.49 => ( iLess0(W0,W1) % 121.53/122.49 => $true ) ) ). % 121.53/122.49 % 121.53/122.49 fof(mDivision,axiom, % 121.53/122.49 ! [W0,W1] : % 121.53/122.49 ( ( aElement0(W0) % 121.53/122.49 & aElement0(W1) % 121.53/122.49 & W1 != sz00 ) % 121.53/122.49 => ? [W2,W3] : % 121.53/122.49 ( aElement0(W2) % 121.53/122.49 & aElement0(W3) % 121.53/122.49 & W0 = sdtpldt0(sdtasdt0(W2,W1),W3) % 121.53/122.49 & ( W3 != sz00 % 121.53/122.49 => iLess0(sbrdtbr0(W3),sbrdtbr0(W1)) ) ) ) ). % 121.53/122.49 % 121.53/122.49 fof(mDefDiv,definition, % 121.53/122.49 ! [W0,W1] : % 121.53/122.49 ( ( aElement0(W0) % 121.53/122.49 & aElement0(W1) ) % 121.53/122.49 => ( doDivides0(W0,W1) % 121.53/122.49 <=> ? [W2] : % 121.53/122.49 ( aElement0(W2) % 121.53/122.49 & sdtasdt0(W0,W2) = W1 ) ) ) ). % 121.53/122.49 % 121.53/122.49 fof(mDefDvs,definition, % 121.53/122.49 ! [W0] : % 121.53/122.49 ( aElement0(W0) % 121.53/122.49 => ! [W1] : % 121.53/122.49 ( aDivisorOf0(W1,W0) % 121.53/122.49 <=> ( aElement0(W1) % 121.53/122.49 & doDivides0(W1,W0) ) ) ) ). % 121.53/122.49 % 121.53/122.49 fof(mDefGCD,definition, % 121.53/122.49 ! [W0,W1] : % 121.53/122.49 ( ( aElement0(W0) % 121.53/122.49 & aElement0(W1) ) % 121.53/122.49 => ! [W2] : % 121.53/122.49 ( aGcdOfAnd0(W2,W0,W1) % 121.53/122.49 <=> ( aDivisorOf0(W2,W0) % 121.53/122.49 & aDivisorOf0(W2,W1) % 121.53/122.49 & ! [W3] : % 121.53/122.49 ( ( aDivisorOf0(W3,W0) % 121.53/122.49 & aDivisorOf0(W3,W1) ) % 121.53/122.49 => doDivides0(W3,W2) ) ) ) ) ). % 121.53/122.49 % 121.53/122.49 fof(mDefRel,definition, % 121.53/122.49 ! [W0,W1] : % 121.53/122.49 ( ( aElement0(W0) % 121.53/122.49 & aElement0(W1) ) % 121.53/122.49 => ( misRelativelyPrime0(W0,W1) % 121.53/122.49 <=> aGcdOfAnd0(sz10,W0,W1) ) ) ). % 121.53/122.49 % 121.53/122.49 fof(mDefPrIdeal,definition, % 121.53/122.49 ! [W0] : % 121.53/122.49 ( aElement0(W0) % 121.53/122.49 => ! [W1] : % 121.53/122.49 ( W1 = slsdtgt0(W0) % 121.53/122.49 <=> ( aSet0(W1) % 121.53/122.49 & ! [W2] : % 121.53/122.49 ( aElementOf0(W2,W1) % 121.53/122.49 <=> ? [W3] : % 121.53/122.49 ( aElement0(W3) % 121.53/122.49 & sdtasdt0(W0,W3) = W2 ) ) ) ) ) ). % 121.53/122.49 % 121.53/122.49 fof(m__1905,hypothesis, % 121.53/122.49 aElement0(xc) ). % 121.53/122.49 % 121.53/122.49 fof(m__1933,hypothesis, % 121.53/122.49 ( aElementOf0(xx,slsdtgt0(xc)) % 121.53/122.49 & aElementOf0(xy,slsdtgt0(xc)) % 121.53/122.49 & aElement0(xz) ) ). % 121.53/122.49 % 121.53/122.49 fof(m__,conjecture, % 121.53/122.49 ? [W0] : % 121.53/122.49 ( aElement0(W0) % 121.53/122.49 & sdtasdt0(xc,W0) = xx ) ). % 121.53/122.49 % 121.53/122.49 %------------------------------------------------------------------------------ % 121.53/122.49 %------------------------------------------- % 121.53/122.49 % Proof found % 121.53/122.49 % SZS status Theorem for theBenchmark % 121.53/122.49 % SZS output start Proof % 121.53/122.49 %ClaNum:176(EqnAxiom:83) % 121.53/122.49 %VarNum:701(SingletonVarNum:213) % 121.53/122.49 %MaxLitNum:8 % 121.53/122.49 %MaxfuncDepth:2 % 121.53/122.49 %SharedTerms:15 % 121.53/122.49 %goalClause: 101 % 121.53/122.49 [84]P1(a1) % 121.53/122.49 [85]P1(a29) % 121.53/122.49 [86]P1(a30) % 121.53/122.49 [87]P1(a31) % 121.53/122.49 [90]~E(a1,a29) % 121.53/122.49 [88]P3(a32,f2(a30)) % 121.53/122.49 [89]P3(a33,f2(a30)) % 121.53/122.49 [91]~P5(x911)+P4(x911) % 121.53/122.49 [92]~P1(x921)+P1(f28(x921)) % 121.53/122.49 [94]~P1(x941)+E(f24(a1,x941),a1) % 121.53/122.49 [95]~P1(x951)+E(f24(x951,a1),a1) % 121.53/122.49 [97]~P1(x971)+E(f26(a1,x971),x971) % 121.53/122.49 [98]~P1(x981)+E(f24(a29,x981),x981) % 121.53/122.49 [99]~P1(x991)+E(f26(x991,a1),x991) % 121.53/122.49 [100]~P1(x1001)+E(f24(x1001,a29),x1001) % 121.53/122.49 [101]~P1(x1011)+~E(f24(a30,x1011),a32) % 121.53/122.49 [102]~P1(x1021)+E(f26(f28(x1021),x1021),a1) % 121.53/122.49 [103]~P1(x1031)+E(f26(x1031,f28(x1031)),a1) % 121.53/122.49 [104]~P1(x1041)+E(f24(x1041,f28(a29)),f28(x1041)) % 121.53/122.49 [105]~P1(x1051)+E(f24(f28(a29),x1051),f28(x1051)) % 121.53/122.49 [93]~P1(x931)+E(x931,a1)+P7(f3(x931)) % 121.53/122.49 [106]~P4(x1061)+P5(x1061)+P3(f4(x1061),x1061) % 121.53/122.49 [107]~P3(x1071,x1072)+P1(x1071)+~P4(x1072) % 121.53/122.49 [108]~P2(x1081,x1082)+P1(x1081)+~P1(x1082) % 121.53/122.49 [115]~P1(x1152)+~P2(x1151,x1152)+P8(x1151,x1152) % 121.53/122.49 [96]~P1(x962)+P4(x961)+~E(x961,f2(x962)) % 121.53/122.49 [110]~P1(x1102)+~P1(x1101)+E(f26(x1101,x1102),f26(x1102,x1101)) % 121.53/122.49 [111]~P1(x1112)+~P1(x1111)+E(f24(x1111,x1112),f24(x1112,x1111)) % 121.53/122.49 [116]~P1(x1162)+~P1(x1161)+P1(f26(x1161,x1162)) % 121.53/122.49 [117]~P1(x1172)+~P1(x1171)+P1(f24(x1171,x1172)) % 121.53/122.49 [118]~P5(x1182)+~P5(x1181)+P5(f27(x1181,x1182)) % 121.53/122.49 [119]~P5(x1192)+~P5(x1191)+P5(f25(x1191,x1192)) % 121.53/122.49 [114]~P4(x1141)+P5(x1141)+P3(f6(x1141),x1141)+P1(f5(x1141)) % 121.53/122.49 [145]~P4(x1451)+P5(x1451)+P1(f5(x1451))+~P3(f26(f4(x1451),f6(x1451)),x1451) % 121.53/122.49 [148]~P4(x1481)+P5(x1481)+P3(f6(x1481),x1481)+~P3(f24(f5(x1481),f4(x1481)),x1481) % 121.53/122.49 [157]~P4(x1571)+P5(x1571)+~P3(f26(f4(x1571),f6(x1571)),x1571)+~P3(f24(f5(x1571),f4(x1571)),x1571) % 121.53/122.49 [122]~P1(x1222)+~P1(x1221)+~P8(x1221,x1222)+P2(x1221,x1222) % 121.53/122.49 [130]~P1(x1302)+~P1(x1301)+~P9(x1301,x1302)+P6(a29,x1301,x1302) % 121.53/122.49 [138]~P1(x1382)+~P1(x1381)+P9(x1381,x1382)+~P6(a29,x1381,x1382) % 121.53/122.49 [120]~P1(x1201)+~P1(x1202)+E(x1201,a1)+P1(f7(x1202,x1201)) % 121.53/122.49 [121]~P1(x1211)+~P1(x1212)+E(x1211,a1)+P1(f10(x1212,x1211)) % 121.53/122.49 [125]~P1(x1252)+~P1(x1251)+~P8(x1251,x1252)+P1(f11(x1251,x1252)) % 121.53/122.49 [129]~P1(x1292)+~P1(x1291)+~P8(x1291,x1292)+E(f24(x1291,f11(x1291,x1292)),x1292) % 121.53/122.49 [150]~P1(x1501)+~P1(x1502)+E(x1501,a1)+E(f26(f24(f7(x1502,x1501),x1501),f10(x1502,x1501)),x1502) % 121.53/122.49 [140]~P1(x1402)+~P6(x1401,x1403,x1402)+P2(x1401,x1402)+~P1(x1403) % 121.53/122.49 [141]~P1(x1412)+~P6(x1411,x1412,x1413)+P2(x1411,x1412)+~P1(x1413) % 121.53/122.49 [112]~P4(x1123)+~P4(x1122)+P4(x1121)+~E(x1121,f27(x1122,x1123)) % 121.53/122.49 [113]~P4(x1133)+~P4(x1132)+P4(x1131)+~E(x1131,f25(x1132,x1133)) % 121.53/122.49 [128]~P1(x1281)+~P5(x1283)+~P3(x1282,x1283)+P3(f24(x1281,x1282),x1283) % 121.53/122.49 [132]~P5(x1323)+~P3(x1321,x1323)+~P3(x1322,x1323)+P3(f26(x1321,x1322),x1323) % 121.53/122.49 [152]~P1(x1521)+~P3(x1523,x1522)+~E(x1522,f2(x1521))+P1(f14(x1521,x1522,x1523)) % 121.53/122.49 [135]~P1(x1353)+~P1(x1352)+~P1(x1351)+E(f26(f26(x1351,x1352),x1353),f26(x1351,f26(x1352,x1353))) % 121.53/122.49 [136]~P1(x1363)+~P1(x1362)+~P1(x1361)+E(f24(f24(x1361,x1362),x1363),f24(x1361,f24(x1362,x1363))) % 121.53/122.49 [146]~P1(x1463)+~P1(x1462)+~P1(x1461)+E(f26(f24(x1461,x1462),f24(x1461,x1463)),f24(x1461,f26(x1462,x1463))) % 121.53/122.49 [147]~P1(x1472)+~P1(x1473)+~P1(x1471)+E(f26(f24(x1471,x1472),f24(x1473,x1472)),f24(f26(x1471,x1473),x1472)) % 121.53/122.49 [154]~P1(x1541)+~P3(x1543,x1542)+~E(x1542,f2(x1541))+E(f24(x1541,f14(x1541,x1542,x1543)),x1543) % 121.53/122.49 [109]~P1(x1091)+~P1(x1092)+E(x1091,a1)+E(x1092,a1)+~E(f24(x1092,x1091),a1) % 121.53/122.49 [131]~P1(x1312)+~P4(x1311)+P3(f13(x1312,x1311),x1311)+E(x1311,f2(x1312))+P1(f12(x1312,x1311)) % 121.53/122.49 [133]~P4(x1332)+~P4(x1331)+E(x1331,x1332)+P3(f16(x1331,x1332),x1331)+P3(f17(x1331,x1332),x1332) % 121.53/122.49 [142]~P4(x1422)+~P4(x1421)+E(x1421,x1422)+P3(f16(x1421,x1422),x1421)+~P3(f17(x1421,x1422),x1421) % 121.53/122.49 [143]~P4(x1432)+~P4(x1431)+E(x1431,x1432)+P3(f17(x1431,x1432),x1432)+~P3(f16(x1431,x1432),x1432) % 121.53/122.49 [151]~P4(x1512)+~P4(x1511)+E(x1511,x1512)+~P3(f16(x1511,x1512),x1512)+~P3(f17(x1511,x1512),x1511) % 121.53/122.49 [137]~P1(x1371)+~P1(x1372)+E(x1371,a1)+P10(f3(f10(x1372,x1371)),f3(x1371))+E(f10(x1372,x1371),a1) % 121.53/122.49 [139]~P1(x1392)+~P4(x1391)+P3(f13(x1392,x1391),x1391)+E(x1391,f2(x1392))+E(f24(x1392,f12(x1392,x1391)),f13(x1392,x1391)) % 121.53/122.49 [123]~P1(x1232)+~P1(x1231)+~P1(x1233)+P8(x1231,x1232)+~E(f24(x1231,x1233),x1232) % 121.53/122.49 [153]~P1(x1532)+~P1(x1531)+~P5(x1533)+P11(x1531,x1532,x1533)+~P3(f26(x1531,f28(x1532)),x1533) % 121.53/122.49 [155]~P1(x1552)+~P1(x1551)+~P5(x1553)+~P11(x1551,x1552,x1553)+P3(f26(x1551,f28(x1552)),x1553) % 121.53/122.49 [124]~P1(x1243)+~P1(x1244)+P3(x1241,x1242)+~E(f24(x1243,x1244),x1241)+~E(x1242,f2(x1243)) % 121.53/122.49 [126]~P4(x1264)+~P4(x1262)+~P3(x1261,x1263)+P3(x1261,x1262)+~E(x1263,f25(x1264,x1262)) % 121.53/122.49 [127]~P4(x1274)+~P4(x1272)+~P3(x1271,x1273)+P3(x1271,x1272)+~E(x1273,f25(x1272,x1274)) % 121.53/122.49 [168]~P4(x1682)+~P4(x1681)+~P3(x1684,x1683)+~E(x1683,f27(x1681,x1682))+P3(f19(x1681,x1682,x1683,x1684),x1681) % 121.53/122.49 [169]~P4(x1692)+~P4(x1691)+~P3(x1694,x1693)+~E(x1693,f27(x1691,x1692))+P3(f20(x1691,x1692,x1693,x1694),x1692) % 121.53/122.49 [176]~P4(x1762)+~P4(x1761)+~P3(x1764,x1763)+~E(x1763,f27(x1761,x1762))+E(f26(f19(x1761,x1762,x1763,x1764),f20(x1761,x1762,x1763,x1764)),x1764) % 121.53/122.49 [149]~P1(x1493)+~P1(x1492)+~P4(x1491)+~P3(f13(x1492,x1491),x1491)+~E(f13(x1492,x1491),f24(x1492,x1493))+E(x1491,f2(x1492)) % 121.53/122.49 [158]~P1(x1583)+~P1(x1582)+~P2(x1581,x1583)+~P2(x1581,x1582)+P6(x1581,x1582,x1583)+P2(f15(x1582,x1583,x1581),x1583) % 121.53/122.49 [159]~P1(x1593)+~P1(x1592)+~P2(x1591,x1593)+~P2(x1591,x1592)+P6(x1591,x1592,x1593)+P2(f15(x1592,x1593,x1591),x1592) % 121.53/122.49 [160]~P4(x1601)+~P4(x1603)+~P4(x1602)+P3(f18(x1602,x1603,x1601),x1601)+P3(f21(x1602,x1603,x1601),x1602)+E(x1601,f27(x1602,x1603)) % 121.53/122.49 [161]~P4(x1611)+~P4(x1613)+~P4(x1612)+P3(f18(x1612,x1613,x1611),x1611)+P3(f22(x1612,x1613,x1611),x1613)+E(x1611,f27(x1612,x1613)) % 121.53/122.49 [162]~P4(x1621)+~P4(x1623)+~P4(x1622)+P3(f23(x1622,x1623,x1621),x1621)+P3(f23(x1622,x1623,x1621),x1623)+E(x1621,f25(x1622,x1623)) % 121.53/122.49 [163]~P4(x1631)+~P4(x1633)+~P4(x1632)+P3(f23(x1632,x1633,x1631),x1631)+P3(f23(x1632,x1633,x1631),x1632)+E(x1631,f25(x1632,x1633)) % 121.53/122.49 [164]~P1(x1643)+~P1(x1642)+~P2(x1641,x1643)+~P2(x1641,x1642)+P6(x1641,x1642,x1643)+~P8(f15(x1642,x1643,x1641),x1641) % 121.53/122.49 [166]~P4(x1661)+~P4(x1663)+~P4(x1662)+P3(f18(x1662,x1663,x1661),x1661)+E(x1661,f27(x1662,x1663))+E(f26(f21(x1662,x1663,x1661),f22(x1662,x1663,x1661)),f18(x1662,x1663,x1661)) % 121.53/122.49 [156]~P2(x1561,x1563)+~P2(x1561,x1564)+~P6(x1562,x1564,x1563)+P8(x1561,x1562)+~P1(x1563)+~P1(x1564) % 121.53/122.49 [134]~P4(x1344)+~P4(x1343)+~P3(x1341,x1344)+~P3(x1341,x1343)+P3(x1341,x1342)+~E(x1342,f25(x1343,x1344)) % 121.53/122.49 [167]~P1(x1674)+~P1(x1673)+~P5(x1672)+~P5(x1671)+P1(f8(x1671,x1672))+P1(f9(x1671,x1672,x1673,x1674)) % 121.53/122.49 [170]~P1(x1704)+~P1(x1703)+~P5(x1702)+~P5(x1701)+P11(f9(x1701,x1702,x1703,x1704),x1704,x1702)+P1(f8(x1701,x1702)) % 121.53/122.49 [171]~P1(x1714)+~P1(x1713)+~P5(x1712)+~P5(x1711)+P11(f9(x1711,x1712,x1713,x1714),x1713,x1711)+P1(f8(x1711,x1712)) % 121.53/122.49 [173]~P1(x1734)+~P1(x1733)+~P5(x1732)+~P5(x1731)+~P3(f8(x1731,x1732),f27(x1731,x1732))+P1(f9(x1731,x1732,x1733,x1734)) % 121.53/122.49 [174]~P1(x1744)+~P1(x1743)+~P5(x1742)+~P5(x1741)+P11(f9(x1741,x1742,x1743,x1744),x1744,x1742)+~P3(f8(x1741,x1742),f27(x1741,x1742)) % 121.53/122.49 [175]~P1(x1754)+~P1(x1753)+~P5(x1752)+~P5(x1751)+P11(f9(x1751,x1752,x1753,x1754),x1753,x1751)+~P3(f8(x1751,x1752),f27(x1751,x1752)) % 121.53/122.49 [172]~P4(x1721)+~P4(x1723)+~P4(x1722)+~P3(f23(x1722,x1723,x1721),x1721)+~P3(f23(x1722,x1723,x1721),x1723)+~P3(f23(x1722,x1723,x1721),x1722)+E(x1721,f25(x1722,x1723)) % 121.53/122.49 [144]~P4(x1444)+~P4(x1443)+~P3(x1446,x1444)+~P3(x1445,x1443)+P3(x1441,x1442)+~E(x1442,f27(x1443,x1444))+~E(f26(x1445,x1446),x1441) % 121.53/122.49 [165]~P4(x1651)+~P4(x1653)+~P4(x1652)+~P3(x1655,x1653)+~P3(x1654,x1652)+~P3(f18(x1652,x1653,x1651),x1651)+E(x1651,f27(x1652,x1653))+~E(f26(x1654,x1655),f18(x1652,x1653,x1651)) % 121.53/122.49 %EqnAxiom % 121.53/122.49 [1]E(x11,x11) % 121.53/122.49 [2]E(x22,x21)+~E(x21,x22) % 121.53/122.49 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 121.53/122.49 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 121.53/122.49 [5]~E(x51,x52)+E(f27(x51,x53),f27(x52,x53)) % 121.53/122.49 [6]~E(x61,x62)+E(f27(x63,x61),f27(x63,x62)) % 121.53/122.49 [7]~E(x71,x72)+E(f28(x71),f28(x72)) % 121.53/122.49 [8]~E(x81,x82)+E(f3(x81),f3(x82)) % 121.53/122.49 [9]~E(x91,x92)+E(f24(x91,x93),f24(x92,x93)) % 121.53/122.49 [10]~E(x101,x102)+E(f24(x103,x101),f24(x103,x102)) % 121.53/122.49 [11]~E(x111,x112)+E(f22(x111,x113,x114),f22(x112,x113,x114)) % 121.53/122.49 [12]~E(x121,x122)+E(f22(x123,x121,x124),f22(x123,x122,x124)) % 121.53/122.49 [13]~E(x131,x132)+E(f22(x133,x134,x131),f22(x133,x134,x132)) % 121.53/122.49 [14]~E(x141,x142)+E(f26(x141,x143),f26(x142,x143)) % 121.53/122.49 [15]~E(x151,x152)+E(f26(x153,x151),f26(x153,x152)) % 121.53/122.49 [16]~E(x161,x162)+E(f18(x161,x163,x164),f18(x162,x163,x164)) % 121.53/122.49 [17]~E(x171,x172)+E(f18(x173,x171,x174),f18(x173,x172,x174)) % 121.53/122.49 [18]~E(x181,x182)+E(f18(x183,x184,x181),f18(x183,x184,x182)) % 121.53/122.49 [19]~E(x191,x192)+E(f21(x191,x193,x194),f21(x192,x193,x194)) % 121.53/122.49 [20]~E(x201,x202)+E(f21(x203,x201,x204),f21(x203,x202,x204)) % 121.53/122.49 [21]~E(x211,x212)+E(f21(x213,x214,x211),f21(x213,x214,x212)) % 121.53/122.49 [22]~E(x221,x222)+E(f14(x221,x223,x224),f14(x222,x223,x224)) % 121.53/122.49 [23]~E(x231,x232)+E(f14(x233,x231,x234),f14(x233,x232,x234)) % 121.53/122.49 [24]~E(x241,x242)+E(f14(x243,x244,x241),f14(x243,x244,x242)) % 121.53/122.49 [25]~E(x251,x252)+E(f9(x251,x253,x254,x255),f9(x252,x253,x254,x255)) % 121.53/122.49 [26]~E(x261,x262)+E(f9(x263,x261,x264,x265),f9(x263,x262,x264,x265)) % 121.53/122.49 [27]~E(x271,x272)+E(f9(x273,x274,x271,x275),f9(x273,x274,x272,x275)) % 121.53/122.49 [28]~E(x281,x282)+E(f9(x283,x284,x285,x281),f9(x283,x284,x285,x282)) % 121.53/122.50 [29]~E(x291,x292)+E(f4(x291),f4(x292)) % 121.53/122.50 [30]~E(x301,x302)+E(f8(x301,x303),f8(x302,x303)) % 121.53/122.50 [31]~E(x311,x312)+E(f8(x313,x311),f8(x313,x312)) % 121.53/122.50 [32]~E(x321,x322)+E(f13(x321,x323),f13(x322,x323)) % 121.53/122.50 [33]~E(x331,x332)+E(f13(x333,x331),f13(x333,x332)) % 121.53/122.50 [34]~E(x341,x342)+E(f6(x341),f6(x342)) % 121.53/122.50 [35]~E(x351,x352)+E(f16(x351,x353),f16(x352,x353)) % 121.53/122.50 [36]~E(x361,x362)+E(f16(x363,x361),f16(x363,x362)) % 121.53/122.50 [37]~E(x371,x372)+E(f20(x371,x373,x374,x375),f20(x372,x373,x374,x375)) % 121.53/122.50 [38]~E(x381,x382)+E(f20(x383,x381,x384,x385),f20(x383,x382,x384,x385)) % 121.53/122.50 [39]~E(x391,x392)+E(f20(x393,x394,x391,x395),f20(x393,x394,x392,x395)) % 121.53/122.50 [40]~E(x401,x402)+E(f20(x403,x404,x405,x401),f20(x403,x404,x405,x402)) % 121.53/122.50 [41]~E(x411,x412)+E(f15(x411,x413,x414),f15(x412,x413,x414)) % 121.53/122.50 [42]~E(x421,x422)+E(f15(x423,x421,x424),f15(x423,x422,x424)) % 121.53/122.50 [43]~E(x431,x432)+E(f15(x433,x434,x431),f15(x433,x434,x432)) % 121.53/122.50 [44]~E(x441,x442)+E(f23(x441,x443,x444),f23(x442,x443,x444)) % 121.53/122.50 [45]~E(x451,x452)+E(f23(x453,x451,x454),f23(x453,x452,x454)) % 121.53/122.50 [46]~E(x461,x462)+E(f23(x463,x464,x461),f23(x463,x464,x462)) % 121.53/122.50 [47]~E(x471,x472)+E(f19(x471,x473,x474,x475),f19(x472,x473,x474,x475)) % 121.53/122.50 [48]~E(x481,x482)+E(f19(x483,x481,x484,x485),f19(x483,x482,x484,x485)) % 121.53/122.50 [49]~E(x491,x492)+E(f19(x493,x494,x491,x495),f19(x493,x494,x492,x495)) % 121.53/122.50 [50]~E(x501,x502)+E(f19(x503,x504,x505,x501),f19(x503,x504,x505,x502)) % 121.53/122.50 [51]~E(x511,x512)+E(f5(x511),f5(x512)) % 121.53/122.50 [52]~E(x521,x522)+E(f11(x521,x523),f11(x522,x523)) % 121.53/122.50 [53]~E(x531,x532)+E(f11(x533,x531),f11(x533,x532)) % 121.53/122.50 [54]~E(x541,x542)+E(f17(x541,x543),f17(x542,x543)) % 121.53/122.50 [55]~E(x551,x552)+E(f17(x553,x551),f17(x553,x552)) % 121.53/122.50 [56]~E(x561,x562)+E(f25(x561,x563),f25(x562,x563)) % 121.53/122.50 [57]~E(x571,x572)+E(f25(x573,x571),f25(x573,x572)) % 121.53/122.50 [58]~E(x581,x582)+E(f10(x581,x583),f10(x582,x583)) % 121.53/122.50 [59]~E(x591,x592)+E(f10(x593,x591),f10(x593,x592)) % 121.53/122.50 [60]~E(x601,x602)+E(f12(x601,x603),f12(x602,x603)) % 121.53/122.50 [61]~E(x611,x612)+E(f12(x613,x611),f12(x613,x612)) % 121.53/122.50 [62]~E(x621,x622)+E(f7(x621,x623),f7(x622,x623)) % 121.53/122.50 [63]~E(x631,x632)+E(f7(x633,x631),f7(x633,x632)) % 121.53/122.50 [64]~P1(x641)+P1(x642)+~E(x641,x642) % 121.53/122.50 [65]P3(x652,x653)+~E(x651,x652)+~P3(x651,x653) % 121.53/122.50 [66]P3(x663,x662)+~E(x661,x662)+~P3(x663,x661) % 121.53/122.50 [67]~P4(x671)+P4(x672)+~E(x671,x672) % 121.53/122.50 [68]P10(x682,x683)+~E(x681,x682)+~P10(x681,x683) % 121.53/122.50 [69]P10(x693,x692)+~E(x691,x692)+~P10(x693,x691) % 121.53/122.50 [70]~P5(x701)+P5(x702)+~E(x701,x702) % 121.53/122.50 [71]P2(x712,x713)+~E(x711,x712)+~P2(x711,x713) % 121.53/122.50 [72]P2(x723,x722)+~E(x721,x722)+~P2(x723,x721) % 121.53/122.50 [73]P9(x732,x733)+~E(x731,x732)+~P9(x731,x733) % 121.53/122.50 [74]P9(x743,x742)+~E(x741,x742)+~P9(x743,x741) % 121.53/122.50 [75]P6(x752,x753,x754)+~E(x751,x752)+~P6(x751,x753,x754) % 121.53/122.50 [76]P6(x763,x762,x764)+~E(x761,x762)+~P6(x763,x761,x764) % 121.53/122.50 [77]P6(x773,x774,x772)+~E(x771,x772)+~P6(x773,x774,x771) % 121.53/122.50 [78]P11(x782,x783,x784)+~E(x781,x782)+~P11(x781,x783,x784) % 121.53/122.50 [79]P11(x793,x792,x794)+~E(x791,x792)+~P11(x793,x791,x794) % 121.53/122.50 [80]P11(x803,x804,x802)+~E(x801,x802)+~P11(x803,x804,x801) % 121.53/122.50 [81]P8(x812,x813)+~E(x811,x812)+~P8(x811,x813) % 121.53/122.50 [82]P8(x823,x822)+~E(x821,x822)+~P8(x823,x821) % 121.53/122.50 [83]~P7(x831)+P7(x832)+~E(x831,x832) % 121.53/122.50 % 121.53/122.50 %------------------------------------------- % 121.53/122.50 cnf(177,plain, % 121.53/122.50 (~P1(x1771)+P4(f2(x1771))), % 121.53/122.50 inference(equality_inference,[],[96])). % 121.53/122.50 cnf(178,plain, % 121.53/122.50 (~P4(x1781)+~P4(x1782)+P4(f27(x1782,x1781))), % 121.53/122.50 inference(equality_inference,[],[112])). % 121.53/122.50 cnf(179,plain, % 121.53/122.50 (~P4(x1791)+~P4(x1792)+P4(f25(x1792,x1791))), % 121.53/122.50 inference(equality_inference,[],[113])). % 121.53/122.50 cnf(180,plain, % 121.53/122.50 (P8(x1801,f24(x1801,x1802))+~P1(f24(x1801,x1802))+~P1(x1801)+~P1(x1802)), % 121.53/122.50 inference(equality_inference,[],[123])). % 121.53/122.50 cnf(184,plain, % 121.53/122.50 (~P1(x1841)+~P3(x1842,f2(x1841))+P1(f14(x1841,f2(x1841),x1842))), % 121.53/122.50 inference(equality_inference,[],[152])). % 121.53/122.50 cnf(185,plain, % 121.53/122.50 (~P1(x1851)+~P3(x1852,f2(x1851))+E(f24(x1851,f14(x1851,f2(x1851),x1852)),x1852)), % 121.53/122.50 inference(equality_inference,[],[154])). % 121.53/122.50 cnf(203,plain, % 121.53/122.50 (P2(a1,f24(a1,a1))+~P1(f24(a1,a1))), % 121.53/122.50 inference(scs_inference,[],[84,88,180,81,82,65,66,122])). % 121.53/122.50 cnf(224,plain, % 121.53/122.50 (P1(f28(f26(a30,a30)))), % 121.53/122.50 inference(scs_inference,[],[86,92,116])). % 121.53/122.50 cnf(232,plain, % 121.53/122.50 (E(a1,f24(a1,a31))), % 121.53/122.50 inference(scs_inference,[],[87,2,94])). % 121.53/122.50 cnf(233,plain, % 121.53/122.50 (E(f24(a1,a31),a1)), % 121.53/122.50 inference(scs_inference,[],[232,2])). % 121.53/122.50 cnf(234,plain, % 121.53/122.50 (P1(f24(a1,a31))), % 121.53/122.50 inference(scs_inference,[],[84,232,2,64])). % 121.53/122.50 cnf(239,plain, % 121.53/122.50 (P8(a1,f24(a1,a31))), % 121.53/122.50 inference(scs_inference,[],[87,84,232,2,64,123,67,81,82])). % 121.53/122.50 cnf(240,plain, % 121.53/122.50 (P2(a1,a1)), % 121.53/122.50 inference(scs_inference,[],[87,84,232,2,64,123,67,81,82,122])). % 121.53/122.50 cnf(250,plain, % 121.53/122.50 (P8(f24(a1,a31),f24(a1,a31))), % 121.53/122.50 inference(scs_inference,[],[239,240,232,71,72,81])). % 121.53/122.50 cnf(258,plain, % 121.53/122.50 (P3(a1,x2581)+~E(x2581,f2(a1))), % 121.53/122.50 inference(scs_inference,[],[87,84,234,233,239,240,232,71,72,81,122,83,67,70,180,124])). % 121.53/122.50 cnf(260,plain, % 121.53/122.50 (P3(a1,f2(a1))), % 121.53/122.50 inference(equality_inference,[],[258])). % 121.53/122.50 cnf(261,plain, % 121.53/122.50 (P3(f24(a1,a31),f2(a1))), % 121.53/122.50 inference(scs_inference,[],[232,260,65])). % 121.53/122.50 cnf(270,plain, % 121.53/122.50 (P3(f24(a1,a31),x2701)+~E(f2(a1),x2701)), % 121.53/122.50 inference(scs_inference,[],[261,66])). % 121.53/122.50 cnf(286,plain, % 121.53/122.50 (E(f24(f28(f24(a1,a31)),a1),a1)), % 121.53/122.50 inference(scs_inference,[],[234,95,92])). % 121.53/122.50 cnf(287,plain, % 121.53/122.50 (E(a1,f24(f28(f24(a1,a31)),a1))), % 121.53/122.50 inference(scs_inference,[],[286,2])). % 121.53/122.50 cnf(395,plain, % 121.53/122.50 (E(f2(a1),f2(f24(a1,a31)))), % 121.53/122.50 inference(scs_inference,[],[233,4,2])). % 121.53/122.50 cnf(396,plain, % 121.53/122.50 (P3(f24(a1,a31),f2(f24(a1,a31)))), % 121.53/122.50 inference(scs_inference,[],[395,270])). % 121.53/122.50 cnf(398,plain, % 121.53/122.50 (P4(f2(a1))), % 121.53/122.50 inference(scs_inference,[],[234,395,270,2,96])). % 121.53/122.50 cnf(400,plain, % 121.53/122.50 (P4(f2(f24(a1,a31)))), % 121.53/122.50 inference(scs_inference,[],[234,395,270,2,96,67])). % 121.53/122.50 cnf(401,plain, % 121.53/122.50 (P3(a1,f2(f24(a1,a31)))), % 121.53/122.50 inference(scs_inference,[],[234,233,395,270,2,96,67,65])). % 121.53/122.50 cnf(556,plain, % 121.53/122.50 (E(f26(f28(f28(a1)),f28(a1)),a1)), % 121.53/122.50 inference(scs_inference,[],[84,102,92])). % 121.53/122.50 cnf(557,plain, % 121.53/122.50 (E(a1,f26(f28(f28(a1)),f28(a1)))), % 121.53/122.50 inference(scs_inference,[],[556,2])). % 121.53/122.50 cnf(620,plain, % 121.53/122.50 (E(f26(f28(a1),f28(f28(a1))),a1)), % 121.53/122.50 inference(scs_inference,[],[84,103,92])). % 121.53/122.50 cnf(621,plain, % 121.53/122.50 (E(a1,f26(f28(a1),f28(f28(a1))))), % 121.53/122.50 inference(scs_inference,[],[620,2])). % 121.53/122.50 cnf(622,plain, % 121.53/122.50 (E(f24(a1,a31),f26(f28(a1),f28(f28(a1))))), % 121.53/122.50 inference(scs_inference,[],[233,620,2,3])). % 121.53/122.50 cnf(623,plain, % 121.53/122.50 (P1(f26(f28(a1),f28(f28(a1))))), % 121.53/122.50 inference(scs_inference,[],[84,233,620,2,3,64])). % 121.53/122.50 cnf(832,plain, % 121.53/122.50 (E(f24(f28(a1),f28(a29)),f28(f28(a1)))), % 121.53/122.50 inference(scs_inference,[],[84,104,92])). % 121.53/122.50 cnf(833,plain, % 121.53/122.50 (E(f28(f28(a1)),f24(f28(a1),f28(a29)))), % 121.53/122.50 inference(scs_inference,[],[832,2])). % 121.53/122.50 cnf(843,plain, % 121.53/122.50 (~P1(f28(f28(a1)))+P1(f24(f28(a1),f28(a29)))), % 121.53/122.50 inference(scs_inference,[],[833,70,64])). % 121.53/122.50 cnf(863,plain, % 121.53/122.50 (E(f24(f28(a29),f28(a1)),f28(f28(a1)))), % 121.53/122.50 inference(scs_inference,[],[84,105,92])). % 121.53/122.50 cnf(864,plain, % 121.53/122.50 (E(f28(f28(a1)),f24(f28(a29),f28(a1)))), % 121.53/122.50 inference(scs_inference,[],[863,2])). % 121.53/122.50 cnf(865,plain, % 121.53/122.50 (E(f24(f28(a1),f28(a29)),f24(f28(a29),f28(a1)))), % 121.53/122.50 inference(scs_inference,[],[832,863,2,3])). % 121.53/122.50 cnf(872,plain, % 121.53/122.50 (~P1(f28(f28(a1)))+P1(f24(f28(a29),f28(a1)))), % 121.53/122.50 inference(scs_inference,[],[864,865,2,70,64])). % 121.53/122.50 cnf(877,plain, % 121.53/122.50 (P8(f26(f28(a1),f28(f28(a1))),f24(a1,a31))), % 121.53/122.50 inference(scs_inference,[],[239,621,81])). % 121.53/122.50 cnf(932,plain, % 121.53/122.50 (P2(a1,f24(a1,a1))), % 121.53/122.50 inference(scs_inference,[],[84,203,117])). % 121.53/122.50 cnf(1042,plain, % 121.53/122.50 (P2(f26(f28(f28(a1)),f28(a1)),f24(a1,a1))), % 121.53/122.50 inference(scs_inference,[],[557,932,71])). % 121.53/122.50 cnf(1836,plain, % 121.53/122.50 (~P1(f28(a1))+P1(f24(f28(a1),f28(a29)))), % 121.53/122.50 inference(scs_inference,[],[843,92])). % 121.53/122.50 cnf(1852,plain, % 121.53/122.50 (~P1(f28(a1))+E(f24(a1,f24(f28(a1),f28(a29))),a1)), % 121.53/122.50 inference(scs_inference,[],[1836,94])). % 121.53/122.50 cnf(1963,plain, % 121.53/122.50 (~P1(f28(a1))+P1(f24(f28(a29),f28(a1)))), % 121.53/122.50 inference(scs_inference,[],[872,92])). % 121.53/122.50 cnf(1979,plain, % 121.53/122.50 (~P1(f28(a1))+E(f24(a1,f24(f28(a29),f28(a1))),a1)), % 121.53/122.50 inference(scs_inference,[],[1963,94])). % 121.53/122.50 cnf(2686,plain, % 121.53/122.50 (E(f26(a1,a1),a1)), % 121.53/122.50 inference(scs_inference,[],[84,224,92,177,97])). % 121.53/122.50 cnf(2692,plain, % 121.53/122.50 (E(f24(a1,a29),a1)), % 121.53/122.50 inference(scs_inference,[],[84,224,92,177,97,98,99,100])). % 121.53/122.50 cnf(2770,plain, % 121.53/122.50 (~E(a29,a1)), % 121.53/122.50 inference(scs_inference,[],[84,90,224,556,92,177,97,98,99,100,94,95,101,4,7,8,29,34,51,102,103,5,6,9,10,14,15,30,31,32,33,35,36,52,53,54,55,56,57,58,59,60,61,62,63,104,105,11,12,13,16,17,18,19,20,21,22,23,24,41,42,43,44,45,46,25,26,27,28,37,38,39,40,47,48,49,50,1852,1979,2])). % 121.53/122.50 cnf(2781,plain, % 121.53/122.50 (P1(f24(a1,a1))), % 121.53/122.50 inference(scs_inference,[],[84,90,224,85,400,556,86,89,92,177,97,98,99,100,94,95,101,4,7,8,29,34,51,102,103,5,6,9,10,14,15,30,31,32,33,35,36,52,53,54,55,56,57,58,59,60,61,62,63,104,105,11,12,13,16,17,18,19,20,21,22,23,24,41,42,43,44,45,46,25,26,27,28,37,38,39,40,47,48,49,50,1852,1979,2,116,178,93,184,185,117])). % 121.53/122.50 cnf(2791,plain, % 121.53/122.50 (P1(f10(a1,a29))), % 121.53/122.50 inference(scs_inference,[],[84,90,224,877,623,396,85,400,287,556,86,622,234,89,92,177,97,98,99,100,94,95,101,4,7,8,29,34,51,102,103,5,6,9,10,14,15,30,31,32,33,35,36,52,53,54,55,56,57,58,59,60,61,62,63,104,105,11,12,13,16,17,18,19,20,21,22,23,24,41,42,43,44,45,46,25,26,27,28,37,38,39,40,47,48,49,50,1852,1979,2,116,178,93,184,185,117,65,179,3,125,120,121])). % 121.53/122.50 cnf(2803,plain, % 121.53/122.50 (E(f26(f24(a1,a1),f24(a1,a1)),f24(f26(a1,a1),a1))), % 121.53/122.50 inference(scs_inference,[],[84,90,224,877,623,250,396,85,400,287,556,86,622,234,89,92,177,97,98,99,100,94,95,101,4,7,8,29,34,51,102,103,5,6,9,10,14,15,30,31,32,33,35,36,52,53,54,55,56,57,58,59,60,61,62,63,104,105,11,12,13,16,17,18,19,20,21,22,23,24,41,42,43,44,45,46,25,26,27,28,37,38,39,40,47,48,49,50,1852,1979,2,116,178,93,184,185,117,65,179,3,125,120,121,129,135,136,150,146,147])). % 121.53/122.50 cnf(2805,plain, % 121.53/122.50 (~E(f24(a29,a29),a1)), % 121.53/122.50 inference(scs_inference,[],[84,90,224,877,623,250,396,85,400,287,556,86,622,234,89,92,177,97,98,99,100,94,95,101,4,7,8,29,34,51,102,103,5,6,9,10,14,15,30,31,32,33,35,36,52,53,54,55,56,57,58,59,60,61,62,63,104,105,11,12,13,16,17,18,19,20,21,22,23,24,41,42,43,44,45,46,25,26,27,28,37,38,39,40,47,48,49,50,1852,1979,2,116,178,93,184,185,117,65,179,3,125,120,121,129,135,136,150,146,147,109])). % 121.53/122.50 cnf(2932,plain, % 121.53/122.50 (~E(a29,f26(a1,a1))), % 121.53/122.50 inference(scs_inference,[],[84,2770,2781,2686,2805,2803,1042,401,260,234,398,177,97,95,104,102,98,9,16,25,94,63,40,18,99,22,20,103,59,23,6,17,48,2,15,57,30,19,31,26,28,39,52,55,47,53,100,35,101,43,105,34,21,41,4,32,37,56,5,10,92,50,24,7,45,12,38,13,44,11,42,46,29,61,60,58,33,51,54,36,62,27,14,49,8,117,184,116,178,115,185,64,179,3])). % 121.53/122.50 cnf(3205,plain, % 121.53/122.50 (P1(f14(a30,f2(a30),a32))), % 121.53/122.50 inference(scs_inference,[],[2692,2791,2932,86,88,97,95,94,102,99,103,177,104,101,20,23,98,92,9,2,56,15,16,105,100,59,53,28,47,57,55,30,25,45,6,29,22,10,58,7,40,31,18,32,17,27,35,34,52,43,50,4,5,13,41,63,21,39,12,24,19,49,11,48,26,38,33,8,37,51,36,54,44,61,46,62,42,60,14,184])). % 121.53/122.50 cnf(3209,plain, % 121.53/122.50 (E(f24(a30,f14(a30,f2(a30),a32)),a32)), % 121.53/122.50 inference(scs_inference,[],[2692,2791,2932,86,88,97,95,94,102,99,103,177,104,101,20,23,98,92,9,2,56,15,16,105,100,59,53,28,47,57,55,30,25,45,6,29,22,10,58,7,40,31,18,32,17,27,35,34,52,43,50,4,5,13,41,63,21,39,12,24,19,49,11,48,26,38,33,8,37,51,36,54,44,61,46,62,42,60,14,184,117,185])). % 121.53/122.50 cnf(5546,plain, % 121.53/122.50 ($false), % 121.53/122.50 inference(scs_inference,[],[2686,3209,3205,2,101]), % 121.53/122.50 ['proof']). % 121.53/122.50 % SZS output end Proof % 121.53/122.50 % Total time :120.860000s %------------------------------------------------------------------------------