%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET762+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 : n022.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 14:22:23 EDT 2024
% Result : Theorem 1.49s 1.59s
% Output : CNFRefutation 1.49s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.15 % Problem : SET762+4 : TPTP v8.2.0. Bugfixed v2.2.1.
% 0.09/0.15 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.16/0.37 % Computer : n022.cluster.edu
% 0.16/0.37 % Model : x86_64 x86_64
% 0.16/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.37 % Memory : 8042.1875MB
% 0.16/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.37 % CPULimit : 300
% 0.16/0.37 % WCLimit : 300
% 0.16/0.37 % DateTime : Sun Jun 23 13:26:54 EDT 2024
% 0.16/0.37 % CPUTime :
% 0.59/0.61 start to proof:theBenchmark
% 1.49/1.58 %-------------------------------------------
% 1.49/1.58 % File :CSE---1.7
% 1.49/1.58 % Problem :theBenchmark
% 1.49/1.58 % Transform :cnf
% 1.49/1.58 % Format :tptp:raw
% 1.49/1.58 % Command :java -jar mcs_scs.jar %d %s
% 1.49/1.58
% 1.49/1.58 % Result :Theorem 0.850000s
% 1.49/1.58 % Output :CNFRefutation 0.850000s
% 1.49/1.58 %-------------------------------------------
% 1.49/1.59 %--------------------------------------------------------------------------
% 1.49/1.59 % File : SET762+4 : TPTP v8.2.0. Bugfixed v2.2.1.
% 1.49/1.59 % Domain : Set Theory (Mappings)
% 1.49/1.59 % Problem : The image of empty set is empty
% 1.49/1.59 % Version : [Pas99] axioms.
% 1.49/1.59 % English :
% 1.49/1.59
% 1.49/1.59 % Refs : [Pas99] Pastre (1999), Email to G. Sutcliffe
% 1.49/1.59 % Source : [Pas99]
% 1.49/1.59 % Names :
% 1.49/1.59
% 1.49/1.59 % Status : Theorem
% 1.49/1.59 % Rating : 0.17 v8.2.0, 0.19 v8.1.0, 0.17 v7.5.0, 0.16 v7.4.0, 0.17 v7.2.0, 0.14 v7.1.0, 0.13 v7.0.0, 0.17 v6.4.0, 0.23 v6.3.0, 0.21 v6.2.0, 0.16 v6.1.0, 0.27 v6.0.0, 0.30 v5.5.0, 0.41 v5.4.0, 0.43 v5.3.0, 0.44 v5.2.0, 0.35 v5.1.0, 0.38 v5.0.0, 0.42 v4.1.0, 0.39 v4.0.0, 0.42 v3.7.0, 0.45 v3.5.0, 0.42 v3.4.0, 0.47 v3.3.0, 0.43 v3.2.0, 0.45 v3.1.0, 0.56 v2.7.0, 0.33 v2.6.0, 0.43 v2.5.0, 0.50 v2.4.0, 0.50 v2.3.0, 0.33 v2.2.1
% 1.49/1.59 % Syntax : Number of formulae : 29 ( 1 unt; 0 def)
% 1.49/1.59 % Number of atoms : 130 ( 6 equ)
% 1.49/1.59 % Maximal formula atoms : 11 ( 4 avg)
% 1.49/1.59 % Number of connectives : 103 ( 2 ~; 2 |; 50 &)
% 1.49/1.59 % ( 30 <=>; 19 =>; 0 <=; 0 <~>)
% 1.49/1.59 % Maximal formula depth : 19 ( 9 avg)
% 1.49/1.59 % Maximal term depth : 2 ( 1 avg)
% 1.49/1.59 % Number of predicates : 16 ( 15 usr; 0 prp; 2-6 aty)
% 1.49/1.59 % Number of functors : 15 ( 15 usr; 1 con; 0-5 aty)
% 1.49/1.59 % Number of variables : 136 ( 127 !; 9 ?)
% 1.49/1.59 % SPC : FOF_THM_RFO_SEQ
% 1.49/1.59
% 1.49/1.59 % Comments :
% 1.49/1.59 % Bugfixes : v2.2.1 - Bugfixes in SET006+1.ax.
% 1.49/1.59 %--------------------------------------------------------------------------
% 1.49/1.59 %----Include set theory definitions
% 1.49/1.59 include('Axioms/SET006+0.ax').
% 1.49/1.59 %----Include mappings axioms
% 1.49/1.59 include('Axioms/SET006+1.ax').
% 1.49/1.59 %--------------------------------------------------------------------------
% 1.49/1.59 fof(thIIa12,conjecture,
% 1.49/1.59 ! [F,A,B] :
% 1.49/1.59 ( maps(F,A,B)
% 1.49/1.59 => equal_set(image2(F,empty_set),empty_set) ) ).
% 1.49/1.59
% 1.49/1.59 %--------------------------------------------------------------------------
% 1.49/1.59 %-------------------------------------------
% 1.49/1.59 % Proof found
% 1.49/1.59 % SZS status Theorem for theBenchmark
% 1.49/1.59 % SZS output start Proof
% 1.49/1.59 %ClaNum:388(EqnAxiom:252)
% 1.49/1.59 %VarNum:1641(SingletonVarNum:571)
% 1.49/1.59 %MaxLitNum:9
% 1.49/1.59 %MaxfuncDepth:1
% 1.49/1.59 %SharedTerms:7
% 1.49/1.59 %goalClause: 253 255
% 1.49/1.59 %singleGoalClaCount:2
% 1.49/1.59 [253]P1(a1,a39,a40)
% 1.49/1.59 [255]~P2(f41(a1,a2),a2)
% 1.49/1.59 [254]~P12(x2541,a2)
% 1.49/1.59 [258]~P2(x2582,x2581)+P13(x2581,x2582)
% 1.49/1.59 [259]~P2(x2591,x2592)+P13(x2591,x2592)
% 1.49/1.59 [256]~E(x2561,x2562)+P12(x2561,f48(x2562))
% 1.49/1.59 [257]E(x2571,x2572)+~P12(x2571,f48(x2572))
% 1.49/1.59 [260]~P13(x2601,x2602)+P12(x2601,f49(x2602))
% 1.49/1.59 [263]P13(x2631,x2632)+~P12(x2631,f49(x2632))
% 1.49/1.59 [264]P13(x2641,x2642)+P12(f5(x2641,x2642),x2641)
% 1.49/1.59 [265]P7(x2651,x2652)+P12(f6(x2651,x2652),x2652)
% 1.49/1.59 [268]P12(f16(x2681,x2682),x2682)+P12(x2681,f55(x2682))
% 1.49/1.59 [274]~P12(x2741,f58(x2742))+P12(x2741,f17(x2741,x2742))
% 1.49/1.59 [275]~P12(x2751,f58(x2752))+P12(f17(x2751,x2752),x2752)
% 1.49/1.59 [280]P13(x2801,x2802)+~P12(f5(x2801,x2802),x2802)
% 1.49/1.59 [281]~P12(x2811,f16(x2811,x2812))+P12(x2811,f55(x2812))
% 1.49/1.59 [294]P7(x2941,x2942)+~P3(x2941,f6(x2941,x2942),f6(x2941,x2942))
% 1.49/1.59 [286]~P14(x2861,x2862,x2863)+P8(x2861,x2862,x2863)
% 1.49/1.59 [287]~P14(x2871,x2872,x2873)+P15(x2871,x2872,x2873)
% 1.49/1.59 [261]~E(x2611,x2613)+P12(x2611,f56(x2612,x2613))
% 1.49/1.59 [262]~E(x2621,x2622)+P12(x2621,f56(x2622,x2623))
% 1.49/1.59 [269]~P12(x2691,x2693)+P12(x2691,f57(x2692,x2693))
% 1.49/1.59 [270]~P12(x2701,x2702)+P12(x2701,f57(x2702,x2703))
% 1.49/1.59 [277]P12(x2771,x2772)+~P12(x2771,f50(x2773,x2772))
% 1.49/1.59 [278]P12(x2781,x2782)+~P12(x2781,f50(x2782,x2783))
% 1.49/1.59 [279]P12(x2791,x2792)+~P12(x2791,f3(x2792,x2793))
% 1.49/1.59 [283]~P12(x2831,x2832)+~P12(x2831,f3(x2833,x2832))
% 1.49/1.59 [290]P8(x2901,x2902,x2903)+P12(f14(x2901,x2902,x2903),x2902)
% 1.49/1.59 [291]P8(x2911,x2912,x2913)+P12(f15(x2911,x2912,x2913),x2912)
% 1.49/1.59 [292]P8(x2921,x2922,x2923)+P12(f18(x2921,x2922,x2923),x2923)
% 1.49/1.59 [293]P15(x2931,x2932,x2933)+P12(f19(x2931,x2932,x2933),x2933)
% 1.49/1.59 [295]~P12(x2953,f41(x2951,x2952))+P12(f21(x2951,x2952,x2953),x2952)
% 1.49/1.59 [296]~P12(x2963,f52(x2961,x2962))+P12(f24(x2961,x2962,x2963),x2962)
% 1.49/1.59 [299]P3(x2991,x2992,f24(x2991,x2993,x2992))+~P12(x2992,f52(x2991,x2993))
% 1.49/1.59 [300]P3(x3001,f21(x3001,x3002,x3003),x3003)+~P12(x3003,f41(x3001,x3002))
% 1.49/1.59 [301]P8(x3011,x3012,x3013)+~E(f15(x3011,x3012,x3013),f14(x3011,x3012,x3013))
% 1.49/1.59 [309]P8(x3091,x3092,x3093)+P3(x3091,f14(x3091,x3092,x3093),f18(x3091,x3092,x3093))
% 1.49/1.59 [310]P8(x3101,x3102,x3103)+P3(x3101,f15(x3101,x3102,x3103),f18(x3101,x3102,x3103))
% 1.49/1.59 [297]P12(x2971,x2972)+~P12(x2971,f51(x2973,x2974,x2972))
% 1.49/1.59 [298]P12(x2981,x2982)+~P12(x2981,f54(x2983,x2984,x2982))
% 1.49/1.59 [331]~P12(x3314,f51(x3311,x3312,x3313))+P12(f25(x3311,x3312,x3313,x3314),x3312)
% 1.49/1.59 [332]~P12(x3324,f54(x3321,x3322,x3323))+P12(f26(x3321,x3322,x3323,x3324),x3322)
% 1.49/1.59 [333]P3(x3331,x3332,f26(x3331,x3333,x3334,x3332))+~P12(x3332,f54(x3331,x3333,x3334))
% 1.49/1.59 [334]P3(x3341,f25(x3341,x3342,x3343,x3344),x3344)+~P12(x3344,f51(x3341,x3342,x3343))
% 1.49/1.59 [335]P4(x3351,x3352,x3353,x3354)+P12(f7(x3351,x3352,x3353,x3354),x3353)
% 1.49/1.59 [336]P4(x3361,x3362,x3363,x3364)+P12(f12(x3361,x3362,x3363,x3364),x3364)
% 1.49/1.59 [337]P4(x3371,x3372,x3373,x3374)+P12(f13(x3371,x3372,x3373,x3374),x3374)
% 1.49/1.59 [338]P10(x3381,x3382,x3383,x3384)+P12(f22(x3381,x3382,x3383,x3384),x3383)
% 1.49/1.59 [339]P10(x3391,x3392,x3393,x3394)+P12(f23(x3391,x3392,x3393,x3394),x3394)
% 1.49/1.59 [340]P4(x3401,x3402,x3403,x3404)+~E(f13(x3401,x3402,x3403,x3404),f12(x3401,x3402,x3403,x3404))
% 1.49/1.59 [341]P4(x3411,x3412,x3413,x3414)+P3(x3412,f7(x3411,x3412,x3413,x3414),f13(x3411,x3412,x3413,x3414))
% 1.49/1.59 [342]P4(x3421,x3422,x3423,x3424)+P3(x3421,f7(x3421,x3422,x3423,x3424),f12(x3421,x3422,x3423,x3424))
% 1.49/1.59 [343]P1(x3431,x3432,x3433)+~P11(x3431,x3432,x3434,x3433,x3435)
% 1.49/1.59 [344]P14(x3441,x3442,x3443)+~P11(x3441,x3442,x3444,x3443,x3445)
% 1.49/1.59 [352]P9(x3521,x3522,x3523,x3524,x3525)+P12(f27(x3521,x3522,x3523,x3524,x3525),x3522)
% 1.49/1.59 [353]P9(x3531,x3532,x3533,x3534,x3535)+P12(f28(x3531,x3532,x3533,x3534,x3535),x3534)
% 1.49/1.59 [354]P9(x3541,x3542,x3543,x3544,x3545)+P12(f29(x3541,x3542,x3543,x3544,x3545),x3542)
% 1.49/1.59 [355]P9(x3551,x3552,x3553,x3554,x3555)+P12(f30(x3551,x3552,x3553,x3554,x3555),x3554)
% 1.49/1.60 [356]P5(x3561,x3562,x3563,x3564,x3565)+P12(f31(x3561,x3562,x3563,x3564,x3565),x3562)
% 1.49/1.60 [357]P5(x3571,x3572,x3573,x3574,x3575)+P12(f32(x3571,x3572,x3573,x3574,x3575),x3574)
% 1.49/1.60 [358]P5(x3581,x3582,x3583,x3584,x3585)+P12(f33(x3581,x3582,x3583,x3584,x3585),x3582)
% 1.49/1.60 [359]P5(x3591,x3592,x3593,x3594,x3595)+P12(f34(x3591,x3592,x3593,x3594,x3595),x3594)
% 1.49/1.60 [364]P9(x3641,x3642,x3643,x3644,x3645)+P3(x3643,f27(x3641,x3642,x3643,x3644,x3645),f29(x3641,x3642,x3643,x3644,x3645))
% 1.49/1.60 [365]P9(x3651,x3652,x3653,x3654,x3655)+P3(x3651,f27(x3651,x3652,x3653,x3654,x3655),f28(x3651,x3652,x3653,x3654,x3655))
% 1.49/1.60 [366]P9(x3661,x3662,x3663,x3664,x3665)+P3(x3661,f29(x3661,x3662,x3663,x3664,x3665),f30(x3661,x3662,x3663,x3664,x3665))
% 1.49/1.60 [367]P5(x3671,x3672,x3673,x3674,x3675)+P3(x3673,f31(x3671,x3672,x3673,x3674,x3675),f33(x3671,x3672,x3673,x3674,x3675))
% 1.49/1.60 [368]P5(x3681,x3682,x3683,x3684,x3685)+P3(x3681,f31(x3681,x3682,x3683,x3684,x3685),f32(x3681,x3682,x3683,x3684,x3685))
% 1.49/1.60 [369]P5(x3691,x3692,x3693,x3694,x3695)+P3(x3691,f33(x3691,x3692,x3693,x3694,x3695),f34(x3691,x3692,x3693,x3694,x3695))
% 1.49/1.60 [372]P9(x3721,x3722,x3723,x3724,x3725)+~P3(x3725,f28(x3721,x3722,x3723,x3724,x3725),f30(x3721,x3722,x3723,x3724,x3725))
% 1.49/1.60 [373]P5(x3731,x3732,x3733,x3734,x3735)+~P3(x3735,f34(x3731,x3732,x3733,x3734,x3735),f32(x3731,x3732,x3733,x3734,x3735))
% 1.49/1.60 [377]P6(x3771,x3772,x3773,x3774,x3775,x3776)+P12(f8(x3771,x3772,x3773,x3774,x3775,x3776),x3774)
% 1.49/1.60 [378]P6(x3781,x3782,x3783,x3784,x3785,x3786)+P12(f9(x3781,x3782,x3783,x3784,x3785,x3786),x3786)
% 1.49/1.60 [267]~P13(x2672,x2671)+~P13(x2671,x2672)+P2(x2671,x2672)
% 1.49/1.60 [266]~P12(x2661,x2663)+P12(x2661,x2662)+~P13(x2663,x2662)
% 1.49/1.60 [285]~P7(x2851,x2853)+P3(x2851,x2852,x2852)+~P12(x2852,x2853)
% 1.49/1.60 [302]~P8(x3021,x3022,x3023)+~P15(x3021,x3022,x3023)+P14(x3021,x3022,x3023)
% 1.49/1.60 [271]~P12(x2713,x2712)+~P12(x2711,x2713)+P12(x2711,f58(x2712))
% 1.49/1.60 [272]E(x2721,x2722)+E(x2721,x2723)+~P12(x2721,f56(x2723,x2722))
% 1.49/1.60 [273]P12(x2731,x2732)+~P12(x2732,x2733)+~P12(x2731,f55(x2733))
% 1.49/1.60 [276]~P12(x2761,x2763)+P12(x2761,x2762)+P12(x2761,f3(x2763,x2762))
% 1.49/1.60 [282]~P12(x2821,x2823)+~P12(x2821,x2822)+P12(x2821,f50(x2822,x2823))
% 1.49/1.60 [284]P12(x2841,x2842)+P12(x2841,x2843)+~P12(x2841,f57(x2843,x2842))
% 1.49/1.60 [306]P1(x3061,x3062,x3063)+P12(f42(x3061,x3062,x3063),x3062)+P12(f44(x3061,x3062,x3063),x3062)
% 1.49/1.60 [307]P1(x3071,x3072,x3073)+P12(f42(x3071,x3072,x3073),x3072)+P12(f45(x3071,x3072,x3073),x3073)
% 1.49/1.60 [308]P1(x3081,x3082,x3083)+P12(f42(x3081,x3082,x3083),x3082)+P12(f46(x3081,x3082,x3083),x3083)
% 1.49/1.60 [314]P1(x3141,x3142,x3143)+P12(f42(x3141,x3142,x3143),x3142)+~E(f46(x3141,x3142,x3143),f45(x3141,x3142,x3143))
% 1.49/1.60 [316]P1(x3161,x3162,x3163)+P3(x3161,f44(x3161,x3162,x3163),f45(x3161,x3162,x3163))+P12(f42(x3161,x3162,x3163),x3162)
% 1.49/1.60 [317]P1(x3171,x3172,x3173)+P3(x3171,f44(x3171,x3172,x3173),f46(x3171,x3172,x3173))+P12(f42(x3171,x3172,x3173),x3172)
% 1.49/1.60 [288]~P3(x2882,x2884,x2881)+~P12(x2884,x2883)+P12(x2881,f41(x2882,x2883))
% 1.49/1.60 [289]~P3(x2892,x2891,x2894)+~P12(x2894,x2893)+P12(x2891,f52(x2892,x2893))
% 1.49/1.60 [313]P15(x3131,x3132,x3133)+~P12(x3134,x3132)+~P3(x3131,x3134,f19(x3131,x3132,x3133))
% 1.49/1.60 [326]~P12(x3264,x3262)+~P1(x3261,x3262,x3263)+P12(f43(x3261,x3262,x3263,x3264),x3263)
% 1.49/1.60 [327]~P12(x3274,x3273)+~P15(x3271,x3272,x3273)+P12(f20(x3271,x3272,x3273,x3274),x3272)
% 1.49/1.60 [329]~P12(x3292,x3293)+~P1(x3291,x3293,x3294)+P3(x3291,x3292,f43(x3291,x3293,x3294,x3292))
% 1.49/1.60 [330]~P12(x3304,x3303)+~P15(x3301,x3302,x3303)+P3(x3301,f20(x3301,x3302,x3303,x3304),x3304)
% 1.49/1.60 [349]P10(x3491,x3492,x3493,x3494)+P3(x3491,f23(x3491,x3492,x3493,x3494),f22(x3491,x3492,x3493,x3494))+P3(x3492,f22(x3491,x3492,x3493,x3494),f23(x3491,x3492,x3493,x3494))
% 1.49/1.60 [351]P10(x3511,x3512,x3513,x3514)+~P3(x3511,f23(x3511,x3512,x3513,x3514),f22(x3511,x3512,x3513,x3514))+~P3(x3512,f22(x3511,x3512,x3513,x3514),f23(x3511,x3512,x3513,x3514))
% 1.49/1.60 [379]P6(x3791,x3792,x3793,x3794,x3795,x3796)+P3(x3791,f8(x3791,x3792,x3793,x3794,x3795,x3796),f9(x3791,x3792,x3793,x3794,x3795,x3796))+P12(f10(x3791,x3792,x3793,x3794,x3795,x3796),x3795)
% 1.49/1.60 [380]P6(x3801,x3802,x3803,x3804,x3805,x3806)+P3(x3801,f8(x3801,x3802,x3803,x3804,x3805,x3806),f9(x3801,x3802,x3803,x3804,x3805,x3806))+P3(x3803,f8(x3801,x3802,x3803,x3804,x3805,x3806),f10(x3801,x3802,x3803,x3804,x3805,x3806))
% 1.49/1.60 [381]P6(x3811,x3812,x3813,x3814,x3815,x3816)+P3(x3811,f8(x3811,x3812,x3813,x3814,x3815,x3816),f9(x3811,x3812,x3813,x3814,x3815,x3816))+P3(x3812,f10(x3811,x3812,x3813,x3814,x3815,x3816),f9(x3811,x3812,x3813,x3814,x3815,x3816))
% 1.49/1.60 [318]P1(x3181,x3182,x3183)+~P12(x3184,x3183)+~P3(x3181,f42(x3181,x3182,x3183),x3184)+P12(f44(x3181,x3182,x3183),x3182)
% 1.49/1.60 [319]P1(x3191,x3192,x3193)+~P12(x3194,x3193)+~P3(x3191,f42(x3191,x3192,x3193),x3194)+P12(f45(x3191,x3192,x3193),x3193)
% 1.49/1.60 [320]P1(x3201,x3202,x3203)+~P12(x3204,x3203)+~P3(x3201,f42(x3201,x3202,x3203),x3204)+P12(f46(x3201,x3202,x3203),x3203)
% 1.49/1.60 [321]P1(x3211,x3212,x3213)+~P12(x3214,x3213)+~P3(x3211,f42(x3211,x3212,x3213),x3214)+~E(f46(x3211,x3212,x3213),f45(x3211,x3212,x3213))
% 1.49/1.60 [324]P1(x3241,x3242,x3243)+~P12(x3244,x3243)+P3(x3241,f44(x3241,x3242,x3243),f45(x3241,x3242,x3243))+~P3(x3241,f42(x3241,x3242,x3243),x3244)
% 1.49/1.60 [325]P1(x3251,x3252,x3253)+~P12(x3254,x3253)+P3(x3251,f44(x3251,x3252,x3253),f46(x3251,x3252,x3253))+~P3(x3251,f42(x3251,x3252,x3253),x3254)
% 1.49/1.60 [303]~P12(x3031,x3034)+~P3(x3032,x3035,x3031)+~P12(x3035,x3033)+P12(x3031,f51(x3032,x3033,x3034))
% 1.49/1.60 [304]~P12(x3041,x3044)+~P3(x3042,x3041,x3045)+~P12(x3045,x3043)+P12(x3041,f54(x3042,x3043,x3044))
% 1.49/1.60 [305]~P12(x3054,x3053)+~P12(x3055,x3052)+~P3(x3051,x3055,x3054)+P3(f53(x3051,x3052,x3053),x3054,x3055)
% 1.49/1.60 [315]P3(x3151,x3152,x3153)+~P12(x3152,x3154)+~P12(x3153,x3155)+~P3(f53(x3151,x3154,x3155),x3153,x3152)
% 1.49/1.60 [360]~P1(x3601,x3602,x3604)+~P14(x3601,x3602,x3604)+P11(x3601,x3602,x3603,x3604,x3605)+P12(f35(x3601,x3602,x3603,x3604,x3605),x3602)
% 1.49/1.60 [361]~P1(x3611,x3612,x3614)+~P14(x3611,x3612,x3614)+P11(x3611,x3612,x3613,x3614,x3615)+P12(f36(x3611,x3612,x3613,x3614,x3615),x3614)
% 1.49/1.60 [362]~P1(x3621,x3622,x3624)+~P14(x3621,x3622,x3624)+P11(x3621,x3622,x3623,x3624,x3625)+P12(f37(x3621,x3622,x3623,x3624,x3625),x3622)
% 1.49/1.60 [363]~P1(x3631,x3632,x3634)+~P14(x3631,x3632,x3634)+P11(x3631,x3632,x3633,x3634,x3635)+P12(f38(x3631,x3632,x3633,x3634,x3635),x3634)
% 1.49/1.60 [370]~P1(x3701,x3702,x3704)+~P14(x3701,x3702,x3704)+P11(x3701,x3702,x3703,x3704,x3705)+P3(x3701,f35(x3701,x3702,x3703,x3704,x3705),f36(x3701,x3702,x3703,x3704,x3705))
% 1.49/1.60 [371]~P1(x3711,x3712,x3714)+~P14(x3711,x3712,x3714)+P11(x3711,x3712,x3713,x3714,x3715)+P3(x3711,f37(x3711,x3712,x3713,x3714,x3715),f38(x3711,x3712,x3713,x3714,x3715))
% 1.49/1.60 [382]~P12(x3827,x3825)+~P12(x3826,x3823)+~P3(f4(x3821,x3822,x3823,x3824,x3825),x3826,x3827)+P12(f11(x3821,x3822,x3823,x3824,x3825,x3826,x3827),x3824)
% 1.49/1.60 [383]~P12(x3837,x3836)+~P12(x3832,x3834)+~P3(f4(x3833,x3831,x3834,x3835,x3836),x3832,x3837)+P3(x3831,x3832,f11(x3833,x3831,x3834,x3835,x3836,x3832,x3837))
% 1.49/1.60 [384]~P12(x3847,x3845)+~P12(x3846,x3843)+~P3(f4(x3841,x3842,x3843,x3844,x3845),x3846,x3847)+P3(x3841,f11(x3841,x3842,x3843,x3844,x3845,x3846,x3847),x3847)
% 1.49/1.60 [375]~P1(x3751,x3752,x3754)+~P14(x3751,x3752,x3754)+P11(x3751,x3752,x3753,x3754,x3755)+P3(x3755,f36(x3751,x3752,x3753,x3754,x3755),f38(x3751,x3752,x3753,x3754,x3755))+P3(x3753,f35(x3751,x3752,x3753,x3754,x3755),f37(x3751,x3752,x3753,x3754,x3755))
% 1.49/1.60 [376]~P1(x3761,x3762,x3764)+~P14(x3761,x3762,x3764)+P11(x3761,x3762,x3763,x3764,x3765)+~P3(x3765,f36(x3761,x3762,x3763,x3764,x3765),f38(x3761,x3762,x3763,x3764,x3765))+~P3(x3763,f35(x3761,x3762,x3763,x3764,x3765),f37(x3761,x3762,x3763,x3764,x3765))
% 1.49/1.60 [322]~P10(x3221,x3226,x3225,x3224)+P3(x3221,x3222,x3223)+~P12(x3222,x3224)+~P3(x3226,x3223,x3222)+~P12(x3223,x3225)
% 1.49/1.60 [323]~P10(x3236,x3231,x3234,x3235)+P3(x3231,x3232,x3233)+~P12(x3232,x3234)+~P3(x3236,x3233,x3232)+~P12(x3233,x3235)
% 1.49/1.60 [385]P6(x3851,x3852,x3853,x3854,x3855,x3856)+~P12(x3857,x3855)+~P3(x3852,x3857,f9(x3851,x3852,x3853,x3854,x3855,x3856))+~P3(x3853,f8(x3851,x3852,x3853,x3854,x3855,x3856),x3857)+~P3(x3851,f8(x3851,x3852,x3853,x3854,x3855,x3856),f9(x3851,x3852,x3853,x3854,x3855,x3856))
% 1.49/1.60 [386]~P12(x3868,x3866)+~P12(x3867,x3864)+~P3(x3861,x3867,x3868)+~P6(x3861,x3862,x3863,x3864,x3865,x3866)+P12(f47(x3861,x3862,x3863,x3864,x3865,x3866,x3867,x3868),x3865)
% 1.49/1.60 [387]~P12(x3878,x3877)+~P12(x3872,x3875)+~P3(x3873,x3872,x3878)+~P6(x3873,x3874,x3871,x3875,x3876,x3877)+P3(x3871,x3872,f47(x3873,x3874,x3871,x3875,x3876,x3877,x3872,x3878))
% 1.49/1.60 [388]~P12(x3888,x3886)+~P12(x3887,x3884)+~P3(x3882,x3887,x3888)+~P6(x3882,x3881,x3883,x3884,x3885,x3886)+P3(x3881,f47(x3882,x3881,x3883,x3884,x3885,x3886,x3887,x3888),x3888)
% 1.49/1.60 [350]~P12(x3507,x3505)+~P12(x3506,x3503)+~P3(x3501,x3508,x3507)+~P3(x3502,x3506,x3508)+~P12(x3508,x3504)+P3(f4(x3501,x3502,x3503,x3504,x3505),x3506,x3507)
% 1.49/1.60 [311]~P12(x3111,x3115)+~P3(x3116,x3111,x3113)+~P8(x3116,x3115,x3114)+E(x3111,x3112)+~P12(x3113,x3114)+~P3(x3116,x3112,x3113)+~P12(x3112,x3115)
% 1.49/1.60 [312]~P12(x3121,x3123)+~P3(x3126,x3124,x3122)+~P3(x3126,x3124,x3121)+E(x3121,x3122)+~P12(x3122,x3123)+~P1(x3126,x3125,x3123)+~P12(x3124,x3125)
% 1.49/1.60 [328]~P12(x3281,x3283)+~P4(x3287,x3286,x3285,x3283)+E(x3281,x3282)+~P12(x3282,x3283)+~P3(x3286,x3284,x3282)+~P3(x3287,x3284,x3281)+~P12(x3284,x3285)
% 1.49/1.60 [374]~P6(x3741,x3748,x3749,x3745,x3747,x3744)+P3(x3741,x3742,x3743)+~P12(x3743,x3744)+~P12(x3742,x3745)+~P3(x3748,x3746,x3743)+~P3(x3749,x3742,x3746)+~P12(x3746,x3747)
% 1.49/1.60 [345]~P12(x3453,x3454)+~P3(x3459,x3457,x3453)+~P5(x3459,x3456,x3458,x3454,x3451)+P3(x3451,x3452,x3453)+~P12(x3452,x3454)+~P3(x3458,x3457,x3455)+~P3(x3459,x3455,x3452)+~P12(x3455,x3456)+~P12(x3457,x3456)
% 1.49/1.60 [346]~P12(x3462,x3464)+~P3(x3469,x3467,x3462)+~P9(x3469,x3466,x3468,x3464,x3461)+P3(x3461,x3462,x3463)+~P12(x3463,x3464)+~P3(x3468,x3467,x3465)+~P3(x3469,x3465,x3463)+~P12(x3465,x3466)+~P12(x3467,x3466)
% 1.49/1.60 [347]~P12(x3472,x3474)+~P3(x3478,x3477,x3472)+~P11(x3478,x3476,x3479,x3474,x3471)+P3(x3471,x3472,x3473)+~P12(x3473,x3474)+~P3(x3478,x3475,x3473)+~P3(x3479,x3477,x3475)+~P12(x3475,x3476)+~P12(x3477,x3476)
% 1.49/1.60 [348]~P12(x3482,x3484)+~P3(x3488,x3482,x3487)+~P11(x3488,x3484,x3481,x3486,x3489)+P3(x3481,x3482,x3483)+~P12(x3483,x3484)+~P3(x3488,x3483,x3485)+~P3(x3489,x3487,x3485)+~P12(x3485,x3486)+~P12(x3487,x3486)
% 1.49/1.60 %EqnAxiom
% 1.49/1.60 [1]E(x11,x11)
% 1.49/1.60 [2]E(x22,x21)+~E(x21,x22)
% 1.49/1.60 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 1.49/1.60 [4]~E(x41,x42)+E(f41(x41,x43),f41(x42,x43))
% 1.49/1.60 [5]~E(x51,x52)+E(f41(x53,x51),f41(x53,x52))
% 1.49/1.60 [6]~E(x61,x62)+E(f48(x61),f48(x62))
% 1.49/1.60 [7]~E(x71,x72)+E(f9(x71,x73,x74,x75,x76,x77),f9(x72,x73,x74,x75,x76,x77))
% 1.49/1.60 [8]~E(x81,x82)+E(f9(x83,x81,x84,x85,x86,x87),f9(x83,x82,x84,x85,x86,x87))
% 1.49/1.60 [9]~E(x91,x92)+E(f9(x93,x94,x91,x95,x96,x97),f9(x93,x94,x92,x95,x96,x97))
% 1.49/1.60 [10]~E(x101,x102)+E(f9(x103,x104,x105,x101,x106,x107),f9(x103,x104,x105,x102,x106,x107))
% 1.49/1.60 [11]~E(x111,x112)+E(f9(x113,x114,x115,x116,x111,x117),f9(x113,x114,x115,x116,x112,x117))
% 1.49/1.60 [12]~E(x121,x122)+E(f9(x123,x124,x125,x126,x127,x121),f9(x123,x124,x125,x126,x127,x122))
% 1.49/1.60 [13]~E(x131,x132)+E(f49(x131),f49(x132))
% 1.49/1.60 [14]~E(x141,x142)+E(f56(x141,x143),f56(x142,x143))
% 1.49/1.60 [15]~E(x151,x152)+E(f56(x153,x151),f56(x153,x152))
% 1.49/1.60 [16]~E(x161,x162)+E(f4(x161,x163,x164,x165,x166),f4(x162,x163,x164,x165,x166))
% 1.49/1.60 [17]~E(x171,x172)+E(f4(x173,x171,x174,x175,x176),f4(x173,x172,x174,x175,x176))
% 1.49/1.60 [18]~E(x181,x182)+E(f4(x183,x184,x181,x185,x186),f4(x183,x184,x182,x185,x186))
% 1.49/1.60 [19]~E(x191,x192)+E(f4(x193,x194,x195,x191,x196),f4(x193,x194,x195,x192,x196))
% 1.49/1.60 [20]~E(x201,x202)+E(f4(x203,x204,x205,x206,x201),f4(x203,x204,x205,x206,x202))
% 1.49/1.60 [21]~E(x211,x212)+E(f11(x211,x213,x214,x215,x216,x217,x218),f11(x212,x213,x214,x215,x216,x217,x218))
% 1.49/1.60 [22]~E(x221,x222)+E(f11(x223,x221,x224,x225,x226,x227,x228),f11(x223,x222,x224,x225,x226,x227,x228))
% 1.49/1.60 [23]~E(x231,x232)+E(f11(x233,x234,x231,x235,x236,x237,x238),f11(x233,x234,x232,x235,x236,x237,x238))
% 1.49/1.60 [24]~E(x241,x242)+E(f11(x243,x244,x245,x241,x246,x247,x248),f11(x243,x244,x245,x242,x246,x247,x248))
% 1.49/1.60 [25]~E(x251,x252)+E(f11(x253,x254,x255,x256,x251,x257,x258),f11(x253,x254,x255,x256,x252,x257,x258))
% 1.49/1.60 [26]~E(x261,x262)+E(f11(x263,x264,x265,x266,x267,x261,x268),f11(x263,x264,x265,x266,x267,x262,x268))
% 1.49/1.60 [27]~E(x271,x272)+E(f11(x273,x274,x275,x276,x277,x278,x271),f11(x273,x274,x275,x276,x277,x278,x272))
% 1.49/1.60 [28]~E(x281,x282)+E(f5(x281,x283),f5(x282,x283))
% 1.49/1.60 [29]~E(x291,x292)+E(f5(x293,x291),f5(x293,x292))
% 1.49/1.60 [30]~E(x301,x302)+E(f6(x301,x303),f6(x302,x303))
% 1.49/1.60 [31]~E(x311,x312)+E(f6(x313,x311),f6(x313,x312))
% 1.49/1.60 [32]~E(x321,x322)+E(f55(x321),f55(x322))
% 1.49/1.60 [33]~E(x331,x332)+E(f16(x331,x333),f16(x332,x333))
% 1.49/1.60 [34]~E(x341,x342)+E(f16(x343,x341),f16(x343,x342))
% 1.49/1.60 [35]~E(x351,x352)+E(f57(x351,x353),f57(x352,x353))
% 1.49/1.60 [36]~E(x361,x362)+E(f57(x363,x361),f57(x363,x362))
% 1.49/1.60 [37]~E(x371,x372)+E(f8(x371,x373,x374,x375,x376,x377),f8(x372,x373,x374,x375,x376,x377))
% 1.49/1.60 [38]~E(x381,x382)+E(f8(x383,x381,x384,x385,x386,x387),f8(x383,x382,x384,x385,x386,x387))
% 1.49/1.60 [39]~E(x391,x392)+E(f8(x393,x394,x391,x395,x396,x397),f8(x393,x394,x392,x395,x396,x397))
% 1.49/1.60 [40]~E(x401,x402)+E(f8(x403,x404,x405,x401,x406,x407),f8(x403,x404,x405,x402,x406,x407))
% 1.49/1.60 [41]~E(x411,x412)+E(f8(x413,x414,x415,x416,x411,x417),f8(x413,x414,x415,x416,x412,x417))
% 1.49/1.60 [42]~E(x421,x422)+E(f8(x423,x424,x425,x426,x427,x421),f8(x423,x424,x425,x426,x427,x422))
% 1.49/1.60 [43]~E(x431,x432)+E(f58(x431),f58(x432))
% 1.49/1.60 [44]~E(x441,x442)+E(f37(x441,x443,x444,x445,x446),f37(x442,x443,x444,x445,x446))
% 1.49/1.60 [45]~E(x451,x452)+E(f37(x453,x451,x454,x455,x456),f37(x453,x452,x454,x455,x456))
% 1.49/1.60 [46]~E(x461,x462)+E(f37(x463,x464,x461,x465,x466),f37(x463,x464,x462,x465,x466))
% 1.49/1.60 [47]~E(x471,x472)+E(f37(x473,x474,x475,x471,x476),f37(x473,x474,x475,x472,x476))
% 1.49/1.60 [48]~E(x481,x482)+E(f37(x483,x484,x485,x486,x481),f37(x483,x484,x485,x486,x482))
% 1.49/1.60 [49]~E(x491,x492)+E(f35(x491,x493,x494,x495,x496),f35(x492,x493,x494,x495,x496))
% 1.49/1.60 [50]~E(x501,x502)+E(f35(x503,x501,x504,x505,x506),f35(x503,x502,x504,x505,x506))
% 1.49/1.60 [51]~E(x511,x512)+E(f35(x513,x514,x511,x515,x516),f35(x513,x514,x512,x515,x516))
% 1.49/1.60 [52]~E(x521,x522)+E(f35(x523,x524,x525,x521,x526),f35(x523,x524,x525,x522,x526))
% 1.49/1.60 [53]~E(x531,x532)+E(f35(x533,x534,x535,x536,x531),f35(x533,x534,x535,x536,x532))
% 1.49/1.60 [54]~E(x541,x542)+E(f17(x541,x543),f17(x542,x543))
% 1.49/1.60 [55]~E(x551,x552)+E(f17(x553,x551),f17(x553,x552))
% 1.49/1.60 [56]~E(x561,x562)+E(f38(x561,x563,x564,x565,x566),f38(x562,x563,x564,x565,x566))
% 1.49/1.60 [57]~E(x571,x572)+E(f38(x573,x571,x574,x575,x576),f38(x573,x572,x574,x575,x576))
% 1.49/1.60 [58]~E(x581,x582)+E(f38(x583,x584,x581,x585,x586),f38(x583,x584,x582,x585,x586))
% 1.49/1.60 [59]~E(x591,x592)+E(f38(x593,x594,x595,x591,x596),f38(x593,x594,x595,x592,x596))
% 1.49/1.60 [60]~E(x601,x602)+E(f38(x603,x604,x605,x606,x601),f38(x603,x604,x605,x606,x602))
% 1.49/1.60 [61]~E(x611,x612)+E(f36(x611,x613,x614,x615,x616),f36(x612,x613,x614,x615,x616))
% 1.49/1.60 [62]~E(x621,x622)+E(f36(x623,x621,x624,x625,x626),f36(x623,x622,x624,x625,x626))
% 1.49/1.60 [63]~E(x631,x632)+E(f36(x633,x634,x631,x635,x636),f36(x633,x634,x632,x635,x636))
% 1.49/1.60 [64]~E(x641,x642)+E(f36(x643,x644,x645,x641,x646),f36(x643,x644,x645,x642,x646))
% 1.49/1.60 [65]~E(x651,x652)+E(f36(x653,x654,x655,x656,x651),f36(x653,x654,x655,x656,x652))
% 1.49/1.60 [66]~E(x661,x662)+E(f32(x661,x663,x664,x665,x666),f32(x662,x663,x664,x665,x666))
% 1.49/1.60 [67]~E(x671,x672)+E(f32(x673,x671,x674,x675,x676),f32(x673,x672,x674,x675,x676))
% 1.49/1.60 [68]~E(x681,x682)+E(f32(x683,x684,x681,x685,x686),f32(x683,x684,x682,x685,x686))
% 1.49/1.60 [69]~E(x691,x692)+E(f32(x693,x694,x695,x691,x696),f32(x693,x694,x695,x692,x696))
% 1.49/1.60 [70]~E(x701,x702)+E(f32(x703,x704,x705,x706,x701),f32(x703,x704,x705,x706,x702))
% 1.49/1.60 [71]~E(x711,x712)+E(f3(x711,x713),f3(x712,x713))
% 1.49/1.60 [72]~E(x721,x722)+E(f3(x723,x721),f3(x723,x722))
% 1.49/1.60 [73]~E(x731,x732)+E(f50(x731,x733),f50(x732,x733))
% 1.49/1.60 [74]~E(x741,x742)+E(f50(x743,x741),f50(x743,x742))
% 1.49/1.60 [75]~E(x751,x752)+E(f27(x751,x753,x754,x755,x756),f27(x752,x753,x754,x755,x756))
% 1.49/1.60 [76]~E(x761,x762)+E(f27(x763,x761,x764,x765,x766),f27(x763,x762,x764,x765,x766))
% 1.49/1.60 [77]~E(x771,x772)+E(f27(x773,x774,x771,x775,x776),f27(x773,x774,x772,x775,x776))
% 1.49/1.60 [78]~E(x781,x782)+E(f27(x783,x784,x785,x781,x786),f27(x783,x784,x785,x782,x786))
% 1.49/1.60 [79]~E(x791,x792)+E(f27(x793,x794,x795,x796,x791),f27(x793,x794,x795,x796,x792))
% 1.49/1.60 [80]~E(x801,x802)+E(f29(x801,x803,x804,x805,x806),f29(x802,x803,x804,x805,x806))
% 1.49/1.60 [81]~E(x811,x812)+E(f29(x813,x811,x814,x815,x816),f29(x813,x812,x814,x815,x816))
% 1.49/1.60 [82]~E(x821,x822)+E(f29(x823,x824,x821,x825,x826),f29(x823,x824,x822,x825,x826))
% 1.49/1.60 [83]~E(x831,x832)+E(f29(x833,x834,x835,x831,x836),f29(x833,x834,x835,x832,x836))
% 1.49/1.60 [84]~E(x841,x842)+E(f29(x843,x844,x845,x846,x841),f29(x843,x844,x845,x846,x842))
% 1.49/1.60 [85]~E(x851,x852)+E(f30(x851,x853,x854,x855,x856),f30(x852,x853,x854,x855,x856))
% 1.49/1.60 [86]~E(x861,x862)+E(f30(x863,x861,x864,x865,x866),f30(x863,x862,x864,x865,x866))
% 1.49/1.60 [87]~E(x871,x872)+E(f30(x873,x874,x871,x875,x876),f30(x873,x874,x872,x875,x876))
% 1.49/1.60 [88]~E(x881,x882)+E(f30(x883,x884,x885,x881,x886),f30(x883,x884,x885,x882,x886))
% 1.49/1.60 [89]~E(x891,x892)+E(f30(x893,x894,x895,x896,x891),f30(x893,x894,x895,x896,x892))
% 1.49/1.60 [90]~E(x901,x902)+E(f31(x901,x903,x904,x905,x906),f31(x902,x903,x904,x905,x906))
% 1.49/1.60 [91]~E(x911,x912)+E(f31(x913,x911,x914,x915,x916),f31(x913,x912,x914,x915,x916))
% 1.49/1.60 [92]~E(x921,x922)+E(f31(x923,x924,x921,x925,x926),f31(x923,x924,x922,x925,x926))
% 1.49/1.60 [93]~E(x931,x932)+E(f31(x933,x934,x935,x931,x936),f31(x933,x934,x935,x932,x936))
% 1.49/1.60 [94]~E(x941,x942)+E(f31(x943,x944,x945,x946,x941),f31(x943,x944,x945,x946,x942))
% 1.49/1.60 [95]~E(x951,x952)+E(f10(x951,x953,x954,x955,x956,x957),f10(x952,x953,x954,x955,x956,x957))
% 1.49/1.60 [96]~E(x961,x962)+E(f10(x963,x961,x964,x965,x966,x967),f10(x963,x962,x964,x965,x966,x967))
% 1.49/1.60 [97]~E(x971,x972)+E(f10(x973,x974,x971,x975,x976,x977),f10(x973,x974,x972,x975,x976,x977))
% 1.49/1.60 [98]~E(x981,x982)+E(f10(x983,x984,x985,x981,x986,x987),f10(x983,x984,x985,x982,x986,x987))
% 1.49/1.60 [99]~E(x991,x992)+E(f10(x993,x994,x995,x996,x991,x997),f10(x993,x994,x995,x996,x992,x997))
% 1.49/1.60 [100]~E(x1001,x1002)+E(f10(x1003,x1004,x1005,x1006,x1007,x1001),f10(x1003,x1004,x1005,x1006,x1007,x1002))
% 1.49/1.60 [101]~E(x1011,x1012)+E(f34(x1011,x1013,x1014,x1015,x1016),f34(x1012,x1013,x1014,x1015,x1016))
% 1.49/1.60 [102]~E(x1021,x1022)+E(f34(x1023,x1021,x1024,x1025,x1026),f34(x1023,x1022,x1024,x1025,x1026))
% 1.49/1.60 [103]~E(x1031,x1032)+E(f34(x1033,x1034,x1031,x1035,x1036),f34(x1033,x1034,x1032,x1035,x1036))
% 1.49/1.60 [104]~E(x1041,x1042)+E(f34(x1043,x1044,x1045,x1041,x1046),f34(x1043,x1044,x1045,x1042,x1046))
% 1.49/1.60 [105]~E(x1051,x1052)+E(f34(x1053,x1054,x1055,x1056,x1051),f34(x1053,x1054,x1055,x1056,x1052))
% 1.49/1.60 [106]~E(x1061,x1062)+E(f28(x1061,x1063,x1064,x1065,x1066),f28(x1062,x1063,x1064,x1065,x1066))
% 1.49/1.60 [107]~E(x1071,x1072)+E(f28(x1073,x1071,x1074,x1075,x1076),f28(x1073,x1072,x1074,x1075,x1076))
% 1.49/1.60 [108]~E(x1081,x1082)+E(f28(x1083,x1084,x1081,x1085,x1086),f28(x1083,x1084,x1082,x1085,x1086))
% 1.49/1.60 [109]~E(x1091,x1092)+E(f28(x1093,x1094,x1095,x1091,x1096),f28(x1093,x1094,x1095,x1092,x1096))
% 1.49/1.60 [110]~E(x1101,x1102)+E(f28(x1103,x1104,x1105,x1106,x1101),f28(x1103,x1104,x1105,x1106,x1102))
% 1.49/1.60 [111]~E(x1111,x1112)+E(f33(x1111,x1113,x1114,x1115,x1116),f33(x1112,x1113,x1114,x1115,x1116))
% 1.49/1.60 [112]~E(x1121,x1122)+E(f33(x1123,x1121,x1124,x1125,x1126),f33(x1123,x1122,x1124,x1125,x1126))
% 1.49/1.60 [113]~E(x1131,x1132)+E(f33(x1133,x1134,x1131,x1135,x1136),f33(x1133,x1134,x1132,x1135,x1136))
% 1.49/1.60 [114]~E(x1141,x1142)+E(f33(x1143,x1144,x1145,x1141,x1146),f33(x1143,x1144,x1145,x1142,x1146))
% 1.49/1.60 [115]~E(x1151,x1152)+E(f33(x1153,x1154,x1155,x1156,x1151),f33(x1153,x1154,x1155,x1156,x1152))
% 1.49/1.60 [116]~E(x1161,x1162)+E(f47(x1161,x1163,x1164,x1165,x1166,x1167,x1168,x1169),f47(x1162,x1163,x1164,x1165,x1166,x1167,x1168,x1169))
% 1.49/1.60 [117]~E(x1171,x1172)+E(f47(x1173,x1171,x1174,x1175,x1176,x1177,x1178,x1179),f47(x1173,x1172,x1174,x1175,x1176,x1177,x1178,x1179))
% 1.49/1.60 [118]~E(x1181,x1182)+E(f47(x1183,x1184,x1181,x1185,x1186,x1187,x1188,x1189),f47(x1183,x1184,x1182,x1185,x1186,x1187,x1188,x1189))
% 1.49/1.60 [119]~E(x1191,x1192)+E(f47(x1193,x1194,x1195,x1191,x1196,x1197,x1198,x1199),f47(x1193,x1194,x1195,x1192,x1196,x1197,x1198,x1199))
% 1.49/1.60 [120]~E(x1201,x1202)+E(f47(x1203,x1204,x1205,x1206,x1201,x1207,x1208,x1209),f47(x1203,x1204,x1205,x1206,x1202,x1207,x1208,x1209))
% 1.49/1.60 [121]~E(x1211,x1212)+E(f47(x1213,x1214,x1215,x1216,x1217,x1211,x1218,x1219),f47(x1213,x1214,x1215,x1216,x1217,x1212,x1218,x1219))
% 1.49/1.60 [122]~E(x1221,x1222)+E(f47(x1223,x1224,x1225,x1226,x1227,x1228,x1221,x1229),f47(x1223,x1224,x1225,x1226,x1227,x1228,x1222,x1229))
% 1.49/1.60 [123]~E(x1231,x1232)+E(f47(x1233,x1234,x1235,x1236,x1237,x1238,x1239,x1231),f47(x1233,x1234,x1235,x1236,x1237,x1238,x1239,x1232))
% 1.49/1.60 [124]~E(x1241,x1242)+E(f52(x1241,x1243),f52(x1242,x1243))
% 1.49/1.60 [125]~E(x1251,x1252)+E(f52(x1253,x1251),f52(x1253,x1252))
% 1.49/1.60 [126]~E(x1261,x1262)+E(f14(x1261,x1263,x1264),f14(x1262,x1263,x1264))
% 1.49/1.60 [127]~E(x1271,x1272)+E(f14(x1273,x1271,x1274),f14(x1273,x1272,x1274))
% 1.49/1.60 [128]~E(x1281,x1282)+E(f14(x1283,x1284,x1281),f14(x1283,x1284,x1282))
% 1.49/1.60 [129]~E(x1291,x1292)+E(f15(x1291,x1293,x1294),f15(x1292,x1293,x1294))
% 1.49/1.60 [130]~E(x1301,x1302)+E(f15(x1303,x1301,x1304),f15(x1303,x1302,x1304))
% 1.49/1.60 [131]~E(x1311,x1312)+E(f15(x1313,x1314,x1311),f15(x1313,x1314,x1312))
% 1.49/1.60 [132]~E(x1321,x1322)+E(f18(x1321,x1323,x1324),f18(x1322,x1323,x1324))
% 1.49/1.60 [133]~E(x1331,x1332)+E(f18(x1333,x1331,x1334),f18(x1333,x1332,x1334))
% 1.49/1.60 [134]~E(x1341,x1342)+E(f18(x1343,x1344,x1341),f18(x1343,x1344,x1342))
% 1.49/1.60 [135]~E(x1351,x1352)+E(f19(x1351,x1353,x1354),f19(x1352,x1353,x1354))
% 1.49/1.60 [136]~E(x1361,x1362)+E(f19(x1363,x1361,x1364),f19(x1363,x1362,x1364))
% 1.49/1.60 [137]~E(x1371,x1372)+E(f19(x1373,x1374,x1371),f19(x1373,x1374,x1372))
% 1.49/1.61 [138]~E(x1381,x1382)+E(f22(x1381,x1383,x1384,x1385),f22(x1382,x1383,x1384,x1385))
% 1.49/1.61 [139]~E(x1391,x1392)+E(f22(x1393,x1391,x1394,x1395),f22(x1393,x1392,x1394,x1395))
% 1.49/1.61 [140]~E(x1401,x1402)+E(f22(x1403,x1404,x1401,x1405),f22(x1403,x1404,x1402,x1405))
% 1.49/1.61 [141]~E(x1411,x1412)+E(f22(x1413,x1414,x1415,x1411),f22(x1413,x1414,x1415,x1412))
% 1.49/1.61 [142]~E(x1421,x1422)+E(f13(x1421,x1423,x1424,x1425),f13(x1422,x1423,x1424,x1425))
% 1.49/1.61 [143]~E(x1431,x1432)+E(f13(x1433,x1431,x1434,x1435),f13(x1433,x1432,x1434,x1435))
% 1.49/1.61 [144]~E(x1441,x1442)+E(f13(x1443,x1444,x1441,x1445),f13(x1443,x1444,x1442,x1445))
% 1.49/1.61 [145]~E(x1451,x1452)+E(f13(x1453,x1454,x1455,x1451),f13(x1453,x1454,x1455,x1452))
% 1.49/1.61 [146]~E(x1461,x1462)+E(f21(x1461,x1463,x1464),f21(x1462,x1463,x1464))
% 1.49/1.61 [147]~E(x1471,x1472)+E(f21(x1473,x1471,x1474),f21(x1473,x1472,x1474))
% 1.49/1.61 [148]~E(x1481,x1482)+E(f21(x1483,x1484,x1481),f21(x1483,x1484,x1482))
% 1.49/1.61 [149]~E(x1491,x1492)+E(f23(x1491,x1493,x1494,x1495),f23(x1492,x1493,x1494,x1495))
% 1.49/1.61 [150]~E(x1501,x1502)+E(f23(x1503,x1501,x1504,x1505),f23(x1503,x1502,x1504,x1505))
% 1.49/1.61 [151]~E(x1511,x1512)+E(f23(x1513,x1514,x1511,x1515),f23(x1513,x1514,x1512,x1515))
% 1.49/1.61 [152]~E(x1521,x1522)+E(f23(x1523,x1524,x1525,x1521),f23(x1523,x1524,x1525,x1522))
% 1.49/1.61 [153]~E(x1531,x1532)+E(f24(x1531,x1533,x1534),f24(x1532,x1533,x1534))
% 1.49/1.61 [154]~E(x1541,x1542)+E(f24(x1543,x1541,x1544),f24(x1543,x1542,x1544))
% 1.49/1.61 [155]~E(x1551,x1552)+E(f24(x1553,x1554,x1551),f24(x1553,x1554,x1552))
% 1.49/1.61 [156]~E(x1561,x1562)+E(f25(x1561,x1563,x1564,x1565),f25(x1562,x1563,x1564,x1565))
% 1.49/1.61 [157]~E(x1571,x1572)+E(f25(x1573,x1571,x1574,x1575),f25(x1573,x1572,x1574,x1575))
% 1.49/1.61 [158]~E(x1581,x1582)+E(f25(x1583,x1584,x1581,x1585),f25(x1583,x1584,x1582,x1585))
% 1.49/1.61 [159]~E(x1591,x1592)+E(f25(x1593,x1594,x1595,x1591),f25(x1593,x1594,x1595,x1592))
% 1.49/1.61 [160]~E(x1601,x1602)+E(f51(x1601,x1603,x1604),f51(x1602,x1603,x1604))
% 1.49/1.61 [161]~E(x1611,x1612)+E(f51(x1613,x1611,x1614),f51(x1613,x1612,x1614))
% 1.49/1.61 [162]~E(x1621,x1622)+E(f51(x1623,x1624,x1621),f51(x1623,x1624,x1622))
% 1.49/1.61 [163]~E(x1631,x1632)+E(f54(x1631,x1633,x1634),f54(x1632,x1633,x1634))
% 1.49/1.61 [164]~E(x1641,x1642)+E(f54(x1643,x1641,x1644),f54(x1643,x1642,x1644))
% 1.49/1.61 [165]~E(x1651,x1652)+E(f54(x1653,x1654,x1651),f54(x1653,x1654,x1652))
% 1.49/1.61 [166]~E(x1661,x1662)+E(f26(x1661,x1663,x1664,x1665),f26(x1662,x1663,x1664,x1665))
% 1.49/1.61 [167]~E(x1671,x1672)+E(f26(x1673,x1671,x1674,x1675),f26(x1673,x1672,x1674,x1675))
% 1.49/1.61 [168]~E(x1681,x1682)+E(f26(x1683,x1684,x1681,x1685),f26(x1683,x1684,x1682,x1685))
% 1.49/1.61 [169]~E(x1691,x1692)+E(f26(x1693,x1694,x1695,x1691),f26(x1693,x1694,x1695,x1692))
% 1.49/1.61 [170]~E(x1701,x1702)+E(f20(x1701,x1703,x1704,x1705),f20(x1702,x1703,x1704,x1705))
% 1.49/1.61 [171]~E(x1711,x1712)+E(f20(x1713,x1711,x1714,x1715),f20(x1713,x1712,x1714,x1715))
% 1.49/1.61 [172]~E(x1721,x1722)+E(f20(x1723,x1724,x1721,x1725),f20(x1723,x1724,x1722,x1725))
% 1.49/1.61 [173]~E(x1731,x1732)+E(f20(x1733,x1734,x1735,x1731),f20(x1733,x1734,x1735,x1732))
% 1.49/1.61 [174]~E(x1741,x1742)+E(f44(x1741,x1743,x1744),f44(x1742,x1743,x1744))
% 1.49/1.61 [175]~E(x1751,x1752)+E(f44(x1753,x1751,x1754),f44(x1753,x1752,x1754))
% 1.49/1.61 [176]~E(x1761,x1762)+E(f44(x1763,x1764,x1761),f44(x1763,x1764,x1762))
% 1.49/1.61 [177]~E(x1771,x1772)+E(f46(x1771,x1773,x1774),f46(x1772,x1773,x1774))
% 1.49/1.61 [178]~E(x1781,x1782)+E(f46(x1783,x1781,x1784),f46(x1783,x1782,x1784))
% 1.49/1.61 [179]~E(x1791,x1792)+E(f46(x1793,x1794,x1791),f46(x1793,x1794,x1792))
% 1.49/1.61 [180]~E(x1801,x1802)+E(f12(x1801,x1803,x1804,x1805),f12(x1802,x1803,x1804,x1805))
% 1.49/1.61 [181]~E(x1811,x1812)+E(f12(x1813,x1811,x1814,x1815),f12(x1813,x1812,x1814,x1815))
% 1.49/1.61 [182]~E(x1821,x1822)+E(f12(x1823,x1824,x1821,x1825),f12(x1823,x1824,x1822,x1825))
% 1.49/1.61 [183]~E(x1831,x1832)+E(f12(x1833,x1834,x1835,x1831),f12(x1833,x1834,x1835,x1832))
% 1.49/1.61 [184]~E(x1841,x1842)+E(f42(x1841,x1843,x1844),f42(x1842,x1843,x1844))
% 1.49/1.61 [185]~E(x1851,x1852)+E(f42(x1853,x1851,x1854),f42(x1853,x1852,x1854))
% 1.49/1.61 [186]~E(x1861,x1862)+E(f42(x1863,x1864,x1861),f42(x1863,x1864,x1862))
% 1.49/1.61 [187]~E(x1871,x1872)+E(f43(x1871,x1873,x1874,x1875),f43(x1872,x1873,x1874,x1875))
% 1.49/1.61 [188]~E(x1881,x1882)+E(f43(x1883,x1881,x1884,x1885),f43(x1883,x1882,x1884,x1885))
% 1.49/1.61 [189]~E(x1891,x1892)+E(f43(x1893,x1894,x1891,x1895),f43(x1893,x1894,x1892,x1895))
% 1.49/1.61 [190]~E(x1901,x1902)+E(f43(x1903,x1904,x1905,x1901),f43(x1903,x1904,x1905,x1902))
% 1.49/1.61 [191]~E(x1911,x1912)+E(f7(x1911,x1913,x1914,x1915),f7(x1912,x1913,x1914,x1915))
% 1.49/1.61 [192]~E(x1921,x1922)+E(f7(x1923,x1921,x1924,x1925),f7(x1923,x1922,x1924,x1925))
% 1.49/1.61 [193]~E(x1931,x1932)+E(f7(x1933,x1934,x1931,x1935),f7(x1933,x1934,x1932,x1935))
% 1.49/1.61 [194]~E(x1941,x1942)+E(f7(x1943,x1944,x1945,x1941),f7(x1943,x1944,x1945,x1942))
% 1.49/1.61 [195]~E(x1951,x1952)+E(f53(x1951,x1953,x1954),f53(x1952,x1953,x1954))
% 1.49/1.61 [196]~E(x1961,x1962)+E(f53(x1963,x1961,x1964),f53(x1963,x1962,x1964))
% 1.49/1.61 [197]~E(x1971,x1972)+E(f53(x1973,x1974,x1971),f53(x1973,x1974,x1972))
% 1.49/1.61 [198]~E(x1981,x1982)+E(f45(x1981,x1983,x1984),f45(x1982,x1983,x1984))
% 1.49/1.61 [199]~E(x1991,x1992)+E(f45(x1993,x1991,x1994),f45(x1993,x1992,x1994))
% 1.49/1.61 [200]~E(x2001,x2002)+E(f45(x2003,x2004,x2001),f45(x2003,x2004,x2002))
% 1.49/1.61 [201]P1(x2012,x2013,x2014)+~E(x2011,x2012)+~P1(x2011,x2013,x2014)
% 1.49/1.61 [202]P1(x2023,x2022,x2024)+~E(x2021,x2022)+~P1(x2023,x2021,x2024)
% 1.49/1.61 [203]P1(x2033,x2034,x2032)+~E(x2031,x2032)+~P1(x2033,x2034,x2031)
% 1.49/1.61 [204]P12(x2042,x2043)+~E(x2041,x2042)+~P12(x2041,x2043)
% 1.49/1.61 [205]P12(x2053,x2052)+~E(x2051,x2052)+~P12(x2053,x2051)
% 1.49/1.61 [206]P2(x2062,x2063)+~E(x2061,x2062)+~P2(x2061,x2063)
% 1.49/1.61 [207]P2(x2073,x2072)+~E(x2071,x2072)+~P2(x2073,x2071)
% 1.49/1.61 [208]P3(x2082,x2083,x2084)+~E(x2081,x2082)+~P3(x2081,x2083,x2084)
% 1.49/1.61 [209]P3(x2093,x2092,x2094)+~E(x2091,x2092)+~P3(x2093,x2091,x2094)
% 1.49/1.61 [210]P3(x2103,x2104,x2102)+~E(x2101,x2102)+~P3(x2103,x2104,x2101)
% 1.49/1.61 [211]P15(x2112,x2113,x2114)+~E(x2111,x2112)+~P15(x2111,x2113,x2114)
% 1.49/1.61 [212]P15(x2123,x2122,x2124)+~E(x2121,x2122)+~P15(x2123,x2121,x2124)
% 1.49/1.61 [213]P15(x2133,x2134,x2132)+~E(x2131,x2132)+~P15(x2133,x2134,x2131)
% 1.49/1.61 [214]P13(x2142,x2143)+~E(x2141,x2142)+~P13(x2141,x2143)
% 1.49/1.61 [215]P13(x2153,x2152)+~E(x2151,x2152)+~P13(x2153,x2151)
% 1.49/1.61 [216]P9(x2162,x2163,x2164,x2165,x2166)+~E(x2161,x2162)+~P9(x2161,x2163,x2164,x2165,x2166)
% 1.49/1.61 [217]P9(x2173,x2172,x2174,x2175,x2176)+~E(x2171,x2172)+~P9(x2173,x2171,x2174,x2175,x2176)
% 1.49/1.61 [218]P9(x2183,x2184,x2182,x2185,x2186)+~E(x2181,x2182)+~P9(x2183,x2184,x2181,x2185,x2186)
% 1.49/1.61 [219]P9(x2193,x2194,x2195,x2192,x2196)+~E(x2191,x2192)+~P9(x2193,x2194,x2195,x2191,x2196)
% 1.49/1.61 [220]P9(x2203,x2204,x2205,x2206,x2202)+~E(x2201,x2202)+~P9(x2203,x2204,x2205,x2206,x2201)
% 1.49/1.61 [221]P5(x2212,x2213,x2214,x2215,x2216)+~E(x2211,x2212)+~P5(x2211,x2213,x2214,x2215,x2216)
% 1.49/1.61 [222]P5(x2223,x2222,x2224,x2225,x2226)+~E(x2221,x2222)+~P5(x2223,x2221,x2224,x2225,x2226)
% 1.49/1.61 [223]P5(x2233,x2234,x2232,x2235,x2236)+~E(x2231,x2232)+~P5(x2233,x2234,x2231,x2235,x2236)
% 1.49/1.61 [224]P5(x2243,x2244,x2245,x2242,x2246)+~E(x2241,x2242)+~P5(x2243,x2244,x2245,x2241,x2246)
% 1.49/1.61 [225]P5(x2253,x2254,x2255,x2256,x2252)+~E(x2251,x2252)+~P5(x2253,x2254,x2255,x2256,x2251)
% 1.49/1.61 [226]P4(x2262,x2263,x2264,x2265)+~E(x2261,x2262)+~P4(x2261,x2263,x2264,x2265)
% 1.49/1.61 [227]P4(x2273,x2272,x2274,x2275)+~E(x2271,x2272)+~P4(x2273,x2271,x2274,x2275)
% 1.49/1.61 [228]P4(x2283,x2284,x2282,x2285)+~E(x2281,x2282)+~P4(x2283,x2284,x2281,x2285)
% 1.49/1.61 [229]P4(x2293,x2294,x2295,x2292)+~E(x2291,x2292)+~P4(x2293,x2294,x2295,x2291)
% 1.49/1.61 [230]P8(x2302,x2303,x2304)+~E(x2301,x2302)+~P8(x2301,x2303,x2304)
% 1.49/1.61 [231]P8(x2313,x2312,x2314)+~E(x2311,x2312)+~P8(x2313,x2311,x2314)
% 1.49/1.61 [232]P8(x2323,x2324,x2322)+~E(x2321,x2322)+~P8(x2323,x2324,x2321)
% 1.49/1.61 [233]P11(x2332,x2333,x2334,x2335,x2336)+~E(x2331,x2332)+~P11(x2331,x2333,x2334,x2335,x2336)
% 1.49/1.61 [234]P11(x2343,x2342,x2344,x2345,x2346)+~E(x2341,x2342)+~P11(x2343,x2341,x2344,x2345,x2346)
% 1.49/1.61 [235]P11(x2353,x2354,x2352,x2355,x2356)+~E(x2351,x2352)+~P11(x2353,x2354,x2351,x2355,x2356)
% 1.49/1.61 [236]P11(x2363,x2364,x2365,x2362,x2366)+~E(x2361,x2362)+~P11(x2363,x2364,x2365,x2361,x2366)
% 1.49/1.61 [237]P11(x2373,x2374,x2375,x2376,x2372)+~E(x2371,x2372)+~P11(x2373,x2374,x2375,x2376,x2371)
% 1.49/1.61 [238]P7(x2382,x2383)+~E(x2381,x2382)+~P7(x2381,x2383)
% 1.49/1.61 [239]P7(x2393,x2392)+~E(x2391,x2392)+~P7(x2393,x2391)
% 1.49/1.61 [240]P10(x2402,x2403,x2404,x2405)+~E(x2401,x2402)+~P10(x2401,x2403,x2404,x2405)
% 1.49/1.61 [241]P10(x2413,x2412,x2414,x2415)+~E(x2411,x2412)+~P10(x2413,x2411,x2414,x2415)
% 1.49/1.61 [242]P10(x2423,x2424,x2422,x2425)+~E(x2421,x2422)+~P10(x2423,x2424,x2421,x2425)
% 1.49/1.61 [243]P10(x2433,x2434,x2435,x2432)+~E(x2431,x2432)+~P10(x2433,x2434,x2435,x2431)
% 1.49/1.61 [244]P14(x2442,x2443,x2444)+~E(x2441,x2442)+~P14(x2441,x2443,x2444)
% 1.49/1.61 [245]P14(x2453,x2452,x2454)+~E(x2451,x2452)+~P14(x2453,x2451,x2454)
% 1.49/1.61 [246]P14(x2463,x2464,x2462)+~E(x2461,x2462)+~P14(x2463,x2464,x2461)
% 1.49/1.61 [247]P6(x2472,x2473,x2474,x2475,x2476,x2477)+~E(x2471,x2472)+~P6(x2471,x2473,x2474,x2475,x2476,x2477)
% 1.49/1.61 [248]P6(x2483,x2482,x2484,x2485,x2486,x2487)+~E(x2481,x2482)+~P6(x2483,x2481,x2484,x2485,x2486,x2487)
% 1.49/1.61 [249]P6(x2493,x2494,x2492,x2495,x2496,x2497)+~E(x2491,x2492)+~P6(x2493,x2494,x2491,x2495,x2496,x2497)
% 1.49/1.61 [250]P6(x2503,x2504,x2505,x2502,x2506,x2507)+~E(x2501,x2502)+~P6(x2503,x2504,x2505,x2501,x2506,x2507)
% 1.49/1.61 [251]P6(x2513,x2514,x2515,x2516,x2512,x2517)+~E(x2511,x2512)+~P6(x2513,x2514,x2515,x2516,x2511,x2517)
% 1.49/1.61 [252]P6(x2523,x2524,x2525,x2526,x2527,x2522)+~E(x2521,x2522)+~P6(x2523,x2524,x2525,x2526,x2527,x2521)
% 1.49/1.61
% 1.49/1.61 %-------------------------------------------
% 1.49/1.61 cnf(389,plain,
% 1.49/1.61 (P12(x3891,f48(x3891))),
% 1.49/1.61 inference(equality_inference,[],[256])).
% 1.49/1.61 cnf(390,plain,
% 1.49/1.61 (P12(x3901,f56(x3902,x3901))),
% 1.49/1.61 inference(equality_inference,[],[261])).
% 1.49/1.61 cnf(391,plain,
% 1.49/1.61 (P12(x3911,f56(x3911,x3912))),
% 1.49/1.61 inference(equality_inference,[],[262])).
% 1.49/1.61 cnf(392,plain,
% 1.49/1.61 (P13(a2,x3921)),
% 1.49/1.61 inference(scs_inference,[],[254,264])).
% 1.49/1.61 cnf(393,plain,
% 1.49/1.61 (~P12(x3931,a2)),
% 1.49/1.61 inference(rename_variables,[],[254])).
% 1.49/1.61 cnf(396,plain,
% 1.49/1.61 (~P12(x3961,a2)),
% 1.49/1.61 inference(rename_variables,[],[254])).
% 1.49/1.61 cnf(398,plain,
% 1.49/1.61 (~P12(x3981,f58(a2))),
% 1.49/1.61 inference(scs_inference,[],[254,393,396,264,265,275])).
% 1.49/1.61 cnf(399,plain,
% 1.49/1.61 (~P12(x3991,a2)),
% 1.49/1.61 inference(rename_variables,[],[254])).
% 1.49/1.61 cnf(401,plain,
% 1.49/1.61 (P8(x4011,a2,x4012)),
% 1.49/1.61 inference(scs_inference,[],[254,393,396,399,264,265,275,290])).
% 1.49/1.61 cnf(402,plain,
% 1.49/1.61 (~P12(x4021,a2)),
% 1.49/1.61 inference(rename_variables,[],[254])).
% 1.49/1.61 cnf(404,plain,
% 1.49/1.61 (P8(x4041,f58(a2),x4042)),
% 1.49/1.61 inference(scs_inference,[],[254,393,396,399,264,265,275,290,291])).
% 1.49/1.61 cnf(406,plain,
% 1.49/1.61 (P8(x4061,x4062,a2)),
% 1.49/1.61 inference(scs_inference,[],[254,393,396,399,402,264,265,275,290,291,292])).
% 1.49/1.61 cnf(407,plain,
% 1.49/1.61 (~P12(x4071,a2)),
% 1.49/1.61 inference(rename_variables,[],[254])).
% 1.49/1.61 cnf(409,plain,
% 1.49/1.61 (P15(x4091,x4092,a2)),
% 1.49/1.61 inference(scs_inference,[],[254,393,396,399,402,407,264,265,275,290,291,292,293])).
% 1.49/1.61 cnf(410,plain,
% 1.49/1.61 (~P12(x4101,a2)),
% 1.49/1.61 inference(rename_variables,[],[254])).
% 1.49/1.61 cnf(412,plain,
% 1.49/1.61 (~P12(x4121,f41(x4122,a2))),
% 1.49/1.61 inference(scs_inference,[],[254,393,396,399,402,407,410,264,265,275,290,291,292,293,295])).
% 1.49/1.61 cnf(413,plain,
% 1.49/1.61 (~P12(x4131,a2)),
% 1.49/1.61 inference(rename_variables,[],[254])).
% 1.49/1.61 cnf(415,plain,
% 1.49/1.61 (~P12(x4151,f52(x4152,a2))),
% 1.49/1.61 inference(scs_inference,[],[254,393,396,399,402,407,410,413,264,265,275,290,291,292,293,295,296])).
% 1.49/1.61 cnf(416,plain,
% 1.49/1.61 (~P12(x4161,a2)),
% 1.49/1.61 inference(rename_variables,[],[254])).
% 1.49/1.61 cnf(418,plain,
% 1.49/1.61 (~P12(x4181,f51(x4182,a2,x4183))),
% 1.49/1.61 inference(scs_inference,[],[254,393,396,399,402,407,410,413,416,264,265,275,290,291,292,293,295,296,331])).
% 1.49/1.61 cnf(419,plain,
% 1.49/1.61 (~P12(x4191,a2)),
% 1.49/1.61 inference(rename_variables,[],[254])).
% 1.49/1.61 cnf(421,plain,
% 1.49/1.61 (~P12(x4211,f54(x4212,a2,x4213))),
% 1.49/1.61 inference(scs_inference,[],[254,393,396,399,402,407,410,413,416,419,264,265,275,290,291,292,293,295,296,331,332])).
% 1.49/1.61 cnf(422,plain,
% 1.49/1.61 (~P12(x4221,a2)),
% 1.49/1.61 inference(rename_variables,[],[254])).
% 1.49/1.61 cnf(425,plain,
% 1.49/1.61 (~P12(x4251,a2)),
% 1.49/1.61 inference(rename_variables,[],[254])).
% 1.49/1.61 cnf(428,plain,
% 1.49/1.61 (~P12(x4281,a2)),
% 1.49/1.61 inference(rename_variables,[],[254])).
% 1.49/1.61 cnf(433,plain,
% 1.49/1.61 (~P12(x4331,a2)),
% 1.49/1.61 inference(rename_variables,[],[254])).
% 1.49/1.61 cnf(436,plain,
% 1.49/1.61 (~P12(x4361,a2)),
% 1.49/1.61 inference(rename_variables,[],[254])).
% 1.49/1.61 cnf(439,plain,
% 1.49/1.61 (~P12(x4391,a2)),
% 1.49/1.61 inference(rename_variables,[],[254])).
% 1.49/1.61 cnf(442,plain,
% 1.49/1.61 (~P12(x4421,a2)),
% 1.49/1.61 inference(rename_variables,[],[254])).
% 1.49/1.61 cnf(449,plain,
% 1.49/1.61 (~P12(x4491,a2)),
% 1.49/1.61 inference(rename_variables,[],[254])).
% 1.49/1.61 cnf(452,plain,
% 1.49/1.61 (~P12(x4521,a2)),
% 1.49/1.61 inference(rename_variables,[],[254])).
% 1.49/1.61 cnf(457,plain,
% 1.49/1.61 (~P12(x4571,a2)),
% 1.49/1.61 inference(rename_variables,[],[254])).
% 1.49/1.61 cnf(460,plain,
% 1.49/1.61 (~P12(x4601,a2)),
% 1.49/1.61 inference(rename_variables,[],[254])).
% 1.49/1.61 cnf(462,plain,
% 1.49/1.61 (~P1(x4621,f48(x4622),a2)),
% 1.49/1.61 inference(scs_inference,[],[389,254,393,396,399,402,407,410,413,416,419,422,425,428,433,436,439,442,449,452,457,460,264,265,275,290,291,292,293,295,296,331,332,335,336,337,338,339,352,353,354,355,356,357,358,377,378,326])).
% 1.49/1.61 cnf(463,plain,
% 1.49/1.61 (~P12(x4631,a2)),
% 1.49/1.61 inference(rename_variables,[],[254])).
% 1.49/1.61 cnf(468,plain,
% 1.49/1.61 (~P15(x4681,a2,f48(x4682))),
% 1.49/1.61 inference(scs_inference,[],[255,389,254,393,396,399,402,407,410,413,416,419,422,425,428,433,436,439,442,449,452,457,460,463,264,265,275,290,291,292,293,295,296,331,332,335,336,337,338,339,352,353,354,355,356,357,358,377,378,326,267,206,327])).
% 1.49/1.61 cnf(469,plain,
% 1.49/1.61 (~P12(x4691,a2)),
% 1.49/1.61 inference(rename_variables,[],[254])).
% 1.49/1.61 cnf(472,plain,
% 1.49/1.61 (P12(x4721,f48(x4721))),
% 1.49/1.61 inference(rename_variables,[],[389])).
% 1.49/1.61 cnf(473,plain,
% 1.49/1.61 (P14(x4731,a2,a2)),
% 1.49/1.61 inference(scs_inference,[],[255,389,254,393,396,399,402,407,410,413,416,419,422,425,428,433,436,439,442,449,452,457,460,463,469,264,265,275,290,291,292,293,295,296,331,332,335,336,337,338,339,352,353,354,355,356,357,358,377,378,326,267,206,327,205,302])).
% 1.49/1.61 cnf(476,plain,
% 1.49/1.61 (~P3(f4(x4761,x4762,f48(x4763),a2,f48(x4763)),x4763,x4763)),
% 1.49/1.61 inference(scs_inference,[],[255,389,472,254,393,396,399,402,407,410,413,416,419,422,425,428,433,436,439,442,449,452,457,460,463,469,264,265,275,290,291,292,293,295,296,331,332,335,336,337,338,339,352,353,354,355,356,357,358,377,378,326,267,206,327,205,302,213,382])).
% 1.49/1.61 cnf(477,plain,
% 1.49/1.61 (~P12(x4771,a2)),
% 1.49/1.61 inference(rename_variables,[],[254])).
% 1.49/1.61 cnf(480,plain,
% 1.49/1.61 (~P7(f4(x4801,x4802,f48(x4803),a2,f48(x4803)),f48(x4803))),
% 1.49/1.61 inference(scs_inference,[],[253,255,389,472,254,393,396,399,402,407,410,413,416,419,422,425,428,433,436,439,442,449,452,457,460,463,469,264,265,275,290,291,292,293,295,296,331,332,335,336,337,338,339,352,353,354,355,356,357,358,377,378,326,267,206,327,205,302,213,382,201,285])).
% 1.49/1.61 cnf(485,plain,
% 1.49/1.61 (P1(x4851,a2,x4852)+P12(f44(x4851,a2,x4852),a2)),
% 1.49/1.61 inference(scs_inference,[],[253,255,389,472,254,393,396,399,402,407,410,413,416,419,422,425,428,433,436,439,442,449,452,457,460,463,469,477,264,265,275,290,291,292,293,295,296,331,332,335,336,337,338,339,352,353,354,355,356,357,358,377,378,326,267,206,327,205,302,213,382,201,285,202,203,207,306])).
% 1.49/1.61 cnf(498,plain,
% 1.49/1.61 (~P12(x4981,a2)),
% 1.49/1.61 inference(rename_variables,[],[254])).
% 1.49/1.61 cnf(504,plain,
% 1.49/1.61 (~P12(x5041,f51(x5042,a2,x5043))),
% 1.49/1.61 inference(rename_variables,[],[418])).
% 1.49/1.61 cnf(506,plain,
% 1.49/1.61 (P8(x5061,f51(x5062,a2,x5063),x5064)),
% 1.49/1.61 inference(scs_inference,[],[462,418,504,468,254,343,485,287,344,359,290])).
% 1.49/1.61 cnf(507,plain,
% 1.49/1.61 (~P12(x5071,f51(x5072,a2,x5073))),
% 1.49/1.61 inference(rename_variables,[],[418])).
% 1.49/1.61 cnf(510,plain,
% 1.49/1.61 (~P12(x5101,f51(x5102,a2,x5103))),
% 1.49/1.61 inference(rename_variables,[],[418])).
% 1.49/1.61 cnf(513,plain,
% 1.49/1.61 (~P12(x5131,f51(x5132,a2,x5133))),
% 1.49/1.61 inference(rename_variables,[],[418])).
% 1.49/1.61 cnf(516,plain,
% 1.49/1.61 (~P12(x5161,f51(x5162,a2,x5163))),
% 1.49/1.61 inference(rename_variables,[],[418])).
% 1.49/1.61 cnf(519,plain,
% 1.49/1.61 (~P12(x5191,f51(x5192,a2,x5193))),
% 1.49/1.61 inference(rename_variables,[],[418])).
% 1.49/1.61 cnf(521,plain,
% 1.49/1.61 (P13(f51(x5211,a2,x5212),x5213)),
% 1.49/1.61 inference(scs_inference,[],[462,418,504,507,510,513,516,519,468,254,343,485,287,344,359,290,296,336,295,275,264])).
% 1.49/1.61 cnf(522,plain,
% 1.49/1.61 (~P12(x5221,f51(x5222,a2,x5223))),
% 1.49/1.61 inference(rename_variables,[],[418])).
% 1.49/1.61 cnf(525,plain,
% 1.49/1.61 (~P12(x5251,f51(x5252,a2,x5253))),
% 1.49/1.61 inference(rename_variables,[],[418])).
% 1.49/1.61 cnf(528,plain,
% 1.49/1.61 (~P12(x5281,f51(x5282,a2,x5283))),
% 1.49/1.61 inference(rename_variables,[],[418])).
% 1.49/1.61 cnf(531,plain,
% 1.49/1.61 (~P12(x5311,f51(x5312,a2,x5313))),
% 1.49/1.61 inference(rename_variables,[],[418])).
% 1.49/1.61 cnf(534,plain,
% 1.49/1.61 (~P12(x5341,f54(x5342,a2,x5343))),
% 1.49/1.61 inference(rename_variables,[],[421])).
% 1.49/1.61 cnf(537,plain,
% 1.49/1.61 (~P12(x5371,f51(x5372,a2,x5373))),
% 1.49/1.61 inference(rename_variables,[],[418])).
% 1.49/1.61 cnf(540,plain,
% 1.49/1.61 (~P12(x5401,f51(x5402,a2,x5403))),
% 1.49/1.61 inference(rename_variables,[],[418])).
% 1.49/1.61 cnf(543,plain,
% 1.49/1.61 (~P12(x5431,f41(x5432,a2))),
% 1.49/1.61 inference(rename_variables,[],[412])).
% 1.49/1.61 cnf(549,plain,
% 1.49/1.61 (~P12(x5491,f51(x5492,a2,x5493))),
% 1.49/1.61 inference(rename_variables,[],[418])).
% 1.49/1.61 cnf(551,plain,
% 1.49/1.61 (P15(x5511,x5512,f51(x5513,a2,x5514))),
% 1.49/1.61 inference(scs_inference,[],[462,418,504,507,510,513,516,519,522,525,528,531,537,540,549,421,412,543,468,254,343,485,287,344,359,290,296,336,295,275,264,377,378,356,355,331,339,358,353,332,293])).
% 1.49/1.61 cnf(552,plain,
% 1.49/1.61 (~P12(x5521,f51(x5522,a2,x5523))),
% 1.49/1.61 inference(rename_variables,[],[418])).
% 1.49/1.61 cnf(555,plain,
% 1.49/1.61 (~P12(x5551,f51(x5552,a2,x5553))),
% 1.49/1.61 inference(rename_variables,[],[418])).
% 1.49/1.61 cnf(558,plain,
% 1.49/1.61 (~P12(x5581,f51(x5582,a2,x5583))),
% 1.49/1.61 inference(rename_variables,[],[418])).
% 1.49/1.61 cnf(561,plain,
% 1.49/1.61 (~P12(x5611,f54(x5612,a2,x5613))),
% 1.49/1.61 inference(rename_variables,[],[421])).
% 1.49/1.61 cnf(564,plain,
% 1.49/1.61 (~P12(x5641,f54(x5642,a2,x5643))),
% 1.49/1.61 inference(rename_variables,[],[421])).
% 1.49/1.61 cnf(567,plain,
% 1.49/1.61 (~P12(x5671,f51(x5672,a2,x5673))),
% 1.49/1.61 inference(rename_variables,[],[418])).
% 1.49/1.61 cnf(570,plain,
% 1.49/1.61 (~P12(x5701,f51(x5702,a2,x5703))),
% 1.49/1.61 inference(rename_variables,[],[418])).
% 1.49/1.61 cnf(572,plain,
% 1.49/1.61 (P8(x5721,f54(x5722,a2,x5723),x5724)),
% 1.49/1.61 inference(scs_inference,[],[462,418,504,507,510,513,516,519,522,525,528,531,537,540,549,552,555,558,567,421,534,561,564,412,543,468,254,343,485,287,344,359,290,296,336,295,275,264,377,378,356,355,331,339,358,353,332,293,292,354,352,357,335,338,291])).
% 1.49/1.61 cnf(573,plain,
% 1.49/1.61 (~P12(x5731,f54(x5732,a2,x5733))),
% 1.49/1.61 inference(rename_variables,[],[421])).
% 1.49/1.61 cnf(576,plain,
% 1.49/1.61 (~P12(x5761,f54(x5762,a2,x5763))),
% 1.49/1.61 inference(rename_variables,[],[421])).
% 1.49/1.61 cnf(578,plain,
% 1.49/1.61 (P7(x5781,f51(x5782,a2,x5783))),
% 1.49/1.61 inference(scs_inference,[],[462,418,504,507,510,513,516,519,522,525,528,531,537,540,549,552,555,558,567,570,421,534,561,564,573,412,543,468,254,343,485,287,344,359,290,296,336,295,275,264,377,378,356,355,331,339,358,353,332,293,292,354,352,357,335,338,291,337,265])).
% 1.49/1.61 cnf(579,plain,
% 1.49/1.61 (~P12(x5791,f51(x5792,a2,x5793))),
% 1.49/1.61 inference(rename_variables,[],[418])).
% 1.49/1.61 cnf(582,plain,
% 1.49/1.61 (~P12(x5821,f51(x5822,a2,x5823))),
% 1.49/1.61 inference(rename_variables,[],[418])).
% 1.49/1.61 cnf(583,plain,
% 1.49/1.61 (~P12(x5831,f54(x5832,a2,x5833))),
% 1.49/1.61 inference(rename_variables,[],[421])).
% 1.49/1.61 cnf(586,plain,
% 1.49/1.61 (~P7(f4(x5861,x5862,f48(x5863),a2,f48(x5863)),f56(x5864,x5863))),
% 1.49/1.61 inference(scs_inference,[],[462,390,476,480,418,504,507,510,513,516,519,522,525,528,531,537,540,549,552,555,558,567,570,579,421,534,561,564,573,576,412,543,468,254,343,485,287,344,359,290,296,336,295,275,264,377,378,356,355,331,339,358,353,332,293,292,354,352,357,335,338,291,337,265,308,239,285])).
% 1.49/1.61 cnf(587,plain,
% 1.49/1.61 (P12(x5871,f56(x5872,x5871))),
% 1.49/1.61 inference(rename_variables,[],[390])).
% 1.49/1.61 cnf(591,plain,
% 1.49/1.61 (~P12(x5911,f51(x5912,a2,x5913))),
% 1.49/1.61 inference(rename_variables,[],[418])).
% 1.49/1.61 cnf(593,plain,
% 1.49/1.61 (~P15(x5931,f51(x5932,a2,x5933),f56(x5934,x5935))),
% 1.49/1.61 inference(scs_inference,[],[462,390,587,476,480,418,504,507,510,513,516,519,522,525,528,531,537,540,549,552,555,558,567,570,579,582,591,421,534,561,564,573,576,583,412,543,468,254,343,485,287,344,359,290,296,336,295,275,264,377,378,356,355,331,339,358,353,332,293,292,354,352,357,335,338,291,337,265,308,239,285,307,327])).
% 1.49/1.61 cnf(594,plain,
% 1.49/1.61 (~P12(x5941,f51(x5942,a2,x5943))),
% 1.49/1.61 inference(rename_variables,[],[418])).
% 1.49/1.61 cnf(599,plain,
% 1.49/1.61 (P14(x5991,f58(a2),a2)),
% 1.49/1.61 inference(scs_inference,[],[462,390,587,476,480,418,504,507,510,513,516,519,522,525,528,531,537,540,549,552,555,558,567,570,579,582,591,421,534,561,564,573,576,583,412,543,404,409,468,392,254,343,485,287,344,359,290,296,336,295,275,264,377,378,356,355,331,339,358,353,332,293,292,354,352,357,335,338,291,337,265,308,239,285,307,327,267,302])).
% 1.49/1.61 cnf(603,plain,
% 1.49/1.61 (~P1(x6031,f56(x6032,x6033),f51(x6034,a2,x6035))),
% 1.49/1.61 inference(scs_inference,[],[462,390,587,476,480,418,504,507,510,513,516,519,522,525,528,531,537,540,549,552,555,558,567,570,579,582,591,594,421,534,561,564,573,576,583,412,543,404,409,468,392,254,343,485,287,344,359,290,296,336,295,275,264,377,378,356,355,331,339,358,353,332,293,292,354,352,357,335,338,291,337,265,308,239,285,307,327,267,302,326])).
% 1.49/1.61 cnf(604,plain,
% 1.49/1.61 (~P12(x6041,f51(x6042,a2,x6043))),
% 1.49/1.61 inference(rename_variables,[],[418])).
% 1.49/1.61 cnf(607,plain,
% 1.49/1.61 (P12(x6071,f56(x6072,x6071))),
% 1.49/1.61 inference(rename_variables,[],[390])).
% 1.49/1.61 cnf(614,plain,
% 1.49/1.61 (~P3(f4(x6141,x6142,f56(x6143,x6144),f51(x6145,a2,x6146),f56(x6143,x6144)),x6144,x6144)),
% 1.49/1.61 inference(scs_inference,[],[255,462,390,587,607,476,480,418,504,507,510,513,516,519,522,525,528,531,537,540,549,552,555,558,567,570,579,582,591,594,604,421,534,561,564,573,576,583,412,543,404,409,468,392,254,498,473,343,485,287,344,359,290,296,336,295,275,264,377,378,356,355,331,339,358,353,332,293,292,354,352,357,335,338,291,337,265,308,239,285,307,327,267,302,326,205,206,202,360,382])).
% 1.49/1.61 cnf(630,plain,
% 1.49/1.61 (~P12(x6301,f52(x6302,a2))),
% 1.49/1.61 inference(rename_variables,[],[415])).
% 1.49/1.61 cnf(633,plain,
% 1.49/1.61 (~P12(x6331,f52(x6332,a2))),
% 1.49/1.61 inference(rename_variables,[],[415])).
% 1.49/1.61 cnf(636,plain,
% 1.49/1.61 (~P12(x6361,f52(x6362,a2))),
% 1.49/1.61 inference(rename_variables,[],[415])).
% 1.49/1.61 cnf(639,plain,
% 1.49/1.61 (~P12(x6391,f52(x6392,a2))),
% 1.49/1.61 inference(rename_variables,[],[415])).
% 1.49/1.61 cnf(642,plain,
% 1.49/1.61 (~P12(x6421,f52(x6422,a2))),
% 1.49/1.61 inference(rename_variables,[],[415])).
% 1.49/1.61 cnf(644,plain,
% 1.49/1.61 (P8(x6441,f52(x6442,a2),x6443)),
% 1.49/1.62 inference(scs_inference,[],[603,415,630,633,636,639,642,593,343,287,295,336,378,296,275,290])).
% 1.49/1.62 cnf(645,plain,
% 1.49/1.62 (~P12(x6451,f52(x6452,a2))),
% 1.49/1.62 inference(rename_variables,[],[415])).
% 1.49/1.62 cnf(647,plain,
% 1.49/1.62 (P13(f52(x6471,a2),x6472)),
% 1.49/1.62 inference(scs_inference,[],[603,415,630,633,636,639,642,645,593,343,287,295,336,378,296,275,290,264])).
% 1.49/1.62 cnf(648,plain,
% 1.49/1.62 (~P12(x6481,f52(x6482,a2))),
% 1.49/1.62 inference(rename_variables,[],[415])).
% 1.49/1.62 cnf(651,plain,
% 1.49/1.62 (~P12(x6511,f52(x6512,a2))),
% 1.49/1.62 inference(rename_variables,[],[415])).
% 1.49/1.62 cnf(654,plain,
% 1.49/1.62 (~P12(x6541,f58(a2))),
% 1.49/1.62 inference(rename_variables,[],[398])).
% 1.49/1.62 cnf(656,plain,
% 1.49/1.62 (P15(x6561,x6562,f52(x6563,a2))),
% 1.49/1.62 inference(scs_inference,[],[603,415,630,633,636,639,642,645,648,651,398,593,343,287,295,336,378,296,275,290,264,359,352,293])).
% 1.49/1.62 cnf(657,plain,
% 1.49/1.62 (~P12(x6571,f52(x6572,a2))),
% 1.49/1.62 inference(rename_variables,[],[415])).
% 1.49/1.62 cnf(660,plain,
% 1.49/1.62 (~P12(x6601,f58(a2))),
% 1.49/1.62 inference(rename_variables,[],[398])).
% 1.49/1.62 cnf(663,plain,
% 1.49/1.62 (~P12(x6631,f52(x6632,a2))),
% 1.49/1.62 inference(rename_variables,[],[415])).
% 1.49/1.62 cnf(666,plain,
% 1.49/1.62 (~P12(x6661,f52(x6662,a2))),
% 1.49/1.62 inference(rename_variables,[],[415])).
% 1.49/1.62 cnf(669,plain,
% 1.49/1.62 (~P12(x6691,f52(x6692,a2))),
% 1.49/1.62 inference(rename_variables,[],[415])).
% 1.49/1.62 cnf(672,plain,
% 1.49/1.62 (~P12(x6721,f52(x6722,a2))),
% 1.49/1.62 inference(rename_variables,[],[415])).
% 1.49/1.62 cnf(675,plain,
% 1.49/1.62 (~P12(x6751,f52(x6752,a2))),
% 1.49/1.62 inference(rename_variables,[],[415])).
% 1.49/1.62 cnf(678,plain,
% 1.49/1.62 (~P12(x6781,f52(x6782,a2))),
% 1.49/1.62 inference(rename_variables,[],[415])).
% 1.49/1.62 cnf(681,plain,
% 1.49/1.62 (~P12(x6811,f58(a2))),
% 1.49/1.62 inference(rename_variables,[],[398])).
% 1.49/1.62 cnf(684,plain,
% 1.49/1.62 (~P12(x6841,f52(x6842,a2))),
% 1.49/1.62 inference(rename_variables,[],[415])).
% 1.49/1.62 cnf(686,plain,
% 1.49/1.62 (P8(x6861,f41(x6862,a2),x6863)),
% 1.49/1.62 inference(scs_inference,[],[603,415,630,633,636,639,642,645,648,651,657,663,666,669,672,675,678,398,654,660,593,412,343,287,295,336,378,296,275,290,264,359,352,293,357,332,377,331,358,338,265,337,355,291])).
% 1.49/1.62 cnf(687,plain,
% 1.49/1.62 (~P12(x6871,f41(x6872,a2))),
% 1.49/1.62 inference(rename_variables,[],[412])).
% 1.49/1.62 cnf(690,plain,
% 1.49/1.62 (~P12(x6901,f52(x6902,a2))),
% 1.49/1.62 inference(rename_variables,[],[415])).
% 1.49/1.62 cnf(693,plain,
% 1.49/1.62 (~P12(x6931,f58(a2))),
% 1.49/1.62 inference(rename_variables,[],[398])).
% 1.49/1.62 cnf(699,plain,
% 1.49/1.62 (~P12(x6991,f58(a2))),
% 1.49/1.62 inference(rename_variables,[],[398])).
% 1.49/1.62 cnf(702,plain,
% 1.49/1.62 (~P12(x7021,f52(x7022,a2))),
% 1.49/1.62 inference(rename_variables,[],[415])).
% 1.49/1.62 cnf(705,plain,
% 1.49/1.62 (~P12(x7051,f52(x7052,a2))),
% 1.49/1.62 inference(rename_variables,[],[415])).
% 1.49/1.62 cnf(707,plain,
% 1.49/1.62 (~P7(f4(x7071,x7072,f56(x7073,x7074),f51(x7075,a2,x7076),f56(x7073,x7074)),f56(x7074,x7077))),
% 1.49/1.62 inference(scs_inference,[],[603,415,630,633,636,639,642,645,648,651,657,663,666,669,672,675,678,684,690,702,398,654,660,681,693,391,614,593,412,687,343,287,295,336,378,296,275,290,264,359,352,293,357,332,377,331,358,338,265,337,355,291,339,356,354,353,292,335,285])).
% 1.49/1.62 cnf(708,plain,
% 1.49/1.62 (P12(x7081,f56(x7081,x7082))),
% 1.49/1.62 inference(rename_variables,[],[391])).
% 1.49/1.62 cnf(710,plain,
% 1.49/1.62 (~P15(x7101,f52(x7102,a2),f56(x7103,x7104))),
% 1.49/1.62 inference(scs_inference,[],[603,415,630,633,636,639,642,645,648,651,657,663,666,669,672,675,678,684,690,702,705,398,654,660,681,693,391,708,614,593,412,687,343,287,295,336,378,296,275,290,264,359,352,293,357,332,377,331,358,338,265,337,355,291,339,356,354,353,292,335,285,327])).
% 1.49/1.62 cnf(711,plain,
% 1.49/1.62 (~P12(x7111,f52(x7112,a2))),
% 1.49/1.62 inference(rename_variables,[],[415])).
% 1.49/1.62 cnf(713,plain,
% 1.49/1.62 (P1(x7131,f52(x7132,a2),f58(a2))),
% 1.49/1.62 inference(scs_inference,[],[603,415,630,633,636,639,642,645,648,651,657,663,666,669,672,675,678,684,690,702,705,711,398,654,660,681,693,699,391,708,614,593,412,687,343,287,295,336,378,296,275,290,264,359,352,293,357,332,377,331,358,338,265,337,355,291,339,356,354,353,292,335,285,327,308])).
% 1.49/1.62 cnf(714,plain,
% 1.49/1.62 (~P12(x7141,f52(x7142,a2))),
% 1.49/1.62 inference(rename_variables,[],[415])).
% 1.49/1.62 cnf(715,plain,
% 1.49/1.62 (~P12(x7151,f58(a2))),
% 1.49/1.62 inference(rename_variables,[],[398])).
% 1.49/1.62 cnf(727,plain,
% 1.49/1.62 (~P12(x7271,f52(x7272,a2))),
% 1.49/1.62 inference(rename_variables,[],[415])).
% 1.49/1.62 cnf(733,plain,
% 1.49/1.62 (~P1(x7331,f56(x7332,x7333),f52(x7334,a2))),
% 1.49/1.62 inference(scs_inference,[],[603,415,630,633,636,639,642,645,648,651,657,663,666,669,672,675,678,684,690,702,705,711,714,727,398,654,660,681,693,699,715,391,708,614,586,506,551,593,521,578,412,687,409,343,287,295,336,378,296,275,290,264,359,352,293,357,332,377,331,358,338,265,337,355,291,339,356,354,353,292,335,285,327,308,239,213,302,307,267,326])).
% 1.49/1.62 cnf(734,plain,
% 1.49/1.62 (~P12(x7341,f52(x7342,a2))),
% 1.49/1.62 inference(rename_variables,[],[415])).
% 1.49/1.62 cnf(738,plain,
% 1.49/1.62 (P12(x7381,f56(x7381,x7382))),
% 1.49/1.62 inference(rename_variables,[],[391])).
% 1.49/1.62 cnf(739,plain,
% 1.49/1.62 (~P3(f4(x7391,x7392,f56(x7393,x7394),f52(x7395,a2),f56(x7393,x7394)),x7393,x7393)),
% 1.49/1.62 inference(scs_inference,[],[603,415,630,633,636,639,642,645,648,651,657,663,666,669,672,675,678,684,690,702,705,711,714,727,734,398,654,660,681,693,699,715,391,708,738,614,586,506,551,593,521,578,412,687,409,343,287,295,336,378,296,275,290,264,359,352,293,357,332,377,331,358,338,265,337,355,291,339,356,354,353,292,335,285,327,308,239,213,302,307,267,326,202,205,382])).
% 1.49/1.62 cnf(750,plain,
% 1.49/1.62 (~P12(x7501,f58(a2))),
% 1.49/1.62 inference(rename_variables,[],[398])).
% 1.49/1.62 cnf(752,plain,
% 1.49/1.62 (P8(x7521,f41(x7522,f58(a2)),x7523)),
% 1.49/1.62 inference(scs_inference,[],[733,398,343,295,290])).
% 1.49/1.62 cnf(754,plain,
% 1.49/1.62 (P13(f58(a2),x7541)),
% 1.49/1.62 inference(scs_inference,[],[733,398,750,343,295,290,264])).
% 1.49/1.62 cnf(755,plain,
% 1.49/1.62 (~P12(x7551,f58(a2))),
% 1.49/1.62 inference(rename_variables,[],[398])).
% 1.49/1.62 cnf(763,plain,
% 1.49/1.62 (~P12(x7631,f58(a2))),
% 1.49/1.62 inference(rename_variables,[],[398])).
% 1.49/1.62 cnf(766,plain,
% 1.49/1.62 (~P12(x7661,f58(a2))),
% 1.49/1.62 inference(rename_variables,[],[398])).
% 1.49/1.62 cnf(769,plain,
% 1.49/1.62 (~P12(x7691,f58(a2))),
% 1.49/1.62 inference(rename_variables,[],[398])).
% 1.49/1.62 cnf(776,plain,
% 1.49/1.62 (~P12(x7761,f58(a2))),
% 1.49/1.62 inference(rename_variables,[],[398])).
% 1.49/1.62 cnf(778,plain,
% 1.49/1.62 (P8(x7781,x7782,f58(a2))),
% 1.49/1.62 inference(scs_inference,[],[733,398,750,755,763,766,769,776,710,412,343,295,290,264,357,287,378,275,296,359,356,331,292])).
% 1.49/1.62 cnf(779,plain,
% 1.49/1.62 (~P12(x7791,f58(a2))),
% 1.49/1.62 inference(rename_variables,[],[398])).
% 1.49/1.62 cnf(781,plain,
% 1.49/1.62 (P15(x7811,x7812,f58(a2))),
% 1.49/1.62 inference(scs_inference,[],[733,398,750,755,763,766,769,776,779,710,412,343,295,290,264,357,287,378,275,296,359,356,331,292,293])).
% 1.49/1.62 cnf(782,plain,
% 1.49/1.62 (~P12(x7821,f58(a2))),
% 1.49/1.62 inference(rename_variables,[],[398])).
% 1.49/1.62 cnf(785,plain,
% 1.49/1.62 (~P12(x7851,f58(a2))),
% 1.49/1.62 inference(rename_variables,[],[398])).
% 1.49/1.62 cnf(788,plain,
% 1.49/1.62 (~P12(x7881,f58(a2))),
% 1.49/1.62 inference(rename_variables,[],[398])).
% 1.49/1.62 cnf(791,plain,
% 1.49/1.62 (~P12(x7911,f58(a2))),
% 1.49/1.62 inference(rename_variables,[],[398])).
% 1.49/1.62 cnf(796,plain,
% 1.49/1.62 (~P12(x7961,f58(a2))),
% 1.49/1.62 inference(rename_variables,[],[398])).
% 1.49/1.62 cnf(799,plain,
% 1.49/1.62 (~P12(x7991,f58(a2))),
% 1.49/1.62 inference(rename_variables,[],[398])).
% 1.49/1.62 cnf(802,plain,
% 1.49/1.62 (~P12(x8021,f58(a2))),
% 1.49/1.62 inference(rename_variables,[],[398])).
% 1.49/1.62 cnf(804,plain,
% 1.49/1.62 (P8(x8041,f54(x8042,f58(a2),x8043),x8044)),
% 1.49/1.62 inference(scs_inference,[],[733,398,750,755,763,766,769,776,779,782,785,788,791,796,799,710,412,343,295,290,264,357,287,378,275,296,359,356,331,292,293,338,339,377,358,265,335,332,291])).
% 1.49/1.62 cnf(807,plain,
% 1.49/1.62 (P12(x8071,f56(x8072,x8071))),
% 1.49/1.62 inference(rename_variables,[],[390])).
% 1.49/1.62 cnf(809,plain,
% 1.49/1.62 (~P15(x8091,a2,f56(x8092,x8093))),
% 1.49/1.62 inference(scs_inference,[],[733,254,398,750,755,763,766,769,776,779,782,785,788,791,796,799,739,710,390,807,412,343,295,290,264,357,287,378,275,296,359,356,331,292,293,338,339,377,358,265,335,332,291,285,327])).
% 1.49/1.62 cnf(810,plain,
% 1.49/1.62 (~P12(x8101,a2)),
% 1.49/1.62 inference(rename_variables,[],[254])).
% 1.49/1.62 cnf(814,plain,
% 1.49/1.62 (~P12(x8141,a2)),
% 1.49/1.62 inference(rename_variables,[],[254])).
% 1.49/1.62 cnf(817,plain,
% 1.49/1.62 (~P12(x8171,f58(a2))),
% 1.49/1.62 inference(rename_variables,[],[398])).
% 1.49/1.62 cnf(818,plain,
% 1.49/1.62 (~P12(x8181,a2)),
% 1.49/1.62 inference(rename_variables,[],[254])).
% 1.49/1.62 cnf(821,plain,
% 1.49/1.62 (P15(x8211,x8212,f52(x8213,a2))),
% 1.49/1.62 inference(rename_variables,[],[656])).
% 1.49/1.62 cnf(822,plain,
% 1.49/1.62 (P14(x8221,f54(x8222,a2,x8223),f52(x8224,a2))),
% 1.49/1.62 inference(scs_inference,[],[733,254,810,814,415,398,750,755,763,766,769,776,779,782,785,788,791,796,799,802,739,572,656,821,710,390,807,412,343,295,290,264,357,287,378,275,296,359,356,331,292,293,338,339,377,358,265,335,332,291,285,327,307,308,213,302])).
% 1.49/1.62 cnf(826,plain,
% 1.49/1.62 (~P1(x8261,f56(x8262,x8263),a2)),
% 1.49/1.62 inference(scs_inference,[],[733,254,810,814,818,415,398,750,755,763,766,769,776,779,782,785,788,791,796,799,802,739,572,656,821,710,390,807,412,343,295,290,264,357,287,378,275,296,359,356,331,292,293,338,339,377,358,265,335,332,291,285,327,307,308,213,302,326])).
% 1.49/1.62 cnf(827,plain,
% 1.49/1.62 (~P12(x8271,a2)),
% 1.49/1.62 inference(rename_variables,[],[254])).
% 1.49/1.62 cnf(835,plain,
% 1.49/1.62 (P12(x8351,f56(x8352,x8351))),
% 1.49/1.62 inference(rename_variables,[],[390])).
% 1.49/1.62 cnf(840,plain,
% 1.49/1.62 (~P3(f4(x8401,x8402,f56(x8403,x8404),a2,f56(x8403,x8404)),x8404,x8404)),
% 1.49/1.62 inference(scs_inference,[],[733,462,254,810,814,818,827,415,398,750,755,763,766,769,776,779,782,785,788,791,796,799,802,817,392,739,572,656,821,710,647,390,807,835,412,599,343,295,290,264,357,287,378,275,296,359,356,331,292,293,338,339,377,358,265,335,332,291,285,327,307,308,213,302,326,267,202,205,362,382])).
% 1.49/1.62 cnf(852,plain,
% 1.49/1.62 (P13(f54(x8521,a2,x8522),x8523)),
% 1.49/1.62 inference(scs_inference,[],[826,421,343,264])).
% 1.49/1.62 cnf(853,plain,
% 1.49/1.62 (~P12(x8531,f54(x8532,a2,x8533))),
% 1.49/1.62 inference(rename_variables,[],[421])).
% 1.49/1.62 cnf(856,plain,
% 1.49/1.62 (~P12(x8561,f54(x8562,a2,x8563))),
% 1.49/1.62 inference(rename_variables,[],[421])).
% 1.49/1.62 cnf(859,plain,
% 1.49/1.62 (~P12(x8591,f54(x8592,a2,x8593))),
% 1.49/1.62 inference(rename_variables,[],[421])).
% 1.49/1.62 cnf(862,plain,
% 1.49/1.62 (~P12(x8621,f54(x8622,a2,x8623))),
% 1.49/1.62 inference(rename_variables,[],[421])).
% 1.49/1.62 cnf(873,plain,
% 1.49/1.62 (~P12(x8731,f54(x8732,a2,x8733))),
% 1.49/1.62 inference(rename_variables,[],[421])).
% 1.49/1.62 cnf(876,plain,
% 1.49/1.62 (~P12(x8761,f54(x8762,a2,x8763))),
% 1.49/1.62 inference(rename_variables,[],[421])).
% 1.49/1.62 cnf(879,plain,
% 1.49/1.62 (~P12(x8791,f54(x8792,a2,x8793))),
% 1.49/1.62 inference(rename_variables,[],[421])).
% 1.49/1.62 cnf(882,plain,
% 1.49/1.62 (~P12(x8821,f54(x8822,a2,x8823))),
% 1.49/1.62 inference(rename_variables,[],[421])).
% 1.49/1.62 cnf(885,plain,
% 1.49/1.62 (~P12(x8851,f54(x8852,a2,x8853))),
% 1.49/1.62 inference(rename_variables,[],[421])).
% 1.49/1.62 cnf(888,plain,
% 1.49/1.62 (~P12(x8881,f54(x8882,a2,x8883))),
% 1.49/1.62 inference(rename_variables,[],[421])).
% 1.49/1.62 cnf(893,plain,
% 1.49/1.62 (~P12(x8931,f54(x8932,a2,x8933))),
% 1.49/1.62 inference(rename_variables,[],[421])).
% 1.49/1.62 cnf(896,plain,
% 1.49/1.62 (~P12(x8961,f54(x8962,a2,x8963))),
% 1.49/1.62 inference(rename_variables,[],[421])).
% 1.49/1.62 cnf(899,plain,
% 1.49/1.62 (~P12(x8991,f54(x8992,a2,x8993))),
% 1.49/1.62 inference(rename_variables,[],[421])).
% 1.49/1.62 cnf(903,plain,
% 1.49/1.62 (P15(x9031,x9032,f54(x9033,a2,x9034))),
% 1.49/1.62 inference(scs_inference,[],[826,421,853,856,859,862,873,876,879,882,885,888,893,896,899,809,343,264,295,296,275,352,354,355,287,292,378,332,335,339,331,358,377,338,265,291,293])).
% 1.49/1.62 cnf(904,plain,
% 1.49/1.62 (~P12(x9041,f54(x9042,a2,x9043))),
% 1.49/1.62 inference(rename_variables,[],[421])).
% 1.49/1.62 cnf(906,plain,
% 1.49/1.62 (~P15(x9061,f54(x9062,a2,x9063),f56(x9064,x9065))),
% 1.49/1.62 inference(scs_inference,[],[826,421,853,856,859,862,873,876,879,882,885,888,893,896,899,904,809,391,343,264,295,296,275,352,354,355,287,292,378,332,335,339,331,358,377,338,265,291,293,327])).
% 1.49/1.62 cnf(907,plain,
% 1.49/1.62 (~P12(x9071,f54(x9072,a2,x9073))),
% 1.49/1.62 inference(rename_variables,[],[421])).
% 1.49/1.62 cnf(910,plain,
% 1.49/1.62 (P12(x9101,f56(x9101,x9102))),
% 1.49/1.62 inference(rename_variables,[],[391])).
% 1.49/1.62 cnf(914,plain,
% 1.49/1.62 (~P12(x9141,a2)),
% 1.49/1.62 inference(rename_variables,[],[254])).
% 1.49/1.62 cnf(920,plain,
% 1.49/1.62 (~P1(x9201,f56(x9202,x9203),f54(x9204,a2,x9205))),
% 1.49/1.62 inference(scs_inference,[],[826,254,418,421,853,856,859,862,873,876,879,882,885,888,893,896,899,904,907,551,804,840,809,391,910,343,264,295,296,275,352,354,355,287,292,378,332,335,339,331,358,377,338,265,291,293,327,285,307,302,326])).
% 1.49/1.62 cnf(921,plain,
% 1.49/1.62 (~P12(x9211,f54(x9212,a2,x9213))),
% 1.49/1.62 inference(rename_variables,[],[421])).
% 1.49/1.62 cnf(925,plain,
% 1.49/1.62 (~P12(x9251,a2)),
% 1.49/1.62 inference(rename_variables,[],[254])).
% 1.49/1.62 cnf(931,plain,
% 1.49/1.62 (~P3(f4(x9311,x9312,f56(x9313,x9314),a2,f56(x9313,x9314)),x9313,x9313)),
% 1.49/1.62 inference(scs_inference,[],[826,254,914,925,418,421,853,856,859,862,873,876,879,882,885,888,893,896,899,904,907,921,551,521,392,804,840,809,391,910,343,264,295,296,275,352,354,355,287,292,378,332,335,339,331,358,377,338,265,291,293,327,285,307,302,326,308,267,382])).
% 1.49/1.62 cnf(942,plain,
% 1.49/1.62 (~P12(x9421,f41(x9422,a2))),
% 1.49/1.62 inference(rename_variables,[],[412])).
% 1.49/1.62 cnf(945,plain,
% 1.49/1.62 (~P12(x9451,f41(x9452,a2))),
% 1.49/1.62 inference(rename_variables,[],[412])).
% 1.49/1.62 cnf(953,plain,
% 1.49/1.62 (P13(f41(x9531,a2),x9532)),
% 1.49/1.62 inference(scs_inference,[],[920,412,942,945,906,343,295,296,337,355,287,264])).
% 1.49/1.62 cnf(954,plain,
% 1.49/1.62 (~P12(x9541,f41(x9542,a2))),
% 1.49/1.62 inference(rename_variables,[],[412])).
% 1.49/1.62 cnf(957,plain,
% 1.49/1.62 (~P12(x9571,f41(x9572,a2))),
% 1.49/1.62 inference(rename_variables,[],[412])).
% 1.49/1.62 cnf(960,plain,
% 1.49/1.62 (~P12(x9601,f41(x9602,a2))),
% 1.49/1.62 inference(rename_variables,[],[412])).
% 1.49/1.62 cnf(963,plain,
% 1.49/1.62 (~P12(x9631,f41(x9632,a2))),
% 1.49/1.62 inference(rename_variables,[],[412])).
% 1.49/1.62 cnf(966,plain,
% 1.49/1.62 (~P12(x9661,f41(x9662,a2))),
% 1.49/1.62 inference(rename_variables,[],[412])).
% 1.49/1.62 cnf(971,plain,
% 1.49/1.62 (~P12(x9711,f41(x9712,a2))),
% 1.49/1.62 inference(rename_variables,[],[412])).
% 1.49/1.62 cnf(974,plain,
% 1.49/1.62 (~P12(x9741,f41(x9742,a2))),
% 1.49/1.62 inference(rename_variables,[],[412])).
% 1.49/1.62 cnf(977,plain,
% 1.49/1.62 (~P12(x9771,f41(x9772,a2))),
% 1.49/1.62 inference(rename_variables,[],[412])).
% 1.49/1.62 cnf(980,plain,
% 1.49/1.62 (~P12(x9801,f41(x9802,a2))),
% 1.49/1.62 inference(rename_variables,[],[412])).
% 1.49/1.62 cnf(983,plain,
% 1.49/1.62 (~P12(x9831,f41(x9832,a2))),
% 1.49/1.62 inference(rename_variables,[],[412])).
% 1.49/1.62 cnf(985,plain,
% 1.49/1.62 (P7(x9851,f41(x9852,a2))),
% 1.49/1.62 inference(scs_inference,[],[920,412,942,945,954,957,960,963,966,971,974,977,980,983,906,343,295,296,337,355,287,264,275,292,335,378,358,293,332,338,377,331,265])).
% 1.49/1.62 cnf(986,plain,
% 1.49/1.62 (~P12(x9861,f41(x9862,a2))),
% 1.49/1.62 inference(rename_variables,[],[412])).
% 1.49/1.62 cnf(989,plain,
% 1.49/1.62 (~P12(x9891,f41(x9892,a2))),
% 1.49/1.62 inference(rename_variables,[],[412])).
% 1.49/1.62 cnf(992,plain,
% 1.49/1.62 (P1(x9921,f41(x9922,a2),f52(x9923,a2))),
% 1.49/1.62 inference(scs_inference,[],[920,415,412,942,945,954,957,960,963,966,971,974,977,980,983,986,989,707,906,343,295,296,337,355,287,264,275,292,335,378,358,293,332,338,377,331,265,339,239,307])).
% 1.49/1.62 cnf(994,plain,
% 1.49/1.62 (~P12(x9941,f52(x9942,a2))),
% 1.49/1.62 inference(rename_variables,[],[415])).
% 1.49/1.62 cnf(997,plain,
% 1.49/1.62 (P12(x9971,f56(x9972,x9971))),
% 1.49/1.62 inference(rename_variables,[],[390])).
% 1.49/1.62 cnf(999,plain,
% 1.49/1.62 (~P15(x9991,f58(a2),f56(x9992,x9993))),
% 1.49/1.62 inference(scs_inference,[],[920,415,398,412,942,945,954,957,960,963,966,971,974,977,980,983,986,989,390,997,707,931,906,343,295,296,337,355,287,264,275,292,335,378,358,293,332,338,377,331,265,339,239,307,285,327])).
% 1.49/1.62 cnf(1000,plain,
% 1.49/1.62 (~P12(x10001,f58(a2))),
% 1.49/1.62 inference(rename_variables,[],[398])).
% 1.49/1.62 cnf(1008,plain,
% 1.49/1.62 (~P12(x10081,f52(x10082,a2))),
% 1.49/1.62 inference(rename_variables,[],[415])).
% 1.49/1.62 cnf(1010,plain,
% 1.49/1.62 (~P1(x10101,f56(x10102,x10103),f58(a2))),
% 1.49/1.62 inference(scs_inference,[],[920,415,994,398,1000,409,412,942,945,954,957,960,963,966,971,974,977,980,983,986,989,418,752,390,997,707,931,906,343,295,296,337,355,287,264,275,292,335,378,358,293,332,338,377,331,265,339,239,307,285,327,302,308,326])).
% 1.49/1.62 cnf(1019,plain,
% 1.49/1.62 (~P3(f4(x10191,x10192,f56(x10193,x10194),f52(x10195,a2),f56(x10193,x10194)),x10194,x10194)),
% 1.49/1.62 inference(scs_inference,[],[920,415,994,1008,398,1000,409,412,942,945,954,957,960,963,966,971,974,977,980,983,986,989,418,752,754,390,997,389,707,931,906,343,295,296,337,355,287,264,275,292,335,378,358,293,332,338,377,331,265,339,239,307,285,327,302,308,326,267,205,382])).
% 1.49/1.62 cnf(1036,plain,
% 1.49/1.62 (~P12(x10361,f41(x10362,a2))),
% 1.49/1.62 inference(rename_variables,[],[412])).
% 1.49/1.62 cnf(1039,plain,
% 1.49/1.62 (~P15(x10391,f41(x10392,a2),f56(x10393,x10394))),
% 1.49/1.62 inference(scs_inference,[],[1010,254,412,1036,391,999,343,287,307,327])).
% 1.49/1.62 cnf(1040,plain,
% 1.49/1.62 (~P12(x10401,f41(x10402,a2))),
% 1.49/1.62 inference(rename_variables,[],[412])).
% 1.49/1.62 cnf(1043,plain,
% 1.49/1.62 (P12(x10431,f56(x10431,x10432))),
% 1.49/1.62 inference(rename_variables,[],[391])).
% 1.49/1.62 cnf(1053,plain,
% 1.49/1.62 (~P1(x10531,f56(x10532,x10533),f41(x10534,a2))),
% 1.49/1.62 inference(scs_inference,[],[1010,254,781,412,1036,1040,644,647,391,1043,1019,999,343,287,307,327,285,302,267,326])).
% 1.49/1.62 cnf(1059,plain,
% 1.49/1.62 (~P3(f4(x10591,x10592,f56(x10593,x10594),f54(x10595,a2,x10596),f56(x10593,x10594)),x10593,x10593)),
% 1.49/1.62 inference(scs_inference,[],[1010,254,421,398,781,412,1036,1040,644,647,391,1043,713,1019,999,343,287,307,327,285,302,267,326,361,382])).
% 1.49/1.62 cnf(1072,plain,
% 1.49/1.62 (~P12(x10721,f52(x10722,a2))),
% 1.49/1.62 inference(rename_variables,[],[415])).
% 1.49/1.62 cnf(1076,plain,
% 1.49/1.62 (~P12(x10761,f54(x10762,a2,x10763))),
% 1.49/1.62 inference(rename_variables,[],[421])).
% 1.49/1.62 cnf(1077,plain,
% 1.49/1.62 (~P12(x10771,f52(x10772,a2))),
% 1.49/1.62 inference(rename_variables,[],[415])).
% 1.49/1.62 cnf(1084,plain,
% 1.49/1.62 (P12(x10841,f56(x10842,x10841))),
% 1.49/1.62 inference(rename_variables,[],[390])).
% 1.49/1.62 cnf(1097,plain,
% 1.49/1.62 (~P3(f4(x10971,x10972,f56(x10973,x10974),f54(x10975,a2,x10976),f56(x10973,x10974)),x10974,x10974)),
% 1.49/1.62 inference(scs_inference,[],[1053,415,1072,1077,418,656,421,1076,412,521,686,852,390,1084,992,1059,1039,822,343,287,307,308,302,285,267,363,362,382])).
% 1.49/1.62 cnf(1111,plain,
% 1.49/1.62 (~P15(x11111,f58(a2),f48(x11112))),
% 1.49/1.62 inference(scs_inference,[],[398,389,327])).
% 1.49/1.62 cnf(1112,plain,
% 1.49/1.62 (~P12(x11121,f58(a2))),
% 1.49/1.62 inference(rename_variables,[],[398])).
% 1.49/1.62 cnf(1119,plain,
% 1.49/1.62 (~P12(x11191,f58(a2))),
% 1.49/1.62 inference(rename_variables,[],[398])).
% 1.49/1.62 cnf(1121,plain,
% 1.49/1.62 (~P7(f4(x11211,x11212,f56(x11213,x11214),f54(x11215,a2,x11216),f56(x11213,x11214)),f48(x11214))),
% 1.49/1.62 inference(scs_inference,[],[398,1112,551,389,401,1097,327,302,326,285])).
% 1.49/1.62 cnf(1122,plain,
% 1.49/1.62 (P12(x11221,f48(x11221))),
% 1.49/1.62 inference(rename_variables,[],[389])).
% 1.49/1.62 cnf(1128,plain,
% 1.49/1.62 (~P3(f4(x11281,x11282,f48(x11283),f58(a2),f48(x11283)),x11283,x11283)),
% 1.49/1.62 inference(scs_inference,[],[398,1112,1119,551,392,754,389,1122,401,1097,327,302,326,285,267,382])).
% 1.49/1.62 cnf(1149,plain,
% 1.49/1.62 (P12(x11491,f56(x11491,x11492))),
% 1.49/1.62 inference(rename_variables,[],[391])).
% 1.49/1.62 cnf(1155,plain,
% 1.49/1.62 (~P3(f4(x11551,x11552,f56(x11553,x11554),f51(x11555,a2,x11556),f56(x11553,x11554)),x11553,x11553)),
% 1.49/1.62 inference(scs_inference,[],[418,409,903,985,647,392,391,1149,406,1121,1128,1111,213,239,302,285,267,382])).
% 1.49/1.62 cnf(1177,plain,
% 1.49/1.62 ($false),
% 1.49/1.62 inference(scs_inference,[],[255,781,953,392,778,390,1155,302,285,267]),
% 1.49/1.62 ['proof']).
% 1.49/1.62 % SZS output end Proof
% 1.49/1.62 % Total time :0.850000s
%------------------------------------------------------------------------------