%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWW293+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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:14:03 AM UTC 2026
% Result : Theorem 237.67s 34.65s
% Output : CNFRefutation 237.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 4
% Syntax : Number of formulae : 19 ( 8 unt; 0 def)
% Number of atoms : 57 ( 10 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 62 ( 24 ~; 21 |; 12 &)
% ( 1 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 6 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-4 aty)
% Number of functors : 17 ( 17 usr; 9 con; 0-5 aty)
% Number of variables : 89 ( 2 sgn 69 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_triple__valid__def2,axiom,
! [V_Qa_2,V_c_2,V_Pa_2,V_n_2,T_b] :
( c_Hoare__Mirabelle_Otriple__valid(T_b,V_n_2,hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(T_b),V_Pa_2),V_c_2),V_Qa_2))
<=> ! [B_Z,B_s] :
( hBOOL(hAPP(hAPP(V_Pa_2,B_Z),B_s))
=> ! [B_s_H] :
( c_Natural_Oevaln(V_c_2,B_s,V_n_2,B_s_H)
=> hBOOL(hAPP(hAPP(V_Qa_2,B_Z),B_s_H)) ) ) ),
file('theBenchmark.p',fact_triple__valid__def2) ).
fof(fact_evaln__elim__cases_I6_J,axiom,
! [V_s1,V_n,V_s,V_P] :
( c_Natural_Oevaln(hAPP(c_Com_Ocom_OBODY,V_P),V_s,V_n,V_s1)
=> ~ ! [B_n] :
( V_n = hAPP(c_Nat_OSuc,B_n)
=> ~ c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,V_P)),V_s,B_n,V_s1) ) ),
file('theBenchmark.p',fact_evaln__elim__cases_I6_J) ).
fof(fact_Suc__neq__Zero,axiom,
! [V_m] : hAPP(c_Nat_OSuc,V_m) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
file('theBenchmark.p',fact_Suc__neq__Zero) ).
fof(conj_0,conjecture,
c_Hoare__Mirabelle_Otriple__valid(t_a,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Com_Ocom_OBODY,v_pn)),v_Q)),
file('theBenchmark.p',conj_0) ).
fof(conj_0_neg,negated_conjecture,
~ c_Hoare__Mirabelle_Otriple__valid(t_a,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Com_Ocom_OBODY,v_pn)),v_Q)),
inference(assume_negation,[status(cth)],[conj_0]) ).
fof(nnf_326,plain,
! [V_s1,V_n,V_s,V_P] :
( ? [B_n] :
( c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,V_P)),V_s,B_n,V_s1)
& hAPP(c_Nat_OSuc,B_n) = V_n )
| ~ c_Natural_Oevaln(hAPP(c_Com_Ocom_OBODY,V_P),V_s,V_n,V_s1) ),
inference(fof_nnf,[status(thm)],[fact_evaln__elim__cases_I6_J]) ).
fof(sk_fact_evaln__elim__cases_I6_J_sk,plain,
! [V_s1,V_n,V_s,V_P] :
( ( c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,V_P)),V_s,sK0(V_s1,V_n,V_s,V_P),V_s1)
& hAPP(c_Nat_OSuc,sK0(V_s1,V_n,V_s,V_P)) = V_n )
| ~ c_Natural_Oevaln(hAPP(c_Com_Ocom_OBODY,V_P),V_s,V_n,V_s1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(B_n,sK0(V_s1,V_n,V_s,V_P))],[nnf_326]) ).
fof(sk_fact_evaln__elim__cases_I6_J,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,VAR_0)),VAR_1,sK0(VAR_3,VAR_2,VAR_1,VAR_0),VAR_3)
| ~ c_Natural_Oevaln(hAPP(c_Com_Ocom_OBODY,VAR_0),VAR_1,VAR_2,VAR_3) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( hAPP(c_Nat_OSuc,sK0(VAR_3,VAR_2,VAR_1,VAR_0)) = VAR_2
| ~ c_Natural_Oevaln(hAPP(c_Com_Ocom_OBODY,VAR_0),VAR_1,VAR_2,VAR_3) ) ),
inference(cnf_transformation,[status(thm)],[sk_fact_evaln__elim__cases_I6_J_sk]) ).
cnf(c_896,plain,
( hAPP(c_Nat_OSuc,sK0(D,C,B,A)) = C
| ~ c_Natural_Oevaln(hAPP(c_Com_Ocom_OBODY,A),B,C,D) ),
inference(split_conjunct,[status(thm)],[sk_fact_evaln__elim__cases_I6_J]) ).
cnf(c_913,plain,
c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != hAPP(c_Nat_OSuc,A),
inference(clausify,[status(thm)],[fact_Suc__neq__Zero]) ).
cnf(c_914,plain,
hAPP(c_Nat_OSuc,A) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(copy,[status(thm)],[c_913]) ).
fof(nnf_5,plain,
! [V_Qa_2,V_c_2,V_Pa_2,V_n_2,T_b] :
( ( ? [B_Z,B_s] :
( ? [B_s_H] :
( ~ hBOOL(hAPP(hAPP(V_Qa_2,B_Z),B_s_H))
& c_Natural_Oevaln(V_c_2,B_s,V_n_2,B_s_H) )
& hBOOL(hAPP(hAPP(V_Pa_2,B_Z),B_s)) )
| c_Hoare__Mirabelle_Otriple__valid(T_b,V_n_2,hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(T_b),V_Pa_2),V_c_2),V_Qa_2)) )
& ( ! [X0,X1] :
( ! [X2] :
( hBOOL(hAPP(hAPP(V_Qa_2,X0),X2))
| ~ c_Natural_Oevaln(V_c_2,X1,V_n_2,X2) )
| ~ hBOOL(hAPP(hAPP(V_Pa_2,X0),X1)) )
| ~ c_Hoare__Mirabelle_Otriple__valid(T_b,V_n_2,hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(T_b),V_Pa_2),V_c_2),V_Qa_2)) ) ),
inference(fof_nnf,[status(thm)],[fact_triple__valid__def2]) ).
fof(sk_fact_triple__valid__def2_sk,plain,
! [V_Qa_2,V_c_2,V_Pa_2,V_n_2,T_b] :
( ( ( ~ hBOOL(hAPP(hAPP(V_Qa_2,sK3(V_Qa_2,V_c_2,V_Pa_2,V_n_2,T_b)),sK2(V_Qa_2,V_c_2,V_Pa_2,V_n_2,T_b)))
& c_Natural_Oevaln(V_c_2,sK1(V_Qa_2,V_c_2,V_Pa_2,V_n_2,T_b),V_n_2,sK2(V_Qa_2,V_c_2,V_Pa_2,V_n_2,T_b))
& hBOOL(hAPP(hAPP(V_Pa_2,sK3(V_Qa_2,V_c_2,V_Pa_2,V_n_2,T_b)),sK1(V_Qa_2,V_c_2,V_Pa_2,V_n_2,T_b))) )
| c_Hoare__Mirabelle_Otriple__valid(T_b,V_n_2,hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(T_b),V_Pa_2),V_c_2),V_Qa_2)) )
& ( ! [X0,X1] :
( ! [X2] :
( hBOOL(hAPP(hAPP(V_Qa_2,X0),X2))
| ~ c_Natural_Oevaln(V_c_2,X1,V_n_2,X2) )
| ~ hBOOL(hAPP(hAPP(V_Pa_2,X0),X1)) )
| ~ c_Hoare__Mirabelle_Otriple__valid(T_b,V_n_2,hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(T_b),V_Pa_2),V_c_2),V_Qa_2)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK1,sK2]),skolemize(B_Z,sK3(V_Qa_2,V_c_2,V_Pa_2,V_n_2,T_b)),skolemize(B_s,sK1(V_Qa_2,V_c_2,V_Pa_2,V_n_2,T_b)),skolemize(B_s_H,sK2(V_Qa_2,V_c_2,V_Pa_2,V_n_2,T_b))],[nnf_5]) ).
fof(sk_fact_triple__valid__def2,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ hBOOL(hAPP(hAPP(VAR_4,sK3(VAR_4,VAR_3,VAR_2,VAR_1,VAR_0)),sK2(VAR_4,VAR_3,VAR_2,VAR_1,VAR_0)))
| c_Hoare__Mirabelle_Otriple__valid(VAR_0,VAR_1,hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(VAR_0),VAR_2),VAR_3),VAR_4)) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( c_Natural_Oevaln(VAR_3,sK1(VAR_4,VAR_3,VAR_2,VAR_1,VAR_0),VAR_1,sK2(VAR_4,VAR_3,VAR_2,VAR_1,VAR_0))
| c_Hoare__Mirabelle_Otriple__valid(VAR_0,VAR_1,hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(VAR_0),VAR_2),VAR_3),VAR_4)) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( hBOOL(hAPP(hAPP(VAR_2,sK3(VAR_4,VAR_3,VAR_2,VAR_1,VAR_0)),sK1(VAR_4,VAR_3,VAR_2,VAR_1,VAR_0)))
| c_Hoare__Mirabelle_Otriple__valid(VAR_0,VAR_1,hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(VAR_0),VAR_2),VAR_3),VAR_4)) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7] :
( hBOOL(hAPP(hAPP(VAR_4,VAR_5),VAR_7))
| ~ c_Natural_Oevaln(VAR_3,VAR_6,VAR_1,VAR_7)
| ~ hBOOL(hAPP(hAPP(VAR_2,VAR_5),VAR_6))
| ~ c_Hoare__Mirabelle_Otriple__valid(VAR_0,VAR_1,hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(VAR_0),VAR_2),VAR_3),VAR_4)) ) ),
inference(cnf_transformation,[status(thm)],[sk_fact_triple__valid__def2_sk]) ).
cnf(c_1912,plain,
( c_Natural_Oevaln(D,sK1(E,D,C,B,A),B,sK2(E,D,C,B,A))
| c_Hoare__Mirabelle_Otriple__valid(A,B,hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(A),C),D),E)) ),
inference(split_conjunct,[status(thm)],[sk_fact_triple__valid__def2]) ).
cnf(c_2260,negated_conjecture,
~ c_Hoare__Mirabelle_Otriple__valid(t_a,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Com_Ocom_OBODY,v_pn)),v_Q)),
inference(clausify,[status(thm)],[conj_0_neg]) ).
cnf(c_3326,plain,
( hAPP(c_Nat_OSuc,sK0(sK2(E,hAPP(c_Com_Ocom_OBODY,D),C,B,A),B,sK1(E,hAPP(c_Com_Ocom_OBODY,D),C,B,A),D)) = B
| c_Hoare__Mirabelle_Otriple__valid(A,B,hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(A),C),hAPP(c_Com_Ocom_OBODY,D)),E)) ),
inference(resolve,[status(thm)],[c_1912,c_896]) ).
cnf(c_35561,negated_conjecture,
hAPP(c_Nat_OSuc,sK0(sK2(v_Q,hAPP(c_Com_Ocom_OBODY,v_pn),v_P,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),t_a),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),sK1(v_Q,hAPP(c_Com_Ocom_OBODY,v_pn),v_P,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),t_a),v_pn)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(resolve,[status(thm)],[c_3326,c_2260]) ).
cnf(c_35560,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_914,c_35561]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW293+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n020.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Sat Sep 26 15:37:03 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.17/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.45 % Process 1912812 was started by sandbox2 on n020,
% 0.17/0.45 % Sat Sep 26 15:37:03 2026
% 0.17/0.45 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 237.67/34.65
% 237.67/34.65 % SInE (scan): 566 to sos (tol 1.5x), 333 to usable (tol 2.0x), 4305 zapped, of 5204 axioms (depth 3).
% 237.67/34.65
% 237.67/34.65 % From the command line: assign(max_seconds, 300).
% 237.67/34.65
% 237.67/34.65 % given #500 (F,wt=33): 15706 hAPP(c_Nat_Osize__class_Osize(tc_Com_Ocom),c_Com_Ocom_OSemi(c_Com_Ocom_OSKIP,c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) != hAPP(c_Nat_Osize__class_Osize(tc_Com_Ocom),c_Orderings_Obot__class_Obot(tc_Nat_Onat)). [para(7399(a,1),15701(a,1,2))].
% 237.67/34.65
% 237.67/34.65 % given #1000 (W,wt=30): 13725 hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OCond(A,c_Com_Ocom_OSKIP,c_Com_Ocom_OLocal(B,C,c_Com_Ocom_OSKIP)))). [resolve(12372,b,12198,a)].
% 237.67/34.65
% 237.67/34.65 % given #1500 (F,wt=29): 29914 hAPP(c_Groups_Ouminus__class_Ouminus(tc_Int_Oint),c_Int_OBit0(c_Int_OBit1(c_Int_OPls))) != c_Groups_Oone__class_Oone(tc_Int_Oint). [para(2347(a,1),7368(a,1,2)),rewrite([18687(9)])].
% 237.67/34.65
% 237.67/34.65 % given #2000 (T,wt=30): 30670 -hBOOL(c_Groups_Oone__class_Oone(tc_Nat_Onat)) | c_Natural_Oevaln(c_Com_Ocom_OCond(c_Nat_OSuc,c_Com_Ocom_OSemi(c_Com_Ocom_OSKIP,c_Com_Ocom_OSKIP),A),c_Orderings_Obot__class_Obot(tc_Nat_Onat),B,c_Orderings_Obot__class_Obot(tc_Nat_Onat)). [back_unit_del(25119),unit_del(a,30594)].
% 237.67/34.65
% 237.67/34.65 % given #2500 (F,wt=65): 30819 -hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),hAPP(c_Set_Oimage(tc_Int_Oint,tc_Nat_Onat,c_Int_Onat),hAPP(c_Set_Oimage(tc_Nat_Onat,tc_Int_Oint,c_Nat_Osemiring__1__class_Oof__nat(tc_Int_Oint)),c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))). [resolve(30742,a,1550,a(flip)),rewrite([30705(17)])].
% 237.67/34.65
% 237.67/34.65 % given #3000 (T,wt=29): 35024 c_Natural_Oevaln(hAPP(c_Int_Onumber__class_Onumber__of(tc_Int_Oint),c_Com_Ocom_OSemi(c_Com_Ocom_OSKIP,c_Com_Ocom_OSKIP)),c_Com_Ocom_OWhile(A,c_Com_Ocom_OSKIP),B,c_Com_Ocom_OWhile(A,c_Com_Ocom_OSKIP)). [resolve(34987,a,14765,a)].
% 237.67/34.65
% 237.67/34.65 % SZS status Theorem for theBenchmark
% 237.67/34.65
% 237.67/34.65 % Proof 1 at 27.40 (+ 6.42) seconds.
% 237.67/34.65 % Length of proof is 11.
% 237.67/34.65 % Level of proof is 3.
% 237.67/34.65 % Maximum clause weight is 76.000.
% 237.67/34.65 % Given clauses 3161.
% 237.67/34.65
% 237.67/34.65 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------