%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWW095+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n017.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 : Fri Sep 25 03:29:11 PM UTC 2026
% Result : Theorem 46.00s 7.41s
% Output : CNFRefutation 46.00s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f171ERROR: Could not build tree for root c_156609ERROR: MakeTreeStats fails)
% 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(f16,axiom,
! [X0,X1,X2] :
( v__1(X0,X2,X2)
| ~ v__1(X1,X2,X2)
| ~ v__1(X0,X1,X1)
| ~ ( object(X2)
& object(X1)
& object(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp_tptp_2) ).
fof(f17,axiom,
! [X0,X1,X2,X3] :
( ( v__1(X1,X0,X3)
& v__1(X1,X2,X0) )
| ~ v__1(X2,X0,X3)
| ~ v__1(X1,X2,X3)
| ~ ( object(X3)
& object(X2)
& object(X1)
& object(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp_tptp_3) ).
fof(f18,axiom,
! [X0,X1,X2,X3] :
( ( v__1(X0,X2,X3)
& v__1(X1,X0,X3) )
| ~ v__1(X1,X0,X2)
| ~ v__1(X1,X2,X3)
| ~ ( object(X3)
& object(X2)
& object(X1)
& object(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp_tptp_4) ).
fof(f19,axiom,
! [X0,X1,X2] :
( 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) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp_tptp_5) ).
fof(f20,axiom,
! [X0,X1,X2] :
( ( v__1(X1,X2,X2)
& v__1(X0,X1,X1) )
| ~ v__1(X0,X1,X2)
| ~ ( object(X2)
& object(X1)
& object(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp_tptp_6) ).
fof(f21,axiom,
! [X0] :
( v__1(X0,X0,X0)
| ~ object(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp_tptp_7) ).
fof(f22,axiom,
! [X0,X1] :
( X0 = X1
| ~ v__1(X0,X1,X0)
| ~ ( object(X1)
& object(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp_tptp_8) ).
fof(f23,axiom,
! [X0,X1] :
( X0 = X1
| ~ v__1(X0,X1,X1)
| X0 != node_next(X0)
| ~ ( object(X1)
& object(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp_tptp_9) ).
fof(f25,axiom,
! [X0,X1] :
( ! [X2] :
( v__1(X0,X2,X1)
| X2 != node_next(X0)
| ~ object(X2) )
| X0 = X1
| ~ v__1(X0,X1,X1)
| ~ ( object(X1)
& object(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp_tptp_11) ).
fof(f26,axiom,
prev_2 != null,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp_tptp_12) ).
fof(f31,axiom,
( ( v__1(sortedList_first,prev_2,prev_2)
& prev_2 != null )
| prev_2 = null ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp_tptp_17) ).
fof(f32,axiom,
( ( v__1(sortedList_first,nn,nn)
& nn != null )
| nn = null ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp_tptp_18) ).
fof(f34,axiom,
( nn = node_next(prev_2)
| prev_2 = null ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp_tptp_20) ).
fof(f44,axiom,
! [X0,X1] :
( ( ! [X5] :
( X5 != node_key(X1)
| X5 != node_key(X0)
| ~ integer(X5) )
& ! [X3,X4] :
( lteq(X3,X4)
| X4 != node_key(X1)
| X3 != node_key(X0)
| ~ ( integer(X4)
& integer(X3) ) ) )
| X1 = null
| ! [X2] :
( X2 != node_next(X0)
| ~ v__1(X2,X1,X1)
| ~ object(X2) )
| X0 = null
| ~ v__1(sortedList_first,X0,X0)
| ~ ( object(X1)
& object(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp_tptp_30) ).
fof(f46,axiom,
( ! [X0] :
( sortedList_first != node_next(X0)
| ~ object(X0) )
| sortedList_first = null ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp_tptp_32) ).
fof(f47,axiom,
nn != null,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp_tptp_33) ).
fof(f57,axiom,
null = node_next(null),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp_tptp_43) ).
fof(f69,plain,
! [X0,X1,X2] :
( v__1(X0,X2,X2)
| ~ v__1(X1,X2,X2)
| ~ v__1(X0,X1,X1)
| ~ object(X2)
| ~ object(X1)
| ~ object(X0) ),
inference(ennf_transformation,[],[f16]) ).
fof(f70,plain,
! [X0,X1,X2] :
( v__1(X0,X2,X2)
| ~ v__1(X1,X2,X2)
| ~ v__1(X0,X1,X1)
| ~ object(X2)
| ~ object(X1)
| ~ object(X0) ),
inference(flattening,[],[f69]) ).
fof(f71,plain,
! [X0,X1,X2,X3] :
( ( v__1(X1,X0,X3)
& v__1(X1,X2,X0) )
| ~ v__1(X2,X0,X3)
| ~ v__1(X1,X2,X3)
| ~ object(X3)
| ~ object(X2)
| ~ object(X1)
| ~ object(X0) ),
inference(ennf_transformation,[],[f17]) ).
fof(f72,plain,
! [X0,X1,X2,X3] :
( ( v__1(X1,X0,X3)
& v__1(X1,X2,X0) )
| ~ v__1(X2,X0,X3)
| ~ v__1(X1,X2,X3)
| ~ object(X3)
| ~ object(X2)
| ~ object(X1)
| ~ object(X0) ),
inference(flattening,[],[f71]) ).
fof(f73,plain,
! [X0,X1,X2,X3] :
( ( v__1(X0,X2,X3)
& v__1(X1,X0,X3) )
| ~ v__1(X1,X0,X2)
| ~ v__1(X1,X2,X3)
| ~ object(X3)
| ~ object(X2)
| ~ object(X1)
| ~ object(X0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f74,plain,
! [X0,X1,X2,X3] :
( ( v__1(X0,X2,X3)
& v__1(X1,X0,X3) )
| ~ v__1(X1,X0,X2)
| ~ v__1(X1,X2,X3)
| ~ object(X3)
| ~ object(X2)
| ~ object(X1)
| ~ object(X0) ),
inference(flattening,[],[f73]) ).
fof(f75,plain,
! [X0,X1,X2] :
( 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(ennf_transformation,[],[f19]) ).
fof(f76,plain,
! [X0,X1,X2] :
( 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(flattening,[],[f75]) ).
fof(f77,plain,
! [X0,X1,X2] :
( ( v__1(X1,X2,X2)
& v__1(X0,X1,X1) )
| ~ v__1(X0,X1,X2)
| ~ object(X2)
| ~ object(X1)
| ~ object(X0) ),
inference(ennf_transformation,[],[f20]) ).
fof(f78,plain,
! [X0,X1,X2] :
( ( v__1(X1,X2,X2)
& v__1(X0,X1,X1) )
| ~ v__1(X0,X1,X2)
| ~ object(X2)
| ~ object(X1)
| ~ object(X0) ),
inference(flattening,[],[f77]) ).
fof(f79,plain,
! [X0,X1] :
( X0 = X1
| ~ v__1(X0,X1,X0)
| ~ object(X1)
| ~ object(X0) ),
inference(ennf_transformation,[],[f22]) ).
fof(f80,plain,
! [X0,X1] :
( X0 = X1
| ~ v__1(X0,X1,X0)
| ~ object(X1)
| ~ object(X0) ),
inference(flattening,[],[f79]) ).
fof(f81,plain,
! [X0,X1] :
( X0 = X1
| ~ v__1(X0,X1,X1)
| X0 != node_next(X0)
| ~ object(X1)
| ~ object(X0) ),
inference(ennf_transformation,[],[f23]) ).
fof(f82,plain,
! [X0,X1] :
( X0 = X1
| ~ v__1(X0,X1,X1)
| X0 != node_next(X0)
| ~ object(X1)
| ~ object(X0) ),
inference(flattening,[],[f81]) ).
fof(f85,plain,
! [X0,X1] :
( ! [X2] :
( v__1(X0,X2,X1)
| X2 != node_next(X0)
| ~ object(X2) )
| X0 = X1
| ~ v__1(X0,X1,X1)
| ~ object(X1)
| ~ object(X0) ),
inference(ennf_transformation,[],[f25]) ).
fof(f86,plain,
! [X0,X1] :
( ! [X2] :
( v__1(X0,X2,X1)
| X2 != node_next(X0)
| ~ object(X2) )
| X0 = X1
| ~ v__1(X0,X1,X1)
| ~ object(X1)
| ~ object(X0) ),
inference(flattening,[],[f85]) ).
fof(f87,plain,
! [X0,X1] :
( ( ! [X5] :
( X5 != node_key(X1)
| X5 != node_key(X0)
| ~ integer(X5) )
& ! [X3,X4] :
( lteq(X3,X4)
| X4 != node_key(X1)
| X3 != node_key(X0)
| ~ integer(X4)
| ~ integer(X3) ) )
| X1 = null
| ! [X2] :
( X2 != node_next(X0)
| ~ v__1(X2,X1,X1)
| ~ object(X2) )
| X0 = null
| ~ v__1(sortedList_first,X0,X0)
| ~ object(X1)
| ~ object(X0) ),
inference(ennf_transformation,[],[f44]) ).
fof(f88,plain,
! [X0,X1] :
( ( ! [X5] :
( X5 != node_key(X1)
| X5 != node_key(X0)
| ~ integer(X5) )
& ! [X3,X4] :
( lteq(X3,X4)
| X4 != node_key(X1)
| X3 != node_key(X0)
| ~ integer(X4)
| ~ integer(X3) ) )
| X1 = null
| ! [X2] :
( X2 != node_next(X0)
| ~ v__1(X2,X1,X1)
| ~ object(X2) )
| X0 = null
| ~ v__1(sortedList_first,X0,X0)
| ~ object(X1)
| ~ object(X0) ),
inference(flattening,[],[f87]) ).
fof(f174,plain,
! [X0] :
( ~ sP77(X0)
| ( sP34(X0)
& sP35(X0)
& ( sP31(X0)
| sP32(X0)
| sP33(X0)
| ( ( ( ~ v__1(sortedList_first,nn,nn)
& v__1(sortedList_first,X0,X0) )
| v__1(sortedList_first,X0,nn) )
& v__1(sortedList_first,prev_2,X0) ) )
& prev_2 != X0 ) ),
inference(nnf_transformation,[],[f171]) ).
fof(f175,plain,
! [X0] :
( ~ sP76(X0)
| ( sP66(X0)
& ( sP57(X0)
| sP58(X0)
| ( ( ( ~ v__1(sortedList_first,nn,nn)
& v__1(sortedList_first,prev_2,prev_2) )
| v__1(sortedList_first,prev_2,nn) )
& v__1(sortedList_first,X0,prev_2) ) )
& ( sP63(X0)
| sP64(X0)
| sP65(X0)
| ( ( ( ~ v__1(sortedList_first,nn,nn)
& v__1(sortedList_first,X0,X0) )
| v__1(sortedList_first,X0,nn) )
& v__1(sortedList_first,prev_2,X0) ) )
& prev_2 != X0 ) ),
inference(nnf_transformation,[],[f170]) ).
fof(f176,plain,
! [X0] :
( ~ sP75(X0)
| ( ( ( ~ v__1(null,nn,nn)
& v__1(null,X0,X0) )
| v__1(null,X0,nn) )
& v__1(sortedList_first,X0,nn)
& ( ( ~ v__1(sortedList_first,X0,X0)
& v__1(sortedList_first,nn,nn) )
| v__1(sortedList_first,nn,X0) )
& nn != X0 ) ),
inference(nnf_transformation,[],[f169]) ).
fof(f177,plain,
! [X0] :
( ~ sP74(X0)
| ( ( ( ~ v__1(null,nn,nn)
& v__1(null,X0,X0) )
| v__1(null,X0,nn) )
& v__1(null,X0,X0)
& ( ( ~ v__1(sortedList_first,X0,X0)
& v__1(sortedList_first,nn,nn) )
| v__1(sortedList_first,nn,X0) )
& nn != X0 ) ),
inference(nnf_transformation,[],[f168]) ).
fof(f178,plain,
! [X0] :
( ~ sP73(X0)
| ( ( ( ~ v__1(null,nn,nn)
& v__1(null,prev_2,prev_2) )
| v__1(null,prev_2,nn) )
& v__1(sortedList_first,X0,nn)
& ( ( ~ v__1(sortedList_first,prev_2,prev_2)
& v__1(sortedList_first,nn,nn) )
| v__1(sortedList_first,nn,prev_2) )
& nn != prev_2 ) ),
inference(nnf_transformation,[],[f167]) ).
fof(f179,plain,
! [X0] :
( ~ sP72(X0)
| ( ( ( ~ v__1(null,nn,nn)
& v__1(null,prev_2,prev_2) )
| v__1(null,prev_2,nn) )
& v__1(null,X0,prev_2)
& ( ( ~ v__1(sortedList_first,prev_2,prev_2)
& v__1(sortedList_first,nn,nn) )
| v__1(sortedList_first,nn,prev_2) )
& nn != prev_2 ) ),
inference(nnf_transformation,[],[f166]) ).
fof(f180,plain,
! [X0] :
( ~ sP71(X0)
| ( sP69
& sP70
& ( ( ( v__1(sortedList_first,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) )
& ( sP67(X0)
| sP68(X0)
| ( ( ( ~ v__1(sortedList_first,nn,nn)
& v__1(sortedList_first,X0,X0) )
| v__1(sortedList_first,X0,nn) )
& v__1(sortedList_first,X0,X0) ) ) ) ),
inference(nnf_transformation,[],[f165]) ).
fof(f181,plain,
( ~ sP70
| ( ( v__1(sortedList_first,prev_2,prev_2)
| ~ v__1(sortedList_first,nn,nn) )
& ~ v__1(sortedList_first,nn,prev_2) )
| ( ( v__1(null,nn,nn)
| ~ v__1(null,prev_2,prev_2) )
& ~ v__1(null,prev_2,nn) )
| ~ v__1(sortedList_first,prev_2,nn)
| nn = prev_2 ),
inference(nnf_transformation,[],[f164]) ).
fof(f187,plain,
! [X0] :
( ~ sP65(X0)
| ( ( ( ~ v__1(null,nn,nn)
& v__1(null,X0,X0) )
| v__1(null,X0,nn) )
& v__1(sortedList_first,prev_2,nn)
& ( ( ~ v__1(sortedList_first,X0,X0)
& v__1(sortedList_first,nn,nn) )
| v__1(sortedList_first,nn,X0) )
& nn != X0 ) ),
inference(nnf_transformation,[],[f159]) ).
fof(f188,plain,
! [X0] :
( ~ sP64(X0)
| ( ( ( ~ v__1(null,nn,nn)
& v__1(null,X0,X0) )
| v__1(null,X0,nn) )
& v__1(null,prev_2,X0)
& ( ( ~ v__1(sortedList_first,X0,X0)
& v__1(sortedList_first,nn,nn) )
| v__1(sortedList_first,nn,X0) )
& nn != X0 ) ),
inference(nnf_transformation,[],[f158]) ).
fof(f189,plain,
! [X0] :
( ~ sP63(X0)
| ( sP61(X0)
& sP62(X0)
& ( ( ( v__1(sortedList_first,nn,nn)
| ~ v__1(sortedList_first,X0,X0) )
& ~ v__1(sortedList_first,X0,nn) )
| ~ v__1(sortedList_first,X0,X0) )
& ( sP59
| sP60
| ( ( ( ~ v__1(sortedList_first,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) ) ) ) ),
inference(nnf_transformation,[],[f157]) ).
fof(f192,plain,
( ~ sP60
| ( ( ( ~ v__1(null,nn,nn)
& v__1(null,prev_2,prev_2) )
| v__1(null,prev_2,nn) )
& v__1(sortedList_first,prev_2,nn)
& ( ( ~ v__1(sortedList_first,prev_2,prev_2)
& v__1(sortedList_first,nn,nn) )
| v__1(sortedList_first,nn,prev_2) )
& nn != prev_2 ) ),
inference(nnf_transformation,[],[f154]) ).
fof(f193,plain,
( ~ sP59
| ( ( ( ~ v__1(null,nn,nn)
& v__1(null,prev_2,prev_2) )
| v__1(null,prev_2,nn) )
& v__1(null,prev_2,prev_2)
& ( ( ~ v__1(sortedList_first,prev_2,prev_2)
& v__1(sortedList_first,nn,nn) )
| v__1(sortedList_first,nn,prev_2) )
& nn != prev_2 ) ),
inference(nnf_transformation,[],[f153]) ).
fof(f194,plain,
! [X0] :
( ~ sP58(X0)
| ( ( ( ~ v__1(null,nn,nn)
& v__1(null,prev_2,prev_2) )
| v__1(null,prev_2,nn) )
& v__1(sortedList_first,X0,nn)
& ( ( ~ v__1(sortedList_first,prev_2,prev_2)
& v__1(sortedList_first,nn,nn) )
| v__1(sortedList_first,nn,prev_2) )
& nn != prev_2 ) ),
inference(nnf_transformation,[],[f152]) ).
fof(f195,plain,
! [X0] :
( ~ sP57(X0)
| ( ( ( ~ v__1(null,nn,nn)
& v__1(null,prev_2,prev_2) )
| v__1(null,prev_2,nn) )
& v__1(null,X0,prev_2)
& ( ( ~ v__1(sortedList_first,prev_2,prev_2)
& v__1(sortedList_first,nn,nn) )
| v__1(sortedList_first,nn,prev_2) )
& nn != prev_2 ) ),
inference(nnf_transformation,[],[f151]) ).
fof(f259,plain,
! [X0] :
( ~ sP35(X0)
| sP25(X0)
| sP26(X0)
| ( ( sP24(X0)
| ? [X35] :
( node_next(nn) = X35
& v__1(X35,X0,nn)
& object(X35) ) )
& ? [X34] :
( node_next(nn) = X34
& v__1(X34,X0,X0)
& object(X34) ) ) ),
inference(nnf_transformation,[],[f129]) ).
fof(f260,plain,
! [X0] :
( ~ sP35(X0)
| sP25(X0)
| sP26(X0)
| ( ( sP24(X0)
| ? [X2] :
( node_next(nn) = X2
& v__1(X2,X0,nn)
& object(X2) ) )
& ? [X1] :
( node_next(nn) = X1
& v__1(X1,X0,X0)
& object(X1) ) ) ),
inference(rectify,[],[f259]) ).
fof(f261,plain,
! [X0] :
( ~ sP35(X0)
| sP25(X0)
| sP26(X0)
| ( ( sP24(X0)
| ( node_next(nn) = sK114(X0)
& v__1(sK114(X0),X0,nn)
& object(sK114(X0)) ) )
& node_next(nn) = sK113(X0)
& v__1(sK113(X0),X0,X0)
& object(sK113(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK113,sK114]),skolemize(X1,sK113(X0)),skolemize(X2,sK114(X0))],[f260]) ).
fof(f265,plain,
! [X0] :
( ~ sP33(X0)
| ( ( ( ~ v__1(null,nn,nn)
& v__1(null,X0,X0) )
| v__1(null,X0,nn) )
& v__1(sortedList_first,prev_2,nn)
& ( ( ~ v__1(sortedList_first,X0,X0)
& v__1(sortedList_first,nn,nn) )
| v__1(sortedList_first,nn,X0) )
& nn != X0 ) ),
inference(nnf_transformation,[],[f127]) ).
fof(f266,plain,
! [X0] :
( ~ sP32(X0)
| ( ( ( ~ v__1(null,nn,nn)
& v__1(null,X0,X0) )
| v__1(null,X0,nn) )
& v__1(null,prev_2,X0)
& ( ( ~ v__1(sortedList_first,X0,X0)
& v__1(sortedList_first,nn,nn) )
| v__1(sortedList_first,nn,X0) )
& nn != X0 ) ),
inference(nnf_transformation,[],[f126]) ).
fof(f267,plain,
! [X0] :
( ~ sP31(X0)
| ( sP29(X0)
& sP30(X0)
& ( ( ( v__1(sortedList_first,nn,nn)
| ~ v__1(sortedList_first,X0,X0) )
& ~ v__1(sortedList_first,X0,nn) )
| ~ v__1(sortedList_first,X0,X0) )
& ( sP27
| sP28
| ( ( ( ~ v__1(sortedList_first,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) ) ) ) ),
inference(nnf_transformation,[],[f125]) ).
fof(f272,plain,
! [X0] :
( ~ sP26(X0)
| ( ( ( ~ v__1(null,nn,nn)
& v__1(null,X0,X0) )
| v__1(null,X0,nn) )
& sP23(X0)
& ( sP22(X0)
| ? [X38] :
( node_next(nn) = X38
& v__1(X38,nn,X0)
& object(X38) ) )
& nn != X0 ) ),
inference(nnf_transformation,[],[f120]) ).
fof(f273,plain,
! [X0] :
( ~ sP26(X0)
| ( ( ( ~ v__1(null,nn,nn)
& v__1(null,X0,X0) )
| v__1(null,X0,nn) )
& sP23(X0)
& ( sP22(X0)
| ? [X1] :
( node_next(nn) = X1
& v__1(X1,nn,X0)
& object(X1) ) )
& nn != X0 ) ),
inference(rectify,[],[f272]) ).
fof(f274,plain,
! [X0] :
( ~ sP26(X0)
| ( ( ( ~ v__1(null,nn,nn)
& v__1(null,X0,X0) )
| v__1(null,X0,nn) )
& sP23(X0)
& ( sP22(X0)
| ( node_next(nn) = sK117(X0)
& v__1(sK117(X0),nn,X0)
& object(sK117(X0)) ) )
& nn != X0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK117]),skolemize(X1,sK117(X0))],[f273]) ).
fof(f275,plain,
! [X0] :
( ~ sP25(X0)
| ( ( ( ~ v__1(null,nn,nn)
& v__1(null,X0,X0) )
| v__1(null,X0,nn) )
& v__1(null,X0,X0)
& ( sP21(X0)
| ? [X42] :
( node_next(nn) = X42
& v__1(X42,nn,X0)
& object(X42) ) )
& nn != X0 ) ),
inference(nnf_transformation,[],[f119]) ).
fof(f276,plain,
! [X0] :
( ~ sP25(X0)
| ( ( ( ~ v__1(null,nn,nn)
& v__1(null,X0,X0) )
| v__1(null,X0,nn) )
& v__1(null,X0,X0)
& ( sP21(X0)
| ? [X1] :
( node_next(nn) = X1
& v__1(X1,nn,X0)
& object(X1) ) )
& nn != X0 ) ),
inference(rectify,[],[f275]) ).
fof(f277,plain,
! [X0] :
( ~ sP25(X0)
| ( ( ( ~ v__1(null,nn,nn)
& v__1(null,X0,X0) )
| v__1(null,X0,nn) )
& v__1(null,X0,X0)
& ( sP21(X0)
| ( node_next(nn) = sK118(X0)
& v__1(sK118(X0),nn,X0)
& object(sK118(X0)) ) )
& nn != X0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK118]),skolemize(X1,sK118(X0))],[f276]) ).
fof(f281,plain,
! [X0] :
( ~ sP23(X0)
| ? [X41] :
( node_next(nn) = X41
& v__1(X41,X0,nn)
& object(X41) ) ),
inference(nnf_transformation,[],[f117]) ).
fof(f282,plain,
! [X0] :
( ~ sP23(X0)
| ? [X1] :
( node_next(nn) = X1
& v__1(X1,X0,nn)
& object(X1) ) ),
inference(rectify,[],[f281]) ).
fof(f283,plain,
! [X0] :
( ~ sP23(X0)
| ( node_next(nn) = sK121(X0)
& v__1(sK121(X0),X0,nn)
& object(sK121(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK121]),skolemize(X1,sK121(X0))],[f282]) ).
fof(f353,plain,
( ( nn = sK157
| ~ v__1(sortedList_first,sK157,sK157)
| null = sK157 )
& ( sP77(sK157)
| sP76(sK157)
| ( ( sP71(sK157)
| sP72(sK157)
| sP73(sK157)
| ( ( ( ~ v__1(sortedList_first,nn,nn)
& v__1(sortedList_first,prev_2,prev_2) )
| v__1(sortedList_first,prev_2,nn) )
& v__1(sortedList_first,sK157,prev_2) ) )
& ( sP74(sK157)
| sP75(sK157)
| ( ( ( ~ v__1(sortedList_first,nn,nn)
& v__1(sortedList_first,sK157,sK157) )
| v__1(sortedList_first,sK157,nn) )
& v__1(sortedList_first,sK157,sK157) ) ) ) )
& null != sK157
& object(sK157) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK157]),skolemize(X0,sK157)],[f172]) ).
fof(f361,plain,
object(nn),
inference(cnf_transformation,[],[f6]) ).
fof(f363,plain,
object(prev_2),
inference(cnf_transformation,[],[f8]) ).
fof(f365,plain,
! [X0] : integer(node_key(X0)),
inference(cnf_transformation,[],[f10]) ).
fof(f366,plain,
object(null),
inference(cnf_transformation,[],[f11]) ).
fof(f368,plain,
object(sortedList_first),
inference(cnf_transformation,[],[f13]) ).
fof(f369,plain,
! [X0] : object(node_next(X0)),
inference(cnf_transformation,[],[f14]) ).
fof(f371,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(f372,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(f373,plain,
! [X2,X3,X0,X1] :
( v__1(X1,X2,X0)
| ~ v__1(X2,X0,X3)
| ~ v__1(X1,X2,X3)
| ~ object(X3)
| ~ object(X2)
| ~ object(X1)
| ~ object(X0) ),
inference(cnf_transformation,[],[f72]) ).
fof(f374,plain,
! [X2,X3,X0,X1] :
( v__1(X0,X2,X3)
| ~ v__1(X1,X0,X2)
| ~ v__1(X1,X2,X3)
| ~ object(X3)
| ~ object(X2)
| ~ object(X1)
| ~ object(X0) ),
inference(cnf_transformation,[],[f74]) ).
fof(f376,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(f377,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(f378,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(f379,plain,
! [X0] :
( v__1(X0,X0,X0)
| ~ object(X0) ),
inference(cnf_transformation,[],[f21]) ).
fof(f380,plain,
! [X0,X1] :
( X0 = X1
| ~ v__1(X0,X1,X0)
| ~ object(X1)
| ~ object(X0) ),
inference(cnf_transformation,[],[f80]) ).
fof(f381,plain,
! [X0,X1] :
( X0 = X1
| ~ v__1(X0,X1,X1)
| node_next(X0) != X0
| ~ object(X1)
| ~ object(X0) ),
inference(cnf_transformation,[],[f82]) ).
fof(f383,plain,
! [X2,X0,X1] :
( v__1(X0,X2,X1)
| node_next(X0) != X2
| ~ object(X2)
| X0 = X1
| ~ v__1(X0,X1,X1)
| ~ object(X1)
| ~ object(X0) ),
inference(cnf_transformation,[],[f86]) ).
fof(f384,plain,
prev_2 != null,
inference(cnf_transformation,[],[f26]) ).
fof(f393,plain,
( v__1(sortedList_first,prev_2,prev_2)
| prev_2 = null ),
inference(cnf_transformation,[],[f31]) ).
fof(f395,plain,
( v__1(sortedList_first,nn,nn)
| nn = null ),
inference(cnf_transformation,[],[f32]) ).
fof(f398,plain,
( nn = node_next(prev_2)
| prev_2 = null ),
inference(cnf_transformation,[],[f34]) ).
fof(f408,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(f412,plain,
! [X0] :
( sortedList_first != node_next(X0)
| ~ object(X0)
| null = sortedList_first ),
inference(cnf_transformation,[],[f46]) ).
fof(f413,plain,
nn != null,
inference(cnf_transformation,[],[f47]) ).
fof(f435,plain,
null = node_next(null),
inference(cnf_transformation,[],[f57]) ).
fof(f438,plain,
! [X0] :
( ~ sP77(X0)
| sP35(X0) ),
inference(cnf_transformation,[],[f174]) ).
fof(f439,plain,
! [X0] :
( ~ sP77(X0)
| sP31(X0)
| sP32(X0)
| sP33(X0)
| ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,X0,nn) ),
inference(cnf_transformation,[],[f174]) ).
fof(f441,plain,
! [X0] :
( ~ sP77(X0)
| sP31(X0)
| sP32(X0)
| sP33(X0)
| v__1(sortedList_first,prev_2,X0) ),
inference(cnf_transformation,[],[f174]) ).
fof(f446,plain,
! [X0] :
( ~ sP76(X0)
| sP57(X0)
| sP58(X0)
| v__1(sortedList_first,X0,prev_2) ),
inference(cnf_transformation,[],[f175]) ).
fof(f449,plain,
! [X0] :
( ~ sP76(X0)
| sP63(X0)
| sP64(X0)
| sP65(X0)
| v__1(sortedList_first,prev_2,X0) ),
inference(cnf_transformation,[],[f175]) ).
fof(f452,plain,
! [X0] :
( ~ sP75(X0)
| v__1(null,X0,X0)
| v__1(null,X0,nn) ),
inference(cnf_transformation,[],[f176]) ).
fof(f453,plain,
! [X0] :
( ~ sP75(X0)
| v__1(sortedList_first,X0,nn) ),
inference(cnf_transformation,[],[f176]) ).
fof(f456,plain,
! [X0] :
( ~ sP75(X0)
| nn != X0 ),
inference(cnf_transformation,[],[f176]) ).
fof(f458,plain,
! [X0] :
( ~ sP74(X0)
| v__1(null,X0,X0)
| v__1(null,X0,nn) ),
inference(cnf_transformation,[],[f177]) ).
fof(f459,plain,
! [X0] :
( ~ sP74(X0)
| v__1(null,X0,X0) ),
inference(cnf_transformation,[],[f177]) ).
fof(f462,plain,
! [X0] :
( ~ sP74(X0)
| nn != X0 ),
inference(cnf_transformation,[],[f177]) ).
fof(f464,plain,
! [X0] :
( ~ sP73(X0)
| v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn) ),
inference(cnf_transformation,[],[f178]) ).
fof(f465,plain,
! [X0] :
( ~ sP73(X0)
| v__1(sortedList_first,X0,nn) ),
inference(cnf_transformation,[],[f178]) ).
fof(f466,plain,
! [X0] :
( ~ sP73(X0)
| ~ v__1(sortedList_first,prev_2,prev_2)
| v__1(sortedList_first,nn,prev_2) ),
inference(cnf_transformation,[],[f178]) ).
fof(f470,plain,
! [X0] :
( ~ sP72(X0)
| v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn) ),
inference(cnf_transformation,[],[f179]) ).
fof(f471,plain,
! [X0] :
( ~ sP72(X0)
| v__1(null,X0,prev_2) ),
inference(cnf_transformation,[],[f179]) ).
fof(f472,plain,
! [X0] :
( ~ sP72(X0)
| ~ v__1(sortedList_first,prev_2,prev_2)
| v__1(sortedList_first,nn,prev_2) ),
inference(cnf_transformation,[],[f179]) ).
fof(f475,plain,
! [X0] :
( ~ sP71(X0)
| sP69 ),
inference(cnf_transformation,[],[f180]) ).
fof(f478,plain,
! [X0] :
( ~ sP71(X0)
| ~ v__1(sortedList_first,prev_2,nn)
| ~ v__1(sortedList_first,prev_2,prev_2) ),
inference(cnf_transformation,[],[f180]) ).
fof(f482,plain,
( ~ sP70
| v__1(sortedList_first,prev_2,prev_2)
| ~ v__1(sortedList_first,nn,nn)
| v__1(null,nn,nn)
| ~ v__1(null,prev_2,prev_2)
| ~ v__1(sortedList_first,prev_2,nn)
| nn = prev_2 ),
inference(cnf_transformation,[],[f181]) ).
fof(f510,plain,
! [X0] :
( ~ sP65(X0)
| v__1(sortedList_first,prev_2,nn) ),
inference(cnf_transformation,[],[f187]) ).
fof(f511,plain,
! [X0] :
( ~ sP65(X0)
| ~ v__1(sortedList_first,X0,X0)
| v__1(sortedList_first,nn,X0) ),
inference(cnf_transformation,[],[f187]) ).
fof(f513,plain,
! [X0] :
( ~ sP65(X0)
| nn != X0 ),
inference(cnf_transformation,[],[f187]) ).
fof(f519,plain,
! [X0] :
( ~ sP64(X0)
| nn != X0 ),
inference(cnf_transformation,[],[f188]) ).
fof(f523,plain,
! [X0] :
( ~ sP63(X0)
| ~ v__1(sortedList_first,X0,nn)
| ~ v__1(sortedList_first,X0,X0) ),
inference(cnf_transformation,[],[f189]) ).
fof(f524,plain,
! [X0] :
( ~ sP63(X0)
| sP59
| sP60
| ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,prev_2,nn) ),
inference(cnf_transformation,[],[f189]) ).
fof(f537,plain,
( ~ sP60
| v__1(sortedList_first,prev_2,nn) ),
inference(cnf_transformation,[],[f192]) ).
fof(f544,plain,
( ~ sP59
| ~ v__1(sortedList_first,prev_2,prev_2)
| v__1(sortedList_first,nn,prev_2) ),
inference(cnf_transformation,[],[f193]) ).
fof(f547,plain,
! [X0] :
( ~ sP58(X0)
| ~ v__1(null,nn,nn)
| v__1(null,prev_2,nn) ),
inference(cnf_transformation,[],[f194]) ).
fof(f548,plain,
! [X0] :
( ~ sP58(X0)
| v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn) ),
inference(cnf_transformation,[],[f194]) ).
fof(f549,plain,
! [X0] :
( ~ sP58(X0)
| v__1(sortedList_first,X0,nn) ),
inference(cnf_transformation,[],[f194]) ).
fof(f550,plain,
! [X0] :
( ~ sP58(X0)
| ~ v__1(sortedList_first,prev_2,prev_2)
| v__1(sortedList_first,nn,prev_2) ),
inference(cnf_transformation,[],[f194]) ).
fof(f553,plain,
! [X0] :
( ~ sP57(X0)
| ~ v__1(null,nn,nn)
| v__1(null,prev_2,nn) ),
inference(cnf_transformation,[],[f195]) ).
fof(f554,plain,
! [X0] :
( ~ sP57(X0)
| v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn) ),
inference(cnf_transformation,[],[f195]) ).
fof(f555,plain,
! [X0] :
( ~ sP57(X0)
| v__1(null,X0,prev_2) ),
inference(cnf_transformation,[],[f195]) ).
fof(f556,plain,
! [X0] :
( ~ sP57(X0)
| ~ v__1(sortedList_first,prev_2,prev_2)
| v__1(sortedList_first,nn,prev_2) ),
inference(cnf_transformation,[],[f195]) ).
fof(f678,plain,
! [X0] :
( ~ sP35(X0)
| sP25(X0)
| sP26(X0)
| node_next(nn) = sK113(X0) ),
inference(cnf_transformation,[],[f261]) ).
fof(f679,plain,
! [X0] :
( ~ sP35(X0)
| sP25(X0)
| sP26(X0)
| v__1(sK113(X0),X0,X0) ),
inference(cnf_transformation,[],[f261]) ).
fof(f688,plain,
! [X0] :
( ~ sP33(X0)
| v__1(null,X0,X0)
| v__1(null,X0,nn) ),
inference(cnf_transformation,[],[f265]) ).
fof(f690,plain,
! [X0] :
( ~ sP33(X0)
| ~ v__1(sortedList_first,X0,X0)
| v__1(sortedList_first,nn,X0) ),
inference(cnf_transformation,[],[f265]) ).
fof(f692,plain,
! [X0] :
( ~ sP33(X0)
| nn != X0 ),
inference(cnf_transformation,[],[f265]) ).
fof(f695,plain,
! [X0] :
( ~ sP32(X0)
| v__1(null,prev_2,X0) ),
inference(cnf_transformation,[],[f266]) ).
fof(f698,plain,
! [X0] :
( ~ sP32(X0)
| nn != X0 ),
inference(cnf_transformation,[],[f266]) ).
fof(f702,plain,
! [X0] :
( ~ sP31(X0)
| ~ v__1(sortedList_first,X0,nn)
| ~ v__1(sortedList_first,X0,X0) ),
inference(cnf_transformation,[],[f267]) ).
fof(f727,plain,
! [X0] :
( ~ sP26(X0)
| v__1(null,X0,X0)
| v__1(null,X0,nn) ),
inference(cnf_transformation,[],[f274]) ).
fof(f728,plain,
! [X0] :
( ~ sP26(X0)
| sP23(X0) ),
inference(cnf_transformation,[],[f274]) ).
fof(f735,plain,
! [X0] :
( ~ sP25(X0)
| v__1(null,X0,X0) ),
inference(cnf_transformation,[],[f277]) ).
fof(f747,plain,
! [X0] :
( ~ sP23(X0)
| v__1(sK121(X0),X0,nn) ),
inference(cnf_transformation,[],[f283]) ).
fof(f748,plain,
! [X0] :
( ~ sP23(X0)
| object(sK121(X0)) ),
inference(cnf_transformation,[],[f283]) ).
fof(f877,plain,
( nn = sK157
| ~ v__1(sortedList_first,sK157,sK157)
| null = sK157 ),
inference(cnf_transformation,[],[f353]) ).
fof(f878,plain,
( sP77(sK157)
| sP76(sK157)
| sP71(sK157)
| sP72(sK157)
| sP73(sK157)
| ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,prev_2,nn) ),
inference(cnf_transformation,[],[f353]) ).
fof(f880,plain,
( sP77(sK157)
| sP76(sK157)
| sP71(sK157)
| sP72(sK157)
| sP73(sK157)
| v__1(sortedList_first,sK157,prev_2) ),
inference(cnf_transformation,[],[f353]) ).
fof(f881,plain,
( sP77(sK157)
| sP76(sK157)
| sP74(sK157)
| sP75(sK157)
| ~ v__1(sortedList_first,nn,nn)
| v__1(sortedList_first,sK157,nn) ),
inference(cnf_transformation,[],[f353]) ).
fof(f882,plain,
( sP77(sK157)
| sP76(sK157)
| sP74(sK157)
| sP75(sK157)
| v__1(sortedList_first,sK157,sK157)
| v__1(sortedList_first,sK157,nn) ),
inference(cnf_transformation,[],[f353]) ).
fof(f883,plain,
( sP77(sK157)
| sP76(sK157)
| sP74(sK157)
| sP75(sK157)
| v__1(sortedList_first,sK157,sK157) ),
inference(cnf_transformation,[],[f353]) ).
fof(f884,plain,
null != sK157,
inference(cnf_transformation,[],[f353]) ).
fof(f885,plain,
object(sK157),
inference(cnf_transformation,[],[f353]) ).
fof(f889,plain,
! [X0,X1] :
( v__1(X0,node_next(X0),X1)
| ~ object(node_next(X0))
| X0 = X1
| ~ v__1(X0,X1,X1)
| ~ object(X1)
| ~ object(X0) ),
inference(equality_resolution,[],[f383]) ).
fof(f893,plain,
! [X0,X1,X5] :
( node_key(X1) != X5
| node_key(X0) != X5
| ~ integer(X5)
| 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,[],[f408]) ).
fof(f894,plain,
! [X0,X1] :
( node_key(X0) != node_key(X1)
| ~ integer(node_key(X0))
| 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,[],[f893]) ).
fof(f910,plain,
~ sP75(nn),
inference(equality_resolution,[],[f456]) ).
fof(f911,plain,
~ sP74(nn),
inference(equality_resolution,[],[f462]) ).
fof(f914,plain,
~ sP65(nn),
inference(equality_resolution,[],[f513]) ).
fof(f915,plain,
~ sP64(nn),
inference(equality_resolution,[],[f519]) ).
fof(f918,plain,
~ sP33(nn),
inference(equality_resolution,[],[f692]) ).
fof(f919,plain,
~ sP32(nn),
inference(equality_resolution,[],[f698]) ).
tcf(c_56,plain,
object(nn),
inference(cnf_transformation,[],[f361]) ).
tcf(c_58,plain,
object(prev_2),
inference(cnf_transformation,[],[f363]) ).
tcf(c_60,plain,
! [X0: $i] : integer(node_key(X0)),
inference(cnf_transformation,[],[f365]) ).
tcf(c_61,plain,
object(null),
inference(cnf_transformation,[],[f366]) ).
tcf(c_63,plain,
object(sortedList_first),
inference(cnf_transformation,[],[f368]) ).
tcf(c_64,plain,
! [X0: $i] : object(node_next(X0)),
inference(cnf_transformation,[],[f369]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i,X2: $i] :
( v__1(X0,X2,X2)
| ~ object(X2)
| ~ object(X1)
| ~ object(X0)
| ~ v__1(X1,X2,X2)
| ~ v__1(X0,X1,X1) ),
inference(cnf_transformation,[],[f371]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v__1(X0,X1,X3)
| ~ object(X3)
| ~ object(X2)
| ~ object(X1)
| ~ object(X0)
| ~ v__1(X1,X3,X2)
| ~ v__1(X0,X1,X2) ),
inference(cnf_transformation,[],[f373]) ).
tcf(c_68,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v__1(X0,X3,X2)
| ~ object(X3)
| ~ object(X2)
| ~ object(X1)
| ~ object(X0)
| ~ v__1(X1,X3,X2)
| ~ v__1(X0,X1,X2) ),
inference(cnf_transformation,[],[f372]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v__1(X1,X2,X3)
| ~ object(X3)
| ~ object(X2)
| ~ object(X1)
| ~ object(X0)
| ~ v__1(X0,X2,X3)
| ~ v__1(X0,X1,X2) ),
inference(cnf_transformation,[],[f374]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i,X2: $i] :
( v__1(X0,X2,X1)
| v__1(X0,X1,X2)
| ~ object(X2)
| ~ object(X1)
| ~ object(X0)
| ~ v__1(X0,X2,X2)
| ~ v__1(X0,X1,X1) ),
inference(cnf_transformation,[],[f376]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i,X2: $i] :
( v__1(X0,X1,X1)
| ~ object(X2)
| ~ object(X1)
| ~ object(X0)
| ~ v__1(X0,X1,X2) ),
inference(cnf_transformation,[],[f378]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i,X2: $i] :
( v__1(X1,X2,X2)
| ~ object(X2)
| ~ object(X1)
| ~ object(X0)
| ~ v__1(X0,X1,X2) ),
inference(cnf_transformation,[],[f377]) ).
tcf(c_74,plain,
! [X0: $i] :
( v__1(X0,X0,X0)
| ~ object(X0) ),
inference(cnf_transformation,[],[f379]) ).
tcf(c_75,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ object(X1)
| ~ object(X0)
| ~ v__1(X0,X1,X0) ),
inference(cnf_transformation,[],[f380]) ).
tcf(c_76,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ object(X1)
| ~ object(X0)
| ~ v__1(X0,X1,X1)
| ( node_next(X0) != X0 ) ),
inference(cnf_transformation,[],[f381]) ).
tcf(c_77,plain,
! [X0: $i] :
( v__1(X0,node_next(X0),node_next(X0))
| ~ object(X0)
| ~ object(node_next(X0)) ),
inference(cnf_transformation,[],[f925]) ).
tcf(c_78,plain,
! [X0: $i,X1: $i] :
( v__1(X0,node_next(X0),X1)
| ( X0 = X1 )
| ~ object(X1)
| ~ object(X0)
| ~ object(node_next(X0))
| ~ v__1(X0,X1,X1) ),
inference(cnf_transformation,[],[f889]) ).
tcf(c_79,plain,
prev_2 != null,
inference(cnf_transformation,[],[f384]) ).
tcf(c_88,plain,
( v__1(sortedList_first,prev_2,prev_2)
| ( prev_2 = null ) ),
inference(cnf_transformation,[],[f393]) ).
tcf(c_89,plain,
( v__1(sortedList_first,nn,nn)
| ( nn = null ) ),
inference(cnf_transformation,[],[f395]) ).
tcf(c_91,plain,
( ( prev_2 = null )
| ( node_next(prev_2) = nn ) ),
inference(cnf_transformation,[],[f398]) ).
tcf(c_101,plain,
! [X0: $i,X1: $i] :
( ( X1 = null )
| ( X0 = null )
| ~ object(X1)
| ~ object(X0)
| ~ object(node_next(X0))
| ~ integer(node_key(X0))
| ~ v__1(sortedList_first,X0,X0)
| ~ v__1(node_next(X0),X1,X1)
| ( node_key(X0) != node_key(X1) ) ),
inference(cnf_transformation,[],[f894]) ).
tcf(c_103,plain,
! [X0: $i] :
( ( null = sortedList_first )
| ~ object(X0)
| ( node_next(X0) != sortedList_first ) ),
inference(cnf_transformation,[],[f412]) ).
tcf(c_104,plain,
nn != null,
inference(cnf_transformation,[],[f413]) ).
tcf(c_125,plain,
node_next(null) = null,
inference(cnf_transformation,[],[f435]) ).
tcf(c_128,plain,
! [X0: $i] :
( sP31(X0)
| sP32(X0)
| sP33(X0)
| v__1(sortedList_first,prev_2,X0)
| ~ sP77(X0) ),
inference(cnf_transformation,[],[f441]) ).
tcf(c_130,plain,
! [X0: $i] :
( sP31(X0)
| sP32(X0)
| sP33(X0)
| v__1(sortedList_first,X0,nn)
| ~ sP77(X0)
| ~ v__1(sortedList_first,nn,nn) ),
inference(cnf_transformation,[],[f439]) ).
tcf(c_131,plain,
! [X0: $i] :
( sP35(X0)
| ~ sP77(X0) ),
inference(cnf_transformation,[],[f438]) ).
tcf(c_134,plain,
! [X0: $i] :
( sP63(X0)
| sP64(X0)
| sP65(X0)
| v__1(sortedList_first,prev_2,X0)
| ~ sP76(X0) ),
inference(cnf_transformation,[],[f449]) ).
tcf(c_137,plain,
! [X0: $i] :
( sP57(X0)
| sP58(X0)
| v__1(sortedList_first,X0,prev_2)
| ~ sP76(X0) ),
inference(cnf_transformation,[],[f446]) ).
tcf(c_141,plain,
~ sP75(nn),
inference(cnf_transformation,[],[f910]) ).
tcf(c_144,plain,
! [X0: $i] :
( v__1(sortedList_first,X0,nn)
| ~ sP75(X0) ),
inference(cnf_transformation,[],[f453]) ).
tcf(c_145,plain,
! [X0: $i] :
( v__1(null,X0,nn)
| v__1(null,X0,X0)
| ~ sP75(X0) ),
inference(cnf_transformation,[],[f452]) ).
tcf(c_147,plain,
~ sP74(nn),
inference(cnf_transformation,[],[f911]) ).
tcf(c_150,plain,
! [X0: $i] :
( v__1(null,X0,X0)
| ~ sP74(X0) ),
inference(cnf_transformation,[],[f459]) ).
tcf(c_151,plain,
! [X0: $i] :
( v__1(null,X0,nn)
| v__1(null,X0,X0)
| ~ sP74(X0) ),
inference(cnf_transformation,[],[f458]) ).
tcf(c_155,plain,
! [X0: $i] :
( v__1(sortedList_first,nn,prev_2)
| ~ sP73(X0)
| ~ v__1(sortedList_first,prev_2,prev_2) ),
inference(cnf_transformation,[],[f466]) ).
tcf(c_156,plain,
! [X0: $i] :
( v__1(sortedList_first,X0,nn)
| ~ sP73(X0) ),
inference(cnf_transformation,[],[f465]) ).
tcf(c_157,plain,
! [X0: $i] :
( v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn)
| ~ sP73(X0) ),
inference(cnf_transformation,[],[f464]) ).
tcf(c_161,plain,
! [X0: $i] :
( v__1(sortedList_first,nn,prev_2)
| ~ sP72(X0)
| ~ v__1(sortedList_first,prev_2,prev_2) ),
inference(cnf_transformation,[],[f472]) ).
tcf(c_162,plain,
! [X0: $i] :
( v__1(null,X0,prev_2)
| ~ sP72(X0) ),
inference(cnf_transformation,[],[f471]) ).
tcf(c_163,plain,
! [X0: $i] :
( v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn)
| ~ sP72(X0) ),
inference(cnf_transformation,[],[f470]) ).
tcf(c_168,plain,
! [X0: $i] :
( ~ sP71(X0)
| ~ v__1(sortedList_first,prev_2,prev_2)
| ~ v__1(sortedList_first,prev_2,nn) ),
inference(cnf_transformation,[],[f478]) ).
tcf(c_169,plain,
! [X0: $i] :
( v__1(sortedList_first,nn,nn)
| ~ sP71(X0)
| ~ v__1(sortedList_first,prev_2,prev_2) ),
inference(cnf_transformation,[],[f926]) ).
tcf(c_171,plain,
! [X0: $i] :
( sP69
| ~ sP71(X0) ),
inference(cnf_transformation,[],[f475]) ).
tcf(c_175,plain,
( v__1(sortedList_first,prev_2,prev_2)
| v__1(null,nn,nn)
| ( nn = prev_2 )
| ~ sP70
| ~ v__1(sortedList_first,prev_2,nn)
| ~ v__1(sortedList_first,nn,nn)
| ~ v__1(null,prev_2,prev_2) ),
inference(cnf_transformation,[],[f482]) ).
tcf(c_178,plain,
( v__1(null,nn,nn)
| ( nn = prev_2 )
| ~ sP69
| ~ v__1(sortedList_first,nn,prev_2)
| ~ v__1(null,prev_2,prev_2) ),
inference(cnf_transformation,[],[f927]) ).
tcf(c_198,plain,
~ sP65(nn),
inference(cnf_transformation,[],[f914]) ).
tcf(c_200,plain,
! [X0: $i] :
( v__1(sortedList_first,nn,X0)
| ~ sP65(X0)
| ~ v__1(sortedList_first,X0,X0) ),
inference(cnf_transformation,[],[f511]) ).
tcf(c_201,plain,
! [X0: $i] :
( v__1(sortedList_first,prev_2,nn)
| ~ sP65(X0) ),
inference(cnf_transformation,[],[f510]) ).
tcf(c_204,plain,
~ sP64(nn),
inference(cnf_transformation,[],[f915]) ).
tcf(c_212,plain,
! [X0: $i] :
( sP59
| sP60
| v__1(sortedList_first,prev_2,nn)
| ~ sP63(X0)
| ~ v__1(sortedList_first,nn,nn) ),
inference(cnf_transformation,[],[f524]) ).
tcf(c_213,plain,
! [X0: $i] :
( ~ sP63(X0)
| ~ v__1(sortedList_first,X0,nn)
| ~ v__1(sortedList_first,X0,X0) ),
inference(cnf_transformation,[],[f523]) ).
tcf(c_228,plain,
( v__1(sortedList_first,prev_2,nn)
| ~ sP60 ),
inference(cnf_transformation,[],[f537]) ).
tcf(c_233,plain,
( v__1(sortedList_first,nn,prev_2)
| ~ sP59
| ~ v__1(sortedList_first,prev_2,prev_2) ),
inference(cnf_transformation,[],[f544]) ).
tcf(c_239,plain,
! [X0: $i] :
( v__1(sortedList_first,nn,prev_2)
| ~ sP58(X0)
| ~ v__1(sortedList_first,prev_2,prev_2) ),
inference(cnf_transformation,[],[f550]) ).
tcf(c_240,plain,
! [X0: $i] :
( v__1(sortedList_first,X0,nn)
| ~ sP58(X0) ),
inference(cnf_transformation,[],[f549]) ).
tcf(c_241,plain,
! [X0: $i] :
( v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn)
| ~ sP58(X0) ),
inference(cnf_transformation,[],[f548]) ).
tcf(c_242,plain,
! [X0: $i] :
( v__1(null,prev_2,nn)
| ~ sP58(X0)
| ~ v__1(null,nn,nn) ),
inference(cnf_transformation,[],[f547]) ).
tcf(c_245,plain,
! [X0: $i] :
( v__1(sortedList_first,nn,prev_2)
| ~ sP57(X0)
| ~ v__1(sortedList_first,prev_2,prev_2) ),
inference(cnf_transformation,[],[f556]) ).
tcf(c_246,plain,
! [X0: $i] :
( v__1(null,X0,prev_2)
| ~ sP57(X0) ),
inference(cnf_transformation,[],[f555]) ).
tcf(c_247,plain,
! [X0: $i] :
( v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn)
| ~ sP57(X0) ),
inference(cnf_transformation,[],[f554]) ).
tcf(c_248,plain,
! [X0: $i] :
( v__1(null,prev_2,nn)
| ~ sP57(X0)
| ~ v__1(null,nn,nn) ),
inference(cnf_transformation,[],[f553]) ).
tcf(c_366,plain,
! [X0: $i] :
( sP25(X0)
| sP26(X0)
| v__1(sK113(X0),X0,X0)
| ~ sP35(X0) ),
inference(cnf_transformation,[],[f679]) ).
tcf(c_367,plain,
! [X0: $i] :
( sP25(X0)
| sP26(X0)
| ( sK113(X0) = node_next(nn) )
| ~ sP35(X0) ),
inference(cnf_transformation,[],[f678]) ).
tcf(c_377,plain,
~ sP33(nn),
inference(cnf_transformation,[],[f918]) ).
tcf(c_379,plain,
! [X0: $i] :
( v__1(sortedList_first,nn,X0)
| ~ sP33(X0)
| ~ v__1(sortedList_first,X0,X0) ),
inference(cnf_transformation,[],[f690]) ).
tcf(c_381,plain,
! [X0: $i] :
( v__1(null,X0,nn)
| v__1(null,X0,X0)
| ~ sP33(X0) ),
inference(cnf_transformation,[],[f688]) ).
tcf(c_383,plain,
~ sP32(nn),
inference(cnf_transformation,[],[f919]) ).
tcf(c_386,plain,
! [X0: $i] :
( v__1(null,prev_2,X0)
| ~ sP32(X0) ),
inference(cnf_transformation,[],[f695]) ).
tcf(c_392,plain,
! [X0: $i] :
( ~ sP31(X0)
| ~ v__1(sortedList_first,X0,nn)
| ~ v__1(sortedList_first,X0,X0) ),
inference(cnf_transformation,[],[f702]) ).
tcf(c_420,plain,
! [X0: $i] :
( sP23(X0)
| ~ sP26(X0) ),
inference(cnf_transformation,[],[f728]) ).
tcf(c_421,plain,
! [X0: $i] :
( v__1(null,X0,nn)
| v__1(null,X0,X0)
| ~ sP26(X0) ),
inference(cnf_transformation,[],[f727]) ).
tcf(c_427,plain,
! [X0: $i] :
( v__1(null,X0,X0)
| ~ sP25(X0) ),
inference(cnf_transformation,[],[f735]) ).
tcf(c_436,plain,
! [X0: $i] :
( object(sK121(X0))
| ~ sP23(X0) ),
inference(cnf_transformation,[],[f748]) ).
tcf(c_437,plain,
! [X0: $i] :
( v__1(sK121(X0),X0,nn)
| ~ sP23(X0) ),
inference(cnf_transformation,[],[f747]) ).
tcf(c_567,negated_conjecture,
object(sK157),
inference(cnf_transformation,[],[f885]) ).
tcf(c_568,negated_conjecture,
null != sK157,
inference(cnf_transformation,[],[f884]) ).
tcf(c_569,negated_conjecture,
( sP74(sK157)
| sP75(sK157)
| sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,sK157) ),
inference(cnf_transformation,[],[f883]) ).
tcf(c_570,negated_conjecture,
( sP74(sK157)
| sP75(sK157)
| sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,sK157)
| v__1(sortedList_first,sK157,nn) ),
inference(cnf_transformation,[],[f882]) ).
tcf(c_571,negated_conjecture,
( sP74(sK157)
| sP75(sK157)
| sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,nn)
| ~ v__1(sortedList_first,nn,nn) ),
inference(cnf_transformation,[],[f881]) ).
tcf(c_572,negated_conjecture,
( sP71(sK157)
| sP72(sK157)
| sP73(sK157)
| sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,prev_2) ),
inference(cnf_transformation,[],[f880]) ).
tcf(c_574,negated_conjecture,
( sP71(sK157)
| sP72(sK157)
| sP73(sK157)
| sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,prev_2,nn)
| ~ v__1(sortedList_first,nn,nn) ),
inference(cnf_transformation,[],[f878]) ).
tcf(c_575,negated_conjecture,
( ( null = sK157 )
| ( nn = sK157 )
| ~ v__1(sortedList_first,sK157,sK157) ),
inference(cnf_transformation,[],[f877]) ).
tcf(c_637,plain,
( v__1(nn,nn,nn)
| ~ object(nn) ),
inference(instantiation,[status(thm)],[c_74]) ).
tcf(c_743,plain,
( ~ sP31(nn)
| ~ v__1(sortedList_first,nn,nn) ),
inference(instantiation,[status(thm)],[c_392]) ).
tcf(c_747,plain,
( ~ sP63(nn)
| ~ v__1(sortedList_first,nn,nn) ),
inference(instantiation,[status(thm)],[c_213]) ).
tcf(c_776,plain,
( ( nn = nn )
| ~ object(nn)
| ~ v__1(nn,nn,nn) ),
inference(instantiation,[status(thm)],[c_75]) ).
tcf(c_815,plain,
node_next(prev_2) = nn,
inference(global_subsumption_just,[status(thm)],[c_91,c_79,c_91]) ).
tcf(c_855,plain,
( v__1(sortedList_first,nn,prev_2)
| ~ sP59 ),
inference(global_subsumption_just,[status(thm)],[c_233,c_79,c_88,c_233]) ).
tcf(c_873,plain,
! [X0: $i] :
( ~ sP74(X0)
| v__1(null,X0,X0) ),
inference(global_subsumption_just,[status(thm)],[c_151,c_150]) ).
tcf(c_874,plain,
! [X0: $i] :
( v__1(null,X0,X0)
| ~ sP74(X0) ),
inference(renaming,[status(thm)],[c_873]) ).
tcf(c_881,plain,
! [X0: $i] :
( v__1(sortedList_first,nn,prev_2)
| ~ sP57(X0) ),
inference(global_subsumption_just,[status(thm)],[c_245,c_79,c_88,c_245]) ).
tcf(c_884,plain,
! [X0: $i] :
( v__1(sortedList_first,nn,prev_2)
| ~ sP58(X0) ),
inference(global_subsumption_just,[status(thm)],[c_239,c_79,c_88,c_239]) ).
tcf(c_889,plain,
v__1(sortedList_first,nn,nn),
inference(global_subsumption_just,[status(thm)],[c_169,c_104,c_89]) ).
tcf(c_891,plain,
! [X0: $i] :
( v__1(sortedList_first,nn,prev_2)
| ~ sP72(X0) ),
inference(global_subsumption_just,[status(thm)],[c_161,c_79,c_88,c_161]) ).
tcf(c_894,plain,
! [X0: $i] :
( v__1(sortedList_first,nn,prev_2)
| ~ sP73(X0) ),
inference(global_subsumption_just,[status(thm)],[c_155,c_79,c_88,c_155]) ).
tcf(c_897,plain,
( ~ v__1(sortedList_first,sK157,sK157)
| ( nn = sK157 ) ),
inference(global_subsumption_just,[status(thm)],[c_575,c_568,c_575]) ).
tcf(c_898,negated_conjecture,
( ( nn = sK157 )
| ~ v__1(sortedList_first,sK157,sK157) ),
inference(renaming,[status(thm)],[c_897]) ).
tcf(c_903,plain,
! [X0: $i] :
( ~ sP71(X0)
| ~ v__1(sortedList_first,prev_2,nn) ),
inference(global_subsumption_just,[status(thm)],[c_168,c_79,c_88,c_168]) ).
tcf(c_911,plain,
! [X0: $i] :
( v__1(X0,node_next(X0),node_next(X0))
| ~ object(X0) ),
inference(global_subsumption_just,[status(thm)],[c_77,c_64,c_77]) ).
tcf(c_917,plain,
! [X0: $i] :
( sP59
| ~ sP63(X0)
| v__1(sortedList_first,prev_2,nn) ),
inference(global_subsumption_just,[status(thm)],[c_212,c_104,c_228,c_89,c_212]) ).
tcf(c_918,plain,
! [X0: $i] :
( sP59
| v__1(sortedList_first,prev_2,nn)
| ~ sP63(X0) ),
inference(renaming,[status(thm)],[c_917]) ).
tcf(c_927,negated_conjecture,
( sP74(sK157)
| sP75(sK157)
| sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,sK157) ),
inference(global_subsumption_just,[status(thm)],[c_570,c_569]) ).
tcf(c_934,negated_conjecture,
( sP74(sK157)
| sP75(sK157)
| sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,nn) ),
inference(global_subsumption_just,[status(thm)],[c_571,c_104,c_89,c_571]) ).
tcf(c_944,plain,
! [X0: $i] :
( sP31(X0)
| sP32(X0)
| sP33(X0)
| v__1(sortedList_first,X0,nn)
| ~ sP77(X0) ),
inference(global_subsumption_just,[status(thm)],[c_130,c_104,c_89,c_130]) ).
tcf(c_946,negated_conjecture,
( sP71(sK157)
| sP72(sK157)
| sP73(sK157)
| sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,prev_2,nn) ),
inference(global_subsumption_just,[status(thm)],[c_574,c_104,c_89,c_574]) ).
tcf(c_953,plain,
! [X0: $i,X1: $i] :
( v__1(X0,node_next(X0),X1)
| ( X0 = X1 )
| ~ object(X1)
| ~ object(X0)
| ~ v__1(X0,X1,X1) ),
inference(global_subsumption_just,[status(thm)],[c_78,c_64,c_78]) ).
tcf(c_971,plain,
v__1(sortedList_first,prev_2,prev_2),
inference(global_subsumption_just,[status(thm)],[c_175,c_79,c_88]) ).
tcf(c_977,plain,
! [X0: $i,X1: $i] :
( ( X1 = null )
| ( X0 = null )
| ~ object(X1)
| ~ object(X0)
| ~ v__1(sortedList_first,X0,X0)
| ~ v__1(node_next(X0),X1,X1)
| ( node_key(X0) != node_key(X1) ) ),
inference(global_subsumption_just,[status(thm)],[c_101,c_64,c_60,c_101]) ).
tcf(c_979,plain,
( ( nn = null )
| ~ object(nn)
| ~ v__1(sortedList_first,nn,nn)
| ~ v__1(node_next(nn),nn,nn)
| ( node_key(nn) != node_key(nn) ) ),
inference(instantiation,[status(thm)],[c_977]) ).
tcf(c_1448,plain,
( sP74(sK157)
| sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,nn) ),
inference(backward_subsumption_resolution,[status(thm)],[c_934,c_144]) ).
tcf(c_6281,plain,
! [X0: $i,X1: $i] :
( v__1(sK121(X1),X1,nn)
| ~ sP26(X0)
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_420,c_437]) ).
tcf(c_6282,plain,
! [X0: $i] :
( v__1(sK121(X0),X0,nn)
| ~ sP26(X0) ),
inference(unflattening,[status(thm)],[c_6281]) ).
tcf(c_6289,plain,
! [X0: $i,X1: $i] :
( object(sK121(X1))
| ~ sP26(X0)
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_420,c_436]) ).
tcf(c_6290,plain,
! [X0: $i] :
( object(sK121(X0))
| ~ sP26(X0) ),
inference(unflattening,[status(thm)],[c_6289]) ).
tcf(c_6928,plain,
! [X0: $i,X1: $i] :
( sP25(X1)
| sP26(X1)
| ( sK113(X1) = node_next(nn) )
| ~ sP77(X0)
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_131,c_367]) ).
tcf(c_6929,plain,
! [X0: $i] :
( sP25(X0)
| sP26(X0)
| ( sK113(X0) = node_next(nn) )
| ~ sP77(X0) ),
inference(unflattening,[status(thm)],[c_6928]) ).
tcf(c_6943,plain,
! [X0: $i,X1: $i] :
( sP25(X1)
| sP26(X1)
| v__1(sK113(X1),X1,X1)
| ~ sP77(X0)
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_131,c_366]) ).
tcf(c_6944,plain,
! [X0: $i] :
( sP25(X0)
| sP26(X0)
| v__1(sK113(X0),X0,X0)
| ~ sP77(X0) ),
inference(unflattening,[status(thm)],[c_6943]) ).
tcf(c_7000,plain,
( sP74(sK157)
| sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,sK157)
| ( nn != sK157 ) ),
inference(resolution_lifted,[status(thm)],[c_141,c_927]) ).
tcf(c_7036,plain,
! [X0: $i] :
( sP74(sK157)
| sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,sK157)
| v__1(null,X0,nn)
| v__1(null,X0,X0)
| ( X0 != sK157 ) ),
inference(resolution_lifted,[status(thm)],[c_145,c_927]) ).
tcf(c_7037,plain,
( sP74(sK157)
| sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,sK157)
| v__1(null,sK157,sK157)
| v__1(null,sK157,nn) ),
inference(unflattening,[status(thm)],[c_7036]) ).
tcf(c_7050,plain,
( sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,sK157)
| v__1(null,sK157,sK157)
| v__1(null,sK157,nn) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7037,c_874]) ).
tcf(c_8619,plain,
( sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,sK157)
| ( nn != sK157 ) ),
inference(resolution_lifted,[status(thm)],[c_147,c_7000]) ).
tcf(c_8668,plain,
! [X0: $i] :
( sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,nn)
| v__1(null,X0,X0)
| ( X0 != sK157 ) ),
inference(resolution_lifted,[status(thm)],[c_874,c_1448]) ).
tcf(c_8669,plain,
( sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,nn)
| v__1(null,sK157,sK157) ),
inference(unflattening,[status(thm)],[c_8668]) ).
tcf(c_8801,plain,
! [X0: $i,X1: $i] :
( sP57(X0)
| v__1(sortedList_first,nn,prev_2)
| v__1(sortedList_first,X0,prev_2)
| ~ sP76(X0)
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_137,c_884]) ).
tcf(c_8802,plain,
! [X0: $i] :
( sP57(X0)
| v__1(sortedList_first,nn,prev_2)
| v__1(sortedList_first,X0,prev_2)
| ~ sP76(X0) ),
inference(unflattening,[status(thm)],[c_8801]) ).
tcf(c_8804,plain,
! [X0: $i] :
( ~ sP76(X0)
| v__1(sortedList_first,X0,prev_2)
| v__1(sortedList_first,nn,prev_2) ),
inference(global_subsumption_just,[status(thm)],[c_8802,c_137,c_881,c_884]) ).
tcf(c_8805,plain,
! [X0: $i] :
( v__1(sortedList_first,nn,prev_2)
| v__1(sortedList_first,X0,prev_2)
| ~ sP76(X0) ),
inference(renaming,[status(thm)],[c_8804]) ).
tcf(c_8806,plain,
( v__1(sortedList_first,nn,prev_2)
| ~ sP76(nn) ),
inference(instantiation,[status(thm)],[c_8805]) ).
tcf(c_9619,plain,
! [X0: $i,X1: $i] :
( sP63(X0)
| sP64(X0)
| v__1(sortedList_first,prev_2,nn)
| v__1(sortedList_first,prev_2,X0)
| ~ sP76(X0)
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_134,c_201]) ).
tcf(c_9620,plain,
! [X0: $i] :
( sP63(X0)
| sP64(X0)
| v__1(sortedList_first,prev_2,nn)
| v__1(sortedList_first,prev_2,X0)
| ~ sP76(X0) ),
inference(unflattening,[status(thm)],[c_9619]) ).
tcf(c_9621,plain,
( sP63(nn)
| sP64(nn)
| v__1(sortedList_first,prev_2,nn)
| ~ sP76(nn) ),
inference(instantiation,[status(thm)],[c_9620]) ).
tcf(c_9658,plain,
! [X0: $i] :
( sP63(X0)
| sP64(X0)
| v__1(sortedList_first,prev_2,X0)
| ~ sP76(X0)
| ( X0 != nn ) ),
inference(resolution_lifted,[status(thm)],[c_134,c_198]) ).
tcf(c_9659,plain,
( sP63(nn)
| sP64(nn)
| v__1(sortedList_first,prev_2,nn)
| ~ sP76(nn) ),
inference(unflattening,[status(thm)],[c_9658]) ).
tcf(c_9660,plain,
( v__1(sortedList_first,prev_2,nn)
| ~ sP76(nn) ),
inference(global_subsumption_just,[status(thm)],[c_9659,c_204,c_104,c_89,c_747,c_9621]) ).
tcf(c_13030,plain,
! [X0: $i] :
( sP71(sK157)
| sP72(sK157)
| sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,prev_2)
| v__1(sortedList_first,nn,prev_2)
| ( X0 != sK157 ) ),
inference(resolution_lifted,[status(thm)],[c_894,c_572]) ).
tcf(c_13031,plain,
( sP71(sK157)
| sP72(sK157)
| sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,prev_2)
| v__1(sortedList_first,nn,prev_2) ),
inference(unflattening,[status(thm)],[c_13030]) ).
tcf(c_13044,plain,
( sP71(sK157)
| sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,prev_2)
| v__1(sortedList_first,nn,prev_2) ),
inference(forward_subsumption_resolution,[status(thm)],[c_13031,c_891]) ).
tcf(c_13119,plain,
! [X0: $i] :
( sP71(sK157)
| sP72(sK157)
| sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,prev_2)
| v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn)
| ( X0 != sK157 ) ),
inference(resolution_lifted,[status(thm)],[c_157,c_572]) ).
tcf(c_13120,plain,
( sP71(sK157)
| sP72(sK157)
| sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,prev_2)
| v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn) ),
inference(unflattening,[status(thm)],[c_13119]) ).
tcf(c_13135,plain,
( sP71(sK157)
| sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,prev_2)
| v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn) ),
inference(forward_subsumption_resolution,[status(thm)],[c_13120,c_163]) ).
tcf(c_13142,plain,
! [X0: $i] :
( sP71(sK157)
| sP72(sK157)
| sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,prev_2,nn)
| v__1(sortedList_first,X0,nn)
| ( X0 != sK157 ) ),
inference(resolution_lifted,[status(thm)],[c_156,c_946]) ).
tcf(c_13143,plain,
( sP71(sK157)
| sP72(sK157)
| sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,nn)
| v__1(sortedList_first,prev_2,nn) ),
inference(unflattening,[status(thm)],[c_13142]) ).
tcf(c_13322,plain,
! [X0: $i] :
( sP71(sK157)
| sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,nn)
| v__1(sortedList_first,prev_2,nn)
| v__1(null,X0,prev_2)
| ( X0 != sK157 ) ),
inference(resolution_lifted,[status(thm)],[c_162,c_13143]) ).
tcf(c_13323,plain,
( sP71(sK157)
| sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,nn)
| v__1(sortedList_first,prev_2,nn)
| v__1(null,sK157,prev_2) ),
inference(unflattening,[status(thm)],[c_13322]) ).
tcf(c_30074,plain,
! [X0: $i] :
( sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,prev_2)
| v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn)
| ~ v__1(sortedList_first,prev_2,nn)
| ( X0 != sK157 ) ),
inference(resolution_lifted,[status(thm)],[c_903,c_13135]) ).
tcf(c_30075,plain,
( sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,prev_2)
| v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn)
| ~ v__1(sortedList_first,prev_2,nn) ),
inference(unflattening,[status(thm)],[c_30074]) ).
tcf(c_30118,plain,
! [X0: $i] :
( sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,prev_2)
| v__1(sortedList_first,nn,prev_2)
| ~ v__1(sortedList_first,prev_2,nn)
| ( X0 != sK157 ) ),
inference(resolution_lifted,[status(thm)],[c_903,c_13044]) ).
tcf(c_30119,plain,
( sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,prev_2)
| v__1(sortedList_first,nn,prev_2)
| ~ v__1(sortedList_first,prev_2,nn) ),
inference(unflattening,[status(thm)],[c_30118]) ).
tcf(c_30137,plain,
! [X0: $i] :
( sP69
| sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,nn)
| v__1(sortedList_first,prev_2,nn)
| v__1(null,sK157,prev_2)
| ( X0 != sK157 ) ),
inference(resolution_lifted,[status(thm)],[c_171,c_13323]) ).
tcf(c_30138,plain,
( sP69
| sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,nn)
| v__1(sortedList_first,prev_2,nn)
| v__1(null,sK157,prev_2) ),
inference(unflattening,[status(thm)],[c_30137]) ).
tcf(c_30545,plain,
( sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,nn)
| v__1(sortedList_first,prev_2,nn)
| v__1(null,sK157,prev_2)
| v__1(null,nn,nn)
| ( nn = prev_2 )
| ~ v__1(sortedList_first,nn,prev_2)
| ~ v__1(null,prev_2,prev_2) ),
inference(resolution,[status(thm)],[c_30138,c_178]) ).
tcf(c_41326,plain,
! [X0: $i,X1: $i] :
( sP57(X0)
| v__1(sortedList_first,nn,prev_2)
| v__1(sortedList_first,X0,prev_2)
| ~ sP76(X0)
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_137,c_884]) ).
tcf(c_41327,plain,
! [X0: $i] :
( sP57(X0)
| v__1(sortedList_first,nn,prev_2)
| v__1(sortedList_first,X0,prev_2)
| ~ sP76(X0) ),
inference(unflattening,[status(thm)],[c_41326]) ).
tcf(c_41328,plain,
! [X0: $i] :
( ~ sP76(X0)
| v__1(sortedList_first,X0,prev_2)
| v__1(sortedList_first,nn,prev_2) ),
inference(global_subsumption_just,[status(thm)],[c_41327,c_137,c_881,c_884]) ).
tcf(c_41329,plain,
! [X0: $i] :
( v__1(sortedList_first,nn,prev_2)
| v__1(sortedList_first,X0,prev_2)
| ~ sP76(X0) ),
inference(renaming,[status(thm)],[c_41328]) ).
tcf(c_41355,plain,
! [X0: $i,X1: $i] :
( sP57(X0)
| v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn)
| v__1(sortedList_first,X0,prev_2)
| ~ sP76(X0)
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_137,c_241]) ).
tcf(c_41356,plain,
! [X0: $i] :
( sP57(X0)
| v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn)
| v__1(sortedList_first,X0,prev_2)
| ~ sP76(X0) ),
inference(unflattening,[status(thm)],[c_41355]) ).
tcf(c_41357,plain,
! [X0: $i] :
( ~ sP76(X0)
| v__1(sortedList_first,X0,prev_2)
| v__1(null,prev_2,nn)
| v__1(null,prev_2,prev_2) ),
inference(global_subsumption_just,[status(thm)],[c_41356,c_247,c_241,c_137]) ).
tcf(c_41358,plain,
! [X0: $i] :
( v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn)
| v__1(sortedList_first,X0,prev_2)
| ~ sP76(X0) ),
inference(renaming,[status(thm)],[c_41357]) ).
tcf(c_41417,plain,
( sP77(sK157)
| v__1(sortedList_first,sK157,prev_2)
| v__1(sortedList_first,nn,prev_2)
| ~ v__1(sortedList_first,prev_2,nn) ),
inference(backward_subsumption_resolution,[status(thm)],[c_30119,c_41329]) ).
tcf(c_41426,plain,
( sP77(sK157)
| v__1(sortedList_first,sK157,prev_2)
| v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn)
| ~ v__1(sortedList_first,prev_2,nn) ),
inference(backward_subsumption_resolution,[status(thm)],[c_30075,c_41358]) ).
tcf(c_96207,plain,
( iPr_def_12
| sP59
| v__1(sortedList_first,prev_2,nn) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_918]) ).
tcf(c_96246,plain,
! [X0: $i] :
( ~ iPr_def_20
| ~ sP57(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_20])],[c_248]) ).
tcf(c_96248,plain,
( iPr_def_20
| v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_247]) ).
tcf(c_96249,plain,
! [X0: $i] :
( ~ iPr_def_21
| ~ sP58(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_21])],[c_242]) ).
tcf(c_96251,plain,
( iPr_def_21
| v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_241]) ).
tcf(c_96253,plain,
( sP77(sK157)
| v__1(sortedList_first,sK157,prev_2)
| v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn)
| ~ v__1(sortedList_first,prev_2,nn) ),
inference(demodulation,[status(thm)],[c_41426]) ).
tcf(c_96255,plain,
( sP77(sK157)
| v__1(sortedList_first,sK157,prev_2)
| v__1(sortedList_first,nn,prev_2)
| ~ v__1(sortedList_first,prev_2,nn) ),
inference(demodulation,[status(thm)],[c_41417]) ).
tcf(c_96257,plain,
( sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,nn)
| v__1(sortedList_first,prev_2,nn)
| v__1(null,sK157,prev_2)
| v__1(null,nn,nn)
| ( nn = prev_2 )
| ~ v__1(sortedList_first,nn,prev_2)
| ~ v__1(null,prev_2,prev_2) ),
inference(demodulation,[status(thm)],[c_30545]) ).
tcf(c_96262,plain,
( sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,nn)
| v__1(null,sK157,sK157) ),
inference(demodulation,[status(thm)],[c_8669]) ).
tcf(c_96265,plain,
( sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,sK157)
| ( nn != sK157 ) ),
inference(demodulation,[status(thm)],[c_8619]) ).
tcf(c_96266,plain,
( sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,sK157)
| v__1(null,sK157,sK157)
| v__1(null,sK157,nn) ),
inference(demodulation,[status(thm)],[c_7050]) ).
tcf(c_96268,negated_conjecture,
( ( nn = sK157 )
| ~ v__1(sortedList_first,sK157,sK157) ),
inference(demodulation,[status(thm)],[c_898]) ).
tcf(c_96269,negated_conjecture,
null != sK157,
inference(demodulation,[status(thm)],[c_568]) ).
tcf(c_96270,negated_conjecture,
object(sK157),
inference(demodulation,[status(thm)],[c_567]) ).
tcf(c_96271,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_96273,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_96278,plain,
! [X0: $i,X1: $i] :
( ( node_key(X0) = node_key(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_96280,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( v__1(X0,X2,X4)
| ~ v__1(X1,X3,X5)
| ( X4 != X5 )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_96284,plain,
! [X0: $i,X1: $i] :
( sP76(X0)
| ~ sP76(X1)
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_96294,plain,
( ( node_key(nn) = node_key(nn) )
| ( nn != nn ) ),
inference(instantiation,[status(thm)],[c_96278]) ).
tcf(c_101285,plain,
( sP76(sK157)
| sP77(sK157)
| v__1(null,sK157,sK157)
| v__1(null,sK157,nn)
| ( nn = sK157 ) ),
inference(superposition,[status(thm)],[c_96266,c_96268]) ).
tcf(c_101498,plain,
( v__1(prev_2,nn,nn)
| ~ object(prev_2) ),
inference(superposition,[status(thm)],[c_815,c_911]) ).
tcf(c_101500,plain,
v__1(prev_2,nn,nn),
inference(forward_subsumption_resolution,[status(thm)],[c_101498,c_58]) ).
tcf(c_101637,plain,
( v__1(sortedList_first,node_next(sortedList_first),nn)
| ( nn = sortedList_first )
| ~ object(sortedList_first)
| ~ object(nn) ),
inference(superposition,[status(thm)],[c_889,c_953]) ).
tcf(c_101640,plain,
( sP76(sK157)
| sP77(sK157)
| v__1(null,sK157,sK157)
| v__1(null,sK157,nn)
| v__1(sortedList_first,node_next(sortedList_first),sK157)
| ( sortedList_first = sK157 )
| ~ object(sK157)
| ~ object(sortedList_first) ),
inference(superposition,[status(thm)],[c_96266,c_953]) ).
tcf(c_101641,plain,
( sP76(sK157)
| sP77(sK157)
| v__1(null,sK157,nn)
| v__1(null,node_next(null),sK157)
| ( null = sK157 )
| ( nn = sK157 )
| ~ object(sK157)
| ~ object(null) ),
inference(superposition,[status(thm)],[c_101285,c_953]) ).
tcf(c_101648,plain,
( v__1(sortedList_first,node_next(sortedList_first),nn)
| ( nn = sortedList_first ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_101637,c_63,c_56]) ).
tcf(c_101655,plain,
( sP76(sK157)
| sP77(sK157)
| v__1(null,sK157,nn)
| v__1(null,null,sK157)
| ( null = sK157 )
| ( nn = sK157 )
| ~ object(sK157)
| ~ object(null) ),
inference(light_normalisation,[status(thm)],[c_101641,c_125]) ).
tcf(c_101656,plain,
( sP76(sK157)
| sP77(sK157)
| v__1(null,sK157,nn)
| v__1(null,null,sK157)
| ( nn = sK157 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_101655,c_96269,c_96270,c_61]) ).
tcf(c_101662,plain,
( sP76(sK157)
| sP77(sK157)
| v__1(null,sK157,sK157)
| v__1(null,sK157,nn)
| v__1(sortedList_first,node_next(sortedList_first),sK157)
| ( sortedList_first = sK157 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_101640,c_96270,c_63]) ).
tcf(c_101782,plain,
! [X0: $i] :
( ( X0 = null )
| ~ object(X0)
| ~ v__1(sortedList_first,X0,X0)
| ~ v__1(node_next(X0),X0,X0) ),
inference(equality_resolution,[status(thm)],[c_977]) ).
tcf(c_102171,plain,
( iPr_def_12
| sP59
| sP77(sK157)
| v__1(sortedList_first,sK157,prev_2)
| v__1(sortedList_first,nn,prev_2) ),
inference(superposition,[status(thm)],[c_96207,c_96255]) ).
tcf(c_102217,plain,
( sP77(sK157)
| v__1(sortedList_first,sK157,prev_2)
| v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn)
| ~ sP58(prev_2) ),
inference(superposition,[status(thm)],[c_240,c_96253]) ).
tcf(c_102320,plain,
( iPr_def_12
| v__1(sortedList_first,nn,prev_2)
| v__1(sortedList_first,sK157,prev_2)
| sP77(sK157) ),
inference(global_subsumption_just,[status(thm)],[c_102171,c_855,c_102171]) ).
tcf(c_102321,plain,
( iPr_def_12
| sP77(sK157)
| v__1(sortedList_first,sK157,prev_2)
| v__1(sortedList_first,nn,prev_2) ),
inference(renaming,[status(thm)],[c_102320]) ).
tcf(c_102493,plain,
( ( prev_2 = null )
| ~ object(prev_2)
| ~ v__1(sortedList_first,prev_2,prev_2)
| ~ v__1(nn,prev_2,prev_2) ),
inference(superposition,[status(thm)],[c_815,c_101782]) ).
tcf(c_102494,plain,
~ v__1(nn,prev_2,prev_2),
inference(forward_subsumption_resolution,[status(thm)],[c_102493,c_79,c_58,c_971]) ).
tcf(c_103424,plain,
( sP57(nn)
| sP58(nn)
| sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,nn)
| v__1(sortedList_first,prev_2,nn)
| v__1(null,sK157,prev_2)
| v__1(null,nn,nn)
| ( nn = prev_2 )
| ~ sP76(nn)
| ~ v__1(null,prev_2,prev_2) ),
inference(superposition,[status(thm)],[c_137,c_96257]) ).
tcf(c_103580,plain,
( ~ sP76(nn)
| v__1(sortedList_first,prev_2,nn) ),
inference(global_subsumption_just,[status(thm)],[c_103424,c_9660]) ).
tcf(c_103581,plain,
( v__1(sortedList_first,prev_2,nn)
| ~ sP76(nn) ),
inference(renaming,[status(thm)],[c_103580]) ).
tcf(c_103587,plain,
( sP77(sK157)
| v__1(sortedList_first,sK157,prev_2)
| v__1(sortedList_first,nn,prev_2)
| ~ sP76(nn) ),
inference(superposition,[status(thm)],[c_103581,c_96255]) ).
tcf(c_103598,plain,
( v__1(sortedList_first,nn,prev_2)
| ~ sP76(nn) ),
inference(global_subsumption_just,[status(thm)],[c_103587,c_8806]) ).
tcf(c_105260,plain,
( ( null = sortedList_first )
| ~ object(prev_2)
| ( nn != sortedList_first ) ),
inference(superposition,[status(thm)],[c_815,c_103]) ).
tcf(c_105261,plain,
( ( null = sortedList_first )
| ( nn != sortedList_first ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_105260,c_58]) ).
tcf(c_105471,plain,
( sP31(nn)
| sP32(nn)
| sP33(nn)
| sP77(sK157)
| v__1(sortedList_first,sK157,prev_2)
| v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn)
| ~ sP77(nn) ),
inference(superposition,[status(thm)],[c_128,c_96253]) ).
tcf(c_105472,plain,
( sP31(nn)
| sP32(nn)
| sP33(nn)
| sP77(sK157)
| v__1(sortedList_first,sK157,prev_2)
| v__1(sortedList_first,nn,prev_2)
| ~ sP77(nn) ),
inference(superposition,[status(thm)],[c_128,c_96255]) ).
tcf(c_105474,plain,
( sP31(nn)
| sP77(sK157)
| v__1(sortedList_first,sK157,prev_2)
| v__1(sortedList_first,nn,prev_2)
| ~ sP77(nn) ),
inference(forward_subsumption_resolution,[status(thm)],[c_105472,c_383,c_377]) ).
tcf(c_105480,plain,
( sP31(nn)
| sP77(sK157)
| v__1(sortedList_first,sK157,prev_2)
| v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn)
| ~ sP77(nn) ),
inference(forward_subsumption_resolution,[status(thm)],[c_105471,c_383,c_377]) ).
tcf(c_105574,plain,
( sP76(sK157)
| sP77(sK157)
| v__1(null,sK157,sK157)
| v__1(null,sK157,nn)
| ~ sP31(sK157)
| ~ v__1(sortedList_first,sK157,nn) ),
inference(superposition,[status(thm)],[c_96266,c_392]) ).
tcf(c_105663,plain,
( sP76(sK157)
| sP77(sK157)
| v__1(null,sK157,sK157)
| v__1(null,sK157,nn)
| ~ sP31(sK157) ),
inference(global_subsumption_just,[status(thm)],[c_105574,c_8669,c_105574]) ).
tcf(c_105711,plain,
( ~ sP77(nn)
| v__1(sortedList_first,nn,prev_2)
| v__1(sortedList_first,sK157,prev_2)
| sP77(sK157) ),
inference(global_subsumption_just,[status(thm)],[c_105474,c_104,c_89,c_743,c_105474]) ).
tcf(c_105712,plain,
( sP77(sK157)
| v__1(sortedList_first,sK157,prev_2)
| v__1(sortedList_first,nn,prev_2)
| ~ sP77(nn) ),
inference(renaming,[status(thm)],[c_105711]) ).
tcf(c_105721,plain,
( ~ sP77(nn)
| v__1(null,prev_2,nn)
| v__1(null,prev_2,prev_2)
| v__1(sortedList_first,sK157,prev_2)
| sP77(sK157) ),
inference(global_subsumption_just,[status(thm)],[c_105480,c_104,c_89,c_743,c_105480]) ).
tcf(c_105722,plain,
( sP77(sK157)
| v__1(sortedList_first,sK157,prev_2)
| v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn)
| ~ sP77(nn) ),
inference(renaming,[status(thm)],[c_105721]) ).
tcf(c_106469,plain,
! [X0: $i] :
( v__1(null,X0,X0)
| ~ object(null)
| ~ object(nn)
| ~ sP26(X0)
| ~ object(X0) ),
inference(superposition,[status(thm)],[c_421,c_72]) ).
tcf(c_106502,plain,
! [X0: $i] :
( v__1(null,X0,X0)
| ~ object(null)
| ~ object(prev_2)
| ~ sP57(X0)
| ~ object(X0) ),
inference(superposition,[status(thm)],[c_246,c_72]) ).
tcf(c_106542,plain,
( sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,sK157)
| v__1(null,sK157,sK157)
| ~ object(sK157)
| ~ object(sortedList_first)
| ~ object(nn) ),
inference(superposition,[status(thm)],[c_96262,c_72]) ).
tcf(c_106546,plain,
( sP77(sK157)
| v__1(sortedList_first,sK157,sK157)
| v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn)
| ~ sP77(nn)
| ~ object(sK157)
| ~ object(sortedList_first)
| ~ object(prev_2) ),
inference(superposition,[status(thm)],[c_105722,c_72]) ).
tcf(c_106547,plain,
( sP77(sK157)
| v__1(sortedList_first,sK157,sK157)
| v__1(sortedList_first,nn,prev_2)
| ~ sP77(nn)
| ~ object(sK157)
| ~ object(sortedList_first)
| ~ object(prev_2) ),
inference(superposition,[status(thm)],[c_105712,c_72]) ).
tcf(c_106565,plain,
( sP77(sK157)
| v__1(sortedList_first,sK157,sK157)
| v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn)
| ~ sP58(prev_2)
| ~ object(sK157)
| ~ object(sortedList_first)
| ~ object(prev_2) ),
inference(superposition,[status(thm)],[c_102217,c_72]) ).
tcf(c_106569,plain,
( iPr_def_12
| sP77(sK157)
| v__1(sortedList_first,sK157,sK157)
| v__1(sortedList_first,nn,prev_2)
| ~ object(sK157)
| ~ object(sortedList_first)
| ~ object(prev_2) ),
inference(superposition,[status(thm)],[c_102321,c_72]) ).
tcf(c_106577,plain,
( sP76(sK157)
| sP77(sK157)
| v__1(null,sK157,sK157)
| v__1(null,null,sK157)
| ( nn = sK157 )
| ~ object(sK157)
| ~ object(null)
| ~ object(nn) ),
inference(superposition,[status(thm)],[c_101656,c_72]) ).
tcf(c_106650,plain,
! [X0: $i] :
( v__1(null,X0,X0)
| ~ sP57(X0)
| ~ object(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_106502,c_61,c_58]) ).
tcf(c_106682,plain,
! [X0: $i] :
( v__1(null,X0,X0)
| ~ sP26(X0)
| ~ object(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_106469,c_61,c_56]) ).
tcf(c_106732,plain,
( iPr_def_12
| sP77(sK157)
| v__1(sortedList_first,sK157,sK157)
| v__1(sortedList_first,nn,prev_2) ),
inference(forward_subsumption_resolution,[status(thm)],[c_106569,c_96270,c_63,c_58]) ).
tcf(c_106784,plain,
( sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,sK157)
| v__1(null,sK157,sK157) ),
inference(forward_subsumption_resolution,[status(thm)],[c_106542,c_96270,c_63,c_56]) ).
tcf(c_106789,plain,
( sP77(sK157)
| v__1(sortedList_first,sK157,sK157)
| v__1(sortedList_first,nn,prev_2)
| ~ sP77(nn) ),
inference(forward_subsumption_resolution,[status(thm)],[c_106547,c_96270,c_63,c_58]) ).
tcf(c_106832,plain,
( sP76(sK157)
| sP77(sK157)
| v__1(null,sK157,sK157)
| v__1(null,null,sK157)
| ( nn = sK157 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_106577,c_96270,c_61,c_56]) ).
tcf(c_106853,plain,
( sP77(sK157)
| v__1(sortedList_first,sK157,sK157)
| v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn)
| ~ sP58(prev_2) ),
inference(forward_subsumption_resolution,[status(thm)],[c_106565,c_96270,c_63,c_58]) ).
tcf(c_106859,plain,
( sP77(sK157)
| v__1(sortedList_first,sK157,sK157)
| v__1(null,prev_2,prev_2)
| v__1(null,prev_2,nn)
| ~ sP77(nn) ),
inference(forward_subsumption_resolution,[status(thm)],[c_106546,c_96270,c_63,c_58]) ).
tcf(c_107168,plain,
( v__1(nn,prev_2,prev_2)
| ~ sP76(nn)
| ~ object(sortedList_first)
| ~ object(prev_2)
| ~ object(nn) ),
inference(superposition,[status(thm)],[c_103598,c_73]) ).
tcf(c_107183,plain,
! [X0: $i] :
( v__1(prev_2,X0,X0)
| ~ object(null)
| ~ object(prev_2)
| ~ sP32(X0)
| ~ object(X0) ),
inference(superposition,[status(thm)],[c_386,c_73]) ).
tcf(c_107202,plain,
! [X0: $i] :
( v__1(X0,nn,nn)
| ~ object(nn)
| ~ sP26(X0)
| ~ object(X0)
| ~ object(sK121(X0)) ),
inference(superposition,[status(thm)],[c_6282,c_73]) ).
tcf(c_107226,plain,
( sP77(sK157)
| v__1(sK157,prev_2,prev_2)
| v__1(sortedList_first,nn,prev_2)
| ~ sP77(nn)
| ~ object(sK157)
| ~ object(sortedList_first)
| ~ object(prev_2) ),
inference(superposition,[status(thm)],[c_105712,c_73]) ).
tcf(c_107365,plain,
! [X0: $i] :
( v__1(prev_2,X0,X0)
| ~ sP32(X0)
| ~ object(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_107183,c_61,c_58]) ).
tcf(c_107381,plain,
~ sP76(nn),
inference(forward_subsumption_resolution,[status(thm)],[c_107168,c_102494,c_63,c_58,c_56]) ).
tcf(c_107400,plain,
! [X0: $i] :
( v__1(X0,nn,nn)
| ~ sP26(X0)
| ~ object(X0)
| ~ object(sK121(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_107202,c_56]) ).
tcf(c_107550,plain,
( sP77(sK157)
| v__1(sK157,prev_2,prev_2)
| v__1(sortedList_first,nn,prev_2)
| ~ sP77(nn) ),
inference(forward_subsumption_resolution,[status(thm)],[c_107226,c_96270,c_63,c_58]) ).
tcf(c_107724,plain,
( iPr_def_12
| sP77(sK157)
| v__1(sortedList_first,nn,prev_2)
| v__1(sortedList_first,node_next(sortedList_first),sK157)
| ( sortedList_first = sK157 )
| ~ object(sK157)
| ~ object(sortedList_first) ),
inference(superposition,[status(thm)],[c_106732,c_953]) ).
tcf(c_107734,plain,
( iPr_def_12
| sP77(sK157)
| v__1(sortedList_first,nn,prev_2)
| ( nn = sK157 ) ),
inference(superposition,[status(thm)],[c_106732,c_96268]) ).
tcf(c_107779,plain,
( iPr_def_12
| sP77(sK157)
| v__1(sortedList_first,nn,prev_2)
| v__1(sortedList_first,node_next(sortedList_first),sK157)
| ( sortedList_first = sK157 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_107724,c_96270,c_63]) ).
tcf(c_107896,plain,
( iPr_def_12
| sP77(sK157)
| v__1(nn,prev_2,prev_2)
| ( nn = sK157 )
| ~ object(sortedList_first)
| ~ object(prev_2)
| ~ object(nn) ),
inference(superposition,[status(thm)],[c_107734,c_73]) ).
tcf(c_107900,plain,
( iPr_def_12
| sP77(sK157)
| ( nn = sK157 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_107896,c_102494,c_63,c_58,c_56]) ).
tcf(c_108279,plain,
! [X0: $i] :
( ( X0 = null )
| ~ object(null)
| ~ object(X0)
| ~ v__1(null,X0,X0) ),
inference(superposition,[status(thm)],[c_125,c_76]) ).
tcf(c_108281,plain,
! [X0: $i] :
( ( X0 = null )
| ~ object(X0)
| ~ v__1(null,X0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_108279,c_61]) ).
tcf(c_108290,plain,
( ( nn = null )
| ~ object(nn)
| ~ v__1(null,nn,nn) ),
inference(instantiation,[status(thm)],[c_108281]) ).
tcf(c_108429,plain,
! [X0: $i] :
( v__1(sortedList_first,sK157,sK157)
| ~ object(sK157)
| ~ object(sortedList_first)
| ~ object(X0)
| ~ v__1(sortedList_first,sK157,X0) ),
inference(instantiation,[status(thm)],[c_72]) ).
tcf(c_108430,plain,
( v__1(sortedList_first,sK157,sK157)
| ~ object(sK157)
| ~ object(sortedList_first)
| ~ object(nn)
| ~ v__1(sortedList_first,sK157,nn) ),
inference(instantiation,[status(thm)],[c_108429]) ).
tcf(c_108449,plain,
( sP76(sK157)
| sP77(sK157)
| v__1(null,sK157,sK157)
| ( nn = sK157 ) ),
inference(superposition,[status(thm)],[c_106784,c_96268]) ).
tcf(c_108604,plain,
( sP77(sK157)
| v__1(sortedList_first,nn,prev_2)
| ( nn = sK157 )
| ~ sP77(nn) ),
inference(superposition,[status(thm)],[c_106789,c_96268]) ).
tcf(c_108702,plain,
( ( null = sK157 )
| ~ object(sK157)
| ~ object(null)
| ~ v__1(null,sK157,sK157)
| ( node_next(null) != null ) ),
inference(instantiation,[status(thm)],[c_76]) ).
tcf(c_108841,plain,
! [X0: $i] :
( v__1(null,nn,nn)
| ~ object(null)
| ~ object(nn)
| ~ object(X0)
| ~ v__1(X0,nn,nn)
| ~ v__1(null,X0,X0) ),
inference(instantiation,[status(thm)],[c_66]) ).
tcf(c_108849,plain,
! [X0: $i] :
( v__1(sortedList_first,sK157,sK157)
| ~ object(sK157)
| ~ object(sortedList_first)
| ~ object(X0)
| ~ v__1(X0,sK157,sK157)
| ~ v__1(sortedList_first,X0,X0) ),
inference(instantiation,[status(thm)],[c_66]) ).
tcf(c_108850,plain,
( v__1(sortedList_first,sK157,sK157)
| ~ object(sK157)
| ~ object(sortedList_first)
| ~ object(nn)
| ~ v__1(sortedList_first,nn,nn)
| ~ v__1(nn,sK157,sK157) ),
inference(instantiation,[status(thm)],[c_108849]) ).
tcf(c_108970,plain,
! [X0: $i,X1: $i,X2: $i] :
( v__1(null,nn,nn)
| ~ v__1(X2,X0,X1)
| ( null != X2 )
| ( nn != X1 )
| ( nn != X0 ) ),
inference(instantiation,[status(thm)],[c_96280]) ).
tcf(c_108988,plain,
! [X0: $i,X1: $i,X2: $i] :
( v__1(sortedList_first,sK157,sK157)
| ~ v__1(X0,X1,X2)
| ( sK157 != X2 )
| ( sK157 != X1 )
| ( sortedList_first != X0 ) ),
inference(instantiation,[status(thm)],[c_96280]) ).
tcf(c_109131,plain,
! [X0: $i,X1: $i] :
( v__1(X0,X1,X1)
| ~ object(X1)
| ~ object(X0)
| ~ object(node_next(X0))
| ~ v__1(node_next(X0),X1,X1) ),
inference(superposition,[status(thm)],[c_911,c_66]) ).
tcf(c_109134,plain,
! [X0: $i] :
( v__1(sortedList_first,X0,X0)
| ~ object(sortedList_first)
| ~ object(prev_2)
| ~ object(X0)
| ~ v__1(prev_2,X0,X0) ),
inference(superposition,[status(thm)],[c_971,c_66]) ).
tcf(c_109159,plain,
! [X0: $i] :
( iPr_def_21
| v__1(null,prev_2,nn)
| v__1(null,X0,X0)
| ~ object(null)
| ~ object(prev_2)
| ~ object(X0)
| ~ v__1(prev_2,X0,X0) ),
inference(superposition,[status(thm)],[c_96251,c_66]) ).
tcf(c_109160,plain,
! [X0: $i] :
( iPr_def_20
| v__1(null,prev_2,nn)
| v__1(null,X0,X0)
| ~ object(null)
| ~ object(prev_2)
| ~ object(X0)
| ~ v__1(prev_2,X0,X0) ),
inference(superposition,[status(thm)],[c_96248,c_66]) ).
tcf(c_109221,plain,
! [X0: $i] :
( v__1(sortedList_first,X0,X0)
| ~ object(X0)
| ~ v__1(prev_2,X0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_109134,c_63,c_58]) ).
tcf(c_109301,plain,
! [X0: $i,X1: $i] :
( v__1(X0,X1,X1)
| ~ object(X1)
| ~ object(X0)
| ~ v__1(node_next(X0),X1,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_109131,c_64]) ).
tcf(c_109398,plain,
! [X0: $i] :
( iPr_def_20
| v__1(null,prev_2,nn)
| v__1(null,X0,X0)
| ~ object(X0)
| ~ v__1(prev_2,X0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_109160,c_61,c_58]) ).
tcf(c_109404,plain,
! [X0: $i] :
( iPr_def_21
| v__1(null,prev_2,nn)
| v__1(null,X0,X0)
| ~ object(X0)
| ~ v__1(prev_2,X0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_109159,c_61,c_58]) ).
tcf(c_109570,plain,
( iPr_def_21
| v__1(null,prev_2,nn)
| v__1(null,nn,nn)
| ~ object(nn)
| ~ v__1(prev_2,nn,nn) ),
inference(instantiation,[status(thm)],[c_109404]) ).
tcf(c_109571,plain,
( iPr_def_20
| v__1(null,prev_2,nn)
| v__1(null,nn,nn)
| ~ object(nn)
| ~ v__1(prev_2,nn,nn) ),
inference(instantiation,[status(thm)],[c_109398]) ).
tcf(c_109600,plain,
! [X0: $i] :
( v__1(null,nn,nn)
| ~ object(null)
| ~ object(nn)
| ~ object(X0)
| ~ v__1(null,X0,nn)
| ~ v__1(X0,nn,nn) ),
inference(instantiation,[status(thm)],[c_68]) ).
tcf(c_109674,plain,
! [X0: $i] :
( v__1(null,sK157,sK157)
| ~ object(sK157)
| ~ object(null)
| ~ object(X0)
| ~ v__1(null,sK157,X0) ),
inference(instantiation,[status(thm)],[c_72]) ).
tcf(c_109675,plain,
( v__1(null,sK157,sK157)
| ~ object(sK157)
| ~ object(null)
| ~ object(nn)
| ~ v__1(null,sK157,nn) ),
inference(instantiation,[status(thm)],[c_109674]) ).
tcf(c_109738,plain,
( sP77(sK157)
| v__1(nn,prev_2,prev_2)
| ( nn = sK157 )
| ~ sP77(nn)
| ~ object(sortedList_first)
| ~ object(prev_2)
| ~ object(nn) ),
inference(superposition,[status(thm)],[c_108604,c_73]) ).
tcf(c_109742,plain,
( sP77(sK157)
| ( nn = sK157 )
| ~ sP77(nn) ),
inference(forward_subsumption_resolution,[status(thm)],[c_109738,c_102494,c_63,c_58,c_56]) ).
tcf(c_110005,plain,
( sP76(sK157)
| sP77(sK157)
| ( nn = sK157 ) ),
inference(global_subsumption_just,[status(thm)],[c_106832,c_567,c_61,c_568,c_125,c_108449,c_108702]) ).
tcf(c_110013,plain,
( sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,sK157,sK157) ),
inference(backward_subsumption_resolution,[status(thm)],[c_96265,c_110005]) ).
tcf(c_110134,plain,
! [X0: $i] :
( v__1(sortedList_first,node_next(sortedList_first),X0)
| ( nn = sortedList_first )
| ~ object(sortedList_first)
| ~ object(nn)
| ~ object(X0)
| ~ object(node_next(sortedList_first))
| ~ v__1(node_next(sortedList_first),X0,nn) ),
inference(superposition,[status(thm)],[c_101648,c_67]) ).
tcf(c_110164,plain,
! [X0: $i] :
( sP77(sK157)
| v__1(sortedList_first,nn,prev_2)
| v__1(sK157,prev_2,X0)
| ~ sP77(nn)
| ~ object(sK157)
| ~ object(prev_2)
| ~ object(X0)
| ~ v__1(prev_2,X0,prev_2) ),
inference(superposition,[status(thm)],[c_107550,c_67]) ).
tcf(c_110635,plain,
! [X0: $i] :
( sP77(sK157)
| v__1(sortedList_first,nn,prev_2)
| v__1(sK157,prev_2,X0)
| ~ sP77(nn)
| ~ object(X0)
| ~ v__1(prev_2,X0,prev_2) ),
inference(forward_subsumption_resolution,[status(thm)],[c_110164,c_96270,c_58]) ).
tcf(c_110674,plain,
! [X0: $i] :
( v__1(sortedList_first,node_next(sortedList_first),X0)
| ( nn = sortedList_first )
| ~ object(X0)
| ~ v__1(node_next(sortedList_first),X0,nn) ),
inference(forward_subsumption_resolution,[status(thm)],[c_110134,c_63,c_56,c_64]) ).
tcf(c_111076,plain,
! [X0: $i] :
( v__1(sortedList_first,node_next(sortedList_first),X0)
| ( sortedList_first = X0 )
| ~ object(sortedList_first)
| ~ object(X0)
| ~ v__1(sortedList_first,X0,X0) ),
inference(instantiation,[status(thm)],[c_953]) ).
tcf(c_111095,plain,
! [X0: $i,X1: $i] :
( v__1(sortedList_first,sK157,sK157)
| ~ v__1(sortedList_first,X0,X1)
| ( sK157 != X1 )
| ( sK157 != X0 )
| ( sortedList_first != sortedList_first ) ),
inference(instantiation,[status(thm)],[c_108988]) ).
tcf(c_111096,plain,
sortedList_first = sortedList_first,
inference(instantiation,[status(thm)],[c_96271]) ).
tcf(c_111097,plain,
( v__1(sortedList_first,sK157,sK157)
| ~ v__1(sortedList_first,nn,nn)
| ( sK157 != nn )
| ( sortedList_first != sortedList_first ) ),
inference(instantiation,[status(thm)],[c_111095]) ).
tcf(c_111104,plain,
! [X0: $i] :
( sP76(X0)
| ~ sP76(sK157)
| ( X0 != sK157 ) ),
inference(instantiation,[status(thm)],[c_96284]) ).
tcf(c_111105,plain,
( sP76(nn)
| ~ sP76(sK157)
| ( nn != sK157 ) ),
inference(instantiation,[status(thm)],[c_111104]) ).
tcf(c_112975,plain,
! [X0: $i] :
( v__1(nn,nn,X0)
| ~ object(sortedList_first)
| ~ object(nn)
| ~ object(X0)
| ~ v__1(sortedList_first,nn,X0) ),
inference(superposition,[status(thm)],[c_889,c_70]) ).
tcf(c_113105,plain,
! [X0: $i] :
( v__1(nn,nn,X0)
| ~ object(X0)
| ~ v__1(sortedList_first,nn,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_112975,c_63,c_56]) ).
tcf(c_113842,plain,
( v__1(null,nn,nn)
| ~ object(null)
| ~ object(prev_2)
| ~ object(nn)
| ~ v__1(null,prev_2,nn)
| ~ v__1(prev_2,nn,nn) ),
inference(instantiation,[status(thm)],[c_109600]) ).
tcf(c_113847,plain,
! [X0: $i,X1: $i] :
( v__1(X1,prev_2,prev_2)
| ~ object(prev_2)
| ~ object(X1)
| ~ object(X0)
| ~ v__1(X0,X1,prev_2) ),
inference(instantiation,[status(thm)],[c_73]) ).
tcf(c_114045,plain,
! [X0: $i,X1: $i] :
( v__1(null,nn,nn)
| ~ v__1(sortedList_first,X0,X1)
| ( null != sortedList_first )
| ( nn != X1 )
| ( nn != X0 ) ),
inference(instantiation,[status(thm)],[c_108970]) ).
tcf(c_114046,plain,
( v__1(null,nn,nn)
| ~ v__1(sortedList_first,nn,nn)
| ( null != sortedList_first )
| ( nn != nn ) ),
inference(instantiation,[status(thm)],[c_114045]) ).
tcf(c_114405,plain,
( sP77(sK157)
| v__1(sortedList_first,sK157,sK157)
| ~ sP77(nn) ),
inference(global_subsumption_just,[status(thm)],[c_106859,c_567,c_61,c_56,c_568,c_125,c_7050,c_107381,c_108702,c_109675,c_109742,c_111105]) ).
tcf(c_114414,plain,
( sP77(sK157)
| v__1(sortedList_first,node_next(sortedList_first),sK157)
| ( sortedList_first = sK157 )
| ~ sP77(nn)
| ~ object(sK157)
| ~ object(sortedList_first) ),
inference(superposition,[status(thm)],[c_114405,c_953]) ).
tcf(c_114457,plain,
( sP77(sK157)
| v__1(sortedList_first,node_next(sortedList_first),sK157)
| ( sortedList_first = sK157 )
| ~ sP77(nn) ),
inference(forward_subsumption_resolution,[status(thm)],[c_114414,c_96270,c_63]) ).
tcf(c_114507,plain,
! [X0: $i] :
( v__1(sortedList_first,prev_2,X0)
| v__1(sortedList_first,X0,prev_2)
| ~ object(sortedList_first)
| ~ object(prev_2)
| ~ object(X0)
| ~ v__1(sortedList_first,X0,X0) ),
inference(superposition,[status(thm)],[c_971,c_71]) ).
tcf(c_114622,plain,
! [X0: $i] :
( v__1(sortedList_first,prev_2,X0)
| v__1(sortedList_first,X0,prev_2)
| ~ object(X0)
| ~ v__1(sortedList_first,X0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_114507,c_63,c_58]) ).
tcf(c_115039,plain,
( v__1(sortedList_first,prev_2,nn)
| v__1(sortedList_first,nn,prev_2)
| ~ object(nn)
| ~ v__1(sortedList_first,nn,nn) ),
inference(instantiation,[status(thm)],[c_114622]) ).
tcf(c_115153,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v__1(node_next(X1),X2,X3)
| ~ object(X3)
| ~ object(X2)
| ~ object(X0)
| ~ object(node_next(X1))
| ~ v__1(X0,X2,X3)
| ~ v__1(X0,node_next(X1),X2) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_115255,plain,
! [X0: $i] :
( sP77(sK157)
| v__1(node_next(sortedList_first),sK157,X0)
| ( sortedList_first = sK157 )
| ~ sP77(nn)
| ~ object(sK157)
| ~ object(sortedList_first)
| ~ object(X0)
| ~ object(node_next(sortedList_first))
| ~ v__1(sortedList_first,sK157,X0) ),
inference(superposition,[status(thm)],[c_114457,c_70]) ).
tcf(c_115285,plain,
! [X0: $i] :
( sP77(sK157)
| v__1(node_next(sortedList_first),sK157,X0)
| ( sortedList_first = sK157 )
| ~ sP77(nn)
| ~ object(X0)
| ~ v__1(sortedList_first,sK157,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_115255,c_96270,c_63,c_64]) ).
tcf(c_115500,plain,
( iPr_def_12
| sP77(sK157)
| ( sortedList_first = sK157 )
| v__1(sortedList_first,node_next(sortedList_first),sK157) ),
inference(global_subsumption_just,[status(thm)],[c_107779,c_567,c_61,c_56,c_568,c_125,c_101662,c_107381,c_107900,c_108702,c_109675,c_111105]) ).
tcf(c_115501,plain,
( iPr_def_12
| sP77(sK157)
| v__1(sortedList_first,node_next(sortedList_first),sK157)
| ( sortedList_first = sK157 ) ),
inference(renaming,[status(thm)],[c_115500]) ).
tcf(c_115514,plain,
( iPr_def_12
| sP77(sK157)
| v__1(node_next(sortedList_first),sK157,sK157)
| ( sortedList_first = sK157 )
| ~ object(sK157)
| ~ object(sortedList_first)
| ~ object(node_next(sortedList_first)) ),
inference(superposition,[status(thm)],[c_115501,c_73]) ).
tcf(c_115516,plain,
( iPr_def_12
| sP77(sK157)
| v__1(node_next(sortedList_first),sK157,sK157)
| ( sortedList_first = sK157 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_115514,c_96270,c_63,c_64]) ).
tcf(c_115566,plain,
! [X0: $i] :
( iPr_def_12
| sP77(sK157)
| v__1(node_next(sortedList_first),X0,sK157)
| ( sortedList_first = sK157 )
| ~ object(sK157)
| ~ object(X0)
| ~ object(node_next(sortedList_first))
| ~ v__1(sK157,X0,sK157) ),
inference(superposition,[status(thm)],[c_115516,c_68]) ).
tcf(c_115583,plain,
! [X0: $i] :
( iPr_def_12
| sP77(sK157)
| v__1(node_next(sortedList_first),X0,sK157)
| ( sortedList_first = sK157 )
| ~ object(X0)
| ~ v__1(sK157,X0,sK157) ),
inference(forward_subsumption_resolution,[status(thm)],[c_115566,c_96270,c_64]) ).
tcf(c_116230,plain,
( sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,node_next(sortedList_first),sK157)
| ( sortedList_first = sK157 )
| ~ object(sK157)
| ~ object(sortedList_first) ),
inference(superposition,[status(thm)],[c_110013,c_953]) ).
tcf(c_116231,plain,
! [X0: $i] :
( sP76(sK157)
| sP77(sK157)
| v__1(sK157,sK157,X0)
| ~ object(sK157)
| ~ object(sortedList_first)
| ~ object(X0)
| ~ v__1(sortedList_first,sK157,X0) ),
inference(superposition,[status(thm)],[c_110013,c_70]) ).
tcf(c_116260,plain,
( sP76(sK157)
| sP77(sK157)
| v__1(sortedList_first,node_next(sortedList_first),sK157)
| ( sortedList_first = sK157 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_116230,c_96270,c_63]) ).
tcf(c_116277,plain,
! [X0: $i] :
( sP76(sK157)
| sP77(sK157)
| v__1(sK157,sK157,X0)
| ~ object(X0)
| ~ v__1(sortedList_first,sK157,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_116231,c_96270,c_63]) ).
tcf(c_116391,plain,
( sP76(sK157)
| sP77(sK157)
| v__1(node_next(sortedList_first),sK157,sK157)
| ( sortedList_first = sK157 )
| ~ object(sK157)
| ~ object(sortedList_first)
| ~ object(node_next(sortedList_first)) ),
inference(superposition,[status(thm)],[c_116260,c_73]) ).
tcf(c_116393,plain,
( sP76(sK157)
| sP77(sK157)
| v__1(node_next(sortedList_first),sK157,sK157)
| ( sortedList_first = sK157 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_116391,c_96270,c_63,c_64]) ).
tcf(c_116443,plain,
! [X0: $i] :
( sP76(sK157)
| sP77(sK157)
| v__1(node_next(sortedList_first),X0,sK157)
| ( sortedList_first = sK157 )
| ~ object(sK157)
| ~ object(X0)
| ~ object(node_next(sortedList_first))
| ~ v__1(sK157,X0,sK157) ),
inference(superposition,[status(thm)],[c_116393,c_68]) ).
tcf(c_116460,plain,
! [X0: $i] :
( sP76(sK157)
| sP77(sK157)
| v__1(node_next(sortedList_first),X0,sK157)
| ( sortedList_first = sK157 )
| ~ object(X0)
| ~ v__1(sK157,X0,sK157) ),
inference(forward_subsumption_resolution,[status(thm)],[c_116443,c_96270,c_64]) ).
tcf(c_116813,plain,
( v__1(null,sK157,sK157)
| v__1(null,sK157,nn)
| ~ sP33(sK157) ),
inference(instantiation,[status(thm)],[c_381]) ).
tcf(c_117193,plain,
! [X0: $i] :
( ~ v__1(sortedList_first,sK157,X0)
| ~ object(X0)
| v__1(sK157,sK157,X0)
| sP77(sK157) ),
inference(global_subsumption_just,[status(thm)],[c_116277,c_567,c_63,c_568,c_575,c_107381,c_108429,c_111105,c_116277]) ).
tcf(c_117194,plain,
! [X0: $i] :
( sP77(sK157)
| v__1(sK157,sK157,X0)
| ~ object(X0)
| ~ v__1(sortedList_first,sK157,X0) ),
inference(renaming,[status(thm)],[c_117193]) ).
tcf(c_117658,plain,
sK157 = sK157,
inference(instantiation,[status(thm)],[c_96271]) ).
tcf(c_117660,plain,
! [X0: $i,X1: $i] :
( ( sK157 = X0 )
| ( sK157 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_96273]) ).
tcf(c_118322,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( v__1(X0,X2,sK157)
| ~ v__1(X1,X3,X4)
| ( sK157 != X4 )
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_96280]) ).
tcf(c_118323,plain,
( v__1(nn,nn,sK157)
| ~ v__1(nn,nn,nn)
| ( sK157 != nn )
| ( nn != nn ) ),
inference(instantiation,[status(thm)],[c_118322]) ).
tcf(c_118458,plain,
( v__1(sortedList_first,node_next(sortedList_first),sK157)
| ( sortedList_first = sK157 )
| ~ object(sK157)
| ~ object(sortedList_first)
| ~ v__1(sortedList_first,sK157,sK157) ),
inference(instantiation,[status(thm)],[c_111076]) ).
tcf(c_118744,plain,
( v__1(sK157,sK157,sK157)
| ~ object(sK157) ),
inference(instantiation,[status(thm)],[c_74]) ).
tcf(c_118874,plain,
( sP77(sK157)
| v__1(sortedList_first,sK157,sK157)
| v__1(null,prev_2,prev_2)
| ~ sP58(prev_2) ),
inference(global_subsumption_just,[status(thm)],[c_106853,c_61,c_58,c_56,c_104,c_101500,c_106853,c_108290,c_113842]) ).
tcf(c_118900,plain,
( sP77(sK157)
| v__1(sK157,sK157,sK157)
| v__1(null,prev_2,prev_2)
| ~ sP58(prev_2)
| ~ object(sK157) ),
inference(superposition,[status(thm)],[c_118874,c_117194]) ).
tcf(c_118905,plain,
( sP77(sK157)
| v__1(sK157,sK157,sK157)
| v__1(null,prev_2,prev_2)
| ~ sP58(prev_2) ),
inference(forward_subsumption_resolution,[status(thm)],[c_118900,c_96270]) ).
tcf(c_119027,plain,
( sP77(sK157)
| v__1(sortedList_first,sK157,prev_2)
| v__1(sortedList_first,nn,prev_2) ),
inference(global_subsumption_just,[status(thm)],[c_96255,c_56,c_104,c_89,c_41417,c_115039]) ).
tcf(c_120625,plain,
v__1(sK157,sK157,sK157),
inference(global_subsumption_just,[status(thm)],[c_118905,c_567,c_118744]) ).
tcf(c_120682,plain,
! [X0: $i] : ~ sP57(X0),
inference(global_subsumption_just,[status(thm)],[c_106650,c_61,c_58,c_56,c_104,c_96246,c_101500,c_108290,c_109571,c_113842]) ).
tcf(c_120685,plain,
! [X0: $i] :
( sP58(X0)
| v__1(sortedList_first,X0,prev_2)
| ~ sP76(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_137,c_120682]) ).
tcf(c_120698,plain,
! [X0: $i] :
( ~ sP76(X0)
| v__1(sortedList_first,X0,prev_2) ),
inference(global_subsumption_just,[status(thm)],[c_120685,c_61,c_58,c_56,c_104,c_137,c_96246,c_96249,c_101500,c_108290,c_109570,c_109571,c_113842]) ).
tcf(c_120699,plain,
! [X0: $i] :
( v__1(sortedList_first,X0,prev_2)
| ~ sP76(X0) ),
inference(renaming,[status(thm)],[c_120698]) ).
tcf(c_120712,plain,
! [X0: $i] :
( v__1(sortedList_first,X0,X0)
| ~ object(sortedList_first)
| ~ object(prev_2)
| ~ sP76(X0)
| ~ object(X0) ),
inference(superposition,[status(thm)],[c_120699,c_72]) ).
tcf(c_120726,plain,
! [X0: $i] :
( v__1(sortedList_first,X0,X0)
| ~ sP76(X0)
| ~ object(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_120712,c_63,c_58]) ).
tcf(c_125743,plain,
! [X0: $i] :
( ~ object(X0)
| ~ sP26(X0) ),
inference(global_subsumption_just,[status(thm)],[c_106682,c_61,c_56,c_104,c_6290,c_106682,c_107400,c_108290,c_108841]) ).
tcf(c_125744,plain,
! [X0: $i] :
( ~ sP26(X0)
| ~ object(X0) ),
inference(renaming,[status(thm)],[c_125743]) ).
tcf(c_125805,plain,
~ sP26(sK157),
inference(superposition,[status(thm)],[c_96270,c_125744]) ).
tcf(c_129226,plain,
( v__1(nn,prev_2,prev_2)
| ~ object(sortedList_first)
| ~ object(prev_2)
| ~ object(nn)
| ~ v__1(sortedList_first,nn,prev_2) ),
inference(instantiation,[status(thm)],[c_113847]) ).
tcf(c_131186,plain,
( sP77(sK157)
| v__1(sortedList_first,sK157,sK157)
| v__1(sortedList_first,nn,prev_2)
| ~ object(sK157)
| ~ object(sortedList_first)
| ~ object(prev_2) ),
inference(superposition,[status(thm)],[c_119027,c_72]) ).
tcf(c_131276,plain,
( sP77(sK157)
| v__1(sortedList_first,sK157,sK157)
| v__1(sortedList_first,nn,prev_2) ),
inference(forward_subsumption_resolution,[status(thm)],[c_131186,c_96270,c_63,c_58]) ).
tcf(c_131416,plain,
! [X0: $i] :
( ~ v__1(sK157,X0,sK157)
| ~ object(X0)
| ( sortedList_first = sK157 )
| v__1(node_next(sortedList_first),X0,sK157)
| sP77(sK157) ),
inference(global_subsumption_just,[status(thm)],[c_115583,c_63,c_58,c_56,c_568,c_575,c_102494,c_107381,c_111105,c_116460,c_129226,c_131276]) ).
tcf(c_131417,plain,
! [X0: $i] :
( sP77(sK157)
| v__1(node_next(sortedList_first),X0,sK157)
| ( sortedList_first = sK157 )
| ~ object(X0)
| ~ v__1(sK157,X0,sK157) ),
inference(renaming,[status(thm)],[c_131416]) ).
tcf(c_131439,plain,
( sP77(sK157)
| v__1(sortedList_first,sK157,sK157)
| ( sortedList_first = sK157 )
| ~ object(sK157)
| ~ object(sortedList_first)
| ~ v__1(sK157,sK157,sK157) ),
inference(superposition,[status(thm)],[c_131417,c_109301]) ).
tcf(c_131447,plain,
( sP77(sK157)
| v__1(sortedList_first,sK157,sK157)
| ( sortedList_first = sK157 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_131439,c_96270,c_63,c_120625]) ).
tcf(c_131517,plain,
( sP77(sK157)
| v__1(sortedList_first,sK157,sK157) ),
inference(global_subsumption_just,[status(thm)],[c_131447,c_63,c_58,c_56,c_102494,c_129226,c_131276]) ).
tcf(c_131537,plain,
( sP77(sK157)
| v__1(sortedList_first,nn,sK157)
| ~ sP33(sK157) ),
inference(superposition,[status(thm)],[c_131517,c_379]) ).
tcf(c_133024,plain,
~ sP33(sK157),
inference(global_subsumption_just,[status(thm)],[c_131537,c_567,c_61,c_56,c_568,c_125,c_108702,c_109675,c_116813]) ).
tcf(c_134079,plain,
! [X0: $i] :
( v__1(sortedList_first,X0,X0)
| ~ sP32(X0)
| ~ object(X0) ),
inference(superposition,[status(thm)],[c_107365,c_109221]) ).
tcf(c_135496,plain,
( ( nn = sK157 )
| ~ sP76(sK157)
| ~ object(sK157) ),
inference(superposition,[status(thm)],[c_120726,c_96268]) ).
tcf(c_135503,plain,
( ( nn = sK157 )
| ~ sP76(sK157) ),
inference(forward_subsumption_resolution,[status(thm)],[c_135496,c_96270]) ).
tcf(c_136110,plain,
( sP77(sK157)
| v__1(sK157,prev_2,prev_2)
| v__1(sortedList_first,nn,prev_2)
| ~ object(sK157)
| ~ object(sortedList_first)
| ~ object(prev_2) ),
inference(superposition,[status(thm)],[c_119027,c_73]) ).
tcf(c_136228,plain,
( sP77(sK157)
| v__1(sK157,prev_2,prev_2)
| v__1(sortedList_first,nn,prev_2) ),
inference(forward_subsumption_resolution,[status(thm)],[c_136110,c_96270,c_63,c_58]) ).
tcf(c_136380,plain,
~ sP76(sK157),
inference(global_subsumption_just,[status(thm)],[c_135503,c_107381,c_111105,c_135503]) ).
tcf(c_137574,plain,
! [X0: $i] :
( sP77(sK157)
| ~ v__1(prev_2,X0,prev_2)
| ~ object(X0)
| ~ sP77(nn)
| v__1(sK157,prev_2,X0) ),
inference(global_subsumption_just,[status(thm)],[c_110635,c_63,c_58,c_56,c_102494,c_110635,c_129226]) ).
tcf(c_137575,plain,
! [X0: $i] :
( sP77(sK157)
| v__1(sK157,prev_2,X0)
| ~ sP77(nn)
| ~ object(X0)
| ~ v__1(prev_2,X0,prev_2) ),
inference(renaming,[status(thm)],[c_137574]) ).
tcf(c_137587,plain,
( sP77(sK157)
| v__1(sK157,prev_2,prev_2)
| ~ sP77(nn)
| ~ object(prev_2) ),
inference(superposition,[status(thm)],[c_74,c_137575]) ).
tcf(c_137592,plain,
( sP77(sK157)
| v__1(sK157,prev_2,prev_2)
| ~ sP77(nn) ),
inference(forward_subsumption_resolution,[status(thm)],[c_137587,c_58]) ).
tcf(c_137596,plain,
( sP77(sK157)
| v__1(sK157,prev_2,prev_2) ),
inference(global_subsumption_just,[status(thm)],[c_137592,c_63,c_58,c_56,c_102494,c_129226,c_136228]) ).
tcf(c_138571,plain,
! [X0: $i] :
( v__1(sortedList_first,node_next(sortedList_first),X0)
| ~ v__1(node_next(sortedList_first),X0,nn)
| ~ object(X0) ),
inference(global_subsumption_just,[status(thm)],[c_110674,c_56,c_104,c_637,c_89,c_776,c_105261,c_108290,c_110674,c_114046]) ).
tcf(c_138572,plain,
! [X0: $i] :
( v__1(sortedList_first,node_next(sortedList_first),X0)
| ~ object(X0)
| ~ v__1(node_next(sortedList_first),X0,nn) ),
inference(renaming,[status(thm)],[c_138571]) ).
tcf(c_140440,plain,
( ( nn = sK157 )
| ~ sP32(sK157)
| ~ object(sK157) ),
inference(superposition,[status(thm)],[c_134079,c_96268]) ).
tcf(c_140447,plain,
( ( nn = sK157 )
| ~ sP32(sK157) ),
inference(forward_subsumption_resolution,[status(thm)],[c_140440,c_96270]) ).
tcf(c_140865,plain,
! [X0: $i,X1: $i] :
( v__1(node_next(sortedList_first),X0,X1)
| ~ object(sortedList_first)
| ~ object(X1)
| ~ object(X0)
| ~ object(node_next(sortedList_first))
| ~ v__1(sortedList_first,X0,X1)
| ~ v__1(sortedList_first,node_next(sortedList_first),X0) ),
inference(instantiation,[status(thm)],[c_115153]) ).
tcf(c_145136,plain,
object(node_next(sortedList_first)),
inference(instantiation,[status(thm)],[c_64]) ).
tcf(c_146493,plain,
! [X0: $i] :
( ( sK157 = X0 )
| ( sK157 != sK157 )
| ( X0 != sK157 ) ),
inference(instantiation,[status(thm)],[c_117660]) ).
tcf(c_146494,plain,
( ( sK157 = nn )
| ( sK157 != sK157 )
| ( nn != sK157 ) ),
inference(instantiation,[status(thm)],[c_146493]) ).
tcf(c_147138,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v__1(sK157,X0,X0)
| ~ v__1(X3,X1,X2)
| ( sK157 != X3 )
| ( X0 != X2 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_96280]) ).
tcf(c_147139,plain,
( v__1(sK157,nn,nn)
| ~ v__1(nn,nn,nn)
| ( sK157 != nn )
| ( nn != nn ) ),
inference(instantiation,[status(thm)],[c_147138]) ).
tcf(c_149191,plain,
! [X0: $i] :
( v__1(node_next(sortedList_first),sK157,X0)
| ~ object(sK157)
| ~ object(sortedList_first)
| ~ object(X0)
| ~ object(node_next(sortedList_first))
| ~ v__1(sortedList_first,sK157,X0)
| ~ v__1(sortedList_first,node_next(sortedList_first),sK157) ),
inference(instantiation,[status(thm)],[c_140865]) ).
tcf(c_150136,plain,
! [X0: $i] :
( ~ object(X0)
| ~ v__1(sortedList_first,sK157,X0)
| ( sortedList_first = sK157 )
| v__1(node_next(sortedList_first),sK157,X0) ),
inference(global_subsumption_just,[status(thm)],[c_115285,c_567,c_63,c_108429,c_118458,c_145136,c_149191]) ).
tcf(c_150137,plain,
! [X0: $i] :
( v__1(node_next(sortedList_first),sK157,X0)
| ( sortedList_first = sK157 )
| ~ object(X0)
| ~ v__1(sortedList_first,sK157,X0) ),
inference(renaming,[status(thm)],[c_150136]) ).
tcf(c_150164,plain,
( v__1(sortedList_first,node_next(sortedList_first),sK157)
| ( sortedList_first = sK157 )
| ~ object(sK157)
| ~ object(nn)
| ~ v__1(sortedList_first,sK157,nn) ),
inference(superposition,[status(thm)],[c_150137,c_138572]) ).
tcf(c_150172,plain,
( v__1(sortedList_first,node_next(sortedList_first),sK157)
| ( sortedList_first = sK157 )
| ~ v__1(sortedList_first,sK157,nn) ),
inference(forward_subsumption_resolution,[status(thm)],[c_150164,c_96270,c_56]) ).
tcf(c_150279,plain,
( v__1(node_next(sortedList_first),sK157,sK157)
| ( sortedList_first = sK157 )
| ~ object(sK157)
| ~ object(sortedList_first)
| ~ object(node_next(sortedList_first))
| ~ v__1(sortedList_first,sK157,nn) ),
inference(superposition,[status(thm)],[c_150172,c_73]) ).
tcf(c_150285,plain,
( v__1(node_next(sortedList_first),sK157,sK157)
| ( sortedList_first = sK157 )
| ~ v__1(sortedList_first,sK157,nn) ),
inference(forward_subsumption_resolution,[status(thm)],[c_150279,c_96270,c_63,c_64]) ).
tcf(c_150433,plain,
( v__1(sortedList_first,sK157,sK157)
| ( sortedList_first = sK157 )
| ~ object(sK157)
| ~ object(sortedList_first)
| ~ v__1(sortedList_first,sK157,nn) ),
inference(superposition,[status(thm)],[c_150285,c_109301]) ).
tcf(c_150437,plain,
( v__1(sortedList_first,sK157,sK157)
| ( sortedList_first = sK157 )
| ~ v__1(sortedList_first,sK157,nn) ),
inference(forward_subsumption_resolution,[status(thm)],[c_150433,c_96270,c_63]) ).
tcf(c_151085,plain,
( v__1(sortedList_first,sK157,sK157)
| ~ v__1(sortedList_first,sK157,nn) ),
inference(global_subsumption_just,[status(thm)],[c_150437,c_567,c_63,c_56,c_108430]) ).
tcf(c_151091,plain,
( sP31(sK157)
| sP32(sK157)
| sP33(sK157)
| v__1(sortedList_first,sK157,sK157)
| ~ sP77(sK157) ),
inference(superposition,[status(thm)],[c_944,c_151085]) ).
tcf(c_151094,plain,
( sP31(sK157)
| sP32(sK157)
| v__1(sortedList_first,sK157,sK157)
| ~ sP77(sK157) ),
inference(forward_subsumption_resolution,[status(thm)],[c_151091,c_133024]) ).
tcf(c_151248,plain,
( sP31(sK157)
| v__1(sortedList_first,sK157,sK157) ),
inference(global_subsumption_just,[status(thm)],[c_151094,c_567,c_61,c_56,c_568,c_125,c_104,c_89,c_7050,c_108702,c_109675,c_111097,c_111096,c_117658,c_136380,c_140447,c_146494,c_151094]) ).
tcf(c_151269,plain,
( sP31(sK157)
| v__1(sortedList_first,nn,sK157)
| ~ sP65(sK157) ),
inference(superposition,[status(thm)],[c_151248,c_200]) ).
tcf(c_151270,plain,
( sP31(sK157)
| ( nn = sK157 ) ),
inference(superposition,[status(thm)],[c_151248,c_96268]) ).
tcf(c_152184,plain,
( sP31(sK157)
| v__1(nn,nn,sK157)
| ~ sP65(sK157)
| ~ object(sK157) ),
inference(superposition,[status(thm)],[c_151269,c_113105]) ).
tcf(c_152188,plain,
( sP31(sK157)
| v__1(nn,nn,sK157)
| ~ sP65(sK157) ),
inference(forward_subsumption_resolution,[status(thm)],[c_152184,c_96270]) ).
tcf(c_152705,plain,
( sP31(sK157)
| v__1(nn,nn,sK157) ),
inference(global_subsumption_just,[status(thm)],[c_152188,c_56,c_637,c_776,c_117658,c_118323,c_146494,c_151270]) ).
tcf(c_152715,plain,
( sP31(sK157)
| v__1(nn,sK157,sK157)
| ~ object(sK157)
| ~ object(nn) ),
inference(superposition,[status(thm)],[c_152705,c_73]) ).
tcf(c_152717,plain,
( sP31(sK157)
| v__1(nn,sK157,sK157) ),
inference(forward_subsumption_resolution,[status(thm)],[c_152715,c_96270,c_56]) ).
tcf(c_152783,plain,
! [X0: $i] :
( sP31(sK157)
| v__1(nn,X0,X0)
| ~ object(sK157)
| ~ object(nn)
| ~ object(X0)
| ~ v__1(sK157,X0,X0) ),
inference(superposition,[status(thm)],[c_152717,c_66]) ).
tcf(c_152817,plain,
! [X0: $i] :
( sP31(sK157)
| v__1(nn,X0,X0)
| ~ object(X0)
| ~ v__1(sK157,X0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_152783,c_96270,c_56]) ).
tcf(c_152859,plain,
( v__1(null,sK157,sK157)
| ~ sP25(sK157) ),
inference(instantiation,[status(thm)],[c_427]) ).
tcf(c_155573,plain,
( sP31(sK157)
| sP77(sK157)
| v__1(nn,prev_2,prev_2)
| ~ object(prev_2) ),
inference(superposition,[status(thm)],[c_137596,c_152817]) ).
tcf(c_155587,plain,
( sP31(sK157)
| sP77(sK157) ),
inference(forward_subsumption_resolution,[status(thm)],[c_155573,c_102494,c_58]) ).
tcf(c_155859,plain,
sP77(sK157),
inference(global_subsumption_just,[status(thm)],[c_155587,c_567,c_61,c_56,c_568,c_125,c_105663,c_108702,c_109675,c_136380,c_155587]) ).
tcf(c_155861,plain,
( sP25(sK157)
| sP26(sK157)
| ( node_next(nn) = sK113(sK157) ) ),
inference(superposition,[status(thm)],[c_155859,c_6929]) ).
tcf(c_155865,plain,
( sP25(sK157)
| ( node_next(nn) = sK113(sK157) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_155861,c_125805]) ).
tcf(c_156170,plain,
node_next(nn) = sK113(sK157),
inference(global_subsumption_just,[status(thm)],[c_155865,c_567,c_61,c_568,c_125,c_108702,c_152859,c_155865]) ).
tcf(c_156175,plain,
( sP25(sK157)
| sP26(sK157)
| v__1(node_next(nn),sK157,sK157)
| ~ sP77(sK157) ),
inference(superposition,[status(thm)],[c_156170,c_6944]) ).
tcf(c_156177,plain,
( sP25(sK157)
| v__1(node_next(nn),sK157,sK157) ),
inference(forward_subsumption_resolution,[status(thm)],[c_156175,c_125805,c_155859]) ).
tcf(c_156566,plain,
v__1(node_next(nn),sK157,sK157),
inference(global_subsumption_just,[status(thm)],[c_156177,c_567,c_61,c_568,c_125,c_108702,c_152859,c_156177]) ).
tcf(c_156569,plain,
! [X0: $i] :
( v__1(node_next(nn),X0,X0)
| ~ object(sK157)
| ~ object(X0)
| ~ object(node_next(nn))
| ~ v__1(sK157,X0,X0) ),
inference(superposition,[status(thm)],[c_156566,c_66]) ).
tcf(c_156578,plain,
( v__1(nn,sK157,sK157)
| ~ object(sK157)
| ~ object(nn) ),
inference(superposition,[status(thm)],[c_156566,c_109301]) ).
tcf(c_156580,plain,
v__1(nn,sK157,sK157),
inference(forward_subsumption_resolution,[status(thm)],[c_156578,c_96270,c_56]) ).
tcf(c_156599,plain,
! [X0: $i] :
( v__1(node_next(nn),X0,X0)
| ~ object(X0)
| ~ v__1(sK157,X0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_156569,c_96270,c_64]) ).
tcf(c_156608,plain,
( v__1(node_next(nn),nn,nn)
| ~ object(nn)
| ~ v__1(sK157,nn,nn) ),
inference(instantiation,[status(thm)],[c_156599]) ).
tcf(c_156609,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_156608,c_156580,c_147139,c_146494,c_117658,c_108850,c_96294,c_979,c_776,c_575,c_89,c_637,c_104,c_568,c_56,c_63,c_567]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW095+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.37 % Computer : n017.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 21:33:47 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.14/0.41 Running first-order theorem proving
% 0.14/0.41 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.42
% 0.14/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.14/0.42
% 0.14/0.42 % Detected problem language: tptp
% 0.14/0.43 % Proving...
% 46.00/7.41 % SZS status Started for theBenchmark.p
% 46.00/7.41 % SZS status Theorem for theBenchmark.p
% 46.00/7.41
% 46.00/7.41 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 46.00/7.41
% 46.00/7.41 % ------ iProver source info
% 46.00/7.41
% 46.00/7.41 % git: date: 2026-07-19 20:42:38 +0200
% 46.00/7.41 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 46.00/7.41 % git: non_committed_changes: false
% 46.00/7.41
% 46.00/7.41 % ------ Parsing...
% 46.00/7.41 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 46.00/7.41
% 46.00/7.41 % ------ Preprocessing... sup_sim: 4 sf_s rm: 23 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe:16:0s pe_e sup_sim: 0 sf_s rm: 18 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 12 0s sf_e pe_s pe_e %
% 46.00/7.41
% 46.00/7.41 % ------ Preprocessing... gs_s sp: 42 0s gs_e snvd_s sp: 0 0s snvd_e %
% 46.00/7.41
% 46.00/7.41 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 46.00/7.41 % ------ Proving...
% 46.00/7.41 % ------ Problem Properties
% 46.00/7.41
% 46.00/7.41 %
% 46.00/7.41 % clauses 408
% 46.00/7.41 % conjectures 3
% 46.00/7.41 % EPR 258
% 46.00/7.41 % Horn 257
% 46.00/7.41 % unary 35
% 46.00/7.41 % binary 182
% 46.00/7.41 % lits 1171
% 46.00/7.41 % lits eq 143
% 46.00/7.41 % fd_pure 0
% 46.00/7.41 % fd_pseudo 0
% 46.00/7.41 % fd_cond 13
% 46.00/7.41 % fd_pseudo_cond 4
% 46.00/7.41 % AC symbols 0
% 46.00/7.41
% 46.00/7.41 % ------ Schedule dynamic 5 is on
% 46.00/7.41
% 46.00/7.41 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 46.00/7.41
% 46.00/7.41
% 46.00/7.41 % ------
% 46.00/7.41 % Current options:
% 46.00/7.41 % ------
% 46.00/7.41
% 46.00/7.41
% 46.00/7.41 %
% 46.00/7.41
% 46.00/7.41 % ------ Proving...
% 46.00/7.41 %
% 46.00/7.41
% 46.00/7.41 % SZS status Theorem for theBenchmark.p
% 46.00/7.41
% 46.00/7.41 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 46.00/7.43
% 46.00/7.43
%------------------------------------------------------------------------------