%------------------------------------------------------------------------------
% File : Vampire-SAT---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/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:00:00 PM UTC 2026
% Result : Theorem 5.83s 1.35s
% Output : Refutation 5.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 47
% Syntax : Number of formulae : 267 ( 27 unt; 44 def)
% Number of atoms : 3767 ( 0 equ)
% Maximal formula atoms : 331 ( 14 avg)
% Number of connectives : 6121 (2621 ~;1999 |;1488 &)
% ( 12 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 66 ( 8 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 79 ( 78 usr; 13 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 1 con; 0-1 aty)
% Number of variables : 667 ( 0 sgn 545 !; 122 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : r1(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity) ).
fof(f2,axiom,
! [X0,X1,X2] :
( ( r1(X0,X1)
& r1(X1,X2) )
=> r1(X0,X2) ),
file('/export/starexec/sandbox/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/sandbox/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] :
( ~ r1(X0,X1)
| p7(X1) )
| ~ ( ! [X2] :
( ~ r1(X0,X2)
| ( ( ( ~ ! [X3] :
( ~ r1(X2,X3)
| ~ ( ~ p16(X3)
& p115(X3) ) )
& ~ ! [X4] :
( ~ r1(X2,X4)
| ~ ( p16(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) )
& ( 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(pure_predicate_removal,[],[f6]) ).
fof(f8,plain,
! [X0,X1,X2] :
( r1(X0,X2)
| ~ r1(X0,X1)
| ~ r1(X1,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f9,plain,
! [X0,X1,X2] :
( r1(X0,X2)
| ~ r1(X0,X1)
| ~ r1(X1,X2) ),
inference(flattening,[],[f8]) ).
fof(f10,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| p7(X1) )
& ! [X2] :
( ~ r1(X0,X2)
| ( ( ( ? [X3] :
( r1(X2,X3)
& ~ p16(X3)
& p115(X3) )
& ? [X4] :
( r1(X2,X4)
& p16(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) )
& ( 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,[],[f7]) ).
fof(f11,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| p7(X1) )
& ! [X2] :
( ~ r1(X0,X2)
| ( ( ( ? [X3] :
( r1(X2,X3)
& ~ p16(X3)
& p115(X3) )
& ? [X4] :
( r1(X2,X4)
& p16(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) )
& ( 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,[],[f10]) ).
fof(f12,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(f13,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(f14,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(f15,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(f16,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(f17,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(f18,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(f19,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(f20,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(f21,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(f22,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(f23,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(f24,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(f25,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(f26,definition,
! [X2] :
( ( ? [X3] :
( r1(X2,X3)
& ~ p16(X3)
& p115(X3) )
& ? [X4] :
( r1(X2,X4)
& p16(X4)
& p115(X4) ) )
| p115(X2)
| ~ p114(X2)
| ~ sP14(X2) ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f27,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(f28,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(f29,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(f30,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(f31,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(f32,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(f33,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(f34,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(f35,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(f36,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(f37,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(f38,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(f39,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(f40,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(f41,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(f42,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(f43,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)
& ( 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(f44,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| p7(X1) )
& ! [X2] :
( ~ r1(X0,X2)
| sP31(X2) )
& ~ p101(X0)
& p100(X0) ),
inference(definition_folding,[],[f11,f43,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]) ).
fof(f45,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)
& ( 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,[],[f43]) ).
fof(f46,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)
& ( 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,[],[f45]) ).
fof(f106,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,[],[f17]) ).
fof(f107,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,[],[f106]) ).
fof(f108,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))],[f107]) ).
fof(f109,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,[],[f16]) ).
fof(f110,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,[],[f109]) ).
fof(f111,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))],[f110]) ).
fof(f112,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,[],[f15]) ).
fof(f113,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,[],[f112]) ).
fof(f114,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))],[f113]) ).
fof(f115,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,[],[f14]) ).
fof(f116,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,[],[f115]) ).
fof(f117,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))],[f116]) ).
fof(f118,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,[],[f13]) ).
fof(f119,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,[],[f118]) ).
fof(f120,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))],[f119]) ).
fof(f121,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,[],[f12]) ).
fof(f122,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,[],[f121]) ).
fof(f123,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))],[f122]) ).
fof(f124,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)],[f44]) ).
fof(f125,plain,
! [X0] : r1(X0,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f126,plain,
! [X2,X0,X1] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| r1(X0,X2) ),
inference(cnf_transformation,[],[f9]) ).
fof(f158,plain,
! [X0] :
( ~ sP31(X0)
| sP0(X0) ),
inference(cnf_transformation,[],[f46]) ).
fof(f159,plain,
! [X0] :
( ~ sP31(X0)
| sP1(X0) ),
inference(cnf_transformation,[],[f46]) ).
fof(f160,plain,
! [X0] :
( ~ sP31(X0)
| sP2(X0) ),
inference(cnf_transformation,[],[f46]) ).
fof(f161,plain,
! [X0] :
( ~ sP31(X0)
| sP3(X0) ),
inference(cnf_transformation,[],[f46]) ).
fof(f162,plain,
! [X0] :
( ~ sP31(X0)
| sP4(X0) ),
inference(cnf_transformation,[],[f46]) ).
fof(f163,plain,
! [X0] :
( ~ sP31(X0)
| sP5(X0) ),
inference(cnf_transformation,[],[f46]) ).
fof(f281,plain,
! [X0] :
( ~ p7(sK50(X0))
| p106(X0)
| ~ p105(X0)
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f108]) ).
fof(f282,plain,
! [X0] :
( r1(X0,sK50(X0))
| p106(X0)
| ~ p105(X0)
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f108]) ).
fof(f283,plain,
! [X0] :
( ~ sP4(X0)
| p105(X0)
| ~ p104(X0)
| p105(sK53(X0)) ),
inference(cnf_transformation,[],[f111]) ).
fof(f284,plain,
! [X0] :
( ~ p106(sK53(X0))
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f111]) ).
fof(f286,plain,
! [X0] :
( r1(X0,sK53(X0))
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f111]) ).
fof(f291,plain,
! [X0] :
( ~ sP3(X0)
| p104(X0)
| ~ p103(X0)
| p104(sK55(X0)) ),
inference(cnf_transformation,[],[f114]) ).
fof(f292,plain,
! [X0] :
( ~ p105(sK55(X0))
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f114]) ).
fof(f294,plain,
! [X0] :
( r1(X0,sK55(X0))
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f114]) ).
fof(f299,plain,
! [X0] :
( ~ sP2(X0)
| p103(X0)
| ~ p102(X0)
| p103(sK57(X0)) ),
inference(cnf_transformation,[],[f117]) ).
fof(f300,plain,
! [X0] :
( ~ p104(sK57(X0))
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f117]) ).
fof(f302,plain,
! [X0] :
( r1(X0,sK57(X0))
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f117]) ).
fof(f307,plain,
! [X0] :
( ~ sP1(X0)
| p102(X0)
| ~ p101(X0)
| p102(sK59(X0)) ),
inference(cnf_transformation,[],[f120]) ).
fof(f308,plain,
! [X0] :
( ~ p103(sK59(X0))
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f120]) ).
fof(f310,plain,
! [X0] :
( r1(X0,sK59(X0))
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f120]) ).
fof(f319,plain,
! [X0] :
( ~ sP0(X0)
| p101(X0)
| ~ p100(X0)
| p101(sK60(X0)) ),
inference(cnf_transformation,[],[f123]) ).
fof(f320,plain,
! [X0] :
( ~ p102(sK60(X0))
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f123]) ).
fof(f322,plain,
! [X0] :
( r1(X0,sK60(X0))
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f123]) ).
fof(f323,plain,
p100(sK62),
inference(cnf_transformation,[],[f124]) ).
fof(f324,plain,
~ p101(sK62),
inference(cnf_transformation,[],[f124]) ).
fof(f325,plain,
! [X2] :
( ~ r1(sK62,X2)
| sP31(X2) ),
inference(cnf_transformation,[],[f124]) ).
fof(f326,plain,
! [X1] :
( ~ r1(sK62,X1)
| p7(X1) ),
inference(cnf_transformation,[],[f124]) ).
fof(f328,plain,
sP31(sK62),
inference(resolution,[],[f125,f325]) ).
fof(f345,plain,
sP0(sK62),
inference(resolution,[],[f158,f328]) ).
fof(f437,plain,
( p101(sK62)
| ~ p100(sK62)
| p101(sK60(sK62)) ),
inference(resolution,[],[f319,f345]) ).
fof(f438,plain,
( ~ p100(sK62)
| p101(sK60(sK62)) ),
inference(forward_subsumption_resolution,[],[f437,f324]) ).
fof(f439,plain,
p101(sK60(sK62)),
inference(forward_subsumption_resolution,[],[f438,f323]) ).
fof(f499,plain,
! [X0,X1] :
( r1(X1,sK50(X0))
| ~ p105(X0)
| ~ sP5(X0)
| ~ r1(X1,X0)
| p106(X0) ),
inference(resolution,[],[f282,f126]) ).
fof(f503,plain,
! [X0,X1] :
( r1(X1,sK53(X0))
| ~ p104(X0)
| ~ sP4(X0)
| ~ r1(X1,X0)
| p105(X0) ),
inference(resolution,[],[f286,f126]) ).
fof(f509,plain,
! [X0,X1] :
( r1(X1,sK55(X0))
| ~ p103(X0)
| ~ sP3(X0)
| ~ r1(X1,X0)
| p104(X0) ),
inference(resolution,[],[f294,f126]) ).
fof(f515,plain,
! [X0,X1] :
( r1(X1,sK57(X0))
| ~ p102(X0)
| ~ sP2(X0)
| ~ r1(X1,X0)
| p103(X0) ),
inference(resolution,[],[f302,f126]) ).
fof(f521,plain,
! [X0,X1] :
( r1(X1,sK59(X0))
| ~ p101(X0)
| ~ sP1(X0)
| ~ r1(X1,X0)
| p102(X0) ),
inference(resolution,[],[f310,f126]) ).
fof(f535,plain,
( p101(sK62)
| ~ p100(sK62)
| ~ sP0(sK62)
| sP31(sK60(sK62)) ),
inference(resolution,[],[f322,f325]) ).
fof(f536,plain,
! [X0,X1] :
( r1(X1,sK60(X0))
| ~ p100(X0)
| ~ sP0(X0)
| ~ r1(X1,X0)
| p101(X0) ),
inference(resolution,[],[f322,f126]) ).
fof(f537,plain,
( ~ p100(sK62)
| ~ sP0(sK62)
| sP31(sK60(sK62)) ),
inference(forward_subsumption_resolution,[],[f535,f324]) ).
fof(f539,plain,
( ~ sP0(sK62)
| sP31(sK60(sK62)) ),
inference(forward_subsumption_resolution,[],[f537,f323]) ).
fof(f541,plain,
sP31(sK60(sK62)),
inference(forward_subsumption_resolution,[],[f539,f345]) ).
fof(f755,plain,
sP1(sK60(sK62)),
inference(resolution,[],[f541,f159]) ).
fof(f834,definition,
( spl63_28
<=> p102(sK60(sK62)) ),
introduced(definition,[new_symbols(definition,[spl63_28])],[avatar_definition]) ).
fof(f835,plain,
( ~ p102(sK60(sK62))
| spl63_28 ),
inference(avatar_component_clause,[],[f834]) ).
fof(f836,plain,
( p102(sK60(sK62))
| ~ spl63_28 ),
inference(avatar_component_clause,[],[f834]) ).
fof(f2644,plain,
! [X0] :
( ~ p105(X0)
| ~ sP5(X0)
| ~ r1(sK62,X0)
| p106(X0)
| p7(sK50(X0)) ),
inference(resolution,[],[f499,f326]) ).
fof(f2680,plain,
! [X0] :
( ~ r1(sK62,X0)
| ~ sP5(X0)
| ~ p105(X0)
| p106(X0) ),
inference(forward_subsumption_resolution,[],[f2644,f281]) ).
fof(f2684,plain,
! [X0] :
( ~ r1(sK62,X0)
| ~ sP4(X0)
| ~ p104(X0)
| p105(X0)
| sP31(sK53(X0)) ),
inference(resolution,[],[f503,f325]) ).
fof(f2759,plain,
! [X0] :
( ~ r1(sK62,X0)
| ~ sP3(X0)
| ~ p103(X0)
| p104(X0)
| sP31(sK55(X0)) ),
inference(resolution,[],[f509,f325]) ).
fof(f2834,plain,
! [X0] :
( ~ r1(sK62,X0)
| ~ sP2(X0)
| ~ p102(X0)
| p103(X0)
| sP31(sK57(X0)) ),
inference(resolution,[],[f515,f325]) ).
fof(f2909,plain,
! [X0] :
( ~ r1(sK62,X0)
| ~ sP1(X0)
| ~ p101(X0)
| p102(X0)
| sP31(sK59(X0)) ),
inference(resolution,[],[f521,f325]) ).
fof(f3063,plain,
( p102(sK60(sK62))
| ~ p101(sK60(sK62))
| p102(sK59(sK60(sK62))) ),
inference(resolution,[],[f755,f307]) ).
fof(f3064,plain,
( p102(sK60(sK62))
| p102(sK59(sK60(sK62))) ),
inference(forward_subsumption_resolution,[],[f3063,f439]) ).
fof(f3068,definition,
( spl63_32
<=> p102(sK59(sK60(sK62))) ),
introduced(definition,[new_symbols(definition,[spl63_32])],[avatar_definition]) ).
fof(f3070,plain,
( p102(sK59(sK60(sK62)))
| ~ spl63_32 ),
inference(avatar_component_clause,[],[f3068]) ).
fof(f3071,plain,
( spl63_32
| spl63_28 ),
inference(avatar_split_clause,[],[f3064,f834,f3068]) ).
fof(f3126,plain,
( p101(sK62)
| ~ p100(sK62)
| ~ sP0(sK62)
| ~ spl63_28 ),
inference(resolution,[],[f836,f320]) ).
fof(f3127,plain,
( ~ p100(sK62)
| ~ sP0(sK62)
| ~ spl63_28 ),
inference(forward_subsumption_resolution,[],[f3126,f324]) ).
fof(f3128,plain,
( ~ sP0(sK62)
| ~ spl63_28 ),
inference(forward_subsumption_resolution,[],[f3127,f323]) ).
fof(f3129,plain,
( $false
| ~ spl63_28 ),
inference(forward_subsumption_resolution,[],[f3128,f345]) ).
fof(f3130,plain,
~ spl63_28,
inference(avatar_contradiction_clause,[],[f3129]) ).
fof(f3175,plain,
! [X0] :
( ~ sP5(sK53(X0))
| ~ p105(sK53(X0))
| p106(sK53(X0))
| ~ p104(X0)
| ~ sP4(X0)
| ~ r1(sK62,X0)
| p105(X0) ),
inference(resolution,[],[f2680,f503]) ).
fof(f3192,plain,
! [X0] :
( ~ sP5(sK53(X0))
| ~ p105(sK53(X0))
| ~ p104(X0)
| ~ sP4(X0)
| ~ r1(sK62,X0)
| p105(X0) ),
inference(forward_subsumption_resolution,[],[f3175,f284]) ).
fof(f3196,plain,
! [X0] :
( ~ sP5(sK53(X0))
| ~ p104(X0)
| ~ sP4(X0)
| ~ r1(sK62,X0)
| p105(X0) ),
inference(forward_subsumption_resolution,[],[f3192,f283]) ).
fof(f5890,plain,
! [X0] :
( ~ sP4(sK55(X0))
| ~ p104(sK55(X0))
| p105(sK55(X0))
| sP31(sK53(sK55(X0)))
| ~ p103(X0)
| ~ sP3(X0)
| ~ r1(sK62,X0)
| p104(X0) ),
inference(resolution,[],[f2684,f509]) ).
fof(f5903,plain,
! [X0] :
( ~ sP4(sK55(X0))
| ~ p104(sK55(X0))
| sP31(sK53(sK55(X0)))
| ~ p103(X0)
| ~ sP3(X0)
| ~ r1(sK62,X0)
| p104(X0) ),
inference(forward_subsumption_resolution,[],[f5890,f292]) ).
fof(f5907,plain,
! [X0] :
( ~ sP4(sK55(X0))
| sP31(sK53(sK55(X0)))
| ~ p103(X0)
| ~ sP3(X0)
| ~ r1(sK62,X0)
| p104(X0) ),
inference(forward_subsumption_resolution,[],[f5903,f291]) ).
fof(f6166,plain,
! [X0] :
( ~ sP3(sK57(X0))
| ~ p103(sK57(X0))
| p104(sK57(X0))
| sP31(sK55(sK57(X0)))
| ~ p102(X0)
| ~ sP2(X0)
| ~ r1(sK62,X0)
| p103(X0) ),
inference(resolution,[],[f2759,f515]) ).
fof(f6175,plain,
! [X0] :
( ~ sP3(sK57(X0))
| ~ p103(sK57(X0))
| sP31(sK55(sK57(X0)))
| ~ p102(X0)
| ~ sP2(X0)
| ~ r1(sK62,X0)
| p103(X0) ),
inference(forward_subsumption_resolution,[],[f6166,f300]) ).
fof(f6179,plain,
! [X0] :
( ~ sP3(sK57(X0))
| sP31(sK55(sK57(X0)))
| ~ p102(X0)
| ~ sP2(X0)
| ~ r1(sK62,X0)
| p103(X0) ),
inference(forward_subsumption_resolution,[],[f6175,f299]) ).
fof(f6439,plain,
! [X0] :
( ~ sP2(sK59(X0))
| ~ p102(sK59(X0))
| p103(sK59(X0))
| sP31(sK57(sK59(X0)))
| ~ p101(X0)
| ~ sP1(X0)
| ~ r1(sK62,X0)
| p102(X0) ),
inference(resolution,[],[f2834,f521]) ).
fof(f6444,plain,
! [X0] :
( ~ sP2(sK59(X0))
| p103(sK59(X0))
| sP31(sK57(sK59(X0)))
| ~ p101(X0)
| ~ sP1(X0)
| ~ r1(sK62,X0)
| p102(X0) ),
inference(forward_subsumption_resolution,[],[f6439,f307]) ).
fof(f6446,plain,
! [X0] :
( ~ sP2(sK59(X0))
| sP31(sK57(sK59(X0)))
| ~ p101(X0)
| ~ sP1(X0)
| ~ r1(sK62,X0)
| p102(X0) ),
inference(forward_subsumption_resolution,[],[f6444,f308]) ).
fof(f6712,plain,
( ~ sP1(sK60(sK62))
| ~ p101(sK60(sK62))
| p102(sK60(sK62))
| sP31(sK59(sK60(sK62)))
| p101(sK62)
| ~ p100(sK62)
| ~ sP0(sK62) ),
inference(resolution,[],[f2909,f322]) ).
fof(f6719,plain,
( ~ sP1(sK60(sK62))
| p102(sK60(sK62))
| sP31(sK59(sK60(sK62)))
| p101(sK62)
| ~ p100(sK62)
| ~ sP0(sK62) ),
inference(forward_subsumption_resolution,[],[f6712,f319]) ).
fof(f6723,plain,
( ~ sP1(sK60(sK62))
| sP31(sK59(sK60(sK62)))
| p101(sK62)
| ~ p100(sK62)
| ~ sP0(sK62) ),
inference(forward_subsumption_resolution,[],[f6719,f320]) ).
fof(f6725,plain,
( sP31(sK59(sK60(sK62)))
| p101(sK62)
| ~ p100(sK62)
| ~ sP0(sK62) ),
inference(forward_subsumption_resolution,[],[f6723,f755]) ).
fof(f6727,plain,
( sP31(sK59(sK60(sK62)))
| ~ p100(sK62)
| ~ sP0(sK62) ),
inference(forward_subsumption_resolution,[],[f6725,f324]) ).
fof(f6729,plain,
( sP31(sK59(sK60(sK62)))
| ~ sP0(sK62) ),
inference(forward_subsumption_resolution,[],[f6727,f323]) ).
fof(f6731,plain,
sP31(sK59(sK60(sK62))),
inference(forward_subsumption_resolution,[],[f6729,f345]) ).
fof(f6886,plain,
sP2(sK59(sK60(sK62))),
inference(resolution,[],[f6731,f160]) ).
fof(f6959,definition,
( spl63_64
<=> p103(sK59(sK60(sK62))) ),
introduced(definition,[new_symbols(definition,[spl63_64])],[avatar_definition]) ).
fof(f6960,plain,
( ~ p103(sK59(sK60(sK62)))
| spl63_64 ),
inference(avatar_component_clause,[],[f6959]) ).
fof(f6961,plain,
( p103(sK59(sK60(sK62)))
| ~ spl63_64 ),
inference(avatar_component_clause,[],[f6959]) ).
fof(f7061,plain,
( p103(sK59(sK60(sK62)))
| ~ p102(sK59(sK60(sK62)))
| p103(sK57(sK59(sK60(sK62)))) ),
inference(resolution,[],[f6886,f299]) ).
fof(f7062,plain,
( p103(sK59(sK60(sK62)))
| p103(sK57(sK59(sK60(sK62))))
| ~ spl63_32 ),
inference(forward_subsumption_resolution,[],[f7061,f3070]) ).
fof(f7066,definition,
( spl63_70
<=> p103(sK57(sK59(sK60(sK62)))) ),
introduced(definition,[new_symbols(definition,[spl63_70])],[avatar_definition]) ).
fof(f7068,plain,
( p103(sK57(sK59(sK60(sK62))))
| ~ spl63_70 ),
inference(avatar_component_clause,[],[f7066]) ).
fof(f7069,plain,
( spl63_70
| spl63_64
| ~ spl63_32 ),
inference(avatar_split_clause,[],[f7062,f3068,f6959,f7066]) ).
fof(f7121,plain,
( p102(sK60(sK62))
| ~ p101(sK60(sK62))
| ~ sP1(sK60(sK62))
| ~ spl63_64 ),
inference(resolution,[],[f6961,f308]) ).
fof(f7122,plain,
( ~ p101(sK60(sK62))
| ~ sP1(sK60(sK62))
| spl63_28
| ~ spl63_64 ),
inference(forward_subsumption_resolution,[],[f7121,f835]) ).
fof(f7123,plain,
( ~ sP1(sK60(sK62))
| spl63_28
| ~ spl63_64 ),
inference(forward_subsumption_resolution,[],[f7122,f439]) ).
fof(f7124,plain,
( $false
| spl63_28
| ~ spl63_64 ),
inference(forward_subsumption_resolution,[],[f7123,f755]) ).
fof(f7125,plain,
( spl63_28
| ~ spl63_64 ),
inference(avatar_contradiction_clause,[],[f7124]) ).
fof(f7944,definition,
( spl63_111
<=> r1(sK62,sK60(sK62)) ),
introduced(definition,[new_symbols(definition,[spl63_111])],[avatar_definition]) ).
fof(f7945,plain,
( r1(sK62,sK60(sK62))
| ~ spl63_111 ),
inference(avatar_component_clause,[],[f7944]) ).
fof(f7946,plain,
( ~ r1(sK62,sK60(sK62))
| spl63_111 ),
inference(avatar_component_clause,[],[f7944]) ).
fof(f7962,plain,
( ~ p100(sK62)
| ~ sP0(sK62)
| ~ r1(sK62,sK62)
| p101(sK62)
| spl63_111 ),
inference(resolution,[],[f7946,f536]) ).
fof(f7963,plain,
( ~ sP0(sK62)
| ~ r1(sK62,sK62)
| p101(sK62)
| spl63_111 ),
inference(forward_subsumption_resolution,[],[f7962,f323]) ).
fof(f7965,plain,
( ~ r1(sK62,sK62)
| p101(sK62)
| spl63_111 ),
inference(forward_subsumption_resolution,[],[f7963,f345]) ).
fof(f7967,plain,
( p101(sK62)
| spl63_111 ),
inference(forward_subsumption_resolution,[],[f7965,f125]) ).
fof(f7970,plain,
( $false
| spl63_111 ),
inference(forward_subsumption_resolution,[],[f7967,f324]) ).
fof(f7971,plain,
spl63_111,
inference(avatar_contradiction_clause,[],[f7970]) ).
fof(f8519,plain,
( sP31(sK57(sK59(sK60(sK62))))
| ~ p101(sK60(sK62))
| ~ sP1(sK60(sK62))
| ~ r1(sK62,sK60(sK62))
| p102(sK60(sK62)) ),
inference(resolution,[],[f6446,f6886]) ).
fof(f8520,plain,
( sP31(sK57(sK59(sK60(sK62))))
| ~ sP1(sK60(sK62))
| ~ r1(sK62,sK60(sK62))
| p102(sK60(sK62)) ),
inference(forward_subsumption_resolution,[],[f8519,f439]) ).
fof(f8522,plain,
( sP31(sK57(sK59(sK60(sK62))))
| ~ r1(sK62,sK60(sK62))
| p102(sK60(sK62)) ),
inference(forward_subsumption_resolution,[],[f8520,f755]) ).
fof(f8524,plain,
( sP31(sK57(sK59(sK60(sK62))))
| p102(sK60(sK62))
| ~ spl63_111 ),
inference(forward_subsumption_resolution,[],[f8522,f7945]) ).
fof(f8526,plain,
( sP31(sK57(sK59(sK60(sK62))))
| spl63_28
| ~ spl63_111 ),
inference(forward_subsumption_resolution,[],[f8524,f835]) ).
fof(f8562,plain,
( sP3(sK57(sK59(sK60(sK62))))
| spl63_28
| ~ spl63_111 ),
inference(resolution,[],[f8526,f161]) ).
fof(f8629,definition,
( spl63_126
<=> p104(sK57(sK59(sK60(sK62)))) ),
introduced(definition,[new_symbols(definition,[spl63_126])],[avatar_definition]) ).
fof(f8630,plain,
( ~ p104(sK57(sK59(sK60(sK62))))
| spl63_126 ),
inference(avatar_component_clause,[],[f8629]) ).
fof(f8631,plain,
( p104(sK57(sK59(sK60(sK62))))
| ~ spl63_126 ),
inference(avatar_component_clause,[],[f8629]) ).
fof(f8781,plain,
( sP31(sK55(sK57(sK59(sK60(sK62)))))
| ~ p102(sK59(sK60(sK62)))
| ~ sP2(sK59(sK60(sK62)))
| ~ r1(sK62,sK59(sK60(sK62)))
| p103(sK59(sK60(sK62)))
| spl63_28
| ~ spl63_111 ),
inference(resolution,[],[f8562,f6179]) ).
fof(f8785,plain,
( p104(sK57(sK59(sK60(sK62))))
| ~ p103(sK57(sK59(sK60(sK62))))
| p104(sK55(sK57(sK59(sK60(sK62)))))
| spl63_28
| ~ spl63_111 ),
inference(resolution,[],[f8562,f291]) ).
fof(f8786,plain,
( p104(sK57(sK59(sK60(sK62))))
| p104(sK55(sK57(sK59(sK60(sK62)))))
| spl63_28
| ~ spl63_70
| ~ spl63_111 ),
inference(forward_subsumption_resolution,[],[f8785,f7068]) ).
fof(f8790,plain,
( sP31(sK55(sK57(sK59(sK60(sK62)))))
| ~ sP2(sK59(sK60(sK62)))
| ~ r1(sK62,sK59(sK60(sK62)))
| p103(sK59(sK60(sK62)))
| spl63_28
| ~ spl63_32
| ~ spl63_111 ),
inference(forward_subsumption_resolution,[],[f8781,f3070]) ).
fof(f8794,definition,
( spl63_145
<=> p104(sK55(sK57(sK59(sK60(sK62))))) ),
introduced(definition,[new_symbols(definition,[spl63_145])],[avatar_definition]) ).
fof(f8796,plain,
( p104(sK55(sK57(sK59(sK60(sK62)))))
| ~ spl63_145 ),
inference(avatar_component_clause,[],[f8794]) ).
fof(f8797,plain,
( spl63_145
| spl63_126
| spl63_28
| ~ spl63_70
| ~ spl63_111 ),
inference(avatar_split_clause,[],[f8786,f7944,f7066,f834,f8629,f8794]) ).
fof(f8809,plain,
( sP31(sK55(sK57(sK59(sK60(sK62)))))
| ~ r1(sK62,sK59(sK60(sK62)))
| p103(sK59(sK60(sK62)))
| spl63_28
| ~ spl63_32
| ~ spl63_111 ),
inference(forward_subsumption_resolution,[],[f8790,f6886]) ).
fof(f8813,plain,
( sP31(sK55(sK57(sK59(sK60(sK62)))))
| ~ r1(sK62,sK59(sK60(sK62)))
| spl63_28
| ~ spl63_32
| spl63_64
| ~ spl63_111 ),
inference(forward_subsumption_resolution,[],[f8809,f6960]) ).
fof(f8817,definition,
( spl63_148
<=> r1(sK62,sK59(sK60(sK62))) ),
introduced(definition,[new_symbols(definition,[spl63_148])],[avatar_definition]) ).
fof(f8818,plain,
( r1(sK62,sK59(sK60(sK62)))
| ~ spl63_148 ),
inference(avatar_component_clause,[],[f8817]) ).
fof(f8819,plain,
( ~ r1(sK62,sK59(sK60(sK62)))
| spl63_148 ),
inference(avatar_component_clause,[],[f8817]) ).
fof(f8826,definition,
( spl63_150
<=> sP31(sK55(sK57(sK59(sK60(sK62))))) ),
introduced(definition,[new_symbols(definition,[spl63_150])],[avatar_definition]) ).
fof(f8828,plain,
( sP31(sK55(sK57(sK59(sK60(sK62)))))
| ~ spl63_150 ),
inference(avatar_component_clause,[],[f8826]) ).
fof(f8829,plain,
( ~ spl63_148
| spl63_150
| spl63_28
| ~ spl63_32
| spl63_64
| ~ spl63_111 ),
inference(avatar_split_clause,[],[f8813,f7944,f6959,f3068,f834,f8826,f8817]) ).
fof(f8878,plain,
( p103(sK59(sK60(sK62)))
| ~ p102(sK59(sK60(sK62)))
| ~ sP2(sK59(sK60(sK62)))
| ~ spl63_126 ),
inference(resolution,[],[f8631,f300]) ).
fof(f8879,plain,
( ~ p102(sK59(sK60(sK62)))
| ~ sP2(sK59(sK60(sK62)))
| spl63_64
| ~ spl63_126 ),
inference(forward_subsumption_resolution,[],[f8878,f6960]) ).
fof(f8880,plain,
( ~ sP2(sK59(sK60(sK62)))
| ~ spl63_32
| spl63_64
| ~ spl63_126 ),
inference(forward_subsumption_resolution,[],[f8879,f3070]) ).
fof(f8881,plain,
( $false
| ~ spl63_32
| spl63_64
| ~ spl63_126 ),
inference(forward_subsumption_resolution,[],[f8880,f6886]) ).
fof(f8882,plain,
( ~ spl63_32
| spl63_64
| ~ spl63_126 ),
inference(avatar_contradiction_clause,[],[f8881]) ).
fof(f9008,plain,
( ~ p101(sK60(sK62))
| ~ sP1(sK60(sK62))
| ~ r1(sK62,sK60(sK62))
| p102(sK60(sK62))
| spl63_148 ),
inference(resolution,[],[f8819,f521]) ).
fof(f9009,plain,
( ~ sP1(sK60(sK62))
| ~ r1(sK62,sK60(sK62))
| p102(sK60(sK62))
| spl63_148 ),
inference(forward_subsumption_resolution,[],[f9008,f439]) ).
fof(f9010,plain,
( ~ r1(sK62,sK60(sK62))
| p102(sK60(sK62))
| spl63_148 ),
inference(forward_subsumption_resolution,[],[f9009,f755]) ).
fof(f9011,plain,
( p102(sK60(sK62))
| ~ spl63_111
| spl63_148 ),
inference(forward_subsumption_resolution,[],[f9010,f7945]) ).
fof(f9012,plain,
( $false
| spl63_28
| ~ spl63_111
| spl63_148 ),
inference(forward_subsumption_resolution,[],[f9011,f835]) ).
fof(f9013,plain,
( spl63_28
| ~ spl63_111
| spl63_148 ),
inference(avatar_contradiction_clause,[],[f9012]) ).
fof(f9711,plain,
( sP4(sK55(sK57(sK59(sK60(sK62)))))
| ~ spl63_150 ),
inference(resolution,[],[f8828,f162]) ).
fof(f9772,definition,
( spl63_207
<=> p105(sK55(sK57(sK59(sK60(sK62))))) ),
introduced(definition,[new_symbols(definition,[spl63_207])],[avatar_definition]) ).
fof(f9773,plain,
( ~ p105(sK55(sK57(sK59(sK60(sK62)))))
| spl63_207 ),
inference(avatar_component_clause,[],[f9772]) ).
fof(f9774,plain,
( p105(sK55(sK57(sK59(sK60(sK62)))))
| ~ spl63_207 ),
inference(avatar_component_clause,[],[f9772]) ).
fof(f10174,plain,
( sP31(sK53(sK55(sK57(sK59(sK60(sK62))))))
| ~ p103(sK57(sK59(sK60(sK62))))
| ~ sP3(sK57(sK59(sK60(sK62))))
| ~ r1(sK62,sK57(sK59(sK60(sK62))))
| p104(sK57(sK59(sK60(sK62))))
| ~ spl63_150 ),
inference(resolution,[],[f9711,f5907]) ).
fof(f10183,plain,
( sP31(sK53(sK55(sK57(sK59(sK60(sK62))))))
| ~ sP3(sK57(sK59(sK60(sK62))))
| ~ r1(sK62,sK57(sK59(sK60(sK62))))
| p104(sK57(sK59(sK60(sK62))))
| ~ spl63_70
| ~ spl63_150 ),
inference(forward_subsumption_resolution,[],[f10174,f7068]) ).
fof(f10202,plain,
( sP31(sK53(sK55(sK57(sK59(sK60(sK62))))))
| ~ r1(sK62,sK57(sK59(sK60(sK62))))
| p104(sK57(sK59(sK60(sK62))))
| spl63_28
| ~ spl63_70
| ~ spl63_111
| ~ spl63_150 ),
inference(forward_subsumption_resolution,[],[f10183,f8562]) ).
fof(f10206,plain,
( sP31(sK53(sK55(sK57(sK59(sK60(sK62))))))
| ~ r1(sK62,sK57(sK59(sK60(sK62))))
| spl63_28
| ~ spl63_70
| ~ spl63_111
| spl63_126
| ~ spl63_150 ),
inference(forward_subsumption_resolution,[],[f10202,f8630]) ).
fof(f10210,definition,
( spl63_260
<=> r1(sK62,sK57(sK59(sK60(sK62)))) ),
introduced(definition,[new_symbols(definition,[spl63_260])],[avatar_definition]) ).
fof(f10211,plain,
( r1(sK62,sK57(sK59(sK60(sK62))))
| ~ spl63_260 ),
inference(avatar_component_clause,[],[f10210]) ).
fof(f10212,plain,
( ~ r1(sK62,sK57(sK59(sK60(sK62))))
| spl63_260 ),
inference(avatar_component_clause,[],[f10210]) ).
fof(f10219,definition,
( spl63_262
<=> sP31(sK53(sK55(sK57(sK59(sK60(sK62)))))) ),
introduced(definition,[new_symbols(definition,[spl63_262])],[avatar_definition]) ).
fof(f10221,plain,
( sP31(sK53(sK55(sK57(sK59(sK60(sK62))))))
| ~ spl63_262 ),
inference(avatar_component_clause,[],[f10219]) ).
fof(f10222,plain,
( ~ spl63_260
| spl63_262
| spl63_28
| ~ spl63_70
| ~ spl63_111
| spl63_126
| ~ spl63_150 ),
inference(avatar_split_clause,[],[f10206,f8826,f8629,f7944,f7066,f834,f10219,f10210]) ).
fof(f10266,plain,
( p104(sK57(sK59(sK60(sK62))))
| ~ p103(sK57(sK59(sK60(sK62))))
| ~ sP3(sK57(sK59(sK60(sK62))))
| ~ spl63_207 ),
inference(resolution,[],[f9774,f292]) ).
fof(f10267,plain,
( ~ p103(sK57(sK59(sK60(sK62))))
| ~ sP3(sK57(sK59(sK60(sK62))))
| spl63_126
| ~ spl63_207 ),
inference(forward_subsumption_resolution,[],[f10266,f8630]) ).
fof(f10268,plain,
( ~ sP3(sK57(sK59(sK60(sK62))))
| ~ spl63_70
| spl63_126
| ~ spl63_207 ),
inference(forward_subsumption_resolution,[],[f10267,f7068]) ).
fof(f10269,plain,
( $false
| spl63_28
| ~ spl63_70
| ~ spl63_111
| spl63_126
| ~ spl63_207 ),
inference(forward_subsumption_resolution,[],[f10268,f8562]) ).
fof(f10270,plain,
( spl63_28
| ~ spl63_70
| ~ spl63_111
| spl63_126
| ~ spl63_207 ),
inference(avatar_contradiction_clause,[],[f10269]) ).
fof(f13741,plain,
( ~ p102(sK59(sK60(sK62)))
| ~ sP2(sK59(sK60(sK62)))
| ~ r1(sK62,sK59(sK60(sK62)))
| p103(sK59(sK60(sK62)))
| spl63_260 ),
inference(resolution,[],[f10212,f515]) ).
fof(f13742,plain,
( ~ sP2(sK59(sK60(sK62)))
| ~ r1(sK62,sK59(sK60(sK62)))
| p103(sK59(sK60(sK62)))
| ~ spl63_32
| spl63_260 ),
inference(forward_subsumption_resolution,[],[f13741,f3070]) ).
fof(f13743,plain,
( ~ r1(sK62,sK59(sK60(sK62)))
| p103(sK59(sK60(sK62)))
| ~ spl63_32
| spl63_260 ),
inference(forward_subsumption_resolution,[],[f13742,f6886]) ).
fof(f13744,plain,
( p103(sK59(sK60(sK62)))
| ~ spl63_32
| ~ spl63_148
| spl63_260 ),
inference(forward_subsumption_resolution,[],[f13743,f8818]) ).
fof(f13745,plain,
( $false
| ~ spl63_32
| spl63_64
| ~ spl63_148
| spl63_260 ),
inference(forward_subsumption_resolution,[],[f13744,f6960]) ).
fof(f13746,plain,
( ~ spl63_32
| spl63_64
| ~ spl63_148
| spl63_260 ),
inference(avatar_contradiction_clause,[],[f13745]) ).
fof(f16617,plain,
( sP5(sK53(sK55(sK57(sK59(sK60(sK62))))))
| ~ spl63_262 ),
inference(resolution,[],[f10221,f163]) ).
fof(f17564,plain,
( ~ p104(sK55(sK57(sK59(sK60(sK62)))))
| ~ sP4(sK55(sK57(sK59(sK60(sK62)))))
| ~ r1(sK62,sK55(sK57(sK59(sK60(sK62)))))
| p105(sK55(sK57(sK59(sK60(sK62)))))
| ~ spl63_262 ),
inference(resolution,[],[f16617,f3196]) ).
fof(f17569,plain,
( ~ sP4(sK55(sK57(sK59(sK60(sK62)))))
| ~ r1(sK62,sK55(sK57(sK59(sK60(sK62)))))
| p105(sK55(sK57(sK59(sK60(sK62)))))
| ~ spl63_145
| ~ spl63_262 ),
inference(forward_subsumption_resolution,[],[f17564,f8796]) ).
fof(f17580,plain,
( ~ r1(sK62,sK55(sK57(sK59(sK60(sK62)))))
| p105(sK55(sK57(sK59(sK60(sK62)))))
| ~ spl63_145
| ~ spl63_150
| ~ spl63_262 ),
inference(forward_subsumption_resolution,[],[f17569,f9711]) ).
fof(f17581,plain,
( ~ r1(sK62,sK55(sK57(sK59(sK60(sK62)))))
| ~ spl63_145
| ~ spl63_150
| spl63_207
| ~ spl63_262 ),
inference(forward_subsumption_resolution,[],[f17580,f9773]) ).
fof(f18579,plain,
( ~ p103(sK57(sK59(sK60(sK62))))
| ~ sP3(sK57(sK59(sK60(sK62))))
| ~ r1(sK62,sK57(sK59(sK60(sK62))))
| p104(sK57(sK59(sK60(sK62))))
| ~ spl63_145
| ~ spl63_150
| spl63_207
| ~ spl63_262 ),
inference(resolution,[],[f17581,f509]) ).
fof(f18580,plain,
( ~ sP3(sK57(sK59(sK60(sK62))))
| ~ r1(sK62,sK57(sK59(sK60(sK62))))
| p104(sK57(sK59(sK60(sK62))))
| ~ spl63_70
| ~ spl63_145
| ~ spl63_150
| spl63_207
| ~ spl63_262 ),
inference(forward_subsumption_resolution,[],[f18579,f7068]) ).
fof(f18581,plain,
( ~ r1(sK62,sK57(sK59(sK60(sK62))))
| p104(sK57(sK59(sK60(sK62))))
| spl63_28
| ~ spl63_70
| ~ spl63_111
| ~ spl63_145
| ~ spl63_150
| spl63_207
| ~ spl63_262 ),
inference(forward_subsumption_resolution,[],[f18580,f8562]) ).
fof(f18582,plain,
( p104(sK57(sK59(sK60(sK62))))
| spl63_28
| ~ spl63_70
| ~ spl63_111
| ~ spl63_145
| ~ spl63_150
| spl63_207
| ~ spl63_260
| ~ spl63_262 ),
inference(forward_subsumption_resolution,[],[f18581,f10211]) ).
fof(f18583,plain,
( $false
| spl63_28
| ~ spl63_70
| ~ spl63_111
| spl63_126
| ~ spl63_145
| ~ spl63_150
| spl63_207
| ~ spl63_260
| ~ spl63_262 ),
inference(forward_subsumption_resolution,[],[f18582,f8630]) ).
fof(f18584,plain,
( spl63_28
| ~ spl63_70
| ~ spl63_111
| spl63_126
| ~ spl63_145
| ~ spl63_150
| spl63_207
| ~ spl63_260
| ~ spl63_262 ),
inference(avatar_contradiction_clause,[],[f18583]) ).
cnf(s31,plain,
( spl63_28
| spl63_32 ),
inference(sat_conversion,[],[f3071]) ).
cnf(s34,plain,
~ spl63_28,
inference(sat_conversion,[],[f3130]) ).
cnf(s68,plain,
( ~ spl63_32
| spl63_64
| spl63_70 ),
inference(sat_conversion,[],[f7069]) ).
cnf(s71,plain,
( spl63_28
| ~ spl63_64 ),
inference(sat_conversion,[],[f7125]) ).
cnf(s112,plain,
spl63_111,
inference(sat_conversion,[],[f7971]) ).
cnf(s144,plain,
( spl63_28
| ~ spl63_70
| ~ spl63_111
| spl63_126
| spl63_145 ),
inference(sat_conversion,[],[f8797]) ).
cnf(s148,plain,
( spl63_28
| ~ spl63_32
| spl63_64
| ~ spl63_111
| ~ spl63_148
| spl63_150 ),
inference(sat_conversion,[],[f8829]) ).
cnf(s151,plain,
( ~ spl63_32
| spl63_64
| ~ spl63_126 ),
inference(sat_conversion,[],[f8882]) ).
cnf(s160,plain,
( spl63_28
| ~ spl63_111
| spl63_148 ),
inference(sat_conversion,[],[f9013]) ).
cnf(s258,plain,
( spl63_28
| ~ spl63_70
| ~ spl63_111
| spl63_126
| ~ spl63_150
| ~ spl63_260
| spl63_262 ),
inference(sat_conversion,[],[f10222]) ).
cnf(s261,plain,
( spl63_28
| ~ spl63_70
| ~ spl63_111
| spl63_126
| ~ spl63_207 ),
inference(sat_conversion,[],[f10270]) ).
cnf(s282,plain,
( ~ spl63_32
| spl63_64
| ~ spl63_148
| spl63_260 ),
inference(sat_conversion,[],[f13746]) ).
cnf(s537,plain,
( spl63_28
| ~ spl63_70
| ~ spl63_111
| spl63_126
| ~ spl63_145
| ~ spl63_150
| spl63_207
| ~ spl63_260
| ~ spl63_262 ),
inference(sat_conversion,[],[f18584]) ).
cnf(s540,plain,
spl63_148,
inference(rat,[],[s160,s112,s34]) ).
cnf(s543,plain,
~ spl63_64,
inference(rat,[],[s71,s34]) ).
cnf(s575,plain,
spl63_32,
inference(rat,[],[s31,s34]) ).
cnf(s577,plain,
spl63_260,
inference(rat,[],[s282,s543,s540,s575]) ).
cnf(s589,plain,
~ spl63_126,
inference(rat,[],[s151,s543,s575]) ).
cnf(s592,plain,
spl63_150,
inference(rat,[],[s148,s543,s540,s112,s34,s575]) ).
cnf(s596,plain,
spl63_70,
inference(rat,[],[s68,s543,s575]) ).
cnf(s611,plain,
~ spl63_207,
inference(rat,[],[s261,s589,s34,s112,s596]) ).
cnf(s614,plain,
spl63_262,
inference(rat,[],[s258,s589,s577,s592,s34,s112,s596]) ).
cnf(s618,plain,
spl63_145,
inference(rat,[],[s144,s589,s34,s112,s596]) ).
cnf(s635,plain,
$false,
inference(rat,[],[s537,s614,s577,s596,s592,s589,s34,s112,s611,s618]) ).
fof(f18585,plain,
$false,
inference(avatar_sat_refutation,[],[s635]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL674+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.39 % Computer : n009.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Sun Sep 27 16:31:45 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.43 Running first-order model finding
% 0.13/0.43 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.83/1.35 % (2231803)Will run a generic schedule for satisfiability detection.
% 5.83/1.35 % (2231808)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1310021299_2999 on theBenchmark for (2999ds/0Mi)
% 5.83/1.35 % (2231809)% WARNING: option uhcvi not known.
% 5.83/1.35 % TRYING [1]
% 5.83/1.35 % TRYING [2]
% 5.83/1.35 % TRYING [3]
% 5.83/1.35 % (2231809)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3972629369:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.83/1.35 % (2231810)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=362406585:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.83/1.35 % (2231811)dis+10_1_sil=32000:sp=arity:random_seed=3217788061:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.83/1.35 % (2231814)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4280044292:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.83/1.35 % (2231812)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2831083219:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.83/1.35 % (2231813)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=748798042:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.83/1.35 % TRYING [4]
% 5.83/1.35 % TRYING [5]
% 5.83/1.35 % TRYING [6]
% 5.83/1.35 % TRYING [7]
% 5.83/1.35 % (2231811)Instruction limit reached!
% 5.83/1.35 % (2231811)------------------------------
% 5.83/1.35 % (2231811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.83/1.35 % (2231811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.35 % (2231811)CaDiCaL version: 2.1.3
% 5.83/1.35 % (2231811)Termination reason: Instruction limit
% 5.83/1.35 % (2231811)Termination phase: Saturation
% 5.83/1.35 % (2231811)Time elapsed: 0.049 s
% 5.83/1.35 % (2231811)Peak memory usage: 12 MB
% 5.83/1.35 % (2231811)Instructions burned: 105 (million)
% 5.83/1.35 % (2231814)Instruction limit reached!
% 5.83/1.35 % (2231814)------------------------------
% 5.83/1.35 % (2231814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.83/1.35 % (2231814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.35 % (2231814)CaDiCaL version: 2.1.3
% 5.83/1.35 % (2231814)Termination reason: Instruction limit
% 5.83/1.35 % (2231814)Termination phase: Saturation
% 5.83/1.35 % (2231814)Time elapsed: 0.057 s
% 5.83/1.35 % (2231814)Peak memory usage: 12 MB
% 5.83/1.35 % (2231814)Instructions burned: 160 (million)
% 5.83/1.35 % (2231812)Instruction limit reached!
% 5.83/1.35 % (2231812)------------------------------
% 5.83/1.35 % (2231812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.83/1.35 % (2231812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.35 % (2231812)CaDiCaL version: 2.1.3
% 5.83/1.35 % (2231812)Termination reason: Instruction limit
% 5.83/1.35 % (2231812)Termination phase: Saturation
% 5.83/1.35 % (2231812)Time elapsed: 0.063 s
% 5.83/1.35 % (2231812)Peak memory usage: 13 MB
% 5.83/1.35 % (2231812)Instructions burned: 117 (million)
% 5.83/1.35 % (2231822)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3896794865:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 5.83/1.35 % (2231813)Instruction limit reached!
% 5.83/1.35 % (2231813)------------------------------
% 5.83/1.35 % (2231813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.83/1.35 % (2231813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.35 % (2231813)CaDiCaL version: 2.1.3
% 5.83/1.35 % (2231813)Termination reason: Instruction limit
% 5.83/1.35 % (2231813)Termination phase: Saturation
% 5.83/1.35 % (2231813)Time elapsed: 0.073 s
% 5.83/1.35 % (2231813)Peak memory usage: 15 MB
% 5.83/1.35 % (2231813)Instructions burned: 132 (million)
% 5.83/1.35 % TRYING [1]
% 5.83/1.35 % TRYING [2]
% 5.83/1.35 % (2231823)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=204290596:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 5.83/1.35 % TRYING [3]
% 5.83/1.35 % TRYING [4]
% 5.83/1.35 % (2231824)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1278580773:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 5.83/1.35 % TRYING [5]
% 5.83/1.35 % (2231826)ott-21_1_sil=16000:fs=off:random_seed=2853156569:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 5.83/1.35 % TRYING [6]
% 5.83/1.35 % TRYING [8]
% 5.83/1.35 % (2231823)Instruction limit reached!
% 5.83/1.35 % (2231823)------------------------------
% 5.83/1.35 % (2231823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.83/1.35 % (2231823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.35 % (2231823)CaDiCaL version: 2.1.3
% 5.83/1.35 % (2231823)Termination reason: Instruction limit
% 5.83/1.35 % (2231823)Termination phase: Saturation
% 5.83/1.35 % (2231823)Time elapsed: 0.073 s
% 5.83/1.35 % (2231823)Peak memory usage: 15 MB
% 5.83/1.35 % (2231823)Instructions burned: 133 (million)
% 5.83/1.35 % TRYING [7]
% 5.83/1.35 % (2231830)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=444862712:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 5.83/1.35 % (2231826)Instruction limit reached!
% 5.83/1.35 % (2231826)------------------------------
% 5.83/1.35 % (2231826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.83/1.35 % (2231826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.35 % (2231826)CaDiCaL version: 2.1.3
% 5.83/1.35 % (2231826)Termination reason: Instruction limit
% 5.83/1.35 % (2231826)Termination phase: Saturation
% 5.83/1.35 % (2231826)Time elapsed: 0.091 s
% 5.83/1.35 % (2231826)Peak memory usage: 14 MB
% 5.83/1.35 % (2231826)Instructions burned: 180 (million)
% 5.83/1.35 % (2231832)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2799110327:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 5.83/1.35 % TRYING [1]
% 5.83/1.35 % TRYING [2]
% 5.83/1.35 % TRYING [3]
% 5.83/1.35 % TRYING [4]
% 5.83/1.35 % TRYING [5]
% 5.83/1.35 % TRYING [6]
% 5.83/1.35 % TRYING [7]
% 5.83/1.35 % TRYING [8]
% 5.83/1.35 % TRYING [8]
% 5.83/1.35 % (2231824)Instruction limit reached!
% 5.83/1.35 % (2231824)------------------------------
% 5.83/1.35 % (2231824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.83/1.35 % (2231824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.35 % (2231824)CaDiCaL version: 2.1.3
% 5.83/1.35 % (2231824)Termination reason: Instruction limit
% 5.83/1.35 % (2231824)Termination phase: Saturation
% 5.83/1.35 % (2231824)Time elapsed: 0.314 s
% 5.83/1.35 % (2231824)Peak memory usage: 25 MB
% 5.83/1.35 % (2231824)Instructions burned: 684 (million)
% 5.83/1.35 % (2231834)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3080898607:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 5.83/1.35 % (2231822)Instruction limit reached!
% 5.83/1.35 % (2231822)------------------------------
% 5.83/1.35 % (2231822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.83/1.35 % (2231822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.35 % (2231822)CaDiCaL version: 2.1.3
% 5.83/1.35 % (2231822)Termination reason: Instruction limit
% 5.83/1.35 % (2231822)Termination phase: Finite model building SAT solving
% 5.83/1.35 % (2231822)Time elapsed: 0.368 s
% 5.83/1.35 % (2231822)Peak memory usage: 17 MB
% 5.83/1.35 % (2231822)Instructions burned: 715 (million)
% 5.83/1.35 % (2231830)Instruction limit reached!
% 5.83/1.35 % (2231830)------------------------------
% 5.83/1.35 % (2231830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.83/1.35 % (2231830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.35 % (2231830)CaDiCaL version: 2.1.3
% 5.83/1.35 % (2231830)Termination reason: Instruction limit
% 5.83/1.35 % (2231830)Termination phase: Saturation
% 5.83/1.35 % (2231830)Time elapsed: 0.280 s
% 5.83/1.35 % (2231830)Peak memory usage: 17 MB
% 5.83/1.35 % (2231830)Instructions burned: 478 (million)
% 5.83/1.35 % (2231836)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3420430467:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 5.83/1.35 % TRYING [14]
% 5.83/1.35 % (2231837)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=95032556:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 5.83/1.35 % (2231832)Instruction limit reached!
% 5.83/1.35 % (2231832)------------------------------
% 5.83/1.35 % (2231832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.83/1.35 % (2231832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.35 % (2231832)CaDiCaL version: 2.1.3
% 5.83/1.35 % (2231832)Termination reason: Instruction limit
% 5.83/1.35 % (2231832)Termination phase: Finite model building SAT solving
% 5.83/1.35 % (2231832)Time elapsed: 0.387 s
% 5.83/1.35 % (2231832)Peak memory usage: 15 MB
% 5.83/1.35 % (2231832)Instructions burned: 867 (million)
% 5.83/1.35 % TRYING [9]
% 5.83/1.35 % (2231840)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2195236971:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 5.83/1.35 % (2231836)Instruction limit reached!
% 5.83/1.35 % (2231836)------------------------------
% 5.83/1.35 % (2231836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.83/1.35 % (2231836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.35 % (2231836)CaDiCaL version: 2.1.3
% 5.83/1.35 % (2231836)Termination reason: Instruction limit
% 5.83/1.35 % (2231836)Termination phase: Finite model building SAT solving
% 5.83/1.35 % (2231836)Time elapsed: 0.309 s
% 5.83/1.35 % (2231836)Peak memory usage: 25 MB
% 5.83/1.35 % (2231836)Instructions burned: 889 (million)
% 5.83/1.35 % (2231842)fmb+10_1_sil=64000:random_seed=1794531740:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 5.83/1.35 % TRYING [1]
% 5.83/1.35 % TRYING [2]
% 5.83/1.35 % TRYING [3]
% 5.83/1.35 % TRYING [4]
% 5.83/1.35 % (2231837)Instruction limit reached!
% 5.83/1.35 % (2231837)------------------------------
% 5.83/1.35 % (2231837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.83/1.35 % (2231837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.35 % (2231837)CaDiCaL version: 2.1.3
% 5.83/1.35 % (2231837)Termination reason: Instruction limit
% 5.83/1.35 % (2231837)Termination phase: Saturation
% 5.83/1.35 % (2231837)Time elapsed: 0.337 s
% 5.83/1.35 % (2231837)Peak memory usage: 30 MB
% 5.83/1.35 % (2231837)Instructions burned: 694 (million)
% 5.83/1.35 % TRYING [5]
% 5.83/1.35 % (2231844)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=89290218:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 5.83/1.35 % TRYING [20]
% 5.83/1.35 % TRYING [6]
% 5.83/1.35 % (2231834) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2231803-2231834"...
% 5.83/1.35 % (2231834)...printing done.
% 5.83/1.35 % TRYING [7]
% 5.83/1.35 % (2231834)Refutation found. Thanks to Tanya!
% 5.83/1.35 % SZS status Theorem for theBenchmark
% 5.83/1.35 % SZS output start Proof for theBenchmark
% See solution above
% 5.83/1.35 % (2231834)------------------------------
% 5.83/1.35 % (2231834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.83/1.35 % (2231834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.35 % (2231834)CaDiCaL version: 2.1.3
% 5.83/1.35 % (2231834)Termination reason: Refutation
% 5.83/1.35 % (2231834)Time elapsed: 0.450 s
% 5.83/1.35 % (2231834)Peak memory usage: 27 MB
% 5.83/1.35 % (2231834)Instructions burned: 916 (million)
% 5.83/1.35 % (2231803)Success in time 0.915 s
% 5.83/1.35 % Vampire exiting
%------------------------------------------------------------------------------