%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWX048+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n008.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:32:36 PM UTC 2026
% Result : Theorem 184.40s 35.79s
% Output : CNFRefutation 184.40s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f660ERROR: Could not build tree for root c_295869ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f73,axiom,
! [X0] :
( list_succeeds(X0)
<=> ( X0 = nil
| ? [X1,X2] :
( list_succeeds(X2)
& X0 = cons(X1,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id73) ).
fof(f273,axiom,
! [X0,X1,X2] :
( list_succeeds(X1)
=> ( occ(X0,X1) = X2
<=> occ_succeeds(X0,X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','occ/2') ).
fof(f283,axiom,
! [X0,X1,X2] :
( occ_succeeds(X0,X1,X2)
=> ( nat_succeeds(X2)
& list_succeeds(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(occ:types)') ).
fof(f288,conjecture,
! [X0,X1,X2] :
( ( X0 != X1
& list_succeeds(X2) )
=> occ(X0,cons(X1,X2)) = occ(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(occ:cons:diff)') ).
fof(f289,negated_conjecture,
~ ! [X0,X1,X2] :
( ( X0 != X1
& list_succeeds(X2) )
=> occ(X0,cons(X1,X2)) = occ(X0,X2) ),
inference(negated_conjecture,[status(cth)],[f288]) ).
fof(f636,plain,
! [X0,X1,X2] :
( ~ list_succeeds(X1)
| ( occ(X0,X1) = X2
<=> occ_succeeds(X0,X1,X2) ) ),
inference(ennf_transformation,[],[f273]) ).
fof(f652,plain,
! [X0,X1,X2] :
( ~ occ_succeeds(X0,X1,X2)
| ( nat_succeeds(X2)
& list_succeeds(X1) ) ),
inference(ennf_transformation,[],[f283]) ).
fof(f657,plain,
? [X0,X1,X2] :
( X0 != X1
& list_succeeds(X2)
& occ(X0,cons(X1,X2)) != occ(X0,X2) ),
inference(ennf_transformation,[],[f289]) ).
fof(f658,plain,
? [X0,X1,X2] :
( X0 != X1
& list_succeeds(X2)
& occ(X0,cons(X1,X2)) != occ(X0,X2) ),
inference(flattening,[],[f657]) ).
fof(f678,plain,
! [X1,X0,X2] :
( ( ~ sP1(X1,X0,X2)
| ( X2 = '0'
& X1 = nil )
| sP0(X1,X0,X2)
| ? [X3,X4] :
( occ_succeeds(X0,X4,X2)
& X0 != X3
& X1 = cons(X3,X4) ) )
& ( ( ( '0' != X2
| nil != X1 )
& ~ sP0(X1,X0,X2)
& ! [X3,X4] :
( ~ occ_succeeds(X0,X4,X2)
| X0 = X3
| cons(X3,X4) != X1 ) )
| sP1(X1,X0,X2) ) ),
inference(nnf_transformation,[],[f660]) ).
fof(f679,plain,
! [X1,X0,X2] :
( ( ~ sP1(X1,X0,X2)
| ( X2 = '0'
& X1 = nil )
| sP0(X1,X0,X2)
| ? [X3,X4] :
( occ_succeeds(X0,X4,X2)
& X0 != X3
& X1 = cons(X3,X4) ) )
& ( ( ( '0' != X2
| nil != X1 )
& ~ sP0(X1,X0,X2)
& ! [X3,X4] :
( ~ occ_succeeds(X0,X4,X2)
| X0 = X3
| cons(X3,X4) != X1 ) )
| sP1(X1,X0,X2) ) ),
inference(flattening,[],[f678]) ).
fof(f680,plain,
! [X0,X1,X2] :
( ( ~ sP1(X0,X1,X2)
| ( X2 = '0'
& nil = X0 )
| sP0(X0,X1,X2)
| ? [X5,X6] :
( occ_succeeds(X1,X6,X2)
& X1 != X5
& cons(X5,X6) = X0 ) )
& ( ( ( '0' != X2
| nil != X0 )
& ~ sP0(X0,X1,X2)
& ! [X3,X4] :
( ~ occ_succeeds(X1,X4,X2)
| X1 = X3
| cons(X3,X4) != X0 ) )
| sP1(X0,X1,X2) ) ),
inference(rectify,[],[f679]) ).
fof(f681,plain,
! [X0,X1,X2] :
( ( ~ sP1(X0,X1,X2)
| ( X2 = '0'
& nil = X0 )
| sP0(X0,X1,X2)
| ( occ_succeeds(X1,sK7(X0,X1,X2),X2)
& sK6(X0,X1,X2) != X1
& cons(sK6(X0,X1,X2),sK7(X0,X1,X2)) = X0 ) )
& ( ( ( '0' != X2
| nil != X0 )
& ~ sP0(X0,X1,X2)
& ! [X3,X4] :
( ~ occ_succeeds(X1,X4,X2)
| X1 = X3
| cons(X3,X4) != X0 ) )
| sP1(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7]),skolemize(X5,sK6(X0,X1,X2)),skolemize(X6,sK7(X0,X1,X2))],[f680]) ).
fof(f685,plain,
! [X0,X1,X2] :
( ( ~ occ_succeeds(X0,X1,X2)
| sP1(X1,X0,X2) )
& ( ~ sP1(X1,X0,X2)
| occ_succeeds(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f661]) ).
fof(f770,plain,
! [X0] :
( ( ~ list_succeeds(X0)
| X0 = nil
| ? [X1,X2] :
( list_succeeds(X2)
& X0 = cons(X1,X2) ) )
& ( ( nil != X0
& ! [X1,X2] :
( ~ list_succeeds(X2)
| cons(X1,X2) != X0 ) )
| list_succeeds(X0) ) ),
inference(nnf_transformation,[],[f73]) ).
fof(f771,plain,
! [X0] :
( ( ~ list_succeeds(X0)
| X0 = nil
| ? [X1,X2] :
( list_succeeds(X2)
& X0 = cons(X1,X2) ) )
& ( ( nil != X0
& ! [X1,X2] :
( ~ list_succeeds(X2)
| cons(X1,X2) != X0 ) )
| list_succeeds(X0) ) ),
inference(flattening,[],[f770]) ).
fof(f772,plain,
! [X0] :
( ( ~ list_succeeds(X0)
| X0 = nil
| ? [X3,X4] :
( list_succeeds(X4)
& cons(X3,X4) = X0 ) )
& ( ( nil != X0
& ! [X1,X2] :
( ~ list_succeeds(X2)
| cons(X1,X2) != X0 ) )
| list_succeeds(X0) ) ),
inference(rectify,[],[f771]) ).
fof(f773,plain,
! [X0] :
( ( ~ list_succeeds(X0)
| X0 = nil
| ( list_succeeds(sK72(X0))
& cons(sK71(X0),sK72(X0)) = X0 ) )
& ( ( nil != X0
& ! [X1,X2] :
( ~ list_succeeds(X2)
| cons(X1,X2) != X0 ) )
| list_succeeds(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK71,sK72]),skolemize(X3,sK71(X0)),skolemize(X4,sK72(X0))],[f772]) ).
fof(f868,plain,
! [X0,X1,X2] :
( ~ list_succeeds(X1)
| ( ( occ(X0,X1) != X2
| occ_succeeds(X0,X1,X2) )
& ( ~ occ_succeeds(X0,X1,X2)
| occ(X0,X1) = X2 ) ) ),
inference(nnf_transformation,[],[f636]) ).
fof(f872,plain,
( sK135 != sK136
& list_succeeds(sK137)
& occ(sK135,cons(sK136,sK137)) != occ(sK135,sK137) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK135,sK136,sK137]),skolemize(X0,sK135),skolemize(X1,sK136),skolemize(X2,sK137)],[f658]) ).
fof(f938,plain,
! [X2,X3,X0,X1,X4] :
( ~ occ_succeeds(X1,X4,X2)
| X1 = X3
| cons(X3,X4) != X0
| sP1(X0,X1,X2) ),
inference(cnf_transformation,[],[f681]) ).
fof(f944,plain,
! [X2,X0,X1] :
( ~ sP1(X1,X0,X2)
| occ_succeeds(X0,X1,X2) ),
inference(cnf_transformation,[],[f685]) ).
fof(f1089,plain,
! [X2,X0,X1] :
( ~ list_succeeds(X2)
| cons(X1,X2) != X0
| list_succeeds(X0) ),
inference(cnf_transformation,[],[f773]) ).
fof(f1391,plain,
! [X2,X0,X1] :
( ~ list_succeeds(X1)
| occ(X0,X1) != X2
| occ_succeeds(X0,X1,X2) ),
inference(cnf_transformation,[],[f868]) ).
fof(f1392,plain,
! [X2,X0,X1] :
( ~ list_succeeds(X1)
| ~ occ_succeeds(X0,X1,X2)
| occ(X0,X1) = X2 ),
inference(cnf_transformation,[],[f868]) ).
fof(f1404,plain,
! [X2,X0,X1] :
( ~ occ_succeeds(X0,X1,X2)
| list_succeeds(X1) ),
inference(cnf_transformation,[],[f652]) ).
fof(f1413,plain,
sK135 != sK136,
inference(cnf_transformation,[],[f872]) ).
fof(f1414,plain,
list_succeeds(sK137),
inference(cnf_transformation,[],[f872]) ).
fof(f1415,plain,
occ(sK135,cons(sK136,sK137)) != occ(sK135,sK137),
inference(cnf_transformation,[],[f872]) ).
fof(f1416,plain,
! [X2,X3,X1,X4] :
( ~ occ_succeeds(X1,X4,X2)
| X1 = X3
| sP1(cons(X3,X4),X1,X2) ),
inference(equality_resolution,[],[f938]) ).
fof(f1472,plain,
! [X2,X1] :
( ~ list_succeeds(X2)
| list_succeeds(cons(X1,X2)) ),
inference(equality_resolution,[],[f1089]) ).
fof(f1529,plain,
! [X0,X1] :
( ~ list_succeeds(X1)
| occ_succeeds(X0,X1,occ(X0,X1)) ),
inference(equality_resolution,[],[f1391]) ).
tcf(c_106,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP1(cons(X3,X1),X0,X2)
| ( X0 = X3 )
| ~ occ_succeeds(X0,X1,X2) ),
inference(cnf_transformation,[],[f1416]) ).
tcf(c_119,plain,
! [X0: $i,X1: $i,X2: $i] :
( occ_succeeds(X1,X0,X2)
| ~ sP1(X0,X1,X2) ),
inference(cnf_transformation,[],[f944]) ).
tcf(c_262,plain,
! [X0: $i,X1: $i] :
( list_succeeds(cons(X1,X0))
| ~ list_succeeds(X0) ),
inference(cnf_transformation,[],[f1472]) ).
tcf(c_567,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( occ(X0,X1) = X2 )
| ~ list_succeeds(X1)
| ~ occ_succeeds(X0,X1,X2) ),
inference(cnf_transformation,[],[f1392]) ).
tcf(c_568,plain,
! [X0: $i,X1: $i] :
( occ_succeeds(X1,X0,occ(X1,X0))
| ~ list_succeeds(X0) ),
inference(cnf_transformation,[],[f1529]) ).
tcf(c_579,plain,
! [X0: $i,X1: $i,X2: $i] :
( list_succeeds(X1)
| ~ occ_succeeds(X0,X1,X2) ),
inference(cnf_transformation,[],[f1404]) ).
tcf(c_589,negated_conjecture,
occ(sK135,cons(sK136,sK137)) != occ(sK135,sK137),
inference(cnf_transformation,[],[f1415]) ).
tcf(c_590,negated_conjecture,
list_succeeds(sK137),
inference(cnf_transformation,[],[f1414]) ).
tcf(c_591,negated_conjecture,
sK135 != sK136,
inference(cnf_transformation,[],[f1413]) ).
tcf(c_979,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( occ(X0,X1) = X2 )
| ~ occ_succeeds(X0,X1,X2) ),
inference(global_subsumption_just,[status(thm)],[c_567,c_579,c_567]) ).
tcf(c_12129,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( occ(X0,X1) = X2 )
| ~ occ_succeeds(X0,X1,X2) ),
inference(prop_impl_just,[status(thm)],[c_979]) ).
tcf(c_22557,definition,
iPr_def_12 = cons(sK136,sK137),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_22558,definition,
iPr_def_13 = occ(sK135,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_22559,definition,
iPr_def_14 = occ(sK135,sK137),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_22560,negated_conjecture,
sK135 != sK136,
inference(demodulation,[status(thm)],[c_591]) ).
tcf(c_22561,negated_conjecture,
list_succeeds(sK137),
inference(demodulation,[status(thm)],[c_590]) ).
tcf(c_22562,negated_conjecture,
iPr_def_13 != iPr_def_14,
inference(demodulation,[status(thm)],[c_589,c_22559,c_22557,c_22558]) ).
tcf(c_270171,plain,
! [X0: $i,X1: $i] :
( sP1(iPr_def_12,X0,X1)
| ( X0 = sK136 )
| ~ occ_succeeds(X0,sK137,X1) ),
inference(superposition,[status(thm)],[c_22557,c_106]) ).
tcf(c_270680,plain,
( list_succeeds(iPr_def_12)
| ~ list_succeeds(sK137) ),
inference(superposition,[status(thm)],[c_22557,c_262]) ).
tcf(c_270683,plain,
list_succeeds(iPr_def_12),
inference(forward_subsumption_resolution,[status(thm)],[c_270680,c_22561]) ).
tcf(c_280559,plain,
( occ_succeeds(sK135,sK137,iPr_def_14)
| ~ list_succeeds(sK137) ),
inference(superposition,[status(thm)],[c_22559,c_568]) ).
tcf(c_280560,plain,
( occ_succeeds(sK135,iPr_def_12,iPr_def_13)
| ~ list_succeeds(iPr_def_12) ),
inference(superposition,[status(thm)],[c_22558,c_568]) ).
tcf(c_280570,plain,
occ_succeeds(sK135,iPr_def_12,iPr_def_13),
inference(forward_subsumption_resolution,[status(thm)],[c_280560,c_270683]) ).
tcf(c_280571,plain,
occ_succeeds(sK135,sK137,iPr_def_14),
inference(forward_subsumption_resolution,[status(thm)],[c_280559,c_22561]) ).
tcf(c_281068,plain,
occ(sK135,iPr_def_12) = iPr_def_13,
inference(superposition,[status(thm)],[c_280570,c_12129]) ).
tcf(c_295810,plain,
( sP1(iPr_def_12,sK135,iPr_def_14)
| ( sK135 = sK136 ) ),
inference(superposition,[status(thm)],[c_280571,c_270171]) ).
tcf(c_295811,plain,
sP1(iPr_def_12,sK135,iPr_def_14),
inference(forward_subsumption_resolution,[status(thm)],[c_295810,c_22560]) ).
tcf(c_295850,plain,
occ_succeeds(sK135,iPr_def_12,iPr_def_14),
inference(superposition,[status(thm)],[c_295811,c_119]) ).
tcf(c_295861,plain,
occ(sK135,iPr_def_12) = iPr_def_14,
inference(superposition,[status(thm)],[c_295850,c_12129]) ).
tcf(c_295868,plain,
iPr_def_13 = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_295861,c_281068]) ).
tcf(c_295869,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_295868,c_22562]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX048+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/5.39 % Computer : n008.cluster.edu
% 0.13/5.39 % Model : x86_64 x86_64
% 0.13/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/5.39 % Memory : 8046.5625MB
% 0.13/5.39 % OS : Linux 6.8.0-71-generic
% 0.13/5.39 % CPULimit : 300
% 0.13/5.39 % WCLimit : 300
% 0.13/5.39 % DateTime : Thu Sep 24 23:22:48 UTC 2026
% 0.17/5.40 % CPUTime :
% 0.17/5.40 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.17/5.46 Running first-order theorem proving
% 0.17/5.46 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/5.48
% 0.17/5.48 % ======== iProver multi-core TPTP/SMT =========
% 0.17/5.48
% 0.17/5.48 % Detected problem language: tptp
% 0.18/5.50 % Proving...
% 184.40/35.79 % SZS status Started for theBenchmark.p
% 184.40/35.79 % SZS status Theorem for theBenchmark.p
% 184.40/35.79
% 184.40/35.79 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 184.40/35.79
% 184.40/35.79 % ------ iProver source info
% 184.40/35.79
% 184.40/35.79 % git: date: 2026-07-19 20:42:38 +0200
% 184.40/35.79 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 184.40/35.79 % git: non_committed_changes: false
% 184.40/35.79
% 184.40/35.79 % ------ Parsing...
% 184.40/35.79 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 184.40/35.79
% 184.40/35.79 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe_e sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 184.40/35.79
% 184.40/35.79 % ------ Preprocessing... gs_s sp: 4 0s gs_e snvd_s sp: 0 0s snvd_e %
% 184.40/35.79
% 184.40/35.79 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 184.40/35.79 % ------ Proving...
% 184.40/35.79 % ------ Problem Properties
% 184.40/35.79
% 184.40/35.79 %
% 184.40/35.79 % clauses 532
% 184.40/35.79 % conjectures 3
% 184.40/35.79 % EPR 173
% 184.40/35.79 % Horn 343
% 184.40/35.79 % unary 51
% 184.40/35.79 % binary 201
% 184.40/35.79 % lits 1372
% 184.40/35.79 % lits eq 304
% 184.40/35.79 % fd_pure 0
% 184.40/35.79 % fd_pseudo 0
% 184.40/35.79 % fd_cond 48
% 184.40/35.79 % fd_pseudo_cond 39
% 184.40/35.79 % AC symbols 0
% 184.40/35.79
% 184.40/35.79 % ------ Schedule dynamic 5 is on
% 184.40/35.79
% 184.40/35.79 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 184.40/35.79
% 184.40/35.79
% 184.40/35.79 % ------
% 184.40/35.79 % Current options:
% 184.40/35.79 % ------
% 184.40/35.79
% 184.40/35.79
% 184.40/35.79 %
% 184.40/35.79
% 184.40/35.79 % ------ Proving...
% 184.40/35.79 % Proof_search_loop: time out after: 4525 full_loop iterations
% 184.40/35.79
% 184.40/35.79 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" Time Limit: 15.
% 184.40/35.79
% 184.40/35.79
% 184.40/35.79 % ------
% 184.40/35.79 % Current options:
% 184.40/35.79 % ------
% 184.40/35.79
% 184.40/35.79
% 184.40/35.79 %
% 184.40/35.79
% 184.40/35.79 % ------ Proving...
% 184.40/35.79 % Proof_search_loop: time out after: 5779 full_loop iterations
% 184.40/35.79
% 184.40/35.79 % ------ Option_1: Negative Selections Time Limit: 35.
% 184.40/35.79
% 184.40/35.79
% 184.40/35.79 % ------
% 184.40/35.79 % Current options:
% 184.40/35.79 % ------
% 184.40/35.79
% 184.40/35.79
% 184.40/35.79 %
% 184.40/35.79
% 184.40/35.79 % ------ Proving...
% 184.40/35.79 %
% 184.40/35.79
% 184.40/35.79 % SZS status Theorem for theBenchmark.p
% 184.40/35.79
% 184.40/35.79 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 184.40/35.79
% 184.40/35.79
%------------------------------------------------------------------------------