%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SWC096+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:25 AM UTC 2026
% Result : Theorem 84.24s 84.78s
% Output : Proof 84.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 7
% Syntax : Number of formulae : 87 ( 49 unt; 0 def)
% Number of atoms : 320 ( 114 equ)
% Maximal formula atoms : 17 ( 3 avg)
% Number of connectives : 347 ( 114 ~; 105 |; 116 &)
% ( 0 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 91 ( 0 sgn 39 !; 37 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax17,axiom,
ssList(nil),
file('SWC001+0.ax',ax17) ).
fof(ax80,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ( app(V,W) = app(V,U)
=> W = U ) ) ) ),
file('SWC001+0.ax',ax80) ).
fof(co1,conjecture,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ( ( neq(X,nil)
| ~ neq(V,nil) )
& ( ! [X1] :
( ssItem(X1)
=> ! [X2] :
( app(X2,cons(X1,nil)) != X
| cons(X1,nil) != W
| ~ ssList(X2) ) )
| ? [Y] :
( ? [Z] :
( app(Z,cons(Y,nil)) = V
& cons(Y,nil) = U
& ssList(Z) )
& ssItem(Y) )
| ~ neq(V,nil) ) )
| U != W
| V != X
| ~ ssList(X) ) ) ) ),
file('theBenchmark.p',co1) ).
fof(f_17_1,plain,
ssList(nil),
inference(fof_nnf,[status(thm)],[ax17]) ).
cnf(f_17_2,plain,
ssList(nil),
inference(clausify,[status(thm)],[f_17_1]) ).
fof(f_80_1,plain,
! [U] :
( ! [V] :
( ! [W] :
( W = U
| app(V,W) != app(V,U)
| ~ ssList(W) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax80]) ).
fof(f_80_2,plain,
! [U_212] :
( ! [U_211] :
( ! [U_210] :
( U_210 = U_212
| app(U_211,U_210) != app(U_211,U_212)
| ~ ssList(U_210) )
| ~ ssList(U_211) )
| ~ ssList(U_212) ),
inference(variable_rename,[status(thm)],[f_80_1]) ).
cnf(f_80_3,plain,
( U_210 = U_212
| app(U_211,U_210) != app(U_211,U_212)
| ~ ssList(U_210)
| ~ ssList(U_211)
| ~ ssList(U_212) ),
inference(clausify,[status(thm)],[f_80_2]) ).
fof(f_96_1,negated_conjecture,
~ ! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ( ( neq(X,nil)
| ~ neq(V,nil) )
& ( ! [X1] :
( ssItem(X1)
=> ! [X2] :
( app(X2,cons(X1,nil)) != X
| cons(X1,nil) != W
| ~ ssList(X2) ) )
| ? [Y] :
( ? [Z] :
( app(Z,cons(Y,nil)) = V
& cons(Y,nil) = U
& ssList(Z) )
& ssItem(Y) )
| ~ neq(V,nil) ) )
| U != W
| V != X
| ~ ssList(X) ) ) ) ),
inference(negate,[status(cth)],[co1]) ).
fof(f_96_2,negated_conjecture,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ( ( ~ neq(X,nil)
& neq(V,nil) )
| ( ? [X1] :
( ? [X2] :
( app(X2,cons(X1,nil)) = X
& cons(X1,nil) = W
& ssList(X2) )
& ssItem(X1) )
& ! [Y] :
( ! [Z] :
( app(Z,cons(Y,nil)) != V
| cons(Y,nil) != U
| ~ ssList(Z) )
| ~ ssItem(Y) )
& neq(V,nil) ) )
& 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_251] :
( ? [U_250] :
( ? [U_249] :
( ? [U_248] :
( ( ( ~ neq(U_248,nil)
& neq(U_250,nil) )
| ( ? [U_247] :
( ? [U_246] :
( app(U_246,cons(U_247,nil)) = U_248
& cons(U_247,nil) = U_249
& ssList(U_246) )
& ssItem(U_247) )
& ! [U_245] :
( ! [U_244] :
( app(U_244,cons(U_245,nil)) != U_250
| cons(U_245,nil) != U_251
| ~ ssList(U_244) )
| ~ ssItem(U_245) )
& neq(U_250,nil) ) )
& U_251 = U_249
& U_250 = U_248
& ssList(U_248) )
& ssList(U_249) )
& ssList(U_250) )
& ssList(U_251) ),
inference(variable_rename,[status(thm)],[f_96_2]) ).
fof(f_96_4,negated_conjecture,
? [U_251] :
( ? [U_250] :
( ? [U_249] :
( ? [U_248] :
( ( ( ~ neq(U_248,nil)
& neq(U_250,nil) )
| ( ? [U_247] :
( ? [U_246] :
( app(U_246,cons(U_247,nil)) = U_248
& ssList(U_246) )
& cons(U_247,nil) = U_249
& ssItem(U_247) )
& ! [U_245] :
( ! [U_244] :
( app(U_244,cons(U_245,nil)) != U_250
| ~ ssList(U_244) )
| cons(U_245,nil) != U_251
| ~ ssItem(U_245) )
& neq(U_250,nil) ) )
& U_250 = U_248
& ssList(U_248) )
& U_251 = U_249
& ssList(U_249) )
& ssList(U_250) )
& ssList(U_251) ),
inference(miniscope,[status(thm)],[f_96_3]) ).
fof(f_96_5,negated_conjecture,
( ? [U_250] :
( ? [U_249] :
( ? [U_248] :
( ( ( ~ neq(U_248,nil)
& neq(U_250,nil) )
| ( ? [U_247] :
( ? [U_246] :
( app(U_246,cons(U_247,nil)) = U_248
& ssList(U_246) )
& cons(U_247,nil) = U_249
& ssItem(U_247) )
& ! [U_245] :
( ! [U_244] :
( app(U_244,cons(U_245,nil)) != U_250
| ~ ssList(U_244) )
| cons(U_245,nil) != sK48
| ~ ssItem(U_245) )
& neq(U_250,nil) ) )
& U_250 = U_248
& ssList(U_248) )
& sK48 = U_249
& ssList(U_249) )
& ssList(U_250) )
& ssList(sK48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK48]),skolemize(U_251,sK48)],[f_96_4]) ).
fof(f_96_6,negated_conjecture,
( ? [U_249] :
( ? [U_248] :
( ( ( ~ neq(U_248,nil)
& neq(sK49,nil) )
| ( ? [U_247] :
( ? [U_246] :
( app(U_246,cons(U_247,nil)) = U_248
& ssList(U_246) )
& cons(U_247,nil) = U_249
& ssItem(U_247) )
& ! [U_245] :
( ! [U_244] :
( app(U_244,cons(U_245,nil)) != sK49
| ~ ssList(U_244) )
| cons(U_245,nil) != sK48
| ~ ssItem(U_245) )
& neq(sK49,nil) ) )
& sK49 = U_248
& ssList(U_248) )
& sK48 = U_249
& ssList(U_249) )
& ssList(sK49)
& ssList(sK48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK49]),skolemize(U_250,sK49)],[f_96_5]) ).
fof(f_96_7,negated_conjecture,
( ? [U_248] :
( ( ( ~ neq(U_248,nil)
& neq(sK49,nil) )
| ( ? [U_247] :
( ? [U_246] :
( app(U_246,cons(U_247,nil)) = U_248
& ssList(U_246) )
& cons(U_247,nil) = sK50
& ssItem(U_247) )
& ! [U_245] :
( ! [U_244] :
( app(U_244,cons(U_245,nil)) != sK49
| ~ ssList(U_244) )
| cons(U_245,nil) != sK48
| ~ ssItem(U_245) )
& neq(sK49,nil) ) )
& sK49 = U_248
& ssList(U_248) )
& sK48 = sK50
& ssList(sK50)
& ssList(sK49)
& ssList(sK48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK50]),skolemize(U_249,sK50)],[f_96_6]) ).
fof(f_96_8,negated_conjecture,
( ( ( ~ neq(sK51,nil)
& neq(sK49,nil) )
| ( ? [U_247] :
( ? [U_246] :
( app(U_246,cons(U_247,nil)) = sK51
& ssList(U_246) )
& cons(U_247,nil) = sK50
& ssItem(U_247) )
& ! [U_245] :
( ! [U_244] :
( app(U_244,cons(U_245,nil)) != sK49
| ~ ssList(U_244) )
| cons(U_245,nil) != sK48
| ~ ssItem(U_245) )
& neq(sK49,nil) ) )
& sK49 = sK51
& ssList(sK51)
& sK48 = sK50
& ssList(sK50)
& ssList(sK49)
& ssList(sK48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK51]),skolemize(U_248,sK51)],[f_96_7]) ).
fof(f_96_9,negated_conjecture,
( ( ( ~ neq(sK51,nil)
& neq(sK49,nil) )
| ( ? [U_246] :
( app(U_246,cons(sK52,nil)) = sK51
& ssList(U_246) )
& cons(sK52,nil) = sK50
& ssItem(sK52)
& ! [U_245] :
( ! [U_244] :
( app(U_244,cons(U_245,nil)) != sK49
| ~ ssList(U_244) )
| cons(U_245,nil) != sK48
| ~ ssItem(U_245) )
& neq(sK49,nil) ) )
& sK49 = sK51
& ssList(sK51)
& sK48 = sK50
& ssList(sK50)
& ssList(sK49)
& ssList(sK48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK52]),skolemize(U_247,sK52)],[f_96_8]) ).
fof(f_96_10,negated_conjecture,
( ( ( ~ neq(sK51,nil)
& neq(sK49,nil) )
| ( app(sK53,cons(sK52,nil)) = sK51
& ssList(sK53)
& cons(sK52,nil) = sK50
& ssItem(sK52)
& ! [U_245] :
( ! [U_244] :
( app(U_244,cons(U_245,nil)) != sK49
| ~ ssList(U_244) )
| cons(U_245,nil) != sK48
| ~ ssItem(U_245) )
& neq(sK49,nil) ) )
& sK49 = sK51
& ssList(sK51)
& sK48 = sK50
& ssList(sK50)
& ssList(sK49)
& ssList(sK48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK53]),skolemize(U_246,sK53)],[f_96_9]) ).
cnf(f_96_14,negated_conjecture,
sK48 = sK50,
inference(clausify,[status(thm)],[f_96_10]) ).
cnf(f_96_15,negated_conjecture,
ssList(sK51),
inference(clausify,[status(thm)],[f_96_10]) ).
cnf(f_96_16,negated_conjecture,
sK49 = sK51,
inference(clausify,[status(thm)],[f_96_10]) ).
cnf(f_96_17,negated_conjecture,
( neq(sK49,nil)
| neq(sK49,nil) ),
inference(clausify,[status(thm)],[f_96_10]) ).
cnf(f_96_20,negated_conjecture,
( ~ neq(sK51,nil)
| app(U_244,cons(U_245,nil)) != sK49
| ~ ssList(U_244)
| cons(U_245,nil) != sK48
| ~ ssItem(U_245) ),
inference(clausify,[status(thm)],[f_96_10]) ).
cnf(f_96_21,negated_conjecture,
( ssItem(sK52)
| neq(sK49,nil) ),
inference(clausify,[status(thm)],[f_96_10]) ).
cnf(f_96_25,negated_conjecture,
( ssItem(sK52)
| ~ neq(sK51,nil) ),
inference(clausify,[status(thm)],[f_96_10]) ).
cnf(f_96_26,negated_conjecture,
( cons(sK52,nil) = sK50
| ~ neq(sK51,nil) ),
inference(clausify,[status(thm)],[f_96_10]) ).
cnf(f_96_27,negated_conjecture,
( ssList(sK53)
| ~ neq(sK51,nil) ),
inference(clausify,[status(thm)],[f_96_10]) ).
cnf(f_96_28,negated_conjecture,
( app(sK53,cons(sK52,nil)) = sK51
| ~ neq(sK51,nil) ),
inference(clausify,[status(thm)],[f_96_10]) ).
cnf(f_96_17_simplified,negated_conjecture,
neq(sK49,nil),
inference(simplify_clause,[status(thm)],[f_96_17]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
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(equality_54,axiom,
( neq(Eq_y_0,Eq_y_1)
| ~ neq(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(t1,plain,
( cons(sK52,nil) != sK48
| ~ ssList(sK53)
| app(sK53,cons(sK52,nil)) != sK49
| ~ neq(sK51,nil)
| ~ ssItem(sK52) ),
inference(start,[status(thm),parent(0:0)],[f_96_20]) ).
cnf(t2,plain,
( ~ neq(sK51,nil)
| ssItem(sK52) ),
inference(extension,[status(thm),parent(t1:1)],[f_96_25]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( nil != nil
| ~ neq(sK49,nil)
| sK49 != sK51
| neq(sK51,nil) ),
inference(extension,[status(thm),parent(t2:2)],[equality_54]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
sK49 = sK51,
inference(extension,[status(thm),parent(t4:2)],[f_96_16]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(t8,plain,
( ssItem(sK52)
| neq(sK49,nil) ),
inference(extension,[status(thm),parent(t4:3)],[f_96_21]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t4:3]) ).
cnf(t10,plain,
$false,
inference(reduction,[status(thm),parent(t8:2)],[t8:2,t1:1]) ).
cnf(t11,plain,
nil = nil,
inference(extension,[status(thm),parent(t4:4)],[equality_1]) ).
cnf(t12,plain,
$false,
inference(connection,[status(thm),parent(t11:1)],[t11:1,t4:4]) ).
cnf(t13,plain,
( nil != nil
| ~ neq(sK49,nil)
| sK49 != sK51
| neq(sK51,nil) ),
inference(extension,[status(thm),parent(t1:2)],[equality_54]) ).
cnf(t14,plain,
$false,
inference(connection,[status(thm),parent(t13:1)],[t13:1,t1:2]) ).
cnf(t15,plain,
sK49 = sK51,
inference(extension,[status(thm),parent(t13:2)],[f_96_16]) ).
cnf(t16,plain,
$false,
inference(connection,[status(thm),parent(t15:1)],[t15:1,t13:2]) ).
cnf(t17,plain,
neq(sK49,nil),
inference(extension,[status(thm),parent(t13:3)],[f_96_17_simplified]) ).
cnf(t18,plain,
$false,
inference(connection,[status(thm),parent(t17:1)],[t17:1,t13:3]) ).
cnf(t19,plain,
( ~ ssList(sK51)
| ~ ssList(nil)
| app(sK51,nil) != app(sK51,nil)
| ~ ssList(nil)
| nil = nil ),
inference(extension,[status(thm),parent(t13:4)],[f_80_3]) ).
cnf(t20,plain,
$false,
inference(connection,[status(thm),parent(t19:1)],[t19:1,t13:4]) ).
cnf(t21,plain,
ssList(nil),
inference(extension,[status(thm),parent(t19:2)],[f_17_2]) ).
cnf(t22,plain,
$false,
inference(connection,[status(thm),parent(t21:1)],[t21:1,t19:2]) ).
cnf(l11,lemma,
ssList(nil),
inference(lemma,[status(cth),parent(t19:2),below(t13:4)],[t19:2]) ).
cnf(t23,plain,
app(sK51,nil) = app(sK51,nil),
inference(extension,[status(thm),parent(t19:3)],[equality_1]) ).
cnf(t24,plain,
$false,
inference(connection,[status(thm),parent(t23:1)],[t23:1,t19:3]) ).
cnf(t25,plain,
ssList(nil),
inference(lemma_extension,[status(thm),parent(t19:4)],[l11:1]) ).
cnf(t26,plain,
$false,
inference(connection,[status(thm),parent(t25:1)],[t25:1,t19:4]) ).
cnf(t27,plain,
ssList(sK51),
inference(extension,[status(thm),parent(t19:5)],[f_96_15]) ).
cnf(t28,plain,
$false,
inference(connection,[status(thm),parent(t27:1)],[t27:1,t19:5]) ).
cnf(l7,lemma,
neq(sK51,nil),
inference(lemma,[status(cth),parent(t1:2),below(0:0)],[t1:2]) ).
cnf(t29,plain,
( sK51 != sK49
| app(sK53,cons(sK52,nil)) != sK51
| app(sK53,cons(sK52,nil)) = sK49 ),
inference(extension,[status(thm),parent(t1:3)],[equality_3]) ).
cnf(t30,plain,
$false,
inference(connection,[status(thm),parent(t29:1)],[t29:1,t1:3]) ).
cnf(t31,plain,
( ~ neq(sK51,nil)
| app(sK53,cons(sK52,nil)) = sK51 ),
inference(extension,[status(thm),parent(t29:2)],[f_96_28]) ).
cnf(t32,plain,
$false,
inference(connection,[status(thm),parent(t31:1)],[t31:1,t29:2]) ).
cnf(t33,plain,
neq(sK51,nil),
inference(lemma_extension,[status(thm),parent(t31:2)],[l7:1]) ).
cnf(t34,plain,
$false,
inference(connection,[status(thm),parent(t33:1)],[t33:1,t31:2]) ).
cnf(t35,plain,
( sK49 != sK51
| sK51 = sK49 ),
inference(extension,[status(thm),parent(t29:3)],[equality_2]) ).
cnf(t36,plain,
$false,
inference(connection,[status(thm),parent(t35:1)],[t35:1,t29:3]) ).
cnf(t37,plain,
sK49 = sK51,
inference(extension,[status(thm),parent(t35:2)],[f_96_16]) ).
cnf(t38,plain,
$false,
inference(connection,[status(thm),parent(t37:1)],[t37:1,t35:2]) ).
cnf(t39,plain,
( ~ neq(sK51,nil)
| ssList(sK53) ),
inference(extension,[status(thm),parent(t1:4)],[f_96_27]) ).
cnf(t40,plain,
$false,
inference(connection,[status(thm),parent(t39:1)],[t39:1,t1:4]) ).
cnf(t41,plain,
neq(sK51,nil),
inference(lemma_extension,[status(thm),parent(t39:2)],[l7:1]) ).
cnf(t42,plain,
$false,
inference(connection,[status(thm),parent(t41:1)],[t41:1,t39:2]) ).
cnf(t43,plain,
( sK50 != sK48
| cons(sK52,nil) != sK50
| cons(sK52,nil) = sK48 ),
inference(extension,[status(thm),parent(t1:5)],[equality_3]) ).
cnf(t44,plain,
$false,
inference(connection,[status(thm),parent(t43:1)],[t43:1,t1:5]) ).
cnf(t45,plain,
( ~ neq(sK51,nil)
| cons(sK52,nil) = sK50 ),
inference(extension,[status(thm),parent(t43:2)],[f_96_26]) ).
cnf(t46,plain,
$false,
inference(connection,[status(thm),parent(t45:1)],[t45:1,t43:2]) ).
cnf(t47,plain,
neq(sK51,nil),
inference(lemma_extension,[status(thm),parent(t45:2)],[l7:1]) ).
cnf(t48,plain,
$false,
inference(connection,[status(thm),parent(t47:1)],[t47:1,t45:2]) ).
cnf(t49,plain,
( sK48 != sK50
| sK50 = sK48 ),
inference(extension,[status(thm),parent(t43:3)],[equality_2]) ).
cnf(t50,plain,
$false,
inference(connection,[status(thm),parent(t49:1)],[t49:1,t43:3]) ).
cnf(t51,plain,
sK48 = sK50,
inference(extension,[status(thm),parent(t49:2)],[f_96_14]) ).
cnf(t52,plain,
$false,
inference(connection,[status(thm),parent(t51:1)],[t51:1,t49:2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC096+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.04 % 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.58 % Computer : n014.cluster.edu
% 0.10/0.58 % Model : x86_64 x86_64
% 0.10/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.58 % Memory : 8046.5625MB
% 0.10/0.58 % OS : Linux 6.8.0-71-generic
% 0.10/0.58 % CPULimit : 300
% 0.10/0.58 % WCLimit : 300
% 0.10/0.58 % DateTime : Sun Sep 20 01:46:36 UTC 2026
% 0.10/0.58 % CPUTime :
% 84.24/84.78 % SZS status Theorem for theBenchmark
% 84.24/84.78 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------