%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : RNG091+2 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n005.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 14:01:02 EDT 2024 % Result : Theorem 0.49s 0.61s % Output : CNFRefutation 0.49s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.05/0.10 % Problem : RNG091+2 : TPTP v8.2.0. Released v4.0.0. % 0.05/0.10 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.10/0.30 % Computer : n005.cluster.edu % 0.10/0.30 % Model : x86_64 x86_64 % 0.10/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.30 % Memory : 8042.1875MB % 0.10/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.30 % CPULimit : 300 % 0.10/0.30 % WCLimit : 300 % 0.10/0.30 % DateTime : Tue Jun 18 13:19:53 EDT 2024 % 0.10/0.30 % CPUTime : % 0.47/0.54 start to proof:theBenchmark % 0.49/0.59 %------------------------------------------- % 0.49/0.59 % File :CSE---1.7 % 0.49/0.59 % Problem :theBenchmark % 0.49/0.59 % Transform :cnf % 0.49/0.60 % Format :tptp:raw % 0.49/0.60 % Command :java -jar mcs_scs.jar %d %s % 0.49/0.60 % 0.49/0.60 % Result :Theorem 0.010000s % 0.49/0.60 % Output :CNFRefutation 0.010000s % 0.49/0.60 %------------------------------------------- % 0.49/0.60 %------------------------------------------------------------------------------ % 0.49/0.60 % File : RNG091+2 : TPTP v8.2.0. Released v4.0.0. % 0.49/0.60 % Domain : Ring Theory % 0.49/0.60 % Problem : Chinese remainder theorem in a ring 03_07, 01 expansion % 0.49/0.60 % Version : Especial. % 0.49/0.60 % English : % 0.49/0.60 % 0.49/0.60 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 0.49/0.60 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 0.49/0.60 % Source : [Pas08] % 0.49/0.60 % Names : chines_03_07.01 [Pas08] % 0.49/0.60 % 0.49/0.60 % Status : Theorem % 0.49/0.60 % Rating : 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.22 v7.0.0, 0.17 v6.4.0, 0.19 v6.3.0, 0.25 v6.2.0, 0.28 v6.1.0, 0.43 v6.0.0, 0.26 v5.5.0, 0.41 v5.4.0, 0.43 v5.3.0, 0.52 v5.2.0, 0.45 v5.1.0, 0.57 v5.0.0, 0.58 v4.1.0, 0.61 v4.0.1, 0.87 v4.0.0 % 0.49/0.60 % Syntax : Number of formulae : 33 ( 5 unt; 3 def) % 0.49/0.60 % Number of atoms : 129 ( 32 equ) % 0.49/0.60 % Maximal formula atoms : 14 ( 3 avg) % 0.49/0.60 % Number of connectives : 97 ( 1 ~; 3 |; 54 &) % 0.49/0.60 % ( 5 <=>; 34 =>; 0 <=; 0 <~>) % 0.49/0.60 % Maximal formula depth : 13 ( 5 avg) % 0.49/0.60 % Maximal term depth : 3 ( 1 avg) % 0.49/0.60 % Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty) % 0.49/0.60 % Number of functors : 16 ( 16 usr; 11 con; 0-2 aty) % 0.49/0.60 % Number of variables : 61 ( 51 !; 10 ?) % 0.49/0.60 % SPC : FOF_THM_RFO_SEQ % 0.49/0.60 % 0.49/0.60 % Comments : Problem generated by the SAD system [VLP07] % 0.49/0.60 %------------------------------------------------------------------------------ % 0.49/0.60 fof(mElmSort,axiom, % 0.49/0.60 ! [W0] : % 0.49/0.60 ( aElement0(W0) % 0.49/0.60 => $true ) ). % 0.49/0.60 % 0.49/0.60 fof(mSortsC,axiom, % 0.49/0.60 aElement0(sz00) ). % 0.49/0.60 % 0.49/0.60 fof(mSortsC_01,axiom, % 0.49/0.60 aElement0(sz10) ). % 0.49/0.60 % 0.49/0.60 fof(mSortsU,axiom, % 0.49/0.60 ! [W0] : % 0.49/0.60 ( aElement0(W0) % 0.49/0.60 => aElement0(smndt0(W0)) ) ). % 0.49/0.60 % 0.49/0.60 fof(mSortsB,axiom, % 0.49/0.60 ! [W0,W1] : % 0.49/0.60 ( ( aElement0(W0) % 0.49/0.60 & aElement0(W1) ) % 0.49/0.60 => aElement0(sdtpldt0(W0,W1)) ) ). % 0.49/0.60 % 0.49/0.60 fof(mSortsB_02,axiom, % 0.49/0.60 ! [W0,W1] : % 0.49/0.60 ( ( aElement0(W0) % 0.49/0.60 & aElement0(W1) ) % 0.49/0.60 => aElement0(sdtasdt0(W0,W1)) ) ). % 0.49/0.60 % 0.49/0.60 fof(mAddComm,axiom, % 0.49/0.60 ! [W0,W1] : % 0.49/0.60 ( ( aElement0(W0) % 0.49/0.60 & aElement0(W1) ) % 0.49/0.60 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 0.49/0.60 % 0.49/0.60 fof(mAddAsso,axiom, % 0.49/0.60 ! [W0,W1,W2] : % 0.49/0.60 ( ( aElement0(W0) % 0.49/0.60 & aElement0(W1) % 0.49/0.60 & aElement0(W2) ) % 0.49/0.60 => sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) ). % 0.49/0.60 % 0.49/0.60 fof(mAddZero,axiom, % 0.49/0.60 ! [W0] : % 0.49/0.60 ( aElement0(W0) % 0.49/0.60 => ( sdtpldt0(W0,sz00) = W0 % 0.49/0.60 & W0 = sdtpldt0(sz00,W0) ) ) ). % 0.49/0.60 % 0.49/0.60 fof(mAddInvr,axiom, % 0.49/0.60 ! [W0] : % 0.49/0.60 ( aElement0(W0) % 0.49/0.60 => ( sdtpldt0(W0,smndt0(W0)) = sz00 % 0.49/0.60 & sz00 = sdtpldt0(smndt0(W0),W0) ) ) ). % 0.49/0.60 % 0.49/0.60 fof(mMulComm,axiom, % 0.49/0.60 ! [W0,W1] : % 0.49/0.60 ( ( aElement0(W0) % 0.49/0.60 & aElement0(W1) ) % 0.49/0.60 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 0.49/0.60 % 0.49/0.60 fof(mMulAsso,axiom, % 0.49/0.60 ! [W0,W1,W2] : % 0.49/0.60 ( ( aElement0(W0) % 0.49/0.60 & aElement0(W1) % 0.49/0.60 & aElement0(W2) ) % 0.49/0.60 => sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) ). % 0.49/0.60 % 0.49/0.60 fof(mMulUnit,axiom, % 0.49/0.60 ! [W0] : % 0.49/0.60 ( aElement0(W0) % 0.49/0.60 => ( sdtasdt0(W0,sz10) = W0 % 0.49/0.60 & W0 = sdtasdt0(sz10,W0) ) ) ). % 0.49/0.60 % 0.49/0.60 fof(mAMDistr,axiom, % 0.49/0.60 ! [W0,W1,W2] : % 0.49/0.60 ( ( aElement0(W0) % 0.49/0.60 & aElement0(W1) % 0.49/0.60 & aElement0(W2) ) % 0.49/0.60 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 0.49/0.60 & sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ). % 0.49/0.60 % 0.49/0.60 fof(mMulMnOne,axiom, % 0.49/0.60 ! [W0] : % 0.49/0.60 ( aElement0(W0) % 0.49/0.60 => ( sdtasdt0(smndt0(sz10),W0) = smndt0(W0) % 0.49/0.60 & smndt0(W0) = sdtasdt0(W0,smndt0(sz10)) ) ) ). % 0.49/0.60 % 0.49/0.60 fof(mMulZero,axiom, % 0.49/0.60 ! [W0] : % 0.49/0.60 ( aElement0(W0) % 0.49/0.60 => ( sdtasdt0(W0,sz00) = sz00 % 0.49/0.60 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 0.49/0.60 % 0.49/0.60 fof(mCancel,axiom, % 0.49/0.60 ! [W0,W1] : % 0.49/0.60 ( ( aElement0(W0) % 0.49/0.60 & aElement0(W1) ) % 0.49/0.60 => ( sdtasdt0(W0,W1) = sz00 % 0.49/0.60 => ( W0 = sz00 % 0.49/0.60 | W1 = sz00 ) ) ) ). % 0.49/0.60 % 0.49/0.60 fof(mUnNeZr,axiom, % 0.49/0.60 sz10 != sz00 ). % 0.49/0.60 % 0.49/0.60 fof(mSetSort,axiom, % 0.49/0.60 ! [W0] : % 0.49/0.60 ( aSet0(W0) % 0.49/0.60 => $true ) ). % 0.49/0.60 % 0.49/0.60 fof(mEOfElem,axiom, % 0.49/0.60 ! [W0] : % 0.49/0.60 ( aSet0(W0) % 0.49/0.60 => ! [W1] : % 0.49/0.60 ( aElementOf0(W1,W0) % 0.49/0.60 => aElement0(W1) ) ) ). % 0.49/0.60 % 0.49/0.60 fof(mSetEq,axiom, % 0.49/0.60 ! [W0,W1] : % 0.49/0.60 ( ( aSet0(W0) % 0.49/0.60 & aSet0(W1) ) % 0.49/0.60 => ( ( ! [W2] : % 0.49/0.60 ( aElementOf0(W2,W0) % 0.49/0.60 => aElementOf0(W2,W1) ) % 0.49/0.60 & ! [W2] : % 0.49/0.60 ( aElementOf0(W2,W1) % 0.49/0.60 => aElementOf0(W2,W0) ) ) % 0.49/0.60 => W0 = W1 ) ) ). % 0.49/0.60 % 0.49/0.60 fof(mDefSSum,definition, % 0.49/0.60 ! [W0,W1] : % 0.49/0.60 ( ( aSet0(W0) % 0.49/0.60 & aSet0(W1) ) % 0.49/0.60 => ! [W2] : % 0.49/0.60 ( W2 = sdtpldt1(W0,W1) % 0.49/0.60 <=> ( aSet0(W2) % 0.49/0.60 & ! [W3] : % 0.49/0.60 ( aElementOf0(W3,W2) % 0.49/0.60 <=> ? [W4,W5] : % 0.49/0.60 ( aElementOf0(W4,W0) % 0.49/0.60 & aElementOf0(W5,W1) % 0.49/0.60 & sdtpldt0(W4,W5) = W3 ) ) ) ) ) ). % 0.49/0.60 % 0.49/0.60 fof(mDefSInt,definition, % 0.49/0.60 ! [W0,W1] : % 0.49/0.60 ( ( aSet0(W0) % 0.49/0.60 & aSet0(W1) ) % 0.49/0.60 => ! [W2] : % 0.49/0.60 ( W2 = sdtasasdt0(W0,W1) % 0.49/0.60 <=> ( aSet0(W2) % 0.49/0.61 & ! [W3] : % 0.49/0.61 ( aElementOf0(W3,W2) % 0.49/0.61 <=> ( aElementOf0(W3,W0) % 0.49/0.61 & aElementOf0(W3,W1) ) ) ) ) ) ). % 0.49/0.61 % 0.49/0.61 fof(mDefIdeal,definition, % 0.49/0.61 ! [W0] : % 0.49/0.61 ( aIdeal0(W0) % 0.49/0.61 <=> ( aSet0(W0) % 0.49/0.61 & ! [W1] : % 0.49/0.61 ( aElementOf0(W1,W0) % 0.49/0.61 => ( ! [W2] : % 0.49/0.61 ( aElementOf0(W2,W0) % 0.49/0.61 => aElementOf0(sdtpldt0(W1,W2),W0) ) % 0.49/0.61 & ! [W2] : % 0.49/0.61 ( aElement0(W2) % 0.49/0.61 => aElementOf0(sdtasdt0(W2,W1),W0) ) ) ) ) ) ). % 0.49/0.61 % 0.49/0.61 fof(m__870,hypothesis, % 0.49/0.61 ( aSet0(xI) % 0.49/0.61 & ! [W0] : % 0.49/0.61 ( aElementOf0(W0,xI) % 0.49/0.61 => ( ! [W1] : % 0.49/0.61 ( aElementOf0(W1,xI) % 0.49/0.61 => aElementOf0(sdtpldt0(W0,W1),xI) ) % 0.49/0.61 & ! [W1] : % 0.49/0.61 ( aElement0(W1) % 0.49/0.61 => aElementOf0(sdtasdt0(W1,W0),xI) ) ) ) % 0.49/0.61 & aIdeal0(xI) % 0.49/0.61 & aSet0(xJ) % 0.49/0.61 & ! [W0] : % 0.49/0.61 ( aElementOf0(W0,xJ) % 0.49/0.61 => ( ! [W1] : % 0.49/0.61 ( aElementOf0(W1,xJ) % 0.49/0.61 => aElementOf0(sdtpldt0(W0,W1),xJ) ) % 0.49/0.61 & ! [W1] : % 0.49/0.61 ( aElement0(W1) % 0.49/0.61 => aElementOf0(sdtasdt0(W1,W0),xJ) ) ) ) % 0.49/0.61 & aIdeal0(xJ) ) ). % 0.49/0.61 % 0.49/0.61 fof(m__901,hypothesis, % 0.49/0.61 ( ? [W0,W1] : % 0.49/0.61 ( aElementOf0(W0,xI) % 0.49/0.61 & aElementOf0(W1,xJ) % 0.49/0.61 & sdtpldt0(W0,W1) = xx ) % 0.49/0.61 & aElementOf0(xx,sdtpldt1(xI,xJ)) % 0.49/0.61 & ? [W0,W1] : % 0.49/0.61 ( aElementOf0(W0,xI) % 0.49/0.61 & aElementOf0(W1,xJ) % 0.49/0.61 & sdtpldt0(W0,W1) = xy ) % 0.49/0.61 & aElementOf0(xy,sdtpldt1(xI,xJ)) % 0.49/0.61 & aElement0(xz) ) ). % 0.49/0.61 % 0.49/0.61 fof(m__934,hypothesis, % 0.49/0.61 ( aElementOf0(xk,xI) % 0.49/0.61 & aElementOf0(xl,xJ) % 0.49/0.61 & xx = sdtpldt0(xk,xl) ) ). % 0.49/0.61 % 0.49/0.61 fof(m__967,hypothesis, % 0.49/0.61 ( aElementOf0(xm,xI) % 0.49/0.61 & aElementOf0(xn,xJ) % 0.49/0.61 & xy = sdtpldt0(xm,xn) ) ). % 0.49/0.61 % 0.49/0.61 fof(m__994,hypothesis, % 0.49/0.61 ( aElementOf0(sdtpldt0(xk,xm),xI) % 0.49/0.61 & aElementOf0(sdtpldt0(xl,xn),xJ) ) ). % 0.49/0.61 % 0.49/0.61 fof(m__1021,hypothesis, % 0.49/0.61 ( aElementOf0(sdtasdt0(xz,xk),xI) % 0.49/0.61 & aElementOf0(sdtasdt0(xz,xl),xJ) ) ). % 0.49/0.61 % 0.49/0.61 fof(m__1061,hypothesis, % 0.49/0.61 sdtpldt0(xx,xy) = sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn)) ). % 0.49/0.61 % 0.49/0.61 fof(m__1098,hypothesis, % 0.49/0.61 sdtasdt0(xz,xx) = sdtpldt0(sdtasdt0(xz,xk),sdtasdt0(xz,xl)) ). % 0.49/0.61 % 0.49/0.61 fof(m__,conjecture, % 0.49/0.61 ( ( ? [W0,W1] : % 0.49/0.61 ( aElementOf0(W0,xI) % 0.49/0.61 & aElementOf0(W1,xJ) % 0.49/0.61 & sdtpldt0(W0,W1) = sdtpldt0(xx,xy) ) % 0.49/0.61 | aElementOf0(sdtpldt0(xx,xy),sdtpldt1(xI,xJ)) ) % 0.49/0.61 & ( ? [W0,W1] : % 0.49/0.61 ( aElementOf0(W0,xI) % 0.49/0.61 & aElementOf0(W1,xJ) % 0.49/0.61 & sdtpldt0(W0,W1) = sdtasdt0(xz,xx) ) % 0.49/0.61 | aElementOf0(sdtasdt0(xz,xx),sdtpldt1(xI,xJ)) ) ) ). % 0.49/0.61 % 0.49/0.61 %------------------------------------------------------------------------------ % 0.49/0.61 %------------------------------------------- % 0.49/0.61 % Proof found % 0.49/0.61 % SZS status Theorem for theBenchmark % 0.49/0.61 % SZS output start Proof % 0.49/0.61 %ClaNum:129(EqnAxiom:44) % 0.49/0.61 %VarNum:424(SingletonVarNum:130) % 0.49/0.61 %MaxLitNum:8 % 0.49/0.61 %MaxfuncDepth:2 % 0.49/0.61 %SharedTerms:59 % 0.49/0.61 %goalClause: 115 116 117 118 % 0.49/0.61 [45]P1(a1) % 0.49/0.61 [46]P1(a22) % 0.49/0.61 [47]P1(a23) % 0.49/0.61 [48]P2(a24) % 0.49/0.61 [49]P2(a25) % 0.49/0.61 [50]P3(a24) % 0.49/0.61 [51]P3(a25) % 0.49/0.61 [56]P4(a26,a24) % 0.49/0.61 [57]P4(a27,a25) % 0.49/0.61 [58]P4(a29,a24) % 0.49/0.61 [59]P4(a30,a25) % 0.49/0.61 [60]P4(a3,a24) % 0.49/0.61 [61]P4(a6,a25) % 0.49/0.61 [62]P4(a7,a24) % 0.49/0.61 [63]P4(a8,a25) % 0.49/0.61 [72]~E(a1,a22) % 0.49/0.61 [52]E(f2(a26,a27),a28) % 0.49/0.61 [53]E(f2(a29,a30),a31) % 0.49/0.61 [54]E(f2(a3,a6),a28) % 0.49/0.61 [55]E(f2(a7,a8),a31) % 0.49/0.61 [64]P4(a28,f20(a24,a25)) % 0.49/0.61 [65]P4(a31,f20(a24,a25)) % 0.49/0.61 [66]P4(f2(a26,a29),a24) % 0.49/0.61 [67]P4(f2(a27,a30),a25) % 0.49/0.61 [68]P4(f9(a23,a26),a24) % 0.49/0.61 [69]P4(f9(a23,a27),a25) % 0.49/0.61 [70]E(f2(f2(a26,a29),f2(a27,a30)),f2(a28,a31)) % 0.49/0.61 [71]E(f2(f9(a23,a26),f9(a23,a27)),f9(a23,a28)) % 0.49/0.61 [118]~P4(f2(a28,a31),f20(a24,a25))+~P4(f9(a23,a28),f20(a24,a25)) % 0.49/0.61 [73]~P3(x731)+P2(x731) % 0.49/0.61 [74]~P1(x741)+P1(f21(x741)) % 0.49/0.61 [75]~P1(x751)+E(f9(a1,x751),a1) % 0.49/0.61 [76]~P1(x761)+E(f9(x761,a1),a1) % 0.49/0.61 [77]~P1(x771)+E(f2(a1,x771),x771) % 0.49/0.61 [78]~P1(x781)+E(f9(a22,x781),x781) % 0.49/0.61 [79]~P1(x791)+E(f2(x791,a1),x791) % 0.49/0.61 [80]~P1(x801)+E(f9(x801,a22),x801) % 0.49/0.61 [81]~P1(x811)+E(f2(f21(x811),x811),a1) % 0.49/0.61 [82]~P1(x821)+E(f2(x821,f21(x821)),a1) % 0.49/0.61 [83]~P1(x831)+E(f9(x831,f21(a22)),f21(x831)) % 0.49/0.61 [84]~P1(x841)+E(f9(f21(a22),x841),f21(x841)) % 0.49/0.61 [85]~P2(x851)+P3(x851)+P4(f10(x851),x851) % 0.49/0.61 [86]~P4(x861,x862)+P1(x861)+~P2(x862) % 0.49/0.61 [88]~P1(x882)+~P1(x881)+E(f2(x881,x882),f2(x882,x881)) % 0.49/0.61 [89]~P1(x892)+~P1(x891)+E(f9(x891,x892),f9(x892,x891)) % 0.49/0.61 [93]~P1(x932)+~P1(x931)+P1(f2(x931,x932)) % 0.49/0.61 [94]~P1(x942)+~P1(x941)+P1(f9(x941,x942)) % 0.49/0.61 [95]~P1(x951)+~P4(x952,a24)+P4(f9(x951,x952),a24) % 0.49/0.61 [96]~P1(x961)+~P4(x962,a25)+P4(f9(x961,x962),a25) % 0.49/0.61 [100]~P4(x1001,a24)+~P4(x1002,a24)+P4(f2(x1001,x1002),a24) % 0.49/0.61 [101]~P4(x1011,a25)+~P4(x1012,a25)+P4(f2(x1011,x1012),a25) % 0.49/0.61 [92]~P2(x921)+P3(x921)+P4(f5(x921),x921)+P1(f4(x921)) % 0.49/0.61 [110]~P2(x1101)+P3(x1101)+P1(f4(x1101))+~P4(f2(f10(x1101),f5(x1101)),x1101) % 0.49/0.61 [113]~P2(x1131)+P3(x1131)+P4(f5(x1131),x1131)+~P4(f9(f4(x1131),f10(x1131)),x1131) % 0.49/0.61 [119]~P2(x1191)+P3(x1191)+~P4(f2(f10(x1191),f5(x1191)),x1191)+~P4(f9(f4(x1191),f10(x1191)),x1191) % 0.49/0.61 [116]~P4(x1162,a25)+~P4(x1161,a24)+~E(f2(x1161,x1162),f2(a28,a31))+~P4(f9(a23,a28),f20(a24,a25)) % 0.49/0.61 [117]~P4(x1172,a25)+~P4(x1171,a24)+~E(f2(x1171,x1172),f9(a23,a28))+~P4(f2(a28,a31),f20(a24,a25)) % 0.49/0.61 [90]~P2(x903)+~P2(x902)+P2(x901)+~E(x901,f20(x902,x903)) % 0.49/0.61 [91]~P2(x913)+~P2(x912)+P2(x911)+~E(x911,f19(x912,x913)) % 0.49/0.61 [99]~P1(x991)+~P3(x993)+~P4(x992,x993)+P4(f9(x991,x992),x993) % 0.49/0.61 [102]~P3(x1023)+~P4(x1021,x1023)+~P4(x1022,x1023)+P4(f2(x1021,x1022),x1023) % 0.49/0.61 [105]~P1(x1053)+~P1(x1052)+~P1(x1051)+E(f2(f2(x1051,x1052),x1053),f2(x1051,f2(x1052,x1053))) % 0.49/0.61 [106]~P1(x1063)+~P1(x1062)+~P1(x1061)+E(f9(f9(x1061,x1062),x1063),f9(x1061,f9(x1062,x1063))) % 0.49/0.61 [111]~P1(x1113)+~P1(x1112)+~P1(x1111)+E(f2(f9(x1111,x1112),f9(x1111,x1113)),f9(x1111,f2(x1112,x1113))) % 0.49/0.61 [112]~P1(x1122)+~P1(x1123)+~P1(x1121)+E(f2(f9(x1121,x1122),f9(x1123,x1122)),f9(f2(x1121,x1123),x1122)) % 0.49/0.61 [87]~P1(x871)+~P1(x872)+E(x871,a1)+E(x872,a1)+~E(f9(x872,x871),a1) % 0.49/0.61 [103]~P2(x1032)+~P2(x1031)+E(x1031,x1032)+P4(f11(x1031,x1032),x1031)+P4(f12(x1031,x1032),x1032) % 0.49/0.61 [107]~P2(x1072)+~P2(x1071)+E(x1071,x1072)+P4(f11(x1071,x1072),x1071)+~P4(f12(x1071,x1072),x1071) % 0.49/0.61 [108]~P2(x1082)+~P2(x1081)+E(x1081,x1082)+P4(f12(x1081,x1082),x1082)+~P4(f11(x1081,x1082),x1082) % 0.49/0.61 [114]~P2(x1142)+~P2(x1141)+E(x1141,x1142)+~P4(f11(x1141,x1142),x1142)+~P4(f12(x1141,x1142),x1141) % 0.49/0.61 [97]~P2(x974)+~P2(x972)+~P4(x971,x973)+P4(x971,x972)+~E(x973,f19(x974,x972)) % 0.49/0.61 [98]~P2(x984)+~P2(x982)+~P4(x981,x983)+P4(x981,x982)+~E(x983,f19(x982,x984)) % 0.49/0.61 [126]~P2(x1262)+~P2(x1261)+~P4(x1264,x1263)+~E(x1263,f20(x1261,x1262))+P4(f14(x1261,x1262,x1263,x1264),x1261) % 0.49/0.61 [127]~P2(x1272)+~P2(x1271)+~P4(x1274,x1273)+~E(x1273,f20(x1271,x1272))+P4(f15(x1271,x1272,x1273,x1274),x1272) % 0.49/0.61 [129]~P2(x1292)+~P2(x1291)+~P4(x1294,x1293)+~E(x1293,f20(x1291,x1292))+E(f2(f14(x1291,x1292,x1293,x1294),f15(x1291,x1292,x1293,x1294)),x1294) % 0.49/0.61 [120]~P2(x1201)+~P2(x1203)+~P2(x1202)+P4(f13(x1202,x1203,x1201),x1201)+P4(f16(x1202,x1203,x1201),x1202)+E(x1201,f20(x1202,x1203)) % 0.49/0.61 [121]~P2(x1211)+~P2(x1213)+~P2(x1212)+P4(f13(x1212,x1213,x1211),x1211)+P4(f17(x1212,x1213,x1211),x1213)+E(x1211,f20(x1212,x1213)) % 0.49/0.61 [122]~P2(x1221)+~P2(x1223)+~P2(x1222)+P4(f18(x1222,x1223,x1221),x1221)+P4(f18(x1222,x1223,x1221),x1223)+E(x1221,f19(x1222,x1223)) % 0.49/0.61 [123]~P2(x1231)+~P2(x1233)+~P2(x1232)+P4(f18(x1232,x1233,x1231),x1231)+P4(f18(x1232,x1233,x1231),x1232)+E(x1231,f19(x1232,x1233)) % 0.49/0.61 [125]~P2(x1251)+~P2(x1253)+~P2(x1252)+P4(f13(x1252,x1253,x1251),x1251)+E(x1251,f20(x1252,x1253))+E(f2(f16(x1252,x1253,x1251),f17(x1252,x1253,x1251)),f13(x1252,x1253,x1251)) % 0.49/0.61 [104]~P2(x1044)+~P2(x1043)+~P4(x1041,x1044)+~P4(x1041,x1043)+P4(x1041,x1042)+~E(x1042,f19(x1043,x1044)) % 0.49/0.61 [115]~P4(x1152,a25)+~P4(x1151,a24)+~P4(x1154,a25)+~P4(x1153,a24)+~E(f2(x1151,x1152),f2(a28,a31))+~E(f2(x1153,x1154),f9(a23,a28)) % 0.49/0.61 [128]~P2(x1281)+~P2(x1283)+~P2(x1282)+~P4(f18(x1282,x1283,x1281),x1281)+~P4(f18(x1282,x1283,x1281),x1283)+~P4(f18(x1282,x1283,x1281),x1282)+E(x1281,f19(x1282,x1283)) % 0.49/0.61 [109]~P2(x1094)+~P2(x1093)+~P4(x1096,x1094)+~P4(x1095,x1093)+P4(x1091,x1092)+~E(x1092,f20(x1093,x1094))+~E(f2(x1095,x1096),x1091) % 0.49/0.61 [124]~P2(x1241)+~P2(x1243)+~P2(x1242)+~P4(x1245,x1243)+~P4(x1244,x1242)+~P4(f13(x1242,x1243,x1241),x1241)+E(x1241,f20(x1242,x1243))+~E(f2(x1244,x1245),f13(x1242,x1243,x1241)) % 0.49/0.61 %EqnAxiom % 0.49/0.61 [1]E(x11,x11) % 0.49/0.61 [2]E(x22,x21)+~E(x21,x22) % 0.49/0.61 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.49/0.61 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 0.49/0.61 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 0.49/0.61 [6]~E(x61,x62)+E(f20(x61,x63),f20(x62,x63)) % 0.49/0.61 [7]~E(x71,x72)+E(f20(x73,x71),f20(x73,x72)) % 0.49/0.61 [8]~E(x81,x82)+E(f15(x81,x83,x84,x85),f15(x82,x83,x84,x85)) % 0.49/0.61 [9]~E(x91,x92)+E(f15(x93,x91,x94,x95),f15(x93,x92,x94,x95)) % 0.49/0.61 [10]~E(x101,x102)+E(f15(x103,x104,x101,x105),f15(x103,x104,x102,x105)) % 0.49/0.61 [11]~E(x111,x112)+E(f15(x113,x114,x115,x111),f15(x113,x114,x115,x112)) % 0.49/0.61 [12]~E(x121,x122)+E(f14(x121,x123,x124,x125),f14(x122,x123,x124,x125)) % 0.49/0.61 [13]~E(x131,x132)+E(f14(x133,x131,x134,x135),f14(x133,x132,x134,x135)) % 0.49/0.61 [14]~E(x141,x142)+E(f14(x143,x144,x141,x145),f14(x143,x144,x142,x145)) % 0.49/0.61 [15]~E(x151,x152)+E(f14(x153,x154,x155,x151),f14(x153,x154,x155,x152)) % 0.49/0.61 [16]~E(x161,x162)+E(f9(x161,x163),f9(x162,x163)) % 0.49/0.62 [17]~E(x171,x172)+E(f9(x173,x171),f9(x173,x172)) % 0.49/0.62 [18]~E(x181,x182)+E(f10(x181),f10(x182)) % 0.49/0.62 [19]~E(x191,x192)+E(f18(x191,x193,x194),f18(x192,x193,x194)) % 0.49/0.62 [20]~E(x201,x202)+E(f18(x203,x201,x204),f18(x203,x202,x204)) % 0.49/0.62 [21]~E(x211,x212)+E(f18(x213,x214,x211),f18(x213,x214,x212)) % 0.49/0.62 [22]~E(x221,x222)+E(f13(x221,x223,x224),f13(x222,x223,x224)) % 0.49/0.62 [23]~E(x231,x232)+E(f13(x233,x231,x234),f13(x233,x232,x234)) % 0.49/0.62 [24]~E(x241,x242)+E(f13(x243,x244,x241),f13(x243,x244,x242)) % 0.49/0.62 [25]~E(x251,x252)+E(f4(x251),f4(x252)) % 0.49/0.62 [26]~E(x261,x262)+E(f5(x261),f5(x262)) % 0.49/0.62 [27]~E(x271,x272)+E(f19(x271,x273),f19(x272,x273)) % 0.49/0.62 [28]~E(x281,x282)+E(f19(x283,x281),f19(x283,x282)) % 0.49/0.62 [29]~E(x291,x292)+E(f21(x291),f21(x292)) % 0.49/0.62 [30]~E(x301,x302)+E(f12(x301,x303),f12(x302,x303)) % 0.49/0.62 [31]~E(x311,x312)+E(f12(x313,x311),f12(x313,x312)) % 0.49/0.62 [32]~E(x321,x322)+E(f11(x321,x323),f11(x322,x323)) % 0.49/0.62 [33]~E(x331,x332)+E(f11(x333,x331),f11(x333,x332)) % 0.49/0.62 [34]~E(x341,x342)+E(f17(x341,x343,x344),f17(x342,x343,x344)) % 0.49/0.62 [35]~E(x351,x352)+E(f17(x353,x351,x354),f17(x353,x352,x354)) % 0.49/0.62 [36]~E(x361,x362)+E(f17(x363,x364,x361),f17(x363,x364,x362)) % 0.49/0.62 [37]~E(x371,x372)+E(f16(x371,x373,x374),f16(x372,x373,x374)) % 0.49/0.62 [38]~E(x381,x382)+E(f16(x383,x381,x384),f16(x383,x382,x384)) % 0.49/0.62 [39]~E(x391,x392)+E(f16(x393,x394,x391),f16(x393,x394,x392)) % 0.49/0.62 [40]~P1(x401)+P1(x402)+~E(x401,x402) % 0.49/0.62 [41]P4(x412,x413)+~E(x411,x412)+~P4(x411,x413) % 0.49/0.62 [42]P4(x423,x422)+~E(x421,x422)+~P4(x423,x421) % 0.49/0.62 [43]~P2(x431)+P2(x432)+~E(x431,x432) % 0.49/0.62 [44]~P3(x441)+P3(x442)+~E(x441,x442) % 0.49/0.62 % 0.49/0.62 %------------------------------------------- % 0.49/0.62 cnf(134,plain, % 0.49/0.62 (~P4(x1341,x1342)+~P2(x1343)+~P4(x1341,x1343)+~P2(x1342)+P4(x1341,f19(x1342,x1343))), % 0.49/0.62 inference(equality_inference,[],[104])). % 0.49/0.62 cnf(143,plain, % 0.49/0.62 ($false), % 0.49/0.62 inference(scs_inference,[],[67,69,48,56,52,64,66,68,70,71,2,41,134,115]), % 0.49/0.62 ['proof']). % 0.49/0.62 % SZS output end Proof % 0.49/0.62 % Total time :0.010000s %------------------------------------------------------------------------------