%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWW473+5 : TPTP v8.1.0. Released v5.3.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n017.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 : Thu Jul 21 01:28:37 EDT 2022
% Result : Theorem 68.31s 68.51s
% Output : Refutation 68.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 5
% Syntax : Number of clauses : 9 ( 6 unt; 0 nHn; 9 RR)
% Number of literals : 13 ( 0 equ; 8 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 18 ( 18 usr; 12 con; 0-4 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(59,axiom,
hBOOL(hAPP(fun(pname,bool),bool,hAPP(pname,fun(fun(pname,bool),bool),member(pname),pn),u__dfg)),
file('SWW473+5.p',unknown),
[] ).
cnf(121,axiom,
hBOOL(hAPP(fun(x_a,bool),bool,hAPP(fun(x_a,bool),fun(fun(x_a,bool),bool),ord_less_eq(fun(x_a,bool)),g),hAPP(fun(pname,bool),fun(x_a,bool),hAPP(fun(pname,x_a),fun(fun(pname,bool),fun(x_a,bool)),image(pname,x_a),mgt_call),u__dfg))),
file('SWW473+5.p',unknown),
[] ).
cnf(152,axiom,
( ~ hBOOL(hAPP(fun(u,bool),bool,hAPP(u,fun(fun(u,bool),bool),member(u),v),w))
| hBOOL(hAPP(fun(x,bool),bool,hAPP(x,fun(fun(x,bool),bool),member(x),hAPP(u,x,y,v)),hAPP(fun(u,bool),fun(x,bool),hAPP(fun(u,x),fun(fun(u,bool),fun(x,bool)),image(u,x),y),w))) ),
file('SWW473+5.p',unknown),
[] ).
cnf(169,axiom,
~ hBOOL(hAPP(fun(x_a,bool),bool,hAPP(fun(x_a,bool),fun(fun(x_a,bool),bool),ord_less_eq(fun(x_a,bool)),hAPP(fun(x_a,bool),fun(x_a,bool),hAPP(x_a,fun(fun(x_a,bool),fun(x_a,bool)),insert(x_a),hAPP(pname,x_a,mgt_call,pn)),g)),hAPP(fun(pname,bool),fun(x_a,bool),hAPP(fun(pname,x_a),fun(fun(pname,bool),fun(x_a,bool)),image(pname,x_a),mgt_call),u__dfg))),
file('SWW473+5.p',unknown),
[] ).
cnf(182,axiom,
( ~ hBOOL(hAPP(fun(u,bool),bool,hAPP(u,fun(fun(u,bool),bool),member(u),v),w))
| ~ hBOOL(hAPP(fun(u,bool),bool,hAPP(fun(u,bool),fun(fun(u,bool),bool),ord_less_eq(fun(u,bool)),x),w))
| hBOOL(hAPP(fun(u,bool),bool,hAPP(fun(u,bool),fun(fun(u,bool),bool),ord_less_eq(fun(u,bool)),hAPP(fun(u,bool),fun(u,bool),hAPP(u,fun(fun(u,bool),fun(u,bool)),insert(u),v),x)),w)) ),
file('SWW473+5.p',unknown),
[] ).
cnf(225,plain,
( ~ hBOOL(hAPP(fun(x_a,bool),bool,hAPP(fun(x_a,bool),fun(fun(x_a,bool),bool),ord_less_eq(fun(x_a,bool)),g),hAPP(fun(pname,bool),fun(x_a,bool),hAPP(fun(pname,x_a),fun(fun(pname,bool),fun(x_a,bool)),image(pname,x_a),mgt_call),u__dfg)))
| ~ hBOOL(hAPP(fun(x_a,bool),bool,hAPP(x_a,fun(fun(x_a,bool),bool),member(x_a),hAPP(pname,x_a,mgt_call,pn)),hAPP(fun(pname,bool),fun(x_a,bool),hAPP(fun(pname,x_a),fun(fun(pname,bool),fun(x_a,bool)),image(pname,x_a),mgt_call),u__dfg))) ),
inference(res,[status(thm),theory(equality)],[182,169]),
[iquote('0:Res:182.2,169.0')] ).
cnf(234,plain,
~ hBOOL(hAPP(fun(x_a,bool),bool,hAPP(x_a,fun(fun(x_a,bool),bool),member(x_a),hAPP(pname,x_a,mgt_call,pn)),hAPP(fun(pname,bool),fun(x_a,bool),hAPP(fun(pname,x_a),fun(fun(pname,bool),fun(x_a,bool)),image(pname,x_a),mgt_call),u__dfg))),
inference(mrr,[status(thm)],[225,121]),
[iquote('0:MRR:225.0,121.0')] ).
cnf(26377,plain,
~ hBOOL(hAPP(fun(pname,bool),bool,hAPP(pname,fun(fun(pname,bool),bool),member(pname),pn),u__dfg)),
inference(res,[status(thm),theory(equality)],[152,234]),
[iquote('0:Res:152.1,234.0')] ).
cnf(26379,plain,
$false,
inference(mrr,[status(thm)],[26377,59]),
[iquote('0:MRR:26377.0,59.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWW473+5 : TPTP v8.1.0. Released v5.3.0.
% 0.03/0.13 % Command : run_spass %d %s
% 0.13/0.33 % Computer : n017.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Sun Jun 5 09:17:15 EDT 2022
% 0.13/0.34 % CPUTime :
% 68.31/68.51
% 68.31/68.51 SPASS V 3.9
% 68.31/68.51 SPASS beiseite: Proof found.
% 68.31/68.51 % SZS status Theorem
% 68.31/68.51 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 68.31/68.51 SPASS derived 21418 clauses, backtracked 0 clauses, performed 2 splits and kept 8553 clauses.
% 68.31/68.51 SPASS allocated 144991 KBytes.
% 68.31/68.51 SPASS spent 0:01:07.16 on the problem.
% 68.31/68.51 0:00:00.04 for the input.
% 68.31/68.51 0:00:00.23 for the FLOTTER CNF translation.
% 68.31/68.51 0:00:01.09 for inferences.
% 68.31/68.51 0:00:04.16 for the backtracking.
% 68.31/68.51 0:01:01.37 for the reduction.
% 68.31/68.51
% 68.31/68.51
% 68.31/68.51 Here is a proof with depth 2, length 9 :
% 68.31/68.51 % SZS output start Refutation
% See solution above
% 68.31/68.51 Formulae used in the proof : conj_4 conj_1 fact_78_imageI conj_6 fact_84_insert__subset
% 68.31/68.51
%------------------------------------------------------------------------------