%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWC072-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 : n019.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 64.48s 16.91s
% Output : CNFRefutation 64.48s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f248ERROR: Could not build tree for root c_235891ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause8) ).
fof(f47,axiom,
! [X0] : ssItem(skaf44(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause47) ).
fof(f57,axiom,
! [X0] :
( segmentP(X0,X0)
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause57) ).
fof(f71,axiom,
! [X0] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause71) ).
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(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(f151,axiom,
! [X2,X0,X1] :
( memberP(app(X0,X2),X1)
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ memberP(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause140) ).
fof(f169,axiom,
! [X2,X0,X1] :
( cons(X0,app(X1,X2)) = app(cons(X0,X1),X2)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause157) ).
fof(f173,axiom,
! [X2,X0,X1] :
( X2 = X0
| memberP(X1,X2)
| ~ ssItem(X2)
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ memberP(cons(X0,X1),X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause161) ).
fof(f174,plain,
! [X2,X0,X1] :
( X0 = X2
| memberP(X1,X2)
| ~ ssItem(X2)
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ memberP(cons(X0,X1),X2) ),
inference(reorient_equations,[],[f173]) ).
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(f212,plain,
! [X0] :
( ~ segmentP(sk3,X0)
| ~ segmentP(sk4,X0)
| ~ neq(X0,nil)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f206,f204,f205]) ).
fof(f213,plain,
( nil != sk3
| nil != sk4 ),
inference(definition_unfolding,[],[f208,f204,f205]) ).
fof(f216,plain,
( frontsegP(nil,nil)
| ~ ssList(nil) ),
inference(equality_resolution,[],[f83]) ).
fof(f221,plain,
! [X0] :
( singletonP(cons(X0,nil))
| ~ ssList(cons(X0,nil))
| ~ ssItem(X0) ),
inference(equality_resolution,[],[f119]) ).
fof(f228,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(f231,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_251,plain,
ssList(nil),
inference(cnf_transformation,[],[f8]) ).
tcf(c_290,plain,
! [X0: $i] : ssItem(skaf44(X0)),
inference(cnf_transformation,[],[f47]) ).
tcf(c_300,plain,
! [X0: $i] :
( segmentP(X0,X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f57]) ).
tcf(c_314,plain,
! [X0: $i] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_315,plain,
! [X0: $i,X1: $i] :
( duplicatefreeP(X0)
| ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_316,plain,
! [X0: $i] :
( ( app(X0,nil) = X0 )
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f73]) ).
tcf(c_317,plain,
! [X0: $i] :
( ( app(nil,X0) = X0 )
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_320,plain,
! [X0: $i] :
( ssList(tl(X0))
| ( X0 = nil )
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f77]) ).
tcf(c_321,plain,
! [X0: $i] :
( ssItem(hd(X0))
| ( X0 = nil )
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_326,plain,
( frontsegP(nil,nil)
| ~ ssList(nil) ),
inference(cnf_transformation,[],[f216]) ).
tcf(c_327,plain,
! [X0: $i] :
( ( X0 = nil )
| ~ ssList(X0)
| ~ frontsegP(nil,X0) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_328,plain,
! [X0: $i,X1: $i] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_329,plain,
! [X0: $i,X1: $i] :
( ssList(cons(X1,X0))
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_339,plain,
! [X0: $i,X1: $i] :
( ( tl(cons(X1,X0)) = X0 )
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f96]) ).
tcf(c_340,plain,
! [X0: $i,X1: $i] :
( ( hd(cons(X1,X0)) = X1 )
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f97]) ).
tcf(c_341,plain,
! [X0: $i,X1: $i] :
( ~ ssItem(X0)
| ~ ssList(X1)
| ( cons(X0,X1) != nil ) ),
inference(cnf_transformation,[],[f99]) ).
tcf(c_343,plain,
! [X0: $i,X1: $i] :
( neq(X1,X0)
| ( X0 = X1 )
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f102]) ).
tcf(c_344,plain,
! [X0: $i] :
( ( cons(skaf44(X0),nil) = X0 )
| ~ singletonP(X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f103]) ).
tcf(c_345,plain,
! [X0: $i,X1: $i] :
( neq(X1,X0)
| ( X0 = X1 )
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[],[f105]) ).
tcf(c_347,plain,
! [X0: $i] :
( ( X0 = nil )
| ( cons(hd(X0),tl(X0)) = X0 )
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f107]) ).
tcf(c_358,plain,
! [X0: $i] :
( ~ ssList(X0)
| ~ neq(X0,X0) ),
inference(cnf_transformation,[],[f243]) ).
tcf(c_359,plain,
! [X0: $i] :
( singletonP(cons(X0,nil))
| ~ ssItem(X0)
| ~ ssList(cons(X0,nil)) ),
inference(cnf_transformation,[],[f221]) ).
tcf(c_363,plain,
! [X0: $i,X1: $i] :
( ( app(cons(X1,nil),X0) = cons(X1,X0) )
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f126]) ).
tcf(c_381,plain,
! [X0: $i,X1: $i] :
( memberP(cons(X1,X0),X1)
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f245]) ).
tcf(c_383,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(app(X0,X2),X1)
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ memberP(X0,X1) ),
inference(cnf_transformation,[],[f151]) ).
tcf(c_400,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( app(cons(X2,X0),X1) = cons(X2,app(X0,X1)) )
| ~ ssItem(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f169]) ).
tcf(c_404,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(X1,X2)
| ( X0 = X2 )
| ~ ssItem(X2)
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ memberP(cons(X0,X1),X2) ),
inference(cnf_transformation,[],[f174]) ).
tcf(c_416,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,[],[f228]) ).
tcf(c_420,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_422,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,[],[f231]) ).
tcf(c_431,negated_conjecture,
ssList(sk3),
inference(cnf_transformation,[],[f202]) ).
tcf(c_432,negated_conjecture,
ssList(sk4),
inference(cnf_transformation,[],[f203]) ).
tcf(c_433,negated_conjecture,
! [X0: $i] :
( ~ ssList(X0)
| ~ segmentP(sk4,X0)
| ~ segmentP(sk3,X0)
| ~ neq(X0,nil) ),
inference(cnf_transformation,[],[f212]) ).
tcf(c_434,negated_conjecture,
( ( sk3 = nil )
| ( sk4 != nil ) ),
inference(cnf_transformation,[],[f207]) ).
tcf(c_435,negated_conjecture,
( ( sk4 != nil )
| ( sk3 != nil ) ),
inference(cnf_transformation,[],[f213]) ).
tcf(c_436,negated_conjecture,
( ( app(tl(sk4),cons(hd(sk4),nil)) = sk3 )
| ~ ssItem(hd(sk4))
| ~ neq(nil,sk4)
| ~ neq(sk4,nil)
| ~ ssList(tl(sk4))
| ~ ssList(cons(hd(sk4),nil))
| ~ ssList(app(tl(sk4),cons(hd(sk4),nil))) ),
inference(cnf_transformation,[],[f248]) ).
tcf(c_482,plain,
( ~ ssList(nil)
| ~ neq(nil,nil) ),
inference(instantiation,[status(thm)],[c_358]) ).
tcf(c_497,plain,
( ( nil = nil )
| ~ ssList(nil)
| ~ frontsegP(nil,nil) ),
inference(instantiation,[status(thm)],[c_327]) ).
tcf(c_550,negated_conjecture,
sk4 != nil,
inference(global_subsumption_just,[status(thm)],[c_434,c_434,c_435]) ).
tcf(c_554,negated_conjecture,
sk4 != nil,
inference(global_subsumption_just,[status(thm)],[c_435,c_550]) ).
tcf(c_791,plain,
( ( app(tl(sk4),cons(hd(sk4),nil)) = sk3 )
| ~ ssItem(hd(sk4))
| ~ neq(nil,sk4)
| ~ neq(sk4,nil)
| ~ ssList(tl(sk4))
| ~ ssList(cons(hd(sk4),nil)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_436,c_328]) ).
tcf(c_6540,plain,
! [X0: $i] :
( ~ iPr_def_10
| ssItem(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_315]) ).
tcf(c_6541,plain,
! [X0: $i] :
( ~ iPr_def_11
| ~ ssList(X0)
| duplicatefreeP(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_315]) ).
tcf(c_6542,plain,
( iPr_def_11
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_315]) ).
tcf(c_6543,definition,
iPr_def_12 = hd(sk4),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_6544,definition,
iPr_def_13 = cons(iPr_def_12,nil),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_6545,definition,
iPr_def_14 = tl(sk4),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_6546,definition,
iPr_def_15 = app(iPr_def_14,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_6547,plain,
( ( iPr_def_15 = sk3 )
| ~ ssItem(iPr_def_12)
| ~ ssList(iPr_def_14)
| ~ ssList(iPr_def_13)
| ~ neq(nil,sk4)
| ~ neq(sk4,nil) ),
inference(demodulation,[status(thm)],[c_791,c_6546,c_6545,c_6543,c_6544]) ).
tcf(c_6548,negated_conjecture,
sk4 != nil,
inference(demodulation,[status(thm)],[c_554]) ).
tcf(c_6549,negated_conjecture,
! [X0: $i] :
( ~ ssList(X0)
| ~ segmentP(sk4,X0)
| ~ segmentP(sk3,X0)
| ~ neq(X0,nil) ),
inference(demodulation,[status(thm)],[c_433]) ).
tcf(c_6550,negated_conjecture,
ssList(sk4),
inference(demodulation,[status(thm)],[c_432]) ).
tcf(c_6551,negated_conjecture,
ssList(sk3),
inference(demodulation,[status(thm)],[c_431]) ).
tcf(c_6556,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( neq(X0,X2)
| ~ neq(X1,X3)
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_9612,plain,
( ssList(iPr_def_14)
| ( sk4 = nil )
| ~ ssList(sk4) ),
inference(superposition,[status(thm)],[c_6545,c_320]) ).
tcf(c_9616,plain,
ssList(iPr_def_14),
inference(forward_subsumption_resolution,[status(thm)],[c_9612,c_6548,c_6550]) ).
tcf(c_9639,plain,
( ssItem(iPr_def_12)
| ( sk4 = nil )
| ~ ssList(sk4) ),
inference(superposition,[status(thm)],[c_6543,c_321]) ).
tcf(c_9640,plain,
ssItem(iPr_def_12),
inference(forward_subsumption_resolution,[status(thm)],[c_9639,c_6548,c_6550]) ).
tcf(c_9696,plain,
( ssList(iPr_def_13)
| ~ ssItem(iPr_def_12)
| ~ ssList(nil) ),
inference(superposition,[status(thm)],[c_6544,c_329]) ).
tcf(c_9700,plain,
ssList(iPr_def_13),
inference(forward_subsumption_resolution,[status(thm)],[c_9696,c_9640,c_251]) ).
tcf(c_10047,plain,
! [X0: $i] :
( singletonP(cons(X0,nil))
| ~ ssList(nil)
| ~ ssItem(X0) ),
inference(superposition,[status(thm)],[c_329,c_359]) ).
tcf(c_10051,plain,
! [X0: $i] :
( singletonP(cons(X0,nil))
| ~ ssItem(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10047,c_251]) ).
tcf(c_10964,plain,
( ( sk4 = nil )
| ( cons(hd(sk4),tl(sk4)) = sk4 ) ),
inference(superposition,[status(thm)],[c_6550,c_347]) ).
tcf(c_11004,plain,
( ( sk4 = nil )
| ( cons(iPr_def_12,iPr_def_14) = sk4 ) ),
inference(light_normalisation,[status(thm)],[c_10964,c_6543,c_6545]) ).
tcf(c_11005,plain,
cons(iPr_def_12,iPr_def_14) = sk4,
inference(forward_subsumption_resolution,[status(thm)],[c_11004,c_6548]) ).
tcf(c_11106,plain,
( neq(nil,sk4)
| ( sk4 = nil )
| ~ ssList(nil)
| ~ ssList(sk4) ),
inference(instantiation,[status(thm)],[c_343]) ).
tcf(c_11346,plain,
! [X0: $i] :
( ( app(cons(X0,nil),sk4) = cons(X0,sk4) )
| ~ ssItem(X0) ),
inference(superposition,[status(thm)],[c_6550,c_363]) ).
tcf(c_11379,plain,
! [X0: $i] :
( ( app(cons(X0,nil),iPr_def_14) = cons(X0,iPr_def_14) )
| ~ ssItem(X0) ),
inference(superposition,[status(thm)],[c_9616,c_363]) ).
tcf(c_11658,plain,
app(cons(iPr_def_12,nil),sk4) = cons(iPr_def_12,sk4),
inference(superposition,[status(thm)],[c_9640,c_11346]) ).
tcf(c_11659,plain,
app(iPr_def_13,sk4) = cons(iPr_def_12,sk4),
inference(light_normalisation,[status(thm)],[c_11658,c_6544]) ).
tcf(c_14789,plain,
! [X0: $i,X1: $i] :
( ( app(cons(X1,sk4),X0) = cons(X1,app(sk4,X0)) )
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(superposition,[status(thm)],[c_6550,c_400]) ).
tcf(c_14992,plain,
! [X0: $i,X1: $i] :
( neq(X0,X1)
| ~ neq(nil,sk4)
| ( X1 != sk4 )
| ( X0 != nil ) ),
inference(instantiation,[status(thm)],[c_6556]) ).
tcf(c_14993,plain,
( neq(nil,nil)
| ~ neq(nil,sk4)
| ( nil != nil )
| ( nil != sk4 ) ),
inference(instantiation,[status(thm)],[c_14992]) ).
tcf(c_15740,plain,
! [X0: $i] :
( ( app(cons(X0,sk4),sk4) = cons(X0,app(sk4,sk4)) )
| ~ ssItem(X0) ),
inference(superposition,[status(thm)],[c_6550,c_14789]) ).
tcf(c_17287,plain,
app(cons(iPr_def_12,sk4),sk4) = cons(iPr_def_12,app(sk4,sk4)),
inference(superposition,[status(thm)],[c_9640,c_15740]) ).
tcf(c_17404,plain,
! [X0: $i] :
( memberP(nil,X0)
| ( X0 = iPr_def_12 )
| ~ ssItem(iPr_def_12)
| ~ ssList(nil)
| ~ ssItem(X0)
| ~ memberP(iPr_def_13,X0) ),
inference(superposition,[status(thm)],[c_6544,c_404]) ).
tcf(c_17412,plain,
! [X0: $i] :
( memberP(nil,X0)
| ( X0 = iPr_def_12 )
| ~ ssItem(X0)
| ~ memberP(iPr_def_13,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_17404,c_9640,c_251]) ).
tcf(c_18873,plain,
( singletonP(iPr_def_13)
| ~ ssItem(iPr_def_12) ),
inference(superposition,[status(thm)],[c_6544,c_10051]) ).
tcf(c_18875,plain,
singletonP(iPr_def_13),
inference(forward_subsumption_resolution,[status(thm)],[c_18873,c_9640]) ).
tcf(c_18879,plain,
( ( cons(skaf44(iPr_def_13),nil) = iPr_def_13 )
| ~ ssList(iPr_def_13) ),
inference(superposition,[status(thm)],[c_18875,c_344]) ).
tcf(c_18880,plain,
cons(skaf44(iPr_def_13),nil) = iPr_def_13,
inference(forward_subsumption_resolution,[status(thm)],[c_18879,c_9700]) ).
tcf(c_22860,plain,
( memberP(iPr_def_13,skaf44(iPr_def_13))
| ~ ssList(nil)
| ~ ssItem(skaf44(iPr_def_13)) ),
inference(superposition,[status(thm)],[c_18880,c_381]) ).
tcf(c_22894,plain,
memberP(iPr_def_13,skaf44(iPr_def_13)),
inference(forward_subsumption_resolution,[status(thm)],[c_22860,c_251,c_290]) ).
tcf(c_27096,plain,
( ssList(cons(iPr_def_12,sk4))
| ~ ssList(iPr_def_13)
| ~ ssList(sk4) ),
inference(superposition,[status(thm)],[c_11659,c_328]) ).
tcf(c_27100,plain,
! [X0: $i] :
( memberP(cons(iPr_def_12,sk4),X0)
| ~ ssList(iPr_def_13)
| ~ ssList(sk4)
| ~ ssItem(X0)
| ~ memberP(iPr_def_13,X0) ),
inference(superposition,[status(thm)],[c_11659,c_383]) ).
tcf(c_27106,plain,
ssList(cons(iPr_def_12,sk4)),
inference(forward_subsumption_resolution,[status(thm)],[c_27096,c_9700,c_6550]) ).
tcf(c_27115,plain,
! [X0: $i] :
( memberP(cons(iPr_def_12,sk4),X0)
| ~ ssItem(X0)
| ~ memberP(iPr_def_13,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_27100,c_9700,c_6550]) ).
tcf(c_27211,plain,
app(nil,cons(iPr_def_12,sk4)) = cons(iPr_def_12,sk4),
inference(superposition,[status(thm)],[c_27106,c_317]) ).
tcf(c_27396,plain,
! [X0: $i] :
( memberP(sk4,X0)
| ( X0 = iPr_def_12 )
| ~ ssItem(iPr_def_12)
| ~ ssList(sk4)
| ~ ssItem(X0)
| ~ memberP(iPr_def_13,X0) ),
inference(superposition,[status(thm)],[c_27115,c_404]) ).
tcf(c_27397,plain,
! [X0: $i] :
( memberP(sk4,X0)
| ( X0 = iPr_def_12 )
| ~ ssItem(X0)
| ~ memberP(iPr_def_13,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_27396,c_9640,c_6550]) ).
tcf(c_27724,plain,
! [X0: $i] :
( ~ memberP(iPr_def_13,X0)
| ~ ssItem(X0)
| ( X0 = iPr_def_12 ) ),
inference(global_subsumption_just,[status(thm)],[c_27397,c_314,c_17412]) ).
tcf(c_27725,plain,
! [X0: $i] :
( ( X0 = iPr_def_12 )
| ~ ssItem(X0)
| ~ memberP(iPr_def_13,X0) ),
inference(renaming,[status(thm)],[c_27724]) ).
tcf(c_27734,plain,
( ( skaf44(iPr_def_13) = iPr_def_12 )
| ~ ssItem(skaf44(iPr_def_13)) ),
inference(superposition,[status(thm)],[c_22894,c_27725]) ).
tcf(c_27737,plain,
skaf44(iPr_def_13) = iPr_def_12,
inference(forward_subsumption_resolution,[status(thm)],[c_27734,c_290]) ).
tcf(c_27741,plain,
cons(iPr_def_12,nil) = iPr_def_13,
inference(demodulation,[status(thm)],[c_18880,c_27737]) ).
tcf(c_29704,plain,
( neq(sk4,nil)
| ( nil = sk4 )
| ~ ssList(nil)
| ~ ssList(sk4) ),
inference(instantiation,[status(thm)],[c_343]) ).
tcf(c_35619,plain,
! [X0: $i] :
( ~ ssItem(iPr_def_12)
| ~ ssList(nil)
| ~ ssList(sk4)
| ~ ssList(X0)
| ~ ssList(app(cons(iPr_def_12,sk4),cons(iPr_def_12,X0)))
| ~ duplicatefreeP(app(app(nil,cons(iPr_def_12,sk4)),cons(iPr_def_12,X0))) ),
inference(superposition,[status(thm)],[c_27211,c_422]) ).
tcf(c_35647,plain,
! [X0: $i] :
( ~ ssItem(iPr_def_12)
| ~ ssList(nil)
| ~ ssList(sk4)
| ~ ssList(X0)
| ~ duplicatefreeP(app(cons(iPr_def_12,sk4),cons(iPr_def_12,X0)))
| ~ ssList(app(cons(iPr_def_12,sk4),cons(iPr_def_12,X0))) ),
inference(light_normalisation,[status(thm)],[c_35619,c_27211]) ).
tcf(c_35648,plain,
! [X0: $i] :
( ~ ssList(X0)
| ~ duplicatefreeP(app(cons(iPr_def_12,sk4),cons(iPr_def_12,X0)))
| ~ ssList(app(cons(iPr_def_12,sk4),cons(iPr_def_12,X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_35647,c_9640,c_251,c_6550]) ).
tcf(c_35745,plain,
( ~ ssList(iPr_def_14)
| ~ ssList(app(cons(iPr_def_12,sk4),sk4))
| ~ duplicatefreeP(app(cons(iPr_def_12,sk4),cons(iPr_def_12,iPr_def_14))) ),
inference(superposition,[status(thm)],[c_11005,c_35648]) ).
tcf(c_35747,plain,
( ~ ssList(iPr_def_14)
| ~ duplicatefreeP(cons(iPr_def_12,app(sk4,sk4)))
| ~ ssList(cons(iPr_def_12,app(sk4,sk4))) ),
inference(light_normalisation,[status(thm)],[c_35745,c_11005,c_17287]) ).
tcf(c_35748,plain,
( ~ duplicatefreeP(cons(iPr_def_12,app(sk4,sk4)))
| ~ ssList(cons(iPr_def_12,app(sk4,sk4))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_35747,c_9616]) ).
tcf(c_37022,plain,
! [X0: $i] :
( ssList(app(sk4,X0))
| ~ ssList(sk4)
| ~ ssList(X0) ),
inference(instantiation,[status(thm)],[c_328]) ).
tcf(c_116047,plain,
( ssList(cons(iPr_def_12,app(sk4,sk4)))
| ~ ssList(sk4)
| ~ ssList(cons(iPr_def_12,sk4)) ),
inference(superposition,[status(thm)],[c_17287,c_328]) ).
tcf(c_116084,plain,
ssList(cons(iPr_def_12,app(sk4,sk4))),
inference(forward_subsumption_resolution,[status(thm)],[c_116047,c_6550,c_27106]) ).
tcf(c_116406,plain,
( duplicatefreeP(cons(iPr_def_12,app(sk4,sk4)))
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_116084,c_6541]) ).
tcf(c_116817,plain,
~ iPr_def_11,
inference(global_subsumption_just,[status(thm)],[c_116406,c_35748,c_116084,c_116406]) ).
tcf(c_116819,plain,
iPr_def_10,
inference(backward_subsumption_resolution,[status(thm)],[c_6542,c_116817]) ).
tcf(c_116845,plain,
! [X0: $i] : ssItem(X0),
inference(backward_subsumption_resolution,[status(thm)],[c_6540,c_116819]) ).
tcf(c_116983,plain,
! [X0: $i,X1: $i] :
( ( app(cons(X1,nil),X0) = cons(X1,X0) )
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_363,c_116845]) ).
tcf(c_116991,plain,
! [X0: $i,X1: $i] :
( neq(X1,X0)
| ( X0 = X1 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_345,c_116845]) ).
tcf(c_116994,plain,
! [X0: $i,X1: $i] :
( ( hd(cons(X1,X0)) = X1 )
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_340,c_116845]) ).
tcf(c_116995,plain,
! [X0: $i,X1: $i] :
( ( tl(cons(X1,X0)) = X0 )
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_339,c_116845]) ).
tcf(c_116996,plain,
! [X0: $i,X1: $i] :
( ssList(cons(X1,X0))
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_329,c_116845]) ).
tcf(c_129254,plain,
! [X0: $i] : app(cons(X0,nil),iPr_def_14) = cons(X0,iPr_def_14),
inference(global_subsumption_just,[status(thm)],[c_11379,c_6540,c_6542,c_11379,c_35748,c_116084,c_116406]) ).
tcf(c_129257,plain,
app(iPr_def_13,iPr_def_14) = cons(iPr_def_12,iPr_def_14),
inference(superposition,[status(thm)],[c_27741,c_129254]) ).
tcf(c_129273,plain,
app(iPr_def_13,iPr_def_14) = sk4,
inference(light_normalisation,[status(thm)],[c_129257,c_11005]) ).
tcf(c_129486,plain,
! [X0: $i] :
( segmentP(app(sk4,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_129273,c_416]) ).
tcf(c_129519,plain,
! [X0: $i] :
( segmentP(app(sk4,X0),iPr_def_14)
| ~ ssList(iPr_def_14)
| ~ ssList(iPr_def_13)
| ~ ssList(X0)
| ~ ssList(app(sk4,X0)) ),
inference(light_normalisation,[status(thm)],[c_129486,c_129273]) ).
tcf(c_129520,plain,
! [X0: $i] :
( segmentP(app(sk4,X0),iPr_def_14)
| ~ ssList(X0)
| ~ ssList(app(sk4,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_129519,c_9616,c_9700]) ).
tcf(c_137710,plain,
! [X0: $i] :
( segmentP(app(sk4,X0),iPr_def_14)
| ~ ssList(X0) ),
inference(global_subsumption_just,[status(thm)],[c_129520,c_432,c_37022,c_129520]) ).
tcf(c_153775,plain,
iPr_def_15 = sk3,
inference(global_subsumption_just,[status(thm)],[c_6547,c_432,c_251,c_326,c_482,c_434,c_435,c_497,c_6547,c_9616,c_9640,c_9700,c_11106,c_14993,c_29704]) ).
tcf(c_153777,plain,
! [X0: $i] :
( ~ ssList(X0)
| ~ segmentP(iPr_def_15,X0)
| ~ segmentP(sk4,X0)
| ~ neq(X0,nil) ),
inference(demodulation,[status(thm)],[c_6549,c_153775]) ).
tcf(c_153778,plain,
ssList(iPr_def_15),
inference(demodulation,[status(thm)],[c_6551,c_153775]) ).
tcf(c_153842,plain,
app(sk4,nil) = sk4,
inference(superposition,[status(thm)],[c_6550,c_316]) ).
tcf(c_153871,plain,
app(iPr_def_15,nil) = iPr_def_15,
inference(superposition,[status(thm)],[c_153778,c_316]) ).
tcf(c_153920,plain,
( ssList(iPr_def_14)
| ( sk4 = nil )
| ~ ssList(sk4) ),
inference(superposition,[status(thm)],[c_6545,c_320]) ).
tcf(c_153923,plain,
ssList(iPr_def_14),
inference(forward_subsumption_resolution,[status(thm)],[c_153920,c_6548,c_6550]) ).
tcf(c_153958,plain,
app(nil,iPr_def_14) = iPr_def_14,
inference(superposition,[status(thm)],[c_153923,c_317]) ).
tcf(c_153972,plain,
! [X0: $i,X1: $i] :
( ssList(cons(X1,X0))
| ~ ssList(X0) ),
inference(global_subsumption_just,[status(thm)],[c_329,c_116996]) ).
tcf(c_153978,plain,
( ssList(iPr_def_13)
| ~ ssList(nil) ),
inference(superposition,[status(thm)],[c_6544,c_153972]) ).
tcf(c_153981,plain,
ssList(iPr_def_13),
inference(forward_subsumption_resolution,[status(thm)],[c_153978,c_251]) ).
tcf(c_154534,plain,
! [X0: $i] : singletonP(cons(X0,nil)),
inference(global_subsumption_just,[status(thm)],[c_359,c_6540,c_6542,c_10051,c_35748,c_116084,c_116406]) ).
tcf(c_154536,plain,
singletonP(iPr_def_13),
inference(superposition,[status(thm)],[c_6544,c_154534]) ).
tcf(c_154537,plain,
! [X0: $i,X1: $i] :
( ( tl(cons(X1,X0)) = X0 )
| ~ ssList(X0) ),
inference(global_subsumption_just,[status(thm)],[c_339,c_116995]) ).
tcf(c_154544,plain,
! [X0: $i] : tl(cons(X0,nil)) = nil,
inference(superposition,[status(thm)],[c_251,c_154537]) ).
tcf(c_154576,plain,
! [X0: $i] : tl(cons(X0,iPr_def_14)) = iPr_def_14,
inference(superposition,[status(thm)],[c_153923,c_154537]) ).
tcf(c_154620,plain,
! [X0: $i,X1: $i] :
( ( hd(cons(X1,X0)) = X1 )
| ~ ssList(X0) ),
inference(global_subsumption_just,[status(thm)],[c_340,c_116994]) ).
tcf(c_154627,plain,
! [X0: $i] : hd(cons(X0,nil)) = X0,
inference(superposition,[status(thm)],[c_251,c_154620]) ).
tcf(c_154659,plain,
! [X0: $i] : hd(cons(X0,iPr_def_14)) = X0,
inference(superposition,[status(thm)],[c_153923,c_154620]) ).
tcf(c_154698,plain,
! [X0: $i,X1: $i] :
( ( cons(X0,X1) != nil )
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_341,c_341,c_6540,c_6542,c_35748,c_116084,c_116406]) ).
tcf(c_154699,plain,
! [X0: $i,X1: $i] :
( ~ ssList(X1)
| ( cons(X0,X1) != nil ) ),
inference(renaming,[status(thm)],[c_154698]) ).
tcf(c_154704,plain,
( ~ ssList(nil)
| ( nil != iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_6544,c_154699]) ).
tcf(c_154705,plain,
nil != iPr_def_13,
inference(forward_subsumption_resolution,[status(thm)],[c_154704,c_251]) ).
tcf(c_154737,plain,
! [X0: $i,X1: $i] :
( neq(X1,X0)
| ( X0 = X1 ) ),
inference(global_subsumption_just,[status(thm)],[c_343,c_116991]) ).
tcf(c_154743,plain,
! [X0: $i] :
( ( X0 = nil )
| ~ ssList(X0)
| ~ segmentP(iPr_def_15,X0)
| ~ segmentP(sk4,X0) ),
inference(superposition,[status(thm)],[c_154737,c_153777]) ).
tcf(c_154756,plain,
( ( cons(skaf44(iPr_def_13),nil) = iPr_def_13 )
| ~ ssList(iPr_def_13) ),
inference(superposition,[status(thm)],[c_154536,c_344]) ).
tcf(c_154757,plain,
cons(skaf44(iPr_def_13),nil) = iPr_def_13,
inference(forward_subsumption_resolution,[status(thm)],[c_154756,c_153981]) ).
tcf(c_154803,plain,
( ( sk4 = nil )
| ~ ssList(sk4)
| ~ segmentP(iPr_def_15,sk4) ),
inference(superposition,[status(thm)],[c_300,c_154743]) ).
tcf(c_154804,plain,
~ segmentP(iPr_def_15,sk4),
inference(forward_subsumption_resolution,[status(thm)],[c_154803,c_6548,c_6550]) ).
tcf(c_154924,plain,
( ( sk4 = nil )
| ( cons(hd(sk4),tl(sk4)) = sk4 ) ),
inference(superposition,[status(thm)],[c_6550,c_347]) ).
tcf(c_154965,plain,
( ( sk4 = nil )
| ( cons(iPr_def_12,iPr_def_14) = sk4 ) ),
inference(light_normalisation,[status(thm)],[c_154924,c_6543,c_6545]) ).
tcf(c_154966,plain,
cons(iPr_def_12,iPr_def_14) = sk4,
inference(forward_subsumption_resolution,[status(thm)],[c_154965,c_6548]) ).
tcf(c_155074,plain,
hd(sk4) = iPr_def_12,
inference(superposition,[status(thm)],[c_154966,c_154659]) ).
tcf(c_155075,plain,
tl(sk4) = iPr_def_14,
inference(superposition,[status(thm)],[c_154966,c_154576]) ).
tcf(c_155291,plain,
! [X0: $i,X1: $i] :
( ( app(cons(X1,nil),X0) = cons(X1,X0) )
| ~ ssList(X0) ),
inference(global_subsumption_just,[status(thm)],[c_363,c_116983]) ).
tcf(c_155330,plain,
! [X0: $i] : app(cons(X0,nil),iPr_def_14) = cons(X0,iPr_def_14),
inference(superposition,[status(thm)],[c_153923,c_155291]) ).
tcf(c_166183,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_6546,c_416]) ).
tcf(c_166240,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_153958,c_416]) ).
tcf(c_166302,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_166240,c_153958]) ).
tcf(c_166303,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_166302,c_153923,c_251]) ).
tcf(c_166317,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_166183,c_6546]) ).
tcf(c_166318,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_166317,c_153923,c_153981]) ).
tcf(c_168831,plain,
! [X0: $i] :
( ( sk4 = nil )
| ( X0 = nil )
| ( X0 = sk4 )
| ~ ssList(sk4)
| ~ ssList(X0)
| ( hd(X0) != hd(sk4) )
| ( tl(X0) != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_155075,c_420]) ).
tcf(c_168838,plain,
! [X0: $i] :
( ( sk4 = nil )
| ( X0 = nil )
| ( X0 = sk4 )
| ~ ssList(sk4)
| ~ ssList(X0)
| ( hd(X0) != iPr_def_12 )
| ( tl(X0) != iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_168831,c_155074]) ).
tcf(c_168839,plain,
! [X0: $i] :
( ( X0 = nil )
| ( X0 = sk4 )
| ~ ssList(X0)
| ( hd(X0) != iPr_def_12 )
| ( tl(X0) != iPr_def_14 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_168838,c_6548,c_6550]) ).
tcf(c_173224,plain,
tl(iPr_def_13) = nil,
inference(superposition,[status(thm)],[c_6544,c_154544]) ).
tcf(c_173585,plain,
hd(iPr_def_13) = iPr_def_12,
inference(superposition,[status(thm)],[c_6544,c_154627]) ).
tcf(c_173628,plain,
hd(iPr_def_13) = skaf44(iPr_def_13),
inference(superposition,[status(thm)],[c_154757,c_154627]) ).
tcf(c_173678,plain,
skaf44(iPr_def_13) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_173628,c_173585]) ).
tcf(c_173814,plain,
cons(iPr_def_12,nil) = iPr_def_13,
inference(demodulation,[status(thm)],[c_154757,c_173678]) ).
tcf(c_174524,plain,
( ( nil = iPr_def_13 )
| ( sk4 = iPr_def_13 )
| ~ ssList(iPr_def_13)
| ( nil != iPr_def_14 )
| ( hd(iPr_def_13) != iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_173224,c_168839]) ).
tcf(c_174526,plain,
( ( nil = iPr_def_13 )
| ( sk4 = iPr_def_13 )
| ~ ssList(iPr_def_13)
| ( nil != iPr_def_14 ) ),
inference(ground_joinability,[status(thm)],[c_174524,c_173585]) ).
tcf(c_174527,plain,
( ( sk4 = iPr_def_13 )
| ( nil != iPr_def_14 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_174526,c_154705,c_153981]) ).
tcf(c_177359,plain,
app(iPr_def_13,iPr_def_14) = cons(iPr_def_12,iPr_def_14),
inference(superposition,[status(thm)],[c_173814,c_155330]) ).
tcf(c_177378,plain,
app(iPr_def_13,iPr_def_14) = sk4,
inference(light_normalisation,[status(thm)],[c_177359,c_154966]) ).
tcf(c_177527,plain,
! [X0: $i] :
( segmentP(app(sk4,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_177378,c_416]) ).
tcf(c_177574,plain,
! [X0: $i] :
( segmentP(app(sk4,X0),iPr_def_14)
| ~ ssList(iPr_def_14)
| ~ ssList(iPr_def_13)
| ~ ssList(X0)
| ~ ssList(app(sk4,X0)) ),
inference(light_normalisation,[status(thm)],[c_177527,c_177378]) ).
tcf(c_177575,plain,
! [X0: $i] :
( segmentP(app(sk4,X0),iPr_def_14)
| ~ ssList(X0)
| ~ ssList(app(sk4,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_177574,c_153923,c_153981]) ).
tcf(c_229888,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_6546,c_166303]) ).
tcf(c_229896,plain,
( segmentP(iPr_def_15,iPr_def_14)
| ~ ssList(iPr_def_15)
| ~ ssList(iPr_def_13) ),
inference(light_normalisation,[status(thm)],[c_229888,c_6546]) ).
tcf(c_229897,plain,
segmentP(iPr_def_15,iPr_def_14),
inference(forward_subsumption_resolution,[status(thm)],[c_229896,c_153778,c_153981]) ).
tcf(c_230840,plain,
( segmentP(iPr_def_15,iPr_def_13)
| ~ ssList(nil)
| ~ ssList(app(iPr_def_15,nil)) ),
inference(superposition,[status(thm)],[c_153871,c_166318]) ).
tcf(c_230845,plain,
( segmentP(iPr_def_15,iPr_def_13)
| ~ ssList(iPr_def_15)
| ~ ssList(nil) ),
inference(light_normalisation,[status(thm)],[c_230840,c_153871]) ).
tcf(c_230846,plain,
segmentP(iPr_def_15,iPr_def_13),
inference(forward_subsumption_resolution,[status(thm)],[c_230845,c_153778,c_251]) ).
tcf(c_233795,plain,
! [X0: $i] :
( segmentP(app(sk4,X0),iPr_def_14)
| ~ ssList(X0) ),
inference(global_subsumption_just,[status(thm)],[c_177575,c_137710]) ).
tcf(c_233801,plain,
( segmentP(sk4,iPr_def_14)
| ~ ssList(nil) ),
inference(superposition,[status(thm)],[c_153842,c_233795]) ).
tcf(c_233806,plain,
segmentP(sk4,iPr_def_14),
inference(forward_subsumption_resolution,[status(thm)],[c_233801,c_251]) ).
tcf(c_234763,plain,
( ( nil = iPr_def_14 )
| ~ ssList(iPr_def_14)
| ~ segmentP(iPr_def_15,iPr_def_14) ),
inference(superposition,[status(thm)],[c_233806,c_154743]) ).
tcf(c_234764,plain,
nil = iPr_def_14,
inference(forward_subsumption_resolution,[status(thm)],[c_234763,c_153923,c_229897]) ).
tcf(c_234771,plain,
sk4 = iPr_def_13,
inference(backward_subsumption_resolution,[status(thm)],[c_174527,c_234764]) ).
tcf(c_235883,plain,
~ segmentP(iPr_def_15,iPr_def_13),
inference(demodulation,[status(thm)],[c_154804,c_234771]) ).
tcf(c_235891,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_235883,c_230846]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC072-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.11/0.39 % Computer : n019.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Thu Sep 24 16:14:42 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.43 Running first-order theorem proving
% 0.11/0.43 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.11/0.44
% 0.11/0.44 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.44
% 0.11/0.44 % Detected problem language: tptp
% 0.11/0.45 % Proving...
% 64.48/16.91 % SZS status Started for theBenchmark.p
% 64.48/16.91 % SZS status Unsatisfiable for theBenchmark.p
% 64.48/16.91
% 64.48/16.91 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 64.48/16.91
% 64.48/16.91 % ------ iProver source info
% 64.48/16.91
% 64.48/16.91 % git: date: 2026-07-19 20:42:38 +0200
% 64.48/16.91 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 64.48/16.91 % git: non_committed_changes: false
% 64.48/16.91
% 64.48/16.91 % ------ Parsing...% successful
% 64.48/16.91
% 64.48/16.91
% 64.48/16.91 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 64.48/16.91
% 64.48/16.91 % ------ 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 %
% 64.48/16.91
% 64.48/16.91 % ------ Preprocessing... gs_s sp: 2 0s gs_e snvd_s sp: 0 0s snvd_e %
% 64.48/16.91
% 64.48/16.91 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 64.48/16.91 % ------ Proving...
% 64.48/16.91 % ------ Problem Properties
% 64.48/16.91
% 64.48/16.91 %
% 64.48/16.91 % clauses 190
% 64.48/16.91 % conjectures 4
% 64.48/16.91 % EPR 61
% 64.48/16.91 % Horn 160
% 64.48/16.91 % unary 65
% 64.48/16.91 % binary 23
% 64.48/16.91 % lits 570
% 64.48/16.91 % lits eq 77
% 64.48/16.91 % fd_pure 0
% 64.48/16.91 % fd_pseudo 0
% 64.48/16.91 % fd_cond 15
% 64.48/16.91 % fd_pseudo_cond 16
% 64.48/16.91 % AC symbols 0
% 64.48/16.91
% 64.48/16.91 % ------ Schedule dynamic 5 is on
% 64.48/16.91
% 64.48/16.91 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 64.48/16.91
% 64.48/16.91
% 64.48/16.91 % ------
% 64.48/16.91 % Current options:
% 64.48/16.91 % ------
% 64.48/16.91
% 64.48/16.91
% 64.48/16.91 %
% 64.48/16.91
% 64.48/16.91 % ------ Proving...
% 64.48/16.91 % Proof_search_loop: time out after: 6109 full_loop iterations
% 64.48/16.91
% 64.48/16.91 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" Time Limit: 15.
% 64.48/16.91
% 64.48/16.91
% 64.48/16.91 % ------
% 64.48/16.91 % Current options:
% 64.48/16.91 % ------
% 64.48/16.91
% 64.48/16.91
% 64.48/16.91 %
% 64.48/16.91
% 64.48/16.91 % ------ Proving...
% 64.48/16.91 %
% 64.48/16.91
% 64.48/16.91 % SZS status Unsatisfiable for theBenchmark.p
% 64.48/16.91
% 64.48/16.91 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 64.48/16.92
% 64.48/16.92
%------------------------------------------------------------------------------