%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HWV026-1 : TPTP v8.2.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n021.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 07:29:15 EDT 2024
% Result : Unsatisfiable 59.20s 59.27s
% Output : CNFRefutation 59.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.13 % Problem : HWV026-1 : TPTP v8.2.0. Released v2.5.0.
% 0.00/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n021.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Fri Jun 21 03:45:24 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.52/0.58 start to proof:theBenchmark
% 59.20/59.26 %-------------------------------------------
% 59.20/59.26 % File :CSE---1.7
% 59.20/59.26 % Problem :theBenchmark
% 59.20/59.26 % Transform :cnf
% 59.20/59.26 % Format :tptp:raw
% 59.20/59.26 % Command :java -jar mcs_scs.jar %d %s
% 59.20/59.26
% 59.20/59.26 % Result :Theorem 58.630000s
% 59.20/59.26 % Output :CNFRefutation 58.630000s
% 59.20/59.26 %-------------------------------------------
% 59.20/59.27 %--------------------------------------------------------------------------
% 59.20/59.27 % File : HWV026-1 : TPTP v8.2.0. Released v2.5.0.
% 59.20/59.27 % Domain : Hardware Verification
% 59.20/59.27 % Problem : Safelogic VHDL design verification obligation
% 59.20/59.27 % Version : [Mar02] axioms : Especial.
% 59.20/59.27 % English :
% 59.20/59.27
% 59.20/59.27 % Refs : [CHM02] Claessen et al. (2002), Verification of Hardware Systems
% 59.20/59.27 % : [Mar02] Martensson (2002), Email to G. Sutcliffe
% 59.20/59.27 % Source : [Mar02]
% 59.20/59.27 % Names :
% 59.20/59.27
% 59.20/59.27 % Status : Unsatisfiable
% 59.20/59.27 % Rating : 0.05 v7.5.0, 0.00 v7.4.0, 0.06 v7.3.0, 0.00 v7.0.0, 0.07 v6.4.0, 0.00 v5.5.0, 0.10 v5.3.0, 0.06 v5.0.0, 0.00 v3.3.0, 0.07 v3.2.0, 0.00 v3.1.0, 0.09 v2.7.0, 0.17 v2.6.0, 0.00 v2.5.0
% 59.20/59.27 % Syntax : Number of clauses : 94 ( 8 unt; 65 nHn; 85 RR)
% 59.20/59.27 % Number of literals : 375 ( 50 equ; 159 neg)
% 59.20/59.27 % Maximal clause size : 7 ( 3 avg)
% 59.20/59.27 % Maximal term depth : 3 ( 1 avg)
% 59.20/59.27 % Number of predicates : 13 ( 12 usr; 0 prp; 1-3 aty)
% 59.20/59.27 % Number of functors : 11 ( 11 usr; 4 con; 0-2 aty)
% 59.20/59.27 % Number of variables : 139 ( 5 sgn)
% 59.20/59.27 % SPC : CNF_UNS_RFO_SEQ_NHN
% 59.20/59.27
% 59.20/59.27 % Comments :
% 59.20/59.27 %--------------------------------------------------------------------------
% 59.20/59.27 %----Include equality
% 59.20/59.27 %----Include VHDL design axioms
% 59.20/59.27 include('Axioms/HWV003-0.ax').
% 59.20/59.27 %--------------------------------------------------------------------------
% 59.20/59.27 cnf(quest_1,negated_conjecture,
% 59.20/59.27 ~ p_Wr(t_139) ).
% 59.20/59.27
% 59.20/59.27 cnf(quest_2,negated_conjecture,
% 59.20/59.27 ~ p_Reset(t_139) ).
% 59.20/59.27
% 59.20/59.27 cnf(quest_3,negated_conjecture,
% 59.20/59.27 ( ~ p_Wr_error(t_139)
% 59.20/59.27 | ~ p_Wr_error(plus(t_139,n1)) ) ).
% 59.20/59.27
% 59.20/59.27 cnf(quest_4,negated_conjecture,
% 59.20/59.27 ( p_Wr_error(t_139)
% 59.20/59.27 | p_Wr_error(plus(t_139,n1)) ) ).
% 59.20/59.27
% 59.20/59.27 %--------------------------------------------------------------------------
% 59.20/59.27 %-------------------------------------------
% 59.20/59.27 % Proof found
% 59.20/59.27 % SZS status Theorem for theBenchmark
% 59.20/59.27 % SZS output start Proof
% 59.20/59.27 %ClaNum:122(EqnAxiom:29)
% 59.20/59.27 %VarNum:496(SingletonVarNum:136)
% 59.20/59.27 %MaxLitNum:7
% 59.20/59.27 %MaxfuncDepth:2
% 59.20/59.27 %SharedTerms:14
% 59.20/59.27 %goalClause: 33 34 44 51
% 59.20/59.27 %singleGoalClaCount:2
% 59.20/59.27 [33]~P3(a7)
% 59.20/59.27 [34]~P11(a7)
% 59.20/59.27 [36]~P1(x361,x361)
% 59.20/59.27 [31]E(f6(a1,x311),x311)
% 59.20/59.27 [32]P1(f6(x321,a5),a1)
% 59.20/59.27 [35]~E(f6(x351,a5),a1)
% 59.20/59.27 [44]P12(a7)+P12(f6(a7,a5))
% 59.20/59.27 [51]~P12(a7)+~P12(f6(a7,a5))
% 59.20/59.27 [41]P1(x411,a1)+E(x411,a1)
% 59.20/59.27 [37]~P4(x371)+E(f2(x371),a1)
% 59.20/59.27 [38]~P7(x381)+E(f2(x381),a3)
% 59.20/59.27 [39]P7(x391)+~E(f2(x391),a3)
% 59.20/59.27 [40]P4(x401)+~E(f2(x401),a1)
% 59.20/59.27 [58]~P3(x581)+~P12(f6(x581,a5))
% 59.20/59.27 [59]~P3(x591)+~P10(f6(x591,a5))
% 59.20/59.28 [64]~P1(x641,a1)+P1(x641,f4(x641,a5))
% 59.20/59.28 [42]E(x421,a1)+E(f6(f9(x421),a5),x421)
% 59.20/59.28 [46]~P3(x461)+E(f2(f6(x461,a5)),a1)
% 59.20/59.28 [47]~P3(x471)+E(f10(f6(x471,a5)),a1)
% 59.20/59.28 [48]~P3(x481)+E(f8(f6(x481,a5)),a1)
% 59.20/59.28 [43]~P2(x431,x432)+~E(x431,x432)
% 59.20/59.28 [55]~P2(x552,x551)+~P1(x551,x552)
% 59.20/59.28 [50]E(x501,x502)+~E(f6(x501,a5),f6(x502,a5))
% 59.20/59.28 [72]~P3(x721)+~P5(x722,f6(x721,a5))
% 59.20/59.28 [84]~P1(x841,x842)+P1(f6(x841,a5),f6(x842,a5))
% 59.20/59.28 [97]P1(x971,x972)+~P1(f6(x971,a5),f6(x972,a5))
% 59.20/59.28 [104]~P3(x1041)+~P9(x1042,x1043,f6(x1041,a5))
% 59.20/59.28 [49]P3(x491)+P11(x491)+E(f10(f6(x491,a5)),f10(x491))
% 59.20/59.28 [45]P1(x452,x451)+P1(x451,x452)+E(x451,x452)
% 59.20/59.28 [78]~P1(x782,x781)+P1(x782,f6(x781,a5))+E(f6(x781,a5),x782)
% 59.20/59.28 [81]P1(x811,x812)+E(x811,x812)+~P1(f6(x811,a5),x812)
% 59.20/59.28 [65]~P1(x651,x653)+P1(x651,x652)+~P1(x653,x652)
% 59.20/59.28 [61]P2(x612,x613)+~E(f4(x613,x612),x611)+E(f6(x611,x612),x613)
% 59.20/59.28 [62]P2(x622,x621)+~E(f6(x623,x622),x621)+E(f4(x621,x622),x623)
% 59.20/59.28 [52]P11(x521)+~P12(x521)+P3(x521)+P12(f6(x521,a5))
% 59.20/59.28 [63]P12(x631)+P11(x631)+P3(x631)+~P12(f6(x631,a5))
% 59.20/59.28 [67]~P11(x671)+~P8(x671)+P3(x671)+~P12(f6(x671,a5))
% 59.20/59.28 [53]P3(x531)+P11(x531)+P8(x531)+E(f2(f6(x531,a5)),f2(x531))
% 59.20/59.28 [54]P3(x541)+P11(x541)+P8(x541)+E(f8(f6(x541,a5)),f8(x541))
% 59.20/59.28 [56]P3(x561)+P8(x561)+~P11(x561)+E(f8(f6(x561,a5)),f8(x561))
% 59.20/59.28 [112]P11(x1121)+~P9(x1122,x1123,x1121)+P3(x1121)+P9(x1122,x1123,f6(x1121,a5))
% 59.20/59.28 [115]P11(x1151)+P3(x1151)+P9(x1152,x1153,x1151)+~P9(x1152,x1153,f6(x1151,a5))
% 59.20/59.28 [57]P11(x571)+P8(x571)+~P10(x571)+P3(x571)+P10(f6(x571,a5))
% 59.20/59.28 [60]P8(x601)+~P10(x601)+~P11(x601)+P3(x601)+P10(f6(x601,a5))
% 59.20/59.28 [66]P10(x661)+P11(x661)+P8(x661)+P3(x661)+~P10(f6(x661,a5))
% 59.20/59.28 [68]P8(x681)+~P11(x681)+P3(x681)+P1(a3,f2(x681))+P12(f6(x681,a5))
% 59.20/59.28 [69]P11(x691)+~P8(x691)+P3(x691)+P1(f2(x691),a1)+P10(f6(x691,a5))
% 59.20/59.28 [70]P10(x701)+P8(x701)+~P11(x701)+P3(x701)+~P10(f6(x701,a5))
% 59.20/59.28 [71]~P11(x711)+~P8(x711)+P3(x711)+P1(f2(x711),a1)+P10(f6(x711,a5))
% 59.20/59.28 [88]P8(x881)+~P11(x881)+P3(x881)+~P1(a3,f2(x881))+~P12(f6(x881,a5))
% 59.20/59.28 [89]P11(x891)+~P8(x891)+P3(x891)+~P1(f2(x891),a1)+~P10(f6(x891,a5))
% 59.20/59.28 [93]~P11(x931)+~P8(x931)+P3(x931)+~P1(f2(x931),a1)+~P10(f6(x931,a5))
% 59.20/59.28 [73]P3(x731)+P8(x731)+~P11(x731)+P1(a3,f2(x731))+E(f2(f6(x731,a5)),f2(x731))
% 59.20/59.28 [74]P3(x741)+P8(x741)+~P11(x741)+P1(a3,f2(x741))+E(f10(f6(x741,a5)),f10(x741))
% 59.20/59.28 [75]P3(x751)+P11(x751)+~P8(x751)+P1(f2(x751),a1)+E(f2(f6(x751,a5)),f2(x751))
% 59.20/59.28 [76]P3(x761)+P11(x761)+~P8(x761)+P1(f2(x761),a1)+E(f8(f6(x761,a5)),f8(x761))
% 59.20/59.28 [77]P3(x771)+~P11(x771)+~P8(x771)+P1(f2(x771),a1)+E(f8(f6(x771,a5)),f8(x771))
% 59.20/59.28 [83]P3(x831)+~P11(x831)+~P8(x831)+~P1(f2(x831),a1)+E(f2(f6(x831,a5)),f2(x831))
% 59.20/59.28 [85]P3(x851)+~P11(x851)+~P8(x851)+P1(f2(x851),a1)+E(f2(f6(x851,a5)),f6(f2(x851),a5))
% 59.20/59.28 [86]P3(x861)+~P11(x861)+~P8(x861)+P1(f4(a3,a5),f10(x861))+E(f10(f6(x861,a5)),a1)
% 59.20/59.28 [91]P3(x911)+P8(x911)+~P11(x911)+~P1(a3,f2(x911))+E(f2(f6(x911,a5)),f6(f2(x911),a5))
% 59.20/59.28 [92]P3(x921)+P11(x921)+~P8(x921)+~P1(f2(x921),a1)+E(f2(f6(x921,a5)),f4(f2(x921),a5))
% 59.20/59.28 [103]P3(x1031)+~P11(x1031)+~P8(x1031)+~P1(f4(a3,a5),f10(x1031))+E(f10(f6(x1031,a5)),f6(f10(x1031),a5))
% 59.20/59.28 [79]P11(x791)+P8(x791)+~P5(x792,x791)+P3(x791)+P5(x792,f6(x791,a5))
% 59.20/59.28 [82]P8(x821)+~P11(x821)+~P5(x822,x821)+P3(x821)+P5(x822,f6(x821,a5))
% 59.20/59.28 [87]P11(x871)+P8(x871)+P3(x871)+P5(x872,x871)+~P5(x872,f6(x871,a5))
% 59.20/59.28 [90]P8(x901)+~P11(x901)+P3(x901)+P5(x902,x901)+~P5(x902,f6(x901,a5))
% 59.20/59.28 [102]~P11(x1021)+~P8(x1021)+~P6(x1022,x1021)+P3(x1021)+P9(f10(x1021),x1022,f6(x1021,a5))
% 59.20/59.28 [109]~P11(x1091)+~P8(x1091)+P3(x1091)+P6(x1092,x1091)+~P9(f10(x1091),x1092,f6(x1091,a5))
% 59.20/59.28 [99]P3(x991)+P8(x991)+~P11(x991)+P1(f4(a3,a5),f10(x991))+~P1(a3,f2(x991))+E(f10(f6(x991,a5)),a1)
% 59.20/59.28 [100]P3(x1001)+P11(x1001)+~P8(x1001)+P1(f4(a3,a5),f8(x1001))+~P1(f2(x1001),a1)+E(f8(f6(x1001,a5)),a1)
% 59.20/59.28 [101]P3(x1011)+~P11(x1011)+~P8(x1011)+P1(f4(a3,a5),f8(x1011))+~P1(f2(x1011),a1)+E(f8(f6(x1011,a5)),a1)
% 59.20/59.28 [106]P3(x1061)+P8(x1061)+~P11(x1061)+~P1(f4(a3,a5),f10(x1061))+~P1(a3,f2(x1061))+E(f10(f6(x1061,a5)),f6(f10(x1061),a5))
% 59.20/59.28 [107]P3(x1071)+P11(x1071)+~P8(x1071)+~P1(f4(a3,a5),f8(x1071))+~P1(f2(x1071),a1)+E(f8(f6(x1071,a5)),f6(f8(x1071),a5))
% 59.20/59.28 [108]P3(x1081)+~P11(x1081)+~P8(x1081)+~P1(f4(a3,a5),f8(x1081))+~P1(f2(x1081),a1)+E(f8(f6(x1081,a5)),f6(f8(x1081),a5))
% 59.20/59.28 [94]P11(x941)+~P8(x941)+~P5(x942,x941)+P3(x941)+P5(x942,f6(x941,a5))+P1(f2(x941),a1)
% 59.20/59.28 [95]~P11(x951)+~P8(x951)+~P5(x952,x951)+P3(x951)+P5(x952,f6(x951,a5))+P1(f2(x951),a1)
% 59.20/59.28 [96]P11(x961)+~P8(x961)+P3(x961)+P5(x962,x961)+~P5(x962,f6(x961,a5))+P1(f2(x961),a1)
% 59.20/59.28 [98]~P11(x981)+~P8(x981)+P3(x981)+P5(x982,x981)+~P5(x982,f6(x981,a5))+P1(f2(x981),a1)
% 59.20/59.28 [105]P8(x1051)+~P11(x1051)+~P6(x1052,x1051)+P3(x1051)+P9(f10(x1051),x1052,f6(x1051,a5))+~P1(a3,f2(x1051))
% 59.20/59.28 [110]P11(x1101)+~P8(x1101)+P3(x1101)+P9(f8(x1101),x1102,x1101)+~P5(x1102,f6(x1101,a5))+~P1(f2(x1101),a1)
% 59.20/59.28 [111]~P11(x1111)+~P8(x1111)+P3(x1111)+P9(f8(x1111),x1112,x1111)+~P5(x1112,f6(x1111,a5))+~P1(f2(x1111),a1)
% 59.20/59.28 [113]P11(x1131)+~P8(x1131)+P3(x1131)+~P9(f8(x1131),x1132,x1131)+P5(x1132,f6(x1131,a5))+~P1(f2(x1131),a1)
% 59.20/59.28 [114]~P11(x1141)+~P8(x1141)+P3(x1141)+~P9(f8(x1141),x1142,x1141)+P5(x1142,f6(x1141,a5))+~P1(f2(x1141),a1)
% 59.20/59.28 [117]P8(x1171)+~P11(x1171)+P3(x1171)+P6(x1172,x1171)+~P9(f10(x1171),x1172,f6(x1171,a5))+~P1(a3,f2(x1171))
% 59.20/59.28 [116]P3(x1162)+~P11(x1162)+~P8(x1162)+~P9(x1161,x1163,x1162)+P9(x1161,x1163,f6(x1162,a5))+E(x1161,f10(x1162))
% 59.20/59.28 [118]P8(x1181)+~P11(x1181)+~P9(x1182,x1183,x1181)+P3(x1181)+P9(x1182,x1183,f6(x1181,a5))+P1(a3,f2(x1181))
% 59.20/59.28 [119]P3(x1192)+~P11(x1192)+~P8(x1192)+P9(x1191,x1193,x1192)+~P9(x1191,x1193,f6(x1192,a5))+E(x1191,f10(x1192))
% 59.20/59.28 [120]P8(x1201)+~P11(x1201)+P3(x1201)+P9(x1202,x1203,x1201)+~P9(x1202,x1203,f6(x1201,a5))+P1(a3,f2(x1201))
% 59.20/59.28 [121]P3(x1212)+P8(x1212)+~P11(x1212)+~P9(x1211,x1213,x1212)+P9(x1211,x1213,f6(x1212,a5))+E(x1211,f10(x1212))+~P1(a3,f2(x1212))
% 59.20/59.28 [122]P3(x1222)+P8(x1222)+~P11(x1222)+P9(x1221,x1223,x1222)+~P9(x1221,x1223,f6(x1222,a5))+E(x1221,f10(x1222))+~P1(a3,f2(x1222))
% 59.20/59.28 %EqnAxiom
% 59.20/59.28 [1]E(x11,x11)
% 59.20/59.28 [2]E(x22,x21)+~E(x21,x22)
% 59.20/59.28 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.20/59.28 [4]~E(x41,x42)+E(f6(x41,x43),f6(x42,x43))
% 59.20/59.28 [5]~E(x51,x52)+E(f6(x53,x51),f6(x53,x52))
% 59.20/59.28 [6]~E(x61,x62)+E(f2(x61),f2(x62))
% 59.20/59.28 [7]~E(x71,x72)+E(f10(x71),f10(x72))
% 59.20/59.28 [8]~E(x81,x82)+E(f4(x81,x83),f4(x82,x83))
% 59.20/59.28 [9]~E(x91,x92)+E(f4(x93,x91),f4(x93,x92))
% 59.20/59.28 [10]~E(x101,x102)+E(f8(x101),f8(x102))
% 59.20/59.28 [11]~E(x111,x112)+E(f9(x111),f9(x112))
% 59.20/59.28 [12]P1(x122,x123)+~E(x121,x122)+~P1(x121,x123)
% 59.20/59.28 [13]P1(x133,x132)+~E(x131,x132)+~P1(x133,x131)
% 59.20/59.28 [14]~P3(x141)+P3(x142)+~E(x141,x142)
% 59.20/59.28 [15]~P11(x151)+P11(x152)+~E(x151,x152)
% 59.20/59.28 [16]P9(x162,x163,x164)+~E(x161,x162)+~P9(x161,x163,x164)
% 59.20/59.28 [17]P9(x173,x172,x174)+~E(x171,x172)+~P9(x173,x171,x174)
% 59.20/59.28 [18]P9(x183,x184,x182)+~E(x181,x182)+~P9(x183,x184,x181)
% 59.20/59.28 [19]~P4(x191)+P4(x192)+~E(x191,x192)
% 59.20/59.28 [20]~P7(x201)+P7(x202)+~E(x201,x202)
% 59.20/59.28 [21]~P8(x211)+P8(x212)+~E(x211,x212)
% 59.20/59.28 [22]~P12(x221)+P12(x222)+~E(x221,x222)
% 59.20/59.28 [23]P5(x232,x233)+~E(x231,x232)+~P5(x231,x233)
% 59.20/59.28 [24]P5(x243,x242)+~E(x241,x242)+~P5(x243,x241)
% 59.20/59.28 [25]P2(x252,x253)+~E(x251,x252)+~P2(x251,x253)
% 59.20/59.28 [26]P2(x263,x262)+~E(x261,x262)+~P2(x263,x261)
% 59.20/59.28 [27]~P10(x271)+P10(x272)+~E(x271,x272)
% 59.20/59.28 [28]P6(x282,x283)+~E(x281,x282)+~P6(x281,x283)
% 59.20/59.28 [29]P6(x293,x292)+~E(x291,x292)+~P6(x293,x291)
% 59.20/59.28
% 59.20/59.28 %-------------------------------------------
% 59.20/59.29 cnf(123,plain,
% 59.20/59.29 (~P2(x1231,x1231)),
% 59.20/59.29 inference(equality_inference,[],[43])).
% 59.20/59.29 cnf(125,plain,
% 59.20/59.29 (P2(x1251,x1252)+E(f6(f4(x1252,x1251),x1251),x1252)),
% 59.20/59.29 inference(equality_inference,[],[61])).
% 59.20/59.29 cnf(126,plain,
% 59.20/59.29 (P2(x1261,f6(x1262,x1261))+E(f4(f6(x1262,x1261),x1261),x1262)),
% 59.20/59.29 inference(equality_inference,[],[62])).
% 59.20/59.29 cnf(127,plain,
% 59.20/59.29 (~P2(f6(a1,x1271),x1271)),
% 59.20/59.29 inference(scs_inference,[],[31,43])).
% 59.20/59.29 cnf(129,plain,
% 59.20/59.29 (E(x1291,f6(a1,x1291))),
% 59.20/59.29 inference(scs_inference,[],[31,43,2])).
% 59.20/59.29 cnf(130,plain,
% 59.20/59.29 (~P2(a1,f6(x1301,a5))),
% 59.20/59.29 inference(scs_inference,[],[31,32,43,2,55])).
% 59.20/59.29 cnf(132,plain,
% 59.20/59.29 (P2(a5,a1)),
% 59.20/59.29 inference(scs_inference,[],[31,32,35,43,2,55,125])).
% 59.20/59.29 cnf(133,plain,
% 59.20/59.29 (~E(f6(x1331,a5),a1)),
% 59.20/59.29 inference(rename_variables,[],[35])).
% 59.20/59.29 cnf(136,plain,
% 59.20/59.29 (E(f6(a1,x1361),x1361)),
% 59.20/59.29 inference(rename_variables,[],[31])).
% 59.20/59.29 cnf(138,plain,
% 59.20/59.29 (E(f6(a1,x1381),x1381)),
% 59.20/59.29 inference(rename_variables,[],[31])).
% 59.20/59.29 cnf(139,plain,
% 59.20/59.29 (~E(f6(x1391,a5),f6(a1,a1))),
% 59.20/59.29 inference(scs_inference,[],[33,34,31,136,138,32,35,133,43,2,55,125,14,15,3])).
% 59.20/59.29 cnf(140,plain,
% 59.20/59.29 (E(f6(a1,x1401),x1401)),
% 59.20/59.29 inference(rename_variables,[],[31])).
% 59.20/59.29 cnf(141,plain,
% 59.20/59.29 (~E(a1,f6(x1411,a5))),
% 59.20/59.29 inference(scs_inference,[],[33,34,36,31,136,138,32,35,133,43,2,55,125,14,15,3,13])).
% 59.20/59.29 cnf(142,plain,
% 59.20/59.29 (~P1(x1421,x1421)),
% 59.20/59.29 inference(rename_variables,[],[36])).
% 59.20/59.29 cnf(146,plain,
% 59.20/59.29 (~P1(a1,x1461)),
% 59.20/59.29 inference(scs_inference,[],[33,34,36,142,31,136,138,32,35,133,43,2,55,125,14,15,3,13,65,78])).
% 59.20/59.29 cnf(148,plain,
% 59.20/59.29 (~E(a5,a1)),
% 59.20/59.29 inference(scs_inference,[],[33,34,123,36,142,31,136,138,32,35,133,43,2,55,125,14,15,3,13,65,78,25])).
% 59.20/59.29 cnf(149,plain,
% 59.20/59.29 (~P2(x1491,x1491)),
% 59.20/59.29 inference(rename_variables,[],[123])).
% 59.20/59.29 cnf(150,plain,
% 59.20/59.29 (~E(a1,a5)),
% 59.20/59.29 inference(scs_inference,[],[33,34,123,149,36,142,31,136,138,32,35,133,43,2,55,125,14,15,3,13,65,78,25,26])).
% 59.20/59.29 cnf(152,plain,
% 59.20/59.29 (P1(a5,a1)),
% 59.20/59.29 inference(scs_inference,[],[33,34,123,149,36,142,31,136,138,32,35,133,43,2,55,125,14,15,3,13,65,78,25,26,41])).
% 59.20/59.29 cnf(154,plain,
% 59.20/59.29 (~P12(f6(a1,x1541))+P12(x1541)),
% 59.20/59.29 inference(scs_inference,[],[33,34,123,149,36,142,31,136,138,140,32,35,133,43,2,55,125,14,15,3,13,65,78,25,26,41,22])).
% 59.20/59.29 cnf(155,plain,
% 59.20/59.29 (P2(a5,f6(a1,a1))+~E(f4(f6(a1,a1),a5),x1551)),
% 59.20/59.29 inference(scs_inference,[],[33,34,123,149,36,142,31,136,138,140,32,35,133,43,2,55,125,14,15,3,13,65,78,25,26,41,22,61])).
% 59.20/59.29 cnf(161,plain,
% 59.20/59.29 (P2(a5,f6(a1,a1))),
% 59.20/59.29 inference(equality_inference,[],[155])).
% 59.20/59.29 cnf(162,plain,
% 59.20/59.29 (~P2(x1621,f6(a1,x1621))),
% 59.20/59.29 inference(scs_inference,[],[129,43])).
% 59.20/59.29 cnf(164,plain,
% 59.20/59.29 (~P2(a1,a5)),
% 59.20/59.29 inference(scs_inference,[],[129,152,43,55])).
% 59.20/59.29 cnf(168,plain,
% 59.20/59.29 (~E(f6(x1681,a5),f6(a1,f6(a1,a1)))),
% 59.20/59.29 inference(scs_inference,[],[127,129,139,152,161,31,43,55,25,3])).
% 59.20/59.29 cnf(172,plain,
% 59.20/59.29 (E(f6(a1,f6(a1,a1)),a1)),
% 59.20/59.29 inference(scs_inference,[],[127,129,139,123,152,161,31,43,55,25,3,26,42])).
% 59.20/59.29 cnf(174,plain,
% 59.20/59.29 (E(a1,f6(a1,f6(a1,a1)))),
% 59.20/59.29 inference(scs_inference,[],[127,129,139,123,152,161,31,43,55,25,3,26,42,2])).
% 59.20/59.29 cnf(176,plain,
% 59.20/59.29 (~E(f4(a5,a1),a1)),
% 59.20/59.29 inference(scs_inference,[],[127,129,139,123,152,161,31,43,55,25,3,26,42,2,15,61])).
% 59.20/59.29 cnf(178,plain,
% 59.20/59.29 (P1(f4(a5,a1),a1)),
% 59.20/59.29 inference(scs_inference,[],[127,129,139,123,152,161,31,43,55,25,3,26,42,2,15,61,41])).
% 59.20/59.29 cnf(183,plain,
% 59.20/59.29 (~P12(x1831)+P12(f6(a1,x1831))),
% 59.20/59.29 inference(scs_inference,[],[127,129,139,123,152,161,31,43,55,25,3,26,42,2,15,61,41,27,20,14,22])).
% 59.20/59.29 cnf(184,plain,
% 59.20/59.29 (~E(a1,f4(a5,a1))),
% 59.20/59.29 inference(scs_inference,[],[127,129,139,123,152,161,36,31,43,55,25,3,26,42,2,15,61,41,27,20,14,22,13])).
% 59.20/59.29 cnf(187,plain,
% 59.20/59.29 (~E(a5,f6(a1,a1))),
% 59.20/59.29 inference(scs_inference,[],[168,5])).
% 59.20/59.29 cnf(188,plain,
% 59.20/59.29 (~E(f6(x1881,a5),f6(a1,f6(a1,a1)))),
% 59.20/59.29 inference(rename_variables,[],[168])).
% 59.20/59.29 cnf(189,plain,
% 59.20/59.29 (P2(a5,f6(a1,f6(a1,a1)))),
% 59.20/59.29 inference(scs_inference,[],[168,188,5,125])).
% 59.20/59.29 cnf(190,plain,
% 59.20/59.29 (~E(f6(x1901,a5),f6(a1,f6(a1,a1)))),
% 59.20/59.29 inference(rename_variables,[],[168])).
% 59.20/59.29 cnf(192,plain,
% 59.20/59.29 (~P2(a1,f4(a5,a1))),
% 59.20/59.29 inference(scs_inference,[],[168,188,178,5,125,55])).
% 59.20/59.29 cnf(194,plain,
% 59.20/59.29 (~P2(a1,f6(a1,f6(a1,a1)))),
% 59.20/59.29 inference(scs_inference,[],[168,188,174,178,5,125,55,43])).
% 59.20/59.29 cnf(198,plain,
% 59.20/59.29 (~E(f6(x1981,a5),f6(a1,f6(a1,f6(a1,a1))))),
% 59.20/59.29 inference(scs_inference,[],[162,168,188,190,174,178,161,31,5,125,55,43,26,3])).
% 59.20/59.29 cnf(200,plain,
% 59.20/59.29 (E(f6(a1,f6(a1,f6(a1,a1))),a1)),
% 59.20/59.29 inference(scs_inference,[],[162,168,188,190,174,178,161,31,5,125,55,43,26,3,42])).
% 59.20/59.29 cnf(202,plain,
% 59.20/59.29 (E(a1,f6(a1,f6(a1,f6(a1,a1))))),
% 59.20/59.29 inference(scs_inference,[],[162,168,188,190,174,178,161,31,5,125,55,43,26,3,42,2])).
% 59.20/59.29 cnf(207,plain,
% 59.20/59.29 (P1(f4(f6(a1,a5),a1),a1)),
% 59.20/59.29 inference(scs_inference,[],[129,162,168,188,190,174,130,178,161,31,5,125,55,43,26,3,42,2,61,21,41])).
% 59.20/59.29 cnf(218,plain,
% 59.20/59.29 (P2(a5,f6(a1,f6(a1,f6(a1,a1))))),
% 59.20/59.29 inference(scs_inference,[],[129,198,202,207,55,43,61])).
% 59.20/59.29 cnf(222,plain,
% 59.20/59.29 (~E(a1,f4(f6(a1,a5),a1))),
% 59.20/59.29 inference(scs_inference,[],[129,198,202,36,207,55,43,61,13])).
% 59.20/59.29 cnf(224,plain,
% 59.20/59.29 (~E(f6(a1,f6(a1,a1)),f6(a1,a5))),
% 59.20/59.29 inference(scs_inference,[],[129,198,202,162,36,189,207,55,43,61,13,26])).
% 59.20/59.29 cnf(229,plain,
% 59.20/59.29 (~P2(f6(a1,f6(a1,a1)),a1)),
% 59.20/59.29 inference(scs_inference,[],[172,43])).
% 59.20/59.29 cnf(231,plain,
% 59.20/59.29 (~E(f6(a1,f6(a1,a1)),a5)),
% 59.20/59.29 inference(scs_inference,[],[123,172,189,43,26])).
% 59.20/59.29 cnf(234,plain,
% 59.20/59.29 (P2(f6(a1,a1),f6(a1,a5))+~E(f4(f6(a1,a5),f6(a1,a1)),a1)),
% 59.20/59.29 inference(scs_inference,[],[123,172,200,189,224,43,26,14,61])).
% 59.20/59.29 cnf(246,plain,
% 59.20/59.29 (P2(f6(a1,a1),a5)+P1(f4(a5,f6(a1,a1)),a1)),
% 59.20/59.29 inference(scs_inference,[],[162,200,218,231,43,26,61,41])).
% 59.20/59.29 cnf(280,plain,
% 59.20/59.29 (~E(a5,f6(a1,f6(a1,f6(a1,a1))))),
% 59.20/59.29 inference(scs_inference,[],[123,218,25])).
% 59.20/59.29 cnf(318,plain,
% 59.20/59.29 (~E(a1,f6(a1,f6(x3181,a5)))),
% 59.20/59.29 inference(scs_inference,[],[141,31,3])).
% 59.20/59.29 cnf(322,plain,
% 59.20/59.29 (P1(f6(a1,f6(x3221,a5)),a1)),
% 59.20/59.29 inference(scs_inference,[],[146,318,45])).
% 59.20/59.29 cnf(323,plain,
% 59.20/59.29 (~P1(a1,x3231)),
% 59.20/59.29 inference(rename_variables,[],[146])).
% 59.20/59.29 cnf(325,plain,
% 59.20/59.29 (~E(f6(a1,f6(x3251,a5)),a1)),
% 59.20/59.29 inference(scs_inference,[],[146,323,318,45,12])).
% 59.20/59.29 cnf(336,plain,
% 59.20/59.29 (~E(f6(a1,f6(x3361,a5)),f6(a1,f6(a1,a1)))),
% 59.20/59.29 inference(scs_inference,[],[325,172,3])).
% 59.20/59.29 cnf(353,plain,
% 59.20/59.29 (~E(f4(a5,a1),f6(a1,f6(a1,a1)))),
% 59.20/59.29 inference(scs_inference,[],[176,172,3])).
% 59.20/59.29 cnf(361,plain,
% 59.20/59.29 (~E(a1,f6(a1,f4(a5,a1)))),
% 59.20/59.29 inference(scs_inference,[],[184,31,3])).
% 59.20/59.29 cnf(363,plain,
% 59.20/59.29 (E(f4(x3631,f6(a1,f6(a1,a1))),f4(x3631,a1))),
% 59.20/59.29 inference(scs_inference,[],[174,9,2])).
% 59.20/59.29 cnf(364,plain,
% 59.20/59.29 (E(f4(x3641,a1),f4(x3641,f6(a1,f6(a1,a1))))),
% 59.20/59.29 inference(scs_inference,[],[363,2])).
% 59.20/59.29 cnf(367,plain,
% 59.20/59.29 (P1(f6(a1,f4(a5,a1)),a1)),
% 59.20/59.29 inference(scs_inference,[],[361,363,146,2,43,45])).
% 59.20/59.29 cnf(368,plain,
% 59.20/59.29 (~P1(a1,x3681)),
% 59.20/59.29 inference(rename_variables,[],[146])).
% 59.20/59.29 cnf(374,plain,
% 59.20/59.29 (~P2(a1,f6(a1,f4(a5,a1)))),
% 59.20/59.29 inference(scs_inference,[],[361,363,146,368,222,2,43,45,12,3,55])).
% 59.20/59.29 cnf(416,plain,
% 59.20/59.29 (~P1(f6(f6(a1,f6(a1,a1)),a5),f6(a5,a5))),
% 59.20/59.29 inference(scs_inference,[],[189,97,55])).
% 59.20/59.29 cnf(421,plain,
% 59.20/59.29 (~P2(f6(a1,f6(a1,a1)),a5)),
% 59.20/59.29 inference(scs_inference,[],[231,416,84,45,55])).
% 59.20/59.29 cnf(430,plain,
% 59.20/59.29 (E(f6(f6(a1,f6(a1,a1)),a5),f6(a5,a5))+P1(f6(a5,a5),f6(f6(a1,f6(a1,a1)),a5))),
% 59.20/59.29 inference(scs_inference,[],[416,45])).
% 59.20/59.29 cnf(482,plain,
% 59.20/59.29 (~E(a1,f6(a1,f4(f6(a1,a5),a1)))),
% 59.20/59.29 inference(scs_inference,[],[222,31,3])).
% 59.20/59.29 cnf(487,plain,
% 59.20/59.29 (~P1(a1,x4871)),
% 59.20/59.29 inference(rename_variables,[],[146])).
% 59.20/59.29 cnf(491,plain,
% 59.20/59.29 (~E(f6(a1,f6(a1,a1)),f6(a1,f6(a1,a5)))),
% 59.20/59.29 inference(scs_inference,[],[224,482,31,146,487,45,12,3])).
% 59.20/59.29 cnf(505,plain,
% 59.20/59.29 (P2(f6(a1,a1),f6(a1,f6(a1,a5)))+P1(f4(f6(a1,f6(a1,a5)),f6(a1,a1)),a1)),
% 59.20/59.29 inference(scs_inference,[],[491,61,41])).
% 59.20/59.29 cnf(600,plain,
% 59.20/59.29 (~P1(a5,f6(a1,a1))+P1(f4(a5,f6(a1,a1)),a1)),
% 59.20/59.29 inference(scs_inference,[],[246,55])).
% 59.20/59.29 cnf(715,plain,
% 59.20/59.29 (P1(f4(a5,f6(a1,a1)),a1)),
% 59.20/59.29 inference(scs_inference,[],[152,129,600,13])).
% 59.20/59.29 cnf(716,plain,
% 59.20/59.29 (~P2(a1,f4(a5,f6(a1,a1)))),
% 59.20/59.29 inference(scs_inference,[],[715,55])).
% 59.20/59.29 cnf(718,plain,
% 59.20/59.29 (~E(f4(a5,f6(a1,a1)),a1)),
% 59.20/59.29 inference(scs_inference,[],[36,715,55,12])).
% 59.20/59.29 cnf(733,plain,
% 59.20/59.29 (P2(f6(a1,a1),a5)+~E(f6(f6(a1,f6(a1,a1)),f6(a1,a1)),a5)),
% 59.20/59.29 inference(scs_inference,[],[718,172,3,62])).
% 59.20/59.29 cnf(776,plain,
% 59.20/59.29 (P2(f6(a1,a1),f6(a1,a5))+P1(f4(f6(a1,a5),f6(a1,a1)),a1)),
% 59.20/59.29 inference(scs_inference,[],[234,41])).
% 59.20/59.29 cnf(800,plain,
% 59.20/59.29 (~P1(a5,f6(a1,a1))+~E(f6(f6(a1,f6(a1,a1)),f6(a1,a1)),a5)),
% 59.20/59.29 inference(scs_inference,[],[733,55])).
% 59.20/59.29 cnf(803,plain,
% 59.20/59.29 (~P1(f6(a1,a5),f6(a1,a1))+P1(f4(f6(a1,a5),f6(a1,a1)),a1)),
% 59.20/59.29 inference(scs_inference,[],[776,55])).
% 59.20/59.29 cnf(814,plain,
% 59.20/59.29 (~E(a5,f6(f6(a1,f6(a1,a1)),f6(a1,a1)))+~P1(a5,f6(a1,a1))),
% 59.20/59.29 inference(scs_inference,[],[800,2])).
% 59.20/59.29 cnf(817,plain,
% 59.20/59.29 (P1(f4(f6(a1,a5),f6(a1,a1)),a1)),
% 59.20/59.29 inference(scs_inference,[],[32,129,803,13])).
% 59.20/59.29 cnf(818,plain,
% 59.20/59.29 (~P2(a1,f4(f6(a1,a5),f6(a1,a1)))),
% 59.20/59.29 inference(scs_inference,[],[817,55])).
% 59.20/59.29 cnf(824,plain,
% 59.20/59.29 (~E(a5,f6(f6(a1,f6(a1,a1)),f6(a1,a1)))),
% 59.20/59.29 inference(scs_inference,[],[152,129,814,13])).
% 59.20/59.29 cnf(848,plain,
% 59.20/59.29 (~P1(f6(a1,f6(a1,a5)),f6(a1,a1))+P1(f4(f6(a1,f6(a1,a5)),f6(a1,a1)),a1)),
% 59.20/59.29 inference(scs_inference,[],[505,55])).
% 59.20/59.29 cnf(881,plain,
% 59.20/59.29 (P1(f4(f6(a1,f6(a1,a5)),f6(a1,a1)),a1)),
% 59.20/59.29 inference(scs_inference,[],[322,129,848,13])).
% 59.20/59.29 cnf(885,plain,
% 59.20/59.29 (~P1(x8851,x8851)),
% 59.20/59.29 inference(rename_variables,[],[36])).
% 59.20/59.29 cnf(886,plain,
% 59.20/59.29 (~E(a1,f4(f6(a1,f6(a1,a5)),f6(a1,a1)))),
% 59.20/59.29 inference(scs_inference,[],[36,885,881,55,12,13])).
% 59.20/59.29 cnf(942,plain,
% 59.20/59.29 (P1(f6(a5,a5),f6(f6(a1,f6(a1,a1)),a5))),
% 59.20/59.29 inference(scs_inference,[],[231,430,50])).
% 59.20/59.29 cnf(945,plain,
% 59.20/59.29 (~E(f6(a5,a5),f6(f6(a1,f6(a1,a1)),a5))),
% 59.20/59.29 inference(scs_inference,[],[36,942,55,12])).
% 59.20/59.29 cnf(981,plain,
% 59.20/59.29 (~E(f6(a1,a1),f6(x9811,a5))),
% 59.20/59.29 inference(scs_inference,[],[336,2,5])).
% 59.20/59.29 cnf(985,plain,
% 59.20/59.29 (P1(f4(f6(x9851,a5),a1),a1)),
% 59.20/59.29 inference(scs_inference,[],[981,130,61,41])).
% 59.20/59.29 cnf(991,plain,
% 59.20/59.29 (E(f6(f6(a1,f6(a1,a1)),x9911),f6(a1,x9911))),
% 59.20/59.29 inference(scs_inference,[],[174,2,4])).
% 59.20/59.29 cnf(992,plain,
% 59.20/59.29 (E(f6(a1,x9921),f6(f6(a1,f6(a1,a1)),x9921))),
% 59.20/59.29 inference(scs_inference,[],[991,2])).
% 59.20/59.29 cnf(993,plain,
% 59.20/59.29 (~P2(f6(f6(a1,f6(a1,a1)),x9931),f6(a1,x9931))),
% 59.20/59.29 inference(scs_inference,[],[991,2,43])).
% 59.20/59.29 cnf(995,plain,
% 59.20/59.29 (~E(f6(a1,f6(x9951,a5)),f6(f6(a1,f6(a1,a1)),f6(a1,a1)))),
% 59.20/59.29 inference(scs_inference,[],[336,991,2,43,3])).
% 59.20/59.29 cnf(1004,plain,
% 59.20/59.29 (~P2(f6(a1,x10041),f6(f6(a1,f6(a1,a1)),x10041))),
% 59.20/59.29 inference(scs_inference,[],[992,43])).
% 59.20/59.29 cnf(1006,plain,
% 59.20/59.29 (~E(a5,f6(f6(a1,f6(a1,a1)),a1))),
% 59.20/59.29 inference(scs_inference,[],[993,992,161,43,25])).
% 59.20/59.29 cnf(1039,plain,
% 59.20/59.29 (~P12(f6(f6(a1,f6(a1,a1)),x10391))+P12(f6(a1,x10391))),
% 59.20/59.29 inference(scs_inference,[],[991,992,995,14,19,61,22])).
% 59.20/59.29 cnf(1043,plain,
% 59.20/59.29 (~P12(x10431)+P12(f6(f6(a1,f6(a1,a1)),x10431))),
% 59.20/59.29 inference(scs_inference,[],[992,22,183])).
% 59.20/59.29 cnf(1053,plain,
% 59.20/59.29 (~E(f4(a5,a1),f6(f6(a1,f6(a1,a1)),f6(a1,a1)))),
% 59.20/59.29 inference(scs_inference,[],[353,991,3])).
% 59.20/59.29 cnf(1185,plain,
% 59.20/59.29 (~E(f6(a5,a5),f6(a1,a5))),
% 59.20/59.29 inference(scs_inference,[],[945,992,3])).
% 59.20/59.29 cnf(1187,plain,
% 59.20/59.29 (~E(f4(f6(a1,a5),a5),a5)),
% 59.20/59.29 inference(scs_inference,[],[945,992,162,3,61])).
% 59.20/59.29 cnf(1213,plain,
% 59.20/59.29 (E(f6(x12131,f6(a1,f6(a1,a1))),f6(x12131,a1))),
% 59.20/59.29 inference(scs_inference,[],[174,2,5])).
% 59.20/59.29 cnf(1215,plain,
% 59.20/59.29 (~P2(f6(x12151,f6(a1,f6(a1,a1))),f6(x12151,a1))),
% 59.20/59.29 inference(scs_inference,[],[1213,2,43])).
% 59.20/59.29 cnf(1270,plain,
% 59.20/59.29 (~E(f6(a5,a5),a5)),
% 59.20/59.29 inference(scs_inference,[],[1185,129,3])).
% 59.20/59.29 cnf(1272,plain,
% 59.20/59.29 (~E(f4(a5,a5),a5)),
% 59.20/59.29 inference(scs_inference,[],[1185,129,123,3,61])).
% 59.20/59.29 cnf(1276,plain,
% 59.20/59.29 (~E(f6(a5,a5),f6(a1,f6(a1,a5)))),
% 59.20/59.29 inference(scs_inference,[],[1185,31,3])).
% 59.20/59.29 cnf(1282,plain,
% 59.20/59.29 (~E(f4(f6(a1,a5),a5),f6(a1,a5))),
% 59.20/59.29 inference(scs_inference,[],[1187,31,3])).
% 59.20/59.29 cnf(1297,plain,
% 59.20/59.29 (~E(f6(f6(a1,a5),a5),a5)),
% 59.20/59.29 inference(scs_inference,[],[1272,123,31,3,62])).
% 59.20/59.29 cnf(1301,plain,
% 59.20/59.29 (~E(f6(a5,a5),f6(f6(a1,f6(a1,a1)),f6(a1,a5)))),
% 59.20/59.29 inference(scs_inference,[],[1276,991,3])).
% 59.20/59.29 cnf(1306,plain,
% 59.20/59.29 (~E(f4(f6(a1,a5),a5),f6(a1,f6(a1,a5)))),
% 59.20/59.29 inference(scs_inference,[],[1282,31,3])).
% 59.20/59.29 cnf(1308,plain,
% 59.20/59.29 (~E(f6(f6(a1,f6(a1,a5)),a5),f6(a1,a5))),
% 59.20/59.29 inference(scs_inference,[],[1282,162,31,3,62])).
% 59.20/59.29 cnf(1324,plain,
% 59.20/59.29 (~E(f4(f6(a1,a5),a5),f6(f6(a1,f6(a1,a1)),f6(a1,a5)))),
% 59.20/59.29 inference(scs_inference,[],[1306,991,3])).
% 59.20/59.29 cnf(1330,plain,
% 59.20/59.29 (~E(f4(a5,a5),f6(a1,f6(a1,a5)))),
% 59.20/59.29 inference(scs_inference,[],[1308,129,123,3,61])).
% 59.20/59.29 cnf(1335,plain,
% 59.20/59.29 (E(f4(f6(a1,f6(a1,a1)),x13351),f4(a1,x13351))),
% 59.20/59.29 inference(scs_inference,[],[174,2,8])).
% 59.20/59.29 cnf(1394,plain,
% 59.20/59.29 (~E(f4(a5,a5),f6(f6(a1,f6(a1,a1)),f6(a1,a5)))),
% 59.20/59.29 inference(scs_inference,[],[1330,991,3])).
% 59.20/59.29 cnf(1417,plain,
% 59.20/59.29 (P2(a5,f6(f6(a1,f6(a1,a1)),a1))),
% 59.20/59.29 inference(scs_inference,[],[139,129,991,3,61])).
% 59.20/59.29 cnf(1464,plain,
% 59.20/59.29 (P2(a5,f6(f6(a1,f6(a1,a1)),f6(a1,a1)))),
% 59.20/59.29 inference(scs_inference,[],[168,129,991,3,61])).
% 59.20/59.29 cnf(1473,plain,
% 59.20/59.29 (E(f9(f6(a1,f6(a1,a1))),f9(a1))),
% 59.20/59.29 inference(scs_inference,[],[174,2,11])).
% 59.20/59.29 cnf(1474,plain,
% 59.20/59.29 (E(f9(a1),f9(f6(a1,f6(a1,a1))))),
% 59.20/59.29 inference(scs_inference,[],[1473,2])).
% 59.20/59.29 cnf(1543,plain,
% 59.20/59.29 (~P1(f6(a1,f6(a1,a1)),x15431)),
% 59.20/59.29 inference(scs_inference,[],[174,146,2,12])).
% 59.20/59.29 cnf(1552,plain,
% 59.20/59.29 (E(f6(f4(a1,a1),f6(a1,f6(a1,a1))),a1)),
% 59.20/59.29 inference(scs_inference,[],[364,229,2,61])).
% 59.20/59.29 cnf(1553,plain,
% 59.20/59.29 (E(a1,f6(f4(a1,a1),f6(a1,f6(a1,a1))))),
% 59.20/59.29 inference(scs_inference,[],[1552,2])).
% 59.20/59.29 cnf(1554,plain,
% 59.20/59.29 (~P2(f6(f4(a1,a1),f6(a1,f6(a1,a1))),a1)),
% 59.20/59.29 inference(scs_inference,[],[1552,2,43])).
% 59.20/59.29 cnf(1665,plain,
% 59.20/59.29 (E(f4(a1,f6(a1,a1)),a1)),
% 59.20/59.29 inference(scs_inference,[],[174,127,2,62])).
% 59.20/59.29 cnf(1666,plain,
% 59.20/59.29 (E(a1,f4(a1,f6(a1,a1)))),
% 59.20/59.29 inference(scs_inference,[],[1665,2])).
% 59.20/59.29 cnf(1675,plain,
% 59.20/59.29 (~P2(a1,f4(a1,f6(a1,a1)))),
% 59.20/59.29 inference(scs_inference,[],[1666,43])).
% 59.20/59.29 cnf(1892,plain,
% 59.20/59.29 (~E(a5,f6(f4(a1,a1),f6(a1,f6(a1,a1))))),
% 59.20/59.29 inference(scs_inference,[],[1554,132,25])).
% 59.20/59.29 cnf(1941,plain,
% 59.20/59.29 (P2(a5,f6(f4(a1,a1),f6(a1,f6(a1,a1))))),
% 59.20/59.29 inference(scs_inference,[],[35,129,1552,3,61])).
% 59.20/59.29 cnf(1948,plain,
% 59.20/59.29 (P2(a5,f4(a1,f6(a1,a1)))),
% 59.20/59.29 inference(scs_inference,[],[35,162,1665,1941,26,3,125])).
% 59.20/59.29 cnf(1960,plain,
% 59.20/59.29 (~E(f6(f6(a1,a5),f6(a1,a1)),a1)),
% 59.20/59.29 inference(scs_inference,[],[127,162,1948,26,62])).
% 59.20/59.29 cnf(1963,plain,
% 59.20/59.29 (P1(f6(f6(a1,a5),f6(a1,a1)),a1)),
% 59.20/59.29 inference(scs_inference,[],[127,162,1948,26,62,41])).
% 59.20/59.29 cnf(1965,plain,
% 59.20/59.29 (~P2(a1,f6(f6(a1,a5),f6(a1,a1)))),
% 59.20/59.29 inference(scs_inference,[],[127,162,1948,26,62,41,55])).
% 59.20/59.29 cnf(1967,plain,
% 59.20/59.29 (~E(f6(f6(a1,a5),f6(a1,a1)),f6(a1,f6(a1,a1)))),
% 59.20/59.29 inference(scs_inference,[],[1543,127,162,1948,26,62,41,55,12])).
% 59.20/59.29 cnf(1969,plain,
% 59.20/59.29 (~E(a1,f6(f6(a1,a5),f6(a1,a1)))),
% 59.20/59.29 inference(scs_inference,[],[1543,127,162,36,1948,26,62,41,55,12,13])).
% 59.20/59.29 cnf(1975,plain,
% 59.20/59.29 (~E(f4(a1,f6(a1,a1)),a5)),
% 59.20/59.29 inference(scs_inference,[],[123,1948,26])).
% 59.20/59.29 cnf(1977,plain,
% 59.20/59.29 (~E(f6(a5,f6(a1,a1)),a1)),
% 59.20/59.29 inference(scs_inference,[],[127,123,1948,26,62])).
% 59.20/59.29 cnf(1986,plain,
% 59.20/59.29 (~E(a1,f6(a5,f6(a1,a1)))),
% 59.20/59.29 inference(scs_inference,[],[1543,127,123,36,1948,26,62,41,55,12,13])).
% 59.20/59.29 cnf(2075,plain,
% 59.20/59.29 (~P2(f6(a1,f6(a1,a1)),f4(f6(a1,a5),f6(a1,a1)))),
% 59.20/59.29 inference(scs_inference,[],[174,818,2,25])).
% 59.20/59.29 cnf(2084,plain,
% 59.20/59.29 (E(a1,f4(f6(a1,x20841),x20841))),
% 59.20/59.29 inference(scs_inference,[],[162,2,126])).
% 59.20/59.29 cnf(2085,plain,
% 59.20/59.29 (E(f4(f6(a1,x20851),x20851),a1)),
% 59.20/59.29 inference(scs_inference,[],[2084,2])).
% 59.20/59.29 cnf(2086,plain,
% 59.20/59.29 (~P2(a1,f4(f6(a1,x20861),x20861))),
% 59.20/59.29 inference(scs_inference,[],[2084,2,43])).
% 59.20/59.29 cnf(2099,plain,
% 59.20/59.29 (~P2(f4(f6(a1,x20991),x20991),a1)),
% 59.20/59.29 inference(scs_inference,[],[2085,43])).
% 59.20/59.29 cnf(2364,plain,
% 59.20/59.29 (E(f6(f9(a5),a5),a5)),
% 59.20/59.29 inference(scs_inference,[],[148,178,1543,1666,6,7,10,11,64,9,8,97,42])).
% 59.20/59.29 cnf(2374,plain,
% 59.20/59.29 (~E(f6(f6(a1,f6(a1,a1)),f6(a1,a1)),f4(a5,a1))),
% 59.20/59.29 inference(scs_inference,[],[150,192,1053,1963,148,178,1543,1666,6,7,10,11,64,9,8,97,42,50,84,4,125,5,2])).
% 59.20/59.29 cnf(2379,plain,
% 59.20/59.29 (~P1(f4(f4(a5,a1),a5),f4(a5,a1))),
% 59.20/59.29 inference(scs_inference,[],[33,150,192,1053,1417,1963,148,178,34,1543,1666,36,6,7,10,11,64,9,8,97,42,50,84,4,125,5,2,55,49,65])).
% 59.20/59.29 cnf(2380,plain,
% 59.20/59.29 (~P1(x23801,x23801)),
% 59.20/59.29 inference(rename_variables,[],[36])).
% 59.20/59.29 cnf(2384,plain,
% 59.20/59.29 (P1(f6(a5,a5),f6(a1,a5))),
% 59.20/59.29 inference(scs_inference,[],[33,150,192,1053,1215,1417,1963,148,178,34,1543,32,1666,1553,36,6,7,10,11,64,9,8,97,42,50,84,4,125,5,2,55,49,65,25,78])).
% 59.20/59.29 cnf(2390,plain,
% 59.20/59.29 (~P1(f6(a1,a5),a5)),
% 59.20/59.29 inference(scs_inference,[],[33,150,192,2099,1053,1215,1417,1963,148,178,34,1543,32,1666,1553,1474,146,2085,36,2380,6,7,10,11,64,9,8,97,42,50,84,4,125,5,2,55,49,65,25,78,26,12,81])).
% 59.20/59.29 cnf(2395,plain,
% 59.20/59.29 (E(f6(f4(a5,a1),f6(a1,f6(a1,a1))),a5)),
% 59.20/59.29 inference(scs_inference,[],[33,150,192,2099,1053,1215,1006,1417,1963,148,178,34,421,1543,32,1666,1553,1474,146,2085,363,36,2380,6,7,10,11,64,9,8,97,42,50,84,4,125,5,2,55,49,65,25,78,26,12,81,45,61])).
% 59.20/59.29 cnf(2401,plain,
% 59.20/59.29 (~E(f4(f6(a1,x24011),x24011),a5)),
% 59.20/59.29 inference(scs_inference,[],[33,150,192,194,2099,1053,1215,1006,1417,1963,148,178,34,421,1543,32,1666,1553,1474,2084,146,2085,363,129,36,2380,6,7,10,11,64,9,8,97,42,50,84,4,125,5,2,55,49,65,25,78,26,12,81,45,61,62,3])).
% 59.20/59.29 cnf(2408,plain,
% 59.20/59.29 (P1(a5,f4(a5,a5))),
% 59.20/59.29 inference(scs_inference,[],[152,64])).
% 59.20/59.29 cnf(2410,plain,
% 59.20/59.29 (~P1(f6(f6(a1,a5),a5),f6(a5,a5))),
% 59.20/59.30 inference(scs_inference,[],[2390,152,64,97])).
% 59.20/59.30 cnf(2414,plain,
% 59.20/59.30 (E(f6(f9(f6(x24141,a5)),a5),f6(x24141,a5))),
% 59.20/59.30 inference(scs_inference,[],[2390,2364,35,152,64,97,9,11,42])).
% 59.20/59.30 cnf(2417,plain,
% 59.20/59.30 (E(f4(f6(f9(a5),a5),x24171),f4(a5,x24171))),
% 59.20/59.30 inference(scs_inference,[],[2390,2364,35,152,64,97,9,11,42,10,8])).
% 59.20/59.30 cnf(2419,plain,
% 59.20/59.30 (~E(f6(a5,a5),f6(f6(a1,a1),a5))),
% 59.20/59.30 inference(scs_inference,[],[187,2390,2364,35,152,64,97,9,11,42,10,8,7,50])).
% 59.20/59.30 cnf(2423,plain,
% 59.20/59.30 (E(f6(f6(f9(a5),a5),x24231),f6(a5,x24231))),
% 59.20/59.30 inference(scs_inference,[],[187,2384,2390,2364,35,152,64,97,9,11,42,10,8,7,50,84,4])).
% 59.20/59.30 cnf(2425,plain,
% 59.20/59.30 (E(f6(f4(a5,a1),a1),a5)),
% 59.20/59.30 inference(scs_inference,[],[187,2384,2390,2364,164,35,152,64,97,9,11,42,10,8,7,50,84,4,6,125])).
% 59.20/59.30 cnf(2427,plain,
% 59.20/59.30 (E(f6(x24271,f6(f9(a5),a5)),f6(x24271,a5))),
% 59.20/59.30 inference(scs_inference,[],[187,2384,2390,2364,164,35,152,64,97,9,11,42,10,8,7,50,84,4,6,125,5])).
% 59.20/59.30 cnf(2428,plain,
% 59.20/59.30 (~E(a5,f4(f6(a1,x24281),x24281))),
% 59.20/59.30 inference(scs_inference,[],[187,2384,2390,2401,2364,164,35,152,64,97,9,11,42,10,8,7,50,84,4,6,125,5,2])).
% 59.20/59.30 cnf(2429,plain,
% 59.20/59.30 (~P1(f4(a1,f6(a1,a1)),a5)),
% 59.20/59.30 inference(scs_inference,[],[187,2384,2390,2401,2364,1948,164,35,152,64,97,9,11,42,10,8,7,50,84,4,6,125,5,2,55])).
% 59.20/59.30 cnf(2431,plain,
% 59.20/59.30 (~P1(f6(a1,a5),f6(a5,a5))),
% 59.20/59.30 inference(scs_inference,[],[187,2384,2390,2401,2364,1948,164,35,152,36,64,97,9,11,42,10,8,7,50,84,4,6,125,5,2,55,65])).
% 59.20/59.30 cnf(2437,plain,
% 59.20/59.30 (E(f6(a1,x24371),x24371)),
% 59.20/59.30 inference(rename_variables,[],[31])).
% 59.20/59.30 cnf(2440,plain,
% 59.20/59.30 (~P1(f6(a1,a5),f6(f6(a1,a5),f6(a1,a1)))),
% 59.20/59.30 inference(scs_inference,[],[187,2384,2390,2379,1965,1969,2401,2364,2075,1948,164,35,152,146,991,36,31,2437,64,97,9,11,42,10,8,7,50,84,4,6,125,5,2,55,65,25,26,12,81])).
% 59.20/59.30 cnf(2446,plain,
% 59.20/59.30 (~P1(f6(a1,a5),f6(f9(a5),a5))),
% 59.20/59.30 inference(scs_inference,[],[187,2384,2390,2379,1965,1969,2401,2364,2075,1967,1948,164,35,152,1543,146,991,36,31,2437,64,97,9,11,42,10,8,7,50,84,4,6,125,5,2,55,65,25,26,12,81,45,13])).
% 59.20/59.30 cnf(2447,plain,
% 59.20/59.30 (E(f6(f4(a1,a1),a1),f6(a1,f6(a1,a1)))),
% 59.20/59.30 inference(scs_inference,[],[187,2384,2390,2379,1965,1969,2401,2364,2075,1967,194,1948,164,35,152,1543,146,1335,991,36,31,2437,64,97,9,11,42,10,8,7,50,84,4,6,125,5,2,55,65,25,26,12,81,45,13,61])).
% 59.20/59.30 cnf(2450,plain,
% 59.20/59.30 (E(f4(a5,a5),f9(a5))),
% 59.20/59.30 inference(scs_inference,[],[187,2384,2390,2379,1965,1969,2401,2364,2075,1967,194,1948,164,35,152,1543,146,1335,123,991,36,31,2437,64,97,9,11,42,10,8,7,50,84,4,6,125,5,2,55,65,25,26,12,81,45,13,61,62])).
% 59.20/59.30 cnf(2462,plain,
% 59.20/59.30 (P1(f6(x24621,a5),f4(f6(x24621,a5),a5))),
% 59.20/59.30 inference(scs_inference,[],[2431,176,32,42,97,64])).
% 59.20/59.30 cnf(2466,plain,
% 59.20/59.30 (E(f4(x24661,f4(a5,a5)),f4(x24661,f9(a5)))),
% 59.20/59.30 inference(scs_inference,[],[2431,2450,176,32,42,97,64,11,10,9])).
% 59.20/59.30 cnf(2469,plain,
% 59.20/59.30 (E(f4(f4(a5,a5),x24691),f4(f9(a5),x24691))),
% 59.20/59.30 inference(scs_inference,[],[2431,2450,1986,176,32,42,97,64,11,10,9,50,8])).
% 59.20/59.30 cnf(2470,plain,
% 59.20/59.30 (P1(f6(a5,a5),f6(f4(a5,a5),a5))),
% 59.20/59.30 inference(scs_inference,[],[2431,2450,2408,1986,176,32,42,97,64,11,10,9,50,8,84])).
% 59.20/59.30 cnf(2475,plain,
% 59.20/59.30 (E(f6(f4(x24751,f6(a1,x24751)),f6(a1,x24751)),x24751)),
% 59.20/59.30 inference(scs_inference,[],[2431,2450,2408,1986,127,176,32,42,97,64,11,10,9,50,8,84,7,6,4,125])).
% 59.20/59.30 cnf(2477,plain,
% 59.20/59.30 (E(f6(x24771,f4(a5,a5)),f6(x24771,f9(a5)))),
% 59.20/59.30 inference(scs_inference,[],[2431,2450,2408,1986,127,176,32,42,97,64,11,10,9,50,8,84,7,6,4,125,5])).
% 59.20/59.30 cnf(2478,plain,
% 59.20/59.30 (~E(f6(f6(a1,a1),a5),f6(a5,a5))),
% 59.20/59.30 inference(scs_inference,[],[2431,2450,2408,1986,2419,127,176,32,42,97,64,11,10,9,50,8,84,7,6,4,125,5,2])).
% 59.20/59.30 cnf(2479,plain,
% 59.20/59.30 (~P1(f6(f4(a1,a1),f6(a1,f6(a1,a1))),a5)),
% 59.20/59.30 inference(scs_inference,[],[2431,2450,2408,1986,2419,1941,127,176,32,42,97,64,11,10,9,50,8,84,7,6,4,125,5,2,55])).
% 59.20/59.30 cnf(2481,plain,
% 59.20/59.30 (~P1(f4(a5,a5),a5)),
% 59.20/59.30 inference(scs_inference,[],[2431,2450,2408,1986,2419,1941,127,176,32,36,42,97,64,11,10,9,50,8,84,7,6,4,125,5,2,55,65])).
% 59.20/59.30 cnf(2482,plain,
% 59.20/59.30 (~P1(x24821,x24821)),
% 59.20/59.30 inference(rename_variables,[],[36])).
% 59.20/59.30 cnf(2484,plain,
% 59.20/59.30 (~P2(f4(a5,a5),f9(a5))),
% 59.20/59.30 inference(scs_inference,[],[2431,2450,2408,1986,2419,1941,127,176,32,123,36,42,97,64,11,10,9,50,8,84,7,6,4,125,5,2,55,65,25])).
% 59.20/59.30 cnf(2486,plain,
% 59.20/59.30 (P1(f6(f6(a5,f6(a1,a1)),a5),f6(a1,a5))),
% 59.20/59.30 inference(scs_inference,[],[2431,2450,2408,1986,2419,1941,127,176,32,123,36,42,97,64,11,10,9,50,8,84,7,6,4,125,5,2,55,65,25,78])).
% 59.20/59.30 cnf(2489,plain,
% 59.20/59.30 (~P2(f6(a1,f9(a5)),f4(a5,a5))),
% 59.20/59.30 inference(scs_inference,[],[2431,2450,2408,1986,2419,1941,127,176,32,123,36,42,97,64,11,10,9,50,8,84,7,6,4,125,5,2,55,65,25,78,26])).
% 59.20/59.30 cnf(2490,plain,
% 59.20/59.30 (~P2(f6(a1,x24901),x24901)),
% 59.20/59.30 inference(rename_variables,[],[127])).
% 59.20/59.30 cnf(2491,plain,
% 59.20/59.30 (~P1(f4(a5,a5),f9(a5))),
% 59.20/59.30 inference(scs_inference,[],[2431,2450,2408,1986,2419,1941,127,176,32,123,36,2482,42,97,64,11,10,9,50,8,84,7,6,4,125,5,2,55,65,25,78,26,12])).
% 59.20/59.30 cnf(2496,plain,
% 59.20/59.30 (P1(a5,f4(a1,f6(a1,a1)))),
% 59.20/59.30 inference(scs_inference,[],[2431,2450,2408,1986,2419,2429,1975,1941,127,176,32,146,123,36,2482,42,97,64,11,10,9,50,8,84,7,6,4,125,5,2,55,65,25,78,26,12,81,45])).
% 59.20/59.30 cnf(2500,plain,
% 59.20/59.30 (E(f6(f4(a5,a1),a1),f6(f9(a5),a5))),
% 59.20/59.30 inference(scs_inference,[],[2431,2450,2408,1986,2419,2429,2417,2423,1975,1941,127,176,32,130,146,123,36,2482,42,97,64,11,10,9,50,8,84,7,6,4,125,5,2,55,65,25,78,26,12,81,45,13,61])).
% 59.20/59.30 cnf(2504,plain,
% 59.20/59.30 (E(f4(f6(a1,a1),f6(a1,f6(a1,a1))),a1)),
% 59.20/59.30 inference(scs_inference,[],[2431,2450,2408,1986,2419,2429,2417,2423,1975,1941,127,2490,176,32,1213,130,146,123,36,2482,42,97,64,11,10,9,50,8,84,7,6,4,125,5,2,55,65,25,78,26,12,81,45,13,61,62])).
% 59.20/59.30 cnf(2508,plain,
% 59.20/59.30 (~E(f9(a5),f6(f6(a1,f6(a1,a1)),f6(a1,a5)))),
% 59.20/59.30 inference(scs_inference,[],[2431,2450,2408,1986,2419,2429,1394,2417,2423,1975,1941,127,2490,176,32,1213,130,146,123,36,2482,42,97,64,11,10,9,50,8,84,7,6,4,125,5,2,55,65,25,78,26,12,81,45,13,61,62,3])).
% 59.20/59.30 cnf(2533,plain,
% 59.20/59.30 (E(f6(f4(f9(a5),f4(a5,a5)),f4(a5,a5)),f9(a5))),
% 59.20/59.30 inference(scs_inference,[],[2484,2491,2496,2428,2425,97,50,9,11,84,10,8,7,4,6,125])).
% 59.20/59.30 cnf(2537,plain,
% 59.20/59.30 (~P1(f6(f6(a1,f6(a1,a1)),f6(a1,a1)),a5)),
% 59.20/59.30 inference(scs_inference,[],[2484,2491,2496,2428,1301,2425,1464,97,50,9,11,84,10,8,7,4,6,125,5,2,55])).
% 59.20/59.30 cnf(2543,plain,
% 59.20/59.30 (E(f6(f4(x25431,f6(a1,x25431)),f6(a1,x25431)),x25431)),
% 59.20/59.30 inference(rename_variables,[],[2475])).
% 59.20/59.30 cnf(2545,plain,
% 59.20/59.30 (E(f6(f4(x25451,f6(a1,x25451)),f6(a1,x25451)),x25451)),
% 59.20/59.30 inference(rename_variables,[],[2475])).
% 59.20/59.30 cnf(2546,plain,
% 59.20/59.30 (~P1(f6(f4(a1,a1),a1),x25461)),
% 59.20/59.30 inference(scs_inference,[],[2484,2491,2410,374,2462,2496,2428,1301,2447,2475,2543,229,2425,1464,1543,97,50,9,11,84,10,8,7,4,6,125,5,2,55,65,25,26,12])).
% 59.20/59.30 cnf(2547,plain,
% 59.20/59.30 (~P1(f6(f4(a5,a5),a5),a5)),
% 59.20/59.30 inference(scs_inference,[],[2484,2491,2481,2410,374,2462,2496,2428,1301,2447,2475,2543,229,2425,1272,1464,1543,97,50,9,11,84,10,8,7,4,6,125,5,2,55,65,25,26,12,81])).
% 59.20/59.30 cnf(2552,plain,
% 59.20/59.30 (E(f6(f4(x25521,f6(a1,x25521)),f6(a1,x25521)),x25521)),
% 59.20/59.30 inference(rename_variables,[],[2475])).
% 59.20/59.30 cnf(2555,plain,
% 59.20/59.30 (~P1(f6(a1,a5),f6(f4(a5,a1),a1))),
% 59.20/59.30 inference(scs_inference,[],[33,2484,2491,2481,2410,374,2446,2462,2496,2428,1301,2447,2475,2543,2545,2552,2500,2479,229,2425,1892,1272,1464,34,1543,97,50,9,11,84,10,8,7,4,6,125,5,2,55,65,25,26,12,81,45,14,15,13])).
% 59.20/59.30 cnf(2563,plain,
% 59.20/59.30 (~E(f6(a1,f6(f6(a1,a1),a5)),f6(a5,a5))),
% 59.20/59.30 inference(scs_inference,[],[33,2484,2491,2481,2410,2478,374,2446,2462,2496,2428,1301,2447,2475,2543,2545,2552,2500,2466,2414,2479,229,2425,1892,1272,1464,34,1543,162,129,97,50,9,11,84,10,8,7,4,6,125,5,2,55,65,25,26,12,81,45,14,15,13,61,62,3])).
% 59.20/59.30 cnf(2565,plain,
% 59.20/59.30 (E(f6(f4(a1,a1),a1),a1)),
% 59.20/59.30 inference(scs_inference,[],[33,2484,2491,2481,2410,2478,374,2446,2462,2496,2428,1301,2447,2475,2543,2545,2552,2500,2466,2414,2479,229,2425,1892,1272,1464,34,1543,162,129,97,50,9,11,84,10,8,7,4,6,125,5,2,55,65,25,26,12,81,45,14,15,13,61,62,3,41])).
% 59.20/59.30 cnf(2573,plain,
% 59.20/59.30 (~E(f6(f6(f6(a1,a5),f6(a1,a1)),a5),f6(a1,a5))),
% 59.20/59.30 inference(scs_inference,[],[1960,985,84,50])).
% 59.20/59.30 cnf(2581,plain,
% 59.20/59.30 (E(f6(f6(f4(a1,a1),a1),x25811),f6(a1,x25811))),
% 59.20/59.30 inference(scs_inference,[],[2546,2565,1960,985,84,50,11,9,10,97,8,4])).
% 59.20/59.30 cnf(2586,plain,
% 59.20/59.30 (E(f6(x25861,f6(f4(a1,a1),a1)),f6(x25861,a1))),
% 59.20/59.30 inference(scs_inference,[],[2546,2565,1960,985,130,84,50,11,9,10,97,8,4,7,6,125,5])).
% 59.20/59.30 cnf(2588,plain,
% 59.20/59.30 (~P1(f6(a1,f6(a1,f6(a1,a1))),a5)),
% 59.20/59.30 inference(scs_inference,[],[2546,2565,2508,1960,985,218,130,84,50,11,9,10,97,8,4,7,6,125,5,2,55])).
% 59.20/59.30 cnf(2590,plain,
% 59.20/59.30 (~P1(f6(f4(a5,a5),a5),f6(a5,a5))),
% 59.20/59.30 inference(scs_inference,[],[2546,2470,2565,2508,1960,985,218,130,36,84,50,11,9,10,97,8,4,7,6,125,5,2,55,65])).
% 59.20/59.30 cnf(2591,plain,
% 59.20/59.30 (~P1(x25911,x25911)),
% 59.20/59.30 inference(rename_variables,[],[36])).
% 59.20/59.30 cnf(2593,plain,
% 59.20/59.30 (~P2(f6(f4(a1,a1),a1),f4(a5,f6(a1,a1)))),
% 59.20/59.30 inference(scs_inference,[],[716,2546,2470,2565,2508,1960,985,218,130,36,84,50,11,9,10,97,8,4,7,6,125,5,2,55,65,25])).
% 59.20/59.30 cnf(2602,plain,
% 59.20/59.30 (E(f6(f4(f9(a5),f4(a5,a5)),f4(a5,a5)),f4(a5,a5))),
% 59.20/59.30 inference(scs_inference,[],[716,2546,2470,2565,2533,886,824,2469,2508,2537,1960,985,2484,218,130,146,123,36,2591,84,50,11,9,10,97,8,4,7,6,125,5,2,55,65,25,26,12,81,45,61])).
% 59.20/59.30 cnf(2632,plain,
% 59.20/59.30 (~P1(f6(a1,a1),a5)),
% 59.20/59.30 inference(scs_inference,[],[2547,2563,1977,367,161,2084,162,1665,97,50,9,84,11,10,8,7,4,6,125,5,2,55])).
% 59.20/59.30 cnf(2647,plain,
% 59.20/59.30 (E(f4(f6(a1,x26471),x26471),f6(f4(a1,a1),a1))),
% 59.20/59.30 inference(scs_inference,[],[2590,2489,2555,2547,2602,2563,2581,2586,2427,280,2504,2588,1977,367,192,2429,2462,1975,161,2084,162,1665,97,50,9,84,11,10,8,7,4,6,125,5,2,55,65,25,26,12,81,45,13,62])).
% 59.20/59.30 cnf(2650,plain,
% 59.20/59.30 (~E(f6(a1,f6(a1,a1)),f4(a5,a1))),
% 59.20/59.30 inference(scs_inference,[],[2590,2489,2555,2547,2374,2602,2563,2581,2586,2427,280,2504,2588,1977,367,192,2429,2462,1975,161,2084,162,1665,991,97,50,9,84,11,10,8,7,4,6,125,5,2,55,65,25,26,12,81,45,13,62,3])).
% 59.20/59.30 cnf(2657,plain,
% 59.20/59.30 (~P1(f6(f6(a1,a1),a5),f6(a5,a5))),
% 59.20/59.30 inference(scs_inference,[],[2632,322,84,97])).
% 59.20/59.30 cnf(2659,plain,
% 59.20/59.30 (~E(f6(f6(a5,a5),a5),f6(a5,a5))),
% 59.20/59.30 inference(scs_inference,[],[2632,1270,322,84,97,50])).
% 59.20/59.30 cnf(2661,plain,
% 59.20/59.30 (E(f4(x26611,f4(f6(a1,x26612),x26612)),f4(x26611,a1))),
% 59.20/59.30 inference(scs_inference,[],[2632,1270,322,2085,84,97,50,9])).
% 59.20/59.30 cnf(2664,plain,
% 59.20/59.30 (E(f6(f4(f6(a1,x26641),x26641),x26642),f6(a1,x26642))),
% 59.20/59.30 inference(scs_inference,[],[2632,1270,322,2085,84,97,50,9,10,11,4])).
% 59.20/59.30 cnf(2667,plain,
% 59.20/59.30 (E(f6(f4(x26671,x26671),x26671),x26671)),
% 59.20/59.30 inference(scs_inference,[],[2632,1270,322,2085,123,84,97,50,9,10,11,4,7,8,125])).
% 59.20/59.30 cnf(2681,plain,
% 59.20/59.30 (~P1(f4(f6(a1,x26811),x26811),x26812)),
% 59.20/59.30 inference(scs_inference,[],[2632,2593,2647,2477,2486,2573,1270,2419,1004,2546,322,2085,123,129,36,84,97,50,9,10,11,4,7,8,125,5,6,2,65,78,25,26,12])).
% 59.20/59.30 cnf(2683,plain,
% 59.20/59.30 (~P1(f6(a1,f6(a1,a1)),x26831)),
% 59.20/59.30 inference(rename_variables,[],[1543])).
% 59.20/59.30 cnf(2699,plain,
% 59.20/59.30 (P12(f6(a7,a5))),
% 59.20/59.30 inference(scs_inference,[],[33,2632,2650,2086,2593,2647,2477,2486,2573,1324,2395,1270,2419,1004,2546,322,34,1543,2683,2085,123,162,991,129,36,84,97,50,9,10,11,4,7,8,125,5,6,2,65,78,25,26,12,81,45,61,13,62,3,52,154,44])).
% 59.20/59.30 cnf(2701,plain,
% 59.20/59.30 (~P12(a7)),
% 59.20/59.30 inference(scs_inference,[],[2699,51])).
% 59.20/59.30 cnf(2724,plain,
% 59.20/59.30 (E(f6(f4(x27241,x27241),x27241),x27241)),
% 59.20/59.30 inference(rename_variables,[],[2667])).
% 59.20/59.30 cnf(2726,plain,
% 59.20/59.30 (E(f6(f4(x27261,x27261),x27261),x27261)),
% 59.20/59.30 inference(rename_variables,[],[2667])).
% 59.20/59.30 cnf(2728,plain,
% 59.20/59.30 (E(f6(f4(x27281,x27281),x27281),x27281)),
% 59.20/59.30 inference(rename_variables,[],[2667])).
% 59.20/59.30 cnf(2744,plain,
% 59.20/59.30 (P12(a7)),
% 59.20/59.30 inference(scs_inference,[],[33,2699,2657,2659,1675,2440,2667,2724,2726,2728,2681,2661,2664,1297,2478,2489,2099,2419,2462,178,34,162,129,1043,1039,183,50,84,97,9,11,10,8,4,7,6,5,2,65,25,26,12,81,45,61,13,62,3,63])).
% 59.20/59.30 cnf(2755,plain,
% 59.20/59.30 ($false),
% 59.20/59.30 inference(scs_inference,[],[2701,2744]),
% 59.20/59.30 ['proof']).
% 59.20/59.30 % SZS output end Proof
% 59.20/59.30 % Total time :58.630000s
%------------------------------------------------------------------------------