%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL674+1.020 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:55:46 AM UTC 2026
% Result : Theorem 8.81s 2.17s
% Output : Refutation 9.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 71
% Syntax : Number of formulae : 339 ( 44 unt; 68 def)
% Number of atoms : 4289 ( 0 equ)
% Maximal formula atoms : 436 ( 12 avg)
% Number of connectives : 6858 (2908 ~;2159 |;1764 &)
% ( 26 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 81 ( 7 avg)
% Maximal term depth : 8 ( 1 avg)
% Number of predicates : 113 ( 112 usr; 27 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 1 con; 0-1 aty)
% Number of variables : 759 ( 0 sgn 604 !; 155 ?)
% 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)
| p8(X1) )
| ~ ( ! [X1] :
( ~ r1(X0,X1)
| ( ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p21(X0)
& ~ p121(X0)
& p120(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p21(X0)
& ~ p121(X0)
& p120(X0) ) ) )
| ~ ( ~ p120(X1)
& p119(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p20(X0)
& ~ p120(X0)
& p119(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p20(X0)
& ~ p120(X0)
& p119(X0) ) ) )
| ~ ( ~ p119(X1)
& p118(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p19(X0)
& ~ p119(X0)
& p118(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p19(X0)
& ~ p119(X0)
& p118(X0) ) ) )
| ~ ( ~ p118(X1)
& p117(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p18(X0)
& ~ p118(X0)
& p117(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p18(X0)
& ~ p118(X0)
& p117(X0) ) ) )
| ~ ( ~ p117(X1)
& p116(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p17(X0)
& ~ p117(X0)
& p116(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p17(X0)
& ~ p117(X0)
& p116(X0) ) ) )
| ~ ( ~ p116(X1)
& p115(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)
| ~ p21(X0)
| ~ p120(X0) )
| p21(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p21(X0)
| ~ p120(X0) )
| ~ p21(X1) ) )
| ~ p120(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p20(X0)
| ~ p119(X0) )
| p20(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p20(X0)
| ~ p119(X0) )
| ~ p20(X1) ) )
| ~ p119(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p19(X0)
| ~ p118(X0) )
| p19(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p19(X0)
| ~ p118(X0) )
| ~ p19(X1) ) )
| ~ p118(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p18(X0)
| ~ p117(X0) )
| p18(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p18(X0)
| ~ p117(X0) )
| ~ p18(X1) ) )
| ~ p117(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p17(X0)
| ~ p116(X0) )
| p17(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p17(X0)
| ~ p116(X0) )
| ~ p17(X1) ) )
| ~ p116(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) )
& ( p120(X1)
| ~ p121(X1) )
& ( p119(X1)
| ~ p120(X1) )
& ( p118(X1)
| ~ p119(X1) )
& ( p117(X1)
| ~ p118(X1) )
& ( p116(X1)
| ~ p117(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)
| p8(X1) )
| ~ ( ! [X1] :
( ~ r1(X0,X1)
| ( ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p21(X0)
& ~ p121(X0)
& p120(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p21(X0)
& ~ p121(X0)
& p120(X0) ) ) )
| ~ ( ~ p120(X1)
& p119(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p20(X0)
& ~ p120(X0)
& p119(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p20(X0)
& ~ p120(X0)
& p119(X0) ) ) )
| ~ ( ~ p119(X1)
& p118(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p19(X0)
& ~ p119(X0)
& p118(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p19(X0)
& ~ p119(X0)
& p118(X0) ) ) )
| ~ ( ~ p118(X1)
& p117(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p18(X0)
& ~ p118(X0)
& p117(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p18(X0)
& ~ p118(X0)
& p117(X0) ) ) )
| ~ ( ~ p117(X1)
& p116(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p17(X0)
& ~ p117(X0)
& p116(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p17(X0)
& ~ p117(X0)
& p116(X0) ) ) )
| ~ ( ~ p116(X1)
& p115(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)
| ~ p21(X0)
| ~ p120(X0) )
| p21(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p21(X0)
| ~ p120(X0) )
| ~ p21(X1) ) )
| ~ p120(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p20(X0)
| ~ p119(X0) )
| p20(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p20(X0)
| ~ p119(X0) )
| ~ p20(X1) ) )
| ~ p119(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p19(X0)
| ~ p118(X0) )
| p19(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p19(X0)
| ~ p118(X0) )
| ~ p19(X1) ) )
| ~ p118(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p18(X0)
| ~ p117(X0) )
| p18(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p18(X0)
| ~ p117(X0) )
| ~ p18(X1) ) )
| ~ p117(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p17(X0)
| ~ p116(X0) )
| p17(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p17(X0)
| ~ p116(X0) )
| ~ p17(X1) ) )
| ~ p116(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) )
& ( p120(X1)
| ~ p121(X1) )
& ( p119(X1)
| ~ p120(X1) )
& ( p118(X1)
| ~ p119(X1) )
& ( p117(X1)
| ~ p118(X1) )
& ( p116(X1)
| ~ p117(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)
| p8(X1) )
| ~ ( ! [X2] :
( ~ r1(X0,X2)
| ( ( ( ~ ! [X3] :
( ~ r1(X2,X3)
| ~ ( ~ p21(X3)
& ~ p121(X3)
& p120(X3) ) )
& ~ ! [X4] :
( ~ r1(X2,X4)
| ~ ( p21(X4)
& ~ p121(X4)
& p120(X4) ) ) )
| ~ ( ~ p120(X2)
& p119(X2) ) )
& ( ( ~ ! [X5] :
( ~ r1(X2,X5)
| ~ ( ~ p20(X5)
& ~ p120(X5)
& p119(X5) ) )
& ~ ! [X6] :
( ~ r1(X2,X6)
| ~ ( p20(X6)
& ~ p120(X6)
& p119(X6) ) ) )
| ~ ( ~ p119(X2)
& p118(X2) ) )
& ( ( ~ ! [X7] :
( ~ r1(X2,X7)
| ~ ( ~ p19(X7)
& ~ p119(X7)
& p118(X7) ) )
& ~ ! [X8] :
( ~ r1(X2,X8)
| ~ ( p19(X8)
& ~ p119(X8)
& p118(X8) ) ) )
| ~ ( ~ p118(X2)
& p117(X2) ) )
& ( ( ~ ! [X9] :
( ~ r1(X2,X9)
| ~ ( ~ p18(X9)
& ~ p118(X9)
& p117(X9) ) )
& ~ ! [X10] :
( ~ r1(X2,X10)
| ~ ( p18(X10)
& ~ p118(X10)
& p117(X10) ) ) )
| ~ ( ~ p117(X2)
& p116(X2) ) )
& ( ( ~ ! [X11] :
( ~ r1(X2,X11)
| ~ ( ~ p17(X11)
& ~ p117(X11)
& p116(X11) ) )
& ~ ! [X12] :
( ~ r1(X2,X12)
| ~ ( p17(X12)
& ~ p117(X12)
& p116(X12) ) ) )
| ~ ( ~ p116(X2)
& p115(X2) ) )
& ( ( ~ ! [X13] :
( ~ r1(X2,X13)
| ~ ( ~ p16(X13)
& ~ p116(X13)
& p115(X13) ) )
& ~ ! [X14] :
( ~ r1(X2,X14)
| ~ ( p16(X14)
& ~ p116(X14)
& p115(X14) ) ) )
| ~ ( ~ p115(X2)
& p114(X2) ) )
& ( ( ~ ! [X15] :
( ~ r1(X2,X15)
| ~ ( ~ p15(X15)
& ~ p115(X15)
& p114(X15) ) )
& ~ ! [X16] :
( ~ r1(X2,X16)
| ~ ( p15(X16)
& ~ p115(X16)
& p114(X16) ) ) )
| ~ ( ~ p114(X2)
& p113(X2) ) )
& ( ( ~ ! [X17] :
( ~ r1(X2,X17)
| ~ ( ~ p14(X17)
& ~ p114(X17)
& p113(X17) ) )
& ~ ! [X18] :
( ~ r1(X2,X18)
| ~ ( p14(X18)
& ~ p114(X18)
& p113(X18) ) ) )
| ~ ( ~ p113(X2)
& p112(X2) ) )
& ( ( ~ ! [X19] :
( ~ r1(X2,X19)
| ~ ( ~ p13(X19)
& ~ p113(X19)
& p112(X19) ) )
& ~ ! [X20] :
( ~ r1(X2,X20)
| ~ ( p13(X20)
& ~ p113(X20)
& p112(X20) ) ) )
| ~ ( ~ p112(X2)
& p111(X2) ) )
& ( ( ~ ! [X21] :
( ~ r1(X2,X21)
| ~ ( ~ p12(X21)
& ~ p112(X21)
& p111(X21) ) )
& ~ ! [X22] :
( ~ r1(X2,X22)
| ~ ( p12(X22)
& ~ p112(X22)
& p111(X22) ) ) )
| ~ ( ~ p111(X2)
& p110(X2) ) )
& ( ( ~ ! [X23] :
( ~ r1(X2,X23)
| ~ ( ~ p11(X23)
& ~ p111(X23)
& p110(X23) ) )
& ~ ! [X24] :
( ~ r1(X2,X24)
| ~ ( p11(X24)
& ~ p111(X24)
& p110(X24) ) ) )
| ~ ( ~ p110(X2)
& p109(X2) ) )
& ( ( ~ ! [X25] :
( ~ r1(X2,X25)
| ~ ( ~ p10(X25)
& ~ p110(X25)
& p109(X25) ) )
& ~ ! [X26] :
( ~ r1(X2,X26)
| ~ ( p10(X26)
& ~ p110(X26)
& p109(X26) ) ) )
| ~ ( ~ p109(X2)
& p108(X2) ) )
& ( ( ~ ! [X27] :
( ~ r1(X2,X27)
| ~ ( ~ p9(X27)
& ~ p109(X27)
& p108(X27) ) )
& ~ ! [X28] :
( ~ r1(X2,X28)
| ~ ( p9(X28)
& ~ p109(X28)
& p108(X28) ) ) )
| ~ ( ~ p108(X2)
& p107(X2) ) )
& ( ( ~ ! [X29] :
( ~ r1(X2,X29)
| ~ ( ~ p8(X29)
& ~ p108(X29)
& p107(X29) ) )
& ~ ! [X30] :
( ~ r1(X2,X30)
| ~ ( p8(X30)
& ~ p108(X30)
& p107(X30) ) ) )
| ~ ( ~ p107(X2)
& p106(X2) ) )
& ( ( ~ ! [X31] :
( ~ r1(X2,X31)
| ~ ( ~ p7(X31)
& ~ p107(X31)
& p106(X31) ) )
& ~ ! [X32] :
( ~ r1(X2,X32)
| ~ ( p7(X32)
& ~ p107(X32)
& p106(X32) ) ) )
| ~ ( ~ p106(X2)
& p105(X2) ) )
& ( ( ~ ! [X33] :
( ~ r1(X2,X33)
| ~ ( ~ p6(X33)
& ~ p106(X33)
& p105(X33) ) )
& ~ ! [X34] :
( ~ r1(X2,X34)
| ~ ( p6(X34)
& ~ p106(X34)
& p105(X34) ) ) )
| ~ ( ~ p105(X2)
& p104(X2) ) )
& ( ( ~ ! [X35] :
( ~ r1(X2,X35)
| ~ ( ~ p5(X35)
& ~ p105(X35)
& p104(X35) ) )
& ~ ! [X36] :
( ~ r1(X2,X36)
| ~ ( p5(X36)
& ~ p105(X36)
& p104(X36) ) ) )
| ~ ( ~ p104(X2)
& p103(X2) ) )
& ( ( ~ ! [X37] :
( ~ r1(X2,X37)
| ~ ( ~ p4(X37)
& ~ p104(X37)
& p103(X37) ) )
& ~ ! [X38] :
( ~ r1(X2,X38)
| ~ ( p4(X38)
& ~ p104(X38)
& p103(X38) ) ) )
| ~ ( ~ p103(X2)
& p102(X2) ) )
& ( ( ~ ! [X39] :
( ~ r1(X2,X39)
| ~ ( ~ p3(X39)
& ~ p103(X39)
& p102(X39) ) )
& ~ ! [X40] :
( ~ r1(X2,X40)
| ~ ( p3(X40)
& ~ p103(X40)
& p102(X40) ) ) )
| ~ ( ~ p102(X2)
& p101(X2) ) )
& ( ( ~ ! [X41] :
( ~ r1(X2,X41)
| ~ ( ~ p2(X41)
& ~ p102(X41)
& p101(X41) ) )
& ~ ! [X42] :
( ~ r1(X2,X42)
| ~ ( p2(X42)
& ~ p102(X42)
& p101(X42) ) ) )
| ~ ( ~ p101(X2)
& p100(X2) ) )
& ( ( ( ! [X43] :
( ~ r1(X2,X43)
| ~ p21(X43)
| ~ p120(X43) )
| p21(X2) )
& ( ! [X44] :
( ~ r1(X2,X44)
| p21(X44)
| ~ p120(X44) )
| ~ p21(X2) ) )
| ~ p120(X2) )
& ( ( ( ! [X45] :
( ~ r1(X2,X45)
| ~ p20(X45)
| ~ p119(X45) )
| p20(X2) )
& ( ! [X46] :
( ~ r1(X2,X46)
| p20(X46)
| ~ p119(X46) )
| ~ p20(X2) ) )
| ~ p119(X2) )
& ( ( ( ! [X47] :
( ~ r1(X2,X47)
| ~ p19(X47)
| ~ p118(X47) )
| p19(X2) )
& ( ! [X48] :
( ~ r1(X2,X48)
| p19(X48)
| ~ p118(X48) )
| ~ p19(X2) ) )
| ~ p118(X2) )
& ( ( ( ! [X49] :
( ~ r1(X2,X49)
| ~ p18(X49)
| ~ p117(X49) )
| p18(X2) )
& ( ! [X50] :
( ~ r1(X2,X50)
| p18(X50)
| ~ p117(X50) )
| ~ p18(X2) ) )
| ~ p117(X2) )
& ( ( ( ! [X51] :
( ~ r1(X2,X51)
| ~ p17(X51)
| ~ p116(X51) )
| p17(X2) )
& ( ! [X52] :
( ~ r1(X2,X52)
| p17(X52)
| ~ p116(X52) )
| ~ p17(X2) ) )
| ~ p116(X2) )
& ( ( ( ! [X53] :
( ~ r1(X2,X53)
| ~ p16(X53)
| ~ p115(X53) )
| p16(X2) )
& ( ! [X54] :
( ~ r1(X2,X54)
| p16(X54)
| ~ p115(X54) )
| ~ p16(X2) ) )
| ~ p115(X2) )
& ( ( ( ! [X55] :
( ~ r1(X2,X55)
| ~ p15(X55)
| ~ p114(X55) )
| p15(X2) )
& ( ! [X56] :
( ~ r1(X2,X56)
| p15(X56)
| ~ p114(X56) )
| ~ p15(X2) ) )
| ~ p114(X2) )
& ( ( ( ! [X57] :
( ~ r1(X2,X57)
| ~ p14(X57)
| ~ p113(X57) )
| p14(X2) )
& ( ! [X58] :
( ~ r1(X2,X58)
| p14(X58)
| ~ p113(X58) )
| ~ p14(X2) ) )
| ~ p113(X2) )
& ( ( ( ! [X59] :
( ~ r1(X2,X59)
| ~ p13(X59)
| ~ p112(X59) )
| p13(X2) )
& ( ! [X60] :
( ~ r1(X2,X60)
| p13(X60)
| ~ p112(X60) )
| ~ p13(X2) ) )
| ~ p112(X2) )
& ( ( ( ! [X61] :
( ~ r1(X2,X61)
| ~ p12(X61)
| ~ p111(X61) )
| p12(X2) )
& ( ! [X62] :
( ~ r1(X2,X62)
| p12(X62)
| ~ p111(X62) )
| ~ p12(X2) ) )
| ~ p111(X2) )
& ( ( ( ! [X63] :
( ~ r1(X2,X63)
| ~ p11(X63)
| ~ p110(X63) )
| p11(X2) )
& ( ! [X64] :
( ~ r1(X2,X64)
| p11(X64)
| ~ p110(X64) )
| ~ p11(X2) ) )
| ~ p110(X2) )
& ( ( ( ! [X65] :
( ~ r1(X2,X65)
| ~ p10(X65)
| ~ p109(X65) )
| p10(X2) )
& ( ! [X66] :
( ~ r1(X2,X66)
| p10(X66)
| ~ p109(X66) )
| ~ p10(X2) ) )
| ~ p109(X2) )
& ( ( ( ! [X67] :
( ~ r1(X2,X67)
| ~ p9(X67)
| ~ p108(X67) )
| p9(X2) )
& ( ! [X68] :
( ~ r1(X2,X68)
| p9(X68)
| ~ p108(X68) )
| ~ p9(X2) ) )
| ~ p108(X2) )
& ( ( ( ! [X69] :
( ~ r1(X2,X69)
| ~ p8(X69)
| ~ p107(X69) )
| p8(X2) )
& ( ! [X70] :
( ~ r1(X2,X70)
| p8(X70)
| ~ p107(X70) )
| ~ p8(X2) ) )
| ~ p107(X2) )
& ( ( ( ! [X71] :
( ~ r1(X2,X71)
| ~ p7(X71)
| ~ p106(X71) )
| p7(X2) )
& ( ! [X72] :
( ~ r1(X2,X72)
| p7(X72)
| ~ p106(X72) )
| ~ p7(X2) ) )
| ~ p106(X2) )
& ( ( ( ! [X73] :
( ~ r1(X2,X73)
| ~ p6(X73)
| ~ p105(X73) )
| p6(X2) )
& ( ! [X74] :
( ~ r1(X2,X74)
| p6(X74)
| ~ p105(X74) )
| ~ p6(X2) ) )
| ~ p105(X2) )
& ( ( ( ! [X75] :
( ~ r1(X2,X75)
| ~ p5(X75)
| ~ p104(X75) )
| p5(X2) )
& ( ! [X76] :
( ~ r1(X2,X76)
| p5(X76)
| ~ p104(X76) )
| ~ p5(X2) ) )
| ~ p104(X2) )
& ( ( ( ! [X77] :
( ~ r1(X2,X77)
| ~ p4(X77)
| ~ p103(X77) )
| p4(X2) )
& ( ! [X78] :
( ~ r1(X2,X78)
| p4(X78)
| ~ p103(X78) )
| ~ p4(X2) ) )
| ~ p103(X2) )
& ( ( ( ! [X79] :
( ~ r1(X2,X79)
| ~ p3(X79)
| ~ p102(X79) )
| p3(X2) )
& ( ! [X80] :
( ~ r1(X2,X80)
| p3(X80)
| ~ p102(X80) )
| ~ p3(X2) ) )
| ~ p102(X2) )
& ( ( ( ! [X81] :
( ~ r1(X2,X81)
| ~ p2(X81)
| ~ p101(X81) )
| p2(X2) )
& ( ! [X82] :
( ~ r1(X2,X82)
| p2(X82)
| ~ p101(X82) )
| ~ p2(X2) ) )
| ~ p101(X2) )
& ( ( ( ! [X83] :
( ~ r1(X2,X83)
| ~ p1(X83)
| ~ p100(X83) )
| p1(X2) )
& ( ! [X84] :
( ~ r1(X2,X84)
| p1(X84)
| ~ p100(X84) )
| ~ p1(X2) ) )
| ~ p100(X2) )
& ( p120(X2)
| ~ p121(X2) )
& ( p119(X2)
| ~ p120(X2) )
& ( p118(X2)
| ~ p119(X2) )
& ( p117(X2)
| ~ p118(X2) )
& ( p116(X2)
| ~ p117(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)
| p8(X1) )
| ~ ( ! [X2] :
( ~ r1(X0,X2)
| ( ( ( ~ ! [X3] :
( ~ r1(X2,X3)
| ~ ( ~ p21(X3)
& ~ p121(X3)
& p120(X3) ) )
& ~ ! [X4] :
( ~ r1(X2,X4)
| ~ ( p21(X4)
& ~ p121(X4)
& p120(X4) ) ) )
| ~ ( ~ p120(X2)
& p119(X2) ) )
& ( ( ~ ! [X5] :
( ~ r1(X2,X5)
| ~ ( ~ p20(X5)
& ~ p120(X5)
& p119(X5) ) )
& ~ ! [X6] :
( ~ r1(X2,X6)
| ~ ( p20(X6)
& ~ p120(X6)
& p119(X6) ) ) )
| ~ ( ~ p119(X2)
& p118(X2) ) )
& ( ( ~ ! [X7] :
( ~ r1(X2,X7)
| ~ ( ~ p19(X7)
& ~ p119(X7)
& p118(X7) ) )
& ~ ! [X8] :
( ~ r1(X2,X8)
| ~ ( p19(X8)
& ~ p119(X8)
& p118(X8) ) ) )
| ~ ( ~ p118(X2)
& p117(X2) ) )
& ( ( ~ ! [X9] :
( ~ r1(X2,X9)
| ~ ( ~ p18(X9)
& ~ p118(X9)
& p117(X9) ) )
& ~ ! [X10] :
( ~ r1(X2,X10)
| ~ ( p18(X10)
& ~ p118(X10)
& p117(X10) ) ) )
| ~ ( ~ p117(X2)
& p116(X2) ) )
& ( ( ~ ! [X11] :
( ~ r1(X2,X11)
| ~ ( ~ p17(X11)
& ~ p117(X11)
& p116(X11) ) )
& ~ ! [X12] :
( ~ r1(X2,X12)
| ~ ( p17(X12)
& ~ p117(X12)
& p116(X12) ) ) )
| ~ ( ~ p116(X2)
& p115(X2) ) )
& ( ( ~ ! [X13] :
( ~ r1(X2,X13)
| ~ ( ~ p16(X13)
& ~ p116(X13)
& p115(X13) ) )
& ~ ! [X14] :
( ~ r1(X2,X14)
| ~ ( p16(X14)
& ~ p116(X14)
& p115(X14) ) ) )
| ~ ( ~ p115(X2)
& p114(X2) ) )
& ( ( ~ ! [X15] :
( ~ r1(X2,X15)
| ~ ( ~ p15(X15)
& ~ p115(X15)
& p114(X15) ) )
& ~ ! [X16] :
( ~ r1(X2,X16)
| ~ ( p15(X16)
& ~ p115(X16)
& p114(X16) ) ) )
| ~ ( ~ p114(X2)
& p113(X2) ) )
& ( ( ~ ! [X17] :
( ~ r1(X2,X17)
| ~ ( ~ p14(X17)
& ~ p114(X17)
& p113(X17) ) )
& ~ ! [X18] :
( ~ r1(X2,X18)
| ~ ( p14(X18)
& ~ p114(X18)
& p113(X18) ) ) )
| ~ ( ~ p113(X2)
& p112(X2) ) )
& ( ( ~ ! [X19] :
( ~ r1(X2,X19)
| ~ ( ~ p13(X19)
& ~ p113(X19)
& p112(X19) ) )
& ~ ! [X20] :
( ~ r1(X2,X20)
| ~ ( p13(X20)
& ~ p113(X20)
& p112(X20) ) ) )
| ~ ( ~ p112(X2)
& p111(X2) ) )
& ( ( ~ ! [X21] :
( ~ r1(X2,X21)
| ~ ( ~ p12(X21)
& ~ p112(X21)
& p111(X21) ) )
& ~ ! [X22] :
( ~ r1(X2,X22)
| ~ ( p12(X22)
& ~ p112(X22)
& p111(X22) ) ) )
| ~ ( ~ p111(X2)
& p110(X2) ) )
& ( ( ~ ! [X23] :
( ~ r1(X2,X23)
| ~ ( ~ p11(X23)
& ~ p111(X23)
& p110(X23) ) )
& ~ ! [X24] :
( ~ r1(X2,X24)
| ~ ( p11(X24)
& ~ p111(X24)
& p110(X24) ) ) )
| ~ ( ~ p110(X2)
& p109(X2) ) )
& ( ( ~ ! [X25] :
( ~ r1(X2,X25)
| ~ ( ~ p10(X25)
& ~ p110(X25)
& p109(X25) ) )
& ~ ! [X26] :
( ~ r1(X2,X26)
| ~ ( p10(X26)
& ~ p110(X26)
& p109(X26) ) ) )
| ~ ( ~ p109(X2)
& p108(X2) ) )
& ( ( ~ ! [X27] :
( ~ r1(X2,X27)
| ~ ( ~ p9(X27)
& ~ p109(X27)
& p108(X27) ) )
& ~ ! [X28] :
( ~ r1(X2,X28)
| ~ ( p9(X28)
& ~ p109(X28)
& p108(X28) ) ) )
| ~ ( ~ p108(X2)
& p107(X2) ) )
& ( ( ~ ! [X29] :
( ~ r1(X2,X29)
| ~ ( ~ p8(X29)
& ~ p108(X29)
& p107(X29) ) )
& ~ ! [X30] :
( ~ r1(X2,X30)
| ~ ( p8(X30)
& ~ p108(X30)
& p107(X30) ) ) )
| ~ ( ~ p107(X2)
& p106(X2) ) )
& ( ( ~ ! [X31] :
( ~ r1(X2,X31)
| ~ ( ~ p7(X31)
& ~ p107(X31)
& p106(X31) ) )
& ~ ! [X32] :
( ~ r1(X2,X32)
| ~ ( p7(X32)
& ~ p107(X32)
& p106(X32) ) ) )
| ~ ( ~ p106(X2)
& p105(X2) ) )
& ( ( ~ ! [X33] :
( ~ r1(X2,X33)
| ~ ( ~ p6(X33)
& ~ p106(X33)
& p105(X33) ) )
& ~ ! [X34] :
( ~ r1(X2,X34)
| ~ ( p6(X34)
& ~ p106(X34)
& p105(X34) ) ) )
| ~ ( ~ p105(X2)
& p104(X2) ) )
& ( ( ~ ! [X35] :
( ~ r1(X2,X35)
| ~ ( ~ p5(X35)
& ~ p105(X35)
& p104(X35) ) )
& ~ ! [X36] :
( ~ r1(X2,X36)
| ~ ( p5(X36)
& ~ p105(X36)
& p104(X36) ) ) )
| ~ ( ~ p104(X2)
& p103(X2) ) )
& ( ( ~ ! [X37] :
( ~ r1(X2,X37)
| ~ ( ~ p4(X37)
& ~ p104(X37)
& p103(X37) ) )
& ~ ! [X38] :
( ~ r1(X2,X38)
| ~ ( p4(X38)
& ~ p104(X38)
& p103(X38) ) ) )
| ~ ( ~ p103(X2)
& p102(X2) ) )
& ( ( ~ ! [X39] :
( ~ r1(X2,X39)
| ~ ( ~ p3(X39)
& ~ p103(X39)
& p102(X39) ) )
& ~ ! [X40] :
( ~ r1(X2,X40)
| ~ ( p3(X40)
& ~ p103(X40)
& p102(X40) ) ) )
| ~ ( ~ p102(X2)
& p101(X2) ) )
& ( ( ~ ! [X41] :
( ~ r1(X2,X41)
| ~ ( ~ p2(X41)
& ~ p102(X41)
& p101(X41) ) )
& ~ ! [X42] :
( ~ r1(X2,X42)
| ~ ( p2(X42)
& ~ p102(X42)
& p101(X42) ) ) )
| ~ ( ~ p101(X2)
& p100(X2) ) )
& ( ( ( ! [X43] :
( ~ r1(X2,X43)
| ~ p21(X43)
| ~ p120(X43) )
| p21(X2) )
& ( ! [X44] :
( ~ r1(X2,X44)
| p21(X44)
| ~ p120(X44) )
| ~ p21(X2) ) )
| ~ p120(X2) )
& ( ( ( ! [X45] :
( ~ r1(X2,X45)
| ~ p20(X45)
| ~ p119(X45) )
| p20(X2) )
& ( ! [X46] :
( ~ r1(X2,X46)
| p20(X46)
| ~ p119(X46) )
| ~ p20(X2) ) )
| ~ p119(X2) )
& ( ( ( ! [X47] :
( ~ r1(X2,X47)
| ~ p19(X47)
| ~ p118(X47) )
| p19(X2) )
& ( ! [X48] :
( ~ r1(X2,X48)
| p19(X48)
| ~ p118(X48) )
| ~ p19(X2) ) )
| ~ p118(X2) )
& ( ( ( ! [X49] :
( ~ r1(X2,X49)
| ~ p18(X49)
| ~ p117(X49) )
| p18(X2) )
& ( ! [X50] :
( ~ r1(X2,X50)
| p18(X50)
| ~ p117(X50) )
| ~ p18(X2) ) )
| ~ p117(X2) )
& ( ( ( ! [X51] :
( ~ r1(X2,X51)
| ~ p17(X51)
| ~ p116(X51) )
| p17(X2) )
& ( ! [X52] :
( ~ r1(X2,X52)
| p17(X52)
| ~ p116(X52) )
| ~ p17(X2) ) )
| ~ p116(X2) )
& ( ( ( ! [X53] :
( ~ r1(X2,X53)
| ~ p16(X53)
| ~ p115(X53) )
| p16(X2) )
& ( ! [X54] :
( ~ r1(X2,X54)
| p16(X54)
| ~ p115(X54) )
| ~ p16(X2) ) )
| ~ p115(X2) )
& ( ( ( ! [X55] :
( ~ r1(X2,X55)
| ~ p15(X55)
| ~ p114(X55) )
| p15(X2) )
& ( ! [X56] :
( ~ r1(X2,X56)
| p15(X56)
| ~ p114(X56) )
| ~ p15(X2) ) )
| ~ p114(X2) )
& ( ( ( ! [X57] :
( ~ r1(X2,X57)
| ~ p14(X57)
| ~ p113(X57) )
| p14(X2) )
& ( ! [X58] :
( ~ r1(X2,X58)
| p14(X58)
| ~ p113(X58) )
| ~ p14(X2) ) )
| ~ p113(X2) )
& ( ( ( ! [X59] :
( ~ r1(X2,X59)
| ~ p13(X59)
| ~ p112(X59) )
| p13(X2) )
& ( ! [X60] :
( ~ r1(X2,X60)
| p13(X60)
| ~ p112(X60) )
| ~ p13(X2) ) )
| ~ p112(X2) )
& ( ( ( ! [X61] :
( ~ r1(X2,X61)
| ~ p12(X61)
| ~ p111(X61) )
| p12(X2) )
& ( ! [X62] :
( ~ r1(X2,X62)
| p12(X62)
| ~ p111(X62) )
| ~ p12(X2) ) )
| ~ p111(X2) )
& ( ( ( ! [X63] :
( ~ r1(X2,X63)
| ~ p11(X63)
| ~ p110(X63) )
| p11(X2) )
& ( ! [X64] :
( ~ r1(X2,X64)
| p11(X64)
| ~ p110(X64) )
| ~ p11(X2) ) )
| ~ p110(X2) )
& ( ( ( ! [X65] :
( ~ r1(X2,X65)
| ~ p10(X65)
| ~ p109(X65) )
| p10(X2) )
& ( ! [X66] :
( ~ r1(X2,X66)
| p10(X66)
| ~ p109(X66) )
| ~ p10(X2) ) )
| ~ p109(X2) )
& ( ( ( ! [X67] :
( ~ r1(X2,X67)
| ~ p9(X67)
| ~ p108(X67) )
| p9(X2) )
& ( ! [X68] :
( ~ r1(X2,X68)
| p9(X68)
| ~ p108(X68) )
| ~ p9(X2) ) )
| ~ p108(X2) )
& ( ( ( ! [X69] :
( ~ r1(X2,X69)
| ~ p8(X69)
| ~ p107(X69) )
| p8(X2) )
& ( ! [X70] :
( ~ r1(X2,X70)
| p8(X70)
| ~ p107(X70) )
| ~ p8(X2) ) )
| ~ p107(X2) )
& ( ( ( ! [X71] :
( ~ r1(X2,X71)
| ~ p7(X71)
| ~ p106(X71) )
| p7(X2) )
& ( ! [X72] :
( ~ r1(X2,X72)
| p7(X72)
| ~ p106(X72) )
| ~ p7(X2) ) )
| ~ p106(X2) )
& ( ( ( ! [X73] :
( ~ r1(X2,X73)
| ~ p6(X73)
| ~ p105(X73) )
| p6(X2) )
& ( ! [X74] :
( ~ r1(X2,X74)
| p6(X74)
| ~ p105(X74) )
| ~ p6(X2) ) )
| ~ p105(X2) )
& ( ( ( ! [X75] :
( ~ r1(X2,X75)
| ~ p5(X75)
| ~ p104(X75) )
| p5(X2) )
& ( ! [X76] :
( ~ r1(X2,X76)
| p5(X76)
| ~ p104(X76) )
| ~ p5(X2) ) )
| ~ p104(X2) )
& ( ( ( ! [X77] :
( ~ r1(X2,X77)
| ~ p4(X77)
| ~ p103(X77) )
| p4(X2) )
& ( ! [X78] :
( ~ r1(X2,X78)
| p4(X78)
| ~ p103(X78) )
| ~ p4(X2) ) )
| ~ p103(X2) )
& ( ( ( ! [X79] :
( ~ r1(X2,X79)
| ~ p3(X79)
| ~ p102(X79) )
| p3(X2) )
& ( ! [X80] :
( ~ r1(X2,X80)
| p3(X80)
| ~ p102(X80) )
| ~ p3(X2) ) )
| ~ p102(X2) )
& ( ( ( ! [X81] :
( ~ r1(X2,X81)
| ~ p2(X81)
| ~ p101(X81) )
| p2(X2) )
& ( ! [X82] :
( ~ r1(X2,X82)
| p2(X82)
| ~ p101(X82) )
| ~ p2(X2) ) )
| ~ p101(X2) )
& ( ( ( ! [X83] :
( ~ r1(X2,X83)
| ~ p1(X83)
| ~ p100(X83) )
| p1(X2) )
& ( ! [X84] :
( ~ r1(X2,X84)
| p1(X84)
| ~ p100(X84) )
| ~ p1(X2) ) )
| ~ p100(X2) )
& ( p120(X2)
| ~ p121(X2) )
& ( p119(X2)
| ~ p120(X2) )
& ( p118(X2)
| ~ p119(X2) )
& ( p117(X2)
| ~ p118(X2) )
& ( p116(X2)
| ~ p117(X2) )
& ( p115(X2)
| ~ p116(X2) )
& ( p114(X2)
| ~ p115(X2) )
& ( p113(X2)
| ~ p114(X2) )
& ( p112(X2)
| ~ p113(X2) )
& ( p111(X2)
| ~ p112(X2) )
& ( p110(X2)
| ~ p111(X2) )
& ( p109(X2)
| ~ p110(X2) )
& ( p108(X2)
| ~ p109(X2) )
& ( p107(X2)
| ~ p108(X2) )
& ( p106(X2)
| ~ p107(X2) )
& ( p105(X2)
| ~ p106(X2) )
& ( p104(X2)
| ~ p105(X2) )
& ( p103(X2)
| ~ p104(X2) )
& ( p102(X2)
| ~ p103(X2) )
& ( p101(X2)
| ~ p102(X2) )
& ( p100(X2)
| ~ p101(X2) ) ) )
& ~ p101(X0)
& p100(X0) ) ),
inference(flattening,[],[f5]) ).
fof(f7,plain,
! [X0,X1,X2] :
( r1(X0,X2)
| ~ r1(X0,X1)
| ~ r1(X1,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f8,plain,
! [X0,X1,X2] :
( r1(X0,X2)
| ~ r1(X0,X1)
| ~ r1(X1,X2) ),
inference(flattening,[],[f7]) ).
fof(f9,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| p8(X1) )
& ! [X2] :
( ~ r1(X0,X2)
| ( ( ( ? [X3] :
( r1(X2,X3)
& ~ p21(X3)
& ~ p121(X3)
& p120(X3) )
& ? [X4] :
( r1(X2,X4)
& p21(X4)
& ~ p121(X4)
& p120(X4) ) )
| p120(X2)
| ~ p119(X2) )
& ( ( ? [X5] :
( r1(X2,X5)
& ~ p20(X5)
& ~ p120(X5)
& p119(X5) )
& ? [X6] :
( r1(X2,X6)
& p20(X6)
& ~ p120(X6)
& p119(X6) ) )
| p119(X2)
| ~ p118(X2) )
& ( ( ? [X7] :
( r1(X2,X7)
& ~ p19(X7)
& ~ p119(X7)
& p118(X7) )
& ? [X8] :
( r1(X2,X8)
& p19(X8)
& ~ p119(X8)
& p118(X8) ) )
| p118(X2)
| ~ p117(X2) )
& ( ( ? [X9] :
( r1(X2,X9)
& ~ p18(X9)
& ~ p118(X9)
& p117(X9) )
& ? [X10] :
( r1(X2,X10)
& p18(X10)
& ~ p118(X10)
& p117(X10) ) )
| p117(X2)
| ~ p116(X2) )
& ( ( ? [X11] :
( r1(X2,X11)
& ~ p17(X11)
& ~ p117(X11)
& p116(X11) )
& ? [X12] :
( r1(X2,X12)
& p17(X12)
& ~ p117(X12)
& p116(X12) ) )
| p116(X2)
| ~ p115(X2) )
& ( ( ? [X13] :
( r1(X2,X13)
& ~ p16(X13)
& ~ p116(X13)
& p115(X13) )
& ? [X14] :
( r1(X2,X14)
& p16(X14)
& ~ p116(X14)
& p115(X14) ) )
| p115(X2)
| ~ p114(X2) )
& ( ( ? [X15] :
( r1(X2,X15)
& ~ p15(X15)
& ~ p115(X15)
& p114(X15) )
& ? [X16] :
( r1(X2,X16)
& p15(X16)
& ~ p115(X16)
& p114(X16) ) )
| p114(X2)
| ~ p113(X2) )
& ( ( ? [X17] :
( r1(X2,X17)
& ~ p14(X17)
& ~ p114(X17)
& p113(X17) )
& ? [X18] :
( r1(X2,X18)
& p14(X18)
& ~ p114(X18)
& p113(X18) ) )
| p113(X2)
| ~ p112(X2) )
& ( ( ? [X19] :
( r1(X2,X19)
& ~ p13(X19)
& ~ p113(X19)
& p112(X19) )
& ? [X20] :
( r1(X2,X20)
& p13(X20)
& ~ p113(X20)
& p112(X20) ) )
| p112(X2)
| ~ p111(X2) )
& ( ( ? [X21] :
( r1(X2,X21)
& ~ p12(X21)
& ~ p112(X21)
& p111(X21) )
& ? [X22] :
( r1(X2,X22)
& p12(X22)
& ~ p112(X22)
& p111(X22) ) )
| p111(X2)
| ~ p110(X2) )
& ( ( ? [X23] :
( r1(X2,X23)
& ~ p11(X23)
& ~ p111(X23)
& p110(X23) )
& ? [X24] :
( r1(X2,X24)
& p11(X24)
& ~ p111(X24)
& p110(X24) ) )
| p110(X2)
| ~ p109(X2) )
& ( ( ? [X25] :
( r1(X2,X25)
& ~ p10(X25)
& ~ p110(X25)
& p109(X25) )
& ? [X26] :
( r1(X2,X26)
& p10(X26)
& ~ p110(X26)
& p109(X26) ) )
| p109(X2)
| ~ p108(X2) )
& ( ( ? [X27] :
( r1(X2,X27)
& ~ p9(X27)
& ~ p109(X27)
& p108(X27) )
& ? [X28] :
( r1(X2,X28)
& p9(X28)
& ~ p109(X28)
& p108(X28) ) )
| p108(X2)
| ~ p107(X2) )
& ( ( ? [X29] :
( r1(X2,X29)
& ~ p8(X29)
& ~ p108(X29)
& p107(X29) )
& ? [X30] :
( r1(X2,X30)
& p8(X30)
& ~ p108(X30)
& p107(X30) ) )
| p107(X2)
| ~ p106(X2) )
& ( ( ? [X31] :
( r1(X2,X31)
& ~ p7(X31)
& ~ p107(X31)
& p106(X31) )
& ? [X32] :
( r1(X2,X32)
& p7(X32)
& ~ p107(X32)
& p106(X32) ) )
| p106(X2)
| ~ p105(X2) )
& ( ( ? [X33] :
( r1(X2,X33)
& ~ p6(X33)
& ~ p106(X33)
& p105(X33) )
& ? [X34] :
( r1(X2,X34)
& p6(X34)
& ~ p106(X34)
& p105(X34) ) )
| p105(X2)
| ~ p104(X2) )
& ( ( ? [X35] :
( r1(X2,X35)
& ~ p5(X35)
& ~ p105(X35)
& p104(X35) )
& ? [X36] :
( r1(X2,X36)
& p5(X36)
& ~ p105(X36)
& p104(X36) ) )
| p104(X2)
| ~ p103(X2) )
& ( ( ? [X37] :
( r1(X2,X37)
& ~ p4(X37)
& ~ p104(X37)
& p103(X37) )
& ? [X38] :
( r1(X2,X38)
& p4(X38)
& ~ p104(X38)
& p103(X38) ) )
| p103(X2)
| ~ p102(X2) )
& ( ( ? [X39] :
( r1(X2,X39)
& ~ p3(X39)
& ~ p103(X39)
& p102(X39) )
& ? [X40] :
( r1(X2,X40)
& p3(X40)
& ~ p103(X40)
& p102(X40) ) )
| p102(X2)
| ~ p101(X2) )
& ( ( ? [X41] :
( r1(X2,X41)
& ~ p2(X41)
& ~ p102(X41)
& p101(X41) )
& ? [X42] :
( r1(X2,X42)
& p2(X42)
& ~ p102(X42)
& p101(X42) ) )
| p101(X2)
| ~ p100(X2) )
& ( ( ( ! [X43] :
( ~ r1(X2,X43)
| ~ p21(X43)
| ~ p120(X43) )
| p21(X2) )
& ( ! [X44] :
( ~ r1(X2,X44)
| p21(X44)
| ~ p120(X44) )
| ~ p21(X2) ) )
| ~ p120(X2) )
& ( ( ( ! [X45] :
( ~ r1(X2,X45)
| ~ p20(X45)
| ~ p119(X45) )
| p20(X2) )
& ( ! [X46] :
( ~ r1(X2,X46)
| p20(X46)
| ~ p119(X46) )
| ~ p20(X2) ) )
| ~ p119(X2) )
& ( ( ( ! [X47] :
( ~ r1(X2,X47)
| ~ p19(X47)
| ~ p118(X47) )
| p19(X2) )
& ( ! [X48] :
( ~ r1(X2,X48)
| p19(X48)
| ~ p118(X48) )
| ~ p19(X2) ) )
| ~ p118(X2) )
& ( ( ( ! [X49] :
( ~ r1(X2,X49)
| ~ p18(X49)
| ~ p117(X49) )
| p18(X2) )
& ( ! [X50] :
( ~ r1(X2,X50)
| p18(X50)
| ~ p117(X50) )
| ~ p18(X2) ) )
| ~ p117(X2) )
& ( ( ( ! [X51] :
( ~ r1(X2,X51)
| ~ p17(X51)
| ~ p116(X51) )
| p17(X2) )
& ( ! [X52] :
( ~ r1(X2,X52)
| p17(X52)
| ~ p116(X52) )
| ~ p17(X2) ) )
| ~ p116(X2) )
& ( ( ( ! [X53] :
( ~ r1(X2,X53)
| ~ p16(X53)
| ~ p115(X53) )
| p16(X2) )
& ( ! [X54] :
( ~ r1(X2,X54)
| p16(X54)
| ~ p115(X54) )
| ~ p16(X2) ) )
| ~ p115(X2) )
& ( ( ( ! [X55] :
( ~ r1(X2,X55)
| ~ p15(X55)
| ~ p114(X55) )
| p15(X2) )
& ( ! [X56] :
( ~ r1(X2,X56)
| p15(X56)
| ~ p114(X56) )
| ~ p15(X2) ) )
| ~ p114(X2) )
& ( ( ( ! [X57] :
( ~ r1(X2,X57)
| ~ p14(X57)
| ~ p113(X57) )
| p14(X2) )
& ( ! [X58] :
( ~ r1(X2,X58)
| p14(X58)
| ~ p113(X58) )
| ~ p14(X2) ) )
| ~ p113(X2) )
& ( ( ( ! [X59] :
( ~ r1(X2,X59)
| ~ p13(X59)
| ~ p112(X59) )
| p13(X2) )
& ( ! [X60] :
( ~ r1(X2,X60)
| p13(X60)
| ~ p112(X60) )
| ~ p13(X2) ) )
| ~ p112(X2) )
& ( ( ( ! [X61] :
( ~ r1(X2,X61)
| ~ p12(X61)
| ~ p111(X61) )
| p12(X2) )
& ( ! [X62] :
( ~ r1(X2,X62)
| p12(X62)
| ~ p111(X62) )
| ~ p12(X2) ) )
| ~ p111(X2) )
& ( ( ( ! [X63] :
( ~ r1(X2,X63)
| ~ p11(X63)
| ~ p110(X63) )
| p11(X2) )
& ( ! [X64] :
( ~ r1(X2,X64)
| p11(X64)
| ~ p110(X64) )
| ~ p11(X2) ) )
| ~ p110(X2) )
& ( ( ( ! [X65] :
( ~ r1(X2,X65)
| ~ p10(X65)
| ~ p109(X65) )
| p10(X2) )
& ( ! [X66] :
( ~ r1(X2,X66)
| p10(X66)
| ~ p109(X66) )
| ~ p10(X2) ) )
| ~ p109(X2) )
& ( ( ( ! [X67] :
( ~ r1(X2,X67)
| ~ p9(X67)
| ~ p108(X67) )
| p9(X2) )
& ( ! [X68] :
( ~ r1(X2,X68)
| p9(X68)
| ~ p108(X68) )
| ~ p9(X2) ) )
| ~ p108(X2) )
& ( ( ( ! [X69] :
( ~ r1(X2,X69)
| ~ p8(X69)
| ~ p107(X69) )
| p8(X2) )
& ( ! [X70] :
( ~ r1(X2,X70)
| p8(X70)
| ~ p107(X70) )
| ~ p8(X2) ) )
| ~ p107(X2) )
& ( ( ( ! [X71] :
( ~ r1(X2,X71)
| ~ p7(X71)
| ~ p106(X71) )
| p7(X2) )
& ( ! [X72] :
( ~ r1(X2,X72)
| p7(X72)
| ~ p106(X72) )
| ~ p7(X2) ) )
| ~ p106(X2) )
& ( ( ( ! [X73] :
( ~ r1(X2,X73)
| ~ p6(X73)
| ~ p105(X73) )
| p6(X2) )
& ( ! [X74] :
( ~ r1(X2,X74)
| p6(X74)
| ~ p105(X74) )
| ~ p6(X2) ) )
| ~ p105(X2) )
& ( ( ( ! [X75] :
( ~ r1(X2,X75)
| ~ p5(X75)
| ~ p104(X75) )
| p5(X2) )
& ( ! [X76] :
( ~ r1(X2,X76)
| p5(X76)
| ~ p104(X76) )
| ~ p5(X2) ) )
| ~ p104(X2) )
& ( ( ( ! [X77] :
( ~ r1(X2,X77)
| ~ p4(X77)
| ~ p103(X77) )
| p4(X2) )
& ( ! [X78] :
( ~ r1(X2,X78)
| p4(X78)
| ~ p103(X78) )
| ~ p4(X2) ) )
| ~ p103(X2) )
& ( ( ( ! [X79] :
( ~ r1(X2,X79)
| ~ p3(X79)
| ~ p102(X79) )
| p3(X2) )
& ( ! [X80] :
( ~ r1(X2,X80)
| p3(X80)
| ~ p102(X80) )
| ~ p3(X2) ) )
| ~ p102(X2) )
& ( ( ( ! [X81] :
( ~ r1(X2,X81)
| ~ p2(X81)
| ~ p101(X81) )
| p2(X2) )
& ( ! [X82] :
( ~ r1(X2,X82)
| p2(X82)
| ~ p101(X82) )
| ~ p2(X2) ) )
| ~ p101(X2) )
& ( ( ( ! [X83] :
( ~ r1(X2,X83)
| ~ p1(X83)
| ~ p100(X83) )
| p1(X2) )
& ( ! [X84] :
( ~ r1(X2,X84)
| p1(X84)
| ~ p100(X84) )
| ~ p1(X2) ) )
| ~ p100(X2) )
& ( p120(X2)
| ~ p121(X2) )
& ( p119(X2)
| ~ p120(X2) )
& ( p118(X2)
| ~ p119(X2) )
& ( p117(X2)
| ~ p118(X2) )
& ( p116(X2)
| ~ p117(X2) )
& ( p115(X2)
| ~ p116(X2) )
& ( p114(X2)
| ~ p115(X2) )
& ( p113(X2)
| ~ p114(X2) )
& ( p112(X2)
| ~ p113(X2) )
& ( p111(X2)
| ~ p112(X2) )
& ( p110(X2)
| ~ p111(X2) )
& ( p109(X2)
| ~ p110(X2) )
& ( p108(X2)
| ~ p109(X2) )
& ( p107(X2)
| ~ p108(X2) )
& ( p106(X2)
| ~ p107(X2) )
& ( p105(X2)
| ~ p106(X2) )
& ( p104(X2)
| ~ p105(X2) )
& ( p103(X2)
| ~ p104(X2) )
& ( p102(X2)
| ~ p103(X2) )
& ( p101(X2)
| ~ p102(X2) )
& ( p100(X2)
| ~ p101(X2) ) ) )
& ~ p101(X0)
& p100(X0) ),
inference(ennf_transformation,[],[f6]) ).
fof(f10,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| p8(X1) )
& ! [X2] :
( ~ r1(X0,X2)
| ( ( ( ? [X3] :
( r1(X2,X3)
& ~ p21(X3)
& ~ p121(X3)
& p120(X3) )
& ? [X4] :
( r1(X2,X4)
& p21(X4)
& ~ p121(X4)
& p120(X4) ) )
| p120(X2)
| ~ p119(X2) )
& ( ( ? [X5] :
( r1(X2,X5)
& ~ p20(X5)
& ~ p120(X5)
& p119(X5) )
& ? [X6] :
( r1(X2,X6)
& p20(X6)
& ~ p120(X6)
& p119(X6) ) )
| p119(X2)
| ~ p118(X2) )
& ( ( ? [X7] :
( r1(X2,X7)
& ~ p19(X7)
& ~ p119(X7)
& p118(X7) )
& ? [X8] :
( r1(X2,X8)
& p19(X8)
& ~ p119(X8)
& p118(X8) ) )
| p118(X2)
| ~ p117(X2) )
& ( ( ? [X9] :
( r1(X2,X9)
& ~ p18(X9)
& ~ p118(X9)
& p117(X9) )
& ? [X10] :
( r1(X2,X10)
& p18(X10)
& ~ p118(X10)
& p117(X10) ) )
| p117(X2)
| ~ p116(X2) )
& ( ( ? [X11] :
( r1(X2,X11)
& ~ p17(X11)
& ~ p117(X11)
& p116(X11) )
& ? [X12] :
( r1(X2,X12)
& p17(X12)
& ~ p117(X12)
& p116(X12) ) )
| p116(X2)
| ~ p115(X2) )
& ( ( ? [X13] :
( r1(X2,X13)
& ~ p16(X13)
& ~ p116(X13)
& p115(X13) )
& ? [X14] :
( r1(X2,X14)
& p16(X14)
& ~ p116(X14)
& p115(X14) ) )
| p115(X2)
| ~ p114(X2) )
& ( ( ? [X15] :
( r1(X2,X15)
& ~ p15(X15)
& ~ p115(X15)
& p114(X15) )
& ? [X16] :
( r1(X2,X16)
& p15(X16)
& ~ p115(X16)
& p114(X16) ) )
| p114(X2)
| ~ p113(X2) )
& ( ( ? [X17] :
( r1(X2,X17)
& ~ p14(X17)
& ~ p114(X17)
& p113(X17) )
& ? [X18] :
( r1(X2,X18)
& p14(X18)
& ~ p114(X18)
& p113(X18) ) )
| p113(X2)
| ~ p112(X2) )
& ( ( ? [X19] :
( r1(X2,X19)
& ~ p13(X19)
& ~ p113(X19)
& p112(X19) )
& ? [X20] :
( r1(X2,X20)
& p13(X20)
& ~ p113(X20)
& p112(X20) ) )
| p112(X2)
| ~ p111(X2) )
& ( ( ? [X21] :
( r1(X2,X21)
& ~ p12(X21)
& ~ p112(X21)
& p111(X21) )
& ? [X22] :
( r1(X2,X22)
& p12(X22)
& ~ p112(X22)
& p111(X22) ) )
| p111(X2)
| ~ p110(X2) )
& ( ( ? [X23] :
( r1(X2,X23)
& ~ p11(X23)
& ~ p111(X23)
& p110(X23) )
& ? [X24] :
( r1(X2,X24)
& p11(X24)
& ~ p111(X24)
& p110(X24) ) )
| p110(X2)
| ~ p109(X2) )
& ( ( ? [X25] :
( r1(X2,X25)
& ~ p10(X25)
& ~ p110(X25)
& p109(X25) )
& ? [X26] :
( r1(X2,X26)
& p10(X26)
& ~ p110(X26)
& p109(X26) ) )
| p109(X2)
| ~ p108(X2) )
& ( ( ? [X27] :
( r1(X2,X27)
& ~ p9(X27)
& ~ p109(X27)
& p108(X27) )
& ? [X28] :
( r1(X2,X28)
& p9(X28)
& ~ p109(X28)
& p108(X28) ) )
| p108(X2)
| ~ p107(X2) )
& ( ( ? [X29] :
( r1(X2,X29)
& ~ p8(X29)
& ~ p108(X29)
& p107(X29) )
& ? [X30] :
( r1(X2,X30)
& p8(X30)
& ~ p108(X30)
& p107(X30) ) )
| p107(X2)
| ~ p106(X2) )
& ( ( ? [X31] :
( r1(X2,X31)
& ~ p7(X31)
& ~ p107(X31)
& p106(X31) )
& ? [X32] :
( r1(X2,X32)
& p7(X32)
& ~ p107(X32)
& p106(X32) ) )
| p106(X2)
| ~ p105(X2) )
& ( ( ? [X33] :
( r1(X2,X33)
& ~ p6(X33)
& ~ p106(X33)
& p105(X33) )
& ? [X34] :
( r1(X2,X34)
& p6(X34)
& ~ p106(X34)
& p105(X34) ) )
| p105(X2)
| ~ p104(X2) )
& ( ( ? [X35] :
( r1(X2,X35)
& ~ p5(X35)
& ~ p105(X35)
& p104(X35) )
& ? [X36] :
( r1(X2,X36)
& p5(X36)
& ~ p105(X36)
& p104(X36) ) )
| p104(X2)
| ~ p103(X2) )
& ( ( ? [X37] :
( r1(X2,X37)
& ~ p4(X37)
& ~ p104(X37)
& p103(X37) )
& ? [X38] :
( r1(X2,X38)
& p4(X38)
& ~ p104(X38)
& p103(X38) ) )
| p103(X2)
| ~ p102(X2) )
& ( ( ? [X39] :
( r1(X2,X39)
& ~ p3(X39)
& ~ p103(X39)
& p102(X39) )
& ? [X40] :
( r1(X2,X40)
& p3(X40)
& ~ p103(X40)
& p102(X40) ) )
| p102(X2)
| ~ p101(X2) )
& ( ( ? [X41] :
( r1(X2,X41)
& ~ p2(X41)
& ~ p102(X41)
& p101(X41) )
& ? [X42] :
( r1(X2,X42)
& p2(X42)
& ~ p102(X42)
& p101(X42) ) )
| p101(X2)
| ~ p100(X2) )
& ( ( ( ! [X43] :
( ~ r1(X2,X43)
| ~ p21(X43)
| ~ p120(X43) )
| p21(X2) )
& ( ! [X44] :
( ~ r1(X2,X44)
| p21(X44)
| ~ p120(X44) )
| ~ p21(X2) ) )
| ~ p120(X2) )
& ( ( ( ! [X45] :
( ~ r1(X2,X45)
| ~ p20(X45)
| ~ p119(X45) )
| p20(X2) )
& ( ! [X46] :
( ~ r1(X2,X46)
| p20(X46)
| ~ p119(X46) )
| ~ p20(X2) ) )
| ~ p119(X2) )
& ( ( ( ! [X47] :
( ~ r1(X2,X47)
| ~ p19(X47)
| ~ p118(X47) )
| p19(X2) )
& ( ! [X48] :
( ~ r1(X2,X48)
| p19(X48)
| ~ p118(X48) )
| ~ p19(X2) ) )
| ~ p118(X2) )
& ( ( ( ! [X49] :
( ~ r1(X2,X49)
| ~ p18(X49)
| ~ p117(X49) )
| p18(X2) )
& ( ! [X50] :
( ~ r1(X2,X50)
| p18(X50)
| ~ p117(X50) )
| ~ p18(X2) ) )
| ~ p117(X2) )
& ( ( ( ! [X51] :
( ~ r1(X2,X51)
| ~ p17(X51)
| ~ p116(X51) )
| p17(X2) )
& ( ! [X52] :
( ~ r1(X2,X52)
| p17(X52)
| ~ p116(X52) )
| ~ p17(X2) ) )
| ~ p116(X2) )
& ( ( ( ! [X53] :
( ~ r1(X2,X53)
| ~ p16(X53)
| ~ p115(X53) )
| p16(X2) )
& ( ! [X54] :
( ~ r1(X2,X54)
| p16(X54)
| ~ p115(X54) )
| ~ p16(X2) ) )
| ~ p115(X2) )
& ( ( ( ! [X55] :
( ~ r1(X2,X55)
| ~ p15(X55)
| ~ p114(X55) )
| p15(X2) )
& ( ! [X56] :
( ~ r1(X2,X56)
| p15(X56)
| ~ p114(X56) )
| ~ p15(X2) ) )
| ~ p114(X2) )
& ( ( ( ! [X57] :
( ~ r1(X2,X57)
| ~ p14(X57)
| ~ p113(X57) )
| p14(X2) )
& ( ! [X58] :
( ~ r1(X2,X58)
| p14(X58)
| ~ p113(X58) )
| ~ p14(X2) ) )
| ~ p113(X2) )
& ( ( ( ! [X59] :
( ~ r1(X2,X59)
| ~ p13(X59)
| ~ p112(X59) )
| p13(X2) )
& ( ! [X60] :
( ~ r1(X2,X60)
| p13(X60)
| ~ p112(X60) )
| ~ p13(X2) ) )
| ~ p112(X2) )
& ( ( ( ! [X61] :
( ~ r1(X2,X61)
| ~ p12(X61)
| ~ p111(X61) )
| p12(X2) )
& ( ! [X62] :
( ~ r1(X2,X62)
| p12(X62)
| ~ p111(X62) )
| ~ p12(X2) ) )
| ~ p111(X2) )
& ( ( ( ! [X63] :
( ~ r1(X2,X63)
| ~ p11(X63)
| ~ p110(X63) )
| p11(X2) )
& ( ! [X64] :
( ~ r1(X2,X64)
| p11(X64)
| ~ p110(X64) )
| ~ p11(X2) ) )
| ~ p110(X2) )
& ( ( ( ! [X65] :
( ~ r1(X2,X65)
| ~ p10(X65)
| ~ p109(X65) )
| p10(X2) )
& ( ! [X66] :
( ~ r1(X2,X66)
| p10(X66)
| ~ p109(X66) )
| ~ p10(X2) ) )
| ~ p109(X2) )
& ( ( ( ! [X67] :
( ~ r1(X2,X67)
| ~ p9(X67)
| ~ p108(X67) )
| p9(X2) )
& ( ! [X68] :
( ~ r1(X2,X68)
| p9(X68)
| ~ p108(X68) )
| ~ p9(X2) ) )
| ~ p108(X2) )
& ( ( ( ! [X69] :
( ~ r1(X2,X69)
| ~ p8(X69)
| ~ p107(X69) )
| p8(X2) )
& ( ! [X70] :
( ~ r1(X2,X70)
| p8(X70)
| ~ p107(X70) )
| ~ p8(X2) ) )
| ~ p107(X2) )
& ( ( ( ! [X71] :
( ~ r1(X2,X71)
| ~ p7(X71)
| ~ p106(X71) )
| p7(X2) )
& ( ! [X72] :
( ~ r1(X2,X72)
| p7(X72)
| ~ p106(X72) )
| ~ p7(X2) ) )
| ~ p106(X2) )
& ( ( ( ! [X73] :
( ~ r1(X2,X73)
| ~ p6(X73)
| ~ p105(X73) )
| p6(X2) )
& ( ! [X74] :
( ~ r1(X2,X74)
| p6(X74)
| ~ p105(X74) )
| ~ p6(X2) ) )
| ~ p105(X2) )
& ( ( ( ! [X75] :
( ~ r1(X2,X75)
| ~ p5(X75)
| ~ p104(X75) )
| p5(X2) )
& ( ! [X76] :
( ~ r1(X2,X76)
| p5(X76)
| ~ p104(X76) )
| ~ p5(X2) ) )
| ~ p104(X2) )
& ( ( ( ! [X77] :
( ~ r1(X2,X77)
| ~ p4(X77)
| ~ p103(X77) )
| p4(X2) )
& ( ! [X78] :
( ~ r1(X2,X78)
| p4(X78)
| ~ p103(X78) )
| ~ p4(X2) ) )
| ~ p103(X2) )
& ( ( ( ! [X79] :
( ~ r1(X2,X79)
| ~ p3(X79)
| ~ p102(X79) )
| p3(X2) )
& ( ! [X80] :
( ~ r1(X2,X80)
| p3(X80)
| ~ p102(X80) )
| ~ p3(X2) ) )
| ~ p102(X2) )
& ( ( ( ! [X81] :
( ~ r1(X2,X81)
| ~ p2(X81)
| ~ p101(X81) )
| p2(X2) )
& ( ! [X82] :
( ~ r1(X2,X82)
| p2(X82)
| ~ p101(X82) )
| ~ p2(X2) ) )
| ~ p101(X2) )
& ( ( ( ! [X83] :
( ~ r1(X2,X83)
| ~ p1(X83)
| ~ p100(X83) )
| p1(X2) )
& ( ! [X84] :
( ~ r1(X2,X84)
| p1(X84)
| ~ p100(X84) )
| ~ p1(X2) ) )
| ~ p100(X2) )
& ( p120(X2)
| ~ p121(X2) )
& ( p119(X2)
| ~ p120(X2) )
& ( p118(X2)
| ~ p119(X2) )
& ( p117(X2)
| ~ p118(X2) )
& ( p116(X2)
| ~ p117(X2) )
& ( p115(X2)
| ~ p116(X2) )
& ( p114(X2)
| ~ p115(X2) )
& ( p113(X2)
| ~ p114(X2) )
& ( p112(X2)
| ~ p113(X2) )
& ( p111(X2)
| ~ p112(X2) )
& ( p110(X2)
| ~ p111(X2) )
& ( p109(X2)
| ~ p110(X2) )
& ( p108(X2)
| ~ p109(X2) )
& ( p107(X2)
| ~ p108(X2) )
& ( p106(X2)
| ~ p107(X2) )
& ( p105(X2)
| ~ p106(X2) )
& ( p104(X2)
| ~ p105(X2) )
& ( p103(X2)
| ~ p104(X2) )
& ( p102(X2)
| ~ p103(X2) )
& ( p101(X2)
| ~ p102(X2) )
& ( p100(X2)
| ~ p101(X2) ) ) )
& ~ p101(X0)
& p100(X0) ),
inference(flattening,[],[f9]) ).
fof(f11,definition,
! [X2] :
( ( ? [X41] :
( r1(X2,X41)
& ~ p2(X41)
& ~ p102(X41)
& p101(X41) )
& ? [X42] :
( r1(X2,X42)
& p2(X42)
& ~ p102(X42)
& p101(X42) ) )
| p101(X2)
| ~ p100(X2)
| ~ sP0(X2) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f12,definition,
! [X2] :
( ( ? [X39] :
( r1(X2,X39)
& ~ p3(X39)
& ~ p103(X39)
& p102(X39) )
& ? [X40] :
( r1(X2,X40)
& p3(X40)
& ~ p103(X40)
& p102(X40) ) )
| p102(X2)
| ~ p101(X2)
| ~ sP1(X2) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f13,definition,
! [X2] :
( ( ? [X37] :
( r1(X2,X37)
& ~ p4(X37)
& ~ p104(X37)
& p103(X37) )
& ? [X38] :
( r1(X2,X38)
& p4(X38)
& ~ p104(X38)
& p103(X38) ) )
| p103(X2)
| ~ p102(X2)
| ~ sP2(X2) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f14,definition,
! [X2] :
( ( ? [X35] :
( r1(X2,X35)
& ~ p5(X35)
& ~ p105(X35)
& p104(X35) )
& ? [X36] :
( r1(X2,X36)
& p5(X36)
& ~ p105(X36)
& p104(X36) ) )
| p104(X2)
| ~ p103(X2)
| ~ sP3(X2) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f15,definition,
! [X2] :
( ( ? [X33] :
( r1(X2,X33)
& ~ p6(X33)
& ~ p106(X33)
& p105(X33) )
& ? [X34] :
( r1(X2,X34)
& p6(X34)
& ~ p106(X34)
& p105(X34) ) )
| p105(X2)
| ~ p104(X2)
| ~ sP4(X2) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f16,definition,
! [X2] :
( ( ? [X31] :
( r1(X2,X31)
& ~ p7(X31)
& ~ p107(X31)
& p106(X31) )
& ? [X32] :
( r1(X2,X32)
& p7(X32)
& ~ p107(X32)
& p106(X32) ) )
| p106(X2)
| ~ p105(X2)
| ~ sP5(X2) ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f17,definition,
! [X2] :
( ( ? [X29] :
( r1(X2,X29)
& ~ p8(X29)
& ~ p108(X29)
& p107(X29) )
& ? [X30] :
( r1(X2,X30)
& p8(X30)
& ~ p108(X30)
& p107(X30) ) )
| p107(X2)
| ~ p106(X2)
| ~ sP6(X2) ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f18,definition,
! [X2] :
( ( ? [X27] :
( r1(X2,X27)
& ~ p9(X27)
& ~ p109(X27)
& p108(X27) )
& ? [X28] :
( r1(X2,X28)
& p9(X28)
& ~ p109(X28)
& p108(X28) ) )
| p108(X2)
| ~ p107(X2)
| ~ sP7(X2) ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f19,definition,
! [X2] :
( ( ? [X25] :
( r1(X2,X25)
& ~ p10(X25)
& ~ p110(X25)
& p109(X25) )
& ? [X26] :
( r1(X2,X26)
& p10(X26)
& ~ p110(X26)
& p109(X26) ) )
| p109(X2)
| ~ p108(X2)
| ~ sP8(X2) ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f20,definition,
! [X2] :
( ( ? [X23] :
( r1(X2,X23)
& ~ p11(X23)
& ~ p111(X23)
& p110(X23) )
& ? [X24] :
( r1(X2,X24)
& p11(X24)
& ~ p111(X24)
& p110(X24) ) )
| p110(X2)
| ~ p109(X2)
| ~ sP9(X2) ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f21,definition,
! [X2] :
( ( ? [X21] :
( r1(X2,X21)
& ~ p12(X21)
& ~ p112(X21)
& p111(X21) )
& ? [X22] :
( r1(X2,X22)
& p12(X22)
& ~ p112(X22)
& p111(X22) ) )
| p111(X2)
| ~ p110(X2)
| ~ sP10(X2) ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f22,definition,
! [X2] :
( ( ? [X19] :
( r1(X2,X19)
& ~ p13(X19)
& ~ p113(X19)
& p112(X19) )
& ? [X20] :
( r1(X2,X20)
& p13(X20)
& ~ p113(X20)
& p112(X20) ) )
| p112(X2)
| ~ p111(X2)
| ~ sP11(X2) ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f23,definition,
! [X2] :
( ( ? [X17] :
( r1(X2,X17)
& ~ p14(X17)
& ~ p114(X17)
& p113(X17) )
& ? [X18] :
( r1(X2,X18)
& p14(X18)
& ~ p114(X18)
& p113(X18) ) )
| p113(X2)
| ~ p112(X2)
| ~ sP12(X2) ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f24,definition,
! [X2] :
( ( ? [X15] :
( r1(X2,X15)
& ~ p15(X15)
& ~ p115(X15)
& p114(X15) )
& ? [X16] :
( r1(X2,X16)
& p15(X16)
& ~ p115(X16)
& p114(X16) ) )
| p114(X2)
| ~ p113(X2)
| ~ sP13(X2) ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f25,definition,
! [X2] :
( ( ? [X13] :
( r1(X2,X13)
& ~ p16(X13)
& ~ p116(X13)
& p115(X13) )
& ? [X14] :
( r1(X2,X14)
& p16(X14)
& ~ p116(X14)
& p115(X14) ) )
| p115(X2)
| ~ p114(X2)
| ~ sP14(X2) ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f26,definition,
! [X2] :
( ( ? [X11] :
( r1(X2,X11)
& ~ p17(X11)
& ~ p117(X11)
& p116(X11) )
& ? [X12] :
( r1(X2,X12)
& p17(X12)
& ~ p117(X12)
& p116(X12) ) )
| p116(X2)
| ~ p115(X2)
| ~ sP15(X2) ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f27,definition,
! [X2] :
( ( ? [X9] :
( r1(X2,X9)
& ~ p18(X9)
& ~ p118(X9)
& p117(X9) )
& ? [X10] :
( r1(X2,X10)
& p18(X10)
& ~ p118(X10)
& p117(X10) ) )
| p117(X2)
| ~ p116(X2)
| ~ sP16(X2) ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f28,definition,
! [X2] :
( ( ? [X7] :
( r1(X2,X7)
& ~ p19(X7)
& ~ p119(X7)
& p118(X7) )
& ? [X8] :
( r1(X2,X8)
& p19(X8)
& ~ p119(X8)
& p118(X8) ) )
| p118(X2)
| ~ p117(X2)
| ~ sP17(X2) ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f29,definition,
! [X2] :
( ( ? [X5] :
( r1(X2,X5)
& ~ p20(X5)
& ~ p120(X5)
& p119(X5) )
& ? [X6] :
( r1(X2,X6)
& p20(X6)
& ~ p120(X6)
& p119(X6) ) )
| p119(X2)
| ~ p118(X2)
| ~ sP18(X2) ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f30,definition,
! [X2] :
( ( ? [X3] :
( r1(X2,X3)
& ~ p21(X3)
& ~ p121(X3)
& p120(X3) )
& ? [X4] :
( r1(X2,X4)
& p21(X4)
& ~ p121(X4)
& p120(X4) ) )
| p120(X2)
| ~ p119(X2)
| ~ sP19(X2) ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f31,definition,
! [X2] :
( ( ( ! [X83] :
( ~ r1(X2,X83)
| ~ p1(X83)
| ~ p100(X83) )
| p1(X2) )
& ( ! [X84] :
( ~ r1(X2,X84)
| p1(X84)
| ~ p100(X84) )
| ~ p1(X2) ) )
| ~ p100(X2)
| ~ sP20(X2) ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f32,definition,
! [X2] :
( ( ( ! [X81] :
( ~ r1(X2,X81)
| ~ p2(X81)
| ~ p101(X81) )
| p2(X2) )
& ( ! [X82] :
( ~ r1(X2,X82)
| p2(X82)
| ~ p101(X82) )
| ~ p2(X2) ) )
| ~ p101(X2)
| ~ sP21(X2) ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f33,definition,
! [X2] :
( ( ( ! [X79] :
( ~ r1(X2,X79)
| ~ p3(X79)
| ~ p102(X79) )
| p3(X2) )
& ( ! [X80] :
( ~ r1(X2,X80)
| p3(X80)
| ~ p102(X80) )
| ~ p3(X2) ) )
| ~ p102(X2)
| ~ sP22(X2) ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f34,definition,
! [X2] :
( ( ( ! [X77] :
( ~ r1(X2,X77)
| ~ p4(X77)
| ~ p103(X77) )
| p4(X2) )
& ( ! [X78] :
( ~ r1(X2,X78)
| p4(X78)
| ~ p103(X78) )
| ~ p4(X2) ) )
| ~ p103(X2)
| ~ sP23(X2) ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f35,definition,
! [X2] :
( ( ( ! [X75] :
( ~ r1(X2,X75)
| ~ p5(X75)
| ~ p104(X75) )
| p5(X2) )
& ( ! [X76] :
( ~ r1(X2,X76)
| p5(X76)
| ~ p104(X76) )
| ~ p5(X2) ) )
| ~ p104(X2)
| ~ sP24(X2) ),
introduced(definition,[new_symbols(definition,[sP24])],[predicate_definition_introduction]) ).
fof(f36,definition,
! [X2] :
( ( ( ! [X73] :
( ~ r1(X2,X73)
| ~ p6(X73)
| ~ p105(X73) )
| p6(X2) )
& ( ! [X74] :
( ~ r1(X2,X74)
| p6(X74)
| ~ p105(X74) )
| ~ p6(X2) ) )
| ~ p105(X2)
| ~ sP25(X2) ),
introduced(definition,[new_symbols(definition,[sP25])],[predicate_definition_introduction]) ).
fof(f37,definition,
! [X2] :
( ( ( ! [X71] :
( ~ r1(X2,X71)
| ~ p7(X71)
| ~ p106(X71) )
| p7(X2) )
& ( ! [X72] :
( ~ r1(X2,X72)
| p7(X72)
| ~ p106(X72) )
| ~ p7(X2) ) )
| ~ p106(X2)
| ~ sP26(X2) ),
introduced(definition,[new_symbols(definition,[sP26])],[predicate_definition_introduction]) ).
fof(f38,definition,
! [X2] :
( ( ( ! [X69] :
( ~ r1(X2,X69)
| ~ p8(X69)
| ~ p107(X69) )
| p8(X2) )
& ( ! [X70] :
( ~ r1(X2,X70)
| p8(X70)
| ~ p107(X70) )
| ~ p8(X2) ) )
| ~ p107(X2)
| ~ sP27(X2) ),
introduced(definition,[new_symbols(definition,[sP27])],[predicate_definition_introduction]) ).
fof(f39,definition,
! [X2] :
( ( ( ! [X67] :
( ~ r1(X2,X67)
| ~ p9(X67)
| ~ p108(X67) )
| p9(X2) )
& ( ! [X68] :
( ~ r1(X2,X68)
| p9(X68)
| ~ p108(X68) )
| ~ p9(X2) ) )
| ~ p108(X2)
| ~ sP28(X2) ),
introduced(definition,[new_symbols(definition,[sP28])],[predicate_definition_introduction]) ).
fof(f40,definition,
! [X2] :
( ( ( ! [X65] :
( ~ r1(X2,X65)
| ~ p10(X65)
| ~ p109(X65) )
| p10(X2) )
& ( ! [X66] :
( ~ r1(X2,X66)
| p10(X66)
| ~ p109(X66) )
| ~ p10(X2) ) )
| ~ p109(X2)
| ~ sP29(X2) ),
introduced(definition,[new_symbols(definition,[sP29])],[predicate_definition_introduction]) ).
fof(f41,definition,
! [X2] :
( ( ( ! [X63] :
( ~ r1(X2,X63)
| ~ p11(X63)
| ~ p110(X63) )
| p11(X2) )
& ( ! [X64] :
( ~ r1(X2,X64)
| p11(X64)
| ~ p110(X64) )
| ~ p11(X2) ) )
| ~ p110(X2)
| ~ sP30(X2) ),
introduced(definition,[new_symbols(definition,[sP30])],[predicate_definition_introduction]) ).
fof(f42,definition,
! [X2] :
( ( ( ! [X61] :
( ~ r1(X2,X61)
| ~ p12(X61)
| ~ p111(X61) )
| p12(X2) )
& ( ! [X62] :
( ~ r1(X2,X62)
| p12(X62)
| ~ p111(X62) )
| ~ p12(X2) ) )
| ~ p111(X2)
| ~ sP31(X2) ),
introduced(definition,[new_symbols(definition,[sP31])],[predicate_definition_introduction]) ).
fof(f43,definition,
! [X2] :
( ( ( ! [X59] :
( ~ r1(X2,X59)
| ~ p13(X59)
| ~ p112(X59) )
| p13(X2) )
& ( ! [X60] :
( ~ r1(X2,X60)
| p13(X60)
| ~ p112(X60) )
| ~ p13(X2) ) )
| ~ p112(X2)
| ~ sP32(X2) ),
introduced(definition,[new_symbols(definition,[sP32])],[predicate_definition_introduction]) ).
fof(f44,definition,
! [X2] :
( ( ( ! [X57] :
( ~ r1(X2,X57)
| ~ p14(X57)
| ~ p113(X57) )
| p14(X2) )
& ( ! [X58] :
( ~ r1(X2,X58)
| p14(X58)
| ~ p113(X58) )
| ~ p14(X2) ) )
| ~ p113(X2)
| ~ sP33(X2) ),
introduced(definition,[new_symbols(definition,[sP33])],[predicate_definition_introduction]) ).
fof(f45,definition,
! [X2] :
( ( ( ! [X55] :
( ~ r1(X2,X55)
| ~ p15(X55)
| ~ p114(X55) )
| p15(X2) )
& ( ! [X56] :
( ~ r1(X2,X56)
| p15(X56)
| ~ p114(X56) )
| ~ p15(X2) ) )
| ~ p114(X2)
| ~ sP34(X2) ),
introduced(definition,[new_symbols(definition,[sP34])],[predicate_definition_introduction]) ).
fof(f46,definition,
! [X2] :
( ( ( ! [X53] :
( ~ r1(X2,X53)
| ~ p16(X53)
| ~ p115(X53) )
| p16(X2) )
& ( ! [X54] :
( ~ r1(X2,X54)
| p16(X54)
| ~ p115(X54) )
| ~ p16(X2) ) )
| ~ p115(X2)
| ~ sP35(X2) ),
introduced(definition,[new_symbols(definition,[sP35])],[predicate_definition_introduction]) ).
fof(f47,definition,
! [X2] :
( ( ( ! [X51] :
( ~ r1(X2,X51)
| ~ p17(X51)
| ~ p116(X51) )
| p17(X2) )
& ( ! [X52] :
( ~ r1(X2,X52)
| p17(X52)
| ~ p116(X52) )
| ~ p17(X2) ) )
| ~ p116(X2)
| ~ sP36(X2) ),
introduced(definition,[new_symbols(definition,[sP36])],[predicate_definition_introduction]) ).
fof(f48,definition,
! [X2] :
( ( ( ! [X49] :
( ~ r1(X2,X49)
| ~ p18(X49)
| ~ p117(X49) )
| p18(X2) )
& ( ! [X50] :
( ~ r1(X2,X50)
| p18(X50)
| ~ p117(X50) )
| ~ p18(X2) ) )
| ~ p117(X2)
| ~ sP37(X2) ),
introduced(definition,[new_symbols(definition,[sP37])],[predicate_definition_introduction]) ).
fof(f49,definition,
! [X2] :
( ( ( ! [X47] :
( ~ r1(X2,X47)
| ~ p19(X47)
| ~ p118(X47) )
| p19(X2) )
& ( ! [X48] :
( ~ r1(X2,X48)
| p19(X48)
| ~ p118(X48) )
| ~ p19(X2) ) )
| ~ p118(X2)
| ~ sP38(X2) ),
introduced(definition,[new_symbols(definition,[sP38])],[predicate_definition_introduction]) ).
fof(f50,definition,
! [X2] :
( ( ( ! [X45] :
( ~ r1(X2,X45)
| ~ p20(X45)
| ~ p119(X45) )
| p20(X2) )
& ( ! [X46] :
( ~ r1(X2,X46)
| p20(X46)
| ~ p119(X46) )
| ~ p20(X2) ) )
| ~ p119(X2)
| ~ sP39(X2) ),
introduced(definition,[new_symbols(definition,[sP39])],[predicate_definition_introduction]) ).
fof(f51,definition,
! [X2] :
( ( ( ! [X43] :
( ~ r1(X2,X43)
| ~ p21(X43)
| ~ p120(X43) )
| p21(X2) )
& ( ! [X44] :
( ~ r1(X2,X44)
| p21(X44)
| ~ p120(X44) )
| ~ p21(X2) ) )
| ~ p120(X2)
| ~ sP40(X2) ),
introduced(definition,[new_symbols(definition,[sP40])],[predicate_definition_introduction]) ).
fof(f52,definition,
! [X2] :
( ( sP19(X2)
& sP18(X2)
& sP17(X2)
& sP16(X2)
& sP15(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)
& sP40(X2)
& sP39(X2)
& sP38(X2)
& sP37(X2)
& sP36(X2)
& sP35(X2)
& sP34(X2)
& sP33(X2)
& sP32(X2)
& sP31(X2)
& sP30(X2)
& sP29(X2)
& sP28(X2)
& sP27(X2)
& sP26(X2)
& sP25(X2)
& sP24(X2)
& sP23(X2)
& sP22(X2)
& sP21(X2)
& sP20(X2)
& ( p120(X2)
| ~ p121(X2) )
& ( p119(X2)
| ~ p120(X2) )
& ( p118(X2)
| ~ p119(X2) )
& ( p117(X2)
| ~ p118(X2) )
& ( p116(X2)
| ~ p117(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) ) )
| ~ sP41(X2) ),
introduced(definition,[new_symbols(definition,[sP41])],[predicate_definition_introduction]) ).
fof(f53,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| p8(X1) )
& ! [X2] :
( ~ r1(X0,X2)
| sP41(X2) )
& ~ p101(X0)
& p100(X0) ),
inference(definition_folding,[],[f10,f52,f51,f50,f49,f48,f47,f46,f45,f44,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,f11]) ).
fof(f54,plain,
! [X2] :
( ( sP19(X2)
& sP18(X2)
& sP17(X2)
& sP16(X2)
& sP15(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)
& sP40(X2)
& sP39(X2)
& sP38(X2)
& sP37(X2)
& sP36(X2)
& sP35(X2)
& sP34(X2)
& sP33(X2)
& sP32(X2)
& sP31(X2)
& sP30(X2)
& sP29(X2)
& sP28(X2)
& sP27(X2)
& sP26(X2)
& sP25(X2)
& sP24(X2)
& sP23(X2)
& sP22(X2)
& sP21(X2)
& sP20(X2)
& ( p120(X2)
| ~ p121(X2) )
& ( p119(X2)
| ~ p120(X2) )
& ( p118(X2)
| ~ p119(X2) )
& ( p117(X2)
| ~ p118(X2) )
& ( p116(X2)
| ~ p117(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) ) )
| ~ sP41(X2) ),
inference(nnf_transformation,[],[f52]) ).
fof(f55,plain,
! [X0] :
( ( sP19(X0)
& sP18(X0)
& sP17(X0)
& sP16(X0)
& sP15(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)
& sP40(X0)
& sP39(X0)
& sP38(X0)
& sP37(X0)
& sP36(X0)
& sP35(X0)
& sP34(X0)
& sP33(X0)
& sP32(X0)
& sP31(X0)
& sP30(X0)
& sP29(X0)
& sP28(X0)
& sP27(X0)
& sP26(X0)
& sP25(X0)
& sP24(X0)
& sP23(X0)
& sP22(X0)
& sP21(X0)
& sP20(X0)
& ( p120(X0)
| ~ p121(X0) )
& ( p119(X0)
| ~ p120(X0) )
& ( p118(X0)
| ~ p119(X0) )
& ( p117(X0)
| ~ p118(X0) )
& ( p116(X0)
| ~ p117(X0) )
& ( p115(X0)
| ~ p116(X0) )
& ( p114(X0)
| ~ p115(X0) )
& ( p113(X0)
| ~ p114(X0) )
& ( p112(X0)
| ~ p113(X0) )
& ( p111(X0)
| ~ p112(X0) )
& ( p110(X0)
| ~ p111(X0) )
& ( p109(X0)
| ~ p110(X0) )
& ( p108(X0)
| ~ p109(X0) )
& ( p107(X0)
| ~ p108(X0) )
& ( p106(X0)
| ~ p107(X0) )
& ( p105(X0)
| ~ p106(X0) )
& ( p104(X0)
| ~ p105(X0) )
& ( p103(X0)
| ~ p104(X0) )
& ( p102(X0)
| ~ p103(X0) )
& ( p101(X0)
| ~ p102(X0) )
& ( p100(X0)
| ~ p101(X0) ) )
| ~ sP41(X0) ),
inference(rectify,[],[f54]) ).
fof(f137,plain,
! [X2] :
( ( ? [X29] :
( r1(X2,X29)
& ~ p8(X29)
& ~ p108(X29)
& p107(X29) )
& ? [X30] :
( r1(X2,X30)
& p8(X30)
& ~ p108(X30)
& p107(X30) ) )
| p107(X2)
| ~ p106(X2)
| ~ sP6(X2) ),
inference(nnf_transformation,[],[f17]) ).
fof(f138,plain,
! [X0] :
( ( ? [X1] :
( r1(X0,X1)
& ~ p8(X1)
& ~ p108(X1)
& p107(X1) )
& ? [X2] :
( r1(X0,X2)
& p8(X2)
& ~ p108(X2)
& p107(X2) ) )
| p107(X0)
| ~ p106(X0)
| ~ sP6(X0) ),
inference(rectify,[],[f137]) ).
fof(f139,plain,
! [X0] :
( ( r1(X0,sK68(X0))
& ~ p8(sK68(X0))
& ~ p108(sK68(X0))
& p107(sK68(X0))
& r1(X0,sK69(X0))
& p8(sK69(X0))
& ~ p108(sK69(X0))
& p107(sK69(X0)) )
| p107(X0)
| ~ p106(X0)
| ~ sP6(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK68,sK69]),skolemize(X1,sK68(X0)),skolemize(X2,sK69(X0))],[f138]) ).
fof(f140,plain,
! [X2] :
( ( ? [X31] :
( r1(X2,X31)
& ~ p7(X31)
& ~ p107(X31)
& p106(X31) )
& ? [X32] :
( r1(X2,X32)
& p7(X32)
& ~ p107(X32)
& p106(X32) ) )
| p106(X2)
| ~ p105(X2)
| ~ sP5(X2) ),
inference(nnf_transformation,[],[f16]) ).
fof(f141,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,[],[f140]) ).
fof(f142,plain,
! [X0] :
( ( r1(X0,sK70(X0))
& ~ p7(sK70(X0))
& ~ p107(sK70(X0))
& p106(sK70(X0))
& r1(X0,sK71(X0))
& p7(sK71(X0))
& ~ p107(sK71(X0))
& p106(sK71(X0)) )
| p106(X0)
| ~ p105(X0)
| ~ sP5(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK70,sK71]),skolemize(X1,sK70(X0)),skolemize(X2,sK71(X0))],[f141]) ).
fof(f143,plain,
! [X2] :
( ( ? [X33] :
( r1(X2,X33)
& ~ p6(X33)
& ~ p106(X33)
& p105(X33) )
& ? [X34] :
( r1(X2,X34)
& p6(X34)
& ~ p106(X34)
& p105(X34) ) )
| p105(X2)
| ~ p104(X2)
| ~ sP4(X2) ),
inference(nnf_transformation,[],[f15]) ).
fof(f144,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,[],[f143]) ).
fof(f145,plain,
! [X0] :
( ( r1(X0,sK72(X0))
& ~ p6(sK72(X0))
& ~ p106(sK72(X0))
& p105(sK72(X0))
& r1(X0,sK73(X0))
& p6(sK73(X0))
& ~ p106(sK73(X0))
& p105(sK73(X0)) )
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK72,sK73]),skolemize(X1,sK72(X0)),skolemize(X2,sK73(X0))],[f144]) ).
fof(f146,plain,
! [X2] :
( ( ? [X35] :
( r1(X2,X35)
& ~ p5(X35)
& ~ p105(X35)
& p104(X35) )
& ? [X36] :
( r1(X2,X36)
& p5(X36)
& ~ p105(X36)
& p104(X36) ) )
| p104(X2)
| ~ p103(X2)
| ~ sP3(X2) ),
inference(nnf_transformation,[],[f14]) ).
fof(f147,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,[],[f146]) ).
fof(f148,plain,
! [X0] :
( ( r1(X0,sK74(X0))
& ~ p5(sK74(X0))
& ~ p105(sK74(X0))
& p104(sK74(X0))
& r1(X0,sK75(X0))
& p5(sK75(X0))
& ~ p105(sK75(X0))
& p104(sK75(X0)) )
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK74,sK75]),skolemize(X1,sK74(X0)),skolemize(X2,sK75(X0))],[f147]) ).
fof(f149,plain,
! [X2] :
( ( ? [X37] :
( r1(X2,X37)
& ~ p4(X37)
& ~ p104(X37)
& p103(X37) )
& ? [X38] :
( r1(X2,X38)
& p4(X38)
& ~ p104(X38)
& p103(X38) ) )
| p103(X2)
| ~ p102(X2)
| ~ sP2(X2) ),
inference(nnf_transformation,[],[f13]) ).
fof(f150,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,[],[f149]) ).
fof(f151,plain,
! [X0] :
( ( r1(X0,sK76(X0))
& ~ p4(sK76(X0))
& ~ p104(sK76(X0))
& p103(sK76(X0))
& r1(X0,sK77(X0))
& p4(sK77(X0))
& ~ p104(sK77(X0))
& p103(sK77(X0)) )
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK76,sK77]),skolemize(X1,sK76(X0)),skolemize(X2,sK77(X0))],[f150]) ).
fof(f152,plain,
! [X2] :
( ( ? [X39] :
( r1(X2,X39)
& ~ p3(X39)
& ~ p103(X39)
& p102(X39) )
& ? [X40] :
( r1(X2,X40)
& p3(X40)
& ~ p103(X40)
& p102(X40) ) )
| p102(X2)
| ~ p101(X2)
| ~ sP1(X2) ),
inference(nnf_transformation,[],[f12]) ).
fof(f153,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,[],[f152]) ).
fof(f154,plain,
! [X0] :
( ( r1(X0,sK78(X0))
& ~ p3(sK78(X0))
& ~ p103(sK78(X0))
& p102(sK78(X0))
& r1(X0,sK79(X0))
& p3(sK79(X0))
& ~ p103(sK79(X0))
& p102(sK79(X0)) )
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK78,sK79]),skolemize(X1,sK78(X0)),skolemize(X2,sK79(X0))],[f153]) ).
fof(f155,plain,
! [X2] :
( ( ? [X41] :
( r1(X2,X41)
& ~ p2(X41)
& ~ p102(X41)
& p101(X41) )
& ? [X42] :
( r1(X2,X42)
& p2(X42)
& ~ p102(X42)
& p101(X42) ) )
| p101(X2)
| ~ p100(X2)
| ~ sP0(X2) ),
inference(nnf_transformation,[],[f11]) ).
fof(f156,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,[],[f155]) ).
fof(f157,plain,
! [X0] :
( ( r1(X0,sK80(X0))
& ~ p2(sK80(X0))
& ~ p102(sK80(X0))
& p101(sK80(X0))
& r1(X0,sK81(X0))
& p2(sK81(X0))
& ~ p102(sK81(X0))
& p101(sK81(X0)) )
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK80,sK81]),skolemize(X1,sK80(X0)),skolemize(X2,sK81(X0))],[f156]) ).
fof(f158,plain,
( ! [X1] :
( ~ r1(sK82,X1)
| p8(X1) )
& ! [X2] :
( ~ r1(sK82,X2)
| sP41(X2) )
& ~ p101(sK82)
& p100(sK82) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK82]),skolemize(X0,sK82)],[f53]) ).
fof(f159,plain,
! [X0] : r1(X0,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f160,plain,
! [X2,X0,X1] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| r1(X0,X2) ),
inference(cnf_transformation,[],[f8]) ).
fof(f203,plain,
! [X0] :
( ~ sP41(X0)
| sP0(X0) ),
inference(cnf_transformation,[],[f55]) ).
fof(f204,plain,
! [X0] :
( sP1(X0)
| ~ sP41(X0) ),
inference(cnf_transformation,[],[f55]) ).
fof(f205,plain,
! [X0] :
( sP2(X0)
| ~ sP41(X0) ),
inference(cnf_transformation,[],[f55]) ).
fof(f206,plain,
! [X0] :
( sP3(X0)
| ~ sP41(X0) ),
inference(cnf_transformation,[],[f55]) ).
fof(f207,plain,
! [X0] :
( sP4(X0)
| ~ sP41(X0) ),
inference(cnf_transformation,[],[f55]) ).
fof(f208,plain,
! [X0] :
( sP5(X0)
| ~ sP41(X0) ),
inference(cnf_transformation,[],[f55]) ).
fof(f209,plain,
! [X0] :
( sP6(X0)
| ~ sP41(X0) ),
inference(cnf_transformation,[],[f55]) ).
fof(f375,plain,
! [X0] :
( ~ p8(sK68(X0))
| p107(X0)
| ~ p106(X0)
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f139]) ).
fof(f376,plain,
! [X0] :
( ~ p106(X0)
| p107(X0)
| r1(X0,sK68(X0))
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f139]) ).
fof(f377,plain,
! [X0] :
( ~ p105(X0)
| p106(X0)
| p106(sK71(X0))
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f142]) ).
fof(f378,plain,
! [X0] :
( ~ p107(sK71(X0))
| p106(X0)
| ~ p105(X0)
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f142]) ).
fof(f380,plain,
! [X0] :
( ~ p105(X0)
| p106(X0)
| r1(X0,sK71(X0))
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f142]) ).
fof(f385,plain,
! [X0] :
( ~ p104(X0)
| p105(X0)
| p105(sK73(X0))
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f145]) ).
fof(f386,plain,
! [X0] :
( ~ p106(sK73(X0))
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f145]) ).
fof(f388,plain,
! [X0] :
( ~ p104(X0)
| p105(X0)
| r1(X0,sK73(X0))
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f145]) ).
fof(f393,plain,
! [X0] :
( ~ sP3(X0)
| p104(X0)
| ~ p103(X0)
| p104(sK75(X0)) ),
inference(cnf_transformation,[],[f148]) ).
fof(f394,plain,
! [X0] :
( ~ p105(sK75(X0))
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f148]) ).
fof(f396,plain,
! [X0] :
( ~ p103(X0)
| p104(X0)
| r1(X0,sK75(X0))
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f148]) ).
fof(f401,plain,
! [X0] :
( ~ sP2(X0)
| p103(X0)
| ~ p102(X0)
| p103(sK77(X0)) ),
inference(cnf_transformation,[],[f151]) ).
fof(f402,plain,
! [X0] :
( ~ p104(sK77(X0))
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f151]) ).
fof(f404,plain,
! [X0] :
( ~ p102(X0)
| p103(X0)
| r1(X0,sK77(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f151]) ).
fof(f409,plain,
! [X0] :
( ~ sP1(X0)
| p102(X0)
| ~ p101(X0)
| p102(sK79(X0)) ),
inference(cnf_transformation,[],[f154]) ).
fof(f410,plain,
! [X0] :
( ~ p103(sK79(X0))
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f154]) ).
fof(f412,plain,
! [X0] :
( ~ sP1(X0)
| p102(X0)
| ~ p101(X0)
| r1(X0,sK79(X0)) ),
inference(cnf_transformation,[],[f154]) ).
fof(f417,plain,
! [X0] :
( p101(sK81(X0))
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f157]) ).
fof(f418,plain,
! [X0] :
( ~ p102(sK81(X0))
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f157]) ).
fof(f420,plain,
! [X0] :
( ~ sP0(X0)
| p101(X0)
| ~ p100(X0)
| r1(X0,sK81(X0)) ),
inference(cnf_transformation,[],[f157]) ).
fof(f425,plain,
p100(sK82),
inference(cnf_transformation,[],[f158]) ).
fof(f426,plain,
~ p101(sK82),
inference(cnf_transformation,[],[f158]) ).
fof(f427,plain,
! [X2] :
( ~ r1(sK82,X2)
| sP41(X2) ),
inference(cnf_transformation,[],[f158]) ).
fof(f428,plain,
! [X1] :
( ~ r1(sK82,X1)
| p8(X1) ),
inference(cnf_transformation,[],[f158]) ).
fof(f430,plain,
sP41(sK82),
inference(resolution,[],[f159,f427]) ).
fof(f431,plain,
sP0(sK82),
inference(resolution,[],[f203,f430]) ).
fof(f434,plain,
( p101(sK82)
| ~ p100(sK82)
| r1(sK82,sK81(sK82)) ),
inference(resolution,[],[f431,f420]) ).
fof(f435,plain,
( ~ p100(sK82)
| r1(sK82,sK81(sK82)) ),
inference(forward_subsumption_resolution,[],[f434,f426]) ).
fof(f437,plain,
r1(sK82,sK81(sK82)),
inference(forward_subsumption_resolution,[],[f435,f425]) ).
fof(f440,plain,
sP41(sK81(sK82)),
inference(resolution,[],[f437,f427]) ).
fof(f452,plain,
! [X0] :
( ~ p101(X0)
| p102(X0)
| r1(X0,sK79(X0))
| ~ sP41(X0) ),
inference(resolution,[],[f412,f204]) ).
fof(f453,plain,
! [X0] :
( p102(sK81(X0))
| r1(sK81(X0),sK79(sK81(X0)))
| ~ sP41(sK81(X0))
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ),
inference(resolution,[],[f452,f417]) ).
fof(f454,plain,
! [X0] :
( ~ sP41(sK81(X0))
| r1(sK81(X0),sK79(sK81(X0)))
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ),
inference(forward_subsumption_resolution,[],[f453,f418]) ).
fof(f455,plain,
( r1(sK81(sK82),sK79(sK81(sK82)))
| p101(sK82)
| ~ p100(sK82)
| ~ sP0(sK82) ),
inference(resolution,[],[f454,f440]) ).
fof(f456,plain,
( r1(sK81(sK82),sK79(sK81(sK82)))
| ~ p100(sK82)
| ~ sP0(sK82) ),
inference(forward_subsumption_resolution,[],[f455,f426]) ).
fof(f457,plain,
( r1(sK81(sK82),sK79(sK81(sK82)))
| ~ sP0(sK82) ),
inference(forward_subsumption_resolution,[],[f456,f425]) ).
fof(f458,plain,
r1(sK81(sK82),sK79(sK81(sK82))),
inference(forward_subsumption_resolution,[],[f457,f431]) ).
fof(f459,plain,
! [X0] :
( ~ r1(X0,sK81(sK82))
| r1(X0,sK79(sK81(sK82))) ),
inference(resolution,[],[f458,f160]) ).
fof(f461,plain,
r1(sK82,sK79(sK81(sK82))),
inference(resolution,[],[f459,f437]) ).
fof(f463,plain,
sP41(sK79(sK81(sK82))),
inference(resolution,[],[f461,f427]) ).
fof(f523,plain,
! [X0] :
( ~ p101(X0)
| p102(X0)
| p102(sK79(X0))
| ~ sP41(X0) ),
inference(resolution,[],[f409,f204]) ).
fof(f524,plain,
! [X0] :
( p102(sK81(X0))
| p102(sK79(sK81(X0)))
| ~ sP41(sK81(X0))
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ),
inference(resolution,[],[f523,f417]) ).
fof(f527,plain,
! [X0] :
( ~ sP41(sK81(X0))
| p102(sK79(sK81(X0)))
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ),
inference(forward_subsumption_resolution,[],[f524,f418]) ).
fof(f556,plain,
( p102(sK79(sK81(sK82)))
| p101(sK82)
| ~ p100(sK82)
| ~ sP0(sK82) ),
inference(resolution,[],[f527,f440]) ).
fof(f557,plain,
( p102(sK79(sK81(sK82)))
| ~ p100(sK82)
| ~ sP0(sK82) ),
inference(forward_subsumption_resolution,[],[f556,f426]) ).
fof(f558,plain,
( p102(sK79(sK81(sK82)))
| ~ sP0(sK82) ),
inference(forward_subsumption_resolution,[],[f557,f425]) ).
fof(f559,plain,
p102(sK79(sK81(sK82))),
inference(forward_subsumption_resolution,[],[f558,f431]) ).
fof(f561,plain,
( p103(sK79(sK81(sK82)))
| r1(sK79(sK81(sK82)),sK77(sK79(sK81(sK82))))
| ~ sP2(sK79(sK81(sK82))) ),
inference(resolution,[],[f559,f404]) ).
fof(f564,definition,
( spl83_15
<=> sP2(sK79(sK81(sK82))) ),
introduced(definition,[new_symbols(definition,[spl83_15])],[avatar_definition]) ).
fof(f565,plain,
( ~ sP2(sK79(sK81(sK82)))
| spl83_15 ),
inference(avatar_component_clause,[],[f564]) ).
fof(f570,definition,
( spl83_17
<=> p103(sK79(sK81(sK82))) ),
introduced(definition,[new_symbols(definition,[spl83_17])],[avatar_definition]) ).
fof(f571,plain,
( p103(sK79(sK81(sK82)))
| ~ spl83_17 ),
inference(avatar_component_clause,[],[f570]) ).
fof(f574,definition,
( spl83_18
<=> r1(sK79(sK81(sK82)),sK77(sK79(sK81(sK82)))) ),
introduced(definition,[new_symbols(definition,[spl83_18])],[avatar_definition]) ).
fof(f575,plain,
( r1(sK79(sK81(sK82)),sK77(sK79(sK81(sK82))))
| ~ spl83_18 ),
inference(avatar_component_clause,[],[f574]) ).
fof(f576,plain,
( ~ spl83_15
| spl83_18
| spl83_17 ),
inference(avatar_split_clause,[],[f561,f570,f574,f564]) ).
fof(f592,plain,
! [X0] :
( p103(sK77(X0))
| ~ p102(X0)
| p103(X0)
| ~ sP41(X0) ),
inference(resolution,[],[f401,f205]) ).
fof(f593,plain,
! [X0] :
( ~ sP3(sK77(X0))
| p103(X0)
| ~ sP41(X0)
| p104(sK77(X0))
| r1(sK77(X0),sK75(sK77(X0)))
| ~ p102(X0) ),
inference(resolution,[],[f592,f396]) ).
fof(f595,plain,
! [X0] :
( ~ p103(X0)
| p104(X0)
| p104(sK75(X0))
| ~ sP41(X0) ),
inference(resolution,[],[f393,f206]) ).
fof(f596,plain,
! [X0] :
( ~ sP41(sK77(X0))
| p104(sK75(sK77(X0)))
| p104(sK77(X0))
| ~ p102(X0)
| p103(X0)
| ~ sP41(X0) ),
inference(resolution,[],[f595,f592]) ).
fof(f607,definition,
( spl83_21
<=> p101(sK81(sK82)) ),
introduced(definition,[new_symbols(definition,[spl83_21])],[avatar_definition]) ).
fof(f644,plain,
( p102(sK81(sK82))
| ~ p101(sK81(sK82))
| ~ sP1(sK81(sK82))
| ~ spl83_17 ),
inference(resolution,[],[f571,f410]) ).
fof(f665,definition,
( spl83_30
<=> sP1(sK81(sK82)) ),
introduced(definition,[new_symbols(definition,[spl83_30])],[avatar_definition]) ).
fof(f666,plain,
( ~ sP1(sK81(sK82))
| spl83_30 ),
inference(avatar_component_clause,[],[f665]) ).
fof(f667,plain,
( ~ p101(sK81(sK82))
| spl83_21 ),
inference(avatar_component_clause,[],[f607]) ).
fof(f669,definition,
( spl83_31
<=> p102(sK81(sK82)) ),
introduced(definition,[new_symbols(definition,[spl83_31])],[avatar_definition]) ).
fof(f670,plain,
( p102(sK81(sK82))
| ~ spl83_31 ),
inference(avatar_component_clause,[],[f669]) ).
fof(f671,plain,
( ~ spl83_30
| ~ spl83_21
| spl83_31
| ~ spl83_17 ),
inference(avatar_split_clause,[],[f644,f570,f669,f607,f665]) ).
fof(f776,plain,
( ~ sP41(sK79(sK81(sK82)))
| spl83_15 ),
inference(resolution,[],[f565,f205]) ).
fof(f778,plain,
( $false
| spl83_15 ),
inference(forward_subsumption_resolution,[],[f776,f463]) ).
fof(f779,plain,
spl83_15,
inference(avatar_contradiction_clause,[],[f778]) ).
fof(f780,plain,
( ! [X0] :
( r1(X0,sK77(sK79(sK81(sK82))))
| ~ r1(X0,sK79(sK81(sK82))) )
| ~ spl83_18 ),
inference(resolution,[],[f575,f160]) ).
fof(f783,plain,
( ~ r1(sK82,sK79(sK81(sK82)))
| sP41(sK77(sK79(sK81(sK82))))
| ~ spl83_18 ),
inference(resolution,[],[f780,f427]) ).
fof(f784,plain,
( ! [X0,X1] :
( ~ r1(X0,sK79(sK81(sK82)))
| ~ r1(X1,X0)
| r1(X1,sK77(sK79(sK81(sK82)))) )
| ~ spl83_18 ),
inference(resolution,[],[f780,f160]) ).
fof(f785,plain,
( sP41(sK77(sK79(sK81(sK82))))
| ~ spl83_18 ),
inference(forward_subsumption_resolution,[],[f783,f461]) ).
fof(f829,plain,
( ~ sP41(sK81(sK82))
| spl83_30 ),
inference(resolution,[],[f666,f204]) ).
fof(f831,plain,
( $false
| spl83_30 ),
inference(forward_subsumption_resolution,[],[f829,f440]) ).
fof(f832,plain,
spl83_30,
inference(avatar_contradiction_clause,[],[f831]) ).
fof(f834,plain,
( p101(sK82)
| ~ p100(sK82)
| ~ sP0(sK82)
| spl83_21 ),
inference(resolution,[],[f667,f417]) ).
fof(f836,plain,
( ~ p100(sK82)
| ~ sP0(sK82)
| spl83_21 ),
inference(forward_subsumption_resolution,[],[f834,f426]) ).
fof(f837,plain,
( ~ sP0(sK82)
| spl83_21 ),
inference(forward_subsumption_resolution,[],[f836,f425]) ).
fof(f838,plain,
( $false
| spl83_21 ),
inference(forward_subsumption_resolution,[],[f837,f431]) ).
fof(f839,plain,
spl83_21,
inference(avatar_contradiction_clause,[],[f838]) ).
fof(f841,plain,
( p101(sK82)
| ~ p100(sK82)
| ~ sP0(sK82)
| ~ spl83_31 ),
inference(resolution,[],[f670,f418]) ).
fof(f862,plain,
( ~ p100(sK82)
| ~ sP0(sK82)
| ~ spl83_31 ),
inference(forward_subsumption_resolution,[],[f841,f426]) ).
fof(f867,plain,
( ~ sP0(sK82)
| ~ spl83_31 ),
inference(forward_subsumption_resolution,[],[f862,f425]) ).
fof(f868,plain,
( $false
| ~ spl83_31 ),
inference(forward_subsumption_resolution,[],[f867,f431]) ).
fof(f869,plain,
~ spl83_31,
inference(avatar_contradiction_clause,[],[f868]) ).
fof(f1012,plain,
( p104(sK75(sK77(sK79(sK81(sK82)))))
| p104(sK77(sK79(sK81(sK82))))
| ~ p102(sK79(sK81(sK82)))
| p103(sK79(sK81(sK82)))
| ~ sP41(sK79(sK81(sK82)))
| ~ spl83_18 ),
inference(resolution,[],[f596,f785]) ).
fof(f1013,plain,
( p104(sK75(sK77(sK79(sK81(sK82)))))
| p104(sK77(sK79(sK81(sK82))))
| p103(sK79(sK81(sK82)))
| ~ sP41(sK79(sK81(sK82)))
| ~ spl83_18 ),
inference(forward_subsumption_resolution,[],[f1012,f559]) ).
fof(f1014,plain,
( p104(sK75(sK77(sK79(sK81(sK82)))))
| p104(sK77(sK79(sK81(sK82))))
| p103(sK79(sK81(sK82)))
| ~ spl83_18 ),
inference(forward_subsumption_resolution,[],[f1013,f463]) ).
fof(f1016,definition,
( spl83_92
<=> p104(sK77(sK79(sK81(sK82)))) ),
introduced(definition,[new_symbols(definition,[spl83_92])],[avatar_definition]) ).
fof(f1017,plain,
( p104(sK77(sK79(sK81(sK82))))
| ~ spl83_92 ),
inference(avatar_component_clause,[],[f1016]) ).
fof(f1019,definition,
( spl83_93
<=> p104(sK75(sK77(sK79(sK81(sK82))))) ),
introduced(definition,[new_symbols(definition,[spl83_93])],[avatar_definition]) ).
fof(f1020,plain,
( p104(sK75(sK77(sK79(sK81(sK82)))))
| ~ spl83_93 ),
inference(avatar_component_clause,[],[f1019]) ).
fof(f1021,plain,
( spl83_17
| spl83_92
| spl83_93
| ~ spl83_18 ),
inference(avatar_split_clause,[],[f1014,f574,f1019,f1016,f570]) ).
fof(f1022,plain,
( p103(sK79(sK81(sK82)))
| ~ p102(sK79(sK81(sK82)))
| ~ sP2(sK79(sK81(sK82)))
| ~ spl83_92 ),
inference(resolution,[],[f1017,f402]) ).
fof(f1051,plain,
( p103(sK79(sK81(sK82)))
| ~ sP2(sK79(sK81(sK82)))
| ~ spl83_92 ),
inference(forward_subsumption_resolution,[],[f1022,f559]) ).
fof(f1052,plain,
( ~ spl83_15
| spl83_17
| ~ spl83_92 ),
inference(avatar_split_clause,[],[f1051,f1016,f570,f564]) ).
fof(f1055,plain,
( p105(sK75(sK77(sK79(sK81(sK82)))))
| p105(sK73(sK75(sK77(sK79(sK81(sK82))))))
| ~ sP4(sK75(sK77(sK79(sK81(sK82)))))
| ~ spl83_93 ),
inference(resolution,[],[f1020,f385]) ).
fof(f1056,plain,
( p105(sK75(sK77(sK79(sK81(sK82)))))
| r1(sK75(sK77(sK79(sK81(sK82)))),sK73(sK75(sK77(sK79(sK81(sK82))))))
| ~ sP4(sK75(sK77(sK79(sK81(sK82)))))
| ~ spl83_93 ),
inference(resolution,[],[f1020,f388]) ).
fof(f1059,definition,
( spl83_100
<=> sP4(sK75(sK77(sK79(sK81(sK82))))) ),
introduced(definition,[new_symbols(definition,[spl83_100])],[avatar_definition]) ).
fof(f1060,plain,
( ~ sP4(sK75(sK77(sK79(sK81(sK82)))))
| spl83_100 ),
inference(avatar_component_clause,[],[f1059]) ).
fof(f1065,definition,
( spl83_102
<=> p105(sK75(sK77(sK79(sK81(sK82))))) ),
introduced(definition,[new_symbols(definition,[spl83_102])],[avatar_definition]) ).
fof(f1066,plain,
( p105(sK75(sK77(sK79(sK81(sK82)))))
| ~ spl83_102 ),
inference(avatar_component_clause,[],[f1065]) ).
fof(f1069,definition,
( spl83_103
<=> r1(sK75(sK77(sK79(sK81(sK82)))),sK73(sK75(sK77(sK79(sK81(sK82)))))) ),
introduced(definition,[new_symbols(definition,[spl83_103])],[avatar_definition]) ).
fof(f1070,plain,
( r1(sK75(sK77(sK79(sK81(sK82)))),sK73(sK75(sK77(sK79(sK81(sK82))))))
| ~ spl83_103 ),
inference(avatar_component_clause,[],[f1069]) ).
fof(f1071,plain,
( ~ spl83_100
| spl83_103
| spl83_102
| ~ spl83_93 ),
inference(avatar_split_clause,[],[f1056,f1019,f1065,f1069,f1059]) ).
fof(f1073,definition,
( spl83_104
<=> p105(sK73(sK75(sK77(sK79(sK81(sK82)))))) ),
introduced(definition,[new_symbols(definition,[spl83_104])],[avatar_definition]) ).
fof(f1074,plain,
( p105(sK73(sK75(sK77(sK79(sK81(sK82))))))
| ~ spl83_104 ),
inference(avatar_component_clause,[],[f1073]) ).
fof(f1075,plain,
( ~ spl83_100
| spl83_104
| spl83_102
| ~ spl83_93 ),
inference(avatar_split_clause,[],[f1055,f1019,f1065,f1073,f1059]) ).
fof(f1077,definition,
( spl83_105
<=> sP41(sK75(sK77(sK79(sK81(sK82))))) ),
introduced(definition,[new_symbols(definition,[spl83_105])],[avatar_definition]) ).
fof(f1129,definition,
( spl83_116
<=> p103(sK77(sK79(sK81(sK82)))) ),
introduced(definition,[new_symbols(definition,[spl83_116])],[avatar_definition]) ).
fof(f1152,definition,
( spl83_119
<=> sP3(sK77(sK79(sK81(sK82)))) ),
introduced(definition,[new_symbols(definition,[spl83_119])],[avatar_definition]) ).
fof(f1153,plain,
( ~ sP3(sK77(sK79(sK81(sK82))))
| spl83_119 ),
inference(avatar_component_clause,[],[f1152]) ).
fof(f1159,definition,
( spl83_121
<=> r1(sK77(sK79(sK81(sK82))),sK75(sK77(sK79(sK81(sK82))))) ),
introduced(definition,[new_symbols(definition,[spl83_121])],[avatar_definition]) ).
fof(f1160,plain,
( r1(sK77(sK79(sK81(sK82))),sK75(sK77(sK79(sK81(sK82)))))
| ~ spl83_121 ),
inference(avatar_component_clause,[],[f1159]) ).
fof(f1242,plain,
! [X0] :
( ~ sP41(sK77(X0))
| ~ sP41(X0)
| p104(sK77(X0))
| r1(sK77(X0),sK75(sK77(X0)))
| ~ p102(X0)
| p103(X0) ),
inference(resolution,[],[f593,f206]) ).
fof(f1243,plain,
( ~ sP41(sK79(sK81(sK82)))
| p104(sK77(sK79(sK81(sK82))))
| r1(sK77(sK79(sK81(sK82))),sK75(sK77(sK79(sK81(sK82)))))
| ~ p102(sK79(sK81(sK82)))
| p103(sK79(sK81(sK82)))
| ~ spl83_18 ),
inference(resolution,[],[f1242,f785]) ).
fof(f1244,plain,
( p104(sK77(sK79(sK81(sK82))))
| r1(sK77(sK79(sK81(sK82))),sK75(sK77(sK79(sK81(sK82)))))
| ~ p102(sK79(sK81(sK82)))
| p103(sK79(sK81(sK82)))
| ~ spl83_18 ),
inference(forward_subsumption_resolution,[],[f1243,f463]) ).
fof(f1245,plain,
( p104(sK77(sK79(sK81(sK82))))
| r1(sK77(sK79(sK81(sK82))),sK75(sK77(sK79(sK81(sK82)))))
| p103(sK79(sK81(sK82)))
| ~ spl83_18 ),
inference(forward_subsumption_resolution,[],[f1244,f559]) ).
fof(f1246,plain,
( spl83_17
| spl83_121
| spl83_92
| ~ spl83_18 ),
inference(avatar_split_clause,[],[f1245,f574,f1016,f1159,f570]) ).
fof(f1247,plain,
( ! [X0] :
( r1(X0,sK75(sK77(sK79(sK81(sK82)))))
| ~ r1(X0,sK77(sK79(sK81(sK82)))) )
| ~ spl83_121 ),
inference(resolution,[],[f1160,f160]) ).
fof(f1249,plain,
( ~ r1(sK82,sK77(sK79(sK81(sK82))))
| sP41(sK75(sK77(sK79(sK81(sK82)))))
| ~ spl83_121 ),
inference(resolution,[],[f1247,f427]) ).
fof(f1250,plain,
( ! [X0,X1] :
( ~ r1(X0,sK77(sK79(sK81(sK82))))
| ~ r1(X1,X0)
| r1(X1,sK75(sK77(sK79(sK81(sK82))))) )
| ~ spl83_121 ),
inference(resolution,[],[f1247,f160]) ).
fof(f1256,definition,
( spl83_140
<=> r1(sK82,sK77(sK79(sK81(sK82)))) ),
introduced(definition,[new_symbols(definition,[spl83_140])],[avatar_definition]) ).
fof(f1257,plain,
( ~ r1(sK82,sK77(sK79(sK81(sK82))))
| spl83_140 ),
inference(avatar_component_clause,[],[f1256]) ).
fof(f1262,plain,
( ~ r1(sK82,sK79(sK81(sK82)))
| ~ spl83_18
| spl83_140 ),
inference(resolution,[],[f1257,f780]) ).
fof(f1265,plain,
( $false
| ~ spl83_18
| spl83_140 ),
inference(forward_subsumption_resolution,[],[f1262,f461]) ).
fof(f1266,plain,
( ~ spl83_18
| spl83_140 ),
inference(avatar_contradiction_clause,[],[f1265]) ).
fof(f1267,plain,
( sP41(sK75(sK77(sK79(sK81(sK82)))))
| ~ spl83_105 ),
inference(avatar_component_clause,[],[f1077]) ).
fof(f1268,plain,
( spl83_105
| ~ spl83_140
| ~ spl83_121 ),
inference(avatar_split_clause,[],[f1249,f1159,f1256,f1077]) ).
fof(f1519,plain,
( ! [X0] :
( ~ r1(X0,sK81(sK82))
| r1(X0,sK77(sK79(sK81(sK82)))) )
| ~ spl83_18 ),
inference(resolution,[],[f784,f458]) ).
fof(f1522,plain,
( r1(sK82,sK77(sK79(sK81(sK82))))
| ~ spl83_18 ),
inference(resolution,[],[f1519,f437]) ).
fof(f1951,plain,
( ! [X0] :
( ~ r1(X0,sK82)
| r1(X0,sK75(sK77(sK79(sK81(sK82))))) )
| ~ spl83_18
| ~ spl83_121 ),
inference(resolution,[],[f1250,f1522]) ).
fof(f1955,plain,
( r1(sK82,sK75(sK77(sK79(sK81(sK82)))))
| ~ spl83_18
| ~ spl83_121 ),
inference(resolution,[],[f1951,f159]) ).
fof(f2390,plain,
( ~ sP41(sK75(sK77(sK79(sK81(sK82)))))
| spl83_100 ),
inference(resolution,[],[f1060,f207]) ).
fof(f2392,plain,
( $false
| spl83_100
| ~ spl83_105 ),
inference(forward_subsumption_resolution,[],[f2390,f1267]) ).
fof(f2393,plain,
( spl83_100
| ~ spl83_105 ),
inference(avatar_contradiction_clause,[],[f2392]) ).
fof(f2394,plain,
( p104(sK77(sK79(sK81(sK82))))
| ~ p103(sK77(sK79(sK81(sK82))))
| ~ sP3(sK77(sK79(sK81(sK82))))
| ~ spl83_102 ),
inference(resolution,[],[f1066,f394]) ).
fof(f2422,plain,
( ~ p103(sK77(sK79(sK81(sK82))))
| spl83_116 ),
inference(avatar_component_clause,[],[f1129]) ).
fof(f2423,plain,
( ~ spl83_119
| ~ spl83_116
| spl83_92
| ~ spl83_102 ),
inference(avatar_split_clause,[],[f2394,f1065,f1016,f1129,f1152]) ).
fof(f2424,plain,
( ~ p102(sK79(sK81(sK82)))
| p103(sK79(sK81(sK82)))
| ~ sP41(sK79(sK81(sK82)))
| spl83_116 ),
inference(resolution,[],[f2422,f592]) ).
fof(f2425,plain,
( p103(sK79(sK81(sK82)))
| ~ sP41(sK79(sK81(sK82)))
| spl83_116 ),
inference(forward_subsumption_resolution,[],[f2424,f559]) ).
fof(f2426,plain,
( p103(sK79(sK81(sK82)))
| spl83_116 ),
inference(forward_subsumption_resolution,[],[f2425,f463]) ).
fof(f2427,plain,
( spl83_17
| spl83_116 ),
inference(avatar_split_clause,[],[f2426,f1129,f570]) ).
fof(f2434,plain,
( ~ sP41(sK77(sK79(sK81(sK82))))
| spl83_119 ),
inference(resolution,[],[f1153,f206]) ).
fof(f2436,plain,
( $false
| ~ spl83_18
| spl83_119 ),
inference(forward_subsumption_resolution,[],[f2434,f785]) ).
fof(f2437,plain,
( ~ spl83_18
| spl83_119 ),
inference(avatar_contradiction_clause,[],[f2436]) ).
fof(f2438,plain,
( ! [X0] :
( r1(X0,sK73(sK75(sK77(sK79(sK81(sK82))))))
| ~ r1(X0,sK75(sK77(sK79(sK81(sK82))))) )
| ~ spl83_103 ),
inference(resolution,[],[f1070,f160]) ).
fof(f2442,plain,
( p106(sK73(sK75(sK77(sK79(sK81(sK82))))))
| p106(sK71(sK73(sK75(sK77(sK79(sK81(sK82)))))))
| ~ sP5(sK73(sK75(sK77(sK79(sK81(sK82))))))
| ~ spl83_104 ),
inference(resolution,[],[f1074,f377]) ).
fof(f2443,plain,
( p106(sK73(sK75(sK77(sK79(sK81(sK82))))))
| r1(sK73(sK75(sK77(sK79(sK81(sK82))))),sK71(sK73(sK75(sK77(sK79(sK81(sK82)))))))
| ~ sP5(sK73(sK75(sK77(sK79(sK81(sK82))))))
| ~ spl83_104 ),
inference(resolution,[],[f1074,f380]) ).
fof(f2446,definition,
( spl83_302
<=> sP5(sK73(sK75(sK77(sK79(sK81(sK82)))))) ),
introduced(definition,[new_symbols(definition,[spl83_302])],[avatar_definition]) ).
fof(f2447,plain,
( ~ sP5(sK73(sK75(sK77(sK79(sK81(sK82))))))
| spl83_302 ),
inference(avatar_component_clause,[],[f2446]) ).
fof(f2452,definition,
( spl83_304
<=> p106(sK73(sK75(sK77(sK79(sK81(sK82)))))) ),
introduced(definition,[new_symbols(definition,[spl83_304])],[avatar_definition]) ).
fof(f2453,plain,
( p106(sK73(sK75(sK77(sK79(sK81(sK82))))))
| ~ spl83_304 ),
inference(avatar_component_clause,[],[f2452]) ).
fof(f2456,definition,
( spl83_305
<=> r1(sK73(sK75(sK77(sK79(sK81(sK82))))),sK71(sK73(sK75(sK77(sK79(sK81(sK82))))))) ),
introduced(definition,[new_symbols(definition,[spl83_305])],[avatar_definition]) ).
fof(f2457,plain,
( r1(sK73(sK75(sK77(sK79(sK81(sK82))))),sK71(sK73(sK75(sK77(sK79(sK81(sK82)))))))
| ~ spl83_305 ),
inference(avatar_component_clause,[],[f2456]) ).
fof(f2458,plain,
( ~ spl83_302
| spl83_305
| spl83_304
| ~ spl83_104 ),
inference(avatar_split_clause,[],[f2443,f1073,f2452,f2456,f2446]) ).
fof(f2460,definition,
( spl83_306
<=> p106(sK71(sK73(sK75(sK77(sK79(sK81(sK82))))))) ),
introduced(definition,[new_symbols(definition,[spl83_306])],[avatar_definition]) ).
fof(f2461,plain,
( p106(sK71(sK73(sK75(sK77(sK79(sK81(sK82)))))))
| ~ spl83_306 ),
inference(avatar_component_clause,[],[f2460]) ).
fof(f2462,plain,
( ~ spl83_302
| spl83_306
| spl83_304
| ~ spl83_104 ),
inference(avatar_split_clause,[],[f2442,f1073,f2452,f2460,f2446]) ).
fof(f2509,plain,
( ~ r1(sK82,sK75(sK77(sK79(sK81(sK82)))))
| sP41(sK73(sK75(sK77(sK79(sK81(sK82))))))
| ~ spl83_103 ),
inference(resolution,[],[f2438,f427]) ).
fof(f2510,plain,
( ! [X0,X1] :
( ~ r1(X0,sK75(sK77(sK79(sK81(sK82)))))
| ~ r1(X1,X0)
| r1(X1,sK73(sK75(sK77(sK79(sK81(sK82)))))) )
| ~ spl83_103 ),
inference(resolution,[],[f2438,f160]) ).
fof(f2511,plain,
( sP41(sK73(sK75(sK77(sK79(sK81(sK82))))))
| ~ spl83_18
| ~ spl83_103
| ~ spl83_121 ),
inference(forward_subsumption_resolution,[],[f2509,f1955]) ).
fof(f2575,plain,
( ! [X0] :
( ~ r1(X0,sK82)
| r1(X0,sK73(sK75(sK77(sK79(sK81(sK82)))))) )
| ~ spl83_18
| ~ spl83_103
| ~ spl83_121 ),
inference(resolution,[],[f2510,f1955]) ).
fof(f2587,plain,
( r1(sK82,sK73(sK75(sK77(sK79(sK81(sK82))))))
| ~ spl83_18
| ~ spl83_103
| ~ spl83_121 ),
inference(resolution,[],[f2575,f159]) ).
fof(f2592,plain,
( ~ sP41(sK73(sK75(sK77(sK79(sK81(sK82))))))
| spl83_302 ),
inference(resolution,[],[f2447,f208]) ).
fof(f2594,plain,
( $false
| ~ spl83_18
| ~ spl83_103
| ~ spl83_121
| spl83_302 ),
inference(forward_subsumption_resolution,[],[f2592,f2511]) ).
fof(f2595,plain,
( ~ spl83_18
| ~ spl83_103
| ~ spl83_121
| spl83_302 ),
inference(avatar_contradiction_clause,[],[f2594]) ).
fof(f2596,plain,
( p105(sK75(sK77(sK79(sK81(sK82)))))
| ~ p104(sK75(sK77(sK79(sK81(sK82)))))
| ~ sP4(sK75(sK77(sK79(sK81(sK82)))))
| ~ spl83_304 ),
inference(resolution,[],[f2453,f386]) ).
fof(f2624,plain,
( p105(sK75(sK77(sK79(sK81(sK82)))))
| ~ sP4(sK75(sK77(sK79(sK81(sK82)))))
| ~ spl83_93
| ~ spl83_304 ),
inference(forward_subsumption_resolution,[],[f2596,f1020]) ).
fof(f2625,plain,
( ~ spl83_100
| spl83_102
| ~ spl83_93
| ~ spl83_304 ),
inference(avatar_split_clause,[],[f2624,f2452,f1019,f1065,f1059]) ).
fof(f2626,plain,
( ! [X0] :
( r1(X0,sK71(sK73(sK75(sK77(sK79(sK81(sK82)))))))
| ~ r1(X0,sK73(sK75(sK77(sK79(sK81(sK82)))))) )
| ~ spl83_305 ),
inference(resolution,[],[f2457,f160]) ).
fof(f2632,plain,
( p107(sK71(sK73(sK75(sK77(sK79(sK81(sK82)))))))
| r1(sK71(sK73(sK75(sK77(sK79(sK81(sK82)))))),sK68(sK71(sK73(sK75(sK77(sK79(sK81(sK82))))))))
| ~ sP6(sK71(sK73(sK75(sK77(sK79(sK81(sK82)))))))
| ~ spl83_306 ),
inference(resolution,[],[f2461,f376]) ).
fof(f2634,definition,
( spl83_324
<=> sP6(sK71(sK73(sK75(sK77(sK79(sK81(sK82))))))) ),
introduced(definition,[new_symbols(definition,[spl83_324])],[avatar_definition]) ).
fof(f2635,plain,
( ~ sP6(sK71(sK73(sK75(sK77(sK79(sK81(sK82)))))))
| spl83_324 ),
inference(avatar_component_clause,[],[f2634]) ).
fof(f2637,definition,
( spl83_325
<=> r1(sK71(sK73(sK75(sK77(sK79(sK81(sK82)))))),sK68(sK71(sK73(sK75(sK77(sK79(sK81(sK82)))))))) ),
introduced(definition,[new_symbols(definition,[spl83_325])],[avatar_definition]) ).
fof(f2638,plain,
( r1(sK71(sK73(sK75(sK77(sK79(sK81(sK82)))))),sK68(sK71(sK73(sK75(sK77(sK79(sK81(sK82))))))))
| ~ spl83_325 ),
inference(avatar_component_clause,[],[f2637]) ).
fof(f2640,definition,
( spl83_326
<=> p107(sK71(sK73(sK75(sK77(sK79(sK81(sK82))))))) ),
introduced(definition,[new_symbols(definition,[spl83_326])],[avatar_definition]) ).
fof(f2641,plain,
( p107(sK71(sK73(sK75(sK77(sK79(sK81(sK82)))))))
| ~ spl83_326 ),
inference(avatar_component_clause,[],[f2640]) ).
fof(f2642,plain,
( ~ spl83_324
| spl83_325
| spl83_326
| ~ spl83_306 ),
inference(avatar_split_clause,[],[f2632,f2460,f2640,f2637,f2634]) ).
fof(f2697,plain,
( ~ r1(sK82,sK73(sK75(sK77(sK79(sK81(sK82))))))
| sP41(sK71(sK73(sK75(sK77(sK79(sK81(sK82)))))))
| ~ spl83_305 ),
inference(resolution,[],[f2626,f427]) ).
fof(f2699,plain,
( sP41(sK71(sK73(sK75(sK77(sK79(sK81(sK82)))))))
| ~ spl83_18
| ~ spl83_103
| ~ spl83_121
| ~ spl83_305 ),
inference(forward_subsumption_resolution,[],[f2697,f2587]) ).
fof(f2771,plain,
( ~ sP41(sK71(sK73(sK75(sK77(sK79(sK81(sK82)))))))
| spl83_324 ),
inference(resolution,[],[f2635,f209]) ).
fof(f2773,plain,
( $false
| ~ spl83_18
| ~ spl83_103
| ~ spl83_121
| ~ spl83_305
| spl83_324 ),
inference(forward_subsumption_resolution,[],[f2771,f2699]) ).
fof(f2774,plain,
( ~ spl83_18
| ~ spl83_103
| ~ spl83_121
| ~ spl83_305
| spl83_324 ),
inference(avatar_contradiction_clause,[],[f2773]) ).
fof(f2775,plain,
( p106(sK73(sK75(sK77(sK79(sK81(sK82))))))
| ~ p105(sK73(sK75(sK77(sK79(sK81(sK82))))))
| ~ sP5(sK73(sK75(sK77(sK79(sK81(sK82))))))
| ~ spl83_326 ),
inference(resolution,[],[f2641,f378]) ).
fof(f2806,plain,
( p106(sK73(sK75(sK77(sK79(sK81(sK82))))))
| ~ sP5(sK73(sK75(sK77(sK79(sK81(sK82))))))
| ~ spl83_104
| ~ spl83_326 ),
inference(forward_subsumption_resolution,[],[f2775,f1074]) ).
fof(f2814,plain,
( ~ spl83_302
| spl83_304
| ~ spl83_104
| ~ spl83_326 ),
inference(avatar_split_clause,[],[f2806,f2640,f1073,f2452,f2446]) ).
fof(f2816,plain,
( ! [X0] :
( r1(X0,sK68(sK71(sK73(sK75(sK77(sK79(sK81(sK82))))))))
| ~ r1(X0,sK71(sK73(sK75(sK77(sK79(sK81(sK82))))))) )
| ~ spl83_325 ),
inference(resolution,[],[f2638,f160]) ).
fof(f2901,definition,
( spl83_367
<=> p8(sK68(sK71(sK73(sK75(sK77(sK79(sK81(sK82)))))))) ),
introduced(definition,[new_symbols(definition,[spl83_367])],[avatar_definition]) ).
fof(f2902,plain,
( p8(sK68(sK71(sK73(sK75(sK77(sK79(sK81(sK82))))))))
| ~ spl83_367 ),
inference(avatar_component_clause,[],[f2901]) ).
fof(f2924,definition,
( spl83_372
<=> r1(sK82,sK71(sK73(sK75(sK77(sK79(sK81(sK82))))))) ),
introduced(definition,[new_symbols(definition,[spl83_372])],[avatar_definition]) ).
fof(f2925,plain,
( ~ r1(sK82,sK71(sK73(sK75(sK77(sK79(sK81(sK82)))))))
| spl83_372 ),
inference(avatar_component_clause,[],[f2924]) ).
fof(f2930,plain,
( ~ r1(sK82,sK73(sK75(sK77(sK79(sK81(sK82))))))
| ~ spl83_305
| spl83_372 ),
inference(resolution,[],[f2925,f2626]) ).
fof(f2933,plain,
( $false
| ~ spl83_18
| ~ spl83_103
| ~ spl83_121
| ~ spl83_305
| spl83_372 ),
inference(forward_subsumption_resolution,[],[f2930,f2587]) ).
fof(f2934,plain,
( ~ spl83_18
| ~ spl83_103
| ~ spl83_121
| ~ spl83_305
| spl83_372 ),
inference(avatar_contradiction_clause,[],[f2933]) ).
fof(f2970,plain,
( ~ r1(sK82,sK71(sK73(sK75(sK77(sK79(sK81(sK82)))))))
| p8(sK68(sK71(sK73(sK75(sK77(sK79(sK81(sK82))))))))
| ~ spl83_325 ),
inference(resolution,[],[f2816,f428]) ).
fof(f2974,plain,
( spl83_367
| ~ spl83_372
| ~ spl83_325 ),
inference(avatar_split_clause,[],[f2970,f2637,f2924,f2901]) ).
fof(f2985,plain,
( p107(sK71(sK73(sK75(sK77(sK79(sK81(sK82)))))))
| ~ p106(sK71(sK73(sK75(sK77(sK79(sK81(sK82)))))))
| ~ sP6(sK71(sK73(sK75(sK77(sK79(sK81(sK82)))))))
| ~ spl83_367 ),
inference(resolution,[],[f2902,f375]) ).
fof(f2986,plain,
( p107(sK71(sK73(sK75(sK77(sK79(sK81(sK82)))))))
| ~ sP6(sK71(sK73(sK75(sK77(sK79(sK81(sK82)))))))
| ~ spl83_306
| ~ spl83_367 ),
inference(forward_subsumption_resolution,[],[f2985,f2461]) ).
fof(f2987,plain,
( ~ spl83_324
| spl83_326
| ~ spl83_306
| ~ spl83_367 ),
inference(avatar_split_clause,[],[f2986,f2901,f2460,f2640,f2634]) ).
cnf(s12,plain,
( ~ spl83_15
| spl83_17
| spl83_18 ),
inference(sat_conversion,[],[f576]) ).
cnf(s21,plain,
( ~ spl83_17
| ~ spl83_21
| ~ spl83_30
| spl83_31 ),
inference(sat_conversion,[],[f671]) ).
cnf(s36,plain,
spl83_15,
inference(sat_conversion,[],[f779]) ).
cnf(s43,plain,
spl83_30,
inference(sat_conversion,[],[f832]) ).
cnf(s45,plain,
spl83_21,
inference(sat_conversion,[],[f839]) ).
cnf(s50,plain,
~ spl83_31,
inference(sat_conversion,[],[f869]) ).
cnf(s71,plain,
( spl83_17
| ~ spl83_18
| spl83_92
| spl83_93 ),
inference(sat_conversion,[],[f1021]) ).
cnf(s76,plain,
( ~ spl83_15
| spl83_17
| ~ spl83_92 ),
inference(sat_conversion,[],[f1052]) ).
cnf(s78,plain,
( ~ spl83_93
| ~ spl83_100
| spl83_102
| spl83_103 ),
inference(sat_conversion,[],[f1071]) ).
cnf(s79,plain,
( ~ spl83_93
| ~ spl83_100
| spl83_102
| spl83_104 ),
inference(sat_conversion,[],[f1075]) ).
cnf(s104,plain,
( spl83_17
| ~ spl83_18
| spl83_92
| spl83_121 ),
inference(sat_conversion,[],[f1246]) ).
cnf(s109,plain,
( ~ spl83_18
| spl83_140 ),
inference(sat_conversion,[],[f1266]) ).
cnf(s110,plain,
( spl83_105
| ~ spl83_121
| ~ spl83_140 ),
inference(sat_conversion,[],[f1268]) ).
cnf(s251,plain,
( spl83_100
| ~ spl83_105 ),
inference(sat_conversion,[],[f2393]) ).
cnf(s256,plain,
( spl83_92
| ~ spl83_102
| ~ spl83_116
| ~ spl83_119 ),
inference(sat_conversion,[],[f2423]) ).
cnf(s257,plain,
( spl83_17
| spl83_116 ),
inference(sat_conversion,[],[f2427]) ).
cnf(s259,plain,
( ~ spl83_18
| spl83_119 ),
inference(sat_conversion,[],[f2437]) ).
cnf(s261,plain,
( ~ spl83_104
| ~ spl83_302
| spl83_304
| spl83_305 ),
inference(sat_conversion,[],[f2458]) ).
cnf(s262,plain,
( ~ spl83_104
| ~ spl83_302
| spl83_304
| spl83_306 ),
inference(sat_conversion,[],[f2462]) ).
cnf(s273,plain,
( ~ spl83_18
| ~ spl83_103
| ~ spl83_121
| spl83_302 ),
inference(sat_conversion,[],[f2595]) ).
cnf(s278,plain,
( ~ spl83_93
| ~ spl83_100
| spl83_102
| ~ spl83_304 ),
inference(sat_conversion,[],[f2625]) ).
cnf(s279,plain,
( ~ spl83_306
| ~ spl83_324
| spl83_325
| spl83_326 ),
inference(sat_conversion,[],[f2642]) ).
cnf(s292,plain,
( ~ spl83_18
| ~ spl83_103
| ~ spl83_121
| ~ spl83_305
| spl83_324 ),
inference(sat_conversion,[],[f2774]) ).
cnf(s298,plain,
( ~ spl83_104
| ~ spl83_302
| spl83_304
| ~ spl83_326 ),
inference(sat_conversion,[],[f2814]) ).
cnf(s317,plain,
( ~ spl83_18
| ~ spl83_103
| ~ spl83_121
| ~ spl83_305
| spl83_372 ),
inference(sat_conversion,[],[f2934]) ).
cnf(s319,plain,
( ~ spl83_325
| spl83_367
| ~ spl83_372 ),
inference(sat_conversion,[],[f2974]) ).
cnf(s322,plain,
( ~ spl83_306
| ~ spl83_324
| spl83_326
| ~ spl83_367 ),
inference(sat_conversion,[],[f2987]) ).
cnf(s339,plain,
~ spl83_17,
inference(rat,[],[s21,s50,s43,s45]) ).
cnf(s340,plain,
spl83_116,
inference(rat,[],[s257,s339]) ).
cnf(s341,plain,
~ spl83_92,
inference(rat,[],[s76,s36,s339]) ).
cnf(s345,plain,
spl83_18,
inference(rat,[],[s12,s339,s36]) ).
cnf(s346,plain,
spl83_119,
inference(rat,[],[s259,s345]) ).
cnf(s348,plain,
spl83_140,
inference(rat,[],[s109,s345]) ).
cnf(s349,plain,
spl83_121,
inference(rat,[],[s104,s341,s339,s345]) ).
cnf(s352,plain,
spl83_93,
inference(rat,[],[s71,s339,s341,s345]) ).
cnf(s353,plain,
~ spl83_102,
inference(rat,[],[s256,s341,s340,s346]) ).
cnf(s356,plain,
spl83_105,
inference(rat,[],[s110,s348,s349]) ).
cnf(s360,plain,
spl83_100,
inference(rat,[],[s251,s356]) ).
cnf(s363,plain,
~ spl83_304,
inference(rat,[],[s278,s352,s353,s360]) ).
cnf(s365,plain,
spl83_104,
inference(rat,[],[s79,s352,s353,s360]) ).
cnf(s366,plain,
spl83_103,
inference(rat,[],[s78,s352,s353,s360]) ).
cnf(s368,plain,
spl83_302,
inference(rat,[],[s273,s349,s345,s366]) ).
cnf(s371,plain,
~ spl83_326,
inference(rat,[],[s298,s365,s363,s368]) ).
cnf(s373,plain,
spl83_306,
inference(rat,[],[s262,s365,s363,s368]) ).
cnf(s374,plain,
spl83_305,
inference(rat,[],[s261,s365,s363,s368]) ).
cnf(s378,plain,
spl83_372,
inference(rat,[],[s317,s366,s349,s345,s374]) ).
cnf(s379,plain,
spl83_324,
inference(rat,[],[s292,s366,s349,s345,s374]) ).
cnf(s382,plain,
~ spl83_367,
inference(rat,[],[s322,s373,s371,s379]) ).
cnf(s386,plain,
spl83_325,
inference(rat,[],[s279,s371,s373,s379]) ).
cnf(s389,plain,
$false,
inference(rat,[],[s319,s378,s382,s386]) ).
fof(f2988,plain,
$false,
inference(avatar_sat_refutation,[],[s389]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL674+1.020 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.38 % Computer : n018.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Sun Sep 27 16:33:39 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.41 Running first-order theorem proving
% 0.09/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.81/2.17 % (2566275)Detected formulas, will run a generic FOF schedule.
% 8.81/2.17 % (2566284)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4053120672:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 8.81/2.17 % (2566284)Instruction limit reached!
% 8.81/2.17 % (2566284)------------------------------
% 8.81/2.17 % (2566284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.81/2.17 % (2566284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.81/2.17 % (2566284)CaDiCaL version: 2.1.3
% 8.81/2.17 % (2566284)Termination reason: Instruction limit
% 8.81/2.17 % (2566284)Termination phase: Saturation
% 8.81/2.17 % (2566284)Time elapsed: 0.027 s
% 8.81/2.17 % (2566284)Peak memory usage: 88 MB
% 8.81/2.17 % (2566284)Instructions burned: 121 (million)
% 8.81/2.17 % (2566283)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1755358734:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 8.81/2.17 % (2566281)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1232695566:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 8.81/2.17 % (2566286)dis-21_1_sil=8000:lcm=predicate:random_seed=2170060740:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 8.81/2.17 % (2566280)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2414539822:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 8.81/2.17 % (2566282)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1341410237:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 8.81/2.17 % (2566285)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=694473714:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 8.81/2.17 % (2566283)Refutation not found, incomplete strategy
% 8.81/2.17 % (2566283)------------------------------
% 8.81/2.17 % (2566283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.81/2.17 % (2566283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.81/2.17 % (2566283)CaDiCaL version: 2.1.3
% 8.81/2.17 % (2566283)Termination reason: Refutation not found, incomplete strategy
% 8.81/2.17 % (2566283)Time elapsed: 0.017 s
% 8.81/2.17 % (2566283)Peak memory usage: 89 MB
% 8.81/2.17 % (2566283)Instructions burned: 30 (million)
% 8.81/2.17 % (2566286)Instruction limit reached!
% 8.81/2.17 % (2566286)------------------------------
% 8.81/2.17 % (2566286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.81/2.17 % (2566286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.81/2.17 % (2566286)CaDiCaL version: 2.1.3
% 8.81/2.17 % (2566286)Termination reason: Instruction limit
% 8.81/2.17 % (2566286)Termination phase: Saturation
% 8.81/2.17 % (2566286)Time elapsed: 0.053 s
% 8.81/2.17 % (2566286)Peak memory usage: 88 MB
% 8.81/2.17 % (2566286)Instructions burned: 131 (million)
% 8.81/2.17 % (2566285)Instruction limit reached!
% 8.81/2.17 % (2566285)------------------------------
% 8.81/2.17 % (2566285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.81/2.17 % (2566285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.81/2.17 % (2566285)CaDiCaL version: 2.1.3
% 8.81/2.17 % (2566285)Termination reason: Instruction limit
% 8.81/2.17 % (2566285)Termination phase: Saturation
% 8.81/2.17 % (2566285)Time elapsed: 0.059 s
% 8.81/2.17 % (2566285)Peak memory usage: 89 MB
% 8.81/2.17 % (2566285)Instructions burned: 141 (million)
% 8.81/2.17 % (2566288)lrs+10_1_sil=8000:sp=occurrence:random_seed=934223782:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 8.81/2.17 % (2566288)Instruction limit reached!
% 8.81/2.17 % (2566288)------------------------------
% 8.81/2.17 % (2566288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.81/2.17 % (2566288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.81/2.17 % (2566288)CaDiCaL version: 2.1.3
% 8.81/2.17 % (2566288)Termination reason: Instruction limit
% 8.81/2.17 % (2566288)Termination phase: Saturation
% 8.81/2.17 % (2566288)Time elapsed: 0.070 s
% 8.81/2.17 % (2566288)Peak memory usage: 94 MB
% 8.81/2.17 % (2566288)Instructions burned: 286 (million)
% 8.81/2.17 % (2566295)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3283646529:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 8.81/2.17 % (2566296)lrs+1011_1_sil=32000:sp=occurrence:random_seed=260107973:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 8.81/2.17 % (2566283)------------------------------
% 8.81/2.17 % (2566283)------------------------------
% 8.81/2.17 % (2566298)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=541741537:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 8.81/2.17 % (2566295)Instruction limit reached!
% 8.81/2.17 % (2566295)------------------------------
% 8.81/2.17 % (2566295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.81/2.17 % (2566295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.81/2.17 % (2566295)CaDiCaL version: 2.1.3
% 8.81/2.17 % (2566295)Termination reason: Instruction limit
% 8.81/2.17 % (2566295)Termination phase: Saturation
% 8.81/2.17 % (2566295)Time elapsed: 0.082 s
% 8.81/2.17 % (2566295)Peak memory usage: 90 MB
% 8.81/2.17 % (2566295)Instructions burned: 158 (million)
% 8.81/2.17 % (2566296)Instruction limit reached!
% 8.81/2.17 % (2566296)------------------------------
% 8.81/2.17 % (2566296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.81/2.17 % (2566296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.81/2.17 % (2566296)CaDiCaL version: 2.1.3
% 8.81/2.17 % (2566296)Termination reason: Instruction limit
% 8.81/2.17 % (2566296)Termination phase: Saturation
% 8.81/2.17 % (2566296)Time elapsed: 0.120 s
% 8.81/2.17 % (2566296)Peak memory usage: 89 MB
% 8.81/2.17 % (2566296)Instructions burned: 326 (million)
% 8.81/2.17 % (2566298)Instruction limit reached!
% 8.81/2.17 % (2566298)------------------------------
% 8.81/2.17 % (2566298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.81/2.17 % (2566298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.81/2.17 % (2566298)CaDiCaL version: 2.1.3
% 8.81/2.17 % (2566298)Termination reason: Instruction limit
% 8.81/2.17 % (2566298)Termination phase: Saturation
% 8.81/2.17 % (2566298)Time elapsed: 0.069 s
% 8.81/2.17 % (2566298)Peak memory usage: 90 MB
% 8.81/2.17 % (2566298)Instructions burned: 250 (million)
% 8.81/2.17 % (2566301)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1043859085:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 8.81/2.17 % (2566303)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1838751203:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 8.81/2.17 % (2566305)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1010302810:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 8.81/2.17 % (2566304)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2565350895:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 8.81/2.17 % (2566305)Instruction limit reached!
% 8.81/2.17 % (2566305)------------------------------
% 8.81/2.17 % (2566305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.81/2.17 % (2566305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.81/2.17 % (2566305)CaDiCaL version: 2.1.3
% 8.81/2.17 % (2566305)Termination reason: Instruction limit
% 8.81/2.17 % (2566305)Termination phase: Saturation
% 8.81/2.17 % (2566305)Time elapsed: 0.035 s
% 8.81/2.17 % (2566305)Peak memory usage: 90 MB
% 8.81/2.17 % (2566305)Instructions burned: 128 (million)
% 8.81/2.17 % (2566304)Instruction limit reached!
% 8.81/2.17 % (2566304)------------------------------
% 8.81/2.17 % (2566304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.81/2.17 % (2566304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.81/2.17 % (2566304)CaDiCaL version: 2.1.3
% 8.81/2.17 % (2566304)Termination reason: Instruction limit
% 8.81/2.17 % (2566304)Termination phase: Saturation
% 8.81/2.17 % (2566304)Time elapsed: 0.059 s
% 8.81/2.17 % (2566304)Peak memory usage: 91 MB
% 8.81/2.17 % (2566304)Instructions burned: 113 (million)
% 8.81/2.17 % (2566301)Instruction limit reached!
% 8.81/2.17 % (2566301)------------------------------
% 8.81/2.17 % (2566301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.81/2.17 % (2566301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.81/2.17 % (2566301)CaDiCaL version: 2.1.3
% 8.81/2.17 % (2566301)Termination reason: Instruction limit
% 8.81/2.17 % (2566301)Termination phase: Saturation
% 8.81/2.17 % (2566301)Time elapsed: 0.157 s
% 8.81/2.17 % (2566301)Peak memory usage: 96 MB
% 8.81/2.17 % (2566301)Instructions burned: 295 (million)
% 8.81/2.17 % (2566310)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2868958097:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 8.81/2.17 % (2566310)Instruction limit reached!
% 8.81/2.17 % (2566310)------------------------------
% 8.81/2.17 % (2566310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.81/2.17 % (2566310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.81/2.17 % (2566310)CaDiCaL version: 2.1.3
% 8.81/2.17 % (2566310)Termination reason: Instruction limit
% 8.81/2.17 % (2566310)Termination phase: Saturation
% 8.81/2.17 % (2566310)Time elapsed: 0.032 s
% 8.81/2.17 % (2566310)Peak memory usage: 89 MB
% 8.81/2.17 % (2566310)Instructions burned: 118 (million)
% 8.81/2.17 % (2566311)lrs+10_1_sil=8000:sp=occurrence:random_seed=1709609593:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 8.81/2.17 % (2566312)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1886547175:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 8.81/2.17 % (2566314)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3889484335:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 8.81/2.17 % (2566281)First to succeed.
% 8.81/2.17 % (2566281)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2566275"
% 8.81/2.17 % (2566312)Instruction limit reached!
% 8.81/2.17 % (2566312)------------------------------
% 8.81/2.17 % (2566312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.81/2.17 % (2566312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.81/2.17 % (2566312)CaDiCaL version: 2.1.3
% 8.81/2.17 % (2566312)Termination reason: Instruction limit
% 8.81/2.17 % (2566312)Termination phase: Saturation
% 8.81/2.17 % (2566312)Time elapsed: 0.169 s
% 8.81/2.17 % (2566312)Peak memory usage: 93 MB
% 8.81/2.17 % (2566312)Instructions burned: 438 (million)
% 8.81/2.17 % (2566318)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3409280736:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi)
% 8.81/2.17 % (2566311)Instruction limit reached!
% 8.81/2.17 % (2566311)------------------------------
% 8.81/2.17 % (2566311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.81/2.17 % (2566311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.81/2.17 % (2566311)CaDiCaL version: 2.1.3
% 8.81/2.17 % (2566311)Termination reason: Instruction limit
% 8.81/2.17 % (2566311)Termination phase: Saturation
% 8.81/2.17 % (2566311)Time elapsed: 0.410 s
% 8.81/2.17 % (2566311)Peak memory usage: 103 MB
% 8.81/2.17 % (2566311)Instructions burned: 908 (million)
% 8.81/2.17 % (2566281)Refutation found. Thanks to Tanya!
% 8.81/2.17 % SZS status Theorem for theBenchmark
% 8.81/2.17 % SZS output start Proof for theBenchmark
% See solution above
% 9.78/2.36 % (2566281)------------------------------
% 9.78/2.36 % (2566281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.78/2.36 % (2566281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.78/2.36 % (2566281)CaDiCaL version: 2.1.3
% 9.78/2.36 % (2566281)Termination reason: Refutation
% 9.78/2.36 % (2566281)Time elapsed: 0.870 s
% 9.78/2.36 % (2566281)Peak memory usage: 132 MB
% 9.78/2.36 % (2566281)Instructions burned: 1269 (million)
% 9.78/2.36 % (2566281)------------------------------
% 9.78/2.36 % (2566281)------------------------------
% 9.78/2.36 % (2566275)Success in time 1.311 s
% 9.78/2.36 % Vampire exiting
%------------------------------------------------------------------------------