%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV884-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 09:09:16 AM UTC 2026
% Result : Unsatisfiable 46.25s 7.16s
% Output : CNFRefutation 46.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 5
% Syntax : Number of formulae : 14 ( 10 unt; 0 def)
% Number of atoms : 18 ( 3 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 10 ( 6 ~; 4 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 7 con; 0-4 aty)
% Number of variables : 21 ( 0 sgn 9 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cls_conjecture_6,axiom,
~ c_lessequals(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a),c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool)),
file('theBenchmark.p',cls_conjecture_6) ).
cnf(c_350,plain,
~ c_lessequals(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a),c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool)),
inference(clausify,[status(thm)],[cls_conjecture_6]) ).
fof(cls_conjecture_4,axiom,
c_in(v_pn,v_U,tc_Com_Opname),
file('theBenchmark.p',cls_conjecture_4) ).
cnf(c_352,plain,
c_in(v_pn,v_U,tc_Com_Opname),
inference(clausify,[status(thm)],[cls_conjecture_4]) ).
fof(cls_conjecture_1,axiom,
c_lessequals(v_G,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool)),
file('theBenchmark.p',cls_conjecture_1) ).
cnf(c_356,plain,
c_lessequals(v_G,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool)),
inference(clausify,[status(thm)],[cls_conjecture_1]) ).
fof(cls_insert__image_0,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ c_in(VAR_1,VAR_2,VAR_3)
| c_Set_Oinsert(hAPP(VAR_0,VAR_1),c_Set_Oimage(VAR_0,VAR_2,VAR_3,VAR_4),VAR_4) = c_Set_Oimage(VAR_0,VAR_2,VAR_3,VAR_4) ),
file('theBenchmark.p',cls_insert__image_0) ).
cnf(c_372,plain,
( ~ c_in(B,C,D)
| c_Set_Oinsert(hAPP(A,B),c_Set_Oimage(A,C,D,E),E) = c_Set_Oimage(A,C,D,E) ),
inference(clausify,[status(thm)],[cls_insert__image_0]) ).
fof(cls_insert__mono_0,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ c_lessequals(VAR_1,VAR_3,tc_fun(VAR_2,tc_bool))
| c_lessequals(c_Set_Oinsert(VAR_0,VAR_1,VAR_2),c_Set_Oinsert(VAR_0,VAR_3,VAR_2),tc_fun(VAR_2,tc_bool)) ),
file('theBenchmark.p',cls_insert__mono_0) ).
cnf(c_431,plain,
( ~ c_lessequals(B,D,tc_fun(C,tc_bool))
| c_lessequals(c_Set_Oinsert(A,B,C),c_Set_Oinsert(A,D,C),tc_fun(C,tc_bool)) ),
inference(clausify,[status(thm)],[cls_insert__mono_0]) ).
cnf(c_1328,plain,
c_Set_Oinsert(hAPP(A,v_pn),c_Set_Oimage(A,v_U,tc_Com_Opname,B),B) = c_Set_Oimage(A,v_U,tc_Com_Opname,B),
inference(resolve,[status(thm)],[c_372,c_352]) ).
cnf(c_1493,plain,
c_lessequals(c_Set_Oinsert(A,v_G,t_a),c_Set_Oinsert(A,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),tc_fun(t_a,tc_bool)),
inference(resolve,[status(thm)],[c_431,c_356]) ).
cnf(c_29448,plain,
c_lessequals(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a),c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool)),
inference(paramod,[status(thm)],[c_1328,c_1493]) ).
cnf(c_29447,plain,
$false,
inference(resolve,[status(thm)],[c_350,c_29448]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV884-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.40 % Computer : n018.cluster.edu
% 0.15/0.40 % Model : x86_64 x86_64
% 0.15/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.40 % Memory : 8046.5625MB
% 0.15/0.40 % OS : Linux 6.8.0-71-generic
% 0.15/0.40 % CPULimit : 300
% 0.15/0.40 % WCLimit : 300
% 0.15/0.40 % DateTime : Sat Sep 26 15:08:51 UTC 2026
% 0.15/0.41 % CPUTime :
% 0.15/0.41 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.15/0.41 % Process 730723 was started by sandbox2 on n018,
% 0.15/0.41 % Sat Sep 26 15:08:51 2026
% 0.15/0.41 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.15/0.44
% 0.15/0.44 % From the command line: assign(max_seconds, 300).
% 46.25/7.16
% 46.25/7.16 % given #500 (I,wt=36): 865 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Finite__Set_Ocard(c_Orderings_Otop__class_Otop(tc_fun(A,tc_bool)),A),tc_nat) | -c_Finite__Set_Ofinite(c_Orderings_Otop__class_Otop(tc_fun(A,tc_bool)),A) # tptp_name(cls_finite__UNIV__card__ge__0_0) # clausal_fof(1). [assumption].
% 46.25/7.16
% 46.25/7.16 % given #1000 (T,wt=19): 9058 c_lessequals(A,B,tc_bool) | -c_lessequals(c_Orderings_Otop__class_Otop(tc_bool),B,tc_bool). [resolve(3895,a,419,d),unit_del(a,331)].
% 46.25/7.16
% 46.25/7.16 % given #1500 (A,wt=37): 1393 c_lessequals(c_HOL_Ominus__class_Ominus(c_Suc(v_na),A,tc_nat),c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),A,tc_nat),tc_nat). [resolve(383,b,355,a)].
% 46.25/7.16
% 46.25/7.16 % SZS status Unsatisfiable for theBenchmark
% 46.25/7.16
% 46.25/7.16 % Proof 1 at 5.36 (+ 1.26) seconds.
% 46.25/7.16 % Length of proof is 8.
% 46.25/7.16 % Level of proof is 2.
% 46.25/7.16 % Maximum clause weight is 35.000.
% 46.25/7.16 % Given clauses 1838.
% 46.25/7.16
% 46.25/7.16 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------