%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SWC189+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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 : Thu Sep 24 09:01:41 AM UTC 2026
% Result : Theorem 75.36s 75.63s
% Output : Proof 75.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 2
% Syntax : Number of formulae : 39 ( 22 unt; 0 def)
% Number of atoms : 274 ( 94 equ)
% Maximal formula atoms : 18 ( 7 avg)
% Number of connectives : 326 ( 91 ~; 77 |; 142 &)
% ( 0 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 8 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 127 ( 0 sgn 60 !; 60 ?)
% Comments :
%------------------------------------------------------------------------------
fof(co1,conjecture,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ! [X3] :
( ssItem(X3)
=> ! [X4] :
( ssItem(X4)
=> ! [X5] :
( ssList(X5)
=> ! [X6] :
( ssList(X6)
=> ( X3 = X4
| app(app(app(X5,cons(X3,nil)),cons(X4,nil)),X6) != U ) ) ) ) )
| ? [Y] :
( ? [Z] :
( ? [X1] :
( ? [X2] :
( app(app(app(X1,cons(Y,nil)),cons(Z,nil)),X2) = W
& Y != Z
& ssList(X2) )
& ssList(X1) )
& ssItem(Z) )
& ssItem(Y) )
| U != W
| V != X ) ) ) ) ),
file('theBenchmark.p',co1) ).
fof(f_96_1,negated_conjecture,
~ ! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ! [X3] :
( ssItem(X3)
=> ! [X4] :
( ssItem(X4)
=> ! [X5] :
( ssList(X5)
=> ! [X6] :
( ssList(X6)
=> ( X3 = X4
| app(app(app(X5,cons(X3,nil)),cons(X4,nil)),X6) != U ) ) ) ) )
| ? [Y] :
( ? [Z] :
( ? [X1] :
( ? [X2] :
( app(app(app(X1,cons(Y,nil)),cons(Z,nil)),X2) = W
& Y != Z
& ssList(X2) )
& ssList(X1) )
& ssItem(Z) )
& ssItem(Y) )
| U != W
| V != X ) ) ) ) ),
inference(negate,[status(cth)],[co1]) ).
fof(f_96_2,negated_conjecture,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( ? [X6] :
( X3 != X4
& app(app(app(X5,cons(X3,nil)),cons(X4,nil)),X6) = U
& ssList(X6) )
& ssList(X5) )
& ssItem(X4) )
& ssItem(X3) )
& ! [Y] :
( ! [Z] :
( ! [X1] :
( ! [X2] :
( app(app(app(X1,cons(Y,nil)),cons(Z,nil)),X2) != W
| Y = Z
| ~ ssList(X2) )
| ~ ssList(X1) )
| ~ ssItem(Z) )
| ~ ssItem(Y) )
& U = W
& V = X
& ssList(X) )
& ssList(W) )
& ssList(V) )
& ssList(U) ),
inference(fof_nnf,[status(thm)],[f_96_1]) ).
fof(f_96_3,negated_conjecture,
? [U_255] :
( ? [U_254] :
( ? [U_253] :
( ? [U_252] :
( ? [U_251] :
( ? [U_250] :
( ? [U_249] :
( ? [U_248] :
( U_251 != U_250
& app(app(app(U_249,cons(U_251,nil)),cons(U_250,nil)),U_248) = U_255
& ssList(U_248) )
& ssList(U_249) )
& ssItem(U_250) )
& ssItem(U_251) )
& ! [U_247] :
( ! [U_246] :
( ! [U_245] :
( ! [U_244] :
( app(app(app(U_245,cons(U_247,nil)),cons(U_246,nil)),U_244) != U_253
| U_247 = U_246
| ~ ssList(U_244) )
| ~ ssList(U_245) )
| ~ ssItem(U_246) )
| ~ ssItem(U_247) )
& U_255 = U_253
& U_254 = U_252
& ssList(U_252) )
& ssList(U_253) )
& ssList(U_254) )
& ssList(U_255) ),
inference(variable_rename,[status(thm)],[f_96_2]) ).
fof(f_96_4,negated_conjecture,
? [U_255] :
( ? [U_254] :
( ? [U_253] :
( ? [U_252] :
( ? [U_251] :
( ? [U_250] :
( ? [U_249] :
( ? [U_248] :
( U_251 != U_250
& app(app(app(U_249,cons(U_251,nil)),cons(U_250,nil)),U_248) = U_255
& ssList(U_248) )
& ssList(U_249) )
& ssItem(U_250) )
& ssItem(U_251) )
& ! [U_247] :
( ! [U_246] :
( ! [U_245] :
( ! [U_244] :
( app(app(app(U_245,cons(U_247,nil)),cons(U_246,nil)),U_244) != U_253
| ~ ssList(U_244) )
| U_247 = U_246
| ~ ssList(U_245) )
| ~ ssItem(U_246) )
| ~ ssItem(U_247) )
& U_255 = U_253
& U_254 = U_252
& ssList(U_252) )
& ssList(U_253) )
& ssList(U_254) )
& ssList(U_255) ),
inference(miniscope,[status(thm)],[f_96_3]) ).
fof(f_96_5,negated_conjecture,
( ? [U_254] :
( ? [U_253] :
( ? [U_252] :
( ? [U_251] :
( ? [U_250] :
( ? [U_249] :
( ? [U_248] :
( U_251 != U_250
& app(app(app(U_249,cons(U_251,nil)),cons(U_250,nil)),U_248) = sK48
& ssList(U_248) )
& ssList(U_249) )
& ssItem(U_250) )
& ssItem(U_251) )
& ! [U_247] :
( ! [U_246] :
( ! [U_245] :
( ! [U_244] :
( app(app(app(U_245,cons(U_247,nil)),cons(U_246,nil)),U_244) != U_253
| ~ ssList(U_244) )
| U_247 = U_246
| ~ ssList(U_245) )
| ~ ssItem(U_246) )
| ~ ssItem(U_247) )
& sK48 = U_253
& U_254 = U_252
& ssList(U_252) )
& ssList(U_253) )
& ssList(U_254) )
& ssList(sK48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK48]),skolemize(U_255,sK48)],[f_96_4]) ).
fof(f_96_6,negated_conjecture,
( ? [U_253] :
( ? [U_252] :
( ? [U_251] :
( ? [U_250] :
( ? [U_249] :
( ? [U_248] :
( U_251 != U_250
& app(app(app(U_249,cons(U_251,nil)),cons(U_250,nil)),U_248) = sK48
& ssList(U_248) )
& ssList(U_249) )
& ssItem(U_250) )
& ssItem(U_251) )
& ! [U_247] :
( ! [U_246] :
( ! [U_245] :
( ! [U_244] :
( app(app(app(U_245,cons(U_247,nil)),cons(U_246,nil)),U_244) != U_253
| ~ ssList(U_244) )
| U_247 = U_246
| ~ ssList(U_245) )
| ~ ssItem(U_246) )
| ~ ssItem(U_247) )
& sK48 = U_253
& sK49 = U_252
& ssList(U_252) )
& ssList(U_253) )
& ssList(sK49)
& ssList(sK48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK49]),skolemize(U_254,sK49)],[f_96_5]) ).
fof(f_96_7,negated_conjecture,
( ? [U_252] :
( ? [U_251] :
( ? [U_250] :
( ? [U_249] :
( ? [U_248] :
( U_251 != U_250
& app(app(app(U_249,cons(U_251,nil)),cons(U_250,nil)),U_248) = sK48
& ssList(U_248) )
& ssList(U_249) )
& ssItem(U_250) )
& ssItem(U_251) )
& ! [U_247] :
( ! [U_246] :
( ! [U_245] :
( ! [U_244] :
( app(app(app(U_245,cons(U_247,nil)),cons(U_246,nil)),U_244) != sK50
| ~ ssList(U_244) )
| U_247 = U_246
| ~ ssList(U_245) )
| ~ ssItem(U_246) )
| ~ ssItem(U_247) )
& sK48 = sK50
& sK49 = U_252
& ssList(U_252) )
& ssList(sK50)
& ssList(sK49)
& ssList(sK48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK50]),skolemize(U_253,sK50)],[f_96_6]) ).
fof(f_96_8,negated_conjecture,
( ? [U_251] :
( ? [U_250] :
( ? [U_249] :
( ? [U_248] :
( U_251 != U_250
& app(app(app(U_249,cons(U_251,nil)),cons(U_250,nil)),U_248) = sK48
& ssList(U_248) )
& ssList(U_249) )
& ssItem(U_250) )
& ssItem(U_251) )
& ! [U_247] :
( ! [U_246] :
( ! [U_245] :
( ! [U_244] :
( app(app(app(U_245,cons(U_247,nil)),cons(U_246,nil)),U_244) != sK50
| ~ ssList(U_244) )
| U_247 = U_246
| ~ ssList(U_245) )
| ~ ssItem(U_246) )
| ~ ssItem(U_247) )
& sK48 = sK50
& sK49 = sK51
& ssList(sK51)
& ssList(sK50)
& ssList(sK49)
& ssList(sK48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK51]),skolemize(U_252,sK51)],[f_96_7]) ).
fof(f_96_9,negated_conjecture,
( ? [U_250] :
( ? [U_249] :
( ? [U_248] :
( sK52 != U_250
& app(app(app(U_249,cons(sK52,nil)),cons(U_250,nil)),U_248) = sK48
& ssList(U_248) )
& ssList(U_249) )
& ssItem(U_250) )
& ssItem(sK52)
& ! [U_247] :
( ! [U_246] :
( ! [U_245] :
( ! [U_244] :
( app(app(app(U_245,cons(U_247,nil)),cons(U_246,nil)),U_244) != sK50
| ~ ssList(U_244) )
| U_247 = U_246
| ~ ssList(U_245) )
| ~ ssItem(U_246) )
| ~ ssItem(U_247) )
& sK48 = sK50
& sK49 = sK51
& ssList(sK51)
& ssList(sK50)
& ssList(sK49)
& ssList(sK48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK52]),skolemize(U_251,sK52)],[f_96_8]) ).
fof(f_96_10,negated_conjecture,
( ? [U_249] :
( ? [U_248] :
( sK52 != sK53
& app(app(app(U_249,cons(sK52,nil)),cons(sK53,nil)),U_248) = sK48
& ssList(U_248) )
& ssList(U_249) )
& ssItem(sK53)
& ssItem(sK52)
& ! [U_247] :
( ! [U_246] :
( ! [U_245] :
( ! [U_244] :
( app(app(app(U_245,cons(U_247,nil)),cons(U_246,nil)),U_244) != sK50
| ~ ssList(U_244) )
| U_247 = U_246
| ~ ssList(U_245) )
| ~ ssItem(U_246) )
| ~ ssItem(U_247) )
& sK48 = sK50
& sK49 = sK51
& ssList(sK51)
& ssList(sK50)
& ssList(sK49)
& ssList(sK48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK53]),skolemize(U_250,sK53)],[f_96_9]) ).
fof(f_96_11,negated_conjecture,
( ? [U_248] :
( sK52 != sK53
& app(app(app(sK54,cons(sK52,nil)),cons(sK53,nil)),U_248) = sK48
& ssList(U_248) )
& ssList(sK54)
& ssItem(sK53)
& ssItem(sK52)
& ! [U_247] :
( ! [U_246] :
( ! [U_245] :
( ! [U_244] :
( app(app(app(U_245,cons(U_247,nil)),cons(U_246,nil)),U_244) != sK50
| ~ ssList(U_244) )
| U_247 = U_246
| ~ ssList(U_245) )
| ~ ssItem(U_246) )
| ~ ssItem(U_247) )
& sK48 = sK50
& sK49 = sK51
& ssList(sK51)
& ssList(sK50)
& ssList(sK49)
& ssList(sK48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK54]),skolemize(U_249,sK54)],[f_96_10]) ).
fof(f_96_12,negated_conjecture,
( sK52 != sK53
& app(app(app(sK54,cons(sK52,nil)),cons(sK53,nil)),sK55) = sK48
& ssList(sK55)
& ssList(sK54)
& ssItem(sK53)
& ssItem(sK52)
& ! [U_247] :
( ! [U_246] :
( ! [U_245] :
( ! [U_244] :
( app(app(app(U_245,cons(U_247,nil)),cons(U_246,nil)),U_244) != sK50
| ~ ssList(U_244) )
| U_247 = U_246
| ~ ssList(U_245) )
| ~ ssItem(U_246) )
| ~ ssItem(U_247) )
& sK48 = sK50
& sK49 = sK51
& ssList(sK51)
& ssList(sK50)
& ssList(sK49)
& ssList(sK48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK55]),skolemize(U_248,sK55)],[f_96_11]) ).
cnf(f_96_18,negated_conjecture,
sK48 = sK50,
inference(clausify,[status(thm)],[f_96_12]) ).
cnf(f_96_19,negated_conjecture,
( app(app(app(U_245,cons(U_247,nil)),cons(U_246,nil)),U_244) != sK50
| ~ ssList(U_244)
| U_247 = U_246
| ~ ssList(U_245)
| ~ ssItem(U_246)
| ~ ssItem(U_247) ),
inference(clausify,[status(thm)],[f_96_12]) ).
cnf(f_96_20,negated_conjecture,
ssItem(sK52),
inference(clausify,[status(thm)],[f_96_12]) ).
cnf(f_96_21,negated_conjecture,
ssItem(sK53),
inference(clausify,[status(thm)],[f_96_12]) ).
cnf(f_96_22,negated_conjecture,
ssList(sK54),
inference(clausify,[status(thm)],[f_96_12]) ).
cnf(f_96_23,negated_conjecture,
ssList(sK55),
inference(clausify,[status(thm)],[f_96_12]) ).
cnf(f_96_24,negated_conjecture,
app(app(app(sK54,cons(sK52,nil)),cons(sK53,nil)),sK55) = sK48,
inference(clausify,[status(thm)],[f_96_12]) ).
cnf(f_96_25,negated_conjecture,
sK52 != sK53,
inference(clausify,[status(thm)],[f_96_12]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(t1,plain,
sK52 != sK53,
inference(start,[status(thm),parent(0:0)],[f_96_25]) ).
cnf(t2,plain,
( ~ ssItem(sK53)
| ~ ssList(sK54)
| app(app(app(sK54,cons(sK52,nil)),cons(sK53,nil)),sK55) != sK50
| ~ ssList(sK55)
| ~ ssItem(sK52)
| sK52 = sK53 ),
inference(extension,[status(thm),parent(t1:1)],[f_96_19]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
ssItem(sK52),
inference(extension,[status(thm),parent(t2:2)],[f_96_20]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
ssList(sK55),
inference(extension,[status(thm),parent(t2:3)],[f_96_23]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t2:3]) ).
cnf(t8,plain,
( sK48 != sK50
| app(app(app(sK54,cons(sK52,nil)),cons(sK53,nil)),sK55) != sK48
| app(app(app(sK54,cons(sK52,nil)),cons(sK53,nil)),sK55) = sK50 ),
inference(extension,[status(thm),parent(t2:4)],[equality_3]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t2:4]) ).
cnf(t10,plain,
app(app(app(sK54,cons(sK52,nil)),cons(sK53,nil)),sK55) = sK48,
inference(extension,[status(thm),parent(t8:2)],[f_96_24]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t8:2]) ).
cnf(t12,plain,
sK48 = sK50,
inference(extension,[status(thm),parent(t8:3)],[f_96_18]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t8:3]) ).
cnf(t14,plain,
ssList(sK54),
inference(extension,[status(thm),parent(t2:5)],[f_96_22]) ).
cnf(t15,plain,
$false,
inference(connection,[status(thm),parent(t14:1)],[t14:1,t2:5]) ).
cnf(t16,plain,
ssItem(sK53),
inference(extension,[status(thm),parent(t2:6)],[f_96_21]) ).
cnf(t17,plain,
$false,
inference(connection,[status(thm),parent(t16:1)],[t16:1,t2:6]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC189+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.03 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n014.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sun Sep 20 02:03:51 UTC 2026
% 0.10/0.35 % CPUTime :
% 75.36/75.63 % SZS status Theorem for theBenchmark
% 75.36/75.63 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------