%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT092+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n001.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 : Tue Sep 8 06:04:24 AM UTC 2026
% Result : Theorem 58.93s 59.04s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT092+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% 0.00/0.03 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.09/0.35 % Computer : n001.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 7 14:29:37 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.25/0.52 start to proof:theBenchmark
% 58.93/59.03 %-------------------------------------------
% 58.93/59.03 % File :CSE---1.7
% 58.93/59.03 % Problem :theBenchmark
% 58.93/59.03 % Transform :cnf
% 58.93/59.03 % Format :tptp:raw
% 58.93/59.03 % Command :java -jar mcs_scs.jar %d %s
% 58.93/59.03
% 58.93/59.03 % Result :Theorem 58.493068s
% 58.93/59.03 % Output :CNFRefutation 58.493068s
% 58.93/59.03 %-------------------------------------------
% 58.93/59.03 %--------------------------------------------------------------------------
% 58.93/59.03 % File : MGT092+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% 58.93/59.03 % Domain : Management
% 58.93/59.03 % Problem : U<V in domain implies conflict completion exists
% 58.93/59.03 % Version : Especial.
% 58.93/59.03 % English : unknown-sound sharpness_conflict:
% 58.93/59.03 % leq(v0,v400) & less(v400,v800) & leq(v800,v1200)
% 58.93/59.03 % => completion_conflict(v400, v800, v0, v1200).
% 58.93/59.03
% 58.93/59.03 % Refs : [MC+26] Mustafa et al. (2026), Axis Decomposition for ODRL
% 58.93/59.03 % Source : [MC+26]
% 58.93/59.03 % Names : ODRL633-1.p [MC+26]
% 58.93/59.03
% 58.93/59.03 % Status : Theorem
% 58.93/59.03 % Rating : ? v9.3.1
% 58.93/59.03 % Syntax : Number of formulae : 42 ( 15 unt; 0 def)
% 58.93/59.03 % Number of atoms : 116 ( 29 equ)
% 58.93/59.03 % Maximal formula atoms : 7 ( 2 avg)
% 58.93/59.03 % Number of connectives : 87 ( 13 ~; 9 |; 38 &)
% 58.93/59.03 % ( 8 <=>; 19 =>; 0 <=; 0 <~>)
% 58.93/59.03 % Maximal formula depth : 10 ( 5 avg)
% 58.93/59.03 % Maximal term depth : 2 ( 1 avg)
% 58.93/59.03 % Number of predicates : 14 ( 13 usr; 0 prp; 1-4 aty)
% 58.93/59.03 % Number of functors : 8 ( 8 usr; 7 con; 0-2 aty)
% 58.93/59.03 % Number of variables : 83 ( 81 !; 2 ?)
% 58.93/59.03 % SPC : FOF_THM_RFO_SEQ
% 58.93/59.03
% 58.93/59.03 % Comments : Requires MGT002+0.ax + MGT002+2.ax.
% 58.93/59.03 % Bugfixes : v9.3.1 - $distinct expanded to inequalities.
% 58.93/59.03 %--------------------------------------------------------------------------
% 58.93/59.04 include('Axioms/MGT002+0.ax').
% 58.93/59.04 include('Axioms/MGT002+4.ax').
% 58.93/59.04 include('Axioms/MGT002+2.ax').
% 58.93/59.04 %--------------------------------------------------------------------------
% 58.93/59.04 %----Named constants and ordering
% 58.93/59.04 fof(val_v0,axiom,
% 58.93/59.04 val(v0) ).
% 58.93/59.04
% 58.93/59.04 fof(val_v400,axiom,
% 58.93/59.04 val(v400) ).
% 58.93/59.04
% 58.93/59.04 fof(val_v800,axiom,
% 58.93/59.04 val(v800) ).
% 58.93/59.04
% 58.93/59.04 fof(val_v1200,axiom,
% 58.93/59.04 val(v1200) ).
% 58.93/59.04
% 58.93/59.04 fof(ord_v0_v400,axiom,
% 58.93/59.04 less(v0,v400) ).
% 58.93/59.04
% 58.93/59.04 fof(ord_v400_v800,axiom,
% 58.93/59.04 less(v400,v800) ).
% 58.93/59.04
% 58.93/59.04 fof(ord_v800_v1200,axiom,
% 58.93/59.04 less(v800,v1200) ).
% 58.93/59.04
% 58.93/59.04 fof(distinct,axiom,
% 58.93/59.04 ( v0 != v400
% 58.93/59.04 & v0 != v800
% 58.93/59.04 & v0 != v1200
% 58.93/59.04 & v400 != v800
% 58.93/59.04 & v400 != v1200
% 58.93/59.04 & v800 != v1200 ) ).
% 58.93/59.04
% 58.93/59.04 fof(odrl633,conjecture,
% 58.93/59.04 completion_conflict(v400,v800,v0,v1200) ).
% 58.93/59.04
% 58.93/59.04 %--------------------------------------------------------------------------
% 58.93/59.04 %-------------------------------------------
% 58.93/59.04 % Proof found
% 58.93/59.04 % SZS status Theorem for theBenchmark
% 58.93/59.04 % SZS output start Proof
% 58.93/59.04 %ClaNum:119(EqnAxiom:54)
% 58.93/59.04 %VarNum:283(SingletonVarNum:124)
% 58.93/59.04 %MaxLitNum:6
% 58.93/59.04 %MaxfuncDepth:1
% 58.93/59.04 %SharedTerms:27
% 58.93/59.04 %goalClause: 75
% 58.93/59.04 %singleGoalClaCount:1
% 58.93/59.04 [55]P1(a1)
% 58.93/59.04 [56]P1(a2)
% 58.93/59.04 [57]P1(a4)
% 58.93/59.04 [58]P11(a8)
% 58.93/59.04 [59]P11(a9)
% 58.93/59.04 [60]P11(a11)
% 58.93/59.04 [61]P11(a10)
% 58.93/59.04 [62]P12(a8,a9)
% 58.93/59.04 [63]P12(a9,a11)
% 58.93/59.04 [64]P12(a11,a10)
% 58.93/59.04 [65]~E(a1,a2)
% 58.93/59.04 [66]~E(a1,a4)
% 58.93/59.04 [67]~E(a4,a2)
% 58.93/59.04 [68]~E(a9,a8)
% 58.93/59.04 [69]~E(a11,a8)
% 58.93/59.04 [70]~E(a11,a9)
% 58.93/59.04 [71]~E(a10,a8)
% 58.93/59.04 [72]~E(a10,a9)
% 58.93/59.04 [73]~E(a10,a11)
% 58.93/59.04 [75]~P2(a9,a11,a8,a10)
% 58.93/59.04 [74]~P12(x741,x741)
% 58.93/59.04 [77]~E(x771,x772)+P13(x771,x772)
% 58.93/59.04 [85]~P12(x851,x852)+P13(x851,x852)
% 58.93/59.04 [98]P12(x981,x982)+~P8(x982,x981,x983)
% 58.93/59.04 [99]P12(x991,x992)+~P9(x991,x993,x992)
% 58.93/59.04 [100]P12(x1001,x1002)+~P10(x1002,x1001,x1003)
% 58.93/59.04 [101]P12(x1011,x1012)+~P10(x1011,x1013,x1012)
% 58.93/59.04 [102]P13(x1021,x1022)+~P7(x1022,x1021,x1023)
% 58.93/59.04 [103]P13(x1031,x1032)+~P7(x1031,x1033,x1032)
% 58.93/59.04 [104]P13(x1041,x1042)+~P8(x1041,x1043,x1042)
% 58.93/59.04 [105]P13(x1051,x1052)+~P9(x1052,x1051,x1053)
% 58.93/59.04 [113]P5(x1131,x1132,x1133,x1134)+P7(f5(x1131,x1132,x1133,x1134),x1131,x1132)
% 58.93/59.04 [114]P6(x1141,x1142,x1143,x1144)+P7(f6(x1141,x1142,x1143,x1144),x1143,x1144)
% 58.93/59.04 [115]P6(x1151,x1152,x1153,x1154)+P7(f6(x1151,x1152,x1153,x1154),x1151,x1152)
% 58.93/59.04 [116]~P4(x1161,x1162,x1163,x1164)+P7(f7(x1161,x1162,x1163,x1164),x1163,x1164)
% 58.93/59.04 [117]~P4(x1171,x1172,x1173,x1174)+P7(f7(x1171,x1172,x1173,x1174),x1171,x1172)
% 58.93/59.04 [119]P5(x1191,x1192,x1193,x1194)+~P7(f5(x1191,x1192,x1193,x1194),x1193,x1194)
% 58.93/59.04 [78]P12(x782,x781)+P12(x781,x782)+E(x781,x782)
% 58.93/59.04 [86]P12(x861,x862)+~P13(x861,x862)+E(x861,x862)
% 58.93/59.04 [87]~P13(x872,x871)+~P13(x871,x872)+E(x871,x872)
% 58.93/59.04 [89]~P12(x891,x893)+P12(x891,x892)+~P12(x893,x892)
% 58.93/59.04 [90]~P13(x901,x903)+P12(x901,x902)+~P12(x903,x902)
% 58.93/59.04 [91]~P13(x913,x912)+P12(x911,x912)+~P12(x911,x913)
% 58.93/59.04 [92]~P13(x921,x923)+P13(x921,x922)+~P13(x923,x922)
% 58.93/59.04 [93]~P13(x931,x933)+~P13(x932,x931)+P3(x931,x932,x933)
% 58.93/59.04 [94]~P13(x941,x943)+~P13(x942,x941)+P7(x941,x942,x943)
% 58.93/59.04 [95]~P12(x952,x951)+~P13(x951,x953)+P8(x951,x952,x953)
% 58.93/59.04 [96]~P12(x961,x963)+~P13(x962,x961)+P9(x961,x962,x963)
% 58.93/59.04 [97]~P12(x971,x973)+~P12(x972,x971)+P10(x971,x972,x973)
% 58.93/59.04 [109]~P7(x1095,x1091,x1092)+P4(x1091,x1092,x1093,x1094)+~P7(x1095,x1093,x1094)
% 58.93/59.04 [111]~P5(x1114,x1115,x1112,x1113)+P7(x1111,x1112,x1113)+~P7(x1111,x1114,x1115)
% 58.93/59.04 [112]~P6(x1124,x1125,x1122,x1123)+~P7(x1121,x1122,x1123)+~P7(x1121,x1124,x1125)
% 58.93/59.04 [118]~P6(x1185,x1186,x1183,x1184)+P6(x1181,x1182,x1183,x1184)+~P5(x1181,x1182,x1185,x1186)
% 58.93/59.04 [76]~P1(x761)+E(x761,a2)+E(x761,a4)+E(x761,a1)
% 58.93/59.04 [79]~P1(x791)+~P1(x792)+~E(x792,a1)+E(f3(x791,x792),a1)
% 58.93/59.04 [80]~P1(x802)+~P1(x801)+~E(x801,a1)+E(f3(x801,x802),a1)
% 58.93/59.04 [81]~P1(x812)+~P1(x811)+~E(x812,a2)+~E(x811,a2)+E(f3(x811,x812),a2)
% 58.93/59.04 [88]~P1(x882)+~P1(x881)+E(f3(x881,x882),a1)+E(f3(x881,x882),a2)+E(f3(x881,x882),a4)
% 58.93/59.04 [107]~P12(x1071,x1072)+~P13(x1072,x1074)+~P13(x1071,x1074)+~P13(x1073,x1071)+P2(x1071,x1072,x1073,x1074)
% 58.93/59.04 [82]~P1(x821)+~P1(x822)+~E(x822,a4)+E(x821,a1)+E(x822,a1)+E(f3(x821,x822),a4)
% 58.93/59.04 [83]~P1(x831)+~P1(x832)+~E(x832,a4)+E(x831,a1)+E(x832,a1)+E(f3(x832,x831),a4)
% 58.93/59.04 %EqnAxiom
% 58.93/59.04 [1]E(x11,x11)
% 58.93/59.04 [2]E(x22,x21)+~E(x21,x22)
% 58.93/59.04 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.93/59.04 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43))
% 58.93/59.04 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52))
% 58.93/59.04 [6]~E(x61,x62)+E(f5(x61,x63,x64,x65),f5(x62,x63,x64,x65))
% 58.93/59.04 [7]~E(x71,x72)+E(f5(x73,x71,x74,x75),f5(x73,x72,x74,x75))
% 58.93/59.04 [8]~E(x81,x82)+E(f5(x83,x84,x81,x85),f5(x83,x84,x82,x85))
% 58.93/59.04 [9]~E(x91,x92)+E(f5(x93,x94,x95,x91),f5(x93,x94,x95,x92))
% 58.93/59.04 [10]~E(x101,x102)+E(f7(x101,x103,x104,x105),f7(x102,x103,x104,x105))
% 58.93/59.04 [11]~E(x111,x112)+E(f7(x113,x111,x114,x115),f7(x113,x112,x114,x115))
% 58.93/59.04 [12]~E(x121,x122)+E(f7(x123,x124,x121,x125),f7(x123,x124,x122,x125))
% 58.93/59.04 [13]~E(x131,x132)+E(f7(x133,x134,x135,x131),f7(x133,x134,x135,x132))
% 58.93/59.04 [14]~E(x141,x142)+E(f6(x141,x143,x144,x145),f6(x142,x143,x144,x145))
% 58.93/59.04 [15]~E(x151,x152)+E(f6(x153,x151,x154,x155),f6(x153,x152,x154,x155))
% 58.93/59.04 [16]~E(x161,x162)+E(f6(x163,x164,x161,x165),f6(x163,x164,x162,x165))
% 58.93/59.04 [17]~E(x171,x172)+E(f6(x173,x174,x175,x171),f6(x173,x174,x175,x172))
% 58.93/59.04 [18]~P1(x181)+P1(x182)+~E(x181,x182)
% 58.93/59.04 [19]P7(x192,x193,x194)+~E(x191,x192)+~P7(x191,x193,x194)
% 58.93/59.04 [20]P7(x203,x202,x204)+~E(x201,x202)+~P7(x203,x201,x204)
% 58.93/59.04 [21]P7(x213,x214,x212)+~E(x211,x212)+~P7(x213,x214,x211)
% 58.93/59.04 [22]P5(x222,x223,x224,x225)+~E(x221,x222)+~P5(x221,x223,x224,x225)
% 58.93/59.04 [23]P5(x233,x232,x234,x235)+~E(x231,x232)+~P5(x233,x231,x234,x235)
% 58.93/59.04 [24]P5(x243,x244,x242,x245)+~E(x241,x242)+~P5(x243,x244,x241,x245)
% 58.93/59.04 [25]P5(x253,x254,x255,x252)+~E(x251,x252)+~P5(x253,x254,x255,x251)
% 58.93/59.04 [26]~P11(x261)+P11(x262)+~E(x261,x262)
% 58.93/59.04 [27]P13(x272,x273)+~E(x271,x272)+~P13(x271,x273)
% 58.93/59.04 [28]P13(x283,x282)+~E(x281,x282)+~P13(x283,x281)
% 58.93/59.04 [29]P12(x292,x293)+~E(x291,x292)+~P12(x291,x293)
% 58.93/59.04 [30]P12(x303,x302)+~E(x301,x302)+~P12(x303,x301)
% 58.93/59.04 [31]P2(x312,x313,x314,x315)+~E(x311,x312)+~P2(x311,x313,x314,x315)
% 58.93/59.04 [32]P2(x323,x322,x324,x325)+~E(x321,x322)+~P2(x323,x321,x324,x325)
% 58.93/59.04 [33]P2(x333,x334,x332,x335)+~E(x331,x332)+~P2(x333,x334,x331,x335)
% 58.93/59.04 [34]P2(x343,x344,x345,x342)+~E(x341,x342)+~P2(x343,x344,x345,x341)
% 58.93/59.04 [35]P8(x352,x353,x354)+~E(x351,x352)+~P8(x351,x353,x354)
% 58.93/59.04 [36]P8(x363,x362,x364)+~E(x361,x362)+~P8(x363,x361,x364)
% 58.93/59.04 [37]P8(x373,x374,x372)+~E(x371,x372)+~P8(x373,x374,x371)
% 58.93/59.04 [38]P9(x382,x383,x384)+~E(x381,x382)+~P9(x381,x383,x384)
% 58.93/59.04 [39]P9(x393,x392,x394)+~E(x391,x392)+~P9(x393,x391,x394)
% 58.93/59.04 [40]P9(x403,x404,x402)+~E(x401,x402)+~P9(x403,x404,x401)
% 58.93/59.04 [41]P10(x412,x413,x414)+~E(x411,x412)+~P10(x411,x413,x414)
% 58.93/59.04 [42]P10(x423,x422,x424)+~E(x421,x422)+~P10(x423,x421,x424)
% 58.93/59.04 [43]P10(x433,x434,x432)+~E(x431,x432)+~P10(x433,x434,x431)
% 58.93/59.04 [44]P3(x442,x443,x444)+~E(x441,x442)+~P3(x441,x443,x444)
% 58.93/59.04 [45]P3(x453,x452,x454)+~E(x451,x452)+~P3(x453,x451,x454)
% 58.93/59.04 [46]P3(x463,x464,x462)+~E(x461,x462)+~P3(x463,x464,x461)
% 58.93/59.04 [47]P6(x472,x473,x474,x475)+~E(x471,x472)+~P6(x471,x473,x474,x475)
% 58.93/59.04 [48]P6(x483,x482,x484,x485)+~E(x481,x482)+~P6(x483,x481,x484,x485)
% 58.93/59.04 [49]P6(x493,x494,x492,x495)+~E(x491,x492)+~P6(x493,x494,x491,x495)
% 58.93/59.04 [50]P6(x503,x504,x505,x502)+~E(x501,x502)+~P6(x503,x504,x505,x501)
% 58.93/59.04 [51]P4(x512,x513,x514,x515)+~E(x511,x512)+~P4(x511,x513,x514,x515)
% 58.93/59.04 [52]P4(x523,x522,x524,x525)+~E(x521,x522)+~P4(x523,x521,x524,x525)
% 58.93/59.04 [53]P4(x533,x534,x532,x535)+~E(x531,x532)+~P4(x533,x534,x531,x535)
% 58.93/59.04 [54]P4(x543,x544,x545,x542)+~E(x541,x542)+~P4(x543,x544,x545,x541)
% 58.93/59.04
% 58.93/59.04 %-------------------------------------------
% 58.93/59.05 cnf(120,plain,
% 58.93/59.05 (P13(x1201,x1201)),
% 58.93/59.05 inference(equality_inference,[],[77])).
% 58.93/59.05 cnf(121,plain,
% 58.93/59.05 (~P1(x1211)+~P1(a1)+E(f3(x1211,a1),a1)),
% 58.93/59.05 inference(equality_inference,[],[79])).
% 58.93/59.05 cnf(122,plain,
% 58.93/59.05 (~P1(x1221)+~P1(a1)+E(f3(a1,x1221),a1)),
% 58.93/59.05 inference(equality_inference,[],[80])).
% 58.93/59.05 cnf(123,plain,
% 58.93/59.05 (~P1(x1231)+~P1(a4)+E(x1231,a1)+E(a4,a1)+E(f3(x1231,a4),a4)),
% 58.93/59.05 inference(equality_inference,[],[82])).
% 58.93/59.05 cnf(124,plain,
% 58.93/59.05 (~P1(x1241)+~P1(a4)+E(x1241,a1)+E(a4,a1)+E(f3(a4,x1241),a4)),
% 58.93/59.05 inference(equality_inference,[],[83])).
% 58.93/59.05 cnf(125,plain,
% 58.93/59.05 (~P1(x1251)+E(f3(x1251,a1),a1)),
% 58.93/59.05 inference(scs_inference,[],[55,121])).
% 58.93/59.05 cnf(126,plain,
% 58.93/59.05 (~P1(x1261)+E(f3(a1,x1261),a1)),
% 58.93/59.05 inference(scs_inference,[],[55,122])).
% 58.93/59.05 cnf(127,plain,
% 58.93/59.05 (~P1(x1271)+E(x1271,a1)+E(a4,a1)+E(f3(x1271,a4),a4)),
% 58.93/59.05 inference(scs_inference,[],[57,123])).
% 58.93/59.05 cnf(128,plain,
% 58.93/59.05 (~P1(x1281)+E(x1281,a1)+E(a4,a1)+E(f3(a4,x1281),a4)),
% 58.93/59.05 inference(scs_inference,[],[57,124])).
% 58.93/59.05 cnf(129,plain,
% 58.93/59.05 (~P8(x1291,x1291,x1292)),
% 58.93/59.05 inference(scs_inference,[],[74,98])).
% 58.93/59.05 cnf(131,plain,
% 58.93/59.05 (~P9(x1311,x1312,x1311)),
% 58.93/59.05 inference(scs_inference,[],[74,98,99])).
% 58.93/59.05 cnf(133,plain,
% 58.93/59.05 (~P10(x1331,x1331,x1332)),
% 58.93/59.05 inference(scs_inference,[],[74,98,99,100])).
% 58.93/59.05 cnf(137,plain,
% 58.93/59.05 (~P12(a9,a8)),
% 58.93/59.05 inference(scs_inference,[],[62,74,98,99,100,101,89])).
% 58.93/59.05 cnf(138,plain,
% 58.93/59.05 (~P12(x1381,x1381)),
% 58.93/59.05 inference(rename_variables,[],[74])).
% 58.93/59.05 cnf(141,plain,
% 58.93/59.05 (~P12(x1411,x1411)),
% 58.93/59.05 inference(rename_variables,[],[74])).
% 58.93/59.05 cnf(142,plain,
% 58.93/59.05 (P13(x1421,x1422)+~E(x1422,x1421)),
% 58.93/59.05 inference(scs_inference,[],[62,120,74,138,98,99,100,101,89,29,27])).
% 58.93/59.05 cnf(148,plain,
% 58.93/59.05 (~P12(x1481,x1481)),
% 58.93/59.05 inference(rename_variables,[],[74])).
% 58.93/59.05 cnf(153,plain,
% 58.93/59.05 (~E(a2,a1)),
% 58.93/59.05 inference(scs_inference,[],[62,120,63,74,138,141,148,65,98,99,100,101,89,29,27,86,87,90,91,92,28])).
% 58.93/59.05 cnf(167,plain,
% 58.93/59.05 (P12(a9,a10)),
% 58.93/59.05 inference(scs_inference,[],[64,63,137,101,98,99,100,89])).
% 58.93/59.05 cnf(175,plain,
% 58.93/59.05 (P12(a8,a11)),
% 58.93/59.05 inference(scs_inference,[],[62,63,89])).
% 58.93/59.05 cnf(179,plain,
% 58.93/59.05 (P12(a8,a10)),
% 58.93/59.05 inference(scs_inference,[],[62,167,89])).
% 58.93/59.05 cnf(181,plain,
% 58.93/59.05 (~E(a9,a10)),
% 58.93/59.05 inference(scs_inference,[],[62,167,74,89,29])).
% 58.93/59.05 cnf(183,plain,
% 58.93/59.05 (~P12(a11,a8)),
% 58.93/59.05 inference(scs_inference,[],[175,74,89])).
% 58.93/59.05 cnf(184,plain,
% 58.93/59.05 (~P12(x1841,x1841)),
% 58.93/59.05 inference(rename_variables,[],[74])).
% 58.93/59.05 cnf(188,plain,
% 58.93/59.05 (~P10(a11,x1881,a8)),
% 58.93/59.05 inference(scs_inference,[],[175,74,184,89,29,101])).
% 58.93/59.05 cnf(209,plain,
% 58.93/59.05 (E(a1,f3(a1,a1))),
% 58.93/59.05 inference(scs_inference,[],[55,2,125])).
% 58.93/59.05 cnf(210,plain,
% 58.93/59.05 (P13(f3(a1,a1),a1)),
% 58.93/59.05 inference(scs_inference,[],[209,142])).
% 58.93/59.05 cnf(211,plain,
% 58.93/59.05 (E(f3(a1,a1),a1)),
% 58.93/59.05 inference(scs_inference,[],[209,142,2])).
% 58.93/59.05 cnf(214,plain,
% 58.93/59.05 (P13(a1,f3(a1,a1))),
% 58.93/59.05 inference(scs_inference,[],[55,120,153,209,142,2,3,18,28])).
% 58.93/59.05 cnf(217,plain,
% 58.93/59.05 (~P13(a9,a8)),
% 58.93/59.05 inference(scs_inference,[],[62,68,85,87])).
% 58.93/59.05 cnf(218,plain,
% 58.93/59.05 (~P7(a8,a9,x2181)),
% 58.93/59.05 inference(scs_inference,[],[217,102])).
% 58.93/59.05 cnf(220,plain,
% 58.93/59.05 (~P7(a9,x2201,a8)),
% 58.93/59.05 inference(scs_inference,[],[217,102,103])).
% 58.93/59.05 cnf(228,plain,
% 58.93/59.05 (E(a1,f3(a1,a4))),
% 58.93/59.05 inference(scs_inference,[],[57,126,2])).
% 58.93/59.05 cnf(229,plain,
% 58.93/59.05 (P13(f3(a1,a4),a1)),
% 58.93/59.05 inference(scs_inference,[],[228,142])).
% 58.93/59.05 cnf(230,plain,
% 58.93/59.05 (E(f3(a1,a4),a1)),
% 58.93/59.05 inference(scs_inference,[],[228,142,2])).
% 58.93/59.05 cnf(232,plain,
% 58.93/59.05 (E(f3(a1,a1),f3(a1,a4))),
% 58.93/59.05 inference(scs_inference,[],[211,228,55,142,2,18,3])).
% 58.93/59.05 cnf(233,plain,
% 58.93/59.05 (P13(f3(a1,a4),f3(a1,a1))),
% 58.93/59.05 inference(scs_inference,[],[211,209,228,55,142,2,18,3,28])).
% 58.93/59.05 cnf(265,plain,
% 58.93/59.05 (E(f3(a1,a4),f3(a1,a1))),
% 58.93/59.05 inference(scs_inference,[],[230,232,142,2])).
% 58.93/59.05 cnf(267,plain,
% 58.93/59.05 (P13(f3(a1,a1),f3(a1,a4))),
% 58.93/59.05 inference(scs_inference,[],[209,230,232,153,142,2,3,27])).
% 58.93/59.06 cnf(281,plain,
% 58.93/59.06 (P5(a1,x2811,x2812,x2813)+P7(f5(f3(a1,a1),x2811,x2812,x2813),f3(a1,a1),x2811)),
% 58.93/59.06 inference(scs_inference,[],[211,113,22])).
% 58.93/59.06 cnf(282,plain,
% 58.93/59.06 (P6(a1,x2821,x2822,x2823)+P7(f6(f3(a1,a1),x2821,x2822,x2823),x2822,x2823)),
% 58.93/59.06 inference(scs_inference,[],[211,114,47])).
% 58.93/59.06 cnf(303,plain,
% 58.93/59.06 (P6(x3031,a1,x3032,x3033)+P7(f6(x3031,f3(a1,a1),x3032,x3033),x3031,f3(a1,a1))),
% 58.93/59.06 inference(scs_inference,[],[211,115,48])).
% 58.93/59.06 cnf(305,plain,
% 58.93/59.06 (~P4(x3051,f3(a1,a1),x3052,x3053)+P7(f7(x3051,a1,x3052,x3053),x3051,a1)),
% 58.93/59.06 inference(scs_inference,[],[211,117,52])).
% 58.93/59.06 cnf(325,plain,
% 58.93/59.06 (P13(x3251,f6(f3(a1,a1),x3252,x3251,x3253))+P6(a1,x3252,x3251,x3253)),
% 58.93/59.06 inference(scs_inference,[],[282,102])).
% 58.93/59.06 cnf(326,plain,
% 58.93/59.06 (P13(f3(a1,a1),f6(f3(a1,a1),x3261,a1,x3262))+P6(a1,x3261,a1,x3262)),
% 58.93/59.06 inference(scs_inference,[],[210,325,92])).
% 58.93/59.06 cnf(339,plain,
% 58.93/59.06 (~P4(x3391,f3(a1,a1),x3392,f3(a1,a1))+P7(f7(x3391,a1,x3392,a1),x3391,a1)),
% 58.93/59.06 inference(scs_inference,[],[211,305,54])).
% 58.93/59.06 cnf(355,plain,
% 58.93/59.06 (P6(f3(a1,a1),x3551,a1,x3552)+P13(f3(a1,a1),f6(f3(a1,a1),x3551,a1,x3552))),
% 58.93/59.06 inference(scs_inference,[],[209,326,47])).
% 58.93/59.06 cnf(358,plain,
% 58.93/59.06 (P5(f3(a1,a1),x3581,f3(a1,a1),x3581)+P5(a1,x3581,f3(a1,a1),x3581)),
% 58.93/59.06 inference(scs_inference,[],[281,119])).
% 58.93/59.06 cnf(359,plain,
% 58.93/59.06 (P5(f3(a1,a1),x3591,a1,x3591)+P5(a1,x3591,f3(a1,a1),x3591)),
% 58.93/59.06 inference(scs_inference,[],[211,358,24])).
% 58.93/59.06 cnf(360,plain,
% 58.93/59.06 (P5(a1,a1,f3(a1,a1),f3(a1,a1))+P5(f3(a1,a1),f3(a1,a1),a1,f3(a1,a1))),
% 58.93/59.06 inference(scs_inference,[],[211,359,23])).
% 58.93/59.06 cnf(361,plain,
% 58.93/59.06 (P13(x3611,f6(x3611,f3(a1,a1),x3612,x3613))+P6(x3611,a1,x3612,x3613)),
% 58.93/59.06 inference(scs_inference,[],[303,102])).
% 58.93/59.06 cnf(363,plain,
% 58.93/59.06 (~P4(x3631,a1,x3632,f3(a1,a1))+P7(f7(x3631,a1,x3632,a1),x3631,a1)),
% 58.93/59.06 inference(scs_inference,[],[209,339,52])).
% 58.93/59.06 cnf(364,plain,
% 58.93/59.06 (~P4(x3641,a1,f3(a1,a1),f3(a1,a1))+P7(f7(x3641,a1,a1,a1),x3641,a1)),
% 58.93/59.06 inference(scs_inference,[],[211,363,53])).
% 58.93/59.06 cnf(365,plain,
% 58.93/59.06 (~P4(x3651,a1,f3(a1,a1),a1)+P7(f7(x3651,a1,a1,a1),x3651,a1)),
% 58.93/59.06 inference(scs_inference,[],[209,364,54])).
% 58.93/59.06 cnf(366,plain,
% 58.93/59.06 (P13(f7(x3661,a1,a1,a1),a1)+~P4(x3661,a1,f3(a1,a1),a1)),
% 58.93/59.06 inference(scs_inference,[],[365,103])).
% 58.93/59.06 cnf(383,plain,
% 58.93/59.06 (P5(a1,f3(a1,a1),a1,f3(a1,a1))+P5(a1,a1,f3(a1,a1),f3(a1,a1))),
% 58.93/59.06 inference(scs_inference,[],[211,360,22])).
% 58.93/59.06 cnf(384,plain,
% 58.93/59.06 (P5(a1,a1,a1,f3(a1,a1))+P5(a1,a1,f3(a1,a1),f3(a1,a1))),
% 58.93/59.06 inference(scs_inference,[],[211,383,23])).
% 58.93/59.06 cnf(385,plain,
% 58.93/59.06 (P5(a1,a1,a1,f3(a1,a1))),
% 58.93/59.06 inference(scs_inference,[],[211,384,24])).
% 58.93/59.06 cnf(386,plain,
% 58.93/59.06 (P5(f3(a1,a1),a1,a1,f3(a1,a1))),
% 58.93/59.06 inference(scs_inference,[],[209,385,22])).
% 58.93/59.06 cnf(387,plain,
% 58.93/59.06 (P5(a1,f3(a1,a1),a1,f3(a1,a1))),
% 58.93/59.06 inference(scs_inference,[],[209,385,22,23])).
% 58.93/59.06 cnf(388,plain,
% 58.93/59.06 (P5(a1,a1,f3(a1,a1),f3(a1,a1))),
% 58.93/59.06 inference(scs_inference,[],[209,385,22,23,24])).
% 58.93/59.06 cnf(389,plain,
% 58.93/59.06 (P5(a1,a1,a1,a1)),
% 58.93/59.06 inference(scs_inference,[],[211,209,385,22,23,24,25])).
% 58.93/59.06 cnf(390,plain,
% 58.93/59.06 (~P6(a1,f3(a1,a1),x3901,x3902)+P6(a1,a1,x3901,x3902)),
% 58.93/59.06 inference(scs_inference,[],[211,209,385,22,23,24,25,118])).
% 58.93/59.06 cnf(412,plain,
% 58.93/59.06 (P5(f3(a1,a1),f3(a1,a1),a1,f3(a1,a1))),
% 58.93/59.06 inference(scs_inference,[],[209,387,22])).
% 58.93/59.06 cnf(413,plain,
% 58.93/59.06 (P5(a1,f3(a1,a1),f3(a1,a1),f3(a1,a1))),
% 58.93/59.06 inference(scs_inference,[],[209,387,22,24])).
% 58.93/59.06 cnf(414,plain,
% 58.93/59.06 (P5(a1,f3(a1,a1),a1,a1)),
% 58.93/59.06 inference(scs_inference,[],[209,387,389,22,24,23])).
% 58.93/59.06 cnf(415,plain,
% 58.93/59.06 (P5(a1,a1,f3(a1,a1),a1)),
% 58.93/59.06 inference(scs_inference,[],[211,209,387,388,389,22,24,23,25])).
% 58.93/59.06 cnf(422,plain,
% 58.93/59.06 (P5(a1,f3(a1,a1),f3(a1,a1),a1)),
% 58.93/59.06 inference(scs_inference,[],[209,413,414,22,24])).
% 58.93/59.06 cnf(423,plain,
% 58.93/59.06 (P5(f3(a1,a1),a1,f3(a1,a1),f3(a1,a1))),
% 58.93/59.06 inference(scs_inference,[],[211,209,413,414,22,24,23])).
% 58.93/59.06 cnf(424,plain,
% 58.93/59.06 (P5(f3(a1,a1),f3(a1,a1),a1,a1)),
% 58.93/59.06 inference(scs_inference,[],[211,209,413,412,414,22,24,23,25])).
% 58.93/59.06 cnf(425,plain,
% 58.93/59.06 (~P6(f3(a1,a1),f3(a1,a1),x4251,x4252)+P6(a1,f3(a1,a1),x4251,x4252)),
% 58.93/59.06 inference(scs_inference,[],[211,209,413,412,414,22,24,23,25,118])).
% 58.93/59.06 cnf(427,plain,
% 58.93/59.06 (P5(f3(a1,a1),f3(a1,a1),f3(a1,a1),a1)),
% 58.93/59.06 inference(scs_inference,[],[209,422,22])).
% 58.93/59.06 cnf(428,plain,
% 58.93/59.06 (P5(f3(a1,a1),a1,a1,a1)),
% 58.93/59.06 inference(scs_inference,[],[211,209,422,424,22,23])).
% 58.93/59.06 cnf(429,plain,
% 58.93/59.06 (P5(f3(a1,a1),a1,f3(a1,a1),a1)),
% 58.93/59.06 inference(scs_inference,[],[211,209,422,424,22,23,24])).
% 58.93/59.06 cnf(430,plain,
% 58.93/59.06 (~P6(f3(a1,a1),f3(a1,a1),x4301,x4302)+P6(f3(a1,a1),a1,x4301,x4302)),
% 58.93/59.06 inference(scs_inference,[],[211,209,423,422,424,22,23,24,118])).
% 58.93/59.06 cnf(437,plain,
% 58.93/59.06 (~P6(a1,f3(a1,a1),x4371,x4372)+P6(f3(a1,a1),a1,x4371,x4372)),
% 58.93/59.06 inference(scs_inference,[],[386,118])).
% 58.93/59.06 cnf(439,plain,
% 58.93/59.06 (P6(f3(a1,a1),a1,x4391,x4392)+P7(f6(f3(a1,a1),f3(a1,a1),x4391,x4392),x4391,x4392)),
% 58.93/59.06 inference(scs_inference,[],[386,118,282])).
% 58.93/59.06 cnf(443,plain,
% 58.93/59.06 (~P6(x4431,x4432,x4431,x4432)+P6(f3(a1,a1),a1,x4431,x4432)),
% 58.93/59.06 inference(scs_inference,[],[386,118,282,325,112])).
% 58.93/59.06 cnf(445,plain,
% 58.93/59.06 (P4(x4451,x4452,x4451,x4452)+P6(f3(a1,a1),a1,x4451,x4452)),
% 58.93/59.06 inference(scs_inference,[],[386,118,282,325,112,109])).
% 58.93/59.06 cnf(452,plain,
% 58.93/59.06 (P4(a1,a1,f3(a1,a1),a1)+P6(f3(a1,a1),a1,f3(a1,a1),a1)),
% 58.93/59.06 inference(scs_inference,[],[211,209,386,118,282,325,112,109,111,19,20,87,54,51])).
% 58.93/59.06 cnf(457,plain,
% 58.93/59.06 (~P6(f3(a1,a1),a1,x4571,x4572)+P6(a1,a1,x4571,x4572)),
% 58.93/59.06 inference(scs_inference,[],[415,118])).
% 58.93/59.06 cnf(459,plain,
% 58.93/59.06 (P6(a1,a1,x4591,x4592)+P13(f3(a1,a1),f6(f3(a1,a1),f3(a1,a1),x4591,x4592))),
% 58.93/59.06 inference(scs_inference,[],[415,118,361])).
% 58.93/59.06 cnf(461,plain,
% 58.93/59.06 (P6(a1,a1,x4611,x4612)+P7(f6(f3(a1,a1),f3(a1,a1),x4611,x4612),f3(a1,a1),f3(a1,a1))),
% 58.93/59.06 inference(scs_inference,[],[415,118,361,303])).
% 58.93/59.06 cnf(467,plain,
% 58.93/59.06 (~P6(x4671,x4672,x4671,x4672)+P6(a1,a1,x4671,x4672)),
% 58.93/59.06 inference(scs_inference,[],[415,118,361,303,430,439,443])).
% 58.93/59.06 cnf(469,plain,
% 58.93/59.06 (P4(x4691,x4692,x4691,x4692)+P6(a1,a1,x4691,x4692)),
% 58.93/59.06 inference(scs_inference,[],[415,118,361,303,430,439,443,445])).
% 58.93/59.06 cnf(473,plain,
% 58.93/59.06 (P6(a1,a1,a1,x4731)+P7(f6(f3(a1,a1),x4731,a1,x4731),a1,x4731)),
% 58.93/59.06 inference(scs_inference,[],[415,118,361,303,430,439,443,445,326,282])).
% 58.93/59.06 cnf(503,plain,
% 58.93/59.06 (P6(a1,f3(a1,a1),a1,x5031)+P7(f6(f3(a1,a1),x5031,a1,x5031),a1,x5031)),
% 58.93/59.06 inference(scs_inference,[],[422,118,355,303,443,445,326,282])).
% 58.93/59.06 cnf(508,plain,
% 58.93/59.06 (P4(a1,x5081,f3(a1,a1),x5081)+P6(a1,f3(a1,a1),a1,x5081)),
% 58.93/59.06 inference(scs_inference,[],[211,209,422,118,355,303,443,445,326,282,325,21,53])).
% 58.93/59.06 cnf(509,plain,
% 58.93/59.06 (P4(f3(a1,a1),f3(a1,a1),f3(a1,a1),f3(a1,a1))+P6(a1,f3(a1,a1),a1,x5091)),
% 58.93/59.06 inference(scs_inference,[],[211,209,422,118,355,303,443,445,326,282,325,21,53,109])).
% 58.93/59.06 cnf(511,plain,
% 58.93/59.06 (~P6(f3(a1,a1),f3(a1,a1),f3(a1,a1),f3(a1,a1))+P6(a1,f3(a1,a1),a1,x5111)),
% 58.93/59.06 inference(scs_inference,[],[211,209,422,118,355,303,443,445,326,282,325,21,53,109,112])).
% 58.93/59.06 cnf(525,plain,
% 58.93/59.06 (~P6(a1,a1,x5251,x5252)+P6(a1,f3(a1,a1),x5251,x5252)),
% 58.93/59.06 inference(scs_inference,[],[414,118])).
% 58.93/59.06 cnf(527,plain,
% 58.93/59.06 (P6(a1,f3(a1,a1),x5271,x5272)+P13(f3(a1,a1),f6(f3(a1,a1),f3(a1,a1),x5271,x5272))),
% 58.93/59.06 inference(scs_inference,[],[414,118,459])).
% 58.93/59.06 cnf(529,plain,
% 58.93/59.06 (P6(a1,f3(a1,a1),x5291,x5292)+P7(f6(f3(a1,a1),f3(a1,a1),x5291,x5292),f3(a1,a1),f3(a1,a1))),
% 58.93/59.06 inference(scs_inference,[],[414,118,459,461])).
% 58.93/59.06 cnf(531,plain,
% 58.93/59.06 (~P6(x5311,x5312,x5311,x5312)+P6(a1,f3(a1,a1),x5311,x5312)),
% 58.93/59.06 inference(scs_inference,[],[414,118,459,461,467])).
% 58.93/59.06 cnf(533,plain,
% 58.93/59.06 (P4(x5331,x5332,x5331,x5332)+P6(a1,f3(a1,a1),x5331,x5332)),
% 58.93/59.06 inference(scs_inference,[],[414,118,459,461,467,469])).
% 58.93/59.06 cnf(546,plain,
% 58.93/59.06 (~P6(a1,a1,x5461,x5462)+P6(f3(a1,a1),f3(a1,a1),x5461,x5462)),
% 58.93/59.06 inference(scs_inference,[],[424,118])).
% 58.93/59.06 cnf(571,plain,
% 58.93/59.06 (~P6(f3(a1,a1),a1,x5711,x5712)+P6(f3(a1,a1),f3(a1,a1),x5711,x5712)),
% 58.93/59.06 inference(scs_inference,[],[427,118])).
% 58.93/59.06 cnf(573,plain,
% 58.93/59.06 (P4(x5731,x5732,x5731,x5732)+P6(f3(a1,a1),f3(a1,a1),x5731,x5732)),
% 58.93/59.06 inference(scs_inference,[],[427,118,445])).
% 58.93/59.06 cnf(591,plain,
% 58.93/59.06 (P6(f3(a1,a1),a1,a1,x5911)+P7(f6(f3(a1,a1),x5911,a1,x5911),a1,x5911)),
% 58.93/59.06 inference(scs_inference,[],[428,118,473])).
% 58.93/59.06 cnf(615,plain,
% 58.93/59.06 (P6(a1,f3(a1,a1),x6151,x6152)+P7(f6(x6151,x6152,x6151,x6152),x6151,x6152)),
% 58.93/59.06 inference(scs_inference,[],[531,115])).
% 58.93/59.06 cnf(616,plain,
% 58.93/59.06 (P6(a1,f3(a1,a1),x6161,x6162)+P7(f7(x6161,x6162,x6161,x6162),x6161,x6162)),
% 58.93/59.06 inference(scs_inference,[],[533,116])).
% 58.93/59.06 cnf(622,plain,
% 58.93/59.06 (P6(f3(a1,a1),f3(a1,a1),x6221,x6222)+P7(f7(x6221,x6222,x6221,x6222),x6221,x6222)),
% 58.93/59.06 inference(scs_inference,[],[573,117])).
% 58.93/59.06 cnf(628,plain,
% 58.93/59.06 (P13(f6(x6281,x6282,x6281,x6282),x6282)+P6(a1,f3(a1,a1),x6281,x6282)),
% 58.93/59.06 inference(scs_inference,[],[615,103])).
% 58.93/59.06 cnf(633,plain,
% 58.93/59.06 (P13(x6331,f7(x6331,x6332,x6331,x6332))+P6(a1,f3(a1,a1),x6331,x6332)),
% 58.93/59.06 inference(scs_inference,[],[616,102])).
% 58.93/59.06 cnf(634,plain,
% 58.93/59.06 (P13(f3(a1,a4),f7(f3(a1,a1),x6341,f3(a1,a1),x6341))+P6(a1,f3(a1,a1),f3(a1,a1),x6341)),
% 58.93/59.06 inference(scs_inference,[],[233,633,92])).
% 58.93/59.06 cnf(638,plain,
% 58.93/59.06 (P6(a1,a1,f3(a1,a1),a1)+P4(a1,a1,f3(a1,a1),a1)),
% 58.93/59.06 inference(scs_inference,[],[452,457])).
% 58.93/59.06 cnf(639,plain,
% 58.93/59.06 (P6(f3(a1,a1),f3(a1,a1),f3(a1,a1),a1)+P4(a1,a1,f3(a1,a1),a1)),
% 58.93/59.06 inference(scs_inference,[],[638,546])).
% 58.93/59.06 cnf(656,plain,
% 58.93/59.06 (P13(f6(f3(a1,a1),x6561,a1,x6561),x6561)+P6(f3(a1,a1),a1,a1,x6561)),
% 58.93/59.06 inference(scs_inference,[],[591,103])).
% 58.93/59.06 cnf(673,plain,
% 58.93/59.06 (P6(a1,f3(a1,a1),f3(a1,a1),a1)+P4(a1,a1,f3(a1,a1),a1)),
% 58.93/59.06 inference(scs_inference,[],[639,425])).
% 58.93/59.06 cnf(674,plain,
% 58.93/59.06 (P6(a1,f3(a1,a1),f3(a1,a1),f3(a1,a1))+P4(a1,a1,f3(a1,a1),a1)),
% 58.93/59.06 inference(scs_inference,[],[209,673,50])).
% 58.93/59.06 cnf(691,plain,
% 58.93/59.06 (P6(a1,a1,f3(a1,a1),f3(a1,a1))+P4(a1,a1,f3(a1,a1),a1)),
% 58.93/59.06 inference(scs_inference,[],[674,390])).
% 58.93/59.06 cnf(695,plain,
% 58.93/59.06 (P5(f3(a1,a4),a1,f3(a1,a1),f3(a1,a1))),
% 58.93/59.06 inference(scs_inference,[],[228,388,22])).
% 58.93/59.06 cnf(696,plain,
% 58.93/59.06 (P5(a1,a1,a1,f3(a1,a4))),
% 58.93/59.06 inference(scs_inference,[],[228,388,389,22,25])).
% 58.93/59.06 cnf(698,plain,
% 58.93/59.06 (P5(f3(a1,a1),f3(a1,a1),f3(a1,a4),f3(a1,a1))),
% 58.93/59.06 inference(scs_inference,[],[228,412,388,389,22,25,23,24])).
% 58.93/59.06 cnf(725,plain,
% 58.93/59.06 (P5(a1,f3(a1,a1),a1,f3(a1,a4))),
% 58.93/59.06 inference(scs_inference,[],[228,413,414,22,25])).
% 58.93/59.06 cnf(727,plain,
% 58.93/59.06 (P5(a1,f3(a1,a1),f3(a1,a4),a1)),
% 58.93/59.06 inference(scs_inference,[],[228,413,414,423,22,25,23,24])).
% 58.93/59.06 cnf(728,plain,
% 58.93/59.06 (~P6(f3(a1,a4),f3(a1,a1),x7281,x7282)+P6(f3(a1,a1),f3(a1,a1),x7281,x7282)),
% 58.93/59.06 inference(scs_inference,[],[228,413,414,423,698,22,25,23,24,118])).
% 58.93/59.06 cnf(730,plain,
% 58.93/59.06 (P5(f3(a1,a4),f3(a1,a1),f3(a1,a1),a1)),
% 58.93/59.06 inference(scs_inference,[],[228,422,22])).
% 58.93/59.06 cnf(731,plain,
% 58.93/59.06 (P5(a1,f3(a1,a1),f3(a1,a1),f3(a1,a4))),
% 58.93/59.06 inference(scs_inference,[],[228,422,22,25])).
% 58.93/59.06 cnf(732,plain,
% 58.93/59.06 (P5(a1,f3(a1,a4),a1,a1)),
% 58.93/59.06 inference(scs_inference,[],[228,422,389,22,25,23])).
% 58.93/59.06 cnf(733,plain,
% 58.93/59.06 (P5(f3(a1,a1),f3(a1,a1),f3(a1,a4),a1)),
% 58.93/59.06 inference(scs_inference,[],[228,422,424,389,22,25,23,24])).
% 58.93/59.06 cnf(761,plain,
% 58.93/59.06 (P5(f3(a1,a4),f3(a1,a1),a1,f3(a1,a1))),
% 58.93/59.06 inference(scs_inference,[],[228,387,22])).
% 58.93/59.06 cnf(762,plain,
% 58.93/59.06 (P5(a1,a1,f3(a1,a1),f3(a1,a4))),
% 58.93/59.06 inference(scs_inference,[],[228,387,415,22,25])).
% 58.93/59.06 cnf(805,plain,
% 58.93/59.06 (P5(f3(a1,a4),a1,a1,a1)),
% 58.93/59.06 inference(scs_inference,[],[228,389,22])).
% 58.93/59.06 cnf(807,plain,
% 58.93/59.06 (P5(f3(a1,a1),f3(a1,a4),a1,f3(a1,a1))),
% 58.93/59.06 inference(scs_inference,[],[228,424,389,386,22,25,23])).
% 58.93/59.06 cnf(808,plain,
% 58.93/59.06 (P5(a1,a1,f3(a1,a4),a1)),
% 58.93/59.06 inference(scs_inference,[],[228,424,389,386,22,25,23,24])).
% 58.93/59.06 cnf(819,plain,
% 58.93/59.06 (P5(f3(a1,a4),f3(a1,a1),a1,a1)),
% 58.93/59.06 inference(scs_inference,[],[228,414,22])).
% 58.93/59.06 cnf(820,plain,
% 58.93/59.06 (P5(f3(a1,a1),f3(a1,a1),f3(a1,a1),f3(a1,a4))),
% 58.93/59.06 inference(scs_inference,[],[228,414,427,22,25])).
% 58.93/59.06 cnf(821,plain,
% 58.93/59.06 (P5(a1,a1,f3(a1,a4),f3(a1,a1))),
% 58.93/59.06 inference(scs_inference,[],[228,414,385,427,22,25,24])).
% 58.93/59.06 cnf(822,plain,
% 58.93/59.06 (P5(a1,f3(a1,a4),a1,f3(a1,a1))),
% 58.93/59.06 inference(scs_inference,[],[228,414,385,427,22,25,24,23])).
% 58.93/59.06 cnf(834,plain,
% 58.93/59.06 (P5(f3(a1,a4),a1,f3(a1,a1),a1)),
% 58.93/59.06 inference(scs_inference,[],[228,415,22])).
% 58.93/59.06 cnf(836,plain,
% 58.93/59.06 (P5(f3(a1,a1),f3(a1,a4),a1,a1)),
% 58.93/59.06 inference(scs_inference,[],[228,415,428,22,25,23])).
% 58.93/59.06 cnf(838,plain,
% 58.93/59.06 (~P6(f3(a1,a1),f3(a1,a4),x8381,x8382)+P6(a1,f3(a1,a1),x8381,x8382)),
% 58.93/59.06 inference(scs_inference,[],[228,386,415,428,731,22,25,23,24,118])).
% 58.93/59.06 cnf(845,plain,
% 58.93/59.06 (P5(f3(a1,a4),a1,a1,f3(a1,a1))),
% 58.93/59.06 inference(scs_inference,[],[228,385,22])).
% 58.93/59.06 cnf(847,plain,
% 58.93/59.06 (P5(f3(a1,a1),a1,f3(a1,a4),a1)),
% 58.93/59.06 inference(scs_inference,[],[228,385,429,428,22,25,24])).
% 58.93/59.06 cnf(848,plain,
% 58.93/59.06 (P5(f3(a1,a1),f3(a1,a4),f3(a1,a1),a1)),
% 58.93/59.06 inference(scs_inference,[],[228,385,429,428,22,25,24,23])).
% 58.93/59.06 cnf(868,plain,
% 58.93/59.06 (P5(f3(a1,a4),f3(a1,a1),a1,f3(a1,a4))),
% 58.93/59.07 inference(scs_inference,[],[228,725,22])).
% 58.93/59.07 cnf(869,plain,
% 58.93/59.07 (P5(a1,f3(a1,a4),a1,f3(a1,a4))),
% 58.93/59.07 inference(scs_inference,[],[228,725,732,22,25])).
% 58.93/59.07 cnf(872,plain,
% 58.93/59.07 (~P6(a1,f3(a1,a4),x8721,x8722)+P6(a1,f3(a1,a1),x8721,x8722)),
% 58.93/59.07 inference(scs_inference,[],[228,695,725,732,22,25,23,24,118])).
% 58.93/59.07 cnf(892,plain,
% 58.93/59.07 (P5(a1,a1,f3(a1,a4),f3(a1,a4))),
% 58.93/59.07 inference(scs_inference,[],[228,762,696,730,22,25,24])).
% 58.93/59.07 cnf(893,plain,
% 58.93/59.07 (P5(a1,f3(a1,a4),f3(a1,a1),f3(a1,a4))),
% 58.93/59.07 inference(scs_inference,[],[228,762,696,730,22,25,24,23])).
% 58.93/59.07 cnf(903,plain,
% 58.93/59.07 (P5(f3(a1,a4),f3(a1,a1),f3(a1,a4),a1)),
% 58.93/59.07 inference(scs_inference,[],[228,727,22])).
% 58.93/59.07 cnf(905,plain,
% 58.93/59.07 (P5(f3(a1,a4),f3(a1,a4),f3(a1,a1),a1)),
% 58.93/59.07 inference(scs_inference,[],[228,834,727,805,22,25,23])).
% 58.93/59.07 cnf(919,plain,
% 58.93/59.07 (P6(f3(a1,a4),a1,a1,x9191)+~P6(f3(a1,a1),f3(a1,a1),f3(a1,a1),f3(a1,a1))),
% 58.93/59.07 inference(scs_inference,[],[228,834,761,727,805,22,25,23,24,118,656,437,503,508,509,511])).
% 58.93/59.07 cnf(977,plain,
% 58.93/59.07 (P5(f3(a1,a4),f3(a1,a4),a1,f3(a1,a1))),
% 58.93/59.07 inference(scs_inference,[],[228,822,22])).
% 58.93/59.07 cnf(980,plain,
% 58.93/59.07 (P5(a1,f3(a1,a4),f3(a1,a4),a1)),
% 58.93/59.07 inference(scs_inference,[],[228,822,808,836,22,25,24,23])).
% 58.93/59.07 cnf(981,plain,
% 58.93/59.07 (~P6(a1,a1,x9811,x9812)+P6(f3(a1,a4),f3(a1,a1),x9811,x9812)),
% 58.93/59.07 inference(scs_inference,[],[228,819,822,808,836,22,25,24,23,118])).
% 58.93/59.07 cnf(1042,plain,
% 58.93/59.07 (P5(f3(a1,a1),f3(a1,a4),f3(a1,a4),a1)),
% 58.93/59.07 inference(scs_inference,[],[228,847,821,22,25,23])).
% 58.93/59.07 cnf(1074,plain,
% 58.93/59.07 (P4(f3(a1,a1),a1,f3(a1,a1),f3(a1,a1))+P6(f3(a1,a4),a1,f3(a1,a1),f3(a1,a1))),
% 58.93/59.07 inference(scs_inference,[],[228,233,211,412,845,807,847,821,22,25,23,24,118,527,628,633,634,533,838,531,615,529,622,92,21,111,87,20,52])).
% 58.93/59.07 cnf(1075,plain,
% 58.93/59.07 (P4(f3(a1,a1),f3(a1,a1),a1,f3(a1,a1))+P6(f3(a1,a4),a1,f3(a1,a1),f3(a1,a1))),
% 58.93/59.07 inference(scs_inference,[],[228,233,211,412,845,807,847,821,22,25,23,24,118,527,628,633,634,533,838,531,615,529,622,92,21,111,87,20,52,19,53])).
% 58.93/59.07 cnf(1081,plain,
% 58.93/59.07 (P5(f3(a1,a4),f3(a1,a1),f3(a1,a4),f3(a1,a4))),
% 58.93/59.07 inference(scs_inference,[],[228,848,893,868,22,25,24])).
% 58.93/59.07 cnf(1082,plain,
% 58.93/59.07 (P5(f3(a1,a4),a1,f3(a1,a4),a1)),
% 58.93/59.07 inference(scs_inference,[],[228,211,848,893,868,903,22,25,24,23])).
% 58.93/59.07 cnf(1125,plain,
% 58.93/59.07 (P5(f3(a1,a4),f3(a1,a4),a1,a1)),
% 58.93/59.07 inference(scs_inference,[],[228,211,977,892,22,25])).
% 58.93/59.07 cnf(1136,plain,
% 58.93/59.07 (P5(f3(a1,a4),f3(a1,a4),f3(a1,a4),a1)),
% 58.93/59.07 inference(scs_inference,[],[228,980,22])).
% 58.93/59.07 cnf(1138,plain,
% 58.93/59.07 (P5(a1,f3(a1,a4),f3(a1,a4),f3(a1,a4))),
% 58.93/59.07 inference(scs_inference,[],[228,869,1042,980,22,25,24])).
% 58.93/59.07 cnf(1146,plain,
% 58.93/59.07 (P5(f3(a1,a1),f3(a1,a1),f3(a1,a4),f3(a1,a4))),
% 58.93/59.07 inference(scs_inference,[],[228,733,25])).
% 58.93/59.07 cnf(1250,plain,
% 58.93/59.07 (~P6(a1,a1,x12501,x12502)+P6(f3(a1,a4),f3(a1,a4),x12501,x12502)),
% 58.93/59.07 inference(scs_inference,[],[1125,118])).
% 58.93/59.07 cnf(1337,plain,
% 58.93/59.07 (~P6(f3(a1,a4),a1,x13371,x13372)+P6(f3(a1,a4),f3(a1,a4),x13371,x13372)),
% 58.93/59.07 inference(scs_inference,[],[1136,118])).
% 58.93/59.07 cnf(1637,plain,
% 58.93/59.07 (~P6(f3(a1,a1),a1,x16371,x16372)+P6(f3(a1,a4),f3(a1,a4),x16371,x16372)),
% 58.93/59.07 inference(scs_inference,[],[905,118])).
% 58.93/59.07 cnf(1849,plain,
% 58.93/59.07 (~P6(f3(a1,a4),f3(a1,a4),x18491,x18492)+P6(f3(a1,a4),f3(a1,a1),x18491,x18492)),
% 58.93/59.07 inference(scs_inference,[],[1081,118])).
% 58.93/59.07 cnf(2297,plain,
% 58.93/59.07 (~P6(f3(a1,a1),f3(a1,a4),x22971,x22972)+P6(f3(a1,a1),f3(a1,a1),x22971,x22972)),
% 58.93/59.07 inference(scs_inference,[],[820,118])).
% 58.93/59.07 cnf(2619,plain,
% 58.93/59.07 (~P6(f3(a1,a4),a1,x26191,x26192)+P6(a1,f3(a1,a1),x26191,x26192)),
% 58.93/59.07 inference(scs_inference,[],[727,118])).
% 58.93/59.07 cnf(2820,plain,
% 58.93/59.07 (~P6(a1,f3(a1,a1),x28201,x28202)+P6(f3(a1,a4),f3(a1,a1),x28201,x28202)),
% 58.93/59.07 inference(scs_inference,[],[761,118])).
% 58.93/59.07 cnf(3479,plain,
% 58.93/59.07 (~P6(a1,f3(a1,a4),x34791,x34792)+P6(f3(a1,a4),f3(a1,a1),x34791,x34792)),
% 58.93/59.07 inference(scs_inference,[],[868,118])).
% 58.93/59.07 cnf(3756,plain,
% 58.93/59.07 (~P6(f3(a1,a4),a1,x37561,x37562)+P6(f3(a1,a4),f3(a1,a1),x37561,x37562)),
% 58.93/59.07 inference(scs_inference,[],[903,118])).
% 58.93/59.07 cnf(4358,plain,
% 58.93/59.07 (~P6(f3(a1,a1),a1,x43581,x43582)+P6(f3(a1,a4),f3(a1,a1),x43581,x43582)),
% 58.93/59.07 inference(scs_inference,[],[730,118])).
% 58.93/59.07 cnf(4904,plain,
% 58.93/59.07 (~P6(f3(a1,a4),f3(a1,a4),x49041,x49042)+P6(f3(a1,a1),f3(a1,a1),x49041,x49042)),
% 58.93/59.07 inference(scs_inference,[],[1146,118])).
% 58.93/59.07 cnf(5305,plain,
% 58.93/59.07 (~P6(f3(a1,a4),f3(a1,a4),f3(a1,a1),f3(a1,a1))+P6(f3(a1,a4),a1,a1,x53051)),
% 58.93/59.07 inference(scs_inference,[],[4904,919])).
% 58.93/59.07 cnf(5790,plain,
% 58.93/59.07 (~P6(a1,a1,f3(a1,a1),f3(a1,a1))+P6(f3(a1,a4),a1,a1,x57901)),
% 58.93/59.07 inference(scs_inference,[],[5305,1250])).
% 58.93/59.07 cnf(5791,plain,
% 58.93/59.07 (P4(a1,a1,f3(a1,a1),a1)+P6(f3(a1,a4),a1,a1,x57911)),
% 58.93/59.07 inference(scs_inference,[],[5790,691])).
% 58.93/59.07 cnf(5792,plain,
% 58.93/59.07 (P7(f7(a1,a1,a1,a1),a1,a1)+P6(f3(a1,a4),a1,a1,x57921)),
% 58.93/59.07 inference(scs_inference,[],[5791,365])).
% 58.93/59.07 cnf(5795,plain,
% 58.93/59.07 (E(f3(a2,a1),a1)),
% 58.93/59.07 inference(scs_inference,[],[56,125])).
% 58.93/59.07 cnf(5797,plain,
% 58.93/59.07 (E(f3(a1,a2),a1)),
% 58.93/59.07 inference(scs_inference,[],[56,125,126])).
% 58.93/59.07 cnf(5799,plain,
% 58.93/59.07 (P13(a9,a10)),
% 58.93/59.07 inference(scs_inference,[],[56,167,125,126,85])).
% 58.93/59.07 cnf(5801,plain,
% 58.93/59.07 (P13(f3(a2,a1),a1)),
% 58.93/59.07 inference(scs_inference,[],[56,167,125,126,85,77])).
% 58.93/59.07 cnf(5803,plain,
% 58.93/59.07 (~E(a4,a1)),
% 58.93/59.07 inference(scs_inference,[],[56,66,167,125,126,85,77,2])).
% 58.93/59.07 cnf(5806,plain,
% 58.93/59.07 (~P8(f3(a1,a4),f3(a1,a1),x58061)),
% 58.93/59.07 inference(scs_inference,[],[56,66,129,167,229,265,214,125,126,85,77,2,93,35])).
% 58.93/59.07 cnf(5808,plain,
% 58.93/59.07 (~P9(f3(a1,a4),x58081,f3(a1,a1))),
% 58.93/59.07 inference(scs_inference,[],[56,66,129,131,167,229,265,214,125,126,85,77,2,93,35,38])).
% 58.93/59.07 cnf(5811,plain,
% 58.93/59.07 (~P10(x58111,x58111,x58112)),
% 58.93/59.07 inference(rename_variables,[],[133])).
% 58.93/59.07 cnf(5818,plain,
% 58.93/59.07 (~P12(a1,f3(a1,a4))),
% 58.93/59.07 inference(scs_inference,[],[133,5811,56,66,129,131,167,229,265,214,74,62,125,126,85,77,2,93,35,38,41,42,94,97,90])).
% 58.93/59.07 cnf(5819,plain,
% 58.93/59.07 (~P12(x58191,x58191)),
% 58.93/59.07 inference(rename_variables,[],[74])).
% 58.93/59.07 cnf(5822,plain,
% 58.93/59.07 (P13(x58221,x58221)),
% 58.93/59.07 inference(rename_variables,[],[120])).
% 58.93/59.07 cnf(5825,plain,
% 58.93/59.07 (~P12(x58251,x58251)),
% 58.93/59.07 inference(rename_variables,[],[74])).
% 58.93/59.07 cnf(5827,plain,
% 58.93/59.07 (P13(x58271,x58271)),
% 58.93/59.07 inference(rename_variables,[],[120])).
% 58.93/59.07 cnf(5829,plain,
% 58.93/59.07 (~P12(a1,f3(a1,a1))),
% 58.93/59.07 inference(scs_inference,[],[133,5811,56,66,129,131,167,229,267,265,214,120,5822,74,5819,62,125,126,85,77,2,93,35,38,41,42,94,97,90,96,30,95,91])).
% 58.93/59.07 cnf(5831,plain,
% 58.93/59.07 (P7(a1,f3(a1,a4),f3(a1,a4))),
% 58.93/59.07 inference(scs_inference,[],[133,5811,56,66,129,1081,131,167,229,267,265,214,120,5822,74,5819,62,125,126,85,77,2,93,35,38,41,42,94,97,90,96,30,95,91,111])).
% 58.93/59.07 cnf(5837,plain,
% 58.93/59.07 (~E(f3(a1,a1),a4)),
% 58.93/59.07 inference(scs_inference,[],[69,133,5811,181,56,66,183,129,1081,131,167,229,267,265,214,120,5822,74,5819,62,209,125,126,85,77,2,93,35,38,41,42,94,97,90,96,30,95,91,111,87,86,3])).
% 58.93/59.07 cnf(5839,plain,
% 58.93/59.07 (~P12(x58391,x58391)),
% 58.93/59.07 inference(rename_variables,[],[74])).
% 58.93/59.07 cnf(5840,plain,
% 58.93/59.07 (E(f3(a2,a4),a4)),
% 58.93/59.07 inference(scs_inference,[],[69,133,5811,181,56,66,183,129,1081,131,167,229,267,265,153,214,120,5822,74,5819,5825,62,209,125,126,85,77,2,93,35,38,41,42,94,97,90,96,30,95,91,111,87,86,3,29,127])).
% 58.93/59.07 cnf(5842,plain,
% 58.93/59.07 (E(f3(a4,a2),a4)),
% 58.93/59.07 inference(scs_inference,[],[69,133,5811,181,56,66,183,129,1081,131,167,229,267,265,153,214,120,5822,74,5819,5825,62,209,125,126,85,77,2,93,35,38,41,42,94,97,90,96,30,95,91,111,87,86,3,29,127,128])).
% 58.93/59.07 cnf(5851,plain,
% 58.93/59.07 (~P6(f3(a1,a4),f3(a1,a1),f3(a1,a4),f3(a1,a1))),
% 58.93/59.07 inference(scs_inference,[],[69,133,5811,181,56,66,188,183,129,1081,131,167,229,267,265,232,153,214,120,5822,74,5819,5825,5839,62,209,125,126,85,77,2,93,35,38,41,42,94,97,90,96,30,95,91,111,87,86,3,29,127,128,43,44,45,46,89,112])).
% 58.93/59.07 cnf(5862,plain,
% 58.93/59.07 (P13(f3(a1,a2),a1)),
% 58.93/59.07 inference(scs_inference,[],[69,133,5811,181,56,66,188,183,129,1081,131,167,229,267,265,232,153,214,120,5822,5827,74,5819,5825,5839,62,209,125,126,85,77,2,93,35,38,41,42,94,97,90,96,30,95,91,111,87,86,3,29,127,128,43,44,45,46,89,112,109,118,52,19,53,54,51,28])).
% 58.93/59.07 cnf(5863,plain,
% 58.93/59.07 (P13(x58631,x58631)),
% 58.93/59.07 inference(rename_variables,[],[120])).
% 58.93/59.07 cnf(5864,plain,
% 58.93/59.07 (P13(a1,f3(a2,a1))),
% 58.93/59.07 inference(scs_inference,[],[69,133,5811,181,56,66,188,183,129,1081,131,167,229,267,265,232,153,214,120,5822,5827,5863,74,5819,5825,5839,62,209,125,126,85,77,2,93,35,38,41,42,94,97,90,96,30,95,91,111,87,86,3,29,127,128,43,44,45,46,89,112,109,118,52,19,53,54,51,28,27])).
% 58.93/59.07 cnf(5866,plain,
% 58.93/59.07 (~P6(a1,a1,f3(a1,a4),f3(a1,a1))),
% 58.93/59.07 inference(scs_inference,[],[69,133,5811,181,56,66,188,183,129,1081,131,167,229,267,265,232,153,214,120,5822,5827,5863,74,5819,5825,5839,62,209,125,126,85,77,2,93,35,38,41,42,94,97,90,96,30,95,91,111,87,86,3,29,127,128,43,44,45,46,89,112,109,118,52,19,53,54,51,28,27,981])).
% 58.93/59.07 cnf(5868,plain,
% 58.93/59.07 (~P6(f3(a1,a4),a1,f3(a1,a4),f3(a1,a1))),
% 58.93/59.07 inference(scs_inference,[],[69,133,5811,181,56,66,188,183,129,1081,131,167,229,267,265,232,153,214,120,5822,5827,5863,74,5819,5825,5839,62,209,125,126,85,77,2,93,35,38,41,42,94,97,90,96,30,95,91,111,87,86,3,29,127,128,43,44,45,46,89,112,109,118,52,19,53,54,51,28,27,981,1337])).
% 58.93/59.07 cnf(5879,plain,
% 58.93/59.07 (~P1(x58791)+E(x58791,a1)+E(f3(x58791,a4),a4)),
% 58.93/59.07 inference(scs_inference,[],[5803,127])).
% 58.93/59.07 cnf(5882,plain,
% 58.93/59.07 (E(f3(a4,a1),a1)),
% 58.93/59.07 inference(scs_inference,[],[57,125])).
% 58.93/59.07 cnf(5886,plain,
% 58.93/59.07 (P13(a8,a11)),
% 58.93/59.07 inference(scs_inference,[],[5840,57,175,125,77,85])).
% 58.93/59.07 cnf(5892,plain,
% 58.93/59.07 (~P6(f3(a1,a4),f3(a1,a1),f3(a1,a4),f3(a1,a4))),
% 58.93/59.07 inference(scs_inference,[],[67,5851,5868,5795,5840,57,175,265,232,125,77,85,2,47,48,49,50])).
% 58.93/59.07 cnf(5893,plain,
% 58.93/59.07 (~P8(f3(a1,a4),a1,x58931)),
% 58.93/59.07 inference(scs_inference,[],[67,5851,5868,5806,5795,5840,57,175,265,232,209,125,77,85,2,47,48,49,50,36])).
% 58.93/59.07 cnf(5894,plain,
% 58.93/59.07 (~P9(f3(a1,a4),x58941,a1)),
% 58.93/59.07 inference(scs_inference,[],[67,5851,5868,5806,5808,5795,5840,57,175,265,232,209,125,77,85,2,47,48,49,50,36,40])).
% 58.93/59.07 cnf(5896,plain,
% 58.93/59.07 (P13(x58961,x58961)),
% 58.93/59.07 inference(rename_variables,[],[120])).
% 58.93/59.07 cnf(5898,plain,
% 58.93/59.07 (~P10(f3(a2,a1),a1,x58981)),
% 58.93/59.07 inference(scs_inference,[],[67,5799,5851,5868,5806,5808,5795,5840,133,57,175,265,232,120,209,125,77,85,2,47,48,49,50,36,40,93,41])).
% 58.93/59.07 cnf(5899,plain,
% 58.93/59.07 (~P10(x58991,x58991,x58992)),
% 58.93/59.07 inference(rename_variables,[],[133])).
% 58.93/59.07 cnf(5901,plain,
% 58.93/59.07 (P13(x59011,x59011)),
% 58.93/59.07 inference(rename_variables,[],[120])).
% 58.93/59.07 cnf(5910,plain,
% 58.93/59.07 (~P12(a1,f3(a2,a1))),
% 58.93/59.07 inference(scs_inference,[],[67,5799,5851,5868,5806,5808,5801,5795,5840,133,57,175,64,265,232,120,5896,5901,74,62,209,125,77,85,2,47,48,49,50,36,40,93,41,96,97,94,95,91])).
% 58.93/59.07 cnf(5911,plain,
% 58.93/59.07 (~P12(x59111,x59111)),
% 58.93/59.07 inference(rename_variables,[],[74])).
% 58.93/59.07 cnf(5913,plain,
% 58.93/59.07 (~P9(f3(a2,a1),x59131,a1)),
% 58.93/59.07 inference(scs_inference,[],[67,5799,5851,5868,5806,5808,5801,5795,5840,133,57,131,175,64,265,232,120,5896,5901,74,62,209,125,77,85,2,47,48,49,50,36,40,93,41,96,97,94,95,91,38])).
% 58.93/59.07 cnf(5915,plain,
% 58.93/59.07 (~P12(a1,f3(a1,a2))),
% 58.93/59.07 inference(scs_inference,[],[67,5799,5851,5868,5806,5808,5801,5862,5795,5840,133,57,131,175,64,265,232,120,5896,5901,74,5911,62,209,125,77,85,2,47,48,49,50,36,40,93,41,96,97,94,95,91,38,90])).
% 58.93/59.07 cnf(5916,plain,
% 58.93/59.07 (~P12(x59161,x59161)),
% 58.93/59.07 inference(rename_variables,[],[74])).
% 58.93/59.07 cnf(5918,plain,
% 58.93/59.07 (~P8(f3(a2,a1),a1,x59181)),
% 58.93/59.07 inference(scs_inference,[],[67,5799,5851,5868,5806,5808,5801,5862,5795,5840,133,57,129,131,175,64,265,232,120,5896,5901,74,5911,62,209,125,77,85,2,47,48,49,50,36,40,93,41,96,97,94,95,91,38,90,35])).
% 58.93/59.07 cnf(5920,plain,
% 58.93/59.07 (~P10(a1,f3(a2,a1),x59201)),
% 58.93/59.07 inference(scs_inference,[],[67,5799,5851,5868,5806,5808,5801,5862,5795,5840,133,5899,57,129,131,175,64,265,232,120,5896,5901,74,5911,62,209,125,77,85,2,47,48,49,50,36,40,93,41,96,97,94,95,91,38,90,35,42])).
% 58.93/59.07 cnf(5928,plain,
% 58.93/59.07 (E(a1,f3(a2,a1))),
% 58.93/59.07 inference(scs_inference,[],[67,5799,5851,5868,5806,5808,5801,5862,5864,5795,5840,133,5899,57,129,220,131,175,64,217,265,232,120,5896,5901,74,5911,5916,62,209,125,77,85,2,47,48,49,50,36,40,93,41,96,97,94,95,91,38,90,35,42,30,111,92,87])).
% 58.93/59.07 cnf(5930,plain,
% 58.93/59.07 (~E(a4,f3(a2,a1))),
% 58.93/59.07 inference(scs_inference,[],[67,5799,5803,5851,5868,5806,5808,5801,5862,5864,5795,5840,133,5899,57,129,220,131,175,64,217,265,232,120,5896,5901,74,5911,5916,62,209,125,77,85,2,47,48,49,50,36,40,93,41,96,97,94,95,91,38,90,35,42,30,111,92,87,3])).
% 58.93/59.07 cnf(5931,plain,
% 58.93/59.07 (~P12(f3(a2,a1),f3(a1,a4))),
% 58.93/59.07 inference(scs_inference,[],[67,5799,5803,5818,5851,5868,5806,5808,5801,5862,5864,5795,5840,133,5899,57,129,220,131,175,64,217,265,232,120,5896,5901,74,5911,5916,62,209,125,77,85,2,47,48,49,50,36,40,93,41,96,97,94,95,91,38,90,35,42,30,111,92,87,3,29])).
% 58.93/59.07 cnf(5934,plain,
% 58.93/59.07 (~P7(f5(a9,a10,x59341,a8),x59341,a8)),
% 58.93/59.07 inference(scs_inference,[],[67,5799,5803,5818,5851,5868,5806,5808,5801,5862,5864,5795,5840,133,5899,57,129,220,131,175,64,217,265,232,120,5896,5901,74,5911,5916,62,209,125,77,85,2,47,48,49,50,36,40,93,41,96,97,94,95,91,38,90,35,42,30,111,92,87,3,29,113,119])).
% 58.93/59.07 cnf(5940,plain,
% 58.93/59.07 (~P6(f3(a1,a1),a1,f3(a1,a1),f3(a1,a1))),
% 58.93/59.07 inference(scs_inference,[],[67,5799,5803,5818,5851,5868,5806,5808,5801,5862,5864,5795,5840,133,5899,57,129,220,131,175,64,217,265,232,120,5896,5901,74,5911,5916,62,209,125,77,85,2,47,48,49,50,36,40,93,41,96,97,94,95,91,38,90,35,42,30,111,92,87,3,29,113,119,3479,3756,4358])).
% 58.93/59.07 cnf(5950,plain,
% 58.93/59.07 (~P6(a1,f3(a1,a1),f3(a1,a1),f3(a1,a1))),
% 58.93/59.07 inference(scs_inference,[],[67,5799,5803,5818,5851,5868,5806,5808,5801,5862,5864,5795,5840,133,5899,57,129,220,131,175,64,217,265,232,120,5896,5901,74,5911,5916,62,209,125,77,85,2,47,48,49,50,36,40,93,41,96,97,94,95,91,38,90,35,42,30,111,92,87,3,29,113,119,3479,3756,4358,1849,2297,1074,1075,981,2820])).
% 58.93/59.07 cnf(5952,plain,
% 58.93/59.07 (P13(a9,f5(a9,a10,x59521,a8))),
% 58.93/59.07 inference(scs_inference,[],[67,5799,5803,5818,5851,5868,5806,5808,5801,5862,5864,5795,5840,133,5899,57,129,220,131,175,64,217,265,232,120,5896,5901,74,5911,5916,62,209,125,77,85,2,47,48,49,50,36,40,93,41,96,97,94,95,91,38,90,35,42,30,111,92,87,3,29,113,119,3479,3756,4358,1849,2297,1074,1075,981,2820,102])).
% 58.93/59.07 cnf(5954,plain,
% 58.93/59.07 (P13(f5(a9,a10,x59541,a8),a10)),
% 58.93/59.07 inference(scs_inference,[],[67,5799,5803,5818,5851,5868,5806,5808,5801,5862,5864,5795,5840,133,5899,57,129,220,131,175,64,217,265,232,120,5896,5901,74,5911,5916,62,209,125,77,85,2,47,48,49,50,36,40,93,41,96,97,94,95,91,38,90,35,42,30,111,92,87,3,29,113,119,3479,3756,4358,1849,2297,1074,1075,981,2820,102,103])).
% 58.93/59.07 cnf(5956,plain,
% 58.93/59.07 (E(f3(a4,a4),a4)),
% 58.93/59.07 inference(scs_inference,[],[67,5799,5803,5818,5851,5868,5806,5808,5801,5862,5864,5795,5840,133,5899,57,129,220,131,175,64,217,265,232,120,5896,5901,74,5911,5916,62,209,125,77,85,2,47,48,49,50,36,40,93,41,96,97,94,95,91,38,90,35,42,30,111,92,87,3,29,113,119,3479,3756,4358,1849,2297,1074,1075,981,2820,102,103,5879])).
% 58.93/59.07 cnf(5958,plain,
% 58.93/59.07 (E(f3(a1,a4),f3(a2,a1))+P12(f3(a1,a4),f3(a2,a1))),
% 58.93/59.07 inference(scs_inference,[],[67,5799,5803,5818,5851,5868,5806,5808,5801,5862,5864,5795,5840,133,5899,57,129,220,131,175,64,217,265,232,120,5896,5901,74,5911,5916,62,209,125,77,85,2,47,48,49,50,36,40,93,41,96,97,94,95,91,38,90,35,42,30,111,92,87,3,29,113,119,3479,3756,4358,1849,2297,1074,1075,981,2820,102,103,5879,78])).
% 58.93/59.07 cnf(5961,plain,
% 58.93/59.07 (P5(f3(a1,a4),f3(a1,a4),a1,f3(a2,a1))),
% 58.93/59.07 inference(scs_inference,[],[67,5799,5803,5818,5851,5868,5806,5808,5801,5862,5864,5795,5840,133,5899,57,1125,1138,129,220,131,175,64,217,265,232,120,5896,5901,74,5911,5916,62,209,125,77,85,2,47,48,49,50,36,40,93,41,96,97,94,95,91,38,90,35,42,30,111,92,87,3,29,113,119,3479,3756,4358,1849,2297,1074,1075,981,2820,102,103,5879,78,22,25])).
% 58.93/59.07 cnf(5963,plain,
% 58.93/59.07 (P4(a1,a1,f3(a1,a1),a1)),
% 58.93/59.07 inference(scs_inference,[],[67,5799,5803,5818,5851,5868,5806,5808,5801,5862,5864,5795,5840,133,5899,57,1125,1138,1082,129,220,131,175,64,217,265,232,120,5896,5901,74,5911,5916,62,209,125,77,85,2,47,48,49,50,36,40,93,41,96,97,94,95,91,38,90,35,42,30,111,92,87,3,29,113,119,3479,3756,4358,1849,2297,1074,1075,981,2820,102,103,5879,78,22,25,23,691])).
% 58.93/59.07 cnf(5986,plain,
% 58.93/59.07 (E(f3(a1,a4),f3(a2,a1))),
% 58.93/59.07 inference(scs_inference,[],[5910,230,5958,29])).
% 58.93/59.07 cnf(5987,plain,
% 58.93/59.07 (P13(f7(a1,a1,a1,a1),a1)),
% 58.93/59.07 inference(scs_inference,[],[5963,366])).
% 58.93/59.07 cnf(6003,plain,
% 58.93/59.07 (P13(a8,a10)),
% 58.93/59.07 inference(scs_inference,[],[5963,5986,5892,179,366,3479,1849,3756,1637,981,77,2820,85])).
% 58.93/59.07 cnf(6007,plain,
% 58.93/59.07 (~P8(f3(a2,a1),f3(a4,a1),x60071)),
% 58.93/59.07 inference(scs_inference,[],[5950,5963,5986,5892,5918,5930,5882,179,366,3479,1849,3756,1637,981,77,2820,85,2,47,36])).
% 58.93/59.07 cnf(6011,plain,
% 58.93/59.07 (P13(x60111,x60111)),
% 58.93/59.07 inference(rename_variables,[],[120])).
% 58.93/59.07 cnf(6013,plain,
% 58.93/59.07 (~P6(a1,f3(a1,a1),a1,f3(a1,a1))),
% 58.93/59.07 inference(scs_inference,[],[5950,5940,5963,5986,5892,5918,5930,5882,179,265,120,209,366,3479,1849,3756,1637,981,77,2820,85,2,47,36,48,50,95,49])).
% 58.93/59.07 cnf(6016,plain,
% 58.93/59.07 (~P9(f3(a2,a1),x60161,f3(a4,a1))),
% 58.93/59.07 inference(scs_inference,[],[5950,5940,5963,5986,5892,5913,5918,5930,5882,179,63,265,120,62,209,366,3479,1849,3756,1637,981,77,2820,85,2,47,36,48,50,95,49,97,40])).
% 58.93/59.07 cnf(6018,plain,
% 58.93/59.07 (P13(x60181,x60181)),
% 58.93/59.07 inference(rename_variables,[],[120])).
% 58.93/59.07 cnf(6033,plain,
% 58.93/59.07 (~P10(f3(a1,a4),a1,x60331)),
% 58.93/59.07 inference(scs_inference,[],[5886,5950,5940,5963,5986,5931,5956,5892,5915,5898,5913,5918,5930,5882,5864,129,179,131,64,267,63,265,120,6011,6018,62,209,366,3479,1849,3756,1637,981,77,2820,85,2,47,36,48,50,95,49,97,40,93,90,91,94,38,96,35,41])).
% 58.93/59.07 cnf(6040,plain,
% 58.93/59.07 (~E(f3(a2,a1),a2)),
% 58.93/59.07 inference(scs_inference,[],[5886,5950,5940,5963,5986,5928,5931,5956,5892,5915,5961,5898,5913,5918,5920,5930,5831,5952,5882,5864,65,129,179,131,64,267,63,217,265,120,6011,6018,62,209,366,3479,1849,3756,1637,981,77,2820,85,2,47,36,48,50,95,49,97,40,93,90,91,94,38,96,35,41,42,111,92,28,3])).
% 58.93/59.07 cnf(6065,plain,
% 58.93/59.07 (~P6(f3(a1,a1),f3(a1,a1),f3(a1,a1),f3(a1,a1))),
% 58.93/59.07 inference(scs_inference,[],[6013,511])).
% 58.93/59.07 cnf(6081,plain,
% 58.93/59.07 (P13(a11,a10)),
% 58.93/59.07 inference(scs_inference,[],[6013,5842,64,525,872,2619,77,85])).
% 58.93/59.07 cnf(6085,plain,
% 58.93/59.07 (P13(x60851,x60851)),
% 58.93/59.07 inference(rename_variables,[],[120])).
% 58.93/59.07 cnf(6088,plain,
% 58.93/59.07 (~P12(x60881,x60881)),
% 58.93/59.07 inference(rename_variables,[],[74])).
% 58.93/59.07 cnf(6091,plain,
% 58.93/59.07 (P13(x60911,x60911)),
% 58.93/59.07 inference(rename_variables,[],[120])).
% 58.93/59.07 cnf(6095,plain,
% 58.93/59.07 (~P12(f3(a4,a1),f3(a2,a1))),
% 58.93/59.07 inference(scs_inference,[],[6003,6013,6007,5987,6040,5842,5801,64,63,120,6085,74,525,872,2619,77,85,2,93,90,94,97,95])).
% 58.93/59.07 cnf(6096,plain,
% 58.93/59.07 (~P8(f3(a2,a1),f3(a4,a1),x60961)),
% 58.93/59.07 inference(rename_variables,[],[6007])).
% 58.93/59.07 cnf(6103,plain,
% 58.93/59.07 (~P6(a1,f3(a1,a1),f3(a1,a2),f3(a1,a1))),
% 58.93/59.07 inference(scs_inference,[],[6003,6013,6007,5987,5894,6040,5954,5797,5842,5801,64,63,120,6085,74,6088,525,872,2619,77,85,2,93,90,94,97,95,40,47,91,49])).
% 58.93/59.07 cnf(6107,plain,
% 58.93/59.07 (P13(x61071,x61071)),
% 58.93/59.07 inference(rename_variables,[],[120])).
% 58.93/59.07 cnf(6121,plain,
% 58.93/59.07 (P13(f7(a1,a1,a1,a1),f3(a2,a1))),
% 58.93/59.07 inference(scs_inference,[],[6003,6065,6013,5866,6007,6096,6016,5987,6033,5893,5894,6040,5954,73,5797,5842,218,5934,5928,5801,179,64,63,265,232,120,6085,6091,74,6088,525,872,2619,77,85,2,93,90,94,97,95,40,47,91,49,50,36,96,48,35,38,41,30,42,111,87,20,28])).
% 58.93/59.07 cnf(6122,plain,
% 58.93/59.07 (~E(f3(a1,a4),a4)),
% 58.93/59.07 inference(scs_inference,[],[6003,6065,6013,5866,6007,6096,6016,5987,6033,5893,5894,6040,5837,5954,73,5797,5842,218,5934,5928,5801,179,64,63,265,232,120,6085,6091,74,6088,525,872,2619,77,85,2,93,90,94,97,95,40,47,91,49,50,36,96,48,35,38,41,30,42,111,87,20,28,3])).
% 58.93/59.07 cnf(6126,plain,
% 58.93/59.07 (~P13(a8,a9)),
% 58.93/59.07 inference(scs_inference,[],[75,6003,6065,6013,5866,6007,6096,6016,5987,6033,5893,5894,6040,5837,5954,73,5829,5797,5842,218,5934,5928,5801,5799,179,64,63,265,232,120,6085,6091,6107,74,6088,525,872,2619,77,85,2,93,90,94,97,95,40,47,91,49,50,36,96,48,35,38,41,30,42,111,87,20,28,3,27,29,107])).
% 58.93/59.07 cnf(6136,plain,
% 58.93/59.07 (P7(f5(a8,a10,a9,x61361),a8,a10)),
% 58.93/59.07 inference(scs_inference,[],[75,6003,6065,6013,5866,6007,6096,6016,5987,6033,5893,5894,6040,5837,5954,73,5829,5797,5842,218,5934,5928,5801,5799,179,64,63,265,232,120,6085,6091,6107,74,6088,525,872,2619,77,85,2,93,90,94,97,95,40,47,91,49,50,36,96,48,35,38,41,30,42,111,87,20,28,3,27,29,107,5792,571,728,4904,113])).
% 58.93/59.07 cnf(6177,plain,
% 58.93/59.07 (E(f3(a2,a1),f3(a4,a1))),
% 58.93/59.07 inference(scs_inference,[],[6081,6121,6095,6103,6122,6136,6016,5956,63,120,872,525,2619,77,102,85,2,94,96,78])).
% 58.93/59.07 cnf(6227,plain,
% 58.93/59.07 ($false),
% 58.93/59.07 inference(scs_inference,[],[6177,6126,62,77,85]),
% 58.93/59.07 ['proof']).
% 58.93/59.07 % SZS output end Proof
% 58.93/59.07 % Total time :58.493068s
%------------------------------------------------------------------------------