%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL656+1.015 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:54:21 AM UTC 2026
% Result : Theorem 12.78s 2.75s
% Output : Refutation 13.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 50
% Syntax : Number of formulae : 333 ( 25 unt; 48 def)
% Number of atoms : 4757 ( 0 equ)
% Maximal formula atoms : 359 ( 14 avg)
% Number of connectives : 7896 (3472 ~;2921 |;1487 &)
% ( 16 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 94 ( 10 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 83 ( 82 usr; 17 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 1 con; 0-1 aty)
% Number of variables : 1240 ( 0 sgn1118 !; 122 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : r1(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity) ).
fof(f2,conjecture,
~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p7(X1) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ( ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p16(X0)
& ~ p116(X0)
& p115(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p16(X0)
& ~ p116(X0)
& p115(X0) ) ) )
| ~ ( ~ p115(X1)
& p114(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p15(X0)
& ~ p115(X0)
& p114(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p15(X0)
& ~ p115(X0)
& p114(X0) ) ) )
| ~ ( ~ p114(X1)
& p113(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p14(X0)
& ~ p114(X0)
& p113(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p14(X0)
& ~ p114(X0)
& p113(X0) ) ) )
| ~ ( ~ p113(X1)
& p112(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p13(X0)
& ~ p113(X0)
& p112(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p13(X0)
& ~ p113(X0)
& p112(X0) ) ) )
| ~ ( ~ p112(X1)
& p111(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p12(X0)
& ~ p112(X0)
& p111(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p12(X0)
& ~ p112(X0)
& p111(X0) ) ) )
| ~ ( ~ p111(X1)
& p110(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p11(X0)
& ~ p111(X0)
& p110(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p11(X0)
& ~ p111(X0)
& p110(X0) ) ) )
| ~ ( ~ p110(X1)
& p109(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p10(X0)
& ~ p110(X0)
& p109(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p10(X0)
& ~ p110(X0)
& p109(X0) ) ) )
| ~ ( ~ p109(X1)
& p108(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p9(X0)
& ~ p109(X0)
& p108(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p9(X0)
& ~ p109(X0)
& p108(X0) ) ) )
| ~ ( ~ p108(X1)
& p107(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p8(X0)
& ~ p108(X0)
& p107(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p8(X0)
& ~ p108(X0)
& p107(X0) ) ) )
| ~ ( ~ p107(X1)
& p106(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p7(X0)
& ~ p107(X0)
& p106(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p7(X0)
& ~ p107(X0)
& p106(X0) ) ) )
| ~ ( ~ p106(X1)
& p105(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p6(X0)
& ~ p106(X0)
& p105(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p6(X0)
& ~ p106(X0)
& p105(X0) ) ) )
| ~ ( ~ p105(X1)
& p104(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p5(X0)
& ~ p105(X0)
& p104(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p5(X0)
& ~ p105(X0)
& p104(X0) ) ) )
| ~ ( ~ p104(X1)
& p103(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p4(X0)
& ~ p104(X0)
& p103(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p4(X0)
& ~ p104(X0)
& p103(X0) ) ) )
| ~ ( ~ p103(X1)
& p102(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p3(X0)
& ~ p103(X0)
& p102(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p3(X0)
& ~ p103(X0)
& p102(X0) ) ) )
| ~ ( ~ p102(X1)
& p101(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p2(X0)
& ~ p102(X0)
& p101(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
& ~ p102(X0)
& p101(X0) ) ) )
| ~ ( ~ p101(X1)
& p100(X1) ) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p16(X0)
| ~ p115(X0) )
| p16(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p16(X0)
| ~ p115(X0) )
| ~ p16(X1) ) )
| ~ p115(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p15(X0)
| ~ p114(X0) )
| p15(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p15(X0)
| ~ p114(X0) )
| ~ p15(X1) ) )
| ~ p114(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p14(X0)
| ~ p113(X0) )
| p14(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p14(X0)
| ~ p113(X0) )
| ~ p14(X1) ) )
| ~ p113(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p13(X0)
| ~ p112(X0) )
| p13(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p13(X0)
| ~ p112(X0) )
| ~ p13(X1) ) )
| ~ p112(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p12(X0)
| ~ p111(X0) )
| p12(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p12(X0)
| ~ p111(X0) )
| ~ p12(X1) ) )
| ~ p111(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p11(X0)
| ~ p110(X0) )
| p11(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p11(X0)
| ~ p110(X0) )
| ~ p11(X1) ) )
| ~ p110(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p10(X0)
| ~ p109(X0) )
| p10(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p10(X0)
| ~ p109(X0) )
| ~ p10(X1) ) )
| ~ p109(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p9(X0)
| ~ p108(X0) )
| p9(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p9(X0)
| ~ p108(X0) )
| ~ p9(X1) ) )
| ~ p108(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p8(X0)
| ~ p107(X0) )
| p8(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p8(X0)
| ~ p107(X0) )
| ~ p8(X1) ) )
| ~ p107(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p7(X0)
| ~ p106(X0) )
| p7(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p7(X0)
| ~ p106(X0) )
| ~ p7(X1) ) )
| ~ p106(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p6(X0)
| ~ p105(X0) )
| p6(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p6(X0)
| ~ p105(X0) )
| ~ p6(X1) ) )
| ~ p105(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p5(X0)
| ~ p104(X0) )
| p5(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p5(X0)
| ~ p104(X0) )
| ~ p5(X1) ) )
| ~ p104(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p4(X0)
| ~ p103(X0) )
| p4(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| ~ p103(X0) )
| ~ p4(X1) ) )
| ~ p103(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p3(X0)
| ~ p102(X0) )
| p3(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p3(X0)
| ~ p102(X0) )
| ~ p3(X1) ) )
| ~ p102(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p2(X0)
| ~ p101(X0) )
| p2(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ p101(X0) )
| ~ p2(X1) ) )
| ~ p101(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0)
| ~ p100(X0) )
| p1(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ p100(X0) )
| ~ p1(X1) ) )
| ~ p100(X1) )
& ( p115(X1)
| ~ p116(X1) )
& ( p114(X1)
| ~ p115(X1) )
& ( p113(X1)
| ~ p114(X1) )
& ( p112(X1)
| ~ p113(X1) )
& ( p111(X1)
| ~ p112(X1) )
& ( p110(X1)
| ~ p111(X1) )
& ( p109(X1)
| ~ p110(X1) )
& ( p108(X1)
| ~ p109(X1) )
& ( p107(X1)
| ~ p108(X1) )
& ( p106(X1)
| ~ p107(X1) )
& ( p105(X1)
| ~ p106(X1) )
& ( p104(X1)
| ~ p105(X1) )
& ( p103(X1)
| ~ p104(X1) )
& ( p102(X1)
| ~ p103(X1) )
& ( p101(X1)
| ~ p102(X1) )
& ( p100(X1)
| ~ p101(X1) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ~ p101(X0)
& p100(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',main) ).
fof(f3,negated_conjecture,
~ ~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p7(X1) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ( ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p16(X0)
& ~ p116(X0)
& p115(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p16(X0)
& ~ p116(X0)
& p115(X0) ) ) )
| ~ ( ~ p115(X1)
& p114(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p15(X0)
& ~ p115(X0)
& p114(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p15(X0)
& ~ p115(X0)
& p114(X0) ) ) )
| ~ ( ~ p114(X1)
& p113(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p14(X0)
& ~ p114(X0)
& p113(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p14(X0)
& ~ p114(X0)
& p113(X0) ) ) )
| ~ ( ~ p113(X1)
& p112(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p13(X0)
& ~ p113(X0)
& p112(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p13(X0)
& ~ p113(X0)
& p112(X0) ) ) )
| ~ ( ~ p112(X1)
& p111(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p12(X0)
& ~ p112(X0)
& p111(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p12(X0)
& ~ p112(X0)
& p111(X0) ) ) )
| ~ ( ~ p111(X1)
& p110(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p11(X0)
& ~ p111(X0)
& p110(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p11(X0)
& ~ p111(X0)
& p110(X0) ) ) )
| ~ ( ~ p110(X1)
& p109(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p10(X0)
& ~ p110(X0)
& p109(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p10(X0)
& ~ p110(X0)
& p109(X0) ) ) )
| ~ ( ~ p109(X1)
& p108(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p9(X0)
& ~ p109(X0)
& p108(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p9(X0)
& ~ p109(X0)
& p108(X0) ) ) )
| ~ ( ~ p108(X1)
& p107(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p8(X0)
& ~ p108(X0)
& p107(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p8(X0)
& ~ p108(X0)
& p107(X0) ) ) )
| ~ ( ~ p107(X1)
& p106(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p7(X0)
& ~ p107(X0)
& p106(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p7(X0)
& ~ p107(X0)
& p106(X0) ) ) )
| ~ ( ~ p106(X1)
& p105(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p6(X0)
& ~ p106(X0)
& p105(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p6(X0)
& ~ p106(X0)
& p105(X0) ) ) )
| ~ ( ~ p105(X1)
& p104(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p5(X0)
& ~ p105(X0)
& p104(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p5(X0)
& ~ p105(X0)
& p104(X0) ) ) )
| ~ ( ~ p104(X1)
& p103(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p4(X0)
& ~ p104(X0)
& p103(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p4(X0)
& ~ p104(X0)
& p103(X0) ) ) )
| ~ ( ~ p103(X1)
& p102(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p3(X0)
& ~ p103(X0)
& p102(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p3(X0)
& ~ p103(X0)
& p102(X0) ) ) )
| ~ ( ~ p102(X1)
& p101(X1) ) )
& ( ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ p2(X0)
& ~ p102(X0)
& p101(X0) ) )
& ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
& ~ p102(X0)
& p101(X0) ) ) )
| ~ ( ~ p101(X1)
& p100(X1) ) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p16(X0)
| ~ p115(X0) )
| p16(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p16(X0)
| ~ p115(X0) )
| ~ p16(X1) ) )
| ~ p115(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p15(X0)
| ~ p114(X0) )
| p15(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p15(X0)
| ~ p114(X0) )
| ~ p15(X1) ) )
| ~ p114(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p14(X0)
| ~ p113(X0) )
| p14(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p14(X0)
| ~ p113(X0) )
| ~ p14(X1) ) )
| ~ p113(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p13(X0)
| ~ p112(X0) )
| p13(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p13(X0)
| ~ p112(X0) )
| ~ p13(X1) ) )
| ~ p112(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p12(X0)
| ~ p111(X0) )
| p12(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p12(X0)
| ~ p111(X0) )
| ~ p12(X1) ) )
| ~ p111(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p11(X0)
| ~ p110(X0) )
| p11(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p11(X0)
| ~ p110(X0) )
| ~ p11(X1) ) )
| ~ p110(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p10(X0)
| ~ p109(X0) )
| p10(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p10(X0)
| ~ p109(X0) )
| ~ p10(X1) ) )
| ~ p109(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p9(X0)
| ~ p108(X0) )
| p9(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p9(X0)
| ~ p108(X0) )
| ~ p9(X1) ) )
| ~ p108(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p8(X0)
| ~ p107(X0) )
| p8(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p8(X0)
| ~ p107(X0) )
| ~ p8(X1) ) )
| ~ p107(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p7(X0)
| ~ p106(X0) )
| p7(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p7(X0)
| ~ p106(X0) )
| ~ p7(X1) ) )
| ~ p106(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p6(X0)
| ~ p105(X0) )
| p6(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p6(X0)
| ~ p105(X0) )
| ~ p6(X1) ) )
| ~ p105(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p5(X0)
| ~ p104(X0) )
| p5(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p5(X0)
| ~ p104(X0) )
| ~ p5(X1) ) )
| ~ p104(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p4(X0)
| ~ p103(X0) )
| p4(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| ~ p103(X0) )
| ~ p4(X1) ) )
| ~ p103(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p3(X0)
| ~ p102(X0) )
| p3(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p3(X0)
| ~ p102(X0) )
| ~ p3(X1) ) )
| ~ p102(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p2(X0)
| ~ p101(X0) )
| p2(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ p101(X0) )
| ~ p2(X1) ) )
| ~ p101(X1) )
& ( ( ( ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0)
| ~ p100(X0) )
| p1(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ p100(X0) )
| ~ p1(X1) ) )
| ~ p100(X1) )
& ( p115(X1)
| ~ p116(X1) )
& ( p114(X1)
| ~ p115(X1) )
& ( p113(X1)
| ~ p114(X1) )
& ( p112(X1)
| ~ p113(X1) )
& ( p111(X1)
| ~ p112(X1) )
& ( p110(X1)
| ~ p111(X1) )
& ( p109(X1)
| ~ p110(X1) )
& ( p108(X1)
| ~ p109(X1) )
& ( p107(X1)
| ~ p108(X1) )
& ( p106(X1)
| ~ p107(X1) )
& ( p105(X1)
| ~ p106(X1) )
& ( p104(X1)
| ~ p105(X1) )
& ( p103(X1)
| ~ p104(X1) )
& ( p102(X1)
| ~ p103(X1) )
& ( p101(X1)
| ~ p102(X1) )
& ( p100(X1)
| ~ p101(X1) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ~ p101(X0)
& p100(X0) ) ),
inference(negated_conjecture,[status(cth)],[f2]) ).
fof(f4,plain,
~ ~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| p7(X15) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ( ! [X16] :
( ~ r1(X0,X16)
| ! [X17] :
( ~ r1(X16,X17)
| ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ( ( ( ~ ! [X31] :
( ~ r1(X30,X31)
| ~ ( ~ p16(X31)
& ~ p116(X31)
& p115(X31) ) )
& ~ ! [X32] :
( ~ r1(X30,X32)
| ~ ( p16(X32)
& ~ p116(X32)
& p115(X32) ) ) )
| ~ ( ~ p115(X30)
& p114(X30) ) )
& ( ( ~ ! [X33] :
( ~ r1(X30,X33)
| ~ ( ~ p15(X33)
& ~ p115(X33)
& p114(X33) ) )
& ~ ! [X34] :
( ~ r1(X30,X34)
| ~ ( p15(X34)
& ~ p115(X34)
& p114(X34) ) ) )
| ~ ( ~ p114(X30)
& p113(X30) ) )
& ( ( ~ ! [X35] :
( ~ r1(X30,X35)
| ~ ( ~ p14(X35)
& ~ p114(X35)
& p113(X35) ) )
& ~ ! [X36] :
( ~ r1(X30,X36)
| ~ ( p14(X36)
& ~ p114(X36)
& p113(X36) ) ) )
| ~ ( ~ p113(X30)
& p112(X30) ) )
& ( ( ~ ! [X37] :
( ~ r1(X30,X37)
| ~ ( ~ p13(X37)
& ~ p113(X37)
& p112(X37) ) )
& ~ ! [X38] :
( ~ r1(X30,X38)
| ~ ( p13(X38)
& ~ p113(X38)
& p112(X38) ) ) )
| ~ ( ~ p112(X30)
& p111(X30) ) )
& ( ( ~ ! [X39] :
( ~ r1(X30,X39)
| ~ ( ~ p12(X39)
& ~ p112(X39)
& p111(X39) ) )
& ~ ! [X40] :
( ~ r1(X30,X40)
| ~ ( p12(X40)
& ~ p112(X40)
& p111(X40) ) ) )
| ~ ( ~ p111(X30)
& p110(X30) ) )
& ( ( ~ ! [X41] :
( ~ r1(X30,X41)
| ~ ( ~ p11(X41)
& ~ p111(X41)
& p110(X41) ) )
& ~ ! [X42] :
( ~ r1(X30,X42)
| ~ ( p11(X42)
& ~ p111(X42)
& p110(X42) ) ) )
| ~ ( ~ p110(X30)
& p109(X30) ) )
& ( ( ~ ! [X43] :
( ~ r1(X30,X43)
| ~ ( ~ p10(X43)
& ~ p110(X43)
& p109(X43) ) )
& ~ ! [X44] :
( ~ r1(X30,X44)
| ~ ( p10(X44)
& ~ p110(X44)
& p109(X44) ) ) )
| ~ ( ~ p109(X30)
& p108(X30) ) )
& ( ( ~ ! [X45] :
( ~ r1(X30,X45)
| ~ ( ~ p9(X45)
& ~ p109(X45)
& p108(X45) ) )
& ~ ! [X46] :
( ~ r1(X30,X46)
| ~ ( p9(X46)
& ~ p109(X46)
& p108(X46) ) ) )
| ~ ( ~ p108(X30)
& p107(X30) ) )
& ( ( ~ ! [X47] :
( ~ r1(X30,X47)
| ~ ( ~ p8(X47)
& ~ p108(X47)
& p107(X47) ) )
& ~ ! [X48] :
( ~ r1(X30,X48)
| ~ ( p8(X48)
& ~ p108(X48)
& p107(X48) ) ) )
| ~ ( ~ p107(X30)
& p106(X30) ) )
& ( ( ~ ! [X49] :
( ~ r1(X30,X49)
| ~ ( ~ p7(X49)
& ~ p107(X49)
& p106(X49) ) )
& ~ ! [X50] :
( ~ r1(X30,X50)
| ~ ( p7(X50)
& ~ p107(X50)
& p106(X50) ) ) )
| ~ ( ~ p106(X30)
& p105(X30) ) )
& ( ( ~ ! [X51] :
( ~ r1(X30,X51)
| ~ ( ~ p6(X51)
& ~ p106(X51)
& p105(X51) ) )
& ~ ! [X52] :
( ~ r1(X30,X52)
| ~ ( p6(X52)
& ~ p106(X52)
& p105(X52) ) ) )
| ~ ( ~ p105(X30)
& p104(X30) ) )
& ( ( ~ ! [X53] :
( ~ r1(X30,X53)
| ~ ( ~ p5(X53)
& ~ p105(X53)
& p104(X53) ) )
& ~ ! [X54] :
( ~ r1(X30,X54)
| ~ ( p5(X54)
& ~ p105(X54)
& p104(X54) ) ) )
| ~ ( ~ p104(X30)
& p103(X30) ) )
& ( ( ~ ! [X55] :
( ~ r1(X30,X55)
| ~ ( ~ p4(X55)
& ~ p104(X55)
& p103(X55) ) )
& ~ ! [X56] :
( ~ r1(X30,X56)
| ~ ( p4(X56)
& ~ p104(X56)
& p103(X56) ) ) )
| ~ ( ~ p103(X30)
& p102(X30) ) )
& ( ( ~ ! [X57] :
( ~ r1(X30,X57)
| ~ ( ~ p3(X57)
& ~ p103(X57)
& p102(X57) ) )
& ~ ! [X58] :
( ~ r1(X30,X58)
| ~ ( p3(X58)
& ~ p103(X58)
& p102(X58) ) ) )
| ~ ( ~ p102(X30)
& p101(X30) ) )
& ( ( ~ ! [X59] :
( ~ r1(X30,X59)
| ~ ( ~ p2(X59)
& ~ p102(X59)
& p101(X59) ) )
& ~ ! [X60] :
( ~ r1(X30,X60)
| ~ ( p2(X60)
& ~ p102(X60)
& p101(X60) ) ) )
| ~ ( ~ p101(X30)
& p100(X30) ) )
& ( ( ( ! [X61] :
( ~ r1(X30,X61)
| ~ p16(X61)
| ~ p115(X61) )
| p16(X30) )
& ( ! [X62] :
( ~ r1(X30,X62)
| p16(X62)
| ~ p115(X62) )
| ~ p16(X30) ) )
| ~ p115(X30) )
& ( ( ( ! [X63] :
( ~ r1(X30,X63)
| ~ p15(X63)
| ~ p114(X63) )
| p15(X30) )
& ( ! [X64] :
( ~ r1(X30,X64)
| p15(X64)
| ~ p114(X64) )
| ~ p15(X30) ) )
| ~ p114(X30) )
& ( ( ( ! [X65] :
( ~ r1(X30,X65)
| ~ p14(X65)
| ~ p113(X65) )
| p14(X30) )
& ( ! [X66] :
( ~ r1(X30,X66)
| p14(X66)
| ~ p113(X66) )
| ~ p14(X30) ) )
| ~ p113(X30) )
& ( ( ( ! [X67] :
( ~ r1(X30,X67)
| ~ p13(X67)
| ~ p112(X67) )
| p13(X30) )
& ( ! [X68] :
( ~ r1(X30,X68)
| p13(X68)
| ~ p112(X68) )
| ~ p13(X30) ) )
| ~ p112(X30) )
& ( ( ( ! [X69] :
( ~ r1(X30,X69)
| ~ p12(X69)
| ~ p111(X69) )
| p12(X30) )
& ( ! [X70] :
( ~ r1(X30,X70)
| p12(X70)
| ~ p111(X70) )
| ~ p12(X30) ) )
| ~ p111(X30) )
& ( ( ( ! [X71] :
( ~ r1(X30,X71)
| ~ p11(X71)
| ~ p110(X71) )
| p11(X30) )
& ( ! [X72] :
( ~ r1(X30,X72)
| p11(X72)
| ~ p110(X72) )
| ~ p11(X30) ) )
| ~ p110(X30) )
& ( ( ( ! [X73] :
( ~ r1(X30,X73)
| ~ p10(X73)
| ~ p109(X73) )
| p10(X30) )
& ( ! [X74] :
( ~ r1(X30,X74)
| p10(X74)
| ~ p109(X74) )
| ~ p10(X30) ) )
| ~ p109(X30) )
& ( ( ( ! [X75] :
( ~ r1(X30,X75)
| ~ p9(X75)
| ~ p108(X75) )
| p9(X30) )
& ( ! [X76] :
( ~ r1(X30,X76)
| p9(X76)
| ~ p108(X76) )
| ~ p9(X30) ) )
| ~ p108(X30) )
& ( ( ( ! [X77] :
( ~ r1(X30,X77)
| ~ p8(X77)
| ~ p107(X77) )
| p8(X30) )
& ( ! [X78] :
( ~ r1(X30,X78)
| p8(X78)
| ~ p107(X78) )
| ~ p8(X30) ) )
| ~ p107(X30) )
& ( ( ( ! [X79] :
( ~ r1(X30,X79)
| ~ p7(X79)
| ~ p106(X79) )
| p7(X30) )
& ( ! [X80] :
( ~ r1(X30,X80)
| p7(X80)
| ~ p106(X80) )
| ~ p7(X30) ) )
| ~ p106(X30) )
& ( ( ( ! [X81] :
( ~ r1(X30,X81)
| ~ p6(X81)
| ~ p105(X81) )
| p6(X30) )
& ( ! [X82] :
( ~ r1(X30,X82)
| p6(X82)
| ~ p105(X82) )
| ~ p6(X30) ) )
| ~ p105(X30) )
& ( ( ( ! [X83] :
( ~ r1(X30,X83)
| ~ p5(X83)
| ~ p104(X83) )
| p5(X30) )
& ( ! [X84] :
( ~ r1(X30,X84)
| p5(X84)
| ~ p104(X84) )
| ~ p5(X30) ) )
| ~ p104(X30) )
& ( ( ( ! [X85] :
( ~ r1(X30,X85)
| ~ p4(X85)
| ~ p103(X85) )
| p4(X30) )
& ( ! [X86] :
( ~ r1(X30,X86)
| p4(X86)
| ~ p103(X86) )
| ~ p4(X30) ) )
| ~ p103(X30) )
& ( ( ( ! [X87] :
( ~ r1(X30,X87)
| ~ p3(X87)
| ~ p102(X87) )
| p3(X30) )
& ( ! [X88] :
( ~ r1(X30,X88)
| p3(X88)
| ~ p102(X88) )
| ~ p3(X30) ) )
| ~ p102(X30) )
& ( ( ( ! [X89] :
( ~ r1(X30,X89)
| ~ p2(X89)
| ~ p101(X89) )
| p2(X30) )
& ( ! [X90] :
( ~ r1(X30,X90)
| p2(X90)
| ~ p101(X90) )
| ~ p2(X30) ) )
| ~ p101(X30) )
& ( ( ( ! [X91] :
( ~ r1(X30,X91)
| ~ p1(X91)
| ~ p100(X91) )
| p1(X30) )
& ( ! [X92] :
( ~ r1(X30,X92)
| p1(X92)
| ~ p100(X92) )
| ~ p1(X30) ) )
| ~ p100(X30) )
& ( p115(X30)
| ~ p116(X30) )
& ( p114(X30)
| ~ p115(X30) )
& ( p113(X30)
| ~ p114(X30) )
& ( p112(X30)
| ~ p113(X30) )
& ( p111(X30)
| ~ p112(X30) )
& ( p110(X30)
| ~ p111(X30) )
& ( p109(X30)
| ~ p110(X30) )
& ( p108(X30)
| ~ p109(X30) )
& ( p107(X30)
| ~ p108(X30) )
& ( p106(X30)
| ~ p107(X30) )
& ( p105(X30)
| ~ p106(X30) )
& ( p104(X30)
| ~ p105(X30) )
& ( p103(X30)
| ~ p104(X30) )
& ( p102(X30)
| ~ p103(X30) )
& ( p101(X30)
| ~ p102(X30) )
& ( p100(X30)
| ~ p101(X30) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ~ p101(X0)
& p100(X0) ) ),
inference(rectify,[],[f3]) ).
fof(f5,plain,
? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| p7(X15) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ( ! [X16] :
( ~ r1(X0,X16)
| ! [X17] :
( ~ r1(X16,X17)
| ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ( ( ( ~ ! [X31] :
( ~ r1(X30,X31)
| ~ ( ~ p16(X31)
& ~ p116(X31)
& p115(X31) ) )
& ~ ! [X32] :
( ~ r1(X30,X32)
| ~ ( p16(X32)
& ~ p116(X32)
& p115(X32) ) ) )
| ~ ( ~ p115(X30)
& p114(X30) ) )
& ( ( ~ ! [X33] :
( ~ r1(X30,X33)
| ~ ( ~ p15(X33)
& ~ p115(X33)
& p114(X33) ) )
& ~ ! [X34] :
( ~ r1(X30,X34)
| ~ ( p15(X34)
& ~ p115(X34)
& p114(X34) ) ) )
| ~ ( ~ p114(X30)
& p113(X30) ) )
& ( ( ~ ! [X35] :
( ~ r1(X30,X35)
| ~ ( ~ p14(X35)
& ~ p114(X35)
& p113(X35) ) )
& ~ ! [X36] :
( ~ r1(X30,X36)
| ~ ( p14(X36)
& ~ p114(X36)
& p113(X36) ) ) )
| ~ ( ~ p113(X30)
& p112(X30) ) )
& ( ( ~ ! [X37] :
( ~ r1(X30,X37)
| ~ ( ~ p13(X37)
& ~ p113(X37)
& p112(X37) ) )
& ~ ! [X38] :
( ~ r1(X30,X38)
| ~ ( p13(X38)
& ~ p113(X38)
& p112(X38) ) ) )
| ~ ( ~ p112(X30)
& p111(X30) ) )
& ( ( ~ ! [X39] :
( ~ r1(X30,X39)
| ~ ( ~ p12(X39)
& ~ p112(X39)
& p111(X39) ) )
& ~ ! [X40] :
( ~ r1(X30,X40)
| ~ ( p12(X40)
& ~ p112(X40)
& p111(X40) ) ) )
| ~ ( ~ p111(X30)
& p110(X30) ) )
& ( ( ~ ! [X41] :
( ~ r1(X30,X41)
| ~ ( ~ p11(X41)
& ~ p111(X41)
& p110(X41) ) )
& ~ ! [X42] :
( ~ r1(X30,X42)
| ~ ( p11(X42)
& ~ p111(X42)
& p110(X42) ) ) )
| ~ ( ~ p110(X30)
& p109(X30) ) )
& ( ( ~ ! [X43] :
( ~ r1(X30,X43)
| ~ ( ~ p10(X43)
& ~ p110(X43)
& p109(X43) ) )
& ~ ! [X44] :
( ~ r1(X30,X44)
| ~ ( p10(X44)
& ~ p110(X44)
& p109(X44) ) ) )
| ~ ( ~ p109(X30)
& p108(X30) ) )
& ( ( ~ ! [X45] :
( ~ r1(X30,X45)
| ~ ( ~ p9(X45)
& ~ p109(X45)
& p108(X45) ) )
& ~ ! [X46] :
( ~ r1(X30,X46)
| ~ ( p9(X46)
& ~ p109(X46)
& p108(X46) ) ) )
| ~ ( ~ p108(X30)
& p107(X30) ) )
& ( ( ~ ! [X47] :
( ~ r1(X30,X47)
| ~ ( ~ p8(X47)
& ~ p108(X47)
& p107(X47) ) )
& ~ ! [X48] :
( ~ r1(X30,X48)
| ~ ( p8(X48)
& ~ p108(X48)
& p107(X48) ) ) )
| ~ ( ~ p107(X30)
& p106(X30) ) )
& ( ( ~ ! [X49] :
( ~ r1(X30,X49)
| ~ ( ~ p7(X49)
& ~ p107(X49)
& p106(X49) ) )
& ~ ! [X50] :
( ~ r1(X30,X50)
| ~ ( p7(X50)
& ~ p107(X50)
& p106(X50) ) ) )
| ~ ( ~ p106(X30)
& p105(X30) ) )
& ( ( ~ ! [X51] :
( ~ r1(X30,X51)
| ~ ( ~ p6(X51)
& ~ p106(X51)
& p105(X51) ) )
& ~ ! [X52] :
( ~ r1(X30,X52)
| ~ ( p6(X52)
& ~ p106(X52)
& p105(X52) ) ) )
| ~ ( ~ p105(X30)
& p104(X30) ) )
& ( ( ~ ! [X53] :
( ~ r1(X30,X53)
| ~ ( ~ p5(X53)
& ~ p105(X53)
& p104(X53) ) )
& ~ ! [X54] :
( ~ r1(X30,X54)
| ~ ( p5(X54)
& ~ p105(X54)
& p104(X54) ) ) )
| ~ ( ~ p104(X30)
& p103(X30) ) )
& ( ( ~ ! [X55] :
( ~ r1(X30,X55)
| ~ ( ~ p4(X55)
& ~ p104(X55)
& p103(X55) ) )
& ~ ! [X56] :
( ~ r1(X30,X56)
| ~ ( p4(X56)
& ~ p104(X56)
& p103(X56) ) ) )
| ~ ( ~ p103(X30)
& p102(X30) ) )
& ( ( ~ ! [X57] :
( ~ r1(X30,X57)
| ~ ( ~ p3(X57)
& ~ p103(X57)
& p102(X57) ) )
& ~ ! [X58] :
( ~ r1(X30,X58)
| ~ ( p3(X58)
& ~ p103(X58)
& p102(X58) ) ) )
| ~ ( ~ p102(X30)
& p101(X30) ) )
& ( ( ~ ! [X59] :
( ~ r1(X30,X59)
| ~ ( ~ p2(X59)
& ~ p102(X59)
& p101(X59) ) )
& ~ ! [X60] :
( ~ r1(X30,X60)
| ~ ( p2(X60)
& ~ p102(X60)
& p101(X60) ) ) )
| ~ ( ~ p101(X30)
& p100(X30) ) )
& ( ( ( ! [X61] :
( ~ r1(X30,X61)
| ~ p16(X61)
| ~ p115(X61) )
| p16(X30) )
& ( ! [X62] :
( ~ r1(X30,X62)
| p16(X62)
| ~ p115(X62) )
| ~ p16(X30) ) )
| ~ p115(X30) )
& ( ( ( ! [X63] :
( ~ r1(X30,X63)
| ~ p15(X63)
| ~ p114(X63) )
| p15(X30) )
& ( ! [X64] :
( ~ r1(X30,X64)
| p15(X64)
| ~ p114(X64) )
| ~ p15(X30) ) )
| ~ p114(X30) )
& ( ( ( ! [X65] :
( ~ r1(X30,X65)
| ~ p14(X65)
| ~ p113(X65) )
| p14(X30) )
& ( ! [X66] :
( ~ r1(X30,X66)
| p14(X66)
| ~ p113(X66) )
| ~ p14(X30) ) )
| ~ p113(X30) )
& ( ( ( ! [X67] :
( ~ r1(X30,X67)
| ~ p13(X67)
| ~ p112(X67) )
| p13(X30) )
& ( ! [X68] :
( ~ r1(X30,X68)
| p13(X68)
| ~ p112(X68) )
| ~ p13(X30) ) )
| ~ p112(X30) )
& ( ( ( ! [X69] :
( ~ r1(X30,X69)
| ~ p12(X69)
| ~ p111(X69) )
| p12(X30) )
& ( ! [X70] :
( ~ r1(X30,X70)
| p12(X70)
| ~ p111(X70) )
| ~ p12(X30) ) )
| ~ p111(X30) )
& ( ( ( ! [X71] :
( ~ r1(X30,X71)
| ~ p11(X71)
| ~ p110(X71) )
| p11(X30) )
& ( ! [X72] :
( ~ r1(X30,X72)
| p11(X72)
| ~ p110(X72) )
| ~ p11(X30) ) )
| ~ p110(X30) )
& ( ( ( ! [X73] :
( ~ r1(X30,X73)
| ~ p10(X73)
| ~ p109(X73) )
| p10(X30) )
& ( ! [X74] :
( ~ r1(X30,X74)
| p10(X74)
| ~ p109(X74) )
| ~ p10(X30) ) )
| ~ p109(X30) )
& ( ( ( ! [X75] :
( ~ r1(X30,X75)
| ~ p9(X75)
| ~ p108(X75) )
| p9(X30) )
& ( ! [X76] :
( ~ r1(X30,X76)
| p9(X76)
| ~ p108(X76) )
| ~ p9(X30) ) )
| ~ p108(X30) )
& ( ( ( ! [X77] :
( ~ r1(X30,X77)
| ~ p8(X77)
| ~ p107(X77) )
| p8(X30) )
& ( ! [X78] :
( ~ r1(X30,X78)
| p8(X78)
| ~ p107(X78) )
| ~ p8(X30) ) )
| ~ p107(X30) )
& ( ( ( ! [X79] :
( ~ r1(X30,X79)
| ~ p7(X79)
| ~ p106(X79) )
| p7(X30) )
& ( ! [X80] :
( ~ r1(X30,X80)
| p7(X80)
| ~ p106(X80) )
| ~ p7(X30) ) )
| ~ p106(X30) )
& ( ( ( ! [X81] :
( ~ r1(X30,X81)
| ~ p6(X81)
| ~ p105(X81) )
| p6(X30) )
& ( ! [X82] :
( ~ r1(X30,X82)
| p6(X82)
| ~ p105(X82) )
| ~ p6(X30) ) )
| ~ p105(X30) )
& ( ( ( ! [X83] :
( ~ r1(X30,X83)
| ~ p5(X83)
| ~ p104(X83) )
| p5(X30) )
& ( ! [X84] :
( ~ r1(X30,X84)
| p5(X84)
| ~ p104(X84) )
| ~ p5(X30) ) )
| ~ p104(X30) )
& ( ( ( ! [X85] :
( ~ r1(X30,X85)
| ~ p4(X85)
| ~ p103(X85) )
| p4(X30) )
& ( ! [X86] :
( ~ r1(X30,X86)
| p4(X86)
| ~ p103(X86) )
| ~ p4(X30) ) )
| ~ p103(X30) )
& ( ( ( ! [X87] :
( ~ r1(X30,X87)
| ~ p3(X87)
| ~ p102(X87) )
| p3(X30) )
& ( ! [X88] :
( ~ r1(X30,X88)
| p3(X88)
| ~ p102(X88) )
| ~ p3(X30) ) )
| ~ p102(X30) )
& ( ( ( ! [X89] :
( ~ r1(X30,X89)
| ~ p2(X89)
| ~ p101(X89) )
| p2(X30) )
& ( ! [X90] :
( ~ r1(X30,X90)
| p2(X90)
| ~ p101(X90) )
| ~ p2(X30) ) )
| ~ p101(X30) )
& ( ( ( ! [X91] :
( ~ r1(X30,X91)
| ~ p1(X91)
| ~ p100(X91) )
| p1(X30) )
& ( ! [X92] :
( ~ r1(X30,X92)
| p1(X92)
| ~ p100(X92) )
| ~ p1(X30) ) )
| ~ p100(X30) )
& ( p115(X30)
| ~ p116(X30) )
& ( p114(X30)
| ~ p115(X30) )
& ( p113(X30)
| ~ p114(X30) )
& ( p112(X30)
| ~ p113(X30) )
& ( p111(X30)
| ~ p112(X30) )
& ( p110(X30)
| ~ p111(X30) )
& ( p109(X30)
| ~ p110(X30) )
& ( p108(X30)
| ~ p109(X30) )
& ( p107(X30)
| ~ p108(X30) )
& ( p106(X30)
| ~ p107(X30) )
& ( p105(X30)
| ~ p106(X30) )
& ( p104(X30)
| ~ p105(X30) )
& ( p103(X30)
| ~ p104(X30) )
& ( p102(X30)
| ~ p103(X30) )
& ( p101(X30)
| ~ p102(X30) )
& ( p100(X30)
| ~ p101(X30) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ~ p101(X0)
& p100(X0) ) ),
inference(flattening,[],[f4]) ).
fof(f6,plain,
? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| p7(X15) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ( ! [X16] :
( ~ r1(X0,X16)
| ! [X17] :
( ~ r1(X16,X17)
| ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ( ( ( ~ ! [X31] :
( ~ r1(X30,X31)
| ~ ( ~ p16(X31)
& p115(X31) ) )
& ~ ! [X32] :
( ~ r1(X30,X32)
| ~ ( p16(X32)
& p115(X32) ) ) )
| ~ ( ~ p115(X30)
& p114(X30) ) )
& ( ( ~ ! [X33] :
( ~ r1(X30,X33)
| ~ ( ~ p15(X33)
& ~ p115(X33)
& p114(X33) ) )
& ~ ! [X34] :
( ~ r1(X30,X34)
| ~ ( p15(X34)
& ~ p115(X34)
& p114(X34) ) ) )
| ~ ( ~ p114(X30)
& p113(X30) ) )
& ( ( ~ ! [X35] :
( ~ r1(X30,X35)
| ~ ( ~ p14(X35)
& ~ p114(X35)
& p113(X35) ) )
& ~ ! [X36] :
( ~ r1(X30,X36)
| ~ ( p14(X36)
& ~ p114(X36)
& p113(X36) ) ) )
| ~ ( ~ p113(X30)
& p112(X30) ) )
& ( ( ~ ! [X37] :
( ~ r1(X30,X37)
| ~ ( ~ p13(X37)
& ~ p113(X37)
& p112(X37) ) )
& ~ ! [X38] :
( ~ r1(X30,X38)
| ~ ( p13(X38)
& ~ p113(X38)
& p112(X38) ) ) )
| ~ ( ~ p112(X30)
& p111(X30) ) )
& ( ( ~ ! [X39] :
( ~ r1(X30,X39)
| ~ ( ~ p12(X39)
& ~ p112(X39)
& p111(X39) ) )
& ~ ! [X40] :
( ~ r1(X30,X40)
| ~ ( p12(X40)
& ~ p112(X40)
& p111(X40) ) ) )
| ~ ( ~ p111(X30)
& p110(X30) ) )
& ( ( ~ ! [X41] :
( ~ r1(X30,X41)
| ~ ( ~ p11(X41)
& ~ p111(X41)
& p110(X41) ) )
& ~ ! [X42] :
( ~ r1(X30,X42)
| ~ ( p11(X42)
& ~ p111(X42)
& p110(X42) ) ) )
| ~ ( ~ p110(X30)
& p109(X30) ) )
& ( ( ~ ! [X43] :
( ~ r1(X30,X43)
| ~ ( ~ p10(X43)
& ~ p110(X43)
& p109(X43) ) )
& ~ ! [X44] :
( ~ r1(X30,X44)
| ~ ( p10(X44)
& ~ p110(X44)
& p109(X44) ) ) )
| ~ ( ~ p109(X30)
& p108(X30) ) )
& ( ( ~ ! [X45] :
( ~ r1(X30,X45)
| ~ ( ~ p9(X45)
& ~ p109(X45)
& p108(X45) ) )
& ~ ! [X46] :
( ~ r1(X30,X46)
| ~ ( p9(X46)
& ~ p109(X46)
& p108(X46) ) ) )
| ~ ( ~ p108(X30)
& p107(X30) ) )
& ( ( ~ ! [X47] :
( ~ r1(X30,X47)
| ~ ( ~ p8(X47)
& ~ p108(X47)
& p107(X47) ) )
& ~ ! [X48] :
( ~ r1(X30,X48)
| ~ ( p8(X48)
& ~ p108(X48)
& p107(X48) ) ) )
| ~ ( ~ p107(X30)
& p106(X30) ) )
& ( ( ~ ! [X49] :
( ~ r1(X30,X49)
| ~ ( ~ p7(X49)
& ~ p107(X49)
& p106(X49) ) )
& ~ ! [X50] :
( ~ r1(X30,X50)
| ~ ( p7(X50)
& ~ p107(X50)
& p106(X50) ) ) )
| ~ ( ~ p106(X30)
& p105(X30) ) )
& ( ( ~ ! [X51] :
( ~ r1(X30,X51)
| ~ ( ~ p6(X51)
& ~ p106(X51)
& p105(X51) ) )
& ~ ! [X52] :
( ~ r1(X30,X52)
| ~ ( p6(X52)
& ~ p106(X52)
& p105(X52) ) ) )
| ~ ( ~ p105(X30)
& p104(X30) ) )
& ( ( ~ ! [X53] :
( ~ r1(X30,X53)
| ~ ( ~ p5(X53)
& ~ p105(X53)
& p104(X53) ) )
& ~ ! [X54] :
( ~ r1(X30,X54)
| ~ ( p5(X54)
& ~ p105(X54)
& p104(X54) ) ) )
| ~ ( ~ p104(X30)
& p103(X30) ) )
& ( ( ~ ! [X55] :
( ~ r1(X30,X55)
| ~ ( ~ p4(X55)
& ~ p104(X55)
& p103(X55) ) )
& ~ ! [X56] :
( ~ r1(X30,X56)
| ~ ( p4(X56)
& ~ p104(X56)
& p103(X56) ) ) )
| ~ ( ~ p103(X30)
& p102(X30) ) )
& ( ( ~ ! [X57] :
( ~ r1(X30,X57)
| ~ ( ~ p3(X57)
& ~ p103(X57)
& p102(X57) ) )
& ~ ! [X58] :
( ~ r1(X30,X58)
| ~ ( p3(X58)
& ~ p103(X58)
& p102(X58) ) ) )
| ~ ( ~ p102(X30)
& p101(X30) ) )
& ( ( ~ ! [X59] :
( ~ r1(X30,X59)
| ~ ( ~ p2(X59)
& ~ p102(X59)
& p101(X59) ) )
& ~ ! [X60] :
( ~ r1(X30,X60)
| ~ ( p2(X60)
& ~ p102(X60)
& p101(X60) ) ) )
| ~ ( ~ p101(X30)
& p100(X30) ) )
& ( ( ( ! [X61] :
( ~ r1(X30,X61)
| ~ p16(X61)
| ~ p115(X61) )
| p16(X30) )
& ( ! [X62] :
( ~ r1(X30,X62)
| p16(X62)
| ~ p115(X62) )
| ~ p16(X30) ) )
| ~ p115(X30) )
& ( ( ( ! [X63] :
( ~ r1(X30,X63)
| ~ p15(X63)
| ~ p114(X63) )
| p15(X30) )
& ( ! [X64] :
( ~ r1(X30,X64)
| p15(X64)
| ~ p114(X64) )
| ~ p15(X30) ) )
| ~ p114(X30) )
& ( ( ( ! [X65] :
( ~ r1(X30,X65)
| ~ p14(X65)
| ~ p113(X65) )
| p14(X30) )
& ( ! [X66] :
( ~ r1(X30,X66)
| p14(X66)
| ~ p113(X66) )
| ~ p14(X30) ) )
| ~ p113(X30) )
& ( ( ( ! [X67] :
( ~ r1(X30,X67)
| ~ p13(X67)
| ~ p112(X67) )
| p13(X30) )
& ( ! [X68] :
( ~ r1(X30,X68)
| p13(X68)
| ~ p112(X68) )
| ~ p13(X30) ) )
| ~ p112(X30) )
& ( ( ( ! [X69] :
( ~ r1(X30,X69)
| ~ p12(X69)
| ~ p111(X69) )
| p12(X30) )
& ( ! [X70] :
( ~ r1(X30,X70)
| p12(X70)
| ~ p111(X70) )
| ~ p12(X30) ) )
| ~ p111(X30) )
& ( ( ( ! [X71] :
( ~ r1(X30,X71)
| ~ p11(X71)
| ~ p110(X71) )
| p11(X30) )
& ( ! [X72] :
( ~ r1(X30,X72)
| p11(X72)
| ~ p110(X72) )
| ~ p11(X30) ) )
| ~ p110(X30) )
& ( ( ( ! [X73] :
( ~ r1(X30,X73)
| ~ p10(X73)
| ~ p109(X73) )
| p10(X30) )
& ( ! [X74] :
( ~ r1(X30,X74)
| p10(X74)
| ~ p109(X74) )
| ~ p10(X30) ) )
| ~ p109(X30) )
& ( ( ( ! [X75] :
( ~ r1(X30,X75)
| ~ p9(X75)
| ~ p108(X75) )
| p9(X30) )
& ( ! [X76] :
( ~ r1(X30,X76)
| p9(X76)
| ~ p108(X76) )
| ~ p9(X30) ) )
| ~ p108(X30) )
& ( ( ( ! [X77] :
( ~ r1(X30,X77)
| ~ p8(X77)
| ~ p107(X77) )
| p8(X30) )
& ( ! [X78] :
( ~ r1(X30,X78)
| p8(X78)
| ~ p107(X78) )
| ~ p8(X30) ) )
| ~ p107(X30) )
& ( ( ( ! [X79] :
( ~ r1(X30,X79)
| ~ p7(X79)
| ~ p106(X79) )
| p7(X30) )
& ( ! [X80] :
( ~ r1(X30,X80)
| p7(X80)
| ~ p106(X80) )
| ~ p7(X30) ) )
| ~ p106(X30) )
& ( ( ( ! [X81] :
( ~ r1(X30,X81)
| ~ p6(X81)
| ~ p105(X81) )
| p6(X30) )
& ( ! [X82] :
( ~ r1(X30,X82)
| p6(X82)
| ~ p105(X82) )
| ~ p6(X30) ) )
| ~ p105(X30) )
& ( ( ( ! [X83] :
( ~ r1(X30,X83)
| ~ p5(X83)
| ~ p104(X83) )
| p5(X30) )
& ( ! [X84] :
( ~ r1(X30,X84)
| p5(X84)
| ~ p104(X84) )
| ~ p5(X30) ) )
| ~ p104(X30) )
& ( ( ( ! [X85] :
( ~ r1(X30,X85)
| ~ p4(X85)
| ~ p103(X85) )
| p4(X30) )
& ( ! [X86] :
( ~ r1(X30,X86)
| p4(X86)
| ~ p103(X86) )
| ~ p4(X30) ) )
| ~ p103(X30) )
& ( ( ( ! [X87] :
( ~ r1(X30,X87)
| ~ p3(X87)
| ~ p102(X87) )
| p3(X30) )
& ( ! [X88] :
( ~ r1(X30,X88)
| p3(X88)
| ~ p102(X88) )
| ~ p3(X30) ) )
| ~ p102(X30) )
& ( ( ( ! [X89] :
( ~ r1(X30,X89)
| ~ p2(X89)
| ~ p101(X89) )
| p2(X30) )
& ( ! [X90] :
( ~ r1(X30,X90)
| p2(X90)
| ~ p101(X90) )
| ~ p2(X30) ) )
| ~ p101(X30) )
& ( ( ( ! [X91] :
( ~ r1(X30,X91)
| ~ p1(X91)
| ~ p100(X91) )
| p1(X30) )
& ( ! [X92] :
( ~ r1(X30,X92)
| p1(X92)
| ~ p100(X92) )
| ~ p1(X30) ) )
| ~ p100(X30) )
& ( p114(X30)
| ~ p115(X30) )
& ( p113(X30)
| ~ p114(X30) )
& ( p112(X30)
| ~ p113(X30) )
& ( p111(X30)
| ~ p112(X30) )
& ( p110(X30)
| ~ p111(X30) )
& ( p109(X30)
| ~ p110(X30) )
& ( p108(X30)
| ~ p109(X30) )
& ( p107(X30)
| ~ p108(X30) )
& ( p106(X30)
| ~ p107(X30) )
& ( p105(X30)
| ~ p106(X30) )
& ( p104(X30)
| ~ p105(X30) )
& ( p103(X30)
| ~ p104(X30) )
& ( p102(X30)
| ~ p103(X30) )
& ( p101(X30)
| ~ p102(X30) )
& ( p100(X30)
| ~ p101(X30) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ~ p101(X0)
& p100(X0) ) ),
inference(pure_predicate_removal,[],[f5]) ).
fof(f7,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| p7(X15) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X16] :
( ~ r1(X0,X16)
| ! [X17] :
( ~ r1(X16,X17)
| ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ( ( ( ? [X31] :
( r1(X30,X31)
& ~ p16(X31)
& p115(X31) )
& ? [X32] :
( r1(X30,X32)
& p16(X32)
& p115(X32) ) )
| p115(X30)
| ~ p114(X30) )
& ( ( ? [X33] :
( r1(X30,X33)
& ~ p15(X33)
& ~ p115(X33)
& p114(X33) )
& ? [X34] :
( r1(X30,X34)
& p15(X34)
& ~ p115(X34)
& p114(X34) ) )
| p114(X30)
| ~ p113(X30) )
& ( ( ? [X35] :
( r1(X30,X35)
& ~ p14(X35)
& ~ p114(X35)
& p113(X35) )
& ? [X36] :
( r1(X30,X36)
& p14(X36)
& ~ p114(X36)
& p113(X36) ) )
| p113(X30)
| ~ p112(X30) )
& ( ( ? [X37] :
( r1(X30,X37)
& ~ p13(X37)
& ~ p113(X37)
& p112(X37) )
& ? [X38] :
( r1(X30,X38)
& p13(X38)
& ~ p113(X38)
& p112(X38) ) )
| p112(X30)
| ~ p111(X30) )
& ( ( ? [X39] :
( r1(X30,X39)
& ~ p12(X39)
& ~ p112(X39)
& p111(X39) )
& ? [X40] :
( r1(X30,X40)
& p12(X40)
& ~ p112(X40)
& p111(X40) ) )
| p111(X30)
| ~ p110(X30) )
& ( ( ? [X41] :
( r1(X30,X41)
& ~ p11(X41)
& ~ p111(X41)
& p110(X41) )
& ? [X42] :
( r1(X30,X42)
& p11(X42)
& ~ p111(X42)
& p110(X42) ) )
| p110(X30)
| ~ p109(X30) )
& ( ( ? [X43] :
( r1(X30,X43)
& ~ p10(X43)
& ~ p110(X43)
& p109(X43) )
& ? [X44] :
( r1(X30,X44)
& p10(X44)
& ~ p110(X44)
& p109(X44) ) )
| p109(X30)
| ~ p108(X30) )
& ( ( ? [X45] :
( r1(X30,X45)
& ~ p9(X45)
& ~ p109(X45)
& p108(X45) )
& ? [X46] :
( r1(X30,X46)
& p9(X46)
& ~ p109(X46)
& p108(X46) ) )
| p108(X30)
| ~ p107(X30) )
& ( ( ? [X47] :
( r1(X30,X47)
& ~ p8(X47)
& ~ p108(X47)
& p107(X47) )
& ? [X48] :
( r1(X30,X48)
& p8(X48)
& ~ p108(X48)
& p107(X48) ) )
| p107(X30)
| ~ p106(X30) )
& ( ( ? [X49] :
( r1(X30,X49)
& ~ p7(X49)
& ~ p107(X49)
& p106(X49) )
& ? [X50] :
( r1(X30,X50)
& p7(X50)
& ~ p107(X50)
& p106(X50) ) )
| p106(X30)
| ~ p105(X30) )
& ( ( ? [X51] :
( r1(X30,X51)
& ~ p6(X51)
& ~ p106(X51)
& p105(X51) )
& ? [X52] :
( r1(X30,X52)
& p6(X52)
& ~ p106(X52)
& p105(X52) ) )
| p105(X30)
| ~ p104(X30) )
& ( ( ? [X53] :
( r1(X30,X53)
& ~ p5(X53)
& ~ p105(X53)
& p104(X53) )
& ? [X54] :
( r1(X30,X54)
& p5(X54)
& ~ p105(X54)
& p104(X54) ) )
| p104(X30)
| ~ p103(X30) )
& ( ( ? [X55] :
( r1(X30,X55)
& ~ p4(X55)
& ~ p104(X55)
& p103(X55) )
& ? [X56] :
( r1(X30,X56)
& p4(X56)
& ~ p104(X56)
& p103(X56) ) )
| p103(X30)
| ~ p102(X30) )
& ( ( ? [X57] :
( r1(X30,X57)
& ~ p3(X57)
& ~ p103(X57)
& p102(X57) )
& ? [X58] :
( r1(X30,X58)
& p3(X58)
& ~ p103(X58)
& p102(X58) ) )
| p102(X30)
| ~ p101(X30) )
& ( ( ? [X59] :
( r1(X30,X59)
& ~ p2(X59)
& ~ p102(X59)
& p101(X59) )
& ? [X60] :
( r1(X30,X60)
& p2(X60)
& ~ p102(X60)
& p101(X60) ) )
| p101(X30)
| ~ p100(X30) )
& ( ( ( ! [X61] :
( ~ r1(X30,X61)
| ~ p16(X61)
| ~ p115(X61) )
| p16(X30) )
& ( ! [X62] :
( ~ r1(X30,X62)
| p16(X62)
| ~ p115(X62) )
| ~ p16(X30) ) )
| ~ p115(X30) )
& ( ( ( ! [X63] :
( ~ r1(X30,X63)
| ~ p15(X63)
| ~ p114(X63) )
| p15(X30) )
& ( ! [X64] :
( ~ r1(X30,X64)
| p15(X64)
| ~ p114(X64) )
| ~ p15(X30) ) )
| ~ p114(X30) )
& ( ( ( ! [X65] :
( ~ r1(X30,X65)
| ~ p14(X65)
| ~ p113(X65) )
| p14(X30) )
& ( ! [X66] :
( ~ r1(X30,X66)
| p14(X66)
| ~ p113(X66) )
| ~ p14(X30) ) )
| ~ p113(X30) )
& ( ( ( ! [X67] :
( ~ r1(X30,X67)
| ~ p13(X67)
| ~ p112(X67) )
| p13(X30) )
& ( ! [X68] :
( ~ r1(X30,X68)
| p13(X68)
| ~ p112(X68) )
| ~ p13(X30) ) )
| ~ p112(X30) )
& ( ( ( ! [X69] :
( ~ r1(X30,X69)
| ~ p12(X69)
| ~ p111(X69) )
| p12(X30) )
& ( ! [X70] :
( ~ r1(X30,X70)
| p12(X70)
| ~ p111(X70) )
| ~ p12(X30) ) )
| ~ p111(X30) )
& ( ( ( ! [X71] :
( ~ r1(X30,X71)
| ~ p11(X71)
| ~ p110(X71) )
| p11(X30) )
& ( ! [X72] :
( ~ r1(X30,X72)
| p11(X72)
| ~ p110(X72) )
| ~ p11(X30) ) )
| ~ p110(X30) )
& ( ( ( ! [X73] :
( ~ r1(X30,X73)
| ~ p10(X73)
| ~ p109(X73) )
| p10(X30) )
& ( ! [X74] :
( ~ r1(X30,X74)
| p10(X74)
| ~ p109(X74) )
| ~ p10(X30) ) )
| ~ p109(X30) )
& ( ( ( ! [X75] :
( ~ r1(X30,X75)
| ~ p9(X75)
| ~ p108(X75) )
| p9(X30) )
& ( ! [X76] :
( ~ r1(X30,X76)
| p9(X76)
| ~ p108(X76) )
| ~ p9(X30) ) )
| ~ p108(X30) )
& ( ( ( ! [X77] :
( ~ r1(X30,X77)
| ~ p8(X77)
| ~ p107(X77) )
| p8(X30) )
& ( ! [X78] :
( ~ r1(X30,X78)
| p8(X78)
| ~ p107(X78) )
| ~ p8(X30) ) )
| ~ p107(X30) )
& ( ( ( ! [X79] :
( ~ r1(X30,X79)
| ~ p7(X79)
| ~ p106(X79) )
| p7(X30) )
& ( ! [X80] :
( ~ r1(X30,X80)
| p7(X80)
| ~ p106(X80) )
| ~ p7(X30) ) )
| ~ p106(X30) )
& ( ( ( ! [X81] :
( ~ r1(X30,X81)
| ~ p6(X81)
| ~ p105(X81) )
| p6(X30) )
& ( ! [X82] :
( ~ r1(X30,X82)
| p6(X82)
| ~ p105(X82) )
| ~ p6(X30) ) )
| ~ p105(X30) )
& ( ( ( ! [X83] :
( ~ r1(X30,X83)
| ~ p5(X83)
| ~ p104(X83) )
| p5(X30) )
& ( ! [X84] :
( ~ r1(X30,X84)
| p5(X84)
| ~ p104(X84) )
| ~ p5(X30) ) )
| ~ p104(X30) )
& ( ( ( ! [X85] :
( ~ r1(X30,X85)
| ~ p4(X85)
| ~ p103(X85) )
| p4(X30) )
& ( ! [X86] :
( ~ r1(X30,X86)
| p4(X86)
| ~ p103(X86) )
| ~ p4(X30) ) )
| ~ p103(X30) )
& ( ( ( ! [X87] :
( ~ r1(X30,X87)
| ~ p3(X87)
| ~ p102(X87) )
| p3(X30) )
& ( ! [X88] :
( ~ r1(X30,X88)
| p3(X88)
| ~ p102(X88) )
| ~ p3(X30) ) )
| ~ p102(X30) )
& ( ( ( ! [X89] :
( ~ r1(X30,X89)
| ~ p2(X89)
| ~ p101(X89) )
| p2(X30) )
& ( ! [X90] :
( ~ r1(X30,X90)
| p2(X90)
| ~ p101(X90) )
| ~ p2(X30) ) )
| ~ p101(X30) )
& ( ( ( ! [X91] :
( ~ r1(X30,X91)
| ~ p1(X91)
| ~ p100(X91) )
| p1(X30) )
& ( ! [X92] :
( ~ r1(X30,X92)
| p1(X92)
| ~ p100(X92) )
| ~ p1(X30) ) )
| ~ p100(X30) )
& ( p114(X30)
| ~ p115(X30) )
& ( p113(X30)
| ~ p114(X30) )
& ( p112(X30)
| ~ p113(X30) )
& ( p111(X30)
| ~ p112(X30) )
& ( p110(X30)
| ~ p111(X30) )
& ( p109(X30)
| ~ p110(X30) )
& ( p108(X30)
| ~ p109(X30) )
& ( p107(X30)
| ~ p108(X30) )
& ( p106(X30)
| ~ p107(X30) )
& ( p105(X30)
| ~ p106(X30) )
& ( p104(X30)
| ~ p105(X30) )
& ( p103(X30)
| ~ p104(X30) )
& ( p102(X30)
| ~ p103(X30) )
& ( p101(X30)
| ~ p102(X30) )
& ( p100(X30)
| ~ p101(X30) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ~ p101(X0)
& p100(X0) ),
inference(ennf_transformation,[],[f6]) ).
fof(f8,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| p7(X15) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X16] :
( ~ r1(X0,X16)
| ! [X17] :
( ~ r1(X16,X17)
| ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ( ( ( ? [X31] :
( r1(X30,X31)
& ~ p16(X31)
& p115(X31) )
& ? [X32] :
( r1(X30,X32)
& p16(X32)
& p115(X32) ) )
| p115(X30)
| ~ p114(X30) )
& ( ( ? [X33] :
( r1(X30,X33)
& ~ p15(X33)
& ~ p115(X33)
& p114(X33) )
& ? [X34] :
( r1(X30,X34)
& p15(X34)
& ~ p115(X34)
& p114(X34) ) )
| p114(X30)
| ~ p113(X30) )
& ( ( ? [X35] :
( r1(X30,X35)
& ~ p14(X35)
& ~ p114(X35)
& p113(X35) )
& ? [X36] :
( r1(X30,X36)
& p14(X36)
& ~ p114(X36)
& p113(X36) ) )
| p113(X30)
| ~ p112(X30) )
& ( ( ? [X37] :
( r1(X30,X37)
& ~ p13(X37)
& ~ p113(X37)
& p112(X37) )
& ? [X38] :
( r1(X30,X38)
& p13(X38)
& ~ p113(X38)
& p112(X38) ) )
| p112(X30)
| ~ p111(X30) )
& ( ( ? [X39] :
( r1(X30,X39)
& ~ p12(X39)
& ~ p112(X39)
& p111(X39) )
& ? [X40] :
( r1(X30,X40)
& p12(X40)
& ~ p112(X40)
& p111(X40) ) )
| p111(X30)
| ~ p110(X30) )
& ( ( ? [X41] :
( r1(X30,X41)
& ~ p11(X41)
& ~ p111(X41)
& p110(X41) )
& ? [X42] :
( r1(X30,X42)
& p11(X42)
& ~ p111(X42)
& p110(X42) ) )
| p110(X30)
| ~ p109(X30) )
& ( ( ? [X43] :
( r1(X30,X43)
& ~ p10(X43)
& ~ p110(X43)
& p109(X43) )
& ? [X44] :
( r1(X30,X44)
& p10(X44)
& ~ p110(X44)
& p109(X44) ) )
| p109(X30)
| ~ p108(X30) )
& ( ( ? [X45] :
( r1(X30,X45)
& ~ p9(X45)
& ~ p109(X45)
& p108(X45) )
& ? [X46] :
( r1(X30,X46)
& p9(X46)
& ~ p109(X46)
& p108(X46) ) )
| p108(X30)
| ~ p107(X30) )
& ( ( ? [X47] :
( r1(X30,X47)
& ~ p8(X47)
& ~ p108(X47)
& p107(X47) )
& ? [X48] :
( r1(X30,X48)
& p8(X48)
& ~ p108(X48)
& p107(X48) ) )
| p107(X30)
| ~ p106(X30) )
& ( ( ? [X49] :
( r1(X30,X49)
& ~ p7(X49)
& ~ p107(X49)
& p106(X49) )
& ? [X50] :
( r1(X30,X50)
& p7(X50)
& ~ p107(X50)
& p106(X50) ) )
| p106(X30)
| ~ p105(X30) )
& ( ( ? [X51] :
( r1(X30,X51)
& ~ p6(X51)
& ~ p106(X51)
& p105(X51) )
& ? [X52] :
( r1(X30,X52)
& p6(X52)
& ~ p106(X52)
& p105(X52) ) )
| p105(X30)
| ~ p104(X30) )
& ( ( ? [X53] :
( r1(X30,X53)
& ~ p5(X53)
& ~ p105(X53)
& p104(X53) )
& ? [X54] :
( r1(X30,X54)
& p5(X54)
& ~ p105(X54)
& p104(X54) ) )
| p104(X30)
| ~ p103(X30) )
& ( ( ? [X55] :
( r1(X30,X55)
& ~ p4(X55)
& ~ p104(X55)
& p103(X55) )
& ? [X56] :
( r1(X30,X56)
& p4(X56)
& ~ p104(X56)
& p103(X56) ) )
| p103(X30)
| ~ p102(X30) )
& ( ( ? [X57] :
( r1(X30,X57)
& ~ p3(X57)
& ~ p103(X57)
& p102(X57) )
& ? [X58] :
( r1(X30,X58)
& p3(X58)
& ~ p103(X58)
& p102(X58) ) )
| p102(X30)
| ~ p101(X30) )
& ( ( ? [X59] :
( r1(X30,X59)
& ~ p2(X59)
& ~ p102(X59)
& p101(X59) )
& ? [X60] :
( r1(X30,X60)
& p2(X60)
& ~ p102(X60)
& p101(X60) ) )
| p101(X30)
| ~ p100(X30) )
& ( ( ( ! [X61] :
( ~ r1(X30,X61)
| ~ p16(X61)
| ~ p115(X61) )
| p16(X30) )
& ( ! [X62] :
( ~ r1(X30,X62)
| p16(X62)
| ~ p115(X62) )
| ~ p16(X30) ) )
| ~ p115(X30) )
& ( ( ( ! [X63] :
( ~ r1(X30,X63)
| ~ p15(X63)
| ~ p114(X63) )
| p15(X30) )
& ( ! [X64] :
( ~ r1(X30,X64)
| p15(X64)
| ~ p114(X64) )
| ~ p15(X30) ) )
| ~ p114(X30) )
& ( ( ( ! [X65] :
( ~ r1(X30,X65)
| ~ p14(X65)
| ~ p113(X65) )
| p14(X30) )
& ( ! [X66] :
( ~ r1(X30,X66)
| p14(X66)
| ~ p113(X66) )
| ~ p14(X30) ) )
| ~ p113(X30) )
& ( ( ( ! [X67] :
( ~ r1(X30,X67)
| ~ p13(X67)
| ~ p112(X67) )
| p13(X30) )
& ( ! [X68] :
( ~ r1(X30,X68)
| p13(X68)
| ~ p112(X68) )
| ~ p13(X30) ) )
| ~ p112(X30) )
& ( ( ( ! [X69] :
( ~ r1(X30,X69)
| ~ p12(X69)
| ~ p111(X69) )
| p12(X30) )
& ( ! [X70] :
( ~ r1(X30,X70)
| p12(X70)
| ~ p111(X70) )
| ~ p12(X30) ) )
| ~ p111(X30) )
& ( ( ( ! [X71] :
( ~ r1(X30,X71)
| ~ p11(X71)
| ~ p110(X71) )
| p11(X30) )
& ( ! [X72] :
( ~ r1(X30,X72)
| p11(X72)
| ~ p110(X72) )
| ~ p11(X30) ) )
| ~ p110(X30) )
& ( ( ( ! [X73] :
( ~ r1(X30,X73)
| ~ p10(X73)
| ~ p109(X73) )
| p10(X30) )
& ( ! [X74] :
( ~ r1(X30,X74)
| p10(X74)
| ~ p109(X74) )
| ~ p10(X30) ) )
| ~ p109(X30) )
& ( ( ( ! [X75] :
( ~ r1(X30,X75)
| ~ p9(X75)
| ~ p108(X75) )
| p9(X30) )
& ( ! [X76] :
( ~ r1(X30,X76)
| p9(X76)
| ~ p108(X76) )
| ~ p9(X30) ) )
| ~ p108(X30) )
& ( ( ( ! [X77] :
( ~ r1(X30,X77)
| ~ p8(X77)
| ~ p107(X77) )
| p8(X30) )
& ( ! [X78] :
( ~ r1(X30,X78)
| p8(X78)
| ~ p107(X78) )
| ~ p8(X30) ) )
| ~ p107(X30) )
& ( ( ( ! [X79] :
( ~ r1(X30,X79)
| ~ p7(X79)
| ~ p106(X79) )
| p7(X30) )
& ( ! [X80] :
( ~ r1(X30,X80)
| p7(X80)
| ~ p106(X80) )
| ~ p7(X30) ) )
| ~ p106(X30) )
& ( ( ( ! [X81] :
( ~ r1(X30,X81)
| ~ p6(X81)
| ~ p105(X81) )
| p6(X30) )
& ( ! [X82] :
( ~ r1(X30,X82)
| p6(X82)
| ~ p105(X82) )
| ~ p6(X30) ) )
| ~ p105(X30) )
& ( ( ( ! [X83] :
( ~ r1(X30,X83)
| ~ p5(X83)
| ~ p104(X83) )
| p5(X30) )
& ( ! [X84] :
( ~ r1(X30,X84)
| p5(X84)
| ~ p104(X84) )
| ~ p5(X30) ) )
| ~ p104(X30) )
& ( ( ( ! [X85] :
( ~ r1(X30,X85)
| ~ p4(X85)
| ~ p103(X85) )
| p4(X30) )
& ( ! [X86] :
( ~ r1(X30,X86)
| p4(X86)
| ~ p103(X86) )
| ~ p4(X30) ) )
| ~ p103(X30) )
& ( ( ( ! [X87] :
( ~ r1(X30,X87)
| ~ p3(X87)
| ~ p102(X87) )
| p3(X30) )
& ( ! [X88] :
( ~ r1(X30,X88)
| p3(X88)
| ~ p102(X88) )
| ~ p3(X30) ) )
| ~ p102(X30) )
& ( ( ( ! [X89] :
( ~ r1(X30,X89)
| ~ p2(X89)
| ~ p101(X89) )
| p2(X30) )
& ( ! [X90] :
( ~ r1(X30,X90)
| p2(X90)
| ~ p101(X90) )
| ~ p2(X30) ) )
| ~ p101(X30) )
& ( ( ( ! [X91] :
( ~ r1(X30,X91)
| ~ p1(X91)
| ~ p100(X91) )
| p1(X30) )
& ( ! [X92] :
( ~ r1(X30,X92)
| p1(X92)
| ~ p100(X92) )
| ~ p1(X30) ) )
| ~ p100(X30) )
& ( p114(X30)
| ~ p115(X30) )
& ( p113(X30)
| ~ p114(X30) )
& ( p112(X30)
| ~ p113(X30) )
& ( p111(X30)
| ~ p112(X30) )
& ( p110(X30)
| ~ p111(X30) )
& ( p109(X30)
| ~ p110(X30) )
& ( p108(X30)
| ~ p109(X30) )
& ( p107(X30)
| ~ p108(X30) )
& ( p106(X30)
| ~ p107(X30) )
& ( p105(X30)
| ~ p106(X30) )
& ( p104(X30)
| ~ p105(X30) )
& ( p103(X30)
| ~ p104(X30) )
& ( p102(X30)
| ~ p103(X30) )
& ( p101(X30)
| ~ p102(X30) )
& ( p100(X30)
| ~ p101(X30) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ~ p101(X0)
& p100(X0) ),
inference(flattening,[],[f7]) ).
fof(f9,definition,
! [X30] :
( ( ? [X59] :
( r1(X30,X59)
& ~ p2(X59)
& ~ p102(X59)
& p101(X59) )
& ? [X60] :
( r1(X30,X60)
& p2(X60)
& ~ p102(X60)
& p101(X60) ) )
| p101(X30)
| ~ p100(X30)
| ~ sP0(X30) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f10,definition,
! [X30] :
( ( ? [X57] :
( r1(X30,X57)
& ~ p3(X57)
& ~ p103(X57)
& p102(X57) )
& ? [X58] :
( r1(X30,X58)
& p3(X58)
& ~ p103(X58)
& p102(X58) ) )
| p102(X30)
| ~ p101(X30)
| ~ sP1(X30) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f11,definition,
! [X30] :
( ( ? [X55] :
( r1(X30,X55)
& ~ p4(X55)
& ~ p104(X55)
& p103(X55) )
& ? [X56] :
( r1(X30,X56)
& p4(X56)
& ~ p104(X56)
& p103(X56) ) )
| p103(X30)
| ~ p102(X30)
| ~ sP2(X30) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f12,definition,
! [X30] :
( ( ? [X53] :
( r1(X30,X53)
& ~ p5(X53)
& ~ p105(X53)
& p104(X53) )
& ? [X54] :
( r1(X30,X54)
& p5(X54)
& ~ p105(X54)
& p104(X54) ) )
| p104(X30)
| ~ p103(X30)
| ~ sP3(X30) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f13,definition,
! [X30] :
( ( ? [X51] :
( r1(X30,X51)
& ~ p6(X51)
& ~ p106(X51)
& p105(X51) )
& ? [X52] :
( r1(X30,X52)
& p6(X52)
& ~ p106(X52)
& p105(X52) ) )
| p105(X30)
| ~ p104(X30)
| ~ sP4(X30) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f14,definition,
! [X30] :
( ( ? [X49] :
( r1(X30,X49)
& ~ p7(X49)
& ~ p107(X49)
& p106(X49) )
& ? [X50] :
( r1(X30,X50)
& p7(X50)
& ~ p107(X50)
& p106(X50) ) )
| p106(X30)
| ~ p105(X30)
| ~ sP5(X30) ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f15,definition,
! [X30] :
( ( ? [X47] :
( r1(X30,X47)
& ~ p8(X47)
& ~ p108(X47)
& p107(X47) )
& ? [X48] :
( r1(X30,X48)
& p8(X48)
& ~ p108(X48)
& p107(X48) ) )
| p107(X30)
| ~ p106(X30)
| ~ sP6(X30) ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f16,definition,
! [X30] :
( ( ? [X45] :
( r1(X30,X45)
& ~ p9(X45)
& ~ p109(X45)
& p108(X45) )
& ? [X46] :
( r1(X30,X46)
& p9(X46)
& ~ p109(X46)
& p108(X46) ) )
| p108(X30)
| ~ p107(X30)
| ~ sP7(X30) ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f17,definition,
! [X30] :
( ( ? [X43] :
( r1(X30,X43)
& ~ p10(X43)
& ~ p110(X43)
& p109(X43) )
& ? [X44] :
( r1(X30,X44)
& p10(X44)
& ~ p110(X44)
& p109(X44) ) )
| p109(X30)
| ~ p108(X30)
| ~ sP8(X30) ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f18,definition,
! [X30] :
( ( ? [X41] :
( r1(X30,X41)
& ~ p11(X41)
& ~ p111(X41)
& p110(X41) )
& ? [X42] :
( r1(X30,X42)
& p11(X42)
& ~ p111(X42)
& p110(X42) ) )
| p110(X30)
| ~ p109(X30)
| ~ sP9(X30) ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f19,definition,
! [X30] :
( ( ? [X39] :
( r1(X30,X39)
& ~ p12(X39)
& ~ p112(X39)
& p111(X39) )
& ? [X40] :
( r1(X30,X40)
& p12(X40)
& ~ p112(X40)
& p111(X40) ) )
| p111(X30)
| ~ p110(X30)
| ~ sP10(X30) ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f20,definition,
! [X30] :
( ( ? [X37] :
( r1(X30,X37)
& ~ p13(X37)
& ~ p113(X37)
& p112(X37) )
& ? [X38] :
( r1(X30,X38)
& p13(X38)
& ~ p113(X38)
& p112(X38) ) )
| p112(X30)
| ~ p111(X30)
| ~ sP11(X30) ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f21,definition,
! [X30] :
( ( ? [X35] :
( r1(X30,X35)
& ~ p14(X35)
& ~ p114(X35)
& p113(X35) )
& ? [X36] :
( r1(X30,X36)
& p14(X36)
& ~ p114(X36)
& p113(X36) ) )
| p113(X30)
| ~ p112(X30)
| ~ sP12(X30) ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f22,definition,
! [X30] :
( ( ? [X33] :
( r1(X30,X33)
& ~ p15(X33)
& ~ p115(X33)
& p114(X33) )
& ? [X34] :
( r1(X30,X34)
& p15(X34)
& ~ p115(X34)
& p114(X34) ) )
| p114(X30)
| ~ p113(X30)
| ~ sP13(X30) ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f23,definition,
! [X30] :
( ( ? [X31] :
( r1(X30,X31)
& ~ p16(X31)
& p115(X31) )
& ? [X32] :
( r1(X30,X32)
& p16(X32)
& p115(X32) ) )
| p115(X30)
| ~ p114(X30)
| ~ sP14(X30) ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f24,definition,
! [X30] :
( ( ( ! [X91] :
( ~ r1(X30,X91)
| ~ p1(X91)
| ~ p100(X91) )
| p1(X30) )
& ( ! [X92] :
( ~ r1(X30,X92)
| p1(X92)
| ~ p100(X92) )
| ~ p1(X30) ) )
| ~ p100(X30)
| ~ sP15(X30) ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f25,definition,
! [X30] :
( ( ( ! [X89] :
( ~ r1(X30,X89)
| ~ p2(X89)
| ~ p101(X89) )
| p2(X30) )
& ( ! [X90] :
( ~ r1(X30,X90)
| p2(X90)
| ~ p101(X90) )
| ~ p2(X30) ) )
| ~ p101(X30)
| ~ sP16(X30) ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f26,definition,
! [X30] :
( ( ( ! [X87] :
( ~ r1(X30,X87)
| ~ p3(X87)
| ~ p102(X87) )
| p3(X30) )
& ( ! [X88] :
( ~ r1(X30,X88)
| p3(X88)
| ~ p102(X88) )
| ~ p3(X30) ) )
| ~ p102(X30)
| ~ sP17(X30) ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f27,definition,
! [X30] :
( ( ( ! [X85] :
( ~ r1(X30,X85)
| ~ p4(X85)
| ~ p103(X85) )
| p4(X30) )
& ( ! [X86] :
( ~ r1(X30,X86)
| p4(X86)
| ~ p103(X86) )
| ~ p4(X30) ) )
| ~ p103(X30)
| ~ sP18(X30) ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f28,definition,
! [X30] :
( ( ( ! [X83] :
( ~ r1(X30,X83)
| ~ p5(X83)
| ~ p104(X83) )
| p5(X30) )
& ( ! [X84] :
( ~ r1(X30,X84)
| p5(X84)
| ~ p104(X84) )
| ~ p5(X30) ) )
| ~ p104(X30)
| ~ sP19(X30) ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f29,definition,
! [X30] :
( ( ( ! [X81] :
( ~ r1(X30,X81)
| ~ p6(X81)
| ~ p105(X81) )
| p6(X30) )
& ( ! [X82] :
( ~ r1(X30,X82)
| p6(X82)
| ~ p105(X82) )
| ~ p6(X30) ) )
| ~ p105(X30)
| ~ sP20(X30) ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f30,definition,
! [X30] :
( ( ( ! [X79] :
( ~ r1(X30,X79)
| ~ p7(X79)
| ~ p106(X79) )
| p7(X30) )
& ( ! [X80] :
( ~ r1(X30,X80)
| p7(X80)
| ~ p106(X80) )
| ~ p7(X30) ) )
| ~ p106(X30)
| ~ sP21(X30) ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f31,definition,
! [X30] :
( ( ( ! [X77] :
( ~ r1(X30,X77)
| ~ p8(X77)
| ~ p107(X77) )
| p8(X30) )
& ( ! [X78] :
( ~ r1(X30,X78)
| p8(X78)
| ~ p107(X78) )
| ~ p8(X30) ) )
| ~ p107(X30)
| ~ sP22(X30) ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f32,definition,
! [X30] :
( ( ( ! [X75] :
( ~ r1(X30,X75)
| ~ p9(X75)
| ~ p108(X75) )
| p9(X30) )
& ( ! [X76] :
( ~ r1(X30,X76)
| p9(X76)
| ~ p108(X76) )
| ~ p9(X30) ) )
| ~ p108(X30)
| ~ sP23(X30) ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f33,definition,
! [X30] :
( ( ( ! [X73] :
( ~ r1(X30,X73)
| ~ p10(X73)
| ~ p109(X73) )
| p10(X30) )
& ( ! [X74] :
( ~ r1(X30,X74)
| p10(X74)
| ~ p109(X74) )
| ~ p10(X30) ) )
| ~ p109(X30)
| ~ sP24(X30) ),
introduced(definition,[new_symbols(definition,[sP24])],[predicate_definition_introduction]) ).
fof(f34,definition,
! [X30] :
( ( ( ! [X71] :
( ~ r1(X30,X71)
| ~ p11(X71)
| ~ p110(X71) )
| p11(X30) )
& ( ! [X72] :
( ~ r1(X30,X72)
| p11(X72)
| ~ p110(X72) )
| ~ p11(X30) ) )
| ~ p110(X30)
| ~ sP25(X30) ),
introduced(definition,[new_symbols(definition,[sP25])],[predicate_definition_introduction]) ).
fof(f35,definition,
! [X30] :
( ( ( ! [X69] :
( ~ r1(X30,X69)
| ~ p12(X69)
| ~ p111(X69) )
| p12(X30) )
& ( ! [X70] :
( ~ r1(X30,X70)
| p12(X70)
| ~ p111(X70) )
| ~ p12(X30) ) )
| ~ p111(X30)
| ~ sP26(X30) ),
introduced(definition,[new_symbols(definition,[sP26])],[predicate_definition_introduction]) ).
fof(f36,definition,
! [X30] :
( ( ( ! [X67] :
( ~ r1(X30,X67)
| ~ p13(X67)
| ~ p112(X67) )
| p13(X30) )
& ( ! [X68] :
( ~ r1(X30,X68)
| p13(X68)
| ~ p112(X68) )
| ~ p13(X30) ) )
| ~ p112(X30)
| ~ sP27(X30) ),
introduced(definition,[new_symbols(definition,[sP27])],[predicate_definition_introduction]) ).
fof(f37,definition,
! [X30] :
( ( ( ! [X65] :
( ~ r1(X30,X65)
| ~ p14(X65)
| ~ p113(X65) )
| p14(X30) )
& ( ! [X66] :
( ~ r1(X30,X66)
| p14(X66)
| ~ p113(X66) )
| ~ p14(X30) ) )
| ~ p113(X30)
| ~ sP28(X30) ),
introduced(definition,[new_symbols(definition,[sP28])],[predicate_definition_introduction]) ).
fof(f38,definition,
! [X30] :
( ( ( ! [X63] :
( ~ r1(X30,X63)
| ~ p15(X63)
| ~ p114(X63) )
| p15(X30) )
& ( ! [X64] :
( ~ r1(X30,X64)
| p15(X64)
| ~ p114(X64) )
| ~ p15(X30) ) )
| ~ p114(X30)
| ~ sP29(X30) ),
introduced(definition,[new_symbols(definition,[sP29])],[predicate_definition_introduction]) ).
fof(f39,definition,
! [X30] :
( ( ( ! [X61] :
( ~ r1(X30,X61)
| ~ p16(X61)
| ~ p115(X61) )
| p16(X30) )
& ( ! [X62] :
( ~ r1(X30,X62)
| p16(X62)
| ~ p115(X62) )
| ~ p16(X30) ) )
| ~ p115(X30)
| ~ sP30(X30) ),
introduced(definition,[new_symbols(definition,[sP30])],[predicate_definition_introduction]) ).
fof(f40,definition,
! [X30] :
( ( sP14(X30)
& sP13(X30)
& sP12(X30)
& sP11(X30)
& sP10(X30)
& sP9(X30)
& sP8(X30)
& sP7(X30)
& sP6(X30)
& sP5(X30)
& sP4(X30)
& sP3(X30)
& sP2(X30)
& sP1(X30)
& sP0(X30)
& sP30(X30)
& sP29(X30)
& sP28(X30)
& sP27(X30)
& sP26(X30)
& sP25(X30)
& sP24(X30)
& sP23(X30)
& sP22(X30)
& sP21(X30)
& sP20(X30)
& sP19(X30)
& sP18(X30)
& sP17(X30)
& sP16(X30)
& sP15(X30)
& ( p114(X30)
| ~ p115(X30) )
& ( p113(X30)
| ~ p114(X30) )
& ( p112(X30)
| ~ p113(X30) )
& ( p111(X30)
| ~ p112(X30) )
& ( p110(X30)
| ~ p111(X30) )
& ( p109(X30)
| ~ p110(X30) )
& ( p108(X30)
| ~ p109(X30) )
& ( p107(X30)
| ~ p108(X30) )
& ( p106(X30)
| ~ p107(X30) )
& ( p105(X30)
| ~ p106(X30) )
& ( p104(X30)
| ~ p105(X30) )
& ( p103(X30)
| ~ p104(X30) )
& ( p102(X30)
| ~ p103(X30) )
& ( p101(X30)
| ~ p102(X30) )
& ( p100(X30)
| ~ p101(X30) ) )
| ~ sP31(X30) ),
introduced(definition,[new_symbols(definition,[sP31])],[predicate_definition_introduction]) ).
fof(f41,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| p7(X15) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X16] :
( ~ r1(X0,X16)
| ! [X17] :
( ~ r1(X16,X17)
| ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| sP31(X30) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ~ p101(X0)
& p100(X0) ),
inference(definition_folding,[],[f8,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,f10,f9]) ).
fof(f42,plain,
! [X30] :
( ( sP14(X30)
& sP13(X30)
& sP12(X30)
& sP11(X30)
& sP10(X30)
& sP9(X30)
& sP8(X30)
& sP7(X30)
& sP6(X30)
& sP5(X30)
& sP4(X30)
& sP3(X30)
& sP2(X30)
& sP1(X30)
& sP0(X30)
& sP30(X30)
& sP29(X30)
& sP28(X30)
& sP27(X30)
& sP26(X30)
& sP25(X30)
& sP24(X30)
& sP23(X30)
& sP22(X30)
& sP21(X30)
& sP20(X30)
& sP19(X30)
& sP18(X30)
& sP17(X30)
& sP16(X30)
& sP15(X30)
& ( p114(X30)
| ~ p115(X30) )
& ( p113(X30)
| ~ p114(X30) )
& ( p112(X30)
| ~ p113(X30) )
& ( p111(X30)
| ~ p112(X30) )
& ( p110(X30)
| ~ p111(X30) )
& ( p109(X30)
| ~ p110(X30) )
& ( p108(X30)
| ~ p109(X30) )
& ( p107(X30)
| ~ p108(X30) )
& ( p106(X30)
| ~ p107(X30) )
& ( p105(X30)
| ~ p106(X30) )
& ( p104(X30)
| ~ p105(X30) )
& ( p103(X30)
| ~ p104(X30) )
& ( p102(X30)
| ~ p103(X30) )
& ( p101(X30)
| ~ p102(X30) )
& ( p100(X30)
| ~ p101(X30) ) )
| ~ sP31(X30) ),
inference(nnf_transformation,[],[f40]) ).
fof(f43,plain,
! [X0] :
( ( sP14(X0)
& sP13(X0)
& sP12(X0)
& sP11(X0)
& sP10(X0)
& sP9(X0)
& sP8(X0)
& sP7(X0)
& sP6(X0)
& sP5(X0)
& sP4(X0)
& sP3(X0)
& sP2(X0)
& sP1(X0)
& sP0(X0)
& sP30(X0)
& sP29(X0)
& sP28(X0)
& sP27(X0)
& sP26(X0)
& sP25(X0)
& sP24(X0)
& sP23(X0)
& sP22(X0)
& sP21(X0)
& sP20(X0)
& sP19(X0)
& sP18(X0)
& sP17(X0)
& sP16(X0)
& sP15(X0)
& ( p114(X0)
| ~ p115(X0) )
& ( p113(X0)
| ~ p114(X0) )
& ( p112(X0)
| ~ p113(X0) )
& ( p111(X0)
| ~ p112(X0) )
& ( p110(X0)
| ~ p111(X0) )
& ( p109(X0)
| ~ p110(X0) )
& ( p108(X0)
| ~ p109(X0) )
& ( p107(X0)
| ~ p108(X0) )
& ( p106(X0)
| ~ p107(X0) )
& ( p105(X0)
| ~ p106(X0) )
& ( p104(X0)
| ~ p105(X0) )
& ( p103(X0)
| ~ p104(X0) )
& ( p102(X0)
| ~ p103(X0) )
& ( p101(X0)
| ~ p102(X0) )
& ( p100(X0)
| ~ p101(X0) ) )
| ~ sP31(X0) ),
inference(rectify,[],[f42]) ).
fof(f103,plain,
! [X30] :
( ( ? [X49] :
( r1(X30,X49)
& ~ p7(X49)
& ~ p107(X49)
& p106(X49) )
& ? [X50] :
( r1(X30,X50)
& p7(X50)
& ~ p107(X50)
& p106(X50) ) )
| p106(X30)
| ~ p105(X30)
| ~ sP5(X30) ),
inference(nnf_transformation,[],[f14]) ).
fof(f104,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,[],[f103]) ).
fof(f105,plain,
! [X0] :
( ( r1(X0,sK50(X0))
& ~ p7(sK50(X0))
& ~ p107(sK50(X0))
& p106(sK50(X0))
& r1(X0,sK51(X0))
& p7(sK51(X0))
& ~ p107(sK51(X0))
& p106(sK51(X0)) )
| p106(X0)
| ~ p105(X0)
| ~ sP5(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK50,sK51]),skolemize(X1,sK50(X0)),skolemize(X2,sK51(X0))],[f104]) ).
fof(f106,plain,
! [X30] :
( ( ? [X51] :
( r1(X30,X51)
& ~ p6(X51)
& ~ p106(X51)
& p105(X51) )
& ? [X52] :
( r1(X30,X52)
& p6(X52)
& ~ p106(X52)
& p105(X52) ) )
| p105(X30)
| ~ p104(X30)
| ~ sP4(X30) ),
inference(nnf_transformation,[],[f13]) ).
fof(f107,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,[],[f106]) ).
fof(f108,plain,
! [X0] :
( ( r1(X0,sK52(X0))
& ~ p6(sK52(X0))
& ~ p106(sK52(X0))
& p105(sK52(X0))
& r1(X0,sK53(X0))
& p6(sK53(X0))
& ~ p106(sK53(X0))
& p105(sK53(X0)) )
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK52,sK53]),skolemize(X1,sK52(X0)),skolemize(X2,sK53(X0))],[f107]) ).
fof(f109,plain,
! [X30] :
( ( ? [X53] :
( r1(X30,X53)
& ~ p5(X53)
& ~ p105(X53)
& p104(X53) )
& ? [X54] :
( r1(X30,X54)
& p5(X54)
& ~ p105(X54)
& p104(X54) ) )
| p104(X30)
| ~ p103(X30)
| ~ sP3(X30) ),
inference(nnf_transformation,[],[f12]) ).
fof(f110,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,[],[f109]) ).
fof(f111,plain,
! [X0] :
( ( r1(X0,sK54(X0))
& ~ p5(sK54(X0))
& ~ p105(sK54(X0))
& p104(sK54(X0))
& r1(X0,sK55(X0))
& p5(sK55(X0))
& ~ p105(sK55(X0))
& p104(sK55(X0)) )
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK54,sK55]),skolemize(X1,sK54(X0)),skolemize(X2,sK55(X0))],[f110]) ).
fof(f112,plain,
! [X30] :
( ( ? [X55] :
( r1(X30,X55)
& ~ p4(X55)
& ~ p104(X55)
& p103(X55) )
& ? [X56] :
( r1(X30,X56)
& p4(X56)
& ~ p104(X56)
& p103(X56) ) )
| p103(X30)
| ~ p102(X30)
| ~ sP2(X30) ),
inference(nnf_transformation,[],[f11]) ).
fof(f113,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,[],[f112]) ).
fof(f114,plain,
! [X0] :
( ( r1(X0,sK56(X0))
& ~ p4(sK56(X0))
& ~ p104(sK56(X0))
& p103(sK56(X0))
& r1(X0,sK57(X0))
& p4(sK57(X0))
& ~ p104(sK57(X0))
& p103(sK57(X0)) )
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK56,sK57]),skolemize(X1,sK56(X0)),skolemize(X2,sK57(X0))],[f113]) ).
fof(f115,plain,
! [X30] :
( ( ? [X57] :
( r1(X30,X57)
& ~ p3(X57)
& ~ p103(X57)
& p102(X57) )
& ? [X58] :
( r1(X30,X58)
& p3(X58)
& ~ p103(X58)
& p102(X58) ) )
| p102(X30)
| ~ p101(X30)
| ~ sP1(X30) ),
inference(nnf_transformation,[],[f10]) ).
fof(f116,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,[],[f115]) ).
fof(f117,plain,
! [X0] :
( ( r1(X0,sK58(X0))
& ~ p3(sK58(X0))
& ~ p103(sK58(X0))
& p102(sK58(X0))
& r1(X0,sK59(X0))
& p3(sK59(X0))
& ~ p103(sK59(X0))
& p102(sK59(X0)) )
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK58,sK59]),skolemize(X1,sK58(X0)),skolemize(X2,sK59(X0))],[f116]) ).
fof(f118,plain,
! [X30] :
( ( ? [X59] :
( r1(X30,X59)
& ~ p2(X59)
& ~ p102(X59)
& p101(X59) )
& ? [X60] :
( r1(X30,X60)
& p2(X60)
& ~ p102(X60)
& p101(X60) ) )
| p101(X30)
| ~ p100(X30)
| ~ sP0(X30) ),
inference(nnf_transformation,[],[f9]) ).
fof(f119,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,[],[f118]) ).
fof(f120,plain,
! [X0] :
( ( r1(X0,sK60(X0))
& ~ p2(sK60(X0))
& ~ p102(sK60(X0))
& p101(sK60(X0))
& r1(X0,sK61(X0))
& p2(sK61(X0))
& ~ p102(sK61(X0))
& p101(sK61(X0)) )
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK60,sK61]),skolemize(X1,sK60(X0)),skolemize(X2,sK61(X0))],[f119]) ).
fof(f121,plain,
( ! [X1] :
( ~ r1(sK62,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| p7(X15) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X16] :
( ~ r1(sK62,X16)
| ! [X17] :
( ~ r1(X16,X17)
| ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| sP31(X30) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ~ p101(sK62)
& p100(sK62) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK62]),skolemize(X0,sK62)],[f41]) ).
fof(f122,plain,
! [X0] : r1(X0,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f154,plain,
! [X0] :
( ~ sP31(X0)
| sP0(X0) ),
inference(cnf_transformation,[],[f43]) ).
fof(f155,plain,
! [X0] :
( ~ sP31(X0)
| sP1(X0) ),
inference(cnf_transformation,[],[f43]) ).
fof(f156,plain,
! [X0] :
( ~ sP31(X0)
| sP2(X0) ),
inference(cnf_transformation,[],[f43]) ).
fof(f157,plain,
! [X0] :
( ~ sP31(X0)
| sP3(X0) ),
inference(cnf_transformation,[],[f43]) ).
fof(f158,plain,
! [X0] :
( ~ sP31(X0)
| sP4(X0) ),
inference(cnf_transformation,[],[f43]) ).
fof(f159,plain,
! [X0] :
( ~ sP31(X0)
| sP5(X0) ),
inference(cnf_transformation,[],[f43]) ).
fof(f277,plain,
! [X0] :
( ~ p7(sK50(X0))
| p106(X0)
| ~ p105(X0)
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f105]) ).
fof(f278,plain,
! [X0] :
( r1(X0,sK50(X0))
| p106(X0)
| ~ p105(X0)
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f105]) ).
fof(f279,plain,
! [X0] :
( p105(sK53(X0))
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f108]) ).
fof(f280,plain,
! [X0] :
( ~ p106(sK53(X0))
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f108]) ).
fof(f282,plain,
! [X0] :
( r1(X0,sK53(X0))
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f108]) ).
fof(f291,plain,
! [X0] :
( p104(sK54(X0))
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f111]) ).
fof(f292,plain,
! [X0] :
( ~ p105(sK54(X0))
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f111]) ).
fof(f294,plain,
! [X0] :
( r1(X0,sK54(X0))
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f111]) ).
fof(f299,plain,
! [X0] :
( p103(sK56(X0))
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f114]) ).
fof(f300,plain,
! [X0] :
( ~ p104(sK56(X0))
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f114]) ).
fof(f302,plain,
! [X0] :
( r1(X0,sK56(X0))
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f114]) ).
fof(f307,plain,
! [X0] :
( p102(sK58(X0))
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f117]) ).
fof(f308,plain,
! [X0] :
( ~ p103(sK58(X0))
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f117]) ).
fof(f310,plain,
! [X0] :
( r1(X0,sK58(X0))
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f117]) ).
fof(f311,plain,
! [X0] :
( p101(sK61(X0))
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f120]) ).
fof(f312,plain,
! [X0] :
( ~ p102(sK61(X0))
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f120]) ).
fof(f314,plain,
! [X0] :
( r1(X0,sK61(X0))
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f120]) ).
fof(f319,plain,
p100(sK62),
inference(cnf_transformation,[],[f121]) ).
fof(f320,plain,
~ p101(sK62),
inference(cnf_transformation,[],[f121]) ).
fof(f321,plain,
! [X21,X28,X29,X18,X19,X26,X16,X27,X17,X24,X22,X25,X23,X30,X20] :
( ~ r1(sK62,X16)
| ~ r1(X16,X17)
| ~ r1(X17,X18)
| ~ r1(X18,X19)
| ~ r1(X19,X20)
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| ~ r1(X23,X24)
| ~ r1(X24,X25)
| ~ r1(X25,X26)
| ~ r1(X26,X27)
| ~ r1(X27,X28)
| ~ r1(X28,X29)
| ~ r1(X29,X30)
| sP31(X30) ),
inference(cnf_transformation,[],[f121]) ).
fof(f322,plain,
! [X2,X3,X10,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] :
( ~ r1(sK62,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ r1(X13,X14)
| ~ r1(X14,X15)
| p7(X15) ),
inference(cnf_transformation,[],[f121]) ).
fof(f323,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ r1(sK62,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| sP31(X13) ),
inference(resolution,[],[f321,f122]) ).
fof(f331,definition,
( spl63_1
<=> sP0(sK62) ),
introduced(definition,[new_symbols(definition,[spl63_1])],[avatar_definition]) ).
fof(f332,plain,
( sP0(sK62)
| ~ spl63_1 ),
inference(avatar_component_clause,[],[f331]) ).
fof(f333,plain,
( ~ sP0(sK62)
| spl63_1 ),
inference(avatar_component_clause,[],[f331]) ).
fof(f342,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ r1(sK62,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| p7(X13) ),
inference(resolution,[],[f322,f122]) ).
fof(f613,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ r1(sK62,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| sP31(X12) ),
inference(resolution,[],[f323,f122]) ).
fof(f644,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK62,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| sP31(X11) ),
inference(resolution,[],[f613,f122]) ).
fof(f675,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK62,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| sP31(X10) ),
inference(resolution,[],[f644,f122]) ).
fof(f706,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK62,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| sP31(X9) ),
inference(resolution,[],[f675,f122]) ).
fof(f737,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ r1(sK62,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| sP31(X8) ),
inference(resolution,[],[f706,f122]) ).
fof(f768,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(sK62,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| sP31(X7) ),
inference(resolution,[],[f737,f122]) ).
fof(f799,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK62,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| sP31(X6) ),
inference(resolution,[],[f768,f122]) ).
fof(f830,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK62,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| sP31(X5) ),
inference(resolution,[],[f799,f122]) ).
fof(f861,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK62,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| sP31(X4) ),
inference(resolution,[],[f830,f122]) ).
fof(f892,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK62,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| sP31(X3) ),
inference(resolution,[],[f861,f122]) ).
fof(f922,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK61(sK62),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| sP31(X3)
| p101(sK62)
| ~ p100(sK62)
| ~ sP0(sK62) ),
inference(resolution,[],[f861,f314]) ).
fof(f923,plain,
! [X2,X0,X1] :
( ~ r1(sK62,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP31(X2) ),
inference(resolution,[],[f892,f122]) ).
fof(f953,plain,
! [X2,X0,X1] :
( ~ r1(sK61(sK62),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP31(X2)
| p101(sK62)
| ~ p100(sK62)
| ~ sP0(sK62) ),
inference(resolution,[],[f892,f314]) ).
fof(f954,plain,
! [X0,X1] :
( ~ r1(sK62,X0)
| ~ r1(X0,X1)
| sP31(X1) ),
inference(resolution,[],[f923,f122]) ).
fof(f984,plain,
! [X0,X1] :
( ~ r1(sK61(sK62),X0)
| ~ r1(X0,X1)
| sP31(X1)
| p101(sK62)
| ~ p100(sK62)
| ~ sP0(sK62) ),
inference(resolution,[],[f923,f314]) ).
fof(f985,plain,
! [X0] :
( ~ r1(sK62,X0)
| sP31(X0) ),
inference(resolution,[],[f954,f122]) ).
fof(f1015,plain,
! [X0] :
( ~ r1(sK61(sK62),X0)
| sP31(X0)
| p101(sK62)
| ~ p100(sK62)
| ~ sP0(sK62) ),
inference(resolution,[],[f954,f314]) ).
fof(f1016,plain,
sP31(sK62),
inference(resolution,[],[f985,f122]) ).
fof(f1046,plain,
( sP31(sK61(sK62))
| p101(sK62)
| ~ p100(sK62)
| ~ sP0(sK62) ),
inference(resolution,[],[f985,f314]) ).
fof(f1047,plain,
sP0(sK62),
inference(resolution,[],[f1016,f154]) ).
fof(f1081,plain,
( $false
| spl63_1 ),
inference(forward_subsumption_resolution,[],[f1047,f333]) ).
fof(f1082,plain,
spl63_1,
inference(avatar_contradiction_clause,[],[f1081]) ).
fof(f1103,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK61(sK62),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| sP31(X3)
| ~ p100(sK62)
| ~ sP0(sK62) ),
inference(forward_subsumption_resolution,[],[f922,f320]) ).
fof(f1105,plain,
! [X2,X0,X1] :
( ~ r1(sK61(sK62),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP31(X2)
| ~ p100(sK62)
| ~ sP0(sK62) ),
inference(forward_subsumption_resolution,[],[f953,f320]) ).
fof(f1107,plain,
! [X0,X1] :
( ~ r1(sK61(sK62),X0)
| ~ r1(X0,X1)
| sP31(X1)
| ~ p100(sK62)
| ~ sP0(sK62) ),
inference(forward_subsumption_resolution,[],[f984,f320]) ).
fof(f1109,plain,
! [X0] :
( ~ r1(sK61(sK62),X0)
| sP31(X0)
| ~ p100(sK62)
| ~ sP0(sK62) ),
inference(forward_subsumption_resolution,[],[f1015,f320]) ).
fof(f1111,plain,
( sP31(sK61(sK62))
| ~ p100(sK62)
| ~ sP0(sK62) ),
inference(forward_subsumption_resolution,[],[f1046,f320]) ).
fof(f1133,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK61(sK62),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| sP31(X3)
| ~ sP0(sK62) ),
inference(forward_subsumption_resolution,[],[f1103,f319]) ).
fof(f1135,plain,
! [X2,X0,X1] :
( ~ r1(sK61(sK62),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP31(X2)
| ~ sP0(sK62) ),
inference(forward_subsumption_resolution,[],[f1105,f319]) ).
fof(f1137,plain,
! [X0,X1] :
( ~ r1(sK61(sK62),X0)
| ~ r1(X0,X1)
| sP31(X1)
| ~ sP0(sK62) ),
inference(forward_subsumption_resolution,[],[f1107,f319]) ).
fof(f1139,plain,
! [X0] :
( ~ r1(sK61(sK62),X0)
| sP31(X0)
| ~ sP0(sK62) ),
inference(forward_subsumption_resolution,[],[f1109,f319]) ).
fof(f1141,plain,
( sP31(sK61(sK62))
| ~ sP0(sK62) ),
inference(forward_subsumption_resolution,[],[f1111,f319]) ).
fof(f1163,plain,
( ! [X2,X3,X0,X1] :
( ~ r1(sK61(sK62),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| sP31(X3) )
| ~ spl63_1 ),
inference(forward_subsumption_resolution,[],[f1133,f332]) ).
fof(f1165,plain,
( ! [X2,X0,X1] :
( ~ r1(sK61(sK62),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP31(X2) )
| ~ spl63_1 ),
inference(forward_subsumption_resolution,[],[f1135,f332]) ).
fof(f1167,plain,
( ! [X0,X1] :
( ~ r1(sK61(sK62),X0)
| ~ r1(X0,X1)
| sP31(X1) )
| ~ spl63_1 ),
inference(forward_subsumption_resolution,[],[f1137,f332]) ).
fof(f1169,plain,
( ! [X0] :
( ~ r1(sK61(sK62),X0)
| sP31(X0) )
| ~ spl63_1 ),
inference(forward_subsumption_resolution,[],[f1139,f332]) ).
fof(f1171,plain,
( sP31(sK61(sK62))
| ~ spl63_1 ),
inference(forward_subsumption_resolution,[],[f1141,f332]) ).
fof(f1505,plain,
( sP31(sK58(sK61(sK62)))
| p102(sK61(sK62))
| ~ p101(sK61(sK62))
| ~ sP1(sK61(sK62))
| ~ spl63_1 ),
inference(resolution,[],[f1169,f310]) ).
fof(f1518,definition,
( spl63_120
<=> p101(sK61(sK62)) ),
introduced(definition,[new_symbols(definition,[spl63_120])],[avatar_definition]) ).
fof(f1519,plain,
( ~ p101(sK61(sK62))
| spl63_120 ),
inference(avatar_component_clause,[],[f1518]) ).
fof(f1520,plain,
( p101(sK61(sK62))
| ~ spl63_120 ),
inference(avatar_component_clause,[],[f1518]) ).
fof(f1532,definition,
( spl63_123
<=> sP1(sK61(sK62)) ),
introduced(definition,[new_symbols(definition,[spl63_123])],[avatar_definition]) ).
fof(f1533,plain,
( sP1(sK61(sK62))
| ~ spl63_123 ),
inference(avatar_component_clause,[],[f1532]) ).
fof(f1534,plain,
( ~ sP1(sK61(sK62))
| spl63_123 ),
inference(avatar_component_clause,[],[f1532]) ).
fof(f1536,definition,
( spl63_124
<=> p102(sK61(sK62)) ),
introduced(definition,[new_symbols(definition,[spl63_124])],[avatar_definition]) ).
fof(f1537,plain,
( ~ p102(sK61(sK62))
| spl63_124 ),
inference(avatar_component_clause,[],[f1536]) ).
fof(f1538,plain,
( p102(sK61(sK62))
| ~ spl63_124 ),
inference(avatar_component_clause,[],[f1536]) ).
fof(f1545,definition,
( spl63_126
<=> sP31(sK58(sK61(sK62))) ),
introduced(definition,[new_symbols(definition,[spl63_126])],[avatar_definition]) ).
fof(f1547,plain,
( sP31(sK58(sK61(sK62)))
| ~ spl63_126 ),
inference(avatar_component_clause,[],[f1545]) ).
fof(f1548,plain,
( ~ spl63_123
| ~ spl63_120
| spl63_124
| spl63_126
| ~ spl63_1 ),
inference(avatar_split_clause,[],[f1505,f331,f1545,f1536,f1518,f1532]) ).
fof(f1854,plain,
( sP1(sK61(sK62))
| ~ spl63_1 ),
inference(resolution,[],[f1171,f155]) ).
fof(f1888,plain,
( $false
| ~ spl63_1
| spl63_123 ),
inference(forward_subsumption_resolution,[],[f1854,f1534]) ).
fof(f1889,plain,
( ~ spl63_1
| spl63_123 ),
inference(avatar_contradiction_clause,[],[f1888]) ).
fof(f1919,plain,
( ! [X0] :
( ~ r1(sK58(sK61(sK62)),X0)
| sP31(X0)
| p102(sK61(sK62))
| ~ p101(sK61(sK62))
| ~ sP1(sK61(sK62)) )
| ~ spl63_1 ),
inference(resolution,[],[f1167,f310]) ).
fof(f1981,plain,
( ! [X0,X1] :
( ~ r1(sK58(sK61(sK62)),X0)
| ~ r1(X0,X1)
| sP31(X1)
| p102(sK61(sK62))
| ~ p101(sK61(sK62))
| ~ sP1(sK61(sK62)) )
| ~ spl63_1 ),
inference(resolution,[],[f1165,f310]) ).
fof(f2105,plain,
( ! [X2,X0,X1] :
( ~ r1(sK58(sK61(sK62)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP31(X2)
| p102(sK61(sK62))
| ~ p101(sK61(sK62))
| ~ sP1(sK61(sK62)) )
| ~ spl63_1 ),
inference(resolution,[],[f1163,f310]) ).
fof(f2171,plain,
( p101(sK62)
| ~ p100(sK62)
| ~ sP0(sK62)
| spl63_120 ),
inference(resolution,[],[f1519,f311]) ).
fof(f2172,plain,
( ~ p100(sK62)
| ~ sP0(sK62)
| spl63_120 ),
inference(forward_subsumption_resolution,[],[f2171,f320]) ).
fof(f2173,plain,
( ~ sP0(sK62)
| spl63_120 ),
inference(forward_subsumption_resolution,[],[f2172,f319]) ).
fof(f2174,plain,
( $false
| ~ spl63_1
| spl63_120 ),
inference(forward_subsumption_resolution,[],[f2173,f332]) ).
fof(f2175,plain,
( ~ spl63_1
| spl63_120 ),
inference(avatar_contradiction_clause,[],[f2174]) ).
fof(f2208,plain,
( sP2(sK58(sK61(sK62)))
| ~ spl63_126 ),
inference(resolution,[],[f1547,f156]) ).
fof(f2595,plain,
( p101(sK62)
| ~ p100(sK62)
| ~ sP0(sK62)
| ~ spl63_124 ),
inference(resolution,[],[f1538,f312]) ).
fof(f2596,plain,
( ~ p100(sK62)
| ~ sP0(sK62)
| ~ spl63_124 ),
inference(forward_subsumption_resolution,[],[f2595,f320]) ).
fof(f2597,plain,
( ~ sP0(sK62)
| ~ spl63_124 ),
inference(forward_subsumption_resolution,[],[f2596,f319]) ).
fof(f2598,plain,
( $false
| ~ spl63_1
| ~ spl63_124 ),
inference(forward_subsumption_resolution,[],[f2597,f332]) ).
fof(f2599,plain,
( ~ spl63_1
| ~ spl63_124 ),
inference(avatar_contradiction_clause,[],[f2598]) ).
fof(f2610,plain,
( ! [X0] :
( ~ r1(sK58(sK61(sK62)),X0)
| sP31(X0)
| ~ p101(sK61(sK62))
| ~ sP1(sK61(sK62)) )
| ~ spl63_1
| spl63_124 ),
inference(forward_subsumption_resolution,[],[f1919,f1537]) ).
fof(f2612,plain,
( ! [X0,X1] :
( ~ r1(sK58(sK61(sK62)),X0)
| ~ r1(X0,X1)
| sP31(X1)
| ~ p101(sK61(sK62))
| ~ sP1(sK61(sK62)) )
| ~ spl63_1
| spl63_124 ),
inference(forward_subsumption_resolution,[],[f1981,f1537]) ).
fof(f2614,plain,
( ! [X2,X0,X1] :
( ~ r1(sK58(sK61(sK62)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP31(X2)
| ~ p101(sK61(sK62))
| ~ sP1(sK61(sK62)) )
| ~ spl63_1
| spl63_124 ),
inference(forward_subsumption_resolution,[],[f2105,f1537]) ).
fof(f2618,plain,
( ! [X0] :
( ~ r1(sK58(sK61(sK62)),X0)
| sP31(X0)
| ~ sP1(sK61(sK62)) )
| ~ spl63_1
| ~ spl63_120
| spl63_124 ),
inference(forward_subsumption_resolution,[],[f2610,f1520]) ).
fof(f2620,plain,
( ! [X0,X1] :
( ~ r1(sK58(sK61(sK62)),X0)
| ~ r1(X0,X1)
| sP31(X1)
| ~ sP1(sK61(sK62)) )
| ~ spl63_1
| ~ spl63_120
| spl63_124 ),
inference(forward_subsumption_resolution,[],[f2612,f1520]) ).
fof(f2622,plain,
( ! [X2,X0,X1] :
( ~ r1(sK58(sK61(sK62)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP31(X2)
| ~ sP1(sK61(sK62)) )
| ~ spl63_1
| ~ spl63_120
| spl63_124 ),
inference(forward_subsumption_resolution,[],[f2614,f1520]) ).
fof(f2626,plain,
( ! [X0] :
( ~ r1(sK58(sK61(sK62)),X0)
| sP31(X0) )
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124 ),
inference(forward_subsumption_resolution,[],[f2618,f1533]) ).
fof(f2628,plain,
( ! [X0,X1] :
( ~ r1(sK58(sK61(sK62)),X0)
| ~ r1(X0,X1)
| sP31(X1) )
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124 ),
inference(forward_subsumption_resolution,[],[f2620,f1533]) ).
fof(f2630,plain,
( ! [X2,X0,X1] :
( ~ r1(sK58(sK61(sK62)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP31(X2) )
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124 ),
inference(forward_subsumption_resolution,[],[f2622,f1533]) ).
fof(f2734,plain,
( sP31(sK56(sK58(sK61(sK62))))
| p103(sK58(sK61(sK62)))
| ~ p102(sK58(sK61(sK62)))
| ~ sP2(sK58(sK61(sK62)))
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124 ),
inference(resolution,[],[f2626,f302]) ).
fof(f2745,plain,
( sP31(sK56(sK58(sK61(sK62))))
| p103(sK58(sK61(sK62)))
| ~ p102(sK58(sK61(sK62)))
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126 ),
inference(forward_subsumption_resolution,[],[f2734,f2208]) ).
fof(f2789,definition,
( spl63_244
<=> p102(sK58(sK61(sK62))) ),
introduced(definition,[new_symbols(definition,[spl63_244])],[avatar_definition]) ).
fof(f2790,plain,
( ~ p102(sK58(sK61(sK62)))
| spl63_244 ),
inference(avatar_component_clause,[],[f2789]) ).
fof(f2791,plain,
( p102(sK58(sK61(sK62)))
| ~ spl63_244 ),
inference(avatar_component_clause,[],[f2789]) ).
fof(f2803,definition,
( spl63_247
<=> p103(sK58(sK61(sK62))) ),
introduced(definition,[new_symbols(definition,[spl63_247])],[avatar_definition]) ).
fof(f2804,plain,
( ~ p103(sK58(sK61(sK62)))
| spl63_247 ),
inference(avatar_component_clause,[],[f2803]) ).
fof(f2805,plain,
( p103(sK58(sK61(sK62)))
| ~ spl63_247 ),
inference(avatar_component_clause,[],[f2803]) ).
fof(f2812,definition,
( spl63_249
<=> sP31(sK56(sK58(sK61(sK62)))) ),
introduced(definition,[new_symbols(definition,[spl63_249])],[avatar_definition]) ).
fof(f2814,plain,
( sP31(sK56(sK58(sK61(sK62))))
| ~ spl63_249 ),
inference(avatar_component_clause,[],[f2812]) ).
fof(f2815,plain,
( ~ spl63_244
| spl63_247
| spl63_249
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126 ),
inference(avatar_split_clause,[],[f2745,f1545,f1536,f1532,f1518,f331,f2812,f2803,f2789]) ).
fof(f3040,plain,
( ! [X0] :
( ~ r1(sK56(sK58(sK61(sK62))),X0)
| sP31(X0)
| p103(sK58(sK61(sK62)))
| ~ p102(sK58(sK61(sK62)))
| ~ sP2(sK58(sK61(sK62))) )
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124 ),
inference(resolution,[],[f2628,f302]) ).
fof(f3102,plain,
( ! [X0,X1] :
( ~ r1(sK56(sK58(sK61(sK62))),X0)
| ~ r1(X0,X1)
| sP31(X1)
| p103(sK58(sK61(sK62)))
| ~ p102(sK58(sK61(sK62)))
| ~ sP2(sK58(sK61(sK62))) )
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124 ),
inference(resolution,[],[f2630,f302]) ).
fof(f4613,plain,
( p102(sK61(sK62))
| ~ p101(sK61(sK62))
| ~ sP1(sK61(sK62))
| spl63_244 ),
inference(resolution,[],[f2790,f307]) ).
fof(f4614,plain,
( ~ p101(sK61(sK62))
| ~ sP1(sK61(sK62))
| spl63_124
| spl63_244 ),
inference(forward_subsumption_resolution,[],[f4613,f1537]) ).
fof(f4615,plain,
( ~ sP1(sK61(sK62))
| ~ spl63_120
| spl63_124
| spl63_244 ),
inference(forward_subsumption_resolution,[],[f4614,f1520]) ).
fof(f4616,plain,
( $false
| ~ spl63_120
| ~ spl63_123
| spl63_124
| spl63_244 ),
inference(forward_subsumption_resolution,[],[f4615,f1533]) ).
fof(f4617,plain,
( ~ spl63_120
| ~ spl63_123
| spl63_124
| spl63_244 ),
inference(avatar_contradiction_clause,[],[f4616]) ).
fof(f4619,plain,
( ! [X0] :
( ~ r1(sK56(sK58(sK61(sK62))),X0)
| sP31(X0)
| ~ p102(sK58(sK61(sK62)))
| ~ sP2(sK58(sK61(sK62))) )
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| spl63_247 ),
inference(forward_subsumption_resolution,[],[f3040,f2804]) ).
fof(f4627,plain,
( ! [X0] :
( ~ r1(sK56(sK58(sK61(sK62))),X0)
| sP31(X0)
| ~ sP2(sK58(sK61(sK62))) )
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_244
| spl63_247 ),
inference(forward_subsumption_resolution,[],[f4619,f2791]) ).
fof(f4635,plain,
( ! [X0] :
( ~ r1(sK56(sK58(sK61(sK62))),X0)
| sP31(X0) )
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247 ),
inference(forward_subsumption_resolution,[],[f4627,f2208]) ).
fof(f4645,plain,
( sP3(sK56(sK58(sK61(sK62))))
| ~ spl63_249 ),
inference(resolution,[],[f2814,f157]) ).
fof(f4970,plain,
( sP31(sK54(sK56(sK58(sK61(sK62)))))
| p104(sK56(sK58(sK61(sK62))))
| ~ p103(sK56(sK58(sK61(sK62))))
| ~ sP3(sK56(sK58(sK61(sK62))))
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247 ),
inference(resolution,[],[f4635,f294]) ).
fof(f4985,plain,
( sP31(sK54(sK56(sK58(sK61(sK62)))))
| p104(sK56(sK58(sK61(sK62))))
| ~ p103(sK56(sK58(sK61(sK62))))
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247
| ~ spl63_249 ),
inference(forward_subsumption_resolution,[],[f4970,f4645]) ).
fof(f5041,definition,
( spl63_431
<=> p103(sK56(sK58(sK61(sK62)))) ),
introduced(definition,[new_symbols(definition,[spl63_431])],[avatar_definition]) ).
fof(f5042,plain,
( ~ p103(sK56(sK58(sK61(sK62))))
| spl63_431 ),
inference(avatar_component_clause,[],[f5041]) ).
fof(f5043,plain,
( p103(sK56(sK58(sK61(sK62))))
| ~ spl63_431 ),
inference(avatar_component_clause,[],[f5041]) ).
fof(f5055,definition,
( spl63_434
<=> p104(sK56(sK58(sK61(sK62)))) ),
introduced(definition,[new_symbols(definition,[spl63_434])],[avatar_definition]) ).
fof(f5056,plain,
( ~ p104(sK56(sK58(sK61(sK62))))
| spl63_434 ),
inference(avatar_component_clause,[],[f5055]) ).
fof(f5057,plain,
( p104(sK56(sK58(sK61(sK62))))
| ~ spl63_434 ),
inference(avatar_component_clause,[],[f5055]) ).
fof(f5064,definition,
( spl63_436
<=> sP31(sK54(sK56(sK58(sK61(sK62))))) ),
introduced(definition,[new_symbols(definition,[spl63_436])],[avatar_definition]) ).
fof(f5066,plain,
( sP31(sK54(sK56(sK58(sK61(sK62)))))
| ~ spl63_436 ),
inference(avatar_component_clause,[],[f5064]) ).
fof(f5067,plain,
( ~ spl63_431
| spl63_434
| spl63_436
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247
| ~ spl63_249 ),
inference(avatar_split_clause,[],[f4985,f2812,f2803,f2789,f1545,f1536,f1532,f1518,f331,f5064,f5055,f5041]) ).
fof(f7463,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ r1(sK62,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| p7(X12) ),
inference(resolution,[],[f342,f122]) ).
fof(f7500,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK62,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| p7(X11) ),
inference(resolution,[],[f7463,f122]) ).
fof(f7537,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK62,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| p7(X10) ),
inference(resolution,[],[f7500,f122]) ).
fof(f7574,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK62,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| p7(X9) ),
inference(resolution,[],[f7537,f122]) ).
fof(f7611,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ r1(sK62,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| p7(X8) ),
inference(resolution,[],[f7574,f122]) ).
fof(f7648,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(sK62,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p7(X7) ),
inference(resolution,[],[f7611,f122]) ).
fof(f7685,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK62,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p7(X6) ),
inference(resolution,[],[f7648,f122]) ).
fof(f7722,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK62,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p7(X5) ),
inference(resolution,[],[f7685,f122]) ).
fof(f7789,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK61(sK62),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p7(X4)
| p101(sK62)
| ~ p100(sK62)
| ~ sP0(sK62) ),
inference(resolution,[],[f7722,f314]) ).
fof(f7790,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK61(sK62),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p7(X4)
| ~ p100(sK62)
| ~ sP0(sK62) ),
inference(forward_subsumption_resolution,[],[f7789,f320]) ).
fof(f7792,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK61(sK62),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p7(X4)
| ~ sP0(sK62) ),
inference(forward_subsumption_resolution,[],[f7790,f319]) ).
fof(f7794,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r1(sK61(sK62),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p7(X4) )
| ~ spl63_1 ),
inference(forward_subsumption_resolution,[],[f7792,f332]) ).
fof(f8755,plain,
( ! [X2,X3,X0,X1] :
( ~ r1(sK58(sK61(sK62)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p7(X3)
| p102(sK61(sK62))
| ~ p101(sK61(sK62))
| ~ sP1(sK61(sK62)) )
| ~ spl63_1 ),
inference(resolution,[],[f7794,f310]) ).
fof(f8760,plain,
( ! [X2,X3,X0,X1] :
( ~ r1(sK58(sK61(sK62)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p7(X3)
| ~ p101(sK61(sK62))
| ~ sP1(sK61(sK62)) )
| ~ spl63_1
| spl63_124 ),
inference(forward_subsumption_resolution,[],[f8755,f1537]) ).
fof(f8762,plain,
( ! [X2,X3,X0,X1] :
( ~ r1(sK58(sK61(sK62)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p7(X3)
| ~ sP1(sK61(sK62)) )
| ~ spl63_1
| ~ spl63_120
| spl63_124 ),
inference(forward_subsumption_resolution,[],[f8760,f1520]) ).
fof(f8764,plain,
( ! [X2,X3,X0,X1] :
( ~ r1(sK58(sK61(sK62)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p7(X3) )
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124 ),
inference(forward_subsumption_resolution,[],[f8762,f1533]) ).
fof(f9446,plain,
( ! [X2,X0,X1] :
( ~ r1(sK56(sK58(sK61(sK62))),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p7(X2)
| p103(sK58(sK61(sK62)))
| ~ p102(sK58(sK61(sK62)))
| ~ sP2(sK58(sK61(sK62))) )
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124 ),
inference(resolution,[],[f8764,f302]) ).
fof(f11635,plain,
( p103(sK58(sK61(sK62)))
| ~ p102(sK58(sK61(sK62)))
| ~ sP2(sK58(sK61(sK62)))
| spl63_431 ),
inference(resolution,[],[f5042,f299]) ).
fof(f11636,plain,
( ~ p102(sK58(sK61(sK62)))
| ~ sP2(sK58(sK61(sK62)))
| spl63_247
| spl63_431 ),
inference(forward_subsumption_resolution,[],[f11635,f2804]) ).
fof(f11637,plain,
( ~ sP2(sK58(sK61(sK62)))
| ~ spl63_244
| spl63_247
| spl63_431 ),
inference(forward_subsumption_resolution,[],[f11636,f2791]) ).
fof(f11638,plain,
( $false
| ~ spl63_126
| ~ spl63_244
| spl63_247
| spl63_431 ),
inference(forward_subsumption_resolution,[],[f11637,f2208]) ).
fof(f11639,plain,
( ~ spl63_126
| ~ spl63_244
| spl63_247
| spl63_431 ),
inference(avatar_contradiction_clause,[],[f11638]) ).
fof(f11780,plain,
( p102(sK61(sK62))
| ~ p101(sK61(sK62))
| ~ sP1(sK61(sK62))
| ~ spl63_247 ),
inference(resolution,[],[f2805,f308]) ).
fof(f11781,plain,
( ~ p101(sK61(sK62))
| ~ sP1(sK61(sK62))
| spl63_124
| ~ spl63_247 ),
inference(forward_subsumption_resolution,[],[f11780,f1537]) ).
fof(f11782,plain,
( ~ sP1(sK61(sK62))
| ~ spl63_120
| spl63_124
| ~ spl63_247 ),
inference(forward_subsumption_resolution,[],[f11781,f1520]) ).
fof(f11783,plain,
( $false
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_247 ),
inference(forward_subsumption_resolution,[],[f11782,f1533]) ).
fof(f11784,plain,
( ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_247 ),
inference(avatar_contradiction_clause,[],[f11783]) ).
fof(f11788,plain,
( ! [X0,X1] :
( ~ r1(sK56(sK58(sK61(sK62))),X0)
| ~ r1(X0,X1)
| sP31(X1)
| ~ p102(sK58(sK61(sK62)))
| ~ sP2(sK58(sK61(sK62))) )
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| spl63_247 ),
inference(forward_subsumption_resolution,[],[f3102,f2804]) ).
fof(f11802,plain,
( ! [X2,X0,X1] :
( ~ r1(sK56(sK58(sK61(sK62))),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p7(X2)
| ~ p102(sK58(sK61(sK62)))
| ~ sP2(sK58(sK61(sK62))) )
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| spl63_247 ),
inference(forward_subsumption_resolution,[],[f9446,f2804]) ).
fof(f11816,plain,
( ! [X0,X1] :
( ~ r1(sK56(sK58(sK61(sK62))),X0)
| ~ r1(X0,X1)
| sP31(X1)
| ~ sP2(sK58(sK61(sK62))) )
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_244
| spl63_247 ),
inference(forward_subsumption_resolution,[],[f11788,f2791]) ).
fof(f11830,plain,
( ! [X2,X0,X1] :
( ~ r1(sK56(sK58(sK61(sK62))),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p7(X2)
| ~ sP2(sK58(sK61(sK62))) )
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_244
| spl63_247 ),
inference(forward_subsumption_resolution,[],[f11802,f2791]) ).
fof(f11844,plain,
( ! [X0,X1] :
( ~ r1(sK56(sK58(sK61(sK62))),X0)
| ~ r1(X0,X1)
| sP31(X1) )
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247 ),
inference(forward_subsumption_resolution,[],[f11816,f2208]) ).
fof(f11858,plain,
( ! [X2,X0,X1] :
( ~ r1(sK56(sK58(sK61(sK62))),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p7(X2) )
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247 ),
inference(forward_subsumption_resolution,[],[f11830,f2208]) ).
fof(f11877,plain,
( sP4(sK54(sK56(sK58(sK61(sK62)))))
| ~ spl63_436 ),
inference(resolution,[],[f5066,f158]) ).
fof(f12111,plain,
( ! [X0] :
( ~ r1(sK54(sK56(sK58(sK61(sK62)))),X0)
| sP31(X0)
| p104(sK56(sK58(sK61(sK62))))
| ~ p103(sK56(sK58(sK61(sK62))))
| ~ sP3(sK56(sK58(sK61(sK62)))) )
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247 ),
inference(resolution,[],[f11844,f294]) ).
fof(f12120,plain,
( ! [X0] :
( ~ r1(sK54(sK56(sK58(sK61(sK62)))),X0)
| sP31(X0)
| ~ p103(sK56(sK58(sK61(sK62))))
| ~ sP3(sK56(sK58(sK61(sK62)))) )
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247
| spl63_434 ),
inference(forward_subsumption_resolution,[],[f12111,f5056]) ).
fof(f12122,plain,
( ! [X0] :
( ~ r1(sK54(sK56(sK58(sK61(sK62)))),X0)
| sP31(X0)
| ~ sP3(sK56(sK58(sK61(sK62)))) )
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247
| ~ spl63_431
| spl63_434 ),
inference(forward_subsumption_resolution,[],[f12120,f5043]) ).
fof(f12124,plain,
( ! [X0] :
( ~ r1(sK54(sK56(sK58(sK61(sK62)))),X0)
| sP31(X0) )
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247
| ~ spl63_249
| ~ spl63_431
| spl63_434 ),
inference(forward_subsumption_resolution,[],[f12122,f4645]) ).
fof(f12147,plain,
( sP31(sK53(sK54(sK56(sK58(sK61(sK62))))))
| p105(sK54(sK56(sK58(sK61(sK62)))))
| ~ p104(sK54(sK56(sK58(sK61(sK62)))))
| ~ sP4(sK54(sK56(sK58(sK61(sK62)))))
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247
| ~ spl63_249
| ~ spl63_431
| spl63_434 ),
inference(resolution,[],[f12124,f282]) ).
fof(f12162,plain,
( sP31(sK53(sK54(sK56(sK58(sK61(sK62))))))
| p105(sK54(sK56(sK58(sK61(sK62)))))
| ~ p104(sK54(sK56(sK58(sK61(sK62)))))
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247
| ~ spl63_249
| ~ spl63_431
| spl63_434
| ~ spl63_436 ),
inference(forward_subsumption_resolution,[],[f12147,f11877]) ).
fof(f12205,definition,
( spl63_762
<=> p104(sK54(sK56(sK58(sK61(sK62))))) ),
introduced(definition,[new_symbols(definition,[spl63_762])],[avatar_definition]) ).
fof(f12206,plain,
( ~ p104(sK54(sK56(sK58(sK61(sK62)))))
| spl63_762 ),
inference(avatar_component_clause,[],[f12205]) ).
fof(f12207,plain,
( p104(sK54(sK56(sK58(sK61(sK62)))))
| ~ spl63_762 ),
inference(avatar_component_clause,[],[f12205]) ).
fof(f12219,definition,
( spl63_765
<=> p105(sK54(sK56(sK58(sK61(sK62))))) ),
introduced(definition,[new_symbols(definition,[spl63_765])],[avatar_definition]) ).
fof(f12220,plain,
( ~ p105(sK54(sK56(sK58(sK61(sK62)))))
| spl63_765 ),
inference(avatar_component_clause,[],[f12219]) ).
fof(f12221,plain,
( p105(sK54(sK56(sK58(sK61(sK62)))))
| ~ spl63_765 ),
inference(avatar_component_clause,[],[f12219]) ).
fof(f12223,definition,
( spl63_766
<=> sP31(sK53(sK54(sK56(sK58(sK61(sK62)))))) ),
introduced(definition,[new_symbols(definition,[spl63_766])],[avatar_definition]) ).
fof(f12225,plain,
( sP31(sK53(sK54(sK56(sK58(sK61(sK62))))))
| ~ spl63_766 ),
inference(avatar_component_clause,[],[f12223]) ).
fof(f12226,plain,
( ~ spl63_762
| spl63_765
| spl63_766
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247
| ~ spl63_249
| ~ spl63_431
| spl63_434
| ~ spl63_436 ),
inference(avatar_split_clause,[],[f12162,f5064,f5055,f5041,f2812,f2803,f2789,f1545,f1536,f1532,f1518,f331,f12223,f12219,f12205]) ).
fof(f13091,plain,
( ! [X0,X1] :
( ~ r1(sK54(sK56(sK58(sK61(sK62)))),X0)
| ~ r1(X0,X1)
| p7(X1)
| p104(sK56(sK58(sK61(sK62))))
| ~ p103(sK56(sK58(sK61(sK62))))
| ~ sP3(sK56(sK58(sK61(sK62)))) )
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247 ),
inference(resolution,[],[f11858,f294]) ).
fof(f20540,plain,
( p104(sK56(sK58(sK61(sK62))))
| ~ p103(sK56(sK58(sK61(sK62))))
| ~ sP3(sK56(sK58(sK61(sK62))))
| spl63_762 ),
inference(resolution,[],[f12206,f291]) ).
fof(f20541,plain,
( ~ p103(sK56(sK58(sK61(sK62))))
| ~ sP3(sK56(sK58(sK61(sK62))))
| spl63_434
| spl63_762 ),
inference(forward_subsumption_resolution,[],[f20540,f5056]) ).
fof(f20542,plain,
( ~ sP3(sK56(sK58(sK61(sK62))))
| ~ spl63_431
| spl63_434
| spl63_762 ),
inference(forward_subsumption_resolution,[],[f20541,f5043]) ).
fof(f20543,plain,
( $false
| ~ spl63_249
| ~ spl63_431
| spl63_434
| spl63_762 ),
inference(forward_subsumption_resolution,[],[f20542,f4645]) ).
fof(f20544,plain,
( ~ spl63_249
| ~ spl63_431
| spl63_434
| spl63_762 ),
inference(avatar_contradiction_clause,[],[f20543]) ).
fof(f20637,plain,
( p103(sK58(sK61(sK62)))
| ~ p102(sK58(sK61(sK62)))
| ~ sP2(sK58(sK61(sK62)))
| ~ spl63_434 ),
inference(resolution,[],[f5057,f300]) ).
fof(f20638,plain,
( ~ p102(sK58(sK61(sK62)))
| ~ sP2(sK58(sK61(sK62)))
| spl63_247
| ~ spl63_434 ),
inference(forward_subsumption_resolution,[],[f20637,f2804]) ).
fof(f20639,plain,
( ~ sP2(sK58(sK61(sK62)))
| ~ spl63_244
| spl63_247
| ~ spl63_434 ),
inference(forward_subsumption_resolution,[],[f20638,f2791]) ).
fof(f20640,plain,
( $false
| ~ spl63_126
| ~ spl63_244
| spl63_247
| ~ spl63_434 ),
inference(forward_subsumption_resolution,[],[f20639,f2208]) ).
fof(f20641,plain,
( ~ spl63_126
| ~ spl63_244
| spl63_247
| ~ spl63_434 ),
inference(avatar_contradiction_clause,[],[f20640]) ).
fof(f20653,plain,
( ! [X0,X1] :
( ~ r1(sK54(sK56(sK58(sK61(sK62)))),X0)
| ~ r1(X0,X1)
| p7(X1)
| ~ p103(sK56(sK58(sK61(sK62))))
| ~ sP3(sK56(sK58(sK61(sK62)))) )
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247
| spl63_434 ),
inference(forward_subsumption_resolution,[],[f13091,f5056]) ).
fof(f20665,plain,
( ! [X0,X1] :
( ~ r1(sK54(sK56(sK58(sK61(sK62)))),X0)
| ~ r1(X0,X1)
| p7(X1)
| ~ sP3(sK56(sK58(sK61(sK62)))) )
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247
| ~ spl63_431
| spl63_434 ),
inference(forward_subsumption_resolution,[],[f20653,f5043]) ).
fof(f20677,plain,
( ! [X0,X1] :
( ~ r1(sK54(sK56(sK58(sK61(sK62)))),X0)
| ~ r1(X0,X1)
| p7(X1) )
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247
| ~ spl63_249
| ~ spl63_431
| spl63_434 ),
inference(forward_subsumption_resolution,[],[f20665,f4645]) ).
fof(f20687,plain,
( sP5(sK53(sK54(sK56(sK58(sK61(sK62))))))
| ~ spl63_766 ),
inference(resolution,[],[f12225,f159]) ).
fof(f20997,definition,
( spl63_1397
<=> p105(sK53(sK54(sK56(sK58(sK61(sK62)))))) ),
introduced(definition,[new_symbols(definition,[spl63_1397])],[avatar_definition]) ).
fof(f20998,plain,
( ~ p105(sK53(sK54(sK56(sK58(sK61(sK62))))))
| spl63_1397 ),
inference(avatar_component_clause,[],[f20997]) ).
fof(f20999,plain,
( p105(sK53(sK54(sK56(sK58(sK61(sK62))))))
| ~ spl63_1397 ),
inference(avatar_component_clause,[],[f20997]) ).
fof(f21011,definition,
( spl63_1400
<=> p106(sK53(sK54(sK56(sK58(sK61(sK62)))))) ),
introduced(definition,[new_symbols(definition,[spl63_1400])],[avatar_definition]) ).
fof(f21012,plain,
( ~ p106(sK53(sK54(sK56(sK58(sK61(sK62))))))
| spl63_1400 ),
inference(avatar_component_clause,[],[f21011]) ).
fof(f21013,plain,
( p106(sK53(sK54(sK56(sK58(sK61(sK62))))))
| ~ spl63_1400 ),
inference(avatar_component_clause,[],[f21011]) ).
fof(f21569,plain,
( ! [X0] :
( ~ r1(sK53(sK54(sK56(sK58(sK61(sK62))))),X0)
| p7(X0)
| p105(sK54(sK56(sK58(sK61(sK62)))))
| ~ p104(sK54(sK56(sK58(sK61(sK62)))))
| ~ sP4(sK54(sK56(sK58(sK61(sK62))))) )
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247
| ~ spl63_249
| ~ spl63_431
| spl63_434 ),
inference(resolution,[],[f20677,f282]) ).
fof(f21710,plain,
( p105(sK54(sK56(sK58(sK61(sK62)))))
| ~ p104(sK54(sK56(sK58(sK61(sK62)))))
| ~ sP4(sK54(sK56(sK58(sK61(sK62)))))
| spl63_1397 ),
inference(resolution,[],[f20998,f279]) ).
fof(f21711,plain,
( ~ p104(sK54(sK56(sK58(sK61(sK62)))))
| ~ sP4(sK54(sK56(sK58(sK61(sK62)))))
| spl63_765
| spl63_1397 ),
inference(forward_subsumption_resolution,[],[f21710,f12220]) ).
fof(f21712,plain,
( ~ sP4(sK54(sK56(sK58(sK61(sK62)))))
| ~ spl63_762
| spl63_765
| spl63_1397 ),
inference(forward_subsumption_resolution,[],[f21711,f12207]) ).
fof(f21713,plain,
( $false
| ~ spl63_436
| ~ spl63_762
| spl63_765
| spl63_1397 ),
inference(forward_subsumption_resolution,[],[f21712,f11877]) ).
fof(f21714,plain,
( ~ spl63_436
| ~ spl63_762
| spl63_765
| spl63_1397 ),
inference(avatar_contradiction_clause,[],[f21713]) ).
fof(f21873,plain,
( p104(sK56(sK58(sK61(sK62))))
| ~ p103(sK56(sK58(sK61(sK62))))
| ~ sP3(sK56(sK58(sK61(sK62))))
| ~ spl63_765 ),
inference(resolution,[],[f12221,f292]) ).
fof(f21874,plain,
( ~ p103(sK56(sK58(sK61(sK62))))
| ~ sP3(sK56(sK58(sK61(sK62))))
| spl63_434
| ~ spl63_765 ),
inference(forward_subsumption_resolution,[],[f21873,f5056]) ).
fof(f21875,plain,
( ~ sP3(sK56(sK58(sK61(sK62))))
| ~ spl63_431
| spl63_434
| ~ spl63_765 ),
inference(forward_subsumption_resolution,[],[f21874,f5043]) ).
fof(f21876,plain,
( $false
| ~ spl63_249
| ~ spl63_431
| spl63_434
| ~ spl63_765 ),
inference(forward_subsumption_resolution,[],[f21875,f4645]) ).
fof(f21877,plain,
( ~ spl63_249
| ~ spl63_431
| spl63_434
| ~ spl63_765 ),
inference(avatar_contradiction_clause,[],[f21876]) ).
fof(f21884,plain,
( ! [X0] :
( ~ r1(sK53(sK54(sK56(sK58(sK61(sK62))))),X0)
| p7(X0)
| ~ p104(sK54(sK56(sK58(sK61(sK62)))))
| ~ sP4(sK54(sK56(sK58(sK61(sK62))))) )
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247
| ~ spl63_249
| ~ spl63_431
| spl63_434
| spl63_765 ),
inference(forward_subsumption_resolution,[],[f21569,f12220]) ).
fof(f21892,plain,
( ! [X0] :
( ~ r1(sK53(sK54(sK56(sK58(sK61(sK62))))),X0)
| p7(X0)
| ~ sP4(sK54(sK56(sK58(sK61(sK62))))) )
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247
| ~ spl63_249
| ~ spl63_431
| spl63_434
| ~ spl63_762
| spl63_765 ),
inference(forward_subsumption_resolution,[],[f21884,f12207]) ).
fof(f21900,plain,
( ! [X0] :
( ~ r1(sK53(sK54(sK56(sK58(sK61(sK62))))),X0)
| p7(X0) )
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247
| ~ spl63_249
| ~ spl63_431
| spl63_434
| ~ spl63_436
| ~ spl63_762
| spl63_765 ),
inference(forward_subsumption_resolution,[],[f21892,f11877]) ).
fof(f22553,plain,
( p7(sK50(sK53(sK54(sK56(sK58(sK61(sK62)))))))
| p106(sK53(sK54(sK56(sK58(sK61(sK62))))))
| ~ p105(sK53(sK54(sK56(sK58(sK61(sK62))))))
| ~ sP5(sK53(sK54(sK56(sK58(sK61(sK62))))))
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247
| ~ spl63_249
| ~ spl63_431
| spl63_434
| ~ spl63_436
| ~ spl63_762
| spl63_765 ),
inference(resolution,[],[f21900,f278]) ).
fof(f22565,plain,
( p106(sK53(sK54(sK56(sK58(sK61(sK62))))))
| ~ p105(sK53(sK54(sK56(sK58(sK61(sK62))))))
| ~ sP5(sK53(sK54(sK56(sK58(sK61(sK62))))))
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247
| ~ spl63_249
| ~ spl63_431
| spl63_434
| ~ spl63_436
| ~ spl63_762
| spl63_765 ),
inference(forward_subsumption_resolution,[],[f22553,f277]) ).
fof(f22566,plain,
( ~ p105(sK53(sK54(sK56(sK58(sK61(sK62))))))
| ~ sP5(sK53(sK54(sK56(sK58(sK61(sK62))))))
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247
| ~ spl63_249
| ~ spl63_431
| spl63_434
| ~ spl63_436
| ~ spl63_762
| spl63_765
| spl63_1400 ),
inference(forward_subsumption_resolution,[],[f22565,f21012]) ).
fof(f22567,plain,
( ~ sP5(sK53(sK54(sK56(sK58(sK61(sK62))))))
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247
| ~ spl63_249
| ~ spl63_431
| spl63_434
| ~ spl63_436
| ~ spl63_762
| spl63_765
| ~ spl63_1397
| spl63_1400 ),
inference(forward_subsumption_resolution,[],[f22566,f20999]) ).
fof(f22568,plain,
( $false
| ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247
| ~ spl63_249
| ~ spl63_431
| spl63_434
| ~ spl63_436
| ~ spl63_762
| spl63_765
| ~ spl63_766
| ~ spl63_1397
| spl63_1400 ),
inference(forward_subsumption_resolution,[],[f22567,f20687]) ).
fof(f22569,plain,
( ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247
| ~ spl63_249
| ~ spl63_431
| spl63_434
| ~ spl63_436
| ~ spl63_762
| spl63_765
| ~ spl63_766
| ~ spl63_1397
| spl63_1400 ),
inference(avatar_contradiction_clause,[],[f22568]) ).
fof(f22632,plain,
( p105(sK54(sK56(sK58(sK61(sK62)))))
| ~ p104(sK54(sK56(sK58(sK61(sK62)))))
| ~ sP4(sK54(sK56(sK58(sK61(sK62)))))
| ~ spl63_1400 ),
inference(resolution,[],[f21013,f280]) ).
fof(f22633,plain,
( ~ p104(sK54(sK56(sK58(sK61(sK62)))))
| ~ sP4(sK54(sK56(sK58(sK61(sK62)))))
| spl63_765
| ~ spl63_1400 ),
inference(forward_subsumption_resolution,[],[f22632,f12220]) ).
fof(f22634,plain,
( ~ sP4(sK54(sK56(sK58(sK61(sK62)))))
| ~ spl63_762
| spl63_765
| ~ spl63_1400 ),
inference(forward_subsumption_resolution,[],[f22633,f12207]) ).
fof(f22635,plain,
( $false
| ~ spl63_436
| ~ spl63_762
| spl63_765
| ~ spl63_1400 ),
inference(forward_subsumption_resolution,[],[f22634,f11877]) ).
fof(f22636,plain,
( ~ spl63_436
| ~ spl63_762
| spl63_765
| ~ spl63_1400 ),
inference(avatar_contradiction_clause,[],[f22635]) ).
cnf(s42,plain,
spl63_1,
inference(sat_conversion,[],[f1082]) ).
cnf(s76,plain,
( ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| spl63_126 ),
inference(sat_conversion,[],[f1548]) ).
cnf(s131,plain,
( ~ spl63_1
| spl63_123 ),
inference(sat_conversion,[],[f1889]) ).
cnf(s133,plain,
( ~ spl63_1
| spl63_120 ),
inference(sat_conversion,[],[f2175]) ).
cnf(s179,plain,
( ~ spl63_1
| ~ spl63_124 ),
inference(sat_conversion,[],[f2599]) ).
cnf(s200,plain,
( ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247
| spl63_249 ),
inference(sat_conversion,[],[f2815]) ).
cnf(s286,plain,
( ~ spl63_120
| ~ spl63_123
| spl63_124
| spl63_244 ),
inference(sat_conversion,[],[f4617]) ).
cnf(s324,plain,
( ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247
| ~ spl63_249
| ~ spl63_431
| spl63_434
| spl63_436 ),
inference(sat_conversion,[],[f5067]) ).
cnf(s537,plain,
( ~ spl63_126
| ~ spl63_244
| spl63_247
| spl63_431 ),
inference(sat_conversion,[],[f11639]) ).
cnf(s540,plain,
( ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_247 ),
inference(sat_conversion,[],[f11784]) ).
cnf(s547,plain,
( ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247
| ~ spl63_249
| ~ spl63_431
| spl63_434
| ~ spl63_436
| ~ spl63_762
| spl63_765
| spl63_766 ),
inference(sat_conversion,[],[f12226]) ).
cnf(s962,plain,
( ~ spl63_249
| ~ spl63_431
| spl63_434
| spl63_762 ),
inference(sat_conversion,[],[f20544]) ).
cnf(s965,plain,
( ~ spl63_126
| ~ spl63_244
| spl63_247
| ~ spl63_434 ),
inference(sat_conversion,[],[f20641]) ).
cnf(s1024,plain,
( ~ spl63_436
| ~ spl63_762
| spl63_765
| spl63_1397 ),
inference(sat_conversion,[],[f21714]) ).
cnf(s1030,plain,
( ~ spl63_249
| ~ spl63_431
| spl63_434
| ~ spl63_765 ),
inference(sat_conversion,[],[f21877]) ).
cnf(s1089,plain,
( ~ spl63_1
| ~ spl63_120
| ~ spl63_123
| spl63_124
| ~ spl63_126
| ~ spl63_244
| spl63_247
| ~ spl63_249
| ~ spl63_431
| spl63_434
| ~ spl63_436
| ~ spl63_762
| spl63_765
| ~ spl63_766
| ~ spl63_1397
| spl63_1400 ),
inference(sat_conversion,[],[f22569]) ).
cnf(s1092,plain,
( ~ spl63_436
| ~ spl63_762
| spl63_765
| ~ spl63_1400 ),
inference(sat_conversion,[],[f22636]) ).
cnf(s1095,plain,
~ spl63_124,
inference(rat,[],[s179,s42]) ).
cnf(s1096,plain,
spl63_120,
inference(rat,[],[s133,s42]) ).
cnf(s1098,plain,
spl63_123,
inference(rat,[],[s131,s42]) ).
cnf(s1129,plain,
spl63_126,
inference(rat,[],[s76,s42,s1095,s1098,s1096]) ).
cnf(s1131,plain,
~ spl63_247,
inference(rat,[],[s540,s1096,s1095,s1098]) ).
cnf(s1133,plain,
spl63_244,
inference(rat,[],[s286,s1096,s1095,s1098]) ).
cnf(s1145,plain,
spl63_249,
inference(rat,[],[s200,s1098,s1131,s1133,s1096,s1095,s42,s1129]) ).
cnf(s1163,plain,
~ spl63_434,
inference(rat,[],[s965,s1129,s1131,s1133]) ).
cnf(s1166,plain,
spl63_431,
inference(rat,[],[s537,s1129,s1131,s1133]) ).
cnf(s1174,plain,
~ spl63_765,
inference(rat,[],[s1030,s1145,s1163,s1166]) ).
cnf(s1175,plain,
spl63_762,
inference(rat,[],[s962,s1145,s1163,s1166]) ).
cnf(s1176,plain,
spl63_436,
inference(rat,[],[s324,s1145,s1163,s1129,s1098,s1131,s1133,s1096,s1095,s42,s1166]) ).
cnf(s1178,plain,
~ spl63_1400,
inference(rat,[],[s1092,s1175,s1174,s1176]) ).
cnf(s1179,plain,
spl63_1397,
inference(rat,[],[s1024,s1175,s1174,s1176]) ).
cnf(s1180,plain,
~ spl63_766,
inference(rat,[],[s1089,s1178,s1179,s1166,s1174,s1175,s1145,s1163,s1129,s1098,s1131,s1133,s1096,s1095,s42,s1176]) ).
cnf(s1182,plain,
$false,
inference(rat,[],[s547,s1166,s1174,s1175,s1145,s1163,s1129,s1098,s1131,s1133,s1096,s1095,s42,s1180,s1176]) ).
fof(f22637,plain,
$false,
inference(avatar_sat_refutation,[],[s1182]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL656+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n011.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 16:20:15 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.53/2.58 % (2595482)Detected formulas, will run a generic FOF schedule.
% 11.53/2.58 % (2595490)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3355766773:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.53/2.58 % (2595490)Instruction limit reached!
% 11.53/2.58 % (2595490)------------------------------
% 11.53/2.58 % (2595490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.53/2.58 % (2595490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.53/2.58 % (2595490)CaDiCaL version: 2.1.3
% 11.53/2.58 % (2595490)Termination reason: Instruction limit
% 11.53/2.58 % (2595490)Termination phase: Saturation
% 11.53/2.58 % (2595490)Time elapsed: 0.032 s
% 11.53/2.58 % (2595490)Peak memory usage: 90 MB
% 11.53/2.58 % (2595490)Instructions burned: 113 (million)
% 11.53/2.58 % (2595487)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=3675132283:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.53/2.58 % (2595493)dis-21_1_sil=8000:lcm=predicate:random_seed=3515939254: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)
% 11.53/2.58 % (2595488)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=3546401204:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.53/2.58 % (2595491)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3340309770:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.53/2.58 % (2595489)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=1470156854:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.53/2.58 % (2595492)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2444101557:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.53/2.58 % (2595491)Instruction limit reached!
% 11.53/2.58 % (2595491)------------------------------
% 11.53/2.58 % (2595491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.53/2.58 % (2595491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.53/2.58 % (2595491)CaDiCaL version: 2.1.3
% 11.53/2.58 % (2595491)Termination reason: Instruction limit
% 11.53/2.58 % (2595491)Termination phase: Saturation
% 11.53/2.58 % (2595491)Time elapsed: 0.043 s
% 11.53/2.58 % (2595491)Peak memory usage: 87 MB
% 11.53/2.58 % (2595491)Instructions burned: 122 (million)
% 11.53/2.58 % (2595493)Instruction limit reached!
% 11.53/2.58 % (2595493)------------------------------
% 11.53/2.58 % (2595493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.53/2.58 % (2595493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.53/2.58 % (2595493)CaDiCaL version: 2.1.3
% 11.53/2.58 % (2595493)Termination reason: Instruction limit
% 11.53/2.58 % (2595493)Termination phase: Saturation
% 11.53/2.58 % (2595493)Time elapsed: 0.045 s
% 11.53/2.58 % (2595493)Peak memory usage: 88 MB
% 11.53/2.58 % (2595493)Instructions burned: 129 (million)
% 11.53/2.58 % (2595492)Instruction limit reached!
% 11.53/2.58 % (2595492)------------------------------
% 11.53/2.58 % (2595492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.53/2.58 % (2595492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.53/2.58 % (2595492)CaDiCaL version: 2.1.3
% 11.53/2.58 % (2595492)Termination reason: Instruction limit
% 11.53/2.58 % (2595492)Termination phase: Saturation
% 11.53/2.58 % (2595492)Time elapsed: 0.052 s
% 11.53/2.58 % (2595492)Peak memory usage: 89 MB
% 11.53/2.58 % (2595492)Instructions burned: 139 (million)
% 11.53/2.58 % (2595495)lrs+10_1_sil=8000:sp=occurrence:random_seed=3530886388:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 11.53/2.58 % (2595495)Instruction limit reached!
% 11.53/2.58 % (2595495)------------------------------
% 11.53/2.58 % (2595495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.53/2.58 % (2595495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.53/2.58 % (2595495)CaDiCaL version: 2.1.3
% 11.53/2.58 % (2595495)Termination reason: Instruction limit
% 11.53/2.58 % (2595495)Termination phase: Saturation
% 11.53/2.58 % (2595495)Time elapsed: 0.067 s
% 11.53/2.58 % (2595495)Peak memory usage: 92 MB
% 11.53/2.58 % (2595495)Instructions burned: 288 (million)
% 12.78/2.75 % (2595502)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2604815595:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 12.78/2.75 % (2595503)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1102240288:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 12.78/2.75 % (2595504)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=2381992638:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 12.78/2.75 % (2595502)Instruction limit reached!
% 12.78/2.75 % (2595502)------------------------------
% 12.78/2.75 % (2595502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.78/2.75 % (2595502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.78/2.75 % (2595502)CaDiCaL version: 2.1.3
% 12.78/2.75 % (2595502)Termination reason: Instruction limit
% 12.78/2.75 % (2595502)Termination phase: Saturation
% 12.78/2.75 % (2595502)Time elapsed: 0.066 s
% 12.78/2.75 % (2595502)Peak memory usage: 88 MB
% 12.78/2.75 % (2595502)Instructions burned: 158 (million)
% 12.78/2.75 % (2595506)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=540160812:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 12.78/2.75 % (2595504)Instruction limit reached!
% 12.78/2.75 % (2595504)------------------------------
% 12.78/2.75 % (2595504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.78/2.75 % (2595504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.78/2.75 % (2595504)CaDiCaL version: 2.1.3
% 12.78/2.75 % (2595504)Termination reason: Instruction limit
% 12.78/2.75 % (2595504)Termination phase: Saturation
% 12.78/2.75 % (2595504)Time elapsed: 0.106 s
% 12.78/2.75 % (2595504)Peak memory usage: 88 MB
% 12.78/2.75 % (2595504)Instructions burned: 249 (million)
% 12.78/2.75 % (2595503)Instruction limit reached!
% 12.78/2.75 % (2595503)------------------------------
% 12.78/2.75 % (2595503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.78/2.75 % (2595503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.78/2.75 % (2595503)CaDiCaL version: 2.1.3
% 12.78/2.75 % (2595503)Termination reason: Instruction limit
% 12.78/2.75 % (2595503)Termination phase: Saturation
% 12.78/2.75 % (2595503)Time elapsed: 0.162 s
% 12.78/2.75 % (2595503)Peak memory usage: 94 MB
% 12.78/2.75 % (2595503)Instructions burned: 326 (million)
% 12.78/2.75 % (2595506)Instruction limit reached!
% 12.78/2.75 % (2595506)------------------------------
% 12.78/2.75 % (2595506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.78/2.75 % (2595506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.78/2.75 % (2595506)CaDiCaL version: 2.1.3
% 12.78/2.75 % (2595506)Termination reason: Instruction limit
% 12.78/2.75 % (2595506)Termination phase: Saturation
% 12.78/2.75 % (2595506)Time elapsed: 0.074 s
% 12.78/2.75 % (2595506)Peak memory usage: 93 MB
% 12.78/2.75 % (2595506)Instructions burned: 299 (million)
% 12.78/2.75 % (2595510)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3239736646:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 12.78/2.75 % (2595512)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=435695308:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi)
% 12.78/2.75 % (2595514)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2700389915:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi)
% 12.78/2.75 % (2595514)Instruction limit reached!
% 12.78/2.75 % (2595514)------------------------------
% 12.78/2.75 % (2595514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.78/2.75 % (2595514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.78/2.75 % (2595514)CaDiCaL version: 2.1.3
% 12.78/2.75 % (2595514)Termination reason: Instruction limit
% 12.78/2.75 % (2595514)Termination phase: Saturation
% 12.78/2.75 % (2595514)Time elapsed: 0.021 s
% 12.78/2.75 % (2595514)Peak memory usage: 88 MB
% 12.78/2.75 % (2595514)Instructions burned: 117 (million)
% 12.78/2.75 % (2595513)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=344501216:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 12.78/2.75 % (2595512)Instruction limit reached!
% 12.78/2.75 % (2595512)------------------------------
% 12.78/2.75 % (2595512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.78/2.75 % (2595512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.78/2.75 % (2595512)CaDiCaL version: 2.1.3
% 12.78/2.75 % (2595512)Termination reason: Instruction limit
% 12.78/2.75 % (2595512)Termination phase: Saturation
% 12.78/2.75 % (2595512)Time elapsed: 0.056 s
% 12.78/2.75 % (2595512)Peak memory usage: 89 MB
% 12.78/2.75 % (2595512)Instructions burned: 113 (million)
% 12.78/2.75 % (2595513)Instruction limit reached!
% 12.78/2.75 % (2595513)------------------------------
% 12.78/2.75 % (2595513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.78/2.75 % (2595513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.78/2.75 % (2595513)CaDiCaL version: 2.1.3
% 12.78/2.75 % (2595513)Termination reason: Instruction limit
% 12.78/2.75 % (2595513)Termination phase: Saturation
% 12.78/2.75 % (2595513)Time elapsed: 0.064 s
% 12.78/2.75 % (2595513)Peak memory usage: 89 MB
% 12.78/2.75 % (2595513)Instructions burned: 127 (million)
% 12.78/2.75 % (2595518)lrs+10_1_sil=8000:sp=occurrence:random_seed=3439052852:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2993 on theBenchmark for (2993ds/907Mi)
% 12.78/2.75 % (2595520)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=573576928:i=437:sd=1:aac=none:ss=included_2993 on theBenchmark for (2993ds/437Mi)
% 12.78/2.75 % (2595521)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4229127501:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi)
% 12.78/2.75 % (2595520)Instruction limit reached!
% 12.78/2.75 % (2595520)------------------------------
% 12.78/2.75 % (2595520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.78/2.75 % (2595520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.78/2.75 % (2595520)CaDiCaL version: 2.1.3
% 12.78/2.75 % (2595520)Termination reason: Instruction limit
% 12.78/2.75 % (2595520)Termination phase: Saturation
% 12.78/2.75 % (2595520)Time elapsed: 0.148 s
% 12.78/2.75 % (2595520)Peak memory usage: 90 MB
% 12.78/2.75 % (2595520)Instructions burned: 437 (million)
% 12.78/2.75 % (2595525)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3286481225:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi)
% 12.78/2.75 % (2595518)Instruction limit reached!
% 12.78/2.75 % (2595518)------------------------------
% 12.78/2.75 % (2595518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.78/2.75 % (2595518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.78/2.75 % (2595518)CaDiCaL version: 2.1.3
% 12.78/2.75 % (2595518)Termination reason: Instruction limit
% 12.78/2.75 % (2595518)Termination phase: Saturation
% 12.78/2.75 % (2595518)Time elapsed: 0.361 s
% 12.78/2.75 % (2595518)Peak memory usage: 97 MB
% 12.78/2.75 % (2595518)Instructions burned: 907 (million)
% 12.78/2.75 % (2595525)Instruction limit reached!
% 12.78/2.75 % (2595525)------------------------------
% 12.78/2.75 % (2595525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.78/2.75 % (2595525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.78/2.75 % (2595525)CaDiCaL version: 2.1.3
% 12.78/2.75 % (2595525)Termination reason: Instruction limit
% 12.78/2.75 % (2595525)Termination phase: Saturation
% 12.78/2.75 % (2595525)Time elapsed: 0.057 s
% 12.78/2.75 % (2595525)Peak memory usage: 88 MB
% 12.78/2.75 % (2595525)Instructions burned: 135 (million)
% 12.78/2.75 % (2595527)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2217658090:st=8:i=592:sd=3:ep=RST:ss=axioms_2988 on theBenchmark for (2988ds/592Mi)
% 12.78/2.75 % (2595528)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=672504780:st=3:i=13193:sd=3:ss=axioms_2987 on theBenchmark for (2987ds/13193Mi)
% 12.78/2.75 % (2595527)Instruction limit reached!
% 12.78/2.75 % (2595527)------------------------------
% 12.78/2.75 % (2595527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.78/2.75 % (2595527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.78/2.75 % (2595527)CaDiCaL version: 2.1.3
% 12.78/2.75 % (2595527)Termination reason: Instruction limit
% 12.78/2.75 % (2595527)Termination phase: Saturation
% 12.78/2.75 % (2595527)Time elapsed: 0.222 s
% 12.78/2.75 % (2595527)Peak memory usage: 93 MB
% 12.78/2.75 % (2595527)Instructions burned: 594 (million)
% 12.78/2.75 % (2595487)First to succeed.
% 12.78/2.75 % (2595487)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2595482"
% 12.78/2.75 % (2595531)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=703153956:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/125Mi)
% 12.78/2.75 % (2595531)Instruction limit reached!
% 12.78/2.75 % (2595531)------------------------------
% 12.78/2.75 % (2595531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.78/2.75 % (2595531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.78/2.75 % (2595531)CaDiCaL version: 2.1.3
% 12.78/2.75 % (2595531)Termination reason: Instruction limit
% 12.78/2.75 % (2595531)Termination phase: Saturation
% 12.78/2.75 % (2595531)Time elapsed: 0.079 s
% 12.78/2.75 % (2595531)Peak memory usage: 90 MB
% 12.78/2.75 % (2595531)Instructions burned: 126 (million)
% 12.78/2.75 % (2595487)Refutation found. Thanks to Tanya!
% 12.78/2.75 % SZS status Theorem for theBenchmark
% 12.78/2.75 % SZS output start Proof for theBenchmark
% See solution above
% 13.94/2.94 % (2595487)------------------------------
% 13.94/2.94 % (2595487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.94/2.94 % (2595487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.94/2.94 % (2595487)CaDiCaL version: 2.1.3
% 13.94/2.94 % (2595487)Termination reason: Refutation
% 13.94/2.94 % (2595487)Time elapsed: 1.455 s
% 13.94/2.94 % (2595487)Peak memory usage: 146 MB
% 13.94/2.94 % (2595487)Instructions burned: 2461 (million)
% 13.94/2.94 % (2595487)------------------------------
% 13.94/2.94 % (2595487)------------------------------
% 13.94/2.94 % (2595482)Success in time 1.893 s
% 13.94/2.94 % Vampire exiting
%------------------------------------------------------------------------------