%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWV822-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 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:24:17 PM UTC 2026
% Result : Unsatisfiable 104.43s 17.97s
% Output : CNFRefutation 104.43s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f850ERROR: Could not build tree for root c_159597ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f107,axiom,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(X0,c_Suc(X1),tc_nat)
| c_lessequals(X0,X1,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_less__Suc__eq__le_0) ).
fof(f742,axiom,
! [X2,X3,X0,X1,X4] :
( ~ c_Natural_Oevaln(X0,X1,X4,X3)
| ~ c_lessequals(X4,X2,tc_nat)
| c_Natural_Oevaln(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_evaln__nonstrict_0) ).
fof(f754,axiom,
! [X0] : c_HOL_Oord__class_Oless(X0,c_Suc(X0),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_lessI_0) ).
fof(f768,axiom,
! [X2,X3,X0,X1] :
( ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(X0),X1,X2,X3)
| c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(X0),tc_Com_Ocom),X1,c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(X0,X2,X1,X3),X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_evaln__elim__cases_I6_J_1) ).
fof(f790,axiom,
! [X2,X3,X0,X1] :
( ~ c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(X0),tc_Com_Ocom),X1,X2,X3)
| c_Natural_Oevaln(c_Com_Ocom_OBODY(X0),X1,c_Suc(X2),X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_evaln_OBody_0) ).
fof(f798,axiom,
! [X2,X3,X0,X1] :
( ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(X1),X2,X0,X3)
| X0 = c_Suc(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(X1,X0,X2,X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_evaln__elim__cases_I6_J_0) ).
fof(f799,plain,
! [X2,X3,X0,X1] :
( ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(X1),X2,X0,X3)
| c_Suc(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(X1,X0,X2,X3)) = X0 ),
inference(reorient_equations,[],[f798]) ).
fof(f803,axiom,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(X1,c_Suc(X0),tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less__eq_1) ).
fof(f804,axiom,
! [X0,X1] :
( c_HOL_Oord__class_Oless(X1,X0,tc_nat)
| c_HOL_Oord__class_Oless(X0,c_Suc(X1),tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less__eq_0) ).
fof(f816,negated_conjecture,
( c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),v_xa,v_n,v_xb)
| c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),v_xa,c_Suc(v_n),v_xb) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f821,negated_conjecture,
! [X2,X3,X0,X1,X4,X5] :
( ~ hBOOL(hAPP(hAPP(v_P,X3),X5))
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X5,c_Suc(v_n),X4)
| hBOOL(hAPP(hAPP(v_Q,X3),X4))
| ~ hBOOL(hAPP(hAPP(v_P,X0),X2))
| ~ c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),X2,v_n,X1)
| hBOOL(hAPP(hAPP(v_Q,X0),X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_9) ).
tcf(c_850,plain,
! [X0: $i,X1: $i] :
( c_lessequals(X0,X1,tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,c_Suc(X1),tc_nat) ),
inference(cnf_transformation,[],[f107]) ).
tcf(c_1288,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( c_Natural_Oevaln(X0,X1,X4,X3)
| ~ c_lessequals(X2,X4,tc_nat)
| ~ c_Natural_Oevaln(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f742]) ).
tcf(c_1299,plain,
! [X0: $i] : c_HOL_Oord__class_Oless(X0,c_Suc(X0),tc_nat),
inference(cnf_transformation,[],[f754]) ).
tcf(c_1311,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(X0),tc_Com_Ocom),X1,c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(X0,X2,X1,X3),X3)
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(X0),X1,X2,X3) ),
inference(cnf_transformation,[],[f768]) ).
tcf(c_1328,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_Natural_Oevaln(c_Com_Ocom_OBODY(X0),X1,c_Suc(X2),X3)
| ~ c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(X0),tc_Com_Ocom),X1,X2,X3) ),
inference(cnf_transformation,[],[f790]) ).
tcf(c_1334,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( c_Suc(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(X0,X2,X1,X3)) = X2 )
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(X0),X1,X2,X3) ),
inference(cnf_transformation,[],[f799]) ).
tcf(c_1337,plain,
! [X0: $i,X1: $i] :
( ~ c_HOL_Oord__class_Oless(X1,X0,tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,c_Suc(X1),tc_nat) ),
inference(cnf_transformation,[],[f803]) ).
tcf(c_1338,plain,
! [X0: $i,X1: $i] :
( c_HOL_Oord__class_Oless(X1,X0,tc_nat)
| c_HOL_Oord__class_Oless(X0,c_Suc(X1),tc_nat) ),
inference(cnf_transformation,[],[f804]) ).
tcf(c_1346,negated_conjecture,
hBOOL(hAPP(hAPP(v_P,v_x),v_xa)),
inference(cnf_transformation,[],[f850]) ).
tcf(c_1350,negated_conjecture,
( c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),v_xa,c_Suc(v_n),v_xb)
| c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),v_xa,v_n,v_xb) ),
inference(cnf_transformation,[],[f816]) ).
tcf(c_1354,negated_conjecture,
~ hBOOL(hAPP(hAPP(v_Q,v_x),v_xb)),
inference(cnf_transformation,[],[f851]) ).
tcf(c_1355,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( hBOOL(hAPP(hAPP(v_Q,X5),X3))
| hBOOL(hAPP(hAPP(v_Q,X4),X1))
| ~ hBOOL(hAPP(hAPP(v_P,X5),X2))
| ~ hBOOL(hAPP(hAPP(v_P,X4),X0))
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X2,c_Suc(v_n),X3)
| ~ c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),X0,v_n,X1) ),
inference(cnf_transformation,[],[f821]) ).
tcf(c_1658,plain,
! [X0: $i,X1: $i] :
( c_lessequals(X0,X1,tc_nat)
| c_HOL_Oord__class_Oless(X1,X0,tc_nat) ),
inference(prop_impl_just,[status(thm)],[c_1338,c_850]) ).
tcf(c_1659,plain,
! [X0: $i,X1: $i] :
( c_HOL_Oord__class_Oless(X1,X0,tc_nat)
| c_lessequals(X0,X1,tc_nat) ),
inference(renaming,[status(thm)],[c_1658]) ).
tcf(c_2032,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_Natural_Oevaln(c_Com_Ocom_OBODY(X0),X1,c_Suc(X2),X3)
| ~ c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(X0),tc_Com_Ocom),X1,X2,X3) ),
inference(prop_impl_just,[status(thm)],[c_1328]) ).
tcf(c_2172,plain,
( c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),v_xa,v_n,v_xb)
| c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),v_xa,c_Suc(v_n),v_xb) ),
inference(prop_impl_just,[status(thm)],[c_1350]) ).
tcf(c_2173,plain,
( c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),v_xa,c_Suc(v_n),v_xb)
| c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),v_xa,v_n,v_xb) ),
inference(renaming,[status(thm)],[c_2172]) ).
tcf(c_3678,plain,
c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),v_xa,c_Suc(v_n),v_xb),
inference(forward_subsumption_resolution,[status(thm)],[c_2173,c_2032]) ).
tcf(c_17777,plain,
! [X0: $i,X1: $i] :
( c_lessequals(X0,X1,tc_nat)
| c_HOL_Oord__class_Oless(X1,X0,tc_nat) ),
inference(prop_impl_just,[status(thm)],[c_1659]) ).
tcf(c_17778,plain,
! [X0: $i,X1: $i] :
( c_HOL_Oord__class_Oless(X1,X0,tc_nat)
| c_lessequals(X0,X1,tc_nat) ),
inference(renaming,[status(thm)],[c_17777]) ).
tcf(c_20825,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ~ iPr_def_10
| ~ hBOOL(hAPP(hAPP(v_P,X2),X0))
| hBOOL(hAPP(hAPP(v_Q,X2),X1))
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X0,c_Suc(v_n),X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_1355]) ).
tcf(c_20826,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ~ iPr_def_11
| ~ hBOOL(hAPP(hAPP(v_P,X2),X0))
| hBOOL(hAPP(hAPP(v_Q,X2),X1))
| ~ c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),X0,v_n,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_1355]) ).
tcf(c_20827,negated_conjecture,
( iPr_def_11
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1355]) ).
tcf(c_25630,plain,
( c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),v_xa,c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(v_pn,c_Suc(v_n),v_xa,v_xb),v_xb)
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),v_xa,c_Suc(v_n),v_xb) ),
inference(instantiation,[status(thm)],[c_1311]) ).
tcf(c_25867,plain,
! [X0: $i] :
( hBOOL(hAPP(hAPP(v_Q,X0),v_xb))
| ~ iPr_def_10
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_xa)) ),
inference(superposition,[status(thm)],[c_3678,c_20825]) ).
tcf(c_25873,plain,
( hBOOL(hAPP(hAPP(v_Q,v_x),v_xb))
| ~ iPr_def_10 ),
inference(superposition,[status(thm)],[c_1346,c_25867]) ).
tcf(c_25874,plain,
~ iPr_def_10,
inference(forward_subsumption_resolution,[status(thm)],[c_25873,c_1354]) ).
tcf(c_25875,plain,
iPr_def_11,
inference(backward_subsumption_resolution,[status(thm)],[c_20827,c_25874]) ).
tcf(c_52094,plain,
c_Suc(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(v_pn,c_Suc(v_n),v_xa,v_xb)) = c_Suc(v_n),
inference(superposition,[status(thm)],[c_3678,c_1334]) ).
tcf(c_52114,plain,
c_HOL_Oord__class_Oless(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(v_pn,c_Suc(v_n),v_xa,v_xb),c_Suc(v_n),tc_nat),
inference(superposition,[status(thm)],[c_52094,c_1299]) ).
tcf(c_55174,plain,
~ c_HOL_Oord__class_Oless(v_n,c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(v_pn,c_Suc(v_n),v_xa,v_xb),tc_nat),
inference(superposition,[status(thm)],[c_52114,c_1337]) ).
tcf(c_74912,plain,
c_lessequals(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(v_pn,c_Suc(v_n),v_xa,v_xb),v_n,tc_nat),
inference(superposition,[status(thm)],[c_17778,c_55174]) ).
tcf(c_154018,plain,
! [X0: $i] :
( c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),v_xa,X0,v_xb)
| ~ c_lessequals(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(v_pn,c_Suc(v_n),v_xa,v_xb),X0,tc_nat)
| ~ c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),v_xa,c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(v_pn,c_Suc(v_n),v_xa,v_xb),v_xb) ),
inference(instantiation,[status(thm)],[c_1288]) ).
tcf(c_157712,plain,
( c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),v_xa,v_n,v_xb)
| ~ c_lessequals(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(v_pn,c_Suc(v_n),v_xa,v_xb),v_n,tc_nat)
| ~ c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),v_xa,c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(v_pn,c_Suc(v_n),v_xa,v_xb),v_xb) ),
inference(instantiation,[status(thm)],[c_154018]) ).
tcf(c_157713,plain,
! [X0: $i] :
( hBOOL(hAPP(hAPP(v_Q,X0),v_xb))
| ~ iPr_def_11
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_xa))
| ~ c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),v_xa,v_n,v_xb) ),
inference(instantiation,[status(thm)],[c_20826]) ).
tcf(c_159596,plain,
( hBOOL(hAPP(hAPP(v_Q,v_x),v_xb))
| ~ iPr_def_11
| ~ hBOOL(hAPP(hAPP(v_P,v_x),v_xa))
| ~ c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),v_xa,v_n,v_xb) ),
inference(instantiation,[status(thm)],[c_157713]) ).
tcf(c_159597,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_159596,c_157712,c_74912,c_25875,c_25630,c_3678,c_1354,c_1346]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV822-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.38 % Computer : n018.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Thu Sep 24 21:09:34 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.43
% 0.11/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.43
% 0.11/0.43 % Detected problem language: tptp
% 0.11/0.45 % Proving...
% 104.43/17.97 % SZS status Started for theBenchmark.p
% 104.43/17.97 % SZS status Unsatisfiable for theBenchmark.p
% 104.43/17.97
% 104.43/17.97 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 104.43/17.97
% 104.43/17.97 % ------ iProver source info
% 104.43/17.97
% 104.43/17.97 % git: date: 2026-07-19 20:42:38 +0200
% 104.43/17.97 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 104.43/17.97 % git: non_committed_changes: false
% 104.43/17.97
% 104.43/17.97 % ------ Parsing...% successful
% 104.43/17.97
% 104.43/17.97
% 104.43/17.97 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 104.43/17.97
% 104.43/17.97 % ------ Preprocessing... sup_sim: 13 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe:16:0s pe_e sup_sim: 9 sf_s rm: 28 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 28 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 28 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 28 0s sf_e pe_s pe_e %
% 104.43/17.97
% 104.43/17.97 % ------ Preprocessing... gs_s sp: 2 0s gs_e snvd_s sp: 0 0s snvd_e %
% 104.43/17.97
% 104.43/17.97 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 104.43/17.97 % ------ Proving...
% 104.43/17.97 % ------ Problem Properties
% 104.43/17.97
% 104.43/17.97 %
% 104.43/17.97 % clauses 322
% 104.43/17.97 % conjectures 5
% 104.43/17.97 % EPR 17
% 104.43/17.97 % Horn 254
% 104.43/17.97 % unary 119
% 104.43/17.97 % binary 128
% 104.43/17.97 % lits 605
% 104.43/17.97 % lits eq 199
% 104.43/17.97 % fd_pure 0
% 104.43/17.97 % fd_pseudo 0
% 104.43/17.97 % fd_cond 13
% 104.43/17.97 % fd_pseudo_cond 22
% 104.43/17.97 % AC symbols 0
% 104.43/17.97
% 104.43/17.97 % ------ Input Options Time Limit: Unbounded
% 104.43/17.97
% 104.43/17.97
% 104.43/17.97 % ------
% 104.43/17.97 % Current options:
% 104.43/17.97 % ------
% 104.43/17.97
% 104.43/17.97
% 104.43/17.97 %
% 104.43/17.97
% 104.43/17.97 % ------ Proving...
% 104.43/17.97 %
% 104.43/17.97
% 104.43/17.97 % SZS status Unsatisfiable for theBenchmark.p
% 104.43/17.97
% 104.43/17.97 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 104.43/17.97
% 104.43/17.97
%------------------------------------------------------------------------------