%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWC022-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n018.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:07:33 PM UTC 2026
% Result : Unsatisfiable 22.11s 3.84s
% Output : CNFRefutation 22.11s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f253ERROR: Could not build tree for root c_13503ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause8) ).
fof(f9,axiom,
ssItem(skac3),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause9) ).
fof(f60,axiom,
! [X0] :
( frontsegP(X0,nil)
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause60) ).
fof(f61,axiom,
! [X0] :
( frontsegP(X0,X0)
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause61) ).
fof(f72,axiom,
! [X0,X1] :
( ssItem(X1)
| duplicatefreeP(X0)
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause72) ).
fof(f77,axiom,
! [X0] :
( nil = X0
| ssList(tl(X0))
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause77) ).
fof(f78,axiom,
! [X0] :
( nil = X0
| ssItem(hd(X0))
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause78) ).
fof(f83,axiom,
! [X0] :
( frontsegP(nil,X0)
| ~ ssList(X0)
| nil != X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause83) ).
fof(f84,axiom,
! [X0] :
( nil = X0
| ~ ssList(X0)
| ~ frontsegP(nil,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause84) ).
fof(f85,axiom,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause85) ).
fof(f86,axiom,
! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause86) ).
fof(f100,axiom,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssItem(X0)
| cons(X0,X1) != X1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause99) ).
fof(f101,axiom,
! [X0,X1] :
( X1 = X0
| neq(X1,X0)
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause100) ).
fof(f102,plain,
! [X0,X1] :
( X0 = X1
| neq(X1,X0)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f101]) ).
fof(f104,axiom,
! [X0,X1] :
( X1 = X0
| neq(X1,X0)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause102) ).
fof(f105,plain,
! [X0,X1] :
( X0 = X1
| neq(X1,X0)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(reorient_equations,[],[f104]) ).
fof(f107,axiom,
! [X0] :
( nil = X0
| cons(hd(X0),tl(X0)) = X0
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause104) ).
fof(f193,axiom,
! [X2,X3,X0,X1,X4] :
( ~ ssList(X4)
| ~ duplicatefreeP(X4)
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ ssList(X3)
| app(app(X0,cons(X1,X2)),cons(X1,X3)) != X4 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause179) ).
fof(f202,negated_conjecture,
ssList(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_3) ).
fof(f203,negated_conjecture,
ssList(sk4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_4) ).
fof(f204,negated_conjecture,
sk2 = sk4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_5) ).
fof(f205,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_6) ).
fof(f210,negated_conjecture,
! [X0] :
( ~ neq(sk4,nil)
| ~ frontsegP(sk1,X0)
| ~ frontsegP(sk2,X0)
| ~ neq(X0,nil)
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_11) ).
fof(f211,negated_conjecture,
! [X0,X1] :
( ~ neq(sk4,nil)
| ~ neq(nil,sk4)
| hd(sk4) != X1
| cons(X1,nil) != X0
| ~ ssItem(X1)
| sk3 = X0
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_12) ).
fof(f218,plain,
! [X0] :
( ~ neq(sk4,nil)
| ~ frontsegP(sk3,X0)
| ~ frontsegP(sk4,X0)
| ~ neq(X0,nil)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f210,f204,f205]) ).
fof(f221,plain,
( frontsegP(nil,nil)
| ~ ssList(nil) ),
inference(equality_resolution,[],[f83]) ).
fof(f236,plain,
! [X2,X3,X0,X1] :
( ~ ssList(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ~ duplicatefreeP(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ ssList(X3) ),
inference(equality_resolution,[],[f193]) ).
fof(f245,plain,
! [X1] :
( ~ neq(sk4,nil)
| ~ neq(nil,sk4)
| hd(sk4) != X1
| ~ ssItem(X1)
| sk3 = cons(X1,nil)
| ~ ssList(cons(X1,nil)) ),
inference(equality_resolution,[],[f211]) ).
fof(f246,plain,
( ~ neq(sk4,nil)
| ~ neq(nil,sk4)
| ~ ssItem(hd(sk4))
| sk3 = cons(hd(sk4),nil)
| ~ ssList(cons(hd(sk4),nil)) ),
inference(equality_resolution,[],[f245]) ).
tcf(c_253,plain,
ssList(nil),
inference(cnf_transformation,[],[f8]) ).
tcf(c_254,plain,
ssItem(skac3),
inference(cnf_transformation,[],[f9]) ).
tcf(c_305,plain,
! [X0: $i] :
( frontsegP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_306,plain,
! [X0: $i] :
( frontsegP(X0,X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f61]) ).
tcf(c_317,plain,
! [X0: $i,X1: $i] :
( duplicatefreeP(X0)
| ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_322,plain,
! [X0: $i] :
( ssList(tl(X0))
| ( X0 = nil )
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f77]) ).
tcf(c_323,plain,
! [X0: $i] :
( ssItem(hd(X0))
| ( X0 = nil )
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_328,plain,
( frontsegP(nil,nil)
| ~ ssList(nil) ),
inference(cnf_transformation,[],[f221]) ).
tcf(c_329,plain,
! [X0: $i] :
( ( X0 = nil )
| ~ ssList(X0)
| ~ frontsegP(nil,X0) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_330,plain,
! [X0: $i,X1: $i] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_331,plain,
! [X0: $i,X1: $i] :
( ssList(cons(X1,X0))
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_344,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ ssItem(X0)
| ~ ssList(X1)
| ( cons(X0,X1) != X1 ) ),
inference(cnf_transformation,[],[f100]) ).
tcf(c_345,plain,
! [X0: $i,X1: $i] :
( neq(X1,X0)
| ( X0 = X1 )
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f102]) ).
tcf(c_347,plain,
! [X0: $i,X1: $i] :
( neq(X1,X0)
| ( X0 = X1 )
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[],[f105]) ).
tcf(c_349,plain,
! [X0: $i] :
( ( X0 = nil )
| ( cons(hd(X0),tl(X0)) = X0 )
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f107]) ).
tcf(c_360,negated_conjecture,
! [X0: $i] :
( ~ ssList(X0)
| ~ neq(X0,X0) ),
inference(cnf_transformation,[],[f248]) ).
tcf(c_423,plain,
! [X0: $i,X1: $i,X2: $i] :
( frontsegP(cons(X2,X0),cons(X2,X1))
| ~ ssItem(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[],[f252]) ).
tcf(c_424,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ssItem(X1)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ duplicatefreeP(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(X1,X3))) ),
inference(cnf_transformation,[],[f236]) ).
tcf(c_433,negated_conjecture,
ssList(sk3),
inference(cnf_transformation,[],[f202]) ).
tcf(c_434,negated_conjecture,
ssList(sk4),
inference(cnf_transformation,[],[f203]) ).
tcf(c_435,negated_conjecture,
neq(sk4,nil),
inference(cnf_transformation,[],[f253]) ).
tcf(c_438,negated_conjecture,
! [X0: $i] :
( ~ ssList(X0)
| ~ neq(sk4,nil)
| ~ frontsegP(sk4,X0)
| ~ frontsegP(sk3,X0)
| ~ neq(X0,nil) ),
inference(cnf_transformation,[],[f218]) ).
tcf(c_439,negated_conjecture,
( ( cons(hd(sk4),nil) = sk3 )
| ~ ssItem(hd(sk4))
| ~ neq(nil,sk4)
| ~ neq(sk4,nil)
| ~ ssList(cons(hd(sk4),nil)) ),
inference(cnf_transformation,[],[f246]) ).
tcf(c_485,plain,
( ~ ssList(nil)
| ~ neq(nil,nil) ),
inference(instantiation,[status(thm)],[c_360]) ).
tcf(c_500,plain,
( ( nil = nil )
| ~ ssList(nil)
| ~ frontsegP(nil,nil) ),
inference(instantiation,[status(thm)],[c_329]) ).
tcf(c_561,plain,
! [X0: $i] :
( ~ ssList(X0)
| ~ neq(X0,nil)
| ~ frontsegP(sk3,X0)
| ~ frontsegP(sk4,X0) ),
inference(global_subsumption_just,[status(thm)],[c_438,c_435,c_438]) ).
tcf(c_562,negated_conjecture,
! [X0: $i] :
( ~ ssList(X0)
| ~ frontsegP(sk4,X0)
| ~ frontsegP(sk3,X0)
| ~ neq(X0,nil) ),
inference(renaming,[status(thm)],[c_561]) ).
tcf(c_565,negated_conjecture,
( ( cons(hd(sk4),nil) = sk3 )
| ~ ssItem(hd(sk4))
| ~ neq(nil,sk4)
| ~ ssList(cons(hd(sk4),nil)) ),
inference(global_subsumption_just,[status(thm)],[c_439,c_435,c_439]) ).
tcf(c_705,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_707,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( neq(X0,X2)
| ~ neq(X1,X3)
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_1397,plain,
( ( cons(hd(sk4),nil) = sk3 )
| ~ ssList(nil)
| ~ ssItem(hd(sk4))
| ~ neq(nil,sk4) ),
inference(superposition,[status(thm)],[c_331,c_565]) ).
tcf(c_1959,negated_conjecture,
( ( cons(hd(sk4),nil) = sk3 )
| ~ ssItem(hd(sk4))
| ~ neq(nil,sk4) ),
inference(global_subsumption_just,[status(thm)],[c_565,c_253,c_1397]) ).
tcf(c_2421,plain,
! [X0: $i,X1: $i] :
( neq(X0,X1)
| ~ neq(sk4,nil)
| ( X1 != nil )
| ( X0 != sk4 ) ),
inference(instantiation,[status(thm)],[c_707]) ).
tcf(c_2422,plain,
( neq(nil,nil)
| ~ neq(sk4,nil)
| ( nil != nil )
| ( nil != sk4 ) ),
inference(instantiation,[status(thm)],[c_2421]) ).
tcf(c_2644,plain,
! [X0: $i] :
( ( X0 = nil )
| ~ ssList(nil)
| ~ ssList(X0)
| ~ frontsegP(sk4,X0)
| ~ frontsegP(sk3,X0) ),
inference(superposition,[status(thm)],[c_345,c_562]) ).
tcf(c_2645,plain,
( ( sk4 = nil )
| ( cons(hd(sk4),nil) = sk3 )
| ~ ssList(nil)
| ~ ssList(sk4)
| ~ ssItem(hd(sk4)) ),
inference(superposition,[status(thm)],[c_345,c_1959]) ).
tcf(c_2651,plain,
( ( sk4 = nil )
| ( cons(hd(sk4),nil) = sk3 )
| ~ ssItem(nil)
| ~ ssItem(sk4)
| ~ ssItem(hd(sk4)) ),
inference(superposition,[status(thm)],[c_347,c_1959]) ).
tcf(c_2658,plain,
! [X0: $i] :
( ( X0 = nil )
| ~ frontsegP(sk3,X0)
| ~ frontsegP(sk4,X0)
| ~ ssList(X0) ),
inference(global_subsumption_just,[status(thm)],[c_2644,c_253,c_2644]) ).
tcf(c_2659,plain,
! [X0: $i] :
( ( X0 = nil )
| ~ ssList(X0)
| ~ frontsegP(sk4,X0)
| ~ frontsegP(sk3,X0) ),
inference(renaming,[status(thm)],[c_2658]) ).
tcf(c_2661,plain,
( ( sk3 = nil )
| ~ ssList(sk3)
| ~ frontsegP(sk4,sk3) ),
inference(superposition,[status(thm)],[c_306,c_2659]) ).
tcf(c_2662,plain,
( ( sk4 = nil )
| ( cons(hd(sk4),nil) = sk3 )
| ~ ssItem(hd(sk4)) ),
inference(global_subsumption_just,[status(thm)],[c_2645,c_434,c_253,c_2645]) ).
tcf(c_2678,plain,
( ( sk4 = nil )
| ( cons(hd(sk4),nil) = sk3 )
| ~ ssList(sk4) ),
inference(superposition,[status(thm)],[c_323,c_2662]) ).
tcf(c_2744,plain,
( ( sk4 = nil )
| ( cons(hd(sk4),nil) = sk3 ) ),
inference(global_subsumption_just,[status(thm)],[c_2651,c_434,c_2678]) ).
tcf(c_2836,negated_conjecture,
( ( cons(hd(sk4),nil) = sk3 )
| ~ ssItem(hd(sk4))
| ~ neq(nil,sk4) ),
inference(global_subsumption_just,[status(thm)],[c_565,c_253,c_1397]) ).
tcf(c_3233,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ssItem(X4)
| ~ ssItem(X1)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(app(app(X0,cons(X1,X2)),cons(X1,X3))) ),
inference(resolution,[status(thm)],[c_424,c_317]) ).
tcf(c_3341,plain,
( ( sk4 = nil )
| ( cons(hd(sk4),tl(sk4)) = sk4 ) ),
inference(superposition,[status(thm)],[c_434,c_349]) ).
tcf(c_3472,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ssItem(X4)
| ~ ssItem(X1)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(cons(X1,X3))
| ~ ssList(app(X0,cons(X1,X2))) ),
inference(resolution,[status(thm)],[c_3233,c_330]) ).
tcf(c_3480,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ssItem(X4)
| ~ ssItem(X1)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(app(X0,cons(X1,X2))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3472,c_331]) ).
tcf(c_3499,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ssItem(X4)
| ~ ssItem(X0)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(cons(X0,X1)) ),
inference(resolution,[status(thm)],[c_3480,c_330]) ).
tcf(c_3540,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ssItem(X4)
| ~ ssItem(X3)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3499,c_331]) ).
tcf(c_3563,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ssItem(X3)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c_3540,c_254]) ).
tcf(c_3639,plain,
! [X0: $i,X1: $i,X2: $i] :
( ssItem(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c_3563,c_433]) ).
tcf(c_3686,plain,
! [X0: $i,X1: $i,X2: $i] :
( frontsegP(cons(X2,X0),cons(X2,X1))
| ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_423,c_3639]) ).
tcf(c_3693,plain,
! [X0: $i,X1: $i] :
( ssItem(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c_3639,c_433]) ).
tcf(c_3764,plain,
! [X0: $i] : ssItem(X0),
inference(resolution,[status(thm)],[c_3693,c_433]) ).
tcf(c_3812,plain,
( ( cons(hd(sk4),nil) = sk3 )
| ~ neq(nil,sk4) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2836,c_3764]) ).
tcf(c_3827,plain,
! [X0: $i,X1: $i] :
( neq(X0,X1)
| ( X1 = X0 )
| ~ ssItem(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_347,c_3764]) ).
tcf(c_4638,plain,
! [X0: $i,X1: $i] :
( neq(X0,X1)
| ( X1 = X0 ) ),
inference(global_subsumption_just,[status(thm)],[c_3827,c_3764,c_3827]) ).
tcf(c_4639,plain,
! [X0: $i,X1: $i] :
( neq(X1,X0)
| ( X0 = X1 ) ),
inference(renaming,[status(thm)],[c_4638]) ).
tcf(c_5504,plain,
! [X0: $i,X1: $i] :
( ( cons(X0,X1) != X1 )
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_344,c_344,c_3764]) ).
tcf(c_5505,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ ssList(X1)
| ( cons(X0,X1) != X1 ) ),
inference(renaming,[status(thm)],[c_5504]) ).
tcf(c_5511,negated_conjecture,
( ( cons(hd(sk4),nil) = sk3 )
| ~ neq(nil,sk4) ),
inference(global_subsumption_just,[status(thm)],[c_565,c_3812]) ).
tcf(c_5834,plain,
! [X0: $i,X1: $i] :
( neq(X1,X0)
| ( X0 = X1 ) ),
inference(global_subsumption_just,[status(thm)],[c_345,c_4639]) ).
tcf(c_5836,plain,
! [X0: $i] :
( ( X0 = nil )
| ~ ssList(X0)
| ~ frontsegP(sk4,X0)
| ~ frontsegP(sk3,X0) ),
inference(superposition,[status(thm)],[c_5834,c_562]) ).
tcf(c_5837,plain,
( ( sk4 = nil )
| ( cons(hd(sk4),nil) = sk3 ) ),
inference(superposition,[status(thm)],[c_5834,c_5511]) ).
tcf(c_5859,plain,
( ( sk4 = nil )
| ~ ssList(nil)
| ( sk3 != nil ) ),
inference(superposition,[status(thm)],[c_5837,c_5505]) ).
tcf(c_5880,plain,
( ( sk3 = nil )
| ~ ssList(sk3)
| ~ frontsegP(sk4,sk3) ),
inference(superposition,[status(thm)],[c_306,c_5836]) ).
tcf(c_7017,plain,
( ( sk3 = nil )
| ~ frontsegP(sk4,sk3) ),
inference(global_subsumption_just,[status(thm)],[c_5880,c_433,c_2661]) ).
tcf(c_7081,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk4 )
| ( sk4 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_705]) ).
tcf(c_7082,plain,
( ( nil = sk4 )
| ( nil != nil )
| ( sk4 != nil ) ),
inference(instantiation,[status(thm)],[c_7081]) ).
tcf(c_10138,plain,
( ssList(tl(sk4))
| ( sk4 = nil )
| ~ ssList(sk4) ),
inference(instantiation,[status(thm)],[c_322]) ).
tcf(c_10952,plain,
! [X0: $i,X1: $i,X2: $i] :
( frontsegP(cons(X2,X0),cons(X2,X1))
| ~ frontsegP(X0,X1)
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_423,c_3686]) ).
tcf(c_10953,plain,
! [X0: $i,X1: $i,X2: $i] :
( frontsegP(cons(X2,X0),cons(X2,X1))
| ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X0,X1) ),
inference(renaming,[status(thm)],[c_10952]) ).
tcf(c_10961,plain,
! [X0: $i] :
( frontsegP(cons(hd(sk4),X0),sk3)
| ( sk4 = nil )
| ~ ssList(nil)
| ~ ssList(X0)
| ~ frontsegP(X0,nil) ),
inference(superposition,[status(thm)],[c_5837,c_10953]) ).
tcf(c_11526,negated_conjecture,
cons(hd(sk4),nil) = sk3,
inference(global_subsumption_just,[status(thm)],[c_565,c_253,c_435,c_328,c_485,c_500,c_2422,c_2744,c_7082]) ).
tcf(c_12062,plain,
( ( sk4 = nil )
| ( cons(hd(sk4),tl(sk4)) = sk4 ) ),
inference(superposition,[status(thm)],[c_434,c_349]) ).
tcf(c_12139,plain,
cons(hd(sk4),tl(sk4)) = sk4,
inference(global_subsumption_just,[status(thm)],[c_12062,c_253,c_435,c_328,c_485,c_500,c_2422,c_3341,c_7082]) ).
tcf(c_13403,plain,
! [X0: $i,X1: $i,X2: $i] :
( frontsegP(cons(X2,X0),cons(X2,X1))
| ~ frontsegP(X0,X1)
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_423,c_3686]) ).
tcf(c_13404,plain,
! [X0: $i,X1: $i,X2: $i] :
( frontsegP(cons(X2,X0),cons(X2,X1))
| ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X0,X1) ),
inference(renaming,[status(thm)],[c_13403]) ).
tcf(c_13413,plain,
! [X0: $i] :
( frontsegP(cons(hd(sk4),X0),sk3)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ frontsegP(X0,nil) ),
inference(superposition,[status(thm)],[c_11526,c_13404]) ).
tcf(c_13493,plain,
! [X0: $i] :
( frontsegP(cons(hd(sk4),X0),sk3)
| ~ ssList(X0) ),
inference(global_subsumption_just,[status(thm)],[c_13413,c_253,c_435,c_328,c_305,c_485,c_500,c_2422,c_7082,c_10961]) ).
tcf(c_13497,plain,
( frontsegP(sk4,sk3)
| ~ ssList(tl(sk4)) ),
inference(superposition,[status(thm)],[c_12139,c_13493]) ).
tcf(c_13503,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_13497,c_10138,c_7082,c_7017,c_5859,c_2422,c_500,c_485,c_328,c_435,c_253,c_434]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC022-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.12/0.38 % Computer : n018.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Thu Sep 24 15:59:49 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 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.12/0.44
% 0.12/0.44 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.44
% 0.12/0.44 % Detected problem language: tptp
% 0.12/0.45 % Proving...
% 22.11/3.84 % SZS status Started for theBenchmark.p
% 22.11/3.84 % SZS status Unsatisfiable for theBenchmark.p
% 22.11/3.84
% 22.11/3.84 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 22.11/3.84
% 22.11/3.84 % ------ iProver source info
% 22.11/3.84
% 22.11/3.84 % git: date: 2026-07-19 20:42:38 +0200
% 22.11/3.84 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 22.11/3.84 % git: non_committed_changes: false
% 22.11/3.84
% 22.11/3.84 % ------ Parsing...% successful
% 22.11/3.84
% 22.11/3.84
% 22.11/3.84 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 22.11/3.84
% 22.11/3.84 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e sup_sim: 0 sf_s rm: 1 0s sf_e %
% 22.11/3.84
% 22.11/3.84 % ------ Preprocessing...%
% 22.11/3.84
% 22.11/3.84 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 22.11/3.84 % ------ Proving...
% 22.11/3.84 % ------ Problem Properties
% 22.11/3.84
% 22.11/3.84 %
% 22.11/3.84 % clauses 184
% 22.11/3.84 % conjectures 17
% 22.11/3.84 % EPR 58
% 22.11/3.84 % Horn 154
% 22.11/3.84 % unary 61
% 22.11/3.84 % binary 21
% 22.11/3.84 % lits 562
% 22.11/3.84 % lits eq 72
% 22.11/3.84 % fd_pure 0
% 22.11/3.84 % fd_pseudo 0
% 22.11/3.84 % fd_cond 15
% 22.11/3.84 % fd_pseudo_cond 16
% 22.11/3.84 % AC symbols 0
% 22.11/3.84
% 22.11/3.84 % ------ Input Options Time Limit: Unbounded
% 22.11/3.84
% 22.11/3.84
% 22.11/3.84 % ------
% 22.11/3.84 % Current options:
% 22.11/3.84 % ------
% 22.11/3.84
% 22.11/3.84
% 22.11/3.84 %
% 22.11/3.84
% 22.11/3.84 % ------ Proving...
% 22.11/3.84 %
% 22.11/3.84
% 22.11/3.84 % SZS status Unsatisfiable for theBenchmark.p
% 22.11/3.84
% 22.11/3.84 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 22.11/3.84
% 22.11/3.84
%------------------------------------------------------------------------------