%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL512+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/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 : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 11:19:17 AM UTC 2026
% Result : Theorem 141.11s 141.16s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL512+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.03 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.08/0.36 % Computer : n029.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 5 17:15:55 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.25/0.52 start to proof:theBenchmark
% 141.11/141.15 %-------------------------------------------
% 141.11/141.15 % File :CSE---1.7
% 141.11/141.15 % Problem :theBenchmark
% 141.11/141.15 % Transform :cnf
% 141.11/141.15 % Format :tptp:raw
% 141.11/141.15 % Command :java -jar mcs_scs.jar %d %s
% 141.11/141.15
% 141.11/141.15 % Result :Theorem 140.616046s
% 141.11/141.15 % Output :CNFRefutation 140.616046s
% 141.11/141.15 %-------------------------------------------
% 141.11/141.15 %------------------------------------------------------------------------------
% 141.11/141.15 % File : LCL512+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 141.11/141.15 % Domain : Logic Calculi (Propositional)
% 141.11/141.15 % Problem : Prove Hilbert's equivalence_1 axiom from Rosser's system
% 141.11/141.15 % Version : [Zen73] axioms.
% 141.11/141.15 % English :
% 141.11/141.15
% 141.11/141.15 % Refs : [Zem73] Zeman (1973), Modal Logic, the Lewis-Modal systems
% 141.11/141.15 % : [Hal] Halleck (URL), John Halleck's Logic Systems
% 141.11/141.15 % Source : [TPTP]
% 141.11/141.15 % Names :
% 141.11/141.15
% 141.11/141.15 % Status : Theorem
% 141.11/141.15 % Rating : 0.22 v9.3.0
% 141.11/141.15 % Syntax : Number of formulae : 43 ( 12 unt; 0 def)
% 141.11/141.15 % Number of atoms : 77 ( 6 equ)
% 141.11/141.15 % Maximal formula atoms : 4 ( 1 avg)
% 141.11/141.15 % Number of connectives : 34 ( 0 ~; 0 |; 1 &)
% 141.11/141.15 % ( 26 <=>; 7 =>; 0 <=; 0 <~>)
% 141.11/141.15 % Maximal formula depth : 6 ( 3 avg)
% 141.11/141.15 % Maximal term depth : 5 ( 2 avg)
% 141.11/141.15 % Number of predicates : 33 ( 32 usr; 31 prp; 0-2 aty)
% 141.11/141.15 % Number of functors : 5 ( 5 usr; 0 con; 1-2 aty)
% 141.11/141.15 % Number of variables : 65 ( 65 !; 0 ?)
% 141.11/141.15 % SPC : FOF_THM_RFO_SEQ
% 141.11/141.15
% 141.11/141.15 % Comments :
% 141.11/141.15 % Bugfixes : v9.2.0 - Bugfix in LCL006+5.ax
% 141.11/141.15 %------------------------------------------------------------------------------
% 141.11/141.15 %----Include axioms of propositional logic
% 141.11/141.15 include('Axioms/LCL006+0.ax').
% 141.11/141.15 include('Axioms/LCL006+1.ax').
% 141.11/141.15 %----Include Rosser's axiomatization of propositional logic
% 141.11/141.15 include('Axioms/LCL006+5.ax').
% 141.11/141.15 %------------------------------------------------------------------------------
% 141.11/141.15 %----Operator definitions to reduce everything to and & not
% 141.11/141.15 fof(hilbert_op_or,axiom,
% 141.11/141.15 op_or ).
% 141.11/141.15
% 141.11/141.15 fof(hilbert_op_implies_and,axiom,
% 141.11/141.15 op_implies_and ).
% 141.11/141.15
% 141.11/141.15 fof(hilbert_op_equiv,axiom,
% 141.11/141.15 op_equiv ).
% 141.11/141.15
% 141.11/141.16 fof(hilbert_equivalence_1,conjecture,
% 141.11/141.16 equivalence_1 ).
% 141.11/141.16
% 141.11/141.16 %------------------------------------------------------------------------------
% 141.11/141.16 %-------------------------------------------
% 141.11/141.16 % Proof found
% 141.11/141.16 % SZS status Theorem for theBenchmark
% 141.11/141.16 % SZS output start Proof
% 141.11/141.16 %ClaNum:116(EqnAxiom:44)
% 141.11/141.16 %VarNum:127(SingletonVarNum:63)
% 141.11/141.16 %MaxLitNum:4
% 141.11/141.16 %MaxfuncDepth:4
% 141.11/141.16 %SharedTerms:228
% 141.11/141.16 %goalClause: 56
% 141.11/141.16 %singleGoalClaCount:1
% 141.11/141.16 [45]P1(a5000)
% 141.11/141.16 [46]P18(a5000)
% 141.11/141.16 [47]P2(a5000)
% 141.11/141.16 [48]P16(a5000)
% 141.11/141.16 [49]P17(a5000)
% 141.11/141.16 [51]P19(a5000)
% 141.11/141.16 [53]P20(a5000)
% 141.11/141.16 [55]P21(a5000)
% 141.11/141.16 [56]~P3(a5000)
% 141.11/141.16 [78]P11(a5000)+~P10(f47(a48,f47(a57,a48)))
% 141.11/141.16 [79]P26(a5000)+~P10(f47(a17,f60(a17,a18)))
% 141.11/141.16 [80]P25(a5000)+~P10(f47(a19,f60(a20,a19)))
% 141.11/141.16 [82]P27(a5000)+~P10(f47(a37,f60(a38,a37)))
% 141.11/141.16 [83]P5(a5000)+~P10(f47(f5(a6,a11),a6))
% 141.11/141.16 [84]P4(a5000)+~P10(f47(f5(a12,a13),a13))
% 141.11/141.16 [86]P28(a5000)+~P10(f47(f60(a39,a39),a39))
% 141.11/141.16 [94]P3(a5000)+~P10(f47(f4(a21,a25),f47(a21,a25)))
% 141.11/141.16 [95]P12(a5000)+~P10(f47(f4(a26,a28),f47(a28,a26)))
% 141.11/141.16 [96]P30(a5000)+~P10(f47(f60(a45,a46),f60(a46,a45)))
% 141.11/141.16 [99]P23(a5000)+~P10(f47(f47(f59(a49),f59(a50)),f47(a50,a49)))
% 141.11/141.16 [102]P14(a5000)+~P10(f47(f47(a58,f47(a58,a7)),f47(a58,a7)))
% 141.11/141.16 [89]P6(a5000)+~P10(f47(a40,f47(f59(a40),a43)))
% 141.11/141.16 [90]P9(a5000)+~P10(f47(f47(f59(a44),a44),a44))
% 141.11/141.16 [101]P7(a5000)+~P10(f47(a14,f47(a15,f5(a14,a15))))
% 141.11/141.16 [108]P15(a5000)+~P10(f47(f47(a8,a9),f47(f47(a9,a10),f47(a8,a10))))
% 141.11/141.16 [109]P13(a5000)+~P10(f47(f47(a29,a30),f47(f47(a30,a29),f4(a29,a30))))
% 141.11/141.16 [110]P8(a5000)+~P10(f47(f47(a33,a41),f47(f47(a41,a42),f47(a33,a42))))
% 141.11/141.16 [111]P31(a5000)+~P10(f47(f47(a51,a56),f47(f60(a52,a51),f60(a52,a56))))
% 141.11/141.16 [112]P32(a5000)+~P10(f47(f60(a53,f60(a54,a55)),f60(a54,f60(a53,a55))))
% 141.11/141.16 [115]P29(a5000)+~P10(f47(f47(a22,a23),f47(f47(a24,a23),f47(f60(a22,a24),a23))))
% 141.11/141.16 [70]~P2(a5000)+P10(f47(x701,f5(x701,x701)))
% 141.11/141.16 [77]~P28(a5000)+P10(f47(f60(x771,x771),x771))
% 141.11/141.16 [88]~P9(a5000)+P10(f47(f47(f59(x881),x881),x881))
% 141.11/141.16 [62]E(f60(f59(x621),x622),f47(x621,x622))+~P24(a5000)
% 141.11/141.16 [68]E(f5(f47(x681,x682),f47(x682,x681)),f4(x681,x682))+~P21(a5000)
% 141.11/141.16 [69]~P11(a5000)+P10(f47(x691,f47(x692,x691)))
% 141.11/141.16 [71]~P25(a5000)+P10(f47(x711,f60(x712,x711)))
% 141.11/141.16 [72]~P27(a5000)+P10(f47(x721,f60(x722,x721)))
% 141.11/141.16 [73]~P26(a5000)+P10(f47(x731,f60(x731,x732)))
% 141.11/141.16 [74]~P4(a5000)+P10(f47(f5(x741,x742),x742))
% 141.11/141.16 [75]~P5(a5000)+P10(f47(f5(x751,x752),x751))
% 141.11/141.16 [76]~P16(a5000)+P10(f47(f5(x761,x762),x761))
% 141.11/141.16 [91]~P12(a5000)+P10(f47(f4(x911,x912),f47(x912,x911)))
% 141.11/141.16 [93]~P30(a5000)+P10(f47(f60(x931,x932),f60(x932,x931)))
% 141.11/141.16 [97]~P23(a5000)+P10(f47(f47(f59(x971),f59(x972)),f47(x972,x971)))
% 141.11/141.16 [100]~P14(a5000)+P10(f47(f47(x1001,f47(x1001,x1002)),f47(x1001,x1002)))
% 141.11/141.16 [64]~P20(a5000)+E(f59(f5(x641,f59(x642))),f47(x641,x642))
% 141.11/141.16 [66]~P22(a5000)+E(f59(f60(f59(x661),f59(x662))),f5(x661,x662))
% 141.11/141.16 [67]~P19(a5000)+E(f59(f5(f59(x671),f59(x672))),f60(x671,x672))
% 141.11/141.16 [87]~P6(a5000)+P10(f47(x871,f47(f59(x871),x872)))
% 141.11/141.16 [98]~P7(a5000)+P10(f47(x981,f47(x982,f5(x981,x982))))
% 141.11/141.16 [105]~P13(a5000)+P10(f47(f47(x1051,x1052),f47(f47(x1052,x1051),f4(x1051,x1052))))
% 141.11/141.16 [103]~P15(a5000)+P10(f47(f47(x1031,x1032),f47(f47(x1032,x1033),f47(x1031,x1033))))
% 141.11/141.16 [104]~P8(a5000)+P10(f47(f47(x1041,x1042),f47(f47(x1042,x1043),f47(x1041,x1043))))
% 141.11/141.16 [106]~P31(a5000)+P10(f47(f47(x1061,x1062),f47(f60(x1063,x1061),f60(x1063,x1062))))
% 141.11/141.16 [107]~P32(a5000)+P10(f47(f60(x1071,f60(x1072,x1073)),f60(x1072,f60(x1071,x1073))))
% 141.11/141.16 [113]~P29(a5000)+P10(f47(f47(x1131,x1132),f47(f47(x1133,x1132),f47(f60(x1131,x1133),x1132))))
% 141.11/141.16 [114]~P17(a5000)+P10(f47(f47(x1141,x1142),f47(f59(f5(x1142,x1143)),f59(f5(x1143,x1141)))))
% 141.11/141.16 [63]E(x631,x632)+~P18(a5000)+~P10(f4(x631,x632))
% 141.11/141.16 [65]P10(x651)+~P10(x652)+~P1(a5000)+~P10(f47(x652,x651))
% 141.11/141.16 %EqnAxiom
% 141.11/141.16 [1]E(x11,x11)
% 141.11/141.16 [2]E(x22,x21)+~E(x21,x22)
% 141.11/141.16 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 141.11/141.16 [4]~E(x41,x42)+E(f47(x41,x43),f47(x42,x43))
% 141.11/141.16 [5]~E(x51,x52)+E(f47(x53,x51),f47(x53,x52))
% 141.11/141.16 [6]~E(x61,x62)+E(f4(x61,x63),f4(x62,x63))
% 141.11/141.16 [7]~E(x71,x72)+E(f4(x73,x71),f4(x73,x72))
% 141.11/141.16 [8]~E(x81,x82)+E(f59(x81),f59(x82))
% 141.11/141.16 [9]~E(x91,x92)+E(f60(x91,x93),f60(x92,x93))
% 141.11/141.16 [10]~E(x101,x102)+E(f60(x103,x101),f60(x103,x102))
% 141.11/141.16 [11]~E(x111,x112)+E(f5(x111,x113),f5(x112,x113))
% 141.11/141.16 [12]~E(x121,x122)+E(f5(x123,x121),f5(x123,x122))
% 141.11/141.16 [13]~P1(x131)+P1(x132)+~E(x131,x132)
% 141.11/141.16 [14]~P18(x141)+P18(x142)+~E(x141,x142)
% 141.11/141.16 [15]~P2(x151)+P2(x152)+~E(x151,x152)
% 141.11/141.16 [16]~P16(x161)+P16(x162)+~E(x161,x162)
% 141.11/141.16 [17]~P17(x171)+P17(x172)+~E(x171,x172)
% 141.11/141.16 [18]~P19(x181)+P19(x182)+~E(x181,x182)
% 141.11/141.16 [19]~P8(x191)+P8(x192)+~E(x191,x192)
% 141.11/141.16 [20]~P20(x201)+P20(x202)+~E(x201,x202)
% 141.11/141.16 [21]~P10(x211)+P10(x212)+~E(x211,x212)
% 141.11/141.16 [22]~P21(x221)+P21(x222)+~E(x221,x222)
% 141.11/141.16 [23]~P25(x231)+P25(x232)+~E(x231,x232)
% 141.11/141.16 [24]~P3(x241)+P3(x242)+~E(x241,x242)
% 141.11/141.16 [25]~P31(x251)+P31(x252)+~E(x251,x252)
% 141.11/141.16 [26]~P32(x261)+P32(x262)+~E(x261,x262)
% 141.11/141.16 [27]~P28(x271)+P28(x272)+~E(x271,x272)
% 141.11/141.16 [28]~P13(x281)+P13(x282)+~E(x281,x282)
% 141.11/141.16 [29]~P4(x291)+P4(x292)+~E(x291,x292)
% 141.11/141.16 [30]~P15(x301)+P15(x302)+~E(x301,x302)
% 141.11/141.16 [31]~P14(x311)+P14(x312)+~E(x311,x312)
% 141.11/141.16 [32]~P7(x321)+P7(x322)+~E(x321,x322)
% 141.11/141.16 [33]~P5(x331)+P5(x332)+~E(x331,x332)
% 141.11/141.16 [34]~P24(x341)+P24(x342)+~E(x341,x342)
% 141.11/141.16 [35]~P29(x351)+P29(x352)+~E(x351,x352)
% 141.11/141.16 [36]~P23(x361)+P23(x362)+~E(x361,x362)
% 141.11/141.16 [37]~P6(x371)+P6(x372)+~E(x371,x372)
% 141.11/141.16 [38]~P9(x381)+P9(x382)+~E(x381,x382)
% 141.11/141.16 [39]~P26(x391)+P26(x392)+~E(x391,x392)
% 141.11/141.16 [40]~P27(x401)+P27(x402)+~E(x401,x402)
% 141.11/141.16 [41]~P30(x411)+P30(x412)+~E(x411,x412)
% 141.11/141.16 [42]~P22(x421)+P22(x422)+~E(x421,x422)
% 141.11/141.16 [43]~P12(x431)+P12(x432)+~E(x431,x432)
% 141.11/141.16 [44]~P11(x441)+P11(x442)+~E(x441,x442)
% 141.11/141.16
% 141.11/141.16 %-------------------------------------------
% 141.11/141.16 cnf(117,plain,
% 141.11/141.16 (E(x1171,x1172)+~P10(f4(x1171,x1172))),
% 141.11/141.16 inference(scs_inference,[],[46,63])).
% 141.11/141.16 cnf(119,plain,
% 141.11/141.16 (E(x1191,x1192)+~P10(x1193)+~P10(f47(x1193,f4(x1191,x1192)))),
% 141.11/141.16 inference(scs_inference,[],[45,46,63,65])).
% 141.11/141.16 cnf(120,plain,
% 141.11/141.16 (E(f59(f5(x1201,f59(x1202))),f47(x1201,x1202))),
% 141.11/141.16 inference(scs_inference,[],[53,64])).
% 141.11/141.16 cnf(121,plain,
% 141.11/141.16 (P10(x1211)+~P10(x1212)+~P10(f47(x1212,x1211))),
% 141.11/141.16 inference(scs_inference,[],[45,65])).
% 141.11/141.16 cnf(122,plain,
% 141.11/141.16 (E(f59(f5(f59(x1221),f59(x1222))),f60(x1221,x1222))),
% 141.11/141.16 inference(scs_inference,[],[51,67])).
% 141.11/141.16 cnf(123,plain,
% 141.11/141.16 (E(f5(f47(x1231,x1232),f47(x1232,x1231)),f4(x1231,x1232))),
% 141.11/141.16 inference(scs_inference,[],[55,68])).
% 141.11/141.16 cnf(124,plain,
% 141.11/141.16 (P10(f47(x1241,f5(x1241,x1241)))),
% 141.11/141.16 inference(scs_inference,[],[47,70])).
% 141.11/141.16 cnf(125,plain,
% 141.11/141.16 (P10(f47(f5(x1251,x1252),x1251))),
% 141.11/141.16 inference(scs_inference,[],[48,76])).
% 141.11/141.16 cnf(126,plain,
% 141.11/141.16 (~P10(f47(f4(a21,a25),f47(a21,a25)))),
% 141.11/141.16 inference(scs_inference,[],[56,94])).
% 141.11/141.16 cnf(127,plain,
% 141.11/141.16 (P10(f47(f47(x1271,x1272),f47(f59(f5(x1272,x1273)),f59(f5(x1273,x1271)))))),
% 141.11/141.16 inference(scs_inference,[],[49,114])).
% 141.11/141.16 cnf(128,plain,
% 141.11/141.16 (P5(a5000)),
% 141.11/141.16 inference(scs_inference,[],[125,83])).
% 141.11/141.16 cnf(129,plain,
% 141.11/141.16 (E(f4(x1291,x1292),f5(f47(x1291,x1292),f47(x1292,x1291)))),
% 141.11/141.16 inference(scs_inference,[],[123,2])).
% 141.11/141.16 cnf(130,plain,
% 141.11/141.16 (P10(f5(f47(f5(x1301,x1302),x1301),f47(f5(x1301,x1302),x1301)))),
% 141.11/141.16 inference(scs_inference,[],[123,124,125,2,121])).
% 141.11/141.16 cnf(133,plain,
% 141.11/141.16 (~P10(f59(f5(f4(a21,a25),f59(f47(a21,a25)))))),
% 141.11/141.16 inference(scs_inference,[],[126,123,120,124,125,2,121,21])).
% 141.11/141.16 cnf(136,plain,
% 141.11/141.16 (E(x1361,x1362)+~P10(f5(f4(x1361,x1362),x1363))),
% 141.11/141.16 inference(scs_inference,[],[126,123,120,124,125,2,121,21,24,119])).
% 141.11/141.16 cnf(141,plain,
% 141.11/141.16 (P10(f47(f5(x1411,x1412),x1411))),
% 141.11/141.16 inference(scs_inference,[],[128,75])).
% 141.11/141.16 cnf(143,plain,
% 141.11/141.16 (E(f60(x1431,x1432),f59(f5(f59(x1431),f59(x1432))))),
% 141.11/141.16 inference(scs_inference,[],[122,2])).
% 141.11/141.16 cnf(144,plain,
% 141.11/141.16 (~P10(f5(f47(f4(a21,a25),f47(a21,a25)),x1441))),
% 141.11/141.16 inference(scs_inference,[],[126,122,141,2,121])).
% 141.11/141.16 cnf(147,plain,
% 141.11/141.16 (E(f60(x1471,x1472),f47(f59(x1471),x1472))),
% 141.11/141.16 inference(scs_inference,[],[126,122,120,141,2,121,3])).
% 141.11/141.16 cnf(149,plain,
% 141.11/141.16 (~P10(f4(f4(a21,a25),f47(a21,a25)))),
% 141.11/141.16 inference(scs_inference,[],[126,122,129,120,141,2,121,3,21])).
% 141.11/141.17 cnf(158,plain,
% 141.11/141.17 (E(f47(f59(x1581),x1582),f60(x1581,x1582))),
% 141.11/141.17 inference(scs_inference,[],[147,2])).
% 141.11/141.17 cnf(159,plain,
% 141.11/141.17 (P10(f47(f59(f5(f5(x1591,x1591),x1592)),f59(f5(x1592,x1591))))),
% 141.11/141.17 inference(scs_inference,[],[147,127,124,2,121])).
% 141.11/141.17 cnf(172,plain,
% 141.11/141.17 (E(f59(f47(x1721,x1722)),f59(f59(f5(x1721,f59(x1722)))))),
% 141.11/141.17 inference(scs_inference,[],[120,8,2])).
% 141.11/141.17 cnf(173,plain,
% 141.11/141.17 (E(f47(x1731,x1732),f59(f5(x1731,f59(x1732))))),
% 141.11/141.17 inference(scs_inference,[],[120,2])).
% 141.11/141.17 cnf(174,plain,
% 141.11/141.17 (~P10(f59(f5(f5(f59(f47(a21,a25)),f59(f47(a21,a25))),f4(a21,a25))))),
% 141.11/141.17 inference(scs_inference,[],[159,120,133,2,121])).
% 141.11/141.17 cnf(186,plain,
% 141.11/141.17 (E(f59(f59(f5(x1861,f59(x1862)))),f59(f47(x1861,x1862)))),
% 141.11/141.17 inference(scs_inference,[],[172,2])).
% 141.11/141.17 cnf(601,plain,
% 141.11/141.17 (~P10(f59(f5(f59(x6011),f59(x6012))))+P10(f60(x6011,x6012))),
% 141.11/141.17 inference(scs_inference,[],[186,122,172,25,44,27,42,21])).
% 141.11/141.17 cnf(746,plain,
% 141.11/141.17 (P10(f47(f59(f5(x7461,x7462)),f59(f5(x7462,f5(x7461,x7463)))))),
% 141.11/141.17 inference(scs_inference,[],[125,127,121])).
% 141.11/141.17 cnf(751,plain,
% 141.11/141.17 (P10(f59(f5(x7511,f5(x7512,x7513))))+~P10(f59(f5(x7512,x7511)))),
% 141.11/141.17 inference(scs_inference,[],[746,158,21,121])).
% 141.11/141.17 cnf(753,plain,
% 141.11/141.17 (~P10(f5(f5(f47(f4(a21,a25),f47(a21,a25)),x7531),x7532))),
% 141.11/141.17 inference(scs_inference,[],[144,125,121])).
% 141.11/141.17 cnf(758,plain,
% 141.11/141.17 (~P10(f5(f4(f4(a21,a25),f47(a21,a25)),x7581))),
% 141.11/141.17 inference(scs_inference,[],[149,141,121])).
% 141.11/141.17 cnf(772,plain,
% 141.11/141.17 (~P10(f5(f5(f4(f4(a21,a25),f47(a21,a25)),x7721),x7722))),
% 141.11/141.17 inference(scs_inference,[],[758,125,121])).
% 141.11/141.17 cnf(792,plain,
% 141.11/141.17 (E(f47(f60(x7921,x7922),x7923),f47(f47(f59(x7921),x7922),x7923))),
% 141.11/141.17 inference(scs_inference,[],[158,4,2])).
% 141.11/141.17 cnf(793,plain,
% 141.11/141.17 (E(f47(f47(f59(x7931),x7932),x7933),f47(f60(x7931,x7932),x7933))),
% 141.11/141.17 inference(scs_inference,[],[792,2])).
% 141.11/141.17 cnf(794,plain,
% 141.11/141.17 (E(f59(f5(f60(x7941,x7942),f59(x7943))),f47(f47(f59(x7941),x7942),x7943))),
% 141.11/141.17 inference(scs_inference,[],[120,792,2,3])).
% 141.11/141.17 cnf(795,plain,
% 141.11/141.17 (E(f47(f60(x7951,x7952),x7953),f47(f47(f59(x7951),x7952),x7953))),
% 141.11/141.17 inference(rename_variables,[],[792])).
% 141.11/141.17 cnf(797,plain,
% 141.11/141.17 (P10(f47(f47(f59(x7971),x7972),f5(f60(x7971,x7972),f60(x7971,x7972))))),
% 141.11/141.17 inference(scs_inference,[],[120,792,795,124,2,3,21])).
% 141.11/141.17 cnf(805,plain,
% 141.11/141.17 (E(f47(x8051,f4(f47(f59(x8052),x8053),x8054)),f47(x8051,f4(f60(x8052,x8053),x8054)))),
% 141.11/141.17 inference(scs_inference,[],[158,5,6])).
% 141.11/141.17 cnf(806,plain,
% 141.11/141.17 (E(f47(f47(f59(x8061),x8062),x8063),f59(f5(f60(x8061,x8062),f59(x8063))))),
% 141.11/141.17 inference(scs_inference,[],[794,2])).
% 141.11/141.17 cnf(807,plain,
% 141.11/141.17 (E(f59(f5(f47(f59(x8071),x8072),f59(x8073))),f47(f60(x8071,x8072),x8073))),
% 141.11/141.17 inference(scs_inference,[],[120,793,794,2,3])).
% 141.11/141.17 cnf(816,plain,
% 141.11/141.17 (E(f59(f5(f47(f59(x8161),x8162),f59(x8163))),f59(f5(f60(x8161,x8162),f59(x8163))))),
% 141.11/141.17 inference(scs_inference,[],[120,807,806,2,3])).
% 141.11/141.17 cnf(824,plain,
% 141.11/141.17 (E(f59(f5(f60(x8241,x8242),f59(x8243))),f59(f5(f47(f59(x8241),x8242),f59(x8243))))),
% 141.11/141.17 inference(scs_inference,[],[816,2])).
% 141.11/141.17 cnf(993,plain,
% 141.11/141.17 (E(f60(f60(x9931,f47(f59(x9932),x9933)),x9934),f60(f60(x9931,f60(x9932,x9933)),x9934))),
% 141.11/141.17 inference(scs_inference,[],[158,9,10])).
% 141.11/141.17 cnf(1531,plain,
% 141.11/141.17 (~P10(f59(f5(f47(f59(x15311),x15312),f59(x15313))))+P10(f47(f60(x15311,x15312),x15313))),
% 141.11/141.17 inference(scs_inference,[],[807,21])).
% 141.11/141.17 cnf(1540,plain,
% 141.11/141.17 (P10(f59(f5(f59(x15401),f5(f60(x15402,x15403),x15404))))+~P10(f59(f5(f47(f59(x15402),x15403),f59(x15401))))),
% 141.11/141.17 inference(scs_inference,[],[746,816,21,121])).
% 141.11/141.17 cnf(1547,plain,
% 141.11/141.17 (~P10(f59(f5(f60(x15471,x15472),f59(x15473))))+P10(f59(f5(f47(f59(x15471),x15472),f59(x15473))))),
% 141.11/141.17 inference(scs_inference,[],[824,21])).
% 141.11/141.17 cnf(1633,plain,
% 141.11/141.17 (P10(f47(f60(x16331,x16332),f5(f47(f59(x16331),x16332),f47(f59(x16331),x16332))))),
% 141.11/141.17 inference(scs_inference,[],[124,793,21])).
% 141.11/141.17 cnf(1662,plain,
% 141.11/141.17 (~P10(f59(f5(f59(x16621),f59(x16622))))+P10(f5(f47(f59(x16621),x16622),f47(f59(x16621),x16622)))),
% 141.11/141.17 inference(scs_inference,[],[1633,601,121])).
% 141.11/141.17 cnf(1683,plain,
% 141.11/141.17 (P10(f59(f5(x16831,f59(f5(x16831,x16831)))))),
% 141.11/141.17 inference(scs_inference,[],[124,173,21])).
% 141.11/141.17 cnf(1685,plain,
% 141.11/141.17 (P10(f59(f5(f59(f5(x16851,x16851)),f5(x16851,x16852))))),
% 141.11/141.17 inference(scs_inference,[],[124,173,21,751])).
% 141.11/141.17 cnf(1688,plain,
% 141.11/141.17 (P10(f59(f5(f5(x16881,x16882),f59(x16881))))),
% 141.11/141.17 inference(scs_inference,[],[125,173,21])).
% 141.11/141.17 cnf(1690,plain,
% 141.11/141.17 (P10(f59(f5(f59(x16901),f5(f5(x16901,x16902),x16903))))),
% 141.11/141.17 inference(scs_inference,[],[125,173,21,751])).
% 141.11/141.17 cnf(1693,plain,
% 141.11/141.17 (P10(f59(f5(f5(f5(x16931,x16932),x16933),f5(f59(x16931),x16934))))),
% 141.11/141.17 inference(scs_inference,[],[1690,751])).
% 141.11/141.17 cnf(1695,plain,
% 141.11/141.17 (P10(f59(f5(f59(x16951),x16951)))),
% 141.11/141.17 inference(scs_inference,[],[1690,159,1688,751,121])).
% 141.11/141.17 cnf(1700,plain,
% 141.11/141.17 (P10(f59(f5(x17001,f5(f59(x17001),x17002))))),
% 141.11/141.17 inference(scs_inference,[],[1695,751])).
% 141.11/141.17 cnf(1702,plain,
% 141.11/141.17 (P10(f59(f5(f5(f59(x17021),x17022),f5(x17021,x17023))))),
% 141.11/141.17 inference(scs_inference,[],[1695,1693,159,751,121])).
% 141.11/141.17 cnf(1706,plain,
% 141.11/141.17 (P10(f60(f59(x17061),x17061))),
% 141.11/141.17 inference(scs_inference,[],[1695,1693,159,122,751,121,21])).
% 141.11/141.17 cnf(1711,plain,
% 141.11/141.17 (E(x17111,x17112)+~P10(f59(f59(f4(x17111,x17112))))),
% 141.11/141.17 inference(scs_inference,[],[147,1706,21,119])).
% 141.11/141.17 cnf(1713,plain,
% 141.11/141.17 (~P10(f59(f59(f4(f4(a21,a25),f47(a21,a25)))))),
% 141.11/141.17 inference(scs_inference,[],[147,1706,149,21,119,121])).
% 141.11/141.17 cnf(1716,plain,
% 141.11/141.17 (~E(f47(f5(x17161,x17162),x17161),f59(f59(f4(x17163,x17164))))+E(x17163,x17164)),
% 141.11/141.17 inference(scs_inference,[],[125,1711,21])).
% 141.11/141.17 cnf(1746,plain,
% 141.11/141.17 (P10(f5(f60(f59(x17461),x17461),f60(f59(x17461),x17461)))),
% 141.11/141.17 inference(scs_inference,[],[1706,124,121])).
% 141.11/141.17 cnf(1810,plain,
% 141.11/141.17 (P10(f5(f47(f59(f59(x18101)),x18101),f47(f59(f59(x18101)),x18101)))),
% 141.11/141.17 inference(scs_inference,[],[1683,1706,1531,121])).
% 141.11/141.17 cnf(1831,plain,
% 141.11/141.17 (~E(f5(f47(f59(f59(x18311)),x18311),f47(f59(f59(x18311)),x18311)),f47(f4(a21,a25),f47(a21,a25)))),
% 141.11/141.17 inference(scs_inference,[],[1695,126,1662,21])).
% 141.11/141.17 cnf(1862,plain,
% 141.11/141.17 (P10(f59(f5(x18621,f59(f5(x18621,x18621)))))),
% 141.11/141.17 inference(rename_variables,[],[1683])).
% 141.11/141.17 cnf(1869,plain,
% 141.11/141.17 (E(f59(f5(f59(f60(x18691,f47(f59(x18692),x18693))),f59(x18694))),f60(f60(x18691,f60(x18692,x18693)),x18694))),
% 141.11/141.17 inference(scs_inference,[],[1685,122,1683,1862,805,993,1540,1547,2,751,3])).
% 141.11/141.17 cnf(1872,plain,
% 141.11/141.17 (P10(f59(f5(f5(f59(f5(x18721,x18721)),x18722),x18721)))),
% 141.11/141.17 inference(scs_inference,[],[1700,159,1685,122,1683,1862,805,993,1540,1547,2,751,3,121])).
% 141.11/141.17 cnf(1932,plain,
% 141.11/141.17 (~E(f5(f60(f59(x19321),x19321),f60(f59(x19321),x19321)),f5(f5(f47(f4(a21,a25),f47(a21,a25)),x19322),x19323))),
% 141.11/141.17 inference(scs_inference,[],[1746,753,1831,1683,824,117,8,4,5,6,7,9,10,11,12,1662,2,121,21])).
% 141.11/141.17 cnf(1949,plain,
% 141.11/141.17 (~E(f5(f5(f47(f4(a21,a25),f47(a21,a25)),x19491),x19492),f5(f60(f59(x19493),x19493),f60(f59(x19493),x19493)))),
% 141.11/141.17 inference(scs_inference,[],[1932,816,10,5,7,11,12,9,8,6,4,2])).
% 141.11/141.17 cnf(1952,plain,
% 141.11/141.17 (~E(f5(f47(f5(x19521,x19522),x19521),f47(f5(x19521,x19522),x19521)),f5(f5(f4(f4(a21,a25),f47(a21,a25)),x19523),x19524))),
% 141.11/141.17 inference(scs_inference,[],[130,772,1932,1688,816,10,5,7,11,12,9,8,6,4,2,121,21])).
% 141.11/141.17 cnf(1959,plain,
% 141.11/141.17 (E(f5(f59(f5(f59(x19591),f59(x19592))),x19593),f5(f60(x19591,x19592),x19593))),
% 141.11/141.17 inference(scs_inference,[],[122,11])).
% 141.11/141.17 cnf(1960,plain,
% 141.11/141.17 (E(f60(f59(f5(f59(x19601),f59(x19602))),x19603),f60(f60(x19601,x19602),x19603))),
% 141.11/141.17 inference(scs_inference,[],[122,11,9])).
% 141.11/141.17 cnf(1964,plain,
% 141.11/141.17 (E(f59(f59(f5(f59(x19641),f59(x19642)))),f59(f60(x19641,x19642)))),
% 141.11/141.17 inference(scs_inference,[],[122,11,9,10,5,6,8])).
% 141.11/141.17 cnf(1969,plain,
% 141.11/141.17 (~E(f5(f47(f5(x19691,x19692),x19691),f47(f5(x19691,x19692),x19691)),f59(f59(f4(f4(a21,a25),f47(a21,a25)))))),
% 141.11/141.17 inference(scs_inference,[],[1713,1952,130,122,11,9,10,5,6,8,12,7,4,2,21])).
% 141.11/141.17 cnf(1972,plain,
% 141.11/141.17 (~E(x19721,f59(f59(f4(f4(a21,a25),f47(a21,a25)))))+~E(f5(f47(f5(x19722,x19723),x19722),f47(f5(x19722,x19723),x19722)),x19721)),
% 141.11/141.17 inference(scs_inference,[],[1713,1952,130,122,11,9,10,5,6,8,12,7,4,2,21,117,3])).
% 141.11/141.17 cnf(1980,plain,
% 141.11/141.17 (E(f47(f5(f59(f5(f59(x19801),f59(x19802))),x19803),x19804),f47(f5(f60(x19801,x19802),x19803),x19804))),
% 141.11/141.17 inference(scs_inference,[],[1959,5,11,8,9,7,4])).
% 141.11/141.17 cnf(1984,plain,
% 141.11/141.17 (~E(f59(f59(f4(f4(a21,a25),f47(a21,a25)))),f5(f47(f5(x19841,x19842),x19841),f47(f5(x19841,x19842),x19841)))),
% 141.11/141.17 inference(scs_inference,[],[1959,1969,5,11,8,9,7,4,12,10,6,2])).
% 141.11/141.17 cnf(2011,plain,
% 141.11/141.17 (~P10(f4(f59(f59(f4(f4(a21,a25),f47(a21,a25)))),x20111))+~E(x20111,f5(f47(f5(x20112,x20113),x20112),f47(f5(x20112,x20113),x20112)))),
% 141.11/141.17 inference(scs_inference,[],[1960,174,1810,1984,797,149,9,5,11,4,10,6,12,7,8,121,21,2,3,117])).
% 141.11/141.17 cnf(2060,plain,
% 141.11/141.17 (~E(f47(f5(f59(f5(f59(x20601),f59(x20601))),x20602),x20601),f5(f47(f4(a21,a25),f47(a21,a25)),x20603))),
% 141.11/141.17 inference(scs_inference,[],[1964,1872,144,120,12,6,4,11,7,8,5,10,9,21,2,3])).
% 141.11/141.17 cnf(2125,plain,
% 141.11/141.17 (E(f4(f47(f47(f59(x21251),x21252),x21253),x21254),f4(f47(f60(x21251,x21252),x21253),x21254))),
% 141.11/141.17 inference(scs_inference,[],[793,11,12,6])).
% 141.11/141.17 cnf(2126,plain,
% 141.11/141.17 (E(f4(x21261,f47(f47(f59(x21262),x21263),x21264)),f4(x21261,f47(f60(x21262,x21263),x21264)))),
% 141.11/141.17 inference(scs_inference,[],[793,11,12,6,7])).
% 141.11/141.17 cnf(2132,plain,
% 141.11/141.17 (~E(f47(f5(f60(x21321,x21321),x21322),x21321),f5(f47(f4(a21,a25),f47(a21,a25)),x21323))),
% 141.11/141.17 inference(scs_inference,[],[1980,2060,793,11,12,6,7,10,8,9,5,4,3])).
% 141.11/141.17 cnf(2136,plain,
% 141.11/141.17 (~E(f5(f47(f4(a21,a25),f47(a21,a25)),x21361),f47(f5(f60(x21362,x21362),x21363),x21362))),
% 141.11/141.17 inference(scs_inference,[],[1980,2060,793,11,12,6,7,10,8,9,5,4,3,117,2])).
% 141.11/141.17 cnf(2137,plain,
% 141.11/141.17 (~P10(f4(f5(f47(f4(a21,a25),f47(a21,a25)),x21371),f47(f5(f60(x21372,x21372),x21373),x21372)))),
% 141.11/141.17 inference(scs_inference,[],[2136,117])).
% 141.11/141.17 cnf(2159,plain,
% 141.11/141.17 (E(f5(f60(x21591,x21592),x21593),f5(f47(f59(x21591),x21592),x21593))),
% 141.11/141.17 inference(scs_inference,[],[147,11])).
% 141.11/141.17 cnf(2160,plain,
% 141.11/141.17 (E(f5(x21601,f60(x21602,x21603)),f5(x21601,f47(f59(x21602),x21603)))),
% 141.11/141.17 inference(scs_inference,[],[147,11,12])).
% 141.11/141.17 cnf(2161,plain,
% 141.11/141.17 (E(f60(x21611,f60(x21612,x21613)),f60(x21611,f47(f59(x21612),x21613)))),
% 141.11/141.17 inference(scs_inference,[],[147,11,12,10])).
% 141.11/141.17 cnf(2162,plain,
% 141.11/141.17 (E(f4(f60(x21621,x21622),x21623),f4(f47(f59(x21621),x21622),x21623))),
% 141.11/141.17 inference(scs_inference,[],[147,11,12,10,6])).
% 141.11/141.17 cnf(2163,plain,
% 141.11/141.17 (E(f59(f60(x21631,x21632)),f59(f47(f59(x21631),x21632)))),
% 141.11/141.17 inference(scs_inference,[],[147,11,12,10,6,8])).
% 141.11/141.17 cnf(2164,plain,
% 141.11/141.17 (E(f47(x21641,f60(x21642,x21643)),f47(x21641,f47(f59(x21642),x21643)))),
% 141.11/141.17 inference(scs_inference,[],[147,11,12,10,6,8,5])).
% 141.11/141.17 cnf(2166,plain,
% 141.11/141.17 (E(f4(x21661,f60(x21662,x21663)),f4(x21661,f47(f59(x21662),x21663)))),
% 141.11/141.17 inference(scs_inference,[],[147,172,11,12,10,6,8,5,4,7])).
% 141.11/141.17 cnf(2167,plain,
% 141.11/141.17 (E(f60(f60(x21671,x21672),x21673),f60(f47(f59(x21671),x21672),x21673))),
% 141.11/141.17 inference(scs_inference,[],[147,172,11,12,10,6,8,5,4,7,9])).
% 141.11/141.17 cnf(2175,plain,
% 141.11/141.17 (E(f47(f5(f60(x21751,x21752),x21753),x21754),f47(f5(f47(f59(x21751),x21752),x21753),x21754))),
% 141.11/141.17 inference(scs_inference,[],[2159,11,12,6,10,5,8,9,4])).
% 141.11/141.17 cnf(2177,plain,
% 141.11/141.17 (~E(f47(f5(f60(f60(x21771,x21772),f60(x21771,x21772)),x21773),f47(f59(x21771),x21772)),f5(f47(f4(a21,a25),f47(a21,a25)),x21774))),
% 141.11/141.17 inference(scs_inference,[],[2159,2164,2132,11,12,6,10,5,8,9,4,7,3])).
% 141.11/141.17 cnf(2182,plain,
% 141.11/141.17 (~E(f5(f47(f4(a21,a25),f47(a21,a25)),x21821),f47(f5(f60(f60(x21822,x21823),f60(x21822,x21823)),x21824),f47(f59(x21822),x21823)))),
% 141.11/141.17 inference(scs_inference,[],[2159,2164,2132,11,12,6,10,5,8,9,4,7,3,117,2])).
% 141.11/141.17 cnf(2185,plain,
% 141.11/141.17 (E(f5(f60(x21851,f60(x21852,x21853)),x21854),f5(f60(x21851,f47(f59(x21852),x21853)),x21854))),
% 141.11/141.17 inference(scs_inference,[],[2161,2182,117,11])).
% 141.11/141.17 cnf(2198,plain,
% 141.11/141.17 (~E(f4(f5(f47(f4(a21,a25),f47(a21,a25)),x21981),f47(f5(f60(x21982,x21982),x21983),x21982)),f59(f5(f5(f59(x21984),x21985),f5(x21984,x21986))))),
% 141.11/141.17 inference(scs_inference,[],[2160,2161,2162,2166,2182,2137,1702,117,11,10,12,6,8,5,7,9,4,3,21,2])).
% 141.11/141.17 cnf(2208,plain,
% 141.11/141.17 (~E(f47(f5(f47(f59(f60(x22081,x22082)),f60(x22081,x22082)),x22083),f47(f59(x22081),x22082)),f5(f47(f4(a21,a25),f47(a21,a25)),x22084))),
% 141.11/141.17 inference(scs_inference,[],[2163,2167,2177,2175,11,12,10,6,8,5,4,9,7,3])).
% 141.11/141.17 cnf(2246,plain,
% 141.11/141.17 (E(f5(f47(x22461,f60(x22462,x22463)),x22464),f5(f47(x22461,f47(f59(x22462),x22463)),x22464))),
% 141.11/141.17 inference(scs_inference,[],[2164,11])).
% 141.11/141.17 cnf(2284,plain,
% 141.11/141.17 (~E(f5(f47(f59(f59(x22841)),x22841),f47(f59(f59(x22841)),x22841)),f5(f4(f4(a21,a25),f47(a21,a25)),x22842))),
% 141.11/141.17 inference(scs_inference,[],[2125,2126,2167,1810,2162,758,11,10,6,12,8,5,9,4,7,3,21])).
% 141.11/141.17 cnf(2295,plain,
% 141.11/141.17 (~E(f5(f47(f59(f59(f60(x22951,x22952))),f47(f59(x22951),x22952)),f47(f59(f59(f60(x22951,x22952))),f60(x22951,x22952))),f47(f4(a21,a25),f47(a21,a25)))),
% 141.11/141.17 inference(scs_inference,[],[2246,2284,1831,2162,172,11,6,12,10,8,2,5,9,7,4,3])).
% 141.11/141.17 cnf(2300,plain,
% 141.11/141.17 (E(f5(f5(f47(x23001,x23002),f47(x23002,x23001)),x23003),f5(f4(x23001,x23002),x23003))),
% 141.11/141.17 inference(scs_inference,[],[123,11])).
% 141.11/141.17 cnf(2301,plain,
% 141.11/141.17 (E(f5(x23011,f5(f47(x23012,x23013),f47(x23013,x23012))),f5(x23011,f4(x23012,x23013)))),
% 141.11/141.17 inference(scs_inference,[],[123,11,12])).
% 141.11/141.17 cnf(2302,plain,
% 141.11/141.17 (E(f60(x23021,f5(f47(x23022,x23023),f47(x23023,x23022))),f60(x23021,f4(x23022,x23023)))),
% 141.11/141.17 inference(scs_inference,[],[123,11,12,10])).
% 141.11/141.17 cnf(2303,plain,
% 141.11/141.17 (E(f4(f5(f47(x23031,x23032),f47(x23032,x23031)),x23033),f4(f4(x23031,x23032),x23033))),
% 141.11/141.17 inference(scs_inference,[],[123,11,12,10,6])).
% 141.11/141.17 cnf(2304,plain,
% 141.11/141.17 (E(f59(f5(f47(x23041,x23042),f47(x23042,x23041))),f59(f4(x23041,x23042)))),
% 141.11/141.17 inference(scs_inference,[],[123,11,12,10,6,8])).
% 141.11/141.18 cnf(2306,plain,
% 141.11/141.18 (E(f47(x23061,f5(f47(x23062,x23063),f47(x23063,x23062))),f47(x23061,f4(x23062,x23063)))),
% 141.11/141.18 inference(scs_inference,[],[2295,123,11,12,10,6,8,2,5])).
% 141.11/141.18 cnf(2307,plain,
% 141.11/141.18 (E(f60(f5(f47(x23071,x23072),f47(x23072,x23071)),x23073),f60(f4(x23071,x23072),x23073))),
% 141.11/141.18 inference(scs_inference,[],[2295,123,11,12,10,6,8,2,5,9])).
% 141.11/141.18 cnf(2308,plain,
% 141.11/141.18 (E(f47(f5(f47(x23081,x23082),f47(x23082,x23081)),x23083),f47(f4(x23081,x23082),x23083))),
% 141.11/141.18 inference(scs_inference,[],[2295,123,11,12,10,6,8,2,5,9,4])).
% 141.11/141.18 cnf(2309,plain,
% 141.11/141.18 (E(f4(x23091,f5(f47(x23092,x23093),f47(x23093,x23092))),f4(x23091,f4(x23092,x23093)))),
% 141.11/141.18 inference(scs_inference,[],[2295,123,11,12,10,6,8,2,5,9,4,7])).
% 141.11/141.18 cnf(2313,plain,
% 141.11/141.18 (E(f5(f59(f5(f47(x23131,x23132),f47(x23132,x23131))),x23133),f5(f59(f4(x23131,x23132)),x23133))),
% 141.11/141.18 inference(scs_inference,[],[2304,11])).
% 141.11/141.18 cnf(2316,plain,
% 141.11/141.18 (E(f4(f59(f5(f47(x23161,x23162),f47(x23162,x23161))),x23163),f4(f59(f4(x23161,x23162)),x23163))),
% 141.11/141.18 inference(scs_inference,[],[2304,11,8,10,6])).
% 141.11/141.18 cnf(2317,plain,
% 141.11/141.18 (E(f5(x23171,f59(f5(f47(x23172,x23173),f47(x23173,x23172)))),f5(x23171,f59(f4(x23172,x23173))))),
% 141.11/141.18 inference(scs_inference,[],[2304,11,8,10,6,12])).
% 141.11/141.18 cnf(2320,plain,
% 141.11/141.18 (E(f4(x23201,f59(f5(f47(x23202,x23203),f47(x23203,x23202)))),f4(x23201,f59(f4(x23202,x23203))))),
% 141.11/141.18 inference(scs_inference,[],[2304,11,8,10,6,12,5,9,7])).
% 141.11/141.18 cnf(2322,plain,
% 141.11/141.18 (~E(f47(f4(f59(f60(x23221,x23222)),f60(x23221,x23222)),f47(f59(x23221),x23222)),f5(f47(f4(a21,a25),f47(a21,a25)),x23223))),
% 141.11/141.18 inference(scs_inference,[],[2304,2308,2208,11,8,10,6,12,5,9,7,4,3])).
% 141.11/141.18 cnf(2325,plain,
% 141.11/141.18 (~P10(f4(f47(f4(f59(f60(x23251,x23252)),f60(x23251,x23252)),f47(f59(x23251),x23252)),f5(f47(f4(a21,a25),f47(a21,a25)),x23253)))),
% 141.11/141.18 inference(scs_inference,[],[2304,2308,2208,11,8,10,6,12,5,9,7,4,3,117])).
% 141.11/141.18 cnf(2327,plain,
% 141.11/141.18 (~E(f5(f47(f4(a21,a25),f47(a21,a25)),x23271),f47(f4(f59(f60(x23272,x23273)),f60(x23272,x23273)),f47(f59(x23272),x23273)))),
% 141.11/141.18 inference(scs_inference,[],[2304,2308,2208,11,8,10,6,12,5,9,7,4,3,117,2])).
% 141.11/141.18 cnf(2328,plain,
% 141.11/141.18 (~P10(f4(f5(f47(f4(a21,a25),f47(a21,a25)),x23281),f47(f4(f59(f60(x23282,x23283)),f60(x23282,x23283)),f47(f59(x23282),x23283))))),
% 141.11/141.18 inference(scs_inference,[],[2327,117])).
% 141.11/141.18 cnf(2339,plain,
% 141.11/141.18 (~E(f5(f4(f4(a21,a25),f47(a21,a25)),x23391),f5(f60(f59(x23392),x23392),f60(f59(x23392),x23392)))),
% 141.11/141.18 inference(scs_inference,[],[2300,2327,1949,117,11,6,8,12,10,5,9,4,7,3])).
% 141.11/141.18 cnf(2342,plain,
% 141.11/141.18 (~E(f47(x23421,f5(x23421,x23421)),f4(f47(f4(f59(f60(x23422,x23423)),f60(x23422,x23423)),f47(f59(x23422),x23423)),f5(f47(f4(a21,a25),f47(a21,a25)),x23424)))),
% 141.11/141.18 inference(scs_inference,[],[2300,2327,2325,1949,124,117,11,6,8,12,10,5,9,4,7,3,21])).
% 141.11/141.18 cnf(2343,plain,
% 141.11/141.18 (~E(f5(f60(f59(x23431),x23431),f60(f59(x23431),x23431)),f5(f4(f4(a21,a25),f47(a21,a25)),x23432))),
% 141.11/141.18 inference(scs_inference,[],[2300,2327,2325,1949,124,117,11,6,8,12,10,5,9,4,7,3,21,2])).
% 141.11/141.18 cnf(2344,plain,
% 141.11/141.18 (~P10(f4(f5(f4(f4(a21,a25),f47(a21,a25)),x23441),f5(f60(f59(x23442),x23442),f60(f59(x23442),x23442))))),
% 141.11/141.18 inference(scs_inference,[],[2339,117])).
% 141.11/141.18 cnf(2352,plain,
% 141.11/141.18 (~E(f4(f47(f4(f59(f60(x23521,x23522)),f60(x23521,x23522)),f47(f59(x23521),x23522)),f5(f47(f4(a21,a25),f47(a21,a25)),x23523)),f47(x23524,f5(x23524,x23524)))),
% 141.11/141.18 inference(scs_inference,[],[2301,2339,2342,117,8,11,6,12,10,5,2])).
% 141.11/141.18 cnf(2356,plain,
% 141.11/141.18 (~E(f5(f60(f59(f60(x23561,x23562)),f47(f59(x23561),x23562)),f60(f59(f60(x23561,x23562)),f60(x23561,x23562))),f5(f4(f4(a21,a25),f47(a21,a25)),x23563))),
% 141.11/141.18 inference(scs_inference,[],[2301,2339,2343,2185,2342,117,8,11,6,12,10,5,2,9,4,7,3])).
% 141.11/141.18 cnf(2362,plain,
% 141.11/141.18 (~P10(f4(f5(f60(f59(x23621),x23621),f60(f59(x23621),x23621)),f5(f4(f4(a21,a25),f47(a21,a25)),x23622)))),
% 141.11/141.18 inference(scs_inference,[],[2343,117])).
% 141.11/141.18 cnf(2366,plain,
% 141.11/141.18 (E(f59(f60(x23661,f5(f47(x23662,x23663),f47(x23663,x23662)))),f59(f60(x23661,f4(x23662,x23663))))),
% 141.11/141.18 inference(scs_inference,[],[2302,2343,117,6,12,8])).
% 141.11/141.18 cnf(2374,plain,
% 141.11/141.18 (~E(f4(f4(f4(a21,a25),f47(a21,a25)),f47(f5(f60(x23741,x23741),x23742),x23741)),f59(f5(f5(f59(x23743),x23744),f5(x23743,x23745))))),
% 141.11/141.18 inference(scs_inference,[],[2302,2303,2356,2198,2343,117,6,12,8,11,10,5,2,9,7,4,3])).
% 141.11/141.18 cnf(2377,plain,
% 141.11/141.18 (~E(f59(f5(f5(x23771,x23772),f59(x23771))),f4(f5(f4(f4(a21,a25),f47(a21,a25)),x23773),f5(f60(f59(x23774),x23774),f60(f59(x23774),x23774))))),
% 141.11/141.18 inference(scs_inference,[],[2302,2303,2344,2356,2198,2343,1688,117,6,12,8,11,10,5,2,9,7,4,3,21])).
% 141.11/141.18 cnf(2378,plain,
% 141.11/141.18 (E(f59(f47(x23781,f5(f47(x23782,x23783),f47(x23783,x23782)))),f59(f47(x23781,f4(x23782,x23783))))),
% 141.11/141.18 inference(scs_inference,[],[2306,8])).
% 141.11/141.18 cnf(2387,plain,
% 141.11/141.18 (E(f4(x23871,f47(x23872,f5(f47(x23873,x23874),f47(x23874,x23873)))),f4(x23871,f47(x23872,f4(x23873,x23874))))),
% 141.11/141.18 inference(scs_inference,[],[2306,2374,8,6,11,12,5,10,2,9,4,7])).
% 141.11/141.18 cnf(2388,plain,
% 141.11/141.18 (~E(f4(f47(f4(f59(f60(x23881,x23882)),f60(x23881,x23882)),f47(f59(x23881),x23882)),f4(f4(a21,a25),f47(a21,a25))),f47(x23883,f5(x23883,x23883)))),
% 141.11/141.18 inference(scs_inference,[],[2306,2309,2374,2352,8,6,11,12,5,10,2,9,4,7,3])).
% 141.11/141.18 cnf(2391,plain,
% 141.11/141.18 (~P10(f4(f4(f47(f4(f59(f60(x23911,x23912)),f60(x23911,x23912)),f47(f59(x23911),x23912)),f4(f4(a21,a25),f47(a21,a25))),f47(x23913,f5(x23913,x23913))))),
% 141.11/141.18 inference(scs_inference,[],[2388,117])).
% 141.11/141.18 cnf(2393,plain,
% 141.11/141.18 (E(f59(f60(f5(f47(x23931,x23932),f47(x23932,x23931)),x23933)),f59(f60(f4(x23931,x23932),x23933)))),
% 141.11/141.18 inference(scs_inference,[],[2307,2388,117,8])).
% 141.11/141.18 cnf(2421,plain,
% 141.11/141.18 (E(f5(x24211,f47(f5(f47(x24212,x24213),f47(x24213,x24212)),x24214)),f5(x24211,f47(f4(x24212,x24213),x24214)))),
% 141.11/141.18 inference(scs_inference,[],[2308,12])).
% 141.11/141.18 cnf(2423,plain,
% 141.11/141.18 (E(f5(f47(f5(f47(x24231,x24232),f47(x24232,x24231)),x24233),x24234),f5(f47(f4(x24231,x24232),x24233),x24234))),
% 141.11/141.18 inference(scs_inference,[],[2308,12,6,11])).
% 141.11/141.18 cnf(2424,plain,
% 141.11/141.18 (E(f59(f47(f5(f47(x24241,x24242),f47(x24242,x24241)),x24243)),f59(f47(f4(x24241,x24242),x24243)))),
% 141.11/141.18 inference(scs_inference,[],[2308,12,6,11,8])).
% 141.11/141.18 cnf(2434,plain,
% 141.11/141.18 (~E(f5(f47(f5(f47(x24341,x24342),f47(x24342,x24341)),f47(x24341,x24342)),f47(f4(x24341,x24342),f47(x24341,x24342))),f59(f59(f4(f4(a21,a25),f47(a21,a25)))))),
% 141.11/141.18 inference(scs_inference,[],[2313,2317,2377,2308,12,6,11,8,2,5,10,9,7,4,3,1972])).
% 141.11/141.18 cnf(2435,plain,
% 141.11/141.18 (~E(f59(f5(f59(x24351),x24351)),f4(f5(f60(f59(x24352),x24352),f60(f59(x24352),x24352)),f5(f4(f4(a21,a25),f47(a21,a25)),x24353)))),
% 141.11/141.18 inference(scs_inference,[],[2313,2317,2362,2377,2308,1695,12,6,11,8,2,5,10,9,7,4,3,1972,21])).
% 141.11/141.18 cnf(2447,plain,
% 141.11/141.18 (~E(f5(f47(f4(x24471,x24472),f47(x24471,x24472)),f47(f4(x24471,x24472),f47(x24471,x24472))),f59(f59(f4(f4(a21,a25),f47(a21,a25)))))),
% 141.11/141.18 inference(scs_inference,[],[2423,2434,2309,11,12,8,6,2,5,10,9,7,4,3])).
% 141.11/141.18 cnf(2450,plain,
% 141.11/141.18 (~E(f59(f5(x24501,f5(f59(x24501),x24502))),f59(f59(f4(f4(a21,a25),f47(a21,a25)))))),
% 141.11/141.18 inference(scs_inference,[],[2423,2434,2309,1713,1700,11,12,8,6,2,5,10,9,7,4,3,21])).
% 141.11/141.18 cnf(2457,plain,
% 141.11/141.18 (~E(f59(f59(f4(f4(a21,a25),f47(a21,a25)))),f5(f47(f4(x24571,x24572),f47(x24571,x24572)),f47(f4(x24571,x24572),f47(x24571,x24572))))),
% 141.11/141.18 inference(scs_inference,[],[2447,172,186,8,11,6,12,2])).
% 141.11/141.18 cnf(2466,plain,
% 141.11/141.18 (~E(f60(f59(x24661),x24661),f4(f4(f47(f4(f59(f60(x24662,x24663)),f60(x24662,x24663)),f47(f59(x24662),x24663)),f4(f4(a21,a25),f47(a21,a25))),f47(x24664,f5(x24664,x24664))))),
% 141.11/141.18 inference(scs_inference,[],[2316,2320,2447,2391,1706,172,186,8,11,6,12,2,5,10,9,7,4,3,21])).
% 141.11/141.18 cnf(2470,plain,
% 141.11/141.18 (E(f5(f47(x24701,x24702),x24703),f5(f59(f5(x24701,f59(x24702))),x24703))),
% 141.11/141.18 inference(scs_inference,[],[186,173,8,11])).
% 141.11/141.18 cnf(2473,plain,
% 141.11/141.18 (~E(f4(f4(f47(f4(f59(f60(x24731,x24732)),f60(x24731,x24732)),f47(f59(x24731),x24732)),f4(f4(a21,a25),f47(a21,a25))),f47(x24733,f5(x24733,x24733))),f60(f59(x24734),x24734))),
% 141.11/141.18 inference(scs_inference,[],[2466,186,173,8,11,6,12,2])).
% 141.11/141.18 cnf(2474,plain,
% 141.11/141.18 (E(f47(x24741,f47(x24742,x24743)),f47(x24741,f59(f5(x24742,f59(x24743)))))),
% 141.11/141.18 inference(scs_inference,[],[2466,186,173,8,11,6,12,2,5])).
% 141.11/141.18 cnf(2478,plain,
% 141.11/141.18 (E(f47(f47(x24781,x24782),x24783),f47(f59(f5(x24781,f59(x24782))),x24783))),
% 141.11/141.18 inference(scs_inference,[],[2466,186,173,8,11,6,12,2,5,10,9,7,4])).
% 141.11/141.18 cnf(2479,plain,
% 141.11/141.18 (~E(f59(f59(f4(f4(a21,a25),f47(a21,a25)))),f5(f47(f4(x24791,x24792),f47(x24791,x24792)),f47(f5(f47(x24791,x24792),f47(x24792,x24791)),f47(x24791,x24792))))),
% 141.11/141.18 inference(scs_inference,[],[2421,2457,2466,186,173,8,11,6,12,2,5,10,9,7,4,3])).
% 141.11/141.18 cnf(2496,plain,
% 141.11/141.18 (~E(f5(f59(f5(f5(x24961,x24962),f59(x24961))),f47(f5(x24961,x24962),x24961)),f59(f59(f4(f4(a21,a25),f47(a21,a25)))))),
% 141.11/141.18 inference(scs_inference,[],[2470,2474,2322,2479,2328,124,8,11,6,12,2,5,10,7,9,4,3,21,1972])).
% 141.11/141.18 cnf(2527,plain,
% 141.11/141.18 (~E(f5(f60(f59(x25271),x25271),f60(f59(x25271),x25271)),f59(f5(f4(a21,a25),f59(f47(a21,a25)))))),
% 141.11/141.18 inference(scs_inference,[],[2478,2366,2393,2496,133,1746,758,8,6,11,12,2,5,7,10,9,4,121,3,21])).
% 141.11/141.18 cnf(2532,plain,
% 141.11/141.18 (~E(f59(f5(f4(a21,a25),f59(f47(a21,a25)))),f5(f60(f59(x25321),x25321),f60(f59(x25321),x25321)))),
% 141.11/141.18 inference(scs_inference,[],[2527,2474,8,12,11,6,2])).
% 141.11/141.18 cnf(2538,plain,
% 141.11/141.18 (~E(f4(f4(f47(f4(f59(f60(x25381,x25382)),f60(x25381,x25382)),f47(f59(x25381),x25382)),f4(f4(a21,a25),f47(a21,a25))),f47(f47(x25383,x25383),f4(x25383,x25383))),f60(f59(x25384),x25384))),
% 141.11/141.18 inference(scs_inference,[],[2387,2527,2473,2474,8,12,11,6,2,5,10,7,4,9,3])).
% 141.11/141.18 cnf(2544,plain,
% 141.11/141.18 (E(f59(f4(x25441,x25442)),f59(f5(f47(x25441,x25442),f47(x25442,x25441))))),
% 141.11/141.18 inference(scs_inference,[],[129,8])).
% 141.11/141.18 cnf(2546,plain,
% 141.11/141.18 (E(f5(f4(x25461,x25462),x25463),f5(f5(f47(x25461,x25462),f47(x25462,x25461)),x25463))),
% 141.11/141.18 inference(scs_inference,[],[173,129,8,6,11])).
% 141.11/141.18 cnf(2549,plain,
% 141.11/141.18 (E(f47(x25491,f4(x25492,x25493)),f47(x25491,f5(f47(x25492,x25493),f47(x25493,x25492))))),
% 141.11/141.18 inference(scs_inference,[],[2538,173,129,8,6,11,12,2,5])).
% 141.11/141.18 cnf(2552,plain,
% 141.11/141.18 (E(f60(f47(x25521,x25522),x25523),f60(f59(f5(x25521,f59(x25522))),x25523))),
% 141.11/141.18 inference(scs_inference,[],[2538,173,129,8,6,11,12,2,5,7,10,9])).
% 141.11/141.18 cnf(2553,plain,
% 141.11/141.18 (E(f47(f4(x25531,x25532),x25533),f47(f5(f47(x25531,x25532),f47(x25532,x25531)),x25533))),
% 141.11/141.18 inference(scs_inference,[],[2538,173,129,8,6,11,12,2,5,7,10,9,4])).
% 141.11/141.18 cnf(2557,plain,
% 141.11/141.18 (~E(f5(f47(f5(x25571,x25572),x25571),f47(f5(x25571,x25572),x25571)),f59(f5(f5(f59(f47(a21,a25)),f59(f47(a21,a25))),f4(a21,a25))))),
% 141.11/141.18 inference(scs_inference,[],[2378,2424,2538,174,130,173,129,8,6,11,12,2,5,7,10,9,4,3,21])).
% 141.11/141.18 cnf(2569,plain,
% 141.11/141.18 (~E(f47(f4(a21,a25),f47(a21,a25)),f5(f60(f59(x25691),x25691),f60(f59(x25691),x25691)))),
% 141.11/141.18 inference(scs_inference,[],[2544,2532,2557,120,8,6,12,11,2,5,9,7,10,4,3])).
% 141.11/141.18 cnf(2583,plain,
% 141.11/141.18 (~E(f47(f5(f47(a21,a25),f47(a25,a21)),f47(a21,a25)),f5(f60(f59(x25831),x25831),f60(f59(x25831),x25831)))),
% 141.11/141.18 inference(scs_inference,[],[2546,2553,2569,8,6,12,11,2,5,9,10,7,4,3])).
% 141.11/141.18 cnf(2595,plain,
% 141.11/141.18 (E(f5(f47(x25951,f4(x25952,x25953)),x25954),f5(f47(x25951,f5(f47(x25952,x25953),f47(x25953,x25952))),x25954))),
% 141.11/141.18 inference(scs_inference,[],[2549,2583,117,8,6,12,11])).
% 141.11/141.18 cnf(2678,plain,
% 141.11/141.18 (~E(f59(f59(f4(f4(a21,a25),f47(a21,a25)))),f59(f5(x26781,f5(f59(x26781),x26782))))),
% 141.11/141.18 inference(scs_inference,[],[2450,2552,8,6,11,12,2])).
% 141.11/141.18 cnf(2692,plain,
% 141.11/141.18 (E(f5(x26921,f47(f4(x26922,x26923),x26924)),f5(x26921,f47(f5(f47(x26922,x26923),f47(x26923,x26922)),x26924)))),
% 141.11/141.18 inference(scs_inference,[],[2553,8,6,12])).
% 141.11/141.18 cnf(2859,plain,
% 141.11/141.18 (E(f4(f60(x28591,x28592),x28593),f4(f59(f5(f59(x28591),f59(x28592))),x28593))),
% 141.11/141.18 inference(scs_inference,[],[143,794,8,11,12,5,6])).
% 141.11/141.18 cnf(2910,plain,
% 141.11/141.18 (~E(f4(f5(f60(f59(x29101),x29101),f60(f59(x29101),x29101)),f5(f4(f4(a21,a25),f47(a21,a25)),x29102)),f59(f5(f59(x29103),x29103)))),
% 141.11/141.18 inference(scs_inference,[],[2435,2859,8,11,12,2])).
% 141.11/141.18 cnf(3296,plain,
% 141.11/141.18 ($false),
% 141.11/141.18 inference(scs_inference,[],[173,125,126,2308,2343,1872,2284,2910,1869,2678,2595,2692,2,8,11,1972,751,136,2011,1716,3,21]),
% 141.11/141.18 ['proof']).
% 141.11/141.18 % SZS output end Proof
% 141.11/141.18 % Total time :140.616046s
%------------------------------------------------------------------------------