%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : RNG088+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 : n026.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:01 EDT 2024 % Result : Theorem 52.26s 52.69s % Output : CNFRefutation 52.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.10 % Problem : RNG088+2 : TPTP v8.2.0. Released v4.0.0. % 0.08/0.10 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.09/0.30 % Computer : n026.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:32:38 EDT 2024 % 0.09/0.31 % CPUTime : % 0.47/0.55 start to proof:theBenchmark % 52.26/52.67 %------------------------------------------- % 52.26/52.67 % File :CSE---1.7 % 52.26/52.67 % Problem :theBenchmark % 52.26/52.67 % Transform :cnf % 52.26/52.67 % Format :tptp:raw % 52.26/52.67 % Command :java -jar mcs_scs.jar %d %s % 52.26/52.67 % 52.26/52.67 % Result :Theorem 51.780000s % 52.26/52.67 % Output :CNFRefutation 51.780000s % 52.26/52.67 %------------------------------------------- % 52.26/52.68 %------------------------------------------------------------------------------ % 52.26/52.68 % File : RNG088+2 : TPTP v8.2.0. Released v4.0.0. % 52.26/52.68 % Domain : Ring Theory % 52.26/52.68 % Problem : Chinese remainder theorem in a ring 03_03, 01 expansion % 52.26/52.68 % Version : Especial. % 52.26/52.68 % English : % 52.26/52.68 % 52.26/52.68 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 52.26/52.68 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 52.26/52.68 % Source : [Pas08] % 52.26/52.68 % Names : chines_03_03.01 [Pas08] % 52.26/52.68 % 52.26/52.68 % Status : Theorem % 52.26/52.68 % Rating : 0.17 v8.2.0, 0.14 v8.1.0, 0.08 v7.5.0, 0.09 v7.4.0, 0.10 v7.3.0, 0.14 v7.1.0, 0.17 v7.0.0, 0.07 v6.4.0, 0.12 v6.1.0, 0.20 v6.0.0, 0.17 v5.5.0, 0.26 v5.4.0, 0.32 v5.3.0, 0.33 v5.2.0, 0.25 v5.1.0, 0.33 v5.0.0, 0.38 v4.1.0, 0.48 v4.0.1, 0.83 v4.0.0 % 52.26/52.68 % Syntax : Number of formulae : 29 ( 3 unt; 3 def) % 52.26/52.68 % Number of atoms : 117 ( 28 equ) % 52.26/52.68 % Maximal formula atoms : 14 ( 4 avg) % 52.26/52.68 % Number of connectives : 89 ( 1 ~; 1 |; 48 &) % 52.26/52.68 % ( 5 <=>; 34 =>; 0 <=; 0 <~>) % 52.26/52.68 % Maximal formula depth : 13 ( 5 avg) % 52.26/52.68 % Maximal term depth : 3 ( 1 avg) % 52.26/52.68 % Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty) % 52.26/52.68 % Number of functors : 16 ( 16 usr; 11 con; 0-2 aty) % 52.26/52.68 % Number of variables : 57 ( 51 !; 6 ?) % 52.26/52.68 % SPC : FOF_THM_RFO_SEQ % 52.26/52.68 % 52.26/52.68 % Comments : Problem generated by the SAD system [VLP07] % 52.26/52.68 %------------------------------------------------------------------------------ % 52.26/52.68 fof(mElmSort,axiom, % 52.26/52.68 ! [W0] : % 52.26/52.68 ( aElement0(W0) % 52.26/52.68 => $true ) ). % 52.26/52.68 % 52.26/52.68 fof(mSortsC,axiom, % 52.26/52.68 aElement0(sz00) ). % 52.26/52.68 % 52.26/52.68 fof(mSortsC_01,axiom, % 52.26/52.68 aElement0(sz10) ). % 52.26/52.68 % 52.26/52.68 fof(mSortsU,axiom, % 52.26/52.68 ! [W0] : % 52.26/52.68 ( aElement0(W0) % 52.26/52.68 => aElement0(smndt0(W0)) ) ). % 52.26/52.68 % 52.26/52.68 fof(mSortsB,axiom, % 52.26/52.68 ! [W0,W1] : % 52.26/52.68 ( ( aElement0(W0) % 52.26/52.68 & aElement0(W1) ) % 52.26/52.68 => aElement0(sdtpldt0(W0,W1)) ) ). % 52.26/52.68 % 52.26/52.68 fof(mSortsB_02,axiom, % 52.26/52.68 ! [W0,W1] : % 52.26/52.68 ( ( aElement0(W0) % 52.26/52.68 & aElement0(W1) ) % 52.26/52.68 => aElement0(sdtasdt0(W0,W1)) ) ). % 52.26/52.68 % 52.26/52.68 fof(mAddComm,axiom, % 52.26/52.68 ! [W0,W1] : % 52.26/52.68 ( ( aElement0(W0) % 52.26/52.68 & aElement0(W1) ) % 52.26/52.68 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 52.26/52.68 % 52.26/52.68 fof(mAddAsso,axiom, % 52.26/52.68 ! [W0,W1,W2] : % 52.26/52.68 ( ( aElement0(W0) % 52.26/52.68 & aElement0(W1) % 52.26/52.68 & aElement0(W2) ) % 52.26/52.68 => sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) ). % 52.26/52.68 % 52.26/52.68 fof(mAddZero,axiom, % 52.26/52.68 ! [W0] : % 52.26/52.68 ( aElement0(W0) % 52.26/52.68 => ( sdtpldt0(W0,sz00) = W0 % 52.26/52.68 & W0 = sdtpldt0(sz00,W0) ) ) ). % 52.26/52.68 % 52.26/52.68 fof(mAddInvr,axiom, % 52.26/52.68 ! [W0] : % 52.26/52.68 ( aElement0(W0) % 52.26/52.68 => ( sdtpldt0(W0,smndt0(W0)) = sz00 % 52.26/52.68 & sz00 = sdtpldt0(smndt0(W0),W0) ) ) ). % 52.26/52.68 % 52.26/52.68 fof(mMulComm,axiom, % 52.26/52.68 ! [W0,W1] : % 52.26/52.68 ( ( aElement0(W0) % 52.26/52.68 & aElement0(W1) ) % 52.26/52.68 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 52.26/52.68 % 52.26/52.68 fof(mMulAsso,axiom, % 52.26/52.68 ! [W0,W1,W2] : % 52.26/52.68 ( ( aElement0(W0) % 52.26/52.68 & aElement0(W1) % 52.26/52.68 & aElement0(W2) ) % 52.26/52.68 => sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) ). % 52.26/52.68 % 52.26/52.68 fof(mMulUnit,axiom, % 52.26/52.68 ! [W0] : % 52.26/52.68 ( aElement0(W0) % 52.26/52.68 => ( sdtasdt0(W0,sz10) = W0 % 52.26/52.68 & W0 = sdtasdt0(sz10,W0) ) ) ). % 52.26/52.68 % 52.26/52.68 fof(mAMDistr,axiom, % 52.26/52.68 ! [W0,W1,W2] : % 52.26/52.68 ( ( aElement0(W0) % 52.26/52.68 & aElement0(W1) % 52.26/52.68 & aElement0(W2) ) % 52.26/52.68 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 52.26/52.68 & sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ). % 52.26/52.68 % 52.26/52.68 fof(mMulMnOne,axiom, % 52.26/52.68 ! [W0] : % 52.26/52.68 ( aElement0(W0) % 52.26/52.68 => ( sdtasdt0(smndt0(sz10),W0) = smndt0(W0) % 52.26/52.68 & smndt0(W0) = sdtasdt0(W0,smndt0(sz10)) ) ) ). % 52.26/52.68 % 52.26/52.68 fof(mMulZero,axiom, % 52.26/52.68 ! [W0] : % 52.26/52.68 ( aElement0(W0) % 52.26/52.68 => ( sdtasdt0(W0,sz00) = sz00 % 52.26/52.68 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 52.26/52.68 % 52.26/52.68 fof(mCancel,axiom, % 52.26/52.68 ! [W0,W1] : % 52.26/52.68 ( ( aElement0(W0) % 52.26/52.68 & aElement0(W1) ) % 52.26/52.68 => ( sdtasdt0(W0,W1) = sz00 % 52.26/52.68 => ( W0 = sz00 % 52.26/52.68 | W1 = sz00 ) ) ) ). % 52.26/52.68 % 52.26/52.68 fof(mUnNeZr,axiom, % 52.26/52.68 sz10 != sz00 ). % 52.26/52.68 % 52.26/52.68 fof(mSetSort,axiom, % 52.26/52.68 ! [W0] : % 52.26/52.68 ( aSet0(W0) % 52.26/52.68 => $true ) ). % 52.26/52.68 % 52.26/52.68 fof(mEOfElem,axiom, % 52.26/52.68 ! [W0] : % 52.26/52.68 ( aSet0(W0) % 52.26/52.68 => ! [W1] : % 52.26/52.68 ( aElementOf0(W1,W0) % 52.26/52.68 => aElement0(W1) ) ) ). % 52.26/52.68 % 52.26/52.68 fof(mSetEq,axiom, % 52.26/52.68 ! [W0,W1] : % 52.26/52.68 ( ( aSet0(W0) % 52.26/52.68 & aSet0(W1) ) % 52.26/52.68 => ( ( ! [W2] : % 52.26/52.68 ( aElementOf0(W2,W0) % 52.26/52.68 => aElementOf0(W2,W1) ) % 52.26/52.68 & ! [W2] : % 52.26/52.68 ( aElementOf0(W2,W1) % 52.26/52.68 => aElementOf0(W2,W0) ) ) % 52.26/52.68 => W0 = W1 ) ) ). % 52.26/52.68 % 52.26/52.68 fof(mDefSSum,definition, % 52.26/52.68 ! [W0,W1] : % 52.26/52.68 ( ( aSet0(W0) % 52.26/52.68 & aSet0(W1) ) % 52.26/52.68 => ! [W2] : % 52.26/52.68 ( W2 = sdtpldt1(W0,W1) % 52.26/52.68 <=> ( aSet0(W2) % 52.26/52.68 & ! [W3] : % 52.26/52.69 ( aElementOf0(W3,W2) % 52.26/52.69 <=> ? [W4,W5] : % 52.26/52.69 ( aElementOf0(W4,W0) % 52.26/52.69 & aElementOf0(W5,W1) % 52.26/52.69 & sdtpldt0(W4,W5) = W3 ) ) ) ) ) ). % 52.26/52.69 % 52.26/52.69 fof(mDefSInt,definition, % 52.26/52.69 ! [W0,W1] : % 52.26/52.69 ( ( aSet0(W0) % 52.26/52.69 & aSet0(W1) ) % 52.26/52.69 => ! [W2] : % 52.26/52.69 ( W2 = sdtasasdt0(W0,W1) % 52.26/52.69 <=> ( aSet0(W2) % 52.26/52.69 & ! [W3] : % 52.26/52.69 ( aElementOf0(W3,W2) % 52.26/52.69 <=> ( aElementOf0(W3,W0) % 52.26/52.69 & aElementOf0(W3,W1) ) ) ) ) ) ). % 52.26/52.69 % 52.26/52.69 fof(mDefIdeal,definition, % 52.26/52.69 ! [W0] : % 52.26/52.69 ( aIdeal0(W0) % 52.26/52.69 <=> ( aSet0(W0) % 52.26/52.69 & ! [W1] : % 52.26/52.69 ( aElementOf0(W1,W0) % 52.26/52.69 => ( ! [W2] : % 52.26/52.69 ( aElementOf0(W2,W0) % 52.26/52.69 => aElementOf0(sdtpldt0(W1,W2),W0) ) % 52.26/52.69 & ! [W2] : % 52.26/52.69 ( aElement0(W2) % 52.26/52.69 => aElementOf0(sdtasdt0(W2,W1),W0) ) ) ) ) ) ). % 52.26/52.69 % 52.26/52.69 fof(m__870,hypothesis, % 52.26/52.69 ( aSet0(xI) % 52.26/52.69 & ! [W0] : % 52.26/52.69 ( aElementOf0(W0,xI) % 52.26/52.69 => ( ! [W1] : % 52.26/52.69 ( aElementOf0(W1,xI) % 52.26/52.69 => aElementOf0(sdtpldt0(W0,W1),xI) ) % 52.26/52.69 & ! [W1] : % 52.26/52.69 ( aElement0(W1) % 52.26/52.69 => aElementOf0(sdtasdt0(W1,W0),xI) ) ) ) % 52.26/52.69 & aIdeal0(xI) % 52.26/52.69 & aSet0(xJ) % 52.26/52.69 & ! [W0] : % 52.26/52.69 ( aElementOf0(W0,xJ) % 52.26/52.69 => ( ! [W1] : % 52.26/52.69 ( aElementOf0(W1,xJ) % 52.26/52.69 => aElementOf0(sdtpldt0(W0,W1),xJ) ) % 52.26/52.69 & ! [W1] : % 52.26/52.69 ( aElement0(W1) % 52.26/52.69 => aElementOf0(sdtasdt0(W1,W0),xJ) ) ) ) % 52.26/52.69 & aIdeal0(xJ) ) ). % 52.26/52.69 % 52.26/52.69 fof(m__901,hypothesis, % 52.26/52.69 ( ? [W0,W1] : % 52.26/52.69 ( aElementOf0(W0,xI) % 52.26/52.69 & aElementOf0(W1,xJ) % 52.26/52.69 & sdtpldt0(W0,W1) = xx ) % 52.26/52.69 & aElementOf0(xx,sdtpldt1(xI,xJ)) % 52.26/52.69 & ? [W0,W1] : % 52.26/52.69 ( aElementOf0(W0,xI) % 52.26/52.69 & aElementOf0(W1,xJ) % 52.26/52.69 & sdtpldt0(W0,W1) = xy ) % 52.26/52.69 & aElementOf0(xy,sdtpldt1(xI,xJ)) % 52.26/52.69 & aElement0(xz) ) ). % 52.26/52.69 % 52.26/52.69 fof(m__934,hypothesis, % 52.26/52.69 ( aElementOf0(xk,xI) % 52.26/52.69 & aElementOf0(xl,xJ) % 52.26/52.69 & xx = sdtpldt0(xk,xl) ) ). % 52.26/52.69 % 52.26/52.69 fof(m__967,hypothesis, % 52.26/52.69 ( aElementOf0(xm,xI) % 52.26/52.69 & aElementOf0(xn,xJ) % 52.26/52.69 & xy = sdtpldt0(xm,xn) ) ). % 52.26/52.69 % 52.26/52.69 fof(m__,conjecture, % 52.26/52.69 ( aElementOf0(sdtpldt0(xk,xm),xI) % 52.26/52.69 & aElementOf0(sdtpldt0(xl,xn),xJ) ) ). % 52.26/52.69 % 52.26/52.69 %------------------------------------------------------------------------------ % 52.26/52.69 %------------------------------------------- % 52.26/52.69 % Proof found % 52.26/52.69 % SZS status Theorem for theBenchmark % 52.26/52.69 % SZS output start Proof % 52.26/52.69 %ClaNum:120(EqnAxiom:44) % 52.26/52.69 %VarNum:408(SingletonVarNum:122) % 52.26/52.69 %MaxLitNum:8 % 52.26/52.69 %MaxfuncDepth:2 % 52.26/52.69 %SharedTerms:47 % 52.26/52.69 %goalClause: 101 % 52.26/52.69 [45]P1(a1) % 52.26/52.69 [46]P1(a22) % 52.26/52.69 [47]P1(a23) % 52.26/52.69 [48]P2(a24) % 52.26/52.69 [49]P2(a25) % 52.26/52.69 [50]P3(a24) % 52.26/52.69 [51]P3(a25) % 52.26/52.69 [56]P4(a26,a24) % 52.26/52.69 [57]P4(a27,a25) % 52.26/52.69 [58]P4(a29,a24) % 52.26/52.69 [59]P4(a30,a25) % 52.26/52.69 [60]P4(a3,a24) % 52.26/52.69 [61]P4(a6,a25) % 52.26/52.69 [62]P4(a7,a24) % 52.26/52.69 [63]P4(a8,a25) % 52.26/52.69 [66]~E(a1,a22) % 52.26/52.69 [52]E(f2(a26,a27),a28) % 52.26/52.69 [53]E(f2(a29,a30),a31) % 52.26/52.69 [54]E(f2(a3,a6),a28) % 52.26/52.69 [55]E(f2(a7,a8),a31) % 52.26/52.69 [64]P4(a28,f20(a24,a25)) % 52.26/52.69 [65]P4(a31,f20(a24,a25)) % 52.26/52.69 [101]~P4(f2(a26,a29),a24)+~P4(f2(a27,a30),a25) % 52.26/52.69 [67]~P3(x671)+P2(x671) % 52.26/52.69 [68]~P1(x681)+P1(f21(x681)) % 52.26/52.69 [69]~P1(x691)+E(f9(a1,x691),a1) % 52.26/52.69 [70]~P1(x701)+E(f9(x701,a1),a1) % 52.26/52.69 [71]~P1(x711)+E(f2(a1,x711),x711) % 52.26/52.69 [72]~P1(x721)+E(f9(a22,x721),x721) % 52.26/52.69 [73]~P1(x731)+E(f2(x731,a1),x731) % 52.26/52.69 [74]~P1(x741)+E(f9(x741,a22),x741) % 52.26/52.69 [75]~P1(x751)+E(f2(f21(x751),x751),a1) % 52.26/52.69 [76]~P1(x761)+E(f2(x761,f21(x761)),a1) % 52.26/52.69 [77]~P1(x771)+E(f9(x771,f21(a22)),f21(x771)) % 52.26/52.69 [78]~P1(x781)+E(f9(f21(a22),x781),f21(x781)) % 52.26/52.69 [79]~P2(x791)+P3(x791)+P4(f10(x791),x791) % 52.26/52.69 [80]~P4(x801,x802)+P1(x801)+~P2(x802) % 52.26/52.69 [82]~P1(x822)+~P1(x821)+E(f2(x821,x822),f2(x822,x821)) % 52.26/52.69 [83]~P1(x832)+~P1(x831)+E(f9(x831,x832),f9(x832,x831)) % 52.26/52.69 [87]~P1(x872)+~P1(x871)+P1(f2(x871,x872)) % 52.26/52.69 [88]~P1(x882)+~P1(x881)+P1(f9(x881,x882)) % 52.26/52.69 [89]~P1(x891)+~P4(x892,a24)+P4(f9(x891,x892),a24) % 52.26/52.69 [90]~P1(x901)+~P4(x902,a25)+P4(f9(x901,x902),a25) % 52.26/52.69 [94]~P4(x941,a24)+~P4(x942,a24)+P4(f2(x941,x942),a24) % 52.26/52.69 [95]~P4(x951,a25)+~P4(x952,a25)+P4(f2(x951,x952),a25) % 52.26/52.69 [86]~P2(x861)+P3(x861)+P4(f5(x861),x861)+P1(f4(x861)) % 52.26/52.69 [105]~P2(x1051)+P3(x1051)+P1(f4(x1051))+~P4(f2(f10(x1051),f5(x1051)),x1051) % 52.26/52.69 [108]~P2(x1081)+P3(x1081)+P4(f5(x1081),x1081)+~P4(f9(f4(x1081),f10(x1081)),x1081) % 52.26/52.69 [110]~P2(x1101)+P3(x1101)+~P4(f2(f10(x1101),f5(x1101)),x1101)+~P4(f9(f4(x1101),f10(x1101)),x1101) % 52.26/52.69 [84]~P2(x843)+~P2(x842)+P2(x841)+~E(x841,f20(x842,x843)) % 52.40/52.69 [85]~P2(x853)+~P2(x852)+P2(x851)+~E(x851,f19(x852,x853)) % 52.40/52.69 [93]~P1(x931)+~P3(x933)+~P4(x932,x933)+P4(f9(x931,x932),x933) % 52.40/52.69 [96]~P3(x963)+~P4(x961,x963)+~P4(x962,x963)+P4(f2(x961,x962),x963) % 52.40/52.69 [99]~P1(x993)+~P1(x992)+~P1(x991)+E(f2(f2(x991,x992),x993),f2(x991,f2(x992,x993))) % 52.40/52.69 [100]~P1(x1003)+~P1(x1002)+~P1(x1001)+E(f9(f9(x1001,x1002),x1003),f9(x1001,f9(x1002,x1003))) % 52.40/52.69 [106]~P1(x1063)+~P1(x1062)+~P1(x1061)+E(f2(f9(x1061,x1062),f9(x1061,x1063)),f9(x1061,f2(x1062,x1063))) % 52.40/52.69 [107]~P1(x1072)+~P1(x1073)+~P1(x1071)+E(f2(f9(x1071,x1072),f9(x1073,x1072)),f9(f2(x1071,x1073),x1072)) % 52.40/52.69 [81]~P1(x811)+~P1(x812)+E(x811,a1)+E(x812,a1)+~E(f9(x812,x811),a1) % 52.40/52.69 [97]~P2(x972)+~P2(x971)+E(x971,x972)+P4(f11(x971,x972),x971)+P4(f12(x971,x972),x972) % 52.40/52.69 [102]~P2(x1022)+~P2(x1021)+E(x1021,x1022)+P4(f11(x1021,x1022),x1021)+~P4(f12(x1021,x1022),x1021) % 52.40/52.69 [103]~P2(x1032)+~P2(x1031)+E(x1031,x1032)+P4(f12(x1031,x1032),x1032)+~P4(f11(x1031,x1032),x1032) % 52.40/52.69 [109]~P2(x1092)+~P2(x1091)+E(x1091,x1092)+~P4(f11(x1091,x1092),x1092)+~P4(f12(x1091,x1092),x1091) % 52.40/52.69 [91]~P2(x914)+~P2(x912)+~P4(x911,x913)+P4(x911,x912)+~E(x913,f19(x914,x912)) % 52.40/52.69 [92]~P2(x924)+~P2(x922)+~P4(x921,x923)+P4(x921,x922)+~E(x923,f19(x922,x924)) % 52.40/52.69 [117]~P2(x1172)+~P2(x1171)+~P4(x1174,x1173)+~E(x1173,f20(x1171,x1172))+P4(f14(x1171,x1172,x1173,x1174),x1171) % 52.40/52.69 [118]~P2(x1182)+~P2(x1181)+~P4(x1184,x1183)+~E(x1183,f20(x1181,x1182))+P4(f15(x1181,x1182,x1183,x1184),x1182) % 52.40/52.69 [120]~P2(x1202)+~P2(x1201)+~P4(x1204,x1203)+~E(x1203,f20(x1201,x1202))+E(f2(f14(x1201,x1202,x1203,x1204),f15(x1201,x1202,x1203,x1204)),x1204) % 52.40/52.69 [111]~P2(x1111)+~P2(x1113)+~P2(x1112)+P4(f13(x1112,x1113,x1111),x1111)+P4(f16(x1112,x1113,x1111),x1112)+E(x1111,f20(x1112,x1113)) % 52.40/52.69 [112]~P2(x1121)+~P2(x1123)+~P2(x1122)+P4(f13(x1122,x1123,x1121),x1121)+P4(f17(x1122,x1123,x1121),x1123)+E(x1121,f20(x1122,x1123)) % 52.40/52.69 [113]~P2(x1131)+~P2(x1133)+~P2(x1132)+P4(f18(x1132,x1133,x1131),x1131)+P4(f18(x1132,x1133,x1131),x1133)+E(x1131,f19(x1132,x1133)) % 52.40/52.69 [114]~P2(x1141)+~P2(x1143)+~P2(x1142)+P4(f18(x1142,x1143,x1141),x1141)+P4(f18(x1142,x1143,x1141),x1142)+E(x1141,f19(x1142,x1143)) % 52.40/52.69 [116]~P2(x1161)+~P2(x1163)+~P2(x1162)+P4(f13(x1162,x1163,x1161),x1161)+E(x1161,f20(x1162,x1163))+E(f2(f16(x1162,x1163,x1161),f17(x1162,x1163,x1161)),f13(x1162,x1163,x1161)) % 52.40/52.69 [98]~P2(x984)+~P2(x983)+~P4(x981,x984)+~P4(x981,x983)+P4(x981,x982)+~E(x982,f19(x983,x984)) % 52.40/52.69 [119]~P2(x1191)+~P2(x1193)+~P2(x1192)+~P4(f18(x1192,x1193,x1191),x1191)+~P4(f18(x1192,x1193,x1191),x1193)+~P4(f18(x1192,x1193,x1191),x1192)+E(x1191,f19(x1192,x1193)) % 52.40/52.69 [104]~P2(x1044)+~P2(x1043)+~P4(x1046,x1044)+~P4(x1045,x1043)+P4(x1041,x1042)+~E(x1042,f20(x1043,x1044))+~E(f2(x1045,x1046),x1041) % 52.40/52.69 [115]~P2(x1151)+~P2(x1153)+~P2(x1152)+~P4(x1155,x1153)+~P4(x1154,x1152)+~P4(f13(x1152,x1153,x1151),x1151)+E(x1151,f20(x1152,x1153))+~E(f2(x1154,x1155),f13(x1152,x1153,x1151)) % 52.40/52.69 %EqnAxiom % 52.40/52.69 [1]E(x11,x11) % 52.40/52.69 [2]E(x22,x21)+~E(x21,x22) % 52.40/52.69 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 52.40/52.69 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 52.40/52.69 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 52.40/52.69 [6]~E(x61,x62)+E(f20(x61,x63),f20(x62,x63)) % 52.40/52.69 [7]~E(x71,x72)+E(f20(x73,x71),f20(x73,x72)) % 52.40/52.69 [8]~E(x81,x82)+E(f15(x81,x83,x84,x85),f15(x82,x83,x84,x85)) % 52.40/52.69 [9]~E(x91,x92)+E(f15(x93,x91,x94,x95),f15(x93,x92,x94,x95)) % 52.40/52.69 [10]~E(x101,x102)+E(f15(x103,x104,x101,x105),f15(x103,x104,x102,x105)) % 52.40/52.69 [11]~E(x111,x112)+E(f15(x113,x114,x115,x111),f15(x113,x114,x115,x112)) % 52.40/52.69 [12]~E(x121,x122)+E(f14(x121,x123,x124,x125),f14(x122,x123,x124,x125)) % 52.40/52.69 [13]~E(x131,x132)+E(f14(x133,x131,x134,x135),f14(x133,x132,x134,x135)) % 52.40/52.69 [14]~E(x141,x142)+E(f14(x143,x144,x141,x145),f14(x143,x144,x142,x145)) % 52.40/52.69 [15]~E(x151,x152)+E(f14(x153,x154,x155,x151),f14(x153,x154,x155,x152)) % 52.40/52.69 [16]~E(x161,x162)+E(f13(x161,x163,x164),f13(x162,x163,x164)) % 52.40/52.69 [17]~E(x171,x172)+E(f13(x173,x171,x174),f13(x173,x172,x174)) % 52.40/52.69 [18]~E(x181,x182)+E(f13(x183,x184,x181),f13(x183,x184,x182)) % 52.40/52.69 [19]~E(x191,x192)+E(f16(x191,x193,x194),f16(x192,x193,x194)) % 52.40/52.69 [20]~E(x201,x202)+E(f16(x203,x201,x204),f16(x203,x202,x204)) % 52.40/52.69 [21]~E(x211,x212)+E(f16(x213,x214,x211),f16(x213,x214,x212)) % 52.40/52.69 [22]~E(x221,x222)+E(f21(x221),f21(x222)) % 52.40/52.69 [23]~E(x231,x232)+E(f9(x231,x233),f9(x232,x233)) % 52.40/52.69 [24]~E(x241,x242)+E(f9(x243,x241),f9(x243,x242)) % 52.40/52.69 [25]~E(x251,x252)+E(f19(x251,x253),f19(x252,x253)) % 52.40/52.69 [26]~E(x261,x262)+E(f19(x263,x261),f19(x263,x262)) % 52.40/52.69 [27]~E(x271,x272)+E(f18(x271,x273,x274),f18(x272,x273,x274)) % 52.40/52.69 [28]~E(x281,x282)+E(f18(x283,x281,x284),f18(x283,x282,x284)) % 52.40/52.69 [29]~E(x291,x292)+E(f18(x293,x294,x291),f18(x293,x294,x292)) % 52.40/52.69 [30]~E(x301,x302)+E(f17(x301,x303,x304),f17(x302,x303,x304)) % 52.40/52.69 [31]~E(x311,x312)+E(f17(x313,x311,x314),f17(x313,x312,x314)) % 52.40/52.69 [32]~E(x321,x322)+E(f17(x323,x324,x321),f17(x323,x324,x322)) % 52.40/52.69 [33]~E(x331,x332)+E(f12(x331,x333),f12(x332,x333)) % 52.40/52.69 [34]~E(x341,x342)+E(f12(x343,x341),f12(x343,x342)) % 52.40/52.69 [35]~E(x351,x352)+E(f5(x351),f5(x352)) % 52.40/52.69 [36]~E(x361,x362)+E(f4(x361),f4(x362)) % 52.40/52.69 [37]~E(x371,x372)+E(f11(x371,x373),f11(x372,x373)) % 52.40/52.69 [38]~E(x381,x382)+E(f11(x383,x381),f11(x383,x382)) % 52.40/52.69 [39]~E(x391,x392)+E(f10(x391),f10(x392)) % 52.40/52.69 [40]~P1(x401)+P1(x402)+~E(x401,x402) % 52.40/52.69 [41]P4(x412,x413)+~E(x411,x412)+~P4(x411,x413) % 52.40/52.69 [42]P4(x423,x422)+~E(x421,x422)+~P4(x423,x421) % 52.40/52.69 [43]~P2(x431)+P2(x432)+~E(x431,x432) % 52.40/52.69 [44]~P3(x441)+P3(x442)+~E(x441,x442) % 52.40/52.69 % 52.40/52.69 %------------------------------------------- % 52.40/52.69 cnf(123,plain, % 52.40/52.69 (P4(x1231,x1232)+~P2(x1233)+~P2(x1232)+~P4(x1231,f19(x1233,x1232))), % 52.40/52.69 inference(equality_inference,[],[91])). % 52.40/52.69 cnf(414,plain, % 52.40/52.69 (~P4(x4141,f19(a25,a25))+P4(x4141,a25)), % 52.40/52.69 inference(scs_inference,[],[55,49,44,123])). % 52.40/52.69 cnf(3868,plain, % 52.40/52.69 (~P4(f2(a27,a30),a25)), % 52.40/52.69 inference(scs_inference,[],[56,58,101,94])). % 52.40/52.69 cnf(3871,plain, % 52.40/52.69 ($false), % 52.40/52.69 inference(scs_inference,[],[3868,57,59,414,95]), % 52.40/52.69 ['proof']). % 52.40/52.69 % SZS output end Proof % 52.40/52.69 % Total time :51.780000s %------------------------------------------------------------------------------