%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SEU375+1 : TPTP v9.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n029.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Jul 25 03:45:19 PM UTC 2025
% Result : Theorem 26.57s 3.72s
% Output : CNFRefutation 26.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 9
% Syntax : Number of formulae : 69 ( 39 unt; 0 def)
% Number of atoms : 189 ( 15 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 194 ( 74 ~; 67 |; 18 &)
% ( 1 <=>; 34 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 7 con; 0-1 aty)
% Number of variables : 57 ( 0 sgn 34 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(t21_yellow_6,plain,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( ( ~ empty_carrier(B)
& net_str(B,A) )
=> ! [C] :
( ( ~ empty_carrier(C)
& full_subnetstr(C,A,B)
& 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))
=> ( ( D = F
& E = G
& related(B,D,E) )
=> related(C,F,G) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t21_yellow_6) ).
fof(t21_yellow_6_negated,plain,
~ ! [A] :
( one_sorted_str(A)
=> ! [B] :
( ( ~ empty_carrier(B)
& net_str(B,A) )
=> ! [C] :
( ( ~ empty_carrier(C)
& full_subnetstr(C,A,B)
& 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))
=> ( ( D = F
& E = G
& related(B,D,E) )
=> related(C,F,G) ) ) ) ) ) ) ) ),
inference(negate_conjecture,[status(cth)],[t21_yellow_6]) ).
cnf(51,plain,
~ empty_carrier(sK18),
inference(cnf,[status(esa)],[t21_yellow_6_negated]) ).
cnf(l0,plain,
~ empty_carrier(sK18),
inference(instantiation,[status(thm)],[51]) ).
fof(fc1_struct_0,plain,
! [A] :
( ( ~ empty_carrier(A)
& one_sorted_str(A) )
=> ~ empty(the_carrier(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_struct_0) ).
cnf(22,plain,
( ~ empty(the_carrier(X0))
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf,[status(esa)],[fc1_struct_0]) ).
cnf(l1,plain,
( ~ empty(the_carrier(sK18))
| ~ one_sorted_str(sK18)
| empty_carrier(sK18) ),
inference(instantiation,[status(thm)],[22]) ).
fof(t2_subset,plain,
! [A,B] :
( element(A,B)
=> ( empty(B)
| in(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
cnf(62,plain,
( ~ element(X0,X1)
| empty(X1)
| in(X0,X1) ),
inference(cnf,[status(esa)],[t2_subset]) ).
cnf(l2,plain,
( ~ element(sK19,the_carrier(sK18))
| empty(the_carrier(sK18))
| in(sK19,the_carrier(sK18)) ),
inference(instantiation,[status(thm)],[62]) ).
fof(t61_yellow_0,plain,
! [A] :
( rel_str(A)
=> ! [B] :
( ( full_subrelstr(B,A)
& 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))
=> ( ( E = C
& F = D
& related(A,C,D)
& in(E,the_carrier(B))
& in(F,the_carrier(B)) )
=> related(B,E,F) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t61_yellow_0) ).
cnf(63,plain,
( ~ in(X0,the_carrier(X1))
| ~ in(X2,the_carrier(X1))
| ~ full_subrelstr(X1,X3)
| ~ rel_str(X3)
| ~ element(X4,the_carrier(X3))
| ~ element(X5,the_carrier(X3))
| ~ element(X0,the_carrier(X1))
| ~ element(X2,the_carrier(X1))
| ~ subrelstr(X1,X3)
| X0 != X4
| X2 != X5
| ~ related(X3,X4,X5)
| related(X1,X0,X2) ),
inference(cnf,[status(esa)],[t61_yellow_0]) ).
cnf(l62,plain,
( ~ in(sK19,the_carrier(sK18))
| ~ in(sK22,the_carrier(sK18))
| ~ full_subrelstr(sK18,sK17)
| ~ rel_str(sK17)
| ~ element(sK19,the_carrier(sK17))
| ~ element(sK20,the_carrier(sK17))
| ~ element(sK19,the_carrier(sK18))
| ~ element(sK22,the_carrier(sK18))
| ~ subrelstr(sK18,sK17)
| sK19 != sK19
| sK22 != sK20
| ~ related(sK17,sK19,sK20)
| related(sK18,sK19,sK22) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(54,plain,
element(sK19,the_carrier(sK17)),
inference(cnf,[status(esa)],[t21_yellow_6_negated]) ).
cnf(l240,plain,
element(sK19,the_carrier(sK17)),
inference(instantiation,[status(thm)],[54]) ).
fof(d9_yellow_6,plain,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( net_str(B,A)
=> ! [C] :
( subnetstr(C,A,B)
=> ( full_subnetstr(C,A,B)
<=> ( full_subrelstr(C,B)
& subrelstr(C,B) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d9_yellow_6) ).
cnf(7,plain,
( ~ full_subnetstr(X0,X1,X2)
| ~ one_sorted_str(X1)
| ~ net_str(X2,X1)
| ~ subnetstr(X0,X1,X2)
| subrelstr(X0,X2) ),
inference(cnf,[status(esa)],[d9_yellow_6]) ).
cnf(l233,plain,
( ~ full_subnetstr(sK18,sK16,sK17)
| ~ one_sorted_str(sK16)
| ~ net_str(sK17,sK16)
| ~ subnetstr(sK18,sK16,sK17)
| subrelstr(sK18,sK17) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(53,plain,
subnetstr(sK18,sK16,sK17),
inference(cnf,[status(esa)],[t21_yellow_6_negated]) ).
cnf(l1854,plain,
subnetstr(sK18,sK16,sK17),
inference(instantiation,[status(thm)],[53]) ).
cnf(48,plain,
one_sorted_str(sK16),
inference(cnf,[status(esa)],[t21_yellow_6_negated]) ).
cnf(l1884,plain,
one_sorted_str(sK16),
inference(instantiation,[status(thm)],[48]) ).
fof(dt_l1_orders_2,plain,
! [A] :
( rel_str(A)
=> one_sorted_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_orders_2) ).
cnf(9,plain,
( ~ rel_str(X0)
| one_sorted_str(X0) ),
inference(cnf,[status(esa)],[dt_l1_orders_2]) ).
cnf(l261,plain,
( ~ rel_str(sK18)
| one_sorted_str(sK18) ),
inference(instantiation,[status(thm)],[9]) ).
fof(t1_subset,plain,
! [A,B] :
( in(A,B)
=> element(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
cnf(47,plain,
( ~ in(X0,X1)
| element(X0,X1) ),
inference(cnf,[status(esa)],[t1_subset]) ).
cnf(l216,plain,
( ~ in(sK19,the_carrier(sK18))
| element(sK19,the_carrier(sK18)) ),
inference(instantiation,[status(thm)],[47]) ).
fof(dt_l1_waybel_0,plain,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( net_str(B,A)
=> rel_str(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_waybel_0) ).
cnf(10,plain,
( ~ one_sorted_str(X0)
| ~ net_str(X1,X0)
| rel_str(X1) ),
inference(cnf,[status(esa)],[dt_l1_waybel_0]) ).
cnf(l921,plain,
( ~ one_sorted_str(sK16)
| ~ net_str(sK18,sK16)
| rel_str(sK18) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(50,plain,
net_str(sK17,sK16),
inference(cnf,[status(esa)],[t21_yellow_6_negated]) ).
cnf(l246,plain,
net_str(sK17,sK16),
inference(instantiation,[status(thm)],[50]) ).
cnf(l82,plain,
( ~ one_sorted_str(sK16)
| ~ net_str(sK17,sK16)
| rel_str(sK17) ),
inference(instantiation,[status(thm)],[10]) ).
fof(dt_m1_yellow_6,plain,
! [A,B] :
( ( one_sorted_str(A)
& net_str(B,A) )
=> ! [C] :
( subnetstr(C,A,B)
=> net_str(C,A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_yellow_6) ).
cnf(12,plain,
( ~ one_sorted_str(X0)
| ~ net_str(X1,X0)
| ~ subnetstr(X2,X0,X1)
| net_str(X2,X0) ),
inference(cnf,[status(esa)],[dt_m1_yellow_6]) ).
cnf(l961,plain,
( ~ one_sorted_str(sK16)
| ~ net_str(sK17,sK16)
| ~ subnetstr(sK18,sK16,sK17)
| net_str(sK18,sK16) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(60,plain,
related(sK17,sK19,sK20),
inference(cnf,[status(esa)],[t21_yellow_6_negated]) ).
cnf(l226,plain,
related(sK17,sK19,sK20),
inference(instantiation,[status(thm)],[60]) ).
cnf(l947,plain,
one_sorted_str(sK16),
inference(instantiation,[status(thm)],[48]) ).
cnf(55,plain,
element(sK20,the_carrier(sK17)),
inference(cnf,[status(esa)],[t21_yellow_6_negated]) ).
cnf(l248,plain,
element(sK20,the_carrier(sK17)),
inference(instantiation,[status(thm)],[55]) ).
cnf(l122,plain,
net_str(sK17,sK16),
inference(instantiation,[status(thm)],[50]) ).
cnf(61,plain,
~ related(sK18,sK21,sK22),
inference(cnf,[status(esa)],[t21_yellow_6_negated]) ).
cnf(l235,plain,
~ related(sK18,sK21,sK22),
inference(instantiation,[status(thm)],[61]) ).
cnf(6,plain,
( ~ full_subnetstr(X0,X1,X2)
| ~ one_sorted_str(X1)
| ~ net_str(X2,X1)
| ~ subnetstr(X0,X1,X2)
| full_subrelstr(X0,X2) ),
inference(cnf,[status(esa)],[d9_yellow_6]) ).
cnf(l77,plain,
( ~ full_subnetstr(sK18,sK16,sK17)
| ~ one_sorted_str(sK16)
| ~ net_str(sK17,sK16)
| ~ subnetstr(sK18,sK16,sK17)
| full_subrelstr(sK18,sK17) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l89,plain,
( ~ element(sK22,the_carrier(sK18))
| empty(the_carrier(sK18))
| in(sK22,the_carrier(sK18)) ),
inference(instantiation,[status(thm)],[62]) ).
cnf(l130,plain,
one_sorted_str(sK16),
inference(instantiation,[status(thm)],[48]) ).
cnf(59,plain,
sK20 = sK22,
inference(cnf,[status(esa)],[t21_yellow_6_negated]) ).
cnf(l236,plain,
sK20 = sK22,
inference(instantiation,[status(thm)],[59]) ).
cnf(l110,plain,
subnetstr(sK18,sK16,sK17),
inference(instantiation,[status(thm)],[53]) ).
cnf(l1016,plain,
one_sorted_str(sK16),
inference(instantiation,[status(thm)],[48]) ).
cnf(l1017,plain,
net_str(sK17,sK16),
inference(instantiation,[status(thm)],[50]) ).
cnf(52,plain,
full_subnetstr(sK18,sK16,sK17),
inference(cnf,[status(esa)],[t21_yellow_6_negated]) ).
cnf(l134,plain,
full_subnetstr(sK18,sK16,sK17),
inference(instantiation,[status(thm)],[52]) ).
cnf(l108,plain,
net_str(sK17,sK16),
inference(instantiation,[status(thm)],[50]) ).
cnf(l1175,plain,
subnetstr(sK18,sK16,sK17),
inference(instantiation,[status(thm)],[53]) ).
cnf(57,plain,
element(sK22,the_carrier(sK18)),
inference(cnf,[status(esa)],[t21_yellow_6_negated]) ).
cnf(l158,plain,
element(sK22,the_carrier(sK18)),
inference(instantiation,[status(thm)],[57]) ).
cnf(58,plain,
sK19 = sK21,
inference(cnf,[status(esa)],[t21_yellow_6_negated]) ).
cnf(l231,plain,
sK19 = sK21,
inference(instantiation,[status(thm)],[58]) ).
cnf(l1882,plain,
full_subnetstr(sK18,sK16,sK17),
inference(instantiation,[status(thm)],[52]) ).
cnf(l88,plain,
one_sorted_str(sK16),
inference(instantiation,[status(thm)],[48]) ).
cnf(l221,plain,
element(sK22,the_carrier(sK18)),
inference(instantiation,[status(thm)],[57]) ).
cnf(56,plain,
element(sK21,the_carrier(sK18)),
inference(cnf,[status(esa)],[t21_yellow_6_negated]) ).
cnf(l213,plain,
element(sK21,the_carrier(sK18)),
inference(instantiation,[status(thm)],[56]) ).
cnf(l98,plain,
sK19 = sK21,
inference(instantiation,[status(thm)],[58]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l2,l62,l240,l233,l1854,l1884,l261,l216,l921,l246,l82,l961,l226,l947,l248,l122,l235,l77,l89,l130,l236,l110,l1016,l1017,l134,l108,l1175,l158,l231,l1882,l88,l221,l213,l98]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SEU375+1 : TPTP v9.0.0. Released v3.3.0.
% 0.03/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n029.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Tue Jul 22 01:13:34 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.34 % launching worker at depth: 2
% 0.12/0.34 % launching worker at depth: 1
% 0.12/0.34 % launching worker at depth: 3
% 0.12/0.34 % launching worker at depth: 4
% 0.12/0.34 % launching worker at depth: 5
% 0.12/0.34 % launching worker at depth: 6
% 0.12/0.34 % launching worker at depth: 7
% 0.12/0.34 % launching worker at depth: 8
% 0.12/0.34 % launching worker at depth: 9
% 0.12/0.35 % launching worker at depth: 10
% 0.19/0.47 % launching worker at depth: 11
% 17.53/2.55 % launching worker at depth: 12
% 26.57/3.72 % SZS status Theorem for theBenchmark
% 26.57/3.72 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------