%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWC298-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/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:09:12 PM UTC 2026
% Result : Unsatisfiable 58.65s 18.85s
% Output : CNFRefutation 58.65s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f254ERROR: Could not build tree for root c_202697ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause8) ).
fof(f50,axiom,
! [X0,X1] : ssList(skaf46(X0,X1)),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause50) ).
fof(f71,axiom,
! [X0] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause71) ).
fof(f72,axiom,
! [X0,X1] :
( ssItem(X1)
| duplicatefreeP(X0)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause72) ).
fof(f73,axiom,
! [X0] :
( app(X0,nil) = X0
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause73) ).
fof(f85,axiom,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause85) ).
fof(f86,axiom,
! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause86) ).
fof(f98,axiom,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssItem(X0)
| cons(X0,X1) != nil ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause98) ).
fof(f99,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssItem(X0)
| nil != cons(X0,X1) ),
inference(reorient_equations,[],[f98]) ).
fof(f108,axiom,
! [X0,X1] :
( lt(X1,X0)
| ~ ssItem(X0)
| ~ ssItem(X1)
| ~ gt(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause105) ).
fof(f109,axiom,
! [X0,X1] :
( gt(X1,X0)
| ~ ssItem(X1)
| ~ ssItem(X0)
| ~ lt(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause106) ).
fof(f121,axiom,
! [X0,X1] :
( nil = X0
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != nil ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause118) ).
fof(f122,plain,
! [X0,X1] :
( nil = X0
| ~ ssList(X0)
| ~ ssList(X1)
| nil != app(X0,X1) ),
inference(reorient_equations,[],[f121]) ).
fof(f123,axiom,
! [X0,X1] :
( nil = X1
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != nil ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause119) ).
fof(f124,plain,
! [X0,X1] :
( nil = X1
| ~ ssList(X0)
| ~ ssList(X1)
| nil != app(X0,X1) ),
inference(reorient_equations,[],[f123]) ).
fof(f136,axiom,
! [X0,X1] :
( X1 = X0
| ~ ssList(X1)
| ~ ssList(X0)
| ~ rearsegP(X1,X0)
| ~ rearsegP(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause128) ).
fof(f137,plain,
! [X0,X1] :
( X0 = X1
| ~ ssList(X1)
| ~ ssList(X0)
| ~ rearsegP(X1,X0)
| ~ rearsegP(X0,X1) ),
inference(reorient_equations,[],[f136]) ).
fof(f142,axiom,
! [X0,X1] :
( app(skaf46(X0,X1),X1) = X0
| ~ ssList(X0)
| ~ ssList(X1)
| ~ rearsegP(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause131) ).
fof(f151,axiom,
! [X2,X0,X1] :
( memberP(app(X0,X2),X1)
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ memberP(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause140) ).
fof(f152,axiom,
! [X2,X0,X1] :
( memberP(app(X2,X0),X1)
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ memberP(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause141) ).
fof(f154,axiom,
! [X2,X0,X1] :
( rearsegP(X2,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| app(X0,X1) != X2 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause143) ).
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/sandbox/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(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/sandbox/benchmark/Axioms/SWC001-0.ax',clause179) ).
fof(f202,negated_conjecture,
ssList(sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_3) ).
fof(f203,negated_conjecture,
ssList(sk4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_4) ).
fof(f205,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_6) ).
fof(f206,negated_conjecture,
ssItem(sk5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_7) ).
fof(f207,negated_conjecture,
ssItem(sk6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_8) ).
fof(f208,negated_conjecture,
ssList(sk7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_9) ).
fof(f209,negated_conjecture,
ssList(sk8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_10) ).
fof(f210,negated_conjecture,
ssList(sk9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_11) ).
fof(f211,negated_conjecture,
app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9) = sk1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_12) ).
fof(f212,plain,
sk1 = app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9),
inference(reorient_equations,[],[f211]) ).
fof(f213,negated_conjecture,
lt(sk6,sk5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_13) ).
fof(f216,negated_conjecture,
( nil = sk4
| cons(sk10,nil) = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_16) ).
fof(f217,plain,
( nil = sk4
| sk3 = cons(sk10,nil) ),
inference(reorient_equations,[],[f216]) ).
fof(f220,negated_conjecture,
( nil = sk3
| cons(sk10,nil) = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_19) ).
fof(f221,plain,
( nil = sk3
| sk3 = cons(sk10,nil) ),
inference(reorient_equations,[],[f220]) ).
fof(f222,negated_conjecture,
( nil = sk3
| memberP(sk4,sk10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_20) ).
fof(f226,plain,
sk3 = app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9),
inference(definition_unfolding,[],[f212,f205]) ).
fof(f237,plain,
! [X0,X1] :
( rearsegP(app(X0,X1),X1)
| ~ ssList(app(X0,X1))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(equality_resolution,[],[f154]) ).
fof(f244,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_262,plain,
ssList(nil),
inference(cnf_transformation,[],[f8]) ).
tcf(c_304,plain,
! [X0: $i,X1: $i] : ssList(skaf46(X0,X1)),
inference(cnf_transformation,[],[f50]) ).
tcf(c_325,plain,
! [X0: $i] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_326,plain,
! [X0: $i,X1: $i] :
( duplicatefreeP(X0)
| ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_327,plain,
! [X0: $i] :
( ( app(X0,nil) = X0 )
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f73]) ).
tcf(c_339,plain,
! [X0: $i,X1: $i] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_340,plain,
! [X0: $i,X1: $i] :
( ssList(cons(X1,X0))
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_352,plain,
! [X0: $i,X1: $i] :
( ~ ssItem(X0)
| ~ ssList(X1)
| ( cons(X0,X1) != nil ) ),
inference(cnf_transformation,[],[f99]) ).
tcf(c_359,plain,
! [X0: $i,X1: $i] :
( lt(X1,X0)
| ~ ssItem(X1)
| ~ ssItem(X0)
| ~ gt(X0,X1) ),
inference(cnf_transformation,[],[f108]) ).
tcf(c_360,plain,
! [X0: $i,X1: $i] :
( gt(X1,X0)
| ~ ssItem(X1)
| ~ ssItem(X0)
| ~ lt(X0,X1) ),
inference(cnf_transformation,[],[f109]) ).
tcf(c_365,plain,
! [X0: $i] :
( ~ ssItem(X0)
| ~ lt(X0,X0) ),
inference(cnf_transformation,[],[f251]) ).
tcf(c_372,plain,
! [X0: $i,X1: $i] :
( ( X0 = nil )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(X0,X1) != nil ) ),
inference(cnf_transformation,[],[f122]) ).
tcf(c_373,plain,
! [X0: $i,X1: $i] :
( ( X1 = nil )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(X0,X1) != nil ) ),
inference(cnf_transformation,[],[f124]) ).
tcf(c_382,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ ssList(X1)
| ~ ssList(X0)
| ~ rearsegP(X1,X0)
| ~ rearsegP(X0,X1) ),
inference(cnf_transformation,[],[f137]) ).
tcf(c_385,plain,
! [X0: $i,X1: $i] :
( ( app(skaf46(X0,X1),X1) = X0 )
| ~ ssList(X1)
| ~ ssList(X0)
| ~ rearsegP(X0,X1) ),
inference(cnf_transformation,[],[f142]) ).
tcf(c_392,plain,
! [X0: $i,X1: $i] :
( memberP(cons(X1,X0),X1)
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f254]) ).
tcf(c_394,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] :
( memberP(app(X2,X0),X1)
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ memberP(X0,X1) ),
inference(cnf_transformation,[],[f152]) ).
tcf(c_397,plain,
! [X0: $i,X1: $i] :
( rearsegP(app(X0,X1),X1)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(app(X0,X1)) ),
inference(cnf_transformation,[],[f237]) ).
tcf(c_415,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_433,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,[],[f244]) ).
tcf(c_442,negated_conjecture,
ssList(sk3),
inference(cnf_transformation,[],[f202]) ).
tcf(c_443,negated_conjecture,
ssList(sk4),
inference(cnf_transformation,[],[f203]) ).
tcf(c_444,negated_conjecture,
ssItem(sk5),
inference(cnf_transformation,[],[f206]) ).
tcf(c_445,negated_conjecture,
ssItem(sk6),
inference(cnf_transformation,[],[f207]) ).
tcf(c_446,negated_conjecture,
ssList(sk7),
inference(cnf_transformation,[],[f208]) ).
tcf(c_447,negated_conjecture,
ssList(sk8),
inference(cnf_transformation,[],[f209]) ).
tcf(c_448,negated_conjecture,
ssList(sk9),
inference(cnf_transformation,[],[f210]) ).
tcf(c_449,negated_conjecture,
app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9) = sk3,
inference(cnf_transformation,[],[f226]) ).
tcf(c_450,negated_conjecture,
lt(sk6,sk5),
inference(cnf_transformation,[],[f213]) ).
tcf(c_453,negated_conjecture,
( ( sk4 = nil )
| ( cons(sk10,nil) = sk3 ) ),
inference(cnf_transformation,[],[f217]) ).
tcf(c_456,negated_conjecture,
( ( sk3 = nil )
| ( cons(sk10,nil) = sk3 ) ),
inference(cnf_transformation,[],[f221]) ).
tcf(c_457,negated_conjecture,
( memberP(sk4,sk10)
| ( sk3 = nil ) ),
inference(cnf_transformation,[],[f222]) ).
tcf(c_847,plain,
! [X0: $i,X1: $i] :
( rearsegP(app(X0,X1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_397,c_339]) ).
tcf(c_6637,plain,
! [X0: $i] :
( ~ iPr_def_10
| ssItem(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_326]) ).
tcf(c_6638,plain,
! [X0: $i] :
( ~ iPr_def_11
| ~ ssList(X0)
| duplicatefreeP(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_326]) ).
tcf(c_6639,plain,
( iPr_def_11
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_326]) ).
tcf(c_6640,definition,
iPr_def_12 = cons(sk5,nil),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_6641,definition,
iPr_def_13 = app(sk7,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_6642,definition,
iPr_def_14 = app(iPr_def_13,sk8),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_6643,definition,
iPr_def_15 = cons(sk6,nil),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_6644,definition,
iPr_def_16 = app(iPr_def_14,iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_6645,definition,
iPr_def_17 = app(iPr_def_16,sk9),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_6646,definition,
iPr_def_18 = cons(sk10,nil),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_6647,negated_conjecture,
iPr_def_17 = sk3,
inference(demodulation,[status(thm)],[c_449,c_6643,c_6640,c_6641,c_6642,c_6644,c_6645]) ).
tcf(c_6649,negated_conjecture,
( memberP(sk4,sk10)
| ( sk3 = nil ) ),
inference(demodulation,[status(thm)],[c_457]) ).
tcf(c_6650,negated_conjecture,
( ( iPr_def_18 = sk3 )
| ( sk3 = nil ) ),
inference(demodulation,[status(thm)],[c_456,c_6646]) ).
tcf(c_6653,negated_conjecture,
( ( iPr_def_18 = sk3 )
| ( sk4 = nil ) ),
inference(demodulation,[status(thm)],[c_453]) ).
tcf(c_6656,negated_conjecture,
lt(sk6,sk5),
inference(demodulation,[status(thm)],[c_450]) ).
tcf(c_6657,negated_conjecture,
ssList(sk9),
inference(demodulation,[status(thm)],[c_448]) ).
tcf(c_6658,negated_conjecture,
ssList(sk8),
inference(demodulation,[status(thm)],[c_447]) ).
tcf(c_6659,negated_conjecture,
ssList(sk7),
inference(demodulation,[status(thm)],[c_446]) ).
tcf(c_6660,negated_conjecture,
ssItem(sk6),
inference(demodulation,[status(thm)],[c_445]) ).
tcf(c_6661,negated_conjecture,
ssItem(sk5),
inference(demodulation,[status(thm)],[c_444]) ).
tcf(c_6662,negated_conjecture,
ssList(sk4),
inference(demodulation,[status(thm)],[c_443]) ).
tcf(c_6663,negated_conjecture,
ssList(sk3),
inference(demodulation,[status(thm)],[c_442]) ).
tcf(c_9284,plain,
ssList(iPr_def_17),
inference(light_normalisation,[status(thm)],[c_6663,c_6647]) ).
tcf(c_9292,plain,
( memberP(sk4,sk10)
| ( nil = iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_6649,c_6647]) ).
tcf(c_9303,plain,
( ( iPr_def_17 = iPr_def_18 )
| ( nil = iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_6650,c_6647]) ).
tcf(c_9335,plain,
( ( iPr_def_17 = iPr_def_18 )
| ( sk4 = nil ) ),
inference(light_normalisation,[status(thm)],[c_6653,c_6647]) ).
tcf(c_9538,plain,
app(sk4,nil) = sk4,
inference(superposition,[status(thm)],[c_6662,c_327]) ).
tcf(c_9570,plain,
app(iPr_def_17,nil) = iPr_def_17,
inference(superposition,[status(thm)],[c_9284,c_327]) ).
tcf(c_9663,plain,
( ( iPr_def_17 = iPr_def_18 )
| ( app(sk4,iPr_def_17) = sk4 ) ),
inference(superposition,[status(thm)],[c_9303,c_9538]) ).
tcf(c_9925,plain,
( ssList(iPr_def_13)
| ~ ssList(iPr_def_12)
| ~ ssList(sk7) ),
inference(superposition,[status(thm)],[c_6641,c_339]) ).
tcf(c_9926,plain,
( ssList(iPr_def_14)
| ~ ssList(iPr_def_13)
| ~ ssList(sk8) ),
inference(superposition,[status(thm)],[c_6642,c_339]) ).
tcf(c_9927,plain,
( ssList(iPr_def_16)
| ~ ssList(iPr_def_15)
| ~ ssList(iPr_def_14) ),
inference(superposition,[status(thm)],[c_6644,c_339]) ).
tcf(c_9952,plain,
( ssList(iPr_def_14)
| ~ ssList(iPr_def_13) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9926,c_6658]) ).
tcf(c_9955,plain,
( ssList(iPr_def_13)
| ~ ssList(iPr_def_12) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9925,c_6659]) ).
tcf(c_9972,plain,
( ssList(iPr_def_12)
| ~ ssItem(sk5)
| ~ ssList(nil) ),
inference(superposition,[status(thm)],[c_6640,c_340]) ).
tcf(c_9973,plain,
( ssList(iPr_def_15)
| ~ ssItem(sk6)
| ~ ssList(nil) ),
inference(superposition,[status(thm)],[c_6643,c_340]) ).
tcf(c_9983,plain,
ssList(iPr_def_15),
inference(forward_subsumption_resolution,[status(thm)],[c_9973,c_6660,c_262]) ).
tcf(c_9984,plain,
ssList(iPr_def_12),
inference(forward_subsumption_resolution,[status(thm)],[c_9972,c_6661,c_262]) ).
tcf(c_10029,plain,
ssList(iPr_def_14),
inference(global_subsumption_just,[status(thm)],[c_9952,c_9955,c_9952,c_9984]) ).
tcf(c_10033,plain,
ssList(iPr_def_13),
inference(global_subsumption_just,[status(thm)],[c_9955,c_9955,c_9984]) ).
tcf(c_10440,plain,
( rearsegP(iPr_def_17,sk9)
| ~ ssList(iPr_def_16)
| ~ ssList(sk9) ),
inference(superposition,[status(thm)],[c_6645,c_847]) ).
tcf(c_10452,plain,
( rearsegP(iPr_def_17,nil)
| ~ ssList(iPr_def_17)
| ~ ssList(nil) ),
inference(superposition,[status(thm)],[c_9570,c_847]) ).
tcf(c_10453,plain,
( rearsegP(sk4,iPr_def_17)
| ( iPr_def_17 = iPr_def_18 )
| ~ ssList(iPr_def_17)
| ~ ssList(sk4) ),
inference(superposition,[status(thm)],[c_9663,c_847]) ).
tcf(c_10485,plain,
rearsegP(iPr_def_17,nil),
inference(forward_subsumption_resolution,[status(thm)],[c_10452,c_9284,c_262]) ).
tcf(c_10490,plain,
( rearsegP(iPr_def_17,sk9)
| ~ ssList(iPr_def_16) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10440,c_6657]) ).
tcf(c_10511,plain,
( rearsegP(sk4,iPr_def_17)
| ( iPr_def_17 = iPr_def_18 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10453,c_9284,c_6662]) ).
tcf(c_10938,plain,
( ~ ssItem(sk5)
| ~ ssList(nil)
| ( nil != iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_6640,c_352]) ).
tcf(c_10948,plain,
nil != iPr_def_12,
inference(forward_subsumption_resolution,[status(thm)],[c_10938,c_6661,c_262]) ).
tcf(c_11062,plain,
rearsegP(iPr_def_17,sk9),
inference(global_subsumption_just,[status(thm)],[c_10490,c_9955,c_9952,c_9927,c_9984,c_9983,c_10490]) ).
tcf(c_11554,plain,
( rearsegP(nil,iPr_def_17)
| ( iPr_def_17 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_9335,c_10511]) ).
tcf(c_11846,plain,
( ( nil = iPr_def_13 )
| ~ ssList(iPr_def_13)
| ~ ssList(sk8)
| ( nil != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_6642,c_372]) ).
tcf(c_11847,plain,
( ( nil = iPr_def_14 )
| ~ ssList(iPr_def_15)
| ~ ssList(iPr_def_14)
| ( nil != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_6644,c_372]) ).
tcf(c_11848,plain,
( ( nil = iPr_def_16 )
| ~ ssList(iPr_def_16)
| ~ ssList(sk9)
| ( nil != iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_6645,c_372]) ).
tcf(c_11885,plain,
( ( nil = iPr_def_16 )
| ~ ssList(iPr_def_16)
| ( nil != iPr_def_17 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11848,c_6657]) ).
tcf(c_11889,plain,
( ( nil = iPr_def_14 )
| ( nil != iPr_def_16 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11847,c_9983,c_10029]) ).
tcf(c_11892,plain,
( ( nil = iPr_def_13 )
| ( nil != iPr_def_14 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11846,c_10033,c_6658]) ).
tcf(c_11907,plain,
( ( nil = iPr_def_12 )
| ~ ssList(iPr_def_12)
| ~ ssList(sk7)
| ( nil != iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_6641,c_373]) ).
tcf(c_11955,plain,
nil != iPr_def_13,
inference(forward_subsumption_resolution,[status(thm)],[c_11907,c_10948,c_9984,c_6659]) ).
tcf(c_12651,plain,
( ( nil = iPr_def_17 )
| ~ ssList(iPr_def_17)
| ~ ssList(nil)
| ~ rearsegP(nil,iPr_def_17) ),
inference(superposition,[status(thm)],[c_10485,c_382]) ).
tcf(c_12709,plain,
( ( nil = iPr_def_17 )
| ~ rearsegP(nil,iPr_def_17) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12651,c_9284,c_262]) ).
tcf(c_13329,plain,
( ( app(skaf46(iPr_def_17,sk9),sk9) = iPr_def_17 )
| ~ ssList(iPr_def_17)
| ~ ssList(sk9) ),
inference(superposition,[status(thm)],[c_11062,c_385]) ).
tcf(c_13374,plain,
app(skaf46(iPr_def_17,sk9),sk9) = iPr_def_17,
inference(forward_subsumption_resolution,[status(thm)],[c_13329,c_9284,c_6657]) ).
tcf(c_13693,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ssItem(sk5)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ duplicatefreeP(app(app(X0,cons(sk5,X1)),cons(sk5,X2)))
| ~ ssList(app(app(X0,cons(sk5,X1)),cons(sk5,X2))) ),
inference(instantiation,[status(thm)],[c_433]) ).
tcf(c_13694,plain,
( ~ ssItem(sk5)
| ~ ssList(nil)
| ~ duplicatefreeP(app(app(nil,cons(sk5,nil)),cons(sk5,nil)))
| ~ ssList(app(app(nil,cons(sk5,nil)),cons(sk5,nil))) ),
inference(instantiation,[status(thm)],[c_13693]) ).
tcf(c_14006,plain,
! [X0: $i] :
( memberP(iPr_def_17,X0)
| ~ ssList(iPr_def_16)
| ~ ssList(sk9)
| ~ ssItem(X0)
| ~ memberP(iPr_def_16,X0) ),
inference(superposition,[status(thm)],[c_6645,c_394]) ).
tcf(c_14041,plain,
! [X0: $i] :
( memberP(iPr_def_17,X0)
| ~ ssList(iPr_def_16)
| ~ ssItem(X0)
| ~ memberP(iPr_def_16,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14006,c_6657]) ).
tcf(c_14867,plain,
( ( sk9 = nil )
| ~ ssList(sk9)
| ~ ssList(skaf46(iPr_def_17,sk9))
| ( nil != iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_13374,c_373]) ).
tcf(c_14876,plain,
( ( sk9 = nil )
| ( nil != iPr_def_17 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14867,c_6657,c_304]) ).
tcf(c_15716,plain,
nil != iPr_def_17,
inference(global_subsumption_just,[status(thm)],[c_14876,c_9955,c_9952,c_9927,c_9984,c_9983,c_11892,c_11889,c_11885,c_11955]) ).
tcf(c_15719,plain,
memberP(sk4,sk10),
inference(backward_subsumption_resolution,[status(thm)],[c_9292,c_15716]) ).
tcf(c_17084,plain,
! [X0: $i,X1: $i] :
( duplicatefreeP(skaf46(X0,X1))
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_304,c_6638]) ).
tcf(c_20620,plain,
! [X0: $i,X1: $i] :
( ssList(app(X1,cons(sk5,X0)))
| ~ ssList(X1)
| ~ ssList(cons(sk5,X0)) ),
inference(instantiation,[status(thm)],[c_339]) ).
tcf(c_20621,plain,
( ssList(app(nil,cons(sk5,nil)))
| ~ ssList(nil)
| ~ ssList(cons(sk5,nil)) ),
inference(instantiation,[status(thm)],[c_20620]) ).
tcf(c_33418,plain,
! [X0: $i] :
( ssList(cons(sk5,X0))
| ~ ssItem(sk5)
| ~ ssList(X0) ),
inference(instantiation,[status(thm)],[c_340]) ).
tcf(c_33419,plain,
( ssList(cons(sk5,nil))
| ~ ssItem(sk5)
| ~ ssList(nil) ),
inference(instantiation,[status(thm)],[c_33418]) ).
tcf(c_39064,plain,
! [X0: $i,X1: $i,X2: $i] :
( ssList(app(app(X0,cons(sk5,X1)),cons(sk5,X2)))
| ~ ssList(cons(sk5,X2))
| ~ ssList(app(X0,cons(sk5,X1))) ),
inference(instantiation,[status(thm)],[c_20620]) ).
tcf(c_39065,plain,
( ssList(app(app(nil,cons(sk5,nil)),cons(sk5,nil)))
| ~ ssList(cons(sk5,nil))
| ~ ssList(app(nil,cons(sk5,nil))) ),
inference(instantiation,[status(thm)],[c_39064]) ).
tcf(c_41954,plain,
! [X0: $i] :
( memberP(iPr_def_17,X0)
| ~ ssList(iPr_def_16)
| ~ ssList(sk9)
| ~ ssItem(X0)
| ~ memberP(iPr_def_16,X0) ),
inference(superposition,[status(thm)],[c_6645,c_394]) ).
tcf(c_41986,plain,
! [X0: $i] :
( memberP(iPr_def_17,X0)
| ~ ssList(iPr_def_16)
| ~ ssItem(X0)
| ~ memberP(iPr_def_16,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_41954,c_6657]) ).
tcf(c_74107,plain,
! [X0: $i,X1: $i,X2: $i] :
( duplicatefreeP(app(app(X0,cons(sk5,X1)),cons(sk5,X2)))
| ~ iPr_def_11
| ~ ssList(app(app(X0,cons(sk5,X1)),cons(sk5,X2))) ),
inference(instantiation,[status(thm)],[c_6638]) ).
tcf(c_74108,plain,
( duplicatefreeP(app(app(nil,cons(sk5,nil)),cons(sk5,nil)))
| ~ iPr_def_11
| ~ ssList(app(app(nil,cons(sk5,nil)),cons(sk5,nil))) ),
inference(instantiation,[status(thm)],[c_74107]) ).
tcf(c_85781,plain,
~ iPr_def_11,
inference(global_subsumption_just,[status(thm)],[c_17084,c_444,c_262,c_13694,c_20621,c_33419,c_39065,c_74108]) ).
tcf(c_85783,plain,
iPr_def_10,
inference(backward_subsumption_resolution,[status(thm)],[c_6639,c_85781]) ).
tcf(c_85784,plain,
! [X0: $i] : ssItem(X0),
inference(backward_subsumption_resolution,[status(thm)],[c_6637,c_85783]) ).
tcf(c_85811,plain,
! [X0: $i,X1: $i] :
( memberP(cons(X1,X0),X1)
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_392,c_85784]) ).
tcf(c_85812,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(X1,X2)
| ( X0 = X2 )
| ~ ssList(X1)
| ~ memberP(cons(X0,X1),X2) ),
inference(backward_subsumption_resolution,[status(thm)],[c_415,c_85784]) ).
tcf(c_85822,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(app(X2,X0),X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ memberP(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_395,c_85784]) ).
tcf(c_85823,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(app(X0,X2),X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ memberP(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_394,c_85784]) ).
tcf(c_85837,plain,
! [X0: $i,X1: $i] :
( gt(X1,X0)
| ~ lt(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_360,c_85784]) ).
tcf(c_85838,plain,
! [X0: $i,X1: $i] :
( lt(X1,X0)
| ~ gt(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_359,c_85784]) ).
tcf(c_85844,plain,
! [X0: $i,X1: $i] :
( ssList(cons(X1,X0))
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_340,c_85784]) ).
tcf(c_91162,plain,
! [X0: $i] :
( memberP(iPr_def_17,X0)
| ~ memberP(iPr_def_16,X0) ),
inference(global_subsumption_just,[status(thm)],[c_41986,c_444,c_262,c_6637,c_6639,c_9955,c_9952,c_9927,c_9984,c_9983,c_13694,c_14041,c_20621,c_33419,c_39065,c_74108]) ).
tcf(c_98831,plain,
! [X0: $i] : ~ memberP(nil,X0),
inference(global_subsumption_just,[status(thm)],[c_325,c_444,c_262,c_325,c_6637,c_6639,c_13694,c_20621,c_33419,c_39065,c_74108]) ).
tcf(c_167128,negated_conjecture,
memberP(sk4,sk10),
inference(global_subsumption_just,[status(thm)],[c_6649,c_15719]) ).
tcf(c_167160,plain,
( ( iPr_def_17 = iPr_def_18 )
| ( sk4 = nil ) ),
inference(light_normalisation,[status(thm)],[c_6653,c_6647]) ).
tcf(c_167167,plain,
( memberP(nil,sk10)
| ( iPr_def_17 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_167160,c_167128]) ).
tcf(c_167191,plain,
iPr_def_17 = iPr_def_18,
inference(global_subsumption_just,[status(thm)],[c_167167,c_9955,c_9952,c_9927,c_9984,c_9983,c_11554,c_11892,c_11889,c_11885,c_11955,c_12709]) ).
tcf(c_167229,plain,
cons(sk10,nil) = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_6646,c_167191]) ).
tcf(c_167302,plain,
! [X0: $i] : ~ lt(X0,X0),
inference(global_subsumption_just,[status(thm)],[c_365,c_444,c_262,c_365,c_6637,c_6639,c_13694,c_20621,c_33419,c_39065,c_74108]) ).
tcf(c_167362,plain,
( ssList(iPr_def_13)
| ~ ssList(iPr_def_12)
| ~ ssList(sk7) ),
inference(superposition,[status(thm)],[c_6641,c_339]) ).
tcf(c_167363,plain,
( ssList(iPr_def_14)
| ~ ssList(iPr_def_13)
| ~ ssList(sk8) ),
inference(superposition,[status(thm)],[c_6642,c_339]) ).
tcf(c_167383,plain,
( ssList(iPr_def_14)
| ~ ssList(iPr_def_13) ),
inference(forward_subsumption_resolution,[status(thm)],[c_167363,c_6658]) ).
tcf(c_167386,plain,
( ssList(iPr_def_13)
| ~ ssList(iPr_def_12) ),
inference(forward_subsumption_resolution,[status(thm)],[c_167362,c_6659]) ).
tcf(c_167395,plain,
! [X0: $i,X1: $i] :
( ssList(cons(X1,X0))
| ~ ssList(X0) ),
inference(global_subsumption_just,[status(thm)],[c_340,c_85844]) ).
tcf(c_167401,plain,
( ssList(iPr_def_12)
| ~ ssList(nil) ),
inference(superposition,[status(thm)],[c_6640,c_167395]) ).
tcf(c_167402,plain,
( ssList(iPr_def_15)
| ~ ssList(nil) ),
inference(superposition,[status(thm)],[c_6643,c_167395]) ).
tcf(c_167406,plain,
ssList(iPr_def_15),
inference(forward_subsumption_resolution,[status(thm)],[c_167402,c_262]) ).
tcf(c_167407,plain,
ssList(iPr_def_12),
inference(forward_subsumption_resolution,[status(thm)],[c_167401,c_262]) ).
tcf(c_167420,plain,
ssList(iPr_def_14),
inference(global_subsumption_just,[status(thm)],[c_167383,c_9955,c_9952,c_9984]) ).
tcf(c_167424,plain,
ssList(iPr_def_13),
inference(global_subsumption_just,[status(thm)],[c_167386,c_9955,c_9984]) ).
tcf(c_167532,plain,
! [X0: $i,X1: $i] :
( memberP(cons(X1,X0),X1)
| ~ ssList(X0) ),
inference(global_subsumption_just,[status(thm)],[c_392,c_85811]) ).
tcf(c_167538,plain,
( memberP(iPr_def_12,sk5)
| ~ ssList(nil) ),
inference(superposition,[status(thm)],[c_6640,c_167532]) ).
tcf(c_167539,plain,
( memberP(iPr_def_15,sk6)
| ~ ssList(nil) ),
inference(superposition,[status(thm)],[c_6643,c_167532]) ).
tcf(c_167542,plain,
memberP(iPr_def_15,sk6),
inference(forward_subsumption_resolution,[status(thm)],[c_167539,c_262]) ).
tcf(c_167543,plain,
memberP(iPr_def_12,sk5),
inference(forward_subsumption_resolution,[status(thm)],[c_167538,c_262]) ).
tcf(c_168007,plain,
! [X0: $i,X1: $i] :
( lt(X1,X0)
| ~ gt(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_359,c_85838]) ).
tcf(c_168016,plain,
! [X0: $i,X1: $i] :
( gt(X1,X0)
| ~ lt(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_360,c_85837]) ).
tcf(c_168022,plain,
gt(sk5,sk6),
inference(superposition,[status(thm)],[c_6656,c_168016]) ).
tcf(c_170780,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(app(X0,X2),X1)
| ~ memberP(X0,X1)
| ~ ssList(X0)
| ~ ssList(X2) ),
inference(global_subsumption_just,[status(thm)],[c_394,c_85823]) ).
tcf(c_170781,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(app(X0,X2),X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ memberP(X0,X1) ),
inference(renaming,[status(thm)],[c_170780]) ).
tcf(c_170792,plain,
! [X0: $i] :
( memberP(iPr_def_14,X0)
| ~ ssList(iPr_def_13)
| ~ ssList(sk8)
| ~ memberP(iPr_def_13,X0) ),
inference(superposition,[status(thm)],[c_6642,c_170781]) ).
tcf(c_170793,plain,
! [X0: $i] :
( memberP(iPr_def_16,X0)
| ~ ssList(iPr_def_15)
| ~ ssList(iPr_def_14)
| ~ memberP(iPr_def_14,X0) ),
inference(superposition,[status(thm)],[c_6644,c_170781]) ).
tcf(c_170794,plain,
! [X0: $i] :
( memberP(iPr_def_17,X0)
| ~ ssList(iPr_def_16)
| ~ ssList(sk9)
| ~ memberP(iPr_def_16,X0) ),
inference(superposition,[status(thm)],[c_6645,c_170781]) ).
tcf(c_170854,plain,
! [X0: $i] :
( memberP(iPr_def_17,X0)
| ~ ssList(iPr_def_16)
| ~ memberP(iPr_def_16,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_170794,c_6657]) ).
tcf(c_170858,plain,
! [X0: $i] :
( memberP(iPr_def_16,X0)
| ~ memberP(iPr_def_14,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_170793,c_167406,c_167420]) ).
tcf(c_170861,plain,
! [X0: $i] :
( memberP(iPr_def_14,X0)
| ~ memberP(iPr_def_13,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_170792,c_167424,c_6658]) ).
tcf(c_170983,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(app(X2,X0),X1)
| ~ memberP(X0,X1)
| ~ ssList(X0)
| ~ ssList(X2) ),
inference(global_subsumption_just,[status(thm)],[c_395,c_85822]) ).
tcf(c_170984,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(app(X2,X0),X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ memberP(X0,X1) ),
inference(renaming,[status(thm)],[c_170983]) ).
tcf(c_170994,plain,
! [X0: $i] :
( memberP(iPr_def_13,X0)
| ~ ssList(iPr_def_12)
| ~ ssList(sk7)
| ~ memberP(iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_6641,c_170984]) ).
tcf(c_170996,plain,
! [X0: $i] :
( memberP(iPr_def_16,X0)
| ~ ssList(iPr_def_15)
| ~ ssList(iPr_def_14)
| ~ memberP(iPr_def_15,X0) ),
inference(superposition,[status(thm)],[c_6644,c_170984]) ).
tcf(c_171061,plain,
! [X0: $i] :
( memberP(iPr_def_16,X0)
| ~ memberP(iPr_def_15,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_170996,c_167406,c_167420]) ).
tcf(c_171067,plain,
! [X0: $i] :
( memberP(iPr_def_13,X0)
| ~ memberP(iPr_def_12,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_170994,c_167407,c_6659]) ).
tcf(c_171160,plain,
memberP(iPr_def_13,sk5),
inference(superposition,[status(thm)],[c_167543,c_171067]) ).
tcf(c_171759,plain,
memberP(iPr_def_14,sk5),
inference(superposition,[status(thm)],[c_171160,c_170861]) ).
tcf(c_175542,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(X1,X2)
| ( X0 = X2 )
| ~ ssList(X1)
| ~ memberP(cons(X0,X1),X2) ),
inference(global_subsumption_just,[status(thm)],[c_415,c_85812]) ).
tcf(c_175556,plain,
! [X0: $i] :
( memberP(nil,X0)
| ( X0 = sk10 )
| ~ ssList(nil)
| ~ memberP(iPr_def_17,X0) ),
inference(superposition,[status(thm)],[c_167229,c_175542]) ).
tcf(c_175561,plain,
! [X0: $i] :
( ( X0 = sk10 )
| ~ memberP(iPr_def_17,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_175556,c_98831,c_262]) ).
tcf(c_178013,plain,
! [X0: $i] :
( memberP(iPr_def_17,X0)
| ~ memberP(iPr_def_16,X0) ),
inference(global_subsumption_just,[status(thm)],[c_170854,c_91162]) ).
tcf(c_190631,plain,
memberP(iPr_def_16,sk5),
inference(superposition,[status(thm)],[c_171759,c_170858]) ).
tcf(c_190636,plain,
memberP(iPr_def_16,sk6),
inference(superposition,[status(thm)],[c_167542,c_171061]) ).
tcf(c_190699,plain,
memberP(iPr_def_17,sk5),
inference(superposition,[status(thm)],[c_190631,c_178013]) ).
tcf(c_191033,plain,
memberP(iPr_def_17,sk6),
inference(superposition,[status(thm)],[c_190636,c_178013]) ).
tcf(c_202270,plain,
sk6 = sk10,
inference(superposition,[status(thm)],[c_191033,c_175561]) ).
tcf(c_202271,plain,
sk5 = sk10,
inference(superposition,[status(thm)],[c_190699,c_175561]) ).
tcf(c_202343,plain,
gt(sk5,sk10),
inference(demodulation,[status(thm)],[c_168022,c_202270]) ).
tcf(c_202693,plain,
gt(sk10,sk10),
inference(light_normalisation,[status(thm)],[c_202343,c_202271]) ).
tcf(c_202696,plain,
lt(sk10,sk10),
inference(superposition,[status(thm)],[c_202693,c_168007]) ).
tcf(c_202697,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_202696,c_167302]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC298-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/5.39 % Computer : n017.cluster.edu
% 0.11/5.39 % Model : x86_64 x86_64
% 0.11/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.39 % Memory : 8046.5625MB
% 0.11/5.39 % OS : Linux 6.8.0-71-generic
% 0.11/5.39 % CPULimit : 300
% 0.11/5.39 % WCLimit : 300
% 0.11/5.39 % DateTime : Thu Sep 24 17:24:54 UTC 2026
% 0.11/5.39 % CPUTime :
% 0.11/5.39 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.15/5.43 Running first-order theorem proving
% 0.15/5.43 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/5.44
% 0.15/5.44 % ======== iProver multi-core TPTP/SMT =========
% 0.15/5.44
% 0.15/5.44 % Detected problem language: tptp
% 0.15/5.45 % Proving...
% 58.65/18.85 % SZS status Started for theBenchmark.p
% 58.65/18.85 % SZS status Unsatisfiable for theBenchmark.p
% 58.65/18.85
% 58.65/18.85 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 58.65/18.85
% 58.65/18.85 % ------ iProver source info
% 58.65/18.85
% 58.65/18.85 % git: date: 2026-07-19 20:42:38 +0200
% 58.65/18.85 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 58.65/18.85 % git: non_committed_changes: false
% 58.65/18.85
% 58.65/18.85 % ------ Parsing...% successful
% 58.65/18.85
% 58.65/18.85
% 58.65/18.85 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 58.65/18.85
% 58.65/18.85 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe_e sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 58.65/18.85
% 58.65/18.85 % ------ Preprocessing... gs_s sp: 2 0s gs_e snvd_s sp: 0 0s snvd_e %
% 58.65/18.85
% 58.65/18.85 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 58.65/18.85 % ------ Proving...
% 58.65/18.85 % ------ Problem Properties
% 58.65/18.85
% 58.65/18.85 %
% 58.65/18.85 % clauses 201
% 58.65/18.85 % conjectures 17
% 58.65/18.85 % EPR 69
% 58.65/18.85 % Horn 165
% 58.65/18.85 % unary 74
% 58.65/18.85 % binary 27
% 58.65/18.85 % lits 579
% 58.65/18.85 % lits eq 89
% 58.65/18.85 % fd_pure 0
% 58.65/18.85 % fd_pseudo 0
% 58.65/18.85 % fd_cond 17
% 58.65/18.85 % fd_pseudo_cond 14
% 58.65/18.85 % AC symbols 0
% 58.65/18.85
% 58.65/18.85 % ------ Schedule dynamic 5 is on
% 58.65/18.85
% 58.65/18.85 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 58.65/18.85
% 58.65/18.85
% 58.65/18.85 % ------
% 58.65/18.85 % Current options:
% 58.65/18.85 % ------
% 58.65/18.85
% 58.65/18.85
% 58.65/18.85 %
% 58.65/18.85
% 58.65/18.85 % ------ Proving...
% 58.65/18.85 % Proof_search_loop: time out after: 6231 full_loop iterations
% 58.65/18.85
% 58.65/18.85 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" Time Limit: 15.
% 58.65/18.85
% 58.65/18.85
% 58.65/18.85 % ------
% 58.65/18.85 % Current options:
% 58.65/18.85 % ------
% 58.65/18.85
% 58.65/18.85
% 58.65/18.85 %
% 58.65/18.85
% 58.65/18.85 % ------ Proving...
% 58.65/18.85 %
% 58.65/18.85
% 58.65/18.85 % SZS status Unsatisfiable for theBenchmark.p
% 58.65/18.85
% 58.65/18.85 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 58.65/18.85
% 58.65/18.85
%------------------------------------------------------------------------------