%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SEU387+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 : n024.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:21 PM UTC 2025
% Result : Theorem 2.37s 0.72s
% Output : CNFRefutation 2.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 11
% Syntax : Number of formulae : 49 ( 30 unt; 0 def)
% Number of atoms : 154 ( 6 equ)
% Maximal formula atoms : 18 ( 3 avg)
% Number of connectives : 151 ( 46 ~; 31 |; 64 &)
% ( 1 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 28 ( 26 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-1 aty)
% Number of variables : 33 ( 7 sgn 19 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(t2_yellow19,plain,
! [A] :
( ~ empty(A)
=> ! [B] :
( ( ~ empty(B)
& filtered_subset(B,boole_POSet(A))
& upper_relstr_subset(B,boole_POSet(A))
& proper_element(B,powerset(the_carrier(boole_POSet(A))))
& element(B,powerset(the_carrier(boole_POSet(A)))) )
=> ! [C] :
~ ( in(C,B)
& empty(C) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_yellow19) ).
fof(t2_yellow19_negated,plain,
~ ! [A] :
( ~ empty(A)
=> ! [B] :
( ( ~ empty(B)
& filtered_subset(B,boole_POSet(A))
& upper_relstr_subset(B,boole_POSet(A))
& proper_element(B,powerset(the_carrier(boole_POSet(A))))
& element(B,powerset(the_carrier(boole_POSet(A)))) )
=> ! [C] :
~ ( in(C,B)
& empty(C) ) ) ),
inference(negate_conjecture,[status(cth)],[t2_yellow19]) ).
cnf(244,plain,
~ empty(sK29),
inference(cnf,[status(esa)],[t2_yellow19_negated]) ).
cnf(l0,plain,
~ empty(sK29),
inference(instantiation,[status(thm)],[244]) ).
fof(t2_subset,plain,
! [A,B] :
( element(A,B)
=> ( empty(B)
| in(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
cnf(242,plain,
( ~ element(X0,X1)
| in(X0,X1)
| empty(X1) ),
inference(cnf,[status(esa)],[t2_subset]) ).
cnf(l1,plain,
( ~ element(empty_set,sK29)
| in(empty_set,sK29)
| empty(sK29) ),
inference(instantiation,[status(thm)],[242]) ).
fof(t1_subset,plain,
! [A,B] :
( in(A,B)
=> element(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
cnf(241,plain,
( ~ in(X0,X1)
| element(X0,X1) ),
inference(cnf,[status(esa)],[t1_subset]) ).
cnf(l5,plain,
( ~ in(sK30,sK29)
| element(sK30,sK29) ),
inference(instantiation,[status(thm)],[241]) ).
cnf(249,plain,
in(sK30,sK29),
inference(cnf,[status(esa)],[t2_yellow19_negated]) ).
cnf(l17,plain,
in(sK30,sK29),
inference(instantiation,[status(thm)],[249]) ).
fof(t6_boole,plain,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_boole) ).
cnf(255,plain,
( ~ empty(X0)
| X0 = empty_set ),
inference(cnf,[status(esa)],[t6_boole]) ).
cnf(l3,plain,
( ~ empty(sK30)
| sK30 = empty_set ),
inference(instantiation,[status(thm)],[255]) ).
cnf(250,plain,
empty(sK30),
inference(cnf,[status(esa)],[t2_yellow19_negated]) ).
cnf(l51,plain,
empty(sK30),
inference(instantiation,[status(thm)],[250]) ).
fof(t18_yellow_1,plain,
! [A] : bottom_of_relstr(boole_POSet(A)) = empty_set,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t18_yellow_1) ).
cnf(240,plain,
bottom_of_relstr(boole_POSet(X0)) = empty_set,
inference(cnf,[status(esa)],[t18_yellow_1]) ).
cnf(l278,plain,
bottom_of_relstr(boole_POSet(sK28)) = empty_set,
inference(instantiation,[status(thm)],[240]) ).
fof(t8_waybel_7,plain,
! [A] :
( ( ~ empty_carrier(A)
& reflexive_relstr(A)
& transitive_relstr(A)
& antisymmetric_relstr(A)
& lower_bounded_relstr(A)
& rel_str(A) )
=> ! [B] :
( ( ~ empty(B)
& filtered_subset(B,A)
& upper_relstr_subset(B,A)
& element(B,powerset(the_carrier(A))) )
=> ( proper_element(B,powerset(the_carrier(A)))
<=> ~ in(bottom_of_relstr(A),B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_waybel_7) ).
cnf(258,plain,
( ~ element(X0,powerset(the_carrier(X1)))
| ~ rel_str(X1)
| ~ in(bottom_of_relstr(X1),X0)
| ~ antisymmetric_relstr(X1)
| ~ reflexive_relstr(X1)
| ~ lower_bounded_relstr(X1)
| ~ transitive_relstr(X1)
| ~ upper_relstr_subset(X0,X1)
| ~ filtered_subset(X0,X1)
| ~ proper_element(X0,powerset(the_carrier(X1)))
| empty_carrier(X1)
| empty(X0) ),
inference(cnf,[status(esa)],[t8_waybel_7]) ).
cnf(l331,plain,
( ~ element(sK29,powerset(the_carrier(boole_POSet(sK28))))
| ~ rel_str(boole_POSet(sK28))
| ~ in(bottom_of_relstr(boole_POSet(sK28)),sK29)
| ~ antisymmetric_relstr(boole_POSet(sK28))
| ~ reflexive_relstr(boole_POSet(sK28))
| ~ lower_bounded_relstr(boole_POSet(sK28))
| ~ transitive_relstr(boole_POSet(sK28))
| ~ upper_relstr_subset(sK29,boole_POSet(sK28))
| ~ filtered_subset(sK29,boole_POSet(sK28))
| ~ proper_element(sK29,powerset(the_carrier(boole_POSet(sK28))))
| empty_carrier(boole_POSet(sK28))
| empty(sK29) ),
inference(instantiation,[status(thm)],[258]) ).
fof(dt_k3_yellow_1,plain,
! [A] :
( strict_rel_str(boole_POSet(A))
& rel_str(boole_POSet(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_yellow_1) ).
cnf(33,plain,
rel_str(boole_POSet(X0)),
inference(cnf,[status(esa)],[dt_k3_yellow_1]) ).
cnf(l355,plain,
rel_str(boole_POSet(sK28)),
inference(instantiation,[status(thm)],[33]) ).
cnf(246,plain,
upper_relstr_subset(sK29,boole_POSet(sK28)),
inference(cnf,[status(esa)],[t2_yellow19_negated]) ).
cnf(l382,plain,
upper_relstr_subset(sK29,boole_POSet(sK28)),
inference(instantiation,[status(thm)],[246]) ).
cnf(247,plain,
proper_element(sK29,powerset(the_carrier(boole_POSet(sK28)))),
inference(cnf,[status(esa)],[t2_yellow19_negated]) ).
cnf(l383,plain,
proper_element(sK29,powerset(the_carrier(boole_POSet(sK28)))),
inference(instantiation,[status(thm)],[247]) ).
fof(fc1_waybel_7,plain,
! [A] :
( ~ empty_carrier(boole_POSet(A))
& strict_rel_str(boole_POSet(A))
& reflexive_relstr(boole_POSet(A))
& transitive_relstr(boole_POSet(A))
& antisymmetric_relstr(boole_POSet(A))
& lower_bounded_relstr(boole_POSet(A))
& upper_bounded_relstr(boole_POSet(A))
& bounded_relstr(boole_POSet(A))
& up_complete_relstr(boole_POSet(A))
& join_complete_relstr(boole_POSet(A))
& ~ v1_yellow_3(boole_POSet(A))
& distributive_relstr(boole_POSet(A))
& heyting_relstr(boole_POSet(A))
& complemented_relstr(boole_POSet(A))
& boolean_relstr(boole_POSet(A))
& with_suprema_relstr(boole_POSet(A))
& with_infima_relstr(boole_POSet(A))
& complete_relstr(boole_POSet(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_waybel_7) ).
cnf(52,plain,
antisymmetric_relstr(boole_POSet(X0)),
inference(cnf,[status(esa)],[fc1_waybel_7]) ).
cnf(l378,plain,
antisymmetric_relstr(boole_POSet(sK28)),
inference(instantiation,[status(thm)],[52]) ).
fof(fc7_yellow_1,plain,
! [A] :
( ~ empty_carrier(boole_POSet(A))
& strict_rel_str(boole_POSet(A))
& reflexive_relstr(boole_POSet(A))
& transitive_relstr(boole_POSet(A))
& antisymmetric_relstr(boole_POSet(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc7_yellow_1) ).
cnf(88,plain,
~ empty_carrier(boole_POSet(X0)),
inference(cnf,[status(esa)],[fc7_yellow_1]) ).
cnf(l379,plain,
~ empty_carrier(boole_POSet(sK28)),
inference(instantiation,[status(thm)],[88]) ).
fof(fc8_yellow_6,plain,
! [A] :
( ~ empty_carrier(boole_POSet(A))
& strict_rel_str(boole_POSet(A))
& reflexive_relstr(boole_POSet(A))
& transitive_relstr(boole_POSet(A))
& antisymmetric_relstr(boole_POSet(A))
& lower_bounded_relstr(boole_POSet(A))
& upper_bounded_relstr(boole_POSet(A))
& bounded_relstr(boole_POSet(A))
& directed_relstr(boole_POSet(A))
& up_complete_relstr(boole_POSet(A))
& join_complete_relstr(boole_POSet(A))
& ~ v1_yellow_3(boole_POSet(A))
& with_suprema_relstr(boole_POSet(A))
& with_infima_relstr(boole_POSet(A))
& complete_relstr(boole_POSet(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc8_yellow_6) ).
cnf(106,plain,
reflexive_relstr(boole_POSet(X0)),
inference(cnf,[status(esa)],[fc8_yellow_6]) ).
cnf(l381,plain,
reflexive_relstr(boole_POSet(sK28)),
inference(instantiation,[status(thm)],[106]) ).
cnf(248,plain,
element(sK29,powerset(the_carrier(boole_POSet(sK28)))),
inference(cnf,[status(esa)],[t2_yellow19_negated]) ).
cnf(l358,plain,
element(sK29,powerset(the_carrier(boole_POSet(sK28)))),
inference(instantiation,[status(thm)],[248]) ).
cnf(53,plain,
lower_bounded_relstr(boole_POSet(X0)),
inference(cnf,[status(esa)],[fc1_waybel_7]) ).
cnf(l385,plain,
lower_bounded_relstr(boole_POSet(sK28)),
inference(instantiation,[status(thm)],[53]) ).
cnf(245,plain,
filtered_subset(sK29,boole_POSet(sK28)),
inference(cnf,[status(esa)],[t2_yellow19_negated]) ).
cnf(l384,plain,
filtered_subset(sK29,boole_POSet(sK28)),
inference(instantiation,[status(thm)],[245]) ).
fof(fc8_yellow_1,plain,
! [A] :
( ~ empty_carrier(boole_POSet(A))
& strict_rel_str(boole_POSet(A))
& reflexive_relstr(boole_POSet(A))
& transitive_relstr(boole_POSet(A))
& antisymmetric_relstr(boole_POSet(A))
& lower_bounded_relstr(boole_POSet(A))
& upper_bounded_relstr(boole_POSet(A))
& bounded_relstr(boole_POSet(A))
& with_suprema_relstr(boole_POSet(A))
& with_infima_relstr(boole_POSet(A))
& complete_relstr(boole_POSet(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc8_yellow_1) ).
cnf(96,plain,
transitive_relstr(boole_POSet(X0)),
inference(cnf,[status(esa)],[fc8_yellow_1]) ).
cnf(l380,plain,
transitive_relstr(boole_POSet(sK28)),
inference(instantiation,[status(thm)],[96]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l5,l17,l3,l51,l278,l331,l355,l382,l383,l378,l379,l381,l358,l385,l384,l380]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SEU387+1 : TPTP v9.0.0. Released v3.3.0.
% 0.11/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.34 % Computer : n024.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % 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 : Tue Jul 22 01:19:34 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.12/0.35 % launching worker at depth: 1
% 0.12/0.35 % launching worker at depth: 6
% 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: 4
% 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: 3
% 0.12/0.35 % launching worker at depth: 9
% 0.12/0.37 % launching worker at depth: 10
% 0.19/0.53 % launching worker at depth: 11
% 2.37/0.72 % SZS status Theorem for theBenchmark
% 2.37/0.72 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------