%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL674+1.015 : 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 : n012.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:55:46 AM UTC 2026
% Result : Theorem 4.46s 1.28s
% Output : Refutation 5.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 59
% Syntax : Number of formulae : 285 ( 38 unt; 56 def)
% Number of atoms : 3306 ( 0 equ)
% Maximal formula atoms : 331 ( 11 avg)
% Number of connectives : 5255 (2234 ~;1648 |;1348 &)
% ( 24 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 66 ( 7 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 91 ( 90 usr; 25 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 1 con; 0-1 aty)
% Number of variables : 585 ( 0 sgn 464 !; 121 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : r1(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity) ).
fof(f2,axiom,
! [X0,X1,X2] :
( ( r1(X0,X1)
& r1(X1,X2) )
=> r1(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',transitivity) ).
fof(f3,conjecture,
~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| p7(X1) )
| ~ ( ! [X1] :
( ~ r1(X0,X1)
| ( ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p16(X0)
& ~ p116(X0)
& p115(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p16(X0)
& ~ p116(X0)
& p115(X0) ) ) )
| ~ ( ~ p115(X1)
& p114(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p15(X0)
& ~ p115(X0)
& p114(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p15(X0)
& ~ p115(X0)
& p114(X0) ) ) )
| ~ ( ~ p114(X1)
& p113(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p14(X0)
& ~ p114(X0)
& p113(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p14(X0)
& ~ p114(X0)
& p113(X0) ) ) )
| ~ ( ~ p113(X1)
& p112(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p13(X0)
& ~ p113(X0)
& p112(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p13(X0)
& ~ p113(X0)
& p112(X0) ) ) )
| ~ ( ~ p112(X1)
& p111(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p12(X0)
& ~ p112(X0)
& p111(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p12(X0)
& ~ p112(X0)
& p111(X0) ) ) )
| ~ ( ~ p111(X1)
& p110(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p11(X0)
& ~ p111(X0)
& p110(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p11(X0)
& ~ p111(X0)
& p110(X0) ) ) )
| ~ ( ~ p110(X1)
& p109(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p10(X0)
& ~ p110(X0)
& p109(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p10(X0)
& ~ p110(X0)
& p109(X0) ) ) )
| ~ ( ~ p109(X1)
& p108(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p9(X0)
& ~ p109(X0)
& p108(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p9(X0)
& ~ p109(X0)
& p108(X0) ) ) )
| ~ ( ~ p108(X1)
& p107(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p8(X0)
& ~ p108(X0)
& p107(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p8(X0)
& ~ p108(X0)
& p107(X0) ) ) )
| ~ ( ~ p107(X1)
& p106(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p7(X0)
& ~ p107(X0)
& p106(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p7(X0)
& ~ p107(X0)
& p106(X0) ) ) )
| ~ ( ~ p106(X1)
& p105(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p6(X0)
& ~ p106(X0)
& p105(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p6(X0)
& ~ p106(X0)
& p105(X0) ) ) )
| ~ ( ~ p105(X1)
& p104(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p5(X0)
& ~ p105(X0)
& p104(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p5(X0)
& ~ p105(X0)
& p104(X0) ) ) )
| ~ ( ~ p104(X1)
& p103(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p4(X0)
& ~ p104(X0)
& p103(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p4(X0)
& ~ p104(X0)
& p103(X0) ) ) )
| ~ ( ~ p103(X1)
& p102(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p3(X0)
& ~ p103(X0)
& p102(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p3(X0)
& ~ p103(X0)
& p102(X0) ) ) )
| ~ ( ~ p102(X1)
& p101(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p2(X0)
& ~ p102(X0)
& p101(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
& ~ p102(X0)
& p101(X0) ) ) )
| ~ ( ~ p101(X1)
& p100(X1) ) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p16(X0)
| ~ p115(X0) )
| p16(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p16(X0)
| ~ p115(X0) )
| ~ p16(X1) ) )
| ~ p115(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p15(X0)
| ~ p114(X0) )
| p15(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p15(X0)
| ~ p114(X0) )
| ~ p15(X1) ) )
| ~ p114(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p14(X0)
| ~ p113(X0) )
| p14(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p14(X0)
| ~ p113(X0) )
| ~ p14(X1) ) )
| ~ p113(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p13(X0)
| ~ p112(X0) )
| p13(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p13(X0)
| ~ p112(X0) )
| ~ p13(X1) ) )
| ~ p112(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p12(X0)
| ~ p111(X0) )
| p12(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p12(X0)
| ~ p111(X0) )
| ~ p12(X1) ) )
| ~ p111(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p11(X0)
| ~ p110(X0) )
| p11(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p11(X0)
| ~ p110(X0) )
| ~ p11(X1) ) )
| ~ p110(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p10(X0)
| ~ p109(X0) )
| p10(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p10(X0)
| ~ p109(X0) )
| ~ p10(X1) ) )
| ~ p109(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p9(X0)
| ~ p108(X0) )
| p9(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p9(X0)
| ~ p108(X0) )
| ~ p9(X1) ) )
| ~ p108(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p8(X0)
| ~ p107(X0) )
| p8(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p8(X0)
| ~ p107(X0) )
| ~ p8(X1) ) )
| ~ p107(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p7(X0)
| ~ p106(X0) )
| p7(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p7(X0)
| ~ p106(X0) )
| ~ p7(X1) ) )
| ~ p106(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p6(X0)
| ~ p105(X0) )
| p6(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p6(X0)
| ~ p105(X0) )
| ~ p6(X1) ) )
| ~ p105(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p5(X0)
| ~ p104(X0) )
| p5(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p5(X0)
| ~ p104(X0) )
| ~ p5(X1) ) )
| ~ p104(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p4(X0)
| ~ p103(X0) )
| p4(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| ~ p103(X0) )
| ~ p4(X1) ) )
| ~ p103(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p3(X0)
| ~ p102(X0) )
| p3(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p3(X0)
| ~ p102(X0) )
| ~ p3(X1) ) )
| ~ p102(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p2(X0)
| ~ p101(X0) )
| p2(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ p101(X0) )
| ~ p2(X1) ) )
| ~ p101(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0)
| ~ p100(X0) )
| p1(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ p100(X0) )
| ~ p1(X1) ) )
| ~ p100(X1) )
& ( p115(X1)
| ~ p116(X1) )
& ( p114(X1)
| ~ p115(X1) )
& ( p113(X1)
| ~ p114(X1) )
& ( p112(X1)
| ~ p113(X1) )
& ( p111(X1)
| ~ p112(X1) )
& ( p110(X1)
| ~ p111(X1) )
& ( p109(X1)
| ~ p110(X1) )
& ( p108(X1)
| ~ p109(X1) )
& ( p107(X1)
| ~ p108(X1) )
& ( p106(X1)
| ~ p107(X1) )
& ( p105(X1)
| ~ p106(X1) )
& ( p104(X1)
| ~ p105(X1) )
& ( p103(X1)
| ~ p104(X1) )
& ( p102(X1)
| ~ p103(X1) )
& ( p101(X1)
| ~ p102(X1) )
& ( p100(X1)
| ~ p101(X1) ) ) )
& ~ p101(X0)
& p100(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',main) ).
fof(f4,negated_conjecture,
~ ~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| p7(X1) )
| ~ ( ! [X1] :
( ~ r1(X0,X1)
| ( ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p16(X0)
& ~ p116(X0)
& p115(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p16(X0)
& ~ p116(X0)
& p115(X0) ) ) )
| ~ ( ~ p115(X1)
& p114(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p15(X0)
& ~ p115(X0)
& p114(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p15(X0)
& ~ p115(X0)
& p114(X0) ) ) )
| ~ ( ~ p114(X1)
& p113(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p14(X0)
& ~ p114(X0)
& p113(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p14(X0)
& ~ p114(X0)
& p113(X0) ) ) )
| ~ ( ~ p113(X1)
& p112(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p13(X0)
& ~ p113(X0)
& p112(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p13(X0)
& ~ p113(X0)
& p112(X0) ) ) )
| ~ ( ~ p112(X1)
& p111(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p12(X0)
& ~ p112(X0)
& p111(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p12(X0)
& ~ p112(X0)
& p111(X0) ) ) )
| ~ ( ~ p111(X1)
& p110(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p11(X0)
& ~ p111(X0)
& p110(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p11(X0)
& ~ p111(X0)
& p110(X0) ) ) )
| ~ ( ~ p110(X1)
& p109(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p10(X0)
& ~ p110(X0)
& p109(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p10(X0)
& ~ p110(X0)
& p109(X0) ) ) )
| ~ ( ~ p109(X1)
& p108(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p9(X0)
& ~ p109(X0)
& p108(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p9(X0)
& ~ p109(X0)
& p108(X0) ) ) )
| ~ ( ~ p108(X1)
& p107(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p8(X0)
& ~ p108(X0)
& p107(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p8(X0)
& ~ p108(X0)
& p107(X0) ) ) )
| ~ ( ~ p107(X1)
& p106(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p7(X0)
& ~ p107(X0)
& p106(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p7(X0)
& ~ p107(X0)
& p106(X0) ) ) )
| ~ ( ~ p106(X1)
& p105(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p6(X0)
& ~ p106(X0)
& p105(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p6(X0)
& ~ p106(X0)
& p105(X0) ) ) )
| ~ ( ~ p105(X1)
& p104(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p5(X0)
& ~ p105(X0)
& p104(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p5(X0)
& ~ p105(X0)
& p104(X0) ) ) )
| ~ ( ~ p104(X1)
& p103(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p4(X0)
& ~ p104(X0)
& p103(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p4(X0)
& ~ p104(X0)
& p103(X0) ) ) )
| ~ ( ~ p103(X1)
& p102(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p3(X0)
& ~ p103(X0)
& p102(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p3(X0)
& ~ p103(X0)
& p102(X0) ) ) )
| ~ ( ~ p102(X1)
& p101(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p2(X0)
& ~ p102(X0)
& p101(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
& ~ p102(X0)
& p101(X0) ) ) )
| ~ ( ~ p101(X1)
& p100(X1) ) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p16(X0)
| ~ p115(X0) )
| p16(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p16(X0)
| ~ p115(X0) )
| ~ p16(X1) ) )
| ~ p115(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p15(X0)
| ~ p114(X0) )
| p15(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p15(X0)
| ~ p114(X0) )
| ~ p15(X1) ) )
| ~ p114(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p14(X0)
| ~ p113(X0) )
| p14(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p14(X0)
| ~ p113(X0) )
| ~ p14(X1) ) )
| ~ p113(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p13(X0)
| ~ p112(X0) )
| p13(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p13(X0)
| ~ p112(X0) )
| ~ p13(X1) ) )
| ~ p112(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p12(X0)
| ~ p111(X0) )
| p12(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p12(X0)
| ~ p111(X0) )
| ~ p12(X1) ) )
| ~ p111(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p11(X0)
| ~ p110(X0) )
| p11(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p11(X0)
| ~ p110(X0) )
| ~ p11(X1) ) )
| ~ p110(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p10(X0)
| ~ p109(X0) )
| p10(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p10(X0)
| ~ p109(X0) )
| ~ p10(X1) ) )
| ~ p109(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p9(X0)
| ~ p108(X0) )
| p9(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p9(X0)
| ~ p108(X0) )
| ~ p9(X1) ) )
| ~ p108(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p8(X0)
| ~ p107(X0) )
| p8(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p8(X0)
| ~ p107(X0) )
| ~ p8(X1) ) )
| ~ p107(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p7(X0)
| ~ p106(X0) )
| p7(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p7(X0)
| ~ p106(X0) )
| ~ p7(X1) ) )
| ~ p106(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p6(X0)
| ~ p105(X0) )
| p6(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p6(X0)
| ~ p105(X0) )
| ~ p6(X1) ) )
| ~ p105(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p5(X0)
| ~ p104(X0) )
| p5(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p5(X0)
| ~ p104(X0) )
| ~ p5(X1) ) )
| ~ p104(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p4(X0)
| ~ p103(X0) )
| p4(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| ~ p103(X0) )
| ~ p4(X1) ) )
| ~ p103(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p3(X0)
| ~ p102(X0) )
| p3(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p3(X0)
| ~ p102(X0) )
| ~ p3(X1) ) )
| ~ p102(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p2(X0)
| ~ p101(X0) )
| p2(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ p101(X0) )
| ~ p2(X1) ) )
| ~ p101(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0)
| ~ p100(X0) )
| p1(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ p100(X0) )
| ~ p1(X1) ) )
| ~ p100(X1) )
& ( p115(X1)
| ~ p116(X1) )
& ( p114(X1)
| ~ p115(X1) )
& ( p113(X1)
| ~ p114(X1) )
& ( p112(X1)
| ~ p113(X1) )
& ( p111(X1)
| ~ p112(X1) )
& ( p110(X1)
| ~ p111(X1) )
& ( p109(X1)
| ~ p110(X1) )
& ( p108(X1)
| ~ p109(X1) )
& ( p107(X1)
| ~ p108(X1) )
& ( p106(X1)
| ~ p107(X1) )
& ( p105(X1)
| ~ p106(X1) )
& ( p104(X1)
| ~ p105(X1) )
& ( p103(X1)
| ~ p104(X1) )
& ( p102(X1)
| ~ p103(X1) )
& ( p101(X1)
| ~ p102(X1) )
& ( p100(X1)
| ~ p101(X1) ) ) )
& ~ p101(X0)
& p100(X0) ) ),
inference(negated_conjecture,[status(cth)],[f3]) ).
fof(f5,plain,
~ ~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| p7(X1) )
| ~ ( ! [X2] :
( ~ r1(X0,X2)
| ( ( ( ~ ! [X3] :
( ~ r1(X2,X3)
| ~ ( ~ p16(X3)
& ~ p116(X3)
& p115(X3) ) )
& ~ ! [X4] :
( ~ r1(X2,X4)
| ~ ( p16(X4)
& ~ p116(X4)
& p115(X4) ) ) )
| ~ ( ~ p115(X2)
& p114(X2) ) )
& ( ( ~ ! [X5] :
( ~ r1(X2,X5)
| ~ ( ~ p15(X5)
& ~ p115(X5)
& p114(X5) ) )
& ~ ! [X6] :
( ~ r1(X2,X6)
| ~ ( p15(X6)
& ~ p115(X6)
& p114(X6) ) ) )
| ~ ( ~ p114(X2)
& p113(X2) ) )
& ( ( ~ ! [X7] :
( ~ r1(X2,X7)
| ~ ( ~ p14(X7)
& ~ p114(X7)
& p113(X7) ) )
& ~ ! [X8] :
( ~ r1(X2,X8)
| ~ ( p14(X8)
& ~ p114(X8)
& p113(X8) ) ) )
| ~ ( ~ p113(X2)
& p112(X2) ) )
& ( ( ~ ! [X9] :
( ~ r1(X2,X9)
| ~ ( ~ p13(X9)
& ~ p113(X9)
& p112(X9) ) )
& ~ ! [X10] :
( ~ r1(X2,X10)
| ~ ( p13(X10)
& ~ p113(X10)
& p112(X10) ) ) )
| ~ ( ~ p112(X2)
& p111(X2) ) )
& ( ( ~ ! [X11] :
( ~ r1(X2,X11)
| ~ ( ~ p12(X11)
& ~ p112(X11)
& p111(X11) ) )
& ~ ! [X12] :
( ~ r1(X2,X12)
| ~ ( p12(X12)
& ~ p112(X12)
& p111(X12) ) ) )
| ~ ( ~ p111(X2)
& p110(X2) ) )
& ( ( ~ ! [X13] :
( ~ r1(X2,X13)
| ~ ( ~ p11(X13)
& ~ p111(X13)
& p110(X13) ) )
& ~ ! [X14] :
( ~ r1(X2,X14)
| ~ ( p11(X14)
& ~ p111(X14)
& p110(X14) ) ) )
| ~ ( ~ p110(X2)
& p109(X2) ) )
& ( ( ~ ! [X15] :
( ~ r1(X2,X15)
| ~ ( ~ p10(X15)
& ~ p110(X15)
& p109(X15) ) )
& ~ ! [X16] :
( ~ r1(X2,X16)
| ~ ( p10(X16)
& ~ p110(X16)
& p109(X16) ) ) )
| ~ ( ~ p109(X2)
& p108(X2) ) )
& ( ( ~ ! [X17] :
( ~ r1(X2,X17)
| ~ ( ~ p9(X17)
& ~ p109(X17)
& p108(X17) ) )
& ~ ! [X18] :
( ~ r1(X2,X18)
| ~ ( p9(X18)
& ~ p109(X18)
& p108(X18) ) ) )
| ~ ( ~ p108(X2)
& p107(X2) ) )
& ( ( ~ ! [X19] :
( ~ r1(X2,X19)
| ~ ( ~ p8(X19)
& ~ p108(X19)
& p107(X19) ) )
& ~ ! [X20] :
( ~ r1(X2,X20)
| ~ ( p8(X20)
& ~ p108(X20)
& p107(X20) ) ) )
| ~ ( ~ p107(X2)
& p106(X2) ) )
& ( ( ~ ! [X21] :
( ~ r1(X2,X21)
| ~ ( ~ p7(X21)
& ~ p107(X21)
& p106(X21) ) )
& ~ ! [X22] :
( ~ r1(X2,X22)
| ~ ( p7(X22)
& ~ p107(X22)
& p106(X22) ) ) )
| ~ ( ~ p106(X2)
& p105(X2) ) )
& ( ( ~ ! [X23] :
( ~ r1(X2,X23)
| ~ ( ~ p6(X23)
& ~ p106(X23)
& p105(X23) ) )
& ~ ! [X24] :
( ~ r1(X2,X24)
| ~ ( p6(X24)
& ~ p106(X24)
& p105(X24) ) ) )
| ~ ( ~ p105(X2)
& p104(X2) ) )
& ( ( ~ ! [X25] :
( ~ r1(X2,X25)
| ~ ( ~ p5(X25)
& ~ p105(X25)
& p104(X25) ) )
& ~ ! [X26] :
( ~ r1(X2,X26)
| ~ ( p5(X26)
& ~ p105(X26)
& p104(X26) ) ) )
| ~ ( ~ p104(X2)
& p103(X2) ) )
& ( ( ~ ! [X27] :
( ~ r1(X2,X27)
| ~ ( ~ p4(X27)
& ~ p104(X27)
& p103(X27) ) )
& ~ ! [X28] :
( ~ r1(X2,X28)
| ~ ( p4(X28)
& ~ p104(X28)
& p103(X28) ) ) )
| ~ ( ~ p103(X2)
& p102(X2) ) )
& ( ( ~ ! [X29] :
( ~ r1(X2,X29)
| ~ ( ~ p3(X29)
& ~ p103(X29)
& p102(X29) ) )
& ~ ! [X30] :
( ~ r1(X2,X30)
| ~ ( p3(X30)
& ~ p103(X30)
& p102(X30) ) ) )
| ~ ( ~ p102(X2)
& p101(X2) ) )
& ( ( ~ ! [X31] :
( ~ r1(X2,X31)
| ~ ( ~ p2(X31)
& ~ p102(X31)
& p101(X31) ) )
& ~ ! [X32] :
( ~ r1(X2,X32)
| ~ ( p2(X32)
& ~ p102(X32)
& p101(X32) ) ) )
| ~ ( ~ p101(X2)
& p100(X2) ) )
& ( ( ( ! [X33] :
( ~ r1(X2,X33)
| ~ p16(X33)
| ~ p115(X33) )
| p16(X2) )
& ( ! [X34] :
( ~ r1(X2,X34)
| p16(X34)
| ~ p115(X34) )
| ~ p16(X2) ) )
| ~ p115(X2) )
& ( ( ( ! [X35] :
( ~ r1(X2,X35)
| ~ p15(X35)
| ~ p114(X35) )
| p15(X2) )
& ( ! [X36] :
( ~ r1(X2,X36)
| p15(X36)
| ~ p114(X36) )
| ~ p15(X2) ) )
| ~ p114(X2) )
& ( ( ( ! [X37] :
( ~ r1(X2,X37)
| ~ p14(X37)
| ~ p113(X37) )
| p14(X2) )
& ( ! [X38] :
( ~ r1(X2,X38)
| p14(X38)
| ~ p113(X38) )
| ~ p14(X2) ) )
| ~ p113(X2) )
& ( ( ( ! [X39] :
( ~ r1(X2,X39)
| ~ p13(X39)
| ~ p112(X39) )
| p13(X2) )
& ( ! [X40] :
( ~ r1(X2,X40)
| p13(X40)
| ~ p112(X40) )
| ~ p13(X2) ) )
| ~ p112(X2) )
& ( ( ( ! [X41] :
( ~ r1(X2,X41)
| ~ p12(X41)
| ~ p111(X41) )
| p12(X2) )
& ( ! [X42] :
( ~ r1(X2,X42)
| p12(X42)
| ~ p111(X42) )
| ~ p12(X2) ) )
| ~ p111(X2) )
& ( ( ( ! [X43] :
( ~ r1(X2,X43)
| ~ p11(X43)
| ~ p110(X43) )
| p11(X2) )
& ( ! [X44] :
( ~ r1(X2,X44)
| p11(X44)
| ~ p110(X44) )
| ~ p11(X2) ) )
| ~ p110(X2) )
& ( ( ( ! [X45] :
( ~ r1(X2,X45)
| ~ p10(X45)
| ~ p109(X45) )
| p10(X2) )
& ( ! [X46] :
( ~ r1(X2,X46)
| p10(X46)
| ~ p109(X46) )
| ~ p10(X2) ) )
| ~ p109(X2) )
& ( ( ( ! [X47] :
( ~ r1(X2,X47)
| ~ p9(X47)
| ~ p108(X47) )
| p9(X2) )
& ( ! [X48] :
( ~ r1(X2,X48)
| p9(X48)
| ~ p108(X48) )
| ~ p9(X2) ) )
| ~ p108(X2) )
& ( ( ( ! [X49] :
( ~ r1(X2,X49)
| ~ p8(X49)
| ~ p107(X49) )
| p8(X2) )
& ( ! [X50] :
( ~ r1(X2,X50)
| p8(X50)
| ~ p107(X50) )
| ~ p8(X2) ) )
| ~ p107(X2) )
& ( ( ( ! [X51] :
( ~ r1(X2,X51)
| ~ p7(X51)
| ~ p106(X51) )
| p7(X2) )
& ( ! [X52] :
( ~ r1(X2,X52)
| p7(X52)
| ~ p106(X52) )
| ~ p7(X2) ) )
| ~ p106(X2) )
& ( ( ( ! [X53] :
( ~ r1(X2,X53)
| ~ p6(X53)
| ~ p105(X53) )
| p6(X2) )
& ( ! [X54] :
( ~ r1(X2,X54)
| p6(X54)
| ~ p105(X54) )
| ~ p6(X2) ) )
| ~ p105(X2) )
& ( ( ( ! [X55] :
( ~ r1(X2,X55)
| ~ p5(X55)
| ~ p104(X55) )
| p5(X2) )
& ( ! [X56] :
( ~ r1(X2,X56)
| p5(X56)
| ~ p104(X56) )
| ~ p5(X2) ) )
| ~ p104(X2) )
& ( ( ( ! [X57] :
( ~ r1(X2,X57)
| ~ p4(X57)
| ~ p103(X57) )
| p4(X2) )
& ( ! [X58] :
( ~ r1(X2,X58)
| p4(X58)
| ~ p103(X58) )
| ~ p4(X2) ) )
| ~ p103(X2) )
& ( ( ( ! [X59] :
( ~ r1(X2,X59)
| ~ p3(X59)
| ~ p102(X59) )
| p3(X2) )
& ( ! [X60] :
( ~ r1(X2,X60)
| p3(X60)
| ~ p102(X60) )
| ~ p3(X2) ) )
| ~ p102(X2) )
& ( ( ( ! [X61] :
( ~ r1(X2,X61)
| ~ p2(X61)
| ~ p101(X61) )
| p2(X2) )
& ( ! [X62] :
( ~ r1(X2,X62)
| p2(X62)
| ~ p101(X62) )
| ~ p2(X2) ) )
| ~ p101(X2) )
& ( ( ( ! [X63] :
( ~ r1(X2,X63)
| ~ p1(X63)
| ~ p100(X63) )
| p1(X2) )
& ( ! [X64] :
( ~ r1(X2,X64)
| p1(X64)
| ~ p100(X64) )
| ~ p1(X2) ) )
| ~ p100(X2) )
& ( p115(X2)
| ~ p116(X2) )
& ( p114(X2)
| ~ p115(X2) )
& ( p113(X2)
| ~ p114(X2) )
& ( p112(X2)
| ~ p113(X2) )
& ( p111(X2)
| ~ p112(X2) )
& ( p110(X2)
| ~ p111(X2) )
& ( p109(X2)
| ~ p110(X2) )
& ( p108(X2)
| ~ p109(X2) )
& ( p107(X2)
| ~ p108(X2) )
& ( p106(X2)
| ~ p107(X2) )
& ( p105(X2)
| ~ p106(X2) )
& ( p104(X2)
| ~ p105(X2) )
& ( p103(X2)
| ~ p104(X2) )
& ( p102(X2)
| ~ p103(X2) )
& ( p101(X2)
| ~ p102(X2) )
& ( p100(X2)
| ~ p101(X2) ) ) )
& ~ p101(X0)
& p100(X0) ) ),
inference(rectify,[],[f4]) ).
fof(f6,plain,
? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| p7(X1) )
| ~ ( ! [X2] :
( ~ r1(X0,X2)
| ( ( ( ~ ! [X3] :
( ~ r1(X2,X3)
| ~ ( ~ p16(X3)
& ~ p116(X3)
& p115(X3) ) )
& ~ ! [X4] :
( ~ r1(X2,X4)
| ~ ( p16(X4)
& ~ p116(X4)
& p115(X4) ) ) )
| ~ ( ~ p115(X2)
& p114(X2) ) )
& ( ( ~ ! [X5] :
( ~ r1(X2,X5)
| ~ ( ~ p15(X5)
& ~ p115(X5)
& p114(X5) ) )
& ~ ! [X6] :
( ~ r1(X2,X6)
| ~ ( p15(X6)
& ~ p115(X6)
& p114(X6) ) ) )
| ~ ( ~ p114(X2)
& p113(X2) ) )
& ( ( ~ ! [X7] :
( ~ r1(X2,X7)
| ~ ( ~ p14(X7)
& ~ p114(X7)
& p113(X7) ) )
& ~ ! [X8] :
( ~ r1(X2,X8)
| ~ ( p14(X8)
& ~ p114(X8)
& p113(X8) ) ) )
| ~ ( ~ p113(X2)
& p112(X2) ) )
& ( ( ~ ! [X9] :
( ~ r1(X2,X9)
| ~ ( ~ p13(X9)
& ~ p113(X9)
& p112(X9) ) )
& ~ ! [X10] :
( ~ r1(X2,X10)
| ~ ( p13(X10)
& ~ p113(X10)
& p112(X10) ) ) )
| ~ ( ~ p112(X2)
& p111(X2) ) )
& ( ( ~ ! [X11] :
( ~ r1(X2,X11)
| ~ ( ~ p12(X11)
& ~ p112(X11)
& p111(X11) ) )
& ~ ! [X12] :
( ~ r1(X2,X12)
| ~ ( p12(X12)
& ~ p112(X12)
& p111(X12) ) ) )
| ~ ( ~ p111(X2)
& p110(X2) ) )
& ( ( ~ ! [X13] :
( ~ r1(X2,X13)
| ~ ( ~ p11(X13)
& ~ p111(X13)
& p110(X13) ) )
& ~ ! [X14] :
( ~ r1(X2,X14)
| ~ ( p11(X14)
& ~ p111(X14)
& p110(X14) ) ) )
| ~ ( ~ p110(X2)
& p109(X2) ) )
& ( ( ~ ! [X15] :
( ~ r1(X2,X15)
| ~ ( ~ p10(X15)
& ~ p110(X15)
& p109(X15) ) )
& ~ ! [X16] :
( ~ r1(X2,X16)
| ~ ( p10(X16)
& ~ p110(X16)
& p109(X16) ) ) )
| ~ ( ~ p109(X2)
& p108(X2) ) )
& ( ( ~ ! [X17] :
( ~ r1(X2,X17)
| ~ ( ~ p9(X17)
& ~ p109(X17)
& p108(X17) ) )
& ~ ! [X18] :
( ~ r1(X2,X18)
| ~ ( p9(X18)
& ~ p109(X18)
& p108(X18) ) ) )
| ~ ( ~ p108(X2)
& p107(X2) ) )
& ( ( ~ ! [X19] :
( ~ r1(X2,X19)
| ~ ( ~ p8(X19)
& ~ p108(X19)
& p107(X19) ) )
& ~ ! [X20] :
( ~ r1(X2,X20)
| ~ ( p8(X20)
& ~ p108(X20)
& p107(X20) ) ) )
| ~ ( ~ p107(X2)
& p106(X2) ) )
& ( ( ~ ! [X21] :
( ~ r1(X2,X21)
| ~ ( ~ p7(X21)
& ~ p107(X21)
& p106(X21) ) )
& ~ ! [X22] :
( ~ r1(X2,X22)
| ~ ( p7(X22)
& ~ p107(X22)
& p106(X22) ) ) )
| ~ ( ~ p106(X2)
& p105(X2) ) )
& ( ( ~ ! [X23] :
( ~ r1(X2,X23)
| ~ ( ~ p6(X23)
& ~ p106(X23)
& p105(X23) ) )
& ~ ! [X24] :
( ~ r1(X2,X24)
| ~ ( p6(X24)
& ~ p106(X24)
& p105(X24) ) ) )
| ~ ( ~ p105(X2)
& p104(X2) ) )
& ( ( ~ ! [X25] :
( ~ r1(X2,X25)
| ~ ( ~ p5(X25)
& ~ p105(X25)
& p104(X25) ) )
& ~ ! [X26] :
( ~ r1(X2,X26)
| ~ ( p5(X26)
& ~ p105(X26)
& p104(X26) ) ) )
| ~ ( ~ p104(X2)
& p103(X2) ) )
& ( ( ~ ! [X27] :
( ~ r1(X2,X27)
| ~ ( ~ p4(X27)
& ~ p104(X27)
& p103(X27) ) )
& ~ ! [X28] :
( ~ r1(X2,X28)
| ~ ( p4(X28)
& ~ p104(X28)
& p103(X28) ) ) )
| ~ ( ~ p103(X2)
& p102(X2) ) )
& ( ( ~ ! [X29] :
( ~ r1(X2,X29)
| ~ ( ~ p3(X29)
& ~ p103(X29)
& p102(X29) ) )
& ~ ! [X30] :
( ~ r1(X2,X30)
| ~ ( p3(X30)
& ~ p103(X30)
& p102(X30) ) ) )
| ~ ( ~ p102(X2)
& p101(X2) ) )
& ( ( ~ ! [X31] :
( ~ r1(X2,X31)
| ~ ( ~ p2(X31)
& ~ p102(X31)
& p101(X31) ) )
& ~ ! [X32] :
( ~ r1(X2,X32)
| ~ ( p2(X32)
& ~ p102(X32)
& p101(X32) ) ) )
| ~ ( ~ p101(X2)
& p100(X2) ) )
& ( ( ( ! [X33] :
( ~ r1(X2,X33)
| ~ p16(X33)
| ~ p115(X33) )
| p16(X2) )
& ( ! [X34] :
( ~ r1(X2,X34)
| p16(X34)
| ~ p115(X34) )
| ~ p16(X2) ) )
| ~ p115(X2) )
& ( ( ( ! [X35] :
( ~ r1(X2,X35)
| ~ p15(X35)
| ~ p114(X35) )
| p15(X2) )
& ( ! [X36] :
( ~ r1(X2,X36)
| p15(X36)
| ~ p114(X36) )
| ~ p15(X2) ) )
| ~ p114(X2) )
& ( ( ( ! [X37] :
( ~ r1(X2,X37)
| ~ p14(X37)
| ~ p113(X37) )
| p14(X2) )
& ( ! [X38] :
( ~ r1(X2,X38)
| p14(X38)
| ~ p113(X38) )
| ~ p14(X2) ) )
| ~ p113(X2) )
& ( ( ( ! [X39] :
( ~ r1(X2,X39)
| ~ p13(X39)
| ~ p112(X39) )
| p13(X2) )
& ( ! [X40] :
( ~ r1(X2,X40)
| p13(X40)
| ~ p112(X40) )
| ~ p13(X2) ) )
| ~ p112(X2) )
& ( ( ( ! [X41] :
( ~ r1(X2,X41)
| ~ p12(X41)
| ~ p111(X41) )
| p12(X2) )
& ( ! [X42] :
( ~ r1(X2,X42)
| p12(X42)
| ~ p111(X42) )
| ~ p12(X2) ) )
| ~ p111(X2) )
& ( ( ( ! [X43] :
( ~ r1(X2,X43)
| ~ p11(X43)
| ~ p110(X43) )
| p11(X2) )
& ( ! [X44] :
( ~ r1(X2,X44)
| p11(X44)
| ~ p110(X44) )
| ~ p11(X2) ) )
| ~ p110(X2) )
& ( ( ( ! [X45] :
( ~ r1(X2,X45)
| ~ p10(X45)
| ~ p109(X45) )
| p10(X2) )
& ( ! [X46] :
( ~ r1(X2,X46)
| p10(X46)
| ~ p109(X46) )
| ~ p10(X2) ) )
| ~ p109(X2) )
& ( ( ( ! [X47] :
( ~ r1(X2,X47)
| ~ p9(X47)
| ~ p108(X47) )
| p9(X2) )
& ( ! [X48] :
( ~ r1(X2,X48)
| p9(X48)
| ~ p108(X48) )
| ~ p9(X2) ) )
| ~ p108(X2) )
& ( ( ( ! [X49] :
( ~ r1(X2,X49)
| ~ p8(X49)
| ~ p107(X49) )
| p8(X2) )
& ( ! [X50] :
( ~ r1(X2,X50)
| p8(X50)
| ~ p107(X50) )
| ~ p8(X2) ) )
| ~ p107(X2) )
& ( ( ( ! [X51] :
( ~ r1(X2,X51)
| ~ p7(X51)
| ~ p106(X51) )
| p7(X2) )
& ( ! [X52] :
( ~ r1(X2,X52)
| p7(X52)
| ~ p106(X52) )
| ~ p7(X2) ) )
| ~ p106(X2) )
& ( ( ( ! [X53] :
( ~ r1(X2,X53)
| ~ p6(X53)
| ~ p105(X53) )
| p6(X2) )
& ( ! [X54] :
( ~ r1(X2,X54)
| p6(X54)
| ~ p105(X54) )
| ~ p6(X2) ) )
| ~ p105(X2) )
& ( ( ( ! [X55] :
( ~ r1(X2,X55)
| ~ p5(X55)
| ~ p104(X55) )
| p5(X2) )
& ( ! [X56] :
( ~ r1(X2,X56)
| p5(X56)
| ~ p104(X56) )
| ~ p5(X2) ) )
| ~ p104(X2) )
& ( ( ( ! [X57] :
( ~ r1(X2,X57)
| ~ p4(X57)
| ~ p103(X57) )
| p4(X2) )
& ( ! [X58] :
( ~ r1(X2,X58)
| p4(X58)
| ~ p103(X58) )
| ~ p4(X2) ) )
| ~ p103(X2) )
& ( ( ( ! [X59] :
( ~ r1(X2,X59)
| ~ p3(X59)
| ~ p102(X59) )
| p3(X2) )
& ( ! [X60] :
( ~ r1(X2,X60)
| p3(X60)
| ~ p102(X60) )
| ~ p3(X2) ) )
| ~ p102(X2) )
& ( ( ( ! [X61] :
( ~ r1(X2,X61)
| ~ p2(X61)
| ~ p101(X61) )
| p2(X2) )
& ( ! [X62] :
( ~ r1(X2,X62)
| p2(X62)
| ~ p101(X62) )
| ~ p2(X2) ) )
| ~ p101(X2) )
& ( ( ( ! [X63] :
( ~ r1(X2,X63)
| ~ p1(X63)
| ~ p100(X63) )
| p1(X2) )
& ( ! [X64] :
( ~ r1(X2,X64)
| p1(X64)
| ~ p100(X64) )
| ~ p1(X2) ) )
| ~ p100(X2) )
& ( p115(X2)
| ~ p116(X2) )
& ( p114(X2)
| ~ p115(X2) )
& ( p113(X2)
| ~ p114(X2) )
& ( p112(X2)
| ~ p113(X2) )
& ( p111(X2)
| ~ p112(X2) )
& ( p110(X2)
| ~ p111(X2) )
& ( p109(X2)
| ~ p110(X2) )
& ( p108(X2)
| ~ p109(X2) )
& ( p107(X2)
| ~ p108(X2) )
& ( p106(X2)
| ~ p107(X2) )
& ( p105(X2)
| ~ p106(X2) )
& ( p104(X2)
| ~ p105(X2) )
& ( p103(X2)
| ~ p104(X2) )
& ( p102(X2)
| ~ p103(X2) )
& ( p101(X2)
| ~ p102(X2) )
& ( p100(X2)
| ~ p101(X2) ) ) )
& ~ p101(X0)
& p100(X0) ) ),
inference(flattening,[],[f5]) ).
fof(f7,plain,
! [X0,X1,X2] :
( r1(X0,X2)
| ~ r1(X0,X1)
| ~ r1(X1,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f8,plain,
! [X0,X1,X2] :
( r1(X0,X2)
| ~ r1(X0,X1)
| ~ r1(X1,X2) ),
inference(flattening,[],[f7]) ).
fof(f9,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| p7(X1) )
& ! [X2] :
( ~ r1(X0,X2)
| ( ( ( ? [X3] :
( r1(X2,X3)
& ~ p16(X3)
& ~ p116(X3)
& p115(X3) )
& ? [X4] :
( r1(X2,X4)
& p16(X4)
& ~ p116(X4)
& p115(X4) ) )
| p115(X2)
| ~ p114(X2) )
& ( ( ? [X5] :
( r1(X2,X5)
& ~ p15(X5)
& ~ p115(X5)
& p114(X5) )
& ? [X6] :
( r1(X2,X6)
& p15(X6)
& ~ p115(X6)
& p114(X6) ) )
| p114(X2)
| ~ p113(X2) )
& ( ( ? [X7] :
( r1(X2,X7)
& ~ p14(X7)
& ~ p114(X7)
& p113(X7) )
& ? [X8] :
( r1(X2,X8)
& p14(X8)
& ~ p114(X8)
& p113(X8) ) )
| p113(X2)
| ~ p112(X2) )
& ( ( ? [X9] :
( r1(X2,X9)
& ~ p13(X9)
& ~ p113(X9)
& p112(X9) )
& ? [X10] :
( r1(X2,X10)
& p13(X10)
& ~ p113(X10)
& p112(X10) ) )
| p112(X2)
| ~ p111(X2) )
& ( ( ? [X11] :
( r1(X2,X11)
& ~ p12(X11)
& ~ p112(X11)
& p111(X11) )
& ? [X12] :
( r1(X2,X12)
& p12(X12)
& ~ p112(X12)
& p111(X12) ) )
| p111(X2)
| ~ p110(X2) )
& ( ( ? [X13] :
( r1(X2,X13)
& ~ p11(X13)
& ~ p111(X13)
& p110(X13) )
& ? [X14] :
( r1(X2,X14)
& p11(X14)
& ~ p111(X14)
& p110(X14) ) )
| p110(X2)
| ~ p109(X2) )
& ( ( ? [X15] :
( r1(X2,X15)
& ~ p10(X15)
& ~ p110(X15)
& p109(X15) )
& ? [X16] :
( r1(X2,X16)
& p10(X16)
& ~ p110(X16)
& p109(X16) ) )
| p109(X2)
| ~ p108(X2) )
& ( ( ? [X17] :
( r1(X2,X17)
& ~ p9(X17)
& ~ p109(X17)
& p108(X17) )
& ? [X18] :
( r1(X2,X18)
& p9(X18)
& ~ p109(X18)
& p108(X18) ) )
| p108(X2)
| ~ p107(X2) )
& ( ( ? [X19] :
( r1(X2,X19)
& ~ p8(X19)
& ~ p108(X19)
& p107(X19) )
& ? [X20] :
( r1(X2,X20)
& p8(X20)
& ~ p108(X20)
& p107(X20) ) )
| p107(X2)
| ~ p106(X2) )
& ( ( ? [X21] :
( r1(X2,X21)
& ~ p7(X21)
& ~ p107(X21)
& p106(X21) )
& ? [X22] :
( r1(X2,X22)
& p7(X22)
& ~ p107(X22)
& p106(X22) ) )
| p106(X2)
| ~ p105(X2) )
& ( ( ? [X23] :
( r1(X2,X23)
& ~ p6(X23)
& ~ p106(X23)
& p105(X23) )
& ? [X24] :
( r1(X2,X24)
& p6(X24)
& ~ p106(X24)
& p105(X24) ) )
| p105(X2)
| ~ p104(X2) )
& ( ( ? [X25] :
( r1(X2,X25)
& ~ p5(X25)
& ~ p105(X25)
& p104(X25) )
& ? [X26] :
( r1(X2,X26)
& p5(X26)
& ~ p105(X26)
& p104(X26) ) )
| p104(X2)
| ~ p103(X2) )
& ( ( ? [X27] :
( r1(X2,X27)
& ~ p4(X27)
& ~ p104(X27)
& p103(X27) )
& ? [X28] :
( r1(X2,X28)
& p4(X28)
& ~ p104(X28)
& p103(X28) ) )
| p103(X2)
| ~ p102(X2) )
& ( ( ? [X29] :
( r1(X2,X29)
& ~ p3(X29)
& ~ p103(X29)
& p102(X29) )
& ? [X30] :
( r1(X2,X30)
& p3(X30)
& ~ p103(X30)
& p102(X30) ) )
| p102(X2)
| ~ p101(X2) )
& ( ( ? [X31] :
( r1(X2,X31)
& ~ p2(X31)
& ~ p102(X31)
& p101(X31) )
& ? [X32] :
( r1(X2,X32)
& p2(X32)
& ~ p102(X32)
& p101(X32) ) )
| p101(X2)
| ~ p100(X2) )
& ( ( ( ! [X33] :
( ~ r1(X2,X33)
| ~ p16(X33)
| ~ p115(X33) )
| p16(X2) )
& ( ! [X34] :
( ~ r1(X2,X34)
| p16(X34)
| ~ p115(X34) )
| ~ p16(X2) ) )
| ~ p115(X2) )
& ( ( ( ! [X35] :
( ~ r1(X2,X35)
| ~ p15(X35)
| ~ p114(X35) )
| p15(X2) )
& ( ! [X36] :
( ~ r1(X2,X36)
| p15(X36)
| ~ p114(X36) )
| ~ p15(X2) ) )
| ~ p114(X2) )
& ( ( ( ! [X37] :
( ~ r1(X2,X37)
| ~ p14(X37)
| ~ p113(X37) )
| p14(X2) )
& ( ! [X38] :
( ~ r1(X2,X38)
| p14(X38)
| ~ p113(X38) )
| ~ p14(X2) ) )
| ~ p113(X2) )
& ( ( ( ! [X39] :
( ~ r1(X2,X39)
| ~ p13(X39)
| ~ p112(X39) )
| p13(X2) )
& ( ! [X40] :
( ~ r1(X2,X40)
| p13(X40)
| ~ p112(X40) )
| ~ p13(X2) ) )
| ~ p112(X2) )
& ( ( ( ! [X41] :
( ~ r1(X2,X41)
| ~ p12(X41)
| ~ p111(X41) )
| p12(X2) )
& ( ! [X42] :
( ~ r1(X2,X42)
| p12(X42)
| ~ p111(X42) )
| ~ p12(X2) ) )
| ~ p111(X2) )
& ( ( ( ! [X43] :
( ~ r1(X2,X43)
| ~ p11(X43)
| ~ p110(X43) )
| p11(X2) )
& ( ! [X44] :
( ~ r1(X2,X44)
| p11(X44)
| ~ p110(X44) )
| ~ p11(X2) ) )
| ~ p110(X2) )
& ( ( ( ! [X45] :
( ~ r1(X2,X45)
| ~ p10(X45)
| ~ p109(X45) )
| p10(X2) )
& ( ! [X46] :
( ~ r1(X2,X46)
| p10(X46)
| ~ p109(X46) )
| ~ p10(X2) ) )
| ~ p109(X2) )
& ( ( ( ! [X47] :
( ~ r1(X2,X47)
| ~ p9(X47)
| ~ p108(X47) )
| p9(X2) )
& ( ! [X48] :
( ~ r1(X2,X48)
| p9(X48)
| ~ p108(X48) )
| ~ p9(X2) ) )
| ~ p108(X2) )
& ( ( ( ! [X49] :
( ~ r1(X2,X49)
| ~ p8(X49)
| ~ p107(X49) )
| p8(X2) )
& ( ! [X50] :
( ~ r1(X2,X50)
| p8(X50)
| ~ p107(X50) )
| ~ p8(X2) ) )
| ~ p107(X2) )
& ( ( ( ! [X51] :
( ~ r1(X2,X51)
| ~ p7(X51)
| ~ p106(X51) )
| p7(X2) )
& ( ! [X52] :
( ~ r1(X2,X52)
| p7(X52)
| ~ p106(X52) )
| ~ p7(X2) ) )
| ~ p106(X2) )
& ( ( ( ! [X53] :
( ~ r1(X2,X53)
| ~ p6(X53)
| ~ p105(X53) )
| p6(X2) )
& ( ! [X54] :
( ~ r1(X2,X54)
| p6(X54)
| ~ p105(X54) )
| ~ p6(X2) ) )
| ~ p105(X2) )
& ( ( ( ! [X55] :
( ~ r1(X2,X55)
| ~ p5(X55)
| ~ p104(X55) )
| p5(X2) )
& ( ! [X56] :
( ~ r1(X2,X56)
| p5(X56)
| ~ p104(X56) )
| ~ p5(X2) ) )
| ~ p104(X2) )
& ( ( ( ! [X57] :
( ~ r1(X2,X57)
| ~ p4(X57)
| ~ p103(X57) )
| p4(X2) )
& ( ! [X58] :
( ~ r1(X2,X58)
| p4(X58)
| ~ p103(X58) )
| ~ p4(X2) ) )
| ~ p103(X2) )
& ( ( ( ! [X59] :
( ~ r1(X2,X59)
| ~ p3(X59)
| ~ p102(X59) )
| p3(X2) )
& ( ! [X60] :
( ~ r1(X2,X60)
| p3(X60)
| ~ p102(X60) )
| ~ p3(X2) ) )
| ~ p102(X2) )
& ( ( ( ! [X61] :
( ~ r1(X2,X61)
| ~ p2(X61)
| ~ p101(X61) )
| p2(X2) )
& ( ! [X62] :
( ~ r1(X2,X62)
| p2(X62)
| ~ p101(X62) )
| ~ p2(X2) ) )
| ~ p101(X2) )
& ( ( ( ! [X63] :
( ~ r1(X2,X63)
| ~ p1(X63)
| ~ p100(X63) )
| p1(X2) )
& ( ! [X64] :
( ~ r1(X2,X64)
| p1(X64)
| ~ p100(X64) )
| ~ p1(X2) ) )
| ~ p100(X2) )
& ( p115(X2)
| ~ p116(X2) )
& ( p114(X2)
| ~ p115(X2) )
& ( p113(X2)
| ~ p114(X2) )
& ( p112(X2)
| ~ p113(X2) )
& ( p111(X2)
| ~ p112(X2) )
& ( p110(X2)
| ~ p111(X2) )
& ( p109(X2)
| ~ p110(X2) )
& ( p108(X2)
| ~ p109(X2) )
& ( p107(X2)
| ~ p108(X2) )
& ( p106(X2)
| ~ p107(X2) )
& ( p105(X2)
| ~ p106(X2) )
& ( p104(X2)
| ~ p105(X2) )
& ( p103(X2)
| ~ p104(X2) )
& ( p102(X2)
| ~ p103(X2) )
& ( p101(X2)
| ~ p102(X2) )
& ( p100(X2)
| ~ p101(X2) ) ) )
& ~ p101(X0)
& p100(X0) ),
inference(ennf_transformation,[],[f6]) ).
fof(f10,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| p7(X1) )
& ! [X2] :
( ~ r1(X0,X2)
| ( ( ( ? [X3] :
( r1(X2,X3)
& ~ p16(X3)
& ~ p116(X3)
& p115(X3) )
& ? [X4] :
( r1(X2,X4)
& p16(X4)
& ~ p116(X4)
& p115(X4) ) )
| p115(X2)
| ~ p114(X2) )
& ( ( ? [X5] :
( r1(X2,X5)
& ~ p15(X5)
& ~ p115(X5)
& p114(X5) )
& ? [X6] :
( r1(X2,X6)
& p15(X6)
& ~ p115(X6)
& p114(X6) ) )
| p114(X2)
| ~ p113(X2) )
& ( ( ? [X7] :
( r1(X2,X7)
& ~ p14(X7)
& ~ p114(X7)
& p113(X7) )
& ? [X8] :
( r1(X2,X8)
& p14(X8)
& ~ p114(X8)
& p113(X8) ) )
| p113(X2)
| ~ p112(X2) )
& ( ( ? [X9] :
( r1(X2,X9)
& ~ p13(X9)
& ~ p113(X9)
& p112(X9) )
& ? [X10] :
( r1(X2,X10)
& p13(X10)
& ~ p113(X10)
& p112(X10) ) )
| p112(X2)
| ~ p111(X2) )
& ( ( ? [X11] :
( r1(X2,X11)
& ~ p12(X11)
& ~ p112(X11)
& p111(X11) )
& ? [X12] :
( r1(X2,X12)
& p12(X12)
& ~ p112(X12)
& p111(X12) ) )
| p111(X2)
| ~ p110(X2) )
& ( ( ? [X13] :
( r1(X2,X13)
& ~ p11(X13)
& ~ p111(X13)
& p110(X13) )
& ? [X14] :
( r1(X2,X14)
& p11(X14)
& ~ p111(X14)
& p110(X14) ) )
| p110(X2)
| ~ p109(X2) )
& ( ( ? [X15] :
( r1(X2,X15)
& ~ p10(X15)
& ~ p110(X15)
& p109(X15) )
& ? [X16] :
( r1(X2,X16)
& p10(X16)
& ~ p110(X16)
& p109(X16) ) )
| p109(X2)
| ~ p108(X2) )
& ( ( ? [X17] :
( r1(X2,X17)
& ~ p9(X17)
& ~ p109(X17)
& p108(X17) )
& ? [X18] :
( r1(X2,X18)
& p9(X18)
& ~ p109(X18)
& p108(X18) ) )
| p108(X2)
| ~ p107(X2) )
& ( ( ? [X19] :
( r1(X2,X19)
& ~ p8(X19)
& ~ p108(X19)
& p107(X19) )
& ? [X20] :
( r1(X2,X20)
& p8(X20)
& ~ p108(X20)
& p107(X20) ) )
| p107(X2)
| ~ p106(X2) )
& ( ( ? [X21] :
( r1(X2,X21)
& ~ p7(X21)
& ~ p107(X21)
& p106(X21) )
& ? [X22] :
( r1(X2,X22)
& p7(X22)
& ~ p107(X22)
& p106(X22) ) )
| p106(X2)
| ~ p105(X2) )
& ( ( ? [X23] :
( r1(X2,X23)
& ~ p6(X23)
& ~ p106(X23)
& p105(X23) )
& ? [X24] :
( r1(X2,X24)
& p6(X24)
& ~ p106(X24)
& p105(X24) ) )
| p105(X2)
| ~ p104(X2) )
& ( ( ? [X25] :
( r1(X2,X25)
& ~ p5(X25)
& ~ p105(X25)
& p104(X25) )
& ? [X26] :
( r1(X2,X26)
& p5(X26)
& ~ p105(X26)
& p104(X26) ) )
| p104(X2)
| ~ p103(X2) )
& ( ( ? [X27] :
( r1(X2,X27)
& ~ p4(X27)
& ~ p104(X27)
& p103(X27) )
& ? [X28] :
( r1(X2,X28)
& p4(X28)
& ~ p104(X28)
& p103(X28) ) )
| p103(X2)
| ~ p102(X2) )
& ( ( ? [X29] :
( r1(X2,X29)
& ~ p3(X29)
& ~ p103(X29)
& p102(X29) )
& ? [X30] :
( r1(X2,X30)
& p3(X30)
& ~ p103(X30)
& p102(X30) ) )
| p102(X2)
| ~ p101(X2) )
& ( ( ? [X31] :
( r1(X2,X31)
& ~ p2(X31)
& ~ p102(X31)
& p101(X31) )
& ? [X32] :
( r1(X2,X32)
& p2(X32)
& ~ p102(X32)
& p101(X32) ) )
| p101(X2)
| ~ p100(X2) )
& ( ( ( ! [X33] :
( ~ r1(X2,X33)
| ~ p16(X33)
| ~ p115(X33) )
| p16(X2) )
& ( ! [X34] :
( ~ r1(X2,X34)
| p16(X34)
| ~ p115(X34) )
| ~ p16(X2) ) )
| ~ p115(X2) )
& ( ( ( ! [X35] :
( ~ r1(X2,X35)
| ~ p15(X35)
| ~ p114(X35) )
| p15(X2) )
& ( ! [X36] :
( ~ r1(X2,X36)
| p15(X36)
| ~ p114(X36) )
| ~ p15(X2) ) )
| ~ p114(X2) )
& ( ( ( ! [X37] :
( ~ r1(X2,X37)
| ~ p14(X37)
| ~ p113(X37) )
| p14(X2) )
& ( ! [X38] :
( ~ r1(X2,X38)
| p14(X38)
| ~ p113(X38) )
| ~ p14(X2) ) )
| ~ p113(X2) )
& ( ( ( ! [X39] :
( ~ r1(X2,X39)
| ~ p13(X39)
| ~ p112(X39) )
| p13(X2) )
& ( ! [X40] :
( ~ r1(X2,X40)
| p13(X40)
| ~ p112(X40) )
| ~ p13(X2) ) )
| ~ p112(X2) )
& ( ( ( ! [X41] :
( ~ r1(X2,X41)
| ~ p12(X41)
| ~ p111(X41) )
| p12(X2) )
& ( ! [X42] :
( ~ r1(X2,X42)
| p12(X42)
| ~ p111(X42) )
| ~ p12(X2) ) )
| ~ p111(X2) )
& ( ( ( ! [X43] :
( ~ r1(X2,X43)
| ~ p11(X43)
| ~ p110(X43) )
| p11(X2) )
& ( ! [X44] :
( ~ r1(X2,X44)
| p11(X44)
| ~ p110(X44) )
| ~ p11(X2) ) )
| ~ p110(X2) )
& ( ( ( ! [X45] :
( ~ r1(X2,X45)
| ~ p10(X45)
| ~ p109(X45) )
| p10(X2) )
& ( ! [X46] :
( ~ r1(X2,X46)
| p10(X46)
| ~ p109(X46) )
| ~ p10(X2) ) )
| ~ p109(X2) )
& ( ( ( ! [X47] :
( ~ r1(X2,X47)
| ~ p9(X47)
| ~ p108(X47) )
| p9(X2) )
& ( ! [X48] :
( ~ r1(X2,X48)
| p9(X48)
| ~ p108(X48) )
| ~ p9(X2) ) )
| ~ p108(X2) )
& ( ( ( ! [X49] :
( ~ r1(X2,X49)
| ~ p8(X49)
| ~ p107(X49) )
| p8(X2) )
& ( ! [X50] :
( ~ r1(X2,X50)
| p8(X50)
| ~ p107(X50) )
| ~ p8(X2) ) )
| ~ p107(X2) )
& ( ( ( ! [X51] :
( ~ r1(X2,X51)
| ~ p7(X51)
| ~ p106(X51) )
| p7(X2) )
& ( ! [X52] :
( ~ r1(X2,X52)
| p7(X52)
| ~ p106(X52) )
| ~ p7(X2) ) )
| ~ p106(X2) )
& ( ( ( ! [X53] :
( ~ r1(X2,X53)
| ~ p6(X53)
| ~ p105(X53) )
| p6(X2) )
& ( ! [X54] :
( ~ r1(X2,X54)
| p6(X54)
| ~ p105(X54) )
| ~ p6(X2) ) )
| ~ p105(X2) )
& ( ( ( ! [X55] :
( ~ r1(X2,X55)
| ~ p5(X55)
| ~ p104(X55) )
| p5(X2) )
& ( ! [X56] :
( ~ r1(X2,X56)
| p5(X56)
| ~ p104(X56) )
| ~ p5(X2) ) )
| ~ p104(X2) )
& ( ( ( ! [X57] :
( ~ r1(X2,X57)
| ~ p4(X57)
| ~ p103(X57) )
| p4(X2) )
& ( ! [X58] :
( ~ r1(X2,X58)
| p4(X58)
| ~ p103(X58) )
| ~ p4(X2) ) )
| ~ p103(X2) )
& ( ( ( ! [X59] :
( ~ r1(X2,X59)
| ~ p3(X59)
| ~ p102(X59) )
| p3(X2) )
& ( ! [X60] :
( ~ r1(X2,X60)
| p3(X60)
| ~ p102(X60) )
| ~ p3(X2) ) )
| ~ p102(X2) )
& ( ( ( ! [X61] :
( ~ r1(X2,X61)
| ~ p2(X61)
| ~ p101(X61) )
| p2(X2) )
& ( ! [X62] :
( ~ r1(X2,X62)
| p2(X62)
| ~ p101(X62) )
| ~ p2(X2) ) )
| ~ p101(X2) )
& ( ( ( ! [X63] :
( ~ r1(X2,X63)
| ~ p1(X63)
| ~ p100(X63) )
| p1(X2) )
& ( ! [X64] :
( ~ r1(X2,X64)
| p1(X64)
| ~ p100(X64) )
| ~ p1(X2) ) )
| ~ p100(X2) )
& ( p115(X2)
| ~ p116(X2) )
& ( p114(X2)
| ~ p115(X2) )
& ( p113(X2)
| ~ p114(X2) )
& ( p112(X2)
| ~ p113(X2) )
& ( p111(X2)
| ~ p112(X2) )
& ( p110(X2)
| ~ p111(X2) )
& ( p109(X2)
| ~ p110(X2) )
& ( p108(X2)
| ~ p109(X2) )
& ( p107(X2)
| ~ p108(X2) )
& ( p106(X2)
| ~ p107(X2) )
& ( p105(X2)
| ~ p106(X2) )
& ( p104(X2)
| ~ p105(X2) )
& ( p103(X2)
| ~ p104(X2) )
& ( p102(X2)
| ~ p103(X2) )
& ( p101(X2)
| ~ p102(X2) )
& ( p100(X2)
| ~ p101(X2) ) ) )
& ~ p101(X0)
& p100(X0) ),
inference(flattening,[],[f9]) ).
fof(f11,definition,
! [X2] :
( ( ? [X31] :
( r1(X2,X31)
& ~ p2(X31)
& ~ p102(X31)
& p101(X31) )
& ? [X32] :
( r1(X2,X32)
& p2(X32)
& ~ p102(X32)
& p101(X32) ) )
| p101(X2)
| ~ p100(X2)
| ~ sP0(X2) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f12,definition,
! [X2] :
( ( ? [X29] :
( r1(X2,X29)
& ~ p3(X29)
& ~ p103(X29)
& p102(X29) )
& ? [X30] :
( r1(X2,X30)
& p3(X30)
& ~ p103(X30)
& p102(X30) ) )
| p102(X2)
| ~ p101(X2)
| ~ sP1(X2) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f13,definition,
! [X2] :
( ( ? [X27] :
( r1(X2,X27)
& ~ p4(X27)
& ~ p104(X27)
& p103(X27) )
& ? [X28] :
( r1(X2,X28)
& p4(X28)
& ~ p104(X28)
& p103(X28) ) )
| p103(X2)
| ~ p102(X2)
| ~ sP2(X2) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f14,definition,
! [X2] :
( ( ? [X25] :
( r1(X2,X25)
& ~ p5(X25)
& ~ p105(X25)
& p104(X25) )
& ? [X26] :
( r1(X2,X26)
& p5(X26)
& ~ p105(X26)
& p104(X26) ) )
| p104(X2)
| ~ p103(X2)
| ~ sP3(X2) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f15,definition,
! [X2] :
( ( ? [X23] :
( r1(X2,X23)
& ~ p6(X23)
& ~ p106(X23)
& p105(X23) )
& ? [X24] :
( r1(X2,X24)
& p6(X24)
& ~ p106(X24)
& p105(X24) ) )
| p105(X2)
| ~ p104(X2)
| ~ sP4(X2) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f16,definition,
! [X2] :
( ( ? [X21] :
( r1(X2,X21)
& ~ p7(X21)
& ~ p107(X21)
& p106(X21) )
& ? [X22] :
( r1(X2,X22)
& p7(X22)
& ~ p107(X22)
& p106(X22) ) )
| p106(X2)
| ~ p105(X2)
| ~ sP5(X2) ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f17,definition,
! [X2] :
( ( ? [X19] :
( r1(X2,X19)
& ~ p8(X19)
& ~ p108(X19)
& p107(X19) )
& ? [X20] :
( r1(X2,X20)
& p8(X20)
& ~ p108(X20)
& p107(X20) ) )
| p107(X2)
| ~ p106(X2)
| ~ sP6(X2) ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f18,definition,
! [X2] :
( ( ? [X17] :
( r1(X2,X17)
& ~ p9(X17)
& ~ p109(X17)
& p108(X17) )
& ? [X18] :
( r1(X2,X18)
& p9(X18)
& ~ p109(X18)
& p108(X18) ) )
| p108(X2)
| ~ p107(X2)
| ~ sP7(X2) ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f19,definition,
! [X2] :
( ( ? [X15] :
( r1(X2,X15)
& ~ p10(X15)
& ~ p110(X15)
& p109(X15) )
& ? [X16] :
( r1(X2,X16)
& p10(X16)
& ~ p110(X16)
& p109(X16) ) )
| p109(X2)
| ~ p108(X2)
| ~ sP8(X2) ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f20,definition,
! [X2] :
( ( ? [X13] :
( r1(X2,X13)
& ~ p11(X13)
& ~ p111(X13)
& p110(X13) )
& ? [X14] :
( r1(X2,X14)
& p11(X14)
& ~ p111(X14)
& p110(X14) ) )
| p110(X2)
| ~ p109(X2)
| ~ sP9(X2) ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f21,definition,
! [X2] :
( ( ? [X11] :
( r1(X2,X11)
& ~ p12(X11)
& ~ p112(X11)
& p111(X11) )
& ? [X12] :
( r1(X2,X12)
& p12(X12)
& ~ p112(X12)
& p111(X12) ) )
| p111(X2)
| ~ p110(X2)
| ~ sP10(X2) ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f22,definition,
! [X2] :
( ( ? [X9] :
( r1(X2,X9)
& ~ p13(X9)
& ~ p113(X9)
& p112(X9) )
& ? [X10] :
( r1(X2,X10)
& p13(X10)
& ~ p113(X10)
& p112(X10) ) )
| p112(X2)
| ~ p111(X2)
| ~ sP11(X2) ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f23,definition,
! [X2] :
( ( ? [X7] :
( r1(X2,X7)
& ~ p14(X7)
& ~ p114(X7)
& p113(X7) )
& ? [X8] :
( r1(X2,X8)
& p14(X8)
& ~ p114(X8)
& p113(X8) ) )
| p113(X2)
| ~ p112(X2)
| ~ sP12(X2) ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f24,definition,
! [X2] :
( ( ? [X5] :
( r1(X2,X5)
& ~ p15(X5)
& ~ p115(X5)
& p114(X5) )
& ? [X6] :
( r1(X2,X6)
& p15(X6)
& ~ p115(X6)
& p114(X6) ) )
| p114(X2)
| ~ p113(X2)
| ~ sP13(X2) ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f25,definition,
! [X2] :
( ( ? [X3] :
( r1(X2,X3)
& ~ p16(X3)
& ~ p116(X3)
& p115(X3) )
& ? [X4] :
( r1(X2,X4)
& p16(X4)
& ~ p116(X4)
& p115(X4) ) )
| p115(X2)
| ~ p114(X2)
| ~ sP14(X2) ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f26,definition,
! [X2] :
( ( ( ! [X63] :
( ~ r1(X2,X63)
| ~ p1(X63)
| ~ p100(X63) )
| p1(X2) )
& ( ! [X64] :
( ~ r1(X2,X64)
| p1(X64)
| ~ p100(X64) )
| ~ p1(X2) ) )
| ~ p100(X2)
| ~ sP15(X2) ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f27,definition,
! [X2] :
( ( ( ! [X61] :
( ~ r1(X2,X61)
| ~ p2(X61)
| ~ p101(X61) )
| p2(X2) )
& ( ! [X62] :
( ~ r1(X2,X62)
| p2(X62)
| ~ p101(X62) )
| ~ p2(X2) ) )
| ~ p101(X2)
| ~ sP16(X2) ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f28,definition,
! [X2] :
( ( ( ! [X59] :
( ~ r1(X2,X59)
| ~ p3(X59)
| ~ p102(X59) )
| p3(X2) )
& ( ! [X60] :
( ~ r1(X2,X60)
| p3(X60)
| ~ p102(X60) )
| ~ p3(X2) ) )
| ~ p102(X2)
| ~ sP17(X2) ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f29,definition,
! [X2] :
( ( ( ! [X57] :
( ~ r1(X2,X57)
| ~ p4(X57)
| ~ p103(X57) )
| p4(X2) )
& ( ! [X58] :
( ~ r1(X2,X58)
| p4(X58)
| ~ p103(X58) )
| ~ p4(X2) ) )
| ~ p103(X2)
| ~ sP18(X2) ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f30,definition,
! [X2] :
( ( ( ! [X55] :
( ~ r1(X2,X55)
| ~ p5(X55)
| ~ p104(X55) )
| p5(X2) )
& ( ! [X56] :
( ~ r1(X2,X56)
| p5(X56)
| ~ p104(X56) )
| ~ p5(X2) ) )
| ~ p104(X2)
| ~ sP19(X2) ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f31,definition,
! [X2] :
( ( ( ! [X53] :
( ~ r1(X2,X53)
| ~ p6(X53)
| ~ p105(X53) )
| p6(X2) )
& ( ! [X54] :
( ~ r1(X2,X54)
| p6(X54)
| ~ p105(X54) )
| ~ p6(X2) ) )
| ~ p105(X2)
| ~ sP20(X2) ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f32,definition,
! [X2] :
( ( ( ! [X51] :
( ~ r1(X2,X51)
| ~ p7(X51)
| ~ p106(X51) )
| p7(X2) )
& ( ! [X52] :
( ~ r1(X2,X52)
| p7(X52)
| ~ p106(X52) )
| ~ p7(X2) ) )
| ~ p106(X2)
| ~ sP21(X2) ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f33,definition,
! [X2] :
( ( ( ! [X49] :
( ~ r1(X2,X49)
| ~ p8(X49)
| ~ p107(X49) )
| p8(X2) )
& ( ! [X50] :
( ~ r1(X2,X50)
| p8(X50)
| ~ p107(X50) )
| ~ p8(X2) ) )
| ~ p107(X2)
| ~ sP22(X2) ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f34,definition,
! [X2] :
( ( ( ! [X47] :
( ~ r1(X2,X47)
| ~ p9(X47)
| ~ p108(X47) )
| p9(X2) )
& ( ! [X48] :
( ~ r1(X2,X48)
| p9(X48)
| ~ p108(X48) )
| ~ p9(X2) ) )
| ~ p108(X2)
| ~ sP23(X2) ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f35,definition,
! [X2] :
( ( ( ! [X45] :
( ~ r1(X2,X45)
| ~ p10(X45)
| ~ p109(X45) )
| p10(X2) )
& ( ! [X46] :
( ~ r1(X2,X46)
| p10(X46)
| ~ p109(X46) )
| ~ p10(X2) ) )
| ~ p109(X2)
| ~ sP24(X2) ),
introduced(definition,[new_symbols(definition,[sP24])],[predicate_definition_introduction]) ).
fof(f36,definition,
! [X2] :
( ( ( ! [X43] :
( ~ r1(X2,X43)
| ~ p11(X43)
| ~ p110(X43) )
| p11(X2) )
& ( ! [X44] :
( ~ r1(X2,X44)
| p11(X44)
| ~ p110(X44) )
| ~ p11(X2) ) )
| ~ p110(X2)
| ~ sP25(X2) ),
introduced(definition,[new_symbols(definition,[sP25])],[predicate_definition_introduction]) ).
fof(f37,definition,
! [X2] :
( ( ( ! [X41] :
( ~ r1(X2,X41)
| ~ p12(X41)
| ~ p111(X41) )
| p12(X2) )
& ( ! [X42] :
( ~ r1(X2,X42)
| p12(X42)
| ~ p111(X42) )
| ~ p12(X2) ) )
| ~ p111(X2)
| ~ sP26(X2) ),
introduced(definition,[new_symbols(definition,[sP26])],[predicate_definition_introduction]) ).
fof(f38,definition,
! [X2] :
( ( ( ! [X39] :
( ~ r1(X2,X39)
| ~ p13(X39)
| ~ p112(X39) )
| p13(X2) )
& ( ! [X40] :
( ~ r1(X2,X40)
| p13(X40)
| ~ p112(X40) )
| ~ p13(X2) ) )
| ~ p112(X2)
| ~ sP27(X2) ),
introduced(definition,[new_symbols(definition,[sP27])],[predicate_definition_introduction]) ).
fof(f39,definition,
! [X2] :
( ( ( ! [X37] :
( ~ r1(X2,X37)
| ~ p14(X37)
| ~ p113(X37) )
| p14(X2) )
& ( ! [X38] :
( ~ r1(X2,X38)
| p14(X38)
| ~ p113(X38) )
| ~ p14(X2) ) )
| ~ p113(X2)
| ~ sP28(X2) ),
introduced(definition,[new_symbols(definition,[sP28])],[predicate_definition_introduction]) ).
fof(f40,definition,
! [X2] :
( ( ( ! [X35] :
( ~ r1(X2,X35)
| ~ p15(X35)
| ~ p114(X35) )
| p15(X2) )
& ( ! [X36] :
( ~ r1(X2,X36)
| p15(X36)
| ~ p114(X36) )
| ~ p15(X2) ) )
| ~ p114(X2)
| ~ sP29(X2) ),
introduced(definition,[new_symbols(definition,[sP29])],[predicate_definition_introduction]) ).
fof(f41,definition,
! [X2] :
( ( ( ! [X33] :
( ~ r1(X2,X33)
| ~ p16(X33)
| ~ p115(X33) )
| p16(X2) )
& ( ! [X34] :
( ~ r1(X2,X34)
| p16(X34)
| ~ p115(X34) )
| ~ p16(X2) ) )
| ~ p115(X2)
| ~ sP30(X2) ),
introduced(definition,[new_symbols(definition,[sP30])],[predicate_definition_introduction]) ).
fof(f42,definition,
! [X2] :
( ( sP14(X2)
& sP13(X2)
& sP12(X2)
& sP11(X2)
& sP10(X2)
& sP9(X2)
& sP8(X2)
& sP7(X2)
& sP6(X2)
& sP5(X2)
& sP4(X2)
& sP3(X2)
& sP2(X2)
& sP1(X2)
& sP0(X2)
& sP30(X2)
& sP29(X2)
& sP28(X2)
& sP27(X2)
& sP26(X2)
& sP25(X2)
& sP24(X2)
& sP23(X2)
& sP22(X2)
& sP21(X2)
& sP20(X2)
& sP19(X2)
& sP18(X2)
& sP17(X2)
& sP16(X2)
& sP15(X2)
& ( p115(X2)
| ~ p116(X2) )
& ( p114(X2)
| ~ p115(X2) )
& ( p113(X2)
| ~ p114(X2) )
& ( p112(X2)
| ~ p113(X2) )
& ( p111(X2)
| ~ p112(X2) )
& ( p110(X2)
| ~ p111(X2) )
& ( p109(X2)
| ~ p110(X2) )
& ( p108(X2)
| ~ p109(X2) )
& ( p107(X2)
| ~ p108(X2) )
& ( p106(X2)
| ~ p107(X2) )
& ( p105(X2)
| ~ p106(X2) )
& ( p104(X2)
| ~ p105(X2) )
& ( p103(X2)
| ~ p104(X2) )
& ( p102(X2)
| ~ p103(X2) )
& ( p101(X2)
| ~ p102(X2) )
& ( p100(X2)
| ~ p101(X2) ) )
| ~ sP31(X2) ),
introduced(definition,[new_symbols(definition,[sP31])],[predicate_definition_introduction]) ).
fof(f43,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| p7(X1) )
& ! [X2] :
( ~ r1(X0,X2)
| sP31(X2) )
& ~ p101(X0)
& p100(X0) ),
inference(definition_folding,[],[f10,f42,f41,f40,f39,f38,f37,f36,f35,f34,f33,f32,f31,f30,f29,f28,f27,f26,f25,f24,f23,f22,f21,f20,f19,f18,f17,f16,f15,f14,f13,f12,f11]) ).
fof(f44,plain,
! [X2] :
( ( sP14(X2)
& sP13(X2)
& sP12(X2)
& sP11(X2)
& sP10(X2)
& sP9(X2)
& sP8(X2)
& sP7(X2)
& sP6(X2)
& sP5(X2)
& sP4(X2)
& sP3(X2)
& sP2(X2)
& sP1(X2)
& sP0(X2)
& sP30(X2)
& sP29(X2)
& sP28(X2)
& sP27(X2)
& sP26(X2)
& sP25(X2)
& sP24(X2)
& sP23(X2)
& sP22(X2)
& sP21(X2)
& sP20(X2)
& sP19(X2)
& sP18(X2)
& sP17(X2)
& sP16(X2)
& sP15(X2)
& ( p115(X2)
| ~ p116(X2) )
& ( p114(X2)
| ~ p115(X2) )
& ( p113(X2)
| ~ p114(X2) )
& ( p112(X2)
| ~ p113(X2) )
& ( p111(X2)
| ~ p112(X2) )
& ( p110(X2)
| ~ p111(X2) )
& ( p109(X2)
| ~ p110(X2) )
& ( p108(X2)
| ~ p109(X2) )
& ( p107(X2)
| ~ p108(X2) )
& ( p106(X2)
| ~ p107(X2) )
& ( p105(X2)
| ~ p106(X2) )
& ( p104(X2)
| ~ p105(X2) )
& ( p103(X2)
| ~ p104(X2) )
& ( p102(X2)
| ~ p103(X2) )
& ( p101(X2)
| ~ p102(X2) )
& ( p100(X2)
| ~ p101(X2) ) )
| ~ sP31(X2) ),
inference(nnf_transformation,[],[f42]) ).
fof(f45,plain,
! [X0] :
( ( sP14(X0)
& sP13(X0)
& sP12(X0)
& sP11(X0)
& sP10(X0)
& sP9(X0)
& sP8(X0)
& sP7(X0)
& sP6(X0)
& sP5(X0)
& sP4(X0)
& sP3(X0)
& sP2(X0)
& sP1(X0)
& sP0(X0)
& sP30(X0)
& sP29(X0)
& sP28(X0)
& sP27(X0)
& sP26(X0)
& sP25(X0)
& sP24(X0)
& sP23(X0)
& sP22(X0)
& sP21(X0)
& sP20(X0)
& sP19(X0)
& sP18(X0)
& sP17(X0)
& sP16(X0)
& sP15(X0)
& ( p115(X0)
| ~ p116(X0) )
& ( p114(X0)
| ~ p115(X0) )
& ( p113(X0)
| ~ p114(X0) )
& ( p112(X0)
| ~ p113(X0) )
& ( p111(X0)
| ~ p112(X0) )
& ( p110(X0)
| ~ p111(X0) )
& ( p109(X0)
| ~ p110(X0) )
& ( p108(X0)
| ~ p109(X0) )
& ( p107(X0)
| ~ p108(X0) )
& ( p106(X0)
| ~ p107(X0) )
& ( p105(X0)
| ~ p106(X0) )
& ( p104(X0)
| ~ p105(X0) )
& ( p103(X0)
| ~ p104(X0) )
& ( p102(X0)
| ~ p103(X0) )
& ( p101(X0)
| ~ p102(X0) )
& ( p100(X0)
| ~ p101(X0) ) )
| ~ sP31(X0) ),
inference(rectify,[],[f44]) ).
fof(f105,plain,
! [X2] :
( ( ? [X21] :
( r1(X2,X21)
& ~ p7(X21)
& ~ p107(X21)
& p106(X21) )
& ? [X22] :
( r1(X2,X22)
& p7(X22)
& ~ p107(X22)
& p106(X22) ) )
| p106(X2)
| ~ p105(X2)
| ~ sP5(X2) ),
inference(nnf_transformation,[],[f16]) ).
fof(f106,plain,
! [X0] :
( ( ? [X1] :
( r1(X0,X1)
& ~ p7(X1)
& ~ p107(X1)
& p106(X1) )
& ? [X2] :
( r1(X0,X2)
& p7(X2)
& ~ p107(X2)
& p106(X2) ) )
| p106(X0)
| ~ p105(X0)
| ~ sP5(X0) ),
inference(rectify,[],[f105]) ).
fof(f107,plain,
! [X0] :
( ( r1(X0,sK50(X0))
& ~ p7(sK50(X0))
& ~ p107(sK50(X0))
& p106(sK50(X0))
& r1(X0,sK51(X0))
& p7(sK51(X0))
& ~ p107(sK51(X0))
& p106(sK51(X0)) )
| p106(X0)
| ~ p105(X0)
| ~ sP5(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK50,sK51]),skolemize(X1,sK50(X0)),skolemize(X2,sK51(X0))],[f106]) ).
fof(f108,plain,
! [X2] :
( ( ? [X23] :
( r1(X2,X23)
& ~ p6(X23)
& ~ p106(X23)
& p105(X23) )
& ? [X24] :
( r1(X2,X24)
& p6(X24)
& ~ p106(X24)
& p105(X24) ) )
| p105(X2)
| ~ p104(X2)
| ~ sP4(X2) ),
inference(nnf_transformation,[],[f15]) ).
fof(f109,plain,
! [X0] :
( ( ? [X1] :
( r1(X0,X1)
& ~ p6(X1)
& ~ p106(X1)
& p105(X1) )
& ? [X2] :
( r1(X0,X2)
& p6(X2)
& ~ p106(X2)
& p105(X2) ) )
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ),
inference(rectify,[],[f108]) ).
fof(f110,plain,
! [X0] :
( ( r1(X0,sK52(X0))
& ~ p6(sK52(X0))
& ~ p106(sK52(X0))
& p105(sK52(X0))
& r1(X0,sK53(X0))
& p6(sK53(X0))
& ~ p106(sK53(X0))
& p105(sK53(X0)) )
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK52,sK53]),skolemize(X1,sK52(X0)),skolemize(X2,sK53(X0))],[f109]) ).
fof(f111,plain,
! [X2] :
( ( ? [X25] :
( r1(X2,X25)
& ~ p5(X25)
& ~ p105(X25)
& p104(X25) )
& ? [X26] :
( r1(X2,X26)
& p5(X26)
& ~ p105(X26)
& p104(X26) ) )
| p104(X2)
| ~ p103(X2)
| ~ sP3(X2) ),
inference(nnf_transformation,[],[f14]) ).
fof(f112,plain,
! [X0] :
( ( ? [X1] :
( r1(X0,X1)
& ~ p5(X1)
& ~ p105(X1)
& p104(X1) )
& ? [X2] :
( r1(X0,X2)
& p5(X2)
& ~ p105(X2)
& p104(X2) ) )
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ),
inference(rectify,[],[f111]) ).
fof(f113,plain,
! [X0] :
( ( r1(X0,sK54(X0))
& ~ p5(sK54(X0))
& ~ p105(sK54(X0))
& p104(sK54(X0))
& r1(X0,sK55(X0))
& p5(sK55(X0))
& ~ p105(sK55(X0))
& p104(sK55(X0)) )
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK54,sK55]),skolemize(X1,sK54(X0)),skolemize(X2,sK55(X0))],[f112]) ).
fof(f114,plain,
! [X2] :
( ( ? [X27] :
( r1(X2,X27)
& ~ p4(X27)
& ~ p104(X27)
& p103(X27) )
& ? [X28] :
( r1(X2,X28)
& p4(X28)
& ~ p104(X28)
& p103(X28) ) )
| p103(X2)
| ~ p102(X2)
| ~ sP2(X2) ),
inference(nnf_transformation,[],[f13]) ).
fof(f115,plain,
! [X0] :
( ( ? [X1] :
( r1(X0,X1)
& ~ p4(X1)
& ~ p104(X1)
& p103(X1) )
& ? [X2] :
( r1(X0,X2)
& p4(X2)
& ~ p104(X2)
& p103(X2) ) )
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ),
inference(rectify,[],[f114]) ).
fof(f116,plain,
! [X0] :
( ( r1(X0,sK56(X0))
& ~ p4(sK56(X0))
& ~ p104(sK56(X0))
& p103(sK56(X0))
& r1(X0,sK57(X0))
& p4(sK57(X0))
& ~ p104(sK57(X0))
& p103(sK57(X0)) )
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK56,sK57]),skolemize(X1,sK56(X0)),skolemize(X2,sK57(X0))],[f115]) ).
fof(f117,plain,
! [X2] :
( ( ? [X29] :
( r1(X2,X29)
& ~ p3(X29)
& ~ p103(X29)
& p102(X29) )
& ? [X30] :
( r1(X2,X30)
& p3(X30)
& ~ p103(X30)
& p102(X30) ) )
| p102(X2)
| ~ p101(X2)
| ~ sP1(X2) ),
inference(nnf_transformation,[],[f12]) ).
fof(f118,plain,
! [X0] :
( ( ? [X1] :
( r1(X0,X1)
& ~ p3(X1)
& ~ p103(X1)
& p102(X1) )
& ? [X2] :
( r1(X0,X2)
& p3(X2)
& ~ p103(X2)
& p102(X2) ) )
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ),
inference(rectify,[],[f117]) ).
fof(f119,plain,
! [X0] :
( ( r1(X0,sK58(X0))
& ~ p3(sK58(X0))
& ~ p103(sK58(X0))
& p102(sK58(X0))
& r1(X0,sK59(X0))
& p3(sK59(X0))
& ~ p103(sK59(X0))
& p102(sK59(X0)) )
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK58,sK59]),skolemize(X1,sK58(X0)),skolemize(X2,sK59(X0))],[f118]) ).
fof(f120,plain,
! [X2] :
( ( ? [X31] :
( r1(X2,X31)
& ~ p2(X31)
& ~ p102(X31)
& p101(X31) )
& ? [X32] :
( r1(X2,X32)
& p2(X32)
& ~ p102(X32)
& p101(X32) ) )
| p101(X2)
| ~ p100(X2)
| ~ sP0(X2) ),
inference(nnf_transformation,[],[f11]) ).
fof(f121,plain,
! [X0] :
( ( ? [X1] :
( r1(X0,X1)
& ~ p2(X1)
& ~ p102(X1)
& p101(X1) )
& ? [X2] :
( r1(X0,X2)
& p2(X2)
& ~ p102(X2)
& p101(X2) ) )
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ),
inference(rectify,[],[f120]) ).
fof(f122,plain,
! [X0] :
( ( r1(X0,sK60(X0))
& ~ p2(sK60(X0))
& ~ p102(sK60(X0))
& p101(sK60(X0))
& r1(X0,sK61(X0))
& p2(sK61(X0))
& ~ p102(sK61(X0))
& p101(sK61(X0)) )
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK60,sK61]),skolemize(X1,sK60(X0)),skolemize(X2,sK61(X0))],[f121]) ).
fof(f123,plain,
( ! [X1] :
( ~ r1(sK62,X1)
| p7(X1) )
& ! [X2] :
( ~ r1(sK62,X2)
| sP31(X2) )
& ~ p101(sK62)
& p100(sK62) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK62]),skolemize(X0,sK62)],[f43]) ).
fof(f124,plain,
! [X0] : r1(X0,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f125,plain,
! [X2,X0,X1] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| r1(X0,X2) ),
inference(cnf_transformation,[],[f8]) ).
fof(f158,plain,
! [X0] :
( ~ sP31(X0)
| sP0(X0) ),
inference(cnf_transformation,[],[f45]) ).
fof(f159,plain,
! [X0] :
( sP1(X0)
| ~ sP31(X0) ),
inference(cnf_transformation,[],[f45]) ).
fof(f160,plain,
! [X0] :
( sP2(X0)
| ~ sP31(X0) ),
inference(cnf_transformation,[],[f45]) ).
fof(f161,plain,
! [X0] :
( sP3(X0)
| ~ sP31(X0) ),
inference(cnf_transformation,[],[f45]) ).
fof(f162,plain,
! [X0] :
( sP4(X0)
| ~ sP31(X0) ),
inference(cnf_transformation,[],[f45]) ).
fof(f163,plain,
! [X0] :
( sP5(X0)
| ~ sP31(X0) ),
inference(cnf_transformation,[],[f45]) ).
fof(f283,plain,
! [X0] :
( ~ p7(sK50(X0))
| p106(X0)
| ~ p105(X0)
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f107]) ).
fof(f284,plain,
! [X0] :
( ~ p105(X0)
| p106(X0)
| r1(X0,sK50(X0))
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f107]) ).
fof(f285,plain,
! [X0] :
( ~ p104(X0)
| p105(X0)
| p105(sK53(X0))
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f110]) ).
fof(f286,plain,
! [X0] :
( ~ p106(sK53(X0))
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f110]) ).
fof(f288,plain,
! [X0] :
( ~ p104(X0)
| p105(X0)
| r1(X0,sK53(X0))
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f110]) ).
fof(f293,plain,
! [X0] :
( ~ p103(X0)
| p104(X0)
| p104(sK55(X0))
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f113]) ).
fof(f294,plain,
! [X0] :
( ~ p105(sK55(X0))
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f113]) ).
fof(f296,plain,
! [X0] :
( ~ p103(X0)
| p104(X0)
| r1(X0,sK55(X0))
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f113]) ).
fof(f301,plain,
! [X0] :
( ~ sP2(X0)
| p103(X0)
| ~ p102(X0)
| p103(sK57(X0)) ),
inference(cnf_transformation,[],[f116]) ).
fof(f302,plain,
! [X0] :
( ~ p104(sK57(X0))
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f304,plain,
! [X0] :
( ~ p102(X0)
| p103(X0)
| r1(X0,sK57(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f309,plain,
! [X0] :
( ~ sP1(X0)
| p102(X0)
| ~ p101(X0)
| p102(sK59(X0)) ),
inference(cnf_transformation,[],[f119]) ).
fof(f310,plain,
! [X0] :
( ~ p103(sK59(X0))
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f119]) ).
fof(f312,plain,
! [X0] :
( ~ sP1(X0)
| p102(X0)
| ~ p101(X0)
| r1(X0,sK59(X0)) ),
inference(cnf_transformation,[],[f119]) ).
fof(f321,plain,
! [X0] :
( p101(sK60(X0))
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f122]) ).
fof(f322,plain,
! [X0] :
( ~ p102(sK60(X0))
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f122]) ).
fof(f324,plain,
! [X0] :
( ~ sP0(X0)
| p101(X0)
| ~ p100(X0)
| r1(X0,sK60(X0)) ),
inference(cnf_transformation,[],[f122]) ).
fof(f325,plain,
p100(sK62),
inference(cnf_transformation,[],[f123]) ).
fof(f326,plain,
~ p101(sK62),
inference(cnf_transformation,[],[f123]) ).
fof(f327,plain,
! [X2] :
( ~ r1(sK62,X2)
| sP31(X2) ),
inference(cnf_transformation,[],[f123]) ).
fof(f328,plain,
! [X1] :
( ~ r1(sK62,X1)
| p7(X1) ),
inference(cnf_transformation,[],[f123]) ).
fof(f330,plain,
sP31(sK62),
inference(resolution,[],[f124,f327]) ).
fof(f331,plain,
sP0(sK62),
inference(resolution,[],[f158,f330]) ).
fof(f335,plain,
! [X0] :
( ~ sP31(X0)
| ~ p101(X0)
| r1(X0,sK59(X0))
| p102(X0) ),
inference(resolution,[],[f312,f159]) ).
fof(f337,plain,
( p101(sK62)
| ~ p100(sK62)
| r1(sK62,sK60(sK62)) ),
inference(resolution,[],[f331,f324]) ).
fof(f340,plain,
( ~ p100(sK62)
| r1(sK62,sK60(sK62)) ),
inference(forward_subsumption_resolution,[],[f337,f326]) ).
fof(f342,plain,
r1(sK62,sK60(sK62)),
inference(forward_subsumption_resolution,[],[f340,f325]) ).
fof(f347,plain,
sP31(sK60(sK62)),
inference(resolution,[],[f342,f327]) ).
fof(f368,plain,
( ~ p101(sK60(sK62))
| r1(sK60(sK62),sK59(sK60(sK62)))
| p102(sK60(sK62)) ),
inference(resolution,[],[f347,f335]) ).
fof(f372,definition,
( spl63_5
<=> p102(sK60(sK62)) ),
introduced(definition,[new_symbols(definition,[spl63_5])],[avatar_definition]) ).
fof(f373,plain,
( p102(sK60(sK62))
| ~ spl63_5 ),
inference(avatar_component_clause,[],[f372]) ).
fof(f378,definition,
( spl63_7
<=> p101(sK60(sK62)) ),
introduced(definition,[new_symbols(definition,[spl63_7])],[avatar_definition]) ).
fof(f379,plain,
( ~ p101(sK60(sK62))
| spl63_7 ),
inference(avatar_component_clause,[],[f378]) ).
fof(f382,definition,
( spl63_8
<=> r1(sK60(sK62),sK59(sK60(sK62))) ),
introduced(definition,[new_symbols(definition,[spl63_8])],[avatar_definition]) ).
fof(f383,plain,
( r1(sK60(sK62),sK59(sK60(sK62)))
| ~ spl63_8 ),
inference(avatar_component_clause,[],[f382]) ).
fof(f384,plain,
( spl63_5
| spl63_8
| ~ spl63_7 ),
inference(avatar_split_clause,[],[f368,f378,f382,f372]) ).
fof(f395,plain,
( p101(sK62)
| ~ p100(sK62)
| ~ sP0(sK62)
| spl63_7 ),
inference(resolution,[],[f379,f321]) ).
fof(f397,plain,
( ~ p100(sK62)
| ~ sP0(sK62)
| spl63_7 ),
inference(forward_subsumption_resolution,[],[f395,f326]) ).
fof(f398,plain,
( ~ sP0(sK62)
| spl63_7 ),
inference(forward_subsumption_resolution,[],[f397,f325]) ).
fof(f399,plain,
( $false
| spl63_7 ),
inference(forward_subsumption_resolution,[],[f398,f331]) ).
fof(f400,plain,
spl63_7,
inference(avatar_contradiction_clause,[],[f399]) ).
fof(f401,plain,
( ! [X0] :
( ~ r1(X0,sK60(sK62))
| r1(X0,sK59(sK60(sK62))) )
| ~ spl63_8 ),
inference(resolution,[],[f383,f125]) ).
fof(f409,plain,
! [X0] :
( ~ p101(X0)
| p102(X0)
| p102(sK59(X0))
| ~ sP31(X0) ),
inference(resolution,[],[f309,f159]) ).
fof(f411,plain,
! [X0] :
( p102(sK60(X0))
| p102(sK59(sK60(X0)))
| ~ sP31(sK60(X0))
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ),
inference(resolution,[],[f409,f321]) ).
fof(f412,plain,
! [X0] :
( ~ sP31(sK60(X0))
| p102(sK59(sK60(X0)))
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ),
inference(forward_subsumption_resolution,[],[f411,f322]) ).
fof(f436,plain,
( p102(sK59(sK60(sK62)))
| p101(sK62)
| ~ p100(sK62)
| ~ sP0(sK62) ),
inference(resolution,[],[f412,f347]) ).
fof(f437,plain,
( p102(sK59(sK60(sK62)))
| ~ p100(sK62)
| ~ sP0(sK62) ),
inference(forward_subsumption_resolution,[],[f436,f326]) ).
fof(f438,plain,
( p102(sK59(sK60(sK62)))
| ~ sP0(sK62) ),
inference(forward_subsumption_resolution,[],[f437,f325]) ).
fof(f439,plain,
p102(sK59(sK60(sK62))),
inference(forward_subsumption_resolution,[],[f438,f331]) ).
fof(f441,plain,
( p103(sK59(sK60(sK62)))
| r1(sK59(sK60(sK62)),sK57(sK59(sK60(sK62))))
| ~ sP2(sK59(sK60(sK62))) ),
inference(resolution,[],[f439,f304]) ).
fof(f444,definition,
( spl63_13
<=> sP2(sK59(sK60(sK62))) ),
introduced(definition,[new_symbols(definition,[spl63_13])],[avatar_definition]) ).
fof(f445,plain,
( ~ sP2(sK59(sK60(sK62)))
| spl63_13 ),
inference(avatar_component_clause,[],[f444]) ).
fof(f450,definition,
( spl63_15
<=> p103(sK59(sK60(sK62))) ),
introduced(definition,[new_symbols(definition,[spl63_15])],[avatar_definition]) ).
fof(f451,plain,
( p103(sK59(sK60(sK62)))
| ~ spl63_15 ),
inference(avatar_component_clause,[],[f450]) ).
fof(f454,definition,
( spl63_16
<=> r1(sK59(sK60(sK62)),sK57(sK59(sK60(sK62)))) ),
introduced(definition,[new_symbols(definition,[spl63_16])],[avatar_definition]) ).
fof(f455,plain,
( r1(sK59(sK60(sK62)),sK57(sK59(sK60(sK62))))
| ~ spl63_16 ),
inference(avatar_component_clause,[],[f454]) ).
fof(f456,plain,
( ~ spl63_13
| spl63_16
| spl63_15 ),
inference(avatar_split_clause,[],[f441,f450,f454,f444]) ).
fof(f458,definition,
( spl63_17
<=> sP31(sK59(sK60(sK62))) ),
introduced(definition,[new_symbols(definition,[spl63_17])],[avatar_definition]) ).
fof(f459,plain,
( ~ sP31(sK59(sK60(sK62)))
| spl63_17 ),
inference(avatar_component_clause,[],[f458]) ).
fof(f488,plain,
! [X0] :
( ~ p102(X0)
| p103(X0)
| p103(sK57(X0))
| ~ sP31(X0) ),
inference(resolution,[],[f301,f160]) ).
fof(f490,plain,
( p103(sK59(sK60(sK62)))
| p103(sK57(sK59(sK60(sK62))))
| ~ sP31(sK59(sK60(sK62))) ),
inference(resolution,[],[f488,f439]) ).
fof(f524,plain,
( r1(sK62,sK59(sK60(sK62)))
| ~ spl63_8 ),
inference(resolution,[],[f401,f342]) ).
fof(f527,plain,
( sP31(sK59(sK60(sK62)))
| ~ spl63_8 ),
inference(resolution,[],[f524,f327]) ).
fof(f530,plain,
( $false
| ~ spl63_8
| spl63_17 ),
inference(forward_subsumption_resolution,[],[f527,f459]) ).
fof(f531,plain,
( ~ spl63_8
| spl63_17 ),
inference(avatar_contradiction_clause,[],[f530]) ).
fof(f533,definition,
( spl63_29
<=> p103(sK57(sK59(sK60(sK62)))) ),
introduced(definition,[new_symbols(definition,[spl63_29])],[avatar_definition]) ).
fof(f534,plain,
( p103(sK57(sK59(sK60(sK62))))
| ~ spl63_29 ),
inference(avatar_component_clause,[],[f533]) ).
fof(f535,plain,
( ~ spl63_17
| spl63_29
| spl63_15 ),
inference(avatar_split_clause,[],[f490,f450,f533,f458]) ).
fof(f537,plain,
( p102(sK60(sK62))
| ~ p101(sK60(sK62))
| ~ sP1(sK60(sK62))
| ~ spl63_15 ),
inference(resolution,[],[f451,f310]) ).
fof(f560,definition,
( spl63_35
<=> sP1(sK60(sK62)) ),
introduced(definition,[new_symbols(definition,[spl63_35])],[avatar_definition]) ).
fof(f561,plain,
( ~ sP1(sK60(sK62))
| spl63_35 ),
inference(avatar_component_clause,[],[f560]) ).
fof(f562,plain,
( ~ spl63_35
| ~ spl63_7
| spl63_5
| ~ spl63_15 ),
inference(avatar_split_clause,[],[f537,f450,f372,f378,f560]) ).
fof(f607,plain,
( p101(sK62)
| ~ p100(sK62)
| ~ sP0(sK62)
| ~ spl63_5 ),
inference(resolution,[],[f373,f322]) ).
fof(f629,plain,
( ~ p100(sK62)
| ~ sP0(sK62)
| ~ spl63_5 ),
inference(forward_subsumption_resolution,[],[f607,f326]) ).
fof(f634,plain,
( ~ sP0(sK62)
| ~ spl63_5 ),
inference(forward_subsumption_resolution,[],[f629,f325]) ).
fof(f635,plain,
( $false
| ~ spl63_5 ),
inference(forward_subsumption_resolution,[],[f634,f331]) ).
fof(f636,plain,
~ spl63_5,
inference(avatar_contradiction_clause,[],[f635]) ).
fof(f643,plain,
( p104(sK57(sK59(sK60(sK62))))
| p104(sK55(sK57(sK59(sK60(sK62)))))
| ~ sP3(sK57(sK59(sK60(sK62))))
| ~ spl63_29 ),
inference(resolution,[],[f534,f293]) ).
fof(f644,plain,
( p104(sK57(sK59(sK60(sK62))))
| r1(sK57(sK59(sK60(sK62))),sK55(sK57(sK59(sK60(sK62)))))
| ~ sP3(sK57(sK59(sK60(sK62))))
| ~ spl63_29 ),
inference(resolution,[],[f534,f296]) ).
fof(f647,definition,
( spl63_47
<=> sP3(sK57(sK59(sK60(sK62)))) ),
introduced(definition,[new_symbols(definition,[spl63_47])],[avatar_definition]) ).
fof(f648,plain,
( ~ sP3(sK57(sK59(sK60(sK62))))
| spl63_47 ),
inference(avatar_component_clause,[],[f647]) ).
fof(f653,definition,
( spl63_49
<=> p104(sK57(sK59(sK60(sK62)))) ),
introduced(definition,[new_symbols(definition,[spl63_49])],[avatar_definition]) ).
fof(f654,plain,
( p104(sK57(sK59(sK60(sK62))))
| ~ spl63_49 ),
inference(avatar_component_clause,[],[f653]) ).
fof(f657,definition,
( spl63_50
<=> r1(sK57(sK59(sK60(sK62))),sK55(sK57(sK59(sK60(sK62))))) ),
introduced(definition,[new_symbols(definition,[spl63_50])],[avatar_definition]) ).
fof(f658,plain,
( r1(sK57(sK59(sK60(sK62))),sK55(sK57(sK59(sK60(sK62)))))
| ~ spl63_50 ),
inference(avatar_component_clause,[],[f657]) ).
fof(f659,plain,
( ~ spl63_47
| spl63_50
| spl63_49
| ~ spl63_29 ),
inference(avatar_split_clause,[],[f644,f533,f653,f657,f647]) ).
fof(f661,definition,
( spl63_51
<=> p104(sK55(sK57(sK59(sK60(sK62))))) ),
introduced(definition,[new_symbols(definition,[spl63_51])],[avatar_definition]) ).
fof(f662,plain,
( p104(sK55(sK57(sK59(sK60(sK62)))))
| ~ spl63_51 ),
inference(avatar_component_clause,[],[f661]) ).
fof(f663,plain,
( ~ spl63_47
| spl63_51
| spl63_49
| ~ spl63_29 ),
inference(avatar_split_clause,[],[f643,f533,f653,f661,f647]) ).
fof(f1077,plain,
( ~ sP31(sK59(sK60(sK62)))
| spl63_13 ),
inference(resolution,[],[f445,f160]) ).
fof(f1079,plain,
( $false
| ~ spl63_8
| spl63_13 ),
inference(forward_subsumption_resolution,[],[f1077,f527]) ).
fof(f1080,plain,
( ~ spl63_8
| spl63_13 ),
inference(avatar_contradiction_clause,[],[f1079]) ).
fof(f1081,plain,
( ! [X0] :
( r1(X0,sK57(sK59(sK60(sK62))))
| ~ r1(X0,sK59(sK60(sK62))) )
| ~ spl63_16 ),
inference(resolution,[],[f455,f125]) ).
fof(f1084,plain,
( ~ r1(sK62,sK59(sK60(sK62)))
| sP31(sK57(sK59(sK60(sK62))))
| ~ spl63_16 ),
inference(resolution,[],[f1081,f327]) ).
fof(f1085,plain,
( ! [X0,X1] :
( ~ r1(X0,sK59(sK60(sK62)))
| ~ r1(X1,X0)
| r1(X1,sK57(sK59(sK60(sK62)))) )
| ~ spl63_16 ),
inference(resolution,[],[f1081,f125]) ).
fof(f1086,plain,
( sP31(sK57(sK59(sK60(sK62))))
| ~ spl63_8
| ~ spl63_16 ),
inference(forward_subsumption_resolution,[],[f1084,f524]) ).
fof(f1090,plain,
( p103(sK59(sK60(sK62)))
| ~ p102(sK59(sK60(sK62)))
| ~ sP2(sK59(sK60(sK62)))
| ~ spl63_49 ),
inference(resolution,[],[f654,f302]) ).
fof(f1118,plain,
( p103(sK59(sK60(sK62)))
| ~ sP2(sK59(sK60(sK62)))
| ~ spl63_49 ),
inference(forward_subsumption_resolution,[],[f1090,f439]) ).
fof(f1119,plain,
( ~ spl63_13
| spl63_15
| ~ spl63_49 ),
inference(avatar_split_clause,[],[f1118,f653,f450,f444]) ).
fof(f1256,plain,
( ~ sP31(sK60(sK62))
| spl63_35 ),
inference(resolution,[],[f561,f159]) ).
fof(f1258,plain,
( $false
| spl63_35 ),
inference(forward_subsumption_resolution,[],[f1256,f347]) ).
fof(f1259,plain,
spl63_35,
inference(avatar_contradiction_clause,[],[f1258]) ).
fof(f1549,plain,
( ! [X0] :
( ~ r1(X0,sK60(sK62))
| r1(X0,sK57(sK59(sK60(sK62)))) )
| ~ spl63_8
| ~ spl63_16 ),
inference(resolution,[],[f1085,f383]) ).
fof(f1552,plain,
( r1(sK62,sK57(sK59(sK60(sK62))))
| ~ spl63_8
| ~ spl63_16 ),
inference(resolution,[],[f1549,f342]) ).
fof(f1593,plain,
( ~ sP31(sK57(sK59(sK60(sK62))))
| spl63_47 ),
inference(resolution,[],[f648,f161]) ).
fof(f1595,plain,
( $false
| ~ spl63_8
| ~ spl63_16
| spl63_47 ),
inference(forward_subsumption_resolution,[],[f1593,f1086]) ).
fof(f1596,plain,
( ~ spl63_8
| ~ spl63_16
| spl63_47 ),
inference(avatar_contradiction_clause,[],[f1595]) ).
fof(f1597,plain,
( ! [X0] :
( r1(X0,sK55(sK57(sK59(sK60(sK62)))))
| ~ r1(X0,sK57(sK59(sK60(sK62)))) )
| ~ spl63_50 ),
inference(resolution,[],[f658,f125]) ).
fof(f1600,plain,
( p105(sK55(sK57(sK59(sK60(sK62)))))
| p105(sK53(sK55(sK57(sK59(sK60(sK62))))))
| ~ sP4(sK55(sK57(sK59(sK60(sK62)))))
| ~ spl63_51 ),
inference(resolution,[],[f662,f285]) ).
fof(f1601,plain,
( p105(sK55(sK57(sK59(sK60(sK62)))))
| r1(sK55(sK57(sK59(sK60(sK62)))),sK53(sK55(sK57(sK59(sK60(sK62))))))
| ~ sP4(sK55(sK57(sK59(sK60(sK62)))))
| ~ spl63_51 ),
inference(resolution,[],[f662,f288]) ).
fof(f1604,definition,
( spl63_212
<=> sP4(sK55(sK57(sK59(sK60(sK62))))) ),
introduced(definition,[new_symbols(definition,[spl63_212])],[avatar_definition]) ).
fof(f1605,plain,
( ~ sP4(sK55(sK57(sK59(sK60(sK62)))))
| spl63_212 ),
inference(avatar_component_clause,[],[f1604]) ).
fof(f1610,definition,
( spl63_214
<=> p105(sK55(sK57(sK59(sK60(sK62))))) ),
introduced(definition,[new_symbols(definition,[spl63_214])],[avatar_definition]) ).
fof(f1611,plain,
( p105(sK55(sK57(sK59(sK60(sK62)))))
| ~ spl63_214 ),
inference(avatar_component_clause,[],[f1610]) ).
fof(f1614,definition,
( spl63_215
<=> r1(sK55(sK57(sK59(sK60(sK62)))),sK53(sK55(sK57(sK59(sK60(sK62)))))) ),
introduced(definition,[new_symbols(definition,[spl63_215])],[avatar_definition]) ).
fof(f1615,plain,
( r1(sK55(sK57(sK59(sK60(sK62)))),sK53(sK55(sK57(sK59(sK60(sK62))))))
| ~ spl63_215 ),
inference(avatar_component_clause,[],[f1614]) ).
fof(f1616,plain,
( ~ spl63_212
| spl63_215
| spl63_214
| ~ spl63_51 ),
inference(avatar_split_clause,[],[f1601,f661,f1610,f1614,f1604]) ).
fof(f1618,definition,
( spl63_216
<=> p105(sK53(sK55(sK57(sK59(sK60(sK62)))))) ),
introduced(definition,[new_symbols(definition,[spl63_216])],[avatar_definition]) ).
fof(f1619,plain,
( p105(sK53(sK55(sK57(sK59(sK60(sK62))))))
| ~ spl63_216 ),
inference(avatar_component_clause,[],[f1618]) ).
fof(f1620,plain,
( ~ spl63_212
| spl63_216
| spl63_214
| ~ spl63_51 ),
inference(avatar_split_clause,[],[f1600,f661,f1610,f1618,f1604]) ).
fof(f1634,plain,
( ~ r1(sK62,sK57(sK59(sK60(sK62))))
| sP31(sK55(sK57(sK59(sK60(sK62)))))
| ~ spl63_50 ),
inference(resolution,[],[f1597,f327]) ).
fof(f1636,plain,
( sP31(sK55(sK57(sK59(sK60(sK62)))))
| ~ spl63_8
| ~ spl63_16
| ~ spl63_50 ),
inference(forward_subsumption_resolution,[],[f1634,f1552]) ).
fof(f1724,plain,
( ~ sP31(sK55(sK57(sK59(sK60(sK62)))))
| spl63_212 ),
inference(resolution,[],[f1605,f162]) ).
fof(f1726,plain,
( $false
| ~ spl63_8
| ~ spl63_16
| ~ spl63_50
| spl63_212 ),
inference(forward_subsumption_resolution,[],[f1724,f1636]) ).
fof(f1727,plain,
( ~ spl63_8
| ~ spl63_16
| ~ spl63_50
| spl63_212 ),
inference(avatar_contradiction_clause,[],[f1726]) ).
fof(f1728,plain,
( p104(sK57(sK59(sK60(sK62))))
| ~ p103(sK57(sK59(sK60(sK62))))
| ~ sP3(sK57(sK59(sK60(sK62))))
| ~ spl63_214 ),
inference(resolution,[],[f1611,f294]) ).
fof(f1756,plain,
( p104(sK57(sK59(sK60(sK62))))
| ~ sP3(sK57(sK59(sK60(sK62))))
| ~ spl63_29
| ~ spl63_214 ),
inference(forward_subsumption_resolution,[],[f1728,f534]) ).
fof(f1757,plain,
( ~ spl63_47
| spl63_49
| ~ spl63_29
| ~ spl63_214 ),
inference(avatar_split_clause,[],[f1756,f1610,f533,f653,f647]) ).
fof(f1758,plain,
( ! [X0] :
( r1(X0,sK53(sK55(sK57(sK59(sK60(sK62))))))
| ~ r1(X0,sK55(sK57(sK59(sK60(sK62))))) )
| ~ spl63_215 ),
inference(resolution,[],[f1615,f125]) ).
fof(f1764,plain,
( p106(sK53(sK55(sK57(sK59(sK60(sK62))))))
| r1(sK53(sK55(sK57(sK59(sK60(sK62))))),sK50(sK53(sK55(sK57(sK59(sK60(sK62)))))))
| ~ sP5(sK53(sK55(sK57(sK59(sK60(sK62))))))
| ~ spl63_216 ),
inference(resolution,[],[f1619,f284]) ).
fof(f1766,definition,
( spl63_234
<=> sP5(sK53(sK55(sK57(sK59(sK60(sK62)))))) ),
introduced(definition,[new_symbols(definition,[spl63_234])],[avatar_definition]) ).
fof(f1767,plain,
( ~ sP5(sK53(sK55(sK57(sK59(sK60(sK62))))))
| spl63_234 ),
inference(avatar_component_clause,[],[f1766]) ).
fof(f1769,definition,
( spl63_235
<=> r1(sK53(sK55(sK57(sK59(sK60(sK62))))),sK50(sK53(sK55(sK57(sK59(sK60(sK62))))))) ),
introduced(definition,[new_symbols(definition,[spl63_235])],[avatar_definition]) ).
fof(f1770,plain,
( r1(sK53(sK55(sK57(sK59(sK60(sK62))))),sK50(sK53(sK55(sK57(sK59(sK60(sK62)))))))
| ~ spl63_235 ),
inference(avatar_component_clause,[],[f1769]) ).
fof(f1772,definition,
( spl63_236
<=> p106(sK53(sK55(sK57(sK59(sK60(sK62)))))) ),
introduced(definition,[new_symbols(definition,[spl63_236])],[avatar_definition]) ).
fof(f1773,plain,
( p106(sK53(sK55(sK57(sK59(sK60(sK62))))))
| ~ spl63_236 ),
inference(avatar_component_clause,[],[f1772]) ).
fof(f1774,plain,
( ~ spl63_234
| spl63_235
| spl63_236
| ~ spl63_216 ),
inference(avatar_split_clause,[],[f1764,f1618,f1772,f1769,f1766]) ).
fof(f1784,definition,
( spl63_239
<=> sP31(sK53(sK55(sK57(sK59(sK60(sK62)))))) ),
introduced(definition,[new_symbols(definition,[spl63_239])],[avatar_definition]) ).
fof(f1829,plain,
( ~ r1(sK62,sK55(sK57(sK59(sK60(sK62)))))
| sP31(sK53(sK55(sK57(sK59(sK60(sK62))))))
| ~ spl63_215 ),
inference(resolution,[],[f1758,f327]) ).
fof(f1836,definition,
( spl63_251
<=> r1(sK62,sK55(sK57(sK59(sK60(sK62))))) ),
introduced(definition,[new_symbols(definition,[spl63_251])],[avatar_definition]) ).
fof(f1837,plain,
( ~ r1(sK62,sK55(sK57(sK59(sK60(sK62)))))
| spl63_251 ),
inference(avatar_component_clause,[],[f1836]) ).
fof(f1842,plain,
( ~ r1(sK62,sK57(sK59(sK60(sK62))))
| ~ spl63_50
| spl63_251 ),
inference(resolution,[],[f1837,f1597]) ).
fof(f1845,plain,
( $false
| ~ spl63_8
| ~ spl63_16
| ~ spl63_50
| spl63_251 ),
inference(forward_subsumption_resolution,[],[f1842,f1552]) ).
fof(f1846,plain,
( ~ spl63_8
| ~ spl63_16
| ~ spl63_50
| spl63_251 ),
inference(avatar_contradiction_clause,[],[f1845]) ).
fof(f1847,plain,
( sP31(sK53(sK55(sK57(sK59(sK60(sK62))))))
| ~ spl63_239 ),
inference(avatar_component_clause,[],[f1784]) ).
fof(f1848,plain,
( spl63_239
| ~ spl63_251
| ~ spl63_215 ),
inference(avatar_split_clause,[],[f1829,f1614,f1836,f1784]) ).
fof(f1949,plain,
( ~ sP31(sK53(sK55(sK57(sK59(sK60(sK62))))))
| spl63_234 ),
inference(resolution,[],[f1767,f163]) ).
fof(f1951,plain,
( $false
| spl63_234
| ~ spl63_239 ),
inference(forward_subsumption_resolution,[],[f1949,f1847]) ).
fof(f1952,plain,
( spl63_234
| ~ spl63_239 ),
inference(avatar_contradiction_clause,[],[f1951]) ).
fof(f1953,plain,
( p105(sK55(sK57(sK59(sK60(sK62)))))
| ~ p104(sK55(sK57(sK59(sK60(sK62)))))
| ~ sP4(sK55(sK57(sK59(sK60(sK62)))))
| ~ spl63_236 ),
inference(resolution,[],[f1773,f286]) ).
fof(f1982,plain,
( p105(sK55(sK57(sK59(sK60(sK62)))))
| ~ sP4(sK55(sK57(sK59(sK60(sK62)))))
| ~ spl63_51
| ~ spl63_236 ),
inference(forward_subsumption_resolution,[],[f1953,f662]) ).
fof(f1983,plain,
( ~ spl63_212
| spl63_214
| ~ spl63_51
| ~ spl63_236 ),
inference(avatar_split_clause,[],[f1982,f1772,f661,f1610,f1604]) ).
fof(f1985,plain,
( ! [X0] :
( r1(X0,sK50(sK53(sK55(sK57(sK59(sK60(sK62)))))))
| ~ r1(X0,sK53(sK55(sK57(sK59(sK60(sK62)))))) )
| ~ spl63_235 ),
inference(resolution,[],[f1770,f125]) ).
fof(f2070,definition,
( spl63_287
<=> p7(sK50(sK53(sK55(sK57(sK59(sK60(sK62))))))) ),
introduced(definition,[new_symbols(definition,[spl63_287])],[avatar_definition]) ).
fof(f2071,plain,
( p7(sK50(sK53(sK55(sK57(sK59(sK60(sK62)))))))
| ~ spl63_287 ),
inference(avatar_component_clause,[],[f2070]) ).
fof(f2081,definition,
( spl63_289
<=> r1(sK62,sK53(sK55(sK57(sK59(sK60(sK62)))))) ),
introduced(definition,[new_symbols(definition,[spl63_289])],[avatar_definition]) ).
fof(f2082,plain,
( ~ r1(sK62,sK53(sK55(sK57(sK59(sK60(sK62))))))
| spl63_289 ),
inference(avatar_component_clause,[],[f2081]) ).
fof(f2085,plain,
( ~ r1(sK62,sK55(sK57(sK59(sK60(sK62)))))
| ~ spl63_215
| spl63_289 ),
inference(resolution,[],[f2082,f1758]) ).
fof(f2086,plain,
( ~ spl63_251
| ~ spl63_215
| spl63_289 ),
inference(avatar_split_clause,[],[f2085,f2081,f1614,f1836]) ).
fof(f2137,plain,
( ~ r1(sK62,sK53(sK55(sK57(sK59(sK60(sK62))))))
| p7(sK50(sK53(sK55(sK57(sK59(sK60(sK62)))))))
| ~ spl63_235 ),
inference(resolution,[],[f1985,f328]) ).
fof(f2141,plain,
( spl63_287
| ~ spl63_289
| ~ spl63_235 ),
inference(avatar_split_clause,[],[f2137,f1769,f2081,f2070]) ).
fof(f2168,plain,
( p106(sK53(sK55(sK57(sK59(sK60(sK62))))))
| ~ p105(sK53(sK55(sK57(sK59(sK60(sK62))))))
| ~ sP5(sK53(sK55(sK57(sK59(sK60(sK62))))))
| ~ spl63_287 ),
inference(resolution,[],[f2071,f283]) ).
fof(f2169,plain,
( p106(sK53(sK55(sK57(sK59(sK60(sK62))))))
| ~ sP5(sK53(sK55(sK57(sK59(sK60(sK62))))))
| ~ spl63_216
| ~ spl63_287 ),
inference(forward_subsumption_resolution,[],[f2168,f1619]) ).
fof(f2170,plain,
( ~ spl63_234
| spl63_236
| ~ spl63_216
| ~ spl63_287 ),
inference(avatar_split_clause,[],[f2169,f2070,f1618,f1772,f1766]) ).
cnf(s4,plain,
( spl63_5
| ~ spl63_7
| spl63_8 ),
inference(sat_conversion,[],[f384]) ).
cnf(s8,plain,
spl63_7,
inference(sat_conversion,[],[f400]) ).
cnf(s12,plain,
( ~ spl63_13
| spl63_15
| spl63_16 ),
inference(sat_conversion,[],[f456]) ).
cnf(s22,plain,
( ~ spl63_8
| spl63_17 ),
inference(sat_conversion,[],[f531]) ).
cnf(s23,plain,
( spl63_15
| ~ spl63_17
| spl63_29 ),
inference(sat_conversion,[],[f535]) ).
cnf(s27,plain,
( spl63_5
| ~ spl63_7
| ~ spl63_15
| ~ spl63_35 ),
inference(sat_conversion,[],[f562]) ).
cnf(s36,plain,
~ spl63_5,
inference(sat_conversion,[],[f636]) ).
cnf(s38,plain,
( ~ spl63_29
| ~ spl63_47
| spl63_49
| spl63_50 ),
inference(sat_conversion,[],[f659]) ).
cnf(s39,plain,
( ~ spl63_29
| ~ spl63_47
| spl63_49
| spl63_51 ),
inference(sat_conversion,[],[f663]) ).
cnf(s101,plain,
( ~ spl63_8
| spl63_13 ),
inference(sat_conversion,[],[f1080]) ).
cnf(s107,plain,
( ~ spl63_13
| spl63_15
| ~ spl63_49 ),
inference(sat_conversion,[],[f1119]) ).
cnf(s125,plain,
spl63_35,
inference(sat_conversion,[],[f1259]) ).
cnf(s173,plain,
( ~ spl63_8
| ~ spl63_16
| spl63_47 ),
inference(sat_conversion,[],[f1596]) ).
cnf(s175,plain,
( ~ spl63_51
| ~ spl63_212
| spl63_214
| spl63_215 ),
inference(sat_conversion,[],[f1616]) ).
cnf(s176,plain,
( ~ spl63_51
| ~ spl63_212
| spl63_214
| spl63_216 ),
inference(sat_conversion,[],[f1620]) ).
cnf(s192,plain,
( ~ spl63_8
| ~ spl63_16
| ~ spl63_50
| spl63_212 ),
inference(sat_conversion,[],[f1727]) ).
cnf(s197,plain,
( ~ spl63_29
| ~ spl63_47
| spl63_49
| ~ spl63_214 ),
inference(sat_conversion,[],[f1757]) ).
cnf(s198,plain,
( ~ spl63_216
| ~ spl63_234
| spl63_235
| spl63_236 ),
inference(sat_conversion,[],[f1774]) ).
cnf(s212,plain,
( ~ spl63_8
| ~ spl63_16
| ~ spl63_50
| spl63_251 ),
inference(sat_conversion,[],[f1846]) ).
cnf(s213,plain,
( ~ spl63_215
| spl63_239
| ~ spl63_251 ),
inference(sat_conversion,[],[f1848]) ).
cnf(s228,plain,
( spl63_234
| ~ spl63_239 ),
inference(sat_conversion,[],[f1952]) ).
cnf(s233,plain,
( ~ spl63_51
| ~ spl63_212
| spl63_214
| ~ spl63_236 ),
inference(sat_conversion,[],[f1983]) ).
cnf(s248,plain,
( ~ spl63_215
| ~ spl63_251
| spl63_289 ),
inference(sat_conversion,[],[f2086]) ).
cnf(s255,plain,
( ~ spl63_235
| spl63_287
| ~ spl63_289 ),
inference(sat_conversion,[],[f2141]) ).
cnf(s260,plain,
( ~ spl63_216
| ~ spl63_234
| spl63_236
| ~ spl63_287 ),
inference(sat_conversion,[],[f2170]) ).
cnf(s261,plain,
( ~ spl63_7
| ~ spl63_15 ),
inference(rat,[],[s27,s125,s36]) ).
cnf(s264,plain,
~ spl63_15,
inference(rat,[],[s261,s8]) ).
cnf(s267,plain,
spl63_8,
inference(rat,[],[s4,s8,s36]) ).
cnf(s269,plain,
spl63_13,
inference(rat,[],[s101,s267]) ).
cnf(s271,plain,
spl63_17,
inference(rat,[],[s22,s267]) ).
cnf(s273,plain,
~ spl63_49,
inference(rat,[],[s107,s264,s269]) ).
cnf(s274,plain,
spl63_16,
inference(rat,[],[s12,s264,s269]) ).
cnf(s276,plain,
spl63_29,
inference(rat,[],[s23,s264,s271]) ).
cnf(s278,plain,
spl63_47,
inference(rat,[],[s173,s267,s274]) ).
cnf(s281,plain,
~ spl63_214,
inference(rat,[],[s197,s276,s273,s278]) ).
cnf(s282,plain,
spl63_51,
inference(rat,[],[s39,s276,s273,s278]) ).
cnf(s283,plain,
spl63_50,
inference(rat,[],[s38,s276,s273,s278]) ).
cnf(s289,plain,
spl63_251,
inference(rat,[],[s212,s274,s267,s283]) ).
cnf(s290,plain,
spl63_212,
inference(rat,[],[s192,s274,s267,s283]) ).
cnf(s293,plain,
~ spl63_236,
inference(rat,[],[s233,s282,s281,s290]) ).
cnf(s295,plain,
spl63_216,
inference(rat,[],[s176,s282,s281,s290]) ).
cnf(s296,plain,
spl63_215,
inference(rat,[],[s175,s282,s281,s290]) ).
cnf(s300,plain,
spl63_289,
inference(rat,[],[s248,s289,s296]) ).
cnf(s301,plain,
spl63_239,
inference(rat,[],[s213,s289,s296]) ).
cnf(s307,plain,
spl63_234,
inference(rat,[],[s228,s301]) ).
cnf(s312,plain,
~ spl63_287,
inference(rat,[],[s260,s295,s293,s307]) ).
cnf(s316,plain,
spl63_235,
inference(rat,[],[s198,s293,s295,s307]) ).
cnf(s319,plain,
$false,
inference(rat,[],[s255,s300,s312,s316]) ).
fof(f2171,plain,
$false,
inference(avatar_sat_refutation,[],[s319]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LCL674+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.03/0.31 % Computer : n012.cluster.edu
% 0.03/0.31 % Model : x86_64 x86_64
% 0.03/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.31 % Memory : 8046.5625MB
% 0.03/0.31 % OS : Linux 6.8.0-71-generic
% 0.03/0.31 % CPULimit : 300
% 0.03/0.31 % WCLimit : 300
% 0.03/0.31 % DateTime : Sun Sep 27 16:30:35 UTC 2026
% 0.03/0.31 % CPUTime :
% 0.03/0.31 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.33 Running first-order theorem proving
% 0.07/0.33 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
% 4.46/1.28 % (2570720)Detected formulas, will run a generic FOF schedule.
% 4.46/1.28 % (2570725)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=3791020946:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 4.46/1.28 % (2570728)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=288311313:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 4.46/1.28 % (2570730)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1173807176:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 4.46/1.28 % (2570731)dis-21_1_sil=8000:lcm=predicate:random_seed=1189385157: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)
% 4.46/1.28 % (2570727)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=2027732327:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 4.46/1.28 % (2570726)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=394371571:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 4.46/1.28 % (2570729)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1956695806:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 4.46/1.28 % (2570728)Refutation not found, incomplete strategy
% 4.46/1.28 % (2570728)------------------------------
% 4.46/1.28 % (2570728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/1.28 % (2570728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/1.28 % (2570728)CaDiCaL version: 2.1.3
% 4.46/1.28 % (2570728)Termination reason: Refutation not found, incomplete strategy
% 4.46/1.28 % (2570728)Time elapsed: 0.007 s
% 4.46/1.28 % (2570728)Peak memory usage: 88 MB
% 4.46/1.28 % (2570728)Instructions burned: 23 (million)
% 4.46/1.28 % (2570729)Instruction limit reached!
% 4.46/1.28 % (2570729)------------------------------
% 4.46/1.28 % (2570729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/1.28 % (2570729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/1.28 % (2570729)CaDiCaL version: 2.1.3
% 4.46/1.28 % (2570729)Termination reason: Instruction limit
% 4.46/1.28 % (2570729)Termination phase: Saturation
% 4.46/1.28 % (2570729)Time elapsed: 0.026 s
% 4.46/1.28 % (2570729)Peak memory usage: 88 MB
% 4.46/1.28 % (2570729)Instructions burned: 121 (million)
% 4.46/1.28 % (2570731)Instruction limit reached!
% 4.46/1.28 % (2570731)------------------------------
% 4.46/1.28 % (2570731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/1.28 % (2570731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/1.28 % (2570731)CaDiCaL version: 2.1.3
% 4.46/1.28 % (2570731)Termination reason: Instruction limit
% 4.46/1.28 % (2570731)Termination phase: Saturation
% 4.46/1.28 % (2570731)Time elapsed: 0.028 s
% 4.46/1.28 % (2570731)Peak memory usage: 88 MB
% 4.46/1.28 % (2570731)Instructions burned: 131 (million)
% 4.46/1.28 % (2570730)Instruction limit reached!
% 4.46/1.28 % (2570730)------------------------------
% 4.46/1.28 % (2570730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/1.28 % (2570730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/1.28 % (2570730)CaDiCaL version: 2.1.3
% 4.46/1.28 % (2570730)Termination reason: Instruction limit
% 4.46/1.28 % (2570730)Termination phase: Saturation
% 4.46/1.28 % (2570730)Time elapsed: 0.032 s
% 4.46/1.28 % (2570730)Peak memory usage: 88 MB
% 4.46/1.28 % (2570730)Instructions burned: 144 (million)
% 4.46/1.28 % (2570739)lrs+10_1_sil=8000:sp=occurrence:random_seed=1036398333:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 4.46/1.28 % (2570740)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2038822726:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/157Mi)
% 4.46/1.28 % (2570741)lrs+1011_1_sil=32000:sp=occurrence:random_seed=432429839:i=325:sd=1:ss=axioms:sgt=32_2998 on theBenchmark for (2998ds/325Mi)
% 4.46/1.28 % (2570728)------------------------------
% 4.46/1.28 % (2570728)------------------------------
% 4.46/1.28 % (2570740)Instruction limit reached!
% 4.46/1.28 % (2570740)------------------------------
% 4.46/1.28 % (2570740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/1.28 % (2570740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/1.28 % (2570740)CaDiCaL version: 2.1.3
% 4.46/1.28 % (2570740)Termination reason: Instruction limit
% 4.46/1.28 % (2570740)Termination phase: Saturation
% 4.46/1.28 % (2570740)Time elapsed: 0.043 s
% 4.46/1.28 % (2570740)Peak memory usage: 89 MB
% 4.46/1.28 % (2570740)Instructions burned: 157 (million)
% 4.46/1.28 % (2570739)Instruction limit reached!
% 4.46/1.28 % (2570739)------------------------------
% 4.46/1.28 % (2570739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/1.28 % (2570739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/1.28 % (2570739)CaDiCaL version: 2.1.3
% 4.46/1.28 % (2570739)Termination reason: Instruction limit
% 4.46/1.28 % (2570739)Termination phase: Saturation
% 4.46/1.28 % (2570739)Time elapsed: 0.073 s
% 4.46/1.28 % (2570739)Peak memory usage: 93 MB
% 4.46/1.28 % (2570739)Instructions burned: 287 (million)
% 4.46/1.28 % (2570741)Instruction limit reached!
% 4.46/1.28 % (2570741)------------------------------
% 4.46/1.28 % (2570741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/1.28 % (2570741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/1.28 % (2570741)CaDiCaL version: 2.1.3
% 4.46/1.28 % (2570741)Termination reason: Instruction limit
% 4.46/1.28 % (2570741)Termination phase: Saturation
% 4.46/1.28 % (2570741)Time elapsed: 0.065 s
% 4.46/1.28 % (2570741)Peak memory usage: 88 MB
% 4.46/1.28 % (2570741)Instructions burned: 330 (million)
% 4.46/1.28 % (2570745)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=3078605640:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 4.46/1.28 % (2570746)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=14558119:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 4.46/1.28 % (2570747)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4292068970:i=2350_2996 on theBenchmark for (2996ds/2350Mi)
% 4.46/1.28 % (2570748)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2901654029:cts=off:i=113:fsr=off:ss=included:sgt=4_2996 on theBenchmark for (2996ds/113Mi)
% 4.46/1.28 % (2570745)Instruction limit reached!
% 4.46/1.28 % (2570745)------------------------------
% 4.46/1.28 % (2570745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/1.28 % (2570745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/1.28 % (2570745)CaDiCaL version: 2.1.3
% 4.46/1.28 % (2570745)Termination reason: Instruction limit
% 4.46/1.28 % (2570745)Termination phase: Saturation
% 4.46/1.28 % (2570745)Time elapsed: 0.069 s
% 4.46/1.28 % (2570745)Peak memory usage: 90 MB
% 4.46/1.28 % (2570745)Instructions burned: 248 (million)
% 4.46/1.28 % (2570748)Instruction limit reached!
% 4.46/1.28 % (2570748)------------------------------
% 4.46/1.28 % (2570748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/1.28 % (2570748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/1.28 % (2570748)CaDiCaL version: 2.1.3
% 4.46/1.28 % (2570748)Termination reason: Instruction limit
% 4.46/1.28 % (2570748)Termination phase: Saturation
% 4.46/1.28 % (2570748)Time elapsed: 0.034 s
% 4.46/1.28 % (2570748)Peak memory usage: 91 MB
% 4.46/1.28 % (2570748)Instructions burned: 115 (million)
% 4.46/1.28 % (2570746)Instruction limit reached!
% 4.46/1.28 % (2570746)------------------------------
% 4.46/1.28 % (2570746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/1.28 % (2570746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/1.28 % (2570746)CaDiCaL version: 2.1.3
% 4.46/1.28 % (2570746)Termination reason: Instruction limit
% 4.46/1.28 % (2570746)Termination phase: Saturation
% 4.46/1.28 % (2570746)Time elapsed: 0.086 s
% 4.46/1.28 % (2570746)Peak memory usage: 95 MB
% 4.46/1.28 % (2570746)Instructions burned: 296 (million)
% 4.46/1.28 % (2570726)First to succeed.
% 4.46/1.28 % (2570726)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2570720"
% 4.46/1.28 % (2570753)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=252860448:i=127:av=off:fsr=off:sup=off_2995 on theBenchmark for (2995ds/127Mi)
% 4.46/1.28 % (2570754)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4144215395:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi)
% 4.46/1.28 % (2570755)lrs+10_1_sil=8000:sp=occurrence:random_seed=3513674192:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi)
% 4.46/1.28 % (2570753)Instruction limit reached!
% 4.46/1.28 % (2570753)------------------------------
% 4.46/1.28 % (2570753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/1.28 % (2570753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/1.28 % (2570753)CaDiCaL version: 2.1.3
% 4.46/1.28 % (2570753)Termination reason: Instruction limit
% 4.46/1.28 % (2570753)Termination phase: Saturation
% 4.46/1.28 % (2570753)Time elapsed: 0.035 s
% 4.46/1.28 % (2570753)Peak memory usage: 90 MB
% 4.46/1.28 % (2570753)Instructions burned: 127 (million)
% 4.46/1.28 % (2570754)Instruction limit reached!
% 4.46/1.28 % (2570754)------------------------------
% 4.46/1.28 % (2570754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/1.28 % (2570754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/1.28 % (2570754)CaDiCaL version: 2.1.3
% 4.46/1.28 % (2570754)Termination reason: Instruction limit
% 4.46/1.28 % (2570754)Termination phase: Saturation
% 4.46/1.28 % (2570754)Time elapsed: 0.031 s
% 4.46/1.28 % (2570754)Peak memory usage: 89 MB
% 4.46/1.28 % (2570754)Instructions burned: 115 (million)
% 4.46/1.28 % (2570726)Refutation found. Thanks to Tanya!
% 4.46/1.28 % SZS status Theorem for theBenchmark
% 4.46/1.28 % SZS output start Proof for theBenchmark
% See solution above
% 5.36/1.37 % (2570726)------------------------------
% 5.36/1.37 % (2570726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.36/1.37 % (2570726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.36/1.37 % (2570726)CaDiCaL version: 2.1.3
% 5.36/1.37 % (2570726)Termination reason: Refutation
% 5.36/1.37 % (2570726)Time elapsed: 0.438 s
% 5.36/1.37 % (2570726)Peak memory usage: 129 MB
% 5.36/1.37 % (2570726)Instructions burned: 1152 (million)
% 5.36/1.37 % (2570726)------------------------------
% 5.36/1.37 % (2570726)------------------------------
% 5.36/1.37 % (2570720)Success in time 0.745 s
% 5.36/1.37 % Vampire exiting
%------------------------------------------------------------------------------