%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SEU115+1 : TPTP v8.1.0. Released v3.2.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n032.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 : 600s
% DateTime : Tue Jul 19 14:34:02 EDT 2022
% Result : Theorem 0.14s 0.37s
% Output : Refutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 14
% Syntax : Number of clauses : 26 ( 23 unt; 0 nHn; 26 RR)
% Number of literals : 29 ( 0 equ; 4 neg)
% Maximal clause size : 2 ( 1 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 11 ( 10 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 2 con; 0-1 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(6,axiom,
empty(empty_set),
file('SEU115+1.p',unknown),
[] ).
cnf(19,axiom,
empty(skf7(u)),
file('SEU115+1.p',unknown),
[] ).
cnf(20,axiom,
relation(skf7(u)),
file('SEU115+1.p',unknown),
[] ).
cnf(21,axiom,
function(skf7(u)),
file('SEU115+1.p',unknown),
[] ).
cnf(22,axiom,
one_to_one(skf7(u)),
file('SEU115+1.p',unknown),
[] ).
cnf(23,axiom,
epsilon_transitive(skf7(u)),
file('SEU115+1.p',unknown),
[] ).
cnf(24,axiom,
epsilon_connected(skf7(u)),
file('SEU115+1.p',unknown),
[] ).
cnf(25,axiom,
ordinal(skf7(u)),
file('SEU115+1.p',unknown),
[] ).
cnf(26,axiom,
natural(skf7(u)),
file('SEU115+1.p',unknown),
[] ).
cnf(27,axiom,
finite(skf7(u)),
file('SEU115+1.p',unknown),
[] ).
cnf(46,axiom,
equal(powerset(empty_set),singleton(empty_set)),
file('SEU115+1.p',unknown),
[] ).
cnf(47,axiom,
~ equal(singleton(empty_set),finite_subsets(empty_set)),
file('SEU115+1.p',unknown),
[] ).
cnf(51,axiom,
( ~ empty(u)
| equal(u,empty_set) ),
file('SEU115+1.p',unknown),
[] ).
cnf(59,axiom,
( ~ finite(u)
| equal(powerset(u),finite_subsets(u)) ),
file('SEU115+1.p',unknown),
[] ).
cnf(78,plain,
equal(skf7(u),empty_set),
inference(ems,[status(thm)],[51,19]),
[iquote('0:EmS:51.0,19.0')] ).
cnf(84,plain,
natural(empty_set),
inference(rew,[status(thm),theory(equality)],[78,26]),
[iquote('0:Rew:78.0,26.0')] ).
cnf(85,plain,
ordinal(empty_set),
inference(rew,[status(thm),theory(equality)],[78,25]),
[iquote('0:Rew:78.0,25.0')] ).
cnf(86,plain,
epsilon_connected(empty_set),
inference(rew,[status(thm),theory(equality)],[78,24]),
[iquote('0:Rew:78.0,24.0')] ).
cnf(87,plain,
epsilon_transitive(empty_set),
inference(rew,[status(thm),theory(equality)],[78,23]),
[iquote('0:Rew:78.0,23.0')] ).
cnf(88,plain,
one_to_one(empty_set),
inference(rew,[status(thm),theory(equality)],[78,22]),
[iquote('0:Rew:78.0,22.0')] ).
cnf(89,plain,
function(empty_set),
inference(rew,[status(thm),theory(equality)],[78,21]),
[iquote('0:Rew:78.0,21.0')] ).
cnf(90,plain,
relation(empty_set),
inference(rew,[status(thm),theory(equality)],[78,20]),
[iquote('0:Rew:78.0,20.0')] ).
cnf(91,plain,
finite(empty_set),
inference(rew,[status(thm),theory(equality)],[78,27]),
[iquote('0:Rew:78.0,27.0')] ).
cnf(111,plain,
( ~ finite(empty_set)
| equal(singleton(empty_set),finite_subsets(empty_set)) ),
inference(spr,[status(thm),theory(equality)],[59,46]),
[iquote('0:SpR:59.1,46.0')] ).
cnf(113,plain,
equal(singleton(empty_set),finite_subsets(empty_set)),
inference(ssi,[status(thm)],[111,6,84,85,86,87,88,89,90,91]),
[iquote('0:SSi:111.0,6.0,84.0,85.0,86.0,87.0,88.0,89.0,90.0,91.0')] ).
cnf(114,plain,
$false,
inference(mrr,[status(thm)],[113,47]),
[iquote('0:MRR:113.0,47.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.09 % Problem : SEU115+1 : TPTP v8.1.0. Released v3.2.0.
% 0.03/0.10 % Command : run_spass %d %s
% 0.10/0.29 % Computer : n032.cluster.edu
% 0.10/0.29 % Model : x86_64 x86_64
% 0.10/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.29 % Memory : 8042.1875MB
% 0.10/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.29 % CPULimit : 300
% 0.10/0.29 % WCLimit : 600
% 0.10/0.29 % DateTime : Sun Jun 19 08:56:32 EDT 2022
% 0.10/0.29 % CPUTime :
% 0.14/0.37
% 0.14/0.37 SPASS V 3.9
% 0.14/0.37 SPASS beiseite: Proof found.
% 0.14/0.37 % SZS status Theorem
% 0.14/0.37 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.37 SPASS derived 47 clauses, backtracked 0 clauses, performed 0 splits and kept 89 clauses.
% 0.14/0.37 SPASS allocated 97718 KBytes.
% 0.14/0.37 SPASS spent 0:00:00.07 on the problem.
% 0.14/0.37 0:00:00.03 for the input.
% 0.14/0.37 0:00:00.02 for the FLOTTER CNF translation.
% 0.14/0.37 0:00:00.00 for inferences.
% 0.14/0.37 0:00:00.00 for the backtracking.
% 0.14/0.37 0:00:00.00 for the reduction.
% 0.14/0.37
% 0.14/0.37
% 0.14/0.37 Here is a proof with depth 1, length 26 :
% 0.14/0.37 % SZS output start Refutation
% See solution above
% 0.14/0.37 Formulae used in the proof : fc1_xboole_0 rc2_finset_1 t1_zfmisc_1 t28_finsub_1 t6_boole t27_finsub_1
% 0.14/0.37
%------------------------------------------------------------------------------