%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SEU290+2 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n019.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:35:53 EDT 2022
% Result : Theorem 59.78s 59.99s
% Output : Refutation 59.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 13
% Syntax : Number of clauses : 28 ( 15 unt; 1 nHn; 28 RR)
% Number of literals : 52 ( 0 equ; 26 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 9 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
function(skc18),
file('SEU290+2.p',unknown),
[] ).
cnf(51,axiom,
in(skc19,skc21),
file('SEU290+2.p',unknown),
[] ).
cnf(78,axiom,
quasi_total(skc18,skc21,skc20),
file('SEU290+2.p',unknown),
[] ).
cnf(79,axiom,
relation_of2_as_subset(skc18,skc21,skc20),
file('SEU290+2.p',unknown),
[] ).
cnf(80,axiom,
~ equal(skc20,empty_set),
file('SEU290+2.p',unknown),
[] ).
cnf(135,axiom,
( skP2(u,v)
| equal(v,empty_set) ),
file('SEU290+2.p',unknown),
[] ).
cnf(178,axiom,
~ in(apply(skc18,skc19),relation_rng(skc18)),
file('SEU290+2.p',unknown),
[] ).
cnf(262,axiom,
( ~ element(u,powerset(cartesian_product2(v,w)))
| relation(u) ),
file('SEU290+2.p',unknown),
[] ).
cnf(415,axiom,
( ~ relation_of2_as_subset(u,v,w)
| element(u,powerset(cartesian_product2(v,w))) ),
file('SEU290+2.p',unknown),
[] ).
cnf(534,axiom,
( ~ relation(u)
| ~ in(ordered_pair(v,w),u)
| in(w,relation_rng(u)) ),
file('SEU290+2.p',unknown),
[] ).
cnf(673,axiom,
( ~ function(u)
| ~ relation(u)
| ~ in(ordered_pair(v,w),u)
| equal(w,apply(u,v)) ),
file('SEU290+2.p',unknown),
[] ).
cnf(732,axiom,
( ~ skP2(u,v)
| ~ relation_of2_as_subset(w,u,v)
| ~ quasi_total(w,u,v)
| equal(relation_dom_as_subset(u,v,w),u) ),
file('SEU290+2.p',unknown),
[] ).
cnf(798,axiom,
( ~ in(u,v)
| ~ equal(relation_dom_as_subset(v,w,x),v)
| ~ relation_of2_as_subset(x,v,w)
| in(ordered_pair(u,skf404(x,u)),x) ),
file('SEU290+2.p',unknown),
[] ).
cnf(1221,plain,
skP2(u,skc20),
inference(res,[status(thm),theory(equality)],[135,80]),
[iquote('0:Res:135.0,80.0')] ).
cnf(1299,plain,
( ~ quasi_total(skc18,skc21,skc20)
| ~ skP2(skc21,skc20)
| equal(relation_dom_as_subset(skc21,skc20,skc18),skc21) ),
inference(res,[status(thm),theory(equality)],[79,732]),
[iquote('0:Res:79.0,732.2')] ).
cnf(1306,plain,
element(skc18,powerset(cartesian_product2(skc21,skc20))),
inference(res,[status(thm),theory(equality)],[79,415]),
[iquote('0:Res:79.0,415.0')] ).
cnf(1312,plain,
( ~ equal(relation_dom_as_subset(skc21,skc20,skc18),skc21)
| ~ in(u,skc21)
| in(ordered_pair(u,skf404(skc18,u)),skc18) ),
inference(res,[status(thm),theory(equality)],[79,798]),
[iquote('0:Res:79.0,798.2')] ).
cnf(1396,plain,
equal(relation_dom_as_subset(skc21,skc20,skc18),skc21),
inference(mrr,[status(thm)],[1299,78,1221]),
[iquote('0:MRR:1299.0,1299.1,78.0,1221.0')] ).
cnf(1397,plain,
( ~ equal(skc21,skc21)
| ~ in(u,skc21)
| in(ordered_pair(u,skf404(skc18,u)),skc18) ),
inference(rew,[status(thm),theory(equality)],[1396,1312]),
[iquote('0:Rew:1396.0,1312.0')] ).
cnf(1398,plain,
( ~ in(u,skc21)
| in(ordered_pair(u,skf404(skc18,u)),skc18) ),
inference(obv,[status(thm),theory(equality)],[1397]),
[iquote('0:Obv:1397.0')] ).
cnf(1465,plain,
in(ordered_pair(skc19,skf404(skc18,skc19)),skc18),
inference(res,[status(thm),theory(equality)],[51,1398]),
[iquote('0:Res:51.0,1398.0')] ).
cnf(3304,plain,
relation(skc18),
inference(res,[status(thm),theory(equality)],[1306,262]),
[iquote('0:Res:1306.0,262.0')] ).
cnf(16808,plain,
( ~ relation(skc18)
| in(skf404(skc18,skc19),relation_rng(skc18)) ),
inference(res,[status(thm),theory(equality)],[1465,534]),
[iquote('0:Res:1465.0,534.1')] ).
cnf(29676,plain,
( ~ function(skc18)
| ~ relation(skc18)
| equal(apply(skc18,skc19),skf404(skc18,skc19)) ),
inference(res,[status(thm),theory(equality)],[1465,673]),
[iquote('0:Res:1465.0,673.2')] ).
cnf(29902,plain,
in(skf404(skc18,skc19),relation_rng(skc18)),
inference(ssi,[status(thm)],[16808,1,3304]),
[iquote('0:SSi:16808.0,1.0,3304.0')] ).
cnf(30232,plain,
equal(apply(skc18,skc19),skf404(skc18,skc19)),
inference(ssi,[status(thm)],[29676,1,3304]),
[iquote('0:SSi:29676.1,29676.0,1.0,3304.0,1.0,3304.0')] ).
cnf(30233,plain,
~ in(skf404(skc18,skc19),relation_rng(skc18)),
inference(rew,[status(thm),theory(equality)],[30232,178]),
[iquote('0:Rew:30232.0,178.0')] ).
cnf(30248,plain,
$false,
inference(mrr,[status(thm)],[30233,29902]),
[iquote('0:MRR:30233.0,29902.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU290+2 : TPTP v8.1.0. Released v3.3.0.
% 0.07/0.12 % Command : run_spass %d %s
% 0.12/0.34 % Computer : n019.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 : 600
% 0.12/0.34 % DateTime : Mon Jun 20 10:17:09 EDT 2022
% 0.12/0.34 % CPUTime :
% 59.78/59.99
% 59.78/59.99 SPASS V 3.9
% 59.78/59.99 SPASS beiseite: Proof found.
% 59.78/59.99 % SZS status Theorem
% 59.78/59.99 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 59.78/59.99 SPASS derived 22605 clauses, backtracked 3502 clauses, performed 20 splits and kept 13021 clauses.
% 59.78/59.99 SPASS allocated 145564 KBytes.
% 59.78/59.99 SPASS spent 0:0:58.97 on the problem.
% 59.78/59.99 0:00:00.04 for the input.
% 59.78/59.99 0:0:40.41 for the FLOTTER CNF translation.
% 59.78/59.99 0:00:00.30 for inferences.
% 59.78/59.99 0:00:00.33 for the backtracking.
% 59.78/59.99 0:0:17.03 for the reduction.
% 59.78/59.99
% 59.78/59.99
% 59.78/59.99 Here is a proof with depth 3, length 28 :
% 59.78/59.99 % SZS output start Refutation
% See solution above
% 59.78/59.99 Formulae used in the proof : t6_funct_2 d1_funct_2 cc1_relset_1 dt_m2_relset_1 t20_relat_1 t8_funct_1 t22_relset_1
% 59.78/59.99
%------------------------------------------------------------------------------