%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SEU368+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 : n010.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:08 AM UTC 2026
% Result : Theorem 31.46s 31.73s
% Output : Proof 31.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 12
% Syntax : Number of formulae : 139 ( 74 unt; 0 def)
% Number of atoms : 262 ( 95 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 218 ( 95 ~; 86 |; 31 &)
% ( 1 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-4 aty)
% Number of functors : 8 ( 8 usr; 2 con; 0-2 aty)
% Number of variables : 130 ( 6 sgn 87 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(existence_m1_relset_1,axiom,
! [A,B] :
? [C] : relation_of2(C,A,B),
file('theBenchmark.p',existence_m1_relset_1) ).
fof(free_g1_orders_2,axiom,
! [A,B] :
( relation_of2(B,A,A)
=> ! [C,D] :
( rel_str_of(A,B) = rel_str_of(C,D)
=> ( B = D
& A = C ) ) ),
file('theBenchmark.p',free_g1_orders_2) ).
fof(abstractness_v1_orders_2,axiom,
! [A] :
( rel_str(A)
=> ( strict_rel_str(A)
=> A = rel_str_of(the_carrier(A),the_InternalRel(A)) ) ),
file('theBenchmark.p',abstractness_v1_orders_2) ).
fof(redefinition_m2_relset_1,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
<=> relation_of2(C,A,B) ),
file('theBenchmark.p',redefinition_m2_relset_1) ).
fof(dt_k2_yellow_1,axiom,
! [A] :
( rel_str(incl_POSet(A))
& strict_rel_str(incl_POSet(A)) ),
file('theBenchmark.p',dt_k2_yellow_1) ).
fof(dt_u1_orders_2,axiom,
! [A] :
( rel_str(A)
=> relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A)) ),
file('theBenchmark.p',dt_u1_orders_2) ).
fof(fc5_yellow_1,axiom,
! [A] :
( antisymmetric_relstr(incl_POSet(A))
& transitive_relstr(incl_POSet(A))
& reflexive_relstr(incl_POSet(A))
& strict_rel_str(incl_POSet(A)) ),
file('theBenchmark.p',fc5_yellow_1) ).
fof(d1_yellow_1,axiom,
! [A] : incl_POSet(A) = rel_str_of(A,inclusion_order(A)),
file('theBenchmark.p',d1_yellow_1) ).
fof(t1_yellow_1,conjecture,
! [A] :
( the_InternalRel(incl_POSet(A)) = inclusion_order(A)
& the_carrier(incl_POSet(A)) = A ),
file('theBenchmark.p',t1_yellow_1) ).
fof(f_23_1,plain,
! [A,B] :
? [C] : relation_of2(C,A,B),
inference(fof_nnf,[status(thm)],[existence_m1_relset_1]) ).
fof(f_23_2,plain,
! [U_37,U_36] :
? [U_35] : relation_of2(U_35,U_37,U_36),
inference(variable_rename,[status(thm)],[f_23_1]) ).
fof(f_23_3,plain,
! [U_37,U_36] : relation_of2(sK8(U_37,U_36),U_37,U_36),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_35,sK8(U_37,U_36))],[f_23_2]) ).
fof(f_23_4,plain,
! [U_36,U_37] : relation_of2(sK8(U_37,U_36),U_37,U_36),
inference(definitional_conversion,[status(esa)],[f_23_3]) ).
cnf(f_23_5,plain,
relation_of2(sK8(U_37,U_36),U_37,U_36),
inference(clausify,[status(thm)],[f_23_4]) ).
fof(f_33_1,plain,
! [A,B] :
( ! [C,D] :
( ( B = D
& A = C )
| rel_str_of(A,B) != rel_str_of(C,D) )
| ~ relation_of2(B,A,A) ),
inference(fof_nnf,[status(thm)],[free_g1_orders_2]) ).
fof(f_33_2,plain,
! [U_55,U_54] :
( ! [U_53,U_52] :
( ( U_54 = U_52
& U_55 = U_53 )
| rel_str_of(U_55,U_54) != rel_str_of(U_53,U_52) )
| ~ relation_of2(U_54,U_55,U_55) ),
inference(variable_rename,[status(thm)],[f_33_1]) ).
fof(f_33_3,plain,
( ! [U_55,U_52,U_54,U_53] :
( U_54 = U_52
| ~ sP5(U_55,U_52,U_54,U_53) )
& ! [U_55,U_52,U_54,U_53] :
( U_55 = U_53
| ~ sP5(U_55,U_52,U_54,U_53) )
& ! [U_55,U_52,U_54,U_53] :
( sP5(U_55,U_52,U_54,U_53)
| rel_str_of(U_55,U_54) != rel_str_of(U_53,U_52)
| ~ relation_of2(U_54,U_55,U_55) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP5])],[f_33_2]) ).
cnf(f_33_4,plain,
( sP5(U_55,U_52,U_54,U_53)
| rel_str_of(U_55,U_54) != rel_str_of(U_53,U_52)
| ~ relation_of2(U_54,U_55,U_55) ),
inference(clausify,[status(thm)],[f_33_3]) ).
cnf(f_33_5,plain,
( U_55 = U_53
| ~ sP5(U_55,U_52,U_54,U_53) ),
inference(clausify,[status(thm)],[f_33_3]) ).
cnf(f_33_6,plain,
( U_54 = U_52
| ~ sP5(U_55,U_52,U_54,U_53) ),
inference(clausify,[status(thm)],[f_33_3]) ).
fof(f_34_1,plain,
! [A] :
( A = rel_str_of(the_carrier(A),the_InternalRel(A))
| ~ strict_rel_str(A)
| ~ rel_str(A) ),
inference(fof_nnf,[status(thm)],[abstractness_v1_orders_2]) ).
fof(f_34_2,plain,
! [U_56] :
( U_56 = rel_str_of(the_carrier(U_56),the_InternalRel(U_56))
| ~ strict_rel_str(U_56)
| ~ rel_str(U_56) ),
inference(variable_rename,[status(thm)],[f_34_1]) ).
fof(f_34_3,plain,
! [U_56] :
( U_56 = rel_str_of(the_carrier(U_56),the_InternalRel(U_56))
| ~ strict_rel_str(U_56)
| ~ rel_str(U_56) ),
inference(definitional_conversion,[status(esa)],[f_34_2]) ).
cnf(f_34_4,plain,
( U_56 = rel_str_of(the_carrier(U_56),the_InternalRel(U_56))
| ~ strict_rel_str(U_56)
| ~ rel_str(U_56) ),
inference(clausify,[status(thm)],[f_34_3]) ).
fof(f_38_1,plain,
! [A,B,C] :
( ( relation_of2_as_subset(C,A,B)
| ~ relation_of2(C,A,B) )
& ( relation_of2(C,A,B)
| ~ relation_of2_as_subset(C,A,B) ) ),
inference(fof_nnf,[status(thm)],[redefinition_m2_relset_1]) ).
fof(f_38_2,plain,
! [U_64,U_63,U_62] :
( ( relation_of2_as_subset(U_62,U_64,U_63)
| ~ relation_of2(U_62,U_64,U_63) )
& ( relation_of2(U_62,U_64,U_63)
| ~ relation_of2_as_subset(U_62,U_64,U_63) ) ),
inference(variable_rename,[status(thm)],[f_38_1]) ).
fof(f_38_3,plain,
( ! [U_70,U_68,U_66] :
( relation_of2_as_subset(U_66,U_70,U_68)
| ~ relation_of2(U_66,U_70,U_68) )
& ! [U_69,U_67,U_65] :
( relation_of2(U_65,U_69,U_67)
| ~ relation_of2_as_subset(U_65,U_69,U_67) ) ),
inference(miniscope,[status(thm)],[f_38_2]) ).
fof(f_38_4,plain,
( ! [U_68,U_66,U_70] :
( relation_of2_as_subset(U_66,U_70,U_68)
| ~ relation_of2(U_66,U_70,U_68) )
& ! [U_69,U_67,U_65] :
( relation_of2(U_65,U_69,U_67)
| ~ relation_of2_as_subset(U_65,U_69,U_67) ) ),
inference(definitional_conversion,[status(esa)],[f_38_3]) ).
cnf(f_38_5,plain,
( relation_of2(U_65,U_69,U_67)
| ~ relation_of2_as_subset(U_65,U_69,U_67) ),
inference(clausify,[status(thm)],[f_38_4]) ).
fof(f_48_1,plain,
! [A] :
( rel_str(incl_POSet(A))
& strict_rel_str(incl_POSet(A)) ),
inference(fof_nnf,[status(thm)],[dt_k2_yellow_1]) ).
fof(f_48_2,plain,
! [U_87] :
( rel_str(incl_POSet(U_87))
& strict_rel_str(incl_POSet(U_87)) ),
inference(variable_rename,[status(thm)],[f_48_1]) ).
fof(f_48_3,plain,
( ! [U_89] : rel_str(incl_POSet(U_89))
& ! [U_88] : strict_rel_str(incl_POSet(U_88)) ),
inference(miniscope,[status(thm)],[f_48_2]) ).
fof(f_48_4,plain,
( ! [U_89] : rel_str(incl_POSet(U_89))
& ! [U_88] : strict_rel_str(incl_POSet(U_88)) ),
inference(definitional_conversion,[status(esa)],[f_48_3]) ).
cnf(f_48_6,plain,
rel_str(incl_POSet(U_89)),
inference(clausify,[status(thm)],[f_48_4]) ).
fof(f_49_1,plain,
! [A] :
( relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A))
| ~ rel_str(A) ),
inference(fof_nnf,[status(thm)],[dt_u1_orders_2]) ).
fof(f_49_2,plain,
! [U_90] :
( relation_of2_as_subset(the_InternalRel(U_90),the_carrier(U_90),the_carrier(U_90))
| ~ rel_str(U_90) ),
inference(variable_rename,[status(thm)],[f_49_1]) ).
fof(f_49_3,plain,
! [U_90] :
( relation_of2_as_subset(the_InternalRel(U_90),the_carrier(U_90),the_carrier(U_90))
| ~ rel_str(U_90) ),
inference(definitional_conversion,[status(esa)],[f_49_2]) ).
cnf(f_49_4,plain,
( relation_of2_as_subset(the_InternalRel(U_90),the_carrier(U_90),the_carrier(U_90))
| ~ rel_str(U_90) ),
inference(clausify,[status(thm)],[f_49_3]) ).
fof(f_51_1,plain,
! [A] :
( antisymmetric_relstr(incl_POSet(A))
& transitive_relstr(incl_POSet(A))
& reflexive_relstr(incl_POSet(A))
& strict_rel_str(incl_POSet(A)) ),
inference(fof_nnf,[status(thm)],[fc5_yellow_1]) ).
fof(f_51_2,plain,
! [U_91] :
( antisymmetric_relstr(incl_POSet(U_91))
& transitive_relstr(incl_POSet(U_91))
& reflexive_relstr(incl_POSet(U_91))
& strict_rel_str(incl_POSet(U_91)) ),
inference(variable_rename,[status(thm)],[f_51_1]) ).
fof(f_51_3,plain,
( ! [U_95] : antisymmetric_relstr(incl_POSet(U_95))
& ! [U_94] : transitive_relstr(incl_POSet(U_94))
& ! [U_93] : reflexive_relstr(incl_POSet(U_93))
& ! [U_92] : strict_rel_str(incl_POSet(U_92)) ),
inference(miniscope,[status(thm)],[f_51_2]) ).
fof(f_51_4,plain,
( ! [U_95] : antisymmetric_relstr(incl_POSet(U_95))
& ! [U_94] : transitive_relstr(incl_POSet(U_94))
& ! [U_93] : reflexive_relstr(incl_POSet(U_93))
& ! [U_92] : strict_rel_str(incl_POSet(U_92)) ),
inference(definitional_conversion,[status(esa)],[f_51_3]) ).
cnf(f_51_5,plain,
strict_rel_str(incl_POSet(U_92)),
inference(clausify,[status(thm)],[f_51_4]) ).
fof(f_52_1,plain,
! [A] : incl_POSet(A) = rel_str_of(A,inclusion_order(A)),
inference(fof_nnf,[status(thm)],[d1_yellow_1]) ).
fof(f_52_2,plain,
! [U_96] : incl_POSet(U_96) = rel_str_of(U_96,inclusion_order(U_96)),
inference(variable_rename,[status(thm)],[f_52_1]) ).
fof(f_52_3,plain,
! [U_96] : incl_POSet(U_96) = rel_str_of(U_96,inclusion_order(U_96)),
inference(definitional_conversion,[status(esa)],[f_52_2]) ).
cnf(f_52_4,plain,
incl_POSet(U_96) = rel_str_of(U_96,inclusion_order(U_96)),
inference(clausify,[status(thm)],[f_52_3]) ).
fof(f_53_1,negated_conjecture,
~ ! [A] :
( the_InternalRel(incl_POSet(A)) = inclusion_order(A)
& the_carrier(incl_POSet(A)) = A ),
inference(negate,[status(cth)],[t1_yellow_1]) ).
fof(f_53_2,negated_conjecture,
? [A] :
( the_InternalRel(incl_POSet(A)) != inclusion_order(A)
| the_carrier(incl_POSet(A)) != A ),
inference(fof_nnf,[status(thm)],[f_53_1]) ).
fof(f_53_3,negated_conjecture,
? [U_97] :
( the_InternalRel(incl_POSet(U_97)) != inclusion_order(U_97)
| the_carrier(incl_POSet(U_97)) != U_97 ),
inference(variable_rename,[status(thm)],[f_53_2]) ).
fof(f_53_4,negated_conjecture,
( ? [U_99] : the_InternalRel(incl_POSet(U_99)) != inclusion_order(U_99)
| ? [U_98] : the_carrier(incl_POSet(U_98)) != U_98 ),
inference(miniscope,[status(thm)],[f_53_3]) ).
fof(f_53_5,negated_conjecture,
( ? [U_99] : the_InternalRel(incl_POSet(U_99)) != inclusion_order(U_99)
| the_carrier(incl_POSet(sK14)) != sK14 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(U_98,sK14)],[f_53_4]) ).
fof(f_53_6,negated_conjecture,
( the_InternalRel(incl_POSet(sK15)) != inclusion_order(sK15)
| the_carrier(incl_POSet(sK14)) != sK14 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(U_99,sK15)],[f_53_5]) ).
fof(f_53_7,negated_conjecture,
( the_InternalRel(incl_POSet(sK15)) != inclusion_order(sK15)
| the_carrier(incl_POSet(sK14)) != sK14 ),
inference(definitional_conversion,[status(esa)],[f_53_6]) ).
cnf(f_53_8,negated_conjecture,
( the_InternalRel(incl_POSet(sK15)) != inclusion_order(sK15)
| the_carrier(incl_POSet(sK14)) != sK14 ),
inference(clausify,[status(thm)],[f_53_7]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_15,axiom,
( sK8(Eq_x_0,Eq_x_1) = sK8(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_41,axiom,
( sP5(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ sP5(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(t1,plain,
( the_InternalRel(incl_POSet(sK15)) != inclusion_order(sK15)
| the_carrier(incl_POSet(sK14)) != sK14 ),
inference(start,[status(thm),parent(0:0)],[f_53_8]) ).
cnf(t2,plain,
( ~ sP5(the_carrier(incl_POSet(sK14)),inclusion_order(sK14),the_InternalRel(incl_POSet(sK14)),sK14)
| the_carrier(incl_POSet(sK14)) = sK14 ),
inference(extension,[status(thm),parent(t1:1)],[f_33_5]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( rel_str_of(the_carrier(incl_POSet(sK14)),the_InternalRel(incl_POSet(sK14))) != rel_str_of(sK14,inclusion_order(sK14))
| ~ relation_of2(the_InternalRel(incl_POSet(sK14)),the_carrier(incl_POSet(sK14)),the_carrier(incl_POSet(sK14)))
| sP5(the_carrier(incl_POSet(sK14)),inclusion_order(sK14),the_InternalRel(incl_POSet(sK14)),sK14) ),
inference(extension,[status(thm),parent(t2:2)],[f_33_4]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
( ~ relation_of2_as_subset(the_InternalRel(incl_POSet(sK14)),the_carrier(incl_POSet(sK14)),the_carrier(incl_POSet(sK14)))
| relation_of2(the_InternalRel(incl_POSet(sK14)),the_carrier(incl_POSet(sK14)),the_carrier(incl_POSet(sK14))) ),
inference(extension,[status(thm),parent(t4:2)],[f_38_5]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(t8,plain,
( ~ rel_str(incl_POSet(sK14))
| relation_of2_as_subset(the_InternalRel(incl_POSet(sK14)),the_carrier(incl_POSet(sK14)),the_carrier(incl_POSet(sK14))) ),
inference(extension,[status(thm),parent(t6:2)],[f_49_4]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t6:2]) ).
cnf(t10,plain,
rel_str(incl_POSet(sK14)),
inference(extension,[status(thm),parent(t8:2)],[f_48_6]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t8:2]) ).
cnf(t12,plain,
( ~ sP5(rel_str_of(the_carrier(incl_POSet(sK14)),the_InternalRel(incl_POSet(sK14))),sK8(rel_str_of(sK14,inclusion_order(sK14)),rel_str_of(sK14,inclusion_order(sK14))),sK8(rel_str_of(sK14,inclusion_order(sK14)),rel_str_of(sK14,inclusion_order(sK14))),rel_str_of(sK14,inclusion_order(sK14)))
| rel_str_of(the_carrier(incl_POSet(sK14)),the_InternalRel(incl_POSet(sK14))) = rel_str_of(sK14,inclusion_order(sK14)) ),
inference(extension,[status(thm),parent(t4:3)],[f_33_5]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t4:3]) ).
cnf(t14,plain,
( sK8(incl_POSet(sK14),incl_POSet(sK14)) != sK8(rel_str_of(sK14,inclusion_order(sK14)),rel_str_of(sK14,inclusion_order(sK14)))
| sK8(incl_POSet(sK14),incl_POSet(sK14)) != sK8(rel_str_of(sK14,inclusion_order(sK14)),rel_str_of(sK14,inclusion_order(sK14)))
| incl_POSet(sK14) != rel_str_of(sK14,inclusion_order(sK14))
| ~ sP5(incl_POSet(sK14),sK8(incl_POSet(sK14),incl_POSet(sK14)),sK8(incl_POSet(sK14),incl_POSet(sK14)),incl_POSet(sK14))
| incl_POSet(sK14) != rel_str_of(the_carrier(incl_POSet(sK14)),the_InternalRel(incl_POSet(sK14)))
| sP5(rel_str_of(the_carrier(incl_POSet(sK14)),the_InternalRel(incl_POSet(sK14))),sK8(rel_str_of(sK14,inclusion_order(sK14)),rel_str_of(sK14,inclusion_order(sK14))),sK8(rel_str_of(sK14,inclusion_order(sK14)),rel_str_of(sK14,inclusion_order(sK14))),rel_str_of(sK14,inclusion_order(sK14))) ),
inference(extension,[status(thm),parent(t12:2)],[equality_41]) ).
cnf(t15,plain,
$false,
inference(connection,[status(thm),parent(t14:1)],[t14:1,t12:2]) ).
cnf(t16,plain,
( ~ strict_rel_str(incl_POSet(sK14))
| ~ rel_str(incl_POSet(sK14))
| incl_POSet(sK14) = rel_str_of(the_carrier(incl_POSet(sK14)),the_InternalRel(incl_POSet(sK14))) ),
inference(extension,[status(thm),parent(t14:2)],[f_34_4]) ).
cnf(t17,plain,
$false,
inference(connection,[status(thm),parent(t16:1)],[t16:1,t14:2]) ).
cnf(t18,plain,
rel_str(incl_POSet(sK14)),
inference(extension,[status(thm),parent(t16:2)],[f_48_6]) ).
cnf(t19,plain,
$false,
inference(connection,[status(thm),parent(t18:1)],[t18:1,t16:2]) ).
cnf(t20,plain,
strict_rel_str(incl_POSet(sK14)),
inference(extension,[status(thm),parent(t16:3)],[f_51_5]) ).
cnf(t21,plain,
$false,
inference(connection,[status(thm),parent(t20:1)],[t20:1,t16:3]) ).
cnf(t22,plain,
( rel_str_of(incl_POSet(sK14),sK8(incl_POSet(sK14),incl_POSet(sK14))) != rel_str_of(incl_POSet(sK14),sK8(incl_POSet(sK14),incl_POSet(sK14)))
| ~ relation_of2(sK8(incl_POSet(sK14),incl_POSet(sK14)),incl_POSet(sK14),incl_POSet(sK14))
| sP5(incl_POSet(sK14),sK8(incl_POSet(sK14),incl_POSet(sK14)),sK8(incl_POSet(sK14),incl_POSet(sK14)),incl_POSet(sK14)) ),
inference(extension,[status(thm),parent(t14:3)],[f_33_4]) ).
cnf(t23,plain,
$false,
inference(connection,[status(thm),parent(t22:1)],[t22:1,t14:3]) ).
cnf(t24,plain,
relation_of2(sK8(incl_POSet(sK14),incl_POSet(sK14)),incl_POSet(sK14),incl_POSet(sK14)),
inference(extension,[status(thm),parent(t22:2)],[f_23_5]) ).
cnf(t25,plain,
$false,
inference(connection,[status(thm),parent(t24:1)],[t24:1,t22:2]) ).
cnf(t26,plain,
rel_str_of(incl_POSet(sK14),sK8(incl_POSet(sK14),incl_POSet(sK14))) = rel_str_of(incl_POSet(sK14),sK8(incl_POSet(sK14),incl_POSet(sK14))),
inference(extension,[status(thm),parent(t22:3)],[equality_1]) ).
cnf(t27,plain,
$false,
inference(connection,[status(thm),parent(t26:1)],[t26:1,t22:3]) ).
cnf(t28,plain,
incl_POSet(sK14) = rel_str_of(sK14,inclusion_order(sK14)),
inference(extension,[status(thm),parent(t14:4)],[f_52_4]) ).
cnf(t29,plain,
$false,
inference(connection,[status(thm),parent(t28:1)],[t28:1,t14:4]) ).
cnf(t30,plain,
( incl_POSet(sK14) != rel_str_of(sK14,inclusion_order(sK14))
| incl_POSet(sK14) != rel_str_of(sK14,inclusion_order(sK14))
| sK8(incl_POSet(sK14),incl_POSet(sK14)) = sK8(rel_str_of(sK14,inclusion_order(sK14)),rel_str_of(sK14,inclusion_order(sK14))) ),
inference(extension,[status(thm),parent(t14:5)],[equality_15]) ).
cnf(t31,plain,
$false,
inference(connection,[status(thm),parent(t30:1)],[t30:1,t14:5]) ).
cnf(t32,plain,
incl_POSet(sK14) = rel_str_of(sK14,inclusion_order(sK14)),
inference(extension,[status(thm),parent(t30:2)],[f_52_4]) ).
cnf(t33,plain,
$false,
inference(connection,[status(thm),parent(t32:1)],[t32:1,t30:2]) ).
cnf(t34,plain,
incl_POSet(sK14) = rel_str_of(sK14,inclusion_order(sK14)),
inference(extension,[status(thm),parent(t30:3)],[f_52_4]) ).
cnf(t35,plain,
$false,
inference(connection,[status(thm),parent(t34:1)],[t34:1,t30:3]) ).
cnf(t36,plain,
( incl_POSet(sK14) != rel_str_of(sK14,inclusion_order(sK14))
| incl_POSet(sK14) != rel_str_of(sK14,inclusion_order(sK14))
| sK8(incl_POSet(sK14),incl_POSet(sK14)) = sK8(rel_str_of(sK14,inclusion_order(sK14)),rel_str_of(sK14,inclusion_order(sK14))) ),
inference(extension,[status(thm),parent(t14:6)],[equality_15]) ).
cnf(t37,plain,
$false,
inference(connection,[status(thm),parent(t36:1)],[t36:1,t14:6]) ).
cnf(t38,plain,
incl_POSet(sK14) = rel_str_of(sK14,inclusion_order(sK14)),
inference(extension,[status(thm),parent(t36:2)],[f_52_4]) ).
cnf(t39,plain,
$false,
inference(connection,[status(thm),parent(t38:1)],[t38:1,t36:2]) ).
cnf(t40,plain,
incl_POSet(sK14) = rel_str_of(sK14,inclusion_order(sK14)),
inference(extension,[status(thm),parent(t36:3)],[f_52_4]) ).
cnf(t41,plain,
$false,
inference(connection,[status(thm),parent(t40:1)],[t40:1,t36:3]) ).
cnf(t42,plain,
( ~ sP5(the_carrier(incl_POSet(sK15)),inclusion_order(sK15),the_InternalRel(incl_POSet(sK15)),sK15)
| the_InternalRel(incl_POSet(sK15)) = inclusion_order(sK15) ),
inference(extension,[status(thm),parent(t1:2)],[f_33_6]) ).
cnf(t43,plain,
$false,
inference(connection,[status(thm),parent(t42:1)],[t42:1,t1:2]) ).
cnf(t44,plain,
( rel_str_of(the_carrier(incl_POSet(sK15)),the_InternalRel(incl_POSet(sK15))) != rel_str_of(sK15,inclusion_order(sK15))
| ~ relation_of2(the_InternalRel(incl_POSet(sK15)),the_carrier(incl_POSet(sK15)),the_carrier(incl_POSet(sK15)))
| sP5(the_carrier(incl_POSet(sK15)),inclusion_order(sK15),the_InternalRel(incl_POSet(sK15)),sK15) ),
inference(extension,[status(thm),parent(t42:2)],[f_33_4]) ).
cnf(t45,plain,
$false,
inference(connection,[status(thm),parent(t44:1)],[t44:1,t42:2]) ).
cnf(t46,plain,
( ~ relation_of2_as_subset(the_InternalRel(incl_POSet(sK15)),the_carrier(incl_POSet(sK15)),the_carrier(incl_POSet(sK15)))
| relation_of2(the_InternalRel(incl_POSet(sK15)),the_carrier(incl_POSet(sK15)),the_carrier(incl_POSet(sK15))) ),
inference(extension,[status(thm),parent(t44:2)],[f_38_5]) ).
cnf(t47,plain,
$false,
inference(connection,[status(thm),parent(t46:1)],[t46:1,t44:2]) ).
cnf(t48,plain,
( ~ rel_str(incl_POSet(sK15))
| relation_of2_as_subset(the_InternalRel(incl_POSet(sK15)),the_carrier(incl_POSet(sK15)),the_carrier(incl_POSet(sK15))) ),
inference(extension,[status(thm),parent(t46:2)],[f_49_4]) ).
cnf(t49,plain,
$false,
inference(connection,[status(thm),parent(t48:1)],[t48:1,t46:2]) ).
cnf(t50,plain,
rel_str(incl_POSet(sK15)),
inference(extension,[status(thm),parent(t48:2)],[f_48_6]) ).
cnf(t51,plain,
$false,
inference(connection,[status(thm),parent(t50:1)],[t50:1,t48:2]) ).
cnf(t52,plain,
( ~ sP5(rel_str_of(the_carrier(incl_POSet(sK15)),the_InternalRel(incl_POSet(sK15))),sK8(rel_str_of(sK15,inclusion_order(sK15)),rel_str_of(sK15,inclusion_order(sK15))),sK8(rel_str_of(sK15,inclusion_order(sK15)),rel_str_of(sK15,inclusion_order(sK15))),rel_str_of(sK15,inclusion_order(sK15)))
| rel_str_of(the_carrier(incl_POSet(sK15)),the_InternalRel(incl_POSet(sK15))) = rel_str_of(sK15,inclusion_order(sK15)) ),
inference(extension,[status(thm),parent(t44:3)],[f_33_5]) ).
cnf(t53,plain,
$false,
inference(connection,[status(thm),parent(t52:1)],[t52:1,t44:3]) ).
cnf(t54,plain,
( sK8(incl_POSet(sK15),incl_POSet(sK15)) != sK8(rel_str_of(sK15,inclusion_order(sK15)),rel_str_of(sK15,inclusion_order(sK15)))
| sK8(incl_POSet(sK15),incl_POSet(sK15)) != sK8(rel_str_of(sK15,inclusion_order(sK15)),rel_str_of(sK15,inclusion_order(sK15)))
| incl_POSet(sK15) != rel_str_of(sK15,inclusion_order(sK15))
| ~ sP5(incl_POSet(sK15),sK8(incl_POSet(sK15),incl_POSet(sK15)),sK8(incl_POSet(sK15),incl_POSet(sK15)),incl_POSet(sK15))
| incl_POSet(sK15) != rel_str_of(the_carrier(incl_POSet(sK15)),the_InternalRel(incl_POSet(sK15)))
| sP5(rel_str_of(the_carrier(incl_POSet(sK15)),the_InternalRel(incl_POSet(sK15))),sK8(rel_str_of(sK15,inclusion_order(sK15)),rel_str_of(sK15,inclusion_order(sK15))),sK8(rel_str_of(sK15,inclusion_order(sK15)),rel_str_of(sK15,inclusion_order(sK15))),rel_str_of(sK15,inclusion_order(sK15))) ),
inference(extension,[status(thm),parent(t52:2)],[equality_41]) ).
cnf(t55,plain,
$false,
inference(connection,[status(thm),parent(t54:1)],[t54:1,t52:2]) ).
cnf(t56,plain,
( ~ strict_rel_str(incl_POSet(sK15))
| ~ rel_str(incl_POSet(sK15))
| incl_POSet(sK15) = rel_str_of(the_carrier(incl_POSet(sK15)),the_InternalRel(incl_POSet(sK15))) ),
inference(extension,[status(thm),parent(t54:2)],[f_34_4]) ).
cnf(t57,plain,
$false,
inference(connection,[status(thm),parent(t56:1)],[t56:1,t54:2]) ).
cnf(t58,plain,
rel_str(incl_POSet(sK15)),
inference(extension,[status(thm),parent(t56:2)],[f_48_6]) ).
cnf(t59,plain,
$false,
inference(connection,[status(thm),parent(t58:1)],[t58:1,t56:2]) ).
cnf(t60,plain,
strict_rel_str(incl_POSet(sK15)),
inference(extension,[status(thm),parent(t56:3)],[f_51_5]) ).
cnf(t61,plain,
$false,
inference(connection,[status(thm),parent(t60:1)],[t60:1,t56:3]) ).
cnf(t62,plain,
( rel_str_of(incl_POSet(sK15),sK8(incl_POSet(sK15),incl_POSet(sK15))) != rel_str_of(incl_POSet(sK15),sK8(incl_POSet(sK15),incl_POSet(sK15)))
| ~ relation_of2(sK8(incl_POSet(sK15),incl_POSet(sK15)),incl_POSet(sK15),incl_POSet(sK15))
| sP5(incl_POSet(sK15),sK8(incl_POSet(sK15),incl_POSet(sK15)),sK8(incl_POSet(sK15),incl_POSet(sK15)),incl_POSet(sK15)) ),
inference(extension,[status(thm),parent(t54:3)],[f_33_4]) ).
cnf(t63,plain,
$false,
inference(connection,[status(thm),parent(t62:1)],[t62:1,t54:3]) ).
cnf(t64,plain,
relation_of2(sK8(incl_POSet(sK15),incl_POSet(sK15)),incl_POSet(sK15),incl_POSet(sK15)),
inference(extension,[status(thm),parent(t62:2)],[f_23_5]) ).
cnf(t65,plain,
$false,
inference(connection,[status(thm),parent(t64:1)],[t64:1,t62:2]) ).
cnf(t66,plain,
rel_str_of(incl_POSet(sK15),sK8(incl_POSet(sK15),incl_POSet(sK15))) = rel_str_of(incl_POSet(sK15),sK8(incl_POSet(sK15),incl_POSet(sK15))),
inference(extension,[status(thm),parent(t62:3)],[equality_1]) ).
cnf(t67,plain,
$false,
inference(connection,[status(thm),parent(t66:1)],[t66:1,t62:3]) ).
cnf(t68,plain,
incl_POSet(sK15) = rel_str_of(sK15,inclusion_order(sK15)),
inference(extension,[status(thm),parent(t54:4)],[f_52_4]) ).
cnf(t69,plain,
$false,
inference(connection,[status(thm),parent(t68:1)],[t68:1,t54:4]) ).
cnf(t70,plain,
( incl_POSet(sK15) != rel_str_of(sK15,inclusion_order(sK15))
| incl_POSet(sK15) != rel_str_of(sK15,inclusion_order(sK15))
| sK8(incl_POSet(sK15),incl_POSet(sK15)) = sK8(rel_str_of(sK15,inclusion_order(sK15)),rel_str_of(sK15,inclusion_order(sK15))) ),
inference(extension,[status(thm),parent(t54:5)],[equality_15]) ).
cnf(t71,plain,
$false,
inference(connection,[status(thm),parent(t70:1)],[t70:1,t54:5]) ).
cnf(t72,plain,
incl_POSet(sK15) = rel_str_of(sK15,inclusion_order(sK15)),
inference(extension,[status(thm),parent(t70:2)],[f_52_4]) ).
cnf(t73,plain,
$false,
inference(connection,[status(thm),parent(t72:1)],[t72:1,t70:2]) ).
cnf(t74,plain,
incl_POSet(sK15) = rel_str_of(sK15,inclusion_order(sK15)),
inference(extension,[status(thm),parent(t70:3)],[f_52_4]) ).
cnf(t75,plain,
$false,
inference(connection,[status(thm),parent(t74:1)],[t74:1,t70:3]) ).
cnf(t76,plain,
( incl_POSet(sK15) != rel_str_of(sK15,inclusion_order(sK15))
| incl_POSet(sK15) != rel_str_of(sK15,inclusion_order(sK15))
| sK8(incl_POSet(sK15),incl_POSet(sK15)) = sK8(rel_str_of(sK15,inclusion_order(sK15)),rel_str_of(sK15,inclusion_order(sK15))) ),
inference(extension,[status(thm),parent(t54:6)],[equality_15]) ).
cnf(t77,plain,
$false,
inference(connection,[status(thm),parent(t76:1)],[t76:1,t54:6]) ).
cnf(t78,plain,
incl_POSet(sK15) = rel_str_of(sK15,inclusion_order(sK15)),
inference(extension,[status(thm),parent(t76:2)],[f_52_4]) ).
cnf(t79,plain,
$false,
inference(connection,[status(thm),parent(t78:1)],[t78:1,t76:2]) ).
cnf(t80,plain,
incl_POSet(sK15) = rel_str_of(sK15,inclusion_order(sK15)),
inference(extension,[status(thm),parent(t76:3)],[f_52_4]) ).
cnf(t81,plain,
$false,
inference(connection,[status(thm),parent(t80:1)],[t80:1,t76:3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU368+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.12/0.37 % Computer : n010.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sun Sep 20 00:05:24 UTC 2026
% 0.12/0.37 % CPUTime :
% 31.46/31.73 % SZS status Theorem for theBenchmark
% 31.46/31.73 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------