%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SEU304+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 : n018.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:08 PM UTC 2025
% Result : Theorem 182.97s 23.40s
% Output : CNFRefutation 182.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 7
% Syntax : Number of formulae : 68 ( 40 unt; 0 def)
% Number of atoms : 179 ( 15 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 182 ( 71 ~; 72 |; 21 &)
% ( 2 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-3 aty)
% Number of variables : 39 ( 0 sgn 22 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(t23_lattices,plain,
! [A] :
( ( ~ empty_carrier(A)
& meet_commutative(A)
& meet_absorbing(A)
& latt_str(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( element(C,the_carrier(A))
=> below(A,meet_commut(A,B,C),B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t23_lattices) ).
fof(t23_lattices_negated,plain,
~ ! [A] :
( ( ~ empty_carrier(A)
& meet_commutative(A)
& meet_absorbing(A)
& latt_str(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( element(C,the_carrier(A))
=> below(A,meet_commut(A,B,C),B) ) ) ),
inference(negate_conjecture,[status(cth)],[t23_lattices]) ).
cnf(50,plain,
~ empty_carrier(sK12),
inference(cnf,[status(esa)],[t23_lattices_negated]) ).
cnf(l0,plain,
~ empty_carrier(sK12),
inference(instantiation,[status(thm)],[50]) ).
fof(d3_lattices,plain,
! [A] :
( ( ~ empty_carrier(A)
& join_semilatt_str(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( element(C,the_carrier(A))
=> ( below(A,B,C)
<=> join(A,B,C) = C ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_lattices) ).
cnf(8,plain,
( join(X0,X1,X2) != X2
| ~ join_semilatt_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| below(X0,X1,X2)
| empty_carrier(X0) ),
inference(cnf,[status(esa)],[d3_lattices]) ).
cnf(l1,plain,
( join(sK12,meet_commut(sK12,sK14,sK13),join(sK12,meet(sK12,sK14,sK13),sK13)) != join(sK12,meet(sK12,sK14,sK13),sK13)
| ~ join_semilatt_str(sK12)
| ~ element(meet_commut(sK12,sK14,sK13),the_carrier(sK12))
| ~ element(join(sK12,meet(sK12,sK14,sK13),sK13),the_carrier(sK12))
| below(sK12,meet_commut(sK12,sK14,sK13),join(sK12,meet(sK12,sK14,sK13),sK13))
| empty_carrier(sK12) ),
inference(instantiation,[status(thm)],[8]) ).
fof(dt_l3_lattices,plain,
! [A] :
( latt_str(A)
=> ( meet_semilatt_str(A)
& join_semilatt_str(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l3_lattices) ).
cnf(20,plain,
( ~ latt_str(X0)
| join_semilatt_str(X0) ),
inference(cnf,[status(esa)],[dt_l3_lattices]) ).
cnf(l8,plain,
( ~ latt_str(sK12)
| join_semilatt_str(sK12) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(53,plain,
latt_str(sK12),
inference(cnf,[status(esa)],[t23_lattices_negated]) ).
cnf(l17,plain,
latt_str(sK12),
inference(instantiation,[status(thm)],[53]) ).
cnf(56,plain,
~ below(sK12,meet_commut(sK12,sK13,sK14),sK13),
inference(cnf,[status(esa)],[t23_lattices_negated]) ).
cnf(l507,plain,
~ below(sK12,meet_commut(sK12,sK13,sK14),sK13),
inference(instantiation,[status(thm)],[56]) ).
fof(dt_k4_lattices,plain,
! [A,B,C] :
( ( ~ empty_carrier(A)
& meet_commutative(A)
& meet_semilatt_str(A)
& element(B,the_carrier(A))
& element(C,the_carrier(A)) )
=> element(meet_commut(A,B,C),the_carrier(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_lattices) ).
cnf(16,plain,
( ~ meet_commutative(X0)
| ~ meet_semilatt_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| empty_carrier(X0)
| element(meet_commut(X0,X1,X2),the_carrier(X0)) ),
inference(cnf,[status(esa)],[dt_k4_lattices]) ).
cnf(l87,plain,
( ~ meet_commutative(sK12)
| ~ meet_semilatt_str(sK12)
| ~ element(sK13,the_carrier(sK12))
| ~ element(sK14,the_carrier(sK12))
| empty_carrier(sK12)
| element(meet_commut(sK12,sK13,sK14),the_carrier(sK12)) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(54,plain,
element(sK13,the_carrier(sK12)),
inference(cnf,[status(esa)],[t23_lattices_negated]) ).
cnf(l549,plain,
element(sK13,the_carrier(sK12)),
inference(instantiation,[status(thm)],[54]) ).
fof(commutativity_k4_lattices,plain,
! [A,B,C] :
( ( ~ empty_carrier(A)
& meet_commutative(A)
& meet_semilatt_str(A)
& element(B,the_carrier(A))
& element(C,the_carrier(A)) )
=> meet_commut(A,B,C) = meet_commut(A,C,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k4_lattices) ).
cnf(4,plain,
( ~ meet_commutative(X0)
| ~ meet_semilatt_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| meet_commut(X0,X1,X2) = meet_commut(X0,X2,X1)
| empty_carrier(X0) ),
inference(cnf,[status(esa)],[commutativity_k4_lattices]) ).
cnf(l227,plain,
( ~ meet_commutative(sK12)
| ~ meet_semilatt_str(sK12)
| ~ element(sK14,the_carrier(sK12))
| ~ element(sK13,the_carrier(sK12))
| meet_commut(sK12,sK14,sK13) = meet_commut(sK12,sK13,sK14)
| empty_carrier(sK12) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(19,plain,
( ~ latt_str(X0)
| meet_semilatt_str(X0) ),
inference(cnf,[status(esa)],[dt_l3_lattices]) ).
cnf(l109,plain,
( ~ latt_str(sK12)
| meet_semilatt_str(sK12) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(51,plain,
meet_commutative(sK12),
inference(cnf,[status(esa)],[t23_lattices_negated]) ).
cnf(l96,plain,
meet_commutative(sK12),
inference(instantiation,[status(thm)],[51]) ).
cnf(l265,plain,
element(sK13,the_carrier(sK12)),
inference(instantiation,[status(thm)],[54]) ).
cnf(l229,plain,
( ~ latt_str(sK12)
| meet_semilatt_str(sK12) ),
inference(instantiation,[status(thm)],[19]) ).
fof(redefinition_k4_lattices,plain,
! [A,B,C] :
( ( ~ empty_carrier(A)
& meet_commutative(A)
& meet_semilatt_str(A)
& element(B,the_carrier(A))
& element(C,the_carrier(A)) )
=> meet_commut(A,B,C) = meet(A,B,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k4_lattices) ).
cnf(45,plain,
( ~ meet_commutative(X0)
| ~ meet_semilatt_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| meet_commut(X0,X1,X2) = meet(X0,X1,X2)
| empty_carrier(X0) ),
inference(cnf,[status(esa)],[redefinition_k4_lattices]) ).
cnf(l7,plain,
( ~ meet_commutative(sK12)
| ~ meet_semilatt_str(sK12)
| ~ element(sK14,the_carrier(sK12))
| ~ element(sK13,the_carrier(sK12))
| meet_commut(sK12,sK14,sK13) = meet(sK12,sK14,sK13)
| empty_carrier(sK12) ),
inference(instantiation,[status(thm)],[45]) ).
fof(d8_lattices,plain,
! [A] :
( ( ~ empty_carrier(A)
& latt_str(A) )
=> ( meet_absorbing(A)
<=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( element(C,the_carrier(A))
=> join(A,meet(A,B,C),C) = C ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_lattices) ).
cnf(9,plain,
( ~ meet_absorbing(X0)
| ~ latt_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| join(X0,meet(X0,X1,X2),X2) = X2
| empty_carrier(X0) ),
inference(cnf,[status(esa)],[d8_lattices]) ).
cnf(l220,plain,
( ~ meet_absorbing(sK12)
| ~ latt_str(sK12)
| ~ element(sK14,the_carrier(sK12))
| ~ element(sK13,the_carrier(sK12))
| join(sK12,meet(sK12,sK14,sK13),sK13) = sK13
| empty_carrier(sK12) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(55,plain,
element(sK14,the_carrier(sK12)),
inference(cnf,[status(esa)],[t23_lattices_negated]) ).
cnf(l268,plain,
element(sK14,the_carrier(sK12)),
inference(instantiation,[status(thm)],[55]) ).
cnf(l1460,plain,
( ~ meet_absorbing(sK12)
| ~ latt_str(sK12)
| ~ element(sK14,the_carrier(sK12))
| ~ element(sK13,the_carrier(sK12))
| join(sK12,meet(sK12,sK14,sK13),sK13) = sK13
| empty_carrier(sK12) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l224,plain,
element(sK14,the_carrier(sK12)),
inference(instantiation,[status(thm)],[55]) ).
cnf(l230,plain,
meet_commutative(sK12),
inference(instantiation,[status(thm)],[51]) ).
cnf(l236,plain,
latt_str(sK12),
inference(instantiation,[status(thm)],[53]) ).
cnf(52,plain,
meet_absorbing(sK12),
inference(cnf,[status(esa)],[t23_lattices_negated]) ).
cnf(l221,plain,
meet_absorbing(sK12),
inference(instantiation,[status(thm)],[52]) ).
cnf(l735,plain,
element(sK14,the_carrier(sK12)),
inference(instantiation,[status(thm)],[55]) ).
cnf(l110,plain,
latt_str(sK12),
inference(instantiation,[status(thm)],[53]) ).
cnf(l461,plain,
latt_str(sK12),
inference(instantiation,[status(thm)],[53]) ).
cnf(l1211,plain,
element(sK14,the_carrier(sK12)),
inference(instantiation,[status(thm)],[55]) ).
cnf(l6,plain,
( ~ meet_commutative(sK12)
| ~ meet_semilatt_str(sK12)
| ~ element(sK13,the_carrier(sK12))
| ~ element(sK14,the_carrier(sK12))
| meet_commut(sK12,sK13,sK14) = meet_commut(sK12,sK14,sK13)
| empty_carrier(sK12) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1503,plain,
element(sK14,the_carrier(sK12)),
inference(instantiation,[status(thm)],[55]) ).
cnf(l530,plain,
element(sK13,the_carrier(sK12)),
inference(instantiation,[status(thm)],[54]) ).
cnf(l16,plain,
( ~ latt_str(sK12)
| meet_semilatt_str(sK12) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l24,plain,
meet_commutative(sK12),
inference(instantiation,[status(thm)],[51]) ).
cnf(l10,plain,
meet_commutative(sK12),
inference(instantiation,[status(thm)],[51]) ).
cnf(l1214,plain,
element(sK13,the_carrier(sK12)),
inference(instantiation,[status(thm)],[54]) ).
cnf(l15,plain,
( ~ latt_str(sK12)
| meet_semilatt_str(sK12) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1491,plain,
element(sK13,the_carrier(sK12)),
inference(instantiation,[status(thm)],[54]) ).
cnf(l53,plain,
element(sK13,the_carrier(sK12)),
inference(instantiation,[status(thm)],[54]) ).
cnf(l129,plain,
element(sK14,the_carrier(sK12)),
inference(instantiation,[status(thm)],[55]) ).
cnf(l1476,plain,
latt_str(sK12),
inference(instantiation,[status(thm)],[53]) ).
cnf(l1465,plain,
meet_absorbing(sK12),
inference(instantiation,[status(thm)],[52]) ).
cnf(l23,plain,
latt_str(sK12),
inference(instantiation,[status(thm)],[53]) ).
cnf(l83,plain,
element(sK13,the_carrier(sK12)),
inference(instantiation,[status(thm)],[54]) ).
cnf(l47,plain,
latt_str(sK12),
inference(instantiation,[status(thm)],[53]) ).
cnf(l141,plain,
( ~ meet_absorbing(sK12)
| ~ latt_str(sK12)
| ~ element(sK14,the_carrier(sK12))
| ~ element(sK13,the_carrier(sK12))
| join(sK12,meet(sK12,sK14,sK13),sK13) = sK13
| empty_carrier(sK12) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l282,plain,
element(sK14,the_carrier(sK12)),
inference(instantiation,[status(thm)],[55]) ).
cnf(l152,plain,
latt_str(sK12),
inference(instantiation,[status(thm)],[53]) ).
cnf(l154,plain,
meet_absorbing(sK12),
inference(instantiation,[status(thm)],[52]) ).
cnf(l284,plain,
element(sK13,the_carrier(sK12)),
inference(instantiation,[status(thm)],[54]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l8,l17,l507,l87,l549,l227,l109,l96,l265,l229,l7,l220,l268,l1460,l224,l230,l236,l221,l735,l110,l461,l1211,l6,l1503,l530,l16,l24,l10,l1214,l15,l1491,l53,l129,l1476,l1465,l23,l83,l47,l141,l282,l152,l154,l284]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SEU304+1 : TPTP v9.0.0. Released v3.3.0.
% 0.12/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n018.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 00:41:04 EDT 2025
% 0.19/0.33 % CPUTime :
% 0.19/0.34 % launching worker at depth: 2
% 0.19/0.34 % launching worker at depth: 3
% 0.19/0.34 % launching worker at depth: 1
% 0.19/0.34 % launching worker at depth: 4
% 0.19/0.34 % launching worker at depth: 5
% 0.19/0.34 % launching worker at depth: 6
% 0.19/0.34 % launching worker at depth: 7
% 0.19/0.34 % launching worker at depth: 8
% 0.19/0.34 % launching worker at depth: 9
% 0.19/0.36 % launching worker at depth: 10
% 0.19/0.52 % launching worker at depth: 11
% 13.25/2.07 % launching worker at depth: 12
% 182.97/23.40 % SZS status Theorem for theBenchmark
% 182.97/23.40 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------