%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SEU114+1 : TPTP v9.0.0. Released v3.2.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 : Fri Jul 25 03:44:30 PM UTC 2025
% Result : Theorem 179.05s 22.84s
% Output : CNFRefutation 179.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 13
% Syntax : Number of formulae : 88 ( 31 unt; 0 def)
% Number of atoms : 196 ( 24 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 189 ( 81 ~; 84 |; 10 &)
% ( 5 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 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-2 aty)
% Number of variables : 65 ( 6 sgn 25 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(t27_finsub_1,plain,
! [A] :
( finite(A)
=> finite_subsets(A) = powerset(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t27_finsub_1) ).
fof(t27_finsub_1_negated,plain,
~ ! [A] :
( finite(A)
=> finite_subsets(A) = powerset(A) ),
inference(negate_conjecture,[status(cth)],[t27_finsub_1]) ).
cnf(66,plain,
finite(sK13),
inference(cnf,[status(esa)],[t27_finsub_1_negated]) ).
cnf(l0,plain,
finite(sK13),
inference(instantiation,[status(thm)],[66]) ).
fof(cc2_finset_1,plain,
! [A] :
( finite(A)
=> ! [B] :
( element(B,powerset(A))
=> finite(B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc2_finset_1) ).
cnf(4,plain,
( ~ finite(X0)
| ~ element(X1,powerset(X0))
| finite(X1) ),
inference(cnf,[status(esa)],[cc2_finset_1]) ).
cnf(l1,plain,
( ~ finite(sK13)
| ~ element(sK2(sK13,powerset(sK13)),powerset(sK13))
| finite(sK2(sK13,powerset(sK13))) ),
inference(instantiation,[status(thm)],[4]) ).
fof(d5_finsub_1,plain,
! [A,B] :
( preboolean(B)
=> ( B = finite_subsets(A)
<=> ! [C] :
( in(C,B)
<=> ( subset(C,A)
& finite(C) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_finsub_1) ).
cnf(17,plain,
( ~ finite(sK2(X0,X1))
| ~ preboolean(X1)
| ~ subset(sK2(X0,X1),X0)
| X1 = finite_subsets(X0)
| sP0(X1,X0) ),
inference(cnf,[status(esa)],[d5_finsub_1]) ).
cnf(l12,plain,
( ~ finite(sK2(sK13,powerset(sK13)))
| ~ preboolean(powerset(sK13))
| ~ subset(sK2(sK13,powerset(sK13)),sK13)
| powerset(sK13) = finite_subsets(sK13)
| sP0(powerset(sK13),sK13) ),
inference(instantiation,[status(thm)],[17]) ).
fof(fc1_finsub_1,plain,
! [A] :
( ~ empty(powerset(A))
& cup_closed(powerset(A))
& diff_closed(powerset(A))
& preboolean(powerset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_finsub_1) ).
cnf(26,plain,
preboolean(powerset(X0)),
inference(cnf,[status(esa)],[fc1_finsub_1]) ).
cnf(l126,plain,
preboolean(powerset(sK13)),
inference(instantiation,[status(thm)],[26]) ).
fof(t4_subset,plain,
! [A,B,C] :
( ( in(A,B)
& element(B,powerset(C)) )
=> element(A,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_subset) ).
cnf(71,plain,
( ~ in(X0,X1)
| ~ element(X1,powerset(X2))
| element(X0,X2) ),
inference(cnf,[status(esa)],[t4_subset]) ).
cnf(l2,plain,
( ~ in(sK2(sK13,powerset(sK13)),finite_subsets(sK13))
| ~ element(finite_subsets(sK13),powerset(powerset(sK13)))
| element(sK2(sK13,powerset(sK13)),powerset(sK13)) ),
inference(instantiation,[status(thm)],[71]) ).
cnf(20,plain,
( subset(sK2(X0,X1),X0)
| ~ sP0(X1,X0) ),
inference(cnf,[status(esa)],[d5_finsub_1]) ).
cnf(l503,plain,
( subset(sK2(sK13,powerset(sK13)),sK13)
| ~ sP0(powerset(sK13),sK13) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(13,plain,
( ~ in(X0,X1)
| ~ preboolean(X1)
| X1 != finite_subsets(X2)
| subset(X0,X2) ),
inference(cnf,[status(esa)],[d5_finsub_1]) ).
cnf(l121,plain,
( ~ in(sK2(sK13,powerset(sK13)),powerset(sK13))
| ~ preboolean(powerset(sK13))
| powerset(sK13) != finite_subsets(sK13)
| subset(sK2(sK13,powerset(sK13)),sK13) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(16,plain,
( ~ preboolean(X0)
| in(sK2(X1,X0),X0)
| X0 = finite_subsets(X1)
| sP0(X0,X1) ),
inference(cnf,[status(esa)],[d5_finsub_1]) ).
cnf(l124,plain,
( ~ preboolean(powerset(sK13))
| in(sK2(sK13,powerset(sK13)),powerset(sK13))
| powerset(sK13) = finite_subsets(sK13)
| sP0(powerset(sK13),sK13) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l625,plain,
( subset(sK2(sK13,powerset(sK13)),sK13)
| ~ sP0(powerset(sK13),sK13) ),
inference(instantiation,[status(thm)],[20]) ).
fof(cc2_finsub_1,plain,
! [A] :
( ( cup_closed(A)
& diff_closed(A) )
=> preboolean(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc2_finsub_1) ).
cnf(5,plain,
( ~ cup_closed(X0)
| ~ diff_closed(X0)
| preboolean(X0) ),
inference(cnf,[status(esa)],[cc2_finsub_1]) ).
cnf(l125,plain,
( ~ cup_closed(powerset(sK13))
| ~ diff_closed(powerset(sK13))
| preboolean(powerset(sK13)) ),
inference(instantiation,[status(thm)],[5]) ).
fof(t3_subset,plain,
! [A,B] :
( element(A,powerset(B))
<=> subset(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_subset) ).
cnf(69,plain,
( ~ element(X0,powerset(X1))
| subset(X0,X1) ),
inference(cnf,[status(esa)],[t3_subset]) ).
cnf(l544,plain,
( ~ element(finite_subsets(sK13),powerset(powerset(sK13)))
| subset(finite_subsets(sK13),powerset(sK13)) ),
inference(instantiation,[status(thm)],[69]) ).
cnf(l386,plain,
preboolean(powerset(sK13)),
inference(instantiation,[status(thm)],[26]) ).
fof(d10_xboole_0,plain,
! [A,B] :
( A = B
<=> ( subset(A,B)
& subset(B,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_xboole_0) ).
cnf(9,plain,
( ~ subset(X0,X1)
| ~ subset(X1,X0)
| X0 = X1 ),
inference(cnf,[status(esa)],[d10_xboole_0]) ).
cnf(l509,plain,
( ~ subset(powerset(finite_subsets(sK13)),powerset(powerset(sK13)))
| ~ subset(powerset(powerset(sK13)),powerset(finite_subsets(sK13)))
| powerset(finite_subsets(sK13)) = powerset(powerset(sK13)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(15,plain,
( ~ finite(X0)
| ~ preboolean(X1)
| ~ subset(X0,X2)
| X1 != finite_subsets(X2)
| in(X0,X1) ),
inference(cnf,[status(esa)],[d5_finsub_1]) ).
cnf(l512,plain,
( ~ finite(sK2(sK13,powerset(sK13)))
| ~ preboolean(finite_subsets(sK13))
| ~ subset(sK2(sK13,powerset(sK13)),sK13)
| finite_subsets(sK13) != finite_subsets(sK13)
| in(sK2(sK13,powerset(sK13)),finite_subsets(sK13)) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(67,plain,
finite_subsets(sK13) != powerset(sK13),
inference(cnf,[status(esa)],[t27_finsub_1_negated]) ).
cnf(l579,plain,
finite_subsets(sK13) != powerset(sK13),
inference(instantiation,[status(thm)],[67]) ).
cnf(l384,plain,
( ~ preboolean(powerset(sK13))
| in(sK2(sK13,powerset(sK13)),powerset(sK13))
| powerset(sK13) = finite_subsets(sK13)
| sP0(powerset(sK13),sK13) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l697,plain,
( subset(sK2(sK13,powerset(sK13)),sK13)
| ~ sP0(powerset(sK13),sK13) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(70,plain,
( ~ subset(X0,X1)
| element(X0,powerset(X1)) ),
inference(cnf,[status(esa)],[t3_subset]) ).
cnf(l1234,plain,
( ~ subset(powerset(sK13),powerset(sK13))
| element(powerset(sK13),powerset(powerset(sK13))) ),
inference(instantiation,[status(thm)],[70]) ).
cnf(25,plain,
diff_closed(powerset(X0)),
inference(cnf,[status(esa)],[fc1_finsub_1]) ).
cnf(l501,plain,
diff_closed(powerset(sK13)),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1242,plain,
( ~ subset(finite_subsets(sK13),powerset(sK13))
| ~ subset(powerset(sK13),finite_subsets(sK13))
| finite_subsets(sK13) = powerset(sK13) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(7,plain,
( X0 != X1
| subset(X0,X1) ),
inference(cnf,[status(esa)],[d10_xboole_0]) ).
cnf(l1263,plain,
( powerset(sK13) != finite_subsets(sK13)
| subset(powerset(sK13),finite_subsets(sK13)) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(24,plain,
cup_closed(powerset(X0)),
inference(cnf,[status(esa)],[fc1_finsub_1]) ).
cnf(l138,plain,
cup_closed(powerset(sK13)),
inference(instantiation,[status(thm)],[24]) ).
fof(reflexivity_r1_tarski,plain,
! [A,B] : subset(A,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
cnf(62,plain,
subset(X0,X0),
inference(cnf,[status(esa)],[reflexivity_r1_tarski]) ).
cnf(l1250,plain,
subset(powerset(sK13),powerset(sK13)),
inference(instantiation,[status(thm)],[62]) ).
cnf(l1267,plain,
finite_subsets(sK13) != powerset(sK13),
inference(instantiation,[status(thm)],[67]) ).
cnf(l546,plain,
subset(powerset(powerset(sK13)),powerset(powerset(sK13))),
inference(instantiation,[status(thm)],[62]) ).
cnf(l950,plain,
( ~ preboolean(powerset(sK13))
| in(sK2(sK13,powerset(sK13)),powerset(sK13))
| powerset(sK13) = finite_subsets(sK13)
| sP0(powerset(sK13),sK13) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l1325,plain,
( ~ preboolean(powerset(sK13))
| in(sK2(sK13,powerset(sK13)),powerset(sK13))
| powerset(sK13) = finite_subsets(sK13)
| sP0(powerset(sK13),sK13) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l1327,plain,
preboolean(powerset(sK13)),
inference(instantiation,[status(thm)],[26]) ).
cnf(l1312,plain,
( subset(sK2(sK13,powerset(sK13)),sK13)
| ~ sP0(powerset(sK13),sK13) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l401,plain,
preboolean(powerset(sK13)),
inference(instantiation,[status(thm)],[26]) ).
cnf(l517,plain,
( ~ cup_closed(finite_subsets(sK13))
| ~ diff_closed(finite_subsets(sK13))
| preboolean(finite_subsets(sK13)) ),
inference(instantiation,[status(thm)],[5]) ).
fof(fc2_finsub_1,plain,
! [A] :
( ~ empty(finite_subsets(A))
& cup_closed(finite_subsets(A))
& diff_closed(finite_subsets(A))
& preboolean(finite_subsets(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_finsub_1) ).
cnf(31,plain,
diff_closed(finite_subsets(X0)),
inference(cnf,[status(esa)],[fc2_finsub_1]) ).
cnf(l518,plain,
diff_closed(finite_subsets(sK13)),
inference(instantiation,[status(thm)],[31]) ).
cnf(l1094,plain,
( ~ cup_closed(powerset(sK13))
| ~ diff_closed(powerset(sK13))
| preboolean(powerset(sK13)) ),
inference(instantiation,[status(thm)],[5]) ).
fof(t1_subset,plain,
! [A,B] :
( in(A,B)
=> element(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_subset) ).
cnf(64,plain,
( ~ in(X0,X1)
| element(X0,X1) ),
inference(cnf,[status(esa)],[t1_subset]) ).
cnf(l385,plain,
( ~ in(sK2(sK13,powerset(sK13)),powerset(sK13))
| element(sK2(sK13,powerset(sK13)),powerset(sK13)) ),
inference(instantiation,[status(thm)],[64]) ).
cnf(l582,plain,
( ~ element(sK2(sK13,powerset(sK13)),powerset(sK13))
| subset(sK2(sK13,powerset(sK13)),sK13) ),
inference(instantiation,[status(thm)],[69]) ).
cnf(l1095,plain,
cup_closed(powerset(sK13)),
inference(instantiation,[status(thm)],[24]) ).
cnf(l1123,plain,
diff_closed(powerset(sK13)),
inference(instantiation,[status(thm)],[25]) ).
fof(d3_tarski,plain,
! [A,B] :
( subset(A,B)
<=> ! [C] :
( in(C,A)
=> in(C,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_tarski) ).
cnf(10,plain,
( ~ in(X0,X1)
| ~ subset(X1,X2)
| in(X0,X2) ),
inference(cnf,[status(esa)],[d3_tarski]) ).
cnf(l1310,plain,
( ~ in(sK2(sK13,powerset(sK13)),finite_subsets(sK13))
| ~ subset(finite_subsets(sK13),powerset(sK13))
| in(sK2(sK13,powerset(sK13)),powerset(sK13)) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l612,plain,
subset(powerset(powerset(sK13)),powerset(powerset(sK13))),
inference(instantiation,[status(thm)],[62]) ).
fof(t26_finsub_1,plain,
! [A] : subset(finite_subsets(A),powerset(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t26_finsub_1) ).
cnf(65,plain,
subset(finite_subsets(X0),powerset(X0)),
inference(cnf,[status(esa)],[t26_finsub_1]) ).
cnf(l1311,plain,
subset(finite_subsets(sK13),powerset(sK13)),
inference(instantiation,[status(thm)],[65]) ).
cnf(l1314,plain,
( ~ subset(sK2(sK13,powerset(sK13)),sK13)
| element(sK2(sK13,powerset(sK13)),powerset(sK13)) ),
inference(instantiation,[status(thm)],[70]) ).
cnf(l1328,plain,
( subset(sK2(sK13,powerset(sK13)),sK13)
| ~ sP0(powerset(sK13),sK13) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(30,plain,
cup_closed(finite_subsets(X0)),
inference(cnf,[status(esa)],[fc2_finsub_1]) ).
cnf(l678,plain,
cup_closed(finite_subsets(sK13)),
inference(instantiation,[status(thm)],[30]) ).
cnf(l1382,plain,
finite_subsets(sK13) != powerset(sK13),
inference(instantiation,[status(thm)],[67]) ).
cnf(l1096,plain,
( ~ in(sK2(sK13,powerset(sK13)),powerset(sK13))
| element(sK2(sK13,powerset(sK13)),powerset(sK13)) ),
inference(instantiation,[status(thm)],[64]) ).
cnf(l1507,plain,
( ~ subset(sK2(sK13,powerset(sK13)),sK13)
| element(sK2(sK13,powerset(sK13)),powerset(sK13)) ),
inference(instantiation,[status(thm)],[70]) ).
cnf(18,plain,
( ~ in(sK2(X0,X1),X1)
| ~ sP0(X1,X0) ),
inference(cnf,[status(esa)],[d5_finsub_1]) ).
cnf(l1408,plain,
( ~ in(sK2(sK13,powerset(sK13)),powerset(sK13))
| ~ sP0(powerset(sK13),sK13) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l947,plain,
( ~ subset(finite_subsets(sK13),powerset(sK13))
| element(finite_subsets(sK13),powerset(powerset(sK13))) ),
inference(instantiation,[status(thm)],[70]) ).
cnf(l948,plain,
subset(finite_subsets(sK13),powerset(sK13)),
inference(instantiation,[status(thm)],[65]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l12,l126,l2,l503,l121,l124,l625,l125,l544,l386,l509,l512,l579,l384,l697,l1234,l501,l1242,l1263,l138,l1250,l1267,l546,l950,l1325,l1327,l1312,l401,l517,l518,l1094,l385,l582,l1095,l1123,l1310,l612,l1311,l1314,l1328,l678,l1382,l1096,l1507,l1408,l947,l948]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.08 % Problem : SEU114+1 : TPTP v9.0.0. Released v3.2.0.
% 0.00/0.09 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.29 % Computer : n029.cluster.edu
% 0.08/0.29 % Model : x86_64 x86_64
% 0.08/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.29 % Memory : 8042.1875MB
% 0.08/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.29 % CPULimit : 300
% 0.08/0.29 % WCLimit : 300
% 0.08/0.29 % DateTime : Mon Jul 21 23:30:34 EDT 2025
% 0.08/0.29 % CPUTime :
% 0.08/0.29 % launching worker at depth: 3
% 0.08/0.29 % launching worker at depth: 4
% 0.08/0.29 % launching worker at depth: 2
% 0.08/0.29 % launching worker at depth: 5
% 0.08/0.29 % launching worker at depth: 6
% 0.08/0.29 % launching worker at depth: 7
% 0.08/0.29 % launching worker at depth: 1
% 0.08/0.29 % launching worker at depth: 8
% 0.08/0.29 % launching worker at depth: 9
% 0.13/0.30 % launching worker at depth: 10
% 0.13/0.32 % launching worker at depth: 11
% 2.70/0.64 % launching worker at depth: 12
% 94.45/12.21 % launching worker at depth: 13
% 179.05/22.84 % SZS status Theorem for theBenchmark
% 179.05/22.84 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------