%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : RNG086+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 : n010.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 0.57s 0.63s % Output : CNFRefutation 0.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : RNG086+2 : TPTP v8.2.0. Released v4.0.0. % 0.10/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n010.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Tue Jun 18 13:39:54 EDT 2024 % 0.13/0.33 % CPUTime : % 0.19/0.57 start to proof:theBenchmark % 0.56/0.62 %------------------------------------------- % 0.56/0.62 % File :CSE---1.7 % 0.56/0.62 % Problem :theBenchmark % 0.56/0.62 % Transform :cnf % 0.56/0.62 % Format :tptp:raw % 0.57/0.62 % Command :java -jar mcs_scs.jar %d %s % 0.57/0.62 % 0.57/0.62 % Result :Theorem 0.010000s % 0.57/0.62 % Output :CNFRefutation 0.010000s % 0.57/0.62 %------------------------------------------- % 0.57/0.62 %------------------------------------------------------------------------------ % 0.57/0.62 % File : RNG086+2 : TPTP v8.2.0. Released v4.0.0. % 0.57/0.62 % Domain : Ring Theory % 0.57/0.62 % Problem : Chinese remainder theorem in a ring 03_01, 01 expansion % 0.57/0.62 % Version : Especial. % 0.57/0.62 % English : % 0.57/0.62 % 0.57/0.62 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 0.57/0.62 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 0.57/0.62 % Source : [Pas08] % 0.57/0.63 % Names : chines_03_01.01 [Pas08] % 0.57/0.63 % 0.57/0.63 % Status : Theorem % 0.57/0.63 % Rating : 0.11 v8.1.0, 0.06 v7.4.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.07 v6.4.0, 0.12 v6.3.0, 0.04 v6.1.0, 0.10 v6.0.0, 0.13 v5.5.0, 0.19 v5.4.0, 0.25 v5.3.0, 0.26 v5.2.0, 0.10 v5.1.0, 0.19 v5.0.0, 0.25 v4.1.0, 0.35 v4.0.1, 0.78 v4.0.0 % 0.57/0.63 % Syntax : Number of formulae : 27 ( 3 unt; 3 def) % 0.57/0.63 % Number of atoms : 112 ( 27 equ) % 0.57/0.63 % Maximal formula atoms : 14 ( 4 avg) % 0.57/0.63 % Number of connectives : 86 ( 1 ~; 1 |; 45 &) % 0.57/0.63 % ( 5 <=>; 34 =>; 0 <=; 0 <~>) % 0.57/0.63 % Maximal formula depth : 13 ( 6 avg) % 0.57/0.63 % Maximal term depth : 3 ( 1 avg) % 0.57/0.63 % Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty) % 0.57/0.63 % Number of functors : 12 ( 12 usr; 7 con; 0-2 aty) % 0.57/0.63 % Number of variables : 59 ( 51 !; 8 ?) % 0.57/0.63 % SPC : FOF_THM_RFO_SEQ % 0.57/0.63 % 0.57/0.63 % Comments : Problem generated by the SAD system [VLP07] % 0.57/0.63 %------------------------------------------------------------------------------ % 0.57/0.63 fof(mElmSort,axiom, % 0.57/0.63 ! [W0] : % 0.57/0.63 ( aElement0(W0) % 0.57/0.63 => $true ) ). % 0.57/0.63 % 0.57/0.63 fof(mSortsC,axiom, % 0.57/0.63 aElement0(sz00) ). % 0.57/0.63 % 0.57/0.63 fof(mSortsC_01,axiom, % 0.57/0.63 aElement0(sz10) ). % 0.57/0.63 % 0.57/0.63 fof(mSortsU,axiom, % 0.57/0.63 ! [W0] : % 0.57/0.63 ( aElement0(W0) % 0.57/0.63 => aElement0(smndt0(W0)) ) ). % 0.57/0.63 % 0.57/0.63 fof(mSortsB,axiom, % 0.57/0.63 ! [W0,W1] : % 0.57/0.63 ( ( aElement0(W0) % 0.57/0.63 & aElement0(W1) ) % 0.57/0.63 => aElement0(sdtpldt0(W0,W1)) ) ). % 0.57/0.63 % 0.57/0.63 fof(mSortsB_02,axiom, % 0.57/0.63 ! [W0,W1] : % 0.57/0.63 ( ( aElement0(W0) % 0.57/0.63 & aElement0(W1) ) % 0.57/0.63 => aElement0(sdtasdt0(W0,W1)) ) ). % 0.57/0.63 % 0.57/0.63 fof(mAddComm,axiom, % 0.57/0.63 ! [W0,W1] : % 0.57/0.63 ( ( aElement0(W0) % 0.57/0.63 & aElement0(W1) ) % 0.57/0.63 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 0.57/0.63 % 0.57/0.63 fof(mAddAsso,axiom, % 0.57/0.63 ! [W0,W1,W2] : % 0.57/0.63 ( ( aElement0(W0) % 0.57/0.63 & aElement0(W1) % 0.57/0.63 & aElement0(W2) ) % 0.57/0.63 => sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) ). % 0.57/0.63 % 0.57/0.63 fof(mAddZero,axiom, % 0.57/0.63 ! [W0] : % 0.57/0.63 ( aElement0(W0) % 0.57/0.63 => ( sdtpldt0(W0,sz00) = W0 % 0.57/0.63 & W0 = sdtpldt0(sz00,W0) ) ) ). % 0.57/0.63 % 0.57/0.63 fof(mAddInvr,axiom, % 0.57/0.63 ! [W0] : % 0.57/0.63 ( aElement0(W0) % 0.57/0.63 => ( sdtpldt0(W0,smndt0(W0)) = sz00 % 0.57/0.63 & sz00 = sdtpldt0(smndt0(W0),W0) ) ) ). % 0.57/0.63 % 0.57/0.63 fof(mMulComm,axiom, % 0.57/0.63 ! [W0,W1] : % 0.57/0.63 ( ( aElement0(W0) % 0.57/0.63 & aElement0(W1) ) % 0.57/0.63 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 0.57/0.63 % 0.57/0.63 fof(mMulAsso,axiom, % 0.57/0.63 ! [W0,W1,W2] : % 0.57/0.63 ( ( aElement0(W0) % 0.57/0.63 & aElement0(W1) % 0.57/0.63 & aElement0(W2) ) % 0.57/0.63 => sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) ). % 0.57/0.63 % 0.57/0.63 fof(mMulUnit,axiom, % 0.57/0.63 ! [W0] : % 0.57/0.63 ( aElement0(W0) % 0.57/0.63 => ( sdtasdt0(W0,sz10) = W0 % 0.57/0.63 & W0 = sdtasdt0(sz10,W0) ) ) ). % 0.57/0.63 % 0.57/0.63 fof(mAMDistr,axiom, % 0.57/0.63 ! [W0,W1,W2] : % 0.57/0.63 ( ( aElement0(W0) % 0.57/0.63 & aElement0(W1) % 0.57/0.63 & aElement0(W2) ) % 0.57/0.63 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 0.57/0.63 & sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ). % 0.57/0.63 % 0.57/0.63 fof(mMulMnOne,axiom, % 0.57/0.63 ! [W0] : % 0.57/0.63 ( aElement0(W0) % 0.57/0.63 => ( sdtasdt0(smndt0(sz10),W0) = smndt0(W0) % 0.57/0.63 & smndt0(W0) = sdtasdt0(W0,smndt0(sz10)) ) ) ). % 0.57/0.63 % 0.57/0.63 fof(mMulZero,axiom, % 0.57/0.63 ! [W0] : % 0.57/0.63 ( aElement0(W0) % 0.57/0.63 => ( sdtasdt0(W0,sz00) = sz00 % 0.57/0.63 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 0.57/0.63 % 0.57/0.63 fof(mCancel,axiom, % 0.57/0.63 ! [W0,W1] : % 0.57/0.63 ( ( aElement0(W0) % 0.57/0.63 & aElement0(W1) ) % 0.57/0.63 => ( sdtasdt0(W0,W1) = sz00 % 0.57/0.63 => ( W0 = sz00 % 0.57/0.63 | W1 = sz00 ) ) ) ). % 0.57/0.63 % 0.57/0.63 fof(mUnNeZr,axiom, % 0.57/0.63 sz10 != sz00 ). % 0.57/0.63 % 0.57/0.63 fof(mSetSort,axiom, % 0.57/0.63 ! [W0] : % 0.57/0.63 ( aSet0(W0) % 0.57/0.63 => $true ) ). % 0.57/0.63 % 0.57/0.63 fof(mEOfElem,axiom, % 0.57/0.63 ! [W0] : % 0.57/0.63 ( aSet0(W0) % 0.57/0.63 => ! [W1] : % 0.57/0.63 ( aElementOf0(W1,W0) % 0.57/0.63 => aElement0(W1) ) ) ). % 0.57/0.63 % 0.57/0.63 fof(mSetEq,axiom, % 0.57/0.63 ! [W0,W1] : % 0.57/0.63 ( ( aSet0(W0) % 0.57/0.63 & aSet0(W1) ) % 0.57/0.63 => ( ( ! [W2] : % 0.57/0.63 ( aElementOf0(W2,W0) % 0.57/0.63 => aElementOf0(W2,W1) ) % 0.57/0.63 & ! [W2] : % 0.57/0.63 ( aElementOf0(W2,W1) % 0.57/0.63 => aElementOf0(W2,W0) ) ) % 0.57/0.63 => W0 = W1 ) ) ). % 0.57/0.63 % 0.57/0.63 fof(mDefSSum,definition, % 0.57/0.63 ! [W0,W1] : % 0.57/0.63 ( ( aSet0(W0) % 0.57/0.63 & aSet0(W1) ) % 0.57/0.63 => ! [W2] : % 0.57/0.63 ( W2 = sdtpldt1(W0,W1) % 0.57/0.63 <=> ( aSet0(W2) % 0.57/0.63 & ! [W3] : % 0.57/0.63 ( aElementOf0(W3,W2) % 0.57/0.63 <=> ? [W4,W5] : % 0.57/0.63 ( aElementOf0(W4,W0) % 0.57/0.63 & aElementOf0(W5,W1) % 0.57/0.63 & sdtpldt0(W4,W5) = W3 ) ) ) ) ) ). % 0.57/0.63 % 0.57/0.63 fof(mDefSInt,definition, % 0.57/0.63 ! [W0,W1] : % 0.57/0.63 ( ( aSet0(W0) % 0.57/0.63 & aSet0(W1) ) % 0.57/0.63 => ! [W2] : % 0.57/0.63 ( W2 = sdtasasdt0(W0,W1) % 0.57/0.63 <=> ( aSet0(W2) % 0.57/0.63 & ! [W3] : % 0.57/0.63 ( aElementOf0(W3,W2) % 0.57/0.63 <=> ( aElementOf0(W3,W0) % 0.57/0.63 & aElementOf0(W3,W1) ) ) ) ) ) ). % 0.57/0.63 % 0.57/0.63 fof(mDefIdeal,definition, % 0.57/0.63 ! [W0] : % 0.57/0.63 ( aIdeal0(W0) % 0.57/0.63 <=> ( aSet0(W0) % 0.57/0.63 & ! [W1] : % 0.57/0.63 ( aElementOf0(W1,W0) % 0.57/0.63 => ( ! [W2] : % 0.57/0.63 ( aElementOf0(W2,W0) % 0.57/0.63 => aElementOf0(sdtpldt0(W1,W2),W0) ) % 0.57/0.63 & ! [W2] : % 0.57/0.63 ( aElement0(W2) % 0.57/0.63 => aElementOf0(sdtasdt0(W2,W1),W0) ) ) ) ) ) ). % 0.57/0.63 % 0.57/0.63 fof(m__870,hypothesis, % 0.57/0.63 ( aSet0(xI) % 0.57/0.63 & ! [W0] : % 0.57/0.63 ( aElementOf0(W0,xI) % 0.57/0.63 => ( ! [W1] : % 0.57/0.63 ( aElementOf0(W1,xI) % 0.57/0.63 => aElementOf0(sdtpldt0(W0,W1),xI) ) % 0.57/0.63 & ! [W1] : % 0.57/0.63 ( aElement0(W1) % 0.57/0.63 => aElementOf0(sdtasdt0(W1,W0),xI) ) ) ) % 0.57/0.63 & aIdeal0(xI) % 0.57/0.63 & aSet0(xJ) % 0.57/0.63 & ! [W0] : % 0.57/0.63 ( aElementOf0(W0,xJ) % 0.57/0.63 => ( ! [W1] : % 0.57/0.63 ( aElementOf0(W1,xJ) % 0.57/0.63 => aElementOf0(sdtpldt0(W0,W1),xJ) ) % 0.57/0.63 & ! [W1] : % 0.57/0.63 ( aElement0(W1) % 0.57/0.63 => aElementOf0(sdtasdt0(W1,W0),xJ) ) ) ) % 0.57/0.63 & aIdeal0(xJ) ) ). % 0.57/0.63 % 0.57/0.63 fof(m__901,hypothesis, % 0.57/0.63 ( ? [W0,W1] : % 0.57/0.63 ( aElementOf0(W0,xI) % 0.57/0.63 & aElementOf0(W1,xJ) % 0.57/0.63 & sdtpldt0(W0,W1) = xx ) % 0.57/0.63 & aElementOf0(xx,sdtpldt1(xI,xJ)) % 0.57/0.63 & ? [W0,W1] : % 0.57/0.63 ( aElementOf0(W0,xI) % 0.57/0.63 & aElementOf0(W1,xJ) % 0.57/0.63 & sdtpldt0(W0,W1) = xy ) % 0.57/0.63 & aElementOf0(xy,sdtpldt1(xI,xJ)) % 0.57/0.63 & aElement0(xz) ) ). % 0.57/0.63 % 0.57/0.63 fof(m__,conjecture, % 0.57/0.63 ? [W0,W1] : % 0.57/0.63 ( aElementOf0(W0,xI) % 0.57/0.63 & aElementOf0(W1,xJ) % 0.57/0.63 & xx = sdtpldt0(W0,W1) ) ). % 0.57/0.63 % 0.57/0.63 %------------------------------------------------------------------------------ % 0.57/0.63 %------------------------------------------- % 0.57/0.63 % Proof found % 0.57/0.63 % SZS status Theorem for theBenchmark % 0.57/0.63 % SZS output start Proof % 0.57/0.63 %ClaNum:114(EqnAxiom:44) % 0.57/0.63 %VarNum:412(SingletonVarNum:124) % 0.57/0.63 %MaxLitNum:8 % 0.57/0.63 %MaxfuncDepth:2 % 0.57/0.63 %SharedTerms:31 % 0.57/0.63 %goalClause: 83 % 0.57/0.63 [45]P1(a1) % 0.57/0.63 [46]P1(a22) % 0.57/0.63 [47]P1(a23) % 0.57/0.63 [48]P2(a24) % 0.57/0.63 [49]P2(a25) % 0.57/0.63 [50]P3(a24) % 0.57/0.63 [51]P3(a25) % 0.57/0.63 [54]P4(a2,a24) % 0.57/0.63 [55]P4(a5,a25) % 0.57/0.63 [56]P4(a7,a24) % 0.57/0.63 [57]P4(a8,a25) % 0.57/0.63 [60]~E(a1,a22) % 0.57/0.63 [52]E(f6(a2,a5),a26) % 0.57/0.63 [53]E(f6(a7,a8),a27) % 0.57/0.63 [58]P4(a26,f20(a24,a25)) % 0.57/0.63 [59]P4(a27,f20(a24,a25)) % 0.57/0.63 [61]~P3(x611)+P2(x611) % 0.57/0.63 [62]~P1(x621)+P1(f21(x621)) % 0.57/0.63 [63]~P1(x631)+E(f9(a1,x631),a1) % 0.57/0.63 [64]~P1(x641)+E(f9(x641,a1),a1) % 0.57/0.63 [65]~P1(x651)+E(f6(a1,x651),x651) % 0.57/0.63 [66]~P1(x661)+E(f9(a22,x661),x661) % 0.57/0.63 [67]~P1(x671)+E(f6(x671,a1),x671) % 0.57/0.63 [68]~P1(x681)+E(f9(x681,a22),x681) % 0.57/0.63 [69]~P1(x691)+E(f6(f21(x691),x691),a1) % 0.57/0.63 [70]~P1(x701)+E(f6(x701,f21(x701)),a1) % 0.57/0.63 [71]~P1(x711)+E(f9(x711,f21(a22)),f21(x711)) % 0.57/0.63 [72]~P1(x721)+E(f9(f21(a22),x721),f21(x721)) % 0.57/0.63 [73]~P2(x731)+P3(x731)+P4(f10(x731),x731) % 0.57/0.63 [74]~P4(x741,x742)+P1(x741)+~P2(x742) % 0.57/0.63 [76]~P1(x762)+~P1(x761)+E(f6(x761,x762),f6(x762,x761)) % 0.57/0.63 [77]~P1(x772)+~P1(x771)+E(f9(x771,x772),f9(x772,x771)) % 0.57/0.63 [81]~P1(x812)+~P1(x811)+P1(f6(x811,x812)) % 0.57/0.63 [82]~P1(x822)+~P1(x821)+P1(f9(x821,x822)) % 0.57/0.63 [83]~P4(x832,a25)+~P4(x831,a24)+~E(f6(x831,x832),a26) % 0.57/0.63 [84]~P1(x841)+~P4(x842,a24)+P4(f9(x841,x842),a24) % 0.57/0.63 [85]~P1(x851)+~P4(x852,a25)+P4(f9(x851,x852),a25) % 0.57/0.63 [89]~P4(x891,a24)+~P4(x892,a24)+P4(f6(x891,x892),a24) % 0.57/0.63 [90]~P4(x901,a25)+~P4(x902,a25)+P4(f6(x901,x902),a25) % 0.57/0.63 [80]~P2(x801)+P3(x801)+P4(f4(x801),x801)+P1(f3(x801)) % 0.57/0.63 [99]~P2(x991)+P3(x991)+P1(f3(x991))+~P4(f6(f10(x991),f4(x991)),x991) % 0.57/0.63 [102]~P2(x1021)+P3(x1021)+P4(f4(x1021),x1021)+~P4(f9(f3(x1021),f10(x1021)),x1021) % 0.57/0.63 [104]~P2(x1041)+P3(x1041)+~P4(f6(f10(x1041),f4(x1041)),x1041)+~P4(f9(f3(x1041),f10(x1041)),x1041) % 0.57/0.63 [78]~P2(x783)+~P2(x782)+P2(x781)+~E(x781,f20(x782,x783)) % 0.57/0.63 [79]~P2(x793)+~P2(x792)+P2(x791)+~E(x791,f19(x792,x793)) % 0.57/0.63 [88]~P1(x881)+~P3(x883)+~P4(x882,x883)+P4(f9(x881,x882),x883) % 0.57/0.63 [91]~P3(x913)+~P4(x911,x913)+~P4(x912,x913)+P4(f6(x911,x912),x913) % 0.57/0.63 [94]~P1(x943)+~P1(x942)+~P1(x941)+E(f6(f6(x941,x942),x943),f6(x941,f6(x942,x943))) % 0.57/0.63 [95]~P1(x953)+~P1(x952)+~P1(x951)+E(f9(f9(x951,x952),x953),f9(x951,f9(x952,x953))) % 0.57/0.63 [100]~P1(x1003)+~P1(x1002)+~P1(x1001)+E(f6(f9(x1001,x1002),f9(x1001,x1003)),f9(x1001,f6(x1002,x1003))) % 0.57/0.63 [101]~P1(x1012)+~P1(x1013)+~P1(x1011)+E(f6(f9(x1011,x1012),f9(x1013,x1012)),f9(f6(x1011,x1013),x1012)) % 0.57/0.63 [75]~P1(x751)+~P1(x752)+E(x751,a1)+E(x752,a1)+~E(f9(x752,x751),a1) % 0.57/0.63 [92]~P2(x922)+~P2(x921)+E(x921,x922)+P4(f11(x921,x922),x921)+P4(f12(x921,x922),x922) % 0.57/0.63 [96]~P2(x962)+~P2(x961)+E(x961,x962)+P4(f11(x961,x962),x961)+~P4(f12(x961,x962),x961) % 0.57/0.63 [97]~P2(x972)+~P2(x971)+E(x971,x972)+P4(f12(x971,x972),x972)+~P4(f11(x971,x972),x972) % 0.57/0.63 [103]~P2(x1032)+~P2(x1031)+E(x1031,x1032)+~P4(f11(x1031,x1032),x1032)+~P4(f12(x1031,x1032),x1031) % 0.57/0.63 [86]~P2(x864)+~P2(x862)+~P4(x861,x863)+P4(x861,x862)+~E(x863,f19(x864,x862)) % 0.57/0.63 [87]~P2(x874)+~P2(x872)+~P4(x871,x873)+P4(x871,x872)+~E(x873,f19(x872,x874)) % 0.57/0.63 [111]~P2(x1112)+~P2(x1111)+~P4(x1114,x1113)+~E(x1113,f20(x1111,x1112))+P4(f14(x1111,x1112,x1113,x1114),x1111) % 0.57/0.63 [112]~P2(x1122)+~P2(x1121)+~P4(x1124,x1123)+~E(x1123,f20(x1121,x1122))+P4(f15(x1121,x1122,x1123,x1124),x1122) % 0.57/0.63 [114]~P2(x1142)+~P2(x1141)+~P4(x1144,x1143)+~E(x1143,f20(x1141,x1142))+E(f6(f14(x1141,x1142,x1143,x1144),f15(x1141,x1142,x1143,x1144)),x1144) % 0.57/0.63 [105]~P2(x1051)+~P2(x1053)+~P2(x1052)+P4(f13(x1052,x1053,x1051),x1051)+P4(f16(x1052,x1053,x1051),x1052)+E(x1051,f20(x1052,x1053)) % 0.57/0.63 [106]~P2(x1061)+~P2(x1063)+~P2(x1062)+P4(f13(x1062,x1063,x1061),x1061)+P4(f17(x1062,x1063,x1061),x1063)+E(x1061,f20(x1062,x1063)) % 0.57/0.63 [107]~P2(x1071)+~P2(x1073)+~P2(x1072)+P4(f18(x1072,x1073,x1071),x1071)+P4(f18(x1072,x1073,x1071),x1073)+E(x1071,f19(x1072,x1073)) % 0.57/0.63 [108]~P2(x1081)+~P2(x1083)+~P2(x1082)+P4(f18(x1082,x1083,x1081),x1081)+P4(f18(x1082,x1083,x1081),x1082)+E(x1081,f19(x1082,x1083)) % 0.57/0.63 [110]~P2(x1101)+~P2(x1103)+~P2(x1102)+P4(f13(x1102,x1103,x1101),x1101)+E(x1101,f20(x1102,x1103))+E(f6(f16(x1102,x1103,x1101),f17(x1102,x1103,x1101)),f13(x1102,x1103,x1101)) % 0.57/0.63 [93]~P2(x934)+~P2(x933)+~P4(x931,x934)+~P4(x931,x933)+P4(x931,x932)+~E(x932,f19(x933,x934)) % 0.57/0.63 [113]~P2(x1131)+~P2(x1133)+~P2(x1132)+~P4(f18(x1132,x1133,x1131),x1131)+~P4(f18(x1132,x1133,x1131),x1133)+~P4(f18(x1132,x1133,x1131),x1132)+E(x1131,f19(x1132,x1133)) % 0.57/0.63 [98]~P2(x984)+~P2(x983)+~P4(x986,x984)+~P4(x985,x983)+P4(x981,x982)+~E(x982,f20(x983,x984))+~E(f6(x985,x986),x981) % 0.57/0.63 [109]~P2(x1091)+~P2(x1093)+~P2(x1092)+~P4(x1095,x1093)+~P4(x1094,x1092)+~P4(f13(x1092,x1093,x1091),x1091)+E(x1091,f20(x1092,x1093))+~E(f6(x1094,x1095),f13(x1092,x1093,x1091)) % 0.57/0.63 %EqnAxiom % 0.57/0.63 [1]E(x11,x11) % 0.57/0.63 [2]E(x22,x21)+~E(x21,x22) % 0.57/0.63 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.57/0.63 [4]~E(x41,x42)+E(f6(x41,x43),f6(x42,x43)) % 0.57/0.63 [5]~E(x51,x52)+E(f6(x53,x51),f6(x53,x52)) % 0.57/0.63 [6]~E(x61,x62)+E(f20(x61,x63),f20(x62,x63)) % 0.57/0.63 [7]~E(x71,x72)+E(f20(x73,x71),f20(x73,x72)) % 0.57/0.63 [8]~E(x81,x82)+E(f18(x81,x83,x84),f18(x82,x83,x84)) % 0.57/0.63 [9]~E(x91,x92)+E(f18(x93,x91,x94),f18(x93,x92,x94)) % 0.57/0.63 [10]~E(x101,x102)+E(f18(x103,x104,x101),f18(x103,x104,x102)) % 0.57/0.63 [11]~E(x111,x112)+E(f19(x111,x113),f19(x112,x113)) % 0.57/0.63 [12]~E(x121,x122)+E(f19(x123,x121),f19(x123,x122)) % 0.57/0.63 [13]~E(x131,x132)+E(f21(x131),f21(x132)) % 0.57/0.63 [14]~E(x141,x142)+E(f9(x141,x143),f9(x142,x143)) % 0.57/0.63 [15]~E(x151,x152)+E(f9(x153,x151),f9(x153,x152)) % 0.57/0.63 [16]~E(x161,x162)+E(f13(x161,x163,x164),f13(x162,x163,x164)) % 0.57/0.63 [17]~E(x171,x172)+E(f13(x173,x171,x174),f13(x173,x172,x174)) % 0.57/0.63 [18]~E(x181,x182)+E(f13(x183,x184,x181),f13(x183,x184,x182)) % 0.57/0.63 [19]~E(x191,x192)+E(f15(x191,x193,x194,x195),f15(x192,x193,x194,x195)) % 0.57/0.63 [20]~E(x201,x202)+E(f15(x203,x201,x204,x205),f15(x203,x202,x204,x205)) % 0.57/0.63 [21]~E(x211,x212)+E(f15(x213,x214,x211,x215),f15(x213,x214,x212,x215)) % 0.57/0.63 [22]~E(x221,x222)+E(f15(x223,x224,x225,x221),f15(x223,x224,x225,x222)) % 0.57/0.63 [23]~E(x231,x232)+E(f4(x231),f4(x232)) % 0.57/0.63 [24]~E(x241,x242)+E(f14(x241,x243,x244,x245),f14(x242,x243,x244,x245)) % 0.57/0.63 [25]~E(x251,x252)+E(f14(x253,x251,x254,x255),f14(x253,x252,x254,x255)) % 0.57/0.63 [26]~E(x261,x262)+E(f14(x263,x264,x261,x265),f14(x263,x264,x262,x265)) % 0.57/0.63 [27]~E(x271,x272)+E(f14(x273,x274,x275,x271),f14(x273,x274,x275,x272)) % 0.57/0.63 [28]~E(x281,x282)+E(f10(x281),f10(x282)) % 0.57/0.63 [29]~E(x291,x292)+E(f11(x291,x293),f11(x292,x293)) % 0.57/0.63 [30]~E(x301,x302)+E(f11(x303,x301),f11(x303,x302)) % 0.57/0.63 [31]~E(x311,x312)+E(f3(x311),f3(x312)) % 0.57/0.63 [32]~E(x321,x322)+E(f17(x321,x323,x324),f17(x322,x323,x324)) % 0.57/0.63 [33]~E(x331,x332)+E(f17(x333,x331,x334),f17(x333,x332,x334)) % 0.57/0.63 [34]~E(x341,x342)+E(f17(x343,x344,x341),f17(x343,x344,x342)) % 0.57/0.63 [35]~E(x351,x352)+E(f12(x351,x353),f12(x352,x353)) % 0.57/0.63 [36]~E(x361,x362)+E(f12(x363,x361),f12(x363,x362)) % 0.57/0.63 [37]~E(x371,x372)+E(f16(x371,x373,x374),f16(x372,x373,x374)) % 0.57/0.63 [38]~E(x381,x382)+E(f16(x383,x381,x384),f16(x383,x382,x384)) % 0.57/0.63 [39]~E(x391,x392)+E(f16(x393,x394,x391),f16(x393,x394,x392)) % 0.57/0.63 [40]~P1(x401)+P1(x402)+~E(x401,x402) % 0.57/0.63 [41]P4(x412,x413)+~E(x411,x412)+~P4(x411,x413) % 0.57/0.63 [42]P4(x423,x422)+~E(x421,x422)+~P4(x423,x421) % 0.57/0.63 [43]~P2(x431)+P2(x432)+~E(x431,x432) % 0.57/0.63 [44]~P3(x441)+P3(x442)+~E(x441,x442) % 0.57/0.63 % 0.57/0.63 %------------------------------------------- % 0.57/0.63 cnf(123,plain, % 0.57/0.63 ($false), % 0.57/0.63 inference(scs_inference,[],[55,54,52,83]), % 0.57/0.64 ['proof']). % 0.57/0.64 % SZS output end Proof % 0.57/0.64 % Total time :0.010000s %------------------------------------------------------------------------------