%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : NUM312+1 : TPTP v8.2.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n028.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:48 EDT 2024
% Result : Theorem 60.56s 60.75s
% Output : CNFRefutation 120.57s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.13 % Problem : NUM312+1 : TPTP v8.2.0. Released v3.1.0.
% 0.06/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n028.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Sat Jun 22 19:50:39 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.59/0.61 start to proof:theBenchmark
% 60.56/60.74 %-------------------------------------------
% 60.56/60.74 % File :CSE---1.7
% 60.56/60.74 % Problem :theBenchmark
% 60.56/60.74 % Transform :cnf
% 60.56/60.74 % Format :tptp:raw
% 60.56/60.74 % Command :java -jar mcs_scs.jar %d %s
% 60.56/60.74
% 60.56/60.74 % Result :Theorem 59.860000s
% 60.56/60.74 % Output :CNFRefutation 59.860000s
% 60.56/60.74 %-------------------------------------------
% 60.56/60.75 %------------------------------------------------------------------------------
% 60.56/60.75 % File : NUM312+1 : TPTP v8.2.0. Released v3.1.0.
% 60.56/60.75 % Domain : Number Theory (RDN arithmetic)
% 60.56/60.75 % Problem : only 2 + 3 = 5
% 60.56/60.75 % Version : Especial.
% 60.56/60.75 % English :
% 60.56/60.75
% 60.56/60.75 % Refs :
% 60.56/60.75 % Source : [TPTP]
% 60.56/60.75 % Names :
% 60.56/60.75
% 60.56/60.75 % Status : Theorem
% 60.56/60.75 % Rating : 0.50 v7.5.0, 0.56 v7.4.0, 0.50 v7.3.0, 0.48 v7.2.0, 0.45 v7.1.0, 0.39 v7.0.0, 0.43 v6.4.0, 0.54 v6.3.0, 0.50 v6.2.0, 0.52 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.4.0, 0.79 v3.3.0, 0.71 v3.2.0, 0.82 v3.1.0
% 60.56/60.75 % Syntax : Number of formulae : 402 ( 374 unt; 0 def)
% 60.56/60.75 % Number of atoms : 474 ( 6 equ)
% 60.56/60.75 % Maximal formula atoms : 8 ( 1 avg)
% 60.56/60.75 % Number of connectives : 74 ( 2 ~; 1 |; 43 &)
% 60.56/60.75 % ( 3 <=>; 25 =>; 0 <=; 0 <~>)
% 60.56/60.75 % Maximal formula depth : 19 ( 1 avg)
% 60.56/60.75 % Maximal term depth : 5 ( 2 avg)
% 60.56/60.75 % Number of predicates : 11 ( 10 usr; 0 prp; 1-4 aty)
% 60.56/60.75 % Number of functors : 260 ( 260 usr; 256 con; 0-2 aty)
% 60.56/60.75 % Number of variables : 122 ( 122 !; 0 ?)
% 60.56/60.75 % SPC : FOF_THM_RFO_SEQ
% 60.56/60.75
% 60.56/60.75 % Comments :
% 60.56/60.75 %------------------------------------------------------------------------------
% 60.56/60.75 %----Include axioms for RDN arithmetic
% 60.56/60.75 include('Axioms/NUM005+0.ax').
% 60.56/60.75 include('Axioms/NUM005+1.ax').
% 60.56/60.75 include('Axioms/NUM005+2.ax').
% 60.56/60.75 %------------------------------------------------------------------------------
% 60.56/60.75 fof(sum_only_n2_n3_n5,conjecture,
% 60.56/60.75 ! [X] :
% 60.56/60.75 ( sum(X,n3,n5)
% 60.56/60.75 => X = n2 ) ).
% 60.56/60.75
% 60.56/60.75 %------------------------------------------------------------------------------
% 60.56/60.75 %-------------------------------------------
% 60.56/60.75 % Proof found
% 60.56/60.75 % SZS status Theorem for theBenchmark
% 60.56/60.75 % SZS output start Proof
% 60.56/60.75 %ClaNum:440(EqnAxiom:32)
% 60.56/60.75 %VarNum:271(SingletonVarNum:132)
% 60.56/60.75 %MaxLitNum:8
% 60.56/60.75 %MaxfuncDepth:4
% 60.56/60.75 %SharedTerms:979
% 60.56/60.75 %goalClause: 70 408
% 60.56/60.75 %singleGoalClaCount:2
% 60.56/60.75 [70]P10(a3,a44,a66)
% 60.56/60.75 [408]~E(a3,a5)
% 60.56/60.75 [33]P1(f4(a1))
% 60.56/60.75 [34]P1(f4(a5))
% 60.56/60.75 [35]P1(f4(a44))
% 60.56/60.75 [36]P1(f4(a55))
% 60.56/60.75 [37]P1(f4(a66))
% 60.56/60.75 [38]P1(f4(a77))
% 60.56/60.75 [39]P1(f4(a88))
% 60.56/60.75 [40]P1(f4(a99))
% 60.56/60.75 [41]P1(f4(a110))
% 60.56/60.75 [42]P8(f4(a2),f4(a1))
% 60.56/60.75 [43]P8(f4(a1),f4(a5))
% 60.56/60.75 [44]P8(f4(a5),f4(a44))
% 60.56/60.75 [45]P8(f4(a44),f4(a55))
% 60.56/60.75 [46]P8(f4(a55),f4(a66))
% 60.56/60.75 [47]P8(f4(a66),f4(a77))
% 60.56/60.75 [48]P8(f4(a77),f4(a88))
% 60.56/60.75 [49]P8(f4(a88),f4(a99))
% 60.56/60.75 [50]P8(f4(a99),f4(a110))
% 60.56/60.75 [308]P2(f4(a2),f4(a2),f4(a2),f4(a2))
% 60.56/60.75 [309]P2(f4(a2),f4(a1),f4(a1),f4(a2))
% 60.56/60.75 [310]P2(f4(a2),f4(a5),f4(a5),f4(a2))
% 60.56/60.75 [311]P2(f4(a2),f4(a44),f4(a44),f4(a2))
% 60.56/60.75 [312]P2(f4(a2),f4(a55),f4(a55),f4(a2))
% 60.56/60.75 [313]P2(f4(a2),f4(a66),f4(a66),f4(a2))
% 60.56/60.75 [314]P2(f4(a2),f4(a77),f4(a77),f4(a2))
% 60.56/60.75 [315]P2(f4(a2),f4(a88),f4(a88),f4(a2))
% 60.56/60.75 [316]P2(f4(a2),f4(a99),f4(a99),f4(a2))
% 60.56/60.75 [317]P2(f4(a2),f4(a110),f4(a110),f4(a2))
% 60.56/60.76 [318]P2(f4(a1),f4(a2),f4(a1),f4(a2))
% 60.56/60.76 [319]P2(f4(a1),f4(a1),f4(a5),f4(a2))
% 60.56/60.76 [320]P2(f4(a1),f4(a5),f4(a44),f4(a2))
% 60.56/60.76 [321]P2(f4(a1),f4(a44),f4(a55),f4(a2))
% 60.56/60.76 [322]P2(f4(a1),f4(a55),f4(a66),f4(a2))
% 60.56/60.76 [323]P2(f4(a1),f4(a66),f4(a77),f4(a2))
% 60.56/60.76 [324]P2(f4(a1),f4(a77),f4(a88),f4(a2))
% 60.56/60.76 [325]P2(f4(a1),f4(a88),f4(a99),f4(a2))
% 60.56/60.76 [326]P2(f4(a1),f4(a99),f4(a110),f4(a2))
% 60.56/60.76 [327]P2(f4(a1),f4(a110),f4(a2),f4(a1))
% 60.56/60.76 [328]P2(f4(a5),f4(a2),f4(a5),f4(a2))
% 60.56/60.76 [329]P2(f4(a5),f4(a1),f4(a44),f4(a2))
% 60.56/60.76 [330]P2(f4(a5),f4(a5),f4(a55),f4(a2))
% 60.56/60.76 [331]P2(f4(a5),f4(a44),f4(a66),f4(a2))
% 60.56/60.76 [332]P2(f4(a5),f4(a55),f4(a77),f4(a2))
% 60.56/60.76 [333]P2(f4(a5),f4(a66),f4(a88),f4(a2))
% 60.56/60.76 [334]P2(f4(a5),f4(a77),f4(a99),f4(a2))
% 60.56/60.76 [335]P2(f4(a5),f4(a88),f4(a110),f4(a2))
% 60.56/60.76 [336]P2(f4(a5),f4(a99),f4(a2),f4(a1))
% 60.56/60.76 [337]P2(f4(a5),f4(a110),f4(a1),f4(a1))
% 60.56/60.76 [338]P2(f4(a44),f4(a2),f4(a44),f4(a2))
% 60.56/60.76 [339]P2(f4(a44),f4(a1),f4(a55),f4(a2))
% 60.56/60.76 [340]P2(f4(a44),f4(a5),f4(a66),f4(a2))
% 60.56/60.76 [341]P2(f4(a44),f4(a44),f4(a77),f4(a2))
% 60.56/60.76 [342]P2(f4(a44),f4(a55),f4(a88),f4(a2))
% 60.56/60.76 [343]P2(f4(a44),f4(a66),f4(a99),f4(a2))
% 60.56/60.76 [344]P2(f4(a44),f4(a77),f4(a110),f4(a2))
% 60.56/60.76 [345]P2(f4(a44),f4(a88),f4(a2),f4(a1))
% 60.56/60.76 [346]P2(f4(a44),f4(a99),f4(a1),f4(a1))
% 60.56/60.76 [347]P2(f4(a44),f4(a110),f4(a5),f4(a1))
% 60.56/60.76 [348]P2(f4(a55),f4(a2),f4(a55),f4(a2))
% 60.56/60.76 [349]P2(f4(a55),f4(a1),f4(a66),f4(a2))
% 60.56/60.76 [350]P2(f4(a55),f4(a5),f4(a77),f4(a2))
% 60.56/60.76 [351]P2(f4(a55),f4(a44),f4(a88),f4(a2))
% 60.56/60.76 [352]P2(f4(a55),f4(a55),f4(a99),f4(a2))
% 60.56/60.76 [353]P2(f4(a55),f4(a66),f4(a110),f4(a2))
% 60.56/60.76 [354]P2(f4(a55),f4(a77),f4(a2),f4(a1))
% 60.56/60.76 [355]P2(f4(a55),f4(a88),f4(a1),f4(a1))
% 60.56/60.76 [356]P2(f4(a55),f4(a99),f4(a5),f4(a1))
% 60.56/60.76 [357]P2(f4(a55),f4(a110),f4(a44),f4(a1))
% 60.56/60.76 [358]P2(f4(a66),f4(a2),f4(a66),f4(a2))
% 60.56/60.76 [359]P2(f4(a66),f4(a1),f4(a77),f4(a2))
% 60.56/60.76 [360]P2(f4(a66),f4(a5),f4(a88),f4(a2))
% 60.56/60.76 [361]P2(f4(a66),f4(a44),f4(a99),f4(a2))
% 60.56/60.76 [362]P2(f4(a66),f4(a55),f4(a110),f4(a2))
% 60.56/60.76 [363]P2(f4(a66),f4(a66),f4(a2),f4(a1))
% 60.56/60.76 [364]P2(f4(a66),f4(a77),f4(a1),f4(a1))
% 60.56/60.76 [365]P2(f4(a66),f4(a88),f4(a5),f4(a1))
% 60.56/60.76 [366]P2(f4(a66),f4(a99),f4(a44),f4(a1))
% 60.56/60.76 [367]P2(f4(a66),f4(a110),f4(a55),f4(a1))
% 60.56/60.76 [368]P2(f4(a77),f4(a2),f4(a77),f4(a2))
% 60.56/60.76 [369]P2(f4(a77),f4(a1),f4(a88),f4(a2))
% 60.56/60.76 [370]P2(f4(a77),f4(a5),f4(a99),f4(a2))
% 60.56/60.76 [371]P2(f4(a77),f4(a44),f4(a110),f4(a2))
% 60.56/60.76 [372]P2(f4(a77),f4(a55),f4(a2),f4(a1))
% 60.56/60.76 [373]P2(f4(a77),f4(a66),f4(a1),f4(a1))
% 60.56/60.76 [374]P2(f4(a77),f4(a77),f4(a5),f4(a1))
% 60.56/60.76 [375]P2(f4(a77),f4(a88),f4(a44),f4(a1))
% 60.56/60.76 [376]P2(f4(a77),f4(a99),f4(a55),f4(a1))
% 60.56/60.76 [377]P2(f4(a77),f4(a110),f4(a66),f4(a1))
% 60.56/60.76 [378]P2(f4(a88),f4(a2),f4(a88),f4(a2))
% 60.56/60.76 [379]P2(f4(a88),f4(a1),f4(a99),f4(a2))
% 60.56/60.76 [380]P2(f4(a88),f4(a5),f4(a110),f4(a2))
% 60.56/60.76 [381]P2(f4(a88),f4(a44),f4(a2),f4(a1))
% 60.56/60.76 [382]P2(f4(a88),f4(a55),f4(a1),f4(a1))
% 60.56/60.76 [383]P2(f4(a88),f4(a66),f4(a5),f4(a1))
% 60.56/60.76 [384]P2(f4(a88),f4(a77),f4(a44),f4(a1))
% 60.56/60.76 [385]P2(f4(a88),f4(a88),f4(a55),f4(a1))
% 60.56/60.76 [386]P2(f4(a88),f4(a99),f4(a66),f4(a1))
% 60.56/60.76 [387]P2(f4(a88),f4(a110),f4(a77),f4(a1))
% 60.56/60.76 [388]P2(f4(a99),f4(a2),f4(a99),f4(a2))
% 60.56/60.76 [389]P2(f4(a99),f4(a1),f4(a110),f4(a2))
% 60.56/60.76 [390]P2(f4(a99),f4(a5),f4(a2),f4(a1))
% 60.56/60.76 [391]P2(f4(a99),f4(a44),f4(a1),f4(a1))
% 60.56/60.76 [392]P2(f4(a99),f4(a55),f4(a5),f4(a1))
% 60.56/60.76 [393]P2(f4(a99),f4(a66),f4(a44),f4(a1))
% 60.56/60.76 [394]P2(f4(a99),f4(a77),f4(a55),f4(a1))
% 60.56/60.76 [395]P2(f4(a99),f4(a88),f4(a66),f4(a1))
% 60.56/60.76 [396]P2(f4(a99),f4(a99),f4(a77),f4(a1))
% 60.56/60.76 [397]P2(f4(a99),f4(a110),f4(a88),f4(a1))
% 60.56/60.76 [398]P2(f4(a110),f4(a2),f4(a110),f4(a2))
% 60.56/60.76 [399]P2(f4(a110),f4(a1),f4(a2),f4(a1))
% 60.56/60.76 [400]P2(f4(a110),f4(a5),f4(a1),f4(a1))
% 60.56/60.76 [401]P2(f4(a110),f4(a44),f4(a5),f4(a1))
% 60.56/60.76 [402]P2(f4(a110),f4(a55),f4(a44),f4(a1))
% 60.56/60.76 [403]P2(f4(a110),f4(a66),f4(a55),f4(a1))
% 60.56/60.76 [404]P2(f4(a110),f4(a77),f4(a66),f4(a1))
% 60.56/60.76 [405]P2(f4(a110),f4(a88),f4(a77),f4(a1))
% 60.56/60.76 [406]P2(f4(a110),f4(a99),f4(a88),f4(a1))
% 60.56/60.76 [407]P2(f4(a110),f4(a110),f4(a99),f4(a1))
% 60.56/60.76 [51]P9(a2,f121(f4(a2)))
% 60.56/60.76 [52]P9(a1,f121(f4(a1)))
% 60.56/60.76 [53]P9(a5,f121(f4(a5)))
% 60.56/60.76 [54]P9(a44,f121(f4(a44)))
% 60.56/60.76 [55]P9(a55,f121(f4(a55)))
% 60.56/60.76 [56]P9(a66,f121(f4(a66)))
% 60.56/60.76 [57]P9(a77,f121(f4(a77)))
% 60.56/60.76 [58]P9(a88,f121(f4(a88)))
% 60.56/60.76 [59]P9(a99,f121(f4(a99)))
% 60.56/60.76 [60]P9(a110,f121(f4(a110)))
% 60.56/60.76 [61]P9(a122,f133(f4(a1)))
% 60.56/60.76 [62]P9(a134,f133(f4(a5)))
% 60.56/60.76 [63]P9(a174,f133(f4(a44)))
% 60.56/60.76 [64]P9(a185,f133(f4(a55)))
% 60.56/60.76 [65]P9(a196,f133(f4(a66)))
% 60.56/60.76 [66]P9(a207,f133(f4(a77)))
% 60.56/60.76 [67]P9(a218,f133(f4(a88)))
% 60.56/60.76 [68]P9(a229,f133(f4(a99)))
% 60.56/60.76 [69]P9(a240,f133(f4(a110)))
% 60.56/60.76 [71]P9(a6,f121(f251(f4(a2),f4(a1))))
% 60.56/60.76 [72]P9(a7,f121(f251(f4(a1),f4(a1))))
% 60.56/60.76 [73]P9(a18,f121(f251(f4(a5),f4(a1))))
% 60.56/60.76 [74]P9(a29,f121(f251(f4(a44),f4(a1))))
% 60.56/60.76 [75]P9(a38,f121(f251(f4(a55),f4(a1))))
% 60.56/60.76 [76]P9(a39,f121(f251(f4(a66),f4(a1))))
% 60.56/60.76 [77]P9(a40,f121(f251(f4(a77),f4(a1))))
% 60.56/60.76 [78]P9(a41,f121(f251(f4(a88),f4(a1))))
% 60.56/60.76 [79]P9(a42,f121(f251(f4(a99),f4(a1))))
% 60.56/60.76 [80]P9(a43,f121(f251(f4(a110),f4(a1))))
% 60.56/60.76 [81]P9(a45,f121(f251(f4(a2),f4(a5))))
% 60.56/60.76 [82]P9(a46,f121(f251(f4(a1),f4(a5))))
% 60.56/60.76 [83]P9(a47,f121(f251(f4(a5),f4(a5))))
% 60.56/60.76 [84]P9(a48,f121(f251(f4(a44),f4(a5))))
% 60.56/60.76 [85]P9(a49,f121(f251(f4(a55),f4(a5))))
% 60.56/60.76 [86]P9(a50,f121(f251(f4(a66),f4(a5))))
% 60.56/60.76 [87]P9(a51,f121(f251(f4(a77),f4(a5))))
% 60.56/60.76 [88]P9(a52,f121(f251(f4(a88),f4(a5))))
% 60.56/60.76 [89]P9(a53,f121(f251(f4(a99),f4(a5))))
% 60.56/60.76 [90]P9(a54,f121(f251(f4(a110),f4(a5))))
% 60.56/60.76 [91]P9(a56,f121(f251(f4(a2),f4(a44))))
% 60.56/60.76 [92]P9(a57,f121(f251(f4(a1),f4(a44))))
% 60.56/60.76 [93]P9(a58,f121(f251(f4(a5),f4(a44))))
% 60.56/60.76 [94]P9(a59,f121(f251(f4(a44),f4(a44))))
% 60.56/60.76 [95]P9(a60,f121(f251(f4(a55),f4(a44))))
% 60.56/60.76 [96]P9(a61,f121(f251(f4(a66),f4(a44))))
% 60.56/60.76 [97]P9(a62,f121(f251(f4(a77),f4(a44))))
% 60.56/60.76 [98]P9(a63,f121(f251(f4(a88),f4(a44))))
% 60.56/60.76 [99]P9(a64,f121(f251(f4(a99),f4(a44))))
% 60.56/60.76 [100]P9(a65,f121(f251(f4(a110),f4(a44))))
% 60.56/60.76 [101]P9(a67,f121(f251(f4(a2),f4(a55))))
% 60.56/60.76 [102]P9(a68,f121(f251(f4(a1),f4(a55))))
% 60.56/60.76 [103]P9(a69,f121(f251(f4(a5),f4(a55))))
% 60.56/60.76 [104]P9(a70,f121(f251(f4(a44),f4(a55))))
% 60.56/60.76 [105]P9(a71,f121(f251(f4(a55),f4(a55))))
% 60.56/60.76 [106]P9(a72,f121(f251(f4(a66),f4(a55))))
% 60.56/60.76 [107]P9(a73,f121(f251(f4(a77),f4(a55))))
% 60.56/60.76 [108]P9(a74,f121(f251(f4(a88),f4(a55))))
% 60.56/60.76 [109]P9(a75,f121(f251(f4(a99),f4(a55))))
% 60.56/60.76 [110]P9(a76,f121(f251(f4(a110),f4(a55))))
% 60.56/60.76 [111]P9(a78,f121(f251(f4(a2),f4(a66))))
% 60.56/60.76 [112]P9(a79,f121(f251(f4(a1),f4(a66))))
% 60.56/60.76 [113]P9(a80,f121(f251(f4(a5),f4(a66))))
% 60.56/60.76 [114]P9(a81,f121(f251(f4(a44),f4(a66))))
% 60.56/60.76 [115]P9(a82,f121(f251(f4(a55),f4(a66))))
% 60.56/60.76 [116]P9(a83,f121(f251(f4(a66),f4(a66))))
% 60.56/60.76 [117]P9(a84,f121(f251(f4(a77),f4(a66))))
% 60.56/60.76 [118]P9(a85,f121(f251(f4(a88),f4(a66))))
% 60.56/60.76 [119]P9(a86,f121(f251(f4(a99),f4(a66))))
% 60.56/60.76 [120]P9(a87,f121(f251(f4(a110),f4(a66))))
% 60.56/60.76 [121]P9(a89,f121(f251(f4(a2),f4(a77))))
% 60.56/60.76 [122]P9(a90,f121(f251(f4(a1),f4(a77))))
% 60.56/60.76 [123]P9(a91,f121(f251(f4(a5),f4(a77))))
% 60.56/60.76 [124]P9(a92,f121(f251(f4(a44),f4(a77))))
% 60.56/60.76 [125]P9(a93,f121(f251(f4(a55),f4(a77))))
% 60.56/60.76 [126]P9(a94,f121(f251(f4(a66),f4(a77))))
% 60.56/60.76 [127]P9(a95,f121(f251(f4(a77),f4(a77))))
% 60.56/60.76 [128]P9(a96,f121(f251(f4(a88),f4(a77))))
% 60.56/60.76 [129]P9(a97,f121(f251(f4(a99),f4(a77))))
% 60.56/60.76 [130]P9(a98,f121(f251(f4(a110),f4(a77))))
% 60.56/60.76 [131]P9(a100,f121(f251(f4(a2),f4(a88))))
% 60.56/60.76 [132]P9(a101,f121(f251(f4(a1),f4(a88))))
% 60.56/60.76 [133]P9(a102,f121(f251(f4(a5),f4(a88))))
% 60.56/60.76 [134]P9(a103,f121(f251(f4(a44),f4(a88))))
% 60.56/60.76 [135]P9(a104,f121(f251(f4(a55),f4(a88))))
% 60.56/60.76 [136]P9(a105,f121(f251(f4(a66),f4(a88))))
% 60.56/60.76 [137]P9(a106,f121(f251(f4(a77),f4(a88))))
% 60.56/60.76 [138]P9(a107,f121(f251(f4(a88),f4(a88))))
% 60.56/60.76 [139]P9(a108,f121(f251(f4(a99),f4(a88))))
% 60.56/60.76 [140]P9(a109,f121(f251(f4(a110),f4(a88))))
% 60.56/60.76 [141]P9(a111,f121(f251(f4(a2),f4(a99))))
% 60.56/60.76 [142]P9(a112,f121(f251(f4(a1),f4(a99))))
% 60.56/60.76 [143]P9(a113,f121(f251(f4(a5),f4(a99))))
% 60.56/60.76 [144]P9(a114,f121(f251(f4(a44),f4(a99))))
% 60.56/60.76 [145]P9(a115,f121(f251(f4(a55),f4(a99))))
% 60.56/60.76 [146]P9(a116,f121(f251(f4(a66),f4(a99))))
% 60.56/60.76 [147]P9(a117,f121(f251(f4(a77),f4(a99))))
% 60.56/60.76 [148]P9(a118,f121(f251(f4(a88),f4(a99))))
% 60.56/60.76 [149]P9(a119,f121(f251(f4(a99),f4(a99))))
% 60.56/60.76 [150]P9(a120,f121(f251(f4(a110),f4(a99))))
% 60.56/60.76 [151]P9(a123,f121(f251(f4(a2),f4(a110))))
% 60.56/60.76 [152]P9(a124,f121(f251(f4(a1),f4(a110))))
% 60.56/60.76 [153]P9(a125,f121(f251(f4(a5),f4(a110))))
% 60.56/60.76 [154]P9(a126,f121(f251(f4(a44),f4(a110))))
% 60.56/60.76 [155]P9(a127,f121(f251(f4(a55),f4(a110))))
% 60.56/60.76 [156]P9(a128,f121(f251(f4(a66),f4(a110))))
% 60.56/60.76 [157]P9(a129,f121(f251(f4(a77),f4(a110))))
% 60.56/60.76 [158]P9(a130,f121(f251(f4(a88),f4(a110))))
% 60.56/60.76 [159]P9(a131,f121(f251(f4(a99),f4(a110))))
% 60.56/60.76 [160]P9(a132,f121(f251(f4(a110),f4(a110))))
% 60.56/60.76 [161]P9(a135,f133(f251(f4(a2),f4(a1))))
% 60.56/60.76 [162]P9(a136,f133(f251(f4(a1),f4(a1))))
% 60.56/60.76 [163]P9(a147,f133(f251(f4(a5),f4(a1))))
% 60.56/60.76 [164]P9(a158,f133(f251(f4(a44),f4(a1))))
% 60.56/60.76 [165]P9(a168,f133(f251(f4(a55),f4(a1))))
% 60.56/60.76 [166]P9(a169,f133(f251(f4(a66),f4(a1))))
% 60.56/60.76 [167]P9(a170,f133(f251(f4(a77),f4(a1))))
% 60.56/60.76 [168]P9(a171,f133(f251(f4(a88),f4(a1))))
% 60.56/60.76 [169]P9(a172,f133(f251(f4(a99),f4(a1))))
% 60.56/60.76 [170]P9(a173,f133(f251(f4(a110),f4(a1))))
% 60.56/60.76 [171]P9(a175,f133(f251(f4(a2),f4(a5))))
% 60.56/60.76 [172]P9(a176,f133(f251(f4(a1),f4(a5))))
% 60.56/60.76 [173]P9(a177,f133(f251(f4(a5),f4(a5))))
% 60.56/60.76 [174]P9(a178,f133(f251(f4(a44),f4(a5))))
% 60.56/60.76 [175]P9(a179,f133(f251(f4(a55),f4(a5))))
% 60.56/60.76 [176]P9(a180,f133(f251(f4(a66),f4(a5))))
% 60.56/60.76 [177]P9(a181,f133(f251(f4(a77),f4(a5))))
% 60.56/60.76 [178]P9(a182,f133(f251(f4(a88),f4(a5))))
% 60.56/60.76 [179]P9(a183,f133(f251(f4(a99),f4(a5))))
% 60.56/60.76 [180]P9(a184,f133(f251(f4(a110),f4(a5))))
% 60.56/60.76 [181]P9(a186,f133(f251(f4(a2),f4(a44))))
% 60.56/60.76 [182]P9(a187,f133(f251(f4(a1),f4(a44))))
% 60.56/60.76 [183]P9(a188,f133(f251(f4(a5),f4(a44))))
% 60.56/60.76 [184]P9(a189,f133(f251(f4(a44),f4(a44))))
% 60.56/60.76 [185]P9(a190,f133(f251(f4(a55),f4(a44))))
% 60.56/60.76 [186]P9(a191,f133(f251(f4(a66),f4(a44))))
% 60.56/60.76 [187]P9(a192,f133(f251(f4(a77),f4(a44))))
% 60.56/60.76 [188]P9(a193,f133(f251(f4(a88),f4(a44))))
% 60.56/60.76 [189]P9(a194,f133(f251(f4(a99),f4(a44))))
% 60.56/60.76 [190]P9(a195,f133(f251(f4(a110),f4(a44))))
% 60.56/60.76 [191]P9(a197,f133(f251(f4(a2),f4(a55))))
% 60.56/60.76 [192]P9(a198,f133(f251(f4(a1),f4(a55))))
% 60.56/60.76 [193]P9(a199,f133(f251(f4(a5),f4(a55))))
% 60.56/60.76 [194]P9(a200,f133(f251(f4(a44),f4(a55))))
% 60.56/60.76 [195]P9(a201,f133(f251(f4(a55),f4(a55))))
% 60.56/60.76 [196]P9(a202,f133(f251(f4(a66),f4(a55))))
% 60.56/60.76 [197]P9(a203,f133(f251(f4(a77),f4(a55))))
% 60.56/60.76 [198]P9(a204,f133(f251(f4(a88),f4(a55))))
% 60.56/60.76 [199]P9(a205,f133(f251(f4(a99),f4(a55))))
% 60.56/60.76 [200]P9(a206,f133(f251(f4(a110),f4(a55))))
% 60.56/60.76 [201]P9(a208,f133(f251(f4(a2),f4(a66))))
% 60.56/60.76 [202]P9(a209,f133(f251(f4(a1),f4(a66))))
% 60.56/60.76 [203]P9(a210,f133(f251(f4(a5),f4(a66))))
% 60.56/60.76 [204]P9(a211,f133(f251(f4(a44),f4(a66))))
% 60.56/60.76 [205]P9(a212,f133(f251(f4(a55),f4(a66))))
% 60.56/60.76 [206]P9(a213,f133(f251(f4(a66),f4(a66))))
% 60.56/60.77 [207]P9(a214,f133(f251(f4(a77),f4(a66))))
% 60.56/60.77 [208]P9(a215,f133(f251(f4(a88),f4(a66))))
% 60.56/60.77 [209]P9(a216,f133(f251(f4(a99),f4(a66))))
% 60.56/60.77 [210]P9(a217,f133(f251(f4(a110),f4(a66))))
% 60.56/60.77 [211]P9(a219,f133(f251(f4(a2),f4(a77))))
% 60.56/60.77 [212]P9(a220,f133(f251(f4(a1),f4(a77))))
% 60.56/60.77 [213]P9(a221,f133(f251(f4(a5),f4(a77))))
% 60.56/60.77 [214]P9(a222,f133(f251(f4(a44),f4(a77))))
% 60.56/60.77 [215]P9(a223,f133(f251(f4(a55),f4(a77))))
% 60.56/60.77 [216]P9(a224,f133(f251(f4(a66),f4(a77))))
% 60.56/60.77 [217]P9(a225,f133(f251(f4(a77),f4(a77))))
% 60.56/60.77 [218]P9(a226,f133(f251(f4(a88),f4(a77))))
% 60.56/60.77 [219]P9(a227,f133(f251(f4(a99),f4(a77))))
% 60.56/60.77 [220]P9(a228,f133(f251(f4(a110),f4(a77))))
% 60.56/60.77 [221]P9(a230,f133(f251(f4(a2),f4(a88))))
% 60.56/60.77 [222]P9(a231,f133(f251(f4(a1),f4(a88))))
% 60.56/60.77 [223]P9(a232,f133(f251(f4(a5),f4(a88))))
% 60.56/60.77 [224]P9(a233,f133(f251(f4(a44),f4(a88))))
% 60.56/60.77 [225]P9(a234,f133(f251(f4(a55),f4(a88))))
% 60.56/60.77 [226]P9(a235,f133(f251(f4(a66),f4(a88))))
% 60.56/60.77 [227]P9(a236,f133(f251(f4(a77),f4(a88))))
% 60.56/60.77 [228]P9(a237,f133(f251(f4(a88),f4(a88))))
% 60.56/60.77 [229]P9(a238,f133(f251(f4(a99),f4(a88))))
% 60.56/60.77 [230]P9(a239,f133(f251(f4(a110),f4(a88))))
% 60.56/60.77 [231]P9(a241,f133(f251(f4(a2),f4(a99))))
% 60.56/60.77 [232]P9(a242,f133(f251(f4(a1),f4(a99))))
% 60.56/60.77 [233]P9(a243,f133(f251(f4(a5),f4(a99))))
% 60.56/60.77 [234]P9(a244,f133(f251(f4(a44),f4(a99))))
% 60.56/60.77 [235]P9(a245,f133(f251(f4(a55),f4(a99))))
% 60.56/60.77 [236]P9(a246,f133(f251(f4(a66),f4(a99))))
% 60.56/60.77 [237]P9(a247,f133(f251(f4(a77),f4(a99))))
% 60.56/60.77 [238]P9(a248,f133(f251(f4(a88),f4(a99))))
% 60.56/60.77 [239]P9(a249,f133(f251(f4(a99),f4(a99))))
% 60.56/60.77 [240]P9(a250,f133(f251(f4(a110),f4(a99))))
% 60.56/60.77 [241]P9(a252,f133(f251(f4(a2),f4(a110))))
% 60.56/60.77 [242]P9(a253,f133(f251(f4(a1),f4(a110))))
% 60.56/60.77 [243]P9(a254,f133(f251(f4(a5),f4(a110))))
% 60.56/60.77 [244]P9(a255,f133(f251(f4(a44),f4(a110))))
% 60.56/60.77 [245]P9(a256,f133(f251(f4(a55),f4(a110))))
% 60.56/60.77 [246]P9(a257,f133(f251(f4(a66),f4(a110))))
% 60.56/60.77 [247]P9(a258,f133(f251(f4(a77),f4(a110))))
% 60.56/60.77 [248]P9(a259,f133(f251(f4(a88),f4(a110))))
% 60.56/60.77 [249]P9(a260,f133(f251(f4(a99),f4(a110))))
% 60.56/60.77 [250]P9(a261,f133(f251(f4(a110),f4(a110))))
% 60.56/60.77 [251]P9(a8,f121(f251(f4(a2),f251(f4(a2),f4(a1)))))
% 60.56/60.77 [252]P9(a9,f121(f251(f4(a1),f251(f4(a2),f4(a1)))))
% 60.56/60.77 [253]P9(a10,f121(f251(f4(a5),f251(f4(a2),f4(a1)))))
% 60.56/60.77 [254]P9(a11,f121(f251(f4(a44),f251(f4(a2),f4(a1)))))
% 60.56/60.77 [255]P9(a12,f121(f251(f4(a55),f251(f4(a2),f4(a1)))))
% 60.56/60.77 [256]P9(a13,f121(f251(f4(a66),f251(f4(a2),f4(a1)))))
% 60.56/60.77 [257]P9(a14,f121(f251(f4(a77),f251(f4(a2),f4(a1)))))
% 60.56/60.77 [258]P9(a15,f121(f251(f4(a88),f251(f4(a2),f4(a1)))))
% 60.56/60.77 [259]P9(a16,f121(f251(f4(a99),f251(f4(a2),f4(a1)))))
% 60.56/60.77 [260]P9(a17,f121(f251(f4(a110),f251(f4(a2),f4(a1)))))
% 60.56/60.77 [261]P9(a19,f121(f251(f4(a2),f251(f4(a1),f4(a1)))))
% 60.56/60.77 [262]P9(a20,f121(f251(f4(a1),f251(f4(a1),f4(a1)))))
% 60.56/60.77 [263]P9(a21,f121(f251(f4(a5),f251(f4(a1),f4(a1)))))
% 60.56/60.77 [264]P9(a22,f121(f251(f4(a44),f251(f4(a1),f4(a1)))))
% 60.56/60.77 [265]P9(a23,f121(f251(f4(a55),f251(f4(a1),f4(a1)))))
% 60.56/60.77 [266]P9(a24,f121(f251(f4(a66),f251(f4(a1),f4(a1)))))
% 60.56/60.77 [267]P9(a25,f121(f251(f4(a77),f251(f4(a1),f4(a1)))))
% 60.56/60.77 [268]P9(a26,f121(f251(f4(a88),f251(f4(a1),f4(a1)))))
% 60.56/60.77 [269]P9(a27,f121(f251(f4(a99),f251(f4(a1),f4(a1)))))
% 60.56/60.77 [270]P9(a28,f121(f251(f4(a110),f251(f4(a1),f4(a1)))))
% 60.56/60.77 [271]P9(a30,f121(f251(f4(a2),f251(f4(a5),f4(a1)))))
% 60.56/60.77 [272]P9(a31,f121(f251(f4(a1),f251(f4(a5),f4(a1)))))
% 60.56/60.77 [273]P9(a32,f121(f251(f4(a5),f251(f4(a5),f4(a1)))))
% 60.56/60.77 [274]P9(a33,f121(f251(f4(a44),f251(f4(a5),f4(a1)))))
% 60.56/60.77 [275]P9(a34,f121(f251(f4(a55),f251(f4(a5),f4(a1)))))
% 60.56/60.77 [276]P9(a35,f121(f251(f4(a66),f251(f4(a5),f4(a1)))))
% 60.56/60.77 [277]P9(a36,f121(f251(f4(a77),f251(f4(a5),f4(a1)))))
% 60.56/60.77 [278]P9(a37,f121(f251(f4(a88),f251(f4(a5),f4(a1)))))
% 60.56/60.77 [279]P9(a137,f133(f251(f4(a2),f251(f4(a2),f4(a1)))))
% 60.56/60.77 [280]P9(a138,f133(f251(f4(a1),f251(f4(a2),f4(a1)))))
% 60.56/60.77 [281]P9(a139,f133(f251(f4(a5),f251(f4(a2),f4(a1)))))
% 60.56/60.77 [282]P9(a140,f133(f251(f4(a44),f251(f4(a2),f4(a1)))))
% 60.56/60.77 [283]P9(a141,f133(f251(f4(a55),f251(f4(a2),f4(a1)))))
% 60.56/60.77 [284]P9(a142,f133(f251(f4(a66),f251(f4(a2),f4(a1)))))
% 60.56/60.77 [285]P9(a143,f133(f251(f4(a77),f251(f4(a2),f4(a1)))))
% 60.56/60.77 [286]P9(a144,f133(f251(f4(a88),f251(f4(a2),f4(a1)))))
% 60.56/60.77 [287]P9(a145,f133(f251(f4(a99),f251(f4(a2),f4(a1)))))
% 60.56/60.77 [288]P9(a146,f133(f251(f4(a110),f251(f4(a2),f4(a1)))))
% 60.56/60.77 [289]P9(a148,f133(f251(f4(a2),f251(f4(a1),f4(a1)))))
% 60.56/60.77 [290]P9(a149,f133(f251(f4(a1),f251(f4(a1),f4(a1)))))
% 60.56/60.77 [291]P9(a150,f133(f251(f4(a5),f251(f4(a1),f4(a1)))))
% 60.56/60.77 [292]P9(a151,f133(f251(f4(a44),f251(f4(a1),f4(a1)))))
% 60.56/60.77 [293]P9(a152,f133(f251(f4(a55),f251(f4(a1),f4(a1)))))
% 60.56/60.77 [294]P9(a153,f133(f251(f4(a66),f251(f4(a1),f4(a1)))))
% 60.56/60.77 [295]P9(a154,f133(f251(f4(a77),f251(f4(a1),f4(a1)))))
% 60.56/60.77 [296]P9(a155,f133(f251(f4(a88),f251(f4(a1),f4(a1)))))
% 60.56/60.77 [297]P9(a156,f133(f251(f4(a99),f251(f4(a1),f4(a1)))))
% 60.56/60.77 [298]P9(a157,f133(f251(f4(a110),f251(f4(a1),f4(a1)))))
% 60.56/60.77 [299]P9(a159,f133(f251(f4(a2),f251(f4(a5),f4(a1)))))
% 60.56/60.77 [300]P9(a160,f133(f251(f4(a1),f251(f4(a5),f4(a1)))))
% 60.56/60.77 [301]P9(a161,f133(f251(f4(a5),f251(f4(a5),f4(a1)))))
% 60.56/60.77 [302]P9(a162,f133(f251(f4(a44),f251(f4(a5),f4(a1)))))
% 60.56/60.77 [303]P9(a163,f133(f251(f4(a55),f251(f4(a5),f4(a1)))))
% 60.56/60.77 [304]P9(a164,f133(f251(f4(a66),f251(f4(a5),f4(a1)))))
% 60.56/60.77 [305]P9(a165,f133(f251(f4(a77),f251(f4(a5),f4(a1)))))
% 60.56/60.77 [306]P9(a166,f133(f251(f4(a88),f251(f4(a5),f4(a1)))))
% 60.56/60.77 [307]P9(a167,f133(f251(f4(a99),f251(f4(a5),f4(a1)))))
% 60.56/60.77 [411]P7(f4(x4111))+~P1(f4(x4111))
% 60.56/60.77 [409]~E(x4091,x4092)+P3(x4091,x4092)
% 60.56/60.77 [410]~P4(x4102,x4101)+~E(x4101,x4102)
% 60.56/60.77 [413]~P4(x4131,x4132)+P3(x4131,x4132)
% 60.56/60.77 [415]~P4(x4152,x4151)+~P4(x4151,x4152)
% 60.56/60.77 [416]~P7(x4162)+P7(f251(f4(x4161),x4162))
% 60.56/60.77 [426]~P5(x4263,x4261,x4262)+P10(x4261,x4262,x4263)
% 60.56/60.77 [427]~P10(x4272,x4273,x4271)+P5(x4271,x4272,x4273)
% 60.56/60.77 [417]~P7(x4173)+P8(f4(x4171),f251(f4(x4172),x4173))
% 60.56/60.77 [422]~P8(x4222,x4224)+P8(f251(f4(x4221),x4222),f251(f4(x4223),x4224))
% 60.56/60.77 [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))
% 60.56/60.77 [412]P4(x4122,x4121)+P4(x4121,x4122)+E(x4121,x4122)
% 60.56/60.77 [414]P4(x4141,x4142)+~P3(x4141,x4142)+E(x4141,x4142)
% 60.56/60.77 [424]P3(x4241,x4242)+~P4(x4241,x4243)+~P10(x4242,a1,x4243)
% 60.56/60.77 [421]P8(f4(x4211),f4(x4212))+~P8(f4(x4213),f4(x4212))+~P8(f4(x4211),f4(x4213))
% 60.56/60.77 [423]P10(x4231,x4232,a2)+~P9(x4231,f121(x4233))+~P9(x4232,f133(x4233))
% 60.56/60.77 [425]~P7(x4252)+~P8(f4(x4251),f4(x4253))+P8(f251(f4(x4251),x4252),f251(f4(x4253),x4252))
% 60.56/60.77 [428]~P10(x4283,x4284,x4281)+E(x4281,x4282)+~P10(x4283,x4284,x4282)
% 60.56/60.77 [429]~P10(x4293,x4291,x4294)+E(x4291,x4292)+~P10(x4293,x4292,x4294)
% 60.56/60.77 [430]~P10(x4301,x4303,x4304)+E(x4301,x4302)+~P10(x4302,x4303,x4304)
% 60.56/60.77 [418]P4(x4181,x4182)+~P9(x4182,f121(x4183))+~P9(x4181,f133(x4184))
% 60.56/60.77 [437]P6(f4(x4371),f4(x4372),f4(x4373),f4(x4374))+~P2(f4(x4375),f4(x4371),f4(x4374),f4(a2))+~P2(f4(x4372),f4(x4373),f4(x4375),f4(a2))
% 60.56/60.77 [419]P4(x4191,x4192)+~P8(x4193,x4194)+~P9(x4192,f133(x4193))+~P9(x4191,f133(x4194))
% 60.56/60.77 [420]P4(x4201,x4202)+~P8(x4203,x4204)+~P9(x4202,f121(x4204))+~P9(x4201,f121(x4203))
% 60.56/60.77 [431]~P10(x4312,x4311,x4313)+P10(x4311,x4312,x4313)+~P9(x4312,f121(x4314))+~P9(x4311,f133(x4315))
% 60.56/60.77 [438]~P2(f4(x4385),f4(x4381),f4(x4384),f4(x4386))+~P2(f4(x4382),f4(x4383),f4(x4385),f4(x4387))+~P2(f4(x4387),f4(x4386),f4(a1),f4(a2))+P6(f4(x4381),f4(x4382),f4(x4383),f251(f4(x4384),f4(a1)))
% 60.56/60.77 [432]P10(x4321,x4322,x4323)+~P6(f4(a2),x4326,x4325,x4324)+~P9(x4323,f121(x4324))+~P9(x4322,f121(x4325))+~P9(x4321,f121(x4326))
% 60.56/60.77 [433]P10(x4331,x4332,x4333)+~P6(f4(a2),x4336,x4335,x4334)+~P9(x4333,f133(x4334))+~P9(x4332,f133(x4335))+~P9(x4331,f133(x4336))
% 60.56/60.77 [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))
% 60.56/60.77 [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))
% 60.56/60.77 [439]~P7(x4396)+~P7(x4394)+~P2(f4(x4398),f4(x4391),f4(x4395),f4(x4399))+~P2(f4(x4392),f4(x4393),f4(x4398),f4(x43910))+~P6(f4(x4397),f4(a2),x4394,x4396)+~P2(f4(x43910),f4(x4399),f4(x4397),f4(a2))+P6(f4(x4391),f4(x4392),f251(f4(x4393),x4394),f251(f4(x4395),x4396))
% 60.56/60.77 [440]~P7(x4407)+~P7(x4405)+~P7(x4403)+~P6(f4(x4408),x4403,x4405,x4407)+~P2(f4(x4409),f4(x4401),f4(x4406),f4(x44010))+~P2(f4(x4402),f4(x4404),f4(x4409),f4(x44011))+~P2(f4(x44011),f4(x44010),f4(x4408),f4(a2))+P6(f4(x4401),f251(f4(x4402),x4403),f251(f4(x4404),x4405),f251(f4(x4406),x4407))
% 60.56/60.77 %EqnAxiom
% 60.56/60.77 [1]E(x11,x11)
% 60.56/60.77 [2]E(x22,x21)+~E(x21,x22)
% 60.56/60.77 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 60.56/60.77 [4]~E(x41,x42)+E(f4(x41),f4(x42))
% 60.56/60.77 [5]~E(x51,x52)+E(f251(x51,x53),f251(x52,x53))
% 60.56/60.77 [6]~E(x61,x62)+E(f251(x63,x61),f251(x63,x62))
% 60.56/60.77 [7]~E(x71,x72)+E(f133(x71),f133(x72))
% 60.56/60.77 [8]~E(x81,x82)+E(f121(x81),f121(x82))
% 60.56/60.77 [9]~P1(x91)+P1(x92)+~E(x91,x92)
% 60.56/60.77 [10]P2(x102,x103,x104,x105)+~E(x101,x102)+~P2(x101,x103,x104,x105)
% 60.56/60.77 [11]P2(x113,x112,x114,x115)+~E(x111,x112)+~P2(x113,x111,x114,x115)
% 60.56/60.77 [12]P2(x123,x124,x122,x125)+~E(x121,x122)+~P2(x123,x124,x121,x125)
% 60.56/60.77 [13]P2(x133,x134,x135,x132)+~E(x131,x132)+~P2(x133,x134,x135,x131)
% 60.56/60.77 [14]P6(x142,x143,x144,x145)+~E(x141,x142)+~P6(x141,x143,x144,x145)
% 60.56/60.77 [15]P6(x153,x152,x154,x155)+~E(x151,x152)+~P6(x153,x151,x154,x155)
% 60.56/60.77 [16]P6(x163,x164,x162,x165)+~E(x161,x162)+~P6(x163,x164,x161,x165)
% 60.56/60.77 [17]P6(x173,x174,x175,x172)+~E(x171,x172)+~P6(x173,x174,x175,x171)
% 60.56/60.77 [18]~P7(x181)+P7(x182)+~E(x181,x182)
% 60.56/60.77 [19]P3(x192,x193)+~E(x191,x192)+~P3(x191,x193)
% 60.56/60.77 [20]P3(x203,x202)+~E(x201,x202)+~P3(x203,x201)
% 60.56/60.77 [21]P8(x212,x213)+~E(x211,x212)+~P8(x211,x213)
% 60.56/60.77 [22]P8(x223,x222)+~E(x221,x222)+~P8(x223,x221)
% 60.56/60.77 [23]P4(x232,x233)+~E(x231,x232)+~P4(x231,x233)
% 60.56/60.77 [24]P4(x243,x242)+~E(x241,x242)+~P4(x243,x241)
% 60.56/60.77 [25]P9(x252,x253)+~E(x251,x252)+~P9(x251,x253)
% 60.56/60.77 [26]P9(x263,x262)+~E(x261,x262)+~P9(x263,x261)
% 60.56/60.77 [27]P10(x272,x273,x274)+~E(x271,x272)+~P10(x271,x273,x274)
% 60.56/60.77 [28]P10(x283,x282,x284)+~E(x281,x282)+~P10(x283,x281,x284)
% 60.56/60.77 [29]P10(x293,x294,x292)+~E(x291,x292)+~P10(x293,x294,x291)
% 60.56/60.77 [30]P5(x302,x303,x304)+~E(x301,x302)+~P5(x301,x303,x304)
% 60.56/60.77 [31]P5(x313,x312,x314)+~E(x311,x312)+~P5(x313,x311,x314)
% 60.56/60.77 [32]P5(x323,x324,x322)+~E(x321,x322)+~P5(x323,x324,x321)
% 60.56/60.77
% 60.56/60.77 %-------------------------------------------
% 60.56/60.77 cnf(441,plain,
% 60.56/60.77 (P3(x4411,x4411)),
% 60.56/60.77 inference(equality_inference,[],[409])).
% 60.56/60.77 cnf(442,plain,
% 60.56/60.77 (~P4(x4421,x4421)),
% 60.56/60.77 inference(equality_inference,[],[410])).
% 60.56/60.77 cnf(443,plain,
% 60.56/60.77 (P10(a1,a122,a2)),
% 60.56/60.77 inference(scs_inference,[],[52,61,423])).
% 60.56/60.77 cnf(449,plain,
% 60.56/60.77 (~E(a122,a2)),
% 60.56/60.77 inference(scs_inference,[],[442,308,51,52,61,423,418,437,23])).
% 60.56/60.77 cnf(450,plain,
% 60.56/60.77 (~P4(x4501,x4501)),
% 60.56/60.77 inference(rename_variables,[],[442])).
% 60.56/60.77 cnf(452,plain,
% 60.56/60.77 (~P4(x4521,x4521)),
% 60.56/60.77 inference(rename_variables,[],[442])).
% 60.56/60.77 cnf(453,plain,
% 60.56/60.77 (P10(a122,a1,a2)),
% 60.56/60.77 inference(scs_inference,[],[442,450,308,51,52,61,423,418,437,23,24,431])).
% 60.56/60.77 cnf(455,plain,
% 60.56/60.77 (~P8(f4(a1),f4(a1))),
% 60.56/60.77 inference(scs_inference,[],[442,450,452,308,51,52,61,423,418,437,23,24,431,419])).
% 60.56/60.77 cnf(456,plain,
% 60.56/60.77 (~P4(x4561,x4561)),
% 60.56/60.77 inference(rename_variables,[],[442])).
% 60.56/60.77 cnf(461,plain,
% 60.56/60.77 (P10(a2,a2,a2)),
% 60.56/60.77 inference(scs_inference,[],[442,450,452,456,308,51,52,61,423,418,437,23,24,431,419,420,432])).
% 60.56/60.77 cnf(466,plain,
% 60.56/60.77 (~P8(f4(a1),f4(a2))),
% 60.56/60.77 inference(scs_inference,[],[70,442,450,452,456,308,42,51,52,61,423,418,437,23,24,431,419,420,432,415,27,421])).
% 60.56/60.77 cnf(469,plain,
% 60.56/60.77 (~E(f4(a1),f4(a2))),
% 60.56/60.77 inference(scs_inference,[],[70,442,450,452,456,308,42,51,52,61,423,418,437,23,24,431,419,420,432,415,27,421,21,22])).
% 60.56/60.77 cnf(474,plain,
% 60.56/60.77 (~E(a1,a2)),
% 60.56/60.77 inference(scs_inference,[],[469,4])).
% 60.56/60.77 cnf(475,plain,
% 60.56/60.77 (P4(a134,a5)),
% 60.56/60.77 inference(scs_inference,[],[469,53,62,4,418])).
% 60.56/60.77 cnf(478,plain,
% 60.56/60.77 (~P4(x4781,x4781)),
% 60.56/60.77 inference(rename_variables,[],[442])).
% 60.56/60.77 cnf(480,plain,
% 60.56/60.77 (~P4(x4801,x4801)),
% 60.56/60.77 inference(rename_variables,[],[442])).
% 60.56/60.77 cnf(481,plain,
% 60.56/60.77 (~P8(f4(a5),f4(a2))),
% 60.56/60.77 inference(scs_inference,[],[442,478,466,469,43,53,62,4,418,24,23,421])).
% 60.56/60.77 cnf(485,plain,
% 60.56/60.77 (P10(a5,a134,a2)),
% 60.56/60.77 inference(scs_inference,[],[442,478,466,469,309,43,53,62,308,4,418,24,23,421,437,423])).
% 60.56/60.77 cnf(487,plain,
% 60.56/60.77 (~E(f4(a5),f4(a1))),
% 60.56/60.77 inference(scs_inference,[],[442,478,455,466,469,309,43,53,62,308,4,418,24,23,421,437,423,22])).
% 60.56/60.77 cnf(488,plain,
% 60.56/60.77 (P10(a134,a5,a2)),
% 60.56/60.77 inference(scs_inference,[],[442,478,455,466,469,309,43,53,62,308,4,418,24,23,421,437,423,22,431])).
% 60.56/60.77 cnf(490,plain,
% 60.56/60.77 (~P8(f4(a5),f4(a5))),
% 60.56/60.77 inference(scs_inference,[],[442,478,480,455,466,469,309,43,53,62,308,4,418,24,23,421,437,423,22,431,419])).
% 60.56/60.77 cnf(491,plain,
% 60.56/60.77 (~P4(x4911,x4911)),
% 60.56/60.77 inference(rename_variables,[],[442])).
% 60.56/60.77 cnf(493,plain,
% 60.56/60.77 (~P8(f4(a44),f4(a44))),
% 60.56/60.77 inference(scs_inference,[],[442,478,480,491,455,466,469,309,43,53,54,62,308,4,418,24,23,421,437,423,22,431,419,420])).
% 60.56/60.77 cnf(499,plain,
% 60.56/60.77 (~E(f4(a1),f4(a5))),
% 60.56/60.77 inference(scs_inference,[],[442,478,480,491,455,466,469,309,43,53,54,62,308,4,418,24,23,421,437,423,22,431,419,420,415,13,21])).
% 60.56/60.77 cnf(511,plain,
% 60.56/60.77 (~E(a5,a1)),
% 60.56/60.77 inference(scs_inference,[],[487,4])).
% 60.56/60.77 cnf(512,plain,
% 60.56/60.77 (P4(a174,a2)),
% 60.56/60.77 inference(scs_inference,[],[51,487,63,4,418])).
% 60.56/60.77 cnf(514,plain,
% 60.56/60.77 (~P8(f4(a5),f4(a1))),
% 60.56/60.77 inference(scs_inference,[],[51,490,487,63,43,4,418,421])).
% 60.56/60.77 cnf(519,plain,
% 60.56/60.77 (~P4(x5191,x5191)),
% 60.56/60.77 inference(rename_variables,[],[442])).
% 60.56/60.77 cnf(520,plain,
% 60.56/60.77 (P10(a44,a174,a2)),
% 60.56/60.77 inference(scs_inference,[],[442,51,490,487,310,63,54,43,308,4,418,421,437,23,423])).
% 60.56/60.77 cnf(523,plain,
% 60.56/60.77 (~P4(x5231,x5231)),
% 60.56/60.77 inference(rename_variables,[],[442])).
% 60.56/60.77 cnf(524,plain,
% 60.56/60.77 (~E(f4(a5),f4(a44))),
% 60.56/60.77 inference(scs_inference,[],[442,519,51,490,487,493,310,44,63,54,43,308,4,418,421,437,23,423,24,21])).
% 60.56/60.77 cnf(525,plain,
% 60.56/60.77 (~E(f4(a44),f4(a5))),
% 60.56/60.77 inference(scs_inference,[],[442,519,51,490,487,493,310,44,63,54,43,308,4,418,421,437,23,423,24,21,22])).
% 60.56/60.77 cnf(526,plain,
% 60.56/60.77 (~P8(f4(a55),f4(a55))),
% 60.56/60.77 inference(scs_inference,[],[442,519,523,51,490,487,493,310,44,63,64,54,43,308,4,418,421,437,23,423,24,21,22,419])).
% 60.56/60.77 cnf(527,plain,
% 60.56/60.77 (~P4(x5271,x5271)),
% 60.56/60.77 inference(rename_variables,[],[442])).
% 60.56/60.77 cnf(529,plain,
% 60.56/60.77 (P10(a174,a44,a2)),
% 60.56/60.77 inference(scs_inference,[],[442,519,523,51,490,487,493,310,44,63,64,54,43,308,4,418,421,437,23,423,24,21,22,419,431])).
% 60.56/60.77 cnf(531,plain,
% 60.56/60.77 (~P8(f4(a66),f4(a66))),
% 60.56/60.77 inference(scs_inference,[],[442,519,523,527,51,490,487,493,310,44,56,63,64,54,43,308,4,418,421,437,23,423,24,21,22,419,431,420])).
% 60.56/60.77 cnf(536,plain,
% 60.56/60.77 (P9(x5361,f121(f4(a2)))+~E(a2,x5361)),
% 60.56/60.77 inference(scs_inference,[],[442,519,523,527,51,490,487,493,310,44,56,63,64,54,43,308,4,418,421,437,23,423,24,21,22,419,431,420,415,25])).
% 60.56/60.77 cnf(543,plain,
% 60.56/60.77 (P4(a196,a2)),
% 60.56/60.77 inference(scs_inference,[],[51,499,65,4,418])).
% 60.56/60.77 cnf(547,plain,
% 60.56/60.77 (~P8(f4(a55),f4(a44))),
% 60.56/60.77 inference(scs_inference,[],[51,526,499,311,45,65,308,4,418,437,421])).
% 60.56/60.77 cnf(549,plain,
% 60.56/60.77 (P10(a66,a196,a2)),
% 60.56/60.77 inference(scs_inference,[],[51,526,499,311,45,65,56,308,4,418,437,421,423])).
% 60.56/60.77 cnf(552,plain,
% 60.56/60.77 (~P4(x5521,x5521)),
% 60.56/60.77 inference(rename_variables,[],[442])).
% 60.56/60.77 cnf(554,plain,
% 60.56/60.77 (~P4(x5541,x5541)),
% 60.56/60.77 inference(rename_variables,[],[442])).
% 60.56/60.77 cnf(555,plain,
% 60.56/60.77 (~E(f4(a55),f4(a44))),
% 60.56/60.77 inference(scs_inference,[],[442,552,51,526,499,311,45,65,493,56,308,4,418,437,421,423,23,24,22])).
% 60.56/60.77 cnf(556,plain,
% 60.56/60.77 (~E(f4(a44),f4(a55))),
% 60.56/60.77 inference(scs_inference,[],[442,552,51,526,499,311,45,65,493,56,308,4,418,437,421,423,23,24,22,21])).
% 60.56/60.77 cnf(557,plain,
% 60.56/60.77 (~P8(f4(a77),f4(a77))),
% 60.56/60.77 inference(scs_inference,[],[442,552,554,51,526,499,311,45,65,66,493,56,308,4,418,437,421,423,23,24,22,21,419])).
% 60.56/60.77 cnf(558,plain,
% 60.56/60.77 (~P4(x5581,x5581)),
% 60.56/60.77 inference(rename_variables,[],[442])).
% 60.56/60.77 cnf(560,plain,
% 60.56/60.77 (P10(a196,a66,a2)),
% 60.56/60.77 inference(scs_inference,[],[442,552,554,51,526,499,311,45,65,66,493,56,308,4,418,437,421,423,23,24,22,21,419,431])).
% 60.56/60.77 cnf(562,plain,
% 60.56/60.77 (~P8(f4(a88),f4(a88))),
% 60.56/60.77 inference(scs_inference,[],[442,552,554,558,51,526,499,311,45,58,65,66,493,56,308,4,418,437,421,423,23,24,22,21,419,431,420])).
% 60.56/60.77 cnf(570,plain,
% 60.56/60.77 (P9(x5701,f121(f4(a66)))+~E(a66,x5701)),
% 60.56/60.77 inference(scs_inference,[],[70,442,552,554,558,51,526,499,311,45,58,65,66,493,56,308,4,418,437,421,423,23,24,22,21,419,431,420,415,29,428,25])).
% 60.56/60.77 cnf(581,plain,
% 60.56/60.77 (~E(a5,a44)),
% 60.56/60.77 inference(scs_inference,[],[524,4])).
% 60.56/60.77 cnf(582,plain,
% 60.56/60.77 (P4(a218,a2)),
% 60.56/60.77 inference(scs_inference,[],[51,524,67,4,418])).
% 60.56/60.77 cnf(584,plain,
% 60.56/60.77 (~P8(f4(a66),f4(a55))),
% 60.56/60.77 inference(scs_inference,[],[51,531,524,46,67,4,418,421])).
% 60.56/60.77 cnf(586,plain,
% 60.56/60.77 (P10(a88,a218,a2)),
% 60.56/60.77 inference(scs_inference,[],[51,531,524,46,67,58,4,418,421,423])).
% 60.56/60.77 cnf(588,plain,
% 60.56/60.77 (P6(f4(a55),f4(a2),f4(a2),f4(a55))),
% 60.56/60.77 inference(scs_inference,[],[51,531,524,312,46,67,58,308,4,418,421,423,437])).
% 60.56/60.77 cnf(591,plain,
% 60.56/60.77 (~P4(x5911,x5911)),
% 60.56/60.77 inference(rename_variables,[],[442])).
% 60.56/60.77 cnf(592,plain,
% 60.56/60.77 (~E(a2,a218)),
% 60.56/60.77 inference(scs_inference,[],[442,591,51,531,524,312,46,67,58,308,4,418,421,423,437,23,24])).
% 60.56/60.77 cnf(593,plain,
% 60.56/60.77 (~P4(x5931,x5931)),
% 60.56/60.77 inference(rename_variables,[],[442])).
% 60.56/60.77 cnf(594,plain,
% 60.56/60.77 (~E(f4(a55),f4(a66))),
% 60.56/60.77 inference(scs_inference,[],[442,591,51,531,524,312,46,67,58,308,4,418,421,423,437,23,24,21])).
% 60.56/60.77 cnf(595,plain,
% 60.56/60.77 (~E(f4(a66),f4(a44))),
% 60.56/60.77 inference(scs_inference,[],[442,591,51,531,524,547,312,46,67,58,308,4,418,421,423,437,23,24,21,22])).
% 60.56/60.77 cnf(596,plain,
% 60.56/60.77 (~P8(f4(a99),f4(a99))),
% 60.56/60.77 inference(scs_inference,[],[442,591,593,51,531,524,547,312,46,67,68,58,308,4,418,421,423,437,23,24,21,22,419])).
% 60.56/60.77 cnf(597,plain,
% 60.56/60.77 (~P4(x5971,x5971)),
% 60.56/60.77 inference(rename_variables,[],[442])).
% 60.56/60.77 cnf(599,plain,
% 60.56/60.77 (P10(a218,a88,a2)),
% 60.56/60.77 inference(scs_inference,[],[442,591,593,51,531,524,547,312,46,67,68,58,308,4,418,421,423,437,23,24,21,22,419,431])).
% 60.56/60.77 cnf(601,plain,
% 60.56/60.77 (~P8(f4(a110),f4(a110))),
% 60.56/60.77 inference(scs_inference,[],[442,591,593,597,51,531,524,547,312,46,60,67,68,58,308,4,418,421,423,437,23,24,21,22,419,431,420])).
% 60.56/60.77 cnf(604,plain,
% 60.56/60.77 (~P4(a2,a218)),
% 60.56/60.77 inference(scs_inference,[],[442,591,593,597,51,531,524,547,312,46,60,67,68,58,308,4,418,421,423,437,23,24,21,22,419,431,420,415])).
% 60.56/60.77 cnf(618,plain,
% 60.56/60.77 (~E(a44,a5)),
% 60.56/60.77 inference(scs_inference,[],[525,4])).
% 60.56/60.77 cnf(619,plain,
% 60.56/60.77 (P4(a240,a2)),
% 60.56/60.77 inference(scs_inference,[],[51,525,69,4,418])).
% 60.56/60.77 cnf(621,plain,
% 60.56/60.77 (P10(a110,a240,a2)),
% 60.56/60.77 inference(scs_inference,[],[51,525,69,60,4,418,423])).
% 60.56/60.77 cnf(623,plain,
% 60.56/60.77 (P6(f4(a66),f4(a2),f4(a2),f4(a66))),
% 60.56/60.77 inference(scs_inference,[],[51,525,313,69,60,308,4,418,423,437])).
% 60.56/60.77 cnf(625,plain,
% 60.56/60.77 (~P8(f4(a77),f4(a66))),
% 60.56/60.77 inference(scs_inference,[],[51,557,525,313,47,69,60,308,4,418,423,437,421])).
% 60.56/60.77 cnf(628,plain,
% 60.56/60.77 (~P4(x6281,x6281)),
% 60.56/60.77 inference(rename_variables,[],[442])).
% 60.56/60.77 cnf(629,plain,
% 60.56/60.77 (~E(a2,a240)),
% 60.56/60.77 inference(scs_inference,[],[442,628,51,557,525,313,47,69,60,308,4,418,423,437,421,23,24])).
% 60.56/60.77 cnf(630,plain,
% 60.56/60.77 (~P4(x6301,x6301)),
% 60.56/60.77 inference(rename_variables,[],[442])).
% 60.56/60.77 cnf(631,plain,
% 60.56/60.77 (~E(f4(a77),f4(a55))),
% 60.56/60.77 inference(scs_inference,[],[442,628,51,557,525,584,313,47,69,60,308,4,418,423,437,421,23,24,22])).
% 60.56/60.77 cnf(632,plain,
% 60.56/60.77 (~E(f4(a66),f4(a77))),
% 60.56/60.77 inference(scs_inference,[],[442,628,51,557,525,584,313,47,69,60,308,4,418,423,437,421,23,24,22,21])).
% 60.56/60.77 cnf(634,plain,
% 60.56/60.77 (~P4(x6341,x6341)),
% 60.56/60.77 inference(rename_variables,[],[442])).
% 60.56/60.77 cnf(636,plain,
% 60.56/60.77 (P10(a240,a110,a2)),
% 60.56/60.77 inference(scs_inference,[],[442,628,630,51,557,525,584,313,47,69,161,60,308,4,418,423,437,421,23,24,22,21,419,431])).
% 60.56/60.77 cnf(641,plain,
% 60.56/60.77 (~P4(a2,a240)),
% 60.56/60.77 inference(scs_inference,[],[442,628,630,634,51,557,525,584,313,47,69,161,72,60,308,4,418,423,437,421,23,24,22,21,419,431,420,415])).
% 60.56/60.77 cnf(655,plain,
% 60.56/60.77 (~E(a55,a44)),
% 60.56/60.77 inference(scs_inference,[],[555,4])).
% 60.56/60.77 cnf(656,plain,
% 60.56/60.77 (P4(a136,a2)),
% 60.56/60.77 inference(scs_inference,[],[51,555,162,4,418])).
% 60.56/60.77 cnf(662,plain,
% 60.56/60.77 (~P8(f4(a99),f4(a88))),
% 60.56/60.77 inference(scs_inference,[],[51,596,555,314,49,162,72,308,4,418,423,437,421])).
% 60.56/60.77 cnf(665,plain,
% 60.56/60.78 (~P4(x6651,x6651)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(667,plain,
% 60.56/60.78 (~P4(x6671,x6671)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(668,plain,
% 60.56/60.78 (~E(f4(a88),f4(a66))),
% 60.56/60.78 inference(scs_inference,[],[442,665,51,596,555,625,314,48,49,162,72,308,4,418,423,437,421,23,24,22])).
% 60.56/60.78 cnf(669,plain,
% 60.56/60.78 (~E(f4(a77),f4(a88))),
% 60.56/60.78 inference(scs_inference,[],[442,665,51,596,562,555,625,314,48,49,162,72,308,4,418,423,437,421,23,24,22,21])).
% 60.56/60.78 cnf(671,plain,
% 60.56/60.78 (~P4(x6711,x6711)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(683,plain,
% 60.56/60.78 (P9(x6831,f121(f4(a77)))+~E(a77,x6831)),
% 60.56/60.78 inference(scs_inference,[],[442,665,667,671,51,596,562,555,625,314,48,49,57,162,163,74,72,308,4,418,423,437,421,23,24,22,21,419,431,420,415,13,11,10,25])).
% 60.56/60.78 cnf(685,plain,
% 60.56/60.78 (P10(a3,x6851,a66)+~E(a44,x6851)),
% 60.56/60.78 inference(scs_inference,[],[70,442,665,667,671,51,596,562,555,588,625,314,48,49,57,162,163,74,72,308,4,418,423,437,421,23,24,22,21,419,431,420,415,13,11,10,25,17,28])).
% 60.56/60.78 cnf(693,plain,
% 60.56/60.78 (P4(a158,a2)),
% 60.56/60.78 inference(scs_inference,[],[51,556,164,4,418])).
% 60.56/60.78 cnf(697,plain,
% 60.56/60.78 (P6(f4(a88),f4(a2),f4(a2),f4(a88))),
% 60.56/60.78 inference(scs_inference,[],[51,556,315,164,74,308,4,418,423,437])).
% 60.56/60.78 cnf(699,plain,
% 60.56/60.78 (~P8(f4(a110),f4(a99))),
% 60.56/60.78 inference(scs_inference,[],[51,601,556,315,50,164,74,308,4,418,423,437,421])).
% 60.56/60.78 cnf(702,plain,
% 60.56/60.78 (~P4(x7021,x7021)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(704,plain,
% 60.56/60.78 (~P4(x7041,x7041)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(705,plain,
% 60.56/60.78 (~E(f4(a110),f4(a88))),
% 60.56/60.78 inference(scs_inference,[],[442,702,51,601,556,662,315,50,164,74,308,4,418,423,437,421,23,24,22])).
% 60.56/60.78 cnf(706,plain,
% 60.56/60.78 (~E(f4(a99),f4(a110))),
% 60.56/60.78 inference(scs_inference,[],[442,702,51,601,556,662,315,50,164,74,308,4,418,423,437,421,23,24,22,21])).
% 60.56/60.78 cnf(708,plain,
% 60.56/60.78 (~P4(x7081,x7081)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(719,plain,
% 60.56/60.78 (P10(x7191,a1,a2)+~E(a122,x7191)),
% 60.56/60.78 inference(scs_inference,[],[453,442,702,704,708,51,601,556,623,662,315,50,164,165,76,74,308,4,418,423,437,421,23,24,22,21,419,431,420,415,12,16,27])).
% 60.56/60.78 cnf(730,plain,
% 60.56/60.78 (P4(a169,a2)),
% 60.56/60.78 inference(scs_inference,[],[51,594,166,4,418])).
% 60.56/60.78 cnf(736,plain,
% 60.56/60.78 (~P8(f4(a44),f4(a2))),
% 60.56/60.78 inference(scs_inference,[],[51,481,594,316,166,76,44,308,4,418,423,437,421])).
% 60.56/60.78 cnf(739,plain,
% 60.56/60.78 (~P4(x7391,x7391)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(742,plain,
% 60.56/60.78 (~E(f4(a99),f4(a88))),
% 60.56/60.78 inference(scs_inference,[],[442,739,51,481,594,316,166,562,49,76,44,308,4,418,423,437,421,23,24,22])).
% 60.56/60.78 cnf(743,plain,
% 60.56/60.78 (~E(f4(a88),f4(a110))),
% 60.56/60.78 inference(scs_inference,[],[442,739,51,481,594,699,316,166,562,49,76,44,308,4,418,423,437,421,23,24,22,21])).
% 60.56/60.78 cnf(758,plain,
% 60.56/60.78 (~E(a66,a44)),
% 60.56/60.78 inference(scs_inference,[],[595,4])).
% 60.56/60.78 cnf(759,plain,
% 60.56/60.78 (P4(a171,a2)),
% 60.56/60.78 inference(scs_inference,[],[51,595,168,4,418])).
% 60.56/60.78 cnf(761,plain,
% 60.56/60.78 (P6(f4(a110),f4(a2),f4(a2),f4(a110))),
% 60.56/60.78 inference(scs_inference,[],[51,595,317,168,308,4,418,437])).
% 60.56/60.78 cnf(765,plain,
% 60.56/60.78 (~P8(f4(a55),f4(a2))),
% 60.56/60.78 inference(scs_inference,[],[51,595,736,317,168,78,45,308,4,418,437,423,421])).
% 60.56/60.78 cnf(768,plain,
% 60.56/60.78 (~P4(x7681,x7681)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(770,plain,
% 60.56/60.78 (~P4(x7701,x7701)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(771,plain,
% 60.56/60.78 (~E(f4(a44),f4(a1))),
% 60.56/60.78 inference(scs_inference,[],[442,768,51,514,595,736,317,168,78,44,45,308,4,418,437,423,421,23,24,22])).
% 60.56/60.78 cnf(772,plain,
% 60.56/60.78 (~E(f4(a77),f4(a99))),
% 60.56/60.78 inference(scs_inference,[],[442,768,51,514,595,736,317,168,662,78,48,44,45,308,4,418,437,423,421,23,24,22,21])).
% 60.56/60.78 cnf(774,plain,
% 60.56/60.78 (~P4(x7741,x7741)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(786,plain,
% 60.56/60.78 (P10(x7861,a5,a2)+~E(a134,x7861)),
% 60.56/60.78 inference(scs_inference,[],[488,442,768,770,774,51,514,595,697,736,317,168,169,80,662,78,48,44,45,308,4,418,437,423,421,23,24,22,21,419,431,420,415,15,12,25,27])).
% 60.56/60.78 cnf(796,plain,
% 60.56/60.78 (P4(a173,a2)),
% 60.56/60.78 inference(scs_inference,[],[51,668,170,4,418])).
% 60.56/60.78 cnf(800,plain,
% 60.56/60.78 (P6(f4(a2),f4(a1),f4(a2),f4(a1))),
% 60.56/60.78 inference(scs_inference,[],[51,668,318,170,80,4,418,423,437])).
% 60.56/60.78 cnf(802,plain,
% 60.56/60.78 (~P8(f4(a66),f4(a2))),
% 60.56/60.78 inference(scs_inference,[],[51,668,765,318,170,80,46,4,418,423,437,421])).
% 60.56/60.78 cnf(805,plain,
% 60.56/60.78 (~P4(x8051,x8051)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(808,plain,
% 60.56/60.78 (~E(f4(a66),f4(a2))),
% 60.56/60.78 inference(scs_inference,[],[442,805,51,668,765,318,170,80,46,4,418,423,437,421,23,24,22])).
% 60.56/60.78 cnf(809,plain,
% 60.56/60.78 (~E(f4(a55),f4(a77))),
% 60.56/60.78 inference(scs_inference,[],[442,805,51,668,765,318,170,625,80,46,4,418,423,437,421,23,24,22,21])).
% 60.56/60.78 cnf(826,plain,
% 60.56/60.78 (P4(a176,a2)),
% 60.56/60.78 inference(scs_inference,[],[51,631,172,4,418])).
% 60.56/60.78 cnf(832,plain,
% 60.56/60.78 (~P8(f4(a77),f4(a2))),
% 60.56/60.78 inference(scs_inference,[],[51,631,802,319,172,318,82,47,4,418,437,423,421])).
% 60.56/60.78 cnf(835,plain,
% 60.56/60.78 (~P4(x8351,x8351)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(837,plain,
% 60.56/60.78 (~P4(x8371,x8371)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(838,plain,
% 60.56/60.78 (~E(f4(a77),f4(a2))),
% 60.56/60.78 inference(scs_inference,[],[442,835,51,631,802,319,172,318,82,47,4,418,437,423,421,23,24,22])).
% 60.56/60.78 cnf(839,plain,
% 60.56/60.78 (~E(f4(a88),f4(a99))),
% 60.56/60.78 inference(scs_inference,[],[442,835,51,631,802,319,172,596,318,82,47,49,4,418,437,423,421,23,24,22,21])).
% 60.56/60.78 cnf(841,plain,
% 60.56/60.78 (~P4(x8411,x8411)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(855,plain,
% 60.56/60.78 (P10(a122,x8551,a2)+~E(a1,x8551)),
% 60.56/60.78 inference(scs_inference,[],[453,442,835,837,841,51,631,761,802,319,172,173,84,596,318,82,47,49,4,418,437,423,421,23,24,22,21,419,431,420,415,12,13,15,14,17,28])).
% 60.56/60.78 cnf(862,plain,
% 60.56/60.78 (~E(a66,a77)),
% 60.56/60.78 inference(scs_inference,[],[632,4])).
% 60.56/60.78 cnf(863,plain,
% 60.56/60.78 (P4(a178,a2)),
% 60.56/60.78 inference(scs_inference,[],[51,632,174,4,418])).
% 60.56/60.78 cnf(869,plain,
% 60.56/60.78 (~P8(f4(a88),f4(a2))),
% 60.56/60.78 inference(scs_inference,[],[51,632,832,320,174,84,309,48,4,418,423,437,421])).
% 60.56/60.78 cnf(872,plain,
% 60.56/60.78 (~P4(x8721,x8721)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(874,plain,
% 60.56/60.78 (~P4(x8741,x8741)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(875,plain,
% 60.56/60.78 (~E(f4(a88),f4(a2))),
% 60.56/60.78 inference(scs_inference,[],[442,872,51,632,832,320,174,84,309,48,4,418,423,437,421,23,24,22])).
% 60.56/60.78 cnf(876,plain,
% 60.56/60.78 (~E(f4(a5),f4(a55))),
% 60.56/60.78 inference(scs_inference,[],[442,872,51,632,832,320,174,547,84,309,48,44,4,418,423,437,421,23,24,22,21])).
% 60.56/60.78 cnf(880,plain,
% 60.56/60.78 (~P4(x8801,x8801)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(890,plain,
% 60.56/60.78 (P10(x8901,a44,a2)+~E(a174,x8901)),
% 60.56/60.78 inference(scs_inference,[],[529,442,872,874,880,51,632,832,320,174,175,86,547,84,309,48,44,4,418,423,437,421,23,24,22,21,431,419,420,415,25,10,29,27])).
% 60.56/60.78 cnf(899,plain,
% 60.56/60.78 (~E(a77,a88)),
% 60.56/60.78 inference(scs_inference,[],[669,4])).
% 60.56/60.78 cnf(900,plain,
% 60.56/60.78 (P4(a180,a2)),
% 60.56/60.78 inference(scs_inference,[],[51,669,176,4,418])).
% 60.56/60.78 cnf(904,plain,
% 60.56/60.78 (P10(a50,a180,a2)),
% 60.56/60.78 inference(scs_inference,[],[51,669,321,176,86,318,4,418,437,423])).
% 60.56/60.78 cnf(906,plain,
% 60.56/60.78 (~P8(f4(a99),f4(a2))),
% 60.56/60.78 inference(scs_inference,[],[51,669,869,321,176,86,318,49,4,418,437,423,421])).
% 60.56/60.78 cnf(908,plain,
% 60.56/60.78 (~E(a2,a180)),
% 60.56/60.78 inference(scs_inference,[],[442,51,669,869,321,176,86,318,49,4,418,437,423,421,24])).
% 60.56/60.78 cnf(909,plain,
% 60.56/60.78 (~P4(x9091,x9091)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(911,plain,
% 60.56/60.78 (~P4(x9111,x9111)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(915,plain,
% 60.56/60.78 (~P4(x9151,x9151)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(928,plain,
% 60.56/60.78 (P10(a218,x9281,a2)+~E(a88,x9281)),
% 60.56/60.78 inference(scs_inference,[],[599,442,909,911,915,51,669,800,869,321,176,177,88,584,86,596,318,50,45,49,4,418,437,423,421,24,23,22,21,419,431,420,415,12,11,15,16,28])).
% 60.56/60.78 cnf(936,plain,
% 60.56/60.78 (~E(a99,a110)),
% 60.56/60.78 inference(scs_inference,[],[706,4])).
% 60.56/60.78 cnf(937,plain,
% 60.56/60.78 (P10(a52,a182,a2)),
% 60.56/60.78 inference(scs_inference,[],[706,178,88,4,423])).
% 60.56/60.78 cnf(941,plain,
% 60.56/60.78 (P4(a182,a2)),
% 60.56/60.78 inference(scs_inference,[],[51,706,322,178,88,309,4,423,437,418])).
% 60.56/60.78 cnf(946,plain,
% 60.56/60.78 (~P4(x9461,x9461)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(947,plain,
% 60.56/60.78 (~E(a2,a182)),
% 60.56/60.78 inference(scs_inference,[],[442,946,51,706,906,322,178,88,309,50,4,423,437,418,421,23,24])).
% 60.56/60.78 cnf(949,plain,
% 60.56/60.78 (~E(f4(a110),f4(a2))),
% 60.56/60.78 inference(scs_inference,[],[442,946,51,706,906,322,178,88,309,50,4,423,437,418,421,23,24,22])).
% 60.56/60.78 cnf(972,plain,
% 60.56/60.78 (~E(a88,a110)),
% 60.56/60.78 inference(scs_inference,[],[743,4])).
% 60.56/60.78 cnf(973,plain,
% 60.56/60.78 (P4(a184,a2)),
% 60.56/60.78 inference(scs_inference,[],[51,743,180,4,418])).
% 60.56/60.78 cnf(979,plain,
% 60.56/60.78 (~P8(f4(a110),f4(a88))),
% 60.56/60.78 inference(scs_inference,[],[51,49,743,323,180,699,90,318,4,418,437,423,421])).
% 60.56/60.78 cnf(982,plain,
% 60.56/60.78 (~P4(x9821,x9821)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(985,plain,
% 60.56/60.78 (~E(f4(a44),f4(a2))),
% 60.56/60.78 inference(scs_inference,[],[442,982,51,44,49,743,323,180,481,699,90,318,4,418,437,423,421,24,23,22])).
% 60.56/60.78 cnf(1008,plain,
% 60.56/60.78 (~P10(a134,a3,a2)),
% 60.56/60.78 inference(scs_inference,[],[408,488,2,429])).
% 60.56/60.78 cnf(1011,plain,
% 60.56/60.78 (~E(a110,a88)),
% 60.56/60.78 inference(scs_inference,[],[1008,705,426,4])).
% 60.56/60.78 cnf(1012,plain,
% 60.56/60.78 (~P10(a3,a5,a66)),
% 60.56/60.78 inference(scs_inference,[],[70,1008,581,705,426,4,429])).
% 60.56/60.78 cnf(1019,plain,
% 60.56/60.78 (P4(a187,a2)),
% 60.56/60.78 inference(scs_inference,[],[70,1008,488,581,51,705,324,182,92,309,426,4,429,28,423,437,418])).
% 60.56/60.78 cnf(1021,plain,
% 60.56/60.78 (~P8(f4(a110),f4(a77))),
% 60.56/60.78 inference(scs_inference,[],[70,1008,488,581,51,48,705,979,324,182,92,309,426,4,429,28,423,437,418,421])).
% 60.56/60.78 cnf(1023,plain,
% 60.56/60.78 (~E(f4(a77),f4(a110))),
% 60.56/60.78 inference(scs_inference,[],[70,1008,488,581,51,48,705,979,324,182,92,309,426,4,429,28,423,437,418,421,21])).
% 60.56/60.78 cnf(1025,plain,
% 60.56/60.78 (~P4(x10251,x10251)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1028,plain,
% 60.56/60.78 (~E(f4(a55),f4(a2))),
% 60.56/60.78 inference(scs_inference,[],[70,1008,488,581,442,1025,51,45,48,705,979,324,182,736,92,309,426,4,429,28,423,437,418,421,21,23,24,22])).
% 60.56/60.78 cnf(1053,plain,
% 60.56/60.78 (~E(a99,a88)),
% 60.56/60.78 inference(scs_inference,[],[1012,742,426,4])).
% 60.56/60.78 cnf(1054,plain,
% 60.56/60.78 (~P10(a3,a55,a66)),
% 60.56/60.78 inference(scs_inference,[],[70,1012,655,742,426,4,429])).
% 60.56/60.78 cnf(1058,plain,
% 60.56/60.78 (P4(a189,a2)),
% 60.56/60.78 inference(scs_inference,[],[70,1012,655,51,742,184,94,426,4,429,423,418])).
% 60.56/60.78 cnf(1062,plain,
% 60.56/60.78 (~P8(f4(a110),f4(a66))),
% 60.56/60.78 inference(scs_inference,[],[70,1012,655,51,47,742,1021,325,184,94,318,426,4,429,423,418,437,421])).
% 60.56/60.78 cnf(1064,plain,
% 60.56/60.78 (~E(f4(a66),f4(a110))),
% 60.56/60.78 inference(scs_inference,[],[70,1012,655,51,47,742,1021,325,184,94,318,426,4,429,423,418,437,421,21])).
% 60.56/60.78 cnf(1066,plain,
% 60.56/60.78 (~P4(x10661,x10661)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1069,plain,
% 60.56/60.78 (~E(f4(a77),f4(a66))),
% 60.56/60.78 inference(scs_inference,[],[70,1012,655,442,1066,51,47,742,1021,325,184,94,531,318,426,4,429,423,418,437,421,21,23,24,22])).
% 60.56/60.78 cnf(1094,plain,
% 60.56/60.78 (~E(a44,a1)),
% 60.56/60.78 inference(scs_inference,[],[1054,771,426,4])).
% 60.56/60.78 cnf(1095,plain,
% 60.56/60.78 (~P10(a3,a66,a66)),
% 60.56/60.78 inference(scs_inference,[],[70,1054,758,771,426,4,429])).
% 60.56/60.78 cnf(1099,plain,
% 60.56/60.78 (P4(a191,a2)),
% 60.56/60.78 inference(scs_inference,[],[70,1054,758,51,771,326,186,309,426,4,429,437,418])).
% 60.56/60.78 cnf(1103,plain,
% 60.56/60.78 (~P8(f4(a110),f4(a55))),
% 60.56/60.78 inference(scs_inference,[],[70,1054,758,51,46,771,1062,326,186,96,309,426,4,429,437,418,423,421])).
% 60.56/60.78 cnf(1105,plain,
% 60.56/60.78 (~E(f4(a55),f4(a110))),
% 60.56/60.78 inference(scs_inference,[],[70,1054,758,51,46,771,1062,326,186,96,309,426,4,429,437,418,423,421,21])).
% 60.56/60.78 cnf(1107,plain,
% 60.56/60.78 (~P4(x11071,x11071)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1108,plain,
% 60.56/60.78 (~E(f4(a66),f4(a55))),
% 60.56/60.78 inference(scs_inference,[],[70,1054,758,442,51,46,771,1062,326,186,96,526,309,426,4,429,437,418,423,421,21,24,22])).
% 60.56/60.78 cnf(1110,plain,
% 60.56/60.78 (~P4(x11101,x11101)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1114,plain,
% 60.56/60.78 (~P4(x11141,x11141)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1119,plain,
% 60.56/60.78 (~E(a44,a66)),
% 60.56/60.78 inference(scs_inference,[],[70,1054,758,442,1107,1110,1114,51,46,771,1062,326,186,187,98,96,526,309,426,4,429,437,418,423,421,21,24,22,23,431,419,420,685])).
% 60.56/60.78 cnf(1137,plain,
% 60.56/60.78 (~P10(a122,a5,a2)),
% 60.56/60.78 inference(scs_inference,[],[453,1095,511,772,426,4,429])).
% 60.56/60.78 cnf(1139,plain,
% 60.56/60.78 (~E(a134,a122)),
% 60.56/60.78 inference(scs_inference,[],[453,488,1095,511,772,426,4,429,27])).
% 60.56/60.78 cnf(1142,plain,
% 60.56/60.78 (P4(a193,a2)),
% 60.56/60.78 inference(scs_inference,[],[453,488,1095,511,51,772,188,98,426,4,429,27,423,418])).
% 60.56/60.78 cnf(1146,plain,
% 60.56/60.78 (~P8(f4(a110),f4(a44))),
% 60.56/60.78 inference(scs_inference,[],[453,488,1095,511,51,45,772,1103,328,188,98,426,4,429,27,423,418,437,421])).
% 60.56/60.78 cnf(1148,plain,
% 60.56/60.78 (~E(f4(a44),f4(a110))),
% 60.56/60.78 inference(scs_inference,[],[453,488,1095,511,51,45,772,1103,328,188,98,426,4,429,27,423,418,437,421,21])).
% 60.56/60.78 cnf(1149,plain,
% 60.56/60.78 (~E(f4(a99),f4(a2))),
% 60.56/60.78 inference(scs_inference,[],[453,488,1095,511,51,45,49,772,1103,328,188,869,98,426,4,429,27,423,418,437,421,21,22])).
% 60.56/60.78 cnf(1170,plain,
% 60.56/60.78 (~E(a66,a2)),
% 60.56/60.78 inference(scs_inference,[],[1137,808,426,4])).
% 60.56/60.78 cnf(1171,plain,
% 60.56/60.78 (~P10(a122,a44,a2)),
% 60.56/60.78 inference(scs_inference,[],[453,1137,1094,808,426,4,429])).
% 60.56/60.78 cnf(1173,plain,
% 60.56/60.78 (~E(a174,a122)),
% 60.56/60.78 inference(scs_inference,[],[453,1137,529,1094,808,426,4,429,27])).
% 60.56/60.78 cnf(1174,plain,
% 60.56/60.78 (P4(a195,a2)),
% 60.56/60.78 inference(scs_inference,[],[453,1137,529,1094,51,808,190,426,4,429,27,418])).
% 60.56/60.78 cnf(1176,plain,
% 60.56/60.78 (P10(a65,a195,a2)),
% 60.56/60.78 inference(scs_inference,[],[453,1137,529,1094,51,808,190,100,426,4,429,27,418,423])).
% 60.56/60.78 cnf(1180,plain,
% 60.56/60.78 (~P8(f4(a110),f4(a5))),
% 60.56/60.78 inference(scs_inference,[],[453,1137,529,1094,51,44,808,1146,329,190,328,100,426,4,429,27,418,423,437,421])).
% 60.56/60.78 cnf(1182,plain,
% 60.56/60.78 (~E(f4(a5),f4(a110))),
% 60.56/60.78 inference(scs_inference,[],[453,1137,529,1094,51,44,808,1146,329,190,328,100,426,4,429,27,418,423,437,421,21])).
% 60.56/60.78 cnf(1185,plain,
% 60.56/60.78 (~P4(x11851,x11851)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1186,plain,
% 60.56/60.78 (~E(a2,a195)),
% 60.56/60.78 inference(scs_inference,[],[453,1137,529,1094,442,1185,51,44,48,808,1146,329,190,328,100,557,426,4,429,27,418,423,437,421,21,22,23,24])).
% 60.56/60.78 cnf(1187,plain,
% 60.56/60.78 (~P4(x11871,x11871)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1191,plain,
% 60.56/60.78 (~P4(x11911,x11911)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1196,plain,
% 60.56/60.78 (~E(a1,a44)),
% 60.56/60.78 inference(scs_inference,[],[453,1137,529,1094,442,1185,1187,1191,51,44,48,808,1146,329,190,191,102,328,100,557,426,4,429,27,418,423,437,421,21,22,23,24,431,419,420,855])).
% 60.56/60.78 cnf(1207,plain,
% 60.56/60.78 (~P10(a3,a1,a66)),
% 60.56/60.78 inference(scs_inference,[],[70,1171,1196,809,426,4,429])).
% 60.56/60.78 cnf(1209,plain,
% 60.56/60.78 (P10(a68,a198,a2)),
% 60.56/60.78 inference(scs_inference,[],[70,1171,1196,809,192,102,426,4,429,423])).
% 60.56/60.78 cnf(1211,plain,
% 60.56/60.78 (~P8(f4(a110),f4(a1))),
% 60.56/60.78 inference(scs_inference,[],[70,1171,1196,43,809,1180,192,102,426,4,429,423,421])).
% 60.56/60.78 cnf(1213,plain,
% 60.56/60.78 (P4(a198,a2)),
% 60.56/60.78 inference(scs_inference,[],[70,1171,1196,51,43,809,1180,192,102,426,4,429,423,421,418])).
% 60.56/60.78 cnf(1217,plain,
% 60.56/60.78 (~E(f4(a1),f4(a110))),
% 60.56/60.78 inference(scs_inference,[],[70,1171,1196,51,43,809,1180,330,192,102,310,426,4,429,423,421,418,437,21])).
% 60.56/60.78 cnf(1219,plain,
% 60.56/60.78 (~P4(x12191,x12191)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1220,plain,
% 60.56/60.78 (~E(a2,a198)),
% 60.56/60.78 inference(scs_inference,[],[70,1171,1196,442,1219,51,43,809,1180,330,192,102,310,426,4,429,423,421,418,437,21,23,24])).
% 60.56/60.78 cnf(1246,plain,
% 60.56/60.78 (~E(a77,a2)),
% 60.56/60.78 inference(scs_inference,[],[1207,838,426,4])).
% 60.56/60.78 cnf(1247,plain,
% 60.56/60.78 (~P10(a174,a1,a2)),
% 60.56/60.78 inference(scs_inference,[],[529,1207,1196,838,426,4,429])).
% 60.56/60.78 cnf(1249,plain,
% 60.56/60.78 (~E(a122,a174)),
% 60.56/60.78 inference(scs_inference,[],[453,529,1207,1196,838,426,4,429,27])).
% 60.56/60.78 cnf(1250,plain,
% 60.56/60.78 (P4(a200,a2)),
% 60.56/60.78 inference(scs_inference,[],[453,529,1207,1196,51,838,194,426,4,429,27,418])).
% 60.56/60.78 cnf(1252,plain,
% 60.56/60.78 (~P8(f4(a44),f4(a5))),
% 60.56/60.78 inference(scs_inference,[],[453,529,1207,1196,51,44,838,194,493,426,4,429,27,418,421])).
% 60.56/60.78 cnf(1254,plain,
% 60.56/60.78 (P10(a70,a200,a2)),
% 60.56/60.78 inference(scs_inference,[],[453,529,1207,1196,51,44,838,194,104,493,426,4,429,27,418,421,423])).
% 60.56/60.78 cnf(1258,plain,
% 60.56/60.78 (~E(f4(a2),f4(a110))),
% 60.56/60.78 inference(scs_inference,[],[453,529,1207,1196,51,42,44,838,1211,331,194,104,493,328,426,4,429,27,418,421,423,437,21])).
% 60.56/60.78 cnf(1260,plain,
% 60.56/60.78 (~P4(x12601,x12601)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1261,plain,
% 60.56/60.78 (~E(a2,a200)),
% 60.56/60.78 inference(scs_inference,[],[453,529,1207,1196,442,1260,51,42,44,838,1211,331,194,104,493,328,426,4,429,27,418,421,423,437,21,23,24])).
% 60.56/60.78 cnf(1288,plain,
% 60.56/60.78 (~P10(a218,a77,a2)),
% 60.56/60.78 inference(scs_inference,[],[1247,599,899,839,426,4,429])).
% 60.56/60.78 cnf(1290,plain,
% 60.56/60.78 (~E(a88,a77)),
% 60.56/60.78 inference(scs_inference,[],[1247,599,899,839,426,4,429,28])).
% 60.56/60.78 cnf(1293,plain,
% 60.56/60.78 (~P8(f4(a44),f4(a1))),
% 60.56/60.78 inference(scs_inference,[],[1247,599,899,43,839,1252,332,319,426,4,429,28,437,421])).
% 60.56/60.78 cnf(1295,plain,
% 60.56/60.78 (P4(a202,a2)),
% 60.56/60.78 inference(scs_inference,[],[1247,599,899,51,43,839,1252,332,196,319,426,4,429,28,437,421,418])).
% 60.56/60.78 cnf(1297,plain,
% 60.56/60.78 (P10(a72,a202,a2)),
% 60.56/60.78 inference(scs_inference,[],[1247,599,899,51,43,839,1252,332,196,106,319,426,4,429,28,437,421,418,423])).
% 60.56/60.78 cnf(1299,plain,
% 60.56/60.78 (~E(f4(a55),f4(a5))),
% 60.56/60.78 inference(scs_inference,[],[1247,599,899,51,43,45,839,1252,332,196,106,319,426,4,429,28,437,421,418,423,22])).
% 60.56/60.78 cnf(1302,plain,
% 60.56/60.78 (~P4(x13021,x13021)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1303,plain,
% 60.56/60.78 (~E(a2,a202)),
% 60.56/60.78 inference(scs_inference,[],[1247,599,899,442,1302,51,43,45,839,1252,332,196,106,319,426,4,429,28,437,421,418,423,22,21,23,24])).
% 60.56/60.78 cnf(1329,plain,
% 60.56/60.78 (~E(a88,a2)),
% 60.56/60.78 inference(scs_inference,[],[1288,875,426,4])).
% 60.56/60.78 cnf(1330,plain,
% 60.56/60.78 (~P10(a240,a99,a2)),
% 60.56/60.78 inference(scs_inference,[],[1288,636,936,875,426,4,429])).
% 60.56/60.78 cnf(1332,plain,
% 60.56/60.78 (~E(a110,a99)),
% 60.56/60.78 inference(scs_inference,[],[1288,636,936,875,426,4,429,28])).
% 60.56/60.78 cnf(1333,plain,
% 60.56/60.78 (P10(a74,a204,a2)),
% 60.56/60.78 inference(scs_inference,[],[1288,636,936,875,198,108,426,4,429,28,423])).
% 60.56/60.78 cnf(1335,plain,
% 60.56/60.78 (~P8(f4(a88),f4(a77))),
% 60.56/60.78 inference(scs_inference,[],[1288,636,936,48,875,198,108,562,426,4,429,28,423,421])).
% 60.56/60.78 cnf(1339,plain,
% 60.56/60.78 (P4(a204,a2)),
% 60.56/60.78 inference(scs_inference,[],[1288,636,936,51,48,875,333,198,108,562,310,426,4,429,28,423,421,437,418])).
% 60.56/60.78 cnf(1341,plain,
% 60.56/60.78 (~E(f4(a55),f4(a1))),
% 60.56/60.78 inference(scs_inference,[],[1288,636,936,51,48,45,875,1293,333,198,108,562,310,426,4,429,28,423,421,437,418,22])).
% 60.56/60.78 cnf(1342,plain,
% 60.56/60.78 (~E(f4(a2),f4(a44))),
% 60.56/60.78 inference(scs_inference,[],[1288,636,936,51,42,48,45,875,1293,333,198,108,562,310,426,4,429,28,423,421,437,418,22,21])).
% 60.56/60.78 cnf(1344,plain,
% 60.56/60.78 (~P4(x13441,x13441)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1345,plain,
% 60.56/60.78 (~E(a2,a204)),
% 60.56/60.78 inference(scs_inference,[],[1288,636,936,442,1344,51,42,48,45,875,1293,333,198,108,562,310,426,4,429,28,423,421,437,418,22,21,23,24])).
% 60.56/60.78 cnf(1372,plain,
% 60.56/60.78 (~P10(a196,a44,a2)),
% 60.56/60.78 inference(scs_inference,[],[1119,1330,560,876,426,4,429])).
% 60.56/60.78 cnf(1374,plain,
% 60.56/60.78 (P4(a206,a2)),
% 60.56/60.78 inference(scs_inference,[],[1119,1330,560,51,876,200,426,4,429,418])).
% 60.56/60.78 cnf(1376,plain,
% 60.56/60.78 (~P8(f4(a88),f4(a66))),
% 60.56/60.78 inference(scs_inference,[],[1119,1330,560,51,47,876,1335,200,426,4,429,418,421])).
% 60.56/60.78 cnf(1378,plain,
% 60.56/60.78 (P10(a76,a206,a2)),
% 60.56/60.78 inference(scs_inference,[],[1119,1330,560,51,47,876,1335,200,110,426,4,429,418,421,423])).
% 60.56/60.78 cnf(1382,plain,
% 60.56/60.78 (~E(f4(a66),f4(a88))),
% 60.56/60.78 inference(scs_inference,[],[1119,1330,560,51,47,876,1335,334,200,110,328,426,4,429,418,421,423,437,21])).
% 60.56/60.78 cnf(1383,plain,
% 60.56/60.78 (~E(f4(a99),f4(a77))),
% 60.56/60.78 inference(scs_inference,[],[1119,1330,560,51,49,47,876,1335,334,200,110,328,426,4,429,418,421,423,437,21,22])).
% 60.56/60.78 cnf(1385,plain,
% 60.56/60.78 (~P4(x13851,x13851)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1386,plain,
% 60.56/60.78 (~E(a2,a206)),
% 60.56/60.78 inference(scs_inference,[],[1119,1330,560,442,1385,51,49,47,876,1335,334,200,110,328,426,4,429,418,421,423,437,21,22,23,24])).
% 60.56/60.78 cnf(1387,plain,
% 60.56/60.78 (~P4(x13871,x13871)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1391,plain,
% 60.56/60.78 (~P4(x13911,x13911)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1396,plain,
% 60.56/60.78 (~E(a174,a196)),
% 60.56/60.78 inference(scs_inference,[],[1119,1330,560,442,1385,1387,1391,51,49,47,876,1335,334,200,201,112,110,328,426,4,429,418,421,423,437,21,22,23,24,431,419,420,890])).
% 60.56/60.78 cnf(1413,plain,
% 60.56/60.78 (~E(a110,a2)),
% 60.56/60.78 inference(scs_inference,[],[1372,949,426,4])).
% 60.56/60.78 cnf(1414,plain,
% 60.56/60.78 (~P10(a218,a110,a2)),
% 60.56/60.78 inference(scs_inference,[],[599,1372,1011,949,426,4,429])).
% 60.56/60.78 cnf(1416,plain,
% 60.56/60.78 (~E(a240,a218)),
% 60.56/60.78 inference(scs_inference,[],[599,636,1372,1011,949,426,4,429,27])).
% 60.56/60.78 cnf(1417,plain,
% 60.56/60.78 (P10(a79,a209,a2)),
% 60.56/60.78 inference(scs_inference,[],[599,636,1372,1011,949,202,112,426,4,429,27,423])).
% 60.56/60.78 cnf(1419,plain,
% 60.56/60.78 (~P8(f4(a88),f4(a55))),
% 60.56/60.78 inference(scs_inference,[],[599,636,1372,1011,46,949,1376,202,112,426,4,429,27,423,421])).
% 60.56/60.78 cnf(1421,plain,
% 60.56/60.78 (P4(a209,a2)),
% 60.56/60.78 inference(scs_inference,[],[599,636,1372,1011,51,46,949,1376,202,112,426,4,429,27,423,421,418])).
% 60.56/60.78 cnf(1425,plain,
% 60.56/60.78 (~E(f4(a55),f4(a88))),
% 60.56/60.78 inference(scs_inference,[],[599,636,1372,1011,51,46,949,1376,335,202,112,319,426,4,429,27,423,421,418,437,21])).
% 60.56/60.78 cnf(1427,plain,
% 60.56/60.78 (~P4(x14271,x14271)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1428,plain,
% 60.56/60.78 (~E(f4(a99),f4(a66))),
% 60.56/60.78 inference(scs_inference,[],[599,636,1372,1011,442,51,49,46,949,1376,335,202,112,319,426,4,429,27,423,421,418,437,21,23,22])).
% 60.56/60.78 cnf(1429,plain,
% 60.56/60.78 (~E(a2,a209)),
% 60.56/60.78 inference(scs_inference,[],[599,636,1372,1011,442,1427,51,49,46,949,1376,335,202,112,319,426,4,429,27,423,421,418,437,21,23,22,24])).
% 60.56/60.78 cnf(1455,plain,
% 60.56/60.78 (~E(a44,a2)),
% 60.56/60.78 inference(scs_inference,[],[1414,985,426,4])).
% 60.56/60.78 cnf(1456,plain,
% 60.56/60.78 (~P10(a240,a88,a2)),
% 60.56/60.78 inference(scs_inference,[],[636,1414,972,985,426,4,429])).
% 60.56/60.78 cnf(1459,plain,
% 60.56/60.78 (P10(a81,a211,a2)),
% 60.56/60.78 inference(scs_inference,[],[636,599,1414,972,985,204,114,426,4,429,27,423])).
% 60.56/60.78 cnf(1461,plain,
% 60.56/60.78 (~P8(f4(a88),f4(a44))),
% 60.56/60.78 inference(scs_inference,[],[636,599,1414,972,45,985,1419,204,114,426,4,429,27,423,421])).
% 60.56/60.78 cnf(1465,plain,
% 60.56/60.78 (P4(a211,a2)),
% 60.56/60.78 inference(scs_inference,[],[636,599,1414,972,51,45,985,1419,338,204,114,426,4,429,27,423,421,437,418])).
% 60.56/60.78 cnf(1467,plain,
% 60.56/60.78 (~E(f4(a44),f4(a88))),
% 60.56/60.78 inference(scs_inference,[],[636,599,1414,972,51,45,985,1419,338,204,114,426,4,429,27,423,421,437,418,21])).
% 60.56/60.78 cnf(1469,plain,
% 60.56/60.78 (~P4(x14691,x14691)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1470,plain,
% 60.56/60.78 (~E(f4(a99),f4(a55))),
% 60.56/60.78 inference(scs_inference,[],[636,599,1414,972,442,51,49,45,985,1419,338,204,114,426,4,429,27,423,421,437,418,21,23,22])).
% 60.56/60.78 cnf(1471,plain,
% 60.56/60.78 (~E(a2,a211)),
% 60.56/60.78 inference(scs_inference,[],[636,599,1414,972,442,1469,51,49,45,985,1419,338,204,114,426,4,429,27,423,421,437,418,21,23,22,24])).
% 60.56/60.78 cnf(1497,plain,
% 60.56/60.78 (~E(a77,a110)),
% 60.56/60.78 inference(scs_inference,[],[1456,1023,426,4])).
% 60.56/60.78 cnf(1498,plain,
% 60.56/60.78 (~P10(a218,a99,a2)),
% 60.56/60.78 inference(scs_inference,[],[599,1456,1053,1023,426,4,429])).
% 60.56/60.78 cnf(1500,plain,
% 60.56/60.78 (P10(a83,a213,a2)),
% 60.56/60.78 inference(scs_inference,[],[599,1456,1053,1023,206,116,426,4,429,423])).
% 60.56/60.78 cnf(1502,plain,
% 60.56/60.78 (~P8(f4(a88),f4(a5))),
% 60.56/60.78 inference(scs_inference,[],[599,1456,1053,44,1023,1461,206,116,426,4,429,423,421])).
% 60.56/60.78 cnf(1504,plain,
% 60.56/60.78 (P4(a213,a2)),
% 60.56/60.78 inference(scs_inference,[],[599,1456,1053,51,44,1023,1461,206,116,426,4,429,423,421,418])).
% 60.56/60.78 cnf(1508,plain,
% 60.56/60.78 (~E(f4(a5),f4(a88))),
% 60.56/60.78 inference(scs_inference,[],[599,1456,1053,51,44,1023,1461,339,206,338,116,426,4,429,423,421,418,437,21])).
% 60.56/60.78 cnf(1510,plain,
% 60.56/60.78 (~P4(x15101,x15101)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1511,plain,
% 60.56/60.78 (~E(f4(a99),f4(a44))),
% 60.56/60.78 inference(scs_inference,[],[599,1456,1053,442,51,44,49,1023,1461,339,206,338,116,426,4,429,423,421,418,437,21,23,22])).
% 60.56/60.78 cnf(1512,plain,
% 60.56/60.78 (~E(a2,a213)),
% 60.56/60.78 inference(scs_inference,[],[599,1456,1053,442,1510,51,44,49,1023,1461,339,206,338,116,426,4,429,423,421,418,437,21,23,22,24])).
% 60.56/60.78 cnf(1538,plain,
% 60.56/60.78 (~E(a55,a2)),
% 60.56/60.78 inference(scs_inference,[],[1498,1028,426,4])).
% 60.56/60.78 cnf(1539,plain,
% 60.56/60.78 (~P10(a240,a77,a2)),
% 60.56/60.78 inference(scs_inference,[],[636,1498,1497,1028,426,4,429])).
% 60.56/60.78 cnf(1541,plain,
% 60.56/60.78 (P10(a85,a215,a2)),
% 60.56/60.78 inference(scs_inference,[],[636,1498,1497,1028,208,118,426,4,429,423])).
% 60.56/60.78 cnf(1543,plain,
% 60.56/60.78 (~P8(f4(a88),f4(a1))),
% 60.56/60.78 inference(scs_inference,[],[636,1498,1497,43,1028,1502,208,118,426,4,429,423,421])).
% 60.56/60.78 cnf(1545,plain,
% 60.56/60.78 (P4(a215,a2)),
% 60.56/60.78 inference(scs_inference,[],[636,1498,1497,51,43,1028,1502,208,118,426,4,429,423,421,418])).
% 60.56/60.78 cnf(1549,plain,
% 60.56/60.78 (~E(f4(a1),f4(a88))),
% 60.56/60.78 inference(scs_inference,[],[636,1498,1497,51,43,1028,1502,340,208,118,311,426,4,429,423,421,418,437,21])).
% 60.56/60.78 cnf(1551,plain,
% 60.56/60.78 (~P4(x15511,x15511)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1552,plain,
% 60.56/60.78 (~E(f4(a99),f4(a5))),
% 60.56/60.78 inference(scs_inference,[],[636,1498,1497,442,51,43,49,1028,1502,340,208,118,311,426,4,429,423,421,418,437,21,23,22])).
% 60.56/60.78 cnf(1553,plain,
% 60.56/60.78 (~E(a2,a215)),
% 60.56/60.78 inference(scs_inference,[],[636,1498,1497,442,1551,51,43,49,1028,1502,340,208,118,311,426,4,429,423,421,418,437,21,23,22,24])).
% 60.56/60.78 cnf(1579,plain,
% 60.56/60.78 (~E(a66,a110)),
% 60.56/60.78 inference(scs_inference,[],[1539,1064,426,4])).
% 60.56/60.78 cnf(1580,plain,
% 60.56/60.78 (~P10(a66,a174,a2)),
% 60.56/60.78 inference(scs_inference,[],[1396,1539,549,1064,426,4,429])).
% 60.56/60.78 cnf(1582,plain,
% 60.56/60.78 (~E(a110,a77)),
% 60.56/60.78 inference(scs_inference,[],[636,1396,1539,549,1064,426,4,429,28])).
% 60.56/60.78 cnf(1583,plain,
% 60.56/60.78 (P10(a87,a217,a2)),
% 60.56/60.78 inference(scs_inference,[],[636,1396,1539,549,1064,210,120,426,4,429,28,423])).
% 60.56/60.78 cnf(1585,plain,
% 60.56/60.78 (~P8(f4(a55),f4(a5))),
% 60.56/60.78 inference(scs_inference,[],[636,1396,1539,549,44,1064,210,120,547,426,4,429,28,423,421])).
% 60.56/60.78 cnf(1587,plain,
% 60.56/60.78 (P4(a217,a2)),
% 60.56/60.78 inference(scs_inference,[],[636,1396,1539,549,51,44,1064,210,120,547,426,4,429,28,423,421,418])).
% 60.56/60.78 cnf(1592,plain,
% 60.56/60.78 (~P4(x15921,x15921)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1593,plain,
% 60.56/60.78 (~E(f4(a2),f4(a88))),
% 60.56/60.78 inference(scs_inference,[],[636,1396,1539,549,442,51,42,44,1064,1543,341,210,120,547,329,426,4,429,28,423,421,418,437,23,21])).
% 60.56/60.78 cnf(1594,plain,
% 60.56/60.78 (~E(f4(a99),f4(a1))),
% 60.56/60.78 inference(scs_inference,[],[636,1396,1539,549,442,51,42,44,49,1064,1543,341,210,120,547,329,426,4,429,28,423,421,418,437,23,21,22])).
% 60.56/60.78 cnf(1595,plain,
% 60.56/60.78 (~E(a2,a217)),
% 60.56/60.78 inference(scs_inference,[],[636,1396,1539,549,442,1592,51,42,44,49,1064,1543,341,210,120,547,329,426,4,429,28,423,421,418,437,23,21,22,24])).
% 60.56/60.78 cnf(1619,plain,
% 60.56/60.78 (P7(f251(f4(x16191),f4(a1)))),
% 60.56/60.78 inference(scs_inference,[],[33,411,416])).
% 60.56/60.78 cnf(1623,plain,
% 60.56/60.78 (~P10(a240,a66,a2)),
% 60.56/60.78 inference(scs_inference,[],[636,1580,1579,1069,426,4,429])).
% 60.56/60.78 cnf(1625,plain,
% 60.56/60.78 (~E(a196,a174)),
% 60.56/60.78 inference(scs_inference,[],[636,1580,1579,549,1069,426,4,429,28])).
% 60.56/60.78 cnf(1626,plain,
% 60.56/60.78 (~E(a196,a240)),
% 60.56/60.78 inference(scs_inference,[],[636,560,1580,1579,549,1069,426,4,429,28,27])).
% 60.56/60.78 cnf(1627,plain,
% 60.56/60.78 (P10(a90,a220,a2)),
% 60.56/60.78 inference(scs_inference,[],[636,560,1580,1579,549,1069,212,122,426,4,429,28,27,423])).
% 60.56/60.78 cnf(1629,plain,
% 60.56/60.78 (~P8(f4(a55),f4(a1))),
% 60.56/60.78 inference(scs_inference,[],[636,560,1580,1579,549,43,1069,1585,212,122,426,4,429,28,27,423,421])).
% 60.56/60.78 cnf(1631,plain,
% 60.56/60.78 (P4(a220,a2)),
% 60.56/60.78 inference(scs_inference,[],[636,560,1580,1579,549,51,43,1069,1585,212,122,426,4,429,28,27,423,421,418])).
% 60.56/60.78 cnf(1636,plain,
% 60.56/60.78 (~P4(x16361,x16361)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1638,plain,
% 60.56/60.78 (~E(f4(a66),f4(a5))),
% 60.56/60.78 inference(scs_inference,[],[636,560,1580,1579,549,442,51,43,46,1069,1585,342,212,122,338,426,4,429,28,27,423,421,418,437,23,21,22])).
% 60.56/60.78 cnf(1639,plain,
% 60.56/60.78 (~E(a2,a220)),
% 60.56/60.78 inference(scs_inference,[],[636,560,1580,1579,549,442,1636,51,43,46,1069,1585,342,212,122,338,426,4,429,28,27,423,421,418,437,23,21,22,24])).
% 60.56/60.78 cnf(1665,plain,
% 60.56/60.78 (~E(a55,a110)),
% 60.56/60.78 inference(scs_inference,[],[1623,1105,426,4])).
% 60.56/60.78 cnf(1666,plain,
% 60.56/60.78 (~P10(a44,a122,a2)),
% 60.56/60.78 inference(scs_inference,[],[1249,1623,520,1105,426,4,429])).
% 60.56/60.78 cnf(1668,plain,
% 60.56/60.78 (~E(a110,a66)),
% 60.56/60.78 inference(scs_inference,[],[636,1249,1623,520,1105,426,4,429,28])).
% 60.56/60.78 cnf(1669,plain,
% 60.56/60.78 (P10(a92,a222,a2)),
% 60.56/60.78 inference(scs_inference,[],[636,1249,1623,520,1105,214,124,426,4,429,28,423])).
% 60.56/60.78 cnf(1671,plain,
% 60.56/60.78 (~P8(f4(a66),f4(a44))),
% 60.56/60.78 inference(scs_inference,[],[636,1249,1623,520,45,1105,214,124,584,426,4,429,28,423,421])).
% 60.56/60.78 cnf(1675,plain,
% 60.56/60.78 (P4(a222,a2)),
% 60.56/60.78 inference(scs_inference,[],[636,1249,1623,520,51,45,1105,343,214,124,584,320,426,4,429,28,423,421,437,418])).
% 60.56/60.78 cnf(1678,plain,
% 60.56/60.78 (~P4(x16781,x16781)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1679,plain,
% 60.56/60.78 (~E(f4(a2),f4(a55))),
% 60.56/60.78 inference(scs_inference,[],[636,1249,1623,520,442,51,42,45,1105,1629,343,214,124,584,320,426,4,429,28,423,421,437,418,23,21])).
% 60.56/60.78 cnf(1680,plain,
% 60.56/60.78 (~E(f4(a66),f4(a1))),
% 60.56/60.78 inference(scs_inference,[],[636,1249,1623,520,442,51,42,45,46,1105,1629,343,214,124,584,320,426,4,429,28,423,421,437,418,23,21,22])).
% 60.56/60.78 cnf(1681,plain,
% 60.56/60.78 (~E(a2,a222)),
% 60.56/60.78 inference(scs_inference,[],[636,1249,1623,520,442,1678,51,42,45,46,1105,1629,343,214,124,584,320,426,4,429,28,423,421,437,418,23,21,22,24])).
% 60.56/60.78 cnf(1699,plain,
% 60.56/60.78 (~E(a66,a55)),
% 60.56/60.78 inference(scs_inference,[],[1666,1108,426,4])).
% 60.56/60.78 cnf(1700,plain,
% 60.56/60.78 (~P10(a240,a55,a2)),
% 60.56/60.78 inference(scs_inference,[],[636,1666,1665,1108,426,4,429])).
% 60.56/60.78 cnf(1702,plain,
% 60.56/60.78 (P10(a94,a224,a2)),
% 60.56/60.78 inference(scs_inference,[],[636,1666,1665,1108,216,126,426,4,429,423])).
% 60.56/60.78 cnf(1704,plain,
% 60.56/60.78 (~P8(f4(a66),f4(a5))),
% 60.56/60.78 inference(scs_inference,[],[636,1666,1665,44,1108,1671,216,126,426,4,429,423,421])).
% 60.56/60.78 cnf(1708,plain,
% 60.56/60.78 (P4(a224,a2)),
% 60.56/60.78 inference(scs_inference,[],[636,1666,1665,51,44,1108,1671,344,216,126,311,426,4,429,423,421,437,418])).
% 60.56/60.78 cnf(1711,plain,
% 60.56/60.78 (~P4(x17111,x17111)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1712,plain,
% 60.56/60.78 (~E(f4(a5),f4(a66))),
% 60.56/60.78 inference(scs_inference,[],[636,1666,1665,442,51,44,1108,1671,344,216,126,311,426,4,429,423,421,437,418,23,21])).
% 60.56/60.78 cnf(1713,plain,
% 60.56/60.78 (~E(f4(a77),f4(a44))),
% 60.56/60.78 inference(scs_inference,[],[636,1666,1665,442,51,47,44,1108,1671,344,216,126,311,426,4,429,423,421,437,418,23,21,22])).
% 60.56/60.78 cnf(1714,plain,
% 60.56/60.78 (~E(a2,a224)),
% 60.56/60.78 inference(scs_inference,[],[636,1666,1665,442,1711,51,47,44,1108,1671,344,216,126,311,426,4,429,423,421,437,418,23,21,22,24])).
% 60.56/60.78 cnf(1740,plain,
% 60.56/60.78 (~E(a44,a110)),
% 60.56/60.78 inference(scs_inference,[],[1700,1148,426,4])).
% 60.56/60.78 cnf(1741,plain,
% 60.56/60.78 (~P10(a196,a110,a2)),
% 60.56/60.78 inference(scs_inference,[],[560,1668,1700,1148,426,4,429])).
% 60.56/60.78 cnf(1743,plain,
% 60.56/60.78 (~E(a110,a55)),
% 60.56/60.78 inference(scs_inference,[],[636,560,1668,1700,1148,426,4,429,28])).
% 60.56/60.78 cnf(1744,plain,
% 60.56/60.78 (P10(a96,a226,a2)),
% 60.56/60.78 inference(scs_inference,[],[636,560,1668,1700,1148,218,128,426,4,429,28,423])).
% 60.56/60.78 cnf(1746,plain,
% 60.56/60.78 (~P8(f4(a66),f4(a1))),
% 60.56/60.78 inference(scs_inference,[],[636,560,1668,1700,43,1148,1704,218,128,426,4,429,28,423,421])).
% 60.56/60.78 cnf(1750,plain,
% 60.56/60.78 (P4(a226,a2)),
% 60.56/60.78 inference(scs_inference,[],[636,560,1668,1700,51,43,1148,1704,348,218,128,426,4,429,28,423,421,437,418])).
% 60.56/60.78 cnf(1753,plain,
% 60.56/60.78 (~P4(x17531,x17531)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1754,plain,
% 60.56/60.78 (~E(f4(a1),f4(a66))),
% 60.56/60.78 inference(scs_inference,[],[636,560,1668,1700,442,51,43,1148,1704,348,218,128,426,4,429,28,423,421,437,418,23,21])).
% 60.56/60.78 cnf(1755,plain,
% 60.56/60.78 (~E(f4(a77),f4(a5))),
% 60.56/60.78 inference(scs_inference,[],[636,560,1668,1700,442,51,47,43,1148,1704,348,218,128,426,4,429,28,423,421,437,418,23,21,22])).
% 60.56/60.78 cnf(1756,plain,
% 60.56/60.78 (~E(a2,a226)),
% 60.56/60.78 inference(scs_inference,[],[636,560,1668,1700,442,1753,51,47,43,1148,1704,348,218,128,426,4,429,28,423,421,437,418,23,21,22,24])).
% 60.56/60.78 cnf(1782,plain,
% 60.56/60.78 (~E(a99,a2)),
% 60.56/60.78 inference(scs_inference,[],[1741,1149,426,4])).
% 60.56/60.78 cnf(1783,plain,
% 60.56/60.78 (~P10(a240,a44,a2)),
% 60.56/60.78 inference(scs_inference,[],[636,1741,1740,1149,426,4,429])).
% 60.56/60.78 cnf(1785,plain,
% 60.56/60.78 (P10(a98,a228,a2)),
% 60.56/60.78 inference(scs_inference,[],[636,1741,1740,1149,220,130,426,4,429,423])).
% 60.56/60.78 cnf(1787,plain,
% 60.56/60.78 (~P8(f4(a77),f4(a55))),
% 60.56/60.78 inference(scs_inference,[],[636,1741,1740,46,1149,220,130,625,426,4,429,423,421])).
% 60.56/60.78 cnf(1791,plain,
% 60.56/60.78 (P4(a228,a2)),
% 60.56/60.78 inference(scs_inference,[],[636,1741,1740,51,46,1149,349,220,339,130,625,426,4,429,423,421,437,418])).
% 60.56/60.78 cnf(1794,plain,
% 60.56/60.78 (~P4(x17941,x17941)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1795,plain,
% 60.56/60.78 (~E(f4(a2),f4(a66))),
% 60.56/60.78 inference(scs_inference,[],[636,1741,1740,442,51,42,46,1149,1746,349,220,339,130,625,426,4,429,423,421,437,418,23,21])).
% 60.56/60.78 cnf(1796,plain,
% 60.56/60.78 (~E(f4(a77),f4(a1))),
% 60.56/60.78 inference(scs_inference,[],[636,1741,1740,442,51,42,47,46,1149,1746,349,220,339,130,625,426,4,429,423,421,437,418,23,21,22])).
% 60.56/60.78 cnf(1797,plain,
% 60.56/60.78 (~E(a2,a228)),
% 60.56/60.78 inference(scs_inference,[],[636,1741,1740,442,1794,51,42,47,46,1149,1746,349,220,339,130,625,426,4,429,423,421,437,418,23,21,22,24])).
% 60.56/60.78 cnf(1798,plain,
% 60.56/60.78 (~P4(x17981,x17981)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1802,plain,
% 60.56/60.78 (~P4(x18021,x18021)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1807,plain,
% 60.56/60.78 (~E(a174,a240)),
% 60.56/60.78 inference(scs_inference,[],[636,1741,1740,442,1794,1798,1802,51,42,47,46,1149,1746,349,220,221,132,339,130,625,426,4,429,423,421,437,418,23,21,22,24,431,419,420,890])).
% 60.56/60.78 cnf(1824,plain,
% 60.56/60.78 (~E(a5,a110)),
% 60.56/60.78 inference(scs_inference,[],[1783,1182,426,4])).
% 60.56/60.78 cnf(1825,plain,
% 60.56/60.78 (~P10(a44,a196,a2)),
% 60.56/60.78 inference(scs_inference,[],[1625,1783,520,1182,426,4,429])).
% 60.56/60.78 cnf(1827,plain,
% 60.56/60.78 (~E(a110,a44)),
% 60.56/60.78 inference(scs_inference,[],[636,1625,1783,520,1182,426,4,429,28])).
% 60.56/60.78 cnf(1828,plain,
% 60.56/60.78 (P10(a101,a231,a2)),
% 60.56/60.78 inference(scs_inference,[],[636,1625,1783,520,1182,222,132,426,4,429,28,423])).
% 60.56/60.78 cnf(1830,plain,
% 60.56/60.78 (~P8(f4(a77),f4(a44))),
% 60.56/60.78 inference(scs_inference,[],[636,1625,1783,520,45,1182,1787,222,132,426,4,429,28,423,421])).
% 60.56/60.78 cnf(1834,plain,
% 60.56/60.78 (P4(a231,a2)),
% 60.56/60.78 inference(scs_inference,[],[636,1625,1783,520,51,45,1182,1787,350,222,348,132,426,4,429,28,423,421,437,418])).
% 60.56/60.78 cnf(1837,plain,
% 60.56/60.78 (~P4(x18371,x18371)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1838,plain,
% 60.56/60.78 (~E(f4(a44),f4(a77))),
% 60.56/60.78 inference(scs_inference,[],[636,1625,1783,520,442,51,45,1182,1787,350,222,348,132,426,4,429,28,423,421,437,418,23,21])).
% 60.56/60.78 cnf(1840,plain,
% 60.56/60.78 (~E(a2,a231)),
% 60.56/60.78 inference(scs_inference,[],[636,1625,1783,520,442,1837,51,48,45,1182,1787,350,222,348,132,426,4,429,28,423,421,437,418,23,21,22,24])).
% 60.56/60.78 cnf(1866,plain,
% 60.56/60.78 (~E(a1,a110)),
% 60.56/60.78 inference(scs_inference,[],[1825,1217,426,4])).
% 60.56/60.78 cnf(1867,plain,
% 60.56/60.78 (~P10(a3,a110,a66)),
% 60.56/60.78 inference(scs_inference,[],[70,1825,1827,1217,426,4,429])).
% 60.56/60.78 cnf(1869,plain,
% 60.56/60.78 (P10(a103,a233,a2)),
% 60.56/60.78 inference(scs_inference,[],[70,1825,1827,1217,224,134,426,4,429,423])).
% 60.56/60.78 cnf(1871,plain,
% 60.56/60.78 (~P8(f4(a77),f4(a5))),
% 60.56/60.78 inference(scs_inference,[],[70,1825,1827,44,1217,1830,224,134,426,4,429,423,421])).
% 60.56/60.78 cnf(1875,plain,
% 60.56/60.78 (P4(a233,a2)),
% 60.56/60.78 inference(scs_inference,[],[70,1825,1827,51,44,1217,1830,351,224,134,339,426,4,429,423,421,437,418])).
% 60.56/60.78 cnf(1878,plain,
% 60.56/60.78 (~P4(x18781,x18781)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1879,plain,
% 60.56/60.78 (~E(f4(a5),f4(a77))),
% 60.56/60.78 inference(scs_inference,[],[70,1825,1827,442,51,44,1217,1830,351,224,134,339,426,4,429,423,421,437,418,23,21])).
% 60.56/60.78 cnf(1881,plain,
% 60.56/60.78 (~E(a2,a233)),
% 60.56/60.78 inference(scs_inference,[],[70,1825,1827,442,1878,51,48,44,1217,1830,351,224,134,339,426,4,429,423,421,437,418,23,21,22,24])).
% 60.56/60.78 cnf(1907,plain,
% 60.56/60.78 (~E(a2,a110)),
% 60.56/60.78 inference(scs_inference,[],[1867,1258,426,4])).
% 60.56/60.78 cnf(1908,plain,
% 60.56/60.78 (~P10(a174,a110,a2)),
% 60.56/60.78 inference(scs_inference,[],[529,1867,1827,1258,426,4,429])).
% 60.56/60.78 cnf(1910,plain,
% 60.56/60.78 (P10(a105,a235,a2)),
% 60.56/60.78 inference(scs_inference,[],[529,1867,1827,1258,226,136,426,4,429,423])).
% 60.56/60.78 cnf(1912,plain,
% 60.56/60.78 (~P8(f4(a77),f4(a1))),
% 60.56/60.78 inference(scs_inference,[],[529,1867,1827,43,1258,1871,226,136,426,4,429,423,421])).
% 60.56/60.78 cnf(1916,plain,
% 60.56/60.78 (P4(a235,a2)),
% 60.56/60.78 inference(scs_inference,[],[529,1867,1827,51,43,1258,1871,352,226,136,348,426,4,429,423,421,437,418])).
% 60.56/60.78 cnf(1919,plain,
% 60.56/60.78 (~P4(x19191,x19191)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1920,plain,
% 60.56/60.78 (~E(f4(a1),f4(a77))),
% 60.56/60.78 inference(scs_inference,[],[529,1867,1827,442,51,43,1258,1871,352,226,136,348,426,4,429,423,421,437,418,23,21])).
% 60.56/60.78 cnf(1922,plain,
% 60.56/60.78 (~E(a2,a235)),
% 60.56/60.78 inference(scs_inference,[],[529,1867,1827,442,1919,51,48,43,1258,1871,352,226,136,348,426,4,429,423,421,437,418,23,21,22,24])).
% 60.56/60.78 cnf(1949,plain,
% 60.56/60.78 (~P10(a240,a5,a2)),
% 60.56/60.78 inference(scs_inference,[],[636,1908,1824,1299,426,4,429])).
% 60.56/60.78 cnf(1951,plain,
% 60.56/60.78 (P10(a107,a237,a2)),
% 60.56/60.78 inference(scs_inference,[],[636,1908,1824,1299,228,138,426,4,429,423])).
% 60.56/60.78 cnf(1953,plain,
% 60.56/60.78 (~P8(f4(a99),f4(a77))),
% 60.56/60.78 inference(scs_inference,[],[636,1908,1824,48,1299,228,138,662,426,4,429,423,421])).
% 60.56/60.78 cnf(1957,plain,
% 60.56/60.78 (P4(a237,a2)),
% 60.56/60.78 inference(scs_inference,[],[636,1908,1824,51,48,1299,353,228,138,662,312,426,4,429,423,421,437,418])).
% 60.56/60.78 cnf(1960,plain,
% 60.56/60.78 (~P4(x19601,x19601)),
% 60.56/60.78 inference(rename_variables,[],[442])).
% 60.56/60.78 cnf(1961,plain,
% 60.56/60.78 (~E(f4(a2),f4(a77))),
% 60.56/60.78 inference(scs_inference,[],[636,1908,1824,442,51,42,48,1299,1912,353,228,138,662,312,426,4,429,423,421,437,418,23,21])).
% 60.56/60.78 cnf(1963,plain,
% 60.56/60.78 (~E(a2,a237)),
% 60.56/60.78 inference(scs_inference,[],[636,1908,1824,442,1960,51,42,48,1299,1912,353,228,138,662,312,426,4,429,423,421,437,418,23,21,22,24])).
% 60.56/60.78 cnf(1964,plain,
% 60.56/60.78 (~P4(x19641,x19641)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(1968,plain,
% 60.56/60.79 (~P4(x19681,x19681)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(1973,plain,
% 60.56/60.79 (~E(a134,a240)),
% 60.56/60.79 inference(scs_inference,[],[636,1908,1824,442,1960,1964,1968,51,42,48,1299,1912,353,228,229,140,138,662,312,426,4,429,423,421,437,418,23,21,22,24,431,419,420,786])).
% 60.56/60.79 cnf(1990,plain,
% 60.56/60.79 (~E(a55,a1)),
% 60.56/60.79 inference(scs_inference,[],[1949,1341,426,4])).
% 60.56/60.79 cnf(1991,plain,
% 60.56/60.79 (~P10(a240,a1,a2)),
% 60.56/60.79 inference(scs_inference,[],[636,1949,1866,1341,426,4,429])).
% 60.56/60.79 cnf(1993,plain,
% 60.56/60.79 (P10(a109,a239,a2)),
% 60.56/60.79 inference(scs_inference,[],[636,1949,1866,1341,230,140,426,4,429,423])).
% 60.56/60.79 cnf(1995,plain,
% 60.56/60.79 (~P8(f4(a99),f4(a66))),
% 60.56/60.79 inference(scs_inference,[],[636,1949,1866,47,1341,1953,230,140,426,4,429,423,421])).
% 60.56/60.79 cnf(1999,plain,
% 60.56/60.79 (P4(a239,a2)),
% 60.56/60.79 inference(scs_inference,[],[636,1949,1866,51,47,1341,1953,358,230,140,426,4,429,423,421,437,418])).
% 60.56/60.79 cnf(2002,plain,
% 60.56/60.79 (~P4(x20021,x20021)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2003,plain,
% 60.56/60.79 (~E(f4(a66),f4(a99))),
% 60.56/60.79 inference(scs_inference,[],[636,1949,1866,442,51,47,1341,1953,358,230,140,426,4,429,423,421,437,418,23,21])).
% 60.56/60.79 cnf(2005,plain,
% 60.56/60.79 (~E(a2,a239)),
% 60.56/60.79 inference(scs_inference,[],[636,1949,1866,442,2002,51,50,47,1341,1953,358,230,140,426,4,429,423,421,437,418,23,21,22,24])).
% 60.56/60.79 cnf(2006,plain,
% 60.56/60.79 (~P4(x20061,x20061)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2010,plain,
% 60.56/60.79 (~P4(x20101,x20101)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2015,plain,
% 60.56/60.79 (~E(a122,a240)),
% 60.56/60.79 inference(scs_inference,[],[636,1949,1866,442,2002,2006,2010,51,50,47,1341,1953,358,230,231,142,140,426,4,429,423,421,437,418,23,21,22,24,431,419,420,719])).
% 60.56/60.79 cnf(2026,plain,
% 60.56/60.79 (~P10(a122,a55,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,1991,1990,1342,426,4,429])).
% 60.56/60.79 cnf(2028,plain,
% 60.56/60.79 (P10(a112,a242,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,1991,1990,1342,232,142,426,4,429,423])).
% 60.56/60.79 cnf(2030,plain,
% 60.56/60.79 (~P8(f4(a99),f4(a55))),
% 60.56/60.79 inference(scs_inference,[],[453,1991,1990,46,1342,1995,232,142,426,4,429,423,421])).
% 60.56/60.79 cnf(2034,plain,
% 60.56/60.79 (P4(a242,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,1991,1990,51,46,1342,1995,359,232,349,142,426,4,429,423,421,437,418])).
% 60.56/60.79 cnf(2037,plain,
% 60.56/60.79 (~P4(x20371,x20371)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2038,plain,
% 60.56/60.79 (~E(f4(a55),f4(a99))),
% 60.56/60.79 inference(scs_inference,[],[453,1991,1990,442,51,46,1342,1995,359,232,349,142,426,4,429,423,421,437,418,23,21])).
% 60.56/60.79 cnf(2040,plain,
% 60.56/60.79 (~E(a2,a242)),
% 60.56/60.79 inference(scs_inference,[],[453,1991,1990,442,2037,51,50,46,1342,1995,359,232,349,142,426,4,429,423,421,437,418,23,21,22,24])).
% 60.56/60.79 cnf(2041,plain,
% 60.56/60.79 (~P4(x20411,x20411)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2042,plain,
% 60.56/60.79 (P10(a242,a112,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,1991,1990,442,2037,51,50,46,1342,1995,359,232,349,142,426,4,429,423,421,437,418,23,21,22,24,431])).
% 60.56/60.79 cnf(2045,plain,
% 60.56/60.79 (~P4(x20451,x20451)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2050,plain,
% 60.56/60.79 (~E(a1,a55)),
% 60.56/60.79 inference(scs_inference,[],[453,1991,1990,442,2037,2041,2045,51,50,46,1342,1995,359,232,233,144,349,142,426,4,429,423,421,437,418,23,21,22,24,431,419,420,855])).
% 60.56/60.79 cnf(2067,plain,
% 60.56/60.79 (~E(a66,a88)),
% 60.56/60.79 inference(scs_inference,[],[2026,1382,426,4])).
% 60.56/60.79 cnf(2068,plain,
% 60.56/60.79 (~P10(a240,a2,a2)),
% 60.56/60.79 inference(scs_inference,[],[636,2026,1907,1382,426,4,429])).
% 60.56/60.79 cnf(2070,plain,
% 60.56/60.79 (P10(a114,a244,a2)),
% 60.56/60.79 inference(scs_inference,[],[636,2026,1907,1382,234,144,426,4,429,423])).
% 60.56/60.79 cnf(2072,plain,
% 60.56/60.79 (~P8(f4(a99),f4(a44))),
% 60.56/60.79 inference(scs_inference,[],[636,2026,1907,45,1382,2030,234,144,426,4,429,423,421])).
% 60.56/60.79 cnf(2076,plain,
% 60.56/60.79 (P4(a244,a2)),
% 60.56/60.79 inference(scs_inference,[],[636,2026,1907,51,45,1382,2030,360,234,358,144,426,4,429,423,421,437,418])).
% 60.56/60.79 cnf(2079,plain,
% 60.56/60.79 (~P4(x20791,x20791)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2080,plain,
% 60.56/60.79 (~E(f4(a44),f4(a99))),
% 60.56/60.79 inference(scs_inference,[],[636,2026,1907,442,51,45,1382,2030,360,234,358,144,426,4,429,423,421,437,418,23,21])).
% 60.56/60.79 cnf(2082,plain,
% 60.56/60.79 (~E(a2,a244)),
% 60.56/60.79 inference(scs_inference,[],[636,2026,1907,442,2079,51,50,45,1382,2030,360,234,358,144,426,4,429,423,421,437,418,23,21,22,24])).
% 60.56/60.79 cnf(2102,plain,
% 60.56/60.79 (~P10(a218,a66,a2)),
% 60.56/60.79 inference(scs_inference,[],[599,2068,2067,1383,426,4,429])).
% 60.56/60.79 cnf(2104,plain,
% 60.56/60.79 (P10(a116,a246,a2)),
% 60.56/60.79 inference(scs_inference,[],[599,2068,2067,1383,236,146,426,4,429,423])).
% 60.56/60.79 cnf(2106,plain,
% 60.56/60.79 (~P8(f4(a99),f4(a5))),
% 60.56/60.79 inference(scs_inference,[],[599,2068,2067,44,1383,2072,236,146,426,4,429,423,421])).
% 60.56/60.79 cnf(2110,plain,
% 60.56/60.79 (P4(a246,a2)),
% 60.56/60.79 inference(scs_inference,[],[599,2068,2067,51,44,1383,2072,361,236,146,313,426,4,429,423,421,437,418])).
% 60.56/60.79 cnf(2113,plain,
% 60.56/60.79 (~P4(x21131,x21131)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2114,plain,
% 60.56/60.79 (~E(f4(a5),f4(a99))),
% 60.56/60.79 inference(scs_inference,[],[599,2068,2067,442,51,44,1383,2072,361,236,146,313,426,4,429,423,421,437,418,23,21])).
% 60.56/60.79 cnf(2116,plain,
% 60.56/60.79 (~E(a2,a246)),
% 60.56/60.79 inference(scs_inference,[],[599,2068,2067,442,2113,51,50,44,1383,2072,361,236,146,313,426,4,429,423,421,437,418,23,21,22,24])).
% 60.56/60.79 cnf(2117,plain,
% 60.56/60.79 (~P4(x21171,x21171)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2121,plain,
% 60.56/60.79 (P10(a246,a116,a2)),
% 60.56/60.79 inference(scs_inference,[],[599,2068,2067,442,2113,2117,51,50,44,1383,2072,361,236,237,146,313,426,4,429,423,421,437,418,23,21,22,24,419,431])).
% 60.56/60.79 cnf(2142,plain,
% 60.56/60.79 (~E(a55,a88)),
% 60.56/60.79 inference(scs_inference,[],[2102,1425,426,4])).
% 60.56/60.79 cnf(2143,plain,
% 60.56/60.79 (~P10(a1,a134,a2)),
% 60.56/60.79 inference(scs_inference,[],[1139,2102,443,1425,426,4,429])).
% 60.56/60.79 cnf(2145,plain,
% 60.56/60.79 (~E(a196,a218)),
% 60.56/60.79 inference(scs_inference,[],[560,1139,2102,443,1425,426,4,429,27])).
% 60.56/60.79 cnf(2146,plain,
% 60.56/60.79 (~E(a122,a134)),
% 60.56/60.79 inference(scs_inference,[],[560,1139,2102,443,1425,426,4,429,27,28])).
% 60.56/60.79 cnf(2147,plain,
% 60.56/60.79 (P10(a118,a248,a2)),
% 60.56/60.79 inference(scs_inference,[],[560,1139,2102,443,1425,238,148,426,4,429,27,28,423])).
% 60.56/60.79 cnf(2149,plain,
% 60.56/60.79 (~P8(f4(a99),f4(a1))),
% 60.56/60.79 inference(scs_inference,[],[560,1139,2102,443,43,1425,2106,238,148,426,4,429,27,28,423,421])).
% 60.56/60.79 cnf(2153,plain,
% 60.56/60.79 (P4(a248,a2)),
% 60.56/60.79 inference(scs_inference,[],[560,1139,2102,443,51,43,1425,2106,362,238,148,331,426,4,429,27,28,423,421,437,418])).
% 60.56/60.79 cnf(2156,plain,
% 60.56/60.79 (~P4(x21561,x21561)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2157,plain,
% 60.56/60.79 (~E(f4(a1),f4(a99))),
% 60.56/60.79 inference(scs_inference,[],[560,1139,2102,443,442,51,43,1425,2106,362,238,148,331,426,4,429,27,28,423,421,437,418,23,21])).
% 60.56/60.79 cnf(2158,plain,
% 60.56/60.79 (~E(f4(a110),f4(a5))),
% 60.56/60.79 inference(scs_inference,[],[560,1139,2102,443,442,51,50,43,1425,2106,362,238,148,331,426,4,429,27,28,423,421,437,418,23,21,22])).
% 60.56/60.79 cnf(2159,plain,
% 60.56/60.79 (~E(a2,a248)),
% 60.56/60.79 inference(scs_inference,[],[560,1139,2102,443,442,2156,51,50,43,1425,2106,362,238,148,331,426,4,429,27,28,423,421,437,418,23,21,22,24])).
% 60.56/60.79 cnf(2160,plain,
% 60.56/60.79 (~P4(x21601,x21601)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2161,plain,
% 60.56/60.79 (~P8(f251(f4(a99),f4(a99)),f251(f4(a99),f4(a99)))),
% 60.56/60.79 inference(scs_inference,[],[560,1139,2102,443,442,2156,2160,51,50,43,1425,2106,362,238,239,148,331,426,4,429,27,28,423,421,437,418,23,21,22,24,419])).
% 60.56/60.79 cnf(2186,plain,
% 60.56/60.79 (~P10(a218,a55,a2)),
% 60.56/60.79 inference(scs_inference,[],[599,2143,2142,1428,426,4,429])).
% 60.56/60.79 cnf(2188,plain,
% 60.56/60.79 (P10(a120,a250,a2)),
% 60.56/60.79 inference(scs_inference,[],[599,2143,2142,1428,240,150,426,4,429,423])).
% 60.56/60.79 cnf(2190,plain,
% 60.56/60.79 (P6(f4(a2),f4(a77),f4(a2),f4(a77))),
% 60.56/60.79 inference(scs_inference,[],[599,2143,2142,1428,368,240,150,426,4,429,423,437])).
% 60.56/60.79 cnf(2192,plain,
% 60.56/60.79 (P4(a250,a2)),
% 60.56/60.79 inference(scs_inference,[],[599,2143,2142,51,1428,368,240,150,426,4,429,423,437,418])).
% 60.56/60.79 cnf(2195,plain,
% 60.56/60.79 (~P4(x21951,x21951)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2196,plain,
% 60.56/60.79 (~E(f4(a2),f4(a99))),
% 60.56/60.79 inference(scs_inference,[],[599,2143,2142,442,51,42,1428,2149,368,240,150,426,4,429,423,437,418,23,21])).
% 60.56/60.79 cnf(2197,plain,
% 60.56/60.79 (~E(f4(a110),f4(a1))),
% 60.56/60.79 inference(scs_inference,[],[599,2143,2142,442,51,42,50,1428,2149,368,240,150,426,4,429,423,437,418,23,21,22])).
% 60.56/60.79 cnf(2198,plain,
% 60.56/60.79 (~E(a2,a250)),
% 60.56/60.79 inference(scs_inference,[],[599,2143,2142,442,2195,51,42,50,1428,2149,368,240,150,426,4,429,423,437,418,23,21,22,24])).
% 60.56/60.79 cnf(2199,plain,
% 60.56/60.79 (~P4(x21991,x21991)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2201,plain,
% 60.56/60.79 (~P4(x22011,x22011)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2208,plain,
% 60.56/60.79 (~E(a88,a55)),
% 60.56/60.79 inference(scs_inference,[],[599,2143,2142,442,2195,2199,2201,51,42,50,1428,2149,368,240,241,152,150,426,4,429,423,437,418,23,21,22,24,419,431,420,928])).
% 60.56/60.79 cnf(2226,plain,
% 60.56/60.79 (~E(a44,a88)),
% 60.56/60.79 inference(scs_inference,[],[2186,1467,426,4])).
% 60.56/60.79 cnf(2227,plain,
% 60.56/60.79 (~P10(a1,a174,a2)),
% 60.56/60.79 inference(scs_inference,[],[1173,2186,443,1467,426,4,429])).
% 60.56/60.79 cnf(2229,plain,
% 60.56/60.79 (P10(a124,a253,a2)),
% 60.56/60.79 inference(scs_inference,[],[1173,2186,443,1467,242,152,426,4,429,423])).
% 60.56/60.79 cnf(2233,plain,
% 60.56/60.79 (P4(a253,a2)),
% 60.56/60.79 inference(scs_inference,[],[1173,2186,443,51,1467,369,242,350,152,426,4,429,423,437,418])).
% 60.56/60.79 cnf(2236,plain,
% 60.56/60.79 (~P4(x22361,x22361)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2237,plain,
% 60.56/60.79 (~E(a2,a253)),
% 60.56/60.79 inference(scs_inference,[],[1173,2186,443,442,2236,51,1467,369,242,350,152,426,4,429,423,437,418,23,24])).
% 60.56/60.79 cnf(2256,plain,
% 60.56/60.79 (~P10(a218,a44,a2)),
% 60.56/60.79 inference(scs_inference,[],[599,2227,2226,1470,426,4,429])).
% 60.56/60.79 cnf(2258,plain,
% 60.56/60.79 (P10(a126,a255,a2)),
% 60.56/60.79 inference(scs_inference,[],[599,2227,2226,1470,244,154,426,4,429,423])).
% 60.56/60.79 cnf(2262,plain,
% 60.56/60.79 (P4(a255,a2)),
% 60.56/60.79 inference(scs_inference,[],[599,2227,2226,51,1470,370,244,359,154,426,4,429,423,437,418])).
% 60.56/60.79 cnf(2264,plain,
% 60.56/60.79 (~E(a255,a2)),
% 60.56/60.79 inference(scs_inference,[],[599,2227,2226,442,51,1470,370,244,359,154,426,4,429,423,437,418,23])).
% 60.56/60.79 cnf(2265,plain,
% 60.56/60.79 (~P4(x22651,x22651)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2267,plain,
% 60.56/60.79 (~P4(x22671,x22671)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2269,plain,
% 60.56/60.79 (~P4(x22691,x22691)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2271,plain,
% 60.56/60.79 (P10(a255,a126,a2)),
% 60.56/60.79 inference(scs_inference,[],[599,2227,2226,442,2265,2267,51,1470,370,244,245,359,154,426,4,429,423,437,418,23,24,419,431])).
% 60.56/60.79 cnf(2276,plain,
% 60.56/60.79 (~E(a88,a44)),
% 60.56/60.79 inference(scs_inference,[],[599,2227,2226,442,2265,2267,2269,51,1470,370,244,245,156,359,154,426,4,429,423,437,418,23,24,419,431,420,928])).
% 60.56/60.79 cnf(2277,plain,
% 60.56/60.79 (~E(a174,a218)),
% 60.56/60.79 inference(scs_inference,[],[599,2227,2226,442,2265,2267,2269,51,1470,370,244,245,156,359,154,426,4,429,423,437,418,23,24,419,431,420,928,890])).
% 60.56/60.79 cnf(2294,plain,
% 60.56/60.79 (~E(a5,a88)),
% 60.56/60.79 inference(scs_inference,[],[2256,1508,426,4])).
% 60.56/60.79 cnf(2295,plain,
% 60.56/60.79 (~P10(a3,a88,a66)),
% 60.56/60.79 inference(scs_inference,[],[70,2256,2276,1508,426,4,429])).
% 60.56/60.79 cnf(2297,plain,
% 60.56/60.79 (P10(a128,a257,a2)),
% 60.56/60.79 inference(scs_inference,[],[70,2256,2276,1508,246,156,426,4,429,423])).
% 60.56/60.79 cnf(2301,plain,
% 60.56/60.79 (P4(a257,a2)),
% 60.56/60.79 inference(scs_inference,[],[70,2256,2276,51,1508,371,246,368,156,426,4,429,423,437,418])).
% 60.56/60.79 cnf(2303,plain,
% 60.56/60.79 (~E(a257,a2)),
% 60.56/60.79 inference(scs_inference,[],[70,2256,2276,442,51,1508,371,246,368,156,426,4,429,423,437,418,23])).
% 60.56/60.79 cnf(2304,plain,
% 60.56/60.79 (~P4(x23041,x23041)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2306,plain,
% 60.56/60.79 (~P4(x23061,x23061)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2310,plain,
% 60.56/60.79 (P10(a257,a128,a2)),
% 60.56/60.79 inference(scs_inference,[],[70,2256,2276,442,2304,2306,51,1508,371,246,247,368,156,426,4,429,423,437,418,23,24,419,431])).
% 60.56/60.79 cnf(2325,plain,
% 60.56/60.79 (~P10(a174,a88,a2)),
% 60.56/60.79 inference(scs_inference,[],[529,2295,2276,1511,426,4,429])).
% 60.56/60.79 cnf(2331,plain,
% 60.56/60.79 (P4(a259,a2)),
% 60.56/60.79 inference(scs_inference,[],[529,2295,2276,51,1511,378,248,158,426,4,429,423,437,418])).
% 60.56/60.79 cnf(2334,plain,
% 60.56/60.79 (~P4(x23341,x23341)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2336,plain,
% 60.56/60.79 (~P4(x23361,x23361)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2339,plain,
% 60.56/60.79 (~P8(f251(f4(a99),f4(a110)),f251(f4(a99),f4(a110)))),
% 60.56/60.79 inference(scs_inference,[],[529,2295,2276,442,2334,2336,51,1511,378,248,249,158,426,4,429,423,437,418,23,24,431,419])).
% 60.56/60.79 cnf(2361,plain,
% 60.56/60.79 (~E(a1,a88)),
% 60.56/60.79 inference(scs_inference,[],[2325,1549,426,4])).
% 60.56/60.79 cnf(2362,plain,
% 60.56/60.79 (~P10(a218,a5,a2)),
% 60.56/60.79 inference(scs_inference,[],[599,2325,2294,1549,426,4,429])).
% 60.56/60.79 cnf(2364,plain,
% 60.56/60.79 (~E(a218,a174)),
% 60.56/60.79 inference(scs_inference,[],[599,2325,2294,1549,426,4,429,27])).
% 60.56/60.79 cnf(2372,plain,
% 60.56/60.79 (~P4(x23721,x23721)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2374,plain,
% 60.56/60.79 (~P4(x23741,x23741)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2376,plain,
% 60.56/60.79 (~P4(x23761,x23761)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2383,plain,
% 60.56/60.79 (~E(a134,a218)),
% 60.56/60.79 inference(scs_inference,[],[599,2325,2294,442,2372,2374,2376,51,1549,379,250,288,270,360,160,426,4,429,27,423,437,418,23,24,419,431,420,786])).
% 60.56/60.79 cnf(2402,plain,
% 60.56/60.79 (~P10(a218,a1,a2)),
% 60.56/60.79 inference(scs_inference,[],[599,2362,2361,1552,426,4,429])).
% 60.56/60.79 cnf(2406,plain,
% 60.56/60.79 (P6(f4(a5),f4(a77),f4(a1),f4(a110))),
% 60.56/60.79 inference(scs_inference,[],[599,2362,2361,1552,380,298,369,270,426,4,429,423,437])).
% 60.56/60.79 cnf(2411,plain,
% 60.56/60.79 (~P4(x24111,x24111)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2413,plain,
% 60.56/60.79 (~P4(x24131,x24131)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2415,plain,
% 60.56/60.79 (~P4(x24151,x24151)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2422,plain,
% 60.56/60.79 (~E(a122,a218)),
% 60.56/60.79 inference(scs_inference,[],[599,2362,2361,442,2411,2413,2415,51,1552,380,298,287,269,369,270,426,4,429,423,437,418,23,24,419,431,420,719])).
% 60.56/60.79 cnf(2423,plain,
% 60.56/60.79 (~E(a88,a1)),
% 60.56/60.79 inference(scs_inference,[],[599,2362,2361,442,2411,2413,2415,51,1552,380,298,287,269,369,270,426,4,429,423,437,418,23,24,419,431,420,719,928])).
% 60.56/60.79 cnf(2433,plain,
% 60.56/60.79 (~E(a2,a88)),
% 60.56/60.79 inference(scs_inference,[],[2402,1593,426,4])).
% 60.56/60.79 cnf(2434,plain,
% 60.56/60.79 (~P10(a122,a88,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,2402,2423,1593,426,4,429])).
% 60.56/60.79 cnf(2471,plain,
% 60.56/60.79 (~P10(a218,a2,a2)),
% 60.56/60.79 inference(scs_inference,[],[599,2434,2433,1594,426,4,429])).
% 60.56/60.79 cnf(2473,plain,
% 60.56/60.79 (~E(a218,a122)),
% 60.56/60.79 inference(scs_inference,[],[599,2434,2433,1594,426,4,429,27])).
% 60.56/60.79 cnf(2476,plain,
% 60.56/60.79 (P6(f4(a1),f4(a66),f4(a44),f4(a110))),
% 60.56/60.79 inference(scs_inference,[],[599,2434,2433,1594,389,296,361,268,426,4,429,27,423,437])).
% 60.56/60.79 cnf(2481,plain,
% 60.56/60.79 (~P4(x24811,x24811)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2483,plain,
% 60.56/60.79 (~P4(x24831,x24831)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2487,plain,
% 60.56/60.79 (~P4(x24871,x24871)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2494,plain,
% 60.56/60.79 (P9(x24941,f121(f251(f4(a2),f4(a1))))+~E(a6,x24941)),
% 60.56/60.79 inference(scs_inference,[],[599,2434,2433,442,2481,2483,2487,51,1594,389,71,296,306,257,361,268,426,4,429,27,423,437,418,23,24,431,419,420,415,25])).
% 60.56/60.79 cnf(2509,plain,
% 60.56/60.79 (~P10(a44,a218,a2)),
% 60.56/60.79 inference(scs_inference,[],[2364,2471,520,1638,426,4,429])).
% 60.56/60.79 cnf(2513,plain,
% 60.56/60.79 (P6(f4(a2),f4(a110),f4(a2),f4(a110))),
% 60.56/60.79 inference(scs_inference,[],[2364,2471,520,1638,398,285,257,426,4,429,423,437])).
% 60.56/60.79 cnf(2539,plain,
% 60.56/60.79 (~P10(a1,a218,a2)),
% 60.56/60.79 inference(scs_inference,[],[2473,2509,443,1679,426,4,429])).
% 60.56/60.79 cnf(2576,plain,
% 60.56/60.79 (~P10(a2,a88,a2)),
% 60.56/60.79 inference(scs_inference,[],[2539,461,1329,1680,426,4,429])).
% 60.56/60.79 cnf(2580,plain,
% 60.56/60.79 (P6(f4(a5),f4(a1),f4(a66),f4(a99))),
% 60.56/60.79 inference(scs_inference,[],[2539,461,1329,1680,294,370,266,323,426,4,429,423,437])).
% 60.56/60.79 cnf(2606,plain,
% 60.56/60.79 (~P10(a2,a1,a2)),
% 60.56/60.79 inference(scs_inference,[],[2576,461,474,1712,426,4,429])).
% 60.56/60.79 cnf(2614,plain,
% 60.56/60.79 (~E(f4(a2),f4(a5))),
% 60.56/60.79 inference(scs_inference,[],[2576,461,474,51,42,514,1712,283,371,255,350,426,4,429,423,437,418,21])).
% 60.56/60.79 cnf(2615,plain,
% 60.56/60.79 (~E(f4(a5),f4(a2))),
% 60.56/60.79 inference(scs_inference,[],[2576,461,474,51,42,43,466,514,1712,283,371,255,350,426,4,429,423,437,418,21,22])).
% 60.56/60.79 cnf(2645,plain,
% 60.56/60.79 (~P10(a2,a66,a2)),
% 60.56/60.79 inference(scs_inference,[],[2606,461,1170,1713,426,4,429])).
% 60.56/60.79 cnf(2654,plain,
% 60.56/60.79 (~P4(x26541,x26541)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2656,plain,
% 60.56/60.79 (~P4(x26561,x26561)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2660,plain,
% 60.56/60.79 (~P4(x26601,x26601)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2667,plain,
% 60.56/60.79 (P9(x26671,f121(f251(f4(a55),f4(a1))))+~E(a38,x26671)),
% 60.56/60.79 inference(scs_inference,[],[2606,461,1170,442,2654,2656,2660,51,1713,75,303,282,264,378,379,275,426,4,429,423,437,418,23,24,431,419,420,415,25])).
% 60.56/60.79 cnf(2682,plain,
% 60.56/60.79 (~P10(a2,a77,a2)),
% 60.56/60.79 inference(scs_inference,[],[2645,461,1246,1754,426,4,429])).
% 60.56/60.79 cnf(2691,plain,
% 60.56/60.79 (~P4(x26911,x26911)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2693,plain,
% 60.56/60.79 (~P4(x26931,x26931)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2695,plain,
% 60.56/60.79 (~P4(x26951,x26951)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2706,plain,
% 60.56/60.79 (P9(x27061,f121(f251(f4(a77),f4(a1))))+~E(a40,x27061)),
% 60.56/60.79 inference(scs_inference,[],[2645,461,1246,442,2691,2693,2695,51,1754,2406,377,77,292,302,253,380,264,324,426,4,429,423,437,418,23,24,419,431,420,415,13,14,25])).
% 60.56/60.79 cnf(2719,plain,
% 60.56/60.79 (~P10(a2,a110,a2)),
% 60.56/60.79 inference(scs_inference,[],[2682,461,1413,1755,426,4,429])).
% 60.56/60.79 cnf(2749,plain,
% 60.56/60.79 (~P10(a2,a44,a2)),
% 60.56/60.79 inference(scs_inference,[],[2719,461,1455,1795,426,4,429])).
% 60.56/60.79 cnf(2779,plain,
% 60.56/60.79 (~P10(a2,a55,a2)),
% 60.56/60.79 inference(scs_inference,[],[2749,461,1538,1796,426,4,429])).
% 60.56/60.79 cnf(2788,plain,
% 60.56/60.79 (~P4(x27881,x27881)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2790,plain,
% 60.56/60.79 (~P4(x27901,x27901)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2794,plain,
% 60.56/60.79 (~P4(x27941,x27941)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2806,plain,
% 60.56/60.79 (P9(x28061,f121(f251(f4(a2),f4(a5))))+~E(a45,x28061)),
% 60.56/60.79 inference(scs_inference,[],[2042,2749,461,1538,442,2788,2790,2794,51,2513,1796,383,81,290,300,251,262,334,310,426,4,429,423,437,418,23,24,431,419,420,415,17,14,26,29,10,25])).
% 60.56/60.79 cnf(2815,plain,
% 60.56/60.79 (~E(a5,a2)),
% 60.56/60.79 inference(scs_inference,[],[2779,2615,426,4])).
% 60.56/60.79 cnf(2816,plain,
% 60.56/60.79 (~P10(a2,a99,a2)),
% 60.56/60.79 inference(scs_inference,[],[2779,461,1782,2615,426,4,429])).
% 60.56/60.79 cnf(2825,plain,
% 60.56/60.79 (~P4(x28251,x28251)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2827,plain,
% 60.56/60.79 (~P4(x28271,x28271)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2829,plain,
% 60.56/60.79 (~P4(x28291,x28291)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2842,plain,
% 60.56/60.79 (P9(x28421,f121(f251(f4(a5),f4(a5))))+~E(a47,x28421)),
% 60.56/60.79 inference(scs_inference,[],[2779,461,1782,442,2825,2827,2829,51,2615,2476,384,83,279,289,271,251,343,329,426,4,429,423,418,437,23,24,419,431,420,415,15,11,13,12,25])).
% 60.56/60.79 cnf(2853,plain,
% 60.56/60.79 (~P10(a2,a5,a2)),
% 60.56/60.79 inference(scs_inference,[],[2816,461,2815,1838,426,4,429])).
% 60.56/60.79 cnf(2862,plain,
% 60.56/60.79 (~P4(x28621,x28621)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2864,plain,
% 60.56/60.79 (~P4(x28641,x28641)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2870,plain,
% 60.56/60.79 (~E(a134,a2)),
% 60.56/60.79 inference(scs_inference,[],[2816,461,2815,442,2862,2864,51,1838,299,307,271,358,359,426,4,429,423,437,418,23,24,431,419,786])).
% 60.56/60.79 cnf(2881,plain,
% 60.56/60.79 (~P10(a2,a134,a2)),
% 60.56/60.79 inference(scs_inference,[],[2853,2870,461,1879,426,4,429])).
% 60.56/60.79 cnf(2883,plain,
% 60.56/60.79 (P10(a55,a185,a2)),
% 60.56/60.79 inference(scs_inference,[],[2853,2870,461,55,1879,64,426,4,429,423])).
% 60.56/60.79 cnf(2890,plain,
% 60.56/60.79 (~P4(x28901,x28901)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2893,plain,
% 60.56/60.79 (P10(a185,a55,a2)),
% 60.56/60.79 inference(scs_inference,[],[2853,2870,461,442,2890,51,55,1879,64,360,340,426,4,429,423,437,418,23,24,431])).
% 60.56/60.79 cnf(2898,plain,
% 60.56/60.79 (~E(a185,a122)),
% 60.56/60.79 inference(scs_inference,[],[2026,2853,2870,461,442,2890,51,55,1879,2580,64,360,340,426,4,429,423,437,418,23,24,431,415,14,27])).
% 60.56/60.79 cnf(2913,plain,
% 60.56/60.79 (~P10(a185,a1,a2)),
% 60.56/60.79 inference(scs_inference,[],[2050,2881,2893,1920,426,4,429])).
% 60.56/60.79 cnf(2915,plain,
% 60.56/60.79 (P10(a77,a207,a2)),
% 60.56/60.79 inference(scs_inference,[],[2050,2881,2893,57,66,1920,426,4,429,423])).
% 60.56/60.79 cnf(2922,plain,
% 60.56/60.79 (~P4(x29221,x29221)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2923,plain,
% 60.56/60.79 (~E(a2,a207)),
% 60.56/60.79 inference(scs_inference,[],[2050,2881,2893,442,2922,51,57,66,1920,362,313,426,4,429,423,437,418,23,24])).
% 60.56/60.79 cnf(2925,plain,
% 60.56/60.79 (P10(a207,a77,a2)),
% 60.56/60.79 inference(scs_inference,[],[2050,2881,2893,442,2922,51,57,66,1920,362,313,426,4,429,423,437,418,23,24,431])).
% 60.56/60.79 cnf(2927,plain,
% 60.56/60.79 (~E(a122,a185)),
% 60.56/60.79 inference(scs_inference,[],[2050,2881,2893,442,2922,51,57,66,1920,362,313,426,4,429,423,437,418,23,24,431,719])).
% 60.56/60.79 cnf(2931,plain,
% 60.56/60.79 (~E(a207,a218)),
% 60.56/60.79 inference(scs_inference,[],[1288,2050,2121,2881,2893,442,2922,51,57,66,1920,362,313,426,4,429,423,437,418,23,24,431,719,415,28,27])).
% 60.56/60.79 cnf(2941,plain,
% 60.56/60.79 (~P10(a185,a88,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,2893,2208,2913,512,1961,426,4,424,429])).
% 60.56/60.79 cnf(2950,plain,
% 60.56/60.79 (~P4(x29501,x29501)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(2953,plain,
% 60.56/60.79 (P10(a229,a99,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,2893,2208,2913,442,2950,51,59,68,512,1961,361,331,426,4,424,429,423,437,418,23,24,431])).
% 60.56/60.79 cnf(2957,plain,
% 60.56/60.79 (P4(a174,a122)),
% 60.56/60.79 inference(scs_inference,[],[453,2893,2208,2913,1173,442,2950,51,59,68,512,1961,361,331,426,4,424,429,423,437,418,23,24,431,415,414])).
% 60.56/60.79 cnf(2960,plain,
% 60.56/60.79 (~E(a229,a218)),
% 60.56/60.79 inference(scs_inference,[],[453,1498,2893,2208,2913,1173,442,2950,51,59,68,512,1961,361,331,426,4,424,429,423,437,418,23,24,431,415,414,20,27])).
% 60.56/60.79 cnf(2965,plain,
% 60.56/60.79 (P9(x29651,f121(f251(f4(a77),f4(a5))))+~E(a51,x29651)),
% 60.56/60.79 inference(scs_inference,[],[453,1498,2893,2208,2913,1173,442,2950,51,87,59,68,512,1961,386,361,331,426,4,424,429,423,437,418,23,24,431,415,414,20,27,19,11,13,12,25])).
% 60.56/60.79 cnf(2979,plain,
% 60.56/60.79 (~P10(a185,a110,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,2893,1743,2941,2957,543,2003,426,415,4,424,429])).
% 60.56/60.79 cnf(2985,plain,
% 60.56/60.79 (P4(a135,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,2893,1743,2941,2957,51,71,161,543,2003,368,369,426,415,4,424,429,423,437,418])).
% 60.56/60.79 cnf(3013,plain,
% 60.56/60.79 (~P10(a207,a88,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,2925,1290,2979,582,2038,2985,426,415,4,424,429])).
% 60.56/60.79 cnf(3019,plain,
% 60.56/60.79 (P4(a147,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,2925,1290,2979,51,73,163,582,2038,2985,370,341,426,415,4,424,429,423,437,418])).
% 60.56/60.79 cnf(3022,plain,
% 60.56/60.79 (~P4(x30221,x30221)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(3027,plain,
% 60.56/60.79 (P4(a218,a122)),
% 60.56/60.79 inference(scs_inference,[],[453,2925,1290,2979,2473,442,3022,51,73,163,582,2038,2985,370,341,426,415,4,424,429,423,437,418,23,24,431,414])).
% 60.56/60.79 cnf(3043,plain,
% 60.56/60.79 (~P4(a122,a218)),
% 60.56/60.79 inference(scs_inference,[],[3013,3027,426,415])).
% 60.56/60.79 cnf(3048,plain,
% 60.56/60.79 (~P10(a207,a110,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,2925,1582,3013,3027,619,2080,426,415,4,424,429])).
% 60.56/60.79 cnf(3054,plain,
% 60.56/60.79 (P4(a168,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,2925,1582,3013,3027,51,75,165,619,2080,371,323,426,415,4,424,429,423,437,418])).
% 60.56/60.79 cnf(3057,plain,
% 60.56/60.79 (~P4(x30571,x30571)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(3070,plain,
% 60.56/60.79 (P4(a240,a122)),
% 60.56/60.79 inference(scs_inference,[],[453,2925,2015,1582,3013,3027,441,621,442,3057,51,75,165,69,619,2080,371,323,426,415,4,424,429,423,437,418,23,24,431,414,19,28,25,410,2,412])).
% 60.56/60.79 cnf(3075,plain,
% 60.56/60.79 (~P4(a122,a240)),
% 60.56/60.79 inference(scs_inference,[],[3070,3048,426,415])).
% 60.56/60.79 cnf(3080,plain,
% 60.56/60.79 (~P10(a229,a110,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,2953,3070,1332,3048,656,2114,426,415,4,424,429])).
% 60.56/60.79 cnf(3086,plain,
% 60.56/60.79 (P4(a170,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,2953,3070,1332,3048,51,77,167,656,2114,378,380,426,415,4,424,429,423,437,418])).
% 60.56/60.79 cnf(3117,plain,
% 60.56/60.79 (~P10(a1,a185,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3080,2898,443,693,2157,3019,426,415,4,424,429])).
% 60.56/60.79 cnf(3123,plain,
% 60.56/60.79 (P4(a172,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3080,2898,443,51,79,169,693,2157,3019,379,315,426,415,4,424,429,423,437,418])).
% 60.56/60.79 cnf(3126,plain,
% 60.56/60.79 (~P4(x31261,x31261)),
% 60.56/60.79 inference(rename_variables,[],[442])).
% 60.56/60.79 cnf(3127,plain,
% 60.56/60.79 (~E(a2,a172)),
% 60.56/60.79 inference(scs_inference,[],[453,3080,2898,443,442,3126,51,79,169,693,2157,3019,3086,379,315,426,415,4,424,429,423,437,418,23,24])).
% 60.56/60.79 cnf(3154,plain,
% 60.56/60.79 (~P10(a5,a122,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,2146,3117,485,730,2158,3054,426,415,4,424,429])).
% 60.56/60.79 cnf(3160,plain,
% 60.56/60.79 (P4(a175,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,2146,3117,485,51,81,171,730,2158,3054,330,328,426,415,4,424,429,423,437,418])).
% 60.56/60.79 cnf(3191,plain,
% 60.56/60.79 (~P10(a88,a240,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,1416,3154,586,759,2196,3160,426,415,4,424,429])).
% 60.56/60.79 cnf(3197,plain,
% 60.56/60.79 (P4(a177,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,1416,3154,586,51,83,173,759,2196,3160,352,339,426,415,4,424,429,423,437,418])).
% 60.56/60.79 cnf(3228,plain,
% 60.56/60.79 (~P10(a88,a174,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,2277,3191,586,796,2197,3197,426,415,4,424,429])).
% 60.56/60.79 cnf(3234,plain,
% 60.56/60.79 (P4(a179,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,2277,3191,586,51,85,175,796,2197,3197,351,348,426,415,4,424,429,423,437,418])).
% 60.56/60.79 cnf(3265,plain,
% 60.56/60.79 (~P10(a88,a122,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,2422,3228,586,826,2614,3234,426,415,4,424,429])).
% 60.56/60.79 cnf(3271,plain,
% 60.56/60.79 (P4(a181,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,2422,3228,586,51,87,177,826,2614,3234,353,321,426,415,4,424,429,423,437,418])).
% 60.56/60.79 cnf(3301,plain,
% 60.56/60.79 (~P10(a88,a134,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,2383,3265,586,863,3271,426,415,424,429])).
% 60.56/60.79 cnf(3307,plain,
% 60.56/60.79 (P4(a183,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,2383,3265,586,51,89,179,863,3271,334,319,426,415,424,429,423,437,418])).
% 60.56/60.79 cnf(3337,plain,
% 60.56/60.79 (~P10(a88,a196,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,2145,3301,586,900,3307,426,415,424,429])).
% 60.56/60.79 cnf(3341,plain,
% 60.56/60.79 (~E(a218,a134)),
% 60.56/60.79 inference(scs_inference,[],[453,2145,3301,586,91,181,900,3307,426,415,424,429,423,28])).
% 60.56/60.79 cnf(3342,plain,
% 60.56/60.79 (P4(a186,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,2145,3301,586,51,91,181,900,3307,426,415,424,429,423,28,418])).
% 60.56/60.79 cnf(3373,plain,
% 60.56/60.79 (~P10(a5,a218,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3337,3341,485,941,3342,426,415,424,429])).
% 60.56/60.79 cnf(3377,plain,
% 60.56/60.79 (~E(a218,a196)),
% 60.56/60.79 inference(scs_inference,[],[453,3337,3341,485,586,93,183,941,3342,426,415,424,429,423,28])).
% 60.56/60.79 cnf(3378,plain,
% 60.56/60.79 (P4(a188,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3337,3341,485,586,51,93,183,941,3342,426,415,424,429,423,28,418])).
% 60.56/60.79 cnf(3408,plain,
% 60.56/60.79 (~P10(a66,a218,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3373,3377,549,973,3378,426,415,424,429])).
% 60.56/60.79 cnf(3412,plain,
% 60.56/60.79 (P4(a190,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3373,3377,549,51,95,185,973,3378,426,415,424,429,423,418])).
% 60.56/60.79 cnf(3444,plain,
% 60.56/60.79 (~P10(a88,a207,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,2931,3408,586,1019,3412,426,415,424,429])).
% 60.56/60.79 cnf(3448,plain,
% 60.56/60.79 (P4(a192,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,2931,3408,586,51,97,187,1019,3412,426,415,424,429,423,418])).
% 60.56/60.79 cnf(3479,plain,
% 60.56/60.79 (~P10(a88,a229,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,2960,3444,586,1058,3448,426,415,424,429])).
% 60.56/60.79 cnf(3483,plain,
% 60.56/60.79 (P4(a194,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,2960,3444,586,51,99,189,1058,3448,426,415,424,429,423,418])).
% 60.56/60.79 cnf(3512,plain,
% 60.56/60.79 (~P10(a50,a2,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3479,904,1099,908,3483,426,415,424,429])).
% 60.56/60.79 cnf(3516,plain,
% 60.56/60.79 (P4(a197,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3479,904,51,101,191,1099,908,3483,426,415,424,429,423,418])).
% 60.56/60.79 cnf(3547,plain,
% 60.56/60.79 (~P10(a52,a2,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3512,937,1142,947,3516,426,415,424,429])).
% 60.56/60.79 cnf(3551,plain,
% 60.56/60.79 (P4(a199,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3512,937,51,103,193,1142,947,3516,426,415,424,429,423,418])).
% 60.56/60.79 cnf(3581,plain,
% 60.56/60.79 (~P10(a65,a2,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3547,1176,1174,1186,3551,426,415,424,429])).
% 60.56/60.79 cnf(3585,plain,
% 60.56/60.79 (P4(a201,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3547,1176,51,105,195,1174,1186,3551,426,415,424,429,423,418])).
% 60.56/60.79 cnf(3615,plain,
% 60.56/60.79 (~P10(a68,a2,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3581,1209,1213,1220,3585,426,415,424,429])).
% 60.56/60.79 cnf(3619,plain,
% 60.56/60.79 (P4(a203,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3581,1209,51,107,197,1213,1220,3585,426,415,424,429,423,418])).
% 60.56/60.79 cnf(3648,plain,
% 60.56/60.79 (~P10(a70,a2,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3615,1254,1250,1261,3619,426,415,424,429])).
% 60.56/60.79 cnf(3652,plain,
% 60.56/60.79 (P4(a205,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3615,1254,51,109,199,1250,1261,3619,426,415,424,429,423,418])).
% 60.56/60.79 cnf(3682,plain,
% 60.56/60.79 (~P10(a72,a2,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3648,1297,1295,1303,3652,426,415,424,429])).
% 60.56/60.79 cnf(3686,plain,
% 60.56/60.79 (P4(a208,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3648,1297,51,111,201,1295,1303,3652,426,415,424,429,423,418])).
% 60.56/60.79 cnf(3715,plain,
% 60.56/60.79 (~P10(a74,a2,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3682,1333,1339,1345,3686,426,415,424,429])).
% 60.56/60.79 cnf(3719,plain,
% 60.56/60.79 (P4(a210,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3682,1333,51,113,203,1339,1345,3686,426,415,424,429,423,418])).
% 60.56/60.79 cnf(3748,plain,
% 60.56/60.79 (~P10(a76,a2,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3715,1378,1374,1386,3719,426,415,424,429])).
% 60.56/60.79 cnf(3752,plain,
% 60.56/60.79 (P4(a212,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3715,1378,51,115,205,1374,1386,3719,426,415,424,429,423,418])).
% 60.56/60.79 cnf(3754,plain,
% 60.56/60.79 (P6(f4(a1),f4(a1),f4(a77),f4(a99))),
% 60.56/60.79 inference(scs_inference,[],[453,3715,1378,51,115,205,1374,1386,3719,324,379,426,415,424,429,423,418,437])).
% 60.56/60.79 cnf(3782,plain,
% 60.56/60.79 (~P10(a79,a2,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3748,1417,1421,1429,3752,426,415,424,429])).
% 60.56/60.79 cnf(3786,plain,
% 60.56/60.79 (P4(a214,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3748,1417,51,117,207,1421,1429,3752,426,415,424,429,423,418])).
% 60.56/60.79 cnf(3815,plain,
% 60.56/60.79 (~P10(a81,a2,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3782,1459,1465,1471,3786,426,415,424,429])).
% 60.56/60.79 cnf(3819,plain,
% 60.56/60.79 (P4(a216,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3782,1459,51,119,209,1465,1471,3786,426,415,424,429,423,418])).
% 60.56/60.79 cnf(3821,plain,
% 60.56/60.79 (P6(f4(a66),f4(a5),f4(a2),f4(a88))),
% 60.56/60.79 inference(scs_inference,[],[453,3782,1459,51,119,209,1465,1471,3786,333,328,426,415,424,429,423,418,437])).
% 60.56/60.79 cnf(3848,plain,
% 60.56/60.79 (~P10(a83,a2,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3815,1500,1504,1512,3819,426,415,424,429])).
% 60.56/60.79 cnf(3852,plain,
% 60.56/60.79 (P4(a219,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3815,1500,51,121,211,1504,1512,3819,426,415,424,429,423,418])).
% 60.56/60.79 cnf(3882,plain,
% 60.56/60.79 (~P10(a85,a2,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3848,1541,1545,1553,3852,426,415,424,429])).
% 60.56/60.79 cnf(3886,plain,
% 60.56/60.79 (P4(a221,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3848,1541,51,123,213,1545,1553,3852,426,415,424,429,423,418])).
% 60.56/60.79 cnf(3917,plain,
% 60.56/60.79 (~P10(a87,a2,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3882,1583,1587,1595,3886,426,415,424,429])).
% 60.56/60.79 cnf(3921,plain,
% 60.56/60.79 (P4(a223,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3882,1583,51,125,215,1587,1595,3886,426,415,424,429,423,418])).
% 60.56/60.79 cnf(3949,plain,
% 60.56/60.79 (~P10(a90,a2,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3917,1627,1631,1639,3921,426,415,424,429])).
% 60.56/60.79 cnf(3953,plain,
% 60.56/60.79 (P4(a225,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3917,1627,51,127,217,1631,1639,3921,426,415,424,429,423,418])).
% 60.56/60.79 cnf(3982,plain,
% 60.56/60.79 (~P10(a92,a2,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3949,1669,1675,1681,3953,426,415,424,429])).
% 60.56/60.79 cnf(3986,plain,
% 60.56/60.79 (P4(a227,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3949,1669,51,129,219,1675,1681,3953,426,415,424,429,423,418])).
% 60.56/60.79 cnf(4015,plain,
% 60.56/60.79 (~P10(a94,a2,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3982,1702,1708,1714,3986,426,415,424,429])).
% 60.56/60.79 cnf(4019,plain,
% 60.56/60.79 (P4(a230,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,3982,1702,51,131,221,1708,1714,3986,426,415,424,429,423,418])).
% 60.56/60.79 cnf(4049,plain,
% 60.56/60.79 (~P10(a96,a2,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,4015,1744,1750,1756,4019,426,415,424,429])).
% 60.56/60.79 cnf(4053,plain,
% 60.56/60.79 (P4(a232,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,4015,1744,51,133,223,1750,1756,4019,426,415,424,429,423,418])).
% 60.56/60.79 cnf(4082,plain,
% 60.56/60.79 (~P10(a98,a2,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,4049,1785,1791,1797,4053,426,415,424,429])).
% 60.56/60.79 cnf(4086,plain,
% 60.56/60.79 (P4(a234,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,4049,1785,51,135,225,1791,1797,4053,426,415,424,429,423,418])).
% 60.56/60.79 cnf(4117,plain,
% 60.56/60.79 (~P10(a101,a2,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,4082,1828,1834,1840,4086,426,415,424,429])).
% 60.56/60.79 cnf(4121,plain,
% 60.56/60.79 (P4(a236,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,4082,1828,51,137,227,1834,1840,4086,426,415,424,429,423,418])).
% 60.56/60.79 cnf(4149,plain,
% 60.56/60.79 (~P10(a103,a2,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,4117,1869,1875,1881,4121,426,415,424,429])).
% 60.56/60.79 cnf(4153,plain,
% 60.56/60.79 (P4(a238,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,4117,1869,51,139,229,1875,1881,4121,426,415,424,429,423,418])).
% 60.56/60.79 cnf(4183,plain,
% 60.56/60.79 (~P10(a105,a2,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,4149,1910,1916,1922,4153,426,415,424,429])).
% 60.56/60.79 cnf(4187,plain,
% 60.56/60.79 (P4(a241,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,4149,1910,51,141,231,1916,1922,4153,426,415,424,429,423,418])).
% 60.56/60.79 cnf(4216,plain,
% 60.56/60.79 (~P10(a107,a2,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,4183,1951,1957,1963,4187,426,415,424,429])).
% 60.56/60.79 cnf(4220,plain,
% 60.56/60.79 (P4(a243,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,4183,1951,51,143,233,1957,1963,4187,426,415,424,429,423,418])).
% 60.56/60.79 cnf(4248,plain,
% 60.56/60.79 (~P10(a109,a2,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,4216,1993,1999,2005,4220,426,415,424,429])).
% 60.56/60.79 cnf(4252,plain,
% 60.56/60.79 (P4(a245,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,4216,1993,51,145,235,1999,2005,4220,426,415,424,429,423,418])).
% 60.56/60.79 cnf(4283,plain,
% 60.56/60.79 (~P10(a112,a2,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,4248,2028,2034,2040,4252,426,415,424,429])).
% 60.56/60.79 cnf(4287,plain,
% 60.56/60.79 (P4(a247,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,4248,2028,51,147,237,2034,2040,4252,426,415,424,429,423,418])).
% 60.56/60.79 cnf(4316,plain,
% 60.56/60.79 (~P10(a114,a2,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,4283,2070,2076,2082,4287,426,415,424,429])).
% 60.56/60.79 cnf(4320,plain,
% 60.56/60.79 (P4(a249,a2)),
% 60.56/60.79 inference(scs_inference,[],[453,4283,2070,51,149,239,2076,2082,4287,426,415,424,429,423,418])).
% 120.57/60.79 cnf(4352,plain,
% 120.57/60.79 (~P10(a116,a2,a2)),
% 120.57/60.79 inference(scs_inference,[],[453,4316,2104,2110,2116,4320,426,415,424,429])).
% 120.57/60.79 cnf(4356,plain,
% 120.57/60.79 (P4(a252,a2)),
% 120.57/60.79 inference(scs_inference,[],[453,4316,2104,51,151,241,2110,2116,4320,426,415,424,429,423,418])).
% 120.57/60.79 cnf(4385,plain,
% 120.57/60.79 (~P10(a118,a2,a2)),
% 120.57/60.79 inference(scs_inference,[],[453,4352,2147,2153,2159,4356,426,415,424,429])).
% 120.57/60.79 cnf(4389,plain,
% 120.57/60.79 (P4(a254,a2)),
% 120.57/60.79 inference(scs_inference,[],[453,4352,2147,51,153,243,2153,2159,4356,426,415,424,429,423,418])).
% 120.57/60.79 cnf(4418,plain,
% 120.57/60.79 (~P10(a120,a2,a2)),
% 120.57/60.79 inference(scs_inference,[],[453,4385,2188,2192,2198,4389,426,415,424,429])).
% 120.57/60.79 cnf(4422,plain,
% 120.57/60.79 (P4(a256,a2)),
% 120.57/60.79 inference(scs_inference,[],[453,4385,2188,51,155,245,2192,2198,4389,426,415,424,429,423,418])).
% 120.57/60.79 cnf(4450,plain,
% 120.57/60.79 (~P4(x44501,x44501)),
% 120.57/60.79 inference(rename_variables,[],[442])).
% 120.57/60.79 cnf(4453,plain,
% 120.57/60.79 (~P10(a124,a2,a2)),
% 120.57/60.79 inference(scs_inference,[],[453,4418,2229,442,2233,2237,4422,415,426,23,424,429])).
% 120.57/60.79 cnf(4459,plain,
% 120.57/60.79 (P4(a258,a2)),
% 120.57/60.79 inference(scs_inference,[],[453,4418,2229,442,51,157,247,2233,2237,4422,342,311,415,426,23,424,429,437,423,418])).
% 120.57/60.79 cnf(4469,plain,
% 120.57/60.79 (P9(x44691,f121(f251(f4(a77),f4(a110))))+~E(a129,x44691)),
% 120.57/60.79 inference(scs_inference,[],[453,4418,2229,442,4450,51,157,247,2233,2237,3754,4422,404,342,311,415,426,23,424,429,437,423,418,431,10,24,13,11,15,25])).
% 120.57/60.79 cnf(4485,plain,
% 120.57/60.79 (~P10(a55,a122,a2)),
% 120.57/60.79 inference(scs_inference,[],[453,2927,4453,2883,442,2262,3086,4459,415,426,23,424,429])).
% 120.57/60.79 cnf(4491,plain,
% 120.57/60.79 (P4(a260,a2)),
% 120.57/60.79 inference(scs_inference,[],[453,2927,4453,2883,442,51,159,249,2262,3086,4459,342,329,415,426,23,424,429,437,423,418])).
% 120.57/60.79 cnf(4509,plain,
% 120.57/60.79 (~P4(a2,a172)),
% 120.57/60.79 inference(scs_inference,[],[3123,415])).
% 120.57/60.79 cnf(4516,plain,
% 120.57/60.79 (~P4(x45161,x45161)),
% 120.57/60.79 inference(rename_variables,[],[442])).
% 120.57/60.79 cnf(4517,plain,
% 120.57/60.79 (~P10(a77,a2,a2)),
% 120.57/60.79 inference(scs_inference,[],[453,4485,2915,442,2301,3123,2923,4491,415,426,424,23,429])).
% 120.57/60.79 cnf(4523,plain,
% 120.57/60.79 (P4(a146,a2)),
% 120.57/60.79 inference(scs_inference,[],[453,4485,2915,442,51,260,288,2301,3123,2923,4491,341,338,415,426,424,23,429,437,423,418])).
% 120.57/60.79 cnf(4535,plain,
% 120.57/60.79 (P9(x45351,f121(f251(f4(a110),f251(f4(a2),f4(a1)))))+~E(a17,x45351)),
% 120.57/60.79 inference(scs_inference,[],[453,4485,2915,442,4516,51,260,288,2301,3123,2923,3821,4491,407,341,338,415,426,424,23,429,437,423,418,431,10,24,13,11,414,15,25])).
% 120.57/60.79 cnf(4543,plain,
% 120.57/60.79 (P7(f4(a5))),
% 120.57/60.79 inference(scs_inference,[],[4523,34,413,411])).
% 120.57/60.79 cnf(4556,plain,
% 120.57/60.79 (~P10(a5,a44,a66)),
% 120.57/60.79 inference(scs_inference,[],[70,1807,4523,34,1619,408,50,413,411,416,417,427,422,2,415,430])).
% 120.57/60.79 cnf(4562,plain,
% 120.57/60.79 (~P3(a2,a218)),
% 120.57/60.79 inference(scs_inference,[],[70,592,1807,4523,34,1619,2339,604,2161,408,50,413,411,416,417,427,422,2,415,430,21,22,425,414])).
% 120.57/60.79 cnf(4568,plain,
% 120.57/60.79 (~P10(a126,a2,a2)),
% 120.57/60.79 inference(scs_inference,[],[70,592,1807,862,2264,2258,4523,34,1619,2339,604,2161,1330,2881,2953,408,461,50,413,411,416,417,427,422,2,415,430,21,22,425,414,27,428,28,429])).
% 120.57/60.79 cnf(4570,plain,
% 120.57/60.79 (P8(f4(a88),f4(a110))),
% 120.57/60.79 inference(scs_inference,[],[70,592,1807,862,2264,2258,4523,34,1619,2339,604,2161,1330,2881,2953,408,461,50,49,413,411,416,417,427,422,2,415,430,21,22,425,414,27,428,28,429,421])).
% 120.57/60.79 cnf(4573,plain,
% 120.57/60.79 (~P4(x45731,x45731)),
% 120.57/60.79 inference(rename_variables,[],[442])).
% 120.57/60.79 cnf(4578,plain,
% 120.57/60.79 (~P9(a145,f121(x45781))),
% 120.57/60.79 inference(scs_inference,[],[70,592,1807,862,2264,2258,4523,34,1619,259,2339,604,2161,1330,2881,398,287,389,2953,408,461,50,49,442,4573,413,411,416,417,427,422,2,415,430,21,22,425,414,27,428,28,429,421,23,437,423,418])).
% 120.57/60.79 cnf(4579,plain,
% 120.57/60.79 (~P4(x45791,x45791)),
% 120.57/60.79 inference(rename_variables,[],[442])).
% 120.57/60.79 cnf(4584,plain,
% 120.57/60.79 (~P4(x45841,x45841)),
% 120.57/60.79 inference(rename_variables,[],[442])).
% 120.57/60.79 cnf(4601,plain,
% 120.57/60.79 (P10(a99,a240,a122)),
% 120.57/60.79 inference(scs_inference,[],[70,592,1807,862,2264,2258,4517,4523,34,1619,259,2339,604,2161,1330,2881,354,398,287,2190,389,52,2953,57,59,60,408,61,68,69,330,309,461,50,49,453,442,4573,4579,4584,51,413,411,416,417,427,422,2,415,430,21,22,425,414,27,428,28,429,421,23,437,423,418,438,420,419,431,536,4535,424,433,432,434,435])).
% 120.57/60.79 cnf(4606,plain,
% 120.57/60.79 (~P9(a145,f121(x46061))),
% 120.57/60.79 inference(rename_variables,[],[4578])).
% 120.57/60.79 cnf(4608,plain,
% 120.57/60.79 (~P9(a145,f121(x46081))),
% 120.57/60.79 inference(rename_variables,[],[4578])).
% 120.57/60.79 cnf(4610,plain,
% 120.57/60.79 (~P9(a145,f121(x46101))),
% 120.57/60.79 inference(rename_variables,[],[4578])).
% 120.57/60.79 cnf(4612,plain,
% 120.57/60.79 (~P9(a145,f121(x46121))),
% 120.57/60.79 inference(rename_variables,[],[4578])).
% 120.57/60.79 cnf(4614,plain,
% 120.57/60.79 (~P9(a145,f121(x46141))),
% 120.57/60.79 inference(rename_variables,[],[4578])).
% 120.57/60.79 cnf(4616,plain,
% 120.57/60.79 (~P9(a145,f121(x46161))),
% 120.57/60.79 inference(rename_variables,[],[4578])).
% 120.57/60.79 cnf(4618,plain,
% 120.57/60.79 (~P9(a145,f121(x46181))),
% 120.57/60.79 inference(rename_variables,[],[4578])).
% 120.57/60.79 cnf(4620,plain,
% 120.57/60.79 (~P9(a145,f121(x46201))),
% 120.57/60.79 inference(rename_variables,[],[4578])).
% 120.57/60.79 cnf(4622,plain,
% 120.57/60.79 (~P9(a145,f121(x46221))),
% 120.57/60.79 inference(rename_variables,[],[4578])).
% 120.57/60.79 cnf(4631,plain,
% 120.57/60.79 (P7(f4(a44))),
% 120.57/60.79 inference(scs_inference,[],[2271,4543,4570,4578,4606,4608,4610,4612,4614,4616,4618,4620,35,475,570,683,2494,2667,2706,2806,2842,2965,4469,417,422,413,427,411])).
% 120.57/60.79 cnf(4645,plain,
% 120.57/60.79 (~P9(a145,f121(x46451))),
% 120.57/60.79 inference(rename_variables,[],[4578])).
% 120.57/60.79 cnf(4651,plain,
% 120.57/60.79 (P8(f4(a77),f4(a110))),
% 120.57/60.79 inference(scs_inference,[],[449,618,1973,3127,2271,4509,4601,4543,4570,4578,4606,4608,4610,4612,4614,4616,4618,4620,4622,4645,35,475,258,4491,520,443,287,48,570,683,2494,2667,2706,2806,2842,2965,4469,417,422,413,427,411,416,2,415,430,414,425,25,428,429,26,421])).
% 120.57/60.79 cnf(4655,plain,
% 120.57/60.79 (~P9(a240,f121(x46551))),
% 120.57/60.79 inference(scs_inference,[],[449,618,1973,3127,2271,4509,4568,4601,4543,4570,4578,4606,4608,4610,4612,4614,4616,4618,4620,4622,4645,35,475,3075,258,4491,154,520,61,443,287,48,570,683,2494,2667,2706,2806,2842,2965,4469,417,422,413,427,411,416,2,415,430,414,425,25,428,429,26,421,423,418])).
% 120.57/60.79 cnf(4668,plain,
% 120.57/60.79 (~P6(f4(a2),f4(a5),f4(a44),f4(a66))),
% 120.57/60.79 inference(scs_inference,[],[449,618,1973,3127,4556,2271,4509,4562,4568,4601,4543,4570,4578,4606,4608,4610,4612,4614,4616,4618,4620,4622,4645,35,475,3075,3043,258,1908,391,4491,388,63,67,53,54,58,154,520,56,60,61,443,287,309,48,442,570,683,2494,2667,2706,2806,2842,2965,4469,417,422,413,427,411,416,2,415,430,414,425,25,428,429,26,421,423,418,420,438,419,431,424,432])).
% 120.57/60.79 cnf(4673,plain,
% 120.57/60.79 (~P9(a240,f121(x46731))),
% 120.57/60.79 inference(rename_variables,[],[4655])).
% 120.57/60.79 cnf(4675,plain,
% 120.57/60.79 (~P9(a240,f121(x46751))),
% 120.57/60.79 inference(rename_variables,[],[4655])).
% 120.57/60.79 cnf(4679,plain,
% 120.57/60.79 (~P9(a240,f121(x46791))),
% 120.57/60.79 inference(rename_variables,[],[4655])).
% 120.57/60.79 cnf(4683,plain,
% 120.57/60.79 (~P9(a240,f121(x46831))),
% 120.57/60.79 inference(rename_variables,[],[4655])).
% 120.57/60.79 cnf(4689,plain,
% 120.57/60.79 (~P9(a240,f121(x46891))),
% 120.57/60.79 inference(rename_variables,[],[4655])).
% 120.57/60.79 cnf(4691,plain,
% 120.57/60.79 (~P9(a240,f121(x46911))),
% 120.57/60.79 inference(rename_variables,[],[4655])).
% 120.57/60.79 cnf(4693,plain,
% 120.57/60.79 (~P9(a240,f121(x46931))),
% 120.57/60.79 inference(rename_variables,[],[4655])).
% 120.57/60.79 cnf(4715,plain,
% 120.57/60.79 ($false),
% 120.57/60.79 inference(scs_inference,[],[70,629,1699,2303,1626,2297,2310,4631,4651,4655,4673,4675,4679,4683,4689,4691,4693,4668,36,2331,641,4459,331,358,453,2667,2806,427,570,413,2706,417,422,683,2965,2842,416,2494,411,415,2,430,414,425,428,424,429,437]),
% 120.57/60.79 ['proof']).
% 120.57/60.79 % SZS output end Proof
% 120.57/60.79 % Total time :59.860000s
%------------------------------------------------------------------------------