%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWC089-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 : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:07:50 PM UTC 2026
% Result : Unsatisfiable 65.13s 9.92s
% Output : CNFRefutation 65.13s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f249ERROR: Could not build tree for root c_127978ERROR: 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(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(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(f129,axiom,
! [X0,X1] :
( hd(app(X1,X0)) = hd(X1)
| nil = X1
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause123) ).
fof(f144,axiom,
! [X0,X1] :
( tl(app(X1,X0)) = app(tl(X1),X0)
| nil = X1
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause133) ).
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(f163,axiom,
! [X2,X0,X1] :
( X0 = X2
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| app(X0,X1) != app(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause151) ).
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,
neq(sk2,nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_7) ).
fof(f207,negated_conjecture,
! [X0] :
( ~ segmentP(sk1,X0)
| ~ segmentP(sk2,X0)
| ~ neq(X0,nil)
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_8) ).
fof(f209,negated_conjecture,
( neq(sk3,nil)
| ~ neq(sk4,nil) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_10) ).
fof(f213,plain,
neq(sk4,nil),
inference(definition_unfolding,[],[f206,f204]) ).
fof(f214,plain,
! [X0] :
( ~ segmentP(sk3,X0)
| ~ segmentP(sk4,X0)
| ~ neq(X0,nil)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f207,f204,f205]) ).
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_291,plain,
! [X0: $i] : ssItem(skaf44(X0)),
inference(cnf_transformation,[],[f47]) ).
tcf(c_301,plain,
! [X0: $i] :
( segmentP(X0,X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f57]) ).
tcf(c_315,plain,
! [X0: $i] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
inference(cnf_transformation,[],[f71]) ).
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_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_348,plain,
! [X0: $i] :
( ( X0 = nil )
| ( cons(hd(X0),tl(X0)) = X0 )
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f107]) ).
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_367,plain,
! [X0: $i,X1: $i] :
( ( X1 = nil )
| ( hd(app(X1,X0)) = hd(X1) )
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f129]) ).
tcf(c_377,plain,
! [X0: $i,X1: $i] :
( ( X1 = nil )
| ( tl(app(X1,X0)) = app(tl(X1),X0) )
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f144]) ).
tcf(c_382,plain,
! [X0: $i,X1: $i] :
( memberP(cons(X1,X0),X1)
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f246]) ).
tcf(c_384,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_395,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = X2 )
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(X0,X1) != app(X2,X1) ) ),
inference(cnf_transformation,[],[f163]) ).
tcf(c_401,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_405,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_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,
neq(sk4,nil),
inference(cnf_transformation,[],[f213]) ).
tcf(c_435,negated_conjecture,
! [X0: $i] :
( ~ ssList(X0)
| ~ segmentP(sk4,X0)
| ~ segmentP(sk3,X0)
| ~ neq(X0,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_552,negated_conjecture,
neq(sk3,nil),
inference(global_subsumption_just,[status(thm)],[c_437,c_434,c_437]) ).
tcf(c_560,plain,
( ( app(tl(sk3),cons(hd(sk3),nil)) = sk4 )
| ~ ssItem(hd(sk3))
| ~ neq(nil,sk3)
| ~ ssList(app(tl(sk3),cons(hd(sk3),nil)))
| ~ ssList(cons(hd(sk3),nil))
| ~ ssList(tl(sk3)) ),
inference(global_subsumption_just,[status(thm)],[c_438,c_434,c_438]) ).
tcf(c_561,negated_conjecture,
( ( app(tl(sk3),cons(hd(sk3),nil)) = sk4 )
| ~ ssItem(hd(sk3))
| ~ neq(nil,sk3)
| ~ ssList(tl(sk3))
| ~ ssList(cons(hd(sk3),nil))
| ~ ssList(app(tl(sk3),cons(hd(sk3),nil))) ),
inference(renaming,[status(thm)],[c_560]) ).
tcf(c_799,plain,
( ( app(tl(sk3),cons(hd(sk3),nil)) = sk4 )
| ~ ssItem(hd(sk3))
| ~ neq(nil,sk3)
| ~ ssList(tl(sk3))
| ~ ssList(cons(hd(sk3),nil)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_561,c_329]) ).
tcf(c_3581,plain,
! [X0: $i] :
( ~ ssList(X0)
| ~ segmentP(sk4,X0)
| ~ segmentP(sk3,X0)
| ( nil != nil )
| ( X0 != sk3 ) ),
inference(resolution_lifted,[status(thm)],[c_435,c_552]) ).
tcf(c_3582,plain,
( ~ ssList(sk3)
| ~ segmentP(sk4,sk3)
| ~ segmentP(sk3,sk3) ),
inference(unflattening,[status(thm)],[c_3581]) ).
tcf(c_3583,plain,
( ~ segmentP(sk3,sk3)
| ~ segmentP(sk4,sk3) ),
inference(global_subsumption_just,[status(thm)],[c_3582,c_432,c_3582]) ).
tcf(c_3584,plain,
( ~ segmentP(sk4,sk3)
| ~ segmentP(sk3,sk3) ),
inference(renaming,[status(thm)],[c_3583]) ).
tcf(c_3612,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X1 = X2 )
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ segmentP(sk4,X0)
| ~ segmentP(sk3,X0)
| ( X2 != nil )
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_435,c_344]) ).
tcf(c_3613,plain,
! [X0: $i] :
( ( X0 = nil )
| ~ ssList(nil)
| ~ ssList(X0)
| ~ segmentP(sk4,X0)
| ~ segmentP(sk3,X0) ),
inference(unflattening,[status(thm)],[c_3612]) ).
tcf(c_3615,plain,
! [X0: $i] :
( ( X0 = nil )
| ~ segmentP(sk3,X0)
| ~ segmentP(sk4,X0)
| ~ ssList(X0) ),
inference(global_subsumption_just,[status(thm)],[c_3613,c_252,c_3613]) ).
tcf(c_3616,plain,
! [X0: $i] :
( ( X0 = nil )
| ~ ssList(X0)
| ~ segmentP(sk4,X0)
| ~ segmentP(sk3,X0) ),
inference(renaming,[status(thm)],[c_3615]) ).
tcf(c_3686,plain,
! [X0: $i] :
( ~ ssList(X0)
| ( X0 != nil )
| ( X0 != sk3 ) ),
inference(resolution_lifted,[status(thm)],[c_552,c_359]) ).
tcf(c_3687,plain,
( ~ ssList(sk3)
| ( sk3 != nil ) ),
inference(unflattening,[status(thm)],[c_3686]) ).
tcf(c_3688,plain,
sk3 != nil,
inference(global_subsumption_just,[status(thm)],[c_3687,c_432,c_3687]) ).
tcf(c_3715,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ( app(tl(sk3),cons(hd(sk3),nil)) = sk4 )
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssItem(hd(sk3))
| ~ ssList(tl(sk3))
| ~ ssList(cons(hd(sk3),nil))
| ( X1 != nil )
| ( X0 != sk3 ) ),
inference(resolution_lifted,[status(thm)],[c_799,c_344]) ).
tcf(c_3716,plain,
( ( sk3 = nil )
| ( app(tl(sk3),cons(hd(sk3),nil)) = sk4 )
| ~ ssList(nil)
| ~ ssList(sk3)
| ~ ssItem(hd(sk3))
| ~ ssList(tl(sk3))
| ~ ssList(cons(hd(sk3),nil)) ),
inference(unflattening,[status(thm)],[c_3715]) ).
tcf(c_3717,plain,
( ~ ssList(cons(hd(sk3),nil))
| ~ ssList(tl(sk3))
| ~ ssItem(hd(sk3))
| ( app(tl(sk3),cons(hd(sk3),nil)) = sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_3716,c_432,c_252,c_3687,c_3716]) ).
tcf(c_3718,plain,
( ( app(tl(sk3),cons(hd(sk3),nil)) = sk4 )
| ~ ssItem(hd(sk3))
| ~ ssList(tl(sk3))
| ~ ssList(cons(hd(sk3),nil)) ),
inference(renaming,[status(thm)],[c_3717]) ).
tcf(c_6691,plain,
! [X0: $i] :
( ~ iPr_def_10
| ssItem(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_316]) ).
tcf(c_6692,plain,
! [X0: $i] :
( ~ iPr_def_11
| ~ ssList(X0)
| duplicatefreeP(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_316]) ).
tcf(c_6693,plain,
( iPr_def_11
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_316]) ).
tcf(c_6694,definition,
iPr_def_12 = hd(sk3),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_6695,definition,
iPr_def_13 = cons(iPr_def_12,nil),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_6696,definition,
iPr_def_14 = tl(sk3),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_6697,definition,
iPr_def_15 = app(iPr_def_14,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_6698,plain,
( ( iPr_def_15 = sk4 )
| ~ ssItem(iPr_def_12)
| ~ ssList(iPr_def_14)
| ~ ssList(iPr_def_13) ),
inference(demodulation,[status(thm)],[c_3718,c_6697,c_6696,c_6694,c_6695]) ).
tcf(c_6699,plain,
sk3 != nil,
inference(demodulation,[status(thm)],[c_3688]) ).
tcf(c_6701,plain,
! [X0: $i] :
( ( X0 = nil )
| ~ ssList(X0)
| ~ segmentP(sk4,X0)
| ~ segmentP(sk3,X0) ),
inference(demodulation,[status(thm)],[c_3616]) ).
tcf(c_6702,plain,
( ~ segmentP(sk4,sk3)
| ~ segmentP(sk3,sk3) ),
inference(demodulation,[status(thm)],[c_3584]) ).
tcf(c_6704,negated_conjecture,
ssList(sk4),
inference(demodulation,[status(thm)],[c_433]) ).
tcf(c_6705,negated_conjecture,
ssList(sk3),
inference(demodulation,[status(thm)],[c_432]) ).
tcf(c_9280,plain,
( ( sk4 = iPr_def_15 )
| ~ iPr_def_10
| ~ ssList(iPr_def_14)
| ~ ssList(iPr_def_13) ),
inference(superposition,[status(thm)],[c_6691,c_6698]) ).
tcf(c_9307,plain,
( ~ ssList(sk3)
| ~ segmentP(sk4,sk3) ),
inference(superposition,[status(thm)],[c_301,c_6702]) ).
tcf(c_9308,plain,
~ segmentP(sk4,sk3),
inference(forward_subsumption_resolution,[status(thm)],[c_9307,c_6705]) ).
tcf(c_9395,plain,
app(sk3,nil) = sk3,
inference(superposition,[status(thm)],[c_6705,c_317]) ).
tcf(c_9396,plain,
app(sk4,nil) = sk4,
inference(superposition,[status(thm)],[c_6704,c_317]) ).
tcf(c_9650,plain,
app(nil,sk3) = sk3,
inference(superposition,[status(thm)],[c_6705,c_318]) ).
tcf(c_9713,plain,
( ssList(iPr_def_14)
| ( sk3 = nil )
| ~ ssList(sk3) ),
inference(superposition,[status(thm)],[c_6696,c_321]) ).
tcf(c_9717,plain,
ssList(iPr_def_14),
inference(forward_subsumption_resolution,[status(thm)],[c_9713,c_6699,c_6705]) ).
tcf(c_9728,plain,
( ( sk4 = iPr_def_15 )
| ~ iPr_def_10
| ~ ssList(iPr_def_13) ),
inference(backward_subsumption_resolution,[status(thm)],[c_9280,c_9717]) ).
tcf(c_9729,plain,
( ( sk4 = iPr_def_15 )
| ~ ssItem(iPr_def_12)
| ~ ssList(iPr_def_13) ),
inference(backward_subsumption_resolution,[status(thm)],[c_6698,c_9717]) ).
tcf(c_9742,plain,
( ssItem(iPr_def_12)
| ( sk3 = nil )
| ~ ssList(sk3) ),
inference(superposition,[status(thm)],[c_6694,c_322]) ).
tcf(c_9743,plain,
ssItem(iPr_def_12),
inference(forward_subsumption_resolution,[status(thm)],[c_9742,c_6699,c_6705]) ).
tcf(c_9781,plain,
app(nil,iPr_def_14) = iPr_def_14,
inference(superposition,[status(thm)],[c_9717,c_318]) ).
tcf(c_9803,plain,
( ssList(iPr_def_13)
| ~ ssItem(iPr_def_12)
| ~ ssList(nil) ),
inference(superposition,[status(thm)],[c_6695,c_330]) ).
tcf(c_9807,plain,
ssList(iPr_def_13),
inference(forward_subsumption_resolution,[status(thm)],[c_9803,c_9743,c_252]) ).
tcf(c_9853,plain,
sk4 = iPr_def_15,
inference(global_subsumption_just,[status(thm)],[c_9728,c_9729,c_9743,c_9807]) ).
tcf(c_9857,plain,
app(iPr_def_15,nil) = iPr_def_15,
inference(demodulation,[status(thm)],[c_9396,c_9853]) ).
tcf(c_9859,plain,
~ segmentP(iPr_def_15,sk3),
inference(demodulation,[status(thm)],[c_9308,c_9853]) ).
tcf(c_9860,plain,
! [X0: $i] :
( ( X0 = nil )
| ~ ssList(X0)
| ~ segmentP(iPr_def_15,X0)
| ~ segmentP(sk3,X0) ),
inference(demodulation,[status(thm)],[c_6701,c_9853]) ).
tcf(c_9862,plain,
ssList(iPr_def_15),
inference(demodulation,[status(thm)],[c_6704,c_9853]) ).
tcf(c_10128,plain,
! [X0: $i] :
( singletonP(cons(X0,nil))
| ~ ssList(nil)
| ~ ssItem(X0) ),
inference(superposition,[status(thm)],[c_330,c_360]) ).
tcf(c_10132,plain,
! [X0: $i] :
( singletonP(cons(X0,nil))
| ~ ssItem(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10128,c_252]) ).
tcf(c_10144,plain,
! [X0: $i] :
( ( tl(cons(X0,sk3)) = sk3 )
| ~ ssItem(X0) ),
inference(superposition,[status(thm)],[c_6705,c_340]) ).
tcf(c_10329,plain,
! [X0: $i] :
( ( hd(cons(X0,sk3)) = X0 )
| ~ ssItem(X0) ),
inference(superposition,[status(thm)],[c_6705,c_341]) ).
tcf(c_10491,plain,
( ~ ssItem(iPr_def_12)
| ~ ssList(nil)
| ( nil != iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_6695,c_342]) ).
tcf(c_10492,plain,
nil != iPr_def_13,
inference(forward_subsumption_resolution,[status(thm)],[c_10491,c_9743,c_252]) ).
tcf(c_10516,plain,
tl(cons(iPr_def_12,sk3)) = sk3,
inference(superposition,[status(thm)],[c_9743,c_10144]) ).
tcf(c_10593,plain,
hd(cons(iPr_def_12,sk3)) = iPr_def_12,
inference(superposition,[status(thm)],[c_9743,c_10329]) ).
tcf(c_10775,plain,
( ( sk3 = nil )
| ( cons(hd(sk3),tl(sk3)) = sk3 ) ),
inference(superposition,[status(thm)],[c_6705,c_348]) ).
tcf(c_10814,plain,
( ( sk3 = nil )
| ( cons(iPr_def_12,iPr_def_14) = sk3 ) ),
inference(light_normalisation,[status(thm)],[c_10775,c_6694,c_6696]) ).
tcf(c_10815,plain,
cons(iPr_def_12,iPr_def_14) = sk3,
inference(forward_subsumption_resolution,[status(thm)],[c_10814,c_6699]) ).
tcf(c_11121,plain,
! [X0: $i] :
( ( app(cons(X0,nil),sk3) = cons(X0,sk3) )
| ~ ssItem(X0) ),
inference(superposition,[status(thm)],[c_6705,c_364]) ).
tcf(c_11154,plain,
! [X0: $i] :
( ( app(cons(X0,nil),iPr_def_14) = cons(X0,iPr_def_14) )
| ~ ssItem(X0) ),
inference(superposition,[status(thm)],[c_9717,c_364]) ).
tcf(c_11365,plain,
app(cons(iPr_def_12,nil),sk3) = cons(iPr_def_12,sk3),
inference(superposition,[status(thm)],[c_9743,c_11121]) ).
tcf(c_11366,plain,
app(iPr_def_13,sk3) = cons(iPr_def_12,sk3),
inference(light_normalisation,[status(thm)],[c_11365,c_6695]) ).
tcf(c_11582,plain,
! [X0: $i] :
( ( X0 = nil )
| ( hd(app(X0,sk3)) = hd(X0) )
| ~ ssList(X0) ),
inference(superposition,[status(thm)],[c_6705,c_367]) ).
tcf(c_11825,plain,
( ( nil = iPr_def_13 )
| ( hd(app(iPr_def_13,sk3)) = hd(iPr_def_13) ) ),
inference(superposition,[status(thm)],[c_9807,c_11582]) ).
tcf(c_11831,plain,
( ( nil = iPr_def_13 )
| ( hd(iPr_def_13) = iPr_def_12 ) ),
inference(light_normalisation,[status(thm)],[c_11825,c_10593,c_11366]) ).
tcf(c_11832,plain,
hd(iPr_def_13) = iPr_def_12,
inference(forward_subsumption_resolution,[status(thm)],[c_11831,c_10492]) ).
tcf(c_13363,plain,
! [X0: $i] :
( ( X0 = nil )
| ( tl(app(X0,sk3)) = app(tl(X0),sk3) )
| ~ ssList(X0) ),
inference(superposition,[status(thm)],[c_6705,c_377]) ).
tcf(c_13642,plain,
( ( nil = iPr_def_13 )
| ( tl(app(iPr_def_13,sk3)) = app(tl(iPr_def_13),sk3) ) ),
inference(superposition,[status(thm)],[c_9807,c_13363]) ).
tcf(c_13648,plain,
( ( nil = iPr_def_13 )
| ( app(tl(iPr_def_13),sk3) = sk3 ) ),
inference(light_normalisation,[status(thm)],[c_13642,c_10516,c_11366]) ).
tcf(c_13649,plain,
app(tl(iPr_def_13),sk3) = sk3,
inference(forward_subsumption_resolution,[status(thm)],[c_13648,c_10492]) ).
tcf(c_15369,plain,
! [X0: $i,X1: $i] :
( ( app(cons(X1,sk3),X0) = cons(X1,app(sk3,X0)) )
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(superposition,[status(thm)],[c_6705,c_401]) ).
tcf(c_16160,plain,
! [X0: $i] :
( ( X0 = nil )
| ~ ssList(nil)
| ~ ssList(sk3)
| ~ ssList(X0)
| ( app(X0,sk3) != sk3 ) ),
inference(superposition,[status(thm)],[c_9650,c_395]) ).
tcf(c_16207,plain,
! [X0: $i] :
( ( X0 = nil )
| ~ ssList(X0)
| ( app(X0,sk3) != sk3 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_16160,c_252,c_6705]) ).
tcf(c_17218,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_6695,c_405]) ).
tcf(c_17220,plain,
! [X0: $i] :
( memberP(nil,X0)
| ( X0 = iPr_def_12 )
| ~ ssItem(X0)
| ~ memberP(iPr_def_13,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_17218,c_9743,c_252]) ).
tcf(c_17489,plain,
! [X0: $i] :
( ( app(cons(X0,sk3),sk3) = cons(X0,app(sk3,sk3)) )
| ~ ssItem(X0) ),
inference(superposition,[status(thm)],[c_6705,c_15369]) ).
tcf(c_17744,plain,
app(cons(iPr_def_12,sk3),sk3) = cons(iPr_def_12,app(sk3,sk3)),
inference(superposition,[status(thm)],[c_9743,c_17489]) ).
tcf(c_20091,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_6697,c_417]) ).
tcf(c_20116,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_9781,c_417]) ).
tcf(c_20168,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_20116,c_9781]) ).
tcf(c_20169,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_20168,c_9717,c_252]) ).
tcf(c_20183,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_20091,c_6697]) ).
tcf(c_20184,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_20183,c_9717,c_9807]) ).
tcf(c_21240,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_6696,c_421]) ).
tcf(c_21260,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_21240,c_6694]) ).
tcf(c_21261,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_21260,c_6699,c_6705]) ).
tcf(c_21702,plain,
( singletonP(iPr_def_13)
| ~ ssItem(iPr_def_12) ),
inference(superposition,[status(thm)],[c_6695,c_10132]) ).
tcf(c_21704,plain,
singletonP(iPr_def_13),
inference(forward_subsumption_resolution,[status(thm)],[c_21702,c_9743]) ).
tcf(c_21708,plain,
( ( cons(skaf44(iPr_def_13),nil) = iPr_def_13 )
| ~ ssList(iPr_def_13) ),
inference(superposition,[status(thm)],[c_21704,c_345]) ).
tcf(c_21709,plain,
cons(skaf44(iPr_def_13),nil) = iPr_def_13,
inference(forward_subsumption_resolution,[status(thm)],[c_21708,c_9807]) ).
tcf(c_22798,plain,
( ( tl(iPr_def_13) = nil )
| ~ ssList(tl(iPr_def_13)) ),
inference(superposition,[status(thm)],[c_13649,c_16207]) ).
tcf(c_23138,plain,
( memberP(iPr_def_13,skaf44(iPr_def_13))
| ~ ssList(nil)
| ~ ssItem(skaf44(iPr_def_13)) ),
inference(superposition,[status(thm)],[c_21709,c_382]) ).
tcf(c_23172,plain,
memberP(iPr_def_13,skaf44(iPr_def_13)),
inference(forward_subsumption_resolution,[status(thm)],[c_23138,c_252,c_291]) ).
tcf(c_24550,plain,
( ( nil = iPr_def_13 )
| ( tl(iPr_def_13) = nil )
| ~ ssList(iPr_def_13) ),
inference(superposition,[status(thm)],[c_321,c_22798]) ).
tcf(c_24551,plain,
tl(iPr_def_13) = nil,
inference(forward_subsumption_resolution,[status(thm)],[c_24550,c_10492,c_9807]) ).
tcf(c_25064,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_24551,c_21261]) ).
tcf(c_25068,plain,
( ( nil = iPr_def_13 )
| ( sk3 = iPr_def_13 )
| ~ ssList(iPr_def_13)
| ( nil != iPr_def_14 ) ),
inference(ground_joinability,[status(thm)],[c_25064,c_11832]) ).
tcf(c_25069,plain,
( ( sk3 = iPr_def_13 )
| ( nil != iPr_def_14 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_25068,c_10492,c_9807]) ).
tcf(c_30044,plain,
( ssList(cons(iPr_def_12,sk3))
| ~ ssList(iPr_def_13)
| ~ ssList(sk3) ),
inference(superposition,[status(thm)],[c_11366,c_329]) ).
tcf(c_30048,plain,
! [X0: $i] :
( memberP(cons(iPr_def_12,sk3),X0)
| ~ ssList(iPr_def_13)
| ~ ssList(sk3)
| ~ ssItem(X0)
| ~ memberP(iPr_def_13,X0) ),
inference(superposition,[status(thm)],[c_11366,c_384]) ).
tcf(c_30055,plain,
ssList(cons(iPr_def_12,sk3)),
inference(forward_subsumption_resolution,[status(thm)],[c_30044,c_9807,c_6705]) ).
tcf(c_30064,plain,
! [X0: $i] :
( memberP(cons(iPr_def_12,sk3),X0)
| ~ ssItem(X0)
| ~ memberP(iPr_def_13,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_30048,c_9807,c_6705]) ).
tcf(c_30118,plain,
! [X0: $i] :
( ssList(app(sk3,X0))
| ~ ssList(sk3)
| ~ ssList(X0) ),
inference(instantiation,[status(thm)],[c_329]) ).
tcf(c_30199,plain,
app(nil,cons(iPr_def_12,sk3)) = cons(iPr_def_12,sk3),
inference(superposition,[status(thm)],[c_30055,c_318]) ).
tcf(c_30380,plain,
! [X0: $i] :
( memberP(sk3,X0)
| ( X0 = iPr_def_12 )
| ~ ssItem(iPr_def_12)
| ~ ssList(sk3)
| ~ ssItem(X0)
| ~ memberP(iPr_def_13,X0) ),
inference(superposition,[status(thm)],[c_30064,c_405]) ).
tcf(c_30381,plain,
! [X0: $i] :
( memberP(sk3,X0)
| ( X0 = iPr_def_12 )
| ~ ssItem(X0)
| ~ memberP(iPr_def_13,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_30380,c_9743,c_6705]) ).
tcf(c_30728,plain,
! [X0: $i] :
( ~ memberP(iPr_def_13,X0)
| ~ ssItem(X0)
| ( X0 = iPr_def_12 ) ),
inference(global_subsumption_just,[status(thm)],[c_30381,c_315,c_17220]) ).
tcf(c_30729,plain,
! [X0: $i] :
( ( X0 = iPr_def_12 )
| ~ ssItem(X0)
| ~ memberP(iPr_def_13,X0) ),
inference(renaming,[status(thm)],[c_30728]) ).
tcf(c_30738,plain,
( ( skaf44(iPr_def_13) = iPr_def_12 )
| ~ ssItem(skaf44(iPr_def_13)) ),
inference(superposition,[status(thm)],[c_23172,c_30729]) ).
tcf(c_30741,plain,
skaf44(iPr_def_13) = iPr_def_12,
inference(forward_subsumption_resolution,[status(thm)],[c_30738,c_291]) ).
tcf(c_30747,plain,
cons(iPr_def_12,nil) = iPr_def_13,
inference(demodulation,[status(thm)],[c_21709,c_30741]) ).
tcf(c_32639,plain,
! [X0: $i] :
( ~ ssItem(iPr_def_12)
| ~ ssList(nil)
| ~ ssList(sk3)
| ~ ssList(X0)
| ~ ssList(app(cons(iPr_def_12,sk3),cons(iPr_def_12,X0)))
| ~ duplicatefreeP(app(app(nil,cons(iPr_def_12,sk3)),cons(iPr_def_12,X0))) ),
inference(superposition,[status(thm)],[c_30199,c_423]) ).
tcf(c_32667,plain,
! [X0: $i] :
( ~ ssItem(iPr_def_12)
| ~ ssList(nil)
| ~ ssList(sk3)
| ~ ssList(X0)
| ~ duplicatefreeP(app(cons(iPr_def_12,sk3),cons(iPr_def_12,X0)))
| ~ ssList(app(cons(iPr_def_12,sk3),cons(iPr_def_12,X0))) ),
inference(light_normalisation,[status(thm)],[c_32639,c_30199]) ).
tcf(c_32668,plain,
! [X0: $i] :
( ~ ssList(X0)
| ~ duplicatefreeP(app(cons(iPr_def_12,sk3),cons(iPr_def_12,X0)))
| ~ ssList(app(cons(iPr_def_12,sk3),cons(iPr_def_12,X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_32667,c_9743,c_252,c_6705]) ).
tcf(c_32741,plain,
( ~ ssList(iPr_def_14)
| ~ ssList(app(cons(iPr_def_12,sk3),sk3))
| ~ duplicatefreeP(app(cons(iPr_def_12,sk3),cons(iPr_def_12,iPr_def_14))) ),
inference(superposition,[status(thm)],[c_10815,c_32668]) ).
tcf(c_32743,plain,
( ~ ssList(iPr_def_14)
| ~ duplicatefreeP(cons(iPr_def_12,app(sk3,sk3)))
| ~ ssList(cons(iPr_def_12,app(sk3,sk3))) ),
inference(light_normalisation,[status(thm)],[c_32741,c_10815,c_17744]) ).
tcf(c_32744,plain,
( ~ duplicatefreeP(cons(iPr_def_12,app(sk3,sk3)))
| ~ ssList(cons(iPr_def_12,app(sk3,sk3))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_32743,c_9717]) ).
tcf(c_99045,plain,
( ssList(cons(iPr_def_12,app(sk3,sk3)))
| ~ ssList(sk3)
| ~ ssList(cons(iPr_def_12,sk3)) ),
inference(superposition,[status(thm)],[c_17744,c_329]) ).
tcf(c_99082,plain,
ssList(cons(iPr_def_12,app(sk3,sk3))),
inference(forward_subsumption_resolution,[status(thm)],[c_99045,c_6705,c_30055]) ).
tcf(c_99382,plain,
( duplicatefreeP(cons(iPr_def_12,app(sk3,sk3)))
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_99082,c_6692]) ).
tcf(c_122610,plain,
! [X0: $i] : app(cons(X0,nil),iPr_def_14) = cons(X0,iPr_def_14),
inference(global_subsumption_just,[status(thm)],[c_11154,c_6691,c_6693,c_11154,c_32744,c_99082,c_99382]) ).
tcf(c_122612,plain,
app(iPr_def_13,iPr_def_14) = cons(iPr_def_12,iPr_def_14),
inference(superposition,[status(thm)],[c_30747,c_122610]) ).
tcf(c_122628,plain,
app(iPr_def_13,iPr_def_14) = sk3,
inference(light_normalisation,[status(thm)],[c_122612,c_10815]) ).
tcf(c_123088,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_122628,c_417]) ).
tcf(c_123117,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_123088,c_122628]) ).
tcf(c_123118,plain,
! [X0: $i] :
( segmentP(app(sk3,X0),iPr_def_14)
| ~ ssList(X0)
| ~ ssList(app(sk3,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_123117,c_9717,c_9807]) ).
tcf(c_125331,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_6697,c_20169]) ).
tcf(c_125339,plain,
( segmentP(iPr_def_15,iPr_def_14)
| ~ ssList(iPr_def_15)
| ~ ssList(iPr_def_13) ),
inference(light_normalisation,[status(thm)],[c_125331,c_6697]) ).
tcf(c_125340,plain,
segmentP(iPr_def_15,iPr_def_14),
inference(forward_subsumption_resolution,[status(thm)],[c_125339,c_9862,c_9807]) ).
tcf(c_125681,plain,
( segmentP(iPr_def_15,iPr_def_13)
| ~ ssList(nil)
| ~ ssList(app(iPr_def_15,nil)) ),
inference(superposition,[status(thm)],[c_9857,c_20184]) ).
tcf(c_125686,plain,
( segmentP(iPr_def_15,iPr_def_13)
| ~ ssList(iPr_def_15)
| ~ ssList(nil) ),
inference(light_normalisation,[status(thm)],[c_125681,c_9857]) ).
tcf(c_125687,plain,
segmentP(iPr_def_15,iPr_def_13),
inference(forward_subsumption_resolution,[status(thm)],[c_125686,c_9862,c_252]) ).
tcf(c_126893,plain,
! [X0: $i] :
( segmentP(app(sk3,X0),iPr_def_14)
| ~ ssList(X0) ),
inference(global_subsumption_just,[status(thm)],[c_123118,c_432,c_30118,c_123118]) ).
tcf(c_126900,plain,
( segmentP(sk3,iPr_def_14)
| ~ ssList(nil) ),
inference(superposition,[status(thm)],[c_9395,c_126893]) ).
tcf(c_126904,plain,
segmentP(sk3,iPr_def_14),
inference(forward_subsumption_resolution,[status(thm)],[c_126900,c_252]) ).
tcf(c_127100,plain,
( ( nil = iPr_def_14 )
| ~ ssList(iPr_def_14)
| ~ segmentP(iPr_def_15,iPr_def_14) ),
inference(superposition,[status(thm)],[c_126904,c_9860]) ).
tcf(c_127101,plain,
nil = iPr_def_14,
inference(forward_subsumption_resolution,[status(thm)],[c_127100,c_9717,c_125340]) ).
tcf(c_127108,plain,
sk3 = iPr_def_13,
inference(backward_subsumption_resolution,[status(thm)],[c_25069,c_127101]) ).
tcf(c_127973,plain,
~ segmentP(iPr_def_15,iPr_def_13),
inference(demodulation,[status(thm)],[c_9859,c_127108]) ).
tcf(c_127978,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_127973,c_125687]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC089-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.09/0.37 % Computer : n017.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Thu Sep 24 16:15:35 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.41 Running first-order theorem proving
% 0.09/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.09/0.43
% 0.09/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.43
% 0.09/0.43 % Detected problem language: tptp
% 0.09/0.44 % Proving...
% 65.13/9.92 % SZS status Started for theBenchmark.p
% 65.13/9.92 % SZS status Unsatisfiable for theBenchmark.p
% 65.13/9.92
% 65.13/9.92 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 65.13/9.92
% 65.13/9.92 % ------ iProver source info
% 65.13/9.92
% 65.13/9.92 % git: date: 2026-07-19 20:42:38 +0200
% 65.13/9.92 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 65.13/9.92 % git: non_committed_changes: false
% 65.13/9.92
% 65.13/9.92 % ------ Parsing...% successful
% 65.13/9.92
% 65.13/9.92
% 65.13/9.92 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 65.13/9.92
% 65.13/9.92 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe_e sup_sim: 0 sf_s rm: 2 0s sf_e pe_s pe_e %
% 65.13/9.92
% 65.13/9.92 % ------ Preprocessing... gs_s sp: 2 0s gs_e snvd_s sp: 0 0s snvd_e %
% 65.13/9.92
% 65.13/9.92 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 65.13/9.92 % ------ Proving...
% 65.13/9.92 % ------ Problem Properties
% 65.13/9.92
% 65.13/9.92 %
% 65.13/9.92 % clauses 189
% 65.13/9.92 % conjectures 2
% 65.13/9.92 % EPR 60
% 65.13/9.92 % Horn 161
% 65.13/9.92 % unary 66
% 65.13/9.92 % binary 23
% 65.13/9.92 % lits 561
% 65.13/9.92 % lits eq 77
% 65.13/9.92 % fd_pure 0
% 65.13/9.92 % fd_pseudo 0
% 65.13/9.92 % fd_cond 16
% 65.13/9.92 % fd_pseudo_cond 14
% 65.13/9.92 % AC symbols 0
% 65.13/9.92
% 65.13/9.92 % ------ Schedule dynamic 5 is on
% 65.13/9.92
% 65.13/9.92 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 65.13/9.92
% 65.13/9.92
% 65.13/9.92 % ------
% 65.13/9.92 % Current options:
% 65.13/9.92 % ------
% 65.13/9.92
% 65.13/9.92
% 65.13/9.92 %
% 65.13/9.92
% 65.13/9.92 % ------ Proving...
% 65.13/9.92 %
% 65.13/9.92
% 65.13/9.92 % SZS status Unsatisfiable for theBenchmark.p
% 65.13/9.92
% 65.13/9.92 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 65.13/9.92
% 65.13/9.92
%------------------------------------------------------------------------------