%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWC073-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 : n006.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:46 PM UTC 2026
% Result : Unsatisfiable 1.00s 16.29s
% Output : CNFRefutation 1.00s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f249ERROR: Could not build tree for root c_234220ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause8) ).
fof(f12,axiom,
! [X0] : ssItem(skaf83(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause12) ).
fof(f13,axiom,
! [X0] : ssList(skaf82(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause13) ).
fof(f57,axiom,
! [X0] :
( segmentP(X0,X0)
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause57) ).
fof(f72,axiom,
! [X0,X1] :
( ssItem(X1)
| duplicatefreeP(X0)
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause72) ).
fof(f73,axiom,
! [X0] :
( app(X0,nil) = X0
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause73) ).
fof(f74,axiom,
! [X0] :
( app(nil,X0) = X0
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause74) ).
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(f96,axiom,
! [X0,X1] :
( tl(cons(X0,X1)) = X1
| ~ ssList(X1)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause96) ).
fof(f97,axiom,
! [X0,X1] :
( hd(cons(X0,X1)) = X0
| ~ ssList(X1)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause97) ).
fof(f98,axiom,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssItem(X0)
| cons(X0,X1) != nil ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause98) ).
fof(f99,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssItem(X0)
| nil != cons(X0,X1) ),
inference(reorient_equations,[],[f98]) ).
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(f103,axiom,
! [X0] :
( cons(skaf44(X0),nil) = X0
| ~ ssList(X0)
| ~ singletonP(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause101) ).
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(f112,axiom,
! [X0] :
( nil = X0
| cons(skaf83(X0),skaf82(X0)) = X0
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause109) ).
fof(f119,axiom,
! [X0,X1] :
( singletonP(X1)
| ~ ssList(X1)
| ~ ssItem(X0)
| cons(X0,nil) != X1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause116) ).
fof(f125,axiom,
! [X0,X1] :
( app(cons(X0,nil),X1) = cons(X0,X1)
| ~ ssList(X1)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause120) ).
fof(f126,plain,
! [X0,X1] :
( cons(X0,X1) = app(cons(X0,nil),X1)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(reorient_equations,[],[f125]) ).
fof(f187,axiom,
! [X2,X3,X0,X1] :
( segmentP(X3,X1)
| ~ ssList(X3)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| app(app(X0,X1),X2) != X3 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause173) ).
fof(f191,axiom,
! [X0,X1] :
( nil = X0
| X0 = X1
| nil = X1
| ~ ssList(X1)
| ~ ssList(X0)
| hd(X0) != hd(X1)
| tl(X0) != tl(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause177) ).
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(f206,negated_conjecture,
! [X0] :
( ~ segmentP(sk1,X0)
| ~ segmentP(sk2,X0)
| ~ neq(X0,nil)
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_7) ).
fof(f207,negated_conjecture,
( nil != sk4
| nil = sk3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_8) ).
fof(f208,negated_conjecture,
( nil != sk1
| nil != sk2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_9) ).
fof(f209,negated_conjecture,
( neq(sk3,nil)
| ~ neq(sk4,nil) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_10) ).
fof(f213,plain,
! [X0] :
( ~ segmentP(sk3,X0)
| ~ segmentP(sk4,X0)
| ~ neq(X0,nil)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f206,f204,f205]) ).
fof(f214,plain,
( nil != sk3
| nil != sk4 ),
inference(definition_unfolding,[],[f208,f204,f205]) ).
fof(f217,plain,
( frontsegP(nil,nil)
| ~ ssList(nil) ),
inference(equality_resolution,[],[f83]) ).
fof(f222,plain,
! [X0] :
( singletonP(cons(X0,nil))
| ~ ssList(cons(X0,nil))
| ~ ssItem(X0) ),
inference(equality_resolution,[],[f119]) ).
fof(f229,plain,
! [X2,X0,X1] :
( segmentP(app(app(X0,X1),X2),X1)
| ~ ssList(app(app(X0,X1),X2))
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X2) ),
inference(equality_resolution,[],[f187]) ).
fof(f232,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]) ).
tcf(c_252,plain,
ssList(nil),
inference(cnf_transformation,[],[f8]) ).
tcf(c_256,plain,
! [X0: $i] : ssItem(skaf83(X0)),
inference(cnf_transformation,[],[f12]) ).
tcf(c_257,plain,
! [X0: $i] : ssList(skaf82(X0)),
inference(cnf_transformation,[],[f13]) ).
tcf(c_301,plain,
! [X0: $i] :
( segmentP(X0,X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f57]) ).
tcf(c_316,plain,
! [X0: $i,X1: $i] :
( duplicatefreeP(X0)
| ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_317,plain,
! [X0: $i] :
( ( app(X0,nil) = X0 )
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f73]) ).
tcf(c_318,plain,
! [X0: $i] :
( ( app(nil,X0) = X0 )
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_321,plain,
! [X0: $i] :
( ssList(tl(X0))
| ( X0 = nil )
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f77]) ).
tcf(c_322,plain,
! [X0: $i] :
( ssItem(hd(X0))
| ( X0 = nil )
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_327,plain,
( frontsegP(nil,nil)
| ~ ssList(nil) ),
inference(cnf_transformation,[],[f217]) ).
tcf(c_328,plain,
! [X0: $i] :
( ( X0 = nil )
| ~ ssList(X0)
| ~ frontsegP(nil,X0) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_329,plain,
! [X0: $i,X1: $i] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_330,plain,
! [X0: $i,X1: $i] :
( ssList(cons(X1,X0))
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_340,plain,
! [X0: $i,X1: $i] :
( ( tl(cons(X1,X0)) = X0 )
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f96]) ).
tcf(c_341,plain,
! [X0: $i,X1: $i] :
( ( hd(cons(X1,X0)) = X1 )
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f97]) ).
tcf(c_342,plain,
! [X0: $i,X1: $i] :
( ~ ssItem(X0)
| ~ ssList(X1)
| ( cons(X0,X1) != nil ) ),
inference(cnf_transformation,[],[f99]) ).
tcf(c_344,plain,
! [X0: $i,X1: $i] :
( neq(X1,X0)
| ( X0 = X1 )
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f102]) ).
tcf(c_345,plain,
! [X0: $i] :
( ( cons(skaf44(X0),nil) = X0 )
| ~ singletonP(X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f103]) ).
tcf(c_346,plain,
! [X0: $i,X1: $i] :
( neq(X1,X0)
| ( X0 = X1 )
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[],[f105]) ).
tcf(c_348,plain,
! [X0: $i] :
( ( X0 = nil )
| ( cons(hd(X0),tl(X0)) = X0 )
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f107]) ).
tcf(c_353,plain,
! [X0: $i] :
( ( X0 = nil )
| ( cons(skaf83(X0),skaf82(X0)) = X0 )
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f112]) ).
tcf(c_359,plain,
! [X0: $i] :
( ~ ssList(X0)
| ~ neq(X0,X0) ),
inference(cnf_transformation,[],[f244]) ).
tcf(c_360,plain,
! [X0: $i] :
( singletonP(cons(X0,nil))
| ~ ssItem(X0)
| ~ ssList(cons(X0,nil)) ),
inference(cnf_transformation,[],[f222]) ).
tcf(c_364,plain,
! [X0: $i,X1: $i] :
( ( app(cons(X1,nil),X0) = cons(X1,X0) )
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f126]) ).
tcf(c_417,plain,
! [X0: $i,X1: $i,X2: $i] :
( segmentP(app(app(X0,X1),X2),X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(app(app(X0,X1),X2)) ),
inference(cnf_transformation,[],[f229]) ).
tcf(c_421,plain,
! [X0: $i,X1: $i] :
( ( X1 = nil )
| ( X0 = nil )
| ( X0 = X1 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( hd(X0) != hd(X1) )
| ( tl(X0) != tl(X1) ) ),
inference(cnf_transformation,[],[f191]) ).
tcf(c_423,plain,
! [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,[],[f232]) ).
tcf(c_432,negated_conjecture,
ssList(sk3),
inference(cnf_transformation,[],[f202]) ).
tcf(c_433,negated_conjecture,
ssList(sk4),
inference(cnf_transformation,[],[f203]) ).
tcf(c_434,negated_conjecture,
! [X0: $i] :
( ~ ssList(X0)
| ~ segmentP(sk4,X0)
| ~ segmentP(sk3,X0)
| ~ neq(X0,nil) ),
inference(cnf_transformation,[],[f213]) ).
tcf(c_435,negated_conjecture,
( ( sk3 = nil )
| ( sk4 != nil ) ),
inference(cnf_transformation,[],[f207]) ).
tcf(c_436,negated_conjecture,
( ( sk4 != nil )
| ( sk3 != nil ) ),
inference(cnf_transformation,[],[f214]) ).
tcf(c_437,negated_conjecture,
( neq(sk3,nil)
| ~ neq(sk4,nil) ),
inference(cnf_transformation,[],[f209]) ).
tcf(c_438,negated_conjecture,
( ( app(tl(sk3),cons(hd(sk3),nil)) = sk4 )
| ~ ssItem(hd(sk3))
| ~ neq(nil,sk3)
| ~ neq(sk4,nil)
| ~ ssList(tl(sk3))
| ~ ssList(cons(hd(sk3),nil))
| ~ ssList(app(tl(sk3),cons(hd(sk3),nil))) ),
inference(cnf_transformation,[],[f249]) ).
tcf(c_484,plain,
( ~ ssList(nil)
| ~ neq(nil,nil) ),
inference(instantiation,[status(thm)],[c_359]) ).
tcf(c_499,plain,
( ( nil = nil )
| ~ ssList(nil)
| ~ frontsegP(nil,nil) ),
inference(instantiation,[status(thm)],[c_328]) ).
tcf(c_552,negated_conjecture,
sk4 != nil,
inference(global_subsumption_just,[status(thm)],[c_435,c_435,c_436]) ).
tcf(c_556,negated_conjecture,
sk4 != nil,
inference(global_subsumption_just,[status(thm)],[c_436,c_552]) ).
tcf(c_797,plain,
( ( app(tl(sk3),cons(hd(sk3),nil)) = sk4 )
| ~ ssItem(hd(sk3))
| ~ neq(nil,sk3)
| ~ neq(sk4,nil)
| ~ ssList(tl(sk3))
| ~ ssList(cons(hd(sk3),nil)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_438,c_329]) ).
tcf(c_6558,plain,
! [X0: $i] :
( ~ iPr_def_10
| ssItem(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_316]) ).
tcf(c_6559,plain,
! [X0: $i] :
( ~ iPr_def_11
| ~ ssList(X0)
| duplicatefreeP(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_316]) ).
tcf(c_6560,plain,
( iPr_def_11
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_316]) ).
tcf(c_6561,definition,
iPr_def_12 = hd(sk3),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_6562,definition,
iPr_def_13 = cons(iPr_def_12,nil),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_6563,definition,
iPr_def_14 = tl(sk3),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_6564,definition,
iPr_def_15 = app(iPr_def_14,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_6565,plain,
( ( iPr_def_15 = sk4 )
| ~ ssItem(iPr_def_12)
| ~ ssList(iPr_def_14)
| ~ ssList(iPr_def_13)
| ~ neq(nil,sk3)
| ~ neq(sk4,nil) ),
inference(demodulation,[status(thm)],[c_797,c_6564,c_6563,c_6561,c_6562]) ).
tcf(c_6566,negated_conjecture,
sk4 != nil,
inference(demodulation,[status(thm)],[c_556]) ).
tcf(c_6567,negated_conjecture,
! [X0: $i] :
( ~ ssList(X0)
| ~ segmentP(sk4,X0)
| ~ segmentP(sk3,X0)
| ~ neq(X0,nil) ),
inference(demodulation,[status(thm)],[c_434]) ).
tcf(c_6568,negated_conjecture,
( neq(sk3,nil)
| ~ neq(sk4,nil) ),
inference(demodulation,[status(thm)],[c_437]) ).
tcf(c_6569,negated_conjecture,
ssList(sk4),
inference(demodulation,[status(thm)],[c_433]) ).
tcf(c_6570,negated_conjecture,
ssList(sk3),
inference(demodulation,[status(thm)],[c_432]) ).
tcf(c_6573,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_6575,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( neq(X0,X2)
| ~ neq(X1,X3)
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_9641,plain,
( ssList(iPr_def_14)
| ( sk3 = nil )
| ~ ssList(sk3) ),
inference(superposition,[status(thm)],[c_6563,c_321]) ).
tcf(c_9645,plain,
( ssList(iPr_def_14)
| ( sk3 = nil ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9641,c_6570]) ).
tcf(c_9664,plain,
( ssItem(iPr_def_12)
| ( sk3 = nil )
| ~ ssList(sk3) ),
inference(superposition,[status(thm)],[c_6561,c_322]) ).
tcf(c_9665,plain,
( ssItem(iPr_def_12)
| ( sk3 = nil ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9664,c_6570]) ).
tcf(c_9778,plain,
( ssList(iPr_def_13)
| ~ ssItem(iPr_def_12)
| ~ ssList(nil) ),
inference(superposition,[status(thm)],[c_6562,c_330]) ).
tcf(c_9782,plain,
( ssList(iPr_def_13)
| ~ ssItem(iPr_def_12) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9778,c_252]) ).
tcf(c_9944,plain,
( ( sk4 = iPr_def_15 )
| ~ ssItem(iPr_def_12)
| ~ ssList(iPr_def_14)
| ~ neq(nil,sk3)
| ~ neq(sk4,nil) ),
inference(backward_subsumption_resolution,[status(thm)],[c_6565,c_9782]) ).
tcf(c_10221,plain,
! [X0: $i] :
( singletonP(cons(X0,nil))
| ~ ssList(nil)
| ~ ssItem(X0) ),
inference(superposition,[status(thm)],[c_330,c_360]) ).
tcf(c_10227,plain,
! [X0: $i] :
( singletonP(cons(X0,nil))
| ~ ssItem(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10221,c_252]) ).
tcf(c_10433,plain,
! [X0: $i,X1: $i] :
( ( hd(cons(X0,skaf82(X1))) = X0 )
| ~ ssItem(X0) ),
inference(superposition,[status(thm)],[c_257,c_341]) ).
tcf(c_10582,plain,
( ssItem(hd(sk4))
| ( sk4 = nil )
| ~ ssList(sk4) ),
inference(instantiation,[status(thm)],[c_322]) ).
tcf(c_10964,plain,
( ( sk4 = iPr_def_15 )
| ( sk4 = nil )
| ~ ssItem(iPr_def_12)
| ~ ssList(iPr_def_14)
| ~ ssList(nil)
| ~ ssList(sk4)
| ~ neq(nil,sk3) ),
inference(superposition,[status(thm)],[c_344,c_9944]) ).
tcf(c_10965,plain,
( neq(sk3,nil)
| ( sk4 = nil )
| ~ ssList(nil)
| ~ ssList(sk4) ),
inference(superposition,[status(thm)],[c_344,c_6568]) ).
tcf(c_10968,plain,
neq(sk3,nil),
inference(forward_subsumption_resolution,[status(thm)],[c_10965,c_6566,c_252,c_6569]) ).
tcf(c_10974,plain,
( ( sk4 = iPr_def_15 )
| ~ ssItem(iPr_def_12)
| ~ ssList(iPr_def_14)
| ~ neq(nil,sk3) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10964,c_6566,c_252,c_6569]) ).
tcf(c_11010,plain,
( ~ ssList(sk3)
| ~ segmentP(sk4,sk3)
| ~ segmentP(sk3,sk3) ),
inference(superposition,[status(thm)],[c_10968,c_6567]) ).
tcf(c_11011,plain,
( ~ segmentP(sk4,sk3)
| ~ segmentP(sk3,sk3) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11010,c_6570]) ).
tcf(c_11018,plain,
( ~ ssList(sk3)
| ~ segmentP(sk4,sk3) ),
inference(superposition,[status(thm)],[c_301,c_11011]) ).
tcf(c_11019,plain,
~ segmentP(sk4,sk3),
inference(forward_subsumption_resolution,[status(thm)],[c_11018,c_6570]) ).
tcf(c_11029,plain,
( ( sk4 = iPr_def_15 )
| ( sk3 = nil )
| ~ ssItem(iPr_def_12)
| ~ ssList(iPr_def_14)
| ~ ssList(nil)
| ~ ssList(sk3) ),
inference(superposition,[status(thm)],[c_344,c_10974]) ).
tcf(c_11030,plain,
( ( sk4 = iPr_def_15 )
| ( sk3 = nil )
| ~ ssItem(iPr_def_12)
| ~ ssList(iPr_def_14) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11029,c_252,c_6570]) ).
tcf(c_11041,plain,
( ( sk4 = iPr_def_15 )
| ( sk3 = nil ) ),
inference(global_subsumption_just,[status(thm)],[c_11030,c_9645,c_9665,c_11030]) ).
tcf(c_11047,plain,
( ( sk3 = nil )
| ~ segmentP(iPr_def_15,sk3) ),
inference(superposition,[status(thm)],[c_11041,c_11019]) ).
tcf(c_11233,plain,
( ( sk3 = nil )
| ( cons(hd(sk3),tl(sk3)) = sk3 ) ),
inference(superposition,[status(thm)],[c_6570,c_348]) ).
tcf(c_11271,plain,
( ( sk3 = nil )
| ( cons(iPr_def_12,iPr_def_14) = sk3 ) ),
inference(light_normalisation,[status(thm)],[c_11233,c_6561,c_6563]) ).
tcf(c_11482,plain,
( ( sk3 = nil )
| ( cons(skaf83(sk3),skaf82(sk3)) = sk3 ) ),
inference(superposition,[status(thm)],[c_6570,c_353]) ).
tcf(c_14761,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssItem(hd(sk4))
| ~ duplicatefreeP(app(app(X0,cons(hd(sk4),X1)),cons(hd(sk4),X2)))
| ~ ssList(app(app(X0,cons(hd(sk4),X1)),cons(hd(sk4),X2))) ),
inference(instantiation,[status(thm)],[c_423]) ).
tcf(c_14769,plain,
( ~ ssList(nil)
| ~ ssItem(hd(sk4))
| ~ duplicatefreeP(app(app(nil,cons(hd(sk4),nil)),cons(hd(sk4),nil)))
| ~ ssList(app(app(nil,cons(hd(sk4),nil)),cons(hd(sk4),nil))) ),
inference(instantiation,[status(thm)],[c_14761]) ).
tcf(c_56423,plain,
! [X0: $i,X1: $i] :
( ssList(app(X1,cons(hd(sk4),X0)))
| ~ ssList(X1)
| ~ ssList(cons(hd(sk4),X0)) ),
inference(instantiation,[status(thm)],[c_329]) ).
tcf(c_56424,plain,
( ssList(app(nil,cons(hd(sk4),nil)))
| ~ ssList(nil)
| ~ ssList(cons(hd(sk4),nil)) ),
inference(instantiation,[status(thm)],[c_56423]) ).
tcf(c_57559,plain,
! [X0: $i] :
( ssList(cons(hd(sk4),X0))
| ~ ssList(X0)
| ~ ssItem(hd(sk4)) ),
inference(instantiation,[status(thm)],[c_330]) ).
tcf(c_57560,plain,
( ssList(cons(hd(sk4),nil))
| ~ ssList(nil)
| ~ ssItem(hd(sk4)) ),
inference(instantiation,[status(thm)],[c_57559]) ).
tcf(c_64617,plain,
! [X0: $i,X1: $i] : hd(cons(skaf83(X0),skaf82(X1))) = skaf83(X0),
inference(superposition,[status(thm)],[c_256,c_10433]) ).
tcf(c_64772,plain,
( ( sk3 = nil )
| ( hd(sk3) = skaf83(sk3) ) ),
inference(superposition,[status(thm)],[c_11482,c_64617]) ).
tcf(c_64776,plain,
( ( sk3 = nil )
| ( skaf83(sk3) = iPr_def_12 ) ),
inference(light_normalisation,[status(thm)],[c_64772,c_6561]) ).
tcf(c_67322,plain,
( ( sk3 = nil )
| ( cons(iPr_def_12,skaf82(sk3)) = sk3 ) ),
inference(superposition,[status(thm)],[c_64776,c_11482]) ).
tcf(c_72264,plain,
! [X0: $i,X1: $i] :
( neq(X0,X1)
| ~ neq(sk3,nil)
| ( X1 != nil )
| ( X0 != sk3 ) ),
inference(instantiation,[status(thm)],[c_6575]) ).
tcf(c_72265,plain,
( neq(nil,nil)
| ~ neq(sk3,nil)
| ( nil != nil )
| ( nil != sk3 ) ),
inference(instantiation,[status(thm)],[c_72264]) ).
tcf(c_80084,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk3 )
| ( sk3 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_6573]) ).
tcf(c_80085,plain,
( ( nil = sk3 )
| ( nil != nil )
| ( sk3 != nil ) ),
inference(instantiation,[status(thm)],[c_80084]) ).
tcf(c_101980,plain,
! [X0: $i,X1: $i] :
( duplicatefreeP(app(X1,X0))
| ~ iPr_def_11
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(superposition,[status(thm)],[c_329,c_6559]) ).
tcf(c_116391,plain,
cons(iPr_def_12,skaf82(sk3)) = sk3,
inference(global_subsumption_just,[status(thm)],[c_67322,c_252,c_327,c_484,c_499,c_10968,c_67322,c_72265,c_80085]) ).
tcf(c_116425,plain,
( ~ ssItem(iPr_def_12)
| ~ ssList(skaf82(sk3))
| ( sk3 != nil ) ),
inference(superposition,[status(thm)],[c_116391,c_342]) ).
tcf(c_116450,plain,
( ~ ssItem(iPr_def_12)
| ( sk3 != nil ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_116425,c_257]) ).
tcf(c_117595,plain,
sk3 != nil,
inference(global_subsumption_just,[status(thm)],[c_116450,c_252,c_327,c_484,c_499,c_10968,c_72265,c_80085]) ).
tcf(c_117672,plain,
sk4 = iPr_def_15,
inference(backward_subsumption_resolution,[status(thm)],[c_11041,c_117595]) ).
tcf(c_153011,plain,
! [X0: $i,X1: $i,X2: $i] :
( ssList(app(app(X0,cons(hd(sk4),X1)),cons(hd(sk4),X2)))
| ~ ssList(cons(hd(sk4),X2))
| ~ ssList(app(X0,cons(hd(sk4),X1))) ),
inference(instantiation,[status(thm)],[c_56423]) ).
tcf(c_153012,plain,
( ssList(app(app(nil,cons(hd(sk4),nil)),cons(hd(sk4),nil)))
| ~ ssList(cons(hd(sk4),nil))
| ~ ssList(app(nil,cons(hd(sk4),nil))) ),
inference(instantiation,[status(thm)],[c_153011]) ).
tcf(c_155238,plain,
! [X0: $i,X1: $i,X2: $i] :
( duplicatefreeP(app(app(X0,cons(hd(sk4),X1)),cons(hd(sk4),X2)))
| ~ iPr_def_11
| ~ ssList(app(app(X0,cons(hd(sk4),X1)),cons(hd(sk4),X2))) ),
inference(instantiation,[status(thm)],[c_6559]) ).
tcf(c_155239,plain,
( duplicatefreeP(app(app(nil,cons(hd(sk4),nil)),cons(hd(sk4),nil)))
| ~ iPr_def_11
| ~ ssList(app(app(nil,cons(hd(sk4),nil)),cons(hd(sk4),nil))) ),
inference(instantiation,[status(thm)],[c_155238]) ).
tcf(c_156129,plain,
~ iPr_def_11,
inference(global_subsumption_just,[status(thm)],[c_101980,c_433,c_252,c_435,c_436,c_10582,c_14769,c_56424,c_57560,c_153012,c_155239]) ).
tcf(c_156131,plain,
iPr_def_10,
inference(backward_subsumption_resolution,[status(thm)],[c_6560,c_156129]) ).
tcf(c_156136,plain,
! [X0: $i] : ssItem(X0),
inference(backward_subsumption_resolution,[status(thm)],[c_6558,c_156131]) ).
tcf(c_156215,plain,
! [X0: $i,X1: $i] :
( ( app(cons(X1,nil),X0) = cons(X1,X0) )
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_364,c_156136]) ).
tcf(c_156223,plain,
! [X0: $i,X1: $i] :
( neq(X1,X0)
| ( X0 = X1 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_346,c_156136]) ).
tcf(c_156226,plain,
! [X0: $i,X1: $i] :
( ( hd(cons(X1,X0)) = X1 )
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_341,c_156136]) ).
tcf(c_156227,plain,
! [X0: $i,X1: $i] :
( ( tl(cons(X1,X0)) = X0 )
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_340,c_156136]) ).
tcf(c_156228,plain,
! [X0: $i,X1: $i] :
( ssList(cons(X1,X0))
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_330,c_156136]) ).
tcf(c_160336,plain,
ssList(iPr_def_15),
inference(light_normalisation,[status(thm)],[c_6569,c_117672]) ).
tcf(c_160338,negated_conjecture,
neq(sk3,nil),
inference(global_subsumption_just,[status(thm)],[c_6568,c_10968]) ).
tcf(c_160340,plain,
! [X0: $i] :
( ~ ssList(X0)
| ~ segmentP(iPr_def_15,X0)
| ~ segmentP(sk3,X0)
| ~ neq(X0,nil) ),
inference(light_normalisation,[status(thm)],[c_6567,c_117672]) ).
tcf(c_160345,plain,
( ~ ssList(sk3)
| ~ segmentP(iPr_def_15,sk3)
| ~ segmentP(sk3,sk3) ),
inference(superposition,[status(thm)],[c_160338,c_160340]) ).
tcf(c_160346,plain,
( ~ segmentP(iPr_def_15,sk3)
| ~ segmentP(sk3,sk3) ),
inference(forward_subsumption_resolution,[status(thm)],[c_160345,c_6570]) ).
tcf(c_160349,plain,
~ segmentP(iPr_def_15,sk3),
inference(global_subsumption_just,[status(thm)],[c_160346,c_252,c_327,c_484,c_499,c_10968,c_11047,c_72265,c_80085]) ).
tcf(c_160408,plain,
app(sk3,nil) = sk3,
inference(superposition,[status(thm)],[c_6570,c_317]) ).
tcf(c_160437,plain,
app(iPr_def_15,nil) = iPr_def_15,
inference(superposition,[status(thm)],[c_160336,c_317]) ).
tcf(c_160486,plain,
( ssList(iPr_def_14)
| ( sk3 = nil )
| ~ ssList(sk3) ),
inference(superposition,[status(thm)],[c_6563,c_321]) ).
tcf(c_160489,plain,
( ssList(iPr_def_14)
| ( sk3 = nil ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_160486,c_6570]) ).
tcf(c_160527,plain,
ssList(iPr_def_14),
inference(global_subsumption_just,[status(thm)],[c_160489,c_252,c_327,c_484,c_499,c_9645,c_10968,c_72265,c_80085]) ).
tcf(c_160529,plain,
app(nil,iPr_def_14) = iPr_def_14,
inference(superposition,[status(thm)],[c_160527,c_318]) ).
tcf(c_160541,plain,
! [X0: $i,X1: $i] :
( ssList(cons(X1,X0))
| ~ ssList(X0) ),
inference(global_subsumption_just,[status(thm)],[c_330,c_156228]) ).
tcf(c_160547,plain,
( ssList(iPr_def_13)
| ~ ssList(nil) ),
inference(superposition,[status(thm)],[c_6562,c_160541]) ).
tcf(c_160550,plain,
ssList(iPr_def_13),
inference(forward_subsumption_resolution,[status(thm)],[c_160547,c_252]) ).
tcf(c_160952,plain,
! [X0: $i] : singletonP(cons(X0,nil)),
inference(global_subsumption_just,[status(thm)],[c_360,c_433,c_252,c_435,c_436,c_6558,c_6560,c_10227,c_10582,c_14769,c_56424,c_57560,c_153012,c_155239]) ).
tcf(c_160954,plain,
singletonP(iPr_def_13),
inference(superposition,[status(thm)],[c_6562,c_160952]) ).
tcf(c_160955,plain,
! [X0: $i,X1: $i] :
( ( tl(cons(X1,X0)) = X0 )
| ~ ssList(X0) ),
inference(global_subsumption_just,[status(thm)],[c_340,c_156227]) ).
tcf(c_160962,plain,
! [X0: $i] : tl(cons(X0,nil)) = nil,
inference(superposition,[status(thm)],[c_252,c_160955]) ).
tcf(c_160994,plain,
! [X0: $i] : tl(cons(X0,iPr_def_14)) = iPr_def_14,
inference(superposition,[status(thm)],[c_160527,c_160955]) ).
tcf(c_161045,plain,
! [X0: $i,X1: $i] :
( ( hd(cons(X1,X0)) = X1 )
| ~ ssList(X0) ),
inference(global_subsumption_just,[status(thm)],[c_341,c_156226]) ).
tcf(c_161052,plain,
! [X0: $i] : hd(cons(X0,nil)) = X0,
inference(superposition,[status(thm)],[c_252,c_161045]) ).
tcf(c_161084,plain,
! [X0: $i] : hd(cons(X0,iPr_def_14)) = X0,
inference(superposition,[status(thm)],[c_160527,c_161045]) ).
tcf(c_161138,plain,
! [X0: $i,X1: $i] :
( ( cons(X0,X1) != nil )
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_342,c_433,c_252,c_435,c_436,c_342,c_6558,c_6560,c_10582,c_14769,c_56424,c_57560,c_153012,c_155239]) ).
tcf(c_161139,plain,
! [X0: $i,X1: $i] :
( ~ ssList(X1)
| ( cons(X0,X1) != nil ) ),
inference(renaming,[status(thm)],[c_161138]) ).
tcf(c_161144,plain,
( ~ ssList(nil)
| ( nil != iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_6562,c_161139]) ).
tcf(c_161145,plain,
nil != iPr_def_13,
inference(forward_subsumption_resolution,[status(thm)],[c_161144,c_252]) ).
tcf(c_161149,plain,
tl(iPr_def_13) = nil,
inference(superposition,[status(thm)],[c_6562,c_160962]) ).
tcf(c_161158,plain,
! [X0: $i,X1: $i] :
( neq(X1,X0)
| ( X0 = X1 ) ),
inference(global_subsumption_just,[status(thm)],[c_344,c_156223]) ).
tcf(c_161164,plain,
! [X0: $i] :
( ( X0 = nil )
| ~ ssList(X0)
| ~ segmentP(iPr_def_15,X0)
| ~ segmentP(sk3,X0) ),
inference(superposition,[status(thm)],[c_161158,c_160340]) ).
tcf(c_161177,plain,
( ( cons(skaf44(iPr_def_13),nil) = iPr_def_13 )
| ~ ssList(iPr_def_13) ),
inference(superposition,[status(thm)],[c_160954,c_345]) ).
tcf(c_161178,plain,
cons(skaf44(iPr_def_13),nil) = iPr_def_13,
inference(forward_subsumption_resolution,[status(thm)],[c_161177,c_160550]) ).
tcf(c_161261,plain,
( ( sk3 = nil )
| ( cons(hd(sk3),tl(sk3)) = sk3 ) ),
inference(superposition,[status(thm)],[c_6570,c_348]) ).
tcf(c_161302,plain,
( ( sk3 = nil )
| ( cons(iPr_def_12,iPr_def_14) = sk3 ) ),
inference(light_normalisation,[status(thm)],[c_161261,c_6561,c_6563]) ).
tcf(c_161406,plain,
cons(iPr_def_12,iPr_def_14) = sk3,
inference(global_subsumption_just,[status(thm)],[c_161302,c_252,c_327,c_484,c_499,c_10968,c_11271,c_72265,c_80085]) ).
tcf(c_161411,plain,
( ~ ssList(iPr_def_14)
| ( sk3 != nil ) ),
inference(superposition,[status(thm)],[c_161406,c_161139]) ).
tcf(c_161412,plain,
hd(sk3) = iPr_def_12,
inference(superposition,[status(thm)],[c_161406,c_161084]) ).
tcf(c_161413,plain,
tl(sk3) = iPr_def_14,
inference(superposition,[status(thm)],[c_161406,c_160994]) ).
tcf(c_161415,plain,
sk3 != nil,
inference(forward_subsumption_resolution,[status(thm)],[c_161411,c_160527]) ).
tcf(c_161587,plain,
! [X0: $i,X1: $i] :
( ( app(cons(X1,nil),X0) = cons(X1,X0) )
| ~ ssList(X0) ),
inference(global_subsumption_just,[status(thm)],[c_364,c_156215]) ).
tcf(c_161626,plain,
! [X0: $i] : app(cons(X0,nil),iPr_def_14) = cons(X0,iPr_def_14),
inference(superposition,[status(thm)],[c_160527,c_161587]) ).
tcf(c_171008,plain,
! [X0: $i] :
( segmentP(app(iPr_def_15,X0),iPr_def_13)
| ~ ssList(iPr_def_14)
| ~ ssList(iPr_def_13)
| ~ ssList(X0)
| ~ ssList(app(app(iPr_def_14,iPr_def_13),X0)) ),
inference(superposition,[status(thm)],[c_6564,c_417]) ).
tcf(c_171065,plain,
! [X0: $i] :
( segmentP(app(iPr_def_14,X0),iPr_def_14)
| ~ ssList(iPr_def_14)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(app(app(nil,iPr_def_14),X0)) ),
inference(superposition,[status(thm)],[c_160529,c_417]) ).
tcf(c_171113,plain,
! [X0: $i] :
( segmentP(app(iPr_def_14,X0),iPr_def_14)
| ~ ssList(iPr_def_14)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(app(iPr_def_14,X0)) ),
inference(light_normalisation,[status(thm)],[c_171065,c_160529]) ).
tcf(c_171114,plain,
! [X0: $i] :
( segmentP(app(iPr_def_14,X0),iPr_def_14)
| ~ ssList(X0)
| ~ ssList(app(iPr_def_14,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_171113,c_160527,c_252]) ).
tcf(c_171128,plain,
! [X0: $i] :
( segmentP(app(iPr_def_15,X0),iPr_def_13)
| ~ ssList(iPr_def_14)
| ~ ssList(iPr_def_13)
| ~ ssList(X0)
| ~ ssList(app(iPr_def_15,X0)) ),
inference(light_normalisation,[status(thm)],[c_171008,c_6564]) ).
tcf(c_171129,plain,
! [X0: $i] :
( segmentP(app(iPr_def_15,X0),iPr_def_13)
| ~ ssList(X0)
| ~ ssList(app(iPr_def_15,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_171128,c_160527,c_160550]) ).
tcf(c_172858,plain,
! [X0: $i] :
( ( sk3 = nil )
| ( X0 = nil )
| ( X0 = sk3 )
| ~ ssList(sk3)
| ~ ssList(X0)
| ( hd(X0) != hd(sk3) )
| ( tl(X0) != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_161413,c_421]) ).
tcf(c_172882,plain,
! [X0: $i] :
( ( sk3 = nil )
| ( X0 = nil )
| ( X0 = sk3 )
| ~ ssList(sk3)
| ~ ssList(X0)
| ( hd(X0) != iPr_def_12 )
| ( tl(X0) != iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_172858,c_161412]) ).
tcf(c_172883,plain,
! [X0: $i] :
( ( X0 = nil )
| ( X0 = sk3 )
| ~ ssList(X0)
| ( hd(X0) != iPr_def_12 )
| ( tl(X0) != iPr_def_14 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_172882,c_161415,c_6570]) ).
tcf(c_176047,plain,
hd(iPr_def_13) = iPr_def_12,
inference(superposition,[status(thm)],[c_6562,c_161052]) ).
tcf(c_176380,plain,
hd(iPr_def_13) = skaf44(iPr_def_13),
inference(superposition,[status(thm)],[c_161178,c_161052]) ).
tcf(c_176430,plain,
skaf44(iPr_def_13) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_176380,c_176047]) ).
tcf(c_176566,plain,
cons(iPr_def_12,nil) = iPr_def_13,
inference(demodulation,[status(thm)],[c_161178,c_176430]) ).
tcf(c_177322,plain,
( ( nil = iPr_def_13 )
| ( sk3 = iPr_def_13 )
| ~ ssList(iPr_def_13)
| ( nil != iPr_def_14 )
| ( hd(iPr_def_13) != iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_161149,c_172883]) ).
tcf(c_177323,plain,
( ( nil = iPr_def_13 )
| ( sk3 = iPr_def_13 )
| ~ ssList(iPr_def_13)
| ( nil != iPr_def_14 ) ),
inference(ground_joinability,[status(thm)],[c_177322,c_176047]) ).
tcf(c_177324,plain,
( ( sk3 = iPr_def_13 )
| ( nil != iPr_def_14 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_177323,c_161145,c_160550]) ).
tcf(c_180190,plain,
app(iPr_def_13,iPr_def_14) = cons(iPr_def_12,iPr_def_14),
inference(superposition,[status(thm)],[c_176566,c_161626]) ).
tcf(c_180209,plain,
app(iPr_def_13,iPr_def_14) = sk3,
inference(light_normalisation,[status(thm)],[c_180190,c_161406]) ).
tcf(c_180961,plain,
! [X0: $i] :
( segmentP(app(sk3,X0),iPr_def_14)
| ~ ssList(iPr_def_14)
| ~ ssList(iPr_def_13)
| ~ ssList(X0)
| ~ ssList(app(app(iPr_def_13,iPr_def_14),X0)) ),
inference(superposition,[status(thm)],[c_180209,c_417]) ).
tcf(c_181010,plain,
! [X0: $i] :
( segmentP(app(sk3,X0),iPr_def_14)
| ~ ssList(iPr_def_14)
| ~ ssList(iPr_def_13)
| ~ ssList(X0)
| ~ ssList(app(sk3,X0)) ),
inference(light_normalisation,[status(thm)],[c_180961,c_180209]) ).
tcf(c_181011,plain,
! [X0: $i] :
( segmentP(app(sk3,X0),iPr_def_14)
| ~ ssList(X0)
| ~ ssList(app(sk3,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_181010,c_160527,c_160550]) ).
tcf(c_227471,plain,
( segmentP(iPr_def_15,iPr_def_14)
| ~ ssList(iPr_def_13)
| ~ ssList(app(iPr_def_14,iPr_def_13)) ),
inference(superposition,[status(thm)],[c_6564,c_171114]) ).
tcf(c_227480,plain,
( segmentP(iPr_def_15,iPr_def_14)
| ~ ssList(iPr_def_15)
| ~ ssList(iPr_def_13) ),
inference(light_normalisation,[status(thm)],[c_227471,c_6564]) ).
tcf(c_227481,plain,
segmentP(iPr_def_15,iPr_def_14),
inference(forward_subsumption_resolution,[status(thm)],[c_227480,c_160336,c_160550]) ).
tcf(c_228986,plain,
( segmentP(iPr_def_15,iPr_def_13)
| ~ ssList(nil)
| ~ ssList(app(iPr_def_15,nil)) ),
inference(superposition,[status(thm)],[c_160437,c_171129]) ).
tcf(c_228991,plain,
( segmentP(iPr_def_15,iPr_def_13)
| ~ ssList(iPr_def_15)
| ~ ssList(nil) ),
inference(light_normalisation,[status(thm)],[c_228986,c_160437]) ).
tcf(c_228992,plain,
segmentP(iPr_def_15,iPr_def_13),
inference(forward_subsumption_resolution,[status(thm)],[c_228991,c_160336,c_252]) ).
tcf(c_233108,plain,
( segmentP(sk3,iPr_def_14)
| ~ ssList(nil)
| ~ ssList(app(sk3,nil)) ),
inference(superposition,[status(thm)],[c_160408,c_181011]) ).
tcf(c_233113,plain,
( segmentP(sk3,iPr_def_14)
| ~ ssList(nil)
| ~ ssList(sk3) ),
inference(light_normalisation,[status(thm)],[c_233108,c_160408]) ).
tcf(c_233114,plain,
segmentP(sk3,iPr_def_14),
inference(forward_subsumption_resolution,[status(thm)],[c_233113,c_252,c_6570]) ).
tcf(c_233137,plain,
( ( nil = iPr_def_14 )
| ~ ssList(iPr_def_14)
| ~ segmentP(iPr_def_15,iPr_def_14) ),
inference(superposition,[status(thm)],[c_233114,c_161164]) ).
tcf(c_233138,plain,
nil = iPr_def_14,
inference(forward_subsumption_resolution,[status(thm)],[c_233137,c_160527,c_227481]) ).
tcf(c_233145,plain,
sk3 = iPr_def_13,
inference(backward_subsumption_resolution,[status(thm)],[c_177324,c_233138]) ).
tcf(c_234218,plain,
~ segmentP(iPr_def_15,iPr_def_13),
inference(demodulation,[status(thm)],[c_160349,c_233145]) ).
tcf(c_234220,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_234218,c_228992]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC073-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.13/0.37 % Computer : n006.cluster.edu
% 0.13/0.37 % Model : x86_64 x86_64
% 0.13/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.37 % Memory : 8046.5625MB
% 0.13/0.37 % OS : Linux 6.8.0-71-generic
% 0.13/0.37 % CPULimit : 300
% 0.13/0.37 % WCLimit : 300
% 0.13/0.37 % DateTime : Thu Sep 24 16:14:26 UTC 2026
% 0.13/0.37 % CPUTime :
% 0.13/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.17/0.41 Running first-order theorem proving
% 0.17/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.17/0.42
% 0.17/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.17/0.42
% 0.17/0.42 % Detected problem language: tptp
% 0.17/0.43 % Proving...
% 1.00/16.29 % SZS status Started for theBenchmark.p
% 1.00/16.29 % SZS status Unsatisfiable for theBenchmark.p
% 1.00/16.29
% 1.00/16.29 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 1.00/16.29
% 1.00/16.29 % ------ iProver source info
% 1.00/16.29
% 1.00/16.29 % git: date: 2026-07-19 20:42:38 +0200
% 1.00/16.29 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 1.00/16.29 % git: non_committed_changes: false
% 1.00/16.29
% 1.00/16.29 % ------ Parsing...% successful
% 1.00/16.29
% 1.00/16.29
% 1.00/16.29 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 1.00/16.29
% 1.00/16.29 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 1.00/16.29
% 1.00/16.29 % ------ Preprocessing... gs_s sp: 2 0s gs_e snvd_s sp: 0 0s snvd_e %
% 1.00/16.29
% 1.00/16.29 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 1.00/16.29 % ------ Proving...
% 1.00/16.29 % ------ Problem Properties
% 1.00/16.29
% 1.00/16.29 %
% 1.00/16.29 % clauses 191
% 1.00/16.29 % conjectures 5
% 1.00/16.29 % EPR 62
% 1.00/16.29 % Horn 161
% 1.00/16.29 % unary 65
% 1.00/16.29 % binary 24
% 1.00/16.29 % lits 572
% 1.00/16.29 % lits eq 77
% 1.00/16.29 % fd_pure 0
% 1.00/16.29 % fd_pseudo 0
% 1.00/16.29 % fd_cond 15
% 1.00/16.29 % fd_pseudo_cond 16
% 1.00/16.29 % AC symbols 0
% 1.00/16.29
% 1.00/16.29 % ------ Schedule dynamic 5 is on
% 1.00/16.29
% 1.00/16.29 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 1.00/16.29
% 1.00/16.29
% 1.00/16.29 % ------
% 1.00/16.29 % Current options:
% 1.00/16.29 % ------
% 1.00/16.29
% 1.00/16.29
% 1.00/16.29 %
% 1.00/16.29
% 1.00/16.29 % ------ Proving...
% 1.00/16.29 % Proof_search_loop: time out after: 5709 full_loop iterations
% 1.00/16.29
% 1.00/16.29 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" Time Limit: 15.
% 1.00/16.29
% 1.00/16.29
% 1.00/16.29 % ------
% 1.00/16.29 % Current options:
% 1.00/16.29 % ------
% 1.00/16.29
% 1.00/16.29
% 1.00/16.29 %
% 1.00/16.29
% 1.00/16.29 % ------ Proving...
% 1.00/16.29 %
% 1.00/16.29
% 1.00/16.29 % SZS status Unsatisfiable for theBenchmark.p
% 1.00/16.29
% 1.00/16.29 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 1.00/16.30
% 1.00/16.30
%------------------------------------------------------------------------------