%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWC192-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 : n009.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:08:49 PM UTC 2026
% Result : Unsatisfiable 17.87s 8.64s
% Output : CNFRefutation 17.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 42
% Syntax : Number of formulae : 235 ( 77 unt; 6 def)
% Number of atoms : 824 ( 230 equ)
% Maximal formula atoms : 6 ( 3 avg)
% Number of connectives : 632 ( 292 ~; 340 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 12 ( 10 usr; 7 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 9 con; 0-2 aty)
% Number of variables : 142 ( 0 sgn 142 !; 0 ?; 77 :)
% 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(f73,axiom,
! [X0] :
( app(X0,nil) = X0
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause73) ).
fof(f74,axiom,
! [X0] :
( app(nil,X0) = X0
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause74) ).
fof(f77,axiom,
! [X0] :
( nil = X0
| ssList(tl(X0))
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause77) ).
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(f96,axiom,
! [X0,X1] :
( tl(cons(X0,X1)) = X1
| ~ ssList(X1)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause96) ).
fof(f97,axiom,
! [X0,X1] :
( hd(cons(X0,X1)) = X0
| ~ ssList(X1)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause97) ).
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(f107,axiom,
! [X0] :
( nil = X0
| cons(hd(X0),tl(X0)) = X0
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause104) ).
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(f125,axiom,
! [X0,X1] :
( app(cons(X0,nil),X1) = cons(X0,X1)
| ~ ssList(X1)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/SWC001-0.ax',clause123) ).
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(f144,axiom,
! [X0,X1] :
( tl(app(X1,X0)) = app(tl(X1),X0)
| nil = X1
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/SWC001-0.ax',clause140) ).
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(f163,axiom,
! [X2,X0,X1] :
( X0 = X2
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| app(X0,X1) != app(X2,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause151) ).
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(f189,axiom,
! [X2,X3,X0,X1] :
( memberP(X3,X1)
| ~ ssList(X3)
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| app(X0,cons(X1,X2)) != X3 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause175) ).
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,
app(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),sk8) = sk1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_11) ).
fof(f211,plain,
sk1 = app(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),sk8),
inference(reorient_equations,[],[f210]) ).
fof(f213,negated_conjecture,
( nil = sk4
| ssItem(sk9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_13) ).
fof(f214,negated_conjecture,
( nil = sk3
| ssItem(sk9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_14) ).
fof(f215,negated_conjecture,
( nil = sk4
| cons(sk9,nil) = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_15) ).
fof(f216,plain,
( nil = sk4
| sk3 = cons(sk9,nil) ),
inference(reorient_equations,[],[f215]) ).
fof(f218,negated_conjecture,
( nil = sk3
| cons(sk9,nil) = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_17) ).
fof(f219,plain,
( nil = sk3
| sk3 = cons(sk9,nil) ),
inference(reorient_equations,[],[f218]) ).
fof(f223,plain,
sk3 = app(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),sk8),
inference(definition_unfolding,[],[f211,f205]) ).
fof(f234,plain,
! [X0,X1] :
( rearsegP(app(X0,X1),X1)
| ~ ssList(app(X0,X1))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(equality_resolution,[],[f154]) ).
fof(f239,plain,
! [X2,X0,X1] :
( memberP(app(X0,cons(X1,X2)),X1)
| ~ ssList(app(X0,cons(X1,X2)))
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(X2) ),
inference(equality_resolution,[],[f189]) ).
tcf(c_259,plain,
ssList(nil),
inference(cnf_transformation,[],[f8]) ).
tcf(c_301,plain,
! [X0: $i,X1: $i] : ssList(skaf46(X0,X1)),
inference(cnf_transformation,[],[f50]) ).
tcf(c_322,plain,
! [X0: $i] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_324,plain,
! [X0: $i] :
( ( app(X0,nil) = X0 )
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f73]) ).
tcf(c_325,plain,
! [X0: $i] :
( ( app(nil,X0) = X0 )
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_328,plain,
! [X0: $i] :
( ssList(tl(X0))
| ( X0 = nil )
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f77]) ).
tcf(c_336,plain,
! [X0: $i,X1: $i] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_337,plain,
! [X0: $i,X1: $i] :
( ssList(cons(X1,X0))
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_347,plain,
! [X0: $i,X1: $i] :
( ( tl(cons(X1,X0)) = X0 )
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f96]) ).
tcf(c_348,plain,
! [X0: $i,X1: $i] :
( ( hd(cons(X1,X0)) = X1 )
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f97]) ).
tcf(c_349,plain,
! [X0: $i,X1: $i] :
( ~ ssItem(X0)
| ~ ssList(X1)
| ( cons(X0,X1) != nil ) ),
inference(cnf_transformation,[],[f99]) ).
tcf(c_355,plain,
! [X0: $i] :
( ( X0 = nil )
| ( cons(hd(X0),tl(X0)) = X0 )
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f107]) ).
tcf(c_369,plain,
! [X0: $i,X1: $i] :
( ( X0 = nil )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(X0,X1) != nil ) ),
inference(cnf_transformation,[],[f122]) ).
tcf(c_370,plain,
! [X0: $i,X1: $i] :
( ( X1 = nil )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(X0,X1) != nil ) ),
inference(cnf_transformation,[],[f124]) ).
tcf(c_371,plain,
! [X0: $i,X1: $i] :
( ( app(cons(X1,nil),X0) = cons(X1,X0) )
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f126]) ).
tcf(c_374,plain,
! [X0: $i,X1: $i] :
( ( X1 = nil )
| ( hd(app(X1,X0)) = hd(X1) )
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f129]) ).
tcf(c_379,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ ssList(X1)
| ~ ssList(X0)
| ~ rearsegP(X1,X0)
| ~ rearsegP(X0,X1) ),
inference(cnf_transformation,[],[f137]) ).
tcf(c_382,plain,
! [X0: $i,X1: $i] :
( ( app(skaf46(X0,X1),X1) = X0 )
| ~ ssList(X1)
| ~ ssList(X0)
| ~ rearsegP(X0,X1) ),
inference(cnf_transformation,[],[f142]) ).
tcf(c_384,plain,
! [X0: $i,X1: $i] :
( ( X1 = nil )
| ( app(tl(X1),X0) = tl(app(X1,X0)) )
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f144]) ).
tcf(c_391,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_394,plain,
! [X0: $i,X1: $i] :
( rearsegP(app(X0,X1),X1)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(app(X0,X1)) ),
inference(cnf_transformation,[],[f234]) ).
tcf(c_402,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_412,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_426,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(app(X0,cons(X1,X2)),X1)
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(app(X0,cons(X1,X2))) ),
inference(cnf_transformation,[],[f239]) ).
tcf(c_439,negated_conjecture,
ssList(sk3),
inference(cnf_transformation,[],[f202]) ).
tcf(c_440,negated_conjecture,
ssList(sk4),
inference(cnf_transformation,[],[f203]) ).
tcf(c_441,negated_conjecture,
ssItem(sk5),
inference(cnf_transformation,[],[f206]) ).
tcf(c_442,negated_conjecture,
ssItem(sk6),
inference(cnf_transformation,[],[f207]) ).
tcf(c_443,negated_conjecture,
ssList(sk7),
inference(cnf_transformation,[],[f208]) ).
tcf(c_444,negated_conjecture,
ssList(sk8),
inference(cnf_transformation,[],[f209]) ).
tcf(c_445,negated_conjecture,
app(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),sk8) = sk3,
inference(cnf_transformation,[],[f223]) ).
tcf(c_447,negated_conjecture,
( ssItem(sk9)
| ( sk4 = nil ) ),
inference(cnf_transformation,[],[f213]) ).
tcf(c_448,negated_conjecture,
( ssItem(sk9)
| ( sk3 = nil ) ),
inference(cnf_transformation,[],[f214]) ).
tcf(c_449,negated_conjecture,
( ( sk4 = nil )
| ( cons(sk9,nil) = sk3 ) ),
inference(cnf_transformation,[],[f216]) ).
tcf(c_451,negated_conjecture,
( ( sk3 = nil )
| ( cons(sk9,nil) = sk3 ) ),
inference(cnf_transformation,[],[f219]) ).
tcf(c_836,plain,
! [X0: $i,X1: $i] :
( rearsegP(app(X0,X1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_394,c_336]) ).
tcf(c_6548,definition,
iPr_def_12 = cons(sk5,nil),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_6549,definition,
iPr_def_13 = app(sk7,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_6550,definition,
iPr_def_14 = cons(sk6,nil),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_6551,definition,
iPr_def_15 = app(iPr_def_13,iPr_def_14),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_6552,definition,
iPr_def_16 = app(iPr_def_15,sk8),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_6553,definition,
iPr_def_17 = cons(sk9,nil),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_6554,negated_conjecture,
iPr_def_16 = sk3,
inference(demodulation,[status(thm)],[c_445,c_6550,c_6548,c_6549,c_6551,c_6552]) ).
tcf(c_6556,negated_conjecture,
( ( iPr_def_17 = sk3 )
| ( sk3 = nil ) ),
inference(demodulation,[status(thm)],[c_451,c_6553]) ).
tcf(c_6558,negated_conjecture,
( ( iPr_def_17 = sk3 )
| ( sk4 = nil ) ),
inference(demodulation,[status(thm)],[c_449]) ).
tcf(c_6559,negated_conjecture,
( ssItem(sk9)
| ( sk3 = nil ) ),
inference(demodulation,[status(thm)],[c_448]) ).
tcf(c_6560,negated_conjecture,
( ssItem(sk9)
| ( sk4 = nil ) ),
inference(demodulation,[status(thm)],[c_447]) ).
tcf(c_6562,negated_conjecture,
ssList(sk8),
inference(demodulation,[status(thm)],[c_444]) ).
tcf(c_6563,negated_conjecture,
ssList(sk7),
inference(demodulation,[status(thm)],[c_443]) ).
tcf(c_6564,negated_conjecture,
ssItem(sk6),
inference(demodulation,[status(thm)],[c_442]) ).
tcf(c_6565,negated_conjecture,
ssItem(sk5),
inference(demodulation,[status(thm)],[c_441]) ).
tcf(c_6566,negated_conjecture,
ssList(sk4),
inference(demodulation,[status(thm)],[c_440]) ).
tcf(c_6567,negated_conjecture,
ssList(sk3),
inference(demodulation,[status(thm)],[c_439]) ).
tcf(c_9140,plain,
ssList(iPr_def_16),
inference(light_normalisation,[status(thm)],[c_6567,c_6554]) ).
tcf(c_9141,plain,
( ssItem(sk9)
| ( nil = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_6559,c_6554]) ).
tcf(c_9159,plain,
( ( iPr_def_16 = iPr_def_17 )
| ( nil = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_6556,c_6554]) ).
tcf(c_9191,plain,
( ( iPr_def_16 = iPr_def_17 )
| ( sk4 = nil ) ),
inference(light_normalisation,[status(thm)],[c_6558,c_6554]) ).
tcf(c_9390,plain,
app(sk4,nil) = sk4,
inference(superposition,[status(thm)],[c_6566,c_324]) ).
tcf(c_9392,plain,
app(sk8,nil) = sk8,
inference(superposition,[status(thm)],[c_6562,c_324]) ).
tcf(c_9421,plain,
app(iPr_def_16,nil) = iPr_def_16,
inference(superposition,[status(thm)],[c_9140,c_324]) ).
tcf(c_9514,plain,
( ( iPr_def_16 = iPr_def_17 )
| ( app(sk4,iPr_def_16) = sk4 ) ),
inference(superposition,[status(thm)],[c_9159,c_9390]) ).
tcf(c_9520,plain,
( ( iPr_def_16 = iPr_def_17 )
| ( app(sk8,iPr_def_16) = sk8 ) ),
inference(superposition,[status(thm)],[c_9159,c_9392]) ).
tcf(c_9649,plain,
app(nil,sk4) = sk4,
inference(superposition,[status(thm)],[c_6566,c_325]) ).
tcf(c_9736,plain,
( ssList(iPr_def_13)
| ~ ssList(iPr_def_12)
| ~ ssList(sk7) ),
inference(superposition,[status(thm)],[c_6549,c_336]) ).
tcf(c_9737,plain,
( ssList(iPr_def_15)
| ~ ssList(iPr_def_14)
| ~ ssList(iPr_def_13) ),
inference(superposition,[status(thm)],[c_6551,c_336]) ).
tcf(c_9754,plain,
( ssList(iPr_def_13)
| ~ ssList(iPr_def_12) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9736,c_6563]) ).
tcf(c_9841,plain,
( ssList(iPr_def_12)
| ~ ssItem(sk5)
| ~ ssList(nil) ),
inference(superposition,[status(thm)],[c_6548,c_337]) ).
tcf(c_9842,plain,
( ssList(iPr_def_14)
| ~ ssItem(sk6)
| ~ ssList(nil) ),
inference(superposition,[status(thm)],[c_6550,c_337]) ).
tcf(c_9852,plain,
ssList(iPr_def_14),
inference(forward_subsumption_resolution,[status(thm)],[c_9842,c_6564,c_259]) ).
tcf(c_9853,plain,
ssList(iPr_def_12),
inference(forward_subsumption_resolution,[status(thm)],[c_9841,c_6565,c_259]) ).
tcf(c_9864,plain,
ssList(iPr_def_13),
inference(backward_subsumption_resolution,[status(thm)],[c_9754,c_9853]) ).
tcf(c_9893,plain,
app(nil,iPr_def_14) = iPr_def_14,
inference(superposition,[status(thm)],[c_9852,c_325]) ).
tcf(c_10202,plain,
( rearsegP(iPr_def_16,sk8)
| ~ ssList(iPr_def_15)
| ~ ssList(sk8) ),
inference(superposition,[status(thm)],[c_6552,c_836]) ).
tcf(c_10213,plain,
( rearsegP(iPr_def_16,nil)
| ~ ssList(iPr_def_16)
| ~ ssList(nil) ),
inference(superposition,[status(thm)],[c_9421,c_836]) ).
tcf(c_10214,plain,
( rearsegP(sk4,iPr_def_16)
| ( iPr_def_16 = iPr_def_17 )
| ~ ssList(iPr_def_16)
| ~ ssList(sk4) ),
inference(superposition,[status(thm)],[c_9514,c_836]) ).
tcf(c_10216,plain,
( rearsegP(sk8,iPr_def_16)
| ( iPr_def_16 = iPr_def_17 )
| ~ ssList(iPr_def_16)
| ~ ssList(sk8) ),
inference(superposition,[status(thm)],[c_9520,c_836]) ).
tcf(c_10240,plain,
rearsegP(iPr_def_16,nil),
inference(forward_subsumption_resolution,[status(thm)],[c_10213,c_9140,c_259]) ).
tcf(c_10244,plain,
( rearsegP(iPr_def_16,sk8)
| ~ ssList(iPr_def_15) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10202,c_6562]) ).
tcf(c_10261,plain,
( rearsegP(sk8,iPr_def_16)
| ( iPr_def_16 = iPr_def_17 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10216,c_9140,c_6562]) ).
tcf(c_10267,plain,
( rearsegP(sk4,iPr_def_16)
| ( iPr_def_16 = iPr_def_17 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10214,c_9140,c_6566]) ).
tcf(c_10483,plain,
! [X0: $i] :
( ( tl(cons(X0,sk4)) = sk4 )
| ~ ssItem(X0) ),
inference(superposition,[status(thm)],[c_6566,c_347]) ).
tcf(c_10724,plain,
! [X0: $i] :
( ( hd(cons(X0,sk4)) = X0 )
| ~ ssItem(X0) ),
inference(superposition,[status(thm)],[c_6566,c_348]) ).
tcf(c_10906,plain,
( ~ ssItem(sk5)
| ~ ssList(nil)
| ( nil != iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_6548,c_349]) ).
tcf(c_10907,plain,
( ~ ssItem(sk6)
| ~ ssList(nil)
| ( nil != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_6550,c_349]) ).
tcf(c_10915,plain,
nil != iPr_def_14,
inference(forward_subsumption_resolution,[status(thm)],[c_10907,c_6564,c_259]) ).
tcf(c_10916,plain,
nil != iPr_def_12,
inference(forward_subsumption_resolution,[status(thm)],[c_10906,c_6565,c_259]) ).
tcf(c_10979,plain,
rearsegP(iPr_def_16,sk8),
inference(global_subsumption_just,[status(thm)],[c_10244,c_9737,c_9864,c_9852,c_10244]) ).
tcf(c_10995,plain,
( rearsegP(nil,iPr_def_16)
| ( iPr_def_16 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_9191,c_10267]) ).
tcf(c_11076,plain,
( ( sk4 = nil )
| ( tl(cons(sk9,sk4)) = sk4 ) ),
inference(superposition,[status(thm)],[c_6560,c_10483]) ).
tcf(c_11077,plain,
( ( nil = iPr_def_16 )
| ( tl(cons(sk9,sk4)) = sk4 ) ),
inference(superposition,[status(thm)],[c_9141,c_10483]) ).
tcf(c_11753,plain,
! [X0: $i] :
( ( app(cons(X0,nil),sk4) = cons(X0,sk4) )
| ~ ssItem(X0) ),
inference(superposition,[status(thm)],[c_6566,c_371]) ).
tcf(c_11952,plain,
( ( sk4 = nil )
| ( hd(cons(sk9,sk4)) = sk9 ) ),
inference(superposition,[status(thm)],[c_6560,c_10724]) ).
tcf(c_11953,plain,
( ( nil = iPr_def_16 )
| ( hd(cons(sk9,sk4)) = sk9 ) ),
inference(superposition,[status(thm)],[c_9141,c_10724]) ).
tcf(c_12203,plain,
( ( nil = iPr_def_13 )
| ~ ssList(iPr_def_14)
| ~ ssList(iPr_def_13)
| ( nil != iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_6551,c_369]) ).
tcf(c_12204,plain,
( ( nil = iPr_def_15 )
| ~ ssList(iPr_def_15)
| ~ ssList(sk8)
| ( nil != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_6552,c_369]) ).
tcf(c_12239,plain,
( ( nil = iPr_def_15 )
| ~ ssList(iPr_def_15)
| ( nil != iPr_def_16 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12204,c_6562]) ).
tcf(c_12243,plain,
( ( nil = iPr_def_13 )
| ( nil != iPr_def_15 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12203,c_9852,c_9864]) ).
tcf(c_12258,plain,
( ( nil = iPr_def_12 )
| ~ ssList(iPr_def_12)
| ~ ssList(sk7)
| ( nil != iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_6549,c_370]) ).
tcf(c_12259,plain,
( ( nil = iPr_def_14 )
| ~ ssList(iPr_def_14)
| ~ ssList(iPr_def_13)
| ( nil != iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_6551,c_370]) ).
tcf(c_12299,plain,
nil != iPr_def_15,
inference(forward_subsumption_resolution,[status(thm)],[c_12259,c_10915,c_9852,c_9864]) ).
tcf(c_12300,plain,
nil != iPr_def_13,
inference(forward_subsumption_resolution,[status(thm)],[c_12258,c_10916,c_9853,c_6563]) ).
tcf(c_12363,plain,
tl(cons(sk9,sk4)) = sk4,
inference(global_subsumption_just,[status(thm)],[c_11076,c_9737,c_9864,c_9852,c_11077,c_12243,c_12239,c_12300]) ).
tcf(c_12376,plain,
hd(cons(sk9,sk4)) = sk9,
inference(global_subsumption_just,[status(thm)],[c_11952,c_9737,c_9864,c_9852,c_11953,c_12243,c_12239,c_12300]) ).
tcf(c_12425,plain,
! [X0: $i] :
( ( X0 = nil )
| ( hd(app(X0,sk4)) = hd(X0) )
| ~ ssList(X0) ),
inference(superposition,[status(thm)],[c_6566,c_374]) ).
tcf(c_12427,plain,
! [X0: $i] :
( ( X0 = nil )
| ( hd(app(X0,sk8)) = hd(X0) )
| ~ ssList(X0) ),
inference(superposition,[status(thm)],[c_6562,c_374]) ).
tcf(c_13078,plain,
( ( nil = iPr_def_16 )
| ~ ssList(iPr_def_16)
| ~ ssList(nil)
| ~ rearsegP(nil,iPr_def_16) ),
inference(superposition,[status(thm)],[c_10240,c_379]) ).
tcf(c_13093,plain,
( ( iPr_def_16 = iPr_def_17 )
| ( sk8 = iPr_def_16 )
| ~ ssList(iPr_def_16)
| ~ ssList(sk8)
| ~ rearsegP(iPr_def_16,sk8) ),
inference(superposition,[status(thm)],[c_10261,c_379]) ).
tcf(c_13127,plain,
( ( nil = iPr_def_16 )
| ~ rearsegP(nil,iPr_def_16) ),
inference(forward_subsumption_resolution,[status(thm)],[c_13078,c_9140,c_259]) ).
tcf(c_13164,plain,
( ( iPr_def_16 = iPr_def_17 )
| ( sk8 = iPr_def_16 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_13093,c_9140,c_6562,c_10979]) ).
tcf(c_13441,plain,
( ( app(skaf46(iPr_def_16,sk8),sk8) = iPr_def_16 )
| ~ ssList(iPr_def_16)
| ~ ssList(sk8) ),
inference(superposition,[status(thm)],[c_10979,c_382]) ).
tcf(c_13480,plain,
app(skaf46(iPr_def_16,sk8),sk8) = iPr_def_16,
inference(forward_subsumption_resolution,[status(thm)],[c_13441,c_9140,c_6562]) ).
tcf(c_13680,plain,
iPr_def_16 = iPr_def_17,
inference(global_subsumption_just,[status(thm)],[c_13164,c_9737,c_9864,c_9852,c_10995,c_12243,c_12239,c_12300,c_13127]) ).
tcf(c_13730,plain,
cons(sk9,nil) = iPr_def_16,
inference(demodulation,[status(thm)],[c_6553,c_13680]) ).
tcf(c_14297,plain,
! [X0: $i] :
( memberP(iPr_def_16,X0)
| ~ ssList(iPr_def_15)
| ~ ssList(sk8)
| ~ ssItem(X0)
| ~ memberP(iPr_def_15,X0) ),
inference(superposition,[status(thm)],[c_6552,c_391]) ).
tcf(c_14328,plain,
! [X0: $i] :
( memberP(iPr_def_16,X0)
| ~ ssList(iPr_def_15)
| ~ ssItem(X0)
| ~ memberP(iPr_def_15,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14297,c_6562]) ).
tcf(c_14611,plain,
( ( sk8 = nil )
| ~ ssList(sk8)
| ~ ssList(skaf46(iPr_def_16,sk8))
| ( nil != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_13480,c_370]) ).
tcf(c_14620,plain,
( ( sk8 = nil )
| ( nil != iPr_def_16 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14611,c_6562,c_301]) ).
tcf(c_15093,plain,
! [X0: $i] :
( ( X0 = nil )
| ( app(tl(X0),sk4) = tl(app(X0,sk4)) )
| ~ ssList(X0) ),
inference(superposition,[status(thm)],[c_6566,c_384]) ).
tcf(c_15095,plain,
! [X0: $i] :
( ( X0 = nil )
| ( app(tl(X0),sk8) = tl(app(X0,sk8)) )
| ~ ssList(X0) ),
inference(superposition,[status(thm)],[c_6562,c_384]) ).
tcf(c_15496,plain,
nil != iPr_def_16,
inference(global_subsumption_just,[status(thm)],[c_14620,c_9737,c_9864,c_9852,c_12243,c_12239,c_12300]) ).
tcf(c_15499,plain,
ssItem(sk9),
inference(backward_subsumption_resolution,[status(thm)],[c_9141,c_15496]) ).
tcf(c_17143,plain,
! [X0: $i] :
( ( X0 = iPr_def_15 )
| ~ ssList(iPr_def_15)
| ~ ssList(sk8)
| ~ ssList(X0)
| ( app(X0,sk8) != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_6552,c_402]) ).
tcf(c_17168,plain,
! [X0: $i] :
( ( X0 = nil )
| ~ ssList(nil)
| ~ ssList(sk4)
| ~ ssList(X0)
| ( app(X0,sk4) != sk4 ) ),
inference(superposition,[status(thm)],[c_9649,c_402]) ).
tcf(c_17212,plain,
! [X0: $i] :
( ( X0 = nil )
| ~ ssList(X0)
| ( app(X0,sk4) != sk4 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_17168,c_259,c_6566]) ).
tcf(c_17236,plain,
! [X0: $i] :
( ( X0 = iPr_def_15 )
| ~ ssList(iPr_def_15)
| ~ ssList(X0)
| ( app(X0,sk8) != iPr_def_16 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_17143,c_6562]) ).
tcf(c_21053,plain,
! [X0: $i] :
( memberP(app(X0,iPr_def_14),sk6)
| ~ ssItem(sk6)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(app(X0,cons(sk6,nil))) ),
inference(superposition,[status(thm)],[c_6550,c_426]) ).
tcf(c_21062,plain,
! [X0: $i] :
( memberP(app(X0,iPr_def_14),sk6)
| ~ ssItem(sk6)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(app(X0,iPr_def_14)) ),
inference(light_normalisation,[status(thm)],[c_21053,c_6550]) ).
tcf(c_21063,plain,
! [X0: $i] :
( memberP(app(X0,iPr_def_14),sk6)
| ~ ssList(X0)
| ~ ssList(app(X0,iPr_def_14)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_21062,c_6564,c_259]) ).
tcf(c_23573,plain,
app(cons(sk9,nil),sk4) = cons(sk9,sk4),
inference(superposition,[status(thm)],[c_15499,c_11753]) ).
tcf(c_23593,plain,
cons(sk9,sk4) = app(iPr_def_16,sk4),
inference(light_normalisation,[status(thm)],[c_23573,c_13730]) ).
tcf(c_23879,plain,
! [X0: $i] :
( memberP(iPr_def_16,X0)
| ~ memberP(iPr_def_15,X0)
| ~ ssItem(X0) ),
inference(global_subsumption_just,[status(thm)],[c_14328,c_9737,c_9864,c_9852,c_14328]) ).
tcf(c_23880,plain,
! [X0: $i] :
( memberP(iPr_def_16,X0)
| ~ ssItem(X0)
| ~ memberP(iPr_def_15,X0) ),
inference(renaming,[status(thm)],[c_23879]) ).
tcf(c_25565,plain,
( memberP(iPr_def_15,sk6)
| ~ ssList(iPr_def_13)
| ~ ssList(app(iPr_def_13,iPr_def_14)) ),
inference(superposition,[status(thm)],[c_6551,c_21063]) ).
tcf(c_25569,plain,
( memberP(iPr_def_15,sk6)
| ~ ssList(iPr_def_15)
| ~ ssList(iPr_def_13) ),
inference(light_normalisation,[status(thm)],[c_25565,c_6551]) ).
tcf(c_25570,plain,
( memberP(iPr_def_15,sk6)
| ~ ssList(iPr_def_15) ),
inference(forward_subsumption_resolution,[status(thm)],[c_25569,c_9864]) ).
tcf(c_26237,plain,
( ( nil = iPr_def_16 )
| ( hd(app(iPr_def_16,sk4)) = hd(iPr_def_16) ) ),
inference(superposition,[status(thm)],[c_9140,c_12425]) ).
tcf(c_26246,plain,
( ( nil = iPr_def_16 )
| ( hd(iPr_def_16) = sk9 ) ),
inference(light_normalisation,[status(thm)],[c_26237,c_12376,c_23593]) ).
tcf(c_26247,plain,
hd(iPr_def_16) = sk9,
inference(forward_subsumption_resolution,[status(thm)],[c_26246,c_15496]) ).
tcf(c_26918,plain,
! [X0: $i] :
( memberP(nil,X0)
| ( X0 = sk9 )
| ~ ssItem(sk9)
| ~ ssList(nil)
| ~ ssItem(X0)
| ~ memberP(iPr_def_16,X0) ),
inference(superposition,[status(thm)],[c_13730,c_412]) ).
tcf(c_26956,plain,
! [X0: $i] :
( memberP(nil,X0)
| ( X0 = sk9 )
| ~ ssItem(X0)
| ~ memberP(iPr_def_16,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_26918,c_15499,c_259]) ).
tcf(c_27216,plain,
memberP(iPr_def_15,sk6),
inference(global_subsumption_just,[status(thm)],[c_25570,c_9737,c_9864,c_9852,c_25570]) ).
tcf(c_27219,plain,
( memberP(iPr_def_16,sk6)
| ~ ssItem(sk6) ),
inference(superposition,[status(thm)],[c_27216,c_23880]) ).
tcf(c_27220,plain,
memberP(iPr_def_16,sk6),
inference(forward_subsumption_resolution,[status(thm)],[c_27219,c_6564]) ).
tcf(c_29539,plain,
( ( nil = iPr_def_16 )
| ( app(tl(iPr_def_16),sk4) = tl(app(iPr_def_16,sk4)) ) ),
inference(superposition,[status(thm)],[c_9140,c_15093]) ).
tcf(c_29548,plain,
( ( nil = iPr_def_16 )
| ( app(tl(iPr_def_16),sk4) = sk4 ) ),
inference(light_normalisation,[status(thm)],[c_29539,c_12363,c_23593]) ).
tcf(c_29549,plain,
app(tl(iPr_def_16),sk4) = sk4,
inference(forward_subsumption_resolution,[status(thm)],[c_29548,c_15496]) ).
tcf(c_30510,plain,
! [X0: $i] :
( ( X0 = iPr_def_15 )
| ( app(X0,sk8) != iPr_def_16 )
| ~ ssList(X0) ),
inference(global_subsumption_just,[status(thm)],[c_17236,c_9737,c_9864,c_9852,c_17236]) ).
tcf(c_30511,plain,
! [X0: $i] :
( ( X0 = iPr_def_15 )
| ~ ssList(X0)
| ( app(X0,sk8) != iPr_def_16 ) ),
inference(renaming,[status(thm)],[c_30510]) ).
tcf(c_30521,plain,
( ( skaf46(iPr_def_16,sk8) = iPr_def_15 )
| ~ ssList(skaf46(iPr_def_16,sk8)) ),
inference(superposition,[status(thm)],[c_13480,c_30511]) ).
tcf(c_30522,plain,
skaf46(iPr_def_16,sk8) = iPr_def_15,
inference(forward_subsumption_resolution,[status(thm)],[c_30521,c_301]) ).
tcf(c_30530,plain,
app(iPr_def_15,sk8) = iPr_def_16,
inference(demodulation,[status(thm)],[c_13480,c_30522]) ).
tcf(c_31101,plain,
ssList(iPr_def_15),
inference(superposition,[status(thm)],[c_30522,c_301]) ).
tcf(c_31161,plain,
( ( nil = iPr_def_15 )
| ( app(tl(iPr_def_15),sk8) = tl(app(iPr_def_15,sk8)) ) ),
inference(superposition,[status(thm)],[c_31101,c_15095]) ).
tcf(c_31165,plain,
( ( nil = iPr_def_15 )
| ( hd(app(iPr_def_15,sk8)) = hd(iPr_def_15) ) ),
inference(superposition,[status(thm)],[c_31101,c_12427]) ).
tcf(c_31181,plain,
( ( nil = iPr_def_15 )
| ( cons(hd(iPr_def_15),tl(iPr_def_15)) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_31101,c_355]) ).
tcf(c_31190,plain,
cons(hd(iPr_def_15),tl(iPr_def_15)) = iPr_def_15,
inference(forward_subsumption_resolution,[status(thm)],[c_31181,c_12299]) ).
tcf(c_31194,plain,
( ( nil = iPr_def_15 )
| ( hd(iPr_def_15) = sk9 ) ),
inference(light_normalisation,[status(thm)],[c_31165,c_26247,c_30530]) ).
tcf(c_31195,plain,
hd(iPr_def_15) = sk9,
inference(forward_subsumption_resolution,[status(thm)],[c_31194,c_12299]) ).
tcf(c_31200,plain,
( ( nil = iPr_def_15 )
| ( app(tl(iPr_def_15),sk8) = tl(iPr_def_16) ) ),
inference(light_normalisation,[status(thm)],[c_31161,c_30530]) ).
tcf(c_31201,plain,
app(tl(iPr_def_15),sk8) = tl(iPr_def_16),
inference(forward_subsumption_resolution,[status(thm)],[c_31200,c_12299]) ).
tcf(c_40302,plain,
( ( tl(iPr_def_16) = nil )
| ~ ssList(tl(iPr_def_16)) ),
inference(superposition,[status(thm)],[c_29549,c_17212]) ).
tcf(c_53911,plain,
! [X0: $i] :
( memberP(cons(sk9,sk4),X0)
| ~ ssList(iPr_def_16)
| ~ ssList(sk4)
| ~ ssItem(X0)
| ~ memberP(iPr_def_16,X0) ),
inference(superposition,[status(thm)],[c_23593,c_391]) ).
tcf(c_53935,plain,
! [X0: $i] :
( memberP(cons(sk9,sk4),X0)
| ~ ssItem(X0)
| ~ memberP(iPr_def_16,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_53911,c_9140,c_6566]) ).
tcf(c_54581,plain,
! [X0: $i] :
( memberP(sk4,X0)
| ( X0 = sk9 )
| ~ ssItem(sk9)
| ~ ssList(sk4)
| ~ ssItem(X0)
| ~ memberP(iPr_def_16,X0) ),
inference(superposition,[status(thm)],[c_53935,c_412]) ).
tcf(c_54582,plain,
! [X0: $i] :
( memberP(sk4,X0)
| ( X0 = sk9 )
| ~ ssItem(X0)
| ~ memberP(iPr_def_16,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_54581,c_15499,c_6566]) ).
tcf(c_60832,plain,
cons(sk9,tl(iPr_def_15)) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_31190,c_31195]) ).
tcf(c_64084,plain,
( ssList(tl(iPr_def_16))
| ~ ssList(sk8)
| ~ ssList(tl(iPr_def_15)) ),
inference(superposition,[status(thm)],[c_31201,c_336]) ).
tcf(c_64090,plain,
( ( tl(iPr_def_15) = nil )
| ~ ssList(sk8)
| ~ ssList(tl(iPr_def_15))
| ( tl(iPr_def_16) != nil ) ),
inference(superposition,[status(thm)],[c_31201,c_369]) ).
tcf(c_64102,plain,
( ssList(tl(iPr_def_16))
| ~ ssList(tl(iPr_def_15)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_64084,c_6562]) ).
tcf(c_64131,plain,
( ( tl(iPr_def_15) = nil )
| ~ ssList(tl(iPr_def_15))
| ( tl(iPr_def_16) != nil ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_64090,c_6562]) ).
tcf(c_64218,plain,
( ssList(tl(iPr_def_16))
| ( nil = iPr_def_15 )
| ~ ssList(iPr_def_15) ),
inference(superposition,[status(thm)],[c_328,c_64102]) ).
tcf(c_64219,plain,
ssList(tl(iPr_def_16)),
inference(forward_subsumption_resolution,[status(thm)],[c_64218,c_12299,c_31101]) ).
tcf(c_65332,plain,
! [X0: $i] :
( ~ memberP(iPr_def_16,X0)
| ~ ssItem(X0)
| ( X0 = sk9 ) ),
inference(global_subsumption_just,[status(thm)],[c_54582,c_322,c_26956]) ).
tcf(c_65333,plain,
! [X0: $i] :
( ( X0 = sk9 )
| ~ ssItem(X0)
| ~ memberP(iPr_def_16,X0) ),
inference(renaming,[status(thm)],[c_65332]) ).
tcf(c_65342,plain,
( ( sk6 = sk9 )
| ~ ssItem(sk6) ),
inference(superposition,[status(thm)],[c_27220,c_65333]) ).
tcf(c_65345,plain,
sk6 = sk9,
inference(forward_subsumption_resolution,[status(thm)],[c_65342,c_6564]) ).
tcf(c_65418,plain,
cons(sk9,nil) = iPr_def_14,
inference(demodulation,[status(thm)],[c_6550,c_65345]) ).
tcf(c_75122,plain,
( ( tl(iPr_def_15) = nil )
| ~ ssList(tl(iPr_def_15)) ),
inference(global_subsumption_just,[status(thm)],[c_64131,c_40302,c_64131,c_64219]) ).
tcf(c_75128,plain,
( ( nil = iPr_def_15 )
| ( tl(iPr_def_15) = nil )
| ~ ssList(iPr_def_15) ),
inference(superposition,[status(thm)],[c_328,c_75122]) ).
tcf(c_75129,plain,
tl(iPr_def_15) = nil,
inference(forward_subsumption_resolution,[status(thm)],[c_75128,c_12299,c_31101]) ).
tcf(c_75130,plain,
cons(sk9,nil) = iPr_def_15,
inference(demodulation,[status(thm)],[c_60832,c_75129]) ).
tcf(c_75131,plain,
iPr_def_14 = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_75130,c_65418]) ).
tcf(c_75159,plain,
app(iPr_def_13,iPr_def_14) = iPr_def_14,
inference(demodulation,[status(thm)],[c_6551,c_75131]) ).
tcf(c_76263,plain,
! [X0: $i] :
( ( X0 = iPr_def_13 )
| ~ ssList(iPr_def_14)
| ~ ssList(iPr_def_13)
| ~ ssList(X0)
| ( app(X0,iPr_def_14) != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_75159,c_402]) ).
tcf(c_76268,plain,
! [X0: $i] :
( ( X0 = iPr_def_13 )
| ~ ssList(X0)
| ( app(X0,iPr_def_14) != iPr_def_14 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_76263,c_9852,c_9864]) ).
tcf(c_76280,plain,
( ( nil = iPr_def_13 )
| ~ ssList(nil)
| ( app(nil,iPr_def_14) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_76268]) ).
tcf(c_76281,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_76280,c_12300,c_9893,c_259]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC192-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.09/5.39 % Computer : n009.cluster.edu
% 0.09/5.39 % Model : x86_64 x86_64
% 0.09/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.39 % Memory : 8046.5625MB
% 0.09/5.39 % OS : Linux 6.8.0-71-generic
% 0.09/5.39 % CPULimit : 300
% 0.09/5.39 % WCLimit : 300
% 0.09/5.39 % DateTime : Thu Sep 24 16:54:20 UTC 2026
% 0.09/5.39 % CPUTime :
% 0.09/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...
% 17.87/8.64 % SZS status Started for theBenchmark.p
% 17.87/8.64 % SZS status Unsatisfiable for theBenchmark.p
% 17.87/8.64
% 17.87/8.64 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 17.87/8.64
% 17.87/8.64 % ------ iProver source info
% 17.87/8.64
% 17.87/8.64 % git: date: 2026-07-19 20:42:38 +0200
% 17.87/8.64 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 17.87/8.64 % git: non_committed_changes: false
% 17.87/8.64
% 17.87/8.64 % ------ Parsing...% successful
% 17.87/8.64
% 17.87/8.64
% 17.87/8.64 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 17.87/8.64
% 17.87/8.64 % ------ 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 %
% 17.87/8.64
% 17.87/8.64 % ------ Preprocessing... gs_s sp: 2 0s gs_e snvd_s sp: 0 0s snvd_e %
% 17.87/8.64
% 17.87/8.64 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 17.87/8.64 % ------ Proving...
% 17.87/8.64 % ------ Problem Properties
% 17.87/8.64
% 17.87/8.64 %
% 17.87/8.64 % clauses 197
% 17.87/8.64 % conjectures 14
% 17.87/8.64 % EPR 66
% 17.87/8.64 % Horn 163
% 17.87/8.64 % unary 72
% 17.87/8.64 % binary 27
% 17.87/8.64 % lits 567
% 17.87/8.64 % lits eq 85
% 17.87/8.64 % fd_pure 0
% 17.87/8.64 % fd_pseudo 0
% 17.87/8.64 % fd_cond 15
% 17.87/8.64 % fd_pseudo_cond 14
% 17.87/8.64 % AC symbols 0
% 17.87/8.64
% 17.87/8.64 % ------ Schedule dynamic 5 is on
% 17.87/8.64
% 17.87/8.64 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 17.87/8.64
% 17.87/8.64
% 17.87/8.64 % ------
% 17.87/8.64 % Current options:
% 17.87/8.64 % ------
% 17.87/8.64
% 17.87/8.64
% 17.87/8.64 %
% 17.87/8.64
% 17.87/8.64 % ------ Proving...
% 17.87/8.64 %
% 17.87/8.64
% 17.87/8.64 % SZS status Unsatisfiable for theBenchmark.p
% 17.87/8.64
% 17.87/8.64 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 17.87/8.64
% 17.87/8.64
%------------------------------------------------------------------------------