%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SEU411+1 : TPTP v9.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n023.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:25 PM UTC 2025
% Result : Theorem 3.66s 0.80s
% Output : CNFRefutation 3.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 9
% Syntax : Number of formulae : 54 ( 33 unt; 0 def)
% Number of atoms : 159 ( 6 equ)
% Maximal formula atoms : 19 ( 2 avg)
% Number of connectives : 162 ( 57 ~; 47 |; 37 &)
% ( 3 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 15 ( 13 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 2 con; 0-2 aty)
% Number of variables : 43 ( 1 sgn 23 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(t20_latsum_1,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v2_orders_2(A)
& v3_orders_2(A)
& v4_orders_2(A)
& v1_yellow_0(A)
& v1_lattice3(A)
& l1_orders_2(A) )
=> ! [B] :
( ( ~ v3_struct_0(B)
& v2_orders_2(B)
& v3_orders_2(B)
& v4_orders_2(B)
& v1_yellow_0(B)
& v1_lattice3(B)
& l1_orders_2(B) )
=> ( ( ~ v1_xboole_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)))
& v1_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)
& v12_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)
& m1_subset_1(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),k1_zfmisc_1(u1_struct_0(B))) )
=> r2_hidden(k3_yellow_0(B),u1_struct_0(A)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t20_latsum_1) ).
fof(t20_latsum_1_negated,plain,
~ ! [A] :
( ( ~ v3_struct_0(A)
& v2_orders_2(A)
& v3_orders_2(A)
& v4_orders_2(A)
& v1_yellow_0(A)
& v1_lattice3(A)
& l1_orders_2(A) )
=> ! [B] :
( ( ~ v3_struct_0(B)
& v2_orders_2(B)
& v3_orders_2(B)
& v4_orders_2(B)
& v1_yellow_0(B)
& v1_lattice3(B)
& l1_orders_2(B) )
=> ( ( ~ v1_xboole_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)))
& v1_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)
& v12_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)
& m1_subset_1(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),k1_zfmisc_1(u1_struct_0(B))) )
=> r2_hidden(k3_yellow_0(B),u1_struct_0(A)) ) ) ),
inference(negate_conjecture,[status(cth)],[t20_latsum_1]) ).
cnf(0,plain,
~ v3_struct_0(sK1),
inference(cnf,[status(esa)],[t20_latsum_1_negated]) ).
cnf(l0,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
fof(t13_latsum_1,plain,
! [A] :
( ( ~ v3_struct_0(A)
& l1_orders_2(A) )
=> ! [B] :
( ( ~ v3_struct_0(B)
& l1_orders_2(B) )
=> ! [C] :
( r2_hidden(C,k3_xboole_0(u1_struct_0(A),u1_struct_0(B)))
=> m1_subset_1(C,u1_struct_0(B)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t13_latsum_1) ).
cnf(59,plain,
( ~ r2_hidden(X0,k3_xboole_0(u1_struct_0(X1),u1_struct_0(X2)))
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X2)
| v3_struct_0(X1)
| v3_struct_0(X2)
| m1_subset_1(X0,u1_struct_0(X2)) ),
inference(cnf,[status(esa)],[t13_latsum_1]) ).
cnf(l1,plain,
( ~ r2_hidden(sK9(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2))),k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)))
| ~ l1_orders_2(sK1)
| ~ l1_orders_2(sK2)
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| m1_subset_1(sK9(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2))),u1_struct_0(sK2)) ),
inference(instantiation,[status(thm)],[59]) ).
fof(d19_waybel_0,plain,
! [A] :
( l1_orders_2(A)
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( v12_waybel_0(B,A)
<=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ! [D] :
( m1_subset_1(D,u1_struct_0(A))
=> ( ( r2_hidden(C,B)
& r1_orders_2(A,D,C) )
=> r2_hidden(D,B) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d19_waybel_0) ).
cnf(21,plain,
( ~ v12_waybel_0(X0,X1)
| ~ r2_hidden(X2,X0)
| ~ l1_orders_2(X1)
| ~ r1_orders_2(X1,X3,X2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| r2_hidden(X3,X0) ),
inference(cnf,[status(esa)],[d19_waybel_0]) ).
cnf(l2,plain,
( ~ v12_waybel_0(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)),sK2)
| ~ r2_hidden(sK9(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2))),k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)))
| ~ l1_orders_2(sK2)
| ~ r1_orders_2(sK2,k3_yellow_0(sK2),sK9(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2))))
| ~ m1_subset_1(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m1_subset_1(sK9(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2))),u1_struct_0(sK2))
| ~ m1_subset_1(k3_yellow_0(sK2),u1_struct_0(sK2))
| r2_hidden(k3_yellow_0(sK2),k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2))) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(17,plain,
m1_subset_1(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)),k1_zfmisc_1(u1_struct_0(sK2))),
inference(cnf,[status(esa)],[t20_latsum_1_negated]) ).
cnf(l44,plain,
m1_subset_1(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)),k1_zfmisc_1(u1_struct_0(sK2))),
inference(instantiation,[status(thm)],[17]) ).
cnf(7,plain,
~ v3_struct_0(sK2),
inference(cnf,[status(esa)],[t20_latsum_1_negated]) ).
cnf(l106,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[7]) ).
cnf(16,plain,
v12_waybel_0(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)),sK2),
inference(cnf,[status(esa)],[t20_latsum_1_negated]) ).
cnf(l11,plain,
v12_waybel_0(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)),sK2),
inference(instantiation,[status(thm)],[16]) ).
fof(t2_subset,plain,
! [A,B] :
( m1_subset_1(A,B)
=> ( v1_xboole_0(B)
| r2_hidden(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_subset) ).
cnf(62,plain,
( ~ m1_subset_1(X0,X1)
| v1_xboole_0(X1)
| r2_hidden(X0,X1) ),
inference(cnf,[status(esa)],[t2_subset]) ).
cnf(l9,plain,
( ~ m1_subset_1(sK9(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2))),k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)))
| v1_xboole_0(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)))
| r2_hidden(sK9(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2))),k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2))) ),
inference(instantiation,[status(thm)],[62]) ).
fof(existence_m1_subset_1,plain,
! [A] :
? [B] : m1_subset_1(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_m1_subset_1) ).
cnf(41,plain,
m1_subset_1(sK9(X0),X0),
inference(cnf,[status(esa)],[existence_m1_subset_1]) ).
cnf(l39,plain,
m1_subset_1(sK9(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2))),k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2))),
inference(instantiation,[status(thm)],[41]) ).
cnf(14,plain,
~ v1_xboole_0(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2))),
inference(cnf,[status(esa)],[t20_latsum_1_negated]) ).
cnf(l40,plain,
~ v1_xboole_0(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2))),
inference(instantiation,[status(thm)],[14]) ).
fof(dt_k3_yellow_0,plain,
! [A] :
( l1_orders_2(A)
=> m1_subset_1(k3_yellow_0(A),u1_struct_0(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k3_yellow_0) ).
cnf(37,plain,
( ~ l1_orders_2(X0)
| m1_subset_1(k3_yellow_0(X0),u1_struct_0(X0)) ),
inference(cnf,[status(esa)],[dt_k3_yellow_0]) ).
cnf(l10,plain,
( ~ l1_orders_2(sK2)
| m1_subset_1(k3_yellow_0(sK2),u1_struct_0(sK2)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(13,plain,
l1_orders_2(sK2),
inference(cnf,[status(esa)],[t20_latsum_1_negated]) ).
cnf(l5,plain,
l1_orders_2(sK2),
inference(instantiation,[status(thm)],[13]) ).
fof(t44_yellow_0,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v4_orders_2(A)
& v1_yellow_0(A)
& l1_orders_2(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> r1_orders_2(A,k3_yellow_0(A),B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t44_yellow_0) ).
cnf(65,plain,
( ~ v4_orders_2(X0)
| ~ v1_yellow_0(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| r1_orders_2(X0,k3_yellow_0(X0),X1) ),
inference(cnf,[status(esa)],[t44_yellow_0]) ).
cnf(l8,plain,
( ~ v4_orders_2(sK2)
| ~ v1_yellow_0(sK2)
| ~ l1_orders_2(sK2)
| ~ m1_subset_1(sK9(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2))),u1_struct_0(sK2))
| v3_struct_0(sK2)
| r1_orders_2(sK2,k3_yellow_0(sK2),sK9(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)))) ),
inference(instantiation,[status(thm)],[65]) ).
cnf(l7,plain,
l1_orders_2(sK2),
inference(instantiation,[status(thm)],[13]) ).
cnf(l66,plain,
l1_orders_2(sK2),
inference(instantiation,[status(thm)],[13]) ).
cnf(11,plain,
v1_yellow_0(sK2),
inference(cnf,[status(esa)],[t20_latsum_1_negated]) ).
cnf(l45,plain,
v1_yellow_0(sK2),
inference(instantiation,[status(thm)],[11]) ).
fof(d3_xboole_0,plain,
! [A,B,C] :
( C = k3_xboole_0(A,B)
<=> ! [D] :
( r2_hidden(D,C)
<=> ( r2_hidden(D,A)
& r2_hidden(D,B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_xboole_0) ).
cnf(30,plain,
( ~ r2_hidden(X0,X1)
| X1 != k3_xboole_0(X2,X3)
| r2_hidden(X0,X3) ),
inference(cnf,[status(esa)],[d3_xboole_0]) ).
cnf(l31,plain,
( ~ r2_hidden(k3_yellow_0(sK2),k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)))
| k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)) != k3_xboole_0(u1_struct_0(sK2),u1_struct_0(sK1))
| r2_hidden(k3_yellow_0(sK2),u1_struct_0(sK1)) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(10,plain,
v4_orders_2(sK2),
inference(cnf,[status(esa)],[t20_latsum_1_negated]) ).
cnf(l13,plain,
v4_orders_2(sK2),
inference(instantiation,[status(thm)],[10]) ).
cnf(l14,plain,
l1_orders_2(sK2),
inference(instantiation,[status(thm)],[13]) ).
fof(commutativity_k3_xboole_0,plain,
! [A,B] : k3_xboole_0(A,B) = k3_xboole_0(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k3_xboole_0) ).
cnf(20,plain,
k3_xboole_0(X0,X1) = k3_xboole_0(X1,X0),
inference(cnf,[status(esa)],[commutativity_k3_xboole_0]) ).
cnf(l42,plain,
k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)) = k3_xboole_0(u1_struct_0(sK2),u1_struct_0(sK1)),
inference(instantiation,[status(thm)],[20]) ).
cnf(6,plain,
l1_orders_2(sK1),
inference(cnf,[status(esa)],[t20_latsum_1_negated]) ).
cnf(l3,plain,
l1_orders_2(sK1),
inference(instantiation,[status(thm)],[6]) ).
cnf(l46,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[7]) ).
cnf(18,plain,
~ r2_hidden(k3_yellow_0(sK2),u1_struct_0(sK1)),
inference(cnf,[status(esa)],[t20_latsum_1_negated]) ).
cnf(l34,plain,
~ r2_hidden(k3_yellow_0(sK2),u1_struct_0(sK1)),
inference(instantiation,[status(thm)],[18]) ).
cnf(l6,plain,
( ~ m1_subset_1(sK9(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2))),k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)))
| v1_xboole_0(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)))
| r2_hidden(sK9(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2))),k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2))) ),
inference(instantiation,[status(thm)],[62]) ).
cnf(l17,plain,
~ v1_xboole_0(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2))),
inference(instantiation,[status(thm)],[14]) ).
cnf(l47,plain,
m1_subset_1(sK9(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2))),k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2))),
inference(instantiation,[status(thm)],[41]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l2,l44,l106,l11,l9,l39,l40,l10,l5,l8,l7,l66,l45,l31,l13,l14,l42,l3,l46,l34,l6,l17,l47]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SEU411+1 : TPTP v9.0.0. Released v3.4.0.
% 0.11/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.34 % Computer : n023.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Tue Jul 22 01:35:04 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.13/0.35 % launching worker at depth: 3
% 0.13/0.35 % launching worker at depth: 1
% 0.13/0.35 % launching worker at depth: 4
% 0.13/0.35 % launching worker at depth: 2
% 0.13/0.35 % launching worker at depth: 5
% 0.13/0.35 % launching worker at depth: 6
% 0.13/0.35 % launching worker at depth: 7
% 0.13/0.35 % launching worker at depth: 8
% 0.13/0.35 % launching worker at depth: 9
% 0.13/0.36 % launching worker at depth: 10
% 0.19/0.49 % launching worker at depth: 11
% 3.66/0.80 % SZS status Theorem for theBenchmark
% 3.66/0.80 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------