%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW095+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n001.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 01:29:36 PM UTC 2026
% Result : Theorem 28.73s 4.77s
% Output : Refutation 29.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 160
% Syntax : Number of formulae : 735 ( 76 unt; 138 def)
% Number of atoms : 4972 ( 806 equ)
% Maximal formula atoms : 521 ( 6 avg)
% Number of connectives : 6795 (2558 ~;2904 |;1273 &)
% ( 60 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 144 ( 142 usr; 87 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 16 con; 0-1 aty)
% Number of variables : 621 ( 0 sgn 435 !; 186 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1] :
( ~ ( integer(X0)
& integer(X1) )
| ~ ( lteq(X0,X1)
& lteq(X1,X0) )
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_tptp_2) ).
fof(f6,axiom,
object(nn),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sort_info_nn) ).
fof(f8,axiom,
object(prev_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sort_info_prev_2) ).
fof(f10,axiom,
! [X0] : integer(node_key(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sort_info_node_key) ).
fof(f11,axiom,
object(null),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sort_info_null) ).
fof(f13,axiom,
object(sortedList_first),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sort_info_sortedList_first) ).
fof(f14,axiom,
! [X0] : object(node_next(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sort_info_node_next) ).
fof(f16,axiom,
! [X0,X1,X2] :
( ~ ( object(X0)
& object(X1)
& object(X2) )
| ~ v__1(X0,X1,X1)
| ~ v__1(X1,X2,X2)
| v__1(X0,X2,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp_tptp_2) ).
fof(f19,axiom,
! [X0,X1,X2] :
( ~ ( object(X0)
& object(X1)
& object(X2) )
| ~ v__1(X0,X1,X1)
| ~ v__1(X0,X2,X2)
| v__1(X0,X1,X2)
| v__1(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp_tptp_5) ).
fof(f20,axiom,
! [X0,X1,X2] :
( ~ ( object(X0)
& object(X1)
& object(X2) )
| ~ v__1(X0,X1,X2)
| ( v__1(X0,X1,X1)
& v__1(X1,X2,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp_tptp_6) ).
fof(f23,axiom,
! [X0,X1] :
( ~ ( object(X0)
& object(X1) )
| X0 != node_next(X0)
| ~ v__1(X0,X1,X1)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp_tptp_9) ).
fof(f26,axiom,
prev_2 != null,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp_tptp_12) ).
fof(f27,axiom,
? [X0,X1] :
( integer(X0)
& integer(X1)
& lteq(X0,X1)
& X0 = node_key(nn)
& X1 = node_key(nn) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp_tptp_13) ).
fof(f30,axiom,
( v__1(nn,nn,nn)
| nn = null
| ~ v__1(sortedList_first,nn,nn) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp_tptp_16) ).
fof(f31,axiom,
( prev_2 = null
| ( prev_2 != null
& v__1(sortedList_first,prev_2,prev_2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp_tptp_17) ).
fof(f32,axiom,
( nn = null
| ( nn != null
& v__1(sortedList_first,nn,nn) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp_tptp_18) ).
fof(f34,axiom,
( prev_2 = null
| nn = node_next(prev_2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp_tptp_20) ).
fof(f44,axiom,
! [X0,X1] :
( ~ ( object(X0)
& object(X1) )
| ~ v__1(sortedList_first,X0,X0)
| X0 = null
| ! [X2] :
( ~ object(X2)
| ~ v__1(X2,X1,X1)
| X2 != node_next(X0) )
| X1 = null
| ( ! [X3,X4] :
( ~ ( integer(X3)
& integer(X4) )
| X3 != node_key(X0)
| X4 != node_key(X1)
| lteq(X3,X4) )
& ! [X5] :
( ~ integer(X5)
| X5 != node_key(X0)
| X5 != node_key(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp_tptp_30) ).
fof(f45,axiom,
! [X0,X1] :
( ~ ( object(X0)
& object(X1) )
| X0 = null
| X1 = null
| X1 != node_next(X0)
| ( X1 != null
& v__1(sortedList_first,X1,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp_tptp_31) ).
fof(f47,axiom,
nn != null,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp_tptp_33) ).
fof(f57,axiom,
null = node_next(null),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp_tptp_43) ).
fof(f59,conjecture,
! [X0] :
( ~ object(X0)
| X0 = null
| ( ( ( ( ~ v__1(sortedList_first,X0,X0)
| ( ~ v__1(sortedList_first,X0,nn)
& ( ~ v__1(sortedList_first,X0,X0)
| v__1(sortedList_first,nn,nn) ) ) )
& ( nn = X0
| ( ~ v__1(sortedList_first,nn,X0)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,X0,X0) ) )
| ~ v__1(sortedList_first,X0,nn)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) ) )
& ( nn = X0
| ( ~ v__1(sortedList_first,nn,X0)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,X0,X0) ) )
| ~ v__1(null,X0,X0)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) ) ) )
| ( ( ~ v__1(sortedList_first,X0,prev_2)
| ( ~ v__1(sortedList_first,prev_2,nn)
& ( ~ v__1(sortedList_first,prev_2,prev_2)
| v__1(sortedList_first,nn,nn) ) ) )
& ( nn = prev_2
| ( ~ v__1(sortedList_first,nn,prev_2)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,prev_2,prev_2) ) )
| ~ v__1(sortedList_first,X0,nn)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) ) )
& ( nn = prev_2
| ( ~ v__1(sortedList_first,nn,prev_2)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,prev_2,prev_2) ) )
| ~ v__1(null,X0,prev_2)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) ) )
& ( ( ( ~ v__1(sortedList_first,X0,X0)
| ( ~ v__1(sortedList_first,X0,nn)
& ( ~ v__1(sortedList_first,X0,X0)
| v__1(sortedList_first,nn,nn) ) ) )
& ( nn = X0
| ( ~ v__1(sortedList_first,nn,X0)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,X0,X0) ) )
| ~ v__1(sortedList_first,X0,nn)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) ) )
& ( nn = X0
| ( ~ v__1(sortedList_first,nn,X0)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,X0,X0) ) )
| ~ v__1(null,X0,X0)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) ) ) )
| ( v__1(sortedList_first,prev_2,prev_2)
& ( v__1(sortedList_first,prev_2,nn)
| ( v__1(sortedList_first,prev_2,prev_2)
& ~ v__1(sortedList_first,nn,nn) ) ) )
| ( nn != prev_2
& v__1(sortedList_first,prev_2,nn)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) )
& ( v__1(sortedList_first,nn,prev_2)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,prev_2,prev_2) ) ) )
| ( nn != prev_2
& v__1(null,prev_2,prev_2)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) )
& ( v__1(sortedList_first,nn,prev_2)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,prev_2,prev_2) ) ) ) ) ) )
& ( prev_2 = X0
| ( ( ~ v__1(sortedList_first,prev_2,X0)
| ( ~ v__1(sortedList_first,X0,nn)
& ( ~ v__1(sortedList_first,X0,X0)
| v__1(sortedList_first,nn,nn) ) ) )
& ( nn = X0
| ( ~ v__1(sortedList_first,nn,X0)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,X0,X0) ) )
| ~ v__1(sortedList_first,prev_2,nn)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) ) )
& ( nn = X0
| ( ~ v__1(sortedList_first,nn,X0)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,X0,X0) ) )
| ~ v__1(null,prev_2,X0)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) ) )
& ( ( ( ~ v__1(sortedList_first,prev_2,prev_2)
| ( ~ v__1(sortedList_first,prev_2,nn)
& ( ~ v__1(sortedList_first,prev_2,prev_2)
| v__1(sortedList_first,nn,nn) ) ) )
& ( nn = prev_2
| ( ~ v__1(sortedList_first,nn,prev_2)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,prev_2,prev_2) ) )
| ~ v__1(sortedList_first,prev_2,nn)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) ) )
& ( nn = prev_2
| ( ~ v__1(sortedList_first,nn,prev_2)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,prev_2,prev_2) ) )
| ~ v__1(null,prev_2,prev_2)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) ) ) )
| ( v__1(sortedList_first,X0,X0)
& ( v__1(sortedList_first,X0,nn)
| ( v__1(sortedList_first,X0,X0)
& ~ v__1(sortedList_first,nn,nn) ) ) )
| ( nn != X0
& v__1(sortedList_first,X0,nn)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) )
& ( v__1(sortedList_first,nn,X0)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,X0,X0) ) ) )
| ( nn != X0
& v__1(null,X0,X0)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) )
& ( v__1(sortedList_first,nn,X0)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,X0,X0) ) ) ) ) )
| ( ( ~ v__1(sortedList_first,X0,prev_2)
| ( ~ v__1(sortedList_first,prev_2,nn)
& ( ~ v__1(sortedList_first,prev_2,prev_2)
| v__1(sortedList_first,nn,nn) ) ) )
& ( nn = prev_2
| ( ~ v__1(sortedList_first,nn,prev_2)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,prev_2,prev_2) ) )
| ~ v__1(sortedList_first,X0,nn)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) ) )
& ( nn = prev_2
| ( ~ v__1(sortedList_first,nn,prev_2)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,prev_2,prev_2) ) )
| ~ v__1(null,X0,prev_2)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) ) ) )
| ( ( ! [X1] :
( ~ object(X1)
| ~ v__1(X1,X0,prev_2)
| X1 != node_next(nn) )
| ( ! [X2] :
( ~ object(X2)
| ~ v__1(X2,prev_2,nn)
| X2 != node_next(nn) )
& ( ! [X3] :
( ~ object(X3)
| ~ v__1(X3,prev_2,prev_2)
| X3 != node_next(nn) )
| ! [X4] :
( ~ object(X4)
| X4 != node_next(nn)
| v__1(X4,nn,nn) ) ) ) )
& ( nn = prev_2
| ( ! [X5] :
( ~ object(X5)
| ~ v__1(X5,nn,prev_2)
| X5 != node_next(nn) )
& ( ! [X6] :
( ~ object(X6)
| ~ v__1(X6,nn,nn)
| X6 != node_next(nn) )
| ! [X7] :
( ~ object(X7)
| X7 != node_next(nn)
| v__1(X7,prev_2,prev_2) ) ) )
| ! [X8] :
( ~ object(X8)
| ~ v__1(X8,X0,nn)
| X8 != node_next(nn) )
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) ) )
& ( nn = prev_2
| ( ! [X9] :
( ~ object(X9)
| ~ v__1(X9,nn,prev_2)
| X9 != node_next(nn) )
& ( ! [X10] :
( ~ object(X10)
| ~ v__1(X10,nn,nn)
| X10 != node_next(nn) )
| ! [X11] :
( ~ object(X11)
| X11 != node_next(nn)
| v__1(X11,prev_2,prev_2) ) ) )
| ~ v__1(null,X0,prev_2)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) ) )
& ( ( ( ! [X12] :
( ~ object(X12)
| ~ v__1(X12,X0,X0)
| X12 != node_next(nn) )
| ( ! [X13] :
( ~ object(X13)
| ~ v__1(X13,X0,nn)
| X13 != node_next(nn) )
& ( ! [X14] :
( ~ object(X14)
| ~ v__1(X14,X0,X0)
| X14 != node_next(nn) )
| ! [X15] :
( ~ object(X15)
| X15 != node_next(nn)
| v__1(X15,nn,nn) ) ) ) )
& ( nn = X0
| ( ! [X16] :
( ~ object(X16)
| ~ v__1(X16,nn,X0)
| X16 != node_next(nn) )
& ( ! [X17] :
( ~ object(X17)
| ~ v__1(X17,nn,nn)
| X17 != node_next(nn) )
| ! [X18] :
( ~ object(X18)
| X18 != node_next(nn)
| v__1(X18,X0,X0) ) ) )
| ! [X19] :
( ~ object(X19)
| ~ v__1(X19,X0,nn)
| X19 != node_next(nn) )
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) ) )
& ( nn = X0
| ( ! [X20] :
( ~ object(X20)
| ~ v__1(X20,nn,X0)
| X20 != node_next(nn) )
& ( ! [X21] :
( ~ object(X21)
| ~ v__1(X21,nn,nn)
| X21 != node_next(nn) )
| ! [X22] :
( ~ object(X22)
| X22 != node_next(nn)
| v__1(X22,X0,X0) ) ) )
| ~ v__1(null,X0,X0)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) ) ) )
| ( ! [X23] :
( ~ object(X23)
| X23 != node_next(nn)
| v__1(X23,prev_2,prev_2) )
& ( ! [X24] :
( ~ object(X24)
| X24 != node_next(nn)
| v__1(X24,prev_2,nn) )
| ( ! [X25] :
( ~ object(X25)
| X25 != node_next(nn)
| v__1(X25,prev_2,prev_2) )
& ! [X26] :
( ~ object(X26)
| ~ v__1(X26,nn,nn)
| X26 != node_next(nn) ) ) ) )
| ( nn != prev_2
& ! [X27] :
( ~ object(X27)
| X27 != node_next(nn)
| v__1(X27,prev_2,nn) )
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) )
& ( ! [X28] :
( ~ object(X28)
| X28 != node_next(nn)
| v__1(X28,nn,prev_2) )
| ( ! [X29] :
( ~ object(X29)
| X29 != node_next(nn)
| v__1(X29,nn,nn) )
& ! [X30] :
( ~ object(X30)
| ~ v__1(X30,prev_2,prev_2)
| X30 != node_next(nn) ) ) ) )
| ( nn != prev_2
& v__1(null,prev_2,prev_2)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) )
& ( ! [X31] :
( ~ object(X31)
| X31 != node_next(nn)
| v__1(X31,nn,prev_2) )
| ( ! [X32] :
( ~ object(X32)
| X32 != node_next(nn)
| v__1(X32,nn,nn) )
& ! [X33] :
( ~ object(X33)
| ~ v__1(X33,prev_2,prev_2)
| X33 != node_next(nn) ) ) ) ) ) ) )
& ( prev_2 = X0
| ( ( ~ v__1(sortedList_first,prev_2,X0)
| ( ~ v__1(sortedList_first,X0,nn)
& ( ~ v__1(sortedList_first,X0,X0)
| v__1(sortedList_first,nn,nn) ) ) )
& ( nn = X0
| ( ~ v__1(sortedList_first,nn,X0)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,X0,X0) ) )
| ~ v__1(sortedList_first,prev_2,nn)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) ) )
& ( nn = X0
| ( ~ v__1(sortedList_first,nn,X0)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,X0,X0) ) )
| ~ v__1(null,prev_2,X0)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) ) )
& ( ( ( ~ v__1(sortedList_first,prev_2,prev_2)
| ( ~ v__1(sortedList_first,prev_2,nn)
& ( ~ v__1(sortedList_first,prev_2,prev_2)
| v__1(sortedList_first,nn,nn) ) ) )
& ( nn = prev_2
| ( ~ v__1(sortedList_first,nn,prev_2)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,prev_2,prev_2) ) )
| ~ v__1(sortedList_first,prev_2,nn)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) ) )
& ( nn = prev_2
| ( ~ v__1(sortedList_first,nn,prev_2)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,prev_2,prev_2) ) )
| ~ v__1(null,prev_2,prev_2)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) ) ) )
| ( v__1(sortedList_first,X0,X0)
& ( v__1(sortedList_first,X0,nn)
| ( v__1(sortedList_first,X0,X0)
& ~ v__1(sortedList_first,nn,nn) ) ) )
| ( nn != X0
& v__1(sortedList_first,X0,nn)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) )
& ( v__1(sortedList_first,nn,X0)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,X0,X0) ) ) )
| ( nn != X0
& v__1(null,X0,X0)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) )
& ( v__1(sortedList_first,nn,X0)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,X0,X0) ) ) ) ) )
| ( ( ! [X34] :
( ~ object(X34)
| ~ v__1(X34,X0,X0)
| X34 != node_next(nn) )
| ( ! [X35] :
( ~ object(X35)
| ~ v__1(X35,X0,nn)
| X35 != node_next(nn) )
& ( ! [X36] :
( ~ object(X36)
| ~ v__1(X36,X0,X0)
| X36 != node_next(nn) )
| ! [X37] :
( ~ object(X37)
| X37 != node_next(nn)
| v__1(X37,nn,nn) ) ) ) )
& ( nn = X0
| ( ! [X38] :
( ~ object(X38)
| ~ v__1(X38,nn,X0)
| X38 != node_next(nn) )
& ( ! [X39] :
( ~ object(X39)
| ~ v__1(X39,nn,nn)
| X39 != node_next(nn) )
| ! [X40] :
( ~ object(X40)
| X40 != node_next(nn)
| v__1(X40,X0,X0) ) ) )
| ! [X41] :
( ~ object(X41)
| ~ v__1(X41,X0,nn)
| X41 != node_next(nn) )
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) ) )
& ( nn = X0
| ( ! [X42] :
( ~ object(X42)
| ~ v__1(X42,nn,X0)
| X42 != node_next(nn) )
& ( ! [X43] :
( ~ object(X43)
| ~ v__1(X43,nn,nn)
| X43 != node_next(nn) )
| ! [X44] :
( ~ object(X44)
| X44 != node_next(nn)
| v__1(X44,X0,X0) ) ) )
| ~ v__1(null,X0,X0)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) ) ) )
| ( ( ! [X45] :
( ~ object(X45)
| ~ v__1(X45,X0,prev_2)
| X45 != node_next(nn) )
| ( ! [X46] :
( ~ object(X46)
| ~ v__1(X46,prev_2,nn)
| X46 != node_next(nn) )
& ( ! [X47] :
( ~ object(X47)
| ~ v__1(X47,prev_2,prev_2)
| X47 != node_next(nn) )
| ! [X48] :
( ~ object(X48)
| X48 != node_next(nn)
| v__1(X48,nn,nn) ) ) ) )
& ( nn = prev_2
| ( ! [X49] :
( ~ object(X49)
| ~ v__1(X49,nn,prev_2)
| X49 != node_next(nn) )
& ( ! [X50] :
( ~ object(X50)
| ~ v__1(X50,nn,nn)
| X50 != node_next(nn) )
| ! [X51] :
( ~ object(X51)
| X51 != node_next(nn)
| v__1(X51,prev_2,prev_2) ) ) )
| ! [X52] :
( ~ object(X52)
| ~ v__1(X52,X0,nn)
| X52 != node_next(nn) )
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) ) )
& ( nn = prev_2
| ( ! [X53] :
( ~ object(X53)
| ~ v__1(X53,nn,prev_2)
| X53 != node_next(nn) )
& ( ! [X54] :
( ~ object(X54)
| ~ v__1(X54,nn,nn)
| X54 != node_next(nn) )
| ! [X55] :
( ~ object(X55)
| X55 != node_next(nn)
| v__1(X55,prev_2,prev_2) ) ) )
| ~ v__1(null,X0,prev_2)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) ) )
& ( ( ( ! [X56] :
( ~ object(X56)
| ~ v__1(X56,X0,X0)
| X56 != node_next(nn) )
| ( ! [X57] :
( ~ object(X57)
| ~ v__1(X57,X0,nn)
| X57 != node_next(nn) )
& ( ! [X58] :
( ~ object(X58)
| ~ v__1(X58,X0,X0)
| X58 != node_next(nn) )
| ! [X59] :
( ~ object(X59)
| X59 != node_next(nn)
| v__1(X59,nn,nn) ) ) ) )
& ( nn = X0
| ( ! [X60] :
( ~ object(X60)
| ~ v__1(X60,nn,X0)
| X60 != node_next(nn) )
& ( ! [X61] :
( ~ object(X61)
| ~ v__1(X61,nn,nn)
| X61 != node_next(nn) )
| ! [X62] :
( ~ object(X62)
| X62 != node_next(nn)
| v__1(X62,X0,X0) ) ) )
| ! [X63] :
( ~ object(X63)
| ~ v__1(X63,X0,nn)
| X63 != node_next(nn) )
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) ) )
& ( nn = X0
| ( ! [X64] :
( ~ object(X64)
| ~ v__1(X64,nn,X0)
| X64 != node_next(nn) )
& ( ! [X65] :
( ~ object(X65)
| ~ v__1(X65,nn,nn)
| X65 != node_next(nn) )
| ! [X66] :
( ~ object(X66)
| X66 != node_next(nn)
| v__1(X66,X0,X0) ) ) )
| ~ v__1(null,X0,X0)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) ) ) )
| ( ! [X67] :
( ~ object(X67)
| X67 != node_next(nn)
| v__1(X67,prev_2,prev_2) )
& ( ! [X68] :
( ~ object(X68)
| X68 != node_next(nn)
| v__1(X68,prev_2,nn) )
| ( ! [X69] :
( ~ object(X69)
| X69 != node_next(nn)
| v__1(X69,prev_2,prev_2) )
& ! [X70] :
( ~ object(X70)
| ~ v__1(X70,nn,nn)
| X70 != node_next(nn) ) ) ) )
| ( nn != prev_2
& ! [X71] :
( ~ object(X71)
| X71 != node_next(nn)
| v__1(X71,prev_2,nn) )
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) )
& ( ! [X72] :
( ~ object(X72)
| X72 != node_next(nn)
| v__1(X72,nn,prev_2) )
| ( ! [X73] :
( ~ object(X73)
| X73 != node_next(nn)
| v__1(X73,nn,nn) )
& ! [X74] :
( ~ object(X74)
| ~ v__1(X74,prev_2,prev_2)
| X74 != node_next(nn) ) ) ) )
| ( nn != prev_2
& v__1(null,prev_2,prev_2)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) )
& ( ! [X75] :
( ~ object(X75)
| X75 != node_next(nn)
| v__1(X75,nn,prev_2) )
| ( ! [X76] :
( ~ object(X76)
| X76 != node_next(nn)
| v__1(X76,nn,nn) )
& ! [X77] :
( ~ object(X77)
| ~ v__1(X77,prev_2,prev_2)
| X77 != node_next(nn) ) ) ) ) ) ) ) )
| ( X0 != null
& v__1(sortedList_first,X0,X0)
& X0 != nn ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f60,negated_conjecture,
~ ! [X0] :
( ~ object(X0)
| X0 = null
| ( ( ( ( ~ v__1(sortedList_first,X0,X0)
| ( ~ v__1(sortedList_first,X0,nn)
& ( ~ v__1(sortedList_first,X0,X0)
| v__1(sortedList_first,nn,nn) ) ) )
& ( nn = X0
| ( ~ v__1(sortedList_first,nn,X0)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,X0,X0) ) )
| ~ v__1(sortedList_first,X0,nn)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) ) )
& ( nn = X0
| ( ~ v__1(sortedList_first,nn,X0)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,X0,X0) ) )
| ~ v__1(null,X0,X0)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) ) ) )
| ( ( ~ v__1(sortedList_first,X0,prev_2)
| ( ~ v__1(sortedList_first,prev_2,nn)
& ( ~ v__1(sortedList_first,prev_2,prev_2)
| v__1(sortedList_first,nn,nn) ) ) )
& ( nn = prev_2
| ( ~ v__1(sortedList_first,nn,prev_2)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,prev_2,prev_2) ) )
| ~ v__1(sortedList_first,X0,nn)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) ) )
& ( nn = prev_2
| ( ~ v__1(sortedList_first,nn,prev_2)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,prev_2,prev_2) ) )
| ~ v__1(null,X0,prev_2)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) ) )
& ( ( ( ~ v__1(sortedList_first,X0,X0)
| ( ~ v__1(sortedList_first,X0,nn)
& ( ~ v__1(sortedList_first,X0,X0)
| v__1(sortedList_first,nn,nn) ) ) )
& ( nn = X0
| ( ~ v__1(sortedList_first,nn,X0)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,X0,X0) ) )
| ~ v__1(sortedList_first,X0,nn)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) ) )
& ( nn = X0
| ( ~ v__1(sortedList_first,nn,X0)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,X0,X0) ) )
| ~ v__1(null,X0,X0)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) ) ) )
| ( v__1(sortedList_first,prev_2,prev_2)
& ( v__1(sortedList_first,prev_2,nn)
| ( v__1(sortedList_first,prev_2,prev_2)
& ~ v__1(sortedList_first,nn,nn) ) ) )
| ( nn != prev_2
& v__1(sortedList_first,prev_2,nn)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) )
& ( v__1(sortedList_first,nn,prev_2)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,prev_2,prev_2) ) ) )
| ( nn != prev_2
& v__1(null,prev_2,prev_2)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) )
& ( v__1(sortedList_first,nn,prev_2)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,prev_2,prev_2) ) ) ) ) ) )
& ( prev_2 = X0
| ( ( ~ v__1(sortedList_first,prev_2,X0)
| ( ~ v__1(sortedList_first,X0,nn)
& ( ~ v__1(sortedList_first,X0,X0)
| v__1(sortedList_first,nn,nn) ) ) )
& ( nn = X0
| ( ~ v__1(sortedList_first,nn,X0)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,X0,X0) ) )
| ~ v__1(sortedList_first,prev_2,nn)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) ) )
& ( nn = X0
| ( ~ v__1(sortedList_first,nn,X0)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,X0,X0) ) )
| ~ v__1(null,prev_2,X0)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) ) )
& ( ( ( ~ v__1(sortedList_first,prev_2,prev_2)
| ( ~ v__1(sortedList_first,prev_2,nn)
& ( ~ v__1(sortedList_first,prev_2,prev_2)
| v__1(sortedList_first,nn,nn) ) ) )
& ( nn = prev_2
| ( ~ v__1(sortedList_first,nn,prev_2)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,prev_2,prev_2) ) )
| ~ v__1(sortedList_first,prev_2,nn)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) ) )
& ( nn = prev_2
| ( ~ v__1(sortedList_first,nn,prev_2)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,prev_2,prev_2) ) )
| ~ v__1(null,prev_2,prev_2)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) ) ) )
| ( v__1(sortedList_first,X0,X0)
& ( v__1(sortedList_first,X0,nn)
| ( v__1(sortedList_first,X0,X0)
& ~ v__1(sortedList_first,nn,nn) ) ) )
| ( nn != X0
& v__1(sortedList_first,X0,nn)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) )
& ( v__1(sortedList_first,nn,X0)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,X0,X0) ) ) )
| ( nn != X0
& v__1(null,X0,X0)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) )
& ( v__1(sortedList_first,nn,X0)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,X0,X0) ) ) ) ) )
| ( ( ~ v__1(sortedList_first,X0,prev_2)
| ( ~ v__1(sortedList_first,prev_2,nn)
& ( ~ v__1(sortedList_first,prev_2,prev_2)
| v__1(sortedList_first,nn,nn) ) ) )
& ( nn = prev_2
| ( ~ v__1(sortedList_first,nn,prev_2)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,prev_2,prev_2) ) )
| ~ v__1(sortedList_first,X0,nn)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) ) )
& ( nn = prev_2
| ( ~ v__1(sortedList_first,nn,prev_2)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,prev_2,prev_2) ) )
| ~ v__1(null,X0,prev_2)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) ) ) )
| ( ( ! [X1] :
( ~ object(X1)
| ~ v__1(X1,X0,prev_2)
| X1 != node_next(nn) )
| ( ! [X2] :
( ~ object(X2)
| ~ v__1(X2,prev_2,nn)
| X2 != node_next(nn) )
& ( ! [X3] :
( ~ object(X3)
| ~ v__1(X3,prev_2,prev_2)
| X3 != node_next(nn) )
| ! [X4] :
( ~ object(X4)
| X4 != node_next(nn)
| v__1(X4,nn,nn) ) ) ) )
& ( nn = prev_2
| ( ! [X5] :
( ~ object(X5)
| ~ v__1(X5,nn,prev_2)
| X5 != node_next(nn) )
& ( ! [X6] :
( ~ object(X6)
| ~ v__1(X6,nn,nn)
| X6 != node_next(nn) )
| ! [X7] :
( ~ object(X7)
| X7 != node_next(nn)
| v__1(X7,prev_2,prev_2) ) ) )
| ! [X8] :
( ~ object(X8)
| ~ v__1(X8,X0,nn)
| X8 != node_next(nn) )
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) ) )
& ( nn = prev_2
| ( ! [X9] :
( ~ object(X9)
| ~ v__1(X9,nn,prev_2)
| X9 != node_next(nn) )
& ( ! [X10] :
( ~ object(X10)
| ~ v__1(X10,nn,nn)
| X10 != node_next(nn) )
| ! [X11] :
( ~ object(X11)
| X11 != node_next(nn)
| v__1(X11,prev_2,prev_2) ) ) )
| ~ v__1(null,X0,prev_2)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) ) )
& ( ( ( ! [X12] :
( ~ object(X12)
| ~ v__1(X12,X0,X0)
| X12 != node_next(nn) )
| ( ! [X13] :
( ~ object(X13)
| ~ v__1(X13,X0,nn)
| X13 != node_next(nn) )
& ( ! [X14] :
( ~ object(X14)
| ~ v__1(X14,X0,X0)
| X14 != node_next(nn) )
| ! [X15] :
( ~ object(X15)
| X15 != node_next(nn)
| v__1(X15,nn,nn) ) ) ) )
& ( nn = X0
| ( ! [X16] :
( ~ object(X16)
| ~ v__1(X16,nn,X0)
| X16 != node_next(nn) )
& ( ! [X17] :
( ~ object(X17)
| ~ v__1(X17,nn,nn)
| X17 != node_next(nn) )
| ! [X18] :
( ~ object(X18)
| X18 != node_next(nn)
| v__1(X18,X0,X0) ) ) )
| ! [X19] :
( ~ object(X19)
| ~ v__1(X19,X0,nn)
| X19 != node_next(nn) )
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) ) )
& ( nn = X0
| ( ! [X20] :
( ~ object(X20)
| ~ v__1(X20,nn,X0)
| X20 != node_next(nn) )
& ( ! [X21] :
( ~ object(X21)
| ~ v__1(X21,nn,nn)
| X21 != node_next(nn) )
| ! [X22] :
( ~ object(X22)
| X22 != node_next(nn)
| v__1(X22,X0,X0) ) ) )
| ~ v__1(null,X0,X0)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) ) ) )
| ( ! [X23] :
( ~ object(X23)
| X23 != node_next(nn)
| v__1(X23,prev_2,prev_2) )
& ( ! [X24] :
( ~ object(X24)
| X24 != node_next(nn)
| v__1(X24,prev_2,nn) )
| ( ! [X25] :
( ~ object(X25)
| X25 != node_next(nn)
| v__1(X25,prev_2,prev_2) )
& ! [X26] :
( ~ object(X26)
| ~ v__1(X26,nn,nn)
| X26 != node_next(nn) ) ) ) )
| ( nn != prev_2
& ! [X27] :
( ~ object(X27)
| X27 != node_next(nn)
| v__1(X27,prev_2,nn) )
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) )
& ( ! [X28] :
( ~ object(X28)
| X28 != node_next(nn)
| v__1(X28,nn,prev_2) )
| ( ! [X29] :
( ~ object(X29)
| X29 != node_next(nn)
| v__1(X29,nn,nn) )
& ! [X30] :
( ~ object(X30)
| ~ v__1(X30,prev_2,prev_2)
| X30 != node_next(nn) ) ) ) )
| ( nn != prev_2
& v__1(null,prev_2,prev_2)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) )
& ( ! [X31] :
( ~ object(X31)
| X31 != node_next(nn)
| v__1(X31,nn,prev_2) )
| ( ! [X32] :
( ~ object(X32)
| X32 != node_next(nn)
| v__1(X32,nn,nn) )
& ! [X33] :
( ~ object(X33)
| ~ v__1(X33,prev_2,prev_2)
| X33 != node_next(nn) ) ) ) ) ) ) )
& ( prev_2 = X0
| ( ( ~ v__1(sortedList_first,prev_2,X0)
| ( ~ v__1(sortedList_first,X0,nn)
& ( ~ v__1(sortedList_first,X0,X0)
| v__1(sortedList_first,nn,nn) ) ) )
& ( nn = X0
| ( ~ v__1(sortedList_first,nn,X0)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,X0,X0) ) )
| ~ v__1(sortedList_first,prev_2,nn)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) ) )
& ( nn = X0
| ( ~ v__1(sortedList_first,nn,X0)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,X0,X0) ) )
| ~ v__1(null,prev_2,X0)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) ) )
& ( ( ( ~ v__1(sortedList_first,prev_2,prev_2)
| ( ~ v__1(sortedList_first,prev_2,nn)
& ( ~ v__1(sortedList_first,prev_2,prev_2)
| v__1(sortedList_first,nn,nn) ) ) )
& ( nn = prev_2
| ( ~ v__1(sortedList_first,nn,prev_2)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,prev_2,prev_2) ) )
| ~ v__1(sortedList_first,prev_2,nn)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) ) )
& ( nn = prev_2
| ( ~ v__1(sortedList_first,nn,prev_2)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,prev_2,prev_2) ) )
| ~ v__1(null,prev_2,prev_2)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) ) ) )
| ( v__1(sortedList_first,X0,X0)
& ( v__1(sortedList_first,X0,nn)
| ( v__1(sortedList_first,X0,X0)
& ~ v__1(sortedList_first,nn,nn) ) ) )
| ( nn != X0
& v__1(sortedList_first,X0,nn)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) )
& ( v__1(sortedList_first,nn,X0)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,X0,X0) ) ) )
| ( nn != X0
& v__1(null,X0,X0)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) )
& ( v__1(sortedList_first,nn,X0)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,X0,X0) ) ) ) ) )
| ( ( ! [X34] :
( ~ object(X34)
| ~ v__1(X34,X0,X0)
| X34 != node_next(nn) )
| ( ! [X35] :
( ~ object(X35)
| ~ v__1(X35,X0,nn)
| X35 != node_next(nn) )
& ( ! [X36] :
( ~ object(X36)
| ~ v__1(X36,X0,X0)
| X36 != node_next(nn) )
| ! [X37] :
( ~ object(X37)
| X37 != node_next(nn)
| v__1(X37,nn,nn) ) ) ) )
& ( nn = X0
| ( ! [X38] :
( ~ object(X38)
| ~ v__1(X38,nn,X0)
| X38 != node_next(nn) )
& ( ! [X39] :
( ~ object(X39)
| ~ v__1(X39,nn,nn)
| X39 != node_next(nn) )
| ! [X40] :
( ~ object(X40)
| X40 != node_next(nn)
| v__1(X40,X0,X0) ) ) )
| ! [X41] :
( ~ object(X41)
| ~ v__1(X41,X0,nn)
| X41 != node_next(nn) )
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) ) )
& ( nn = X0
| ( ! [X42] :
( ~ object(X42)
| ~ v__1(X42,nn,X0)
| X42 != node_next(nn) )
& ( ! [X43] :
( ~ object(X43)
| ~ v__1(X43,nn,nn)
| X43 != node_next(nn) )
| ! [X44] :
( ~ object(X44)
| X44 != node_next(nn)
| v__1(X44,X0,X0) ) ) )
| ~ v__1(null,X0,X0)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) ) ) )
| ( ( ! [X45] :
( ~ object(X45)
| ~ v__1(X45,X0,prev_2)
| X45 != node_next(nn) )
| ( ! [X46] :
( ~ object(X46)
| ~ v__1(X46,prev_2,nn)
| X46 != node_next(nn) )
& ( ! [X47] :
( ~ object(X47)
| ~ v__1(X47,prev_2,prev_2)
| X47 != node_next(nn) )
| ! [X48] :
( ~ object(X48)
| X48 != node_next(nn)
| v__1(X48,nn,nn) ) ) ) )
& ( nn = prev_2
| ( ! [X49] :
( ~ object(X49)
| ~ v__1(X49,nn,prev_2)
| X49 != node_next(nn) )
& ( ! [X50] :
( ~ object(X50)
| ~ v__1(X50,nn,nn)
| X50 != node_next(nn) )
| ! [X51] :
( ~ object(X51)
| X51 != node_next(nn)
| v__1(X51,prev_2,prev_2) ) ) )
| ! [X52] :
( ~ object(X52)
| ~ v__1(X52,X0,nn)
| X52 != node_next(nn) )
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) ) )
& ( nn = prev_2
| ( ! [X53] :
( ~ object(X53)
| ~ v__1(X53,nn,prev_2)
| X53 != node_next(nn) )
& ( ! [X54] :
( ~ object(X54)
| ~ v__1(X54,nn,nn)
| X54 != node_next(nn) )
| ! [X55] :
( ~ object(X55)
| X55 != node_next(nn)
| v__1(X55,prev_2,prev_2) ) ) )
| ~ v__1(null,X0,prev_2)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) ) )
& ( ( ( ! [X56] :
( ~ object(X56)
| ~ v__1(X56,X0,X0)
| X56 != node_next(nn) )
| ( ! [X57] :
( ~ object(X57)
| ~ v__1(X57,X0,nn)
| X57 != node_next(nn) )
& ( ! [X58] :
( ~ object(X58)
| ~ v__1(X58,X0,X0)
| X58 != node_next(nn) )
| ! [X59] :
( ~ object(X59)
| X59 != node_next(nn)
| v__1(X59,nn,nn) ) ) ) )
& ( nn = X0
| ( ! [X60] :
( ~ object(X60)
| ~ v__1(X60,nn,X0)
| X60 != node_next(nn) )
& ( ! [X61] :
( ~ object(X61)
| ~ v__1(X61,nn,nn)
| X61 != node_next(nn) )
| ! [X62] :
( ~ object(X62)
| X62 != node_next(nn)
| v__1(X62,X0,X0) ) ) )
| ! [X63] :
( ~ object(X63)
| ~ v__1(X63,X0,nn)
| X63 != node_next(nn) )
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) ) )
& ( nn = X0
| ( ! [X64] :
( ~ object(X64)
| ~ v__1(X64,nn,X0)
| X64 != node_next(nn) )
& ( ! [X65] :
( ~ object(X65)
| ~ v__1(X65,nn,nn)
| X65 != node_next(nn) )
| ! [X66] :
( ~ object(X66)
| X66 != node_next(nn)
| v__1(X66,X0,X0) ) ) )
| ~ v__1(null,X0,X0)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) ) ) )
| ( ! [X67] :
( ~ object(X67)
| X67 != node_next(nn)
| v__1(X67,prev_2,prev_2) )
& ( ! [X68] :
( ~ object(X68)
| X68 != node_next(nn)
| v__1(X68,prev_2,nn) )
| ( ! [X69] :
( ~ object(X69)
| X69 != node_next(nn)
| v__1(X69,prev_2,prev_2) )
& ! [X70] :
( ~ object(X70)
| ~ v__1(X70,nn,nn)
| X70 != node_next(nn) ) ) ) )
| ( nn != prev_2
& ! [X71] :
( ~ object(X71)
| X71 != node_next(nn)
| v__1(X71,prev_2,nn) )
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) )
& ( ! [X72] :
( ~ object(X72)
| X72 != node_next(nn)
| v__1(X72,nn,prev_2) )
| ( ! [X73] :
( ~ object(X73)
| X73 != node_next(nn)
| v__1(X73,nn,nn) )
& ! [X74] :
( ~ object(X74)
| ~ v__1(X74,prev_2,prev_2)
| X74 != node_next(nn) ) ) ) )
| ( nn != prev_2
& v__1(null,prev_2,prev_2)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) )
& ( ! [X75] :
( ~ object(X75)
| X75 != node_next(nn)
| v__1(X75,nn,prev_2) )
| ( ! [X76] :
( ~ object(X76)
| X76 != node_next(nn)
| v__1(X76,nn,nn) )
& ! [X77] :
( ~ object(X77)
| ~ v__1(X77,prev_2,prev_2)
| X77 != node_next(nn) ) ) ) ) ) ) ) )
| ( X0 != null
& v__1(sortedList_first,X0,X0)
& X0 != nn ) ),
inference(negated_conjecture,[status(cth)],[f59]) ).
fof(f61,plain,
! [X0,X1,X2] :
( ~ object(X0)
| ~ object(X1)
| ~ object(X2)
| ~ v__1(X0,X1,X1)
| ~ v__1(X1,X2,X2)
| v__1(X0,X2,X2) ),
inference(ennf_transformation,[],[f16]) ).
fof(f62,plain,
! [X0,X1,X2] :
( ~ object(X0)
| ~ object(X1)
| ~ object(X2)
| ~ v__1(X0,X1,X1)
| ~ v__1(X1,X2,X2)
| v__1(X0,X2,X2) ),
inference(flattening,[],[f61]) ).
fof(f67,plain,
! [X0,X1,X2] :
( ~ object(X0)
| ~ object(X1)
| ~ object(X2)
| ~ v__1(X0,X1,X1)
| ~ v__1(X0,X2,X2)
| v__1(X0,X1,X2)
| v__1(X0,X2,X1) ),
inference(ennf_transformation,[],[f19]) ).
fof(f68,plain,
! [X0,X1,X2] :
( ~ object(X0)
| ~ object(X1)
| ~ object(X2)
| ~ v__1(X0,X1,X1)
| ~ v__1(X0,X2,X2)
| v__1(X0,X1,X2)
| v__1(X0,X2,X1) ),
inference(flattening,[],[f67]) ).
fof(f69,plain,
! [X0,X1,X2] :
( ~ object(X0)
| ~ object(X1)
| ~ object(X2)
| ~ v__1(X0,X1,X2)
| ( v__1(X0,X1,X1)
& v__1(X1,X2,X2) ) ),
inference(ennf_transformation,[],[f20]) ).
fof(f70,plain,
! [X0,X1,X2] :
( ~ object(X0)
| ~ object(X1)
| ~ object(X2)
| ~ v__1(X0,X1,X2)
| ( v__1(X0,X1,X1)
& v__1(X1,X2,X2) ) ),
inference(flattening,[],[f69]) ).
fof(f73,plain,
! [X0,X1] :
( ~ object(X0)
| ~ object(X1)
| X0 != node_next(X0)
| ~ v__1(X0,X1,X1)
| X0 = X1 ),
inference(ennf_transformation,[],[f23]) ).
fof(f74,plain,
! [X0,X1] :
( ~ object(X0)
| ~ object(X1)
| X0 != node_next(X0)
| ~ v__1(X0,X1,X1)
| X0 = X1 ),
inference(flattening,[],[f73]) ).
fof(f79,plain,
! [X0,X1] :
( ~ object(X0)
| ~ object(X1)
| ~ v__1(sortedList_first,X0,X0)
| X0 = null
| ! [X2] :
( ~ object(X2)
| ~ v__1(X2,X1,X1)
| X2 != node_next(X0) )
| X1 = null
| ( ! [X3,X4] :
( ~ integer(X3)
| ~ integer(X4)
| X3 != node_key(X0)
| X4 != node_key(X1)
| lteq(X3,X4) )
& ! [X5] :
( ~ integer(X5)
| X5 != node_key(X0)
| X5 != node_key(X1) ) ) ),
inference(ennf_transformation,[],[f44]) ).
fof(f80,plain,
! [X0,X1] :
( ~ object(X0)
| ~ object(X1)
| ~ v__1(sortedList_first,X0,X0)
| X0 = null
| ! [X2] :
( ~ object(X2)
| ~ v__1(X2,X1,X1)
| X2 != node_next(X0) )
| X1 = null
| ( ! [X3,X4] :
( ~ integer(X3)
| ~ integer(X4)
| X3 != node_key(X0)
| X4 != node_key(X1)
| lteq(X3,X4) )
& ! [X5] :
( ~ integer(X5)
| X5 != node_key(X0)
| X5 != node_key(X1) ) ) ),
inference(flattening,[],[f79]) ).
fof(f81,plain,
! [X0,X1] :
( ~ object(X0)
| ~ object(X1)
| X0 = null
| X1 = null
| X1 != node_next(X0)
| ( X1 != null
& v__1(sortedList_first,X1,X1) ) ),
inference(ennf_transformation,[],[f45]) ).
fof(f82,plain,
! [X0,X1] :
( ~ object(X0)
| ~ object(X1)
| X0 = null
| X1 = null
| X1 != node_next(X0)
| ( X1 != null
& v__1(sortedList_first,X1,X1) ) ),
inference(flattening,[],[f81]) ).
fof(f85,plain,
? [X0] :
( object(X0)
& null != X0
& ( ( ( ( v__1(sortedList_first,X0,X0)
& ( v__1(sortedList_first,X0,nn)
| ( v__1(sortedList_first,X0,X0)
& ~ v__1(sortedList_first,nn,nn) ) ) )
| ( nn != X0
& ( v__1(sortedList_first,nn,X0)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,X0,X0) ) )
& v__1(sortedList_first,X0,nn)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ( nn != X0
& ( v__1(sortedList_first,nn,X0)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,X0,X0) ) )
& v__1(null,X0,X0)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) ) )
& ( ( v__1(sortedList_first,X0,prev_2)
& ( v__1(sortedList_first,prev_2,nn)
| ( v__1(sortedList_first,prev_2,prev_2)
& ~ v__1(sortedList_first,nn,nn) ) ) )
| ( nn != prev_2
& ( v__1(sortedList_first,nn,prev_2)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,prev_2,prev_2) ) )
& v__1(sortedList_first,X0,nn)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ( nn != prev_2
& ( v__1(sortedList_first,nn,prev_2)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,prev_2,prev_2) ) )
& v__1(null,X0,prev_2)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ( ( ( v__1(sortedList_first,X0,X0)
& ( v__1(sortedList_first,X0,nn)
| ( v__1(sortedList_first,X0,X0)
& ~ v__1(sortedList_first,nn,nn) ) ) )
| ( nn != X0
& ( v__1(sortedList_first,nn,X0)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,X0,X0) ) )
& v__1(sortedList_first,X0,nn)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ( nn != X0
& ( v__1(sortedList_first,nn,X0)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,X0,X0) ) )
& v__1(null,X0,X0)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) ) )
& ( ~ v__1(sortedList_first,prev_2,prev_2)
| ( ~ v__1(sortedList_first,prev_2,nn)
& ( ~ v__1(sortedList_first,prev_2,prev_2)
| v__1(sortedList_first,nn,nn) ) ) )
& ( nn = prev_2
| ~ v__1(sortedList_first,prev_2,nn)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) )
| ( ~ v__1(sortedList_first,nn,prev_2)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,prev_2,prev_2) ) ) )
& ( nn = prev_2
| ~ v__1(null,prev_2,prev_2)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) )
| ( ~ v__1(sortedList_first,nn,prev_2)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,prev_2,prev_2) ) ) ) ) ) )
| ( prev_2 != X0
& ( ( v__1(sortedList_first,prev_2,X0)
& ( v__1(sortedList_first,X0,nn)
| ( v__1(sortedList_first,X0,X0)
& ~ v__1(sortedList_first,nn,nn) ) ) )
| ( nn != X0
& ( v__1(sortedList_first,nn,X0)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,X0,X0) ) )
& v__1(sortedList_first,prev_2,nn)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ( nn != X0
& ( v__1(sortedList_first,nn,X0)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,X0,X0) ) )
& v__1(null,prev_2,X0)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ( ( ( v__1(sortedList_first,prev_2,prev_2)
& ( v__1(sortedList_first,prev_2,nn)
| ( v__1(sortedList_first,prev_2,prev_2)
& ~ v__1(sortedList_first,nn,nn) ) ) )
| ( nn != prev_2
& ( v__1(sortedList_first,nn,prev_2)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,prev_2,prev_2) ) )
& v__1(sortedList_first,prev_2,nn)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ( nn != prev_2
& ( v__1(sortedList_first,nn,prev_2)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,prev_2,prev_2) ) )
& v__1(null,prev_2,prev_2)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) ) )
& ( ~ v__1(sortedList_first,X0,X0)
| ( ~ v__1(sortedList_first,X0,nn)
& ( ~ v__1(sortedList_first,X0,X0)
| v__1(sortedList_first,nn,nn) ) ) )
& ( nn = X0
| ~ v__1(sortedList_first,X0,nn)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) )
| ( ~ v__1(sortedList_first,nn,X0)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,X0,X0) ) ) )
& ( nn = X0
| ~ v__1(null,X0,X0)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) )
| ( ~ v__1(sortedList_first,nn,X0)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,X0,X0) ) ) ) ) )
& ( ( v__1(sortedList_first,X0,prev_2)
& ( v__1(sortedList_first,prev_2,nn)
| ( v__1(sortedList_first,prev_2,prev_2)
& ~ v__1(sortedList_first,nn,nn) ) ) )
| ( nn != prev_2
& ( v__1(sortedList_first,nn,prev_2)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,prev_2,prev_2) ) )
& v__1(sortedList_first,X0,nn)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ( nn != prev_2
& ( v__1(sortedList_first,nn,prev_2)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,prev_2,prev_2) ) )
& v__1(null,X0,prev_2)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) ) )
& ( ( ? [X1] :
( object(X1)
& v__1(X1,X0,prev_2)
& node_next(nn) = X1 )
& ( ? [X2] :
( object(X2)
& v__1(X2,prev_2,nn)
& node_next(nn) = X2 )
| ( ? [X3] :
( object(X3)
& v__1(X3,prev_2,prev_2)
& node_next(nn) = X3 )
& ? [X4] :
( object(X4)
& node_next(nn) = X4
& ~ v__1(X4,nn,nn) ) ) ) )
| ( nn != prev_2
& ( ? [X5] :
( object(X5)
& v__1(X5,nn,prev_2)
& node_next(nn) = X5 )
| ( ? [X6] :
( object(X6)
& v__1(X6,nn,nn)
& node_next(nn) = X6 )
& ? [X7] :
( object(X7)
& node_next(nn) = X7
& ~ v__1(X7,prev_2,prev_2) ) ) )
& ? [X8] :
( object(X8)
& v__1(X8,X0,nn)
& node_next(nn) = X8 )
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ( nn != prev_2
& ( ? [X9] :
( object(X9)
& v__1(X9,nn,prev_2)
& node_next(nn) = X9 )
| ( ? [X10] :
( object(X10)
& v__1(X10,nn,nn)
& node_next(nn) = X10 )
& ? [X11] :
( object(X11)
& node_next(nn) = X11
& ~ v__1(X11,prev_2,prev_2) ) ) )
& v__1(null,X0,prev_2)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ( ( ( ? [X12] :
( object(X12)
& v__1(X12,X0,X0)
& node_next(nn) = X12 )
& ( ? [X13] :
( object(X13)
& v__1(X13,X0,nn)
& node_next(nn) = X13 )
| ( ? [X14] :
( object(X14)
& v__1(X14,X0,X0)
& node_next(nn) = X14 )
& ? [X15] :
( object(X15)
& node_next(nn) = X15
& ~ v__1(X15,nn,nn) ) ) ) )
| ( nn != X0
& ( ? [X16] :
( object(X16)
& v__1(X16,nn,X0)
& node_next(nn) = X16 )
| ( ? [X17] :
( object(X17)
& v__1(X17,nn,nn)
& node_next(nn) = X17 )
& ? [X18] :
( object(X18)
& node_next(nn) = X18
& ~ v__1(X18,X0,X0) ) ) )
& ? [X19] :
( object(X19)
& v__1(X19,X0,nn)
& node_next(nn) = X19 )
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ( nn != X0
& ( ? [X20] :
( object(X20)
& v__1(X20,nn,X0)
& node_next(nn) = X20 )
| ( ? [X21] :
( object(X21)
& v__1(X21,nn,nn)
& node_next(nn) = X21 )
& ? [X22] :
( object(X22)
& node_next(nn) = X22
& ~ v__1(X22,X0,X0) ) ) )
& v__1(null,X0,X0)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) ) )
& ( ? [X23] :
( object(X23)
& node_next(nn) = X23
& ~ v__1(X23,prev_2,prev_2) )
| ( ? [X24] :
( object(X24)
& node_next(nn) = X24
& ~ v__1(X24,prev_2,nn) )
& ( ? [X25] :
( object(X25)
& node_next(nn) = X25
& ~ v__1(X25,prev_2,prev_2) )
| ? [X26] :
( object(X26)
& v__1(X26,nn,nn)
& node_next(nn) = X26 ) ) ) )
& ( nn = prev_2
| ? [X27] :
( object(X27)
& node_next(nn) = X27
& ~ v__1(X27,prev_2,nn) )
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) )
| ( ? [X28] :
( object(X28)
& node_next(nn) = X28
& ~ v__1(X28,nn,prev_2) )
& ( ? [X29] :
( object(X29)
& node_next(nn) = X29
& ~ v__1(X29,nn,nn) )
| ? [X30] :
( object(X30)
& v__1(X30,prev_2,prev_2)
& node_next(nn) = X30 ) ) ) )
& ( nn = prev_2
| ~ v__1(null,prev_2,prev_2)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) )
| ( ? [X31] :
( object(X31)
& node_next(nn) = X31
& ~ v__1(X31,nn,prev_2) )
& ( ? [X32] :
( object(X32)
& node_next(nn) = X32
& ~ v__1(X32,nn,nn) )
| ? [X33] :
( object(X33)
& v__1(X33,prev_2,prev_2)
& node_next(nn) = X33 ) ) ) ) ) ) )
| ( prev_2 != X0
& ( ( v__1(sortedList_first,prev_2,X0)
& ( v__1(sortedList_first,X0,nn)
| ( v__1(sortedList_first,X0,X0)
& ~ v__1(sortedList_first,nn,nn) ) ) )
| ( nn != X0
& ( v__1(sortedList_first,nn,X0)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,X0,X0) ) )
& v__1(sortedList_first,prev_2,nn)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ( nn != X0
& ( v__1(sortedList_first,nn,X0)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,X0,X0) ) )
& v__1(null,prev_2,X0)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ( ( ( v__1(sortedList_first,prev_2,prev_2)
& ( v__1(sortedList_first,prev_2,nn)
| ( v__1(sortedList_first,prev_2,prev_2)
& ~ v__1(sortedList_first,nn,nn) ) ) )
| ( nn != prev_2
& ( v__1(sortedList_first,nn,prev_2)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,prev_2,prev_2) ) )
& v__1(sortedList_first,prev_2,nn)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ( nn != prev_2
& ( v__1(sortedList_first,nn,prev_2)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,prev_2,prev_2) ) )
& v__1(null,prev_2,prev_2)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) ) )
& ( ~ v__1(sortedList_first,X0,X0)
| ( ~ v__1(sortedList_first,X0,nn)
& ( ~ v__1(sortedList_first,X0,X0)
| v__1(sortedList_first,nn,nn) ) ) )
& ( nn = X0
| ~ v__1(sortedList_first,X0,nn)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) )
| ( ~ v__1(sortedList_first,nn,X0)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,X0,X0) ) ) )
& ( nn = X0
| ~ v__1(null,X0,X0)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) )
| ( ~ v__1(sortedList_first,nn,X0)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,X0,X0) ) ) ) ) )
& ( ( ? [X34] :
( object(X34)
& v__1(X34,X0,X0)
& node_next(nn) = X34 )
& ( ? [X35] :
( object(X35)
& v__1(X35,X0,nn)
& node_next(nn) = X35 )
| ( ? [X36] :
( object(X36)
& v__1(X36,X0,X0)
& node_next(nn) = X36 )
& ? [X37] :
( object(X37)
& node_next(nn) = X37
& ~ v__1(X37,nn,nn) ) ) ) )
| ( nn != X0
& ( ? [X38] :
( object(X38)
& v__1(X38,nn,X0)
& node_next(nn) = X38 )
| ( ? [X39] :
( object(X39)
& v__1(X39,nn,nn)
& node_next(nn) = X39 )
& ? [X40] :
( object(X40)
& node_next(nn) = X40
& ~ v__1(X40,X0,X0) ) ) )
& ? [X41] :
( object(X41)
& v__1(X41,X0,nn)
& node_next(nn) = X41 )
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ( nn != X0
& ( ? [X42] :
( object(X42)
& v__1(X42,nn,X0)
& node_next(nn) = X42 )
| ( ? [X43] :
( object(X43)
& v__1(X43,nn,nn)
& node_next(nn) = X43 )
& ? [X44] :
( object(X44)
& node_next(nn) = X44
& ~ v__1(X44,X0,X0) ) ) )
& v__1(null,X0,X0)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) ) )
& ( ( ? [X45] :
( object(X45)
& v__1(X45,X0,prev_2)
& node_next(nn) = X45 )
& ( ? [X46] :
( object(X46)
& v__1(X46,prev_2,nn)
& node_next(nn) = X46 )
| ( ? [X47] :
( object(X47)
& v__1(X47,prev_2,prev_2)
& node_next(nn) = X47 )
& ? [X48] :
( object(X48)
& node_next(nn) = X48
& ~ v__1(X48,nn,nn) ) ) ) )
| ( nn != prev_2
& ( ? [X49] :
( object(X49)
& v__1(X49,nn,prev_2)
& node_next(nn) = X49 )
| ( ? [X50] :
( object(X50)
& v__1(X50,nn,nn)
& node_next(nn) = X50 )
& ? [X51] :
( object(X51)
& node_next(nn) = X51
& ~ v__1(X51,prev_2,prev_2) ) ) )
& ? [X52] :
( object(X52)
& v__1(X52,X0,nn)
& node_next(nn) = X52 )
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ( nn != prev_2
& ( ? [X53] :
( object(X53)
& v__1(X53,nn,prev_2)
& node_next(nn) = X53 )
| ( ? [X54] :
( object(X54)
& v__1(X54,nn,nn)
& node_next(nn) = X54 )
& ? [X55] :
( object(X55)
& node_next(nn) = X55
& ~ v__1(X55,prev_2,prev_2) ) ) )
& v__1(null,X0,prev_2)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ( ( ( ? [X56] :
( object(X56)
& v__1(X56,X0,X0)
& node_next(nn) = X56 )
& ( ? [X57] :
( object(X57)
& v__1(X57,X0,nn)
& node_next(nn) = X57 )
| ( ? [X58] :
( object(X58)
& v__1(X58,X0,X0)
& node_next(nn) = X58 )
& ? [X59] :
( object(X59)
& node_next(nn) = X59
& ~ v__1(X59,nn,nn) ) ) ) )
| ( nn != X0
& ( ? [X60] :
( object(X60)
& v__1(X60,nn,X0)
& node_next(nn) = X60 )
| ( ? [X61] :
( object(X61)
& v__1(X61,nn,nn)
& node_next(nn) = X61 )
& ? [X62] :
( object(X62)
& node_next(nn) = X62
& ~ v__1(X62,X0,X0) ) ) )
& ? [X63] :
( object(X63)
& v__1(X63,X0,nn)
& node_next(nn) = X63 )
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ( nn != X0
& ( ? [X64] :
( object(X64)
& v__1(X64,nn,X0)
& node_next(nn) = X64 )
| ( ? [X65] :
( object(X65)
& v__1(X65,nn,nn)
& node_next(nn) = X65 )
& ? [X66] :
( object(X66)
& node_next(nn) = X66
& ~ v__1(X66,X0,X0) ) ) )
& v__1(null,X0,X0)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) ) )
& ( ? [X67] :
( object(X67)
& node_next(nn) = X67
& ~ v__1(X67,prev_2,prev_2) )
| ( ? [X68] :
( object(X68)
& node_next(nn) = X68
& ~ v__1(X68,prev_2,nn) )
& ( ? [X69] :
( object(X69)
& node_next(nn) = X69
& ~ v__1(X69,prev_2,prev_2) )
| ? [X70] :
( object(X70)
& v__1(X70,nn,nn)
& node_next(nn) = X70 ) ) ) )
& ( nn = prev_2
| ? [X71] :
( object(X71)
& node_next(nn) = X71
& ~ v__1(X71,prev_2,nn) )
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) )
| ( ? [X72] :
( object(X72)
& node_next(nn) = X72
& ~ v__1(X72,nn,prev_2) )
& ( ? [X73] :
( object(X73)
& node_next(nn) = X73
& ~ v__1(X73,nn,nn) )
| ? [X74] :
( object(X74)
& v__1(X74,prev_2,prev_2)
& node_next(nn) = X74 ) ) ) )
& ( nn = prev_2
| ~ v__1(null,prev_2,prev_2)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) )
| ( ? [X75] :
( object(X75)
& node_next(nn) = X75
& ~ v__1(X75,nn,prev_2) )
& ( ? [X76] :
( object(X76)
& node_next(nn) = X76
& ~ v__1(X76,nn,nn) )
| ? [X77] :
( object(X77)
& v__1(X77,prev_2,prev_2)
& node_next(nn) = X77 ) ) ) ) ) ) ) )
& ( null = X0
| ~ v__1(sortedList_first,X0,X0)
| nn = X0 ) ),
inference(ennf_transformation,[],[f60]) ).
fof(f92,plain,
! [X0,X1] :
( ~ integer(X0)
| ~ integer(X1)
| ~ lteq(X0,X1)
| ~ lteq(X1,X0)
| X0 = X1 ),
inference(ennf_transformation,[],[f2]) ).
fof(f93,plain,
! [X0,X1] :
( ~ integer(X0)
| ~ integer(X1)
| ~ lteq(X0,X1)
| ~ lteq(X1,X0)
| X0 = X1 ),
inference(flattening,[],[f92]) ).
fof(f94,definition,
( ? [X77] :
( object(X77)
& v__1(X77,prev_2,prev_2)
& node_next(nn) = X77 )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f95,definition,
( ( ? [X75] :
( object(X75)
& node_next(nn) = X75
& ~ v__1(X75,nn,prev_2) )
& ( ? [X76] :
( object(X76)
& node_next(nn) = X76
& ~ v__1(X76,nn,nn) )
| sP0 ) )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f96,definition,
( ? [X74] :
( object(X74)
& v__1(X74,prev_2,prev_2)
& node_next(nn) = X74 )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f97,definition,
( ( ? [X72] :
( object(X72)
& node_next(nn) = X72
& ~ v__1(X72,nn,prev_2) )
& ( ? [X73] :
( object(X73)
& node_next(nn) = X73
& ~ v__1(X73,nn,nn) )
| sP2 ) )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f98,definition,
( ? [X70] :
( object(X70)
& v__1(X70,nn,nn)
& node_next(nn) = X70 )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f99,definition,
( ( ? [X68] :
( object(X68)
& node_next(nn) = X68
& ~ v__1(X68,prev_2,nn) )
& ( ? [X69] :
( object(X69)
& node_next(nn) = X69
& ~ v__1(X69,prev_2,prev_2) )
| sP4 ) )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f100,definition,
! [X0] :
( ( ? [X65] :
( object(X65)
& v__1(X65,nn,nn)
& node_next(nn) = X65 )
& ? [X66] :
( object(X66)
& node_next(nn) = X66
& ~ v__1(X66,X0,X0) ) )
| ~ sP6(X0) ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f101,definition,
! [X0] :
( ( ? [X61] :
( object(X61)
& v__1(X61,nn,nn)
& node_next(nn) = X61 )
& ? [X62] :
( object(X62)
& node_next(nn) = X62
& ~ v__1(X62,X0,X0) ) )
| ~ sP7(X0) ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f102,definition,
! [X0] :
( ? [X63] :
( object(X63)
& v__1(X63,X0,nn)
& node_next(nn) = X63 )
| ~ sP8(X0) ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f103,definition,
! [X0] :
( ( ? [X58] :
( object(X58)
& v__1(X58,X0,X0)
& node_next(nn) = X58 )
& ? [X59] :
( object(X59)
& node_next(nn) = X59
& ~ v__1(X59,nn,nn) ) )
| ~ sP9(X0) ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f104,definition,
! [X0] :
( ( nn != X0
& ( ? [X64] :
( object(X64)
& v__1(X64,nn,X0)
& node_next(nn) = X64 )
| sP6(X0) )
& v__1(null,X0,X0)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP10(X0) ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f105,definition,
! [X0] :
( ( nn != X0
& ( ? [X60] :
( object(X60)
& v__1(X60,nn,X0)
& node_next(nn) = X60 )
| sP7(X0) )
& sP8(X0)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP11(X0) ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f106,definition,
( nn = prev_2
| ? [X71] :
( object(X71)
& node_next(nn) = X71
& ~ v__1(X71,prev_2,nn) )
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) )
| sP3
| ~ sP12 ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f107,definition,
! [X0] :
( ( ? [X56] :
( object(X56)
& v__1(X56,X0,X0)
& node_next(nn) = X56 )
& ( ? [X57] :
( object(X57)
& v__1(X57,X0,nn)
& node_next(nn) = X57 )
| sP9(X0) ) )
| sP11(X0)
| sP10(X0)
| ~ sP13(X0) ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f108,definition,
( ( ? [X54] :
( object(X54)
& v__1(X54,nn,nn)
& node_next(nn) = X54 )
& ? [X55] :
( object(X55)
& node_next(nn) = X55
& ~ v__1(X55,prev_2,prev_2) ) )
| ~ sP14 ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f109,definition,
( ( ? [X50] :
( object(X50)
& v__1(X50,nn,nn)
& node_next(nn) = X50 )
& ? [X51] :
( object(X51)
& node_next(nn) = X51
& ~ v__1(X51,prev_2,prev_2) ) )
| ~ sP15 ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f110,definition,
! [X0] :
( ? [X52] :
( object(X52)
& v__1(X52,X0,nn)
& node_next(nn) = X52 )
| ~ sP16(X0) ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f111,definition,
( ( ? [X47] :
( object(X47)
& v__1(X47,prev_2,prev_2)
& node_next(nn) = X47 )
& ? [X48] :
( object(X48)
& node_next(nn) = X48
& ~ v__1(X48,nn,nn) ) )
| ~ sP17 ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f112,definition,
! [X0] :
( ( sP13(X0)
& ( ? [X67] :
( object(X67)
& node_next(nn) = X67
& ~ v__1(X67,prev_2,prev_2) )
| sP5 )
& sP12
& ( nn = prev_2
| ~ v__1(null,prev_2,prev_2)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) )
| sP1 ) )
| ~ sP18(X0) ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f113,definition,
! [X0] :
( ( nn != prev_2
& ( ? [X53] :
( object(X53)
& v__1(X53,nn,prev_2)
& node_next(nn) = X53 )
| sP14 )
& v__1(null,X0,prev_2)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP19(X0) ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f114,definition,
! [X0] :
( ( nn != prev_2
& ( ? [X49] :
( object(X49)
& v__1(X49,nn,prev_2)
& node_next(nn) = X49 )
| sP15 )
& sP16(X0)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP20(X0) ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f115,definition,
! [X0] :
( ( ? [X43] :
( object(X43)
& v__1(X43,nn,nn)
& node_next(nn) = X43 )
& ? [X44] :
( object(X44)
& node_next(nn) = X44
& ~ v__1(X44,X0,X0) ) )
| ~ sP21(X0) ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f116,definition,
! [X0] :
( ( ? [X39] :
( object(X39)
& v__1(X39,nn,nn)
& node_next(nn) = X39 )
& ? [X40] :
( object(X40)
& node_next(nn) = X40
& ~ v__1(X40,X0,X0) ) )
| ~ sP22(X0) ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f117,definition,
! [X0] :
( ? [X41] :
( object(X41)
& v__1(X41,X0,nn)
& node_next(nn) = X41 )
| ~ sP23(X0) ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f118,definition,
! [X0] :
( ( ? [X36] :
( object(X36)
& v__1(X36,X0,X0)
& node_next(nn) = X36 )
& ? [X37] :
( object(X37)
& node_next(nn) = X37
& ~ v__1(X37,nn,nn) ) )
| ~ sP24(X0) ),
introduced(definition,[new_symbols(definition,[sP24])],[predicate_definition_introduction]) ).
fof(f119,definition,
! [X0] :
( ( nn != X0
& ( ? [X42] :
( object(X42)
& v__1(X42,nn,X0)
& node_next(nn) = X42 )
| sP21(X0) )
& v__1(null,X0,X0)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP25(X0) ),
introduced(definition,[new_symbols(definition,[sP25])],[predicate_definition_introduction]) ).
fof(f120,definition,
! [X0] :
( ( nn != X0
& ( ? [X38] :
( object(X38)
& v__1(X38,nn,X0)
& node_next(nn) = X38 )
| sP22(X0) )
& sP23(X0)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP26(X0) ),
introduced(definition,[new_symbols(definition,[sP26])],[predicate_definition_introduction]) ).
fof(f121,definition,
( ( nn != prev_2
& ( v__1(sortedList_first,nn,prev_2)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,prev_2,prev_2) ) )
& v__1(null,prev_2,prev_2)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP27 ),
introduced(definition,[new_symbols(definition,[sP27])],[predicate_definition_introduction]) ).
fof(f122,definition,
( ( nn != prev_2
& ( v__1(sortedList_first,nn,prev_2)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,prev_2,prev_2) ) )
& v__1(sortedList_first,prev_2,nn)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP28 ),
introduced(definition,[new_symbols(definition,[sP28])],[predicate_definition_introduction]) ).
fof(f123,definition,
! [X0] :
( nn = X0
| ~ v__1(null,X0,X0)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) )
| ( ~ v__1(sortedList_first,nn,X0)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,X0,X0) ) )
| ~ sP29(X0) ),
introduced(definition,[new_symbols(definition,[sP29])],[predicate_definition_introduction]) ).
fof(f124,definition,
! [X0] :
( nn = X0
| ~ v__1(sortedList_first,X0,nn)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) )
| ( ~ v__1(sortedList_first,nn,X0)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,X0,X0) ) )
| ~ sP30(X0) ),
introduced(definition,[new_symbols(definition,[sP30])],[predicate_definition_introduction]) ).
fof(f125,definition,
! [X0] :
( ( ( ( v__1(sortedList_first,prev_2,prev_2)
& ( v__1(sortedList_first,prev_2,nn)
| ( v__1(sortedList_first,prev_2,prev_2)
& ~ v__1(sortedList_first,nn,nn) ) ) )
| sP28
| sP27 )
& ( ~ v__1(sortedList_first,X0,X0)
| ( ~ v__1(sortedList_first,X0,nn)
& ( ~ v__1(sortedList_first,X0,X0)
| v__1(sortedList_first,nn,nn) ) ) )
& sP30(X0)
& sP29(X0) )
| ~ sP31(X0) ),
introduced(definition,[new_symbols(definition,[sP31])],[predicate_definition_introduction]) ).
fof(f126,definition,
! [X0] :
( ( nn != X0
& ( v__1(sortedList_first,nn,X0)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,X0,X0) ) )
& v__1(null,prev_2,X0)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP32(X0) ),
introduced(definition,[new_symbols(definition,[sP32])],[predicate_definition_introduction]) ).
fof(f127,definition,
! [X0] :
( ( nn != X0
& ( v__1(sortedList_first,nn,X0)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,X0,X0) ) )
& v__1(sortedList_first,prev_2,nn)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP33(X0) ),
introduced(definition,[new_symbols(definition,[sP33])],[predicate_definition_introduction]) ).
fof(f128,definition,
! [X0] :
( ( ? [X45] :
( object(X45)
& v__1(X45,X0,prev_2)
& node_next(nn) = X45 )
& ( ? [X46] :
( object(X46)
& v__1(X46,prev_2,nn)
& node_next(nn) = X46 )
| sP17 ) )
| sP20(X0)
| sP19(X0)
| sP18(X0)
| ~ sP34(X0) ),
introduced(definition,[new_symbols(definition,[sP34])],[predicate_definition_introduction]) ).
fof(f129,definition,
! [X0] :
( ( ? [X34] :
( object(X34)
& v__1(X34,X0,X0)
& node_next(nn) = X34 )
& ( ? [X35] :
( object(X35)
& v__1(X35,X0,nn)
& node_next(nn) = X35 )
| sP24(X0) ) )
| sP26(X0)
| sP25(X0)
| ~ sP35(X0) ),
introduced(definition,[new_symbols(definition,[sP35])],[predicate_definition_introduction]) ).
fof(f130,definition,
( ? [X33] :
( object(X33)
& v__1(X33,prev_2,prev_2)
& node_next(nn) = X33 )
| ~ sP36 ),
introduced(definition,[new_symbols(definition,[sP36])],[predicate_definition_introduction]) ).
fof(f131,definition,
( ( ? [X31] :
( object(X31)
& node_next(nn) = X31
& ~ v__1(X31,nn,prev_2) )
& ( ? [X32] :
( object(X32)
& node_next(nn) = X32
& ~ v__1(X32,nn,nn) )
| sP36 ) )
| ~ sP37 ),
introduced(definition,[new_symbols(definition,[sP37])],[predicate_definition_introduction]) ).
fof(f132,definition,
( ? [X30] :
( object(X30)
& v__1(X30,prev_2,prev_2)
& node_next(nn) = X30 )
| ~ sP38 ),
introduced(definition,[new_symbols(definition,[sP38])],[predicate_definition_introduction]) ).
fof(f133,definition,
( ( ? [X28] :
( object(X28)
& node_next(nn) = X28
& ~ v__1(X28,nn,prev_2) )
& ( ? [X29] :
( object(X29)
& node_next(nn) = X29
& ~ v__1(X29,nn,nn) )
| sP38 ) )
| ~ sP39 ),
introduced(definition,[new_symbols(definition,[sP39])],[predicate_definition_introduction]) ).
fof(f134,definition,
( ? [X26] :
( object(X26)
& v__1(X26,nn,nn)
& node_next(nn) = X26 )
| ~ sP40 ),
introduced(definition,[new_symbols(definition,[sP40])],[predicate_definition_introduction]) ).
fof(f135,definition,
( ( ? [X24] :
( object(X24)
& node_next(nn) = X24
& ~ v__1(X24,prev_2,nn) )
& ( ? [X25] :
( object(X25)
& node_next(nn) = X25
& ~ v__1(X25,prev_2,prev_2) )
| sP40 ) )
| ~ sP41 ),
introduced(definition,[new_symbols(definition,[sP41])],[predicate_definition_introduction]) ).
fof(f136,definition,
! [X0] :
( ( ? [X21] :
( object(X21)
& v__1(X21,nn,nn)
& node_next(nn) = X21 )
& ? [X22] :
( object(X22)
& node_next(nn) = X22
& ~ v__1(X22,X0,X0) ) )
| ~ sP42(X0) ),
introduced(definition,[new_symbols(definition,[sP42])],[predicate_definition_introduction]) ).
fof(f137,definition,
! [X0] :
( ( ? [X17] :
( object(X17)
& v__1(X17,nn,nn)
& node_next(nn) = X17 )
& ? [X18] :
( object(X18)
& node_next(nn) = X18
& ~ v__1(X18,X0,X0) ) )
| ~ sP43(X0) ),
introduced(definition,[new_symbols(definition,[sP43])],[predicate_definition_introduction]) ).
fof(f138,definition,
! [X0] :
( ? [X19] :
( object(X19)
& v__1(X19,X0,nn)
& node_next(nn) = X19 )
| ~ sP44(X0) ),
introduced(definition,[new_symbols(definition,[sP44])],[predicate_definition_introduction]) ).
fof(f139,definition,
! [X0] :
( ( ? [X14] :
( object(X14)
& v__1(X14,X0,X0)
& node_next(nn) = X14 )
& ? [X15] :
( object(X15)
& node_next(nn) = X15
& ~ v__1(X15,nn,nn) ) )
| ~ sP45(X0) ),
introduced(definition,[new_symbols(definition,[sP45])],[predicate_definition_introduction]) ).
fof(f140,definition,
! [X0] :
( ( nn != X0
& ( ? [X20] :
( object(X20)
& v__1(X20,nn,X0)
& node_next(nn) = X20 )
| sP42(X0) )
& v__1(null,X0,X0)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP46(X0) ),
introduced(definition,[new_symbols(definition,[sP46])],[predicate_definition_introduction]) ).
fof(f141,definition,
! [X0] :
( ( nn != X0
& ( ? [X16] :
( object(X16)
& v__1(X16,nn,X0)
& node_next(nn) = X16 )
| sP43(X0) )
& sP44(X0)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP47(X0) ),
introduced(definition,[new_symbols(definition,[sP47])],[predicate_definition_introduction]) ).
fof(f142,definition,
( nn = prev_2
| ? [X27] :
( object(X27)
& node_next(nn) = X27
& ~ v__1(X27,prev_2,nn) )
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) )
| sP39
| ~ sP48 ),
introduced(definition,[new_symbols(definition,[sP48])],[predicate_definition_introduction]) ).
fof(f143,definition,
! [X0] :
( ( ? [X12] :
( object(X12)
& v__1(X12,X0,X0)
& node_next(nn) = X12 )
& ( ? [X13] :
( object(X13)
& v__1(X13,X0,nn)
& node_next(nn) = X13 )
| sP45(X0) ) )
| sP47(X0)
| sP46(X0)
| ~ sP49(X0) ),
introduced(definition,[new_symbols(definition,[sP49])],[predicate_definition_introduction]) ).
fof(f144,definition,
( ( ? [X10] :
( object(X10)
& v__1(X10,nn,nn)
& node_next(nn) = X10 )
& ? [X11] :
( object(X11)
& node_next(nn) = X11
& ~ v__1(X11,prev_2,prev_2) ) )
| ~ sP50 ),
introduced(definition,[new_symbols(definition,[sP50])],[predicate_definition_introduction]) ).
fof(f145,definition,
( ( ? [X6] :
( object(X6)
& v__1(X6,nn,nn)
& node_next(nn) = X6 )
& ? [X7] :
( object(X7)
& node_next(nn) = X7
& ~ v__1(X7,prev_2,prev_2) ) )
| ~ sP51 ),
introduced(definition,[new_symbols(definition,[sP51])],[predicate_definition_introduction]) ).
fof(f146,definition,
! [X0] :
( ? [X8] :
( object(X8)
& v__1(X8,X0,nn)
& node_next(nn) = X8 )
| ~ sP52(X0) ),
introduced(definition,[new_symbols(definition,[sP52])],[predicate_definition_introduction]) ).
fof(f147,definition,
( ( ? [X3] :
( object(X3)
& v__1(X3,prev_2,prev_2)
& node_next(nn) = X3 )
& ? [X4] :
( object(X4)
& node_next(nn) = X4
& ~ v__1(X4,nn,nn) ) )
| ~ sP53 ),
introduced(definition,[new_symbols(definition,[sP53])],[predicate_definition_introduction]) ).
fof(f148,definition,
! [X0] :
( ( sP49(X0)
& ( ? [X23] :
( object(X23)
& node_next(nn) = X23
& ~ v__1(X23,prev_2,prev_2) )
| sP41 )
& sP48
& ( nn = prev_2
| ~ v__1(null,prev_2,prev_2)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) )
| sP37 ) )
| ~ sP54(X0) ),
introduced(definition,[new_symbols(definition,[sP54])],[predicate_definition_introduction]) ).
fof(f149,definition,
! [X0] :
( ( nn != prev_2
& ( ? [X9] :
( object(X9)
& v__1(X9,nn,prev_2)
& node_next(nn) = X9 )
| sP50 )
& v__1(null,X0,prev_2)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP55(X0) ),
introduced(definition,[new_symbols(definition,[sP55])],[predicate_definition_introduction]) ).
fof(f150,definition,
! [X0] :
( ( nn != prev_2
& ( ? [X5] :
( object(X5)
& v__1(X5,nn,prev_2)
& node_next(nn) = X5 )
| sP51 )
& sP52(X0)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP56(X0) ),
introduced(definition,[new_symbols(definition,[sP56])],[predicate_definition_introduction]) ).
fof(f151,definition,
! [X0] :
( ( nn != prev_2
& ( v__1(sortedList_first,nn,prev_2)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,prev_2,prev_2) ) )
& v__1(null,X0,prev_2)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP57(X0) ),
introduced(definition,[new_symbols(definition,[sP57])],[predicate_definition_introduction]) ).
fof(f152,definition,
! [X0] :
( ( nn != prev_2
& ( v__1(sortedList_first,nn,prev_2)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,prev_2,prev_2) ) )
& v__1(sortedList_first,X0,nn)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP58(X0) ),
introduced(definition,[new_symbols(definition,[sP58])],[predicate_definition_introduction]) ).
fof(f153,definition,
( ( nn != prev_2
& ( v__1(sortedList_first,nn,prev_2)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,prev_2,prev_2) ) )
& v__1(null,prev_2,prev_2)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP59 ),
introduced(definition,[new_symbols(definition,[sP59])],[predicate_definition_introduction]) ).
fof(f154,definition,
( ( nn != prev_2
& ( v__1(sortedList_first,nn,prev_2)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,prev_2,prev_2) ) )
& v__1(sortedList_first,prev_2,nn)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP60 ),
introduced(definition,[new_symbols(definition,[sP60])],[predicate_definition_introduction]) ).
fof(f155,definition,
! [X0] :
( nn = X0
| ~ v__1(null,X0,X0)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) )
| ( ~ v__1(sortedList_first,nn,X0)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,X0,X0) ) )
| ~ sP61(X0) ),
introduced(definition,[new_symbols(definition,[sP61])],[predicate_definition_introduction]) ).
fof(f156,definition,
! [X0] :
( nn = X0
| ~ v__1(sortedList_first,X0,nn)
| ( ~ v__1(null,X0,nn)
& ( ~ v__1(null,X0,X0)
| v__1(null,nn,nn) ) )
| ( ~ v__1(sortedList_first,nn,X0)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,X0,X0) ) )
| ~ sP62(X0) ),
introduced(definition,[new_symbols(definition,[sP62])],[predicate_definition_introduction]) ).
fof(f157,definition,
! [X0] :
( ( ( ( v__1(sortedList_first,prev_2,prev_2)
& ( v__1(sortedList_first,prev_2,nn)
| ( v__1(sortedList_first,prev_2,prev_2)
& ~ v__1(sortedList_first,nn,nn) ) ) )
| sP60
| sP59 )
& ( ~ v__1(sortedList_first,X0,X0)
| ( ~ v__1(sortedList_first,X0,nn)
& ( ~ v__1(sortedList_first,X0,X0)
| v__1(sortedList_first,nn,nn) ) ) )
& sP62(X0)
& sP61(X0) )
| ~ sP63(X0) ),
introduced(definition,[new_symbols(definition,[sP63])],[predicate_definition_introduction]) ).
fof(f158,definition,
! [X0] :
( ( nn != X0
& ( v__1(sortedList_first,nn,X0)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,X0,X0) ) )
& v__1(null,prev_2,X0)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP64(X0) ),
introduced(definition,[new_symbols(definition,[sP64])],[predicate_definition_introduction]) ).
fof(f159,definition,
! [X0] :
( ( nn != X0
& ( v__1(sortedList_first,nn,X0)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,X0,X0) ) )
& v__1(sortedList_first,prev_2,nn)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP65(X0) ),
introduced(definition,[new_symbols(definition,[sP65])],[predicate_definition_introduction]) ).
fof(f160,definition,
! [X0] :
( ( ? [X1] :
( object(X1)
& v__1(X1,X0,prev_2)
& node_next(nn) = X1 )
& ( ? [X2] :
( object(X2)
& v__1(X2,prev_2,nn)
& node_next(nn) = X2 )
| sP53 ) )
| sP56(X0)
| sP55(X0)
| sP54(X0)
| ~ sP66(X0) ),
introduced(definition,[new_symbols(definition,[sP66])],[predicate_definition_introduction]) ).
fof(f161,definition,
! [X0] :
( ( nn != X0
& ( v__1(sortedList_first,nn,X0)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,X0,X0) ) )
& v__1(null,X0,X0)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP67(X0) ),
introduced(definition,[new_symbols(definition,[sP67])],[predicate_definition_introduction]) ).
fof(f162,definition,
! [X0] :
( ( nn != X0
& ( v__1(sortedList_first,nn,X0)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,X0,X0) ) )
& v__1(sortedList_first,X0,nn)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP68(X0) ),
introduced(definition,[new_symbols(definition,[sP68])],[predicate_definition_introduction]) ).
fof(f163,definition,
( nn = prev_2
| ~ v__1(null,prev_2,prev_2)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) )
| ( ~ v__1(sortedList_first,nn,prev_2)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,prev_2,prev_2) ) )
| ~ sP69 ),
introduced(definition,[new_symbols(definition,[sP69])],[predicate_definition_introduction]) ).
fof(f164,definition,
( nn = prev_2
| ~ v__1(sortedList_first,prev_2,nn)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) )
| ( ~ v__1(sortedList_first,nn,prev_2)
& ( ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,prev_2,prev_2) ) )
| ~ sP70 ),
introduced(definition,[new_symbols(definition,[sP70])],[predicate_definition_introduction]) ).
fof(f165,definition,
! [X0] :
( ( ( ( v__1(sortedList_first,X0,X0)
& ( v__1(sortedList_first,X0,nn)
| ( v__1(sortedList_first,X0,X0)
& ~ v__1(sortedList_first,nn,nn) ) ) )
| sP68(X0)
| sP67(X0) )
& ( ~ v__1(sortedList_first,prev_2,prev_2)
| ( ~ v__1(sortedList_first,prev_2,nn)
& ( ~ v__1(sortedList_first,prev_2,prev_2)
| v__1(sortedList_first,nn,nn) ) ) )
& sP70
& sP69 )
| ~ sP71(X0) ),
introduced(definition,[new_symbols(definition,[sP71])],[predicate_definition_introduction]) ).
fof(f166,definition,
! [X0] :
( ( nn != prev_2
& ( v__1(sortedList_first,nn,prev_2)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,prev_2,prev_2) ) )
& v__1(null,X0,prev_2)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP72(X0) ),
introduced(definition,[new_symbols(definition,[sP72])],[predicate_definition_introduction]) ).
fof(f167,definition,
! [X0] :
( ( nn != prev_2
& ( v__1(sortedList_first,nn,prev_2)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,prev_2,prev_2) ) )
& v__1(sortedList_first,X0,nn)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP73(X0) ),
introduced(definition,[new_symbols(definition,[sP73])],[predicate_definition_introduction]) ).
fof(f168,definition,
! [X0] :
( ( nn != X0
& ( v__1(sortedList_first,nn,X0)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,X0,X0) ) )
& v__1(null,X0,X0)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP74(X0) ),
introduced(definition,[new_symbols(definition,[sP74])],[predicate_definition_introduction]) ).
fof(f169,definition,
! [X0] :
( ( nn != X0
& ( v__1(sortedList_first,nn,X0)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,X0,X0) ) )
& v__1(sortedList_first,X0,nn)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP75(X0) ),
introduced(definition,[new_symbols(definition,[sP75])],[predicate_definition_introduction]) ).
fof(f170,definition,
! [X0] :
( ( prev_2 != X0
& ( ( v__1(sortedList_first,prev_2,X0)
& ( v__1(sortedList_first,X0,nn)
| ( v__1(sortedList_first,X0,X0)
& ~ v__1(sortedList_first,nn,nn) ) ) )
| sP65(X0)
| sP64(X0)
| sP63(X0) )
& ( ( v__1(sortedList_first,X0,prev_2)
& ( v__1(sortedList_first,prev_2,nn)
| ( v__1(sortedList_first,prev_2,prev_2)
& ~ v__1(sortedList_first,nn,nn) ) ) )
| sP58(X0)
| sP57(X0) )
& sP66(X0) )
| ~ sP76(X0) ),
introduced(definition,[new_symbols(definition,[sP76])],[predicate_definition_introduction]) ).
fof(f171,definition,
! [X0] :
( ( prev_2 != X0
& ( ( v__1(sortedList_first,prev_2,X0)
& ( v__1(sortedList_first,X0,nn)
| ( v__1(sortedList_first,X0,X0)
& ~ v__1(sortedList_first,nn,nn) ) ) )
| sP33(X0)
| sP32(X0)
| sP31(X0) )
& sP35(X0)
& sP34(X0) )
| ~ sP77(X0) ),
introduced(definition,[new_symbols(definition,[sP77])],[predicate_definition_introduction]) ).
fof(f172,plain,
? [X0] :
( object(X0)
& null != X0
& ( ( ( ( v__1(sortedList_first,X0,X0)
& ( v__1(sortedList_first,X0,nn)
| ( v__1(sortedList_first,X0,X0)
& ~ v__1(sortedList_first,nn,nn) ) ) )
| sP75(X0)
| sP74(X0) )
& ( ( v__1(sortedList_first,X0,prev_2)
& ( v__1(sortedList_first,prev_2,nn)
| ( v__1(sortedList_first,prev_2,prev_2)
& ~ v__1(sortedList_first,nn,nn) ) ) )
| sP73(X0)
| sP72(X0)
| sP71(X0) ) )
| sP76(X0)
| sP77(X0) )
& ( null = X0
| ~ v__1(sortedList_first,X0,X0)
| nn = X0 ) ),
inference(definition_folding,[],[f85,f171,f170,f169,f168,f167,f166,f165,f164,f163,f162,f161,f160,f159,f158,f157,f156,f155,f154,f153,f152,f151,f150,f149,f148,f147,f146,f145,f144,f143,f142,f141,f140,f139,f138,f137,f136,f135,f134,f133,f132,f131,f130,f129,f128,f127,f126,f125,f124,f123,f122,f121,f120,f119,f118,f117,f116,f115,f114,f113,f112,f111,f110,f109,f108,f107,f106,f105,f104,f103,f102,f101,f100,f99,f98,f97,f96,f95,f94]) ).
fof(f173,plain,
( integer(sK78)
& integer(sK79)
& lteq(sK78,sK79)
& node_key(nn) = sK78
& node_key(nn) = sK79 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK78,sK79]),skolemize(X0,sK78),skolemize(X1,sK79)],[f27]) ).
fof(f174,plain,
! [X0] :
( ( prev_2 != X0
& ( ( v__1(sortedList_first,prev_2,X0)
& ( v__1(sortedList_first,X0,nn)
| ( v__1(sortedList_first,X0,X0)
& ~ v__1(sortedList_first,nn,nn) ) ) )
| sP33(X0)
| sP32(X0)
| sP31(X0) )
& sP35(X0)
& sP34(X0) )
| ~ sP77(X0) ),
inference(nnf_transformation,[],[f171]) ).
fof(f175,plain,
! [X0] :
( ( prev_2 != X0
& ( ( v__1(sortedList_first,prev_2,X0)
& ( v__1(sortedList_first,X0,nn)
| ( v__1(sortedList_first,X0,X0)
& ~ v__1(sortedList_first,nn,nn) ) ) )
| sP65(X0)
| sP64(X0)
| sP63(X0) )
& ( ( v__1(sortedList_first,X0,prev_2)
& ( v__1(sortedList_first,prev_2,nn)
| ( v__1(sortedList_first,prev_2,prev_2)
& ~ v__1(sortedList_first,nn,nn) ) ) )
| sP58(X0)
| sP57(X0) )
& sP66(X0) )
| ~ sP76(X0) ),
inference(nnf_transformation,[],[f170]) ).
fof(f178,plain,
! [X0] :
( ( nn != prev_2
& ( v__1(sortedList_first,nn,prev_2)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,prev_2,prev_2) ) )
& v__1(sortedList_first,X0,nn)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP73(X0) ),
inference(nnf_transformation,[],[f167]) ).
fof(f179,plain,
! [X0] :
( ( nn != prev_2
& ( v__1(sortedList_first,nn,prev_2)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,prev_2,prev_2) ) )
& v__1(null,X0,prev_2)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP72(X0) ),
inference(nnf_transformation,[],[f166]) ).
fof(f180,plain,
! [X0] :
( ( ( ( v__1(sortedList_first,X0,X0)
& ( v__1(sortedList_first,X0,nn)
| ( v__1(sortedList_first,X0,X0)
& ~ v__1(sortedList_first,nn,nn) ) ) )
| sP68(X0)
| sP67(X0) )
& ( ~ v__1(sortedList_first,prev_2,prev_2)
| ( ~ v__1(sortedList_first,prev_2,nn)
& ( ~ v__1(sortedList_first,prev_2,prev_2)
| v__1(sortedList_first,nn,nn) ) ) )
& sP70
& sP69 )
| ~ sP71(X0) ),
inference(nnf_transformation,[],[f165]) ).
fof(f194,plain,
! [X0] :
( ( nn != prev_2
& ( v__1(sortedList_first,nn,prev_2)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,prev_2,prev_2) ) )
& v__1(sortedList_first,X0,nn)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP58(X0) ),
inference(nnf_transformation,[],[f152]) ).
fof(f195,plain,
! [X0] :
( ( nn != prev_2
& ( v__1(sortedList_first,nn,prev_2)
| ( v__1(sortedList_first,nn,nn)
& ~ v__1(sortedList_first,prev_2,prev_2) ) )
& v__1(null,X0,prev_2)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP57(X0) ),
inference(nnf_transformation,[],[f151]) ).
fof(f259,plain,
! [X0] :
( ( ? [X34] :
( object(X34)
& v__1(X34,X0,X0)
& node_next(nn) = X34 )
& ( ? [X35] :
( object(X35)
& v__1(X35,X0,nn)
& node_next(nn) = X35 )
| sP24(X0) ) )
| sP26(X0)
| sP25(X0)
| ~ sP35(X0) ),
inference(nnf_transformation,[],[f129]) ).
fof(f260,plain,
! [X0] :
( ( ? [X1] :
( object(X1)
& v__1(X1,X0,X0)
& node_next(nn) = X1 )
& ( ? [X2] :
( object(X2)
& v__1(X2,X0,nn)
& node_next(nn) = X2 )
| sP24(X0) ) )
| sP26(X0)
| sP25(X0)
| ~ sP35(X0) ),
inference(rectify,[],[f259]) ).
fof(f261,plain,
! [X0] :
( ( object(sK113(X0))
& v__1(sK113(X0),X0,X0)
& node_next(nn) = sK113(X0)
& ( ( object(sK114(X0))
& v__1(sK114(X0),X0,nn)
& node_next(nn) = sK114(X0) )
| sP24(X0) ) )
| sP26(X0)
| sP25(X0)
| ~ sP35(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK113,sK114]),skolemize(X1,sK113(X0)),skolemize(X2,sK114(X0))],[f260]) ).
fof(f262,plain,
! [X0] :
( ( ? [X45] :
( object(X45)
& v__1(X45,X0,prev_2)
& node_next(nn) = X45 )
& ( ? [X46] :
( object(X46)
& v__1(X46,prev_2,nn)
& node_next(nn) = X46 )
| sP17 ) )
| sP20(X0)
| sP19(X0)
| sP18(X0)
| ~ sP34(X0) ),
inference(nnf_transformation,[],[f128]) ).
fof(f263,plain,
! [X0] :
( ( ? [X1] :
( object(X1)
& v__1(X1,X0,prev_2)
& node_next(nn) = X1 )
& ( ? [X2] :
( object(X2)
& v__1(X2,prev_2,nn)
& node_next(nn) = X2 )
| sP17 ) )
| sP20(X0)
| sP19(X0)
| sP18(X0)
| ~ sP34(X0) ),
inference(rectify,[],[f262]) ).
fof(f264,plain,
! [X0] :
( ( object(sK115(X0))
& v__1(sK115(X0),X0,prev_2)
& node_next(nn) = sK115(X0)
& ( ( object(sK116)
& v__1(sK116,prev_2,nn)
& node_next(nn) = sK116 )
| sP17 ) )
| sP20(X0)
| sP19(X0)
| sP18(X0)
| ~ sP34(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK115,sK116]),skolemize(X1,sK115(X0)),skolemize(X2,sK116)],[f263]) ).
fof(f272,plain,
! [X0] :
( ( nn != X0
& ( ? [X38] :
( object(X38)
& v__1(X38,nn,X0)
& node_next(nn) = X38 )
| sP22(X0) )
& sP23(X0)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP26(X0) ),
inference(nnf_transformation,[],[f120]) ).
fof(f273,plain,
! [X0] :
( ( nn != X0
& ( ? [X1] :
( object(X1)
& v__1(X1,nn,X0)
& node_next(nn) = X1 )
| sP22(X0) )
& sP23(X0)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP26(X0) ),
inference(rectify,[],[f272]) ).
fof(f274,plain,
! [X0] :
( ( nn != X0
& ( ( object(sK117(X0))
& v__1(sK117(X0),nn,X0)
& node_next(nn) = sK117(X0) )
| sP22(X0) )
& sP23(X0)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP26(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK117]),skolemize(X1,sK117(X0))],[f273]) ).
fof(f275,plain,
! [X0] :
( ( nn != X0
& ( ? [X42] :
( object(X42)
& v__1(X42,nn,X0)
& node_next(nn) = X42 )
| sP21(X0) )
& v__1(null,X0,X0)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP25(X0) ),
inference(nnf_transformation,[],[f119]) ).
fof(f276,plain,
! [X0] :
( ( nn != X0
& ( ? [X1] :
( object(X1)
& v__1(X1,nn,X0)
& node_next(nn) = X1 )
| sP21(X0) )
& v__1(null,X0,X0)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP25(X0) ),
inference(rectify,[],[f275]) ).
fof(f277,plain,
! [X0] :
( ( nn != X0
& ( ( object(sK118(X0))
& v__1(sK118(X0),nn,X0)
& node_next(nn) = sK118(X0) )
| sP21(X0) )
& v__1(null,X0,X0)
& ( v__1(null,X0,nn)
| ( v__1(null,X0,X0)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP25(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK118]),skolemize(X1,sK118(X0))],[f276]) ).
fof(f290,plain,
! [X0] :
( ( nn != prev_2
& ( ? [X49] :
( object(X49)
& v__1(X49,nn,prev_2)
& node_next(nn) = X49 )
| sP15 )
& sP16(X0)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP20(X0) ),
inference(nnf_transformation,[],[f114]) ).
fof(f291,plain,
! [X0] :
( ( nn != prev_2
& ( ? [X1] :
( object(X1)
& v__1(X1,nn,prev_2)
& node_next(nn) = X1 )
| sP15 )
& sP16(X0)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP20(X0) ),
inference(rectify,[],[f290]) ).
fof(f292,plain,
! [X0] :
( ( nn != prev_2
& ( ( object(sK126)
& v__1(sK126,nn,prev_2)
& node_next(nn) = sK126 )
| sP15 )
& sP16(X0)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP20(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK126]),skolemize(X1,sK126)],[f291]) ).
fof(f293,plain,
! [X0] :
( ( nn != prev_2
& ( ? [X53] :
( object(X53)
& v__1(X53,nn,prev_2)
& node_next(nn) = X53 )
| sP14 )
& v__1(null,X0,prev_2)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP19(X0) ),
inference(nnf_transformation,[],[f113]) ).
fof(f294,plain,
! [X0] :
( ( nn != prev_2
& ( ? [X1] :
( object(X1)
& v__1(X1,nn,prev_2)
& node_next(nn) = X1 )
| sP14 )
& v__1(null,X0,prev_2)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP19(X0) ),
inference(rectify,[],[f293]) ).
fof(f295,plain,
! [X0] :
( ( nn != prev_2
& ( ( object(sK127)
& v__1(sK127,nn,prev_2)
& node_next(nn) = sK127 )
| sP14 )
& v__1(null,X0,prev_2)
& ( v__1(null,prev_2,nn)
| ( v__1(null,prev_2,prev_2)
& ~ v__1(null,nn,nn) ) ) )
| ~ sP19(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK127]),skolemize(X1,sK127)],[f294]) ).
fof(f296,plain,
! [X0] :
( ( sP13(X0)
& ( ? [X67] :
( object(X67)
& node_next(nn) = X67
& ~ v__1(X67,prev_2,prev_2) )
| sP5 )
& sP12
& ( nn = prev_2
| ~ v__1(null,prev_2,prev_2)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) )
| sP1 ) )
| ~ sP18(X0) ),
inference(nnf_transformation,[],[f112]) ).
fof(f297,plain,
! [X0] :
( ( sP13(X0)
& ( ? [X1] :
( object(X1)
& node_next(nn) = X1
& ~ v__1(X1,prev_2,prev_2) )
| sP5 )
& sP12
& ( nn = prev_2
| ~ v__1(null,prev_2,prev_2)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) )
| sP1 ) )
| ~ sP18(X0) ),
inference(rectify,[],[f296]) ).
fof(f298,plain,
! [X0] :
( ( sP13(X0)
& ( ( object(sK128)
& node_next(nn) = sK128
& ~ v__1(sK128,prev_2,prev_2) )
| sP5 )
& sP12
& ( nn = prev_2
| ~ v__1(null,prev_2,prev_2)
| ( ~ v__1(null,prev_2,nn)
& ( ~ v__1(null,prev_2,prev_2)
| v__1(null,nn,nn) ) )
| sP1 ) )
| ~ sP18(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK128]),skolemize(X1,sK128)],[f297]) ).
fof(f299,plain,
( ( ? [X47] :
( object(X47)
& v__1(X47,prev_2,prev_2)
& node_next(nn) = X47 )
& ? [X48] :
( object(X48)
& node_next(nn) = X48
& ~ v__1(X48,nn,nn) ) )
| ~ sP17 ),
inference(nnf_transformation,[],[f111]) ).
fof(f300,plain,
( ( ? [X0] :
( object(X0)
& v__1(X0,prev_2,prev_2)
& node_next(nn) = X0 )
& ? [X1] :
( object(X1)
& node_next(nn) = X1
& ~ v__1(X1,nn,nn) ) )
| ~ sP17 ),
inference(rectify,[],[f299]) ).
fof(f301,plain,
( ( object(sK129)
& v__1(sK129,prev_2,prev_2)
& node_next(nn) = sK129
& object(sK130)
& node_next(nn) = sK130
& ~ v__1(sK130,nn,nn) )
| ~ sP17 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK129,sK130]),skolemize(X0,sK129),skolemize(X1,sK130)],[f300]) ).
fof(f335,plain,
( ( ? [X68] :
( object(X68)
& node_next(nn) = X68
& ~ v__1(X68,prev_2,nn) )
& ( ? [X69] :
( object(X69)
& node_next(nn) = X69
& ~ v__1(X69,prev_2,prev_2) )
| sP4 ) )
| ~ sP5 ),
inference(nnf_transformation,[],[f99]) ).
fof(f336,plain,
( ( ? [X0] :
( object(X0)
& node_next(nn) = X0
& ~ v__1(X0,prev_2,nn) )
& ( ? [X1] :
( object(X1)
& node_next(nn) = X1
& ~ v__1(X1,prev_2,prev_2) )
| sP4 ) )
| ~ sP5 ),
inference(rectify,[],[f335]) ).
fof(f337,plain,
( ( object(sK148)
& node_next(nn) = sK148
& ~ v__1(sK148,prev_2,nn)
& ( ( object(sK149)
& node_next(nn) = sK149
& ~ v__1(sK149,prev_2,prev_2) )
| sP4 ) )
| ~ sP5 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK148,sK149]),skolemize(X0,sK148),skolemize(X1,sK149)],[f336]) ).
fof(f338,plain,
( ? [X70] :
( object(X70)
& v__1(X70,nn,nn)
& node_next(nn) = X70 )
| ~ sP4 ),
inference(nnf_transformation,[],[f98]) ).
fof(f339,plain,
( ? [X0] :
( object(X0)
& v__1(X0,nn,nn)
& node_next(nn) = X0 )
| ~ sP4 ),
inference(rectify,[],[f338]) ).
fof(f340,plain,
( ( object(sK150)
& v__1(sK150,nn,nn)
& node_next(nn) = sK150 )
| ~ sP4 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK150]),skolemize(X0,sK150)],[f339]) ).
fof(f353,plain,
( object(sK157)
& null != sK157
& ( ( ( ( v__1(sortedList_first,sK157,sK157)
& ( v__1(sortedList_first,sK157,nn)
| ( v__1(sortedList_first,sK157,sK157)
& ~ v__1(sortedList_first,nn,nn) ) ) )
| sP75(sK157)
| sP74(sK157) )
& ( ( v__1(sortedList_first,sK157,prev_2)
& ( v__1(sortedList_first,prev_2,nn)
| ( v__1(sortedList_first,prev_2,prev_2)
& ~ v__1(sortedList_first,nn,nn) ) ) )
| sP73(sK157)
| sP72(sK157)
| sP71(sK157) ) )
| sP76(sK157)
| sP77(sK157) )
& ( null = sK157
| ~ v__1(sortedList_first,sK157,sK157)
| nn = sK157 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK157]),skolemize(X0,sK157)],[f172]) ).
fof(f354,plain,
object(nn),
inference(cnf_transformation,[],[f6]) ).
fof(f356,plain,
object(prev_2),
inference(cnf_transformation,[],[f8]) ).
fof(f358,plain,
! [X0] : integer(node_key(X0)),
inference(cnf_transformation,[],[f10]) ).
fof(f359,plain,
object(null),
inference(cnf_transformation,[],[f11]) ).
fof(f361,plain,
object(sortedList_first),
inference(cnf_transformation,[],[f13]) ).
fof(f362,plain,
! [X0] : object(node_next(X0)),
inference(cnf_transformation,[],[f14]) ).
fof(f364,plain,
! [X2,X0,X1] :
( ~ v__1(X1,X2,X2)
| ~ object(X1)
| ~ object(X2)
| ~ v__1(X0,X1,X1)
| ~ object(X0)
| v__1(X0,X2,X2) ),
inference(cnf_transformation,[],[f62]) ).
fof(f369,plain,
! [X2,X0,X1] :
( ~ v__1(X0,X2,X2)
| ~ object(X1)
| ~ object(X2)
| ~ v__1(X0,X1,X1)
| ~ object(X0)
| v__1(X0,X1,X2)
| v__1(X0,X2,X1) ),
inference(cnf_transformation,[],[f68]) ).
fof(f370,plain,
! [X2,X0,X1] :
( ~ v__1(X0,X1,X2)
| ~ object(X1)
| ~ object(X2)
| ~ object(X0)
| v__1(X1,X2,X2) ),
inference(cnf_transformation,[],[f70]) ).
fof(f371,plain,
! [X2,X0,X1] :
( ~ v__1(X0,X1,X2)
| ~ object(X1)
| ~ object(X2)
| ~ object(X0)
| v__1(X0,X1,X1) ),
inference(cnf_transformation,[],[f70]) ).
fof(f374,plain,
! [X0,X1] :
( node_next(X0) != X0
| ~ object(X1)
| ~ object(X0)
| ~ v__1(X0,X1,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f74]) ).
fof(f377,plain,
prev_2 != null,
inference(cnf_transformation,[],[f26]) ).
fof(f378,plain,
node_key(nn) = sK79,
inference(cnf_transformation,[],[f173]) ).
fof(f379,plain,
node_key(nn) = sK78,
inference(cnf_transformation,[],[f173]) ).
fof(f382,plain,
integer(sK78),
inference(cnf_transformation,[],[f173]) ).
fof(f385,plain,
( v__1(nn,nn,nn)
| nn = null
| ~ v__1(sortedList_first,nn,nn) ),
inference(cnf_transformation,[],[f30]) ).
fof(f386,plain,
( prev_2 = null
| v__1(sortedList_first,prev_2,prev_2) ),
inference(cnf_transformation,[],[f31]) ).
fof(f388,plain,
( nn = null
| v__1(sortedList_first,nn,nn) ),
inference(cnf_transformation,[],[f32]) ).
fof(f391,plain,
( prev_2 = null
| nn = node_next(prev_2) ),
inference(cnf_transformation,[],[f34]) ).
fof(f401,plain,
! [X2,X0,X1,X5] :
( ~ object(X0)
| ~ object(X1)
| ~ v__1(sortedList_first,X0,X0)
| null = X0
| ~ object(X2)
| ~ v__1(X2,X1,X1)
| node_next(X0) != X2
| null = X1
| ~ integer(X5)
| node_key(X0) != X5
| node_key(X1) != X5 ),
inference(cnf_transformation,[],[f80]) ).
fof(f402,plain,
! [X2,X3,X0,X1,X4] :
( ~ object(X0)
| ~ object(X1)
| ~ v__1(sortedList_first,X0,X0)
| null = X0
| ~ object(X2)
| ~ v__1(X2,X1,X1)
| node_next(X0) != X2
| null = X1
| ~ integer(X3)
| ~ integer(X4)
| node_key(X0) != X3
| node_key(X1) != X4
| lteq(X3,X4) ),
inference(cnf_transformation,[],[f80]) ).
fof(f403,plain,
! [X0,X1] :
( ~ object(X0)
| ~ object(X1)
| null = X0
| null = X1
| node_next(X0) != X1
| v__1(sortedList_first,X1,X1) ),
inference(cnf_transformation,[],[f82]) ).
fof(f406,plain,
nn != null,
inference(cnf_transformation,[],[f47]) ).
fof(f428,plain,
null = node_next(null),
inference(cnf_transformation,[],[f57]) ).
fof(f430,plain,
! [X0] :
( ~ sP77(X0)
| sP34(X0) ),
inference(cnf_transformation,[],[f174]) ).
fof(f431,plain,
! [X0] :
( ~ sP77(X0)
| sP35(X0) ),
inference(cnf_transformation,[],[f174]) ).
fof(f439,plain,
! [X0] :
( v__1(sortedList_first,X0,prev_2)
| sP58(X0)
| sP57(X0)
| ~ sP76(X0) ),
inference(cnf_transformation,[],[f175]) ).
fof(f459,plain,
! [X0] :
( v__1(sortedList_first,nn,prev_2)
| ~ v__1(sortedList_first,prev_2,prev_2)
| ~ sP73(X0) ),
inference(cnf_transformation,[],[f178]) ).
fof(f465,plain,
! [X0] :
( v__1(sortedList_first,nn,prev_2)
| ~ v__1(sortedList_first,prev_2,prev_2)
| ~ sP72(X0) ),
inference(cnf_transformation,[],[f179]) ).
fof(f471,plain,
! [X0] :
( ~ v__1(sortedList_first,prev_2,prev_2)
| ~ v__1(sortedList_first,prev_2,nn)
| ~ sP71(X0) ),
inference(cnf_transformation,[],[f180]) ).
fof(f543,plain,
! [X0] :
( v__1(sortedList_first,nn,prev_2)
| ~ v__1(sortedList_first,prev_2,prev_2)
| ~ sP58(X0) ),
inference(cnf_transformation,[],[f194]) ).
fof(f549,plain,
! [X0] :
( v__1(sortedList_first,nn,prev_2)
| ~ v__1(sortedList_first,prev_2,prev_2)
| ~ sP57(X0) ),
inference(cnf_transformation,[],[f195]) ).
fof(f671,plain,
! [X0] :
( ~ sP35(X0)
| sP26(X0)
| sP25(X0)
| node_next(nn) = sK113(X0) ),
inference(cnf_transformation,[],[f261]) ).
fof(f672,plain,
! [X0] :
( v__1(sK113(X0),X0,X0)
| sP26(X0)
| sP25(X0)
| ~ sP35(X0) ),
inference(cnf_transformation,[],[f261]) ).
fof(f674,plain,
! [X0] :
( node_next(nn) = sK116
| sP17
| sP20(X0)
| sP19(X0)
| sP18(X0)
| ~ sP34(X0) ),
inference(cnf_transformation,[],[f264]) ).
fof(f675,plain,
! [X0] :
( v__1(sK116,prev_2,nn)
| sP17
| sP20(X0)
| sP19(X0)
| sP18(X0)
| ~ sP34(X0) ),
inference(cnf_transformation,[],[f264]) ).
fof(f676,plain,
! [X0] :
( object(sK116)
| sP17
| sP20(X0)
| sP19(X0)
| sP18(X0)
| ~ sP34(X0) ),
inference(cnf_transformation,[],[f264]) ).
fof(f720,plain,
! [X0] :
( v__1(null,X0,nn)
| v__1(null,X0,X0)
| ~ sP26(X0) ),
inference(cnf_transformation,[],[f274]) ).
fof(f725,plain,
! [X0] :
( nn != X0
| ~ sP26(X0) ),
inference(cnf_transformation,[],[f274]) ).
fof(f728,plain,
! [X0] :
( v__1(null,X0,X0)
| ~ sP25(X0) ),
inference(cnf_transformation,[],[f277]) ).
fof(f732,plain,
! [X0] :
( nn != X0
| ~ sP25(X0) ),
inference(cnf_transformation,[],[f277]) ).
fof(f755,plain,
! [X0] :
( v__1(null,prev_2,nn)
| v__1(null,prev_2,prev_2)
| ~ sP20(X0) ),
inference(cnf_transformation,[],[f292]) ).
fof(f762,plain,
! [X0] :
( v__1(null,prev_2,nn)
| v__1(null,prev_2,prev_2)
| ~ sP19(X0) ),
inference(cnf_transformation,[],[f295]) ).
fof(f772,plain,
! [X0] :
( node_next(nn) = sK128
| sP5
| ~ sP18(X0) ),
inference(cnf_transformation,[],[f298]) ).
fof(f773,plain,
! [X0] :
( object(sK128)
| sP5
| ~ sP18(X0) ),
inference(cnf_transformation,[],[f298]) ).
fof(f776,plain,
( node_next(nn) = sK130
| ~ sP17 ),
inference(cnf_transformation,[],[f301]) ).
fof(f777,plain,
( object(sK130)
| ~ sP17 ),
inference(cnf_transformation,[],[f301]) ).
fof(f778,plain,
( node_next(nn) = sK129
| ~ sP17 ),
inference(cnf_transformation,[],[f301]) ).
fof(f780,plain,
( object(sK129)
| ~ sP17 ),
inference(cnf_transformation,[],[f301]) ).
fof(f844,plain,
( node_next(nn) = sK149
| sP4
| ~ sP5 ),
inference(cnf_transformation,[],[f337]) ).
fof(f845,plain,
( object(sK149)
| sP4
| ~ sP5 ),
inference(cnf_transformation,[],[f337]) ).
fof(f849,plain,
( node_next(nn) = sK150
| ~ sP4 ),
inference(cnf_transformation,[],[f340]) ).
fof(f850,plain,
( v__1(sK150,nn,nn)
| ~ sP4 ),
inference(cnf_transformation,[],[f340]) ).
fof(f870,plain,
( null = sK157
| ~ v__1(sortedList_first,sK157,sK157)
| nn = sK157 ),
inference(cnf_transformation,[],[f353]) ).
fof(f873,plain,
( v__1(sortedList_first,sK157,prev_2)
| sP73(sK157)
| sP72(sK157)
| sP71(sK157)
| sP76(sK157)
| sP77(sK157) ),
inference(cnf_transformation,[],[f353]) ).
fof(f877,plain,
null != sK157,
inference(cnf_transformation,[],[f353]) ).
fof(f878,plain,
object(sK157),
inference(cnf_transformation,[],[f353]) ).
fof(f884,plain,
! [X0,X1] :
( ~ lteq(X1,X0)
| ~ integer(X1)
| ~ lteq(X0,X1)
| ~ integer(X0)
| X0 = X1 ),
inference(cnf_transformation,[],[f93]) ).
fof(f889,plain,
! [X3,X0,X1,X4] :
( ~ object(X0)
| ~ object(X1)
| ~ v__1(sortedList_first,X0,X0)
| null = X0
| ~ object(node_next(X0))
| ~ v__1(node_next(X0),X1,X1)
| null = X1
| ~ integer(X3)
| ~ integer(X4)
| node_key(X0) != X3
| node_key(X1) != X4
| lteq(X3,X4) ),
inference(equality_resolution,[],[f402]) ).
fof(f890,plain,
! [X0,X1,X4] :
( ~ object(X0)
| ~ object(X1)
| ~ v__1(sortedList_first,X0,X0)
| null = X0
| ~ object(node_next(X0))
| ~ v__1(node_next(X0),X1,X1)
| null = X1
| ~ integer(node_key(X0))
| ~ integer(X4)
| node_key(X1) != X4
| lteq(node_key(X0),X4) ),
inference(equality_resolution,[],[f889]) ).
fof(f891,plain,
! [X0,X1] :
( ~ v__1(node_next(X0),X1,X1)
| ~ object(X1)
| ~ v__1(sortedList_first,X0,X0)
| null = X0
| ~ object(node_next(X0))
| ~ object(X0)
| null = X1
| ~ integer(node_key(X0))
| ~ integer(node_key(X1))
| lteq(node_key(X0),node_key(X1)) ),
inference(equality_resolution,[],[f890]) ).
fof(f892,plain,
! [X0,X1,X5] :
( ~ object(X0)
| ~ object(X1)
| ~ v__1(sortedList_first,X0,X0)
| null = X0
| ~ object(node_next(X0))
| ~ v__1(node_next(X0),X1,X1)
| null = X1
| ~ integer(X5)
| node_key(X0) != X5
| node_key(X1) != X5 ),
inference(equality_resolution,[],[f401]) ).
fof(f893,plain,
! [X0,X1] :
( node_key(X0) != node_key(X1)
| ~ object(X1)
| ~ v__1(sortedList_first,X0,X0)
| null = X0
| ~ object(node_next(X0))
| ~ v__1(node_next(X0),X1,X1)
| null = X1
| ~ integer(node_key(X0))
| ~ object(X0) ),
inference(equality_resolution,[],[f892]) ).
fof(f895,plain,
! [X0] :
( v__1(sortedList_first,node_next(X0),node_next(X0))
| ~ object(node_next(X0))
| null = X0
| null = node_next(X0)
| ~ object(X0) ),
inference(equality_resolution,[],[f403]) ).
fof(f919,plain,
~ sP26(nn),
inference(equality_resolution,[],[f725]) ).
fof(f920,plain,
~ sP25(nn),
inference(equality_resolution,[],[f732]) ).
fof(f938,definition,
( spl158_1
<=> nn = sK157 ),
introduced(definition,[new_symbols(definition,[spl158_1])],[avatar_definition]) ).
fof(f940,plain,
( nn = sK157
| ~ spl158_1 ),
inference(avatar_component_clause,[],[f938]) ).
fof(f942,definition,
( spl158_2
<=> v__1(sortedList_first,sK157,sK157) ),
introduced(definition,[new_symbols(definition,[spl158_2])],[avatar_definition]) ).
fof(f944,plain,
( ~ v__1(sortedList_first,sK157,sK157)
| spl158_2 ),
inference(avatar_component_clause,[],[f942]) ).
fof(f946,definition,
( spl158_3
<=> null = sK157 ),
introduced(definition,[new_symbols(definition,[spl158_3])],[avatar_definition]) ).
fof(f947,plain,
( null != sK157
| spl158_3 ),
inference(avatar_component_clause,[],[f946]) ).
fof(f949,plain,
( spl158_1
| ~ spl158_2
| spl158_3 ),
inference(avatar_split_clause,[],[f870,f946,f942,f938]) ).
fof(f951,definition,
( spl158_4
<=> sP77(sK157) ),
introduced(definition,[new_symbols(definition,[spl158_4])],[avatar_definition]) ).
fof(f953,plain,
( sP77(sK157)
| ~ spl158_4 ),
inference(avatar_component_clause,[],[f951]) ).
fof(f955,definition,
( spl158_5
<=> sP76(sK157) ),
introduced(definition,[new_symbols(definition,[spl158_5])],[avatar_definition]) ).
fof(f957,plain,
( sP76(sK157)
| ~ spl158_5 ),
inference(avatar_component_clause,[],[f955]) ).
fof(f959,definition,
( spl158_6
<=> sP71(sK157) ),
introduced(definition,[new_symbols(definition,[spl158_6])],[avatar_definition]) ).
fof(f961,plain,
( sP71(sK157)
| ~ spl158_6 ),
inference(avatar_component_clause,[],[f959]) ).
fof(f963,definition,
( spl158_7
<=> sP72(sK157) ),
introduced(definition,[new_symbols(definition,[spl158_7])],[avatar_definition]) ).
fof(f965,plain,
( sP72(sK157)
| ~ spl158_7 ),
inference(avatar_component_clause,[],[f963]) ).
fof(f967,definition,
( spl158_8
<=> sP73(sK157) ),
introduced(definition,[new_symbols(definition,[spl158_8])],[avatar_definition]) ).
fof(f969,plain,
( sP73(sK157)
| ~ spl158_8 ),
inference(avatar_component_clause,[],[f967]) ).
fof(f971,definition,
( spl158_9
<=> v__1(sortedList_first,nn,nn) ),
introduced(definition,[new_symbols(definition,[spl158_9])],[avatar_definition]) ).
fof(f972,plain,
( v__1(sortedList_first,nn,nn)
| ~ spl158_9 ),
inference(avatar_component_clause,[],[f971]) ).
fof(f975,definition,
( spl158_10
<=> v__1(sortedList_first,prev_2,nn) ),
introduced(definition,[new_symbols(definition,[spl158_10])],[avatar_definition]) ).
fof(f980,definition,
( spl158_11
<=> v__1(sortedList_first,prev_2,prev_2) ),
introduced(definition,[new_symbols(definition,[spl158_11])],[avatar_definition]) ).
fof(f982,plain,
( v__1(sortedList_first,prev_2,prev_2)
| ~ spl158_11 ),
inference(avatar_component_clause,[],[f980]) ).
fof(f985,definition,
( spl158_12
<=> v__1(sortedList_first,sK157,prev_2) ),
introduced(definition,[new_symbols(definition,[spl158_12])],[avatar_definition]) ).
fof(f986,plain,
( ~ v__1(sortedList_first,sK157,prev_2)
| spl158_12 ),
inference(avatar_component_clause,[],[f985]) ).
fof(f987,plain,
( v__1(sortedList_first,sK157,prev_2)
| ~ spl158_12 ),
inference(avatar_component_clause,[],[f985]) ).
fof(f988,plain,
( spl158_4
| spl158_5
| spl158_6
| spl158_7
| spl158_8
| spl158_12 ),
inference(avatar_split_clause,[],[f873,f985,f967,f963,f959,f955,f951]) ).
fof(f1004,plain,
~ spl158_3,
inference(avatar_split_clause,[],[f877,f946]) ).
fof(f1112,definition,
( spl158_38
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl158_38])],[avatar_definition]) ).
fof(f1116,definition,
( spl158_39
<=> node_next(nn) = sK150 ),
introduced(definition,[new_symbols(definition,[spl158_39])],[avatar_definition]) ).
fof(f1118,plain,
( node_next(nn) = sK150
| ~ spl158_39 ),
inference(avatar_component_clause,[],[f1116]) ).
fof(f1119,plain,
( ~ spl158_38
| spl158_39 ),
inference(avatar_split_clause,[],[f849,f1116,f1112]) ).
fof(f1121,definition,
( spl158_40
<=> v__1(sK150,nn,nn) ),
introduced(definition,[new_symbols(definition,[spl158_40])],[avatar_definition]) ).
fof(f1123,plain,
( v__1(sK150,nn,nn)
| ~ spl158_40 ),
inference(avatar_component_clause,[],[f1121]) ).
fof(f1124,plain,
( ~ spl158_38
| spl158_40 ),
inference(avatar_split_clause,[],[f850,f1121,f1112]) ).
fof(f1131,definition,
( spl158_42
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl158_42])],[avatar_definition]) ).
fof(f1140,definition,
( spl158_44
<=> node_next(nn) = sK149 ),
introduced(definition,[new_symbols(definition,[spl158_44])],[avatar_definition]) ).
fof(f1142,plain,
( node_next(nn) = sK149
| ~ spl158_44 ),
inference(avatar_component_clause,[],[f1140]) ).
fof(f1143,plain,
( ~ spl158_42
| spl158_38
| spl158_44 ),
inference(avatar_split_clause,[],[f844,f1140,f1112,f1131]) ).
fof(f1145,definition,
( spl158_45
<=> object(sK149) ),
introduced(definition,[new_symbols(definition,[spl158_45])],[avatar_definition]) ).
fof(f1147,plain,
( object(sK149)
| ~ spl158_45 ),
inference(avatar_component_clause,[],[f1145]) ).
fof(f1148,plain,
( ~ spl158_42
| spl158_38
| spl158_45 ),
inference(avatar_split_clause,[],[f845,f1145,f1112,f1131]) ).
fof(f1235,definition,
( spl158_65
<=> v__1(null,prev_2,prev_2) ),
introduced(definition,[new_symbols(definition,[spl158_65])],[avatar_definition]) ).
fof(f1236,plain,
( v__1(null,prev_2,prev_2)
| ~ spl158_65 ),
inference(avatar_component_clause,[],[f1235]) ).
fof(f1237,plain,
( ~ v__1(null,prev_2,prev_2)
| spl158_65 ),
inference(avatar_component_clause,[],[f1235]) ).
fof(f1248,definition,
( spl158_68
<=> v__1(null,prev_2,nn) ),
introduced(definition,[new_symbols(definition,[spl158_68])],[avatar_definition]) ).
fof(f1249,plain,
( v__1(null,prev_2,nn)
| ~ spl158_68 ),
inference(avatar_component_clause,[],[f1248]) ).
fof(f1333,definition,
( spl158_85
<=> sP17 ),
introduced(definition,[new_symbols(definition,[spl158_85])],[avatar_definition]) ).
fof(f1342,definition,
( spl158_87
<=> node_next(nn) = sK130 ),
introduced(definition,[new_symbols(definition,[spl158_87])],[avatar_definition]) ).
fof(f1344,plain,
( node_next(nn) = sK130
| ~ spl158_87 ),
inference(avatar_component_clause,[],[f1342]) ).
fof(f1345,plain,
( ~ spl158_85
| spl158_87 ),
inference(avatar_split_clause,[],[f776,f1342,f1333]) ).
fof(f1347,definition,
( spl158_88
<=> object(sK130) ),
introduced(definition,[new_symbols(definition,[spl158_88])],[avatar_definition]) ).
fof(f1349,plain,
( object(sK130)
| ~ spl158_88 ),
inference(avatar_component_clause,[],[f1347]) ).
fof(f1350,plain,
( ~ spl158_85
| spl158_88 ),
inference(avatar_split_clause,[],[f777,f1347,f1333]) ).
fof(f1352,definition,
( spl158_89
<=> node_next(nn) = sK129 ),
introduced(definition,[new_symbols(definition,[spl158_89])],[avatar_definition]) ).
fof(f1354,plain,
( node_next(nn) = sK129
| ~ spl158_89 ),
inference(avatar_component_clause,[],[f1352]) ).
fof(f1355,plain,
( ~ spl158_85
| spl158_89 ),
inference(avatar_split_clause,[],[f778,f1352,f1333]) ).
fof(f1362,definition,
( spl158_91
<=> object(sK129) ),
introduced(definition,[new_symbols(definition,[spl158_91])],[avatar_definition]) ).
fof(f1364,plain,
( object(sK129)
| ~ spl158_91 ),
inference(avatar_component_clause,[],[f1362]) ).
fof(f1365,plain,
( ~ spl158_85
| spl158_91 ),
inference(avatar_split_clause,[],[f780,f1362,f1333]) ).
fof(f1367,definition,
( spl158_92
<=> ! [X0] : ~ sP18(X0) ),
introduced(definition,[new_symbols(definition,[spl158_92])],[avatar_definition]) ).
fof(f1368,plain,
( ! [X0] : ~ sP18(X0)
| ~ spl158_92 ),
inference(avatar_component_clause,[],[f1367]) ).
fof(f1378,definition,
( spl158_94
<=> node_next(nn) = sK128 ),
introduced(definition,[new_symbols(definition,[spl158_94])],[avatar_definition]) ).
fof(f1380,plain,
( node_next(nn) = sK128
| ~ spl158_94 ),
inference(avatar_component_clause,[],[f1378]) ).
fof(f1381,plain,
( spl158_92
| spl158_42
| spl158_94 ),
inference(avatar_split_clause,[],[f772,f1378,f1131,f1367]) ).
fof(f1383,definition,
( spl158_95
<=> object(sK128) ),
introduced(definition,[new_symbols(definition,[spl158_95])],[avatar_definition]) ).
fof(f1385,plain,
( object(sK128)
| ~ spl158_95 ),
inference(avatar_component_clause,[],[f1383]) ).
fof(f1386,plain,
( spl158_92
| spl158_42
| spl158_95 ),
inference(avatar_split_clause,[],[f773,f1383,f1131,f1367]) ).
fof(f1388,definition,
( spl158_96
<=> ! [X0] : ~ sP19(X0) ),
introduced(definition,[new_symbols(definition,[spl158_96])],[avatar_definition]) ).
fof(f1389,plain,
( ! [X0] : ~ sP19(X0)
| ~ spl158_96 ),
inference(avatar_component_clause,[],[f1388]) ).
fof(f1391,plain,
( spl158_96
| spl158_65
| spl158_68 ),
inference(avatar_split_clause,[],[f762,f1248,f1235,f1388]) ).
fof(f1409,definition,
( spl158_100
<=> ! [X0] : ~ sP20(X0) ),
introduced(definition,[new_symbols(definition,[spl158_100])],[avatar_definition]) ).
fof(f1410,plain,
( ! [X0] : ~ sP20(X0)
| ~ spl158_100 ),
inference(avatar_component_clause,[],[f1409]) ).
fof(f1412,plain,
( spl158_100
| spl158_65
| spl158_68 ),
inference(avatar_split_clause,[],[f755,f1248,f1235,f1409]) ).
fof(f1499,definition,
( spl158_119
<=> v__1(sortedList_first,nn,prev_2) ),
introduced(definition,[new_symbols(definition,[spl158_119])],[avatar_definition]) ).
fof(f1500,plain,
( ~ v__1(sortedList_first,nn,prev_2)
| spl158_119 ),
inference(avatar_component_clause,[],[f1499]) ).
fof(f1501,plain,
( v__1(sortedList_first,nn,prev_2)
| ~ spl158_119 ),
inference(avatar_component_clause,[],[f1499]) ).
fof(f1570,definition,
( spl158_134
<=> ! [X0] :
( sP20(X0)
| ~ sP34(X0)
| sP18(X0)
| sP19(X0) ) ),
introduced(definition,[new_symbols(definition,[spl158_134])],[avatar_definition]) ).
fof(f1571,plain,
( ! [X0] :
( sP20(X0)
| ~ sP34(X0)
| sP18(X0)
| sP19(X0) )
| ~ spl158_134 ),
inference(avatar_component_clause,[],[f1570]) ).
fof(f1573,definition,
( spl158_135
<=> node_next(nn) = sK116 ),
introduced(definition,[new_symbols(definition,[spl158_135])],[avatar_definition]) ).
fof(f1575,plain,
( node_next(nn) = sK116
| ~ spl158_135 ),
inference(avatar_component_clause,[],[f1573]) ).
fof(f1576,plain,
( spl158_134
| spl158_85
| spl158_135 ),
inference(avatar_split_clause,[],[f674,f1573,f1333,f1570]) ).
fof(f1578,definition,
( spl158_136
<=> v__1(sK116,prev_2,nn) ),
introduced(definition,[new_symbols(definition,[spl158_136])],[avatar_definition]) ).
fof(f1580,plain,
( v__1(sK116,prev_2,nn)
| ~ spl158_136 ),
inference(avatar_component_clause,[],[f1578]) ).
fof(f1581,plain,
( spl158_134
| spl158_85
| spl158_136 ),
inference(avatar_split_clause,[],[f675,f1578,f1333,f1570]) ).
fof(f1583,definition,
( spl158_137
<=> object(sK116) ),
introduced(definition,[new_symbols(definition,[spl158_137])],[avatar_definition]) ).
fof(f1585,plain,
( object(sK116)
| ~ spl158_137 ),
inference(avatar_component_clause,[],[f1583]) ).
fof(f1586,plain,
( spl158_134
| spl158_85
| spl158_137 ),
inference(avatar_split_clause,[],[f676,f1583,f1333,f1570]) ).
fof(f1996,definition,
( spl158_222
<=> ! [X0] : ~ sP57(X0) ),
introduced(definition,[new_symbols(definition,[spl158_222])],[avatar_definition]) ).
fof(f1997,plain,
( ! [X0] : ~ sP57(X0)
| ~ spl158_222 ),
inference(avatar_component_clause,[],[f1996]) ).
fof(f2000,plain,
( spl158_222
| ~ spl158_11
| spl158_119 ),
inference(avatar_split_clause,[],[f549,f1499,f980,f1996]) ).
fof(f2004,definition,
( spl158_223
<=> ! [X0] : ~ sP58(X0) ),
introduced(definition,[new_symbols(definition,[spl158_223])],[avatar_definition]) ).
fof(f2005,plain,
( ! [X0] : ~ sP58(X0)
| ~ spl158_223 ),
inference(avatar_component_clause,[],[f2004]) ).
fof(f2008,plain,
( spl158_223
| ~ spl158_11
| spl158_119 ),
inference(avatar_split_clause,[],[f543,f1499,f980,f2004]) ).
fof(f2136,definition,
( spl158_249
<=> ! [X0] : ~ sP71(X0) ),
introduced(definition,[new_symbols(definition,[spl158_249])],[avatar_definition]) ).
fof(f2137,plain,
( ! [X0] : ~ sP71(X0)
| ~ spl158_249 ),
inference(avatar_component_clause,[],[f2136]) ).
fof(f2141,plain,
( spl158_249
| ~ spl158_10
| ~ spl158_11 ),
inference(avatar_split_clause,[],[f471,f980,f975,f2136]) ).
fof(f2145,definition,
( spl158_250
<=> ! [X0] : ~ sP72(X0) ),
introduced(definition,[new_symbols(definition,[spl158_250])],[avatar_definition]) ).
fof(f2146,plain,
( ! [X0] : ~ sP72(X0)
| ~ spl158_250 ),
inference(avatar_component_clause,[],[f2145]) ).
fof(f2149,plain,
( spl158_250
| ~ spl158_11
| spl158_119 ),
inference(avatar_split_clause,[],[f465,f1499,f980,f2145]) ).
fof(f2153,definition,
( spl158_251
<=> ! [X0] : ~ sP73(X0) ),
introduced(definition,[new_symbols(definition,[spl158_251])],[avatar_definition]) ).
fof(f2154,plain,
( ! [X0] : ~ sP73(X0)
| ~ spl158_251 ),
inference(avatar_component_clause,[],[f2153]) ).
fof(f2157,plain,
( spl158_251
| ~ spl158_11
| spl158_119 ),
inference(avatar_split_clause,[],[f459,f1499,f980,f2153]) ).
fof(f2194,definition,
( spl158_260
<=> object(null) ),
introduced(definition,[new_symbols(definition,[spl158_260])],[avatar_definition]) ).
fof(f2195,plain,
( object(null)
| ~ spl158_260 ),
inference(avatar_component_clause,[],[f2194]) ).
fof(f2220,definition,
( spl158_265
<=> nn = node_next(prev_2) ),
introduced(definition,[new_symbols(definition,[spl158_265])],[avatar_definition]) ).
fof(f2222,plain,
( nn = node_next(prev_2)
| ~ spl158_265 ),
inference(avatar_component_clause,[],[f2220]) ).
fof(f2224,definition,
( spl158_266
<=> prev_2 = null ),
introduced(definition,[new_symbols(definition,[spl158_266])],[avatar_definition]) ).
fof(f2225,plain,
( prev_2 != null
| spl158_266 ),
inference(avatar_component_clause,[],[f2224]) ).
fof(f2227,plain,
( spl158_265
| spl158_266 ),
inference(avatar_split_clause,[],[f391,f2224,f2220]) ).
fof(f2233,plain,
v__1(sortedList_first,nn,nn),
inference(forward_subsumption_resolution,[],[f388,f406]) ).
fof(f2234,plain,
( spl158_11
| spl158_266 ),
inference(avatar_split_clause,[],[f386,f2224,f980]) ).
fof(f2235,plain,
( v__1(nn,nn,nn)
| ~ v__1(sortedList_first,nn,nn) ),
inference(forward_subsumption_resolution,[],[f385,f406]) ).
fof(f2236,plain,
~ spl158_266,
inference(avatar_split_clause,[],[f377,f2224]) ).
fof(f2237,plain,
spl158_260,
inference(avatar_split_clause,[],[f359,f2194]) ).
fof(f2242,plain,
spl158_9,
inference(avatar_split_clause,[],[f2233,f971]) ).
fof(f2244,definition,
( spl158_269
<=> v__1(nn,nn,nn) ),
introduced(definition,[new_symbols(definition,[spl158_269])],[avatar_definition]) ).
fof(f2246,plain,
( v__1(nn,nn,nn)
| ~ spl158_269 ),
inference(avatar_component_clause,[],[f2244]) ).
fof(f2247,plain,
( ~ spl158_9
| spl158_269 ),
inference(avatar_split_clause,[],[f2235,f2244,f971]) ).
fof(f2249,plain,
sK78 = sK79,
inference(superposition,[],[f379,f378]) ).
fof(f2304,plain,
! [X0] :
( null != null
| ~ object(X0)
| ~ object(null)
| ~ v__1(null,X0,X0)
| null = X0 ),
inference(superposition,[],[f374,f428]) ).
fof(f2307,plain,
! [X0] :
( ~ object(X0)
| ~ object(null)
| ~ v__1(null,X0,X0)
| null = X0 ),
inference(trivial_inequality_removal,[],[f2304]) ).
fof(f2309,plain,
( ! [X0] :
( ~ v__1(null,X0,X0)
| ~ object(X0)
| null = X0 )
| ~ spl158_260 ),
inference(forward_subsumption_resolution,[],[f2307,f2195]) ).
fof(f2328,plain,
( $false
| ~ spl158_6
| ~ spl158_249 ),
inference(resolution,[],[f2137,f961]) ).
fof(f2329,plain,
( ~ spl158_6
| ~ spl158_249 ),
inference(avatar_contradiction_clause,[],[f2328]) ).
fof(f2339,plain,
( v__1(sortedList_first,sK149,sK149)
| ~ object(sK149)
| nn = null
| null = sK149
| ~ object(nn)
| ~ spl158_44 ),
inference(superposition,[],[f895,f1142]) ).
fof(f2340,plain,
( v__1(sortedList_first,sK149,sK149)
| nn = null
| null = sK149
| ~ object(nn)
| ~ spl158_44
| ~ spl158_45 ),
inference(forward_subsumption_resolution,[],[f2339,f1147]) ).
fof(f2342,plain,
( v__1(sortedList_first,sK149,sK149)
| null = sK149
| ~ object(nn)
| ~ spl158_44
| ~ spl158_45 ),
inference(forward_subsumption_resolution,[],[f2340,f406]) ).
fof(f2343,plain,
( v__1(sortedList_first,sK149,sK149)
| null = sK149
| ~ spl158_44
| ~ spl158_45 ),
inference(forward_subsumption_resolution,[],[f2342,f354]) ).
fof(f2345,definition,
( spl158_272
<=> null = sK149 ),
introduced(definition,[new_symbols(definition,[spl158_272])],[avatar_definition]) ).
fof(f2347,plain,
( null = sK149
| ~ spl158_272 ),
inference(avatar_component_clause,[],[f2345]) ).
fof(f2349,definition,
( spl158_273
<=> v__1(sortedList_first,sK149,sK149) ),
introduced(definition,[new_symbols(definition,[spl158_273])],[avatar_definition]) ).
fof(f2351,plain,
( v__1(sortedList_first,sK149,sK149)
| ~ spl158_273 ),
inference(avatar_component_clause,[],[f2349]) ).
fof(f2352,plain,
( spl158_272
| spl158_273
| ~ spl158_44
| ~ spl158_45 ),
inference(avatar_split_clause,[],[f2343,f1145,f1140,f2349,f2345]) ).
fof(f3034,plain,
( v__1(sortedList_first,sK130,sK130)
| ~ object(sK130)
| nn = null
| null = sK130
| ~ object(nn)
| ~ spl158_87 ),
inference(superposition,[],[f895,f1344]) ).
fof(f3039,plain,
( v__1(sortedList_first,sK130,sK130)
| nn = null
| null = sK130
| ~ object(nn)
| ~ spl158_87
| ~ spl158_88 ),
inference(forward_subsumption_resolution,[],[f3034,f1349]) ).
fof(f3061,plain,
( v__1(sortedList_first,sK130,sK130)
| null = sK130
| ~ object(nn)
| ~ spl158_87
| ~ spl158_88 ),
inference(forward_subsumption_resolution,[],[f3039,f406]) ).
fof(f3077,definition,
( spl158_318
<=> sP76(nn) ),
introduced(definition,[new_symbols(definition,[spl158_318])],[avatar_definition]) ).
fof(f3079,plain,
( ~ sP76(nn)
| spl158_318 ),
inference(avatar_component_clause,[],[f3077]) ).
fof(f3481,plain,
( ~ object(nn)
| ~ object(prev_2)
| ~ object(sortedList_first)
| v__1(nn,prev_2,prev_2)
| ~ spl158_119 ),
inference(resolution,[],[f370,f1501]) ).
fof(f3535,plain,
( ~ object(prev_2)
| ~ object(sortedList_first)
| v__1(nn,prev_2,prev_2)
| ~ spl158_119 ),
inference(forward_subsumption_resolution,[],[f3481,f354]) ).
fof(f3557,plain,
( ~ object(sortedList_first)
| v__1(nn,prev_2,prev_2)
| ~ spl158_119 ),
inference(forward_subsumption_resolution,[],[f3535,f356]) ).
fof(f3577,plain,
( v__1(nn,prev_2,prev_2)
| ~ spl158_119 ),
inference(forward_subsumption_resolution,[],[f3557,f361]) ).
fof(f3603,plain,
( sP58(sK157)
| sP57(sK157)
| ~ sP76(sK157)
| spl158_12 ),
inference(resolution,[],[f986,f439]) ).
fof(f3605,definition,
( spl158_346
<=> sP57(sK157) ),
introduced(definition,[new_symbols(definition,[spl158_346])],[avatar_definition]) ).
fof(f3607,plain,
( sP57(sK157)
| ~ spl158_346 ),
inference(avatar_component_clause,[],[f3605]) ).
fof(f3609,definition,
( spl158_347
<=> sP58(sK157) ),
introduced(definition,[new_symbols(definition,[spl158_347])],[avatar_definition]) ).
fof(f3611,plain,
( sP58(sK157)
| ~ spl158_347 ),
inference(avatar_component_clause,[],[f3609]) ).
fof(f3612,plain,
( ~ spl158_5
| spl158_346
| spl158_347
| spl158_12 ),
inference(avatar_split_clause,[],[f3603,f985,f3609,f3605,f955]) ).
fof(f3798,plain,
( ~ object(prev_2)
| ~ object(nn)
| ~ object(null)
| v__1(null,prev_2,prev_2)
| ~ spl158_68 ),
inference(resolution,[],[f371,f1249]) ).
fof(f3855,plain,
( ~ object(nn)
| ~ object(null)
| v__1(null,prev_2,prev_2)
| ~ spl158_68 ),
inference(forward_subsumption_resolution,[],[f3798,f356]) ).
fof(f3871,plain,
( ~ object(null)
| v__1(null,prev_2,prev_2)
| ~ spl158_68 ),
inference(forward_subsumption_resolution,[],[f3855,f354]) ).
fof(f3887,plain,
( v__1(null,prev_2,prev_2)
| ~ spl158_68
| ~ spl158_260 ),
inference(forward_subsumption_resolution,[],[f3871,f2195]) ).
fof(f3888,plain,
( $false
| spl158_65
| ~ spl158_68
| ~ spl158_260 ),
inference(forward_subsumption_resolution,[],[f3887,f1237]) ).
fof(f3889,plain,
( spl158_65
| ~ spl158_68
| ~ spl158_260 ),
inference(avatar_contradiction_clause,[],[f3888]) ).
fof(f3939,plain,
( ~ object(prev_2)
| prev_2 = null
| ~ spl158_65
| ~ spl158_260 ),
inference(resolution,[],[f1236,f2309]) ).
fof(f3946,plain,
( prev_2 = null
| ~ spl158_65
| ~ spl158_260 ),
inference(forward_subsumption_resolution,[],[f3939,f356]) ).
fof(f3948,plain,
( $false
| ~ spl158_65
| ~ spl158_260
| spl158_266 ),
inference(forward_subsumption_resolution,[],[f3946,f2225]) ).
fof(f3949,plain,
( ~ spl158_65
| ~ spl158_260
| spl158_266 ),
inference(avatar_contradiction_clause,[],[f3948]) ).
fof(f4115,plain,
( $false
| ~ spl158_7
| ~ spl158_250 ),
inference(resolution,[],[f2146,f965]) ).
fof(f4116,plain,
( ~ spl158_7
| ~ spl158_250 ),
inference(avatar_contradiction_clause,[],[f4115]) ).
fof(f4117,plain,
( $false
| ~ spl158_8
| ~ spl158_251 ),
inference(forward_subsumption_resolution,[],[f969,f2154]) ).
fof(f4118,plain,
( ~ spl158_8
| ~ spl158_251 ),
inference(avatar_contradiction_clause,[],[f4117]) ).
fof(f4119,plain,
( $false
| ~ spl158_223
| ~ spl158_347 ),
inference(forward_subsumption_resolution,[],[f3611,f2005]) ).
fof(f4120,plain,
( ~ spl158_223
| ~ spl158_347 ),
inference(avatar_contradiction_clause,[],[f4119]) ).
fof(f4121,plain,
( $false
| ~ spl158_222
| ~ spl158_346 ),
inference(forward_subsumption_resolution,[],[f3607,f1997]) ).
fof(f4122,plain,
( ~ spl158_222
| ~ spl158_346 ),
inference(avatar_contradiction_clause,[],[f4121]) ).
fof(f4123,plain,
( sP35(sK157)
| ~ spl158_4 ),
inference(resolution,[],[f953,f431]) ).
fof(f4124,plain,
( sP34(sK157)
| ~ spl158_4 ),
inference(resolution,[],[f953,f430]) ).
fof(f4166,definition,
( spl158_355
<=> null = sK128 ),
introduced(definition,[new_symbols(definition,[spl158_355])],[avatar_definition]) ).
fof(f4168,plain,
( null != sK128
| spl158_355 ),
inference(avatar_component_clause,[],[f4166]) ).
fof(f4481,plain,
( ! [X0] :
( ~ object(X0)
| ~ object(prev_2)
| ~ v__1(sortedList_first,X0,X0)
| ~ object(sortedList_first)
| v__1(sortedList_first,X0,prev_2)
| v__1(sortedList_first,prev_2,X0) )
| ~ spl158_11 ),
inference(resolution,[],[f369,f982]) ).
fof(f4507,plain,
( ! [X0] :
( ~ object(X0)
| ~ v__1(sortedList_first,X0,X0)
| ~ object(sortedList_first)
| v__1(sortedList_first,X0,prev_2)
| v__1(sortedList_first,prev_2,X0) )
| ~ spl158_11 ),
inference(forward_subsumption_resolution,[],[f4481,f356]) ).
fof(f4540,plain,
( ! [X0] :
( ~ v__1(sortedList_first,X0,X0)
| ~ object(X0)
| v__1(sortedList_first,X0,prev_2)
| v__1(sortedList_first,prev_2,X0) )
| ~ spl158_11 ),
inference(forward_subsumption_resolution,[],[f4507,f361]) ).
fof(f4637,plain,
( ! [X0] :
( ~ sP25(X0)
| ~ object(X0)
| null = X0 )
| ~ spl158_260 ),
inference(resolution,[],[f728,f2309]) ).
fof(f4688,plain,
( ~ object(nn)
| v__1(sortedList_first,nn,prev_2)
| v__1(sortedList_first,prev_2,nn)
| ~ spl158_9
| ~ spl158_11 ),
inference(resolution,[],[f4540,f972]) ).
fof(f4724,plain,
! [X0] :
( node_key(X0) != sK78
| ~ object(X0)
| ~ v__1(sortedList_first,nn,nn)
| nn = null
| ~ object(node_next(nn))
| ~ v__1(node_next(nn),X0,X0)
| null = X0
| ~ integer(sK78)
| ~ object(nn) ),
inference(superposition,[],[f893,f379]) ).
fof(f4726,plain,
! [X0] :
( node_key(X0) != sK78
| ~ object(nn)
| ~ v__1(sortedList_first,X0,X0)
| null = X0
| ~ object(node_next(X0))
| ~ v__1(node_next(X0),nn,nn)
| nn = null
| ~ integer(node_key(X0))
| ~ object(X0) ),
inference(superposition,[],[f893,f379]) ).
fof(f4727,plain,
! [X0] :
( ~ object(X0)
| ~ v__1(sortedList_first,X0,X0)
| null = X0
| ~ object(node_next(X0))
| ~ v__1(node_next(X0),X0,X0)
| null = X0
| ~ integer(node_key(X0))
| ~ object(X0) ),
inference(equality_resolution,[],[f893]) ).
fof(f4728,plain,
! [X0] :
( ~ object(X0)
| ~ v__1(sortedList_first,X0,X0)
| null = X0
| ~ object(node_next(X0))
| ~ v__1(node_next(X0),X0,X0)
| ~ integer(node_key(X0)) ),
inference(duplicate_literal_removal,[],[f4727]) ).
fof(f4729,plain,
! [X0] :
( ~ object(X0)
| ~ v__1(sortedList_first,X0,X0)
| null = X0
| ~ v__1(node_next(X0),X0,X0)
| ~ integer(node_key(X0)) ),
inference(forward_subsumption_resolution,[],[f4728,f362]) ).
fof(f4730,plain,
! [X0] :
( node_key(X0) != sK78
| ~ v__1(sortedList_first,X0,X0)
| null = X0
| ~ object(node_next(X0))
| ~ v__1(node_next(X0),nn,nn)
| nn = null
| ~ integer(node_key(X0))
| ~ object(X0) ),
inference(forward_subsumption_resolution,[],[f4726,f354]) ).
fof(f4732,plain,
( ! [X0] :
( node_key(X0) != sK78
| ~ object(X0)
| nn = null
| ~ object(node_next(nn))
| ~ v__1(node_next(nn),X0,X0)
| null = X0
| ~ integer(sK78)
| ~ object(nn) )
| ~ spl158_9 ),
inference(forward_subsumption_resolution,[],[f4724,f972]) ).
fof(f4734,plain,
! [X0] :
( ~ v__1(node_next(X0),X0,X0)
| ~ v__1(sortedList_first,X0,X0)
| null = X0
| ~ object(X0) ),
inference(forward_subsumption_resolution,[],[f4729,f358]) ).
fof(f4735,plain,
! [X0] :
( node_key(X0) != sK78
| ~ v__1(sortedList_first,X0,X0)
| null = X0
| ~ object(node_next(X0))
| ~ v__1(node_next(X0),nn,nn)
| ~ integer(node_key(X0))
| ~ object(X0) ),
inference(forward_subsumption_resolution,[],[f4730,f406]) ).
fof(f4737,plain,
( ! [X0] :
( node_key(X0) != sK78
| ~ object(X0)
| ~ object(node_next(nn))
| ~ v__1(node_next(nn),X0,X0)
| null = X0
| ~ integer(sK78)
| ~ object(nn) )
| ~ spl158_9 ),
inference(forward_subsumption_resolution,[],[f4732,f406]) ).
fof(f4739,plain,
! [X0] :
( node_key(X0) != sK78
| ~ v__1(sortedList_first,X0,X0)
| null = X0
| ~ v__1(node_next(X0),nn,nn)
| ~ integer(node_key(X0))
| ~ object(X0) ),
inference(forward_subsumption_resolution,[],[f4735,f362]) ).
fof(f4741,plain,
( ! [X0] :
( node_key(X0) != sK78
| ~ object(X0)
| ~ v__1(node_next(nn),X0,X0)
| null = X0
| ~ integer(sK78)
| ~ object(nn) )
| ~ spl158_9 ),
inference(forward_subsumption_resolution,[],[f4737,f362]) ).
fof(f4743,plain,
! [X0] :
( node_key(X0) != sK78
| ~ v__1(sortedList_first,X0,X0)
| null = X0
| ~ v__1(node_next(X0),nn,nn)
| ~ object(X0) ),
inference(forward_subsumption_resolution,[],[f4739,f358]) ).
fof(f4745,plain,
( ! [X0] :
( node_key(X0) != sK78
| ~ object(X0)
| ~ v__1(node_next(nn),X0,X0)
| null = X0
| ~ object(nn) )
| ~ spl158_9 ),
inference(forward_subsumption_resolution,[],[f4741,f382]) ).
fof(f4748,plain,
( ! [X0] :
( node_key(X0) != sK78
| ~ object(X0)
| ~ v__1(node_next(nn),X0,X0)
| null = X0 )
| ~ spl158_9 ),
inference(forward_subsumption_resolution,[],[f4745,f354]) ).
fof(f4771,plain,
( ~ v__1(sK149,nn,nn)
| ~ v__1(sortedList_first,nn,nn)
| nn = null
| ~ object(nn)
| ~ spl158_44 ),
inference(superposition,[],[f4734,f1142]) ).
fof(f4777,plain,
( ~ v__1(nn,prev_2,prev_2)
| ~ v__1(sortedList_first,prev_2,prev_2)
| prev_2 = null
| ~ object(prev_2)
| ~ spl158_265 ),
inference(superposition,[],[f4734,f2222]) ).
fof(f4781,plain,
( ~ v__1(sortedList_first,prev_2,prev_2)
| prev_2 = null
| ~ object(prev_2)
| ~ spl158_119
| ~ spl158_265 ),
inference(forward_subsumption_resolution,[],[f4777,f3577]) ).
fof(f4786,plain,
( ~ v__1(sK149,nn,nn)
| nn = null
| ~ object(nn)
| ~ spl158_9
| ~ spl158_44 ),
inference(forward_subsumption_resolution,[],[f4771,f972]) ).
fof(f4790,plain,
( prev_2 = null
| ~ object(prev_2)
| ~ spl158_11
| ~ spl158_119
| ~ spl158_265 ),
inference(forward_subsumption_resolution,[],[f4781,f982]) ).
fof(f4795,plain,
( ~ v__1(sK149,nn,nn)
| ~ object(nn)
| ~ spl158_9
| ~ spl158_44 ),
inference(forward_subsumption_resolution,[],[f4786,f406]) ).
fof(f4799,plain,
( ~ object(prev_2)
| ~ spl158_11
| ~ spl158_119
| ~ spl158_265
| spl158_266 ),
inference(forward_subsumption_resolution,[],[f4790,f2225]) ).
fof(f4804,plain,
( ~ v__1(sK149,nn,nn)
| ~ spl158_9
| ~ spl158_44 ),
inference(forward_subsumption_resolution,[],[f4795,f354]) ).
fof(f4807,plain,
( $false
| ~ spl158_11
| ~ spl158_119
| ~ spl158_265
| spl158_266 ),
inference(forward_subsumption_resolution,[],[f4799,f356]) ).
fof(f4808,plain,
( ~ spl158_11
| ~ spl158_119
| ~ spl158_265
| spl158_266 ),
inference(avatar_contradiction_clause,[],[f4807]) ).
fof(f4898,plain,
( sP58(nn)
| sP57(nn)
| ~ sP76(nn)
| spl158_119 ),
inference(resolution,[],[f1500,f439]) ).
fof(f4900,plain,
( sP57(nn)
| ~ sP76(nn)
| spl158_119
| ~ spl158_223 ),
inference(forward_subsumption_resolution,[],[f4898,f2005]) ).
fof(f4901,plain,
( ~ sP76(nn)
| spl158_119
| ~ spl158_222
| ~ spl158_223 ),
inference(forward_subsumption_resolution,[],[f4900,f1997]) ).
fof(f4902,plain,
( ~ spl158_318
| spl158_119
| ~ spl158_222
| ~ spl158_223 ),
inference(avatar_split_clause,[],[f4901,f2004,f1996,f1499,f3077]) ).
fof(f6357,plain,
( sK129 = sK130
| ~ spl158_87
| ~ spl158_89 ),
inference(superposition,[],[f1354,f1344]) ).
fof(f6377,plain,
( ~ v__1(sK129,nn,nn)
| ~ v__1(sortedList_first,nn,nn)
| nn = null
| ~ object(nn)
| ~ spl158_89 ),
inference(superposition,[],[f4734,f1354]) ).
fof(f6378,plain,
( ~ v__1(sK129,nn,nn)
| nn = null
| ~ object(nn)
| ~ spl158_9
| ~ spl158_89 ),
inference(forward_subsumption_resolution,[],[f6377,f972]) ).
fof(f6400,plain,
( ~ v__1(sK129,nn,nn)
| ~ object(nn)
| ~ spl158_9
| ~ spl158_89 ),
inference(forward_subsumption_resolution,[],[f6378,f406]) ).
fof(f6412,plain,
( ~ v__1(sK129,nn,nn)
| ~ spl158_9
| ~ spl158_89 ),
inference(forward_subsumption_resolution,[],[f6400,f354]) ).
fof(f6427,plain,
( ! [X0] :
( ~ sP34(X0)
| sP18(X0)
| sP19(X0) )
| ~ spl158_100
| ~ spl158_134 ),
inference(forward_subsumption_resolution,[],[f1571,f1410]) ).
fof(f6428,plain,
( ! [X0] :
( ~ sP34(X0)
| sP19(X0) )
| ~ spl158_92
| ~ spl158_100
| ~ spl158_134 ),
inference(forward_subsumption_resolution,[],[f6427,f1368]) ).
fof(f6429,plain,
( ! [X0] : ~ sP34(X0)
| ~ spl158_92
| ~ spl158_96
| ~ spl158_100
| ~ spl158_134 ),
inference(forward_subsumption_resolution,[],[f6428,f1389]) ).
fof(f8022,plain,
( ! [X0] :
( ~ v__1(nn,X0,X0)
| ~ object(X0)
| ~ v__1(sortedList_first,prev_2,prev_2)
| prev_2 = null
| ~ object(nn)
| ~ object(prev_2)
| null = X0
| ~ integer(node_key(prev_2))
| ~ integer(node_key(X0))
| lteq(node_key(prev_2),node_key(X0)) )
| ~ spl158_265 ),
inference(superposition,[],[f891,f2222]) ).
fof(f8036,plain,
( ! [X0] :
( ~ v__1(nn,X0,X0)
| ~ object(X0)
| prev_2 = null
| ~ object(nn)
| ~ object(prev_2)
| null = X0
| ~ integer(node_key(prev_2))
| ~ integer(node_key(X0))
| lteq(node_key(prev_2),node_key(X0)) )
| ~ spl158_11
| ~ spl158_265 ),
inference(forward_subsumption_resolution,[],[f8022,f982]) ).
fof(f8056,plain,
( ! [X0] :
( ~ v__1(nn,X0,X0)
| ~ object(X0)
| ~ object(nn)
| ~ object(prev_2)
| null = X0
| ~ integer(node_key(prev_2))
| ~ integer(node_key(X0))
| lteq(node_key(prev_2),node_key(X0)) )
| ~ spl158_11
| ~ spl158_265
| spl158_266 ),
inference(forward_subsumption_resolution,[],[f8036,f2225]) ).
fof(f8076,plain,
( ! [X0] :
( ~ v__1(nn,X0,X0)
| ~ object(X0)
| ~ object(prev_2)
| null = X0
| ~ integer(node_key(prev_2))
| ~ integer(node_key(X0))
| lteq(node_key(prev_2),node_key(X0)) )
| ~ spl158_11
| ~ spl158_265
| spl158_266 ),
inference(forward_subsumption_resolution,[],[f8056,f354]) ).
fof(f8096,plain,
( ! [X0] :
( ~ v__1(nn,X0,X0)
| ~ object(X0)
| null = X0
| ~ integer(node_key(prev_2))
| ~ integer(node_key(X0))
| lteq(node_key(prev_2),node_key(X0)) )
| ~ spl158_11
| ~ spl158_265
| spl158_266 ),
inference(forward_subsumption_resolution,[],[f8076,f356]) ).
fof(f8116,plain,
( ! [X0] :
( ~ v__1(nn,X0,X0)
| ~ object(X0)
| null = X0
| ~ integer(node_key(prev_2))
| lteq(node_key(prev_2),node_key(X0)) )
| ~ spl158_11
| ~ spl158_265
| spl158_266 ),
inference(forward_subsumption_resolution,[],[f8096,f358]) ).
fof(f8135,plain,
( ! [X0] :
( ~ v__1(nn,X0,X0)
| ~ object(X0)
| null = X0
| lteq(node_key(prev_2),node_key(X0)) )
| ~ spl158_11
| ~ spl158_265
| spl158_266 ),
inference(forward_subsumption_resolution,[],[f8116,f358]) ).
fof(f8180,plain,
( ~ object(nn)
| nn = null
| lteq(node_key(prev_2),node_key(nn))
| ~ spl158_11
| ~ spl158_265
| spl158_266
| ~ spl158_269 ),
inference(resolution,[],[f8135,f2246]) ).
fof(f8201,plain,
( nn = null
| lteq(node_key(prev_2),node_key(nn))
| ~ spl158_11
| ~ spl158_265
| spl158_266
| ~ spl158_269 ),
inference(forward_subsumption_resolution,[],[f8180,f354]) ).
fof(f8204,plain,
( lteq(node_key(prev_2),node_key(nn))
| ~ spl158_11
| ~ spl158_265
| spl158_266
| ~ spl158_269 ),
inference(forward_subsumption_resolution,[],[f8201,f406]) ).
fof(f8207,plain,
( lteq(node_key(prev_2),sK79)
| ~ spl158_11
| ~ spl158_265
| spl158_266
| ~ spl158_269 ),
inference(forward_demodulation,[],[f8204,f378]) ).
fof(f8209,plain,
( lteq(node_key(prev_2),sK78)
| ~ spl158_11
| ~ spl158_265
| spl158_266
| ~ spl158_269 ),
inference(forward_demodulation,[],[f8207,f2249]) ).
fof(f8218,definition,
( spl158_425
<=> sK78 = node_key(prev_2) ),
introduced(definition,[new_symbols(definition,[spl158_425])],[avatar_definition]) ).
fof(f8220,plain,
( sK78 = node_key(prev_2)
| ~ spl158_425 ),
inference(avatar_component_clause,[],[f8218]) ).
fof(f8222,definition,
( spl158_426
<=> lteq(sK78,node_key(prev_2)) ),
introduced(definition,[new_symbols(definition,[spl158_426])],[avatar_definition]) ).
fof(f8223,plain,
( lteq(sK78,node_key(prev_2))
| ~ spl158_426 ),
inference(avatar_component_clause,[],[f8222]) ).
fof(f8224,plain,
( ~ lteq(sK78,node_key(prev_2))
| spl158_426 ),
inference(avatar_component_clause,[],[f8222]) ).
fof(f8533,definition,
( spl158_432
<=> sP25(sK157) ),
introduced(definition,[new_symbols(definition,[spl158_432])],[avatar_definition]) ).
fof(f8534,plain,
( ~ sP25(sK157)
| spl158_432 ),
inference(avatar_component_clause,[],[f8533]) ).
fof(f8535,plain,
( sP25(sK157)
| ~ spl158_432 ),
inference(avatar_component_clause,[],[f8533]) ).
fof(f8537,definition,
( spl158_433
<=> sP26(sK157) ),
introduced(definition,[new_symbols(definition,[spl158_433])],[avatar_definition]) ).
fof(f8538,plain,
( ~ sP26(sK157)
| spl158_433 ),
inference(avatar_component_clause,[],[f8537]) ).
fof(f8539,plain,
( sP26(sK157)
| ~ spl158_433 ),
inference(avatar_component_clause,[],[f8537]) ).
fof(f8541,definition,
( spl158_434
<=> null = sK113(sK157) ),
introduced(definition,[new_symbols(definition,[spl158_434])],[avatar_definition]) ).
fof(f8542,plain,
( null != sK113(sK157)
| spl158_434 ),
inference(avatar_component_clause,[],[f8541]) ).
fof(f8543,plain,
( null = sK113(sK157)
| ~ spl158_434 ),
inference(avatar_component_clause,[],[f8541]) ).
fof(f8546,plain,
( ~ object(sK157)
| null = sK157
| ~ spl158_260
| ~ spl158_432 ),
inference(resolution,[],[f8535,f4637]) ).
fof(f8547,plain,
( null = sK157
| ~ spl158_260
| ~ spl158_432 ),
inference(forward_subsumption_resolution,[],[f8546,f878]) ).
fof(f8549,plain,
( $false
| spl158_3
| ~ spl158_260
| ~ spl158_432 ),
inference(forward_subsumption_resolution,[],[f8547,f947]) ).
fof(f8550,plain,
( spl158_3
| ~ spl158_260
| ~ spl158_432 ),
inference(avatar_contradiction_clause,[],[f8549]) ).
fof(f10263,plain,
( v__1(null,sK157,sK157)
| sP26(sK157)
| sP25(sK157)
| ~ sP35(sK157)
| ~ spl158_434 ),
inference(superposition,[],[f672,f8543]) ).
fof(f10266,plain,
( v__1(null,sK157,sK157)
| sP26(sK157)
| ~ sP35(sK157)
| ~ spl158_434 ),
inference(forward_subsumption_resolution,[],[f10263,f728]) ).
fof(f10273,plain,
( v__1(null,sK157,sK157)
| sP26(sK157)
| ~ spl158_4
| ~ spl158_434 ),
inference(forward_subsumption_resolution,[],[f10266,f4123]) ).
fof(f10278,definition,
( spl158_467
<=> v__1(null,sK157,sK157) ),
introduced(definition,[new_symbols(definition,[spl158_467])],[avatar_definition]) ).
fof(f10279,plain,
( ~ v__1(null,sK157,sK157)
| spl158_467 ),
inference(avatar_component_clause,[],[f10278]) ).
fof(f10280,plain,
( v__1(null,sK157,sK157)
| ~ spl158_467 ),
inference(avatar_component_clause,[],[f10278]) ).
fof(f10281,plain,
( spl158_433
| spl158_467
| ~ spl158_4
| ~ spl158_434 ),
inference(avatar_split_clause,[],[f10273,f8541,f951,f10278,f8537]) ).
fof(f10311,plain,
( ~ object(sK157)
| null = sK157
| ~ spl158_260
| ~ spl158_467 ),
inference(resolution,[],[f10280,f2309]) ).
fof(f10324,plain,
( null = sK157
| ~ spl158_260
| ~ spl158_467 ),
inference(forward_subsumption_resolution,[],[f10311,f878]) ).
fof(f10332,plain,
( $false
| spl158_3
| ~ spl158_260
| ~ spl158_467 ),
inference(forward_subsumption_resolution,[],[f10324,f947]) ).
fof(f10333,plain,
( spl158_3
| ~ spl158_260
| ~ spl158_467 ),
inference(avatar_contradiction_clause,[],[f10332]) ).
fof(f10392,plain,
( v__1(sortedList_first,nn,prev_2)
| v__1(sortedList_first,prev_2,nn)
| ~ spl158_9
| ~ spl158_11 ),
inference(forward_subsumption_resolution,[],[f4688,f354]) ).
fof(f10421,plain,
( v__1(sortedList_first,prev_2,nn)
| ~ spl158_9
| ~ spl158_11
| spl158_119 ),
inference(forward_subsumption_resolution,[],[f10392,f1500]) ).
fof(f10472,plain,
( $false
| ~ spl158_4
| ~ spl158_92
| ~ spl158_96
| ~ spl158_100
| ~ spl158_134 ),
inference(forward_subsumption_resolution,[],[f4124,f6429]) ).
fof(f10473,plain,
( ~ spl158_4
| ~ spl158_92
| ~ spl158_96
| ~ spl158_100
| ~ spl158_134 ),
inference(avatar_contradiction_clause,[],[f10472]) ).
fof(f10482,plain,
( ~ object(prev_2)
| ~ object(nn)
| ~ object(sK116)
| v__1(sK116,prev_2,prev_2)
| ~ spl158_136 ),
inference(resolution,[],[f1580,f371]) ).
fof(f10484,plain,
( ~ object(nn)
| ~ object(sK116)
| v__1(sK116,prev_2,prev_2)
| ~ spl158_136 ),
inference(forward_subsumption_resolution,[],[f10482,f356]) ).
fof(f10485,plain,
( ~ object(sK116)
| v__1(sK116,prev_2,prev_2)
| ~ spl158_136 ),
inference(forward_subsumption_resolution,[],[f10484,f354]) ).
fof(f10486,plain,
( v__1(sK116,prev_2,prev_2)
| ~ spl158_136
| ~ spl158_137 ),
inference(forward_subsumption_resolution,[],[f10485,f1585]) ).
fof(f10675,plain,
( sP26(sK157)
| sP25(sK157)
| node_next(nn) = sK113(sK157)
| ~ spl158_4 ),
inference(resolution,[],[f4123,f671]) ).
fof(f10695,plain,
( v__1(null,sK157,nn)
| ~ sP26(sK157)
| spl158_467 ),
inference(resolution,[],[f10279,f720]) ).
fof(f10716,definition,
( spl158_501
<=> v__1(null,sK157,nn) ),
introduced(definition,[new_symbols(definition,[spl158_501])],[avatar_definition]) ).
fof(f10718,plain,
( v__1(null,sK157,nn)
| ~ spl158_501 ),
inference(avatar_component_clause,[],[f10716]) ).
fof(f10720,plain,
( v__1(null,sK157,nn)
| ~ spl158_433
| spl158_467 ),
inference(forward_subsumption_resolution,[],[f10695,f8539]) ).
fof(f10738,plain,
( spl158_501
| ~ spl158_433
| spl158_467 ),
inference(avatar_split_clause,[],[f10720,f10278,f8537,f10716]) ).
fof(f10743,plain,
( ~ object(sK157)
| ~ object(nn)
| ~ object(null)
| v__1(null,sK157,sK157)
| ~ spl158_501 ),
inference(resolution,[],[f10718,f371]) ).
fof(f10746,plain,
( ~ object(nn)
| ~ object(null)
| v__1(null,sK157,sK157)
| ~ spl158_501 ),
inference(forward_subsumption_resolution,[],[f10743,f878]) ).
fof(f10748,plain,
( ~ object(null)
| v__1(null,sK157,sK157)
| ~ spl158_501 ),
inference(forward_subsumption_resolution,[],[f10746,f354]) ).
fof(f10750,plain,
( v__1(null,sK157,sK157)
| ~ spl158_260
| ~ spl158_501 ),
inference(forward_subsumption_resolution,[],[f10748,f2195]) ).
fof(f10751,plain,
( $false
| ~ spl158_260
| spl158_467
| ~ spl158_501 ),
inference(forward_subsumption_resolution,[],[f10750,f10279]) ).
fof(f10752,plain,
( ~ spl158_260
| spl158_467
| ~ spl158_501 ),
inference(avatar_contradiction_clause,[],[f10751]) ).
fof(f10754,plain,
( sP25(sK157)
| node_next(nn) = sK113(sK157)
| ~ spl158_4
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f10675,f8538]) ).
fof(f10817,plain,
( node_next(nn) = sK113(sK157)
| ~ spl158_4
| spl158_432
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f10754,f8534]) ).
fof(f10840,plain,
( sK149 = sK113(sK157)
| ~ spl158_4
| ~ spl158_44
| spl158_432
| spl158_433 ),
inference(forward_demodulation,[],[f10817,f1142]) ).
fof(f10843,plain,
( null = sK113(sK157)
| ~ spl158_4
| ~ spl158_44
| ~ spl158_272
| spl158_432
| spl158_433 ),
inference(forward_demodulation,[],[f10840,f2347]) ).
fof(f10845,plain,
( $false
| ~ spl158_4
| ~ spl158_44
| ~ spl158_272
| spl158_432
| spl158_433
| spl158_434 ),
inference(forward_subsumption_resolution,[],[f10843,f8542]) ).
fof(f10846,plain,
( ~ spl158_4
| ~ spl158_44
| ~ spl158_272
| spl158_432
| spl158_433
| spl158_434 ),
inference(avatar_contradiction_clause,[],[f10845]) ).
fof(f11615,plain,
( spl158_10
| ~ spl158_9
| ~ spl158_11
| spl158_119 ),
inference(avatar_split_clause,[],[f10421,f1499,f980,f971,f975]) ).
fof(f11663,plain,
( ~ object(sK157)
| ~ object(prev_2)
| ~ object(sortedList_first)
| v__1(sortedList_first,sK157,sK157)
| ~ spl158_12 ),
inference(resolution,[],[f987,f371]) ).
fof(f11665,plain,
( ~ object(prev_2)
| ~ object(sortedList_first)
| v__1(sortedList_first,sK157,sK157)
| ~ spl158_12 ),
inference(forward_subsumption_resolution,[],[f11663,f878]) ).
fof(f11666,plain,
( ~ object(sortedList_first)
| v__1(sortedList_first,sK157,sK157)
| ~ spl158_12 ),
inference(forward_subsumption_resolution,[],[f11665,f356]) ).
fof(f11667,plain,
( v__1(sortedList_first,sK157,sK157)
| ~ spl158_12 ),
inference(forward_subsumption_resolution,[],[f11666,f361]) ).
fof(f11668,plain,
( $false
| spl158_2
| ~ spl158_12 ),
inference(forward_subsumption_resolution,[],[f11667,f944]) ).
fof(f11669,plain,
( spl158_2
| ~ spl158_12 ),
inference(avatar_contradiction_clause,[],[f11668]) ).
fof(f11721,plain,
( sP76(nn)
| ~ spl158_1
| ~ spl158_5 ),
inference(superposition,[],[f957,f940]) ).
fof(f11722,plain,
( v__1(sortedList_first,nn,prev_2)
| ~ spl158_1
| ~ spl158_12 ),
inference(superposition,[],[f987,f940]) ).
fof(f11730,plain,
( $false
| ~ spl158_1
| ~ spl158_12
| spl158_119 ),
inference(forward_subsumption_resolution,[],[f11722,f1500]) ).
fof(f11731,plain,
( ~ spl158_1
| ~ spl158_12
| spl158_119 ),
inference(avatar_contradiction_clause,[],[f11730]) ).
fof(f11732,plain,
( $false
| ~ spl158_1
| ~ spl158_5
| spl158_318 ),
inference(forward_subsumption_resolution,[],[f11721,f3079]) ).
fof(f11733,plain,
( ~ spl158_1
| ~ spl158_5
| spl158_318 ),
inference(avatar_contradiction_clause,[],[f11732]) ).
fof(f11735,plain,
( sP35(nn)
| ~ spl158_1
| ~ spl158_4 ),
inference(forward_demodulation,[],[f4123,f940]) ).
fof(f11737,plain,
( sK149 = sK113(nn)
| ~ spl158_1
| ~ spl158_4
| ~ spl158_44
| spl158_432
| spl158_433 ),
inference(forward_demodulation,[],[f10840,f940]) ).
fof(f11757,plain,
( v__1(sortedList_first,sK130,sK130)
| null = sK130
| ~ spl158_87
| ~ spl158_88 ),
inference(forward_subsumption_resolution,[],[f3061,f354]) ).
fof(f12044,plain,
( ~ integer(node_key(prev_2))
| ~ lteq(sK78,node_key(prev_2))
| ~ integer(sK78)
| sK78 = node_key(prev_2)
| ~ spl158_11
| ~ spl158_265
| spl158_266
| ~ spl158_269 ),
inference(resolution,[],[f8209,f884]) ).
fof(f12045,plain,
( ~ lteq(sK78,node_key(prev_2))
| ~ integer(sK78)
| sK78 = node_key(prev_2)
| ~ spl158_11
| ~ spl158_265
| spl158_266
| ~ spl158_269 ),
inference(forward_subsumption_resolution,[],[f12044,f358]) ).
fof(f12047,plain,
( ~ integer(sK78)
| sK78 = node_key(prev_2)
| ~ spl158_11
| ~ spl158_265
| spl158_266
| ~ spl158_269
| ~ spl158_426 ),
inference(forward_subsumption_resolution,[],[f12045,f8223]) ).
fof(f12049,plain,
( sK78 = node_key(prev_2)
| ~ spl158_11
| ~ spl158_265
| spl158_266
| ~ spl158_269
| ~ spl158_426 ),
inference(forward_subsumption_resolution,[],[f12047,f382]) ).
fof(f12050,plain,
( spl158_425
| ~ spl158_11
| ~ spl158_265
| spl158_266
| ~ spl158_269
| ~ spl158_426 ),
inference(avatar_split_clause,[],[f12049,f8222,f2244,f2224,f2220,f980,f8218]) ).
fof(f12322,plain,
( sK78 != sK78
| ~ v__1(sortedList_first,prev_2,prev_2)
| prev_2 = null
| ~ v__1(node_next(prev_2),nn,nn)
| ~ object(prev_2)
| ~ spl158_425 ),
inference(superposition,[],[f4743,f8220]) ).
fof(f12327,plain,
( ~ v__1(sortedList_first,prev_2,prev_2)
| prev_2 = null
| ~ v__1(node_next(prev_2),nn,nn)
| ~ object(prev_2)
| ~ spl158_425 ),
inference(trivial_inequality_removal,[],[f12322]) ).
fof(f12331,plain,
( prev_2 = null
| ~ v__1(node_next(prev_2),nn,nn)
| ~ object(prev_2)
| ~ spl158_11
| ~ spl158_425 ),
inference(forward_subsumption_resolution,[],[f12327,f982]) ).
fof(f12334,plain,
( ~ v__1(node_next(prev_2),nn,nn)
| ~ object(prev_2)
| ~ spl158_11
| spl158_266
| ~ spl158_425 ),
inference(forward_subsumption_resolution,[],[f12331,f2225]) ).
fof(f12337,plain,
( ~ v__1(node_next(prev_2),nn,nn)
| ~ spl158_11
| spl158_266
| ~ spl158_425 ),
inference(forward_subsumption_resolution,[],[f12334,f356]) ).
fof(f12340,plain,
( ~ v__1(nn,nn,nn)
| ~ spl158_11
| ~ spl158_265
| spl158_266
| ~ spl158_425 ),
inference(forward_demodulation,[],[f12337,f2222]) ).
fof(f12342,plain,
( $false
| ~ spl158_11
| ~ spl158_265
| spl158_266
| ~ spl158_269
| ~ spl158_425 ),
inference(forward_subsumption_resolution,[],[f12340,f2246]) ).
fof(f12343,plain,
( ~ spl158_11
| ~ spl158_265
| spl158_266
| ~ spl158_269
| ~ spl158_425 ),
inference(avatar_contradiction_clause,[],[f12342]) ).
fof(f13193,plain,
( v__1(sK149,nn,nn)
| sP26(nn)
| sP25(nn)
| ~ sP35(nn)
| ~ spl158_1
| ~ spl158_4
| ~ spl158_44
| spl158_432
| spl158_433 ),
inference(superposition,[],[f672,f11737]) ).
fof(f13194,plain,
( v__1(sK149,nn,nn)
| sP25(nn)
| ~ sP35(nn)
| ~ spl158_1
| ~ spl158_4
| ~ spl158_44
| spl158_432
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f13193,f919]) ).
fof(f13195,plain,
( v__1(sK149,nn,nn)
| ~ sP35(nn)
| ~ spl158_1
| ~ spl158_4
| ~ spl158_44
| spl158_432
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f13194,f920]) ).
fof(f13196,plain,
( v__1(sK149,nn,nn)
| ~ spl158_1
| ~ spl158_4
| ~ spl158_44
| spl158_432
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f13195,f11735]) ).
fof(f13334,definition,
( spl158_603
<=> null = sK130 ),
introduced(definition,[new_symbols(definition,[spl158_603])],[avatar_definition]) ).
fof(f13336,plain,
( null = sK130
| ~ spl158_603 ),
inference(avatar_component_clause,[],[f13334]) ).
fof(f13338,definition,
( spl158_604
<=> v__1(sortedList_first,sK130,sK130) ),
introduced(definition,[new_symbols(definition,[spl158_604])],[avatar_definition]) ).
fof(f13340,plain,
( v__1(sortedList_first,sK130,sK130)
| ~ spl158_604 ),
inference(avatar_component_clause,[],[f13338]) ).
fof(f13341,plain,
( spl158_603
| spl158_604
| ~ spl158_87
| ~ spl158_88 ),
inference(avatar_split_clause,[],[f11757,f1347,f1342,f13338,f13334]) ).
fof(f13471,plain,
( $false
| ~ spl158_1
| ~ spl158_4
| ~ spl158_9
| ~ spl158_44
| spl158_432
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f13196,f4804]) ).
fof(f13472,plain,
( ~ spl158_1
| ~ spl158_4
| ~ spl158_9
| ~ spl158_44
| spl158_432
| spl158_433 ),
inference(avatar_contradiction_clause,[],[f13471]) ).
fof(f13795,plain,
( v__1(sK149,sK157,sK157)
| sP26(sK157)
| sP25(sK157)
| ~ sP35(sK157)
| ~ spl158_4
| ~ spl158_44
| spl158_432
| spl158_433 ),
inference(superposition,[],[f672,f10840]) ).
fof(f13796,plain,
( v__1(sK149,sK157,sK157)
| sP25(sK157)
| ~ sP35(sK157)
| ~ spl158_4
| ~ spl158_44
| spl158_432
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f13795,f8538]) ).
fof(f13797,plain,
( v__1(sK149,sK157,sK157)
| ~ sP35(sK157)
| ~ spl158_4
| ~ spl158_44
| spl158_432
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f13796,f8534]) ).
fof(f13798,plain,
( v__1(sK149,sK157,sK157)
| ~ spl158_4
| ~ spl158_44
| spl158_432
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f13797,f4123]) ).
fof(f13800,plain,
( ! [X0] :
( ~ object(sK149)
| ~ object(sK157)
| ~ v__1(X0,sK149,sK149)
| ~ object(X0)
| v__1(X0,sK157,sK157) )
| ~ spl158_4
| ~ spl158_44
| spl158_432
| spl158_433 ),
inference(resolution,[],[f13798,f364]) ).
fof(f13809,plain,
( ! [X0] :
( ~ object(sK157)
| ~ v__1(X0,sK149,sK149)
| ~ object(X0)
| v__1(X0,sK157,sK157) )
| ~ spl158_4
| ~ spl158_44
| ~ spl158_45
| spl158_432
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f13800,f1147]) ).
fof(f13813,plain,
( ! [X0] :
( ~ v__1(X0,sK149,sK149)
| ~ object(X0)
| v__1(X0,sK157,sK157) )
| ~ spl158_4
| ~ spl158_44
| ~ spl158_45
| spl158_432
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f13809,f878]) ).
fof(f14062,plain,
( ~ object(sortedList_first)
| v__1(sortedList_first,sK157,sK157)
| ~ spl158_4
| ~ spl158_44
| ~ spl158_45
| ~ spl158_273
| spl158_432
| spl158_433 ),
inference(resolution,[],[f13813,f2351]) ).
fof(f14132,plain,
( v__1(sortedList_first,sK157,sK157)
| ~ spl158_4
| ~ spl158_44
| ~ spl158_45
| ~ spl158_273
| spl158_432
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f14062,f361]) ).
fof(f14204,plain,
( $false
| spl158_2
| ~ spl158_4
| ~ spl158_44
| ~ spl158_45
| ~ spl158_273
| spl158_432
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f14132,f944]) ).
fof(f14205,plain,
( spl158_2
| ~ spl158_4
| ~ spl158_44
| ~ spl158_45
| ~ spl158_273
| spl158_432
| spl158_433 ),
inference(avatar_contradiction_clause,[],[f14204]) ).
fof(f14388,plain,
( v__1(sortedList_first,sK128,sK128)
| ~ object(sK128)
| nn = null
| null = sK128
| ~ object(nn)
| ~ spl158_94 ),
inference(superposition,[],[f895,f1380]) ).
fof(f14393,plain,
( ~ v__1(sK128,nn,nn)
| ~ v__1(sortedList_first,nn,nn)
| nn = null
| ~ object(nn)
| ~ spl158_94 ),
inference(superposition,[],[f4734,f1380]) ).
fof(f14395,plain,
( ~ v__1(sK128,nn,nn)
| nn = null
| ~ object(nn)
| ~ spl158_9
| ~ spl158_94 ),
inference(forward_subsumption_resolution,[],[f14393,f972]) ).
fof(f14398,plain,
( v__1(sortedList_first,sK128,sK128)
| nn = null
| null = sK128
| ~ object(nn)
| ~ spl158_94
| ~ spl158_95 ),
inference(forward_subsumption_resolution,[],[f14388,f1385]) ).
fof(f14400,plain,
( ~ v__1(sK128,nn,nn)
| ~ object(nn)
| ~ spl158_9
| ~ spl158_94 ),
inference(forward_subsumption_resolution,[],[f14395,f406]) ).
fof(f14403,plain,
( v__1(sortedList_first,sK128,sK128)
| null = sK128
| ~ object(nn)
| ~ spl158_94
| ~ spl158_95 ),
inference(forward_subsumption_resolution,[],[f14398,f406]) ).
fof(f14405,plain,
( ~ v__1(sK128,nn,nn)
| ~ spl158_9
| ~ spl158_94 ),
inference(forward_subsumption_resolution,[],[f14400,f354]) ).
fof(f14407,plain,
( v__1(sortedList_first,sK128,sK128)
| ~ object(nn)
| ~ spl158_94
| ~ spl158_95
| spl158_355 ),
inference(forward_subsumption_resolution,[],[f14403,f4168]) ).
fof(f14409,plain,
( v__1(sortedList_first,sK128,sK128)
| ~ spl158_94
| ~ spl158_95
| spl158_355 ),
inference(forward_subsumption_resolution,[],[f14407,f354]) ).
fof(f14909,plain,
( sP26(sK157)
| sP25(sK157)
| node_next(nn) = sK113(sK157)
| ~ spl158_4 ),
inference(resolution,[],[f4123,f671]) ).
fof(f14910,plain,
( sP25(sK157)
| node_next(nn) = sK113(sK157)
| ~ spl158_4
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f14909,f8538]) ).
fof(f14911,plain,
( node_next(nn) = sK113(sK157)
| ~ spl158_4
| spl158_432
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f14910,f8534]) ).
fof(f14912,plain,
( sK128 = sK113(sK157)
| ~ spl158_4
| ~ spl158_94
| spl158_432
| spl158_433 ),
inference(forward_demodulation,[],[f14911,f1380]) ).
fof(f14913,plain,
( null != sK128
| ~ spl158_4
| ~ spl158_94
| spl158_432
| spl158_433
| spl158_434 ),
inference(superposition,[],[f8542,f14912]) ).
fof(f14914,plain,
( v__1(sK128,sK157,sK157)
| sP26(sK157)
| sP25(sK157)
| ~ sP35(sK157)
| ~ spl158_4
| ~ spl158_94
| spl158_432
| spl158_433 ),
inference(superposition,[],[f672,f14912]) ).
fof(f14915,plain,
( v__1(sK128,sK157,sK157)
| sP25(sK157)
| ~ sP35(sK157)
| ~ spl158_4
| ~ spl158_94
| spl158_432
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f14914,f8538]) ).
fof(f14916,plain,
( v__1(sK128,sK157,sK157)
| ~ sP35(sK157)
| ~ spl158_4
| ~ spl158_94
| spl158_432
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f14915,f8534]) ).
fof(f14917,plain,
( v__1(sK128,sK157,sK157)
| ~ spl158_4
| ~ spl158_94
| spl158_432
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f14916,f4123]) ).
fof(f14920,plain,
( ! [X0] :
( ~ object(sK128)
| ~ object(sK157)
| ~ v__1(X0,sK128,sK128)
| ~ object(X0)
| v__1(X0,sK157,sK157) )
| ~ spl158_4
| ~ spl158_94
| spl158_432
| spl158_433 ),
inference(resolution,[],[f14917,f364]) ).
fof(f14929,plain,
( ! [X0] :
( ~ object(sK157)
| ~ v__1(X0,sK128,sK128)
| ~ object(X0)
| v__1(X0,sK157,sK157) )
| ~ spl158_4
| ~ spl158_94
| ~ spl158_95
| spl158_432
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f14920,f1385]) ).
fof(f14934,plain,
( ! [X0] :
( ~ v__1(X0,sK128,sK128)
| ~ object(X0)
| v__1(X0,sK157,sK157) )
| ~ spl158_4
| ~ spl158_94
| ~ spl158_95
| spl158_432
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f14929,f878]) ).
fof(f14988,plain,
( ~ object(sortedList_first)
| v__1(sortedList_first,sK157,sK157)
| ~ spl158_4
| ~ spl158_94
| ~ spl158_95
| spl158_355
| spl158_432
| spl158_433 ),
inference(resolution,[],[f14934,f14409]) ).
fof(f15058,plain,
( v__1(sortedList_first,sK157,sK157)
| ~ spl158_4
| ~ spl158_94
| ~ spl158_95
| spl158_355
| spl158_432
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f14988,f361]) ).
fof(f15130,plain,
( $false
| spl158_2
| ~ spl158_4
| ~ spl158_94
| ~ spl158_95
| spl158_355
| spl158_432
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f15058,f944]) ).
fof(f15131,plain,
( spl158_2
| ~ spl158_4
| ~ spl158_94
| ~ spl158_95
| spl158_355
| spl158_432
| spl158_433 ),
inference(avatar_contradiction_clause,[],[f15130]) ).
fof(f15180,plain,
( ! [X0] :
( node_key(X0) != sK78
| ~ v__1(sK150,X0,X0)
| ~ object(X0)
| null = X0 )
| ~ spl158_9
| ~ spl158_39 ),
inference(forward_demodulation,[],[f4748,f1118]) ).
fof(f15229,plain,
( sK78 != sK79
| ~ v__1(sK150,nn,nn)
| ~ object(nn)
| nn = null
| ~ spl158_9
| ~ spl158_39 ),
inference(superposition,[],[f15180,f378]) ).
fof(f15233,plain,
( ~ v__1(sK150,nn,nn)
| ~ object(nn)
| nn = null
| ~ spl158_9
| ~ spl158_39 ),
inference(forward_subsumption_resolution,[],[f15229,f2249]) ).
fof(f15235,plain,
( ~ object(nn)
| nn = null
| ~ spl158_9
| ~ spl158_39
| ~ spl158_40 ),
inference(forward_subsumption_resolution,[],[f15233,f1123]) ).
fof(f15238,plain,
( nn = null
| ~ spl158_9
| ~ spl158_39
| ~ spl158_40 ),
inference(forward_subsumption_resolution,[],[f15235,f354]) ).
fof(f15239,plain,
( $false
| ~ spl158_9
| ~ spl158_39
| ~ spl158_40 ),
inference(forward_subsumption_resolution,[],[f15238,f406]) ).
fof(f15240,plain,
( ~ spl158_9
| ~ spl158_39
| ~ spl158_40 ),
inference(avatar_contradiction_clause,[],[f15239]) ).
fof(f15283,plain,
( ! [X0] :
( ~ v__1(sK116,X0,X0)
| ~ object(X0)
| ~ v__1(sortedList_first,nn,nn)
| nn = null
| ~ object(sK116)
| ~ object(nn)
| null = X0
| ~ integer(node_key(nn))
| ~ integer(node_key(X0))
| lteq(node_key(nn),node_key(X0)) )
| ~ spl158_135 ),
inference(superposition,[],[f891,f1575]) ).
fof(f15295,plain,
( ! [X0] :
( ~ v__1(sK116,X0,X0)
| ~ object(X0)
| nn = null
| ~ object(sK116)
| ~ object(nn)
| null = X0
| ~ integer(node_key(nn))
| ~ integer(node_key(X0))
| lteq(node_key(nn),node_key(X0)) )
| ~ spl158_9
| ~ spl158_135 ),
inference(forward_subsumption_resolution,[],[f15283,f972]) ).
fof(f15300,plain,
( ! [X0] :
( ~ v__1(sK116,X0,X0)
| ~ object(X0)
| ~ object(sK116)
| ~ object(nn)
| null = X0
| ~ integer(node_key(nn))
| ~ integer(node_key(X0))
| lteq(node_key(nn),node_key(X0)) )
| ~ spl158_9
| ~ spl158_135 ),
inference(forward_subsumption_resolution,[],[f15295,f406]) ).
fof(f15303,plain,
( ! [X0] :
( ~ v__1(sK116,X0,X0)
| ~ object(X0)
| ~ object(nn)
| null = X0
| ~ integer(node_key(nn))
| ~ integer(node_key(X0))
| lteq(node_key(nn),node_key(X0)) )
| ~ spl158_9
| ~ spl158_135
| ~ spl158_137 ),
inference(forward_subsumption_resolution,[],[f15300,f1585]) ).
fof(f15305,plain,
( ! [X0] :
( ~ v__1(sK116,X0,X0)
| ~ object(X0)
| null = X0
| ~ integer(node_key(nn))
| ~ integer(node_key(X0))
| lteq(node_key(nn),node_key(X0)) )
| ~ spl158_9
| ~ spl158_135
| ~ spl158_137 ),
inference(forward_subsumption_resolution,[],[f15303,f354]) ).
fof(f15306,plain,
( ! [X0] :
( ~ v__1(sK116,X0,X0)
| ~ object(X0)
| null = X0
| ~ integer(node_key(nn))
| lteq(node_key(nn),node_key(X0)) )
| ~ spl158_9
| ~ spl158_135
| ~ spl158_137 ),
inference(forward_subsumption_resolution,[],[f15305,f358]) ).
fof(f15307,plain,
( ! [X0] :
( ~ v__1(sK116,X0,X0)
| ~ object(X0)
| null = X0
| lteq(node_key(nn),node_key(X0)) )
| ~ spl158_9
| ~ spl158_135
| ~ spl158_137 ),
inference(forward_subsumption_resolution,[],[f15306,f358]) ).
fof(f15308,plain,
( ! [X0] :
( lteq(sK79,node_key(X0))
| ~ v__1(sK116,X0,X0)
| ~ object(X0)
| null = X0 )
| ~ spl158_9
| ~ spl158_135
| ~ spl158_137 ),
inference(forward_demodulation,[],[f15307,f378]) ).
fof(f15309,plain,
( ! [X0] :
( ~ v__1(sK116,X0,X0)
| lteq(sK78,node_key(X0))
| ~ object(X0)
| null = X0 )
| ~ spl158_9
| ~ spl158_135
| ~ spl158_137 ),
inference(forward_demodulation,[],[f15308,f2249]) ).
fof(f16717,plain,
( lteq(sK78,node_key(prev_2))
| ~ object(prev_2)
| prev_2 = null
| ~ spl158_9
| ~ spl158_135
| ~ spl158_136
| ~ spl158_137 ),
inference(resolution,[],[f10486,f15309]) ).
fof(f16730,plain,
( ~ object(prev_2)
| prev_2 = null
| ~ spl158_9
| ~ spl158_135
| ~ spl158_136
| ~ spl158_137
| spl158_426 ),
inference(forward_subsumption_resolution,[],[f16717,f8224]) ).
fof(f16735,plain,
( prev_2 = null
| ~ spl158_9
| ~ spl158_135
| ~ spl158_136
| ~ spl158_137
| spl158_426 ),
inference(forward_subsumption_resolution,[],[f16730,f356]) ).
fof(f16746,plain,
( $false
| ~ spl158_9
| ~ spl158_135
| ~ spl158_136
| ~ spl158_137
| spl158_266
| spl158_426 ),
inference(forward_subsumption_resolution,[],[f16735,f2225]) ).
fof(f16747,plain,
( ~ spl158_9
| ~ spl158_135
| ~ spl158_136
| ~ spl158_137
| spl158_266
| spl158_426 ),
inference(avatar_contradiction_clause,[],[f16746]) ).
fof(f16814,plain,
( v__1(sortedList_first,sK129,sK129)
| ~ spl158_87
| ~ spl158_89
| ~ spl158_604 ),
inference(forward_demodulation,[],[f13340,f6357]) ).
fof(f18292,plain,
( sK129 = sK113(sK157)
| ~ spl158_4
| ~ spl158_89
| spl158_432
| spl158_433 ),
inference(forward_demodulation,[],[f14911,f1354]) ).
fof(f18355,plain,
( null != sK129
| ~ spl158_4
| ~ spl158_89
| spl158_432
| spl158_433
| spl158_434 ),
inference(superposition,[],[f8542,f18292]) ).
fof(f18356,plain,
( v__1(sK129,sK157,sK157)
| sP26(sK157)
| sP25(sK157)
| ~ sP35(sK157)
| ~ spl158_4
| ~ spl158_89
| spl158_432
| spl158_433 ),
inference(superposition,[],[f672,f18292]) ).
fof(f18357,plain,
( v__1(sK129,sK157,sK157)
| sP25(sK157)
| ~ sP35(sK157)
| ~ spl158_4
| ~ spl158_89
| spl158_432
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f18356,f8538]) ).
fof(f18358,plain,
( v__1(sK129,sK157,sK157)
| ~ sP35(sK157)
| ~ spl158_4
| ~ spl158_89
| spl158_432
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f18357,f8534]) ).
fof(f18359,plain,
( v__1(sK129,sK157,sK157)
| ~ spl158_4
| ~ spl158_89
| spl158_432
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f18358,f4123]) ).
fof(f18372,plain,
( ! [X0] :
( ~ object(sK129)
| ~ object(sK157)
| ~ v__1(X0,sK129,sK129)
| ~ object(X0)
| v__1(X0,sK157,sK157) )
| ~ spl158_4
| ~ spl158_89
| spl158_432
| spl158_433 ),
inference(resolution,[],[f18359,f364]) ).
fof(f18381,plain,
( ! [X0] :
( ~ object(sK157)
| ~ v__1(X0,sK129,sK129)
| ~ object(X0)
| v__1(X0,sK157,sK157) )
| ~ spl158_4
| ~ spl158_89
| ~ spl158_91
| spl158_432
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f18372,f1364]) ).
fof(f18385,plain,
( ! [X0] :
( ~ v__1(X0,sK129,sK129)
| ~ object(X0)
| v__1(X0,sK157,sK157) )
| ~ spl158_4
| ~ spl158_89
| ~ spl158_91
| spl158_432
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f18381,f878]) ).
fof(f18605,plain,
( ~ object(sortedList_first)
| v__1(sortedList_first,sK157,sK157)
| ~ spl158_4
| ~ spl158_87
| ~ spl158_89
| ~ spl158_91
| spl158_432
| spl158_433
| ~ spl158_604 ),
inference(resolution,[],[f16814,f18385]) ).
fof(f18638,plain,
( v__1(sortedList_first,sK157,sK157)
| ~ spl158_4
| ~ spl158_87
| ~ spl158_89
| ~ spl158_91
| spl158_432
| spl158_433
| ~ spl158_604 ),
inference(forward_subsumption_resolution,[],[f18605,f361]) ).
fof(f18662,plain,
( $false
| spl158_2
| ~ spl158_4
| ~ spl158_87
| ~ spl158_89
| ~ spl158_91
| spl158_432
| spl158_433
| ~ spl158_604 ),
inference(forward_subsumption_resolution,[],[f18638,f944]) ).
fof(f18663,plain,
( spl158_2
| ~ spl158_4
| ~ spl158_87
| ~ spl158_89
| ~ spl158_91
| spl158_432
| spl158_433
| ~ spl158_604 ),
inference(avatar_contradiction_clause,[],[f18662]) ).
fof(f18691,plain,
( null = sK129
| ~ spl158_87
| ~ spl158_89
| ~ spl158_603 ),
inference(superposition,[],[f6357,f13336]) ).
fof(f18707,definition,
( spl158_888
<=> null = sK129 ),
introduced(definition,[new_symbols(definition,[spl158_888])],[avatar_definition]) ).
fof(f18712,plain,
( ~ spl158_888
| ~ spl158_4
| ~ spl158_89
| spl158_432
| spl158_433
| spl158_434 ),
inference(avatar_split_clause,[],[f18355,f8541,f8537,f8533,f1352,f951,f18707]) ).
fof(f18718,plain,
( spl158_888
| ~ spl158_87
| ~ spl158_89
| ~ spl158_603 ),
inference(avatar_split_clause,[],[f18691,f13334,f1352,f1342,f18707]) ).
fof(f18721,plain,
( ~ spl158_355
| ~ spl158_4
| ~ spl158_94
| spl158_432
| spl158_433
| spl158_434 ),
inference(avatar_split_clause,[],[f14913,f8541,f8537,f8533,f1378,f951,f4166]) ).
fof(f18849,plain,
( v__1(sK129,nn,nn)
| ~ spl158_1
| ~ spl158_4
| ~ spl158_89
| spl158_432
| spl158_433 ),
inference(superposition,[],[f18359,f940]) ).
fof(f18852,plain,
( $false
| ~ spl158_1
| ~ spl158_4
| ~ spl158_9
| ~ spl158_89
| spl158_432
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f18849,f6412]) ).
fof(f18853,plain,
( ~ spl158_1
| ~ spl158_4
| ~ spl158_9
| ~ spl158_89
| spl158_432
| spl158_433 ),
inference(avatar_contradiction_clause,[],[f18852]) ).
fof(f18881,plain,
( v__1(sK128,nn,nn)
| ~ spl158_1
| ~ spl158_4
| ~ spl158_94
| spl158_432
| spl158_433 ),
inference(forward_demodulation,[],[f14917,f940]) ).
fof(f18933,plain,
( $false
| ~ spl158_1
| ~ spl158_4
| ~ spl158_9
| ~ spl158_94
| spl158_432
| spl158_433 ),
inference(forward_subsumption_resolution,[],[f18881,f14405]) ).
fof(f18934,plain,
( ~ spl158_1
| ~ spl158_4
| ~ spl158_9
| ~ spl158_94
| spl158_432
| spl158_433 ),
inference(avatar_contradiction_clause,[],[f18933]) ).
cnf(s1,plain,
( spl158_1
| ~ spl158_2
| spl158_3 ),
inference(sat_conversion,[],[f949]) ).
cnf(s4,plain,
( spl158_4
| spl158_5
| spl158_6
| spl158_7
| spl158_8
| spl158_12 ),
inference(sat_conversion,[],[f988]) ).
cnf(s8,plain,
~ spl158_3,
inference(sat_conversion,[],[f1004]) ).
cnf(s27,plain,
( ~ spl158_38
| spl158_39 ),
inference(sat_conversion,[],[f1119]) ).
cnf(s28,plain,
( ~ spl158_38
| spl158_40 ),
inference(sat_conversion,[],[f1124]) ).
cnf(s31,plain,
( spl158_38
| ~ spl158_42
| spl158_44 ),
inference(sat_conversion,[],[f1143]) ).
cnf(s32,plain,
( spl158_38
| ~ spl158_42
| spl158_45 ),
inference(sat_conversion,[],[f1148]) ).
cnf(s66,plain,
( ~ spl158_85
| spl158_87 ),
inference(sat_conversion,[],[f1345]) ).
cnf(s67,plain,
( ~ spl158_85
| spl158_88 ),
inference(sat_conversion,[],[f1350]) ).
cnf(s68,plain,
( ~ spl158_85
| spl158_89 ),
inference(sat_conversion,[],[f1355]) ).
cnf(s70,plain,
( ~ spl158_85
| spl158_91 ),
inference(sat_conversion,[],[f1365]) ).
cnf(s75,plain,
( spl158_42
| spl158_92
| spl158_94 ),
inference(sat_conversion,[],[f1381]) ).
cnf(s76,plain,
( spl158_42
| spl158_92
| spl158_95 ),
inference(sat_conversion,[],[f1386]) ).
cnf(s78,plain,
( spl158_65
| spl158_68
| spl158_96 ),
inference(sat_conversion,[],[f1391]) ).
cnf(s84,plain,
( spl158_65
| spl158_68
| spl158_100 ),
inference(sat_conversion,[],[f1412]) ).
cnf(s127,plain,
( spl158_85
| spl158_134
| spl158_135 ),
inference(sat_conversion,[],[f1576]) ).
cnf(s128,plain,
( spl158_85
| spl158_134
| spl158_136 ),
inference(sat_conversion,[],[f1581]) ).
cnf(s129,plain,
( spl158_85
| spl158_134
| spl158_137 ),
inference(sat_conversion,[],[f1586]) ).
cnf(s212,plain,
( ~ spl158_11
| spl158_119
| spl158_222 ),
inference(sat_conversion,[],[f2000]) ).
cnf(s217,plain,
( ~ spl158_11
| spl158_119
| spl158_223 ),
inference(sat_conversion,[],[f2008]) ).
cnf(s265,plain,
( ~ spl158_10
| ~ spl158_11
| spl158_249 ),
inference(sat_conversion,[],[f2141]) ).
cnf(s268,plain,
( ~ spl158_11
| spl158_119
| spl158_250 ),
inference(sat_conversion,[],[f2149]) ).
cnf(s273,plain,
( ~ spl158_11
| spl158_119
| spl158_251 ),
inference(sat_conversion,[],[f2157]) ).
cnf(s291,plain,
( spl158_265
| spl158_266 ),
inference(sat_conversion,[],[f2227]) ).
cnf(s293,plain,
( spl158_11
| spl158_266 ),
inference(sat_conversion,[],[f2234]) ).
cnf(s294,plain,
~ spl158_266,
inference(sat_conversion,[],[f2236]) ).
cnf(s295,plain,
spl158_260,
inference(sat_conversion,[],[f2237]) ).
cnf(s297,plain,
spl158_9,
inference(sat_conversion,[],[f2242]) ).
cnf(s298,plain,
( ~ spl158_9
| spl158_269 ),
inference(sat_conversion,[],[f2247]) ).
cnf(s302,plain,
( ~ spl158_6
| ~ spl158_249 ),
inference(sat_conversion,[],[f2329]) ).
cnf(s303,plain,
( ~ spl158_44
| ~ spl158_45
| spl158_272
| spl158_273 ),
inference(sat_conversion,[],[f2352]) ).
cnf(s359,plain,
( ~ spl158_5
| spl158_12
| spl158_346
| spl158_347 ),
inference(sat_conversion,[],[f3612]) ).
cnf(s361,plain,
( spl158_65
| ~ spl158_68
| ~ spl158_260 ),
inference(sat_conversion,[],[f3889]) ).
cnf(s371,plain,
( ~ spl158_65
| ~ spl158_260
| spl158_266 ),
inference(sat_conversion,[],[f3949]) ).
cnf(s380,plain,
( ~ spl158_7
| ~ spl158_250 ),
inference(sat_conversion,[],[f4116]) ).
cnf(s381,plain,
( ~ spl158_8
| ~ spl158_251 ),
inference(sat_conversion,[],[f4118]) ).
cnf(s382,plain,
( ~ spl158_223
| ~ spl158_347 ),
inference(sat_conversion,[],[f4120]) ).
cnf(s383,plain,
( ~ spl158_222
| ~ spl158_346 ),
inference(sat_conversion,[],[f4122]) ).
cnf(s388,plain,
( ~ spl158_11
| ~ spl158_119
| ~ spl158_265
| spl158_266 ),
inference(sat_conversion,[],[f4808]) ).
cnf(s392,plain,
( spl158_119
| ~ spl158_222
| ~ spl158_223
| ~ spl158_318 ),
inference(sat_conversion,[],[f4902]) ).
cnf(s517,plain,
( spl158_3
| ~ spl158_260
| ~ spl158_432 ),
inference(sat_conversion,[],[f8550]) ).
cnf(s535,plain,
( ~ spl158_4
| spl158_433
| ~ spl158_434
| spl158_467 ),
inference(sat_conversion,[],[f10281]) ).
cnf(s538,plain,
( spl158_3
| ~ spl158_260
| ~ spl158_467 ),
inference(sat_conversion,[],[f10333]) ).
cnf(s546,plain,
( ~ spl158_4
| ~ spl158_92
| ~ spl158_96
| ~ spl158_100
| ~ spl158_134 ),
inference(sat_conversion,[],[f10473]) ).
cnf(s575,plain,
( ~ spl158_433
| spl158_467
| spl158_501 ),
inference(sat_conversion,[],[f10738]) ).
cnf(s576,plain,
( ~ spl158_260
| spl158_467
| ~ spl158_501 ),
inference(sat_conversion,[],[f10752]) ).
cnf(s583,plain,
( ~ spl158_4
| ~ spl158_44
| ~ spl158_272
| spl158_432
| spl158_433
| spl158_434 ),
inference(sat_conversion,[],[f10846]) ).
cnf(s608,plain,
( ~ spl158_9
| spl158_10
| ~ spl158_11
| spl158_119 ),
inference(sat_conversion,[],[f11615]) ).
cnf(s618,plain,
( spl158_2
| ~ spl158_12 ),
inference(sat_conversion,[],[f11669]) ).
cnf(s631,plain,
( ~ spl158_1
| ~ spl158_12
| spl158_119 ),
inference(sat_conversion,[],[f11731]) ).
cnf(s632,plain,
( ~ spl158_1
| ~ spl158_5
| spl158_318 ),
inference(sat_conversion,[],[f11733]) ).
cnf(s650,plain,
( ~ spl158_11
| ~ spl158_265
| spl158_266
| ~ spl158_269
| spl158_425
| ~ spl158_426 ),
inference(sat_conversion,[],[f12050]) ).
cnf(s674,plain,
( ~ spl158_11
| ~ spl158_265
| spl158_266
| ~ spl158_269
| ~ spl158_425 ),
inference(sat_conversion,[],[f12343]) ).
cnf(s771,plain,
( ~ spl158_87
| ~ spl158_88
| spl158_603
| spl158_604 ),
inference(sat_conversion,[],[f13341]) ).
cnf(s783,plain,
( ~ spl158_1
| ~ spl158_4
| ~ spl158_9
| ~ spl158_44
| spl158_432
| spl158_433 ),
inference(sat_conversion,[],[f13472]) ).
cnf(s839,plain,
( spl158_2
| ~ spl158_4
| ~ spl158_44
| ~ spl158_45
| ~ spl158_273
| spl158_432
| spl158_433 ),
inference(sat_conversion,[],[f14205]) ).
cnf(s891,plain,
( spl158_2
| ~ spl158_4
| ~ spl158_94
| ~ spl158_95
| spl158_355
| spl158_432
| spl158_433 ),
inference(sat_conversion,[],[f15131]) ).
cnf(s917,plain,
( ~ spl158_9
| ~ spl158_39
| ~ spl158_40 ),
inference(sat_conversion,[],[f15240]) ).
cnf(s997,plain,
( ~ spl158_9
| ~ spl158_135
| ~ spl158_136
| ~ spl158_137
| spl158_266
| spl158_426 ),
inference(sat_conversion,[],[f16747]) ).
cnf(s1142,plain,
( spl158_2
| ~ spl158_4
| ~ spl158_87
| ~ spl158_89
| ~ spl158_91
| spl158_432
| spl158_433
| ~ spl158_604 ),
inference(sat_conversion,[],[f18663]) ).
cnf(s1149,plain,
( ~ spl158_4
| ~ spl158_89
| spl158_432
| spl158_433
| spl158_434
| ~ spl158_888 ),
inference(sat_conversion,[],[f18712]) ).
cnf(s1151,plain,
( ~ spl158_87
| ~ spl158_89
| ~ spl158_603
| spl158_888 ),
inference(sat_conversion,[],[f18718]) ).
cnf(s1153,plain,
( ~ spl158_4
| ~ spl158_94
| ~ spl158_355
| spl158_432
| spl158_433
| spl158_434 ),
inference(sat_conversion,[],[f18721]) ).
cnf(s1166,plain,
( ~ spl158_1
| ~ spl158_4
| ~ spl158_9
| ~ spl158_89
| spl158_432
| spl158_433 ),
inference(sat_conversion,[],[f18853]) ).
cnf(s1172,plain,
( ~ spl158_1
| ~ spl158_4
| ~ spl158_9
| ~ spl158_94
| spl158_432
| spl158_433 ),
inference(sat_conversion,[],[f18934]) ).
cnf(s1184,plain,
spl158_269,
inference(rat,[],[s298,s297]) ).
cnf(s1186,plain,
~ spl158_65,
inference(rat,[],[s371,s295,s294]) ).
cnf(s1187,plain,
~ spl158_68,
inference(rat,[],[s361,s295,s1186]) ).
cnf(s1188,plain,
spl158_11,
inference(rat,[],[s293,s294]) ).
cnf(s1189,plain,
spl158_265,
inference(rat,[],[s291,s294]) ).
cnf(s1190,plain,
~ spl158_425,
inference(rat,[],[s674,s1188,s1184,s294,s1189]) ).
cnf(s1191,plain,
~ spl158_119,
inference(rat,[],[s388,s294,s1188,s1189]) ).
cnf(s1192,plain,
~ spl158_426,
inference(rat,[],[s650,s1189,s1188,s1184,s294,s1190]) ).
cnf(s1194,plain,
spl158_10,
inference(rat,[],[s608,s1188,s297,s1191]) ).
cnf(s1205,plain,
spl158_251,
inference(rat,[],[s273,s1191,s1188]) ).
cnf(s1206,plain,
~ spl158_8,
inference(rat,[],[s381,s1205]) ).
cnf(s1207,plain,
spl158_250,
inference(rat,[],[s268,s1191,s1188]) ).
cnf(s1208,plain,
~ spl158_7,
inference(rat,[],[s380,s1207]) ).
cnf(s1209,plain,
spl158_249,
inference(rat,[],[s265,s1188,s1194]) ).
cnf(s1210,plain,
~ spl158_6,
inference(rat,[],[s302,s1209]) ).
cnf(s1217,plain,
spl158_223,
inference(rat,[],[s217,s1191,s1188]) ).
cnf(s1218,plain,
~ spl158_347,
inference(rat,[],[s382,s1217]) ).
cnf(s1219,plain,
spl158_222,
inference(rat,[],[s212,s1191,s1188]) ).
cnf(s1220,plain,
~ spl158_318,
inference(rat,[],[s392,s1217,s1191,s1219]) ).
cnf(s1221,plain,
~ spl158_346,
inference(rat,[],[s383,s1219]) ).
cnf(s1230,plain,
spl158_100,
inference(rat,[],[s84,s1187,s1186]) ).
cnf(s1231,plain,
spl158_96,
inference(rat,[],[s78,s1187,s1186]) ).
cnf(s1232,plain,
~ spl158_467,
inference(rat,[],[s538,s295,s8]) ).
cnf(s1233,plain,
~ spl158_432,
inference(rat,[],[s517,s295,s8]) ).
cnf(s1235,plain,
~ spl158_501,
inference(rat,[],[s576,s295,s1232]) ).
cnf(s1236,plain,
~ spl158_433,
inference(rat,[],[s575,s1235,s1232]) ).
cnf(s1245,plain,
( spl158_4
| spl158_5
| spl158_12 ),
inference(rat,[],[s4,s1206,s1208,s1210]) ).
cnf(s1246,plain,
( spl158_1
| ~ spl158_2 ),
inference(rat,[],[s1,s8]) ).
cnf(s1247,plain,
( spl158_85
| spl158_134 ),
inference(rat,[],[s997,s127,s128,s129,s1192,s294,s297]) ).
cnf(s1248,plain,
( ~ spl158_85
| spl158_2 ),
inference(rat,[],[s771,s1142,s1151,s1149,s66,s67,s68,s70,s535,s1245,s359,s618,s1233,s1236,s1232,s1218,s1221]) ).
cnf(s1249,plain,
( spl158_42
| spl158_2 ),
inference(rat,[],[s891,s1153,s76,s75,s535,s546,s1247,s1248,s1245,s359,s618,s1233,s1236,s1218,s1221,s1230,s1231,s1232]) ).
cnf(s1250,plain,
( spl158_38
| spl158_2 ),
inference(rat,[],[s839,s303,s583,s32,s31,s535,s1245,s359,s618,s1249,s1233,s1236,s1232,s1218,s1221]) ).
cnf(s1251,plain,
~ spl158_38,
inference(rat,[],[s917,s27,s28,s297]) ).
cnf(s1252,plain,
spl158_2,
inference(rat,[],[s1250,s1251]) ).
cnf(s1253,plain,
spl158_1,
inference(rat,[],[s1246,s1252]) ).
cnf(s1255,plain,
~ spl158_5,
inference(rat,[],[s632,s1220,s1253]) ).
cnf(s1256,plain,
~ spl158_12,
inference(rat,[],[s631,s1191,s1253]) ).
cnf(s1260,plain,
spl158_4,
inference(rat,[],[s1245,s1256,s1255]) ).
cnf(s1262,plain,
~ spl158_89,
inference(rat,[],[s1166,s1236,s1233,s1253,s297,s1260]) ).
cnf(s1265,plain,
~ spl158_94,
inference(rat,[],[s1172,s1236,s1233,s1253,s297,s1260]) ).
cnf(s1266,plain,
~ spl158_44,
inference(rat,[],[s783,s1236,s1233,s1253,s297,s1260]) ).
cnf(s1267,plain,
~ spl158_85,
inference(rat,[],[s68,s1262]) ).
cnf(s1268,plain,
~ spl158_42,
inference(rat,[],[s31,s1251,s1266]) ).
cnf(s1269,plain,
spl158_134,
inference(rat,[],[s1247,s1267]) ).
cnf(s1270,plain,
spl158_92,
inference(rat,[],[s75,s1265,s1268]) ).
cnf(s1271,plain,
$false,
inference(rat,[],[s546,s1260,s1230,s1231,s1269,s1270]) ).
fof(f18959,plain,
$false,
inference(avatar_sat_refutation,[],[s1271]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW095+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n001.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 13:18:03 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.10/3.01 % (345189)Detected formulas, will run a generic FOF schedule.
% 15.10/3.01 % (345293)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=3540268149:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 15.10/3.01 % (345302)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1266190510:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 15.10/3.01 % (345297)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=2820319949:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 15.10/3.01 % (345301)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1630135285:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 15.10/3.01 % (345303)dis-21_1_sil=8000:lcm=predicate:random_seed=417903044: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)
% 15.10/3.01 % (345299)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=1063274841:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 15.10/3.01 % (345300)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=140181227:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 15.10/3.01 % (345301)Instruction limit reached!
% 15.10/3.01 % (345301)------------------------------
% 15.10/3.01 % (345301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.10/3.01 % (345301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.10/3.01 % (345301)CaDiCaL version: 2.1.3
% 15.10/3.01 % (345301)Termination reason: Instruction limit
% 15.10/3.01 % (345301)Termination phase: Saturation
% 15.10/3.01 % (345301)Time elapsed: 0.059 s
% 15.10/3.01 % (345301)Peak memory usage: 89 MB
% 15.10/3.01 % (345301)Instructions burned: 121 (million)
% 15.10/3.01 % (345303)Instruction limit reached!
% 15.10/3.01 % (345303)------------------------------
% 15.10/3.01 % (345303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.10/3.01 % (345303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.10/3.01 % (345303)CaDiCaL version: 2.1.3
% 15.10/3.01 % (345303)Termination reason: Instruction limit
% 15.10/3.01 % (345303)Termination phase: Saturation
% 15.10/3.01 % (345303)Time elapsed: 0.072 s
% 15.10/3.01 % (345303)Peak memory usage: 91 MB
% 15.10/3.01 % (345303)Instructions burned: 131 (million)
% 15.10/3.01 % (345302)Instruction limit reached!
% 15.10/3.01 % (345302)------------------------------
% 15.10/3.01 % (345302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.10/3.01 % (345302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.10/3.01 % (345302)CaDiCaL version: 2.1.3
% 15.10/3.01 % (345302)Termination reason: Instruction limit
% 15.10/3.01 % (345302)Termination phase: Saturation
% 15.10/3.01 % (345302)Time elapsed: 0.086 s
% 15.10/3.01 % (345302)Peak memory usage: 90 MB
% 15.10/3.01 % (345302)Instructions burned: 140 (million)
% 15.10/3.01 % (345300)Instruction limit reached!
% 15.10/3.01 % (345300)------------------------------
% 15.10/3.01 % (345300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.10/3.01 % (345300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.10/3.01 % (345300)CaDiCaL version: 2.1.3
% 15.10/3.01 % (345300)Termination reason: Instruction limit
% 15.10/3.01 % (345300)Termination phase: Saturation
% 15.10/3.01 % (345300)Time elapsed: 0.101 s
% 15.10/3.01 % (345300)Peak memory usage: 91 MB
% 15.10/3.01 % (345300)Instructions burned: 109 (million)
% 15.10/3.01 % (345338)lrs+10_1_sil=8000:sp=occurrence:random_seed=3987146795:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 15.10/3.01 % (345340)lrs+1011_1_sil=32000:sp=occurrence:random_seed=956447642:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 15.10/3.01 % (345339)lrs+10_1_sil=32000:urr=on:br=off:random_seed=222357348:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 15.10/3.01 % (345339)Instruction limit reached!
% 15.10/3.01 % (345339)------------------------------
% 15.10/3.01 % (345339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.10/3.01 % (345339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.10/3.01 % (345341)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=4165743876:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 22.04/3.86 % (345339)CaDiCaL version: 2.1.3
% 22.04/3.86 % (345339)Termination reason: Instruction limit
% 22.04/3.86 % (345339)Termination phase: Saturation
% 22.04/3.86 % (345339)Time elapsed: 0.087 s
% 22.04/3.86 % (345339)Peak memory usage: 92 MB
% 22.04/3.86 % (345339)Instructions burned: 158 (million)
% 22.04/3.86 % (345341)Instruction limit reached!
% 22.04/3.86 % (345341)------------------------------
% 22.04/3.86 % (345341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.04/3.86 % (345341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.04/3.86 % (345341)CaDiCaL version: 2.1.3
% 22.04/3.86 % (345341)Termination reason: Instruction limit
% 22.04/3.86 % (345341)Termination phase: Saturation
% 22.04/3.86 % (345341)Time elapsed: 0.070 s
% 22.04/3.86 % (345341)Peak memory usage: 91 MB
% 22.04/3.86 % (345341)Instructions burned: 249 (million)
% 22.04/3.86 % (345338)Instruction limit reached!
% 22.04/3.86 % (345338)------------------------------
% 22.04/3.86 % (345338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.04/3.86 % (345338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.04/3.86 % (345338)CaDiCaL version: 2.1.3
% 22.04/3.86 % (345338)Termination reason: Instruction limit
% 22.04/3.86 % (345338)Termination phase: Saturation
% 22.04/3.86 % (345338)Time elapsed: 0.179 s
% 22.04/3.86 % (345338)Peak memory usage: 92 MB
% 22.04/3.86 % (345338)Instructions burned: 285 (million)
% 22.04/3.86 % (345340)Instruction limit reached!
% 22.04/3.86 % (345340)------------------------------
% 22.04/3.86 % (345340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.04/3.86 % (345340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.04/3.86 % (345340)CaDiCaL version: 2.1.3
% 22.04/3.86 % (345340)Termination reason: Instruction limit
% 22.04/3.86 % (345340)Termination phase: Saturation
% 22.04/3.86 % (345340)Time elapsed: 0.198 s
% 22.04/3.86 % (345340)Peak memory usage: 93 MB
% 22.04/3.86 % (345340)Instructions burned: 325 (million)
% 22.04/3.86 % (345346)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=162686870:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 22.04/3.86 % (345347)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1128532415:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 22.04/3.86 % (345349)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3445880755:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 22.04/3.86 % (345348)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2945691166:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 22.04/3.86 % (345346)Instruction limit reached!
% 22.04/3.86 % (345346)------------------------------
% 22.04/3.86 % (345346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.04/3.86 % (345346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.04/3.86 % (345346)CaDiCaL version: 2.1.3
% 22.04/3.86 % (345346)Termination reason: Instruction limit
% 22.04/3.86 % (345346)Termination phase: Saturation
% 22.04/3.86 % (345346)Time elapsed: 0.154 s
% 22.04/3.86 % (345346)Peak memory usage: 90 MB
% 22.04/3.86 % (345346)Instructions burned: 294 (million)
% 22.04/3.86 % (345349)Instruction limit reached!
% 22.04/3.86 % (345349)------------------------------
% 22.04/3.86 % (345349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.04/3.86 % (345349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.04/3.86 % (345349)CaDiCaL version: 2.1.3
% 22.04/3.86 % (345349)Termination reason: Instruction limit
% 22.04/3.86 % (345349)Termination phase: Saturation
% 22.04/3.86 % (345349)Time elapsed: 0.061 s
% 22.04/3.86 % (345349)Peak memory usage: 89 MB
% 22.04/3.86 % (345349)Instructions burned: 128 (million)
% 22.04/3.86 % (345348)Instruction limit reached!
% 22.04/3.86 % (345348)------------------------------
% 22.04/3.86 % (345348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.04/3.86 % (345348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.04/3.86 % (345348)CaDiCaL version: 2.1.3
% 22.04/3.86 % (345348)Termination reason: Instruction limit
% 22.04/3.86 % (345348)Termination phase: Saturation
% 22.04/3.86 % (345348)Time elapsed: 0.063 s
% 22.04/3.86 % (345348)Peak memory usage: 91 MB
% 22.04/3.86 % (345348)Instructions burned: 114 (million)
% 28.73/4.76 % (345357)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1110516887:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 28.73/4.76 % (345355)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=495499977:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 28.73/4.76 % (345356)lrs+10_1_sil=8000:sp=occurrence:random_seed=3265023517:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 28.73/4.76 % (345355)Instruction limit reached!
% 28.73/4.76 % (345355)------------------------------
% 28.73/4.76 % (345355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.73/4.76 % (345355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.73/4.76 % (345355)CaDiCaL version: 2.1.3
% 28.73/4.76 % (345355)Termination reason: Instruction limit
% 28.73/4.76 % (345355)Termination phase: Clausification
% 28.73/4.76 % (345355)Time elapsed: 0.134 s
% 28.73/4.76 % (345355)Peak memory usage: 139 MB
% 28.73/4.76 % (345355)Instructions burned: 114 (million)
% 28.73/4.76 % (345357)Instruction limit reached!
% 28.73/4.76 % (345357)------------------------------
% 28.73/4.76 % (345357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.73/4.76 % (345357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.73/4.76 % (345357)CaDiCaL version: 2.1.3
% 28.73/4.76 % (345357)Termination reason: Instruction limit
% 28.73/4.76 % (345357)Termination phase: Saturation
% 28.73/4.76 % (345357)Time elapsed: 0.346 s
% 28.73/4.76 % (345357)Peak memory usage: 94 MB
% 28.73/4.76 % (345357)Instructions burned: 438 (million)
% 28.73/4.76 % (345383)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1105361746:i=5202:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/5202Mi)
% 28.73/4.76 % (345397)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3185209113:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2985 on theBenchmark for (2985ds/134Mi)
% 28.73/4.76 % (345397)Instruction limit reached!
% 28.73/4.76 % (345397)------------------------------
% 28.73/4.76 % (345397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.73/4.76 % (345397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.73/4.76 % (345397)CaDiCaL version: 2.1.3
% 28.73/4.76 % (345397)Termination reason: Instruction limit
% 28.73/4.76 % (345397)Termination phase: Saturation
% 28.73/4.76 % (345397)Time elapsed: 0.109 s
% 28.73/4.76 % (345397)Peak memory usage: 90 MB
% 28.73/4.76 % (345397)Instructions burned: 135 (million)
% 28.73/4.76 % (345356)Instruction limit reached!
% 28.73/4.76 % (345356)------------------------------
% 28.73/4.76 % (345356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.73/4.76 % (345356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.73/4.76 % (345356)CaDiCaL version: 2.1.3
% 28.73/4.76 % (345356)Termination reason: Instruction limit
% 28.73/4.76 % (345356)Termination phase: Saturation
% 28.73/4.76 % (345356)Time elapsed: 0.786 s
% 28.73/4.76 % (345356)Peak memory usage: 98 MB
% 28.73/4.76 % (345356)Instructions burned: 907 (million)
% 28.73/4.76 % (345347)Instruction limit reached!
% 28.73/4.76 % (345347)------------------------------
% 28.73/4.76 % (345347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.73/4.76 % (345347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.73/4.76 % (345347)CaDiCaL version: 2.1.3
% 28.73/4.76 % (345347)Termination reason: Instruction limit
% 28.73/4.76 % (345347)Termination phase: Saturation
% 28.73/4.76 % (345347)Time elapsed: 1.315 s
% 28.73/4.76 % (345347)Peak memory usage: 142 MB
% 28.73/4.76 % (345347)Instructions burned: 2351 (million)
% 28.73/4.76 % (345428)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4283586316:st=8:i=592:sd=3:ep=RST:ss=axioms_2981 on theBenchmark for (2981ds/592Mi)
% 28.73/4.76 % (345429)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1628241343:st=3:i=13193:sd=3:ss=axioms_2981 on theBenchmark for (2981ds/13193Mi)
% 28.73/4.76 % (345440)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=2338779968:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/125Mi)
% 28.73/4.76 % (345440)Instruction limit reached!
% 28.73/4.76 % (345440)------------------------------
% 28.73/4.76 % (345440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.73/4.76 % (345440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.73/4.76 % (345440)CaDiCaL version: 2.1.3
% 28.73/4.76 % (345440)Termination reason: Instruction limit
% 28.73/4.76 % (345440)Termination phase: Saturation
% 28.73/4.76 % (345440)Time elapsed: 0.079 s
% 28.73/4.76 % (345440)Peak memory usage: 90 MB
% 28.73/4.76 % (345440)Instructions burned: 126 (million)
% 28.73/4.76 % (345454)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2638863760:i=134:gtgl=5:slsql=off:gtg=exists_sym_2976 on theBenchmark for (2976ds/134Mi)
% 28.73/4.76 % (345428)Instruction limit reached!
% 28.73/4.76 % (345428)------------------------------
% 28.73/4.76 % (345428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.73/4.76 % (345428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.73/4.76 % (345428)CaDiCaL version: 2.1.3
% 28.73/4.76 % (345428)Termination reason: Instruction limit
% 28.73/4.76 % (345428)Termination phase: Saturation
% 28.73/4.76 % (345428)Time elapsed: 0.500 s
% 28.73/4.76 % (345428)Peak memory usage: 95 MB
% 28.73/4.76 % (345428)Instructions burned: 592 (million)
% 28.73/4.76 % (345454)Instruction limit reached!
% 28.73/4.76 % (345454)------------------------------
% 28.73/4.76 % (345454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.73/4.76 % (345454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.73/4.76 % (345454)CaDiCaL version: 2.1.3
% 28.73/4.76 % (345454)Termination reason: Instruction limit
% 28.73/4.76 % (345454)Termination phase: Saturation
% 28.73/4.76 % (345454)Time elapsed: 0.062 s
% 28.73/4.76 % (345454)Peak memory usage: 91 MB
% 28.73/4.76 % (345454)Instructions burned: 134 (million)
% 28.73/4.76 % (345465)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2914549668:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2973 on theBenchmark for (2973ds/431Mi)
% 28.73/4.76 % (345464)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1855033529:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2973 on theBenchmark for (2973ds/141Mi)
% 28.73/4.76 % (345464)Instruction limit reached!
% 28.73/4.76 % (345464)------------------------------
% 28.73/4.76 % (345464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.73/4.77 % (345464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.73/4.77 % (345464)CaDiCaL version: 2.1.3
% 28.73/4.77 % (345464)Termination reason: Instruction limit
% 28.73/4.77 % (345464)Termination phase: Saturation
% 28.73/4.77 % (345464)Time elapsed: 0.074 s
% 28.73/4.77 % (345464)Peak memory usage: 91 MB
% 28.73/4.77 % (345464)Instructions burned: 142 (million)
% 28.73/4.77 % (345465)Instruction limit reached!
% 28.73/4.77 % (345465)------------------------------
% 28.73/4.77 % (345465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.73/4.77 % (345465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.73/4.77 % (345465)CaDiCaL version: 2.1.3
% 28.73/4.77 % (345465)Termination reason: Instruction limit
% 28.73/4.77 % (345465)Termination phase: Saturation
% 28.73/4.77 % (345465)Time elapsed: 0.126 s
% 28.73/4.77 % (345465)Peak memory usage: 97 MB
% 28.73/4.77 % (345465)Instructions burned: 435 (million)
% 28.73/4.77 % (345468)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=1199038772:i=6060:aac=none:ins=25_2971 on theBenchmark for (2971ds/6060Mi)
% 28.73/4.77 % (345470)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=3433634709:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2971 on theBenchmark for (2971ds/150Mi)
% 28.73/4.77 % (345470)Instruction limit reached!
% 28.73/4.77 % (345470)------------------------------
% 28.73/4.77 % (345470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.73/4.77 % (345470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.73/4.77 % (345470)CaDiCaL version: 2.1.3
% 28.73/4.77 % (345470)Termination reason: Instruction limit
% 28.73/4.77 % (345470)Termination phase: Saturation
% 28.73/4.77 % (345470)Time elapsed: 0.050 s
% 28.73/4.77 % (345470)Peak memory usage: 91 MB
% 28.73/4.77 % (345470)Instructions burned: 151 (million)
% 28.73/4.77 % (345496)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=584888719:i=14155:bd=all_2969 on theBenchmark for (2969ds/14155Mi)
% 28.73/4.77 % (345429)First to succeed.
% 28.73/4.77 % (345429)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-345189"
% 28.73/4.77 % (345429)Refutation found. Thanks to Tanya!
% 28.73/4.77 % SZS status Theorem for theBenchmark
% 28.73/4.77 % SZS output start Proof for theBenchmark
% See solution above
% 29.35/4.96 % (345429)------------------------------
% 29.35/4.96 % (345429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.35/4.96 % (345429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.35/4.96 % (345429)CaDiCaL version: 2.1.3
% 29.35/4.96 % (345429)Termination reason: Refutation
% 29.35/4.96 % (345429)Time elapsed: 1.638 s
% 29.35/4.96 % (345429)Peak memory usage: 143 MB
% 29.35/4.96 % (345429)Instructions burned: 2247 (million)
% 29.35/4.96 % (345429)------------------------------
% 29.35/4.96 % (345429)------------------------------
% 29.35/4.96 % (345189)Success in time 4.075 s
% 29.35/4.96 % Vampire exiting
%------------------------------------------------------------------------------