%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1.1
% Problem : LCL686+1.015 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 01:10:15 PM UTC 2026
% Result : Theorem 182.47s 182.74s
% Output : Proof 182.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 46
% Syntax : Number of formulae : 74 ( 9 unt; 44 def)
% Number of atoms : 2514 ( 0 equ)
% Maximal formula atoms : 440 ( 33 avg)
% Number of connectives : 4229 (1789 ~;1349 |;1047 &)
% ( 0 <=>; 0 =>; 44 <=; 0 <~>)
% Maximal formula depth : 179 ( 17 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 91 ( 90 usr; 1 prp; 0-2 aty)
% Number of functors : 49 ( 49 usr; 4 con; 0-1 aty)
% Number of variables : 570 ( 0 sgn 506 !; 53 ?)
% Comments :
%------------------------------------------------------------------------------
% FILE RECORD
fof(main,conjecture,
~ ? [X1] :
~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ p45(X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) )
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| $false )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p44(X2)
& ~ p43(X2) )
| ( ~ p44(X2)
& p43(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p43(X1)
& ~ p42(X1) )
| ( ~ p43(X1)
& p42(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p42(X2)
& ~ p41(X2) )
| ( ~ p42(X2)
& p41(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p41(X1)
& ~ p40(X1) )
| ( ~ p41(X1)
& p40(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p40(X2)
& ~ p39(X2) )
| ( ~ p40(X2)
& p39(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p39(X1)
& ~ p38(X1) )
| ( ~ p39(X1)
& p38(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p38(X2)
& ~ p37(X2) )
| ( ~ p38(X2)
& p37(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p37(X1)
& ~ p36(X1) )
| ( ~ p37(X1)
& p36(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p36(X2)
& ~ p35(X2) )
| ( ~ p36(X2)
& p35(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p35(X1)
& ~ p34(X1) )
| ( ~ p35(X1)
& p34(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p34(X2)
& ~ p33(X2) )
| ( ~ p34(X2)
& p33(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p33(X1)
& ~ p32(X1) )
| ( ~ p33(X1)
& p32(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p32(X2)
& ~ p31(X2) )
| ( ~ p32(X2)
& p31(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p31(X1)
& ~ p30(X1) )
| ( ~ p31(X1)
& p30(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p30(X2)
& ~ p29(X2) )
| ( ~ p30(X2)
& p29(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p29(X1)
& ~ p28(X1) )
| ( ~ p29(X1)
& p28(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p28(X2)
& ~ p27(X2) )
| ( ~ p28(X2)
& p27(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p27(X1)
& ~ p26(X1) )
| ( ~ p27(X1)
& p26(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p26(X2)
& ~ p25(X2) )
| ( ~ p26(X2)
& p25(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p25(X1)
& ~ p24(X1) )
| ( ~ p25(X1)
& p24(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p24(X2)
& ~ p23(X2) )
| ( ~ p24(X2)
& p23(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p23(X1)
& ~ p22(X1) )
| ( ~ p23(X1)
& p22(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p22(X2)
& ~ p21(X2) )
| ( ~ p22(X2)
& p21(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p21(X1)
& ~ p20(X1) )
| ( ~ p21(X1)
& p20(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p20(X2)
& ~ p19(X2) )
| ( ~ p20(X2)
& p19(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p19(X1)
& ~ p18(X1) )
| ( ~ p19(X1)
& p18(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p18(X2)
& ~ p17(X2) )
| ( ~ p18(X2)
& p17(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p17(X1)
& ~ p16(X1) )
| ( ~ p17(X1)
& p16(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p16(X2)
& ~ p15(X2) )
| ( ~ p16(X2)
& p15(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p15(X1)
& ~ p14(X1) )
| ( ~ p15(X1)
& p14(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p14(X2)
& ~ p13(X2) )
| ( ~ p14(X2)
& p13(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p13(X1)
& ~ p12(X1) )
| ( ~ p13(X1)
& p12(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p12(X2)
& ~ p11(X2) )
| ( ~ p12(X2)
& p11(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p11(X1)
& ~ p10(X1) )
| ( ~ p11(X1)
& p10(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p10(X2)
& ~ p9(X2) )
| ( ~ p10(X2)
& p9(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p9(X1)
& ~ p8(X1) )
| ( ~ p9(X1)
& p8(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p8(X2)
& ~ p7(X2) )
| ( ~ p8(X2)
& p7(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p7(X1)
& ~ p6(X1) )
| ( ~ p7(X1)
& p6(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p6(X2)
& ~ p5(X2) )
| ( ~ p6(X2)
& p5(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p5(X1)
& ~ p4(X1) )
| ( ~ p5(X1)
& p4(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p4(X2)
& ~ p3(X2) )
| ( ~ p4(X2)
& p3(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p3(X1)
& ~ p2(X1) )
| ( ~ p3(X1)
& p2(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p2(X2)
& ~ p1(X2) )
| ( ~ p2(X2)
& p1(X2) ) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p45(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| ( ~ p43(X2)
& ~ p44(X2) )
| ( p44(X2)
& p43(X2) )
| ( ~ p42(X2)
& ~ p43(X2) )
| ( p43(X2)
& p42(X2) )
| ( ~ p41(X2)
& ~ p42(X2) )
| ( p42(X2)
& p41(X2) )
| ( ~ p40(X2)
& ~ p41(X2) )
| ( p41(X2)
& p40(X2) )
| ( ~ p39(X2)
& ~ p40(X2) )
| ( p40(X2)
& p39(X2) )
| ( ~ p38(X2)
& ~ p39(X2) )
| ( p39(X2)
& p38(X2) )
| ( ~ p37(X2)
& ~ p38(X2) )
| ( p38(X2)
& p37(X2) )
| ( ~ p36(X2)
& ~ p37(X2) )
| ( p37(X2)
& p36(X2) )
| ( ~ p35(X2)
& ~ p36(X2) )
| ( p36(X2)
& p35(X2) )
| ( ~ p34(X2)
& ~ p35(X2) )
| ( p35(X2)
& p34(X2) )
| ( ~ p33(X2)
& ~ p34(X2) )
| ( p34(X2)
& p33(X2) )
| ( ~ p32(X2)
& ~ p33(X2) )
| ( p33(X2)
& p32(X2) )
| ( ~ p31(X2)
& ~ p32(X2) )
| ( p32(X2)
& p31(X2) )
| ( ~ p30(X2)
& ~ p31(X2) )
| ( p31(X2)
& p30(X2) )
| ( ~ p29(X2)
& ~ p30(X2) )
| ( p30(X2)
& p29(X2) )
| ( ~ p28(X2)
& ~ p29(X2) )
| ( p29(X2)
& p28(X2) )
| ( ~ p27(X2)
& ~ p28(X2) )
| ( p28(X2)
& p27(X2) )
| ( ~ p26(X2)
& ~ p27(X2) )
| ( p27(X2)
& p26(X2) )
| ( ~ p25(X2)
& ~ p26(X2) )
| ( p26(X2)
& p25(X2) )
| ( ~ p24(X2)
& ~ p25(X2) )
| ( p25(X2)
& p24(X2) )
| ( ~ p23(X2)
& ~ p24(X2) )
| ( p24(X2)
& p23(X2) )
| ( ~ p22(X2)
& ~ p23(X2) )
| ( p23(X2)
& p22(X2) )
| ( ~ p21(X2)
& ~ p22(X2) )
| ( p22(X2)
& p21(X2) )
| ( ~ p20(X2)
& ~ p21(X2) )
| ( p21(X2)
& p20(X2) )
| ( ~ p19(X2)
& ~ p20(X2) )
| ( p20(X2)
& p19(X2) )
| ( ~ p18(X2)
& ~ p19(X2) )
| ( p19(X2)
& p18(X2) )
| ( ~ p17(X2)
& ~ p18(X2) )
| ( p18(X2)
& p17(X2) )
| ( ~ p16(X2)
& ~ p17(X2) )
| ( p17(X2)
& p16(X2) )
| ( ~ p15(X2)
& ~ p16(X2) )
| ( p16(X2)
& p15(X2) )
| ( ~ p14(X2)
& ~ p15(X2) )
| ( p15(X2)
& p14(X2) )
| ( ~ p13(X2)
& ~ p14(X2) )
| ( p14(X2)
& p13(X2) )
| ( ~ p12(X2)
& ~ p13(X2) )
| ( p13(X2)
& p12(X2) )
| ( ~ p11(X2)
& ~ p12(X2) )
| ( p12(X2)
& p11(X2) )
| ( ~ p10(X2)
& ~ p11(X2) )
| ( p11(X2)
& p10(X2) )
| ( ~ p9(X2)
& ~ p10(X2) )
| ( p10(X2)
& p9(X2) )
| ( ~ p8(X2)
& ~ p9(X2) )
| ( p9(X2)
& p8(X2) )
| ( ~ p7(X2)
& ~ p8(X2) )
| ( p8(X2)
& p7(X2) )
| ( ~ p6(X2)
& ~ p7(X2) )
| ( p7(X2)
& p6(X2) )
| ( ~ p5(X2)
& ~ p6(X2) )
| ( p6(X2)
& p5(X2) )
| ( ~ p4(X2)
& ~ p5(X2) )
| ( p5(X2)
& p4(X2) )
| ( ~ p3(X2)
& ~ p4(X2) )
| ( p4(X2)
& p3(X2) )
| ( ~ p2(X2)
& ~ p3(X2) )
| ( p3(X2)
& p2(X2) )
| ( ~ p1(X2)
& ~ p2(X2) )
| ( p2(X2)
& p1(X2) ) ) ) ) ) ),
file('theBenchmark.p',main) ).
% NEGATING CONJECTURE
fof(main_nc,negated_conjecture,
? [X1] :
~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ p45(X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) )
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| $false )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p44(X2)
& ~ p43(X2) )
| ( ~ p44(X2)
& p43(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p43(X1)
& ~ p42(X1) )
| ( ~ p43(X1)
& p42(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p42(X2)
& ~ p41(X2) )
| ( ~ p42(X2)
& p41(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p41(X1)
& ~ p40(X1) )
| ( ~ p41(X1)
& p40(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p40(X2)
& ~ p39(X2) )
| ( ~ p40(X2)
& p39(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p39(X1)
& ~ p38(X1) )
| ( ~ p39(X1)
& p38(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p38(X2)
& ~ p37(X2) )
| ( ~ p38(X2)
& p37(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p37(X1)
& ~ p36(X1) )
| ( ~ p37(X1)
& p36(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p36(X2)
& ~ p35(X2) )
| ( ~ p36(X2)
& p35(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p35(X1)
& ~ p34(X1) )
| ( ~ p35(X1)
& p34(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p34(X2)
& ~ p33(X2) )
| ( ~ p34(X2)
& p33(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p33(X1)
& ~ p32(X1) )
| ( ~ p33(X1)
& p32(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p32(X2)
& ~ p31(X2) )
| ( ~ p32(X2)
& p31(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p31(X1)
& ~ p30(X1) )
| ( ~ p31(X1)
& p30(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p30(X2)
& ~ p29(X2) )
| ( ~ p30(X2)
& p29(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p29(X1)
& ~ p28(X1) )
| ( ~ p29(X1)
& p28(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p28(X2)
& ~ p27(X2) )
| ( ~ p28(X2)
& p27(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p27(X1)
& ~ p26(X1) )
| ( ~ p27(X1)
& p26(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p26(X2)
& ~ p25(X2) )
| ( ~ p26(X2)
& p25(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p25(X1)
& ~ p24(X1) )
| ( ~ p25(X1)
& p24(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p24(X2)
& ~ p23(X2) )
| ( ~ p24(X2)
& p23(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p23(X1)
& ~ p22(X1) )
| ( ~ p23(X1)
& p22(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p22(X2)
& ~ p21(X2) )
| ( ~ p22(X2)
& p21(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p21(X1)
& ~ p20(X1) )
| ( ~ p21(X1)
& p20(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p20(X2)
& ~ p19(X2) )
| ( ~ p20(X2)
& p19(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p19(X1)
& ~ p18(X1) )
| ( ~ p19(X1)
& p18(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p18(X2)
& ~ p17(X2) )
| ( ~ p18(X2)
& p17(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p17(X1)
& ~ p16(X1) )
| ( ~ p17(X1)
& p16(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p16(X2)
& ~ p15(X2) )
| ( ~ p16(X2)
& p15(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p15(X1)
& ~ p14(X1) )
| ( ~ p15(X1)
& p14(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p14(X2)
& ~ p13(X2) )
| ( ~ p14(X2)
& p13(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p13(X1)
& ~ p12(X1) )
| ( ~ p13(X1)
& p12(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p12(X2)
& ~ p11(X2) )
| ( ~ p12(X2)
& p11(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p11(X1)
& ~ p10(X1) )
| ( ~ p11(X1)
& p10(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p10(X2)
& ~ p9(X2) )
| ( ~ p10(X2)
& p9(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p9(X1)
& ~ p8(X1) )
| ( ~ p9(X1)
& p8(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p8(X2)
& ~ p7(X2) )
| ( ~ p8(X2)
& p7(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p7(X1)
& ~ p6(X1) )
| ( ~ p7(X1)
& p6(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p6(X2)
& ~ p5(X2) )
| ( ~ p6(X2)
& p5(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p5(X1)
& ~ p4(X1) )
| ( ~ p5(X1)
& p4(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p4(X2)
& ~ p3(X2) )
| ( ~ p4(X2)
& p3(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p3(X1)
& ~ p2(X1) )
| ( ~ p3(X1)
& p2(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p2(X2)
& ~ p1(X2) )
| ( ~ p2(X2)
& p1(X2) ) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p45(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| ( ~ p43(X2)
& ~ p44(X2) )
| ( p44(X2)
& p43(X2) )
| ( ~ p42(X2)
& ~ p43(X2) )
| ( p43(X2)
& p42(X2) )
| ( ~ p41(X2)
& ~ p42(X2) )
| ( p42(X2)
& p41(X2) )
| ( ~ p40(X2)
& ~ p41(X2) )
| ( p41(X2)
& p40(X2) )
| ( ~ p39(X2)
& ~ p40(X2) )
| ( p40(X2)
& p39(X2) )
| ( ~ p38(X2)
& ~ p39(X2) )
| ( p39(X2)
& p38(X2) )
| ( ~ p37(X2)
& ~ p38(X2) )
| ( p38(X2)
& p37(X2) )
| ( ~ p36(X2)
& ~ p37(X2) )
| ( p37(X2)
& p36(X2) )
| ( ~ p35(X2)
& ~ p36(X2) )
| ( p36(X2)
& p35(X2) )
| ( ~ p34(X2)
& ~ p35(X2) )
| ( p35(X2)
& p34(X2) )
| ( ~ p33(X2)
& ~ p34(X2) )
| ( p34(X2)
& p33(X2) )
| ( ~ p32(X2)
& ~ p33(X2) )
| ( p33(X2)
& p32(X2) )
| ( ~ p31(X2)
& ~ p32(X2) )
| ( p32(X2)
& p31(X2) )
| ( ~ p30(X2)
& ~ p31(X2) )
| ( p31(X2)
& p30(X2) )
| ( ~ p29(X2)
& ~ p30(X2) )
| ( p30(X2)
& p29(X2) )
| ( ~ p28(X2)
& ~ p29(X2) )
| ( p29(X2)
& p28(X2) )
| ( ~ p27(X2)
& ~ p28(X2) )
| ( p28(X2)
& p27(X2) )
| ( ~ p26(X2)
& ~ p27(X2) )
| ( p27(X2)
& p26(X2) )
| ( ~ p25(X2)
& ~ p26(X2) )
| ( p26(X2)
& p25(X2) )
| ( ~ p24(X2)
& ~ p25(X2) )
| ( p25(X2)
& p24(X2) )
| ( ~ p23(X2)
& ~ p24(X2) )
| ( p24(X2)
& p23(X2) )
| ( ~ p22(X2)
& ~ p23(X2) )
| ( p23(X2)
& p22(X2) )
| ( ~ p21(X2)
& ~ p22(X2) )
| ( p22(X2)
& p21(X2) )
| ( ~ p20(X2)
& ~ p21(X2) )
| ( p21(X2)
& p20(X2) )
| ( ~ p19(X2)
& ~ p20(X2) )
| ( p20(X2)
& p19(X2) )
| ( ~ p18(X2)
& ~ p19(X2) )
| ( p19(X2)
& p18(X2) )
| ( ~ p17(X2)
& ~ p18(X2) )
| ( p18(X2)
& p17(X2) )
| ( ~ p16(X2)
& ~ p17(X2) )
| ( p17(X2)
& p16(X2) )
| ( ~ p15(X2)
& ~ p16(X2) )
| ( p16(X2)
& p15(X2) )
| ( ~ p14(X2)
& ~ p15(X2) )
| ( p15(X2)
& p14(X2) )
| ( ~ p13(X2)
& ~ p14(X2) )
| ( p14(X2)
& p13(X2) )
| ( ~ p12(X2)
& ~ p13(X2) )
| ( p13(X2)
& p12(X2) )
| ( ~ p11(X2)
& ~ p12(X2) )
| ( p12(X2)
& p11(X2) )
| ( ~ p10(X2)
& ~ p11(X2) )
| ( p11(X2)
& p10(X2) )
| ( ~ p9(X2)
& ~ p10(X2) )
| ( p10(X2)
& p9(X2) )
| ( ~ p8(X2)
& ~ p9(X2) )
| ( p9(X2)
& p8(X2) )
| ( ~ p7(X2)
& ~ p8(X2) )
| ( p8(X2)
& p7(X2) )
| ( ~ p6(X2)
& ~ p7(X2) )
| ( p7(X2)
& p6(X2) )
| ( ~ p5(X2)
& ~ p6(X2) )
| ( p6(X2)
& p5(X2) )
| ( ~ p4(X2)
& ~ p5(X2) )
| ( p5(X2)
& p4(X2) )
| ( ~ p3(X2)
& ~ p4(X2) )
| ( p4(X2)
& p3(X2) )
| ( ~ p2(X2)
& ~ p3(X2) )
| ( p3(X2)
& p2(X2) )
| ( ~ p1(X2)
& ~ p2(X2) )
| ( p2(X2)
& p1(X2) ) ) ) ) ) ),
inference(negating_conjecture,[status(cth)],[main]) ).
% FOF SIMPLE INFERENCE
fof(main_nc_elimTB,negated_conjecture,
? [X1] :
~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ p45(X2)
| ! [X3] :
( ~ r1(X2,X3)
| ~ p1(X3) ) )
| ! [X4] :
( ~ r1(X1,X4)
| ~ ! [X5] :
( ~ r1(X4,X5)
| ~ ( ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| ! [X16] :
( ~ r1(X15,X16)
| ! [X17] :
( ~ r1(X16,X17)
| ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| ! [X32] :
( ~ r1(X31,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| ! [X48] : ~ r1(X47,X48)
| ~ ! [X49] :
( ~ r1(X47,X49)
| ~ ( ( p44(X49)
& ~ p43(X49) )
| ( ~ p44(X49)
& p43(X49) ) ) ) )
| ~ ! [X50] :
( ~ r1(X46,X50)
| ~ ( ( p43(X50)
& ~ p42(X50) )
| ( ~ p43(X50)
& p42(X50) ) ) ) )
| ~ ! [X51] :
( ~ r1(X45,X51)
| ~ ( ( p42(X51)
& ~ p41(X51) )
| ( ~ p42(X51)
& p41(X51) ) ) ) )
| ~ ! [X52] :
( ~ r1(X44,X52)
| ~ ( ( p41(X52)
& ~ p40(X52) )
| ( ~ p41(X52)
& p40(X52) ) ) ) )
| ~ ! [X53] :
( ~ r1(X43,X53)
| ~ ( ( p40(X53)
& ~ p39(X53) )
| ( ~ p40(X53)
& p39(X53) ) ) ) )
| ~ ! [X54] :
( ~ r1(X42,X54)
| ~ ( ( p39(X54)
& ~ p38(X54) )
| ( ~ p39(X54)
& p38(X54) ) ) ) )
| ~ ! [X55] :
( ~ r1(X41,X55)
| ~ ( ( p38(X55)
& ~ p37(X55) )
| ( ~ p38(X55)
& p37(X55) ) ) ) )
| ~ ! [X56] :
( ~ r1(X40,X56)
| ~ ( ( p37(X56)
& ~ p36(X56) )
| ( ~ p37(X56)
& p36(X56) ) ) ) )
| ~ ! [X57] :
( ~ r1(X39,X57)
| ~ ( ( p36(X57)
& ~ p35(X57) )
| ( ~ p36(X57)
& p35(X57) ) ) ) )
| ~ ! [X58] :
( ~ r1(X38,X58)
| ~ ( ( p35(X58)
& ~ p34(X58) )
| ( ~ p35(X58)
& p34(X58) ) ) ) )
| ~ ! [X59] :
( ~ r1(X37,X59)
| ~ ( ( p34(X59)
& ~ p33(X59) )
| ( ~ p34(X59)
& p33(X59) ) ) ) )
| ~ ! [X60] :
( ~ r1(X36,X60)
| ~ ( ( p33(X60)
& ~ p32(X60) )
| ( ~ p33(X60)
& p32(X60) ) ) ) )
| ~ ! [X61] :
( ~ r1(X35,X61)
| ~ ( ( p32(X61)
& ~ p31(X61) )
| ( ~ p32(X61)
& p31(X61) ) ) ) )
| ~ ! [X62] :
( ~ r1(X34,X62)
| ~ ( ( p31(X62)
& ~ p30(X62) )
| ( ~ p31(X62)
& p30(X62) ) ) ) )
| ~ ! [X63] :
( ~ r1(X33,X63)
| ~ ( ( p30(X63)
& ~ p29(X63) )
| ( ~ p30(X63)
& p29(X63) ) ) ) )
| ~ ! [X64] :
( ~ r1(X32,X64)
| ~ ( ( p29(X64)
& ~ p28(X64) )
| ( ~ p29(X64)
& p28(X64) ) ) ) )
| ~ ! [X65] :
( ~ r1(X31,X65)
| ~ ( ( p28(X65)
& ~ p27(X65) )
| ( ~ p28(X65)
& p27(X65) ) ) ) )
| ~ ! [X66] :
( ~ r1(X30,X66)
| ~ ( ( p27(X66)
& ~ p26(X66) )
| ( ~ p27(X66)
& p26(X66) ) ) ) )
| ~ ! [X67] :
( ~ r1(X29,X67)
| ~ ( ( p26(X67)
& ~ p25(X67) )
| ( ~ p26(X67)
& p25(X67) ) ) ) )
| ~ ! [X68] :
( ~ r1(X28,X68)
| ~ ( ( p25(X68)
& ~ p24(X68) )
| ( ~ p25(X68)
& p24(X68) ) ) ) )
| ~ ! [X69] :
( ~ r1(X27,X69)
| ~ ( ( p24(X69)
& ~ p23(X69) )
| ( ~ p24(X69)
& p23(X69) ) ) ) )
| ~ ! [X70] :
( ~ r1(X26,X70)
| ~ ( ( p23(X70)
& ~ p22(X70) )
| ( ~ p23(X70)
& p22(X70) ) ) ) )
| ~ ! [X71] :
( ~ r1(X25,X71)
| ~ ( ( p22(X71)
& ~ p21(X71) )
| ( ~ p22(X71)
& p21(X71) ) ) ) )
| ~ ! [X72] :
( ~ r1(X24,X72)
| ~ ( ( p21(X72)
& ~ p20(X72) )
| ( ~ p21(X72)
& p20(X72) ) ) ) )
| ~ ! [X73] :
( ~ r1(X23,X73)
| ~ ( ( p20(X73)
& ~ p19(X73) )
| ( ~ p20(X73)
& p19(X73) ) ) ) )
| ~ ! [X74] :
( ~ r1(X22,X74)
| ~ ( ( p19(X74)
& ~ p18(X74) )
| ( ~ p19(X74)
& p18(X74) ) ) ) )
| ~ ! [X75] :
( ~ r1(X21,X75)
| ~ ( ( p18(X75)
& ~ p17(X75) )
| ( ~ p18(X75)
& p17(X75) ) ) ) )
| ~ ! [X76] :
( ~ r1(X20,X76)
| ~ ( ( p17(X76)
& ~ p16(X76) )
| ( ~ p17(X76)
& p16(X76) ) ) ) )
| ~ ! [X77] :
( ~ r1(X19,X77)
| ~ ( ( p16(X77)
& ~ p15(X77) )
| ( ~ p16(X77)
& p15(X77) ) ) ) )
| ~ ! [X78] :
( ~ r1(X18,X78)
| ~ ( ( p15(X78)
& ~ p14(X78) )
| ( ~ p15(X78)
& p14(X78) ) ) ) )
| ~ ! [X79] :
( ~ r1(X17,X79)
| ~ ( ( p14(X79)
& ~ p13(X79) )
| ( ~ p14(X79)
& p13(X79) ) ) ) )
| ~ ! [X80] :
( ~ r1(X16,X80)
| ~ ( ( p13(X80)
& ~ p12(X80) )
| ( ~ p13(X80)
& p12(X80) ) ) ) )
| ~ ! [X81] :
( ~ r1(X15,X81)
| ~ ( ( p12(X81)
& ~ p11(X81) )
| ( ~ p12(X81)
& p11(X81) ) ) ) )
| ~ ! [X82] :
( ~ r1(X14,X82)
| ~ ( ( p11(X82)
& ~ p10(X82) )
| ( ~ p11(X82)
& p10(X82) ) ) ) )
| ~ ! [X83] :
( ~ r1(X13,X83)
| ~ ( ( p10(X83)
& ~ p9(X83) )
| ( ~ p10(X83)
& p9(X83) ) ) ) )
| ~ ! [X84] :
( ~ r1(X12,X84)
| ~ ( ( p9(X84)
& ~ p8(X84) )
| ( ~ p9(X84)
& p8(X84) ) ) ) )
| ~ ! [X85] :
( ~ r1(X11,X85)
| ~ ( ( p8(X85)
& ~ p7(X85) )
| ( ~ p8(X85)
& p7(X85) ) ) ) )
| ~ ! [X86] :
( ~ r1(X10,X86)
| ~ ( ( p7(X86)
& ~ p6(X86) )
| ( ~ p7(X86)
& p6(X86) ) ) ) )
| ~ ! [X87] :
( ~ r1(X9,X87)
| ~ ( ( p6(X87)
& ~ p5(X87) )
| ( ~ p6(X87)
& p5(X87) ) ) ) )
| ~ ! [X88] :
( ~ r1(X8,X88)
| ~ ( ( p5(X88)
& ~ p4(X88) )
| ( ~ p5(X88)
& p4(X88) ) ) ) )
| ~ ! [X89] :
( ~ r1(X7,X89)
| ~ ( ( p4(X89)
& ~ p3(X89) )
| ( ~ p4(X89)
& p3(X89) ) ) ) )
| ~ ! [X90] :
( ~ r1(X6,X90)
| ~ ( ( p3(X90)
& ~ p2(X90) )
| ( ~ p3(X90)
& p2(X90) ) ) ) )
| ~ ! [X91] :
( ~ r1(X5,X91)
| ~ ( ( p2(X91)
& ~ p1(X91) )
| ( ~ p2(X91)
& p1(X91) ) ) )
| ! [X92] :
( ~ r1(X5,X92)
| p45(X92) )
| ! [X93] :
( ~ r1(X5,X93)
| ( ~ p43(X93)
& ~ p44(X93) )
| ( p44(X93)
& p43(X93) )
| ( ~ p42(X93)
& ~ p43(X93) )
| ( p43(X93)
& p42(X93) )
| ( ~ p41(X93)
& ~ p42(X93) )
| ( p42(X93)
& p41(X93) )
| ( ~ p40(X93)
& ~ p41(X93) )
| ( p41(X93)
& p40(X93) )
| ( ~ p39(X93)
& ~ p40(X93) )
| ( p40(X93)
& p39(X93) )
| ( ~ p38(X93)
& ~ p39(X93) )
| ( p39(X93)
& p38(X93) )
| ( ~ p37(X93)
& ~ p38(X93) )
| ( p38(X93)
& p37(X93) )
| ( ~ p36(X93)
& ~ p37(X93) )
| ( p37(X93)
& p36(X93) )
| ( ~ p35(X93)
& ~ p36(X93) )
| ( p36(X93)
& p35(X93) )
| ( ~ p34(X93)
& ~ p35(X93) )
| ( p35(X93)
& p34(X93) )
| ( ~ p33(X93)
& ~ p34(X93) )
| ( p34(X93)
& p33(X93) )
| ( ~ p32(X93)
& ~ p33(X93) )
| ( p33(X93)
& p32(X93) )
| ( ~ p31(X93)
& ~ p32(X93) )
| ( p32(X93)
& p31(X93) )
| ( ~ p30(X93)
& ~ p31(X93) )
| ( p31(X93)
& p30(X93) )
| ( ~ p29(X93)
& ~ p30(X93) )
| ( p30(X93)
& p29(X93) )
| ( ~ p28(X93)
& ~ p29(X93) )
| ( p29(X93)
& p28(X93) )
| ( ~ p27(X93)
& ~ p28(X93) )
| ( p28(X93)
& p27(X93) )
| ( ~ p26(X93)
& ~ p27(X93) )
| ( p27(X93)
& p26(X93) )
| ( ~ p25(X93)
& ~ p26(X93) )
| ( p26(X93)
& p25(X93) )
| ( ~ p24(X93)
& ~ p25(X93) )
| ( p25(X93)
& p24(X93) )
| ( ~ p23(X93)
& ~ p24(X93) )
| ( p24(X93)
& p23(X93) )
| ( ~ p22(X93)
& ~ p23(X93) )
| ( p23(X93)
& p22(X93) )
| ( ~ p21(X93)
& ~ p22(X93) )
| ( p22(X93)
& p21(X93) )
| ( ~ p20(X93)
& ~ p21(X93) )
| ( p21(X93)
& p20(X93) )
| ( ~ p19(X93)
& ~ p20(X93) )
| ( p20(X93)
& p19(X93) )
| ( ~ p18(X93)
& ~ p19(X93) )
| ( p19(X93)
& p18(X93) )
| ( ~ p17(X93)
& ~ p18(X93) )
| ( p18(X93)
& p17(X93) )
| ( ~ p16(X93)
& ~ p17(X93) )
| ( p17(X93)
& p16(X93) )
| ( ~ p15(X93)
& ~ p16(X93) )
| ( p16(X93)
& p15(X93) )
| ( ~ p14(X93)
& ~ p15(X93) )
| ( p15(X93)
& p14(X93) )
| ( ~ p13(X93)
& ~ p14(X93) )
| ( p14(X93)
& p13(X93) )
| ( ~ p12(X93)
& ~ p13(X93) )
| ( p13(X93)
& p12(X93) )
| ( ~ p11(X93)
& ~ p12(X93) )
| ( p12(X93)
& p11(X93) )
| ( ~ p10(X93)
& ~ p11(X93) )
| ( p11(X93)
& p10(X93) )
| ( ~ p9(X93)
& ~ p10(X93) )
| ( p10(X93)
& p9(X93) )
| ( ~ p8(X93)
& ~ p9(X93) )
| ( p9(X93)
& p8(X93) )
| ( ~ p7(X93)
& ~ p8(X93) )
| ( p8(X93)
& p7(X93) )
| ( ~ p6(X93)
& ~ p7(X93) )
| ( p7(X93)
& p6(X93) )
| ( ~ p5(X93)
& ~ p6(X93) )
| ( p6(X93)
& p5(X93) )
| ( ~ p4(X93)
& ~ p5(X93) )
| ( p5(X93)
& p4(X93) )
| ( ~ p3(X93)
& ~ p4(X93) )
| ( p4(X93)
& p3(X93) )
| ( ~ p2(X93)
& ~ p3(X93) )
| ( p3(X93)
& p2(X93) )
| ( ~ p1(X93)
& ~ p2(X93) )
| ( p2(X93)
& p1(X93) ) ) ) ) ) ),
inference(elimTB,[status(thm)],[inference(variable_rename,[status(thm)],[main_nc])]) ).
% FOF INTRODUCE RENAMING
fof(ren43_defn,definition,
! [X91] :
( ren43(X91)
<= ( ( p2(X91)
& ~ p1(X91) )
| ( ~ p2(X91)
& p1(X91) ) ) ),
introduced(definition,[new_symbols(definition,[ren43])],[main_nc_elimTB]) ).
% FOF SIMPLE INFERENCE
fof(ren43_elimImpEquivPushNegMiniScope,plain,
! [X1] :
( ( ( ~ p2(X1)
| p1(X1) )
& ( p2(X1)
| ~ p1(X1) ) )
| ren43(X1) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[ren43_defn]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_87,plain,
( ~ p2(X0)
| p1(X0)
| ren43(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren43_elimImpEquivPushNegMiniScope])]) ).
% FILE RECORD
fof(reflexivity,axiom,
! [X1] : r1(X1,X1),
file('theBenchmark.p',reflexivity) ).
% FOF SIMPLE INFERENCE
fof(reflexivity_elimTB,axiom,
! [X1] : r1(X1,X1),
inference(elimTB,[status(thm)],[inference(variable_rename,[status(thm)],[reflexivity])]) ).
% FOF SIMPLE INFERENCE
fof(reflexivity_elimImpEquivPushNegMiniScope,axiom,
! [X1] : r1(X1,X1),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[reflexivity_elimTB]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_1,plain,
r1(X0,X0),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[reflexivity_elimImpEquivPushNegMiniScope])]) ).
% FOF INTRODUCE RENAMING
fof(ren44_defn,definition,
! [X5] :
( ren44(X5)
<= ( ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| ! [X16] :
( ~ r1(X15,X16)
| ! [X17] :
( ~ r1(X16,X17)
| ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| ! [X32] :
( ~ r1(X31,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| ! [X48] : ~ r1(X47,X48)
| ~ ! [X49] :
( ~ r1(X47,X49)
| ~ ren1(X49) ) )
| ~ ! [X50] :
( ~ r1(X46,X50)
| ~ ren2(X50) ) )
| ~ ! [X51] :
( ~ r1(X45,X51)
| ~ ren3(X51) ) )
| ~ ! [X52] :
( ~ r1(X44,X52)
| ~ ren4(X52) ) )
| ~ ! [X53] :
( ~ r1(X43,X53)
| ~ ren5(X53) ) )
| ~ ! [X54] :
( ~ r1(X42,X54)
| ~ ren6(X54) ) )
| ~ ! [X55] :
( ~ r1(X41,X55)
| ~ ren7(X55) ) )
| ~ ! [X56] :
( ~ r1(X40,X56)
| ~ ren8(X56) ) )
| ~ ! [X57] :
( ~ r1(X39,X57)
| ~ ren9(X57) ) )
| ~ ! [X58] :
( ~ r1(X38,X58)
| ~ ren10(X58) ) )
| ~ ! [X59] :
( ~ r1(X37,X59)
| ~ ren11(X59) ) )
| ~ ! [X60] :
( ~ r1(X36,X60)
| ~ ren12(X60) ) )
| ~ ! [X61] :
( ~ r1(X35,X61)
| ~ ren13(X61) ) )
| ~ ! [X62] :
( ~ r1(X34,X62)
| ~ ren14(X62) ) )
| ~ ! [X63] :
( ~ r1(X33,X63)
| ~ ren15(X63) ) )
| ~ ! [X64] :
( ~ r1(X32,X64)
| ~ ren16(X64) ) )
| ~ ! [X65] :
( ~ r1(X31,X65)
| ~ ren17(X65) ) )
| ~ ! [X66] :
( ~ r1(X30,X66)
| ~ ren18(X66) ) )
| ~ ! [X67] :
( ~ r1(X29,X67)
| ~ ren19(X67) ) )
| ~ ! [X68] :
( ~ r1(X28,X68)
| ~ ren20(X68) ) )
| ~ ! [X69] :
( ~ r1(X27,X69)
| ~ ren21(X69) ) )
| ~ ! [X70] :
( ~ r1(X26,X70)
| ~ ren22(X70) ) )
| ~ ! [X71] :
( ~ r1(X25,X71)
| ~ ren23(X71) ) )
| ~ ! [X72] :
( ~ r1(X24,X72)
| ~ ren24(X72) ) )
| ~ ! [X73] :
( ~ r1(X23,X73)
| ~ ren25(X73) ) )
| ~ ! [X74] :
( ~ r1(X22,X74)
| ~ ren26(X74) ) )
| ~ ! [X75] :
( ~ r1(X21,X75)
| ~ ren27(X75) ) )
| ~ ! [X76] :
( ~ r1(X20,X76)
| ~ ren28(X76) ) )
| ~ ! [X77] :
( ~ r1(X19,X77)
| ~ ren29(X77) ) )
| ~ ! [X78] :
( ~ r1(X18,X78)
| ~ ren30(X78) ) )
| ~ ! [X79] :
( ~ r1(X17,X79)
| ~ ren31(X79) ) )
| ~ ! [X80] :
( ~ r1(X16,X80)
| ~ ren32(X80) ) )
| ~ ! [X81] :
( ~ r1(X15,X81)
| ~ ren33(X81) ) )
| ~ ! [X82] :
( ~ r1(X14,X82)
| ~ ren34(X82) ) )
| ~ ! [X83] :
( ~ r1(X13,X83)
| ~ ren35(X83) ) )
| ~ ! [X84] :
( ~ r1(X12,X84)
| ~ ren36(X84) ) )
| ~ ! [X85] :
( ~ r1(X11,X85)
| ~ ren37(X85) ) )
| ~ ! [X86] :
( ~ r1(X10,X86)
| ~ ren38(X86) ) )
| ~ ! [X87] :
( ~ r1(X9,X87)
| ~ ren39(X87) ) )
| ~ ! [X88] :
( ~ r1(X8,X88)
| ~ ren40(X88) ) )
| ~ ! [X89] :
( ~ r1(X7,X89)
| ~ ren41(X89) ) )
| ~ ! [X90] :
( ~ r1(X6,X90)
| ~ ren42(X90) ) )
| ~ ! [X91] :
( ~ r1(X5,X91)
| ~ ren43(X91) )
| ! [X92] :
( ~ r1(X5,X92)
| p45(X92) )
| ! [X93] :
( ~ r1(X5,X93)
| ( ~ p43(X93)
& ~ p44(X93) )
| ( p44(X93)
& p43(X93) )
| ( ~ p42(X93)
& ~ p43(X93) )
| ( p43(X93)
& p42(X93) )
| ( ~ p41(X93)
& ~ p42(X93) )
| ( p42(X93)
& p41(X93) )
| ( ~ p40(X93)
& ~ p41(X93) )
| ( p41(X93)
& p40(X93) )
| ( ~ p39(X93)
& ~ p40(X93) )
| ( p40(X93)
& p39(X93) )
| ( ~ p38(X93)
& ~ p39(X93) )
| ( p39(X93)
& p38(X93) )
| ( ~ p37(X93)
& ~ p38(X93) )
| ( p38(X93)
& p37(X93) )
| ( ~ p36(X93)
& ~ p37(X93) )
| ( p37(X93)
& p36(X93) )
| ( ~ p35(X93)
& ~ p36(X93) )
| ( p36(X93)
& p35(X93) )
| ( ~ p34(X93)
& ~ p35(X93) )
| ( p35(X93)
& p34(X93) )
| ( ~ p33(X93)
& ~ p34(X93) )
| ( p34(X93)
& p33(X93) )
| ( ~ p32(X93)
& ~ p33(X93) )
| ( p33(X93)
& p32(X93) )
| ( ~ p31(X93)
& ~ p32(X93) )
| ( p32(X93)
& p31(X93) )
| ( ~ p30(X93)
& ~ p31(X93) )
| ( p31(X93)
& p30(X93) )
| ( ~ p29(X93)
& ~ p30(X93) )
| ( p30(X93)
& p29(X93) )
| ( ~ p28(X93)
& ~ p29(X93) )
| ( p29(X93)
& p28(X93) )
| ( ~ p27(X93)
& ~ p28(X93) )
| ( p28(X93)
& p27(X93) )
| ( ~ p26(X93)
& ~ p27(X93) )
| ( p27(X93)
& p26(X93) )
| ( ~ p25(X93)
& ~ p26(X93) )
| ( p26(X93)
& p25(X93) )
| ( ~ p24(X93)
& ~ p25(X93) )
| ( p25(X93)
& p24(X93) )
| ( ~ p23(X93)
& ~ p24(X93) )
| ( p24(X93)
& p23(X93) )
| ( ~ p22(X93)
& ~ p23(X93) )
| ( p23(X93)
& p22(X93) )
| ( ~ p21(X93)
& ~ p22(X93) )
| ( p22(X93)
& p21(X93) )
| ( ~ p20(X93)
& ~ p21(X93) )
| ( p21(X93)
& p20(X93) )
| ( ~ p19(X93)
& ~ p20(X93) )
| ( p20(X93)
& p19(X93) )
| ( ~ p18(X93)
& ~ p19(X93) )
| ( p19(X93)
& p18(X93) )
| ( ~ p17(X93)
& ~ p18(X93) )
| ( p18(X93)
& p17(X93) )
| ( ~ p16(X93)
& ~ p17(X93) )
| ( p17(X93)
& p16(X93) )
| ( ~ p15(X93)
& ~ p16(X93) )
| ( p16(X93)
& p15(X93) )
| ( ~ p14(X93)
& ~ p15(X93) )
| ( p15(X93)
& p14(X93) )
| ( ~ p13(X93)
& ~ p14(X93) )
| ( p14(X93)
& p13(X93) )
| ( ~ p12(X93)
& ~ p13(X93) )
| ( p13(X93)
& p12(X93) )
| ( ~ p11(X93)
& ~ p12(X93) )
| ( p12(X93)
& p11(X93) )
| ( ~ p10(X93)
& ~ p11(X93) )
| ( p11(X93)
& p10(X93) )
| ( ~ p9(X93)
& ~ p10(X93) )
| ( p10(X93)
& p9(X93) )
| ( ~ p8(X93)
& ~ p9(X93) )
| ( p9(X93)
& p8(X93) )
| ( ~ p7(X93)
& ~ p8(X93) )
| ( p8(X93)
& p7(X93) )
| ( ~ p6(X93)
& ~ p7(X93) )
| ( p7(X93)
& p6(X93) )
| ( ~ p5(X93)
& ~ p6(X93) )
| ( p6(X93)
& p5(X93) )
| ( ~ p4(X93)
& ~ p5(X93) )
| ( p5(X93)
& p4(X93) )
| ( ~ p3(X93)
& ~ p4(X93) )
| ( p4(X93)
& p3(X93) )
| ( ~ p2(X93)
& ~ p3(X93) )
| ( p3(X93)
& p2(X93) )
| ( ~ p1(X93)
& ~ p2(X93) )
| ( p2(X93)
& p1(X93) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren44])],[main_nc_elimTB]) ).
% FOF SIMPLE INFERENCE
fof(ren44_elimImpEquivPushNegMiniScope,plain,
! [X1] :
( ( ? [X2] :
( r1(X1,X2)
& ? [X3] :
( r1(X2,X3)
& ? [X4] :
( r1(X3,X4)
& ? [X5] :
( r1(X4,X5)
& ? [X6] :
( r1(X5,X6)
& ? [X7] :
( r1(X6,X7)
& ? [X8] :
( r1(X7,X8)
& ? [X9] :
( r1(X8,X9)
& ? [X10] :
( r1(X9,X10)
& ? [X11] :
( r1(X10,X11)
& ? [X12] :
( r1(X11,X12)
& ? [X13] :
( r1(X12,X13)
& ? [X14] :
( r1(X13,X14)
& ? [X15] :
( r1(X14,X15)
& ? [X16] :
( r1(X15,X16)
& ? [X17] :
( r1(X16,X17)
& ? [X18] :
( r1(X17,X18)
& ? [X19] :
( r1(X18,X19)
& ? [X20] :
( r1(X19,X20)
& ? [X21] :
( r1(X20,X21)
& ? [X22] :
( r1(X21,X22)
& ? [X23] :
( r1(X22,X23)
& ? [X24] :
( r1(X23,X24)
& ? [X25] :
( r1(X24,X25)
& ? [X26] :
( r1(X25,X26)
& ? [X27] :
( r1(X26,X27)
& ? [X28] :
( r1(X27,X28)
& ? [X29] :
( r1(X28,X29)
& ? [X30] :
( r1(X29,X30)
& ? [X31] :
( r1(X30,X31)
& ? [X32] :
( r1(X31,X32)
& ? [X33] :
( r1(X32,X33)
& ? [X34] :
( r1(X33,X34)
& ? [X35] :
( r1(X34,X35)
& ? [X36] :
( r1(X35,X36)
& ? [X37] :
( r1(X36,X37)
& ? [X38] :
( r1(X37,X38)
& ? [X39] :
( r1(X38,X39)
& ? [X40] :
( r1(X39,X40)
& ? [X41] :
( r1(X40,X41)
& ? [X42] :
( r1(X41,X42)
& ? [X43] :
( r1(X42,X43)
& ? [X44] : r1(X43,X44)
& ! [X45] :
( ~ r1(X43,X45)
| ~ ren1(X45) ) )
& ! [X46] :
( ~ r1(X42,X46)
| ~ ren2(X46) ) )
& ! [X47] :
( ~ r1(X41,X47)
| ~ ren3(X47) ) )
& ! [X48] :
( ~ r1(X40,X48)
| ~ ren4(X48) ) )
& ! [X49] :
( ~ r1(X39,X49)
| ~ ren5(X49) ) )
& ! [X50] :
( ~ r1(X38,X50)
| ~ ren6(X50) ) )
& ! [X51] :
( ~ r1(X37,X51)
| ~ ren7(X51) ) )
& ! [X52] :
( ~ r1(X36,X52)
| ~ ren8(X52) ) )
& ! [X53] :
( ~ r1(X35,X53)
| ~ ren9(X53) ) )
& ! [X54] :
( ~ r1(X34,X54)
| ~ ren10(X54) ) )
& ! [X55] :
( ~ r1(X33,X55)
| ~ ren11(X55) ) )
& ! [X56] :
( ~ r1(X32,X56)
| ~ ren12(X56) ) )
& ! [X57] :
( ~ r1(X31,X57)
| ~ ren13(X57) ) )
& ! [X58] :
( ~ r1(X30,X58)
| ~ ren14(X58) ) )
& ! [X59] :
( ~ r1(X29,X59)
| ~ ren15(X59) ) )
& ! [X60] :
( ~ r1(X28,X60)
| ~ ren16(X60) ) )
& ! [X61] :
( ~ r1(X27,X61)
| ~ ren17(X61) ) )
& ! [X62] :
( ~ r1(X26,X62)
| ~ ren18(X62) ) )
& ! [X63] :
( ~ r1(X25,X63)
| ~ ren19(X63) ) )
& ! [X64] :
( ~ r1(X24,X64)
| ~ ren20(X64) ) )
& ! [X65] :
( ~ r1(X23,X65)
| ~ ren21(X65) ) )
& ! [X66] :
( ~ r1(X22,X66)
| ~ ren22(X66) ) )
& ! [X67] :
( ~ r1(X21,X67)
| ~ ren23(X67) ) )
& ! [X68] :
( ~ r1(X20,X68)
| ~ ren24(X68) ) )
& ! [X69] :
( ~ r1(X19,X69)
| ~ ren25(X69) ) )
& ! [X70] :
( ~ r1(X18,X70)
| ~ ren26(X70) ) )
& ! [X71] :
( ~ r1(X17,X71)
| ~ ren27(X71) ) )
& ! [X72] :
( ~ r1(X16,X72)
| ~ ren28(X72) ) )
& ! [X73] :
( ~ r1(X15,X73)
| ~ ren29(X73) ) )
& ! [X74] :
( ~ r1(X14,X74)
| ~ ren30(X74) ) )
& ! [X75] :
( ~ r1(X13,X75)
| ~ ren31(X75) ) )
& ! [X76] :
( ~ r1(X12,X76)
| ~ ren32(X76) ) )
& ! [X77] :
( ~ r1(X11,X77)
| ~ ren33(X77) ) )
& ! [X78] :
( ~ r1(X10,X78)
| ~ ren34(X78) ) )
& ! [X79] :
( ~ r1(X9,X79)
| ~ ren35(X79) ) )
& ! [X80] :
( ~ r1(X8,X80)
| ~ ren36(X80) ) )
& ! [X81] :
( ~ r1(X7,X81)
| ~ ren37(X81) ) )
& ! [X82] :
( ~ r1(X6,X82)
| ~ ren38(X82) ) )
& ! [X83] :
( ~ r1(X5,X83)
| ~ ren39(X83) ) )
& ! [X84] :
( ~ r1(X4,X84)
| ~ ren40(X84) ) )
& ! [X85] :
( ~ r1(X3,X85)
| ~ ren41(X85) ) )
& ! [X86] :
( ~ r1(X2,X86)
| ~ ren42(X86) ) )
& ! [X87] :
( ~ r1(X1,X87)
| ~ ren43(X87) )
& ? [X88] :
( r1(X1,X88)
& ~ p45(X88) )
& ? [X89] :
( r1(X1,X89)
& ( p43(X89)
| p44(X89) )
& ( ~ p44(X89)
| ~ p43(X89) )
& ( p42(X89)
| p43(X89) )
& ( ~ p43(X89)
| ~ p42(X89) )
& ( p41(X89)
| p42(X89) )
& ( ~ p42(X89)
| ~ p41(X89) )
& ( p40(X89)
| p41(X89) )
& ( ~ p41(X89)
| ~ p40(X89) )
& ( p39(X89)
| p40(X89) )
& ( ~ p40(X89)
| ~ p39(X89) )
& ( p38(X89)
| p39(X89) )
& ( ~ p39(X89)
| ~ p38(X89) )
& ( p37(X89)
| p38(X89) )
& ( ~ p38(X89)
| ~ p37(X89) )
& ( p36(X89)
| p37(X89) )
& ( ~ p37(X89)
| ~ p36(X89) )
& ( p35(X89)
| p36(X89) )
& ( ~ p36(X89)
| ~ p35(X89) )
& ( p34(X89)
| p35(X89) )
& ( ~ p35(X89)
| ~ p34(X89) )
& ( p33(X89)
| p34(X89) )
& ( ~ p34(X89)
| ~ p33(X89) )
& ( p32(X89)
| p33(X89) )
& ( ~ p33(X89)
| ~ p32(X89) )
& ( p31(X89)
| p32(X89) )
& ( ~ p32(X89)
| ~ p31(X89) )
& ( p30(X89)
| p31(X89) )
& ( ~ p31(X89)
| ~ p30(X89) )
& ( p29(X89)
| p30(X89) )
& ( ~ p30(X89)
| ~ p29(X89) )
& ( p28(X89)
| p29(X89) )
& ( ~ p29(X89)
| ~ p28(X89) )
& ( p27(X89)
| p28(X89) )
& ( ~ p28(X89)
| ~ p27(X89) )
& ( p26(X89)
| p27(X89) )
& ( ~ p27(X89)
| ~ p26(X89) )
& ( p25(X89)
| p26(X89) )
& ( ~ p26(X89)
| ~ p25(X89) )
& ( p24(X89)
| p25(X89) )
& ( ~ p25(X89)
| ~ p24(X89) )
& ( p23(X89)
| p24(X89) )
& ( ~ p24(X89)
| ~ p23(X89) )
& ( p22(X89)
| p23(X89) )
& ( ~ p23(X89)
| ~ p22(X89) )
& ( p21(X89)
| p22(X89) )
& ( ~ p22(X89)
| ~ p21(X89) )
& ( p20(X89)
| p21(X89) )
& ( ~ p21(X89)
| ~ p20(X89) )
& ( p19(X89)
| p20(X89) )
& ( ~ p20(X89)
| ~ p19(X89) )
& ( p18(X89)
| p19(X89) )
& ( ~ p19(X89)
| ~ p18(X89) )
& ( p17(X89)
| p18(X89) )
& ( ~ p18(X89)
| ~ p17(X89) )
& ( p16(X89)
| p17(X89) )
& ( ~ p17(X89)
| ~ p16(X89) )
& ( p15(X89)
| p16(X89) )
& ( ~ p16(X89)
| ~ p15(X89) )
& ( p14(X89)
| p15(X89) )
& ( ~ p15(X89)
| ~ p14(X89) )
& ( p13(X89)
| p14(X89) )
& ( ~ p14(X89)
| ~ p13(X89) )
& ( p12(X89)
| p13(X89) )
& ( ~ p13(X89)
| ~ p12(X89) )
& ( p11(X89)
| p12(X89) )
& ( ~ p12(X89)
| ~ p11(X89) )
& ( p10(X89)
| p11(X89) )
& ( ~ p11(X89)
| ~ p10(X89) )
& ( p9(X89)
| p10(X89) )
& ( ~ p10(X89)
| ~ p9(X89) )
& ( p8(X89)
| p9(X89) )
& ( ~ p9(X89)
| ~ p8(X89) )
& ( p7(X89)
| p8(X89) )
& ( ~ p8(X89)
| ~ p7(X89) )
& ( p6(X89)
| p7(X89) )
& ( ~ p7(X89)
| ~ p6(X89) )
& ( p5(X89)
| p6(X89) )
& ( ~ p6(X89)
| ~ p5(X89) )
& ( p4(X89)
| p5(X89) )
& ( ~ p5(X89)
| ~ p4(X89) )
& ( p3(X89)
| p4(X89) )
& ( ~ p4(X89)
| ~ p3(X89) )
& ( p2(X89)
| p3(X89) )
& ( ~ p3(X89)
| ~ p2(X89) )
& ( p1(X89)
| p2(X89) )
& ( ~ p2(X89)
| ~ p1(X89) ) ) )
| ren44(X1) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[ren44_defn]) ).
% FOF SKOLEM INFERENCE. WIP!!
fof(ren44_skol,plain,
! [X1] :
( ( r1(X1,skf1(X1))
& r1(skf1(X1),skf2(X1))
& r1(skf2(X1),skf3(X1))
& r1(skf3(X1),skf4(X1))
& r1(skf4(X1),skf5(X1))
& r1(skf5(X1),skf6(X1))
& r1(skf6(X1),skf7(X1))
& r1(skf7(X1),skf8(X1))
& r1(skf8(X1),skf9(X1))
& r1(skf9(X1),skf10(X1))
& r1(skf10(X1),skf11(X1))
& r1(skf11(X1),skf12(X1))
& r1(skf12(X1),skf13(X1))
& r1(skf13(X1),skf14(X1))
& r1(skf14(X1),skf15(X1))
& r1(skf15(X1),skf16(X1))
& r1(skf16(X1),skf17(X1))
& r1(skf17(X1),skf18(X1))
& r1(skf18(X1),skf19(X1))
& r1(skf19(X1),skf20(X1))
& r1(skf20(X1),skf21(X1))
& r1(skf21(X1),skf22(X1))
& r1(skf22(X1),skf23(X1))
& r1(skf23(X1),skf24(X1))
& r1(skf24(X1),skf25(X1))
& r1(skf25(X1),skf26(X1))
& r1(skf26(X1),skf27(X1))
& r1(skf27(X1),skf28(X1))
& r1(skf28(X1),skf29(X1))
& r1(skf29(X1),skf30(X1))
& r1(skf30(X1),skf31(X1))
& r1(skf31(X1),skf32(X1))
& r1(skf32(X1),skf33(X1))
& r1(skf33(X1),skf34(X1))
& r1(skf34(X1),skf35(X1))
& r1(skf35(X1),skf36(X1))
& r1(skf36(X1),skf37(X1))
& r1(skf37(X1),skf38(X1))
& r1(skf38(X1),skf39(X1))
& r1(skf39(X1),skf40(X1))
& r1(skf40(X1),skf41(X1))
& r1(skf41(X1),skf42(X1))
& r1(skf42(X1),skf43(X1))
& ! [X45] :
( ~ r1(skf42(X1),X45)
| ~ ren1(X45) )
& ! [X46] :
( ~ r1(skf41(X1),X46)
| ~ ren2(X46) )
& ! [X47] :
( ~ r1(skf40(X1),X47)
| ~ ren3(X47) )
& ! [X48] :
( ~ r1(skf39(X1),X48)
| ~ ren4(X48) )
& ! [X49] :
( ~ r1(skf38(X1),X49)
| ~ ren5(X49) )
& ! [X50] :
( ~ r1(skf37(X1),X50)
| ~ ren6(X50) )
& ! [X51] :
( ~ r1(skf36(X1),X51)
| ~ ren7(X51) )
& ! [X52] :
( ~ r1(skf35(X1),X52)
| ~ ren8(X52) )
& ! [X53] :
( ~ r1(skf34(X1),X53)
| ~ ren9(X53) )
& ! [X54] :
( ~ r1(skf33(X1),X54)
| ~ ren10(X54) )
& ! [X55] :
( ~ r1(skf32(X1),X55)
| ~ ren11(X55) )
& ! [X56] :
( ~ r1(skf31(X1),X56)
| ~ ren12(X56) )
& ! [X57] :
( ~ r1(skf30(X1),X57)
| ~ ren13(X57) )
& ! [X58] :
( ~ r1(skf29(X1),X58)
| ~ ren14(X58) )
& ! [X59] :
( ~ r1(skf28(X1),X59)
| ~ ren15(X59) )
& ! [X60] :
( ~ r1(skf27(X1),X60)
| ~ ren16(X60) )
& ! [X61] :
( ~ r1(skf26(X1),X61)
| ~ ren17(X61) )
& ! [X62] :
( ~ r1(skf25(X1),X62)
| ~ ren18(X62) )
& ! [X63] :
( ~ r1(skf24(X1),X63)
| ~ ren19(X63) )
& ! [X64] :
( ~ r1(skf23(X1),X64)
| ~ ren20(X64) )
& ! [X65] :
( ~ r1(skf22(X1),X65)
| ~ ren21(X65) )
& ! [X66] :
( ~ r1(skf21(X1),X66)
| ~ ren22(X66) )
& ! [X67] :
( ~ r1(skf20(X1),X67)
| ~ ren23(X67) )
& ! [X68] :
( ~ r1(skf19(X1),X68)
| ~ ren24(X68) )
& ! [X69] :
( ~ r1(skf18(X1),X69)
| ~ ren25(X69) )
& ! [X70] :
( ~ r1(skf17(X1),X70)
| ~ ren26(X70) )
& ! [X71] :
( ~ r1(skf16(X1),X71)
| ~ ren27(X71) )
& ! [X72] :
( ~ r1(skf15(X1),X72)
| ~ ren28(X72) )
& ! [X73] :
( ~ r1(skf14(X1),X73)
| ~ ren29(X73) )
& ! [X74] :
( ~ r1(skf13(X1),X74)
| ~ ren30(X74) )
& ! [X75] :
( ~ r1(skf12(X1),X75)
| ~ ren31(X75) )
& ! [X76] :
( ~ r1(skf11(X1),X76)
| ~ ren32(X76) )
& ! [X77] :
( ~ r1(skf10(X1),X77)
| ~ ren33(X77) )
& ! [X78] :
( ~ r1(skf9(X1),X78)
| ~ ren34(X78) )
& ! [X79] :
( ~ r1(skf8(X1),X79)
| ~ ren35(X79) )
& ! [X80] :
( ~ r1(skf7(X1),X80)
| ~ ren36(X80) )
& ! [X81] :
( ~ r1(skf6(X1),X81)
| ~ ren37(X81) )
& ! [X82] :
( ~ r1(skf5(X1),X82)
| ~ ren38(X82) )
& ! [X83] :
( ~ r1(skf4(X1),X83)
| ~ ren39(X83) )
& ! [X84] :
( ~ r1(skf3(X1),X84)
| ~ ren40(X84) )
& ! [X85] :
( ~ r1(skf2(X1),X85)
| ~ ren41(X85) )
& ! [X86] :
( ~ r1(skf1(X1),X86)
| ~ ren42(X86) )
& ! [X87] :
( ~ r1(X1,X87)
| ~ ren43(X87) )
& r1(X1,skf44(X1))
& ~ p45(skf44(X1))
& r1(X1,skf45(X1))
& ( p43(skf45(X1))
| p44(skf45(X1)) )
& ( ~ p44(skf45(X1))
| ~ p43(skf45(X1)) )
& ( p42(skf45(X1))
| p43(skf45(X1)) )
& ( ~ p43(skf45(X1))
| ~ p42(skf45(X1)) )
& ( p41(skf45(X1))
| p42(skf45(X1)) )
& ( ~ p42(skf45(X1))
| ~ p41(skf45(X1)) )
& ( p40(skf45(X1))
| p41(skf45(X1)) )
& ( ~ p41(skf45(X1))
| ~ p40(skf45(X1)) )
& ( p39(skf45(X1))
| p40(skf45(X1)) )
& ( ~ p40(skf45(X1))
| ~ p39(skf45(X1)) )
& ( p38(skf45(X1))
| p39(skf45(X1)) )
& ( ~ p39(skf45(X1))
| ~ p38(skf45(X1)) )
& ( p37(skf45(X1))
| p38(skf45(X1)) )
& ( ~ p38(skf45(X1))
| ~ p37(skf45(X1)) )
& ( p36(skf45(X1))
| p37(skf45(X1)) )
& ( ~ p37(skf45(X1))
| ~ p36(skf45(X1)) )
& ( p35(skf45(X1))
| p36(skf45(X1)) )
& ( ~ p36(skf45(X1))
| ~ p35(skf45(X1)) )
& ( p34(skf45(X1))
| p35(skf45(X1)) )
& ( ~ p35(skf45(X1))
| ~ p34(skf45(X1)) )
& ( p33(skf45(X1))
| p34(skf45(X1)) )
& ( ~ p34(skf45(X1))
| ~ p33(skf45(X1)) )
& ( p32(skf45(X1))
| p33(skf45(X1)) )
& ( ~ p33(skf45(X1))
| ~ p32(skf45(X1)) )
& ( p31(skf45(X1))
| p32(skf45(X1)) )
& ( ~ p32(skf45(X1))
| ~ p31(skf45(X1)) )
& ( p30(skf45(X1))
| p31(skf45(X1)) )
& ( ~ p31(skf45(X1))
| ~ p30(skf45(X1)) )
& ( p29(skf45(X1))
| p30(skf45(X1)) )
& ( ~ p30(skf45(X1))
| ~ p29(skf45(X1)) )
& ( p28(skf45(X1))
| p29(skf45(X1)) )
& ( ~ p29(skf45(X1))
| ~ p28(skf45(X1)) )
& ( p27(skf45(X1))
| p28(skf45(X1)) )
& ( ~ p28(skf45(X1))
| ~ p27(skf45(X1)) )
& ( p26(skf45(X1))
| p27(skf45(X1)) )
& ( ~ p27(skf45(X1))
| ~ p26(skf45(X1)) )
& ( p25(skf45(X1))
| p26(skf45(X1)) )
& ( ~ p26(skf45(X1))
| ~ p25(skf45(X1)) )
& ( p24(skf45(X1))
| p25(skf45(X1)) )
& ( ~ p25(skf45(X1))
| ~ p24(skf45(X1)) )
& ( p23(skf45(X1))
| p24(skf45(X1)) )
& ( ~ p24(skf45(X1))
| ~ p23(skf45(X1)) )
& ( p22(skf45(X1))
| p23(skf45(X1)) )
& ( ~ p23(skf45(X1))
| ~ p22(skf45(X1)) )
& ( p21(skf45(X1))
| p22(skf45(X1)) )
& ( ~ p22(skf45(X1))
| ~ p21(skf45(X1)) )
& ( p20(skf45(X1))
| p21(skf45(X1)) )
& ( ~ p21(skf45(X1))
| ~ p20(skf45(X1)) )
& ( p19(skf45(X1))
| p20(skf45(X1)) )
& ( ~ p20(skf45(X1))
| ~ p19(skf45(X1)) )
& ( p18(skf45(X1))
| p19(skf45(X1)) )
& ( ~ p19(skf45(X1))
| ~ p18(skf45(X1)) )
& ( p17(skf45(X1))
| p18(skf45(X1)) )
& ( ~ p18(skf45(X1))
| ~ p17(skf45(X1)) )
& ( p16(skf45(X1))
| p17(skf45(X1)) )
& ( ~ p17(skf45(X1))
| ~ p16(skf45(X1)) )
& ( p15(skf45(X1))
| p16(skf45(X1)) )
& ( ~ p16(skf45(X1))
| ~ p15(skf45(X1)) )
& ( p14(skf45(X1))
| p15(skf45(X1)) )
& ( ~ p15(skf45(X1))
| ~ p14(skf45(X1)) )
& ( p13(skf45(X1))
| p14(skf45(X1)) )
& ( ~ p14(skf45(X1))
| ~ p13(skf45(X1)) )
& ( p12(skf45(X1))
| p13(skf45(X1)) )
& ( ~ p13(skf45(X1))
| ~ p12(skf45(X1)) )
& ( p11(skf45(X1))
| p12(skf45(X1)) )
& ( ~ p12(skf45(X1))
| ~ p11(skf45(X1)) )
& ( p10(skf45(X1))
| p11(skf45(X1)) )
& ( ~ p11(skf45(X1))
| ~ p10(skf45(X1)) )
& ( p9(skf45(X1))
| p10(skf45(X1)) )
& ( ~ p10(skf45(X1))
| ~ p9(skf45(X1)) )
& ( p8(skf45(X1))
| p9(skf45(X1)) )
& ( ~ p9(skf45(X1))
| ~ p8(skf45(X1)) )
& ( p7(skf45(X1))
| p8(skf45(X1)) )
& ( ~ p8(skf45(X1))
| ~ p7(skf45(X1)) )
& ( p6(skf45(X1))
| p7(skf45(X1)) )
& ( ~ p7(skf45(X1))
| ~ p6(skf45(X1)) )
& ( p5(skf45(X1))
| p6(skf45(X1)) )
& ( ~ p6(skf45(X1))
| ~ p5(skf45(X1)) )
& ( p4(skf45(X1))
| p5(skf45(X1)) )
& ( ~ p5(skf45(X1))
| ~ p4(skf45(X1)) )
& ( p3(skf45(X1))
| p4(skf45(X1)) )
& ( ~ p4(skf45(X1))
| ~ p3(skf45(X1)) )
& ( p2(skf45(X1))
| p3(skf45(X1)) )
& ( ~ p3(skf45(X1))
| ~ p2(skf45(X1)) )
& ( p1(skf45(X1))
| p2(skf45(X1)) )
& ( ~ p2(skf45(X1))
| ~ p1(skf45(X1)) ) )
| ren44(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[skf1,skf2,skf3,skf4,skf5,skf6,skf7,skf8,skf9,skf10,skf11,skf12,skf13,skf14,skf15,skf16,skf17,skf18,skf19,skf20,skf21,skf22,skf23,skf24,skf25,skf26,skf27,skf28,skf29,skf30,skf31,skf32,skf33,skf34,skf35,skf36,skf37,skf38,skf39,skf40,skf41,skf42,skf43,skf44,skf45]),skolemize(X2,skf1(X1)),skolemize(X3,skf2(X1)),skolemize(X4,skf3(X1)),skolemize(X5,skf4(X1)),skolemize(X6,skf5(X1)),skolemize(X7,skf6(X1)),skolemize(X8,skf7(X1)),skolemize(X9,skf8(X1)),skolemize(X10,skf9(X1)),skolemize(X11,skf10(X1)),skolemize(X12,skf11(X1)),skolemize(X13,skf12(X1)),skolemize(X14,skf13(X1)),skolemize(X15,skf14(X1)),skolemize(X16,skf15(X1)),skolemize(X17,skf16(X1)),skolemize(X18,skf17(X1)),skolemize(X19,skf18(X1)),skolemize(X20,skf19(X1)),skolemize(X21,skf20(X1)),skolemize(X22,skf21(X1)),skolemize(X23,skf22(X1)),skolemize(X24,skf23(X1)),skolemize(X25,skf24(X1)),skolemize(X26,skf25(X1)),skolemize(X27,skf26(X1)),skolemize(X28,skf27(X1)),skolemize(X29,skf28(X1)),skolemize(X30,skf29(X1)),skolemize(X31,skf30(X1)),skolemize(X32,skf31(X1)),skolemize(X33,skf32(X1)),skolemize(X34,skf33(X1)),skolemize(X35,skf34(X1)),skolemize(X36,skf35(X1)),skolemize(X37,skf36(X1)),skolemize(X38,skf37(X1)),skolemize(X39,skf38(X1)),skolemize(X40,skf39(X1)),skolemize(X41,skf40(X1)),skolemize(X42,skf41(X1)),skolemize(X43,skf42(X1)),skolemize(X44,skf43(X1)),skolemize(X88,skf44(X1)),skolemize(X89,skf45(X1))],[ren44_elimImpEquivPushNegMiniScope]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_174,plain,
( ~ r1(X0,X1)
| ~ ren43(X1)
| ren44(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren44_skol])]) ).
% CNF SPASS RESOLUTION.
cnf(c_270,plain,
( ~ ren43(X0)
| ren44(X0) ),
inference(resolution,[status(thm)],[c_1,c_174]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_177,plain,
( r1(X0,skf45(X0))
| ren44(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren44_skol])]) ).
% FOF INTRODUCE RENAMING
fof(ren1_defn,definition,
! [X49] :
( ren1(X49)
<= ( ( p44(X49)
& ~ p43(X49) )
| ( ~ p44(X49)
& p43(X49) ) ) ),
introduced(definition,[new_symbols(definition,[ren1])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren2_defn,definition,
! [X50] :
( ren2(X50)
<= ( ( p43(X50)
& ~ p42(X50) )
| ( ~ p43(X50)
& p42(X50) ) ) ),
introduced(definition,[new_symbols(definition,[ren2])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren3_defn,definition,
! [X51] :
( ren3(X51)
<= ( ( p42(X51)
& ~ p41(X51) )
| ( ~ p42(X51)
& p41(X51) ) ) ),
introduced(definition,[new_symbols(definition,[ren3])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren4_defn,definition,
! [X52] :
( ren4(X52)
<= ( ( p41(X52)
& ~ p40(X52) )
| ( ~ p41(X52)
& p40(X52) ) ) ),
introduced(definition,[new_symbols(definition,[ren4])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren5_defn,definition,
! [X53] :
( ren5(X53)
<= ( ( p40(X53)
& ~ p39(X53) )
| ( ~ p40(X53)
& p39(X53) ) ) ),
introduced(definition,[new_symbols(definition,[ren5])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren6_defn,definition,
! [X54] :
( ren6(X54)
<= ( ( p39(X54)
& ~ p38(X54) )
| ( ~ p39(X54)
& p38(X54) ) ) ),
introduced(definition,[new_symbols(definition,[ren6])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren7_defn,definition,
! [X55] :
( ren7(X55)
<= ( ( p38(X55)
& ~ p37(X55) )
| ( ~ p38(X55)
& p37(X55) ) ) ),
introduced(definition,[new_symbols(definition,[ren7])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren8_defn,definition,
! [X56] :
( ren8(X56)
<= ( ( p37(X56)
& ~ p36(X56) )
| ( ~ p37(X56)
& p36(X56) ) ) ),
introduced(definition,[new_symbols(definition,[ren8])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren9_defn,definition,
! [X57] :
( ren9(X57)
<= ( ( p36(X57)
& ~ p35(X57) )
| ( ~ p36(X57)
& p35(X57) ) ) ),
introduced(definition,[new_symbols(definition,[ren9])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren10_defn,definition,
! [X58] :
( ren10(X58)
<= ( ( p35(X58)
& ~ p34(X58) )
| ( ~ p35(X58)
& p34(X58) ) ) ),
introduced(definition,[new_symbols(definition,[ren10])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren11_defn,definition,
! [X59] :
( ren11(X59)
<= ( ( p34(X59)
& ~ p33(X59) )
| ( ~ p34(X59)
& p33(X59) ) ) ),
introduced(definition,[new_symbols(definition,[ren11])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren12_defn,definition,
! [X60] :
( ren12(X60)
<= ( ( p33(X60)
& ~ p32(X60) )
| ( ~ p33(X60)
& p32(X60) ) ) ),
introduced(definition,[new_symbols(definition,[ren12])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren13_defn,definition,
! [X61] :
( ren13(X61)
<= ( ( p32(X61)
& ~ p31(X61) )
| ( ~ p32(X61)
& p31(X61) ) ) ),
introduced(definition,[new_symbols(definition,[ren13])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren14_defn,definition,
! [X62] :
( ren14(X62)
<= ( ( p31(X62)
& ~ p30(X62) )
| ( ~ p31(X62)
& p30(X62) ) ) ),
introduced(definition,[new_symbols(definition,[ren14])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren15_defn,definition,
! [X63] :
( ren15(X63)
<= ( ( p30(X63)
& ~ p29(X63) )
| ( ~ p30(X63)
& p29(X63) ) ) ),
introduced(definition,[new_symbols(definition,[ren15])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren16_defn,definition,
! [X64] :
( ren16(X64)
<= ( ( p29(X64)
& ~ p28(X64) )
| ( ~ p29(X64)
& p28(X64) ) ) ),
introduced(definition,[new_symbols(definition,[ren16])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren17_defn,definition,
! [X65] :
( ren17(X65)
<= ( ( p28(X65)
& ~ p27(X65) )
| ( ~ p28(X65)
& p27(X65) ) ) ),
introduced(definition,[new_symbols(definition,[ren17])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren18_defn,definition,
! [X66] :
( ren18(X66)
<= ( ( p27(X66)
& ~ p26(X66) )
| ( ~ p27(X66)
& p26(X66) ) ) ),
introduced(definition,[new_symbols(definition,[ren18])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren19_defn,definition,
! [X67] :
( ren19(X67)
<= ( ( p26(X67)
& ~ p25(X67) )
| ( ~ p26(X67)
& p25(X67) ) ) ),
introduced(definition,[new_symbols(definition,[ren19])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren20_defn,definition,
! [X68] :
( ren20(X68)
<= ( ( p25(X68)
& ~ p24(X68) )
| ( ~ p25(X68)
& p24(X68) ) ) ),
introduced(definition,[new_symbols(definition,[ren20])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren21_defn,definition,
! [X69] :
( ren21(X69)
<= ( ( p24(X69)
& ~ p23(X69) )
| ( ~ p24(X69)
& p23(X69) ) ) ),
introduced(definition,[new_symbols(definition,[ren21])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren22_defn,definition,
! [X70] :
( ren22(X70)
<= ( ( p23(X70)
& ~ p22(X70) )
| ( ~ p23(X70)
& p22(X70) ) ) ),
introduced(definition,[new_symbols(definition,[ren22])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren23_defn,definition,
! [X71] :
( ren23(X71)
<= ( ( p22(X71)
& ~ p21(X71) )
| ( ~ p22(X71)
& p21(X71) ) ) ),
introduced(definition,[new_symbols(definition,[ren23])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren24_defn,definition,
! [X72] :
( ren24(X72)
<= ( ( p21(X72)
& ~ p20(X72) )
| ( ~ p21(X72)
& p20(X72) ) ) ),
introduced(definition,[new_symbols(definition,[ren24])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren25_defn,definition,
! [X73] :
( ren25(X73)
<= ( ( p20(X73)
& ~ p19(X73) )
| ( ~ p20(X73)
& p19(X73) ) ) ),
introduced(definition,[new_symbols(definition,[ren25])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren26_defn,definition,
! [X74] :
( ren26(X74)
<= ( ( p19(X74)
& ~ p18(X74) )
| ( ~ p19(X74)
& p18(X74) ) ) ),
introduced(definition,[new_symbols(definition,[ren26])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren27_defn,definition,
! [X75] :
( ren27(X75)
<= ( ( p18(X75)
& ~ p17(X75) )
| ( ~ p18(X75)
& p17(X75) ) ) ),
introduced(definition,[new_symbols(definition,[ren27])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren28_defn,definition,
! [X76] :
( ren28(X76)
<= ( ( p17(X76)
& ~ p16(X76) )
| ( ~ p17(X76)
& p16(X76) ) ) ),
introduced(definition,[new_symbols(definition,[ren28])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren29_defn,definition,
! [X77] :
( ren29(X77)
<= ( ( p16(X77)
& ~ p15(X77) )
| ( ~ p16(X77)
& p15(X77) ) ) ),
introduced(definition,[new_symbols(definition,[ren29])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren30_defn,definition,
! [X78] :
( ren30(X78)
<= ( ( p15(X78)
& ~ p14(X78) )
| ( ~ p15(X78)
& p14(X78) ) ) ),
introduced(definition,[new_symbols(definition,[ren30])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren31_defn,definition,
! [X79] :
( ren31(X79)
<= ( ( p14(X79)
& ~ p13(X79) )
| ( ~ p14(X79)
& p13(X79) ) ) ),
introduced(definition,[new_symbols(definition,[ren31])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren32_defn,definition,
! [X80] :
( ren32(X80)
<= ( ( p13(X80)
& ~ p12(X80) )
| ( ~ p13(X80)
& p12(X80) ) ) ),
introduced(definition,[new_symbols(definition,[ren32])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren33_defn,definition,
! [X81] :
( ren33(X81)
<= ( ( p12(X81)
& ~ p11(X81) )
| ( ~ p12(X81)
& p11(X81) ) ) ),
introduced(definition,[new_symbols(definition,[ren33])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren34_defn,definition,
! [X82] :
( ren34(X82)
<= ( ( p11(X82)
& ~ p10(X82) )
| ( ~ p11(X82)
& p10(X82) ) ) ),
introduced(definition,[new_symbols(definition,[ren34])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren35_defn,definition,
! [X83] :
( ren35(X83)
<= ( ( p10(X83)
& ~ p9(X83) )
| ( ~ p10(X83)
& p9(X83) ) ) ),
introduced(definition,[new_symbols(definition,[ren35])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren36_defn,definition,
! [X84] :
( ren36(X84)
<= ( ( p9(X84)
& ~ p8(X84) )
| ( ~ p9(X84)
& p8(X84) ) ) ),
introduced(definition,[new_symbols(definition,[ren36])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren37_defn,definition,
! [X85] :
( ren37(X85)
<= ( ( p8(X85)
& ~ p7(X85) )
| ( ~ p8(X85)
& p7(X85) ) ) ),
introduced(definition,[new_symbols(definition,[ren37])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren38_defn,definition,
! [X86] :
( ren38(X86)
<= ( ( p7(X86)
& ~ p6(X86) )
| ( ~ p7(X86)
& p6(X86) ) ) ),
introduced(definition,[new_symbols(definition,[ren38])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren39_defn,definition,
! [X87] :
( ren39(X87)
<= ( ( p6(X87)
& ~ p5(X87) )
| ( ~ p6(X87)
& p5(X87) ) ) ),
introduced(definition,[new_symbols(definition,[ren39])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren40_defn,definition,
! [X88] :
( ren40(X88)
<= ( ( p5(X88)
& ~ p4(X88) )
| ( ~ p5(X88)
& p4(X88) ) ) ),
introduced(definition,[new_symbols(definition,[ren40])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren41_defn,definition,
! [X89] :
( ren41(X89)
<= ( ( p4(X89)
& ~ p3(X89) )
| ( ~ p4(X89)
& p3(X89) ) ) ),
introduced(definition,[new_symbols(definition,[ren41])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren42_defn,definition,
! [X90] :
( ren42(X90)
<= ( ( p3(X90)
& ~ p2(X90) )
| ( ~ p3(X90)
& p2(X90) ) ) ),
introduced(definition,[new_symbols(definition,[ren42])],[main_nc_elimTB]) ).
% FOF RENAMING INFERENCE
fof(main_nc_renObv,negated_conjecture,
? [X1] :
~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ p45(X2)
| ! [X3] :
( ~ r1(X2,X3)
| ~ p1(X3) ) )
| ! [X4] :
( ~ r1(X1,X4)
| ~ ! [X5] :
( ~ r1(X4,X5)
| ~ ren44(X5) ) ) ),
inference(renaming,[status(esa)],[main_nc_elimTB,ren1_defn,ren2_defn,ren3_defn,ren4_defn,ren5_defn,ren6_defn,ren7_defn,ren8_defn,ren9_defn,ren10_defn,ren11_defn,ren12_defn,ren13_defn,ren14_defn,ren15_defn,ren16_defn,ren17_defn,ren18_defn,ren19_defn,ren20_defn,ren21_defn,ren22_defn,ren23_defn,ren24_defn,ren25_defn,ren26_defn,ren27_defn,ren28_defn,ren29_defn,ren30_defn,ren31_defn,ren32_defn,ren33_defn,ren34_defn,ren35_defn,ren36_defn,ren37_defn,ren38_defn,ren39_defn,ren40_defn,ren41_defn,ren42_defn,ren43_defn,ren44_defn]) ).
% FOF SIMPLE INFERENCE
fof(main_nc_elimImpEquivPushNegMiniScope,negated_conjecture,
? [X1] :
( ? [X2] :
( r1(X1,X2)
& p45(X2)
& ? [X3] :
( r1(X2,X3)
& p1(X3) ) )
& ? [X4] :
( r1(X1,X4)
& ! [X5] :
( ~ r1(X4,X5)
| ~ ren44(X5) ) ) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[main_nc_renObv]) ).
% FOF SKOLEM INFERENCE. WIP!!
fof(main_nc_skol,negated_conjecture,
( r1(skc46,skc47)
& p45(skc47)
& r1(skc47,skc48)
& p1(skc48)
& r1(skc46,skc49)
& ! [X5] :
( ~ r1(skc49,X5)
| ~ ren44(X5) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[skc46,skc47,skc48,skc49]),skolemize(X1,skc46),skolemize(X2,skc47),skolemize(X3,skc48),skolemize(X4,skc49)],[main_nc_elimImpEquivPushNegMiniScope]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_269,plain,
( ~ r1(skc49,X0)
| ~ ren44(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[main_nc_skol])]) ).
% CNF SPASS RESOLUTION.
cnf(c_272,plain,
~ ren44(skc49),
inference(resolution,[status(thm)],[c_1,c_269]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_88,plain,
( ~ p1(X0)
| p2(X0)
| ren43(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren43_elimImpEquivPushNegMiniScope])]) ).
% CNF SPASS RESOLUTION.
cnf(c_317,plain,
( ~ p1(X0)
| ren44(X0)
| p2(X0) ),
inference(resolution,[status(thm)],[c_270,c_88]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_262,plain,
( p1(skf45(X0))
| p2(skf45(X0))
| ren44(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren44_skol])]) ).
% CNF SPASS RESOLUTION.
cnf(c_315,plain,
( p1(skf45(skc49))
| p2(skf45(skc49)) ),
inference(resolution,[status(thm)],[c_262,c_272]) ).
% CNF SPASS RESOLUTION.
cnf(c_318,plain,
p2(skf45(skc49)),
inference(resolution,[status(thm)],[c_177,c_269,c_272,c_317,c_315]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_263,plain,
( ~ p2(skf45(X0))
| ~ p1(skf45(X0))
| ren44(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren44_skol])]) ).
% CNF SPASS RESOLUTION.
cnf(c_319,plain,
( ~ p2(skf45(skc49))
| ~ p1(skf45(skc49)) ),
inference(resolution,[status(thm)],[c_263,c_272]) ).
% CNF SPASS RESOLUTION.
cnf(c_320,plain,
~ p1(skf45(skc49)),
inference(resolution,[status(thm)],[c_318,c_319]) ).
% CNF SPASS RESOLUTION.
cnf(c_321,plain,
( ~ ren44(skf45(skc49))
| ren44(skc49) ),
inference(resolution,[status(thm)],[c_269,c_177]) ).
% CNF SPASS RESOLUTION.
cnf(c_322,plain,
~ ren44(skf45(skc49)),
inference(resolution,[status(thm)],[c_272,c_321]) ).
% CNF SPASS RESOLUTION.
cnf(c_323,plain,
$false,
inference(resolution,[status(thm)],[c_87,c_270,c_320,c_318,c_322]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL686+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n009.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Fri Sep 4 19:16:36 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.35 Running /export/starexec/sandbox2/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.36
% 0.14/0.36 % Input Clauses:
% 0.14/0.36 % 1:1:1:INP:Top: -> r1(x0,x0)
% 0.14/0.36 % 2:3:3:INP:TopTopTop: r1(x0,x1),r1(x1,x2) -> r1(x0,x2)
% 0.14/0.36 % 3:3:1:INP:Top: p44(x0) -> p43(x0),ren1(x0)
% 0.14/0.36 % 4:3:1:INP:Top: p43(x0) -> p44(x0),ren1(x0)
% 0.14/0.36 % 5:3:1:INP:Top: p43(x0) -> p42(x0),ren2(x0)
% 0.14/0.36 % 6:3:1:INP:Top: p42(x0) -> p43(x0),ren2(x0)
% 0.14/0.36 % 7:3:1:INP:Top: p42(x0) -> p41(x0),ren3(x0)
% 0.14/0.36 % 8:3:1:INP:Top: p41(x0) -> p42(x0),ren3(x0)
% 0.14/0.36 % 9:3:1:INP:Top: p41(x0) -> p40(x0),ren4(x0)
% 0.14/0.36 % 10:3:1:INP:Top: p40(x0) -> p41(x0),ren4(x0)
% 0.14/0.36 % 11:3:1:INP:Top: p40(x0) -> p39(x0),ren5(x0)
% 0.14/0.36 % 12:3:1:INP:Top: p39(x0) -> p40(x0),ren5(x0)
% 0.14/0.36 % 13:3:1:INP:Top: p39(x0) -> p38(x0),ren6(x0)
% 0.14/0.36 % 14:3:1:INP:Top: p38(x0) -> p39(x0),ren6(x0)
% 0.14/0.36 % 15:3:1:INP:Top: p38(x0) -> p37(x0),ren7(x0)
% 0.14/0.36 % 16:3:1:INP:Top: p37(x0) -> p38(x0),ren7(x0)
% 0.14/0.36 % 17:3:1:INP:Top: p37(x0) -> p36(x0),ren8(x0)
% 0.14/0.36 % 18:3:1:INP:Top: p36(x0) -> p37(x0),ren8(x0)
% 0.14/0.36 % 19:3:1:INP:Top: p36(x0) -> p35(x0),ren9(x0)
% 0.14/0.36 % 20:3:1:INP:Top: p35(x0) -> p36(x0),ren9(x0)
% 0.14/0.36 % 21:3:1:INP:Top: p35(x0) -> p34(x0),ren10(x0)
% 0.14/0.36 % 22:3:1:INP:Top: p34(x0) -> p35(x0),ren10(x0)
% 0.14/0.36 % 23:3:1:INP:Top: p34(x0) -> p33(x0),ren11(x0)
% 0.14/0.36 % 24:3:1:INP:Top: p33(x0) -> p34(x0),ren11(x0)
% 0.14/0.36 % 25:3:1:INP:Top: p33(x0) -> p32(x0),ren12(x0)
% 0.14/0.36 % 26:3:1:INP:Top: p32(x0) -> p33(x0),ren12(x0)
% 0.14/0.36 % 27:3:1:INP:Top: p32(x0) -> p31(x0),ren13(x0)
% 0.14/0.36 % 28:3:1:INP:Top: p31(x0) -> p32(x0),ren13(x0)
% 0.14/0.36 % 29:3:1:INP:Top: p31(x0) -> p30(x0),ren14(x0)
% 0.14/0.36 % 30:3:1:INP:Top: p30(x0) -> p31(x0),ren14(x0)
% 0.14/0.36 % 31:3:1:INP:Top: p30(x0) -> p29(x0),ren15(x0)
% 0.14/0.36 % 32:3:1:INP:Top: p29(x0) -> p30(x0),ren15(x0)
% 0.14/0.36 % 33:3:1:INP:Top: p29(x0) -> p28(x0),ren16(x0)
% 0.14/0.36 % 34:3:1:INP:Top: p28(x0) -> p29(x0),ren16(x0)
% 0.14/0.36 % 35:3:1:INP:Top: p28(x0) -> p27(x0),ren17(x0)
% 0.14/0.36 % 36:3:1:INP:Top: p27(x0) -> p28(x0),ren17(x0)
% 0.14/0.36 % 37:3:1:INP:Top: p27(x0) -> p26(x0),ren18(x0)
% 0.14/0.36 % 38:3:1:INP:Top: p26(x0) -> p27(x0),ren18(x0)
% 0.14/0.36 % 39:3:1:INP:Top: p26(x0) -> p25(x0),ren19(x0)
% 0.14/0.36 % 40:3:1:INP:Top: p25(x0) -> p26(x0),ren19(x0)
% 0.14/0.36 % 41:3:1:INP:Top: p25(x0) -> p24(x0),ren20(x0)
% 0.14/0.36 % 42:3:1:INP:Top: p24(x0) -> p25(x0),ren20(x0)
% 0.14/0.36 % 43:3:1:INP:Top: p24(x0) -> p23(x0),ren21(x0)
% 0.14/0.36 % 44:3:1:INP:Top: p23(x0) -> p24(x0),ren21(x0)
% 0.14/0.36 % 45:3:1:INP:Top: p23(x0) -> p22(x0),ren22(x0)
% 0.14/0.36 % 46:3:1:INP:Top: p22(x0) -> p23(x0),ren22(x0)
% 0.14/0.36 % 47:3:1:INP:Top: p22(x0) -> p21(x0),ren23(x0)
% 0.14/0.36 % 48:3:1:INP:Top: p21(x0) -> p22(x0),ren23(x0)
% 0.14/0.36 % 49:3:1:INP:Top: p21(x0) -> p20(x0),ren24(x0)
% 0.14/0.36 % 50:3:1:INP:Top: p20(x0) -> p21(x0),ren24(x0)
% 0.14/0.36 % 51:3:1:INP:Top: p20(x0) -> p19(x0),ren25(x0)
% 0.14/0.36 % 52:3:1:INP:Top: p19(x0) -> p20(x0),ren25(x0)
% 0.14/0.36 % 53:3:1:INP:Top: p19(x0) -> p18(x0),ren26(x0)
% 0.14/0.36 % 54:3:1:INP:Top: p18(x0) -> p19(x0),ren26(x0)
% 0.14/0.36 % 55:3:1:INP:Top: p18(x0) -> p17(x0),ren27(x0)
% 0.14/0.36 % 56:3:1:INP:Top: p17(x0) -> p18(x0),ren27(x0)
% 0.14/0.36 % 57:3:1:INP:Top: p17(x0) -> p16(x0),ren28(x0)
% 0.14/0.36 % 58:3:1:INP:Top: p16(x0) -> p17(x0),ren28(x0)
% 0.14/0.36 % 59:3:1:INP:Top: p16(x0) -> p15(x0),ren29(x0)
% 0.14/0.36 % 60:3:1:INP:Top: p15(x0) -> p16(x0),ren29(x0)
% 0.14/0.36 % 61:3:1:INP:Top: p15(x0) -> p14(x0),ren30(x0)
% 0.14/0.36 % 62:3:1:INP:Top: p14(x0) -> p15(x0),ren30(x0)
% 0.14/0.36 % 63:3:1:INP:Top: p14(x0) -> p13(x0),ren31(x0)
% 0.14/0.36 % 64:3:1:INP:Top: p13(x0) -> p14(x0),ren31(x0)
% 0.14/0.36 % 65:3:1:INP:Top: p13(x0) -> p12(x0),ren32(x0)
% 0.14/0.36 % 66:3:1:INP:Top: p12(x0) -> p13(x0),ren32(x0)
% 0.14/0.36 % 67:3:1:INP:Top: p12(x0) -> p11(x0),ren33(x0)
% 0.14/0.36 % 68:3:1:INP:Top: p11(x0) -> p12(x0),ren33(x0)
% 0.14/0.36 % 69:3:1:INP:Top: p11(x0) -> p10(x0),ren34(x0)
% 0.14/0.36 % 70:3:1:INP:Top: p10(x0) -> p11(x0),ren34(x0)
% 0.14/0.36 % 71:3:1:INP:Top: p10(x0) -> p9(x0),ren35(x0)
% 0.14/0.36 % 72:3:1:INP:Top: p9(x0) -> p10(x0),ren35(x0)
% 0.14/0.36 % 73:3:1:INP:Top: p9(x0) -> p8(x0),ren36(x0)
% 0.14/0.36 % 74:3:1:INP:Top: p8(x0) -> p9(x0),ren36(x0)
% 0.14/0.36 % 75:3:1:INP:Top: p8(x0) -> p7(x0),ren37(x0)
% 0.14/0.36 % 76:3:1:INP:Top: p7(x0) -> p8(x0),ren37(x0)
% 0.14/0.36 % 77:3:1:INP:Top: p7(x0) -> p6(x0),ren38(x0)
% 0.14/0.36 % 78:3:1:INP:Top: p6(x0) -> p7(x0),ren38(x0)
% 0.14/0.36 % 79:3:1:INP:Top: p6(x0) -> p5(x0),ren39(x0)
% 0.14/0.36 % 80:3:1:INP:Top: p5(x0) -> p6(x0),ren39(x0)
% 0.14/0.36 % 81:3:1:INP:Top: p5(x0) -> p4(x0),ren40(x0)
% 0.14/0.36 % 82:3:1:INP:Top: p4(x0) -> p5(x0),ren40(x0)
% 0.14/0.36 % 83:3:1:INP:Top: p4(x0) -> p3(x0),ren41(x0)
% 0.14/0.36 % 84:3:1:INP:Top: p3(x0) -> p4(x0),ren41(x0)
% 0.14/0.36 % 85:3:1:INP:Top: p3(x0) -> p2(x0),ren42(x0)
% 0.14/0.36 % 86:3:1:INP:Top: p2(x0) -> p3(x0),ren42(x0)
% 0.14/0.36 % 87:3:1:INP:Top: p2(x0) -> p1(x0),ren43(x0)
% 0.14/0.36 % 88:3:1:INP:Top: p1(x0) -> p2(x0),ren43(x0)
% 0.14/0.36 % 89:2:1:INP:Top: -> r1(x0,skf1(x0)),ren44(x0)
% 0.14/0.36 % 90:2:1:INP:Top: -> r1(skf1(x0),skf2(x0)),ren44(x0)
% 0.14/0.36 % 91:2:1:INP:Top: -> r1(skf2(x0),skf3(x0)),ren44(x0)
% 0.14/0.36 % 92:2:1:INP:Top: -> r1(skf3(x0),skf4(x0)),ren44(x0)
% 0.14/0.36 % 93:2:1:INP:Top: -> r1(skf4(x0),skf5(x0)),ren44(x0)
% 0.14/0.36 % 94:2:1:INP:Top: -> r1(skf5(x0),skf6(x0)),ren44(x0)
% 0.14/0.36 % 95:2:1:INP:Top: -> r1(skf6(x0),skf7(x0)),ren44(x0)
% 0.14/0.36 % 96:2:1:INP:Top: -> r1(skf7(x0),skf8(x0)),ren44(x0)
% 0.14/0.36 % 97:2:1:INP:Top: -> r1(skf8(x0),skf9(x0)),ren44(x0)
% 0.14/0.36 % 98:2:1:INP:Top: -> r1(skf9(x0),skf10(x0)),ren44(x0)
% 0.14/0.36 % 99:2:1:INP:Top: -> r1(skf10(x0),skf11(x0)),ren44(x0)
% 0.14/0.36 % 100:2:1:INP:Top: -> r1(skf11(x0),skf12(x0)),ren44(x0)
% 0.14/0.36 % 101:2:1:INP:Top: -> r1(skf12(x0),skf13(x0)),ren44(x0)
% 0.14/0.36 % 102:2:1:INP:Top: -> r1(skf13(x0),skf14(x0)),ren44(x0)
% 0.14/0.36 % 103:2:1:INP:Top: -> r1(skf14(x0),skf15(x0)),ren44(x0)
% 0.14/0.36 % 104:2:1:INP:Top: -> r1(skf15(x0),skf16(x0)),ren44(x0)
% 0.14/0.36 % 105:2:1:INP:Top: -> r1(skf16(x0),skf17(x0)),ren44(x0)
% 0.14/0.36 % 106:2:1:INP:Top: -> r1(skf17(x0),skf18(x0)),ren44(x0)
% 0.14/0.36 % 107:2:1:INP:Top: -> r1(skf18(x0),skf19(x0)),ren44(x0)
% 0.14/0.36 % 108:2:1:INP:Top: -> r1(skf19(x0),skf20(x0)),ren44(x0)
% 0.14/0.36 % 109:2:1:INP:Top: -> r1(skf20(x0),skf21(x0)),ren44(x0)
% 0.14/0.36 % 110:2:1:INP:Top: -> r1(skf21(x0),skf22(x0)),ren44(x0)
% 0.14/0.36 % 111:2:1:INP:Top: -> r1(skf22(x0),skf23(x0)),ren44(x0)
% 0.14/0.36 % 112:2:1:INP:Top: -> r1(skf23(x0),skf24(x0)),ren44(x0)
% 0.14/0.36 % 113:2:1:INP:Top: -> r1(skf24(x0),skf25(x0)),ren44(x0)
% 0.14/0.36 % 114:2:1:INP:Top: -> r1(skf25(x0),skf26(x0)),ren44(x0)
% 0.14/0.36 % 115:2:1:INP:Top: -> r1(skf26(x0),skf27(x0)),ren44(x0)
% 0.14/0.36 % 116:2:1:INP:Top: -> r1(skf27(x0),skf28(x0)),ren44(x0)
% 0.14/0.36 % 117:2:1:INP:Top: -> r1(skf28(x0),skf29(x0)),ren44(x0)
% 0.14/0.36 % 118:2:1:INP:Top: -> r1(skf29(x0),skf30(x0)),ren44(x0)
% 0.14/0.36 % 119:2:1:INP:Top: -> r1(skf30(x0),skf31(x0)),ren44(x0)
% 0.14/0.36 % 120:2:1:INP:Top: -> r1(skf31(x0),skf32(x0)),ren44(x0)
% 0.14/0.36 % 121:2:1:INP:Top: -> r1(skf32(x0),skf33(x0)),ren44(x0)
% 0.14/0.36 % 122:2:1:INP:Top: -> r1(skf33(x0),skf34(x0)),ren44(x0)
% 0.14/0.36 % 123:2:1:INP:Top: -> r1(skf34(x0),skf35(x0)),ren44(x0)
% 0.14/0.36 % 124:2:1:INP:Top: -> r1(skf35(x0),skf36(x0)),ren44(x0)
% 0.14/0.36 % 125:2:1:INP:Top: -> r1(skf36(x0),skf37(x0)),ren44(x0)
% 0.14/0.36 % 126:2:1:INP:Top: -> r1(skf37(x0),skf38(x0)),ren44(x0)
% 0.14/0.36 % 127:2:1:INP:Top: -> r1(skf38(x0),skf39(x0)),ren44(x0)
% 0.14/0.36 % 128:2:1:INP:Top: -> r1(skf39(x0),skf40(x0)),ren44(x0)
% 0.14/0.36 % 129:2:1:INP:Top: -> r1(skf40(x0),skf41(x0)),ren44(x0)
% 0.14/0.36 % 130:2:1:INP:Top: -> r1(skf41(x0),skf42(x0)),ren44(x0)
% 0.14/0.36 % 131:2:1:INP:Top: -> r1(skf42(x0),skf43(x0)),ren44(x0)
% 0.14/0.36 % 132:3:2:INP:TopTop: r1(skf42(x0),x1),ren1(x1) -> ren44(x0)
% 0.14/0.36 % 133:3:2:INP:TopTop: r1(skf41(x0),x1),ren2(x1) -> ren44(x0)
% 0.14/0.36 % 134:3:2:INP:TopTop: r1(skf40(x0),x1),ren3(x1) -> ren44(x0)
% 0.14/0.36 % 135:3:2:INP:TopTop: r1(skf39(x0),x1),ren4(x1) -> ren44(x0)
% 0.14/0.36 % 136:3:2:INP:TopTop: r1(skf38(x0),x1),ren5(x1) -> ren44(x0)
% 0.14/0.36 % 137:3:2:INP:TopTop: r1(skf37(x0),x1),ren6(x1) -> ren44(x0)
% 0.14/0.36 % 138:3:2:INP:TopTop: r1(skf36(x0),x1),ren7(x1) -> ren44(x0)
% 0.14/0.36 % 139:3:2:INP:TopTop: r1(skf35(x0),x1),ren8(x1) -> ren44(x0)
% 0.14/0.36 % 140:3:2:INP:TopTop: r1(skf34(x0),x1),ren9(x1) -> ren44(x0)
% 0.14/0.36 % 141:3:2:INP:TopTop: r1(skf33(x0),x1),ren10(x1) -> ren44(x0)
% 0.14/0.36 % 142:3:2:INP:TopTop: r1(skf32(x0),x1),ren11(x1) -> ren44(x0)
% 0.14/0.36 % 143:3:2:INP:TopTop: r1(skf31(x0),x1),ren12(x1) -> ren44(x0)
% 0.14/0.36 % 144:3:2:INP:TopTop: r1(skf30(x0),x1),ren13(x1) -> ren44(x0)
% 0.14/0.36 % 145:3:2:INP:TopTop: r1(skf29(x0),x1),ren14(x1) -> ren44(x0)
% 0.14/0.36 % 146:3:2:INP:TopTop: r1(skf28(x0),x1),ren15(x1) -> ren44(x0)
% 0.14/0.36 % 147:3:2:INP:TopTop: r1(skf27(x0),x1),ren16(x1) -> ren44(x0)
% 0.14/0.36 % 148:3:2:INP:TopTop: r1(skf26(x0),x1),ren17(x1) -> ren44(x0)
% 0.14/0.36 % 149:3:2:INP:TopTop: r1(skf25(x0),x1),ren18(x1) -> ren44(x0)
% 0.14/0.36 % 150:3:2:INP:TopTop: r1(skf24(x0),x1),ren19(x1) -> ren44(x0)
% 0.14/0.36 % 151:3:2:INP:TopTop: r1(skf23(x0),x1),ren20(x1) -> ren44(x0)
% 0.14/0.36 % 152:3:2:INP:TopTop: r1(skf22(x0),x1),ren21(x1) -> ren44(x0)
% 0.14/0.36 % 153:3:2:INP:TopTop: r1(skf21(x0),x1),ren22(x1) -> ren44(x0)
% 0.14/0.36 % 154:3:2:INP:TopTop: r1(skf20(x0),x1),ren23(x1) -> ren44(x0)
% 0.14/0.36 % 155:3:2:INP:TopTop: r1(skf19(x0),x1),ren24(x1) -> ren44(x0)
% 0.14/0.36 % 156:3:2:INP:TopTop: r1(skf18(x0),x1),ren25(x1) -> ren44(x0)
% 0.14/0.36 % 157:3:2:INP:TopTop: r1(skf17(x0),x1),ren26(x1) -> ren44(x0)
% 0.14/0.36 % 158:3:2:INP:TopTop: r1(skf16(x0),x1),ren27(x1) -> ren44(x0)
% 0.14/0.36 % 159:3:2:INP:TopTop: r1(skf15(x0),x1),ren28(x1) -> ren44(x0)
% 0.14/0.36 % 160:3:2:INP:TopTop: r1(skf14(x0),x1),ren29(x1) -> ren44(x0)
% 0.14/0.36 % 161:3:2:INP:TopTop: r1(skf13(x0),x1),ren30(x1) -> ren44(x0)
% 0.14/0.36 % 162:3:2:INP:TopTop: r1(skf12(x0),x1),ren31(x1) -> ren44(x0)
% 0.14/0.36 % 163:3:2:INP:TopTop: r1(skf11(x0),x1),ren32(x1) -> ren44(x0)
% 0.14/0.36 % 164:3:2:INP:TopTop: r1(skf10(x0),x1),ren33(x1) -> ren44(x0)
% 0.14/0.36 % 165:3:2:INP:TopTop: r1(skf9(x0),x1),ren34(x1) -> ren44(x0)
% 0.14/0.36 % 166:3:2:INP:TopTop: r1(skf8(x0),x1),ren35(x1) -> ren44(x0)
% 0.14/0.36 % 167:3:2:INP:TopTop: r1(skf7(x0),x1),ren36(x1) -> ren44(x0)
% 0.14/0.36 % 168:3:2:INP:TopTop: r1(skf6(x0),x1),ren37(x1) -> ren44(x0)
% 0.14/0.36 % 169:3:2:INP:TopTop: r1(skf5(x0),x1),ren38(x1) -> ren44(x0)
% 0.14/0.36 % 170:3:2:INP:TopTop: r1(skf4(x0),x1),ren39(x1) -> ren44(x0)
% 0.14/0.36 % 171:3:2:INP:TopTop: r1(skf3(x0),x1),ren40(x1) -> ren44(x0)
% 0.14/0.36 % 172:3:2:INP:TopTop: r1(skf2(x0),x1),ren41(x1) -> ren44(x0)
% 0.14/0.36 % 173:3:2:INP:TopTop: r1(skf1(x0),x1),ren42(x1) -> ren44(x0)
% 0.14/0.36 % 174:3:2:INP:TopTop: r1(x0,x1),ren43(x1) -> ren44(x0)
% 0.14/0.36 % 175:2:1:INP:Top: -> r1(x0,skf44(x0)),ren44(x0)
% 0.14/0.36 % 176:2:1:INP:Top: p45(skf44(x0)) -> ren44(x0)
% 0.14/0.36 % 177:2:1:INP:Top: -> r1(x0,skf45(x0)),ren44(x0)
% 0.14/0.36 % 178:3:1:INP:Top: -> p43(skf45(x0)),p44(skf45(x0)),ren44(x0)
% 0.14/0.36 % 179:3:1:INP:Top: p44(skf45(x0)),p43(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 180:3:1:INP:Top: -> p42(skf45(x0)),p43(skf45(x0)),ren44(x0)
% 0.14/0.36 % 181:3:1:INP:Top: p43(skf45(x0)),p42(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 182:3:1:INP:Top: -> p41(skf45(x0)),p42(skf45(x0)),ren44(x0)
% 0.14/0.36 % 183:3:1:INP:Top: p42(skf45(x0)),p41(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 184:3:1:INP:Top: -> p40(skf45(x0)),p41(skf45(x0)),ren44(x0)
% 0.14/0.36 % 185:3:1:INP:Top: p41(skf45(x0)),p40(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 186:3:1:INP:Top: -> p39(skf45(x0)),p40(skf45(x0)),ren44(x0)
% 0.14/0.36 % 187:3:1:INP:Top: p40(skf45(x0)),p39(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 188:3:1:INP:Top: -> p38(skf45(x0)),p39(skf45(x0)),ren44(x0)
% 0.14/0.36 % 189:3:1:INP:Top: p39(skf45(x0)),p38(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 190:3:1:INP:Top: -> p37(skf45(x0)),p38(skf45(x0)),ren44(x0)
% 0.14/0.36 % 191:3:1:INP:Top: p38(skf45(x0)),p37(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 192:3:1:INP:Top: -> p36(skf45(x0)),p37(skf45(x0)),ren44(x0)
% 0.14/0.36 % 193:3:1:INP:Top: p37(skf45(x0)),p36(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 194:3:1:INP:Top: -> p35(skf45(x0)),p36(skf45(x0)),ren44(x0)
% 0.14/0.36 % 195:3:1:INP:Top: p36(skf45(x0)),p35(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 196:3:1:INP:Top: -> p34(skf45(x0)),p35(skf45(x0)),ren44(x0)
% 0.14/0.36 % 197:3:1:INP:Top: p35(skf45(x0)),p34(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 198:3:1:INP:Top: -> p33(skf45(x0)),p34(skf45(x0)),ren44(x0)
% 0.14/0.36 % 199:3:1:INP:Top: p34(skf45(x0)),p33(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 200:3:1:INP:Top: -> p32(skf45(x0)),p33(skf45(x0)),ren44(x0)
% 0.14/0.36 % 201:3:1:INP:Top: p33(skf45(x0)),p32(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 202:3:1:INP:Top: -> p31(skf45(x0)),p32(skf45(x0)),ren44(x0)
% 0.14/0.36 % 203:3:1:INP:Top: p32(skf45(x0)),p31(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 204:3:1:INP:Top: -> p30(skf45(x0)),p31(skf45(x0)),ren44(x0)
% 0.14/0.36 % 205:3:1:INP:Top: p31(skf45(x0)),p30(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 206:3:1:INP:Top: -> p29(skf45(x0)),p30(skf45(x0)),ren44(x0)
% 0.14/0.36 % 207:3:1:INP:Top: p30(skf45(x0)),p29(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 208:3:1:INP:Top: -> p28(skf45(x0)),p29(skf45(x0)),ren44(x0)
% 0.14/0.36 % 209:3:1:INP:Top: p29(skf45(x0)),p28(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 210:3:1:INP:Top: -> p27(skf45(x0)),p28(skf45(x0)),ren44(x0)
% 0.14/0.36 % 211:3:1:INP:Top: p28(skf45(x0)),p27(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 212:3:1:INP:Top: -> p26(skf45(x0)),p27(skf45(x0)),ren44(x0)
% 0.14/0.36 % 213:3:1:INP:Top: p27(skf45(x0)),p26(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 214:3:1:INP:Top: -> p25(skf45(x0)),p26(skf45(x0)),ren44(x0)
% 0.14/0.36 % 215:3:1:INP:Top: p26(skf45(x0)),p25(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 216:3:1:INP:Top: -> p24(skf45(x0)),p25(skf45(x0)),ren44(x0)
% 0.14/0.36 % 217:3:1:INP:Top: p25(skf45(x0)),p24(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 218:3:1:INP:Top: -> p23(skf45(x0)),p24(skf45(x0)),ren44(x0)
% 0.14/0.36 % 219:3:1:INP:Top: p24(skf45(x0)),p23(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 220:3:1:INP:Top: -> p22(skf45(x0)),p23(skf45(x0)),ren44(x0)
% 0.14/0.36 % 221:3:1:INP:Top: p23(skf45(x0)),p22(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 222:3:1:INP:Top: -> p21(skf45(x0)),p22(skf45(x0)),ren44(x0)
% 0.14/0.36 % 223:3:1:INP:Top: p22(skf45(x0)),p21(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 224:3:1:INP:Top: -> p20(skf45(x0)),p21(skf45(x0)),ren44(x0)
% 0.14/0.36 % 225:3:1:INP:Top: p21(skf45(x0)),p20(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 226:3:1:INP:Top: -> p19(skf45(x0)),p20(skf45(x0)),ren44(x0)
% 0.14/0.36 % 227:3:1:INP:Top: p20(skf45(x0)),p19(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 228:3:1:INP:Top: -> p18(skf45(x0)),p19(skf45(x0)),ren44(x0)
% 0.14/0.36 % 229:3:1:INP:Top: p19(skf45(x0)),p18(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 230:3:1:INP:Top: -> p17(skf45(x0)),p18(skf45(x0)),ren44(x0)
% 0.14/0.36 % 231:3:1:INP:Top: p18(skf45(x0)),p17(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 232:3:1:INP:Top: -> p16(skf45(x0)),p17(skf45(x0)),ren44(x0)
% 0.14/0.36 % 233:3:1:INP:Top: p17(skf45(x0)),p16(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 234:3:1:INP:Top: -> p15(skf45(x0)),p16(skf45(x0)),ren44(x0)
% 0.14/0.36 % 235:3:1:INP:Top: p16(skf45(x0)),p15(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 236:3:1:INP:Top: -> p14(skf45(x0)),p15(skf45(x0)),ren44(x0)
% 0.14/0.36 % 237:3:1:INP:Top: p15(skf45(x0)),p14(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 238:3:1:INP:Top: -> p13(skf45(x0)),p14(skf45(x0)),ren44(x0)
% 0.14/0.36 % 239:3:1:INP:Top: p14(skf45(x0)),p13(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 240:3:1:INP:Top: -> p12(skf45(x0)),p13(skf45(x0)),ren44(x0)
% 0.14/0.36 % 241:3:1:INP:Top: p13(skf45(x0)),p12(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 242:3:1:INP:Top: -> p11(skf45(x0)),p12(skf45(x0)),ren44(x0)
% 0.14/0.36 % 243:3:1:INP:Top: p12(skf45(x0)),p11(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 244:3:1:INP:Top: -> p10(skf45(x0)),p11(skf45(x0)),ren44(x0)
% 0.14/0.36 % 245:3:1:INP:Top: p11(skf45(x0)),p10(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 246:3:1:INP:Top: -> p9(skf45(x0)),p10(skf45(x0)),ren44(x0)
% 0.14/0.36 % 247:3:1:INP:Top: p10(skf45(x0)),p9(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 248:3:1:INP:Top: -> p8(skf45(x0)),p9(skf45(x0)),ren44(x0)
% 0.14/0.36 % 249:3:1:INP:Top: p9(skf45(x0)),p8(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 250:3:1:INP:Top: -> p7(skf45(x0)),p8(skf45(x0)),ren44(x0)
% 0.14/0.36 % 251:3:1:INP:Top: p8(skf45(x0)),p7(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 252:3:1:INP:Top: -> p6(skf45(x0)),p7(skf45(x0)),ren44(x0)
% 0.14/0.36 % 253:3:1:INP:Top: p7(skf45(x0)),p6(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 254:3:1:INP:Top: -> p5(skf45(x0)),p6(skf45(x0)),ren44(x0)
% 0.14/0.36 % 255:3:1:INP:Top: p6(skf45(x0)),p5(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 256:3:1:INP:Top: -> p4(skf45(x0)),p5(skf45(x0)),ren44(x0)
% 0.14/0.36 % 257:3:1:INP:Top: p5(skf45(x0)),p4(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 258:3:1:INP:Top: -> p3(skf45(x0)),p4(skf45(x0)),ren44(x0)
% 0.14/0.36 % 259:3:1:INP:Top: p4(skf45(x0)),p3(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 260:3:1:INP:Top: -> p2(skf45(x0)),p3(skf45(x0)),ren44(x0)
% 0.14/0.36 % 261:3:1:INP:Top: p3(skf45(x0)),p2(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 262:3:1:INP:Top: -> p1(skf45(x0)),p2(skf45(x0)),ren44(x0)
% 0.14/0.36 % 263:3:1:INP:Top: p2(skf45(x0)),p1(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 264:1:0:INP:: -> r1(skc46,skc47)
% 0.14/0.36 % 265:1:0:INP:: -> p45(skc47)
% 0.14/0.36 % 266:1:0:INP:: -> r1(skc47,skc48)
% 0.14/0.36 % 267:1:0:INP:: -> p1(skc48)
% 0.14/0.36 % 268:1:0:INP:: -> r1(skc46,skc49)
% 0.14/0.36 % 269:2:1:INP:Top: r1(skc49,x0),ren44(x0) ->
% 0.14/0.36
% 0.14/0.36 % Predicates: r1 p45 p1 p44 p43 p42 p41 p40 p39 p38 p37 p36 p35 p34 p33 p32 p31 p30 p29 p28 p27 p26 p25 p24 p23 p22 p21 p20 p19 p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 ren12 ren13 ren14 ren15 ren16 ren17 ren18 ren19 ren20 ren21 ren22 ren23 ren24 ren25 ren26 ren27 ren28 ren29 ren30 ren31 ren32 ren33 ren34 ren35 ren36 ren37 ren38 ren39 ren40 ren41 ren42 ren43 ren44
% 0.14/0.36 % Fol Constants: skc46 skc47 skc48 skc49
% 0.14/0.36 % Fol Functions: skf1 skf2 skf3 skf4 skf5 skf6 skf7 skf8 skf9 skf10 skf11 skf12 skf13 skf14 skf15 skf16 skf17 skf18 skf19 skf20 skf21 skf22 skf23 skf24 skf25 skf26 skf27 skf28 skf29 skf30 skf31 skf32 skf33 skf34 skf35 skf36 skf37 skf38 skf39 skf40 skf41 skf42 skf43 skf44 skf45
% 0.14/0.36 % Problem Properties:
% 0.14/0.36 % This is a full first-order problem without equality. The Problem is non-linear.
% 0.14/0.36
% 0.14/0.36
% 0.14/0.36 % Reduced Input Axiom Clauses:
% 0.14/0.36 % 1:1:1:INP:Top: -> r1(x0,x0)
% 0.14/0.36 % 2:3:3:INP:TopTopTop: r1(x0,x1),r1(x1,x2) -> r1(x0,x2)
% 0.14/0.36 % 3:3:1:INP:Top: p44(x0) -> p43(x0),ren1(x0)
% 0.14/0.36 % 4:3:1:INP:Top: p43(x0) -> p44(x0),ren1(x0)
% 0.14/0.36 % 5:3:1:INP:Top: p43(x0) -> p42(x0),ren2(x0)
% 0.14/0.36 % 6:3:1:INP:Top: p42(x0) -> p43(x0),ren2(x0)
% 0.14/0.36 % 7:3:1:INP:Top: p42(x0) -> p41(x0),ren3(x0)
% 0.14/0.36 % 8:3:1:INP:Top: p41(x0) -> p42(x0),ren3(x0)
% 0.14/0.36 % 9:3:1:INP:Top: p41(x0) -> p40(x0),ren4(x0)
% 0.14/0.36 % 10:3:1:INP:Top: p40(x0) -> p41(x0),ren4(x0)
% 0.14/0.36 % 11:3:1:INP:Top: p40(x0) -> p39(x0),ren5(x0)
% 0.14/0.36 % 12:3:1:INP:Top: p39(x0) -> p40(x0),ren5(x0)
% 0.14/0.36 % 13:3:1:INP:Top: p39(x0) -> p38(x0),ren6(x0)
% 0.14/0.36 % 14:3:1:INP:Top: p38(x0) -> p39(x0),ren6(x0)
% 0.14/0.36 % 15:3:1:INP:Top: p38(x0) -> p37(x0),ren7(x0)
% 0.14/0.36 % 16:3:1:INP:Top: p37(x0) -> p38(x0),ren7(x0)
% 0.14/0.36 % 17:3:1:INP:Top: p37(x0) -> p36(x0),ren8(x0)
% 0.14/0.36 % 18:3:1:INP:Top: p36(x0) -> p37(x0),ren8(x0)
% 0.14/0.36 % 19:3:1:INP:Top: p36(x0) -> p35(x0),ren9(x0)
% 0.14/0.36 % 20:3:1:INP:Top: p35(x0) -> p36(x0),ren9(x0)
% 0.14/0.36 % 21:3:1:INP:Top: p35(x0) -> p34(x0),ren10(x0)
% 0.14/0.36 % 22:3:1:INP:Top: p34(x0) -> p35(x0),ren10(x0)
% 0.14/0.36 % 23:3:1:INP:Top: p34(x0) -> p33(x0),ren11(x0)
% 0.14/0.36 % 24:3:1:INP:Top: p33(x0) -> p34(x0),ren11(x0)
% 0.14/0.36 % 25:3:1:INP:Top: p33(x0) -> p32(x0),ren12(x0)
% 0.14/0.36 % 26:3:1:INP:Top: p32(x0) -> p33(x0),ren12(x0)
% 0.14/0.36 % 27:3:1:INP:Top: p32(x0) -> p31(x0),ren13(x0)
% 0.14/0.36 % 28:3:1:INP:Top: p31(x0) -> p32(x0),ren13(x0)
% 0.14/0.36 % 29:3:1:INP:Top: p31(x0) -> p30(x0),ren14(x0)
% 0.14/0.36 % 30:3:1:INP:Top: p30(x0) -> p31(x0),ren14(x0)
% 0.14/0.36 % 31:3:1:INP:Top: p30(x0) -> p29(x0),ren15(x0)
% 0.14/0.36 % 32:3:1:INP:Top: p29(x0) -> p30(x0),ren15(x0)
% 0.14/0.36 % 33:3:1:INP:Top: p29(x0) -> p28(x0),ren16(x0)
% 0.14/0.36 % 34:3:1:INP:Top: p28(x0) -> p29(x0),ren16(x0)
% 0.14/0.36 % 35:3:1:INP:Top: p28(x0) -> p27(x0),ren17(x0)
% 0.14/0.36 % 36:3:1:INP:Top: p27(x0) -> p28(x0),ren17(x0)
% 0.14/0.36 % 37:3:1:INP:Top: p27(x0) -> p26(x0),ren18(x0)
% 0.14/0.36 % 38:3:1:INP:Top: p26(x0) -> p27(x0),ren18(x0)
% 0.14/0.36 % 39:3:1:INP:Top: p26(x0) -> p25(x0),ren19(x0)
% 0.14/0.36 % 40:3:1:INP:Top: p25(x0) -> p26(x0),ren19(x0)
% 0.14/0.36 % 41:3:1:INP:Top: p25(x0) -> p24(x0),ren20(x0)
% 0.14/0.36 % 42:3:1:INP:Top: p24(x0) -> p25(x0),ren20(x0)
% 0.14/0.36 % 43:3:1:INP:Top: p24(x0) -> p23(x0),ren21(x0)
% 0.14/0.36 % 44:3:1:INP:Top: p23(x0) -> p24(x0),ren21(x0)
% 0.14/0.36 % 45:3:1:INP:Top: p23(x0) -> p22(x0),ren22(x0)
% 0.14/0.36 % 46:3:1:INP:Top: p22(x0) -> p23(x0),ren22(x0)
% 0.14/0.36 % 47:3:1:INP:Top: p22(x0) -> p21(x0),ren23(x0)
% 0.14/0.36 % 48:3:1:INP:Top: p21(x0) -> p22(x0),ren23(x0)
% 0.14/0.36 % 49:3:1:INP:Top: p21(x0) -> p20(x0),ren24(x0)
% 0.14/0.36 % 50:3:1:INP:Top: p20(x0) -> p21(x0),ren24(x0)
% 0.14/0.36 % 51:3:1:INP:Top: p20(x0) -> p19(x0),ren25(x0)
% 0.14/0.36 % 52:3:1:INP:Top: p19(x0) -> p20(x0),ren25(x0)
% 0.14/0.36 % 53:3:1:INP:Top: p19(x0) -> p18(x0),ren26(x0)
% 0.14/0.36 % 54:3:1:INP:Top: p18(x0) -> p19(x0),ren26(x0)
% 0.14/0.36 % 55:3:1:INP:Top: p18(x0) -> p17(x0),ren27(x0)
% 0.14/0.36 % 56:3:1:INP:Top: p17(x0) -> p18(x0),ren27(x0)
% 0.14/0.36 % 57:3:1:INP:Top: p17(x0) -> p16(x0),ren28(x0)
% 0.14/0.36 % 58:3:1:INP:Top: p16(x0) -> p17(x0),ren28(x0)
% 0.14/0.36 % 59:3:1:INP:Top: p16(x0) -> p15(x0),ren29(x0)
% 0.14/0.36 % 60:3:1:INP:Top: p15(x0) -> p16(x0),ren29(x0)
% 0.14/0.36 % 61:3:1:INP:Top: p15(x0) -> p14(x0),ren30(x0)
% 0.14/0.36 % 62:3:1:INP:Top: p14(x0) -> p15(x0),ren30(x0)
% 0.14/0.36 % 63:3:1:INP:Top: p14(x0) -> p13(x0),ren31(x0)
% 0.14/0.36 % 64:3:1:INP:Top: p13(x0) -> p14(x0),ren31(x0)
% 0.14/0.36 % 65:3:1:INP:Top: p13(x0) -> p12(x0),ren32(x0)
% 0.14/0.36 % 66:3:1:INP:Top: p12(x0) -> p13(x0),ren32(x0)
% 0.14/0.36 % 67:3:1:INP:Top: p12(x0) -> p11(x0),ren33(x0)
% 0.14/0.36 % 68:3:1:INP:Top: p11(x0) -> p12(x0),ren33(x0)
% 0.14/0.36 % 69:3:1:INP:Top: p11(x0) -> p10(x0),ren34(x0)
% 0.14/0.36 % 70:3:1:INP:Top: p10(x0) -> p11(x0),ren34(x0)
% 0.14/0.36 % 71:3:1:INP:Top: p10(x0) -> p9(x0),ren35(x0)
% 0.14/0.36 % 72:3:1:INP:Top: p9(x0) -> p10(x0),ren35(x0)
% 0.14/0.36 % 73:3:1:INP:Top: p9(x0) -> p8(x0),ren36(x0)
% 0.14/0.36 % 74:3:1:INP:Top: p8(x0) -> p9(x0),ren36(x0)
% 0.14/0.36 % 75:3:1:INP:Top: p8(x0) -> p7(x0),ren37(x0)
% 0.14/0.36 % 76:3:1:INP:Top: p7(x0) -> p8(x0),ren37(x0)
% 0.14/0.36 % 77:3:1:INP:Top: p7(x0) -> p6(x0),ren38(x0)
% 0.14/0.36 % 78:3:1:INP:Top: p6(x0) -> p7(x0),ren38(x0)
% 0.14/0.36 % 79:3:1:INP:Top: p6(x0) -> p5(x0),ren39(x0)
% 0.14/0.36 % 80:3:1:INP:Top: p5(x0) -> p6(x0),ren39(x0)
% 0.14/0.36 % 81:3:1:INP:Top: p5(x0) -> p4(x0),ren40(x0)
% 0.14/0.36 % 82:3:1:INP:Top: p4(x0) -> p5(x0),ren40(x0)
% 0.14/0.36 % 83:3:1:INP:Top: p4(x0) -> p3(x0),ren41(x0)
% 0.14/0.36 % 84:3:1:INP:Top: p3(x0) -> p4(x0),ren41(x0)
% 0.14/0.36 % 85:3:1:INP:Top: p3(x0) -> p2(x0),ren42(x0)
% 0.14/0.36 % 86:3:1:INP:Top: p2(x0) -> p3(x0),ren42(x0)
% 0.14/0.36 % 87:3:1:INP:Top: p2(x0) -> p1(x0),ren43(x0)
% 0.14/0.36 % 88:3:1:INP:Top: p1(x0) -> p2(x0),ren43(x0)
% 0.14/0.36 % 89:2:1:INP:Top: -> r1(x0,skf1(x0)),ren44(x0)
% 0.14/0.36 % 90:2:1:INP:Top: -> r1(skf1(x0),skf2(x0)),ren44(x0)
% 0.14/0.36 % 91:2:1:INP:Top: -> r1(skf2(x0),skf3(x0)),ren44(x0)
% 0.14/0.36 % 92:2:1:INP:Top: -> r1(skf3(x0),skf4(x0)),ren44(x0)
% 0.14/0.36 % 93:2:1:INP:Top: -> r1(skf4(x0),skf5(x0)),ren44(x0)
% 0.14/0.36 % 94:2:1:INP:Top: -> r1(skf5(x0),skf6(x0)),ren44(x0)
% 0.14/0.36 % 95:2:1:INP:Top: -> r1(skf6(x0),skf7(x0)),ren44(x0)
% 0.14/0.36 % 96:2:1:INP:Top: -> r1(skf7(x0),skf8(x0)),ren44(x0)
% 0.14/0.36 % 97:2:1:INP:Top: -> r1(skf8(x0),skf9(x0)),ren44(x0)
% 0.14/0.36 % 98:2:1:INP:Top: -> r1(skf9(x0),skf10(x0)),ren44(x0)
% 0.14/0.36 % 99:2:1:INP:Top: -> r1(skf10(x0),skf11(x0)),ren44(x0)
% 0.14/0.36 % 100:2:1:INP:Top: -> r1(skf11(x0),skf12(x0)),ren44(x0)
% 0.14/0.36 % 101:2:1:INP:Top: -> r1(skf12(x0),skf13(x0)),ren44(x0)
% 0.14/0.36 % 102:2:1:INP:Top: -> r1(skf13(x0),skf14(x0)),ren44(x0)
% 0.14/0.36 % 103:2:1:INP:Top: -> r1(skf14(x0),skf15(x0)),ren44(x0)
% 0.14/0.36 % 104:2:1:INP:Top: -> r1(skf15(x0),skf16(x0)),ren44(x0)
% 0.14/0.36 % 105:2:1:INP:Top: -> r1(skf16(x0),skf17(x0)),ren44(x0)
% 0.14/0.36 % 106:2:1:INP:Top: -> r1(skf17(x0),skf18(x0)),ren44(x0)
% 0.14/0.36 % 107:2:1:INP:Top: -> r1(skf18(x0),skf19(x0)),ren44(x0)
% 0.14/0.36 % 108:2:1:INP:Top: -> r1(skf19(x0),skf20(x0)),ren44(x0)
% 0.14/0.36 % 109:2:1:INP:Top: -> r1(skf20(x0),skf21(x0)),ren44(x0)
% 0.14/0.36 % 110:2:1:INP:Top: -> r1(skf21(x0),skf22(x0)),ren44(x0)
% 0.14/0.36 % 111:2:1:INP:Top: -> r1(skf22(x0),skf23(x0)),ren44(x0)
% 0.14/0.36 % 112:2:1:INP:Top: -> r1(skf23(x0),skf24(x0)),ren44(x0)
% 0.14/0.36 % 113:2:1:INP:Top: -> r1(skf24(x0),skf25(x0)),ren44(x0)
% 0.14/0.36 % 114:2:1:INP:Top: -> r1(skf25(x0),skf26(x0)),ren44(x0)
% 0.14/0.36 % 115:2:1:INP:Top: -> r1(skf26(x0),skf27(x0)),ren44(x0)
% 0.14/0.36 % 116:2:1:INP:Top: -> r1(skf27(x0),skf28(x0)),ren44(x0)
% 0.14/0.36 % 117:2:1:INP:Top: -> r1(skf28(x0),skf29(x0)),ren44(x0)
% 0.14/0.36 % 118:2:1:INP:Top: -> r1(skf29(x0),skf30(x0)),ren44(x0)
% 0.14/0.36 % 119:2:1:INP:Top: -> r1(skf30(x0),skf31(x0)),ren44(x0)
% 0.14/0.36 % 120:2:1:INP:Top: -> r1(skf31(x0),skf32(x0)),ren44(x0)
% 0.14/0.36 % 121:2:1:INP:Top: -> r1(skf32(x0),skf33(x0)),ren44(x0)
% 0.14/0.36 % 122:2:1:INP:Top: -> r1(skf33(x0),skf34(x0)),ren44(x0)
% 0.14/0.36 % 123:2:1:INP:Top: -> r1(skf34(x0),skf35(x0)),ren44(x0)
% 0.14/0.36 % 124:2:1:INP:Top: -> r1(skf35(x0),skf36(x0)),ren44(x0)
% 0.14/0.36 % 125:2:1:INP:Top: -> r1(skf36(x0),skf37(x0)),ren44(x0)
% 0.14/0.36 % 126:2:1:INP:Top: -> r1(skf37(x0),skf38(x0)),ren44(x0)
% 0.14/0.36 % 127:2:1:INP:Top: -> r1(skf38(x0),skf39(x0)),ren44(x0)
% 0.14/0.36 % 128:2:1:INP:Top: -> r1(skf39(x0),skf40(x0)),ren44(x0)
% 0.14/0.36 % 129:2:1:INP:Top: -> r1(skf40(x0),skf41(x0)),ren44(x0)
% 0.14/0.36 % 130:2:1:INP:Top: -> r1(skf41(x0),skf42(x0)),ren44(x0)
% 0.14/0.36 % 131:2:1:INP:Top: -> r1(skf42(x0),skf43(x0)),ren44(x0)
% 0.14/0.36 % 132:3:2:INP:TopTop: r1(skf42(x0),x1),ren1(x1) -> ren44(x0)
% 0.14/0.36 % 133:3:2:INP:TopTop: r1(skf41(x0),x1),ren2(x1) -> ren44(x0)
% 0.14/0.36 % 134:3:2:INP:TopTop: r1(skf40(x0),x1),ren3(x1) -> ren44(x0)
% 0.14/0.36 % 135:3:2:INP:TopTop: r1(skf39(x0),x1),ren4(x1) -> ren44(x0)
% 0.14/0.36 % 136:3:2:INP:TopTop: r1(skf38(x0),x1),ren5(x1) -> ren44(x0)
% 0.14/0.36 % 137:3:2:INP:TopTop: r1(skf37(x0),x1),ren6(x1) -> ren44(x0)
% 0.14/0.36 % 138:3:2:INP:TopTop: r1(skf36(x0),x1),ren7(x1) -> ren44(x0)
% 0.14/0.36 % 139:3:2:INP:TopTop: r1(skf35(x0),x1),ren8(x1) -> ren44(x0)
% 0.14/0.36 % 140:3:2:INP:TopTop: r1(skf34(x0),x1),ren9(x1) -> ren44(x0)
% 0.14/0.36 % 141:3:2:INP:TopTop: r1(skf33(x0),x1),ren10(x1) -> ren44(x0)
% 0.14/0.36 % 142:3:2:INP:TopTop: r1(skf32(x0),x1),ren11(x1) -> ren44(x0)
% 0.14/0.36 % 143:3:2:INP:TopTop: r1(skf31(x0),x1),ren12(x1) -> ren44(x0)
% 0.14/0.36 % 144:3:2:INP:TopTop: r1(skf30(x0),x1),ren13(x1) -> ren44(x0)
% 0.14/0.36 % 145:3:2:INP:TopTop: r1(skf29(x0),x1),ren14(x1) -> ren44(x0)
% 0.14/0.36 % 146:3:2:INP:TopTop: r1(skf28(x0),x1),ren15(x1) -> ren44(x0)
% 0.14/0.36 % 147:3:2:INP:TopTop: r1(skf27(x0),x1),ren16(x1) -> ren44(x0)
% 0.14/0.36 % 148:3:2:INP:TopTop: r1(skf26(x0),x1),ren17(x1) -> ren44(x0)
% 0.14/0.36 % 149:3:2:INP:TopTop: r1(skf25(x0),x1),ren18(x1) -> ren44(x0)
% 0.14/0.36 % 150:3:2:INP:TopTop: r1(skf24(x0),x1),ren19(x1) -> ren44(x0)
% 0.14/0.36 % 151:3:2:INP:TopTop: r1(skf23(x0),x1),ren20(x1) -> ren44(x0)
% 0.14/0.36 % 152:3:2:INP:TopTop: r1(skf22(x0),x1),ren21(x1) -> ren44(x0)
% 0.14/0.36 % 153:3:2:INP:TopTop: r1(skf21(x0),x1),ren22(x1) -> ren44(x0)
% 0.14/0.36 % 154:3:2:INP:TopTop: r1(skf20(x0),x1),ren23(x1) -> ren44(x0)
% 0.14/0.36 % 155:3:2:INP:TopTop: r1(skf19(x0),x1),ren24(x1) -> ren44(x0)
% 0.14/0.36 % 156:3:2:INP:TopTop: r1(skf18(x0),x1),ren25(x1) -> ren44(x0)
% 0.14/0.36 % 157:3:2:INP:TopTop: r1(skf17(x0),x1),ren26(x1) -> ren44(x0)
% 0.14/0.36 % 158:3:2:INP:TopTop: r1(skf16(x0),x1),ren27(x1) -> ren44(x0)
% 0.14/0.36 % 159:3:2:INP:TopTop: r1(skf15(x0),x1),ren28(x1) -> ren44(x0)
% 0.14/0.36 % 160:3:2:INP:TopTop: r1(skf14(x0),x1),ren29(x1) -> ren44(x0)
% 0.14/0.36 % 161:3:2:INP:TopTop: r1(skf13(x0),x1),ren30(x1) -> ren44(x0)
% 0.14/0.36 % 162:3:2:INP:TopTop: r1(skf12(x0),x1),ren31(x1) -> ren44(x0)
% 0.14/0.36 % 163:3:2:INP:TopTop: r1(skf11(x0),x1),ren32(x1) -> ren44(x0)
% 0.14/0.36 % 164:3:2:INP:TopTop: r1(skf10(x0),x1),ren33(x1) -> ren44(x0)
% 0.14/0.36 % 165:3:2:INP:TopTop: r1(skf9(x0),x1),ren34(x1) -> ren44(x0)
% 0.14/0.36 % 166:3:2:INP:TopTop: r1(skf8(x0),x1),ren35(x1) -> ren44(x0)
% 0.14/0.36 % 167:3:2:INP:TopTop: r1(skf7(x0),x1),ren36(x1) -> ren44(x0)
% 0.14/0.36 % 168:3:2:INP:TopTop: r1(skf6(x0),x1),ren37(x1) -> ren44(x0)
% 0.14/0.36 % 169:3:2:INP:TopTop: r1(skf5(x0),x1),ren38(x1) -> ren44(x0)
% 0.14/0.36 % 170:3:2:INP:TopTop: r1(skf4(x0),x1),ren39(x1) -> ren44(x0)
% 0.14/0.36 % 171:3:2:INP:TopTop: r1(skf3(x0),x1),ren40(x1) -> ren44(x0)
% 0.14/0.36 % 172:3:2:INP:TopTop: r1(skf2(x0),x1),ren41(x1) -> ren44(x0)
% 0.14/0.36 % 173:3:2:INP:TopTop: r1(skf1(x0),x1),ren42(x1) -> ren44(x0)
% 0.14/0.36 % 174:3:2:INP:TopTop: r1(x0,x1),ren43(x1) -> ren44(x0)
% 0.14/0.36 % 175:2:1:INP:Top: -> r1(x0,skf44(x0)),ren44(x0)
% 0.14/0.36 % 176:2:1:INP:Top: p45(skf44(x0)) -> ren44(x0)
% 0.14/0.36 % 177:2:1:INP:Top: -> r1(x0,skf45(x0)),ren44(x0)
% 0.14/0.36 % 178:3:1:INP:Top: -> p43(skf45(x0)),p44(skf45(x0)),ren44(x0)
% 0.14/0.36 % 179:3:1:INP:Top: p44(skf45(x0)),p43(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 180:3:1:INP:Top: -> p42(skf45(x0)),p43(skf45(x0)),ren44(x0)
% 0.14/0.36 % 181:3:1:INP:Top: p43(skf45(x0)),p42(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 182:3:1:INP:Top: -> p41(skf45(x0)),p42(skf45(x0)),ren44(x0)
% 0.14/0.36 % 183:3:1:INP:Top: p42(skf45(x0)),p41(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 184:3:1:INP:Top: -> p40(skf45(x0)),p41(skf45(x0)),ren44(x0)
% 0.14/0.36 % 185:3:1:INP:Top: p41(skf45(x0)),p40(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 186:3:1:INP:Top: -> p39(skf45(x0)),p40(skf45(x0)),ren44(x0)
% 0.14/0.36 % 187:3:1:INP:Top: p40(skf45(x0)),p39(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 188:3:1:INP:Top: -> p38(skf45(x0)),p39(skf45(x0)),ren44(x0)
% 0.14/0.36 % 189:3:1:INP:Top: p39(skf45(x0)),p38(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 190:3:1:INP:Top: -> p37(skf45(x0)),p38(skf45(x0)),ren44(x0)
% 0.14/0.36 % 191:3:1:INP:Top: p38(skf45(x0)),p37(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 192:3:1:INP:Top: -> p36(skf45(x0)),p37(skf45(x0)),ren44(x0)
% 0.14/0.36 % 193:3:1:INP:Top: p37(skf45(x0)),p36(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 194:3:1:INP:Top: -> p35(skf45(x0)),p36(skf45(x0)),ren44(x0)
% 0.14/0.36 % 195:3:1:INP:Top: p36(skf45(x0)),p35(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 196:3:1:INP:Top: -> p34(skf45(x0)),p35(skf45(x0)),ren44(x0)
% 0.14/0.36 % 197:3:1:INP:Top: p35(skf45(x0)),p34(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 198:3:1:INP:Top: -> p33(skf45(x0)),p34(skf45(x0)),ren44(x0)
% 0.14/0.36 % 199:3:1:INP:Top: p34(skf45(x0)),p33(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 200:3:1:INP:Top: -> p32(skf45(x0)),p33(skf45(x0)),ren44(x0)
% 0.14/0.36 % 201:3:1:INP:Top: p33(skf45(x0)),p32(skf45(x0)) -> ren44(x0)
% 0.14/0.36 % 202:3:1:INP:Top: -> p31(skf45(x0)),p32(skf45(x0)),ren44(x0)
% 0.14/0.36 % 203:3:1:INP:Top: p32(skf45(x0)),p31(skf45(x0)) -> ren44(x0)
% 0.14/0.37 % 204:3:1:INP:Top: -> p30(skf45(x0)),p31(skf45(x0)),ren44(x0)
% 0.14/0.37 % 205:3:1:INP:Top: p31(skf45(x0)),p30(skf45(x0)) -> ren44(x0)
% 0.14/0.37 % 206:3:1:INP:Top: -> p29(skf45(x0)),p30(skf45(x0)),ren44(x0)
% 0.14/0.37 % 207:3:1:INP:Top: p30(skf45(x0)),p29(skf45(x0)) -> ren44(x0)
% 0.14/0.37 % 208:3:1:INP:Top: -> p28(skf45(x0)),p29(skf45(x0)),ren44(x0)
% 0.14/0.37 % 209:3:1:INP:Top: p29(skf45(x0)),p28(skf45(x0)) -> ren44(x0)
% 0.14/0.37 % 210:3:1:INP:Top: -> p27(skf45(x0)),p28(skf45(x0)),ren44(x0)
% 0.14/0.37 % 211:3:1:INP:Top: p28(skf45(x0)),p27(skf45(x0)) -> ren44(x0)
% 0.14/0.37 % 212:3:1:INP:Top: -> p26(skf45(x0)),p27(skf45(x0)),ren44(x0)
% 0.14/0.37 % 213:3:1:INP:Top: p27(skf45(x0)),p26(skf45(x0)) -> ren44(x0)
% 0.14/0.37 % 214:3:1:INP:Top: -> p25(skf45(x0)),p26(skf45(x0)),ren44(x0)
% 0.14/0.37 % 215:3:1:INP:Top: p26(skf45(x0)),p25(skf45(x0)) -> ren44(x0)
% 0.14/0.37 % 216:3:1:INP:Top: -> p24(skf45(x0)),p25(skf45(x0)),ren44(x0)
% 0.14/0.37 % 217:3:1:INP:Top: p25(skf45(x0)),p24(skf45(x0)) -> ren44(x0)
% 0.14/0.37 % 218:3:1:INP:Top: -> p23(skf45(x0)),p24(skf45(x0)),ren44(x0)
% 0.14/0.37 % 219:3:1:INP:Top: p24(skf45(x0)),p23(skf45(x0)) -> ren44(x0)
% 0.14/0.37 % 220:3:1:INP:Top: -> p22(skf45(x0)),p23(skf45(x0)),ren44(x0)
% 0.14/0.37 % 221:3:1:INP:Top: p23(skf45(x0)),p22(skf45(x0)) -> ren44(x0)
% 0.14/0.37 % 222:3:1:INP:Top: -> p21(skf45(x0)),p22(skf45(x0)),ren44(x0)
% 0.14/0.37 % 223:3:1:INP:Top: p22(skf45(x0)),p21(skf45(x0)) -> ren44(x0)
% 0.14/0.37 % 224:3:1:INP:Top: -> p20(skf45(x0)),p21(skf45(x0)),ren44(x0)
% 0.14/0.37 % 225:3:1:INP:Top: p21(skf45(x0)),p20(skf45(x0)) -> ren44(x0)
% 0.14/0.37 % 226:3:1:INP:Top: -> p19(skf45(x0)),p20(skf45(x0)),ren44(x0)
% 0.14/0.37 % 227:3:1:INP:Top: p20(skf45(x0)),p19(skf45(x0)) -> ren44(x0)
% 0.14/0.37 % 228:3:1:INP:Top: -> p18(skf45(x0)),p19(skf45(x0)),ren44(x0)
% 0.14/0.37 % 229:3:1:INP:Top: p19(skf45(x0)),p18(skf45(x0)) -> ren44(x0)
% 0.14/0.37 % 230:3:1:INP:Top: -> p17(skf45(x0)),p18(skf45(x0)),ren44(x0)
% 0.14/0.37 % 231:3:1:INP:Top: p18(skf45(x0)),p17(skf45(x0)) -> ren44(x0)
% 0.14/0.37 % 232:3:1:INP:Top: -> p16(skf45(x0)),p17(skf45(x0)),ren44(x0)
% 0.14/0.37 % 233:3:1:INP:Top: p17(skf45(x0)),p16(skf45(x0)) -> ren44(x0)
% 0.14/0.37 % 234:3:1:INP:Top: -> p15(skf45(x0)),p16(skf45(x0)),ren44(x0)
% 0.14/0.37 % 235:3:1:INP:Top: p16(skf45(x0)),p15(skf45(x0)) -> ren44(x0)
% 0.14/0.37 % 236:3:1:INP:Top: -> p14(skf45(x0)),p15(skf45(x0)),ren44(x0)
% 182.47/182.74 % 237:3:1:INP:Top: p15(skf45(x0)),p14(skf45(x0)) -> ren44(x0)
% 182.47/182.74 % 238:3:1:INP:Top: -> p13(skf45(x0)),p14(skf45(x0)),ren44(x0)
% 182.47/182.74 % 239:3:1:INP:Top: p14(skf45(x0)),p13(skf45(x0)) -> ren44(x0)
% 182.47/182.74 % 240:3:1:INP:Top: -> p12(skf45(x0)),p13(skf45(x0)),ren44(x0)
% 182.47/182.74 % 241:3:1:INP:Top: p13(skf45(x0)),p12(skf45(x0)) -> ren44(x0)
% 182.47/182.74 % 242:3:1:INP:Top: -> p11(skf45(x0)),p12(skf45(x0)),ren44(x0)
% 182.47/182.74 % 243:3:1:INP:Top: p12(skf45(x0)),p11(skf45(x0)) -> ren44(x0)
% 182.47/182.74 % 244:3:1:INP:Top: -> p10(skf45(x0)),p11(skf45(x0)),ren44(x0)
% 182.47/182.74 % 245:3:1:INP:Top: p11(skf45(x0)),p10(skf45(x0)) -> ren44(x0)
% 182.47/182.74 % 246:3:1:INP:Top: -> p9(skf45(x0)),p10(skf45(x0)),ren44(x0)
% 182.47/182.74 % 247:3:1:INP:Top: p10(skf45(x0)),p9(skf45(x0)) -> ren44(x0)
% 182.47/182.74 % 248:3:1:INP:Top: -> p8(skf45(x0)),p9(skf45(x0)),ren44(x0)
% 182.47/182.74 % 249:3:1:INP:Top: p9(skf45(x0)),p8(skf45(x0)) -> ren44(x0)
% 182.47/182.74 % 250:3:1:INP:Top: -> p7(skf45(x0)),p8(skf45(x0)),ren44(x0)
% 182.47/182.74 % 251:3:1:INP:Top: p8(skf45(x0)),p7(skf45(x0)) -> ren44(x0)
% 182.47/182.74 % 252:3:1:INP:Top: -> p6(skf45(x0)),p7(skf45(x0)),ren44(x0)
% 182.47/182.74 % 253:3:1:INP:Top: p7(skf45(x0)),p6(skf45(x0)) -> ren44(x0)
% 182.47/182.74 % 254:3:1:INP:Top: -> p5(skf45(x0)),p6(skf45(x0)),ren44(x0)
% 182.47/182.74 % 255:3:1:INP:Top: p6(skf45(x0)),p5(skf45(x0)) -> ren44(x0)
% 182.47/182.74 % 256:3:1:INP:Top: -> p4(skf45(x0)),p5(skf45(x0)),ren44(x0)
% 182.47/182.74 % 257:3:1:INP:Top: p5(skf45(x0)),p4(skf45(x0)) -> ren44(x0)
% 182.47/182.74 % 258:3:1:INP:Top: -> p3(skf45(x0)),p4(skf45(x0)),ren44(x0)
% 182.47/182.74 % 259:3:1:INP:Top: p4(skf45(x0)),p3(skf45(x0)) -> ren44(x0)
% 182.47/182.74 % 260:3:1:INP:Top: -> p2(skf45(x0)),p3(skf45(x0)),ren44(x0)
% 182.47/182.74 % 261:3:1:INP:Top: p3(skf45(x0)),p2(skf45(x0)) -> ren44(x0)
% 182.47/182.74 % 262:3:1:INP:Top: -> p1(skf45(x0)),p2(skf45(x0)),ren44(x0)
% 182.47/182.74 % 263:3:1:INP:Top: p2(skf45(x0)),p1(skf45(x0)) -> ren44(x0)
% 182.47/182.74
% 182.47/182.74 % Reduced Input Conjecture Clauses:
% 182.47/182.74 % 264:1:0:INP:: -> r1(skc46,skc47)
% 182.47/182.74 % 265:1:0:INP:: -> p45(skc47)
% 182.47/182.74 % 266:1:0:INP:: -> r1(skc47,skc48)
% 182.47/182.74 % 267:1:0:INP:: -> p1(skc48)
% 182.47/182.74 % 268:1:0:INP:: -> r1(skc46,skc49)
% 182.47/182.74 % 269:2:1:INP:Top: r1(skc49,x0),ren44(x0) ->
% 182.47/182.74
% 182.47/182.74
% 182.47/182.74 % === Starting SPASS-SCL-FOL A Little Less Naive, considering 748 atoms initially. Used heuristic: lmodel_grow ===
% 182.47/182.74
% 182.47/182.74
% 182.47/182.74
% 182.47/182.74 % SZS status Theorem
% 182.47/182.74 % Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 182.47/182.74
% 182.47/182.74 % SPASS-SCL-FOL Statistics:
% 182.47/182.74 % Number of learned clauses: 51
% 182.47/182.74 % Number of propagations: 26358
% 182.47/182.74 % Number of decisions: 10216
% 182.47/182.74 % Number of resolutions: 59
% 182.47/182.74 % Number of condensations: 0
% 182.47/182.74 % Number of sub resolutions: 2
% 182.47/182.74
% 182.47/182.74 % Solver is done. Empty clause found
% 182.47/182.74
% 182.47/182.74 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 182.47/182.74 % SZS output start Proof for theBenchmark
% See solution above
% 182.47/182.75 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 182.47/182.75
% 182.47/182.75
% 182.47/182.75 % Needed: 0:03:02.38
% 182.47/182.75
% 182.47/182.75 % ###
% 182.47/182.75 % ### Pagesize: 8192
% 182.47/182.75 % ### Marksize: 0
% 182.47/182.75 % ### Memory demanded: 214834 KBytes
% 182.47/182.75 % ### Memory freed: 214834 KBytes
% 182.47/182.75 % ### Memory remaining: 0 Bytes
% 182.47/182.75 % ### Pages allocated: 8323 Pages
% 182.47/182.75 % ###
%------------------------------------------------------------------------------