%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW095+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n010.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:39:32 PM UTC 2026
% Result : Theorem 17.75s 2.86s
% Output : Refutation 17.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 84
% Syntax : Number of formulae : 906 ( 69 unt; 62 def)
% Number of atoms : 5506 ( 661 equ)
% Maximal formula atoms : 521 ( 6 avg)
% Number of connectives : 7554 (2954 ~;3826 |; 712 &)
% ( 62 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 86 ( 84 usr; 66 prp; 0-3 aty)
% Number of functors : 22 ( 22 usr; 16 con; 0-1 aty)
% Number of variables : 491 ( 0 sgn 411 !; 80 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
object(nn),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sort_info_nn) ).
fof(f8,axiom,
object(prev_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sort_info_prev_2) ).
fof(f10,axiom,
! [X0] : integer(node_key(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sort_info_node_key) ).
fof(f11,axiom,
object(null),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sort_info_null) ).
fof(f13,axiom,
object(sortedList_first),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sort_info_sortedList_first) ).
fof(f14,axiom,
! [X0] : object(node_next(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sort_info_node_next) ).
fof(f15,axiom,
null = node_next(null),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp_tptp_1) ).
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/sandbox2/benchmark/theBenchmark.p',hyp_tptp_2) ).
fof(f17,axiom,
! [X0,X1,X2,X3] :
( ~ ( object(X0)
& object(X1)
& object(X2)
& object(X3) )
| ~ v__1(X1,X2,X3)
| ~ v__1(X2,X0,X3)
| ( v__1(X1,X2,X0)
& v__1(X1,X0,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp_tptp_3) ).
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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',hyp_tptp_9) ).
fof(f24,axiom,
! [X0] :
( ~ object(X0)
| ! [X1,X2] :
( ~ ( object(X1)
& object(X2) )
| X1 != node_next(X0)
| X2 != node_next(X0)
| v__1(X0,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp_tptp_10) ).
fof(f26,axiom,
prev_2 != null,
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p',hyp_tptp_13) ).
fof(f28,axiom,
nn != null,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp_tptp_14) ).
fof(f31,axiom,
( prev_2 = null
| ( prev_2 != null
& v__1(sortedList_first,prev_2,prev_2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp_tptp_17) ).
fof(f32,axiom,
( nn = null
| ( nn != null
& v__1(sortedList_first,nn,nn) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp_tptp_18) ).
fof(f34,axiom,
( prev_2 = null
| nn = node_next(prev_2) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',hyp_tptp_31) ).
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/sandbox2/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(f69,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(f70,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,[],[f69]) ).
fof(f71,plain,
! [X0,X1,X2,X3] :
( ~ object(X0)
| ~ object(X1)
| ~ object(X2)
| ~ object(X3)
| ~ v__1(X1,X2,X3)
| ~ v__1(X2,X0,X3)
| ( v__1(X1,X2,X0)
& v__1(X1,X0,X3) ) ),
inference(ennf_transformation,[],[f17]) ).
fof(f72,plain,
! [X0,X1,X2,X3] :
( ~ object(X0)
| ~ object(X1)
| ~ object(X2)
| ~ object(X3)
| ~ v__1(X1,X2,X3)
| ~ v__1(X2,X0,X3)
| ( v__1(X1,X2,X0)
& v__1(X1,X0,X3) ) ),
inference(flattening,[],[f71]) ).
fof(f75,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(f76,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,[],[f75]) ).
fof(f77,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(f78,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,[],[f77]) ).
fof(f81,plain,
! [X0,X1] :
( ~ object(X0)
| ~ object(X1)
| X0 != node_next(X0)
| ~ v__1(X0,X1,X1)
| X0 = X1 ),
inference(ennf_transformation,[],[f23]) ).
fof(f82,plain,
! [X0,X1] :
( ~ object(X0)
| ~ object(X1)
| X0 != node_next(X0)
| ~ v__1(X0,X1,X1)
| X0 = X1 ),
inference(flattening,[],[f81]) ).
fof(f83,plain,
! [X0] :
( ~ object(X0)
| ! [X1,X2] :
( ~ object(X1)
| ~ object(X2)
| X1 != node_next(X0)
| X2 != node_next(X0)
| v__1(X0,X1,X2) ) ),
inference(ennf_transformation,[],[f24]) ).
fof(f84,plain,
! [X0] :
( ~ object(X0)
| ! [X1,X2] :
( ~ object(X1)
| ~ object(X2)
| X1 != node_next(X0)
| X2 != node_next(X0)
| v__1(X0,X1,X2) ) ),
inference(flattening,[],[f83]) ).
fof(f87,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(f88,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,[],[f87]) ).
fof(f89,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(f90,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,[],[f89]) ).
fof(f93,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(f101,plain,
object(nn),
inference(cnf_transformation,[],[f6]) ).
fof(f103,plain,
object(prev_2),
inference(cnf_transformation,[],[f8]) ).
fof(f105,plain,
! [X0] : integer(node_key(X0)),
inference(cnf_transformation,[],[f10]) ).
fof(f106,plain,
object(null),
inference(cnf_transformation,[],[f11]) ).
fof(f108,plain,
object(sortedList_first),
inference(cnf_transformation,[],[f13]) ).
fof(f109,plain,
! [X0] : object(node_next(X0)),
inference(cnf_transformation,[],[f14]) ).
fof(f110,plain,
null = node_next(null),
inference(cnf_transformation,[],[f15]) ).
fof(f111,plain,
! [X2,X0,X1] :
( v__1(X0,X2,X2)
| ~ v__1(X1,X2,X2)
| ~ v__1(X0,X1,X1)
| ~ object(X2)
| ~ object(X1)
| ~ object(X0) ),
inference(cnf_transformation,[],[f70]) ).
fof(f112,plain,
! [X2,X3,X0,X1] :
( v__1(X1,X0,X3)
| ~ v__1(X2,X0,X3)
| ~ v__1(X1,X2,X3)
| ~ object(X3)
| ~ object(X2)
| ~ object(X1)
| ~ object(X0) ),
inference(cnf_transformation,[],[f72]) ).
fof(f116,plain,
! [X2,X0,X1] :
( v__1(X0,X2,X1)
| v__1(X0,X1,X2)
| ~ v__1(X0,X2,X2)
| ~ v__1(X0,X1,X1)
| ~ object(X2)
| ~ object(X1)
| ~ object(X0) ),
inference(cnf_transformation,[],[f76]) ).
fof(f117,plain,
! [X2,X0,X1] :
( v__1(X1,X2,X2)
| ~ v__1(X0,X1,X2)
| ~ object(X2)
| ~ object(X1)
| ~ object(X0) ),
inference(cnf_transformation,[],[f78]) ).
fof(f118,plain,
! [X2,X0,X1] :
( v__1(X0,X1,X1)
| ~ v__1(X0,X1,X2)
| ~ object(X2)
| ~ object(X1)
| ~ object(X0) ),
inference(cnf_transformation,[],[f78]) ).
fof(f121,plain,
! [X0,X1] :
( node_next(X0) != X0
| ~ v__1(X0,X1,X1)
| X0 = X1
| ~ object(X1)
| ~ object(X0) ),
inference(cnf_transformation,[],[f82]) ).
fof(f122,plain,
! [X2,X0,X1] :
( v__1(X0,X1,X2)
| node_next(X0) != X2
| node_next(X0) != X1
| ~ object(X2)
| ~ object(X1)
| ~ object(X0) ),
inference(cnf_transformation,[],[f84]) ).
fof(f124,plain,
prev_2 != null,
inference(cnf_transformation,[],[f26]) ).
fof(f125,plain,
node_key(nn) = sK1,
inference(cnf_transformation,[],[f27]) ).
fof(f126,plain,
node_key(nn) = sK0,
inference(cnf_transformation,[],[f27]) ).
fof(f130,plain,
nn != null,
inference(cnf_transformation,[],[f28]) ).
fof(f133,plain,
( v__1(sortedList_first,prev_2,prev_2)
| prev_2 = null ),
inference(cnf_transformation,[],[f31]) ).
fof(f134,plain,
( v__1(sortedList_first,nn,nn)
| nn = null ),
inference(cnf_transformation,[],[f32]) ).
fof(f136,plain,
( nn = node_next(prev_2)
| prev_2 = null ),
inference(cnf_transformation,[],[f34]) ).
fof(f146,plain,
! [X2,X0,X1,X5] :
( node_key(X1) != X5
| node_key(X0) != X5
| ~ integer(X5)
| null = X1
| node_next(X0) != X2
| ~ v__1(X2,X1,X1)
| ~ object(X2)
| null = X0
| ~ v__1(sortedList_first,X0,X0)
| ~ object(X1)
| ~ object(X0) ),
inference(cnf_transformation,[],[f88]) ).
fof(f147,plain,
! [X0,X1] :
( v__1(sortedList_first,X1,X1)
| node_next(X0) != X1
| null = X1
| null = X0
| ~ object(X1)
| ~ object(X0) ),
inference(cnf_transformation,[],[f90]) ).
fof(f269,plain,
! [X0] :
( node_next(nn) = sK114
| v__1(sK100(X0),X0,nn)
| ~ sP29(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f272,plain,
! [X0] :
( node_next(nn) = sK114
| node_next(nn) = sK100(X0)
| ~ sP29(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f355,plain,
( node_next(nn) = sK96
| ~ sP66 ),
inference(cnf_transformation,[],[f93]) ).
fof(f357,plain,
( node_next(nn) = sK95
| ~ sP65 ),
inference(cnf_transformation,[],[f93]) ).
fof(f358,plain,
( v__1(sK95,nn,nn)
| ~ sP65 ),
inference(cnf_transformation,[],[f93]) ).
fof(f549,plain,
! [X0] :
( ~ v__1(sK81,nn,nn)
| v__1(sK49(X0),X0,nn)
| ~ sP8(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f550,plain,
! [X0] :
( node_next(nn) = sK81
| v__1(sK49(X0),X0,nn)
| ~ sP8(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f553,plain,
! [X0] :
( node_next(nn) = sK81
| node_next(nn) = sK49(X0)
| ~ sP8(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f582,plain,
! [X0] :
( node_next(nn) = sK76
| v__1(sK45,prev_2,nn)
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f583,plain,
! [X0] :
( v__1(sK76,prev_2,prev_2)
| v__1(sK45,prev_2,nn)
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f585,plain,
! [X0] :
( node_next(nn) = sK76
| node_next(nn) = sK45
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f586,plain,
! [X0] :
( v__1(sK76,prev_2,prev_2)
| node_next(nn) = sK45
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f588,plain,
! [X0] :
( ~ v__1(sK75,nn,nn)
| object(sK45)
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f591,plain,
! [X0] :
( ~ v__1(sK75,nn,nn)
| v__1(sK45,prev_2,nn)
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f592,plain,
! [X0] :
( node_next(nn) = sK75
| v__1(sK45,prev_2,nn)
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f593,plain,
! [X0] :
( object(sK75)
| v__1(sK45,prev_2,nn)
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f595,plain,
! [X0] :
( node_next(nn) = sK75
| node_next(nn) = sK45
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f596,plain,
! [X0] :
( object(sK75)
| node_next(nn) = sK45
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f633,plain,
! [X0] :
( ~ sP29(X0)
| node_next(nn) = sK70(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f634,plain,
! [X0] :
( v__1(sK70(X0),X0,X0)
| ~ sP29(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f640,plain,
! [X0] :
( v__1(null,X0,nn)
| v__1(null,X0,X0)
| ~ sP28(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f666,plain,
! [X68] :
( ~ sP67(X68)
| node_next(nn) = X68 ),
inference(cnf_transformation,[],[f93]) ).
fof(f667,plain,
! [X68] :
( ~ sP67(X68)
| object(X68) ),
inference(cnf_transformation,[],[f93]) ).
fof(f723,plain,
! [X0] :
( v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn)
| ~ sP23(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f727,plain,
( v__1(null,prev_2,prev_2)
| ~ sP59 ),
inference(cnf_transformation,[],[f93]) ).
fof(f847,plain,
! [X0] :
( v__1(null,X0,nn)
| v__1(null,X0,X0)
| sP25(X0)
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f874,plain,
! [X0] :
( ~ v__1(sortedList_first,prev_2,nn)
| ~ v__1(sortedList_first,prev_2,prev_2)
| sP59
| v__1(null,prev_2,nn)
| sP23(X0)
| sP24(X0)
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f900,plain,
! [X0] :
( v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn)
| ~ sP17(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f904,plain,
! [X0] :
( v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn)
| ~ sP16(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f958,plain,
! [X0] :
( ~ sP8(X0)
| node_next(nn) = sK34(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f959,plain,
! [X0] :
( v__1(sK34(X0),X0,X0)
| ~ sP8(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f965,plain,
! [X0] :
( v__1(null,X0,nn)
| v__1(null,X0,X0)
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f997,plain,
! [X0] :
( v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn)
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f999,plain,
! [X0] :
( v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn)
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f1005,plain,
( sP67(sK42)
| node_next(nn) = sK27
| sP4(sK2)
| sP5(sK2)
| sP6(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2) ),
inference(cnf_transformation,[],[f93]) ).
fof(f1006,plain,
( sP67(sK42)
| object(sK27)
| sP4(sK2)
| sP5(sK2)
| sP6(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2) ),
inference(cnf_transformation,[],[f93]) ).
fof(f1020,plain,
( sP65
| sP66
| node_next(nn) = sK27
| sP4(sK2)
| sP5(sK2)
| sP6(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2) ),
inference(cnf_transformation,[],[f93]) ).
fof(f1021,plain,
( sP65
| sP66
| object(sK27)
| sP4(sK2)
| sP5(sK2)
| sP6(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2) ),
inference(cnf_transformation,[],[f93]) ).
fof(f1025,plain,
! [X0] :
( v__1(sortedList_first,X0,X0)
| ~ sP25(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f1026,plain,
! [X0] :
( v__1(sortedList_first,X0,prev_2)
| ~ sP24(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f1054,plain,
( v__1(null,sK2,sK2)
| v__1(null,sK2,nn)
| sP7(sK2)
| sP8(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2) ),
inference(cnf_transformation,[],[f93]) ).
fof(f1061,plain,
( v__1(null,sK2,sK2)
| sP28(sK2)
| sP29(sK2)
| sP4(sK2)
| sP5(sK2)
| sP6(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2) ),
inference(cnf_transformation,[],[f93]) ).
fof(f1074,plain,
! [X0] :
( v__1(sortedList_first,X0,prev_2)
| ~ sP18(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f1096,plain,
( nn != sK2
| sP7(sK2)
| sP8(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2) ),
inference(cnf_transformation,[],[f93]) ).
fof(f1103,plain,
( nn = sK2
| ~ v__1(sortedList_first,sK2,sK2)
| null = sK2 ),
inference(cnf_transformation,[],[f93]) ).
fof(f1104,plain,
null != sK2,
inference(cnf_transformation,[],[f93]) ).
fof(f1105,plain,
object(sK2),
inference(cnf_transformation,[],[f93]) ).
fof(f1107,plain,
! [X0,X1] :
( v__1(X0,X1,node_next(X0))
| node_next(X0) != X1
| ~ object(node_next(X0))
| ~ object(X1)
| ~ object(X0) ),
inference(equality_resolution,[],[f122]) ).
fof(f1108,plain,
! [X0] :
( v__1(X0,node_next(X0),node_next(X0))
| ~ object(node_next(X0))
| ~ object(node_next(X0))
| ~ object(X0) ),
inference(equality_resolution,[],[f1107]) ).
fof(f1110,plain,
! [X2,X0,X1] :
( node_key(X0) != node_key(X1)
| ~ integer(node_key(X1))
| null = X1
| node_next(X0) != X2
| ~ v__1(X2,X1,X1)
| ~ object(X2)
| null = X0
| ~ v__1(sortedList_first,X0,X0)
| ~ object(X1)
| ~ object(X0) ),
inference(equality_resolution,[],[f146]) ).
fof(f1111,plain,
! [X0,X1] :
( node_key(X0) != node_key(X1)
| ~ integer(node_key(X1))
| null = X1
| ~ v__1(node_next(X0),X1,X1)
| ~ object(node_next(X0))
| null = X0
| ~ v__1(sortedList_first,X0,X0)
| ~ object(X1)
| ~ object(X0) ),
inference(equality_resolution,[],[f1110]) ).
fof(f1115,plain,
! [X0] :
( v__1(sortedList_first,node_next(X0),node_next(X0))
| null = node_next(X0)
| null = X0
| ~ object(node_next(X0))
| ~ object(X0) ),
inference(equality_resolution,[],[f147]) ).
fof(f1172,plain,
! [X0] :
( v__1(X0,node_next(X0),node_next(X0))
| ~ object(node_next(X0))
| ~ object(X0) ),
inference(duplicate_literal_removal,[],[f1108]) ).
fof(f1175,definition,
( spl129_1
<=> sP66 ),
introduced(definition,[new_symbols(definition,[spl129_1])],[avatar_definition]) ).
fof(f1176,plain,
( sP66
| ~ spl129_1 ),
inference(avatar_component_clause,[],[f1175]) ).
fof(f1177,plain,
( ~ sP66
| spl129_1 ),
inference(avatar_component_clause,[],[f1175]) ).
fof(f1184,definition,
( spl129_3
<=> sP65 ),
introduced(definition,[new_symbols(definition,[spl129_3])],[avatar_definition]) ).
fof(f1185,plain,
( sP65
| ~ spl129_3 ),
inference(avatar_component_clause,[],[f1184]) ).
fof(f1186,plain,
( ~ sP65
| spl129_3 ),
inference(avatar_component_clause,[],[f1184]) ).
fof(f1233,definition,
( spl129_14
<=> v__1(sortedList_first,prev_2,prev_2) ),
introduced(definition,[new_symbols(definition,[spl129_14])],[avatar_definition]) ).
fof(f1234,plain,
( v__1(sortedList_first,prev_2,prev_2)
| ~ spl129_14 ),
inference(avatar_component_clause,[],[f1233]) ).
fof(f1235,plain,
( ~ v__1(sortedList_first,prev_2,prev_2)
| spl129_14 ),
inference(avatar_component_clause,[],[f1233]) ).
fof(f1238,definition,
( spl129_15
<=> sP59 ),
introduced(definition,[new_symbols(definition,[spl129_15])],[avatar_definition]) ).
fof(f1239,plain,
( sP59
| ~ spl129_15 ),
inference(avatar_component_clause,[],[f1238]) ).
fof(f1240,plain,
( ~ sP59
| spl129_15 ),
inference(avatar_component_clause,[],[f1238]) ).
fof(f1242,definition,
( spl129_16
<=> v__1(null,nn,nn) ),
introduced(definition,[new_symbols(definition,[spl129_16])],[avatar_definition]) ).
fof(f1243,plain,
( v__1(null,nn,nn)
| ~ spl129_16 ),
inference(avatar_component_clause,[],[f1242]) ).
fof(f1244,plain,
( ~ v__1(null,nn,nn)
| spl129_16 ),
inference(avatar_component_clause,[],[f1242]) ).
fof(f1257,definition,
( spl129_19
<=> ! [X0] : ~ sP23(X0) ),
introduced(definition,[new_symbols(definition,[spl129_19])],[avatar_definition]) ).
fof(f1258,plain,
( ! [X0] : ~ sP23(X0)
| ~ spl129_19 ),
inference(avatar_component_clause,[],[f1257]) ).
fof(f1261,definition,
( spl129_20
<=> sP3(sK2) ),
introduced(definition,[new_symbols(definition,[spl129_20])],[avatar_definition]) ).
fof(f1262,plain,
( ~ sP3(sK2)
| spl129_20 ),
inference(avatar_component_clause,[],[f1261]) ).
fof(f1263,plain,
( sP3(sK2)
| ~ spl129_20 ),
inference(avatar_component_clause,[],[f1261]) ).
fof(f1327,definition,
( spl129_34
<=> ! [X0] : ~ sP6(X0) ),
introduced(definition,[new_symbols(definition,[spl129_34])],[avatar_definition]) ).
fof(f1328,plain,
( ! [X0] : ~ sP6(X0)
| ~ spl129_34 ),
inference(avatar_component_clause,[],[f1327]) ).
fof(f1330,definition,
( spl129_35
<=> object(sK45) ),
introduced(definition,[new_symbols(definition,[spl129_35])],[avatar_definition]) ).
fof(f1331,plain,
( ~ object(sK45)
| spl129_35 ),
inference(avatar_component_clause,[],[f1330]) ).
fof(f1332,plain,
( object(sK45)
| ~ spl129_35 ),
inference(avatar_component_clause,[],[f1330]) ).
fof(f1339,definition,
( spl129_37
<=> ! [X0] : ~ sP5(X0) ),
introduced(definition,[new_symbols(definition,[spl129_37])],[avatar_definition]) ).
fof(f1340,plain,
( ! [X0] : ~ sP5(X0)
| ~ spl129_37 ),
inference(avatar_component_clause,[],[f1339]) ).
fof(f1351,definition,
( spl129_40
<=> ! [X0] : ~ sP4(X0) ),
introduced(definition,[new_symbols(definition,[spl129_40])],[avatar_definition]) ).
fof(f1352,plain,
( ! [X0] : ~ sP4(X0)
| ~ spl129_40 ),
inference(avatar_component_clause,[],[f1351]) ).
fof(f1408,definition,
( spl129_49
<=> v__1(sortedList_first,prev_2,nn) ),
introduced(definition,[new_symbols(definition,[spl129_49])],[avatar_definition]) ).
fof(f1409,plain,
( ~ v__1(sortedList_first,prev_2,nn)
| spl129_49 ),
inference(avatar_component_clause,[],[f1408]) ).
fof(f1410,plain,
( v__1(sortedList_first,prev_2,nn)
| ~ spl129_49 ),
inference(avatar_component_clause,[],[f1408]) ).
fof(f1498,definition,
( spl129_61
<=> object(sK114) ),
introduced(definition,[new_symbols(definition,[spl129_61])],[avatar_definition]) ).
fof(f1499,plain,
( ~ object(sK114)
| spl129_61 ),
inference(avatar_component_clause,[],[f1498]) ).
fof(f1500,plain,
( object(sK114)
| ~ spl129_61 ),
inference(avatar_component_clause,[],[f1498]) ).
fof(f1754,definition,
( spl129_101
<=> ! [X0] :
( v__1(sK100(X0),X0,nn)
| ~ sP29(X0) ) ),
introduced(definition,[new_symbols(definition,[spl129_101])],[avatar_definition]) ).
fof(f1755,plain,
( ! [X0] :
( v__1(sK100(X0),X0,nn)
| ~ sP29(X0) )
| ~ spl129_101 ),
inference(avatar_component_clause,[],[f1754]) ).
fof(f1762,definition,
( spl129_103
<=> ! [X0] :
( v__1(sK49(X0),X0,nn)
| ~ sP8(X0) ) ),
introduced(definition,[new_symbols(definition,[spl129_103])],[avatar_definition]) ).
fof(f1763,plain,
( ! [X0] :
( v__1(sK49(X0),X0,nn)
| ~ sP8(X0) )
| ~ spl129_103 ),
inference(avatar_component_clause,[],[f1762]) ).
fof(f1773,definition,
( spl129_106
<=> v__1(sortedList_first,nn,nn) ),
introduced(definition,[new_symbols(definition,[spl129_106])],[avatar_definition]) ).
fof(f1774,plain,
( v__1(sortedList_first,nn,nn)
| ~ spl129_106 ),
inference(avatar_component_clause,[],[f1773]) ).
fof(f1775,plain,
( ~ v__1(sortedList_first,nn,nn)
| spl129_106 ),
inference(avatar_component_clause,[],[f1773]) ).
fof(f1822,definition,
( spl129_109
<=> v__1(null,prev_2,prev_2) ),
introduced(definition,[new_symbols(definition,[spl129_109])],[avatar_definition]) ).
fof(f1823,plain,
( ~ v__1(null,prev_2,prev_2)
| spl129_109 ),
inference(avatar_component_clause,[],[f1822]) ).
fof(f1824,plain,
( v__1(null,prev_2,prev_2)
| ~ spl129_109 ),
inference(avatar_component_clause,[],[f1822]) ).
fof(f1836,definition,
( spl129_110
<=> v__1(sortedList_first,nn,prev_2) ),
introduced(definition,[new_symbols(definition,[spl129_110])],[avatar_definition]) ).
fof(f1837,plain,
( ~ v__1(sortedList_first,nn,prev_2)
| spl129_110 ),
inference(avatar_component_clause,[],[f1836]) ).
fof(f1838,plain,
( v__1(sortedList_first,nn,prev_2)
| ~ spl129_110 ),
inference(avatar_component_clause,[],[f1836]) ).
fof(f1907,definition,
( spl129_111
<=> ! [X0] : ~ sP17(X0) ),
introduced(definition,[new_symbols(definition,[spl129_111])],[avatar_definition]) ).
fof(f1908,plain,
( ! [X0] : ~ sP17(X0)
| ~ spl129_111 ),
inference(avatar_component_clause,[],[f1907]) ).
fof(f1960,definition,
( spl129_112
<=> v__1(null,prev_2,nn) ),
introduced(definition,[new_symbols(definition,[spl129_112])],[avatar_definition]) ).
fof(f1961,plain,
( ~ v__1(null,prev_2,nn)
| spl129_112 ),
inference(avatar_component_clause,[],[f1960]) ).
fof(f1962,plain,
( v__1(null,prev_2,nn)
| ~ spl129_112 ),
inference(avatar_component_clause,[],[f1960]) ).
fof(f1963,plain,
( spl129_111
| spl129_112
| spl129_109 ),
inference(avatar_split_clause,[],[f900,f1822,f1960,f1907]) ).
fof(f2114,plain,
( nn = sK2
| ~ v__1(sortedList_first,sK2,sK2) ),
inference(forward_subsumption_resolution,[],[f1103,f1104]) ).
fof(f2116,definition,
( spl129_113
<=> v__1(sortedList_first,sK2,sK2) ),
introduced(definition,[new_symbols(definition,[spl129_113])],[avatar_definition]) ).
fof(f2117,plain,
( v__1(sortedList_first,sK2,sK2)
| ~ spl129_113 ),
inference(avatar_component_clause,[],[f2116]) ).
fof(f2118,plain,
( ~ v__1(sortedList_first,sK2,sK2)
| spl129_113 ),
inference(avatar_component_clause,[],[f2116]) ).
fof(f2120,definition,
( spl129_114
<=> nn = sK2 ),
introduced(definition,[new_symbols(definition,[spl129_114])],[avatar_definition]) ).
fof(f2122,plain,
( nn = sK2
| ~ spl129_114 ),
inference(avatar_component_clause,[],[f2120]) ).
fof(f2123,plain,
( ~ spl129_113
| spl129_114 ),
inference(avatar_split_clause,[],[f2114,f2120,f2116]) ).
fof(f2124,plain,
( ~ sP25(sK2)
| spl129_113 ),
inference(resolution,[],[f2118,f1025]) ).
fof(f2157,definition,
( spl129_119
<=> v__1(sK114,nn,nn) ),
introduced(definition,[new_symbols(definition,[spl129_119])],[avatar_definition]) ).
fof(f2158,plain,
( v__1(sK114,nn,nn)
| ~ spl129_119 ),
inference(avatar_component_clause,[],[f2157]) ).
fof(f2159,plain,
( ~ v__1(sK114,nn,nn)
| spl129_119 ),
inference(avatar_component_clause,[],[f2157]) ).
fof(f2190,definition,
( spl129_123
<=> ! [X0] :
( node_next(nn) = sK100(X0)
| ~ sP29(X0) ) ),
introduced(definition,[new_symbols(definition,[spl129_123])],[avatar_definition]) ).
fof(f2191,plain,
( ! [X0] :
( ~ sP29(X0)
| node_next(nn) = sK100(X0) )
| ~ spl129_123 ),
inference(avatar_component_clause,[],[f2190]) ).
fof(f2193,definition,
( spl129_124
<=> node_next(nn) = sK114 ),
introduced(definition,[new_symbols(definition,[spl129_124])],[avatar_definition]) ).
fof(f2194,plain,
( node_next(nn) != sK114
| spl129_124 ),
inference(avatar_component_clause,[],[f2193]) ).
fof(f2195,plain,
( node_next(nn) = sK114
| ~ spl129_124 ),
inference(avatar_component_clause,[],[f2193]) ).
fof(f2196,plain,
( spl129_123
| spl129_124 ),
inference(avatar_split_clause,[],[f272,f2193,f2190]) ).
fof(f2223,definition,
( spl129_129
<=> v__1(sK81,nn,nn) ),
introduced(definition,[new_symbols(definition,[spl129_129])],[avatar_definition]) ).
fof(f2224,plain,
( v__1(sK81,nn,nn)
| ~ spl129_129 ),
inference(avatar_component_clause,[],[f2223]) ).
fof(f2225,plain,
( ~ v__1(sK81,nn,nn)
| spl129_129 ),
inference(avatar_component_clause,[],[f2223]) ).
fof(f2226,plain,
( spl129_103
| ~ spl129_129 ),
inference(avatar_split_clause,[],[f549,f2223,f1762]) ).
fof(f2232,definition,
( spl129_130
<=> node_next(nn) = sK81 ),
introduced(definition,[new_symbols(definition,[spl129_130])],[avatar_definition]) ).
fof(f2234,plain,
( node_next(nn) = sK81
| ~ spl129_130 ),
inference(avatar_component_clause,[],[f2232]) ).
fof(f2235,plain,
( spl129_103
| spl129_130 ),
inference(avatar_split_clause,[],[f550,f2232,f1762]) ).
fof(f2244,definition,
( spl129_131
<=> ! [X0] :
( node_next(nn) = sK49(X0)
| ~ sP8(X0) ) ),
introduced(definition,[new_symbols(definition,[spl129_131])],[avatar_definition]) ).
fof(f2245,plain,
( ! [X0] :
( ~ sP8(X0)
| node_next(nn) = sK49(X0) )
| ~ spl129_131 ),
inference(avatar_component_clause,[],[f2244]) ).
fof(f2246,plain,
( spl129_131
| spl129_130 ),
inference(avatar_split_clause,[],[f553,f2232,f2244]) ).
fof(f2401,definition,
( spl129_137
<=> sP18(sK2) ),
introduced(definition,[new_symbols(definition,[spl129_137])],[avatar_definition]) ).
fof(f2402,plain,
( ~ sP18(sK2)
| spl129_137 ),
inference(avatar_component_clause,[],[f2401]) ).
fof(f2403,plain,
( sP18(sK2)
| ~ spl129_137 ),
inference(avatar_component_clause,[],[f2401]) ).
fof(f2405,definition,
( spl129_138
<=> sP17(sK2) ),
introduced(definition,[new_symbols(definition,[spl129_138])],[avatar_definition]) ).
fof(f2407,plain,
( sP17(sK2)
| ~ spl129_138 ),
inference(avatar_component_clause,[],[f2405]) ).
fof(f2409,definition,
( spl129_139
<=> sP16(sK2) ),
introduced(definition,[new_symbols(definition,[spl129_139])],[avatar_definition]) ).
fof(f2410,plain,
( ~ sP16(sK2)
| spl129_139 ),
inference(avatar_component_clause,[],[f2409]) ).
fof(f2411,plain,
( sP16(sK2)
| ~ spl129_139 ),
inference(avatar_component_clause,[],[f2409]) ).
fof(f2413,definition,
( spl129_140
<=> sP8(sK2) ),
introduced(definition,[new_symbols(definition,[spl129_140])],[avatar_definition]) ).
fof(f2414,plain,
( ~ sP8(sK2)
| spl129_140 ),
inference(avatar_component_clause,[],[f2413]) ).
fof(f2415,plain,
( sP8(sK2)
| ~ spl129_140 ),
inference(avatar_component_clause,[],[f2413]) ).
fof(f2417,definition,
( spl129_141
<=> sP7(sK2) ),
introduced(definition,[new_symbols(definition,[spl129_141])],[avatar_definition]) ).
fof(f2419,plain,
( sP7(sK2)
| ~ spl129_141 ),
inference(avatar_component_clause,[],[f2417]) ).
fof(f2420,plain,
( spl129_20
| spl129_137
| spl129_138
| spl129_139
| spl129_140
| spl129_141
| ~ spl129_114 ),
inference(avatar_split_clause,[],[f1096,f2120,f2417,f2413,f2409,f2405,f2401,f1261]) ).
fof(f2986,plain,
( v__1(null,sK2,sK2)
| v__1(null,sK2,nn)
| sP8(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2) ),
inference(forward_subsumption_resolution,[],[f1054,f965]) ).
fof(f3092,definition,
( spl129_150
<=> v__1(null,sK2,sK2) ),
introduced(definition,[new_symbols(definition,[spl129_150])],[avatar_definition]) ).
fof(f3093,plain,
( v__1(null,sK2,sK2)
| ~ spl129_150 ),
inference(avatar_component_clause,[],[f3092]) ).
fof(f3094,plain,
( ~ v__1(null,sK2,sK2)
| spl129_150 ),
inference(avatar_component_clause,[],[f3092]) ).
fof(f3639,plain,
( v__1(null,prev_2,prev_2)
| ~ spl129_15 ),
inference(forward_subsumption_resolution,[],[f727,f1239]) ).
fof(f3670,plain,
( spl129_109
| ~ spl129_15 ),
inference(avatar_split_clause,[],[f3639,f1238,f1822]) ).
fof(f3770,plain,
sK0 = sK1,
inference(superposition,[],[f126,f125]) ).
fof(f3818,plain,
nn = node_next(prev_2),
inference(forward_subsumption_resolution,[],[f136,f124]) ).
fof(f3920,plain,
! [X0] :
( v__1(X0,node_next(X0),node_next(X0))
| ~ object(X0) ),
inference(forward_subsumption_resolution,[],[f1172,f109]) ).
fof(f3957,plain,
( v__1(prev_2,nn,nn)
| ~ object(prev_2) ),
inference(superposition,[],[f3920,f3818]) ).
fof(f3958,plain,
v__1(prev_2,nn,nn),
inference(forward_subsumption_resolution,[],[f3957,f103]) ).
fof(f4121,plain,
( ! [X0] :
( ~ v__1(sortedList_first,sK2,X0)
| ~ object(X0)
| ~ object(sK2)
| ~ object(sortedList_first) )
| spl129_113 ),
inference(resolution,[],[f118,f2118]) ).
fof(f4129,plain,
( ! [X0] :
( ~ v__1(sortedList_first,sK2,X0)
| ~ object(X0)
| ~ object(sortedList_first) )
| spl129_113 ),
inference(forward_subsumption_resolution,[],[f4121,f1105]) ).
fof(f4142,plain,
( ! [X0] :
( ~ v__1(sortedList_first,sK2,X0)
| ~ object(X0) )
| spl129_113 ),
inference(forward_subsumption_resolution,[],[f4129,f108]) ).
fof(f4149,plain,
! [X0] :
( null != null
| ~ v__1(null,X0,X0)
| null = X0
| ~ object(X0)
| ~ object(null) ),
inference(superposition,[],[f121,f110]) ).
fof(f4151,plain,
! [X0] :
( ~ v__1(null,X0,X0)
| null = X0
| ~ object(X0)
| ~ object(null) ),
inference(trivial_inequality_removal,[],[f4149]) ).
fof(f4152,plain,
! [X0] :
( ~ v__1(null,X0,X0)
| null = X0
| ~ object(X0) ),
inference(forward_subsumption_resolution,[],[f4151,f106]) ).
fof(f4253,plain,
! [X0] :
( v__1(sortedList_first,node_next(X0),node_next(X0))
| null = node_next(X0)
| null = X0
| ~ object(X0) ),
inference(forward_subsumption_resolution,[],[f1115,f109]) ).
fof(f4370,plain,
( ! [X0] :
( ~ v__1(X0,nn,nn)
| ~ v__1(null,X0,nn)
| ~ object(nn)
| ~ object(X0)
| ~ object(null)
| ~ object(nn) )
| spl129_16 ),
inference(resolution,[],[f112,f1244]) ).
fof(f4461,plain,
( ! [X0] :
( ~ v__1(X0,nn,nn)
| ~ v__1(null,X0,nn)
| ~ object(nn)
| ~ object(X0)
| ~ object(null) )
| spl129_16 ),
inference(duplicate_literal_removal,[],[f4370]) ).
fof(f4503,plain,
( ! [X0] :
( ~ v__1(null,X0,nn)
| ~ object(nn)
| ~ object(X0)
| ~ object(null) )
| spl129_16 ),
inference(forward_subsumption_resolution,[],[f4461,f117]) ).
fof(f4518,plain,
( ! [X0] :
( ~ v__1(null,X0,nn)
| ~ object(X0)
| ~ object(null) )
| spl129_16 ),
inference(forward_subsumption_resolution,[],[f4503,f101]) ).
fof(f4533,plain,
( ! [X0] :
( ~ v__1(null,X0,nn)
| ~ object(X0) )
| spl129_16 ),
inference(forward_subsumption_resolution,[],[f4518,f106]) ).
fof(f5134,plain,
! [X0,X1] :
( node_key(X0) != node_key(X1)
| null = X1
| ~ v__1(node_next(X0),X1,X1)
| ~ object(node_next(X0))
| null = X0
| ~ v__1(sortedList_first,X0,X0)
| ~ object(X1)
| ~ object(X0) ),
inference(forward_subsumption_resolution,[],[f1111,f105]) ).
fof(f5135,plain,
! [X0,X1] :
( node_key(X0) != node_key(X1)
| null = X1
| ~ v__1(node_next(X0),X1,X1)
| null = X0
| ~ v__1(sortedList_first,X0,X0)
| ~ object(X1)
| ~ object(X0) ),
inference(forward_subsumption_resolution,[],[f5134,f109]) ).
fof(f5136,plain,
! [X0] :
( node_key(X0) != sK0
| null = X0
| ~ v__1(node_next(nn),X0,X0)
| nn = null
| ~ v__1(sortedList_first,nn,nn)
| ~ object(X0)
| ~ object(nn) ),
inference(superposition,[],[f5135,f126]) ).
fof(f5140,plain,
! [X0] :
( null = X0
| ~ v__1(node_next(X0),X0,X0)
| null = X0
| ~ v__1(sortedList_first,X0,X0)
| ~ object(X0)
| ~ object(X0) ),
inference(equality_resolution,[],[f5135]) ).
fof(f5141,plain,
! [X0] :
( ~ v__1(node_next(X0),X0,X0)
| null = X0
| ~ v__1(sortedList_first,X0,X0)
| ~ object(X0) ),
inference(duplicate_literal_removal,[],[f5140]) ).
fof(f5145,plain,
! [X0] :
( node_key(X0) != sK0
| null = X0
| ~ v__1(node_next(nn),X0,X0)
| ~ v__1(sortedList_first,nn,nn)
| ~ object(X0)
| ~ object(nn) ),
inference(forward_subsumption_resolution,[],[f5136,f130]) ).
fof(f5443,plain,
( ~ object(prev_2)
| ~ sP18(sK2)
| spl129_113 ),
inference(resolution,[],[f4142,f1074]) ).
fof(f5630,plain,
( ~ object(prev_2)
| spl129_16
| ~ spl129_112 ),
inference(resolution,[],[f4533,f1962]) ).
fof(f5666,plain,
( $false
| spl129_16
| ~ spl129_112 ),
inference(forward_subsumption_resolution,[],[f5630,f103]) ).
fof(f5667,plain,
( spl129_16
| ~ spl129_112 ),
inference(avatar_contradiction_clause,[],[f5666]) ).
fof(f5672,plain,
( ! [X0] :
( v__1(null,prev_2,nn)
| ~ sP23(X0) )
| spl129_109 ),
inference(forward_subsumption_resolution,[],[f723,f1823]) ).
fof(f5673,plain,
( ! [X0] :
( v__1(null,prev_2,nn)
| ~ sP16(X0) )
| spl129_109 ),
inference(forward_subsumption_resolution,[],[f904,f1823]) ).
fof(f5702,plain,
( ! [X0] : ~ sP23(X0)
| spl129_109
| spl129_112 ),
inference(forward_subsumption_resolution,[],[f5672,f1961]) ).
fof(f5703,plain,
( spl129_19
| spl129_109
| spl129_112 ),
inference(avatar_split_clause,[],[f5702,f1960,f1822,f1257]) ).
fof(f5705,plain,
( ! [X0] : ~ sP16(X0)
| spl129_109
| spl129_112 ),
inference(forward_subsumption_resolution,[],[f5673,f1961]) ).
fof(f7359,plain,
( ~ v__1(sortedList_first,prev_2,sK2)
| spl129_49
| ~ spl129_114 ),
inference(superposition,[],[f1409,f2122]) ).
fof(f7392,plain,
( v__1(sortedList_first,sK2,prev_2)
| ~ spl129_110
| ~ spl129_114 ),
inference(superposition,[],[f1838,f2122]) ).
fof(f13811,plain,
( ~ v__1(nn,prev_2,prev_2)
| prev_2 = null
| ~ v__1(sortedList_first,prev_2,prev_2)
| ~ object(prev_2) ),
inference(superposition,[],[f5141,f3818]) ).
fof(f13820,plain,
( ~ v__1(nn,prev_2,prev_2)
| ~ v__1(sortedList_first,prev_2,prev_2)
| ~ object(prev_2) ),
inference(forward_subsumption_resolution,[],[f13811,f124]) ).
fof(f13836,plain,
( ~ v__1(nn,prev_2,prev_2)
| ~ object(prev_2)
| ~ spl129_14 ),
inference(forward_subsumption_resolution,[],[f13820,f1234]) ).
fof(f13846,plain,
( ~ v__1(nn,prev_2,prev_2)
| ~ spl129_14 ),
inference(forward_subsumption_resolution,[],[f13836,f103]) ).
fof(f13855,plain,
( ~ v__1(sK2,prev_2,prev_2)
| ~ spl129_14
| ~ spl129_114 ),
inference(forward_demodulation,[],[f13846,f2122]) ).
fof(f15829,plain,
( ! [X0] :
( ~ v__1(X0,sK2,prev_2)
| ~ object(prev_2)
| ~ object(sK2)
| ~ object(X0) )
| ~ spl129_14
| ~ spl129_114 ),
inference(resolution,[],[f13855,f117]) ).
fof(f15844,plain,
( ! [X0] :
( ~ v__1(X0,sK2,prev_2)
| ~ object(sK2)
| ~ object(X0) )
| ~ spl129_14
| ~ spl129_114 ),
inference(forward_subsumption_resolution,[],[f15829,f103]) ).
fof(f15851,plain,
( ! [X0] :
( ~ v__1(X0,sK2,prev_2)
| ~ object(X0) )
| ~ spl129_14
| ~ spl129_114 ),
inference(forward_subsumption_resolution,[],[f15844,f1105]) ).
fof(f17834,plain,
( ~ object(sortedList_first)
| ~ spl129_14
| ~ spl129_110
| ~ spl129_114 ),
inference(resolution,[],[f15851,f7392]) ).
fof(f17852,plain,
( $false
| ~ spl129_14
| ~ spl129_110
| ~ spl129_114 ),
inference(forward_subsumption_resolution,[],[f17834,f108]) ).
fof(f17853,plain,
( ~ spl129_14
| ~ spl129_110
| ~ spl129_114 ),
inference(avatar_contradiction_clause,[],[f17852]) ).
fof(f17918,plain,
( sP66
| object(sK27)
| sP4(sK2)
| sP5(sK2)
| sP6(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| spl129_3 ),
inference(forward_subsumption_resolution,[],[f1021,f1186]) ).
fof(f17935,plain,
( sP66
| node_next(nn) = sK27
| sP4(sK2)
| sP5(sK2)
| sP6(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| spl129_3 ),
inference(forward_subsumption_resolution,[],[f1020,f1186]) ).
fof(f18033,plain,
( object(sK27)
| sP4(sK2)
| sP5(sK2)
| sP6(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| spl129_1
| spl129_3 ),
inference(forward_subsumption_resolution,[],[f17918,f1177]) ).
fof(f18422,plain,
( node_next(nn) = sK49(sK2)
| ~ spl129_131
| ~ spl129_140 ),
inference(resolution,[],[f2415,f2245]) ).
fof(f18460,definition,
( spl129_186
<=> sP29(sK2) ),
introduced(definition,[new_symbols(definition,[spl129_186])],[avatar_definition]) ).
fof(f18461,plain,
( ~ sP29(sK2)
| spl129_186 ),
inference(avatar_component_clause,[],[f18460]) ).
fof(f18462,plain,
( sP29(sK2)
| ~ spl129_186 ),
inference(avatar_component_clause,[],[f18460]) ).
fof(f18464,definition,
( spl129_187
<=> sP28(sK2) ),
introduced(definition,[new_symbols(definition,[spl129_187])],[avatar_definition]) ).
fof(f18465,plain,
( ~ sP28(sK2)
| spl129_187 ),
inference(avatar_component_clause,[],[f18464]) ).
fof(f18466,plain,
( sP28(sK2)
| ~ spl129_187 ),
inference(avatar_component_clause,[],[f18464]) ).
fof(f18468,plain,
( node_next(nn) = sK100(sK2)
| ~ spl129_123
| ~ spl129_186 ),
inference(resolution,[],[f18462,f2191]) ).
fof(f18681,plain,
( null = sK2
| ~ object(sK2)
| ~ spl129_150 ),
inference(resolution,[],[f3093,f4152]) ).
fof(f18730,plain,
( ~ object(sK2)
| ~ spl129_150 ),
inference(forward_subsumption_resolution,[],[f18681,f1104]) ).
fof(f18734,plain,
( $false
| ~ spl129_150 ),
inference(forward_subsumption_resolution,[],[f18730,f1105]) ).
fof(f18735,plain,
~ spl129_150,
inference(avatar_contradiction_clause,[],[f18734]) ).
fof(f19256,plain,
( nn = null
| ~ object(nn)
| ~ spl129_16 ),
inference(resolution,[],[f1243,f4152]) ).
fof(f19318,plain,
( ~ object(nn)
| ~ spl129_16 ),
inference(forward_subsumption_resolution,[],[f19256,f130]) ).
fof(f19322,plain,
( $false
| ~ spl129_16 ),
inference(forward_subsumption_resolution,[],[f19318,f101]) ).
fof(f19323,plain,
~ spl129_16,
inference(avatar_contradiction_clause,[],[f19322]) ).
fof(f19394,plain,
v__1(sortedList_first,prev_2,prev_2),
inference(forward_subsumption_resolution,[],[f133,f124]) ).
fof(f20359,plain,
( $false
| spl129_14 ),
inference(forward_subsumption_resolution,[],[f19394,f1235]) ).
fof(f20360,plain,
spl129_14,
inference(avatar_contradiction_clause,[],[f20359]) ).
fof(f20363,plain,
( ~ v__1(sortedList_first,sK2,prev_2)
| spl129_110
| ~ spl129_114 ),
inference(forward_demodulation,[],[f1837,f2122]) ).
fof(f20445,plain,
( ~ sP18(sK2)
| spl129_110
| ~ spl129_114 ),
inference(resolution,[],[f20363,f1074]) ).
fof(f20446,plain,
( ~ sP24(sK2)
| spl129_110
| ~ spl129_114 ),
inference(resolution,[],[f20363,f1026]) ).
fof(f20447,plain,
( v__1(sortedList_first,prev_2,sK2)
| ~ v__1(sortedList_first,sK2,sK2)
| ~ v__1(sortedList_first,prev_2,prev_2)
| ~ object(sK2)
| ~ object(prev_2)
| ~ object(sortedList_first)
| spl129_110
| ~ spl129_114 ),
inference(resolution,[],[f20363,f116]) ).
fof(f20456,plain,
( ~ v__1(sortedList_first,sK2,sK2)
| ~ v__1(sortedList_first,prev_2,prev_2)
| ~ object(sK2)
| ~ object(prev_2)
| ~ object(sortedList_first)
| spl129_49
| spl129_110
| ~ spl129_114 ),
inference(forward_subsumption_resolution,[],[f20447,f7359]) ).
fof(f20461,plain,
( ~ v__1(sortedList_first,prev_2,prev_2)
| ~ object(sK2)
| ~ object(prev_2)
| ~ object(sortedList_first)
| spl129_49
| spl129_110
| ~ spl129_113
| ~ spl129_114 ),
inference(forward_subsumption_resolution,[],[f20456,f2117]) ).
fof(f20466,plain,
( ~ object(sK2)
| ~ object(prev_2)
| ~ object(sortedList_first)
| ~ spl129_14
| spl129_49
| spl129_110
| ~ spl129_113
| ~ spl129_114 ),
inference(forward_subsumption_resolution,[],[f20461,f1234]) ).
fof(f20467,plain,
( ~ object(prev_2)
| ~ object(sortedList_first)
| ~ spl129_14
| spl129_49
| spl129_110
| ~ spl129_113
| ~ spl129_114 ),
inference(forward_subsumption_resolution,[],[f20466,f1105]) ).
fof(f20468,plain,
( ~ object(sortedList_first)
| ~ spl129_14
| spl129_49
| spl129_110
| ~ spl129_113
| ~ spl129_114 ),
inference(forward_subsumption_resolution,[],[f20467,f103]) ).
fof(f20469,plain,
( $false
| ~ spl129_14
| spl129_49
| spl129_110
| ~ spl129_113
| ~ spl129_114 ),
inference(forward_subsumption_resolution,[],[f20468,f108]) ).
fof(f20470,plain,
( ~ spl129_14
| spl129_49
| spl129_110
| ~ spl129_113
| ~ spl129_114 ),
inference(avatar_contradiction_clause,[],[f20469]) ).
fof(f20586,plain,
( ! [X0] :
( ~ v__1(sortedList_first,prev_2,nn)
| sP59
| v__1(null,prev_2,nn)
| sP23(X0)
| sP24(X0)
| ~ sP3(X0) )
| ~ spl129_14 ),
inference(forward_subsumption_resolution,[],[f874,f1234]) ).
fof(f20869,plain,
( ! [X0] :
( ~ v__1(sortedList_first,prev_2,nn)
| v__1(null,prev_2,nn)
| sP23(X0)
| sP24(X0)
| ~ sP3(X0) )
| ~ spl129_14
| spl129_15 ),
inference(forward_subsumption_resolution,[],[f20586,f1240]) ).
fof(f21077,plain,
( ! [X0] :
( ~ v__1(sortedList_first,prev_2,nn)
| v__1(null,prev_2,nn)
| sP24(X0)
| ~ sP3(X0) )
| ~ spl129_14
| spl129_15
| ~ spl129_19 ),
inference(forward_subsumption_resolution,[],[f20869,f1258]) ).
fof(f21431,plain,
( ~ spl129_137
| spl129_110
| ~ spl129_114 ),
inference(avatar_split_clause,[],[f20445,f2120,f1836,f2401]) ).
fof(f21519,plain,
( object(sK27)
| sP4(sK2)
| sP6(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| spl129_1
| spl129_3
| ~ spl129_37 ),
inference(forward_subsumption_resolution,[],[f18033,f1340]) ).
fof(f21547,plain,
( sP28(sK2)
| sP29(sK2)
| sP4(sK2)
| sP5(sK2)
| sP6(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| spl129_150 ),
inference(forward_subsumption_resolution,[],[f1061,f3094]) ).
fof(f21598,plain,
( object(sK27)
| sP4(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| spl129_1
| spl129_3
| ~ spl129_34
| ~ spl129_37 ),
inference(forward_subsumption_resolution,[],[f21519,f1328]) ).
fof(f21625,plain,
( sP29(sK2)
| sP4(sK2)
| sP5(sK2)
| sP6(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| spl129_150
| spl129_187 ),
inference(forward_subsumption_resolution,[],[f21547,f18465]) ).
fof(f21670,plain,
( object(sK27)
| sP4(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| spl129_1
| spl129_3
| ~ spl129_34
| ~ spl129_37
| spl129_109
| spl129_112 ),
inference(forward_subsumption_resolution,[],[f21598,f5705]) ).
fof(f21697,plain,
( sP4(sK2)
| sP5(sK2)
| sP6(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| spl129_150
| spl129_186
| spl129_187 ),
inference(forward_subsumption_resolution,[],[f21625,f18461]) ).
fof(f21738,plain,
( object(sK27)
| sP4(sK2)
| sP18(sK2)
| sP3(sK2)
| spl129_1
| spl129_3
| ~ spl129_34
| ~ spl129_37
| spl129_109
| ~ spl129_111
| spl129_112 ),
inference(forward_subsumption_resolution,[],[f21670,f1908]) ).
fof(f21765,plain,
( sP4(sK2)
| sP6(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| ~ spl129_37
| spl129_150
| spl129_186
| spl129_187 ),
inference(forward_subsumption_resolution,[],[f21697,f1340]) ).
fof(f21804,plain,
( object(sK27)
| sP4(sK2)
| sP3(sK2)
| spl129_1
| spl129_3
| ~ spl129_34
| ~ spl129_37
| spl129_109
| ~ spl129_111
| spl129_112
| spl129_137 ),
inference(forward_subsumption_resolution,[],[f21738,f2402]) ).
fof(f21831,plain,
( sP4(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| ~ spl129_34
| ~ spl129_37
| spl129_150
| spl129_186
| spl129_187 ),
inference(forward_subsumption_resolution,[],[f21765,f1328]) ).
fof(f21870,plain,
( object(sK27)
| sP4(sK2)
| spl129_1
| spl129_3
| spl129_20
| ~ spl129_34
| ~ spl129_37
| spl129_109
| ~ spl129_111
| spl129_112
| spl129_137 ),
inference(forward_subsumption_resolution,[],[f21804,f1262]) ).
fof(f21897,plain,
( sP4(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| ~ spl129_34
| ~ spl129_37
| spl129_109
| spl129_112
| spl129_150
| spl129_186
| spl129_187 ),
inference(forward_subsumption_resolution,[],[f21831,f5705]) ).
fof(f21951,plain,
( sP4(sK2)
| sP18(sK2)
| sP3(sK2)
| ~ spl129_34
| ~ spl129_37
| spl129_109
| ~ spl129_111
| spl129_112
| spl129_150
| spl129_186
| spl129_187 ),
inference(forward_subsumption_resolution,[],[f21897,f1908]) ).
fof(f21996,plain,
( sP4(sK2)
| sP3(sK2)
| ~ spl129_34
| ~ spl129_37
| spl129_109
| ~ spl129_111
| spl129_112
| spl129_137
| spl129_150
| spl129_186
| spl129_187 ),
inference(forward_subsumption_resolution,[],[f21951,f2402]) ).
fof(f22640,plain,
( ! [X0] :
( ~ v__1(X0,nn,nn)
| ~ v__1(null,X0,nn)
| ~ object(nn)
| ~ object(X0)
| ~ object(null)
| ~ object(nn) )
| spl129_16 ),
inference(resolution,[],[f1244,f112]) ).
fof(f22641,plain,
( ! [X0] :
( ~ v__1(X0,nn,nn)
| ~ v__1(null,X0,nn)
| ~ object(nn)
| ~ object(X0)
| ~ object(null) )
| spl129_16 ),
inference(duplicate_literal_removal,[],[f22640]) ).
fof(f22646,plain,
( ! [X0] :
( ~ v__1(null,X0,nn)
| ~ object(nn)
| ~ object(X0)
| ~ object(null) )
| spl129_16 ),
inference(forward_subsumption_resolution,[],[f22641,f117]) ).
fof(f22653,plain,
( ! [X0] :
( ~ v__1(null,X0,nn)
| ~ object(X0)
| ~ object(null) )
| spl129_16 ),
inference(forward_subsumption_resolution,[],[f22646,f101]) ).
fof(f22660,plain,
( ! [X0] :
( ~ v__1(null,X0,nn)
| ~ object(X0) )
| spl129_16 ),
inference(forward_subsumption_resolution,[],[f22653,f106]) ).
fof(f22809,plain,
( ~ sP18(sK2)
| spl129_113 ),
inference(forward_subsumption_resolution,[],[f5443,f103]) ).
fof(f22921,plain,
( $false
| spl129_113
| ~ spl129_137 ),
inference(forward_subsumption_resolution,[],[f22809,f2403]) ).
fof(f22922,plain,
( spl129_113
| ~ spl129_137 ),
inference(avatar_contradiction_clause,[],[f22921]) ).
fof(f23290,definition,
( spl129_204
<=> v__1(sK45,prev_2,nn) ),
introduced(definition,[new_symbols(definition,[spl129_204])],[avatar_definition]) ).
fof(f23291,plain,
( ~ v__1(sK45,prev_2,nn)
| spl129_204 ),
inference(avatar_component_clause,[],[f23290]) ).
fof(f23292,plain,
( v__1(sK45,prev_2,nn)
| ~ spl129_204 ),
inference(avatar_component_clause,[],[f23290]) ).
fof(f23550,plain,
( ! [X0] :
( v__1(null,prev_2,nn)
| sP24(X0)
| ~ sP3(X0) )
| ~ spl129_14
| spl129_15
| ~ spl129_19
| ~ spl129_49 ),
inference(forward_subsumption_resolution,[],[f21077,f1410]) ).
fof(f23551,plain,
( ! [X0] :
( sP24(X0)
| ~ sP3(X0) )
| ~ spl129_14
| spl129_15
| ~ spl129_19
| ~ spl129_49
| spl129_112 ),
inference(forward_subsumption_resolution,[],[f23550,f1961]) ).
fof(f23653,definition,
( spl129_207
<=> v__1(null,sK2,nn) ),
introduced(definition,[new_symbols(definition,[spl129_207])],[avatar_definition]) ).
fof(f23654,plain,
( v__1(null,sK2,nn)
| ~ spl129_207 ),
inference(avatar_component_clause,[],[f23653]) ).
fof(f23655,plain,
( ~ v__1(null,sK2,nn)
| spl129_207 ),
inference(avatar_component_clause,[],[f23653]) ).
fof(f24905,plain,
( $false
| spl129_109
| spl129_112
| ~ spl129_139 ),
inference(forward_subsumption_resolution,[],[f2411,f5705]) ).
fof(f24906,plain,
( spl129_109
| spl129_112
| ~ spl129_139 ),
inference(avatar_contradiction_clause,[],[f24905]) ).
fof(f24909,plain,
( v__1(null,sK2,nn)
| sP8(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| spl129_150 ),
inference(forward_subsumption_resolution,[],[f2986,f3094]) ).
fof(f24927,plain,
( v__1(null,sK2,nn)
| sP8(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| spl129_109
| spl129_112
| spl129_150 ),
inference(forward_subsumption_resolution,[],[f24909,f5705]) ).
fof(f24945,plain,
( v__1(null,sK2,nn)
| sP8(sK2)
| sP18(sK2)
| sP3(sK2)
| spl129_109
| ~ spl129_111
| spl129_112
| spl129_150 ),
inference(forward_subsumption_resolution,[],[f24927,f1908]) ).
fof(f24960,plain,
( v__1(null,sK2,nn)
| sP8(sK2)
| sP3(sK2)
| spl129_109
| ~ spl129_111
| spl129_112
| spl129_137
| spl129_150 ),
inference(forward_subsumption_resolution,[],[f24945,f2402]) ).
fof(f24975,plain,
( v__1(null,sK2,nn)
| sP8(sK2)
| spl129_20
| spl129_109
| ~ spl129_111
| spl129_112
| spl129_137
| spl129_150 ),
inference(forward_subsumption_resolution,[],[f24960,f1262]) ).
fof(f25046,plain,
( v__1(null,sK2,nn)
| spl129_20
| spl129_109
| ~ spl129_111
| spl129_112
| spl129_137
| spl129_140
| spl129_150 ),
inference(forward_subsumption_resolution,[],[f24975,f2414]) ).
fof(f25047,plain,
( spl129_207
| spl129_20
| spl129_109
| ~ spl129_111
| spl129_112
| spl129_137
| spl129_140
| spl129_150 ),
inference(avatar_split_clause,[],[f25046,f3092,f2413,f2401,f1960,f1907,f1822,f1261,f23653]) ).
fof(f25058,plain,
( ~ object(sK2)
| spl129_16
| ~ spl129_207 ),
inference(resolution,[],[f23654,f22660]) ).
fof(f25092,plain,
( $false
| spl129_16
| ~ spl129_207 ),
inference(forward_subsumption_resolution,[],[f25058,f1105]) ).
fof(f25093,plain,
( spl129_16
| ~ spl129_207 ),
inference(avatar_contradiction_clause,[],[f25092]) ).
fof(f25113,plain,
( node_next(nn) = sK49(sK2)
| ~ spl129_131
| ~ spl129_140 ),
inference(resolution,[],[f2415,f2245]) ).
fof(f25120,plain,
( v__1(null,sK2,sK2)
| ~ sP28(sK2)
| spl129_207 ),
inference(resolution,[],[f23655,f640]) ).
fof(f25121,plain,
( v__1(null,sK2,sK2)
| sP25(sK2)
| ~ sP3(sK2)
| spl129_207 ),
inference(resolution,[],[f23655,f847]) ).
fof(f25125,plain,
( v__1(null,sK2,sK2)
| ~ sP7(sK2)
| spl129_207 ),
inference(resolution,[],[f23655,f965]) ).
fof(f25134,plain,
( ~ sP7(sK2)
| spl129_150
| spl129_207 ),
inference(forward_subsumption_resolution,[],[f25125,f3094]) ).
fof(f25138,plain,
( $false
| ~ spl129_141
| spl129_150
| spl129_207 ),
inference(forward_subsumption_resolution,[],[f25134,f2419]) ).
fof(f25139,plain,
( ~ spl129_141
| spl129_150
| spl129_207 ),
inference(avatar_contradiction_clause,[],[f25138]) ).
fof(f25267,definition,
( spl129_216
<=> object(sK75) ),
introduced(definition,[new_symbols(definition,[spl129_216])],[avatar_definition]) ).
fof(f25268,plain,
( ~ object(sK75)
| spl129_216 ),
inference(avatar_component_clause,[],[f25267]) ).
fof(f25269,plain,
( object(sK75)
| ~ spl129_216 ),
inference(avatar_component_clause,[],[f25267]) ).
fof(f25513,plain,
( object(sK27)
| spl129_1
| spl129_3
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| spl129_109
| ~ spl129_111
| spl129_112
| spl129_137 ),
inference(forward_subsumption_resolution,[],[f21870,f1352]) ).
fof(f25517,plain,
( sP3(sK2)
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| spl129_109
| ~ spl129_111
| spl129_112
| spl129_137
| spl129_150
| spl129_186
| spl129_187 ),
inference(forward_subsumption_resolution,[],[f21996,f1352]) ).
fof(f25520,plain,
( $false
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| spl129_109
| ~ spl129_111
| spl129_112
| spl129_137
| spl129_150
| spl129_186
| spl129_187 ),
inference(forward_subsumption_resolution,[],[f25517,f1262]) ).
fof(f25521,plain,
( spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| spl129_109
| ~ spl129_111
| spl129_112
| spl129_137
| spl129_150
| spl129_186
| spl129_187 ),
inference(avatar_contradiction_clause,[],[f25520]) ).
fof(f25550,plain,
( ~ sP28(sK2)
| spl129_150
| spl129_207 ),
inference(forward_subsumption_resolution,[],[f25120,f3094]) ).
fof(f25820,plain,
( $false
| spl129_150
| ~ spl129_187
| spl129_207 ),
inference(forward_subsumption_resolution,[],[f25550,f18466]) ).
fof(f25821,plain,
( spl129_150
| ~ spl129_187
| spl129_207 ),
inference(avatar_contradiction_clause,[],[f25820]) ).
fof(f26011,plain,
( sP67(sK42)
| object(sK27)
| sP5(sK2)
| sP6(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| ~ spl129_40 ),
inference(forward_subsumption_resolution,[],[f1006,f1352]) ).
fof(f26065,plain,
( sP67(sK42)
| object(sK27)
| sP5(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| ~ spl129_34
| ~ spl129_40 ),
inference(forward_subsumption_resolution,[],[f26011,f1328]) ).
fof(f26118,plain,
( sP67(sK42)
| object(sK27)
| sP5(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| ~ spl129_34
| ~ spl129_40
| spl129_109
| spl129_112 ),
inference(forward_subsumption_resolution,[],[f26065,f5705]) ).
fof(f26162,plain,
( sP67(sK42)
| object(sK27)
| sP5(sK2)
| sP18(sK2)
| sP3(sK2)
| ~ spl129_34
| ~ spl129_40
| spl129_109
| ~ spl129_111
| spl129_112 ),
inference(forward_subsumption_resolution,[],[f26118,f1908]) ).
fof(f26206,plain,
( sP67(sK42)
| object(sK27)
| sP5(sK2)
| sP3(sK2)
| ~ spl129_34
| ~ spl129_40
| spl129_109
| ~ spl129_111
| spl129_112
| spl129_137 ),
inference(forward_subsumption_resolution,[],[f26162,f2402]) ).
fof(f26364,plain,
v__1(sortedList_first,nn,nn),
inference(forward_subsumption_resolution,[],[f134,f130]) ).
fof(f26368,plain,
! [X0] :
( node_key(X0) != sK0
| null = X0
| ~ v__1(node_next(nn),X0,X0)
| ~ v__1(sortedList_first,nn,nn)
| ~ object(X0) ),
inference(forward_subsumption_resolution,[],[f5145,f101]) ).
fof(f26429,plain,
( sP25(sK2)
| ~ sP3(sK2)
| spl129_150
| spl129_207 ),
inference(forward_subsumption_resolution,[],[f25121,f3094]) ).
fof(f26486,plain,
( ~ sP3(sK2)
| spl129_113
| spl129_150
| spl129_207 ),
inference(forward_subsumption_resolution,[],[f26429,f2124]) ).
fof(f26598,plain,
( $false
| ~ spl129_20
| spl129_113
| spl129_150
| spl129_207 ),
inference(forward_subsumption_resolution,[],[f26486,f1263]) ).
fof(f26599,plain,
( ~ spl129_20
| spl129_113
| spl129_150
| spl129_207 ),
inference(avatar_contradiction_clause,[],[f26598]) ).
fof(f26965,plain,
( ~ sP3(sK2)
| ~ spl129_14
| spl129_15
| ~ spl129_19
| ~ spl129_49
| spl129_110
| spl129_112
| ~ spl129_114 ),
inference(resolution,[],[f20446,f23551]) ).
fof(f26966,plain,
( $false
| ~ spl129_14
| spl129_15
| ~ spl129_19
| ~ spl129_20
| ~ spl129_49
| spl129_110
| spl129_112
| ~ spl129_114 ),
inference(forward_subsumption_resolution,[],[f26965,f1263]) ).
fof(f26967,plain,
( ~ spl129_14
| spl129_15
| ~ spl129_19
| ~ spl129_20
| ~ spl129_49
| spl129_110
| spl129_112
| ~ spl129_114 ),
inference(avatar_contradiction_clause,[],[f26966]) ).
fof(f28175,plain,
( sP67(sK42)
| object(sK27)
| sP3(sK2)
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| spl129_109
| ~ spl129_111
| spl129_112
| spl129_137 ),
inference(forward_subsumption_resolution,[],[f26206,f1340]) ).
fof(f28192,plain,
( sP67(sK42)
| object(sK27)
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| spl129_109
| ~ spl129_111
| spl129_112
| spl129_137 ),
inference(forward_subsumption_resolution,[],[f28175,f1262]) ).
fof(f28255,definition,
( spl129_222
<=> object(sK27) ),
introduced(definition,[new_symbols(definition,[spl129_222])],[avatar_definition]) ).
fof(f28257,plain,
( object(sK27)
| ~ spl129_222 ),
inference(avatar_component_clause,[],[f28255]) ).
fof(f28259,definition,
( spl129_223
<=> sP67(sK42) ),
introduced(definition,[new_symbols(definition,[spl129_223])],[avatar_definition]) ).
fof(f28260,plain,
( ~ sP67(sK42)
| spl129_223 ),
inference(avatar_component_clause,[],[f28259]) ).
fof(f28261,plain,
( sP67(sK42)
| ~ spl129_223 ),
inference(avatar_component_clause,[],[f28259]) ).
fof(f28262,plain,
( spl129_222
| spl129_223
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| spl129_109
| ~ spl129_111
| spl129_112
| spl129_137 ),
inference(avatar_split_clause,[],[f28192,f2401,f1960,f1907,f1822,f1351,f1339,f1327,f1261,f28259,f28255]) ).
fof(f28263,plain,
( node_next(nn) = sK42
| ~ spl129_223 ),
inference(resolution,[],[f28261,f666]) ).
fof(f28264,plain,
( object(sK42)
| ~ spl129_223 ),
inference(resolution,[],[f28261,f667]) ).
fof(f32715,plain,
( v__1(sK81,sK2,sK2)
| ~ spl129_114
| ~ spl129_129 ),
inference(forward_demodulation,[],[f2224,f2122]) ).
fof(f32802,plain,
( ~ v__1(sK81,sK2,sK2)
| ~ spl129_114
| spl129_129 ),
inference(forward_demodulation,[],[f2225,f2122]) ).
fof(f33641,plain,
( $false
| ~ spl129_111
| ~ spl129_138 ),
inference(forward_subsumption_resolution,[],[f2407,f1908]) ).
fof(f33642,plain,
( ~ spl129_111
| ~ spl129_138 ),
inference(avatar_contradiction_clause,[],[f33641]) ).
fof(f36038,plain,
( ! [X0] :
( v__1(null,prev_2,prev_2)
| ~ sP4(X0) )
| spl129_112 ),
inference(forward_subsumption_resolution,[],[f999,f1961]) ).
fof(f36386,plain,
( node_next(nn) = sK34(sK2)
| ~ spl129_140 ),
inference(resolution,[],[f2415,f958]) ).
fof(f36777,plain,
( spl129_40
| spl129_109
| spl129_112 ),
inference(avatar_split_clause,[],[f36038,f1960,f1822,f1351]) ).
fof(f36955,definition,
( spl129_244
<=> v__1(sK45,nn,nn) ),
introduced(definition,[new_symbols(definition,[spl129_244])],[avatar_definition]) ).
fof(f36956,plain,
( ~ v__1(sK45,nn,nn)
| spl129_244 ),
inference(avatar_component_clause,[],[f36955]) ).
fof(f36957,plain,
( v__1(sK45,nn,nn)
| ~ spl129_244 ),
inference(avatar_component_clause,[],[f36955]) ).
fof(f37681,plain,
( ! [X0] :
( v__1(null,prev_2,prev_2)
| ~ sP5(X0) )
| spl129_112 ),
inference(forward_subsumption_resolution,[],[f997,f1961]) ).
fof(f37979,plain,
( spl129_37
| spl129_109
| spl129_112 ),
inference(avatar_split_clause,[],[f37681,f1960,f1822,f1339]) ).
fof(f38372,plain,
( prev_2 = null
| ~ object(prev_2)
| ~ spl129_109 ),
inference(resolution,[],[f1824,f4152]) ).
fof(f38418,plain,
( ~ object(prev_2)
| ~ spl129_109 ),
inference(forward_subsumption_resolution,[],[f38372,f124]) ).
fof(f38422,plain,
( $false
| ~ spl129_109 ),
inference(forward_subsumption_resolution,[],[f38418,f103]) ).
fof(f38423,plain,
~ spl129_109,
inference(avatar_contradiction_clause,[],[f38422]) ).
fof(f44782,plain,
( ! [X0] :
( ~ v__1(X0,sK2,sK2)
| ~ v__1(sortedList_first,X0,X0)
| ~ object(sK2)
| ~ object(X0)
| ~ object(sortedList_first) )
| spl129_113 ),
inference(resolution,[],[f2118,f111]) ).
fof(f44801,plain,
( ! [X0] :
( ~ v__1(X0,sK2,sK2)
| ~ v__1(sortedList_first,X0,X0)
| ~ object(X0)
| ~ object(sortedList_first) )
| spl129_113 ),
inference(forward_subsumption_resolution,[],[f44782,f1105]) ).
fof(f44808,plain,
( ! [X0] :
( ~ v__1(X0,sK2,sK2)
| ~ v__1(sortedList_first,X0,X0)
| ~ object(X0) )
| spl129_113 ),
inference(forward_subsumption_resolution,[],[f44801,f108]) ).
fof(f44870,plain,
( ! [X0] :
( ~ v__1(X0,nn,nn)
| ~ v__1(sK45,X0,nn)
| ~ object(nn)
| ~ object(X0)
| ~ object(sK45)
| ~ object(nn) )
| spl129_244 ),
inference(resolution,[],[f36956,f112]) ).
fof(f44871,plain,
( ! [X0] :
( ~ v__1(X0,nn,nn)
| ~ v__1(sK45,X0,nn)
| ~ object(nn)
| ~ object(X0)
| ~ object(sK45) )
| spl129_244 ),
inference(duplicate_literal_removal,[],[f44870]) ).
fof(f44876,plain,
( ! [X0] :
( ~ v__1(sK45,X0,nn)
| ~ object(nn)
| ~ object(X0)
| ~ object(sK45) )
| spl129_244 ),
inference(forward_subsumption_resolution,[],[f44871,f117]) ).
fof(f44883,plain,
( ! [X0] :
( ~ v__1(sK45,X0,nn)
| ~ object(X0)
| ~ object(sK45) )
| spl129_244 ),
inference(forward_subsumption_resolution,[],[f44876,f101]) ).
fof(f44890,plain,
( ! [X0] :
( ~ v__1(sK45,X0,nn)
| ~ object(X0) )
| ~ spl129_35
| spl129_244 ),
inference(forward_subsumption_resolution,[],[f44883,f1332]) ).
fof(f45616,plain,
( $false
| spl129_106 ),
inference(forward_subsumption_resolution,[],[f26364,f1775]) ).
fof(f45617,plain,
spl129_106,
inference(avatar_contradiction_clause,[],[f45616]) ).
fof(f47165,plain,
( ~ object(prev_2)
| ~ spl129_35
| ~ spl129_204
| spl129_244 ),
inference(resolution,[],[f23292,f44890]) ).
fof(f47202,plain,
( $false
| ~ spl129_35
| ~ spl129_204
| spl129_244 ),
inference(forward_subsumption_resolution,[],[f47165,f103]) ).
fof(f47203,plain,
( ~ spl129_35
| ~ spl129_204
| spl129_244 ),
inference(avatar_contradiction_clause,[],[f47202]) ).
fof(f47539,plain,
( node_next(nn) = sK70(sK2)
| ~ spl129_186 ),
inference(resolution,[],[f18462,f633]) ).
fof(f47541,plain,
( spl129_222
| spl129_1
| spl129_3
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| spl129_109
| ~ spl129_111
| spl129_112
| spl129_137 ),
inference(avatar_split_clause,[],[f25513,f2401,f1960,f1907,f1822,f1351,f1339,f1327,f1261,f1184,f1175,f28255]) ).
fof(f47547,plain,
( sP66
| node_next(nn) = sK27
| sP5(sK2)
| sP6(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| spl129_3
| ~ spl129_40 ),
inference(forward_subsumption_resolution,[],[f17935,f1352]) ).
fof(f47556,plain,
( sP66
| node_next(nn) = sK27
| sP6(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| spl129_3
| ~ spl129_37
| ~ spl129_40 ),
inference(forward_subsumption_resolution,[],[f47547,f1340]) ).
fof(f51656,plain,
( ! [X0] :
( node_key(X0) != sK0
| null = X0
| ~ v__1(node_next(nn),X0,X0)
| ~ object(X0) )
| ~ spl129_106 ),
inference(forward_subsumption_resolution,[],[f26368,f1774]) ).
fof(f51802,plain,
( sK81 = sK114
| ~ spl129_124
| ~ spl129_130 ),
inference(superposition,[],[f2234,f2195]) ).
fof(f51815,plain,
( v__1(sortedList_first,sK81,sK81)
| null = sK81
| nn = null
| ~ object(nn)
| ~ spl129_130 ),
inference(superposition,[],[f4253,f2234]) ).
fof(f51821,plain,
( ~ v__1(sK81,nn,nn)
| nn = null
| ~ v__1(sortedList_first,nn,nn)
| ~ object(nn)
| ~ spl129_130 ),
inference(superposition,[],[f5141,f2234]) ).
fof(f51829,plain,
( v__1(sortedList_first,sK81,sK81)
| null = sK81
| ~ object(nn)
| ~ spl129_130 ),
inference(forward_subsumption_resolution,[],[f51815,f130]) ).
fof(f51840,plain,
( v__1(sortedList_first,sK81,sK81)
| null = sK81
| ~ spl129_130 ),
inference(forward_subsumption_resolution,[],[f51829,f101]) ).
fof(f52047,plain,
( sK42 = sK81
| ~ spl129_130
| ~ spl129_223 ),
inference(superposition,[],[f28263,f2234]) ).
fof(f52048,plain,
( sK42 = sK114
| ~ spl129_124
| ~ spl129_223 ),
inference(superposition,[],[f28263,f2195]) ).
fof(f52069,plain,
( ~ v__1(sK42,nn,nn)
| nn = null
| ~ v__1(sortedList_first,nn,nn)
| ~ object(nn)
| ~ spl129_223 ),
inference(superposition,[],[f5141,f28263]) ).
fof(f52072,plain,
( ~ v__1(sK42,nn,nn)
| ~ v__1(sortedList_first,nn,nn)
| ~ object(nn)
| ~ spl129_223 ),
inference(forward_subsumption_resolution,[],[f52069,f130]) ).
fof(f52085,plain,
( ~ v__1(sK42,nn,nn)
| ~ object(nn)
| ~ spl129_106
| ~ spl129_223 ),
inference(forward_subsumption_resolution,[],[f52072,f1774]) ).
fof(f52093,plain,
( ~ v__1(sK42,nn,nn)
| ~ spl129_106
| ~ spl129_223 ),
inference(forward_subsumption_resolution,[],[f52085,f101]) ).
fof(f52193,plain,
( sK114 = sK34(sK2)
| ~ spl129_124
| ~ spl129_140 ),
inference(forward_demodulation,[],[f36386,f2195]) ).
fof(f52194,plain,
( sK81 = sK34(sK2)
| ~ spl129_124
| ~ spl129_130
| ~ spl129_140 ),
inference(forward_demodulation,[],[f52193,f51802]) ).
fof(f52198,plain,
( v__1(sK81,sK2,sK2)
| ~ sP8(sK2)
| ~ spl129_124
| ~ spl129_130
| ~ spl129_140 ),
inference(superposition,[],[f959,f52194]) ).
fof(f52200,plain,
( v__1(sK81,sK2,sK2)
| ~ spl129_124
| ~ spl129_130
| ~ spl129_140 ),
inference(forward_subsumption_resolution,[],[f52198,f2415]) ).
fof(f52204,plain,
( sK114 = sK70(sK2)
| ~ spl129_124
| ~ spl129_186 ),
inference(forward_demodulation,[],[f47539,f2195]) ).
fof(f52205,plain,
( sK81 = sK70(sK2)
| ~ spl129_124
| ~ spl129_130
| ~ spl129_186 ),
inference(forward_demodulation,[],[f52204,f51802]) ).
fof(f52209,plain,
( v__1(sK81,sK2,sK2)
| ~ sP29(sK2)
| ~ spl129_124
| ~ spl129_130
| ~ spl129_186 ),
inference(superposition,[],[f634,f52205]) ).
fof(f52211,plain,
( v__1(sK81,sK2,sK2)
| ~ spl129_124
| ~ spl129_130
| ~ spl129_186 ),
inference(forward_subsumption_resolution,[],[f52209,f18462]) ).
fof(f52406,definition,
( spl129_277
<=> null = sK81 ),
introduced(definition,[new_symbols(definition,[spl129_277])],[avatar_definition]) ).
fof(f52408,plain,
( null = sK81
| ~ spl129_277 ),
inference(avatar_component_clause,[],[f52406]) ).
fof(f52410,definition,
( spl129_278
<=> v__1(sortedList_first,sK81,sK81) ),
introduced(definition,[new_symbols(definition,[spl129_278])],[avatar_definition]) ).
fof(f52412,plain,
( v__1(sortedList_first,sK81,sK81)
| ~ spl129_278 ),
inference(avatar_component_clause,[],[f52410]) ).
fof(f52413,plain,
( spl129_277
| spl129_278
| ~ spl129_130 ),
inference(avatar_split_clause,[],[f51840,f2232,f52410,f52406]) ).
fof(f52550,definition,
( spl129_280
<=> sK81 = sK100(sK2) ),
introduced(definition,[new_symbols(definition,[spl129_280])],[avatar_definition]) ).
fof(f52551,plain,
( sK81 != sK100(sK2)
| spl129_280 ),
inference(avatar_component_clause,[],[f52550]) ).
fof(f52552,plain,
( sK81 = sK100(sK2)
| ~ spl129_280 ),
inference(avatar_component_clause,[],[f52550]) ).
fof(f52555,plain,
( v__1(sK81,sK2,nn)
| ~ sP29(sK2)
| ~ spl129_101
| ~ spl129_280 ),
inference(superposition,[],[f1755,f52552]) ).
fof(f52557,plain,
( v__1(sK81,sK2,nn)
| ~ spl129_101
| ~ spl129_186
| ~ spl129_280 ),
inference(forward_subsumption_resolution,[],[f52555,f18462]) ).
fof(f53015,definition,
( spl129_283
<=> sK42 = sK49(sK2) ),
introduced(definition,[new_symbols(definition,[spl129_283])],[avatar_definition]) ).
fof(f53016,plain,
( sK42 != sK49(sK2)
| spl129_283 ),
inference(avatar_component_clause,[],[f53015]) ).
fof(f53017,plain,
( sK42 = sK49(sK2)
| ~ spl129_283 ),
inference(avatar_component_clause,[],[f53015]) ).
fof(f53379,plain,
( sP67(sK42)
| node_next(nn) = sK27
| sP5(sK2)
| sP6(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| ~ spl129_40 ),
inference(forward_subsumption_resolution,[],[f1005,f1352]) ).
fof(f53390,plain,
( sP67(sK42)
| node_next(nn) = sK27
| sP6(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| ~ spl129_37
| ~ spl129_40 ),
inference(forward_subsumption_resolution,[],[f53379,f1340]) ).
fof(f53643,definition,
( spl129_286
<=> sK27 = sK49(sK2) ),
introduced(definition,[new_symbols(definition,[spl129_286])],[avatar_definition]) ).
fof(f53644,plain,
( sK27 != sK49(sK2)
| spl129_286 ),
inference(avatar_component_clause,[],[f53643]) ).
fof(f53645,plain,
( sK27 = sK49(sK2)
| ~ spl129_286 ),
inference(avatar_component_clause,[],[f53643]) ).
fof(f53647,definition,
( spl129_287
<=> sK27 = sK42 ),
introduced(definition,[new_symbols(definition,[spl129_287])],[avatar_definition]) ).
fof(f53648,plain,
( sK27 != sK42
| spl129_287 ),
inference(avatar_component_clause,[],[f53647]) ).
fof(f53649,plain,
( sK27 = sK42
| ~ spl129_287 ),
inference(avatar_component_clause,[],[f53647]) ).
fof(f53653,plain,
( v__1(sK27,sK2,nn)
| ~ sP8(sK2)
| ~ spl129_103
| ~ spl129_286 ),
inference(superposition,[],[f1763,f53645]) ).
fof(f53655,plain,
( v__1(sK27,sK2,nn)
| ~ spl129_103
| ~ spl129_140
| ~ spl129_286 ),
inference(forward_subsumption_resolution,[],[f53653,f2415]) ).
fof(f54179,plain,
( v__1(null,sK2,sK2)
| ~ spl129_124
| ~ spl129_130
| ~ spl129_140
| ~ spl129_277 ),
inference(forward_demodulation,[],[f52200,f52408]) ).
fof(f54181,plain,
( v__1(null,sK2,sK2)
| ~ spl129_124
| ~ spl129_130
| ~ spl129_186
| ~ spl129_277 ),
inference(forward_demodulation,[],[f52211,f52408]) ).
fof(f54183,plain,
( v__1(null,sK2,nn)
| ~ spl129_101
| ~ spl129_186
| ~ spl129_277
| ~ spl129_280 ),
inference(forward_demodulation,[],[f52557,f52408]) ).
fof(f54193,plain,
( $false
| ~ spl129_124
| ~ spl129_130
| ~ spl129_140
| spl129_150
| ~ spl129_277 ),
inference(forward_subsumption_resolution,[],[f54179,f3094]) ).
fof(f54194,plain,
( ~ spl129_124
| ~ spl129_130
| ~ spl129_140
| spl129_150
| ~ spl129_277 ),
inference(avatar_contradiction_clause,[],[f54193]) ).
fof(f54196,plain,
( $false
| ~ spl129_124
| ~ spl129_130
| spl129_150
| ~ spl129_186
| ~ spl129_277 ),
inference(forward_subsumption_resolution,[],[f54181,f3094]) ).
fof(f54197,plain,
( ~ spl129_124
| ~ spl129_130
| spl129_150
| ~ spl129_186
| ~ spl129_277 ),
inference(avatar_contradiction_clause,[],[f54196]) ).
fof(f54199,plain,
( $false
| ~ spl129_101
| ~ spl129_186
| spl129_207
| ~ spl129_277
| ~ spl129_280 ),
inference(forward_subsumption_resolution,[],[f54183,f23655]) ).
fof(f54200,plain,
( ~ spl129_101
| ~ spl129_186
| spl129_207
| ~ spl129_277
| ~ spl129_280 ),
inference(avatar_contradiction_clause,[],[f54199]) ).
fof(f54206,plain,
( sK81 = sK100(sK2)
| ~ spl129_123
| ~ spl129_130
| ~ spl129_186 ),
inference(forward_demodulation,[],[f18468,f2234]) ).
fof(f54209,plain,
( null != sK100(sK2)
| ~ spl129_277
| spl129_280 ),
inference(forward_demodulation,[],[f52551,f52408]) ).
fof(f54215,plain,
( sK81 = sK34(sK2)
| ~ spl129_130
| ~ spl129_140 ),
inference(forward_demodulation,[],[f36386,f2234]) ).
fof(f54234,plain,
( null = sK100(sK2)
| ~ spl129_123
| ~ spl129_130
| ~ spl129_186
| ~ spl129_277 ),
inference(forward_demodulation,[],[f54206,f52408]) ).
fof(f54367,plain,
( $false
| ~ spl129_123
| ~ spl129_130
| ~ spl129_186
| ~ spl129_277
| spl129_280 ),
inference(forward_subsumption_resolution,[],[f54234,f54209]) ).
fof(f54368,plain,
( ~ spl129_123
| ~ spl129_130
| ~ spl129_186
| ~ spl129_277
| spl129_280 ),
inference(avatar_contradiction_clause,[],[f54367]) ).
fof(f54637,plain,
( v__1(sK81,sK2,sK2)
| ~ sP8(sK2)
| ~ spl129_130
| ~ spl129_140 ),
inference(superposition,[],[f959,f54215]) ).
fof(f54639,plain,
( v__1(sK81,sK2,sK2)
| ~ spl129_130
| ~ spl129_140 ),
inference(forward_subsumption_resolution,[],[f54637,f2415]) ).
fof(f54824,definition,
( spl129_289
<=> sK42 = sK81 ),
introduced(definition,[new_symbols(definition,[spl129_289])],[avatar_definition]) ).
fof(f54825,plain,
( sK42 != sK81
| spl129_289 ),
inference(avatar_component_clause,[],[f54824]) ).
fof(f54826,plain,
( sK42 = sK81
| ~ spl129_289 ),
inference(avatar_component_clause,[],[f54824]) ).
fof(f54828,definition,
( spl129_290
<=> sK27 = sK81 ),
introduced(definition,[new_symbols(definition,[spl129_290])],[avatar_definition]) ).
fof(f54830,plain,
( sK27 = sK81
| ~ spl129_290 ),
inference(avatar_component_clause,[],[f54828]) ).
fof(f54864,plain,
( v__1(sortedList_first,sK42,sK42)
| ~ spl129_278
| ~ spl129_289 ),
inference(superposition,[],[f52412,f54826]) ).
fof(f55291,plain,
( v__1(sK42,sK2,sK2)
| ~ spl129_130
| ~ spl129_140
| ~ spl129_289 ),
inference(forward_demodulation,[],[f54639,f54826]) ).
fof(f55390,plain,
( ~ v__1(sortedList_first,sK42,sK42)
| ~ object(sK42)
| spl129_113
| ~ spl129_130
| ~ spl129_140
| ~ spl129_289 ),
inference(resolution,[],[f55291,f44808]) ).
fof(f55434,plain,
( ~ object(sK42)
| spl129_113
| ~ spl129_130
| ~ spl129_140
| ~ spl129_278
| ~ spl129_289 ),
inference(forward_subsumption_resolution,[],[f55390,f54864]) ).
fof(f55438,plain,
( $false
| spl129_113
| ~ spl129_130
| ~ spl129_140
| ~ spl129_223
| ~ spl129_278
| ~ spl129_289 ),
inference(forward_subsumption_resolution,[],[f55434,f28264]) ).
fof(f55439,plain,
( spl129_113
| ~ spl129_130
| ~ spl129_140
| ~ spl129_223
| ~ spl129_278
| ~ spl129_289 ),
inference(avatar_contradiction_clause,[],[f55438]) ).
fof(f55528,plain,
( $false
| ~ spl129_130
| ~ spl129_223
| spl129_289 ),
inference(forward_subsumption_resolution,[],[f52047,f54825]) ).
fof(f55529,plain,
( ~ spl129_130
| ~ spl129_223
| spl129_289 ),
inference(avatar_contradiction_clause,[],[f55528]) ).
fof(f55598,plain,
( v__1(sortedList_first,sK27,sK27)
| ~ spl129_278
| ~ spl129_290 ),
inference(superposition,[],[f52412,f54830]) ).
fof(f55889,plain,
( v__1(sK27,sK2,sK2)
| ~ spl129_130
| ~ spl129_140
| ~ spl129_290 ),
inference(forward_demodulation,[],[f54639,f54830]) ).
fof(f56116,plain,
( ~ v__1(sortedList_first,sK27,sK27)
| ~ object(sK27)
| spl129_113
| ~ spl129_130
| ~ spl129_140
| ~ spl129_290 ),
inference(resolution,[],[f55889,f44808]) ).
fof(f56160,plain,
( ~ object(sK27)
| spl129_113
| ~ spl129_130
| ~ spl129_140
| ~ spl129_278
| ~ spl129_290 ),
inference(forward_subsumption_resolution,[],[f56116,f55598]) ).
fof(f56164,plain,
( $false
| spl129_113
| ~ spl129_130
| ~ spl129_140
| ~ spl129_222
| ~ spl129_278
| ~ spl129_290 ),
inference(forward_subsumption_resolution,[],[f56160,f28257]) ).
fof(f56165,plain,
( spl129_113
| ~ spl129_130
| ~ spl129_140
| ~ spl129_222
| ~ spl129_278
| ~ spl129_290 ),
inference(avatar_contradiction_clause,[],[f56164]) ).
fof(f56170,plain,
( ! [X0] :
( v__1(sK76,prev_2,prev_2)
| ~ sP6(X0) )
| spl129_204 ),
inference(forward_subsumption_resolution,[],[f583,f23291]) ).
fof(f56171,plain,
( ! [X0] :
( ~ v__1(sK75,nn,nn)
| ~ sP6(X0) )
| spl129_204 ),
inference(forward_subsumption_resolution,[],[f591,f23291]) ).
fof(f56181,plain,
( node_next(nn) = sK27
| sP6(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| ~ spl129_37
| ~ spl129_40
| spl129_223 ),
inference(forward_subsumption_resolution,[],[f53390,f28260]) ).
fof(f56282,definition,
( spl129_292
<=> sK75 = sK76 ),
introduced(definition,[new_symbols(definition,[spl129_292])],[avatar_definition]) ).
fof(f56283,plain,
( sK75 != sK76
| spl129_292 ),
inference(avatar_component_clause,[],[f56282]) ).
fof(f56284,plain,
( sK75 = sK76
| ~ spl129_292 ),
inference(avatar_component_clause,[],[f56282]) ).
fof(f56319,plain,
( ! [X0] :
( v__1(sK75,prev_2,prev_2)
| ~ sP6(X0) )
| spl129_204
| ~ spl129_292 ),
inference(forward_demodulation,[],[f56170,f56284]) ).
fof(f56322,definition,
( spl129_295
<=> v__1(sK75,nn,nn) ),
introduced(definition,[new_symbols(definition,[spl129_295])],[avatar_definition]) ).
fof(f56323,plain,
( v__1(sK75,nn,nn)
| ~ spl129_295 ),
inference(avatar_component_clause,[],[f56322]) ).
fof(f56324,plain,
( ~ v__1(sK75,nn,nn)
| spl129_295 ),
inference(avatar_component_clause,[],[f56322]) ).
fof(f56325,plain,
( spl129_34
| ~ spl129_295
| spl129_204 ),
inference(avatar_split_clause,[],[f56171,f23290,f56322,f1327]) ).
fof(f56331,plain,
( ! [X0] :
( ~ v__1(X0,nn,nn)
| ~ v__1(sK75,X0,X0)
| ~ object(nn)
| ~ object(X0)
| ~ object(sK75) )
| spl129_295 ),
inference(resolution,[],[f56324,f111]) ).
fof(f56350,plain,
( ! [X0] :
( ~ v__1(X0,nn,nn)
| ~ v__1(sK75,X0,X0)
| ~ object(X0)
| ~ object(sK75) )
| spl129_295 ),
inference(forward_subsumption_resolution,[],[f56331,f101]) ).
fof(f56357,plain,
( ! [X0] :
( ~ v__1(X0,nn,nn)
| ~ v__1(sK75,X0,X0)
| ~ object(X0) )
| ~ spl129_216
| spl129_295 ),
inference(forward_subsumption_resolution,[],[f56350,f25269]) ).
fof(f56364,definition,
( spl129_296
<=> v__1(sK75,prev_2,prev_2) ),
introduced(definition,[new_symbols(definition,[spl129_296])],[avatar_definition]) ).
fof(f56365,plain,
( ~ v__1(sK75,prev_2,prev_2)
| spl129_296 ),
inference(avatar_component_clause,[],[f56364]) ).
fof(f56366,plain,
( v__1(sK75,prev_2,prev_2)
| ~ spl129_296 ),
inference(avatar_component_clause,[],[f56364]) ).
fof(f56367,plain,
( spl129_34
| spl129_296
| spl129_204
| ~ spl129_292 ),
inference(avatar_split_clause,[],[f56319,f56282,f23290,f56364,f1327]) ).
fof(f56600,plain,
( ~ v__1(prev_2,nn,nn)
| ~ object(prev_2)
| ~ spl129_216
| spl129_295
| ~ spl129_296 ),
inference(resolution,[],[f56357,f56366]) ).
fof(f56644,plain,
( ~ object(prev_2)
| ~ spl129_216
| spl129_295
| ~ spl129_296 ),
inference(forward_subsumption_resolution,[],[f56600,f3958]) ).
fof(f56658,plain,
( $false
| ~ spl129_216
| spl129_295
| ~ spl129_296 ),
inference(forward_subsumption_resolution,[],[f56644,f103]) ).
fof(f56659,plain,
( ~ spl129_216
| spl129_295
| ~ spl129_296 ),
inference(avatar_contradiction_clause,[],[f56658]) ).
fof(f56661,plain,
( ! [X0] :
( object(sK75)
| ~ sP6(X0) )
| spl129_204 ),
inference(forward_subsumption_resolution,[],[f593,f23291]) ).
fof(f56676,plain,
( ! [X0] : ~ sP6(X0)
| spl129_204
| spl129_216 ),
inference(forward_subsumption_resolution,[],[f56661,f25268]) ).
fof(f56677,plain,
( spl129_34
| spl129_204
| spl129_216 ),
inference(avatar_split_clause,[],[f56676,f25267,f23290,f1327]) ).
fof(f56894,plain,
( ! [X0] :
( ~ v__1(sK75,nn,nn)
| ~ sP6(X0) )
| spl129_35 ),
inference(forward_subsumption_resolution,[],[f588,f1331]) ).
fof(f57061,plain,
( ! [X0] : ~ sP6(X0)
| spl129_35
| ~ spl129_295 ),
inference(forward_subsumption_resolution,[],[f56894,f56323]) ).
fof(f57062,plain,
( spl129_34
| spl129_35
| ~ spl129_295 ),
inference(avatar_split_clause,[],[f57061,f56322,f1330,f1327]) ).
fof(f57363,plain,
( ~ v__1(sK81,nn,nn)
| ~ v__1(sortedList_first,nn,nn)
| ~ object(nn)
| ~ spl129_130 ),
inference(forward_subsumption_resolution,[],[f51821,f130]) ).
fof(f57373,plain,
( ~ v__1(sK81,nn,nn)
| ~ object(nn)
| ~ spl129_106
| ~ spl129_130 ),
inference(forward_subsumption_resolution,[],[f57363,f1774]) ).
fof(f57375,plain,
( ~ v__1(sK81,nn,nn)
| ~ spl129_106
| ~ spl129_130 ),
inference(forward_subsumption_resolution,[],[f57373,f101]) ).
fof(f57918,plain,
( node_next(nn) = sK27
| sP6(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| spl129_1
| spl129_3
| ~ spl129_37
| ~ spl129_40 ),
inference(forward_subsumption_resolution,[],[f47556,f1177]) ).
fof(f57926,plain,
( node_next(nn) = sK27
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| spl129_223 ),
inference(forward_subsumption_resolution,[],[f56181,f1328]) ).
fof(f57930,plain,
( node_next(nn) = sK27
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| spl129_1
| spl129_3
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40 ),
inference(forward_subsumption_resolution,[],[f57918,f1328]) ).
fof(f57938,plain,
( node_next(nn) = sK27
| sP16(sK2)
| sP18(sK2)
| sP3(sK2)
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_223 ),
inference(forward_subsumption_resolution,[],[f57926,f1908]) ).
fof(f57942,plain,
( node_next(nn) = sK27
| sP16(sK2)
| sP18(sK2)
| sP3(sK2)
| spl129_1
| spl129_3
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111 ),
inference(forward_subsumption_resolution,[],[f57930,f1908]) ).
fof(f57950,plain,
( node_next(nn) = sK27
| sP16(sK2)
| sP3(sK2)
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_137
| spl129_223 ),
inference(forward_subsumption_resolution,[],[f57938,f2402]) ).
fof(f57954,plain,
( node_next(nn) = sK27
| sP16(sK2)
| sP3(sK2)
| spl129_1
| spl129_3
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_137 ),
inference(forward_subsumption_resolution,[],[f57942,f2402]) ).
fof(f57962,plain,
( node_next(nn) = sK27
| sP16(sK2)
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_137
| spl129_223 ),
inference(forward_subsumption_resolution,[],[f57950,f1262]) ).
fof(f57966,plain,
( node_next(nn) = sK27
| sP16(sK2)
| spl129_1
| spl129_3
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_137 ),
inference(forward_subsumption_resolution,[],[f57954,f1262]) ).
fof(f57973,plain,
( sK27 = sK81
| sP16(sK2)
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| ~ spl129_130
| spl129_137
| spl129_223 ),
inference(forward_demodulation,[],[f57962,f2234]) ).
fof(f57976,plain,
( sK27 = sK81
| sP16(sK2)
| spl129_1
| spl129_3
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| ~ spl129_130
| spl129_137 ),
inference(forward_demodulation,[],[f57966,f2234]) ).
fof(f58089,plain,
( sK27 = sK81
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| ~ spl129_130
| spl129_137
| spl129_139
| spl129_223 ),
inference(forward_subsumption_resolution,[],[f57973,f2410]) ).
fof(f58090,plain,
( sK27 = sK81
| spl129_1
| spl129_3
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| ~ spl129_130
| spl129_137
| spl129_139 ),
inference(forward_subsumption_resolution,[],[f57976,f2410]) ).
fof(f58447,plain,
( spl129_290
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| ~ spl129_130
| spl129_137
| spl129_139
| spl129_223 ),
inference(avatar_split_clause,[],[f58089,f28259,f2409,f2401,f2232,f1907,f1351,f1339,f1327,f1261,f54828]) ).
fof(f58448,plain,
( spl129_290
| spl129_1
| spl129_3
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| ~ spl129_130
| spl129_137
| spl129_139 ),
inference(avatar_split_clause,[],[f58090,f2409,f2401,f2232,f1907,f1351,f1339,f1327,f1261,f1184,f1175,f54828]) ).
fof(f59485,plain,
( v__1(sK27,sK2,sK2)
| ~ spl129_103
| ~ spl129_114
| ~ spl129_140
| ~ spl129_286 ),
inference(forward_demodulation,[],[f53655,f2122]) ).
fof(f60084,plain,
( ~ v__1(sK27,sK2,sK2)
| ~ spl129_114
| spl129_129
| ~ spl129_290 ),
inference(forward_demodulation,[],[f32802,f54830]) ).
fof(f60137,plain,
( sK27 = sK100(sK2)
| ~ spl129_123
| ~ spl129_130
| ~ spl129_186
| ~ spl129_290 ),
inference(forward_demodulation,[],[f54206,f54830]) ).
fof(f60424,plain,
( v__1(sK27,sK2,nn)
| ~ sP29(sK2)
| ~ spl129_101
| ~ spl129_123
| ~ spl129_130
| ~ spl129_186
| ~ spl129_290 ),
inference(superposition,[],[f1755,f60137]) ).
fof(f60425,plain,
( v__1(sK27,sK2,nn)
| ~ spl129_101
| ~ spl129_123
| ~ spl129_130
| ~ spl129_186
| ~ spl129_290 ),
inference(forward_subsumption_resolution,[],[f60424,f18462]) ).
fof(f60427,plain,
( v__1(sK27,sK2,sK2)
| ~ spl129_101
| ~ spl129_114
| ~ spl129_123
| ~ spl129_130
| ~ spl129_186
| ~ spl129_290 ),
inference(forward_demodulation,[],[f60425,f2122]) ).
fof(f60430,plain,
( $false
| ~ spl129_101
| ~ spl129_114
| ~ spl129_123
| spl129_129
| ~ spl129_130
| ~ spl129_186
| ~ spl129_290 ),
inference(forward_subsumption_resolution,[],[f60427,f60084]) ).
fof(f60431,plain,
( ~ spl129_101
| ~ spl129_114
| ~ spl129_123
| spl129_129
| ~ spl129_130
| ~ spl129_186
| ~ spl129_290 ),
inference(avatar_contradiction_clause,[],[f60430]) ).
fof(f60998,plain,
( sK81 = sK95
| ~ sP65
| ~ spl129_130 ),
inference(forward_demodulation,[],[f357,f2234]) ).
fof(f60999,plain,
( v__1(sK95,sK2,sK2)
| ~ sP65
| ~ spl129_114 ),
inference(forward_demodulation,[],[f358,f2122]) ).
fof(f61147,plain,
( sK81 = sK95
| ~ spl129_3
| ~ spl129_130 ),
inference(forward_subsumption_resolution,[],[f60998,f1185]) ).
fof(f61149,plain,
( v__1(sK95,sK2,sK2)
| ~ spl129_3
| ~ spl129_114 ),
inference(forward_subsumption_resolution,[],[f60999,f1185]) ).
fof(f61150,plain,
( v__1(sK81,sK2,sK2)
| ~ spl129_3
| ~ spl129_114
| ~ spl129_130 ),
inference(forward_demodulation,[],[f61149,f61147]) ).
fof(f61262,plain,
( sK27 != sK42
| ~ spl129_283
| spl129_286 ),
inference(superposition,[],[f53644,f53017]) ).
fof(f65304,plain,
( ~ v__1(sK81,sK2,sK2)
| ~ spl129_106
| ~ spl129_114
| ~ spl129_130 ),
inference(forward_demodulation,[],[f57375,f2122]) ).
fof(f65305,plain,
( $false
| ~ spl129_106
| ~ spl129_114
| ~ spl129_129
| ~ spl129_130 ),
inference(forward_subsumption_resolution,[],[f65304,f32715]) ).
fof(f65306,plain,
( ~ spl129_106
| ~ spl129_114
| ~ spl129_129
| ~ spl129_130 ),
inference(avatar_contradiction_clause,[],[f65305]) ).
fof(f65408,plain,
( ~ v__1(sK42,sK2,sK2)
| ~ spl129_106
| ~ spl129_114
| ~ spl129_130
| ~ spl129_289 ),
inference(forward_demodulation,[],[f65304,f54826]) ).
fof(f65439,plain,
( $false
| ~ spl129_106
| ~ spl129_114
| ~ spl129_130
| ~ spl129_140
| ~ spl129_289 ),
inference(forward_subsumption_resolution,[],[f65408,f55291]) ).
fof(f65440,plain,
( ~ spl129_106
| ~ spl129_114
| ~ spl129_130
| ~ spl129_140
| ~ spl129_289 ),
inference(avatar_contradiction_clause,[],[f65439]) ).
fof(f65629,plain,
( $false
| ~ spl129_3
| ~ spl129_114
| spl129_129
| ~ spl129_130 ),
inference(forward_subsumption_resolution,[],[f61150,f32802]) ).
fof(f65630,plain,
( ~ spl129_3
| ~ spl129_114
| spl129_129
| ~ spl129_130 ),
inference(avatar_contradiction_clause,[],[f65629]) ).
fof(f66787,plain,
( $false
| ~ spl129_114
| ~ spl129_124
| spl129_129
| ~ spl129_130
| ~ spl129_140 ),
inference(forward_subsumption_resolution,[],[f52200,f32802]) ).
fof(f66788,plain,
( ~ spl129_114
| ~ spl129_124
| spl129_129
| ~ spl129_130
| ~ spl129_140 ),
inference(avatar_contradiction_clause,[],[f66787]) ).
fof(f66893,plain,
( node_next(sK2) = sK49(sK2)
| ~ spl129_114
| ~ spl129_131
| ~ spl129_140 ),
inference(forward_demodulation,[],[f18422,f2122]) ).
fof(f67107,plain,
( sP65
| sP66
| node_next(nn) = sK27
| sP5(sK2)
| sP6(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| ~ spl129_40 ),
inference(forward_subsumption_resolution,[],[f1020,f1352]) ).
fof(f67114,plain,
( sP65
| sP66
| node_next(nn) = sK27
| sP6(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| ~ spl129_37
| ~ spl129_40 ),
inference(forward_subsumption_resolution,[],[f67107,f1340]) ).
fof(f68183,definition,
( spl129_319
<=> v__1(sortedList_first,sK42,sK42) ),
introduced(definition,[new_symbols(definition,[spl129_319])],[avatar_definition]) ).
fof(f68184,plain,
( ~ v__1(sortedList_first,sK42,sK42)
| spl129_319 ),
inference(avatar_component_clause,[],[f68183]) ).
fof(f68185,plain,
( v__1(sortedList_first,sK42,sK42)
| ~ spl129_319 ),
inference(avatar_component_clause,[],[f68183]) ).
fof(f68187,definition,
( spl129_320
<=> null = sK42 ),
introduced(definition,[new_symbols(definition,[spl129_320])],[avatar_definition]) ).
fof(f68188,plain,
( null != sK42
| spl129_320 ),
inference(avatar_component_clause,[],[f68187]) ).
fof(f68189,plain,
( null = sK42
| ~ spl129_320 ),
inference(avatar_component_clause,[],[f68187]) ).
fof(f69023,definition,
( spl129_322
<=> v__1(sortedList_first,sK27,sK27) ),
introduced(definition,[new_symbols(definition,[spl129_322])],[avatar_definition]) ).
fof(f69024,plain,
( ~ v__1(sortedList_first,sK27,sK27)
| spl129_322 ),
inference(avatar_component_clause,[],[f69023]) ).
fof(f69025,plain,
( v__1(sortedList_first,sK27,sK27)
| ~ spl129_322 ),
inference(avatar_component_clause,[],[f69023]) ).
fof(f69027,definition,
( spl129_323
<=> null = sK27 ),
introduced(definition,[new_symbols(definition,[spl129_323])],[avatar_definition]) ).
fof(f69028,plain,
( null != sK27
| spl129_323 ),
inference(avatar_component_clause,[],[f69027]) ).
fof(f69029,plain,
( null = sK27
| ~ spl129_323 ),
inference(avatar_component_clause,[],[f69027]) ).
fof(f70176,plain,
( sK42 = node_next(sK2)
| ~ spl129_114
| ~ spl129_131
| ~ spl129_140
| ~ spl129_283 ),
inference(forward_demodulation,[],[f66893,f53017]) ).
fof(f70370,definition,
( spl129_328
<=> sK45 = sK75 ),
introduced(definition,[new_symbols(definition,[spl129_328])],[avatar_definition]) ).
fof(f70371,plain,
( sK45 != sK75
| spl129_328 ),
inference(avatar_component_clause,[],[f70370]) ).
fof(f70372,plain,
( sK45 = sK75
| ~ spl129_328 ),
inference(avatar_component_clause,[],[f70370]) ).
fof(f70664,plain,
( ~ v__1(sK42,sK2,sK2)
| null = sK2
| ~ v__1(sortedList_first,sK2,sK2)
| ~ object(sK2)
| ~ spl129_114
| ~ spl129_131
| ~ spl129_140
| ~ spl129_283 ),
inference(superposition,[],[f5141,f70176]) ).
fof(f70667,plain,
( ~ v__1(sK42,sK2,sK2)
| ~ v__1(sortedList_first,sK2,sK2)
| ~ object(sK2)
| ~ spl129_114
| ~ spl129_131
| ~ spl129_140
| ~ spl129_283 ),
inference(forward_subsumption_resolution,[],[f70664,f1104]) ).
fof(f70677,plain,
( ~ v__1(sK42,sK2,sK2)
| ~ object(sK2)
| ~ spl129_113
| ~ spl129_114
| ~ spl129_131
| ~ spl129_140
| ~ spl129_283 ),
inference(forward_subsumption_resolution,[],[f70667,f2117]) ).
fof(f70681,plain,
( ~ v__1(sK42,sK2,sK2)
| ~ spl129_113
| ~ spl129_114
| ~ spl129_131
| ~ spl129_140
| ~ spl129_283 ),
inference(forward_subsumption_resolution,[],[f70677,f1105]) ).
fof(f71513,plain,
( ! [X0] :
( v__1(sK75,prev_2,prev_2)
| node_next(nn) = sK45
| ~ sP6(X0) )
| ~ spl129_292 ),
inference(forward_demodulation,[],[f586,f56284]) ).
fof(f71574,plain,
( ! [X0] :
( ~ v__1(X0,sK2,sK2)
| ~ v__1(sortedList_first,X0,X0)
| ~ object(sK2)
| ~ object(X0)
| ~ object(sortedList_first) )
| spl129_113 ),
inference(resolution,[],[f2118,f111]) ).
fof(f71593,plain,
( ! [X0] :
( ~ v__1(X0,sK2,sK2)
| ~ v__1(sortedList_first,X0,X0)
| ~ object(X0)
| ~ object(sortedList_first) )
| spl129_113 ),
inference(forward_subsumption_resolution,[],[f71574,f1105]) ).
fof(f71600,plain,
( ! [X0] :
( ~ v__1(X0,sK2,sK2)
| ~ v__1(sortedList_first,X0,X0)
| ~ object(X0) )
| spl129_113 ),
inference(forward_subsumption_resolution,[],[f71593,f108]) ).
fof(f72294,plain,
( node_next(nn) = sK49(sK2)
| ~ spl129_131
| ~ spl129_140 ),
inference(resolution,[],[f2245,f2415]) ).
fof(f72296,plain,
( ! [X0] :
( node_next(nn) = sK45
| ~ sP6(X0) )
| spl129_216 ),
inference(forward_subsumption_resolution,[],[f596,f25268]) ).
fof(f72298,definition,
( spl129_332
<=> node_next(nn) = sK45 ),
introduced(definition,[new_symbols(definition,[spl129_332])],[avatar_definition]) ).
fof(f72299,plain,
( node_next(nn) != sK45
| spl129_332 ),
inference(avatar_component_clause,[],[f72298]) ).
fof(f72300,plain,
( node_next(nn) = sK45
| ~ spl129_332 ),
inference(avatar_component_clause,[],[f72298]) ).
fof(f72301,plain,
( spl129_34
| spl129_332
| spl129_216 ),
inference(avatar_split_clause,[],[f72296,f25267,f72298,f1327]) ).
fof(f72322,plain,
( ~ v__1(sK45,nn,nn)
| nn = null
| ~ v__1(sortedList_first,nn,nn)
| ~ object(nn)
| ~ spl129_332 ),
inference(superposition,[],[f5141,f72300]) ).
fof(f72325,plain,
( nn = null
| ~ v__1(sortedList_first,nn,nn)
| ~ object(nn)
| ~ spl129_244
| ~ spl129_332 ),
inference(forward_subsumption_resolution,[],[f72322,f36957]) ).
fof(f72332,plain,
( ~ v__1(sortedList_first,nn,nn)
| ~ object(nn)
| ~ spl129_244
| ~ spl129_332 ),
inference(forward_subsumption_resolution,[],[f72325,f130]) ).
fof(f72335,plain,
( ~ object(nn)
| ~ spl129_106
| ~ spl129_244
| ~ spl129_332 ),
inference(forward_subsumption_resolution,[],[f72332,f1774]) ).
fof(f72337,plain,
( $false
| ~ spl129_106
| ~ spl129_244
| ~ spl129_332 ),
inference(forward_subsumption_resolution,[],[f72335,f101]) ).
fof(f72338,plain,
( ~ spl129_106
| ~ spl129_244
| ~ spl129_332 ),
inference(avatar_contradiction_clause,[],[f72337]) ).
fof(f72381,plain,
( ! [X0] :
( node_next(nn) = sK75
| ~ sP6(X0) )
| spl129_332 ),
inference(forward_subsumption_resolution,[],[f595,f72299]) ).
fof(f72383,definition,
( spl129_333
<=> node_next(nn) = sK75 ),
introduced(definition,[new_symbols(definition,[spl129_333])],[avatar_definition]) ).
fof(f72384,plain,
( node_next(nn) != sK75
| spl129_333 ),
inference(avatar_component_clause,[],[f72383]) ).
fof(f72385,plain,
( node_next(nn) = sK75
| ~ spl129_333 ),
inference(avatar_component_clause,[],[f72383]) ).
fof(f72386,plain,
( spl129_34
| spl129_333
| spl129_332 ),
inference(avatar_split_clause,[],[f72381,f72298,f72383,f1327]) ).
fof(f72437,plain,
( ! [X0] :
( node_next(nn) = sK45
| ~ sP6(X0) )
| ~ spl129_292
| spl129_296 ),
inference(forward_subsumption_resolution,[],[f71513,f56365]) ).
fof(f72438,plain,
( ! [X0] : ~ sP6(X0)
| ~ spl129_292
| spl129_296
| spl129_332 ),
inference(forward_subsumption_resolution,[],[f72437,f72299]) ).
fof(f72439,plain,
( spl129_34
| ~ spl129_292
| spl129_296
| spl129_332 ),
inference(avatar_split_clause,[],[f72438,f72298,f56364,f56282,f1327]) ).
fof(f72483,plain,
( object(sK45)
| ~ spl129_332 ),
inference(superposition,[],[f109,f72300]) ).
fof(f72507,plain,
( $false
| spl129_35
| ~ spl129_332 ),
inference(forward_subsumption_resolution,[],[f72483,f1331]) ).
fof(f72508,plain,
( spl129_35
| ~ spl129_332 ),
inference(avatar_contradiction_clause,[],[f72507]) ).
fof(f72807,plain,
( ~ v__1(sK75,nn,nn)
| nn = null
| ~ v__1(sortedList_first,nn,nn)
| ~ object(nn)
| ~ spl129_333 ),
inference(superposition,[],[f5141,f72385]) ).
fof(f72810,plain,
( nn = null
| ~ v__1(sortedList_first,nn,nn)
| ~ object(nn)
| ~ spl129_295
| ~ spl129_333 ),
inference(forward_subsumption_resolution,[],[f72807,f56323]) ).
fof(f72823,plain,
( ~ v__1(sortedList_first,nn,nn)
| ~ object(nn)
| ~ spl129_295
| ~ spl129_333 ),
inference(forward_subsumption_resolution,[],[f72810,f130]) ).
fof(f72831,plain,
( ~ object(nn)
| ~ spl129_106
| ~ spl129_295
| ~ spl129_333 ),
inference(forward_subsumption_resolution,[],[f72823,f1774]) ).
fof(f72838,plain,
( $false
| ~ spl129_106
| ~ spl129_295
| ~ spl129_333 ),
inference(forward_subsumption_resolution,[],[f72831,f101]) ).
fof(f72839,plain,
( ~ spl129_106
| ~ spl129_295
| ~ spl129_333 ),
inference(avatar_contradiction_clause,[],[f72838]) ).
fof(f72845,plain,
( ! [X0] :
( node_next(nn) = sK76
| ~ sP6(X0) )
| spl129_332 ),
inference(forward_subsumption_resolution,[],[f585,f72299]) ).
fof(f72849,plain,
( ! [X0] :
( sK75 = sK76
| ~ sP6(X0) )
| spl129_332
| ~ spl129_333 ),
inference(forward_demodulation,[],[f72845,f72385]) ).
fof(f72985,plain,
( ! [X0] : ~ sP6(X0)
| spl129_292
| spl129_332
| ~ spl129_333 ),
inference(forward_subsumption_resolution,[],[f72849,f56283]) ).
fof(f72986,plain,
( spl129_34
| spl129_292
| spl129_332
| ~ spl129_333 ),
inference(avatar_split_clause,[],[f72985,f72383,f72298,f56282,f1327]) ).
fof(f72995,plain,
( ! [X0] :
( sK75 = sK76
| v__1(sK45,prev_2,nn)
| ~ sP6(X0) )
| ~ spl129_333 ),
inference(forward_demodulation,[],[f582,f72385]) ).
fof(f72997,plain,
( ! [X0] :
( v__1(sK45,prev_2,nn)
| ~ sP6(X0) )
| spl129_292
| ~ spl129_333 ),
inference(forward_subsumption_resolution,[],[f72995,f56283]) ).
fof(f73098,plain,
( ! [X0] : ~ sP6(X0)
| spl129_204
| spl129_292
| ~ spl129_333 ),
inference(forward_subsumption_resolution,[],[f72997,f23291]) ).
fof(f73099,plain,
( spl129_34
| spl129_204
| spl129_292
| ~ spl129_333 ),
inference(avatar_split_clause,[],[f73098,f72383,f56282,f23290,f1327]) ).
fof(f73100,plain,
( node_next(nn) != sK45
| ~ spl129_328
| spl129_333 ),
inference(forward_demodulation,[],[f72384,f70372]) ).
fof(f73101,plain,
( ! [X0] :
( node_next(nn) = sK75
| ~ sP6(X0) )
| spl129_204 ),
inference(forward_subsumption_resolution,[],[f592,f23291]) ).
fof(f73103,plain,
( $false
| ~ spl129_328
| ~ spl129_332
| spl129_333 ),
inference(forward_subsumption_resolution,[],[f73100,f72300]) ).
fof(f73104,plain,
( ~ spl129_328
| ~ spl129_332
| spl129_333 ),
inference(avatar_contradiction_clause,[],[f73103]) ).
fof(f73109,plain,
( ! [X0] :
( sK45 = sK75
| ~ sP6(X0) )
| spl129_204
| ~ spl129_332 ),
inference(forward_demodulation,[],[f73101,f72300]) ).
fof(f73119,plain,
( ! [X0] : ~ sP6(X0)
| spl129_204
| spl129_328
| ~ spl129_332 ),
inference(forward_subsumption_resolution,[],[f73109,f70371]) ).
fof(f73120,plain,
( spl129_34
| spl129_204
| spl129_328
| ~ spl129_332 ),
inference(avatar_split_clause,[],[f73119,f72298,f70370,f23290,f1327]) ).
fof(f73123,plain,
( sP66
| node_next(nn) = sK27
| sP6(sK2)
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| spl129_3
| ~ spl129_37
| ~ spl129_40 ),
inference(forward_subsumption_resolution,[],[f67114,f1186]) ).
fof(f73319,plain,
( sP66
| node_next(nn) = sK27
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| spl129_3
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40 ),
inference(forward_subsumption_resolution,[],[f73123,f1328]) ).
fof(f73329,plain,
( sP66
| node_next(nn) = sK27
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| spl129_3
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| spl129_139 ),
inference(forward_subsumption_resolution,[],[f73319,f2410]) ).
fof(f73335,plain,
( sP66
| node_next(nn) = sK27
| sP18(sK2)
| sP3(sK2)
| spl129_3
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_139 ),
inference(forward_subsumption_resolution,[],[f73329,f1908]) ).
fof(f73341,plain,
( sP66
| node_next(nn) = sK27
| sP3(sK2)
| spl129_3
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_137
| spl129_139 ),
inference(forward_subsumption_resolution,[],[f73335,f2402]) ).
fof(f73347,plain,
( sP66
| node_next(nn) = sK27
| spl129_3
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_137
| spl129_139 ),
inference(forward_subsumption_resolution,[],[f73341,f1262]) ).
fof(f73551,plain,
( node_next(nn) = sK27
| ~ spl129_131
| ~ spl129_140
| ~ spl129_286 ),
inference(forward_demodulation,[],[f25113,f53645]) ).
fof(f73575,plain,
( ~ v__1(sK27,nn,nn)
| nn = null
| ~ v__1(sortedList_first,nn,nn)
| ~ object(nn)
| ~ spl129_131
| ~ spl129_140
| ~ spl129_286 ),
inference(superposition,[],[f5141,f73551]) ).
fof(f75309,plain,
( ~ v__1(sK27,nn,nn)
| ~ v__1(sortedList_first,nn,nn)
| ~ object(nn)
| ~ spl129_131
| ~ spl129_140
| ~ spl129_286 ),
inference(forward_subsumption_resolution,[],[f73575,f130]) ).
fof(f75321,plain,
( ~ v__1(sK27,nn,nn)
| ~ object(nn)
| ~ spl129_106
| ~ spl129_131
| ~ spl129_140
| ~ spl129_286 ),
inference(forward_subsumption_resolution,[],[f75309,f1774]) ).
fof(f75329,plain,
( ~ v__1(sK27,nn,nn)
| ~ spl129_106
| ~ spl129_131
| ~ spl129_140
| ~ spl129_286 ),
inference(forward_subsumption_resolution,[],[f75321,f101]) ).
fof(f75346,plain,
( node_next(nn) = sK42
| ~ spl129_223 ),
inference(resolution,[],[f28261,f666]) ).
fof(f75967,plain,
( ! [X0] :
( v__1(sK100(X0),X0,nn)
| ~ sP29(X0) )
| spl129_124 ),
inference(forward_subsumption_resolution,[],[f269,f2194]) ).
fof(f75980,plain,
( ! [X0] :
( ~ v__1(X0,nn,nn)
| ~ v__1(sK114,X0,nn)
| ~ object(nn)
| ~ object(X0)
| ~ object(sK114)
| ~ object(nn) )
| spl129_119 ),
inference(resolution,[],[f2159,f112]) ).
fof(f75981,plain,
( ! [X0] :
( ~ v__1(X0,nn,nn)
| ~ v__1(sK114,X0,nn)
| ~ object(nn)
| ~ object(X0)
| ~ object(sK114) )
| spl129_119 ),
inference(duplicate_literal_removal,[],[f75980]) ).
fof(f75986,plain,
( ! [X0] :
( ~ v__1(sK114,X0,nn)
| ~ object(nn)
| ~ object(X0)
| ~ object(sK114) )
| spl129_119 ),
inference(forward_subsumption_resolution,[],[f75981,f117]) ).
fof(f75993,plain,
( ! [X0] :
( ~ v__1(sK114,X0,nn)
| ~ object(X0)
| ~ object(sK114) )
| spl129_119 ),
inference(forward_subsumption_resolution,[],[f75986,f101]) ).
fof(f76000,plain,
( ! [X0] :
( ~ v__1(sK114,X0,nn)
| ~ object(X0) )
| ~ spl129_61
| spl129_119 ),
inference(forward_subsumption_resolution,[],[f75993,f1500]) ).
fof(f76001,plain,
( spl129_101
| spl129_124 ),
inference(avatar_split_clause,[],[f75967,f2193,f1754]) ).
fof(f76531,plain,
( node_next(nn) = sK27
| spl129_1
| spl129_3
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_137
| spl129_139 ),
inference(forward_subsumption_resolution,[],[f73347,f1177]) ).
fof(f76728,plain,
( v__1(sK42,sK2,nn)
| ~ sP8(sK2)
| ~ spl129_103
| ~ spl129_283 ),
inference(superposition,[],[f1763,f53017]) ).
fof(f76730,plain,
( v__1(sK42,sK2,nn)
| ~ spl129_103
| ~ spl129_140
| ~ spl129_283 ),
inference(forward_subsumption_resolution,[],[f76728,f2415]) ).
fof(f76731,plain,
( sK27 = sK42
| spl129_1
| spl129_3
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_137
| spl129_139
| ~ spl129_223 ),
inference(forward_demodulation,[],[f75346,f76531]) ).
fof(f76732,plain,
( $false
| spl129_1
| spl129_3
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_137
| spl129_139
| ~ spl129_223
| spl129_287 ),
inference(forward_subsumption_resolution,[],[f76731,f53648]) ).
fof(f76733,plain,
( spl129_1
| spl129_3
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_137
| spl129_139
| ~ spl129_223
| spl129_287 ),
inference(avatar_contradiction_clause,[],[f76732]) ).
fof(f76872,plain,
( node_next(nn) = sK42
| ~ spl129_131
| ~ spl129_140
| ~ spl129_283 ),
inference(forward_demodulation,[],[f18422,f53017]) ).
fof(f76912,plain,
( ! [X0] :
( ~ v__1(sK42,X0,nn)
| ~ object(X0) )
| ~ spl129_61
| spl129_119
| ~ spl129_124
| ~ spl129_223 ),
inference(forward_demodulation,[],[f76000,f52048]) ).
fof(f77415,plain,
( ~ object(sK2)
| ~ spl129_61
| ~ spl129_103
| spl129_119
| ~ spl129_124
| ~ spl129_140
| ~ spl129_223
| ~ spl129_283 ),
inference(resolution,[],[f76730,f76912]) ).
fof(f77451,plain,
( $false
| ~ spl129_61
| ~ spl129_103
| spl129_119
| ~ spl129_124
| ~ spl129_140
| ~ spl129_223
| ~ spl129_283 ),
inference(forward_subsumption_resolution,[],[f77415,f1105]) ).
fof(f77452,plain,
( ~ spl129_61
| ~ spl129_103
| spl129_119
| ~ spl129_124
| ~ spl129_140
| ~ spl129_223
| ~ spl129_283 ),
inference(avatar_contradiction_clause,[],[f77451]) ).
fof(f77468,plain,
( ~ object(sK42)
| spl129_61
| ~ spl129_124
| ~ spl129_223 ),
inference(forward_demodulation,[],[f1499,f52048]) ).
fof(f77554,plain,
( $false
| spl129_61
| ~ spl129_124
| ~ spl129_223 ),
inference(forward_subsumption_resolution,[],[f77468,f28264]) ).
fof(f77555,plain,
( spl129_61
| ~ spl129_124
| ~ spl129_223 ),
inference(avatar_contradiction_clause,[],[f77554]) ).
fof(f77619,plain,
( v__1(sK42,nn,nn)
| ~ spl129_119
| ~ spl129_124
| ~ spl129_223 ),
inference(forward_demodulation,[],[f2158,f52048]) ).
fof(f77640,plain,
( $false
| ~ spl129_106
| ~ spl129_119
| ~ spl129_124
| ~ spl129_223 ),
inference(forward_subsumption_resolution,[],[f77619,f52093]) ).
fof(f77641,plain,
( ~ spl129_106
| ~ spl129_119
| ~ spl129_124
| ~ spl129_223 ),
inference(avatar_contradiction_clause,[],[f77640]) ).
fof(f77645,plain,
( sP67(sK42)
| node_next(nn) = sK27
| sP16(sK2)
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40 ),
inference(forward_subsumption_resolution,[],[f53390,f1328]) ).
fof(f77654,plain,
( sP67(sK42)
| node_next(nn) = sK27
| sP17(sK2)
| sP18(sK2)
| sP3(sK2)
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| spl129_139 ),
inference(forward_subsumption_resolution,[],[f77645,f2410]) ).
fof(f77660,plain,
( sP67(sK42)
| node_next(nn) = sK27
| sP18(sK2)
| sP3(sK2)
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_139 ),
inference(forward_subsumption_resolution,[],[f77654,f1908]) ).
fof(f77663,plain,
( sP67(sK42)
| node_next(nn) = sK27
| sP3(sK2)
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_137
| spl129_139 ),
inference(forward_subsumption_resolution,[],[f77660,f2402]) ).
fof(f77666,plain,
( sP67(sK42)
| node_next(nn) = sK27
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_137
| spl129_139 ),
inference(forward_subsumption_resolution,[],[f77663,f1262]) ).
fof(f78149,plain,
( $false
| ~ spl129_283
| spl129_286
| ~ spl129_287 ),
inference(forward_subsumption_resolution,[],[f61262,f53649]) ).
fof(f78150,plain,
( ~ spl129_283
| spl129_286
| ~ spl129_287 ),
inference(avatar_contradiction_clause,[],[f78149]) ).
fof(f78213,plain,
( v__1(sortedList_first,sK27,sK27)
| null = sK27
| nn = null
| ~ object(nn)
| ~ spl129_131
| ~ spl129_140
| ~ spl129_286 ),
inference(superposition,[],[f4253,f73551]) ).
fof(f78477,plain,
( v__1(sortedList_first,sK27,sK27)
| nn = null
| ~ object(nn)
| ~ spl129_131
| ~ spl129_140
| ~ spl129_286
| spl129_323 ),
inference(forward_subsumption_resolution,[],[f78213,f69028]) ).
fof(f78484,plain,
( v__1(sortedList_first,sK27,sK27)
| ~ object(nn)
| ~ spl129_131
| ~ spl129_140
| ~ spl129_286
| spl129_323 ),
inference(forward_subsumption_resolution,[],[f78477,f130]) ).
fof(f78489,plain,
( v__1(sortedList_first,sK27,sK27)
| ~ spl129_131
| ~ spl129_140
| ~ spl129_286
| spl129_323 ),
inference(forward_subsumption_resolution,[],[f78484,f101]) ).
fof(f78534,plain,
( v__1(null,sK2,nn)
| ~ spl129_103
| ~ spl129_140
| ~ spl129_286
| ~ spl129_323 ),
inference(superposition,[],[f53655,f69029]) ).
fof(f78577,plain,
( $false
| ~ spl129_103
| ~ spl129_140
| spl129_207
| ~ spl129_286
| ~ spl129_323 ),
inference(forward_subsumption_resolution,[],[f78534,f23655]) ).
fof(f78578,plain,
( ~ spl129_103
| ~ spl129_140
| spl129_207
| ~ spl129_286
| ~ spl129_323 ),
inference(avatar_contradiction_clause,[],[f78577]) ).
fof(f78580,plain,
( $false
| ~ spl129_131
| ~ spl129_140
| ~ spl129_286
| spl129_322
| spl129_323 ),
inference(forward_subsumption_resolution,[],[f78489,f69024]) ).
fof(f78581,plain,
( ~ spl129_131
| ~ spl129_140
| ~ spl129_286
| spl129_322
| spl129_323 ),
inference(avatar_contradiction_clause,[],[f78580]) ).
fof(f78585,plain,
( node_next(nn) = sK96
| ~ spl129_1 ),
inference(forward_subsumption_resolution,[],[f355,f1176]) ).
fof(f78592,plain,
( sK42 = sK34(sK2)
| ~ spl129_131
| ~ spl129_140
| ~ spl129_283 ),
inference(forward_demodulation,[],[f36386,f76872]) ).
fof(f78610,plain,
( sK42 = sK96
| ~ spl129_1
| ~ spl129_131
| ~ spl129_140
| ~ spl129_283 ),
inference(forward_demodulation,[],[f78585,f76872]) ).
fof(f78617,plain,
( sK27 = sK34(sK2)
| ~ spl129_131
| ~ spl129_140
| ~ spl129_283
| ~ spl129_287 ),
inference(forward_demodulation,[],[f78592,f53649]) ).
fof(f78627,plain,
( node_next(nn) = sK27
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_137
| spl129_139
| spl129_223 ),
inference(forward_subsumption_resolution,[],[f77666,f28260]) ).
fof(f78649,plain,
( v__1(sortedList_first,sK27,sK27)
| null = sK27
| nn = null
| ~ object(nn)
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_137
| spl129_139
| spl129_223 ),
inference(superposition,[],[f4253,f78627]) ).
fof(f78663,plain,
( null = sK27
| nn = null
| ~ object(nn)
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_137
| spl129_139
| spl129_223
| spl129_322 ),
inference(forward_subsumption_resolution,[],[f78649,f69024]) ).
fof(f78673,plain,
( null = sK27
| ~ object(nn)
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_137
| spl129_139
| spl129_223
| spl129_322 ),
inference(forward_subsumption_resolution,[],[f78663,f130]) ).
fof(f78677,plain,
( null = sK27
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_137
| spl129_139
| spl129_223
| spl129_322 ),
inference(forward_subsumption_resolution,[],[f78673,f101]) ).
fof(f78709,plain,
( $false
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_137
| spl129_139
| spl129_223
| spl129_322
| spl129_323 ),
inference(forward_subsumption_resolution,[],[f78677,f69028]) ).
fof(f78710,plain,
( spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_137
| spl129_139
| spl129_223
| spl129_322
| spl129_323 ),
inference(avatar_contradiction_clause,[],[f78709]) ).
fof(f78745,plain,
( v__1(sK42,sK2,sK2)
| ~ sP8(sK2)
| ~ spl129_131
| ~ spl129_140
| ~ spl129_283 ),
inference(superposition,[],[f959,f78592]) ).
fof(f78747,plain,
( v__1(sK42,sK2,sK2)
| ~ spl129_131
| ~ spl129_140
| ~ spl129_283 ),
inference(forward_subsumption_resolution,[],[f78745,f2415]) ).
fof(f79182,plain,
( v__1(sK27,sK2,sK2)
| ~ sP8(sK2)
| ~ spl129_131
| ~ spl129_140
| ~ spl129_283
| ~ spl129_287 ),
inference(superposition,[],[f959,f78617]) ).
fof(f79184,plain,
( v__1(sK27,sK2,sK2)
| ~ spl129_131
| ~ spl129_140
| ~ spl129_283
| ~ spl129_287 ),
inference(forward_subsumption_resolution,[],[f79182,f2415]) ).
fof(f79432,plain,
( ~ v__1(sortedList_first,sK27,sK27)
| ~ object(sK27)
| spl129_113
| ~ spl129_131
| ~ spl129_140
| ~ spl129_283
| ~ spl129_287 ),
inference(resolution,[],[f79184,f71600]) ).
fof(f79476,plain,
( ~ object(sK27)
| spl129_113
| ~ spl129_131
| ~ spl129_140
| ~ spl129_283
| ~ spl129_287
| ~ spl129_322 ),
inference(forward_subsumption_resolution,[],[f79432,f69025]) ).
fof(f79480,plain,
( $false
| spl129_113
| ~ spl129_131
| ~ spl129_140
| ~ spl129_222
| ~ spl129_283
| ~ spl129_287
| ~ spl129_322 ),
inference(forward_subsumption_resolution,[],[f79476,f28257]) ).
fof(f79481,plain,
( spl129_113
| ~ spl129_131
| ~ spl129_140
| ~ spl129_222
| ~ spl129_283
| ~ spl129_287
| ~ spl129_322 ),
inference(avatar_contradiction_clause,[],[f79480]) ).
fof(f79497,plain,
( sK27 = sK34(sK2)
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_137
| spl129_139
| ~ spl129_140
| spl129_223 ),
inference(forward_demodulation,[],[f36386,f78627]) ).
fof(f79523,plain,
( v__1(sK27,sK2,sK2)
| ~ sP8(sK2)
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_137
| spl129_139
| ~ spl129_140
| spl129_223 ),
inference(superposition,[],[f959,f79497]) ).
fof(f79525,plain,
( v__1(sK27,sK2,sK2)
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_137
| spl129_139
| ~ spl129_140
| spl129_223 ),
inference(forward_subsumption_resolution,[],[f79523,f2415]) ).
fof(f79552,plain,
( ~ v__1(sortedList_first,sK27,sK27)
| ~ object(sK27)
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_113
| spl129_137
| spl129_139
| ~ spl129_140
| spl129_223 ),
inference(resolution,[],[f79525,f71600]) ).
fof(f79596,plain,
( ~ object(sK27)
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_113
| spl129_137
| spl129_139
| ~ spl129_140
| spl129_223
| ~ spl129_322 ),
inference(forward_subsumption_resolution,[],[f79552,f69025]) ).
fof(f79600,plain,
( $false
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_113
| spl129_137
| spl129_139
| ~ spl129_140
| ~ spl129_222
| spl129_223
| ~ spl129_322 ),
inference(forward_subsumption_resolution,[],[f79596,f28257]) ).
fof(f79601,plain,
( spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_113
| spl129_137
| spl129_139
| ~ spl129_140
| ~ spl129_222
| spl129_223
| ~ spl129_322 ),
inference(avatar_contradiction_clause,[],[f79600]) ).
fof(f79603,plain,
( sK27 = sK49(sK2)
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| ~ spl129_131
| spl129_137
| spl129_139
| ~ spl129_140
| spl129_223 ),
inference(forward_demodulation,[],[f18422,f78627]) ).
fof(f79643,plain,
( v__1(null,sK2,sK2)
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_137
| spl129_139
| ~ spl129_140
| spl129_223
| ~ spl129_323 ),
inference(superposition,[],[f79525,f69029]) ).
fof(f79644,plain,
( $false
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_137
| spl129_139
| ~ spl129_140
| spl129_150
| spl129_223
| ~ spl129_323 ),
inference(forward_subsumption_resolution,[],[f79643,f3094]) ).
fof(f79645,plain,
( spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_137
| spl129_139
| ~ spl129_140
| spl129_150
| spl129_223
| ~ spl129_323 ),
inference(avatar_contradiction_clause,[],[f79644]) ).
fof(f79648,plain,
( node_next(nn) = sK42
| ~ spl129_223 ),
inference(resolution,[],[f28261,f666]) ).
fof(f79694,plain,
( v__1(sortedList_first,sK96,sK96)
| null = sK96
| nn = null
| ~ object(nn)
| ~ spl129_1 ),
inference(superposition,[],[f4253,f78585]) ).
fof(f79709,plain,
( v__1(sortedList_first,sK96,sK96)
| null = sK96
| ~ object(nn)
| ~ spl129_1 ),
inference(forward_subsumption_resolution,[],[f79694,f130]) ).
fof(f79721,plain,
( v__1(sortedList_first,sK96,sK96)
| null = sK96
| ~ spl129_1 ),
inference(forward_subsumption_resolution,[],[f79709,f101]) ).
fof(f79956,definition,
( spl129_348
<=> null = sK96 ),
introduced(definition,[new_symbols(definition,[spl129_348])],[avatar_definition]) ).
fof(f79958,plain,
( null = sK96
| ~ spl129_348 ),
inference(avatar_component_clause,[],[f79956]) ).
fof(f79960,definition,
( spl129_349
<=> v__1(sortedList_first,sK96,sK96) ),
introduced(definition,[new_symbols(definition,[spl129_349])],[avatar_definition]) ).
fof(f79962,plain,
( v__1(sortedList_first,sK96,sK96)
| ~ spl129_349 ),
inference(avatar_component_clause,[],[f79960]) ).
fof(f79963,plain,
( spl129_348
| spl129_349
| ~ spl129_1 ),
inference(avatar_split_clause,[],[f79721,f1175,f79960,f79956]) ).
fof(f80202,plain,
( sK42 = sK95
| ~ sP65
| ~ spl129_223 ),
inference(forward_demodulation,[],[f357,f79648]) ).
fof(f80223,plain,
( sK42 = sK49(sK2)
| ~ spl129_131
| ~ spl129_140
| ~ spl129_223 ),
inference(forward_demodulation,[],[f72294,f79648]) ).
fof(f80225,plain,
( ! [X0] :
( node_key(X0) != sK0
| ~ v__1(sK42,X0,X0)
| null = X0
| ~ object(X0) )
| ~ spl129_106
| ~ spl129_223 ),
inference(forward_demodulation,[],[f51656,f79648]) ).
fof(f80239,plain,
( $false
| ~ spl129_131
| ~ spl129_140
| ~ spl129_223
| spl129_283 ),
inference(forward_subsumption_resolution,[],[f80223,f53016]) ).
fof(f80240,plain,
( ~ spl129_131
| ~ spl129_140
| ~ spl129_223
| spl129_283 ),
inference(avatar_contradiction_clause,[],[f80239]) ).
fof(f80279,plain,
( sK42 = sK95
| ~ spl129_3
| ~ spl129_223 ),
inference(forward_subsumption_resolution,[],[f80202,f1185]) ).
fof(f80281,plain,
( v__1(sK95,nn,nn)
| ~ spl129_3 ),
inference(forward_subsumption_resolution,[],[f358,f1185]) ).
fof(f80282,plain,
( v__1(sK42,nn,nn)
| ~ spl129_3
| ~ spl129_223 ),
inference(forward_demodulation,[],[f80281,f80279]) ).
fof(f80389,plain,
( sK0 != sK1
| ~ v__1(sK42,nn,nn)
| nn = null
| ~ object(nn)
| ~ spl129_106
| ~ spl129_223 ),
inference(superposition,[],[f80225,f125]) ).
fof(f80391,plain,
( ~ v__1(sK42,nn,nn)
| nn = null
| ~ object(nn)
| ~ spl129_106
| ~ spl129_223 ),
inference(forward_subsumption_resolution,[],[f80389,f3770]) ).
fof(f80393,plain,
( nn = null
| ~ object(nn)
| ~ spl129_3
| ~ spl129_106
| ~ spl129_223 ),
inference(forward_subsumption_resolution,[],[f80391,f80282]) ).
fof(f80395,plain,
( ~ object(nn)
| ~ spl129_3
| ~ spl129_106
| ~ spl129_223 ),
inference(forward_subsumption_resolution,[],[f80393,f130]) ).
fof(f80398,plain,
( $false
| ~ spl129_3
| ~ spl129_106
| ~ spl129_223 ),
inference(forward_subsumption_resolution,[],[f80395,f101]) ).
fof(f80399,plain,
( ~ spl129_3
| ~ spl129_106
| ~ spl129_223 ),
inference(avatar_contradiction_clause,[],[f80398]) ).
fof(f80407,plain,
( v__1(sortedList_first,sK42,sK42)
| ~ spl129_1
| ~ spl129_131
| ~ spl129_140
| ~ spl129_283
| ~ spl129_349 ),
inference(superposition,[],[f79962,f78610]) ).
fof(f80697,plain,
( ~ v__1(sortedList_first,sK42,sK42)
| ~ object(sK42)
| spl129_113
| ~ spl129_131
| ~ spl129_140
| ~ spl129_283 ),
inference(resolution,[],[f78747,f71600]) ).
fof(f80741,plain,
( ~ object(sK42)
| spl129_113
| ~ spl129_131
| ~ spl129_140
| ~ spl129_283
| ~ spl129_319 ),
inference(forward_subsumption_resolution,[],[f80697,f68185]) ).
fof(f80745,plain,
( $false
| spl129_113
| ~ spl129_131
| ~ spl129_140
| ~ spl129_223
| ~ spl129_283
| ~ spl129_319 ),
inference(forward_subsumption_resolution,[],[f80741,f28264]) ).
fof(f80746,plain,
( spl129_113
| ~ spl129_131
| ~ spl129_140
| ~ spl129_223
| ~ spl129_283
| ~ spl129_319 ),
inference(avatar_contradiction_clause,[],[f80745]) ).
fof(f80801,plain,
( $false
| ~ spl129_1
| ~ spl129_131
| ~ spl129_140
| ~ spl129_283
| spl129_319
| ~ spl129_349 ),
inference(forward_subsumption_resolution,[],[f80407,f68184]) ).
fof(f80802,plain,
( ~ spl129_1
| ~ spl129_131
| ~ spl129_140
| ~ spl129_283
| spl129_319
| ~ spl129_349 ),
inference(avatar_contradiction_clause,[],[f80801]) ).
fof(f80804,plain,
( null = sK42
| ~ spl129_1
| ~ spl129_131
| ~ spl129_140
| ~ spl129_283
| ~ spl129_348 ),
inference(superposition,[],[f79958,f78610]) ).
fof(f80814,plain,
( $false
| ~ spl129_1
| ~ spl129_131
| ~ spl129_140
| ~ spl129_283
| spl129_320
| ~ spl129_348 ),
inference(forward_subsumption_resolution,[],[f80804,f68188]) ).
fof(f80815,plain,
( ~ spl129_1
| ~ spl129_131
| ~ spl129_140
| ~ spl129_283
| spl129_320
| ~ spl129_348 ),
inference(avatar_contradiction_clause,[],[f80814]) ).
fof(f80841,plain,
( v__1(null,sK2,nn)
| ~ spl129_103
| ~ spl129_140
| ~ spl129_283
| ~ spl129_320 ),
inference(superposition,[],[f76730,f68189]) ).
fof(f80868,plain,
( $false
| ~ spl129_103
| ~ spl129_140
| spl129_207
| ~ spl129_283
| ~ spl129_320 ),
inference(forward_subsumption_resolution,[],[f80841,f23655]) ).
fof(f80869,plain,
( ~ spl129_103
| ~ spl129_140
| spl129_207
| ~ spl129_283
| ~ spl129_320 ),
inference(avatar_contradiction_clause,[],[f80868]) ).
fof(f80885,plain,
( $false
| ~ spl129_113
| ~ spl129_114
| ~ spl129_131
| ~ spl129_140
| ~ spl129_283 ),
inference(forward_subsumption_resolution,[],[f70681,f78747]) ).
fof(f80886,plain,
( ~ spl129_113
| ~ spl129_114
| ~ spl129_131
| ~ spl129_140
| ~ spl129_283 ),
inference(avatar_contradiction_clause,[],[f80885]) ).
fof(f86665,plain,
( ~ v__1(sK27,sK2,sK2)
| ~ spl129_106
| ~ spl129_114
| ~ spl129_131
| ~ spl129_140
| ~ spl129_286 ),
inference(forward_demodulation,[],[f75329,f2122]) ).
fof(f86666,plain,
( $false
| ~ spl129_103
| ~ spl129_106
| ~ spl129_114
| ~ spl129_131
| ~ spl129_140
| ~ spl129_286 ),
inference(forward_subsumption_resolution,[],[f86665,f59485]) ).
fof(f86667,plain,
( ~ spl129_103
| ~ spl129_106
| ~ spl129_114
| ~ spl129_131
| ~ spl129_140
| ~ spl129_286 ),
inference(avatar_contradiction_clause,[],[f86666]) ).
fof(f86677,plain,
( $false
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| ~ spl129_131
| spl129_137
| spl129_139
| ~ spl129_140
| spl129_223
| spl129_286 ),
inference(forward_subsumption_resolution,[],[f79603,f53644]) ).
fof(f86678,plain,
( spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| ~ spl129_131
| spl129_137
| spl129_139
| ~ spl129_140
| spl129_223
| spl129_286 ),
inference(avatar_contradiction_clause,[],[f86677]) ).
cnf(s74,plain,
( spl129_109
| spl129_111
| spl129_112 ),
inference(sat_conversion,[],[f1963]) ).
cnf(s76,plain,
( ~ spl129_113
| spl129_114 ),
inference(sat_conversion,[],[f2123]) ).
cnf(s85,plain,
( spl129_123
| spl129_124 ),
inference(sat_conversion,[],[f2196]) ).
cnf(s89,plain,
( spl129_103
| ~ spl129_129 ),
inference(sat_conversion,[],[f2226]) ).
cnf(s90,plain,
( spl129_103
| spl129_130 ),
inference(sat_conversion,[],[f2235]) ).
cnf(s91,plain,
( spl129_130
| spl129_131 ),
inference(sat_conversion,[],[f2246]) ).
cnf(s96,plain,
( spl129_20
| ~ spl129_114
| spl129_137
| spl129_138
| spl129_139
| spl129_140
| spl129_141 ),
inference(sat_conversion,[],[f2420]) ).
cnf(s108,plain,
( ~ spl129_15
| spl129_109 ),
inference(sat_conversion,[],[f3670]) ).
cnf(s120,plain,
( spl129_16
| ~ spl129_112 ),
inference(sat_conversion,[],[f5667]) ).
cnf(s122,plain,
( spl129_19
| spl129_109
| spl129_112 ),
inference(sat_conversion,[],[f5703]) ).
cnf(s149,plain,
( ~ spl129_14
| ~ spl129_110
| ~ spl129_114 ),
inference(sat_conversion,[],[f17853]) ).
cnf(s153,plain,
~ spl129_150,
inference(sat_conversion,[],[f18735]) ).
cnf(s156,plain,
~ spl129_16,
inference(sat_conversion,[],[f19323]) ).
cnf(s170,plain,
spl129_14,
inference(sat_conversion,[],[f20360]) ).
cnf(s171,plain,
( ~ spl129_14
| spl129_49
| spl129_110
| ~ spl129_113
| ~ spl129_114 ),
inference(sat_conversion,[],[f20470]) ).
cnf(s173,plain,
( spl129_110
| ~ spl129_114
| ~ spl129_137 ),
inference(sat_conversion,[],[f21431]) ).
cnf(s179,plain,
( spl129_113
| ~ spl129_137 ),
inference(sat_conversion,[],[f22922]) ).
cnf(s199,plain,
( spl129_109
| spl129_112
| ~ spl129_139 ),
inference(sat_conversion,[],[f24906]) ).
cnf(s201,plain,
( spl129_20
| spl129_109
| ~ spl129_111
| spl129_112
| spl129_137
| spl129_140
| spl129_150
| spl129_207 ),
inference(sat_conversion,[],[f25047]) ).
cnf(s202,plain,
( spl129_16
| ~ spl129_207 ),
inference(sat_conversion,[],[f25093]) ).
cnf(s203,plain,
( ~ spl129_141
| spl129_150
| spl129_207 ),
inference(sat_conversion,[],[f25139]) ).
cnf(s220,plain,
( spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| spl129_109
| ~ spl129_111
| spl129_112
| spl129_137
| spl129_150
| spl129_186
| spl129_187 ),
inference(sat_conversion,[],[f25521]) ).
cnf(s223,plain,
( spl129_150
| ~ spl129_187
| spl129_207 ),
inference(sat_conversion,[],[f25821]) ).
cnf(s230,plain,
( ~ spl129_20
| spl129_113
| spl129_150
| spl129_207 ),
inference(sat_conversion,[],[f26599]) ).
cnf(s234,plain,
( ~ spl129_14
| spl129_15
| ~ spl129_19
| ~ spl129_20
| ~ spl129_49
| spl129_110
| spl129_112
| ~ spl129_114 ),
inference(sat_conversion,[],[f26967]) ).
cnf(s237,plain,
( spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| spl129_109
| ~ spl129_111
| spl129_112
| spl129_137
| spl129_222
| spl129_223 ),
inference(sat_conversion,[],[f28262]) ).
cnf(s261,plain,
( ~ spl129_111
| ~ spl129_138 ),
inference(sat_conversion,[],[f33642]) ).
cnf(s285,plain,
( spl129_40
| spl129_109
| spl129_112 ),
inference(sat_conversion,[],[f36777]) ).
cnf(s302,plain,
( spl129_37
| spl129_109
| spl129_112 ),
inference(sat_conversion,[],[f37979]) ).
cnf(s312,plain,
~ spl129_109,
inference(sat_conversion,[],[f38423]) ).
cnf(s355,plain,
spl129_106,
inference(sat_conversion,[],[f45617]) ).
cnf(s363,plain,
( ~ spl129_35
| ~ spl129_204
| spl129_244 ),
inference(sat_conversion,[],[f47203]) ).
cnf(s375,plain,
( spl129_1
| spl129_3
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| spl129_109
| ~ spl129_111
| spl129_112
| spl129_137
| spl129_222 ),
inference(sat_conversion,[],[f47541]) ).
cnf(s391,plain,
( ~ spl129_130
| spl129_277
| spl129_278 ),
inference(sat_conversion,[],[f52413]) ).
cnf(s405,plain,
( ~ spl129_124
| ~ spl129_130
| ~ spl129_140
| spl129_150
| ~ spl129_277 ),
inference(sat_conversion,[],[f54194]) ).
cnf(s406,plain,
( ~ spl129_124
| ~ spl129_130
| spl129_150
| ~ spl129_186
| ~ spl129_277 ),
inference(sat_conversion,[],[f54197]) ).
cnf(s407,plain,
( ~ spl129_101
| ~ spl129_186
| spl129_207
| ~ spl129_277
| ~ spl129_280 ),
inference(sat_conversion,[],[f54200]) ).
cnf(s408,plain,
( ~ spl129_123
| ~ spl129_130
| ~ spl129_186
| ~ spl129_277
| spl129_280 ),
inference(sat_conversion,[],[f54368]) ).
cnf(s412,plain,
( spl129_113
| ~ spl129_130
| ~ spl129_140
| ~ spl129_223
| ~ spl129_278
| ~ spl129_289 ),
inference(sat_conversion,[],[f55439]) ).
cnf(s413,plain,
( ~ spl129_130
| ~ spl129_223
| spl129_289 ),
inference(sat_conversion,[],[f55529]) ).
cnf(s420,plain,
( spl129_113
| ~ spl129_130
| ~ spl129_140
| ~ spl129_222
| ~ spl129_278
| ~ spl129_290 ),
inference(sat_conversion,[],[f56165]) ).
cnf(s424,plain,
( spl129_34
| spl129_204
| ~ spl129_295 ),
inference(sat_conversion,[],[f56325]) ).
cnf(s425,plain,
( spl129_34
| spl129_204
| ~ spl129_292
| spl129_296 ),
inference(sat_conversion,[],[f56367]) ).
cnf(s426,plain,
( ~ spl129_216
| spl129_295
| ~ spl129_296 ),
inference(sat_conversion,[],[f56659]) ).
cnf(s427,plain,
( spl129_34
| spl129_204
| spl129_216 ),
inference(sat_conversion,[],[f56677]) ).
cnf(s439,plain,
( spl129_34
| spl129_35
| ~ spl129_295 ),
inference(sat_conversion,[],[f57062]) ).
cnf(s474,plain,
( spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| ~ spl129_130
| spl129_137
| spl129_139
| spl129_223
| spl129_290 ),
inference(sat_conversion,[],[f58447]) ).
cnf(s475,plain,
( spl129_1
| spl129_3
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| ~ spl129_130
| spl129_137
| spl129_139
| spl129_290 ),
inference(sat_conversion,[],[f58448]) ).
cnf(s505,plain,
( ~ spl129_101
| ~ spl129_114
| ~ spl129_123
| spl129_129
| ~ spl129_130
| ~ spl129_186
| ~ spl129_290 ),
inference(sat_conversion,[],[f60431]) ).
cnf(s515,plain,
( ~ spl129_106
| ~ spl129_114
| ~ spl129_129
| ~ spl129_130 ),
inference(sat_conversion,[],[f65306]) ).
cnf(s520,plain,
( ~ spl129_106
| ~ spl129_114
| ~ spl129_130
| ~ spl129_140
| ~ spl129_289 ),
inference(sat_conversion,[],[f65440]) ).
cnf(s526,plain,
( ~ spl129_3
| ~ spl129_114
| spl129_129
| ~ spl129_130 ),
inference(sat_conversion,[],[f65630]) ).
cnf(s563,plain,
( ~ spl129_114
| ~ spl129_124
| spl129_129
| ~ spl129_130
| ~ spl129_140 ),
inference(sat_conversion,[],[f66788]) ).
cnf(s659,plain,
( spl129_34
| spl129_216
| spl129_332 ),
inference(sat_conversion,[],[f72301]) ).
cnf(s660,plain,
( ~ spl129_106
| ~ spl129_244
| ~ spl129_332 ),
inference(sat_conversion,[],[f72338]) ).
cnf(s661,plain,
( spl129_34
| spl129_332
| spl129_333 ),
inference(sat_conversion,[],[f72386]) ).
cnf(s662,plain,
( spl129_34
| ~ spl129_292
| spl129_296
| spl129_332 ),
inference(sat_conversion,[],[f72439]) ).
cnf(s664,plain,
( spl129_35
| ~ spl129_332 ),
inference(sat_conversion,[],[f72508]) ).
cnf(s665,plain,
( ~ spl129_106
| ~ spl129_295
| ~ spl129_333 ),
inference(sat_conversion,[],[f72839]) ).
cnf(s666,plain,
( spl129_34
| spl129_292
| spl129_332
| ~ spl129_333 ),
inference(sat_conversion,[],[f72986]) ).
cnf(s668,plain,
( spl129_34
| spl129_204
| spl129_292
| ~ spl129_333 ),
inference(sat_conversion,[],[f73099]) ).
cnf(s669,plain,
( ~ spl129_328
| ~ spl129_332
| spl129_333 ),
inference(sat_conversion,[],[f73104]) ).
cnf(s672,plain,
( spl129_34
| spl129_204
| spl129_328
| ~ spl129_332 ),
inference(sat_conversion,[],[f73120]) ).
cnf(s691,plain,
( spl129_101
| spl129_124 ),
inference(sat_conversion,[],[f76001]) ).
cnf(s709,plain,
( spl129_1
| spl129_3
| spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_137
| spl129_139
| ~ spl129_223
| spl129_287 ),
inference(sat_conversion,[],[f76733]) ).
cnf(s712,plain,
( ~ spl129_61
| ~ spl129_103
| spl129_119
| ~ spl129_124
| ~ spl129_140
| ~ spl129_223
| ~ spl129_283 ),
inference(sat_conversion,[],[f77452]) ).
cnf(s714,plain,
( spl129_61
| ~ spl129_124
| ~ spl129_223 ),
inference(sat_conversion,[],[f77555]) ).
cnf(s715,plain,
( ~ spl129_106
| ~ spl129_119
| ~ spl129_124
| ~ spl129_223 ),
inference(sat_conversion,[],[f77641]) ).
cnf(s718,plain,
( ~ spl129_283
| spl129_286
| ~ spl129_287 ),
inference(sat_conversion,[],[f78150]) ).
cnf(s723,plain,
( ~ spl129_103
| ~ spl129_140
| spl129_207
| ~ spl129_286
| ~ spl129_323 ),
inference(sat_conversion,[],[f78578]) ).
cnf(s724,plain,
( ~ spl129_131
| ~ spl129_140
| ~ spl129_286
| spl129_322
| spl129_323 ),
inference(sat_conversion,[],[f78581]) ).
cnf(s725,plain,
( spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_137
| spl129_139
| spl129_223
| spl129_322
| spl129_323 ),
inference(sat_conversion,[],[f78710]) ).
cnf(s727,plain,
( spl129_113
| ~ spl129_131
| ~ spl129_140
| ~ spl129_222
| ~ spl129_283
| ~ spl129_287
| ~ spl129_322 ),
inference(sat_conversion,[],[f79481]) ).
cnf(s733,plain,
( spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_113
| spl129_137
| spl129_139
| ~ spl129_140
| ~ spl129_222
| spl129_223
| ~ spl129_322 ),
inference(sat_conversion,[],[f79601]) ).
cnf(s734,plain,
( spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_137
| spl129_139
| ~ spl129_140
| spl129_150
| spl129_223
| ~ spl129_323 ),
inference(sat_conversion,[],[f79645]) ).
cnf(s735,plain,
( ~ spl129_1
| spl129_348
| spl129_349 ),
inference(sat_conversion,[],[f79963]) ).
cnf(s740,plain,
( ~ spl129_131
| ~ spl129_140
| ~ spl129_223
| spl129_283 ),
inference(sat_conversion,[],[f80240]) ).
cnf(s742,plain,
( ~ spl129_3
| ~ spl129_106
| ~ spl129_223 ),
inference(sat_conversion,[],[f80399]) ).
cnf(s743,plain,
( spl129_113
| ~ spl129_131
| ~ spl129_140
| ~ spl129_223
| ~ spl129_283
| ~ spl129_319 ),
inference(sat_conversion,[],[f80746]) ).
cnf(s744,plain,
( ~ spl129_1
| ~ spl129_131
| ~ spl129_140
| ~ spl129_283
| spl129_319
| ~ spl129_349 ),
inference(sat_conversion,[],[f80802]) ).
cnf(s746,plain,
( ~ spl129_1
| ~ spl129_131
| ~ spl129_140
| ~ spl129_283
| spl129_320
| ~ spl129_348 ),
inference(sat_conversion,[],[f80815]) ).
cnf(s748,plain,
( ~ spl129_103
| ~ spl129_140
| spl129_207
| ~ spl129_283
| ~ spl129_320 ),
inference(sat_conversion,[],[f80869]) ).
cnf(s749,plain,
( ~ spl129_113
| ~ spl129_114
| ~ spl129_131
| ~ spl129_140
| ~ spl129_283 ),
inference(sat_conversion,[],[f80886]) ).
cnf(s750,plain,
( ~ spl129_103
| ~ spl129_106
| ~ spl129_114
| ~ spl129_131
| ~ spl129_140
| ~ spl129_286 ),
inference(sat_conversion,[],[f86667]) ).
cnf(s751,plain,
( spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| ~ spl129_131
| spl129_137
| spl129_139
| ~ spl129_140
| spl129_223
| spl129_286 ),
inference(sat_conversion,[],[f86678]) ).
cnf(s760,plain,
( spl129_37
| spl129_112 ),
inference(rat,[],[s302,s312]) ).
cnf(s761,plain,
( spl129_40
| spl129_112 ),
inference(rat,[],[s285,s312]) ).
cnf(s763,plain,
( spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_112
| spl129_137
| spl129_222
| spl129_223 ),
inference(rat,[],[s237,s312]) ).
cnf(s769,plain,
( spl129_20
| ~ spl129_34
| ~ spl129_37
| ~ spl129_40
| ~ spl129_111
| spl129_112
| spl129_137
| spl129_150
| spl129_186
| spl129_187 ),
inference(rat,[],[s220,s312]) ).
cnf(s774,plain,
( spl129_20
| ~ spl129_111
| spl129_112
| spl129_137
| spl129_140
| spl129_150
| spl129_207 ),
inference(rat,[],[s201,s312]) ).
cnf(s776,plain,
( spl129_112
| ~ spl129_139 ),
inference(rat,[],[s199,s312]) ).
cnf(s788,plain,
~ spl129_207,
inference(rat,[],[s202,s156]) ).
cnf(s791,plain,
~ spl129_187,
inference(rat,[],[s223,s788,s153]) ).
cnf(s792,plain,
~ spl129_141,
inference(rat,[],[s203,s788,s153]) ).
cnf(s795,plain,
( ~ spl129_110
| ~ spl129_114 ),
inference(rat,[],[s149,s170]) ).
cnf(s810,plain,
( spl129_19
| spl129_112 ),
inference(rat,[],[s122,s312]) ).
cnf(s812,plain,
~ spl129_112,
inference(rat,[],[s120,s156]) ).
cnf(s813,plain,
spl129_37,
inference(rat,[],[s760,s812]) ).
cnf(s814,plain,
spl129_40,
inference(rat,[],[s761,s812]) ).
cnf(s816,plain,
~ spl129_139,
inference(rat,[],[s776,s812]) ).
cnf(s817,plain,
spl129_19,
inference(rat,[],[s810,s812]) ).
cnf(s823,plain,
~ spl129_15,
inference(rat,[],[s108,s312]) ).
cnf(s827,plain,
( spl129_20
| ~ spl129_114
| spl129_137
| spl129_138
| spl129_140 ),
inference(rat,[],[s96,s792,s816]) ).
cnf(s828,plain,
spl129_111,
inference(rat,[],[s74,s812,s312]) ).
cnf(s829,plain,
~ spl129_138,
inference(rat,[],[s261,s828]) ).
cnf(s835,plain,
( spl129_35
| spl129_34 ),
inference(rat,[],[s426,s662,s659,s666,s661,s439,s664]) ).
cnf(s836,plain,
( spl129_296
| ~ spl129_292
| spl129_34 ),
inference(rat,[],[s363,s660,s425,s662,s835,s355]) ).
cnf(s837,plain,
( ~ spl129_295
| spl129_34 ),
inference(rat,[],[s660,s363,s661,s424,s665,s835,s355]) ).
cnf(s838,plain,
( ~ spl129_332
| spl129_292
| spl129_34 ),
inference(rat,[],[s669,s668,s672,s363,s660,s835,s355]) ).
cnf(s839,plain,
( spl129_292
| spl129_34 ),
inference(rat,[],[s666,s661,s838]) ).
cnf(s840,plain,
spl129_34,
inference(rat,[],[s363,s660,s427,s659,s426,s836,s839,s837,s835,s355]) ).
cnf(s842,plain,
( spl129_113
| ~ spl129_130
| ~ spl129_124
| spl129_20
| spl129_3
| spl129_1 ),
inference(rat,[],[s391,s420,s405,s475,s375,s774,s179,s153,s813,s814,s828,s840,s816,s312,s812,s788]) ).
cnf(s843,plain,
( spl129_140
| ~ spl129_114
| spl129_20 ),
inference(rat,[],[s173,s795,s827,s829]) ).
cnf(s844,plain,
( spl129_103
| ~ spl129_124
| spl129_20
| spl129_3
| spl129_1 ),
inference(rat,[],[s843,s563,s76,s842,s89,s90]) ).
cnf(s846,plain,
( spl129_140
| spl129_20 ),
inference(rat,[],[s179,s76,s774,s843,s788,s153,s828,s812]) ).
cnf(s848,plain,
( ~ spl129_124
| ~ spl129_130
| spl129_20
| spl129_3
| spl129_1 ),
inference(rat,[],[s563,s515,s76,s842,s846,s355]) ).
cnf(s850,plain,
~ spl129_137,
inference(rat,[],[s173,s795,s76,s179]) ).
cnf(s852,plain,
( spl129_223
| spl129_113
| ~ spl129_222
| spl129_20 ),
inference(rat,[],[s725,s733,s734,s846,s813,s814,s828,s840,s816,s850,s153]) ).
cnf(s853,plain,
( ~ spl129_223
| ~ spl129_131
| ~ spl129_103
| ~ spl129_124
| ~ spl129_140 ),
inference(rat,[],[s712,s714,s715,s740,s355]) ).
cnf(s854,plain,
( ~ spl129_124
| spl129_20
| spl129_3
| spl129_1 ),
inference(rat,[],[s76,s750,s852,s751,s853,s91,s848,s844,s846,s375,s355,s813,s814,s828,s840,s850,s816,s812,s312]) ).
cnf(s855,plain,
( spl129_130
| ~ spl129_287
| ~ spl129_223
| spl129_113
| ~ spl129_222
| ~ spl129_140 ),
inference(rat,[],[s724,s723,s727,s718,s740,s90,s91,s788]) ).
cnf(s856,plain,
( spl129_113
| spl129_20
| spl129_3
| spl129_1 ),
inference(rat,[],[s408,s407,s391,s420,s475,s855,s709,s852,s846,s769,s375,s691,s85,s854,s788,s813,s814,s828,s840,s850,s816,s812,s312,s791,s153]) ).
cnf(s857,plain,
( spl129_130
| ~ spl129_113
| spl129_20 ),
inference(rat,[],[s751,s740,s750,s749,s90,s91,s846,s76,s813,s814,s828,s840,s850,s816,s355]) ).
cnf(s858,plain,
( spl129_20
| spl129_3
| spl129_1 ),
inference(rat,[],[s505,s515,s475,s857,s76,s856,s85,s691,s854,s769,s355,s813,s814,s828,s840,s850,s816,s812,s153,s791]) ).
cnf(s859,plain,
~ spl129_20,
inference(rat,[],[s234,s171,s795,s76,s230,s170,s817,s823,s812,s153,s788]) ).
cnf(s860,plain,
spl129_140,
inference(rat,[],[s774,s788,s153,s859,s828,s812,s850]) ).
cnf(s861,plain,
spl129_186,
inference(rat,[],[s769,s791,s859,s153,s840,s812,s828,s814,s813,s850]) ).
cnf(s863,plain,
( ~ spl129_114
| ~ spl129_130
| ~ spl129_3 ),
inference(rat,[],[s515,s526,s355]) ).
cnf(s864,plain,
~ spl129_3,
inference(rat,[],[s863,s857,s76,s852,s763,s742,s859,s813,s814,s828,s812,s840,s850,s355]) ).
cnf(s865,plain,
spl129_1,
inference(rat,[],[s858,s859,s864]) ).
cnf(s867,plain,
( spl129_223
| spl129_113 ),
inference(rat,[],[s852,s763,s859,s813,s814,s828,s812,s840,s850]) ).
cnf(s868,plain,
spl129_130,
inference(rat,[],[s735,s744,s746,s743,s748,s740,s867,s857,s90,s91,s865,s860,s788,s859]) ).
cnf(s870,plain,
~ spl129_277,
inference(rat,[],[s408,s407,s85,s691,s406,s868,s861,s788,s153]) ).
cnf(s871,plain,
spl129_278,
inference(rat,[],[s391,s868,s870]) ).
cnf(s872,plain,
( spl129_113
| ~ spl129_223 ),
inference(rat,[],[s413,s412,s860,s871,s868]) ).
cnf(s873,plain,
spl129_113,
inference(rat,[],[s872,s867]) ).
cnf(s874,plain,
spl129_114,
inference(rat,[],[s76,s873]) ).
cnf(s883,plain,
~ spl129_129,
inference(rat,[],[s515,s868,s355,s874]) ).
cnf(s884,plain,
~ spl129_289,
inference(rat,[],[s520,s868,s860,s355,s874]) ).
cnf(s891,plain,
~ spl129_124,
inference(rat,[],[s563,s860,s868,s874,s883]) ).
cnf(s892,plain,
~ spl129_223,
inference(rat,[],[s413,s868,s884]) ).
cnf(s894,plain,
spl129_101,
inference(rat,[],[s691,s891]) ).
cnf(s895,plain,
spl129_123,
inference(rat,[],[s85,s891]) ).
cnf(s899,plain,
spl129_290,
inference(rat,[],[s474,s859,s868,s816,s850,s840,s828,s814,s813,s892]) ).
cnf(s900,plain,
$false,
inference(rat,[],[s505,s895,s883,s868,s874,s861,s894,s899]) ).
fof(f86679,plain,
$false,
inference(avatar_sat_refutation,[],[s900]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW095+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n010.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 13:12:32 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.68/2.32 % (1915356)Will run a generic schedule for satisfiability detection.
% 14.68/2.32 % (1915364)dis+10_1_sil=32000:sp=arity:random_seed=1346193452:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.68/2.32 % (1915362)% WARNING: option uhcvi not known.
% 14.68/2.32 % (1915361)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1615843589_2999 on theBenchmark for (2999ds/0Mi)
% 14.68/2.32 % (1915362)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4121553085:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.68/2.32 % (1915363)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2063512936:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.68/2.32 % (1915365)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3524287356:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.68/2.32 % (1915367)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2619410:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.68/2.32 % (1915366)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3521429731:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.68/2.32 % (1915364)Instruction limit reached!
% 14.68/2.32 % (1915364)------------------------------
% 14.68/2.32 % (1915364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.68/2.32 % (1915364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.68/2.32 % (1915364)CaDiCaL version: 2.1.3
% 14.68/2.32 % (1915364)Termination reason: Instruction limit
% 14.68/2.32 % (1915364)Termination phase: Saturation
% 14.68/2.32 % (1915364)Time elapsed: 0.032 s
% 14.68/2.32 % (1915364)Peak memory usage: 13 MB
% 14.68/2.32 % (1915364)Instructions burned: 104 (million)
% 14.68/2.32 % (1915375)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3612669169:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.68/2.32 % TRYING [1]
% 14.68/2.32 % TRYING [2]
% 14.68/2.32 % TRYING [3]
% 14.68/2.32 % TRYING [1]
% 14.68/2.32 % TRYING [2]
% 14.68/2.32 % (1915365)Instruction limit reached!
% 14.68/2.32 % (1915365)------------------------------
% 14.68/2.32 % (1915365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.68/2.32 % (1915365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.68/2.32 % (1915365)CaDiCaL version: 2.1.3
% 14.68/2.32 % (1915365)Termination reason: Instruction limit
% 14.68/2.32 % (1915365)Termination phase: Saturation
% 14.68/2.32 % (1915365)Time elapsed: 0.054 s
% 14.68/2.32 % (1915365)Peak memory usage: 12 MB
% 14.68/2.32 % (1915365)Instructions burned: 116 (million)
% 14.68/2.32 % TRYING [3]
% 14.68/2.32 % TRYING [4]
% 14.68/2.32 % TRYING [4]
% 14.68/2.32 % (1915377)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=469968983:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 14.68/2.32 % (1915366)Instruction limit reached!
% 14.68/2.32 % (1915366)------------------------------
% 14.68/2.32 % (1915366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.68/2.32 % (1915366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.68/2.32 % (1915366)CaDiCaL version: 2.1.3
% 14.68/2.32 % (1915366)Termination reason: Instruction limit
% 14.68/2.32 % (1915366)Termination phase: Saturation
% 14.68/2.32 % (1915366)Time elapsed: 0.077 s
% 14.68/2.32 % (1915366)Peak memory usage: 14 MB
% 14.68/2.32 % (1915366)Instructions burned: 131 (million)
% 14.68/2.32 % (1915367)Instruction limit reached!
% 14.68/2.32 % (1915367)------------------------------
% 14.68/2.32 % (1915367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.68/2.32 % (1915367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.68/2.32 % (1915367)CaDiCaL version: 2.1.3
% 14.68/2.32 % (1915367)Termination reason: Instruction limit
% 14.68/2.32 % (1915367)Termination phase: Saturation
% 14.68/2.32 % (1915367)Time elapsed: 0.082 s
% 14.68/2.32 % (1915367)Peak memory usage: 15 MB
% 14.68/2.32 % (1915367)Instructions burned: 161 (million)
% 14.68/2.32 % TRYING [5]
% 14.68/2.32 % (1915379)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1231939003:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.68/2.32 % (1915380)ott-21_1_sil=16000:fs=off:random_seed=926424252:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.68/2.32 % TRYING [5]
% 14.68/2.32 % TRYING [6]
% 14.68/2.32 % (1915377)Instruction limit reached!
% 14.68/2.32 % (1915377)------------------------------
% 14.68/2.32 % (1915377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.75/2.86 % (1915377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/2.86 % (1915377)CaDiCaL version: 2.1.3
% 17.75/2.86 % (1915377)Termination reason: Instruction limit
% 17.75/2.86 % (1915377)Termination phase: Saturation
% 17.75/2.86 % (1915377)Time elapsed: 0.078 s
% 17.75/2.86 % (1915377)Peak memory usage: 14 MB
% 17.75/2.86 % (1915377)Instructions burned: 131 (million)
% 17.75/2.86 % (1915383)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=133459115:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 17.75/2.86 % TRYING [7]
% 17.75/2.86 % (1915375)Instruction limit reached!
% 17.75/2.86 % (1915375)------------------------------
% 17.75/2.86 % (1915375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.75/2.86 % (1915375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/2.86 % (1915375)CaDiCaL version: 2.1.3
% 17.75/2.86 % (1915375)Termination reason: Instruction limit
% 17.75/2.86 % (1915375)Termination phase: Finite model building constraint generation
% 17.75/2.86 % (1915375)Time elapsed: 0.143 s
% 17.75/2.86 % (1915375)Peak memory usage: 23 MB
% 17.75/2.86 % (1915375)Instructions burned: 723 (million)
% 17.75/2.86 % TRYING [6]
% 17.75/2.86 % (1915385)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3576216086:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 17.75/2.86 % (1915380)Instruction limit reached!
% 17.75/2.86 % (1915380)------------------------------
% 17.75/2.86 % (1915380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.75/2.86 % (1915380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/2.86 % (1915380)CaDiCaL version: 2.1.3
% 17.75/2.86 % (1915380)Termination reason: Instruction limit
% 17.75/2.86 % (1915380)Termination phase: Saturation
% 17.75/2.86 % (1915380)Time elapsed: 0.090 s
% 17.75/2.86 % (1915380)Peak memory usage: 14 MB
% 17.75/2.86 % (1915380)Instructions burned: 181 (million)
% 17.75/2.86 % TRYING [1]
% 17.75/2.86 % TRYING [2]
% 17.75/2.86 % (1915387)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2595230698:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 17.75/2.86 % TRYING [3]
% 17.75/2.86 % TRYING [4]
% 17.75/2.86 % TRYING [5]
% 17.75/2.86 % TRYING [7]
% 17.75/2.86 % TRYING [6]
% 17.75/2.86 % (1915385)Instruction limit reached!
% 17.75/2.86 % (1915385)------------------------------
% 17.75/2.86 % (1915385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.75/2.86 % (1915385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/2.86 % (1915385)CaDiCaL version: 2.1.3
% 17.75/2.86 % (1915385)Termination reason: Instruction limit
% 17.75/2.86 % (1915385)Termination phase: Finite model building SAT solving
% 17.75/2.86 % (1915385)Time elapsed: 0.177 s
% 17.75/2.86 % (1915385)Peak memory usage: 22 MB
% 17.75/2.86 % (1915385)Instructions burned: 867 (million)
% 17.75/2.86 % (1915389)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4092706948:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 17.75/2.86 % TRYING [14]
% 17.75/2.86 % (1915379)Instruction limit reached!
% 17.75/2.86 % (1915379)------------------------------
% 17.75/2.86 % (1915379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.75/2.86 % (1915379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/2.86 % (1915379)CaDiCaL version: 2.1.3
% 17.75/2.86 % (1915379)Termination reason: Instruction limit
% 17.75/2.86 % (1915379)Termination phase: Saturation
% 17.75/2.86 % (1915379)Time elapsed: 0.378 s
% 17.75/2.86 % (1915379)Peak memory usage: 19 MB
% 17.75/2.86 % (1915379)Instructions burned: 685 (million)
% 17.75/2.86 % (1915383)Instruction limit reached!
% 17.75/2.86 % (1915383)------------------------------
% 17.75/2.86 % (1915383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.75/2.86 % (1915383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/2.86 % (1915383)CaDiCaL version: 2.1.3
% 17.75/2.86 % (1915383)Termination reason: Instruction limit
% 17.75/2.86 % (1915383)Termination phase: Saturation
% 17.75/2.86 % (1915383)Time elapsed: 0.310 s
% 17.75/2.86 % (1915383)Peak memory usage: 15 MB
% 17.75/2.86 % (1915383)Instructions burned: 477 (million)
% 17.75/2.86 % (1915391)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1476713461:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 17.75/2.86 % (1915392)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=995319195:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 17.75/2.86 % TRYING [8]
% 17.75/2.86 % (1915389)Instruction limit reached!
% 17.75/2.86 % (1915389)------------------------------
% 17.75/2.86 % (1915389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.75/2.86 % (1915389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/2.86 % (1915389)CaDiCaL version: 2.1.3
% 17.75/2.86 % (1915389)Termination reason: Instruction limit
% 17.75/2.86 % (1915389)Termination phase: Finite model building constraint generation
% 17.75/2.86 % (1915389)Time elapsed: 0.173 s
% 17.75/2.86 % (1915389)Peak memory usage: 66 MB
% 17.75/2.86 % (1915389)Instructions burned: 892 (million)
% 17.75/2.86 % (1915395)fmb+10_1_sil=64000:random_seed=1502522122:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 17.75/2.86 % TRYING [1]
% 17.75/2.86 % TRYING [2]
% 17.75/2.86 % TRYING [3]
% 17.75/2.86 % TRYING [4]
% 17.75/2.86 % TRYING [5]
% 17.75/2.86 % TRYING [6]
% 17.75/2.86 % TRYING [7]
% 17.75/2.86 % TRYING [9]
% 17.75/2.86 % (1915387)Instruction limit reached!
% 17.75/2.86 % (1915387)------------------------------
% 17.75/2.86 % (1915387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.75/2.86 % (1915387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/2.86 % (1915387)CaDiCaL version: 2.1.3
% 17.75/2.86 % (1915387)Termination reason: Instruction limit
% 17.75/2.86 % (1915387)Termination phase: Saturation
% 17.75/2.86 % (1915387)Time elapsed: 0.652 s
% 17.75/2.86 % (1915387)Peak memory usage: 23 MB
% 17.75/2.86 % (1915387)Instructions burned: 1179 (million)
% 17.75/2.86 % (1915397)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2689183771:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 17.75/2.86 % TRYING [8]
% 17.75/2.86 % (1915391)Instruction limit reached!
% 17.75/2.86 % (1915391)------------------------------
% 17.75/2.86 % (1915391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.75/2.86 % (1915391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/2.86 % (1915391)CaDiCaL version: 2.1.3
% 17.75/2.86 % (1915391)Termination reason: Instruction limit
% 17.75/2.86 % (1915391)Termination phase: Saturation
% 17.75/2.86 % (1915391)Time elapsed: 0.411 s
% 17.75/2.86 % (1915391)Peak memory usage: 19 MB
% 17.75/2.86 % (1915391)Instructions burned: 693 (million)
% 17.75/2.86 % TRYING [20]
% 17.75/2.86 % (1915399)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2356219980:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 17.75/2.86 % TRYING [8]
% 17.75/2.86 % (1915392)Instruction limit reached!
% 17.75/2.86 % (1915392)------------------------------
% 17.75/2.86 % (1915392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.75/2.86 % (1915392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/2.86 % (1915392)CaDiCaL version: 2.1.3
% 17.75/2.86 % (1915392)Termination reason: Instruction limit
% 17.75/2.86 % (1915392)Termination phase: Saturation
% 17.75/2.86 % (1915392)Time elapsed: 0.485 s
% 17.75/2.86 % (1915392)Peak memory usage: 21 MB
% 17.75/2.86 % (1915392)Instructions burned: 879 (million)
% 17.75/2.86 % (1915401)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2331439680:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 17.75/2.86 % TRYING [9]
% 17.75/2.86 % TRYING [10]
% 17.75/2.86 % TRYING [9]
% 17.75/2.86 % (1915399)Instruction limit reached!
% 17.75/2.86 % (1915399)------------------------------
% 17.75/2.86 % (1915399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.75/2.86 % (1915399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/2.86 % (1915399)CaDiCaL version: 2.1.3
% 17.75/2.86 % (1915399)Termination reason: Instruction limit
% 17.75/2.86 % (1915399)Termination phase: Finite model building constraint generation
% 17.75/2.86 % (1915399)Time elapsed: 0.349 s
% 17.75/2.86 % (1915399)Peak memory usage: 40 MB
% 17.75/2.86 % (1915399)Instructions burned: 921 (million)
% 17.75/2.86 % (1915403)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3408201974:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 17.75/2.86 % TRYING [10]
% 17.75/2.86 % TRYING [11]
% 17.75/2.86 % TRYING [11]
% 17.75/2.86 % (1915403)Instruction limit reached!
% 17.75/2.86 % (1915403)------------------------------
% 17.75/2.86 % (1915403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.75/2.86 % (1915403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/2.86 % (1915403)CaDiCaL version: 2.1.3
% 17.75/2.86 % (1915403)Termination reason: Instruction limit
% 17.75/2.86 % (1915403)Termination phase: Saturation
% 17.75/2.86 % (1915403)Time elapsed: 0.749 s
% 17.75/2.86 % (1915403)Peak memory usage: 27 MB
% 17.75/2.86 % (1915403)Instructions burned: 1472 (million)
% 17.75/2.86 % (1915405)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1808647196:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 17.75/2.86 % TRYING [77]
% 17.75/2.86 % TRYING [12]
% 17.75/2.86 % (1915401) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1915356-1915401"...
% 17.75/2.86 % (1915401)...printing done.
% 17.75/2.86 % (1915401)Refutation found. Thanks to Tanya!
% 17.75/2.86 % SZS status Theorem for theBenchmark
% 17.75/2.86 % SZS output start Proof for theBenchmark
% See solution above
% 17.75/2.88 % (1915401)------------------------------
% 17.75/2.88 % (1915401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.75/2.88 % (1915401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/2.88 % (1915401)CaDiCaL version: 2.1.3
% 17.75/2.88 % (1915401)Termination reason: Refutation
% 17.75/2.88 % (1915401)Time elapsed: 1.537 s
% 17.75/2.88 % (1915401)Peak memory usage: 28 MB
% 17.75/2.88 % (1915401)Instructions burned: 2684 (million)
% 17.75/2.88 % (1915356)Success in time 2.634 s
% 17.75/2.88 % Vampire exiting
%------------------------------------------------------------------------------