%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SWC422+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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:02:19 AM UTC 2026
% Result : Theorem 79.34s 79.60s
% Output : Proof 79.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 7
% Syntax : Number of formulae : 92 ( 52 unt; 0 def)
% Number of atoms : 351 ( 114 equ)
% Maximal formula atoms : 19 ( 3 avg)
% Number of connectives : 382 ( 123 ~; 114 |; 127 &)
% ( 0 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 107 ( 0 sgn 50 !; 41 ?)
% 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] :
( ssList(X)
=> ( ( ( neq(X,nil)
| ~ neq(V,nil) )
& ( ! [X2] :
( ssItem(X2)
=> ! [X3] :
( ssList(X3)
=> ! [X4] :
( ssList(X4)
=> ( app(app(X4,cons(X2,nil)),X3) != W
| app(app(X3,cons(X2,nil)),X4) != X ) ) ) )
| ? [Y] :
( ? [Z] :
( ? [X1] :
( app(app(X1,cons(Y,nil)),Z) = U
& app(app(Z,cons(Y,nil)),X1) = V
& ssList(X1) )
& ssList(Z) )
& ssItem(Y) )
| ~ neq(V,nil) ) )
| U != W
| V != 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] :
( ssList(X)
=> ( ( ( neq(X,nil)
| ~ neq(V,nil) )
& ( ! [X2] :
( ssItem(X2)
=> ! [X3] :
( ssList(X3)
=> ! [X4] :
( ssList(X4)
=> ( app(app(X4,cons(X2,nil)),X3) != W
| app(app(X3,cons(X2,nil)),X4) != X ) ) ) )
| ? [Y] :
( ? [Z] :
( ? [X1] :
( app(app(X1,cons(Y,nil)),Z) = U
& app(app(Z,cons(Y,nil)),X1) = V
& ssList(X1) )
& ssList(Z) )
& ssItem(Y) )
| ~ neq(V,nil) ) )
| U != W
| V != X ) ) ) ) ),
inference(negate,[status(cth)],[co1]) ).
fof(f_96_2,negated_conjecture,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ( ( ~ neq(X,nil)
& neq(V,nil) )
| ( ? [X2] :
( ? [X3] :
( ? [X4] :
( app(app(X4,cons(X2,nil)),X3) = W
& app(app(X3,cons(X2,nil)),X4) = X
& ssList(X4) )
& ssList(X3) )
& ssItem(X2) )
& ! [Y] :
( ! [Z] :
( ! [X1] :
( app(app(X1,cons(Y,nil)),Z) != U
| app(app(Z,cons(Y,nil)),X1) != V
| ~ ssList(X1) )
| ~ 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_253] :
( ? [U_252] :
( ? [U_251] :
( ? [U_250] :
( ( ( ~ neq(U_250,nil)
& neq(U_252,nil) )
| ( ? [U_249] :
( ? [U_248] :
( ? [U_247] :
( app(app(U_247,cons(U_249,nil)),U_248) = U_251
& app(app(U_248,cons(U_249,nil)),U_247) = U_250
& ssList(U_247) )
& ssList(U_248) )
& ssItem(U_249) )
& ! [U_246] :
( ! [U_245] :
( ! [U_244] :
( app(app(U_244,cons(U_246,nil)),U_245) != U_253
| app(app(U_245,cons(U_246,nil)),U_244) != U_252
| ~ ssList(U_244) )
| ~ ssList(U_245) )
| ~ ssItem(U_246) )
& neq(U_252,nil) ) )
& U_253 = U_251
& U_252 = U_250
& ssList(U_250) )
& ssList(U_251) )
& ssList(U_252) )
& ssList(U_253) ),
inference(variable_rename,[status(thm)],[f_96_2]) ).
fof(f_96_4,negated_conjecture,
( ? [U_252] :
( ? [U_251] :
( ? [U_250] :
( ( ( ~ neq(U_250,nil)
& neq(U_252,nil) )
| ( ? [U_249] :
( ? [U_248] :
( ? [U_247] :
( app(app(U_247,cons(U_249,nil)),U_248) = U_251
& app(app(U_248,cons(U_249,nil)),U_247) = U_250
& ssList(U_247) )
& ssList(U_248) )
& ssItem(U_249) )
& ! [U_246] :
( ! [U_245] :
( ! [U_244] :
( app(app(U_244,cons(U_246,nil)),U_245) != sK48
| app(app(U_245,cons(U_246,nil)),U_244) != U_252
| ~ ssList(U_244) )
| ~ ssList(U_245) )
| ~ ssItem(U_246) )
& neq(U_252,nil) ) )
& sK48 = U_251
& U_252 = U_250
& ssList(U_250) )
& ssList(U_251) )
& ssList(U_252) )
& ssList(sK48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK48]),skolemize(U_253,sK48)],[f_96_3]) ).
fof(f_96_5,negated_conjecture,
( ? [U_251] :
( ? [U_250] :
( ( ( ~ neq(U_250,nil)
& neq(sK49,nil) )
| ( ? [U_249] :
( ? [U_248] :
( ? [U_247] :
( app(app(U_247,cons(U_249,nil)),U_248) = U_251
& app(app(U_248,cons(U_249,nil)),U_247) = U_250
& ssList(U_247) )
& ssList(U_248) )
& ssItem(U_249) )
& ! [U_246] :
( ! [U_245] :
( ! [U_244] :
( app(app(U_244,cons(U_246,nil)),U_245) != sK48
| app(app(U_245,cons(U_246,nil)),U_244) != sK49
| ~ ssList(U_244) )
| ~ ssList(U_245) )
| ~ ssItem(U_246) )
& neq(sK49,nil) ) )
& sK48 = U_251
& sK49 = U_250
& ssList(U_250) )
& ssList(U_251) )
& ssList(sK49)
& ssList(sK48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK49]),skolemize(U_252,sK49)],[f_96_4]) ).
fof(f_96_6,negated_conjecture,
( ? [U_250] :
( ( ( ~ neq(U_250,nil)
& neq(sK49,nil) )
| ( ? [U_249] :
( ? [U_248] :
( ? [U_247] :
( app(app(U_247,cons(U_249,nil)),U_248) = sK50
& app(app(U_248,cons(U_249,nil)),U_247) = U_250
& ssList(U_247) )
& ssList(U_248) )
& ssItem(U_249) )
& ! [U_246] :
( ! [U_245] :
( ! [U_244] :
( app(app(U_244,cons(U_246,nil)),U_245) != sK48
| app(app(U_245,cons(U_246,nil)),U_244) != sK49
| ~ ssList(U_244) )
| ~ ssList(U_245) )
| ~ ssItem(U_246) )
& neq(sK49,nil) ) )
& sK48 = sK50
& sK49 = U_250
& ssList(U_250) )
& ssList(sK50)
& ssList(sK49)
& ssList(sK48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK50]),skolemize(U_251,sK50)],[f_96_5]) ).
fof(f_96_7,negated_conjecture,
( ( ( ~ neq(sK51,nil)
& neq(sK49,nil) )
| ( ? [U_249] :
( ? [U_248] :
( ? [U_247] :
( app(app(U_247,cons(U_249,nil)),U_248) = sK50
& app(app(U_248,cons(U_249,nil)),U_247) = sK51
& ssList(U_247) )
& ssList(U_248) )
& ssItem(U_249) )
& ! [U_246] :
( ! [U_245] :
( ! [U_244] :
( app(app(U_244,cons(U_246,nil)),U_245) != sK48
| app(app(U_245,cons(U_246,nil)),U_244) != sK49
| ~ ssList(U_244) )
| ~ ssList(U_245) )
| ~ ssItem(U_246) )
& neq(sK49,nil) ) )
& sK48 = sK50
& sK49 = sK51
& ssList(sK51)
& ssList(sK50)
& ssList(sK49)
& ssList(sK48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK51]),skolemize(U_250,sK51)],[f_96_6]) ).
fof(f_96_8,negated_conjecture,
( ( ( ~ neq(sK51,nil)
& neq(sK49,nil) )
| ( ? [U_248] :
( ? [U_247] :
( app(app(U_247,cons(sK52,nil)),U_248) = sK50
& app(app(U_248,cons(sK52,nil)),U_247) = sK51
& ssList(U_247) )
& ssList(U_248) )
& ssItem(sK52)
& ! [U_246] :
( ! [U_245] :
( ! [U_244] :
( app(app(U_244,cons(U_246,nil)),U_245) != sK48
| app(app(U_245,cons(U_246,nil)),U_244) != sK49
| ~ ssList(U_244) )
| ~ ssList(U_245) )
| ~ ssItem(U_246) )
& neq(sK49,nil) ) )
& sK48 = sK50
& sK49 = sK51
& ssList(sK51)
& ssList(sK50)
& ssList(sK49)
& ssList(sK48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK52]),skolemize(U_249,sK52)],[f_96_7]) ).
fof(f_96_9,negated_conjecture,
( ( ( ~ neq(sK51,nil)
& neq(sK49,nil) )
| ( ? [U_247] :
( app(app(U_247,cons(sK52,nil)),sK53) = sK50
& app(app(sK53,cons(sK52,nil)),U_247) = sK51
& ssList(U_247) )
& ssList(sK53)
& ssItem(sK52)
& ! [U_246] :
( ! [U_245] :
( ! [U_244] :
( app(app(U_244,cons(U_246,nil)),U_245) != sK48
| app(app(U_245,cons(U_246,nil)),U_244) != sK49
| ~ ssList(U_244) )
| ~ ssList(U_245) )
| ~ ssItem(U_246) )
& neq(sK49,nil) ) )
& sK48 = sK50
& sK49 = sK51
& ssList(sK51)
& ssList(sK50)
& ssList(sK49)
& ssList(sK48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK53]),skolemize(U_248,sK53)],[f_96_8]) ).
fof(f_96_10,negated_conjecture,
( ( ( ~ neq(sK51,nil)
& neq(sK49,nil) )
| ( app(app(sK54,cons(sK52,nil)),sK53) = sK50
& app(app(sK53,cons(sK52,nil)),sK54) = sK51
& ssList(sK54)
& ssList(sK53)
& ssItem(sK52)
& ! [U_246] :
( ! [U_245] :
( ! [U_244] :
( app(app(U_244,cons(U_246,nil)),U_245) != sK48
| app(app(U_245,cons(U_246,nil)),U_244) != sK49
| ~ ssList(U_244) )
| ~ ssList(U_245) )
| ~ ssItem(U_246) )
& neq(sK49,nil) ) )
& sK48 = sK50
& sK49 = sK51
& ssList(sK51)
& ssList(sK50)
& ssList(sK49)
& ssList(sK48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK54]),skolemize(U_247,sK54)],[f_96_9]) ).
cnf(f_96_14,negated_conjecture,
ssList(sK51),
inference(clausify,[status(thm)],[f_96_10]) ).
cnf(f_96_15,negated_conjecture,
sK49 = sK51,
inference(clausify,[status(thm)],[f_96_10]) ).
cnf(f_96_16,negated_conjecture,
sK48 = sK50,
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(app(U_244,cons(U_246,nil)),U_245) != sK48
| app(app(U_245,cons(U_246,nil)),U_244) != sK49
| ~ ssList(U_244)
| ~ ssList(U_245)
| ~ ssItem(U_246) ),
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_26,negated_conjecture,
( ssItem(sK52)
| ~ 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,
( ssList(sK54)
| ~ neq(sK51,nil) ),
inference(clausify,[status(thm)],[f_96_10]) ).
cnf(f_96_29,negated_conjecture,
( app(app(sK53,cons(sK52,nil)),sK54) = sK51
| ~ neq(sK51,nil) ),
inference(clausify,[status(thm)],[f_96_10]) ).
cnf(f_96_30,negated_conjecture,
( app(app(sK54,cons(sK52,nil)),sK53) = sK50
| ~ 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,
( ~ ssList(sK53)
| ~ ssList(sK54)
| app(app(sK53,cons(sK52,nil)),sK54) != sK49
| app(app(sK54,cons(sK52,nil)),sK53) != sK48
| ~ 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_26]) ).
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_15]) ).
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_15]) ).
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_14]) ).
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,
( sK50 != sK48
| app(app(sK54,cons(sK52,nil)),sK53) != sK50
| app(app(sK54,cons(sK52,nil)),sK53) = sK48 ),
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(app(sK54,cons(sK52,nil)),sK53) = sK50 ),
inference(extension,[status(thm),parent(t29:2)],[f_96_30]) ).
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,
( sK48 != sK50
| sK50 = sK48 ),
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,
sK48 = sK50,
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,
( sK51 != sK49
| app(app(sK53,cons(sK52,nil)),sK54) != sK51
| app(app(sK53,cons(sK52,nil)),sK54) = sK49 ),
inference(extension,[status(thm),parent(t1:4)],[equality_3]) ).
cnf(t40,plain,
$false,
inference(connection,[status(thm),parent(t39:1)],[t39:1,t1:4]) ).
cnf(t41,plain,
( ~ neq(sK51,nil)
| app(app(sK53,cons(sK52,nil)),sK54) = sK51 ),
inference(extension,[status(thm),parent(t39:2)],[f_96_29]) ).
cnf(t42,plain,
$false,
inference(connection,[status(thm),parent(t41:1)],[t41:1,t39:2]) ).
cnf(t43,plain,
neq(sK51,nil),
inference(lemma_extension,[status(thm),parent(t41:2)],[l7:1]) ).
cnf(t44,plain,
$false,
inference(connection,[status(thm),parent(t43:1)],[t43:1,t41:2]) ).
cnf(t45,plain,
( sK49 != sK51
| sK51 = sK49 ),
inference(extension,[status(thm),parent(t39:3)],[equality_2]) ).
cnf(t46,plain,
$false,
inference(connection,[status(thm),parent(t45:1)],[t45:1,t39:3]) ).
cnf(t47,plain,
sK49 = sK51,
inference(extension,[status(thm),parent(t45:2)],[f_96_15]) ).
cnf(t48,plain,
$false,
inference(connection,[status(thm),parent(t47:1)],[t47:1,t45:2]) ).
cnf(t49,plain,
( ~ neq(sK51,nil)
| ssList(sK54) ),
inference(extension,[status(thm),parent(t1:5)],[f_96_28]) ).
cnf(t50,plain,
$false,
inference(connection,[status(thm),parent(t49:1)],[t49:1,t1:5]) ).
cnf(t51,plain,
neq(sK51,nil),
inference(lemma_extension,[status(thm),parent(t49:2)],[l7:1]) ).
cnf(t52,plain,
$false,
inference(connection,[status(thm),parent(t51:1)],[t51:1,t49:2]) ).
cnf(t53,plain,
( ~ neq(sK51,nil)
| ssList(sK53) ),
inference(extension,[status(thm),parent(t1:6)],[f_96_27]) ).
cnf(t54,plain,
$false,
inference(connection,[status(thm),parent(t53:1)],[t53:1,t1:6]) ).
cnf(t55,plain,
neq(sK51,nil),
inference(lemma_extension,[status(thm),parent(t53:2)],[l7:1]) ).
cnf(t56,plain,
$false,
inference(connection,[status(thm),parent(t55:1)],[t55:1,t53:2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC422+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/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.36 % Computer : n005.cluster.edu
% 0.07/0.36 % Model : x86_64 x86_64
% 0.07/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.36 % Memory : 8046.5625MB
% 0.07/0.36 % OS : Linux 6.8.0-71-generic
% 0.07/0.36 % CPULimit : 300
% 0.07/0.36 % WCLimit : 300
% 0.07/0.36 % DateTime : Sun Sep 20 02:55:18 UTC 2026
% 0.07/0.36 % CPUTime :
% 79.34/79.60 % SZS status Theorem for theBenchmark
% 79.34/79.60 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------