%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SEU361+1 : TPTP v9.3.1. Released v3.3.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 : n013.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:59:07 AM UTC 2026
% Result : Theorem 0.22s 0.51s
% Output : Proof 0.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 6
% Syntax : Number of formulae : 69 ( 35 unt; 0 def)
% Number of atoms : 234 ( 17 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 261 ( 96 ~; 82 |; 66 &)
% ( 0 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-3 aty)
% Number of variables : 59 ( 0 sgn 42 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d11_yellow_0,axiom,
! [A] :
( rel_str(A)
=> bottom_of_relstr(A) = join_on_relstr(A,empty_set) ),
file('theBenchmark.p',d11_yellow_0) ).
fof(dt_k3_yellow_0,axiom,
! [A] :
( rel_str(A)
=> element(bottom_of_relstr(A),the_carrier(A)) ),
file('theBenchmark.p',dt_k3_yellow_0) ).
fof(t30_yellow_0,axiom,
! [A] :
( ( rel_str(A)
& antisymmetric_relstr(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( ( ( ! [D] :
( element(D,the_carrier(A))
=> ( relstr_set_smaller(A,C,D)
=> related(A,B,D) ) )
& relstr_set_smaller(A,C,B) )
=> ( ex_sup_of_relstr_set(A,C)
& B = join_on_relstr(A,C) ) )
& ( ( ex_sup_of_relstr_set(A,C)
& B = join_on_relstr(A,C) )
=> ( ! [D] :
( element(D,the_carrier(A))
=> ( relstr_set_smaller(A,C,D)
=> related(A,B,D) ) )
& relstr_set_smaller(A,C,B) ) ) ) ) ),
file('theBenchmark.p',t30_yellow_0) ).
fof(t42_yellow_0,axiom,
! [A] :
( ( rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& ~ empty_carrier(A) )
=> ( ex_inf_of_relstr_set(A,the_carrier(A))
& ex_sup_of_relstr_set(A,empty_set) ) ),
file('theBenchmark.p',t42_yellow_0) ).
fof(t44_yellow_0,conjecture,
! [A] :
( ( rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> related(A,bottom_of_relstr(A),B) ) ),
file('theBenchmark.p',t44_yellow_0) ).
fof(t6_yellow_0,axiom,
! [A] :
( rel_str(A)
=> ! [B] :
( element(B,the_carrier(A))
=> ( relstr_element_smaller(A,empty_set,B)
& relstr_set_smaller(A,empty_set,B) ) ) ),
file('theBenchmark.p',t6_yellow_0) ).
fof(f_3_1,plain,
! [A] :
( bottom_of_relstr(A) = join_on_relstr(A,empty_set)
| ~ rel_str(A) ),
inference(fof_nnf,[status(thm)],[d11_yellow_0]) ).
fof(f_3_2,plain,
! [U_3] :
( bottom_of_relstr(U_3) = join_on_relstr(U_3,empty_set)
| ~ rel_str(U_3) ),
inference(variable_rename,[status(thm)],[f_3_1]) ).
cnf(f_3_3,plain,
( bottom_of_relstr(U_3) = join_on_relstr(U_3,empty_set)
| ~ rel_str(U_3) ),
inference(clausify,[status(thm)],[f_3_2]) ).
fof(f_6_1,plain,
! [A] :
( element(bottom_of_relstr(A),the_carrier(A))
| ~ rel_str(A) ),
inference(fof_nnf,[status(thm)],[dt_k3_yellow_0]) ).
fof(f_6_2,plain,
! [U_6] :
( element(bottom_of_relstr(U_6),the_carrier(U_6))
| ~ rel_str(U_6) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
cnf(f_6_3,plain,
( element(bottom_of_relstr(U_6),the_carrier(U_6))
| ~ rel_str(U_6) ),
inference(clausify,[status(thm)],[f_6_2]) ).
fof(f_22_1,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ex_sup_of_relstr_set(A,C)
& B = join_on_relstr(A,C) )
| ? [D] :
( ~ related(A,B,D)
& relstr_set_smaller(A,C,D)
& element(D,the_carrier(A)) )
| ~ relstr_set_smaller(A,C,B) )
& ( ( ! [D] :
( related(A,B,D)
| ~ relstr_set_smaller(A,C,D)
| ~ element(D,the_carrier(A)) )
& relstr_set_smaller(A,C,B) )
| ~ ex_sup_of_relstr_set(A,C)
| B != join_on_relstr(A,C) ) )
| ~ element(B,the_carrier(A)) )
| ~ rel_str(A)
| ~ antisymmetric_relstr(A) ),
inference(fof_nnf,[status(thm)],[t30_yellow_0]) ).
fof(f_22_2,plain,
! [U_25] :
( ! [U_24] :
( ! [U_23] :
( ( ( ex_sup_of_relstr_set(U_25,U_23)
& U_24 = join_on_relstr(U_25,U_23) )
| ? [U_22] :
( ~ related(U_25,U_24,U_22)
& relstr_set_smaller(U_25,U_23,U_22)
& element(U_22,the_carrier(U_25)) )
| ~ relstr_set_smaller(U_25,U_23,U_24) )
& ( ( ! [U_21] :
( related(U_25,U_24,U_21)
| ~ relstr_set_smaller(U_25,U_23,U_21)
| ~ element(U_21,the_carrier(U_25)) )
& relstr_set_smaller(U_25,U_23,U_24) )
| ~ ex_sup_of_relstr_set(U_25,U_23)
| U_24 != join_on_relstr(U_25,U_23) ) )
| ~ element(U_24,the_carrier(U_25)) )
| ~ rel_str(U_25)
| ~ antisymmetric_relstr(U_25) ),
inference(variable_rename,[status(thm)],[f_22_1]) ).
fof(f_22_3,plain,
! [U_25] :
( ! [U_24] :
( ( ! [U_27] :
( ( ex_sup_of_relstr_set(U_25,U_27)
& U_24 = join_on_relstr(U_25,U_27) )
| ? [U_22] :
( ~ related(U_25,U_24,U_22)
& relstr_set_smaller(U_25,U_27,U_22)
& element(U_22,the_carrier(U_25)) )
| ~ relstr_set_smaller(U_25,U_27,U_24) )
& ! [U_26] :
( ( ! [U_21] :
( related(U_25,U_24,U_21)
| ~ relstr_set_smaller(U_25,U_26,U_21)
| ~ element(U_21,the_carrier(U_25)) )
& relstr_set_smaller(U_25,U_26,U_24) )
| ~ ex_sup_of_relstr_set(U_25,U_26)
| U_24 != join_on_relstr(U_25,U_26) ) )
| ~ element(U_24,the_carrier(U_25)) )
| ~ rel_str(U_25)
| ~ antisymmetric_relstr(U_25) ),
inference(miniscope,[status(thm)],[f_22_2]) ).
fof(f_22_4,plain,
! [U_25] :
( ! [U_24] :
( ( ! [U_27] :
( ( ex_sup_of_relstr_set(U_25,U_27)
& U_24 = join_on_relstr(U_25,U_27) )
| ( ~ related(U_25,U_24,sK8(U_25,U_24,U_27))
& relstr_set_smaller(U_25,U_27,sK8(U_25,U_24,U_27))
& element(sK8(U_25,U_24,U_27),the_carrier(U_25)) )
| ~ relstr_set_smaller(U_25,U_27,U_24) )
& ! [U_26] :
( ( ! [U_21] :
( related(U_25,U_24,U_21)
| ~ relstr_set_smaller(U_25,U_26,U_21)
| ~ element(U_21,the_carrier(U_25)) )
& relstr_set_smaller(U_25,U_26,U_24) )
| ~ ex_sup_of_relstr_set(U_25,U_26)
| U_24 != join_on_relstr(U_25,U_26) ) )
| ~ element(U_24,the_carrier(U_25)) )
| ~ rel_str(U_25)
| ~ antisymmetric_relstr(U_25) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_22,sK8(U_25,U_24,U_27))],[f_22_3]) ).
cnf(f_22_6,plain,
( related(U_25,U_24,U_21)
| ~ relstr_set_smaller(U_25,U_26,U_21)
| ~ element(U_21,the_carrier(U_25))
| ~ ex_sup_of_relstr_set(U_25,U_26)
| U_24 != join_on_relstr(U_25,U_26)
| ~ element(U_24,the_carrier(U_25))
| ~ rel_str(U_25)
| ~ antisymmetric_relstr(U_25) ),
inference(clausify,[status(thm)],[f_22_4]) ).
fof(f_23_1,plain,
! [A] :
( ( ex_inf_of_relstr_set(A,the_carrier(A))
& ex_sup_of_relstr_set(A,empty_set) )
| ~ rel_str(A)
| ~ lower_bounded_relstr(A)
| ~ antisymmetric_relstr(A)
| empty_carrier(A) ),
inference(fof_nnf,[status(thm)],[t42_yellow_0]) ).
fof(f_23_2,plain,
! [U_28] :
( ( ex_inf_of_relstr_set(U_28,the_carrier(U_28))
& ex_sup_of_relstr_set(U_28,empty_set) )
| ~ rel_str(U_28)
| ~ lower_bounded_relstr(U_28)
| ~ antisymmetric_relstr(U_28)
| empty_carrier(U_28) ),
inference(variable_rename,[status(thm)],[f_23_1]) ).
cnf(f_23_3,plain,
( ex_sup_of_relstr_set(U_28,empty_set)
| ~ rel_str(U_28)
| ~ lower_bounded_relstr(U_28)
| ~ antisymmetric_relstr(U_28)
| empty_carrier(U_28) ),
inference(clausify,[status(thm)],[f_23_2]) ).
fof(f_24_1,negated_conjecture,
~ ! [A] :
( ( rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> related(A,bottom_of_relstr(A),B) ) ),
inference(negate,[status(cth)],[t44_yellow_0]) ).
fof(f_24_2,negated_conjecture,
? [A] :
( ? [B] :
( ~ related(A,bottom_of_relstr(A),B)
& element(B,the_carrier(A)) )
& rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& ~ empty_carrier(A) ),
inference(fof_nnf,[status(thm)],[f_24_1]) ).
fof(f_24_3,negated_conjecture,
? [U_30] :
( ? [U_29] :
( ~ related(U_30,bottom_of_relstr(U_30),U_29)
& element(U_29,the_carrier(U_30)) )
& rel_str(U_30)
& lower_bounded_relstr(U_30)
& antisymmetric_relstr(U_30)
& ~ empty_carrier(U_30) ),
inference(variable_rename,[status(thm)],[f_24_2]) ).
fof(f_24_4,negated_conjecture,
( ? [U_29] :
( ~ related(sK9,bottom_of_relstr(sK9),U_29)
& element(U_29,the_carrier(sK9)) )
& rel_str(sK9)
& lower_bounded_relstr(sK9)
& antisymmetric_relstr(sK9)
& ~ empty_carrier(sK9) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_30,sK9)],[f_24_3]) ).
fof(f_24_5,negated_conjecture,
( ~ related(sK9,bottom_of_relstr(sK9),sK10)
& element(sK10,the_carrier(sK9))
& rel_str(sK9)
& lower_bounded_relstr(sK9)
& antisymmetric_relstr(sK9)
& ~ empty_carrier(sK9) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(U_29,sK10)],[f_24_4]) ).
fof(f_24_6,negated_conjecture,
( ~ related(sK9,bottom_of_relstr(sK9),sK10)
& element(sK10,the_carrier(sK9))
& rel_str(sK9)
& lower_bounded_relstr(sK9)
& antisymmetric_relstr(sK9)
& ~ empty_carrier(sK9) ),
inference(definitional_conversion,[status(esa)],[f_24_5]) ).
cnf(f_24_7,negated_conjecture,
~ empty_carrier(sK9),
inference(clausify,[status(thm)],[f_24_6]) ).
cnf(f_24_8,negated_conjecture,
antisymmetric_relstr(sK9),
inference(clausify,[status(thm)],[f_24_6]) ).
cnf(f_24_9,negated_conjecture,
lower_bounded_relstr(sK9),
inference(clausify,[status(thm)],[f_24_6]) ).
cnf(f_24_10,negated_conjecture,
rel_str(sK9),
inference(clausify,[status(thm)],[f_24_6]) ).
cnf(f_24_11,negated_conjecture,
element(sK10,the_carrier(sK9)),
inference(clausify,[status(thm)],[f_24_6]) ).
cnf(f_24_12,negated_conjecture,
~ related(sK9,bottom_of_relstr(sK9),sK10),
inference(clausify,[status(thm)],[f_24_6]) ).
fof(f_26_1,plain,
! [A] :
( ! [B] :
( ( relstr_element_smaller(A,empty_set,B)
& relstr_set_smaller(A,empty_set,B) )
| ~ element(B,the_carrier(A)) )
| ~ rel_str(A) ),
inference(fof_nnf,[status(thm)],[t6_yellow_0]) ).
fof(f_26_2,plain,
! [U_33] :
( ! [U_32] :
( ( relstr_element_smaller(U_33,empty_set,U_32)
& relstr_set_smaller(U_33,empty_set,U_32) )
| ~ element(U_32,the_carrier(U_33)) )
| ~ rel_str(U_33) ),
inference(variable_rename,[status(thm)],[f_26_1]) ).
cnf(f_26_3,plain,
( relstr_set_smaller(U_33,empty_set,U_32)
| ~ element(U_32,the_carrier(U_33))
| ~ rel_str(U_33) ),
inference(clausify,[status(thm)],[f_26_2]) ).
cnf(t1,plain,
~ related(sK9,bottom_of_relstr(sK9),sK10),
inference(start,[status(thm),parent(0:0)],[f_24_12]) ).
cnf(t2,plain,
( ~ rel_str(sK9)
| ~ element(bottom_of_relstr(sK9),the_carrier(sK9))
| bottom_of_relstr(sK9) != join_on_relstr(sK9,empty_set)
| ~ ex_sup_of_relstr_set(sK9,empty_set)
| ~ element(sK10,the_carrier(sK9))
| ~ relstr_set_smaller(sK9,empty_set,sK10)
| ~ antisymmetric_relstr(sK9)
| related(sK9,bottom_of_relstr(sK9),sK10) ),
inference(extension,[status(thm),parent(t1:1)],[f_22_6]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
antisymmetric_relstr(sK9),
inference(extension,[status(thm),parent(t2:2)],[f_24_8]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(l2,lemma,
antisymmetric_relstr(sK9),
inference(lemma,[status(cth),parent(t2:2),below(t1:1)],[t2:2]) ).
cnf(t6,plain,
( ~ element(sK10,the_carrier(sK9))
| ~ rel_str(sK9)
| relstr_set_smaller(sK9,empty_set,sK10) ),
inference(extension,[status(thm),parent(t2:3)],[f_26_3]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t2:3]) ).
cnf(t8,plain,
rel_str(sK9),
inference(extension,[status(thm),parent(t6:2)],[f_24_10]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t6:2]) ).
cnf(t10,plain,
element(sK10,the_carrier(sK9)),
inference(extension,[status(thm),parent(t6:3)],[f_24_11]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t6:3]) ).
cnf(t12,plain,
element(sK10,the_carrier(sK9)),
inference(extension,[status(thm),parent(t2:4)],[f_24_11]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t2:4]) ).
cnf(t14,plain,
( ~ antisymmetric_relstr(sK9)
| ~ lower_bounded_relstr(sK9)
| ~ rel_str(sK9)
| empty_carrier(sK9)
| ex_sup_of_relstr_set(sK9,empty_set) ),
inference(extension,[status(thm),parent(t2:5)],[f_23_3]) ).
cnf(t15,plain,
$false,
inference(connection,[status(thm),parent(t14:1)],[t14:1,t2:5]) ).
cnf(t16,plain,
~ empty_carrier(sK9),
inference(extension,[status(thm),parent(t14:2)],[f_24_7]) ).
cnf(t17,plain,
$false,
inference(connection,[status(thm),parent(t16:1)],[t16:1,t14:2]) ).
cnf(t18,plain,
rel_str(sK9),
inference(extension,[status(thm),parent(t14:3)],[f_24_10]) ).
cnf(t19,plain,
$false,
inference(connection,[status(thm),parent(t18:1)],[t18:1,t14:3]) ).
cnf(t20,plain,
lower_bounded_relstr(sK9),
inference(extension,[status(thm),parent(t14:4)],[f_24_9]) ).
cnf(t21,plain,
$false,
inference(connection,[status(thm),parent(t20:1)],[t20:1,t14:4]) ).
cnf(t22,plain,
antisymmetric_relstr(sK9),
inference(lemma_extension,[status(thm),parent(t14:5)],[l2:1]) ).
cnf(t23,plain,
$false,
inference(connection,[status(thm),parent(t22:1)],[t22:1,t14:5]) ).
cnf(t24,plain,
( ~ rel_str(sK9)
| bottom_of_relstr(sK9) = join_on_relstr(sK9,empty_set) ),
inference(extension,[status(thm),parent(t2:6)],[f_3_3]) ).
cnf(t25,plain,
$false,
inference(connection,[status(thm),parent(t24:1)],[t24:1,t2:6]) ).
cnf(t26,plain,
rel_str(sK9),
inference(extension,[status(thm),parent(t24:2)],[f_24_10]) ).
cnf(t27,plain,
$false,
inference(connection,[status(thm),parent(t26:1)],[t26:1,t24:2]) ).
cnf(t28,plain,
( ~ rel_str(sK9)
| element(bottom_of_relstr(sK9),the_carrier(sK9)) ),
inference(extension,[status(thm),parent(t2:7)],[f_6_3]) ).
cnf(t29,plain,
$false,
inference(connection,[status(thm),parent(t28:1)],[t28:1,t2:7]) ).
cnf(t30,plain,
rel_str(sK9),
inference(extension,[status(thm),parent(t28:2)],[f_24_10]) ).
cnf(t31,plain,
$false,
inference(connection,[status(thm),parent(t30:1)],[t30:1,t28:2]) ).
cnf(t32,plain,
rel_str(sK9),
inference(extension,[status(thm),parent(t2:8)],[f_24_10]) ).
cnf(t33,plain,
$false,
inference(connection,[status(thm),parent(t32:1)],[t32:1,t2:8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU361+1 : TPTP v9.3.1. Released v3.3.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.08/0.36 % Computer : n013.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sun Sep 20 00:02:50 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.22/0.51 % SZS status Theorem for theBenchmark
% 0.22/0.51 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------