%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SEU280+1 : TPTP v9.3.1. Released v3.3.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 : n019.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 08:58:50 AM UTC 2026
% Result : Theorem 35.96s 36.22s
% Output : Proof 35.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 8
% Syntax : Number of formulae : 108 ( 41 unt; 0 def)
% Number of atoms : 348 ( 96 equ)
% Maximal formula atoms : 26 ( 3 avg)
% Number of connectives : 389 ( 149 ~; 139 |; 96 &)
% ( 3 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 2 prp; 0-4 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% Number of variables : 152 ( 14 sgn 69 !; 39 ?)
% Comments :
%------------------------------------------------------------------------------
fof(s1_xboole_0__e6_22__wellord2,conjecture,
! [A] :
? [B] :
! [C] :
( in(C,B)
<=> ( ordinal(C)
& in(C,A) ) ),
file('theBenchmark.p',s1_xboole_0__e6_22__wellord2) ).
fof(s1_tarski__e6_22__wellord2__1,axiom,
! [A] :
( ! [B,C,D] :
( ( ordinal(D)
& B = D
& ordinal(C)
& B = C )
=> C = D )
=> ? [B] :
! [C] :
( in(C,B)
<=> ? [D] :
( ordinal(C)
& D = C
& in(D,A) ) ) ),
file('theBenchmark.p',s1_tarski__e6_22__wellord2__1) ).
fof(f_1_1,negated_conjecture,
~ ! [A] :
? [B] :
! [C] :
( in(C,B)
<=> ( ordinal(C)
& in(C,A) ) ),
inference(negate,[status(cth)],[s1_xboole_0__e6_22__wellord2]) ).
fof(f_1_2,negated_conjecture,
? [A] :
! [B] :
? [C] :
( ( ~ in(C,B)
& ordinal(C)
& in(C,A) )
| ( ( ~ ordinal(C)
| ~ in(C,A) )
& in(C,B) ) ),
inference(fof_nnf,[status(thm)],[f_1_1]) ).
fof(f_1_3,negated_conjecture,
? [U_2] :
! [U_1] :
? [U_0] :
( ( ~ in(U_0,U_1)
& ordinal(U_0)
& in(U_0,U_2) )
| ( ( ~ ordinal(U_0)
| ~ in(U_0,U_2) )
& in(U_0,U_1) ) ),
inference(variable_rename,[status(thm)],[f_1_2]) ).
fof(f_1_4,negated_conjecture,
? [U_2] :
! [U_1] :
( ? [U_4] :
( ~ in(U_4,U_1)
& ordinal(U_4)
& in(U_4,U_2) )
| ? [U_3] :
( ( ~ ordinal(U_3)
| ~ in(U_3,U_2) )
& in(U_3,U_1) ) ),
inference(miniscope,[status(thm)],[f_1_3]) ).
fof(f_1_5,negated_conjecture,
! [U_1] :
( ? [U_4] :
( ~ in(U_4,U_1)
& ordinal(U_4)
& in(U_4,sK1) )
| ? [U_3] :
( ( ~ ordinal(U_3)
| ~ in(U_3,sK1) )
& in(U_3,U_1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_2,sK1)],[f_1_4]) ).
fof(f_1_6,negated_conjecture,
! [U_1] :
( ? [U_4] :
( ~ in(U_4,U_1)
& ordinal(U_4)
& in(U_4,sK1) )
| ( ( ~ ordinal(sK2(U_1))
| ~ in(sK2(U_1),sK1) )
& in(sK2(U_1),U_1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_3,sK2(U_1))],[f_1_5]) ).
fof(f_1_7,negated_conjecture,
! [U_1] :
( ( ~ in(sK3(U_1),U_1)
& ordinal(sK3(U_1))
& in(sK3(U_1),sK1) )
| ( ( ~ ordinal(sK2(U_1))
| ~ in(sK2(U_1),sK1) )
& in(sK2(U_1),U_1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_4,sK3(U_1))],[f_1_6]) ).
fof(f_1_8,negated_conjecture,
( ! [U_1] :
( ~ in(sK3(U_1),U_1)
| ~ sP1(U_1) )
& ! [U_1] :
( ordinal(sK3(U_1))
| ~ sP1(U_1) )
& ! [U_1] :
( in(sK3(U_1),sK1)
| ~ sP1(U_1) )
& ! [U_1] :
( ~ ordinal(sK2(U_1))
| ~ in(sK2(U_1),sK1)
| ~ sP0(U_1) )
& ! [U_1] :
( in(sK2(U_1),U_1)
| ~ sP0(U_1) )
& ! [U_1] :
( sP1(U_1)
| sP0(U_1) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0,sP1])],[f_1_7]) ).
cnf(f_1_9,negated_conjecture,
( sP1(U_1)
| sP0(U_1) ),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_10,negated_conjecture,
( in(sK2(U_1),U_1)
| ~ sP0(U_1) ),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_11,negated_conjecture,
( ~ ordinal(sK2(U_1))
| ~ in(sK2(U_1),sK1)
| ~ sP0(U_1) ),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_12,negated_conjecture,
( in(sK3(U_1),sK1)
| ~ sP1(U_1) ),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_13,negated_conjecture,
( ordinal(sK3(U_1))
| ~ sP1(U_1) ),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_14,negated_conjecture,
( ~ in(sK3(U_1),U_1)
| ~ sP1(U_1) ),
inference(clausify,[status(thm)],[f_1_8]) ).
fof(f_6_1,plain,
! [A] :
( ? [B] :
! [C] :
( ( in(C,B)
| ! [D] :
( ~ ordinal(C)
| D != C
| ~ in(D,A) ) )
& ( ? [D] :
( ordinal(C)
& D = C
& in(D,A) )
| ~ in(C,B) ) )
| ? [B,C,D] :
( C != D
& ordinal(D)
& B = D
& ordinal(C)
& B = C ) ),
inference(fof_nnf,[status(thm)],[s1_tarski__e6_22__wellord2__1]) ).
fof(f_6_2,plain,
! [U_17] :
( ? [U_16] :
! [U_15] :
( ( in(U_15,U_16)
| ! [U_14] :
( ~ ordinal(U_15)
| U_14 != U_15
| ~ in(U_14,U_17) ) )
& ( ? [U_13] :
( ordinal(U_15)
& U_13 = U_15
& in(U_13,U_17) )
| ~ in(U_15,U_16) ) )
| ? [U_12,U_11,U_10] :
( U_11 != U_10
& ordinal(U_10)
& U_12 = U_10
& ordinal(U_11)
& U_12 = U_11 ) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
fof(f_6_3,plain,
( ! [U_17] :
? [U_16] :
( ! [U_19] :
( in(U_19,U_16)
| ! [U_14] :
( U_14 != U_19
| ~ in(U_14,U_17) )
| ~ ordinal(U_19) )
& ! [U_18] :
( ( ? [U_13] :
( U_13 = U_18
& in(U_13,U_17) )
& ordinal(U_18) )
| ~ in(U_18,U_16) ) )
| ? [U_12,U_11,U_10] :
( U_11 != U_10
& ordinal(U_10)
& U_12 = U_10
& ordinal(U_11)
& U_12 = U_11 ) ),
inference(miniscope,[status(thm)],[f_6_2]) ).
fof(f_6_4,plain,
( ! [U_17] :
? [U_16] :
( ! [U_19] :
( in(U_19,U_16)
| ! [U_14] :
( U_14 != U_19
| ~ in(U_14,U_17) )
| ~ ordinal(U_19) )
& ! [U_18] :
( ( ? [U_13] :
( U_13 = U_18
& in(U_13,U_17) )
& ordinal(U_18) )
| ~ in(U_18,U_16) ) )
| ? [U_11,U_10] :
( U_11 != U_10
& ordinal(U_10)
& sK5 = U_10
& ordinal(U_11)
& sK5 = U_11 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_12,sK5)],[f_6_3]) ).
fof(f_6_5,plain,
( ! [U_17] :
? [U_16] :
( ! [U_19] :
( in(U_19,U_16)
| ! [U_14] :
( U_14 != U_19
| ~ in(U_14,U_17) )
| ~ ordinal(U_19) )
& ! [U_18] :
( ( ? [U_13] :
( U_13 = U_18
& in(U_13,U_17) )
& ordinal(U_18) )
| ~ in(U_18,U_16) ) )
| ? [U_10] :
( sK6 != U_10
& ordinal(U_10)
& sK5 = U_10
& ordinal(sK6)
& sK5 = sK6 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_11,sK6)],[f_6_4]) ).
fof(f_6_6,plain,
( ! [U_17] :
? [U_16] :
( ! [U_19] :
( in(U_19,U_16)
| ! [U_14] :
( U_14 != U_19
| ~ in(U_14,U_17) )
| ~ ordinal(U_19) )
& ! [U_18] :
( ( ? [U_13] :
( U_13 = U_18
& in(U_13,U_17) )
& ordinal(U_18) )
| ~ in(U_18,U_16) ) )
| ( sK6 != sK7
& ordinal(sK7)
& sK5 = sK7
& ordinal(sK6)
& sK5 = sK6 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_10,sK7)],[f_6_5]) ).
fof(f_6_7,plain,
( ! [U_17] :
( ! [U_19] :
( in(U_19,sK8(U_17))
| ! [U_14] :
( U_14 != U_19
| ~ in(U_14,U_17) )
| ~ ordinal(U_19) )
& ! [U_18] :
( ( ? [U_13] :
( U_13 = U_18
& in(U_13,U_17) )
& ordinal(U_18) )
| ~ in(U_18,sK8(U_17)) ) )
| ( sK6 != sK7
& ordinal(sK7)
& sK5 = sK7
& ordinal(sK6)
& sK5 = sK6 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_16,sK8(U_17))],[f_6_6]) ).
fof(f_6_8,plain,
( ! [U_17] :
( ! [U_19] :
( in(U_19,sK8(U_17))
| ! [U_14] :
( U_14 != U_19
| ~ in(U_14,U_17) )
| ~ ordinal(U_19) )
& ! [U_18] :
( ( sK9(U_17,U_18) = U_18
& in(sK9(U_17,U_18),U_17)
& ordinal(U_18) )
| ~ in(U_18,sK8(U_17)) ) )
| ( sK6 != sK7
& ordinal(sK7)
& sK5 = sK7
& ordinal(sK6)
& sK5 = sK6 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_13,sK9(U_17,U_18))],[f_6_7]) ).
fof(f_6_9,plain,
( ! [U_17,U_18] :
( sK9(U_17,U_18) = U_18
| ~ sP4(U_17,U_18) )
& ! [U_17,U_18] :
( in(sK9(U_17,U_18),U_17)
| ~ sP4(U_17,U_18) )
& ! [U_17,U_18] :
( ordinal(U_18)
| ~ sP4(U_17,U_18) )
& ! [U_14,U_17,U_18,U_19] :
( in(U_19,sK8(U_17))
| U_14 != U_19
| ~ in(U_14,U_17)
| ~ ordinal(U_19)
| ~ sP5(U_14,U_17,U_18,U_19) )
& ! [U_14,U_17,U_18,U_19] :
( sP4(U_17,U_18)
| ~ in(U_18,sK8(U_17))
| ~ sP5(U_14,U_17,U_18,U_19) )
& ( sK6 != sK7
| ~ sP3 )
& ( ordinal(sK7)
| ~ sP3 )
& ( sK5 = sK7
| ~ sP3 )
& ( ordinal(sK6)
| ~ sP3 )
& ( sK5 = sK6
| ~ sP3 )
& ! [U_14,U_17,U_18,U_19] :
( sP5(U_14,U_17,U_18,U_19)
| sP3 ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP3,sP4,sP5])],[f_6_8]) ).
cnf(f_6_10,plain,
( sP5(U_14,U_17,U_18,U_19)
| sP3 ),
inference(clausify,[status(thm)],[f_6_9]) ).
cnf(f_6_11,plain,
( sK5 = sK6
| ~ sP3 ),
inference(clausify,[status(thm)],[f_6_9]) ).
cnf(f_6_13,plain,
( sK5 = sK7
| ~ sP3 ),
inference(clausify,[status(thm)],[f_6_9]) ).
cnf(f_6_15,plain,
( sK6 != sK7
| ~ sP3 ),
inference(clausify,[status(thm)],[f_6_9]) ).
cnf(f_6_16,plain,
( sP4(U_17,U_18)
| ~ in(U_18,sK8(U_17))
| ~ sP5(U_14,U_17,U_18,U_19) ),
inference(clausify,[status(thm)],[f_6_9]) ).
cnf(f_6_17,plain,
( in(U_19,sK8(U_17))
| U_14 != U_19
| ~ in(U_14,U_17)
| ~ ordinal(U_19)
| ~ sP5(U_14,U_17,U_18,U_19) ),
inference(clausify,[status(thm)],[f_6_9]) ).
cnf(f_6_18,plain,
( ordinal(U_18)
| ~ sP4(U_17,U_18) ),
inference(clausify,[status(thm)],[f_6_9]) ).
cnf(f_6_19,plain,
( in(sK9(U_17,U_18),U_17)
| ~ sP4(U_17,U_18) ),
inference(clausify,[status(thm)],[f_6_9]) ).
cnf(f_6_20,plain,
( sK9(U_17,U_18) = U_18
| ~ sP4(U_17,U_18) ),
inference(clausify,[status(thm)],[f_6_9]) ).
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_5,axiom,
( sK3(Eq_x_0) = sK3(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( sK8(Eq_x_0) = sK8(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( in(Eq_y_0,Eq_y_1)
| ~ in(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,
( sP1(sK8(sK1))
| sP0(sK8(sK1)) ),
inference(start,[status(thm),parent(0:0)],[f_1_9]) ).
cnf(t2,plain,
( in(sK2(sK8(sK1)),sK8(sK1))
| ~ sP0(sK8(sK1)) ),
inference(extension,[status(thm),parent(t1:1)],[f_1_10]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( sP4(sK1,sK2(sK8(sK1)))
| ~ sP5(U_469,sK1,sK2(sK8(sK1)),U_472)
| ~ in(sK2(sK8(sK1)),sK8(sK1)) ),
inference(extension,[status(thm),parent(t2:2)],[f_6_16]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
( sP3
| sP5(U_469,sK1,sK2(sK8(sK1)),U_472) ),
inference(extension,[status(thm),parent(t4:2)],[f_6_10]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(t8,plain,
( sK6 != sK7
| ~ sP3 ),
inference(extension,[status(thm),parent(t6:2)],[f_6_15]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t6:2]) ).
cnf(t10,plain,
( sK5 != sK7
| sK6 != sK5
| sK6 = sK7 ),
inference(extension,[status(thm),parent(t8:2)],[equality_3]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t8:2]) ).
cnf(t12,plain,
( sK5 != sK6
| sK6 = sK5 ),
inference(extension,[status(thm),parent(t10:2)],[equality_2]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t10:2]) ).
cnf(t14,plain,
( ~ sP3
| sK5 = sK6 ),
inference(extension,[status(thm),parent(t12:2)],[f_6_11]) ).
cnf(t15,plain,
$false,
inference(connection,[status(thm),parent(t14:1)],[t14:1,t12:2]) ).
cnf(t16,plain,
$false,
inference(reduction,[status(thm),parent(t14:2)],[t14:2,t6:2]) ).
cnf(t17,plain,
( ~ sP3
| sK5 = sK7 ),
inference(extension,[status(thm),parent(t10:3)],[f_6_13]) ).
cnf(t18,plain,
$false,
inference(connection,[status(thm),parent(t17:1)],[t17:1,t10:3]) ).
cnf(t19,plain,
$false,
inference(reduction,[status(thm),parent(t17:2)],[t17:2,t6:2]) ).
cnf(t20,plain,
( ordinal(sK2(sK8(sK1)))
| ~ sP4(sK1,sK2(sK8(sK1))) ),
inference(extension,[status(thm),parent(t4:3)],[f_6_18]) ).
cnf(t21,plain,
$false,
inference(connection,[status(thm),parent(t20:1)],[t20:1,t4:3]) ).
cnf(t22,plain,
( ~ in(sK2(sK8(sK1)),sK1)
| ~ sP0(sK8(sK1))
| ~ ordinal(sK2(sK8(sK1))) ),
inference(extension,[status(thm),parent(t20:2)],[f_1_11]) ).
cnf(t23,plain,
$false,
inference(connection,[status(thm),parent(t22:1)],[t22:1,t20:2]) ).
cnf(t24,plain,
$false,
inference(reduction,[status(thm),parent(t22:2)],[t22:2,t1:1]) ).
cnf(t25,plain,
( sK1 != sK1
| ~ in(sK9(sK1,sK2(sK8(sK1))),sK1)
| sK9(sK1,sK2(sK8(sK1))) != sK2(sK8(sK1))
| in(sK2(sK8(sK1)),sK1) ),
inference(extension,[status(thm),parent(t22:3)],[equality_8]) ).
cnf(t26,plain,
$false,
inference(connection,[status(thm),parent(t25:1)],[t25:1,t22:3]) ).
cnf(t27,plain,
( ~ sP4(sK1,sK2(sK8(sK1)))
| sK9(sK1,sK2(sK8(sK1))) = sK2(sK8(sK1)) ),
inference(extension,[status(thm),parent(t25:2)],[f_6_20]) ).
cnf(t28,plain,
$false,
inference(connection,[status(thm),parent(t27:1)],[t27:1,t25:2]) ).
cnf(t29,plain,
$false,
inference(reduction,[status(thm),parent(t27:2)],[t27:2,t4:3]) ).
cnf(t30,plain,
( ~ sP4(sK1,sK2(sK8(sK1)))
| in(sK9(sK1,sK2(sK8(sK1))),sK1) ),
inference(extension,[status(thm),parent(t25:3)],[f_6_19]) ).
cnf(t31,plain,
$false,
inference(connection,[status(thm),parent(t30:1)],[t30:1,t25:3]) ).
cnf(t32,plain,
$false,
inference(reduction,[status(thm),parent(t30:2)],[t30:2,t4:3]) ).
cnf(t33,plain,
( sK1 != sK1
| sK1 = sK1 ),
inference(extension,[status(thm),parent(t25:4)],[equality_2]) ).
cnf(t34,plain,
$false,
inference(connection,[status(thm),parent(t33:1)],[t33:1,t25:4]) ).
cnf(t35,plain,
sK1 = sK1,
inference(extension,[status(thm),parent(t33:2)],[equality_1]) ).
cnf(t36,plain,
$false,
inference(connection,[status(thm),parent(t35:1)],[t35:1,t33:2]) ).
cnf(t37,plain,
( ~ in(sK3(sK8(sK1)),sK8(sK1))
| ~ sP1(sK8(sK1)) ),
inference(extension,[status(thm),parent(t1:2)],[f_1_14]) ).
cnf(t38,plain,
$false,
inference(connection,[status(thm),parent(t37:1)],[t37:1,t1:2]) ).
cnf(t39,plain,
( ~ ordinal(sK3(sK8(sK1)))
| ~ in(sK3(sK8(sK1)),sK1)
| sK3(sK8(sK1)) != sK3(sK8(sK1))
| ~ sP5(sK3(sK8(sK1)),sK1,U_499,sK3(sK8(sK1)))
| in(sK3(sK8(sK1)),sK8(sK1)) ),
inference(extension,[status(thm),parent(t37:2)],[f_6_17]) ).
cnf(t40,plain,
$false,
inference(connection,[status(thm),parent(t39:1)],[t39:1,t37:2]) ).
cnf(t41,plain,
( sP3
| sP5(sK3(sK8(sK1)),sK1,U_499,sK3(sK8(sK1))) ),
inference(extension,[status(thm),parent(t39:2)],[f_6_10]) ).
cnf(t42,plain,
$false,
inference(connection,[status(thm),parent(t41:1)],[t41:1,t39:2]) ).
cnf(t43,plain,
( sK6 != sK7
| ~ sP3 ),
inference(extension,[status(thm),parent(t41:2)],[f_6_15]) ).
cnf(t44,plain,
$false,
inference(connection,[status(thm),parent(t43:1)],[t43:1,t41:2]) ).
cnf(t45,plain,
( sK5 != sK7
| sK6 != sK5
| sK6 = sK7 ),
inference(extension,[status(thm),parent(t43:2)],[equality_3]) ).
cnf(t46,plain,
$false,
inference(connection,[status(thm),parent(t45:1)],[t45:1,t43:2]) ).
cnf(t47,plain,
( sK5 != sK6
| sK6 = sK5 ),
inference(extension,[status(thm),parent(t45:2)],[equality_2]) ).
cnf(t48,plain,
$false,
inference(connection,[status(thm),parent(t47:1)],[t47:1,t45:2]) ).
cnf(t49,plain,
( ~ sP3
| sK5 = sK6 ),
inference(extension,[status(thm),parent(t47:2)],[f_6_11]) ).
cnf(t50,plain,
$false,
inference(connection,[status(thm),parent(t49:1)],[t49:1,t47:2]) ).
cnf(t51,plain,
$false,
inference(reduction,[status(thm),parent(t49:2)],[t49:2,t41:2]) ).
cnf(t52,plain,
( ~ sP3
| sK5 = sK7 ),
inference(extension,[status(thm),parent(t45:3)],[f_6_13]) ).
cnf(t53,plain,
$false,
inference(connection,[status(thm),parent(t52:1)],[t52:1,t45:3]) ).
cnf(t54,plain,
$false,
inference(reduction,[status(thm),parent(t52:2)],[t52:2,t41:2]) ).
cnf(t55,plain,
( sK8(sK1) != sK8(sK1)
| sK3(sK8(sK1)) = sK3(sK8(sK1)) ),
inference(extension,[status(thm),parent(t39:3)],[equality_5]) ).
cnf(t56,plain,
$false,
inference(connection,[status(thm),parent(t55:1)],[t55:1,t39:3]) ).
cnf(t57,plain,
( sK1 != sK1
| sK8(sK1) = sK8(sK1) ),
inference(extension,[status(thm),parent(t55:2)],[equality_6]) ).
cnf(t58,plain,
$false,
inference(connection,[status(thm),parent(t57:1)],[t57:1,t55:2]) ).
cnf(t59,plain,
( sK1 != sK1
| sK1 = sK1 ),
inference(extension,[status(thm),parent(t57:2)],[equality_2]) ).
cnf(t60,plain,
$false,
inference(connection,[status(thm),parent(t59:1)],[t59:1,t57:2]) ).
cnf(t61,plain,
sK1 = sK1,
inference(extension,[status(thm),parent(t59:2)],[equality_1]) ).
cnf(t62,plain,
$false,
inference(connection,[status(thm),parent(t61:1)],[t61:1,t59:2]) ).
cnf(t63,plain,
( ~ sP1(sK8(sK1))
| in(sK3(sK8(sK1)),sK1) ),
inference(extension,[status(thm),parent(t39:4)],[f_1_12]) ).
cnf(t64,plain,
$false,
inference(connection,[status(thm),parent(t63:1)],[t63:1,t39:4]) ).
cnf(t65,plain,
$false,
inference(reduction,[status(thm),parent(t63:2)],[t63:2,t1:2]) ).
cnf(t66,plain,
( ~ sP1(sK8(sK1))
| ordinal(sK3(sK8(sK1))) ),
inference(extension,[status(thm),parent(t39:5)],[f_1_13]) ).
cnf(t67,plain,
$false,
inference(connection,[status(thm),parent(t66:1)],[t66:1,t39:5]) ).
cnf(t68,plain,
$false,
inference(reduction,[status(thm),parent(t66:2)],[t66:2,t1:2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU280+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.03 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n019.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 19 23:45:36 UTC 2026
% 0.08/0.35 % CPUTime :
% 35.96/36.22 % SZS status Theorem for theBenchmark
% 35.96/36.22 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------