%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : NUM334+1 : TPTP v8.2.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n024.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 12:23:52 EDT 2024
% Result : Theorem 60.39s 60.43s
% Output : CNFRefutation 60.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NUM334+1 : TPTP v8.2.0. Released v3.1.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n024.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Sat Jun 22 23:53:24 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.52/0.56 start to proof:theBenchmark
% 60.35/60.42 %-------------------------------------------
% 60.35/60.42 % File :CSE---1.7
% 60.35/60.42 % Problem :theBenchmark
% 60.35/60.42 % Transform :cnf
% 60.35/60.42 % Format :tptp:raw
% 60.35/60.42 % Command :java -jar mcs_scs.jar %d %s
% 60.35/60.42
% 60.35/60.42 % Result :Theorem 59.760000s
% 60.35/60.42 % Output :CNFRefutation 59.760000s
% 60.35/60.42 %-------------------------------------------
% 60.39/60.43 %------------------------------------------------------------------------------
% 60.39/60.43 % File : NUM334+1 : TPTP v8.2.0. Released v3.1.0.
% 60.39/60.43 % Domain : Number Theory (RDN arithmetic)
% 60.39/60.43 % Problem : 7 - 5 = 2
% 60.39/60.43 % Version : Especial.
% 60.39/60.43 % English :
% 60.39/60.43
% 60.39/60.43 % Refs :
% 60.39/60.43 % Source : [TPTP]
% 60.39/60.43 % Names :
% 60.39/60.43
% 60.39/60.43 % Status : Theorem
% 60.39/60.43 % Rating : 0.47 v8.2.0, 0.50 v8.1.0, 0.47 v7.4.0, 0.50 v7.3.0, 0.45 v7.2.0, 0.41 v7.1.0, 0.35 v7.0.0, 0.43 v6.4.0, 0.54 v6.3.0, 0.42 v6.2.0, 0.44 v6.1.0, 0.53 v6.0.0, 0.48 v5.5.0, 0.56 v5.4.0, 0.57 v5.3.0, 0.63 v5.2.0, 0.50 v5.1.0, 0.48 v5.0.0, 0.58 v4.1.0, 0.61 v4.0.1, 0.65 v4.0.0, 0.62 v3.7.0, 0.65 v3.5.0, 0.74 v3.3.0, 0.71 v3.2.0, 0.82 v3.1.0
% 60.39/60.43 % Syntax : Number of formulae : 402 ( 375 unt; 0 def)
% 60.39/60.43 % Number of atoms : 473 ( 5 equ)
% 60.39/60.43 % Maximal formula atoms : 8 ( 1 avg)
% 60.39/60.43 % Number of connectives : 73 ( 2 ~; 1 |; 43 &)
% 60.39/60.43 % ( 3 <=>; 24 =>; 0 <=; 0 <~>)
% 60.39/60.43 % Maximal formula depth : 19 ( 1 avg)
% 60.39/60.43 % Maximal term depth : 5 ( 2 avg)
% 60.39/60.43 % Number of predicates : 11 ( 10 usr; 0 prp; 1-4 aty)
% 60.39/60.43 % Number of functors : 260 ( 260 usr; 256 con; 0-2 aty)
% 60.39/60.43 % Number of variables : 121 ( 121 !; 0 ?)
% 60.39/60.43 % SPC : FOF_THM_RFO_SEQ
% 60.39/60.43
% 60.39/60.43 % Comments :
% 60.39/60.43 %------------------------------------------------------------------------------
% 60.39/60.43 %----Include axioms for RDN arithmetic
% 60.39/60.43 include('Axioms/NUM005+0.ax').
% 60.39/60.43 include('Axioms/NUM005+1.ax').
% 60.39/60.43 include('Axioms/NUM005+2.ax').
% 60.39/60.43 %------------------------------------------------------------------------------
% 60.39/60.43 fof(diff_n7_n5_n2,conjecture,
% 60.39/60.43 difference(n7,n5,n2) ).
% 60.39/60.43
% 60.39/60.43 %------------------------------------------------------------------------------
% 60.39/60.43 %-------------------------------------------
% 60.39/60.43 % Proof found
% 60.39/60.43 % SZS status Theorem for theBenchmark
% 60.39/60.43 % SZS output start Proof
% 60.39/60.43 %ClaNum:439(EqnAxiom:32)
% 60.39/60.43 %VarNum:271(SingletonVarNum:132)
% 60.39/60.43 %MaxLitNum:8
% 60.39/60.43 %MaxfuncDepth:4
% 60.39/60.43 %SharedTerms:967
% 60.39/60.43 %goalClause: 407
% 60.39/60.43 %singleGoalClaCount:1
% 60.39/60.43 [407]~P3(a87,a65,a4)
% 60.39/60.43 [33]P1(f3(a1))
% 60.39/60.43 [34]P1(f3(a4))
% 60.39/60.43 [35]P1(f3(a43))
% 60.39/60.43 [36]P1(f3(a54))
% 60.39/60.43 [37]P1(f3(a65))
% 60.39/60.43 [38]P1(f3(a76))
% 60.39/60.43 [39]P1(f3(a87))
% 60.39/60.43 [40]P1(f3(a98))
% 60.39/60.43 [41]P1(f3(a109))
% 60.39/60.43 [42]P8(f3(a2),f3(a1))
% 60.39/60.43 [43]P8(f3(a1),f3(a4))
% 60.39/60.43 [44]P8(f3(a4),f3(a43))
% 60.39/60.44 [45]P8(f3(a43),f3(a54))
% 60.39/60.44 [46]P8(f3(a54),f3(a65))
% 60.39/60.44 [47]P8(f3(a65),f3(a76))
% 60.39/60.44 [48]P8(f3(a76),f3(a87))
% 60.39/60.44 [49]P8(f3(a87),f3(a98))
% 60.39/60.44 [50]P8(f3(a98),f3(a109))
% 60.39/60.44 [307]P2(f3(a2),f3(a2),f3(a2),f3(a2))
% 60.39/60.44 [308]P2(f3(a2),f3(a1),f3(a1),f3(a2))
% 60.39/60.44 [309]P2(f3(a2),f3(a4),f3(a4),f3(a2))
% 60.39/60.44 [310]P2(f3(a2),f3(a43),f3(a43),f3(a2))
% 60.39/60.44 [311]P2(f3(a2),f3(a54),f3(a54),f3(a2))
% 60.39/60.44 [312]P2(f3(a2),f3(a65),f3(a65),f3(a2))
% 60.39/60.44 [313]P2(f3(a2),f3(a76),f3(a76),f3(a2))
% 60.39/60.44 [314]P2(f3(a2),f3(a87),f3(a87),f3(a2))
% 60.39/60.44 [315]P2(f3(a2),f3(a98),f3(a98),f3(a2))
% 60.39/60.44 [316]P2(f3(a2),f3(a109),f3(a109),f3(a2))
% 60.39/60.44 [317]P2(f3(a1),f3(a2),f3(a1),f3(a2))
% 60.39/60.44 [318]P2(f3(a1),f3(a1),f3(a4),f3(a2))
% 60.39/60.44 [319]P2(f3(a1),f3(a4),f3(a43),f3(a2))
% 60.39/60.44 [320]P2(f3(a1),f3(a43),f3(a54),f3(a2))
% 60.39/60.44 [321]P2(f3(a1),f3(a54),f3(a65),f3(a2))
% 60.39/60.44 [322]P2(f3(a1),f3(a65),f3(a76),f3(a2))
% 60.39/60.44 [323]P2(f3(a1),f3(a76),f3(a87),f3(a2))
% 60.39/60.44 [324]P2(f3(a1),f3(a87),f3(a98),f3(a2))
% 60.39/60.44 [325]P2(f3(a1),f3(a98),f3(a109),f3(a2))
% 60.39/60.44 [326]P2(f3(a1),f3(a109),f3(a2),f3(a1))
% 60.39/60.44 [327]P2(f3(a4),f3(a2),f3(a4),f3(a2))
% 60.39/60.44 [328]P2(f3(a4),f3(a1),f3(a43),f3(a2))
% 60.39/60.44 [329]P2(f3(a4),f3(a4),f3(a54),f3(a2))
% 60.39/60.44 [330]P2(f3(a4),f3(a43),f3(a65),f3(a2))
% 60.39/60.44 [331]P2(f3(a4),f3(a54),f3(a76),f3(a2))
% 60.39/60.44 [332]P2(f3(a4),f3(a65),f3(a87),f3(a2))
% 60.39/60.44 [333]P2(f3(a4),f3(a76),f3(a98),f3(a2))
% 60.39/60.44 [334]P2(f3(a4),f3(a87),f3(a109),f3(a2))
% 60.39/60.44 [335]P2(f3(a4),f3(a98),f3(a2),f3(a1))
% 60.39/60.44 [336]P2(f3(a4),f3(a109),f3(a1),f3(a1))
% 60.39/60.44 [337]P2(f3(a43),f3(a2),f3(a43),f3(a2))
% 60.39/60.44 [338]P2(f3(a43),f3(a1),f3(a54),f3(a2))
% 60.39/60.44 [339]P2(f3(a43),f3(a4),f3(a65),f3(a2))
% 60.39/60.44 [340]P2(f3(a43),f3(a43),f3(a76),f3(a2))
% 60.39/60.44 [341]P2(f3(a43),f3(a54),f3(a87),f3(a2))
% 60.39/60.44 [342]P2(f3(a43),f3(a65),f3(a98),f3(a2))
% 60.39/60.44 [343]P2(f3(a43),f3(a76),f3(a109),f3(a2))
% 60.39/60.44 [344]P2(f3(a43),f3(a87),f3(a2),f3(a1))
% 60.39/60.44 [345]P2(f3(a43),f3(a98),f3(a1),f3(a1))
% 60.39/60.44 [346]P2(f3(a43),f3(a109),f3(a4),f3(a1))
% 60.39/60.44 [347]P2(f3(a54),f3(a2),f3(a54),f3(a2))
% 60.39/60.44 [348]P2(f3(a54),f3(a1),f3(a65),f3(a2))
% 60.39/60.44 [349]P2(f3(a54),f3(a4),f3(a76),f3(a2))
% 60.39/60.44 [350]P2(f3(a54),f3(a43),f3(a87),f3(a2))
% 60.39/60.44 [351]P2(f3(a54),f3(a54),f3(a98),f3(a2))
% 60.39/60.44 [352]P2(f3(a54),f3(a65),f3(a109),f3(a2))
% 60.39/60.44 [353]P2(f3(a54),f3(a76),f3(a2),f3(a1))
% 60.39/60.44 [354]P2(f3(a54),f3(a87),f3(a1),f3(a1))
% 60.39/60.44 [355]P2(f3(a54),f3(a98),f3(a4),f3(a1))
% 60.39/60.44 [356]P2(f3(a54),f3(a109),f3(a43),f3(a1))
% 60.39/60.44 [357]P2(f3(a65),f3(a2),f3(a65),f3(a2))
% 60.39/60.44 [358]P2(f3(a65),f3(a1),f3(a76),f3(a2))
% 60.39/60.44 [359]P2(f3(a65),f3(a4),f3(a87),f3(a2))
% 60.39/60.44 [360]P2(f3(a65),f3(a43),f3(a98),f3(a2))
% 60.39/60.44 [361]P2(f3(a65),f3(a54),f3(a109),f3(a2))
% 60.39/60.44 [362]P2(f3(a65),f3(a65),f3(a2),f3(a1))
% 60.39/60.44 [363]P2(f3(a65),f3(a76),f3(a1),f3(a1))
% 60.39/60.44 [364]P2(f3(a65),f3(a87),f3(a4),f3(a1))
% 60.39/60.44 [365]P2(f3(a65),f3(a98),f3(a43),f3(a1))
% 60.39/60.44 [366]P2(f3(a65),f3(a109),f3(a54),f3(a1))
% 60.39/60.44 [367]P2(f3(a76),f3(a2),f3(a76),f3(a2))
% 60.39/60.44 [368]P2(f3(a76),f3(a1),f3(a87),f3(a2))
% 60.39/60.44 [369]P2(f3(a76),f3(a4),f3(a98),f3(a2))
% 60.39/60.44 [370]P2(f3(a76),f3(a43),f3(a109),f3(a2))
% 60.39/60.44 [371]P2(f3(a76),f3(a54),f3(a2),f3(a1))
% 60.39/60.44 [372]P2(f3(a76),f3(a65),f3(a1),f3(a1))
% 60.39/60.44 [373]P2(f3(a76),f3(a76),f3(a4),f3(a1))
% 60.39/60.44 [374]P2(f3(a76),f3(a87),f3(a43),f3(a1))
% 60.39/60.44 [375]P2(f3(a76),f3(a98),f3(a54),f3(a1))
% 60.39/60.44 [376]P2(f3(a76),f3(a109),f3(a65),f3(a1))
% 60.39/60.44 [377]P2(f3(a87),f3(a2),f3(a87),f3(a2))
% 60.39/60.44 [378]P2(f3(a87),f3(a1),f3(a98),f3(a2))
% 60.39/60.44 [379]P2(f3(a87),f3(a4),f3(a109),f3(a2))
% 60.39/60.44 [380]P2(f3(a87),f3(a43),f3(a2),f3(a1))
% 60.39/60.44 [381]P2(f3(a87),f3(a54),f3(a1),f3(a1))
% 60.39/60.44 [382]P2(f3(a87),f3(a65),f3(a4),f3(a1))
% 60.39/60.44 [383]P2(f3(a87),f3(a76),f3(a43),f3(a1))
% 60.39/60.44 [384]P2(f3(a87),f3(a87),f3(a54),f3(a1))
% 60.39/60.44 [385]P2(f3(a87),f3(a98),f3(a65),f3(a1))
% 60.39/60.44 [386]P2(f3(a87),f3(a109),f3(a76),f3(a1))
% 60.39/60.44 [387]P2(f3(a98),f3(a2),f3(a98),f3(a2))
% 60.39/60.44 [388]P2(f3(a98),f3(a1),f3(a109),f3(a2))
% 60.39/60.44 [389]P2(f3(a98),f3(a4),f3(a2),f3(a1))
% 60.39/60.44 [390]P2(f3(a98),f3(a43),f3(a1),f3(a1))
% 60.39/60.44 [391]P2(f3(a98),f3(a54),f3(a4),f3(a1))
% 60.39/60.44 [392]P2(f3(a98),f3(a65),f3(a43),f3(a1))
% 60.39/60.44 [393]P2(f3(a98),f3(a76),f3(a54),f3(a1))
% 60.39/60.44 [394]P2(f3(a98),f3(a87),f3(a65),f3(a1))
% 60.39/60.44 [395]P2(f3(a98),f3(a98),f3(a76),f3(a1))
% 60.39/60.44 [396]P2(f3(a98),f3(a109),f3(a87),f3(a1))
% 60.39/60.44 [397]P2(f3(a109),f3(a2),f3(a109),f3(a2))
% 60.39/60.44 [398]P2(f3(a109),f3(a1),f3(a2),f3(a1))
% 60.39/60.44 [399]P2(f3(a109),f3(a4),f3(a1),f3(a1))
% 60.39/60.44 [400]P2(f3(a109),f3(a43),f3(a4),f3(a1))
% 60.39/60.44 [401]P2(f3(a109),f3(a54),f3(a43),f3(a1))
% 60.39/60.44 [402]P2(f3(a109),f3(a65),f3(a54),f3(a1))
% 60.39/60.44 [403]P2(f3(a109),f3(a76),f3(a65),f3(a1))
% 60.39/60.44 [404]P2(f3(a109),f3(a87),f3(a76),f3(a1))
% 60.39/60.44 [405]P2(f3(a109),f3(a98),f3(a87),f3(a1))
% 60.39/60.44 [406]P2(f3(a109),f3(a109),f3(a98),f3(a1))
% 60.39/60.44 [51]P9(a2,f120(f3(a2)))
% 60.39/60.44 [52]P9(a1,f120(f3(a1)))
% 60.39/60.44 [53]P9(a4,f120(f3(a4)))
% 60.39/60.44 [54]P9(a43,f120(f3(a43)))
% 60.39/60.44 [55]P9(a54,f120(f3(a54)))
% 60.39/60.44 [56]P9(a65,f120(f3(a65)))
% 60.39/60.44 [57]P9(a76,f120(f3(a76)))
% 60.39/60.44 [58]P9(a87,f120(f3(a87)))
% 60.39/60.44 [59]P9(a98,f120(f3(a98)))
% 60.39/60.44 [60]P9(a109,f120(f3(a109)))
% 60.39/60.44 [61]P9(a121,f132(f3(a1)))
% 60.39/60.44 [62]P9(a133,f132(f3(a4)))
% 60.39/60.44 [63]P9(a173,f132(f3(a43)))
% 60.39/60.44 [64]P9(a184,f132(f3(a54)))
% 60.39/60.44 [65]P9(a195,f132(f3(a65)))
% 60.39/60.44 [66]P9(a206,f132(f3(a76)))
% 60.39/60.44 [67]P9(a217,f132(f3(a87)))
% 60.39/60.44 [68]P9(a228,f132(f3(a98)))
% 60.39/60.44 [69]P9(a239,f132(f3(a109)))
% 60.39/60.44 [70]P9(a5,f120(f250(f3(a2),f3(a1))))
% 60.39/60.44 [71]P9(a6,f120(f250(f3(a1),f3(a1))))
% 60.39/60.44 [72]P9(a17,f120(f250(f3(a4),f3(a1))))
% 60.39/60.44 [73]P9(a28,f120(f250(f3(a43),f3(a1))))
% 60.39/60.44 [74]P9(a37,f120(f250(f3(a54),f3(a1))))
% 60.39/60.44 [75]P9(a38,f120(f250(f3(a65),f3(a1))))
% 60.39/60.44 [76]P9(a39,f120(f250(f3(a76),f3(a1))))
% 60.39/60.44 [77]P9(a40,f120(f250(f3(a87),f3(a1))))
% 60.39/60.44 [78]P9(a41,f120(f250(f3(a98),f3(a1))))
% 60.39/60.44 [79]P9(a42,f120(f250(f3(a109),f3(a1))))
% 60.39/60.44 [80]P9(a44,f120(f250(f3(a2),f3(a4))))
% 60.39/60.44 [81]P9(a45,f120(f250(f3(a1),f3(a4))))
% 60.39/60.44 [82]P9(a46,f120(f250(f3(a4),f3(a4))))
% 60.39/60.44 [83]P9(a47,f120(f250(f3(a43),f3(a4))))
% 60.39/60.44 [84]P9(a48,f120(f250(f3(a54),f3(a4))))
% 60.39/60.44 [85]P9(a49,f120(f250(f3(a65),f3(a4))))
% 60.39/60.44 [86]P9(a50,f120(f250(f3(a76),f3(a4))))
% 60.39/60.44 [87]P9(a51,f120(f250(f3(a87),f3(a4))))
% 60.39/60.44 [88]P9(a52,f120(f250(f3(a98),f3(a4))))
% 60.39/60.44 [89]P9(a53,f120(f250(f3(a109),f3(a4))))
% 60.39/60.44 [90]P9(a55,f120(f250(f3(a2),f3(a43))))
% 60.39/60.44 [91]P9(a56,f120(f250(f3(a1),f3(a43))))
% 60.39/60.44 [92]P9(a57,f120(f250(f3(a4),f3(a43))))
% 60.39/60.44 [93]P9(a58,f120(f250(f3(a43),f3(a43))))
% 60.39/60.44 [94]P9(a59,f120(f250(f3(a54),f3(a43))))
% 60.39/60.44 [95]P9(a60,f120(f250(f3(a65),f3(a43))))
% 60.39/60.44 [96]P9(a61,f120(f250(f3(a76),f3(a43))))
% 60.39/60.44 [97]P9(a62,f120(f250(f3(a87),f3(a43))))
% 60.39/60.44 [98]P9(a63,f120(f250(f3(a98),f3(a43))))
% 60.39/60.44 [99]P9(a64,f120(f250(f3(a109),f3(a43))))
% 60.39/60.44 [100]P9(a66,f120(f250(f3(a2),f3(a54))))
% 60.39/60.44 [101]P9(a67,f120(f250(f3(a1),f3(a54))))
% 60.39/60.44 [102]P9(a68,f120(f250(f3(a4),f3(a54))))
% 60.39/60.44 [103]P9(a69,f120(f250(f3(a43),f3(a54))))
% 60.39/60.44 [104]P9(a70,f120(f250(f3(a54),f3(a54))))
% 60.39/60.44 [105]P9(a71,f120(f250(f3(a65),f3(a54))))
% 60.39/60.44 [106]P9(a72,f120(f250(f3(a76),f3(a54))))
% 60.39/60.44 [107]P9(a73,f120(f250(f3(a87),f3(a54))))
% 60.39/60.44 [108]P9(a74,f120(f250(f3(a98),f3(a54))))
% 60.39/60.44 [109]P9(a75,f120(f250(f3(a109),f3(a54))))
% 60.39/60.44 [110]P9(a77,f120(f250(f3(a2),f3(a65))))
% 60.39/60.44 [111]P9(a78,f120(f250(f3(a1),f3(a65))))
% 60.39/60.44 [112]P9(a79,f120(f250(f3(a4),f3(a65))))
% 60.39/60.44 [113]P9(a80,f120(f250(f3(a43),f3(a65))))
% 60.39/60.44 [114]P9(a81,f120(f250(f3(a54),f3(a65))))
% 60.39/60.44 [115]P9(a82,f120(f250(f3(a65),f3(a65))))
% 60.39/60.44 [116]P9(a83,f120(f250(f3(a76),f3(a65))))
% 60.39/60.44 [117]P9(a84,f120(f250(f3(a87),f3(a65))))
% 60.39/60.44 [118]P9(a85,f120(f250(f3(a98),f3(a65))))
% 60.39/60.44 [119]P9(a86,f120(f250(f3(a109),f3(a65))))
% 60.39/60.44 [120]P9(a88,f120(f250(f3(a2),f3(a76))))
% 60.39/60.44 [121]P9(a89,f120(f250(f3(a1),f3(a76))))
% 60.39/60.44 [122]P9(a90,f120(f250(f3(a4),f3(a76))))
% 60.39/60.44 [123]P9(a91,f120(f250(f3(a43),f3(a76))))
% 60.39/60.44 [124]P9(a92,f120(f250(f3(a54),f3(a76))))
% 60.39/60.44 [125]P9(a93,f120(f250(f3(a65),f3(a76))))
% 60.39/60.44 [126]P9(a94,f120(f250(f3(a76),f3(a76))))
% 60.39/60.44 [127]P9(a95,f120(f250(f3(a87),f3(a76))))
% 60.39/60.44 [128]P9(a96,f120(f250(f3(a98),f3(a76))))
% 60.39/60.44 [129]P9(a97,f120(f250(f3(a109),f3(a76))))
% 60.39/60.44 [130]P9(a99,f120(f250(f3(a2),f3(a87))))
% 60.39/60.44 [131]P9(a100,f120(f250(f3(a1),f3(a87))))
% 60.39/60.44 [132]P9(a101,f120(f250(f3(a4),f3(a87))))
% 60.39/60.44 [133]P9(a102,f120(f250(f3(a43),f3(a87))))
% 60.39/60.44 [134]P9(a103,f120(f250(f3(a54),f3(a87))))
% 60.39/60.44 [135]P9(a104,f120(f250(f3(a65),f3(a87))))
% 60.39/60.44 [136]P9(a105,f120(f250(f3(a76),f3(a87))))
% 60.39/60.44 [137]P9(a106,f120(f250(f3(a87),f3(a87))))
% 60.39/60.44 [138]P9(a107,f120(f250(f3(a98),f3(a87))))
% 60.39/60.44 [139]P9(a108,f120(f250(f3(a109),f3(a87))))
% 60.39/60.44 [140]P9(a110,f120(f250(f3(a2),f3(a98))))
% 60.39/60.44 [141]P9(a111,f120(f250(f3(a1),f3(a98))))
% 60.39/60.44 [142]P9(a112,f120(f250(f3(a4),f3(a98))))
% 60.39/60.44 [143]P9(a113,f120(f250(f3(a43),f3(a98))))
% 60.39/60.44 [144]P9(a114,f120(f250(f3(a54),f3(a98))))
% 60.39/60.44 [145]P9(a115,f120(f250(f3(a65),f3(a98))))
% 60.39/60.44 [146]P9(a116,f120(f250(f3(a76),f3(a98))))
% 60.39/60.44 [147]P9(a117,f120(f250(f3(a87),f3(a98))))
% 60.39/60.44 [148]P9(a118,f120(f250(f3(a98),f3(a98))))
% 60.39/60.44 [149]P9(a119,f120(f250(f3(a109),f3(a98))))
% 60.39/60.44 [150]P9(a122,f120(f250(f3(a2),f3(a109))))
% 60.39/60.44 [151]P9(a123,f120(f250(f3(a1),f3(a109))))
% 60.39/60.44 [152]P9(a124,f120(f250(f3(a4),f3(a109))))
% 60.39/60.44 [153]P9(a125,f120(f250(f3(a43),f3(a109))))
% 60.39/60.44 [154]P9(a126,f120(f250(f3(a54),f3(a109))))
% 60.39/60.44 [155]P9(a127,f120(f250(f3(a65),f3(a109))))
% 60.39/60.44 [156]P9(a128,f120(f250(f3(a76),f3(a109))))
% 60.39/60.44 [157]P9(a129,f120(f250(f3(a87),f3(a109))))
% 60.39/60.44 [158]P9(a130,f120(f250(f3(a98),f3(a109))))
% 60.39/60.44 [159]P9(a131,f120(f250(f3(a109),f3(a109))))
% 60.39/60.44 [160]P9(a134,f132(f250(f3(a2),f3(a1))))
% 60.39/60.44 [161]P9(a135,f132(f250(f3(a1),f3(a1))))
% 60.39/60.44 [162]P9(a146,f132(f250(f3(a4),f3(a1))))
% 60.39/60.44 [163]P9(a157,f132(f250(f3(a43),f3(a1))))
% 60.39/60.44 [164]P9(a167,f132(f250(f3(a54),f3(a1))))
% 60.39/60.44 [165]P9(a168,f132(f250(f3(a65),f3(a1))))
% 60.39/60.44 [166]P9(a169,f132(f250(f3(a76),f3(a1))))
% 60.39/60.44 [167]P9(a170,f132(f250(f3(a87),f3(a1))))
% 60.39/60.44 [168]P9(a171,f132(f250(f3(a98),f3(a1))))
% 60.39/60.44 [169]P9(a172,f132(f250(f3(a109),f3(a1))))
% 60.39/60.44 [170]P9(a174,f132(f250(f3(a2),f3(a4))))
% 60.39/60.44 [171]P9(a175,f132(f250(f3(a1),f3(a4))))
% 60.39/60.44 [172]P9(a176,f132(f250(f3(a4),f3(a4))))
% 60.39/60.44 [173]P9(a177,f132(f250(f3(a43),f3(a4))))
% 60.39/60.44 [174]P9(a178,f132(f250(f3(a54),f3(a4))))
% 60.39/60.44 [175]P9(a179,f132(f250(f3(a65),f3(a4))))
% 60.39/60.44 [176]P9(a180,f132(f250(f3(a76),f3(a4))))
% 60.39/60.44 [177]P9(a181,f132(f250(f3(a87),f3(a4))))
% 60.39/60.44 [178]P9(a182,f132(f250(f3(a98),f3(a4))))
% 60.39/60.44 [179]P9(a183,f132(f250(f3(a109),f3(a4))))
% 60.39/60.44 [180]P9(a185,f132(f250(f3(a2),f3(a43))))
% 60.39/60.44 [181]P9(a186,f132(f250(f3(a1),f3(a43))))
% 60.39/60.44 [182]P9(a187,f132(f250(f3(a4),f3(a43))))
% 60.39/60.45 [183]P9(a188,f132(f250(f3(a43),f3(a43))))
% 60.39/60.45 [184]P9(a189,f132(f250(f3(a54),f3(a43))))
% 60.39/60.45 [185]P9(a190,f132(f250(f3(a65),f3(a43))))
% 60.39/60.45 [186]P9(a191,f132(f250(f3(a76),f3(a43))))
% 60.39/60.45 [187]P9(a192,f132(f250(f3(a87),f3(a43))))
% 60.39/60.45 [188]P9(a193,f132(f250(f3(a98),f3(a43))))
% 60.39/60.45 [189]P9(a194,f132(f250(f3(a109),f3(a43))))
% 60.39/60.45 [190]P9(a196,f132(f250(f3(a2),f3(a54))))
% 60.39/60.45 [191]P9(a197,f132(f250(f3(a1),f3(a54))))
% 60.39/60.45 [192]P9(a198,f132(f250(f3(a4),f3(a54))))
% 60.39/60.45 [193]P9(a199,f132(f250(f3(a43),f3(a54))))
% 60.39/60.45 [194]P9(a200,f132(f250(f3(a54),f3(a54))))
% 60.39/60.45 [195]P9(a201,f132(f250(f3(a65),f3(a54))))
% 60.39/60.45 [196]P9(a202,f132(f250(f3(a76),f3(a54))))
% 60.39/60.45 [197]P9(a203,f132(f250(f3(a87),f3(a54))))
% 60.39/60.45 [198]P9(a204,f132(f250(f3(a98),f3(a54))))
% 60.39/60.45 [199]P9(a205,f132(f250(f3(a109),f3(a54))))
% 60.39/60.45 [200]P9(a207,f132(f250(f3(a2),f3(a65))))
% 60.39/60.45 [201]P9(a208,f132(f250(f3(a1),f3(a65))))
% 60.39/60.45 [202]P9(a209,f132(f250(f3(a4),f3(a65))))
% 60.39/60.45 [203]P9(a210,f132(f250(f3(a43),f3(a65))))
% 60.39/60.45 [204]P9(a211,f132(f250(f3(a54),f3(a65))))
% 60.39/60.45 [205]P9(a212,f132(f250(f3(a65),f3(a65))))
% 60.39/60.45 [206]P9(a213,f132(f250(f3(a76),f3(a65))))
% 60.39/60.45 [207]P9(a214,f132(f250(f3(a87),f3(a65))))
% 60.39/60.45 [208]P9(a215,f132(f250(f3(a98),f3(a65))))
% 60.39/60.45 [209]P9(a216,f132(f250(f3(a109),f3(a65))))
% 60.39/60.45 [210]P9(a218,f132(f250(f3(a2),f3(a76))))
% 60.39/60.45 [211]P9(a219,f132(f250(f3(a1),f3(a76))))
% 60.39/60.45 [212]P9(a220,f132(f250(f3(a4),f3(a76))))
% 60.39/60.45 [213]P9(a221,f132(f250(f3(a43),f3(a76))))
% 60.39/60.45 [214]P9(a222,f132(f250(f3(a54),f3(a76))))
% 60.39/60.45 [215]P9(a223,f132(f250(f3(a65),f3(a76))))
% 60.39/60.45 [216]P9(a224,f132(f250(f3(a76),f3(a76))))
% 60.39/60.45 [217]P9(a225,f132(f250(f3(a87),f3(a76))))
% 60.39/60.45 [218]P9(a226,f132(f250(f3(a98),f3(a76))))
% 60.39/60.45 [219]P9(a227,f132(f250(f3(a109),f3(a76))))
% 60.39/60.45 [220]P9(a229,f132(f250(f3(a2),f3(a87))))
% 60.39/60.45 [221]P9(a230,f132(f250(f3(a1),f3(a87))))
% 60.39/60.45 [222]P9(a231,f132(f250(f3(a4),f3(a87))))
% 60.39/60.45 [223]P9(a232,f132(f250(f3(a43),f3(a87))))
% 60.39/60.45 [224]P9(a233,f132(f250(f3(a54),f3(a87))))
% 60.39/60.45 [225]P9(a234,f132(f250(f3(a65),f3(a87))))
% 60.39/60.45 [226]P9(a235,f132(f250(f3(a76),f3(a87))))
% 60.39/60.45 [227]P9(a236,f132(f250(f3(a87),f3(a87))))
% 60.39/60.45 [228]P9(a237,f132(f250(f3(a98),f3(a87))))
% 60.39/60.45 [229]P9(a238,f132(f250(f3(a109),f3(a87))))
% 60.39/60.45 [230]P9(a240,f132(f250(f3(a2),f3(a98))))
% 60.39/60.45 [231]P9(a241,f132(f250(f3(a1),f3(a98))))
% 60.39/60.45 [232]P9(a242,f132(f250(f3(a4),f3(a98))))
% 60.39/60.45 [233]P9(a243,f132(f250(f3(a43),f3(a98))))
% 60.39/60.45 [234]P9(a244,f132(f250(f3(a54),f3(a98))))
% 60.39/60.45 [235]P9(a245,f132(f250(f3(a65),f3(a98))))
% 60.39/60.45 [236]P9(a246,f132(f250(f3(a76),f3(a98))))
% 60.39/60.45 [237]P9(a247,f132(f250(f3(a87),f3(a98))))
% 60.39/60.45 [238]P9(a248,f132(f250(f3(a98),f3(a98))))
% 60.39/60.45 [239]P9(a249,f132(f250(f3(a109),f3(a98))))
% 60.39/60.45 [240]P9(a251,f132(f250(f3(a2),f3(a109))))
% 60.39/60.45 [241]P9(a252,f132(f250(f3(a1),f3(a109))))
% 60.39/60.45 [242]P9(a253,f132(f250(f3(a4),f3(a109))))
% 60.39/60.45 [243]P9(a254,f132(f250(f3(a43),f3(a109))))
% 60.39/60.45 [244]P9(a255,f132(f250(f3(a54),f3(a109))))
% 60.39/60.45 [245]P9(a256,f132(f250(f3(a65),f3(a109))))
% 60.39/60.45 [246]P9(a257,f132(f250(f3(a76),f3(a109))))
% 60.39/60.45 [247]P9(a258,f132(f250(f3(a87),f3(a109))))
% 60.39/60.45 [248]P9(a259,f132(f250(f3(a98),f3(a109))))
% 60.39/60.45 [249]P9(a260,f132(f250(f3(a109),f3(a109))))
% 60.39/60.45 [250]P9(a7,f120(f250(f3(a2),f250(f3(a2),f3(a1)))))
% 60.39/60.45 [251]P9(a8,f120(f250(f3(a1),f250(f3(a2),f3(a1)))))
% 60.39/60.45 [252]P9(a9,f120(f250(f3(a4),f250(f3(a2),f3(a1)))))
% 60.39/60.45 [253]P9(a10,f120(f250(f3(a43),f250(f3(a2),f3(a1)))))
% 60.39/60.45 [254]P9(a11,f120(f250(f3(a54),f250(f3(a2),f3(a1)))))
% 60.39/60.45 [255]P9(a12,f120(f250(f3(a65),f250(f3(a2),f3(a1)))))
% 60.39/60.45 [256]P9(a13,f120(f250(f3(a76),f250(f3(a2),f3(a1)))))
% 60.39/60.45 [257]P9(a14,f120(f250(f3(a87),f250(f3(a2),f3(a1)))))
% 60.39/60.45 [258]P9(a15,f120(f250(f3(a98),f250(f3(a2),f3(a1)))))
% 60.39/60.45 [259]P9(a16,f120(f250(f3(a109),f250(f3(a2),f3(a1)))))
% 60.39/60.45 [260]P9(a18,f120(f250(f3(a2),f250(f3(a1),f3(a1)))))
% 60.39/60.45 [261]P9(a19,f120(f250(f3(a1),f250(f3(a1),f3(a1)))))
% 60.39/60.45 [262]P9(a20,f120(f250(f3(a4),f250(f3(a1),f3(a1)))))
% 60.39/60.45 [263]P9(a21,f120(f250(f3(a43),f250(f3(a1),f3(a1)))))
% 60.39/60.45 [264]P9(a22,f120(f250(f3(a54),f250(f3(a1),f3(a1)))))
% 60.39/60.45 [265]P9(a23,f120(f250(f3(a65),f250(f3(a1),f3(a1)))))
% 60.39/60.45 [266]P9(a24,f120(f250(f3(a76),f250(f3(a1),f3(a1)))))
% 60.39/60.45 [267]P9(a25,f120(f250(f3(a87),f250(f3(a1),f3(a1)))))
% 60.39/60.45 [268]P9(a26,f120(f250(f3(a98),f250(f3(a1),f3(a1)))))
% 60.39/60.45 [269]P9(a27,f120(f250(f3(a109),f250(f3(a1),f3(a1)))))
% 60.39/60.45 [270]P9(a29,f120(f250(f3(a2),f250(f3(a4),f3(a1)))))
% 60.39/60.45 [271]P9(a30,f120(f250(f3(a1),f250(f3(a4),f3(a1)))))
% 60.39/60.45 [272]P9(a31,f120(f250(f3(a4),f250(f3(a4),f3(a1)))))
% 60.39/60.45 [273]P9(a32,f120(f250(f3(a43),f250(f3(a4),f3(a1)))))
% 60.39/60.45 [274]P9(a33,f120(f250(f3(a54),f250(f3(a4),f3(a1)))))
% 60.39/60.45 [275]P9(a34,f120(f250(f3(a65),f250(f3(a4),f3(a1)))))
% 60.39/60.45 [276]P9(a35,f120(f250(f3(a76),f250(f3(a4),f3(a1)))))
% 60.39/60.45 [277]P9(a36,f120(f250(f3(a87),f250(f3(a4),f3(a1)))))
% 60.39/60.45 [278]P9(a136,f132(f250(f3(a2),f250(f3(a2),f3(a1)))))
% 60.39/60.45 [279]P9(a137,f132(f250(f3(a1),f250(f3(a2),f3(a1)))))
% 60.39/60.45 [280]P9(a138,f132(f250(f3(a4),f250(f3(a2),f3(a1)))))
% 60.39/60.45 [281]P9(a139,f132(f250(f3(a43),f250(f3(a2),f3(a1)))))
% 60.39/60.45 [282]P9(a140,f132(f250(f3(a54),f250(f3(a2),f3(a1)))))
% 60.39/60.45 [283]P9(a141,f132(f250(f3(a65),f250(f3(a2),f3(a1)))))
% 60.39/60.45 [284]P9(a142,f132(f250(f3(a76),f250(f3(a2),f3(a1)))))
% 60.39/60.45 [285]P9(a143,f132(f250(f3(a87),f250(f3(a2),f3(a1)))))
% 60.39/60.45 [286]P9(a144,f132(f250(f3(a98),f250(f3(a2),f3(a1)))))
% 60.39/60.45 [287]P9(a145,f132(f250(f3(a109),f250(f3(a2),f3(a1)))))
% 60.39/60.45 [288]P9(a147,f132(f250(f3(a2),f250(f3(a1),f3(a1)))))
% 60.39/60.45 [289]P9(a148,f132(f250(f3(a1),f250(f3(a1),f3(a1)))))
% 60.39/60.45 [290]P9(a149,f132(f250(f3(a4),f250(f3(a1),f3(a1)))))
% 60.39/60.45 [291]P9(a150,f132(f250(f3(a43),f250(f3(a1),f3(a1)))))
% 60.39/60.45 [292]P9(a151,f132(f250(f3(a54),f250(f3(a1),f3(a1)))))
% 60.39/60.45 [293]P9(a152,f132(f250(f3(a65),f250(f3(a1),f3(a1)))))
% 60.39/60.45 [294]P9(a153,f132(f250(f3(a76),f250(f3(a1),f3(a1)))))
% 60.39/60.45 [295]P9(a154,f132(f250(f3(a87),f250(f3(a1),f3(a1)))))
% 60.39/60.45 [296]P9(a155,f132(f250(f3(a98),f250(f3(a1),f3(a1)))))
% 60.39/60.45 [297]P9(a156,f132(f250(f3(a109),f250(f3(a1),f3(a1)))))
% 60.39/60.45 [298]P9(a158,f132(f250(f3(a2),f250(f3(a4),f3(a1)))))
% 60.39/60.45 [299]P9(a159,f132(f250(f3(a1),f250(f3(a4),f3(a1)))))
% 60.39/60.45 [300]P9(a160,f132(f250(f3(a4),f250(f3(a4),f3(a1)))))
% 60.39/60.45 [301]P9(a161,f132(f250(f3(a43),f250(f3(a4),f3(a1)))))
% 60.39/60.45 [302]P9(a162,f132(f250(f3(a54),f250(f3(a4),f3(a1)))))
% 60.39/60.45 [303]P9(a163,f132(f250(f3(a65),f250(f3(a4),f3(a1)))))
% 60.39/60.45 [304]P9(a164,f132(f250(f3(a76),f250(f3(a4),f3(a1)))))
% 60.39/60.45 [305]P9(a165,f132(f250(f3(a87),f250(f3(a4),f3(a1)))))
% 60.39/60.45 [306]P9(a166,f132(f250(f3(a98),f250(f3(a4),f3(a1)))))
% 60.39/60.45 [410]P7(f3(x4101))+~P1(f3(x4101))
% 60.39/60.45 [408]~E(x4081,x4082)+P4(x4081,x4082)
% 60.39/60.45 [409]~P5(x4092,x4091)+~E(x4091,x4092)
% 60.39/60.45 [412]~P5(x4121,x4122)+P4(x4121,x4122)
% 60.39/60.45 [414]~P5(x4142,x4141)+~P5(x4141,x4142)
% 60.39/60.45 [415]~P7(x4152)+P7(f250(f3(x4151),x4152))
% 60.39/60.45 [425]~P3(x4253,x4251,x4252)+P10(x4251,x4252,x4253)
% 60.39/60.45 [426]~P10(x4262,x4263,x4261)+P3(x4261,x4262,x4263)
% 60.39/60.45 [416]~P7(x4163)+P8(f3(x4161),f250(f3(x4162),x4163))
% 60.39/60.45 [421]~P8(x4212,x4214)+P8(f250(f3(x4211),x4212),f250(f3(x4213),x4214))
% 60.39/60.45 [435]P6(f3(x4351),f250(f3(x4352),x4353),f3(x4354),f250(f3(x4355),x4356))+~P6(f3(x4351),f3(x4354),f250(f3(x4352),x4353),f250(f3(x4355),x4356))
% 60.39/60.45 [411]P5(x4112,x4111)+P5(x4111,x4112)+E(x4111,x4112)
% 60.39/60.45 [413]P5(x4131,x4132)+~P4(x4131,x4132)+E(x4131,x4132)
% 60.39/60.45 [423]P4(x4231,x4232)+~P5(x4231,x4233)+~P10(x4232,a1,x4233)
% 60.39/60.45 [420]P8(f3(x4201),f3(x4202))+~P8(f3(x4203),f3(x4202))+~P8(f3(x4201),f3(x4203))
% 60.39/60.45 [422]P10(x4221,x4222,a2)+~P9(x4221,f120(x4223))+~P9(x4222,f132(x4223))
% 60.39/60.45 [424]~P7(x4242)+~P8(f3(x4241),f3(x4243))+P8(f250(f3(x4241),x4242),f250(f3(x4243),x4242))
% 60.39/60.45 [427]~P10(x4273,x4274,x4271)+E(x4271,x4272)+~P10(x4273,x4274,x4272)
% 60.39/60.45 [428]~P10(x4283,x4281,x4284)+E(x4281,x4282)+~P10(x4283,x4282,x4284)
% 60.39/60.45 [429]~P10(x4291,x4293,x4294)+E(x4291,x4292)+~P10(x4292,x4293,x4294)
% 60.39/60.45 [417]P5(x4171,x4172)+~P9(x4172,f120(x4173))+~P9(x4171,f132(x4174))
% 60.39/60.45 [436]P6(f3(x4361),f3(x4362),f3(x4363),f3(x4364))+~P2(f3(x4365),f3(x4361),f3(x4364),f3(a2))+~P2(f3(x4362),f3(x4363),f3(x4365),f3(a2))
% 60.39/60.45 [418]P5(x4181,x4182)+~P8(x4183,x4184)+~P9(x4182,f132(x4183))+~P9(x4181,f132(x4184))
% 60.39/60.45 [419]P5(x4191,x4192)+~P8(x4193,x4194)+~P9(x4192,f120(x4194))+~P9(x4191,f120(x4193))
% 60.39/60.45 [430]~P10(x4302,x4301,x4303)+P10(x4301,x4302,x4303)+~P9(x4302,f120(x4304))+~P9(x4301,f132(x4305))
% 60.39/60.45 [437]~P2(f3(x4375),f3(x4371),f3(x4374),f3(x4376))+~P2(f3(x4372),f3(x4373),f3(x4375),f3(x4377))+~P2(f3(x4377),f3(x4376),f3(a1),f3(a2))+P6(f3(x4371),f3(x4372),f3(x4373),f250(f3(x4374),f3(a1)))
% 60.39/60.45 [431]P10(x4311,x4312,x4313)+~P6(f3(a2),x4316,x4315,x4314)+~P9(x4313,f120(x4314))+~P9(x4312,f120(x4315))+~P9(x4311,f120(x4316))
% 60.39/60.45 [432]P10(x4321,x4322,x4323)+~P6(f3(a2),x4326,x4325,x4324)+~P9(x4323,f132(x4324))+~P9(x4322,f132(x4325))+~P9(x4321,f132(x4326))
% 60.39/60.45 [433]P10(x4331,x4332,x4333)+~P8(x4334,x4335)+~P6(f3(a2),x4334,x4336,x4335)+~P9(x4332,f132(x4334))+~P9(x4331,f120(x4335))+~P9(x4333,f120(x4336))
% 60.39/60.45 [434]P10(x4341,x4342,x4343)+~P8(x4344,x4345)+~P6(f3(a2),x4344,x4346,x4345)+~P9(x4342,f132(x4345))+~P9(x4341,f120(x4344))+~P9(x4343,f132(x4346))
% 60.39/60.45 [438]~P7(x4386)+~P7(x4384)+~P2(f3(x4388),f3(x4381),f3(x4385),f3(x4389))+~P2(f3(x4382),f3(x4383),f3(x4388),f3(x43810))+~P6(f3(x4387),f3(a2),x4384,x4386)+~P2(f3(x43810),f3(x4389),f3(x4387),f3(a2))+P6(f3(x4381),f3(x4382),f250(f3(x4383),x4384),f250(f3(x4385),x4386))
% 60.39/60.45 [439]~P7(x4397)+~P7(x4395)+~P7(x4393)+~P6(f3(x4398),x4393,x4395,x4397)+~P2(f3(x4399),f3(x4391),f3(x4396),f3(x43910))+~P2(f3(x4392),f3(x4394),f3(x4399),f3(x43911))+~P2(f3(x43911),f3(x43910),f3(x4398),f3(a2))+P6(f3(x4391),f250(f3(x4392),x4393),f250(f3(x4394),x4395),f250(f3(x4396),x4397))
% 60.39/60.45 %EqnAxiom
% 60.39/60.45 [1]E(x11,x11)
% 60.39/60.45 [2]E(x22,x21)+~E(x21,x22)
% 60.39/60.45 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 60.39/60.45 [4]~E(x41,x42)+E(f3(x41),f3(x42))
% 60.39/60.45 [5]~E(x51,x52)+E(f250(x51,x53),f250(x52,x53))
% 60.39/60.45 [6]~E(x61,x62)+E(f250(x63,x61),f250(x63,x62))
% 60.39/60.45 [7]~E(x71,x72)+E(f132(x71),f132(x72))
% 60.39/60.45 [8]~E(x81,x82)+E(f120(x81),f120(x82))
% 60.39/60.45 [9]~P1(x91)+P1(x92)+~E(x91,x92)
% 60.39/60.45 [10]P2(x102,x103,x104,x105)+~E(x101,x102)+~P2(x101,x103,x104,x105)
% 60.39/60.45 [11]P2(x113,x112,x114,x115)+~E(x111,x112)+~P2(x113,x111,x114,x115)
% 60.39/60.45 [12]P2(x123,x124,x122,x125)+~E(x121,x122)+~P2(x123,x124,x121,x125)
% 60.39/60.45 [13]P2(x133,x134,x135,x132)+~E(x131,x132)+~P2(x133,x134,x135,x131)
% 60.39/60.45 [14]P6(x142,x143,x144,x145)+~E(x141,x142)+~P6(x141,x143,x144,x145)
% 60.39/60.45 [15]P6(x153,x152,x154,x155)+~E(x151,x152)+~P6(x153,x151,x154,x155)
% 60.39/60.45 [16]P6(x163,x164,x162,x165)+~E(x161,x162)+~P6(x163,x164,x161,x165)
% 60.39/60.45 [17]P6(x173,x174,x175,x172)+~E(x171,x172)+~P6(x173,x174,x175,x171)
% 60.39/60.45 [18]~P7(x181)+P7(x182)+~E(x181,x182)
% 60.39/60.45 [19]P3(x192,x193,x194)+~E(x191,x192)+~P3(x191,x193,x194)
% 60.39/60.45 [20]P3(x203,x202,x204)+~E(x201,x202)+~P3(x203,x201,x204)
% 60.39/60.45 [21]P3(x213,x214,x212)+~E(x211,x212)+~P3(x213,x214,x211)
% 60.39/60.45 [22]P5(x222,x223)+~E(x221,x222)+~P5(x221,x223)
% 60.39/60.45 [23]P5(x233,x232)+~E(x231,x232)+~P5(x233,x231)
% 60.39/60.45 [24]P8(x242,x243)+~E(x241,x242)+~P8(x241,x243)
% 60.39/60.45 [25]P8(x253,x252)+~E(x251,x252)+~P8(x253,x251)
% 60.39/60.45 [26]P9(x262,x263)+~E(x261,x262)+~P9(x261,x263)
% 60.39/60.45 [27]P9(x273,x272)+~E(x271,x272)+~P9(x273,x271)
% 60.39/60.45 [28]P4(x282,x283)+~E(x281,x282)+~P4(x281,x283)
% 60.39/60.45 [29]P4(x293,x292)+~E(x291,x292)+~P4(x293,x291)
% 60.39/60.45 [30]P10(x302,x303,x304)+~E(x301,x302)+~P10(x301,x303,x304)
% 60.39/60.45 [31]P10(x313,x312,x314)+~E(x311,x312)+~P10(x313,x311,x314)
% 60.39/60.45 [32]P10(x323,x324,x322)+~E(x321,x322)+~P10(x323,x324,x321)
% 60.39/60.45
% 60.39/60.45 %-------------------------------------------
% 60.39/60.45 cnf(441,plain,
% 60.39/60.45 (~P5(x4411,x4411)),
% 60.39/60.45 inference(equality_inference,[],[409])).
% 60.39/60.45 cnf(442,plain,
% 60.39/60.45 (~P10(a65,a4,a87)),
% 60.39/60.45 inference(scs_inference,[],[407,426])).
% 60.39/60.45 cnf(446,plain,
% 60.39/60.45 (P6(f3(a2),f3(a2),f3(a2),f3(a2))),
% 60.39/60.45 inference(scs_inference,[],[407,52,61,307,426,422,436])).
% 60.39/60.45 cnf(450,plain,
% 60.39/60.45 (P10(a121,a1,a2)),
% 60.39/60.45 inference(scs_inference,[],[407,51,52,61,307,426,422,436,417,430])).
% 60.39/60.45 cnf(452,plain,
% 60.39/60.45 (~P8(f3(a1),f3(a1))),
% 60.39/60.45 inference(scs_inference,[],[407,441,51,52,61,307,426,422,436,417,430,418])).
% 60.39/60.45 cnf(453,plain,
% 60.39/60.45 (~P5(x4531,x4531)),
% 60.39/60.45 inference(rename_variables,[],[441])).
% 60.39/60.45 cnf(456,plain,
% 60.39/60.45 (~P5(x4561,x4561)),
% 60.39/60.45 inference(rename_variables,[],[441])).
% 60.39/60.45 cnf(458,plain,
% 60.39/60.45 (P10(a2,a2,a2)),
% 60.39/60.45 inference(scs_inference,[],[407,441,453,51,52,61,307,426,422,436,417,430,418,419,431])).
% 60.39/60.45 cnf(463,plain,
% 60.39/60.45 (~P8(f3(a1),f3(a2))),
% 60.39/60.45 inference(scs_inference,[],[407,441,453,42,51,52,61,307,426,422,436,417,430,418,419,431,414,30,420])).
% 60.39/60.45 cnf(466,plain,
% 60.39/60.45 (~P5(x4661,x4661)),
% 60.39/60.45 inference(rename_variables,[],[441])).
% 60.39/60.45 cnf(470,plain,
% 60.39/60.45 (~E(f3(a1),f3(a2))),
% 60.39/60.45 inference(scs_inference,[],[407,441,453,456,466,42,51,52,61,307,426,422,436,417,430,418,419,431,414,30,420,22,23,24,25])).
% 60.39/60.45 cnf(478,plain,
% 60.39/60.45 (~P8(f3(a4),f3(a2))),
% 60.39/60.45 inference(scs_inference,[],[463,470,43,4,420])).
% 60.39/60.45 cnf(486,plain,
% 60.39/60.45 (~E(f3(a4),f3(a2))),
% 60.39/60.45 inference(scs_inference,[],[463,470,43,53,62,308,307,4,420,422,417,436,25])).
% 60.39/60.45 cnf(488,plain,
% 60.39/60.45 (~P5(x4881,x4881)),
% 60.39/60.45 inference(rename_variables,[],[441])).
% 60.39/60.45 cnf(489,plain,
% 60.39/60.45 (~E(a133,a4)),
% 60.39/60.45 inference(scs_inference,[],[463,470,43,53,62,441,488,308,307,4,420,422,417,436,25,23,22])).
% 60.39/60.45 cnf(490,plain,
% 60.39/60.45 (~P5(x4901,x4901)),
% 60.39/60.45 inference(rename_variables,[],[441])).
% 60.39/60.45 cnf(491,plain,
% 60.39/60.45 (~P8(f3(a4),f3(a4))),
% 60.39/60.45 inference(scs_inference,[],[463,470,43,53,62,441,488,490,308,307,4,420,422,417,436,25,23,22,419])).
% 60.39/60.45 cnf(492,plain,
% 60.39/60.45 (~P5(x4921,x4921)),
% 60.39/60.45 inference(rename_variables,[],[441])).
% 60.39/60.45 cnf(494,plain,
% 60.39/60.45 (P10(a133,a4,a2)),
% 60.39/60.45 inference(scs_inference,[],[463,470,43,53,62,441,488,490,308,307,4,420,422,417,436,25,23,22,419,430])).
% 60.39/60.45 cnf(496,plain,
% 60.39/60.45 (~P8(f3(a43),f3(a43))),
% 60.39/60.45 inference(scs_inference,[],[463,470,43,53,62,63,441,488,490,492,308,307,4,420,422,417,436,25,23,22,419,430,418])).
% 60.39/60.45 cnf(502,plain,
% 60.39/60.45 (~E(f3(a1),f3(a4))),
% 60.39/60.45 inference(scs_inference,[],[446,463,470,43,53,62,63,441,488,490,492,308,307,4,420,422,417,436,25,23,22,419,430,418,414,16,24])).
% 60.39/60.45 cnf(504,plain,
% 60.39/60.45 (P9(x5041,f120(f3(a4)))+~E(a4,x5041)),
% 60.39/60.45 inference(scs_inference,[],[446,463,470,43,53,62,63,441,488,490,492,308,307,4,420,422,417,436,25,23,22,419,430,418,414,16,24,17,26])).
% 60.39/60.45 cnf(514,plain,
% 60.39/60.45 (~E(a4,a2)),
% 60.39/60.45 inference(scs_inference,[],[486,4])).
% 60.39/60.45 cnf(515,plain,
% 60.39/60.45 (~P8(f3(a43),f3(a2))),
% 60.39/60.45 inference(scs_inference,[],[478,486,44,4,420])).
% 60.39/60.45 cnf(523,plain,
% 60.39/60.45 (~E(a2,a184)),
% 60.39/60.45 inference(scs_inference,[],[51,478,486,44,55,64,441,309,307,4,420,422,436,417,23])).
% 60.39/60.45 cnf(524,plain,
% 60.39/60.45 (~P5(x5241,x5241)),
% 60.39/60.45 inference(rename_variables,[],[441])).
% 60.39/60.45 cnf(525,plain,
% 60.39/60.45 (~E(f3(a4),f3(a43))),
% 60.39/60.45 inference(scs_inference,[],[51,478,486,44,55,64,441,496,309,307,4,420,422,436,417,23,24])).
% 60.39/60.45 cnf(527,plain,
% 60.39/60.45 (~P5(x5271,x5271)),
% 60.39/60.45 inference(rename_variables,[],[441])).
% 60.39/60.45 cnf(528,plain,
% 60.39/60.45 (~E(f3(a43),f3(a2))),
% 60.39/60.45 inference(scs_inference,[],[51,478,486,44,55,64,441,524,496,309,307,4,420,422,436,417,23,24,22,25])).
% 60.39/60.45 cnf(529,plain,
% 60.39/60.45 (P10(a184,a54,a2)),
% 60.39/60.45 inference(scs_inference,[],[51,478,486,44,55,64,441,524,496,309,307,4,420,422,436,417,23,24,22,25,430])).
% 60.39/60.45 cnf(531,plain,
% 60.39/60.45 (~P8(f3(a54),f3(a54))),
% 60.39/60.45 inference(scs_inference,[],[51,478,486,44,55,64,441,524,527,496,309,307,4,420,422,436,417,23,24,22,25,430,418])).
% 60.39/60.45 cnf(532,plain,
% 60.39/60.45 (~P5(x5321,x5321)),
% 60.39/60.45 inference(rename_variables,[],[441])).
% 60.39/60.45 cnf(534,plain,
% 60.39/60.45 (~P8(f3(a65),f3(a65))),
% 60.39/60.45 inference(scs_inference,[],[51,478,486,44,55,56,64,441,524,527,532,496,309,307,4,420,422,436,417,23,24,22,25,430,418,419])).
% 60.39/60.45 cnf(537,plain,
% 60.39/60.45 (~P5(a2,a184)),
% 60.39/60.45 inference(scs_inference,[],[51,478,486,44,55,56,64,441,524,527,532,496,309,307,4,420,422,436,417,23,24,22,25,430,418,419,414])).
% 60.39/60.45 cnf(546,plain,
% 60.39/60.45 (~E(a1,a4)),
% 60.39/60.45 inference(scs_inference,[],[502,4])).
% 60.39/60.45 cnf(547,plain,
% 60.39/60.45 (~P8(f3(a54),f3(a2))),
% 60.39/60.45 inference(scs_inference,[],[502,515,45,4,420])).
% 60.39/60.45 cnf(555,plain,
% 60.39/60.45 (~E(f3(a43),f3(a54))),
% 60.39/60.45 inference(scs_inference,[],[51,502,515,45,65,56,531,310,307,4,420,422,417,436,24])).
% 60.39/60.45 cnf(556,plain,
% 60.39/60.45 (~E(a2,a195)),
% 60.39/60.45 inference(scs_inference,[],[51,502,515,45,65,56,441,531,310,307,4,420,422,417,436,24,23])).
% 60.39/60.45 cnf(557,plain,
% 60.39/60.45 (~P5(x5571,x5571)),
% 60.39/60.45 inference(rename_variables,[],[441])).
% 60.39/60.45 cnf(559,plain,
% 60.39/60.45 (~P5(x5591,x5591)),
% 60.39/60.45 inference(rename_variables,[],[441])).
% 60.39/60.45 cnf(560,plain,
% 60.39/60.45 (~E(f3(a54),f3(a2))),
% 60.39/60.45 inference(scs_inference,[],[51,502,515,45,65,56,441,557,531,310,307,4,420,422,417,436,24,23,22,25])).
% 60.39/60.45 cnf(561,plain,
% 60.39/60.45 (~P8(f3(a76),f3(a76))),
% 60.39/60.45 inference(scs_inference,[],[51,502,515,45,65,66,56,441,557,559,531,310,307,4,420,422,417,436,24,23,22,25,418])).
% 60.39/60.45 cnf(562,plain,
% 60.39/60.45 (~P5(x5621,x5621)),
% 60.39/60.45 inference(rename_variables,[],[441])).
% 60.39/60.45 cnf(566,plain,
% 60.39/60.45 (~P8(f3(a87),f3(a87))),
% 60.39/60.45 inference(scs_inference,[],[51,502,515,45,58,65,66,56,441,557,559,562,531,310,307,4,420,422,417,436,24,23,22,25,418,430,419])).
% 60.39/60.45 cnf(569,plain,
% 60.39/60.45 (~P5(a2,a195)),
% 60.39/60.45 inference(scs_inference,[],[51,502,515,45,58,65,66,56,441,557,559,562,531,310,307,4,420,422,417,436,24,23,22,25,418,430,419,414])).
% 60.39/60.45 cnf(575,plain,
% 60.39/60.45 (~E(a4,a43)),
% 60.39/60.45 inference(scs_inference,[],[525,4])).
% 60.39/60.45 cnf(576,plain,
% 60.39/60.46 (~P8(f3(a65),f3(a2))),
% 60.39/60.46 inference(scs_inference,[],[525,547,46,4,420])).
% 60.39/60.46 cnf(585,plain,
% 60.39/60.46 (~P5(x5851,x5851)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(586,plain,
% 60.39/60.46 (~E(f3(a54),f3(a65))),
% 60.39/60.46 inference(scs_inference,[],[51,525,547,46,67,58,441,534,311,307,4,420,422,436,417,23,24])).
% 60.39/60.46 cnf(588,plain,
% 60.39/60.46 (~P5(x5881,x5881)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(589,plain,
% 60.39/60.46 (~E(f3(a65),f3(a2))),
% 60.39/60.46 inference(scs_inference,[],[51,525,547,46,67,58,441,585,534,311,307,4,420,422,436,417,23,24,22,25])).
% 60.39/60.46 cnf(592,plain,
% 60.39/60.46 (~P8(f3(a98),f3(a98))),
% 60.39/60.46 inference(scs_inference,[],[51,525,547,46,67,68,58,441,585,588,534,311,307,4,420,422,436,417,23,24,22,25,430,418])).
% 60.39/60.46 cnf(593,plain,
% 60.39/60.46 (~P5(x5931,x5931)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(595,plain,
% 60.39/60.46 (~P8(f3(a109),f3(a109))),
% 60.39/60.46 inference(scs_inference,[],[51,525,547,46,60,67,68,58,441,585,588,593,534,311,307,4,420,422,436,417,23,24,22,25,430,418,419])).
% 60.39/60.46 cnf(603,plain,
% 60.39/60.46 (P9(x6031,f120(f3(a2)))+~E(a2,x6031)),
% 60.39/60.46 inference(scs_inference,[],[450,51,525,547,46,60,67,68,58,441,585,588,593,534,311,307,4,420,422,436,417,23,24,22,25,430,418,419,414,27,12,32,26])).
% 60.39/60.46 cnf(613,plain,
% 60.39/60.46 (~P8(f3(a76),f3(a2))),
% 60.39/60.46 inference(scs_inference,[],[528,576,47,4,420])).
% 60.39/60.46 cnf(617,plain,
% 60.39/60.46 (P5(a239,a2)),
% 60.39/60.46 inference(scs_inference,[],[51,528,576,47,69,60,4,420,422,417])).
% 60.39/60.46 cnf(619,plain,
% 60.39/60.46 (P6(f3(a65),f3(a2),f3(a2),f3(a65))),
% 60.39/60.46 inference(scs_inference,[],[51,528,576,47,69,60,312,307,4,420,422,417,436])).
% 60.39/60.46 cnf(621,plain,
% 60.39/60.46 (~E(f3(a65),f3(a76))),
% 60.39/60.46 inference(scs_inference,[],[51,528,576,47,69,60,561,312,307,4,420,422,417,436,24])).
% 60.39/60.46 cnf(623,plain,
% 60.39/60.46 (~P5(x6231,x6231)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(626,plain,
% 60.39/60.46 (~E(f3(a76),f3(a2))),
% 60.39/60.46 inference(scs_inference,[],[51,528,576,47,69,60,441,623,561,312,307,4,420,422,417,436,24,23,22,25])).
% 60.39/60.46 cnf(649,plain,
% 60.39/60.46 (~E(a43,a54)),
% 60.39/60.46 inference(scs_inference,[],[555,4])).
% 60.39/60.46 cnf(650,plain,
% 60.39/60.46 (~P8(f3(a87),f3(a2))),
% 60.39/60.46 inference(scs_inference,[],[555,613,48,4,420])).
% 60.39/60.46 cnf(654,plain,
% 60.39/60.46 (P6(f3(a76),f3(a2),f3(a2),f3(a76))),
% 60.39/60.46 inference(scs_inference,[],[555,613,48,161,71,313,307,4,420,422,436])).
% 60.39/60.46 cnf(659,plain,
% 60.39/60.46 (~P5(x6591,x6591)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(660,plain,
% 60.39/60.46 (~E(f3(a76),f3(a87))),
% 60.39/60.46 inference(scs_inference,[],[51,555,613,48,161,71,441,566,313,307,4,420,422,436,417,23,24])).
% 60.39/60.46 cnf(662,plain,
% 60.39/60.46 (~P5(x6621,x6621)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(663,plain,
% 60.39/60.46 (~E(f3(a87),f3(a2))),
% 60.39/60.46 inference(scs_inference,[],[51,555,613,48,161,71,441,659,566,313,307,4,420,422,436,417,23,24,22,25])).
% 60.39/60.46 cnf(667,plain,
% 60.39/60.46 (~P5(x6671,x6671)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(678,plain,
% 60.39/60.46 (P9(x6781,f120(f3(a43)))+~E(a43,x6781)),
% 60.39/60.46 inference(scs_inference,[],[51,555,613,619,48,54,161,162,73,71,441,659,662,667,566,313,307,4,420,422,436,417,23,24,22,25,430,418,419,414,14,12,27,13,26])).
% 60.39/60.46 cnf(687,plain,
% 60.39/60.46 (~P8(f3(a98),f3(a2))),
% 60.39/60.46 inference(scs_inference,[],[560,650,49,4,420])).
% 60.39/60.46 cnf(695,plain,
% 60.39/60.46 (~E(f3(a87),f3(a98))),
% 60.39/60.46 inference(scs_inference,[],[51,560,650,49,163,73,592,314,307,4,420,422,417,436,24])).
% 60.39/60.46 cnf(697,plain,
% 60.39/60.46 (~P5(x6971,x6971)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(699,plain,
% 60.39/60.46 (~P5(x6991,x6991)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(700,plain,
% 60.39/60.46 (~E(f3(a98),f3(a2))),
% 60.39/60.46 inference(scs_inference,[],[51,560,650,49,163,73,441,697,592,314,307,4,420,422,417,436,24,23,22,25])).
% 60.39/60.46 cnf(702,plain,
% 60.39/60.46 (~P5(x7021,x7021)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(715,plain,
% 60.39/60.46 (P9(x7151,f120(f3(a76)))+~E(a76,x7151)),
% 60.39/60.46 inference(scs_inference,[],[51,560,650,654,49,57,163,164,75,73,441,697,699,702,592,314,307,4,420,422,417,436,24,23,22,25,418,430,419,414,15,17,11,10,26])).
% 60.39/60.46 cnf(732,plain,
% 60.39/60.46 (~E(f3(a98),f3(a109))),
% 60.39/60.46 inference(scs_inference,[],[51,586,687,50,165,75,595,315,307,4,420,422,436,417,24])).
% 60.39/60.46 cnf(759,plain,
% 60.39/60.46 (~P8(f3(a4),f3(a1))),
% 60.39/60.46 inference(scs_inference,[],[589,43,491,4,420])).
% 60.39/60.46 cnf(794,plain,
% 60.39/60.46 (~P8(f3(a43),f3(a4))),
% 60.39/60.46 inference(scs_inference,[],[44,621,496,4,420])).
% 60.39/60.46 cnf(802,plain,
% 60.39/60.46 (~E(f3(a2),f3(a4))),
% 60.39/60.46 inference(scs_inference,[],[51,42,44,621,759,169,79,317,496,4,420,422,436,417,24])).
% 60.39/60.46 cnf(804,plain,
% 60.39/60.46 (~P5(x8041,x8041)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(807,plain,
% 60.39/60.46 (~E(f3(a43),f3(a1))),
% 60.39/60.46 inference(scs_inference,[],[51,42,44,621,759,169,79,441,804,317,496,4,420,422,436,417,24,23,22,25])).
% 60.39/60.46 cnf(831,plain,
% 60.39/60.46 (~P8(f3(a43),f3(a1))),
% 60.39/60.46 inference(scs_inference,[],[43,626,794,4,420])).
% 60.39/60.46 cnf(839,plain,
% 60.39/60.46 (~E(f3(a1),f3(a43))),
% 60.39/60.46 inference(scs_inference,[],[51,43,626,794,171,81,318,308,4,420,422,417,436,24])).
% 60.39/60.46 cnf(841,plain,
% 60.39/60.46 (~P5(x8411,x8411)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(844,plain,
% 60.39/60.46 (~E(f3(a54),f3(a4))),
% 60.39/60.46 inference(scs_inference,[],[51,45,43,626,794,171,81,441,841,318,308,4,420,422,417,436,24,23,22,25])).
% 60.39/60.46 cnf(868,plain,
% 60.39/60.46 (~P8(f3(a76),f3(a65))),
% 60.39/60.46 inference(scs_inference,[],[47,660,561,4,420])).
% 60.39/60.46 cnf(876,plain,
% 60.39/60.46 (~E(f3(a2),f3(a43))),
% 60.39/60.46 inference(scs_inference,[],[51,47,42,660,831,173,83,319,561,317,4,420,422,436,417,24])).
% 60.39/60.46 cnf(878,plain,
% 60.39/60.46 (~P5(x8781,x8781)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(881,plain,
% 60.39/60.46 (~E(f3(a54),f3(a1))),
% 60.39/60.46 inference(scs_inference,[],[51,47,42,45,660,831,173,83,441,878,319,561,317,4,420,422,436,417,24,23,22,25])).
% 60.39/60.46 cnf(905,plain,
% 60.39/60.46 (~P8(f3(a76),f3(a54))),
% 60.39/60.46 inference(scs_inference,[],[46,695,868,4,420])).
% 60.39/60.46 cnf(913,plain,
% 60.39/60.46 (~E(f3(a54),f3(a76))),
% 60.39/60.46 inference(scs_inference,[],[51,46,695,868,175,85,320,308,4,420,422,417,436,24])).
% 60.39/60.46 cnf(915,plain,
% 60.39/60.46 (~P5(x9151,x9151)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(917,plain,
% 60.39/60.46 (~P5(x9171,x9171)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(918,plain,
% 60.39/60.46 (~E(f3(a87),f3(a65))),
% 60.39/60.46 inference(scs_inference,[],[51,46,48,695,868,175,85,441,915,320,308,4,420,422,417,436,24,23,22,25])).
% 60.39/60.46 cnf(922,plain,
% 60.39/60.46 (P10(a179,a49,a2)),
% 60.39/60.46 inference(scs_inference,[],[51,46,48,695,868,175,176,85,441,915,917,320,308,4,420,422,417,436,24,23,22,25,418,430])).
% 60.39/60.46 cnf(942,plain,
% 60.39/60.46 (~P8(f3(a76),f3(a43))),
% 60.39/60.46 inference(scs_inference,[],[45,732,905,4,420])).
% 60.39/60.46 cnf(950,plain,
% 60.39/60.46 (~E(f3(a43),f3(a76))),
% 60.39/60.46 inference(scs_inference,[],[51,45,732,905,177,87,321,317,4,420,422,436,417,24])).
% 60.39/60.46 cnf(952,plain,
% 60.39/60.46 (~P5(x9521,x9521)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(955,plain,
% 60.39/60.46 (~E(f3(a87),f3(a54))),
% 60.39/60.46 inference(scs_inference,[],[51,48,45,732,905,177,87,441,952,321,317,4,420,422,436,417,24,23,22,25])).
% 60.39/60.46 cnf(981,plain,
% 60.39/60.46 (~P8(f3(a76),f3(a4))),
% 60.39/60.46 inference(scs_inference,[],[44,700,942,179,89,4,422,420])).
% 60.39/60.46 cnf(983,plain,
% 60.39/60.46 (P5(a183,a2)),
% 60.39/60.46 inference(scs_inference,[],[51,44,700,942,179,89,4,422,420,417])).
% 60.39/60.46 cnf(987,plain,
% 60.39/60.46 (~E(f3(a4),f3(a76))),
% 60.39/60.46 inference(scs_inference,[],[51,44,700,942,179,89,322,308,4,422,420,417,436,24])).
% 60.39/60.46 cnf(989,plain,
% 60.39/60.46 (~P5(x9891,x9891)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(992,plain,
% 60.39/60.46 (~E(f3(a87),f3(a43))),
% 60.39/60.46 inference(scs_inference,[],[51,44,48,700,942,179,89,441,989,322,308,4,422,420,417,436,24,23,22,25])).
% 60.39/60.46 cnf(1017,plain,
% 60.39/60.46 (~P8(f3(a76),f3(a1))),
% 60.39/60.46 inference(scs_inference,[],[43,663,981,4,420])).
% 60.39/60.46 cnf(1025,plain,
% 60.39/60.46 (~E(f3(a1),f3(a76))),
% 60.39/60.46 inference(scs_inference,[],[51,43,663,981,181,91,323,317,4,420,422,436,417,24])).
% 60.39/60.46 cnf(1027,plain,
% 60.39/60.46 (~P5(x10271,x10271)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(1030,plain,
% 60.39/60.46 (~E(f3(a87),f3(a4))),
% 60.39/60.46 inference(scs_inference,[],[51,43,48,663,981,181,91,441,1027,323,317,4,420,422,436,417,24,23,22,25])).
% 60.39/60.46 cnf(1056,plain,
% 60.39/60.46 (~P8(f3(a54),f3(a43))),
% 60.39/60.46 inference(scs_inference,[],[45,802,183,93,531,4,422,420])).
% 60.39/60.46 cnf(1062,plain,
% 60.39/60.46 (~E(f3(a2),f3(a76))),
% 60.39/60.46 inference(scs_inference,[],[51,42,45,802,1017,183,93,324,531,308,4,422,420,417,436,24])).
% 60.39/60.46 cnf(1064,plain,
% 60.39/60.46 (~P5(x10641,x10641)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(1067,plain,
% 60.39/60.46 (~E(f3(a87),f3(a1))),
% 60.39/60.46 inference(scs_inference,[],[51,42,45,48,802,1017,183,93,441,1064,324,531,308,4,422,420,417,436,24,23,22,25])).
% 60.39/60.46 cnf(1091,plain,
% 60.39/60.46 (~P8(f3(a54),f3(a4))),
% 60.39/60.46 inference(scs_inference,[],[44,913,1056,4,420])).
% 60.39/60.46 cnf(1097,plain,
% 60.39/60.46 (~E(f3(a4),f3(a54))),
% 60.39/60.46 inference(scs_inference,[],[44,913,1056,185,95,325,317,4,420,422,436,24])).
% 60.39/60.46 cnf(1098,plain,
% 60.39/60.46 (P5(a190,a2)),
% 60.39/60.46 inference(scs_inference,[],[51,44,913,1056,185,95,325,317,4,420,422,436,24,417])).
% 60.39/60.46 cnf(1101,plain,
% 60.39/60.46 (~P5(x11011,x11011)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(1104,plain,
% 60.39/60.46 (~E(f3(a65),f3(a43))),
% 60.39/60.46 inference(scs_inference,[],[51,46,44,913,1056,185,95,441,1101,325,317,4,420,422,436,24,417,23,22,25])).
% 60.39/60.46 cnf(1130,plain,
% 60.39/60.46 (~P8(f3(a54),f3(a1))),
% 60.39/60.46 inference(scs_inference,[],[43,807,1091,187,97,4,422,420])).
% 60.39/60.46 cnf(1136,plain,
% 60.39/60.46 (~E(f3(a1),f3(a54))),
% 60.39/60.46 inference(scs_inference,[],[51,43,807,1091,187,97,327,4,422,420,417,436,24])).
% 60.39/60.46 cnf(1138,plain,
% 60.39/60.46 (~P5(x11381,x11381)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(1141,plain,
% 60.39/60.46 (~E(f3(a65),f3(a4))),
% 60.39/60.46 inference(scs_inference,[],[51,46,43,807,1091,187,97,441,1138,327,4,422,420,417,436,24,23,22,25])).
% 60.39/60.46 cnf(1165,plain,
% 60.39/60.46 (~P8(f3(a65),f3(a54))),
% 60.39/60.46 inference(scs_inference,[],[46,839,534,4,420])).
% 60.39/60.46 cnf(1173,plain,
% 60.39/60.46 (~E(f3(a2),f3(a54))),
% 60.39/60.46 inference(scs_inference,[],[51,42,46,839,1130,189,99,328,534,327,4,420,422,417,436,24])).
% 60.39/60.46 cnf(1175,plain,
% 60.39/60.46 (~P5(x11751,x11751)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(1177,plain,
% 60.39/60.46 (~P5(x11771,x11771)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(1178,plain,
% 60.39/60.46 (~E(f3(a65),f3(a1))),
% 60.39/60.46 inference(scs_inference,[],[51,42,46,839,1130,189,99,441,1175,328,534,327,4,420,422,417,436,24,23,22,25])).
% 60.39/60.46 cnf(1180,plain,
% 60.39/60.46 (~P5(x11801,x11801)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(1185,plain,
% 60.39/60.46 (P10(a194,a64,a2)),
% 60.39/60.46 inference(scs_inference,[],[51,42,46,839,1130,189,190,101,99,441,1175,1177,1180,328,534,327,4,420,422,417,436,24,23,22,25,418,419,430])).
% 60.39/60.46 cnf(1204,plain,
% 60.39/60.46 (~P8(f3(a65),f3(a43))),
% 60.39/60.46 inference(scs_inference,[],[45,844,1165,191,101,4,422,420])).
% 60.39/60.46 cnf(1212,plain,
% 60.39/60.46 (~P5(x12121,x12121)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(1215,plain,
% 60.39/60.46 (~E(f3(a76),f3(a54))),
% 60.39/60.46 inference(scs_inference,[],[51,47,45,844,1165,191,101,441,1212,329,327,4,422,420,417,436,24,23,22,25])).
% 60.39/60.46 cnf(1231,plain,
% 60.39/60.46 (~P8(f3(a65),f3(a4))),
% 60.39/60.46 inference(scs_inference,[],[44,876,1204,4,420])).
% 60.39/60.46 cnf(1235,plain,
% 60.39/60.46 (P5(a199,a2)),
% 60.39/60.46 inference(scs_inference,[],[51,44,876,1204,193,103,4,420,422,417])).
% 60.39/60.46 cnf(1241,plain,
% 60.39/60.46 (~P5(x12411,x12411)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(1244,plain,
% 60.39/60.46 (~E(f3(a76),f3(a43))),
% 60.39/60.46 inference(scs_inference,[],[51,47,44,876,1204,193,103,441,1241,330,318,4,420,422,417,436,24,23,22,25])).
% 60.39/60.46 cnf(1270,plain,
% 60.39/60.46 (~P8(f3(a65),f3(a1))),
% 60.39/60.46 inference(scs_inference,[],[43,881,1231,195,105,4,422,420])).
% 60.39/60.46 cnf(1276,plain,
% 60.39/60.46 (~E(f3(a1),f3(a65))),
% 60.39/60.46 inference(scs_inference,[],[51,43,881,1231,195,105,331,327,4,422,420,417,436,24])).
% 60.39/60.46 cnf(1305,plain,
% 60.39/60.46 (~P8(f3(a87),f3(a76))),
% 60.39/60.46 inference(scs_inference,[],[48,918,566,4,420])).
% 60.39/60.46 cnf(1313,plain,
% 60.39/60.46 (~E(f3(a2),f3(a65))),
% 60.39/60.46 inference(scs_inference,[],[51,42,48,918,1270,197,107,332,566,309,4,420,422,417,436,24])).
% 60.39/60.46 cnf(1315,plain,
% 60.39/60.46 (~P5(x13151,x13151)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(1317,plain,
% 60.39/60.46 (~P5(x13171,x13171)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(1320,plain,
% 60.39/60.46 (~P5(x13201,x13201)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(1325,plain,
% 60.39/60.46 (P10(a203,a73,a2)),
% 60.39/60.46 inference(scs_inference,[],[51,42,47,48,918,1270,197,198,109,107,441,1315,1317,1320,332,566,309,4,420,422,417,436,24,23,22,25,418,419,430])).
% 60.39/60.46 cnf(1344,plain,
% 60.39/60.46 (~P8(f3(a87),f3(a65))),
% 60.39/60.46 inference(scs_inference,[],[47,950,1305,199,109,4,422,420])).
% 60.39/60.46 cnf(1346,plain,
% 60.39/60.46 (P5(a205,a2)),
% 60.39/60.46 inference(scs_inference,[],[51,47,950,1305,199,109,4,422,420,417])).
% 60.39/60.46 cnf(1350,plain,
% 60.39/60.46 (~E(f3(a65),f3(a87))),
% 60.39/60.46 inference(scs_inference,[],[51,47,950,1305,199,109,333,318,4,422,420,417,436,24])).
% 60.39/60.46 cnf(1352,plain,
% 60.39/60.46 (~P5(x13521,x13521)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(1354,plain,
% 60.39/60.46 (~P5(x13541,x13541)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(1355,plain,
% 60.39/60.46 (~E(f3(a98),f3(a76))),
% 60.39/60.46 inference(scs_inference,[],[51,49,47,950,1305,199,109,441,1352,333,318,4,422,420,417,436,24,23,22,25])).
% 60.39/60.46 cnf(1357,plain,
% 60.39/60.46 (~P5(x13571,x13571)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(1362,plain,
% 60.39/60.46 (P10(a205,a75,a2)),
% 60.39/60.46 inference(scs_inference,[],[51,49,47,950,1305,199,200,111,109,441,1352,1354,1357,333,318,4,422,420,417,436,24,23,22,25,418,419,430])).
% 60.39/60.46 cnf(1371,plain,
% 60.39/60.46 (~P8(f3(a87),f3(a54))),
% 60.39/60.46 inference(scs_inference,[],[46,955,1344,4,420])).
% 60.39/60.46 cnf(1379,plain,
% 60.39/60.46 (~E(f3(a54),f3(a87))),
% 60.39/60.46 inference(scs_inference,[],[51,46,955,1344,201,111,334,327,4,420,422,417,436,24])).
% 60.39/60.46 cnf(1381,plain,
% 60.39/60.46 (~P5(x13811,x13811)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(1384,plain,
% 60.39/60.46 (~E(f3(a98),f3(a65))),
% 60.39/60.46 inference(scs_inference,[],[51,49,46,955,1344,201,111,441,1381,334,327,4,420,422,417,436,24,23,22,25])).
% 60.39/60.46 cnf(1401,plain,
% 60.39/60.46 (~P8(f3(a87),f3(a43))),
% 60.39/60.46 inference(scs_inference,[],[45,987,1371,4,420])).
% 60.39/60.46 cnf(1409,plain,
% 60.39/60.46 (~E(f3(a43),f3(a87))),
% 60.39/60.46 inference(scs_inference,[],[51,45,987,1371,203,113,337,4,420,422,417,436,24])).
% 60.39/60.46 cnf(1411,plain,
% 60.39/60.46 (~P5(x14111,x14111)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(1414,plain,
% 60.39/60.46 (~E(f3(a98),f3(a54))),
% 60.39/60.46 inference(scs_inference,[],[51,49,45,987,1371,203,113,441,1411,337,4,420,422,417,436,24,23,22,25])).
% 60.39/60.46 cnf(1438,plain,
% 60.39/60.46 (~P8(f3(a87),f3(a4))),
% 60.39/60.46 inference(scs_inference,[],[44,992,1401,4,420])).
% 60.39/60.46 cnf(1483,plain,
% 60.39/60.46 (~E(f3(a1),f3(a87))),
% 60.39/60.46 inference(scs_inference,[],[51,43,1350,1438,207,117,339,319,4,420,422,417,436,24])).
% 60.39/60.46 cnf(1485,plain,
% 60.39/60.46 (~P5(x14851,x14851)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(1488,plain,
% 60.39/60.46 (~E(f3(a98),f3(a4))),
% 60.39/60.46 inference(scs_inference,[],[51,49,43,1350,1438,207,117,441,1485,339,319,4,420,422,417,436,24,23,22,25])).
% 60.39/60.46 cnf(1505,plain,
% 60.39/60.46 (~P8(f3(a98),f3(a87))),
% 60.39/60.46 inference(scs_inference,[],[49,1025,592,4,420])).
% 60.39/60.46 cnf(1533,plain,
% 60.39/60.46 (P7(f250(f3(x15331),f3(a1)))),
% 60.39/60.46 inference(scs_inference,[],[33,410,415])).
% 60.39/60.46 cnf(1535,plain,
% 60.39/60.46 (~P8(f3(a98),f3(a76))),
% 60.39/60.46 inference(scs_inference,[],[48,1030,1505,4,420])).
% 60.39/60.46 cnf(1543,plain,
% 60.39/60.46 (~E(f3(a76),f3(a98))),
% 60.39/60.46 inference(scs_inference,[],[51,48,1030,1505,211,121,341,328,4,420,422,417,436,24])).
% 60.39/60.46 cnf(1572,plain,
% 60.39/60.46 (~P8(f3(a98),f3(a65))),
% 60.39/60.46 inference(scs_inference,[],[47,1062,1535,4,420])).
% 60.39/60.46 cnf(1582,plain,
% 60.39/60.46 (~P5(x15821,x15821)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(1585,plain,
% 60.39/60.46 (~E(f3(a109),f3(a76))),
% 60.39/60.46 inference(scs_inference,[],[51,50,47,1062,1535,213,123,441,1582,342,319,4,420,422,436,417,24,23,22,25])).
% 60.39/60.46 cnf(1609,plain,
% 60.39/60.46 (~P8(f3(a98),f3(a54))),
% 60.39/60.46 inference(scs_inference,[],[46,1067,1572,4,420])).
% 60.39/60.46 cnf(1617,plain,
% 60.39/60.46 (~E(f3(a54),f3(a98))),
% 60.39/60.46 inference(scs_inference,[],[51,46,1067,1572,215,125,343,310,4,420,422,417,436,24])).
% 60.39/60.46 cnf(1638,plain,
% 60.39/60.46 (~P8(f3(a98),f3(a43))),
% 60.39/60.46 inference(scs_inference,[],[45,1097,1609,4,420])).
% 60.39/60.46 cnf(1642,plain,
% 60.39/60.46 (P5(a225,a2)),
% 60.39/60.46 inference(scs_inference,[],[51,45,1097,1609,217,127,4,420,422,417])).
% 60.39/60.46 cnf(1646,plain,
% 60.39/60.46 (~E(f3(a43),f3(a98))),
% 60.39/60.46 inference(scs_inference,[],[51,45,1097,1609,217,127,347,4,420,422,417,436,24])).
% 60.39/60.46 cnf(1675,plain,
% 60.39/60.46 (~P8(f3(a98),f3(a4))),
% 60.39/60.46 inference(scs_inference,[],[44,1543,1638,4,420])).
% 60.39/60.46 cnf(1681,plain,
% 60.39/60.46 (P6(f3(a1),f3(a4),f3(a4),f3(a65))),
% 60.39/60.46 inference(scs_inference,[],[51,44,1543,1638,219,129,348,329,4,420,422,417,436])).
% 60.39/60.46 cnf(1685,plain,
% 60.39/60.46 (~P5(x16851,x16851)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(1688,plain,
% 60.39/60.46 (~E(f3(a109),f3(a43))),
% 60.39/60.46 inference(scs_inference,[],[51,50,44,1543,1638,219,129,441,1685,348,329,4,420,422,417,436,24,23,22,25])).
% 60.39/60.46 cnf(1712,plain,
% 60.39/60.46 (~P8(f3(a98),f3(a1))),
% 60.39/60.46 inference(scs_inference,[],[43,1104,1675,4,420])).
% 60.39/60.46 cnf(1749,plain,
% 60.39/60.46 (~P8(f3(a109),f3(a98))),
% 60.39/60.46 inference(scs_inference,[],[50,1379,595,4,420])).
% 60.39/60.46 cnf(1759,plain,
% 60.39/60.46 (~P5(x17591,x17591)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(1762,plain,
% 60.39/60.46 (~E(f3(a109),f3(a1))),
% 60.39/60.46 inference(scs_inference,[],[51,42,50,1379,1712,223,133,441,1759,350,595,347,4,420,417,422,436,24,23,22,25])).
% 60.39/60.46 cnf(1786,plain,
% 60.39/60.46 (~P8(f3(a109),f3(a87))),
% 60.39/60.46 inference(scs_inference,[],[49,1136,1749,4,420])).
% 60.39/60.46 cnf(1790,plain,
% 60.39/60.46 (P5(a234,a2)),
% 60.39/60.46 inference(scs_inference,[],[51,49,1136,1749,225,135,4,420,422,417])).
% 60.39/60.46 cnf(1794,plain,
% 60.39/60.46 (~E(f3(a87),f3(a109))),
% 60.39/60.46 inference(scs_inference,[],[51,49,1136,1749,225,135,351,311,4,420,422,417,436,24])).
% 60.39/60.46 cnf(1822,plain,
% 60.39/60.46 (~P8(f3(a109),f3(a76))),
% 60.39/60.46 inference(scs_inference,[],[48,1173,1786,4,420])).
% 60.39/60.46 cnf(1826,plain,
% 60.39/60.46 (P10(a106,a236,a2)),
% 60.39/60.46 inference(scs_inference,[],[48,55,64,1173,1786,227,137,4,420,417,422])).
% 60.39/60.46 cnf(1830,plain,
% 60.39/60.46 (~E(f3(a76),f3(a109))),
% 60.39/60.46 inference(scs_inference,[],[48,55,64,1173,1786,227,137,352,329,4,420,417,422,436,24])).
% 60.39/60.46 cnf(1832,plain,
% 60.39/60.46 (~P5(x18321,x18321)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(1834,plain,
% 60.39/60.46 (~P5(x18341,x18341)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(1836,plain,
% 60.39/60.46 (~P5(x18361,x18361)),
% 60.39/60.46 inference(rename_variables,[],[441])).
% 60.39/60.46 cnf(1848,plain,
% 60.39/60.46 (P9(x18481,f120(f3(a54)))+~E(a54,x18481)),
% 60.39/60.46 inference(scs_inference,[],[922,48,55,64,1173,1681,1786,227,228,139,137,441,1832,1834,1836,352,329,4,420,417,422,436,24,23,22,418,419,414,15,11,32,16,30,26])).
% 60.39/60.46 cnf(1856,plain,
% 60.39/60.46 (~P8(f3(a109),f3(a65))),
% 60.39/60.46 inference(scs_inference,[],[47,1141,1822,4,420])).
% 60.39/60.46 cnf(1864,plain,
% 60.39/60.46 (~E(f3(a65),f3(a109))),
% 60.39/60.46 inference(scs_inference,[],[47,64,1141,1822,229,70,139,357,4,420,417,422,436,24])).
% 60.39/60.46 cnf(1890,plain,
% 60.39/60.46 (~P8(f3(a109),f3(a54))),
% 60.39/60.46 inference(scs_inference,[],[46,1178,1856,4,420])).
% 60.39/60.46 cnf(1898,plain,
% 60.39/60.46 (~E(f3(a54),f3(a109))),
% 60.39/60.46 inference(scs_inference,[],[46,64,1178,1856,231,72,141,358,339,4,420,417,422,436,24])).
% 60.52/60.46 cnf(1924,plain,
% 60.52/60.46 (~P8(f3(a109),f3(a43))),
% 60.52/60.46 inference(scs_inference,[],[45,1794,1890,4,420])).
% 60.52/60.46 cnf(1928,plain,
% 60.52/60.46 (P10(a112,a242,a2)),
% 60.52/60.46 inference(scs_inference,[],[45,64,1794,1890,232,74,142,4,420,417,422])).
% 60.52/60.46 cnf(1932,plain,
% 60.52/60.46 (~E(f3(a43),f3(a109))),
% 60.52/60.46 inference(scs_inference,[],[45,64,1794,1890,232,74,142,359,348,4,420,417,422,436,24])).
% 60.52/60.46 cnf(1958,plain,
% 60.52/60.46 (~P8(f3(a109),f3(a4))),
% 60.52/60.46 inference(scs_inference,[],[44,1830,1924,4,420])).
% 60.52/60.46 cnf(1966,plain,
% 60.52/60.46 (~E(f3(a4),f3(a109))),
% 60.52/60.46 inference(scs_inference,[],[44,64,1830,1924,235,76,145,360,357,4,420,417,422,436,24])).
% 60.52/60.46 cnf(2000,plain,
% 60.52/60.46 (~E(f3(a1),f3(a109))),
% 60.52/60.46 inference(scs_inference,[],[43,64,1864,1958,236,78,146,361,339,4,420,417,422,436,24])).
% 60.52/60.46 cnf(2028,plain,
% 60.52/60.46 (P10(a119,a249,a2)),
% 60.52/60.46 inference(scs_inference,[],[64,1898,239,80,149,4,417,422])).
% 60.52/60.46 cnf(2096,plain,
% 60.52/60.46 (P6(f3(a4),f3(a65),f3(a1),f3(a98))),
% 60.52/60.46 inference(scs_inference,[],[64,1932,242,84,152,369,358,4,417,422,436])).
% 60.52/60.46 cnf(2125,plain,
% 60.52/60.46 (P10(a126,a255,a2)),
% 60.52/60.46 inference(scs_inference,[],[64,1966,244,86,154,4,417,422])).
% 60.52/60.46 cnf(2156,plain,
% 60.52/60.46 (P10(a128,a257,a2)),
% 60.52/60.46 inference(scs_inference,[],[64,2000,246,88,156,4,417,422])).
% 60.52/60.46 cnf(2189,plain,
% 60.52/60.46 (P6(f3(a1),f3(a65),f3(a4),f3(a98))),
% 60.52/60.46 inference(scs_inference,[],[64,1215,248,90,158,378,359,4,417,422,436])).
% 60.52/60.46 cnf(2243,plain,
% 60.52/60.46 (P6(f3(a2),f3(a98),f3(a2),f3(a98))),
% 60.52/60.46 inference(scs_inference,[],[64,1244,94,286,258,387,4,417,422,436])).
% 60.52/60.46 cnf(2265,plain,
% 60.52/60.46 (P10(a25,a154,a2)),
% 60.52/60.46 inference(scs_inference,[],[64,1276,96,295,267,4,417,422])).
% 60.52/60.46 cnf(2270,plain,
% 60.52/60.46 (~P5(x22701,x22701)),
% 60.52/60.46 inference(rename_variables,[],[441])).
% 60.52/60.46 cnf(2272,plain,
% 60.52/60.46 (~P5(x22721,x22721)),
% 60.52/60.46 inference(rename_variables,[],[441])).
% 60.52/60.46 cnf(2274,plain,
% 60.52/60.46 (~P5(x22741,x22741)),
% 60.52/60.46 inference(rename_variables,[],[441])).
% 60.52/60.46 cnf(2284,plain,
% 60.52/60.46 (P9(x22841,f120(f250(f3(a76),f3(a43))))+~E(a61,x22841)),
% 60.52/60.46 inference(scs_inference,[],[64,1276,2096,96,295,305,256,267,441,2270,2272,2274,372,388,315,4,417,422,436,23,22,418,419,414,14,10,15,26])).
% 60.52/60.46 cnf(2322,plain,
% 60.52/60.46 (P6(f3(a76),f3(a2),f3(a4),f3(a98))),
% 60.52/60.46 inference(scs_inference,[],[64,1313,100,304,276,333,309,4,417,422,436])).
% 60.52/60.46 cnf(2376,plain,
% 60.52/60.46 (P6(f3(a4),f3(a43),f3(a43),f3(a98))),
% 60.52/60.46 inference(scs_inference,[],[64,1355,104,282,254,369,340,4,417,422,436])).
% 60.52/60.46 cnf(2379,plain,
% 60.52/60.46 (~P5(x23791,x23791)),
% 60.52/60.46 inference(rename_variables,[],[441])).
% 60.52/60.46 cnf(2381,plain,
% 60.52/60.46 (~P5(x23811,x23811)),
% 60.52/60.46 inference(rename_variables,[],[441])).
% 60.52/60.46 cnf(2383,plain,
% 60.52/60.46 (~P5(x23831,x23831)),
% 60.52/60.46 inference(rename_variables,[],[441])).
% 60.52/60.46 cnf(2392,plain,
% 60.52/60.46 (P9(x23921,f120(f250(f3(a54),f3(a54))))+~E(a70,x23921)),
% 60.52/60.46 inference(scs_inference,[],[64,1355,2189,104,282,292,274,254,441,2379,2381,2383,374,369,340,4,417,422,436,22,23,418,419,414,16,13,26])).
% 60.52/60.46 cnf(2407,plain,
% 60.52/60.46 (P6(f3(a43),f3(a54),f3(a4),f3(a109))),
% 60.52/60.46 inference(scs_inference,[],[64,1384,106,302,274,370,349,4,417,422,436])).
% 60.52/60.46 cnf(2441,plain,
% 60.52/60.46 (~P5(x24411,x24411)),
% 60.52/60.46 inference(rename_variables,[],[441])).
% 60.52/60.46 cnf(2443,plain,
% 60.52/60.46 (~P5(x24431,x24431)),
% 60.52/60.46 inference(rename_variables,[],[441])).
% 60.52/60.46 cnf(2445,plain,
% 60.52/60.46 (~P5(x24451,x24451)),
% 60.52/60.46 inference(rename_variables,[],[441])).
% 60.52/60.46 cnf(2455,plain,
% 60.52/60.46 (P9(x24551,f120(f250(f3(a98),f3(a54))))+~E(a74,x24551)),
% 60.52/60.46 inference(scs_inference,[],[1185,64,1409,2243,108,291,301,252,263,441,2441,2443,2445,377,378,4,417,436,422,22,23,418,419,414,15,31,16,26])).
% 60.52/60.46 cnf(2467,plain,
% 60.52/60.46 (P6(f3(a4),f3(a65),f3(a4),f3(a109))),
% 60.52/60.46 inference(scs_inference,[],[64,1414,110,379,359,4,417,436])).
% 60.52/60.46 cnf(2545,plain,
% 60.52/60.46 (P6(f3(a87),f3(a1),f3(a1),f3(a109))),
% 60.52/60.46 inference(scs_inference,[],[64,1483,116,334,318,4,417,436])).
% 60.52/60.46 cnf(2550,plain,
% 60.52/60.46 (~P5(x25501,x25501)),
% 60.52/60.46 inference(rename_variables,[],[441])).
% 60.52/60.46 cnf(2552,plain,
% 60.52/60.46 (~P5(x25521,x25521)),
% 60.52/60.46 inference(rename_variables,[],[441])).
% 60.52/60.46 cnf(2554,plain,
% 60.52/60.46 (~P5(x25541,x25541)),
% 60.52/60.46 inference(rename_variables,[],[441])).
% 60.52/60.46 cnf(2564,plain,
% 60.52/60.46 (P9(x25641,f120(f250(f3(a76),f3(a65))))+~E(a83,x25641)),
% 60.52/60.46 inference(scs_inference,[],[64,1483,2322,116,278,288,270,250,441,2550,2552,2554,334,318,4,417,436,422,22,23,418,419,414,15,14,17,26])).
% 60.52/60.46 cnf(2581,plain,
% 60.52/60.46 (~P5(x25811,x25811)),
% 60.52/60.46 inference(rename_variables,[],[441])).
% 60.52/60.46 cnf(2583,plain,
% 60.52/60.46 (~P5(x25831,x25831)),
% 60.52/60.46 inference(rename_variables,[],[441])).
% 60.52/60.46 cnf(2584,plain,
% 60.52/60.46 (~P8(f250(f3(a98),f250(f3(a4),f3(a1))),f250(f3(a98),f250(f3(a4),f3(a1))))),
% 60.52/60.46 inference(scs_inference,[],[64,1488,118,298,306,270,441,2581,2583,333,327,4,417,436,422,22,23,418])).
% 60.52/60.46 cnf(2684,plain,
% 60.52/60.46 (~P5(x26841,x26841)),
% 60.52/60.46 inference(rename_variables,[],[441])).
% 60.52/60.46 cnf(2693,plain,
% 60.52/60.46 (P9(x26931,f120(f250(f3(a98),f3(a76))))+~E(a96,x26931)),
% 60.52/60.46 inference(scs_inference,[],[64,128,72,162,1585,2376,441,2684,383,369,313,4,417,436,422,22,23,414,17,13,14,15,26])).
% 60.52/60.46 cnf(2709,plain,
% 60.52/60.46 (~P5(x27091,x27091)),
% 60.52/60.46 inference(rename_variables,[],[441])).
% 60.52/60.46 cnf(2718,plain,
% 60.52/60.46 (P9(x27181,f120(f250(f3(a2),f3(a87))))+~E(a99,x27181)),
% 60.52/60.46 inference(scs_inference,[],[1325,64,130,74,164,1617,2407,441,2709,384,370,322,4,417,436,422,22,23,414,12,31,15,32,26])).
% 60.52/60.46 cnf(2759,plain,
% 60.52/60.46 (~P5(x27591,x27591)),
% 60.52/60.46 inference(rename_variables,[],[441])).
% 60.52/60.46 cnf(2768,plain,
% 60.52/60.46 (P9(x27681,f120(f250(f3(a54),f3(a87))))+~E(a103,x27681)),
% 60.52/60.46 inference(scs_inference,[],[1362,64,134,78,168,1646,2467,441,2759,386,378,314,4,417,436,422,22,23,414,17,31,14,13,26])).
% 60.52/60.46 cnf(2834,plain,
% 60.52/60.46 (~P5(x28341,x28341)),
% 60.52/60.46 inference(rename_variables,[],[441])).
% 60.52/60.46 cnf(2840,plain,
% 60.52/60.46 (P9(x28401,f120(f250(f3(a2),f3(a98))))+~E(a110,x28401)),
% 60.52/60.46 inference(scs_inference,[],[64,140,84,174,1688,2545,441,2834,325,308,4,417,436,422,22,23,414,14,26])).
% 60.52/60.46 cnf(2931,plain,
% 60.52/60.46 (P4(a239,a121)),
% 60.52/60.46 inference(scs_inference,[],[450,1762,617,4,423])).
% 60.52/60.46 cnf(3218,plain,
% 60.52/60.46 (P6(f3(a4),f3(a65),f3(a2),f3(a87))),
% 60.52/60.46 inference(scs_inference,[],[450,64,266,983,357,359,423,417,436])).
% 60.52/60.46 cnf(3300,plain,
% 60.52/60.46 (P6(f3(a4),f3(a76),f3(a2),f3(a98))),
% 60.52/60.46 inference(scs_inference,[],[450,64,264,1098,367,369,423,417,436])).
% 60.52/60.46 cnf(3409,plain,
% 60.52/60.46 (P6(f3(a76),f3(a2),f3(a1),f3(a87))),
% 60.52/60.46 inference(scs_inference,[],[450,64,251,1235,323,308,423,417,436])).
% 60.52/60.46 cnf(3495,plain,
% 60.52/60.46 (~P5(x34951,x34951)),
% 60.52/60.46 inference(rename_variables,[],[441])).
% 60.52/60.46 cnf(3498,plain,
% 60.52/60.46 (~P5(a76,a184)),
% 60.52/60.46 inference(scs_inference,[],[450,64,57,132,222,441,3495,1346,334,309,423,417,436,422,23,22,414])).
% 60.52/60.46 cnf(3736,plain,
% 60.52/60.46 (~E(a119,a184)),
% 60.52/60.46 inference(scs_inference,[],[450,64,151,149,241,441,1642,361,357,423,417,436,422,23])).
% 60.52/60.46 cnf(3840,plain,
% 60.52/60.46 (P5(a184,a128)),
% 60.52/60.46 inference(scs_inference,[],[450,64,159,156,249,1790,360,330,423,422,436,417])).
% 60.52/60.46 cnf(3846,plain,
% 60.52/60.46 (~P5(x38461,x38461)),
% 60.52/60.46 inference(rename_variables,[],[441])).
% 60.52/60.46 cnf(3847,plain,
% 60.52/60.46 (~E(a128,a184)),
% 60.52/60.46 inference(scs_inference,[],[450,1826,64,159,156,249,441,3846,1790,360,330,423,422,436,417,414,32,22,23])).
% 60.52/60.46 cnf(3856,plain,
% 60.52/60.46 (P5(a184,a130)),
% 60.52/60.46 inference(scs_inference,[],[64,259,158,287,331,318,436,422,417])).
% 60.52/60.46 cnf(3880,plain,
% 60.52/60.46 (P5(a184,a27)),
% 60.52/60.46 inference(scs_inference,[],[64,268,269,296,332,327,422,436,417])).
% 60.52/60.46 cnf(3906,plain,
% 60.52/60.46 (P5(a184,a15)),
% 60.52/60.46 inference(scs_inference,[],[64,257,258,285,441,3880,342,310,436,422,22,417])).
% 60.52/60.46 cnf(3929,plain,
% 60.52/60.46 (~P5(x39291,x39291)),
% 60.52/60.46 inference(rename_variables,[],[441])).
% 60.52/60.46 cnf(3930,plain,
% 60.52/60.46 (P5(a184,a25)),
% 60.52/60.46 inference(scs_inference,[],[64,277,267,305,441,3906,341,337,436,422,22,417])).
% 60.52/60.46 cnf(3940,plain,
% 60.52/60.46 (P9(x39401,f120(f250(f3(a87),f250(f3(a4),f3(a1)))))+~E(a36,x39401)),
% 60.52/60.46 inference(scs_inference,[],[2931,64,277,267,305,3300,441,3929,3906,394,341,337,436,422,22,417,23,414,16,29,15,12,26])).
% 60.52/60.46 cnf(3953,plain,
% 60.52/60.46 (~P5(x39531,x39531)),
% 60.52/60.46 inference(rename_variables,[],[441])).
% 60.52/60.46 cnf(3956,plain,
% 60.52/60.46 (~E(a25,a184)),
% 60.52/60.46 inference(scs_inference,[],[64,266,256,294,441,3953,3930,343,328,422,436,22,417,23])).
% 60.52/60.46 cnf(3965,plain,
% 60.52/60.46 (P9(x39651,f120(f250(f3(a76),f250(f3(a1),f3(a1)))))+~E(a24,x39651)),
% 60.52/60.46 inference(scs_inference,[],[1928,64,266,256,294,3409,441,3953,3930,395,343,328,422,436,22,417,23,414,17,27,11,32,10,26])).
% 60.52/60.46 cnf(4024,plain,
% 60.52/60.46 (P5(a184,a11)),
% 60.52/60.46 inference(scs_inference,[],[64,264,254,292,339,310,436,422,417])).
% 60.52/60.46 cnf(4052,plain,
% 60.52/60.46 (~P5(x40521,x40521)),
% 60.52/60.46 inference(rename_variables,[],[441])).
% 60.52/60.46 cnf(4057,plain,
% 60.52/60.46 (P9(x40571,f120(f250(f3(a43),f250(f3(a2),f3(a1)))))+~E(a10,x40571)),
% 60.52/60.46 inference(scs_inference,[],[64,253,274,281,441,4052,4024,311,348,436,422,417,22,23,414,26])).
% 60.52/60.46 cnf(4115,plain,
% 60.52/60.46 (P5(a184,a31)),
% 60.52/60.46 inference(scs_inference,[],[64,251,272,279,329,318,436,422,417])).
% 60.52/60.46 cnf(4142,plain,
% 60.52/60.46 (~P5(x41421,x41421)),
% 60.52/60.46 inference(rename_variables,[],[441])).
% 60.52/60.46 cnf(4148,plain,
% 60.52/60.46 (P9(x41481,f120(f250(f3(a1),f250(f3(a4),f3(a1)))))+~E(a30,x41481)),
% 60.52/60.46 inference(scs_inference,[],[64,271,261,299,3218,441,4142,4115,311,349,436,422,417,23,22,414,16,26])).
% 60.52/60.46 cnf(4519,plain,
% 60.52/60.46 (P5(a184,a64)),
% 60.52/60.46 inference(scs_inference,[],[64,99,417])).
% 60.52/60.46 cnf(4535,plain,
% 60.52/60.46 (P5(a184,a67)),
% 60.52/60.46 inference(scs_inference,[],[64,101,313,368,436,417])).
% 60.52/60.46 cnf(4538,plain,
% 60.52/60.46 (~P5(x45381,x45381)),
% 60.52/60.46 inference(rename_variables,[],[441])).
% 60.52/60.46 cnf(4541,plain,
% 60.52/60.46 (~P5(a67,a184)),
% 60.52/60.46 inference(scs_inference,[],[64,101,441,4538,313,368,4519,436,417,23,22,414])).
% 60.52/60.46 cnf(4559,plain,
% 60.52/60.46 (P7(f3(a4))),
% 60.52/60.46 inference(scs_inference,[],[4535,34,412,410])).
% 60.52/60.46 cnf(4569,plain,
% 60.52/60.46 (~E(a67,a184)),
% 60.52/60.46 inference(scs_inference,[],[2028,4535,34,1533,49,412,410,415,421,426,416,409])).
% 60.52/60.46 cnf(4572,plain,
% 60.52/60.46 (~P10(a184,a249,a2)),
% 60.52/60.46 inference(scs_inference,[],[546,2028,3736,4535,34,1533,49,412,410,415,421,426,416,409,2,429])).
% 60.52/60.46 cnf(4576,plain,
% 60.52/60.46 (P8(f3(a76),f3(a98))),
% 60.52/60.46 inference(scs_inference,[],[523,546,2028,3736,4535,34,458,1533,49,48,412,410,415,421,426,416,409,2,429,428,420])).
% 60.52/60.46 cnf(4592,plain,
% 60.52/60.46 (~P9(a154,f120(x45921))),
% 60.52/60.46 inference(scs_inference,[],[523,546,2028,3736,4535,34,452,537,2584,458,1533,295,529,370,397,49,48,43,51,64,441,412,410,415,421,426,416,409,2,429,428,420,424,427,413,25,24,422,31,436,27,417])).
% 60.52/60.46 cnf(4593,plain,
% 60.52/60.46 (~P5(x45931,x45931)),
% 60.52/60.46 inference(rename_variables,[],[441])).
% 60.52/60.46 cnf(4599,plain,
% 60.52/60.46 (P10(a154,a25,a2)),
% 60.52/60.46 inference(scs_inference,[],[523,546,2028,3736,4535,34,452,537,2584,458,1533,295,529,2265,335,267,370,397,327,308,49,48,43,51,64,441,4593,412,410,415,421,426,416,409,2,429,428,420,424,427,413,25,24,422,31,436,27,417,22,437,430])).
% 60.52/60.46 cnf(4618,plain,
% 60.52/60.46 (~P9(a154,f120(x46181))),
% 60.52/60.46 inference(rename_variables,[],[4592])).
% 60.52/60.46 cnf(4620,plain,
% 60.52/60.46 (~P9(a154,f120(x46201))),
% 60.52/60.46 inference(rename_variables,[],[4592])).
% 60.52/60.46 cnf(4622,plain,
% 60.52/60.46 (~P9(a154,f120(x46221))),
% 60.52/60.46 inference(rename_variables,[],[4592])).
% 60.52/60.46 cnf(4624,plain,
% 60.52/60.46 (~P9(a154,f120(x46241))),
% 60.52/60.46 inference(rename_variables,[],[4592])).
% 60.52/60.46 cnf(4626,plain,
% 60.52/60.46 (~P9(a154,f120(x46261))),
% 60.52/60.46 inference(rename_variables,[],[4592])).
% 60.52/60.46 cnf(4628,plain,
% 60.52/60.46 (~P9(a154,f120(x46281))),
% 60.52/60.46 inference(rename_variables,[],[4592])).
% 60.52/60.46 cnf(4630,plain,
% 60.52/60.46 (~P9(a154,f120(x46301))),
% 60.52/60.46 inference(rename_variables,[],[4592])).
% 60.52/60.46 cnf(4632,plain,
% 60.52/60.46 (~P9(a154,f120(x46321))),
% 60.52/60.46 inference(rename_variables,[],[4592])).
% 60.52/60.46 cnf(4634,plain,
% 60.52/60.46 (~P9(a154,f120(x46341))),
% 60.52/60.46 inference(rename_variables,[],[4592])).
% 60.52/60.46 cnf(4636,plain,
% 60.52/60.46 (~P9(a154,f120(x46361))),
% 60.52/60.46 inference(rename_variables,[],[4592])).
% 60.52/60.46 cnf(4638,plain,
% 60.52/60.46 (~P9(a154,f120(x46381))),
% 60.52/60.46 inference(rename_variables,[],[4592])).
% 60.52/60.46 cnf(4640,plain,
% 60.52/60.46 (~P9(a154,f120(x46401))),
% 60.52/60.46 inference(rename_variables,[],[4592])).
% 60.52/60.46 cnf(4642,plain,
% 60.52/60.46 (~P9(a154,f120(x46421))),
% 60.52/60.46 inference(rename_variables,[],[4592])).
% 60.52/60.46 cnf(4644,plain,
% 60.52/60.46 (~P9(a154,f120(x46441))),
% 60.52/60.46 inference(rename_variables,[],[4592])).
% 60.52/60.46 cnf(4646,plain,
% 60.52/60.46 (~P9(a154,f120(x46461))),
% 60.52/60.46 inference(rename_variables,[],[4592])).
% 60.52/60.46 cnf(4648,plain,
% 60.52/60.46 (~P9(a154,f120(x46481))),
% 60.52/60.46 inference(rename_variables,[],[4592])).
% 60.52/60.46 cnf(4655,plain,
% 60.52/60.46 (P7(f3(a43))),
% 60.52/60.46 inference(scs_inference,[],[2125,4559,4576,4592,4618,4620,4622,4624,4626,4628,4630,4632,4634,4636,4638,4640,4642,4644,4646,35,603,678,715,1848,2284,2392,2455,2564,2693,2718,2768,2840,3940,3965,4057,4148,421,426,415,410])).
% 60.52/60.46 cnf(4662,plain,
% 60.52/60.46 (~P10(a4,a4,a2)),
% 60.52/60.46 inference(scs_inference,[],[489,575,2125,4559,4576,4592,4618,4620,4622,4624,4626,4628,4630,4632,4634,4636,4638,4640,4642,4644,4646,35,3856,494,603,678,715,1848,2284,2392,2455,2564,2693,2718,2768,2840,3940,3965,4057,4148,421,426,415,410,412,416,2,429])).
% 60.52/60.46 cnf(4666,plain,
% 60.52/60.46 (P8(f3(a76),f3(a109))),
% 60.52/60.46 inference(scs_inference,[],[489,514,575,2125,4559,4576,4592,4618,4620,4622,4624,4626,4628,4630,4632,4634,4636,4638,4640,4642,4644,4646,35,3856,494,50,603,678,715,1848,2284,2392,2455,2564,2693,2718,2768,2840,3940,3965,4057,4148,421,426,415,410,412,416,2,429,428,420])).
% 60.52/60.46 cnf(4679,plain,
% 60.52/60.46 (~P9(a142,f120(x46791))),
% 60.52/60.46 inference(scs_inference,[],[489,514,575,2125,4541,4569,4572,4559,4576,4592,4618,4620,4622,4624,4626,4628,4630,4632,4634,4636,4638,4640,4642,4644,4646,4648,35,3856,494,284,458,70,239,50,441,603,678,715,1848,2284,2392,2455,2564,2693,2718,2768,2840,3940,3965,4057,4148,421,426,415,410,412,416,2,429,428,420,424,427,413,422,26,30,417])).
% 60.52/60.46 cnf(4680,plain,
% 60.52/60.46 (~P5(x46801,x46801)),
% 60.52/60.46 inference(rename_variables,[],[441])).
% 60.52/60.46 cnf(4694,plain,
% 60.52/60.46 (~P6(f3(a2),f3(a65),f3(a4),f3(a87))),
% 60.52/60.46 inference(scs_inference,[],[489,514,575,2125,4541,4569,4572,4559,4576,4592,4618,4620,4622,4624,4626,4628,4630,4632,4634,4636,4638,4640,4642,4644,4646,4648,35,3856,442,494,3498,284,458,398,70,68,239,62,56,58,361,57,53,308,50,51,441,4680,603,678,715,1848,2284,2392,2455,2564,2693,2718,2768,2840,3940,3965,4057,4148,421,426,415,410,412,416,2,429,428,420,424,427,413,422,26,30,417,437,430,419,418,504,423,431])).
% 60.52/60.46 cnf(4701,plain,
% 60.52/60.46 (~P9(a142,f120(x47011))),
% 60.52/60.46 inference(rename_variables,[],[4679])).
% 60.52/60.46 cnf(4703,plain,
% 60.52/60.46 (~P9(a142,f120(x47031))),
% 60.52/60.46 inference(rename_variables,[],[4679])).
% 60.52/60.46 cnf(4705,plain,
% 60.52/60.46 (~P9(a142,f120(x47051))),
% 60.52/60.46 inference(rename_variables,[],[4679])).
% 60.52/60.46 cnf(4707,plain,
% 60.52/60.46 (~P9(a142,f120(x47071))),
% 60.52/60.46 inference(rename_variables,[],[4679])).
% 60.52/60.46 cnf(4709,plain,
% 60.52/60.46 (~P9(a142,f120(x47091))),
% 60.52/60.46 inference(rename_variables,[],[4679])).
% 60.52/60.46 cnf(4711,plain,
% 60.52/60.46 (~P9(a142,f120(x47111))),
% 60.52/60.46 inference(rename_variables,[],[4679])).
% 60.52/60.46 cnf(4715,plain,
% 60.52/60.46 (~P9(a142,f120(x47151))),
% 60.52/60.46 inference(rename_variables,[],[4679])).
% 60.52/60.46 cnf(4717,plain,
% 60.52/60.46 (~P9(a142,f120(x47171))),
% 60.52/60.46 inference(rename_variables,[],[4679])).
% 60.52/60.46 cnf(4719,plain,
% 60.52/60.46 (~P9(a142,f120(x47191))),
% 60.52/60.46 inference(rename_variables,[],[4679])).
% 60.52/60.46 cnf(4723,plain,
% 60.52/60.46 (~P9(a142,f120(x47231))),
% 60.52/60.46 inference(rename_variables,[],[4679])).
% 60.52/60.46 cnf(4727,plain,
% 60.52/60.46 (~P9(a142,f120(x47271))),
% 60.52/60.46 inference(rename_variables,[],[4679])).
% 60.52/60.46 cnf(4729,plain,
% 60.52/60.46 (~P9(a142,f120(x47291))),
% 60.52/60.46 inference(rename_variables,[],[4679])).
% 60.52/60.46 cnf(4731,plain,
% 60.52/60.46 (~P9(a142,f120(x47311))),
% 60.52/60.46 inference(rename_variables,[],[4679])).
% 60.52/60.46 cnf(4733,plain,
% 60.52/60.46 (~P9(a142,f120(x47331))),
% 60.52/60.46 inference(rename_variables,[],[4679])).
% 60.52/60.46 cnf(4735,plain,
% 60.52/60.46 (~P9(a142,f120(x47351))),
% 60.52/60.46 inference(rename_variables,[],[4679])).
% 60.52/60.46 cnf(4757,plain,
% 60.52/60.46 ($false),
% 60.52/60.46 inference(scs_inference,[],[556,649,2156,3847,3956,4662,4599,4655,4666,4679,4701,4703,4705,4707,4709,4711,4715,4717,4719,4723,4727,4729,4731,4733,4735,4694,36,3840,569,377,359,53,47,421,1848,2455,2564,2693,2718,3965,415,2284,4057,3940,410,715,412,678,4148,2392,2840,603,426,2768,416,2,429,428,420,424,427,413,422,436]),
% 60.52/60.46 ['proof']).
% 60.52/60.46 % SZS output end Proof
% 60.52/60.46 % Total time :59.760000s
%------------------------------------------------------------------------------