%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWV580-1 : TPTP v8.1.0. Released v4.1.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n010.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 : Wed Jul 20 21:44:27 EDT 2022
% Result : Unsatisfiable 35.44s 35.66s
% Output : Refutation 35.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 29
% Syntax : Number of clauses : 37 ( 33 unt; 0 nHn; 37 RR)
% Number of literals : 44 ( 0 equ; 12 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 24 ( 23 usr; 1 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 9 con; 0-4 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(355,axiom,
equal(c_Collect(u,v),u),
file('SWV580-1.p',unknown),
[] ).
cnf(456,axiom,
equal(c_Set_Oinsert(u,c_Orderings_Obot__class_Obot(tc_fun(v,tc_bool)),v),c_Collect(c_fequal(u,v),v)),
file('SWV580-1.p',unknown),
[] ).
cnf(507,axiom,
( ~ class_Orderings_Olinorder(u)
| ~ c_HOL_Oord__class_Oless(v,w,u)
| equal(c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(v,c_Orderings_Obot__class_Obot(tc_fun(u,tc_bool)),u),c_SetInterval_Oord__class_OgreaterThanLessThan(v,w,u),tc_fun(u,tc_bool)),c_SetInterval_Oord__class_OatLeastLessThan(v,w,u)) ),
file('SWV580-1.p',unknown),
[] ).
cnf(513,axiom,
equal(c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(u,v,w),x,tc_fun(w,tc_bool)),c_Set_Oinsert(u,c_Lattices_Oupper__semilattice__class_Osup(v,x,tc_fun(w,tc_bool)),w)),
file('SWV580-1.p',unknown),
[] ).
cnf(524,axiom,
equal(c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(u,tc_bool)),v,tc_fun(u,tc_bool)),v),
file('SWV580-1.p',unknown),
[] ).
cnf(548,axiom,
equal(c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(u,c_Orderings_Obot__class_Obot(tc_fun(v,tc_bool)),v),w,tc_fun(v,tc_bool)),c_Set_Oinsert(u,w,v)),
file('SWV580-1.p',unknown),
[] ).
cnf(552,axiom,
c_HOL_Oord__class_Oless(v_m,v_n,tc_nat),
file('SWV580-1.p',unknown),
[] ).
cnf(566,axiom,
class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_nat),
file('SWV580-1.p',unknown),
[] ).
cnf(567,axiom,
class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat),
file('SWV580-1.p',unknown),
[] ).
cnf(568,axiom,
class_OrderedGroup_Opordered__ab__semigroup__add(tc_nat),
file('SWV580-1.p',unknown),
[] ).
cnf(569,axiom,
class_OrderedGroup_Opordered__comm__monoid__add(tc_nat),
file('SWV580-1.p',unknown),
[] ).
cnf(570,axiom,
class_OrderedGroup_Ocancel__ab__semigroup__add(tc_nat),
file('SWV580-1.p',unknown),
[] ).
cnf(571,axiom,
class_OrderedGroup_Ocancel__semigroup__add(tc_nat),
file('SWV580-1.p',unknown),
[] ).
cnf(572,axiom,
class_Ring__and__Field_Oordered__semidom(tc_nat),
file('SWV580-1.p',unknown),
[] ).
cnf(573,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_nat),
file('SWV580-1.p',unknown),
[] ).
cnf(574,axiom,
class_OrderedGroup_Oab__semigroup__add(tc_nat),
file('SWV580-1.p',unknown),
[] ).
cnf(575,axiom,
class_OrderedGroup_Ocomm__monoid__add(tc_nat),
file('SWV580-1.p',unknown),
[] ).
cnf(576,axiom,
class_Lattices_Oupper__semilattice(tc_nat),
file('SWV580-1.p',unknown),
[] ).
cnf(577,axiom,
class_Lattices_Olower__semilattice(tc_nat),
file('SWV580-1.p',unknown),
[] ).
cnf(578,axiom,
class_Lattices_Odistrib__lattice(tc_nat),
file('SWV580-1.p',unknown),
[] ).
cnf(579,axiom,
class_OrderedGroup_Omonoid__add(tc_nat),
file('SWV580-1.p',unknown),
[] ).
cnf(580,axiom,
class_Orderings_Opreorder(tc_nat),
file('SWV580-1.p',unknown),
[] ).
cnf(581,axiom,
class_Orderings_Olinorder(tc_nat),
file('SWV580-1.p',unknown),
[] ).
cnf(582,axiom,
class_Lattices_Olattice(tc_nat),
file('SWV580-1.p',unknown),
[] ).
cnf(583,axiom,
class_Orderings_Oorder(tc_nat),
file('SWV580-1.p',unknown),
[] ).
cnf(584,axiom,
class_Orderings_Obot(tc_nat),
file('SWV580-1.p',unknown),
[] ).
cnf(585,axiom,
class_HOL_Ominus(tc_nat),
file('SWV580-1.p',unknown),
[] ).
cnf(586,axiom,
class_HOL_Oord(tc_nat),
file('SWV580-1.p',unknown),
[] ).
cnf(601,axiom,
~ equal(c_Finite__Set_Osetsum(v,c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(v_m,c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),c_SetInterval_Oord__class_OgreaterThanLessThan(v_m,v_n,tc_nat),tc_fun(tc_nat,tc_bool)),tc_nat,t_a),c_Finite__Set_Osetsum(v,c_SetInterval_Oord__class_OatLeastLessThan(v_m,v_n,tc_nat),tc_nat,t_a)),
file('SWV580-1.p',unknown),
[] ).
cnf(604,plain,
equal(c_Set_Oinsert(u,c_Orderings_Obot__class_Obot(tc_fun(v,tc_bool)),v),c_fequal(u,v)),
inference(rew,[status(thm),theory(equality)],[355,456]),
[iquote('0:Rew:355.0,456.0')] ).
cnf(622,plain,
equal(c_Lattices_Oupper__semilattice__class_Osup(c_fequal(u,v),w,tc_fun(v,tc_bool)),c_Set_Oinsert(u,w,v)),
inference(rew,[status(thm),theory(equality)],[604,548]),
[iquote('0:Rew:604.0,548.0')] ).
cnf(661,plain,
( ~ class_Orderings_Olinorder(u)
| ~ c_HOL_Oord__class_Oless(v,w,u)
| equal(c_Set_Oinsert(v,c_SetInterval_Oord__class_OgreaterThanLessThan(v,w,u),u),c_SetInterval_Oord__class_OatLeastLessThan(v,w,u)) ),
inference(rew,[status(thm),theory(equality)],[524,507,513]),
[iquote('0:Rew:524.0,507.2,513.0,507.2')] ).
cnf(669,plain,
~ equal(c_Finite__Set_Osetsum(v,c_Set_Oinsert(v_m,c_SetInterval_Oord__class_OgreaterThanLessThan(v_m,v_n,tc_nat),tc_nat),tc_nat,t_a),c_Finite__Set_Osetsum(v,c_SetInterval_Oord__class_OatLeastLessThan(v_m,v_n,tc_nat),tc_nat,t_a)),
inference(rew,[status(thm),theory(equality)],[622,601,604]),
[iquote('0:Rew:622.0,601.0,604.0,601.0')] ).
cnf(73232,plain,
( ~ class_Orderings_Olinorder(tc_nat)
| ~ c_HOL_Oord__class_Oless(v_m,v_n,tc_nat)
| ~ equal(c_Finite__Set_Osetsum(v,c_SetInterval_Oord__class_OatLeastLessThan(v_m,v_n,tc_nat),tc_nat,t_a),c_Finite__Set_Osetsum(v,c_SetInterval_Oord__class_OatLeastLessThan(v_m,v_n,tc_nat),tc_nat,t_a)) ),
inference(spl,[status(thm),theory(equality)],[661,669]),
[iquote('0:SpL:661.2,669.0')] ).
cnf(73235,plain,
( ~ class_Orderings_Olinorder(tc_nat)
| ~ c_HOL_Oord__class_Oless(v_m,v_n,tc_nat) ),
inference(obv,[status(thm),theory(equality)],[73232]),
[iquote('0:Obv:73232.2')] ).
cnf(73236,plain,
~ c_HOL_Oord__class_Oless(v_m,v_n,tc_nat),
inference(ssi,[status(thm)],[73235,572,570,571,574,568,585,579,584,566,578,573,586,569,580,567,577,576,575,582,581,583]),
[iquote('0:SSi:73235.0,572.0,570.0,571.0,574.0,568.0,585.0,579.0,584.0,566.0,578.0,573.0,586.0,569.0,580.0,567.0,577.0,576.0,575.0,582.0,581.0,583.0')] ).
cnf(73237,plain,
$false,
inference(mrr,[status(thm)],[73236,552]),
[iquote('0:MRR:73236.0,552.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SWV580-1 : TPTP v8.1.0. Released v4.1.0.
% 0.04/0.14 % Command : run_spass %d %s
% 0.14/0.36 % Computer : n010.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 600
% 0.14/0.36 % DateTime : Wed Jun 15 12:42:39 EDT 2022
% 0.14/0.36 % CPUTime :
% 35.44/35.66
% 35.44/35.66 SPASS V 3.9
% 35.44/35.66 SPASS beiseite: Proof found.
% 35.44/35.66 % SZS status Theorem
% 35.44/35.66 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 35.44/35.66 SPASS derived 63194 clauses, backtracked 452 clauses, performed 2 splits and kept 10946 clauses.
% 35.44/35.66 SPASS allocated 120678 KBytes.
% 35.44/35.66 SPASS spent 0:0:33.69 on the problem.
% 35.44/35.66 0:00:00.06 for the input.
% 35.44/35.66 0:00:00.00 for the FLOTTER CNF translation.
% 35.44/35.66 0:00:00.85 for inferences.
% 35.44/35.66 0:00:02.45 for the backtracking.
% 35.44/35.66 0:0:29.92 for the reduction.
% 35.44/35.66
% 35.44/35.66
% 35.44/35.66 Here is a proof with depth 1, length 37 :
% 35.44/35.66 % SZS output start Refutation
% See solution above
% 35.44/35.66 Formulae used in the proof : cls_Collect__def_0 cls_singleton__conv2_0 cls_ivl__disj__un_I3_J_0 cls_Un__insert__left_0 cls_Un__empty__left_0 cls_insert__is__Un_0 cls_CHAINED_0 clsarity_nat__OrderedGroup_Opordered__cancel__ab__semigroup__add clsarity_nat__OrderedGroup_Opordered__ab__semigroup__add__imp__le clsarity_nat__OrderedGroup_Opordered__ab__semigroup__add clsarity_nat__OrderedGroup_Opordered__comm__monoid__add clsarity_nat__OrderedGroup_Ocancel__ab__semigroup__add clsarity_nat__OrderedGroup_Ocancel__semigroup__add clsarity_nat__Ring__and__Field_Oordered__semidom clsarity_nat__Ring__and__Field_Ocomm__semiring__1 clsarity_nat__OrderedGroup_Oab__semigroup__add clsarity_nat__OrderedGroup_Ocomm__monoid__add clsarity_nat__Lattices_Oupper__semilattice clsarity_nat__Lattices_Olower__semilattice clsarity_nat__Lattices_Odistrib__lattice clsarity_nat__OrderedGroup_Omonoid__add clsarity_nat__Orderings_Opreorder clsarity_nat__Orderings_Olinorder clsarity_nat__Lattices_Olattice clsarity_nat__Orderings_Oorder clsarity_nat__Orderings_Obot clsarity_nat__HOL_Ominus clsarity_nat__HOL_Oord cls_conjecture_0
% 35.44/35.66
%------------------------------------------------------------------------------