%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : LAT292+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 : 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 : Thu Jul 24 10:34:19 PM UTC 2025
% Result : Theorem 0.19s 0.59s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 5
% Syntax : Number of formulae : 49 ( 31 unt; 0 def)
% Number of atoms : 145 ( 3 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 162 ( 66 ~; 56 |; 34 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 1 con; 0-1 aty)
% Number of variables : 14 ( 0 sgn 6 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(t44_lopclset,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& v17_lattices(A)
& ~ v3_realset2(A)
& l3_lattices(A) )
=> ? [B] :
( ~ v3_struct_0(B)
& v2_pre_topc(B)
& l1_pre_topc(B)
& r1_filter_1(A,k6_lopclset(B)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t44_lopclset) ).
fof(t44_lopclset_negated,plain,
~ ! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& v17_lattices(A)
& ~ v3_realset2(A)
& l3_lattices(A) )
=> ? [B] :
( ~ v3_struct_0(B)
& v2_pre_topc(B)
& l1_pre_topc(B)
& r1_filter_1(A,k6_lopclset(B)) ) ),
inference(negate_conjecture,[status(cth)],[t44_lopclset]) ).
cnf(5,plain,
( ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ r1_filter_1(sK1,k6_lopclset(X0))
| v3_struct_0(X0) ),
inference(cnf,[status(esa)],[t44_lopclset_negated]) ).
cnf(l0,plain,
( ~ v2_pre_topc(k11_lopclset(sK1))
| ~ l1_pre_topc(k11_lopclset(sK1))
| ~ r1_filter_1(sK1,k6_lopclset(k11_lopclset(sK1)))
| v3_struct_0(k11_lopclset(sK1)) ),
inference(instantiation,[status(thm)],[5]) ).
fof(dt_k11_lopclset,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& v17_lattices(A)
& ~ v3_realset2(A)
& l3_lattices(A) )
=> ( v1_pre_topc(k11_lopclset(A))
& v2_pre_topc(k11_lopclset(A))
& l1_pre_topc(k11_lopclset(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k11_lopclset) ).
cnf(89,plain,
( ~ v17_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_realset2(X0)
| v2_pre_topc(k11_lopclset(X0))
| v3_struct_0(X0) ),
inference(cnf,[status(esa)],[dt_k11_lopclset]) ).
cnf(l1,plain,
( ~ v17_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_realset2(sK1)
| v2_pre_topc(k11_lopclset(sK1))
| v3_struct_0(sK1) ),
inference(instantiation,[status(thm)],[89]) ).
cnf(0,plain,
~ v3_struct_0(sK1),
inference(cnf,[status(esa)],[t44_lopclset_negated]) ).
cnf(l8,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(4,plain,
l3_lattices(sK1),
inference(cnf,[status(esa)],[t44_lopclset_negated]) ).
cnf(l3,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(1,plain,
v10_lattices(sK1),
inference(cnf,[status(esa)],[t44_lopclset_negated]) ).
cnf(l9,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(3,plain,
~ v3_realset2(sK1),
inference(cnf,[status(esa)],[t44_lopclset_negated]) ).
cnf(l18,plain,
~ v3_realset2(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(90,plain,
( ~ v17_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_realset2(X0)
| l1_pre_topc(k11_lopclset(X0))
| v3_struct_0(X0) ),
inference(cnf,[status(esa)],[dt_k11_lopclset]) ).
cnf(l83,plain,
( ~ v17_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_realset2(sK1)
| l1_pre_topc(k11_lopclset(sK1))
| v3_struct_0(sK1) ),
inference(instantiation,[status(thm)],[90]) ).
cnf(l95,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l155,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(2,plain,
v17_lattices(sK1),
inference(cnf,[status(esa)],[t44_lopclset_negated]) ).
cnf(l2,plain,
v17_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l158,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l153,plain,
~ v3_realset2(sK1),
inference(instantiation,[status(thm)],[3]) ).
fof(d9_lopclset,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& v17_lattices(A)
& ~ v3_realset2(A)
& l3_lattices(A) )
=> k12_lopclset(A) = k6_lopclset(k11_lopclset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d9_lopclset) ).
cnf(83,plain,
( ~ v17_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| k12_lopclset(X0) = k6_lopclset(k11_lopclset(X0))
| v3_realset2(X0)
| v3_struct_0(X0) ),
inference(cnf,[status(esa)],[d9_lopclset]) ).
cnf(l78,plain,
( ~ v17_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| k12_lopclset(sK1) = k6_lopclset(k11_lopclset(sK1))
| v3_realset2(sK1)
| v3_struct_0(sK1) ),
inference(instantiation,[status(thm)],[83]) ).
fof(fc4_lopclset,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& v17_lattices(A)
& ~ v3_realset2(A)
& l3_lattices(A) )
=> ( ~ v3_struct_0(k11_lopclset(A))
& v1_pre_topc(k11_lopclset(A))
& v2_pre_topc(k11_lopclset(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc4_lopclset) ).
cnf(134,plain,
( ~ v17_lattices(X0)
| ~ l3_lattices(X0)
| ~ v3_struct_0(k11_lopclset(X0))
| ~ v10_lattices(X0)
| v3_realset2(X0)
| v3_struct_0(X0) ),
inference(cnf,[status(esa)],[fc4_lopclset]) ).
cnf(l77,plain,
( ~ v17_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ v3_struct_0(k11_lopclset(sK1))
| ~ v10_lattices(sK1)
| v3_realset2(sK1)
| v3_struct_0(sK1) ),
inference(instantiation,[status(thm)],[134]) ).
fof(t43_lopclset,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& v17_lattices(A)
& ~ v3_realset2(A)
& l3_lattices(A) )
=> r1_filter_1(A,k12_lopclset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t43_lopclset) ).
cnf(289,plain,
( ~ v17_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_realset2(X0)
| v3_struct_0(X0)
| r1_filter_1(X0,k12_lopclset(X0)) ),
inference(cnf,[status(esa)],[t43_lopclset]) ).
cnf(l76,plain,
( ~ v17_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_realset2(sK1)
| v3_struct_0(sK1)
| r1_filter_1(sK1,k12_lopclset(sK1)) ),
inference(instantiation,[status(thm)],[289]) ).
cnf(l79,plain,
v17_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l128,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l90,plain,
~ v3_realset2(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(l129,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l99,plain,
v17_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l93,plain,
v17_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l84,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l135,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l130,plain,
~ v3_realset2(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(l86,plain,
v17_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l87,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l81,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l91,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l88,plain,
~ v3_realset2(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(l85,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l82,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l8,l3,l9,l18,l83,l95,l155,l2,l158,l153,l78,l77,l76,l79,l128,l90,l129,l99,l93,l84,l135,l130,l86,l87,l81,l91,l88,l85,l82]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : LAT292+1 : TPTP v9.0.0. Released v3.4.0.
% 0.06/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/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.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Mon Jul 21 00:07:49 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.12/0.35 % launching worker at depth: 6
% 0.12/0.35 % launching worker at depth: 1
% 0.12/0.35 % launching worker at depth: 5
% 0.12/0.35 % launching worker at depth: 2
% 0.12/0.35 % launching worker at depth: 4
% 0.12/0.35 % launching worker at depth: 3
% 0.12/0.35 % launching worker at depth: 7
% 0.12/0.35 % launching worker at depth: 8
% 0.12/0.35 % launching worker at depth: 9
% 0.12/0.38 % launching worker at depth: 10
% 0.19/0.59 % SZS status Theorem for theBenchmark
% 0.19/0.59 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------