%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SEU374+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:09 AM UTC 2026
% Result : Theorem 2.89s 3.16s
% Output : Proof 2.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 8
% Syntax : Number of formulae : 94 ( 56 unt; 0 def)
% Number of atoms : 322 ( 61 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 326 ( 98 ~; 85 |; 112 &)
% ( 1 <=>; 30 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 7 con; 0-4 aty)
% Number of variables : 111 ( 0 sgn 56 !; 35 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d8_yellow_6,axiom,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( net_str(B,A)
=> ! [C] :
( net_str(C,A)
=> ( subnetstr(C,A,B)
<=> ( the_mapping(A,C) = relation_dom_restr_as_relation_of(the_carrier(B),the_carrier(A),the_mapping(A,B),the_carrier(C))
& subrelstr(C,B) ) ) ) ) ),
file('theBenchmark.p',d8_yellow_6) ).
fof(dt_l1_waybel_0,axiom,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( net_str(B,A)
=> rel_str(B) ) ),
file('theBenchmark.p',dt_l1_waybel_0) ).
fof(dt_m1_yellow_6,axiom,
! [A,B] :
( ( net_str(B,A)
& one_sorted_str(A) )
=> ! [C] :
( subnetstr(C,A,B)
=> net_str(C,A) ) ),
file('theBenchmark.p',dt_m1_yellow_6) ).
fof(t20_yellow_6,conjecture,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( net_str(B,A)
=> ! [C] :
( subnetstr(C,A,B)
=> ! [D] :
( element(D,the_carrier(B))
=> ! [E] :
( element(E,the_carrier(B))
=> ! [F] :
( element(F,the_carrier(C))
=> ! [G] :
( element(G,the_carrier(C))
=> ( ( related(C,F,G)
& E = G
& D = F )
=> related(B,D,E) ) ) ) ) ) ) ) ),
file('theBenchmark.p',t20_yellow_6) ).
fof(t60_yellow_0,axiom,
! [A] :
( rel_str(A)
=> ! [B] :
( subrelstr(B,A)
=> ! [C] :
( element(C,the_carrier(A))
=> ! [D] :
( element(D,the_carrier(A))
=> ! [E] :
( element(E,the_carrier(B))
=> ! [F] :
( element(F,the_carrier(B))
=> ( ( related(B,E,F)
& F = D
& E = C )
=> related(A,C,D) ) ) ) ) ) ) ),
file('theBenchmark.p',t60_yellow_0) ).
fof(f_6_1,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( subnetstr(C,A,B)
| the_mapping(A,C) != relation_dom_restr_as_relation_of(the_carrier(B),the_carrier(A),the_mapping(A,B),the_carrier(C))
| ~ subrelstr(C,B) )
& ( ( the_mapping(A,C) = relation_dom_restr_as_relation_of(the_carrier(B),the_carrier(A),the_mapping(A,B),the_carrier(C))
& subrelstr(C,B) )
| ~ subnetstr(C,A,B) ) )
| ~ net_str(C,A) )
| ~ net_str(B,A) )
| ~ one_sorted_str(A) ),
inference(fof_nnf,[status(thm)],[d8_yellow_6]) ).
fof(f_6_2,plain,
! [U_10] :
( ! [U_9] :
( ! [U_8] :
( ( ( subnetstr(U_8,U_10,U_9)
| the_mapping(U_10,U_8) != relation_dom_restr_as_relation_of(the_carrier(U_9),the_carrier(U_10),the_mapping(U_10,U_9),the_carrier(U_8))
| ~ subrelstr(U_8,U_9) )
& ( ( the_mapping(U_10,U_8) = relation_dom_restr_as_relation_of(the_carrier(U_9),the_carrier(U_10),the_mapping(U_10,U_9),the_carrier(U_8))
& subrelstr(U_8,U_9) )
| ~ subnetstr(U_8,U_10,U_9) ) )
| ~ net_str(U_8,U_10) )
| ~ net_str(U_9,U_10) )
| ~ one_sorted_str(U_10) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
cnf(f_6_3,plain,
( subrelstr(U_8,U_9)
| ~ subnetstr(U_8,U_10,U_9)
| ~ net_str(U_8,U_10)
| ~ net_str(U_9,U_10)
| ~ one_sorted_str(U_10) ),
inference(clausify,[status(thm)],[f_6_2]) ).
fof(f_14_1,plain,
! [A] :
( ! [B] :
( rel_str(B)
| ~ net_str(B,A) )
| ~ one_sorted_str(A) ),
inference(fof_nnf,[status(thm)],[dt_l1_waybel_0]) ).
fof(f_14_2,plain,
! [U_19] :
( ! [U_18] :
( rel_str(U_18)
| ~ net_str(U_18,U_19) )
| ~ one_sorted_str(U_19) ),
inference(variable_rename,[status(thm)],[f_14_1]) ).
cnf(f_14_3,plain,
( rel_str(U_18)
| ~ net_str(U_18,U_19)
| ~ one_sorted_str(U_19) ),
inference(clausify,[status(thm)],[f_14_2]) ).
fof(f_18_1,plain,
! [A,B] :
( ! [C] :
( net_str(C,A)
| ~ subnetstr(C,A,B) )
| ~ net_str(B,A)
| ~ one_sorted_str(A) ),
inference(fof_nnf,[status(thm)],[dt_m1_yellow_6]) ).
fof(f_18_2,plain,
! [U_24,U_23] :
( ! [U_22] :
( net_str(U_22,U_24)
| ~ subnetstr(U_22,U_24,U_23) )
| ~ net_str(U_23,U_24)
| ~ one_sorted_str(U_24) ),
inference(variable_rename,[status(thm)],[f_18_1]) ).
cnf(f_18_3,plain,
( net_str(U_22,U_24)
| ~ subnetstr(U_22,U_24,U_23)
| ~ net_str(U_23,U_24)
| ~ one_sorted_str(U_24) ),
inference(clausify,[status(thm)],[f_18_2]) ).
fof(f_50_1,negated_conjecture,
~ ! [A] :
( one_sorted_str(A)
=> ! [B] :
( net_str(B,A)
=> ! [C] :
( subnetstr(C,A,B)
=> ! [D] :
( element(D,the_carrier(B))
=> ! [E] :
( element(E,the_carrier(B))
=> ! [F] :
( element(F,the_carrier(C))
=> ! [G] :
( element(G,the_carrier(C))
=> ( ( related(C,F,G)
& E = G
& D = F )
=> related(B,D,E) ) ) ) ) ) ) ) ),
inference(negate,[status(cth)],[t20_yellow_6]) ).
fof(f_50_2,negated_conjecture,
? [A] :
( ? [B] :
( ? [C] :
( ? [D] :
( ? [E] :
( ? [F] :
( ? [G] :
( ~ related(B,D,E)
& related(C,F,G)
& E = G
& D = F
& element(G,the_carrier(C)) )
& element(F,the_carrier(C)) )
& element(E,the_carrier(B)) )
& element(D,the_carrier(B)) )
& subnetstr(C,A,B) )
& net_str(B,A) )
& one_sorted_str(A) ),
inference(fof_nnf,[status(thm)],[f_50_1]) ).
fof(f_50_3,negated_conjecture,
? [U_93] :
( ? [U_92] :
( ? [U_91] :
( ? [U_90] :
( ? [U_89] :
( ? [U_88] :
( ? [U_87] :
( ~ related(U_92,U_90,U_89)
& related(U_91,U_88,U_87)
& U_89 = U_87
& U_90 = U_88
& element(U_87,the_carrier(U_91)) )
& element(U_88,the_carrier(U_91)) )
& element(U_89,the_carrier(U_92)) )
& element(U_90,the_carrier(U_92)) )
& subnetstr(U_91,U_93,U_92) )
& net_str(U_92,U_93) )
& one_sorted_str(U_93) ),
inference(variable_rename,[status(thm)],[f_50_2]) ).
fof(f_50_4,negated_conjecture,
( ? [U_92] :
( ? [U_91] :
( ? [U_90] :
( ? [U_89] :
( ? [U_88] :
( ? [U_87] :
( ~ related(U_92,U_90,U_89)
& related(U_91,U_88,U_87)
& U_89 = U_87
& U_90 = U_88
& element(U_87,the_carrier(U_91)) )
& element(U_88,the_carrier(U_91)) )
& element(U_89,the_carrier(U_92)) )
& element(U_90,the_carrier(U_92)) )
& subnetstr(U_91,sK19,U_92) )
& net_str(U_92,sK19) )
& one_sorted_str(sK19) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(U_93,sK19)],[f_50_3]) ).
fof(f_50_5,negated_conjecture,
( ? [U_91] :
( ? [U_90] :
( ? [U_89] :
( ? [U_88] :
( ? [U_87] :
( ~ related(sK20,U_90,U_89)
& related(U_91,U_88,U_87)
& U_89 = U_87
& U_90 = U_88
& element(U_87,the_carrier(U_91)) )
& element(U_88,the_carrier(U_91)) )
& element(U_89,the_carrier(sK20)) )
& element(U_90,the_carrier(sK20)) )
& subnetstr(U_91,sK19,sK20) )
& net_str(sK20,sK19)
& one_sorted_str(sK19) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(U_92,sK20)],[f_50_4]) ).
fof(f_50_6,negated_conjecture,
( ? [U_90] :
( ? [U_89] :
( ? [U_88] :
( ? [U_87] :
( ~ related(sK20,U_90,U_89)
& related(sK21,U_88,U_87)
& U_89 = U_87
& U_90 = U_88
& element(U_87,the_carrier(sK21)) )
& element(U_88,the_carrier(sK21)) )
& element(U_89,the_carrier(sK20)) )
& element(U_90,the_carrier(sK20)) )
& subnetstr(sK21,sK19,sK20)
& net_str(sK20,sK19)
& one_sorted_str(sK19) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21]),skolemize(U_91,sK21)],[f_50_5]) ).
fof(f_50_7,negated_conjecture,
( ? [U_89] :
( ? [U_88] :
( ? [U_87] :
( ~ related(sK20,sK22,U_89)
& related(sK21,U_88,U_87)
& U_89 = U_87
& sK22 = U_88
& element(U_87,the_carrier(sK21)) )
& element(U_88,the_carrier(sK21)) )
& element(U_89,the_carrier(sK20)) )
& element(sK22,the_carrier(sK20))
& subnetstr(sK21,sK19,sK20)
& net_str(sK20,sK19)
& one_sorted_str(sK19) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22]),skolemize(U_90,sK22)],[f_50_6]) ).
fof(f_50_8,negated_conjecture,
( ? [U_88] :
( ? [U_87] :
( ~ related(sK20,sK22,sK23)
& related(sK21,U_88,U_87)
& sK23 = U_87
& sK22 = U_88
& element(U_87,the_carrier(sK21)) )
& element(U_88,the_carrier(sK21)) )
& element(sK23,the_carrier(sK20))
& element(sK22,the_carrier(sK20))
& subnetstr(sK21,sK19,sK20)
& net_str(sK20,sK19)
& one_sorted_str(sK19) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23]),skolemize(U_89,sK23)],[f_50_7]) ).
fof(f_50_9,negated_conjecture,
( ? [U_87] :
( ~ related(sK20,sK22,sK23)
& related(sK21,sK24,U_87)
& sK23 = U_87
& sK22 = sK24
& element(U_87,the_carrier(sK21)) )
& element(sK24,the_carrier(sK21))
& element(sK23,the_carrier(sK20))
& element(sK22,the_carrier(sK20))
& subnetstr(sK21,sK19,sK20)
& net_str(sK20,sK19)
& one_sorted_str(sK19) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24]),skolemize(U_88,sK24)],[f_50_8]) ).
fof(f_50_10,negated_conjecture,
( ~ related(sK20,sK22,sK23)
& related(sK21,sK24,sK25)
& sK23 = sK25
& sK22 = sK24
& element(sK25,the_carrier(sK21))
& element(sK24,the_carrier(sK21))
& element(sK23,the_carrier(sK20))
& element(sK22,the_carrier(sK20))
& subnetstr(sK21,sK19,sK20)
& net_str(sK20,sK19)
& one_sorted_str(sK19) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25]),skolemize(U_87,sK25)],[f_50_9]) ).
fof(f_50_11,negated_conjecture,
( ~ related(sK20,sK22,sK23)
& related(sK21,sK24,sK25)
& sK23 = sK25
& sK22 = sK24
& element(sK25,the_carrier(sK21))
& element(sK24,the_carrier(sK21))
& element(sK23,the_carrier(sK20))
& element(sK22,the_carrier(sK20))
& subnetstr(sK21,sK19,sK20)
& net_str(sK20,sK19)
& one_sorted_str(sK19) ),
inference(definitional_conversion,[status(esa)],[f_50_10]) ).
cnf(f_50_12,negated_conjecture,
one_sorted_str(sK19),
inference(clausify,[status(thm)],[f_50_11]) ).
cnf(f_50_13,negated_conjecture,
net_str(sK20,sK19),
inference(clausify,[status(thm)],[f_50_11]) ).
cnf(f_50_14,negated_conjecture,
subnetstr(sK21,sK19,sK20),
inference(clausify,[status(thm)],[f_50_11]) ).
cnf(f_50_15,negated_conjecture,
element(sK22,the_carrier(sK20)),
inference(clausify,[status(thm)],[f_50_11]) ).
cnf(f_50_16,negated_conjecture,
element(sK23,the_carrier(sK20)),
inference(clausify,[status(thm)],[f_50_11]) ).
cnf(f_50_17,negated_conjecture,
element(sK24,the_carrier(sK21)),
inference(clausify,[status(thm)],[f_50_11]) ).
cnf(f_50_18,negated_conjecture,
element(sK25,the_carrier(sK21)),
inference(clausify,[status(thm)],[f_50_11]) ).
cnf(f_50_19,negated_conjecture,
sK22 = sK24,
inference(clausify,[status(thm)],[f_50_11]) ).
cnf(f_50_20,negated_conjecture,
sK23 = sK25,
inference(clausify,[status(thm)],[f_50_11]) ).
cnf(f_50_21,negated_conjecture,
related(sK21,sK24,sK25),
inference(clausify,[status(thm)],[f_50_11]) ).
cnf(f_50_22,negated_conjecture,
~ related(sK20,sK22,sK23),
inference(clausify,[status(thm)],[f_50_11]) ).
fof(f_55_1,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ! [E] :
( ! [F] :
( related(A,C,D)
| ~ related(B,E,F)
| F != D
| E != C
| ~ element(F,the_carrier(B)) )
| ~ element(E,the_carrier(B)) )
| ~ element(D,the_carrier(A)) )
| ~ element(C,the_carrier(A)) )
| ~ subrelstr(B,A) )
| ~ rel_str(A) ),
inference(fof_nnf,[status(thm)],[t60_yellow_0]) ).
fof(f_55_2,plain,
! [U_113] :
( ! [U_112] :
( ! [U_111] :
( ! [U_110] :
( ! [U_109] :
( ! [U_108] :
( related(U_113,U_111,U_110)
| ~ related(U_112,U_109,U_108)
| U_108 != U_110
| U_109 != U_111
| ~ element(U_108,the_carrier(U_112)) )
| ~ element(U_109,the_carrier(U_112)) )
| ~ element(U_110,the_carrier(U_113)) )
| ~ element(U_111,the_carrier(U_113)) )
| ~ subrelstr(U_112,U_113) )
| ~ rel_str(U_113) ),
inference(variable_rename,[status(thm)],[f_55_1]) ).
cnf(f_55_3,plain,
( related(U_113,U_111,U_110)
| ~ related(U_112,U_109,U_108)
| U_108 != U_110
| U_109 != U_111
| ~ element(U_108,the_carrier(U_112))
| ~ element(U_109,the_carrier(U_112))
| ~ element(U_110,the_carrier(U_113))
| ~ element(U_111,the_carrier(U_113))
| ~ subrelstr(U_112,U_113)
| ~ rel_str(U_113) ),
inference(clausify,[status(thm)],[f_55_2]) ).
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(t1,plain,
~ related(sK20,sK22,sK23),
inference(start,[status(thm),parent(0:0)],[f_50_22]) ).
cnf(t2,plain,
( ~ subrelstr(sK21,sK20)
| ~ element(sK22,the_carrier(sK20))
| ~ element(sK23,the_carrier(sK20))
| ~ element(sK24,the_carrier(sK21))
| ~ element(sK25,the_carrier(sK21))
| sK24 != sK22
| sK25 != sK23
| ~ related(sK21,sK24,sK25)
| ~ rel_str(sK20)
| related(sK20,sK22,sK23) ),
inference(extension,[status(thm),parent(t1:1)],[f_55_3]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( ~ net_str(sK20,sK19)
| ~ one_sorted_str(sK19)
| rel_str(sK20) ),
inference(extension,[status(thm),parent(t2:2)],[f_14_3]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
one_sorted_str(sK19),
inference(extension,[status(thm),parent(t4:2)],[f_50_12]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(t8,plain,
net_str(sK20,sK19),
inference(extension,[status(thm),parent(t4:3)],[f_50_13]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t4:3]) ).
cnf(t10,plain,
related(sK21,sK24,sK25),
inference(extension,[status(thm),parent(t2:3)],[f_50_21]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t2:3]) ).
cnf(t12,plain,
( sK23 != sK23
| sK25 != sK23
| sK25 = sK23 ),
inference(extension,[status(thm),parent(t2:4)],[equality_3]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t2:4]) ).
cnf(t14,plain,
( sK23 != sK25
| sK25 = sK23 ),
inference(extension,[status(thm),parent(t12:2)],[equality_2]) ).
cnf(t15,plain,
$false,
inference(connection,[status(thm),parent(t14:1)],[t14:1,t12:2]) ).
cnf(t16,plain,
sK23 = sK25,
inference(extension,[status(thm),parent(t14:2)],[f_50_20]) ).
cnf(t17,plain,
$false,
inference(connection,[status(thm),parent(t16:1)],[t16:1,t14:2]) ).
cnf(t18,plain,
sK23 = sK23,
inference(extension,[status(thm),parent(t12:3)],[equality_1]) ).
cnf(t19,plain,
$false,
inference(connection,[status(thm),parent(t18:1)],[t18:1,t12:3]) ).
cnf(t20,plain,
( sK22 != sK22
| sK24 != sK22
| sK24 = sK22 ),
inference(extension,[status(thm),parent(t2:5)],[equality_3]) ).
cnf(t21,plain,
$false,
inference(connection,[status(thm),parent(t20:1)],[t20:1,t2:5]) ).
cnf(t22,plain,
( sK22 != sK24
| sK24 = sK22 ),
inference(extension,[status(thm),parent(t20:2)],[equality_2]) ).
cnf(t23,plain,
$false,
inference(connection,[status(thm),parent(t22:1)],[t22:1,t20:2]) ).
cnf(t24,plain,
sK22 = sK24,
inference(extension,[status(thm),parent(t22:2)],[f_50_19]) ).
cnf(t25,plain,
$false,
inference(connection,[status(thm),parent(t24:1)],[t24:1,t22:2]) ).
cnf(t26,plain,
sK22 = sK22,
inference(extension,[status(thm),parent(t20:3)],[equality_1]) ).
cnf(t27,plain,
$false,
inference(connection,[status(thm),parent(t26:1)],[t26:1,t20:3]) ).
cnf(t28,plain,
element(sK25,the_carrier(sK21)),
inference(extension,[status(thm),parent(t2:6)],[f_50_18]) ).
cnf(t29,plain,
$false,
inference(connection,[status(thm),parent(t28:1)],[t28:1,t2:6]) ).
cnf(t30,plain,
element(sK24,the_carrier(sK21)),
inference(extension,[status(thm),parent(t2:7)],[f_50_17]) ).
cnf(t31,plain,
$false,
inference(connection,[status(thm),parent(t30:1)],[t30:1,t2:7]) ).
cnf(t32,plain,
element(sK23,the_carrier(sK20)),
inference(extension,[status(thm),parent(t2:8)],[f_50_16]) ).
cnf(t33,plain,
$false,
inference(connection,[status(thm),parent(t32:1)],[t32:1,t2:8]) ).
cnf(t34,plain,
element(sK22,the_carrier(sK20)),
inference(extension,[status(thm),parent(t2:9)],[f_50_15]) ).
cnf(t35,plain,
$false,
inference(connection,[status(thm),parent(t34:1)],[t34:1,t2:9]) ).
cnf(t36,plain,
( ~ net_str(sK20,sK19)
| ~ net_str(sK21,sK19)
| ~ subnetstr(sK21,sK19,sK20)
| ~ one_sorted_str(sK19)
| subrelstr(sK21,sK20) ),
inference(extension,[status(thm),parent(t2:10)],[f_6_3]) ).
cnf(t37,plain,
$false,
inference(connection,[status(thm),parent(t36:1)],[t36:1,t2:10]) ).
cnf(t38,plain,
one_sorted_str(sK19),
inference(extension,[status(thm),parent(t36:2)],[f_50_12]) ).
cnf(t39,plain,
$false,
inference(connection,[status(thm),parent(t38:1)],[t38:1,t36:2]) ).
cnf(l19,lemma,
one_sorted_str(sK19),
inference(lemma,[status(cth),parent(t36:2),below(t2:10)],[t36:2]) ).
cnf(t40,plain,
subnetstr(sK21,sK19,sK20),
inference(extension,[status(thm),parent(t36:3)],[f_50_14]) ).
cnf(t41,plain,
$false,
inference(connection,[status(thm),parent(t40:1)],[t40:1,t36:3]) ).
cnf(t42,plain,
( ~ net_str(sK20,sK19)
| ~ subnetstr(sK21,sK19,sK20)
| ~ one_sorted_str(sK19)
| net_str(sK21,sK19) ),
inference(extension,[status(thm),parent(t36:4)],[f_18_3]) ).
cnf(t43,plain,
$false,
inference(connection,[status(thm),parent(t42:1)],[t42:1,t36:4]) ).
cnf(t44,plain,
one_sorted_str(sK19),
inference(lemma_extension,[status(thm),parent(t42:2)],[l19:1]) ).
cnf(t45,plain,
$false,
inference(connection,[status(thm),parent(t44:1)],[t44:1,t42:2]) ).
cnf(t46,plain,
subnetstr(sK21,sK19,sK20),
inference(extension,[status(thm),parent(t42:3)],[f_50_14]) ).
cnf(t47,plain,
$false,
inference(connection,[status(thm),parent(t46:1)],[t46:1,t42:3]) ).
cnf(t48,plain,
net_str(sK20,sK19),
inference(extension,[status(thm),parent(t42:4)],[f_50_13]) ).
cnf(t49,plain,
$false,
inference(connection,[status(thm),parent(t48:1)],[t48:1,t42:4]) ).
cnf(t50,plain,
net_str(sK20,sK19),
inference(extension,[status(thm),parent(t36:5)],[f_50_13]) ).
cnf(t51,plain,
$false,
inference(connection,[status(thm),parent(t50:1)],[t50:1,t36:5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU374+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.09/0.36 % Computer : n010.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 20 00:06:08 UTC 2026
% 0.09/0.37 % CPUTime :
% 2.89/3.16 % SZS status Theorem for theBenchmark
% 2.89/3.16 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------