%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : NUM338+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 : n022.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:53 EDT 2024
% Result : Theorem 63.07s 63.19s
% Output : CNFRefutation 63.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : NUM338+1 : TPTP v8.2.0. Released v3.1.0.
% 0.12/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n022.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Sun Jun 23 02:52:54 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.51/0.58 start to proof:theBenchmark
% 63.07/63.18 %-------------------------------------------
% 63.07/63.18 % File :CSE---1.7
% 63.07/63.18 % Problem :theBenchmark
% 63.07/63.18 % Transform :cnf
% 63.07/63.18 % Format :tptp:raw
% 63.07/63.18 % Command :java -jar mcs_scs.jar %d %s
% 63.07/63.18
% 63.07/63.18 % Result :Theorem 62.450000s
% 63.07/63.18 % Output :CNFRefutation 62.450000s
% 63.07/63.18 %-------------------------------------------
% 63.07/63.19 %------------------------------------------------------------------------------
% 63.07/63.19 % File : NUM338+1 : TPTP v8.2.0. Released v3.1.0.
% 63.07/63.19 % Domain : Number Theory (RDN arithmetic)
% 63.07/63.19 % Problem : 5 - 3 = only 2
% 63.07/63.19 % Version : Especial.
% 63.07/63.19 % English :
% 63.07/63.19
% 63.07/63.19 % Refs :
% 63.07/63.19 % Source : [TPTP]
% 63.07/63.19 % Names :
% 63.07/63.19
% 63.07/63.19 % Status : Theorem
% 63.07/63.19 % Rating : 0.50 v8.2.0, 0.53 v8.1.0, 0.56 v7.5.0, 0.59 v7.4.0, 0.53 v7.3.0, 0.52 v7.2.0, 0.48 v7.1.0, 0.43 v7.0.0, 0.47 v6.4.0, 0.58 v6.3.0, 0.50 v6.2.0, 0.60 v6.1.0, 0.70 v6.0.0, 0.57 v5.5.0, 0.59 v5.4.0, 0.61 v5.3.0, 0.63 v5.2.0, 0.55 v5.1.0, 0.52 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
% 63.07/63.19 % Syntax : Number of formulae : 402 ( 374 unt; 0 def)
% 63.07/63.19 % Number of atoms : 474 ( 6 equ)
% 63.07/63.19 % Maximal formula atoms : 8 ( 1 avg)
% 63.07/63.19 % Number of connectives : 74 ( 2 ~; 1 |; 43 &)
% 63.07/63.19 % ( 3 <=>; 25 =>; 0 <=; 0 <~>)
% 63.07/63.19 % Maximal formula depth : 19 ( 1 avg)
% 63.07/63.19 % Maximal term depth : 5 ( 2 avg)
% 63.07/63.19 % Number of predicates : 11 ( 10 usr; 0 prp; 1-4 aty)
% 63.07/63.19 % Number of functors : 260 ( 260 usr; 256 con; 0-2 aty)
% 63.07/63.19 % Number of variables : 122 ( 122 !; 0 ?)
% 63.07/63.19 % SPC : FOF_THM_RFO_SEQ
% 63.07/63.19
% 63.07/63.19 % Comments :
% 63.07/63.19 %------------------------------------------------------------------------------
% 63.07/63.19 %----Include axioms for RDN arithmetic
% 63.07/63.19 include('Axioms/NUM005+0.ax').
% 63.07/63.19 include('Axioms/NUM005+1.ax').
% 63.07/63.19 include('Axioms/NUM005+2.ax').
% 63.07/63.19 %------------------------------------------------------------------------------
% 63.07/63.19 fof(diff_n5_n3_only_n2,conjecture,
% 63.07/63.19 ! [X] :
% 63.07/63.19 ( difference(n5,n3,X)
% 63.07/63.19 => X = n2 ) ).
% 63.07/63.19
% 63.07/63.19 %------------------------------------------------------------------------------
% 63.07/63.19 %-------------------------------------------
% 63.07/63.19 % Proof found
% 63.07/63.19 % SZS status Theorem for theBenchmark
% 63.07/63.19 % SZS output start Proof
% 63.07/63.19 %ClaNum:440(EqnAxiom:32)
% 63.07/63.19 %VarNum:271(SingletonVarNum:132)
% 63.07/63.19 %MaxLitNum:8
% 63.07/63.19 %MaxfuncDepth:4
% 63.07/63.19 %SharedTerms:979
% 63.07/63.19 %goalClause: 70 408
% 63.07/63.19 %singleGoalClaCount:2
% 63.07/63.19 [70]P2(a66,a44,a3)
% 63.07/63.19 [408]~E(a3,a5)
% 63.07/63.19 [33]P1(f4(a1))
% 63.07/63.19 [34]P1(f4(a5))
% 63.07/63.19 [35]P1(f4(a44))
% 63.07/63.19 [36]P1(f4(a55))
% 63.07/63.19 [37]P1(f4(a66))
% 63.07/63.19 [38]P1(f4(a77))
% 63.07/63.19 [39]P1(f4(a88))
% 63.07/63.19 [40]P1(f4(a99))
% 63.07/63.19 [41]P1(f4(a110))
% 63.07/63.19 [42]P8(f4(a2),f4(a1))
% 63.07/63.19 [43]P8(f4(a1),f4(a5))
% 63.07/63.19 [44]P8(f4(a5),f4(a44))
% 63.07/63.19 [45]P8(f4(a44),f4(a55))
% 63.07/63.19 [46]P8(f4(a55),f4(a66))
% 63.07/63.19 [47]P8(f4(a66),f4(a77))
% 63.07/63.19 [48]P8(f4(a77),f4(a88))
% 63.07/63.19 [49]P8(f4(a88),f4(a99))
% 63.07/63.19 [50]P8(f4(a99),f4(a110))
% 63.07/63.19 [308]P3(f4(a2),f4(a2),f4(a2),f4(a2))
% 63.07/63.19 [309]P3(f4(a2),f4(a1),f4(a1),f4(a2))
% 63.07/63.19 [310]P3(f4(a2),f4(a5),f4(a5),f4(a2))
% 63.07/63.19 [311]P3(f4(a2),f4(a44),f4(a44),f4(a2))
% 63.07/63.19 [312]P3(f4(a2),f4(a55),f4(a55),f4(a2))
% 63.07/63.19 [313]P3(f4(a2),f4(a66),f4(a66),f4(a2))
% 63.07/63.19 [314]P3(f4(a2),f4(a77),f4(a77),f4(a2))
% 63.07/63.19 [315]P3(f4(a2),f4(a88),f4(a88),f4(a2))
% 63.07/63.19 [316]P3(f4(a2),f4(a99),f4(a99),f4(a2))
% 63.07/63.19 [317]P3(f4(a2),f4(a110),f4(a110),f4(a2))
% 63.07/63.19 [318]P3(f4(a1),f4(a2),f4(a1),f4(a2))
% 63.07/63.19 [319]P3(f4(a1),f4(a1),f4(a5),f4(a2))
% 63.07/63.19 [320]P3(f4(a1),f4(a5),f4(a44),f4(a2))
% 63.07/63.19 [321]P3(f4(a1),f4(a44),f4(a55),f4(a2))
% 63.07/63.19 [322]P3(f4(a1),f4(a55),f4(a66),f4(a2))
% 63.07/63.19 [323]P3(f4(a1),f4(a66),f4(a77),f4(a2))
% 63.07/63.20 [324]P3(f4(a1),f4(a77),f4(a88),f4(a2))
% 63.07/63.20 [325]P3(f4(a1),f4(a88),f4(a99),f4(a2))
% 63.07/63.20 [326]P3(f4(a1),f4(a99),f4(a110),f4(a2))
% 63.07/63.20 [327]P3(f4(a1),f4(a110),f4(a2),f4(a1))
% 63.07/63.20 [328]P3(f4(a5),f4(a2),f4(a5),f4(a2))
% 63.07/63.20 [329]P3(f4(a5),f4(a1),f4(a44),f4(a2))
% 63.07/63.20 [330]P3(f4(a5),f4(a5),f4(a55),f4(a2))
% 63.07/63.20 [331]P3(f4(a5),f4(a44),f4(a66),f4(a2))
% 63.07/63.20 [332]P3(f4(a5),f4(a55),f4(a77),f4(a2))
% 63.07/63.20 [333]P3(f4(a5),f4(a66),f4(a88),f4(a2))
% 63.07/63.20 [334]P3(f4(a5),f4(a77),f4(a99),f4(a2))
% 63.07/63.20 [335]P3(f4(a5),f4(a88),f4(a110),f4(a2))
% 63.07/63.20 [336]P3(f4(a5),f4(a99),f4(a2),f4(a1))
% 63.07/63.20 [337]P3(f4(a5),f4(a110),f4(a1),f4(a1))
% 63.07/63.20 [338]P3(f4(a44),f4(a2),f4(a44),f4(a2))
% 63.07/63.20 [339]P3(f4(a44),f4(a1),f4(a55),f4(a2))
% 63.07/63.20 [340]P3(f4(a44),f4(a5),f4(a66),f4(a2))
% 63.07/63.20 [341]P3(f4(a44),f4(a44),f4(a77),f4(a2))
% 63.07/63.20 [342]P3(f4(a44),f4(a55),f4(a88),f4(a2))
% 63.07/63.20 [343]P3(f4(a44),f4(a66),f4(a99),f4(a2))
% 63.07/63.20 [344]P3(f4(a44),f4(a77),f4(a110),f4(a2))
% 63.07/63.20 [345]P3(f4(a44),f4(a88),f4(a2),f4(a1))
% 63.07/63.20 [346]P3(f4(a44),f4(a99),f4(a1),f4(a1))
% 63.07/63.20 [347]P3(f4(a44),f4(a110),f4(a5),f4(a1))
% 63.07/63.20 [348]P3(f4(a55),f4(a2),f4(a55),f4(a2))
% 63.07/63.20 [349]P3(f4(a55),f4(a1),f4(a66),f4(a2))
% 63.07/63.20 [350]P3(f4(a55),f4(a5),f4(a77),f4(a2))
% 63.07/63.20 [351]P3(f4(a55),f4(a44),f4(a88),f4(a2))
% 63.07/63.20 [352]P3(f4(a55),f4(a55),f4(a99),f4(a2))
% 63.07/63.20 [353]P3(f4(a55),f4(a66),f4(a110),f4(a2))
% 63.07/63.20 [354]P3(f4(a55),f4(a77),f4(a2),f4(a1))
% 63.07/63.20 [355]P3(f4(a55),f4(a88),f4(a1),f4(a1))
% 63.07/63.20 [356]P3(f4(a55),f4(a99),f4(a5),f4(a1))
% 63.07/63.20 [357]P3(f4(a55),f4(a110),f4(a44),f4(a1))
% 63.07/63.20 [358]P3(f4(a66),f4(a2),f4(a66),f4(a2))
% 63.07/63.20 [359]P3(f4(a66),f4(a1),f4(a77),f4(a2))
% 63.07/63.20 [360]P3(f4(a66),f4(a5),f4(a88),f4(a2))
% 63.07/63.20 [361]P3(f4(a66),f4(a44),f4(a99),f4(a2))
% 63.07/63.20 [362]P3(f4(a66),f4(a55),f4(a110),f4(a2))
% 63.07/63.20 [363]P3(f4(a66),f4(a66),f4(a2),f4(a1))
% 63.07/63.20 [364]P3(f4(a66),f4(a77),f4(a1),f4(a1))
% 63.07/63.20 [365]P3(f4(a66),f4(a88),f4(a5),f4(a1))
% 63.07/63.20 [366]P3(f4(a66),f4(a99),f4(a44),f4(a1))
% 63.07/63.20 [367]P3(f4(a66),f4(a110),f4(a55),f4(a1))
% 63.07/63.20 [368]P3(f4(a77),f4(a2),f4(a77),f4(a2))
% 63.07/63.20 [369]P3(f4(a77),f4(a1),f4(a88),f4(a2))
% 63.07/63.20 [370]P3(f4(a77),f4(a5),f4(a99),f4(a2))
% 63.07/63.20 [371]P3(f4(a77),f4(a44),f4(a110),f4(a2))
% 63.07/63.20 [372]P3(f4(a77),f4(a55),f4(a2),f4(a1))
% 63.07/63.20 [373]P3(f4(a77),f4(a66),f4(a1),f4(a1))
% 63.07/63.20 [374]P3(f4(a77),f4(a77),f4(a5),f4(a1))
% 63.07/63.20 [375]P3(f4(a77),f4(a88),f4(a44),f4(a1))
% 63.07/63.20 [376]P3(f4(a77),f4(a99),f4(a55),f4(a1))
% 63.07/63.20 [377]P3(f4(a77),f4(a110),f4(a66),f4(a1))
% 63.07/63.20 [378]P3(f4(a88),f4(a2),f4(a88),f4(a2))
% 63.07/63.20 [379]P3(f4(a88),f4(a1),f4(a99),f4(a2))
% 63.07/63.20 [380]P3(f4(a88),f4(a5),f4(a110),f4(a2))
% 63.07/63.20 [381]P3(f4(a88),f4(a44),f4(a2),f4(a1))
% 63.07/63.20 [382]P3(f4(a88),f4(a55),f4(a1),f4(a1))
% 63.07/63.20 [383]P3(f4(a88),f4(a66),f4(a5),f4(a1))
% 63.07/63.20 [384]P3(f4(a88),f4(a77),f4(a44),f4(a1))
% 63.07/63.20 [385]P3(f4(a88),f4(a88),f4(a55),f4(a1))
% 63.07/63.20 [386]P3(f4(a88),f4(a99),f4(a66),f4(a1))
% 63.07/63.20 [387]P3(f4(a88),f4(a110),f4(a77),f4(a1))
% 63.07/63.20 [388]P3(f4(a99),f4(a2),f4(a99),f4(a2))
% 63.07/63.20 [389]P3(f4(a99),f4(a1),f4(a110),f4(a2))
% 63.07/63.20 [390]P3(f4(a99),f4(a5),f4(a2),f4(a1))
% 63.07/63.20 [391]P3(f4(a99),f4(a44),f4(a1),f4(a1))
% 63.07/63.20 [392]P3(f4(a99),f4(a55),f4(a5),f4(a1))
% 63.07/63.20 [393]P3(f4(a99),f4(a66),f4(a44),f4(a1))
% 63.07/63.20 [394]P3(f4(a99),f4(a77),f4(a55),f4(a1))
% 63.07/63.20 [395]P3(f4(a99),f4(a88),f4(a66),f4(a1))
% 63.07/63.20 [396]P3(f4(a99),f4(a99),f4(a77),f4(a1))
% 63.07/63.20 [397]P3(f4(a99),f4(a110),f4(a88),f4(a1))
% 63.07/63.20 [398]P3(f4(a110),f4(a2),f4(a110),f4(a2))
% 63.07/63.20 [399]P3(f4(a110),f4(a1),f4(a2),f4(a1))
% 63.07/63.20 [400]P3(f4(a110),f4(a5),f4(a1),f4(a1))
% 63.07/63.20 [401]P3(f4(a110),f4(a44),f4(a5),f4(a1))
% 63.07/63.20 [402]P3(f4(a110),f4(a55),f4(a44),f4(a1))
% 63.07/63.20 [403]P3(f4(a110),f4(a66),f4(a55),f4(a1))
% 63.07/63.20 [404]P3(f4(a110),f4(a77),f4(a66),f4(a1))
% 63.07/63.20 [405]P3(f4(a110),f4(a88),f4(a77),f4(a1))
% 63.07/63.20 [406]P3(f4(a110),f4(a99),f4(a88),f4(a1))
% 63.07/63.20 [407]P3(f4(a110),f4(a110),f4(a99),f4(a1))
% 63.07/63.20 [51]P9(a2,f121(f4(a2)))
% 63.07/63.20 [52]P9(a1,f121(f4(a1)))
% 63.07/63.20 [53]P9(a5,f121(f4(a5)))
% 63.07/63.20 [54]P9(a44,f121(f4(a44)))
% 63.07/63.20 [55]P9(a55,f121(f4(a55)))
% 63.07/63.20 [56]P9(a66,f121(f4(a66)))
% 63.07/63.20 [57]P9(a77,f121(f4(a77)))
% 63.07/63.20 [58]P9(a88,f121(f4(a88)))
% 63.07/63.20 [59]P9(a99,f121(f4(a99)))
% 63.07/63.20 [60]P9(a110,f121(f4(a110)))
% 63.07/63.20 [61]P9(a122,f133(f4(a1)))
% 63.07/63.20 [62]P9(a134,f133(f4(a5)))
% 63.07/63.20 [63]P9(a174,f133(f4(a44)))
% 63.07/63.20 [64]P9(a185,f133(f4(a55)))
% 63.07/63.20 [65]P9(a196,f133(f4(a66)))
% 63.07/63.20 [66]P9(a207,f133(f4(a77)))
% 63.07/63.20 [67]P9(a218,f133(f4(a88)))
% 63.07/63.20 [68]P9(a229,f133(f4(a99)))
% 63.07/63.20 [69]P9(a240,f133(f4(a110)))
% 63.07/63.20 [71]P9(a6,f121(f251(f4(a2),f4(a1))))
% 63.07/63.20 [72]P9(a7,f121(f251(f4(a1),f4(a1))))
% 63.07/63.20 [73]P9(a18,f121(f251(f4(a5),f4(a1))))
% 63.07/63.20 [74]P9(a29,f121(f251(f4(a44),f4(a1))))
% 63.07/63.20 [75]P9(a38,f121(f251(f4(a55),f4(a1))))
% 63.07/63.20 [76]P9(a39,f121(f251(f4(a66),f4(a1))))
% 63.07/63.20 [77]P9(a40,f121(f251(f4(a77),f4(a1))))
% 63.07/63.20 [78]P9(a41,f121(f251(f4(a88),f4(a1))))
% 63.07/63.20 [79]P9(a42,f121(f251(f4(a99),f4(a1))))
% 63.07/63.20 [80]P9(a43,f121(f251(f4(a110),f4(a1))))
% 63.07/63.20 [81]P9(a45,f121(f251(f4(a2),f4(a5))))
% 63.07/63.20 [82]P9(a46,f121(f251(f4(a1),f4(a5))))
% 63.07/63.20 [83]P9(a47,f121(f251(f4(a5),f4(a5))))
% 63.07/63.20 [84]P9(a48,f121(f251(f4(a44),f4(a5))))
% 63.07/63.20 [85]P9(a49,f121(f251(f4(a55),f4(a5))))
% 63.07/63.20 [86]P9(a50,f121(f251(f4(a66),f4(a5))))
% 63.07/63.20 [87]P9(a51,f121(f251(f4(a77),f4(a5))))
% 63.07/63.20 [88]P9(a52,f121(f251(f4(a88),f4(a5))))
% 63.07/63.20 [89]P9(a53,f121(f251(f4(a99),f4(a5))))
% 63.07/63.20 [90]P9(a54,f121(f251(f4(a110),f4(a5))))
% 63.07/63.20 [91]P9(a56,f121(f251(f4(a2),f4(a44))))
% 63.07/63.20 [92]P9(a57,f121(f251(f4(a1),f4(a44))))
% 63.07/63.20 [93]P9(a58,f121(f251(f4(a5),f4(a44))))
% 63.07/63.20 [94]P9(a59,f121(f251(f4(a44),f4(a44))))
% 63.07/63.20 [95]P9(a60,f121(f251(f4(a55),f4(a44))))
% 63.07/63.20 [96]P9(a61,f121(f251(f4(a66),f4(a44))))
% 63.07/63.20 [97]P9(a62,f121(f251(f4(a77),f4(a44))))
% 63.07/63.20 [98]P9(a63,f121(f251(f4(a88),f4(a44))))
% 63.07/63.20 [99]P9(a64,f121(f251(f4(a99),f4(a44))))
% 63.07/63.20 [100]P9(a65,f121(f251(f4(a110),f4(a44))))
% 63.07/63.20 [101]P9(a67,f121(f251(f4(a2),f4(a55))))
% 63.07/63.20 [102]P9(a68,f121(f251(f4(a1),f4(a55))))
% 63.07/63.20 [103]P9(a69,f121(f251(f4(a5),f4(a55))))
% 63.07/63.20 [104]P9(a70,f121(f251(f4(a44),f4(a55))))
% 63.07/63.20 [105]P9(a71,f121(f251(f4(a55),f4(a55))))
% 63.07/63.20 [106]P9(a72,f121(f251(f4(a66),f4(a55))))
% 63.07/63.20 [107]P9(a73,f121(f251(f4(a77),f4(a55))))
% 63.07/63.20 [108]P9(a74,f121(f251(f4(a88),f4(a55))))
% 63.07/63.20 [109]P9(a75,f121(f251(f4(a99),f4(a55))))
% 63.07/63.20 [110]P9(a76,f121(f251(f4(a110),f4(a55))))
% 63.07/63.20 [111]P9(a78,f121(f251(f4(a2),f4(a66))))
% 63.07/63.20 [112]P9(a79,f121(f251(f4(a1),f4(a66))))
% 63.07/63.20 [113]P9(a80,f121(f251(f4(a5),f4(a66))))
% 63.07/63.20 [114]P9(a81,f121(f251(f4(a44),f4(a66))))
% 63.07/63.20 [115]P9(a82,f121(f251(f4(a55),f4(a66))))
% 63.07/63.20 [116]P9(a83,f121(f251(f4(a66),f4(a66))))
% 63.07/63.20 [117]P9(a84,f121(f251(f4(a77),f4(a66))))
% 63.07/63.20 [118]P9(a85,f121(f251(f4(a88),f4(a66))))
% 63.07/63.20 [119]P9(a86,f121(f251(f4(a99),f4(a66))))
% 63.07/63.20 [120]P9(a87,f121(f251(f4(a110),f4(a66))))
% 63.07/63.20 [121]P9(a89,f121(f251(f4(a2),f4(a77))))
% 63.07/63.20 [122]P9(a90,f121(f251(f4(a1),f4(a77))))
% 63.07/63.20 [123]P9(a91,f121(f251(f4(a5),f4(a77))))
% 63.07/63.20 [124]P9(a92,f121(f251(f4(a44),f4(a77))))
% 63.07/63.20 [125]P9(a93,f121(f251(f4(a55),f4(a77))))
% 63.07/63.20 [126]P9(a94,f121(f251(f4(a66),f4(a77))))
% 63.07/63.20 [127]P9(a95,f121(f251(f4(a77),f4(a77))))
% 63.07/63.20 [128]P9(a96,f121(f251(f4(a88),f4(a77))))
% 63.07/63.20 [129]P9(a97,f121(f251(f4(a99),f4(a77))))
% 63.07/63.20 [130]P9(a98,f121(f251(f4(a110),f4(a77))))
% 63.07/63.20 [131]P9(a100,f121(f251(f4(a2),f4(a88))))
% 63.07/63.20 [132]P9(a101,f121(f251(f4(a1),f4(a88))))
% 63.07/63.20 [133]P9(a102,f121(f251(f4(a5),f4(a88))))
% 63.07/63.20 [134]P9(a103,f121(f251(f4(a44),f4(a88))))
% 63.07/63.20 [135]P9(a104,f121(f251(f4(a55),f4(a88))))
% 63.07/63.20 [136]P9(a105,f121(f251(f4(a66),f4(a88))))
% 63.07/63.20 [137]P9(a106,f121(f251(f4(a77),f4(a88))))
% 63.07/63.20 [138]P9(a107,f121(f251(f4(a88),f4(a88))))
% 63.07/63.20 [139]P9(a108,f121(f251(f4(a99),f4(a88))))
% 63.07/63.20 [140]P9(a109,f121(f251(f4(a110),f4(a88))))
% 63.07/63.20 [141]P9(a111,f121(f251(f4(a2),f4(a99))))
% 63.07/63.20 [142]P9(a112,f121(f251(f4(a1),f4(a99))))
% 63.07/63.20 [143]P9(a113,f121(f251(f4(a5),f4(a99))))
% 63.07/63.20 [144]P9(a114,f121(f251(f4(a44),f4(a99))))
% 63.07/63.20 [145]P9(a115,f121(f251(f4(a55),f4(a99))))
% 63.07/63.20 [146]P9(a116,f121(f251(f4(a66),f4(a99))))
% 63.07/63.20 [147]P9(a117,f121(f251(f4(a77),f4(a99))))
% 63.07/63.20 [148]P9(a118,f121(f251(f4(a88),f4(a99))))
% 63.07/63.20 [149]P9(a119,f121(f251(f4(a99),f4(a99))))
% 63.07/63.21 [150]P9(a120,f121(f251(f4(a110),f4(a99))))
% 63.07/63.21 [151]P9(a123,f121(f251(f4(a2),f4(a110))))
% 63.07/63.21 [152]P9(a124,f121(f251(f4(a1),f4(a110))))
% 63.07/63.21 [153]P9(a125,f121(f251(f4(a5),f4(a110))))
% 63.07/63.21 [154]P9(a126,f121(f251(f4(a44),f4(a110))))
% 63.07/63.21 [155]P9(a127,f121(f251(f4(a55),f4(a110))))
% 63.07/63.21 [156]P9(a128,f121(f251(f4(a66),f4(a110))))
% 63.07/63.21 [157]P9(a129,f121(f251(f4(a77),f4(a110))))
% 63.07/63.21 [158]P9(a130,f121(f251(f4(a88),f4(a110))))
% 63.07/63.21 [159]P9(a131,f121(f251(f4(a99),f4(a110))))
% 63.07/63.21 [160]P9(a132,f121(f251(f4(a110),f4(a110))))
% 63.07/63.21 [161]P9(a135,f133(f251(f4(a2),f4(a1))))
% 63.07/63.21 [162]P9(a136,f133(f251(f4(a1),f4(a1))))
% 63.07/63.21 [163]P9(a147,f133(f251(f4(a5),f4(a1))))
% 63.07/63.21 [164]P9(a158,f133(f251(f4(a44),f4(a1))))
% 63.07/63.21 [165]P9(a168,f133(f251(f4(a55),f4(a1))))
% 63.07/63.21 [166]P9(a169,f133(f251(f4(a66),f4(a1))))
% 63.07/63.21 [167]P9(a170,f133(f251(f4(a77),f4(a1))))
% 63.07/63.21 [168]P9(a171,f133(f251(f4(a88),f4(a1))))
% 63.07/63.21 [169]P9(a172,f133(f251(f4(a99),f4(a1))))
% 63.07/63.21 [170]P9(a173,f133(f251(f4(a110),f4(a1))))
% 63.07/63.21 [171]P9(a175,f133(f251(f4(a2),f4(a5))))
% 63.07/63.21 [172]P9(a176,f133(f251(f4(a1),f4(a5))))
% 63.07/63.21 [173]P9(a177,f133(f251(f4(a5),f4(a5))))
% 63.07/63.21 [174]P9(a178,f133(f251(f4(a44),f4(a5))))
% 63.07/63.21 [175]P9(a179,f133(f251(f4(a55),f4(a5))))
% 63.07/63.21 [176]P9(a180,f133(f251(f4(a66),f4(a5))))
% 63.07/63.21 [177]P9(a181,f133(f251(f4(a77),f4(a5))))
% 63.07/63.21 [178]P9(a182,f133(f251(f4(a88),f4(a5))))
% 63.07/63.21 [179]P9(a183,f133(f251(f4(a99),f4(a5))))
% 63.07/63.21 [180]P9(a184,f133(f251(f4(a110),f4(a5))))
% 63.07/63.21 [181]P9(a186,f133(f251(f4(a2),f4(a44))))
% 63.07/63.21 [182]P9(a187,f133(f251(f4(a1),f4(a44))))
% 63.07/63.21 [183]P9(a188,f133(f251(f4(a5),f4(a44))))
% 63.07/63.21 [184]P9(a189,f133(f251(f4(a44),f4(a44))))
% 63.07/63.21 [185]P9(a190,f133(f251(f4(a55),f4(a44))))
% 63.07/63.21 [186]P9(a191,f133(f251(f4(a66),f4(a44))))
% 63.07/63.21 [187]P9(a192,f133(f251(f4(a77),f4(a44))))
% 63.07/63.21 [188]P9(a193,f133(f251(f4(a88),f4(a44))))
% 63.07/63.21 [189]P9(a194,f133(f251(f4(a99),f4(a44))))
% 63.07/63.21 [190]P9(a195,f133(f251(f4(a110),f4(a44))))
% 63.07/63.21 [191]P9(a197,f133(f251(f4(a2),f4(a55))))
% 63.07/63.21 [192]P9(a198,f133(f251(f4(a1),f4(a55))))
% 63.07/63.21 [193]P9(a199,f133(f251(f4(a5),f4(a55))))
% 63.07/63.21 [194]P9(a200,f133(f251(f4(a44),f4(a55))))
% 63.07/63.21 [195]P9(a201,f133(f251(f4(a55),f4(a55))))
% 63.07/63.21 [196]P9(a202,f133(f251(f4(a66),f4(a55))))
% 63.07/63.21 [197]P9(a203,f133(f251(f4(a77),f4(a55))))
% 63.07/63.21 [198]P9(a204,f133(f251(f4(a88),f4(a55))))
% 63.07/63.21 [199]P9(a205,f133(f251(f4(a99),f4(a55))))
% 63.07/63.21 [200]P9(a206,f133(f251(f4(a110),f4(a55))))
% 63.07/63.21 [201]P9(a208,f133(f251(f4(a2),f4(a66))))
% 63.07/63.21 [202]P9(a209,f133(f251(f4(a1),f4(a66))))
% 63.07/63.21 [203]P9(a210,f133(f251(f4(a5),f4(a66))))
% 63.07/63.21 [204]P9(a211,f133(f251(f4(a44),f4(a66))))
% 63.07/63.21 [205]P9(a212,f133(f251(f4(a55),f4(a66))))
% 63.07/63.21 [206]P9(a213,f133(f251(f4(a66),f4(a66))))
% 63.07/63.21 [207]P9(a214,f133(f251(f4(a77),f4(a66))))
% 63.07/63.21 [208]P9(a215,f133(f251(f4(a88),f4(a66))))
% 63.07/63.21 [209]P9(a216,f133(f251(f4(a99),f4(a66))))
% 63.07/63.21 [210]P9(a217,f133(f251(f4(a110),f4(a66))))
% 63.07/63.21 [211]P9(a219,f133(f251(f4(a2),f4(a77))))
% 63.07/63.21 [212]P9(a220,f133(f251(f4(a1),f4(a77))))
% 63.07/63.21 [213]P9(a221,f133(f251(f4(a5),f4(a77))))
% 63.07/63.21 [214]P9(a222,f133(f251(f4(a44),f4(a77))))
% 63.07/63.21 [215]P9(a223,f133(f251(f4(a55),f4(a77))))
% 63.07/63.21 [216]P9(a224,f133(f251(f4(a66),f4(a77))))
% 63.07/63.21 [217]P9(a225,f133(f251(f4(a77),f4(a77))))
% 63.07/63.21 [218]P9(a226,f133(f251(f4(a88),f4(a77))))
% 63.07/63.21 [219]P9(a227,f133(f251(f4(a99),f4(a77))))
% 63.07/63.21 [220]P9(a228,f133(f251(f4(a110),f4(a77))))
% 63.07/63.21 [221]P9(a230,f133(f251(f4(a2),f4(a88))))
% 63.07/63.21 [222]P9(a231,f133(f251(f4(a1),f4(a88))))
% 63.07/63.21 [223]P9(a232,f133(f251(f4(a5),f4(a88))))
% 63.07/63.21 [224]P9(a233,f133(f251(f4(a44),f4(a88))))
% 63.07/63.21 [225]P9(a234,f133(f251(f4(a55),f4(a88))))
% 63.07/63.21 [226]P9(a235,f133(f251(f4(a66),f4(a88))))
% 63.07/63.21 [227]P9(a236,f133(f251(f4(a77),f4(a88))))
% 63.07/63.21 [228]P9(a237,f133(f251(f4(a88),f4(a88))))
% 63.07/63.21 [229]P9(a238,f133(f251(f4(a99),f4(a88))))
% 63.07/63.21 [230]P9(a239,f133(f251(f4(a110),f4(a88))))
% 63.07/63.21 [231]P9(a241,f133(f251(f4(a2),f4(a99))))
% 63.07/63.21 [232]P9(a242,f133(f251(f4(a1),f4(a99))))
% 63.07/63.21 [233]P9(a243,f133(f251(f4(a5),f4(a99))))
% 63.07/63.21 [234]P9(a244,f133(f251(f4(a44),f4(a99))))
% 63.07/63.21 [235]P9(a245,f133(f251(f4(a55),f4(a99))))
% 63.07/63.21 [236]P9(a246,f133(f251(f4(a66),f4(a99))))
% 63.07/63.21 [237]P9(a247,f133(f251(f4(a77),f4(a99))))
% 63.07/63.21 [238]P9(a248,f133(f251(f4(a88),f4(a99))))
% 63.07/63.21 [239]P9(a249,f133(f251(f4(a99),f4(a99))))
% 63.07/63.21 [240]P9(a250,f133(f251(f4(a110),f4(a99))))
% 63.07/63.21 [241]P9(a252,f133(f251(f4(a2),f4(a110))))
% 63.07/63.21 [242]P9(a253,f133(f251(f4(a1),f4(a110))))
% 63.07/63.21 [243]P9(a254,f133(f251(f4(a5),f4(a110))))
% 63.07/63.21 [244]P9(a255,f133(f251(f4(a44),f4(a110))))
% 63.07/63.21 [245]P9(a256,f133(f251(f4(a55),f4(a110))))
% 63.07/63.21 [246]P9(a257,f133(f251(f4(a66),f4(a110))))
% 63.07/63.21 [247]P9(a258,f133(f251(f4(a77),f4(a110))))
% 63.07/63.21 [248]P9(a259,f133(f251(f4(a88),f4(a110))))
% 63.07/63.21 [249]P9(a260,f133(f251(f4(a99),f4(a110))))
% 63.07/63.21 [250]P9(a261,f133(f251(f4(a110),f4(a110))))
% 63.07/63.21 [251]P9(a8,f121(f251(f4(a2),f251(f4(a2),f4(a1)))))
% 63.07/63.21 [252]P9(a9,f121(f251(f4(a1),f251(f4(a2),f4(a1)))))
% 63.07/63.21 [253]P9(a10,f121(f251(f4(a5),f251(f4(a2),f4(a1)))))
% 63.07/63.21 [254]P9(a11,f121(f251(f4(a44),f251(f4(a2),f4(a1)))))
% 63.07/63.21 [255]P9(a12,f121(f251(f4(a55),f251(f4(a2),f4(a1)))))
% 63.07/63.21 [256]P9(a13,f121(f251(f4(a66),f251(f4(a2),f4(a1)))))
% 63.07/63.21 [257]P9(a14,f121(f251(f4(a77),f251(f4(a2),f4(a1)))))
% 63.07/63.21 [258]P9(a15,f121(f251(f4(a88),f251(f4(a2),f4(a1)))))
% 63.07/63.21 [259]P9(a16,f121(f251(f4(a99),f251(f4(a2),f4(a1)))))
% 63.07/63.21 [260]P9(a17,f121(f251(f4(a110),f251(f4(a2),f4(a1)))))
% 63.07/63.21 [261]P9(a19,f121(f251(f4(a2),f251(f4(a1),f4(a1)))))
% 63.07/63.21 [262]P9(a20,f121(f251(f4(a1),f251(f4(a1),f4(a1)))))
% 63.07/63.21 [263]P9(a21,f121(f251(f4(a5),f251(f4(a1),f4(a1)))))
% 63.07/63.21 [264]P9(a22,f121(f251(f4(a44),f251(f4(a1),f4(a1)))))
% 63.07/63.21 [265]P9(a23,f121(f251(f4(a55),f251(f4(a1),f4(a1)))))
% 63.07/63.21 [266]P9(a24,f121(f251(f4(a66),f251(f4(a1),f4(a1)))))
% 63.07/63.21 [267]P9(a25,f121(f251(f4(a77),f251(f4(a1),f4(a1)))))
% 63.07/63.21 [268]P9(a26,f121(f251(f4(a88),f251(f4(a1),f4(a1)))))
% 63.07/63.21 [269]P9(a27,f121(f251(f4(a99),f251(f4(a1),f4(a1)))))
% 63.07/63.21 [270]P9(a28,f121(f251(f4(a110),f251(f4(a1),f4(a1)))))
% 63.07/63.21 [271]P9(a30,f121(f251(f4(a2),f251(f4(a5),f4(a1)))))
% 63.07/63.21 [272]P9(a31,f121(f251(f4(a1),f251(f4(a5),f4(a1)))))
% 63.07/63.21 [273]P9(a32,f121(f251(f4(a5),f251(f4(a5),f4(a1)))))
% 63.07/63.21 [274]P9(a33,f121(f251(f4(a44),f251(f4(a5),f4(a1)))))
% 63.07/63.21 [275]P9(a34,f121(f251(f4(a55),f251(f4(a5),f4(a1)))))
% 63.07/63.21 [276]P9(a35,f121(f251(f4(a66),f251(f4(a5),f4(a1)))))
% 63.07/63.21 [277]P9(a36,f121(f251(f4(a77),f251(f4(a5),f4(a1)))))
% 63.07/63.21 [278]P9(a37,f121(f251(f4(a88),f251(f4(a5),f4(a1)))))
% 63.07/63.21 [279]P9(a137,f133(f251(f4(a2),f251(f4(a2),f4(a1)))))
% 63.07/63.21 [280]P9(a138,f133(f251(f4(a1),f251(f4(a2),f4(a1)))))
% 63.07/63.21 [281]P9(a139,f133(f251(f4(a5),f251(f4(a2),f4(a1)))))
% 63.07/63.21 [282]P9(a140,f133(f251(f4(a44),f251(f4(a2),f4(a1)))))
% 63.07/63.21 [283]P9(a141,f133(f251(f4(a55),f251(f4(a2),f4(a1)))))
% 63.07/63.21 [284]P9(a142,f133(f251(f4(a66),f251(f4(a2),f4(a1)))))
% 63.07/63.21 [285]P9(a143,f133(f251(f4(a77),f251(f4(a2),f4(a1)))))
% 63.07/63.21 [286]P9(a144,f133(f251(f4(a88),f251(f4(a2),f4(a1)))))
% 63.07/63.21 [287]P9(a145,f133(f251(f4(a99),f251(f4(a2),f4(a1)))))
% 63.07/63.21 [288]P9(a146,f133(f251(f4(a110),f251(f4(a2),f4(a1)))))
% 63.07/63.21 [289]P9(a148,f133(f251(f4(a2),f251(f4(a1),f4(a1)))))
% 63.07/63.21 [290]P9(a149,f133(f251(f4(a1),f251(f4(a1),f4(a1)))))
% 63.07/63.21 [291]P9(a150,f133(f251(f4(a5),f251(f4(a1),f4(a1)))))
% 63.07/63.21 [292]P9(a151,f133(f251(f4(a44),f251(f4(a1),f4(a1)))))
% 63.07/63.21 [293]P9(a152,f133(f251(f4(a55),f251(f4(a1),f4(a1)))))
% 63.07/63.21 [294]P9(a153,f133(f251(f4(a66),f251(f4(a1),f4(a1)))))
% 63.07/63.21 [295]P9(a154,f133(f251(f4(a77),f251(f4(a1),f4(a1)))))
% 63.07/63.21 [296]P9(a155,f133(f251(f4(a88),f251(f4(a1),f4(a1)))))
% 63.07/63.21 [297]P9(a156,f133(f251(f4(a99),f251(f4(a1),f4(a1)))))
% 63.07/63.21 [298]P9(a157,f133(f251(f4(a110),f251(f4(a1),f4(a1)))))
% 63.07/63.21 [299]P9(a159,f133(f251(f4(a2),f251(f4(a5),f4(a1)))))
% 63.07/63.21 [300]P9(a160,f133(f251(f4(a1),f251(f4(a5),f4(a1)))))
% 63.07/63.21 [301]P9(a161,f133(f251(f4(a5),f251(f4(a5),f4(a1)))))
% 63.07/63.21 [302]P9(a162,f133(f251(f4(a44),f251(f4(a5),f4(a1)))))
% 63.07/63.21 [303]P9(a163,f133(f251(f4(a55),f251(f4(a5),f4(a1)))))
% 63.07/63.21 [304]P9(a164,f133(f251(f4(a66),f251(f4(a5),f4(a1)))))
% 63.07/63.21 [305]P9(a165,f133(f251(f4(a77),f251(f4(a5),f4(a1)))))
% 63.07/63.21 [306]P9(a166,f133(f251(f4(a88),f251(f4(a5),f4(a1)))))
% 63.07/63.21 [307]P9(a167,f133(f251(f4(a99),f251(f4(a5),f4(a1)))))
% 63.07/63.21 [411]P7(f4(x4111))+~P1(f4(x4111))
% 63.07/63.21 [409]~E(x4091,x4092)+P4(x4091,x4092)
% 63.07/63.21 [410]~P5(x4102,x4101)+~E(x4101,x4102)
% 63.07/63.21 [413]~P5(x4131,x4132)+P4(x4131,x4132)
% 63.07/63.21 [415]~P5(x4152,x4151)+~P5(x4151,x4152)
% 63.07/63.21 [416]~P7(x4162)+P7(f251(f4(x4161),x4162))
% 63.07/63.21 [426]~P2(x4263,x4261,x4262)+P10(x4261,x4262,x4263)
% 63.07/63.21 [427]~P10(x4272,x4273,x4271)+P2(x4271,x4272,x4273)
% 63.07/63.21 [417]~P7(x4173)+P8(f4(x4171),f251(f4(x4172),x4173))
% 63.07/63.21 [422]~P8(x4222,x4224)+P8(f251(f4(x4221),x4222),f251(f4(x4223),x4224))
% 63.07/63.21 [436]P6(f4(x4361),f251(f4(x4362),x4363),f4(x4364),f251(f4(x4365),x4366))+~P6(f4(x4361),f4(x4364),f251(f4(x4362),x4363),f251(f4(x4365),x4366))
% 63.07/63.21 [412]P5(x4122,x4121)+P5(x4121,x4122)+E(x4121,x4122)
% 63.07/63.21 [414]P5(x4141,x4142)+~P4(x4141,x4142)+E(x4141,x4142)
% 63.07/63.21 [424]P4(x4241,x4242)+~P5(x4241,x4243)+~P10(x4242,a1,x4243)
% 63.07/63.21 [421]P8(f4(x4211),f4(x4212))+~P8(f4(x4213),f4(x4212))+~P8(f4(x4211),f4(x4213))
% 63.07/63.21 [423]P10(x4231,x4232,a2)+~P9(x4231,f121(x4233))+~P9(x4232,f133(x4233))
% 63.07/63.21 [425]~P7(x4252)+~P8(f4(x4251),f4(x4253))+P8(f251(f4(x4251),x4252),f251(f4(x4253),x4252))
% 63.07/63.21 [428]~P10(x4283,x4284,x4281)+E(x4281,x4282)+~P10(x4283,x4284,x4282)
% 63.07/63.21 [429]~P10(x4293,x4291,x4294)+E(x4291,x4292)+~P10(x4293,x4292,x4294)
% 63.07/63.21 [430]~P10(x4301,x4303,x4304)+E(x4301,x4302)+~P10(x4302,x4303,x4304)
% 63.07/63.21 [418]P5(x4181,x4182)+~P9(x4182,f121(x4183))+~P9(x4181,f133(x4184))
% 63.07/63.21 [437]P6(f4(x4371),f4(x4372),f4(x4373),f4(x4374))+~P3(f4(x4375),f4(x4371),f4(x4374),f4(a2))+~P3(f4(x4372),f4(x4373),f4(x4375),f4(a2))
% 63.07/63.21 [419]P5(x4191,x4192)+~P8(x4193,x4194)+~P9(x4192,f133(x4193))+~P9(x4191,f133(x4194))
% 63.07/63.21 [420]P5(x4201,x4202)+~P8(x4203,x4204)+~P9(x4202,f121(x4204))+~P9(x4201,f121(x4203))
% 63.07/63.21 [431]~P10(x4312,x4311,x4313)+P10(x4311,x4312,x4313)+~P9(x4312,f121(x4314))+~P9(x4311,f133(x4315))
% 63.07/63.21 [438]~P3(f4(x4385),f4(x4381),f4(x4384),f4(x4386))+~P3(f4(x4382),f4(x4383),f4(x4385),f4(x4387))+~P3(f4(x4387),f4(x4386),f4(a1),f4(a2))+P6(f4(x4381),f4(x4382),f4(x4383),f251(f4(x4384),f4(a1)))
% 63.07/63.21 [432]P10(x4321,x4322,x4323)+~P6(f4(a2),x4326,x4325,x4324)+~P9(x4323,f121(x4324))+~P9(x4322,f121(x4325))+~P9(x4321,f121(x4326))
% 63.07/63.21 [433]P10(x4331,x4332,x4333)+~P6(f4(a2),x4336,x4335,x4334)+~P9(x4333,f133(x4334))+~P9(x4332,f133(x4335))+~P9(x4331,f133(x4336))
% 63.07/63.21 [434]P10(x4341,x4342,x4343)+~P8(x4344,x4345)+~P6(f4(a2),x4344,x4346,x4345)+~P9(x4342,f133(x4344))+~P9(x4341,f121(x4345))+~P9(x4343,f121(x4346))
% 63.07/63.21 [435]P10(x4351,x4352,x4353)+~P8(x4354,x4355)+~P6(f4(a2),x4354,x4356,x4355)+~P9(x4352,f133(x4355))+~P9(x4351,f121(x4354))+~P9(x4353,f133(x4356))
% 63.07/63.21 [439]~P7(x4396)+~P7(x4394)+~P3(f4(x4398),f4(x4391),f4(x4395),f4(x4399))+~P3(f4(x4392),f4(x4393),f4(x4398),f4(x43910))+~P6(f4(x4397),f4(a2),x4394,x4396)+~P3(f4(x43910),f4(x4399),f4(x4397),f4(a2))+P6(f4(x4391),f4(x4392),f251(f4(x4393),x4394),f251(f4(x4395),x4396))
% 63.07/63.21 [440]~P7(x4407)+~P7(x4405)+~P7(x4403)+~P6(f4(x4408),x4403,x4405,x4407)+~P3(f4(x4409),f4(x4401),f4(x4406),f4(x44010))+~P3(f4(x4402),f4(x4404),f4(x4409),f4(x44011))+~P3(f4(x44011),f4(x44010),f4(x4408),f4(a2))+P6(f4(x4401),f251(f4(x4402),x4403),f251(f4(x4404),x4405),f251(f4(x4406),x4407))
% 63.07/63.21 %EqnAxiom
% 63.07/63.21 [1]E(x11,x11)
% 63.07/63.21 [2]E(x22,x21)+~E(x21,x22)
% 63.07/63.21 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 63.07/63.21 [4]~E(x41,x42)+E(f4(x41),f4(x42))
% 63.07/63.21 [5]~E(x51,x52)+E(f251(x51,x53),f251(x52,x53))
% 63.07/63.21 [6]~E(x61,x62)+E(f251(x63,x61),f251(x63,x62))
% 63.07/63.21 [7]~E(x71,x72)+E(f133(x71),f133(x72))
% 63.07/63.21 [8]~E(x81,x82)+E(f121(x81),f121(x82))
% 63.07/63.21 [9]~P1(x91)+P1(x92)+~E(x91,x92)
% 63.07/63.21 [10]P3(x102,x103,x104,x105)+~E(x101,x102)+~P3(x101,x103,x104,x105)
% 63.07/63.21 [11]P3(x113,x112,x114,x115)+~E(x111,x112)+~P3(x113,x111,x114,x115)
% 63.07/63.21 [12]P3(x123,x124,x122,x125)+~E(x121,x122)+~P3(x123,x124,x121,x125)
% 63.07/63.21 [13]P3(x133,x134,x135,x132)+~E(x131,x132)+~P3(x133,x134,x135,x131)
% 63.07/63.21 [14]P6(x142,x143,x144,x145)+~E(x141,x142)+~P6(x141,x143,x144,x145)
% 63.07/63.21 [15]P6(x153,x152,x154,x155)+~E(x151,x152)+~P6(x153,x151,x154,x155)
% 63.07/63.21 [16]P6(x163,x164,x162,x165)+~E(x161,x162)+~P6(x163,x164,x161,x165)
% 63.07/63.21 [17]P6(x173,x174,x175,x172)+~E(x171,x172)+~P6(x173,x174,x175,x171)
% 63.07/63.21 [18]~P7(x181)+P7(x182)+~E(x181,x182)
% 63.07/63.21 [19]P4(x192,x193)+~E(x191,x192)+~P4(x191,x193)
% 63.07/63.21 [20]P4(x203,x202)+~E(x201,x202)+~P4(x203,x201)
% 63.07/63.21 [21]P8(x212,x213)+~E(x211,x212)+~P8(x211,x213)
% 63.07/63.21 [22]P8(x223,x222)+~E(x221,x222)+~P8(x223,x221)
% 63.07/63.21 [23]P5(x232,x233)+~E(x231,x232)+~P5(x231,x233)
% 63.07/63.21 [24]P5(x243,x242)+~E(x241,x242)+~P5(x243,x241)
% 63.07/63.21 [25]P9(x252,x253)+~E(x251,x252)+~P9(x251,x253)
% 63.07/63.21 [26]P9(x263,x262)+~E(x261,x262)+~P9(x263,x261)
% 63.07/63.21 [27]P10(x272,x273,x274)+~E(x271,x272)+~P10(x271,x273,x274)
% 63.07/63.21 [28]P10(x283,x282,x284)+~E(x281,x282)+~P10(x283,x281,x284)
% 63.07/63.21 [29]P10(x293,x294,x292)+~E(x291,x292)+~P10(x293,x294,x291)
% 63.07/63.21 [30]P2(x302,x303,x304)+~E(x301,x302)+~P2(x301,x303,x304)
% 63.07/63.21 [31]P2(x313,x312,x314)+~E(x311,x312)+~P2(x313,x311,x314)
% 63.07/63.21 [32]P2(x323,x324,x322)+~E(x321,x322)+~P2(x323,x324,x321)
% 63.07/63.21
% 63.07/63.21 %-------------------------------------------
% 63.23/63.23 cnf(441,plain,
% 63.23/63.23 (P4(x4411,x4411)),
% 63.23/63.23 inference(equality_inference,[],[409])).
% 63.23/63.23 cnf(442,plain,
% 63.23/63.23 (~P5(x4421,x4421)),
% 63.23/63.23 inference(equality_inference,[],[410])).
% 63.23/63.23 cnf(445,plain,
% 63.23/63.23 (P10(a1,a122,a2)),
% 63.23/63.23 inference(scs_inference,[],[51,52,61,418,423])).
% 63.23/63.23 cnf(449,plain,
% 63.23/63.23 (P10(a122,a1,a2)),
% 63.23/63.23 inference(scs_inference,[],[308,51,52,61,418,423,437,431])).
% 63.23/63.23 cnf(451,plain,
% 63.23/63.23 (~P8(f4(a1),f4(a1))),
% 63.23/63.23 inference(scs_inference,[],[442,308,51,52,61,418,423,437,431,419])).
% 63.23/63.23 cnf(452,plain,
% 63.23/63.23 (~P5(x4521,x4521)),
% 63.23/63.23 inference(rename_variables,[],[442])).
% 63.23/63.23 cnf(455,plain,
% 63.23/63.23 (~P5(x4551,x4551)),
% 63.23/63.23 inference(rename_variables,[],[442])).
% 63.23/63.23 cnf(457,plain,
% 63.23/63.23 (P10(a2,a2,a2)),
% 63.23/63.23 inference(scs_inference,[],[442,452,308,51,52,61,418,423,437,431,419,420,432])).
% 63.23/63.23 cnf(459,plain,
% 63.23/63.23 (~P5(a2,a122)),
% 63.23/63.23 inference(scs_inference,[],[442,452,308,51,52,61,418,423,437,431,419,420,432,415])).
% 63.23/63.23 cnf(463,plain,
% 63.23/63.23 (~E(f4(a1),f4(a2))),
% 63.23/63.23 inference(scs_inference,[],[70,442,452,308,42,51,52,61,418,423,437,431,419,420,432,415,30,21,22])).
% 63.23/63.23 cnf(465,plain,
% 63.23/63.23 (~P5(x4651,x4651)),
% 63.23/63.23 inference(rename_variables,[],[442])).
% 63.23/63.23 cnf(468,plain,
% 63.23/63.23 (~P8(f4(a1),f4(a2))),
% 63.23/63.23 inference(scs_inference,[],[70,442,452,455,465,308,42,51,52,61,418,423,437,431,419,420,432,415,30,21,22,23,24,421])).
% 63.23/63.23 cnf(470,plain,
% 63.23/63.23 (~E(a2,a1)),
% 63.23/63.23 inference(scs_inference,[],[70,442,452,455,465,308,42,51,52,61,418,423,437,431,419,420,432,415,30,21,22,23,24,421,4])).
% 63.23/63.23 cnf(482,plain,
% 63.23/63.23 (~E(a1,a2)),
% 63.23/63.23 inference(scs_inference,[],[463,4])).
% 63.23/63.23 cnf(483,plain,
% 63.23/63.23 (P5(a134,a5)),
% 63.23/63.23 inference(scs_inference,[],[463,53,62,4,418])).
% 63.23/63.23 cnf(485,plain,
% 63.23/63.23 (~P8(f4(a5),f4(a2))),
% 63.23/63.23 inference(scs_inference,[],[463,468,43,53,62,4,418,421])).
% 63.23/63.23 cnf(487,plain,
% 63.23/63.23 (P6(f4(a1),f4(a2),f4(a2),f4(a1))),
% 63.23/63.23 inference(scs_inference,[],[463,468,309,43,53,62,308,4,418,421,437])).
% 63.23/63.23 cnf(489,plain,
% 63.23/63.23 (P10(a5,a134,a2)),
% 63.23/63.23 inference(scs_inference,[],[463,468,309,43,53,62,308,4,418,421,437,423])).
% 63.23/63.23 cnf(491,plain,
% 63.23/63.23 (~E(f4(a5),f4(a1))),
% 63.23/63.23 inference(scs_inference,[],[451,463,468,309,43,53,62,308,4,418,421,437,423,22])).
% 63.23/63.23 cnf(492,plain,
% 63.23/63.23 (~E(a5,a134)),
% 63.23/63.23 inference(scs_inference,[],[442,451,463,468,309,43,53,62,308,4,418,421,437,423,22,24])).
% 63.23/63.23 cnf(493,plain,
% 63.23/63.23 (~P5(x4931,x4931)),
% 63.23/63.23 inference(rename_variables,[],[442])).
% 63.23/63.23 cnf(495,plain,
% 63.23/63.23 (~P5(x4951,x4951)),
% 63.23/63.23 inference(rename_variables,[],[442])).
% 63.23/63.23 cnf(496,plain,
% 63.23/63.23 (~P8(f4(a5),f4(a5))),
% 63.23/63.23 inference(scs_inference,[],[442,493,495,451,463,468,309,43,53,62,308,4,418,421,437,423,22,24,23,420])).
% 63.23/63.23 cnf(497,plain,
% 63.23/63.23 (~P5(x4971,x4971)),
% 63.23/63.23 inference(rename_variables,[],[442])).
% 63.23/63.23 cnf(499,plain,
% 63.23/63.23 (P10(a134,a5,a2)),
% 63.23/63.23 inference(scs_inference,[],[442,493,495,451,463,468,309,43,53,62,308,4,418,421,437,423,22,24,23,420,431])).
% 63.23/63.23 cnf(501,plain,
% 63.23/63.23 (~P8(f4(a44),f4(a44))),
% 63.23/63.23 inference(scs_inference,[],[442,493,495,497,451,463,468,309,43,53,62,63,308,4,418,421,437,423,22,24,23,420,431,419])).
% 63.23/63.23 cnf(507,plain,
% 63.23/63.23 (~E(f4(a1),f4(a5))),
% 63.23/63.23 inference(scs_inference,[],[442,493,495,497,451,463,468,309,43,53,62,63,308,4,418,421,437,423,22,24,23,420,431,419,415,13,21])).
% 63.23/63.23 cnf(519,plain,
% 63.23/63.23 (~E(a1,a5)),
% 63.23/63.23 inference(scs_inference,[],[507,4])).
% 63.23/63.23 cnf(520,plain,
% 63.23/63.23 (P5(a185,a2)),
% 63.23/63.23 inference(scs_inference,[],[507,51,64,4,418])).
% 63.23/63.23 cnf(522,plain,
% 63.23/63.23 (P6(f4(a5),f4(a2),f4(a2),f4(a5))),
% 63.23/63.23 inference(scs_inference,[],[507,51,310,64,308,4,418,437])).
% 63.23/63.23 cnf(524,plain,
% 63.23/63.23 (~P8(f4(a5),f4(a1))),
% 63.23/63.23 inference(scs_inference,[],[507,51,496,310,64,43,308,4,418,437,421])).
% 63.23/63.23 cnf(526,plain,
% 63.23/63.23 (P10(a55,a185,a2)),
% 63.23/63.23 inference(scs_inference,[],[507,51,496,310,55,64,43,308,4,418,437,421,423])).
% 63.23/63.23 cnf(528,plain,
% 63.23/63.23 (~E(f4(a44),f4(a5))),
% 63.23/63.23 inference(scs_inference,[],[507,51,496,310,44,55,64,43,308,4,418,437,421,423,22])).
% 63.23/63.23 cnf(529,plain,
% 63.23/63.23 (~E(f4(a5),f4(a44))),
% 63.23/63.23 inference(scs_inference,[],[507,51,496,501,310,44,55,64,43,308,4,418,437,421,423,22,21])).
% 63.23/63.23 cnf(531,plain,
% 63.23/63.23 (~P5(x5311,x5311)),
% 63.23/63.23 inference(rename_variables,[],[442])).
% 63.23/63.23 cnf(532,plain,
% 63.23/63.23 (~E(a185,a2)),
% 63.23/63.23 inference(scs_inference,[],[507,442,531,51,496,501,310,44,55,64,43,308,4,418,437,421,423,22,21,24,23])).
% 63.23/63.23 cnf(533,plain,
% 63.23/63.23 (~P5(x5331,x5331)),
% 63.23/63.23 inference(rename_variables,[],[442])).
% 63.23/63.23 cnf(534,plain,
% 63.23/63.23 (~P8(f4(a55),f4(a55))),
% 63.23/63.23 inference(scs_inference,[],[507,442,531,533,51,496,501,310,44,55,64,43,308,4,418,437,421,423,22,21,24,23,420])).
% 63.23/63.23 cnf(535,plain,
% 63.23/63.23 (~P5(x5351,x5351)),
% 63.23/63.23 inference(rename_variables,[],[442])).
% 63.23/63.23 cnf(537,plain,
% 63.23/63.23 (~P8(f4(a66),f4(a66))),
% 63.23/63.23 inference(scs_inference,[],[507,442,531,533,535,51,496,501,310,44,55,64,65,43,308,4,418,437,421,423,22,21,24,23,420,419])).
% 63.23/63.23 cnf(540,plain,
% 63.23/63.23 (P10(a185,a55,a2)),
% 63.23/63.23 inference(scs_inference,[],[507,442,531,533,535,51,496,501,310,44,55,64,65,43,308,4,418,437,421,423,22,21,24,23,420,419,431])).
% 63.23/63.23 cnf(544,plain,
% 63.23/63.23 (P10(x5441,a1,a2)+~E(a122,x5441)),
% 63.23/63.23 inference(scs_inference,[],[449,507,442,531,533,535,51,496,501,310,44,55,64,65,43,308,4,418,437,421,423,22,21,24,23,420,419,431,415,27])).
% 63.23/63.23 cnf(548,plain,
% 63.23/63.23 (~E(a5,a44)),
% 63.23/63.23 inference(scs_inference,[],[529,4])).
% 63.23/63.23 cnf(549,plain,
% 63.23/63.23 (~P8(f4(a55),f4(a44))),
% 63.23/63.23 inference(scs_inference,[],[529,534,45,4,421])).
% 63.23/63.23 cnf(551,plain,
% 63.23/63.23 (P5(a207,a2)),
% 63.23/63.23 inference(scs_inference,[],[529,51,534,45,66,4,421,418])).
% 63.23/63.23 cnf(553,plain,
% 63.23/63.23 (P10(a77,a207,a2)),
% 63.23/63.23 inference(scs_inference,[],[529,51,534,45,57,66,4,421,418,423])).
% 63.23/63.23 cnf(558,plain,
% 63.23/63.23 (~E(f4(a44),f4(a55))),
% 63.23/63.23 inference(scs_inference,[],[529,51,534,311,45,57,66,501,308,4,421,418,423,437,22,21])).
% 63.23/63.23 cnf(559,plain,
% 63.23/63.23 (~E(a207,a2)),
% 63.23/63.23 inference(scs_inference,[],[529,442,51,534,311,45,57,66,501,308,4,421,418,423,437,22,21,23])).
% 63.23/63.23 cnf(560,plain,
% 63.23/63.23 (~P5(x5601,x5601)),
% 63.23/63.23 inference(rename_variables,[],[442])).
% 63.23/63.23 cnf(562,plain,
% 63.23/63.23 (~P5(x5621,x5621)),
% 63.23/63.23 inference(rename_variables,[],[442])).
% 63.23/63.23 cnf(563,plain,
% 63.23/63.23 (~P8(f4(a77),f4(a77))),
% 63.23/63.23 inference(scs_inference,[],[529,442,560,562,51,534,311,45,57,66,501,308,4,421,418,423,437,22,21,23,24,419])).
% 63.23/63.23 cnf(564,plain,
% 63.23/63.23 (~P5(x5641,x5641)),
% 63.23/63.23 inference(rename_variables,[],[442])).
% 63.23/63.23 cnf(566,plain,
% 63.23/63.23 (~P8(f4(a88),f4(a88))),
% 63.23/63.23 inference(scs_inference,[],[529,442,560,562,564,51,534,311,45,57,58,66,501,308,4,421,418,423,437,22,21,23,24,419,420])).
% 63.23/63.23 cnf(569,plain,
% 63.23/63.23 (P10(a207,a77,a2)),
% 63.23/63.23 inference(scs_inference,[],[529,442,560,562,564,51,534,311,45,57,58,66,501,308,4,421,418,423,437,22,21,23,24,419,420,431])).
% 63.23/63.23 cnf(571,plain,
% 63.23/63.23 (~P5(a2,a207)),
% 63.23/63.23 inference(scs_inference,[],[529,442,560,562,564,51,534,311,45,57,58,66,501,308,4,421,418,423,437,22,21,23,24,419,420,431,415])).
% 63.23/63.23 cnf(577,plain,
% 63.23/63.23 (P10(x5771,a5,a2)+~E(a134,x5771)),
% 63.23/63.23 inference(scs_inference,[],[449,529,499,442,560,562,564,51,534,487,311,45,57,58,66,501,308,4,421,418,423,437,22,21,23,24,419,420,431,415,14,15,16,28,27])).
% 63.23/63.23 cnf(585,plain,
% 63.23/63.23 (~E(a44,a55)),
% 63.23/63.23 inference(scs_inference,[],[558,4])).
% 63.23/63.23 cnf(586,plain,
% 63.23/63.23 (P10(a88,a218,a2)),
% 63.23/63.23 inference(scs_inference,[],[558,67,58,4,423])).
% 63.23/63.23 cnf(588,plain,
% 63.23/63.23 (P6(f4(a55),f4(a2),f4(a2),f4(a55))),
% 63.23/63.23 inference(scs_inference,[],[558,312,67,58,308,4,423,437])).
% 63.23/63.23 cnf(590,plain,
% 63.23/63.23 (~P8(f4(a66),f4(a55))),
% 63.23/63.23 inference(scs_inference,[],[558,537,312,46,67,58,308,4,423,437,421])).
% 63.23/63.23 cnf(592,plain,
% 63.23/63.23 (P5(a218,a2)),
% 63.23/63.23 inference(scs_inference,[],[558,51,537,312,46,67,58,308,4,423,437,421,418])).
% 63.23/63.23 cnf(594,plain,
% 63.23/63.23 (~E(f4(a66),f4(a44))),
% 63.23/63.23 inference(scs_inference,[],[558,51,537,549,312,46,67,58,308,4,423,437,421,418,22])).
% 63.23/63.23 cnf(595,plain,
% 63.23/63.23 (~E(f4(a55),f4(a66))),
% 63.23/63.23 inference(scs_inference,[],[558,51,537,549,312,46,67,58,308,4,423,437,421,418,22,21])).
% 63.23/63.23 cnf(597,plain,
% 63.23/63.23 (~P5(x5971,x5971)),
% 63.23/63.23 inference(rename_variables,[],[442])).
% 63.23/63.23 cnf(598,plain,
% 63.23/63.23 (~E(a218,a2)),
% 63.23/63.23 inference(scs_inference,[],[558,442,597,51,537,549,312,46,67,58,308,4,423,437,421,418,22,21,24,23])).
% 63.23/63.23 cnf(599,plain,
% 63.23/63.23 (~P5(x5991,x5991)),
% 63.23/63.23 inference(rename_variables,[],[442])).
% 63.23/63.23 cnf(600,plain,
% 63.23/63.23 (~P8(f4(a99),f4(a99))),
% 63.23/63.23 inference(scs_inference,[],[558,442,597,599,51,537,549,312,46,59,67,58,308,4,423,437,421,418,22,21,24,23,420])).
% 63.23/63.23 cnf(601,plain,
% 63.23/63.23 (~P5(x6011,x6011)),
% 63.23/63.23 inference(rename_variables,[],[442])).
% 63.23/63.23 cnf(603,plain,
% 63.23/63.23 (~P8(f4(a110),f4(a110))),
% 63.23/63.23 inference(scs_inference,[],[558,442,597,599,601,51,537,549,312,46,59,67,69,58,308,4,423,437,421,418,22,21,24,23,420,419])).
% 63.23/63.23 cnf(606,plain,
% 63.23/63.23 (P10(a218,a88,a2)),
% 63.23/63.23 inference(scs_inference,[],[558,442,597,599,601,51,537,549,312,46,59,67,69,58,308,4,423,437,421,418,22,21,24,23,420,419,431])).
% 63.23/63.23 cnf(613,plain,
% 63.23/63.23 (P9(x6131,f121(f4(a2)))+~E(a2,x6131)),
% 63.23/63.23 inference(scs_inference,[],[449,558,442,597,599,601,51,537,522,549,312,46,59,67,69,58,308,4,423,437,421,418,22,21,24,23,420,419,431,415,17,29,11,25])).
% 63.23/63.23 cnf(622,plain,
% 63.23/63.23 (~E(a55,a66)),
% 63.23/63.23 inference(scs_inference,[],[595,4])).
% 63.23/63.23 cnf(623,plain,
% 63.23/63.23 (~P8(f4(a77),f4(a66))),
% 63.23/63.23 inference(scs_inference,[],[595,563,47,4,421])).
% 63.23/63.23 cnf(625,plain,
% 63.23/63.23 (P10(a99,a229,a2)),
% 63.23/63.23 inference(scs_inference,[],[595,563,47,68,59,4,421,423])).
% 63.23/63.23 cnf(627,plain,
% 63.23/63.23 (P5(a229,a2)),
% 63.23/63.23 inference(scs_inference,[],[595,51,563,47,68,59,4,421,423,418])).
% 63.23/63.23 cnf(629,plain,
% 63.23/63.23 (P6(f4(a66),f4(a2),f4(a2),f4(a66))),
% 63.23/63.23 inference(scs_inference,[],[595,51,563,313,47,68,59,308,4,421,423,418,437])).
% 63.23/63.23 cnf(632,plain,
% 63.23/63.23 (~E(f4(a66),f4(a77))),
% 63.23/63.23 inference(scs_inference,[],[595,51,563,590,313,47,68,59,308,4,421,423,418,437,22,21])).
% 63.23/63.23 cnf(633,plain,
% 63.23/63.23 (~E(a229,a2)),
% 63.23/63.23 inference(scs_inference,[],[595,442,51,563,590,313,47,68,59,308,4,421,423,418,437,22,21,23])).
% 63.23/63.23 cnf(634,plain,
% 63.23/63.23 (~P5(x6341,x6341)),
% 63.23/63.23 inference(rename_variables,[],[442])).
% 63.23/63.23 cnf(636,plain,
% 63.23/63.23 (~P5(x6361,x6361)),
% 63.23/63.23 inference(rename_variables,[],[442])).
% 63.23/63.23 cnf(638,plain,
% 63.23/63.23 (~P5(x6381,x6381)),
% 63.23/63.23 inference(rename_variables,[],[442])).
% 63.23/63.23 cnf(643,plain,
% 63.23/63.23 (P10(a229,a99,a2)),
% 63.23/63.23 inference(scs_inference,[],[595,442,634,636,638,51,563,590,313,47,68,161,72,59,308,4,421,423,418,437,22,21,23,24,419,420,431])).
% 63.23/63.23 cnf(659,plain,
% 63.23/63.23 (~E(a66,a77)),
% 63.23/63.23 inference(scs_inference,[],[632,4])).
% 63.23/63.23 cnf(660,plain,
% 63.23/63.23 (~P8(f4(a99),f4(a88))),
% 63.23/63.23 inference(scs_inference,[],[632,600,49,4,421])).
% 63.23/63.23 cnf(662,plain,
% 63.23/63.23 (P5(a136,a2)),
% 63.23/63.23 inference(scs_inference,[],[632,51,600,49,162,4,421,418])).
% 63.23/63.23 cnf(664,plain,
% 63.23/63.23 (P10(a7,a136,a2)),
% 63.23/63.23 inference(scs_inference,[],[632,51,600,49,162,72,4,421,418,423])).
% 63.23/63.23 cnf(668,plain,
% 63.23/63.23 (~E(f4(a88),f4(a66))),
% 63.23/63.23 inference(scs_inference,[],[632,51,600,623,314,48,49,162,72,308,4,421,418,423,437,22])).
% 63.23/63.23 cnf(669,plain,
% 63.23/63.23 (~E(f4(a77),f4(a88))),
% 63.23/63.23 inference(scs_inference,[],[632,51,600,566,623,314,48,49,162,72,308,4,421,418,423,437,22,21])).
% 63.23/63.23 cnf(671,plain,
% 63.23/63.23 (~P5(x6711,x6711)),
% 63.23/63.23 inference(rename_variables,[],[442])).
% 63.23/63.23 cnf(672,plain,
% 63.23/63.23 (~E(a136,a2)),
% 63.23/63.23 inference(scs_inference,[],[632,442,671,51,600,566,623,314,48,49,162,72,308,4,421,418,423,437,22,21,24,23])).
% 63.23/63.23 cnf(673,plain,
% 63.23/63.23 (~P5(x6731,x6731)),
% 63.23/63.23 inference(rename_variables,[],[442])).
% 63.23/63.23 cnf(675,plain,
% 63.23/63.23 (~P5(x6751,x6751)),
% 63.23/63.23 inference(rename_variables,[],[442])).
% 63.23/63.23 cnf(680,plain,
% 63.23/63.23 (P10(a136,a7,a2)),
% 63.23/63.23 inference(scs_inference,[],[632,442,671,673,675,51,600,566,623,314,48,49,162,163,74,72,308,4,421,418,423,437,22,21,24,23,419,420,431])).
% 63.23/63.23 cnf(685,plain,
% 63.23/63.23 (P10(a207,x6851,a2)+~E(a77,x6851)),
% 63.23/63.23 inference(scs_inference,[],[632,569,442,671,673,675,51,600,566,623,314,48,49,162,163,74,72,308,4,421,418,423,437,22,21,24,23,419,420,431,415,13,28])).
% 63.23/63.23 cnf(687,plain,
% 63.23/63.23 (P10(x6871,a77,a2)+~E(a207,x6871)),
% 63.23/63.23 inference(scs_inference,[],[632,569,442,671,673,675,51,600,566,588,623,314,48,49,162,163,74,72,308,4,421,418,423,437,22,21,24,23,419,420,431,415,13,28,17,27])).
% 63.23/63.23 cnf(688,plain,
% 63.23/63.23 (P9(x6881,f121(f4(a44)))+~E(a44,x6881)),
% 63.23/63.23 inference(scs_inference,[],[632,569,442,671,673,675,51,600,566,588,623,314,48,49,54,162,163,74,72,308,4,421,418,423,437,22,21,24,23,419,420,431,415,13,28,17,27,25])).
% 63.23/63.23 cnf(696,plain,
% 63.23/63.23 (~E(a77,a88)),
% 63.23/63.23 inference(scs_inference,[],[669,4])).
% 63.23/63.23 cnf(697,plain,
% 63.23/63.23 (~P8(f4(a110),f4(a99))),
% 63.23/63.23 inference(scs_inference,[],[669,603,50,4,421])).
% 63.23/63.23 cnf(699,plain,
% 63.23/63.23 (P10(a29,a158,a2)),
% 63.23/63.23 inference(scs_inference,[],[669,603,50,164,74,4,421,423])).
% 63.23/63.23 cnf(701,plain,
% 63.23/63.23 (P5(a158,a2)),
% 63.23/63.23 inference(scs_inference,[],[669,51,603,50,164,74,4,421,423,418])).
% 63.23/63.23 cnf(705,plain,
% 63.23/63.23 (~E(f4(a110),f4(a88))),
% 63.23/63.23 inference(scs_inference,[],[669,51,603,660,315,50,164,74,308,4,421,423,418,437,22])).
% 63.23/63.23 cnf(706,plain,
% 63.23/63.23 (~E(f4(a99),f4(a110))),
% 63.23/63.23 inference(scs_inference,[],[669,51,603,660,315,50,164,74,308,4,421,423,418,437,22,21])).
% 63.23/63.23 cnf(707,plain,
% 63.23/63.23 (~E(a158,a2)),
% 63.23/63.23 inference(scs_inference,[],[669,442,51,603,660,315,50,164,74,308,4,421,423,418,437,22,21,23])).
% 63.23/63.23 cnf(708,plain,
% 63.23/63.23 (~P5(x7081,x7081)),
% 63.23/63.23 inference(rename_variables,[],[442])).
% 63.23/63.23 cnf(709,plain,
% 63.23/63.23 (~E(a2,a158)),
% 63.23/63.23 inference(scs_inference,[],[669,442,708,51,603,660,315,50,164,74,308,4,421,423,418,437,22,21,23,24])).
% 63.23/63.23 cnf(710,plain,
% 63.23/63.23 (~P5(x7101,x7101)),
% 63.23/63.23 inference(rename_variables,[],[442])).
% 63.23/63.23 cnf(712,plain,
% 63.23/63.23 (~P5(x7121,x7121)),
% 63.23/63.23 inference(rename_variables,[],[442])).
% 63.23/63.23 cnf(717,plain,
% 63.23/63.23 (P10(a158,a29,a2)),
% 63.23/63.23 inference(scs_inference,[],[669,442,708,710,712,51,603,660,315,50,164,165,76,74,308,4,421,423,418,437,22,21,23,24,419,420,431])).
% 63.23/63.23 cnf(726,plain,
% 63.23/63.23 (P9(x7261,f121(f4(a66)))+~E(a66,x7261)),
% 63.23/63.23 inference(scs_inference,[],[669,606,442,708,710,712,51,603,629,660,315,50,56,164,165,76,74,308,4,421,423,418,437,22,21,23,24,419,420,431,415,12,29,26,16,14,25])).
% 63.23/63.23 cnf(733,plain,
% 63.23/63.23 (~E(a99,a110)),
% 63.23/63.23 inference(scs_inference,[],[706,4])).
% 63.23/63.23 cnf(734,plain,
% 63.23/63.23 (~P8(f4(a44),f4(a2))),
% 63.23/63.23 inference(scs_inference,[],[706,485,44,4,421])).
% 63.23/63.23 cnf(736,plain,
% 63.23/63.23 (P5(a169,a2)),
% 63.23/63.23 inference(scs_inference,[],[706,51,485,166,44,4,421,418])).
% 63.23/63.23 cnf(738,plain,
% 63.23/63.23 (P10(a39,a169,a2)),
% 63.23/63.23 inference(scs_inference,[],[706,51,485,166,76,44,4,421,418,423])).
% 63.23/63.23 cnf(742,plain,
% 63.23/63.23 (~E(f4(a99),f4(a88))),
% 63.23/63.23 inference(scs_inference,[],[706,51,485,316,166,566,49,76,44,308,4,421,418,423,437,22])).
% 63.23/63.23 cnf(743,plain,
% 63.23/63.23 (~E(f4(a88),f4(a110))),
% 63.23/63.23 inference(scs_inference,[],[706,51,485,697,316,166,566,49,76,44,308,4,421,418,423,437,22,21])).
% 63.23/63.23 cnf(744,plain,
% 63.23/63.23 (~E(a2,a169)),
% 63.23/63.23 inference(scs_inference,[],[706,442,51,485,697,316,166,566,49,76,44,308,4,421,418,423,437,22,21,24])).
% 63.23/63.23 cnf(745,plain,
% 63.23/63.24 (~P5(x7451,x7451)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(746,plain,
% 63.23/63.24 (~E(a169,a2)),
% 63.23/63.24 inference(scs_inference,[],[706,442,745,51,485,697,316,166,566,49,76,44,308,4,421,418,423,437,22,21,24,23])).
% 63.23/63.24 cnf(747,plain,
% 63.23/63.24 (~P5(x7471,x7471)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(749,plain,
% 63.23/63.24 (~P5(x7491,x7491)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(754,plain,
% 63.23/63.24 (P10(a169,a39,a2)),
% 63.23/63.24 inference(scs_inference,[],[706,442,745,747,749,51,485,697,316,166,167,78,566,49,76,44,308,4,421,418,423,437,22,21,24,23,419,420,431])).
% 63.23/63.24 cnf(759,plain,
% 63.23/63.24 (P10(x7591,a99,a2)+~E(a229,x7591)),
% 63.23/63.24 inference(scs_inference,[],[706,643,442,745,747,749,51,485,697,316,166,167,78,566,49,76,44,308,4,421,418,423,437,22,21,24,23,419,420,431,415,13,27])).
% 63.23/63.24 cnf(771,plain,
% 63.23/63.24 (~P8(f4(a55),f4(a2))),
% 63.23/63.24 inference(scs_inference,[],[743,734,45,4,421])).
% 63.23/63.24 cnf(773,plain,
% 63.23/63.24 (P10(a41,a171,a2)),
% 63.23/63.24 inference(scs_inference,[],[743,734,168,78,45,4,421,423])).
% 63.23/63.24 cnf(775,plain,
% 63.23/63.24 (P5(a171,a2)),
% 63.23/63.24 inference(scs_inference,[],[743,51,734,168,78,45,4,421,423,418])).
% 63.23/63.24 cnf(777,plain,
% 63.23/63.24 (~E(f4(a44),f4(a1))),
% 63.23/63.24 inference(scs_inference,[],[743,51,524,734,168,78,44,45,4,421,423,418,22])).
% 63.23/63.24 cnf(780,plain,
% 63.23/63.24 (~E(f4(a77),f4(a99))),
% 63.23/63.24 inference(scs_inference,[],[743,51,524,734,317,168,660,78,48,44,45,308,4,421,423,418,22,437,21])).
% 63.23/63.24 cnf(781,plain,
% 63.23/63.24 (~E(a171,a2)),
% 63.23/63.24 inference(scs_inference,[],[743,442,51,524,734,317,168,660,78,48,44,45,308,4,421,423,418,22,437,21,23])).
% 63.23/63.24 cnf(782,plain,
% 63.23/63.24 (~P5(x7821,x7821)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(783,plain,
% 63.23/63.24 (~E(a2,a171)),
% 63.23/63.24 inference(scs_inference,[],[743,442,782,51,524,734,317,168,660,78,48,44,45,308,4,421,423,418,22,437,21,23,24])).
% 63.23/63.24 cnf(807,plain,
% 63.23/63.24 (~E(a77,a99)),
% 63.23/63.24 inference(scs_inference,[],[780,4])).
% 63.23/63.24 cnf(808,plain,
% 63.23/63.24 (~P8(f4(a66),f4(a2))),
% 63.23/63.24 inference(scs_inference,[],[780,771,46,4,421])).
% 63.23/63.24 cnf(810,plain,
% 63.23/63.24 (P5(a173,a2)),
% 63.23/63.24 inference(scs_inference,[],[780,51,771,170,46,4,421,418])).
% 63.23/63.24 cnf(812,plain,
% 63.23/63.24 (P10(a43,a173,a2)),
% 63.23/63.24 inference(scs_inference,[],[780,51,771,170,80,46,4,421,418,423])).
% 63.23/63.24 cnf(816,plain,
% 63.23/63.24 (~E(f4(a66),f4(a2))),
% 63.23/63.24 inference(scs_inference,[],[780,51,771,318,170,80,46,4,421,418,423,437,22])).
% 63.23/63.24 cnf(818,plain,
% 63.23/63.24 (~P5(x8181,x8181)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(819,plain,
% 63.23/63.24 (~E(f4(a55),f4(a77))),
% 63.23/63.24 inference(scs_inference,[],[780,442,51,771,318,170,623,80,46,4,421,418,423,437,22,24,21])).
% 63.23/63.24 cnf(820,plain,
% 63.23/63.24 (~E(a173,a2)),
% 63.23/63.24 inference(scs_inference,[],[780,442,818,51,771,318,170,623,80,46,4,421,418,423,437,22,24,21,23])).
% 63.23/63.24 cnf(844,plain,
% 63.23/63.24 (~E(a55,a77)),
% 63.23/63.24 inference(scs_inference,[],[819,4])).
% 63.23/63.24 cnf(845,plain,
% 63.23/63.24 (~P8(f4(a77),f4(a2))),
% 63.23/63.24 inference(scs_inference,[],[819,808,47,4,421])).
% 63.23/63.24 cnf(849,plain,
% 63.23/63.24 (P5(a176,a2)),
% 63.23/63.24 inference(scs_inference,[],[819,51,808,172,82,47,4,421,423,418])).
% 63.23/63.24 cnf(855,plain,
% 63.23/63.24 (~P5(x8551,x8551)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(858,plain,
% 63.23/63.24 (~E(f4(a88),f4(a99))),
% 63.23/63.24 inference(scs_inference,[],[819,442,855,51,808,319,172,600,82,309,47,49,4,421,423,418,437,22,24,23,21])).
% 63.23/63.24 cnf(876,plain,
% 63.23/63.24 (~E(a88,a99)),
% 63.23/63.24 inference(scs_inference,[],[858,4])).
% 63.23/63.24 cnf(877,plain,
% 63.23/63.24 (~P8(f4(a88),f4(a2))),
% 63.23/63.24 inference(scs_inference,[],[858,845,48,4,421])).
% 63.23/63.24 cnf(879,plain,
% 63.23/63.24 (P5(a178,a2)),
% 63.23/63.24 inference(scs_inference,[],[858,51,845,174,48,4,421,418])).
% 63.23/63.24 cnf(881,plain,
% 63.23/63.24 (P10(a48,a178,a2)),
% 63.23/63.24 inference(scs_inference,[],[858,51,845,174,84,48,4,421,418,423])).
% 63.23/63.24 cnf(885,plain,
% 63.23/63.24 (~E(f4(a88),f4(a2))),
% 63.23/63.24 inference(scs_inference,[],[858,51,845,320,174,84,309,48,4,421,418,423,437,22])).
% 63.23/63.24 cnf(886,plain,
% 63.23/63.24 (~E(f4(a5),f4(a55))),
% 63.23/63.24 inference(scs_inference,[],[858,51,845,320,174,549,84,309,48,44,4,421,418,423,437,22,21])).
% 63.23/63.24 cnf(888,plain,
% 63.23/63.24 (~P5(x8881,x8881)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(889,plain,
% 63.23/63.24 (~E(a178,a2)),
% 63.23/63.24 inference(scs_inference,[],[858,442,888,51,845,320,174,549,84,309,48,44,4,421,418,423,437,22,21,24,23])).
% 63.23/63.24 cnf(913,plain,
% 63.23/63.24 (~E(a5,a55)),
% 63.23/63.24 inference(scs_inference,[],[886,4])).
% 63.23/63.24 cnf(914,plain,
% 63.23/63.24 (~P8(f4(a99),f4(a2))),
% 63.23/63.24 inference(scs_inference,[],[886,877,49,4,421])).
% 63.23/63.24 cnf(916,plain,
% 63.23/63.24 (P10(a50,a180,a2)),
% 63.23/63.24 inference(scs_inference,[],[886,877,176,86,49,4,421,423])).
% 63.23/63.24 cnf(918,plain,
% 63.23/63.24 (P5(a180,a2)),
% 63.23/63.24 inference(scs_inference,[],[886,51,877,176,86,49,4,421,423,418])).
% 63.23/63.24 cnf(922,plain,
% 63.23/63.24 (~E(f4(a110),f4(a99))),
% 63.23/63.24 inference(scs_inference,[],[886,51,877,321,176,86,600,50,318,49,4,421,423,418,437,22])).
% 63.23/63.24 cnf(923,plain,
% 63.23/63.24 (~E(f4(a44),f4(a66))),
% 63.23/63.24 inference(scs_inference,[],[886,51,877,321,176,590,86,600,50,318,45,49,4,421,423,418,437,22,21])).
% 63.23/63.24 cnf(924,plain,
% 63.23/63.24 (~E(a180,a2)),
% 63.23/63.24 inference(scs_inference,[],[886,442,51,877,321,176,590,86,600,50,318,45,49,4,421,423,418,437,22,21,23])).
% 63.23/63.24 cnf(950,plain,
% 63.23/63.24 (~E(a44,a66)),
% 63.23/63.24 inference(scs_inference,[],[923,4])).
% 63.23/63.24 cnf(953,plain,
% 63.23/63.24 (P5(a182,a2)),
% 63.23/63.24 inference(scs_inference,[],[923,51,914,178,50,4,421,418])).
% 63.23/63.24 cnf(959,plain,
% 63.23/63.24 (~E(f4(a110),f4(a2))),
% 63.23/63.24 inference(scs_inference,[],[923,51,914,322,178,88,309,50,4,421,418,423,437,22])).
% 63.23/63.24 cnf(978,plain,
% 63.23/63.24 (~E(a5,a1)),
% 63.23/63.24 inference(scs_inference,[],[491,4])).
% 63.23/63.24 cnf(979,plain,
% 63.23/63.24 (~P8(f4(a110),f4(a88))),
% 63.23/63.24 inference(scs_inference,[],[49,491,697,4,421])).
% 63.23/63.24 cnf(981,plain,
% 63.23/63.24 (P10(a54,a184,a2)),
% 63.23/63.24 inference(scs_inference,[],[49,491,180,697,90,4,421,423])).
% 63.23/63.24 cnf(983,plain,
% 63.23/63.24 (P5(a184,a2)),
% 63.23/63.24 inference(scs_inference,[],[51,49,491,180,697,90,4,421,423,418])).
% 63.23/63.24 cnf(987,plain,
% 63.23/63.24 (~E(f4(a44),f4(a2))),
% 63.23/63.24 inference(scs_inference,[],[51,44,49,491,323,180,485,697,90,318,4,421,423,418,437,22])).
% 63.23/63.24 cnf(989,plain,
% 63.23/63.24 (~P5(x9891,x9891)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(990,plain,
% 63.23/63.24 (~E(a184,a2)),
% 63.23/63.24 inference(scs_inference,[],[442,989,51,44,49,491,323,180,485,697,90,318,4,421,423,418,437,22,24,23])).
% 63.23/63.24 cnf(1014,plain,
% 63.23/63.24 (~P10(a134,a3,a2)),
% 63.23/63.24 inference(scs_inference,[],[408,499,2,429])).
% 63.23/63.24 cnf(1017,plain,
% 63.23/63.24 (~E(a88,a66)),
% 63.23/63.24 inference(scs_inference,[],[1014,668,426,4])).
% 63.23/63.24 cnf(1018,plain,
% 63.23/63.24 (~P10(a122,a2,a2)),
% 63.23/63.24 inference(scs_inference,[],[1014,449,470,668,426,4,429])).
% 63.23/63.24 cnf(1021,plain,
% 63.23/63.24 (~P8(f4(a110),f4(a77))),
% 63.23/63.24 inference(scs_inference,[],[1014,449,470,499,48,668,979,426,4,429,28,421])).
% 63.23/63.24 cnf(1023,plain,
% 63.23/63.24 (P10(a57,a187,a2)),
% 63.23/63.24 inference(scs_inference,[],[1014,449,470,499,48,668,979,182,92,426,4,429,28,421,423])).
% 63.23/63.24 cnf(1025,plain,
% 63.23/63.24 (P5(a187,a2)),
% 63.23/63.24 inference(scs_inference,[],[1014,449,470,499,51,48,668,979,182,92,426,4,429,28,421,423,418])).
% 63.23/63.24 cnf(1030,plain,
% 63.23/63.24 (~E(f4(a77),f4(a110))),
% 63.23/63.24 inference(scs_inference,[],[1014,449,470,499,51,45,48,668,979,324,182,734,92,309,426,4,429,28,421,423,418,437,22,21])).
% 63.23/63.24 cnf(1032,plain,
% 63.23/63.24 (~P5(x10321,x10321)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(1033,plain,
% 63.23/63.24 (~E(a187,a2)),
% 63.23/63.24 inference(scs_inference,[],[1014,449,470,499,442,1032,51,45,48,668,979,324,182,734,92,309,426,4,429,28,421,423,418,437,22,21,24,23])).
% 63.23/63.24 cnf(1060,plain,
% 63.23/63.24 (~P10(a122,a5,a2)),
% 63.23/63.24 inference(scs_inference,[],[1018,449,1030,978,426,4,429])).
% 63.23/63.24 cnf(1063,plain,
% 63.23/63.24 (~P8(f4(a110),f4(a66))),
% 63.23/63.24 inference(scs_inference,[],[1018,449,1030,978,499,47,1021,426,4,429,27,421])).
% 63.23/63.24 cnf(1065,plain,
% 63.23/63.24 (P10(a59,a189,a2)),
% 63.23/63.24 inference(scs_inference,[],[1018,449,1030,978,499,47,1021,184,94,426,4,429,27,421,423])).
% 63.23/63.24 cnf(1067,plain,
% 63.23/63.24 (P5(a189,a2)),
% 63.23/63.24 inference(scs_inference,[],[1018,449,1030,978,499,51,47,1021,184,94,426,4,429,27,421,423,418])).
% 63.23/63.24 cnf(1072,plain,
% 63.23/63.24 (~E(f4(a66),f4(a110))),
% 63.23/63.24 inference(scs_inference,[],[1018,449,1030,978,499,51,47,1021,325,184,94,537,318,426,4,429,27,421,423,418,437,22,21])).
% 63.23/63.24 cnf(1074,plain,
% 63.23/63.24 (~P5(x10741,x10741)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(1075,plain,
% 63.23/63.24 (~E(a189,a2)),
% 63.23/63.24 inference(scs_inference,[],[1018,449,1030,978,499,442,1074,51,47,1021,325,184,94,537,318,426,4,429,27,421,423,418,437,22,21,24,23])).
% 63.23/63.24 cnf(1095,plain,
% 63.23/63.24 (~P10(a185,a44,a2)),
% 63.23/63.24 inference(scs_inference,[],[1060,585,1072,540,426,4,429])).
% 63.23/63.24 cnf(1098,plain,
% 63.23/63.24 (~P8(f4(a110),f4(a55))),
% 63.23/63.24 inference(scs_inference,[],[1060,585,1072,540,46,1063,426,4,429,28,421])).
% 63.23/63.24 cnf(1100,plain,
% 63.23/63.24 (P10(a61,a191,a2)),
% 63.23/63.24 inference(scs_inference,[],[1060,585,1072,540,46,1063,186,96,426,4,429,28,421,423])).
% 63.23/63.24 cnf(1102,plain,
% 63.23/63.24 (P5(a191,a2)),
% 63.23/63.24 inference(scs_inference,[],[1060,585,1072,540,51,46,1063,186,96,426,4,429,28,421,423,418])).
% 63.23/63.24 cnf(1106,plain,
% 63.23/63.24 (~E(f4(a66),f4(a55))),
% 63.23/63.24 inference(scs_inference,[],[1060,585,1072,540,51,46,1063,326,186,96,534,309,426,4,429,28,421,423,418,437,22])).
% 63.23/63.24 cnf(1107,plain,
% 63.23/63.24 (~E(f4(a55),f4(a110))),
% 63.23/63.24 inference(scs_inference,[],[1060,585,1072,540,51,46,1063,326,186,96,534,309,426,4,429,28,421,423,418,437,22,21])).
% 63.23/63.24 cnf(1108,plain,
% 63.23/63.24 (~E(a191,a2)),
% 63.23/63.24 inference(scs_inference,[],[1060,585,1072,540,442,51,46,1063,326,186,96,534,309,426,4,429,28,421,423,418,437,22,21,23])).
% 63.23/63.24 cnf(1137,plain,
% 63.23/63.24 (~P10(a218,a77,a2)),
% 63.23/63.24 inference(scs_inference,[],[1095,696,1107,606,426,4,429])).
% 63.23/63.24 cnf(1140,plain,
% 63.23/63.24 (~E(a88,a77)),
% 63.23/63.24 inference(scs_inference,[],[1095,696,1107,606,569,426,4,429,27,28])).
% 63.23/63.24 cnf(1141,plain,
% 63.23/63.24 (~P8(f4(a110),f4(a44))),
% 63.23/63.24 inference(scs_inference,[],[1095,696,1107,606,569,45,1098,426,4,429,27,28,421])).
% 63.23/63.24 cnf(1145,plain,
% 63.23/63.24 (P5(a193,a2)),
% 63.23/63.24 inference(scs_inference,[],[1095,696,1107,606,569,51,45,1098,188,98,426,4,429,27,28,421,423,418])).
% 63.23/63.24 cnf(1149,plain,
% 63.23/63.24 (~E(f4(a99),f4(a2))),
% 63.23/63.24 inference(scs_inference,[],[1095,696,1107,606,569,51,45,49,1098,328,188,877,98,426,4,429,27,28,421,423,418,437,22])).
% 63.23/63.24 cnf(1150,plain,
% 63.23/63.24 (~E(f4(a44),f4(a110))),
% 63.23/63.24 inference(scs_inference,[],[1095,696,1107,606,569,51,45,49,1098,328,188,877,98,426,4,429,27,28,421,423,418,437,22,21])).
% 63.23/63.24 cnf(1152,plain,
% 63.23/63.24 (~P5(x11521,x11521)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(1153,plain,
% 63.23/63.24 (~E(a193,a2)),
% 63.23/63.24 inference(scs_inference,[],[1095,696,1107,606,569,442,1152,51,45,49,1098,328,188,877,98,426,4,429,27,28,421,423,418,437,22,21,24,23])).
% 63.23/63.24 cnf(1180,plain,
% 63.23/63.24 (~P10(a229,a77,a2)),
% 63.23/63.24 inference(scs_inference,[],[1137,807,1150,643,426,4,429])).
% 63.23/63.24 cnf(1182,plain,
% 63.23/63.24 (~P8(f4(a110),f4(a5))),
% 63.23/63.24 inference(scs_inference,[],[1137,807,1150,643,44,1141,426,4,429,421])).
% 63.23/63.24 cnf(1184,plain,
% 63.23/63.24 (~E(a99,a77)),
% 63.23/63.24 inference(scs_inference,[],[1137,807,1150,643,44,1141,426,4,429,421,28])).
% 63.23/63.24 cnf(1185,plain,
% 63.23/63.24 (P10(a65,a195,a2)),
% 63.23/63.24 inference(scs_inference,[],[1137,807,1150,643,44,1141,190,100,426,4,429,421,28,423])).
% 63.23/63.24 cnf(1187,plain,
% 63.23/63.24 (P5(a195,a2)),
% 63.23/63.24 inference(scs_inference,[],[1137,807,1150,643,51,44,1141,190,100,426,4,429,421,28,423,418])).
% 63.23/63.24 cnf(1192,plain,
% 63.23/63.24 (~E(f4(a5),f4(a110))),
% 63.23/63.24 inference(scs_inference,[],[1137,807,1150,643,51,44,48,1141,329,190,310,100,563,426,4,429,421,28,423,418,437,22,21])).
% 63.23/63.24 cnf(1194,plain,
% 63.23/63.24 (~P5(x11941,x11941)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(1195,plain,
% 63.23/63.24 (~E(a195,a2)),
% 63.23/63.24 inference(scs_inference,[],[1137,807,1150,643,442,1194,51,44,48,1141,329,190,310,100,563,426,4,429,421,28,423,418,437,22,21,24,23])).
% 63.23/63.24 cnf(1196,plain,
% 63.23/63.24 (~P5(x11961,x11961)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(1198,plain,
% 63.23/63.24 (~P5(x11981,x11981)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(1205,plain,
% 63.23/63.24 (~E(a207,a229)),
% 63.23/63.24 inference(scs_inference,[],[1137,807,1150,643,442,1194,1196,1198,51,44,48,1141,329,190,191,102,310,100,563,426,4,429,421,28,423,418,437,22,21,24,23,419,420,431,687])).
% 63.23/63.24 cnf(1215,plain,
% 63.23/63.24 (~P10(a207,a66,a2)),
% 63.23/63.24 inference(scs_inference,[],[1180,659,1192,569,426,4,429])).
% 63.23/63.24 cnf(1217,plain,
% 63.23/63.24 (~P8(f4(a110),f4(a1))),
% 63.23/63.24 inference(scs_inference,[],[1180,659,1192,569,43,1182,426,4,429,421])).
% 63.23/63.24 cnf(1220,plain,
% 63.23/63.24 (P10(a68,a198,a2)),
% 63.23/63.24 inference(scs_inference,[],[1180,659,1192,569,43,1182,192,102,426,4,429,421,28,423])).
% 63.23/63.24 cnf(1222,plain,
% 63.23/63.24 (P5(a198,a2)),
% 63.23/63.24 inference(scs_inference,[],[1180,659,1192,569,51,43,1182,192,102,426,4,429,421,28,423,418])).
% 63.23/63.24 cnf(1227,plain,
% 63.23/63.24 (~P5(x12271,x12271)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(1228,plain,
% 63.23/63.24 (~E(f4(a1),f4(a110))),
% 63.23/63.24 inference(scs_inference,[],[1180,659,1192,569,442,51,43,1182,330,192,319,102,426,4,429,421,28,423,418,437,24,21])).
% 63.23/63.24 cnf(1229,plain,
% 63.23/63.24 (~E(a198,a2)),
% 63.23/63.24 inference(scs_inference,[],[1180,659,1192,569,442,1227,51,43,1182,330,192,319,102,426,4,429,421,28,423,418,437,24,21,23])).
% 63.23/63.24 cnf(1256,plain,
% 63.23/63.24 (~P10(a207,a55,a2)),
% 63.23/63.24 inference(scs_inference,[],[1215,569,844,1228,426,4,429])).
% 63.23/63.24 cnf(1258,plain,
% 63.23/63.24 (~P8(f4(a44),f4(a5))),
% 63.23/63.24 inference(scs_inference,[],[1215,569,844,1228,44,501,426,4,429,421])).
% 63.23/63.24 cnf(1261,plain,
% 63.23/63.24 (P10(a70,a200,a2)),
% 63.23/63.24 inference(scs_inference,[],[1215,569,844,1228,540,44,194,104,501,426,4,429,421,27,423])).
% 63.23/63.24 cnf(1263,plain,
% 63.23/63.24 (P5(a200,a2)),
% 63.23/63.24 inference(scs_inference,[],[1215,569,844,1228,540,51,44,194,104,501,426,4,429,421,27,423,418])).
% 63.23/63.24 cnf(1268,plain,
% 63.23/63.24 (~P5(x12681,x12681)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(1269,plain,
% 63.23/63.24 (~E(a200,a2)),
% 63.23/63.24 inference(scs_inference,[],[1215,569,844,1228,540,442,1268,51,44,331,194,328,104,501,426,4,429,421,27,423,418,437,24,23])).
% 63.23/63.24 cnf(1270,plain,
% 63.23/63.24 (~P5(x12701,x12701)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(1271,plain,
% 63.23/63.24 (~E(f4(a2),f4(a110))),
% 63.23/63.24 inference(scs_inference,[],[1215,569,844,1228,540,442,1268,51,42,44,1217,331,194,328,104,501,426,4,429,421,27,423,418,437,24,23,21])).
% 63.23/63.24 cnf(1273,plain,
% 63.23/63.24 (~P5(x12731,x12731)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(1278,plain,
% 63.23/63.24 (P10(a200,a70,a2)),
% 63.23/63.24 inference(scs_inference,[],[1215,569,844,1228,540,442,1268,1270,1273,51,42,44,1217,331,194,195,106,328,104,501,426,4,429,421,27,423,418,437,24,23,21,419,420,431])).
% 63.23/63.24 cnf(1280,plain,
% 63.23/63.24 (~E(a77,a55)),
% 63.23/63.24 inference(scs_inference,[],[1215,569,844,1228,540,442,1268,1270,1273,51,42,44,1217,331,194,195,106,328,104,501,426,4,429,421,27,423,418,437,24,23,21,419,420,431,685])).
% 63.23/63.24 cnf(1298,plain,
% 63.23/63.24 (~P10(a207,a88,a2)),
% 63.23/63.24 inference(scs_inference,[],[1256,569,1140,1271,426,4,429])).
% 63.23/63.24 cnf(1300,plain,
% 63.23/63.24 (~P8(f4(a44),f4(a1))),
% 63.23/63.24 inference(scs_inference,[],[1256,569,1140,1271,43,1258,426,4,429,421])).
% 63.23/63.24 cnf(1305,plain,
% 63.23/63.24 (P5(a202,a2)),
% 63.23/63.24 inference(scs_inference,[],[1256,569,606,1140,1271,51,43,1258,196,106,426,4,429,421,27,423,418])).
% 63.23/63.24 cnf(1309,plain,
% 63.23/63.24 (~E(f4(a55),f4(a5))),
% 63.23/63.24 inference(scs_inference,[],[1256,569,606,1140,1271,51,43,45,1258,332,196,106,310,426,4,429,421,27,423,418,437,22])).
% 63.23/63.24 cnf(1311,plain,
% 63.23/63.24 (~P5(x13111,x13111)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(1312,plain,
% 63.23/63.24 (~E(f4(a1),f4(a44))),
% 63.23/63.24 inference(scs_inference,[],[1256,569,606,1140,1271,442,51,43,45,1258,332,196,106,310,426,4,429,421,27,423,418,437,22,24,21])).
% 63.23/63.24 cnf(1313,plain,
% 63.23/63.24 (~E(a202,a2)),
% 63.23/63.24 inference(scs_inference,[],[1256,569,606,1140,1271,442,1311,51,43,45,1258,332,196,106,310,426,4,429,421,27,423,418,437,22,24,21,23])).
% 63.23/63.24 cnf(1340,plain,
% 63.23/63.24 (~P10(a207,a99,a2)),
% 63.23/63.24 inference(scs_inference,[],[1298,569,1184,1312,426,4,429])).
% 63.23/63.24 cnf(1342,plain,
% 63.23/63.24 (~P8(f4(a88),f4(a77))),
% 63.23/63.24 inference(scs_inference,[],[1298,569,1184,1312,48,566,426,4,429,421])).
% 63.23/63.24 cnf(1349,plain,
% 63.23/63.24 (P5(a204,a2)),
% 63.23/63.24 inference(scs_inference,[],[1298,569,643,1184,1312,51,48,333,198,108,566,319,426,4,429,421,423,27,437,418])).
% 63.23/63.24 cnf(1351,plain,
% 63.23/63.24 (~E(f4(a55),f4(a1))),
% 63.23/63.24 inference(scs_inference,[],[1298,569,643,1184,1312,51,48,45,1300,333,198,108,566,319,426,4,429,421,423,27,437,418,22])).
% 63.23/63.24 cnf(1353,plain,
% 63.23/63.24 (~P5(x13531,x13531)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(1354,plain,
% 63.23/63.24 (~E(a204,a2)),
% 63.23/63.24 inference(scs_inference,[],[1298,569,643,1184,1312,442,1353,51,48,45,1300,333,198,108,566,319,426,4,429,421,423,27,437,418,22,24,23])).
% 63.23/63.24 cnf(1356,plain,
% 63.23/63.24 (~E(f4(a2),f4(a44))),
% 63.23/63.24 inference(scs_inference,[],[1298,569,643,1184,1312,442,1353,51,42,48,45,1300,333,198,108,566,319,426,4,429,421,423,27,437,418,22,24,23,21])).
% 63.23/63.24 cnf(1375,plain,
% 63.23/63.24 (~P10(a185,a77,a2)),
% 63.23/63.24 inference(scs_inference,[],[1340,540,1280,1356,426,4,429])).
% 63.23/63.24 cnf(1377,plain,
% 63.23/63.24 (~P8(f4(a88),f4(a66))),
% 63.23/63.24 inference(scs_inference,[],[1340,540,1280,1356,47,1342,426,4,429,421])).
% 63.23/63.24 cnf(1383,plain,
% 63.23/63.24 (P5(a206,a2)),
% 63.23/63.24 inference(scs_inference,[],[1340,540,1280,1356,51,47,1342,334,200,110,328,426,4,429,421,423,437,418])).
% 63.23/63.24 cnf(1386,plain,
% 63.23/63.24 (~E(a206,a2)),
% 63.23/63.24 inference(scs_inference,[],[1340,540,1280,1356,442,51,49,47,1342,334,200,110,328,426,4,429,421,423,437,418,22,23])).
% 63.23/63.24 cnf(1387,plain,
% 63.23/63.24 (~P5(x13871,x13871)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(1390,plain,
% 63.23/63.24 (~E(f4(a66),f4(a88))),
% 63.23/63.24 inference(scs_inference,[],[1340,540,1280,1356,442,1387,51,49,47,1342,334,200,110,328,426,4,429,421,423,437,418,22,23,24,21])).
% 63.23/63.24 cnf(1416,plain,
% 63.23/63.24 (~E(a66,a88)),
% 63.23/63.24 inference(scs_inference,[],[1375,1390,426,4])).
% 63.23/63.24 cnf(1417,plain,
% 63.23/63.24 (~P10(a185,a5,a2)),
% 63.23/63.24 inference(scs_inference,[],[1375,540,913,1390,426,4,429])).
% 63.23/63.24 cnf(1419,plain,
% 63.23/63.24 (~P8(f4(a88),f4(a55))),
% 63.23/63.24 inference(scs_inference,[],[1375,540,913,1390,46,1377,426,4,429,421])).
% 63.23/63.24 cnf(1427,plain,
% 63.23/63.24 (~E(f4(a99),f4(a66))),
% 63.23/63.24 inference(scs_inference,[],[1375,540,913,1390,51,49,46,1377,335,202,112,310,426,4,429,421,423,418,437,22])).
% 63.23/63.24 cnf(1428,plain,
% 63.23/63.24 (~E(f4(a55),f4(a88))),
% 63.23/63.24 inference(scs_inference,[],[1375,540,913,1390,51,49,46,1377,335,202,112,310,426,4,429,421,423,418,437,22,21])).
% 63.23/63.24 cnf(1429,plain,
% 63.23/63.24 (~E(a209,a2)),
% 63.23/63.24 inference(scs_inference,[],[1375,540,913,1390,442,51,49,46,1377,335,202,112,310,426,4,429,421,423,418,437,22,21,23])).
% 63.23/63.24 cnf(1430,plain,
% 63.23/63.24 (~P5(x14301,x14301)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(1432,plain,
% 63.23/63.24 (~P5(x14321,x14321)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(1434,plain,
% 63.23/63.24 (~P5(x14341,x14341)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(1441,plain,
% 63.23/63.24 (~E(a134,a185)),
% 63.23/63.24 inference(scs_inference,[],[1375,540,913,1390,442,1430,1432,1434,51,49,46,1377,335,202,203,114,112,310,426,4,429,421,423,418,437,22,21,23,24,419,420,431,577])).
% 63.23/63.24 cnf(1458,plain,
% 63.23/63.24 (~E(a55,a88)),
% 63.23/63.24 inference(scs_inference,[],[1417,1428,426,4])).
% 63.23/63.24 cnf(1459,plain,
% 63.23/63.24 (~P10(a218,a66,a2)),
% 63.23/63.24 inference(scs_inference,[],[1417,606,1428,1416,426,4,429])).
% 63.23/63.24 cnf(1461,plain,
% 63.23/63.24 (~P8(f4(a88),f4(a44))),
% 63.23/63.24 inference(scs_inference,[],[1417,606,1428,1416,45,1419,426,4,429,421])).
% 63.23/63.24 cnf(1469,plain,
% 63.23/63.24 (~E(f4(a99),f4(a55))),
% 63.23/63.24 inference(scs_inference,[],[1417,606,1428,1416,51,49,45,1419,338,204,114,426,4,429,421,423,437,418,22])).
% 63.23/63.24 cnf(1471,plain,
% 63.23/63.24 (~P5(x14711,x14711)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(1472,plain,
% 63.23/63.24 (~E(f4(a44),f4(a88))),
% 63.23/63.24 inference(scs_inference,[],[1417,606,1428,1416,442,51,49,45,1419,338,204,114,426,4,429,421,423,437,418,22,24,21])).
% 63.23/63.24 cnf(1473,plain,
% 63.23/63.24 (~E(a211,a2)),
% 63.23/63.24 inference(scs_inference,[],[1417,606,1428,1416,442,1471,51,49,45,1419,338,204,114,426,4,429,421,423,437,418,22,24,21,23])).
% 63.23/63.24 cnf(1499,plain,
% 63.23/63.24 (~E(a44,a88)),
% 63.23/63.24 inference(scs_inference,[],[1459,1472,426,4])).
% 63.23/63.24 cnf(1500,plain,
% 63.23/63.24 (~P10(a218,a55,a2)),
% 63.23/63.24 inference(scs_inference,[],[1459,606,1472,1458,426,4,429])).
% 63.23/63.24 cnf(1502,plain,
% 63.23/63.24 (~P8(f4(a88),f4(a5))),
% 63.23/63.24 inference(scs_inference,[],[1459,606,1472,1458,44,1461,426,4,429,421])).
% 63.23/63.24 cnf(1510,plain,
% 63.23/63.24 (~E(f4(a99),f4(a44))),
% 63.23/63.24 inference(scs_inference,[],[1459,606,1472,1458,51,44,49,1461,339,206,329,116,426,4,429,421,423,418,437,22])).
% 63.23/63.24 cnf(1511,plain,
% 63.23/63.24 (~E(a213,a2)),
% 63.23/63.24 inference(scs_inference,[],[1459,606,1472,1458,442,51,44,49,1461,339,206,329,116,426,4,429,421,423,418,437,22,23])).
% 63.23/63.24 cnf(1512,plain,
% 63.23/63.24 (~P5(x15121,x15121)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(1515,plain,
% 63.23/63.24 (~E(f4(a5),f4(a88))),
% 63.23/63.24 inference(scs_inference,[],[1459,606,1472,1458,442,1512,51,44,49,1461,339,206,329,116,426,4,429,421,423,418,437,22,23,24,21])).
% 63.23/63.24 cnf(1540,plain,
% 63.23/63.24 (~E(a5,a88)),
% 63.23/63.24 inference(scs_inference,[],[1500,1515,426,4])).
% 63.23/63.24 cnf(1541,plain,
% 63.23/63.24 (~P10(a218,a44,a2)),
% 63.23/63.24 inference(scs_inference,[],[1500,606,1515,1499,426,4,429])).
% 63.23/63.24 cnf(1543,plain,
% 63.23/63.24 (~P8(f4(a88),f4(a1))),
% 63.23/63.24 inference(scs_inference,[],[1500,606,1515,1499,43,1502,426,4,429,421])).
% 63.23/63.24 cnf(1551,plain,
% 63.23/63.24 (~E(f4(a99),f4(a5))),
% 63.23/63.24 inference(scs_inference,[],[1500,606,1515,1499,51,43,49,1502,340,208,338,118,426,4,429,421,423,437,418,22])).
% 63.23/63.24 cnf(1552,plain,
% 63.23/63.24 (~E(f4(a1),f4(a88))),
% 63.23/63.24 inference(scs_inference,[],[1500,606,1515,1499,51,43,49,1502,340,208,338,118,426,4,429,421,423,437,418,22,21])).
% 63.23/63.24 cnf(1553,plain,
% 63.23/63.24 (~E(a215,a2)),
% 63.23/63.24 inference(scs_inference,[],[1500,606,1515,1499,442,51,43,49,1502,340,208,338,118,426,4,429,421,423,437,418,22,21,23])).
% 63.23/63.24 cnf(1581,plain,
% 63.23/63.24 (~E(a1,a88)),
% 63.23/63.24 inference(scs_inference,[],[1541,1552,426,4])).
% 63.23/63.24 cnf(1582,plain,
% 63.23/63.24 (~P10(a218,a5,a2)),
% 63.23/63.24 inference(scs_inference,[],[1541,606,1552,1540,426,4,429])).
% 63.23/63.24 cnf(1584,plain,
% 63.23/63.24 (~P8(f4(a55),f4(a5))),
% 63.23/63.24 inference(scs_inference,[],[1541,606,1552,1540,44,549,426,4,429,421])).
% 63.23/63.24 cnf(1592,plain,
% 63.23/63.24 (~E(f4(a99),f4(a1))),
% 63.23/63.24 inference(scs_inference,[],[1541,606,1552,1540,51,44,49,1543,341,210,120,311,549,426,4,429,421,423,418,437,22])).
% 63.23/63.24 cnf(1594,plain,
% 63.23/63.24 (~P5(x15941,x15941)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(1595,plain,
% 63.23/63.24 (~E(f4(a2),f4(a88))),
% 63.23/63.24 inference(scs_inference,[],[1541,606,1552,1540,442,51,42,44,49,1543,341,210,120,311,549,426,4,429,421,423,418,437,22,24,21])).
% 63.23/63.24 cnf(1596,plain,
% 63.23/63.24 (~E(a217,a2)),
% 63.23/63.24 inference(scs_inference,[],[1541,606,1552,1540,442,1594,51,42,44,49,1543,341,210,120,311,549,426,4,429,421,423,418,437,22,24,21,23])).
% 63.23/63.24 cnf(1597,plain,
% 63.23/63.24 (~P5(x15971,x15971)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(1599,plain,
% 63.23/63.24 (~P5(x15991,x15991)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(1606,plain,
% 63.23/63.24 (~E(a134,a218)),
% 63.23/63.24 inference(scs_inference,[],[1541,606,1552,1540,442,1594,1597,1599,51,42,44,49,1543,341,210,211,122,120,311,549,426,4,429,421,423,418,437,22,24,21,23,419,420,431,577])).
% 63.23/63.24 cnf(1614,plain,
% 63.23/63.24 (P7(f251(f4(x16141),f4(a1)))),
% 63.23/63.24 inference(scs_inference,[],[33,411,416])).
% 63.23/63.24 cnf(1617,plain,
% 63.23/63.24 (~E(a2,a88)),
% 63.23/63.24 inference(scs_inference,[],[1582,1595,426,4])).
% 63.23/63.24 cnf(1618,plain,
% 63.23/63.24 (~P10(a218,a1,a2)),
% 63.23/63.24 inference(scs_inference,[],[1582,606,1595,1581,426,4,429])).
% 63.23/63.24 cnf(1620,plain,
% 63.23/63.24 (~P8(f4(a55),f4(a1))),
% 63.23/63.24 inference(scs_inference,[],[1582,606,1595,1581,43,1584,426,4,429,421])).
% 63.23/63.24 cnf(1622,plain,
% 63.23/63.24 (~E(a122,a218)),
% 63.23/63.24 inference(scs_inference,[],[1582,449,606,1595,1581,43,1584,426,4,429,421,27])).
% 63.23/63.24 cnf(1629,plain,
% 63.23/63.24 (~E(f4(a66),f4(a5))),
% 63.23/63.24 inference(scs_inference,[],[1582,449,606,1595,1581,51,43,46,1584,342,212,122,320,426,4,429,421,27,423,437,418,22])).
% 63.23/63.24 cnf(1630,plain,
% 63.23/63.24 (~E(a220,a2)),
% 63.23/63.24 inference(scs_inference,[],[1582,449,606,1595,1581,442,51,43,46,1584,342,212,122,320,426,4,429,421,27,423,437,418,22,23])).
% 63.23/63.24 cnf(1631,plain,
% 63.23/63.24 (~P5(x16311,x16311)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(1634,plain,
% 63.23/63.24 (~E(f4(a1),f4(a55))),
% 63.23/63.24 inference(scs_inference,[],[1582,449,606,1595,1581,442,1631,51,43,46,1584,342,212,122,320,426,4,429,421,27,423,437,418,22,23,24,21])).
% 63.23/63.24 cnf(1652,plain,
% 63.23/63.24 (~E(a1,a55)),
% 63.23/63.24 inference(scs_inference,[],[1618,1634,426,4])).
% 63.23/63.24 cnf(1653,plain,
% 63.23/63.24 (~P10(a218,a2,a2)),
% 63.23/63.24 inference(scs_inference,[],[1618,606,1634,1617,426,4,429])).
% 63.23/63.24 cnf(1655,plain,
% 63.23/63.24 (~P8(f4(a66),f4(a44))),
% 63.23/63.24 inference(scs_inference,[],[1618,606,1634,1617,45,590,426,4,429,421])).
% 63.23/63.24 cnf(1663,plain,
% 63.23/63.24 (~E(f4(a66),f4(a1))),
% 63.23/63.24 inference(scs_inference,[],[1618,606,1634,1617,51,45,46,1620,343,214,124,590,329,426,4,429,421,423,437,418,22])).
% 63.23/63.24 cnf(1665,plain,
% 63.23/63.24 (~P5(x16651,x16651)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(1666,plain,
% 63.23/63.24 (~E(a222,a2)),
% 63.23/63.24 inference(scs_inference,[],[1618,606,1634,1617,442,1665,51,45,46,1620,343,214,124,590,329,426,4,429,421,423,437,418,22,24,23])).
% 63.23/63.24 cnf(1668,plain,
% 63.23/63.24 (~E(f4(a2),f4(a55))),
% 63.23/63.24 inference(scs_inference,[],[1618,606,1634,1617,442,1665,51,42,45,46,1620,343,214,124,590,329,426,4,429,421,423,437,418,22,24,23,21])).
% 63.23/63.24 cnf(1693,plain,
% 63.23/63.24 (~E(a2,a55)),
% 63.23/63.24 inference(scs_inference,[],[1653,1668,426,4])).
% 63.23/63.24 cnf(1694,plain,
% 63.23/63.24 (~P10(a185,a1,a2)),
% 63.23/63.24 inference(scs_inference,[],[1653,540,1668,1652,426,4,429])).
% 63.23/63.24 cnf(1696,plain,
% 63.23/63.24 (~P8(f4(a66),f4(a5))),
% 63.23/63.24 inference(scs_inference,[],[1653,540,1668,1652,44,1655,426,4,429,421])).
% 63.23/63.24 cnf(1700,plain,
% 63.23/63.24 (P6(f4(a77),f4(a44),f4(a2),f4(a110))),
% 63.23/63.24 inference(scs_inference,[],[1653,540,1668,1652,44,1655,344,216,126,338,426,4,429,421,423,437])).
% 63.23/63.24 cnf(1702,plain,
% 63.23/63.24 (P5(a224,a2)),
% 63.23/63.24 inference(scs_inference,[],[1653,540,1668,1652,51,44,1655,344,216,126,338,426,4,429,421,423,437,418])).
% 63.23/63.24 cnf(1706,plain,
% 63.23/63.24 (~P5(x17061,x17061)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(1707,plain,
% 63.23/63.24 (~E(f4(a5),f4(a66))),
% 63.23/63.24 inference(scs_inference,[],[1653,540,1668,1652,442,51,47,44,1655,344,216,126,338,426,4,429,421,423,437,418,22,24,21])).
% 63.23/63.24 cnf(1708,plain,
% 63.23/63.24 (~E(a224,a2)),
% 63.23/63.24 inference(scs_inference,[],[1653,540,1668,1652,442,1706,51,47,44,1655,344,216,126,338,426,4,429,421,423,437,418,22,24,21,23])).
% 63.23/63.24 cnf(1709,plain,
% 63.23/63.24 (~P5(x17091,x17091)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(1711,plain,
% 63.23/63.24 (~P5(x17111,x17111)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(1718,plain,
% 63.23/63.24 (~E(a122,a185)),
% 63.23/63.24 inference(scs_inference,[],[1653,540,1668,1652,442,1706,1709,1711,51,47,44,1655,344,216,217,128,126,338,426,4,429,421,423,437,418,22,24,21,23,419,420,431,544])).
% 63.23/63.24 cnf(1729,plain,
% 63.23/63.24 (~P10(a185,a2,a2)),
% 63.23/63.24 inference(scs_inference,[],[1694,540,1707,1693,426,4,429])).
% 63.23/63.24 cnf(1731,plain,
% 63.23/63.24 (~P8(f4(a66),f4(a1))),
% 63.23/63.24 inference(scs_inference,[],[1694,540,1707,1693,43,1696,426,4,429,421])).
% 63.23/63.24 cnf(1737,plain,
% 63.23/63.24 (P6(f4(a2),f4(a55),f4(a2),f4(a55))),
% 63.23/63.24 inference(scs_inference,[],[1694,540,1707,1693,51,43,1696,348,218,128,426,4,429,421,423,418,437])).
% 63.23/63.24 cnf(1740,plain,
% 63.23/63.24 (~E(a226,a2)),
% 63.23/63.24 inference(scs_inference,[],[1694,540,1707,1693,442,51,47,43,1696,348,218,128,426,4,429,421,423,418,437,22,23])).
% 63.23/63.24 cnf(1741,plain,
% 63.23/63.24 (~P5(x17411,x17411)),
% 63.23/63.24 inference(rename_variables,[],[442])).
% 63.23/63.24 cnf(1744,plain,
% 63.23/63.24 (~E(f4(a1),f4(a66))),
% 63.23/63.24 inference(scs_inference,[],[1694,540,1707,1693,442,1741,51,47,43,1696,348,218,128,426,4,429,421,423,418,437,22,23,24,21])).
% 63.23/63.24 cnf(1770,plain,
% 63.23/63.24 (~P10(a229,a88,a2)),
% 63.23/63.24 inference(scs_inference,[],[1729,643,876,1744,426,4,429])).
% 63.23/63.24 cnf(1772,plain,
% 63.23/63.24 (~P8(f4(a77),f4(a55))),
% 63.23/63.24 inference(scs_inference,[],[1729,643,876,1744,46,623,426,4,429,421])).
% 63.23/63.24 cnf(1781,plain,
% 63.23/63.24 (~E(a228,a2)),
% 63.23/63.24 inference(scs_inference,[],[1729,643,876,1744,442,51,47,46,1731,349,220,339,130,623,426,4,429,421,423,437,418,22,23])).
% 63.23/63.24 cnf(1783,plain,
% 63.23/63.24 (~E(f4(a2),f4(a66))),
% 63.23/63.24 inference(scs_inference,[],[1729,643,876,1744,442,51,42,47,46,1731,349,220,339,130,623,426,4,429,421,423,437,418,22,23,21])).
% 63.23/63.24 cnf(1803,plain,
% 63.23/63.24 (~E(a2,a66)),
% 63.23/63.24 inference(scs_inference,[],[1770,1783,426,4])).
% 63.23/63.24 cnf(1804,plain,
% 63.23/63.24 (~P10(a2,a1,a2)),
% 63.23/63.24 inference(scs_inference,[],[1770,482,1783,457,426,4,429])).
% 63.23/63.24 cnf(1806,plain,
% 63.23/63.24 (~P8(f4(a77),f4(a44))),
% 63.23/63.24 inference(scs_inference,[],[1770,482,1783,457,45,1772,426,4,429,421])).
% 63.23/63.24 cnf(1810,plain,
% 63.23/63.24 (P5(a231,a2)),
% 63.23/63.24 inference(scs_inference,[],[1770,482,1783,51,457,45,1772,222,132,426,4,429,421,423,418])).
% 63.23/63.25 cnf(1812,plain,
% 63.23/63.25 (P6(f4(a5),f4(a55),f4(a2),f4(a77))),
% 63.23/63.25 inference(scs_inference,[],[1770,482,1783,51,457,45,1772,350,222,348,132,426,4,429,421,423,418,437])).
% 63.23/63.25 cnf(1814,plain,
% 63.23/63.25 (~E(f4(a88),f4(a55))),
% 63.23/63.25 inference(scs_inference,[],[1770,482,1783,51,457,48,45,1772,350,222,348,132,426,4,429,421,423,418,437,22])).
% 63.23/63.25 cnf(1816,plain,
% 63.23/63.25 (~P5(x18161,x18161)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(1817,plain,
% 63.23/63.25 (~E(a231,a2)),
% 63.23/63.25 inference(scs_inference,[],[1770,482,1783,442,1816,51,457,48,45,1772,350,222,348,132,426,4,429,421,423,418,437,22,24,23])).
% 63.23/63.25 cnf(1819,plain,
% 63.23/63.25 (~E(f4(a44),f4(a77))),
% 63.23/63.25 inference(scs_inference,[],[1770,482,1783,442,1816,51,457,48,45,1772,350,222,348,132,426,4,429,421,423,418,437,22,24,23,21])).
% 63.23/63.25 cnf(1837,plain,
% 63.23/63.25 (~E(a44,a77)),
% 63.23/63.25 inference(scs_inference,[],[1804,1819,426,4])).
% 63.23/63.25 cnf(1838,plain,
% 63.23/63.25 (~P10(a2,a185,a2)),
% 63.23/63.25 inference(scs_inference,[],[1804,532,1819,457,426,4,429])).
% 63.23/63.25 cnf(1840,plain,
% 63.23/63.25 (~P8(f4(a77),f4(a5))),
% 63.23/63.25 inference(scs_inference,[],[1804,532,1819,457,44,1806,426,4,429,421])).
% 63.23/63.25 cnf(1844,plain,
% 63.23/63.25 (~E(a55,a2)),
% 63.23/63.25 inference(scs_inference,[],[1804,532,1819,457,44,1806,526,224,134,426,4,429,421,423,27])).
% 63.23/63.25 cnf(1849,plain,
% 63.23/63.25 (~E(f4(a88),f4(a44))),
% 63.23/63.25 inference(scs_inference,[],[1804,532,1819,51,457,48,44,1806,351,526,224,134,339,426,4,429,421,423,27,437,418,22])).
% 63.23/63.25 cnf(1850,plain,
% 63.23/63.25 (~E(f4(a5),f4(a77))),
% 63.23/63.25 inference(scs_inference,[],[1804,532,1819,51,457,48,44,1806,351,526,224,134,339,426,4,429,421,423,27,437,418,22,21])).
% 63.23/63.25 cnf(1852,plain,
% 63.23/63.25 (~P5(x18521,x18521)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(1853,plain,
% 63.23/63.25 (~E(a233,a2)),
% 63.23/63.25 inference(scs_inference,[],[1804,532,1819,442,1852,51,457,48,44,1806,351,526,224,134,339,426,4,429,421,423,27,437,418,22,21,24,23])).
% 63.23/63.25 cnf(1854,plain,
% 63.23/63.25 (~P5(x18541,x18541)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(1856,plain,
% 63.23/63.25 (~P5(x18561,x18561)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(1861,plain,
% 63.23/63.25 (P10(a233,a103,a2)),
% 63.23/63.25 inference(scs_inference,[],[1804,532,1819,442,1852,1854,1856,51,457,48,44,1806,351,526,224,225,136,134,339,426,4,429,421,423,27,437,418,22,21,24,23,419,420,431])).
% 63.23/63.25 cnf(1879,plain,
% 63.23/63.25 (~E(a5,a77)),
% 63.23/63.25 inference(scs_inference,[],[1838,1850,426,4])).
% 63.23/63.25 cnf(1880,plain,
% 63.23/63.25 (~P10(a207,a44,a2)),
% 63.23/63.25 inference(scs_inference,[],[1838,569,1850,1837,426,4,429])).
% 63.23/63.25 cnf(1882,plain,
% 63.23/63.25 (~P8(f4(a77),f4(a1))),
% 63.23/63.25 inference(scs_inference,[],[1838,569,1850,1837,43,1840,426,4,429,421])).
% 63.23/63.25 cnf(1888,plain,
% 63.23/63.25 (P5(a235,a2)),
% 63.23/63.25 inference(scs_inference,[],[1838,569,1850,1837,51,43,1840,352,226,136,348,426,4,429,421,423,437,418])).
% 63.23/63.25 cnf(1890,plain,
% 63.23/63.25 (~E(f4(a88),f4(a5))),
% 63.23/63.25 inference(scs_inference,[],[1838,569,1850,1837,51,48,43,1840,352,226,136,348,426,4,429,421,423,437,418,22])).
% 63.23/63.25 cnf(1891,plain,
% 63.23/63.25 (~E(a235,a2)),
% 63.23/63.25 inference(scs_inference,[],[1838,569,1850,1837,442,51,48,43,1840,352,226,136,348,426,4,429,421,423,437,418,22,23])).
% 63.23/63.25 cnf(1893,plain,
% 63.23/63.25 (~E(f4(a1),f4(a77))),
% 63.23/63.25 inference(scs_inference,[],[1838,569,1850,1837,442,51,48,43,1840,352,226,136,348,426,4,429,421,423,437,418,22,23,21])).
% 63.23/63.25 cnf(1914,plain,
% 63.23/63.25 (~E(a1,a77)),
% 63.23/63.25 inference(scs_inference,[],[1880,1893,426,4])).
% 63.23/63.25 cnf(1915,plain,
% 63.23/63.25 (~P10(a207,a5,a2)),
% 63.23/63.25 inference(scs_inference,[],[1880,569,1893,1879,426,4,429])).
% 63.23/63.25 cnf(1917,plain,
% 63.23/63.25 (~P8(f4(a99),f4(a77))),
% 63.23/63.25 inference(scs_inference,[],[1880,569,1893,1879,48,660,426,4,429,421])).
% 63.23/63.25 cnf(1923,plain,
% 63.23/63.25 (P5(a237,a2)),
% 63.23/63.25 inference(scs_inference,[],[1880,569,1893,1879,51,48,353,228,138,660,312,426,4,429,421,423,437,418])).
% 63.23/63.25 cnf(1925,plain,
% 63.23/63.25 (~E(f4(a88),f4(a1))),
% 63.23/63.25 inference(scs_inference,[],[1880,569,1893,1879,51,48,1882,353,228,138,660,312,426,4,429,421,423,437,418,22])).
% 63.23/63.25 cnf(1926,plain,
% 63.23/63.25 (~E(a237,a2)),
% 63.23/63.25 inference(scs_inference,[],[1880,569,1893,1879,442,51,48,1882,353,228,138,660,312,426,4,429,421,423,437,418,22,23])).
% 63.23/63.25 cnf(1927,plain,
% 63.23/63.25 (~P5(x19271,x19271)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(1928,plain,
% 63.23/63.25 (~E(f4(a2),f4(a77))),
% 63.23/63.25 inference(scs_inference,[],[1880,569,1893,1879,442,51,42,48,1882,353,228,138,660,312,426,4,429,421,423,437,418,22,23,21])).
% 63.23/63.25 cnf(1930,plain,
% 63.23/63.25 (~P5(x19301,x19301)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(1932,plain,
% 63.23/63.25 (~P5(x19321,x19321)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(1934,plain,
% 63.23/63.25 (P10(a237,a107,a2)),
% 63.23/63.25 inference(scs_inference,[],[1880,569,1893,1879,442,1927,1930,51,42,48,1882,353,228,229,138,660,312,426,4,429,421,423,437,418,22,23,21,24,419,431])).
% 63.23/63.25 cnf(1939,plain,
% 63.23/63.25 (~E(a134,a207)),
% 63.23/63.25 inference(scs_inference,[],[1880,569,1893,1879,442,1927,1930,1932,51,42,48,1882,353,228,229,140,138,660,312,426,4,429,421,423,437,418,22,23,21,24,419,431,420,577])).
% 63.23/63.25 cnf(1957,plain,
% 63.23/63.25 (~E(a2,a77)),
% 63.23/63.25 inference(scs_inference,[],[1915,1928,426,4])).
% 63.23/63.25 cnf(1958,plain,
% 63.23/63.25 (~P10(a207,a1,a2)),
% 63.23/63.25 inference(scs_inference,[],[1915,569,1928,1914,426,4,429])).
% 63.23/63.25 cnf(1960,plain,
% 63.23/63.25 (~P8(f4(a99),f4(a66))),
% 63.23/63.25 inference(scs_inference,[],[1915,569,1928,1914,47,1917,426,4,429,421])).
% 63.23/63.25 cnf(1966,plain,
% 63.23/63.25 (P5(a239,a2)),
% 63.23/63.25 inference(scs_inference,[],[1915,569,1928,1914,51,47,1917,358,230,140,426,4,429,421,423,437,418])).
% 63.23/63.25 cnf(1968,plain,
% 63.23/63.25 (~E(f4(a110),f4(a77))),
% 63.23/63.25 inference(scs_inference,[],[1915,569,1928,1914,51,50,47,1917,358,230,140,426,4,429,421,423,437,418,22])).
% 63.23/63.25 cnf(1969,plain,
% 63.23/63.25 (~E(f4(a66),f4(a99))),
% 63.23/63.25 inference(scs_inference,[],[1915,569,1928,1914,51,50,47,1917,358,230,140,426,4,429,421,423,437,418,22,21])).
% 63.23/63.25 cnf(1970,plain,
% 63.23/63.25 (~E(a239,a2)),
% 63.23/63.25 inference(scs_inference,[],[1915,569,1928,1914,442,51,50,47,1917,358,230,140,426,4,429,421,423,437,418,22,21,23])).
% 63.23/63.25 cnf(1971,plain,
% 63.23/63.25 (~P5(x19711,x19711)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(1973,plain,
% 63.23/63.25 (~P5(x19731,x19731)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(1975,plain,
% 63.23/63.25 (~P5(x19751,x19751)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(1982,plain,
% 63.23/63.25 (~E(a122,a207)),
% 63.23/63.25 inference(scs_inference,[],[1915,569,1928,1914,442,1971,1973,1975,51,50,47,1917,358,230,231,142,140,426,4,429,421,423,437,418,22,21,23,24,419,420,431,544])).
% 63.23/63.25 cnf(1983,plain,
% 63.23/63.25 (~E(a77,a1)),
% 63.23/63.25 inference(scs_inference,[],[1915,569,1928,1914,442,1971,1973,1975,51,50,47,1917,358,230,231,142,140,426,4,429,421,423,437,418,22,21,23,24,419,420,431,544,685])).
% 63.23/63.25 cnf(2000,plain,
% 63.23/63.25 (~E(a66,a99)),
% 63.23/63.25 inference(scs_inference,[],[1958,1969,426,4])).
% 63.23/63.25 cnf(2001,plain,
% 63.23/63.25 (~P10(a122,a77,a2)),
% 63.23/63.25 inference(scs_inference,[],[1958,449,1969,1983,426,4,429])).
% 63.23/63.25 cnf(2003,plain,
% 63.23/63.25 (~P8(f4(a99),f4(a55))),
% 63.23/63.25 inference(scs_inference,[],[1958,449,1969,1983,46,1960,426,4,429,421])).
% 63.23/63.25 cnf(2007,plain,
% 63.23/63.25 (P6(f4(a1),f4(a1),f4(a55),f4(a77))),
% 63.23/63.25 inference(scs_inference,[],[1958,449,1969,1983,46,1960,359,232,322,142,426,4,429,421,423,437])).
% 63.23/63.25 cnf(2009,plain,
% 63.23/63.25 (P5(a242,a2)),
% 63.23/63.25 inference(scs_inference,[],[1958,449,1969,1983,51,46,1960,359,232,322,142,426,4,429,421,423,437,418])).
% 63.23/63.25 cnf(2011,plain,
% 63.23/63.25 (~E(f4(a110),f4(a66))),
% 63.23/63.25 inference(scs_inference,[],[1958,449,1969,1983,51,50,46,1960,359,232,322,142,426,4,429,421,423,437,418,22])).
% 63.23/63.25 cnf(2012,plain,
% 63.23/63.25 (~E(a242,a2)),
% 63.23/63.25 inference(scs_inference,[],[1958,449,1969,1983,442,51,50,46,1960,359,232,322,142,426,4,429,421,423,437,418,22,23])).
% 63.23/63.25 cnf(2013,plain,
% 63.23/63.25 (~P5(x20131,x20131)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2014,plain,
% 63.23/63.25 (~E(f4(a55),f4(a99))),
% 63.23/63.25 inference(scs_inference,[],[1958,449,1969,1983,442,51,50,46,1960,359,232,322,142,426,4,429,421,423,437,418,22,23,21])).
% 63.23/63.25 cnf(2016,plain,
% 63.23/63.25 (~P5(x20161,x20161)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2018,plain,
% 63.23/63.25 (~P5(x20181,x20181)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2020,plain,
% 63.23/63.25 (P10(a242,a112,a2)),
% 63.23/63.25 inference(scs_inference,[],[1958,449,1969,1983,442,2013,2016,51,50,46,1960,359,232,233,322,142,426,4,429,421,423,437,418,22,23,21,24,419,431])).
% 63.23/63.25 cnf(2025,plain,
% 63.23/63.25 (~E(a207,a122)),
% 63.23/63.25 inference(scs_inference,[],[1958,449,1969,1983,442,2013,2016,2018,51,50,46,1960,359,232,233,144,322,142,426,4,429,421,423,437,418,22,23,21,24,419,431,420,687])).
% 63.23/63.25 cnf(2035,plain,
% 63.23/63.25 (~E(a55,a99)),
% 63.23/63.25 inference(scs_inference,[],[2001,2014,426,4])).
% 63.23/63.25 cnf(2036,plain,
% 63.23/63.25 (~P10(a207,a2,a2)),
% 63.23/63.25 inference(scs_inference,[],[2001,569,2014,1957,426,4,429])).
% 63.23/63.25 cnf(2038,plain,
% 63.23/63.25 (~P8(f4(a99),f4(a44))),
% 63.23/63.25 inference(scs_inference,[],[2001,569,2014,1957,45,2003,426,4,429,421])).
% 63.23/63.25 cnf(2044,plain,
% 63.23/63.25 (P5(a244,a2)),
% 63.23/63.25 inference(scs_inference,[],[2001,569,2014,1957,51,45,2003,360,234,349,144,426,4,429,421,423,437,418])).
% 63.23/63.25 cnf(2046,plain,
% 63.23/63.25 (~E(f4(a110),f4(a55))),
% 63.23/63.25 inference(scs_inference,[],[2001,569,2014,1957,51,50,45,2003,360,234,349,144,426,4,429,421,423,437,418,22])).
% 63.23/63.25 cnf(2047,plain,
% 63.23/63.25 (~E(f4(a44),f4(a99))),
% 63.23/63.25 inference(scs_inference,[],[2001,569,2014,1957,51,50,45,2003,360,234,349,144,426,4,429,421,423,437,418,22,21])).
% 63.23/63.25 cnf(2048,plain,
% 63.23/63.25 (~E(a244,a2)),
% 63.23/63.25 inference(scs_inference,[],[2001,569,2014,1957,442,51,50,45,2003,360,234,349,144,426,4,429,421,423,437,418,22,21,23])).
% 63.23/63.25 cnf(2049,plain,
% 63.23/63.25 (~P5(x20491,x20491)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2051,plain,
% 63.23/63.25 (~P5(x20511,x20511)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2053,plain,
% 63.23/63.25 (~P5(x20531,x20531)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2060,plain,
% 63.23/63.25 (~E(a77,a2)),
% 63.23/63.25 inference(scs_inference,[],[2001,569,2014,1957,442,2049,2051,2053,51,50,45,2003,360,234,235,146,349,144,426,4,429,421,423,437,418,22,21,23,24,419,420,431,685])).
% 63.23/63.25 cnf(2077,plain,
% 63.23/63.25 (~E(a44,a99)),
% 63.23/63.25 inference(scs_inference,[],[2036,2047,426,4])).
% 63.23/63.25 cnf(2078,plain,
% 63.23/63.25 (~P10(a229,a66,a2)),
% 63.23/63.25 inference(scs_inference,[],[2036,643,2047,2000,426,4,429])).
% 63.23/63.25 cnf(2080,plain,
% 63.23/63.25 (~P8(f4(a99),f4(a5))),
% 63.23/63.25 inference(scs_inference,[],[2036,643,2047,2000,44,2038,426,4,429,421])).
% 63.23/63.25 cnf(2086,plain,
% 63.23/63.25 (P5(a246,a2)),
% 63.23/63.25 inference(scs_inference,[],[2036,643,2047,2000,51,44,2038,361,236,358,146,426,4,429,421,423,437,418])).
% 63.23/63.25 cnf(2088,plain,
% 63.23/63.25 (~E(f4(a110),f4(a44))),
% 63.23/63.25 inference(scs_inference,[],[2036,643,2047,2000,51,50,44,2038,361,236,358,146,426,4,429,421,423,437,418,22])).
% 63.23/63.25 cnf(2089,plain,
% 63.23/63.25 (~E(f4(a5),f4(a99))),
% 63.23/63.25 inference(scs_inference,[],[2036,643,2047,2000,51,50,44,2038,361,236,358,146,426,4,429,421,423,437,418,22,21])).
% 63.23/63.25 cnf(2090,plain,
% 63.23/63.25 (~E(a246,a2)),
% 63.23/63.25 inference(scs_inference,[],[2036,643,2047,2000,442,51,50,44,2038,361,236,358,146,426,4,429,421,423,437,418,22,21,23])).
% 63.23/63.25 cnf(2118,plain,
% 63.23/63.25 (~E(a5,a99)),
% 63.23/63.25 inference(scs_inference,[],[2078,2089,426,4])).
% 63.23/63.25 cnf(2119,plain,
% 63.23/63.25 (~P10(a229,a55,a2)),
% 63.23/63.25 inference(scs_inference,[],[2078,643,2089,2035,426,4,429])).
% 63.23/63.25 cnf(2121,plain,
% 63.23/63.25 (~P8(f4(a99),f4(a1))),
% 63.23/63.25 inference(scs_inference,[],[2078,643,2089,2035,43,2080,426,4,429,421])).
% 63.23/63.25 cnf(2127,plain,
% 63.23/63.25 (P5(a248,a2)),
% 63.23/63.25 inference(scs_inference,[],[2078,643,2089,2035,51,43,2080,362,238,148,331,426,4,429,421,423,437,418])).
% 63.23/63.25 cnf(2129,plain,
% 63.23/63.25 (~E(f4(a110),f4(a5))),
% 63.23/63.25 inference(scs_inference,[],[2078,643,2089,2035,51,50,43,2080,362,238,148,331,426,4,429,421,423,437,418,22])).
% 63.23/63.25 cnf(2130,plain,
% 63.23/63.25 (~E(f4(a1),f4(a99))),
% 63.23/63.25 inference(scs_inference,[],[2078,643,2089,2035,51,50,43,2080,362,238,148,331,426,4,429,421,423,437,418,22,21])).
% 63.23/63.25 cnf(2131,plain,
% 63.23/63.25 (~E(a248,a2)),
% 63.23/63.25 inference(scs_inference,[],[2078,643,2089,2035,442,51,50,43,2080,362,238,148,331,426,4,429,421,423,437,418,22,21,23])).
% 63.23/63.25 cnf(2132,plain,
% 63.23/63.25 (~P5(x21321,x21321)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2134,plain,
% 63.23/63.25 (~P5(x21341,x21341)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2135,plain,
% 63.23/63.25 (~P8(f251(f4(a99),f4(a99)),f251(f4(a99),f4(a99)))),
% 63.23/63.25 inference(scs_inference,[],[2078,643,2089,2035,442,2132,2134,51,50,43,2080,362,238,239,148,331,426,4,429,421,423,437,418,22,21,23,24,419])).
% 63.23/63.25 cnf(2152,plain,
% 63.23/63.25 (~E(a1,a99)),
% 63.23/63.25 inference(scs_inference,[],[2119,2130,426,4])).
% 63.23/63.25 cnf(2153,plain,
% 63.23/63.25 (~P10(a229,a44,a2)),
% 63.23/63.25 inference(scs_inference,[],[2119,643,2130,2077,426,4,429])).
% 63.23/63.25 cnf(2159,plain,
% 63.23/63.25 (P5(a250,a2)),
% 63.23/63.25 inference(scs_inference,[],[2119,643,2130,2077,51,368,240,150,426,4,429,423,437,418])).
% 63.23/63.25 cnf(2161,plain,
% 63.23/63.25 (~E(f4(a110),f4(a1))),
% 63.23/63.25 inference(scs_inference,[],[2119,643,2130,2077,51,50,2121,368,240,150,426,4,429,423,437,418,22])).
% 63.23/63.25 cnf(2162,plain,
% 63.23/63.25 (~E(f4(a2),f4(a99))),
% 63.23/63.25 inference(scs_inference,[],[2119,643,2130,2077,51,42,50,2121,368,240,150,426,4,429,423,437,418,22,21])).
% 63.23/63.25 cnf(2163,plain,
% 63.23/63.25 (~E(a250,a2)),
% 63.23/63.25 inference(scs_inference,[],[2119,643,2130,2077,442,51,42,50,2121,368,240,150,426,4,429,423,437,418,22,21,23])).
% 63.23/63.25 cnf(2192,plain,
% 63.23/63.25 (~E(a2,a99)),
% 63.23/63.25 inference(scs_inference,[],[2153,2162,426,4])).
% 63.23/63.25 cnf(2193,plain,
% 63.23/63.25 (~P10(a229,a5,a2)),
% 63.23/63.25 inference(scs_inference,[],[2153,643,2162,2118,426,4,429])).
% 63.23/63.25 cnf(2199,plain,
% 63.23/63.25 (P5(a253,a2)),
% 63.23/63.25 inference(scs_inference,[],[2153,643,2162,2118,51,369,242,341,152,426,4,429,423,437,418])).
% 63.23/63.25 cnf(2201,plain,
% 63.23/63.25 (~E(a253,a2)),
% 63.23/63.25 inference(scs_inference,[],[2153,643,2162,2118,442,51,369,242,341,152,426,4,429,423,437,418,23])).
% 63.23/63.25 cnf(2202,plain,
% 63.23/63.25 (~P5(x22021,x22021)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2204,plain,
% 63.23/63.25 (~P5(x22041,x22041)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2206,plain,
% 63.23/63.25 (~P5(x22061,x22061)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2213,plain,
% 63.23/63.25 (~E(a134,a229)),
% 63.23/63.25 inference(scs_inference,[],[2153,643,2162,2118,442,2202,2204,2206,51,369,242,243,154,341,152,426,4,429,423,437,418,23,24,419,420,431,577])).
% 63.23/63.25 cnf(2230,plain,
% 63.23/63.25 (~E(a110,a88)),
% 63.23/63.25 inference(scs_inference,[],[2193,705,426,4])).
% 63.23/63.25 cnf(2231,plain,
% 63.23/63.25 (~P10(a229,a1,a2)),
% 63.23/63.25 inference(scs_inference,[],[2193,643,2152,705,426,4,429])).
% 63.23/63.25 cnf(2237,plain,
% 63.23/63.25 (P5(a255,a2)),
% 63.23/63.25 inference(scs_inference,[],[2193,643,2152,51,705,370,244,350,154,426,4,429,423,437,418])).
% 63.23/63.25 cnf(2239,plain,
% 63.23/63.25 (~E(a255,a2)),
% 63.23/63.25 inference(scs_inference,[],[2193,643,2152,442,51,705,370,244,350,154,426,4,429,423,437,418,23])).
% 63.23/63.25 cnf(2240,plain,
% 63.23/63.25 (~P5(x22401,x22401)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2242,plain,
% 63.23/63.25 (~P5(x22421,x22421)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2244,plain,
% 63.23/63.25 (~P5(x22441,x22441)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2251,plain,
% 63.23/63.25 (~E(a122,a229)),
% 63.23/63.25 inference(scs_inference,[],[2193,643,2152,442,2240,2242,2244,51,705,370,244,245,156,350,154,426,4,429,423,437,418,23,24,419,420,431,544])).
% 63.23/63.25 cnf(2268,plain,
% 63.23/63.25 (~E(a44,a1)),
% 63.23/63.25 inference(scs_inference,[],[2231,777,426,4])).
% 63.23/63.25 cnf(2269,plain,
% 63.23/63.25 (~P10(a218,a110,a2)),
% 63.23/63.25 inference(scs_inference,[],[2231,606,2230,777,426,4,429])).
% 63.23/63.25 cnf(2273,plain,
% 63.23/63.25 (P6(f4(a44),f4(a66),f4(a1),f4(a110))),
% 63.23/63.25 inference(scs_inference,[],[2231,606,2230,777,371,246,359,156,426,4,429,423,437])).
% 63.23/63.25 cnf(2275,plain,
% 63.23/63.25 (P5(a257,a2)),
% 63.23/63.25 inference(scs_inference,[],[2231,606,2230,51,777,371,246,359,156,426,4,429,423,437,418])).
% 63.23/63.25 cnf(2277,plain,
% 63.23/63.25 (~E(a257,a2)),
% 63.23/63.25 inference(scs_inference,[],[2231,606,2230,442,51,777,371,246,359,156,426,4,429,423,437,418,23])).
% 63.23/63.25 cnf(2305,plain,
% 63.23/63.25 (~E(a110,a2)),
% 63.23/63.25 inference(scs_inference,[],[2269,959,426,4])).
% 63.23/63.25 cnf(2306,plain,
% 63.23/63.25 (~P10(a122,a44,a2)),
% 63.23/63.25 inference(scs_inference,[],[2269,449,2268,959,426,4,429])).
% 63.23/63.25 cnf(2308,plain,
% 63.23/63.25 (P10(a130,a259,a2)),
% 63.23/63.25 inference(scs_inference,[],[2269,449,2268,959,248,158,426,4,429,423])).
% 63.23/63.25 cnf(2310,plain,
% 63.23/63.25 (P6(f4(a2),f4(a88),f4(a2),f4(a88))),
% 63.23/63.25 inference(scs_inference,[],[2269,449,2268,959,378,248,158,426,4,429,423,437])).
% 63.23/63.25 cnf(2312,plain,
% 63.23/63.25 (P5(a259,a2)),
% 63.23/63.25 inference(scs_inference,[],[2269,449,2268,51,959,378,248,158,426,4,429,423,437,418])).
% 63.23/63.25 cnf(2314,plain,
% 63.23/63.25 (~E(a259,a2)),
% 63.23/63.25 inference(scs_inference,[],[2269,449,2268,442,51,959,378,248,158,426,4,429,423,437,418,23])).
% 63.23/63.25 cnf(2334,plain,
% 63.23/63.25 (~E(a66,a2)),
% 63.23/63.25 inference(scs_inference,[],[2306,816,426,4])).
% 63.23/63.25 cnf(2335,plain,
% 63.23/63.25 (~P10(a229,a2,a2)),
% 63.23/63.25 inference(scs_inference,[],[2306,643,2192,816,426,4,429])).
% 63.23/63.25 cnf(2341,plain,
% 63.23/63.25 (P5(a261,a2)),
% 63.23/63.25 inference(scs_inference,[],[2306,643,2192,51,816,379,250,333,160,426,4,429,423,437,418])).
% 63.23/63.25 cnf(2344,plain,
% 63.23/63.25 (~P5(x23441,x23441)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2345,plain,
% 63.23/63.25 (~E(a261,a2)),
% 63.23/63.25 inference(scs_inference,[],[2306,643,2192,442,2344,51,816,379,250,333,160,426,4,429,423,437,418,24,23])).
% 63.23/63.25 cnf(2346,plain,
% 63.23/63.25 (~P5(x23461,x23461)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2348,plain,
% 63.23/63.25 (~P5(x23481,x23481)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2353,plain,
% 63.23/63.25 (P10(a261,a132,a2)),
% 63.23/63.25 inference(scs_inference,[],[2306,643,2192,442,2344,2346,2348,51,816,379,250,288,270,333,160,426,4,429,423,437,418,24,23,419,420,431])).
% 63.23/63.25 cnf(2364,plain,
% 63.23/63.25 (~E(a88,a2)),
% 63.23/63.25 inference(scs_inference,[],[2335,885,426,4])).
% 63.23/63.25 cnf(2365,plain,
% 63.23/63.25 (~P10(a2,a207,a2)),
% 63.23/63.25 inference(scs_inference,[],[2335,559,457,885,426,4,429])).
% 63.23/63.25 cnf(2367,plain,
% 63.23/63.25 (P10(a28,a157,a2)),
% 63.23/63.25 inference(scs_inference,[],[2335,559,457,885,298,270,426,4,429,423])).
% 63.23/63.25 cnf(2369,plain,
% 63.23/63.25 (P6(f4(a5),f4(a44),f4(a55),f4(a110))),
% 63.23/63.25 inference(scs_inference,[],[2335,559,457,885,380,298,342,270,426,4,429,423,437])).
% 63.23/63.25 cnf(2371,plain,
% 63.23/63.25 (P5(a157,a2)),
% 63.23/63.25 inference(scs_inference,[],[2335,559,51,457,885,380,298,342,270,426,4,429,423,437,418])).
% 63.23/63.25 cnf(2374,plain,
% 63.23/63.25 (~P5(x23741,x23741)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2375,plain,
% 63.23/63.25 (~E(a157,a2)),
% 63.23/63.25 inference(scs_inference,[],[2335,559,442,2374,51,457,885,380,298,342,270,426,4,429,423,437,418,24,23])).
% 63.23/63.25 cnf(2376,plain,
% 63.23/63.25 (~P5(x23761,x23761)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2378,plain,
% 63.23/63.25 (~P5(x23781,x23781)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2388,plain,
% 63.23/63.25 (P9(x23881,f121(f251(f4(a2),f4(a1))))+~E(a6,x23881)),
% 63.23/63.25 inference(scs_inference,[],[2335,559,442,2374,2376,2378,51,457,885,1700,380,71,298,287,269,342,270,426,4,429,423,437,418,24,23,419,420,431,415,16,25])).
% 63.23/63.25 cnf(2401,plain,
% 63.23/63.25 (~E(a99,a2)),
% 63.23/63.25 inference(scs_inference,[],[2365,1149,426,4])).
% 63.23/63.25 cnf(2402,plain,
% 63.23/63.25 (~P10(a2,a218,a2)),
% 63.23/63.25 inference(scs_inference,[],[2365,598,457,1149,426,4,429])).
% 63.23/63.25 cnf(2406,plain,
% 63.23/63.25 (P6(f4(a2),f4(a99),f4(a2),f4(a99))),
% 63.23/63.25 inference(scs_inference,[],[2365,598,457,1149,388,297,269,426,4,429,423,437])).
% 63.23/63.25 cnf(2408,plain,
% 63.23/63.25 (P5(a156,a2)),
% 63.23/63.25 inference(scs_inference,[],[2365,598,51,457,1149,388,297,269,426,4,429,423,437,418])).
% 63.23/63.25 cnf(2411,plain,
% 63.23/63.25 (~P5(x24111,x24111)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2412,plain,
% 63.23/63.25 (~E(a156,a2)),
% 63.23/63.25 inference(scs_inference,[],[2365,598,442,2411,51,457,1149,388,297,269,426,4,429,423,437,418,24,23])).
% 63.23/63.25 cnf(2413,plain,
% 63.23/63.25 (~P5(x24131,x24131)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2415,plain,
% 63.23/63.25 (~P5(x24151,x24151)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2422,plain,
% 63.23/63.25 (~P5(a2,a156)),
% 63.23/63.25 inference(scs_inference,[],[2365,598,442,2411,2413,2415,51,457,1149,388,297,286,268,269,426,4,429,423,437,418,24,23,419,420,431,415])).
% 63.23/63.25 cnf(2439,plain,
% 63.23/63.25 (~P10(a2,a229,a2)),
% 63.23/63.25 inference(scs_inference,[],[2402,633,457,594,426,4,429])).
% 63.23/63.25 cnf(2441,plain,
% 63.23/63.25 (P10(a26,a155,a2)),
% 63.23/63.25 inference(scs_inference,[],[2402,633,457,594,296,268,426,4,429,423])).
% 63.23/63.25 cnf(2445,plain,
% 63.23/63.25 (P5(a185,a18)),
% 63.23/63.25 inference(scs_inference,[],[2402,633,457,64,594,389,73,296,325,268,426,4,429,423,437,418])).
% 63.23/63.25 cnf(2468,plain,
% 63.23/63.25 (~E(a99,a88)),
% 63.23/63.25 inference(scs_inference,[],[2439,742,426,4])).
% 63.23/63.25 cnf(2469,plain,
% 63.23/63.25 (~P10(a2,a136,a2)),
% 63.23/63.25 inference(scs_inference,[],[2439,672,457,742,426,4,429])).
% 63.23/63.25 cnf(2471,plain,
% 63.23/63.25 (~E(a7,a2)),
% 63.23/63.25 inference(scs_inference,[],[2439,672,457,742,664,426,4,429,27])).
% 63.23/63.25 cnf(2472,plain,
% 63.23/63.25 (P10(a14,a143,a2)),
% 63.23/63.25 inference(scs_inference,[],[2439,672,457,742,664,285,257,426,4,429,27,423])).
% 63.23/63.25 cnf(2474,plain,
% 63.23/63.25 (P6(f4(a2),f4(a110),f4(a2),f4(a110))),
% 63.23/63.25 inference(scs_inference,[],[2439,672,457,742,398,664,285,257,426,4,429,27,423,437])).
% 63.23/63.25 cnf(2476,plain,
% 63.23/63.25 (P5(a185,a38)),
% 63.23/63.25 inference(scs_inference,[],[2439,672,457,64,742,398,664,75,285,257,426,4,429,27,423,437,418])).
% 63.23/63.25 cnf(2479,plain,
% 63.23/63.25 (~P5(x24791,x24791)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2481,plain,
% 63.23/63.25 (~P5(x24811,x24811)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2483,plain,
% 63.23/63.25 (~P5(x24831,x24831)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2488,plain,
% 63.23/63.25 (~P10(a1,a185,a2)),
% 63.23/63.25 inference(scs_inference,[],[1694,2439,672,442,2479,2481,2483,457,64,742,398,664,75,285,295,277,257,52,426,4,429,27,423,437,418,24,23,419,420,431])).
% 63.23/63.25 cnf(2492,plain,
% 63.23/63.25 (P9(x24921,f133(f4(a55)))+~E(a185,x24921)),
% 63.23/63.25 inference(scs_inference,[],[1694,2439,672,442,2479,2481,2483,457,64,742,398,664,75,285,295,277,257,52,426,4,429,27,423,437,418,24,23,419,420,431,415,25])).
% 63.23/63.25 cnf(2507,plain,
% 63.23/63.25 (~P10(a218,a99,a2)),
% 63.23/63.25 inference(scs_inference,[],[2469,606,2468,528,426,4,429])).
% 63.23/63.25 cnf(2509,plain,
% 63.23/63.25 (P10(a36,a165,a2)),
% 63.23/63.25 inference(scs_inference,[],[2469,606,2468,528,305,277,426,4,429,423])).
% 63.23/63.25 cnf(2511,plain,
% 63.23/63.25 (P6(f4(a77),f4(a2),f4(a44),f4(a110))),
% 63.23/63.25 inference(scs_inference,[],[2469,606,2468,528,305,344,277,311,426,4,429,423,437])).
% 63.23/63.25 cnf(2513,plain,
% 63.23/63.25 (P5(a185,a40)),
% 63.23/63.25 inference(scs_inference,[],[2469,606,2468,64,528,77,305,344,277,311,426,4,429,423,437,418])).
% 63.23/63.25 cnf(2516,plain,
% 63.23/63.25 (~P5(x25161,x25161)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2518,plain,
% 63.23/63.25 (~P5(x25181,x25181)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2520,plain,
% 63.23/63.25 (~P5(x25201,x25201)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2527,plain,
% 63.23/63.25 (~E(a229,a218)),
% 63.23/63.25 inference(scs_inference,[],[1375,2469,606,2468,442,2516,2518,2520,64,528,77,305,284,266,344,277,57,311,426,4,429,423,437,418,24,23,419,420,431,759])).
% 63.23/63.25 cnf(2531,plain,
% 63.23/63.25 (P9(x25311,f121(f251(f4(a77),f4(a1))))+~E(a40,x25311)),
% 63.23/63.25 inference(scs_inference,[],[1375,2469,606,2468,442,2516,2518,2520,64,528,1812,77,305,284,266,344,277,57,311,426,4,429,423,437,418,24,23,419,420,431,759,415,17,25])).
% 63.23/63.25 cnf(2544,plain,
% 63.23/63.25 (~E(a110,a99)),
% 63.23/63.25 inference(scs_inference,[],[2507,922,426,4])).
% 63.23/63.25 cnf(2545,plain,
% 63.23/63.25 (~P10(a2,a77,a2)),
% 63.23/63.25 inference(scs_inference,[],[2507,2060,457,922,426,4,429])).
% 63.23/63.25 cnf(2547,plain,
% 63.23/63.25 (P10(a24,a153,a2)),
% 63.23/63.25 inference(scs_inference,[],[2507,2060,457,922,294,266,426,4,429,423])).
% 63.23/63.25 cnf(2549,plain,
% 63.23/63.25 (P6(f4(a44),f4(a1),f4(a44),f4(a88))),
% 63.23/63.25 inference(scs_inference,[],[2507,2060,457,922,294,351,266,321,426,4,429,423,437])).
% 63.23/63.25 cnf(2551,plain,
% 63.23/63.25 (P5(a185,a42)),
% 63.23/63.25 inference(scs_inference,[],[2507,2060,457,64,922,79,294,351,266,321,426,4,429,423,437,418])).
% 63.23/63.25 cnf(2554,plain,
% 63.23/63.25 (~P5(x25541,x25541)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2556,plain,
% 63.23/63.25 (~P5(x25561,x25561)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2558,plain,
% 63.23/63.25 (~P5(x25581,x25581)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2563,plain,
% 63.23/63.25 (~P10(a5,a185,a2)),
% 63.23/63.25 inference(scs_inference,[],[1417,2507,2060,442,2554,2556,2558,457,64,922,79,294,304,255,351,266,321,53,426,4,429,423,437,418,24,23,419,420,431])).
% 63.23/63.25 cnf(2581,plain,
% 63.23/63.25 (~E(a44,a2)),
% 63.23/63.25 inference(scs_inference,[],[2545,987,426,4])).
% 63.23/63.25 cnf(2582,plain,
% 63.23/63.25 (~P10(a229,a110,a2)),
% 63.23/63.25 inference(scs_inference,[],[2545,643,2544,987,426,4,429])).
% 63.23/63.25 cnf(2584,plain,
% 63.23/63.25 (P10(a12,a141,a2)),
% 63.23/63.25 inference(scs_inference,[],[2545,643,2544,987,283,255,426,4,429,423])).
% 63.23/63.25 cnf(2586,plain,
% 63.23/63.25 (P6(f4(a55),f4(a44),f4(a1),f4(a99))),
% 63.23/63.25 inference(scs_inference,[],[2545,643,2544,987,283,352,255,339,426,4,429,423,437])).
% 63.23/63.25 cnf(2588,plain,
% 63.23/63.25 (P5(a185,a45)),
% 63.23/63.25 inference(scs_inference,[],[2545,643,2544,64,987,81,283,352,255,339,426,4,429,423,437,418])).
% 63.23/63.25 cnf(2608,plain,
% 63.23/63.25 (~E(a66,a55)),
% 63.23/63.25 inference(scs_inference,[],[2582,1106,426,4])).
% 63.23/63.25 cnf(2609,plain,
% 63.23/63.25 (~P10(a2,a158,a2)),
% 63.23/63.25 inference(scs_inference,[],[2582,707,457,1106,426,4,429])).
% 63.23/63.25 cnf(2611,plain,
% 63.23/63.25 (~E(a29,a2)),
% 63.23/63.25 inference(scs_inference,[],[2582,707,457,1106,699,426,4,429,27])).
% 63.23/63.25 cnf(2612,plain,
% 63.23/63.25 (P10(a34,a163,a2)),
% 63.23/63.25 inference(scs_inference,[],[2582,707,457,1106,699,303,275,426,4,429,27,423])).
% 63.23/63.25 cnf(2616,plain,
% 63.23/63.25 (P5(a185,a44)),
% 63.23/63.25 inference(scs_inference,[],[2582,707,457,64,54,1106,699,303,353,275,348,426,4,429,27,423,437,418])).
% 63.23/63.25 cnf(2645,plain,
% 63.23/63.25 (~P10(a185,a66,a2)),
% 63.23/63.25 inference(scs_inference,[],[2609,540,2608,1309,426,4,429])).
% 63.23/63.25 cnf(2653,plain,
% 63.23/63.25 (~E(a1,a185)),
% 63.23/63.25 inference(scs_inference,[],[2609,540,2608,442,64,52,1309,292,360,264,322,426,4,429,423,437,418,24])).
% 63.23/63.25 cnf(2654,plain,
% 63.23/63.25 (~P5(x26541,x26541)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2655,plain,
% 63.23/63.25 (~E(a185,a1)),
% 63.23/63.25 inference(scs_inference,[],[2609,540,2608,442,2654,64,52,1309,292,360,264,322,426,4,429,423,437,418,24,23])).
% 63.23/63.25 cnf(2656,plain,
% 63.23/63.25 (~P5(x26561,x26561)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2658,plain,
% 63.23/63.25 (~P5(x26581,x26581)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2663,plain,
% 63.23/63.25 (~P10(a66,a185,a2)),
% 63.23/63.25 inference(scs_inference,[],[2609,540,2608,442,2654,2656,2658,64,52,1309,292,302,253,360,264,56,322,426,4,429,423,437,418,24,23,419,420,431])).
% 63.23/63.25 cnf(2665,plain,
% 63.23/63.25 (~P5(a1,a185)),
% 63.23/63.25 inference(scs_inference,[],[2609,540,2608,442,2654,2656,2658,64,52,1309,292,302,253,360,264,56,322,426,4,429,423,437,418,24,23,419,420,431,415])).
% 63.23/63.25 cnf(2667,plain,
% 63.23/63.25 (P9(x26671,f121(f4(a1)))+~E(a1,x26671)),
% 63.23/63.25 inference(scs_inference,[],[2609,540,2608,442,2654,2656,2658,64,52,1309,292,302,253,360,264,56,322,426,4,429,423,437,418,24,23,419,420,431,415,25])).
% 63.23/63.25 cnf(2681,plain,
% 63.23/63.25 (~E(a55,a1)),
% 63.23/63.25 inference(scs_inference,[],[2645,1351,426,4])).
% 63.23/63.25 cnf(2682,plain,
% 63.23/63.25 (~P10(a122,a185,a2)),
% 63.23/63.25 inference(scs_inference,[],[2645,449,2655,1351,426,4,429])).
% 63.23/63.25 cnf(2684,plain,
% 63.23/63.25 (P10(a10,a139,a2)),
% 63.23/63.25 inference(scs_inference,[],[2645,449,2655,1351,281,253,426,4,429,423])).
% 63.23/63.25 cnf(2691,plain,
% 63.23/63.25 (~P5(x26911,x26911)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2692,plain,
% 63.23/63.25 (~E(a185,a55)),
% 63.23/63.25 inference(scs_inference,[],[2645,449,2655,442,2691,64,55,1351,281,361,253,349,426,4,429,423,437,418,24,23])).
% 63.23/63.25 cnf(2717,plain,
% 63.23/63.25 (~P10(a122,a55,a2)),
% 63.23/63.25 inference(scs_inference,[],[2682,449,2681,1427,426,4,429])).
% 63.23/63.25 cnf(2720,plain,
% 63.23/63.25 (P10(a32,a161,a2)),
% 63.23/63.25 inference(scs_inference,[],[2682,449,2681,526,1427,301,273,426,4,429,27,423])).
% 63.23/63.25 cnf(2726,plain,
% 63.23/63.25 (~E(a77,a185)),
% 63.23/63.25 inference(scs_inference,[],[2682,449,2681,442,526,64,57,1427,301,362,273,358,426,4,429,27,423,437,418,24])).
% 63.23/63.25 cnf(2727,plain,
% 63.23/63.25 (~P5(x27271,x27271)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2728,plain,
% 63.23/63.25 (~E(a185,a77)),
% 63.23/63.25 inference(scs_inference,[],[2682,449,2681,442,2727,526,64,57,1427,301,362,273,358,426,4,429,27,423,437,418,24,23])).
% 63.23/63.25 cnf(2729,plain,
% 63.23/63.25 (~P5(x27291,x27291)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2731,plain,
% 63.23/63.25 (~P5(x27311,x27311)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2736,plain,
% 63.23/63.25 (~P5(a77,a185)),
% 63.23/63.25 inference(scs_inference,[],[2682,449,2681,442,2727,2729,2731,526,64,57,1427,301,280,262,362,273,358,426,4,429,27,423,437,418,24,23,419,420,415])).
% 63.23/63.25 cnf(2741,plain,
% 63.23/63.25 (P9(x27411,f121(f4(a77)))+~E(a77,x27411)),
% 63.23/63.25 inference(scs_inference,[],[2682,449,1861,2681,442,2727,2729,2731,526,64,57,1427,2007,301,280,262,362,273,358,426,4,429,27,423,437,418,24,23,419,420,415,15,28,17,25])).
% 63.23/63.25 cnf(2752,plain,
% 63.23/63.25 (~E(a99,a55)),
% 63.23/63.25 inference(scs_inference,[],[2717,1469,426,4])).
% 63.23/63.25 cnf(2753,plain,
% 63.23/63.25 (~P10(a207,a185,a2)),
% 63.23/63.25 inference(scs_inference,[],[2717,569,2728,1469,426,4,429])).
% 63.23/63.25 cnf(2788,plain,
% 63.23/63.25 (~P10(a185,a185,a2)),
% 63.23/63.25 inference(scs_inference,[],[2753,540,2692,1510,426,4,429])).
% 63.23/63.25 cnf(2823,plain,
% 63.23/63.25 (~P10(a185,a99,a2)),
% 63.23/63.25 inference(scs_inference,[],[2788,540,2752,1551,426,4,429])).
% 63.23/63.25 cnf(2832,plain,
% 63.23/63.25 (~P5(x28321,x28321)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2834,plain,
% 63.23/63.25 (~P5(x28341,x28341)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2835,plain,
% 63.23/63.25 (~P8(f251(f4(a99),f251(f4(a5),f4(a1))),f251(f4(a99),f251(f4(a5),f4(a1))))),
% 63.23/63.25 inference(scs_inference,[],[2788,540,2752,442,2832,2834,64,1551,83,299,307,371,271,350,426,4,429,423,437,418,24,23,419])).
% 63.23/63.25 cnf(2840,plain,
% 63.23/63.25 (~E(a229,a185)),
% 63.23/63.25 inference(scs_inference,[],[2788,540,2752,442,2832,2834,64,1551,83,299,307,371,271,350,59,426,4,429,423,437,418,24,23,419,431,759])).
% 63.23/63.25 cnf(2845,plain,
% 63.23/63.25 (P9(x28451,f121(f4(a55)))+~E(a55,x28451)),
% 63.23/63.25 inference(scs_inference,[],[2788,540,1934,2752,442,2832,2834,64,55,1551,384,83,299,307,371,271,350,59,426,4,429,423,437,418,24,23,419,431,759,415,13,29,25])).
% 63.23/63.25 cnf(2857,plain,
% 63.23/63.25 (~E(a99,a1)),
% 63.23/63.25 inference(scs_inference,[],[2823,1592,426,4])).
% 63.23/63.25 cnf(2858,plain,
% 63.23/63.25 (~P10(a2,a55,a2)),
% 63.23/63.25 inference(scs_inference,[],[2823,1844,457,1592,426,4,429])).
% 63.23/63.25 cnf(2888,plain,
% 63.23/63.25 (~P10(a122,a99,a2)),
% 63.23/63.25 inference(scs_inference,[],[2858,449,2857,1629,426,4,429])).
% 63.23/63.25 cnf(2897,plain,
% 63.23/63.25 (~P5(x28971,x28971)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2898,plain,
% 63.23/63.25 (~E(a185,a99)),
% 63.23/63.25 inference(scs_inference,[],[2858,449,2857,442,2897,64,56,59,65,1629,380,315,426,4,429,423,437,418,24,23])).
% 63.23/63.25 cnf(2900,plain,
% 63.23/63.25 (~E(a229,a122)),
% 63.23/63.25 inference(scs_inference,[],[2858,449,2857,442,2897,64,56,59,65,1629,380,315,426,4,429,423,437,418,24,23,759])).
% 63.23/63.25 cnf(2908,plain,
% 63.23/63.25 (P9(x29081,f121(f4(a5)))+~E(a5,x29081)),
% 63.23/63.25 inference(scs_inference,[],[2858,449,2663,2020,2857,442,2897,64,57,53,56,59,65,2310,1629,386,380,315,426,4,429,423,437,418,24,23,759,415,15,28,26,11,27,25])).
% 63.23/63.25 cnf(2918,plain,
% 63.23/63.25 (~E(a66,a1)),
% 63.23/63.25 inference(scs_inference,[],[2888,1663,426,4])).
% 63.23/63.25 cnf(2919,plain,
% 63.23/63.25 (~P10(a229,a185,a2)),
% 63.23/63.25 inference(scs_inference,[],[2888,643,2898,1663,426,4,429])).
% 63.23/63.25 cnf(2947,plain,
% 63.23/63.25 (~E(a88,a55)),
% 63.23/63.25 inference(scs_inference,[],[2919,1814,426,4])).
% 63.23/63.25 cnf(2948,plain,
% 63.23/63.25 (~P10(a122,a66,a2)),
% 63.23/63.25 inference(scs_inference,[],[2919,449,2918,1814,426,4,429])).
% 63.23/63.25 cnf(2957,plain,
% 63.23/63.25 (~P5(x29571,x29571)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2965,plain,
% 63.23/63.25 (P9(x29651,f121(f4(a99)))+~E(a99,x29651)),
% 63.23/63.25 inference(scs_inference,[],[2919,449,2918,442,2957,64,59,89,71,161,2406,1814,390,324,318,426,4,429,437,423,418,24,23,415,13,12,15,25])).
% 63.23/63.25 cnf(2977,plain,
% 63.23/63.25 (~P10(a185,a88,a2)),
% 63.23/63.25 inference(scs_inference,[],[2948,540,2947,1849,426,4,429])).
% 63.23/63.25 cnf(2986,plain,
% 63.23/63.25 (~P5(x29861,x29861)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(2999,plain,
% 63.23/63.25 (P9(x29991,f121(f251(f4(a2),f4(a44))))+~E(a56,x29991)),
% 63.23/63.25 inference(scs_inference,[],[2948,540,2947,442,2986,64,586,59,91,73,58,163,2474,1849,391,325,309,426,4,429,423,437,418,24,23,431,415,17,28,10,14,26,16,25])).
% 63.23/63.25 cnf(3009,plain,
% 63.23/63.25 (~P10(a2,a169,a2)),
% 63.23/63.25 inference(scs_inference,[],[2977,746,457,1890,426,4,429])).
% 63.23/63.25 cnf(3011,plain,
% 63.23/63.25 (~E(a39,a2)),
% 63.23/63.25 inference(scs_inference,[],[2977,746,457,1890,738,426,4,429,27])).
% 63.23/63.25 cnf(3030,plain,
% 63.23/63.25 (~E(a88,a1)),
% 63.23/63.25 inference(scs_inference,[],[3009,1925,426,4])).
% 63.23/63.25 cnf(3031,plain,
% 63.23/63.25 (~P10(a2,a171,a2)),
% 63.23/63.25 inference(scs_inference,[],[3009,781,457,1925,426,4,429])).
% 63.23/63.25 cnf(3033,plain,
% 63.23/63.25 (~E(a41,a2)),
% 63.23/63.25 inference(scs_inference,[],[3009,781,457,1925,773,426,4,429,27])).
% 63.23/63.25 cnf(3041,plain,
% 63.23/63.25 (~P5(x30411,x30411)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(3042,plain,
% 63.23/63.25 (~E(a185,a88)),
% 63.23/63.25 inference(scs_inference,[],[3009,781,442,3041,457,64,58,77,167,1925,773,342,329,426,4,429,27,437,423,418,24,23])).
% 63.23/63.25 cnf(3044,plain,
% 63.23/63.25 (~P5(a88,a185)),
% 63.23/63.25 inference(scs_inference,[],[3009,781,442,3041,457,64,58,77,167,1925,773,342,329,426,4,429,27,437,423,418,24,23,415])).
% 63.23/63.25 cnf(3060,plain,
% 63.23/63.25 (~E(a110,a77)),
% 63.23/63.25 inference(scs_inference,[],[3031,1968,426,4])).
% 63.23/63.25 cnf(3061,plain,
% 63.23/63.25 (~P10(a122,a88,a2)),
% 63.23/63.25 inference(scs_inference,[],[3031,449,3030,1968,426,4,429])).
% 63.23/63.25 cnf(3082,plain,
% 63.23/63.25 (~P10(a207,a110,a2)),
% 63.23/63.25 inference(scs_inference,[],[3061,569,3060,2011,426,4,429])).
% 63.23/63.25 cnf(3091,plain,
% 63.23/63.25 (~P5(x30911,x30911)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(3097,plain,
% 63.23/63.25 (P9(x30971,f121(f4(a88)))+~E(a88,x30971)),
% 63.23/63.25 inference(scs_inference,[],[3061,569,3060,442,3091,64,58,97,81,171,2011,2273,352,312,426,4,429,423,437,418,24,23,415,14,25])).
% 63.23/63.25 cnf(3110,plain,
% 63.23/63.25 (~E(a110,a55)),
% 63.23/63.25 inference(scs_inference,[],[3082,2046,426,4])).
% 63.23/63.25 cnf(3111,plain,
% 63.23/63.25 (~P10(a218,a185,a2)),
% 63.23/63.25 inference(scs_inference,[],[3082,606,3042,2046,426,4,429])).
% 63.23/63.25 cnf(3133,plain,
% 63.23/63.25 (~P10(a185,a110,a2)),
% 63.23/63.25 inference(scs_inference,[],[3111,540,3110,2088,426,4,429])).
% 63.23/63.25 cnf(3142,plain,
% 63.23/63.25 (~P5(x31421,x31421)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(3145,plain,
% 63.23/63.25 (~P10(a110,a185,a2)),
% 63.23/63.25 inference(scs_inference,[],[3111,540,3110,442,3142,64,101,85,60,175,2088,359,313,426,4,429,423,437,418,24,23,431])).
% 63.23/63.25 cnf(3166,plain,
% 63.23/63.25 (~P10(a2,a173,a2)),
% 63.23/63.25 inference(scs_inference,[],[3133,820,457,2129,426,4,429])).
% 63.23/63.25 cnf(3168,plain,
% 63.23/63.25 (~E(a43,a2)),
% 63.23/63.25 inference(scs_inference,[],[3133,820,457,2129,812,426,4,429,27])).
% 63.23/63.25 cnf(3176,plain,
% 63.23/63.25 (~P5(x31761,x31761)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(3184,plain,
% 63.23/63.25 (P9(x31841,f121(f251(f4(a5),f4(a55))))+~E(a69,x31841)),
% 63.23/63.25 inference(scs_inference,[],[3133,820,442,3176,457,64,103,87,177,2129,2369,394,812,360,331,426,4,429,27,423,437,418,24,23,415,12,14,26,25])).
% 63.23/63.25 cnf(3195,plain,
% 63.23/63.25 (~E(a110,a1)),
% 63.23/63.25 inference(scs_inference,[],[3166,2161,426,4])).
% 63.23/63.25 cnf(3196,plain,
% 63.23/63.25 (~P10(a2,a178,a2)),
% 63.23/63.25 inference(scs_inference,[],[3166,889,457,2161,426,4,429])).
% 63.23/63.25 cnf(3198,plain,
% 63.23/63.25 (~E(a48,a2)),
% 63.23/63.25 inference(scs_inference,[],[3166,889,457,2161,881,426,4,429,27])).
% 63.23/63.25 cnf(3225,plain,
% 63.23/63.25 (~P10(a122,a110,a2)),
% 63.23/63.25 inference(scs_inference,[],[3196,449,3195,426,429])).
% 63.23/63.25 cnf(3234,plain,
% 63.23/63.25 (~P5(x32341,x32341)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(3241,plain,
% 63.23/63.25 (P9(x32411,f121(f4(a110)))+~E(a110,x32411)),
% 63.23/63.25 inference(scs_inference,[],[3196,449,3195,442,3234,64,60,105,91,181,2511,362,349,426,429,423,437,418,24,23,415,14,26,25])).
% 63.23/63.25 cnf(3253,plain,
% 63.23/63.25 (~P10(a2,a180,a2)),
% 63.23/63.25 inference(scs_inference,[],[3225,924,457,426,429])).
% 63.23/63.25 cnf(3255,plain,
% 63.23/63.25 (~E(a50,a2)),
% 63.23/63.25 inference(scs_inference,[],[3225,924,457,916,426,429,27])).
% 63.23/63.25 cnf(3263,plain,
% 63.23/63.25 (~P5(x32631,x32631)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(3273,plain,
% 63.23/63.25 (P9(x32731,f121(f251(f4(a77),f4(a55))))+~E(a73,x32731)),
% 63.23/63.25 inference(scs_inference,[],[3225,924,2353,442,3263,457,64,107,93,183,2549,397,916,368,370,426,429,27,423,437,418,24,23,415,16,11,28,13,15,25])).
% 63.23/63.25 cnf(3282,plain,
% 63.23/63.25 (~P10(a2,a184,a2)),
% 63.23/63.25 inference(scs_inference,[],[3253,990,457,426,429])).
% 63.23/63.25 cnf(3284,plain,
% 63.23/63.25 (~E(a54,a2)),
% 63.23/63.25 inference(scs_inference,[],[3253,990,457,981,426,429,27])).
% 63.23/63.25 cnf(3304,plain,
% 63.23/63.25 (~P10(a2,a187,a2)),
% 63.23/63.25 inference(scs_inference,[],[3282,1033,457,426,429])).
% 63.23/63.25 cnf(3308,plain,
% 63.23/63.25 (~E(a57,a2)),
% 63.23/63.25 inference(scs_inference,[],[3282,1033,457,97,187,1023,426,429,423,27])).
% 63.23/63.25 cnf(3333,plain,
% 63.23/63.25 (~P10(a2,a189,a2)),
% 63.23/63.25 inference(scs_inference,[],[3304,1075,457,426,429])).
% 63.23/63.25 cnf(3337,plain,
% 63.23/63.25 (~E(a59,a2)),
% 63.23/63.25 inference(scs_inference,[],[3304,1075,457,99,189,1065,426,429,423,27])).
% 63.23/63.25 cnf(3354,plain,
% 63.23/63.25 (~P10(a2,a88,a2)),
% 63.23/63.25 inference(scs_inference,[],[3333,2364,457,426,429])).
% 63.23/63.25 cnf(3363,plain,
% 63.23/63.25 (~P5(x33631,x33631)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(3368,plain,
% 63.23/63.25 (P9(x33681,f121(f251(f4(a55),f4(a66))))+~E(a82,x33681)),
% 63.23/63.25 inference(scs_inference,[],[3333,2364,442,3363,457,64,115,101,191,379,389,426,429,423,437,418,24,23,415,25])).
% 63.23/63.25 cnf(3371,plain,
% 63.23/63.25 (~P7(f4(a66))+~E(a82,a122)),
% 63.23/63.25 inference(scs_inference,[],[3333,459,2364,442,3363,51,457,64,115,101,191,379,389,426,429,423,437,418,24,23,415,25,420,417])).
% 63.23/63.25 cnf(3377,plain,
% 63.23/63.25 (~P10(a2,a99,a2)),
% 63.23/63.25 inference(scs_inference,[],[3354,2401,457,426,429])).
% 63.23/63.25 cnf(3405,plain,
% 63.23/63.25 (~P10(a2,a191,a2)),
% 63.23/63.25 inference(scs_inference,[],[3377,1108,457,426,429])).
% 63.23/63.25 cnf(3415,plain,
% 63.23/63.25 (~P5(x34151,x34151)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(3425,plain,
% 63.23/63.25 (P9(x34251,f121(f251(f4(a99),f4(a66))))+~E(a86,x34251)),
% 63.23/63.25 inference(scs_inference,[],[3377,1108,680,442,3415,457,64,119,105,195,2586,401,1100,335,328,426,429,27,423,437,418,24,23,415,12,10,11,16,29,25])).
% 63.23/63.25 cnf(3434,plain,
% 63.23/63.25 (~P10(a2,a193,a2)),
% 63.23/63.25 inference(scs_inference,[],[3405,1153,457,426,429])).
% 63.23/63.25 cnf(3458,plain,
% 63.23/63.25 (~P10(a2,a195,a2)),
% 63.23/63.25 inference(scs_inference,[],[3434,449,1195,457,520,426,424,429])).
% 63.23/63.25 cnf(3468,plain,
% 63.23/63.25 (~P5(x34681,x34681)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(3481,plain,
% 63.23/63.25 (P5(a185,a122)),
% 63.23/63.25 inference(scs_inference,[],[3434,441,449,1718,1195,442,3468,457,64,526,123,109,199,520,1185,333,310,426,424,429,423,27,437,418,24,23,415,414,19,28,25,2,410,412])).
% 63.23/63.25 cnf(3490,plain,
% 63.23/63.25 (~P10(a2,a198,a2)),
% 63.23/63.25 inference(scs_inference,[],[3481,3458,449,1229,457,551,426,415,424,429])).
% 63.23/63.25 cnf(3497,plain,
% 63.23/63.25 (P5(a185,a93)),
% 63.23/63.25 inference(scs_inference,[],[3481,3458,449,1229,457,64,125,111,201,551,1220,342,311,426,415,424,429,423,437,27,418])).
% 63.23/63.25 cnf(3500,plain,
% 63.23/63.25 (~P5(x35001,x35001)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(3503,plain,
% 63.23/63.25 (P5(a207,a122)),
% 63.23/63.25 inference(scs_inference,[],[3481,3458,449,2025,1229,442,3500,457,64,125,111,201,551,1220,342,311,426,415,424,429,423,437,27,418,24,23,414])).
% 63.23/63.25 cnf(3519,plain,
% 63.23/63.25 (~P5(a122,a207)),
% 63.23/63.25 inference(scs_inference,[],[3490,3503,426,415])).
% 63.23/63.25 cnf(3523,plain,
% 63.23/63.25 (~P10(a2,a200,a2)),
% 63.23/63.25 inference(scs_inference,[],[3490,3503,449,1269,457,592,426,415,424,429])).
% 63.23/63.25 cnf(3529,plain,
% 63.23/63.25 (P5(a185,a95)),
% 63.23/63.25 inference(scs_inference,[],[3490,3503,449,1269,457,64,127,113,203,592,350,339,426,415,424,429,423,437,418])).
% 63.23/63.25 cnf(3533,plain,
% 63.23/63.25 (~P5(x35331,x35331)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(3543,plain,
% 63.23/63.25 (P5(a218,a122)),
% 63.23/63.25 inference(scs_inference,[],[3490,3503,441,449,1622,1269,442,3533,457,64,127,113,203,67,592,1261,350,339,426,415,424,429,423,437,418,27,24,23,414,19,25,410,2,412])).
% 63.23/63.25 cnf(3548,plain,
% 63.23/63.25 (~P5(a122,a218)),
% 63.23/63.25 inference(scs_inference,[],[3543,3523,426,415])).
% 63.23/63.25 cnf(3552,plain,
% 63.23/63.25 (P5(a229,a122)),
% 63.23/63.25 inference(scs_inference,[],[3543,3523,449,2900,627,426,415,424,414])).
% 63.23/63.25 cnf(3554,plain,
% 63.23/63.25 (~P10(a2,a202,a2)),
% 63.23/63.25 inference(scs_inference,[],[3543,3523,449,2900,1313,457,627,426,415,424,414,429])).
% 63.23/63.25 cnf(3560,plain,
% 63.23/63.25 (P5(a185,a97)),
% 63.23/63.25 inference(scs_inference,[],[3543,3523,449,2900,1313,457,64,129,115,205,627,351,348,426,415,424,414,429,423,437,418])).
% 63.23/63.25 cnf(3582,plain,
% 63.23/63.25 (~P5(a122,a229)),
% 63.23/63.25 inference(scs_inference,[],[3552,3554,426,415])).
% 63.23/63.25 cnf(3586,plain,
% 63.23/63.25 (~P10(a2,a204,a2)),
% 63.23/63.25 inference(scs_inference,[],[3552,3554,449,1354,457,662,426,415,424,429])).
% 63.23/63.25 cnf(3592,plain,
% 63.23/63.25 (P5(a185,a100)),
% 63.23/63.25 inference(scs_inference,[],[3552,3554,449,1354,457,64,131,117,207,662,352,330,426,415,424,429,423,437,418])).
% 63.23/63.25 cnf(3617,plain,
% 63.23/63.25 (~P10(a2,a206,a2)),
% 63.23/63.25 inference(scs_inference,[],[3586,449,1386,457,701,3497,426,415,424,429])).
% 63.23/63.25 cnf(3623,plain,
% 63.23/63.25 (P5(a185,a102)),
% 63.23/63.25 inference(scs_inference,[],[3586,449,1386,457,64,133,119,209,701,3497,358,359,426,415,424,429,423,437,418])).
% 63.23/63.25 cnf(3648,plain,
% 63.23/63.25 (~P10(a2,a209,a2)),
% 63.23/63.25 inference(scs_inference,[],[3617,449,1429,457,736,3529,426,415,424,429])).
% 63.23/63.25 cnf(3654,plain,
% 63.23/63.25 (P5(a185,a104)),
% 63.23/63.25 inference(scs_inference,[],[3617,449,1429,457,64,135,121,211,736,3529,360,340,426,415,424,429,423,437,418])).
% 63.23/63.25 cnf(3678,plain,
% 63.23/63.25 (~P10(a2,a211,a2)),
% 63.23/63.25 inference(scs_inference,[],[3648,449,1473,457,775,3560,426,415,424,429])).
% 63.23/63.25 cnf(3684,plain,
% 63.23/63.25 (P5(a185,a106)),
% 63.23/63.25 inference(scs_inference,[],[3648,449,1473,457,64,137,123,213,775,3560,361,313,426,415,424,429,423,437,418])).
% 63.23/63.25 cnf(3708,plain,
% 63.23/63.25 (~P10(a2,a213,a2)),
% 63.23/63.25 inference(scs_inference,[],[3678,449,1511,457,810,3592,426,415,424,429])).
% 63.23/63.25 cnf(3714,plain,
% 63.23/63.25 (P5(a185,a108)),
% 63.23/63.25 inference(scs_inference,[],[3678,449,1511,457,64,139,125,215,810,3592,368,371,426,415,424,429,423,437,418])).
% 63.23/63.25 cnf(3738,plain,
% 63.23/63.25 (~P10(a2,a215,a2)),
% 63.23/63.25 inference(scs_inference,[],[3708,449,1553,457,849,3623,426,415,424,429])).
% 63.23/63.25 cnf(3744,plain,
% 63.23/63.25 (P5(a185,a111)),
% 63.23/63.25 inference(scs_inference,[],[3708,449,1553,457,64,141,127,217,849,3623,369,323,426,415,424,429,423,437,418])).
% 63.23/63.25 cnf(3768,plain,
% 63.23/63.25 (~P10(a2,a217,a2)),
% 63.23/63.25 inference(scs_inference,[],[3738,449,1596,457,879,3654,426,415,424,429])).
% 63.23/63.25 cnf(3774,plain,
% 63.23/63.25 (P5(a185,a113)),
% 63.23/63.25 inference(scs_inference,[],[3738,449,1596,457,64,143,129,219,879,3654,370,332,426,415,424,429,423,437,418])).
% 63.23/63.25 cnf(3798,plain,
% 63.23/63.25 (~P10(a2,a220,a2)),
% 63.23/63.25 inference(scs_inference,[],[3768,449,1630,457,918,3684,426,415,424,429])).
% 63.23/63.25 cnf(3804,plain,
% 63.23/63.25 (P5(a185,a115)),
% 63.23/63.25 inference(scs_inference,[],[3768,449,1630,457,64,145,131,221,918,3684,378,380,426,415,424,429,423,437,418])).
% 63.23/63.25 cnf(3828,plain,
% 63.23/63.25 (~P10(a2,a222,a2)),
% 63.23/63.25 inference(scs_inference,[],[3798,449,1666,457,953,3714,426,415,424,429])).
% 63.23/63.25 cnf(3834,plain,
% 63.23/63.25 (P5(a185,a117)),
% 63.23/63.25 inference(scs_inference,[],[3798,449,1666,457,64,147,133,223,953,3714,315,379,426,415,424,429,423,437,418])).
% 63.23/63.25 cnf(3858,plain,
% 63.23/63.25 (~P10(a2,a224,a2)),
% 63.23/63.25 inference(scs_inference,[],[3828,449,1708,457,983,3744,426,415,424,429])).
% 63.23/63.25 cnf(3864,plain,
% 63.23/63.25 (P5(a185,a119)),
% 63.23/63.25 inference(scs_inference,[],[3828,449,1708,457,64,149,135,225,983,3744,326,318,426,415,424,429,423,437,418])).
% 63.23/63.25 cnf(3888,plain,
% 63.23/63.25 (~P10(a2,a110,a2)),
% 63.23/63.25 inference(scs_inference,[],[3858,449,2305,457,1025,3774,426,415,424,429])).
% 63.23/63.25 cnf(3894,plain,
% 63.23/63.25 (P5(a185,a123)),
% 63.23/63.25 inference(scs_inference,[],[3858,449,2305,457,64,151,137,227,1025,3774,335,319,426,415,424,429,423,437,418])).
% 63.23/63.25 cnf(3918,plain,
% 63.23/63.25 (~P10(a2,a66,a2)),
% 63.23/63.25 inference(scs_inference,[],[3888,449,2334,457,1067,3804,426,415,424,429])).
% 63.23/63.25 cnf(3924,plain,
% 63.23/63.25 (P5(a185,a125)),
% 63.23/63.25 inference(scs_inference,[],[3888,449,2334,457,64,153,139,229,1067,3804,343,320,426,415,424,429,423,437,418])).
% 63.23/63.25 cnf(3948,plain,
% 63.23/63.25 (~P10(a2,a44,a2)),
% 63.23/63.25 inference(scs_inference,[],[3918,449,2581,457,1102,3834,426,415,424,429])).
% 63.23/63.25 cnf(3954,plain,
% 63.23/63.25 (P5(a185,a127)),
% 63.23/63.25 inference(scs_inference,[],[3918,449,2581,457,64,155,141,231,1102,3834,344,329,426,415,424,429,423,437,418])).
% 63.23/63.25 cnf(3974,plain,
% 63.23/63.25 (~P5(a119,a185)),
% 63.23/63.25 inference(scs_inference,[],[3948,3864,426,415])).
% 63.23/63.25 cnf(3978,plain,
% 63.23/63.25 (~P10(a2,a226,a2)),
% 63.23/63.25 inference(scs_inference,[],[3948,449,1740,457,1145,3864,426,415,424,429])).
% 63.23/63.25 cnf(3984,plain,
% 63.23/63.25 (P5(a185,a129)),
% 63.23/63.25 inference(scs_inference,[],[3948,449,1740,457,64,157,143,233,1145,3864,328,333,426,415,424,429,423,437,418])).
% 63.23/63.25 cnf(4008,plain,
% 63.23/63.25 (~P10(a2,a228,a2)),
% 63.23/63.25 inference(scs_inference,[],[3978,449,1781,457,1187,3894,426,415,424,429])).
% 63.23/63.25 cnf(4012,plain,
% 63.23/63.25 (P6(f4(a77),f4(a2),f4(a5),f4(a99))),
% 63.23/63.25 inference(scs_inference,[],[3978,449,1781,457,145,235,1187,3894,334,310,426,415,424,429,423,437])).
% 63.23/63.25 cnf(4014,plain,
% 63.23/63.25 (P5(a185,a131)),
% 63.23/63.25 inference(scs_inference,[],[3978,449,1781,457,64,159,145,235,1187,3894,334,310,426,415,424,429,423,437,418])).
% 63.23/63.25 cnf(4039,plain,
% 63.23/63.25 (~P10(a2,a7,a2)),
% 63.23/63.25 inference(scs_inference,[],[4008,449,2471,457,1222,3924,426,415,424,429])).
% 63.23/63.25 cnf(4045,plain,
% 63.23/63.25 (P5(a185,a17)),
% 63.23/63.25 inference(scs_inference,[],[4008,449,2471,457,64,260,147,237,1222,3924,331,319,426,415,424,429,423,437,418])).
% 63.23/63.25 cnf(4069,plain,
% 63.23/63.25 (~P10(a2,a231,a2)),
% 63.23/63.25 inference(scs_inference,[],[4039,449,1817,457,1263,3954,426,415,424,429])).
% 63.23/63.25 cnf(4075,plain,
% 63.23/63.25 (P5(a185,a16)),
% 63.23/63.25 inference(scs_inference,[],[4039,449,1817,457,64,259,149,239,1263,3954,362,322,426,415,424,429,423,437,418])).
% 63.23/63.25 cnf(4099,plain,
% 63.23/63.25 (~P10(a2,a233,a2)),
% 63.23/63.25 inference(scs_inference,[],[4069,449,1853,457,1305,3984,426,415,424,429])).
% 63.23/63.25 cnf(4105,plain,
% 63.23/63.25 (P5(a185,a15)),
% 63.23/63.25 inference(scs_inference,[],[4069,449,1853,457,64,258,151,241,1305,3984,338,341,426,415,424,429,423,437,418])).
% 63.23/63.25 cnf(4129,plain,
% 63.23/63.25 (~P10(a2,a235,a2)),
% 63.23/63.25 inference(scs_inference,[],[4099,449,1891,457,1349,4014,426,415,424,429])).
% 63.23/63.25 cnf(4135,plain,
% 63.23/63.25 (P5(a185,a37)),
% 63.23/63.25 inference(scs_inference,[],[4099,449,1891,457,64,278,153,243,1349,4014,349,312,426,415,424,429,423,437,418])).
% 63.23/63.25 cnf(4159,plain,
% 63.23/63.25 (~P10(a2,a237,a2)),
% 63.23/63.25 inference(scs_inference,[],[4129,449,1926,457,1383,4045,426,415,424,429])).
% 63.23/63.25 cnf(4165,plain,
% 63.23/63.25 (P5(a185,a25)),
% 63.23/63.25 inference(scs_inference,[],[4129,449,1926,457,64,267,155,245,1383,4045,350,321,426,415,424,429,423,437,418])).
% 63.23/63.25 cnf(4187,plain,
% 63.23/63.25 (~P10(a2,a239,a2)),
% 63.23/63.25 inference(scs_inference,[],[4159,1970,457,4075,426,415,429])).
% 63.23/63.25 cnf(4189,plain,
% 63.23/63.25 (P5(a185,a13)),
% 63.23/63.25 inference(scs_inference,[],[4159,1970,457,64,256,4075,426,415,429,418])).
% 63.23/63.25 cnf(4218,plain,
% 63.23/63.25 (~P10(a2,a242,a2)),
% 63.23/63.25 inference(scs_inference,[],[4187,2012,457,4105,426,415,429])).
% 63.23/63.25 cnf(4220,plain,
% 63.23/63.25 (P5(a185,a35)),
% 63.23/63.25 inference(scs_inference,[],[4187,2012,457,64,276,4105,426,415,429,418])).
% 63.23/63.25 cnf(4249,plain,
% 63.23/63.25 (~P10(a2,a244,a2)),
% 63.23/63.25 inference(scs_inference,[],[4218,2048,457,4135,426,415,429])).
% 63.23/63.25 cnf(4251,plain,
% 63.23/63.25 (P5(a185,a23)),
% 63.23/63.25 inference(scs_inference,[],[4218,2048,457,64,265,4135,426,415,429,418])).
% 63.23/63.25 cnf(4280,plain,
% 63.23/63.25 (~P10(a2,a246,a2)),
% 63.23/63.25 inference(scs_inference,[],[4249,2090,457,4165,426,415,429])).
% 63.23/63.25 cnf(4284,plain,
% 63.23/63.25 (P5(a185,a11)),
% 63.23/63.25 inference(scs_inference,[],[4249,2090,457,64,254,259,287,4165,426,415,429,423,418])).
% 63.23/63.25 cnf(4311,plain,
% 63.23/63.25 (~P10(a2,a248,a2)),
% 63.23/63.25 inference(scs_inference,[],[4280,2131,457,4189,426,415,429])).
% 63.23/63.25 cnf(4313,plain,
% 63.23/63.25 (P5(a185,a33)),
% 63.23/63.25 inference(scs_inference,[],[4280,2131,457,64,274,4189,426,415,429,418])).
% 63.23/63.25 cnf(4335,plain,
% 63.23/63.25 (~P10(a2,a250,a2)),
% 63.23/63.25 inference(scs_inference,[],[4311,2163,457,4313,426,415,429])).
% 63.23/63.25 cnf(4337,plain,
% 63.23/63.25 (P5(a185,a21)),
% 63.23/63.25 inference(scs_inference,[],[4311,2163,457,64,263,4313,426,415,429,418])).
% 63.23/63.25 cnf(4364,plain,
% 63.23/63.25 (~P10(a2,a253,a2)),
% 63.23/63.25 inference(scs_inference,[],[4335,2201,457,4220,426,415,429])).
% 63.23/63.25 cnf(4366,plain,
% 63.23/63.25 (P5(a185,a9)),
% 63.23/63.25 inference(scs_inference,[],[4335,2201,457,64,252,4220,426,415,429,418])).
% 63.23/63.25 cnf(4394,plain,
% 63.23/63.25 (~P10(a2,a29,a2)),
% 63.23/63.25 inference(scs_inference,[],[4364,2611,43,457,468,4251,426,415,22,429])).
% 63.23/63.25 cnf(4396,plain,
% 63.23/63.25 (~E(f4(a2),f4(a5))),
% 63.23/63.25 inference(scs_inference,[],[4364,2611,42,43,457,468,524,4251,426,415,22,429,21])).
% 63.23/63.25 cnf(4397,plain,
% 63.23/63.25 (P5(a185,a31)),
% 63.23/63.25 inference(scs_inference,[],[4364,2611,42,43,457,64,468,524,272,4251,426,415,22,429,21,418])).
% 63.23/63.25 cnf(4406,plain,
% 63.23/63.25 (~P5(x44061,x44061)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(4409,plain,
% 63.23/63.25 (~E(a5,a2)),
% 63.23/63.25 inference(scs_inference,[],[4364,449,2611,442,4406,42,43,457,64,468,524,272,256,284,1702,4251,323,309,426,415,22,429,21,418,437,423,424,23,24,4])).
% 63.23/63.25 cnf(4427,plain,
% 63.23/63.25 (~P10(a2,a255,a2)),
% 63.23/63.25 inference(scs_inference,[],[4394,2239,4396,457,4284,4,426,415,429])).
% 63.23/63.25 cnf(4429,plain,
% 63.23/63.25 (P5(a185,a19)),
% 63.23/63.25 inference(scs_inference,[],[4394,2239,4396,457,64,261,4284,4,426,415,429,418])).
% 63.23/63.25 cnf(4458,plain,
% 63.23/63.25 (~P10(a2,a257,a2)),
% 63.23/63.25 inference(scs_inference,[],[4427,2277,457,4337,426,415,429])).
% 63.23/63.25 cnf(4460,plain,
% 63.23/63.25 (P5(a185,a6)),
% 63.23/63.25 inference(scs_inference,[],[4427,2277,457,64,71,4337,426,415,429,418])).
% 63.23/63.25 cnf(4490,plain,
% 63.23/63.25 (~P10(a2,a259,a2)),
% 63.23/63.25 inference(scs_inference,[],[4458,2314,457,4366,426,415,429])).
% 63.23/63.25 cnf(4492,plain,
% 63.23/63.25 (P5(a185,a26)),
% 63.23/63.25 inference(scs_inference,[],[4458,2314,457,64,268,4366,426,415,429,418])).
% 63.23/63.25 cnf(4501,plain,
% 63.23/63.25 (~P5(x45011,x45011)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(4502,plain,
% 63.23/63.25 (~E(a26,a185)),
% 63.23/63.25 inference(scs_inference,[],[4458,449,2314,442,4501,457,64,254,268,282,1810,4366,320,318,426,415,429,418,437,424,423,23,24])).
% 63.23/63.25 cnf(4507,plain,
% 63.23/63.25 (P9(x45071,f121(f251(f4(a44),f251(f4(a2),f4(a1)))))+~E(a11,x45071)),
% 63.23/63.25 inference(scs_inference,[],[4458,449,2314,1278,442,4501,457,64,254,268,282,367,1810,4366,2308,320,318,426,415,429,418,437,424,423,23,24,27,13,29,25])).
% 63.23/63.25 cnf(4521,plain,
% 63.23/63.25 (~P10(a2,a261,a2)),
% 63.23/63.25 inference(scs_inference,[],[4490,2345,457,4429,426,415,429])).
% 63.23/63.25 cnf(4523,plain,
% 63.23/63.25 (P5(a185,a14)),
% 63.23/63.25 inference(scs_inference,[],[4490,2345,457,64,257,4429,426,415,429,418])).
% 63.23/63.25 cnf(4552,plain,
% 63.23/63.25 (~P10(a2,a157,a2)),
% 63.23/63.25 inference(scs_inference,[],[4521,2375,457,4397,426,415,429])).
% 63.23/63.25 cnf(4556,plain,
% 63.23/63.25 (P5(a185,a36)),
% 63.23/63.25 inference(scs_inference,[],[4521,2375,457,64,277,4397,342,338,426,415,429,437,418])).
% 63.23/63.25 cnf(4563,plain,
% 63.23/63.25 (~P5(x45631,x45631)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(4564,plain,
% 63.23/63.25 (~E(a36,a185)),
% 63.23/63.25 inference(scs_inference,[],[4521,449,2375,442,4563,457,64,263,277,291,1888,4397,342,338,426,415,429,437,418,424,423,23,24])).
% 63.23/63.25 cnf(4569,plain,
% 63.23/63.25 (P9(x45691,f121(f251(f4(a1),f251(f4(a2),f4(a1)))))+~E(a9,x45691)),
% 63.23/63.25 inference(scs_inference,[],[4521,449,2375,442,4563,457,64,252,263,277,291,1888,4012,4397,2367,381,342,338,426,415,429,437,418,424,423,23,24,27,15,11,25])).
% 63.23/63.25 cnf(4583,plain,
% 63.23/63.25 (~P10(a2,a156,a2)),
% 63.23/63.25 inference(scs_inference,[],[4552,2412,457,4460,426,415,429])).
% 63.23/63.25 cnf(4589,plain,
% 63.23/63.25 (P5(a185,a24)),
% 63.23/63.25 inference(scs_inference,[],[4552,449,2412,457,64,266,1923,4460,348,349,426,415,429,437,424,418])).
% 63.23/63.25 cnf(4612,plain,
% 63.23/63.25 (~P10(a2,a39,a2)),
% 63.23/63.25 inference(scs_inference,[],[4583,3011,457,4492,426,415,429])).
% 63.23/63.25 cnf(4618,plain,
% 63.23/63.25 (P5(a185,a12)),
% 63.23/63.25 inference(scs_inference,[],[4583,449,3011,457,64,255,1966,4492,353,330,426,415,429,424,437,418])).
% 63.23/63.25 cnf(4623,plain,
% 63.23/63.25 (~P5(x46231,x46231)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(4624,plain,
% 63.23/63.25 (~E(a12,a185)),
% 63.23/63.25 inference(scs_inference,[],[4583,449,3011,442,4623,457,64,272,255,300,1966,4492,353,330,426,415,429,424,437,418,423,23,24])).
% 63.23/63.25 cnf(4642,plain,
% 63.23/63.25 (~P10(a2,a41,a2)),
% 63.23/63.25 inference(scs_inference,[],[4612,3033,457,4523,426,415,429])).
% 63.23/63.25 cnf(4648,plain,
% 63.23/63.25 (P5(a185,a34)),
% 63.23/63.25 inference(scs_inference,[],[4612,449,3033,457,64,275,2009,4523,351,312,426,415,429,424,437,418])).
% 63.23/63.25 cnf(4653,plain,
% 63.23/63.25 (~P5(x46531,x46531)),
% 63.23/63.25 inference(rename_variables,[],[442])).
% 63.23/63.25 cnf(4654,plain,
% 63.23/63.25 (~E(a34,a185)),
% 63.23/63.25 inference(scs_inference,[],[4612,449,3033,442,4653,457,64,261,275,289,2009,4523,351,312,426,415,429,424,437,418,423,23,24])).
% 63.23/63.25 cnf(4672,plain,
% 63.23/63.25 (~P10(a2,a43,a2)),
% 63.23/63.25 inference(scs_inference,[],[4642,3168,457,4556,426,415,429])).
% 63.23/63.25 cnf(4678,plain,
% 63.23/63.25 (P5(a185,a22)),
% 63.23/63.25 inference(scs_inference,[],[4642,449,3168,457,64,264,2044,4556,352,321,426,415,429,424,437,418])).
% 63.23/63.25 cnf(4700,plain,
% 63.23/63.25 (~P10(a2,a48,a2)),
% 63.23/63.25 inference(scs_inference,[],[4672,3198,457,4589,426,415,429])).
% 63.23/63.25 cnf(4706,plain,
% 63.23/63.25 (P5(a185,a10)),
% 63.23/63.25 inference(scs_inference,[],[4672,449,3198,457,64,253,2086,4589,340,311,426,415,429,424,437,418])).
% 63.23/63.25 cnf(4723,plain,
% 63.23/63.25 (~P10(a2,a50,a2)),
% 63.23/63.25 inference(scs_inference,[],[4700,3255,457,4618,426,415,429])).
% 63.23/63.25 cnf(4729,plain,
% 63.23/63.25 (P5(a185,a32)),
% 63.23/63.25 inference(scs_inference,[],[4700,449,3255,457,64,273,2127,4618,331,310,426,415,429,424,437,418])).
% 63.23/63.25 cnf(4731,plain,
% 63.23/63.25 (~E(a32,a185)),
% 63.23/63.25 inference(scs_inference,[],[4700,449,3255,442,457,64,273,2127,4618,331,310,426,415,429,424,437,418,24])).
% 63.23/63.25 cnf(4751,plain,
% 63.23/63.25 (~P10(a2,a54,a2)),
% 63.23/63.25 inference(scs_inference,[],[4723,3284,457,4648,426,415,429])).
% 63.23/63.25 cnf(4757,plain,
% 63.23/63.25 (P5(a185,a20)),
% 63.23/63.25 inference(scs_inference,[],[4723,449,3284,457,64,262,2159,4648,332,319,426,415,429,424,437,418])).
% 63.23/63.25 cnf(4771,plain,
% 63.23/63.26 (~P10(a2,a57,a2)),
% 63.23/63.26 inference(scs_inference,[],[4751,3308,457,4678,426,415,429])).
% 63.23/63.26 cnf(4777,plain,
% 63.23/63.26 (P5(a185,a8)),
% 63.23/63.26 inference(scs_inference,[],[4751,449,3308,457,64,251,2199,4678,328,329,426,415,429,424,437,418])).
% 63.23/63.26 cnf(4794,plain,
% 63.23/63.26 (~P10(a2,a59,a2)),
% 63.23/63.26 inference(scs_inference,[],[4771,3337,457,4706,426,415,429])).
% 63.23/63.26 cnf(4800,plain,
% 63.23/63.26 (P5(a185,a30)),
% 63.23/63.26 inference(scs_inference,[],[4771,449,3337,457,64,271,2237,4706,320,339,426,415,429,424,437,418])).
% 63.23/63.26 cnf(4802,plain,
% 63.23/63.26 (~E(a30,a185)),
% 63.23/63.26 inference(scs_inference,[],[4771,449,3337,442,457,64,271,2237,4706,320,339,426,415,429,424,437,418,24])).
% 63.23/63.26 cnf(4822,plain,
% 63.23/63.26 (~P10(a2,a5,a2)),
% 63.23/63.26 inference(scs_inference,[],[4794,4409,457,4729,426,415,429])).
% 63.23/63.26 cnf(4828,plain,
% 63.23/63.26 (P5(a185,a7)),
% 63.23/63.26 inference(scs_inference,[],[4794,449,4409,457,64,72,2275,4729,330,310,426,415,429,424,437,418])).
% 63.23/63.26 cnf(4831,plain,
% 63.23/63.26 (~P5(x48311,x48311)),
% 63.23/63.26 inference(rename_variables,[],[442])).
% 63.23/63.26 cnf(4832,plain,
% 63.23/63.26 (~E(a185,a7)),
% 63.23/63.26 inference(scs_inference,[],[4794,449,4409,442,4831,457,64,72,2275,4729,330,310,426,415,429,424,437,418,24,23])).
% 63.23/63.26 cnf(4843,plain,
% 63.23/63.26 (~P10(a136,a185,a2)),
% 63.23/63.26 inference(scs_inference,[],[4822,680,4832,4757,426,415,429])).
% 63.23/63.26 cnf(4849,plain,
% 63.23/63.26 (P5(a185,a29)),
% 63.23/63.26 inference(scs_inference,[],[4822,449,680,4832,64,74,2312,4757,321,309,426,415,429,424,437,418])).
% 63.23/63.26 cnf(4852,plain,
% 63.23/63.26 (~P5(x48521,x48521)),
% 63.23/63.26 inference(rename_variables,[],[442])).
% 63.23/63.26 cnf(4853,plain,
% 63.23/63.26 (~E(a185,a29)),
% 63.23/63.26 inference(scs_inference,[],[4822,449,680,4832,442,4852,64,74,2312,4757,321,309,426,415,429,424,437,418,24,23])).
% 63.23/63.26 cnf(4867,plain,
% 63.23/63.26 (~P10(a158,a185,a2)),
% 63.23/63.26 inference(scs_inference,[],[4843,717,4853,4777,426,415,429])).
% 63.23/63.26 cnf(4873,plain,
% 63.23/63.26 (P5(a185,a39)),
% 63.23/63.26 inference(scs_inference,[],[4843,449,717,4853,64,76,2341,4777,322,318,426,415,429,424,437,418])).
% 63.23/63.26 cnf(4876,plain,
% 63.23/63.26 (~P5(x48761,x48761)),
% 63.23/63.26 inference(rename_variables,[],[442])).
% 63.23/63.26 cnf(4877,plain,
% 63.23/63.26 (~E(a185,a39)),
% 63.23/63.26 inference(scs_inference,[],[4843,449,717,4853,442,4876,64,76,2341,4777,322,318,426,415,429,424,437,418,24,23])).
% 63.23/63.26 cnf(4894,plain,
% 63.23/63.26 (~P5(a30,a185)),
% 63.23/63.26 inference(scs_inference,[],[4867,4800,426,415])).
% 63.23/63.26 cnf(4896,plain,
% 63.23/63.26 (~P10(a169,a185,a2)),
% 63.23/63.26 inference(scs_inference,[],[4867,754,4877,4800,426,415,429])).
% 63.23/63.26 cnf(4902,plain,
% 63.23/63.26 (P5(a185,a41)),
% 63.23/63.26 inference(scs_inference,[],[4867,449,754,4877,64,78,2371,4800,319,329,426,415,429,424,437,418])).
% 63.23/63.26 cnf(4904,plain,
% 63.23/63.26 (~E(a41,a185)),
% 63.23/63.26 inference(scs_inference,[],[4867,449,754,4877,442,64,78,2371,4800,319,329,426,415,429,424,437,418,24])).
% 63.23/63.26 cnf(4914,plain,
% 63.23/63.26 (P7(f4(a5))),
% 63.23/63.26 inference(scs_inference,[],[483,34,413,411])).
% 63.23/63.26 cnf(4925,plain,
% 63.23/63.26 (P10(a44,a3,a66)),
% 63.23/63.26 inference(scs_inference,[],[70,483,1441,2441,34,1614,50,413,411,416,427,422,417,2,426])).
% 63.23/63.26 cnf(4929,plain,
% 63.23/63.26 (~P10(a185,a155,a2)),
% 63.23/63.26 inference(scs_inference,[],[70,483,1441,2441,4502,4828,34,1614,50,413,411,416,427,422,417,2,426,415,430])).
% 63.23/63.26 cnf(4935,plain,
% 63.23/63.26 (P8(f4(a88),f4(a110))),
% 63.23/63.26 inference(scs_inference,[],[70,483,1441,1803,2441,4502,4828,34,1614,2835,2135,50,49,413,411,416,427,422,417,2,426,415,430,22,428,21,421])).
% 63.23/63.26 cnf(4949,plain,
% 63.23/63.26 (~P9(a167,f121(x49491))),
% 63.23/63.26 inference(scs_inference,[],[70,483,1441,1803,1982,3145,2441,4502,4828,34,1614,3519,445,2835,2135,4039,307,388,316,60,50,49,457,442,413,411,416,427,422,417,2,426,415,430,22,428,21,421,425,28,414,429,423,437,418])).
% 63.23/63.26 cnf(4950,plain,
% 63.23/63.26 (~P5(x49501,x49501)),
% 63.23/63.26 inference(rename_variables,[],[442])).
% 63.23/63.26 cnf(4958,plain,
% 63.23/63.26 (P10(a141,a12,a2)),
% 63.23/63.26 inference(scs_inference,[],[70,483,1441,1803,1982,3145,2441,2584,4502,4828,4896,34,1614,3519,445,2835,2135,4039,307,283,337,388,316,526,255,60,328,309,50,49,457,442,4950,413,411,416,427,422,417,2,426,415,430,22,428,21,421,425,28,414,429,423,437,418,27,438,419,431])).
% 63.23/63.26 cnf(4968,plain,
% 63.23/63.26 (P10(a55,a2,a55)),
% 63.23/63.26 inference(scs_inference,[],[70,483,519,1441,1803,1982,2408,3145,2441,2584,4502,4828,4896,34,1614,3974,3519,445,2835,2135,4039,307,283,337,388,149,1737,316,526,255,60,55,328,309,50,49,449,457,51,442,4950,413,411,416,427,422,417,2,426,415,430,22,428,21,421,425,28,414,429,423,437,418,27,438,419,431,420,613,2492,412,424,432])).
% 63.23/63.26 cnf(4972,plain,
% 63.23/63.26 (~P9(a167,f121(x49721))),
% 63.23/63.26 inference(rename_variables,[],[4949])).
% 63.23/63.26 cnf(4974,plain,
% 63.23/63.26 (~P9(a167,f121(x49741))),
% 63.23/63.26 inference(rename_variables,[],[4949])).
% 63.23/63.26 cnf(4976,plain,
% 63.23/63.26 (~P9(a167,f121(x49761))),
% 63.23/63.26 inference(rename_variables,[],[4949])).
% 63.23/63.26 cnf(4978,plain,
% 63.23/63.26 (~P9(a167,f121(x49781))),
% 63.23/63.26 inference(rename_variables,[],[4949])).
% 63.23/63.26 cnf(4980,plain,
% 63.23/63.26 (~P9(a167,f121(x49801))),
% 63.23/63.26 inference(rename_variables,[],[4949])).
% 63.23/63.26 cnf(4982,plain,
% 63.23/63.26 (~P9(a167,f121(x49821))),
% 63.23/63.26 inference(rename_variables,[],[4949])).
% 63.23/63.26 cnf(4984,plain,
% 63.23/63.26 (~P9(a167,f121(x49841))),
% 63.23/63.26 inference(rename_variables,[],[4949])).
% 63.23/63.26 cnf(4986,plain,
% 63.23/63.26 (~P9(a167,f121(x49861))),
% 63.23/63.26 inference(rename_variables,[],[4949])).
% 63.23/63.26 cnf(4988,plain,
% 63.23/63.26 (~P9(a167,f121(x49881))),
% 63.23/63.26 inference(rename_variables,[],[4949])).
% 63.23/63.26 cnf(4990,plain,
% 63.23/63.26 (~P9(a167,f121(x49901))),
% 63.23/63.26 inference(rename_variables,[],[4949])).
% 63.23/63.26 cnf(4992,plain,
% 63.23/63.26 (~P9(a167,f121(x49921))),
% 63.23/63.26 inference(rename_variables,[],[4949])).
% 63.23/63.26 cnf(4994,plain,
% 63.23/63.26 (~P9(a167,f121(x49941))),
% 63.23/63.26 inference(rename_variables,[],[4949])).
% 63.23/63.26 cnf(4996,plain,
% 63.23/63.26 (~P9(a167,f121(x49961))),
% 63.23/63.26 inference(rename_variables,[],[4949])).
% 63.23/63.26 cnf(4998,plain,
% 63.23/63.26 (~P9(a167,f121(x49981))),
% 63.23/63.26 inference(rename_variables,[],[4949])).
% 63.23/63.26 cnf(5000,plain,
% 63.23/63.26 (~P9(a167,f121(x50001))),
% 63.23/63.26 inference(rename_variables,[],[4949])).
% 63.23/63.26 cnf(5002,plain,
% 63.23/63.26 (~P9(a167,f121(x50021))),
% 63.23/63.26 inference(rename_variables,[],[4949])).
% 63.23/63.26 cnf(5004,plain,
% 63.23/63.26 (~P9(a167,f121(x50041))),
% 63.23/63.26 inference(rename_variables,[],[4949])).
% 63.23/63.26 cnf(5006,plain,
% 63.23/63.26 (~P9(a167,f121(x50061))),
% 63.23/63.26 inference(rename_variables,[],[4949])).
% 63.23/63.26 cnf(5007,plain,
% 63.23/63.26 (P7(f4(a44))),
% 63.23/63.26 inference(scs_inference,[],[4949,4972,4974,4976,4978,4980,4982,4984,4986,4988,4990,4992,4994,4996,4998,5000,5002,5004,35,688,726,2667,2741,2845,2908,2965,3097,3241,2388,2531,2999,3184,3273,3368,3425,4507,4569,411])).
% 63.23/63.26 cnf(5022,plain,
% 63.23/63.26 (~P10(a44,a134,a2)),
% 63.23/63.26 inference(scs_inference,[],[548,1606,2472,4914,4935,4949,4972,4974,4976,4978,4980,4982,4984,4986,4988,4990,4992,4994,4996,4998,5000,5002,5004,35,2445,4849,489,688,726,2667,2741,2845,2908,2965,3097,3241,2388,2531,2999,3184,3273,3368,3425,4507,4569,411,427,413,422,416,417,2,415,430])).
% 63.23/63.26 cnf(5026,plain,
% 63.23/63.26 (P8(f4(a2),f4(a5))),
% 63.23/63.26 inference(scs_inference,[],[548,622,1606,2472,4968,4914,4935,4949,4972,4974,4976,4978,4980,4982,4984,4986,4988,4990,4992,4994,4996,4998,5000,5002,5004,35,2445,4849,489,42,43,688,726,2667,2741,2845,2908,2965,3097,3241,2388,2531,2999,3184,3273,3368,3425,4507,4569,411,427,413,422,416,417,2,415,430,428,421])).
% 63.23/63.26 cnf(5031,plain,
% 63.23/63.26 (~P9(a167,f121(x50311))),
% 63.23/63.26 inference(rename_variables,[],[4949])).
% 63.23/63.26 cnf(5039,plain,
% 63.23/63.26 (~P9(a229,f121(x50391))),
% 63.23/63.26 inference(scs_inference,[],[548,622,1606,2488,2472,4802,4894,4968,4914,4935,4949,4972,4974,4976,4978,4980,4982,4984,4986,4988,4990,4992,4994,4996,4998,5000,5002,5004,5006,5031,35,2445,4849,3582,489,73,307,61,499,52,42,43,688,726,2667,2741,2845,2908,2965,3097,3241,2388,2531,2999,3184,3273,3368,3425,4507,4569,411,427,413,422,416,417,2,415,430,428,421,425,25,414,26,429,423,418])).
% 63.23/63.26 cnf(5051,plain,
% 63.23/63.26 (~P6(f4(a2),f4(a2),f4(a55),f4(a2))),
% 63.23/63.26 inference(scs_inference,[],[548,622,1606,2488,2472,4802,4894,4968,4914,4935,4949,4972,4974,4976,4978,4980,4982,4984,4986,4988,4990,4992,4994,4996,4998,5000,5002,5004,5006,5031,35,2445,4849,3582,3548,3044,489,1459,2858,402,398,73,307,61,67,56,499,52,58,55,309,42,43,51,688,726,2667,2741,2845,2908,2965,3097,3241,2388,2531,2999,3184,3273,3368,3425,4507,4569,411,427,413,422,416,417,2,415,430,428,421,425,25,414,26,429,423,418,438,419,431,420,424,432])).
% 63.23/63.26 cnf(5055,plain,
% 63.23/63.26 (P7(f4(a55))),
% 63.23/63.26 inference(scs_inference,[],[36,411])).
% 63.23/63.26 cnf(5058,plain,
% 63.23/63.26 (~P9(a229,f121(x50581))),
% 63.23/63.26 inference(rename_variables,[],[5039])).
% 63.23/63.26 cnf(5060,plain,
% 63.23/63.26 (~P9(a229,f121(x50601))),
% 63.23/63.26 inference(rename_variables,[],[5039])).
% 63.23/63.26 cnf(5062,plain,
% 63.23/63.26 (~P9(a229,f121(x50621))),
% 63.23/63.26 inference(rename_variables,[],[5039])).
% 63.23/63.26 cnf(5064,plain,
% 63.23/63.26 (~P9(a229,f121(x50641))),
% 63.23/63.26 inference(rename_variables,[],[5039])).
% 63.23/63.26 cnf(5066,plain,
% 63.23/63.26 (~P9(a229,f121(x50661))),
% 63.23/63.26 inference(rename_variables,[],[5039])).
% 63.23/63.26 cnf(5068,plain,
% 63.23/63.26 (~P9(a229,f121(x50681))),
% 63.23/63.26 inference(rename_variables,[],[5039])).
% 63.23/63.26 cnf(5070,plain,
% 63.23/63.26 (~P9(a229,f121(x50701))),
% 63.23/63.26 inference(rename_variables,[],[5039])).
% 63.23/63.26 cnf(5074,plain,
% 63.23/63.26 (~P9(a229,f121(x50741))),
% 63.23/63.26 inference(rename_variables,[],[5039])).
% 63.23/63.26 cnf(5076,plain,
% 63.23/63.26 (~P9(a229,f121(x50761))),
% 63.23/63.26 inference(rename_variables,[],[5039])).
% 63.23/63.26 cnf(5078,plain,
% 63.23/63.26 (~P9(a229,f121(x50781))),
% 63.23/63.26 inference(rename_variables,[],[5039])).
% 63.23/63.26 cnf(5080,plain,
% 63.23/63.26 (~P9(a229,f121(x50801))),
% 63.23/63.26 inference(rename_variables,[],[5039])).
% 63.23/63.26 cnf(5082,plain,
% 63.23/63.26 (~P9(a229,f121(x50821))),
% 63.23/63.26 inference(rename_variables,[],[5039])).
% 63.23/63.26 cnf(5084,plain,
% 63.23/63.26 (~P9(a229,f121(x50841))),
% 63.23/63.26 inference(rename_variables,[],[5039])).
% 63.23/63.26 cnf(5086,plain,
% 63.23/63.26 (~P9(a229,f121(x50861))),
% 63.23/63.26 inference(rename_variables,[],[5039])).
% 63.23/63.26 cnf(5092,plain,
% 63.23/63.26 (~P9(a229,f121(x50921))),
% 63.23/63.26 inference(rename_variables,[],[5039])).
% 63.23/63.26 cnf(5094,plain,
% 63.23/63.26 (~P9(a229,f121(x50941))),
% 63.23/63.26 inference(rename_variables,[],[5039])).
% 63.23/63.26 cnf(5096,plain,
% 63.23/63.26 (~P9(a229,f121(x50961))),
% 63.23/63.26 inference(rename_variables,[],[5039])).
% 63.23/63.26 cnf(5110,plain,
% 63.23/63.26 (P8(f4(a2),f4(a44))),
% 63.23/63.26 inference(scs_inference,[],[1939,709,2509,4564,5007,5026,5039,5058,5060,5062,5064,5066,5068,5070,5074,5076,5078,5080,5082,5084,5086,5092,5094,5096,36,2476,4873,44,411,3368,3425,726,2388,2999,4507,2741,413,3184,3273,3241,688,2845,2908,4569,422,427,3097,2531,2667,2965,416,417,2,415,430,428,421])).
% 63.23/63.26 cnf(5116,plain,
% 63.23/63.26 (~P10(a44,a5,a66)),
% 63.23/63.26 inference(scs_inference,[],[1939,2251,709,2509,4564,4925,5007,5026,5039,5058,5060,5062,5064,5066,5068,5070,5074,5076,5078,5080,5082,5084,5086,5092,5094,5096,36,2476,4873,3582,408,44,411,3368,3425,726,2388,2999,4507,2741,413,3184,3273,3241,688,2845,2908,4569,422,427,3097,2531,2667,2965,416,417,2,415,430,428,421,425,414,429])).
% 63.23/63.26 cnf(5122,plain,
% 63.23/63.26 (~P9(a163,f121(x51221))),
% 63.23/63.26 inference(scs_inference,[],[1939,2251,709,2509,4564,4925,5022,5007,5026,5039,5058,5060,5062,5064,5066,5068,5070,5074,5076,5078,5080,5082,5084,5086,5092,5094,5096,5051,36,2476,4873,3582,303,408,54,312,44,442,411,3368,3425,726,2388,2999,4507,2741,413,3184,3273,3241,688,2845,2908,4569,422,427,3097,2531,2667,2965,416,417,2,415,430,428,421,425,414,429,423,437,418])).
% 63.23/63.26 cnf(5123,plain,
% 63.23/63.26 (~P5(x51231,x51231)),
% 63.23/63.26 inference(rename_variables,[],[442])).
% 63.23/63.26 cnf(5130,plain,
% 63.23/63.26 (P10(a165,a36,a2)),
% 63.23/63.26 inference(scs_inference,[],[1939,2251,709,2509,4564,4925,5022,5007,5026,5039,5058,5060,5062,5064,5066,5068,5070,5074,5076,5078,5080,5082,5084,5086,5092,5094,5096,5051,36,2476,4873,3582,303,408,345,305,317,62,277,54,312,318,44,442,5123,411,3368,3425,726,2388,2999,4507,2741,413,3184,3273,3241,688,2845,2908,4569,422,427,3097,2531,2667,2965,416,417,2,415,430,428,421,425,414,429,423,437,418,438,419,431])).
% 63.23/63.26 cnf(5132,plain,
% 63.23/63.26 (~P9(a156,f121(f4(a5)))),
% 63.23/63.26 inference(scs_inference,[],[1939,2251,709,2509,4564,4925,5022,5007,5026,5039,5058,5060,5062,5064,5066,5068,5070,5074,5076,5078,5080,5082,5084,5086,5092,5094,5096,5051,36,2476,4873,2422,3582,303,408,345,305,317,62,277,54,312,318,44,51,442,5123,411,3368,3425,726,2388,2999,4507,2741,413,3184,3273,3241,688,2845,2908,4569,422,427,3097,2531,2667,2965,416,417,2,415,430,428,421,425,414,429,423,437,418,438,419,431,420])).
% 63.23/63.26 cnf(5141,plain,
% 63.23/63.26 (P7(f4(a66))),
% 63.23/63.26 inference(scs_inference,[],[37,411])).
% 63.23/63.26 cnf(5146,plain,
% 63.23/63.26 (~P9(a163,f121(x51461))),
% 63.23/63.26 inference(rename_variables,[],[5122])).
% 63.23/63.26 cnf(5150,plain,
% 63.23/63.26 (~P9(a163,f121(x51501))),
% 63.23/63.26 inference(rename_variables,[],[5122])).
% 63.23/63.26 cnf(5152,plain,
% 63.23/63.26 (~P9(a163,f121(x51521))),
% 63.23/63.26 inference(rename_variables,[],[5122])).
% 63.23/63.26 cnf(5154,plain,
% 63.23/63.26 (~P9(a163,f121(x51541))),
% 63.23/63.26 inference(rename_variables,[],[5122])).
% 63.23/63.26 cnf(5156,plain,
% 63.23/63.26 (~P9(a163,f121(x51561))),
% 63.23/63.26 inference(rename_variables,[],[5122])).
% 63.23/63.26 cnf(5160,plain,
% 63.23/63.26 (~P9(a163,f121(x51601))),
% 63.23/63.26 inference(rename_variables,[],[5122])).
% 63.23/63.26 cnf(5162,plain,
% 63.23/63.26 (~P9(a163,f121(x51621))),
% 63.23/63.26 inference(rename_variables,[],[5122])).
% 63.23/63.26 cnf(5164,plain,
% 63.23/63.26 (~P9(a163,f121(x51641))),
% 63.23/63.26 inference(rename_variables,[],[5122])).
% 63.23/63.26 cnf(5166,plain,
% 63.23/63.26 (~P9(a163,f121(x51661))),
% 63.23/63.26 inference(rename_variables,[],[5122])).
% 63.23/63.26 cnf(5168,plain,
% 63.23/63.26 (~P9(a163,f121(x51681))),
% 63.23/63.26 inference(rename_variables,[],[5122])).
% 63.23/63.26 cnf(5170,plain,
% 63.23/63.26 (~P9(a163,f121(x51701))),
% 63.23/63.26 inference(rename_variables,[],[5122])).
% 63.23/63.26 cnf(5172,plain,
% 63.23/63.26 (~P9(a163,f121(x51721))),
% 63.23/63.26 inference(rename_variables,[],[5122])).
% 63.23/63.26 cnf(5174,plain,
% 63.23/63.26 (~P9(a163,f121(x51741))),
% 63.23/63.26 inference(rename_variables,[],[5122])).
% 63.23/63.26 cnf(5178,plain,
% 63.23/63.26 (~P9(a163,f121(x51781))),
% 63.23/63.26 inference(rename_variables,[],[5122])).
% 63.23/63.26 cnf(5180,plain,
% 63.23/63.26 (~P9(a163,f121(x51801))),
% 63.23/63.26 inference(rename_variables,[],[5122])).
% 63.23/63.26 cnf(5182,plain,
% 63.23/63.26 (~P9(a163,f121(x51821))),
% 63.23/63.26 inference(rename_variables,[],[5122])).
% 63.23/63.26 cnf(5184,plain,
% 63.23/63.26 (~P9(a163,f121(x51841))),
% 63.23/63.26 inference(rename_variables,[],[5122])).
% 63.23/63.26 cnf(5190,plain,
% 63.23/63.26 (~P5(a41,a185)),
% 63.23/63.26 inference(scs_inference,[],[2213,2547,5055,5110,5122,5146,5150,5152,5154,5156,5160,5162,5164,5166,5168,5170,5172,5174,5178,5180,5182,5184,37,2513,4902,411,413,3368,422,2999,726,3241,3273,427,3425,2667,2741,3184,4507,2531,4569,2388,416,2965,2845,2908,3097,688,417,2,415])).
% 63.23/63.26 cnf(5192,plain,
% 63.23/63.26 (~P10(a110,a229,a2)),
% 63.23/63.26 inference(scs_inference,[],[733,2213,2547,5055,5110,5122,5146,5150,5152,5154,5156,5160,5162,5164,5166,5168,5170,5172,5174,5178,5180,5182,5184,37,2513,4902,625,411,413,3368,422,2999,726,3241,3273,427,3425,2667,2741,3184,4507,2531,4569,2388,416,2965,2845,2908,3097,688,417,2,415,430])).
% 63.23/63.26 cnf(5196,plain,
% 63.23/63.26 (P8(f4(a77),f4(a110))),
% 63.23/63.26 inference(scs_inference,[],[733,950,2213,2547,5055,5110,5122,5146,5150,5152,5154,5156,5160,5162,5164,5166,5168,5170,5172,5174,5178,5180,5182,5184,37,2513,4902,625,4925,4935,48,411,413,3368,422,2999,726,3241,3273,427,3425,2667,2741,3184,4507,2531,4569,2388,416,2965,2845,2908,3097,688,417,2,415,430,428,421])).
% 63.23/63.26 cnf(5232,plain,
% 63.23/63.26 (~E(a82,a122)),
% 63.23/63.26 inference(scs_inference,[],[5141,3371])).
% 63.23/63.26 cnf(5233,plain,
% 63.23/63.26 (P7(f4(a77))),
% 63.23/63.26 inference(scs_inference,[],[38,411])).
% 63.23/63.26 cnf(5251,plain,
% 63.23/63.26 (P8(f4(a66),f4(a110))),
% 63.23/63.26 inference(scs_inference,[],[2527,744,2612,4654,5141,5196,38,5132,2551,47,411,413,422,427,416,2908,417,2,430,428,421])).
% 63.23/63.26 cnf(5261,plain,
% 63.23/63.26 (~P9(a139,f121(x52611))),
% 63.23/63.26 inference(scs_inference,[],[2527,2653,744,2612,4624,4654,4958,5192,5141,5196,38,5132,2551,2665,281,60,47,442,411,413,422,427,416,2908,417,2,430,428,421,425,414,429,423,418])).
% 63.23/63.26 cnf(5262,plain,
% 63.23/63.26 (~P5(x52621,x52621)),
% 63.23/63.26 inference(rename_variables,[],[442])).
% 63.23/63.26 cnf(5273,plain,
% 63.23/63.26 (~P6(f4(a2),f4(a44),f4(a5),f4(a66))),
% 63.23/63.26 inference(scs_inference,[],[2527,2653,744,2612,4624,4654,4958,5116,5192,5141,5196,38,5132,2551,2665,571,1500,281,403,398,66,67,60,56,54,57,53,55,309,47,442,5262,411,413,422,427,416,2908,417,2,430,428,421,425,414,429,423,418,438,419,431,420,432])).
% 63.23/63.26 cnf(5290,plain,
% 63.23/63.26 (P7(f4(a88))),
% 63.23/63.26 inference(scs_inference,[],[5251,39,2588,422,413,411])).
% 63.23/63.26 cnf(5293,plain,
% 63.23/63.26 (~P9(a139,f121(x52931))),
% 63.23/63.26 inference(rename_variables,[],[5261])).
% 63.23/63.26 cnf(5295,plain,
% 63.23/63.26 (~P9(a139,f121(x52951))),
% 63.23/63.26 inference(rename_variables,[],[5261])).
% 63.23/63.26 cnf(5297,plain,
% 63.23/63.26 (~P9(a139,f121(x52971))),
% 63.23/63.26 inference(rename_variables,[],[5261])).
% 63.23/63.26 cnf(5299,plain,
% 63.23/63.26 (~P9(a139,f121(x52991))),
% 63.23/63.26 inference(rename_variables,[],[5261])).
% 63.23/63.26 cnf(5301,plain,
% 63.23/63.26 (~P9(a139,f121(x53011))),
% 63.23/63.26 inference(rename_variables,[],[5261])).
% 63.23/63.26 cnf(5305,plain,
% 63.23/63.26 (~P9(a139,f121(x53051))),
% 63.23/63.26 inference(rename_variables,[],[5261])).
% 63.23/63.26 cnf(5307,plain,
% 63.23/63.26 (~P9(a139,f121(x53071))),
% 63.23/63.26 inference(rename_variables,[],[5261])).
% 63.23/63.26 cnf(5309,plain,
% 63.23/63.26 (~P9(a139,f121(x53091))),
% 63.23/63.26 inference(rename_variables,[],[5261])).
% 63.23/63.26 cnf(5313,plain,
% 63.23/63.26 (~P9(a139,f121(x53131))),
% 63.23/63.26 inference(rename_variables,[],[5261])).
% 63.23/63.26 cnf(5315,plain,
% 63.23/63.26 (~P9(a139,f121(x53151))),
% 63.23/63.26 inference(rename_variables,[],[5261])).
% 63.23/63.26 cnf(5317,plain,
% 63.23/63.26 (~P9(a139,f121(x53171))),
% 63.23/63.26 inference(rename_variables,[],[5261])).
% 63.23/63.26 cnf(5319,plain,
% 63.23/63.26 (~P9(a139,f121(x53191))),
% 63.23/63.26 inference(rename_variables,[],[5261])).
% 63.23/63.26 cnf(5321,plain,
% 63.23/63.26 (~P9(a139,f121(x53211))),
% 63.23/63.26 inference(rename_variables,[],[5261])).
% 63.23/63.26 cnf(5323,plain,
% 63.23/63.26 (~P9(a139,f121(x53231))),
% 63.23/63.26 inference(rename_variables,[],[5261])).
% 63.23/63.26 cnf(5325,plain,
% 63.23/63.26 (~P9(a139,f121(x53251))),
% 63.23/63.26 inference(rename_variables,[],[5261])).
% 63.23/63.26 cnf(5327,plain,
% 63.23/63.26 (~P9(a139,f121(x53271))),
% 63.23/63.26 inference(rename_variables,[],[5261])).
% 63.23/63.26 cnf(5329,plain,
% 63.23/63.26 (~P9(a139,f121(x53291))),
% 63.23/63.26 inference(rename_variables,[],[5261])).
% 63.23/63.26 cnf(5339,plain,
% 63.23/63.26 (P8(f4(a2),f4(a55))),
% 63.23/63.26 inference(scs_inference,[],[492,1017,2840,2684,5233,5251,5261,5293,5295,5297,5299,5301,5305,5307,5309,5313,5315,5317,5319,5321,5323,5325,5327,5329,39,2588,489,4925,5110,45,422,413,411,726,3368,2667,2741,2388,427,2999,3241,3273,416,3425,4569,2845,688,3097,4507,3184,2531,2965,2908,417,2,430,428,421])).
% 63.23/63.26 cnf(5351,plain,
% 63.23/63.26 (~P9(a207,f121(x53511))),
% 63.23/63.26 inference(scs_inference,[],[492,1017,1205,2563,2840,2684,4904,5190,5233,5251,5261,5293,5295,5297,5299,5301,5305,5307,5309,5313,5315,5317,5319,5321,5323,5325,5327,5329,39,2588,3519,489,553,4925,5110,389,398,61,53,45,422,413,411,726,3368,2667,2741,2388,427,2999,3241,3273,416,3425,4569,2845,688,3097,4507,3184,2531,2965,2908,417,2,430,428,421,425,414,429,437,423,418])).
% 63.23/63.26 cnf(5378,plain,
% 63.23/63.26 (~P9(a207,f121(x53781))),
% 63.23/63.26 inference(rename_variables,[],[5351])).
% 63.23/63.26 cnf(5380,plain,
% 63.23/63.26 (~P9(a207,f121(x53801))),
% 63.23/63.26 inference(rename_variables,[],[5351])).
% 63.23/63.26 cnf(5382,plain,
% 63.23/63.26 (~P9(a207,f121(x53821))),
% 63.23/63.26 inference(rename_variables,[],[5351])).
% 63.23/63.26 cnf(5384,plain,
% 63.23/63.26 (~P9(a207,f121(x53841))),
% 63.23/63.26 inference(rename_variables,[],[5351])).
% 63.23/63.26 cnf(5386,plain,
% 63.23/63.26 (~P9(a207,f121(x53861))),
% 63.23/63.26 inference(rename_variables,[],[5351])).
% 63.23/63.26 cnf(5392,plain,
% 63.23/63.26 (~P9(a207,f121(x53921))),
% 63.23/63.26 inference(rename_variables,[],[5351])).
% 63.23/63.26 cnf(5394,plain,
% 63.23/63.26 (~P9(a207,f121(x53941))),
% 63.23/63.26 inference(rename_variables,[],[5351])).
% 63.23/63.26 cnf(5396,plain,
% 63.23/63.26 (~P9(a207,f121(x53961))),
% 63.23/63.26 inference(rename_variables,[],[5351])).
% 63.23/63.26 cnf(5398,plain,
% 63.23/63.26 (~P9(a207,f121(x53981))),
% 63.23/63.26 inference(rename_variables,[],[5351])).
% 63.23/63.26 cnf(5400,plain,
% 63.23/63.26 (~P9(a207,f121(x54001))),
% 63.23/63.26 inference(rename_variables,[],[5351])).
% 63.23/63.26 cnf(5402,plain,
% 63.23/63.26 (~P9(a207,f121(x54021))),
% 63.23/63.26 inference(rename_variables,[],[5351])).
% 63.23/63.26 cnf(5404,plain,
% 63.23/63.26 (~P9(a207,f121(x54041))),
% 63.23/63.26 inference(rename_variables,[],[5351])).
% 63.23/63.26 cnf(5406,plain,
% 63.23/63.26 (~P9(a207,f121(x54061))),
% 63.23/63.26 inference(rename_variables,[],[5351])).
% 63.23/63.26 cnf(5408,plain,
% 63.23/63.26 (~P9(a207,f121(x54081))),
% 63.23/63.26 inference(rename_variables,[],[5351])).
% 63.23/63.26 cnf(5410,plain,
% 63.23/63.26 (~P9(a207,f121(x54101))),
% 63.23/63.26 inference(rename_variables,[],[5351])).
% 63.23/63.26 cnf(5429,plain,
% 63.23/63.26 ($false),
% 63.23/63.26 inference(scs_inference,[],[2726,5232,783,2720,4731,4929,5130,5273,5290,5339,5351,5378,5380,5382,5384,5386,5392,5394,5396,5398,5400,5402,5404,5406,5408,5410,40,2616,2736,4564,358,340,540,46,413,422,411,726,2999,2388,3241,3368,427,416,3425,2741,2667,3097,3273,688,3184,2965,2845,2531,417,2908,2,430,428,421,28,425,414,429,437]),
% 63.23/63.26 ['proof']).
% 63.23/63.26 % SZS output end Proof
% 63.23/63.26 % Total time :62.450000s
%------------------------------------------------------------------------------