%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : RNG086+1 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n004.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:00 EDT 2024 % Result : Theorem 118.51s 118.57s % Output : CNFRefutation 118.51s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : RNG086+1 : TPTP v8.2.0. Released v4.0.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n004.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:46:54 EDT 2024 % 0.13/0.33 % CPUTime : % 0.55/0.59 start to proof:theBenchmark % 118.50/118.56 %------------------------------------------- % 118.50/118.56 % File :CSE---1.7 % 118.50/118.56 % Problem :theBenchmark % 118.50/118.56 % Transform :cnf % 118.50/118.56 % Format :tptp:raw % 118.50/118.56 % Command :java -jar mcs_scs.jar %d %s % 118.50/118.56 % 118.50/118.56 % Result :Theorem 117.850000s % 118.50/118.56 % Output :CNFRefutation 117.850000s % 118.50/118.56 %------------------------------------------- % 118.51/118.57 %------------------------------------------------------------------------------ % 118.51/118.57 % File : RNG086+1 : TPTP v8.2.0. Released v4.0.0. % 118.51/118.57 % Domain : Ring Theory % 118.51/118.57 % Problem : Chinese remainder theorem in a ring 03_01, 00 expansion % 118.51/118.57 % Version : Especial. % 118.51/118.57 % English : % 118.51/118.57 % 118.51/118.57 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 118.51/118.57 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 118.51/118.57 % Source : [Pas08] % 118.51/118.57 % Names : chines_03_01.00 [Pas08] % 118.51/118.57 % 118.51/118.57 % Status : Theorem % 118.51/118.57 % Rating : 0.36 v8.2.0, 0.42 v7.5.0, 0.44 v7.4.0, 0.40 v7.3.0, 0.38 v7.1.0, 0.39 v7.0.0, 0.43 v6.4.0, 0.46 v6.3.0, 0.42 v6.2.0, 0.48 v6.1.0, 0.60 v6.0.0, 0.57 v5.5.0, 0.70 v5.4.0, 0.71 v5.3.0, 0.70 v5.2.0, 0.55 v5.1.0, 0.57 v5.0.0, 0.71 v4.1.0, 0.74 v4.0.1, 0.91 v4.0.0 % 118.51/118.57 % Syntax : Number of formulae : 27 ( 3 unt; 3 def) % 118.51/118.57 % Number of atoms : 94 ( 25 equ) % 118.51/118.57 % Maximal formula atoms : 8 ( 3 avg) % 118.51/118.57 % Number of connectives : 68 ( 1 ~; 1 |; 33 &) % 118.51/118.57 % ( 5 <=>; 28 =>; 0 <=; 0 <~>) % 118.51/118.57 % Maximal formula depth : 13 ( 5 avg) % 118.51/118.57 % Maximal term depth : 3 ( 1 avg) % 118.51/118.57 % Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty) % 118.51/118.57 % Number of functors : 12 ( 12 usr; 7 con; 0-2 aty) % 118.51/118.57 % Number of variables : 49 ( 45 !; 4 ?) % 118.51/118.57 % SPC : FOF_THM_RFO_SEQ % 118.51/118.57 % 118.51/118.57 % Comments : Problem generated by the SAD system [VLP07] % 118.51/118.57 %------------------------------------------------------------------------------ % 118.51/118.57 fof(mElmSort,axiom, % 118.51/118.57 ! [W0] : % 118.51/118.57 ( aElement0(W0) % 118.51/118.57 => $true ) ). % 118.51/118.57 % 118.51/118.57 fof(mSortsC,axiom, % 118.51/118.57 aElement0(sz00) ). % 118.51/118.57 % 118.51/118.57 fof(mSortsC_01,axiom, % 118.51/118.57 aElement0(sz10) ). % 118.51/118.57 % 118.51/118.57 fof(mSortsU,axiom, % 118.51/118.57 ! [W0] : % 118.51/118.57 ( aElement0(W0) % 118.51/118.57 => aElement0(smndt0(W0)) ) ). % 118.51/118.57 % 118.51/118.57 fof(mSortsB,axiom, % 118.51/118.57 ! [W0,W1] : % 118.51/118.57 ( ( aElement0(W0) % 118.51/118.57 & aElement0(W1) ) % 118.51/118.57 => aElement0(sdtpldt0(W0,W1)) ) ). % 118.51/118.57 % 118.51/118.57 fof(mSortsB_02,axiom, % 118.51/118.57 ! [W0,W1] : % 118.51/118.57 ( ( aElement0(W0) % 118.51/118.57 & aElement0(W1) ) % 118.51/118.57 => aElement0(sdtasdt0(W0,W1)) ) ). % 118.51/118.57 % 118.51/118.57 fof(mAddComm,axiom, % 118.51/118.57 ! [W0,W1] : % 118.51/118.57 ( ( aElement0(W0) % 118.51/118.57 & aElement0(W1) ) % 118.51/118.57 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 118.51/118.57 % 118.51/118.57 fof(mAddAsso,axiom, % 118.51/118.57 ! [W0,W1,W2] : % 118.51/118.57 ( ( aElement0(W0) % 118.51/118.57 & aElement0(W1) % 118.51/118.57 & aElement0(W2) ) % 118.51/118.57 => sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) ). % 118.51/118.57 % 118.51/118.57 fof(mAddZero,axiom, % 118.51/118.57 ! [W0] : % 118.51/118.57 ( aElement0(W0) % 118.51/118.57 => ( sdtpldt0(W0,sz00) = W0 % 118.51/118.57 & W0 = sdtpldt0(sz00,W0) ) ) ). % 118.51/118.57 % 118.51/118.57 fof(mAddInvr,axiom, % 118.51/118.57 ! [W0] : % 118.51/118.57 ( aElement0(W0) % 118.51/118.57 => ( sdtpldt0(W0,smndt0(W0)) = sz00 % 118.51/118.57 & sz00 = sdtpldt0(smndt0(W0),W0) ) ) ). % 118.51/118.57 % 118.51/118.57 fof(mMulComm,axiom, % 118.51/118.57 ! [W0,W1] : % 118.51/118.57 ( ( aElement0(W0) % 118.51/118.57 & aElement0(W1) ) % 118.51/118.57 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 118.51/118.57 % 118.51/118.57 fof(mMulAsso,axiom, % 118.51/118.57 ! [W0,W1,W2] : % 118.51/118.57 ( ( aElement0(W0) % 118.51/118.57 & aElement0(W1) % 118.51/118.57 & aElement0(W2) ) % 118.51/118.57 => sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) ). % 118.51/118.57 % 118.51/118.57 fof(mMulUnit,axiom, % 118.51/118.57 ! [W0] : % 118.51/118.57 ( aElement0(W0) % 118.51/118.57 => ( sdtasdt0(W0,sz10) = W0 % 118.51/118.57 & W0 = sdtasdt0(sz10,W0) ) ) ). % 118.51/118.57 % 118.51/118.57 fof(mAMDistr,axiom, % 118.51/118.57 ! [W0,W1,W2] : % 118.51/118.57 ( ( aElement0(W0) % 118.51/118.57 & aElement0(W1) % 118.51/118.57 & aElement0(W2) ) % 118.51/118.57 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 118.51/118.57 & sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ). % 118.51/118.57 % 118.51/118.57 fof(mMulMnOne,axiom, % 118.51/118.57 ! [W0] : % 118.51/118.57 ( aElement0(W0) % 118.51/118.57 => ( sdtasdt0(smndt0(sz10),W0) = smndt0(W0) % 118.51/118.57 & smndt0(W0) = sdtasdt0(W0,smndt0(sz10)) ) ) ). % 118.51/118.57 % 118.51/118.57 fof(mMulZero,axiom, % 118.51/118.57 ! [W0] : % 118.51/118.57 ( aElement0(W0) % 118.51/118.57 => ( sdtasdt0(W0,sz00) = sz00 % 118.51/118.57 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 118.51/118.57 % 118.51/118.57 fof(mCancel,axiom, % 118.51/118.57 ! [W0,W1] : % 118.51/118.57 ( ( aElement0(W0) % 118.51/118.57 & aElement0(W1) ) % 118.51/118.57 => ( sdtasdt0(W0,W1) = sz00 % 118.51/118.57 => ( W0 = sz00 % 118.51/118.57 | W1 = sz00 ) ) ) ). % 118.51/118.57 % 118.51/118.57 fof(mUnNeZr,axiom, % 118.51/118.57 sz10 != sz00 ). % 118.51/118.57 % 118.51/118.57 fof(mSetSort,axiom, % 118.51/118.57 ! [W0] : % 118.51/118.57 ( aSet0(W0) % 118.51/118.57 => $true ) ). % 118.51/118.57 % 118.51/118.57 fof(mEOfElem,axiom, % 118.51/118.57 ! [W0] : % 118.51/118.57 ( aSet0(W0) % 118.51/118.57 => ! [W1] : % 118.51/118.57 ( aElementOf0(W1,W0) % 118.51/118.57 => aElement0(W1) ) ) ). % 118.51/118.57 % 118.51/118.57 fof(mSetEq,axiom, % 118.51/118.57 ! [W0,W1] : % 118.51/118.57 ( ( aSet0(W0) % 118.51/118.57 & aSet0(W1) ) % 118.51/118.57 => ( ( ! [W2] : % 118.51/118.57 ( aElementOf0(W2,W0) % 118.51/118.57 => aElementOf0(W2,W1) ) % 118.51/118.57 & ! [W2] : % 118.51/118.57 ( aElementOf0(W2,W1) % 118.51/118.57 => aElementOf0(W2,W0) ) ) % 118.51/118.57 => W0 = W1 ) ) ). % 118.51/118.57 % 118.51/118.57 fof(mDefSSum,definition, % 118.51/118.57 ! [W0,W1] : % 118.51/118.57 ( ( aSet0(W0) % 118.51/118.57 & aSet0(W1) ) % 118.51/118.57 => ! [W2] : % 118.51/118.57 ( W2 = sdtpldt1(W0,W1) % 118.51/118.57 <=> ( aSet0(W2) % 118.51/118.57 & ! [W3] : % 118.51/118.57 ( aElementOf0(W3,W2) % 118.51/118.57 <=> ? [W4,W5] : % 118.51/118.57 ( aElementOf0(W4,W0) % 118.51/118.57 & aElementOf0(W5,W1) % 118.51/118.57 & sdtpldt0(W4,W5) = W3 ) ) ) ) ) ). % 118.51/118.57 % 118.51/118.57 fof(mDefSInt,definition, % 118.51/118.57 ! [W0,W1] : % 118.51/118.57 ( ( aSet0(W0) % 118.51/118.57 & aSet0(W1) ) % 118.51/118.57 => ! [W2] : % 118.51/118.57 ( W2 = sdtasasdt0(W0,W1) % 118.51/118.57 <=> ( aSet0(W2) % 118.51/118.57 & ! [W3] : % 118.51/118.57 ( aElementOf0(W3,W2) % 118.51/118.57 <=> ( aElementOf0(W3,W0) % 118.51/118.57 & aElementOf0(W3,W1) ) ) ) ) ) ). % 118.51/118.57 % 118.51/118.57 fof(mDefIdeal,definition, % 118.51/118.57 ! [W0] : % 118.51/118.57 ( aIdeal0(W0) % 118.51/118.57 <=> ( aSet0(W0) % 118.51/118.57 & ! [W1] : % 118.51/118.57 ( aElementOf0(W1,W0) % 118.51/118.57 => ( ! [W2] : % 118.51/118.57 ( aElementOf0(W2,W0) % 118.51/118.57 => aElementOf0(sdtpldt0(W1,W2),W0) ) % 118.51/118.57 & ! [W2] : % 118.51/118.57 ( aElement0(W2) % 118.51/118.57 => aElementOf0(sdtasdt0(W2,W1),W0) ) ) ) ) ) ). % 118.51/118.57 % 118.51/118.57 fof(m__870,hypothesis, % 118.51/118.57 ( aIdeal0(xI) % 118.51/118.57 & aIdeal0(xJ) ) ). % 118.51/118.57 % 118.51/118.57 fof(m__901,hypothesis, % 118.51/118.57 ( aElementOf0(xx,sdtpldt1(xI,xJ)) % 118.51/118.57 & aElementOf0(xy,sdtpldt1(xI,xJ)) % 118.51/118.57 & aElement0(xz) ) ). % 118.51/118.57 % 118.51/118.57 fof(m__,conjecture, % 118.51/118.57 ? [W0,W1] : % 118.51/118.57 ( aElementOf0(W0,xI) % 118.51/118.57 & aElementOf0(W1,xJ) % 118.51/118.57 & xx = sdtpldt0(W0,W1) ) ). % 118.51/118.57 % 118.51/118.57 %------------------------------------------------------------------------------ % 118.51/118.57 %------------------------------------------- % 118.51/118.57 % Proof found % 118.51/118.57 % SZS status Theorem for theBenchmark % 118.51/118.57 % SZS output start Proof % 118.51/118.58 %ClaNum:102(EqnAxiom:44) % 118.51/118.58 %VarNum:396(SingletonVarNum:116) % 118.51/118.58 %MaxLitNum:8 % 118.51/118.58 %MaxfuncDepth:2 % 118.51/118.58 %SharedTerms:17 % 118.51/118.58 %goalClause: 75 % 118.51/118.58 [45]P1(a1) % 118.51/118.58 [46]P1(a18) % 118.51/118.58 [47]P1(a19) % 118.51/118.58 [48]P2(a20) % 118.51/118.58 [49]P2(a21) % 118.51/118.58 [52]~E(a1,a18) % 118.51/118.58 [50]P3(a22,f2(a20,a21)) % 118.51/118.58 [51]P3(a23,f2(a20,a21)) % 118.51/118.58 [53]~P2(x531)+P4(x531) % 118.51/118.58 [54]~P1(x541)+P1(f17(x541)) % 118.51/118.58 [55]~P1(x551)+E(f3(a1,x551),a1) % 118.51/118.58 [56]~P1(x561)+E(f3(x561,a1),a1) % 118.51/118.58 [57]~P1(x571)+E(f16(a1,x571),x571) % 118.51/118.58 [58]~P1(x581)+E(f3(a18,x581),x581) % 118.51/118.58 [59]~P1(x591)+E(f16(x591,a1),x591) % 118.51/118.58 [60]~P1(x601)+E(f3(x601,a18),x601) % 118.51/118.58 [61]~P1(x611)+E(f16(f17(x611),x611),a1) % 118.51/118.58 [62]~P1(x621)+E(f16(x621,f17(x621)),a1) % 118.51/118.58 [63]~P1(x631)+E(f3(x631,f17(a18)),f17(x631)) % 118.51/118.58 [64]~P1(x641)+E(f3(f17(a18),x641),f17(x641)) % 118.51/118.58 [65]~P4(x651)+P2(x651)+P3(f4(x651),x651) % 118.51/118.58 [66]~P3(x661,x662)+P1(x661)+~P4(x662) % 118.51/118.58 [68]~P1(x682)+~P1(x681)+E(f16(x681,x682),f16(x682,x681)) % 118.51/118.58 [69]~P1(x692)+~P1(x691)+E(f3(x691,x692),f3(x692,x691)) % 118.51/118.58 [73]~P1(x732)+~P1(x731)+P1(f16(x731,x732)) % 118.51/118.58 [74]~P1(x742)+~P1(x741)+P1(f3(x741,x742)) % 118.51/118.58 [75]~P3(x752,a21)+~P3(x751,a20)+~E(f16(x751,x752),a22) % 118.51/118.58 [72]~P4(x721)+P2(x721)+P3(f6(x721),x721)+P1(f5(x721)) % 118.51/118.58 [87]~P4(x871)+P2(x871)+P1(f5(x871))+~P3(f16(f4(x871),f6(x871)),x871) % 118.51/118.58 [90]~P4(x901)+P2(x901)+P3(f6(x901),x901)+~P3(f3(f5(x901),f4(x901)),x901) % 118.51/118.58 [92]~P4(x921)+P2(x921)+~P3(f16(f4(x921),f6(x921)),x921)+~P3(f3(f5(x921),f4(x921)),x921) % 118.51/118.58 [70]~P4(x703)+~P4(x702)+P4(x701)+~E(x701,f2(x702,x703)) % 118.51/118.58 [71]~P4(x713)+~P4(x712)+P4(x711)+~E(x711,f15(x712,x713)) % 118.51/118.58 [78]~P1(x781)+~P2(x783)+~P3(x782,x783)+P3(f3(x781,x782),x783) % 118.51/118.58 [79]~P2(x793)+~P3(x791,x793)+~P3(x792,x793)+P3(f16(x791,x792),x793) % 118.51/118.58 [82]~P1(x823)+~P1(x822)+~P1(x821)+E(f16(f16(x821,x822),x823),f16(x821,f16(x822,x823))) % 118.51/118.58 [83]~P1(x833)+~P1(x832)+~P1(x831)+E(f3(f3(x831,x832),x833),f3(x831,f3(x832,x833))) % 118.51/118.58 [88]~P1(x883)+~P1(x882)+~P1(x881)+E(f16(f3(x881,x882),f3(x881,x883)),f3(x881,f16(x882,x883))) % 118.51/118.58 [89]~P1(x892)+~P1(x893)+~P1(x891)+E(f16(f3(x891,x892),f3(x893,x892)),f3(f16(x891,x893),x892)) % 118.51/118.58 [67]~P1(x671)+~P1(x672)+E(x671,a1)+E(x672,a1)+~E(f3(x672,x671),a1) % 118.51/118.58 [80]~P4(x802)+~P4(x801)+E(x801,x802)+P3(f7(x801,x802),x801)+P3(f8(x801,x802),x802) % 118.51/118.58 [84]~P4(x842)+~P4(x841)+E(x841,x842)+P3(f7(x841,x842),x841)+~P3(f8(x841,x842),x841) % 118.51/118.58 [85]~P4(x852)+~P4(x851)+E(x851,x852)+P3(f8(x851,x852),x852)+~P3(f7(x851,x852),x852) % 118.51/118.58 [91]~P4(x912)+~P4(x911)+E(x911,x912)+~P3(f7(x911,x912),x912)+~P3(f8(x911,x912),x911) % 118.51/118.58 [76]~P4(x764)+~P4(x762)+~P3(x761,x763)+P3(x761,x762)+~E(x763,f15(x764,x762)) % 118.51/118.58 [77]~P4(x774)+~P4(x772)+~P3(x771,x773)+P3(x771,x772)+~E(x773,f15(x772,x774)) % 118.51/118.58 [99]~P4(x992)+~P4(x991)+~P3(x994,x993)+~E(x993,f2(x991,x992))+P3(f10(x991,x992,x993,x994),x991) % 118.51/118.58 [100]~P4(x1002)+~P4(x1001)+~P3(x1004,x1003)+~E(x1003,f2(x1001,x1002))+P3(f11(x1001,x1002,x1003,x1004),x1002) % 118.51/118.58 [102]~P4(x1022)+~P4(x1021)+~P3(x1024,x1023)+~E(x1023,f2(x1021,x1022))+E(f16(f10(x1021,x1022,x1023,x1024),f11(x1021,x1022,x1023,x1024)),x1024) % 118.51/118.58 [93]~P4(x931)+~P4(x933)+~P4(x932)+P3(f9(x932,x933,x931),x931)+P3(f12(x932,x933,x931),x932)+E(x931,f2(x932,x933)) % 118.51/118.58 [94]~P4(x941)+~P4(x943)+~P4(x942)+P3(f9(x942,x943,x941),x941)+P3(f13(x942,x943,x941),x943)+E(x941,f2(x942,x943)) % 118.51/118.58 [95]~P4(x951)+~P4(x953)+~P4(x952)+P3(f14(x952,x953,x951),x951)+P3(f14(x952,x953,x951),x953)+E(x951,f15(x952,x953)) % 118.51/118.58 [96]~P4(x961)+~P4(x963)+~P4(x962)+P3(f14(x962,x963,x961),x961)+P3(f14(x962,x963,x961),x962)+E(x961,f15(x962,x963)) % 118.51/118.58 [98]~P4(x981)+~P4(x983)+~P4(x982)+P3(f9(x982,x983,x981),x981)+E(x981,f2(x982,x983))+E(f16(f12(x982,x983,x981),f13(x982,x983,x981)),f9(x982,x983,x981)) % 118.51/118.58 [81]~P4(x814)+~P4(x813)+~P3(x811,x814)+~P3(x811,x813)+P3(x811,x812)+~E(x812,f15(x813,x814)) % 118.51/118.58 [101]~P4(x1011)+~P4(x1013)+~P4(x1012)+~P3(f14(x1012,x1013,x1011),x1011)+~P3(f14(x1012,x1013,x1011),x1013)+~P3(f14(x1012,x1013,x1011),x1012)+E(x1011,f15(x1012,x1013)) % 118.51/118.58 [86]~P4(x864)+~P4(x863)+~P3(x866,x864)+~P3(x865,x863)+P3(x861,x862)+~E(x862,f2(x863,x864))+~E(f16(x865,x866),x861) % 118.51/118.58 [97]~P4(x971)+~P4(x973)+~P4(x972)+~P3(x975,x973)+~P3(x974,x972)+~P3(f9(x972,x973,x971),x971)+E(x971,f2(x972,x973))+~E(f16(x974,x975),f9(x972,x973,x971)) % 118.51/118.58 %EqnAxiom % 118.51/118.58 [1]E(x11,x11) % 118.51/118.58 [2]E(x22,x21)+~E(x21,x22) % 118.51/118.58 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 118.51/118.58 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 118.51/118.58 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 118.51/118.58 [6]~E(x61,x62)+E(f16(x61,x63),f16(x62,x63)) % 118.51/118.58 [7]~E(x71,x72)+E(f16(x73,x71),f16(x73,x72)) % 118.51/118.58 [8]~E(x81,x82)+E(f17(x81),f17(x82)) % 118.51/118.58 [9]~E(x91,x92)+E(f3(x91,x93),f3(x92,x93)) % 118.51/118.58 [10]~E(x101,x102)+E(f3(x103,x101),f3(x103,x102)) % 118.51/118.58 [11]~E(x111,x112)+E(f6(x111),f6(x112)) % 118.51/118.58 [12]~E(x121,x122)+E(f11(x121,x123,x124,x125),f11(x122,x123,x124,x125)) % 118.51/118.58 [13]~E(x131,x132)+E(f11(x133,x131,x134,x135),f11(x133,x132,x134,x135)) % 118.51/118.58 [14]~E(x141,x142)+E(f11(x143,x144,x141,x145),f11(x143,x144,x142,x145)) % 118.51/118.58 [15]~E(x151,x152)+E(f11(x153,x154,x155,x151),f11(x153,x154,x155,x152)) % 118.51/118.58 [16]~E(x161,x162)+E(f4(x161),f4(x162)) % 118.51/118.58 [17]~E(x171,x172)+E(f10(x171,x173,x174,x175),f10(x172,x173,x174,x175)) % 118.51/118.58 [18]~E(x181,x182)+E(f10(x183,x181,x184,x185),f10(x183,x182,x184,x185)) % 118.51/118.58 [19]~E(x191,x192)+E(f10(x193,x194,x191,x195),f10(x193,x194,x192,x195)) % 118.51/118.58 [20]~E(x201,x202)+E(f10(x203,x204,x205,x201),f10(x203,x204,x205,x202)) % 118.51/118.58 [21]~E(x211,x212)+E(f8(x211,x213),f8(x212,x213)) % 118.51/118.58 [22]~E(x221,x222)+E(f8(x223,x221),f8(x223,x222)) % 118.51/118.58 [23]~E(x231,x232)+E(f9(x231,x233,x234),f9(x232,x233,x234)) % 118.51/118.58 [24]~E(x241,x242)+E(f9(x243,x241,x244),f9(x243,x242,x244)) % 118.51/118.58 [25]~E(x251,x252)+E(f9(x253,x254,x251),f9(x253,x254,x252)) % 118.51/118.58 [26]~E(x261,x262)+E(f14(x261,x263,x264),f14(x262,x263,x264)) % 118.51/118.58 [27]~E(x271,x272)+E(f14(x273,x271,x274),f14(x273,x272,x274)) % 118.51/118.58 [28]~E(x281,x282)+E(f14(x283,x284,x281),f14(x283,x284,x282)) % 118.51/118.58 [29]~E(x291,x292)+E(f7(x291,x293),f7(x292,x293)) % 118.51/118.58 [30]~E(x301,x302)+E(f7(x303,x301),f7(x303,x302)) % 118.51/118.58 [31]~E(x311,x312)+E(f15(x311,x313),f15(x312,x313)) % 118.51/118.58 [32]~E(x321,x322)+E(f15(x323,x321),f15(x323,x322)) % 118.51/118.58 [33]~E(x331,x332)+E(f13(x331,x333,x334),f13(x332,x333,x334)) % 118.51/118.58 [34]~E(x341,x342)+E(f13(x343,x341,x344),f13(x343,x342,x344)) % 118.51/118.58 [35]~E(x351,x352)+E(f13(x353,x354,x351),f13(x353,x354,x352)) % 118.51/118.58 [36]~E(x361,x362)+E(f12(x361,x363,x364),f12(x362,x363,x364)) % 118.51/118.58 [37]~E(x371,x372)+E(f12(x373,x371,x374),f12(x373,x372,x374)) % 118.51/118.58 [38]~E(x381,x382)+E(f12(x383,x384,x381),f12(x383,x384,x382)) % 118.51/118.58 [39]~E(x391,x392)+E(f5(x391),f5(x392)) % 118.51/118.58 [40]~P1(x401)+P1(x402)+~E(x401,x402) % 118.51/118.58 [41]P3(x412,x413)+~E(x411,x412)+~P3(x411,x413) % 118.51/118.58 [42]P3(x423,x422)+~E(x421,x422)+~P3(x423,x421) % 118.51/118.58 [43]~P4(x431)+P4(x432)+~E(x431,x432) % 118.51/118.58 [44]~P2(x441)+P2(x442)+~E(x441,x442) % 118.51/118.58 % 118.51/118.58 %------------------------------------------- % 118.51/118.59 cnf(103,plain, % 118.51/118.59 (~P4(x1031)+~P4(x1032)+P4(f2(x1032,x1031))), % 118.51/118.59 inference(equality_inference,[],[70])). % 118.51/118.59 cnf(104,plain, % 118.51/118.59 (~P4(x1041)+~P4(x1042)+P4(f15(x1042,x1041))), % 118.51/118.59 inference(equality_inference,[],[71])). % 118.51/118.59 cnf(105,plain, % 118.51/118.59 (P3(x1051,x1052)+~P4(x1053)+~P4(x1052)+~P3(x1051,f15(x1053,x1052))), % 118.51/118.59 inference(equality_inference,[],[76])). % 118.51/118.59 cnf(107,plain, % 118.51/118.59 (~P3(x1071,x1072)+~P4(x1073)+~P3(x1071,x1073)+~P4(x1072)+P3(x1071,f15(x1072,x1073))), % 118.51/118.59 inference(equality_inference,[],[81])). % 118.51/118.59 cnf(108,plain, % 118.51/118.59 (~P4(x1081)+~P4(x1082)+~P3(x1083,f2(x1082,x1081))+P3(f10(x1082,x1081,f2(x1082,x1081),x1083),x1082)), % 118.51/118.59 inference(equality_inference,[],[99])). % 118.51/118.59 cnf(109,plain, % 118.51/118.59 (~P4(x1091)+~P4(x1092)+~P3(x1093,f2(x1092,x1091))+P3(f11(x1092,x1091,f2(x1092,x1091),x1093),x1091)), % 118.51/118.59 inference(equality_inference,[],[100])). % 118.51/118.59 cnf(110,plain, % 118.51/118.59 (~P4(x1101)+~P4(x1102)+~P3(x1103,f2(x1102,x1101))+E(f16(f10(x1102,x1101,f2(x1102,x1101),x1103),f11(x1102,x1101,f2(x1102,x1101),x1103)),x1103)), % 118.51/118.59 inference(equality_inference,[],[102])). % 118.51/118.59 cnf(129,plain, % 118.51/118.59 (P4(f2(a20,a20))), % 118.51/118.59 inference(scs_inference,[],[48,53,103])). % 118.51/118.59 cnf(143,plain, % 118.51/118.59 (E(a1,f3(a1,a18))), % 118.51/118.59 inference(scs_inference,[],[46,2,55])). % 118.51/118.59 cnf(144,plain, % 118.51/118.59 (E(f3(a1,a18),a1)), % 118.51/118.59 inference(scs_inference,[],[143,2])). % 118.51/118.59 cnf(145,plain, % 118.51/118.59 (P1(f3(a1,a18))), % 118.51/118.59 inference(scs_inference,[],[143,45,2,40])). % 118.51/118.59 cnf(266,plain, % 118.51/118.59 (E(f3(f17(a19),a1),a1)), % 118.51/118.59 inference(scs_inference,[],[47,56,54])). % 118.51/118.59 cnf(267,plain, % 118.51/118.59 (E(a1,f3(f17(a19),a1))), % 118.51/118.59 inference(scs_inference,[],[266,2])). % 118.51/118.59 cnf(268,plain, % 118.51/118.59 (E(f3(a1,a18),f3(f17(a19),a1))), % 118.51/118.59 inference(scs_inference,[],[144,266,2,3])). % 118.51/118.59 cnf(274,plain, % 118.51/118.59 (E(f3(f17(a19),a1),f3(a1,a18))), % 118.51/118.59 inference(scs_inference,[],[268,2])). % 118.51/118.59 cnf(301,plain, % 118.51/118.59 (E(f16(a1,f17(a19)),f17(a19))), % 118.51/118.59 inference(scs_inference,[],[47,57,54])). % 118.51/118.59 cnf(302,plain, % 118.51/118.59 (E(f17(a19),f16(a1,f17(a19)))), % 118.51/118.59 inference(scs_inference,[],[301,2])). % 118.51/118.59 cnf(350,plain, % 118.51/118.59 (E(f3(a18,f17(a19)),f17(a19))), % 118.51/118.59 inference(scs_inference,[],[47,58,54])). % 118.51/118.59 cnf(351,plain, % 118.51/118.59 (E(f17(a19),f3(a18,f17(a19)))), % 118.51/118.59 inference(scs_inference,[],[350,2])). % 118.51/118.59 cnf(399,plain, % 118.51/118.59 (E(f16(f17(a19),a1),f17(a19))), % 118.51/118.59 inference(scs_inference,[],[47,59,54])). % 118.51/118.59 cnf(400,plain, % 118.51/118.59 (E(f17(a19),f16(f17(a19),a1))), % 118.51/118.59 inference(scs_inference,[],[399,2])). % 118.51/118.59 cnf(401,plain, % 118.51/118.59 (E(f16(a1,f17(a19)),f16(f17(a19),a1))), % 118.51/118.59 inference(scs_inference,[],[301,399,2,3])). % 118.51/118.60 cnf(406,plain, % 118.51/118.60 (E(f16(f17(a19),a1),f16(a1,f17(a19)))), % 118.51/118.60 inference(scs_inference,[],[401,2])). % 118.51/118.60 cnf(1368,plain, % 118.51/118.60 (E(f16(x13681,f16(a1,f17(a19))),f16(x13681,f17(a19)))), % 118.51/118.60 inference(scs_inference,[],[302,7,2])). % 118.51/118.60 cnf(3788,plain, % 118.51/118.60 (P4(a21)), % 118.51/118.60 inference(scs_inference,[],[49,53])). % 118.51/118.60 cnf(3791,plain, % 118.51/118.60 (P4(a20)), % 118.51/118.60 inference(scs_inference,[],[48,53])). % 118.51/118.60 cnf(3804,plain, % 118.51/118.60 (~E(a18,a1)), % 118.51/118.60 inference(scs_inference,[],[52,2])). % 118.51/118.60 cnf(3871,plain, % 118.51/118.60 (P4(f15(a20,a20))), % 118.51/118.60 inference(scs_inference,[],[3791,104])). % 118.51/118.60 cnf(3877,plain, % 118.51/118.60 (P4(f15(f15(a20,a20),f15(a20,a20)))), % 118.51/118.60 inference(scs_inference,[],[3871,104])). % 118.51/118.60 cnf(5053,plain, % 118.51/118.60 (~P3(x50531,f15(f2(a20,a20),a21))+~P3(x50532,a20)+~E(f16(x50532,x50531),a22)), % 118.51/118.60 inference(scs_inference,[],[3788,129,75,105])). % 118.51/118.60 cnf(6082,plain, % 118.51/118.60 (P3(f10(a20,a21,f2(a20,a21),a23),a20)), % 118.51/118.60 inference(scs_inference,[],[49,51,3791,53,108])). % 118.51/118.60 cnf(6117,plain, % 118.51/118.60 (P3(f11(a20,a21,f2(a20,a21),a23),a21)), % 118.51/118.60 inference(scs_inference,[],[49,51,3791,53,109])). % 118.51/118.60 cnf(6183,plain, % 118.51/118.60 (P3(f10(a20,a21,f2(a20,a21),a23),f15(a20,a20))), % 118.51/118.60 inference(scs_inference,[],[48,6082,53,107])). % 118.51/118.60 cnf(6502,plain, % 118.51/118.60 (P3(f10(a20,a21,f2(a20,a21),a23),f15(f15(a20,a20),f15(a20,a20)))), % 118.51/118.60 inference(scs_inference,[],[3871,6183,107])). % 118.51/118.60 cnf(7095,plain, % 118.51/118.60 (P1(f11(a20,a21,f2(a20,a21),a23))), % 118.51/118.60 inference(scs_inference,[],[49,6117,53,66])). % 118.51/118.60 cnf(7573,plain, % 118.51/118.60 (E(f16(a1,a1),a1)), % 118.51/118.60 inference(scs_inference,[],[45,57])). % 118.51/118.60 cnf(7575,plain, % 118.51/118.60 (E(f3(a18,a1),a1)), % 118.51/118.60 inference(scs_inference,[],[45,57,58])). % 118.51/118.60 cnf(7581,plain, % 118.51/118.60 (E(f3(a1,a1),a1)), % 118.51/118.60 inference(scs_inference,[],[45,7095,57,58,59,60,55])). % 118.51/118.60 cnf(7589,plain, % 118.51/118.60 (E(f16(f17(a1),a1),a1)), % 118.51/118.60 inference(scs_inference,[],[45,7095,351,57,58,59,60,55,56,8,11,16,39,61])). % 118.51/118.60 cnf(7591,plain, % 118.51/118.60 (E(f16(a1,f17(a1)),a1)), % 118.51/118.60 inference(scs_inference,[],[45,7095,351,57,58,59,60,55,56,8,11,16,39,61,62])). % 118.51/118.60 cnf(7597,plain, % 118.51/118.60 (E(f3(f17(a19),x75971),f3(f3(a18,f17(a19)),x75971))), % 118.51/118.60 inference(scs_inference,[],[45,7095,351,57,58,59,60,55,56,8,11,16,39,61,62,4,5,6,7,9])). % 118.51/118.60 cnf(7607,plain, % 118.51/118.60 (E(f3(f17(a18),a1),f17(a1))), % 118.51/118.60 inference(scs_inference,[],[45,7095,351,57,58,59,60,55,56,8,11,16,39,61,62,4,5,6,7,9,10,21,22,29,30,31,32,63,64])). % 118.51/118.60 cnf(7629,plain, % 118.51/118.60 (P1(f17(a1))), % 118.51/118.60 inference(scs_inference,[],[45,7095,351,57,58,59,60,55,56,8,11,16,39,61,62,4,5,6,7,9,10,21,22,29,30,31,32,63,64,23,24,25,26,27,28,33,34,35,36,37,38,12,13,14,15,17,18,19,20,54])). % 118.51/118.60 cnf(7631,plain, % 118.51/118.60 (P1(f3(a1,a1))), % 118.51/118.60 inference(scs_inference,[],[45,7095,351,57,58,59,60,55,56,8,11,16,39,61,62,4,5,6,7,9,10,21,22,29,30,31,32,63,64,23,24,25,26,27,28,33,34,35,36,37,38,12,13,14,15,17,18,19,20,54,74])). % 118.51/118.60 cnf(7637,plain, % 118.51/118.60 (P1(f16(a1,a1))), % 118.51/118.60 inference(scs_inference,[],[45,7095,351,6117,6082,3877,57,58,59,60,55,56,8,11,16,39,61,62,4,5,6,7,9,10,21,22,29,30,31,32,63,64,23,24,25,26,27,28,33,34,35,36,37,38,12,13,14,15,17,18,19,20,54,74,75,103,73])). % 118.51/118.60 cnf(7653,plain, % 118.51/118.60 (E(f16(f10(a20,a21,f2(a20,a21),a22),f11(a20,a21,f2(a20,a21),a22)),a22)), % 118.51/118.60 inference(scs_inference,[],[45,1368,7095,351,401,49,6117,6082,3877,50,3788,3791,57,58,59,60,55,56,8,11,16,39,61,62,4,5,6,7,9,10,21,22,29,30,31,32,63,64,23,24,25,26,27,28,33,34,35,36,37,38,12,13,14,15,17,18,19,20,54,74,75,103,73,3,104,79,82,83,88,89,110])). % 118.51/118.60 cnf(7655,plain, % 118.51/118.60 (P3(f3(a1,f11(a20,a21,f2(a20,a21),a23)),a21)), % 118.51/118.60 inference(scs_inference,[],[45,1368,7095,351,401,49,6117,6082,3877,50,3788,3791,57,58,59,60,55,56,8,11,16,39,61,62,4,5,6,7,9,10,21,22,29,30,31,32,63,64,23,24,25,26,27,28,33,34,35,36,37,38,12,13,14,15,17,18,19,20,54,74,75,103,73,3,104,79,82,83,88,89,110,78])). % 118.51/118.60 cnf(7657,plain, % 118.51/118.60 (~E(f3(a18,a18),a1)), % 118.51/118.60 inference(scs_inference,[],[45,1368,3804,7095,351,401,49,46,6117,6082,3877,50,3788,3791,57,58,59,60,55,56,8,11,16,39,61,62,4,5,6,7,9,10,21,22,29,30,31,32,63,64,23,24,25,26,27,28,33,34,35,36,37,38,12,13,14,15,17,18,19,20,54,74,75,103,73,3,104,79,82,83,88,89,110,78,67])). % 118.51/118.60 cnf(7664,plain, % 118.51/118.60 (P3(f11(a20,a21,f2(a20,a21),a22),a21)), % 118.51/118.60 inference(scs_inference,[],[45,1368,3804,7095,351,6502,401,49,46,6117,6082,3877,50,3788,3791,57,58,59,60,55,56,8,11,16,39,61,62,4,5,6,7,9,10,21,22,29,30,31,32,63,64,23,24,25,26,27,28,33,34,35,36,37,38,12,13,14,15,17,18,19,20,54,74,75,103,73,3,104,79,82,83,88,89,110,78,67,107,2,65,109])). % 118.51/118.60 cnf(7666,plain, % 118.51/118.60 (P3(f10(a20,a21,f2(a20,a21),a22),a20)), % 118.51/118.60 inference(scs_inference,[],[45,1368,3804,7095,351,6502,401,49,46,6117,6082,3877,50,3788,3791,57,58,59,60,55,56,8,11,16,39,61,62,4,5,6,7,9,10,21,22,29,30,31,32,63,64,23,24,25,26,27,28,33,34,35,36,37,38,12,13,14,15,17,18,19,20,54,74,75,103,73,3,104,79,82,83,88,89,110,78,67,107,2,65,109,108])). % 118.51/118.60 cnf(7688,plain, % 118.51/118.60 (E(f3(x76881,f16(a1,a1)),f3(x76881,a1))), % 118.51/118.60 inference(scs_inference,[],[7573,7631,64,55,61,56,4,12,14,18,39,21,28,58,30,10])). % 118.51/118.60 cnf(7728,plain, % 118.51/118.60 (~E(a1,f3(a18,a18))), % 118.51/118.60 inference(scs_inference,[],[7573,7631,7657,64,55,61,56,4,12,14,18,39,21,28,58,30,10,60,38,5,33,25,63,29,34,16,57,7,15,59,62,27,22,35,11,19,54,20,23,36,24,9,37,26,8,17,6,31,13,32,2])). % 118.51/118.60 cnf(7729,plain, % 118.51/118.60 (P1(f3(f3(a1,a1),f3(a1,a1)))), % 118.51/118.60 inference(scs_inference,[],[7573,7631,7657,64,55,61,56,4,12,14,18,39,21,28,58,30,10,60,38,5,33,25,63,29,34,16,57,7,15,59,62,27,22,35,11,19,54,20,23,36,24,9,37,26,8,17,6,31,13,32,2,74])). % 118.51/118.60 cnf(7731,plain, % 118.51/118.60 (P1(f16(f3(a1,a1),f3(a1,a1)))), % 118.51/118.60 inference(scs_inference,[],[7573,7631,7657,64,55,61,56,4,12,14,18,39,21,28,58,30,10,60,38,5,33,25,63,29,34,16,57,7,15,59,62,27,22,35,11,19,54,20,23,36,24,9,37,26,8,17,6,31,13,32,2,74,73])). % 118.51/118.60 cnf(7733,plain, % 118.51/118.60 (~E(f3(a18,a18),f16(a1,a1))), % 118.51/118.60 inference(scs_inference,[],[7573,7631,7657,64,55,61,56,4,12,14,18,39,21,28,58,30,10,60,38,5,33,25,63,29,34,16,57,7,15,59,62,27,22,35,11,19,54,20,23,36,24,9,37,26,8,17,6,31,13,32,2,74,73,3])). % 118.51/118.60 cnf(7762,plain, % 118.51/118.60 (E(f3(x77621,f3(a1,a1)),f3(x77621,a1))), % 118.51/118.60 inference(scs_inference,[],[7581,7629,55,21,30,56,64,63,25,10])). % 118.51/118.60 cnf(7795,plain, % 118.51/118.60 (E(f16(f3(a1,a1),x77951),f16(a1,x77951))), % 118.51/118.60 inference(scs_inference,[],[7581,7629,55,21,30,56,64,63,25,10,33,39,54,61,34,59,4,58,38,12,28,18,11,29,60,62,27,15,19,57,9,26,14,24,35,6])). % 118.51/118.60 cnf(7834,plain, % 118.51/118.60 (E(f16(f3(a1,a18),a1),f3(a1,a18))), % 118.51/118.60 inference(scs_inference,[],[7637,145,64,59])). % 118.51/118.60 cnf(7840,plain, % 118.51/118.60 (E(f3(a18,f16(a1,a1)),f16(a1,a1))), % 118.51/118.60 inference(scs_inference,[],[7729,7637,145,64,59,63,56,58])). % 118.51/118.60 cnf(7856,plain, % 118.51/118.60 (E(f3(x78561,f3(a18,a1)),f3(x78561,a1))), % 118.51/118.60 inference(scs_inference,[],[7575,7729,7637,145,64,59,63,56,58,54,39,55,34,28,12,21,29,33,61,11,10])). % 118.51/118.60 cnf(7860,plain, % 118.51/118.60 (E(f16(a1,f3(a1,a18)),f3(a1,a18))), % 118.51/118.60 inference(scs_inference,[],[7575,7729,7637,145,64,59,63,56,58,54,39,55,34,28,12,21,29,33,61,11,10,24,15,30,57])). % 118.51/118.60 cnf(7862,plain, % 118.51/118.60 (E(f3(f16(a1,a1),a18),f16(a1,a1))), % 118.51/118.60 inference(scs_inference,[],[7575,7729,7637,145,64,59,63,56,58,54,39,55,34,28,12,21,29,33,61,11,10,24,15,30,57,60])). % 118.51/118.60 cnf(7890,plain, % 118.51/118.60 (P1(f3(f16(a1,a1),f16(a1,a1)))), % 118.51/118.60 inference(scs_inference,[],[7575,7729,7637,145,64,59,63,56,58,54,39,55,34,28,12,21,29,33,61,11,10,24,15,30,57,60,18,9,25,62,35,32,6,14,16,38,8,19,4,27,5,31,26,23,20,7,37,13,22,17,36,74])). % 118.51/118.60 cnf(7892,plain, % 118.51/118.60 (P1(f16(f16(a1,a1),f16(a1,a1)))), % 118.51/118.60 inference(scs_inference,[],[7575,7729,7637,145,64,59,63,56,58,54,39,55,34,28,12,21,29,33,61,11,10,24,15,30,57,60,18,9,25,62,35,32,6,14,16,38,8,19,4,27,5,31,26,23,20,7,37,13,22,17,36,74,73])). % 118.51/118.60 cnf(7894,plain, % 118.51/118.60 (~E(f3(f17(a19),a1),f3(a18,a18))), % 118.51/118.60 inference(scs_inference,[],[7575,7728,7729,7637,145,267,64,59,63,56,58,54,39,55,34,28,12,21,29,33,61,11,10,24,15,30,57,60,18,9,25,62,35,32,6,14,16,38,8,19,4,27,5,31,26,23,20,7,37,13,22,17,36,74,73,3])). % 118.51/118.60 cnf(7902,plain, % 118.51/118.60 (E(f16(a19,a1),a19)), % 118.51/118.60 inference(scs_inference,[],[47,59])). % 118.51/118.60 cnf(7921,plain, % 118.51/118.60 (E(f16(a1,a19),a19)), % 118.51/118.60 inference(scs_inference,[],[7890,7589,145,47,59,58,54,55,56,64,60,28,63,29,34,57])). % 118.51/118.60 cnf(7960,plain, % 118.51/118.60 (P1(f3(f3(a1,a18),f3(a1,a18)))), % 118.51/118.60 inference(scs_inference,[],[7890,7589,145,47,59,58,54,55,56,64,60,28,63,29,34,57,33,62,15,24,12,39,11,61,38,6,30,8,21,26,10,31,19,16,35,20,25,32,4,18,9,14,13,27,5,7,36,23,22,37,17,74])). % 118.51/118.60 cnf(7962,plain, % 118.51/118.60 (P1(f16(f3(a1,a18),f3(a1,a18)))), % 118.51/118.60 inference(scs_inference,[],[7890,7589,145,47,59,58,54,55,56,64,60,28,63,29,34,57,33,62,15,24,12,39,11,61,38,6,30,8,21,26,10,31,19,16,35,20,25,32,4,18,9,14,13,27,5,7,36,23,22,37,17,74,73])). % 118.51/118.60 cnf(7974,plain, % 118.51/118.60 (E(f3(a18,a19),a19)), % 118.51/118.60 inference(scs_inference,[],[7960,47,56,58])). % 118.51/118.60 cnf(7978,plain, % 118.51/118.60 (E(f3(f17(a18),a19),f17(a19))), % 118.51/118.60 inference(scs_inference,[],[7960,47,56,58,63,64])). % 118.51/118.60 cnf(7982,plain, % 118.51/118.60 (E(f16(a19,f17(a19)),a1)), % 118.51/118.60 inference(scs_inference,[],[7960,47,56,58,63,64,55,62])). % 118.51/118.60 cnf(7984,plain, % 118.51/118.60 (E(f16(a18,a1),a18)), % 118.51/118.60 inference(scs_inference,[],[7960,47,46,56,58,63,64,55,62,59])). % 118.51/118.60 cnf(7995,plain, % 118.51/118.60 (E(f16(a1,a18),a18)), % 118.51/118.60 inference(scs_inference,[],[7902,7960,47,46,56,58,63,64,55,62,59,29,54,33,60,28,61,57])). % 118.51/118.60 cnf(8030,plain, % 118.51/118.60 (P1(f3(a19,a19))), % 118.51/118.60 inference(scs_inference,[],[7902,7960,47,46,56,58,63,64,55,62,59,29,54,33,60,28,61,57,11,34,39,24,6,38,20,19,26,12,15,25,13,14,32,35,10,5,21,31,30,4,8,16,23,18,7,9,17,27,22,36,37,74])). % 118.51/118.60 cnf(8032,plain, % 118.51/118.60 (P1(f16(a19,a19))), % 118.51/118.60 inference(scs_inference,[],[7902,7960,47,46,56,58,63,64,55,62,59,29,54,33,60,28,61,57,11,34,39,24,6,38,20,19,26,12,15,25,13,14,32,35,10,5,21,31,30,4,8,16,23,18,7,9,17,27,22,36,37,74,73])). % 118.51/118.60 cnf(8036,plain, % 118.51/118.60 (~P3(x80361,f15(f2(a20,a20),a21))+~E(f16(f10(a20,a21,f2(a20,a21),a22),x80361),a22)), % 118.51/118.60 inference(scs_inference,[],[7902,7960,7894,7666,274,47,46,56,58,63,64,55,62,59,29,54,33,60,28,61,57,11,34,39,24,6,38,20,19,26,12,15,25,13,14,32,35,10,5,21,31,30,4,8,16,23,18,7,9,17,27,22,36,37,74,73,3,2,5053])). % 118.51/118.60 cnf(8100,plain, % 118.51/118.60 (P1(f16(f3(a19,a19),f3(a19,a19)))), % 118.51/118.60 inference(scs_inference,[],[8030,7921,7834,268,61,38,24,20,26,19,12,6,39,15,13,5,35,7,4,8,18,32,14,10,9,31,25,23,27,30,21,37,16,17,22,36,63,64,55,58,56,59,29,62,33,57,54,60,11,34,28,3,73])). % 118.51/118.60 cnf(8143,plain, % 118.51/118.60 (E(f3(a18,a18),a18)), % 118.51/118.60 inference(scs_inference,[],[46,7974,61,24,38,26,20,6,15,12,19,4,5,25,8,9,31,10,39,7,32,23,13,27,14,35,21,18,30,37,17,36,16,22,58])). % 118.51/118.60 cnf(8153,plain, % 118.51/118.60 (E(f3(a1,f16(a19,a19)),a1)), % 118.51/118.60 inference(scs_inference,[],[46,8032,7974,61,24,38,26,20,6,15,12,19,4,5,25,8,9,31,10,39,7,32,23,13,27,14,35,21,18,30,37,17,36,16,22,58,56,64,63,62,55])). % 118.51/118.60 cnf(8161,plain, % 118.51/118.60 (P1(f17(a18))), % 118.51/118.60 inference(scs_inference,[],[46,8032,7974,61,24,38,26,20,6,15,12,19,4,5,25,8,9,31,10,39,7,32,23,13,27,14,35,21,18,30,37,17,36,16,22,58,56,64,63,62,55,57,60,59,54])). % 118.51/118.60 cnf(8168,plain, % 118.51/118.60 (~E(a18,f16(a1,a1))), % 118.51/118.60 inference(scs_inference,[],[46,8032,7974,7733,61,24,38,26,20,6,15,12,19,4,5,25,8,9,31,10,39,7,32,23,13,27,14,35,21,18,30,37,17,36,16,22,58,56,64,63,62,55,57,60,59,54,33,29,28,11,34,3])). % 118.51/118.60 cnf(8169,plain, % 118.51/118.60 (P1(f16(a18,a18))), % 118.51/118.60 inference(scs_inference,[],[46,8032,7974,7733,61,24,38,26,20,6,15,12,19,4,5,25,8,9,31,10,39,7,32,23,13,27,14,35,21,18,30,37,17,36,16,22,58,56,64,63,62,55,57,60,59,54,33,29,28,11,34,3,73])). % 118.51/118.60 cnf(8171,plain, % 118.51/118.60 (P1(f3(a18,a18))), % 118.51/118.60 inference(scs_inference,[],[46,8032,7974,7733,61,24,38,26,20,6,15,12,19,4,5,25,8,9,31,10,39,7,32,23,13,27,14,35,21,18,30,37,17,36,16,22,58,56,64,63,62,55,57,60,59,54,33,29,28,11,34,3,73,74])). % 118.51/118.60 cnf(8173,plain, % 118.51/118.60 (~E(f3(f3(a18,a18),a18),a1)), % 118.51/118.60 inference(scs_inference,[],[46,8032,7974,7733,3804,7657,61,24,38,26,20,6,15,12,19,4,5,25,8,9,31,10,39,7,32,23,13,27,14,35,21,18,30,37,17,36,16,22,58,56,64,63,62,55,57,60,59,54,33,29,28,11,34,3,73,74,67])). % 118.51/118.60 cnf(8196,plain, % 118.51/118.60 (E(f3(f3(a18,a18),x81961),f3(a18,x81961))), % 118.51/118.60 inference(scs_inference,[],[8171,8143,61,24,38,20,26,6,15,12,19,4,8,31,5,25,9])). % 118.51/118.60 cnf(8231,plain, % 118.51/118.60 (E(f16(f3(a18,a18),a1),f3(a18,a18))), % 118.51/118.60 inference(scs_inference,[],[8171,8169,8143,8173,61,24,38,20,26,6,15,12,19,4,8,31,5,25,9,10,39,7,23,32,13,27,14,35,21,18,30,17,36,37,16,22,58,56,64,63,55,62,60,57,2,59])). % 118.51/118.60 cnf(8233,plain, % 118.51/118.60 (P1(f17(f3(a18,a18)))), % 118.51/118.60 inference(scs_inference,[],[8171,8169,8143,8173,61,24,38,20,26,6,15,12,19,4,8,31,5,25,9,10,39,7,23,32,13,27,14,35,21,18,30,17,36,37,16,22,58,56,64,63,55,62,60,57,2,59,54])). % 118.51/118.60 cnf(8243,plain, % 118.51/118.60 (P1(f3(f3(a18,a18),f3(a18,a18)))), % 118.51/118.60 inference(scs_inference,[],[8171,8169,8143,7860,8173,268,61,24,38,20,26,6,15,12,19,4,8,31,5,25,9,10,39,7,23,32,13,27,14,35,21,18,30,17,36,37,16,22,58,56,64,63,55,62,60,57,2,59,54,33,29,28,11,34,3,73,74])). % 118.51/118.60 cnf(8247,plain, % 118.51/118.60 (~E(f3(f3(a18,a18),f3(a18,a18)),a1)), % 118.51/118.60 inference(scs_inference,[],[46,8171,8169,8143,7860,8173,7666,7657,268,48,61,24,38,20,26,6,15,12,19,4,8,31,5,25,9,10,39,7,23,32,13,27,14,35,21,18,30,17,36,37,16,22,58,56,64,63,55,62,60,57,2,59,54,33,29,28,11,34,3,73,74,78,67])). % 118.51/118.60 cnf(8297,plain, % 118.51/118.60 (E(f3(a1,f17(a18)),a1)), % 118.51/118.60 inference(scs_inference,[],[7984,8161,8169,8032,61,24,38,26,20,15,6,12,19,5,9,4,8,31,25,10,7,39,32,23,13,14,27,35,21,18,30,37,36,17,16,22,58,56,64,63,62,55])). % 118.51/118.60 cnf(8311,plain, % 118.51/118.60 (~E(a18,f3(a18,f16(a1,a1)))), % 118.51/118.60 inference(scs_inference,[],[7984,8168,8161,7840,8247,8169,8032,61,24,38,26,20,15,6,12,19,5,9,4,8,31,25,10,7,39,32,23,13,14,27,35,21,18,30,37,36,17,16,22,58,56,64,63,62,55,57,2,59,54,33,29,28,11,34,3])). % 118.51/118.60 cnf(8312,plain, % 118.51/118.60 (P1(f16(f17(a18),f17(a18)))), % 118.51/118.60 inference(scs_inference,[],[7984,8168,8161,7840,8247,8169,8032,61,24,38,26,20,15,6,12,19,5,9,4,8,31,25,10,7,39,32,23,13,14,27,35,21,18,30,37,36,17,16,22,58,56,64,63,62,55,57,2,59,54,33,29,28,11,34,3,73])). % 118.51/118.60 cnf(8335,plain, % 118.51/118.60 (E(f3(f16(a1,a18),x83351),f3(a18,x83351))), % 118.51/118.60 inference(scs_inference,[],[7995,8169,61,24,38,20,26,6,15,12,19,8,25,5,9])). % 118.51/118.60 cnf(8367,plain, % 118.51/118.60 (~E(f3(a18,f16(a1,a1)),a18)), % 118.51/118.60 inference(scs_inference,[],[7995,8233,8311,8169,8032,61,24,38,20,26,6,15,12,19,8,25,5,9,4,31,10,39,7,23,32,13,27,14,35,21,18,30,17,37,36,16,22,56,64,63,55,62,57,2])). % 118.51/118.60 cnf(8378,plain, % 118.51/118.60 (P1(f16(f16(a18,a18),f16(a18,a18)))), % 118.51/118.60 inference(scs_inference,[],[7995,7862,8233,8311,8169,8032,7573,61,24,38,20,26,6,15,12,19,8,25,5,9,4,31,10,39,7,23,32,13,27,14,35,21,18,30,17,37,36,16,22,56,64,63,55,62,57,2,59,54,33,29,28,11,34,3,73])). % 118.51/118.60 cnf(8520,plain, % 118.51/118.60 (E(f3(x85201,f16(a1,f17(a1))),f3(x85201,a1))), % 118.51/118.60 inference(scs_inference,[],[7591,24,38,20,26,6,15,12,19,25,31,9,4,5,8,7,39,10])). % 118.51/118.60 cnf(8646,plain, % 118.51/118.60 (~E(a18,f3(a18,a1))), % 118.51/118.60 inference(scs_inference,[],[7688,8378,7982,8367,24,38,20,26,15,6,19,12,31,25,5,8,9,4,39,10,7,23,32,13,14,27,35,21,18,17,36,37,30,22,16,56,55,54,33,29,28,11,34,3,2])). % 118.51/118.60 cnf(8677,plain, % 118.51/118.60 (~E(a18,f3(a18,f3(a1,a1)))), % 118.51/118.60 inference(scs_inference,[],[7762,7892,8297,8646,55,54,9,10,3])). % 118.51/118.60 cnf(8723,plain, % 118.51/118.60 (~E(f3(f3(a18,a18),f3(a1,a1)),a18)), % 118.51/118.60 inference(scs_inference,[],[8196,8677,7655,3788,3,107,2])). % 118.51/118.60 cnf(8732,plain, % 118.51/118.60 (P1(f17(a19))), % 118.51/118.60 inference(scs_inference,[],[47,54])). % 118.51/118.60 cnf(8772,plain, % 118.51/118.60 (~E(a18,f3(f3(a18,a18),a1))), % 118.51/118.60 inference(scs_inference,[],[47,8723,7762,3,55,2])). % 118.51/118.60 cnf(8872,plain, % 118.51/118.60 (~E(f3(f3(a18,a18),f3(a18,a1)),a18)), % 118.51/118.60 inference(scs_inference,[],[7856,8772,3,2])). % 118.51/118.60 cnf(8904,plain, % 118.51/118.60 (~E(a18,f3(a18,f3(a18,a1)))), % 118.51/118.60 inference(scs_inference,[],[8100,8872,8196,3,55,2])). % 118.51/118.60 cnf(8946,plain, % 118.51/118.60 (~E(f3(f16(a1,a18),f3(a18,a1)),a18)), % 118.51/118.60 inference(scs_inference,[],[7795,8335,7731,8904,40,3,2])). % 118.51/118.60 cnf(8953,plain, % 118.51/118.60 (E(f16(f3(a18,a18),a1),a18)), % 118.51/118.60 inference(scs_inference,[],[8231,8143,3])). % 118.51/118.60 cnf(8978,plain, % 118.51/118.60 (~E(a18,f3(f16(a1,a18),a1))), % 118.51/118.60 inference(scs_inference,[],[7962,8953,8946,7856,3,16,22,55,2])). % 118.51/118.60 cnf(9025,plain, % 118.51/118.60 (~E(a18,f3(f16(a1,a18),f16(a1,f17(a1))))), % 118.51/118.60 inference(scs_inference,[],[8520,8978,3])). % 118.51/118.60 cnf(9047,plain, % 118.51/118.60 (P3(f3(f17(a19),f10(a20,a21,f2(a20,a21),a22)),a20)), % 118.51/118.60 inference(scs_inference,[],[48,7607,7978,8312,8153,9025,8732,400,7666,2,3,54,11,6,12,5,31,8,7,32,13,14,41,78])). % 118.51/118.60 cnf(9635,plain, % 118.51/118.60 ($false), % 118.51/118.60 inference(scs_inference,[],[406,8143,7575,8032,9047,7666,7664,7657,7729,8196,8243,7597,7653,57,13,60,63,4,64,32,9,8,5,7,58,31,12,6,11,2,61,54,14,59,62,8036,41,42,40,3,75]), % 118.51/118.60 ['proof']). % 118.51/118.60 % SZS output end Proof % 118.51/118.60 % Total time :117.850000s %------------------------------------------------------------------------------