%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWV901-1 : TPTP v8.1.0. Released v4.1.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 : Wed Jul 20 21:45:32 EDT 2022
% Result : Unsatisfiable 39.49s 39.66s
% Output : Refutation 39.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 12
% Syntax : Number of clauses : 23 ( 15 unt; 0 nHn; 23 RR)
% Number of literals : 38 ( 0 equ; 18 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 6 ( 5 usr; 3 prp; 0-3 aty)
% Number of functors : 27 ( 27 usr; 15 con; 0-5 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(108,axiom,
equal(c_Collect(u,v),u),
file('SWV901-1.p',unknown),
[] ).
cnf(490,axiom,
equal(c_Set_Oinsert(u,c_Orderings_Obot__class_Obot(tc_fun(v,tc_bool)),v),c_Collect(hAPP(c_fequal(v),u),v)),
file('SWV901-1.p',unknown),
[] ).
cnf(542,axiom,
equal(c_Set_Oinsert(u,c_Orderings_Obot__class_Obot(tc_fun(v,tc_bool)),v),c_Option_Oset(c_Option_Ooption_OSome(u,v),v)),
file('SWV901-1.p',unknown),
[] ).
cnf(556,axiom,
( ~ equal(hAPP(c_Com_Obody,u),c_Option_Ooption_OSome(v,tc_Com_Ocom))
| ~ c_Com_OWT__bodies
| c_Com_OWT(v) ),
file('SWV901-1.p',unknown),
[] ).
cnf(560,axiom,
( ~ c_Com_OWT(u)
| ~ c_Com_OWT__bodies
| ~ c_Hoare__Mirabelle_Ostate__not__singleton
| c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,u),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ),
file('SWV901-1.p',unknown),
[] ).
cnf(590,axiom,
equal(c_Set_Oimage(u,c_Set_Oimage(v,w,x,y),y,z),c_Set_Oimage(c_COMBB(u,v,y,z,x),w,x,z)),
file('SWV901-1.p',unknown),
[] ).
cnf(594,axiom,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(u,v,w)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(x,u,w)
| c_Hoare__Mirabelle_Ohoare__derivs(x,v,w) ),
file('SWV901-1.p',unknown),
[] ).
cnf(614,axiom,
c_Hoare__Mirabelle_Ohoare__derivs(u,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(v),tc_bool)),v),
file('SWV901-1.p',unknown),
[] ).
cnf(706,axiom,
c_Hoare__Mirabelle_Ostate__not__singleton,
file('SWV901-1.p',unknown),
[] ).
cnf(707,axiom,
c_Com_OWT__bodies,
file('SWV901-1.p',unknown),
[] ).
cnf(711,axiom,
equal(hAPP(c_Com_Obody,v_pn),c_Option_Ooption_OSome(v_y,tc_Com_Ocom)),
file('SWV901-1.p',unknown),
[] ).
cnf(713,axiom,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,v_y),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
file('SWV901-1.p',unknown),
[] ).
cnf(717,plain,
( ~ equal(hAPP(c_Com_Obody,u),c_Option_Ooption_OSome(v,tc_Com_Ocom))
| c_Com_OWT(v) ),
inference(mrr,[status(thm)],[556,707]),
[iquote('0:MRR:556.1,707.0')] ).
cnf(723,plain,
equal(c_Option_Oset(c_Option_Ooption_OSome(u,v),v),hAPP(c_fequal(v),u)),
inference(rew,[status(thm),theory(equality)],[542,490,108]),
[iquote('0:Rew:542.0,490.0,108.0,490.0')] ).
cnf(728,plain,
equal(c_Set_Oinsert(u,c_Orderings_Obot__class_Obot(tc_fun(v,tc_bool)),v),hAPP(c_fequal(v),u)),
inference(rew,[status(thm),theory(equality)],[723,542]),
[iquote('0:Rew:723.0,542.0')] ).
cnf(772,plain,
( ~ c_Com_OWT(u)
| ~ c_Com_OWT__bodies
| ~ c_Hoare__Mirabelle_Ostate__not__singleton
| c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),hAPP(c_Hoare__Mirabelle_OMGT,u)),tc_Com_Ostate) ),
inference(rew,[status(thm),theory(equality)],[728,560]),
[iquote('0:Rew:728.0,560.3')] ).
cnf(773,plain,
( ~ c_Com_OWT(u)
| c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),hAPP(c_Hoare__Mirabelle_OMGT,u)),tc_Com_Ostate) ),
inference(mrr,[status(thm)],[772,707,706]),
[iquote('0:MRR:772.1,772.2,707.0,706.0')] ).
cnf(793,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),hAPP(c_Hoare__Mirabelle_OMGT,v_y)),tc_Com_Ostate),
inference(rew,[status(thm),theory(equality)],[590,713,728]),
[iquote('0:Rew:590.0,713.0,728.0,713.0')] ).
cnf(867,plain,
c_Com_OWT(v_y),
inference(res,[status(thm),theory(equality)],[711,717]),
[iquote('0:Res:711.0,717.0')] ).
cnf(20217,plain,
( ~ c_Com_OWT(u)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(v,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Com_Ostate)
| c_Hoare__Mirabelle_Ohoare__derivs(v,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),hAPP(c_Hoare__Mirabelle_OMGT,u)),tc_Com_Ostate) ),
inference(res,[status(thm),theory(equality)],[773,594]),
[iquote('0:Res:773.1,594.0')] ).
cnf(20219,plain,
( ~ c_Com_OWT(u)
| c_Hoare__Mirabelle_Ohoare__derivs(v,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),hAPP(c_Hoare__Mirabelle_OMGT,u)),tc_Com_Ostate) ),
inference(mrr,[status(thm)],[20217,614]),
[iquote('0:MRR:20217.1,614.0')] ).
cnf(65908,plain,
~ c_Com_OWT(v_y),
inference(res,[status(thm),theory(equality)],[20219,793]),
[iquote('0:Res:20219.1,793.0')] ).
cnf(65909,plain,
$false,
inference(ssi,[status(thm)],[65908,867]),
[iquote('0:SSi:65908.0,867.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : SWV901-1 : TPTP v8.1.0. Released v4.1.0.
% 0.03/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n019.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Wed Jun 15 23:31:54 EDT 2022
% 0.12/0.33 % CPUTime :
% 39.49/39.66
% 39.49/39.66 SPASS V 3.9
% 39.49/39.66 SPASS beiseite: Proof found.
% 39.49/39.66 % SZS status Theorem
% 39.49/39.66 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 39.49/39.66 SPASS derived 52284 clauses, backtracked 0 clauses, performed 4 splits and kept 11836 clauses.
% 39.49/39.66 SPASS allocated 133981 KBytes.
% 39.49/39.66 SPASS spent 0:0:36.33 on the problem.
% 39.49/39.66 0:00:00.06 for the input.
% 39.49/39.66 0:00:00.00 for the FLOTTER CNF translation.
% 39.49/39.66 0:00:00.77 for inferences.
% 39.49/39.66 0:00:02.03 for the backtracking.
% 39.49/39.66 0:0:33.06 for the reduction.
% 39.49/39.66
% 39.49/39.66
% 39.49/39.66 Here is a proof with depth 2, length 23 :
% 39.49/39.66 % SZS output start Refutation
% See solution above
% 39.49/39.66 Formulae used in the proof : cls_Collect__def_0 cls_singleton__conv2_0 cls_Option_Oset_Osimps_I2_J_0 cls_WT__bodiesD_0 cls_MGF_0 cls_image__image_0 cls_cut_0 cls_empty_0 cls_conjecture_0 cls_conjecture_1 cls_conjecture_5 cls_conjecture_7
% 39.49/39.66
%------------------------------------------------------------------------------