%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV938-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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:22 AM UTC 2026
% Result : Unsatisfiable 28.57s 9.54s
% Output : CNFRefutation 28.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 7
% Syntax : Number of formulae : 22 ( 17 unt; 0 def)
% Number of atoms : 29 ( 7 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 16 ( 9 ~; 7 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-5 aty)
% Number of functors : 19 ( 19 usr; 11 con; 0-5 aty)
% Number of variables : 75 ( 8 sgn 24 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cls_conjecture_0,axiom,
~ c_WellTypeRT_OWTrt(v_P,v_ha____,c_Map_Omap__upds(v_E____,c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____),
file('theBenchmark.p',cls_conjecture_0) ).
cnf(c_26,plain,
~ c_WellTypeRT_OWTrt(v_P,v_ha____,c_Map_Omap__upds(v_E____,c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____),
inference(clausify,[status(thm)],[cls_conjecture_0]) ).
fof(cls_wtabody_0,axiom,
c_WellType_OWT(v_P,c_Map_Omap__upds(c_COMBK(c_Option_Ooption_ONone(tc_Type_Oty),tc_Option_Ooption(tc_Type_Oty),tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____),
file('theBenchmark.p',cls_wtabody_0) ).
cnf(c_39,plain,
c_WellType_OWT(v_P,c_Map_Omap__upds(c_COMBK(c_Option_Ooption_ONone(tc_Type_Oty),tc_Option_Ooption(tc_Type_Oty),tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____),
inference(clausify,[status(thm)],[cls_wtabody_0]) ).
fof(cls_WT__implies__WTrt_0,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ c_WellType_OWT(VAR_0,VAR_2,VAR_3,VAR_4)
| c_WellTypeRT_OWTrt(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4) ),
file('theBenchmark.p',cls_WT__implies__WTrt_0) ).
cnf(c_50,plain,
( ~ c_WellType_OWT(A,C,D,E)
| c_WellTypeRT_OWTrt(A,B,C,D,E) ),
inference(clausify,[status(thm)],[cls_WT__implies__WTrt_0]) ).
fof(cls_WTrt__env__mono_0,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( ~ c_WellTypeRT_OWTrt(VAR_0,VAR_1,VAR_5,VAR_3,VAR_4)
| ~ c_Map_Omap__le(VAR_5,VAR_2,tc_List_Olist(tc_String_Ochar),tc_Type_Oty)
| c_WellTypeRT_OWTrt(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4) ),
file('theBenchmark.p',cls_WTrt__env__mono_0) ).
cnf(c_72,plain,
( ~ c_WellTypeRT_OWTrt(A,B,F,D,E)
| ~ c_Map_Omap__le(F,C,tc_List_Olist(tc_String_Ochar),tc_Type_Oty)
| c_WellTypeRT_OWTrt(A,B,C,D,E) ),
inference(clausify,[status(thm)],[cls_WTrt__env__mono_0]) ).
fof(cls_map__add__upds_0,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] : c_Map_Omap__add(VAR_0,c_Map_Omap__upds(VAR_1,VAR_2,VAR_3,VAR_4,VAR_5),VAR_4,VAR_5) = c_Map_Omap__upds(c_Map_Omap__add(VAR_0,VAR_1,VAR_4,VAR_5),VAR_2,VAR_3,VAR_4,VAR_5),
file('theBenchmark.p',cls_map__add__upds_0) ).
cnf(c_87,plain,
c_Map_Omap__add(A,c_Map_Omap__upds(B,C,D,E,F),E,F) = c_Map_Omap__upds(c_Map_Omap__add(A,B,E,F),C,D,E,F),
inference(clausify,[status(thm)],[cls_map__add__upds_0]) ).
cnf(c_88,plain,
c_Map_Omap__upds(c_Map_Omap__add(A,B,C,D),E,F,C,D) = c_Map_Omap__add(A,c_Map_Omap__upds(B,E,F,C,D),C,D),
inference(copy,[status(thm)],[c_87]) ).
fof(cls_map__le__map__add_0,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : c_Map_Omap__le(VAR_0,c_Map_Omap__add(VAR_1,VAR_0,VAR_2,VAR_3),VAR_2,VAR_3),
file('theBenchmark.p',cls_map__le__map__add_0) ).
cnf(c_251,plain,
c_Map_Omap__le(A,c_Map_Omap__add(B,A,C,D),C,D),
inference(clausify,[status(thm)],[cls_map__le__map__add_0]) ).
fof(cls_map__add__empty_0,axiom,
! [VAR_0,VAR_1,VAR_2] : c_Map_Omap__add(VAR_0,c_COMBK(c_Option_Ooption_ONone(VAR_1),tc_Option_Ooption(VAR_1),VAR_2),VAR_2,VAR_1) = VAR_0,
file('theBenchmark.p',cls_map__add__empty_0) ).
cnf(c_307,plain,
c_Map_Omap__add(A,c_COMBK(c_Option_Ooption_ONone(B),tc_Option_Ooption(B),C),C,B) = A,
inference(clausify,[status(thm)],[cls_map__add__empty_0]) ).
cnf(c_1020,plain,
c_WellTypeRT_OWTrt(v_P,A,c_Map_Omap__upds(c_COMBK(c_Option_Ooption_ONone(tc_Type_Oty),tc_Option_Ooption(tc_Type_Oty),tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____),
inference(resolve,[status(thm)],[c_50,c_39]) ).
cnf(c_1169,plain,
( ~ c_WellTypeRT_OWTrt(A,B,D,E,F)
| c_WellTypeRT_OWTrt(A,B,c_Map_Omap__add(C,D,tc_List_Olist(tc_String_Ochar),tc_Type_Oty),E,F) ),
inference(resolve,[status(thm)],[c_251,c_72]) ).
cnf(c_11200,plain,
c_Map_Omap__upds(A,B,C,D,E) = c_Map_Omap__add(A,c_Map_Omap__upds(c_COMBK(c_Option_Ooption_ONone(E),tc_Option_Ooption(E),D),B,C,D,E),D,E),
inference(paramod,[status(thm)],[c_307,c_88]) ).
cnf(c_1219,plain,
c_Map_Omap__add(A,c_Map_Omap__upds(c_COMBK(c_Option_Ooption_ONone(B),tc_Option_Ooption(B),C),D,E,C,B),C,B) = c_Map_Omap__upds(A,D,E,C,B),
inference(copy,[status(thm)],[c_11200]) ).
cnf(c_11201,plain,
c_WellTypeRT_OWTrt(v_P,A,c_Map_Omap__add(B,c_Map_Omap__upds(c_COMBK(c_Option_Ooption_ONone(tc_Type_Oty),tc_Option_Ooption(tc_Type_Oty),tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____),
inference(resolve,[status(thm)],[c_1169,c_1020]) ).
cnf(c_11198,plain,
c_WellTypeRT_OWTrt(v_P,A,c_Map_Omap__upds(B,c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____),
inference(paramod,[status(thm)],[c_1219,c_11201]) ).
cnf(c_11199,plain,
$false,
inference(resolve,[status(thm)],[c_11198,c_26]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV938-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/5.38 % Computer : n007.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Sat Sep 26 15:10:15 UTC 2026
% 0.11/5.38 % CPUTime :
% 0.11/5.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/5.38 % Process 4043614 was started by sandbox on n007,
% 0.11/5.38 % Sat Sep 26 15:10:15 2026
% 0.11/5.38 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.15/5.40
% 0.15/5.40 % From the command line: assign(max_seconds, 300).
% 28.57/9.54
% 28.57/9.54 % given #500 (I,wt=44): 749 hBOOL(hAPP(A,c_Type_Oty_Oty__case(B,C,D,B,E,F,t_a))) | c_Type_Oty_OClass(v_sko__Type__Xty__Xsplit__1(A,E,F)) = F | -hBOOL(hAPP(A,B)) | c_Type_Oty_OInteger = F | -hBOOL(hAPP(A,C)). [factor(562,c,f)].
% 28.57/9.54
% 28.57/9.54 % SZS status Unsatisfiable for theBenchmark
% 28.57/9.54
% 28.57/9.54 % Proof 1 at 3.60 (+ 0.45) seconds.
% 28.57/9.54 % Length of proof is 13.
% 28.57/9.54 % Level of proof is 4.
% 28.57/9.54 % Maximum clause weight is 47.000.
% 28.57/9.54 % Given clauses 899.
% 28.57/9.54
% 28.57/9.54 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------