%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV954-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 : n013.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:23 AM UTC 2026
% Result : Unsatisfiable 0.57s 0.48s
% Output : CNFRefutation 0.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 4
% Syntax : Number of formulae : 12 ( 7 unt; 0 def)
% Number of atoms : 19 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 14 ( 7 ~; 7 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 2 prp; 0-5 aty)
% Number of functors : 13 ( 13 usr; 9 con; 0-7 aty)
% Number of variables : 19 ( 3 sgn 9 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cls_conjecture_0,axiom,
~ v_thesis____,
file('theBenchmark.p',cls_conjecture_0) ).
cnf(c_25,plain,
~ v_thesis____,
inference(clausify,[status(thm)],[cls_conjecture_0]) ).
fof(cls_CHAINED_0,axiom,
c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OFAss(v_ea____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),v_T____),
file('theBenchmark.p',cls_CHAINED_0) ).
cnf(c_26,plain,
c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OFAss(v_ea____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),v_T____),
inference(clausify,[status(thm)],[cls_CHAINED_0]) ).
fof(cls_that_0,axiom,
! [VAR_0] :
( ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,VAR_0)
| v_thesis____ ),
file('theBenchmark.p',cls_that_0) ).
cnf(c_27,plain,
( ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,A)
| v_thesis____ ),
inference(clausify,[status(thm)],[cls_that_0]) ).
cnf(c_28,plain,
~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,A),
inference(resolve,[status(thm)],[c_25,c_27]) ).
fof(cls_WTrt__elim__cases_I8_J_11,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7] :
( ~ c_WellTypeRT_OWTrt(VAR_0,VAR_1,VAR_2,c_Expr_Oexp_OFAss(VAR_6,VAR_5,VAR_4,VAR_3,tc_List_Olist(tc_String_Ochar)),VAR_7)
| c_WellTypeRT_OWTrt(VAR_0,VAR_1,VAR_2,VAR_3,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(VAR_4,VAR_2,VAR_5,VAR_0,VAR_6,VAR_1,VAR_3))
| c_WellTypeRT_OWTrt(VAR_0,VAR_1,VAR_2,VAR_3,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__4(VAR_2,VAR_0,VAR_1,VAR_3)) ),
file('theBenchmark.p',cls_WTrt__elim__cases_I8_J_11) ).
cnf(c_143,plain,
( ~ c_WellTypeRT_OWTrt(A,B,C,c_Expr_Oexp_OFAss(V6,F,E,D,tc_List_Olist(tc_String_Ochar)),V7)
| c_WellTypeRT_OWTrt(A,B,C,D,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(E,C,F,A,V6,B,D))
| c_WellTypeRT_OWTrt(A,B,C,D,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__4(C,A,B,D)) ),
inference(clausify,[status(thm)],[cls_WTrt__elim__cases_I8_J_11]) ).
cnf(c_438,plain,
( c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))
| c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__4(v_E____,v_P,v_ha____,v_e_092_060_094isub_0622____)) ),
inference(resolve,[status(thm)],[c_143,c_26]) ).
cnf(c_439,plain,
c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),
inference(resolve,[status(thm)],[c_28,c_438]) ).
cnf(c_437,plain,
$false,
inference(resolve,[status(thm)],[c_28,c_439]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV954-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.10/0.36 % Computer : n013.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sat Sep 26 15:13:21 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 3024991 was started by sandbox on n013,
% 0.10/0.37 % Sat Sep 26 15:13:21 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.40
% 0.10/0.40 % From the command line: assign(max_seconds, 300).
% 0.57/0.48
% 0.57/0.48 % SZS status Unsatisfiable for theBenchmark
% 0.57/0.48
% 0.57/0.48 % Proof 1 at 0.05 (+ 0.01) seconds.
% 0.57/0.48 % Length of proof is 6.
% 0.57/0.48 % Level of proof is 2.
% 0.57/0.48 % Maximum clause weight is 50.000.
% 0.57/0.48 % Given clauses 119.
% 0.57/0.48
% 0.57/0.48 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------