%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWC412+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 : n004.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:41 PM UTC 2026
% Result : Theorem 65.80s 11.33s
% Output : CNFRefutation 65.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 6
% Syntax : Number of formulae : 91 ( 9 unt; 2 def)
% Number of atoms : 439 ( 117 equ)
% Maximal formula atoms : 28 ( 4 avg)
% Number of connectives : 481 ( 181 ~; 185 |; 91 &)
% ( 0 <=>; 24 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 7 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 : 11 ( 9 usr; 3 prp; 0-4 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-2 aty)
% Number of variables : 257 ( 0 sgn 207 !; 50 ?; 86 :)
% Comments :
%------------------------------------------------------------------------------
fof(f25,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssItem(X1)
=> tl(cons(X1,X0)) = X0 ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax25) ).
fof(f96,conjecture,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> ! [X3] :
( ( ( ! [X16] :
( ssItem(X16)
=> ! [X17] :
( ssItem(X17)
=> ! [X18] :
( app(app(cons(X17,nil),X18),cons(X16,nil)) = X0
| app(app(cons(X16,nil),X18),cons(X17,nil)) != X1
| ~ ssList(X18) ) ) )
| ! [X13] :
( ssItem(X13)
=> ! [X14] :
( ssItem(X14)
=> ! [X15] :
( ssList(X15)
=> app(app(cons(X13,nil),cons(X14,nil)),X15) != X1 ) ) )
| ? [X10] :
( ? [X11] :
( ? [X12] :
( app(app(cons(X10,nil),X12),cons(X11,nil)) = X3
& app(app(cons(X11,nil),X12),cons(X10,nil)) != X2
& ssList(X12) )
& ssItem(X11) )
& ssItem(X10) ) )
& ( ! [X7] :
( ssItem(X7)
=> ! [X8] :
( ssItem(X8)
=> ! [X9] :
( ssList(X9)
=> app(app(cons(X7,nil),cons(X8,nil)),X9) != X1 ) ) )
| ? [X4] :
( ? [X5] :
( ? [X6] :
( app(app(cons(X4,nil),cons(X5,nil)),X6) = X3
& ssList(X6) )
& ssItem(X5) )
& ssItem(X4) ) ) )
| X0 != X2
| X1 != X3
| ~ ssList(X3) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f97,negated_conjecture,
~ ! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> ! [X3] :
( ( ( ! [X16] :
( ssItem(X16)
=> ! [X17] :
( ssItem(X17)
=> ! [X18] :
( app(app(cons(X17,nil),X18),cons(X16,nil)) = X0
| app(app(cons(X16,nil),X18),cons(X17,nil)) != X1
| ~ ssList(X18) ) ) )
| ! [X13] :
( ssItem(X13)
=> ! [X14] :
( ssItem(X14)
=> ! [X15] :
( ssList(X15)
=> app(app(cons(X13,nil),cons(X14,nil)),X15) != X1 ) ) )
| ? [X10] :
( ? [X11] :
( ? [X12] :
( app(app(cons(X10,nil),X12),cons(X11,nil)) = X3
& app(app(cons(X11,nil),X12),cons(X10,nil)) != X2
& ssList(X12) )
& ssItem(X11) )
& ssItem(X10) ) )
& ( ! [X7] :
( ssItem(X7)
=> ! [X8] :
( ssItem(X8)
=> ! [X9] :
( ssList(X9)
=> app(app(cons(X7,nil),cons(X8,nil)),X9) != X1 ) ) )
| ? [X4] :
( ? [X5] :
( ? [X6] :
( app(app(cons(X4,nil),cons(X5,nil)),X6) = X3
& ssList(X6) )
& ssItem(X5) )
& ssItem(X4) ) ) )
| X0 != X2
| X1 != X3
| ~ ssList(X3) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f96]) ).
fof(f131,plain,
! [X0] :
( ~ ssList(X0)
| ! [X1] :
( ~ ssItem(X1)
| tl(cons(X1,X0)) = X0 ) ),
inference(ennf_transformation,[],[f25]) ).
fof(f221,plain,
? [X0] :
( ssList(X0)
& ? [X1] :
( ssList(X1)
& ? [X2] :
( ssList(X2)
& ? [X3] :
( ( ( ? [X16] :
( ssItem(X16)
& ? [X17] :
( ssItem(X17)
& ? [X18] :
( app(app(cons(X17,nil),X18),cons(X16,nil)) != X0
& app(app(cons(X16,nil),X18),cons(X17,nil)) = X1
& ssList(X18) ) ) )
& ? [X13] :
( ssItem(X13)
& ? [X14] :
( ssItem(X14)
& ? [X15] :
( ssList(X15)
& app(app(cons(X13,nil),cons(X14,nil)),X15) = X1 ) ) )
& ! [X10] :
( ! [X11] :
( ! [X12] :
( app(app(cons(X10,nil),X12),cons(X11,nil)) != X3
| app(app(cons(X11,nil),X12),cons(X10,nil)) = X2
| ~ ssList(X12) )
| ~ ssItem(X11) )
| ~ ssItem(X10) ) )
| ( ? [X7] :
( ssItem(X7)
& ? [X8] :
( ssItem(X8)
& ? [X9] :
( ssList(X9)
& app(app(cons(X7,nil),cons(X8,nil)),X9) = X1 ) ) )
& ! [X4] :
( ! [X5] :
( ! [X6] :
( app(app(cons(X4,nil),cons(X5,nil)),X6) != X3
| ~ ssList(X6) )
| ~ ssItem(X5) )
| ~ ssItem(X4) ) ) )
& X0 = X2
& X1 = X3
& ssList(X3) ) ) ) ),
inference(ennf_transformation,[],[f97]) ).
fof(f298,plain,
! [X2,X3,X1,X0] :
( ~ sP7(X2,X3,X1,X0)
| ( sP6(X1,X0)
& ? [X13] :
( ssItem(X13)
& ? [X14] :
( ssItem(X14)
& ? [X15] :
( ssList(X15)
& app(app(cons(X13,nil),cons(X14,nil)),X15) = X1 ) ) )
& ! [X10] :
( ! [X11] :
( ! [X12] :
( app(app(cons(X10,nil),X12),cons(X11,nil)) != X3
| app(app(cons(X11,nil),X12),cons(X10,nil)) = X2
| ~ ssList(X12) )
| ~ ssItem(X11) )
| ~ ssItem(X10) ) ) ),
inference(nnf_transformation,[],[f232]) ).
fof(f299,plain,
! [X0,X1,X2,X3] :
( ~ sP7(X0,X1,X2,X3)
| ( sP6(X2,X3)
& ? [X7] :
( ssItem(X7)
& ? [X8] :
( ssItem(X8)
& ? [X9] :
( ssList(X9)
& app(app(cons(X7,nil),cons(X8,nil)),X9) = X2 ) ) )
& ! [X4] :
( ! [X5] :
( ! [X6] :
( app(app(cons(X4,nil),X6),cons(X5,nil)) != X1
| app(app(cons(X5,nil),X6),cons(X4,nil)) = X0
| ~ ssList(X6) )
| ~ ssItem(X5) )
| ~ ssItem(X4) ) ) ),
inference(rectify,[],[f298]) ).
fof(f300,plain,
! [X0,X1,X2,X3] :
( ~ sP7(X0,X1,X2,X3)
| ( sP6(X2,X3)
& ssItem(sK55(X2))
& ssItem(sK56(X2))
& ssList(sK57(X2))
& app(app(cons(sK55(X2),nil),cons(sK56(X2),nil)),sK57(X2)) = X2
& ! [X4] :
( ! [X5] :
( ! [X6] :
( app(app(cons(X4,nil),X6),cons(X5,nil)) != X1
| app(app(cons(X5,nil),X6),cons(X4,nil)) = X0
| ~ ssList(X6) )
| ~ ssItem(X5) )
| ~ ssItem(X4) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK55,sK56,sK57]),skolemize(X7,sK55(X2)),skolemize(X8,sK56(X2)),skolemize(X9,sK57(X2))],[f299]) ).
fof(f304,plain,
( ssList(sK61)
& ssList(sK62)
& ssList(sK63)
& ( sP7(sK63,sK64,sK62,sK61)
| ( ssItem(sK65)
& ssItem(sK66)
& ssList(sK67)
& sK62 = app(app(cons(sK65,nil),cons(sK66,nil)),sK67)
& ! [X4] :
( ! [X5] :
( ! [X6] :
( app(app(cons(X4,nil),cons(X5,nil)),X6) != sK64
| ~ ssList(X6) )
| ~ ssItem(X5) )
| ~ ssItem(X4) ) ) )
& sK61 = sK63
& sK62 = sK64
& ssList(sK64) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK61,sK62,sK63,sK64,sK65,sK66,sK67]),skolemize(X0,sK61),skolemize(X1,sK62),skolemize(X2,sK63),skolemize(X3,sK64),skolemize(X7,sK65),skolemize(X8,sK66),skolemize(X9,sK67)],[f233]) ).
fof(f408,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssItem(X1)
| tl(cons(X1,X0)) = X0 ),
inference(cnf_transformation,[],[f131]) ).
fof(f504,plain,
! [X2,X3,X0,X1] :
( ~ sP7(X0,X1,X2,X3)
| sP6(X2,X3) ),
inference(cnf_transformation,[],[f300]) ).
fof(f505,plain,
! [X2,X3,X0,X1] :
( ~ sP7(X0,X1,X2,X3)
| ssItem(sK55(X2)) ),
inference(cnf_transformation,[],[f300]) ).
fof(f508,plain,
! [X2,X3,X0,X1] :
( ~ sP7(X0,X1,X2,X3)
| app(app(cons(sK55(X2),nil),cons(sK56(X2),nil)),sK57(X2)) = X2 ),
inference(cnf_transformation,[],[f300]) ).
fof(f509,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sP7(X0,X1,X2,X3)
| app(app(cons(X4,nil),X6),cons(X5,nil)) != X1
| app(app(cons(X5,nil),X6),cons(X4,nil)) = X0
| ~ ssList(X6)
| ~ ssItem(X5)
| ~ ssItem(X4) ),
inference(cnf_transformation,[],[f300]) ).
fof(f515,plain,
ssList(sK61),
inference(cnf_transformation,[],[f304]) ).
fof(f518,plain,
( sP7(sK63,sK64,sK62,sK61)
| ssItem(sK65) ),
inference(cnf_transformation,[],[f304]) ).
fof(f519,plain,
( sP7(sK63,sK64,sK62,sK61)
| ssItem(sK66) ),
inference(cnf_transformation,[],[f304]) ).
fof(f520,plain,
( sP7(sK63,sK64,sK62,sK61)
| ssList(sK67) ),
inference(cnf_transformation,[],[f304]) ).
fof(f521,plain,
( sP7(sK63,sK64,sK62,sK61)
| sK62 = app(app(cons(sK65,nil),cons(sK66,nil)),sK67) ),
inference(cnf_transformation,[],[f304]) ).
fof(f522,plain,
! [X6,X4,X5] :
( sP7(sK63,sK64,sK62,sK61)
| app(app(cons(X4,nil),cons(X5,nil)),X6) != sK64
| ~ ssList(X6)
| ~ ssItem(X5)
| ~ ssItem(X4) ),
inference(cnf_transformation,[],[f304]) ).
fof(f523,plain,
sK61 = sK63,
inference(cnf_transformation,[],[f304]) ).
fof(f524,plain,
sK62 = sK64,
inference(cnf_transformation,[],[f304]) ).
fof(f526,plain,
! [X6,X4,X5] :
( sP7(sK63,sK64,sK64,sK63)
| app(app(cons(X4,nil),cons(X5,nil)),X6) != sK64
| ~ ssList(X6)
| ~ ssItem(X5)
| ~ ssItem(X4) ),
inference(definition_unfolding,[],[f522,f524,f523]) ).
fof(f527,plain,
( sP7(sK63,sK64,sK64,sK63)
| sK64 = app(app(cons(sK65,nil),cons(sK66,nil)),sK67) ),
inference(definition_unfolding,[],[f521,f524,f524,f523]) ).
fof(f528,plain,
( sP7(sK63,sK64,sK64,sK63)
| ssList(sK67) ),
inference(definition_unfolding,[],[f520,f524,f523]) ).
fof(f529,plain,
( sP7(sK63,sK64,sK64,sK63)
| ssItem(sK66) ),
inference(definition_unfolding,[],[f519,f524,f523]) ).
fof(f530,plain,
( sP7(sK63,sK64,sK64,sK63)
| ssItem(sK65) ),
inference(definition_unfolding,[],[f518,f524,f523]) ).
fof(f532,plain,
ssList(sK63),
inference(definition_unfolding,[],[f515,f523]) ).
fof(f560,plain,
! [X2,X3,X0,X6,X4,X5] :
( ~ sP7(X0,app(app(cons(X4,nil),X6),cons(X5,nil)),X2,X3)
| app(app(cons(X5,nil),X6),cons(X4,nil)) = X0
| ~ ssList(X6)
| ~ ssItem(X5)
| ~ ssItem(X4) ),
inference(equality_resolution,[],[f509]) ).
tcf(c_152,plain,
! [X0: $i,X1: $i] :
( ( tl(cons(X0,X1)) = X1 )
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[],[f408]) ).
tcf(c_246,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( app(app(cons(X3,nil),X2),cons(X1,nil)) = X0 )
| ~ ssList(X2)
| ~ ssItem(X3)
| ~ ssItem(X1)
| ~ sP7(X0,app(app(cons(X1,nil),X2),cons(X3,nil)),X4,X5) ),
inference(cnf_transformation,[],[f560]) ).
tcf(c_247,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( app(app(cons(sK55(X2),nil),cons(sK56(X2),nil)),sK57(X2)) = X2 )
| ~ sP7(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f508]) ).
tcf(c_250,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ssItem(sK55(X2))
| ~ sP7(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f505]) ).
tcf(c_251,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP6(X2,X3)
| ~ sP7(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f504]) ).
tcf(c_258,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( sP7(sK63,sK64,sK64,sK63)
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X0)
| ( app(app(cons(X0,nil),cons(X1,nil)),X2) != sK64 ) ),
inference(cnf_transformation,[],[f526]) ).
tcf(c_259,negated_conjecture,
( sP7(sK63,sK64,sK64,sK63)
| ( app(app(cons(sK65,nil),cons(sK66,nil)),sK67) = sK64 ) ),
inference(cnf_transformation,[],[f527]) ).
tcf(c_260,negated_conjecture,
( ssList(sK67)
| sP7(sK63,sK64,sK64,sK63) ),
inference(cnf_transformation,[],[f528]) ).
tcf(c_261,negated_conjecture,
( ssItem(sK66)
| sP7(sK63,sK64,sK64,sK63) ),
inference(cnf_transformation,[],[f529]) ).
tcf(c_262,negated_conjecture,
( ssItem(sK65)
| sP7(sK63,sK64,sK64,sK63) ),
inference(cnf_transformation,[],[f530]) ).
tcf(c_265,negated_conjecture,
ssList(sK63),
inference(cnf_transformation,[],[f532]) ).
tcf(c_8816,negated_conjecture,
( ssItem(sK65)
| sP7(sK63,sK64,sK64,sK63) ),
inference(subtyping,[status(esa)],[c_262]) ).
tcf(c_8819,negated_conjecture,
( sP7(sK63,sK64,sK64,sK63)
| ( app(app(cons(sK65,nil),cons(sK66,nil)),sK67) = sK64 ) ),
inference(subtyping,[status(esa)],[c_259]) ).
tcf(c_8820,negated_conjecture,
! [X0_iProver_sP4_1: iProver_sP4_1,X0_iProver_ssItem_1: iProver_ssItem_1,X1_iProver_ssItem_1: iProver_ssItem_1] :
( sP7(sK63,sK64,sK64,sK63)
| ~ ssList(X0_iProver_sP4_1)
| ~ ssItem(X1_iProver_ssItem_1)
| ~ ssItem(X0_iProver_ssItem_1)
| ( app(app(cons(X0_iProver_ssItem_1,nil),cons(X1_iProver_ssItem_1,nil)),X0_iProver_sP4_1) != sK64 ) ),
inference(subtyping,[status(esa)],[c_258]) ).
tcf(c_8827,plain,
! [X0_iProver_sP4_1: iProver_sP4_1,X1_iProver_sP4_1: iProver_sP4_1,X2_iProver_sP4_1: iProver_sP4_1,X3_iProver_sP4_1: iProver_sP4_1] :
( sP6(X2_iProver_sP4_1,X3_iProver_sP4_1)
| ~ sP7(X0_iProver_sP4_1,X1_iProver_sP4_1,X2_iProver_sP4_1,X3_iProver_sP4_1) ),
inference(subtyping,[status(esa)],[c_251]) ).
tcf(c_8828,plain,
! [X0_iProver_sP4_1: iProver_sP4_1,X1_iProver_sP4_1: iProver_sP4_1,X2_iProver_sP4_1: iProver_sP4_1,X3_iProver_sP4_1: iProver_sP4_1] :
( ssItem(sK55(X2_iProver_sP4_1))
| ~ sP7(X0_iProver_sP4_1,X1_iProver_sP4_1,X2_iProver_sP4_1,X3_iProver_sP4_1) ),
inference(subtyping,[status(esa)],[c_250]) ).
tcf(c_8831,plain,
! [X0_iProver_sP4_1: iProver_sP4_1,X1_iProver_sP4_1: iProver_sP4_1,X2_iProver_sP4_1: iProver_sP4_1,X3_iProver_sP4_1: iProver_sP4_1] :
( ( app(app(cons(sK55(X2_iProver_sP4_1),nil),cons(sK56(X2_iProver_sP4_1),nil)),sK57(X2_iProver_sP4_1)) = X2_iProver_sP4_1 )
| ~ sP7(X0_iProver_sP4_1,X1_iProver_sP4_1,X2_iProver_sP4_1,X3_iProver_sP4_1) ),
inference(subtyping,[status(esa)],[c_247]) ).
tcf(c_8832,plain,
! [X0_iProver_sP4_1: iProver_sP4_1,X0_iProver_ssItem_1: iProver_ssItem_1,X1_iProver_sP4_1: iProver_sP4_1,X1_iProver_ssItem_1: iProver_ssItem_1,X2_iProver_sP4_1: iProver_sP4_1,X3_iProver_sP4_1: iProver_sP4_1] :
( ( app(app(cons(X1_iProver_ssItem_1,nil),X1_iProver_sP4_1),cons(X0_iProver_ssItem_1,nil)) = X0_iProver_sP4_1 )
| ~ ssList(X1_iProver_sP4_1)
| ~ ssItem(X1_iProver_ssItem_1)
| ~ ssItem(X0_iProver_ssItem_1)
| ~ sP7(X0_iProver_sP4_1,app(app(cons(X0_iProver_ssItem_1,nil),X1_iProver_sP4_1),cons(X1_iProver_ssItem_1,nil)),X2_iProver_sP4_1,X3_iProver_sP4_1) ),
inference(subtyping,[status(esa)],[c_246]) ).
tcf(c_8912,plain,
! [X0_iProver_sP4_1: iProver_sP4_1,X0_iProver_ssItem_1: iProver_ssItem_1] :
( ( tl(cons(X0_iProver_ssItem_1,X0_iProver_sP4_1)) = X0_iProver_sP4_1 )
| ~ ssList(X0_iProver_sP4_1)
| ~ ssItem(X0_iProver_ssItem_1) ),
inference(subtyping,[status(esa)],[c_152]) ).
tcf(c_9002,plain,
! [X0_iProver_sP4_1: iProver_sP4_1] : X0_iProver_sP4_1 = X0_iProver_sP4_1,
theory(equality) ).
tcf(c_9026,plain,
! [X0_iProver_sP4_1: iProver_sP4_1,X1_iProver_sP4_1: iProver_sP4_1,X2_iProver_sP4_1: iProver_sP4_1,X3_iProver_sP4_1: iProver_sP4_1,X4_iProver_sP4_1: iProver_sP4_1,X5_iProver_sP4_1: iProver_sP4_1,X6_iProver_sP4_1: iProver_sP4_1,X7_iProver_sP4_1: iProver_sP4_1] :
( sP7(X0_iProver_sP4_1,X2_iProver_sP4_1,X4_iProver_sP4_1,X6_iProver_sP4_1)
| ~ sP7(X1_iProver_sP4_1,X3_iProver_sP4_1,X5_iProver_sP4_1,X7_iProver_sP4_1)
| ( X6_iProver_sP4_1 != X7_iProver_sP4_1 )
| ( X4_iProver_sP4_1 != X5_iProver_sP4_1 )
| ( X2_iProver_sP4_1 != X3_iProver_sP4_1 )
| ( X0_iProver_sP4_1 != X1_iProver_sP4_1 ) ),
theory(equality) ).
tcf(c_13042,plain,
( ssItem(sK55(sK64))
| ~ sP7(sK63,sK64,sK64,sK63) ),
inference(instantiation,[status(thm)],[c_8828]) ).
tcf(c_13100,plain,
( sP6(sK64,sK63)
| ~ sP7(sK63,sK64,sK64,sK63) ),
inference(instantiation,[status(thm)],[c_8827]) ).
tcf(c_13143,plain,
( ( app(app(cons(sK55(sK64),nil),cons(sK56(sK64),nil)),sK57(sK64)) = sK64 )
| ~ sP7(sK63,sK64,sK64,sK63) ),
inference(instantiation,[status(thm)],[c_8831]) ).
tcf(c_13144,plain,
! [X0_iProver_sP4_1: iProver_sP4_1,X1_iProver_sP4_1: iProver_sP4_1,X2_iProver_sP4_1: iProver_sP4_1,X3_iProver_sP4_1: iProver_sP4_1] :
( sP7(X0_iProver_sP4_1,X1_iProver_sP4_1,X2_iProver_sP4_1,X3_iProver_sP4_1)
| ~ sP7(sK63,sK64,sK64,sK63)
| ( X3_iProver_sP4_1 != sK63 )
| ( X2_iProver_sP4_1 != sK64 )
| ( X1_iProver_sP4_1 != sK64 )
| ( X0_iProver_sP4_1 != sK63 ) ),
inference(instantiation,[status(thm)],[c_9026]) ).
tcf(c_13299,plain,
! [X0_iProver_sP4_1: iProver_sP4_1] :
( ( tl(cons(sK55(sK64),X0_iProver_sP4_1)) = X0_iProver_sP4_1 )
| ~ ssList(X0_iProver_sP4_1)
| ~ ssItem(sK55(sK64)) ),
inference(instantiation,[status(thm)],[c_8912]) ).
tcf(c_13825,plain,
( sP7(sK63,sK64,sK64,sK63)
| ~ ssList(sK67)
| ~ ssItem(sK66)
| ~ ssItem(sK65)
| ( app(app(cons(sK65,nil),cons(sK66,nil)),sK67) != sK64 ) ),
inference(instantiation,[status(thm)],[c_8820]) ).
tcf(c_14553,plain,
sK63 = sK63,
inference(instantiation,[status(thm)],[c_9002]) ).
tcf(c_15251,negated_conjecture,
sP7(sK63,sK64,sK64,sK63),
inference(global_subsumption_just,[status(thm)],[c_8816,c_262,c_261,c_260,c_8819,c_13825]) ).
tcf(c_16949,plain,
( ( tl(cons(sK55(sK64),sK63)) = sK63 )
| ~ ssList(sK63)
| ~ ssItem(sK55(sK64)) ),
inference(instantiation,[status(thm)],[c_13299]) ).
tcf(c_16950,plain,
! [X0_iProver_sP4_1: iProver_sP4_1,X1_iProver_sP4_1: iProver_sP4_1,X2_iProver_sP4_1: iProver_sP4_1] :
( sP7(X0_iProver_sP4_1,X1_iProver_sP4_1,X2_iProver_sP4_1,tl(cons(sK55(sK64),sK63)))
| ~ sP7(sK63,sK64,sK64,sK63)
| ( X2_iProver_sP4_1 != sK64 )
| ( X1_iProver_sP4_1 != sK64 )
| ( X0_iProver_sP4_1 != sK63 )
| ( tl(cons(sK55(sK64),sK63)) != sK63 ) ),
inference(instantiation,[status(thm)],[c_13144]) ).
tcf(c_30837,plain,
! [X0_iProver_sP4_1: iProver_sP4_1,X1_iProver_sP4_1: iProver_sP4_1] :
( sP7(X0_iProver_sP4_1,X1_iProver_sP4_1,app(app(cons(sK55(sK64),nil),cons(sK56(sK64),nil)),sK57(sK64)),tl(cons(sK55(sK64),sK63)))
| ~ sP7(sK63,sK64,sK64,sK63)
| ( X1_iProver_sP4_1 != sK64 )
| ( X0_iProver_sP4_1 != sK63 )
| ( tl(cons(sK55(sK64),sK63)) != sK63 )
| ( app(app(cons(sK55(sK64),nil),cons(sK56(sK64),nil)),sK57(sK64)) != sK64 ) ),
inference(instantiation,[status(thm)],[c_16950]) ).
tcf(c_37852,plain,
! [X0_iProver_sP4_1: iProver_sP4_1] :
( sP7(X0_iProver_sP4_1,app(app(cons(sK58(sK64,sK63),nil),sK60(sK64,sK63)),cons(sK59(sK64,sK63),nil)),app(app(cons(sK55(sK64),nil),cons(sK56(sK64),nil)),sK57(sK64)),tl(cons(sK55(sK64),sK63)))
| ~ sP7(sK63,sK64,sK64,sK63)
| ( X0_iProver_sP4_1 != sK63 )
| ( tl(cons(sK55(sK64),sK63)) != sK63 )
| ( app(app(cons(sK55(sK64),nil),cons(sK56(sK64),nil)),sK57(sK64)) != sK64 )
| ( app(app(cons(sK58(sK64,sK63),nil),sK60(sK64,sK63)),cons(sK59(sK64,sK63),nil)) != sK64 ) ),
inference(instantiation,[status(thm)],[c_30837]) ).
tcf(c_53399,plain,
( sP7(sK63,app(app(cons(sK58(sK64,sK63),nil),sK60(sK64,sK63)),cons(sK59(sK64,sK63),nil)),app(app(cons(sK55(sK64),nil),cons(sK56(sK64),nil)),sK57(sK64)),tl(cons(sK55(sK64),sK63)))
| ~ sP7(sK63,sK64,sK64,sK63)
| ( sK63 != sK63 )
| ( tl(cons(sK55(sK64),sK63)) != sK63 )
| ( app(app(cons(sK55(sK64),nil),cons(sK56(sK64),nil)),sK57(sK64)) != sK64 )
| ( app(app(cons(sK58(sK64,sK63),nil),sK60(sK64,sK63)),cons(sK59(sK64,sK63),nil)) != sK64 ) ),
inference(instantiation,[status(thm)],[c_37852]) ).
tcf(c_61559,plain,
( ( app(app(cons(sK59(sK64,sK63),nil),sK60(sK64,sK63)),cons(sK58(sK64,sK63),nil)) = sK63 )
| ~ ssList(sK60(sK64,sK63))
| ~ ssItem(sK59(sK64,sK63))
| ~ ssItem(sK58(sK64,sK63))
| ~ sP7(sK63,app(app(cons(sK58(sK64,sK63),nil),sK60(sK64,sK63)),cons(sK59(sK64,sK63),nil)),app(app(cons(sK55(sK64),nil),cons(sK56(sK64),nil)),sK57(sK64)),tl(cons(sK55(sK64),sK63))) ),
inference(instantiation,[status(thm)],[c_8832]) ).
fof(f231,definition,
! [X1,X0] :
( ~ sP6(X1,X0)
| ? [X16] :
( ssItem(X16)
& ? [X17] :
( ssItem(X17)
& ? [X18] :
( app(app(cons(X17,nil),X18),cons(X16,nil)) != X0
& app(app(cons(X16,nil),X18),cons(X17,nil)) = X1
& ssList(X18) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f232,definition,
! [X2,X3,X1,X0] :
( ~ sP7(X2,X3,X1,X0)
| ( sP6(X1,X0)
& ? [X13] :
( ssItem(X13)
& ? [X14] :
( ssItem(X14)
& ? [X15] :
( ssList(X15)
& app(app(cons(X13,nil),cons(X14,nil)),X15) = X1 ) ) )
& ! [X10] :
( ! [X11] :
( ! [X12] :
( app(app(cons(X10,nil),X12),cons(X11,nil)) != X3
| app(app(cons(X11,nil),X12),cons(X10,nil)) = X2
| ~ ssList(X12) )
| ~ ssItem(X11) )
| ~ ssItem(X10) ) ) ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f233,plain,
? [X0] :
( ssList(X0)
& ? [X1] :
( ssList(X1)
& ? [X2] :
( ssList(X2)
& ? [X3] :
( ( sP7(X2,X3,X1,X0)
| ( ? [X7] :
( ssItem(X7)
& ? [X8] :
( ssItem(X8)
& ? [X9] :
( ssList(X9)
& app(app(cons(X7,nil),cons(X8,nil)),X9) = X1 ) ) )
& ! [X4] :
( ! [X5] :
( ! [X6] :
( app(app(cons(X4,nil),cons(X5,nil)),X6) != X3
| ~ ssList(X6) )
| ~ ssItem(X5) )
| ~ ssItem(X4) ) ) )
& X0 = X2
& X1 = X3
& ssList(X3) ) ) ) ),
inference(definition_folding,[],[f221,f232,f231]) ).
fof(f301,plain,
! [X1,X0] :
( ~ sP6(X1,X0)
| ? [X16] :
( ssItem(X16)
& ? [X17] :
( ssItem(X17)
& ? [X18] :
( app(app(cons(X17,nil),X18),cons(X16,nil)) != X0
& app(app(cons(X16,nil),X18),cons(X17,nil)) = X1
& ssList(X18) ) ) ) ),
inference(nnf_transformation,[],[f231]) ).
fof(f302,plain,
! [X0,X1] :
( ~ sP6(X0,X1)
| ? [X2] :
( ssItem(X2)
& ? [X3] :
( ssItem(X3)
& ? [X4] :
( app(app(cons(X3,nil),X4),cons(X2,nil)) != X1
& app(app(cons(X2,nil),X4),cons(X3,nil)) = X0
& ssList(X4) ) ) ) ),
inference(rectify,[],[f301]) ).
fof(f303,plain,
! [X0,X1] :
( ~ sP6(X0,X1)
| ( ssItem(sK58(X0,X1))
& ssItem(sK59(X0,X1))
& app(app(cons(sK59(X0,X1),nil),sK60(X0,X1)),cons(sK58(X0,X1),nil)) != X1
& app(app(cons(sK58(X0,X1),nil),sK60(X0,X1)),cons(sK59(X0,X1),nil)) = X0
& ssList(sK60(X0,X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK58,sK59,sK60]),skolemize(X2,sK58(X0,X1)),skolemize(X3,sK59(X0,X1)),skolemize(X4,sK60(X0,X1))],[f302]) ).
fof(f510,plain,
! [X0,X1] :
( ~ sP6(X0,X1)
| ssItem(sK58(X0,X1)) ),
inference(cnf_transformation,[],[f303]) ).
fof(f511,plain,
! [X0,X1] :
( ~ sP6(X0,X1)
| ssItem(sK59(X0,X1)) ),
inference(cnf_transformation,[],[f303]) ).
fof(f512,plain,
! [X0,X1] :
( ~ sP6(X0,X1)
| app(app(cons(sK59(X0,X1),nil),sK60(X0,X1)),cons(sK58(X0,X1),nil)) != X1 ),
inference(cnf_transformation,[],[f303]) ).
fof(f513,plain,
! [X0,X1] :
( ~ sP6(X0,X1)
| app(app(cons(sK58(X0,X1),nil),sK60(X0,X1)),cons(sK59(X0,X1),nil)) = X0 ),
inference(cnf_transformation,[],[f303]) ).
fof(f514,plain,
! [X0,X1] :
( ~ sP6(X0,X1)
| ssList(sK60(X0,X1)) ),
inference(cnf_transformation,[],[f303]) ).
tcf(c_252,plain,
! [X0: $i,X1: $i] :
( ssList(sK60(X0,X1))
| ~ sP6(X0,X1) ),
inference(cnf_transformation,[],[f514]) ).
tcf(c_253,plain,
! [X0: $i,X1: $i] :
( ( app(app(cons(sK58(X0,X1),nil),sK60(X0,X1)),cons(sK59(X0,X1),nil)) = X0 )
| ~ sP6(X0,X1) ),
inference(cnf_transformation,[],[f513]) ).
tcf(c_254,plain,
! [X0: $i,X1: $i] :
( ~ sP6(X0,X1)
| ( app(app(cons(sK59(X0,X1),nil),sK60(X0,X1)),cons(sK58(X0,X1),nil)) != X1 ) ),
inference(cnf_transformation,[],[f512]) ).
tcf(c_255,plain,
! [X0: $i,X1: $i] :
( ssItem(sK59(X0,X1))
| ~ sP6(X0,X1) ),
inference(cnf_transformation,[],[f511]) ).
tcf(c_256,plain,
! [X0: $i,X1: $i] :
( ssItem(sK58(X0,X1))
| ~ sP6(X0,X1) ),
inference(cnf_transformation,[],[f510]) ).
tcf(c_8822,plain,
! [X0_iProver_sP4_1: iProver_sP4_1,X1_iProver_sP4_1: iProver_sP4_1] :
( ssItem(sK58(X0_iProver_sP4_1,X1_iProver_sP4_1))
| ~ sP6(X0_iProver_sP4_1,X1_iProver_sP4_1) ),
inference(subtyping,[status(esa)],[c_256]) ).
tcf(c_8823,plain,
! [X0_iProver_sP4_1: iProver_sP4_1,X1_iProver_sP4_1: iProver_sP4_1] :
( ssItem(sK59(X0_iProver_sP4_1,X1_iProver_sP4_1))
| ~ sP6(X0_iProver_sP4_1,X1_iProver_sP4_1) ),
inference(subtyping,[status(esa)],[c_255]) ).
tcf(c_8824,plain,
! [X0_iProver_sP4_1: iProver_sP4_1,X1_iProver_sP4_1: iProver_sP4_1] :
( ~ sP6(X0_iProver_sP4_1,X1_iProver_sP4_1)
| ( app(app(cons(sK59(X0_iProver_sP4_1,X1_iProver_sP4_1),nil),sK60(X0_iProver_sP4_1,X1_iProver_sP4_1)),cons(sK58(X0_iProver_sP4_1,X1_iProver_sP4_1),nil)) != X1_iProver_sP4_1 ) ),
inference(subtyping,[status(esa)],[c_254]) ).
tcf(c_8825,plain,
! [X0_iProver_sP4_1: iProver_sP4_1,X1_iProver_sP4_1: iProver_sP4_1] :
( ( app(app(cons(sK58(X0_iProver_sP4_1,X1_iProver_sP4_1),nil),sK60(X0_iProver_sP4_1,X1_iProver_sP4_1)),cons(sK59(X0_iProver_sP4_1,X1_iProver_sP4_1),nil)) = X0_iProver_sP4_1 )
| ~ sP6(X0_iProver_sP4_1,X1_iProver_sP4_1) ),
inference(subtyping,[status(esa)],[c_253]) ).
tcf(c_8826,plain,
! [X0_iProver_sP4_1: iProver_sP4_1,X1_iProver_sP4_1: iProver_sP4_1] :
( ssList(sK60(X0_iProver_sP4_1,X1_iProver_sP4_1))
| ~ sP6(X0_iProver_sP4_1,X1_iProver_sP4_1) ),
inference(subtyping,[status(esa)],[c_252]) ).
tcf(c_13521,plain,
( ( app(app(cons(sK58(sK64,sK63),nil),sK60(sK64,sK63)),cons(sK59(sK64,sK63),nil)) = sK64 )
| ~ sP6(sK64,sK63) ),
inference(instantiation,[status(thm)],[c_8825]) ).
tcf(c_13522,plain,
( ~ sP6(sK64,sK63)
| ( app(app(cons(sK59(sK64,sK63),nil),sK60(sK64,sK63)),cons(sK58(sK64,sK63),nil)) != sK63 ) ),
inference(instantiation,[status(thm)],[c_8824]) ).
tcf(c_13523,plain,
( ssList(sK60(sK64,sK63))
| ~ sP6(sK64,sK63) ),
inference(instantiation,[status(thm)],[c_8826]) ).
tcf(c_13524,plain,
( ssItem(sK59(sK64,sK63))
| ~ sP6(sK64,sK63) ),
inference(instantiation,[status(thm)],[c_8823]) ).
tcf(c_13525,plain,
( ssItem(sK58(sK64,sK63))
| ~ sP6(sK64,sK63) ),
inference(instantiation,[status(thm)],[c_8822]) ).
tcf(c_61560,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_61559,c_53399,c_16949,c_15251,c_14553,c_13521,c_13522,c_13523,c_13524,c_13525,c_13143,c_13100,c_13042,c_265]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC412+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.10/0.36 % Computer : n004.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 18:06:52 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/0.39 Running first-order theorem proving
% 0.13/0.39 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.13/0.41
% 0.13/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.41
% 0.13/0.41 % Detected problem language: tptp
% 0.13/0.42 % Proving...
% 65.80/11.33 % SZS status Started for theBenchmark.p
% 65.80/11.33 % SZS status Theorem for theBenchmark.p
% 65.80/11.33
% 65.80/11.33 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 65.80/11.33
% 65.80/11.33 % ------ iProver source info
% 65.80/11.33
% 65.80/11.33 % git: date: 2026-07-19 20:42:38 +0200
% 65.80/11.33 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 65.80/11.33 % git: non_committed_changes: false
% 65.80/11.33
% 65.80/11.33 % ------ Parsing...
% 65.80/11.33 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 65.80/11.33
% 65.80/11.33 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe_e sup_sim: 0 sf_s rm: 4 0s sf_e pe_s pe_e %
% 65.80/11.33
% 65.80/11.33 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 65.80/11.33
% 65.80/11.33 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 65.80/11.33 % ------ Proving...
% 65.80/11.33 % ------ Problem Properties
% 65.80/11.33
% 65.80/11.33 %
% 65.80/11.33 % clauses 198
% 65.80/11.33 % conjectures 7
% 65.80/11.33 % EPR 55
% 65.80/11.33 % Horn 126
% 65.80/11.33 % unary 18
% 65.80/11.33 % binary 54
% 65.80/11.33 % lits 658
% 65.80/11.33 % lits eq 84
% 65.80/11.33 % fd_pure 0
% 65.80/11.33 % fd_pseudo 0
% 65.80/11.33 % fd_cond 21
% 65.80/11.33 % fd_pseudo_cond 15
% 65.80/11.33 % AC symbols 0
% 65.80/11.33
% 65.80/11.33 % ------ Input Options Time Limit: Unbounded
% 65.80/11.33
% 65.80/11.33
% 65.80/11.33 % ------
% 65.80/11.33 % Current options:
% 65.80/11.33 % ------
% 65.80/11.33
% 65.80/11.33
% 65.80/11.33 %
% 65.80/11.33
% 65.80/11.33 % ------ Proving...
% 65.80/11.33 %
% 65.80/11.33
% 65.80/11.33 % SZS status Theorem for theBenchmark.p
% 65.80/11.33
% 65.80/11.33 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 65.80/11.33
% 65.80/11.33
%------------------------------------------------------------------------------