%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWV204+1 : TPTP v8.2.0. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/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 16:46:03 EDT 2024
% Result : Theorem 25.11s 25.22s
% Output : CNFRefutation 25.11s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SWV204+1 : TPTP v8.2.0. Bugfixed v3.3.0.
% 0.07/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n032.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu Jun 20 21:08:53 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.19/0.54 start to proof:theBenchmark
% 25.06/25.21 %-------------------------------------------
% 25.06/25.21 % File :CSE---1.7
% 25.06/25.21 % Problem :theBenchmark
% 25.06/25.21 % Transform :cnf
% 25.06/25.21 % Format :tptp:raw
% 25.06/25.21 % Command :java -jar mcs_scs.jar %d %s
% 25.06/25.21
% 25.06/25.21 % Result :Theorem 24.470000s
% 25.06/25.21 % Output :CNFRefutation 24.470000s
% 25.06/25.21 %-------------------------------------------
% 25.06/25.21 %------------------------------------------------------------------------------
% 25.06/25.21 % File : SWV204+1 : TPTP v8.2.0. Bugfixed v3.3.0.
% 25.06/25.21 % Domain : Software Verification
% 25.06/25.21 % Problem : Simplified proof obligation quaternion_ds1_inuse_0015
% 25.06/25.21 % Version : [DFS04] axioms : Especial.
% 25.06/25.21 % English : Proof obligation emerging from the inuse-safety verification for
% 25.06/25.21 % the quaternion_ds1 program. inuse-safety ensures that each sensor
% 25.06/25.21 % reading passed as an input to the Kalman filter algorithm is
% 25.06/25.21 % actually used during the computation of the output estimate.
% 25.06/25.21
% 25.06/25.21 % Refs : [Fis04] Fischer (2004), Email to G. Sutcliffe
% 25.06/25.21 % : [DFS04] Denney et al. (2004), Using Automated Theorem Provers
% 25.06/25.21 % Source : [Fis04]
% 25.06/25.21 % Names : quaternion_ds1_inuse_0015 [Fis04]
% 25.06/25.21
% 25.06/25.21 % Status : Theorem
% 25.06/25.21 % Rating : 0.33 v8.2.0, 0.28 v8.1.0, 0.22 v7.5.0, 0.25 v7.4.0, 0.23 v7.3.0, 0.24 v7.2.0, 0.21 v7.1.0, 0.30 v6.4.0, 0.27 v6.3.0, 0.29 v6.2.0, 0.36 v6.1.0, 0.40 v6.0.0, 0.30 v5.5.0, 0.48 v5.4.0, 0.54 v5.3.0, 0.52 v5.2.0, 0.50 v5.1.0, 0.52 v5.0.0, 0.54 v4.1.0, 0.52 v4.0.0, 0.58 v3.7.0, 0.55 v3.5.0, 0.58 v3.3.0
% 25.06/25.21 % Syntax : Number of formulae : 92 ( 56 unt; 0 def)
% 25.06/25.22 % Number of atoms : 296 ( 110 equ)
% 25.06/25.22 % Maximal formula atoms : 40 ( 3 avg)
% 25.06/25.22 % Number of connectives : 209 ( 5 ~; 17 |; 127 &)
% 25.06/25.22 % ( 5 <=>; 55 =>; 0 <=; 0 <~>)
% 25.06/25.22 % Maximal formula depth : 36 ( 4 avg)
% 25.06/25.22 % Maximal term depth : 9 ( 1 avg)
% 25.06/25.22 % Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% 25.06/25.22 % Number of functors : 36 ( 36 usr; 18 con; 0-4 aty)
% 25.06/25.22 % Number of variables : 173 ( 173 !; 0 ?)
% 25.06/25.22 % SPC : FOF_THM_RFO_SEQ
% 25.06/25.22
% 25.06/25.22 % Comments :
% 25.06/25.22 % Bugfixes : v3.3.0 - Bugfix in SWV003+0
% 25.06/25.22 %------------------------------------------------------------------------------
% 25.06/25.22 %----Include NASA software certification axioms
% 25.06/25.22 include('Axioms/SWV003+0.ax').
% 25.06/25.22 %------------------------------------------------------------------------------
% 25.06/25.22 %----Proof obligation generated by the AutoBayes/AutoFilter system
% 25.06/25.22 fof(quaternion_ds1_inuse_0015,conjecture,
% 25.06/25.22 ( ( a_select2(rho_defuse,n0) = use
% 25.06/25.22 & a_select2(rho_defuse,n1) = use
% 25.06/25.22 & a_select2(rho_defuse,n2) = use
% 25.06/25.22 & a_select2(sigma_defuse,n0) = use
% 25.06/25.22 & a_select2(sigma_defuse,n1) = use
% 25.06/25.22 & a_select2(sigma_defuse,n2) = use
% 25.06/25.22 & a_select2(sigma_defuse,n3) = use
% 25.06/25.22 & a_select2(sigma_defuse,n4) = use
% 25.06/25.22 & a_select2(sigma_defuse,n5) = use
% 25.06/25.22 & a_select3(u_defuse,n0,n0) = use
% 25.08/25.22 & a_select3(u_defuse,n1,n0) = use
% 25.08/25.22 & a_select3(u_defuse,n2,n0) = use
% 25.08/25.22 & a_select2(xinit_defuse,n3) = use
% 25.08/25.22 & a_select2(xinit_defuse,n4) = use
% 25.08/25.22 & a_select2(xinit_defuse,n5) = use
% 25.08/25.22 & a_select2(xinit_mean_defuse,n0) = use
% 25.08/25.22 & a_select2(xinit_mean_defuse,n1) = use
% 25.08/25.22 & a_select2(xinit_mean_defuse,n2) = use
% 25.08/25.22 & a_select2(xinit_mean_defuse,n3) = use
% 25.08/25.22 & a_select2(xinit_mean_defuse,n4) = use
% 25.08/25.22 & a_select2(xinit_mean_defuse,n5) = use
% 25.08/25.22 & a_select2(xinit_noise_defuse,n0) = use
% 25.08/25.22 & a_select2(xinit_noise_defuse,n1) = use
% 25.08/25.22 & a_select2(xinit_noise_defuse,n2) = use
% 25.08/25.22 & a_select2(xinit_noise_defuse,n3) = use
% 25.08/25.22 & a_select2(xinit_noise_defuse,n4) = use
% 25.08/25.22 & a_select2(xinit_noise_defuse,n5) = use
% 25.08/25.22 & ! [A,B] :
% 25.08/25.22 ( ( leq(n0,A)
% 25.08/25.22 & leq(n0,B)
% 25.08/25.22 & leq(A,n2)
% 25.08/25.22 & leq(B,n998) )
% 25.08/25.22 => a_select3(u_defuse,A,B) = use )
% 25.08/25.22 & ! [C,D] :
% 25.08/25.22 ( ( leq(n0,C)
% 25.08/25.22 & leq(n0,D)
% 25.08/25.22 & leq(C,n2)
% 25.08/25.22 & leq(D,n998) )
% 25.08/25.22 => a_select3(z_defuse,C,D) = use ) )
% 25.08/25.22 => ! [E] :
% 25.08/25.22 ( ( leq(n0,E)
% 25.08/25.22 & leq(E,n2) )
% 25.08/25.22 => a_select2(rho_defuse,E) = use ) ) ).
% 25.08/25.22
% 25.08/25.22 %----Automatically generated axioms
% 25.08/25.22
% 25.08/25.22 fof(gt_5_4,axiom,
% 25.08/25.22 gt(n5,n4) ).
% 25.08/25.22
% 25.08/25.22 fof(gt_998_4,axiom,
% 25.08/25.22 gt(n998,n4) ).
% 25.08/25.22
% 25.08/25.22 fof(gt_998_5,axiom,
% 25.08/25.22 gt(n998,n5) ).
% 25.08/25.22
% 25.08/25.22 fof(gt_4_tptp_minus_1,axiom,
% 25.08/25.22 gt(n4,tptp_minus_1) ).
% 25.08/25.22
% 25.08/25.22 fof(gt_5_tptp_minus_1,axiom,
% 25.08/25.22 gt(n5,tptp_minus_1) ).
% 25.08/25.22
% 25.08/25.22 fof(gt_998_tptp_minus_1,axiom,
% 25.08/25.22 gt(n998,tptp_minus_1) ).
% 25.08/25.22
% 25.08/25.22 fof(gt_0_tptp_minus_1,axiom,
% 25.08/25.22 gt(n0,tptp_minus_1) ).
% 25.08/25.22
% 25.08/25.22 fof(gt_1_tptp_minus_1,axiom,
% 25.08/25.22 gt(n1,tptp_minus_1) ).
% 25.08/25.22
% 25.08/25.22 fof(gt_2_tptp_minus_1,axiom,
% 25.08/25.22 gt(n2,tptp_minus_1) ).
% 25.08/25.22
% 25.08/25.22 fof(gt_3_tptp_minus_1,axiom,
% 25.08/25.22 gt(n3,tptp_minus_1) ).
% 25.08/25.22
% 25.08/25.22 fof(gt_4_0,axiom,
% 25.08/25.22 gt(n4,n0) ).
% 25.08/25.22
% 25.08/25.22 fof(gt_5_0,axiom,
% 25.08/25.22 gt(n5,n0) ).
% 25.08/25.22
% 25.08/25.22 fof(gt_998_0,axiom,
% 25.08/25.22 gt(n998,n0) ).
% 25.08/25.22
% 25.08/25.22 fof(gt_1_0,axiom,
% 25.08/25.22 gt(n1,n0) ).
% 25.08/25.22
% 25.08/25.22 fof(gt_2_0,axiom,
% 25.08/25.22 gt(n2,n0) ).
% 25.08/25.22
% 25.08/25.22 fof(gt_3_0,axiom,
% 25.08/25.22 gt(n3,n0) ).
% 25.08/25.22
% 25.08/25.22 fof(gt_4_1,axiom,
% 25.08/25.22 gt(n4,n1) ).
% 25.08/25.22
% 25.08/25.22 fof(gt_5_1,axiom,
% 25.08/25.22 gt(n5,n1) ).
% 25.08/25.22
% 25.08/25.22 fof(gt_998_1,axiom,
% 25.08/25.22 gt(n998,n1) ).
% 25.08/25.22
% 25.08/25.22 fof(gt_2_1,axiom,
% 25.08/25.22 gt(n2,n1) ).
% 25.08/25.22
% 25.08/25.22 fof(gt_3_1,axiom,
% 25.08/25.22 gt(n3,n1) ).
% 25.08/25.22
% 25.08/25.22 fof(gt_4_2,axiom,
% 25.08/25.22 gt(n4,n2) ).
% 25.08/25.22
% 25.08/25.22 fof(gt_5_2,axiom,
% 25.08/25.22 gt(n5,n2) ).
% 25.08/25.22
% 25.08/25.22 fof(gt_998_2,axiom,
% 25.08/25.22 gt(n998,n2) ).
% 25.08/25.22
% 25.08/25.22 fof(gt_3_2,axiom,
% 25.08/25.22 gt(n3,n2) ).
% 25.08/25.22
% 25.08/25.22 fof(gt_4_3,axiom,
% 25.08/25.22 gt(n4,n3) ).
% 25.08/25.22
% 25.08/25.22 fof(gt_5_3,axiom,
% 25.08/25.22 gt(n5,n3) ).
% 25.08/25.22
% 25.08/25.22 fof(gt_998_3,axiom,
% 25.08/25.22 gt(n998,n3) ).
% 25.08/25.22
% 25.08/25.22 fof(finite_domain_4,axiom,
% 25.08/25.22 ! [X] :
% 25.08/25.22 ( ( leq(n0,X)
% 25.08/25.22 & leq(X,n4) )
% 25.08/25.22 => ( X = n0
% 25.08/25.22 | X = n1
% 25.08/25.22 | X = n2
% 25.08/25.22 | X = n3
% 25.08/25.22 | X = n4 ) ) ).
% 25.08/25.22
% 25.08/25.22 fof(finite_domain_5,axiom,
% 25.08/25.22 ! [X] :
% 25.08/25.22 ( ( leq(n0,X)
% 25.08/25.22 & leq(X,n5) )
% 25.08/25.22 => ( X = n0
% 25.08/25.22 | X = n1
% 25.08/25.22 | X = n2
% 25.08/25.22 | X = n3
% 25.08/25.22 | X = n4
% 25.08/25.22 | X = n5 ) ) ).
% 25.08/25.22
% 25.08/25.22 fof(finite_domain_0,axiom,
% 25.08/25.22 ! [X] :
% 25.08/25.22 ( ( leq(n0,X)
% 25.08/25.22 & leq(X,n0) )
% 25.08/25.22 => X = n0 ) ).
% 25.08/25.22
% 25.08/25.22 fof(finite_domain_1,axiom,
% 25.08/25.22 ! [X] :
% 25.08/25.22 ( ( leq(n0,X)
% 25.08/25.22 & leq(X,n1) )
% 25.08/25.22 => ( X = n0
% 25.08/25.22 | X = n1 ) ) ).
% 25.08/25.22
% 25.08/25.22 fof(finite_domain_2,axiom,
% 25.08/25.22 ! [X] :
% 25.08/25.22 ( ( leq(n0,X)
% 25.08/25.22 & leq(X,n2) )
% 25.08/25.22 => ( X = n0
% 25.08/25.22 | X = n1
% 25.08/25.22 | X = n2 ) ) ).
% 25.08/25.22
% 25.08/25.22 fof(finite_domain_3,axiom,
% 25.08/25.22 ! [X] :
% 25.11/25.22 ( ( leq(n0,X)
% 25.11/25.22 & leq(X,n3) )
% 25.11/25.22 => ( X = n0
% 25.11/25.22 | X = n1
% 25.11/25.22 | X = n2
% 25.11/25.22 | X = n3 ) ) ).
% 25.11/25.22
% 25.11/25.22 fof(successor_4,axiom,
% 25.11/25.22 succ(succ(succ(succ(n0)))) = n4 ).
% 25.11/25.22
% 25.11/25.22 fof(successor_5,axiom,
% 25.11/25.22 succ(succ(succ(succ(succ(n0))))) = n5 ).
% 25.11/25.22
% 25.11/25.22 fof(successor_1,axiom,
% 25.11/25.22 succ(n0) = n1 ).
% 25.11/25.22
% 25.11/25.22 fof(successor_2,axiom,
% 25.11/25.22 succ(succ(n0)) = n2 ).
% 25.11/25.22
% 25.11/25.22 fof(successor_3,axiom,
% 25.11/25.22 succ(succ(succ(n0))) = n3 ).
% 25.11/25.22
% 25.11/25.22 %------------------------------------------------------------------------------
% 25.11/25.22 %-------------------------------------------
% 25.11/25.22 % Proof found
% 25.11/25.22 % SZS status Theorem for theBenchmark
% 25.11/25.22 % SZS output start Proof
% 25.11/25.22 %ClaNum:377(EqnAxiom:147)
% 25.11/25.22 %VarNum:2809(SingletonVarNum:665)
% 25.11/25.22 %MaxLitNum:8
% 25.11/25.22 %MaxfuncDepth:5
% 25.11/25.22 %SharedTerms:122
% 25.11/25.22 %goalClause: 149 180 181 204
% 25.11/25.22 %singleGoalClaCount:4
% 25.11/25.22 [148]P1(a5000)
% 25.11/25.22 [149]P2(a5000)
% 25.11/25.22 [152]P4(a1,a43)
% 25.11/25.22 [153]P4(a36,a1)
% 25.11/25.22 [154]P4(a36,a43)
% 25.11/25.22 [155]P4(a38,a1)
% 25.11/25.23 [156]P4(a38,a43)
% 25.11/25.23 [157]P4(a38,a36)
% 25.11/25.23 [158]P4(a39,a1)
% 25.11/25.23 [159]P4(a39,a43)
% 25.11/25.23 [160]P4(a39,a36)
% 25.11/25.23 [161]P4(a39,a38)
% 25.11/25.23 [162]P4(a40,a1)
% 25.11/25.23 [163]P4(a40,a43)
% 25.11/25.23 [164]P4(a40,a36)
% 25.11/25.23 [165]P4(a40,a38)
% 25.11/25.23 [166]P4(a40,a39)
% 25.11/25.23 [167]P4(a41,a1)
% 25.11/25.23 [168]P4(a41,a43)
% 25.11/25.23 [169]P4(a41,a36)
% 25.11/25.23 [170]P4(a41,a38)
% 25.11/25.23 [171]P4(a41,a39)
% 25.11/25.23 [172]P4(a41,a40)
% 25.11/25.23 [173]P4(a42,a1)
% 25.11/25.23 [174]P4(a42,a43)
% 25.11/25.23 [175]P4(a42,a36)
% 25.11/25.23 [176]P4(a42,a38)
% 25.11/25.23 [177]P4(a42,a39)
% 25.11/25.23 [178]P4(a42,a40)
% 25.11/25.23 [179]P4(a42,a41)
% 25.11/25.23 [180]P6(a1,a2)
% 25.11/25.23 [181]P6(a2,a38)
% 25.11/25.23 [203]~E(a5,a55)
% 25.11/25.23 [150]E(f37(a1,a36),a36)
% 25.11/25.23 [151]E(f37(a43,a36),a1)
% 25.11/25.23 [204]~E(f3(a45,a2),a55)
% 25.11/25.23 [184]E(f37(f37(a1,a36),a36),a38)
% 25.11/25.23 [192]E(f37(f37(f37(a1,a36),a36),a36),a39)
% 25.11/25.23 [196]E(f37(f37(f37(f37(a1,a36),a36),a36),a36),a40)
% 25.11/25.23 [199]E(f37(f37(f37(f37(f37(a1,a36),a36),a36),a36),a36),a41)
% 25.11/25.23 [182]P6(x1821,x1821)
% 25.11/25.23 [205]~P4(x2051,x2051)
% 25.11/25.23 [183]E(f37(a36,x1831),f37(x1831,a36))
% 25.11/25.23 [187]P4(f37(x1871,a36),x1871)
% 25.11/25.23 [190]E(f44(a1,a43,x1901),a47)
% 25.11/25.23 [191]E(f44(a1,a43,x1911),a1)
% 25.11/25.23 [185]E(f37(f22(x1851,a36),a36),x1851)
% 25.11/25.23 [186]E(f22(f37(x1861,a36),a36),x1861)
% 25.11/25.23 [188]E(f37(f37(x1881,a36),a36),f37(x1881,a38))
% 25.11/25.23 [189]E(f37(f37(x1891,a36),a36),f37(a38,x1891))
% 25.11/25.23 [193]E(f37(f37(f37(x1931,a36),a36),a36),f37(x1931,a39))
% 25.11/25.23 [194]E(f37(f37(f37(x1941,a36),a36),a36),f37(a39,x1941))
% 25.11/25.23 [197]E(f37(f37(f37(f37(x1971,a36),a36),a36),a36),f37(x1971,a40))
% 25.11/25.23 [198]E(f37(f37(f37(f37(x1981,a36),a36),a36),a36),f37(a40,x1981))
% 25.11/25.23 [200]E(f37(f37(f37(f37(f37(x2001,a36),a36),a36),a36),a36),f37(x2001,a41))
% 25.11/25.23 [201]E(f37(f37(f37(f37(f37(x2011,a36),a36),a36),a36),a36),f37(a41,x2011))
% 25.11/25.23 [195]E(f3(f51(x1951,x1952,x1953),x1952),x1953)
% 25.11/25.23 [202]E(f4(f54(x2021,x2022,x2023,x2024),x2022,x2023),x2024)
% 25.11/25.23 [206]~P2(a5000)+E(f3(a45,a1),a55)
% 25.11/25.23 [207]~P2(a5000)+E(f3(a45,a36),a55)
% 25.11/25.23 [208]~P2(a5000)+E(f3(a45,a38),a55)
% 25.11/25.23 [209]~P2(a5000)+E(f3(a46,a1),a55)
% 25.11/25.23 [210]~P2(a5000)+E(f3(a46,a36),a55)
% 25.11/25.23 [211]~P2(a5000)+E(f3(a46,a38),a55)
% 25.11/25.23 [212]~P2(a5000)+E(f3(a46,a39),a55)
% 25.11/25.23 [213]~P2(a5000)+E(f3(a46,a40),a55)
% 25.11/25.23 [214]~P2(a5000)+E(f3(a46,a41),a55)
% 25.11/25.23 [215]~P2(a5000)+E(f3(a59,a39),a55)
% 25.11/25.23 [216]~P2(a5000)+E(f3(a59,a40),a55)
% 25.11/25.23 [217]~P2(a5000)+E(f3(a59,a41),a55)
% 25.11/25.23 [218]~P2(a5000)+E(f3(a60,a1),a55)
% 25.11/25.23 [219]~P2(a5000)+E(f3(a60,a36),a55)
% 25.11/25.23 [220]~P2(a5000)+E(f3(a60,a38),a55)
% 25.11/25.23 [221]~P2(a5000)+E(f3(a60,a39),a55)
% 25.11/25.23 [222]~P2(a5000)+E(f3(a60,a40),a55)
% 25.11/25.23 [223]~P2(a5000)+E(f3(a60,a41),a55)
% 25.11/25.23 [224]~P2(a5000)+E(f3(a61,a1),a55)
% 25.11/25.23 [225]~P2(a5000)+E(f3(a61,a36),a55)
% 25.11/25.23 [226]~P2(a5000)+E(f3(a61,a38),a55)
% 25.11/25.23 [227]~P2(a5000)+E(f3(a61,a39),a55)
% 25.11/25.23 [228]~P2(a5000)+E(f3(a61,a40),a55)
% 25.11/25.23 [229]~P2(a5000)+E(f3(a61,a41),a55)
% 25.11/25.23 [243]~P2(a5000)+E(f4(a56,a1,a1),a55)
% 25.11/25.23 [244]~P2(a5000)+E(f4(a56,a36,a1),a55)
% 25.11/25.23 [245]~P2(a5000)+E(f4(a56,a38,a1),a55)
% 25.11/25.23 [231]~P7(x2312,x2311)+P4(x2311,x2312)
% 25.11/25.23 [232]~P4(x2322,x2321)+P6(x2321,x2322)
% 25.11/25.23 [233]~P5(x2332,x2331)+P6(x2331,x2332)
% 25.11/25.23 [234]~P4(x2342,x2341)+P7(x2341,x2342)
% 25.11/25.23 [235]~P6(x2352,x2351)+P5(x2351,x2352)
% 25.11/25.23 [246]~P6(a1,x2462)+P6(a1,f58(x2461,x2462))
% 25.11/25.23 [249]~P4(x2492,x2491)+P6(x2491,f22(x2492,a36))
% 25.11/25.23 [250]~P6(x2501,x2502)+P6(x2501,f37(x2502,a36))
% 25.11/25.23 [251]~P6(x2512,x2511)+P4(f37(x2511,a36),x2512)
% 25.11/25.23 [252]~P6(a1,x2522)+P6(f58(x2521,x2522),x2522)
% 25.11/25.23 [253]P4(x2531,x2532)+~P6(x2532,f22(x2531,a36))
% 25.11/25.23 [254]P4(x2541,x2542)+~P6(f37(x2542,a36),x2541)
% 25.11/25.23 [255]P6(x2551,x2552)+~P4(f37(x2552,a36),x2551)
% 25.11/25.23 [256]~P6(f22(x2562,x2561),x2562)+P6(a1,x2561)
% 25.11/25.23 [257]~P6(x2571,x2572)+P6(f37(x2571,a36),f37(x2572,a36))
% 25.11/25.23 [258]P6(x2581,x2582)+~P6(f37(x2581,a36),f37(x2582,a36))
% 25.11/25.23 [237]~P6(x2371,a1)+~P6(a1,x2371)+E(x2371,a1)
% 25.11/25.23 [230]P4(x2302,x2301)+P4(x2301,x2302)+E(x2301,x2302)
% 25.11/25.23 [236]P4(x2362,x2361)+~P6(x2361,x2362)+E(x2361,x2362)
% 25.11/25.23 [247]~P4(x2471,x2473)+P4(x2471,x2472)+~P4(x2473,x2472)
% 25.11/25.23 [248]~P6(x2481,x2483)+P6(x2481,x2482)+~P6(x2483,x2482)
% 25.11/25.23 [336]P3(x3361,x3362,x3363,x3364)+P6(a1,f24(x3364,x3363,x3362,x3361))+P6(a1,f25(x3364,x3363,x3362,x3361))
% 25.11/25.23 [337]P3(x3371,x3372,x3373,x3374)+P6(a1,f24(x3374,x3373,x3372,x3371))+P6(a1,f27(x3374,x3373,x3372,x3371))
% 25.11/25.23 [338]P3(x3381,x3382,x3383,x3384)+P6(a1,f26(x3384,x3383,x3382,x3381))+P6(a1,f25(x3384,x3383,x3382,x3381))
% 25.11/25.23 [339]P3(x3391,x3392,x3393,x3394)+P6(a1,f26(x3394,x3393,x3392,x3391))+P6(a1,f27(x3394,x3393,x3392,x3391))
% 25.11/25.23 [340]P3(x3401,x3402,x3403,x3404)+P6(f24(x3404,x3403,x3402,x3401),x3403)+P6(a1,f25(x3404,x3403,x3402,x3401))
% 25.11/25.23 [341]P3(x3411,x3412,x3413,x3414)+P6(f24(x3414,x3413,x3412,x3411),x3413)+P6(a1,f27(x3414,x3413,x3412,x3411))
% 25.11/25.23 [342]P3(x3421,x3422,x3423,x3424)+P6(f26(x3424,x3423,x3422,x3421),x3423)+P6(a1,f25(x3424,x3423,x3422,x3421))
% 25.11/25.23 [343]P3(x3431,x3432,x3433,x3434)+P6(f26(x3434,x3433,x3432,x3431),x3433)+P6(a1,f27(x3434,x3433,x3432,x3431))
% 25.11/25.23 [344]P3(x3441,x3442,x3443,x3444)+P6(f25(x3444,x3443,x3442,x3441),x3442)+P6(a1,f24(x3444,x3443,x3442,x3441))
% 25.11/25.23 [345]P3(x3451,x3452,x3453,x3454)+P6(f25(x3454,x3453,x3452,x3451),x3452)+P6(a1,f26(x3454,x3453,x3452,x3451))
% 25.11/25.23 [346]P3(x3461,x3462,x3463,x3464)+P6(f27(x3464,x3463,x3462,x3461),x3462)+P6(a1,f24(x3464,x3463,x3462,x3461))
% 25.11/25.23 [347]P3(x3471,x3472,x3473,x3474)+P6(f27(x3474,x3473,x3472,x3471),x3472)+P6(a1,f26(x3474,x3473,x3472,x3471))
% 25.11/25.23 [348]P3(x3481,x3482,x3483,x3484)+P6(f24(x3484,x3483,x3482,x3481),x3483)+P6(f25(x3484,x3483,x3482,x3481),x3482)
% 25.11/25.23 [349]P3(x3491,x3492,x3493,x3494)+P6(f24(x3494,x3493,x3492,x3491),x3493)+P6(f27(x3494,x3493,x3492,x3491),x3492)
% 25.11/25.23 [350]P3(x3501,x3502,x3503,x3504)+P6(f26(x3504,x3503,x3502,x3501),x3503)+P6(f25(x3504,x3503,x3502,x3501),x3502)
% 25.11/25.23 [351]P3(x3511,x3512,x3513,x3514)+P6(f26(x3514,x3513,x3512,x3511),x3513)+P6(f27(x3514,x3513,x3512,x3511),x3512)
% 25.11/25.23 [359]P3(x3591,x3592,x3593,x3594)+P6(a1,f25(x3594,x3593,x3592,x3591))+~E(f4(x3594,f26(x3594,x3593,x3592,x3591),f24(x3594,x3593,x3592,x3591)),f4(x3594,f24(x3594,x3593,x3592,x3591),f26(x3594,x3593,x3592,x3591)))
% 25.11/25.23 [360]P3(x3601,x3602,x3603,x3604)+P6(a1,f27(x3604,x3603,x3602,x3601))+~E(f4(x3604,f26(x3604,x3603,x3602,x3601),f24(x3604,x3603,x3602,x3601)),f4(x3604,f24(x3604,x3603,x3602,x3601),f26(x3604,x3603,x3602,x3601)))
% 25.11/25.23 [361]P3(x3611,x3612,x3613,x3614)+P6(a1,f24(x3614,x3613,x3612,x3611))+~E(f4(x3611,f27(x3614,x3613,x3612,x3611),f25(x3614,x3613,x3612,x3611)),f4(x3611,f25(x3614,x3613,x3612,x3611),f27(x3614,x3613,x3612,x3611)))
% 25.11/25.23 [362]P3(x3621,x3622,x3623,x3624)+P6(a1,f26(x3624,x3623,x3622,x3621))+~E(f4(x3621,f27(x3624,x3623,x3622,x3621),f25(x3624,x3623,x3622,x3621)),f4(x3621,f25(x3624,x3623,x3622,x3621),f27(x3624,x3623,x3622,x3621)))
% 25.11/25.23 [363]P3(x3631,x3632,x3633,x3634)+P6(f25(x3634,x3633,x3632,x3631),x3632)+~E(f4(x3634,f26(x3634,x3633,x3632,x3631),f24(x3634,x3633,x3632,x3631)),f4(x3634,f24(x3634,x3633,x3632,x3631),f26(x3634,x3633,x3632,x3631)))
% 25.11/25.23 [364]P3(x3641,x3642,x3643,x3644)+P6(f27(x3644,x3643,x3642,x3641),x3642)+~E(f4(x3644,f26(x3644,x3643,x3642,x3641),f24(x3644,x3643,x3642,x3641)),f4(x3644,f24(x3644,x3643,x3642,x3641),f26(x3644,x3643,x3642,x3641)))
% 25.11/25.23 [365]P3(x3651,x3652,x3653,x3654)+P6(f24(x3654,x3653,x3652,x3651),x3653)+~E(f4(x3651,f27(x3654,x3653,x3652,x3651),f25(x3654,x3653,x3652,x3651)),f4(x3651,f25(x3654,x3653,x3652,x3651),f27(x3654,x3653,x3652,x3651)))
% 25.11/25.23 [366]P3(x3661,x3662,x3663,x3664)+P6(f26(x3664,x3663,x3662,x3661),x3663)+~E(f4(x3661,f27(x3664,x3663,x3662,x3661),f25(x3664,x3663,x3662,x3661)),f4(x3661,f25(x3664,x3663,x3662,x3661),f27(x3664,x3663,x3662,x3661)))
% 25.11/25.23 [367]P3(x3671,x3672,x3673,x3674)+~E(f4(x3674,f26(x3674,x3673,x3672,x3671),f24(x3674,x3673,x3672,x3671)),f4(x3674,f24(x3674,x3673,x3672,x3671),f26(x3674,x3673,x3672,x3671)))+~E(f4(x3671,f27(x3674,x3673,x3672,x3671),f25(x3674,x3673,x3672,x3671)),f4(x3671,f25(x3674,x3673,x3672,x3671),f27(x3674,x3673,x3672,x3671)))
% 25.11/25.23 [261]~P6(x2614,x2612)+~P6(x2611,x2614)+E(f3(f48(f6(x2611,x2612),x2613),x2614),x2613)
% 25.11/25.23 [262]E(x2621,x2622)+~E(f3(x2623,x2622),x2625)+E(f3(f51(x2623,x2621,x2624),x2622),x2625)
% 25.11/25.23 [238]E(x2381,a36)+~P6(x2381,a36)+~P6(a1,x2381)+E(x2381,a1)
% 25.11/25.23 [315]~P6(x3154,x3152)+~P6(a1,x3154)+P6(a1,f18(x3154,x3152,x3151,x3153))+E(f3(f51(x3151,x3152,x3153),x3154),x3153)
% 25.11/25.23 [316]~P6(x3164,x3162)+P6(f18(x3164,x3162,x3161,x3163),x3162)+~P6(a1,x3164)+E(f3(f51(x3161,x3162,x3163),x3164),x3163)
% 25.11/25.23 [317]~P6(x3174,x3172)+~P6(a1,x3174)+~E(f3(x3171,f18(x3174,x3172,x3171,x3173)),x3173)+E(f3(f51(x3171,x3172,x3173),x3174),x3173)
% 25.11/25.23 [314]~E(x3144,x3146)+E(x3141,x3142)+~E(f4(x3143,x3142,x3146),x3147)+E(f4(f54(x3143,x3141,x3144,x3145),x3142,x3146),x3147)
% 25.11/25.23 [239]E(x2391,a36)+E(x2391,a38)+~P6(x2391,a38)+~P6(a1,x2391)+E(x2391,a1)
% 25.11/25.23 [271]~P6(x2717,x2714)+~P6(x2713,x2717)+~P6(x2716,x2712)+~P6(x2711,x2716)+E(f4(f49(f6(x2711,x2712),f6(x2713,x2714),x2715),x2716,x2717),x2715)
% 25.11/25.23 [240]E(x2401,a36)+E(x2401,a38)+E(x2401,a39)+~P6(x2401,a39)+~P6(a1,x2401)+E(x2401,a1)
% 25.11/25.23 [259]~P6(x2592,a42)+~P6(x2591,a38)+~P6(a1,x2592)+~P6(a1,x2591)+~P2(a5000)+E(f4(a56,x2591,x2592),a55)
% 25.11/25.23 [260]~P6(x2602,a42)+~P6(x2601,a38)+~P6(a1,x2602)+~P6(a1,x2601)+~P2(a5000)+E(f4(a62,x2601,x2602),a55)
% 25.11/25.23 [263]~P6(x2633,x2634)+~P6(x2632,x2634)+~P6(a1,x2633)+~P6(a1,x2632)+E(f4(f57(x2631),x2632,x2633),f4(f57(x2631),x2633,x2632))+P6(a1,f7(x2631,x2634))
% 25.11/25.23 [264]~P6(x2643,x2644)+~P6(x2642,x2644)+~P6(a1,x2643)+~P6(a1,x2642)+E(f4(f57(x2641),x2642,x2643),f4(f57(x2641),x2643,x2642))+P6(a1,f23(x2641,x2644))
% 25.11/25.23 [265]~P6(x2653,x2654)+~P6(x2652,x2654)+~P6(a1,x2653)+~P6(a1,x2652)+E(f4(f28(x2651),x2652,x2653),f4(f28(x2651),x2653,x2652))+P6(a1,f29(x2651,x2654))
% 25.11/25.23 [266]~P6(x2663,x2664)+~P6(x2662,x2664)+~P6(a1,x2663)+~P6(a1,x2662)+E(f4(f28(x2661),x2662,x2663),f4(f28(x2661),x2663,x2662))+P6(a1,f30(x2661,x2664))
% 25.11/25.23 [267]~P6(x2673,x2674)+~P6(x2672,x2674)+~P6(a1,x2673)+~P6(a1,x2672)+P6(f7(x2671,x2674),x2674)+E(f4(f57(x2671),x2672,x2673),f4(f57(x2671),x2673,x2672))
% 25.11/25.23 [268]~P6(x2683,x2684)+~P6(x2682,x2684)+~P6(a1,x2683)+~P6(a1,x2682)+P6(f23(x2681,x2684),x2684)+E(f4(f57(x2681),x2682,x2683),f4(f57(x2681),x2683,x2682))
% 25.11/25.23 [269]~P6(x2693,x2694)+~P6(x2692,x2694)+~P6(a1,x2693)+~P6(a1,x2692)+P6(f29(x2691,x2694),x2694)+E(f4(f28(x2691),x2692,x2693),f4(f28(x2691),x2693,x2692))
% 25.11/25.23 [270]~P6(x2703,x2704)+~P6(x2702,x2704)+~P6(a1,x2703)+~P6(a1,x2702)+P6(f30(x2701,x2704),x2704)+E(f4(f28(x2701),x2702,x2703),f4(f28(x2701),x2703,x2702))
% 25.11/25.23 [312]~P6(x3123,x3124)+~P6(x3122,x3124)+~P6(a1,x3123)+~P6(a1,x3122)+~E(f4(x3121,f23(x3121,x3124),f7(x3121,x3124)),f4(x3121,f7(x3121,x3124),f23(x3121,x3124)))+E(f4(f57(x3121),x3122,x3123),f4(f57(x3121),x3123,x3122))
% 25.11/25.23 [313]~P6(x3133,x3134)+~P6(x3132,x3134)+~P6(a1,x3133)+~P6(a1,x3132)+~E(f4(x3131,f30(x3131,x3134),f29(x3131,x3134)),f4(x3131,f29(x3131,x3134),f30(x3131,x3134)))+E(f4(f28(x3131),x3132,x3133),f4(f28(x3131),x3133,x3132))
% 25.11/25.23 [306]~P6(x3064,x3065)+~P6(x3063,x3065)+~P6(a1,x3064)+~P6(a1,x3063)+P6(a1,f14(x3061,x3062,x3065))+E(f4(f53(x3061,f53(x3062,f57(x3061))),x3063,x3064),f4(f53(x3061,f53(x3062,f57(x3061))),x3064,x3063))
% 25.11/25.23 [307]~P6(x3074,x3075)+~P6(x3073,x3075)+~P6(a1,x3074)+~P6(a1,x3073)+P6(a1,f15(x3071,x3072,x3075))+E(f4(f53(x3071,f53(x3072,f57(x3071))),x3073,x3074),f4(f53(x3071,f53(x3072,f57(x3071))),x3074,x3073))
% 25.11/25.23 [310]~P6(x3104,x3105)+~P6(x3103,x3105)+~P6(a1,x3104)+~P6(a1,x3103)+P6(f14(x3101,x3102,x3105),x3105)+E(f4(f53(x3101,f53(x3102,f57(x3101))),x3103,x3104),f4(f53(x3101,f53(x3102,f57(x3101))),x3104,x3103))
% 25.11/25.23 [311]~P6(x3114,x3115)+~P6(x3113,x3115)+~P6(a1,x3114)+~P6(a1,x3113)+P6(f15(x3111,x3112,x3115),x3115)+E(f4(f53(x3111,f53(x3112,f57(x3111))),x3113,x3114),f4(f53(x3111,f53(x3112,f57(x3111))),x3114,x3113))
% 25.11/25.23 [335]~P6(x3354,x3355)+~P6(x3353,x3355)+~P6(a1,x3354)+~P6(a1,x3353)+~E(f4(x3352,f15(x3351,x3352,x3355),f14(x3351,x3352,x3355)),f4(x3352,f14(x3351,x3352,x3355),f15(x3351,x3352,x3355)))+E(f4(f53(x3351,f53(x3352,f57(x3351))),x3353,x3354),f4(f53(x3351,f53(x3352,f57(x3351))),x3354,x3353))
% 25.11/25.23 [368]~P6(x3686,x3683)+~P6(x3685,x3682)+~P6(a1,x3686)+~P6(a1,x3685)+P6(a1,f19(x3685,x3686,x3682,x3683,x3681,x3684))+E(f4(f54(x3681,x3682,x3683,x3684),x3685,x3686),x3684)
% 25.11/25.23 [369]~P6(x3696,x3693)+~P6(x3695,x3692)+~P6(a1,x3696)+~P6(a1,x3695)+P6(a1,f21(x3695,x3696,x3692,x3693,x3691,x3694))+E(f4(f54(x3691,x3692,x3693,x3694),x3695,x3696),x3694)
% 25.11/25.23 [370]~P6(x3706,x3703)+~P6(x3705,x3702)+P6(f19(x3705,x3706,x3702,x3703,x3701,x3704),x3702)+~P6(a1,x3706)+~P6(a1,x3705)+E(f4(f54(x3701,x3702,x3703,x3704),x3705,x3706),x3704)
% 25.11/25.23 [371]~P6(x3716,x3713)+~P6(x3715,x3712)+P6(f21(x3715,x3716,x3712,x3713,x3711,x3714),x3713)+~P6(a1,x3716)+~P6(a1,x3715)+E(f4(f54(x3711,x3712,x3713,x3714),x3715,x3716),x3714)
% 25.11/25.23 [372]~P6(x3726,x3723)+~P6(x3725,x3722)+~P6(a1,x3726)+~P6(a1,x3725)+~E(f4(x3721,f19(x3725,x3726,x3722,x3723,x3721,x3724),f21(x3725,x3726,x3722,x3723,x3721,x3724)),x3724)+E(f4(f54(x3721,x3722,x3723,x3724),x3725,x3726),x3724)
% 25.11/25.23 [304]~P6(x3043,x3046)+~P6(x3044,x3046)+~P6(a1,x3044)+~P6(a1,x3043)+P6(a1,f13(x3041,x3042,x3045))+E(f4(f53(x3041,f53(x3042,f57(x3041))),x3043,x3044),f4(f53(x3041,f53(x3042,f57(x3041))),x3044,x3043))
% 25.11/25.23 [305]~P6(x3053,x3056)+~P6(x3054,x3056)+~P6(a1,x3054)+~P6(a1,x3053)+P6(a1,f16(x3051,x3052,x3055))+E(f4(f53(x3051,f53(x3052,f57(x3051))),x3053,x3054),f4(f53(x3051,f53(x3052,f57(x3051))),x3054,x3053))
% 25.11/25.23 [308]~P6(x3083,x3086)+~P6(x3084,x3086)+~P6(a1,x3084)+~P6(a1,x3083)+P6(f13(x3081,x3082,x3085),x3085)+E(f4(f53(x3081,f53(x3082,f57(x3081))),x3083,x3084),f4(f53(x3081,f53(x3082,f57(x3081))),x3084,x3083))
% 25.11/25.23 [309]~P6(x3093,x3096)+~P6(x3094,x3096)+~P6(a1,x3094)+~P6(a1,x3093)+P6(f16(x3091,x3092,x3095),x3095)+E(f4(f53(x3091,f53(x3092,f57(x3091))),x3093,x3094),f4(f53(x3091,f53(x3092,f57(x3091))),x3094,x3093))
% 25.11/25.23 [334]~P6(x3343,x3346)+~P6(x3344,x3346)+~P6(a1,x3344)+~P6(a1,x3343)+~E(f4(x3342,f16(x3341,x3342,x3345),f13(x3341,x3342,x3345)),f4(x3342,f13(x3341,x3342,x3345),f16(x3341,x3342,x3345)))+E(f4(f53(x3341,f53(x3342,f57(x3341))),x3343,x3344),f4(f53(x3341,f53(x3342,f57(x3341))),x3344,x3343))
% 25.11/25.23 [241]E(x2411,a36)+E(x2411,a38)+E(x2411,a39)+E(x2411,a40)+~P6(x2411,a40)+~P6(a1,x2411)+E(x2411,a1)
% 25.11/25.23 [272]~P6(x2724,x2725)+~P6(x2723,x2725)+~P6(a1,x2724)+~P6(a1,x2723)+P6(a1,f34(x2721,x2722,x2725))+E(f4(f50(x2721,x2722),x2723,x2724),f4(f50(x2721,x2722),x2724,x2723))+P6(a1,f31(x2721,x2722,x2725))
% 25.11/25.23 [273]~P6(x2734,x2735)+~P6(x2733,x2735)+~P6(a1,x2734)+~P6(a1,x2733)+P6(a1,f8(x2731,x2732,x2735))+E(f4(f50(x2731,x2732),x2733,x2734),f4(f50(x2731,x2732),x2734,x2733))+P6(a1,f31(x2731,x2732,x2735))
% 25.11/25.23 [274]~P6(x2744,x2745)+~P6(x2743,x2745)+~P6(a1,x2744)+~P6(a1,x2743)+P6(a1,f34(x2741,x2742,x2745))+E(f4(f50(x2741,x2742),x2743,x2744),f4(f50(x2741,x2742),x2744,x2743))+P6(a1,f35(x2741,x2742,x2745))
% 25.11/25.23 [275]~P6(x2754,x2755)+~P6(x2753,x2755)+~P6(a1,x2754)+~P6(a1,x2753)+P6(a1,f8(x2751,x2752,x2755))+E(f4(f50(x2751,x2752),x2753,x2754),f4(f50(x2751,x2752),x2754,x2753))+P6(a1,f35(x2751,x2752,x2755))
% 25.11/25.23 [276]~P6(x2764,x2765)+~P6(x2763,x2765)+~P6(a1,x2764)+~P6(a1,x2763)+P6(a1,f10(x2761,x2762,x2765))+E(f4(f52(x2761,x2762),x2763,x2764),f4(f52(x2761,x2762),x2764,x2763))+P6(a1,f9(x2761,x2762,x2765))
% 25.11/25.23 [277]~P6(x2774,x2775)+~P6(x2773,x2775)+~P6(a1,x2774)+~P6(a1,x2773)+P6(a1,f12(x2771,x2772,x2775))+E(f4(f52(x2771,x2772),x2773,x2774),f4(f52(x2771,x2772),x2774,x2773))+P6(a1,f9(x2771,x2772,x2775))
% 25.11/25.23 [278]~P6(x2784,x2785)+~P6(x2783,x2785)+~P6(a1,x2784)+~P6(a1,x2783)+P6(a1,f10(x2781,x2782,x2785))+E(f4(f52(x2781,x2782),x2783,x2784),f4(f52(x2781,x2782),x2784,x2783))+P6(a1,f11(x2781,x2782,x2785))
% 25.11/25.23 [279]~P6(x2794,x2795)+~P6(x2793,x2795)+~P6(a1,x2794)+~P6(a1,x2793)+P6(a1,f12(x2791,x2792,x2795))+E(f4(f52(x2791,x2792),x2793,x2794),f4(f52(x2791,x2792),x2794,x2793))+P6(a1,f11(x2791,x2792,x2795))
% 25.11/25.23 [280]~P6(x2804,x2805)+~P6(x2803,x2805)+~P6(a1,x2804)+~P6(a1,x2803)+P6(f31(x2801,x2802,x2805),x2805)+P6(a1,f34(x2801,x2802,x2805))+E(f4(f50(x2801,x2802),x2803,x2804),f4(f50(x2801,x2802),x2804,x2803))
% 25.11/25.23 [281]~P6(x2814,x2815)+~P6(x2813,x2815)+~P6(a1,x2814)+~P6(a1,x2813)+P6(f31(x2811,x2812,x2815),x2815)+P6(a1,f8(x2811,x2812,x2815))+E(f4(f50(x2811,x2812),x2813,x2814),f4(f50(x2811,x2812),x2814,x2813))
% 25.11/25.23 [282]~P6(x2824,x2825)+~P6(x2823,x2825)+~P6(a1,x2824)+~P6(a1,x2823)+P6(f35(x2821,x2822,x2825),x2825)+P6(a1,f34(x2821,x2822,x2825))+E(f4(f50(x2821,x2822),x2823,x2824),f4(f50(x2821,x2822),x2824,x2823))
% 25.11/25.23 [283]~P6(x2834,x2835)+~P6(x2833,x2835)+~P6(a1,x2834)+~P6(a1,x2833)+P6(f35(x2831,x2832,x2835),x2835)+P6(a1,f8(x2831,x2832,x2835))+E(f4(f50(x2831,x2832),x2833,x2834),f4(f50(x2831,x2832),x2834,x2833))
% 25.11/25.23 [284]~P6(x2844,x2845)+~P6(x2843,x2845)+~P6(a1,x2844)+~P6(a1,x2843)+P6(f34(x2841,x2842,x2845),x2845)+P6(a1,f31(x2841,x2842,x2845))+E(f4(f50(x2841,x2842),x2843,x2844),f4(f50(x2841,x2842),x2844,x2843))
% 25.11/25.23 [285]~P6(x2854,x2855)+~P6(x2853,x2855)+~P6(a1,x2854)+~P6(a1,x2853)+P6(f34(x2851,x2852,x2855),x2855)+P6(a1,f35(x2851,x2852,x2855))+E(f4(f50(x2851,x2852),x2853,x2854),f4(f50(x2851,x2852),x2854,x2853))
% 25.11/25.23 [286]~P6(x2864,x2865)+~P6(x2863,x2865)+~P6(a1,x2864)+~P6(a1,x2863)+P6(f8(x2861,x2862,x2865),x2865)+P6(a1,f31(x2861,x2862,x2865))+E(f4(f50(x2861,x2862),x2863,x2864),f4(f50(x2861,x2862),x2864,x2863))
% 25.11/25.23 [287]~P6(x2874,x2875)+~P6(x2873,x2875)+~P6(a1,x2874)+~P6(a1,x2873)+P6(f8(x2871,x2872,x2875),x2875)+P6(a1,f35(x2871,x2872,x2875))+E(f4(f50(x2871,x2872),x2873,x2874),f4(f50(x2871,x2872),x2874,x2873))
% 25.11/25.23 [288]~P6(x2884,x2885)+~P6(x2883,x2885)+~P6(a1,x2884)+~P6(a1,x2883)+P6(f9(x2881,x2882,x2885),x2885)+P6(a1,f10(x2881,x2882,x2885))+E(f4(f52(x2881,x2882),x2883,x2884),f4(f52(x2881,x2882),x2884,x2883))
% 25.11/25.23 [289]~P6(x2894,x2895)+~P6(x2893,x2895)+~P6(a1,x2894)+~P6(a1,x2893)+P6(f9(x2891,x2892,x2895),x2895)+P6(a1,f12(x2891,x2892,x2895))+E(f4(f52(x2891,x2892),x2893,x2894),f4(f52(x2891,x2892),x2894,x2893))
% 25.11/25.23 [290]~P6(x2904,x2905)+~P6(x2903,x2905)+~P6(a1,x2904)+~P6(a1,x2903)+P6(f11(x2901,x2902,x2905),x2905)+P6(a1,f10(x2901,x2902,x2905))+E(f4(f52(x2901,x2902),x2903,x2904),f4(f52(x2901,x2902),x2904,x2903))
% 25.11/25.23 [291]~P6(x2914,x2915)+~P6(x2913,x2915)+~P6(a1,x2914)+~P6(a1,x2913)+P6(f11(x2911,x2912,x2915),x2915)+P6(a1,f12(x2911,x2912,x2915))+E(f4(f52(x2911,x2912),x2913,x2914),f4(f52(x2911,x2912),x2914,x2913))
% 25.11/25.23 [292]~P6(x2924,x2925)+~P6(x2923,x2925)+~P6(a1,x2924)+~P6(a1,x2923)+P6(f10(x2921,x2922,x2925),x2925)+P6(a1,f9(x2921,x2922,x2925))+E(f4(f52(x2921,x2922),x2923,x2924),f4(f52(x2921,x2922),x2924,x2923))
% 25.11/25.23 [293]~P6(x2934,x2935)+~P6(x2933,x2935)+~P6(a1,x2934)+~P6(a1,x2933)+P6(f10(x2931,x2932,x2935),x2935)+P6(a1,f11(x2931,x2932,x2935))+E(f4(f52(x2931,x2932),x2933,x2934),f4(f52(x2931,x2932),x2934,x2933))
% 25.11/25.23 [294]~P6(x2944,x2945)+~P6(x2943,x2945)+~P6(a1,x2944)+~P6(a1,x2943)+P6(f12(x2941,x2942,x2945),x2945)+P6(a1,f9(x2941,x2942,x2945))+E(f4(f52(x2941,x2942),x2943,x2944),f4(f52(x2941,x2942),x2944,x2943))
% 25.11/25.23 [295]~P6(x2954,x2955)+~P6(x2953,x2955)+~P6(a1,x2954)+~P6(a1,x2953)+P6(f12(x2951,x2952,x2955),x2955)+P6(a1,f11(x2951,x2952,x2955))+E(f4(f52(x2951,x2952),x2953,x2954),f4(f52(x2951,x2952),x2954,x2953))
% 25.11/25.23 [296]~P6(x2964,x2965)+~P6(x2963,x2965)+P6(f34(x2961,x2962,x2965),x2965)+~P6(a1,x2964)+~P6(a1,x2963)+P6(f31(x2961,x2962,x2965),x2965)+E(f4(f50(x2961,x2962),x2963,x2964),f4(f50(x2961,x2962),x2964,x2963))
% 25.11/25.23 [297]~P6(x2974,x2975)+~P6(x2973,x2975)+P6(f8(x2971,x2972,x2975),x2975)+~P6(a1,x2974)+~P6(a1,x2973)+P6(f31(x2971,x2972,x2975),x2975)+E(f4(f50(x2971,x2972),x2973,x2974),f4(f50(x2971,x2972),x2974,x2973))
% 25.11/25.23 [298]~P6(x2984,x2985)+~P6(x2983,x2985)+P6(f34(x2981,x2982,x2985),x2985)+~P6(a1,x2984)+~P6(a1,x2983)+P6(f35(x2981,x2982,x2985),x2985)+E(f4(f50(x2981,x2982),x2983,x2984),f4(f50(x2981,x2982),x2984,x2983))
% 25.11/25.23 [299]~P6(x2994,x2995)+~P6(x2993,x2995)+P6(f8(x2991,x2992,x2995),x2995)+~P6(a1,x2994)+~P6(a1,x2993)+P6(f35(x2991,x2992,x2995),x2995)+E(f4(f50(x2991,x2992),x2993,x2994),f4(f50(x2991,x2992),x2994,x2993))
% 25.11/25.23 [300]~P6(x3004,x3005)+~P6(x3003,x3005)+P6(f10(x3001,x3002,x3005),x3005)+~P6(a1,x3004)+~P6(a1,x3003)+P6(f9(x3001,x3002,x3005),x3005)+E(f4(f52(x3001,x3002),x3003,x3004),f4(f52(x3001,x3002),x3004,x3003))
% 25.11/25.23 [301]~P6(x3014,x3015)+~P6(x3013,x3015)+P6(f12(x3011,x3012,x3015),x3015)+~P6(a1,x3014)+~P6(a1,x3013)+P6(f9(x3011,x3012,x3015),x3015)+E(f4(f52(x3011,x3012),x3013,x3014),f4(f52(x3011,x3012),x3014,x3013))
% 25.11/25.23 [302]~P6(x3024,x3025)+~P6(x3023,x3025)+P6(f10(x3021,x3022,x3025),x3025)+~P6(a1,x3024)+~P6(a1,x3023)+P6(f11(x3021,x3022,x3025),x3025)+E(f4(f52(x3021,x3022),x3023,x3024),f4(f52(x3021,x3022),x3024,x3023))
% 25.11/25.23 [303]~P6(x3034,x3035)+~P6(x3033,x3035)+P6(f12(x3031,x3032,x3035),x3035)+~P6(a1,x3034)+~P6(a1,x3033)+P6(f11(x3031,x3032,x3035),x3035)+E(f4(f52(x3031,x3032),x3033,x3034),f4(f52(x3031,x3032),x3034,x3033))
% 25.11/25.23 [318]~P6(x3184,x3185)+~P6(x3183,x3185)+~P6(a1,x3184)+~P6(a1,x3183)+~E(f4(x3182,f8(x3181,x3182,x3185),f34(x3181,x3182,x3185)),f4(x3182,f34(x3181,x3182,x3185),f8(x3181,x3182,x3185)))+E(f4(f50(x3181,x3182),x3183,x3184),f4(f50(x3181,x3182),x3184,x3183))+P6(a1,f31(x3181,x3182,x3185))
% 25.11/25.23 [319]~P6(x3194,x3195)+~P6(x3193,x3195)+~P6(a1,x3194)+~P6(a1,x3193)+~E(f4(x3192,f8(x3191,x3192,x3195),f34(x3191,x3192,x3195)),f4(x3192,f34(x3191,x3192,x3195),f8(x3191,x3192,x3195)))+E(f4(f50(x3191,x3192),x3193,x3194),f4(f50(x3191,x3192),x3194,x3193))+P6(a1,f35(x3191,x3192,x3195))
% 25.11/25.23 [320]~P6(x3204,x3205)+~P6(x3203,x3205)+~P6(a1,x3204)+~P6(a1,x3203)+~E(f4(x3201,f35(x3201,x3202,x3205),f31(x3201,x3202,x3205)),f4(x3201,f31(x3201,x3202,x3205),f35(x3201,x3202,x3205)))+E(f4(f50(x3201,x3202),x3203,x3204),f4(f50(x3201,x3202),x3204,x3203))+P6(a1,f34(x3201,x3202,x3205))
% 25.11/25.23 [321]~P6(x3214,x3215)+~P6(x3213,x3215)+~P6(a1,x3214)+~P6(a1,x3213)+~E(f4(x3211,f35(x3211,x3212,x3215),f31(x3211,x3212,x3215)),f4(x3211,f31(x3211,x3212,x3215),f35(x3211,x3212,x3215)))+E(f4(f50(x3211,x3212),x3213,x3214),f4(f50(x3211,x3212),x3214,x3213))+P6(a1,f8(x3211,x3212,x3215))
% 25.11/25.23 [322]~P6(x3224,x3225)+~P6(x3223,x3225)+~P6(a1,x3224)+~P6(a1,x3223)+~E(f4(x3222,f12(x3221,x3222,x3225),f10(x3221,x3222,x3225)),f4(x3222,f10(x3221,x3222,x3225),f12(x3221,x3222,x3225)))+E(f4(f52(x3221,x3222),x3223,x3224),f4(f52(x3221,x3222),x3224,x3223))+P6(a1,f9(x3221,x3222,x3225))
% 25.11/25.23 [323]~P6(x3234,x3235)+~P6(x3233,x3235)+~P6(a1,x3234)+~P6(a1,x3233)+~E(f4(x3232,f12(x3231,x3232,x3235),f10(x3231,x3232,x3235)),f4(x3232,f10(x3231,x3232,x3235),f12(x3231,x3232,x3235)))+E(f4(f52(x3231,x3232),x3233,x3234),f4(f52(x3231,x3232),x3234,x3233))+P6(a1,f11(x3231,x3232,x3235))
% 25.11/25.23 [324]~P6(x3244,x3245)+~P6(x3243,x3245)+~P6(a1,x3244)+~P6(a1,x3243)+~E(f4(x3241,f11(x3241,x3242,x3245),f9(x3241,x3242,x3245)),f4(x3241,f9(x3241,x3242,x3245),f11(x3241,x3242,x3245)))+E(f4(f52(x3241,x3242),x3243,x3244),f4(f52(x3241,x3242),x3244,x3243))+P6(a1,f10(x3241,x3242,x3245))
% 25.11/25.23 [325]~P6(x3254,x3255)+~P6(x3253,x3255)+~P6(a1,x3254)+~P6(a1,x3253)+~E(f4(x3251,f11(x3251,x3252,x3255),f9(x3251,x3252,x3255)),f4(x3251,f9(x3251,x3252,x3255),f11(x3251,x3252,x3255)))+E(f4(f52(x3251,x3252),x3253,x3254),f4(f52(x3251,x3252),x3254,x3253))+P6(a1,f12(x3251,x3252,x3255))
% 25.11/25.23 [326]~P6(x3264,x3265)+~P6(x3263,x3265)+~P6(a1,x3264)+~P6(a1,x3263)+P6(f31(x3261,x3262,x3265),x3265)+~E(f4(x3262,f8(x3261,x3262,x3265),f34(x3261,x3262,x3265)),f4(x3262,f34(x3261,x3262,x3265),f8(x3261,x3262,x3265)))+E(f4(f50(x3261,x3262),x3263,x3264),f4(f50(x3261,x3262),x3264,x3263))
% 25.11/25.23 [327]~P6(x3274,x3275)+~P6(x3273,x3275)+~P6(a1,x3274)+~P6(a1,x3273)+P6(f35(x3271,x3272,x3275),x3275)+~E(f4(x3272,f8(x3271,x3272,x3275),f34(x3271,x3272,x3275)),f4(x3272,f34(x3271,x3272,x3275),f8(x3271,x3272,x3275)))+E(f4(f50(x3271,x3272),x3273,x3274),f4(f50(x3271,x3272),x3274,x3273))
% 25.11/25.23 [328]~P6(x3284,x3285)+~P6(x3283,x3285)+~P6(a1,x3284)+~P6(a1,x3283)+P6(f34(x3281,x3282,x3285),x3285)+~E(f4(x3281,f35(x3281,x3282,x3285),f31(x3281,x3282,x3285)),f4(x3281,f31(x3281,x3282,x3285),f35(x3281,x3282,x3285)))+E(f4(f50(x3281,x3282),x3283,x3284),f4(f50(x3281,x3282),x3284,x3283))
% 25.11/25.23 [329]~P6(x3294,x3295)+~P6(x3293,x3295)+~P6(a1,x3294)+~P6(a1,x3293)+P6(f8(x3291,x3292,x3295),x3295)+~E(f4(x3291,f35(x3291,x3292,x3295),f31(x3291,x3292,x3295)),f4(x3291,f31(x3291,x3292,x3295),f35(x3291,x3292,x3295)))+E(f4(f50(x3291,x3292),x3293,x3294),f4(f50(x3291,x3292),x3294,x3293))
% 25.11/25.23 [330]~P6(x3304,x3305)+~P6(x3303,x3305)+~P6(a1,x3304)+~P6(a1,x3303)+P6(f9(x3301,x3302,x3305),x3305)+~E(f4(x3302,f12(x3301,x3302,x3305),f10(x3301,x3302,x3305)),f4(x3302,f10(x3301,x3302,x3305),f12(x3301,x3302,x3305)))+E(f4(f52(x3301,x3302),x3303,x3304),f4(f52(x3301,x3302),x3304,x3303))
% 25.11/25.23 [331]~P6(x3314,x3315)+~P6(x3313,x3315)+~P6(a1,x3314)+~P6(a1,x3313)+P6(f11(x3311,x3312,x3315),x3315)+~E(f4(x3312,f12(x3311,x3312,x3315),f10(x3311,x3312,x3315)),f4(x3312,f10(x3311,x3312,x3315),f12(x3311,x3312,x3315)))+E(f4(f52(x3311,x3312),x3313,x3314),f4(f52(x3311,x3312),x3314,x3313))
% 25.11/25.23 [332]~P6(x3324,x3325)+~P6(x3323,x3325)+~P6(a1,x3324)+~P6(a1,x3323)+P6(f10(x3321,x3322,x3325),x3325)+~E(f4(x3321,f11(x3321,x3322,x3325),f9(x3321,x3322,x3325)),f4(x3321,f9(x3321,x3322,x3325),f11(x3321,x3322,x3325)))+E(f4(f52(x3321,x3322),x3323,x3324),f4(f52(x3321,x3322),x3324,x3323))
% 25.11/25.23 [333]~P6(x3334,x3335)+~P6(x3333,x3335)+~P6(a1,x3334)+~P6(a1,x3333)+P6(f12(x3331,x3332,x3335),x3335)+~E(f4(x3331,f11(x3331,x3332,x3335),f9(x3331,x3332,x3335)),f4(x3331,f9(x3331,x3332,x3335),f11(x3331,x3332,x3335)))+E(f4(f52(x3331,x3332),x3333,x3334),f4(f52(x3331,x3332),x3334,x3333))
% 25.11/25.23 [357]~P6(x3574,x3575)+~P6(x3573,x3575)+~P6(a1,x3574)+~P6(a1,x3573)+~E(f4(x3572,f8(x3571,x3572,x3575),f34(x3571,x3572,x3575)),f4(x3572,f34(x3571,x3572,x3575),f8(x3571,x3572,x3575)))+~E(f4(x3571,f35(x3571,x3572,x3575),f31(x3571,x3572,x3575)),f4(x3571,f31(x3571,x3572,x3575),f35(x3571,x3572,x3575)))+E(f4(f50(x3571,x3572),x3573,x3574),f4(f50(x3571,x3572),x3574,x3573))
% 25.11/25.23 [358]~P6(x3584,x3585)+~P6(x3583,x3585)+~P6(a1,x3584)+~P6(a1,x3583)+~E(f4(x3582,f12(x3581,x3582,x3585),f10(x3581,x3582,x3585)),f4(x3582,f10(x3581,x3582,x3585),f12(x3581,x3582,x3585)))+~E(f4(x3581,f11(x3581,x3582,x3585),f9(x3581,x3582,x3585)),f4(x3581,f9(x3581,x3582,x3585),f11(x3581,x3582,x3585)))+E(f4(f52(x3581,x3582),x3583,x3584),f4(f52(x3581,x3582),x3584,x3583))
% 25.11/25.23 [373]~P6(x3738,x3739)+~P6(x3737,x3739)+~P3(x3731,x3739,x37310,x3734)+~P6(a1,x3738)+~P6(a1,x3737)+P6(a1,f17(x3731,x3732,x3733,x3734,x3735,x3736,x3739))+E(f4(f50(x3731,f53(x3732,f53(f50(f53(x3733,f53(x3734,f57(x3733))),f53(x3735,f53(x3736,f57(x3735)))),f57(x3732)))),x3737,x3738),f4(f50(x3731,f53(x3732,f53(f50(f53(x3733,f53(x3734,f57(x3733))),f53(x3735,f53(x3736,f57(x3735)))),f57(x3732)))),x3738,x3737))
% 25.11/25.23 [374]~P6(x3748,x3749)+~P6(x3747,x3749)+~P3(x3741,x3749,x37410,x3744)+~P6(a1,x3748)+~P6(a1,x3747)+P6(a1,f20(x3741,x3742,x3743,x3744,x3745,x3746,x3749))+E(f4(f50(x3741,f53(x3742,f53(f50(f53(x3743,f53(x3744,f57(x3743))),f53(x3745,f53(x3746,f57(x3745)))),f57(x3742)))),x3747,x3748),f4(f50(x3741,f53(x3742,f53(f50(f53(x3743,f53(x3744,f57(x3743))),f53(x3745,f53(x3746,f57(x3745)))),f57(x3742)))),x3748,x3747))
% 25.11/25.23 [375]~P6(x3758,x3759)+~P6(x3757,x3759)+~P3(x3751,x3759,x37510,x3754)+~P6(a1,x3758)+~P6(a1,x3757)+P6(f17(x3751,x3752,x3753,x3754,x3755,x3756,x3759),x3759)+E(f4(f50(x3751,f53(x3752,f53(f50(f53(x3753,f53(x3754,f57(x3753))),f53(x3755,f53(x3756,f57(x3755)))),f57(x3752)))),x3757,x3758),f4(f50(x3751,f53(x3752,f53(f50(f53(x3753,f53(x3754,f57(x3753))),f53(x3755,f53(x3756,f57(x3755)))),f57(x3752)))),x3758,x3757))
% 25.11/25.23 [376]~P6(x3768,x3769)+~P6(x3767,x3769)+~P3(x3761,x3769,x37610,x3764)+~P6(a1,x3768)+~P6(a1,x3767)+P6(f20(x3761,x3762,x3763,x3764,x3765,x3766,x3769),x3769)+E(f4(f50(x3761,f53(x3762,f53(f50(f53(x3763,f53(x3764,f57(x3763))),f53(x3765,f53(x3766,f57(x3765)))),f57(x3762)))),x3767,x3768),f4(f50(x3761,f53(x3762,f53(f50(f53(x3763,f53(x3764,f57(x3763))),f53(x3765,f53(x3766,f57(x3765)))),f57(x3762)))),x3768,x3767))
% 25.11/25.23 [377]~P6(x3778,x3779)+~P6(x3777,x3779)+~P3(x3771,x3779,x37710,x3774)+~P6(a1,x3778)+~P6(a1,x3777)+~E(f4(x3776,f20(x3771,x3772,x3773,x3774,x3775,x3776,x3779),f17(x3771,x3772,x3773,x3774,x3775,x3776,x3779)),f4(x3776,f17(x3771,x3772,x3773,x3774,x3775,x3776,x3779),f20(x3771,x3772,x3773,x3774,x3775,x3776,x3779)))+E(f4(f50(x3771,f53(x3772,f53(f50(f53(x3773,f53(x3774,f57(x3773))),f53(x3775,f53(x3776,f57(x3775)))),f57(x3772)))),x3777,x3778),f4(f50(x3771,f53(x3772,f53(f50(f53(x3773,f53(x3774,f57(x3773))),f53(x3775,f53(x3776,f57(x3775)))),f57(x3772)))),x3778,x3777))
% 25.11/25.23 [242]E(x2421,a36)+E(x2421,a38)+E(x2421,a39)+E(x2421,a40)+E(x2421,a41)+~P6(x2421,a41)+~P6(a1,x2421)+E(x2421,a1)
% 25.11/25.23 [352]~P6(x3522,x3526)+~P6(x3525,x3526)+~P6(x3524,x3526)+~P6(a1,x3522)+~P6(a1,x3525)+~P6(a1,x3524)+E(f4(f54(x3521,x3522,x3522,x3523),x3524,x3525),f4(f54(x3521,x3522,x3522,x3523),x3525,x3524))+P6(a1,f32(x3521,x3526))
% 25.11/25.23 [353]~P6(x3532,x3536)+~P6(x3535,x3536)+~P6(x3534,x3536)+~P6(a1,x3532)+~P6(a1,x3535)+~P6(a1,x3534)+E(f4(f54(x3531,x3532,x3532,x3533),x3534,x3535),f4(f54(x3531,x3532,x3532,x3533),x3535,x3534))+P6(a1,f33(x3531,x3536))
% 25.11/25.23 [354]~P6(x3542,x3546)+~P6(x3545,x3546)+~P6(x3544,x3546)+~P6(a1,x3542)+~P6(a1,x3545)+~P6(a1,x3544)+P6(f32(x3541,x3546),x3546)+E(f4(f54(x3541,x3542,x3542,x3543),x3544,x3545),f4(f54(x3541,x3542,x3542,x3543),x3545,x3544))
% 25.11/25.23 [355]~P6(x3552,x3556)+~P6(x3555,x3556)+~P6(x3554,x3556)+~P6(a1,x3552)+~P6(a1,x3555)+~P6(a1,x3554)+P6(f33(x3551,x3556),x3556)+E(f4(f54(x3551,x3552,x3552,x3553),x3554,x3555),f4(f54(x3551,x3552,x3552,x3553),x3555,x3554))
% 25.11/25.23 [356]~P6(x3562,x3566)+~P6(x3565,x3566)+~P6(x3564,x3566)+~P6(a1,x3562)+~P6(a1,x3565)+~P6(a1,x3564)+E(f4(f54(x3561,x3562,x3562,x3563),x3564,x3565),f4(f54(x3561,x3562,x3562,x3563),x3565,x3564))+~E(f4(x3561,f33(x3561,x3566),f32(x3561,x3566)),f4(x3561,f32(x3561,x3566),f33(x3561,x3566)))
% 25.11/25.23 %EqnAxiom
% 25.11/25.23 [1]E(x11,x11)
% 25.11/25.23 [2]E(x22,x21)+~E(x21,x22)
% 25.11/25.23 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 25.11/25.23 [4]~E(x41,x42)+E(f37(x41,x43),f37(x42,x43))
% 25.11/25.23 [5]~E(x51,x52)+E(f37(x53,x51),f37(x53,x52))
% 25.11/25.23 [6]~E(x61,x62)+E(f4(x61,x63,x64),f4(x62,x63,x64))
% 25.11/25.23 [7]~E(x71,x72)+E(f4(x73,x71,x74),f4(x73,x72,x74))
% 25.11/25.23 [8]~E(x81,x82)+E(f4(x83,x84,x81),f4(x83,x84,x82))
% 25.11/25.23 [9]~E(x91,x92)+E(f20(x91,x93,x94,x95,x96,x97,x98),f20(x92,x93,x94,x95,x96,x97,x98))
% 25.11/25.23 [10]~E(x101,x102)+E(f20(x103,x101,x104,x105,x106,x107,x108),f20(x103,x102,x104,x105,x106,x107,x108))
% 25.11/25.23 [11]~E(x111,x112)+E(f20(x113,x114,x111,x115,x116,x117,x118),f20(x113,x114,x112,x115,x116,x117,x118))
% 25.11/25.23 [12]~E(x121,x122)+E(f20(x123,x124,x125,x121,x126,x127,x128),f20(x123,x124,x125,x122,x126,x127,x128))
% 25.11/25.23 [13]~E(x131,x132)+E(f20(x133,x134,x135,x136,x131,x137,x138),f20(x133,x134,x135,x136,x132,x137,x138))
% 25.11/25.23 [14]~E(x141,x142)+E(f20(x143,x144,x145,x146,x147,x141,x148),f20(x143,x144,x145,x146,x147,x142,x148))
% 25.11/25.23 [15]~E(x151,x152)+E(f20(x153,x154,x155,x156,x157,x158,x151),f20(x153,x154,x155,x156,x157,x158,x152))
% 25.11/25.23 [16]~E(x161,x162)+E(f17(x161,x163,x164,x165,x166,x167,x168),f17(x162,x163,x164,x165,x166,x167,x168))
% 25.11/25.23 [17]~E(x171,x172)+E(f17(x173,x171,x174,x175,x176,x177,x178),f17(x173,x172,x174,x175,x176,x177,x178))
% 25.11/25.23 [18]~E(x181,x182)+E(f17(x183,x184,x181,x185,x186,x187,x188),f17(x183,x184,x182,x185,x186,x187,x188))
% 25.11/25.23 [19]~E(x191,x192)+E(f17(x193,x194,x195,x191,x196,x197,x198),f17(x193,x194,x195,x192,x196,x197,x198))
% 25.11/25.23 [20]~E(x201,x202)+E(f17(x203,x204,x205,x206,x201,x207,x208),f17(x203,x204,x205,x206,x202,x207,x208))
% 25.11/25.23 [21]~E(x211,x212)+E(f17(x213,x214,x215,x216,x217,x211,x218),f17(x213,x214,x215,x216,x217,x212,x218))
% 25.11/25.23 [22]~E(x221,x222)+E(f17(x223,x224,x225,x226,x227,x228,x221),f17(x223,x224,x225,x226,x227,x228,x222))
% 25.11/25.23 [23]~E(x231,x232)+E(f57(x231),f57(x232))
% 25.11/25.23 [24]~E(x241,x242)+E(f14(x241,x243,x244),f14(x242,x243,x244))
% 25.11/25.23 [25]~E(x251,x252)+E(f14(x253,x251,x254),f14(x253,x252,x254))
% 25.11/25.23 [26]~E(x261,x262)+E(f14(x263,x264,x261),f14(x263,x264,x262))
% 25.11/25.23 [27]~E(x271,x272)+E(f22(x271,x273),f22(x272,x273))
% 25.11/25.23 [28]~E(x281,x282)+E(f22(x283,x281),f22(x283,x282))
% 25.11/25.23 [29]~E(x291,x292)+E(f15(x291,x293,x294),f15(x292,x293,x294))
% 25.11/25.23 [30]~E(x301,x302)+E(f15(x303,x301,x304),f15(x303,x302,x304))
% 25.11/25.23 [31]~E(x311,x312)+E(f15(x313,x314,x311),f15(x313,x314,x312))
% 25.11/25.23 [32]~E(x321,x322)+E(f53(x321,x323),f53(x322,x323))
% 25.11/25.23 [33]~E(x331,x332)+E(f53(x333,x331),f53(x333,x332))
% 25.11/25.23 [34]~E(x341,x342)+E(f52(x341,x343),f52(x342,x343))
% 25.11/25.23 [35]~E(x351,x352)+E(f52(x353,x351),f52(x353,x352))
% 25.11/25.23 [36]~E(x361,x362)+E(f50(x361,x363),f50(x362,x363))
% 25.11/25.23 [37]~E(x371,x372)+E(f50(x373,x371),f50(x373,x372))
% 25.11/25.23 [38]~E(x381,x382)+E(f31(x381,x383,x384),f31(x382,x383,x384))
% 25.11/25.23 [39]~E(x391,x392)+E(f31(x393,x391,x394),f31(x393,x392,x394))
% 25.11/25.23 [40]~E(x401,x402)+E(f31(x403,x404,x401),f31(x403,x404,x402))
% 25.11/25.23 [41]~E(x411,x412)+E(f35(x411,x413,x414),f35(x412,x413,x414))
% 25.11/25.23 [42]~E(x421,x422)+E(f35(x423,x421,x424),f35(x423,x422,x424))
% 25.11/25.23 [43]~E(x431,x432)+E(f35(x433,x434,x431),f35(x433,x434,x432))
% 25.11/25.23 [44]~E(x441,x442)+E(f8(x441,x443,x444),f8(x442,x443,x444))
% 25.11/25.23 [45]~E(x451,x452)+E(f8(x453,x451,x454),f8(x453,x452,x454))
% 25.11/25.23 [46]~E(x461,x462)+E(f8(x463,x464,x461),f8(x463,x464,x462))
% 25.11/25.23 [47]~E(x471,x472)+E(f28(x471),f28(x472))
% 25.11/25.23 [48]~E(x481,x482)+E(f25(x481,x483,x484,x485),f25(x482,x483,x484,x485))
% 25.11/25.23 [49]~E(x491,x492)+E(f25(x493,x491,x494,x495),f25(x493,x492,x494,x495))
% 25.11/25.23 [50]~E(x501,x502)+E(f25(x503,x504,x501,x505),f25(x503,x504,x502,x505))
% 25.11/25.23 [51]~E(x511,x512)+E(f25(x513,x514,x515,x511),f25(x513,x514,x515,x512))
% 25.11/25.23 [52]~E(x521,x522)+E(f26(x521,x523,x524,x525),f26(x522,x523,x524,x525))
% 25.11/25.23 [53]~E(x531,x532)+E(f26(x533,x531,x534,x535),f26(x533,x532,x534,x535))
% 25.11/25.23 [54]~E(x541,x542)+E(f26(x543,x544,x541,x545),f26(x543,x544,x542,x545))
% 25.11/25.23 [55]~E(x551,x552)+E(f26(x553,x554,x555,x551),f26(x553,x554,x555,x552))
% 25.11/25.23 [56]~E(x561,x562)+E(f44(x561,x563,x564),f44(x562,x563,x564))
% 25.11/25.23 [57]~E(x571,x572)+E(f44(x573,x571,x574),f44(x573,x572,x574))
% 25.11/25.23 [58]~E(x581,x582)+E(f44(x583,x584,x581),f44(x583,x584,x582))
% 25.11/25.23 [59]~E(x591,x592)+E(f54(x591,x593,x594,x595),f54(x592,x593,x594,x595))
% 25.11/25.23 [60]~E(x601,x602)+E(f54(x603,x601,x604,x605),f54(x603,x602,x604,x605))
% 25.11/25.23 [61]~E(x611,x612)+E(f54(x613,x614,x611,x615),f54(x613,x614,x612,x615))
% 25.11/25.23 [62]~E(x621,x622)+E(f54(x623,x624,x625,x621),f54(x623,x624,x625,x622))
% 25.11/25.23 [63]~E(x631,x632)+E(f24(x631,x633,x634,x635),f24(x632,x633,x634,x635))
% 25.11/25.24 [64]~E(x641,x642)+E(f24(x643,x641,x644,x645),f24(x643,x642,x644,x645))
% 25.11/25.24 [65]~E(x651,x652)+E(f24(x653,x654,x651,x655),f24(x653,x654,x652,x655))
% 25.11/25.24 [66]~E(x661,x662)+E(f24(x663,x664,x665,x661),f24(x663,x664,x665,x662))
% 25.11/25.24 [67]~E(x671,x672)+E(f10(x671,x673,x674),f10(x672,x673,x674))
% 25.11/25.24 [68]~E(x681,x682)+E(f10(x683,x681,x684),f10(x683,x682,x684))
% 25.11/25.24 [69]~E(x691,x692)+E(f10(x693,x694,x691),f10(x693,x694,x692))
% 25.11/25.24 [70]~E(x701,x702)+E(f27(x701,x703,x704,x705),f27(x702,x703,x704,x705))
% 25.11/25.24 [71]~E(x711,x712)+E(f27(x713,x711,x714,x715),f27(x713,x712,x714,x715))
% 25.11/25.24 [72]~E(x721,x722)+E(f27(x723,x724,x721,x725),f27(x723,x724,x722,x725))
% 25.11/25.24 [73]~E(x731,x732)+E(f27(x733,x734,x735,x731),f27(x733,x734,x735,x732))
% 25.11/25.24 [74]~E(x741,x742)+E(f12(x741,x743,x744),f12(x742,x743,x744))
% 25.11/25.24 [75]~E(x751,x752)+E(f12(x753,x751,x754),f12(x753,x752,x754))
% 25.11/25.24 [76]~E(x761,x762)+E(f12(x763,x764,x761),f12(x763,x764,x762))
% 25.11/25.24 [77]~E(x771,x772)+E(f9(x771,x773,x774),f9(x772,x773,x774))
% 25.11/25.24 [78]~E(x781,x782)+E(f9(x783,x781,x784),f9(x783,x782,x784))
% 25.11/25.24 [79]~E(x791,x792)+E(f9(x793,x794,x791),f9(x793,x794,x792))
% 25.11/25.24 [80]~E(x801,x802)+E(f29(x801,x803),f29(x802,x803))
% 25.11/25.24 [81]~E(x811,x812)+E(f29(x813,x811),f29(x813,x812))
% 25.11/25.24 [82]~E(x821,x822)+E(f34(x821,x823,x824),f34(x822,x823,x824))
% 25.11/25.24 [83]~E(x831,x832)+E(f34(x833,x831,x834),f34(x833,x832,x834))
% 25.11/25.24 [84]~E(x841,x842)+E(f34(x843,x844,x841),f34(x843,x844,x842))
% 25.11/25.24 [85]~E(x851,x852)+E(f33(x851,x853),f33(x852,x853))
% 25.11/25.24 [86]~E(x861,x862)+E(f33(x863,x861),f33(x863,x862))
% 25.11/25.24 [87]~E(x871,x872)+E(f51(x871,x873,x874),f51(x872,x873,x874))
% 25.11/25.24 [88]~E(x881,x882)+E(f51(x883,x881,x884),f51(x883,x882,x884))
% 25.11/25.24 [89]~E(x891,x892)+E(f51(x893,x894,x891),f51(x893,x894,x892))
% 25.11/25.24 [90]~E(x901,x902)+E(f23(x901,x903),f23(x902,x903))
% 25.11/25.24 [91]~E(x911,x912)+E(f23(x913,x911),f23(x913,x912))
% 25.11/25.24 [92]~E(x921,x922)+E(f11(x921,x923,x924),f11(x922,x923,x924))
% 25.11/25.24 [93]~E(x931,x932)+E(f11(x933,x931,x934),f11(x933,x932,x934))
% 25.11/25.24 [94]~E(x941,x942)+E(f11(x943,x944,x941),f11(x943,x944,x942))
% 25.11/25.24 [95]~E(x951,x952)+E(f3(x951,x953),f3(x952,x953))
% 25.11/25.24 [96]~E(x961,x962)+E(f3(x963,x961),f3(x963,x962))
% 25.11/25.24 [97]~E(x971,x972)+E(f30(x971,x973),f30(x972,x973))
% 25.11/25.24 [98]~E(x981,x982)+E(f30(x983,x981),f30(x983,x982))
% 25.11/25.24 [99]~E(x991,x992)+E(f21(x991,x993,x994,x995,x996,x997),f21(x992,x993,x994,x995,x996,x997))
% 25.11/25.24 [100]~E(x1001,x1002)+E(f21(x1003,x1001,x1004,x1005,x1006,x1007),f21(x1003,x1002,x1004,x1005,x1006,x1007))
% 25.11/25.24 [101]~E(x1011,x1012)+E(f21(x1013,x1014,x1011,x1015,x1016,x1017),f21(x1013,x1014,x1012,x1015,x1016,x1017))
% 25.11/25.24 [102]~E(x1021,x1022)+E(f21(x1023,x1024,x1025,x1021,x1026,x1027),f21(x1023,x1024,x1025,x1022,x1026,x1027))
% 25.11/25.24 [103]~E(x1031,x1032)+E(f21(x1033,x1034,x1035,x1036,x1031,x1037),f21(x1033,x1034,x1035,x1036,x1032,x1037))
% 25.11/25.24 [104]~E(x1041,x1042)+E(f21(x1043,x1044,x1045,x1046,x1047,x1041),f21(x1043,x1044,x1045,x1046,x1047,x1042))
% 25.11/25.24 [105]~E(x1051,x1052)+E(f19(x1051,x1053,x1054,x1055,x1056,x1057),f19(x1052,x1053,x1054,x1055,x1056,x1057))
% 25.11/25.24 [106]~E(x1061,x1062)+E(f19(x1063,x1061,x1064,x1065,x1066,x1067),f19(x1063,x1062,x1064,x1065,x1066,x1067))
% 25.11/25.24 [107]~E(x1071,x1072)+E(f19(x1073,x1074,x1071,x1075,x1076,x1077),f19(x1073,x1074,x1072,x1075,x1076,x1077))
% 25.11/25.24 [108]~E(x1081,x1082)+E(f19(x1083,x1084,x1085,x1081,x1086,x1087),f19(x1083,x1084,x1085,x1082,x1086,x1087))
% 25.11/25.24 [109]~E(x1091,x1092)+E(f19(x1093,x1094,x1095,x1096,x1091,x1097),f19(x1093,x1094,x1095,x1096,x1092,x1097))
% 25.11/25.24 [110]~E(x1101,x1102)+E(f19(x1103,x1104,x1105,x1106,x1107,x1101),f19(x1103,x1104,x1105,x1106,x1107,x1102))
% 25.11/25.24 [111]~E(x1111,x1112)+E(f7(x1111,x1113),f7(x1112,x1113))
% 25.11/25.24 [112]~E(x1121,x1122)+E(f7(x1123,x1121),f7(x1123,x1122))
% 25.11/25.24 [113]~E(x1131,x1132)+E(f13(x1131,x1133,x1134),f13(x1132,x1133,x1134))
% 25.11/25.24 [114]~E(x1141,x1142)+E(f13(x1143,x1141,x1144),f13(x1143,x1142,x1144))
% 25.11/25.24 [115]~E(x1151,x1152)+E(f13(x1153,x1154,x1151),f13(x1153,x1154,x1152))
% 25.11/25.24 [116]~E(x1161,x1162)+E(f16(x1161,x1163,x1164),f16(x1162,x1163,x1164))
% 25.11/25.24 [117]~E(x1171,x1172)+E(f16(x1173,x1171,x1174),f16(x1173,x1172,x1174))
% 25.11/25.24 [118]~E(x1181,x1182)+E(f16(x1183,x1184,x1181),f16(x1183,x1184,x1182))
% 25.11/25.24 [119]~E(x1191,x1192)+E(f6(x1191,x1193),f6(x1192,x1193))
% 25.11/25.24 [120]~E(x1201,x1202)+E(f6(x1203,x1201),f6(x1203,x1202))
% 25.11/25.24 [121]~E(x1211,x1212)+E(f32(x1211,x1213),f32(x1212,x1213))
% 25.11/25.24 [122]~E(x1221,x1222)+E(f32(x1223,x1221),f32(x1223,x1222))
% 25.11/25.24 [123]~E(x1231,x1232)+E(f18(x1231,x1233,x1234,x1235),f18(x1232,x1233,x1234,x1235))
% 25.11/25.24 [124]~E(x1241,x1242)+E(f18(x1243,x1241,x1244,x1245),f18(x1243,x1242,x1244,x1245))
% 25.11/25.24 [125]~E(x1251,x1252)+E(f18(x1253,x1254,x1251,x1255),f18(x1253,x1254,x1252,x1255))
% 25.11/25.24 [126]~E(x1261,x1262)+E(f18(x1263,x1264,x1265,x1261),f18(x1263,x1264,x1265,x1262))
% 25.11/25.24 [127]~E(x1271,x1272)+E(f49(x1271,x1273,x1274),f49(x1272,x1273,x1274))
% 25.11/25.24 [128]~E(x1281,x1282)+E(f49(x1283,x1281,x1284),f49(x1283,x1282,x1284))
% 25.11/25.24 [129]~E(x1291,x1292)+E(f49(x1293,x1294,x1291),f49(x1293,x1294,x1292))
% 25.11/25.24 [130]~E(x1301,x1302)+E(f48(x1301,x1303),f48(x1302,x1303))
% 25.11/25.24 [131]~E(x1311,x1312)+E(f48(x1313,x1311),f48(x1313,x1312))
% 25.11/25.24 [132]~E(x1321,x1322)+E(f58(x1321,x1323),f58(x1322,x1323))
% 25.11/25.24 [133]~E(x1331,x1332)+E(f58(x1333,x1331),f58(x1333,x1332))
% 25.11/25.24 [134]~P1(x1341)+P1(x1342)+~E(x1341,x1342)
% 25.11/25.24 [135]~P2(x1351)+P2(x1352)+~E(x1351,x1352)
% 25.11/25.24 [136]P4(x1362,x1363)+~E(x1361,x1362)+~P4(x1361,x1363)
% 25.11/25.24 [137]P4(x1373,x1372)+~E(x1371,x1372)+~P4(x1373,x1371)
% 25.11/25.24 [138]P6(x1382,x1383)+~E(x1381,x1382)+~P6(x1381,x1383)
% 25.11/25.24 [139]P6(x1393,x1392)+~E(x1391,x1392)+~P6(x1393,x1391)
% 25.11/25.24 [140]P3(x1402,x1403,x1404,x1405)+~E(x1401,x1402)+~P3(x1401,x1403,x1404,x1405)
% 25.11/25.24 [141]P3(x1413,x1412,x1414,x1415)+~E(x1411,x1412)+~P3(x1413,x1411,x1414,x1415)
% 25.11/25.24 [142]P3(x1423,x1424,x1422,x1425)+~E(x1421,x1422)+~P3(x1423,x1424,x1421,x1425)
% 25.11/25.24 [143]P3(x1433,x1434,x1435,x1432)+~E(x1431,x1432)+~P3(x1433,x1434,x1435,x1431)
% 25.11/25.24 [144]P7(x1442,x1443)+~E(x1441,x1442)+~P7(x1441,x1443)
% 25.11/25.24 [145]P7(x1453,x1452)+~E(x1451,x1452)+~P7(x1453,x1451)
% 25.11/25.24 [146]P5(x1462,x1463)+~E(x1461,x1462)+~P5(x1461,x1463)
% 25.11/25.24 [147]P5(x1473,x1472)+~E(x1471,x1472)+~P5(x1473,x1471)
% 25.11/25.24
% 25.11/25.24 %-------------------------------------------
% 25.11/25.24 cnf(379,plain,
% 25.11/25.24 (~P6(f37(x3791,a36),x3791)),
% 25.11/25.24 inference(scs_inference,[],[205,251])).
% 25.11/25.24 cnf(380,plain,
% 25.11/25.24 (~P4(x3801,x3801)),
% 25.11/25.24 inference(rename_variables,[],[205])).
% 25.11/25.24 cnf(382,plain,
% 25.11/25.24 (E(f37(x3821,a36),f37(a36,x3821))),
% 25.11/25.24 inference(scs_inference,[],[205,183,251,2])).
% 25.11/25.24 cnf(383,plain,
% 25.11/25.24 (~P7(x3831,x3831)),
% 25.11/25.24 inference(scs_inference,[],[205,380,183,251,2,231])).
% 25.11/25.24 cnf(385,plain,
% 25.11/25.24 (~P4(x3851,f37(x3851,a36))),
% 25.11/25.24 inference(scs_inference,[],[205,380,183,251,2,231,232])).
% 25.11/25.24 cnf(387,plain,
% 25.11/25.24 (~P5(x3871,f37(x3871,a36))),
% 25.11/25.24 inference(scs_inference,[],[205,380,183,251,2,231,232,233])).
% 25.11/25.24 cnf(389,plain,
% 25.11/25.24 (~P4(x3891,f37(f22(x3891,a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[205,380,183,251,2,231,232,233,249])).
% 25.11/25.24 cnf(391,plain,
% 25.11/25.24 (P4(x3911,f22(x3911,a36))),
% 25.11/25.24 inference(scs_inference,[],[182,205,380,183,251,2,231,232,233,249,253])).
% 25.11/25.24 cnf(392,plain,
% 25.11/25.24 (P6(x3921,x3921)),
% 25.11/25.24 inference(rename_variables,[],[182])).
% 25.11/25.24 cnf(394,plain,
% 25.11/25.24 (P6(f22(f37(x3941,a36),a36),x3941)),
% 25.11/25.24 inference(scs_inference,[],[182,205,380,183,251,2,231,232,233,249,253,255])).
% 25.11/25.24 cnf(396,plain,
% 25.11/25.24 (P6(a1,a38)),
% 25.11/25.24 inference(scs_inference,[],[180,181,182,205,380,183,251,2,231,232,233,249,253,255,248])).
% 25.11/25.24 cnf(401,plain,
% 25.11/25.24 (P6(x4011,x4011)),
% 25.11/25.24 inference(rename_variables,[],[182])).
% 25.11/25.24 cnf(404,plain,
% 25.11/25.24 (~E(f37(x4041,a36),x4041)),
% 25.11/25.24 inference(scs_inference,[],[180,181,204,182,392,401,205,380,187,183,202,251,2,231,232,233,249,253,255,248,3,138,139,136])).
% 25.11/25.24 cnf(405,plain,
% 25.11/25.24 (P4(f37(x4051,a36),x4051)),
% 25.11/25.24 inference(rename_variables,[],[187])).
% 25.11/25.24 cnf(406,plain,
% 25.11/25.24 (~E(x4061,f37(x4061,a36))),
% 25.11/25.24 inference(scs_inference,[],[180,181,204,182,392,401,205,380,187,405,183,202,251,2,231,232,233,249,253,255,248,3,138,139,136,137])).
% 25.11/25.24 cnf(408,plain,
% 25.11/25.24 (P4(f37(a1,a36),a43)),
% 25.11/25.24 inference(scs_inference,[],[180,181,204,182,392,401,205,380,187,405,183,152,202,251,2,231,232,233,249,253,255,248,3,138,139,136,137,247])).
% 25.11/25.24 cnf(417,plain,
% 25.11/25.24 (E(f3(a45,a1),a55)),
% 25.11/25.24 inference(scs_inference,[],[149,206])).
% 25.11/25.24 cnf(418,plain,
% 25.11/25.24 (E(f3(a45,a36),a55)),
% 25.11/25.24 inference(scs_inference,[],[149,207])).
% 25.11/25.24 cnf(419,plain,
% 25.11/25.24 (E(f3(a45,a38),a55)),
% 25.11/25.24 inference(scs_inference,[],[149,208])).
% 25.11/25.24 cnf(420,plain,
% 25.11/25.24 (E(f3(a46,a1),a55)),
% 25.11/25.24 inference(scs_inference,[],[149,209])).
% 25.11/25.24 cnf(421,plain,
% 25.11/25.24 (E(f3(a46,a36),a55)),
% 25.11/25.24 inference(scs_inference,[],[149,210])).
% 25.11/25.24 cnf(422,plain,
% 25.11/25.24 (E(f3(a46,a38),a55)),
% 25.11/25.24 inference(scs_inference,[],[149,211])).
% 25.11/25.24 cnf(423,plain,
% 25.11/25.24 (E(f3(a46,a39),a55)),
% 25.11/25.24 inference(scs_inference,[],[149,212])).
% 25.11/25.24 cnf(424,plain,
% 25.11/25.24 (E(f3(a46,a40),a55)),
% 25.11/25.24 inference(scs_inference,[],[149,213])).
% 25.11/25.24 cnf(425,plain,
% 25.11/25.24 (E(f3(a46,a41),a55)),
% 25.11/25.24 inference(scs_inference,[],[149,214])).
% 25.11/25.24 cnf(426,plain,
% 25.11/25.24 (E(f3(a59,a39),a55)),
% 25.11/25.24 inference(scs_inference,[],[149,215])).
% 25.11/25.24 cnf(427,plain,
% 25.11/25.24 (E(f3(a59,a40),a55)),
% 25.11/25.24 inference(scs_inference,[],[149,216])).
% 25.11/25.24 cnf(428,plain,
% 25.11/25.24 (E(f3(a59,a41),a55)),
% 25.11/25.24 inference(scs_inference,[],[149,217])).
% 25.11/25.24 cnf(429,plain,
% 25.11/25.24 (E(f3(a60,a1),a55)),
% 25.11/25.24 inference(scs_inference,[],[149,218])).
% 25.11/25.24 cnf(430,plain,
% 25.11/25.24 (E(f3(a60,a36),a55)),
% 25.11/25.24 inference(scs_inference,[],[149,219])).
% 25.11/25.24 cnf(431,plain,
% 25.11/25.24 (E(f3(a60,a38),a55)),
% 25.11/25.24 inference(scs_inference,[],[149,220])).
% 25.11/25.24 cnf(432,plain,
% 25.11/25.24 (E(f3(a60,a39),a55)),
% 25.11/25.24 inference(scs_inference,[],[149,221])).
% 25.11/25.24 cnf(433,plain,
% 25.11/25.24 (E(f3(a60,a40),a55)),
% 25.11/25.24 inference(scs_inference,[],[149,222])).
% 25.11/25.24 cnf(434,plain,
% 25.11/25.24 (E(f3(a60,a41),a55)),
% 25.11/25.24 inference(scs_inference,[],[149,223])).
% 25.11/25.24 cnf(435,plain,
% 25.11/25.24 (E(f3(a61,a1),a55)),
% 25.11/25.24 inference(scs_inference,[],[149,224])).
% 25.11/25.24 cnf(436,plain,
% 25.11/25.24 (E(f3(a61,a36),a55)),
% 25.11/25.24 inference(scs_inference,[],[149,225])).
% 25.11/25.24 cnf(437,plain,
% 25.11/25.24 (E(f3(a61,a38),a55)),
% 25.11/25.24 inference(scs_inference,[],[149,226])).
% 25.11/25.24 cnf(438,plain,
% 25.11/25.24 (E(f3(a61,a39),a55)),
% 25.11/25.24 inference(scs_inference,[],[149,227])).
% 25.11/25.24 cnf(439,plain,
% 25.11/25.24 (E(f3(a61,a40),a55)),
% 25.11/25.24 inference(scs_inference,[],[149,228])).
% 25.11/25.24 cnf(440,plain,
% 25.11/25.24 (E(f3(a61,a41),a55)),
% 25.11/25.24 inference(scs_inference,[],[149,229])).
% 25.11/25.24 cnf(441,plain,
% 25.11/25.24 (E(f4(a56,a1,a1),a55)),
% 25.11/25.24 inference(scs_inference,[],[149,243])).
% 25.11/25.24 cnf(442,plain,
% 25.11/25.24 (E(f4(a56,a36,a1),a55)),
% 25.11/25.24 inference(scs_inference,[],[149,244])).
% 25.11/25.24 cnf(443,plain,
% 25.11/25.24 (E(f4(a56,a38,a1),a55)),
% 25.11/25.24 inference(scs_inference,[],[149,245])).
% 25.11/25.24 cnf(446,plain,
% 25.11/25.24 (~P6(f37(f37(x4461,a36),a36),x4461)),
% 25.11/25.24 inference(scs_inference,[],[379,250])).
% 25.11/25.24 cnf(447,plain,
% 25.11/25.24 (~P6(f37(x4471,a36),x4471)),
% 25.11/25.24 inference(rename_variables,[],[379])).
% 25.11/25.24 cnf(449,plain,
% 25.11/25.24 (P4(x4491,f22(f37(f22(x4491,a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[379,394,250,253])).
% 25.11/25.24 cnf(450,plain,
% 25.11/25.24 (P6(f22(f37(x4501,a36),a36),x4501)),
% 25.11/25.24 inference(rename_variables,[],[394])).
% 25.11/25.24 cnf(452,plain,
% 25.11/25.24 (~P5(x4521,f37(f37(x4521,a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[379,394,250,253,233])).
% 25.11/25.24 cnf(456,plain,
% 25.11/25.24 (~P4(x4561,f37(f37(x4561,a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[379,394,408,250,253,233,255,232])).
% 25.11/25.24 cnf(458,plain,
% 25.11/25.24 (~P6(f37(f22(f37(x4581,a36),a36),a36),x4581)),
% 25.11/25.24 inference(scs_inference,[],[379,389,394,408,250,253,233,255,232,251])).
% 25.11/25.24 cnf(461,plain,
% 25.11/25.24 (~P4(x4611,f37(f37(f22(x4611,a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[379,389,394,408,250,253,233,255,232,251,249])).
% 25.11/25.24 cnf(465,plain,
% 25.11/25.24 (E(x4651,f3(f51(x4652,x4653,x4651),x4653))),
% 25.11/25.24 inference(scs_inference,[],[379,385,389,394,408,195,250,253,233,255,232,251,249,231,2])).
% 25.11/25.24 cnf(466,plain,
% 25.11/25.24 (~E(f3(x4661,a55),f37(f3(f51(x4661,f3(a45,a2),x4662),a55),a36))),
% 25.11/25.24 inference(scs_inference,[],[204,379,385,406,389,394,408,195,250,253,233,255,232,251,249,231,2,262])).
% 25.11/25.24 cnf(467,plain,
% 25.11/25.24 (~E(x4671,f37(x4671,a36))),
% 25.11/25.24 inference(rename_variables,[],[406])).
% 25.11/25.24 cnf(469,plain,
% 25.11/25.24 (P4(f37(a1,a36),f22(a43,a36))),
% 25.11/25.24 inference(scs_inference,[],[204,379,385,391,406,389,394,408,195,250,253,233,255,232,251,249,231,2,262,247])).
% 25.11/25.24 cnf(470,plain,
% 25.11/25.24 (P4(x4701,f22(x4701,a36))),
% 25.11/25.24 inference(rename_variables,[],[391])).
% 25.11/25.24 cnf(472,plain,
% 25.11/25.24 (~E(x4721,f22(x4721,a36))),
% 25.11/25.24 inference(scs_inference,[],[204,379,385,391,470,406,389,394,408,195,205,250,253,233,255,232,251,249,231,2,262,247,136])).
% 25.11/25.24 cnf(474,plain,
% 25.11/25.24 (P6(a2,f3(f51(x4741,x4742,a38),x4742))),
% 25.11/25.24 inference(scs_inference,[],[181,204,379,385,391,470,406,389,394,408,195,205,250,253,233,255,232,251,249,231,2,262,247,136,139])).
% 25.11/25.24 cnf(477,plain,
% 25.11/25.24 (P6(f22(f37(a1,a36),a36),a2)),
% 25.11/25.24 inference(scs_inference,[],[181,204,180,379,447,385,391,470,406,389,394,450,408,195,205,250,253,233,255,232,251,249,231,2,262,247,136,139,138,248])).
% 25.11/25.24 cnf(484,plain,
% 25.11/25.24 (~E(f4(x4841,a55,f37(a36,x4842)),f37(f4(f54(x4841,f3(a45,a2),f37(x4842,a36),x4843),a55,f37(a36,x4842)),a36))),
% 25.11/25.24 inference(scs_inference,[],[181,204,180,379,447,382,404,385,391,470,406,467,389,394,450,408,195,205,250,253,233,255,232,251,249,231,2,262,247,136,139,138,248,3,137,314])).
% 25.11/25.24 cnf(487,plain,
% 25.11/25.24 (~E(f37(a36,x4871),x4871)),
% 25.11/25.24 inference(scs_inference,[],[181,204,180,379,447,382,404,385,391,470,406,467,389,394,450,408,195,205,250,253,233,255,232,251,249,231,2,262,247,136,139,138,248,3,137,314,4])).
% 25.11/25.24 cnf(488,plain,
% 25.11/25.24 (~P6(f22(f37(f37(x4881,a36),a36),a36),x4881)),
% 25.11/25.24 inference(scs_inference,[],[181,204,180,379,447,382,404,385,391,470,406,467,389,394,450,408,195,205,250,253,233,255,232,251,249,231,2,262,247,136,139,138,248,3,137,314,4,257])).
% 25.11/25.24 cnf(498,plain,
% 25.11/25.24 (~P4(x4981,f37(f22(f37(x4981,a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[458,232])).
% 25.11/25.24 cnf(500,plain,
% 25.11/25.24 (~P6(f37(f37(f37(x5001,a36),a36),a36),x5001)),
% 25.11/25.24 inference(scs_inference,[],[446,458,232,250])).
% 25.11/25.24 cnf(501,plain,
% 25.11/25.24 (~P6(f37(f37(x5011,a36),a36),x5011)),
% 25.11/25.24 inference(rename_variables,[],[446])).
% 25.11/25.24 cnf(504,plain,
% 25.11/25.24 (P4(x5041,f22(f37(f22(x5041,a36),a36),a36))),
% 25.11/25.24 inference(rename_variables,[],[449])).
% 25.11/25.24 cnf(506,plain,
% 25.11/25.24 (~P4(x5061,f37(f22(f37(f22(x5061,a36),a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[446,458,449,232,250,255,249])).
% 25.11/25.24 cnf(507,plain,
% 25.11/25.24 (~P6(f37(f22(f37(x5071,a36),a36),a36),x5071)),
% 25.11/25.24 inference(rename_variables,[],[458])).
% 25.11/25.24 cnf(509,plain,
% 25.11/25.24 (P4(x5091,f22(f37(f22(f37(f22(x5091,a36),a36),a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[446,458,449,232,250,255,249,253])).
% 25.11/25.24 cnf(511,plain,
% 25.11/25.24 (~P5(x5111,f37(f22(f37(x5111,a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[446,458,507,449,232,250,255,249,253,233])).
% 25.11/25.24 cnf(515,plain,
% 25.11/25.24 (~P6(f37(f37(f22(f37(x5151,a36),a36),a36),a36),x5151)),
% 25.11/25.24 inference(scs_inference,[],[446,458,507,456,449,461,232,250,255,249,253,233,231,251])).
% 25.11/25.24 cnf(518,plain,
% 25.11/25.24 (E(a55,f3(a45,a1))),
% 25.11/25.24 inference(scs_inference,[],[446,458,507,417,456,449,461,232,250,255,249,253,233,231,251,2])).
% 25.11/25.24 cnf(519,plain,
% 25.11/25.24 (~E(f3(x5191,a55),f37(f3(f51(f51(x5191,f3(a45,a2),x5192),f3(a45,a2),x5193),a55),a36))),
% 25.11/25.24 inference(scs_inference,[],[204,446,458,507,466,417,456,449,461,232,250,255,249,253,233,231,251,2,262])).
% 25.11/25.24 cnf(522,plain,
% 25.11/25.24 (P4(f37(a1,a36),f22(f37(f22(f22(a43,a36),a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[204,446,458,507,466,417,456,449,504,461,469,232,250,255,249,253,233,231,251,2,262,247])).
% 25.11/25.24 cnf(523,plain,
% 25.11/25.24 (P4(x5231,f22(f37(f22(x5231,a36),a36),a36))),
% 25.11/25.24 inference(rename_variables,[],[449])).
% 25.11/25.24 cnf(525,plain,
% 25.11/25.24 (P6(a1,f3(f51(x5251,x5252,a2),x5252))),
% 25.11/25.24 inference(scs_inference,[],[204,180,465,446,458,507,466,417,456,449,504,461,469,232,250,255,249,253,233,231,251,2,262,247,139])).
% 25.11/25.24 cnf(526,plain,
% 25.11/25.24 (E(x5261,f3(f51(x5262,x5263,x5261),x5263))),
% 25.11/25.24 inference(rename_variables,[],[465])).
% 25.11/25.24 cnf(527,plain,
% 25.11/25.24 (P6(a1,f3(f51(x5271,x5272,a38),x5272))),
% 25.11/25.24 inference(scs_inference,[],[204,180,465,446,458,507,466,474,417,456,449,504,461,469,232,250,255,249,253,233,231,251,2,262,247,139,248])).
% 25.11/25.24 cnf(529,plain,
% 25.11/25.24 (~E(x5291,f22(f37(f22(x5291,a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[204,180,465,446,458,507,466,474,417,456,449,504,523,461,469,205,232,250,255,249,253,233,231,251,2,262,247,139,248,136])).
% 25.11/25.24 cnf(532,plain,
% 25.11/25.24 (E(x5321,f3(f51(x5322,x5323,x5321),x5323))),
% 25.11/25.24 inference(rename_variables,[],[465])).
% 25.11/25.24 cnf(533,plain,
% 25.11/25.24 (~E(f37(a36,f3(f51(x5331,x5332,x5333),x5332)),x5333)),
% 25.11/25.24 inference(scs_inference,[],[149,204,180,465,526,532,487,446,458,507,466,474,417,456,449,504,523,461,469,205,232,250,255,249,253,233,231,251,2,262,247,139,248,136,135,3])).
% 25.11/25.24 cnf(539,plain,
% 25.11/25.24 (P1(f3(f51(x5391,x5392,a5000),x5392))),
% 25.11/25.24 inference(scs_inference,[],[149,204,181,180,465,526,532,487,446,501,458,507,466,474,417,385,456,449,504,523,461,469,148,205,232,250,255,249,253,233,231,251,2,262,247,139,248,136,135,3,138,137,134])).
% 25.11/25.24 cnf(541,plain,
% 25.11/25.24 (~E(f4(x5411,a55,f37(a36,x5412)),f37(f4(f54(f54(x5411,f3(a45,a2),f37(x5412,a36),x5413),f3(a45,a2),f37(x5412,a36),x5414),a55,f37(a36,x5412)),a36))),
% 25.11/25.24 inference(scs_inference,[],[149,204,181,180,465,526,532,487,446,501,458,507,484,466,474,417,382,385,456,449,504,523,461,469,148,205,232,250,255,249,253,233,231,251,2,262,247,139,248,136,135,3,138,137,134,314])).
% 25.11/25.24 cnf(544,plain,
% 25.11/25.24 (~E(x5441,f37(f22(f22(x5441,a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[149,204,181,180,465,526,532,487,446,501,458,507,484,466,474,417,382,385,456,449,504,523,461,469,148,205,232,250,255,249,253,233,231,251,2,262,247,139,248,136,135,3,138,137,134,314,27])).
% 25.11/25.24 cnf(545,plain,
% 25.11/25.24 (~P6(f37(f22(f37(f37(x5451,a36),a36),a36),a36),x5451)),
% 25.11/25.24 inference(scs_inference,[],[149,204,181,180,465,526,532,487,446,501,458,507,484,466,474,417,382,385,456,449,504,523,461,469,148,205,232,250,255,249,253,233,231,251,2,262,247,139,248,136,135,3,138,137,134,314,27,257])).
% 25.11/25.24 cnf(547,plain,
% 25.11/25.24 (~E(x5471,f22(f22(f37(x5471,a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[149,204,181,180,465,526,532,487,446,501,458,507,484,466,474,417,382,385,456,449,504,523,461,469,148,205,232,250,255,249,253,233,231,251,2,262,247,139,248,136,135,3,138,137,134,314,27,257,4])).
% 25.11/25.24 cnf(552,plain,
% 25.11/25.24 (E(a38,a1)+~P6(a38,a1)),
% 25.11/25.24 inference(scs_inference,[],[149,204,181,180,465,526,532,487,446,501,458,507,484,466,396,474,417,382,385,456,449,504,523,461,469,148,205,232,250,255,249,253,233,231,251,2,262,247,139,248,136,135,3,138,137,134,314,27,257,4,236,230,237])).
% 25.11/25.24 cnf(556,plain,
% 25.11/25.24 (~E(f22(f37(f22(f37(f22(x5561,a36),a36),a36),a36),a36),x5561)),
% 25.11/25.24 inference(scs_inference,[],[509,383,234,144])).
% 25.11/25.24 cnf(558,plain,
% 25.11/25.24 (~E(f37(a36,f3(f51(x5581,x5582,x5583),x5582)),x5583)),
% 25.11/25.24 inference(rename_variables,[],[533])).
% 25.11/25.24 cnf(563,plain,
% 25.11/25.24 (~P4(x5631,f22(f37(f37(f22(x5631,a36),a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[533,488,498,556,5,27,231,249])).
% 25.11/25.24 cnf(564,plain,
% 25.11/25.24 (~P6(f22(f37(f37(x5641,a36),a36),a36),x5641)),
% 25.11/25.24 inference(rename_variables,[],[488])).
% 25.11/25.24 cnf(566,plain,
% 25.11/25.24 (~P4(x5661,f22(f37(f37(x5661,a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[533,488,564,498,556,5,27,231,249,232])).
% 25.11/25.24 cnf(570,plain,
% 25.11/25.24 (~P6(f22(f37(f37(f37(x5701,a36),a36),a36),a36),x5701)),
% 25.11/25.24 inference(scs_inference,[],[533,488,564,498,556,522,5,27,231,249,232,255,250])).
% 25.11/25.24 cnf(571,plain,
% 25.11/25.24 (~P6(f22(f37(f37(x5711,a36),a36),a36),x5711)),
% 25.11/25.24 inference(rename_variables,[],[488])).
% 25.11/25.24 cnf(573,plain,
% 25.11/25.24 (~P5(x5731,f22(f37(f37(x5731,a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[533,488,564,571,498,556,522,5,27,231,249,232,255,250,233])).
% 25.11/25.24 cnf(575,plain,
% 25.11/25.24 (~P6(f37(f22(f37(f22(f37(x5751,a36),a36),a36),a36),a36),x5751)),
% 25.11/25.24 inference(scs_inference,[],[533,488,564,571,498,506,556,522,5,27,231,249,232,255,250,233,251])).
% 25.11/25.24 cnf(578,plain,
% 25.11/25.24 (~E(f22(f37(f22(f22(f37(x5781,a36),a36),a36),a36),a36),x5781)),
% 25.11/25.24 inference(scs_inference,[],[533,488,564,571,498,506,556,522,5,27,231,249,232,255,250,233,251,4])).
% 25.11/25.24 cnf(579,plain,
% 25.11/25.24 (E(a55,f3(a45,a36))),
% 25.11/25.24 inference(scs_inference,[],[533,488,564,571,418,498,506,556,522,5,27,231,249,232,255,250,233,251,4,2])).
% 25.11/25.24 cnf(581,plain,
% 25.11/25.24 (~E(x5811,f22(f22(f37(x5811,a36),a36),a36))),
% 25.11/25.24 inference(rename_variables,[],[547])).
% 25.11/25.24 cnf(583,plain,
% 25.11/25.24 (P4(f37(f37(a1,a36),a36),f22(f37(f22(f22(a43,a36),a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[204,533,488,564,571,547,418,498,506,556,522,187,5,27,231,249,232,255,250,233,251,4,2,262,247])).
% 25.11/25.24 cnf(586,plain,
% 25.11/25.24 (P6(a1,f3(f51(x5861,x5862,f3(f51(x5863,x5864,a2),x5864)),x5862))),
% 25.11/25.24 inference(scs_inference,[],[204,533,488,564,571,547,525,418,465,498,506,556,522,187,5,27,231,249,232,255,250,233,251,4,2,262,247,139])).
% 25.11/25.24 cnf(587,plain,
% 25.11/25.24 (E(x5871,f3(f51(x5872,x5873,x5871),x5873))),
% 25.11/25.24 inference(rename_variables,[],[465])).
% 25.11/25.24 cnf(592,plain,
% 25.11/25.24 (P1(f3(f51(x5921,x5922,f3(f51(x5923,x5924,a5000),x5924)),x5922))),
% 25.11/25.24 inference(scs_inference,[],[204,533,558,488,564,571,547,525,518,418,465,587,539,498,506,556,522,187,205,5,27,231,249,232,255,250,233,251,4,2,262,247,139,136,3,134])).
% 25.11/25.24 cnf(598,plain,
% 25.11/25.24 (~E(f4(x5981,a55,f3(a45,a1)),f22(f22(f37(f4(f54(x5981,f3(a45,a2),a55,x5982),a55,f3(a45,a1)),a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[181,204,533,558,488,564,571,547,581,525,518,418,465,587,539,385,498,506,556,522,187,205,5,27,231,249,232,255,250,233,251,4,2,262,247,139,136,3,134,138,137,314])).
% 25.11/25.24 cnf(602,plain,
% 25.11/25.24 (~P6(f22(f37(f22(f37(f37(x6021,a36),a36),a36),a36),a36),x6021)),
% 25.11/25.24 inference(scs_inference,[],[181,204,533,558,488,564,571,547,581,525,518,418,465,587,539,385,498,506,556,522,187,205,5,27,231,249,232,255,250,233,251,4,2,262,247,139,136,3,134,138,137,314,95,257])).
% 25.11/25.24 cnf(614,plain,
% 25.11/25.24 (~P4(x6141,f37(f37(f37(x6141,a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[500,232])).
% 25.11/25.24 cnf(616,plain,
% 25.11/25.24 (~P6(f37(f37(f37(f37(x6161,a36),a36),a36),a36),x6161)),
% 25.11/25.24 inference(scs_inference,[],[500,232,250])).
% 25.11/25.24 cnf(617,plain,
% 25.11/25.24 (~P6(f37(f37(f37(x6171,a36),a36),a36),x6171)),
% 25.11/25.24 inference(rename_variables,[],[500])).
% 25.11/25.24 cnf(619,plain,
% 25.11/25.24 (~P4(x6191,f37(f37(f37(f22(x6191,a36),a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[500,617,232,250,249])).
% 25.11/25.24 cnf(620,plain,
% 25.11/25.24 (~P6(f37(f37(f37(x6201,a36),a36),a36),x6201)),
% 25.11/25.24 inference(rename_variables,[],[500])).
% 25.11/25.24 cnf(624,plain,
% 25.11/25.24 (~P5(x6241,f37(f37(f37(x6241,a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[500,617,620,566,232,250,249,231,233])).
% 25.11/25.24 cnf(629,plain,
% 25.11/25.24 (~E(f22(f37(f22(f22(f37(x6291,a36),a36),a36),a36),a36),x6291)),
% 25.11/25.24 inference(rename_variables,[],[578])).
% 25.11/25.24 cnf(630,plain,
% 25.11/25.24 (~P6(f22(f37(f37(f22(f37(x6301,a36),a36),a36),a36),a36),x6301)),
% 25.11/25.24 inference(scs_inference,[],[500,617,620,578,566,563,583,232,250,249,231,233,255,27,251])).
% 25.11/25.24 cnf(633,plain,
% 25.11/25.24 (~E(f22(f22(f37(f22(f37(x6331,a36),a36),a36),a36),a36),x6331)),
% 25.11/25.24 inference(scs_inference,[],[500,617,620,578,566,563,583,232,250,249,231,233,255,27,251,4])).
% 25.11/25.24 cnf(634,plain,
% 25.11/25.24 (E(a55,f3(a45,a38))),
% 25.11/25.24 inference(scs_inference,[],[500,617,620,578,419,566,563,583,232,250,249,231,233,255,27,251,4,2])).
% 25.11/25.24 cnf(635,plain,
% 25.11/25.24 (~E(f3(x6351,a55),f37(f3(f51(f51(f51(x6351,f3(a45,a2),x6352),f3(a45,a2),x6353),f3(a45,a2),x6354),a55),a36))),
% 25.11/25.24 inference(scs_inference,[],[204,500,617,620,578,519,419,566,563,583,232,250,249,231,233,255,27,251,4,2,262])).
% 25.11/25.24 cnf(638,plain,
% 25.11/25.24 (P4(f37(f37(f37(a1,a36),a36),a36),f22(f37(f22(f22(a43,a36),a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[204,500,617,620,578,519,419,566,563,583,187,232,250,249,231,233,255,27,251,4,2,262,247])).
% 25.11/25.24 cnf(641,plain,
% 25.11/25.24 (P6(a2,f3(f51(x6411,x6412,f3(f51(x6413,x6414,a38),x6414)),x6412))),
% 25.11/25.24 inference(scs_inference,[],[204,474,500,617,620,578,519,419,465,566,563,583,187,232,250,249,231,233,255,27,251,4,2,262,247,139])).
% 25.11/25.24 cnf(642,plain,
% 25.11/25.24 (E(x6421,f3(f51(x6422,x6423,x6421),x6423))),
% 25.11/25.24 inference(rename_variables,[],[465])).
% 25.11/25.24 cnf(647,plain,
% 25.11/25.24 (P1(f3(f51(x6471,x6472,f3(f51(x6473,x6474,f3(f51(x6475,x6476,a5000),x6476)),x6474)),x6472))),
% 25.11/25.24 inference(scs_inference,[],[204,474,500,617,620,578,629,519,579,419,465,642,592,566,563,583,187,205,232,250,249,231,233,255,27,251,4,2,262,247,139,136,3,134])).
% 25.11/25.24 cnf(658,plain,
% 25.11/25.24 (P6(a1,f3(f51(x6581,x6582,f3(f51(x6583,x6584,a38),x6584)),x6582))),
% 25.11/25.24 inference(scs_inference,[],[181,180,204,474,500,617,620,578,629,541,519,579,419,465,642,382,592,385,566,563,583,187,205,232,250,249,231,233,255,27,251,4,2,262,247,139,136,3,134,137,138,314,236,248])).
% 25.11/25.24 cnf(668,plain,
% 25.11/25.24 (~P4(x6681,f37(f37(f22(f37(x6681,a36),a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[515,232])).
% 25.11/25.24 cnf(670,plain,
% 25.11/25.24 (~P5(x6701,f37(f37(f22(f37(x6701,a36),a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[515,232,233])).
% 25.11/25.24 cnf(674,plain,
% 25.11/25.24 (~P6(f37(f37(f22(f37(f37(x6741,a36),a36),a36),a36),a36),x6741)),
% 25.11/25.24 inference(scs_inference,[],[515,614,232,233,231,250])).
% 25.11/25.24 cnf(675,plain,
% 25.11/25.24 (~P6(f37(f37(f22(f37(x6751,a36),a36),a36),a36),x6751)),
% 25.11/25.24 inference(rename_variables,[],[515])).
% 25.11/25.24 cnf(677,plain,
% 25.11/25.24 (~P4(x6771,f37(f37(f22(f37(f22(x6771,a36),a36),a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[515,675,614,232,233,231,250,249])).
% 25.11/25.24 cnf(678,plain,
% 25.11/25.24 (~P6(f37(f37(f22(f37(x6781,a36),a36),a36),a36),x6781)),
% 25.11/25.24 inference(rename_variables,[],[515])).
% 25.11/25.24 cnf(680,plain,
% 25.11/25.24 (~P6(f37(f22(f37(f37(f37(x6801,a36),a36),a36),a36),a36),x6801)),
% 25.11/25.24 inference(scs_inference,[],[515,675,614,232,233,231,250,249,257])).
% 25.11/25.24 cnf(682,plain,
% 25.11/25.24 (P6(f22(f37(f22(f22(a43,a36),a36),a36),a36),f37(f37(a1,a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[515,675,614,638,232,233,231,250,249,257,255])).
% 25.11/25.24 cnf(684,plain,
% 25.11/25.24 (~P6(f37(f37(f37(f22(f37(x6841,a36),a36),a36),a36),a36),x6841)),
% 25.11/25.24 inference(scs_inference,[],[515,675,614,619,638,232,233,231,250,249,257,255,251])).
% 25.11/25.24 cnf(691,plain,
% 25.11/25.24 (P4(f37(f37(f37(f37(a1,a36),a36),a36),a36),f22(f37(f22(f22(a43,a36),a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[204,515,675,635,420,614,619,638,187,232,233,231,250,249,257,255,251,2,262,247])).
% 25.11/25.24 cnf(694,plain,
% 25.11/25.24 (P6(a2,f3(f51(x6941,x6942,f3(f51(x6943,x6944,f3(f51(x6945,x6946,a38),x6946)),x6944)),x6942))),
% 25.11/25.24 inference(scs_inference,[],[204,515,675,635,641,420,465,614,619,638,187,232,233,231,250,249,257,255,251,2,262,247,139])).
% 25.11/25.24 cnf(695,plain,
% 25.11/25.24 (E(x6951,f3(f51(x6952,x6953,x6951),x6953))),
% 25.11/25.24 inference(rename_variables,[],[465])).
% 25.11/25.24 cnf(711,plain,
% 25.11/25.24 (P6(a1,f3(f51(x7111,x7112,f3(f51(x7113,x7114,f3(f51(x7115,x7116,a38),x7116)),x7114)),x7112))),
% 25.11/25.24 inference(scs_inference,[],[181,180,204,515,675,678,487,635,598,641,634,420,465,695,518,647,385,614,619,638,187,205,232,233,231,250,249,257,255,251,2,262,247,139,136,3,134,137,138,314,236,248])).
% 25.11/25.24 cnf(713,plain,
% 25.11/25.24 (E(f3(f51(x7131,x7132,f3(f51(x7133,x7134,a38),x7134)),x7132),a1)+~P6(f3(f51(x7131,x7132,f3(f51(x7133,x7134,a38),x7134)),x7132),a1)),
% 25.11/25.24 inference(scs_inference,[],[181,180,204,515,675,678,487,635,598,641,658,634,420,465,695,518,647,385,614,619,638,187,205,232,233,231,250,249,257,255,251,2,262,247,139,136,3,134,137,138,314,236,248,237])).
% 25.11/25.24 cnf(721,plain,
% 25.11/25.24 (~P4(x7211,f37(f22(f37(f37(f22(x7211,a36),a36),a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[545,249])).
% 25.11/25.24 cnf(722,plain,
% 25.11/25.24 (~P6(f37(f22(f37(f37(x7221,a36),a36),a36),a36),x7221)),
% 25.11/25.24 inference(rename_variables,[],[545])).
% 25.11/25.24 cnf(724,plain,
% 25.11/25.24 (~P6(f37(f22(f37(f22(f37(f37(x7241,a36),a36),a36),a36),a36),a36),x7241)),
% 25.11/25.24 inference(scs_inference,[],[545,575,249,250])).
% 25.11/25.24 cnf(727,plain,
% 25.11/25.24 (~P4(x7271,f37(f22(f37(f37(x7271,a36),a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[545,722,575,249,250,232])).
% 25.11/25.24 cnf(729,plain,
% 25.11/25.24 (~P5(x7291,f37(f22(f37(f37(x7291,a36),a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[545,722,575,249,250,232,233])).
% 25.11/25.24 cnf(731,plain,
% 25.11/25.24 (P6(f22(f37(f22(f22(a43,a36),a36),a36),a36),f37(f37(f37(a1,a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[545,722,575,691,249,250,232,233,255])).
% 25.11/25.24 cnf(735,plain,
% 25.11/25.24 (~P6(f37(f37(f22(f37(f22(f37(x7351,a36),a36),a36),a36),a36),a36),x7351)),
% 25.11/25.24 inference(scs_inference,[],[545,722,575,668,677,691,249,250,232,233,255,231,251])).
% 25.11/25.24 cnf(738,plain,
% 25.11/25.24 (~P6(f22(f37(f37(f37(f37(x7381,a36),a36),a36),a36),a36),x7381)),
% 25.11/25.24 inference(scs_inference,[],[545,722,575,680,668,677,691,249,250,232,233,255,231,251,257])).
% 25.11/25.24 cnf(742,plain,
% 25.11/25.24 (P4(f37(f37(f37(f37(f37(a1,a36),a36),a36),a36),a36),f22(f37(f22(f22(a43,a36),a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[545,722,575,680,421,668,677,691,187,249,250,232,233,255,231,251,257,2,247])).
% 25.11/25.24 cnf(771,plain,
% 25.11/25.24 (P6(f22(f37(f22(f22(a43,a36),a36),a36),a36),f37(f37(f37(f37(a1,a36),a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[742,255])).
% 25.11/25.24 cnf(773,plain,
% 25.11/25.24 (~P4(x7731,f37(f22(f37(f22(f37(f22(x7731,a36),a36),a36),a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[575,742,255,249])).
% 25.11/25.24 cnf(774,plain,
% 25.11/25.24 (~P6(f37(f22(f37(f22(f37(x7741,a36),a36),a36),a36),a36),x7741)),
% 25.11/25.24 inference(rename_variables,[],[575])).
% 25.11/25.24 cnf(778,plain,
% 25.11/25.24 (~P6(f37(f37(f37(f37(f37(x7781,a36),a36),a36),a36),a36),x7781)),
% 25.11/25.24 inference(scs_inference,[],[575,774,616,742,255,249,233,250])).
% 25.11/25.24 cnf(781,plain,
% 25.11/25.24 (~P4(x7811,f37(f22(f37(f22(f37(x7811,a36),a36),a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[575,774,616,742,255,249,233,250,232])).
% 25.11/25.24 cnf(783,plain,
% 25.11/25.24 (~P6(f37(f22(f37(f37(f22(f37(x7831,a36),a36),a36),a36),a36),a36),x7831)),
% 25.11/25.24 inference(scs_inference,[],[575,774,616,721,742,255,249,233,250,232,251])).
% 25.11/25.24 cnf(788,plain,
% 25.11/25.24 (~P6(f22(f37(f22(f37(f37(f37(x7881,a36),a36),a36),a36),a36),a36),x7881)),
% 25.11/25.24 inference(scs_inference,[],[575,774,616,724,727,721,742,255,249,233,250,232,251,231,257])).
% 25.11/25.24 cnf(791,plain,
% 25.11/25.24 (E(a55,f3(a46,a38))),
% 25.11/25.24 inference(scs_inference,[],[575,774,616,724,422,727,721,742,255,249,233,250,232,251,231,257,2])).
% 25.11/25.24 cnf(792,plain,
% 25.11/25.24 (~E(f3(x7921,a55),f22(f3(f51(x7921,f3(a45,a2),x7922),a55),a36))),
% 25.11/25.24 inference(scs_inference,[],[204,575,774,616,724,422,472,727,721,742,255,249,233,250,232,251,231,257,2,262])).
% 25.11/25.24 cnf(795,plain,
% 25.11/25.24 (P4(f37(f37(f37(f37(f37(f37(a1,a36),a36),a36),a36),a36),a36),f22(f37(f22(f22(a43,a36),a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[204,575,774,616,724,422,472,727,721,742,187,255,249,233,250,232,251,231,257,2,262,247])).
% 25.11/25.24 cnf(798,plain,
% 25.11/25.24 (P6(f22(f37(a1,a36),a36),f3(f51(x7981,x7982,a2),x7982))),
% 25.11/25.24 inference(scs_inference,[],[204,575,774,616,724,477,422,465,472,727,721,742,187,255,249,233,250,232,251,231,257,2,262,247,139])).
% 25.11/25.24 cnf(819,plain,
% 25.11/25.24 (~P4(x8191,f22(f37(f37(f37(x8191,a36),a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[570,232])).
% 25.11/25.24 cnf(823,plain,
% 25.11/25.24 (~P6(f22(f37(f37(f22(f37(f37(x8231,a36),a36),a36),a36),a36),a36),x8231)),
% 25.11/25.24 inference(scs_inference,[],[570,630,795,232,255,250])).
% 25.11/25.24 cnf(828,plain,
% 25.11/25.24 (~P4(x8281,f22(f37(f37(f37(f22(x8281,a36),a36),a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[570,630,781,795,232,255,250,231,249])).
% 25.11/25.24 cnf(829,plain,
% 25.11/25.24 (~P6(f22(f37(f37(f37(x8291,a36),a36),a36),a36),x8291)),
% 25.11/25.24 inference(rename_variables,[],[570])).
% 25.11/25.24 cnf(833,plain,
% 25.11/25.24 (~P6(f37(f22(f37(f22(f37(f22(f37(x8331,a36),a36),a36),a36),a36),a36),a36),x8331)),
% 25.11/25.24 inference(scs_inference,[],[570,829,630,781,773,795,232,255,250,231,249,233,251])).
% 25.11/25.24 cnf(837,plain,
% 25.11/25.24 (P4(f37(f37(f37(f37(f37(f37(f37(a1,a36),a36),a36),a36),a36),a36),a36),f22(f37(f22(f22(a43,a36),a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[570,829,630,423,781,773,795,187,232,255,250,231,249,233,251,2,247])).
% 25.11/25.24 cnf(840,plain,
% 25.11/25.24 (~E(f3(x8401,a55),f22(f3(f51(f51(x8401,f3(a45,a2),x8402),f3(a45,a2),x8403),a55),a36))),
% 25.11/25.24 inference(scs_inference,[],[204,570,829,630,792,423,781,773,795,187,232,255,250,231,249,233,251,2,247,262])).
% 25.11/25.24 cnf(843,plain,
% 25.11/25.24 (P6(f22(f37(a1,a36),a36),f3(f51(x8431,x8432,f3(f51(x8433,x8434,a2),x8434)),x8432))),
% 25.11/25.24 inference(scs_inference,[],[204,798,570,829,630,792,423,465,781,773,795,187,232,255,250,231,249,233,251,2,247,262,139])).
% 25.11/25.24 cnf(856,plain,
% 25.11/25.24 (~P6(f22(f37(f22(f37(f22(f37(f37(x8561,a36),a36),a36),a36),a36),a36),a36),x8561)),
% 25.11/25.24 inference(scs_inference,[],[180,204,578,446,547,798,570,829,630,792,791,423,465,385,781,773,795,187,205,232,255,250,231,249,233,251,2,247,262,139,136,137,3,138,314,257])).
% 25.11/25.24 cnf(858,plain,
% 25.11/25.24 (E(f3(f51(x8581,x8582,a38),x8582),a1)+~P6(f3(f51(x8581,x8582,a38),x8582),a1)),
% 25.11/25.24 inference(scs_inference,[],[180,204,578,446,547,798,570,829,630,792,527,791,423,465,385,781,773,795,187,205,232,255,250,231,249,233,251,2,247,262,139,136,137,3,138,314,257,237])).
% 25.11/25.24 cnf(866,plain,
% 25.11/25.24 (~P4(x8661,f22(f37(f22(f37(f37(f22(x8661,a36),a36),a36),a36),a36),a36))),
% 25.11/25.24 inference(scs_inference,[],[602,249])).
% 25.11/25.24 cnf(867,plain,
% 25.11/25.24 (~P6(f22(f37(f22(f37(f37(x8671,a36),a36),a36),a36),a36),x8671)),
% 25.11/25.24 inference(rename_variables,[],[602])).
% 25.11/25.24 cnf(871,plain,
% 25.11/25.24 (~P4(x8711,f22(f37(f22(f37(f37(x8711,a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[602,867,819,249,231,232])).
% 25.11/25.25 cnf(873,plain,
% 25.11/25.25 (~P6(f22(f37(f37(f37(f22(f37(x8731,a36),a36),a36),a36),a36),a36),x8731)),
% 25.11/25.25 inference(scs_inference,[],[602,867,819,828,249,231,232,251])).
% 25.11/25.25 cnf(878,plain,
% 25.11/25.25 (~P6(f37(f37(f22(f37(f37(f37(x8781,a36),a36),a36),a36),a36),a36),x8781)),
% 25.11/25.25 inference(scs_inference,[],[602,867,674,819,828,837,249,231,232,251,255,250])).
% 25.11/25.25 cnf(883,plain,
% 25.11/25.25 (~P6(f37(f22(f37(f37(f37(f37(x8831,a36),a36),a36),a36),a36),a36),x8831)),
% 25.11/25.25 inference(scs_inference,[],[602,867,674,819,828,837,249,231,232,251,255,250,233,257])).
% 25.11/25.25 cnf(886,plain,
% 25.11/25.25 (~E(f3(x8861,a55),f22(f3(f51(f51(f51(x8861,f3(a45,a2),x8862),f3(a45,a2),x8863),f3(a45,a2),x8864),a55),a36))),
% 25.11/25.25 inference(scs_inference,[],[204,602,867,674,840,424,819,828,837,249,231,232,251,255,250,233,257,2,262])).
% 25.11/25.25 cnf(889,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(f37(f37(f37(f37(a1,a36),a36),a36),a36),a36),a36),a36),a36),f22(f37(f22(f22(a43,a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[204,602,867,674,840,424,819,828,837,187,249,231,232,251,255,250,233,257,2,262,247])).
% 25.11/25.25 cnf(892,plain,
% 25.11/25.25 (P6(f22(f37(a1,a36),a36),f3(f51(x8921,x8922,f3(f51(x8923,x8924,f3(f51(x8925,x8926,a2),x8926)),x8924)),x8922))),
% 25.11/25.25 inference(scs_inference,[],[204,843,602,867,674,840,424,465,819,828,837,187,249,231,232,251,255,250,233,257,2,262,247,139])).
% 25.11/25.25 cnf(916,plain,
% 25.11/25.25 (~P6(f22(f37(f22(f37(f37(f22(f37(x9161,a36),a36),a36),a36),a36),a36),a36),x9161)),
% 25.11/25.25 inference(scs_inference,[],[866,889,255,251])).
% 25.11/25.25 cnf(919,plain,
% 25.11/25.25 (~P4(x9191,f37(f37(f37(f22(f37(f22(x9191,a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[684,866,889,255,251,249])).
% 25.11/25.25 cnf(920,plain,
% 25.11/25.25 (~P6(f37(f37(f37(f22(f37(x9201,a36),a36),a36),a36),a36),x9201)),
% 25.11/25.25 inference(rename_variables,[],[684])).
% 25.11/25.25 cnf(926,plain,
% 25.11/25.25 (~P4(x9261,f37(f37(f37(f22(f37(x9261,a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[684,920,871,866,889,255,251,249,233,231,232])).
% 25.11/25.25 cnf(928,plain,
% 25.11/25.25 (~P6(f37(f37(f37(f22(f37(f37(x9281,a36),a36),a36),a36),a36),a36),x9281)),
% 25.11/25.25 inference(scs_inference,[],[684,920,871,866,889,255,251,249,233,231,232,250])).
% 25.11/25.25 cnf(931,plain,
% 25.11/25.25 (~P6(f22(f37(f37(f37(f37(f37(x9311,a36),a36),a36),a36),a36),a36),x9311)),
% 25.11/25.25 inference(scs_inference,[],[684,920,883,871,866,889,255,251,249,233,231,232,250,257])).
% 25.11/25.25 cnf(934,plain,
% 25.11/25.25 (E(a55,f3(a46,a41))),
% 25.11/25.25 inference(scs_inference,[],[684,920,883,425,871,866,889,255,251,249,233,231,232,250,257,2])).
% 25.11/25.25 cnf(938,plain,
% 25.11/25.25 (P4(f37(a42,a36),a1)),
% 25.11/25.25 inference(scs_inference,[],[204,684,920,883,886,425,871,866,889,173,187,255,251,249,233,231,232,250,257,2,262,247])).
% 25.11/25.25 cnf(941,plain,
% 25.11/25.25 (P6(a1,f3(f51(x9411,x9412,f3(f51(x9413,x9414,f3(f51(x9415,x9416,a2),x9416)),x9414)),x9412))),
% 25.11/25.25 inference(scs_inference,[],[204,586,684,920,883,886,425,465,871,866,889,173,187,255,251,249,233,231,232,250,257,2,262,247,139])).
% 25.11/25.25 cnf(968,plain,
% 25.11/25.25 (~P6(f37(f37(f37(f37(f37(f37(x9681,a36),a36),a36),a36),a36),a36),x9681)),
% 25.11/25.25 inference(scs_inference,[],[738,778,926,938,231,233,255,250])).
% 25.11/25.25 cnf(971,plain,
% 25.11/25.25 (~P6(f37(f37(f37(f22(f37(f22(f37(x9711,a36),a36),a36),a36),a36),a36),a36),x9711)),
% 25.11/25.25 inference(scs_inference,[],[738,778,926,919,938,231,233,255,250,251])).
% 25.11/25.25 cnf(974,plain,
% 25.11/25.25 (~P4(x9741,f22(f37(f37(f37(f37(f22(x9741,a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[738,778,926,919,938,231,233,255,250,251,249])).
% 25.11/25.25 cnf(975,plain,
% 25.11/25.25 (~P6(f22(f37(f37(f37(f37(x9751,a36),a36),a36),a36),a36),x9751)),
% 25.11/25.25 inference(rename_variables,[],[738])).
% 25.11/25.25 cnf(977,plain,
% 25.11/25.25 (~P6(f37(f37(f22(f37(f22(f37(f37(x9771,a36),a36),a36),a36),a36),a36),a36),x9771)),
% 25.11/25.25 inference(scs_inference,[],[738,778,926,919,938,231,233,255,250,251,249,257])).
% 25.11/25.25 cnf(979,plain,
% 25.11/25.25 (~P4(x9791,f22(f37(f37(f37(f37(x9791,a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[738,975,778,926,919,938,231,233,255,250,251,249,257,232])).
% 25.11/25.25 cnf(981,plain,
% 25.11/25.25 (E(a55,f3(a59,a39))),
% 25.11/25.25 inference(scs_inference,[],[738,975,778,426,926,919,938,231,233,255,250,251,249,257,232,2])).
% 25.11/25.25 cnf(982,plain,
% 25.11/25.25 (P4(f37(a42,a36),a43)),
% 25.11/25.25 inference(scs_inference,[],[738,975,778,426,926,919,174,938,187,231,233,255,250,251,249,257,232,2,247])).
% 25.11/25.25 cnf(985,plain,
% 25.11/25.25 (~E(f3(x9851,a55),f22(f37(f22(f3(f51(x9851,f3(a45,a2),x9852),a55),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[204,738,975,778,426,529,926,919,174,938,187,231,233,255,250,251,249,257,232,2,247,262])).
% 25.11/25.25 cnf(1001,plain,
% 25.11/25.25 (~P6(a38,a1)),
% 25.11/25.25 inference(scs_inference,[],[204,474,633,446,547,892,738,975,778,934,426,465,529,385,926,919,155,174,938,187,205,231,233,255,250,251,249,257,232,2,247,262,139,136,137,3,138,314,552])).
% 25.11/25.25 cnf(1006,plain,
% 25.11/25.25 (E(a42,a1)+~P6(a42,a1)),
% 25.11/25.25 inference(scs_inference,[],[204,474,633,711,446,547,892,738,975,778,934,426,465,529,385,926,919,155,174,938,187,205,231,233,255,250,251,249,257,232,2,247,262,139,136,137,3,138,314,552,236,230,237])).
% 25.11/25.25 cnf(1010,plain,
% 25.11/25.25 (~P6(f22(f37(f37(f37(f37(f22(f37(x10101,a36),a36),a36),a36),a36),a36),a36),x10101)),
% 25.11/25.25 inference(scs_inference,[],[974,251])).
% 25.11/25.25 cnf(1013,plain,
% 25.11/25.25 (~P6(f37(f22(f37(f22(f37(f37(f37(x10131,a36),a36),a36),a36),a36),a36),a36),x10131)),
% 25.11/25.25 inference(scs_inference,[],[977,974,251,257])).
% 25.11/25.25 cnf(1016,plain,
% 25.11/25.25 (~P6(f37(f22(f37(f37(f22(f37(f37(x10161,a36),a36),a36),a36),a36),a36),a36),x10161)),
% 25.11/25.25 inference(scs_inference,[],[783,977,974,251,257,250])).
% 25.11/25.25 cnf(1023,plain,
% 25.11/25.25 (~P4(a1,a38)),
% 25.11/25.25 inference(scs_inference,[],[1001,783,977,979,974,251,257,250,231,233,232])).
% 25.11/25.25 cnf(1027,plain,
% 25.11/25.25 (~P4(x10271,f37(f37(f22(f37(f22(f37(f22(x10271,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[1001,735,783,977,979,974,982,251,257,250,231,233,232,255,249])).
% 25.11/25.25 cnf(1030,plain,
% 25.11/25.25 (E(a55,f3(a59,a40))),
% 25.11/25.25 inference(scs_inference,[],[1001,735,783,977,427,979,974,982,251,257,250,231,233,232,255,249,2])).
% 25.11/25.25 cnf(1034,plain,
% 25.11/25.25 (P4(f37(a42,a36),a36)),
% 25.11/25.25 inference(scs_inference,[],[204,1001,735,783,977,985,427,175,979,974,982,187,251,257,250,231,233,232,255,249,2,262,247])).
% 25.11/25.25 cnf(1047,plain,
% 25.11/25.25 (~E(f4(x10471,a55,f3(a59,a39)),f22(f22(f37(f4(f54(x10471,f3(a45,a2),a55,x10472),a55,f3(a59,a39)),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[181,204,578,941,458,547,1001,735,783,977,985,981,427,465,385,175,979,974,982,187,205,251,257,250,231,233,232,255,249,2,262,247,136,139,137,3,138,314])).
% 25.11/25.25 cnf(1064,plain,
% 25.11/25.25 (~P6(f37(f37(f22(f37(f22(f37(f22(f37(x10641,a36),a36),a36),a36),a36),a36),a36),a36),x10641)),
% 25.11/25.25 inference(scs_inference,[],[788,1027,1034,233,231,255,251])).
% 25.11/25.25 cnf(1067,plain,
% 25.11/25.25 (~P6(f22(f37(f22(f37(f37(f37(f37(x10671,a36),a36),a36),a36),a36),a36),a36),x10671)),
% 25.11/25.25 inference(scs_inference,[],[788,1013,1027,1034,233,231,255,251,257])).
% 25.11/25.25 cnf(1070,plain,
% 25.11/25.25 (~P4(x10701,f22(f37(f22(f37(f37(f37(f22(x10701,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[788,1013,1027,1034,233,231,255,251,257,249])).
% 25.11/25.25 cnf(1071,plain,
% 25.11/25.25 (~P6(f22(f37(f22(f37(f37(f37(x10711,a36),a36),a36),a36),a36),a36),x10711)),
% 25.11/25.25 inference(rename_variables,[],[788])).
% 25.11/25.25 cnf(1073,plain,
% 25.11/25.25 (~P6(f22(f37(f37(f22(f37(f37(f37(x10731,a36),a36),a36),a36),a36),a36),a36),x10731)),
% 25.11/25.25 inference(scs_inference,[],[788,823,1013,1027,1034,233,231,255,251,257,249,250])).
% 25.11/25.25 cnf(1076,plain,
% 25.11/25.25 (~P4(x10761,f22(f37(f22(f37(f37(f37(x10761,a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[788,1071,823,1013,1027,1034,233,231,255,251,257,249,250,232])).
% 25.11/25.25 cnf(1078,plain,
% 25.11/25.25 (E(a55,f3(a59,a41))),
% 25.11/25.25 inference(scs_inference,[],[788,1071,823,1013,428,1027,1034,233,231,255,251,257,249,250,232,2])).
% 25.11/25.25 cnf(1079,plain,
% 25.11/25.25 (P4(f37(a42,a36),a38)),
% 25.11/25.25 inference(scs_inference,[],[788,1071,823,1013,428,176,1027,1034,187,233,231,255,251,257,249,250,232,2,247])).
% 25.11/25.25 cnf(1082,plain,
% 25.11/25.25 (~E(f3(x10821,a55),f37(f22(f22(f3(f51(x10821,f3(a45,a2),x10822),a55),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[204,788,1071,823,1013,428,544,176,1027,1034,187,233,231,255,251,257,249,250,232,2,247,262])).
% 25.11/25.25 cnf(1085,plain,
% 25.11/25.25 (~E(f37(f22(f37(f37(x10851,a36),a36),a36),a36),x10851)),
% 25.11/25.25 inference(scs_inference,[],[204,545,788,1071,823,1013,428,544,182,176,1027,1034,187,233,231,255,251,257,249,250,232,2,247,262,139])).
% 25.11/25.25 cnf(1097,plain,
% 25.11/25.25 (~P6(a42,a1)),
% 25.11/25.25 inference(scs_inference,[],[204,474,487,545,547,788,1071,823,1013,1030,428,544,182,385,176,1027,1034,1023,187,233,231,255,251,257,249,250,232,2,247,262,139,136,3,137,138,314,1006])).
% 25.11/25.25 cnf(1107,plain,
% 25.11/25.25 (~P6(f22(f37(f37(f37(f22(f37(f37(x11071,a36),a36),a36),a36),a36),a36),a36),x11071)),
% 25.11/25.25 inference(scs_inference,[],[1085,873,4,250])).
% 25.11/25.25 cnf(1108,plain,
% 25.11/25.25 (~P6(f22(f37(f37(f37(f22(f37(x11081,a36),a36),a36),a36),a36),a36),x11081)),
% 25.11/25.25 inference(rename_variables,[],[873])).
% 25.11/25.25 cnf(1110,plain,
% 25.11/25.25 (~P6(f37(f22(f37(f22(f37(f22(f37(f37(x11101,a36),a36),a36),a36),a36),a36),a36),a36),x11101)),
% 25.11/25.25 inference(scs_inference,[],[1085,873,1064,4,250,257])).
% 25.11/25.25 cnf(1113,plain,
% 25.11/25.25 (~P6(f22(f37(f22(f37(f37(f37(f22(f37(x11131,a36),a36),a36),a36),a36),a36),a36),a36),x11131)),
% 25.11/25.25 inference(scs_inference,[],[1085,873,1064,1070,4,250,257,251])).
% 25.11/25.25 cnf(1122,plain,
% 25.11/25.25 (~P4(x11221,f22(f37(f37(f37(f22(f37(x11221,a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[1085,873,1108,1064,1076,1070,1079,4,250,257,251,233,231,255,232])).
% 25.11/25.25 cnf(1124,plain,
% 25.11/25.25 (~P4(x11241,f22(f37(f37(f37(f22(f37(f22(x11241,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[1085,873,1108,1064,1076,1070,1079,4,250,257,251,233,231,255,232,249])).
% 25.11/25.25 cnf(1128,plain,
% 25.11/25.25 (P6(a2,a42)),
% 25.11/25.25 inference(scs_inference,[],[181,1085,873,1108,1064,429,1076,1070,1079,4,250,257,251,233,231,255,232,249,2,248])).
% 25.11/25.25 cnf(1133,plain,
% 25.11/25.25 (P4(f37(a42,a36),a39)),
% 25.11/25.25 inference(scs_inference,[],[181,204,1085,873,1108,1064,1082,429,1076,1070,177,1079,187,4,250,257,251,233,231,255,232,249,2,248,262,247])).
% 25.11/25.25 cnf(1138,plain,
% 25.11/25.25 (~E(f37(f22(f37(f22(f37(x11381,a36),a36),a36),a36),a36),x11381)),
% 25.11/25.25 inference(scs_inference,[],[181,204,575,1085,873,1108,1064,1082,429,182,1076,1070,162,177,1079,187,205,4,250,257,251,233,231,255,232,249,2,248,262,247,136,139])).
% 25.11/25.25 cnf(1142,plain,
% 25.11/25.25 (~E(f37(a36,f3(f51(x11421,x11422,f3(f51(x11423,x11424,x11425),x11424)),x11422)),x11425)),
% 25.11/25.25 inference(scs_inference,[],[181,204,533,575,465,1085,873,1108,1064,1082,429,182,385,1076,1070,162,177,1079,187,205,4,250,257,251,233,231,255,232,249,2,248,262,247,136,139,137,3])).
% 25.11/25.25 cnf(1146,plain,
% 25.11/25.25 (~E(f4(x11461,a55,f3(f51(x11462,x11463,x11464),x11463)),f22(f22(f37(f4(f54(x11461,f3(a45,a2),x11464,x11465),a55,f3(f51(x11462,x11463,x11464),x11463)),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[181,204,533,575,547,465,1085,873,1108,1064,1082,429,182,385,1076,1070,162,177,1079,187,205,4,250,257,251,233,231,255,232,249,2,248,262,247,136,139,137,3,138,314])).
% 25.11/25.25 cnf(1149,plain,
% 25.11/25.25 (~E(f3(f51(x11491,x11492,f3(f51(x11493,x11494,f37(a36,x11495)),x11494)),x11492),x11495)),
% 25.11/25.25 inference(scs_inference,[],[181,204,533,575,547,465,1085,873,1108,1064,1082,429,182,385,1076,1070,162,177,1079,187,205,4,250,257,251,233,231,255,232,249,2,248,262,247,136,139,137,3,138,314,5])).
% 25.11/25.25 cnf(1150,plain,
% 25.11/25.25 (~E(f37(f37(f37(f22(x11501,a36),a36),a36),a36),x11501)),
% 25.11/25.25 inference(scs_inference,[],[181,204,533,575,547,465,1085,873,1108,1064,1082,429,182,385,1076,1070,162,177,1079,187,205,4,250,257,251,233,231,255,232,249,2,248,262,247,136,139,137,3,138,314,5,27])).
% 25.11/25.25 cnf(1163,plain,
% 25.11/25.25 (~P6(f22(f37(f22(f37(f22(f37(f37(f37(x11631,a36),a36),a36),a36),a36),a36),a36),a36),x11631)),
% 25.11/25.25 inference(scs_inference,[],[1138,1110,1149,95,4,257])).
% 25.11/25.25 cnf(1170,plain,
% 25.11/25.25 (~P4(x11701,f37(f37(f22(f37(f37(f37(f22(x11701,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[1097,1138,878,1110,1149,1122,95,4,257,233,231,249])).
% 25.11/25.25 cnf(1171,plain,
% 25.11/25.25 (~P6(f37(f37(f22(f37(f37(f37(x11711,a36),a36),a36),a36),a36),a36),x11711)),
% 25.11/25.25 inference(rename_variables,[],[878])).
% 25.11/25.25 cnf(1173,plain,
% 25.11/25.25 (~P6(f37(f37(f22(f37(f37(f37(f37(x11731,a36),a36),a36),a36),a36),a36),a36),x11731)),
% 25.11/25.25 inference(scs_inference,[],[1097,1138,878,1171,1110,1149,1122,95,4,257,233,231,249,250])).
% 25.11/25.25 cnf(1176,plain,
% 25.11/25.25 (~P6(f22(f37(f37(f37(f22(f37(f22(f37(x11761,a36),a36),a36),a36),a36),a36),a36),a36),x11761)),
% 25.11/25.25 inference(scs_inference,[],[1097,1138,878,1171,1110,1149,1122,1124,95,4,257,233,231,249,250,251])).
% 25.11/25.25 cnf(1184,plain,
% 25.11/25.25 (P4(f37(a42,a36),a40)),
% 25.11/25.25 inference(scs_inference,[],[1097,1138,878,1171,1110,430,1149,1122,1124,178,1133,187,95,4,257,233,231,249,250,251,232,255,2,247])).
% 25.11/25.25 cnf(1189,plain,
% 25.11/25.25 (P6(a2,f3(f51(x11891,x11892,a42),x11892))),
% 25.11/25.25 inference(scs_inference,[],[465,1097,1138,878,1171,1110,1128,430,1149,1122,1124,163,178,1133,187,205,95,4,257,233,231,249,250,251,232,255,2,247,136,139])).
% 25.11/25.25 cnf(1190,plain,
% 25.11/25.25 (E(x11901,f3(f51(x11902,x11903,x11901),x11903))),
% 25.11/25.25 inference(rename_variables,[],[465])).
% 25.11/25.25 cnf(1200,plain,
% 25.11/25.25 (~E(f3(f51(x12001,x12002,f37(a36,f3(f51(x12003,x12004,x12005),x12004))),x12002),x12005)),
% 25.11/25.25 inference(scs_inference,[],[204,641,533,379,465,1190,1097,1138,878,1171,1110,1146,1078,1128,430,1149,385,1122,1124,163,178,1133,187,205,95,4,257,233,231,249,250,251,232,255,2,247,136,139,137,138,3,314,89])).
% 25.11/25.25 cnf(1201,plain,
% 25.11/25.25 (~E(f37(f22(f37(f37(f22(x12011,a36),a36),a36),a36),a36),x12011)),
% 25.11/25.25 inference(scs_inference,[],[204,641,533,379,465,1190,1097,1138,878,1171,1110,1146,1078,1128,430,1149,385,1122,1124,163,178,1133,187,205,95,4,257,233,231,249,250,251,232,255,2,247,136,139,137,138,3,314,89,27])).
% 25.11/25.25 cnf(1213,plain,
% 25.11/25.25 (~P6(f37(f22(f37(f37(f37(f37(f37(x12131,a36),a36),a36),a36),a36),a36),a36),x12131)),
% 25.11/25.25 inference(scs_inference,[],[1173,1200,95,257])).
% 25.11/25.25 cnf(1220,plain,
% 25.11/25.25 (~P4(x12201,f37(f37(f37(f22(f37(f37(f22(x12201,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[928,1173,1200,1150,1170,95,257,231,4,249])).
% 25.11/25.25 cnf(1221,plain,
% 25.11/25.25 (~P6(f37(f37(f37(f22(f37(f37(x12211,a36),a36),a36),a36),a36),a36),x12211)),
% 25.11/25.25 inference(rename_variables,[],[928])).
% 25.11/25.25 cnf(1225,plain,
% 25.11/25.25 (~P4(x12251,f37(f37(f37(f22(f37(f37(x12251,a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[928,1221,1173,1200,1150,1170,95,257,231,4,249,233,232])).
% 25.11/25.25 cnf(1227,plain,
% 25.11/25.25 (~P6(f37(f37(f37(f22(f37(f37(f37(x12271,a36),a36),a36),a36),a36),a36),a36),x12271)),
% 25.11/25.25 inference(scs_inference,[],[928,1221,1173,1200,1150,1170,95,257,231,4,249,233,232,250])).
% 25.11/25.25 cnf(1230,plain,
% 25.11/25.25 (~P6(f37(f37(f22(f37(f37(f37(f22(f37(x12301,a36),a36),a36),a36),a36),a36),a36),a36),x12301)),
% 25.11/25.25 inference(scs_inference,[],[928,1221,1173,1200,1150,1170,95,257,231,4,249,233,232,250,251])).
% 25.11/25.25 cnf(1236,plain,
% 25.11/25.25 (P4(f37(f37(a42,a36),a36),a40)),
% 25.11/25.25 inference(scs_inference,[],[928,1221,1173,431,1200,1150,1170,1184,187,95,257,231,4,249,233,232,250,251,255,2,247])).
% 25.11/25.25 cnf(1241,plain,
% 25.11/25.25 (P6(a2,f3(f51(x12411,x12412,f3(f51(x12413,x12414,a42),x12414)),x12412))),
% 25.11/25.25 inference(scs_inference,[],[465,928,1221,1173,1189,431,1200,1150,167,1170,1184,187,205,95,257,231,4,249,233,232,250,251,255,2,247,136,139])).
% 25.11/25.25 cnf(1264,plain,
% 25.11/25.25 (~P4(x12641,f22(f37(f37(f37(f37(f37(f22(x12641,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[931,1225,231,249])).
% 25.11/25.25 cnf(1265,plain,
% 25.11/25.25 (~P6(f22(f37(f37(f37(f37(f37(x12651,a36),a36),a36),a36),a36),a36),x12651)),
% 25.11/25.25 inference(rename_variables,[],[931])).
% 25.11/25.25 cnf(1269,plain,
% 25.11/25.25 (~P6(f22(f37(f37(f37(f37(f37(f37(x12691,a36),a36),a36),a36),a36),a36),a36),x12691)),
% 25.11/25.25 inference(scs_inference,[],[931,1265,1213,1225,231,249,233,257])).
% 25.11/25.25 cnf(1272,plain,
% 25.11/25.25 (~P6(f37(f37(f37(f22(f37(f37(f22(f37(x12721,a36),a36),a36),a36),a36),a36),a36),a36),x12721)),
% 25.11/25.25 inference(scs_inference,[],[931,1265,1213,1225,1220,231,249,233,257,251])).
% 25.11/25.25 cnf(1275,plain,
% 25.11/25.25 (~P4(x12751,f22(f37(f37(f37(f37(f37(x12751,a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[931,1265,1213,1225,1220,231,249,233,257,251,232])).
% 25.11/25.25 cnf(1279,plain,
% 25.11/25.25 (~P6(f37(f37(f37(f37(f37(f37(f37(x12791,a36),a36),a36),a36),a36),a36),a36),x12791)),
% 25.11/25.25 inference(scs_inference,[],[931,1265,968,1213,1201,1225,1220,231,249,233,257,251,232,4,250])).
% 25.11/25.25 cnf(1285,plain,
% 25.11/25.25 (P4(f37(f37(a42,a36),a36),a36)),
% 25.11/25.25 inference(scs_inference,[],[931,1265,968,1213,432,1201,1225,1220,164,1236,231,249,233,257,251,232,4,250,255,2,247])).
% 25.11/25.25 cnf(1311,plain,
% 25.11/25.25 (P5(f3(f51(x13111,x13112,a38),x13112),a2)),
% 25.11/25.25 inference(scs_inference,[],[181,465,235,146])).
% 25.11/25.25 cnf(1317,plain,
% 25.11/25.25 (~P6(f37(f22(f37(f22(f37(f22(f37(x13171,a36),a36),a36),a36),a36),a36),a36),x13171)),
% 25.11/25.25 inference(rename_variables,[],[833])).
% 25.11/25.25 cnf(1319,plain,
% 25.11/25.25 (~P6(f22(f37(f37(f37(f37(f37(f22(f37(x13191,a36),a36),a36),a36),a36),a36),a36),a36),x13191)),
% 25.11/25.25 inference(scs_inference,[],[833,1275,1264,231,233,249,251])).
% 25.11/25.25 cnf(1322,plain,
% 25.11/25.25 (~P4(x13221,f37(f22(f37(f22(f37(f22(f37(x13221,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[833,1317,1275,1264,231,233,249,251,232])).
% 25.11/25.25 cnf(1324,plain,
% 25.11/25.25 (~P6(f37(f22(f37(f37(f37(f22(f37(f37(x13241,a36),a36),a36),a36),a36),a36),a36),a36),x13241)),
% 25.11/25.25 inference(scs_inference,[],[833,1317,1230,1275,1264,231,233,249,251,232,257])).
% 25.11/25.25 cnf(1333,plain,
% 25.11/25.25 (P5(f3(f51(x13331,x13332,f3(f51(x13333,x13334,a38),x13334)),x13332),a2)),
% 25.11/25.25 inference(scs_inference,[],[465,833,1317,916,1230,433,1275,1264,1311,1285,231,233,249,251,232,257,255,250,2,146])).
% 25.11/25.25 cnf(1335,plain,
% 25.11/25.25 (P4(f37(f37(f37(a42,a36),a36),a36),a36)),
% 25.11/25.25 inference(scs_inference,[],[465,833,1317,916,1230,433,1275,1264,1311,1285,187,231,233,249,251,232,257,255,250,2,146,247])).
% 25.11/25.25 cnf(1364,plain,
% 25.11/25.25 (~P6(f22(f37(f22(f37(f22(f37(f37(x13641,a36),a36),a36),a36),a36),a36),a36),x13641)),
% 25.11/25.25 inference(rename_variables,[],[856])).
% 25.11/25.25 cnf(1366,plain,
% 25.11/25.25 (~P4(x13661,f22(f37(f22(f37(f22(f37(f37(x13661,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[856,1364,1322,231,249,232])).
% 25.11/25.25 cnf(1368,plain,
% 25.11/25.25 (~P6(f37(f37(f22(f37(f37(f22(f37(f37(x13681,a36),a36),a36),a36),a36),a36),a36),a36),x13681)),
% 25.11/25.25 inference(scs_inference,[],[856,1364,1272,1322,231,249,232,257])).
% 25.11/25.25 cnf(1375,plain,
% 25.11/25.25 (~P6(f37(f37(f37(f22(f37(f22(f37(f37(x13751,a36),a36),a36),a36),a36),a36),a36),a36),x13751)),
% 25.11/25.25 inference(scs_inference,[],[856,1364,971,1272,1322,1335,231,249,232,257,233,255,250])).
% 25.11/25.25 cnf(1379,plain,
% 25.11/25.25 (P5(f3(f51(x13791,x13792,f3(f51(x13793,x13794,f3(f51(x13795,x13796,a38),x13796)),x13794)),x13792),a2)),
% 25.11/25.25 inference(scs_inference,[],[465,856,1364,971,1272,434,1322,1333,1335,231,249,232,257,233,255,250,2,146])).
% 25.11/25.25 cnf(1381,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(a42,a36),a36),a36),a36),a36)),
% 25.11/25.25 inference(scs_inference,[],[465,856,1364,971,1272,434,1322,1333,1335,187,231,249,232,257,233,255,250,2,146,247])).
% 25.11/25.25 cnf(1409,plain,
% 25.11/25.25 (~P4(x14091,f22(f37(f37(f37(f37(f22(f37(x14091,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[1010,389,231,232])).
% 25.11/25.25 cnf(1416,plain,
% 25.11/25.25 (~P6(f37(f22(f37(f37(f22(f37(f37(x14161,a36),a36),a36),a36),a36),a36),a36),x14161)),
% 25.11/25.25 inference(rename_variables,[],[1016])).
% 25.11/25.25 cnf(1423,plain,
% 25.11/25.25 (~P6(f37(f22(f37(f37(f22(f37(f37(f37(x14231,a36),a36),a36),a36),a36),a36),a36),a36),x14231)),
% 25.11/25.25 inference(scs_inference,[],[1010,1016,1416,1324,389,1381,231,232,233,251,249,257,255,250])).
% 25.11/25.25 cnf(1429,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(f37(a42,a36),a36),a36),a36),a36),a36)),
% 25.11/25.25 inference(scs_inference,[],[465,1010,1016,1416,1324,435,389,1379,1381,187,231,232,233,251,249,257,255,250,2,146,247])).
% 25.11/25.25 cnf(1459,plain,
% 25.11/25.25 (~P6(f22(f37(f22(f37(f37(f37(f37(x14591,a36),a36),a36),a36),a36),a36),a36),x14591)),
% 25.11/25.25 inference(rename_variables,[],[1067])).
% 25.11/25.25 cnf(1461,plain,
% 25.11/25.25 (~P4(x14611,f22(f37(f22(f37(f37(f37(f37(x14611,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[1067,1459,506,231,233,249,232])).
% 25.11/25.25 cnf(1463,plain,
% 25.11/25.25 (~P6(f37(f37(f22(f37(f22(f37(f37(f37(x14631,a36),a36),a36),a36),a36),a36),a36),a36),x14631)),
% 25.11/25.25 inference(scs_inference,[],[1067,1459,1375,506,231,233,249,232,257])).
% 25.11/25.25 cnf(1474,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(f37(f37(a42,a36),a36),a36),a36),a36),a36),a36)),
% 25.11/25.25 inference(scs_inference,[],[1067,1459,1073,1375,436,506,1429,187,231,233,249,232,257,251,255,250,2,247])).
% 25.11/25.25 cnf(1503,plain,
% 25.11/25.25 (~P6(f22(f37(f37(f37(f22(f37(f37(x15031,a36),a36),a36),a36),a36),a36),a36),x15031)),
% 25.11/25.25 inference(rename_variables,[],[1107])).
% 25.11/25.25 cnf(1505,plain,
% 25.11/25.25 (~P6(f37(f22(f37(f22(f37(f37(f37(f37(x15051,a36),a36),a36),a36),a36),a36),a36),a36),x15051)),
% 25.11/25.25 inference(scs_inference,[],[1107,1463,563,231,249,257])).
% 25.11/25.25 cnf(1510,plain,
% 25.11/25.25 (~P4(x15101,f22(f37(f37(f37(f22(f37(f37(x15101,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[1107,1503,1463,563,231,249,257,233,232])).
% 25.11/25.25 cnf(1514,plain,
% 25.11/25.25 (~P6(f37(f37(f37(f22(f37(f37(f37(f37(x15141,a36),a36),a36),a36),a36),a36),a36),a36),x15141)),
% 25.11/25.25 inference(scs_inference,[],[1107,1503,1227,1463,563,1474,231,249,257,233,232,255,250])).
% 25.11/25.25 cnf(1517,plain,
% 25.11/25.25 (E(a55,f3(a61,a38))),
% 25.11/25.25 inference(scs_inference,[],[1107,1503,1227,1463,437,563,1474,231,249,257,233,232,255,250,2])).
% 25.11/25.25 cnf(1518,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(f37(f37(f37(a42,a36),a36),a36),a36),a36),a36),a36),a36)),
% 25.11/25.25 inference(scs_inference,[],[1107,1503,1227,1463,437,563,1474,187,231,249,257,233,232,255,250,2,247])).
% 25.11/25.25 cnf(1534,plain,
% 25.11/25.25 (~E(f22(f37(f22(f37(f3(f51(x15341,x15342,f22(x15343,a36)),x15342),a36),a36),a36),a36),x15343)),
% 25.11/25.25 inference(scs_inference,[],[204,396,633,465,515,1107,1503,1227,1463,1047,437,981,394,385,563,160,1474,187,205,231,249,257,233,232,255,250,2,247,136,139,138,3,137,314,27])).
% 25.11/25.25 cnf(1535,plain,
% 25.11/25.25 (~E(f37(f22(f37(f37(f37(x15351,a36),a36),a36),a36),a36),x15351)),
% 25.11/25.25 inference(scs_inference,[],[204,396,633,465,515,1107,1503,1227,1463,1047,437,981,394,385,563,160,1474,187,205,231,249,257,233,232,255,250,2,247,136,139,138,3,137,314,27,4])).
% 25.11/25.25 cnf(1536,plain,
% 25.11/25.25 (P5(a38,a2)),
% 25.11/25.25 inference(scs_inference,[],[204,396,633,465,515,1107,1503,1227,1463,1047,437,981,195,394,1311,385,563,160,1474,187,205,231,249,257,233,232,255,250,2,247,136,139,138,3,137,314,27,4,146])).
% 25.11/25.25 cnf(1549,plain,
% 25.11/25.25 (~E(f37(f22(f37(f3(f51(x15491,x15492,f22(f22(x15493,a36),a36)),x15492),a36),a36),a36),x15493)),
% 25.11/25.25 inference(scs_inference,[],[1534,27])).
% 25.11/25.25 cnf(1553,plain,
% 25.11/25.25 (~P6(f37(f37(f22(f37(f37(f37(f37(f37(x15531,a36),a36),a36),a36),a36),a36),a36),a36),x15531)),
% 25.11/25.25 inference(scs_inference,[],[1514,1534,619,27,231,257])).
% 25.11/25.25 cnf(1557,plain,
% 25.11/25.25 (~P6(f22(f37(f37(f37(f37(f37(f37(x15571,a36),a36),a36),a36),a36),a36),a36),x15571)),
% 25.11/25.25 inference(rename_variables,[],[1269])).
% 25.11/25.25 cnf(1559,plain,
% 25.11/25.25 (~P4(x15591,f22(f37(f37(f37(f37(f37(f37(x15591,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[1269,1557,1514,1534,619,27,231,257,249,232])).
% 25.11/25.25 cnf(1563,plain,
% 25.11/25.25 (~E(f22(f37(f37(f37(f37(x15631,a36),a36),a36),a36),a36),x15631)),
% 25.11/25.25 inference(scs_inference,[],[1535,1269,1557,1514,1534,619,27,231,257,249,232,233,4])).
% 25.11/25.25 cnf(1570,plain,
% 25.11/25.25 (E(a55,f3(a61,a39))),
% 25.11/25.25 inference(scs_inference,[],[1535,1269,1557,1514,438,1534,619,1518,27,231,257,249,232,233,4,255,250,2])).
% 25.11/25.25 cnf(1571,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(f37(f37(f37(f37(a42,a36),a36),a36),a36),a36),a36),a36),a36),a36)),
% 25.11/25.25 inference(scs_inference,[],[1535,1269,1557,1514,438,1534,619,1518,187,27,231,257,249,232,233,4,255,250,2,247])).
% 25.11/25.25 cnf(1594,plain,
% 25.11/25.25 (~E(f37(f37(f37(f37(f22(x15941,a36),a36),a36),a36),a36),x15941)),
% 25.11/25.25 inference(scs_inference,[],[1563,27])).
% 25.11/25.25 cnf(1599,plain,
% 25.11/25.25 (~P6(f37(f37(f37(f37(f37(f37(f37(x15991,a36),a36),a36),a36),a36),a36),a36),x15991)),
% 25.11/25.25 inference(rename_variables,[],[1279])).
% 25.11/25.25 cnf(1601,plain,
% 25.11/25.25 (~P6(f37(f22(f37(f37(f37(f37(f37(f37(x16011,a36),a36),a36),a36),a36),a36),a36),a36),x16011)),
% 25.11/25.25 inference(scs_inference,[],[1563,1279,1553,677,27,231,249,257])).
% 25.11/25.25 cnf(1604,plain,
% 25.11/25.25 (~P4(x16041,f37(f37(f37(f37(f37(f37(f37(x16041,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[1563,1279,1599,1553,677,27,231,249,257,232])).
% 25.11/25.25 cnf(1606,plain,
% 25.11/25.25 (~E(f22(f37(f3(f51(x16061,x16062,f22(f22(f37(x16063,a36),a36),a36)),x16062),a36),a36),x16063)),
% 25.11/25.25 inference(scs_inference,[],[1563,1279,1599,1553,1549,677,27,231,249,257,232,4])).
% 25.11/25.25 cnf(1612,plain,
% 25.11/25.25 (~P6(f37(f37(f37(f37(f37(f37(f37(f37(x16121,a36),a36),a36),a36),a36),a36),a36),a36),x16121)),
% 25.11/25.25 inference(scs_inference,[],[1563,1279,1599,1553,1549,677,1571,27,231,249,257,232,4,233,255,250])).
% 25.11/25.25 cnf(1615,plain,
% 25.11/25.25 (E(a55,f3(a61,a40))),
% 25.11/25.25 inference(scs_inference,[],[1563,1279,1599,1553,439,1549,677,1571,27,231,249,257,232,4,233,255,250,2])).
% 25.11/25.25 cnf(1616,plain,
% 25.11/25.25 (P4(f37(a42,a36),a41)),
% 25.11/25.25 inference(scs_inference,[],[1563,1279,1599,1553,439,1549,677,1571,179,187,27,231,249,257,232,4,233,255,250,2,247])).
% 25.11/25.25 cnf(1621,plain,
% 25.11/25.25 (~E(f22(f37(f37(f37(f22(f37(x16211,a36),a36),a36),a36),a36),a36),x16211)),
% 25.11/25.25 inference(scs_inference,[],[1563,1279,1599,1113,1553,439,1549,394,677,1571,179,187,205,27,231,249,257,232,4,233,255,250,2,247,136,139])).
% 25.11/25.25 cnf(1629,plain,
% 25.11/25.25 (~E(f4(x16291,a55,f3(f51(x16292,x16293,x16294),x16293)),f22(f4(f54(x16291,f3(a45,a2),x16294,x16295),a55,f3(f51(x16292,x16293,x16294),x16293)),a36))),
% 25.11/25.25 inference(scs_inference,[],[180,204,533,465,575,1563,1279,1599,1113,1553,1517,439,472,1549,394,389,677,1571,157,179,187,205,27,231,249,257,232,4,233,255,250,2,247,136,139,138,3,137,314])).
% 25.11/25.25 cnf(1639,plain,
% 25.11/25.25 (~E(f37(f3(f51(x16391,x16392,f22(f22(f37(f22(x16393,a36),a36),a36),a36)),x16392),a36),x16393)),
% 25.11/25.25 inference(scs_inference,[],[1606,27])).
% 25.11/25.25 cnf(1643,plain,
% 25.11/25.25 (~P4(x16431,f37(f37(f37(f37(f22(x16431,a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[1606,616,721,27,231,249])).
% 25.11/25.25 cnf(1654,plain,
% 25.11/25.25 (E(a55,f3(a61,a41))),
% 25.11/25.25 inference(scs_inference,[],[1606,1163,440,616,1594,721,1616,27,231,249,232,233,255,4,2])).
% 25.11/25.25 cnf(1655,plain,
% 25.11/25.25 (P4(f37(f37(a42,a36),a36),a41)),
% 25.11/25.25 inference(scs_inference,[],[1606,1163,440,616,1594,721,1616,187,27,231,249,232,233,255,4,2,247])).
% 25.11/25.25 cnf(1658,plain,
% 25.11/25.25 (~E(f22(f37(f22(f37(f37(f37(x16581,a36),a36),a36),a36),a36),a36),x16581)),
% 25.11/25.25 inference(scs_inference,[],[1606,1163,440,616,1594,394,721,1616,187,27,231,249,232,233,255,4,2,247,139])).
% 25.11/25.25 cnf(1668,plain,
% 25.11/25.25 (~E(f4(x16681,a55,f3(f51(x16682,x16683,x16684),x16683)),f22(f4(f54(f54(x16681,f3(a45,a2),x16684,x16685),f3(a45,a2),x16684,x16686),a55,f3(f51(x16682,x16683,x16684),x16683)),a36))),
% 25.11/25.25 inference(scs_inference,[],[204,711,487,465,379,1606,1163,1629,1570,440,616,1594,394,385,721,1616,187,205,27,231,249,232,233,255,4,2,247,139,136,3,138,137,314])).
% 25.11/25.25 cnf(1671,plain,
% 25.11/25.25 (~P6(f37(f37(f37(f37(f22(f37(x16711,a36),a36),a36),a36),a36),a36),x16711)),
% 25.11/25.25 inference(scs_inference,[],[204,711,487,465,379,1606,1163,1629,1570,440,616,1594,394,385,721,1616,187,205,27,231,249,232,233,255,4,2,247,139,136,3,138,137,314,251])).
% 25.11/25.25 cnf(1673,plain,
% 25.11/25.25 (~P6(f37(f37(f37(f37(f22(f37(f37(x16731,a36),a36),a36),a36),a36),a36),a36),x16731)),
% 25.11/25.25 inference(scs_inference,[],[204,711,487,465,379,1606,1163,1629,1570,440,616,1594,394,385,721,1616,187,205,27,231,249,232,233,255,4,2,247,139,136,3,138,137,314,251,250])).
% 25.11/25.25 cnf(1688,plain,
% 25.11/25.25 (~P4(x16881,f37(f37(f22(f37(f37(f22(x16881,a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[1368,674,1621,828,27,231,232,249])).
% 25.11/25.25 cnf(1697,plain,
% 25.11/25.25 (~P6(f37(f37(f37(f37(f22(f37(f37(f37(x16971,a36),a36),a36),a36),a36),a36),a36),a36),x16971)),
% 25.11/25.25 inference(scs_inference,[],[1368,674,1621,1673,1639,828,1655,27,231,232,249,233,255,4,250])).
% 25.11/25.25 cnf(1700,plain,
% 25.11/25.25 (E(a55,f4(a56,a1,a1))),
% 25.11/25.25 inference(scs_inference,[],[1368,674,1621,1673,441,1639,828,1655,27,231,232,249,233,255,4,250,2])).
% 25.11/25.25 cnf(1701,plain,
% 25.11/25.25 (P4(f37(f37(f37(a42,a36),a36),a36),a41)),
% 25.11/25.25 inference(scs_inference,[],[1368,674,1621,1673,441,1639,828,1655,187,27,231,232,249,233,255,4,250,2,247])).
% 25.11/25.25 cnf(1704,plain,
% 25.11/25.25 (~E(f37(f37(f22(f37(f22(f37(x17041,a36),a36),a36),a36),a36),a36),x17041)),
% 25.11/25.25 inference(scs_inference,[],[1368,674,1621,1673,1176,441,1639,394,828,1655,187,27,231,232,249,233,255,4,250,2,247,139])).
% 25.11/25.25 cnf(1714,plain,
% 25.11/25.25 (~E(f4(x17141,a55,f3(f51(x17142,x17143,x17144),x17143)),f22(f4(f54(f54(f54(x17141,f3(a45,a2),x17144,x17145),f3(a45,a2),x17144,x17146),f3(a45,a2),x17144,x17147),a55,f3(f51(x17142,x17143,x17144),x17143)),a36))),
% 25.11/25.25 inference(scs_inference,[],[204,396,533,465,458,1368,674,1621,1673,1176,1668,1615,441,1639,394,389,828,1655,187,205,27,231,232,249,233,255,4,250,2,247,139,136,138,3,137,314])).
% 25.11/25.25 cnf(1718,plain,
% 25.11/25.25 (~P6(f37(f37(f22(f37(f37(f22(f37(x17181,a36),a36),a36),a36),a36),a36),a36),x17181)),
% 25.11/25.25 inference(scs_inference,[],[204,396,533,465,458,1368,674,1621,1673,1176,1668,1615,441,1639,394,389,828,1655,187,205,27,231,232,249,233,255,4,250,2,247,139,136,138,3,137,314,95,251])).
% 25.11/25.25 cnf(1728,plain,
% 25.11/25.25 (~P4(x17281,f37(f22(f37(f37(f37(f22(x17281,a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[680,249])).
% 25.11/25.25 cnf(1744,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(a42,a36),a36),a36),a36),a41)),
% 25.11/25.25 inference(scs_inference,[],[1423,680,1658,1704,442,773,1701,187,249,27,232,231,233,4,255,2,247])).
% 25.11/25.25 cnf(1747,plain,
% 25.11/25.25 (~E(f37(f37(f37(f37(f22(f37(x17471,a36),a36),a36),a36),a36),a36),x17471)),
% 25.11/25.25 inference(scs_inference,[],[1423,680,1658,1704,1319,442,394,773,1701,187,249,27,232,231,233,4,255,2,247,139])).
% 25.11/25.25 cnf(1760,plain,
% 25.11/25.25 (~P6(f37(f22(f37(f37(f37(f22(f37(x17601,a36),a36),a36),a36),a36),a36),a36),x17601)),
% 25.11/25.25 inference(scs_inference,[],[204,474,487,465,515,1423,680,1658,1704,1319,1714,1654,442,394,389,773,1701,187,205,249,27,232,231,233,4,255,2,247,139,136,138,3,137,314,251])).
% 25.11/25.25 cnf(1771,plain,
% 25.11/25.25 (~P4(x17711,f37(f37(f37(f37(f37(f22(x17711,a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[778,866,231,249])).
% 25.11/25.25 cnf(1772,plain,
% 25.11/25.25 (~P6(f37(f37(f37(f37(f37(x17721,a36),a36),a36),a36),a36),x17721)),
% 25.11/25.25 inference(rename_variables,[],[778])).
% 25.11/25.25 cnf(1774,plain,
% 25.11/25.25 (~P4(x17741,f37(f37(f37(f37(f37(x17741,a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[778,1772,866,231,249,232])).
% 25.11/25.25 cnf(1780,plain,
% 25.11/25.25 (~E(f37(f37(f37(f22(f37(f37(x17801,a36),a36),a36),a36),a36),a36),x17801)),
% 25.11/25.25 inference(scs_inference,[],[778,1772,1747,866,1744,231,249,232,233,255,4])).
% 25.11/25.25 cnf(1783,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(f37(a42,a36),a36),a36),a36),a36),a41)),
% 25.11/25.25 inference(scs_inference,[],[778,1772,1747,443,866,1744,187,231,249,232,233,255,4,2,247])).
% 25.11/25.25 cnf(1786,plain,
% 25.11/25.25 (P6(f22(f37(f22(f22(a43,a36),a36),a36),a36),f3(f51(x17861,x17862,f37(f37(a1,a36),a36)),x17862))),
% 25.11/25.25 inference(scs_inference,[],[465,778,1772,1747,443,682,866,1744,187,231,249,232,233,255,4,2,247,139])).
% 25.11/25.25 cnf(1787,plain,
% 25.11/25.25 (E(x17871,f3(f51(x17872,x17873,x17871),x17873))),
% 25.11/25.25 inference(rename_variables,[],[465])).
% 25.11/25.25 cnf(1799,plain,
% 25.11/25.25 (~P6(f37(f37(f37(f37(f37(f22(f37(x17991,a36),a36),a36),a36),a36),a36),a36),x17991)),
% 25.11/25.25 inference(scs_inference,[],[204,641,533,465,1787,545,778,1772,1747,1700,443,529,682,389,866,1744,187,205,231,249,232,233,255,4,2,247,139,136,138,3,137,314,251])).
% 25.11/25.25 cnf(1801,plain,
% 25.11/25.25 (~P6(f37(f37(f37(f37(f37(f22(f37(f37(x18011,a36),a36),a36),a36),a36),a36),a36),a36),x18011)),
% 25.11/25.25 inference(scs_inference,[],[204,641,533,465,1787,545,778,1772,1747,1700,443,529,682,389,866,1744,187,205,231,249,232,233,255,4,2,247,139,136,138,3,137,314,251,250])).
% 25.11/25.25 cnf(1815,plain,
% 25.11/25.25 (~P4(x18151,f37(f22(f37(f22(f37(f37(f22(x18151,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[724,919,231,233,249])).
% 25.11/25.25 cnf(1816,plain,
% 25.11/25.25 (~P6(f37(f22(f37(f22(f37(f37(x18161,a36),a36),a36),a36),a36),a36),x18161)),
% 25.11/25.25 inference(rename_variables,[],[724])).
% 25.11/25.25 cnf(1818,plain,
% 25.11/25.25 (~P4(x18181,f37(f22(f37(f22(f37(f37(x18181,a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[724,1816,919,231,233,249,232])).
% 25.11/25.25 cnf(1822,plain,
% 25.11/25.25 (~E(f37(f37(f22(f37(f37(f37(x18221,a36),a36),a36),a36),a36),a36),x18221)),
% 25.11/25.25 inference(scs_inference,[],[724,1816,1780,919,1783,231,233,249,232,255,4])).
% 25.11/25.25 cnf(1824,plain,
% 25.11/25.25 (E(x18241,f37(f22(x18241,a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[724,1816,1780,919,1783,185,231,233,249,232,255,4,2])).
% 25.11/25.25 cnf(1825,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(f37(f37(a42,a36),a36),a36),a36),a36),a36),a41)),
% 25.11/25.25 inference(scs_inference,[],[724,1816,1780,919,1783,185,187,231,233,249,232,255,4,2,247])).
% 25.11/25.25 cnf(1828,plain,
% 25.11/25.25 (P6(f22(f37(f22(f22(a43,a36),a36),a36),a36),f3(f51(x18281,x18282,f3(f51(x18283,x18284,f37(f37(a1,a36),a36)),x18284)),x18282))),
% 25.11/25.25 inference(scs_inference,[],[465,724,1816,1780,1786,919,1783,185,187,231,233,249,232,255,4,2,247,139])).
% 25.11/25.25 cnf(1830,plain,
% 25.11/25.25 (P2(f37(f22(a5000,a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[149,465,724,1816,1780,1786,919,1783,185,187,231,233,249,232,255,4,2,247,139,135])).
% 25.11/25.25 cnf(1833,plain,
% 25.11/25.25 (P1(f37(f22(a5000,a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[149,465,724,1816,1780,1786,919,1783,185,148,187,205,231,233,249,232,255,4,2,247,139,135,136,134])).
% 25.11/25.25 cnf(1851,plain,
% 25.11/25.25 (~P4(x18511,f37(f37(f22(f37(f22(f37(x18511,a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[735,232])).
% 25.11/25.25 cnf(1855,plain,
% 25.11/25.25 (~P4(x18551,f37(f22(f37(f37(f22(f37(f22(x18551,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[735,783,974,232,231,249])).
% 25.11/25.25 cnf(1862,plain,
% 25.11/25.25 (~E(f37(f22(f37(f37(f37(f37(x18621,a36),a36),a36),a36),a36),a36),x18621)),
% 25.11/25.25 inference(scs_inference,[],[735,783,1822,974,1825,232,231,249,233,255,4])).
% 25.11/25.25 cnf(1864,plain,
% 25.11/25.25 (E(x18641,f22(f37(x18641,a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[735,783,1822,974,1825,186,232,231,249,233,255,4,2])).
% 25.11/25.25 cnf(1865,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(f37(f37(f37(a42,a36),a36),a36),a36),a36),a36),a36),a41)),
% 25.11/25.25 inference(scs_inference,[],[735,783,1822,974,1825,186,187,232,231,249,233,255,4,2,247])).
% 25.11/25.25 cnf(1869,plain,
% 25.11/25.25 (E(x18691,f3(f51(x18692,x18693,x18691),x18693))),
% 25.11/25.25 inference(rename_variables,[],[465])).
% 25.11/25.25 cnf(1871,plain,
% 25.11/25.25 (E(f37(x18711,a36),f37(a36,x18711))),
% 25.11/25.25 inference(rename_variables,[],[382])).
% 25.11/25.25 cnf(1891,plain,
% 25.11/25.25 (~E(f37(f22(f37(a36,f3(f51(x18911,x18912,x18913),x18912)),a36),a36),x18913)),
% 25.11/25.25 inference(scs_inference,[],[204,694,533,446,465,1869,735,783,1824,1822,1828,1830,382,1871,544,1833,389,974,1825,186,187,205,232,231,249,233,255,4,2,247,139,135,136,134,138,3,137,314,5,95,251,230,89])).
% 25.11/25.25 cnf(1898,plain,
% 25.11/25.25 (~P4(x18981,f37(f37(f22(f37(f37(f37(x18981,a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[878,232])).
% 25.11/25.25 cnf(1900,plain,
% 25.11/25.25 (~P4(x19001,f37(f22(f37(f37(f37(f37(f22(x19001,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[878,883,232,249])).
% 25.11/25.25 cnf(1912,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(f37(f37(f37(f37(a42,a36),a36),a36),a36),a36),a36),a36),a36),a41)),
% 25.11/25.25 inference(scs_inference,[],[878,883,1862,1070,1865,190,187,232,249,233,231,255,4,2,247])).
% 25.11/25.25 cnf(1915,plain,
% 25.11/25.25 (P6(f22(f37(f22(f22(a43,a36),a36),a36),a36),f3(f51(x19151,x19152,f37(f37(f37(a1,a36),a36),a36)),x19152))),
% 25.11/25.25 inference(scs_inference,[],[878,883,465,1862,731,1070,1865,190,187,232,249,233,231,255,4,2,247,139])).
% 25.11/25.25 cnf(1942,plain,
% 25.11/25.25 (~P4(x19421,f37(f37(f37(f37(f37(f37(x19421,a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[968,232])).
% 25.11/25.25 cnf(1948,plain,
% 25.11/25.25 (~P4(x19481,f37(f37(f37(f37(f37(f37(f22(x19481,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[968,1124,232,231,233,249])).
% 25.11/25.25 cnf(1956,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(f37(f37(f37(f37(a42,a36),a36),a36),a36),a36),a36),a36),a36),a40)),
% 25.11/25.25 inference(scs_inference,[],[968,1891,1124,1912,172,191,232,231,233,249,255,4,2,247])).
% 25.11/25.25 cnf(1959,plain,
% 25.11/25.25 (E(x19591,f3(f51(x19592,x19593,x19591),x19593))),
% 25.11/25.25 inference(rename_variables,[],[465])).
% 25.11/25.25 cnf(1968,plain,
% 25.11/25.25 (~E(f4(x19681,a55,f3(f51(x19682,x19683,x19684),x19683)),f37(f4(f54(x19681,f3(a45,a2),x19684,x19685),a55,f3(f51(x19682,x19683,x19684),x19683)),a36))),
% 25.11/25.25 inference(scs_inference,[],[181,204,1142,928,968,465,1959,1915,1891,406,389,1124,1912,166,172,191,205,232,231,233,249,255,4,2,247,139,136,3,138,137,314])).
% 25.11/25.25 cnf(1972,plain,
% 25.11/25.25 (~E(f51(x19721,x19722,f3(f51(x19723,x19724,f3(f51(x19725,x19726,f37(a36,f3(x19727,x19722))),x19726)),x19724)),x19727)),
% 25.11/25.25 inference(scs_inference,[],[181,204,1142,928,968,465,1959,1915,1891,406,389,1124,1912,166,172,191,205,232,231,233,249,255,4,2,247,139,136,3,138,137,314,5,95])).
% 25.11/25.25 cnf(1975,plain,
% 25.11/25.25 (P5(f37(f22(f3(f51(x19751,x19752,f3(f51(x19753,x19754,a38),x19754)),x19752),a36),a36),a2)),
% 25.11/25.25 inference(scs_inference,[],[181,204,1142,928,968,465,1959,1915,1824,1891,406,1333,389,1124,1912,166,172,191,205,232,231,233,249,255,4,2,247,139,136,3,138,137,314,5,95,251,146])).
% 25.11/25.25 cnf(1990,plain,
% 25.11/25.25 (~E(f51(x19901,x19902,f3(f51(x19903,x19904,f37(a36,f3(f51(x19905,x19906,f3(x19907,x19902)),x19906))),x19904)),x19907)),
% 25.11/25.25 inference(scs_inference,[],[1972,89,95])).
% 25.11/25.25 cnf(1991,plain,
% 25.11/25.25 (~P4(x19911,f37(f37(f37(f22(f37(f22(f37(x19911,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[971,1972,89,95,232])).
% 25.11/25.25 cnf(1996,plain,
% 25.11/25.25 (~P6(f37(f37(f37(f22(f37(f22(f37(x19961,a36),a36),a36),a36),a36),a36),a36),x19961)),
% 25.11/25.25 inference(rename_variables,[],[971])).
% 25.11/25.25 cnf(2006,plain,
% 25.11/25.25 (E(x20061,f3(f51(x20062,x20063,x20061),x20063))),
% 25.11/25.25 inference(rename_variables,[],[465])).
% 25.11/25.25 cnf(2007,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(f37(f37(f37(f37(a42,a36),a36),a36),a36),a36),a36),a36),a36),f22(a40,a36))),
% 25.11/25.25 inference(scs_inference,[],[971,465,1972,387,1220,1956,1975,150,391,89,95,232,233,249,231,255,2,147,146,247])).
% 25.11/25.25 cnf(2010,plain,
% 25.11/25.25 (~E(f37(f37(f37(f22(f37(f22(f37(x20101,a36),a36),a36),a36),a36),a36),a36),x20101)),
% 25.11/25.25 inference(scs_inference,[],[971,1996,465,1972,182,387,1220,1956,1975,150,391,89,95,232,233,249,231,255,2,147,146,247,139])).
% 25.11/25.25 cnf(2020,plain,
% 25.11/25.25 (~E(f4(x20201,a55,f3(f51(x20202,x20203,x20204),x20203)),f37(f4(f54(f54(x20201,f3(a45,a2),x20204,x20205),f3(a45,a2),x20204,x20206),a55,f3(f51(x20202,x20203,x20204),x20203)),a36))),
% 25.11/25.25 inference(scs_inference,[],[181,204,1142,971,1996,465,2006,382,1968,1972,182,387,389,1220,1956,1975,150,1034,391,205,89,95,232,233,249,231,255,2,147,146,247,139,136,3,138,137,314])).
% 25.11/25.25 cnf(2033,plain,
% 25.11/25.25 (~P4(x20331,f37(f37(f22(f37(f22(f37(f37(x20331,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[977,1990,89,95,232])).
% 25.11/25.25 cnf(2036,plain,
% 25.11/25.25 (~P6(f37(f37(f22(f37(f22(f37(f37(x20361,a36),a36),a36),a36),a36),a36),a36),x20361)),
% 25.11/25.25 inference(rename_variables,[],[977])).
% 25.11/25.25 cnf(2044,plain,
% 25.11/25.25 (~E(f37(f37(f22(f37(f22(f37(f37(x20441,a36),a36),a36),a36),a36),a36),a36),x20441)),
% 25.11/25.25 inference(scs_inference,[],[977,2036,2010,1990,1264,2007,89,95,232,249,233,231,255,4])).
% 25.11/25.25 cnf(2046,plain,
% 25.11/25.25 (E(a1,f37(a43,a36))),
% 25.11/25.25 inference(scs_inference,[],[977,2036,2010,1990,1264,2007,151,89,95,232,249,233,231,255,4,2])).
% 25.11/25.25 cnf(2049,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(f37(f37(f37(f37(a42,a36),a36),a36),a36),a36),a36),a36),a36),f22(f37(f22(f22(a40,a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[977,2036,2010,1990,452,1264,2007,151,449,1975,89,95,232,249,233,231,255,4,2,147,247])).
% 25.11/25.25 cnf(2053,plain,
% 25.11/25.25 (E(x20531,f3(f51(x20532,x20533,x20531),x20533))),
% 25.11/25.25 inference(rename_variables,[],[465])).
% 25.11/25.25 cnf(2062,plain,
% 25.11/25.25 (~E(f4(x20621,a55,f3(f51(x20622,x20623,x20624),x20623)),f37(f4(f54(f54(f54(x20621,f3(a45,a2),x20624,x20625),f3(a45,a2),x20624,x20626),f3(a45,a2),x20624,x20627),a55,f3(f51(x20622,x20623,x20624),x20623)),a36))),
% 25.11/25.25 inference(scs_inference,[],[181,204,487,977,2036,465,2053,382,2010,2020,1990,452,771,385,1264,2007,151,177,449,1975,205,89,95,232,249,233,231,255,4,2,147,247,139,136,3,138,137,314])).
% 25.11/25.25 cnf(2071,plain,
% 25.11/25.25 (~P4(x20711,f37(f22(f37(f22(f37(f37(f37(x20711,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[1013,232])).
% 25.11/25.25 cnf(2082,plain,
% 25.11/25.25 (~E(f37(f22(f37(f22(f37(f37(f37(x20821,a36),a36),a36),a36),a36),a36),a36),x20821)),
% 25.11/25.25 inference(scs_inference,[],[1013,2044,461,2049,232,233,249,231,255,4])).
% 25.11/25.25 cnf(2084,plain,
% 25.11/25.25 (E(f37(x20841,a38),f37(f37(x20841,a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[1013,2044,461,2049,188,232,233,249,231,255,4,2])).
% 25.11/25.25 cnf(2085,plain,
% 25.11/25.25 (P5(f37(a36,f22(f3(f51(x20851,x20852,f3(f51(x20853,x20854,a38),x20854)),x20852),a36)),a2)),
% 25.11/25.25 inference(scs_inference,[],[1013,382,2044,461,1975,2049,188,232,233,249,231,255,4,2,146])).
% 25.11/25.25 cnf(2087,plain,
% 25.11/25.25 (P4(f37(f37(a42,a36),a36),a39)),
% 25.11/25.25 inference(scs_inference,[],[1013,382,2044,461,1975,2049,188,1133,187,232,233,249,231,255,4,2,146,247])).
% 25.11/25.25 cnf(2111,plain,
% 25.11/25.25 (~P4(x21111,f37(f22(f37(f37(f22(f37(f37(x21111,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[1016,232])).
% 25.11/25.25 cnf(2124,plain,
% 25.11/25.25 (E(f37(a38,x21241),f37(f37(x21241,a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[1016,1173,2082,1409,2087,189,232,233,249,231,255,4,2])).
% 25.11/25.25 cnf(2128,plain,
% 25.11/25.25 (E(x21281,f3(f51(x21282,x21283,x21281),x21283))),
% 25.11/25.25 inference(rename_variables,[],[465])).
% 25.11/25.25 cnf(2129,plain,
% 25.11/25.25 (P4(f37(f37(f37(a42,a36),a36),a36),a39)),
% 25.11/25.25 inference(scs_inference,[],[1016,1173,465,2082,511,1333,1409,2087,2085,189,187,232,233,249,231,255,4,2,147,146,247])).
% 25.11/25.25 cnf(2134,plain,
% 25.11/25.25 (~E(f37(f22(f37(f37(f22(f37(f37(x21341,a36),a36),a36),a36),a36),a36),a36),x21341)),
% 25.11/25.25 inference(scs_inference,[],[1016,1173,465,2082,182,511,1333,1409,2087,2085,189,187,205,232,233,249,231,255,4,2,147,146,247,136,139])).
% 25.11/25.25 cnf(2146,plain,
% 25.11/25.25 (~E(f37(f22(f37(f37(f37(f37(f22(x21461,a36),a36),a36),a36),a36),a36),a36),x21461)),
% 25.11/25.25 inference(scs_inference,[],[181,204,1016,1173,1142,465,2128,2082,2062,2084,182,511,1333,456,1409,2087,2085,189,187,205,232,233,249,231,255,4,2,147,146,247,136,139,3,138,137,314,5,27])).
% 25.11/25.25 cnf(2156,plain,
% 25.11/25.25 (~P4(x21561,f37(f22(f37(f37(f37(f37(f37(x21561,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[1213,233,232])).
% 25.11/25.25 cnf(2159,plain,
% 25.11/25.25 (~P6(f37(f22(f37(f37(f37(f37(f37(x21591,a36),a36),a36),a36),a36),a36),a36),x21591)),
% 25.11/25.25 inference(rename_variables,[],[1213])).
% 25.11/25.25 cnf(2167,plain,
% 25.11/25.25 (E(a38,f37(f37(a1,a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[1213,2134,1461,2129,184,233,232,249,231,255,4,2])).
% 25.11/25.25 cnf(2170,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(a42,a36),a36),a36),a36),a39)),
% 25.11/25.25 inference(scs_inference,[],[1213,2134,452,1461,2129,184,2085,187,233,232,249,231,255,4,2,147,247])).
% 25.11/25.25 cnf(2173,plain,
% 25.11/25.25 (~E(f37(f22(f37(f37(f37(f37(f37(x21731,a36),a36),a36),a36),a36),a36),a36),x21731)),
% 25.11/25.25 inference(scs_inference,[],[1213,2159,2134,182,452,1461,2129,184,2085,187,233,232,249,231,255,4,2,147,247,139])).
% 25.11/25.25 cnf(2183,plain,
% 25.11/25.25 (~E(f4(x21831,a55,f37(a36,x21832)),f22(f4(f54(x21831,f3(a45,a2),f37(x21832,a36),x21833),a55,f37(a36,x21832)),a36))),
% 25.11/25.25 inference(scs_inference,[],[181,204,1213,2159,1142,382,2134,2124,472,182,452,498,1461,2129,184,2085,187,205,233,232,249,231,255,4,2,147,247,139,136,138,3,137,314])).
% 25.11/25.25 cnf(2186,plain,
% 25.11/25.25 (~E(f37(f37(f22(f37(f37(f37(f22(x21861,a36),a36),a36),a36),a36),a36),a36),x21861)),
% 25.11/25.25 inference(scs_inference,[],[181,204,1213,2159,1142,382,2134,2124,472,182,452,498,1461,2129,184,2085,187,205,233,232,249,231,255,4,2,147,247,139,136,138,3,137,314,27])).
% 25.11/25.25 cnf(2193,plain,
% 25.11/25.25 (~P4(x21931,f37(f37(f37(f22(f37(f37(f37(x21931,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[1227,232])).
% 25.11/25.25 cnf(2196,plain,
% 25.11/25.25 (~P6(f37(f37(f37(f22(f37(f37(f37(x21961,a36),a36),a36),a36),a36),a36),a36),x21961)),
% 25.11/25.25 inference(rename_variables,[],[1227])).
% 25.11/25.25 cnf(2207,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(f37(a42,a36),a36),a36),a36),a36),a39)),
% 25.11/25.25 inference(scs_inference,[],[1227,2196,2173,1510,2170,193,187,232,249,233,231,255,4,2,247])).
% 25.11/25.25 cnf(2210,plain,
% 25.11/25.25 (~E(f37(f37(f37(f22(f37(f37(f37(x22101,a36),a36),a36),a36),a36),a36),a36),x22101)),
% 25.11/25.25 inference(scs_inference,[],[1227,2196,2173,182,1510,2170,193,187,232,249,233,231,255,4,2,247,139])).
% 25.11/25.25 cnf(2223,plain,
% 25.11/25.25 (~E(f37(f37(f37(f37(f37(f37(f22(x22231,a36),a36),a36),a36),a36),a36),a36),x22231)),
% 25.11/25.25 inference(scs_inference,[],[181,204,1227,2196,487,382,2173,2183,2167,182,566,1510,2170,193,187,205,232,249,233,231,255,4,2,247,139,136,138,3,137,314,27])).
% 25.11/25.25 cnf(2230,plain,
% 25.11/25.25 (~P4(x22301,f37(f37(f37(f37(f22(f37(f22(x22301,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[1671,249])).
% 25.11/25.25 cnf(2231,plain,
% 25.11/25.25 (~P6(f37(f37(f37(f37(f22(f37(x22311,a36),a36),a36),a36),a36),a36),x22311)),
% 25.11/25.25 inference(rename_variables,[],[1671])).
% 25.11/25.25 cnf(2235,plain,
% 25.11/25.25 (~P4(x22351,f37(f37(f37(f37(f22(f37(x22351,a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[1671,2231,249,233,232])).
% 25.11/25.25 cnf(2244,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(f37(f37(a42,a36),a36),a36),a36),a36),a36),a39)),
% 25.11/25.25 inference(scs_inference,[],[1671,2231,2210,1366,2207,194,187,249,233,232,231,255,4,2,247])).
% 25.11/25.25 cnf(2275,plain,
% 25.11/25.25 (~P4(x22751,f37(f37(f37(f37(x22751,a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[616,1718,249,233,232])).
% 25.11/25.25 cnf(2284,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(f37(f37(f37(a42,a36),a36),a36),a36),a36),a36),a36),a39)),
% 25.11/25.25 inference(scs_inference,[],[616,1718,2146,1559,2244,192,187,249,233,232,231,255,4,2,247])).
% 25.11/25.25 cnf(2313,plain,
% 25.11/25.25 (~P4(x23131,f37(f37(f22(f37(f37(x23131,a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[674,1673,249,233,232])).
% 25.11/25.25 cnf(2319,plain,
% 25.11/25.25 (~E(f37(f22(f37(f37(f37(f22(f37(x23191,a36),a36),a36),a36),a36),a36),a36),x23191)),
% 25.11/25.25 inference(scs_inference,[],[674,1673,2186,1774,2284,249,233,232,231,255,4])).
% 25.11/25.25 cnf(2321,plain,
% 25.11/25.25 (E(f37(x23211,a40),f37(f37(f37(f37(x23211,a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[674,1673,2186,1774,2284,197,249,233,232,231,255,4,2])).
% 25.11/25.25 cnf(2322,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(f37(f37(f37(f37(a42,a36),a36),a36),a36),a36),a36),a36),a36),a39)),
% 25.11/25.25 inference(scs_inference,[],[674,1673,2186,1774,2284,197,187,249,233,232,231,255,4,2,247])).
% 25.11/25.25 cnf(2325,plain,
% 25.11/25.25 (~E(f37(f22(f37(f22(f37(f22(f37(x23251,a36),a36),a36),a36),a36),a36),a36),x23251)),
% 25.11/25.25 inference(scs_inference,[],[833,674,1673,2186,182,1774,2284,197,187,249,233,232,231,255,4,2,247,139])).
% 25.11/25.25 cnf(2352,plain,
% 25.11/25.25 (~P4(x23521,f37(f22(f37(f37(f37(x23521,a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[680,1760,1688,249,233,231,232])).
% 25.11/25.25 cnf(2358,plain,
% 25.11/25.25 (E(f37(a40,x23581),f37(f37(f37(f37(x23581,a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[680,1760,2319,1688,2322,198,249,233,231,232,255,4,2])).
% 25.11/25.25 cnf(2359,plain,
% 25.11/25.25 (P4(f37(f37(a42,a36),a36),a43)),
% 25.11/25.25 inference(scs_inference,[],[680,1760,2319,1688,2322,198,982,187,249,233,231,232,255,4,2,247])).
% 25.11/25.25 cnf(2364,plain,
% 25.11/25.25 (P6(f22(f37(f22(f22(a43,a36),a36),a36),a36),f37(a36,f37(a1,a36)))),
% 25.11/25.25 inference(scs_inference,[],[680,1760,382,2319,682,1688,2322,198,982,187,205,249,233,231,232,255,4,2,247,136,139])).
% 25.11/25.25 cnf(2373,plain,
% 25.11/25.25 (~E(f37(f37(f37(f22(f37(f37(f22(x23731,a36),a36),a36),a36),a36),a36),a36),x23731)),
% 25.11/25.25 inference(scs_inference,[],[181,735,680,1760,382,487,2319,2321,682,819,1688,2322,198,982,187,205,249,233,231,232,255,4,2,247,136,139,138,3,137,5,27])).
% 25.11/25.25 cnf(2394,plain,
% 25.11/25.25 (E(a40,f37(f37(f37(f37(a1,a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[783,1799,2325,1728,2359,196,233,249,231,232,255,4,2])).
% 25.11/25.25 cnf(2395,plain,
% 25.11/25.25 (P4(f37(f37(f37(a42,a36),a36),a36),a43)),
% 25.11/25.25 inference(scs_inference,[],[783,1799,2325,1728,2359,196,187,233,249,231,232,255,4,2,247])).
% 25.11/25.25 cnf(2400,plain,
% 25.11/25.25 (P6(f22(f37(f22(f22(a43,a36),a36),a36),a36),f3(f51(x24001,x24002,f37(a36,f37(a1,a36))),x24002))),
% 25.11/25.25 inference(scs_inference,[],[783,1799,465,2325,2364,1728,2359,196,187,205,233,249,231,232,255,4,2,247,136,139])).
% 25.11/25.25 cnf(2408,plain,
% 25.11/25.25 (~E(f37(f22(f37(f22(f37(f37(f22(x24081,a36),a36),a36),a36),a36),a36),a36),x24081)),
% 25.11/25.25 inference(scs_inference,[],[181,878,783,1799,487,465,2325,2358,2364,781,1728,2359,196,187,205,233,249,231,232,255,4,2,247,136,139,138,3,137,27])).
% 25.11/25.25 cnf(2416,plain,
% 25.11/25.25 (~P4(x24161,f22(f37(f37(f22(f37(f22(x24161,a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[630,249])).
% 25.11/25.25 cnf(2423,plain,
% 25.11/25.25 (~P4(x24231,f37(f22(f37(f37(f37(f37(x24231,a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[883,630,1771,249,233,231,232])).
% 25.11/25.25 cnf(2427,plain,
% 25.11/25.25 (~E(f37(f37(f37(f37(f37(f22(f37(x24271,a36),a36),a36),a36),a36),a36),a36),x24271)),
% 25.11/25.25 inference(scs_inference,[],[883,630,2223,1771,2395,249,233,231,232,255,4])).
% 25.11/25.25 cnf(2430,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(a42,a36),a36),a36),a36),a43)),
% 25.11/25.25 inference(scs_inference,[],[883,630,2223,1771,2395,200,187,249,233,231,232,255,4,2,247])).
% 25.11/25.25 cnf(2443,plain,
% 25.11/25.25 (~P6(f22(f37(f37(f22(f37(f22(f37(x24431,a36),a36),a36),a36),a36),a36),a36),x24431)),
% 25.11/25.25 inference(scs_inference,[],[379,883,1128,533,630,465,2400,2394,2223,871,1771,2395,200,187,205,249,233,231,232,255,4,2,247,136,139,138,3,137,251])).
% 25.11/25.25 cnf(2465,plain,
% 25.11/25.25 (E(f37(a41,x24651),f37(f37(f37(f37(f37(x24651,a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[1173,823,2427,1818,2430,201,249,233,231,232,255,4,2])).
% 25.11/25.25 cnf(2466,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(f37(a42,a36),a36),a36),a36),a36),a43)),
% 25.11/25.25 inference(scs_inference,[],[1173,823,2427,1818,2430,201,187,249,233,231,232,255,4,2,247])).
% 25.11/25.25 cnf(2503,plain,
% 25.11/25.25 (E(a41,f37(f37(f37(f37(f37(a1,a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[1718,916,2373,1851,2466,199,249,231,233,232,255,4,2])).
% 25.11/25.25 cnf(2504,plain,
% 25.11/25.25 (P5(f22(f37(f3(f51(x25041,x25042,a38),x25042),a36),a36),a2)),
% 25.11/25.25 inference(scs_inference,[],[1718,916,1864,2373,1311,1851,2466,199,249,231,233,232,255,4,2,146])).
% 25.11/25.25 cnf(2505,plain,
% 25.11/25.25 (E(x25051,f22(f37(x25051,a36),a36))),
% 25.11/25.25 inference(rename_variables,[],[1864])).
% 25.11/25.25 cnf(2506,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(f37(f37(a42,a36),a36),a36),a36),a36),a36),a43)),
% 25.11/25.25 inference(scs_inference,[],[1718,916,1864,2373,1311,1851,2466,199,187,249,231,233,232,255,4,2,146,247])).
% 25.11/25.25 cnf(2519,plain,
% 25.11/25.25 (P4(f37(a38,a36),a2)),
% 25.11/25.25 inference(scs_inference,[],[181,545,1718,1189,487,916,1864,2505,2465,2373,1311,979,1851,2466,199,171,187,205,249,231,233,232,255,4,2,146,247,136,139,138,3,137,253])).
% 25.11/25.25 cnf(2521,plain,
% 25.11/25.25 (P6(a1,f22(f37(a38,a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[181,180,545,1718,1189,487,916,1864,2505,2465,2373,1311,979,1851,2466,199,171,187,205,249,231,233,232,255,4,2,146,247,136,139,138,3,137,253,248])).
% 25.11/25.25 cnf(2531,plain,
% 25.11/25.25 (P4(f37(a38,a36),a1)),
% 25.11/25.25 inference(scs_inference,[],[2521,253])).
% 25.11/25.25 cnf(2546,plain,
% 25.11/25.25 (E(x25461,f4(f54(x25462,x25463,x25464,x25461),x25463,x25464))),
% 25.11/25.25 inference(scs_inference,[],[1673,1073,2521,2408,1898,2506,202,253,233,231,249,232,255,4,2])).
% 25.11/25.25 cnf(2547,plain,
% 25.11/25.25 (P5(f37(f22(f3(f51(x25471,x25472,a38),x25472),a36),a36),a2)),
% 25.11/25.25 inference(scs_inference,[],[1673,1073,1824,2521,2408,1311,1898,2506,202,253,233,231,249,232,255,4,2,146])).
% 25.11/25.25 cnf(2548,plain,
% 25.11/25.25 (E(x25481,f37(f22(x25481,a36),a36))),
% 25.11/25.25 inference(rename_variables,[],[1824])).
% 25.11/25.25 cnf(2549,plain,
% 25.11/25.25 (P4(f37(f37(a38,a36),a36),a2)),
% 25.11/25.25 inference(scs_inference,[],[1673,1073,1824,2521,2408,1311,1898,2519,2506,202,187,253,233,231,249,232,255,4,2,146,247])).
% 25.11/25.25 cnf(2564,plain,
% 25.11/25.25 (~E(f37(f22(f37(f37(f22(f37(f22(x25641,a36),a36),a36),a36),a36),a36),a36),x25641)),
% 25.11/25.25 inference(scs_inference,[],[149,181,778,1673,533,1073,1824,2548,2521,2503,2408,1311,1076,1898,2519,2506,202,148,187,205,253,233,231,249,232,255,4,2,146,247,136,135,134,139,138,3,137,27])).
% 25.11/25.25 cnf(2595,plain,
% 25.11/25.25 (P5(f37(f22(f3(f51(x25951,x25952,f3(f51(x25953,x25954,f3(f51(x25955,x25956,a38),x25956)),x25954)),x25952),a36),a36),a2)),
% 25.11/25.25 inference(scs_inference,[],[180,1760,1010,1824,2564,573,1333,1379,1942,2549,231,233,232,249,255,4,248,147,146])).
% 25.11/25.25 cnf(2596,plain,
% 25.11/25.25 (E(x25961,f37(f22(x25961,a36),a36))),
% 25.11/25.25 inference(rename_variables,[],[1824])).
% 25.11/25.25 cnf(2597,plain,
% 25.11/25.25 (P4(f37(f37(a38,a36),a36),a1)),
% 25.11/25.25 inference(scs_inference,[],[180,1760,1010,1824,2564,573,1333,1379,1942,2531,2549,187,231,233,232,249,255,4,248,147,146,247])).
% 25.11/25.25 cnf(2611,plain,
% 25.11/25.25 (~E(f51(x26111,x26112,f3(f51(x26113,x26114,f4(f54(x26115,x26116,x26117,f37(a36,f3(x26118,x26112))),x26116,x26117)),x26114)),x26118)),
% 25.11/25.25 inference(scs_inference,[],[181,180,616,1760,1142,1010,1824,2596,2546,2564,573,1333,1379,1122,1942,2531,2549,187,205,231,233,232,249,255,4,248,147,146,247,136,139,138,3,137,5,95])).
% 25.11/25.25 cnf(2627,plain,
% 25.11/25.25 (~E(f51(x26271,x26272,f4(f54(x26273,x26274,x26275,f37(a36,f3(f51(x26276,x26277,f3(x26278,x26272)),x26277))),x26274,x26275)),x26278)),
% 25.11/25.25 inference(scs_inference,[],[2611,89,95])).
% 25.11/25.25 cnf(2644,plain,
% 25.11/25.25 (P4(f37(f37(f37(a38,a36),a36),a36),a1)),
% 25.11/25.25 inference(scs_inference,[],[382,1799,2443,2611,511,1604,2597,2595,2504,509,187,89,95,233,231,232,249,255,147,146,247])).
% 25.11/25.25 cnf(2647,plain,
% 25.11/25.25 (~E(f37(f37(a38,a36),a36),a1)),
% 25.11/25.25 inference(scs_inference,[],[382,1799,2443,2611,511,1604,2597,2595,2504,509,187,205,89,95,233,231,232,249,255,147,146,247,136])).
% 25.11/25.25 cnf(2657,plain,
% 25.11/25.25 (P4(x26571,f22(f37(f22(f37(f22(f37(f22(x26571,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[181,674,382,1799,1142,465,2443,2521,2046,2611,511,1225,1604,2597,2595,2504,509,187,205,89,95,233,231,232,249,255,147,146,247,136,139,138,3,137,253])).
% 25.11/25.25 cnf(2675,plain,
% 25.11/25.25 (P4(x26751,f22(f37(f22(f37(f22(f37(f22(x26751,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(rename_variables,[],[2657])).
% 25.11/25.25 cnf(2679,plain,
% 25.11/25.25 (P5(f22(f37(f3(f51(x26791,x26792,f3(f51(x26793,x26794,a38),x26794)),x26792),a36),a36),a2)),
% 25.11/25.25 inference(scs_inference,[],[1505,1864,2627,452,1333,1815,2657,2547,89,233,231,232,255,147,146])).
% 25.11/25.25 cnf(2680,plain,
% 25.11/25.25 (E(x26801,f22(f37(x26801,a36),a36))),
% 25.11/25.25 inference(rename_variables,[],[1864])).
% 25.11/25.25 cnf(2681,plain,
% 25.11/25.25 (P4(f37(f37(f37(a38,a36),a36),a36),f22(f37(f22(f37(f22(f37(f22(a1,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[1505,1864,2627,452,1333,1815,2657,2675,2644,2547,89,233,231,232,255,147,146,247])).
% 25.11/25.25 cnf(2682,plain,
% 25.11/25.25 (P4(x26821,f22(f37(f22(f37(f22(f37(f22(x26821,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(rename_variables,[],[2657])).
% 25.11/25.25 cnf(2684,plain,
% 25.11/25.25 (~E(x26841,f22(f37(f22(f37(f22(f37(f22(x26841,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[1505,1864,2627,452,1333,1815,2657,2675,2682,2644,2547,205,89,233,231,232,255,147,146,247,136])).
% 25.11/25.25 cnf(2697,plain,
% 25.11/25.25 (~E(f4(f54(x26971,x26972,x26973,f37(a36,x26974)),x26972,x26973),x26974)),
% 25.11/25.25 inference(scs_inference,[],[180,641,515,1505,487,1864,2680,2546,2627,452,1333,1275,1815,2657,2675,2682,2644,2547,205,89,233,231,232,255,147,146,247,136,139,138,3,137,6,253,5])).
% 25.11/25.25 cnf(2719,plain,
% 25.11/25.25 (~E(x27191,f22(f37(f22(f37(f22(f22(f37(x27191,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[1601,2697,2684,1855,2681,6,27,233,232,231,255,4])).
% 25.11/25.25 cnf(2720,plain,
% 25.11/25.25 (P5(f37(f22(a38,a36),a36),a2)),
% 25.11/25.25 inference(scs_inference,[],[1601,1824,2697,2684,1536,1855,2681,6,27,233,232,231,255,4,146])).
% 25.11/25.25 cnf(2721,plain,
% 25.11/25.25 (E(x27211,f37(f22(x27211,a36),a36))),
% 25.11/25.25 inference(rename_variables,[],[1824])).
% 25.11/25.25 cnf(2722,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(a38,a36),a36),a36),a36),f22(f37(f22(f37(f22(f37(f22(a1,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[1601,1824,2697,2684,1536,1855,2681,187,6,27,233,232,231,255,4,146,247])).
% 25.11/25.25 cnf(2727,plain,
% 25.11/25.25 (P6(a2,f37(f22(f3(f51(x27271,x27272,a38),x27272),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[474,1601,1824,2721,2697,2684,1536,1855,2681,187,205,6,27,233,232,231,255,4,146,247,136,139])).
% 25.11/25.25 cnf(2757,plain,
% 25.11/25.25 (~E(x27571,f22(f37(f22(f22(f37(f22(f37(x27571,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[1612,2719,1900,2722,27,233,232,231,255,4])).
% 25.11/25.25 cnf(2760,plain,
% 25.11/25.25 (P5(f37(a36,f22(a38,a36)),a2)),
% 25.11/25.25 inference(scs_inference,[],[382,1612,2719,624,1311,1900,2722,2720,27,233,232,231,255,4,147,146])).
% 25.11/25.25 cnf(2762,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(f37(a38,a36),a36),a36),a36),a36),f22(f37(f22(f37(f22(f37(f22(a1,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[382,1612,2719,624,1311,1900,2722,2720,187,27,233,232,231,255,4,147,146,247])).
% 25.11/25.25 cnf(2795,plain,
% 25.11/25.25 (P5(f3(f51(x27951,x27952,f37(a36,f22(a38,a36))),x27952),a2)),
% 25.11/25.25 inference(scs_inference,[],[1064,465,2757,573,1311,1948,2762,2760,233,232,231,27,255,4,147,146])).
% 25.11/25.25 cnf(2797,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(f37(f37(a38,a36),a36),a36),a36),a36),a36),f22(f37(f22(f37(f22(f37(f22(a1,a36),a36),a36),a36),a36),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[1064,465,2757,573,1311,1948,2762,2760,187,233,232,231,27,255,4,147,146,247])).
% 25.11/25.25 cnf(2827,plain,
% 25.11/25.25 (E(x28271,f22(f37(x28271,a36),a36))),
% 25.11/25.25 inference(rename_variables,[],[1864])).
% 25.11/25.25 cnf(2828,plain,
% 25.11/25.25 (P4(f37(f37(a1,a36),a36),f22(a43,a36))),
% 25.11/25.25 inference(scs_inference,[],[1110,1864,511,1379,1991,2797,2795,469,187,232,233,231,255,147,146,247])).
% 25.11/25.25 cnf(2840,plain,
% 25.11/25.25 (P4(f37(f3(f51(x28401,x28402,a38),x28402),a36),a2)),
% 25.11/25.25 inference(scs_inference,[],[180,204,474,928,1110,1864,2827,432,511,1379,461,1991,2797,2795,2657,469,187,205,232,233,231,255,147,146,247,136,139,138,3,137,253])).
% 25.11/25.25 cnf(2842,plain,
% 25.11/25.25 (P6(a1,f22(f37(f3(f51(x28421,x28422,a38),x28422),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[180,204,474,928,1110,1864,2827,432,511,1379,461,1991,2797,2795,2657,469,187,205,232,233,231,255,147,146,247,136,139,138,3,137,253,248])).
% 25.11/25.25 cnf(2863,plain,
% 25.11/25.25 (P5(f37(f22(f37(a36,f22(f3(f51(x28631,x28632,f3(f51(x28633,x28634,a38),x28634)),x28632),a36)),a36),a36),a2)),
% 25.11/25.25 inference(scs_inference,[],[630,1824,2842,452,1643,2085,2828,2720,253,232,233,231,255,147,146])).
% 25.11/25.25 cnf(2865,plain,
% 25.11/25.25 (P4(f37(f37(f37(a1,a36),a36),a36),f22(a43,a36))),
% 25.11/25.25 inference(scs_inference,[],[630,1824,2842,452,1643,2085,2828,2720,187,253,232,233,231,255,147,146,247])).
% 25.11/25.25 cnf(2898,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(a1,a36),a36),a36),a36),f22(a43,a36))),
% 25.11/25.25 inference(scs_inference,[],[823,465,387,2071,2865,2679,2795,187,232,233,231,255,147,146,247])).
% 25.11/25.25 cnf(2930,plain,
% 25.11/25.25 (P5(f22(f37(a38,a36),a36),a2)),
% 25.11/25.25 inference(scs_inference,[],[916,1864,670,1536,2033,2898,2760,233,232,231,255,147,146])).
% 25.11/25.25 cnf(2931,plain,
% 25.11/25.25 (E(x29311,f22(f37(x29311,a36),a36))),
% 25.11/25.25 inference(rename_variables,[],[1864])).
% 25.11/25.25 cnf(2932,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(f37(a1,a36),a36),a36),a36),a36),f22(a43,a36))),
% 25.11/25.25 inference(scs_inference,[],[916,1864,670,1536,2033,2898,2760,187,233,232,231,255,147,146,247])).
% 25.11/25.25 cnf(2944,plain,
% 25.11/25.25 (P4(f37(f3(f51(x29441,x29442,f3(f51(x29443,x29444,a38),x29444)),x29442),a36),a2)),
% 25.11/25.25 inference(scs_inference,[],[180,204,1227,641,916,1864,2931,435,670,721,1536,2033,2898,2840,2760,187,205,233,232,231,255,147,146,247,136,139,138,3,137,253])).
% 25.11/25.25 cnf(2946,plain,
% 25.11/25.25 (P6(a1,f22(f37(f3(f51(x29461,x29462,f3(f51(x29463,x29464,a38),x29464)),x29462),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[180,204,1227,641,916,1864,2931,435,670,721,1536,2033,2898,2840,2760,187,205,233,232,231,255,147,146,247,136,139,138,3,137,253,248])).
% 25.11/25.25 cnf(2955,plain,
% 25.11/25.25 (P4(f37(f3(f51(x29551,x29552,f3(f51(x29553,x29554,a38),x29554)),x29552),a36),a1)),
% 25.11/25.25 inference(scs_inference,[],[2946,253])).
% 25.11/25.25 cnf(2967,plain,
% 25.11/25.25 (P5(f37(f22(f22(f37(a38,a36),a36),a36),a36),a2)),
% 25.11/25.25 inference(scs_inference,[],[1073,1824,2946,624,1333,2156,2932,2930,253,233,232,231,255,147,146])).
% 25.11/25.25 cnf(2969,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(f37(f37(a1,a36),a36),a36),a36),a36),a36),f22(a43,a36))),
% 25.11/25.25 inference(scs_inference,[],[1073,1824,2946,624,1333,2156,2932,2930,187,253,233,232,231,255,147,146,247])).
% 25.11/25.25 cnf(3000,plain,
% 25.11/25.25 (P5(f37(a36,f22(f22(f37(a38,a36),a36),a36)),a2)),
% 25.11/25.25 inference(scs_inference,[],[382,1230,573,2111,2969,2967,232,233,231,255,147,146])).
% 25.11/25.25 cnf(3002,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(f37(f37(f37(a1,a36),a36),a36),a36),a36),a36),a36),f22(a43,a36))),
% 25.11/25.25 inference(scs_inference,[],[382,1230,573,2111,2969,2967,187,232,233,231,255,147,146,247])).
% 25.11/25.25 cnf(3032,plain,
% 25.11/25.25 (E(x30321,f22(f37(x30321,a36),a36))),
% 25.11/25.25 inference(rename_variables,[],[1864])).
% 25.11/25.25 cnf(3033,plain,
% 25.11/25.25 (P4(f37(f37(f37(f37(f37(f37(f37(f37(a1,a36),a36),a36),a36),a36),a36),a36),a36),f22(a43,a36))),
% 25.11/25.25 inference(scs_inference,[],[1272,1864,511,2193,2085,3002,3000,187,232,233,231,255,147,146,247])).
% 25.11/25.25 cnf(3045,plain,
% 25.11/25.25 (P4(f37(f3(f51(x30451,x30452,f3(f51(x30453,x30454,f3(f51(x30455,x30456,a38),x30456)),x30454)),x30452),a36),a2)),
% 25.11/25.25 inference(scs_inference,[],[181,204,680,694,1272,1864,3032,438,511,866,2193,2085,3002,3000,1079,187,205,232,233,231,255,147,146,247,136,139,3,138,137,253])).
% 25.11/25.25 cnf(3047,plain,
% 25.11/25.25 (P6(a1,f22(f37(f3(f51(x30471,x30472,f3(f51(x30473,x30474,f3(f51(x30475,x30476,a38),x30476)),x30474)),x30472),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[181,180,204,680,694,1272,1864,3032,438,511,866,2193,2085,3002,3000,1079,187,205,232,233,231,255,147,146,247,136,139,3,138,137,253,248])).
% 25.11/25.25 cnf(3056,plain,
% 25.11/25.25 (P4(f37(f3(f51(x30561,x30562,f3(f51(x30563,x30564,f3(f51(x30565,x30566,a38),x30566)),x30564)),x30562),a36),a1)),
% 25.11/25.25 inference(scs_inference,[],[3047,253])).
% 25.11/25.25 cnf(3070,plain,
% 25.11/25.25 (P4(f37(f37(f3(f51(x30701,x30702,f3(f51(x30703,x30704,f3(f51(x30705,x30706,a38),x30706)),x30704)),x30702),a36),a36),a2)),
% 25.11/25.25 inference(scs_inference,[],[382,1324,3047,452,2230,3033,3045,2863,3000,187,253,232,231,233,255,147,146,247])).
% 25.11/25.25 cnf(3104,plain,
% 25.11/25.25 (P5(f3(f51(x31041,x31042,f22(f37(a38,a36),a36)),x31042),a2)),
% 25.11/25.25 inference(scs_inference,[],[180,1375,465,387,2275,3070,2930,2760,232,255,233,231,248,147,146])).
% 25.11/25.25 cnf(3111,plain,
% 25.11/25.25 (P6(a2,f37(a36,f22(f3(f51(x31111,x31112,a38),x31112),a36)))),
% 25.11/25.25 inference(scs_inference,[],[180,382,1375,465,2727,387,2275,3056,3070,2930,2760,187,205,232,255,233,231,248,147,146,247,136,139])).
% 25.11/25.25 cnf(3140,plain,
% 25.11/25.25 (P5(f22(f37(f3(f51(x31401,x31402,f22(f37(a38,a36),a36)),x31402),a36),a36),a2)),
% 25.11/25.25 inference(scs_inference,[],[180,1463,1864,3111,729,2235,3104,2644,232,231,233,255,248,147,146])).
% 25.11/25.25 cnf(3141,plain,
% 25.11/25.25 (E(x31411,f22(f37(x31411,a36),a36))),
% 25.11/25.25 inference(rename_variables,[],[1864])).
% 25.11/25.25 cnf(3142,plain,
% 25.11/25.25 (P4(f37(f37(f3(f51(x31421,x31422,f3(f51(x31423,x31424,a38),x31424)),x31422),a36),a36),a2)),
% 25.11/25.25 inference(scs_inference,[],[180,1463,1864,3111,729,2235,3104,2944,2644,187,232,231,233,255,248,147,146,247])).
% 25.11/25.25 cnf(3149,plain,
% 25.11/25.25 (P6(a2,f22(f37(f3(f51(x31491,x31492,f3(f51(x31493,x31494,a42),x31494)),x31492),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[180,1463,1864,3141,1241,3111,2647,729,2235,3104,2944,2644,187,205,232,231,233,255,248,147,146,247,237,136,139])).
% 25.11/25.25 cnf(3156,plain,
% 25.11/25.25 (P4(f37(f3(f51(x31561,x31562,f3(f51(x31563,x31564,a42),x31564)),x31562),a36),a2)),
% 25.11/25.25 inference(scs_inference,[],[180,204,878,1463,1864,3141,1241,441,3111,2647,1275,729,2235,3104,2944,2549,2644,187,205,232,231,233,255,248,147,146,247,237,136,139,3,138,137,253])).
% 25.11/25.25 cnf(3178,plain,
% 25.11/25.25 (P5(f37(f22(f22(f37(f3(f51(x31781,x31782,f22(f37(a38,a36),a36)),x31782),a36),a36),a36),a36),a2)),
% 25.11/25.25 inference(scs_inference,[],[180,1514,1824,3149,670,2352,3140,3142,2504,232,255,231,233,248,147,146])).
% 25.11/25.25 cnf(3179,plain,
% 25.11/25.25 (E(x31791,f37(f22(x31791,a36),a36))),
% 25.11/25.25 inference(rename_variables,[],[1824])).
% 25.11/25.25 cnf(3180,plain,
% 25.11/25.25 (P4(f37(f37(f3(f51(x31801,x31802,f3(f51(x31803,x31804,a38),x31804)),x31802),a36),a36),a1)),
% 25.11/25.25 inference(scs_inference,[],[180,1514,1824,3149,670,2352,2955,3140,3142,2504,187,232,255,231,233,248,147,146,247])).
% 25.11/25.25 cnf(3183,plain,
% 25.11/25.25 (~E(f37(f3(f51(x31831,x31832,f3(f51(x31833,x31834,a38),x31834)),x31832),a36),a1)),
% 25.11/25.25 inference(scs_inference,[],[180,1514,1824,3149,670,2352,2955,3140,3142,2504,187,205,232,255,231,233,248,147,146,247,136])).
% 25.11/25.25 cnf(3185,plain,
% 25.11/25.25 (P6(a2,f37(f22(f3(f51(x31851,x31852,a42),x31852),a36),a36))),
% 25.11/25.25 inference(scs_inference,[],[180,1514,1824,3179,1189,3149,670,2352,2955,3140,3142,2504,187,205,232,255,231,233,248,147,146,247,136,139])).
% 25.11/25.25 cnf(3192,plain,
% 25.11/25.25 (~E(a2,a1)),
% 25.11/25.25 inference(scs_inference,[],[181,180,204,883,1514,1824,3179,1189,417,3149,1070,670,2352,2955,3140,3142,2504,152,187,205,232,255,231,233,248,147,146,247,136,139,3,138,137,96])).
% 25.11/25.25 cnf(3193,plain,
% 25.11/25.25 (P4(f37(f3(f51(x31931,x31932,f3(f51(x31933,x31934,a42),x31934)),x31932),a36),a1)),
% 25.11/25.25 inference(scs_inference,[],[181,180,204,883,1514,1824,3179,1189,417,3149,1070,670,2352,2955,3140,3142,2504,152,187,205,232,255,231,233,248,147,146,247,136,139,3,138,137,96,253])).
% 25.11/25.25 cnf(3197,plain,
% 25.11/25.25 (~P6(a2,a1)),
% 25.11/25.25 inference(scs_inference,[],[181,180,204,883,1514,1824,3179,1189,417,3149,1070,670,2352,2955,3140,3142,2504,152,187,205,232,255,231,233,248,147,146,247,136,139,3,138,137,96,253,230,237])).
% 25.11/25.25 cnf(3219,plain,
% 25.11/25.25 (P4(f37(f37(f3(f51(x32191,x32192,f3(f51(x32193,x32194,a42),x32194)),x32192),a36),a36),a2)),
% 25.11/25.25 inference(scs_inference,[],[180,382,1553,3185,624,2313,3156,3180,3178,2547,187,232,233,255,231,248,147,146,247])).
% 25.11/25.25 cnf(3234,plain,
% 25.11/25.25 (~E(a2,a36)),
% 25.11/25.25 inference(scs_inference,[],[181,180,204,968,382,474,1553,418,3197,3185,3183,1124,624,2313,3156,3180,3178,2547,153,187,205,232,233,255,231,248,147,146,247,237,136,139,3,138,137,858,96])).
% 25.11/25.25 cnf(3270,plain,
% 25.11/25.25 (~E(a2,a38)),
% 25.11/25.25 inference(scs_inference,[],[180,204,833,641,465,1697,419,3197,461,573,2416,3193,3219,3140,2720,187,205,232,231,233,255,248,147,146,247,136,139,3,138,137,713,96])).
% 25.11/25.25 cnf(3273,plain,
% 25.11/25.25 (P4(a38,a2)),
% 25.11/25.25 inference(scs_inference,[],[181,180,204,833,641,465,1697,419,3197,461,573,2416,3193,3219,3140,2720,187,205,232,231,233,255,248,147,146,247,136,139,3,138,137,713,96,230,236])).
% 25.11/25.25 cnf(3307,plain,
% 25.11/25.25 ($false),
% 25.11/25.25 inference(scs_inference,[],[181,180,204,971,694,1864,1801,420,3273,3197,3270,3192,3234,389,511,2423,2679,161,469,3104,205,232,231,255,233,147,146,247,136,139,3,138,137,239]),
% 25.11/25.25 ['proof']).
% 25.11/25.25 % SZS output end Proof
% 25.11/25.25 % Total time :24.470000s
%------------------------------------------------------------------------------