%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET763+4 : TPTP v8.2.0. Bugfixed v2.2.1.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n018.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 14:22:24 EDT 2024
% Result : Theorem 58.77s 58.85s
% Output : CNFRefutation 58.94s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.14 % Problem : SET763+4 : TPTP v8.2.0. Bugfixed v2.2.1.
% 0.09/0.14 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.14/0.35 % Computer : n018.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Sun Jun 23 13:03:09 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.22/0.59 start to proof:theBenchmark
% 58.77/58.84 %-------------------------------------------
% 58.77/58.84 % File :CSE---1.7
% 58.77/58.84 % Problem :theBenchmark
% 58.77/58.84 % Transform :cnf
% 58.77/58.84 % Format :tptp:raw
% 58.77/58.84 % Command :java -jar mcs_scs.jar %d %s
% 58.77/58.84
% 58.77/58.84 % Result :Theorem 58.160000s
% 58.77/58.84 % Output :CNFRefutation 58.160000s
% 58.77/58.84 %-------------------------------------------
% 58.77/58.85 %--------------------------------------------------------------------------
% 58.77/58.85 % File : SET763+4 : TPTP v8.2.0. Bugfixed v2.2.1.
% 58.77/58.85 % Domain : Set Theory (Mappings)
% 58.77/58.85 % Problem : If the image of X is empty then X is empty
% 58.77/58.85 % Version : [Pas99] axioms.
% 58.77/58.85 % English :
% 58.77/58.85
% 58.77/58.85 % Refs : [Pas99] Pastre (1999), Email to G. Sutcliffe
% 58.77/58.85 % Source : [Pas99]
% 58.77/58.85 % Names :
% 58.77/58.85
% 58.77/58.85 % Status : Theorem
% 58.77/58.85 % Rating : 0.47 v8.1.0, 0.44 v7.5.0, 0.47 v7.4.0, 0.50 v7.3.0, 0.38 v7.2.0, 0.34 v7.1.0, 0.35 v7.0.0, 0.40 v6.4.0, 0.42 v6.3.0, 0.46 v6.2.0, 0.52 v6.1.0, 0.60 v6.0.0, 0.70 v5.5.0, 0.59 v5.4.0, 0.57 v5.3.0, 0.59 v5.2.0, 0.50 v5.1.0, 0.52 v5.0.0, 0.54 v4.1.0, 0.52 v4.0.1, 0.48 v4.0.0, 0.46 v3.7.0, 0.50 v3.5.0, 0.53 v3.4.0, 0.58 v3.3.0, 0.50 v3.2.0, 0.64 v3.1.0, 0.56 v2.7.0, 0.50 v2.6.0, 0.57 v2.5.0, 0.62 v2.4.0, 0.50 v2.3.0, 0.33 v2.2.1
% 58.77/58.85 % Syntax : Number of formulae : 29 ( 1 unt; 0 def)
% 58.77/58.85 % Number of atoms : 132 ( 6 equ)
% 58.77/58.85 % Maximal formula atoms : 11 ( 4 avg)
% 58.77/58.85 % Number of connectives : 105 ( 2 ~; 2 |; 52 &)
% 58.77/58.85 % ( 30 <=>; 19 =>; 0 <=; 0 <~>)
% 58.77/58.85 % Maximal formula depth : 19 ( 9 avg)
% 58.77/58.85 % Maximal term depth : 2 ( 1 avg)
% 58.77/58.85 % Number of predicates : 16 ( 15 usr; 0 prp; 2-6 aty)
% 58.77/58.85 % Number of functors : 15 ( 15 usr; 1 con; 0-5 aty)
% 58.77/58.85 % Number of variables : 137 ( 128 !; 9 ?)
% 58.77/58.85 % SPC : FOF_THM_RFO_SEQ
% 58.77/58.85
% 58.77/58.85 % Comments :
% 58.77/58.85 % Bugfixes : v2.2.1 - Bugfixes in SET006+1.ax.
% 58.77/58.85 %--------------------------------------------------------------------------
% 58.77/58.85 %----Include set theory definitions
% 58.77/58.85 include('Axioms/SET006+0.ax').
% 58.77/58.85 %----Include mappings axioms
% 58.77/58.85 include('Axioms/SET006+1.ax').
% 58.77/58.85 %--------------------------------------------------------------------------
% 58.77/58.85 fof(thIIa13,conjecture,
% 58.77/58.85 ! [F,A,B,X] :
% 58.77/58.85 ( ( maps(F,A,B)
% 58.77/58.85 & subset(X,A)
% 58.77/58.85 & equal_set(image2(F,X),empty_set) )
% 58.77/58.85 => equal_set(X,empty_set) ) ).
% 58.77/58.85
% 58.77/58.85 %--------------------------------------------------------------------------
% 58.77/58.85 %-------------------------------------------
% 58.77/58.85 % Proof found
% 58.77/58.85 % SZS status Theorem for theBenchmark
% 58.77/58.85 % SZS output start Proof
% 58.77/58.86 %ClaNum:390(EqnAxiom:252)
% 58.77/58.86 %VarNum:1641(SingletonVarNum:571)
% 58.77/58.86 %MaxLitNum:9
% 58.77/58.86 %MaxfuncDepth:1
% 58.77/58.86 %SharedTerms:10
% 58.77/58.86 %goalClause: 253 254 255 256
% 58.77/58.86 %singleGoalClaCount:4
% 58.77/58.86 [253]P1(a1,a2)
% 58.77/58.86 [255]P7(a3,a2,a41)
% 58.77/58.86 [256]~P2(a1,a4)
% 58.77/58.86 [254]P2(f42(a3,a1),a4)
% 58.77/58.86 [257]~P13(x2571,a4)
% 58.77/58.86 [260]~P2(x2602,x2601)+P1(x2601,x2602)
% 58.77/58.86 [261]~P2(x2611,x2612)+P1(x2611,x2612)
% 58.77/58.86 [258]~E(x2581,x2582)+P13(x2581,f49(x2582))
% 58.77/58.86 [259]E(x2591,x2592)+~P13(x2591,f49(x2592))
% 58.77/58.86 [262]~P1(x2621,x2622)+P13(x2621,f50(x2622))
% 58.77/58.86 [265]P1(x2651,x2652)+~P13(x2651,f50(x2652))
% 58.77/58.86 [266]P1(x2661,x2662)+P13(f7(x2661,x2662),x2661)
% 58.77/58.86 [267]P8(x2671,x2672)+P13(f8(x2671,x2672),x2672)
% 58.77/58.86 [270]P13(f18(x2701,x2702),x2702)+P13(x2701,f56(x2702))
% 58.77/58.86 [276]~P13(x2761,f59(x2762))+P13(x2761,f19(x2761,x2762))
% 58.77/58.86 [277]~P13(x2771,f59(x2772))+P13(f19(x2771,x2772),x2772)
% 58.77/58.86 [282]P1(x2821,x2822)+~P13(f7(x2821,x2822),x2822)
% 58.77/58.86 [283]~P13(x2831,f18(x2831,x2832))+P13(x2831,f56(x2832))
% 58.77/58.86 [296]P8(x2961,x2962)+~P3(x2961,f8(x2961,x2962),f8(x2961,x2962))
% 58.77/58.86 [288]~P14(x2881,x2882,x2883)+P9(x2881,x2882,x2883)
% 58.77/58.86 [289]~P14(x2891,x2892,x2893)+P15(x2891,x2892,x2893)
% 58.77/58.86 [263]~E(x2631,x2633)+P13(x2631,f57(x2632,x2633))
% 58.77/58.86 [264]~E(x2641,x2642)+P13(x2641,f57(x2642,x2643))
% 58.77/58.86 [271]~P13(x2711,x2713)+P13(x2711,f58(x2712,x2713))
% 58.77/58.86 [272]~P13(x2721,x2722)+P13(x2721,f58(x2722,x2723))
% 58.77/58.86 [279]P13(x2791,x2792)+~P13(x2791,f51(x2793,x2792))
% 58.77/58.86 [280]P13(x2801,x2802)+~P13(x2801,f51(x2802,x2803))
% 58.77/58.86 [281]P13(x2811,x2812)+~P13(x2811,f5(x2812,x2813))
% 58.77/58.86 [285]~P13(x2851,x2852)+~P13(x2851,f5(x2853,x2852))
% 58.77/58.86 [292]P9(x2921,x2922,x2923)+P13(f16(x2921,x2922,x2923),x2922)
% 58.77/58.86 [293]P9(x2931,x2932,x2933)+P13(f17(x2931,x2932,x2933),x2932)
% 58.77/58.86 [294]P9(x2941,x2942,x2943)+P13(f20(x2941,x2942,x2943),x2943)
% 58.77/58.86 [295]P15(x2951,x2952,x2953)+P13(f21(x2951,x2952,x2953),x2953)
% 58.77/58.86 [297]~P13(x2973,f42(x2971,x2972))+P13(f23(x2971,x2972,x2973),x2972)
% 58.77/58.86 [298]~P13(x2983,f53(x2981,x2982))+P13(f26(x2981,x2982,x2983),x2982)
% 58.77/58.86 [301]P3(x3011,x3012,f26(x3011,x3013,x3012))+~P13(x3012,f53(x3011,x3013))
% 58.77/58.86 [302]P3(x3021,f23(x3021,x3022,x3023),x3023)+~P13(x3023,f42(x3021,x3022))
% 58.77/58.86 [303]P9(x3031,x3032,x3033)+~E(f17(x3031,x3032,x3033),f16(x3031,x3032,x3033))
% 58.77/58.86 [311]P9(x3111,x3112,x3113)+P3(x3111,f16(x3111,x3112,x3113),f20(x3111,x3112,x3113))
% 58.77/58.86 [312]P9(x3121,x3122,x3123)+P3(x3121,f17(x3121,x3122,x3123),f20(x3121,x3122,x3123))
% 58.77/58.86 [299]P13(x2991,x2992)+~P13(x2991,f52(x2993,x2994,x2992))
% 58.77/58.86 [300]P13(x3001,x3002)+~P13(x3001,f55(x3003,x3004,x3002))
% 58.77/58.86 [333]~P13(x3334,f52(x3331,x3332,x3333))+P13(f27(x3331,x3332,x3333,x3334),x3332)
% 58.77/58.86 [334]~P13(x3344,f55(x3341,x3342,x3343))+P13(f28(x3341,x3342,x3343,x3344),x3342)
% 58.77/58.86 [335]P3(x3351,x3352,f28(x3351,x3353,x3354,x3352))+~P13(x3352,f55(x3351,x3353,x3354))
% 58.77/58.86 [336]P3(x3361,f27(x3361,x3362,x3363,x3364),x3364)+~P13(x3364,f52(x3361,x3362,x3363))
% 58.77/58.86 [337]P4(x3371,x3372,x3373,x3374)+P13(f9(x3371,x3372,x3373,x3374),x3373)
% 58.77/58.86 [338]P4(x3381,x3382,x3383,x3384)+P13(f14(x3381,x3382,x3383,x3384),x3384)
% 58.77/58.86 [339]P4(x3391,x3392,x3393,x3394)+P13(f15(x3391,x3392,x3393,x3394),x3394)
% 58.77/58.86 [340]P11(x3401,x3402,x3403,x3404)+P13(f24(x3401,x3402,x3403,x3404),x3403)
% 58.77/58.86 [341]P11(x3411,x3412,x3413,x3414)+P13(f25(x3411,x3412,x3413,x3414),x3414)
% 58.77/58.86 [342]P4(x3421,x3422,x3423,x3424)+~E(f15(x3421,x3422,x3423,x3424),f14(x3421,x3422,x3423,x3424))
% 58.77/58.86 [343]P4(x3431,x3432,x3433,x3434)+P3(x3432,f9(x3431,x3432,x3433,x3434),f15(x3431,x3432,x3433,x3434))
% 58.77/58.86 [344]P4(x3441,x3442,x3443,x3444)+P3(x3441,f9(x3441,x3442,x3443,x3444),f14(x3441,x3442,x3443,x3444))
% 58.77/58.86 [345]P7(x3451,x3452,x3453)+~P12(x3451,x3452,x3454,x3453,x3455)
% 58.77/58.86 [346]P14(x3461,x3462,x3463)+~P12(x3461,x3462,x3464,x3463,x3465)
% 58.77/58.86 [354]P10(x3541,x3542,x3543,x3544,x3545)+P13(f29(x3541,x3542,x3543,x3544,x3545),x3542)
% 58.77/58.86 [355]P10(x3551,x3552,x3553,x3554,x3555)+P13(f30(x3551,x3552,x3553,x3554,x3555),x3554)
% 58.77/58.86 [356]P10(x3561,x3562,x3563,x3564,x3565)+P13(f31(x3561,x3562,x3563,x3564,x3565),x3562)
% 58.77/58.86 [357]P10(x3571,x3572,x3573,x3574,x3575)+P13(f32(x3571,x3572,x3573,x3574,x3575),x3574)
% 58.77/58.86 [358]P5(x3581,x3582,x3583,x3584,x3585)+P13(f33(x3581,x3582,x3583,x3584,x3585),x3582)
% 58.77/58.86 [359]P5(x3591,x3592,x3593,x3594,x3595)+P13(f34(x3591,x3592,x3593,x3594,x3595),x3594)
% 58.77/58.86 [360]P5(x3601,x3602,x3603,x3604,x3605)+P13(f35(x3601,x3602,x3603,x3604,x3605),x3602)
% 58.77/58.86 [361]P5(x3611,x3612,x3613,x3614,x3615)+P13(f36(x3611,x3612,x3613,x3614,x3615),x3614)
% 58.77/58.86 [366]P10(x3661,x3662,x3663,x3664,x3665)+P3(x3663,f29(x3661,x3662,x3663,x3664,x3665),f31(x3661,x3662,x3663,x3664,x3665))
% 58.77/58.86 [367]P10(x3671,x3672,x3673,x3674,x3675)+P3(x3671,f29(x3671,x3672,x3673,x3674,x3675),f30(x3671,x3672,x3673,x3674,x3675))
% 58.77/58.86 [368]P10(x3681,x3682,x3683,x3684,x3685)+P3(x3681,f31(x3681,x3682,x3683,x3684,x3685),f32(x3681,x3682,x3683,x3684,x3685))
% 58.77/58.86 [369]P5(x3691,x3692,x3693,x3694,x3695)+P3(x3693,f33(x3691,x3692,x3693,x3694,x3695),f35(x3691,x3692,x3693,x3694,x3695))
% 58.77/58.86 [370]P5(x3701,x3702,x3703,x3704,x3705)+P3(x3701,f33(x3701,x3702,x3703,x3704,x3705),f34(x3701,x3702,x3703,x3704,x3705))
% 58.77/58.86 [371]P5(x3711,x3712,x3713,x3714,x3715)+P3(x3711,f35(x3711,x3712,x3713,x3714,x3715),f36(x3711,x3712,x3713,x3714,x3715))
% 58.77/58.86 [374]P10(x3741,x3742,x3743,x3744,x3745)+~P3(x3745,f30(x3741,x3742,x3743,x3744,x3745),f32(x3741,x3742,x3743,x3744,x3745))
% 58.77/58.86 [375]P5(x3751,x3752,x3753,x3754,x3755)+~P3(x3755,f36(x3751,x3752,x3753,x3754,x3755),f34(x3751,x3752,x3753,x3754,x3755))
% 58.77/58.86 [379]P6(x3791,x3792,x3793,x3794,x3795,x3796)+P13(f10(x3791,x3792,x3793,x3794,x3795,x3796),x3794)
% 58.77/58.86 [380]P6(x3801,x3802,x3803,x3804,x3805,x3806)+P13(f11(x3801,x3802,x3803,x3804,x3805,x3806),x3806)
% 58.77/58.86 [269]~P1(x2692,x2691)+~P1(x2691,x2692)+P2(x2691,x2692)
% 58.77/58.86 [268]~P13(x2681,x2683)+P13(x2681,x2682)+~P1(x2683,x2682)
% 58.77/58.86 [287]~P8(x2871,x2873)+P3(x2871,x2872,x2872)+~P13(x2872,x2873)
% 58.77/58.86 [304]~P9(x3041,x3042,x3043)+~P15(x3041,x3042,x3043)+P14(x3041,x3042,x3043)
% 58.77/58.86 [273]~P13(x2733,x2732)+~P13(x2731,x2733)+P13(x2731,f59(x2732))
% 58.77/58.86 [274]E(x2741,x2742)+E(x2741,x2743)+~P13(x2741,f57(x2743,x2742))
% 58.77/58.86 [275]P13(x2751,x2752)+~P13(x2752,x2753)+~P13(x2751,f56(x2753))
% 58.77/58.86 [278]~P13(x2781,x2783)+P13(x2781,x2782)+P13(x2781,f5(x2783,x2782))
% 58.77/58.86 [284]~P13(x2841,x2843)+~P13(x2841,x2842)+P13(x2841,f51(x2842,x2843))
% 58.77/58.86 [286]P13(x2861,x2862)+P13(x2861,x2863)+~P13(x2861,f58(x2863,x2862))
% 58.77/58.86 [308]P7(x3081,x3082,x3083)+P13(f43(x3081,x3082,x3083),x3082)+P13(f45(x3081,x3082,x3083),x3082)
% 58.77/58.86 [309]P7(x3091,x3092,x3093)+P13(f43(x3091,x3092,x3093),x3092)+P13(f46(x3091,x3092,x3093),x3093)
% 58.77/58.86 [310]P7(x3101,x3102,x3103)+P13(f43(x3101,x3102,x3103),x3102)+P13(f47(x3101,x3102,x3103),x3103)
% 58.77/58.86 [316]P7(x3161,x3162,x3163)+P13(f43(x3161,x3162,x3163),x3162)+~E(f47(x3161,x3162,x3163),f46(x3161,x3162,x3163))
% 58.77/58.86 [318]P7(x3181,x3182,x3183)+P3(x3181,f45(x3181,x3182,x3183),f46(x3181,x3182,x3183))+P13(f43(x3181,x3182,x3183),x3182)
% 58.77/58.86 [319]P7(x3191,x3192,x3193)+P3(x3191,f45(x3191,x3192,x3193),f47(x3191,x3192,x3193))+P13(f43(x3191,x3192,x3193),x3192)
% 58.77/58.86 [290]~P3(x2902,x2904,x2901)+~P13(x2904,x2903)+P13(x2901,f42(x2902,x2903))
% 58.77/58.86 [291]~P3(x2912,x2911,x2914)+~P13(x2914,x2913)+P13(x2911,f53(x2912,x2913))
% 58.77/58.86 [315]P15(x3151,x3152,x3153)+~P13(x3154,x3152)+~P3(x3151,x3154,f21(x3151,x3152,x3153))
% 58.77/58.86 [328]~P13(x3284,x3282)+~P7(x3281,x3282,x3283)+P13(f44(x3281,x3282,x3283,x3284),x3283)
% 58.77/58.86 [329]~P13(x3294,x3293)+~P15(x3291,x3292,x3293)+P13(f22(x3291,x3292,x3293,x3294),x3292)
% 58.77/58.86 [331]~P13(x3312,x3313)+~P7(x3311,x3313,x3314)+P3(x3311,x3312,f44(x3311,x3313,x3314,x3312))
% 58.77/58.86 [332]~P13(x3324,x3323)+~P15(x3321,x3322,x3323)+P3(x3321,f22(x3321,x3322,x3323,x3324),x3324)
% 58.77/58.86 [351]P11(x3511,x3512,x3513,x3514)+P3(x3511,f25(x3511,x3512,x3513,x3514),f24(x3511,x3512,x3513,x3514))+P3(x3512,f24(x3511,x3512,x3513,x3514),f25(x3511,x3512,x3513,x3514))
% 58.77/58.86 [353]P11(x3531,x3532,x3533,x3534)+~P3(x3531,f25(x3531,x3532,x3533,x3534),f24(x3531,x3532,x3533,x3534))+~P3(x3532,f24(x3531,x3532,x3533,x3534),f25(x3531,x3532,x3533,x3534))
% 58.77/58.86 [381]P6(x3811,x3812,x3813,x3814,x3815,x3816)+P3(x3811,f10(x3811,x3812,x3813,x3814,x3815,x3816),f11(x3811,x3812,x3813,x3814,x3815,x3816))+P13(f12(x3811,x3812,x3813,x3814,x3815,x3816),x3815)
% 58.77/58.86 [382]P6(x3821,x3822,x3823,x3824,x3825,x3826)+P3(x3821,f10(x3821,x3822,x3823,x3824,x3825,x3826),f11(x3821,x3822,x3823,x3824,x3825,x3826))+P3(x3823,f10(x3821,x3822,x3823,x3824,x3825,x3826),f12(x3821,x3822,x3823,x3824,x3825,x3826))
% 58.77/58.86 [383]P6(x3831,x3832,x3833,x3834,x3835,x3836)+P3(x3831,f10(x3831,x3832,x3833,x3834,x3835,x3836),f11(x3831,x3832,x3833,x3834,x3835,x3836))+P3(x3832,f12(x3831,x3832,x3833,x3834,x3835,x3836),f11(x3831,x3832,x3833,x3834,x3835,x3836))
% 58.77/58.86 [320]P7(x3201,x3202,x3203)+~P13(x3204,x3203)+~P3(x3201,f43(x3201,x3202,x3203),x3204)+P13(f45(x3201,x3202,x3203),x3202)
% 58.77/58.86 [321]P7(x3211,x3212,x3213)+~P13(x3214,x3213)+~P3(x3211,f43(x3211,x3212,x3213),x3214)+P13(f46(x3211,x3212,x3213),x3213)
% 58.77/58.86 [322]P7(x3221,x3222,x3223)+~P13(x3224,x3223)+~P3(x3221,f43(x3221,x3222,x3223),x3224)+P13(f47(x3221,x3222,x3223),x3223)
% 58.77/58.87 [323]P7(x3231,x3232,x3233)+~P13(x3234,x3233)+~P3(x3231,f43(x3231,x3232,x3233),x3234)+~E(f47(x3231,x3232,x3233),f46(x3231,x3232,x3233))
% 58.77/58.87 [326]P7(x3261,x3262,x3263)+~P13(x3264,x3263)+P3(x3261,f45(x3261,x3262,x3263),f46(x3261,x3262,x3263))+~P3(x3261,f43(x3261,x3262,x3263),x3264)
% 58.77/58.87 [327]P7(x3271,x3272,x3273)+~P13(x3274,x3273)+P3(x3271,f45(x3271,x3272,x3273),f47(x3271,x3272,x3273))+~P3(x3271,f43(x3271,x3272,x3273),x3274)
% 58.77/58.87 [305]~P13(x3051,x3054)+~P3(x3052,x3055,x3051)+~P13(x3055,x3053)+P13(x3051,f52(x3052,x3053,x3054))
% 58.77/58.87 [306]~P13(x3061,x3064)+~P3(x3062,x3061,x3065)+~P13(x3065,x3063)+P13(x3061,f55(x3062,x3063,x3064))
% 58.77/58.87 [307]~P13(x3074,x3073)+~P13(x3075,x3072)+~P3(x3071,x3075,x3074)+P3(f54(x3071,x3072,x3073),x3074,x3075)
% 58.77/58.87 [317]P3(x3171,x3172,x3173)+~P13(x3172,x3174)+~P13(x3173,x3175)+~P3(f54(x3171,x3174,x3175),x3173,x3172)
% 58.77/58.87 [362]~P7(x3621,x3622,x3624)+~P14(x3621,x3622,x3624)+P12(x3621,x3622,x3623,x3624,x3625)+P13(f37(x3621,x3622,x3623,x3624,x3625),x3622)
% 58.77/58.87 [363]~P7(x3631,x3632,x3634)+~P14(x3631,x3632,x3634)+P12(x3631,x3632,x3633,x3634,x3635)+P13(f38(x3631,x3632,x3633,x3634,x3635),x3634)
% 58.77/58.87 [364]~P7(x3641,x3642,x3644)+~P14(x3641,x3642,x3644)+P12(x3641,x3642,x3643,x3644,x3645)+P13(f39(x3641,x3642,x3643,x3644,x3645),x3642)
% 58.77/58.87 [365]~P7(x3651,x3652,x3654)+~P14(x3651,x3652,x3654)+P12(x3651,x3652,x3653,x3654,x3655)+P13(f40(x3651,x3652,x3653,x3654,x3655),x3654)
% 58.77/58.87 [372]~P7(x3721,x3722,x3724)+~P14(x3721,x3722,x3724)+P12(x3721,x3722,x3723,x3724,x3725)+P3(x3721,f37(x3721,x3722,x3723,x3724,x3725),f38(x3721,x3722,x3723,x3724,x3725))
% 58.77/58.87 [373]~P7(x3731,x3732,x3734)+~P14(x3731,x3732,x3734)+P12(x3731,x3732,x3733,x3734,x3735)+P3(x3731,f39(x3731,x3732,x3733,x3734,x3735),f40(x3731,x3732,x3733,x3734,x3735))
% 58.77/58.87 [384]~P13(x3847,x3845)+~P13(x3846,x3843)+~P3(f6(x3841,x3842,x3843,x3844,x3845),x3846,x3847)+P13(f13(x3841,x3842,x3843,x3844,x3845,x3846,x3847),x3844)
% 58.77/58.87 [385]~P13(x3857,x3856)+~P13(x3852,x3854)+~P3(f6(x3853,x3851,x3854,x3855,x3856),x3852,x3857)+P3(x3851,x3852,f13(x3853,x3851,x3854,x3855,x3856,x3852,x3857))
% 58.77/58.87 [386]~P13(x3867,x3865)+~P13(x3866,x3863)+~P3(f6(x3861,x3862,x3863,x3864,x3865),x3866,x3867)+P3(x3861,f13(x3861,x3862,x3863,x3864,x3865,x3866,x3867),x3867)
% 58.77/58.87 [377]~P7(x3771,x3772,x3774)+~P14(x3771,x3772,x3774)+P12(x3771,x3772,x3773,x3774,x3775)+P3(x3775,f38(x3771,x3772,x3773,x3774,x3775),f40(x3771,x3772,x3773,x3774,x3775))+P3(x3773,f37(x3771,x3772,x3773,x3774,x3775),f39(x3771,x3772,x3773,x3774,x3775))
% 58.77/58.87 [378]~P7(x3781,x3782,x3784)+~P14(x3781,x3782,x3784)+P12(x3781,x3782,x3783,x3784,x3785)+~P3(x3785,f38(x3781,x3782,x3783,x3784,x3785),f40(x3781,x3782,x3783,x3784,x3785))+~P3(x3783,f37(x3781,x3782,x3783,x3784,x3785),f39(x3781,x3782,x3783,x3784,x3785))
% 58.77/58.87 [324]~P11(x3241,x3246,x3245,x3244)+P3(x3241,x3242,x3243)+~P13(x3242,x3244)+~P3(x3246,x3243,x3242)+~P13(x3243,x3245)
% 58.77/58.87 [325]~P11(x3256,x3251,x3254,x3255)+P3(x3251,x3252,x3253)+~P13(x3252,x3254)+~P3(x3256,x3253,x3252)+~P13(x3253,x3255)
% 58.77/58.87 [387]P6(x3871,x3872,x3873,x3874,x3875,x3876)+~P13(x3877,x3875)+~P3(x3872,x3877,f11(x3871,x3872,x3873,x3874,x3875,x3876))+~P3(x3873,f10(x3871,x3872,x3873,x3874,x3875,x3876),x3877)+~P3(x3871,f10(x3871,x3872,x3873,x3874,x3875,x3876),f11(x3871,x3872,x3873,x3874,x3875,x3876))
% 58.77/58.87 [388]~P13(x3888,x3886)+~P13(x3887,x3884)+~P3(x3881,x3887,x3888)+~P6(x3881,x3882,x3883,x3884,x3885,x3886)+P13(f48(x3881,x3882,x3883,x3884,x3885,x3886,x3887,x3888),x3885)
% 58.77/58.87 [389]~P13(x3898,x3897)+~P13(x3892,x3895)+~P3(x3893,x3892,x3898)+~P6(x3893,x3894,x3891,x3895,x3896,x3897)+P3(x3891,x3892,f48(x3893,x3894,x3891,x3895,x3896,x3897,x3892,x3898))
% 58.77/58.87 [390]~P13(x3908,x3906)+~P13(x3907,x3904)+~P3(x3902,x3907,x3908)+~P6(x3902,x3901,x3903,x3904,x3905,x3906)+P3(x3901,f48(x3902,x3901,x3903,x3904,x3905,x3906,x3907,x3908),x3908)
% 58.77/58.87 [352]~P13(x3527,x3525)+~P13(x3526,x3523)+~P3(x3521,x3528,x3527)+~P3(x3522,x3526,x3528)+~P13(x3528,x3524)+P3(f6(x3521,x3522,x3523,x3524,x3525),x3526,x3527)
% 58.77/58.87 [313]~P13(x3131,x3135)+~P3(x3136,x3131,x3133)+~P9(x3136,x3135,x3134)+E(x3131,x3132)+~P13(x3133,x3134)+~P3(x3136,x3132,x3133)+~P13(x3132,x3135)
% 58.77/58.87 [314]~P13(x3141,x3143)+~P3(x3146,x3144,x3142)+~P3(x3146,x3144,x3141)+E(x3141,x3142)+~P13(x3142,x3143)+~P7(x3146,x3145,x3143)+~P13(x3144,x3145)
% 58.77/58.87 [330]~P13(x3301,x3303)+~P4(x3307,x3306,x3305,x3303)+E(x3301,x3302)+~P13(x3302,x3303)+~P3(x3306,x3304,x3302)+~P3(x3307,x3304,x3301)+~P13(x3304,x3305)
% 58.77/58.87 [376]~P6(x3761,x3768,x3769,x3765,x3767,x3764)+P3(x3761,x3762,x3763)+~P13(x3763,x3764)+~P13(x3762,x3765)+~P3(x3768,x3766,x3763)+~P3(x3769,x3762,x3766)+~P13(x3766,x3767)
% 58.77/58.87 [347]~P13(x3473,x3474)+~P3(x3479,x3477,x3473)+~P5(x3479,x3476,x3478,x3474,x3471)+P3(x3471,x3472,x3473)+~P13(x3472,x3474)+~P3(x3478,x3477,x3475)+~P3(x3479,x3475,x3472)+~P13(x3475,x3476)+~P13(x3477,x3476)
% 58.77/58.87 [348]~P13(x3482,x3484)+~P3(x3489,x3487,x3482)+~P10(x3489,x3486,x3488,x3484,x3481)+P3(x3481,x3482,x3483)+~P13(x3483,x3484)+~P3(x3488,x3487,x3485)+~P3(x3489,x3485,x3483)+~P13(x3485,x3486)+~P13(x3487,x3486)
% 58.77/58.87 [349]~P13(x3492,x3494)+~P3(x3498,x3497,x3492)+~P12(x3498,x3496,x3499,x3494,x3491)+P3(x3491,x3492,x3493)+~P13(x3493,x3494)+~P3(x3498,x3495,x3493)+~P3(x3499,x3497,x3495)+~P13(x3495,x3496)+~P13(x3497,x3496)
% 58.77/58.87 [350]~P13(x3502,x3504)+~P3(x3508,x3502,x3507)+~P12(x3508,x3504,x3501,x3506,x3509)+P3(x3501,x3502,x3503)+~P13(x3503,x3504)+~P3(x3508,x3503,x3505)+~P3(x3509,x3507,x3505)+~P13(x3505,x3506)+~P13(x3507,x3506)
% 58.77/58.87 %EqnAxiom
% 58.77/58.87 [1]E(x11,x11)
% 58.77/58.87 [2]E(x22,x21)+~E(x21,x22)
% 58.77/58.87 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.77/58.87 [4]~E(x41,x42)+E(f42(x41,x43),f42(x42,x43))
% 58.77/58.87 [5]~E(x51,x52)+E(f42(x53,x51),f42(x53,x52))
% 58.77/58.87 [6]~E(x61,x62)+E(f49(x61),f49(x62))
% 58.77/58.87 [7]~E(x71,x72)+E(f11(x71,x73,x74,x75,x76,x77),f11(x72,x73,x74,x75,x76,x77))
% 58.77/58.87 [8]~E(x81,x82)+E(f11(x83,x81,x84,x85,x86,x87),f11(x83,x82,x84,x85,x86,x87))
% 58.77/58.87 [9]~E(x91,x92)+E(f11(x93,x94,x91,x95,x96,x97),f11(x93,x94,x92,x95,x96,x97))
% 58.77/58.87 [10]~E(x101,x102)+E(f11(x103,x104,x105,x101,x106,x107),f11(x103,x104,x105,x102,x106,x107))
% 58.77/58.87 [11]~E(x111,x112)+E(f11(x113,x114,x115,x116,x111,x117),f11(x113,x114,x115,x116,x112,x117))
% 58.77/58.87 [12]~E(x121,x122)+E(f11(x123,x124,x125,x126,x127,x121),f11(x123,x124,x125,x126,x127,x122))
% 58.77/58.87 [13]~E(x131,x132)+E(f50(x131),f50(x132))
% 58.77/58.87 [14]~E(x141,x142)+E(f57(x141,x143),f57(x142,x143))
% 58.77/58.87 [15]~E(x151,x152)+E(f57(x153,x151),f57(x153,x152))
% 58.77/58.87 [16]~E(x161,x162)+E(f6(x161,x163,x164,x165,x166),f6(x162,x163,x164,x165,x166))
% 58.77/58.87 [17]~E(x171,x172)+E(f6(x173,x171,x174,x175,x176),f6(x173,x172,x174,x175,x176))
% 58.77/58.87 [18]~E(x181,x182)+E(f6(x183,x184,x181,x185,x186),f6(x183,x184,x182,x185,x186))
% 58.77/58.87 [19]~E(x191,x192)+E(f6(x193,x194,x195,x191,x196),f6(x193,x194,x195,x192,x196))
% 58.77/58.87 [20]~E(x201,x202)+E(f6(x203,x204,x205,x206,x201),f6(x203,x204,x205,x206,x202))
% 58.77/58.87 [21]~E(x211,x212)+E(f13(x211,x213,x214,x215,x216,x217,x218),f13(x212,x213,x214,x215,x216,x217,x218))
% 58.77/58.87 [22]~E(x221,x222)+E(f13(x223,x221,x224,x225,x226,x227,x228),f13(x223,x222,x224,x225,x226,x227,x228))
% 58.77/58.87 [23]~E(x231,x232)+E(f13(x233,x234,x231,x235,x236,x237,x238),f13(x233,x234,x232,x235,x236,x237,x238))
% 58.77/58.87 [24]~E(x241,x242)+E(f13(x243,x244,x245,x241,x246,x247,x248),f13(x243,x244,x245,x242,x246,x247,x248))
% 58.77/58.87 [25]~E(x251,x252)+E(f13(x253,x254,x255,x256,x251,x257,x258),f13(x253,x254,x255,x256,x252,x257,x258))
% 58.77/58.87 [26]~E(x261,x262)+E(f13(x263,x264,x265,x266,x267,x261,x268),f13(x263,x264,x265,x266,x267,x262,x268))
% 58.77/58.87 [27]~E(x271,x272)+E(f13(x273,x274,x275,x276,x277,x278,x271),f13(x273,x274,x275,x276,x277,x278,x272))
% 58.77/58.87 [28]~E(x281,x282)+E(f7(x281,x283),f7(x282,x283))
% 58.77/58.87 [29]~E(x291,x292)+E(f7(x293,x291),f7(x293,x292))
% 58.77/58.87 [30]~E(x301,x302)+E(f8(x301,x303),f8(x302,x303))
% 58.77/58.87 [31]~E(x311,x312)+E(f8(x313,x311),f8(x313,x312))
% 58.77/58.87 [32]~E(x321,x322)+E(f56(x321),f56(x322))
% 58.77/58.87 [33]~E(x331,x332)+E(f18(x331,x333),f18(x332,x333))
% 58.77/58.87 [34]~E(x341,x342)+E(f18(x343,x341),f18(x343,x342))
% 58.77/58.87 [35]~E(x351,x352)+E(f58(x351,x353),f58(x352,x353))
% 58.77/58.87 [36]~E(x361,x362)+E(f58(x363,x361),f58(x363,x362))
% 58.77/58.87 [37]~E(x371,x372)+E(f10(x371,x373,x374,x375,x376,x377),f10(x372,x373,x374,x375,x376,x377))
% 58.77/58.87 [38]~E(x381,x382)+E(f10(x383,x381,x384,x385,x386,x387),f10(x383,x382,x384,x385,x386,x387))
% 58.77/58.87 [39]~E(x391,x392)+E(f10(x393,x394,x391,x395,x396,x397),f10(x393,x394,x392,x395,x396,x397))
% 58.77/58.87 [40]~E(x401,x402)+E(f10(x403,x404,x405,x401,x406,x407),f10(x403,x404,x405,x402,x406,x407))
% 58.77/58.87 [41]~E(x411,x412)+E(f10(x413,x414,x415,x416,x411,x417),f10(x413,x414,x415,x416,x412,x417))
% 58.77/58.87 [42]~E(x421,x422)+E(f10(x423,x424,x425,x426,x427,x421),f10(x423,x424,x425,x426,x427,x422))
% 58.77/58.87 [43]~E(x431,x432)+E(f59(x431),f59(x432))
% 58.77/58.87 [44]~E(x441,x442)+E(f39(x441,x443,x444,x445,x446),f39(x442,x443,x444,x445,x446))
% 58.77/58.87 [45]~E(x451,x452)+E(f39(x453,x451,x454,x455,x456),f39(x453,x452,x454,x455,x456))
% 58.77/58.87 [46]~E(x461,x462)+E(f39(x463,x464,x461,x465,x466),f39(x463,x464,x462,x465,x466))
% 58.77/58.87 [47]~E(x471,x472)+E(f39(x473,x474,x475,x471,x476),f39(x473,x474,x475,x472,x476))
% 58.77/58.87 [48]~E(x481,x482)+E(f39(x483,x484,x485,x486,x481),f39(x483,x484,x485,x486,x482))
% 58.77/58.87 [49]~E(x491,x492)+E(f37(x491,x493,x494,x495,x496),f37(x492,x493,x494,x495,x496))
% 58.77/58.87 [50]~E(x501,x502)+E(f37(x503,x501,x504,x505,x506),f37(x503,x502,x504,x505,x506))
% 58.77/58.87 [51]~E(x511,x512)+E(f37(x513,x514,x511,x515,x516),f37(x513,x514,x512,x515,x516))
% 58.77/58.87 [52]~E(x521,x522)+E(f37(x523,x524,x525,x521,x526),f37(x523,x524,x525,x522,x526))
% 58.77/58.87 [53]~E(x531,x532)+E(f37(x533,x534,x535,x536,x531),f37(x533,x534,x535,x536,x532))
% 58.77/58.87 [54]~E(x541,x542)+E(f19(x541,x543),f19(x542,x543))
% 58.77/58.87 [55]~E(x551,x552)+E(f19(x553,x551),f19(x553,x552))
% 58.77/58.87 [56]~E(x561,x562)+E(f40(x561,x563,x564,x565,x566),f40(x562,x563,x564,x565,x566))
% 58.77/58.87 [57]~E(x571,x572)+E(f40(x573,x571,x574,x575,x576),f40(x573,x572,x574,x575,x576))
% 58.77/58.87 [58]~E(x581,x582)+E(f40(x583,x584,x581,x585,x586),f40(x583,x584,x582,x585,x586))
% 58.77/58.87 [59]~E(x591,x592)+E(f40(x593,x594,x595,x591,x596),f40(x593,x594,x595,x592,x596))
% 58.77/58.87 [60]~E(x601,x602)+E(f40(x603,x604,x605,x606,x601),f40(x603,x604,x605,x606,x602))
% 58.77/58.87 [61]~E(x611,x612)+E(f38(x611,x613,x614,x615,x616),f38(x612,x613,x614,x615,x616))
% 58.77/58.87 [62]~E(x621,x622)+E(f38(x623,x621,x624,x625,x626),f38(x623,x622,x624,x625,x626))
% 58.77/58.87 [63]~E(x631,x632)+E(f38(x633,x634,x631,x635,x636),f38(x633,x634,x632,x635,x636))
% 58.77/58.87 [64]~E(x641,x642)+E(f38(x643,x644,x645,x641,x646),f38(x643,x644,x645,x642,x646))
% 58.77/58.87 [65]~E(x651,x652)+E(f38(x653,x654,x655,x656,x651),f38(x653,x654,x655,x656,x652))
% 58.77/58.87 [66]~E(x661,x662)+E(f34(x661,x663,x664,x665,x666),f34(x662,x663,x664,x665,x666))
% 58.77/58.87 [67]~E(x671,x672)+E(f34(x673,x671,x674,x675,x676),f34(x673,x672,x674,x675,x676))
% 58.77/58.87 [68]~E(x681,x682)+E(f34(x683,x684,x681,x685,x686),f34(x683,x684,x682,x685,x686))
% 58.77/58.87 [69]~E(x691,x692)+E(f34(x693,x694,x695,x691,x696),f34(x693,x694,x695,x692,x696))
% 58.77/58.87 [70]~E(x701,x702)+E(f34(x703,x704,x705,x706,x701),f34(x703,x704,x705,x706,x702))
% 58.77/58.87 [71]~E(x711,x712)+E(f5(x711,x713),f5(x712,x713))
% 58.77/58.87 [72]~E(x721,x722)+E(f5(x723,x721),f5(x723,x722))
% 58.77/58.87 [73]~E(x731,x732)+E(f51(x731,x733),f51(x732,x733))
% 58.77/58.87 [74]~E(x741,x742)+E(f51(x743,x741),f51(x743,x742))
% 58.77/58.87 [75]~E(x751,x752)+E(f29(x751,x753,x754,x755,x756),f29(x752,x753,x754,x755,x756))
% 58.77/58.87 [76]~E(x761,x762)+E(f29(x763,x761,x764,x765,x766),f29(x763,x762,x764,x765,x766))
% 58.77/58.87 [77]~E(x771,x772)+E(f29(x773,x774,x771,x775,x776),f29(x773,x774,x772,x775,x776))
% 58.77/58.87 [78]~E(x781,x782)+E(f29(x783,x784,x785,x781,x786),f29(x783,x784,x785,x782,x786))
% 58.77/58.87 [79]~E(x791,x792)+E(f29(x793,x794,x795,x796,x791),f29(x793,x794,x795,x796,x792))
% 58.77/58.87 [80]~E(x801,x802)+E(f31(x801,x803,x804,x805,x806),f31(x802,x803,x804,x805,x806))
% 58.77/58.87 [81]~E(x811,x812)+E(f31(x813,x811,x814,x815,x816),f31(x813,x812,x814,x815,x816))
% 58.77/58.87 [82]~E(x821,x822)+E(f31(x823,x824,x821,x825,x826),f31(x823,x824,x822,x825,x826))
% 58.77/58.87 [83]~E(x831,x832)+E(f31(x833,x834,x835,x831,x836),f31(x833,x834,x835,x832,x836))
% 58.77/58.87 [84]~E(x841,x842)+E(f31(x843,x844,x845,x846,x841),f31(x843,x844,x845,x846,x842))
% 58.77/58.87 [85]~E(x851,x852)+E(f32(x851,x853,x854,x855,x856),f32(x852,x853,x854,x855,x856))
% 58.77/58.87 [86]~E(x861,x862)+E(f32(x863,x861,x864,x865,x866),f32(x863,x862,x864,x865,x866))
% 58.77/58.87 [87]~E(x871,x872)+E(f32(x873,x874,x871,x875,x876),f32(x873,x874,x872,x875,x876))
% 58.77/58.87 [88]~E(x881,x882)+E(f32(x883,x884,x885,x881,x886),f32(x883,x884,x885,x882,x886))
% 58.77/58.87 [89]~E(x891,x892)+E(f32(x893,x894,x895,x896,x891),f32(x893,x894,x895,x896,x892))
% 58.77/58.87 [90]~E(x901,x902)+E(f33(x901,x903,x904,x905,x906),f33(x902,x903,x904,x905,x906))
% 58.77/58.87 [91]~E(x911,x912)+E(f33(x913,x911,x914,x915,x916),f33(x913,x912,x914,x915,x916))
% 58.77/58.87 [92]~E(x921,x922)+E(f33(x923,x924,x921,x925,x926),f33(x923,x924,x922,x925,x926))
% 58.77/58.87 [93]~E(x931,x932)+E(f33(x933,x934,x935,x931,x936),f33(x933,x934,x935,x932,x936))
% 58.77/58.87 [94]~E(x941,x942)+E(f33(x943,x944,x945,x946,x941),f33(x943,x944,x945,x946,x942))
% 58.77/58.87 [95]~E(x951,x952)+E(f12(x951,x953,x954,x955,x956,x957),f12(x952,x953,x954,x955,x956,x957))
% 58.77/58.87 [96]~E(x961,x962)+E(f12(x963,x961,x964,x965,x966,x967),f12(x963,x962,x964,x965,x966,x967))
% 58.77/58.87 [97]~E(x971,x972)+E(f12(x973,x974,x971,x975,x976,x977),f12(x973,x974,x972,x975,x976,x977))
% 58.77/58.87 [98]~E(x981,x982)+E(f12(x983,x984,x985,x981,x986,x987),f12(x983,x984,x985,x982,x986,x987))
% 58.77/58.87 [99]~E(x991,x992)+E(f12(x993,x994,x995,x996,x991,x997),f12(x993,x994,x995,x996,x992,x997))
% 58.77/58.87 [100]~E(x1001,x1002)+E(f12(x1003,x1004,x1005,x1006,x1007,x1001),f12(x1003,x1004,x1005,x1006,x1007,x1002))
% 58.77/58.87 [101]~E(x1011,x1012)+E(f36(x1011,x1013,x1014,x1015,x1016),f36(x1012,x1013,x1014,x1015,x1016))
% 58.77/58.87 [102]~E(x1021,x1022)+E(f36(x1023,x1021,x1024,x1025,x1026),f36(x1023,x1022,x1024,x1025,x1026))
% 58.77/58.87 [103]~E(x1031,x1032)+E(f36(x1033,x1034,x1031,x1035,x1036),f36(x1033,x1034,x1032,x1035,x1036))
% 58.77/58.87 [104]~E(x1041,x1042)+E(f36(x1043,x1044,x1045,x1041,x1046),f36(x1043,x1044,x1045,x1042,x1046))
% 58.77/58.87 [105]~E(x1051,x1052)+E(f36(x1053,x1054,x1055,x1056,x1051),f36(x1053,x1054,x1055,x1056,x1052))
% 58.77/58.87 [106]~E(x1061,x1062)+E(f30(x1061,x1063,x1064,x1065,x1066),f30(x1062,x1063,x1064,x1065,x1066))
% 58.77/58.87 [107]~E(x1071,x1072)+E(f30(x1073,x1071,x1074,x1075,x1076),f30(x1073,x1072,x1074,x1075,x1076))
% 58.77/58.87 [108]~E(x1081,x1082)+E(f30(x1083,x1084,x1081,x1085,x1086),f30(x1083,x1084,x1082,x1085,x1086))
% 58.77/58.87 [109]~E(x1091,x1092)+E(f30(x1093,x1094,x1095,x1091,x1096),f30(x1093,x1094,x1095,x1092,x1096))
% 58.77/58.87 [110]~E(x1101,x1102)+E(f30(x1103,x1104,x1105,x1106,x1101),f30(x1103,x1104,x1105,x1106,x1102))
% 58.77/58.87 [111]~E(x1111,x1112)+E(f35(x1111,x1113,x1114,x1115,x1116),f35(x1112,x1113,x1114,x1115,x1116))
% 58.77/58.87 [112]~E(x1121,x1122)+E(f35(x1123,x1121,x1124,x1125,x1126),f35(x1123,x1122,x1124,x1125,x1126))
% 58.77/58.87 [113]~E(x1131,x1132)+E(f35(x1133,x1134,x1131,x1135,x1136),f35(x1133,x1134,x1132,x1135,x1136))
% 58.77/58.87 [114]~E(x1141,x1142)+E(f35(x1143,x1144,x1145,x1141,x1146),f35(x1143,x1144,x1145,x1142,x1146))
% 58.77/58.87 [115]~E(x1151,x1152)+E(f35(x1153,x1154,x1155,x1156,x1151),f35(x1153,x1154,x1155,x1156,x1152))
% 58.77/58.87 [116]~E(x1161,x1162)+E(f48(x1161,x1163,x1164,x1165,x1166,x1167,x1168,x1169),f48(x1162,x1163,x1164,x1165,x1166,x1167,x1168,x1169))
% 58.77/58.87 [117]~E(x1171,x1172)+E(f48(x1173,x1171,x1174,x1175,x1176,x1177,x1178,x1179),f48(x1173,x1172,x1174,x1175,x1176,x1177,x1178,x1179))
% 58.77/58.87 [118]~E(x1181,x1182)+E(f48(x1183,x1184,x1181,x1185,x1186,x1187,x1188,x1189),f48(x1183,x1184,x1182,x1185,x1186,x1187,x1188,x1189))
% 58.77/58.87 [119]~E(x1191,x1192)+E(f48(x1193,x1194,x1195,x1191,x1196,x1197,x1198,x1199),f48(x1193,x1194,x1195,x1192,x1196,x1197,x1198,x1199))
% 58.77/58.87 [120]~E(x1201,x1202)+E(f48(x1203,x1204,x1205,x1206,x1201,x1207,x1208,x1209),f48(x1203,x1204,x1205,x1206,x1202,x1207,x1208,x1209))
% 58.77/58.87 [121]~E(x1211,x1212)+E(f48(x1213,x1214,x1215,x1216,x1217,x1211,x1218,x1219),f48(x1213,x1214,x1215,x1216,x1217,x1212,x1218,x1219))
% 58.77/58.87 [122]~E(x1221,x1222)+E(f48(x1223,x1224,x1225,x1226,x1227,x1228,x1221,x1229),f48(x1223,x1224,x1225,x1226,x1227,x1228,x1222,x1229))
% 58.77/58.87 [123]~E(x1231,x1232)+E(f48(x1233,x1234,x1235,x1236,x1237,x1238,x1239,x1231),f48(x1233,x1234,x1235,x1236,x1237,x1238,x1239,x1232))
% 58.77/58.87 [124]~E(x1241,x1242)+E(f53(x1241,x1243),f53(x1242,x1243))
% 58.77/58.87 [125]~E(x1251,x1252)+E(f53(x1253,x1251),f53(x1253,x1252))
% 58.77/58.87 [126]~E(x1261,x1262)+E(f16(x1261,x1263,x1264),f16(x1262,x1263,x1264))
% 58.77/58.87 [127]~E(x1271,x1272)+E(f16(x1273,x1271,x1274),f16(x1273,x1272,x1274))
% 58.77/58.87 [128]~E(x1281,x1282)+E(f16(x1283,x1284,x1281),f16(x1283,x1284,x1282))
% 58.77/58.87 [129]~E(x1291,x1292)+E(f17(x1291,x1293,x1294),f17(x1292,x1293,x1294))
% 58.77/58.87 [130]~E(x1301,x1302)+E(f17(x1303,x1301,x1304),f17(x1303,x1302,x1304))
% 58.77/58.87 [131]~E(x1311,x1312)+E(f17(x1313,x1314,x1311),f17(x1313,x1314,x1312))
% 58.77/58.87 [132]~E(x1321,x1322)+E(f20(x1321,x1323,x1324),f20(x1322,x1323,x1324))
% 58.77/58.87 [133]~E(x1331,x1332)+E(f20(x1333,x1331,x1334),f20(x1333,x1332,x1334))
% 58.77/58.87 [134]~E(x1341,x1342)+E(f20(x1343,x1344,x1341),f20(x1343,x1344,x1342))
% 58.77/58.87 [135]~E(x1351,x1352)+E(f21(x1351,x1353,x1354),f21(x1352,x1353,x1354))
% 58.77/58.87 [136]~E(x1361,x1362)+E(f21(x1363,x1361,x1364),f21(x1363,x1362,x1364))
% 58.77/58.87 [137]~E(x1371,x1372)+E(f21(x1373,x1374,x1371),f21(x1373,x1374,x1372))
% 58.77/58.87 [138]~E(x1381,x1382)+E(f24(x1381,x1383,x1384,x1385),f24(x1382,x1383,x1384,x1385))
% 58.77/58.87 [139]~E(x1391,x1392)+E(f24(x1393,x1391,x1394,x1395),f24(x1393,x1392,x1394,x1395))
% 58.77/58.87 [140]~E(x1401,x1402)+E(f24(x1403,x1404,x1401,x1405),f24(x1403,x1404,x1402,x1405))
% 58.77/58.87 [141]~E(x1411,x1412)+E(f24(x1413,x1414,x1415,x1411),f24(x1413,x1414,x1415,x1412))
% 58.77/58.87 [142]~E(x1421,x1422)+E(f15(x1421,x1423,x1424,x1425),f15(x1422,x1423,x1424,x1425))
% 58.77/58.87 [143]~E(x1431,x1432)+E(f15(x1433,x1431,x1434,x1435),f15(x1433,x1432,x1434,x1435))
% 58.77/58.87 [144]~E(x1441,x1442)+E(f15(x1443,x1444,x1441,x1445),f15(x1443,x1444,x1442,x1445))
% 58.77/58.87 [145]~E(x1451,x1452)+E(f15(x1453,x1454,x1455,x1451),f15(x1453,x1454,x1455,x1452))
% 58.77/58.87 [146]~E(x1461,x1462)+E(f23(x1461,x1463,x1464),f23(x1462,x1463,x1464))
% 58.77/58.87 [147]~E(x1471,x1472)+E(f23(x1473,x1471,x1474),f23(x1473,x1472,x1474))
% 58.77/58.87 [148]~E(x1481,x1482)+E(f23(x1483,x1484,x1481),f23(x1483,x1484,x1482))
% 58.77/58.87 [149]~E(x1491,x1492)+E(f25(x1491,x1493,x1494,x1495),f25(x1492,x1493,x1494,x1495))
% 58.77/58.87 [150]~E(x1501,x1502)+E(f25(x1503,x1501,x1504,x1505),f25(x1503,x1502,x1504,x1505))
% 58.77/58.87 [151]~E(x1511,x1512)+E(f25(x1513,x1514,x1511,x1515),f25(x1513,x1514,x1512,x1515))
% 58.77/58.87 [152]~E(x1521,x1522)+E(f25(x1523,x1524,x1525,x1521),f25(x1523,x1524,x1525,x1522))
% 58.77/58.87 [153]~E(x1531,x1532)+E(f26(x1531,x1533,x1534),f26(x1532,x1533,x1534))
% 58.77/58.87 [154]~E(x1541,x1542)+E(f26(x1543,x1541,x1544),f26(x1543,x1542,x1544))
% 58.77/58.87 [155]~E(x1551,x1552)+E(f26(x1553,x1554,x1551),f26(x1553,x1554,x1552))
% 58.77/58.87 [156]~E(x1561,x1562)+E(f27(x1561,x1563,x1564,x1565),f27(x1562,x1563,x1564,x1565))
% 58.77/58.87 [157]~E(x1571,x1572)+E(f27(x1573,x1571,x1574,x1575),f27(x1573,x1572,x1574,x1575))
% 58.77/58.87 [158]~E(x1581,x1582)+E(f27(x1583,x1584,x1581,x1585),f27(x1583,x1584,x1582,x1585))
% 58.77/58.87 [159]~E(x1591,x1592)+E(f27(x1593,x1594,x1595,x1591),f27(x1593,x1594,x1595,x1592))
% 58.77/58.87 [160]~E(x1601,x1602)+E(f52(x1601,x1603,x1604),f52(x1602,x1603,x1604))
% 58.77/58.87 [161]~E(x1611,x1612)+E(f52(x1613,x1611,x1614),f52(x1613,x1612,x1614))
% 58.77/58.87 [162]~E(x1621,x1622)+E(f52(x1623,x1624,x1621),f52(x1623,x1624,x1622))
% 58.77/58.87 [163]~E(x1631,x1632)+E(f55(x1631,x1633,x1634),f55(x1632,x1633,x1634))
% 58.77/58.87 [164]~E(x1641,x1642)+E(f55(x1643,x1641,x1644),f55(x1643,x1642,x1644))
% 58.77/58.87 [165]~E(x1651,x1652)+E(f55(x1653,x1654,x1651),f55(x1653,x1654,x1652))
% 58.77/58.87 [166]~E(x1661,x1662)+E(f28(x1661,x1663,x1664,x1665),f28(x1662,x1663,x1664,x1665))
% 58.77/58.87 [167]~E(x1671,x1672)+E(f28(x1673,x1671,x1674,x1675),f28(x1673,x1672,x1674,x1675))
% 58.77/58.87 [168]~E(x1681,x1682)+E(f28(x1683,x1684,x1681,x1685),f28(x1683,x1684,x1682,x1685))
% 58.77/58.87 [169]~E(x1691,x1692)+E(f28(x1693,x1694,x1695,x1691),f28(x1693,x1694,x1695,x1692))
% 58.77/58.87 [170]~E(x1701,x1702)+E(f22(x1701,x1703,x1704,x1705),f22(x1702,x1703,x1704,x1705))
% 58.77/58.87 [171]~E(x1711,x1712)+E(f22(x1713,x1711,x1714,x1715),f22(x1713,x1712,x1714,x1715))
% 58.77/58.87 [172]~E(x1721,x1722)+E(f22(x1723,x1724,x1721,x1725),f22(x1723,x1724,x1722,x1725))
% 58.77/58.87 [173]~E(x1731,x1732)+E(f22(x1733,x1734,x1735,x1731),f22(x1733,x1734,x1735,x1732))
% 58.77/58.87 [174]~E(x1741,x1742)+E(f45(x1741,x1743,x1744),f45(x1742,x1743,x1744))
% 58.77/58.87 [175]~E(x1751,x1752)+E(f45(x1753,x1751,x1754),f45(x1753,x1752,x1754))
% 58.77/58.87 [176]~E(x1761,x1762)+E(f45(x1763,x1764,x1761),f45(x1763,x1764,x1762))
% 58.77/58.87 [177]~E(x1771,x1772)+E(f47(x1771,x1773,x1774),f47(x1772,x1773,x1774))
% 58.77/58.87 [178]~E(x1781,x1782)+E(f47(x1783,x1781,x1784),f47(x1783,x1782,x1784))
% 58.77/58.87 [179]~E(x1791,x1792)+E(f47(x1793,x1794,x1791),f47(x1793,x1794,x1792))
% 58.77/58.87 [180]~E(x1801,x1802)+E(f14(x1801,x1803,x1804,x1805),f14(x1802,x1803,x1804,x1805))
% 58.77/58.87 [181]~E(x1811,x1812)+E(f14(x1813,x1811,x1814,x1815),f14(x1813,x1812,x1814,x1815))
% 58.77/58.87 [182]~E(x1821,x1822)+E(f14(x1823,x1824,x1821,x1825),f14(x1823,x1824,x1822,x1825))
% 58.77/58.87 [183]~E(x1831,x1832)+E(f14(x1833,x1834,x1835,x1831),f14(x1833,x1834,x1835,x1832))
% 58.77/58.87 [184]~E(x1841,x1842)+E(f43(x1841,x1843,x1844),f43(x1842,x1843,x1844))
% 58.77/58.87 [185]~E(x1851,x1852)+E(f43(x1853,x1851,x1854),f43(x1853,x1852,x1854))
% 58.77/58.87 [186]~E(x1861,x1862)+E(f43(x1863,x1864,x1861),f43(x1863,x1864,x1862))
% 58.77/58.87 [187]~E(x1871,x1872)+E(f44(x1871,x1873,x1874,x1875),f44(x1872,x1873,x1874,x1875))
% 58.77/58.87 [188]~E(x1881,x1882)+E(f44(x1883,x1881,x1884,x1885),f44(x1883,x1882,x1884,x1885))
% 58.77/58.87 [189]~E(x1891,x1892)+E(f44(x1893,x1894,x1891,x1895),f44(x1893,x1894,x1892,x1895))
% 58.77/58.87 [190]~E(x1901,x1902)+E(f44(x1903,x1904,x1905,x1901),f44(x1903,x1904,x1905,x1902))
% 58.77/58.87 [191]~E(x1911,x1912)+E(f9(x1911,x1913,x1914,x1915),f9(x1912,x1913,x1914,x1915))
% 58.77/58.87 [192]~E(x1921,x1922)+E(f9(x1923,x1921,x1924,x1925),f9(x1923,x1922,x1924,x1925))
% 58.77/58.87 [193]~E(x1931,x1932)+E(f9(x1933,x1934,x1931,x1935),f9(x1933,x1934,x1932,x1935))
% 58.77/58.87 [194]~E(x1941,x1942)+E(f9(x1943,x1944,x1945,x1941),f9(x1943,x1944,x1945,x1942))
% 58.77/58.87 [195]~E(x1951,x1952)+E(f54(x1951,x1953,x1954),f54(x1952,x1953,x1954))
% 58.77/58.87 [196]~E(x1961,x1962)+E(f54(x1963,x1961,x1964),f54(x1963,x1962,x1964))
% 58.77/58.87 [197]~E(x1971,x1972)+E(f54(x1973,x1974,x1971),f54(x1973,x1974,x1972))
% 58.77/58.87 [198]~E(x1981,x1982)+E(f46(x1981,x1983,x1984),f46(x1982,x1983,x1984))
% 58.77/58.87 [199]~E(x1991,x1992)+E(f46(x1993,x1991,x1994),f46(x1993,x1992,x1994))
% 58.77/58.87 [200]~E(x2001,x2002)+E(f46(x2003,x2004,x2001),f46(x2003,x2004,x2002))
% 58.77/58.87 [201]P1(x2012,x2013)+~E(x2011,x2012)+~P1(x2011,x2013)
% 58.77/58.87 [202]P1(x2023,x2022)+~E(x2021,x2022)+~P1(x2023,x2021)
% 58.77/58.87 [203]P2(x2032,x2033)+~E(x2031,x2032)+~P2(x2031,x2033)
% 58.77/58.87 [204]P2(x2043,x2042)+~E(x2041,x2042)+~P2(x2043,x2041)
% 58.77/58.87 [205]P7(x2052,x2053,x2054)+~E(x2051,x2052)+~P7(x2051,x2053,x2054)
% 58.77/58.87 [206]P7(x2063,x2062,x2064)+~E(x2061,x2062)+~P7(x2063,x2061,x2064)
% 58.77/58.87 [207]P7(x2073,x2074,x2072)+~E(x2071,x2072)+~P7(x2073,x2074,x2071)
% 58.77/58.87 [208]P3(x2082,x2083,x2084)+~E(x2081,x2082)+~P3(x2081,x2083,x2084)
% 58.77/58.87 [209]P3(x2093,x2092,x2094)+~E(x2091,x2092)+~P3(x2093,x2091,x2094)
% 58.77/58.87 [210]P3(x2103,x2104,x2102)+~E(x2101,x2102)+~P3(x2103,x2104,x2101)
% 58.77/58.87 [211]P13(x2112,x2113)+~E(x2111,x2112)+~P13(x2111,x2113)
% 58.77/58.87 [212]P13(x2123,x2122)+~E(x2121,x2122)+~P13(x2123,x2121)
% 58.77/58.87 [213]P12(x2132,x2133,x2134,x2135,x2136)+~E(x2131,x2132)+~P12(x2131,x2133,x2134,x2135,x2136)
% 58.77/58.87 [214]P12(x2143,x2142,x2144,x2145,x2146)+~E(x2141,x2142)+~P12(x2143,x2141,x2144,x2145,x2146)
% 58.77/58.87 [215]P12(x2153,x2154,x2152,x2155,x2156)+~E(x2151,x2152)+~P12(x2153,x2154,x2151,x2155,x2156)
% 58.77/58.87 [216]P12(x2163,x2164,x2165,x2162,x2166)+~E(x2161,x2162)+~P12(x2163,x2164,x2165,x2161,x2166)
% 58.77/58.87 [217]P12(x2173,x2174,x2175,x2176,x2172)+~E(x2171,x2172)+~P12(x2173,x2174,x2175,x2176,x2171)
% 58.77/58.87 [218]P14(x2182,x2183,x2184)+~E(x2181,x2182)+~P14(x2181,x2183,x2184)
% 58.77/58.87 [219]P14(x2193,x2192,x2194)+~E(x2191,x2192)+~P14(x2193,x2191,x2194)
% 58.77/58.87 [220]P14(x2203,x2204,x2202)+~E(x2201,x2202)+~P14(x2203,x2204,x2201)
% 58.77/58.87 [221]P6(x2212,x2213,x2214,x2215,x2216,x2217)+~E(x2211,x2212)+~P6(x2211,x2213,x2214,x2215,x2216,x2217)
% 58.77/58.87 [222]P6(x2223,x2222,x2224,x2225,x2226,x2227)+~E(x2221,x2222)+~P6(x2223,x2221,x2224,x2225,x2226,x2227)
% 58.77/58.87 [223]P6(x2233,x2234,x2232,x2235,x2236,x2237)+~E(x2231,x2232)+~P6(x2233,x2234,x2231,x2235,x2236,x2237)
% 58.77/58.87 [224]P6(x2243,x2244,x2245,x2242,x2246,x2247)+~E(x2241,x2242)+~P6(x2243,x2244,x2245,x2241,x2246,x2247)
% 58.77/58.87 [225]P6(x2253,x2254,x2255,x2256,x2252,x2257)+~E(x2251,x2252)+~P6(x2253,x2254,x2255,x2256,x2251,x2257)
% 58.77/58.87 [226]P6(x2263,x2264,x2265,x2266,x2267,x2262)+~E(x2261,x2262)+~P6(x2263,x2264,x2265,x2266,x2267,x2261)
% 58.77/58.87 [227]P9(x2272,x2273,x2274)+~E(x2271,x2272)+~P9(x2271,x2273,x2274)
% 58.77/58.87 [228]P9(x2283,x2282,x2284)+~E(x2281,x2282)+~P9(x2283,x2281,x2284)
% 58.77/58.87 [229]P9(x2293,x2294,x2292)+~E(x2291,x2292)+~P9(x2293,x2294,x2291)
% 58.77/58.87 [230]P10(x2302,x2303,x2304,x2305,x2306)+~E(x2301,x2302)+~P10(x2301,x2303,x2304,x2305,x2306)
% 58.77/58.87 [231]P10(x2313,x2312,x2314,x2315,x2316)+~E(x2311,x2312)+~P10(x2313,x2311,x2314,x2315,x2316)
% 58.77/58.87 [232]P10(x2323,x2324,x2322,x2325,x2326)+~E(x2321,x2322)+~P10(x2323,x2324,x2321,x2325,x2326)
% 58.77/58.87 [233]P10(x2333,x2334,x2335,x2332,x2336)+~E(x2331,x2332)+~P10(x2333,x2334,x2335,x2331,x2336)
% 58.77/58.87 [234]P10(x2343,x2344,x2345,x2346,x2342)+~E(x2341,x2342)+~P10(x2343,x2344,x2345,x2346,x2341)
% 58.77/58.87 [235]P11(x2352,x2353,x2354,x2355)+~E(x2351,x2352)+~P11(x2351,x2353,x2354,x2355)
% 58.77/58.88 [236]P11(x2363,x2362,x2364,x2365)+~E(x2361,x2362)+~P11(x2363,x2361,x2364,x2365)
% 58.77/58.88 [237]P11(x2373,x2374,x2372,x2375)+~E(x2371,x2372)+~P11(x2373,x2374,x2371,x2375)
% 58.77/58.88 [238]P11(x2383,x2384,x2385,x2382)+~E(x2381,x2382)+~P11(x2383,x2384,x2385,x2381)
% 58.77/58.88 [239]P15(x2392,x2393,x2394)+~E(x2391,x2392)+~P15(x2391,x2393,x2394)
% 58.77/58.88 [240]P15(x2403,x2402,x2404)+~E(x2401,x2402)+~P15(x2403,x2401,x2404)
% 58.77/58.88 [241]P15(x2413,x2414,x2412)+~E(x2411,x2412)+~P15(x2413,x2414,x2411)
% 58.77/58.88 [242]P5(x2422,x2423,x2424,x2425,x2426)+~E(x2421,x2422)+~P5(x2421,x2423,x2424,x2425,x2426)
% 58.77/58.88 [243]P5(x2433,x2432,x2434,x2435,x2436)+~E(x2431,x2432)+~P5(x2433,x2431,x2434,x2435,x2436)
% 58.77/58.88 [244]P5(x2443,x2444,x2442,x2445,x2446)+~E(x2441,x2442)+~P5(x2443,x2444,x2441,x2445,x2446)
% 58.77/58.88 [245]P5(x2453,x2454,x2455,x2452,x2456)+~E(x2451,x2452)+~P5(x2453,x2454,x2455,x2451,x2456)
% 58.77/58.88 [246]P5(x2463,x2464,x2465,x2466,x2462)+~E(x2461,x2462)+~P5(x2463,x2464,x2465,x2466,x2461)
% 58.77/58.88 [247]P8(x2472,x2473)+~E(x2471,x2472)+~P8(x2471,x2473)
% 58.77/58.88 [248]P8(x2483,x2482)+~E(x2481,x2482)+~P8(x2483,x2481)
% 58.77/58.88 [249]P4(x2492,x2493,x2494,x2495)+~E(x2491,x2492)+~P4(x2491,x2493,x2494,x2495)
% 58.77/58.88 [250]P4(x2503,x2502,x2504,x2505)+~E(x2501,x2502)+~P4(x2503,x2501,x2504,x2505)
% 58.77/58.88 [251]P4(x2513,x2514,x2512,x2515)+~E(x2511,x2512)+~P4(x2513,x2514,x2511,x2515)
% 58.77/58.88 [252]P4(x2523,x2524,x2525,x2522)+~E(x2521,x2522)+~P4(x2523,x2524,x2525,x2521)
% 58.77/58.88
% 58.77/58.88 %-------------------------------------------
% 58.77/58.88 cnf(391,plain,
% 58.77/58.88 (P13(x3911,f49(x3911))),
% 58.77/58.88 inference(equality_inference,[],[258])).
% 58.77/58.88 cnf(392,plain,
% 58.77/58.88 (P13(x3921,f57(x3922,x3921))),
% 58.77/58.88 inference(equality_inference,[],[263])).
% 58.77/58.88 cnf(393,plain,
% 58.77/58.88 (P13(x3931,f57(x3931,x3932))),
% 58.77/58.88 inference(equality_inference,[],[264])).
% 58.77/58.88 cnf(394,plain,
% 58.77/58.88 (P1(a4,x3941)),
% 58.77/58.88 inference(scs_inference,[],[257,266])).
% 58.77/58.88 cnf(395,plain,
% 58.77/58.88 (~P13(x3951,a4)),
% 58.77/58.88 inference(rename_variables,[],[257])).
% 58.77/58.88 cnf(397,plain,
% 58.77/58.88 (P8(x3971,a4)),
% 58.77/58.88 inference(scs_inference,[],[257,395,266,267])).
% 58.77/58.88 cnf(398,plain,
% 58.77/58.88 (~P13(x3981,a4)),
% 58.77/58.88 inference(rename_variables,[],[257])).
% 58.77/58.88 cnf(400,plain,
% 58.77/58.88 (~P13(x4001,f59(a4))),
% 58.77/58.88 inference(scs_inference,[],[257,395,398,266,267,277])).
% 58.77/58.88 cnf(401,plain,
% 58.77/58.88 (~P13(x4011,a4)),
% 58.77/58.88 inference(rename_variables,[],[257])).
% 58.77/58.88 cnf(403,plain,
% 58.77/58.88 (P9(x4031,a4,x4032)),
% 58.77/58.88 inference(scs_inference,[],[257,395,398,401,266,267,277,292])).
% 58.77/58.88 cnf(404,plain,
% 58.77/58.88 (~P13(x4041,a4)),
% 58.77/58.88 inference(rename_variables,[],[257])).
% 58.77/58.88 cnf(406,plain,
% 58.77/58.88 (P9(x4061,f59(a4),x4062)),
% 58.77/58.88 inference(scs_inference,[],[257,395,398,401,266,267,277,292,293])).
% 58.77/58.88 cnf(408,plain,
% 58.77/58.88 (P9(x4081,x4082,a4)),
% 58.77/58.88 inference(scs_inference,[],[257,395,398,401,404,266,267,277,292,293,294])).
% 58.77/58.88 cnf(409,plain,
% 58.77/58.88 (~P13(x4091,a4)),
% 58.77/58.88 inference(rename_variables,[],[257])).
% 58.77/58.88 cnf(411,plain,
% 58.77/58.88 (P15(x4111,x4112,a4)),
% 58.77/58.88 inference(scs_inference,[],[257,395,398,401,404,409,266,267,277,292,293,294,295])).
% 58.77/58.88 cnf(412,plain,
% 58.77/58.88 (~P13(x4121,a4)),
% 58.77/58.88 inference(rename_variables,[],[257])).
% 58.77/58.88 cnf(414,plain,
% 58.77/58.88 (~P13(x4141,f42(x4142,a4))),
% 58.77/58.88 inference(scs_inference,[],[257,395,398,401,404,409,412,266,267,277,292,293,294,295,297])).
% 58.77/58.88 cnf(415,plain,
% 58.77/58.88 (~P13(x4151,a4)),
% 58.77/58.88 inference(rename_variables,[],[257])).
% 58.77/58.88 cnf(417,plain,
% 58.77/58.88 (~P13(x4171,f53(x4172,a4))),
% 58.77/58.88 inference(scs_inference,[],[257,395,398,401,404,409,412,415,266,267,277,292,293,294,295,297,298])).
% 58.77/58.88 cnf(418,plain,
% 58.77/58.88 (~P13(x4181,a4)),
% 58.77/58.88 inference(rename_variables,[],[257])).
% 58.77/58.88 cnf(420,plain,
% 58.77/58.88 (~P13(x4201,f52(x4202,a4,x4203))),
% 58.77/58.88 inference(scs_inference,[],[257,395,398,401,404,409,412,415,418,266,267,277,292,293,294,295,297,298,333])).
% 58.77/58.88 cnf(421,plain,
% 58.77/58.88 (~P13(x4211,a4)),
% 58.77/58.88 inference(rename_variables,[],[257])).
% 58.77/58.88 cnf(423,plain,
% 58.77/58.88 (~P13(x4231,f55(x4232,a4,x4233))),
% 58.77/58.88 inference(scs_inference,[],[257,395,398,401,404,409,412,415,418,421,266,267,277,292,293,294,295,297,298,333,334])).
% 58.77/58.88 cnf(424,plain,
% 58.77/58.88 (~P13(x4241,a4)),
% 58.77/58.88 inference(rename_variables,[],[257])).
% 58.77/58.88 cnf(427,plain,
% 58.77/58.88 (~P13(x4271,a4)),
% 58.77/58.88 inference(rename_variables,[],[257])).
% 58.77/58.88 cnf(430,plain,
% 58.77/58.88 (~P13(x4301,a4)),
% 58.77/58.88 inference(rename_variables,[],[257])).
% 58.77/58.88 cnf(435,plain,
% 58.77/58.88 (~P13(x4351,a4)),
% 58.77/58.88 inference(rename_variables,[],[257])).
% 58.77/58.88 cnf(438,plain,
% 58.77/58.88 (~P13(x4381,a4)),
% 58.77/58.88 inference(rename_variables,[],[257])).
% 58.77/58.88 cnf(441,plain,
% 58.77/58.88 (~P13(x4411,a4)),
% 58.77/58.88 inference(rename_variables,[],[257])).
% 58.77/58.88 cnf(444,plain,
% 58.77/58.88 (~P13(x4441,a4)),
% 58.77/58.88 inference(rename_variables,[],[257])).
% 58.77/58.88 cnf(451,plain,
% 58.77/58.88 (~P13(x4511,a4)),
% 58.77/58.88 inference(rename_variables,[],[257])).
% 58.77/58.88 cnf(454,plain,
% 58.77/58.88 (~P13(x4541,a4)),
% 58.77/58.88 inference(rename_variables,[],[257])).
% 58.77/58.88 cnf(459,plain,
% 58.77/58.88 (~P13(x4591,a4)),
% 58.77/58.88 inference(rename_variables,[],[257])).
% 58.77/58.88 cnf(462,plain,
% 58.77/58.88 (~P13(x4621,a4)),
% 58.77/58.88 inference(rename_variables,[],[257])).
% 58.77/58.88 cnf(464,plain,
% 58.77/58.88 (P2(a4,a4)),
% 58.77/58.88 inference(scs_inference,[],[257,395,398,401,404,409,412,415,418,421,424,427,430,435,438,441,444,451,454,459,266,267,277,292,293,294,295,297,298,333,334,337,338,339,340,341,354,355,356,357,358,359,360,379,380,269])).
% 58.77/58.88 cnf(466,plain,
% 58.77/58.88 (~P7(x4661,f49(x4662),a4)),
% 58.77/58.88 inference(scs_inference,[],[391,257,395,398,401,404,409,412,415,418,421,424,427,430,435,438,441,444,451,454,459,462,266,267,277,292,293,294,295,297,298,333,334,337,338,339,340,341,354,355,356,357,358,359,360,379,380,269,328])).
% 58.77/58.88 cnf(467,plain,
% 58.77/58.88 (~P13(x4671,a4)),
% 58.77/58.88 inference(rename_variables,[],[257])).
% 58.77/58.88 cnf(470,plain,
% 58.77/58.88 (~P15(x4701,a4,f49(x4702))),
% 58.77/58.88 inference(scs_inference,[],[256,254,391,257,395,398,401,404,409,412,415,418,421,424,427,430,435,438,441,444,451,454,459,462,467,266,267,277,292,293,294,295,297,298,333,334,337,338,339,340,341,354,355,356,357,358,359,360,379,380,269,328,203,329])).
% 58.77/58.88 cnf(471,plain,
% 58.77/58.88 (~P13(x4711,a4)),
% 58.77/58.88 inference(rename_variables,[],[257])).
% 58.77/58.88 cnf(475,plain,
% 58.77/58.88 (~E(f49(x4751),a4)),
% 58.77/58.88 inference(scs_inference,[],[256,254,391,257,395,398,401,404,409,412,415,418,421,424,427,430,435,438,441,444,451,454,459,462,467,471,266,267,277,292,293,294,295,297,298,333,334,337,338,339,340,341,354,355,356,357,358,359,360,379,380,269,328,203,329,304,212])).
% 58.77/58.88 cnf(476,plain,
% 58.77/58.88 (P13(x4761,f49(x4761))),
% 58.77/58.88 inference(rename_variables,[],[391])).
% 58.77/58.88 cnf(478,plain,
% 58.77/58.88 (~P3(f6(x4781,x4782,f49(x4783),a4,f49(x4783)),x4783,x4783)),
% 58.77/58.88 inference(scs_inference,[],[256,254,391,476,257,395,398,401,404,409,412,415,418,421,424,427,430,435,438,441,444,451,454,459,462,467,471,266,267,277,292,293,294,295,297,298,333,334,337,338,339,340,341,354,355,356,357,358,359,360,379,380,269,328,203,329,304,212,241,384])).
% 58.77/58.88 cnf(481,plain,
% 58.77/58.88 (~P13(x4811,a1)+P13(x4811,a2)),
% 58.77/58.88 inference(scs_inference,[],[253,256,254,391,476,257,395,398,401,404,409,412,415,418,421,424,427,430,435,438,441,444,451,454,459,462,467,471,266,267,277,292,293,294,295,297,298,333,334,337,338,339,340,341,354,355,356,357,358,359,360,379,380,269,328,203,329,304,212,241,384,268])).
% 58.77/58.88 cnf(483,plain,
% 58.77/58.88 (~P8(f6(x4831,x4832,f49(x4833),a4,f49(x4833)),f49(x4833))),
% 58.77/58.88 inference(scs_inference,[],[253,256,254,391,476,257,395,398,401,404,409,412,415,418,421,424,427,430,435,438,441,444,451,454,459,462,467,471,266,267,277,292,293,294,295,297,298,333,334,337,338,339,340,341,354,355,356,357,358,359,360,379,380,269,328,203,329,304,212,241,384,268,287])).
% 58.77/58.88 cnf(497,plain,
% 58.77/58.88 (~P13(x4971,f52(x4972,a4,x4973))),
% 58.77/58.88 inference(rename_variables,[],[420])).
% 58.77/58.88 cnf(499,plain,
% 58.77/58.88 (~P13(x4991,f59(f52(x4992,a4,x4993)))),
% 58.77/58.88 inference(scs_inference,[],[466,470,420,497,289,345,346,361,277])).
% 58.77/58.88 cnf(500,plain,
% 58.77/58.88 (~P13(x5001,f52(x5002,a4,x5003))),
% 58.77/58.88 inference(rename_variables,[],[420])).
% 58.77/58.88 cnf(503,plain,
% 58.77/58.88 (~P13(x5031,f55(x5032,a4,x5033))),
% 58.77/58.88 inference(rename_variables,[],[423])).
% 58.77/58.88 cnf(505,plain,
% 58.77/58.88 (~P13(x5051,f55(x5052,f52(x5053,a4,x5054),x5055))),
% 58.77/58.88 inference(scs_inference,[],[466,470,420,497,500,423,289,345,346,361,277,357,334])).
% 58.77/58.88 cnf(506,plain,
% 58.77/58.88 (~P13(x5061,f52(x5062,a4,x5063))),
% 58.77/58.88 inference(rename_variables,[],[420])).
% 58.77/58.88 cnf(508,plain,
% 58.77/58.88 (P9(x5081,x5082,f52(x5083,a4,x5084))),
% 58.77/58.88 inference(scs_inference,[],[466,470,420,497,500,506,423,289,345,346,361,277,357,334,294])).
% 58.77/58.88 cnf(509,plain,
% 58.77/58.88 (~P13(x5091,f52(x5092,a4,x5093))),
% 58.77/58.88 inference(rename_variables,[],[420])).
% 58.77/58.88 cnf(512,plain,
% 58.77/58.88 (~P13(x5121,f52(x5122,a4,x5123))),
% 58.77/58.88 inference(rename_variables,[],[420])).
% 58.77/58.88 cnf(515,plain,
% 58.77/58.88 (~P13(x5151,f52(x5152,a4,x5153))),
% 58.77/58.88 inference(rename_variables,[],[420])).
% 58.77/58.88 cnf(518,plain,
% 58.77/58.88 (~P13(x5181,f52(x5182,a4,x5183))),
% 58.77/58.88 inference(rename_variables,[],[420])).
% 58.77/58.88 cnf(520,plain,
% 58.77/58.88 (P1(f52(x5201,a4,x5202),x5203)),
% 58.77/58.88 inference(scs_inference,[],[466,470,420,497,500,506,509,512,515,518,423,289,345,346,361,277,357,334,294,341,356,338,266])).
% 58.77/58.88 cnf(521,plain,
% 58.77/58.88 (~P13(x5211,f52(x5212,a4,x5213))),
% 58.77/58.88 inference(rename_variables,[],[420])).
% 58.77/58.88 cnf(524,plain,
% 58.77/58.88 (~P13(x5241,f55(x5242,a4,x5243))),
% 58.77/58.88 inference(rename_variables,[],[423])).
% 58.77/58.88 cnf(527,plain,
% 58.77/58.88 (~P13(x5271,f52(x5272,a4,x5273))),
% 58.77/58.88 inference(rename_variables,[],[420])).
% 58.77/58.88 cnf(530,plain,
% 58.77/58.88 (~P13(x5301,f52(x5302,a4,x5303))),
% 58.77/58.88 inference(rename_variables,[],[420])).
% 58.77/58.88 cnf(533,plain,
% 58.77/58.88 (~P13(x5331,f55(x5332,a4,x5333))),
% 58.77/58.88 inference(rename_variables,[],[423])).
% 58.77/58.88 cnf(536,plain,
% 58.77/58.88 (~P13(x5361,f42(x5362,a4))),
% 58.77/58.88 inference(rename_variables,[],[414])).
% 58.77/58.88 cnf(539,plain,
% 58.77/58.88 (~P13(x5391,f52(x5392,a4,x5393))),
% 58.77/58.88 inference(rename_variables,[],[420])).
% 58.77/58.88 cnf(542,plain,
% 58.77/58.88 (~P13(x5421,f55(x5422,a4,x5423))),
% 58.77/58.88 inference(rename_variables,[],[423])).
% 58.77/58.88 cnf(544,plain,
% 58.77/58.88 (P8(x5441,f52(x5442,a4,x5443))),
% 58.77/58.88 inference(scs_inference,[],[466,470,420,497,500,506,509,512,515,518,521,527,530,539,423,503,524,533,414,289,345,346,361,277,357,334,294,341,356,338,266,354,337,298,359,355,380,339,267])).
% 58.77/58.88 cnf(545,plain,
% 58.77/58.88 (~P13(x5451,f52(x5452,a4,x5453))),
% 58.77/58.88 inference(rename_variables,[],[420])).
% 58.77/58.88 cnf(548,plain,
% 58.77/58.88 (~P13(x5481,f52(x5482,a4,x5483))),
% 58.77/58.88 inference(rename_variables,[],[420])).
% 58.77/58.88 cnf(553,plain,
% 58.77/58.88 (P9(x5531,f52(x5532,a4,x5533),x5534)),
% 58.77/58.88 inference(scs_inference,[],[466,470,420,497,500,506,509,512,515,518,521,527,530,539,545,548,423,503,524,533,414,536,289,345,346,361,277,357,334,294,341,356,338,266,354,337,298,359,355,380,339,267,358,360,293])).
% 58.77/58.88 cnf(554,plain,
% 58.77/58.88 (~P13(x5541,f52(x5542,a4,x5543))),
% 58.77/58.88 inference(rename_variables,[],[420])).
% 58.77/58.88 cnf(557,plain,
% 58.77/58.88 (~P13(x5571,f52(x5572,a4,x5573))),
% 58.77/58.88 inference(rename_variables,[],[420])).
% 58.77/58.88 cnf(559,plain,
% 58.77/58.88 (P9(x5591,f55(x5592,a4,x5593),x5594)),
% 58.77/58.88 inference(scs_inference,[],[466,470,420,497,500,506,509,512,515,518,521,527,530,539,545,548,554,423,503,524,533,542,414,536,289,345,346,361,277,357,334,294,341,356,338,266,354,337,298,359,355,380,339,267,358,360,293,297,292])).
% 58.77/58.88 cnf(560,plain,
% 58.77/58.88 (~P13(x5601,f55(x5602,a4,x5603))),
% 58.77/58.88 inference(rename_variables,[],[423])).
% 58.77/58.88 cnf(562,plain,
% 58.77/58.88 (P15(x5621,x5622,f52(x5623,a4,x5624))),
% 58.77/58.88 inference(scs_inference,[],[466,470,420,497,500,506,509,512,515,518,521,527,530,539,545,548,554,557,423,503,524,533,542,414,536,289,345,346,361,277,357,334,294,341,356,338,266,354,337,298,359,355,380,339,267,358,360,293,297,292,295])).
% 58.77/58.88 cnf(563,plain,
% 58.77/58.88 (~P13(x5631,f52(x5632,a4,x5633))),
% 58.77/58.88 inference(rename_variables,[],[420])).
% 58.77/58.88 cnf(566,plain,
% 58.77/58.88 (~P13(x5661,f52(x5662,a4,x5663))),
% 58.77/58.88 inference(rename_variables,[],[420])).
% 58.77/58.88 cnf(569,plain,
% 58.77/58.88 (~P13(x5691,f52(x5692,a4,x5693))),
% 58.77/58.88 inference(rename_variables,[],[420])).
% 58.77/58.88 cnf(572,plain,
% 58.77/58.88 (~P13(x5721,f52(x5722,a4,x5723))),
% 58.77/58.88 inference(rename_variables,[],[420])).
% 58.77/58.88 cnf(574,plain,
% 58.77/58.88 (P7(x5741,f52(x5742,a4,x5743),f55(x5744,a4,x5745))),
% 58.77/58.88 inference(scs_inference,[],[466,470,420,497,500,506,509,512,515,518,521,527,530,539,545,548,554,557,563,566,569,572,423,503,524,533,542,560,414,536,289,345,346,361,277,357,334,294,341,356,338,266,354,337,298,359,355,380,339,267,358,360,293,297,292,295,379,333,340,310])).
% 58.77/58.88 cnf(575,plain,
% 58.77/58.88 (~P13(x5751,f52(x5752,a4,x5753))),
% 58.77/58.88 inference(rename_variables,[],[420])).
% 58.77/58.88 cnf(576,plain,
% 58.77/58.88 (~P13(x5761,f55(x5762,a4,x5763))),
% 58.77/58.88 inference(rename_variables,[],[423])).
% 58.77/58.88 cnf(579,plain,
% 58.77/58.88 (~P7(x5791,f57(x5792,x5793),f52(x5794,a4,x5795))),
% 58.77/58.88 inference(scs_inference,[],[466,483,470,392,420,497,500,506,509,512,515,518,521,527,530,539,545,548,554,557,563,566,569,572,575,423,503,524,533,542,560,414,536,289,345,346,361,277,357,334,294,341,356,338,266,354,337,298,359,355,380,339,267,358,360,293,297,292,295,379,333,340,310,248,328])).
% 58.77/58.88 cnf(580,plain,
% 58.77/58.88 (~P13(x5801,f52(x5802,a4,x5803))),
% 58.77/58.88 inference(rename_variables,[],[420])).
% 58.77/58.88 cnf(582,plain,
% 58.77/58.88 (~P15(x5821,f52(x5822,a4,x5823),f57(x5824,x5825))),
% 58.77/58.88 inference(scs_inference,[],[466,483,470,392,420,497,500,506,509,512,515,518,521,527,530,539,545,548,554,557,563,566,569,572,575,580,423,503,524,533,542,560,414,536,289,345,346,361,277,357,334,294,341,356,338,266,354,337,298,359,355,380,339,267,358,360,293,297,292,295,379,333,340,310,248,328,329])).
% 58.77/58.88 cnf(583,plain,
% 58.77/58.88 (~P13(x5831,f52(x5832,a4,x5833))),
% 58.77/58.88 inference(rename_variables,[],[420])).
% 58.77/58.88 cnf(585,plain,
% 58.77/58.88 (P2(f52(x5851,a4,x5852),a4)),
% 58.77/58.88 inference(scs_inference,[],[466,483,470,394,392,420,497,500,506,509,512,515,518,521,527,530,539,545,548,554,557,563,566,569,572,575,580,423,503,524,533,542,560,414,536,289,345,346,361,277,357,334,294,341,356,338,266,354,337,298,359,355,380,339,267,358,360,293,297,292,295,379,333,340,310,248,328,329,269])).
% 58.77/58.88 cnf(588,plain,
% 58.77/58.88 (~P8(f6(x5881,x5882,f49(x5883),a4,f49(x5883)),f57(x5884,x5883))),
% 58.77/58.88 inference(scs_inference,[],[466,478,483,470,394,392,420,497,500,506,509,512,515,518,521,527,530,539,545,548,554,557,563,566,569,572,575,580,423,503,524,533,542,560,414,536,289,345,346,361,277,357,334,294,341,356,338,266,354,337,298,359,355,380,339,267,358,360,293,297,292,295,379,333,340,310,248,328,329,269,287])).
% 58.77/58.88 cnf(589,plain,
% 58.77/58.88 (P13(x5891,f57(x5892,x5891))),
% 58.77/58.88 inference(rename_variables,[],[392])).
% 58.77/58.88 cnf(591,plain,
% 58.77/58.88 (P14(x5911,f59(a4),a4)),
% 58.77/58.88 inference(scs_inference,[],[466,478,483,470,394,392,420,497,500,506,509,512,515,518,521,527,530,539,545,548,554,557,563,566,569,572,575,580,423,503,524,533,542,560,414,536,406,411,289,345,346,361,277,357,334,294,341,356,338,266,354,337,298,359,355,380,339,267,358,360,293,297,292,295,379,333,340,310,248,328,329,269,287,304])).
% 58.77/58.88 cnf(596,plain,
% 58.77/58.88 (P13(x5961,f57(x5962,x5961))),
% 58.77/58.88 inference(rename_variables,[],[392])).
% 58.77/58.88 cnf(597,plain,
% 58.77/58.88 (~E(a4,a1)),
% 58.77/58.88 inference(scs_inference,[],[256,466,464,478,483,470,394,392,589,420,497,500,506,509,512,515,518,521,527,530,539,545,548,554,557,563,566,569,572,575,580,583,423,503,524,533,542,560,414,536,406,411,289,345,346,361,277,357,334,294,341,356,338,266,354,337,298,359,355,380,339,267,358,360,293,297,292,295,379,333,340,310,248,328,329,269,287,304,212,203])).
% 58.77/58.88 cnf(598,plain,
% 58.77/58.88 (P7(x5981,f55(x5982,a4,x5983),f52(x5984,a4,x5985))),
% 58.77/58.88 inference(scs_inference,[],[256,466,464,478,483,470,394,392,589,420,497,500,506,509,512,515,518,521,527,530,539,545,548,554,557,563,566,569,572,575,580,583,423,503,524,533,542,560,576,414,536,406,411,289,345,346,361,277,357,334,294,341,356,338,266,354,337,298,359,355,380,339,267,358,360,293,297,292,295,379,333,340,310,248,328,329,269,287,304,212,203,309])).
% 58.77/58.88 cnf(600,plain,
% 58.77/58.88 (~P13(x6001,f52(x6002,a4,x6003))),
% 58.77/58.88 inference(rename_variables,[],[420])).
% 58.77/58.88 cnf(602,plain,
% 58.94/58.88 (~P3(f6(x6021,x6022,f57(x6023,x6024),f52(x6025,a4,x6026),f57(x6023,x6024)),x6024,x6024)),
% 58.94/58.88 inference(scs_inference,[],[256,466,464,478,483,470,394,392,589,596,420,497,500,506,509,512,515,518,521,527,530,539,545,548,554,557,563,566,569,572,575,580,583,600,423,503,524,533,542,560,576,414,536,406,411,289,345,346,361,277,357,334,294,341,356,338,266,354,337,298,359,355,380,339,267,358,360,293,297,292,295,379,333,340,310,248,328,329,269,287,304,212,203,309,384])).
% 58.94/58.88 cnf(616,plain,
% 58.94/58.88 (~P13(x6161,f59(a4))),
% 58.94/58.88 inference(rename_variables,[],[400])).
% 58.94/58.88 cnf(621,plain,
% 58.94/58.88 (~P13(x6211,f59(a4))),
% 58.94/58.88 inference(rename_variables,[],[400])).
% 58.94/58.88 cnf(624,plain,
% 58.94/58.88 (~P13(x6241,f59(a4))),
% 58.94/58.88 inference(rename_variables,[],[400])).
% 58.94/58.88 cnf(627,plain,
% 58.94/58.88 (~P13(x6271,f59(a4))),
% 58.94/58.88 inference(rename_variables,[],[400])).
% 58.94/58.88 cnf(630,plain,
% 58.94/58.88 (~P13(x6301,f59(a4))),
% 58.94/58.88 inference(rename_variables,[],[400])).
% 58.94/58.88 cnf(634,plain,
% 58.94/58.88 (P1(f59(a4),x6341)),
% 58.94/58.88 inference(scs_inference,[],[579,582,400,616,621,624,627,630,357,289,338,341,354,359,345,266])).
% 58.94/58.88 cnf(635,plain,
% 58.94/58.88 (~P13(x6351,f59(a4))),
% 58.94/58.88 inference(rename_variables,[],[400])).
% 58.94/58.88 cnf(637,plain,
% 58.94/58.88 (P8(x6371,f59(a4))),
% 58.94/58.88 inference(scs_inference,[],[579,582,400,616,621,624,627,630,635,357,289,338,341,354,359,345,266,267])).
% 58.94/58.88 cnf(638,plain,
% 58.94/58.88 (~P13(x6381,f59(a4))),
% 58.94/58.88 inference(rename_variables,[],[400])).
% 58.94/58.88 cnf(641,plain,
% 58.94/58.88 (~P13(x6411,f53(x6412,a4))),
% 58.94/58.88 inference(rename_variables,[],[417])).
% 58.94/58.88 cnf(644,plain,
% 58.94/58.88 (~P13(x6441,f42(x6442,a4))),
% 58.94/58.88 inference(rename_variables,[],[414])).
% 58.94/58.88 cnf(647,plain,
% 58.94/58.88 (~P13(x6471,f59(a4))),
% 58.94/58.88 inference(rename_variables,[],[400])).
% 58.94/58.88 cnf(650,plain,
% 58.94/58.88 (~P13(x6501,f53(x6502,a4))),
% 58.94/58.88 inference(rename_variables,[],[417])).
% 58.94/58.88 cnf(652,plain,
% 58.94/58.88 (P9(x6521,x6522,f59(a4))),
% 58.94/58.88 inference(scs_inference,[],[579,582,400,616,621,624,627,630,635,638,647,414,417,641,357,289,338,341,354,359,345,266,267,339,361,277,355,294])).
% 58.94/58.88 cnf(653,plain,
% 58.94/58.88 (~P13(x6531,f59(a4))),
% 58.94/58.88 inference(rename_variables,[],[400])).
% 58.94/58.88 cnf(656,plain,
% 58.94/58.88 (~P13(x6561,f59(a4))),
% 58.94/58.88 inference(rename_variables,[],[400])).
% 58.94/58.88 cnf(659,plain,
% 58.94/58.88 (~P13(x6591,f59(a4))),
% 58.94/58.88 inference(rename_variables,[],[400])).
% 58.94/58.88 cnf(662,plain,
% 58.94/58.88 (~P13(x6621,f59(a4))),
% 58.94/58.88 inference(rename_variables,[],[400])).
% 58.94/58.88 cnf(665,plain,
% 58.94/58.88 (~P13(x6651,f42(x6652,a4))),
% 58.94/58.88 inference(rename_variables,[],[414])).
% 58.94/58.88 cnf(668,plain,
% 58.94/58.88 (~P13(x6681,f59(a4))),
% 58.94/58.88 inference(rename_variables,[],[400])).
% 58.94/58.88 cnf(671,plain,
% 58.94/58.88 (~P13(x6711,f59(a4))),
% 58.94/58.88 inference(rename_variables,[],[400])).
% 58.94/58.88 cnf(674,plain,
% 58.94/58.88 (~P13(x6741,f53(x6742,a4))),
% 58.94/58.88 inference(rename_variables,[],[417])).
% 58.94/58.88 cnf(677,plain,
% 58.94/58.88 (~P13(x6771,f59(a4))),
% 58.94/58.88 inference(rename_variables,[],[400])).
% 58.94/58.88 cnf(680,plain,
% 58.94/58.88 (~P13(x6801,f59(a4))),
% 58.94/58.88 inference(rename_variables,[],[400])).
% 58.94/58.88 cnf(682,plain,
% 58.94/58.88 (P9(x6821,f42(x6822,a4),x6823)),
% 58.94/58.88 inference(scs_inference,[],[579,582,400,616,621,624,627,630,635,638,647,653,656,659,662,668,671,677,414,644,665,417,641,650,357,289,338,341,354,359,345,266,267,339,361,277,355,294,337,379,334,356,380,360,358,298,333,292])).
% 58.94/58.88 cnf(685,plain,
% 58.94/58.88 (P9(x6851,f53(x6852,a4),x6853)),
% 58.94/58.88 inference(scs_inference,[],[579,582,400,616,621,624,627,630,635,638,647,653,656,659,662,668,671,677,414,644,665,417,641,650,674,357,289,338,341,354,359,345,266,267,339,361,277,355,294,337,379,334,356,380,360,358,298,333,292,293])).
% 58.94/58.88 cnf(689,plain,
% 58.94/58.88 (~P13(x6891,f59(a4))),
% 58.94/58.88 inference(rename_variables,[],[400])).
% 58.94/58.88 cnf(691,plain,
% 58.94/58.88 (P15(x6911,x6912,f59(a4))),
% 58.94/58.88 inference(scs_inference,[],[579,582,400,616,621,624,627,630,635,638,647,653,656,659,662,668,671,677,680,689,414,644,665,417,641,650,674,357,289,338,341,354,359,345,266,267,339,361,277,355,294,337,379,334,356,380,360,358,298,333,292,293,340,295])).
% 58.94/58.88 cnf(692,plain,
% 58.94/58.88 (~P13(x6921,f59(a4))),
% 58.94/58.88 inference(rename_variables,[],[400])).
% 58.94/58.88 cnf(695,plain,
% 58.94/58.88 (~P13(x6951,f59(a4))),
% 58.94/58.88 inference(rename_variables,[],[400])).
% 58.94/58.88 cnf(698,plain,
% 58.94/58.88 (~P13(x6981,f59(a4))),
% 58.94/58.88 inference(rename_variables,[],[400])).
% 58.94/58.88 cnf(703,plain,
% 58.94/58.88 (~P15(x7031,f59(a4),f57(x7032,x7033))),
% 58.94/58.88 inference(scs_inference,[],[579,588,582,400,616,621,624,627,630,635,638,647,653,656,659,662,668,671,677,680,689,692,695,698,393,505,544,414,644,665,417,641,650,674,357,289,338,341,354,359,345,266,267,339,361,277,355,294,337,379,334,356,380,360,358,298,333,292,293,340,295,297,310,248,329])).
% 58.94/58.88 cnf(704,plain,
% 58.94/58.88 (~P13(x7041,f59(a4))),
% 58.94/58.88 inference(rename_variables,[],[400])).
% 58.94/58.88 cnf(706,plain,
% 58.94/58.88 (~P7(x7061,f57(x7062,x7063),f59(a4))),
% 58.94/58.88 inference(scs_inference,[],[579,588,582,400,616,621,624,627,630,635,638,647,653,656,659,662,668,671,677,680,689,692,695,698,704,393,505,544,414,644,665,417,641,650,674,357,289,338,341,354,359,345,266,267,339,361,277,355,294,337,379,334,356,380,360,358,298,333,292,293,340,295,297,310,248,329,328])).
% 58.94/58.88 cnf(707,plain,
% 58.94/58.88 (~P13(x7071,f59(a4))),
% 58.94/58.88 inference(rename_variables,[],[400])).
% 58.94/58.88 cnf(710,plain,
% 58.94/58.88 (P7(x7101,f55(x7102,a4,x7103),f52(x7104,a4,x7105))),
% 58.94/58.88 inference(rename_variables,[],[598])).
% 58.94/58.88 cnf(717,plain,
% 58.94/58.88 (~P8(f6(x7171,x7172,f57(x7173,x7174),f52(x7175,a4,x7176),f57(x7173,x7174)),f57(x7174,x7177))),
% 58.94/58.88 inference(scs_inference,[],[579,602,588,582,520,400,616,621,624,627,630,635,638,647,653,656,659,662,668,671,677,680,689,692,695,698,704,393,505,544,598,414,644,665,417,641,650,674,411,357,289,338,341,354,359,345,266,267,339,361,277,355,294,337,379,334,356,380,360,358,298,333,292,293,340,295,297,310,248,329,328,206,269,241,287])).
% 58.94/58.88 cnf(718,plain,
% 58.94/58.88 (P13(x7181,f57(x7181,x7182))),
% 58.94/58.88 inference(rename_variables,[],[393])).
% 58.94/58.88 cnf(721,plain,
% 58.94/58.88 (P13(x7211,f57(x7211,x7212))),
% 58.94/58.88 inference(rename_variables,[],[393])).
% 58.94/58.88 cnf(722,plain,
% 58.94/58.88 (P14(x7221,x7222,f52(x7223,a4,x7224))),
% 58.94/58.88 inference(scs_inference,[],[579,602,588,582,520,400,616,621,624,627,630,635,638,647,653,656,659,662,668,671,677,680,689,692,695,698,704,707,393,718,505,508,562,544,598,414,644,665,417,641,650,674,411,357,289,338,341,354,359,345,266,267,339,361,277,355,294,337,379,334,356,380,360,358,298,333,292,293,340,295,297,310,248,329,328,206,269,241,287,212,304])).
% 58.94/58.88 cnf(725,plain,
% 58.94/58.88 (P7(x7251,f52(x7252,a4,x7253),f59(a4))),
% 58.94/58.88 inference(scs_inference,[],[579,602,588,582,520,400,616,621,624,627,630,635,638,647,653,656,659,662,668,671,677,680,689,692,695,698,704,707,393,718,505,508,562,544,598,420,414,644,665,417,641,650,674,411,357,289,338,341,354,359,345,266,267,339,361,277,355,294,337,379,334,356,380,360,358,298,333,292,293,340,295,297,310,248,329,328,206,269,241,287,212,304,309])).
% 58.94/58.88 cnf(727,plain,
% 58.94/58.88 (~P13(x7271,f59(a4))),
% 58.94/58.88 inference(rename_variables,[],[400])).
% 58.94/58.88 cnf(733,plain,
% 58.94/58.88 (~P3(f6(x7331,x7332,f57(x7333,x7334),f59(a4),f57(x7333,x7334)),x7333,x7333)),
% 58.94/58.88 inference(scs_inference,[],[256,579,585,602,588,582,520,400,616,621,624,627,630,635,638,647,653,656,659,662,668,671,677,680,689,692,695,698,704,707,727,393,718,721,505,508,562,544,598,710,420,423,414,644,665,417,641,650,674,411,357,289,338,341,354,359,345,266,267,339,361,277,355,294,337,379,334,356,380,360,358,298,333,292,293,340,295,297,310,248,329,328,206,269,241,287,212,304,309,203,362,384])).
% 58.94/58.88 cnf(752,plain,
% 58.94/58.88 (~P13(x7521,f55(x7522,a4,x7523))),
% 58.94/58.88 inference(rename_variables,[],[423])).
% 58.94/58.88 cnf(755,plain,
% 58.94/58.88 (~P13(x7551,f55(x7552,a4,x7553))),
% 58.94/58.88 inference(rename_variables,[],[423])).
% 58.94/58.88 cnf(758,plain,
% 58.94/58.88 (~P13(x7581,f55(x7582,a4,x7583))),
% 58.94/58.88 inference(rename_variables,[],[423])).
% 58.94/58.88 cnf(763,plain,
% 58.94/58.88 (~P13(x7631,f55(x7632,a4,x7633))),
% 58.94/58.88 inference(rename_variables,[],[423])).
% 58.94/58.88 cnf(766,plain,
% 58.94/58.88 (~P13(x7661,f55(x7662,a4,x7663))),
% 58.94/58.88 inference(rename_variables,[],[423])).
% 58.94/58.88 cnf(769,plain,
% 58.94/58.88 (~P13(x7691,f55(x7692,a4,x7693))),
% 58.94/58.88 inference(rename_variables,[],[423])).
% 58.94/58.88 cnf(771,plain,
% 58.94/58.88 (P1(f55(x7711,a4,x7712),x7713)),
% 58.94/58.88 inference(scs_inference,[],[703,423,752,755,758,763,766,769,417,359,289,267,379,277,360,380,341,334,266])).
% 58.94/58.88 cnf(772,plain,
% 58.94/58.88 (~P13(x7721,f55(x7722,a4,x7723))),
% 58.94/58.88 inference(rename_variables,[],[423])).
% 58.94/58.88 cnf(774,plain,
% 58.94/58.88 (P9(x7741,x7742,f55(x7743,a4,x7744))),
% 58.94/58.88 inference(scs_inference,[],[703,423,752,755,758,763,766,769,772,417,359,289,267,379,277,360,380,341,334,266,294])).
% 58.94/58.88 cnf(775,plain,
% 58.94/58.88 (~P13(x7751,f55(x7752,a4,x7753))),
% 58.94/58.88 inference(rename_variables,[],[423])).
% 58.94/58.88 cnf(781,plain,
% 58.94/58.88 (P15(x7811,x7812,f55(x7813,a4,x7814))),
% 58.94/58.88 inference(scs_inference,[],[706,703,423,752,755,758,763,766,769,772,775,417,359,289,267,379,277,360,380,341,334,266,294,345,356,295])).
% 58.94/58.88 cnf(782,plain,
% 58.94/58.88 (~P13(x7821,f55(x7822,a4,x7823))),
% 58.94/58.88 inference(rename_variables,[],[423])).
% 58.94/58.88 cnf(785,plain,
% 58.94/58.88 (~P13(x7851,f55(x7852,a4,x7853))),
% 58.94/58.88 inference(rename_variables,[],[423])).
% 58.94/58.88 cnf(787,plain,
% 58.94/58.88 (P4(x7871,x7872,f55(x7873,a4,x7874),x7875)),
% 58.94/58.88 inference(scs_inference,[],[706,703,423,752,755,758,763,766,769,772,775,782,785,417,359,289,267,379,277,360,380,341,334,266,294,345,356,295,298,337])).
% 58.94/58.88 cnf(788,plain,
% 58.94/58.88 (~P13(x7881,f55(x7882,a4,x7883))),
% 58.94/58.88 inference(rename_variables,[],[423])).
% 58.94/58.88 cnf(793,plain,
% 58.94/58.88 (~P13(x7931,f55(x7932,a4,x7933))),
% 58.94/58.88 inference(rename_variables,[],[423])).
% 58.94/58.88 cnf(796,plain,
% 58.94/58.88 (~P13(x7961,f55(x7962,a4,x7963))),
% 58.94/58.88 inference(rename_variables,[],[423])).
% 58.94/58.88 cnf(798,plain,
% 58.94/58.88 (P11(x7981,x7982,f55(x7983,a4,x7984),x7985)),
% 58.94/58.88 inference(scs_inference,[],[706,703,423,752,755,758,763,766,769,772,775,782,785,788,793,796,417,359,289,267,379,277,360,380,341,334,266,294,345,356,295,298,337,358,333,297,340])).
% 58.94/58.88 cnf(799,plain,
% 58.94/58.88 (~P13(x7991,f55(x7992,a4,x7993))),
% 58.94/58.88 inference(rename_variables,[],[423])).
% 58.94/58.88 cnf(801,plain,
% 58.94/58.88 (P9(x8011,f52(x8012,f55(x8013,a4,x8014),x8015),x8016)),
% 58.94/58.88 inference(scs_inference,[],[706,703,423,752,755,758,763,766,769,772,775,782,785,788,793,796,417,359,289,267,379,277,360,380,341,334,266,294,345,356,295,298,337,358,333,297,340,292])).
% 58.94/58.88 cnf(803,plain,
% 58.94/58.88 (~P15(x8031,f59(a4),f49(x8032))),
% 58.94/58.88 inference(scs_inference,[],[706,703,400,423,752,755,758,763,766,769,772,775,782,785,788,793,796,417,391,359,289,267,379,277,360,380,341,334,266,294,345,356,295,298,337,358,333,297,340,292,329])).
% 58.94/58.88 cnf(804,plain,
% 58.94/58.88 (~P13(x8041,f59(a4))),
% 58.94/58.88 inference(rename_variables,[],[400])).
% 58.94/58.88 cnf(811,plain,
% 58.94/58.88 (~P13(x8111,f59(a4))),
% 58.94/58.88 inference(rename_variables,[],[400])).
% 58.94/58.88 cnf(814,plain,
% 58.94/58.89 (~P7(x8141,f49(x8142),f59(a4))),
% 58.94/58.89 inference(scs_inference,[],[706,394,703,634,400,804,811,499,423,752,755,758,763,766,769,772,775,782,785,788,793,796,417,391,359,289,267,379,277,360,380,341,334,266,294,345,356,295,298,337,358,333,297,340,292,329,269,310,328])).
% 58.94/58.89 cnf(815,plain,
% 58.94/58.89 (~P13(x8151,f59(a4))),
% 58.94/58.89 inference(rename_variables,[],[400])).
% 58.94/58.89 cnf(824,plain,
% 58.94/58.89 (P13(x8241,f49(x8241))),
% 58.94/58.89 inference(rename_variables,[],[391])).
% 58.94/58.89 cnf(825,plain,
% 58.94/58.89 (~P8(f6(x8251,x8252,f57(x8253,x8254),f59(a4),f57(x8253,x8254)),f49(x8253))),
% 58.94/58.89 inference(scs_inference,[],[706,394,717,733,703,634,400,804,811,815,499,553,691,637,423,752,755,758,763,766,769,772,775,782,785,788,793,796,417,391,824,359,289,267,379,277,360,380,341,334,266,294,345,356,295,298,337,358,333,297,340,292,329,269,310,328,248,304,212,287])).
% 58.94/58.89 cnf(826,plain,
% 58.94/58.89 (P13(x8261,f49(x8261))),
% 58.94/58.89 inference(rename_variables,[],[391])).
% 58.94/58.89 cnf(828,plain,
% 58.94/58.89 (P7(x8281,f55(x8282,a4,x8283),f59(a4))),
% 58.94/58.89 inference(scs_inference,[],[706,394,717,733,703,634,400,804,811,815,499,553,691,637,423,752,755,758,763,766,769,772,775,782,785,788,793,796,799,417,391,824,359,289,267,379,277,360,380,341,334,266,294,345,356,295,298,337,358,333,297,340,292,329,269,310,328,248,304,212,287,309])).
% 58.94/58.89 cnf(830,plain,
% 58.94/58.89 (~P13(x8301,f59(a4))),
% 58.94/58.89 inference(rename_variables,[],[400])).
% 58.94/58.89 cnf(834,plain,
% 58.94/58.89 (~P13(x8341,f59(a4))),
% 58.94/58.89 inference(rename_variables,[],[400])).
% 58.94/58.89 cnf(836,plain,
% 58.94/58.89 (~P3(f6(x8361,x8362,f49(x8363),f59(a4),f49(x8363)),x8363,x8363)),
% 58.94/58.89 inference(scs_inference,[],[256,706,394,717,733,703,634,400,804,811,815,830,834,499,553,691,725,637,423,752,755,758,763,766,769,772,775,782,785,788,793,796,799,417,391,824,826,359,289,267,379,277,360,380,341,334,266,294,345,356,295,298,337,358,333,297,340,292,329,269,310,328,248,304,212,287,309,203,363,384])).
% 58.94/58.89 cnf(847,plain,
% 58.94/58.89 (~P13(x8471,f42(x8472,a4))),
% 58.94/58.89 inference(rename_variables,[],[414])).
% 58.94/58.89 cnf(854,plain,
% 58.94/58.89 (~P13(x8541,f42(x8542,a4))),
% 58.94/58.89 inference(rename_variables,[],[414])).
% 58.94/58.89 cnf(857,plain,
% 58.94/58.89 (~P13(x8571,f42(x8572,a4))),
% 58.94/58.89 inference(rename_variables,[],[414])).
% 58.94/58.89 cnf(864,plain,
% 58.94/58.89 (~P13(x8641,f42(x8642,a4))),
% 58.94/58.89 inference(rename_variables,[],[414])).
% 58.94/58.89 cnf(867,plain,
% 58.94/58.89 (~P13(x8671,f42(x8672,a4))),
% 58.94/58.89 inference(rename_variables,[],[414])).
% 58.94/58.89 cnf(870,plain,
% 58.94/58.89 (~P13(x8701,f42(x8702,a4))),
% 58.94/58.89 inference(rename_variables,[],[414])).
% 58.94/58.89 cnf(875,plain,
% 58.94/58.89 (~P13(x8751,f42(x8752,a4))),
% 58.94/58.89 inference(rename_variables,[],[414])).
% 58.94/58.89 cnf(878,plain,
% 58.94/58.89 (~P13(x8781,f42(x8782,a4))),
% 58.94/58.89 inference(rename_variables,[],[414])).
% 58.94/58.89 cnf(880,plain,
% 58.94/58.89 (P15(x8801,x8802,f42(x8803,a4))),
% 58.94/58.89 inference(scs_inference,[],[814,803,414,847,854,857,864,867,870,875,878,267,289,346,294,334,339,345,379,277,337,293,341,380,295])).
% 58.94/58.89 cnf(881,plain,
% 58.94/58.89 (~P13(x8811,f42(x8812,a4))),
% 58.94/58.89 inference(rename_variables,[],[414])).
% 58.94/58.89 cnf(884,plain,
% 58.94/58.89 (~P13(x8841,f42(x8842,a4))),
% 58.94/58.89 inference(rename_variables,[],[414])).
% 58.94/58.89 cnf(887,plain,
% 58.94/58.89 (~P13(x8871,f42(x8872,a4))),
% 58.94/58.89 inference(rename_variables,[],[414])).
% 58.94/58.89 cnf(889,plain,
% 58.94/58.89 (P1(f42(x8891,a4),x8892)),
% 58.94/58.89 inference(scs_inference,[],[814,803,414,847,854,857,864,867,870,875,878,881,884,887,267,289,346,294,334,339,345,379,277,337,293,341,380,295,297,340,266])).
% 58.94/58.89 cnf(890,plain,
% 58.94/58.89 (~P13(x8901,f42(x8902,a4))),
% 58.94/58.89 inference(rename_variables,[],[414])).
% 58.94/58.89 cnf(893,plain,
% 58.94/58.89 (~P13(x8931,f42(x8932,a4))),
% 58.94/58.89 inference(rename_variables,[],[414])).
% 58.94/58.89 cnf(896,plain,
% 58.94/58.89 (~P13(x8961,f42(x8962,a4))),
% 58.94/58.89 inference(rename_variables,[],[414])).
% 58.94/58.89 cnf(900,plain,
% 58.94/58.89 (~P15(x9001,f42(x9002,a4),f57(x9003,x9004))),
% 58.94/58.89 inference(scs_inference,[],[814,803,414,847,854,857,864,867,870,875,878,881,884,887,890,893,896,392,267,289,346,294,334,339,345,379,277,337,293,341,380,295,297,340,266,333,298,292,329])).
% 58.94/58.89 cnf(901,plain,
% 58.94/58.89 (~P13(x9011,f42(x9012,a4))),
% 58.94/58.89 inference(rename_variables,[],[414])).
% 58.94/58.89 cnf(909,plain,
% 58.94/58.89 (P14(x9091,f52(x9092,f55(x9093,a4,x9094),x9095),a4)),
% 58.94/58.89 inference(scs_inference,[],[814,520,394,803,414,847,854,857,864,867,870,875,878,881,884,887,890,893,896,411,801,828,392,267,289,346,294,334,339,345,379,277,337,293,341,380,295,297,340,266,333,298,292,329,206,269,304])).
% 58.94/58.89 cnf(914,plain,
% 58.94/58.89 (~P13(x9141,f52(x9142,a4,x9143))),
% 58.94/58.89 inference(rename_variables,[],[420])).
% 58.94/58.89 cnf(915,plain,
% 58.94/58.89 (~P13(x9151,f42(x9152,a4))),
% 58.94/58.89 inference(rename_variables,[],[414])).
% 58.94/58.89 cnf(917,plain,
% 58.94/58.89 (~P7(x9171,f57(x9172,x9173),f42(x9174,a4))),
% 58.94/58.89 inference(scs_inference,[],[814,520,394,803,420,414,847,854,857,864,867,870,875,878,881,884,887,890,893,896,901,915,411,801,828,392,267,289,346,294,334,339,345,379,277,337,293,341,380,295,297,340,266,333,298,292,329,206,269,304,310,328])).
% 58.94/58.89 cnf(918,plain,
% 58.94/58.89 (~P13(x9181,f42(x9182,a4))),
% 58.94/58.89 inference(rename_variables,[],[414])).
% 58.94/58.89 cnf(923,plain,
% 58.94/58.89 (P13(x9231,f57(x9232,x9231))),
% 58.94/58.89 inference(rename_variables,[],[392])).
% 58.94/58.89 cnf(929,plain,
% 58.94/58.89 (~P13(x9291,f42(x9292,a4))),
% 58.94/58.89 inference(rename_variables,[],[414])).
% 58.94/58.89 cnf(933,plain,
% 58.94/58.89 (~P13(x9331,f42(x9332,a4))),
% 58.94/58.89 inference(rename_variables,[],[414])).
% 58.94/58.89 cnf(936,plain,
% 58.94/58.89 (~P3(f6(x9361,x9362,f57(x9363,x9364),f42(x9365,a4),f57(x9363,x9364)),x9364,x9364)),
% 58.94/58.89 inference(scs_inference,[],[814,520,394,836,825,803,420,914,414,847,854,857,864,867,870,875,878,881,884,887,890,893,896,901,915,918,929,933,722,411,801,828,691,392,923,391,267,289,346,294,334,339,345,379,277,337,293,341,380,295,297,340,266,333,298,292,329,206,269,304,310,328,241,287,248,212,309,364,384])).
% 58.94/58.89 cnf(948,plain,
% 58.94/58.89 (~P13(x9481,f53(x9482,a4))),
% 58.94/58.89 inference(rename_variables,[],[417])).
% 58.94/58.89 cnf(953,plain,
% 58.94/58.89 (~P13(x9531,f53(x9532,a4))),
% 58.94/58.89 inference(rename_variables,[],[417])).
% 58.94/58.89 cnf(956,plain,
% 58.94/58.89 (~P13(x9561,f53(x9562,a4))),
% 58.94/58.89 inference(rename_variables,[],[417])).
% 58.94/58.89 cnf(959,plain,
% 58.94/58.89 (~P13(x9591,f53(x9592,a4))),
% 58.94/58.89 inference(rename_variables,[],[417])).
% 58.94/58.89 cnf(961,plain,
% 58.94/58.89 (P11(x9611,x9612,x9613,f53(x9614,a4))),
% 58.94/58.89 inference(scs_inference,[],[900,417,948,953,956,959,267,289,277,294,380,341])).
% 58.94/58.89 cnf(962,plain,
% 58.94/58.89 (~P13(x9621,f53(x9622,a4))),
% 58.94/58.89 inference(rename_variables,[],[417])).
% 58.94/58.89 cnf(965,plain,
% 58.94/58.89 (~P13(x9651,f53(x9652,a4))),
% 58.94/58.89 inference(rename_variables,[],[417])).
% 58.94/58.89 cnf(968,plain,
% 58.94/58.89 (~P13(x9681,f53(x9682,a4))),
% 58.94/58.89 inference(rename_variables,[],[417])).
% 58.94/58.89 cnf(970,plain,
% 58.94/58.89 (P1(f53(x9701,a4),x9702)),
% 58.94/58.89 inference(scs_inference,[],[900,417,948,953,956,959,962,965,968,267,289,277,294,380,341,334,340,266])).
% 58.94/58.89 cnf(971,plain,
% 58.94/58.89 (~P13(x9711,f53(x9712,a4))),
% 58.94/58.89 inference(rename_variables,[],[417])).
% 58.94/58.89 cnf(974,plain,
% 58.94/58.89 (~P13(x9741,f53(x9742,a4))),
% 58.94/58.89 inference(rename_variables,[],[417])).
% 58.94/58.89 cnf(978,plain,
% 58.94/58.89 (P15(x9781,x9782,f53(x9783,a4))),
% 58.94/58.89 inference(scs_inference,[],[917,900,417,948,953,956,959,962,965,968,971,974,267,289,277,294,380,341,334,340,266,379,345,295])).
% 58.94/58.89 cnf(979,plain,
% 58.94/58.89 (~P13(x9791,f53(x9792,a4))),
% 58.94/58.89 inference(rename_variables,[],[417])).
% 58.94/58.89 cnf(982,plain,
% 58.94/58.89 (~P13(x9821,f53(x9822,a4))),
% 58.94/58.89 inference(rename_variables,[],[417])).
% 58.94/58.89 cnf(985,plain,
% 58.94/58.89 (~P13(x9851,f53(x9852,a4))),
% 58.94/58.89 inference(rename_variables,[],[417])).
% 58.94/58.89 cnf(990,plain,
% 58.94/58.89 (~P13(x9901,f53(x9902,a4))),
% 58.94/58.89 inference(rename_variables,[],[417])).
% 58.94/58.89 cnf(995,plain,
% 58.94/58.89 (~P15(x9951,a4,f57(x9952,x9953))),
% 58.94/58.89 inference(scs_inference,[],[917,900,257,417,948,953,956,959,962,965,968,971,974,979,982,985,990,393,267,289,277,294,380,341,334,340,266,379,345,295,298,337,292,333,297,329])).
% 58.94/58.89 cnf(996,plain,
% 58.94/58.89 (~P13(x9961,a4)),
% 58.94/58.89 inference(rename_variables,[],[257])).
% 58.94/58.89 cnf(1003,plain,
% 58.94/58.89 (~P13(x10031,a4)),
% 58.94/58.89 inference(rename_variables,[],[257])).
% 58.94/58.89 cnf(1004,plain,
% 58.94/58.89 (~P13(x10041,f59(a4))),
% 58.94/58.89 inference(rename_variables,[],[400])).
% 58.94/58.89 cnf(1006,plain,
% 58.94/58.89 (~P7(x10061,f57(x10062,x10063),a4)),
% 58.94/58.89 inference(scs_inference,[],[917,771,900,257,996,1003,400,417,948,953,956,959,962,965,968,971,974,979,982,985,990,393,267,289,277,294,380,341,334,340,266,379,345,295,298,337,292,333,297,329,269,310,328])).
% 58.94/58.89 cnf(1007,plain,
% 58.94/58.89 (~P13(x10071,a4)),
% 58.94/58.89 inference(rename_variables,[],[257])).
% 58.94/58.89 cnf(1015,plain,
% 58.94/58.89 (P13(x10151,f57(x10151,x10152))),
% 58.94/58.89 inference(rename_variables,[],[393])).
% 58.94/58.89 cnf(1018,plain,
% 58.94/58.89 (~P13(x10181,f59(a4))),
% 58.94/58.89 inference(rename_variables,[],[400])).
% 58.94/58.89 cnf(1019,plain,
% 58.94/58.89 (~P13(x10191,a4)),
% 58.94/58.89 inference(rename_variables,[],[257])).
% 58.94/58.89 cnf(1022,plain,
% 58.94/58.89 (P13(x10221,f57(x10221,x10222))),
% 58.94/58.89 inference(rename_variables,[],[393])).
% 58.94/58.89 cnf(1023,plain,
% 58.94/58.89 (P12(x10231,f59(a4),x10232,a4,x10233)),
% 58.94/58.89 inference(scs_inference,[],[917,771,936,900,257,996,1003,1007,1019,400,1004,1018,417,948,953,956,959,962,965,968,971,974,979,982,985,990,559,591,411,393,1015,267,289,277,294,380,341,334,340,266,379,345,295,298,337,292,333,297,329,269,310,328,241,304,287,309,212,362])).
% 58.94/58.89 cnf(1027,plain,
% 58.94/58.89 (~P3(f6(x10271,x10272,f57(x10273,x10274),a4,f57(x10273,x10274)),x10273,x10273)),
% 58.94/58.89 inference(scs_inference,[],[917,771,936,900,257,996,1003,1007,1019,400,1004,1018,417,948,953,956,959,962,965,968,971,974,979,982,985,990,559,591,411,393,1015,1022,267,289,277,294,380,341,334,340,266,379,345,295,298,337,292,333,297,329,269,310,328,241,304,287,309,212,362,384])).
% 58.94/58.89 cnf(1047,plain,
% 58.94/58.89 (~P15(x10471,f55(x10472,a4,x10473),f57(x10474,x10475))),
% 58.94/58.89 inference(scs_inference,[],[1006,995,423,392,289,345,329])).
% 58.94/58.89 cnf(1048,plain,
% 58.94/58.89 (~P13(x10481,f55(x10482,a4,x10483))),
% 58.94/58.89 inference(rename_variables,[],[423])).
% 58.94/58.89 cnf(1056,plain,
% 58.94/58.89 (~P13(x10561,f52(x10562,a4,x10563))),
% 58.94/58.89 inference(rename_variables,[],[420])).
% 58.94/58.89 cnf(1058,plain,
% 58.94/58.89 (~P7(x10581,f57(x10582,x10583),f55(x10584,a4,x10585))),
% 58.94/58.89 inference(scs_inference,[],[1006,634,995,420,423,1048,257,392,289,345,329,269,310,328])).
% 58.94/58.89 cnf(1059,plain,
% 58.94/58.89 (~P13(x10591,f55(x10592,a4,x10593))),
% 58.94/58.89 inference(rename_variables,[],[423])).
% 58.94/58.89 cnf(1066,plain,
% 58.94/58.89 (~P13(x10661,f59(a4))),
% 58.94/58.89 inference(rename_variables,[],[400])).
% 58.94/58.89 cnf(1070,plain,
% 58.94/58.89 (P13(x10701,f57(x10702,x10701))),
% 58.94/58.89 inference(rename_variables,[],[392])).
% 58.94/58.89 cnf(1076,plain,
% 58.94/58.89 (~P3(f6(x10761,x10762,f57(x10763,x10764),f55(x10765,a4,x10766),f57(x10763,x10764)),x10764,x10764)),
% 58.94/58.89 inference(scs_inference,[],[1006,634,1027,995,420,1056,423,1048,1059,257,400,1066,682,722,411,392,1070,289,345,329,269,310,328,304,309,287,362,384])).
% 58.94/58.89 cnf(1088,plain,
% 58.94/58.89 (~P15(x10881,f53(x10882,a4),f57(x10883,x10884))),
% 58.94/58.89 inference(scs_inference,[],[1058,1047,417,393,289,345,329])).
% 58.94/58.89 cnf(1089,plain,
% 58.94/58.89 (~P13(x10891,f53(x10892,a4))),
% 58.94/58.89 inference(rename_variables,[],[417])).
% 58.94/58.89 cnf(1096,plain,
% 58.94/58.89 (~P13(x10961,f42(x10962,a4))),
% 58.94/58.89 inference(rename_variables,[],[414])).
% 58.94/58.89 cnf(1097,plain,
% 58.94/58.89 (~P13(x10971,f53(x10972,a4))),
% 58.94/58.89 inference(rename_variables,[],[417])).
% 58.94/58.89 cnf(1099,plain,
% 58.94/58.89 (~P7(x10991,f57(x10992,x10993),f53(x10994,a4))),
% 58.94/58.89 inference(scs_inference,[],[1058,520,889,1047,414,417,1089,1097,393,289,345,329,269,310,328])).
% 58.94/58.89 cnf(1100,plain,
% 58.94/58.89 (~P13(x11001,f53(x11002,a4))),
% 58.94/58.89 inference(rename_variables,[],[417])).
% 58.94/58.89 cnf(1103,plain,
% 58.94/58.89 (P13(x11031,f57(x11031,x11032))),
% 58.94/58.89 inference(rename_variables,[],[393])).
% 58.94/58.89 cnf(1105,plain,
% 58.94/58.89 (P14(x11051,x11052,f55(x11053,a4,x11054))),
% 58.94/58.89 inference(scs_inference,[],[1058,520,889,1076,1047,414,417,1089,1097,781,774,393,289,345,329,269,310,328,287,304])).
% 58.94/58.89 cnf(1108,plain,
% 58.94/58.89 (P7(x11081,f53(x11082,a4),f42(x11083,a4))),
% 58.94/58.89 inference(scs_inference,[],[1058,520,889,1076,1047,414,1096,417,1089,1097,1100,781,774,393,289,345,329,269,310,328,287,304,309])).
% 58.94/58.89 cnf(1110,plain,
% 58.94/58.89 (~P13(x11101,f42(x11102,a4))),
% 58.94/58.89 inference(rename_variables,[],[414])).
% 58.94/58.89 cnf(1113,plain,
% 58.94/58.89 (P13(x11131,f57(x11131,x11132))),
% 58.94/58.89 inference(rename_variables,[],[393])).
% 58.94/58.89 cnf(1117,plain,
% 58.94/58.89 (~P3(f6(x11171,x11172,f57(x11173,x11174),f42(x11175,a4),f57(x11173,x11174)),x11173,x11173)),
% 58.94/58.89 inference(scs_inference,[],[1058,520,889,1076,1047,414,1096,1110,417,1089,1097,1100,423,781,774,574,393,1103,1113,289,345,329,269,310,328,287,304,309,212,365,384])).
% 58.94/58.89 cnf(1132,plain,
% 58.94/58.89 (~P15(x11321,f52(x11322,a4,x11323),f49(x11324))),
% 58.94/58.89 inference(scs_inference,[],[1099,1088,420,391,289,345,329])).
% 58.94/58.89 cnf(1133,plain,
% 58.94/58.89 (~P13(x11331,f52(x11332,a4,x11333))),
% 58.94/58.89 inference(rename_variables,[],[420])).
% 58.94/58.89 cnf(1135,plain,
% 58.94/58.89 (~P7(x11351,f49(x11352),f52(x11353,a4,x11354))),
% 58.94/58.89 inference(scs_inference,[],[1099,1088,420,1133,391,289,345,329,328])).
% 58.94/58.89 cnf(1136,plain,
% 58.94/58.89 (~P13(x11361,f52(x11362,a4,x11363))),
% 58.94/58.89 inference(rename_variables,[],[420])).
% 58.94/58.89 cnf(1138,plain,
% 58.94/58.89 (P7(x11381,f53(x11382,a4),f52(x11383,a4,x11384))),
% 58.94/58.89 inference(scs_inference,[],[1099,1088,420,1133,1136,417,391,289,345,329,328,310])).
% 58.94/58.89 cnf(1139,plain,
% 58.94/58.89 (~P13(x11391,f53(x11392,a4))),
% 58.94/58.89 inference(rename_variables,[],[417])).
% 58.94/58.89 cnf(1140,plain,
% 58.94/58.89 (~P13(x11401,f52(x11402,a4,x11403))),
% 58.94/58.89 inference(rename_variables,[],[420])).
% 58.94/58.89 cnf(1151,plain,
% 58.94/58.89 (P13(x11511,f49(x11511))),
% 58.94/58.89 inference(rename_variables,[],[391])).
% 58.94/58.89 cnf(1160,plain,
% 58.94/58.89 (~P3(f6(x11601,x11602,f49(x11603),f52(x11604,a4,x11605),f49(x11603)),x11603,x11603)),
% 58.94/58.89 inference(scs_inference,[],[1099,394,771,1117,1088,420,1133,1136,1140,414,417,1139,880,722,685,391,1151,1108,289,345,329,328,310,269,304,287,365,364,384])).
% 58.94/58.89 cnf(1186,plain,
% 58.94/58.89 (~P13(x11861,f59(a4))),
% 58.94/58.89 inference(rename_variables,[],[400])).
% 58.94/58.89 cnf(1192,plain,
% 58.94/58.89 (P14(x11921,a4,f53(x11922,a4))),
% 58.94/58.89 inference(scs_inference,[],[1135,394,970,1132,400,1186,414,417,978,403,1138,289,345,206,269,309,310,304])).
% 58.94/58.89 cnf(1197,plain,
% 58.94/58.89 (P13(x11971,f57(x11971,x11972))),
% 58.94/58.89 inference(rename_variables,[],[393])).
% 58.94/58.89 cnf(1199,plain,
% 58.94/58.89 (~P3(f6(x11991,x11992,f57(x11993,x11994),f52(x11995,a4,x11996),f57(x11993,x11994)),x11993,x11993)),
% 58.94/58.89 inference(scs_inference,[],[1135,394,970,1160,1132,400,1186,420,414,417,978,403,393,1197,1138,289,345,206,269,309,310,304,287,384])).
% 58.94/58.89 cnf(1220,plain,
% 58.94/58.89 (~P13(x12201,f59(a4))),
% 58.94/58.89 inference(rename_variables,[],[400])).
% 58.94/58.89 cnf(1221,plain,
% 58.94/58.89 (~P13(x12211,f55(x12212,a4,x12213))),
% 58.94/58.89 inference(rename_variables,[],[423])).
% 58.94/58.89 cnf(1225,plain,
% 58.94/58.89 (~P13(x12251,f55(x12252,a4,x12253))),
% 58.94/58.89 inference(rename_variables,[],[423])).
% 58.94/58.89 cnf(1227,plain,
% 58.94/58.89 (P14(x12271,x12272,f59(a4))),
% 58.94/58.89 inference(scs_inference,[],[771,634,423,1221,400,414,691,652,269,310,309,304])).
% 58.94/58.89 cnf(1231,plain,
% 58.94/58.89 (P13(x12311,f57(x12312,x12311))),
% 58.94/58.89 inference(rename_variables,[],[392])).
% 58.94/58.89 cnf(1233,plain,
% 58.94/58.89 (P13(x12331,f57(x12332,x12331))),
% 58.94/58.89 inference(rename_variables,[],[392])).
% 58.94/58.89 cnf(1235,plain,
% 58.94/58.89 (~P3(f6(x12351,x12352,f57(x12353,x12354),f59(a4),f57(x12353,x12354)),x12354,x12354)),
% 58.94/58.89 inference(scs_inference,[],[771,634,1199,423,1221,1225,400,1220,414,691,652,392,1231,1233,269,310,309,304,212,287,384])).
% 58.94/58.89 cnf(1249,plain,
% 58.94/58.89 (~P13(x12491,f55(x12492,a4,x12493))),
% 58.94/58.89 inference(rename_variables,[],[423])).
% 58.94/58.89 cnf(1252,plain,
% 58.94/58.89 (~P13(x12521,f55(x12522,a4,x12523))),
% 58.94/58.89 inference(rename_variables,[],[423])).
% 58.94/58.89 cnf(1263,plain,
% 58.94/58.89 (P13(x12631,f49(x12631))),
% 58.94/58.89 inference(rename_variables,[],[391])).
% 58.94/58.89 cnf(1265,plain,
% 58.94/58.89 (~P3(f6(x12651,x12652,f49(x12653),f55(x12654,a4,x12655),f49(x12653)),x12653,x12653)),
% 58.94/58.89 inference(scs_inference,[],[520,771,1235,423,1249,1252,978,553,391,1263,329,328,269,304,287,384])).
% 58.94/58.89 cnf(1273,plain,
% 58.94/58.89 (~P13(x12731,f52(x12732,a4,x12733))),
% 58.94/58.89 inference(rename_variables,[],[420])).
% 58.94/58.89 cnf(1279,plain,
% 58.94/58.89 (~P12(x12791,f55(x12792,a4,x12793),x12794,f49(x12795),x12796)+P13(f45(x12797,f52(x12798,a4,x12799),f52(x127910,a4,x127911)),f52(x12798,a4,x12799))),
% 58.94/58.89 inference(scs_inference,[],[520,771,1235,420,1273,423,1249,1252,978,722,553,391,1263,329,328,269,304,287,384,345,289,308,364,346])).
% 58.94/58.89 cnf(1295,plain,
% 58.94/58.89 (P13(x12951,f57(x12952,x12951))),
% 58.94/58.89 inference(rename_variables,[],[392])).
% 58.94/58.89 cnf(1297,plain,
% 58.94/58.89 (~P3(f6(x12971,x12972,f57(x12973,x12974),a4,f57(x12973,x12974)),x12974,x12974)),
% 58.94/58.89 inference(scs_inference,[],[394,889,1265,257,420,978,392,1295,559,1279,269,304,287,384])).
% 58.94/58.89 cnf(1313,plain,
% 58.94/58.89 (~P13(x13131,f59(a4))),
% 58.94/58.89 inference(rename_variables,[],[400])).
% 58.94/58.89 cnf(1314,plain,
% 58.94/58.89 (~P13(x13141,f53(x13142,a4))),
% 58.94/58.89 inference(rename_variables,[],[417])).
% 58.94/58.89 cnf(1325,plain,
% 58.94/58.89 (P13(x13251,f57(x13251,x13252))),
% 58.94/58.89 inference(rename_variables,[],[393])).
% 58.94/58.89 cnf(1327,plain,
% 58.94/58.89 (~P3(f6(x13271,x13272,f57(x13273,x13274),f53(x13275,a4),f57(x13273,x13274)),x13273,x13273)),
% 58.94/58.89 inference(scs_inference,[],[634,520,1297,400,417,1314,880,393,1325,682,310,269,304,287,384])).
% 58.94/58.89 cnf(1334,plain,
% 58.94/58.89 (P7(x13341,f59(a4),x13342)+P13(f45(x13341,f59(a4),x13342),f59(a4))),
% 58.94/58.89 inference(scs_inference,[],[254,634,520,1297,400,1313,417,1314,880,393,1325,787,798,682,909,310,269,304,287,384,237,220,204,251,308])).
% 58.94/58.89 cnf(1345,plain,
% 58.94/58.89 (~P13(x13451,f55(x13452,a4,x13453))),
% 58.94/58.89 inference(rename_variables,[],[423])).
% 58.94/58.89 cnf(1346,plain,
% 58.94/58.89 (~P13(x13461,f42(x13462,a4))),
% 58.94/58.89 inference(rename_variables,[],[414])).
% 58.94/58.89 cnf(1350,plain,
% 58.94/58.89 (~P13(x13501,f55(x13502,a4,x13503))),
% 58.94/58.89 inference(rename_variables,[],[423])).
% 58.94/58.89 cnf(1359,plain,
% 58.94/58.89 (P13(x13591,f57(x13592,x13591))),
% 58.94/58.89 inference(rename_variables,[],[392])).
% 58.94/58.89 cnf(1361,plain,
% 58.94/58.89 (~P3(f6(x13611,x13612,f57(x13613,x13614),f53(x13615,a4),f57(x13613,x13614)),x13614,x13614)),
% 58.94/58.89 inference(scs_inference,[],[1327,423,1345,1350,414,400,257,417,978,392,1359,391,685,1334,310,309,212,304,287,384])).
% 58.94/58.89 cnf(1367,plain,
% 58.94/58.89 (P1(a1,x13671)+~E(a2,x13671)),
% 58.94/58.89 inference(scs_inference,[],[253,1327,423,1345,1350,414,1346,400,257,417,978,392,1359,391,685,1334,310,309,212,304,287,384,308,202])).
% 58.94/58.89 cnf(1398,plain,
% 58.94/58.89 (~P13(a1,f49(a4))),
% 58.94/58.89 inference(scs_inference,[],[597,2,259])).
% 58.94/58.89 cnf(1399,plain,
% 58.94/58.89 (~E(a1,a4)),
% 58.94/58.89 inference(scs_inference,[],[1398,258])).
% 58.94/58.89 cnf(1401,plain,
% 58.94/58.89 (~P15(x14011,f42(x14012,a4),f49(x14013))),
% 58.94/58.89 inference(scs_inference,[],[414,391,1398,258,329])).
% 58.94/58.89 cnf(1402,plain,
% 58.94/58.89 (~P13(x14021,f42(x14022,a4))),
% 58.94/58.89 inference(rename_variables,[],[414])).
% 58.94/58.89 cnf(1404,plain,
% 58.94/58.89 (~P7(x14041,f49(x14042),f42(x14043,a4))),
% 58.94/58.89 inference(scs_inference,[],[414,1402,391,1398,258,329,328])).
% 58.94/58.89 cnf(1405,plain,
% 58.94/58.89 (~P13(x14051,f42(x14052,a4))),
% 58.94/58.89 inference(rename_variables,[],[414])).
% 58.94/58.89 cnf(1409,plain,
% 58.94/58.89 (~P13(x14091,f42(x14092,a4))),
% 58.94/58.89 inference(rename_variables,[],[414])).
% 58.94/58.89 cnf(1412,plain,
% 58.94/58.89 (P13(x14121,f49(x14121))),
% 58.94/58.89 inference(rename_variables,[],[391])).
% 58.94/58.89 cnf(1417,plain,
% 58.94/58.89 (~P8(f6(x14171,x14172,f57(x14173,x14174),f52(x14175,a4,x14176),f57(x14173,x14174)),f49(x14174))),
% 58.94/58.89 inference(scs_inference,[],[602,414,1402,1405,1409,257,880,403,391,1412,1398,258,329,328,309,212,304,287])).
% 58.94/58.89 cnf(1418,plain,
% 58.94/58.89 (P13(x14181,f49(x14181))),
% 58.94/58.89 inference(rename_variables,[],[391])).
% 58.94/58.89 cnf(1420,plain,
% 58.94/58.89 (~P3(f6(x14201,x14202,f49(x14203),f42(x14204,a4),f49(x14203)),x14203,x14203)),
% 58.94/58.89 inference(scs_inference,[],[602,414,1402,1405,1409,257,880,403,391,1412,1418,1398,258,329,328,309,212,304,287,384])).
% 58.94/58.89 cnf(1439,plain,
% 58.94/58.89 (P14(x14391,x14392,a4)),
% 58.94/58.89 inference(scs_inference,[],[1404,1401,411,408,345,289,304])).
% 58.94/58.89 cnf(1552,plain,
% 58.94/58.89 (P7(x15521,a4,x15522)+P13(f45(x15521,a4,x15522),a4)),
% 58.94/58.89 inference(scs_inference,[],[1361,257,391,961,287,238,308])).
% 58.94/58.89 cnf(1564,plain,
% 58.94/58.89 (P7(x15641,a4,x15642)),
% 58.94/58.89 inference(scs_inference,[],[257,1552])).
% 58.94/58.89 cnf(1569,plain,
% 58.94/58.89 (P12(x15691,a4,x15692,f53(x15693,a4),x15694)),
% 58.94/58.89 inference(scs_inference,[],[1420,257,417,1192,393,1552,287,365])).
% 58.94/58.89 cnf(1594,plain,
% 58.94/58.89 (P13(a4,f50(f42(a3,a1)))),
% 58.94/58.89 inference(scs_inference,[],[254,260,262])).
% 58.94/58.89 cnf(1820,plain,
% 58.94/58.89 (P13(f42(a3,a1),f50(a4))),
% 58.94/58.89 inference(scs_inference,[],[254,261,262])).
% 58.94/58.89 cnf(1821,plain,
% 58.94/58.89 (P1(f42(a3,a1),a4)),
% 58.94/58.89 inference(scs_inference,[],[1820,265])).
% 58.94/58.89 cnf(1823,plain,
% 58.94/58.89 (~P13(x18231,f42(a3,a1))),
% 58.94/58.89 inference(scs_inference,[],[1820,257,265,268])).
% 58.94/58.89 cnf(1847,plain,
% 58.94/58.89 (~P13(x18471,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1850,plain,
% 58.94/58.89 (~P13(x18501,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1853,plain,
% 58.94/58.89 (~P13(x18531,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1856,plain,
% 58.94/58.89 (~P13(x18561,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1859,plain,
% 58.94/58.89 (~P13(x18591,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1862,plain,
% 58.94/58.89 (~P13(x18621,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1865,plain,
% 58.94/58.89 (~P13(x18651,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1868,plain,
% 58.94/58.89 (~P13(x18681,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1871,plain,
% 58.94/58.89 (~P13(x18711,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1873,plain,
% 58.94/58.89 (P1(f42(a3,a1),x18731)),
% 58.94/58.89 inference(scs_inference,[],[1823,1847,1850,1853,1856,1859,1862,1865,1868,1871,359,354,360,357,338,267,293,277,341,266])).
% 58.94/58.89 cnf(1874,plain,
% 58.94/58.89 (~P13(x18741,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1877,plain,
% 58.94/58.89 (~P13(x18771,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1879,plain,
% 58.94/58.89 (P15(x18791,x18792,f42(a3,a1))),
% 58.94/58.89 inference(scs_inference,[],[1823,1847,1850,1853,1856,1859,1862,1865,1868,1871,1874,1877,359,354,360,357,338,267,293,277,341,266,298,295])).
% 58.94/58.89 cnf(1880,plain,
% 58.94/58.89 (~P13(x18801,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1883,plain,
% 58.94/58.89 (~P13(x18831,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1885,plain,
% 58.94/58.89 (P9(x18851,x18852,f42(a3,a1))),
% 58.94/58.89 inference(scs_inference,[],[1823,1847,1850,1853,1856,1859,1862,1865,1868,1871,1874,1877,1880,1883,359,354,360,357,338,267,293,277,341,266,298,295,380,294])).
% 58.94/58.89 cnf(1886,plain,
% 58.94/58.89 (~P13(x18861,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1889,plain,
% 58.94/58.89 (~P13(x18891,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1892,plain,
% 58.94/58.89 (~P13(x18921,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1895,plain,
% 58.94/58.89 (~P13(x18951,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1898,plain,
% 58.94/58.89 (~P13(x18981,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1901,plain,
% 58.94/58.89 (~P13(x19011,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1904,plain,
% 58.94/58.89 (~P13(x19041,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1913,plain,
% 58.94/58.89 (~P13(x19131,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1916,plain,
% 58.94/58.89 (~P13(x19161,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1917,plain,
% 58.94/58.89 (~P13(x19171,f42(x19172,a4))),
% 58.94/58.89 inference(rename_variables,[],[414])).
% 58.94/58.89 cnf(1920,plain,
% 58.94/58.89 (~P13(x19201,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1922,plain,
% 58.94/58.89 (P7(x19221,f42(x19222,a4),f42(a3,a1))),
% 58.94/58.89 inference(scs_inference,[],[1594,1823,1847,1850,1853,1856,1859,1862,1865,1868,1871,1874,1877,1880,1883,1886,1889,1892,1895,1898,1901,1904,1913,1916,1920,1821,394,1417,414,1917,359,354,360,357,338,267,293,277,341,266,298,295,380,294,340,333,334,337,297,379,292,248,269,329,309,328,310])).
% 58.94/58.89 cnf(1924,plain,
% 58.94/58.89 (~P13(x19241,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1930,plain,
% 58.94/58.89 (~P13(x19301,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1934,plain,
% 58.94/58.89 (P12(x19341,a4,x19342,f42(a3,a1),x19343)),
% 58.94/58.89 inference(scs_inference,[],[1594,1823,1847,1850,1853,1856,1859,1862,1865,1868,1871,1874,1877,1880,1883,1886,1889,1892,1895,1898,1901,1904,1913,1916,1920,1924,1930,1821,394,1417,836,414,1917,391,1564,403,359,354,360,357,338,267,293,277,341,266,298,295,380,294,340,333,334,337,297,379,292,248,269,329,309,328,310,304,212,287,365])).
% 58.94/58.89 cnf(1935,plain,
% 58.94/58.89 (~P13(x19351,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1951,plain,
% 58.94/58.89 (P7(x19511,f42(a3,a1),x19512)+P13(f45(x19511,f42(a3,a1),x19512),f42(a3,a1))),
% 58.94/58.89 inference(scs_inference,[],[1594,1823,1847,1850,1853,1856,1859,1862,1865,1868,1871,1874,1877,1880,1883,1886,1889,1892,1895,1898,1901,1904,1913,1916,1920,1924,1930,1935,1821,394,1417,836,414,1917,391,1564,403,359,354,360,357,338,267,293,277,341,266,298,295,380,294,340,333,334,337,297,379,292,248,269,329,309,328,310,304,212,287,365,361,339,356,355,289,345,214,308])).
% 58.94/58.89 cnf(1952,plain,
% 58.94/58.89 (~P13(x19521,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1955,plain,
% 58.94/58.89 (P12(x19551,f42(a3,a1),x19552,f52(x19553,a4,x19554),x19555)+P13(f45(x19551,f42(a3,a1),f52(x19553,a4,x19554)),f42(a3,a1))),
% 58.94/58.89 inference(scs_inference,[],[1594,1823,1847,1850,1853,1856,1859,1862,1865,1868,1871,1874,1877,1880,1883,1886,1889,1892,1895,1898,1901,1904,1913,1916,1920,1924,1930,1935,1952,1821,394,1417,836,414,1917,722,391,1564,403,359,354,360,357,338,267,293,277,341,266,298,295,380,294,340,333,334,337,297,379,292,248,269,329,309,328,310,304,212,287,365,361,339,356,355,289,345,214,308,206,364])).
% 58.94/58.89 cnf(1959,plain,
% 58.94/58.89 (~P12(x19591,f42(a3,a1),x19592,f50(f42(a3,a1)),x19593)+P13(f45(x19594,f42(a3,a1),f52(x19595,a4,x19596)),f42(a3,a1))),
% 58.94/58.89 inference(scs_inference,[],[1594,1823,1847,1850,1853,1856,1859,1862,1865,1868,1871,1874,1877,1880,1883,1886,1889,1892,1895,1898,1901,1904,1913,1916,1920,1924,1930,1935,1952,1821,394,1417,836,414,1917,722,391,1564,403,359,354,360,357,338,267,293,277,341,266,298,295,380,294,340,333,334,337,297,379,292,248,269,329,309,328,310,304,212,287,365,361,339,356,355,289,345,214,308,206,364,346])).
% 58.94/58.89 cnf(1961,plain,
% 58.94/58.89 (~E(f52(x19611,a4,x19612),f50(f42(a3,a1)))+P13(f45(x19613,f42(a3,a1),f52(x19611,a4,x19612)),f42(a3,a1))),
% 58.94/58.89 inference(scs_inference,[],[1594,1823,1847,1850,1853,1856,1859,1862,1865,1868,1871,1874,1877,1880,1883,1886,1889,1892,1895,1898,1901,1904,1913,1916,1920,1924,1930,1935,1952,1821,394,1417,836,414,1917,722,391,1564,403,359,354,360,357,338,267,293,277,341,266,298,295,380,294,340,333,334,337,297,379,292,248,269,329,309,328,310,304,212,287,365,361,339,356,355,289,345,214,308,206,364,346,216])).
% 58.94/58.89 cnf(1966,plain,
% 58.94/58.89 (~P13(x19661,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1967,plain,
% 58.94/58.89 (P7(x19671,f42(a3,a1),x19672)),
% 58.94/58.89 inference(scs_inference,[],[1823,1966,1955,1951])).
% 58.94/58.89 cnf(1968,plain,
% 58.94/58.89 (~P13(x19681,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1970,plain,
% 58.94/58.89 (~P13(x19701,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1972,plain,
% 58.94/58.89 (~P13(x19721,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1975,plain,
% 58.94/58.89 (~P13(x19751,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1977,plain,
% 58.94/58.89 (P7(x19771,f55(x19772,a4,x19773),f42(a3,a1))),
% 58.94/58.89 inference(scs_inference,[],[1823,1966,1968,1970,1972,1975,417,423,1955,1951,1959,1961,309,310])).
% 58.94/58.89 cnf(1979,plain,
% 58.94/58.89 (~P13(x19791,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(1981,plain,
% 58.94/58.89 (P14(x19811,f52(x19812,a4,x19813),f42(a3,a1))),
% 58.94/58.89 inference(scs_inference,[],[1823,1966,1968,1970,1972,1975,417,423,553,1879,1955,1951,1959,1961,309,310,304])).
% 58.94/58.89 cnf(1985,plain,
% 58.94/58.89 (~E(f50(a4),f42(a3,a1))),
% 58.94/58.89 inference(scs_inference,[],[1823,1966,1968,1970,1972,1975,1979,1820,417,423,553,1879,1955,1951,1959,1961,309,310,304,212])).
% 58.94/58.89 cnf(1998,plain,
% 58.94/58.89 (P7(x19981,f52(x19982,a4,x19983),f42(a3,a1))),
% 58.94/58.89 inference(scs_inference,[],[1823,420,309])).
% 58.94/58.89 cnf(3974,plain,
% 58.94/58.89 (~P13(x39741,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(3976,plain,
% 58.94/58.89 (~P7(x39761,f50(a4),f42(a3,a1))),
% 58.94/58.89 inference(scs_inference,[],[1823,3974,1820,329,328])).
% 58.94/58.89 cnf(3986,plain,
% 58.94/58.89 (~E(a4,f50(a4))),
% 58.94/58.89 inference(scs_inference,[],[1823,3974,1934,1820,1922,397,329,328,345,289,248,206,214])).
% 58.94/58.89 cnf(3997,plain,
% 58.94/58.89 (~P13(x39971,a4)),
% 58.94/58.89 inference(rename_variables,[],[257])).
% 58.94/58.89 cnf(4002,plain,
% 58.94/58.89 (~P12(x40021,f50(a4),x40022,a4,x40023)),
% 58.94/58.89 inference(scs_inference,[],[1820,3976,257,3997,1977,206,329,328,345])).
% 58.94/58.89 cnf(4007,plain,
% 58.94/58.89 (~P12(x40071,a4,x40072,f50(a4),x40073)),
% 58.94/58.89 inference(scs_inference,[],[1820,3976,257,3997,1977,544,206,329,328,345,289,248,346])).
% 58.94/58.89 cnf(4027,plain,
% 58.94/58.89 (~P13(x40271,a4)),
% 58.94/58.89 inference(rename_variables,[],[257])).
% 58.94/58.89 cnf(4030,plain,
% 58.94/58.89 (~P13(x40301,f55(x40302,a4,x40303))),
% 58.94/58.89 inference(rename_variables,[],[423])).
% 58.94/58.89 cnf(4041,plain,
% 58.94/58.89 (~P13(x40411,f55(x40412,a4,x40413))),
% 58.94/58.89 inference(rename_variables,[],[423])).
% 58.94/58.89 cnf(4051,plain,
% 58.94/58.89 (P7(x40511,f42(a3,a1),x40512)),
% 58.94/58.89 inference(rename_variables,[],[1967])).
% 58.94/58.89 cnf(4056,plain,
% 58.94/58.89 (P7(x40561,f42(a3,a1),x40562)),
% 58.94/58.89 inference(rename_variables,[],[1967])).
% 58.94/58.89 cnf(4062,plain,
% 58.94/58.89 (~P13(x40621,f42(a3,a1))),
% 58.94/58.89 inference(rename_variables,[],[1823])).
% 58.94/58.89 cnf(4069,plain,
% 58.94/58.89 (~E(a2,a4)),
% 58.94/58.89 inference(scs_inference,[],[253,1399,1985,4002,4007,475,1967,4051,4056,1439,1227,1105,1569,1023,1398,1998,1981,394,1820,256,423,4030,4041,420,257,4027,1823,400,391,2,259,262,279,280,281,299,300,270,268,274,214,212,216,329,328,269,363,365,362,364,1367])).
% 58.94/58.89 cnf(4078,plain,
% 58.94/58.89 (~P3(a3,f7(a1,a4),x40781)),
% 58.94/58.89 inference(scs_inference,[],[253,1399,1985,4002,4007,475,1967,4051,4056,1439,1227,1105,1569,1023,1398,1998,1981,394,1820,256,423,4030,4041,420,257,4027,1823,4062,400,391,2,259,262,279,280,281,299,300,270,268,274,214,212,216,329,328,269,363,365,362,364,1367,265,266,284,315,290])).
% 58.94/58.89 cnf(4085,plain,
% 58.94/58.89 (P13(f7(a1,a4),a2)),
% 58.94/58.89 inference(scs_inference,[],[253,1399,1985,4002,4007,475,1967,4051,4056,1439,1227,1105,1569,1023,1398,1998,1981,1879,1885,394,1820,256,423,4030,4041,420,257,4027,1823,4062,400,391,2,259,262,279,280,281,299,300,270,268,274,214,212,216,329,328,269,363,365,362,364,1367,265,266,284,315,290,304,317,481])).
% 58.94/58.89 cnf(4096,plain,
% 58.94/58.89 (~P3(a3,f7(a1,a4),x40961)),
% 58.94/58.89 inference(rename_variables,[],[4078])).
% 58.94/58.89 cnf(4109,plain,
% 58.94/58.89 (~E(a4,a2)),
% 58.94/58.89 inference(scs_inference,[],[4069,4078,4096,4085,1873,301,335,271,262,272,285,2])).
% 58.94/58.89 cnf(4173,plain,
% 58.94/58.89 ($false),
% 58.94/58.89 inference(scs_inference,[],[4109,3986,4078,970,4085,255,262,259,2,331]),
% 58.94/58.89 ['proof']).
% 58.94/58.89 % SZS output end Proof
% 58.94/58.89 % Total time :58.160000s
%------------------------------------------------------------------------------