%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV849-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 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 : Fri Sep 25 03:14:13 PM UTC 2026
% Result : Unsatisfiable 30.87s 4.49s
% Output : Proof 30.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 13
% Syntax : Number of formulae : 102 ( 21 unt; 0 def)
% Number of atoms : 290 ( 30 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 332 ( 144 ~; 188 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-4 aty)
% Number of functors : 18 ( 18 usr; 13 con; 0-2 aty)
% Number of variables : 80 ( 12 sgn 26 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f462,negated_conjecture,
v_ca = v_c,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f462_nnf,plain,
v_ca = v_c,
inference(nnf_transformation,[status(thm)],[f462]) ).
cnf(c462,plain,
v_ca = v_c,
inference(cnf_transformation,[status(esa)],[f462_nnf]) ).
cnf(f461,negated_conjecture,
v_ba = v_b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f461_nnf,plain,
v_ba = v_b,
inference(nnf_transformation,[status(thm)],[f461]) ).
cnf(c461,plain,
v_ba = v_b,
inference(cnf_transformation,[status(esa)],[f461_nnf]) ).
cnf(f470,negated_conjecture,
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,V_Z),v_s1))
| hBOOL(hAPP(hAPP(v_P,V_Z),v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_12) ).
fof(f470_nnf,plain,
! [V_Z] :
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,V_Z),v_s1))
| hBOOL(hAPP(hAPP(v_P,V_Z),v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ),
inference(nnf_transformation,[status(thm)],[f470]) ).
fof(f470_sk,plain,
! [V_Z] :
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,V_Z),v_s1))
| hBOOL(hAPP(hAPP(v_P,V_Z),v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ),
inference(skolemisation,[status(esa)],[f470_nnf]) ).
cnf(c470,plain,
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s1))
| hBOOL(hAPP(hAPP(v_P,X0),v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ),
inference(cnf_transformation,[status(esa)],[f470_sk]) ).
cnf(p535,plain,
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s1))
| hBOOL(hAPP(hAPP(v_P,X0),v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_ba,v_c) ),
inference(superposition,[status(thm)],[c461,c470]) ).
cnf(p544,plain,
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s1))
| hBOOL(hAPP(hAPP(v_P,X0),v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_ba,v_ca) ),
inference(superposition,[status(thm)],[c462,p535]) ).
cnf(p558,plain,
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s1))
| hBOOL(hAPP(hAPP(v_P,X0),v_s2)) ),
inference(equality_resolution,[status(thm)],[p544]) ).
cnf(f474,negated_conjecture,
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(V_na)),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,V_Z),V_s))
| ~ hBOOL(hAPP(v_b,V_s))
| ~ c_Natural_Oevaln(v_c,V_s,V_na,V_s_H)
| hBOOL(hAPP(hAPP(v_P,V_Z),V_s_H)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_16) ).
fof(f474_nnf,plain,
! [V_Z,V_s_H,V_s,V_na] :
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(V_na)),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,V_Z),V_s))
| ~ hBOOL(hAPP(v_b,V_s))
| ~ c_Natural_Oevaln(v_c,V_s,V_na,V_s_H)
| hBOOL(hAPP(hAPP(v_P,V_Z),V_s_H)) ),
inference(nnf_transformation,[status(thm)],[f474]) ).
fof(f474_sk,plain,
! [V_Z,V_s_H,V_s,V_na] :
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(V_na)),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,V_Z),V_s))
| ~ hBOOL(hAPP(v_b,V_s))
| ~ c_Natural_Oevaln(v_c,V_s,V_na,V_s_H)
| hBOOL(hAPP(hAPP(v_P,V_Z),V_s_H)) ),
inference(skolemisation,[status(esa)],[f474_nnf]) ).
cnf(c474,plain,
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(X3)),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,X0),X2))
| ~ hBOOL(hAPP(v_b,X2))
| ~ c_Natural_Oevaln(v_c,X2,X3,X1)
| hBOOL(hAPP(hAPP(v_P,X0),X1)) ),
inference(cnf_transformation,[status(esa)],[f474_sk]) ).
cnf(p539,plain,
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(X3)),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,X0),X2))
| ~ hBOOL(hAPP(v_b,X2))
| ~ c_Natural_Oevaln(v_ca,X2,X3,X1)
| hBOOL(hAPP(hAPP(v_P,X0),X1)) ),
inference(superposition,[status(thm)],[c462,c474]) ).
cnf(f459,negated_conjecture,
c_Natural_Oevaln(v_ca,v_s0,v_na,v_s1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f459_nnf,plain,
c_Natural_Oevaln(v_ca,v_s0,v_na,v_s1),
inference(nnf_transformation,[status(thm)],[f459]) ).
cnf(c459,plain,
c_Natural_Oevaln(v_ca,v_s0,v_na,v_s1),
inference(cnf_transformation,[status(esa)],[f459_nnf]) ).
cnf(p549,plain,
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(v_na)),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s0))
| ~ hBOOL(hAPP(v_b,v_s0))
| hBOOL(hAPP(hAPP(v_P,X0),v_s1)) ),
inference(resolution,[status(thm)],[p539,c459]) ).
cnf(p550,plain,
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(v_na)),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s0))
| ~ hBOOL(hAPP(v_ba,v_s0))
| hBOOL(hAPP(hAPP(v_P,X0),v_s1)) ),
inference(superposition,[status(thm)],[c461,p549]) ).
cnf(f458,negated_conjecture,
hBOOL(hAPP(v_ba,v_s0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f458_nnf,plain,
hBOOL(hAPP(v_ba,v_s0)),
inference(nnf_transformation,[status(thm)],[f458]) ).
cnf(c458,plain,
hBOOL(hAPP(v_ba,v_s0)),
inference(cnf_transformation,[status(esa)],[f458_nnf]) ).
cnf(p551,plain,
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(v_na)),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s0))
| hBOOL(hAPP(hAPP(v_P,X0),v_s1)) ),
inference(resolution,[status(thm)],[p550,c458]) ).
cnf(f463,negated_conjecture,
hBOOL(hAPP(hAPP(v_P,v_xb),v_s0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_5) ).
fof(f463_nnf,plain,
hBOOL(hAPP(hAPP(v_P,v_xb),v_s0)),
inference(nnf_transformation,[status(thm)],[f463]) ).
cnf(c463,plain,
hBOOL(hAPP(hAPP(v_P,v_xb),v_s0)),
inference(cnf_transformation,[status(esa)],[f463_nnf]) ).
cnf(p553,plain,
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(v_na)),v_G))
| hBOOL(hAPP(hAPP(v_P,v_xb),v_s1)) ),
inference(resolution,[status(thm)],[p551,c463]) ).
cnf(f464,negated_conjecture,
( ~ hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),V_x),v_G))
| c_Hoare__Mirabelle_Otriple__valid(v_na,V_x,t_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_6) ).
fof(f464_nnf,plain,
! [V_x] :
( ~ hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),V_x),v_G))
| c_Hoare__Mirabelle_Otriple__valid(v_na,V_x,t_a) ),
inference(nnf_transformation,[status(thm)],[f464]) ).
fof(f464_sk,plain,
! [V_x] :
( ~ hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),V_x),v_G))
| c_Hoare__Mirabelle_Otriple__valid(v_na,V_x,t_a) ),
inference(skolemisation,[status(esa)],[f464_nnf]) ).
cnf(c464,plain,
( ~ hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),X0),v_G))
| c_Hoare__Mirabelle_Otriple__valid(v_na,X0,t_a) ),
inference(cnf_transformation,[status(esa)],[f464_sk]) ).
cnf(p554,plain,
( c_Hoare__Mirabelle_Otriple__valid(v_na,v_n(v_na),t_a)
| hBOOL(hAPP(hAPP(v_P,v_xb),v_s1)) ),
inference(resolution,[status(thm)],[p553,c464]) ).
cnf(p559,plain,
( c_Hoare__Mirabelle_Otriple__valid(v_na,v_n(v_na),t_a)
| hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_G))
| hBOOL(hAPP(hAPP(v_P,v_xb),v_s2)) ),
inference(resolution,[status(thm)],[p558,p554]) ).
cnf(p560,plain,
( c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a)
| c_Hoare__Mirabelle_Otriple__valid(v_na,v_n(v_na),t_a)
| hBOOL(hAPP(hAPP(v_P,v_xb),v_s2)) ),
inference(resolution,[status(thm)],[p559,c464]) ).
cnf(f465,negated_conjecture,
( ~ hBOOL(hAPP(hAPP(v_P,v_xb),v_s2))
| hBOOL(hAPP(v_b,v_s2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_7) ).
fof(f465_nnf,plain,
( ~ hBOOL(hAPP(hAPP(v_P,v_xb),v_s2))
| hBOOL(hAPP(v_b,v_s2)) ),
inference(nnf_transformation,[status(thm)],[f465]) ).
fof(f465_sk,plain,
( ~ hBOOL(hAPP(hAPP(v_P,v_xb),v_s2))
| hBOOL(hAPP(v_b,v_s2)) ),
inference(skolemisation,[status(esa)],[f465_nnf]) ).
cnf(c465,plain,
( ~ hBOOL(hAPP(hAPP(v_P,v_xb),v_s2))
| hBOOL(hAPP(v_b,v_s2)) ),
inference(cnf_transformation,[status(esa)],[f465_sk]) ).
cnf(p562,plain,
( hBOOL(hAPP(v_b,v_s2))
| c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a)
| c_Hoare__Mirabelle_Otriple__valid(v_na,v_n(v_na),t_a) ),
inference(resolution,[status(thm)],[p560,c465]) ).
cnf(f475,negated_conjecture,
( ~ c_Hoare__Mirabelle_Otriple__valid(V_na,v_n(V_na),t_a)
| ~ hBOOL(hAPP(hAPP(v_P,V_Za),V_sa))
| ~ hBOOL(hAPP(v_b,V_sa))
| ~ c_Natural_Oevaln(v_c,V_sa,V_na,V_s_Ha)
| hBOOL(hAPP(hAPP(v_P,V_Za),V_s_Ha)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_17) ).
fof(f475_nnf,plain,
! [V_Za,V_s_Ha,V_sa,V_na] :
( ~ c_Hoare__Mirabelle_Otriple__valid(V_na,v_n(V_na),t_a)
| ~ hBOOL(hAPP(hAPP(v_P,V_Za),V_sa))
| ~ hBOOL(hAPP(v_b,V_sa))
| ~ c_Natural_Oevaln(v_c,V_sa,V_na,V_s_Ha)
| hBOOL(hAPP(hAPP(v_P,V_Za),V_s_Ha)) ),
inference(nnf_transformation,[status(thm)],[f475]) ).
fof(f475_sk,plain,
! [V_Za,V_s_Ha,V_sa,V_na] :
( ~ c_Hoare__Mirabelle_Otriple__valid(V_na,v_n(V_na),t_a)
| ~ hBOOL(hAPP(hAPP(v_P,V_Za),V_sa))
| ~ hBOOL(hAPP(v_b,V_sa))
| ~ c_Natural_Oevaln(v_c,V_sa,V_na,V_s_Ha)
| hBOOL(hAPP(hAPP(v_P,V_Za),V_s_Ha)) ),
inference(skolemisation,[status(esa)],[f475_nnf]) ).
cnf(c475,plain,
( ~ c_Hoare__Mirabelle_Otriple__valid(X3,v_n(X3),t_a)
| ~ hBOOL(hAPP(hAPP(v_P,X0),X2))
| ~ hBOOL(hAPP(v_b,X2))
| ~ c_Natural_Oevaln(v_c,X2,X3,X1)
| hBOOL(hAPP(hAPP(v_P,X0),X1)) ),
inference(cnf_transformation,[status(esa)],[f475_sk]) ).
cnf(p537,plain,
( ~ c_Hoare__Mirabelle_Otriple__valid(X3,v_n(X3),t_a)
| ~ hBOOL(hAPP(hAPP(v_P,X0),X2))
| ~ hBOOL(hAPP(v_b,X2))
| ~ c_Natural_Oevaln(v_ca,X2,X3,X1)
| hBOOL(hAPP(hAPP(v_P,X0),X1)) ),
inference(superposition,[status(thm)],[c462,c475]) ).
cnf(p540,plain,
( ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_n(v_na),t_a)
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s0))
| ~ hBOOL(hAPP(v_b,v_s0))
| hBOOL(hAPP(hAPP(v_P,X0),v_s1)) ),
inference(resolution,[status(thm)],[p537,c459]) ).
cnf(p541,plain,
( ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_n(v_na),t_a)
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s0))
| ~ hBOOL(hAPP(v_ba,v_s0))
| hBOOL(hAPP(hAPP(v_P,X0),v_s1)) ),
inference(superposition,[status(thm)],[c461,p540]) ).
cnf(p542,plain,
( ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_n(v_na),t_a)
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s0))
| hBOOL(hAPP(hAPP(v_P,X0),v_s1)) ),
inference(resolution,[status(thm)],[p541,c458]) ).
cnf(p543,plain,
( ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_n(v_na),t_a)
| hBOOL(hAPP(hAPP(v_P,v_xb),v_s1)) ),
inference(resolution,[status(thm)],[p542,c463]) ).
cnf(p563,plain,
( hBOOL(hAPP(hAPP(v_P,v_xb),v_s1))
| hBOOL(hAPP(v_b,v_s2))
| c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a) ),
inference(resolution,[status(thm)],[p562,p543]) ).
cnf(p564,plain,
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_G))
| hBOOL(hAPP(hAPP(v_P,v_xb),v_s2))
| hBOOL(hAPP(v_b,v_s2))
| c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a) ),
inference(resolution,[status(thm)],[p563,p558]) ).
cnf(p565,plain,
( c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a)
| hBOOL(hAPP(hAPP(v_P,v_xb),v_s2))
| hBOOL(hAPP(v_b,v_s2))
| c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a) ),
inference(resolution,[status(thm)],[p564,c464]) ).
cnf(p567,plain,
( hBOOL(hAPP(hAPP(v_P,v_xb),v_s2))
| hBOOL(hAPP(v_b,v_s2))
| c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a) ),
inference(factoring,[status(thm)],[p565]) ).
cnf(p568,plain,
( hBOOL(hAPP(v_b,v_s2))
| hBOOL(hAPP(v_b,v_s2))
| c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a) ),
inference(resolution,[status(thm)],[p567,c465]) ).
cnf(p569,plain,
( hBOOL(hAPP(v_b,v_s2))
| c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a) ),
inference(factoring,[status(thm)],[p568]) ).
cnf(f472,negated_conjecture,
( ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a)
| ~ hBOOL(hAPP(hAPP(v_P,V_Za),v_s1))
| hBOOL(hAPP(hAPP(v_P,V_Za),v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_14) ).
fof(f472_nnf,plain,
! [V_Za] :
( ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a)
| ~ hBOOL(hAPP(hAPP(v_P,V_Za),v_s1))
| hBOOL(hAPP(hAPP(v_P,V_Za),v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ),
inference(nnf_transformation,[status(thm)],[f472]) ).
fof(f472_sk,plain,
! [V_Za] :
( ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a)
| ~ hBOOL(hAPP(hAPP(v_P,V_Za),v_s1))
| hBOOL(hAPP(hAPP(v_P,V_Za),v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ),
inference(skolemisation,[status(esa)],[f472_nnf]) ).
cnf(c472,plain,
( ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a)
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s1))
| hBOOL(hAPP(hAPP(v_P,X0),v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ),
inference(cnf_transformation,[status(esa)],[f472_sk]) ).
cnf(p522,plain,
( ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a)
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s1))
| hBOOL(hAPP(hAPP(v_P,X0),v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_ba,v_c) ),
inference(superposition,[status(thm)],[c461,c472]) ).
cnf(p525,plain,
( ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a)
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s1))
| hBOOL(hAPP(hAPP(v_P,X0),v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_ba,v_ca) ),
inference(superposition,[status(thm)],[c462,p522]) ).
cnf(p526,plain,
( ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a)
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s1))
| hBOOL(hAPP(hAPP(v_P,X0),v_s2)) ),
inference(equality_resolution,[status(thm)],[p525]) ).
cnf(p556,plain,
( ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a)
| hBOOL(hAPP(hAPP(v_P,v_xb),v_s2))
| c_Hoare__Mirabelle_Otriple__valid(v_na,v_n(v_na),t_a) ),
inference(resolution,[status(thm)],[p554,p526]) ).
cnf(p570,plain,
( hBOOL(hAPP(hAPP(v_P,v_xb),v_s2))
| c_Hoare__Mirabelle_Otriple__valid(v_na,v_n(v_na),t_a)
| hBOOL(hAPP(v_b,v_s2)) ),
inference(resolution,[status(thm)],[p569,p556]) ).
cnf(p571,plain,
( hBOOL(hAPP(v_b,v_s2))
| c_Hoare__Mirabelle_Otriple__valid(v_na,v_n(v_na),t_a)
| hBOOL(hAPP(v_b,v_s2)) ),
inference(resolution,[status(thm)],[p570,c465]) ).
cnf(p572,plain,
( c_Hoare__Mirabelle_Otriple__valid(v_na,v_n(v_na),t_a)
| hBOOL(hAPP(v_b,v_s2)) ),
inference(factoring,[status(thm)],[p571]) ).
cnf(p573,plain,
( hBOOL(hAPP(hAPP(v_P,v_xb),v_s1))
| hBOOL(hAPP(v_b,v_s2)) ),
inference(resolution,[status(thm)],[p572,p543]) ).
cnf(p574,plain,
( ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a)
| hBOOL(hAPP(hAPP(v_P,v_xb),v_s2))
| hBOOL(hAPP(v_b,v_s2)) ),
inference(resolution,[status(thm)],[p573,p526]) ).
cnf(p578,plain,
( hBOOL(hAPP(v_b,v_s2))
| hBOOL(hAPP(hAPP(v_P,v_xb),v_s2))
| hBOOL(hAPP(v_b,v_s2)) ),
inference(resolution,[status(thm)],[p574,p569]) ).
cnf(p579,plain,
( hBOOL(hAPP(hAPP(v_P,v_xb),v_s2))
| hBOOL(hAPP(v_b,v_s2)) ),
inference(factoring,[status(thm)],[p578]) ).
cnf(p580,plain,
( hBOOL(hAPP(v_b,v_s2))
| hBOOL(hAPP(v_b,v_s2)) ),
inference(resolution,[status(thm)],[p579,c465]) ).
cnf(p581,plain,
hBOOL(hAPP(v_b,v_s2)),
inference(factoring,[status(thm)],[p580]) ).
cnf(f471,negated_conjecture,
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,V_Z),v_s1))
| ~ hBOOL(hAPP(v_b,v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_13) ).
fof(f471_nnf,plain,
! [V_Z] :
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,V_Z),v_s1))
| ~ hBOOL(hAPP(v_b,v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ),
inference(nnf_transformation,[status(thm)],[f471]) ).
fof(f471_sk,plain,
! [V_Z] :
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,V_Z),v_s1))
| ~ hBOOL(hAPP(v_b,v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ),
inference(skolemisation,[status(esa)],[f471_nnf]) ).
cnf(c471,plain,
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s1))
| ~ hBOOL(hAPP(v_b,v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ),
inference(cnf_transformation,[status(esa)],[f471_sk]) ).
cnf(p529,plain,
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s1))
| ~ hBOOL(hAPP(v_b,v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_ba,v_c) ),
inference(superposition,[status(thm)],[c461,c471]) ).
cnf(p532,plain,
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s1))
| ~ hBOOL(hAPP(v_b,v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_ba,v_ca) ),
inference(superposition,[status(thm)],[c462,p529]) ).
cnf(p533,plain,
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s1))
| ~ hBOOL(hAPP(v_b,v_s2)) ),
inference(equality_resolution,[status(thm)],[p532]) ).
cnf(p584,plain,
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s1)) ),
inference(resolution,[status(thm)],[p581,p533]) ).
cnf(p589,plain,
( c_Hoare__Mirabelle_Otriple__valid(v_na,v_n(v_na),t_a)
| hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_G)) ),
inference(resolution,[status(thm)],[p584,p554]) ).
cnf(p590,plain,
( c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a)
| c_Hoare__Mirabelle_Otriple__valid(v_na,v_n(v_na),t_a) ),
inference(resolution,[status(thm)],[p589,c464]) ).
cnf(p592,plain,
( hBOOL(hAPP(hAPP(v_P,v_xb),v_s1))
| c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a) ),
inference(resolution,[status(thm)],[p590,p543]) ).
cnf(p593,plain,
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_G))
| c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a) ),
inference(resolution,[status(thm)],[p592,p584]) ).
cnf(p595,plain,
( c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a)
| c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a) ),
inference(resolution,[status(thm)],[p593,c464]) ).
cnf(p597,plain,
c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a),
inference(factoring,[status(thm)],[p595]) ).
cnf(f473,negated_conjecture,
( ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a)
| ~ hBOOL(hAPP(hAPP(v_P,V_Za),v_s1))
| ~ hBOOL(hAPP(v_b,v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_15) ).
fof(f473_nnf,plain,
! [V_Za] :
( ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a)
| ~ hBOOL(hAPP(hAPP(v_P,V_Za),v_s1))
| ~ hBOOL(hAPP(v_b,v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ),
inference(nnf_transformation,[status(thm)],[f473]) ).
fof(f473_sk,plain,
! [V_Za] :
( ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a)
| ~ hBOOL(hAPP(hAPP(v_P,V_Za),v_s1))
| ~ hBOOL(hAPP(v_b,v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ),
inference(skolemisation,[status(esa)],[f473_nnf]) ).
cnf(c473,plain,
( ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a)
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s1))
| ~ hBOOL(hAPP(v_b,v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ),
inference(cnf_transformation,[status(esa)],[f473_sk]) ).
cnf(p513,plain,
( ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a)
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s1))
| ~ hBOOL(hAPP(v_b,v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_ba,v_c) ),
inference(superposition,[status(thm)],[c461,c473]) ).
cnf(p516,plain,
( ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a)
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s1))
| ~ hBOOL(hAPP(v_b,v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_ba,v_ca) ),
inference(superposition,[status(thm)],[c462,p513]) ).
cnf(p517,plain,
( ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a)
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s1))
| ~ hBOOL(hAPP(v_b,v_s2)) ),
inference(equality_resolution,[status(thm)],[p516]) ).
cnf(p583,plain,
( ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a)
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s1)) ),
inference(resolution,[status(thm)],[p581,p517]) ).
cnf(p585,plain,
( c_Hoare__Mirabelle_Otriple__valid(v_na,v_n(v_na),t_a)
| ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a) ),
inference(resolution,[status(thm)],[p583,p554]) ).
cnf(p598,plain,
c_Hoare__Mirabelle_Otriple__valid(v_na,v_n(v_na),t_a),
inference(resolution,[status(thm)],[p597,p585]) ).
cnf(p599,plain,
hBOOL(hAPP(hAPP(v_P,v_xb),v_s1)),
inference(resolution,[status(thm)],[p598,p543]) ).
cnf(p600,plain,
~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a),
inference(resolution,[status(thm)],[p599,p583]) ).
cnf(p602,plain,
$false,
inference(resolution,[status(thm)],[p600,p597]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV849-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.13/0.38 % Computer : n018.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Thu Sep 24 21:12:04 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 30.87/4.49 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 30.87/4.49 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------