%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : NUM315+1 : TPTP v8.2.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n032.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.88s 60.94s
% Output : CNFRefutation 60.88s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.08 % Problem : NUM315+1 : TPTP v8.2.0. Released v3.1.0.
% 0.00/0.08 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.07/0.27 % Computer : n032.cluster.edu
% 0.07/0.27 % Model : x86_64 x86_64
% 0.07/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.27 % Memory : 8042.1875MB
% 0.07/0.27 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.27 % CPULimit : 300
% 0.07/0.27 % WCLimit : 300
% 0.07/0.27 % DateTime : Sat Jun 22 23:03:23 EDT 2024
% 0.07/0.27 % CPUTime :
% 0.12/0.47 start to proof:theBenchmark
% 60.88/60.93 %-------------------------------------------
% 60.88/60.93 % File :CSE---1.7
% 60.88/60.93 % Problem :theBenchmark
% 60.88/60.93 % Transform :cnf
% 60.88/60.93 % Format :tptp:raw
% 60.88/60.93 % Command :java -jar mcs_scs.jar %d %s
% 60.88/60.93
% 60.88/60.93 % Result :Theorem 60.360000s
% 60.88/60.93 % Output :CNFRefutation 60.360000s
% 60.88/60.93 %-------------------------------------------
% 60.88/60.94 %------------------------------------------------------------------------------
% 60.88/60.94 % File : NUM315+1 : TPTP v8.2.0. Released v3.1.0.
% 60.88/60.94 % Domain : Number Theory (RDN arithmetic)
% 60.88/60.94 % Problem : -2 + -5 = -7
% 60.88/60.94 % Version : Especial.
% 60.88/60.94 % English :
% 60.88/60.94
% 60.88/60.94 % Refs :
% 60.88/60.94 % Source : [TPTP]
% 60.88/60.94 % Names :
% 60.88/60.94
% 60.88/60.94 % Status : Theorem
% 60.88/60.94 % Rating : 0.42 v7.5.0, 0.44 v7.4.0, 0.43 v7.3.0, 0.34 v7.2.0, 0.31 v7.1.0, 0.26 v7.0.0, 0.37 v6.4.0, 0.35 v6.3.0, 0.42 v6.2.0, 0.44 v6.1.0, 0.57 v6.0.0, 0.52 v5.5.0, 0.56 v5.4.0, 0.64 v5.3.0, 0.70 v5.2.0, 0.55 v5.1.0, 0.48 v5.0.0, 0.54 v4.1.0, 0.57 v4.0.1, 0.61 v4.0.0, 0.58 v3.7.0, 0.60 v3.5.0, 0.68 v3.3.0, 0.64 v3.2.0, 0.82 v3.1.0
% 60.88/60.94 % Syntax : Number of formulae : 402 ( 375 unt; 0 def)
% 60.88/60.94 % Number of atoms : 473 ( 5 equ)
% 60.88/60.94 % Maximal formula atoms : 8 ( 1 avg)
% 60.88/60.94 % Number of connectives : 73 ( 2 ~; 1 |; 43 &)
% 60.88/60.94 % ( 3 <=>; 24 =>; 0 <=; 0 <~>)
% 60.88/60.94 % Maximal formula depth : 19 ( 1 avg)
% 60.88/60.94 % Maximal term depth : 5 ( 2 avg)
% 60.88/60.94 % Number of predicates : 11 ( 10 usr; 0 prp; 1-4 aty)
% 60.88/60.94 % Number of functors : 260 ( 260 usr; 256 con; 0-2 aty)
% 60.88/60.94 % Number of variables : 121 ( 121 !; 0 ?)
% 60.88/60.94 % SPC : FOF_THM_RFO_SEQ
% 60.88/60.94
% 60.88/60.94 % Comments :
% 60.88/60.94 %------------------------------------------------------------------------------
% 60.88/60.94 %----Include axioms for RDN arithmetic
% 60.88/60.94 include('Axioms/NUM005+0.ax').
% 60.88/60.94 include('Axioms/NUM005+1.ax').
% 60.88/60.94 include('Axioms/NUM005+2.ax').
% 60.88/60.94 %------------------------------------------------------------------------------
% 60.88/60.94 fof(sum_nn2_nn5_nn7,conjecture,
% 60.88/60.94 sum(nn2,nn5,nn7) ).
% 60.88/60.94
% 60.88/60.94 %------------------------------------------------------------------------------
% 60.88/60.94 %-------------------------------------------
% 60.88/60.94 % Proof found
% 60.88/60.94 % SZS status Theorem for theBenchmark
% 60.88/60.94 % SZS output start Proof
% 60.88/60.94 %ClaNum:439(EqnAxiom:32)
% 60.88/60.94 %VarNum:271(SingletonVarNum:132)
% 60.88/60.94 %MaxLitNum:8
% 60.88/60.94 %MaxfuncDepth:4
% 60.88/60.94 %SharedTerms:967
% 60.88/60.94 %goalClause: 407
% 60.88/60.94 %singleGoalClaCount:1
% 60.88/60.94 [407]~P10(a133,a195,a217)
% 60.88/60.94 [33]P1(f3(a1))
% 60.88/60.94 [34]P1(f3(a4))
% 60.88/60.94 [35]P1(f3(a43))
% 60.88/60.94 [36]P1(f3(a54))
% 60.88/60.94 [37]P1(f3(a65))
% 60.88/60.94 [38]P1(f3(a76))
% 60.88/60.94 [39]P1(f3(a87))
% 60.88/60.94 [40]P1(f3(a98))
% 60.88/60.94 [41]P1(f3(a109))
% 60.88/60.94 [42]P8(f3(a2),f3(a1))
% 60.88/60.94 [43]P8(f3(a1),f3(a4))
% 60.88/60.94 [44]P8(f3(a4),f3(a43))
% 60.88/60.94 [45]P8(f3(a43),f3(a54))
% 60.88/60.94 [46]P8(f3(a54),f3(a65))
% 60.88/60.94 [47]P8(f3(a65),f3(a76))
% 60.88/60.94 [48]P8(f3(a76),f3(a87))
% 60.88/60.94 [49]P8(f3(a87),f3(a98))
% 60.88/60.94 [50]P8(f3(a98),f3(a109))
% 60.88/60.94 [307]P2(f3(a2),f3(a2),f3(a2),f3(a2))
% 60.88/60.94 [308]P2(f3(a2),f3(a1),f3(a1),f3(a2))
% 60.88/60.94 [309]P2(f3(a2),f3(a4),f3(a4),f3(a2))
% 60.88/60.94 [310]P2(f3(a2),f3(a43),f3(a43),f3(a2))
% 60.88/60.94 [311]P2(f3(a2),f3(a54),f3(a54),f3(a2))
% 60.88/60.94 [312]P2(f3(a2),f3(a65),f3(a65),f3(a2))
% 60.88/60.94 [313]P2(f3(a2),f3(a76),f3(a76),f3(a2))
% 60.88/60.94 [314]P2(f3(a2),f3(a87),f3(a87),f3(a2))
% 60.88/60.94 [315]P2(f3(a2),f3(a98),f3(a98),f3(a2))
% 60.88/60.94 [316]P2(f3(a2),f3(a109),f3(a109),f3(a2))
% 60.88/60.94 [317]P2(f3(a1),f3(a2),f3(a1),f3(a2))
% 60.88/60.94 [318]P2(f3(a1),f3(a1),f3(a4),f3(a2))
% 60.88/60.94 [319]P2(f3(a1),f3(a4),f3(a43),f3(a2))
% 60.88/60.94 [320]P2(f3(a1),f3(a43),f3(a54),f3(a2))
% 60.88/60.94 [321]P2(f3(a1),f3(a54),f3(a65),f3(a2))
% 60.88/60.94 [322]P2(f3(a1),f3(a65),f3(a76),f3(a2))
% 60.88/60.94 [323]P2(f3(a1),f3(a76),f3(a87),f3(a2))
% 60.88/60.94 [324]P2(f3(a1),f3(a87),f3(a98),f3(a2))
% 60.88/60.94 [325]P2(f3(a1),f3(a98),f3(a109),f3(a2))
% 60.88/60.94 [326]P2(f3(a1),f3(a109),f3(a2),f3(a1))
% 60.88/60.94 [327]P2(f3(a4),f3(a2),f3(a4),f3(a2))
% 60.88/60.94 [328]P2(f3(a4),f3(a1),f3(a43),f3(a2))
% 60.88/60.94 [329]P2(f3(a4),f3(a4),f3(a54),f3(a2))
% 60.88/60.94 [330]P2(f3(a4),f3(a43),f3(a65),f3(a2))
% 60.88/60.94 [331]P2(f3(a4),f3(a54),f3(a76),f3(a2))
% 60.88/60.94 [332]P2(f3(a4),f3(a65),f3(a87),f3(a2))
% 60.88/60.94 [333]P2(f3(a4),f3(a76),f3(a98),f3(a2))
% 60.88/60.94 [334]P2(f3(a4),f3(a87),f3(a109),f3(a2))
% 60.88/60.94 [335]P2(f3(a4),f3(a98),f3(a2),f3(a1))
% 60.88/60.94 [336]P2(f3(a4),f3(a109),f3(a1),f3(a1))
% 60.88/60.94 [337]P2(f3(a43),f3(a2),f3(a43),f3(a2))
% 60.88/60.94 [338]P2(f3(a43),f3(a1),f3(a54),f3(a2))
% 60.88/60.94 [339]P2(f3(a43),f3(a4),f3(a65),f3(a2))
% 60.88/60.94 [340]P2(f3(a43),f3(a43),f3(a76),f3(a2))
% 60.88/60.94 [341]P2(f3(a43),f3(a54),f3(a87),f3(a2))
% 60.88/60.94 [342]P2(f3(a43),f3(a65),f3(a98),f3(a2))
% 60.88/60.94 [343]P2(f3(a43),f3(a76),f3(a109),f3(a2))
% 60.88/60.94 [344]P2(f3(a43),f3(a87),f3(a2),f3(a1))
% 60.88/60.94 [345]P2(f3(a43),f3(a98),f3(a1),f3(a1))
% 60.88/60.94 [346]P2(f3(a43),f3(a109),f3(a4),f3(a1))
% 60.88/60.94 [347]P2(f3(a54),f3(a2),f3(a54),f3(a2))
% 60.88/60.94 [348]P2(f3(a54),f3(a1),f3(a65),f3(a2))
% 60.88/60.94 [349]P2(f3(a54),f3(a4),f3(a76),f3(a2))
% 60.88/60.94 [350]P2(f3(a54),f3(a43),f3(a87),f3(a2))
% 60.88/60.94 [351]P2(f3(a54),f3(a54),f3(a98),f3(a2))
% 60.88/60.94 [352]P2(f3(a54),f3(a65),f3(a109),f3(a2))
% 60.88/60.94 [353]P2(f3(a54),f3(a76),f3(a2),f3(a1))
% 60.88/60.94 [354]P2(f3(a54),f3(a87),f3(a1),f3(a1))
% 60.88/60.94 [355]P2(f3(a54),f3(a98),f3(a4),f3(a1))
% 60.88/60.94 [356]P2(f3(a54),f3(a109),f3(a43),f3(a1))
% 60.88/60.94 [357]P2(f3(a65),f3(a2),f3(a65),f3(a2))
% 60.88/60.94 [358]P2(f3(a65),f3(a1),f3(a76),f3(a2))
% 60.88/60.94 [359]P2(f3(a65),f3(a4),f3(a87),f3(a2))
% 60.88/60.94 [360]P2(f3(a65),f3(a43),f3(a98),f3(a2))
% 60.88/60.94 [361]P2(f3(a65),f3(a54),f3(a109),f3(a2))
% 60.88/60.94 [362]P2(f3(a65),f3(a65),f3(a2),f3(a1))
% 60.88/60.94 [363]P2(f3(a65),f3(a76),f3(a1),f3(a1))
% 60.88/60.94 [364]P2(f3(a65),f3(a87),f3(a4),f3(a1))
% 60.88/60.94 [365]P2(f3(a65),f3(a98),f3(a43),f3(a1))
% 60.88/60.94 [366]P2(f3(a65),f3(a109),f3(a54),f3(a1))
% 60.88/60.94 [367]P2(f3(a76),f3(a2),f3(a76),f3(a2))
% 60.88/60.94 [368]P2(f3(a76),f3(a1),f3(a87),f3(a2))
% 60.88/60.94 [369]P2(f3(a76),f3(a4),f3(a98),f3(a2))
% 60.88/60.94 [370]P2(f3(a76),f3(a43),f3(a109),f3(a2))
% 60.88/60.94 [371]P2(f3(a76),f3(a54),f3(a2),f3(a1))
% 60.88/60.94 [372]P2(f3(a76),f3(a65),f3(a1),f3(a1))
% 60.88/60.94 [373]P2(f3(a76),f3(a76),f3(a4),f3(a1))
% 60.88/60.94 [374]P2(f3(a76),f3(a87),f3(a43),f3(a1))
% 60.88/60.94 [375]P2(f3(a76),f3(a98),f3(a54),f3(a1))
% 60.88/60.94 [376]P2(f3(a76),f3(a109),f3(a65),f3(a1))
% 60.88/60.94 [377]P2(f3(a87),f3(a2),f3(a87),f3(a2))
% 60.88/60.94 [378]P2(f3(a87),f3(a1),f3(a98),f3(a2))
% 60.88/60.94 [379]P2(f3(a87),f3(a4),f3(a109),f3(a2))
% 60.88/60.94 [380]P2(f3(a87),f3(a43),f3(a2),f3(a1))
% 60.88/60.94 [381]P2(f3(a87),f3(a54),f3(a1),f3(a1))
% 60.88/60.94 [382]P2(f3(a87),f3(a65),f3(a4),f3(a1))
% 60.88/60.94 [383]P2(f3(a87),f3(a76),f3(a43),f3(a1))
% 60.88/60.94 [384]P2(f3(a87),f3(a87),f3(a54),f3(a1))
% 60.88/60.94 [385]P2(f3(a87),f3(a98),f3(a65),f3(a1))
% 60.88/60.94 [386]P2(f3(a87),f3(a109),f3(a76),f3(a1))
% 60.88/60.94 [387]P2(f3(a98),f3(a2),f3(a98),f3(a2))
% 60.88/60.94 [388]P2(f3(a98),f3(a1),f3(a109),f3(a2))
% 60.88/60.94 [389]P2(f3(a98),f3(a4),f3(a2),f3(a1))
% 60.88/60.94 [390]P2(f3(a98),f3(a43),f3(a1),f3(a1))
% 60.88/60.94 [391]P2(f3(a98),f3(a54),f3(a4),f3(a1))
% 60.88/60.94 [392]P2(f3(a98),f3(a65),f3(a43),f3(a1))
% 60.88/60.94 [393]P2(f3(a98),f3(a76),f3(a54),f3(a1))
% 60.88/60.94 [394]P2(f3(a98),f3(a87),f3(a65),f3(a1))
% 60.88/60.94 [395]P2(f3(a98),f3(a98),f3(a76),f3(a1))
% 60.88/60.94 [396]P2(f3(a98),f3(a109),f3(a87),f3(a1))
% 60.88/60.94 [397]P2(f3(a109),f3(a2),f3(a109),f3(a2))
% 60.88/60.94 [398]P2(f3(a109),f3(a1),f3(a2),f3(a1))
% 60.88/60.94 [399]P2(f3(a109),f3(a4),f3(a1),f3(a1))
% 60.88/60.94 [400]P2(f3(a109),f3(a43),f3(a4),f3(a1))
% 60.88/60.94 [401]P2(f3(a109),f3(a54),f3(a43),f3(a1))
% 60.88/60.94 [402]P2(f3(a109),f3(a65),f3(a54),f3(a1))
% 60.88/60.94 [403]P2(f3(a109),f3(a76),f3(a65),f3(a1))
% 60.88/60.94 [404]P2(f3(a109),f3(a87),f3(a76),f3(a1))
% 60.88/60.94 [405]P2(f3(a109),f3(a98),f3(a87),f3(a1))
% 60.88/60.94 [406]P2(f3(a109),f3(a109),f3(a98),f3(a1))
% 60.88/60.94 [51]P9(a2,f120(f3(a2)))
% 60.88/60.94 [52]P9(a1,f120(f3(a1)))
% 60.88/60.94 [53]P9(a4,f120(f3(a4)))
% 60.88/60.94 [54]P9(a43,f120(f3(a43)))
% 60.88/60.94 [55]P9(a54,f120(f3(a54)))
% 60.88/60.94 [56]P9(a65,f120(f3(a65)))
% 60.88/60.94 [57]P9(a76,f120(f3(a76)))
% 60.88/60.94 [58]P9(a87,f120(f3(a87)))
% 60.88/60.94 [59]P9(a98,f120(f3(a98)))
% 60.88/60.94 [60]P9(a109,f120(f3(a109)))
% 60.88/60.94 [61]P9(a121,f132(f3(a1)))
% 60.88/60.94 [62]P9(a133,f132(f3(a4)))
% 60.88/60.94 [63]P9(a173,f132(f3(a43)))
% 60.88/60.94 [64]P9(a184,f132(f3(a54)))
% 60.88/60.94 [65]P9(a195,f132(f3(a65)))
% 60.88/60.94 [66]P9(a206,f132(f3(a76)))
% 60.88/60.95 [67]P9(a217,f132(f3(a87)))
% 60.88/60.95 [68]P9(a228,f132(f3(a98)))
% 60.88/60.95 [69]P9(a239,f132(f3(a109)))
% 60.88/60.95 [70]P9(a5,f120(f250(f3(a2),f3(a1))))
% 60.88/60.95 [71]P9(a6,f120(f250(f3(a1),f3(a1))))
% 60.88/60.95 [72]P9(a17,f120(f250(f3(a4),f3(a1))))
% 60.88/60.95 [73]P9(a28,f120(f250(f3(a43),f3(a1))))
% 60.88/60.95 [74]P9(a37,f120(f250(f3(a54),f3(a1))))
% 60.88/60.95 [75]P9(a38,f120(f250(f3(a65),f3(a1))))
% 60.88/60.95 [76]P9(a39,f120(f250(f3(a76),f3(a1))))
% 60.88/60.95 [77]P9(a40,f120(f250(f3(a87),f3(a1))))
% 60.88/60.95 [78]P9(a41,f120(f250(f3(a98),f3(a1))))
% 60.88/60.95 [79]P9(a42,f120(f250(f3(a109),f3(a1))))
% 60.88/60.95 [80]P9(a44,f120(f250(f3(a2),f3(a4))))
% 60.88/60.95 [81]P9(a45,f120(f250(f3(a1),f3(a4))))
% 60.88/60.95 [82]P9(a46,f120(f250(f3(a4),f3(a4))))
% 60.88/60.95 [83]P9(a47,f120(f250(f3(a43),f3(a4))))
% 60.88/60.95 [84]P9(a48,f120(f250(f3(a54),f3(a4))))
% 60.88/60.95 [85]P9(a49,f120(f250(f3(a65),f3(a4))))
% 60.88/60.95 [86]P9(a50,f120(f250(f3(a76),f3(a4))))
% 60.88/60.95 [87]P9(a51,f120(f250(f3(a87),f3(a4))))
% 60.88/60.95 [88]P9(a52,f120(f250(f3(a98),f3(a4))))
% 60.88/60.95 [89]P9(a53,f120(f250(f3(a109),f3(a4))))
% 60.88/60.95 [90]P9(a55,f120(f250(f3(a2),f3(a43))))
% 60.88/60.95 [91]P9(a56,f120(f250(f3(a1),f3(a43))))
% 60.88/60.95 [92]P9(a57,f120(f250(f3(a4),f3(a43))))
% 60.88/60.95 [93]P9(a58,f120(f250(f3(a43),f3(a43))))
% 60.88/60.95 [94]P9(a59,f120(f250(f3(a54),f3(a43))))
% 60.88/60.95 [95]P9(a60,f120(f250(f3(a65),f3(a43))))
% 60.88/60.95 [96]P9(a61,f120(f250(f3(a76),f3(a43))))
% 60.88/60.95 [97]P9(a62,f120(f250(f3(a87),f3(a43))))
% 60.88/60.95 [98]P9(a63,f120(f250(f3(a98),f3(a43))))
% 60.88/60.95 [99]P9(a64,f120(f250(f3(a109),f3(a43))))
% 60.88/60.95 [100]P9(a66,f120(f250(f3(a2),f3(a54))))
% 60.88/60.95 [101]P9(a67,f120(f250(f3(a1),f3(a54))))
% 60.88/60.95 [102]P9(a68,f120(f250(f3(a4),f3(a54))))
% 60.88/60.95 [103]P9(a69,f120(f250(f3(a43),f3(a54))))
% 60.88/60.95 [104]P9(a70,f120(f250(f3(a54),f3(a54))))
% 60.88/60.95 [105]P9(a71,f120(f250(f3(a65),f3(a54))))
% 60.88/60.95 [106]P9(a72,f120(f250(f3(a76),f3(a54))))
% 60.88/60.95 [107]P9(a73,f120(f250(f3(a87),f3(a54))))
% 60.88/60.95 [108]P9(a74,f120(f250(f3(a98),f3(a54))))
% 60.88/60.95 [109]P9(a75,f120(f250(f3(a109),f3(a54))))
% 60.88/60.95 [110]P9(a77,f120(f250(f3(a2),f3(a65))))
% 60.88/60.95 [111]P9(a78,f120(f250(f3(a1),f3(a65))))
% 60.88/60.95 [112]P9(a79,f120(f250(f3(a4),f3(a65))))
% 60.88/60.95 [113]P9(a80,f120(f250(f3(a43),f3(a65))))
% 60.88/60.95 [114]P9(a81,f120(f250(f3(a54),f3(a65))))
% 60.88/60.95 [115]P9(a82,f120(f250(f3(a65),f3(a65))))
% 60.88/60.95 [116]P9(a83,f120(f250(f3(a76),f3(a65))))
% 60.88/60.95 [117]P9(a84,f120(f250(f3(a87),f3(a65))))
% 60.88/60.95 [118]P9(a85,f120(f250(f3(a98),f3(a65))))
% 60.88/60.95 [119]P9(a86,f120(f250(f3(a109),f3(a65))))
% 60.88/60.95 [120]P9(a88,f120(f250(f3(a2),f3(a76))))
% 60.88/60.95 [121]P9(a89,f120(f250(f3(a1),f3(a76))))
% 60.88/60.95 [122]P9(a90,f120(f250(f3(a4),f3(a76))))
% 60.88/60.95 [123]P9(a91,f120(f250(f3(a43),f3(a76))))
% 60.88/60.95 [124]P9(a92,f120(f250(f3(a54),f3(a76))))
% 60.88/60.95 [125]P9(a93,f120(f250(f3(a65),f3(a76))))
% 60.88/60.95 [126]P9(a94,f120(f250(f3(a76),f3(a76))))
% 60.88/60.95 [127]P9(a95,f120(f250(f3(a87),f3(a76))))
% 60.88/60.95 [128]P9(a96,f120(f250(f3(a98),f3(a76))))
% 60.88/60.95 [129]P9(a97,f120(f250(f3(a109),f3(a76))))
% 60.88/60.95 [130]P9(a99,f120(f250(f3(a2),f3(a87))))
% 60.88/60.95 [131]P9(a100,f120(f250(f3(a1),f3(a87))))
% 60.88/60.95 [132]P9(a101,f120(f250(f3(a4),f3(a87))))
% 60.88/60.95 [133]P9(a102,f120(f250(f3(a43),f3(a87))))
% 60.88/60.95 [134]P9(a103,f120(f250(f3(a54),f3(a87))))
% 60.88/60.95 [135]P9(a104,f120(f250(f3(a65),f3(a87))))
% 60.88/60.95 [136]P9(a105,f120(f250(f3(a76),f3(a87))))
% 60.88/60.95 [137]P9(a106,f120(f250(f3(a87),f3(a87))))
% 60.88/60.95 [138]P9(a107,f120(f250(f3(a98),f3(a87))))
% 60.88/60.95 [139]P9(a108,f120(f250(f3(a109),f3(a87))))
% 60.88/60.95 [140]P9(a110,f120(f250(f3(a2),f3(a98))))
% 60.88/60.95 [141]P9(a111,f120(f250(f3(a1),f3(a98))))
% 60.88/60.95 [142]P9(a112,f120(f250(f3(a4),f3(a98))))
% 60.88/60.95 [143]P9(a113,f120(f250(f3(a43),f3(a98))))
% 60.88/60.95 [144]P9(a114,f120(f250(f3(a54),f3(a98))))
% 60.88/60.95 [145]P9(a115,f120(f250(f3(a65),f3(a98))))
% 60.88/60.95 [146]P9(a116,f120(f250(f3(a76),f3(a98))))
% 60.88/60.95 [147]P9(a117,f120(f250(f3(a87),f3(a98))))
% 60.88/60.95 [148]P9(a118,f120(f250(f3(a98),f3(a98))))
% 60.88/60.95 [149]P9(a119,f120(f250(f3(a109),f3(a98))))
% 60.88/60.95 [150]P9(a122,f120(f250(f3(a2),f3(a109))))
% 60.88/60.95 [151]P9(a123,f120(f250(f3(a1),f3(a109))))
% 60.88/60.95 [152]P9(a124,f120(f250(f3(a4),f3(a109))))
% 60.88/60.95 [153]P9(a125,f120(f250(f3(a43),f3(a109))))
% 60.88/60.95 [154]P9(a126,f120(f250(f3(a54),f3(a109))))
% 60.88/60.95 [155]P9(a127,f120(f250(f3(a65),f3(a109))))
% 60.88/60.95 [156]P9(a128,f120(f250(f3(a76),f3(a109))))
% 60.88/60.95 [157]P9(a129,f120(f250(f3(a87),f3(a109))))
% 60.88/60.95 [158]P9(a130,f120(f250(f3(a98),f3(a109))))
% 60.88/60.95 [159]P9(a131,f120(f250(f3(a109),f3(a109))))
% 60.88/60.95 [160]P9(a134,f132(f250(f3(a2),f3(a1))))
% 60.88/60.95 [161]P9(a135,f132(f250(f3(a1),f3(a1))))
% 60.88/60.95 [162]P9(a146,f132(f250(f3(a4),f3(a1))))
% 60.88/60.95 [163]P9(a157,f132(f250(f3(a43),f3(a1))))
% 60.88/60.95 [164]P9(a167,f132(f250(f3(a54),f3(a1))))
% 60.88/60.95 [165]P9(a168,f132(f250(f3(a65),f3(a1))))
% 60.88/60.95 [166]P9(a169,f132(f250(f3(a76),f3(a1))))
% 60.88/60.95 [167]P9(a170,f132(f250(f3(a87),f3(a1))))
% 60.88/60.95 [168]P9(a171,f132(f250(f3(a98),f3(a1))))
% 60.88/60.95 [169]P9(a172,f132(f250(f3(a109),f3(a1))))
% 60.88/60.95 [170]P9(a174,f132(f250(f3(a2),f3(a4))))
% 60.88/60.95 [171]P9(a175,f132(f250(f3(a1),f3(a4))))
% 60.88/60.95 [172]P9(a176,f132(f250(f3(a4),f3(a4))))
% 60.88/60.95 [173]P9(a177,f132(f250(f3(a43),f3(a4))))
% 60.88/60.95 [174]P9(a178,f132(f250(f3(a54),f3(a4))))
% 60.88/60.95 [175]P9(a179,f132(f250(f3(a65),f3(a4))))
% 60.88/60.95 [176]P9(a180,f132(f250(f3(a76),f3(a4))))
% 60.88/60.95 [177]P9(a181,f132(f250(f3(a87),f3(a4))))
% 60.88/60.95 [178]P9(a182,f132(f250(f3(a98),f3(a4))))
% 60.88/60.95 [179]P9(a183,f132(f250(f3(a109),f3(a4))))
% 60.88/60.95 [180]P9(a185,f132(f250(f3(a2),f3(a43))))
% 60.88/60.95 [181]P9(a186,f132(f250(f3(a1),f3(a43))))
% 60.88/60.95 [182]P9(a187,f132(f250(f3(a4),f3(a43))))
% 60.88/60.95 [183]P9(a188,f132(f250(f3(a43),f3(a43))))
% 60.88/60.95 [184]P9(a189,f132(f250(f3(a54),f3(a43))))
% 60.88/60.95 [185]P9(a190,f132(f250(f3(a65),f3(a43))))
% 60.88/60.95 [186]P9(a191,f132(f250(f3(a76),f3(a43))))
% 60.88/60.95 [187]P9(a192,f132(f250(f3(a87),f3(a43))))
% 60.88/60.95 [188]P9(a193,f132(f250(f3(a98),f3(a43))))
% 60.88/60.95 [189]P9(a194,f132(f250(f3(a109),f3(a43))))
% 60.88/60.95 [190]P9(a196,f132(f250(f3(a2),f3(a54))))
% 60.88/60.95 [191]P9(a197,f132(f250(f3(a1),f3(a54))))
% 60.88/60.95 [192]P9(a198,f132(f250(f3(a4),f3(a54))))
% 60.88/60.95 [193]P9(a199,f132(f250(f3(a43),f3(a54))))
% 60.88/60.95 [194]P9(a200,f132(f250(f3(a54),f3(a54))))
% 60.88/60.95 [195]P9(a201,f132(f250(f3(a65),f3(a54))))
% 60.88/60.95 [196]P9(a202,f132(f250(f3(a76),f3(a54))))
% 60.88/60.95 [197]P9(a203,f132(f250(f3(a87),f3(a54))))
% 60.88/60.95 [198]P9(a204,f132(f250(f3(a98),f3(a54))))
% 60.88/60.95 [199]P9(a205,f132(f250(f3(a109),f3(a54))))
% 60.88/60.95 [200]P9(a207,f132(f250(f3(a2),f3(a65))))
% 60.88/60.95 [201]P9(a208,f132(f250(f3(a1),f3(a65))))
% 60.88/60.95 [202]P9(a209,f132(f250(f3(a4),f3(a65))))
% 60.88/60.95 [203]P9(a210,f132(f250(f3(a43),f3(a65))))
% 60.88/60.95 [204]P9(a211,f132(f250(f3(a54),f3(a65))))
% 60.88/60.95 [205]P9(a212,f132(f250(f3(a65),f3(a65))))
% 60.88/60.95 [206]P9(a213,f132(f250(f3(a76),f3(a65))))
% 60.88/60.95 [207]P9(a214,f132(f250(f3(a87),f3(a65))))
% 60.88/60.95 [208]P9(a215,f132(f250(f3(a98),f3(a65))))
% 60.88/60.95 [209]P9(a216,f132(f250(f3(a109),f3(a65))))
% 60.88/60.95 [210]P9(a218,f132(f250(f3(a2),f3(a76))))
% 60.88/60.95 [211]P9(a219,f132(f250(f3(a1),f3(a76))))
% 60.88/60.95 [212]P9(a220,f132(f250(f3(a4),f3(a76))))
% 60.88/60.95 [213]P9(a221,f132(f250(f3(a43),f3(a76))))
% 60.88/60.95 [214]P9(a222,f132(f250(f3(a54),f3(a76))))
% 60.88/60.95 [215]P9(a223,f132(f250(f3(a65),f3(a76))))
% 60.88/60.95 [216]P9(a224,f132(f250(f3(a76),f3(a76))))
% 60.88/60.95 [217]P9(a225,f132(f250(f3(a87),f3(a76))))
% 60.88/60.95 [218]P9(a226,f132(f250(f3(a98),f3(a76))))
% 60.88/60.95 [219]P9(a227,f132(f250(f3(a109),f3(a76))))
% 60.88/60.95 [220]P9(a229,f132(f250(f3(a2),f3(a87))))
% 60.88/60.95 [221]P9(a230,f132(f250(f3(a1),f3(a87))))
% 60.88/60.95 [222]P9(a231,f132(f250(f3(a4),f3(a87))))
% 60.88/60.95 [223]P9(a232,f132(f250(f3(a43),f3(a87))))
% 60.88/60.95 [224]P9(a233,f132(f250(f3(a54),f3(a87))))
% 60.88/60.95 [225]P9(a234,f132(f250(f3(a65),f3(a87))))
% 60.88/60.95 [226]P9(a235,f132(f250(f3(a76),f3(a87))))
% 60.88/60.95 [227]P9(a236,f132(f250(f3(a87),f3(a87))))
% 60.88/60.95 [228]P9(a237,f132(f250(f3(a98),f3(a87))))
% 60.88/60.95 [229]P9(a238,f132(f250(f3(a109),f3(a87))))
% 60.88/60.95 [230]P9(a240,f132(f250(f3(a2),f3(a98))))
% 60.88/60.95 [231]P9(a241,f132(f250(f3(a1),f3(a98))))
% 60.88/60.95 [232]P9(a242,f132(f250(f3(a4),f3(a98))))
% 60.88/60.95 [233]P9(a243,f132(f250(f3(a43),f3(a98))))
% 60.88/60.95 [234]P9(a244,f132(f250(f3(a54),f3(a98))))
% 60.88/60.95 [235]P9(a245,f132(f250(f3(a65),f3(a98))))
% 60.88/60.95 [236]P9(a246,f132(f250(f3(a76),f3(a98))))
% 60.88/60.95 [237]P9(a247,f132(f250(f3(a87),f3(a98))))
% 60.88/60.95 [238]P9(a248,f132(f250(f3(a98),f3(a98))))
% 60.88/60.95 [239]P9(a249,f132(f250(f3(a109),f3(a98))))
% 60.88/60.95 [240]P9(a251,f132(f250(f3(a2),f3(a109))))
% 60.88/60.95 [241]P9(a252,f132(f250(f3(a1),f3(a109))))
% 60.88/60.95 [242]P9(a253,f132(f250(f3(a4),f3(a109))))
% 60.88/60.95 [243]P9(a254,f132(f250(f3(a43),f3(a109))))
% 60.88/60.95 [244]P9(a255,f132(f250(f3(a54),f3(a109))))
% 60.88/60.95 [245]P9(a256,f132(f250(f3(a65),f3(a109))))
% 60.88/60.95 [246]P9(a257,f132(f250(f3(a76),f3(a109))))
% 60.88/60.95 [247]P9(a258,f132(f250(f3(a87),f3(a109))))
% 60.88/60.95 [248]P9(a259,f132(f250(f3(a98),f3(a109))))
% 60.88/60.95 [249]P9(a260,f132(f250(f3(a109),f3(a109))))
% 60.88/60.95 [250]P9(a7,f120(f250(f3(a2),f250(f3(a2),f3(a1)))))
% 60.88/60.95 [251]P9(a8,f120(f250(f3(a1),f250(f3(a2),f3(a1)))))
% 60.88/60.95 [252]P9(a9,f120(f250(f3(a4),f250(f3(a2),f3(a1)))))
% 60.88/60.95 [253]P9(a10,f120(f250(f3(a43),f250(f3(a2),f3(a1)))))
% 60.88/60.95 [254]P9(a11,f120(f250(f3(a54),f250(f3(a2),f3(a1)))))
% 60.88/60.95 [255]P9(a12,f120(f250(f3(a65),f250(f3(a2),f3(a1)))))
% 60.88/60.95 [256]P9(a13,f120(f250(f3(a76),f250(f3(a2),f3(a1)))))
% 60.88/60.95 [257]P9(a14,f120(f250(f3(a87),f250(f3(a2),f3(a1)))))
% 60.88/60.95 [258]P9(a15,f120(f250(f3(a98),f250(f3(a2),f3(a1)))))
% 60.88/60.95 [259]P9(a16,f120(f250(f3(a109),f250(f3(a2),f3(a1)))))
% 60.88/60.95 [260]P9(a18,f120(f250(f3(a2),f250(f3(a1),f3(a1)))))
% 60.88/60.95 [261]P9(a19,f120(f250(f3(a1),f250(f3(a1),f3(a1)))))
% 60.88/60.95 [262]P9(a20,f120(f250(f3(a4),f250(f3(a1),f3(a1)))))
% 60.88/60.95 [263]P9(a21,f120(f250(f3(a43),f250(f3(a1),f3(a1)))))
% 60.88/60.95 [264]P9(a22,f120(f250(f3(a54),f250(f3(a1),f3(a1)))))
% 60.88/60.95 [265]P9(a23,f120(f250(f3(a65),f250(f3(a1),f3(a1)))))
% 60.88/60.95 [266]P9(a24,f120(f250(f3(a76),f250(f3(a1),f3(a1)))))
% 60.88/60.95 [267]P9(a25,f120(f250(f3(a87),f250(f3(a1),f3(a1)))))
% 60.88/60.95 [268]P9(a26,f120(f250(f3(a98),f250(f3(a1),f3(a1)))))
% 60.88/60.95 [269]P9(a27,f120(f250(f3(a109),f250(f3(a1),f3(a1)))))
% 60.88/60.95 [270]P9(a29,f120(f250(f3(a2),f250(f3(a4),f3(a1)))))
% 60.88/60.95 [271]P9(a30,f120(f250(f3(a1),f250(f3(a4),f3(a1)))))
% 60.88/60.95 [272]P9(a31,f120(f250(f3(a4),f250(f3(a4),f3(a1)))))
% 60.88/60.95 [273]P9(a32,f120(f250(f3(a43),f250(f3(a4),f3(a1)))))
% 60.88/60.95 [274]P9(a33,f120(f250(f3(a54),f250(f3(a4),f3(a1)))))
% 60.88/60.95 [275]P9(a34,f120(f250(f3(a65),f250(f3(a4),f3(a1)))))
% 60.88/60.95 [276]P9(a35,f120(f250(f3(a76),f250(f3(a4),f3(a1)))))
% 60.88/60.95 [277]P9(a36,f120(f250(f3(a87),f250(f3(a4),f3(a1)))))
% 60.88/60.95 [278]P9(a136,f132(f250(f3(a2),f250(f3(a2),f3(a1)))))
% 60.88/60.95 [279]P9(a137,f132(f250(f3(a1),f250(f3(a2),f3(a1)))))
% 60.88/60.95 [280]P9(a138,f132(f250(f3(a4),f250(f3(a2),f3(a1)))))
% 60.88/60.95 [281]P9(a139,f132(f250(f3(a43),f250(f3(a2),f3(a1)))))
% 60.88/60.95 [282]P9(a140,f132(f250(f3(a54),f250(f3(a2),f3(a1)))))
% 60.88/60.95 [283]P9(a141,f132(f250(f3(a65),f250(f3(a2),f3(a1)))))
% 60.88/60.95 [284]P9(a142,f132(f250(f3(a76),f250(f3(a2),f3(a1)))))
% 60.88/60.95 [285]P9(a143,f132(f250(f3(a87),f250(f3(a2),f3(a1)))))
% 60.88/60.95 [286]P9(a144,f132(f250(f3(a98),f250(f3(a2),f3(a1)))))
% 60.88/60.95 [287]P9(a145,f132(f250(f3(a109),f250(f3(a2),f3(a1)))))
% 60.88/60.95 [288]P9(a147,f132(f250(f3(a2),f250(f3(a1),f3(a1)))))
% 60.88/60.95 [289]P9(a148,f132(f250(f3(a1),f250(f3(a1),f3(a1)))))
% 60.88/60.95 [290]P9(a149,f132(f250(f3(a4),f250(f3(a1),f3(a1)))))
% 60.88/60.95 [291]P9(a150,f132(f250(f3(a43),f250(f3(a1),f3(a1)))))
% 60.88/60.95 [292]P9(a151,f132(f250(f3(a54),f250(f3(a1),f3(a1)))))
% 60.88/60.95 [293]P9(a152,f132(f250(f3(a65),f250(f3(a1),f3(a1)))))
% 60.88/60.95 [294]P9(a153,f132(f250(f3(a76),f250(f3(a1),f3(a1)))))
% 60.88/60.95 [295]P9(a154,f132(f250(f3(a87),f250(f3(a1),f3(a1)))))
% 60.88/60.95 [296]P9(a155,f132(f250(f3(a98),f250(f3(a1),f3(a1)))))
% 60.88/60.95 [297]P9(a156,f132(f250(f3(a109),f250(f3(a1),f3(a1)))))
% 60.88/60.95 [298]P9(a158,f132(f250(f3(a2),f250(f3(a4),f3(a1)))))
% 60.88/60.95 [299]P9(a159,f132(f250(f3(a1),f250(f3(a4),f3(a1)))))
% 60.88/60.95 [300]P9(a160,f132(f250(f3(a4),f250(f3(a4),f3(a1)))))
% 60.88/60.95 [301]P9(a161,f132(f250(f3(a43),f250(f3(a4),f3(a1)))))
% 60.88/60.95 [302]P9(a162,f132(f250(f3(a54),f250(f3(a4),f3(a1)))))
% 60.88/60.95 [303]P9(a163,f132(f250(f3(a65),f250(f3(a4),f3(a1)))))
% 60.88/60.95 [304]P9(a164,f132(f250(f3(a76),f250(f3(a4),f3(a1)))))
% 60.88/60.95 [305]P9(a165,f132(f250(f3(a87),f250(f3(a4),f3(a1)))))
% 60.88/60.95 [306]P9(a166,f132(f250(f3(a98),f250(f3(a4),f3(a1)))))
% 60.88/60.95 [410]P7(f3(x4101))+~P1(f3(x4101))
% 60.88/60.95 [408]~E(x4081,x4082)+P3(x4081,x4082)
% 60.88/60.95 [409]~P4(x4092,x4091)+~E(x4091,x4092)
% 60.88/60.95 [412]~P4(x4121,x4122)+P3(x4121,x4122)
% 60.88/60.95 [414]~P4(x4142,x4141)+~P4(x4141,x4142)
% 60.88/60.95 [415]~P7(x4152)+P7(f250(f3(x4151),x4152))
% 60.88/60.95 [425]~P5(x4253,x4251,x4252)+P10(x4251,x4252,x4253)
% 60.88/60.95 [426]~P10(x4262,x4263,x4261)+P5(x4261,x4262,x4263)
% 60.88/60.95 [416]~P7(x4163)+P8(f3(x4161),f250(f3(x4162),x4163))
% 60.88/60.95 [421]~P8(x4212,x4214)+P8(f250(f3(x4211),x4212),f250(f3(x4213),x4214))
% 60.88/60.95 [435]P6(f3(x4351),f250(f3(x4352),x4353),f3(x4354),f250(f3(x4355),x4356))+~P6(f3(x4351),f3(x4354),f250(f3(x4352),x4353),f250(f3(x4355),x4356))
% 60.88/60.95 [411]P4(x4112,x4111)+P4(x4111,x4112)+E(x4111,x4112)
% 60.88/60.95 [413]P4(x4131,x4132)+~P3(x4131,x4132)+E(x4131,x4132)
% 60.88/60.95 [423]P3(x4231,x4232)+~P4(x4231,x4233)+~P10(x4232,a1,x4233)
% 60.88/60.95 [420]P8(f3(x4201),f3(x4202))+~P8(f3(x4203),f3(x4202))+~P8(f3(x4201),f3(x4203))
% 60.88/60.95 [422]P10(x4221,x4222,a2)+~P9(x4221,f120(x4223))+~P9(x4222,f132(x4223))
% 60.88/60.95 [424]~P7(x4242)+~P8(f3(x4241),f3(x4243))+P8(f250(f3(x4241),x4242),f250(f3(x4243),x4242))
% 60.88/60.95 [427]~P10(x4273,x4274,x4271)+E(x4271,x4272)+~P10(x4273,x4274,x4272)
% 60.88/60.95 [428]~P10(x4283,x4281,x4284)+E(x4281,x4282)+~P10(x4283,x4282,x4284)
% 60.88/60.95 [429]~P10(x4291,x4293,x4294)+E(x4291,x4292)+~P10(x4292,x4293,x4294)
% 60.88/60.95 [417]P4(x4171,x4172)+~P9(x4172,f120(x4173))+~P9(x4171,f132(x4174))
% 60.88/60.95 [436]P6(f3(x4361),f3(x4362),f3(x4363),f3(x4364))+~P2(f3(x4365),f3(x4361),f3(x4364),f3(a2))+~P2(f3(x4362),f3(x4363),f3(x4365),f3(a2))
% 60.88/60.95 [418]P4(x4181,x4182)+~P8(x4183,x4184)+~P9(x4182,f132(x4183))+~P9(x4181,f132(x4184))
% 60.88/60.95 [419]P4(x4191,x4192)+~P8(x4193,x4194)+~P9(x4192,f120(x4194))+~P9(x4191,f120(x4193))
% 60.88/60.95 [430]~P10(x4302,x4301,x4303)+P10(x4301,x4302,x4303)+~P9(x4302,f120(x4304))+~P9(x4301,f132(x4305))
% 60.88/60.95 [437]~P2(f3(x4375),f3(x4371),f3(x4374),f3(x4376))+~P2(f3(x4372),f3(x4373),f3(x4375),f3(x4377))+~P2(f3(x4377),f3(x4376),f3(a1),f3(a2))+P6(f3(x4371),f3(x4372),f3(x4373),f250(f3(x4374),f3(a1)))
% 60.88/60.95 [431]P10(x4311,x4312,x4313)+~P6(f3(a2),x4316,x4315,x4314)+~P9(x4313,f120(x4314))+~P9(x4312,f120(x4315))+~P9(x4311,f120(x4316))
% 60.88/60.95 [432]P10(x4321,x4322,x4323)+~P6(f3(a2),x4326,x4325,x4324)+~P9(x4323,f132(x4324))+~P9(x4322,f132(x4325))+~P9(x4321,f132(x4326))
% 60.88/60.95 [433]P10(x4331,x4332,x4333)+~P8(x4334,x4335)+~P6(f3(a2),x4334,x4336,x4335)+~P9(x4332,f132(x4334))+~P9(x4331,f120(x4335))+~P9(x4333,f120(x4336))
% 60.88/60.95 [434]P10(x4341,x4342,x4343)+~P8(x4344,x4345)+~P6(f3(a2),x4344,x4346,x4345)+~P9(x4342,f132(x4345))+~P9(x4341,f120(x4344))+~P9(x4343,f132(x4346))
% 60.88/60.95 [438]~P7(x4386)+~P7(x4384)+~P2(f3(x4388),f3(x4381),f3(x4385),f3(x4389))+~P2(f3(x4382),f3(x4383),f3(x4388),f3(x43810))+~P6(f3(x4387),f3(a2),x4384,x4386)+~P2(f3(x43810),f3(x4389),f3(x4387),f3(a2))+P6(f3(x4381),f3(x4382),f250(f3(x4383),x4384),f250(f3(x4385),x4386))
% 60.88/60.95 [439]~P7(x4397)+~P7(x4395)+~P7(x4393)+~P6(f3(x4398),x4393,x4395,x4397)+~P2(f3(x4399),f3(x4391),f3(x4396),f3(x43910))+~P2(f3(x4392),f3(x4394),f3(x4399),f3(x43911))+~P2(f3(x43911),f3(x43910),f3(x4398),f3(a2))+P6(f3(x4391),f250(f3(x4392),x4393),f250(f3(x4394),x4395),f250(f3(x4396),x4397))
% 60.88/60.95 %EqnAxiom
% 60.88/60.95 [1]E(x11,x11)
% 60.88/60.95 [2]E(x22,x21)+~E(x21,x22)
% 60.88/60.95 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 60.88/60.95 [4]~E(x41,x42)+E(f3(x41),f3(x42))
% 60.88/60.95 [5]~E(x51,x52)+E(f250(x51,x53),f250(x52,x53))
% 60.88/60.95 [6]~E(x61,x62)+E(f250(x63,x61),f250(x63,x62))
% 60.88/60.95 [7]~E(x71,x72)+E(f132(x71),f132(x72))
% 60.88/60.95 [8]~E(x81,x82)+E(f120(x81),f120(x82))
% 60.88/60.95 [9]~P1(x91)+P1(x92)+~E(x91,x92)
% 60.88/60.95 [10]P2(x102,x103,x104,x105)+~E(x101,x102)+~P2(x101,x103,x104,x105)
% 60.88/60.95 [11]P2(x113,x112,x114,x115)+~E(x111,x112)+~P2(x113,x111,x114,x115)
% 60.88/60.95 [12]P2(x123,x124,x122,x125)+~E(x121,x122)+~P2(x123,x124,x121,x125)
% 60.88/60.95 [13]P2(x133,x134,x135,x132)+~E(x131,x132)+~P2(x133,x134,x135,x131)
% 60.88/60.95 [14]P6(x142,x143,x144,x145)+~E(x141,x142)+~P6(x141,x143,x144,x145)
% 60.88/60.95 [15]P6(x153,x152,x154,x155)+~E(x151,x152)+~P6(x153,x151,x154,x155)
% 60.88/60.95 [16]P6(x163,x164,x162,x165)+~E(x161,x162)+~P6(x163,x164,x161,x165)
% 60.88/60.95 [17]P6(x173,x174,x175,x172)+~E(x171,x172)+~P6(x173,x174,x175,x171)
% 60.88/60.95 [18]~P7(x181)+P7(x182)+~E(x181,x182)
% 60.88/60.95 [19]P10(x192,x193,x194)+~E(x191,x192)+~P10(x191,x193,x194)
% 60.88/60.95 [20]P10(x203,x202,x204)+~E(x201,x202)+~P10(x203,x201,x204)
% 60.88/60.95 [21]P10(x213,x214,x212)+~E(x211,x212)+~P10(x213,x214,x211)
% 60.88/60.95 [22]P4(x222,x223)+~E(x221,x222)+~P4(x221,x223)
% 60.88/60.95 [23]P4(x233,x232)+~E(x231,x232)+~P4(x233,x231)
% 60.88/60.95 [24]P8(x242,x243)+~E(x241,x242)+~P8(x241,x243)
% 60.88/60.95 [25]P8(x253,x252)+~E(x251,x252)+~P8(x253,x251)
% 60.88/60.95 [26]P3(x262,x263)+~E(x261,x262)+~P3(x261,x263)
% 60.88/60.95 [27]P3(x273,x272)+~E(x271,x272)+~P3(x273,x271)
% 60.88/60.95 [28]P9(x282,x283)+~E(x281,x282)+~P9(x281,x283)
% 60.88/60.95 [29]P9(x293,x292)+~E(x291,x292)+~P9(x293,x291)
% 60.88/60.95 [30]P5(x302,x303,x304)+~E(x301,x302)+~P5(x301,x303,x304)
% 60.88/60.95 [31]P5(x313,x312,x314)+~E(x311,x312)+~P5(x313,x311,x314)
% 60.88/60.95 [32]P5(x323,x324,x322)+~E(x321,x322)+~P5(x323,x324,x321)
% 60.88/60.95
% 60.88/60.95 %-------------------------------------------
% 60.88/60.95 cnf(441,plain,
% 60.88/60.95 (~P4(x4411,x4411)),
% 60.88/60.95 inference(equality_inference,[],[409])).
% 60.88/60.95 cnf(444,plain,
% 60.88/60.95 (P10(a1,a121,a2)),
% 60.88/60.95 inference(scs_inference,[],[407,52,61,425,422])).
% 60.88/60.95 cnf(450,plain,
% 60.88/60.95 (~E(a121,a2)),
% 60.88/60.95 inference(scs_inference,[],[407,51,52,61,441,307,425,422,436,417,22])).
% 60.88/60.95 cnf(451,plain,
% 60.88/60.95 (~P4(x4511,x4511)),
% 60.88/60.95 inference(rename_variables,[],[441])).
% 60.88/60.95 cnf(453,plain,
% 60.88/60.95 (~P4(x4531,x4531)),
% 60.88/60.95 inference(rename_variables,[],[441])).
% 60.88/60.95 cnf(454,plain,
% 60.88/60.95 (P10(a121,a1,a2)),
% 60.88/60.95 inference(scs_inference,[],[407,51,52,61,441,451,307,425,422,436,417,22,23,430])).
% 60.88/60.95 cnf(456,plain,
% 60.88/60.95 (~P8(f3(a1),f3(a1))),
% 60.88/60.95 inference(scs_inference,[],[407,51,52,61,441,451,453,307,425,422,436,417,22,23,430,418])).
% 60.88/60.95 cnf(457,plain,
% 60.88/60.95 (~P4(x4571,x4571)),
% 60.88/60.95 inference(rename_variables,[],[441])).
% 60.88/60.95 cnf(459,plain,
% 60.88/60.95 (~P8(f3(a2),f3(a2))),
% 60.88/60.95 inference(scs_inference,[],[407,51,52,61,441,451,453,457,307,425,422,436,417,22,23,430,418,419])).
% 60.88/60.95 cnf(462,plain,
% 60.88/60.95 (P10(a2,a2,a2)),
% 60.88/60.95 inference(scs_inference,[],[407,51,52,61,441,451,453,457,307,425,422,436,417,22,23,430,418,419,431])).
% 60.88/60.95 cnf(467,plain,
% 60.88/60.95 (~P8(f3(a1),f3(a2))),
% 60.88/60.95 inference(scs_inference,[],[407,42,51,52,61,441,451,453,457,307,425,422,436,417,22,23,430,418,419,431,414,19,420])).
% 60.88/60.95 cnf(486,plain,
% 60.88/60.95 (~P8(f3(a4),f3(a2))),
% 60.88/60.95 inference(scs_inference,[],[467,43,53,62,308,307,417,436,420])).
% 60.88/60.95 cnf(488,plain,
% 60.88/60.95 (~E(a4,a133)),
% 60.88/60.95 inference(scs_inference,[],[467,43,53,62,441,308,307,417,436,420,23])).
% 60.88/60.95 cnf(489,plain,
% 60.88/60.95 (~P4(x4891,x4891)),
% 60.88/60.95 inference(rename_variables,[],[441])).
% 60.88/60.95 cnf(491,plain,
% 60.88/60.95 (P10(a4,a133,a2)),
% 60.88/60.95 inference(scs_inference,[],[467,43,53,62,42,456,441,308,307,417,436,420,23,24,422])).
% 60.88/60.95 cnf(493,plain,
% 60.88/60.95 (~E(f3(a4),f3(a2))),
% 60.88/60.95 inference(scs_inference,[],[467,43,53,62,42,456,441,308,307,417,436,420,23,24,422,25])).
% 60.88/60.95 cnf(495,plain,
% 60.88/60.95 (~P4(x4951,x4951)),
% 60.88/60.95 inference(rename_variables,[],[441])).
% 60.88/60.95 cnf(496,plain,
% 60.88/60.95 (~P8(f3(a4),f3(a4))),
% 60.88/60.95 inference(scs_inference,[],[467,43,53,62,42,456,441,489,495,308,307,417,436,420,23,24,422,25,22,418])).
% 60.88/60.95 cnf(497,plain,
% 60.88/60.95 (~P4(x4971,x4971)),
% 60.88/60.95 inference(rename_variables,[],[441])).
% 60.88/60.95 cnf(499,plain,
% 60.88/60.95 (P10(a133,a4,a2)),
% 60.88/60.95 inference(scs_inference,[],[467,43,53,62,42,456,441,489,495,308,307,417,436,420,23,24,422,25,22,418,430])).
% 60.88/60.95 cnf(501,plain,
% 60.88/60.95 (~P8(f3(a43),f3(a43))),
% 60.88/60.95 inference(scs_inference,[],[467,43,53,54,62,42,456,441,489,495,497,308,307,417,436,420,23,24,422,25,22,418,430,419])).
% 60.88/60.95 cnf(504,plain,
% 60.88/60.95 (~P4(a4,a133)),
% 60.88/60.95 inference(scs_inference,[],[467,43,53,54,62,42,456,441,489,495,497,308,307,417,436,420,23,24,422,25,22,418,430,419,414])).
% 60.88/60.95 cnf(519,plain,
% 60.88/60.95 (~E(a4,a2)),
% 60.88/60.95 inference(scs_inference,[],[493,4])).
% 60.88/60.95 cnf(522,plain,
% 60.88/60.96 (~P8(f3(a43),f3(a2))),
% 60.88/60.96 inference(scs_inference,[],[486,493,44,63,54,4,422,420])).
% 60.88/60.96 cnf(524,plain,
% 60.88/60.96 (P4(a173,a2)),
% 60.88/60.96 inference(scs_inference,[],[51,486,493,44,63,54,4,422,420,417])).
% 60.88/60.96 cnf(528,plain,
% 60.88/60.96 (~E(a2,a173)),
% 60.88/60.96 inference(scs_inference,[],[51,486,493,44,63,54,441,309,307,4,422,420,417,436,23])).
% 60.88/60.96 cnf(529,plain,
% 60.88/60.96 (~P4(x5291,x5291)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(531,plain,
% 60.88/60.96 (~P4(x5311,x5311)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(532,plain,
% 60.88/60.96 (~E(f3(a4),f3(a43))),
% 60.88/60.96 inference(scs_inference,[],[51,486,493,44,63,54,501,441,529,309,307,4,422,420,417,436,23,22,24])).
% 60.88/60.96 cnf(533,plain,
% 60.88/60.96 (~E(f3(a43),f3(a2))),
% 60.88/60.96 inference(scs_inference,[],[51,486,493,44,63,54,501,441,529,309,307,4,422,420,417,436,23,22,24,25])).
% 60.88/60.96 cnf(536,plain,
% 60.88/60.96 (~P8(f3(a54),f3(a54))),
% 60.88/60.96 inference(scs_inference,[],[51,486,493,44,63,64,54,501,441,529,531,309,307,4,422,420,417,436,23,22,24,25,430,418])).
% 60.88/60.96 cnf(537,plain,
% 60.88/60.96 (~P4(x5371,x5371)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(539,plain,
% 60.88/60.96 (~P8(f3(a65),f3(a65))),
% 60.88/60.96 inference(scs_inference,[],[51,486,493,44,56,63,64,54,501,441,529,531,537,309,307,4,422,420,417,436,23,22,24,25,430,418,419])).
% 60.88/60.96 cnf(542,plain,
% 60.88/60.96 (~P4(a2,a173)),
% 60.88/60.96 inference(scs_inference,[],[51,486,493,44,56,63,64,54,501,441,529,531,537,309,307,4,422,420,417,436,23,22,24,25,430,418,419,414])).
% 60.88/60.96 cnf(556,plain,
% 60.88/60.96 (~E(a4,a43)),
% 60.88/60.96 inference(scs_inference,[],[532,4])).
% 60.88/60.96 cnf(557,plain,
% 60.88/60.96 (~P8(f3(a54),f3(a2))),
% 60.88/60.96 inference(scs_inference,[],[522,532,45,4,420])).
% 60.88/60.96 cnf(559,plain,
% 60.88/60.96 (P4(a195,a2)),
% 60.88/60.96 inference(scs_inference,[],[51,522,532,45,65,4,420,417])).
% 60.88/60.96 cnf(566,plain,
% 60.88/60.96 (~P4(x5661,x5661)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(567,plain,
% 60.88/60.96 (~E(f3(a43),f3(a54))),
% 60.88/60.96 inference(scs_inference,[],[51,522,532,45,65,56,536,441,310,307,4,420,417,422,436,23,24])).
% 60.88/60.96 cnf(569,plain,
% 60.88/60.96 (~P4(x5691,x5691)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(570,plain,
% 60.88/60.96 (~E(f3(a54),f3(a2))),
% 60.88/60.96 inference(scs_inference,[],[51,522,532,45,65,56,536,441,566,310,307,4,420,417,422,436,23,24,22,25])).
% 60.88/60.96 cnf(573,plain,
% 60.88/60.96 (~P8(f3(a76),f3(a76))),
% 60.88/60.96 inference(scs_inference,[],[51,522,532,45,65,66,56,536,441,566,569,310,307,4,420,417,422,436,23,24,22,25,430,418])).
% 60.88/60.96 cnf(574,plain,
% 60.88/60.96 (~P4(x5741,x5741)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(576,plain,
% 60.88/60.96 (~P8(f3(a87),f3(a87))),
% 60.88/60.96 inference(scs_inference,[],[51,522,532,45,58,65,66,56,536,441,566,569,574,310,307,4,420,417,422,436,23,24,22,25,430,418,419])).
% 60.88/60.96 cnf(594,plain,
% 60.88/60.96 (P4(a217,a2)),
% 60.88/60.96 inference(scs_inference,[],[51,533,67,4,417])).
% 60.88/60.96 cnf(598,plain,
% 60.88/60.96 (~P8(f3(a65),f3(a2))),
% 60.88/60.96 inference(scs_inference,[],[51,533,557,46,67,58,4,417,422,420])).
% 60.88/60.96 cnf(603,plain,
% 60.88/60.96 (~P4(x6031,x6031)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(605,plain,
% 60.88/60.96 (~P4(x6051,x6051)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(606,plain,
% 60.88/60.96 (~E(f3(a54),f3(a65))),
% 60.88/60.96 inference(scs_inference,[],[51,533,557,46,67,58,539,441,603,311,307,4,417,422,420,436,23,22,24])).
% 60.88/60.96 cnf(607,plain,
% 60.88/60.96 (~E(f3(a65),f3(a2))),
% 60.88/60.96 inference(scs_inference,[],[51,533,557,46,67,58,539,441,603,311,307,4,417,422,420,436,23,22,24,25])).
% 60.88/60.96 cnf(610,plain,
% 60.88/60.96 (~P8(f3(a98),f3(a98))),
% 60.88/60.96 inference(scs_inference,[],[51,533,557,46,67,68,58,539,441,603,605,311,307,4,417,422,420,436,23,22,24,25,430,418])).
% 60.88/60.96 cnf(611,plain,
% 60.88/60.96 (~P4(x6111,x6111)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(613,plain,
% 60.88/60.96 (~P8(f3(a109),f3(a109))),
% 60.88/60.96 inference(scs_inference,[],[51,533,557,46,60,67,68,58,539,441,603,605,611,311,307,4,417,422,420,436,23,22,24,25,430,418,419])).
% 60.88/60.96 cnf(616,plain,
% 60.88/60.96 (~P4(a2,a217)),
% 60.88/60.96 inference(scs_inference,[],[51,533,557,46,60,67,68,58,539,441,603,605,611,311,307,4,417,422,420,436,23,22,24,25,430,418,419,414])).
% 60.88/60.96 cnf(622,plain,
% 60.88/60.96 (~E(a43,a54)),
% 60.88/60.96 inference(scs_inference,[],[567,4])).
% 60.88/60.96 cnf(627,plain,
% 60.88/60.96 (~P8(f3(a76),f3(a2))),
% 60.88/60.96 inference(scs_inference,[],[454,567,598,47,69,60,524,4,423,422,420])).
% 60.88/60.96 cnf(629,plain,
% 60.88/60.96 (P4(a239,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,567,598,47,69,60,524,4,423,422,420,417])).
% 60.88/60.96 cnf(634,plain,
% 60.88/60.96 (~P4(x6341,x6341)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(635,plain,
% 60.88/60.96 (~E(f3(a65),f3(a76))),
% 60.88/60.96 inference(scs_inference,[],[454,51,567,598,47,69,60,524,573,441,312,307,4,423,422,420,417,436,23,24])).
% 60.88/60.96 cnf(638,plain,
% 60.88/60.96 (~E(f3(a76),f3(a2))),
% 60.88/60.96 inference(scs_inference,[],[454,51,567,598,47,69,60,524,573,441,634,312,307,4,423,422,420,417,436,23,24,22,25])).
% 60.88/60.96 cnf(664,plain,
% 60.88/60.96 (~P8(f3(a87),f3(a2))),
% 60.88/60.96 inference(scs_inference,[],[454,570,627,48,559,4,423,420])).
% 60.88/60.96 cnf(668,plain,
% 60.88/60.96 (P4(a134,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,570,627,48,160,70,559,4,423,420,422,417])).
% 60.88/60.96 cnf(673,plain,
% 60.88/60.96 (~P4(x6731,x6731)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(674,plain,
% 60.88/60.96 (~E(f3(a76),f3(a87))),
% 60.88/60.96 inference(scs_inference,[],[454,51,570,627,48,160,70,559,576,441,313,307,4,423,420,422,417,436,23,24])).
% 60.88/60.96 cnf(677,plain,
% 60.88/60.96 (~E(f3(a87),f3(a2))),
% 60.88/60.96 inference(scs_inference,[],[454,51,570,627,48,160,70,559,576,441,673,313,307,4,423,420,422,417,436,23,24,22,25])).
% 60.88/60.96 cnf(702,plain,
% 60.88/60.96 (~E(a54,a65)),
% 60.88/60.96 inference(scs_inference,[],[606,4])).
% 60.88/60.96 cnf(705,plain,
% 60.88/60.96 (P10(a17,a146,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,606,162,72,594,4,423,422])).
% 60.88/60.96 cnf(707,plain,
% 60.88/60.96 (~P8(f3(a98),f3(a2))),
% 60.88/60.96 inference(scs_inference,[],[454,606,664,49,162,72,594,4,423,422,420])).
% 60.88/60.96 cnf(711,plain,
% 60.88/60.96 (P4(a146,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,606,664,49,162,72,594,314,307,4,423,422,420,436,417])).
% 60.88/60.96 cnf(713,plain,
% 60.88/60.96 (~E(f3(a87),f3(a98))),
% 60.88/60.96 inference(scs_inference,[],[454,51,606,664,49,162,72,594,610,314,307,4,423,422,420,436,417,24])).
% 60.88/60.96 cnf(716,plain,
% 60.88/60.96 (~E(f3(a98),f3(a2))),
% 60.88/60.96 inference(scs_inference,[],[454,51,606,664,49,162,72,594,610,441,314,307,4,423,422,420,436,417,24,23,25])).
% 60.88/60.96 cnf(750,plain,
% 60.88/60.96 (P4(a167,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,607,707,50,164,74,629,4,420,422,423,417])).
% 60.88/60.96 cnf(755,plain,
% 60.88/60.96 (~P4(x7551,x7551)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(756,plain,
% 60.88/60.96 (~E(f3(a98),f3(a109))),
% 60.88/60.96 inference(scs_inference,[],[454,51,607,707,50,164,74,629,613,441,315,307,4,420,422,423,417,436,23,24])).
% 60.88/60.96 cnf(759,plain,
% 60.88/60.96 (~E(f3(a109),f3(a2))),
% 60.88/60.96 inference(scs_inference,[],[454,51,607,707,50,164,74,629,613,441,755,315,307,4,420,422,423,417,436,23,24,22,25])).
% 60.88/60.96 cnf(787,plain,
% 60.88/60.96 (~P8(f3(a4),f3(a1))),
% 60.88/60.96 inference(scs_inference,[],[454,635,166,76,43,668,496,4,422,423,420])).
% 60.88/60.96 cnf(789,plain,
% 60.88/60.96 (P4(a169,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,635,166,76,43,668,496,4,422,423,420,417])).
% 60.88/60.96 cnf(795,plain,
% 60.88/60.96 (~E(f3(a1),f3(a4))),
% 60.88/60.96 inference(scs_inference,[],[454,51,635,166,76,43,668,496,441,316,307,4,422,423,420,417,436,23,24])).
% 60.88/60.96 cnf(796,plain,
% 60.88/60.96 (~E(f3(a1),f3(a2))),
% 60.88/60.96 inference(scs_inference,[],[454,51,635,166,76,43,42,459,668,496,441,316,307,4,422,423,420,417,436,23,24,25])).
% 60.88/60.96 cnf(827,plain,
% 60.88/60.96 (~P8(f3(a54),f3(a43))),
% 60.88/60.96 inference(scs_inference,[],[454,638,168,78,45,711,536,4,423,422,420])).
% 60.88/60.96 cnf(831,plain,
% 60.88/60.96 (P4(a171,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,638,168,78,45,711,536,317,4,423,422,420,436,417])).
% 60.88/60.96 cnf(834,plain,
% 60.88/60.96 (~P4(x8341,x8341)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(835,plain,
% 60.88/60.96 (~E(f3(a2),f3(a4))),
% 60.88/60.96 inference(scs_inference,[],[454,51,638,787,168,78,45,42,711,536,441,317,4,423,422,420,436,417,23,24])).
% 60.88/60.96 cnf(838,plain,
% 60.88/60.96 (~E(f3(a43),f3(a1))),
% 60.88/60.96 inference(scs_inference,[],[454,51,638,787,168,78,44,45,42,711,536,441,834,317,4,423,422,420,436,417,23,24,22,25])).
% 60.88/60.96 cnf(858,plain,
% 60.88/60.96 (~P8(f3(a54),f3(a4))),
% 60.88/60.96 inference(scs_inference,[],[674,827,170,80,44,4,422,420])).
% 60.88/60.96 cnf(862,plain,
% 60.88/60.96 (P4(a174,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,674,827,170,80,44,750,4,422,420,423,417])).
% 60.88/60.96 cnf(868,plain,
% 60.88/60.96 (~E(f3(a4),f3(a54))),
% 60.88/60.96 inference(scs_inference,[],[454,51,674,827,170,80,44,750,441,318,317,4,422,420,423,417,436,23,24])).
% 60.88/60.96 cnf(869,plain,
% 60.88/60.96 (~E(f3(a65),f3(a43))),
% 60.88/60.96 inference(scs_inference,[],[454,51,674,827,170,80,46,44,750,441,318,317,4,422,420,423,417,436,23,24,25])).
% 60.88/60.96 cnf(894,plain,
% 60.88/60.96 (~P8(f3(a54),f3(a1))),
% 60.88/60.96 inference(scs_inference,[],[713,858,43,4,420])).
% 60.88/60.96 cnf(902,plain,
% 60.88/60.96 (P4(a176,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,713,858,172,82,43,789,319,317,4,420,423,422,436,417])).
% 60.88/60.96 cnf(905,plain,
% 60.88/60.96 (~P4(x9051,x9051)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(906,plain,
% 60.88/60.96 (~E(f3(a1),f3(a54))),
% 60.88/60.96 inference(scs_inference,[],[454,51,713,858,172,82,43,789,441,319,317,4,420,423,422,436,417,23,24])).
% 60.88/60.96 cnf(909,plain,
% 60.88/60.96 (~E(f3(a65),f3(a4))),
% 60.88/60.96 inference(scs_inference,[],[454,51,713,858,172,82,43,46,789,441,905,319,317,4,420,423,422,436,417,23,24,22,25])).
% 60.88/60.96 cnf(930,plain,
% 60.88/60.96 (~P8(f3(a76),f3(a65))),
% 60.88/60.96 inference(scs_inference,[],[454,756,174,84,47,831,573,4,423,422,420])).
% 60.88/60.96 cnf(932,plain,
% 60.88/60.96 (P4(a178,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,756,174,84,47,831,573,4,423,422,420,417])).
% 60.88/60.96 cnf(938,plain,
% 60.88/60.96 (~E(f3(a2),f3(a54))),
% 60.88/60.96 inference(scs_inference,[],[454,51,756,894,174,84,47,42,831,573,441,320,317,4,423,422,420,417,436,23,24])).
% 60.88/60.96 cnf(939,plain,
% 60.88/60.96 (~E(f3(a65),f3(a1))),
% 60.88/60.96 inference(scs_inference,[],[454,51,756,894,174,84,47,46,42,831,573,441,320,317,4,423,422,420,417,436,23,24,25])).
% 60.88/60.96 cnf(967,plain,
% 60.88/60.96 (~P8(f3(a76),f3(a54))),
% 60.88/60.96 inference(scs_inference,[],[677,930,176,86,46,4,422,420])).
% 60.88/60.96 cnf(973,plain,
% 60.88/60.96 (P4(a180,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,677,930,176,86,46,862,321,308,4,422,420,423,436,417])).
% 60.88/60.96 cnf(976,plain,
% 60.88/60.96 (~P4(x9761,x9761)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(977,plain,
% 60.88/60.96 (~E(f3(a54),f3(a76))),
% 60.88/60.96 inference(scs_inference,[],[454,51,677,930,176,86,46,862,441,321,308,4,422,420,423,436,417,23,24])).
% 60.88/60.96 cnf(980,plain,
% 60.88/60.96 (~E(f3(a87),f3(a65))),
% 60.88/60.96 inference(scs_inference,[],[454,51,677,930,176,86,48,46,862,441,976,321,308,4,422,420,423,436,417,23,24,22,25])).
% 60.88/60.96 cnf(1004,plain,
% 60.88/60.96 (~P8(f3(a76),f3(a43))),
% 60.88/60.96 inference(scs_inference,[],[716,967,45,4,420])).
% 60.88/60.96 cnf(1010,plain,
% 60.88/60.96 (P4(a182,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,716,967,178,88,45,902,4,420,423,422,417])).
% 60.88/60.96 cnf(1016,plain,
% 60.88/60.96 (~E(f3(a43),f3(a76))),
% 60.88/60.96 inference(scs_inference,[],[454,51,716,967,178,88,45,902,441,322,317,4,420,423,422,417,436,23,24])).
% 60.88/60.96 cnf(1017,plain,
% 60.88/60.96 (~E(f3(a87),f3(a54))),
% 60.88/60.96 inference(scs_inference,[],[454,51,716,967,178,88,45,48,902,441,322,317,4,420,423,422,417,436,23,24,25])).
% 60.88/60.96 cnf(1042,plain,
% 60.88/60.96 (P7(f250(f3(x10421),f3(a1)))),
% 60.88/60.96 inference(scs_inference,[],[33,410,415])).
% 60.88/60.96 cnf(1048,plain,
% 60.88/60.96 (~P8(f3(a76),f3(a4))),
% 60.88/60.96 inference(scs_inference,[],[454,759,1004,180,90,44,932,4,423,422,420])).
% 60.88/60.96 cnf(1052,plain,
% 60.88/60.96 (P4(a185,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,759,1004,180,90,44,932,323,308,4,423,422,420,436,417])).
% 60.88/60.96 cnf(1055,plain,
% 60.88/60.96 (~P4(x10551,x10551)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(1056,plain,
% 60.88/60.96 (~E(f3(a4),f3(a76))),
% 60.88/60.96 inference(scs_inference,[],[454,51,759,1004,180,90,44,932,441,323,308,4,423,422,420,436,417,23,24])).
% 60.88/60.96 cnf(1059,plain,
% 60.88/60.96 (~E(f3(a87),f3(a43))),
% 60.88/60.96 inference(scs_inference,[],[454,51,759,1004,180,90,48,44,932,441,1055,323,308,4,423,422,420,436,417,23,24,22,25])).
% 60.88/60.96 cnf(1082,plain,
% 60.88/60.96 (~E(a1,a4)),
% 60.88/60.96 inference(scs_inference,[],[795,4])).
% 60.88/60.96 cnf(1085,plain,
% 60.88/60.96 (~P8(f3(a76),f3(a1))),
% 60.88/60.96 inference(scs_inference,[],[795,1048,182,92,43,4,422,420])).
% 60.88/60.96 cnf(1089,plain,
% 60.88/60.96 (P4(a187,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,795,1048,182,92,43,973,4,422,420,423,417])).
% 60.88/60.96 cnf(1094,plain,
% 60.88/60.96 (~P4(x10941,x10941)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(1095,plain,
% 60.88/60.96 (~E(f3(a1),f3(a76))),
% 60.88/60.96 inference(scs_inference,[],[454,51,795,1048,182,92,43,973,441,324,317,4,422,420,423,417,436,23,24])).
% 60.88/60.96 cnf(1096,plain,
% 60.88/60.96 (~E(f3(a87),f3(a4))),
% 60.88/60.96 inference(scs_inference,[],[454,51,795,1048,182,92,43,48,973,441,324,317,4,422,420,423,417,436,23,24,25])).
% 60.88/60.96 cnf(1098,plain,
% 60.88/60.96 (~P4(x10981,x10981)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(1102,plain,
% 60.88/60.96 (~P4(x11021,x11021)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(1109,plain,
% 60.88/60.96 (P9(x11091,f120(f3(a98)))+~E(a98,x11091)),
% 60.88/60.96 inference(scs_inference,[],[454,51,795,1048,59,182,185,94,92,43,48,973,441,1094,1098,1102,324,317,4,422,420,423,417,436,23,24,25,22,430,419,418,414,28])).
% 60.88/60.96 cnf(1122,plain,
% 60.88/60.96 (~P8(f3(a43),f3(a4))),
% 60.88/60.96 inference(scs_inference,[],[906,44,501,4,420])).
% 60.88/60.96 cnf(1130,plain,
% 60.88/60.96 (P4(a189,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,906,184,94,44,1010,501,325,308,4,420,423,422,436,417])).
% 60.88/60.96 cnf(1133,plain,
% 60.88/60.96 (~P4(x11331,x11331)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(1134,plain,
% 60.88/60.96 (~E(f3(a2),f3(a76))),
% 60.88/60.96 inference(scs_inference,[],[454,51,906,1085,184,94,42,44,1010,501,441,325,308,4,420,423,422,436,417,23,24])).
% 60.88/60.96 cnf(1137,plain,
% 60.88/60.96 (~E(f3(a87),f3(a1))),
% 60.88/60.96 inference(scs_inference,[],[454,51,906,1085,184,94,42,48,44,1010,501,441,1133,325,308,4,420,423,422,436,417,23,24,22,25])).
% 60.88/60.96 cnf(1165,plain,
% 60.88/60.96 (~P8(f3(a43),f3(a1))),
% 60.88/60.96 inference(scs_inference,[],[454,796,1122,186,96,43,1052,4,423,422,420])).
% 60.88/60.96 cnf(1167,plain,
% 60.88/60.96 (P4(a191,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,796,1122,186,96,43,1052,4,423,422,420,417])).
% 60.88/60.96 cnf(1173,plain,
% 60.88/60.96 (~E(f3(a1),f3(a43))),
% 60.88/60.96 inference(scs_inference,[],[454,51,796,1122,186,96,43,1052,441,327,4,423,422,420,417,436,23,24])).
% 60.88/60.96 cnf(1174,plain,
% 60.88/60.96 (~E(f3(a54),f3(a4))),
% 60.88/60.96 inference(scs_inference,[],[454,51,796,1122,186,96,45,43,1052,441,327,4,423,422,420,417,436,23,24,25])).
% 60.88/60.96 cnf(1196,plain,
% 60.88/60.96 (P4(a193,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,1016,188,98,1089,4,423,422,417])).
% 60.88/60.96 cnf(1200,plain,
% 60.88/60.96 (~P8(f3(a98),f3(a87))),
% 60.88/60.96 inference(scs_inference,[],[454,51,1016,188,98,49,1089,610,328,327,4,423,422,417,436,420])).
% 60.88/60.96 cnf(1204,plain,
% 60.88/60.96 (~E(f3(a2),f3(a43))),
% 60.88/60.96 inference(scs_inference,[],[454,51,1016,1165,188,98,49,42,1089,610,441,328,327,4,423,422,417,436,420,23,24])).
% 60.88/60.96 cnf(1205,plain,
% 60.88/60.96 (~E(f3(a54),f3(a1))),
% 60.88/60.96 inference(scs_inference,[],[454,51,1016,1165,188,98,49,45,42,1089,610,441,328,327,4,423,422,417,436,420,23,24,25])).
% 60.88/60.96 cnf(1237,plain,
% 60.88/60.96 (P4(a196,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,868,190,100,1130,329,327,4,423,422,436,417])).
% 60.88/60.96 cnf(1239,plain,
% 60.88/60.96 (~P8(f3(a98),f3(a76))),
% 60.88/60.96 inference(scs_inference,[],[454,51,868,1200,190,100,48,1130,329,327,4,423,422,436,417,420])).
% 60.88/60.96 cnf(1243,plain,
% 60.88/60.96 (~E(f3(a76),f3(a98))),
% 60.88/60.96 inference(scs_inference,[],[454,51,868,1200,190,100,48,1130,441,329,327,4,423,422,436,417,420,23,24])).
% 60.88/60.96 cnf(1270,plain,
% 60.88/60.96 (P3(a191,a121)),
% 60.88/60.96 inference(scs_inference,[],[454,938,1167,4,423])).
% 60.88/60.96 cnf(1274,plain,
% 60.88/60.96 (P4(a198,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,938,192,102,1167,4,423,422,417])).
% 60.88/60.96 cnf(1278,plain,
% 60.88/60.96 (~P8(f3(a98),f3(a65))),
% 60.88/60.96 inference(scs_inference,[],[454,51,938,1239,192,102,47,1167,330,309,4,423,422,417,436,420])).
% 60.88/60.96 cnf(1282,plain,
% 60.88/60.96 (~E(f3(a65),f3(a98))),
% 60.88/60.96 inference(scs_inference,[],[454,51,938,1239,192,102,47,1167,441,330,309,4,423,422,417,436,420,23,24])).
% 60.88/60.96 cnf(1283,plain,
% 60.88/60.96 (~E(f3(a109),f3(a76))),
% 60.88/60.96 inference(scs_inference,[],[454,51,938,1239,192,102,47,50,1167,441,330,309,4,423,422,417,436,420,23,24,25])).
% 60.88/60.96 cnf(1312,plain,
% 60.88/60.96 (P4(a200,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,977,194,104,1196,331,318,4,422,423,436,417])).
% 60.88/60.96 cnf(1314,plain,
% 60.88/60.96 (~P8(f3(a98),f3(a54))),
% 60.88/60.96 inference(scs_inference,[],[454,51,977,1278,194,104,46,1196,331,318,4,422,423,436,417,420])).
% 60.88/60.96 cnf(1318,plain,
% 60.88/60.96 (~E(f3(a54),f3(a98))),
% 60.88/60.96 inference(scs_inference,[],[454,51,977,1278,194,104,46,1196,441,331,318,4,422,423,436,417,420,23,24])).
% 60.88/60.96 cnf(1319,plain,
% 60.88/60.96 (~E(f3(a109),f3(a65))),
% 60.88/60.96 inference(scs_inference,[],[454,51,977,1278,194,104,50,46,1196,441,331,318,4,422,423,436,417,420,23,24,25])).
% 60.88/60.96 cnf(1349,plain,
% 60.88/60.96 (P4(a202,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,1282,196,106,1237,4,423,422,417])).
% 60.88/60.96 cnf(1353,plain,
% 60.88/60.96 (~P8(f3(a98),f3(a43))),
% 60.88/60.96 inference(scs_inference,[],[454,51,1282,1314,196,106,45,1237,332,327,4,423,422,417,436,420])).
% 60.88/60.96 cnf(1358,plain,
% 60.88/60.96 (~E(f3(a109),f3(a54))),
% 60.88/60.96 inference(scs_inference,[],[454,51,1282,1314,196,106,50,45,1237,441,332,327,4,423,422,417,436,420,24,23,25])).
% 60.88/60.96 cnf(1390,plain,
% 60.88/60.96 (P4(a204,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,835,198,108,1274,333,309,4,422,423,436,417])).
% 60.88/60.96 cnf(1392,plain,
% 60.88/60.96 (~P8(f3(a98),f3(a4))),
% 60.88/60.96 inference(scs_inference,[],[454,51,835,1353,198,108,44,1274,333,309,4,422,423,436,417,420])).
% 60.88/60.96 cnf(1396,plain,
% 60.88/60.96 (~E(f3(a4),f3(a98))),
% 60.88/60.96 inference(scs_inference,[],[454,51,835,1353,198,108,44,1274,441,333,309,4,422,423,436,417,420,23,24])).
% 60.88/60.96 cnf(1397,plain,
% 60.88/60.96 (~E(f3(a109),f3(a43))),
% 60.88/60.96 inference(scs_inference,[],[454,51,835,1353,198,108,50,44,1274,441,333,309,4,422,423,436,417,420,23,24,25])).
% 60.88/60.96 cnf(1427,plain,
% 60.88/60.96 (P4(a208,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,838,201,111,1312,4,423,422,417])).
% 60.88/60.96 cnf(1431,plain,
% 60.88/60.96 (~P8(f3(a98),f3(a1))),
% 60.88/60.96 inference(scs_inference,[],[454,51,838,1392,201,111,43,1312,334,318,4,423,422,417,436,420])).
% 60.88/60.96 cnf(1468,plain,
% 60.88/60.96 (P4(a209,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,869,202,112,1349,337,4,422,423,436,417])).
% 60.88/60.96 cnf(1470,plain,
% 60.88/60.96 (~P8(f3(a65),f3(a54))),
% 60.88/60.96 inference(scs_inference,[],[454,51,869,202,112,46,1349,539,337,4,422,423,436,417,420])).
% 60.88/60.96 cnf(1474,plain,
% 60.88/60.96 (~E(f3(a2),f3(a98))),
% 60.88/60.96 inference(scs_inference,[],[454,51,869,1431,202,112,42,46,1349,539,441,337,4,422,423,436,417,420,23,24])).
% 60.88/60.96 cnf(1498,plain,
% 60.88/60.96 (P4(a212,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,909,205,115,1390,4,422,423,417])).
% 60.88/60.96 cnf(1502,plain,
% 60.88/60.96 (~P8(f3(a65),f3(a43))),
% 60.88/60.96 inference(scs_inference,[],[454,51,909,1470,205,115,45,1390,338,319,4,422,423,417,436,420])).
% 60.88/60.96 cnf(1507,plain,
% 60.88/60.96 (~E(f3(a76),f3(a54))),
% 60.88/60.96 inference(scs_inference,[],[454,51,909,1470,205,115,47,45,1390,441,338,319,4,422,423,417,436,420,23,24,25])).
% 60.88/60.96 cnf(1539,plain,
% 60.88/60.96 (P4(a214,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,939,207,117,1427,339,328,4,422,423,436,417])).
% 60.88/60.96 cnf(1541,plain,
% 60.88/60.96 (~P8(f3(a65),f3(a4))),
% 60.88/60.96 inference(scs_inference,[],[454,51,939,1502,207,117,44,1427,339,328,4,422,423,436,417,420])).
% 60.88/60.96 cnf(1546,plain,
% 60.88/60.96 (~E(f3(a76),f3(a43))),
% 60.88/60.96 inference(scs_inference,[],[454,51,939,1502,207,117,47,44,1427,441,339,328,4,422,423,436,417,420,23,24,25])).
% 60.88/60.96 cnf(1577,plain,
% 60.88/60.96 (P4(a215,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,1243,208,118,1468,4,422,423,417])).
% 60.88/60.96 cnf(1581,plain,
% 60.88/60.96 (~P8(f3(a65),f3(a1))),
% 60.88/60.96 inference(scs_inference,[],[454,51,1243,1541,208,118,43,1468,340,337,4,422,423,417,436,420])).
% 60.88/60.96 cnf(1585,plain,
% 60.88/60.96 (~E(f3(a1),f3(a65))),
% 60.88/60.96 inference(scs_inference,[],[454,51,1243,1541,208,118,43,1468,441,340,337,4,422,423,417,436,420,23,24])).
% 60.88/60.96 cnf(1586,plain,
% 60.88/60.96 (~E(f3(a76),f3(a4))),
% 60.88/60.96 inference(scs_inference,[],[454,51,1243,1541,208,118,47,43,1468,441,340,337,4,422,423,417,436,420,23,24,25])).
% 60.88/60.96 cnf(1620,plain,
% 60.88/60.96 (P4(a219,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,1318,211,121,1498,341,319,4,422,423,436,417])).
% 60.88/60.96 cnf(1622,plain,
% 60.88/60.96 (~P8(f3(a87),f3(a76))),
% 60.88/60.96 inference(scs_inference,[],[454,51,1318,211,121,48,1498,576,341,319,4,422,423,436,417,420])).
% 60.88/60.96 cnf(1626,plain,
% 60.88/60.96 (~E(f3(a2),f3(a65))),
% 60.88/60.96 inference(scs_inference,[],[454,51,1318,1581,211,121,42,48,1498,576,441,341,319,4,422,423,436,417,420,23,24])).
% 60.88/60.96 cnf(1658,plain,
% 60.88/60.96 (P4(a221,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,980,213,123,1539,4,422,423,417])).
% 60.88/60.96 cnf(1662,plain,
% 60.88/60.96 (~P8(f3(a87),f3(a65))),
% 60.88/60.96 inference(scs_inference,[],[454,51,980,1622,213,123,47,1539,342,328,4,422,423,417,436,420])).
% 60.88/60.96 cnf(1666,plain,
% 60.88/60.96 (~E(f3(a65),f3(a87))),
% 60.88/60.96 inference(scs_inference,[],[454,51,980,1622,213,123,47,1539,441,342,328,4,422,423,417,436,420,23,24])).
% 60.88/60.96 cnf(1700,plain,
% 60.88/60.96 (P4(a222,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,1017,214,124,1577,343,337,4,422,423,436,417])).
% 60.88/60.96 cnf(1702,plain,
% 60.88/60.96 (~P8(f3(a87),f3(a54))),
% 60.88/60.96 inference(scs_inference,[],[454,51,1017,1662,214,124,46,1577,343,337,4,422,423,436,417,420])).
% 60.88/60.96 cnf(1707,plain,
% 60.88/60.96 (~E(f3(a98),f3(a65))),
% 60.88/60.96 inference(scs_inference,[],[454,51,1017,1662,214,124,49,46,1577,441,343,337,4,422,423,436,417,420,23,24,25])).
% 60.88/60.96 cnf(1739,plain,
% 60.88/60.96 (P4(a225,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,1056,217,127,1620,347,4,422,423,436,417])).
% 60.88/60.96 cnf(1741,plain,
% 60.88/60.96 (~P8(f3(a87),f3(a43))),
% 60.88/60.96 inference(scs_inference,[],[454,51,1056,1702,217,127,45,1620,347,4,422,423,436,417,420])).
% 60.88/60.96 cnf(1778,plain,
% 60.88/60.96 (P4(a227,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,1059,219,129,1658,348,338,4,422,436,423,417])).
% 60.88/60.96 cnf(1780,plain,
% 60.88/60.96 (~P8(f3(a87),f3(a4))),
% 60.88/60.96 inference(scs_inference,[],[454,51,1059,1741,219,129,44,1658,348,338,4,422,436,423,417,420])).
% 60.88/60.96 cnf(1784,plain,
% 60.88/60.96 (~E(f3(a4),f3(a87))),
% 60.88/60.96 inference(scs_inference,[],[454,51,1059,1741,219,129,44,1658,441,348,338,4,422,436,423,417,420,23,24])).
% 60.88/60.96 cnf(1814,plain,
% 60.88/60.96 (P4(a230,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,1095,221,1700,4,423,417])).
% 60.88/60.96 cnf(1820,plain,
% 60.88/60.96 (~P8(f3(a87),f3(a1))),
% 60.88/60.96 inference(scs_inference,[],[454,51,1095,1780,221,131,43,1700,349,347,4,423,417,436,422,420])).
% 60.88/60.96 cnf(1825,plain,
% 60.88/60.96 (~E(f3(a98),f3(a4))),
% 60.88/60.96 inference(scs_inference,[],[454,51,1095,1780,221,131,49,43,1700,441,349,347,4,423,417,436,422,420,23,24,25])).
% 60.88/60.96 cnf(1857,plain,
% 60.88/60.96 (P4(a232,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,1096,223,133,1739,350,311,4,436,422,423,417])).
% 60.88/60.96 cnf(1859,plain,
% 60.88/60.96 (~P8(f3(a109),f3(a98))),
% 60.88/60.96 inference(scs_inference,[],[454,51,1096,223,133,50,1739,613,350,311,4,436,422,423,417,420])).
% 60.88/60.96 cnf(1862,plain,
% 60.88/60.96 (~P4(x18621,x18621)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(1864,plain,
% 60.88/60.96 (~E(f3(a98),f3(a1))),
% 60.88/60.96 inference(scs_inference,[],[454,51,1096,1820,223,133,49,50,42,1739,613,441,350,311,4,436,422,423,417,420,23,24,25])).
% 60.88/60.96 cnf(1866,plain,
% 60.88/60.96 (~P4(x18661,x18661)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(1870,plain,
% 60.88/60.96 (P10(a232,a102,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,1096,1820,223,224,133,49,50,42,1739,613,441,1862,1866,350,311,4,436,422,423,417,420,23,24,25,22,418,430])).
% 60.88/60.96 cnf(1890,plain,
% 60.88/60.96 (P4(a234,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,1134,225,1778,4,423,417])).
% 60.88/60.96 cnf(1896,plain,
% 60.88/60.96 (~P8(f3(a109),f3(a87))),
% 60.88/60.96 inference(scs_inference,[],[454,51,1134,1859,225,135,49,1778,351,338,4,423,417,422,436,420])).
% 60.88/60.96 cnf(1900,plain,
% 60.88/60.96 (~E(f3(a87),f3(a109))),
% 60.88/60.96 inference(scs_inference,[],[454,51,1134,1859,225,135,49,1778,441,351,338,4,423,417,422,436,420,23,24])).
% 60.88/60.96 cnf(1930,plain,
% 60.88/60.96 (~P8(f3(a109),f3(a76))),
% 60.88/60.96 inference(scs_inference,[],[48,1137,1896,227,137,4,422,420])).
% 60.88/60.96 cnf(1934,plain,
% 60.88/60.96 (P4(a236,a2)),
% 60.88/60.96 inference(scs_inference,[],[51,48,1137,1896,227,137,352,347,4,422,420,436,417])).
% 60.88/60.96 cnf(1940,plain,
% 60.88/60.96 (~E(f3(a76),f3(a109))),
% 60.88/60.96 inference(scs_inference,[],[454,51,48,1137,1896,227,137,1814,441,352,347,4,422,420,436,417,423,23,24])).
% 60.88/60.96 cnf(1966,plain,
% 60.88/60.96 (P4(a238,a2)),
% 60.88/60.96 inference(scs_inference,[],[51,1173,229,4,417])).
% 60.88/60.96 cnf(1974,plain,
% 60.88/60.96 (~P8(f3(a109),f3(a65))),
% 60.88/60.96 inference(scs_inference,[],[454,51,47,1173,1930,229,139,1857,357,4,417,423,422,436,420])).
% 60.88/60.96 cnf(1978,plain,
% 60.88/60.96 (~E(f3(a65),f3(a109))),
% 60.88/60.96 inference(scs_inference,[],[454,51,47,1173,1930,229,139,1857,441,357,4,417,423,422,436,420,23,24])).
% 60.88/60.96 cnf(2004,plain,
% 60.88/60.96 (~P8(f3(a109),f3(a54))),
% 60.88/60.96 inference(scs_inference,[],[46,1174,1974,4,420])).
% 60.88/60.96 cnf(2008,plain,
% 60.88/60.96 (P4(a241,a2)),
% 60.88/60.96 inference(scs_inference,[],[51,46,1174,1974,231,358,321,4,420,436,417])).
% 60.88/60.96 cnf(2016,plain,
% 60.88/60.96 (~E(f3(a54),f3(a109))),
% 60.88/60.96 inference(scs_inference,[],[454,51,46,1174,1974,231,141,1890,441,358,321,4,420,436,417,422,423,23,24])).
% 60.88/60.96 cnf(2042,plain,
% 60.88/60.96 (P3(a236,a121)),
% 60.88/60.96 inference(scs_inference,[],[454,1900,1934,4,423])).
% 60.88/60.96 cnf(2046,plain,
% 60.88/60.96 (~P8(f3(a109),f3(a43))),
% 60.88/60.96 inference(scs_inference,[],[454,45,1900,2004,233,143,1934,4,423,422,420])).
% 60.88/60.96 cnf(2088,plain,
% 60.88/60.96 (~P8(f3(a109),f3(a4))),
% 60.88/60.96 inference(scs_inference,[],[454,51,44,1940,2046,235,145,1966,360,348,4,417,436,423,422,420])).
% 60.88/60.96 cnf(2092,plain,
% 60.88/60.96 (~E(f3(a4),f3(a109))),
% 60.88/60.96 inference(scs_inference,[],[454,51,44,1940,2046,235,145,1966,441,360,348,4,417,436,423,422,420,23,24])).
% 60.88/60.96 cnf(2130,plain,
% 60.88/60.96 (~P4(x21301,x21301)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(2131,plain,
% 60.88/60.96 (~E(f3(a1),f3(a109))),
% 60.88/60.96 inference(scs_inference,[],[454,51,43,1978,2088,237,147,2008,441,361,357,4,436,417,422,423,420,23,24])).
% 60.88/60.96 cnf(2133,plain,
% 60.88/60.96 (~P4(x21331,x21331)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(2136,plain,
% 60.88/60.96 (~P8(f250(f3(a98),f3(a98)),f250(f3(a98),f3(a98)))),
% 60.88/60.96 inference(scs_inference,[],[454,51,43,1978,2088,237,238,147,2008,441,2130,2133,361,357,4,436,417,422,423,420,23,24,22,430,418])).
% 60.88/60.96 cnf(2158,plain,
% 60.88/60.96 (P4(a249,a2)),
% 60.88/60.96 inference(scs_inference,[],[51,2016,239,4,417])).
% 60.88/60.96 cnf(2160,plain,
% 60.88/60.96 (P6(f3(a2),f3(a76),f3(a2),f3(a76))),
% 60.88/60.96 inference(scs_inference,[],[51,2016,239,367,4,417,436])).
% 60.88/60.96 cnf(2196,plain,
% 60.88/60.96 (P4(a252,a2)),
% 60.88/60.96 inference(scs_inference,[],[51,1204,241,368,313,4,436,417])).
% 60.88/60.96 cnf(2260,plain,
% 60.88/60.96 (P4(a256,a2)),
% 60.88/60.96 inference(scs_inference,[],[51,2092,245,370,358,4,436,417])).
% 60.88/60.96 cnf(2264,plain,
% 60.88/60.96 (P3(a249,a121)),
% 60.88/60.96 inference(scs_inference,[],[454,51,2092,245,155,2158,370,358,4,436,417,422,423])).
% 60.88/60.96 cnf(2299,plain,
% 60.88/60.96 (P3(a252,a121)),
% 60.88/60.96 inference(scs_inference,[],[454,51,2131,247,157,2196,377,4,436,417,422,423])).
% 60.88/60.96 cnf(2302,plain,
% 60.88/60.96 (~P4(x23021,x23021)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(2305,plain,
% 60.88/60.96 (P10(a258,a129,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,2131,247,157,2196,441,2302,377,4,436,417,422,423,23,22,430])).
% 60.88/60.96 cnf(2365,plain,
% 60.88/60.96 (P3(a256,a121)),
% 60.88/60.96 inference(scs_inference,[],[454,51,1205,297,269,2260,379,368,4,436,417,422,423])).
% 60.88/60.96 cnf(2429,plain,
% 60.88/60.96 (P6(f3(a1),f3(a2),f3(a98),f3(a109))),
% 60.88/60.96 inference(scs_inference,[],[1283,388,315,4,436])).
% 60.88/60.96 cnf(2466,plain,
% 60.88/60.96 (P4(a142,a2)),
% 60.88/60.96 inference(scs_inference,[],[51,1319,284,397,4,436,417])).
% 60.88/60.96 cnf(2527,plain,
% 60.88/60.96 (P6(f3(a76),f3(a1),f3(a4),f3(a109))),
% 60.88/60.96 inference(scs_inference,[],[1358,343,319,4,436])).
% 60.88/60.96 cnf(2571,plain,
% 60.88/60.96 (~P4(x25711,x25711)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(2573,plain,
% 60.88/60.96 (~P4(x25731,x25731)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(2577,plain,
% 60.88/60.96 (~P4(x25771,x25771)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(2588,plain,
% 60.88/60.96 (P9(x25881,f120(f250(f3(a109),f3(a1))))+~E(a42,x25881)),
% 60.88/60.96 inference(scs_inference,[],[454,1870,51,1396,2160,2042,79,282,292,274,254,2466,441,2571,2573,2577,360,321,4,436,417,422,423,23,22,430,418,419,414,15,413,19,28])).
% 60.88/60.96 cnf(2597,plain,
% 60.88/60.96 (P6(f3(a54),f3(a4),f3(a43),f3(a109))),
% 60.88/60.96 inference(scs_inference,[],[1397,361,330,4,436])).
% 60.88/60.96 cnf(2599,plain,
% 60.88/60.96 (P4(a162,a2)),
% 60.88/60.96 inference(scs_inference,[],[51,1397,302,361,330,4,436,417])).
% 60.88/60.96 cnf(2687,plain,
% 60.88/60.96 (~E(a2,a98)),
% 60.88/60.96 inference(scs_inference,[],[1474,4])).
% 60.88/60.96 cnf(2690,plain,
% 60.88/60.96 (P4(a160,a2)),
% 60.88/60.96 inference(scs_inference,[],[51,1474,300,377,378,4,436,417])).
% 60.88/60.96 cnf(2694,plain,
% 60.88/60.96 (P3(a162,a121)),
% 60.88/60.96 inference(scs_inference,[],[454,51,1474,300,272,2599,377,378,4,436,417,422,423])).
% 60.88/60.96 cnf(2697,plain,
% 60.88/60.96 (~P4(x26971,x26971)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(2699,plain,
% 60.88/60.96 (~P4(x26991,x26991)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(2703,plain,
% 60.88/60.96 (~P4(x27031,x27031)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(2710,plain,
% 60.88/60.96 (P9(x27101,f120(f250(f3(a43),f3(a4))))+~E(a47,x27101)),
% 60.88/60.96 inference(scs_inference,[],[454,51,1474,83,300,279,261,272,2599,441,2697,2699,2703,377,378,4,436,417,422,423,23,22,430,418,419,414,28])).
% 60.88/60.96 cnf(2802,plain,
% 60.88/60.96 (~P4(x28021,x28021)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(2804,plain,
% 60.88/60.96 (~P4(x28041,x28041)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(2807,plain,
% 60.88/60.96 (~P8(f250(f3(a98),f250(f3(a4),f3(a1))),f250(f3(a98),f250(f3(a4),f3(a1))))),
% 60.88/60.96 inference(scs_inference,[],[454,51,1507,298,306,270,2690,441,2802,2804,333,327,4,436,417,423,422,23,22,430,418])).
% 60.88/60.96 cnf(2852,plain,
% 60.88/60.96 (P4(a206,a2)),
% 60.88/60.96 inference(scs_inference,[],[51,57,66,1546,351,329,4,436,422,417])).
% 60.88/60.96 cnf(2877,plain,
% 60.88/60.96 (P6(f3(a76),f3(a4),f3(a1),f3(a109))),
% 60.88/60.96 inference(scs_inference,[],[1585,343,328,4,436])).
% 60.88/60.96 cnf(2900,plain,
% 60.88/60.96 (P4(a135,a2)),
% 60.88/60.96 inference(scs_inference,[],[51,161,1586,339,337,4,436,417])).
% 60.88/60.96 cnf(2918,plain,
% 60.88/60.96 (~E(a2,a65)),
% 60.88/60.96 inference(scs_inference,[],[1626,4])).
% 60.88/60.96 cnf(2919,plain,
% 60.88/60.96 (P6(f3(a1),f3(a2),f3(a54),f3(a65))),
% 60.88/60.96 inference(scs_inference,[],[1626,348,311,4,436])).
% 60.88/60.96 cnf(2928,plain,
% 60.88/60.96 (~P4(x29281,x29281)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(2938,plain,
% 60.88/60.96 (P9(x29381,f120(f250(f3(a87),f3(a4))))+~E(a51,x29381)),
% 60.88/60.96 inference(scs_inference,[],[454,51,87,73,163,1626,2429,2264,2852,441,2928,348,311,4,436,417,422,423,23,22,430,414,15,413,28])).
% 60.88/60.96 cnf(2977,plain,
% 60.88/60.96 (P6(f3(a1),f3(a65),f3(a2),f3(a76))),
% 60.88/60.96 inference(scs_inference,[],[1666,357,358,4,436])).
% 60.88/60.96 cnf(2979,plain,
% 60.88/60.96 (P4(a170,a2)),
% 60.88/60.96 inference(scs_inference,[],[51,167,1666,357,358,4,436,417])).
% 60.88/60.96 cnf(2986,plain,
% 60.88/60.96 (~P4(x29861,x29861)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(2998,plain,
% 60.88/60.96 (P9(x29981,f120(f250(f3(a109),f3(a4))))+~E(a53,x29981)),
% 60.88/60.96 inference(scs_inference,[],[454,51,89,77,167,1666,2527,2299,2900,441,2986,357,358,4,436,417,422,423,23,22,430,414,16,29,413,17,28])).
% 60.88/60.96 cnf(3066,plain,
% 60.88/60.96 (~P4(x30661,x30661)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(3078,plain,
% 60.88/60.96 (P9(x30781,f120(f250(f3(a1),f3(a43))))+~E(a56,x30781)),
% 60.88/60.96 inference(scs_inference,[],[454,2305,51,91,83,173,1707,2597,2365,2979,441,3066,394,360,330,4,417,422,436,423,23,22,430,414,14,13,413,19,28])).
% 60.88/60.96 cnf(3142,plain,
% 60.88/60.96 (P4(a183,a2)),
% 60.88/60.96 inference(scs_inference,[],[51,179,1784,4,417])).
% 60.88/60.96 cnf(3231,plain,
% 60.88/60.96 (~P4(x32311,x32311)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(3241,plain,
% 60.88/60.96 (P9(x32411,f120(f250(f3(a65),f3(a43))))+~E(a60,x32411)),
% 60.88/60.96 inference(scs_inference,[],[454,51,95,185,1825,3142,441,3231,400,325,317,4,422,436,417,423,23,22,430,414,12,13,10,28])).
% 60.88/60.96 cnf(3280,plain,
% 60.88/60.96 (P4(a194,a2)),
% 60.88/60.96 inference(scs_inference,[],[51,189,1864,4,417])).
% 60.88/60.96 cnf(3338,plain,
% 60.88/60.96 (P4(a199,a2)),
% 60.88/60.96 inference(scs_inference,[],[51,193,341,310,436,417])).
% 60.88/60.96 cnf(3340,plain,
% 60.88/60.96 (P10(a69,a199,a2)),
% 60.88/60.96 inference(scs_inference,[],[51,103,193,341,310,436,417,422])).
% 60.88/60.96 cnf(3366,plain,
% 60.88/60.96 (P10(a71,a201,a2)),
% 60.88/60.96 inference(scs_inference,[],[105,195,342,319,436,422])).
% 60.88/60.96 cnf(3373,plain,
% 60.88/60.96 (~P4(x33731,x33731)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(3374,plain,
% 60.88/60.96 (~E(a201,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,105,195,3280,441,3373,342,319,436,422,417,423,23,22])).
% 60.88/60.96 cnf(3397,plain,
% 60.88/60.96 (P4(a203,a2)),
% 60.88/60.96 inference(scs_inference,[],[51,107,197,351,347,436,422,417])).
% 60.88/60.96 cnf(3430,plain,
% 60.88/60.96 (~P4(x34301,x34301)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(3440,plain,
% 60.88/60.96 (P9(x34401,f120(f250(f3(a109),f3(a54))))+~E(a75,x34401)),
% 60.88/60.96 inference(scs_inference,[],[454,51,109,199,2877,3338,441,3430,405,348,329,436,422,417,423,23,22,430,414,12,16,29,28])).
% 60.88/60.96 cnf(3453,plain,
% 60.88/60.96 (P4(a207,a2)),
% 60.88/60.96 inference(scs_inference,[],[51,110,200,349,311,422,436,417])).
% 60.88/60.96 cnf(3486,plain,
% 60.88/60.96 (~P4(x34861,x34861)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(3496,plain,
% 60.88/60.96 (P9(x34961,f120(f250(f3(a43),f3(a65))))+~E(a80,x34961)),
% 60.88/60.96 inference(scs_inference,[],[454,51,113,203,2919,3397,441,3486,336,339,358,422,436,417,423,23,22,430,414,14,10,17,28])).
% 60.88/60.96 cnf(3543,plain,
% 60.88/60.96 (~P4(x35431,x35431)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(3553,plain,
% 60.88/60.96 (P9(x35531,f120(f250(f3(a76),f3(a65))))+~E(a83,x35531)),
% 60.88/60.96 inference(scs_inference,[],[454,51,1270,116,206,2977,2694,3453,441,3543,360,312,422,436,417,423,23,22,430,414,27,15,26,28])).
% 60.88/60.96 cnf(3595,plain,
% 60.88/60.96 (P4(a218,a2)),
% 60.88/60.96 inference(scs_inference,[],[51,120,210,367,370,422,436,417])).
% 60.88/60.96 cnf(3669,plain,
% 60.88/60.96 (P4(a224,a2)),
% 60.88/60.96 inference(scs_inference,[],[51,126,216,422,417])).
% 60.88/60.96 cnf(3676,plain,
% 60.88/60.96 (~P4(x36761,x36761)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(3683,plain,
% 60.88/60.96 (P9(x36831,f120(f250(f3(a76),f3(a76))))+~E(a94,x36831)),
% 60.88/60.96 inference(scs_inference,[],[454,51,126,216,3595,441,3676,334,327,422,417,436,423,23,22,430,414,28])).
% 60.88/60.96 cnf(3752,plain,
% 60.88/60.96 (~P4(x37521,x37521)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(3759,plain,
% 60.88/60.96 (P9(x37591,f120(f250(f3(a4),f3(a87))))+~E(a101,x37591)),
% 60.88/60.96 inference(scs_inference,[],[454,51,132,222,3669,441,3752,333,318,422,417,436,423,23,22,430,414,28])).
% 60.88/60.96 cnf(4038,plain,
% 60.88/60.96 (P4(a255,a2)),
% 60.88/60.96 inference(scs_inference,[],[51,154,244,361,348,422,436,417])).
% 60.88/60.96 cnf(4118,plain,
% 60.88/60.96 (P4(a145,a2)),
% 60.88/60.96 inference(scs_inference,[],[454,51,259,287,4038,322,308,422,423,436,417])).
% 60.88/60.96 cnf(4144,plain,
% 60.88/60.96 (P4(a144,a2)),
% 60.88/60.96 inference(scs_inference,[],[51,258,286,334,309,422,436,417])).
% 60.88/60.96 cnf(4171,plain,
% 60.88/60.96 (P4(a143,a2)),
% 60.88/60.96 inference(scs_inference,[],[51,257,285,352,311,422,436,417])).
% 60.88/60.96 cnf(4248,plain,
% 60.88/60.96 (~P4(x42481,x42481)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(4255,plain,
% 60.88/60.96 (P9(x42551,f120(f250(f3(a65),f250(f3(a2),f3(a1)))))+~E(a12,x42551)),
% 60.88/60.96 inference(scs_inference,[],[51,255,283,441,4248,340,310,422,417,436,22,23,430,414,28])).
% 60.88/60.96 cnf(4501,plain,
% 60.88/60.96 (~P4(x45011,x45011)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(4502,plain,
% 60.88/60.96 (~E(a17,a167)),
% 60.88/60.96 inference(scs_inference,[],[164,72,441,4501,337,338,417,436,22,23])).
% 60.88/60.96 cnf(4560,plain,
% 60.88/60.96 (~P4(x45601,x45601)),
% 60.88/60.96 inference(rename_variables,[],[441])).
% 60.88/60.96 cnf(4561,plain,
% 60.88/60.96 (~E(a41,a174)),
% 60.88/60.96 inference(scs_inference,[],[170,78,441,4560,329,318,417,436,22,23])).
% 60.88/60.96 cnf(4563,plain,
% 60.88/60.96 (~P4(a41,a174)),
% 60.88/60.96 inference(scs_inference,[],[170,78,441,4560,329,318,417,436,22,23,414])).
% 60.88/60.96 cnf(4579,plain,
% 60.88/60.96 (P7(f3(a4))),
% 60.88/60.96 inference(scs_inference,[],[4118,444,34,1042,50,412,415,426,421,416,410])).
% 60.88/60.96 cnf(4584,plain,
% 60.88/60.96 (~P10(a4,a121,a2)),
% 60.88/60.96 inference(scs_inference,[],[556,1082,450,4118,444,34,1042,50,412,415,426,421,416,410,2,428,429])).
% 60.88/60.96 cnf(4590,plain,
% 60.88/60.96 (P8(f3(a87),f3(a109))),
% 60.88/60.96 inference(scs_inference,[],[556,1082,2687,450,4118,444,34,2807,2136,1042,50,49,412,415,426,421,416,410,2,428,429,24,25,427,420])).
% 60.88/60.96 cnf(4600,plain,
% 60.88/60.96 (~P9(a166,f120(x46001))),
% 60.88/60.96 inference(scs_inference,[],[556,1082,2687,450,528,4118,444,491,34,2807,542,2136,1042,306,52,50,49,441,412,415,426,421,416,410,2,428,429,24,25,427,420,424,20,413,422,417])).
% 60.88/60.96 cnf(4623,plain,
% 60.88/60.96 (~P9(a166,f120(x46231))),
% 60.88/60.96 inference(rename_variables,[],[4600])).
% 60.88/60.96 cnf(4625,plain,
% 60.88/60.96 (~P9(a166,f120(x46251))),
% 60.88/60.96 inference(rename_variables,[],[4600])).
% 60.88/60.96 cnf(4627,plain,
% 60.88/60.96 (~P9(a166,f120(x46271))),
% 60.88/60.96 inference(rename_variables,[],[4600])).
% 60.88/60.96 cnf(4629,plain,
% 60.88/60.96 (~P9(a166,f120(x46291))),
% 60.88/60.96 inference(rename_variables,[],[4600])).
% 60.88/60.96 cnf(4631,plain,
% 60.88/60.96 (~P9(a166,f120(x46311))),
% 60.88/60.96 inference(rename_variables,[],[4600])).
% 60.88/60.96 cnf(4633,plain,
% 60.88/60.96 (~P9(a166,f120(x46331))),
% 60.88/60.96 inference(rename_variables,[],[4600])).
% 60.88/60.96 cnf(4635,plain,
% 60.88/60.96 (~P9(a166,f120(x46351))),
% 60.88/60.96 inference(rename_variables,[],[4600])).
% 60.88/60.96 cnf(4637,plain,
% 60.88/60.96 (~P9(a166,f120(x46371))),
% 60.88/60.96 inference(rename_variables,[],[4600])).
% 60.88/60.96 cnf(4639,plain,
% 60.88/60.96 (~P9(a166,f120(x46391))),
% 60.88/60.96 inference(rename_variables,[],[4600])).
% 60.88/60.96 cnf(4641,plain,
% 60.88/60.96 (~P9(a166,f120(x46411))),
% 60.88/60.96 inference(rename_variables,[],[4600])).
% 60.88/60.96 cnf(4643,plain,
% 60.88/60.96 (~P9(a166,f120(x46431))),
% 60.88/60.96 inference(rename_variables,[],[4600])).
% 60.88/60.96 cnf(4645,plain,
% 60.88/60.97 (~P9(a166,f120(x46451))),
% 60.88/60.97 inference(rename_variables,[],[4600])).
% 60.88/60.97 cnf(4654,plain,
% 60.88/60.97 (P7(f3(a43))),
% 60.88/60.97 inference(scs_inference,[],[3340,4579,4590,4600,4623,4625,4627,4629,4631,4633,4635,4637,4639,4641,4643,35,4144,2588,2710,2938,2998,3078,3241,3440,3496,3553,3683,3759,4255,415,412,426,421,410])).
% 60.88/60.97 cnf(4667,plain,
% 60.88/60.97 (P8(f3(a76),f3(a109))),
% 60.88/60.97 inference(scs_inference,[],[519,622,3340,4579,4590,4600,4623,4625,4627,4629,4631,4633,4635,4637,4639,4641,4643,35,4144,491,499,48,454,2588,2710,2938,2998,3078,3241,3440,3496,3553,3683,3759,4255,415,412,426,421,410,416,2,429,428,427,423,420])).
% 60.88/60.97 cnf(4672,plain,
% 60.88/60.97 (~P9(a166,f120(x46721))),
% 60.88/60.97 inference(rename_variables,[],[4600])).
% 60.88/60.97 cnf(4679,plain,
% 60.88/60.97 (~P9(a176,f120(x46791))),
% 60.88/60.97 inference(scs_inference,[],[519,622,3340,4561,4563,4584,4579,4590,4600,4623,4625,4627,4629,4631,4633,4635,4637,4639,4641,4643,4645,4672,35,4144,462,491,499,103,172,306,53,48,441,454,2588,2710,2938,2998,3078,3241,3440,3496,3553,3683,3759,4255,415,412,426,421,410,416,2,429,428,427,423,420,424,28,413,29,19,422,417])).
% 60.88/60.97 cnf(4680,plain,
% 60.88/60.97 (~P4(x46801,x46801)),
% 60.88/60.97 inference(rename_variables,[],[441])).
% 60.88/60.97 cnf(4692,plain,
% 60.88/60.97 (~P6(f3(a2),f3(a4),f3(a65),f3(a87))),
% 60.88/60.97 inference(scs_inference,[],[407,519,622,3340,4561,4563,4584,4579,4590,4600,4623,4625,4627,4629,4631,4633,4635,4637,4639,4641,4643,4645,4672,35,4144,616,462,491,499,380,103,377,58,172,306,53,62,65,67,308,48,441,4680,454,2588,2710,2938,2998,3078,3241,3440,3496,3553,3683,3759,4255,415,412,426,421,410,416,2,429,428,427,423,420,424,28,413,29,19,422,417,437,418,419,1109,430,432])).
% 60.88/60.97 cnf(4700,plain,
% 60.88/60.97 (~P9(a176,f120(x47001))),
% 60.88/60.97 inference(rename_variables,[],[4679])).
% 60.88/60.97 cnf(4702,plain,
% 60.88/60.97 (~P9(a176,f120(x47021))),
% 60.88/60.97 inference(rename_variables,[],[4679])).
% 60.88/60.97 cnf(4704,plain,
% 60.88/60.97 (~P9(a176,f120(x47041))),
% 60.88/60.97 inference(rename_variables,[],[4679])).
% 60.88/60.97 cnf(4708,plain,
% 60.88/60.97 (~P9(a176,f120(x47081))),
% 60.88/60.97 inference(rename_variables,[],[4679])).
% 60.88/60.97 cnf(4710,plain,
% 60.88/60.97 (~P9(a176,f120(x47101))),
% 60.88/60.97 inference(rename_variables,[],[4679])).
% 60.88/60.97 cnf(4712,plain,
% 60.88/60.97 (~P9(a176,f120(x47121))),
% 60.88/60.97 inference(rename_variables,[],[4679])).
% 60.88/60.97 cnf(4714,plain,
% 60.88/60.97 (~P9(a176,f120(x47141))),
% 60.88/60.97 inference(rename_variables,[],[4679])).
% 60.88/60.97 cnf(4718,plain,
% 60.88/60.97 (~P9(a176,f120(x47181))),
% 60.88/60.97 inference(rename_variables,[],[4679])).
% 60.88/60.97 cnf(4722,plain,
% 60.88/60.97 (~P9(a176,f120(x47221))),
% 60.88/60.97 inference(rename_variables,[],[4679])).
% 60.88/60.97 cnf(4724,plain,
% 60.88/60.97 (~P9(a176,f120(x47241))),
% 60.88/60.97 inference(rename_variables,[],[4679])).
% 60.88/60.97 cnf(4726,plain,
% 60.88/60.97 (~P9(a176,f120(x47261))),
% 60.88/60.97 inference(rename_variables,[],[4679])).
% 60.88/60.97 cnf(4748,plain,
% 60.88/60.97 ($false),
% 60.88/60.97 inference(scs_inference,[],[702,2918,488,3374,3366,705,4502,4654,4667,4679,4700,4702,4704,4708,4710,4712,4714,4718,4722,4724,4726,4692,36,4171,504,105,332,377,47,415,3553,2710,2588,421,3759,2938,3496,2998,426,3440,412,3241,4255,3683,3078,410,416,2,429,428,427,420,424,413,422,436]),
% 60.88/60.97 ['proof']).
% 60.88/60.97 % SZS output end Proof
% 60.88/60.97 % Total time :60.360000s
%------------------------------------------------------------------------------