%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM423+3 : 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 : n029.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 12:24:11 EDT 2024 % Result : Theorem 117.88s 117.93s % Output : CNFRefutation 117.88s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.14 % Problem : NUM423+3 : TPTP v8.2.0. Released v4.0.0. % 0.09/0.14 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.14/0.36 % Computer : n029.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 300 % 0.14/0.36 % DateTime : Sat Jun 22 21:04:09 EDT 2024 % 0.14/0.36 % CPUTime : % 0.22/0.60 start to proof:theBenchmark % 117.88/117.92 %------------------------------------------- % 117.88/117.92 % File :CSE---1.7 % 117.88/117.92 % Problem :theBenchmark % 117.88/117.92 % Transform :cnf % 117.88/117.92 % Format :tptp:raw % 117.88/117.92 % Command :java -jar mcs_scs.jar %d %s % 117.88/117.92 % 117.88/117.92 % Result :Theorem 117.260000s % 117.88/117.92 % Output :CNFRefutation 117.260000s % 117.88/117.92 %------------------------------------------- % 117.88/117.92 %------------------------------------------------------------------------------ % 117.88/117.92 % File : NUM423+3 : TPTP v8.2.0. Released v4.0.0. % 117.88/117.92 % Domain : Number Theory % 117.88/117.92 % Problem : Fuerstenberg's infinitude of primes 03, 02 expansion % 117.88/117.92 % Version : Especial. % 117.88/117.92 % English : % 117.88/117.92 % 117.88/117.92 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 117.88/117.92 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 117.88/117.92 % Source : [Pas08] % 117.88/117.92 % Names : fuerst_03.02 [Pas08] % 117.88/117.92 % 117.88/117.92 % Status : Theorem % 117.88/117.92 % Rating : 0.08 v8.2.0, 0.06 v8.1.0, 0.03 v7.1.0, 0.04 v7.0.0, 0.07 v6.4.0, 0.12 v6.3.0, 0.04 v6.1.0, 0.13 v6.0.0, 0.09 v5.5.0, 0.19 v5.4.0, 0.25 v5.3.0, 0.26 v5.2.0, 0.10 v5.1.0, 0.14 v5.0.0, 0.25 v4.1.0, 0.35 v4.0.1, 0.61 v4.0.0 % 117.88/117.92 % Syntax : Number of formulae : 21 ( 2 unt; 2 def) % 117.88/117.92 % Number of atoms : 70 ( 24 equ) % 117.88/117.92 % Maximal formula atoms : 6 ( 3 avg) % 117.88/117.92 % Number of connectives : 52 ( 3 ~; 3 |; 26 &) % 117.88/117.92 % ( 2 <=>; 18 =>; 0 <=; 0 <~>) % 117.88/117.92 % Maximal formula depth : 9 ( 5 avg) % 117.88/117.92 % Maximal term depth : 3 ( 1 avg) % 117.88/117.92 % Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty) % 117.88/117.92 % Number of functors : 7 ( 7 usr; 4 con; 0-2 aty) % 117.88/117.92 % Number of variables : 33 ( 31 !; 2 ?) % 117.88/117.93 % SPC : FOF_THM_RFO_SEQ % 117.88/117.93 % 117.88/117.93 % Comments : Problem generated by the SAD system [VLP07] % 117.88/117.93 %------------------------------------------------------------------------------ % 117.88/117.93 fof(mIntegers,axiom, % 117.88/117.93 ! [W0] : % 117.88/117.93 ( aInteger0(W0) % 117.88/117.93 => $true ) ). % 117.88/117.93 % 117.88/117.93 fof(mIntZero,axiom, % 117.88/117.93 aInteger0(sz00) ). % 117.88/117.93 % 117.88/117.93 fof(mIntOne,axiom, % 117.88/117.93 aInteger0(sz10) ). % 117.88/117.93 % 117.88/117.93 fof(mIntNeg,axiom, % 117.88/117.93 ! [W0] : % 117.88/117.93 ( aInteger0(W0) % 117.88/117.93 => aInteger0(smndt0(W0)) ) ). % 117.88/117.93 % 117.88/117.93 fof(mIntPlus,axiom, % 117.88/117.93 ! [W0,W1] : % 117.88/117.93 ( ( aInteger0(W0) % 117.88/117.93 & aInteger0(W1) ) % 117.88/117.93 => aInteger0(sdtpldt0(W0,W1)) ) ). % 117.88/117.93 % 117.88/117.93 fof(mIntMult,axiom, % 117.88/117.93 ! [W0,W1] : % 117.88/117.93 ( ( aInteger0(W0) % 117.88/117.93 & aInteger0(W1) ) % 117.88/117.93 => aInteger0(sdtasdt0(W0,W1)) ) ). % 117.88/117.93 % 117.88/117.93 fof(mAddAsso,axiom, % 117.88/117.93 ! [W0,W1,W2] : % 117.88/117.93 ( ( aInteger0(W0) % 117.88/117.93 & aInteger0(W1) % 117.88/117.93 & aInteger0(W2) ) % 117.88/117.93 => sdtpldt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtpldt0(W0,W1),W2) ) ). % 117.88/117.93 % 117.88/117.93 fof(mAddComm,axiom, % 117.88/117.93 ! [W0,W1] : % 117.88/117.93 ( ( aInteger0(W0) % 117.88/117.93 & aInteger0(W1) ) % 117.88/117.93 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 117.88/117.93 % 117.88/117.93 fof(mAddZero,axiom, % 117.88/117.93 ! [W0] : % 117.88/117.93 ( aInteger0(W0) % 117.88/117.93 => ( sdtpldt0(W0,sz00) = W0 % 117.88/117.93 & W0 = sdtpldt0(sz00,W0) ) ) ). % 117.88/117.93 % 117.88/117.93 fof(mAddNeg,axiom, % 117.88/117.93 ! [W0] : % 117.88/117.93 ( aInteger0(W0) % 117.88/117.93 => ( sdtpldt0(W0,smndt0(W0)) = sz00 % 117.88/117.93 & sz00 = sdtpldt0(smndt0(W0),W0) ) ) ). % 117.88/117.93 % 117.88/117.93 fof(mMulAsso,axiom, % 117.88/117.93 ! [W0,W1,W2] : % 117.88/117.93 ( ( aInteger0(W0) % 117.88/117.93 & aInteger0(W1) % 117.88/117.93 & aInteger0(W2) ) % 117.88/117.93 => sdtasdt0(W0,sdtasdt0(W1,W2)) = sdtasdt0(sdtasdt0(W0,W1),W2) ) ). % 117.88/117.93 % 117.88/117.93 fof(mMulComm,axiom, % 117.88/117.93 ! [W0,W1] : % 117.88/117.93 ( ( aInteger0(W0) % 117.88/117.93 & aInteger0(W1) ) % 117.88/117.93 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 117.88/117.93 % 117.88/117.93 fof(mMulOne,axiom, % 117.88/117.93 ! [W0] : % 117.88/117.93 ( aInteger0(W0) % 117.88/117.93 => ( sdtasdt0(W0,sz10) = W0 % 117.88/117.93 & W0 = sdtasdt0(sz10,W0) ) ) ). % 117.88/117.93 % 117.88/117.93 fof(mDistrib,axiom, % 117.88/117.93 ! [W0,W1,W2] : % 117.88/117.93 ( ( aInteger0(W0) % 117.88/117.93 & aInteger0(W1) % 117.88/117.93 & aInteger0(W2) ) % 117.88/117.93 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 117.88/117.93 & sdtasdt0(sdtpldt0(W0,W1),W2) = sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W1,W2)) ) ) ). % 117.88/117.93 % 117.88/117.93 fof(mMulZero,axiom, % 117.88/117.93 ! [W0] : % 117.88/117.93 ( aInteger0(W0) % 117.88/117.93 => ( sdtasdt0(W0,sz00) = sz00 % 117.88/117.93 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 117.88/117.93 % 117.88/117.93 fof(mMulMinOne,axiom, % 117.88/117.93 ! [W0] : % 117.88/117.93 ( aInteger0(W0) % 117.88/117.93 => ( sdtasdt0(smndt0(sz10),W0) = smndt0(W0) % 117.88/117.93 & smndt0(W0) = sdtasdt0(W0,smndt0(sz10)) ) ) ). % 117.88/117.93 % 117.88/117.93 fof(mZeroDiv,axiom, % 117.88/117.93 ! [W0,W1] : % 117.88/117.93 ( ( aInteger0(W0) % 117.88/117.93 & aInteger0(W1) ) % 117.88/117.93 => ( sdtasdt0(W0,W1) = sz00 % 117.88/117.93 => ( W0 = sz00 % 117.88/117.93 | W1 = sz00 ) ) ) ). % 117.88/117.93 % 117.88/117.93 fof(mDivisor,definition, % 117.88/117.93 ! [W0] : % 117.88/117.93 ( aInteger0(W0) % 117.88/117.93 => ! [W1] : % 117.88/117.93 ( aDivisorOf0(W1,W0) % 117.88/117.93 <=> ( aInteger0(W1) % 117.88/117.93 & W1 != sz00 % 117.88/117.93 & ? [W2] : % 117.88/117.93 ( aInteger0(W2) % 117.88/117.93 & sdtasdt0(W1,W2) = W0 ) ) ) ) ). % 117.88/117.93 % 117.88/117.93 fof(mEquMod,definition, % 117.88/117.93 ! [W0,W1,W2] : % 117.88/117.93 ( ( aInteger0(W0) % 117.88/117.93 & aInteger0(W1) % 117.88/117.93 & aInteger0(W2) % 117.88/117.93 & W2 != sz00 ) % 117.88/117.93 => ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 117.88/117.93 <=> aDivisorOf0(W2,sdtpldt0(W0,smndt0(W1))) ) ) ). % 117.88/117.93 % 117.88/117.93 fof(m__671,hypothesis, % 117.88/117.93 ( aInteger0(xa) % 117.88/117.93 & aInteger0(xq) % 117.88/117.93 & xq != sz00 ) ). % 117.88/117.93 % 117.88/117.93 fof(m__,conjecture, % 117.88/117.93 ( ? [W0] : % 117.88/117.93 ( aInteger0(W0) % 117.88/117.93 & sdtasdt0(xq,W0) = sdtpldt0(xa,smndt0(xa)) ) % 117.88/117.93 | aDivisorOf0(xq,sdtpldt0(xa,smndt0(xa))) % 117.88/117.93 | sdteqdtlpzmzozddtrp0(xa,xa,xq) ) ). % 117.88/117.93 % 117.88/117.93 %------------------------------------------------------------------------------ % 117.88/117.93 %------------------------------------------- % 117.88/117.93 % Proof found % 117.88/117.93 % SZS status Theorem for theBenchmark % 117.88/117.93 % SZS output start Proof % 117.88/117.93 %ClaNum:51(EqnAxiom:16) % 117.88/117.93 %VarNum:145(SingletonVarNum:51) % 117.88/117.93 %MaxLitNum:6 % 117.88/117.93 %MaxfuncDepth:2 % 117.88/117.93 %SharedTerms:14 % 117.88/117.93 %goalClause: 22 23 42 % 117.88/117.93 %singleGoalClaCount:2 % 117.88/117.93 [17]P1(a1) % 117.88/117.93 [18]P1(a6) % 117.88/117.93 [19]P1(a7) % 117.88/117.93 [20]P1(a8) % 117.88/117.93 [21]~E(a1,a8) % 117.88/117.93 [23]~P3(a7,a7,a8) % 117.88/117.93 [22]~P2(a8,f3(a7,f2(a7))) % 117.88/117.93 [24]~P1(x241)+P1(f2(x241)) % 117.88/117.93 [25]~P1(x251)+E(f4(a1,x251),a1) % 117.88/117.93 [26]~P1(x261)+E(f4(x261,a1),a1) % 117.88/117.93 [27]~P1(x271)+E(f3(a1,x271),x271) % 117.88/117.93 [28]~P1(x281)+E(f4(a6,x281),x281) % 117.88/117.93 [29]~P1(x291)+E(f3(x291,a1),x291) % 117.88/117.93 [30]~P1(x301)+E(f4(x301,a6),x301) % 117.88/117.93 [31]~P1(x311)+E(f3(f2(x311),x311),a1) % 117.88/117.93 [32]~P1(x321)+E(f3(x321,f2(x321)),a1) % 117.88/117.93 [33]~P1(x331)+E(f4(x331,f2(a6)),f2(x331)) % 117.88/117.93 [34]~P1(x341)+E(f4(f2(a6),x341),f2(x341)) % 117.88/117.93 [42]~P1(x421)+~E(f4(a8,x421),f3(a7,f2(a7))) % 117.88/117.93 [35]~P2(x351,x352)+~P1(x352)+~E(x351,a1) % 117.88/117.93 [36]~P2(x361,x362)+P1(x361)+~P1(x362) % 117.88/117.93 [38]~P1(x382)+~P1(x381)+E(f3(x381,x382),f3(x382,x381)) % 117.88/117.93 [39]~P1(x392)+~P1(x391)+E(f4(x391,x392),f4(x392,x391)) % 117.88/117.93 [40]~P1(x402)+~P1(x401)+P1(f3(x401,x402)) % 117.88/117.93 [41]~P1(x412)+~P1(x411)+P1(f4(x411,x412)) % 117.88/117.93 [43]~P1(x431)+~P2(x432,x431)+P1(f5(x431,x432)) % 117.88/117.93 [45]~P1(x452)+~P2(x451,x452)+E(f4(x451,f5(x452,x451)),x452) % 117.88/117.93 [46]~P1(x463)+~P1(x462)+~P1(x461)+E(f3(f3(x461,x462),x463),f3(x461,f3(x462,x463))) % 117.88/117.93 [47]~P1(x473)+~P1(x472)+~P1(x471)+E(f4(f4(x471,x472),x473),f4(x471,f4(x472,x473))) % 117.88/117.93 [48]~P1(x483)+~P1(x482)+~P1(x481)+E(f3(f4(x481,x482),f4(x481,x483)),f4(x481,f3(x482,x483))) % 117.88/117.93 [49]~P1(x492)+~P1(x493)+~P1(x491)+E(f3(f4(x491,x492),f4(x493,x492)),f4(f3(x491,x493),x492)) % 117.88/117.93 [37]~P1(x371)+~P1(x372)+E(x371,a1)+E(x372,a1)+~E(f4(x372,x371),a1) % 117.88/117.93 [44]~P1(x442)+~P1(x443)+~P1(x441)+P2(x441,x442)+E(x441,a1)+~E(f4(x441,x443),x442) % 117.88/117.93 [50]~P1(x503)+~P1(x502)+~P1(x501)+P3(x502,x503,x501)+E(x501,a1)+~P2(x501,f3(x502,f2(x503))) % 117.88/117.93 [51]~P1(x511)+~P1(x513)+~P1(x512)+~P3(x512,x513,x511)+E(x511,a1)+P2(x511,f3(x512,f2(x513))) % 117.88/117.93 %EqnAxiom % 117.88/117.93 [1]E(x11,x11) % 117.88/117.93 [2]E(x22,x21)+~E(x21,x22) % 117.88/117.93 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 117.88/117.93 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 117.88/117.93 [5]~E(x51,x52)+E(f3(x51,x53),f3(x52,x53)) % 117.88/117.93 [6]~E(x61,x62)+E(f3(x63,x61),f3(x63,x62)) % 117.88/117.93 [7]~E(x71,x72)+E(f4(x71,x73),f4(x72,x73)) % 117.88/117.93 [8]~E(x81,x82)+E(f4(x83,x81),f4(x83,x82)) % 117.88/117.93 [9]~E(x91,x92)+E(f5(x91,x93),f5(x92,x93)) % 117.88/117.93 [10]~E(x101,x102)+E(f5(x103,x101),f5(x103,x102)) % 117.88/117.93 [11]~P1(x111)+P1(x112)+~E(x111,x112) % 117.88/117.93 [12]P3(x122,x123,x124)+~E(x121,x122)+~P3(x121,x123,x124) % 117.88/117.93 [13]P3(x133,x132,x134)+~E(x131,x132)+~P3(x133,x131,x134) % 117.88/117.93 [14]P3(x143,x144,x142)+~E(x141,x142)+~P3(x143,x144,x141) % 117.88/117.93 [15]P2(x152,x153)+~E(x151,x152)+~P2(x151,x153) % 117.88/117.93 [16]P2(x163,x162)+~E(x161,x162)+~P2(x163,x161) % 117.88/117.93 % 117.88/117.93 %------------------------------------------- % 117.88/117.94 cnf(52,plain, % 117.88/117.94 (~P1(x521)+~P2(a1,x521)), % 117.88/117.94 inference(equality_inference,[],[35])). % 117.88/117.94 cnf(53,plain, % 117.88/117.94 (P2(x531,f4(x531,x532))+~P1(f4(x531,x532))+~P1(x532)+~P1(x531)+E(x531,a1)), % 117.88/117.94 inference(equality_inference,[],[44])). % 117.88/117.94 cnf(55,plain, % 117.88/117.94 (~P2(a1,f2(a1))), % 117.88/117.94 inference(scs_inference,[],[17,52,24])). % 117.88/117.94 cnf(56,plain, % 117.88/117.94 (E(a1,f4(a1,a6))), % 117.88/117.94 inference(scs_inference,[],[18,2,25])). % 117.88/117.94 cnf(57,plain, % 117.88/117.94 (E(f4(a1,a6),a1)), % 117.88/117.94 inference(scs_inference,[],[56,2])). % 117.88/117.94 cnf(58,plain, % 117.88/117.94 (P1(f4(a1,a6))), % 117.88/117.94 inference(scs_inference,[],[56,17,2,11])). % 117.88/117.94 cnf(59,plain, % 117.88/117.94 (~P2(f4(a1,a6),a6)), % 117.88/117.94 inference(scs_inference,[],[18,56,17,2,11,35])). % 117.88/117.94 cnf(61,plain, % 117.88/117.94 (E(f4(f2(a6),a1),a1)), % 117.88/117.94 inference(scs_inference,[],[18,26,24])). % 117.88/117.94 cnf(62,plain, % 117.88/117.94 (E(a1,f4(f2(a6),a1))), % 117.88/117.94 inference(scs_inference,[],[61,2])). % 117.88/117.94 cnf(63,plain, % 117.88/117.94 (E(f4(a1,a6),f4(f2(a6),a1))), % 117.88/117.94 inference(scs_inference,[],[57,61,2,3])). % 117.88/117.94 cnf(64,plain, % 117.88/117.94 (~P2(f4(f2(a6),a1),a6)), % 117.88/117.94 inference(scs_inference,[],[18,57,61,2,3,35])). % 117.88/117.94 cnf(67,plain, % 117.88/117.94 (E(f3(a1,f2(a6)),f2(a6))), % 117.88/117.94 inference(scs_inference,[],[18,27,24])). % 117.88/117.94 cnf(68,plain, % 117.88/117.94 (E(f2(a6),f3(a1,f2(a6)))), % 117.88/117.94 inference(scs_inference,[],[67,2])). % 117.88/117.94 cnf(69,plain, % 117.88/117.94 (~P1(f3(a1,f2(a6)))+P1(f2(a6))), % 117.88/117.94 inference(scs_inference,[],[67,2,11])). % 117.88/117.94 cnf(72,plain, % 117.88/117.94 (~P1(f2(a6))+P1(f2(a6))), % 117.88/117.94 inference(scs_inference,[],[18,17,67,2,11,36,40])). % 117.88/117.94 cnf(75,plain, % 117.88/117.94 (E(f4(f2(a6),a1),f4(a1,a6))), % 117.88/117.94 inference(scs_inference,[],[63,2])). % 117.88/117.94 cnf(76,plain, % 117.88/117.94 (~P1(f2(a6))+P1(f3(a1,f2(a6)))), % 117.88/117.94 inference(scs_inference,[],[68,63,2,11])). % 117.88/117.94 cnf(82,plain, % 117.88/117.94 (E(f4(a6,f2(a7)),f2(a7))), % 117.88/117.94 inference(scs_inference,[],[19,28,24])). % 117.88/117.94 cnf(83,plain, % 117.88/117.94 (E(f2(a7),f4(a6,f2(a7)))), % 117.88/117.94 inference(scs_inference,[],[82,2])). % 117.88/117.94 cnf(84,plain, % 117.88/117.94 (~P2(f4(a1,a6),a7)), % 117.88/117.94 inference(scs_inference,[],[19,57,82,2,35])). % 117.88/117.94 cnf(86,plain, % 117.88/117.94 (~P1(f4(a6,f2(a7)))+P1(f2(a7))), % 117.88/117.94 inference(scs_inference,[],[19,57,82,2,35,11])). % 117.88/117.94 cnf(87,plain, % 117.88/117.94 (~P1(f2(a7))+P1(f2(a7))), % 117.88/117.94 inference(scs_inference,[],[19,57,18,82,2,35,11,41])). % 117.88/117.94 cnf(92,plain, % 117.88/117.94 (~P2(f4(f2(a6),a1),a7)), % 117.88/117.94 inference(scs_inference,[],[19,61,35])). % 117.88/117.94 cnf(94,plain, % 117.88/117.94 (~P1(f2(a7))+P1(f4(a6,f2(a7)))), % 117.88/117.94 inference(scs_inference,[],[19,83,61,35,11])). % 117.88/117.94 cnf(100,plain, % 117.88/117.94 (E(f3(f2(a8),a1),f2(a8))), % 117.88/117.94 inference(scs_inference,[],[20,29,24])). % 117.88/117.94 cnf(101,plain, % 117.88/117.94 (E(f2(a8),f3(f2(a8),a1))), % 117.88/117.94 inference(scs_inference,[],[100,2])). % 117.88/117.94 cnf(104,plain, % 117.88/117.94 (~P1(f3(f2(a8),a1))+P1(f2(a8))), % 117.88/117.94 inference(scs_inference,[],[20,57,100,2,35,11])). % 117.88/117.94 cnf(107,plain, % 117.88/117.94 (~P1(f2(a8))+P1(f2(a8))), % 117.88/117.94 inference(scs_inference,[],[20,57,17,100,2,35,11,36,40])). % 117.88/117.94 cnf(112,plain, % 117.88/117.94 (~P1(f2(a8))+P1(f3(f2(a8),a1))), % 117.88/117.94 inference(scs_inference,[],[20,101,61,35,11])). % 117.88/117.94 cnf(115,plain, % 117.88/117.94 (~P2(f2(a8),a8)+P1(f3(f2(a8),a1))), % 117.88/117.94 inference(scs_inference,[],[20,101,61,35,11,104,24,36])). % 117.88/117.94 cnf(130,plain, % 117.88/117.94 (~P1(f2(a6))+P1(f3(f3(a1,f2(a6)),f3(a1,f2(a6))))), % 117.88/117.94 inference(scs_inference,[],[76,40])). % 117.88/117.94 cnf(144,plain, % 117.88/117.94 (~P2(a1,f3(f2(a8),a1))+~P2(f2(a8),a8)), % 117.88/117.94 inference(scs_inference,[],[115,52])). % 117.88/117.94 cnf(148,plain, % 117.88/117.94 (~P2(f4(a1,a6),f3(f2(a8),a1))+~P2(f2(a8),a8)), % 117.88/117.94 inference(scs_inference,[],[57,144,15])). % 117.88/117.94 cnf(159,plain, % 117.88/117.94 (~P2(f4(a1,a6),f2(a8))+~P2(f2(a8),a8)), % 117.88/117.94 inference(scs_inference,[],[101,148,16])). % 117.88/117.94 cnf(160,plain, % 117.88/117.94 (~P2(f4(f2(a6),a1),f2(a8))+~P2(f2(a8),a8)), % 117.88/117.94 inference(scs_inference,[],[75,159,15])). % 117.88/117.94 cnf(161,plain, % 117.88/117.94 (~P2(f4(f2(a6),a1),f3(f2(a8),a1))+~P2(f2(a8),a8)), % 117.88/117.94 inference(scs_inference,[],[100,160,16])). % 117.88/117.94 cnf(165,plain, % 117.88/117.94 (~P2(f3(f2(a8),a1),a8)+~P2(f4(f2(a6),a1),f3(f2(a8),a1))), % 117.88/117.94 inference(scs_inference,[],[100,161,15])). % 117.88/117.94 cnf(168,plain, % 117.88/117.94 (~P2(a1,f3(f2(a8),a1))+~P2(f3(f2(a8),a1),a8)), % 117.88/117.94 inference(scs_inference,[],[62,165,15])). % 117.88/117.94 cnf(169,plain, % 117.88/117.94 (~P2(a1,f2(a8))+~P2(f3(f2(a8),a1),a8)), % 117.88/117.94 inference(scs_inference,[],[101,168,16])). % 117.88/117.94 cnf(170,plain, % 117.88/117.94 (~P2(f2(a8),a8)+~P2(a1,f2(a8))), % 117.88/117.94 inference(scs_inference,[],[101,169,15])). % 117.88/117.94 cnf(171,plain, % 117.88/117.94 (~P2(f2(a8),x1711)+~E(x1711,a8)+~P2(a1,f2(a8))), % 117.88/117.94 inference(scs_inference,[],[170,16])). % 117.88/117.94 cnf(175,plain, % 117.88/117.94 (~P3(x1751,x1752,a8)+~E(x1751,a7)+~E(x1752,a7)), % 117.88/117.94 inference(scs_inference,[],[23,12,13])). % 117.88/117.94 cnf(178,plain, % 117.88/117.94 (~P3(f2(a6),x1781,a8)+~E(f3(a1,f2(a6)),a7)+~E(x1781,a7)), % 117.88/117.94 inference(scs_inference,[],[68,175,12])). % 117.88/117.95 cnf(179,plain, % 117.88/117.95 (~P2(f4(f2(a6),a1),a1)), % 117.88/117.95 inference(scs_inference,[],[17,61,35])). % 117.88/117.95 cnf(181,plain, % 117.88/117.95 (~P3(a7,x1811,x1812)+~E(x1812,a8)+~E(x1811,a7)), % 117.88/117.95 inference(scs_inference,[],[23,14,13])). % 117.88/117.95 cnf(184,plain, % 117.88/117.95 (~P3(a7,x1841,f2(a6))+~E(f3(a1,f2(a6)),a8)+~E(x1841,a7)), % 117.88/117.95 inference(scs_inference,[],[68,181,14])). % 117.88/117.95 cnf(195,plain, % 117.88/117.95 (~P3(f2(a6),f3(a1,a7),a8)+~E(f3(a1,f2(a6)),a7)), % 117.88/117.95 inference(scs_inference,[],[19,178,27])). % 117.88/117.95 cnf(196,plain, % 117.88/117.95 (~E(a7,f3(a1,f2(a6)))+~P3(f2(a6),f3(a1,a7),a8)), % 117.88/117.95 inference(scs_inference,[],[195,2])). % 117.88/117.95 cnf(197,plain, % 117.88/117.95 (~E(a7,f2(a6))+~P3(f2(a6),f3(a1,a7),a8)), % 117.88/117.95 inference(scs_inference,[],[68,196,3])). % 117.88/117.95 cnf(198,plain, % 117.88/117.95 (~P3(f3(a1,f2(a6)),f3(a1,a7),a8)+~E(a7,f2(a6))), % 117.88/117.95 inference(scs_inference,[],[67,197,12])). % 117.88/117.95 cnf(199,plain, % 117.88/117.95 (~P3(f3(a1,f2(a6)),x1991,a8)+~E(x1991,f3(a1,a7))+~E(a7,f2(a6))), % 117.88/117.95 inference(scs_inference,[],[198,13])). % 117.88/117.95 cnf(235,plain, % 117.88/117.95 (E(f3(a1,f2(a1)),f2(a1))), % 117.88/117.95 inference(scs_inference,[],[17,24,27])). % 117.88/117.95 cnf(236,plain, % 117.88/117.95 (E(f2(a1),f3(a1,f2(a1)))), % 117.88/117.95 inference(scs_inference,[],[235,2])). % 117.88/117.95 cnf(237,plain, % 117.88/117.95 (~P1(f3(a1,f2(a1)))+P1(f2(a1))), % 117.88/117.95 inference(scs_inference,[],[235,2,11])). % 117.88/117.95 cnf(239,plain, % 117.88/117.95 (~P1(f2(a1))+P1(f3(a1,f2(a1)))), % 117.88/117.95 inference(scs_inference,[],[236,11])). % 117.88/117.95 cnf(279,plain, % 117.88/117.95 (P1(f3(a1,f2(a6)))), % 117.88/117.95 inference(scs_inference,[],[18,24,76])). % 117.88/117.95 cnf(280,plain, % 117.88/117.95 (P1(f2(a6))), % 117.88/117.95 inference(scs_inference,[],[279,69])). % 117.88/117.95 cnf(283,plain, % 117.88/117.95 (P1(f2(a6))), % 117.88/117.95 inference(scs_inference,[],[280,72])). % 117.88/117.95 cnf(284,plain, % 117.88/117.95 (P1(f3(f3(a1,f2(a6)),f3(a1,f2(a6))))), % 117.88/117.95 inference(scs_inference,[],[280,130])). % 117.88/117.95 cnf(290,plain, % 117.88/117.95 (P1(f4(a6,f2(a7)))), % 117.88/117.95 inference(scs_inference,[],[19,24,94])). % 117.88/117.95 cnf(291,plain, % 117.88/117.95 (P1(f2(a7))), % 117.88/117.95 inference(scs_inference,[],[290,86])). % 117.88/117.95 cnf(294,plain, % 117.88/117.95 (P1(f2(a7))), % 117.88/117.95 inference(scs_inference,[],[291,87])). % 117.88/117.95 cnf(299,plain, % 117.88/117.95 (P1(f3(f2(a8),a1))), % 117.88/117.95 inference(scs_inference,[],[20,24,112])). % 117.88/117.95 cnf(300,plain, % 117.88/117.95 (P1(f2(a8))), % 117.88/117.95 inference(scs_inference,[],[299,104])). % 117.88/117.95 cnf(303,plain, % 117.88/117.95 (P1(f2(a8))), % 117.88/117.95 inference(scs_inference,[],[300,107])). % 117.88/117.95 cnf(307,plain, % 117.88/117.95 (P1(f3(a1,f2(a1)))), % 117.88/117.95 inference(scs_inference,[],[17,24,239])). % 117.88/117.95 cnf(308,plain, % 117.88/117.95 (P1(f2(a1))), % 117.88/117.95 inference(scs_inference,[],[307,237])). % 117.88/117.95 cnf(335,plain, % 117.88/117.95 (~P2(f4(a1,a6),f2(a6))), % 117.88/117.95 inference(scs_inference,[],[57,280,35])). % 117.88/117.95 cnf(356,plain, % 117.88/117.95 (~P2(f4(a1,a6),f2(a7))), % 117.88/117.95 inference(scs_inference,[],[57,291,35])). % 117.88/117.95 cnf(396,plain, % 117.88/117.95 (P1(f2(f2(a1)))), % 117.88/117.95 inference(scs_inference,[],[235,307,24,11])). % 117.88/117.95 cnf(415,plain, % 117.88/117.95 (E(f3(a1,f2(f2(a7))),f2(f2(a7)))), % 117.88/117.95 inference(scs_inference,[],[291,24,27])). % 117.88/117.95 cnf(423,plain, % 117.88/117.95 (E(f3(f2(f2(a6)),a1),f2(f2(a6)))), % 117.88/117.95 inference(scs_inference,[],[280,24,29])). % 117.88/117.95 cnf(438,plain, % 117.88/117.95 (E(f4(f2(f2(a8)),a1),a1)), % 117.88/117.95 inference(scs_inference,[],[300,24,26])). % 117.88/117.95 cnf(448,plain, % 117.88/117.95 (E(f4(f2(f2(a8)),a6),f2(f2(a8)))), % 117.88/117.95 inference(scs_inference,[],[300,24,30])). % 117.88/117.95 cnf(575,plain, % 117.88/117.95 (E(f4(f2(a1),a6),f2(a1))), % 117.88/117.95 inference(scs_inference,[],[17,24,30])). % 117.88/117.95 cnf(577,plain, % 117.88/117.95 (E(f3(a1,f2(a1)),f4(f2(a1),a6))), % 117.88/117.95 inference(scs_inference,[],[235,575,2,3])). % 117.88/117.95 cnf(578,plain, % 117.88/117.95 (P1(f4(f2(a1),a6))), % 117.88/117.95 inference(scs_inference,[],[308,235,575,2,3,11])). % 117.88/117.95 cnf(581,plain, % 117.88/117.95 (E(f3(f2(f2(a1)),f2(a1)),a1)), % 117.88/117.95 inference(scs_inference,[],[17,24,31])). % 117.88/117.95 cnf(585,plain, % 117.88/117.95 (E(x5851,a1)+~E(x5851,f3(f2(f2(a1)),f2(a1)))), % 117.88/117.95 inference(scs_inference,[],[17,577,581,2,35,3])). % 117.88/117.95 cnf(587,plain, % 117.88/117.95 (E(f3(f2(a1),f2(f2(a1))),a1)), % 117.88/117.95 inference(scs_inference,[],[17,24,32])). % 117.88/117.95 cnf(588,plain, % 117.88/117.95 (E(a1,f3(f2(f2(a1)),f2(a1)))), % 117.88/117.95 inference(scs_inference,[],[581,2])). % 117.88/117.95 cnf(589,plain, % 117.88/117.95 (E(f4(a1,a6),f3(f2(f2(a1)),f2(a1)))), % 117.88/117.95 inference(scs_inference,[],[57,581,2,3])). % 117.88/117.95 cnf(593,plain, % 117.88/117.95 (E(f4(f2(a1),f2(a6)),f2(f2(a1)))), % 117.88/117.95 inference(scs_inference,[],[17,24,33])). % 117.88/117.95 cnf(594,plain, % 117.88/117.95 (E(f2(f2(a1)),f4(f2(a1),f2(a6)))), % 117.88/117.95 inference(scs_inference,[],[593,2])). % 117.88/117.95 cnf(595,plain, % 117.88/117.95 (E(f4(f2(a6),a1),f3(f2(f2(a1)),f2(a1)))), % 117.88/117.95 inference(scs_inference,[],[75,593,589,2,3])). % 117.88/117.95 cnf(599,plain, % 117.88/117.95 (E(f4(f2(a6),f2(a1)),f2(f2(a1)))), % 117.88/117.95 inference(scs_inference,[],[17,24,34])). % 117.88/117.95 cnf(601,plain, % 117.88/117.95 (E(f4(f2(a6),f2(a1)),f4(f2(a1),f2(a6)))), % 117.88/117.95 inference(scs_inference,[],[594,595,599,2,3])). % 117.88/117.95 cnf(607,plain, % 117.88/117.95 (E(x6071,a1)+~E(x6071,f3(f2(a1),f2(f2(a1))))), % 117.88/117.95 inference(scs_inference,[],[396,599,587,2,11,3])). % 117.88/117.95 cnf(613,plain, % 117.88/117.95 (E(f4(a1,f2(a1)),a1)), % 117.88/117.95 inference(scs_inference,[],[17,24,25])). % 117.88/117.95 cnf(620,plain, % 117.88/117.95 (E(x6201,a1)+~E(x6201,f4(a1,f2(a1)))), % 117.88/117.95 inference(scs_inference,[],[601,613,2,3])). % 117.88/117.95 cnf(621,plain, % 117.88/117.95 (~P2(x6211,a1)+~E(x6211,f4(a1,f2(a1)))), % 117.88/117.95 inference(scs_inference,[],[17,601,613,2,3,35])). % 117.88/117.95 cnf(627,plain, % 117.88/117.95 (E(a1,f4(a1,f2(a1)))), % 117.88/117.95 inference(scs_inference,[],[613,2])). % 117.88/117.95 cnf(629,plain, % 117.88/117.95 (P1(f4(a1,f2(a1)))), % 117.88/117.95 inference(scs_inference,[],[17,57,613,2,3,11])). % 117.88/117.95 cnf(643,plain, % 117.88/117.95 (E(f4(a6,f2(a6)),f2(a6))), % 117.88/117.95 inference(scs_inference,[],[18,24,28])). % 117.88/117.95 cnf(645,plain, % 117.88/117.95 (E(f3(a1,f2(a6)),f4(a6,f2(a6)))), % 117.88/117.95 inference(scs_inference,[],[67,643,2,3])). % 117.88/117.95 cnf(649,plain, % 117.88/117.95 (E(f3(f2(a6),a1),f2(a6))), % 117.88/117.95 inference(scs_inference,[],[18,24,29])). % 117.88/117.95 cnf(653,plain, % 117.88/117.95 (E(x6531,f2(a6))+~E(x6531,f3(f2(a6),a1))), % 117.88/117.95 inference(scs_inference,[],[18,438,645,649,2,35,3])). % 117.88/117.95 cnf(662,plain, % 117.88/117.95 (P1(f3(f2(a6),a1))), % 117.88/117.95 inference(scs_inference,[],[283,67,649,2,3,11])). % 117.88/117.95 cnf(838,plain, % 117.88/117.95 (E(f4(a1,f2(f4(a1,a6))),a1)), % 117.88/117.95 inference(scs_inference,[],[58,24,25])). % 117.88/117.95 cnf(839,plain, % 117.88/117.95 (E(a1,f4(a1,f2(f4(a1,a6))))), % 117.88/117.95 inference(scs_inference,[],[838,2])). % 117.88/117.95 cnf(840,plain, % 117.88/117.95 (E(f4(a1,a6),f4(a1,f2(f4(a1,a6))))), % 117.88/117.95 inference(scs_inference,[],[57,838,2,3])). % 117.88/117.95 cnf(844,plain, % 117.88/117.95 (E(f4(f2(f4(a1,a6)),a1),a1)), % 117.88/117.95 inference(scs_inference,[],[58,24,26])). % 117.88/117.95 cnf(848,plain, % 117.88/117.95 (E(x8481,a1)+~E(x8481,f4(f2(f4(a1,a6)),a1))), % 117.88/117.95 inference(scs_inference,[],[58,840,844,2,35,3])). % 117.88/117.95 cnf(875,plain, % 117.88/117.95 (P1(f2(f2(a6)))), % 117.88/117.95 inference(scs_inference,[],[67,279,24,11])). % 117.88/117.95 cnf(890,plain, % 117.88/117.95 (P1(f2(f2(a7)))), % 117.88/117.95 inference(scs_inference,[],[82,290,24,11])). % 117.88/117.95 cnf(906,plain, % 117.88/117.95 (P1(f2(f2(a8)))), % 117.88/117.95 inference(scs_inference,[],[100,299,24,11])). % 117.88/117.95 cnf(907,plain, % 117.88/117.95 (~P2(f4(a1,a6),f2(f2(a8)))), % 117.88/117.95 inference(scs_inference,[],[57,906,35])). % 117.88/117.95 cnf(1115,plain, % 117.88/117.95 (E(f4(a1,f2(f2(a1))),a1)), % 117.88/117.95 inference(scs_inference,[],[308,24,25])). % 117.88/117.95 cnf(1117,plain, % 117.88/117.95 (E(f4(a1,a6),f4(a1,f2(f2(a1))))), % 117.88/117.95 inference(scs_inference,[],[57,1115,2,3])). % 117.88/117.95 cnf(1121,plain, % 117.88/117.95 (E(f4(f2(f2(a1)),a1),a1)), % 117.88/117.95 inference(scs_inference,[],[308,24,26])). % 117.88/117.95 cnf(1125,plain, % 117.88/117.95 (E(x11251,a1)+~E(x11251,f4(f2(f2(a1)),a1))), % 117.88/117.95 inference(scs_inference,[],[308,613,1117,1121,2,35,3])). % 117.88/117.95 cnf(1254,plain, % 117.88/117.95 (E(f4(a1,f2(a1)),f3(f2(f2(a1)),f2(a1)))), % 117.88/117.95 inference(scs_inference,[],[581,627,3,2])). % 117.88/117.95 cnf(1529,plain, % 117.88/117.95 (E(f3(f2(a1),a1),f2(a1))), % 117.88/117.95 inference(scs_inference,[],[17,24,29])). % 117.88/117.95 cnf(1532,plain, % 117.88/117.95 (E(f3(a1,f2(a1)),f3(f2(a1),a1))), % 117.88/117.95 inference(scs_inference,[],[308,235,1529,2,11,3])). % 117.88/117.95 cnf(1535,plain, % 117.88/117.95 (E(f4(f2(a1),a1),a1)), % 117.88/117.95 inference(scs_inference,[],[17,24,26])). % 117.88/117.95 cnf(1539,plain, % 117.88/117.95 (E(x15391,a1)+~E(x15391,f4(f2(a1),a1))), % 117.88/117.95 inference(scs_inference,[],[17,844,1532,1535,2,35,3])). % 117.88/117.95 cnf(1542,plain, % 117.88/117.95 (E(a1,f4(f2(a1),a1))), % 117.88/117.95 inference(scs_inference,[],[1535,2])). % 117.88/117.95 cnf(1543,plain, % 117.88/117.95 (P1(f4(f2(a1),a1))), % 117.88/117.95 inference(scs_inference,[],[17,1535,2,11])). % 117.88/117.95 cnf(1544,plain, % 117.88/117.95 (E(f4(a1,a6),f4(f2(a1),a1))), % 117.88/117.95 inference(scs_inference,[],[17,57,1535,2,11,3])). % 117.88/117.95 cnf(1563,plain, % 117.88/117.95 (E(f4(f2(a1),a1),f4(a1,a6))), % 117.88/117.95 inference(scs_inference,[],[1544,2])). % 117.88/117.95 cnf(1567,plain, % 117.88/117.95 (E(f4(f2(a6),a6),f2(a6))), % 117.88/117.95 inference(scs_inference,[],[18,24,30])). % 117.88/117.95 cnf(1569,plain, % 117.88/117.95 (P1(f4(f2(a6),a6))), % 117.88/117.95 inference(scs_inference,[],[283,1567,2,11])). % 117.88/117.95 cnf(1573,plain, % 117.88/117.95 (E(f3(f2(a6),f2(f2(a6))),a1)), % 117.88/117.95 inference(scs_inference,[],[18,24,32])). % 117.88/117.95 cnf(1613,plain, % 117.88/117.95 (P1(f2(f4(a7,a7)))), % 117.88/117.95 inference(scs_inference,[],[19,24,41])). % 117.88/117.95 cnf(1616,plain, % 117.88/117.95 (E(f4(a1,f2(a7)),a1)), % 117.88/117.95 inference(scs_inference,[],[19,24,25])). % 117.88/117.95 cnf(1617,plain, % 117.88/117.95 (E(a1,f4(a1,f2(a7)))), % 117.88/117.95 inference(scs_inference,[],[1616,2])). % 117.88/117.95 cnf(1618,plain, % 117.88/117.95 (P1(f4(a1,f2(a7)))), % 117.88/117.95 inference(scs_inference,[],[17,1616,2,11])). % 117.88/117.95 cnf(1622,plain, % 117.88/117.95 (E(f4(f2(a7),a1),a1)), % 117.88/117.95 inference(scs_inference,[],[19,24,26])). % 117.88/117.95 cnf(1627,plain, % 117.88/117.95 (E(f3(a1,f2(a7)),f2(a7))), % 117.88/117.95 inference(scs_inference,[],[19,24,27])). % 117.88/117.95 cnf(1628,plain, % 117.88/117.95 (E(a1,f4(f2(a7),a1))), % 117.88/117.95 inference(scs_inference,[],[1622,2])). % 117.88/117.95 cnf(1629,plain, % 117.88/117.95 (P1(f4(f2(a7),a1))), % 117.88/117.95 inference(scs_inference,[],[17,1622,2,11])). % 117.88/117.95 cnf(1630,plain, % 117.88/117.95 (E(f4(a1,a6),f4(f2(a7),a1))), % 117.88/117.95 inference(scs_inference,[],[57,17,1622,2,11,3])). % 117.88/117.95 cnf(1633,plain, % 117.88/117.95 (E(f3(f2(a7),a1),f2(a7))), % 117.88/117.95 inference(scs_inference,[],[19,24,29])). % 117.88/117.95 cnf(1638,plain, % 117.88/117.95 (E(f4(f2(a7),a6),f2(a7))), % 117.88/117.95 inference(scs_inference,[],[19,24,30])). % 117.88/117.95 cnf(1639,plain, % 117.88/117.95 (E(f2(a7),f3(a1,f2(a7)))), % 117.88/117.95 inference(scs_inference,[],[1627,2])). % 117.88/117.95 cnf(1641,plain, % 117.88/117.95 (E(f4(a6,f2(a7)),f3(a1,f2(a7)))), % 117.88/117.95 inference(scs_inference,[],[294,82,1627,2,11,3])). % 117.88/117.95 cnf(1643,plain, % 117.88/117.95 (E(f2(a7),f3(f2(a7),a1))), % 117.88/117.95 inference(scs_inference,[],[1633,2])). % 117.88/117.95 cnf(1648,plain, % 117.88/117.95 (E(f3(f2(a7),f2(f2(a7))),a1)), % 117.88/117.95 inference(scs_inference,[],[19,24,32])). % 117.88/117.95 cnf(1652,plain, % 117.88/117.95 (E(x16521,f2(a7))+~E(x16521,f4(f2(a7),a6))), % 117.88/117.95 inference(scs_inference,[],[19,1641,1638,1648,2,35,3])). % 117.88/117.95 cnf(1654,plain, % 117.88/117.95 (E(f4(f2(a7),f2(a6)),f2(f2(a7)))), % 117.88/117.95 inference(scs_inference,[],[19,24,33])). % 117.88/117.95 cnf(1658,plain, % 117.88/117.95 (E(f4(f2(a6),f2(a7)),f2(f2(a7)))), % 117.88/117.95 inference(scs_inference,[],[19,24,34])). % 117.88/117.95 cnf(1662,plain, % 117.88/117.95 (~E(f4(a8,f2(a7)),f3(a7,f2(a7)))), % 117.88/117.95 inference(scs_inference,[],[19,24,42])). % 117.88/117.95 cnf(1666,plain, % 117.88/117.95 (~P2(a1,f2(a7))), % 117.88/117.95 inference(scs_inference,[],[19,24,52])). % 117.88/117.95 cnf(1670,plain, % 117.88/117.95 (E(f2(f2(a7)),f4(f2(a7),f2(a6)))), % 117.88/117.95 inference(scs_inference,[],[1654,2])). % 117.88/117.95 cnf(1672,plain, % 117.88/117.95 (E(x16721,f2(f2(a7)))+~E(x16721,f4(f2(a6),f2(a7)))), % 117.88/117.95 inference(scs_inference,[],[890,1654,1658,2,11,3])). % 117.88/117.95 cnf(1684,plain, % 117.88/117.95 (E(f4(f2(a7),a1),f4(a1,a6))), % 117.88/117.95 inference(scs_inference,[],[1630,2])). % 117.88/117.95 cnf(1903,plain, % 117.88/117.95 (P1(f4(f2(f4(a1,a6)),f2(f4(a1,a6))))), % 117.88/117.95 inference(scs_inference,[],[58,24,41])). % 117.88/117.95 cnf(2331,plain, % 117.88/117.95 (~P2(a1,x23311)+~E(x23311,f2(f2(a6)))), % 117.88/117.95 inference(scs_inference,[],[875,52,16])). % 117.88/117.95 cnf(2344,plain, % 117.88/117.95 (E(f3(f3(a1,f2(a6)),x23441),f3(f2(a6),x23441))), % 117.88/117.95 inference(scs_inference,[],[68,2,5])). % 117.88/117.95 cnf(2348,plain, % 117.88/117.95 (E(f4(f3(a1,f2(a6)),x23481),f4(f2(a6),x23481))), % 117.88/117.95 inference(scs_inference,[],[68,2,7])). % 117.88/117.95 cnf(2349,plain, % 117.88/117.95 (~P2(f3(f2(a6),f2(f2(a6))),f2(a1))), % 117.88/117.95 inference(scs_inference,[],[308,1573,35])). % 117.88/117.95 cnf(2363,plain, % 117.88/117.95 (~E(a8,f3(f2(f2(a1)),f2(a1)))), % 117.88/117.95 inference(scs_inference,[],[21,2,585])). % 117.88/117.95 cnf(2364,plain, % 117.88/117.95 (~E(a8,a1)), % 117.88/117.95 inference(scs_inference,[],[588,2363,3])). % 117.88/117.95 cnf(2366,plain, % 117.88/117.95 (~E(a8,f4(a1,f2(a1)))), % 117.88/117.95 inference(scs_inference,[],[588,2363,3,607,620])). % 117.88/117.95 cnf(2369,plain, % 117.88/117.95 (~E(a8,f4(f2(a1),a1))), % 117.88/117.95 inference(scs_inference,[],[588,2363,3,607,620,848,1125,1539])). % 117.88/117.95 cnf(2375,plain, % 117.88/117.95 (~E(a8,f4(a1,a6))), % 117.88/117.95 inference(scs_inference,[],[57,2364,3])). % 117.88/117.95 cnf(2380,plain, % 117.88/117.95 (~E(a8,f4(f2(a6),a1))), % 117.88/117.95 inference(scs_inference,[],[75,2375,3])). % 117.88/117.95 cnf(2416,plain, % 117.88/117.95 (E(f3(f3(a1,f2(a6)),x24161),f3(f2(a6),x24161))), % 117.88/117.95 inference(rename_variables,[],[2344])). % 117.88/117.95 cnf(2419,plain, % 117.88/117.95 (P1(f2(f2(f4(a7,a7))))), % 117.88/117.95 inference(scs_inference,[],[423,2344,2348,1903,1684,1613,303,52,27,28,29,30,25,26,4,31,32,2331,5,6,7,8,9,10,33,34,42,653,1672,24])). % 117.88/117.95 cnf(2421,plain, % 117.88/117.95 (~E(f4(a1,f2(a1)),a8)), % 117.88/117.95 inference(scs_inference,[],[2366,423,2344,2348,1903,1684,1613,303,52,27,28,29,30,25,26,4,31,32,2331,5,6,7,8,9,10,33,34,42,653,1672,24,2])). % 117.88/117.95 cnf(2428,plain, % 117.88/117.95 (E(f3(f3(a1,f2(a6)),x24281),f3(f2(a6),x24281))), % 117.88/117.95 inference(rename_variables,[],[2344])). % 117.88/117.95 cnf(2442,plain, % 117.88/117.95 (~E(f4(a8,a8),a1)), % 117.88/117.95 inference(scs_inference,[],[907,2366,2349,448,415,423,2344,2416,2428,2348,1903,284,1684,1670,2364,1648,1613,303,18,20,52,27,28,29,30,25,26,4,31,32,2331,5,6,7,8,9,10,33,34,42,653,1672,24,2,41,40,16,15,11,3,35,46,47,48,49,37])). % 117.88/117.95 cnf(2447,plain, % 117.88/117.95 (E(f3(a6,a1),a6)), % 117.88/117.95 inference(scs_inference,[],[18,29])). % 117.88/117.95 cnf(2455,plain, % 117.88/117.95 (E(f4(a6,f2(a8)),f2(a8))), % 117.88/117.95 inference(scs_inference,[],[2419,578,283,303,18,29,31,52,25,28])). % 117.88/117.95 cnf(2467,plain, % 117.88/117.95 (~E(f4(a8,f2(a6)),f3(a7,f2(a7)))), % 117.88/117.95 inference(scs_inference,[],[2419,1617,578,283,303,18,20,29,31,52,25,28,27,30,5,34,33,4,42])). % 117.88/117.95 cnf(2472,plain, % 117.88/117.95 (E(f3(x24721,a1),f3(x24721,f4(a1,f2(a7))))), % 117.88/117.95 inference(scs_inference,[],[2419,1617,578,283,303,18,20,29,31,52,25,28,27,30,5,34,33,4,42,26,9,6])). % 117.88/117.95 cnf(2473,plain, % 117.88/117.95 (E(f3(a6,f2(a6)),a1)), % 117.88/117.95 inference(scs_inference,[],[2419,1617,578,283,303,18,20,29,31,52,25,28,27,30,5,34,33,4,42,26,9,6,32])). % 117.88/117.95 cnf(2475,plain, % 117.88/117.95 (E(f4(x24751,a1),f4(x24751,f4(a1,f2(a7))))), % 117.88/117.95 inference(scs_inference,[],[2419,1617,578,283,303,18,20,29,31,52,25,28,27,30,5,34,33,4,42,26,9,6,32,8])). % 117.88/117.95 cnf(2477,plain, % 117.88/117.95 (E(f4(a1,x24771),f4(f4(a1,f2(a7)),x24771))), % 117.88/117.95 inference(scs_inference,[],[2419,1617,578,283,303,18,20,29,31,52,25,28,27,30,5,34,33,4,42,26,9,6,32,8,10,7])). % 117.88/117.95 cnf(2480,plain, % 117.88/117.95 (~E(a1,f4(a8,a8))), % 117.88/117.95 inference(scs_inference,[],[2442,2419,1617,578,1543,283,303,18,20,29,31,52,25,28,27,30,5,34,33,4,42,26,9,6,32,8,10,7,24,2])). % 117.88/117.95 cnf(2481,plain, % 117.88/117.95 (P1(f4(f2(a7),f2(a7)))), % 117.88/117.95 inference(scs_inference,[],[2442,2419,1617,578,1543,294,283,303,18,20,29,31,52,25,28,27,30,5,34,33,4,42,26,9,6,32,8,10,7,24,2,41])). % 117.88/117.95 cnf(2483,plain, % 117.88/117.95 (P1(f3(f2(a6),f2(a6)))), % 117.88/117.95 inference(scs_inference,[],[2442,2419,1617,578,1543,294,283,303,18,20,29,31,52,25,28,27,30,5,34,33,4,42,26,9,6,32,8,10,7,24,2,41,40])). % 117.88/117.95 cnf(2506,plain, % 117.88/117.95 (E(f3(f4(a1,a6),a1),f4(a1,a6))), % 117.88/117.95 inference(scs_inference,[],[2481,58,25,29])). % 117.88/117.95 cnf(2512,plain, % 117.88/117.95 (E(f3(a1,a6),a6)), % 117.88/117.95 inference(scs_inference,[],[2481,18,58,25,29,31,52,27])). % 117.88/117.95 cnf(2514,plain, % 117.88/117.95 (E(f4(a6,a6),a6)), % 117.88/117.95 inference(scs_inference,[],[2481,18,58,25,29,31,52,27,28])). % 117.88/117.95 cnf(2518,plain, % 117.88/117.95 (~E(f4(a8,f2(a8)),f3(a7,f2(a7)))), % 117.88/117.95 inference(scs_inference,[],[2481,303,18,58,25,29,31,52,27,28,34,42])). % 117.88/117.95 cnf(2522,plain, % 117.88/117.95 (E(f2(f3(a6,a1)),f2(a6))), % 117.88/117.95 inference(scs_inference,[],[2447,2481,303,18,58,25,29,31,52,27,28,34,42,26,4])). % 117.88/117.95 cnf(2532,plain, % 117.88/117.95 (E(f4(x25321,f3(a6,a1)),f4(x25321,a6))), % 117.88/117.95 inference(scs_inference,[],[2447,2481,303,18,58,25,29,31,52,27,28,34,42,26,4,30,5,32,33,6,9,8])). % 117.88/117.95 cnf(2534,plain, % 117.88/117.95 (E(f4(f3(a6,a1),x25341),f4(a6,x25341))), % 117.88/117.95 inference(scs_inference,[],[2447,2481,303,18,58,25,29,31,52,27,28,34,42,26,4,30,5,32,33,6,9,8,10,7])). % 117.88/117.95 cnf(2537,plain, % 117.88/117.95 (~E(f4(f2(a1),a1),a8)), % 117.88/117.95 inference(scs_inference,[],[2447,2481,2369,1569,303,18,58,25,29,31,52,27,28,34,42,26,4,30,5,32,33,6,9,8,10,7,24,2])). % 117.88/117.95 cnf(2538,plain, % 117.88/117.95 (P1(f4(f2(a6),f2(a6)))), % 117.88/117.95 inference(scs_inference,[],[2447,2481,2369,1569,283,303,18,58,25,29,31,52,27,28,34,42,26,4,30,5,32,33,6,9,8,10,7,24,2,41])). % 117.88/117.95 cnf(2542,plain, % 117.88/117.95 (~P2(f4(a1,a6),f3(a6,a1))), % 117.88/117.95 inference(scs_inference,[],[59,2447,2481,2369,1569,283,303,18,58,25,29,31,52,27,28,34,42,26,4,30,5,32,33,6,9,8,10,7,24,2,41,40,16])). % 117.88/117.95 cnf(2555,plain, % 117.88/117.95 (E(f4(f2(a7),f3(a6,a1)),f2(a7))), % 117.88/117.95 inference(scs_inference,[],[59,55,2447,2455,2481,2369,2473,2477,101,629,1569,283,303,18,58,19,25,29,31,52,27,28,34,42,26,4,30,5,32,33,6,9,8,10,7,24,2,41,40,16,15,11,3,46,47,49,48,1652])). % 117.88/117.95 cnf(2571,plain, % 117.88/117.95 (E(f3(a8,a1),a8)), % 117.88/117.95 inference(scs_inference,[],[2538,2483,20,25,52,29])). % 117.88/117.95 cnf(2573,plain, % 117.88/117.95 (E(f3(f2(a8),a8),a1)), % 117.88/117.95 inference(scs_inference,[],[2538,2483,20,25,52,29,31])). % 117.88/117.95 cnf(2575,plain, % 117.88/117.95 (E(f4(a6,a8),a8)), % 117.88/117.96 inference(scs_inference,[],[2538,2483,20,25,52,29,31,28])). % 117.88/117.96 cnf(2577,plain, % 117.88/117.96 (E(f3(a1,a8),a8)), % 117.88/117.96 inference(scs_inference,[],[2538,2483,20,25,52,29,31,28,27])). % 117.88/117.96 cnf(2579,plain, % 117.88/117.96 (~E(f4(a8,a6),f3(a7,f2(a7)))), % 117.88/117.96 inference(scs_inference,[],[2538,2483,18,20,25,52,29,31,28,27,42])). % 117.88/117.96 cnf(2581,plain, % 117.88/117.96 (E(f4(a8,a6),a8)), % 117.88/117.96 inference(scs_inference,[],[2538,2483,18,20,25,52,29,31,28,27,42,30])). % 117.88/117.96 cnf(2587,plain, % 117.88/117.96 (E(f3(a8,f2(a8)),a1)), % 117.88/117.96 inference(scs_inference,[],[2538,2483,18,20,25,52,29,31,28,27,42,30,26,34,32])). % 117.88/117.96 cnf(2589,plain, % 117.88/117.96 (E(f3(f4(a6,a6),x25891),f3(a6,x25891))), % 117.88/117.96 inference(scs_inference,[],[2514,2538,2483,18,20,25,52,29,31,28,27,42,30,26,34,32,5])). % 117.88/117.96 cnf(2597,plain, % 117.88/117.96 (E(f4(f4(a6,a6),x25971),f4(a6,x25971))), % 117.88/117.96 inference(scs_inference,[],[2514,2538,2483,1618,18,20,19,25,52,29,31,28,27,42,30,26,34,32,5,33,4,6,9,24,7])). % 117.88/117.96 cnf(2598,plain, % 117.88/117.96 (E(f4(x25981,f4(a6,a6)),f4(x25981,a6))), % 117.88/117.96 inference(scs_inference,[],[2514,2538,2483,1618,18,20,19,25,52,29,31,28,27,42,30,26,34,32,5,33,4,6,9,24,7,8])). % 117.88/117.96 cnf(2601,plain, % 117.88/117.96 (~P3(a7,a7,f3(a8,a1))), % 117.88/117.96 inference(scs_inference,[],[2514,2538,2483,2380,23,1618,18,20,19,25,52,29,31,28,27,42,30,26,34,32,5,33,4,6,9,24,7,8,10,2,14])). % 117.88/117.96 cnf(2602,plain, % 117.88/117.96 (P1(f4(f2(a8),f2(a8)))), % 117.88/117.96 inference(scs_inference,[],[2514,2538,2483,2380,23,1618,303,18,20,19,25,52,29,31,28,27,42,30,26,34,32,5,33,4,6,9,24,7,8,10,2,14,41])). % 117.88/117.96 cnf(2604,plain, % 117.88/117.96 (P1(f3(a6,a6))), % 117.88/117.96 inference(scs_inference,[],[2514,2538,2483,2380,23,1618,303,18,20,19,25,52,29,31,28,27,42,30,26,34,32,5,33,4,6,9,24,7,8,10,2,14,41,40])). % 117.88/117.96 cnf(2610,plain, % 117.88/117.96 (~E(f4(f2(a7),a1),f4(a8,a8))), % 117.88/117.96 inference(scs_inference,[],[22,356,2514,2480,2555,2538,2483,2380,2472,1628,23,662,1618,303,18,20,19,25,52,29,31,28,27,42,30,26,34,32,5,33,4,6,9,24,7,8,10,2,14,41,40,16,15,11,3])). % 117.88/117.96 cnf(2619,plain, % 117.88/117.96 (E(f4(f2(a7),f4(a6,a6)),f2(a7))), % 117.88/117.96 inference(scs_inference,[],[22,356,2514,2480,2555,2538,2483,2380,2472,1628,23,662,1618,303,18,20,19,17,25,52,29,31,28,27,42,30,26,34,32,5,33,4,6,9,24,7,8,10,2,14,41,40,16,15,11,3,46,48,47,49,1652])). % 117.88/117.96 cnf(2622,plain, % 117.88/117.96 (~P3(a7,x26221,a8)+~E(x26221,a7)), % 117.88/117.96 inference(scs_inference,[],[22,356,2514,2480,2555,2538,2483,2380,2472,1628,23,662,1618,303,18,20,19,17,25,52,29,31,28,27,42,30,26,34,32,5,33,4,6,9,24,7,8,10,2,14,41,40,16,15,11,3,46,48,47,49,1652,171,13])). % 117.88/117.96 cnf(2628,plain, % 117.88/117.96 (~P2(a1,f3(a6,a6))), % 117.88/117.96 inference(scs_inference,[],[2604,31,25,52])). % 117.88/117.96 cnf(2638,plain, % 117.88/117.96 (E(f4(f3(a6,a6),a6),f3(a6,a6))), % 117.88/117.96 inference(scs_inference,[],[2604,31,25,52,29,27,28,26,30])). % 117.88/117.96 cnf(2654,plain, % 117.88/117.96 (E(f4(x26541,f3(a1,a6)),f4(x26541,a6))), % 117.88/117.96 inference(scs_inference,[],[2604,2512,1629,31,25,52,29,27,28,26,30,32,42,5,34,33,9,4,6,24,8])). % 117.88/117.96 cnf(2655,plain, % 117.88/117.96 (E(f4(f3(a1,a6),x26551),f4(a6,x26551))), % 117.88/117.96 inference(scs_inference,[],[2604,2512,1629,31,25,52,29,27,28,26,30,32,42,5,34,33,9,4,6,24,8,7])). % 117.88/117.96 cnf(2657,plain, % 117.88/117.96 (~E(f4(a8,a8),f4(f2(a7),a1))), % 117.88/117.96 inference(scs_inference,[],[2604,2512,2610,1629,31,25,52,29,27,28,26,30,32,42,5,34,33,9,4,6,24,8,7,10,2])). % 117.88/117.96 cnf(2658,plain, % 117.88/117.96 (~P3(a7,a7,f4(a8,a6))), % 117.88/117.96 inference(scs_inference,[],[2604,2512,2581,2610,23,1629,31,25,52,29,27,28,26,30,32,42,5,34,33,9,4,6,24,8,7,10,2,14])). % 117.88/117.96 cnf(2659,plain, % 117.88/117.96 (P1(f3(f3(a6,a6),f3(a6,a6)))), % 117.88/117.96 inference(scs_inference,[],[2604,2512,2581,2610,23,1629,31,25,52,29,27,28,26,30,32,42,5,34,33,9,4,6,24,8,7,10,2,14,40])). % 117.88/117.96 cnf(2661,plain, % 117.88/117.96 (P1(f4(f3(a6,a6),f3(a6,a6)))), % 117.88/117.96 inference(scs_inference,[],[2604,2512,2581,2610,23,1629,31,25,52,29,27,28,26,30,32,42,5,34,33,9,4,6,24,8,7,10,2,14,40,41])). % 117.88/117.96 cnf(2667,plain, % 117.88/117.96 (~E(a8,f3(a7,f2(a7)))), % 117.88/117.96 inference(scs_inference,[],[22,2604,2512,2581,2610,64,2579,2475,23,1629,31,25,52,29,27,28,26,30,32,42,5,34,33,9,4,6,24,8,7,10,2,14,40,41,16,15,11,3])). % 117.88/117.96 cnf(2668,plain, % 117.88/117.96 (E(f4(f2(a7),f3(a1,a6)),f2(a7))), % 117.88/117.96 inference(scs_inference,[],[22,2604,2512,2581,2610,64,2579,2475,23,1629,31,25,52,29,27,28,26,30,32,42,5,34,33,9,4,6,24,8,7,10,2,14,40,41,16,15,11,3,1652])). % 117.88/117.96 cnf(2669,plain, % 117.88/117.96 (~P3(x26691,a7,f3(a8,a1))+~E(x26691,a7)), % 117.88/117.96 inference(scs_inference,[],[22,2604,2512,2581,2601,2610,64,2579,2475,23,1629,31,25,52,29,27,28,26,30,32,42,5,34,33,9,4,6,24,8,7,10,2,14,40,41,16,15,11,3,1652,12])). % 117.88/117.96 cnf(2673,plain, % 117.88/117.96 (E(f3(a7,a1),a7)), % 117.88/117.96 inference(scs_inference,[],[19,29])). % 117.88/117.96 cnf(2675,plain, % 117.88/117.96 (E(f4(a7,a6),a7)), % 117.88/117.96 inference(scs_inference,[],[19,29,30])). % 117.88/117.96 cnf(2683,plain, % 117.88/117.96 (E(f3(a1,f4(a1,a6)),f4(a1,a6))), % 117.88/117.96 inference(scs_inference,[],[2602,58,19,29,30,31,25,52,27])). % 117.88/117.96 cnf(2689,plain, % 117.88/117.96 (E(f3(a7,f2(a7)),a1)), % 117.88/117.96 inference(scs_inference,[],[2602,58,19,29,30,31,25,52,27,28,42,32])). % 117.88/117.96 cnf(2695,plain, % 117.88/117.96 (E(f3(f3(a8,a1),x26951),f3(a8,x26951))), % 117.88/117.96 inference(scs_inference,[],[2571,2602,58,19,29,30,31,25,52,27,28,42,32,26,34,5])). % 117.88/117.96 cnf(2703,plain, % 117.88/117.96 (E(f4(f3(a8,a1),x27031),f4(a8,x27031))), % 117.88/117.96 inference(scs_inference,[],[2571,2602,2659,58,19,17,29,30,31,25,52,27,28,42,32,26,34,5,33,24,4,6,9,7])). % 117.88/117.96 cnf(2704,plain, % 117.88/117.96 (E(f4(x27041,f3(a8,a1)),f4(x27041,a8))), % 117.88/117.96 inference(scs_inference,[],[2571,2602,2659,58,19,17,29,30,31,25,52,27,28,42,32,26,34,5,33,24,4,6,9,7,8])). % 117.88/117.96 cnf(2707,plain, % 117.88/117.96 (~P3(f3(a7,a1),f3(a7,a1),a8)), % 117.88/117.96 inference(scs_inference,[],[2571,2602,2659,2667,58,19,17,29,30,31,25,52,27,28,42,32,26,34,5,33,24,4,6,9,7,8,10,2,175])). % 117.88/117.96 cnf(2708,plain, % 117.88/117.96 (~P3(a7,f3(a7,a1),f3(a8,a1))), % 117.88/117.96 inference(scs_inference,[],[2571,2602,2659,2667,58,19,17,29,30,31,25,52,27,28,42,32,26,34,5,33,24,4,6,9,7,8,10,2,175,181])). % 117.88/117.96 cnf(2709,plain, % 117.88/117.96 (~P3(f3(a7,a1),a7,f4(a8,a6))), % 117.88/117.96 inference(scs_inference,[],[2571,2658,2602,2659,2667,58,19,17,29,30,31,25,52,27,28,42,32,26,34,5,33,24,4,6,9,7,8,10,2,175,181,12])). % 117.88/117.96 cnf(2710,plain, % 117.88/117.96 (~P3(a7,f3(a7,a1),f4(a8,a6))), % 117.88/117.96 inference(scs_inference,[],[2571,2658,2602,2659,2667,58,19,17,29,30,31,25,52,27,28,42,32,26,34,5,33,24,4,6,9,7,8,10,2,175,181,12,13])). % 117.88/117.96 cnf(2711,plain, % 117.88/117.96 (P1(f4(a6,a6))), % 117.88/117.96 inference(scs_inference,[],[2571,2658,2602,2659,2667,18,58,19,17,29,30,31,25,52,27,28,42,32,26,34,5,33,24,4,6,9,7,8,10,2,175,181,12,13,41])). % 117.88/117.96 cnf(2714,plain, % 117.88/117.96 (E(f4(x27141,f4(a6,a6)),f4(x27141,a6))), % 117.88/117.96 inference(rename_variables,[],[2598])). % 117.88/117.96 cnf(2719,plain, % 117.88/117.96 (~P2(f4(a1,a6),f3(a7,a1))), % 117.88/117.96 inference(scs_inference,[],[84,2571,2658,2598,2714,2602,2659,2667,18,58,19,17,29,30,31,25,52,27,28,42,32,26,34,5,33,24,4,6,9,7,8,10,2,175,181,12,13,41,14,40,15,16])). % 117.88/117.96 cnf(2722,plain, % 117.88/117.96 (~P3(a7,f3(a7,a1),a8)), % 117.88/117.96 inference(scs_inference,[],[84,2571,2658,2598,2714,2602,2659,2421,2667,1254,18,58,19,17,29,30,31,25,52,27,28,42,32,26,34,5,33,24,4,6,9,7,8,10,2,175,181,12,13,41,14,40,15,16,3,184,2622])). % 117.88/117.96 cnf(2723,plain, % 117.88/117.96 (~P3(f3(a7,a1),a7,f3(a8,a1))), % 117.88/117.96 inference(scs_inference,[],[84,2571,2658,2598,2714,2602,2659,2421,2667,1254,18,58,19,17,29,30,31,25,52,27,28,42,32,26,34,5,33,24,4,6,9,7,8,10,2,175,181,12,13,41,14,40,15,16,3,184,2622,2669])). % 117.88/117.96 cnf(2728,plain, % 117.88/117.96 (~E(f4(a8,f4(a6,a6)),f3(a7,f2(a7)))), % 117.88/117.96 inference(scs_inference,[],[2711,25,42])). % 117.88/117.96 cnf(2744,plain, % 117.88/117.96 (E(f4(a6,a7),a7)), % 117.88/117.96 inference(scs_inference,[],[2711,19,25,42,29,52,26,31,27,32,34,28])). % 117.88/117.96 cnf(2746,plain, % 117.88/117.96 (E(f3(f4(a6,a8),x27461),f3(a8,x27461))), % 117.88/117.96 inference(scs_inference,[],[2711,2575,19,25,42,29,52,26,31,27,32,34,28,5])). % 117.88/117.96 cnf(2753,plain, % 117.88/117.96 (E(f3(x27531,f4(a6,a8)),f3(x27531,a8))), % 117.88/117.96 inference(scs_inference,[],[2711,2575,2661,19,25,42,29,52,26,31,27,32,34,28,5,33,24,9,4,6])). % 117.88/117.96 cnf(2755,plain, % 117.88/117.96 (E(f4(f4(a6,a8),x27551),f4(a8,x27551))), % 117.88/117.96 inference(scs_inference,[],[2711,2575,2661,19,25,42,29,52,26,31,27,32,34,28,5,33,24,9,4,6,8,7])). % 117.88/117.96 cnf(2758,plain, % 117.88/117.96 (~P3(f3(a7,a1),f3(a7,a1),f4(a8,a6))), % 117.88/117.96 inference(scs_inference,[],[2711,2710,2575,2673,2661,1662,19,25,42,29,52,26,31,27,32,34,28,5,33,24,9,4,6,8,7,10,2,12])). % 117.88/117.96 cnf(2759,plain, % 117.88/117.96 (P1(f4(f4(a6,a6),f4(a6,a6)))), % 117.88/117.96 inference(scs_inference,[],[2711,2710,2575,2673,2661,1662,19,25,42,29,52,26,31,27,32,34,28,5,33,24,9,4,6,8,7,10,2,12,41])). % 117.88/117.96 cnf(2761,plain, % 117.88/117.96 (~P3(f3(a7,a1),f3(a7,a1),f3(a8,a1))), % 117.88/117.96 inference(scs_inference,[],[2711,2723,2710,2575,2673,2661,1662,19,25,42,29,52,26,31,27,32,34,28,5,33,24,9,4,6,8,7,10,2,12,41,13])). % 117.88/117.96 cnf(2762,plain, % 117.88/117.96 (~P3(f3(a7,a1),f3(a7,a1),f4(a6,a8))), % 117.88/117.96 inference(scs_inference,[],[2711,2723,2710,2707,2575,2673,2661,1662,19,25,42,29,52,26,31,27,32,34,28,5,33,24,9,4,6,8,7,10,2,12,41,13,14])). % 117.88/117.96 cnf(2777,plain, % 117.88/117.96 (E(f3(a1,f2(a1)),a1)), % 117.88/117.96 inference(scs_inference,[],[2759,17,52,32])). % 117.88/117.96 cnf(2781,plain, % 117.88/117.96 (E(f3(a1,a1),a1)), % 117.88/117.96 inference(scs_inference,[],[2759,17,52,32,25,29])). % 117.88/117.96 cnf(2785,plain, % 117.88/117.96 (~E(f4(a8,a8),f3(a7,f2(a7)))), % 117.88/117.96 inference(scs_inference,[],[2759,20,17,52,32,25,29,26,42])). % 117.88/117.96 cnf(2787,plain, % 117.88/117.96 (E(f4(a6,a1),a1)), % 117.88/117.96 inference(scs_inference,[],[2759,20,17,52,32,25,29,26,42,28])). % 117.88/117.96 cnf(2789,plain, % 117.88/117.96 (E(f3(f2(a7),a7),a1)), % 117.88/117.96 inference(scs_inference,[],[2759,20,19,17,52,32,25,29,26,42,28,31])). % 117.88/117.96 cnf(2793,plain, % 117.88/117.96 (E(f3(a1,a7),a7)), % 117.88/117.96 inference(scs_inference,[],[2759,20,19,17,52,32,25,29,26,42,28,31,34,27])). % 117.88/117.96 cnf(2795,plain, % 117.88/117.96 (E(f3(f4(a7,a6),x27951),f3(a7,x27951))), % 117.88/117.96 inference(scs_inference,[],[2675,2759,20,19,17,52,32,25,29,26,42,28,31,34,27,5])). % 117.88/117.96 cnf(2799,plain, % 117.88/117.96 (E(f4(x27991,f4(a7,a6)),f4(x27991,a7))), % 117.88/117.96 inference(scs_inference,[],[2675,2759,20,19,17,52,32,25,29,26,42,28,31,34,27,5,24,9,8])). % 117.88/117.96 cnf(2802,plain, % 117.88/117.96 (E(f4(f4(a7,a6),x28021),f4(a7,x28021))), % 117.88/117.96 inference(scs_inference,[],[2675,2759,20,19,17,52,32,25,29,26,42,28,31,34,27,5,24,9,8,4,6,7])). % 117.88/117.96 cnf(2805,plain, % 117.88/117.96 (P1(f4(a8,a8))), % 117.88/117.96 inference(scs_inference,[],[2675,2759,2467,20,19,17,52,32,25,29,26,42,28,31,34,27,5,24,9,8,4,6,7,10,2,41])). % 117.88/117.96 cnf(2807,plain, % 117.88/117.96 (~P3(f4(a7,a6),f3(a7,a1),f3(a8,a1))), % 117.88/117.96 inference(scs_inference,[],[2675,2708,2759,2467,20,19,17,52,32,25,29,26,42,28,31,34,27,5,24,9,8,4,6,7,10,2,41,12])). % 117.88/117.96 cnf(2810,plain, % 117.88/117.96 (~P3(f3(a7,a1),f4(a7,a6),f4(a8,a6))), % 117.88/117.96 inference(scs_inference,[],[2758,2675,2708,2709,2755,2759,2467,20,19,17,52,32,25,29,26,42,28,31,34,27,5,24,9,8,4,6,7,10,2,41,12,14,13])). % 117.88/117.96 cnf(2811,plain, % 117.88/117.96 (P1(f3(a8,a8))), % 117.88/117.96 inference(scs_inference,[],[2758,2675,2708,2709,2755,2759,2467,20,19,17,52,32,25,29,26,42,28,31,34,27,5,24,9,8,4,6,7,10,2,41,12,14,13,40])). % 117.88/117.96 cnf(2818,plain, % 117.88/117.96 (E(f4(f4(a8,a8),a6),f4(a8,a8))), % 117.88/117.96 inference(scs_inference,[],[22,2758,2675,2708,2709,2577,2755,2759,2537,2467,1563,2364,20,19,17,52,32,25,29,26,42,28,31,34,27,5,24,9,8,4,6,7,10,2,41,12,14,13,40,15,16,3,53,30])). % 117.88/117.96 cnf(2827,plain, % 117.88/117.96 (~E(f4(f4(a8,a8),f4(a8,a8)),a1)), % 117.88/117.96 inference(scs_inference,[],[22,2758,2675,2708,2709,2577,2755,2759,2537,2467,1563,2442,2364,20,19,17,52,32,25,29,26,42,28,31,34,27,5,24,9,8,4,6,7,10,2,41,12,14,13,40,15,16,3,53,30,33,199,43,45,37])). % 117.88/117.96 cnf(2845,plain, % 117.88/117.96 (~E(f4(a8,f4(a8,a8)),f3(a7,f2(a7)))), % 117.88/117.96 inference(scs_inference,[],[2805,2811,29,31,30,52,26,27,25,42])). % 117.88/117.96 cnf(2856,plain, % 117.88/117.96 (P1(f2(f4(a8,a8)))), % 117.88/117.96 inference(scs_inference,[],[2805,2811,2744,29,31,30,52,26,27,25,42,32,28,34,5,33,24])). % 117.88/117.96 cnf(2858,plain, % 117.88/117.96 (E(f4(f4(a6,a7),x28581),f4(a7,x28581))), % 117.88/117.96 inference(scs_inference,[],[2805,2811,2744,29,31,30,52,26,27,25,42,32,28,34,5,33,24,7])). % 117.88/117.96 cnf(2860,plain, % 117.88/117.96 (E(f4(x28601,f4(a6,a7)),f4(x28601,a7))), % 117.88/117.96 inference(scs_inference,[],[2805,2811,2744,29,31,30,52,26,27,25,42,32,28,34,5,33,24,7,4,8])). % 117.88/117.96 cnf(2865,plain, % 117.88/117.96 (P1(f4(f4(a8,a8),f4(a8,a8)))), % 117.88/117.96 inference(scs_inference,[],[2805,2811,2744,2785,29,31,30,52,26,27,25,42,32,28,34,5,33,24,7,4,8,9,6,10,2,41])). % 117.88/117.96 cnf(2868,plain, % 117.88/117.96 (E(f3(f4(a7,a6),x28681),f3(a7,x28681))), % 117.88/117.96 inference(rename_variables,[],[2795])). % 117.88/117.96 cnf(2869,plain, % 117.88/117.96 (~P3(f3(a7,a1),f3(a7,a1),f4(f4(a6,a6),a8))), % 117.88/117.96 inference(scs_inference,[],[2805,2811,2761,2762,2744,2597,2795,2785,29,31,30,52,26,27,25,42,32,28,34,5,33,24,7,4,8,9,6,10,2,41,12,14])). % 117.88/117.96 cnf(2876,plain, % 117.88/117.96 (~P2(f3(a1,a1),f2(a7))), % 117.88/117.96 inference(scs_inference,[],[2805,2811,2761,2762,2744,1666,2781,2597,2795,2868,92,2785,29,31,30,52,26,27,25,42,32,28,34,5,33,24,7,4,8,9,6,10,2,41,12,14,40,13,16,15])). % 117.88/117.96 cnf(2881,plain, % 117.88/117.96 (P2(f4(a8,a8),f4(f4(a8,a8),f4(a8,a8)))), % 117.88/117.96 inference(scs_inference,[],[2805,2811,2761,2762,2744,1666,2781,2597,2795,2868,92,2785,2827,1542,2442,29,31,30,52,26,27,25,42,32,28,34,5,33,24,7,4,8,9,6,10,2,41,12,14,40,13,16,15,3,37,199,53])). % 117.88/117.96 cnf(2892,plain, % 117.88/117.96 (~E(f4(a8,f3(a8,a8)),f3(a7,f2(a7)))), % 117.88/117.96 inference(scs_inference,[],[2856,2811,27,31,25,42])). % 117.88/117.96 cnf(2906,plain, % 117.88/117.96 (E(f3(f3(a1,a7),x29061),f3(a7,x29061))), % 117.88/117.96 inference(scs_inference,[],[2793,2856,2811,27,31,25,42,52,29,34,28,26,32,5])). % 117.88/117.96 cnf(2909,plain, % 117.88/117.96 (E(f4(f3(a1,a7),x29091),f4(a7,x29091))), % 117.88/117.96 inference(scs_inference,[],[2793,2856,2811,27,31,25,42,52,29,34,28,26,32,5,24,7])). % 117.88/117.96 cnf(2911,plain, % 117.88/117.96 (E(f4(x29111,f3(a1,a7)),f4(x29111,a7))), % 117.88/117.96 inference(scs_inference,[],[2793,2856,2811,27,31,25,42,52,29,34,28,26,32,5,24,7,9,8])). % 117.88/117.96 cnf(2918,plain, % 117.88/117.96 (P1(f4(f3(a8,a8),f3(a8,a8)))), % 117.88/117.96 inference(scs_inference,[],[2793,2881,2856,2865,2845,2811,27,31,25,42,52,29,34,28,26,32,5,24,7,9,8,6,4,10,2,43,41])). % 117.88/117.96 cnf(2920,plain, % 117.88/117.96 (P1(f3(f3(a8,a8),f3(a8,a8)))), % 117.88/117.96 inference(scs_inference,[],[2793,2881,2856,2865,2845,2811,27,31,25,42,52,29,34,28,26,32,5,24,7,9,8,6,4,10,2,43,41,40])). % 117.88/117.96 cnf(2922,plain, % 117.88/117.96 (~P3(f3(a1,a7),f3(a7,a1),a8)), % 117.88/117.96 inference(scs_inference,[],[2793,2722,2881,2856,2865,2845,2811,27,31,25,42,52,29,34,28,26,32,5,24,7,9,8,6,4,10,2,43,41,40,12])). % 117.88/117.96 cnf(2923,plain, % 117.88/117.96 (~P3(f3(a7,a1),f4(a7,a6),f4(a8,f3(a6,a1)))), % 117.88/117.96 inference(scs_inference,[],[2810,2793,2722,2881,2856,2865,2845,2532,2811,27,31,25,42,52,29,34,28,26,32,5,24,7,9,8,6,4,10,2,43,41,40,12,14])). % 117.88/117.96 cnf(2944,plain, % 117.88/117.96 (E(f3(f2(a1),a1),a1)), % 117.88/117.96 inference(scs_inference,[],[17,31])). % 117.88/117.96 cnf(2948,plain, % 117.88/117.96 (~E(f4(a8,a7),f3(a7,f2(a7)))), % 117.88/117.96 inference(scs_inference,[],[2918,19,17,31,25,42])). % 117.88/117.96 cnf(2957,plain, % 117.88/117.96 (E(f4(f4(a6,a1),x29571),f4(a1,x29571))), % 117.88/117.96 inference(scs_inference,[],[2787,2918,19,17,31,25,42,52,26,5,24,7])). % 117.88/117.96 cnf(2958,plain, % 117.88/117.96 (E(f4(x29581,f4(a6,a1)),f4(x29581,a1))), % 117.88/117.96 inference(scs_inference,[],[2787,2918,19,17,31,25,42,52,26,5,24,7,8])). % 117.88/117.96 cnf(2964,plain, % 117.88/117.96 (P1(f4(f4(a1,a6),f4(a1,a6)))), % 117.88/117.96 inference(scs_inference,[],[2787,2918,2892,58,19,17,31,25,42,52,26,5,24,7,8,10,4,9,6,2,41])). % 117.88/117.96 cnf(2966,plain, % 117.88/117.96 (P1(f3(a7,a7))), % 117.88/117.96 inference(scs_inference,[],[2787,2918,2892,58,19,17,31,25,42,52,26,5,24,7,8,10,4,9,6,2,41,40])). % 117.88/117.96 cnf(2970,plain, % 117.88/117.96 (~P3(f4(a7,a6),f3(a7,a1),f3(f3(a8,a1),a1))), % 117.88/117.96 inference(scs_inference,[],[2807,2787,2695,2802,2918,2892,58,19,17,31,25,42,52,26,5,24,7,8,10,4,9,6,2,41,40,12,14])). % 117.88/117.96 cnf(2972,plain, % 117.88/117.96 (~P3(f4(a7,a6),f3(f3(a1,a7),a1),f3(a8,a1))), % 117.88/117.96 inference(scs_inference,[],[2807,2787,2695,2802,2906,2918,2892,58,19,17,31,25,42,52,26,5,24,7,8,10,4,9,6,2,41,40,12,14,13])). % 117.88/117.96 cnf(2975,plain, % 117.88/117.96 (~P2(f4(a6,a1),f3(a6,a6))), % 117.88/117.96 inference(scs_inference,[],[2807,2628,2787,2695,2802,2906,179,2918,2892,58,19,17,31,25,42,52,26,5,24,7,8,10,4,9,6,2,41,40,12,14,13,16,15])). % 117.88/117.96 cnf(2979,plain, % 117.88/117.96 (E(f4(f4(a6,a1),f2(a1)),a1)), % 117.88/117.96 inference(scs_inference,[],[2807,2628,2787,2695,2802,2906,179,2918,2892,839,58,19,17,31,25,42,52,26,5,24,7,8,10,4,9,6,2,41,40,12,14,13,16,15,3,621,620])). % 117.88/117.96 cnf(2981,plain, % 117.88/117.96 (E(f4(f2(a1),f4(a6,a1)),a1)), % 117.88/117.96 inference(scs_inference,[],[2807,2628,2787,2695,2802,2906,179,2918,2892,839,58,19,17,31,25,42,52,26,5,24,7,8,10,4,9,6,2,41,40,12,14,13,16,15,3,621,620,653,1539])). % 117.88/117.96 cnf(3018,plain, % 117.88/117.96 (~E(f3(a7,f2(a7)),f4(a8,a7))), % 117.88/117.96 inference(scs_inference,[],[2966,2920,2587,2948,25,42,31,52,26,5,24,7,4,10,9,8,6,2])). % 117.88/117.96 cnf(3019,plain, % 117.88/117.96 (~P3(a7,f3(a7,a1),f3(a1,a8))), % 117.88/117.96 inference(scs_inference,[],[2966,2920,2587,2948,2577,2673,25,42,31,52,26,5,24,7,4,10,9,8,6,2,181])). % 117.88/117.96 cnf(3020,plain, % 117.88/117.96 (P1(f4(f3(a7,a7),f3(a7,a7)))), % 117.88/117.96 inference(scs_inference,[],[2966,2920,2587,2948,2577,2673,25,42,31,52,26,5,24,7,4,10,9,8,6,2,181,41])). % 117.88/117.96 cnf(3022,plain, % 117.88/117.96 (P1(f3(f3(a7,a7),f3(a7,a7)))), % 117.88/117.96 inference(scs_inference,[],[2966,2920,2587,2948,2577,2673,25,42,31,52,26,5,24,7,4,10,9,8,6,2,181,41,40])). % 117.88/117.96 cnf(3026,plain, % 117.88/117.96 (E(f4(f4(a6,a7),x30261),f4(a7,x30261))), % 117.88/117.96 inference(rename_variables,[],[2858])). % 117.88/117.96 cnf(3031,plain, % 117.88/117.96 (~E(f4(a8,a8),f4(f2(a7),f4(a6,a1)))), % 117.88/117.96 inference(scs_inference,[],[2966,335,2922,2506,2972,2858,3026,2958,2522,2920,2587,2923,2657,2948,2577,2673,25,42,31,52,26,5,24,7,4,10,9,8,6,2,181,41,40,14,12,13,16,15,3])). % 117.88/117.96 cnf(3043,plain, % 117.88/117.96 (~E(f4(a8,a1),f3(a7,f2(a7)))), % 117.88/117.96 inference(scs_inference,[],[17,42])). % 117.88/117.96 cnf(3059,plain, % 117.88/117.96 (E(f3(x30591,f3(a1,f2(a1))),f3(x30591,a1))), % 117.88/117.96 inference(scs_inference,[],[2964,3020,2777,17,42,25,52,5,26,24,7,10,9,4,8,6])). % 117.88/117.96 cnf(3061,plain, % 117.88/117.96 (P1(f4(a7,a7))), % 117.88/117.96 inference(scs_inference,[],[2964,3020,2777,3031,19,17,42,25,52,5,26,24,7,10,9,4,8,6,2,41])). % 117.88/117.96 cnf(3063,plain, % 117.88/117.96 (P1(f3(a1,a1))), % 117.88/117.96 inference(scs_inference,[],[2964,3020,2777,3031,19,17,42,25,52,5,26,24,7,10,9,4,8,6,2,41,40])). % 117.88/117.96 cnf(3101,plain, % 117.88/117.96 (E(f3(f3(a1,a1),a1),f3(a1,a1))), % 117.88/117.96 inference(scs_inference,[],[3063,29])). % 117.88/117.96 cnf(3111,plain, % 117.88/117.96 (E(f3(a1,f3(a1,a1)),f3(a1,a1))), % 117.88/117.96 inference(scs_inference,[],[3061,3063,29,28,42,30,34,27])). % 117.88/117.96 cnf(3134,plain, % 117.88/117.96 (~E(f3(a7,f2(a7)),f4(a8,a1))), % 117.88/117.96 inference(scs_inference,[],[3061,3063,3022,2979,3043,29,28,42,30,34,27,32,25,31,52,26,33,24,5,7,10,9,4,8,6,2])). % 117.88/117.96 cnf(3135,plain, % 117.88/117.96 (P1(f4(f4(a7,a7),f4(a7,a7)))), % 117.88/117.96 inference(scs_inference,[],[3061,3063,3022,2979,3043,29,28,42,30,34,27,32,25,31,52,26,33,24,5,7,10,9,4,8,6,2,41])). % 117.88/117.96 cnf(3142,plain, % 117.88/117.96 (E(f4(f3(a1,a7),x31421),f4(a7,x31421))), % 117.88/117.96 inference(rename_variables,[],[2909])). % 117.88/117.96 cnf(3148,plain, % 117.88/117.96 (~E(a1,f4(a8,a7))), % 117.88/117.96 inference(scs_inference,[],[3061,3063,2975,3019,2638,2534,2753,2909,3142,3018,3022,2979,2970,3043,2689,2810,29,28,42,30,34,27,32,25,31,52,26,33,24,5,7,10,9,4,8,6,2,41,40,14,12,13,16,15,3])). % 117.88/117.96 cnf(3149,plain, % 117.88/117.96 (~P3(a7,f4(a6,a7),a8)), % 117.88/117.96 inference(scs_inference,[],[3061,3063,2975,3019,2638,2534,2753,2909,3142,3018,3022,2979,2970,3043,2689,2810,2744,29,28,42,30,34,27,32,25,31,52,26,33,24,5,7,10,9,4,8,6,2,41,40,14,12,13,16,15,3,2622])). % 117.88/117.96 cnf(3152,plain, % 117.88/117.96 (~P3(f4(a6,a7),a7,f3(a8,a1))), % 117.88/117.96 inference(scs_inference,[],[3061,3063,2975,3019,2638,2534,2753,2909,3142,3018,3022,2979,2970,3043,2689,2810,2744,29,28,42,30,34,27,32,25,31,52,26,33,24,5,7,10,9,4,8,6,2,41,40,14,12,13,16,15,3,2622,621,2669])). % 117.88/117.96 cnf(3177,plain, % 117.88/117.96 (~E(f4(a8,a7),a1)), % 117.88/117.96 inference(scs_inference,[],[3148,3135,2981,3063,42,25,52,26,24,5,7,4,10,9,8,6,2])). % 117.88/117.96 cnf(3178,plain, % 117.88/117.96 (P1(f4(f3(a1,a1),f3(a1,a1)))), % 117.88/117.96 inference(scs_inference,[],[3148,3135,2981,3063,42,25,52,26,24,5,7,4,10,9,8,6,2,41])). % 117.88/117.96 cnf(3180,plain, % 117.88/117.96 (P1(f3(f3(a1,a1),f3(a1,a1)))), % 117.88/117.96 inference(scs_inference,[],[3148,3135,2981,3063,42,25,52,26,24,5,7,4,10,9,8,6,2,41,40])). % 117.88/117.96 cnf(3186,plain, % 117.88/117.96 (~P3(f4(a6,a7),f3(a7,a1),f3(a8,a1))), % 117.88/117.96 inference(scs_inference,[],[3152,3148,2704,2799,3135,2981,2869,2673,3063,42,25,52,26,24,5,7,4,10,9,8,6,2,41,40,14,12,13])). % 117.88/117.96 cnf(3187,plain, % 117.88/117.96 (~P2(f3(a1,a1),f4(f2(a7),f4(a6,a6)))), % 117.88/117.96 inference(scs_inference,[],[2876,3152,3148,2619,2704,2799,3135,2981,2869,2673,3063,42,25,52,26,24,5,7,4,10,9,8,6,2,41,40,14,12,13,16])). % 117.88/117.96 cnf(3188,plain, % 117.88/117.96 (~P2(f3(a1,f3(a1,a1)),f2(a7))), % 117.88/117.96 inference(scs_inference,[],[2876,3152,3148,2619,3111,2704,2799,3135,2981,2869,2673,3063,42,25,52,26,24,5,7,4,10,9,8,6,2,41,40,14,12,13,16,15])). % 117.88/117.96 cnf(3195,plain, % 117.88/117.96 (~P3(f4(a7,a6),f4(a7,a6),a8)), % 117.88/117.96 inference(scs_inference,[],[2876,3152,3148,2619,3111,2704,2799,3135,2981,2869,1639,2673,3063,2675,42,25,52,26,24,5,7,4,10,9,8,6,2,41,40,14,12,13,16,15,3,621,653,620,1539,175])). % 117.88/117.96 cnf(3217,plain, % 117.88/117.96 (P1(f4(a1,a1))), % 117.88/117.96 inference(scs_inference,[],[3178,2573,2518,17,25,52,26,24,5,7,4,9,10,6,8,2,41])). % 117.88/117.96 cnf(3221,plain, % 117.88/117.96 (~P3(f4(a6,a7),f3(a7,a1),f3(f4(a6,a8),a1))), % 117.88/117.96 inference(scs_inference,[],[3186,2746,3178,2573,2518,17,25,52,26,24,5,7,4,9,10,6,8,2,41,40,14])). % 117.88/117.96 cnf(3224,plain, % 117.88/117.96 (E(f4(x32241,f4(a6,a7)),f4(x32241,a7))), % 117.88/117.96 inference(rename_variables,[],[2860])). % 117.88/117.96 cnf(3230,plain, % 117.88/117.96 (~E(f4(a8,a7),f3(f2(a8),a8))), % 117.88/117.96 inference(scs_inference,[],[3186,2719,3177,3149,2683,2860,3224,2746,3178,2573,2518,3059,17,25,52,26,24,5,7,4,9,10,6,8,2,41,40,14,13,12,16,15,3])). % 117.88/117.96 cnf(3257,plain, % 117.88/117.96 (E(f4(a1,f4(a1,a1)),a1)), % 117.88/117.96 inference(scs_inference,[],[3217,25])). % 117.88/117.96 cnf(3273,plain, % 117.88/117.96 (P1(f4(f4(a1,a1),f4(a1,a1)))), % 117.88/117.96 inference(scs_inference,[],[3217,3180,2789,3230,25,26,52,24,5,7,10,9,4,6,8,2,41])). % 117.88/117.96 cnf(3276,plain, % 117.88/117.96 (E(f4(x32761,f3(a1,a6)),f4(x32761,a6))), % 117.88/117.96 inference(rename_variables,[],[2654])). % 117.88/117.96 cnf(3291,plain, % 117.88/117.96 (~P3(a7,f4(a6,a7),f4(a8,a6))), % 117.88/117.96 inference(scs_inference,[],[3217,3195,2668,3101,2655,3188,3180,3187,2789,3230,1643,2654,3276,2762,2581,2575,2744,25,26,52,24,5,7,10,9,4,6,8,2,41,13,14,12,16,15,3,621,653,620,1539,171,181])). % 117.88/117.96 cnf(3294,plain, % 117.88/117.96 (P1(f5(f4(a8,a8),f4(a8,a8)))), % 117.88/117.96 inference(scs_inference,[],[3217,3195,2668,3101,2818,2655,3188,3180,3187,2789,3230,1643,2654,3276,2762,2581,2442,2575,2744,2805,18,25,26,52,24,5,7,10,9,4,6,8,2,41,13,14,12,16,15,3,621,653,620,1539,171,181,44,43])). % 117.88/117.96 cnf(3317,plain, % 117.88/117.96 (E(f4(x33171,f3(a1,a7)),f4(x33171,a7))), % 117.88/117.96 inference(rename_variables,[],[2911])). % 117.88/117.96 cnf(3326,plain, % 117.88/117.96 (~E(a1,f4(a8,a1))), % 117.88/117.96 inference(scs_inference,[],[3291,2542,2589,2911,3317,2957,3134,3273,2944,3221,2728,2703,2689,25,52,26,24,5,7,9,4,10,6,8,2,13,14,12,16,15,3])). % 117.88/117.96 cnf(3361,plain, % 117.88/117.96 (~E(f4(a8,a1),a1)), % 117.88/117.96 inference(scs_inference,[],[3326,3294,3257,25,26,52,24,5,7,4,9,6,8,10,2])). % 117.88/117.96 cnf(4652,plain, % 117.88/117.96 ($false), % 117.88/117.96 inference(scs_inference,[],[20,2673,2442,3361,2,1539,620,26]), % 117.88/117.96 ['proof']). % 117.88/117.96 % SZS output end Proof % 117.88/117.96 % Total time :117.260000s %------------------------------------------------------------------------------