%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL650+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.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 : Tue Sep 29 11:54:08 AM UTC 2026
% Result : Theorem 11.82s 2.82s
% Output : Refutation 14.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 23
% Syntax : Number of formulae : 424 ( 44 unt; 22 def)
% Number of atoms : 4964 ( 0 equ)
% Maximal formula atoms : 289 ( 11 avg)
% Number of connectives : 8523 (3983 ~;3861 |; 661 &)
% ( 18 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 88 ( 13 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 49 ( 48 usr; 19 prp; 0-2 aty)
% Number of functors : 48 ( 48 usr; 34 con; 0-1 aty)
% Number of variables : 3199 ( 0 sgn3039 !; 160 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ ? [X0] :
~ ( ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( ~ p32(X0)
& ~ p30(X0)
& ~ p28(X0)
& ~ p26(X0)
& ~ p24(X0)
& ~ p22(X0)
& ~ p20(X0)
& ~ p18(X0)
& ~ p16(X0)
& ~ p14(X0)
& ~ p12(X0)
& ~ p10(X0)
& ~ p8(X0)
& ~ p6(X0)
& ~ p4(X0)
& ~ p2(X0) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p17(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p15(X0)
& ~ p1(X0) )
| ( p1(X0)
& p15(X0) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X0] :
( ~ r1(X1,X0)
| p16(X0) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p14(X0)
& ~ p15(X0) )
| ( p15(X0)
& p14(X0) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p15(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p13(X0)
& ~ p14(X0) )
| ( p14(X0)
& p13(X0) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X0] :
( ~ r1(X1,X0)
| p14(X0) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p12(X0)
& ~ p13(X0) )
| ( p13(X0)
& p12(X0) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p13(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p11(X0)
& ~ p12(X0) )
| ( p12(X0)
& p11(X0) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X0] :
( ~ r1(X1,X0)
| p12(X0) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p10(X0)
& ~ p11(X0) )
| ( p11(X0)
& p10(X0) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p11(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p9(X0)
& ~ p10(X0) )
| ( p10(X0)
& p9(X0) ) ) ) ) ) ) ) ) ) ) )
| ! [X0] :
( ~ r1(X1,X0)
| p10(X0) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p8(X0)
& ~ p9(X0) )
| ( p9(X0)
& p8(X0) ) ) ) ) ) ) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p9(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p7(X0)
& ~ p8(X0) )
| ( p8(X0)
& p7(X0) ) ) ) ) ) ) ) ) )
| ! [X0] :
( ~ r1(X1,X0)
| p8(X0) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p6(X0)
& ~ p7(X0) )
| ( p7(X0)
& p6(X0) ) ) ) ) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p7(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p5(X0)
& ~ p6(X0) )
| ( p6(X0)
& p5(X0) ) ) ) ) ) ) )
| ! [X0] :
( ~ r1(X1,X0)
| p6(X0) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p4(X0)
& ~ p5(X0) )
| ( p5(X0)
& p4(X0) ) ) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p5(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p3(X0)
& ~ p4(X0) )
| ( p4(X0)
& p3(X0) ) ) ) ) )
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p2(X0)
& ~ p3(X0) )
| ( p3(X0)
& p2(X0) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p3(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p1(X0)
& ~ p2(X0) )
| ( p2(X0)
& p1(X0) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( p16(X0)
& p15(X0)
& p14(X0)
& p13(X0)
& p12(X0)
& p11(X0)
& p10(X0)
& p9(X0)
& p8(X0)
& p7(X0)
& p6(X0)
& p5(X0)
& p4(X0)
& p3(X0)
& p2(X0)
& p1(X0) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',main) ).
fof(f2,negated_conjecture,
~ ~ ? [X0] :
~ ( ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( ~ p32(X0)
& ~ p30(X0)
& ~ p28(X0)
& ~ p26(X0)
& ~ p24(X0)
& ~ p22(X0)
& ~ p20(X0)
& ~ p18(X0)
& ~ p16(X0)
& ~ p14(X0)
& ~ p12(X0)
& ~ p10(X0)
& ~ p8(X0)
& ~ p6(X0)
& ~ p4(X0)
& ~ p2(X0) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p17(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p15(X0)
& ~ p1(X0) )
| ( p1(X0)
& p15(X0) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X0] :
( ~ r1(X1,X0)
| p16(X0) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p14(X0)
& ~ p15(X0) )
| ( p15(X0)
& p14(X0) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p15(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p13(X0)
& ~ p14(X0) )
| ( p14(X0)
& p13(X0) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X0] :
( ~ r1(X1,X0)
| p14(X0) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p12(X0)
& ~ p13(X0) )
| ( p13(X0)
& p12(X0) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p13(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p11(X0)
& ~ p12(X0) )
| ( p12(X0)
& p11(X0) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X0] :
( ~ r1(X1,X0)
| p12(X0) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p10(X0)
& ~ p11(X0) )
| ( p11(X0)
& p10(X0) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p11(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p9(X0)
& ~ p10(X0) )
| ( p10(X0)
& p9(X0) ) ) ) ) ) ) ) ) ) ) )
| ! [X0] :
( ~ r1(X1,X0)
| p10(X0) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p8(X0)
& ~ p9(X0) )
| ( p9(X0)
& p8(X0) ) ) ) ) ) ) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p9(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p7(X0)
& ~ p8(X0) )
| ( p8(X0)
& p7(X0) ) ) ) ) ) ) ) ) )
| ! [X0] :
( ~ r1(X1,X0)
| p8(X0) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p6(X0)
& ~ p7(X0) )
| ( p7(X0)
& p6(X0) ) ) ) ) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p7(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p5(X0)
& ~ p6(X0) )
| ( p6(X0)
& p5(X0) ) ) ) ) ) ) )
| ! [X0] :
( ~ r1(X1,X0)
| p6(X0) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p4(X0)
& ~ p5(X0) )
| ( p5(X0)
& p4(X0) ) ) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p5(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p3(X0)
& ~ p4(X0) )
| ( p4(X0)
& p3(X0) ) ) ) ) )
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p2(X0)
& ~ p3(X0) )
| ( p3(X0)
& p2(X0) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p3(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p1(X0)
& ~ p2(X0) )
| ( p2(X0)
& p1(X0) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( p16(X0)
& p15(X0)
& p14(X0)
& p13(X0)
& p12(X0)
& p11(X0)
& p10(X0)
& p9(X0)
& p8(X0)
& p7(X0)
& p6(X0)
& p5(X0)
& p4(X0)
& p3(X0)
& p2(X0)
& p1(X0) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
~ ~ ? [X0] :
~ ( ! [X1] :
( ~ r1(X0,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)
| ( ~ p32(X16)
& ~ p30(X16)
& ~ p28(X16)
& ~ p26(X16)
& ~ p24(X16)
& ~ p22(X16)
& ~ p20(X16)
& ~ p18(X16)
& ~ p16(X16)
& ~ p14(X16)
& ~ p12(X16)
& ~ p10(X16)
& ~ p8(X16)
& ~ p6(X16)
& ~ p4(X16)
& ~ p2(X16) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X17] :
( ~ r1(X0,X17)
| p17(X17) )
| ~ ! [X18] :
( ~ r1(X0,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)
| ~ ( ( ~ p15(X33)
& ~ p1(X33) )
| ( p1(X33)
& p15(X33) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X34] :
( ~ r1(X18,X34)
| p16(X34) )
| ~ ! [X35] :
( ~ r1(X18,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(X48,X49)
| ~ ( ( ~ p14(X49)
& ~ p15(X49) )
| ( p15(X49)
& p14(X49) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X50] :
( ~ r1(X35,X50)
| p15(X50) )
| ~ ! [X51] :
( ~ r1(X35,X51)
| ~ ( ~ ! [X52] :
( ~ r1(X51,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ! [X58] :
( ~ r1(X57,X58)
| ! [X59] :
( ~ r1(X58,X59)
| ! [X60] :
( ~ r1(X59,X60)
| ! [X61] :
( ~ r1(X60,X61)
| ! [X62] :
( ~ r1(X61,X62)
| ! [X63] :
( ~ r1(X62,X63)
| ! [X64] :
( ~ r1(X63,X64)
| ~ ( ( ~ p13(X64)
& ~ p14(X64) )
| ( p14(X64)
& p13(X64) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X65] :
( ~ r1(X51,X65)
| p14(X65) )
| ~ ! [X66] :
( ~ r1(X51,X66)
| ~ ( ~ ! [X67] :
( ~ r1(X66,X67)
| ! [X68] :
( ~ r1(X67,X68)
| ! [X69] :
( ~ r1(X68,X69)
| ! [X70] :
( ~ r1(X69,X70)
| ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| ! [X73] :
( ~ r1(X72,X73)
| ! [X74] :
( ~ r1(X73,X74)
| ! [X75] :
( ~ r1(X74,X75)
| ! [X76] :
( ~ r1(X75,X76)
| ! [X77] :
( ~ r1(X76,X77)
| ! [X78] :
( ~ r1(X77,X78)
| ~ ( ( ~ p12(X78)
& ~ p13(X78) )
| ( p13(X78)
& p12(X78) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X79] :
( ~ r1(X66,X79)
| p13(X79) )
| ~ ! [X80] :
( ~ r1(X66,X80)
| ~ ( ~ ! [X81] :
( ~ r1(X80,X81)
| ! [X82] :
( ~ r1(X81,X82)
| ! [X83] :
( ~ r1(X82,X83)
| ! [X84] :
( ~ r1(X83,X84)
| ! [X85] :
( ~ r1(X84,X85)
| ! [X86] :
( ~ r1(X85,X86)
| ! [X87] :
( ~ r1(X86,X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ! [X90] :
( ~ r1(X89,X90)
| ! [X91] :
( ~ r1(X90,X91)
| ~ ( ( ~ p11(X91)
& ~ p12(X91) )
| ( p12(X91)
& p11(X91) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X92] :
( ~ r1(X80,X92)
| p12(X92) )
| ~ ! [X93] :
( ~ r1(X80,X93)
| ~ ( ~ ! [X94] :
( ~ r1(X93,X94)
| ! [X95] :
( ~ r1(X94,X95)
| ! [X96] :
( ~ r1(X95,X96)
| ! [X97] :
( ~ r1(X96,X97)
| ! [X98] :
( ~ r1(X97,X98)
| ! [X99] :
( ~ r1(X98,X99)
| ! [X100] :
( ~ r1(X99,X100)
| ! [X101] :
( ~ r1(X100,X101)
| ! [X102] :
( ~ r1(X101,X102)
| ! [X103] :
( ~ r1(X102,X103)
| ~ ( ( ~ p10(X103)
& ~ p11(X103) )
| ( p11(X103)
& p10(X103) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X104] :
( ~ r1(X93,X104)
| p11(X104) )
| ~ ! [X105] :
( ~ r1(X93,X105)
| ~ ( ~ ! [X106] :
( ~ r1(X105,X106)
| ! [X107] :
( ~ r1(X106,X107)
| ! [X108] :
( ~ r1(X107,X108)
| ! [X109] :
( ~ r1(X108,X109)
| ! [X110] :
( ~ r1(X109,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ! [X114] :
( ~ r1(X113,X114)
| ~ ( ( ~ p9(X114)
& ~ p10(X114) )
| ( p10(X114)
& p9(X114) ) ) ) ) ) ) ) ) ) ) )
| ! [X115] :
( ~ r1(X105,X115)
| p10(X115) )
| ~ ! [X116] :
( ~ r1(X105,X116)
| ~ ( ~ ! [X117] :
( ~ r1(X116,X117)
| ! [X118] :
( ~ r1(X117,X118)
| ! [X119] :
( ~ r1(X118,X119)
| ! [X120] :
( ~ r1(X119,X120)
| ! [X121] :
( ~ r1(X120,X121)
| ! [X122] :
( ~ r1(X121,X122)
| ! [X123] :
( ~ r1(X122,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ~ ( ( ~ p8(X124)
& ~ p9(X124) )
| ( p9(X124)
& p8(X124) ) ) ) ) ) ) ) ) ) )
| ! [X125] :
( ~ r1(X116,X125)
| p9(X125) )
| ~ ! [X126] :
( ~ r1(X116,X126)
| ~ ( ~ ! [X127] :
( ~ r1(X126,X127)
| ! [X128] :
( ~ r1(X127,X128)
| ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| ! [X131] :
( ~ r1(X130,X131)
| ! [X132] :
( ~ r1(X131,X132)
| ! [X133] :
( ~ r1(X132,X133)
| ~ ( ( ~ p7(X133)
& ~ p8(X133) )
| ( p8(X133)
& p7(X133) ) ) ) ) ) ) ) ) )
| ! [X134] :
( ~ r1(X126,X134)
| p8(X134) )
| ~ ! [X135] :
( ~ r1(X126,X135)
| ~ ( ~ ! [X136] :
( ~ r1(X135,X136)
| ! [X137] :
( ~ r1(X136,X137)
| ! [X138] :
( ~ r1(X137,X138)
| ! [X139] :
( ~ r1(X138,X139)
| ! [X140] :
( ~ r1(X139,X140)
| ! [X141] :
( ~ r1(X140,X141)
| ~ ( ( ~ p6(X141)
& ~ p7(X141) )
| ( p7(X141)
& p6(X141) ) ) ) ) ) ) ) )
| ! [X142] :
( ~ r1(X135,X142)
| p7(X142) )
| ~ ! [X143] :
( ~ r1(X135,X143)
| ~ ( ~ ! [X144] :
( ~ r1(X143,X144)
| ! [X145] :
( ~ r1(X144,X145)
| ! [X146] :
( ~ r1(X145,X146)
| ! [X147] :
( ~ r1(X146,X147)
| ! [X148] :
( ~ r1(X147,X148)
| ~ ( ( ~ p5(X148)
& ~ p6(X148) )
| ( p6(X148)
& p5(X148) ) ) ) ) ) ) )
| ! [X149] :
( ~ r1(X143,X149)
| p6(X149) )
| ~ ! [X150] :
( ~ r1(X143,X150)
| ~ ( ~ ! [X151] :
( ~ r1(X150,X151)
| ! [X152] :
( ~ r1(X151,X152)
| ! [X153] :
( ~ r1(X152,X153)
| ! [X154] :
( ~ r1(X153,X154)
| ~ ( ( ~ p4(X154)
& ~ p5(X154) )
| ( p5(X154)
& p4(X154) ) ) ) ) ) )
| ! [X155] :
( ~ r1(X150,X155)
| p5(X155) )
| ~ ! [X156] :
( ~ r1(X150,X156)
| ~ ( ~ ! [X157] :
( ~ r1(X156,X157)
| ! [X158] :
( ~ r1(X157,X158)
| ! [X159] :
( ~ r1(X158,X159)
| ~ ( ( ~ p3(X159)
& ~ p4(X159) )
| ( p4(X159)
& p3(X159) ) ) ) ) )
| ! [X160] :
( ~ r1(X156,X160)
| p4(X160) )
| ~ ! [X161] :
( ~ r1(X156,X161)
| ~ ( ~ ! [X162] :
( ~ r1(X161,X162)
| ! [X163] :
( ~ r1(X162,X163)
| ~ ( ( ~ p2(X163)
& ~ p3(X163) )
| ( p3(X163)
& p2(X163) ) ) ) )
| ! [X164] :
( ~ r1(X161,X164)
| p3(X164) )
| ~ ! [X165] :
( ~ r1(X161,X165)
| ~ ~ ! [X166] :
( ~ r1(X165,X166)
| ~ ( ( ~ p1(X166)
& ~ p2(X166) )
| ( p2(X166)
& p1(X166) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X167] :
( ~ r1(X0,X167)
| ! [X168] :
( ~ r1(X167,X168)
| ! [X169] :
( ~ r1(X168,X169)
| ! [X170] :
( ~ r1(X169,X170)
| ! [X171] :
( ~ r1(X170,X171)
| ! [X172] :
( ~ r1(X171,X172)
| ! [X173] :
( ~ r1(X172,X173)
| ! [X174] :
( ~ r1(X173,X174)
| ! [X175] :
( ~ r1(X174,X175)
| ! [X176] :
( ~ r1(X175,X176)
| ! [X177] :
( ~ r1(X176,X177)
| ! [X178] :
( ~ r1(X177,X178)
| ! [X179] :
( ~ r1(X178,X179)
| ! [X180] :
( ~ r1(X179,X180)
| ! [X181] :
( ~ r1(X180,X181)
| ! [X182] :
( ~ r1(X181,X182)
| ( p16(X182)
& p15(X182)
& p14(X182)
& p13(X182)
& p12(X182)
& p11(X182)
& p10(X182)
& p9(X182)
& p8(X182)
& p7(X182)
& p6(X182)
& p5(X182)
& p4(X182)
& p3(X182)
& p2(X182)
& p1(X182) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f2]) ).
fof(f4,plain,
? [X0] :
~ ( ! [X1] :
( ~ r1(X0,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)
| ( ~ p32(X16)
& ~ p30(X16)
& ~ p28(X16)
& ~ p26(X16)
& ~ p24(X16)
& ~ p22(X16)
& ~ p20(X16)
& ~ p18(X16)
& ~ p16(X16)
& ~ p14(X16)
& ~ p12(X16)
& ~ p10(X16)
& ~ p8(X16)
& ~ p6(X16)
& ~ p4(X16)
& ~ p2(X16) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X17] :
( ~ r1(X0,X17)
| p17(X17) )
| ~ ! [X18] :
( ~ r1(X0,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)
| ~ ( ( ~ p15(X33)
& ~ p1(X33) )
| ( p1(X33)
& p15(X33) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X34] :
( ~ r1(X18,X34)
| p16(X34) )
| ~ ! [X35] :
( ~ r1(X18,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(X48,X49)
| ~ ( ( ~ p14(X49)
& ~ p15(X49) )
| ( p15(X49)
& p14(X49) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X50] :
( ~ r1(X35,X50)
| p15(X50) )
| ~ ! [X51] :
( ~ r1(X35,X51)
| ~ ( ~ ! [X52] :
( ~ r1(X51,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ! [X58] :
( ~ r1(X57,X58)
| ! [X59] :
( ~ r1(X58,X59)
| ! [X60] :
( ~ r1(X59,X60)
| ! [X61] :
( ~ r1(X60,X61)
| ! [X62] :
( ~ r1(X61,X62)
| ! [X63] :
( ~ r1(X62,X63)
| ! [X64] :
( ~ r1(X63,X64)
| ~ ( ( ~ p13(X64)
& ~ p14(X64) )
| ( p14(X64)
& p13(X64) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X65] :
( ~ r1(X51,X65)
| p14(X65) )
| ~ ! [X66] :
( ~ r1(X51,X66)
| ~ ( ~ ! [X67] :
( ~ r1(X66,X67)
| ! [X68] :
( ~ r1(X67,X68)
| ! [X69] :
( ~ r1(X68,X69)
| ! [X70] :
( ~ r1(X69,X70)
| ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| ! [X73] :
( ~ r1(X72,X73)
| ! [X74] :
( ~ r1(X73,X74)
| ! [X75] :
( ~ r1(X74,X75)
| ! [X76] :
( ~ r1(X75,X76)
| ! [X77] :
( ~ r1(X76,X77)
| ! [X78] :
( ~ r1(X77,X78)
| ~ ( ( ~ p12(X78)
& ~ p13(X78) )
| ( p13(X78)
& p12(X78) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X79] :
( ~ r1(X66,X79)
| p13(X79) )
| ~ ! [X80] :
( ~ r1(X66,X80)
| ~ ( ~ ! [X81] :
( ~ r1(X80,X81)
| ! [X82] :
( ~ r1(X81,X82)
| ! [X83] :
( ~ r1(X82,X83)
| ! [X84] :
( ~ r1(X83,X84)
| ! [X85] :
( ~ r1(X84,X85)
| ! [X86] :
( ~ r1(X85,X86)
| ! [X87] :
( ~ r1(X86,X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ! [X90] :
( ~ r1(X89,X90)
| ! [X91] :
( ~ r1(X90,X91)
| ~ ( ( ~ p11(X91)
& ~ p12(X91) )
| ( p12(X91)
& p11(X91) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X92] :
( ~ r1(X80,X92)
| p12(X92) )
| ~ ! [X93] :
( ~ r1(X80,X93)
| ~ ( ~ ! [X94] :
( ~ r1(X93,X94)
| ! [X95] :
( ~ r1(X94,X95)
| ! [X96] :
( ~ r1(X95,X96)
| ! [X97] :
( ~ r1(X96,X97)
| ! [X98] :
( ~ r1(X97,X98)
| ! [X99] :
( ~ r1(X98,X99)
| ! [X100] :
( ~ r1(X99,X100)
| ! [X101] :
( ~ r1(X100,X101)
| ! [X102] :
( ~ r1(X101,X102)
| ! [X103] :
( ~ r1(X102,X103)
| ~ ( ( ~ p10(X103)
& ~ p11(X103) )
| ( p11(X103)
& p10(X103) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X104] :
( ~ r1(X93,X104)
| p11(X104) )
| ~ ! [X105] :
( ~ r1(X93,X105)
| ~ ( ~ ! [X106] :
( ~ r1(X105,X106)
| ! [X107] :
( ~ r1(X106,X107)
| ! [X108] :
( ~ r1(X107,X108)
| ! [X109] :
( ~ r1(X108,X109)
| ! [X110] :
( ~ r1(X109,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ! [X114] :
( ~ r1(X113,X114)
| ~ ( ( ~ p9(X114)
& ~ p10(X114) )
| ( p10(X114)
& p9(X114) ) ) ) ) ) ) ) ) ) ) )
| ! [X115] :
( ~ r1(X105,X115)
| p10(X115) )
| ~ ! [X116] :
( ~ r1(X105,X116)
| ~ ( ~ ! [X117] :
( ~ r1(X116,X117)
| ! [X118] :
( ~ r1(X117,X118)
| ! [X119] :
( ~ r1(X118,X119)
| ! [X120] :
( ~ r1(X119,X120)
| ! [X121] :
( ~ r1(X120,X121)
| ! [X122] :
( ~ r1(X121,X122)
| ! [X123] :
( ~ r1(X122,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ~ ( ( ~ p8(X124)
& ~ p9(X124) )
| ( p9(X124)
& p8(X124) ) ) ) ) ) ) ) ) ) )
| ! [X125] :
( ~ r1(X116,X125)
| p9(X125) )
| ~ ! [X126] :
( ~ r1(X116,X126)
| ~ ( ~ ! [X127] :
( ~ r1(X126,X127)
| ! [X128] :
( ~ r1(X127,X128)
| ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| ! [X131] :
( ~ r1(X130,X131)
| ! [X132] :
( ~ r1(X131,X132)
| ! [X133] :
( ~ r1(X132,X133)
| ~ ( ( ~ p7(X133)
& ~ p8(X133) )
| ( p8(X133)
& p7(X133) ) ) ) ) ) ) ) ) )
| ! [X134] :
( ~ r1(X126,X134)
| p8(X134) )
| ~ ! [X135] :
( ~ r1(X126,X135)
| ~ ( ~ ! [X136] :
( ~ r1(X135,X136)
| ! [X137] :
( ~ r1(X136,X137)
| ! [X138] :
( ~ r1(X137,X138)
| ! [X139] :
( ~ r1(X138,X139)
| ! [X140] :
( ~ r1(X139,X140)
| ! [X141] :
( ~ r1(X140,X141)
| ~ ( ( ~ p6(X141)
& ~ p7(X141) )
| ( p7(X141)
& p6(X141) ) ) ) ) ) ) ) )
| ! [X142] :
( ~ r1(X135,X142)
| p7(X142) )
| ~ ! [X143] :
( ~ r1(X135,X143)
| ~ ( ~ ! [X144] :
( ~ r1(X143,X144)
| ! [X145] :
( ~ r1(X144,X145)
| ! [X146] :
( ~ r1(X145,X146)
| ! [X147] :
( ~ r1(X146,X147)
| ! [X148] :
( ~ r1(X147,X148)
| ~ ( ( ~ p5(X148)
& ~ p6(X148) )
| ( p6(X148)
& p5(X148) ) ) ) ) ) ) )
| ! [X149] :
( ~ r1(X143,X149)
| p6(X149) )
| ~ ! [X150] :
( ~ r1(X143,X150)
| ~ ( ~ ! [X151] :
( ~ r1(X150,X151)
| ! [X152] :
( ~ r1(X151,X152)
| ! [X153] :
( ~ r1(X152,X153)
| ! [X154] :
( ~ r1(X153,X154)
| ~ ( ( ~ p4(X154)
& ~ p5(X154) )
| ( p5(X154)
& p4(X154) ) ) ) ) ) )
| ! [X155] :
( ~ r1(X150,X155)
| p5(X155) )
| ~ ! [X156] :
( ~ r1(X150,X156)
| ~ ( ~ ! [X157] :
( ~ r1(X156,X157)
| ! [X158] :
( ~ r1(X157,X158)
| ! [X159] :
( ~ r1(X158,X159)
| ~ ( ( ~ p3(X159)
& ~ p4(X159) )
| ( p4(X159)
& p3(X159) ) ) ) ) )
| ! [X160] :
( ~ r1(X156,X160)
| p4(X160) )
| ~ ! [X161] :
( ~ r1(X156,X161)
| ~ ( ~ ! [X162] :
( ~ r1(X161,X162)
| ! [X163] :
( ~ r1(X162,X163)
| ~ ( ( ~ p2(X163)
& ~ p3(X163) )
| ( p3(X163)
& p2(X163) ) ) ) )
| ! [X164] :
( ~ r1(X161,X164)
| p3(X164) )
| ~ ! [X165] :
( ~ r1(X161,X165)
| ! [X166] :
( ~ r1(X165,X166)
| ~ ( ( ~ p1(X166)
& ~ p2(X166) )
| ( p2(X166)
& p1(X166) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X167] :
( ~ r1(X0,X167)
| ! [X168] :
( ~ r1(X167,X168)
| ! [X169] :
( ~ r1(X168,X169)
| ! [X170] :
( ~ r1(X169,X170)
| ! [X171] :
( ~ r1(X170,X171)
| ! [X172] :
( ~ r1(X171,X172)
| ! [X173] :
( ~ r1(X172,X173)
| ! [X174] :
( ~ r1(X173,X174)
| ! [X175] :
( ~ r1(X174,X175)
| ! [X176] :
( ~ r1(X175,X176)
| ! [X177] :
( ~ r1(X176,X177)
| ! [X178] :
( ~ r1(X177,X178)
| ! [X179] :
( ~ r1(X178,X179)
| ! [X180] :
( ~ r1(X179,X180)
| ! [X181] :
( ~ r1(X180,X181)
| ! [X182] :
( ~ r1(X181,X182)
| ( p16(X182)
& p15(X182)
& p14(X182)
& p13(X182)
& p12(X182)
& p11(X182)
& p10(X182)
& p9(X182)
& p8(X182)
& p7(X182)
& p6(X182)
& p5(X182)
& p4(X182)
& p3(X182)
& p2(X182)
& p1(X182) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(flattening,[],[f3]) ).
fof(f5,plain,
? [X0] :
( ? [X1] :
( r1(X0,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)
& ( p32(X16)
| p30(X16)
| p28(X16)
| p26(X16)
| p24(X16)
| p22(X16)
| p20(X16)
| p18(X16)
| p16(X16)
| p14(X16)
| p12(X16)
| p10(X16)
| p8(X16)
| p6(X16)
| p4(X16)
| p2(X16) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X17] :
( r1(X0,X17)
& ~ p17(X17) )
& ! [X18] :
( ~ r1(X0,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)
| ( ( p15(X33)
| p1(X33) )
& ( ~ p1(X33)
| ~ p15(X33) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X34] :
( r1(X18,X34)
& ~ p16(X34) )
& ! [X35] :
( ~ r1(X18,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(X48,X49)
| ( ( p14(X49)
| p15(X49) )
& ( ~ p15(X49)
| ~ p14(X49) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X50] :
( r1(X35,X50)
& ~ p15(X50) )
& ! [X51] :
( ~ r1(X35,X51)
| ( ! [X52] :
( ~ r1(X51,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ! [X58] :
( ~ r1(X57,X58)
| ! [X59] :
( ~ r1(X58,X59)
| ! [X60] :
( ~ r1(X59,X60)
| ! [X61] :
( ~ r1(X60,X61)
| ! [X62] :
( ~ r1(X61,X62)
| ! [X63] :
( ~ r1(X62,X63)
| ! [X64] :
( ~ r1(X63,X64)
| ( ( p13(X64)
| p14(X64) )
& ( ~ p14(X64)
| ~ p13(X64) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X65] :
( r1(X51,X65)
& ~ p14(X65) )
& ! [X66] :
( ~ r1(X51,X66)
| ( ! [X67] :
( ~ r1(X66,X67)
| ! [X68] :
( ~ r1(X67,X68)
| ! [X69] :
( ~ r1(X68,X69)
| ! [X70] :
( ~ r1(X69,X70)
| ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| ! [X73] :
( ~ r1(X72,X73)
| ! [X74] :
( ~ r1(X73,X74)
| ! [X75] :
( ~ r1(X74,X75)
| ! [X76] :
( ~ r1(X75,X76)
| ! [X77] :
( ~ r1(X76,X77)
| ! [X78] :
( ~ r1(X77,X78)
| ( ( p12(X78)
| p13(X78) )
& ( ~ p13(X78)
| ~ p12(X78) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X79] :
( r1(X66,X79)
& ~ p13(X79) )
& ! [X80] :
( ~ r1(X66,X80)
| ( ! [X81] :
( ~ r1(X80,X81)
| ! [X82] :
( ~ r1(X81,X82)
| ! [X83] :
( ~ r1(X82,X83)
| ! [X84] :
( ~ r1(X83,X84)
| ! [X85] :
( ~ r1(X84,X85)
| ! [X86] :
( ~ r1(X85,X86)
| ! [X87] :
( ~ r1(X86,X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ! [X90] :
( ~ r1(X89,X90)
| ! [X91] :
( ~ r1(X90,X91)
| ( ( p11(X91)
| p12(X91) )
& ( ~ p12(X91)
| ~ p11(X91) ) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X92] :
( r1(X80,X92)
& ~ p12(X92) )
& ! [X93] :
( ~ r1(X80,X93)
| ( ! [X94] :
( ~ r1(X93,X94)
| ! [X95] :
( ~ r1(X94,X95)
| ! [X96] :
( ~ r1(X95,X96)
| ! [X97] :
( ~ r1(X96,X97)
| ! [X98] :
( ~ r1(X97,X98)
| ! [X99] :
( ~ r1(X98,X99)
| ! [X100] :
( ~ r1(X99,X100)
| ! [X101] :
( ~ r1(X100,X101)
| ! [X102] :
( ~ r1(X101,X102)
| ! [X103] :
( ~ r1(X102,X103)
| ( ( p10(X103)
| p11(X103) )
& ( ~ p11(X103)
| ~ p10(X103) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X104] :
( r1(X93,X104)
& ~ p11(X104) )
& ! [X105] :
( ~ r1(X93,X105)
| ( ! [X106] :
( ~ r1(X105,X106)
| ! [X107] :
( ~ r1(X106,X107)
| ! [X108] :
( ~ r1(X107,X108)
| ! [X109] :
( ~ r1(X108,X109)
| ! [X110] :
( ~ r1(X109,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ! [X114] :
( ~ r1(X113,X114)
| ( ( p9(X114)
| p10(X114) )
& ( ~ p10(X114)
| ~ p9(X114) ) ) ) ) ) ) ) ) ) ) )
& ? [X115] :
( r1(X105,X115)
& ~ p10(X115) )
& ! [X116] :
( ~ r1(X105,X116)
| ( ! [X117] :
( ~ r1(X116,X117)
| ! [X118] :
( ~ r1(X117,X118)
| ! [X119] :
( ~ r1(X118,X119)
| ! [X120] :
( ~ r1(X119,X120)
| ! [X121] :
( ~ r1(X120,X121)
| ! [X122] :
( ~ r1(X121,X122)
| ! [X123] :
( ~ r1(X122,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ( ( p8(X124)
| p9(X124) )
& ( ~ p9(X124)
| ~ p8(X124) ) ) ) ) ) ) ) ) ) )
& ? [X125] :
( r1(X116,X125)
& ~ p9(X125) )
& ! [X126] :
( ~ r1(X116,X126)
| ( ! [X127] :
( ~ r1(X126,X127)
| ! [X128] :
( ~ r1(X127,X128)
| ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| ! [X131] :
( ~ r1(X130,X131)
| ! [X132] :
( ~ r1(X131,X132)
| ! [X133] :
( ~ r1(X132,X133)
| ( ( p7(X133)
| p8(X133) )
& ( ~ p8(X133)
| ~ p7(X133) ) ) ) ) ) ) ) ) )
& ? [X134] :
( r1(X126,X134)
& ~ p8(X134) )
& ! [X135] :
( ~ r1(X126,X135)
| ( ! [X136] :
( ~ r1(X135,X136)
| ! [X137] :
( ~ r1(X136,X137)
| ! [X138] :
( ~ r1(X137,X138)
| ! [X139] :
( ~ r1(X138,X139)
| ! [X140] :
( ~ r1(X139,X140)
| ! [X141] :
( ~ r1(X140,X141)
| ( ( p6(X141)
| p7(X141) )
& ( ~ p7(X141)
| ~ p6(X141) ) ) ) ) ) ) ) )
& ? [X142] :
( r1(X135,X142)
& ~ p7(X142) )
& ! [X143] :
( ~ r1(X135,X143)
| ( ! [X144] :
( ~ r1(X143,X144)
| ! [X145] :
( ~ r1(X144,X145)
| ! [X146] :
( ~ r1(X145,X146)
| ! [X147] :
( ~ r1(X146,X147)
| ! [X148] :
( ~ r1(X147,X148)
| ( ( p5(X148)
| p6(X148) )
& ( ~ p6(X148)
| ~ p5(X148) ) ) ) ) ) ) )
& ? [X149] :
( r1(X143,X149)
& ~ p6(X149) )
& ! [X150] :
( ~ r1(X143,X150)
| ( ! [X151] :
( ~ r1(X150,X151)
| ! [X152] :
( ~ r1(X151,X152)
| ! [X153] :
( ~ r1(X152,X153)
| ! [X154] :
( ~ r1(X153,X154)
| ( ( p4(X154)
| p5(X154) )
& ( ~ p5(X154)
| ~ p4(X154) ) ) ) ) ) )
& ? [X155] :
( r1(X150,X155)
& ~ p5(X155) )
& ! [X156] :
( ~ r1(X150,X156)
| ( ! [X157] :
( ~ r1(X156,X157)
| ! [X158] :
( ~ r1(X157,X158)
| ! [X159] :
( ~ r1(X158,X159)
| ( ( p3(X159)
| p4(X159) )
& ( ~ p4(X159)
| ~ p3(X159) ) ) ) ) )
& ? [X160] :
( r1(X156,X160)
& ~ p4(X160) )
& ! [X161] :
( ~ r1(X156,X161)
| ( ! [X162] :
( ~ r1(X161,X162)
| ! [X163] :
( ~ r1(X162,X163)
| ( ( p2(X163)
| p3(X163) )
& ( ~ p3(X163)
| ~ p2(X163) ) ) ) )
& ? [X164] :
( r1(X161,X164)
& ~ p3(X164) )
& ! [X165] :
( ~ r1(X161,X165)
| ! [X166] :
( ~ r1(X165,X166)
| ( ( p1(X166)
| p2(X166) )
& ( ~ p2(X166)
| ~ p1(X166) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X167] :
( r1(X0,X167)
& ? [X168] :
( r1(X167,X168)
& ? [X169] :
( r1(X168,X169)
& ? [X170] :
( r1(X169,X170)
& ? [X171] :
( r1(X170,X171)
& ? [X172] :
( r1(X171,X172)
& ? [X173] :
( r1(X172,X173)
& ? [X174] :
( r1(X173,X174)
& ? [X175] :
( r1(X174,X175)
& ? [X176] :
( r1(X175,X176)
& ? [X177] :
( r1(X176,X177)
& ? [X178] :
( r1(X177,X178)
& ? [X179] :
( r1(X178,X179)
& ? [X180] :
( r1(X179,X180)
& ? [X181] :
( r1(X180,X181)
& ? [X182] :
( r1(X181,X182)
& ( ~ p16(X182)
| ~ p15(X182)
| ~ p14(X182)
| ~ p13(X182)
| ~ p12(X182)
| ~ p11(X182)
| ~ p10(X182)
| ~ p9(X182)
| ~ p8(X182)
| ~ p7(X182)
| ~ p6(X182)
| ~ p5(X182)
| ~ p4(X182)
| ~ p3(X182)
| ~ p2(X182)
| ~ p1(X182) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(ennf_transformation,[],[f4]) ).
fof(f6,definition,
! [X143] :
( ! [X150] :
( ~ r1(X143,X150)
| ( ! [X151] :
( ~ r1(X150,X151)
| ! [X152] :
( ~ r1(X151,X152)
| ! [X153] :
( ~ r1(X152,X153)
| ! [X154] :
( ~ r1(X153,X154)
| ( ( p4(X154)
| p5(X154) )
& ( ~ p5(X154)
| ~ p4(X154) ) ) ) ) ) )
& ? [X155] :
( r1(X150,X155)
& ~ p5(X155) )
& ! [X156] :
( ~ r1(X150,X156)
| ( ! [X157] :
( ~ r1(X156,X157)
| ! [X158] :
( ~ r1(X157,X158)
| ! [X159] :
( ~ r1(X158,X159)
| ( ( p3(X159)
| p4(X159) )
& ( ~ p4(X159)
| ~ p3(X159) ) ) ) ) )
& ? [X160] :
( r1(X156,X160)
& ~ p4(X160) )
& ! [X161] :
( ~ r1(X156,X161)
| ( ! [X162] :
( ~ r1(X161,X162)
| ! [X163] :
( ~ r1(X162,X163)
| ( ( p2(X163)
| p3(X163) )
& ( ~ p3(X163)
| ~ p2(X163) ) ) ) )
& ? [X164] :
( r1(X161,X164)
& ~ p3(X164) )
& ! [X165] :
( ~ r1(X161,X165)
| ! [X166] :
( ~ r1(X165,X166)
| ( ( p1(X166)
| p2(X166) )
& ( ~ p2(X166)
| ~ p1(X166) ) ) ) ) ) ) ) ) ) )
| ~ sP0(X143) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f7,definition,
! [X116] :
( ! [X126] :
( ~ r1(X116,X126)
| ( ! [X127] :
( ~ r1(X126,X127)
| ! [X128] :
( ~ r1(X127,X128)
| ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| ! [X131] :
( ~ r1(X130,X131)
| ! [X132] :
( ~ r1(X131,X132)
| ! [X133] :
( ~ r1(X132,X133)
| ( ( p7(X133)
| p8(X133) )
& ( ~ p8(X133)
| ~ p7(X133) ) ) ) ) ) ) ) ) )
& ? [X134] :
( r1(X126,X134)
& ~ p8(X134) )
& ! [X135] :
( ~ r1(X126,X135)
| ( ! [X136] :
( ~ r1(X135,X136)
| ! [X137] :
( ~ r1(X136,X137)
| ! [X138] :
( ~ r1(X137,X138)
| ! [X139] :
( ~ r1(X138,X139)
| ! [X140] :
( ~ r1(X139,X140)
| ! [X141] :
( ~ r1(X140,X141)
| ( ( p6(X141)
| p7(X141) )
& ( ~ p7(X141)
| ~ p6(X141) ) ) ) ) ) ) ) )
& ? [X142] :
( r1(X135,X142)
& ~ p7(X142) )
& ! [X143] :
( ~ r1(X135,X143)
| ( ! [X144] :
( ~ r1(X143,X144)
| ! [X145] :
( ~ r1(X144,X145)
| ! [X146] :
( ~ r1(X145,X146)
| ! [X147] :
( ~ r1(X146,X147)
| ! [X148] :
( ~ r1(X147,X148)
| ( ( p5(X148)
| p6(X148) )
& ( ~ p6(X148)
| ~ p5(X148) ) ) ) ) ) ) )
& ? [X149] :
( r1(X143,X149)
& ~ p6(X149) )
& sP0(X143) ) ) ) ) ) )
| ~ sP1(X116) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f8,definition,
! [X80] :
( ! [X93] :
( ~ r1(X80,X93)
| ( ! [X94] :
( ~ r1(X93,X94)
| ! [X95] :
( ~ r1(X94,X95)
| ! [X96] :
( ~ r1(X95,X96)
| ! [X97] :
( ~ r1(X96,X97)
| ! [X98] :
( ~ r1(X97,X98)
| ! [X99] :
( ~ r1(X98,X99)
| ! [X100] :
( ~ r1(X99,X100)
| ! [X101] :
( ~ r1(X100,X101)
| ! [X102] :
( ~ r1(X101,X102)
| ! [X103] :
( ~ r1(X102,X103)
| ( ( p10(X103)
| p11(X103) )
& ( ~ p11(X103)
| ~ p10(X103) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X104] :
( r1(X93,X104)
& ~ p11(X104) )
& ! [X105] :
( ~ r1(X93,X105)
| ( ! [X106] :
( ~ r1(X105,X106)
| ! [X107] :
( ~ r1(X106,X107)
| ! [X108] :
( ~ r1(X107,X108)
| ! [X109] :
( ~ r1(X108,X109)
| ! [X110] :
( ~ r1(X109,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ! [X114] :
( ~ r1(X113,X114)
| ( ( p9(X114)
| p10(X114) )
& ( ~ p10(X114)
| ~ p9(X114) ) ) ) ) ) ) ) ) ) ) )
& ? [X115] :
( r1(X105,X115)
& ~ p10(X115) )
& ! [X116] :
( ~ r1(X105,X116)
| ( ! [X117] :
( ~ r1(X116,X117)
| ! [X118] :
( ~ r1(X117,X118)
| ! [X119] :
( ~ r1(X118,X119)
| ! [X120] :
( ~ r1(X119,X120)
| ! [X121] :
( ~ r1(X120,X121)
| ! [X122] :
( ~ r1(X121,X122)
| ! [X123] :
( ~ r1(X122,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ( ( p8(X124)
| p9(X124) )
& ( ~ p9(X124)
| ~ p8(X124) ) ) ) ) ) ) ) ) ) )
& ? [X125] :
( r1(X116,X125)
& ~ p9(X125) )
& sP1(X116) ) ) ) ) ) )
| ~ sP2(X80) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f9,definition,
! [X35] :
( ! [X51] :
( ~ r1(X35,X51)
| ( ! [X52] :
( ~ r1(X51,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ! [X58] :
( ~ r1(X57,X58)
| ! [X59] :
( ~ r1(X58,X59)
| ! [X60] :
( ~ r1(X59,X60)
| ! [X61] :
( ~ r1(X60,X61)
| ! [X62] :
( ~ r1(X61,X62)
| ! [X63] :
( ~ r1(X62,X63)
| ! [X64] :
( ~ r1(X63,X64)
| ( ( p13(X64)
| p14(X64) )
& ( ~ p14(X64)
| ~ p13(X64) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X65] :
( r1(X51,X65)
& ~ p14(X65) )
& ! [X66] :
( ~ r1(X51,X66)
| ( ! [X67] :
( ~ r1(X66,X67)
| ! [X68] :
( ~ r1(X67,X68)
| ! [X69] :
( ~ r1(X68,X69)
| ! [X70] :
( ~ r1(X69,X70)
| ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| ! [X73] :
( ~ r1(X72,X73)
| ! [X74] :
( ~ r1(X73,X74)
| ! [X75] :
( ~ r1(X74,X75)
| ! [X76] :
( ~ r1(X75,X76)
| ! [X77] :
( ~ r1(X76,X77)
| ! [X78] :
( ~ r1(X77,X78)
| ( ( p12(X78)
| p13(X78) )
& ( ~ p13(X78)
| ~ p12(X78) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X79] :
( r1(X66,X79)
& ~ p13(X79) )
& ! [X80] :
( ~ r1(X66,X80)
| ( ! [X81] :
( ~ r1(X80,X81)
| ! [X82] :
( ~ r1(X81,X82)
| ! [X83] :
( ~ r1(X82,X83)
| ! [X84] :
( ~ r1(X83,X84)
| ! [X85] :
( ~ r1(X84,X85)
| ! [X86] :
( ~ r1(X85,X86)
| ! [X87] :
( ~ r1(X86,X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ! [X90] :
( ~ r1(X89,X90)
| ! [X91] :
( ~ r1(X90,X91)
| ( ( p11(X91)
| p12(X91) )
& ( ~ p12(X91)
| ~ p11(X91) ) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X92] :
( r1(X80,X92)
& ~ p12(X92) )
& sP2(X80) ) ) ) ) ) )
| ~ sP3(X35) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f10,plain,
? [X0] :
( ? [X1] :
( r1(X0,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)
& ( p32(X16)
| p30(X16)
| p28(X16)
| p26(X16)
| p24(X16)
| p22(X16)
| p20(X16)
| p18(X16)
| p16(X16)
| p14(X16)
| p12(X16)
| p10(X16)
| p8(X16)
| p6(X16)
| p4(X16)
| p2(X16) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X17] :
( r1(X0,X17)
& ~ p17(X17) )
& ! [X18] :
( ~ r1(X0,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)
| ( ( p15(X33)
| p1(X33) )
& ( ~ p1(X33)
| ~ p15(X33) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X34] :
( r1(X18,X34)
& ~ p16(X34) )
& ! [X35] :
( ~ r1(X18,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(X48,X49)
| ( ( p14(X49)
| p15(X49) )
& ( ~ p15(X49)
| ~ p14(X49) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X50] :
( r1(X35,X50)
& ~ p15(X50) )
& sP3(X35) ) ) ) )
& ? [X167] :
( r1(X0,X167)
& ? [X168] :
( r1(X167,X168)
& ? [X169] :
( r1(X168,X169)
& ? [X170] :
( r1(X169,X170)
& ? [X171] :
( r1(X170,X171)
& ? [X172] :
( r1(X171,X172)
& ? [X173] :
( r1(X172,X173)
& ? [X174] :
( r1(X173,X174)
& ? [X175] :
( r1(X174,X175)
& ? [X176] :
( r1(X175,X176)
& ? [X177] :
( r1(X176,X177)
& ? [X178] :
( r1(X177,X178)
& ? [X179] :
( r1(X178,X179)
& ? [X180] :
( r1(X179,X180)
& ? [X181] :
( r1(X180,X181)
& ? [X182] :
( r1(X181,X182)
& ( ~ p16(X182)
| ~ p15(X182)
| ~ p14(X182)
| ~ p13(X182)
| ~ p12(X182)
| ~ p11(X182)
| ~ p10(X182)
| ~ p9(X182)
| ~ p8(X182)
| ~ p7(X182)
| ~ p6(X182)
| ~ p5(X182)
| ~ p4(X182)
| ~ p3(X182)
| ~ p2(X182)
| ~ p1(X182) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(definition_folding,[],[f5,f9,f8,f7,f6]) ).
fof(f11,plain,
! [X35] :
( ! [X51] :
( ~ r1(X35,X51)
| ( ! [X52] :
( ~ r1(X51,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ! [X58] :
( ~ r1(X57,X58)
| ! [X59] :
( ~ r1(X58,X59)
| ! [X60] :
( ~ r1(X59,X60)
| ! [X61] :
( ~ r1(X60,X61)
| ! [X62] :
( ~ r1(X61,X62)
| ! [X63] :
( ~ r1(X62,X63)
| ! [X64] :
( ~ r1(X63,X64)
| ( ( p13(X64)
| p14(X64) )
& ( ~ p14(X64)
| ~ p13(X64) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X65] :
( r1(X51,X65)
& ~ p14(X65) )
& ! [X66] :
( ~ r1(X51,X66)
| ( ! [X67] :
( ~ r1(X66,X67)
| ! [X68] :
( ~ r1(X67,X68)
| ! [X69] :
( ~ r1(X68,X69)
| ! [X70] :
( ~ r1(X69,X70)
| ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| ! [X73] :
( ~ r1(X72,X73)
| ! [X74] :
( ~ r1(X73,X74)
| ! [X75] :
( ~ r1(X74,X75)
| ! [X76] :
( ~ r1(X75,X76)
| ! [X77] :
( ~ r1(X76,X77)
| ! [X78] :
( ~ r1(X77,X78)
| ( ( p12(X78)
| p13(X78) )
& ( ~ p13(X78)
| ~ p12(X78) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X79] :
( r1(X66,X79)
& ~ p13(X79) )
& ! [X80] :
( ~ r1(X66,X80)
| ( ! [X81] :
( ~ r1(X80,X81)
| ! [X82] :
( ~ r1(X81,X82)
| ! [X83] :
( ~ r1(X82,X83)
| ! [X84] :
( ~ r1(X83,X84)
| ! [X85] :
( ~ r1(X84,X85)
| ! [X86] :
( ~ r1(X85,X86)
| ! [X87] :
( ~ r1(X86,X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ! [X90] :
( ~ r1(X89,X90)
| ! [X91] :
( ~ r1(X90,X91)
| ( ( p11(X91)
| p12(X91) )
& ( ~ p12(X91)
| ~ p11(X91) ) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X92] :
( r1(X80,X92)
& ~ p12(X92) )
& sP2(X80) ) ) ) ) ) )
| ~ sP3(X35) ),
inference(nnf_transformation,[],[f9]) ).
fof(f12,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,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)
| ( ( p13(X14)
| p14(X14) )
& ( ~ p14(X14)
| ~ p13(X14) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X15] :
( r1(X1,X15)
& ~ p14(X15) )
& ! [X16] :
( ~ r1(X1,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)
| ( ( p12(X28)
| p13(X28) )
& ( ~ p13(X28)
| ~ p12(X28) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X29] :
( r1(X16,X29)
& ~ p13(X29) )
& ! [X30] :
( ~ r1(X16,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)
| ( ( p11(X41)
| p12(X41) )
& ( ~ p12(X41)
| ~ p11(X41) ) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X42] :
( r1(X30,X42)
& ~ p12(X42) )
& sP2(X30) ) ) ) ) ) )
| ~ sP3(X0) ),
inference(rectify,[],[f11]) ).
fof(f13,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,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)
| ( ( p13(X14)
| p14(X14) )
& ( ~ p14(X14)
| ~ p13(X14) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& r1(X1,sK4(X1))
& ~ p14(sK4(X1))
& ! [X16] :
( ~ r1(X1,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)
| ( ( p12(X28)
| p13(X28) )
& ( ~ p13(X28)
| ~ p12(X28) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& r1(X16,sK5(X16))
& ~ p13(sK5(X16))
& ! [X30] :
( ~ r1(X16,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)
| ( ( p11(X41)
| p12(X41) )
& ( ~ p12(X41)
| ~ p11(X41) ) ) ) ) ) ) ) ) ) ) ) ) )
& r1(X30,sK6(X30))
& ~ p12(sK6(X30))
& sP2(X30) ) ) ) ) ) )
| ~ sP3(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5,sK6]),skolemize(X15,sK4(X1)),skolemize(X29,sK5(X16)),skolemize(X42,sK6(X30))],[f12]) ).
fof(f14,plain,
! [X80] :
( ! [X93] :
( ~ r1(X80,X93)
| ( ! [X94] :
( ~ r1(X93,X94)
| ! [X95] :
( ~ r1(X94,X95)
| ! [X96] :
( ~ r1(X95,X96)
| ! [X97] :
( ~ r1(X96,X97)
| ! [X98] :
( ~ r1(X97,X98)
| ! [X99] :
( ~ r1(X98,X99)
| ! [X100] :
( ~ r1(X99,X100)
| ! [X101] :
( ~ r1(X100,X101)
| ! [X102] :
( ~ r1(X101,X102)
| ! [X103] :
( ~ r1(X102,X103)
| ( ( p10(X103)
| p11(X103) )
& ( ~ p11(X103)
| ~ p10(X103) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X104] :
( r1(X93,X104)
& ~ p11(X104) )
& ! [X105] :
( ~ r1(X93,X105)
| ( ! [X106] :
( ~ r1(X105,X106)
| ! [X107] :
( ~ r1(X106,X107)
| ! [X108] :
( ~ r1(X107,X108)
| ! [X109] :
( ~ r1(X108,X109)
| ! [X110] :
( ~ r1(X109,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ! [X114] :
( ~ r1(X113,X114)
| ( ( p9(X114)
| p10(X114) )
& ( ~ p10(X114)
| ~ p9(X114) ) ) ) ) ) ) ) ) ) ) )
& ? [X115] :
( r1(X105,X115)
& ~ p10(X115) )
& ! [X116] :
( ~ r1(X105,X116)
| ( ! [X117] :
( ~ r1(X116,X117)
| ! [X118] :
( ~ r1(X117,X118)
| ! [X119] :
( ~ r1(X118,X119)
| ! [X120] :
( ~ r1(X119,X120)
| ! [X121] :
( ~ r1(X120,X121)
| ! [X122] :
( ~ r1(X121,X122)
| ! [X123] :
( ~ r1(X122,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ( ( p8(X124)
| p9(X124) )
& ( ~ p9(X124)
| ~ p8(X124) ) ) ) ) ) ) ) ) ) )
& ? [X125] :
( r1(X116,X125)
& ~ p9(X125) )
& sP1(X116) ) ) ) ) ) )
| ~ sP2(X80) ),
inference(nnf_transformation,[],[f8]) ).
fof(f15,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,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)
| ( ( p10(X11)
| p11(X11) )
& ( ~ p11(X11)
| ~ p10(X11) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X12] :
( r1(X1,X12)
& ~ p11(X12) )
& ! [X13] :
( ~ r1(X1,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)
| ( ( p9(X22)
| p10(X22) )
& ( ~ p10(X22)
| ~ p9(X22) ) ) ) ) ) ) ) ) ) ) )
& ? [X23] :
( r1(X13,X23)
& ~ p10(X23) )
& ! [X24] :
( ~ r1(X13,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)
| ( ( p8(X32)
| p9(X32) )
& ( ~ p9(X32)
| ~ p8(X32) ) ) ) ) ) ) ) ) ) )
& ? [X33] :
( r1(X24,X33)
& ~ p9(X33) )
& sP1(X24) ) ) ) ) ) )
| ~ sP2(X0) ),
inference(rectify,[],[f14]) ).
fof(f16,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,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)
| ( ( p10(X11)
| p11(X11) )
& ( ~ p11(X11)
| ~ p10(X11) ) ) ) ) ) ) ) ) ) ) ) )
& r1(X1,sK7(X1))
& ~ p11(sK7(X1))
& ! [X13] :
( ~ r1(X1,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)
| ( ( p9(X22)
| p10(X22) )
& ( ~ p10(X22)
| ~ p9(X22) ) ) ) ) ) ) ) ) ) ) )
& r1(X13,sK8(X13))
& ~ p10(sK8(X13))
& ! [X24] :
( ~ r1(X13,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)
| ( ( p8(X32)
| p9(X32) )
& ( ~ p9(X32)
| ~ p8(X32) ) ) ) ) ) ) ) ) ) )
& r1(X24,sK9(X24))
& ~ p9(sK9(X24))
& sP1(X24) ) ) ) ) ) )
| ~ sP2(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK8,sK9]),skolemize(X12,sK7(X1)),skolemize(X23,sK8(X13)),skolemize(X33,sK9(X24))],[f15]) ).
fof(f17,plain,
! [X116] :
( ! [X126] :
( ~ r1(X116,X126)
| ( ! [X127] :
( ~ r1(X126,X127)
| ! [X128] :
( ~ r1(X127,X128)
| ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| ! [X131] :
( ~ r1(X130,X131)
| ! [X132] :
( ~ r1(X131,X132)
| ! [X133] :
( ~ r1(X132,X133)
| ( ( p7(X133)
| p8(X133) )
& ( ~ p8(X133)
| ~ p7(X133) ) ) ) ) ) ) ) ) )
& ? [X134] :
( r1(X126,X134)
& ~ p8(X134) )
& ! [X135] :
( ~ r1(X126,X135)
| ( ! [X136] :
( ~ r1(X135,X136)
| ! [X137] :
( ~ r1(X136,X137)
| ! [X138] :
( ~ r1(X137,X138)
| ! [X139] :
( ~ r1(X138,X139)
| ! [X140] :
( ~ r1(X139,X140)
| ! [X141] :
( ~ r1(X140,X141)
| ( ( p6(X141)
| p7(X141) )
& ( ~ p7(X141)
| ~ p6(X141) ) ) ) ) ) ) ) )
& ? [X142] :
( r1(X135,X142)
& ~ p7(X142) )
& ! [X143] :
( ~ r1(X135,X143)
| ( ! [X144] :
( ~ r1(X143,X144)
| ! [X145] :
( ~ r1(X144,X145)
| ! [X146] :
( ~ r1(X145,X146)
| ! [X147] :
( ~ r1(X146,X147)
| ! [X148] :
( ~ r1(X147,X148)
| ( ( p5(X148)
| p6(X148) )
& ( ~ p6(X148)
| ~ p5(X148) ) ) ) ) ) ) )
& ? [X149] :
( r1(X143,X149)
& ~ p6(X149) )
& sP0(X143) ) ) ) ) ) )
| ~ sP1(X116) ),
inference(nnf_transformation,[],[f7]) ).
fof(f18,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,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)
| ( ( p7(X8)
| p8(X8) )
& ( ~ p8(X8)
| ~ p7(X8) ) ) ) ) ) ) ) ) )
& ? [X9] :
( r1(X1,X9)
& ~ p8(X9) )
& ! [X10] :
( ~ r1(X1,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)
| ( ( p6(X16)
| p7(X16) )
& ( ~ p7(X16)
| ~ p6(X16) ) ) ) ) ) ) ) )
& ? [X17] :
( r1(X10,X17)
& ~ p7(X17) )
& ! [X18] :
( ~ r1(X10,X18)
| ( ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ( ( p5(X23)
| p6(X23) )
& ( ~ p6(X23)
| ~ p5(X23) ) ) ) ) ) ) )
& ? [X24] :
( r1(X18,X24)
& ~ p6(X24) )
& sP0(X18) ) ) ) ) ) )
| ~ sP1(X0) ),
inference(rectify,[],[f17]) ).
fof(f19,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,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)
| ( ( p7(X8)
| p8(X8) )
& ( ~ p8(X8)
| ~ p7(X8) ) ) ) ) ) ) ) ) )
& r1(X1,sK10(X1))
& ~ p8(sK10(X1))
& ! [X10] :
( ~ r1(X1,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)
| ( ( p6(X16)
| p7(X16) )
& ( ~ p7(X16)
| ~ p6(X16) ) ) ) ) ) ) ) )
& r1(X10,sK11(X10))
& ~ p7(sK11(X10))
& ! [X18] :
( ~ r1(X10,X18)
| ( ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ( ( p5(X23)
| p6(X23) )
& ( ~ p6(X23)
| ~ p5(X23) ) ) ) ) ) ) )
& r1(X18,sK12(X18))
& ~ p6(sK12(X18))
& sP0(X18) ) ) ) ) ) )
| ~ sP1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11,sK12]),skolemize(X9,sK10(X1)),skolemize(X17,sK11(X10)),skolemize(X24,sK12(X18))],[f18]) ).
fof(f20,plain,
! [X143] :
( ! [X150] :
( ~ r1(X143,X150)
| ( ! [X151] :
( ~ r1(X150,X151)
| ! [X152] :
( ~ r1(X151,X152)
| ! [X153] :
( ~ r1(X152,X153)
| ! [X154] :
( ~ r1(X153,X154)
| ( ( p4(X154)
| p5(X154) )
& ( ~ p5(X154)
| ~ p4(X154) ) ) ) ) ) )
& ? [X155] :
( r1(X150,X155)
& ~ p5(X155) )
& ! [X156] :
( ~ r1(X150,X156)
| ( ! [X157] :
( ~ r1(X156,X157)
| ! [X158] :
( ~ r1(X157,X158)
| ! [X159] :
( ~ r1(X158,X159)
| ( ( p3(X159)
| p4(X159) )
& ( ~ p4(X159)
| ~ p3(X159) ) ) ) ) )
& ? [X160] :
( r1(X156,X160)
& ~ p4(X160) )
& ! [X161] :
( ~ r1(X156,X161)
| ( ! [X162] :
( ~ r1(X161,X162)
| ! [X163] :
( ~ r1(X162,X163)
| ( ( p2(X163)
| p3(X163) )
& ( ~ p3(X163)
| ~ p2(X163) ) ) ) )
& ? [X164] :
( r1(X161,X164)
& ~ p3(X164) )
& ! [X165] :
( ~ r1(X161,X165)
| ! [X166] :
( ~ r1(X165,X166)
| ( ( p1(X166)
| p2(X166) )
& ( ~ p2(X166)
| ~ p1(X166) ) ) ) ) ) ) ) ) ) )
| ~ sP0(X143) ),
inference(nnf_transformation,[],[f6]) ).
fof(f21,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ( ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ( ( p4(X5)
| p5(X5) )
& ( ~ p5(X5)
| ~ p4(X5) ) ) ) ) ) )
& ? [X6] :
( r1(X1,X6)
& ~ p5(X6) )
& ! [X7] :
( ~ r1(X1,X7)
| ( ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ( ( p3(X10)
| p4(X10) )
& ( ~ p4(X10)
| ~ p3(X10) ) ) ) ) )
& ? [X11] :
( r1(X7,X11)
& ~ p4(X11) )
& ! [X12] :
( ~ r1(X7,X12)
| ( ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ( ( p2(X14)
| p3(X14) )
& ( ~ p3(X14)
| ~ p2(X14) ) ) ) )
& ? [X15] :
( r1(X12,X15)
& ~ p3(X15) )
& ! [X16] :
( ~ r1(X12,X16)
| ! [X17] :
( ~ r1(X16,X17)
| ( ( p1(X17)
| p2(X17) )
& ( ~ p2(X17)
| ~ p1(X17) ) ) ) ) ) ) ) ) ) )
| ~ sP0(X0) ),
inference(rectify,[],[f20]) ).
fof(f22,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ( ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ( ( p4(X5)
| p5(X5) )
& ( ~ p5(X5)
| ~ p4(X5) ) ) ) ) ) )
& r1(X1,sK13(X1))
& ~ p5(sK13(X1))
& ! [X7] :
( ~ r1(X1,X7)
| ( ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ( ( p3(X10)
| p4(X10) )
& ( ~ p4(X10)
| ~ p3(X10) ) ) ) ) )
& r1(X7,sK14(X7))
& ~ p4(sK14(X7))
& ! [X12] :
( ~ r1(X7,X12)
| ( ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ( ( p2(X14)
| p3(X14) )
& ( ~ p3(X14)
| ~ p2(X14) ) ) ) )
& r1(X12,sK15(X12))
& ~ p3(sK15(X12))
& ! [X16] :
( ~ r1(X12,X16)
| ! [X17] :
( ~ r1(X16,X17)
| ( ( p1(X17)
| p2(X17) )
& ( ~ p2(X17)
| ~ p1(X17) ) ) ) ) ) ) ) ) ) )
| ~ sP0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14,sK15]),skolemize(X6,sK13(X1)),skolemize(X11,sK14(X7)),skolemize(X15,sK15(X12))],[f21]) ).
fof(f23,plain,
? [X0] :
( ? [X1] :
( r1(X0,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)
& ( p32(X16)
| p30(X16)
| p28(X16)
| p26(X16)
| p24(X16)
| p22(X16)
| p20(X16)
| p18(X16)
| p16(X16)
| p14(X16)
| p12(X16)
| p10(X16)
| p8(X16)
| p6(X16)
| p4(X16)
| p2(X16) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X17] :
( r1(X0,X17)
& ~ p17(X17) )
& ! [X18] :
( ~ r1(X0,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)
| ( ( p15(X33)
| p1(X33) )
& ( ~ p1(X33)
| ~ p15(X33) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X34] :
( r1(X18,X34)
& ~ p16(X34) )
& ! [X35] :
( ~ r1(X18,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(X48,X49)
| ( ( p14(X49)
| p15(X49) )
& ( ~ p15(X49)
| ~ p14(X49) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X50] :
( r1(X35,X50)
& ~ p15(X50) )
& sP3(X35) ) ) ) )
& ? [X51] :
( r1(X0,X51)
& ? [X52] :
( r1(X51,X52)
& ? [X53] :
( r1(X52,X53)
& ? [X54] :
( r1(X53,X54)
& ? [X55] :
( r1(X54,X55)
& ? [X56] :
( r1(X55,X56)
& ? [X57] :
( r1(X56,X57)
& ? [X58] :
( r1(X57,X58)
& ? [X59] :
( r1(X58,X59)
& ? [X60] :
( r1(X59,X60)
& ? [X61] :
( r1(X60,X61)
& ? [X62] :
( r1(X61,X62)
& ? [X63] :
( r1(X62,X63)
& ? [X64] :
( r1(X63,X64)
& ? [X65] :
( r1(X64,X65)
& ? [X66] :
( r1(X65,X66)
& ( ~ p16(X66)
| ~ p15(X66)
| ~ p14(X66)
| ~ p13(X66)
| ~ p12(X66)
| ~ p11(X66)
| ~ p10(X66)
| ~ p9(X66)
| ~ p8(X66)
| ~ p7(X66)
| ~ p6(X66)
| ~ p5(X66)
| ~ p4(X66)
| ~ p3(X66)
| ~ p2(X66)
| ~ p1(X66) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f10]) ).
fof(f24,plain,
( r1(sK16,sK17)
& r1(sK17,sK18)
& r1(sK18,sK19)
& r1(sK19,sK20)
& r1(sK20,sK21)
& r1(sK21,sK22)
& r1(sK22,sK23)
& r1(sK23,sK24)
& r1(sK24,sK25)
& r1(sK25,sK26)
& r1(sK26,sK27)
& r1(sK27,sK28)
& r1(sK28,sK29)
& r1(sK29,sK30)
& r1(sK30,sK31)
& r1(sK31,sK32)
& ( p32(sK32)
| p30(sK32)
| p28(sK32)
| p26(sK32)
| p24(sK32)
| p22(sK32)
| p20(sK32)
| p18(sK32)
| p16(sK32)
| p14(sK32)
| p12(sK32)
| p10(sK32)
| p8(sK32)
| p6(sK32)
| p4(sK32)
| p2(sK32) )
& r1(sK16,sK33)
& ~ p17(sK33)
& ! [X18] :
( ~ r1(sK16,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)
| ( ( p15(X33)
| p1(X33) )
& ( ~ p1(X33)
| ~ p15(X33) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& r1(X18,sK34(X18))
& ~ p16(sK34(X18))
& ! [X35] :
( ~ r1(X18,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(X48,X49)
| ( ( p14(X49)
| p15(X49) )
& ( ~ p15(X49)
| ~ p14(X49) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& r1(X35,sK35(X35))
& ~ p15(sK35(X35))
& sP3(X35) ) ) ) )
& r1(sK16,sK36)
& r1(sK36,sK37)
& r1(sK37,sK38)
& r1(sK38,sK39)
& r1(sK39,sK40)
& r1(sK40,sK41)
& r1(sK41,sK42)
& r1(sK42,sK43)
& r1(sK43,sK44)
& r1(sK44,sK45)
& r1(sK45,sK46)
& r1(sK46,sK47)
& r1(sK47,sK48)
& r1(sK48,sK49)
& r1(sK49,sK50)
& r1(sK50,sK51)
& ( ~ p16(sK51)
| ~ p15(sK51)
| ~ p14(sK51)
| ~ p13(sK51)
| ~ p12(sK51)
| ~ p11(sK51)
| ~ p10(sK51)
| ~ p9(sK51)
| ~ p8(sK51)
| ~ p7(sK51)
| ~ p6(sK51)
| ~ p5(sK51)
| ~ p4(sK51)
| ~ p3(sK51)
| ~ p2(sK51)
| ~ p1(sK51) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16,sK17,sK18,sK19,sK20,sK21,sK22,sK23,sK24,sK25,sK26,sK27,sK28,sK29,sK30,sK31,sK32,sK33,sK34,sK35,sK36,sK37,sK38,sK39,sK40,sK41,sK42,sK43,sK44,sK45,sK46,sK47,sK48,sK49,sK50,sK51]),skolemize(X0,sK16),skolemize(X1,sK17),skolemize(X2,sK18),skolemize(X3,sK19),skolemize(X4,sK20),skolemize(X5,sK21),skolemize(X6,sK22),skolemize(X7,sK23),skolemize(X8,sK24),skolemize(X9,sK25),skolemize(X10,sK26),skolemize(X11,sK27),skolemize(X12,sK28),skolemize(X13,sK29),skolemize(X14,sK30),skolemize(X15,sK31),skolemize(X16,sK32),skolemize(X17,sK33),skolemize(X34,sK34(X18)),skolemize(X50,sK35(X35)),skolemize(X51,sK36),skolemize(X52,sK37),skolemize(X53,sK38),skolemize(X54,sK39),skolemize(X55,sK40),skolemize(X56,sK41),skolemize(X57,sK42),skolemize(X58,sK43),skolemize(X59,sK44),skolemize(X60,sK45),skolemize(X61,sK46),skolemize(X62,sK47),skolemize(X63,sK48),skolemize(X64,sK49),skolemize(X65,sK50),skolemize(X66,sK51)],[f23]) ).
fof(f25,plain,
! [X0,X1,X16,X30] :
( ~ sP3(X0)
| ~ r1(X1,X16)
| ~ r1(X16,X30)
| sP2(X30)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f13]) ).
fof(f28,plain,
! [X31,X38,X40,X39,X0,X36,X41,X1,X37,X16,X34,X35,X32,X30,X33] :
( ~ sP3(X0)
| ~ r1(X1,X16)
| ~ r1(X16,X30)
| ~ r1(X30,X31)
| ~ r1(X31,X32)
| ~ r1(X32,X33)
| ~ r1(X33,X34)
| ~ r1(X34,X35)
| ~ r1(X35,X36)
| ~ r1(X36,X37)
| ~ r1(X37,X38)
| ~ r1(X38,X39)
| ~ r1(X39,X40)
| ~ r1(X40,X41)
| ~ p12(X41)
| ~ p11(X41)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f13]) ).
fof(f29,plain,
! [X31,X38,X40,X39,X0,X36,X41,X1,X37,X16,X34,X35,X32,X30,X33] :
( ~ sP3(X0)
| ~ r1(X1,X16)
| ~ r1(X16,X30)
| ~ r1(X30,X31)
| ~ r1(X31,X32)
| ~ r1(X32,X33)
| ~ r1(X33,X34)
| ~ r1(X34,X35)
| ~ r1(X35,X36)
| ~ r1(X36,X37)
| ~ r1(X37,X38)
| ~ r1(X38,X39)
| ~ r1(X39,X40)
| ~ r1(X40,X41)
| p11(X41)
| p12(X41)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f13]) ).
fof(f32,plain,
! [X21,X28,X0,X1,X18,X19,X26,X16,X27,X17,X24,X22,X25,X23,X20] :
( ~ sP3(X0)
| ~ r1(X1,X16)
| ~ r1(X16,X17)
| ~ r1(X17,X18)
| ~ r1(X18,X19)
| ~ r1(X19,X20)
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| ~ r1(X23,X24)
| ~ r1(X24,X25)
| ~ r1(X25,X26)
| ~ r1(X26,X27)
| ~ r1(X27,X28)
| ~ p13(X28)
| ~ p12(X28)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f13]) ).
fof(f33,plain,
! [X21,X28,X0,X1,X18,X19,X26,X16,X27,X17,X24,X22,X25,X23,X20] :
( ~ sP3(X0)
| ~ r1(X1,X16)
| ~ r1(X16,X17)
| ~ r1(X17,X18)
| ~ r1(X18,X19)
| ~ r1(X19,X20)
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| ~ r1(X23,X24)
| ~ r1(X24,X25)
| ~ r1(X25,X26)
| ~ r1(X26,X27)
| ~ r1(X27,X28)
| p12(X28)
| p13(X28)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f13]) ).
fof(f36,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X5,X12,X13] :
( ~ sP3(X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ r1(X13,X14)
| ~ p14(X14)
| ~ p13(X14)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f13]) ).
fof(f37,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X5,X12,X13] :
( ~ sP3(X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ r1(X13,X14)
| p13(X14)
| p14(X14)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f13]) ).
fof(f38,plain,
! [X0,X1,X24,X13] :
( ~ sP2(X0)
| ~ r1(X1,X13)
| ~ r1(X13,X24)
| sP1(X24)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f16]) ).
fof(f41,plain,
! [X31,X28,X0,X29,X1,X26,X27,X24,X25,X32,X13,X30] :
( ~ sP2(X0)
| ~ r1(X1,X13)
| ~ r1(X13,X24)
| ~ r1(X24,X25)
| ~ r1(X25,X26)
| ~ r1(X26,X27)
| ~ r1(X27,X28)
| ~ r1(X28,X29)
| ~ r1(X29,X30)
| ~ r1(X30,X31)
| ~ r1(X31,X32)
| ~ p9(X32)
| ~ p8(X32)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f16]) ).
fof(f42,plain,
! [X31,X28,X0,X29,X1,X26,X27,X24,X25,X32,X13,X30] :
( ~ sP2(X0)
| ~ r1(X1,X13)
| ~ r1(X13,X24)
| ~ r1(X24,X25)
| ~ r1(X25,X26)
| ~ r1(X26,X27)
| ~ r1(X27,X28)
| ~ r1(X28,X29)
| ~ r1(X29,X30)
| ~ r1(X30,X31)
| ~ r1(X31,X32)
| p8(X32)
| p9(X32)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f16]) ).
fof(f45,plain,
! [X21,X0,X1,X18,X19,X16,X14,X17,X15,X22,X13,X20] :
( ~ sP2(X0)
| ~ r1(X1,X13)
| ~ r1(X13,X14)
| ~ r1(X14,X15)
| ~ r1(X15,X16)
| ~ r1(X16,X17)
| ~ r1(X17,X18)
| ~ r1(X18,X19)
| ~ r1(X19,X20)
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ p10(X22)
| ~ p9(X22)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f16]) ).
fof(f46,plain,
! [X21,X0,X1,X18,X19,X16,X14,X17,X15,X22,X13,X20] :
( ~ sP2(X0)
| ~ r1(X1,X13)
| ~ r1(X13,X14)
| ~ r1(X14,X15)
| ~ r1(X15,X16)
| ~ r1(X16,X17)
| ~ r1(X17,X18)
| ~ r1(X18,X19)
| ~ r1(X19,X20)
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| p9(X22)
| p10(X22)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f16]) ).
fof(f49,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ sP2(X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ p11(X11)
| ~ p10(X11)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f16]) ).
fof(f50,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ sP2(X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| p10(X11)
| p11(X11)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f16]) ).
fof(f51,plain,
! [X10,X0,X1,X18] :
( ~ sP1(X0)
| ~ r1(X1,X10)
| ~ r1(X10,X18)
| sP0(X18)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f19]) ).
fof(f54,plain,
! [X21,X10,X0,X1,X18,X19,X22,X23,X20] :
( ~ sP1(X0)
| ~ r1(X1,X10)
| ~ r1(X10,X18)
| ~ r1(X18,X19)
| ~ r1(X19,X20)
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| ~ p6(X23)
| ~ p5(X23)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f19]) ).
fof(f55,plain,
! [X21,X10,X0,X1,X18,X19,X22,X23,X20] :
( ~ sP1(X0)
| ~ r1(X1,X10)
| ~ r1(X10,X18)
| ~ r1(X18,X19)
| ~ r1(X19,X20)
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| p5(X23)
| p6(X23)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f19]) ).
fof(f58,plain,
! [X10,X0,X11,X1,X16,X14,X15,X12,X13] :
( ~ sP1(X0)
| ~ r1(X1,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ r1(X13,X14)
| ~ r1(X14,X15)
| ~ r1(X15,X16)
| ~ p7(X16)
| ~ p6(X16)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f19]) ).
fof(f59,plain,
! [X10,X0,X11,X1,X16,X14,X15,X12,X13] :
( ~ sP1(X0)
| ~ r1(X1,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ r1(X13,X14)
| ~ r1(X14,X15)
| ~ r1(X15,X16)
| p6(X16)
| p7(X16)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f19]) ).
fof(f62,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ sP1(X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ p8(X8)
| ~ p7(X8)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f19]) ).
fof(f63,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ sP1(X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| p7(X8)
| p8(X8)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f19]) ).
fof(f64,plain,
! [X0,X1,X7,X16,X17,X12] :
( ~ sP0(X0)
| ~ r1(X1,X7)
| ~ r1(X7,X12)
| ~ r1(X12,X16)
| ~ r1(X16,X17)
| ~ p2(X17)
| ~ p1(X17)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
fof(f65,plain,
! [X0,X1,X7,X16,X17,X12] :
( ~ sP0(X0)
| ~ r1(X1,X7)
| ~ r1(X7,X12)
| ~ r1(X12,X16)
| ~ r1(X16,X17)
| p1(X17)
| p2(X17)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
fof(f68,plain,
! [X0,X1,X7,X14,X12,X13] :
( ~ sP0(X0)
| ~ r1(X1,X7)
| ~ r1(X7,X12)
| ~ r1(X12,X13)
| ~ r1(X13,X14)
| ~ p3(X14)
| ~ p2(X14)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
fof(f69,plain,
! [X0,X1,X7,X14,X12,X13] :
( ~ sP0(X0)
| ~ r1(X1,X7)
| ~ r1(X7,X12)
| ~ r1(X12,X13)
| ~ r1(X13,X14)
| p2(X14)
| p3(X14)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
fof(f72,plain,
! [X10,X0,X1,X8,X9,X7] :
( ~ sP0(X0)
| ~ r1(X1,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ p4(X10)
| ~ p3(X10)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
fof(f73,plain,
! [X10,X0,X1,X8,X9,X7] :
( ~ sP0(X0)
| ~ r1(X1,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| p3(X10)
| p4(X10)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
fof(f76,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ sP0(X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ p5(X5)
| ~ p4(X5)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
fof(f77,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ sP0(X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p4(X5)
| p5(X5)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
fof(f79,plain,
r1(sK50,sK51),
inference(cnf_transformation,[],[f24]) ).
fof(f80,plain,
r1(sK49,sK50),
inference(cnf_transformation,[],[f24]) ).
fof(f81,plain,
r1(sK48,sK49),
inference(cnf_transformation,[],[f24]) ).
fof(f82,plain,
r1(sK47,sK48),
inference(cnf_transformation,[],[f24]) ).
fof(f83,plain,
r1(sK46,sK47),
inference(cnf_transformation,[],[f24]) ).
fof(f84,plain,
r1(sK45,sK46),
inference(cnf_transformation,[],[f24]) ).
fof(f85,plain,
r1(sK44,sK45),
inference(cnf_transformation,[],[f24]) ).
fof(f86,plain,
r1(sK43,sK44),
inference(cnf_transformation,[],[f24]) ).
fof(f87,plain,
r1(sK42,sK43),
inference(cnf_transformation,[],[f24]) ).
fof(f88,plain,
r1(sK41,sK42),
inference(cnf_transformation,[],[f24]) ).
fof(f89,plain,
r1(sK40,sK41),
inference(cnf_transformation,[],[f24]) ).
fof(f90,plain,
r1(sK39,sK40),
inference(cnf_transformation,[],[f24]) ).
fof(f91,plain,
r1(sK38,sK39),
inference(cnf_transformation,[],[f24]) ).
fof(f92,plain,
r1(sK37,sK38),
inference(cnf_transformation,[],[f24]) ).
fof(f93,plain,
r1(sK36,sK37),
inference(cnf_transformation,[],[f24]) ).
fof(f94,plain,
r1(sK16,sK36),
inference(cnf_transformation,[],[f24]) ).
fof(f95,plain,
! [X18,X35] :
( ~ r1(sK16,X18)
| ~ r1(X18,X35)
| sP3(X35) ),
inference(cnf_transformation,[],[f24]) ).
fof(f98,plain,
! [X40,X38,X41,X39,X46,X49,X36,X48,X18,X37,X44,X47,X45,X35,X42,X43] :
( ~ p15(X49)
| ~ r1(X18,X35)
| ~ r1(X35,X36)
| ~ r1(X36,X37)
| ~ r1(X37,X38)
| ~ r1(X38,X39)
| ~ r1(X39,X40)
| ~ r1(X40,X41)
| ~ r1(X41,X42)
| ~ r1(X42,X43)
| ~ r1(X43,X44)
| ~ r1(X44,X45)
| ~ r1(X45,X46)
| ~ r1(X46,X47)
| ~ r1(X47,X48)
| ~ r1(X48,X49)
| ~ r1(sK16,X18)
| ~ p14(X49) ),
inference(cnf_transformation,[],[f24]) ).
fof(f99,plain,
! [X40,X38,X41,X39,X46,X36,X48,X49,X18,X37,X44,X47,X45,X35,X42,X43] :
( ~ r1(sK16,X18)
| ~ r1(X18,X35)
| ~ r1(X35,X36)
| ~ r1(X36,X37)
| ~ r1(X37,X38)
| ~ r1(X38,X39)
| ~ r1(X39,X40)
| ~ r1(X40,X41)
| ~ r1(X41,X42)
| ~ r1(X42,X43)
| ~ r1(X43,X44)
| ~ r1(X44,X45)
| ~ r1(X45,X46)
| ~ r1(X46,X47)
| ~ r1(X47,X48)
| ~ r1(X48,X49)
| p14(X49)
| p15(X49) ),
inference(cnf_transformation,[],[f24]) ).
fof(f102,plain,
! [X32,X31,X21,X28,X29,X18,X19,X26,X27,X24,X22,X25,X23,X30,X33,X20] :
( ~ p1(X33)
| ~ r1(X18,X19)
| ~ r1(X19,X20)
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| ~ r1(X23,X24)
| ~ r1(X24,X25)
| ~ r1(X25,X26)
| ~ r1(X26,X27)
| ~ r1(X27,X28)
| ~ r1(X28,X29)
| ~ r1(X29,X30)
| ~ r1(X30,X31)
| ~ r1(X31,X32)
| ~ r1(X32,X33)
| ~ r1(sK16,X18)
| ~ p15(X33) ),
inference(cnf_transformation,[],[f24]) ).
fof(f103,plain,
! [X33,X31,X21,X28,X29,X18,X19,X26,X27,X24,X22,X25,X23,X30,X20,X32] :
( ~ r1(sK16,X18)
| ~ r1(X18,X19)
| ~ r1(X19,X20)
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| ~ r1(X23,X24)
| ~ r1(X24,X25)
| ~ r1(X25,X26)
| ~ r1(X26,X27)
| ~ r1(X27,X28)
| ~ r1(X28,X29)
| ~ r1(X29,X30)
| ~ r1(X30,X31)
| ~ r1(X31,X32)
| ~ r1(X32,X33)
| p15(X33)
| p1(X33) ),
inference(cnf_transformation,[],[f24]) ).
fof(f126,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X5,X12,X13] :
( ~ r1(sK36,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ r1(X13,X14)
| p15(X14)
| p1(X14) ),
inference(resolution,[],[f94,f103]) ).
fof(f127,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X5,X12,X13] :
( ~ r1(sK36,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ r1(X13,X14)
| p14(X14)
| p15(X14) ),
inference(resolution,[],[f94,f99]) ).
fof(f128,plain,
! [X0] :
( ~ r1(sK36,X0)
| sP3(X0) ),
inference(resolution,[],[f94,f95]) ).
fof(f142,plain,
sP3(sK37),
inference(resolution,[],[f93,f128]) ).
fof(f143,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ r1(sK37,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| p15(X13)
| p1(X13) ),
inference(resolution,[],[f93,f126]) ).
fof(f144,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ r1(sK37,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| p14(X13)
| p15(X13) ),
inference(resolution,[],[f93,f127]) ).
fof(f145,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ r1(sK38,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| p15(X12)
| p1(X12) ),
inference(resolution,[],[f92,f143]) ).
fof(f146,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ r1(sK38,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| p14(X12)
| p15(X12) ),
inference(resolution,[],[f92,f144]) ).
fof(f147,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK39,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| p14(X11)
| p15(X11) ),
inference(resolution,[],[f146,f91]) ).
fof(f148,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK40,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| p14(X10)
| p15(X10) ),
inference(resolution,[],[f147,f90]) ).
fof(f149,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK39,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| p15(X11)
| p1(X11) ),
inference(resolution,[],[f145,f91]) ).
fof(f150,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK40,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| p15(X10)
| p1(X10) ),
inference(resolution,[],[f149,f90]) ).
fof(f151,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK41,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| p15(X9)
| p1(X9) ),
inference(resolution,[],[f89,f150]) ).
fof(f152,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK41,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| p14(X9)
| p15(X9) ),
inference(resolution,[],[f89,f148]) ).
fof(f153,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ r1(sK42,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| p15(X8)
| p1(X8) ),
inference(resolution,[],[f88,f151]) ).
fof(f154,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ r1(sK42,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| p14(X8)
| p15(X8) ),
inference(resolution,[],[f88,f152]) ).
fof(f174,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(sK43,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p14(X7)
| p15(X7) ),
inference(resolution,[],[f154,f87]) ).
fof(f175,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK44,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p14(X6)
| p15(X6) ),
inference(resolution,[],[f174,f86]) ).
fof(f176,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK45,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p14(X5)
| p15(X5) ),
inference(resolution,[],[f175,f85]) ).
fof(f177,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK46,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p14(X4)
| p15(X4) ),
inference(resolution,[],[f176,f84]) ).
fof(f178,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK47,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p14(X3)
| p15(X3) ),
inference(resolution,[],[f177,f83]) ).
fof(f179,plain,
! [X2,X0,X1] :
( ~ r1(sK48,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p14(X2)
| p15(X2) ),
inference(resolution,[],[f178,f82]) ).
fof(f180,plain,
! [X0,X1] :
( ~ r1(sK49,X0)
| ~ r1(X0,X1)
| p14(X1)
| p15(X1) ),
inference(resolution,[],[f179,f81]) ).
fof(f181,plain,
! [X0] :
( ~ r1(sK50,X0)
| p14(X0)
| p15(X0) ),
inference(resolution,[],[f180,f80]) ).
fof(f182,plain,
( p14(sK51)
| p15(sK51) ),
inference(resolution,[],[f181,f79]) ).
fof(f184,definition,
( spl52_3
<=> p15(sK51) ),
introduced(definition,[new_symbols(definition,[spl52_3])],[avatar_definition]) ).
fof(f185,plain,
( p15(sK51)
| ~ spl52_3 ),
inference(avatar_component_clause,[],[f184]) ).
fof(f187,definition,
( spl52_4
<=> p14(sK51) ),
introduced(definition,[new_symbols(definition,[spl52_4])],[avatar_definition]) ).
fof(f188,plain,
( p14(sK51)
| ~ spl52_4 ),
inference(avatar_component_clause,[],[f187]) ).
fof(f189,plain,
( spl52_3
| spl52_4 ),
inference(avatar_split_clause,[],[f182,f187,f184]) ).
fof(f206,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(sK43,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p15(X7)
| p1(X7) ),
inference(resolution,[],[f153,f87]) ).
fof(f207,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK44,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p15(X6)
| p1(X6) ),
inference(resolution,[],[f206,f86]) ).
fof(f208,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK45,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p15(X5)
| p1(X5) ),
inference(resolution,[],[f207,f85]) ).
fof(f209,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK46,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p15(X4)
| p1(X4) ),
inference(resolution,[],[f208,f84]) ).
fof(f210,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK47,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p15(X3)
| p1(X3) ),
inference(resolution,[],[f209,f83]) ).
fof(f211,plain,
! [X2,X0,X1] :
( ~ r1(sK48,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p15(X2)
| p1(X2) ),
inference(resolution,[],[f210,f82]) ).
fof(f212,plain,
! [X0,X1] :
( ~ r1(sK49,X0)
| ~ r1(X0,X1)
| p15(X1)
| p1(X1) ),
inference(resolution,[],[f211,f81]) ).
fof(f213,plain,
! [X0] :
( ~ r1(sK50,X0)
| p15(X0)
| p1(X0) ),
inference(resolution,[],[f212,f80]) ).
fof(f214,plain,
( p15(sK51)
| p1(sK51) ),
inference(resolution,[],[f213,f79]) ).
fof(f373,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X5,X12,X13] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ r1(X13,X14)
| ~ r1(X14,sK51)
| ~ r1(sK16,X0)
| ~ p14(sK51) )
| ~ spl52_3 ),
inference(resolution,[],[f185,f98]) ).
fof(f374,plain,
( ~ p14(sK51)
| spl52_4 ),
inference(avatar_component_clause,[],[f187]) ).
fof(f376,definition,
( spl52_16
<=> ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X5,X12,X13] :
( ~ r1(X0,X1)
| ~ r1(sK16,X0)
| ~ r1(X14,sK51)
| ~ r1(X13,X14)
| ~ r1(X12,X13)
| ~ r1(X11,X12)
| ~ r1(X10,X11)
| ~ r1(X9,X10)
| ~ r1(X8,X9)
| ~ r1(X7,X8)
| ~ r1(X6,X7)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl52_16])],[avatar_definition]) ).
fof(f377,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X5,X12,X13] :
( ~ r1(X14,sK51)
| ~ r1(sK16,X0)
| ~ r1(X0,X1)
| ~ r1(X13,X14)
| ~ r1(X12,X13)
| ~ r1(X11,X12)
| ~ r1(X10,X11)
| ~ r1(X9,X10)
| ~ r1(X8,X9)
| ~ r1(X7,X8)
| ~ r1(X6,X7)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2) )
| ~ spl52_16 ),
inference(avatar_component_clause,[],[f376]) ).
fof(f378,plain,
( ~ spl52_4
| spl52_16
| ~ spl52_3 ),
inference(avatar_split_clause,[],[f373,f184,f376,f187]) ).
fof(f379,plain,
! [X2,X0,X1] :
( ~ r1(sK37,X0)
| ~ r1(X1,X2)
| sP2(X2)
| ~ r1(X0,X1) ),
inference(resolution,[],[f142,f25]) ).
fof(f381,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ p11(X13)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ p12(X13)
| ~ r1(X0,X1)
| ~ r1(sK37,X0) ),
inference(resolution,[],[f142,f28]) ).
fof(f382,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ r1(sK37,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| p11(X13)
| p12(X13)
| ~ r1(X0,X1) ),
inference(resolution,[],[f142,f29]) ).
fof(f384,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ r1(sK37,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| p12(X13)
| p13(X13)
| ~ r1(X0,X1) ),
inference(resolution,[],[f142,f33]) ).
fof(f385,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ p13(X13)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ p14(X13)
| ~ r1(X0,X1)
| ~ r1(sK37,X0) ),
inference(resolution,[],[f142,f36]) ).
fof(f386,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ r1(sK37,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| p13(X13)
| p14(X13)
| ~ r1(X0,X1) ),
inference(resolution,[],[f142,f37]) ).
fof(f387,plain,
! [X0,X1] :
( ~ r1(sK38,X0)
| sP2(X1)
| ~ r1(X0,X1) ),
inference(resolution,[],[f379,f92]) ).
fof(f388,plain,
! [X0] :
( ~ r1(sK39,X0)
| sP2(X0) ),
inference(resolution,[],[f387,f91]) ).
fof(f389,plain,
sP2(sK40),
inference(resolution,[],[f388,f90]) ).
fof(f390,plain,
! [X2,X0,X1] :
( ~ r1(sK40,X0)
| ~ r1(X1,X2)
| sP1(X2)
| ~ r1(X0,X1) ),
inference(resolution,[],[f389,f38]) ).
fof(f391,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ p9(X10)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X0,X1)
| ~ p8(X10)
| ~ r1(sK40,X0) ),
inference(resolution,[],[f389,f41]) ).
fof(f392,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK40,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| p8(X10)
| p9(X10)
| ~ r1(X0,X1) ),
inference(resolution,[],[f389,f42]) ).
fof(f393,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ p9(X10)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ p10(X10)
| ~ r1(X0,X1)
| ~ r1(sK40,X0) ),
inference(resolution,[],[f389,f45]) ).
fof(f394,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK40,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| p9(X10)
| p10(X10)
| ~ r1(X0,X1) ),
inference(resolution,[],[f389,f46]) ).
fof(f396,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK40,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| p10(X10)
| p11(X10)
| ~ r1(X0,X1) ),
inference(resolution,[],[f389,f50]) ).
fof(f397,plain,
! [X0,X1] :
( ~ r1(sK41,X0)
| sP1(X1)
| ~ r1(X0,X1) ),
inference(resolution,[],[f390,f89]) ).
fof(f398,plain,
! [X0] :
( ~ r1(sK42,X0)
| sP1(X0) ),
inference(resolution,[],[f397,f88]) ).
fof(f399,plain,
sP1(sK43),
inference(resolution,[],[f398,f87]) ).
fof(f400,plain,
! [X2,X0,X1] :
( ~ r1(sK43,X0)
| ~ r1(X1,X2)
| sP0(X2)
| ~ r1(X0,X1) ),
inference(resolution,[],[f399,f51]) ).
fof(f402,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ p6(X7)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X0,X1)
| ~ p5(X7)
| ~ r1(sK43,X0) ),
inference(resolution,[],[f399,f54]) ).
fof(f403,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(sK43,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p5(X7)
| p6(X7)
| ~ r1(X0,X1) ),
inference(resolution,[],[f399,f55]) ).
fof(f404,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ p6(X7)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ p7(X7)
| ~ r1(X0,X1)
| ~ r1(sK43,X0) ),
inference(resolution,[],[f399,f58]) ).
fof(f405,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(sK43,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p6(X7)
| p7(X7)
| ~ r1(X0,X1) ),
inference(resolution,[],[f399,f59]) ).
fof(f406,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ p8(X7)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X0,X1)
| ~ p7(X7)
| ~ r1(sK43,X0) ),
inference(resolution,[],[f399,f62]) ).
fof(f407,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(sK43,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p7(X7)
| p8(X7)
| ~ r1(X0,X1) ),
inference(resolution,[],[f399,f63]) ).
fof(f408,plain,
! [X0,X1] :
( ~ r1(sK44,X0)
| sP0(X1)
| ~ r1(X0,X1) ),
inference(resolution,[],[f400,f86]) ).
fof(f409,plain,
! [X0] :
( ~ r1(sK45,X0)
| sP0(X0) ),
inference(resolution,[],[f408,f85]) ).
fof(f410,plain,
sP0(sK46),
inference(resolution,[],[f409,f84]) ).
fof(f411,plain,
! [X2,X3,X0,X1,X4] :
( ~ p2(X4)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X0,X1)
| ~ p1(X4)
| ~ r1(sK46,X0) ),
inference(resolution,[],[f410,f64]) ).
fof(f412,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK46,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| p2(X4)
| ~ r1(X0,X1) ),
inference(resolution,[],[f410,f65]) ).
fof(f414,plain,
! [X2,X3,X0,X1,X4] :
( ~ p2(X4)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ p3(X4)
| ~ r1(X0,X1)
| ~ r1(sK46,X0) ),
inference(resolution,[],[f410,f68]) ).
fof(f415,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK46,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p2(X4)
| p3(X4)
| ~ r1(X0,X1) ),
inference(resolution,[],[f410,f69]) ).
fof(f416,plain,
! [X2,X3,X0,X1,X4] :
( ~ p4(X4)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X0,X1)
| ~ p3(X4)
| ~ r1(sK46,X0) ),
inference(resolution,[],[f410,f72]) ).
fof(f417,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK46,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p3(X4)
| p4(X4)
| ~ r1(X0,X1) ),
inference(resolution,[],[f410,f73]) ).
fof(f418,plain,
! [X2,X3,X0,X1,X4] :
( ~ p4(X4)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ p5(X4)
| ~ r1(X0,X1)
| ~ r1(sK46,X0) ),
inference(resolution,[],[f410,f76]) ).
fof(f419,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK46,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p4(X4)
| p5(X4)
| ~ r1(X0,X1) ),
inference(resolution,[],[f410,f77]) ).
fof(f420,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK47,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p4(X3)
| p5(X3)
| ~ r1(X0,X1) ),
inference(resolution,[],[f419,f83]) ).
fof(f421,plain,
! [X2,X0,X1] :
( ~ r1(sK48,X0)
| ~ r1(X1,X2)
| p4(X2)
| p5(X2)
| ~ r1(X0,X1) ),
inference(resolution,[],[f420,f82]) ).
fof(f422,plain,
! [X0,X1] :
( ~ r1(sK49,X0)
| p4(X1)
| p5(X1)
| ~ r1(X0,X1) ),
inference(resolution,[],[f421,f81]) ).
fof(f423,plain,
! [X0] :
( ~ r1(sK50,X0)
| p5(X0)
| p4(X0) ),
inference(resolution,[],[f422,f80]) ).
fof(f424,plain,
( p5(sK51)
| p4(sK51) ),
inference(resolution,[],[f423,f79]) ).
fof(f426,definition,
( spl52_17
<=> p4(sK51) ),
introduced(definition,[new_symbols(definition,[spl52_17])],[avatar_definition]) ).
fof(f427,plain,
( p4(sK51)
| ~ spl52_17 ),
inference(avatar_component_clause,[],[f426]) ).
fof(f429,definition,
( spl52_18
<=> p5(sK51) ),
introduced(definition,[new_symbols(definition,[spl52_18])],[avatar_definition]) ).
fof(f430,plain,
( p5(sK51)
| ~ spl52_18 ),
inference(avatar_component_clause,[],[f429]) ).
fof(f431,plain,
( spl52_17
| spl52_18 ),
inference(avatar_split_clause,[],[f424,f429,f426]) ).
fof(f432,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK47,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p3(X3)
| p4(X3)
| ~ r1(X0,X1) ),
inference(resolution,[],[f417,f83]) ).
fof(f433,plain,
! [X2,X0,X1] :
( ~ r1(sK48,X0)
| ~ r1(X1,X2)
| p3(X2)
| p4(X2)
| ~ r1(X0,X1) ),
inference(resolution,[],[f432,f82]) ).
fof(f434,plain,
! [X0,X1] :
( ~ r1(sK49,X0)
| p3(X1)
| p4(X1)
| ~ r1(X0,X1) ),
inference(resolution,[],[f433,f81]) ).
fof(f435,plain,
! [X0] :
( ~ r1(sK50,X0)
| p4(X0)
| p3(X0) ),
inference(resolution,[],[f434,f80]) ).
fof(f436,plain,
( p4(sK51)
| p3(sK51) ),
inference(resolution,[],[f435,f79]) ).
fof(f437,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK47,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p2(X3)
| p3(X3)
| ~ r1(X0,X1) ),
inference(resolution,[],[f415,f83]) ).
fof(f438,plain,
! [X2,X0,X1] :
( ~ r1(sK48,X0)
| ~ r1(X1,X2)
| p2(X2)
| p3(X2)
| ~ r1(X0,X1) ),
inference(resolution,[],[f437,f82]) ).
fof(f439,plain,
! [X0,X1] :
( ~ r1(sK49,X0)
| p2(X1)
| p3(X1)
| ~ r1(X0,X1) ),
inference(resolution,[],[f438,f81]) ).
fof(f440,plain,
! [X0] :
( ~ r1(sK50,X0)
| p3(X0)
| p2(X0) ),
inference(resolution,[],[f439,f80]) ).
fof(f441,plain,
( p3(sK51)
| p2(sK51) ),
inference(resolution,[],[f440,f79]) ).
fof(f443,definition,
( spl52_19
<=> p2(sK51) ),
introduced(definition,[new_symbols(definition,[spl52_19])],[avatar_definition]) ).
fof(f444,plain,
( p2(sK51)
| ~ spl52_19 ),
inference(avatar_component_clause,[],[f443]) ).
fof(f446,definition,
( spl52_20
<=> p3(sK51) ),
introduced(definition,[new_symbols(definition,[spl52_20])],[avatar_definition]) ).
fof(f447,plain,
( p3(sK51)
| ~ spl52_20 ),
inference(avatar_component_clause,[],[f446]) ).
fof(f448,plain,
( spl52_19
| spl52_20 ),
inference(avatar_split_clause,[],[f441,f446,f443]) ).
fof(f449,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK47,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| p2(X3)
| ~ r1(X0,X1) ),
inference(resolution,[],[f412,f83]) ).
fof(f450,plain,
! [X2,X0,X1] :
( ~ r1(sK48,X0)
| ~ r1(X1,X2)
| p1(X2)
| p2(X2)
| ~ r1(X0,X1) ),
inference(resolution,[],[f449,f82]) ).
fof(f451,plain,
! [X0,X1] :
( ~ r1(sK49,X0)
| p1(X1)
| p2(X1)
| ~ r1(X0,X1) ),
inference(resolution,[],[f450,f81]) ).
fof(f452,plain,
! [X0] :
( ~ r1(sK50,X0)
| p2(X0)
| p1(X0) ),
inference(resolution,[],[f451,f80]) ).
fof(f453,plain,
( p2(sK51)
| p1(sK51) ),
inference(resolution,[],[f452,f79]) ).
fof(f454,plain,
( ! [X2,X3,X0,X1] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,sK51)
| ~ r1(X3,X0)
| ~ p3(sK51)
| ~ r1(sK46,X3) )
| ~ spl52_17 ),
inference(resolution,[],[f427,f416]) ).
fof(f455,plain,
( ! [X2,X3,X0,X1] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,sK51)
| ~ p5(sK51)
| ~ r1(X3,X0)
| ~ r1(sK46,X3) )
| ~ spl52_17 ),
inference(resolution,[],[f427,f418]) ).
fof(f456,plain,
( ~ p5(sK51)
| spl52_18 ),
inference(avatar_component_clause,[],[f429]) ).
fof(f458,definition,
( spl52_21
<=> ! [X0,X3,X2,X1] :
( ~ r1(X0,X1)
| ~ r1(sK46,X3)
| ~ r1(X3,X0)
| ~ r1(X2,sK51)
| ~ r1(X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl52_21])],[avatar_definition]) ).
fof(f459,plain,
( ! [X2,X3,X0,X1] :
( ~ r1(sK46,X3)
| ~ r1(X0,X1)
| ~ r1(X3,X0)
| ~ r1(X2,sK51)
| ~ r1(X1,X2) )
| ~ spl52_21 ),
inference(avatar_component_clause,[],[f458]) ).
fof(f460,plain,
( ~ spl52_18
| spl52_21
| ~ spl52_17 ),
inference(avatar_split_clause,[],[f455,f426,f458,f429]) ).
fof(f461,plain,
( ~ p3(sK51)
| spl52_20 ),
inference(avatar_component_clause,[],[f446]) ).
fof(f462,plain,
( ~ spl52_20
| spl52_21
| ~ spl52_17 ),
inference(avatar_split_clause,[],[f454,f426,f458,f446]) ).
fof(f463,plain,
( ! [X2,X3,X0,X1] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,sK51)
| ~ p3(sK51)
| ~ r1(X3,X0)
| ~ r1(sK46,X3) )
| ~ spl52_19 ),
inference(resolution,[],[f444,f414]) ).
fof(f464,plain,
( ! [X2,X3,X0,X1] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,sK51)
| ~ r1(X3,X0)
| ~ p1(sK51)
| ~ r1(sK46,X3) )
| ~ spl52_19 ),
inference(resolution,[],[f444,f411]) ).
fof(f467,definition,
( spl52_22
<=> p1(sK51) ),
introduced(definition,[new_symbols(definition,[spl52_22])],[avatar_definition]) ).
fof(f473,plain,
( ~ spl52_22
| spl52_21
| ~ spl52_19 ),
inference(avatar_split_clause,[],[f464,f443,f458,f467]) ).
fof(f475,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ r1(sK38,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| p11(X12)
| p12(X12)
| ~ r1(X0,X1) ),
inference(resolution,[],[f382,f92]) ).
fof(f476,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ r1(sK38,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| p12(X12)
| p13(X12)
| ~ r1(X0,X1) ),
inference(resolution,[],[f384,f92]) ).
fof(f477,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK44,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p7(X6)
| p8(X6)
| ~ r1(X0,X1) ),
inference(resolution,[],[f407,f86]) ).
fof(f478,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK45,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p7(X5)
| p8(X5)
| ~ r1(X0,X1) ),
inference(resolution,[],[f477,f85]) ).
fof(f479,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK46,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p7(X4)
| p8(X4)
| ~ r1(X0,X1) ),
inference(resolution,[],[f478,f84]) ).
fof(f480,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK47,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p7(X3)
| p8(X3)
| ~ r1(X0,X1) ),
inference(resolution,[],[f479,f83]) ).
fof(f481,plain,
! [X2,X0,X1] :
( ~ r1(sK48,X0)
| ~ r1(X1,X2)
| p7(X2)
| p8(X2)
| ~ r1(X0,X1) ),
inference(resolution,[],[f480,f82]) ).
fof(f482,plain,
! [X0,X1] :
( ~ r1(sK49,X0)
| p7(X1)
| p8(X1)
| ~ r1(X0,X1) ),
inference(resolution,[],[f481,f81]) ).
fof(f483,plain,
! [X0] :
( ~ r1(sK50,X0)
| p8(X0)
| p7(X0) ),
inference(resolution,[],[f482,f80]) ).
fof(f484,plain,
( p8(sK51)
| p7(sK51) ),
inference(resolution,[],[f483,f79]) ).
fof(f486,definition,
( spl52_24
<=> p7(sK51) ),
introduced(definition,[new_symbols(definition,[spl52_24])],[avatar_definition]) ).
fof(f487,plain,
( p7(sK51)
| ~ spl52_24 ),
inference(avatar_component_clause,[],[f486]) ).
fof(f489,definition,
( spl52_25
<=> p8(sK51) ),
introduced(definition,[new_symbols(definition,[spl52_25])],[avatar_definition]) ).
fof(f490,plain,
( p8(sK51)
| ~ spl52_25 ),
inference(avatar_component_clause,[],[f489]) ).
fof(f491,plain,
( spl52_24
| spl52_25 ),
inference(avatar_split_clause,[],[f484,f489,f486]) ).
fof(f494,plain,
( ~ p8(sK51)
| spl52_25 ),
inference(avatar_component_clause,[],[f489]) ).
fof(f505,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK44,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p6(X6)
| p7(X6)
| ~ r1(X0,X1) ),
inference(resolution,[],[f405,f86]) ).
fof(f506,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK45,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p6(X5)
| p7(X5)
| ~ r1(X0,X1) ),
inference(resolution,[],[f505,f85]) ).
fof(f507,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK46,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p6(X4)
| p7(X4)
| ~ r1(X0,X1) ),
inference(resolution,[],[f506,f84]) ).
fof(f508,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK47,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p6(X3)
| p7(X3)
| ~ r1(X0,X1) ),
inference(resolution,[],[f507,f83]) ).
fof(f509,plain,
! [X2,X0,X1] :
( ~ r1(sK48,X0)
| ~ r1(X1,X2)
| p6(X2)
| p7(X2)
| ~ r1(X0,X1) ),
inference(resolution,[],[f508,f82]) ).
fof(f510,plain,
! [X0,X1] :
( ~ r1(sK49,X0)
| p6(X1)
| p7(X1)
| ~ r1(X0,X1) ),
inference(resolution,[],[f509,f81]) ).
fof(f511,plain,
! [X0] :
( ~ r1(sK50,X0)
| p7(X0)
| p6(X0) ),
inference(resolution,[],[f510,f80]) ).
fof(f512,plain,
( p7(sK51)
| p6(sK51) ),
inference(resolution,[],[f511,f79]) ).
fof(f513,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK44,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p5(X6)
| p6(X6)
| ~ r1(X0,X1) ),
inference(resolution,[],[f403,f86]) ).
fof(f514,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK45,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p5(X5)
| p6(X5)
| ~ r1(X0,X1) ),
inference(resolution,[],[f513,f85]) ).
fof(f515,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK46,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p5(X4)
| p6(X4)
| ~ r1(X0,X1) ),
inference(resolution,[],[f514,f84]) ).
fof(f516,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK47,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p5(X3)
| p6(X3)
| ~ r1(X0,X1) ),
inference(resolution,[],[f515,f83]) ).
fof(f517,plain,
! [X2,X0,X1] :
( ~ r1(sK48,X0)
| ~ r1(X1,X2)
| p5(X2)
| p6(X2)
| ~ r1(X0,X1) ),
inference(resolution,[],[f516,f82]) ).
fof(f518,plain,
! [X0,X1] :
( ~ r1(sK49,X0)
| p5(X1)
| p6(X1)
| ~ r1(X0,X1) ),
inference(resolution,[],[f517,f81]) ).
fof(f519,plain,
! [X0] :
( ~ r1(sK50,X0)
| p6(X0)
| p5(X0) ),
inference(resolution,[],[f518,f80]) ).
fof(f520,plain,
( p6(sK51)
| p5(sK51) ),
inference(resolution,[],[f519,f79]) ).
fof(f524,plain,
( p4(sK51)
| spl52_20 ),
inference(forward_subsumption_resolution,[],[f436,f461]) ).
fof(f525,plain,
( spl52_17
| spl52_20 ),
inference(avatar_split_clause,[],[f524,f446,f426]) ).
fof(f526,plain,
( ! [X2,X3,X0,X1] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,sK51)
| ~ r1(X3,X0)
| ~ r1(sK46,X3) )
| ~ spl52_19
| ~ spl52_20 ),
inference(forward_subsumption_resolution,[],[f463,f447]) ).
fof(f527,plain,
( spl52_21
| ~ spl52_19
| ~ spl52_20 ),
inference(avatar_split_clause,[],[f526,f446,f443,f458]) ).
fof(f530,plain,
( $false
| ~ spl52_21 ),
inference(unit_resulting_resolution,[],[f459,f80,f79,f81,f82,f83]) ).
fof(f532,plain,
~ spl52_21,
inference(avatar_contradiction_clause,[],[f530]) ).
fof(f533,plain,
( p6(sK51)
| spl52_18 ),
inference(forward_subsumption_resolution,[],[f520,f456]) ).
fof(f548,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ r1(sK38,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| p13(X12)
| p14(X12)
| ~ r1(X0,X1) ),
inference(resolution,[],[f386,f92]) ).
fof(f553,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK39,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| p12(X11)
| p13(X11)
| ~ r1(X0,X1) ),
inference(resolution,[],[f476,f91]) ).
fof(f554,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK40,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| p12(X10)
| p13(X10)
| ~ r1(X0,X1) ),
inference(resolution,[],[f553,f90]) ).
fof(f555,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK41,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| p12(X9)
| p13(X9)
| ~ r1(X0,X1) ),
inference(resolution,[],[f554,f89]) ).
fof(f556,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ r1(sK42,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| p12(X8)
| p13(X8)
| ~ r1(X0,X1) ),
inference(resolution,[],[f555,f88]) ).
fof(f557,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(sK43,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p12(X7)
| p13(X7)
| ~ r1(X0,X1) ),
inference(resolution,[],[f556,f87]) ).
fof(f558,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK44,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p12(X6)
| p13(X6)
| ~ r1(X0,X1) ),
inference(resolution,[],[f557,f86]) ).
fof(f559,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK45,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p12(X5)
| p13(X5)
| ~ r1(X0,X1) ),
inference(resolution,[],[f558,f85]) ).
fof(f560,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK46,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p12(X4)
| p13(X4)
| ~ r1(X0,X1) ),
inference(resolution,[],[f559,f84]) ).
fof(f561,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK47,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p12(X3)
| p13(X3)
| ~ r1(X0,X1) ),
inference(resolution,[],[f560,f83]) ).
fof(f562,plain,
! [X2,X0,X1] :
( ~ r1(sK48,X0)
| ~ r1(X1,X2)
| p12(X2)
| p13(X2)
| ~ r1(X0,X1) ),
inference(resolution,[],[f561,f82]) ).
fof(f563,plain,
! [X0,X1] :
( ~ r1(sK49,X0)
| p12(X1)
| p13(X1)
| ~ r1(X0,X1) ),
inference(resolution,[],[f562,f81]) ).
fof(f564,plain,
! [X0] :
( ~ r1(sK50,X0)
| p13(X0)
| p12(X0) ),
inference(resolution,[],[f563,f80]) ).
fof(f565,plain,
( p13(sK51)
| p12(sK51) ),
inference(resolution,[],[f564,f79]) ).
fof(f567,definition,
( spl52_28
<=> p12(sK51) ),
introduced(definition,[new_symbols(definition,[spl52_28])],[avatar_definition]) ).
fof(f568,plain,
( p12(sK51)
| ~ spl52_28 ),
inference(avatar_component_clause,[],[f567]) ).
fof(f570,definition,
( spl52_29
<=> p13(sK51) ),
introduced(definition,[new_symbols(definition,[spl52_29])],[avatar_definition]) ).
fof(f571,plain,
( p13(sK51)
| ~ spl52_29 ),
inference(avatar_component_clause,[],[f570]) ).
fof(f572,plain,
( spl52_28
| spl52_29 ),
inference(avatar_split_clause,[],[f565,f570,f567]) ).
fof(f577,plain,
( ~ p12(sK51)
| spl52_28 ),
inference(avatar_component_clause,[],[f567]) ).
fof(f583,definition,
( spl52_31
<=> ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ r1(X0,X1)
| ~ r1(sK37,X12)
| ~ r1(X12,X0)
| ~ r1(X11,sK51)
| ~ r1(X10,X11)
| ~ r1(X9,X10)
| ~ r1(X8,X9)
| ~ r1(X7,X8)
| ~ r1(X6,X7)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl52_31])],[avatar_definition]) ).
fof(f584,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ r1(sK37,X12)
| ~ r1(X0,X1)
| ~ r1(X12,X0)
| ~ r1(X11,sK51)
| ~ r1(X10,X11)
| ~ r1(X9,X10)
| ~ r1(X8,X9)
| ~ r1(X7,X8)
| ~ r1(X6,X7)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2) )
| ~ spl52_31 ),
inference(avatar_component_clause,[],[f583]) ).
fof(f612,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,sK51)
| ~ p7(sK51)
| ~ r1(X6,X0)
| ~ r1(sK43,X6) )
| spl52_18 ),
inference(resolution,[],[f533,f404]) ).
fof(f617,plain,
( ~ p7(sK51)
| spl52_24 ),
inference(avatar_component_clause,[],[f486]) ).
fof(f619,definition,
( spl52_34
<=> ! [X5,X3,X4,X2,X0,X6,X1] :
( ~ r1(X0,X1)
| ~ r1(sK43,X6)
| ~ r1(X6,X0)
| ~ r1(X5,sK51)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl52_34])],[avatar_definition]) ).
fof(f620,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK43,X6)
| ~ r1(X0,X1)
| ~ r1(X6,X0)
| ~ r1(X5,sK51)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2) )
| ~ spl52_34 ),
inference(avatar_component_clause,[],[f619]) ).
fof(f621,plain,
( ~ spl52_24
| spl52_34
| spl52_18 ),
inference(avatar_split_clause,[],[f612,f429,f619,f486]) ).
fof(f622,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,sK51)
| ~ r1(X6,X0)
| ~ p7(sK51)
| ~ r1(sK43,X6) )
| ~ spl52_25 ),
inference(resolution,[],[f490,f406]) ).
fof(f650,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK41,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| p8(X9)
| p9(X9)
| ~ r1(X0,X1) ),
inference(resolution,[],[f392,f89]) ).
fof(f651,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ r1(sK42,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| p8(X8)
| p9(X8)
| ~ r1(X0,X1) ),
inference(resolution,[],[f650,f88]) ).
fof(f652,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(sK43,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p8(X7)
| p9(X7)
| ~ r1(X0,X1) ),
inference(resolution,[],[f651,f87]) ).
fof(f653,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK44,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p8(X6)
| p9(X6)
| ~ r1(X0,X1) ),
inference(resolution,[],[f652,f86]) ).
fof(f654,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK45,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p8(X5)
| p9(X5)
| ~ r1(X0,X1) ),
inference(resolution,[],[f653,f85]) ).
fof(f655,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK46,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p8(X4)
| p9(X4)
| ~ r1(X0,X1) ),
inference(resolution,[],[f654,f84]) ).
fof(f656,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK47,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p8(X3)
| p9(X3)
| ~ r1(X0,X1) ),
inference(resolution,[],[f655,f83]) ).
fof(f657,plain,
! [X2,X0,X1] :
( ~ r1(sK48,X0)
| ~ r1(X1,X2)
| p8(X2)
| p9(X2)
| ~ r1(X0,X1) ),
inference(resolution,[],[f656,f82]) ).
fof(f658,plain,
! [X0,X1] :
( ~ r1(sK49,X0)
| p8(X1)
| p9(X1)
| ~ r1(X0,X1) ),
inference(resolution,[],[f657,f81]) ).
fof(f659,plain,
! [X0] :
( ~ r1(sK50,X0)
| p9(X0)
| p8(X0) ),
inference(resolution,[],[f658,f80]) ).
fof(f660,plain,
( p9(sK51)
| p8(sK51) ),
inference(resolution,[],[f659,f79]) ).
fof(f663,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK39,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| p11(X11)
| p12(X11)
| ~ r1(X0,X1) ),
inference(resolution,[],[f475,f91]) ).
fof(f664,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK40,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| p11(X10)
| p12(X10)
| ~ r1(X0,X1) ),
inference(resolution,[],[f663,f90]) ).
fof(f665,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK41,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| p11(X9)
| p12(X9)
| ~ r1(X0,X1) ),
inference(resolution,[],[f664,f89]) ).
fof(f666,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ r1(sK42,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| p11(X8)
| p12(X8)
| ~ r1(X0,X1) ),
inference(resolution,[],[f665,f88]) ).
fof(f667,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(sK43,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p11(X7)
| p12(X7)
| ~ r1(X0,X1) ),
inference(resolution,[],[f666,f87]) ).
fof(f668,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK44,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p11(X6)
| p12(X6)
| ~ r1(X0,X1) ),
inference(resolution,[],[f667,f86]) ).
fof(f669,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK45,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p11(X5)
| p12(X5)
| ~ r1(X0,X1) ),
inference(resolution,[],[f668,f85]) ).
fof(f670,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK46,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p11(X4)
| p12(X4)
| ~ r1(X0,X1) ),
inference(resolution,[],[f669,f84]) ).
fof(f671,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK47,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p11(X3)
| p12(X3)
| ~ r1(X0,X1) ),
inference(resolution,[],[f670,f83]) ).
fof(f672,plain,
! [X2,X0,X1] :
( ~ r1(sK48,X0)
| ~ r1(X1,X2)
| p11(X2)
| p12(X2)
| ~ r1(X0,X1) ),
inference(resolution,[],[f671,f82]) ).
fof(f673,plain,
! [X0,X1] :
( ~ r1(sK49,X0)
| p11(X1)
| p12(X1)
| ~ r1(X0,X1) ),
inference(resolution,[],[f672,f81]) ).
fof(f674,plain,
! [X0] :
( ~ r1(sK50,X0)
| p12(X0)
| p11(X0) ),
inference(resolution,[],[f673,f80]) ).
fof(f675,plain,
( p12(sK51)
| p11(sK51) ),
inference(resolution,[],[f674,f79]) ).
fof(f676,plain,
( p11(sK51)
| spl52_28 ),
inference(forward_subsumption_resolution,[],[f675,f577]) ).
fof(f682,definition,
( spl52_38
<=> p10(sK51) ),
introduced(definition,[new_symbols(definition,[spl52_38])],[avatar_definition]) ).
fof(f683,plain,
( ~ p10(sK51)
| spl52_38 ),
inference(avatar_component_clause,[],[f682]) ).
fof(f689,definition,
( spl52_40
<=> ! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(sK40,X9)
| ~ r1(X9,X0)
| ~ r1(X8,sK51)
| ~ r1(X7,X8)
| ~ r1(X6,X7)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl52_40])],[avatar_definition]) ).
fof(f690,plain,
( ! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK40,X9)
| ~ r1(X0,X1)
| ~ r1(X9,X0)
| ~ r1(X8,sK51)
| ~ r1(X7,X8)
| ~ r1(X6,X7)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2) )
| ~ spl52_40 ),
inference(avatar_component_clause,[],[f689]) ).
fof(f718,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK41,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| p10(X9)
| p11(X9)
| ~ r1(X0,X1) ),
inference(resolution,[],[f396,f89]) ).
fof(f719,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ r1(sK42,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| p10(X8)
| p11(X8)
| ~ r1(X0,X1) ),
inference(resolution,[],[f718,f88]) ).
fof(f720,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(sK43,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p10(X7)
| p11(X7)
| ~ r1(X0,X1) ),
inference(resolution,[],[f719,f87]) ).
fof(f721,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK44,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p10(X6)
| p11(X6)
| ~ r1(X0,X1) ),
inference(resolution,[],[f720,f86]) ).
fof(f722,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK45,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p10(X5)
| p11(X5)
| ~ r1(X0,X1) ),
inference(resolution,[],[f721,f85]) ).
fof(f723,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK46,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p10(X4)
| p11(X4)
| ~ r1(X0,X1) ),
inference(resolution,[],[f722,f84]) ).
fof(f724,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK47,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p10(X3)
| p11(X3)
| ~ r1(X0,X1) ),
inference(resolution,[],[f723,f83]) ).
fof(f725,plain,
! [X2,X0,X1] :
( ~ r1(sK48,X0)
| ~ r1(X1,X2)
| p10(X2)
| p11(X2)
| ~ r1(X0,X1) ),
inference(resolution,[],[f724,f82]) ).
fof(f726,plain,
! [X0,X1] :
( ~ r1(sK49,X0)
| p10(X1)
| p11(X1)
| ~ r1(X0,X1) ),
inference(resolution,[],[f725,f81]) ).
fof(f727,plain,
! [X0] :
( ~ r1(sK50,X0)
| p11(X0)
| p10(X0) ),
inference(resolution,[],[f726,f80]) ).
fof(f728,plain,
( p11(sK51)
| p10(sK51) ),
inference(resolution,[],[f727,f79]) ).
fof(f741,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK41,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| p9(X9)
| p10(X9)
| ~ r1(X0,X1) ),
inference(resolution,[],[f394,f89]) ).
fof(f742,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ r1(sK42,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| p9(X8)
| p10(X8)
| ~ r1(X0,X1) ),
inference(resolution,[],[f741,f88]) ).
fof(f743,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(sK43,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p9(X7)
| p10(X7)
| ~ r1(X0,X1) ),
inference(resolution,[],[f742,f87]) ).
fof(f744,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK44,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p9(X6)
| p10(X6)
| ~ r1(X0,X1) ),
inference(resolution,[],[f743,f86]) ).
fof(f745,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK45,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p9(X5)
| p10(X5)
| ~ r1(X0,X1) ),
inference(resolution,[],[f744,f85]) ).
fof(f746,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK46,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p9(X4)
| p10(X4)
| ~ r1(X0,X1) ),
inference(resolution,[],[f745,f84]) ).
fof(f747,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK47,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p9(X3)
| p10(X3)
| ~ r1(X0,X1) ),
inference(resolution,[],[f746,f83]) ).
fof(f748,plain,
! [X2,X0,X1] :
( ~ r1(sK48,X0)
| ~ r1(X1,X2)
| p9(X2)
| p10(X2)
| ~ r1(X0,X1) ),
inference(resolution,[],[f747,f82]) ).
fof(f749,plain,
! [X0,X1] :
( ~ r1(sK49,X0)
| p9(X1)
| p10(X1)
| ~ r1(X0,X1) ),
inference(resolution,[],[f748,f81]) ).
fof(f750,plain,
! [X0] :
( ~ r1(sK50,X0)
| p10(X0)
| p9(X0) ),
inference(resolution,[],[f749,f80]) ).
fof(f751,plain,
( p10(sK51)
| p9(sK51) ),
inference(resolution,[],[f750,f79]) ).
fof(f752,plain,
( p9(sK51)
| spl52_38 ),
inference(forward_subsumption_resolution,[],[f751,f683]) ).
fof(f757,plain,
( ! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,sK51)
| ~ r1(X9,X0)
| ~ p8(sK51)
| ~ r1(sK40,X9) )
| spl52_38 ),
inference(resolution,[],[f752,f391]) ).
fof(f762,plain,
( ! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,sK51)
| ~ r1(X9,X0)
| ~ r1(sK40,X9) )
| ~ spl52_25
| spl52_38 ),
inference(forward_subsumption_resolution,[],[f757,f490]) ).
fof(f764,plain,
( spl52_40
| ~ spl52_25
| spl52_38 ),
inference(avatar_split_clause,[],[f762,f682,f489,f689]) ).
fof(f766,definition,
( spl52_41
<=> p9(sK51) ),
introduced(definition,[new_symbols(definition,[spl52_41])],[avatar_definition]) ).
fof(f767,plain,
( p9(sK51)
| ~ spl52_41 ),
inference(avatar_component_clause,[],[f766]) ).
fof(f768,plain,
( p10(sK51)
| ~ spl52_38 ),
inference(avatar_component_clause,[],[f682]) ).
fof(f771,plain,
( $false
| spl52_28
| ~ spl52_38 ),
inference(unit_resulting_resolution,[],[f49,f389,f89,f676,f88,f87,f86,f85,f84,f83,f82,f81,f80,f79,f768]) ).
fof(f773,plain,
( spl52_28
| ~ spl52_38 ),
inference(avatar_contradiction_clause,[],[f771]) ).
fof(f774,plain,
( $false
| ~ spl52_40 ),
inference(unit_resulting_resolution,[],[f690,f86,f85,f84,f83,f82,f81,f80,f79,f87,f88,f89]) ).
fof(f776,plain,
~ spl52_40,
inference(avatar_contradiction_clause,[],[f774]) ).
fof(f901,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK39,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| p13(X11)
| p14(X11)
| ~ r1(X0,X1) ),
inference(resolution,[],[f548,f91]) ).
fof(f902,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK40,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| p13(X10)
| p14(X10)
| ~ r1(X0,X1) ),
inference(resolution,[],[f901,f90]) ).
fof(f903,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK41,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| p13(X9)
| p14(X9)
| ~ r1(X0,X1) ),
inference(resolution,[],[f902,f89]) ).
fof(f904,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ r1(sK42,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| p13(X8)
| p14(X8)
| ~ r1(X0,X1) ),
inference(resolution,[],[f903,f88]) ).
fof(f905,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(sK43,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p13(X7)
| p14(X7)
| ~ r1(X0,X1) ),
inference(resolution,[],[f904,f87]) ).
fof(f906,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK44,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p13(X6)
| p14(X6)
| ~ r1(X0,X1) ),
inference(resolution,[],[f905,f86]) ).
fof(f907,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK45,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p13(X5)
| p14(X5)
| ~ r1(X0,X1) ),
inference(resolution,[],[f906,f85]) ).
fof(f908,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK46,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p13(X4)
| p14(X4)
| ~ r1(X0,X1) ),
inference(resolution,[],[f907,f84]) ).
fof(f909,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK47,X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p13(X3)
| p14(X3)
| ~ r1(X0,X1) ),
inference(resolution,[],[f908,f83]) ).
fof(f910,plain,
! [X2,X0,X1] :
( ~ r1(sK48,X0)
| ~ r1(X1,X2)
| p13(X2)
| p14(X2)
| ~ r1(X0,X1) ),
inference(resolution,[],[f909,f82]) ).
fof(f911,plain,
! [X0,X1] :
( ~ r1(sK49,X0)
| p13(X1)
| p14(X1)
| ~ r1(X0,X1) ),
inference(resolution,[],[f910,f81]) ).
fof(f912,plain,
! [X0] :
( ~ r1(sK50,X0)
| p14(X0)
| p13(X0) ),
inference(resolution,[],[f911,f80]) ).
fof(f913,plain,
( p14(sK51)
| p13(sK51) ),
inference(resolution,[],[f912,f79]) ).
fof(f914,plain,
( p13(sK51)
| spl52_4 ),
inference(forward_subsumption_resolution,[],[f913,f374]) ).
fof(f915,plain,
( spl52_29
| spl52_4 ),
inference(avatar_split_clause,[],[f914,f187,f570]) ).
fof(f916,plain,
( $false
| ~ spl52_16 ),
inference(unit_resulting_resolution,[],[f377,f92,f91,f90,f89,f88,f87,f86,f85,f84,f83,f82,f81,f80,f93,f94,f79]) ).
fof(f918,plain,
~ spl52_16,
inference(avatar_contradiction_clause,[],[f916]) ).
fof(f922,plain,
( $false
| ~ spl52_28
| ~ spl52_29 ),
inference(unit_resulting_resolution,[],[f32,f142,f92,f568,f91,f90,f89,f88,f87,f86,f85,f84,f83,f82,f81,f80,f79,f571]) ).
fof(f928,plain,
( ~ spl52_28
| ~ spl52_29 ),
inference(avatar_contradiction_clause,[],[f922]) ).
fof(f929,plain,
( p1(sK51)
| ~ spl52_22 ),
inference(avatar_component_clause,[],[f467]) ).
fof(f930,plain,
( spl52_22
| spl52_19 ),
inference(avatar_split_clause,[],[f453,f443,f467]) ).
fof(f931,plain,
( spl52_22
| spl52_3 ),
inference(avatar_split_clause,[],[f214,f184,f467]) ).
fof(f932,plain,
( p6(sK51)
| spl52_24 ),
inference(forward_subsumption_resolution,[],[f512,f617]) ).
fof(f937,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X5,X12,X13] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ r1(X13,X14)
| ~ r1(X14,sK51)
| ~ r1(sK16,X0)
| ~ p15(sK51) )
| ~ spl52_22 ),
inference(resolution,[],[f929,f102]) ).
fof(f939,plain,
( ~ spl52_3
| spl52_16
| ~ spl52_22 ),
inference(avatar_split_clause,[],[f937,f467,f376,f184]) ).
fof(f943,plain,
( $false
| ~ spl52_31 ),
inference(unit_resulting_resolution,[],[f584,f89,f88,f87,f86,f85,f84,f83,f82,f81,f80,f79,f90,f91,f92]) ).
fof(f945,plain,
~ spl52_31,
inference(avatar_contradiction_clause,[],[f943]) ).
fof(f949,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,sK51)
| ~ r1(X6,X0)
| ~ p5(sK51)
| ~ r1(sK43,X6) )
| spl52_24 ),
inference(resolution,[],[f932,f402]) ).
fof(f952,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,sK51)
| ~ r1(X6,X0)
| ~ r1(sK43,X6) )
| ~ spl52_18
| spl52_24 ),
inference(forward_subsumption_resolution,[],[f949,f430]) ).
fof(f953,plain,
( spl52_34
| ~ spl52_18
| spl52_24 ),
inference(avatar_split_clause,[],[f952,f486,f429,f619]) ).
fof(f954,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,sK51)
| ~ r1(X6,X0)
| ~ r1(sK43,X6) )
| ~ spl52_24
| ~ spl52_25 ),
inference(forward_subsumption_resolution,[],[f622,f487]) ).
fof(f955,plain,
( spl52_34
| ~ spl52_24
| ~ spl52_25 ),
inference(avatar_split_clause,[],[f954,f489,f486,f619]) ).
fof(f962,plain,
( p9(sK51)
| spl52_25 ),
inference(forward_subsumption_resolution,[],[f660,f494]) ).
fof(f963,plain,
( spl52_41
| spl52_25 ),
inference(avatar_split_clause,[],[f962,f489,f766]) ).
fof(f966,plain,
( ! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,sK51)
| ~ p10(sK51)
| ~ r1(X9,X0)
| ~ r1(sK40,X9) )
| ~ spl52_41 ),
inference(resolution,[],[f767,f393]) ).
fof(f972,plain,
( ! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,sK51)
| ~ r1(X9,X0)
| ~ r1(sK40,X9) )
| ~ spl52_38
| ~ spl52_41 ),
inference(forward_subsumption_resolution,[],[f966,f768]) ).
fof(f973,plain,
( spl52_40
| ~ spl52_38
| ~ spl52_41 ),
inference(avatar_split_clause,[],[f972,f766,f682,f689]) ).
fof(f974,plain,
( p11(sK51)
| spl52_38 ),
inference(forward_subsumption_resolution,[],[f728,f683]) ).
fof(f975,plain,
( $false
| ~ spl52_34 ),
inference(unit_resulting_resolution,[],[f620,f83,f82,f81,f80,f79,f84,f85,f86]) ).
fof(f977,plain,
~ spl52_34,
inference(avatar_contradiction_clause,[],[f975]) ).
fof(f982,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,sK51)
| ~ p12(sK51)
| ~ r1(X12,X0)
| ~ r1(sK37,X12) )
| spl52_38 ),
inference(resolution,[],[f974,f381]) ).
fof(f986,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,sK51)
| ~ r1(X12,X0)
| ~ r1(sK37,X12) )
| ~ spl52_28
| spl52_38 ),
inference(forward_subsumption_resolution,[],[f982,f568]) ).
fof(f987,plain,
( spl52_31
| ~ spl52_28
| spl52_38 ),
inference(avatar_split_clause,[],[f986,f682,f567,f583]) ).
fof(f990,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,sK51)
| ~ p14(sK51)
| ~ r1(X12,X0)
| ~ r1(sK37,X12) )
| ~ spl52_29 ),
inference(resolution,[],[f571,f385]) ).
fof(f996,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,sK51)
| ~ r1(X12,X0)
| ~ r1(sK37,X12) )
| ~ spl52_4
| ~ spl52_29 ),
inference(forward_subsumption_resolution,[],[f990,f188]) ).
fof(f997,plain,
( spl52_31
| ~ spl52_4
| ~ spl52_29 ),
inference(avatar_split_clause,[],[f996,f570,f187,f583]) ).
cnf(s2,plain,
( spl52_3
| spl52_4 ),
inference(sat_conversion,[],[f189]) ).
cnf(s17,plain,
( ~ spl52_3
| ~ spl52_4
| spl52_16 ),
inference(sat_conversion,[],[f378]) ).
cnf(s18,plain,
( spl52_17
| spl52_18 ),
inference(sat_conversion,[],[f431]) ).
cnf(s19,plain,
( spl52_19
| spl52_20 ),
inference(sat_conversion,[],[f448]) ).
cnf(s20,plain,
( ~ spl52_17
| ~ spl52_18
| spl52_21 ),
inference(sat_conversion,[],[f460]) ).
cnf(s21,plain,
( ~ spl52_17
| ~ spl52_20
| spl52_21 ),
inference(sat_conversion,[],[f462]) ).
cnf(s23,plain,
( ~ spl52_19
| spl52_21
| ~ spl52_22 ),
inference(sat_conversion,[],[f473]) ).
cnf(s24,plain,
( spl52_24
| spl52_25 ),
inference(sat_conversion,[],[f491]) ).
cnf(s28,plain,
( spl52_17
| spl52_20 ),
inference(sat_conversion,[],[f525]) ).
cnf(s29,plain,
( ~ spl52_19
| ~ spl52_20
| spl52_21 ),
inference(sat_conversion,[],[f527]) ).
cnf(s31,plain,
~ spl52_21,
inference(sat_conversion,[],[f532]) ).
cnf(s33,plain,
( spl52_28
| spl52_29 ),
inference(sat_conversion,[],[f572]) ).
cnf(s39,plain,
( spl52_18
| ~ spl52_24
| spl52_34 ),
inference(sat_conversion,[],[f621]) ).
cnf(s47,plain,
( ~ spl52_25
| spl52_38
| spl52_40 ),
inference(sat_conversion,[],[f764]) ).
cnf(s50,plain,
( spl52_28
| ~ spl52_38 ),
inference(sat_conversion,[],[f773]) ).
cnf(s51,plain,
~ spl52_40,
inference(sat_conversion,[],[f776]) ).
cnf(s89,plain,
( spl52_4
| spl52_29 ),
inference(sat_conversion,[],[f915]) ).
cnf(s90,plain,
~ spl52_16,
inference(sat_conversion,[],[f918]) ).
cnf(s94,plain,
( ~ spl52_28
| ~ spl52_29 ),
inference(sat_conversion,[],[f928]) ).
cnf(s95,plain,
( spl52_19
| spl52_22 ),
inference(sat_conversion,[],[f930]) ).
cnf(s96,plain,
( spl52_3
| spl52_22 ),
inference(sat_conversion,[],[f931]) ).
cnf(s97,plain,
( ~ spl52_3
| spl52_16
| ~ spl52_22 ),
inference(sat_conversion,[],[f939]) ).
cnf(s98,plain,
~ spl52_31,
inference(sat_conversion,[],[f945]) ).
cnf(s101,plain,
( ~ spl52_18
| spl52_24
| spl52_34 ),
inference(sat_conversion,[],[f953]) ).
cnf(s102,plain,
( ~ spl52_24
| ~ spl52_25
| spl52_34 ),
inference(sat_conversion,[],[f955]) ).
cnf(s105,plain,
( spl52_25
| spl52_41 ),
inference(sat_conversion,[],[f963]) ).
cnf(s108,plain,
( ~ spl52_38
| spl52_40
| ~ spl52_41 ),
inference(sat_conversion,[],[f973]) ).
cnf(s109,plain,
~ spl52_34,
inference(sat_conversion,[],[f977]) ).
cnf(s112,plain,
( ~ spl52_28
| spl52_31
| spl52_38 ),
inference(sat_conversion,[],[f987]) ).
cnf(s115,plain,
( ~ spl52_4
| ~ spl52_29
| spl52_31 ),
inference(sat_conversion,[],[f997]) ).
cnf(s116,plain,
( ~ spl52_24
| ~ spl52_25 ),
inference(rat,[],[s102,s109]) ).
cnf(s117,plain,
( ~ spl52_18
| spl52_24 ),
inference(rat,[],[s101,s109]) ).
cnf(s118,plain,
( ~ spl52_25
| spl52_38 ),
inference(rat,[],[s47,s51]) ).
cnf(s120,plain,
( spl52_18
| ~ spl52_24 ),
inference(rat,[],[s39,s109]) ).
cnf(s122,plain,
( ~ spl52_19
| ~ spl52_20 ),
inference(rat,[],[s29,s31]) ).
cnf(s123,plain,
( ~ spl52_19
| ~ spl52_22 ),
inference(rat,[],[s23,s31]) ).
cnf(s124,plain,
( ~ spl52_17
| ~ spl52_20 ),
inference(rat,[],[s21,s31]) ).
cnf(s125,plain,
( ~ spl52_17
| ~ spl52_18 ),
inference(rat,[],[s20,s31]) ).
cnf(s126,plain,
( ~ spl52_3
| ~ spl52_4 ),
inference(rat,[],[s17,s90]) ).
cnf(s131,plain,
spl52_3,
inference(rat,[],[s116,s105,s117,s108,s18,s112,s124,s33,s19,s115,s123,s2,s96,s51,s98]) ).
cnf(s132,plain,
~ spl52_22,
inference(rat,[],[s97,s90,s131]) ).
cnf(s133,plain,
~ spl52_4,
inference(rat,[],[s126,s131]) ).
cnf(s134,plain,
spl52_19,
inference(rat,[],[s95,s132]) ).
cnf(s135,plain,
spl52_29,
inference(rat,[],[s89,s133]) ).
cnf(s136,plain,
~ spl52_20,
inference(rat,[],[s122,s134]) ).
cnf(s137,plain,
~ spl52_28,
inference(rat,[],[s94,s135]) ).
cnf(s138,plain,
spl52_17,
inference(rat,[],[s28,s136]) ).
cnf(s139,plain,
~ spl52_38,
inference(rat,[],[s50,s137]) ).
cnf(s140,plain,
~ spl52_18,
inference(rat,[],[s125,s138]) ).
cnf(s142,plain,
~ spl52_25,
inference(rat,[],[s118,s139]) ).
cnf(s143,plain,
~ spl52_24,
inference(rat,[],[s120,s140]) ).
cnf(s145,plain,
$false,
inference(rat,[],[s24,s142,s143]) ).
fof(f998,plain,
$false,
inference(avatar_sat_refutation,[],[s145]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL650+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.39 % Computer : n026.cluster.edu
% 0.10/0.39 % Model : x86_64 x86_64
% 0.10/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.39 % Memory : 8046.5625MB
% 0.10/0.39 % OS : Linux 6.8.0-71-generic
% 0.10/0.39 % CPULimit : 300
% 0.10/0.39 % WCLimit : 300
% 0.10/0.39 % DateTime : Sun Sep 27 16:19:01 UTC 2026
% 0.10/0.39 % CPUTime :
% 0.10/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.43 Running first-order theorem proving
% 0.10/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.80/2.29 % (3040966)Detected formulas, will run a generic FOF schedule.
% 9.80/2.29 % (3040976)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2913330681:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 9.80/2.29 % (3040976)Instruction limit reached!
% 9.80/2.29 % (3040976)------------------------------
% 9.80/2.29 % (3040976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.80/2.29 % (3040976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.80/2.29 % (3040976)CaDiCaL version: 2.1.3
% 9.80/2.29 % (3040976)Termination reason: Instruction limit
% 9.80/2.29 % (3040976)Termination phase: Saturation
% 9.80/2.29 % (3040976)Time elapsed: 0.030 s
% 9.80/2.29 % (3040976)Peak memory usage: 88 MB
% 9.80/2.29 % (3040976)Instructions burned: 139 (million)
% 9.80/2.29 % (3040971)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3126544727:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 9.80/2.29 % (3040972)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1334873462:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 9.80/2.29 % (3040975)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=54635634:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 9.80/2.29 % (3040977)dis-21_1_sil=8000:lcm=predicate:random_seed=3648621658:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 9.80/2.29 % (3040973)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=681362349:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 9.80/2.29 % (3040974)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1112858175:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 9.80/2.29 % (3040977)Instruction limit reached!
% 9.80/2.29 % (3040977)------------------------------
% 9.80/2.29 % (3040977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.80/2.29 % (3040977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.80/2.29 % (3040977)CaDiCaL version: 2.1.3
% 9.80/2.29 % (3040977)Termination reason: Instruction limit
% 9.80/2.29 % (3040977)Termination phase: Saturation
% 9.80/2.29 % (3040977)Time elapsed: 0.043 s
% 9.80/2.29 % (3040977)Peak memory usage: 88 MB
% 9.80/2.29 % (3040977)Instructions burned: 130 (million)
% 9.80/2.29 % (3040975)Instruction limit reached!
% 9.80/2.29 % (3040975)------------------------------
% 9.80/2.29 % (3040975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.80/2.29 % (3040975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.80/2.29 % (3040975)CaDiCaL version: 2.1.3
% 9.80/2.29 % (3040975)Termination reason: Instruction limit
% 9.80/2.29 % (3040975)Termination phase: Saturation
% 9.80/2.29 % (3040975)Time elapsed: 0.047 s
% 9.80/2.29 % (3040975)Peak memory usage: 88 MB
% 9.80/2.29 % (3040975)Instructions burned: 122 (million)
% 9.80/2.29 % (3040974)Instruction limit reached!
% 9.80/2.29 % (3040974)------------------------------
% 9.80/2.29 % (3040974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.80/2.29 % (3040974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.80/2.29 % (3040974)CaDiCaL version: 2.1.3
% 9.80/2.29 % (3040974)Termination reason: Instruction limit
% 9.80/2.29 % (3040974)Termination phase: Saturation
% 9.80/2.29 % (3040974)Time elapsed: 0.066 s
% 9.80/2.29 % (3040974)Peak memory usage: 94 MB
% 9.80/2.29 % (3040974)Instructions burned: 110 (million)
% 9.80/2.29 % (3040979)lrs+10_1_sil=8000:sp=occurrence:random_seed=2231416006:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 9.80/2.29 % (3040979)Instruction limit reached!
% 9.80/2.29 % (3040979)------------------------------
% 9.80/2.29 % (3040979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.80/2.29 % (3040979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.80/2.29 % (3040979)CaDiCaL version: 2.1.3
% 9.80/2.29 % (3040979)Termination reason: Instruction limit
% 9.80/2.29 % (3040979)Termination phase: Saturation
% 9.80/2.29 % (3040979)Time elapsed: 0.066 s
% 9.80/2.29 % (3040979)Peak memory usage: 92 MB
% 9.80/2.29 % (3040979)Instructions burned: 286 (million)
% 11.82/2.82 % (3040986)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3972018468:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 11.82/2.82 % (3040987)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3618159753:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 11.82/2.82 % (3040989)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=305132075:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 11.82/2.82 % (3040990)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1892584215:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2997 on theBenchmark for (2997ds/294Mi)
% 11.82/2.82 % (3040986)Instruction limit reached!
% 11.82/2.82 % (3040986)------------------------------
% 11.82/2.82 % (3040986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.82/2.82 % (3040986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.82/2.82 % (3040986)CaDiCaL version: 2.1.3
% 11.82/2.82 % (3040986)Termination reason: Instruction limit
% 11.82/2.82 % (3040986)Termination phase: Saturation
% 11.82/2.82 % (3040986)Time elapsed: 0.067 s
% 11.82/2.82 % (3040986)Peak memory usage: 88 MB
% 11.82/2.82 % (3040986)Instructions burned: 159 (million)
% 11.82/2.82 % (3040987)Instruction limit reached!
% 11.82/2.82 % (3040987)------------------------------
% 11.82/2.82 % (3040987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.82/2.82 % (3040987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.82/2.82 % (3040987)CaDiCaL version: 2.1.3
% 11.82/2.82 % (3040987)Termination reason: Instruction limit
% 11.82/2.82 % (3040987)Termination phase: Saturation
% 11.82/2.82 % (3040987)Time elapsed: 0.104 s
% 11.82/2.82 % (3040987)Peak memory usage: 89 MB
% 11.82/2.82 % (3040987)Instructions burned: 326 (million)
% 11.82/2.82 % (3040990)Instruction limit reached!
% 11.82/2.82 % (3040990)------------------------------
% 11.82/2.82 % (3040990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.82/2.82 % (3040990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.82/2.82 % (3040990)CaDiCaL version: 2.1.3
% 11.82/2.82 % (3040990)Termination reason: Instruction limit
% 11.82/2.82 % (3040990)Termination phase: Saturation
% 11.82/2.82 % (3040990)Time elapsed: 0.074 s
% 11.82/2.82 % (3040990)Peak memory usage: 92 MB
% 11.82/2.82 % (3040990)Instructions burned: 294 (million)
% 11.82/2.82 % (3040989)Instruction limit reached!
% 11.82/2.82 % (3040989)------------------------------
% 11.82/2.82 % (3040989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.82/2.82 % (3040989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.82/2.82 % (3040989)CaDiCaL version: 2.1.3
% 11.82/2.82 % (3040989)Termination reason: Instruction limit
% 11.82/2.82 % (3040989)Termination phase: Saturation
% 11.82/2.82 % (3040989)Time elapsed: 0.104 s
% 11.82/2.82 % (3040989)Peak memory usage: 88 MB
% 11.82/2.82 % (3040989)Instructions burned: 249 (million)
% 11.82/2.82 % (3040995)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=964763367:i=2350_2996 on theBenchmark for (2996ds/2350Mi)
% 11.82/2.82 % (3040997)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=811541608:i=127:av=off:fsr=off:sup=off_2995 on theBenchmark for (2995ds/127Mi)
% 11.82/2.82 % (3040997)Instruction limit reached!
% 11.82/2.82 % (3040997)------------------------------
% 11.82/2.82 % (3040997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.82/2.82 % (3040997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.82/2.82 % (3040997)CaDiCaL version: 2.1.3
% 11.82/2.82 % (3040997)Termination reason: Instruction limit
% 11.82/2.82 % (3040997)Termination phase: Saturation
% 11.82/2.82 % (3040997)Time elapsed: 0.032 s
% 11.82/2.82 % (3040997)Peak memory usage: 89 MB
% 11.82/2.82 % (3040997)Instructions burned: 129 (million)
% 11.82/2.82 % (3040996)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2046338317:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi)
% 11.82/2.82 % (3040998)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1815748816:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2995 on theBenchmark for (2995ds/114Mi)
% 11.82/2.82 % (3040998)Instruction limit reached!
% 11.82/2.82 % (3040998)------------------------------
% 11.82/2.82 % (3040998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.82/2.82 % (3040998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.82/2.82 % (3040998)CaDiCaL version: 2.1.3
% 11.82/2.82 % (3040998)Termination reason: Instruction limit
% 11.82/2.82 % (3040998)Termination phase: Saturation
% 11.82/2.82 % (3040998)Time elapsed: 0.037 s
% 11.82/2.82 % (3040998)Peak memory usage: 88 MB
% 11.82/2.82 % (3040998)Instructions burned: 117 (million)
% 11.82/2.82 % (3040996)Instruction limit reached!
% 11.82/2.82 % (3040996)------------------------------
% 11.82/2.82 % (3040996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.82/2.82 % (3040996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.82/2.82 % (3040996)CaDiCaL version: 2.1.3
% 11.82/2.82 % (3040996)Termination reason: Instruction limit
% 11.82/2.82 % (3040996)Termination phase: Saturation
% 11.82/2.82 % (3040996)Time elapsed: 0.060 s
% 11.82/2.82 % (3040996)Peak memory usage: 92 MB
% 11.82/2.82 % (3040996)Instructions burned: 113 (million)
% 11.82/2.82 % (3041001)lrs+10_1_sil=8000:sp=occurrence:random_seed=1679128141:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi)
% 11.82/2.82 % (3041005)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=270324644:i=5202:ss=axioms:sgt=16_2993 on theBenchmark for (2993ds/5202Mi)
% 11.82/2.82 % (3041004)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3249341215:i=437:sd=1:aac=none:ss=included_2993 on theBenchmark for (2993ds/437Mi)
% 11.82/2.82 % (3041001)Instruction limit reached!
% 11.82/2.82 % (3041001)------------------------------
% 11.82/2.82 % (3041001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.82/2.82 % (3041001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.82/2.82 % (3041001)CaDiCaL version: 2.1.3
% 11.82/2.82 % (3041001)Termination reason: Instruction limit
% 11.82/2.82 % (3041001)Termination phase: Saturation
% 11.82/2.82 % (3041001)Time elapsed: 0.197 s
% 11.82/2.82 % (3041001)Peak memory usage: 96 MB
% 11.82/2.82 % (3041001)Instructions burned: 911 (million)
% 11.82/2.82 % (3041009)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2856285844:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2991 on theBenchmark for (2991ds/134Mi)
% 11.82/2.82 % (3041004)Instruction limit reached!
% 11.82/2.82 % (3041004)------------------------------
% 11.82/2.82 % (3041004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.82/2.82 % (3041004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.82/2.82 % (3041004)CaDiCaL version: 2.1.3
% 11.82/2.82 % (3041004)Termination reason: Instruction limit
% 11.82/2.82 % (3041004)Termination phase: Saturation
% 11.82/2.82 % (3041004)Time elapsed: 0.173 s
% 11.82/2.82 % (3041004)Peak memory usage: 92 MB
% 11.82/2.82 % (3041004)Instructions burned: 438 (million)
% 11.82/2.82 % (3041009)Instruction limit reached!
% 11.82/2.82 % (3041009)------------------------------
% 11.82/2.82 % (3041009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.82/2.82 % (3041009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.82/2.82 % (3041009)CaDiCaL version: 2.1.3
% 11.82/2.82 % (3041009)Termination reason: Instruction limit
% 11.82/2.82 % (3041009)Termination phase: Saturation
% 11.82/2.82 % (3041009)Time elapsed: 0.031 s
% 11.82/2.82 % (3041009)Peak memory usage: 88 MB
% 11.82/2.82 % (3041009)Instructions burned: 137 (million)
% 11.82/2.82 % (3041011)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=128563664:st=8:i=592:sd=3:ep=RST:ss=axioms_2990 on theBenchmark for (2990ds/592Mi)
% 11.82/2.82 % (3041012)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3893440100:st=3:i=13193:sd=3:ss=axioms_2990 on theBenchmark for (2990ds/13193Mi)
% 11.82/2.82 % (3041011)Instruction limit reached!
% 11.82/2.82 % (3041011)------------------------------
% 11.82/2.82 % (3041011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.82/2.82 % (3041011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.82/2.82 % (3041011)CaDiCaL version: 2.1.3
% 11.82/2.82 % (3041011)Termination reason: Instruction limit
% 11.82/2.82 % (3041011)Termination phase: Saturation
% 11.82/2.82 % (3041011)Time elapsed: 0.217 s
% 11.82/2.82 % (3041011)Peak memory usage: 91 MB
% 11.82/2.82 % (3041011)Instructions burned: 592 (million)
% 11.82/2.82 % (3041015)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=2600538408:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2987 on theBenchmark for (2987ds/125Mi)
% 11.82/2.82 % (3041015)Instruction limit reached!
% 11.82/2.82 % (3041015)------------------------------
% 11.82/2.82 % (3041015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.82/2.82 % (3041015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.82/2.82 % (3041015)CaDiCaL version: 2.1.3
% 11.82/2.82 % (3041015)Termination reason: Instruction limit
% 11.82/2.82 % (3041015)Termination phase: Saturation
% 11.82/2.82 % (3041015)Time elapsed: 0.065 s
% 11.82/2.82 % (3041015)Peak memory usage: 92 MB
% 11.82/2.82 % (3041015)Instructions burned: 127 (million)
% 11.82/2.82 % (3040995)Instruction limit reached!
% 11.82/2.82 % (3040995)------------------------------
% 11.82/2.82 % (3040995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.82/2.82 % (3040995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.82/2.82 % (3040995)CaDiCaL version: 2.1.3
% 11.82/2.82 % (3040995)Termination reason: Instruction limit
% 11.82/2.82 % (3040995)Termination phase: Saturation
% 11.82/2.82 % (3040995)Time elapsed: 0.997 s
% 11.82/2.82 % (3040995)Peak memory usage: 140 MB
% 11.82/2.82 % (3040995)Instructions burned: 2354 (million)
% 11.82/2.82 % (3041017)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3048512122:i=134:gtgl=5:slsql=off:gtg=exists_sym_2985 on theBenchmark for (2985ds/134Mi)
% 11.82/2.82 % (3041018)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=940731143:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/141Mi)
% 11.82/2.82 % (3041018)Instruction limit reached!
% 11.82/2.82 % (3041018)------------------------------
% 11.82/2.82 % (3041018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.82/2.82 % (3041018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.82/2.82 % (3041018)CaDiCaL version: 2.1.3
% 11.82/2.82 % (3041018)Termination reason: Instruction limit
% 11.82/2.82 % (3041018)Termination phase: Saturation
% 11.82/2.82 % (3041018)Time elapsed: 0.042 s
% 11.82/2.82 % (3041018)Peak memory usage: 95 MB
% 11.82/2.82 % (3041018)Instructions burned: 144 (million)
% 11.82/2.82 % (3040972)First to succeed.
% 11.82/2.82 % (3041017)Instruction limit reached!
% 11.82/2.82 % (3041017)------------------------------
% 11.82/2.82 % (3041017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.82/2.82 % (3041017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.82/2.82 % (3041017)CaDiCaL version: 2.1.3
% 11.82/2.82 % (3041017)Termination reason: Instruction limit
% 11.82/2.82 % (3041017)Termination phase: Saturation
% 11.82/2.82 % (3041017)Time elapsed: 0.063 s
% 11.82/2.82 % (3041017)Peak memory usage: 90 MB
% 11.82/2.82 % (3041017)Instructions burned: 135 (million)
% 11.82/2.82 % (3040972)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3040966"
% 11.82/2.82 % (3041021)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1742451608:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2983 on theBenchmark for (2983ds/431Mi)
% 11.82/2.82 % (3041022)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=2344342470:i=6060:aac=none:ins=25_2983 on theBenchmark for (2983ds/6060Mi)
% 11.82/2.82 % (3041021)Instruction limit reached!
% 11.82/2.82 % (3041021)------------------------------
% 11.82/2.82 % (3041021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.82/2.82 % (3041021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.82/2.82 % (3041021)CaDiCaL version: 2.1.3
% 11.82/2.82 % (3041021)Termination reason: Instruction limit
% 11.82/2.82 % (3041021)Termination phase: Saturation
% 11.82/2.82 % (3041021)Time elapsed: 0.105 s
% 11.82/2.82 % (3041021)Peak memory usage: 90 MB
% 11.82/2.82 % (3041021)Instructions burned: 433 (million)
% 11.82/2.82 % (3040972)Refutation found. Thanks to Tanya!
% 11.82/2.82 % SZS status Theorem for theBenchmark
% 11.82/2.82 % SZS output start Proof for theBenchmark
% See solution above
% 14.33/3.02 % (3040972)------------------------------
% 14.33/3.02 % (3040972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.33/3.02 % (3040972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.33/3.02 % (3040972)CaDiCaL version: 2.1.3
% 14.33/3.02 % (3040972)Termination reason: Refutation
% 14.33/3.02 % (3040972)Time elapsed: 1.534 s
% 14.33/3.02 % (3040972)Peak memory usage: 132 MB
% 14.33/3.02 % (3040972)Instructions burned: 2864 (million)
% 14.33/3.02 % (3040972)------------------------------
% 14.33/3.02 % (3040972)------------------------------
% 14.33/3.02 % (3040966)Success in time 1.955 s
% 14.33/3.02 % Vampire exiting
%------------------------------------------------------------------------------