%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : CSR034+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n026.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 01:10:01 PM UTC 2026
% Result : Theorem 14.73s 8.08s
% Output : CNFRefutation 14.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 18
% Syntax : Number of formulae : 96 ( 48 unt; 0 def)
% Number of atoms : 178 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 162 ( 80 ~; 75 |; 2 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 6 ( 5 usr; 2 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 17 con; 0-1 aty)
% Number of variables : 36 ( 0 sgn 34 !; 2 ?; 21 :)
% Comments :
%------------------------------------------------------------------------------
fof(f53,axiom,
genlmt(c_ethnicgroupsmt,c_ethnicgroupsvocabularymt),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_53) ).
fof(f66,axiom,
genlmt(c_nooescapearchitecturemt,c_organizationdatamt),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_66) ).
fof(f137,axiom,
genlmt(c_worldgeographydualistmt,c_worldgeographymt),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_137) ).
fof(f147,axiom,
genlmt(c_tptp_member3515_mt,c_tptp_spindleheadmt),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_147) ).
fof(f232,axiom,
genlmt(f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman),c_massmediadatamt),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_232) ).
fof(f254,axiom,
genlmt(c_tptp_spindleheadmt,c_cyclistsmt),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_254) ).
fof(f257,axiom,
genlmt(c_keinteractionresourcetestmt,c_testvocabularymt),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_257) ).
fof(f275,axiom,
genlmt(c_testvocabularymt,c_nooescapearchitecturemt),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_275) ).
fof(f310,axiom,
genlmt(c_cyclistsmt,c_keinteractionresourcetestmt),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_310) ).
fof(f321,axiom,
( mtvisible(c_worldgeographymt)
=> state_geopolitical(c_wanica_districtsuriname) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_321) ).
fof(f329,axiom,
genlmt(c_massmediadatamt,c_ethnicgroupsmt),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_329) ).
fof(f339,axiom,
genlmt(c_worldcompletedualistgeographymt,c_unitedstatesgeographydualistmt),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_339) ).
fof(f367,axiom,
genlmt(c_ethnicgroupsvocabularymt,c_worldcompletedualistgeographymt),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_367) ).
fof(f454,axiom,
genlmt(c_unitedstatesgeographydualistmt,c_worldgeographydualistmt),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_454) ).
fof(f486,axiom,
genlmt(c_organizationdatamt,f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman)),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_486) ).
fof(f629,axiom,
! [X0] :
( state_geopolitical(X0)
=> isa(X0,c_state_geopolitical) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_629) ).
fof(f1123,axiom,
! [X0,X1] :
( ( genlmt(X0,X1)
& mtvisible(X0) )
=> mtvisible(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_1123) ).
fof(f1132,conjecture,
? [X0] :
( mtvisible(c_tptp_member3515_mt)
=> isa(c_wanica_districtsuriname,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',query84) ).
fof(f1133,negated_conjecture,
~ ? [X0] :
( mtvisible(c_tptp_member3515_mt)
=> isa(c_wanica_districtsuriname,X0) ),
inference(negated_conjecture,[status(cth)],[f1132]) ).
fof(f1381,plain,
( ~ mtvisible(c_worldgeographymt)
| state_geopolitical(c_wanica_districtsuriname) ),
inference(ennf_transformation,[],[f321]) ).
fof(f1581,plain,
! [X0] :
( ~ state_geopolitical(X0)
| isa(X0,c_state_geopolitical) ),
inference(ennf_transformation,[],[f629]) ).
fof(f2012,plain,
! [X0,X1] :
( ~ genlmt(X0,X1)
| ~ mtvisible(X0)
| mtvisible(X1) ),
inference(ennf_transformation,[],[f1123]) ).
fof(f2013,plain,
! [X0,X1] :
( ~ genlmt(X0,X1)
| ~ mtvisible(X0)
| mtvisible(X1) ),
inference(flattening,[],[f2012]) ).
fof(f2022,plain,
! [X0] :
( mtvisible(c_tptp_member3515_mt)
& ~ isa(c_wanica_districtsuriname,X0) ),
inference(ennf_transformation,[],[f1133]) ).
fof(f2075,plain,
genlmt(c_ethnicgroupsmt,c_ethnicgroupsvocabularymt),
inference(cnf_transformation,[],[f53]) ).
fof(f2087,plain,
genlmt(c_nooescapearchitecturemt,c_organizationdatamt),
inference(cnf_transformation,[],[f66]) ).
fof(f2158,plain,
genlmt(c_worldgeographydualistmt,c_worldgeographymt),
inference(cnf_transformation,[],[f137]) ).
fof(f2168,plain,
genlmt(c_tptp_member3515_mt,c_tptp_spindleheadmt),
inference(cnf_transformation,[],[f147]) ).
fof(f2253,plain,
genlmt(f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman),c_massmediadatamt),
inference(cnf_transformation,[],[f232]) ).
fof(f2275,plain,
genlmt(c_tptp_spindleheadmt,c_cyclistsmt),
inference(cnf_transformation,[],[f254]) ).
fof(f2278,plain,
genlmt(c_keinteractionresourcetestmt,c_testvocabularymt),
inference(cnf_transformation,[],[f257]) ).
fof(f2296,plain,
genlmt(c_testvocabularymt,c_nooescapearchitecturemt),
inference(cnf_transformation,[],[f275]) ).
fof(f2330,plain,
genlmt(c_cyclistsmt,c_keinteractionresourcetestmt),
inference(cnf_transformation,[],[f310]) ).
fof(f2341,plain,
( ~ mtvisible(c_worldgeographymt)
| state_geopolitical(c_wanica_districtsuriname) ),
inference(cnf_transformation,[],[f1381]) ).
fof(f2349,plain,
genlmt(c_massmediadatamt,c_ethnicgroupsmt),
inference(cnf_transformation,[],[f329]) ).
fof(f2359,plain,
genlmt(c_worldcompletedualistgeographymt,c_unitedstatesgeographydualistmt),
inference(cnf_transformation,[],[f339]) ).
fof(f2387,plain,
genlmt(c_ethnicgroupsvocabularymt,c_worldcompletedualistgeographymt),
inference(cnf_transformation,[],[f367]) ).
fof(f2474,plain,
genlmt(c_unitedstatesgeographydualistmt,c_worldgeographydualistmt),
inference(cnf_transformation,[],[f454]) ).
fof(f2506,plain,
genlmt(c_organizationdatamt,f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman)),
inference(cnf_transformation,[],[f486]) ).
fof(f2636,plain,
! [X0] :
( ~ state_geopolitical(X0)
| isa(X0,c_state_geopolitical) ),
inference(cnf_transformation,[],[f1581]) ).
fof(f3053,plain,
! [X0,X1] :
( ~ genlmt(X0,X1)
| ~ mtvisible(X0)
| mtvisible(X1) ),
inference(cnf_transformation,[],[f2013]) ).
fof(f3062,plain,
mtvisible(c_tptp_member3515_mt),
inference(cnf_transformation,[],[f2022]) ).
fof(f3063,plain,
! [X0] : ~ isa(c_wanica_districtsuriname,X0),
inference(cnf_transformation,[],[f2022]) ).
tcf(c_101,plain,
genlmt(c_ethnicgroupsmt,c_ethnicgroupsvocabularymt),
inference(cnf_transformation,[],[f2075]) ).
tcf(c_113,plain,
genlmt(c_nooescapearchitecturemt,c_organizationdatamt),
inference(cnf_transformation,[],[f2087]) ).
tcf(c_184,plain,
genlmt(c_worldgeographydualistmt,c_worldgeographymt),
inference(cnf_transformation,[],[f2158]) ).
tcf(c_194,plain,
genlmt(c_tptp_member3515_mt,c_tptp_spindleheadmt),
inference(cnf_transformation,[],[f2168]) ).
tcf(c_279,plain,
genlmt(f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman),c_massmediadatamt),
inference(cnf_transformation,[],[f2253]) ).
tcf(c_301,plain,
genlmt(c_tptp_spindleheadmt,c_cyclistsmt),
inference(cnf_transformation,[],[f2275]) ).
tcf(c_304,plain,
genlmt(c_keinteractionresourcetestmt,c_testvocabularymt),
inference(cnf_transformation,[],[f2278]) ).
tcf(c_322,plain,
genlmt(c_testvocabularymt,c_nooescapearchitecturemt),
inference(cnf_transformation,[],[f2296]) ).
tcf(c_356,plain,
genlmt(c_cyclistsmt,c_keinteractionresourcetestmt),
inference(cnf_transformation,[],[f2330]) ).
tcf(c_367,plain,
( state_geopolitical(c_wanica_districtsuriname)
| ~ mtvisible(c_worldgeographymt) ),
inference(cnf_transformation,[],[f2341]) ).
tcf(c_375,plain,
genlmt(c_massmediadatamt,c_ethnicgroupsmt),
inference(cnf_transformation,[],[f2349]) ).
tcf(c_385,plain,
genlmt(c_worldcompletedualistgeographymt,c_unitedstatesgeographydualistmt),
inference(cnf_transformation,[],[f2359]) ).
tcf(c_413,plain,
genlmt(c_ethnicgroupsvocabularymt,c_worldcompletedualistgeographymt),
inference(cnf_transformation,[],[f2387]) ).
tcf(c_500,plain,
genlmt(c_unitedstatesgeographydualistmt,c_worldgeographydualistmt),
inference(cnf_transformation,[],[f2474]) ).
tcf(c_532,plain,
genlmt(c_organizationdatamt,f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman)),
inference(cnf_transformation,[],[f2506]) ).
tcf(c_662,plain,
! [X0: $i] :
( isa(X0,c_state_geopolitical)
| ~ state_geopolitical(X0) ),
inference(cnf_transformation,[],[f2636]) ).
tcf(c_1079,plain,
! [X0: $i,X1: $i] :
( mtvisible(X1)
| ~ mtvisible(X0)
| ~ genlmt(X0,X1) ),
inference(cnf_transformation,[],[f3053]) ).
tcf(c_1088,negated_conjecture,
! [X0: $i] : ~ isa(c_wanica_districtsuriname,X0),
inference(cnf_transformation,[],[f3063]) ).
tcf(c_1089,negated_conjecture,
mtvisible(c_tptp_member3515_mt),
inference(cnf_transformation,[],[f3062]) ).
tcf(c_1944,plain,
! [X0: $i] :
( isa(X0,c_state_geopolitical)
| ~ state_geopolitical(X0) ),
inference(prop_impl_just,[status(thm)],[c_662]) ).
tcf(c_2846,plain,
( state_geopolitical(c_wanica_districtsuriname)
| ~ mtvisible(c_worldgeographymt) ),
inference(prop_impl_just,[status(thm)],[c_367]) ).
tcf(c_11546,plain,
( isa(c_wanica_districtsuriname,c_state_geopolitical)
| ~ mtvisible(c_worldgeographymt) ),
inference(resolution,[status(thm)],[c_1944,c_2846]) ).
tcf(c_11551,plain,
~ mtvisible(c_worldgeographymt),
inference(forward_subsumption_resolution,[status(thm)],[c_11546,c_1088]) ).
tcf(c_18569,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1,X1_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( mtvisible(X1_iProver_partiallytangible_1)
| ~ mtvisible(X0_iProver_partiallytangible_1)
| ~ genlmt(X0_iProver_partiallytangible_1,X1_iProver_partiallytangible_1) ),
inference(subtyping,[status(esa)],[c_1079]) ).
tcf(c_19048,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( mtvisible(c_worldgeographymt)
| ~ mtvisible(X0_iProver_partiallytangible_1)
| ~ genlmt(X0_iProver_partiallytangible_1,c_worldgeographymt) ),
inference(instantiation,[status(thm)],[c_18569]) ).
tcf(c_19188,plain,
( mtvisible(c_worldgeographymt)
| ~ mtvisible(c_worldgeographydualistmt)
| ~ genlmt(c_worldgeographydualistmt,c_worldgeographymt) ),
inference(instantiation,[status(thm)],[c_19048]) ).
tcf(c_19469,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( mtvisible(c_worldgeographydualistmt)
| ~ mtvisible(X0_iProver_partiallytangible_1)
| ~ genlmt(X0_iProver_partiallytangible_1,c_worldgeographydualistmt) ),
inference(instantiation,[status(thm)],[c_18569]) ).
tcf(c_19931,plain,
( mtvisible(c_worldgeographydualistmt)
| ~ mtvisible(c_unitedstatesgeographydualistmt)
| ~ genlmt(c_unitedstatesgeographydualistmt,c_worldgeographydualistmt) ),
inference(instantiation,[status(thm)],[c_19469]) ).
tcf(c_20050,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( mtvisible(c_tptp_spindleheadmt)
| ~ mtvisible(X0_iProver_partiallytangible_1)
| ~ genlmt(X0_iProver_partiallytangible_1,c_tptp_spindleheadmt) ),
inference(instantiation,[status(thm)],[c_18569]) ).
tcf(c_20230,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( mtvisible(c_unitedstatesgeographydualistmt)
| ~ mtvisible(X0_iProver_partiallytangible_1)
| ~ genlmt(X0_iProver_partiallytangible_1,c_unitedstatesgeographydualistmt) ),
inference(instantiation,[status(thm)],[c_18569]) ).
tcf(c_20232,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( mtvisible(c_cyclistsmt)
| ~ mtvisible(X0_iProver_partiallytangible_1)
| ~ genlmt(X0_iProver_partiallytangible_1,c_cyclistsmt) ),
inference(instantiation,[status(thm)],[c_18569]) ).
tcf(c_20233,plain,
( mtvisible(c_cyclistsmt)
| ~ mtvisible(c_tptp_spindleheadmt)
| ~ genlmt(c_tptp_spindleheadmt,c_cyclistsmt) ),
inference(instantiation,[status(thm)],[c_20232]) ).
tcf(c_20287,plain,
( mtvisible(c_tptp_spindleheadmt)
| ~ mtvisible(c_tptp_member3515_mt)
| ~ genlmt(c_tptp_member3515_mt,c_tptp_spindleheadmt) ),
inference(instantiation,[status(thm)],[c_20050]) ).
tcf(c_20510,plain,
( mtvisible(c_unitedstatesgeographydualistmt)
| ~ mtvisible(c_worldcompletedualistgeographymt)
| ~ genlmt(c_worldcompletedualistgeographymt,c_unitedstatesgeographydualistmt) ),
inference(instantiation,[status(thm)],[c_20230]) ).
tcf(c_20581,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( mtvisible(c_worldcompletedualistgeographymt)
| ~ mtvisible(X0_iProver_partiallytangible_1)
| ~ genlmt(X0_iProver_partiallytangible_1,c_worldcompletedualistgeographymt) ),
inference(instantiation,[status(thm)],[c_18569]) ).
tcf(c_20653,plain,
( mtvisible(c_worldcompletedualistgeographymt)
| ~ mtvisible(c_ethnicgroupsvocabularymt)
| ~ genlmt(c_ethnicgroupsvocabularymt,c_worldcompletedualistgeographymt) ),
inference(instantiation,[status(thm)],[c_20581]) ).
tcf(c_20713,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( mtvisible(c_ethnicgroupsvocabularymt)
| ~ mtvisible(X0_iProver_partiallytangible_1)
| ~ genlmt(X0_iProver_partiallytangible_1,c_ethnicgroupsvocabularymt) ),
inference(instantiation,[status(thm)],[c_18569]) ).
tcf(c_20734,plain,
( mtvisible(c_ethnicgroupsvocabularymt)
| ~ mtvisible(c_ethnicgroupsmt)
| ~ genlmt(c_ethnicgroupsmt,c_ethnicgroupsvocabularymt) ),
inference(instantiation,[status(thm)],[c_20713]) ).
tcf(c_20758,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( mtvisible(c_ethnicgroupsmt)
| ~ mtvisible(X0_iProver_partiallytangible_1)
| ~ genlmt(X0_iProver_partiallytangible_1,c_ethnicgroupsmt) ),
inference(instantiation,[status(thm)],[c_18569]) ).
tcf(c_20799,plain,
( mtvisible(c_ethnicgroupsmt)
| ~ mtvisible(c_massmediadatamt)
| ~ genlmt(c_massmediadatamt,c_ethnicgroupsmt) ),
inference(instantiation,[status(thm)],[c_20758]) ).
tcf(c_20820,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( mtvisible(c_massmediadatamt)
| ~ mtvisible(X0_iProver_partiallytangible_1)
| ~ genlmt(X0_iProver_partiallytangible_1,c_massmediadatamt) ),
inference(instantiation,[status(thm)],[c_18569]) ).
tcf(c_20873,plain,
( mtvisible(c_massmediadatamt)
| ~ mtvisible(f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman))
| ~ genlmt(f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman),c_massmediadatamt) ),
inference(instantiation,[status(thm)],[c_20820]) ).
tcf(c_20911,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( mtvisible(f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman))
| ~ mtvisible(X0_iProver_partiallytangible_1)
| ~ genlmt(X0_iProver_partiallytangible_1,f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman)) ),
inference(instantiation,[status(thm)],[c_18569]) ).
tcf(c_20989,plain,
( mtvisible(f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman))
| ~ mtvisible(c_organizationdatamt)
| ~ genlmt(c_organizationdatamt,f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman)) ),
inference(instantiation,[status(thm)],[c_20911]) ).
tcf(c_21039,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( mtvisible(c_organizationdatamt)
| ~ mtvisible(X0_iProver_partiallytangible_1)
| ~ genlmt(X0_iProver_partiallytangible_1,c_organizationdatamt) ),
inference(instantiation,[status(thm)],[c_18569]) ).
tcf(c_21153,plain,
( mtvisible(c_organizationdatamt)
| ~ mtvisible(c_nooescapearchitecturemt)
| ~ genlmt(c_nooescapearchitecturemt,c_organizationdatamt) ),
inference(instantiation,[status(thm)],[c_21039]) ).
tcf(c_21208,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( mtvisible(c_nooescapearchitecturemt)
| ~ mtvisible(X0_iProver_partiallytangible_1)
| ~ genlmt(X0_iProver_partiallytangible_1,c_nooescapearchitecturemt) ),
inference(instantiation,[status(thm)],[c_18569]) ).
tcf(c_21371,plain,
( mtvisible(c_nooescapearchitecturemt)
| ~ mtvisible(c_testvocabularymt)
| ~ genlmt(c_testvocabularymt,c_nooescapearchitecturemt) ),
inference(instantiation,[status(thm)],[c_21208]) ).
tcf(c_21423,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( mtvisible(c_testvocabularymt)
| ~ mtvisible(X0_iProver_partiallytangible_1)
| ~ genlmt(X0_iProver_partiallytangible_1,c_testvocabularymt) ),
inference(instantiation,[status(thm)],[c_18569]) ).
tcf(c_21636,plain,
( mtvisible(c_testvocabularymt)
| ~ mtvisible(c_keinteractionresourcetestmt)
| ~ genlmt(c_keinteractionresourcetestmt,c_testvocabularymt) ),
inference(instantiation,[status(thm)],[c_21423]) ).
tcf(c_21694,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( mtvisible(c_keinteractionresourcetestmt)
| ~ mtvisible(X0_iProver_partiallytangible_1)
| ~ genlmt(X0_iProver_partiallytangible_1,c_keinteractionresourcetestmt) ),
inference(instantiation,[status(thm)],[c_18569]) ).
tcf(c_21936,plain,
( mtvisible(c_keinteractionresourcetestmt)
| ~ mtvisible(c_cyclistsmt)
| ~ genlmt(c_cyclistsmt,c_keinteractionresourcetestmt) ),
inference(instantiation,[status(thm)],[c_21694]) ).
tcf(c_21937,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_21936,c_21636,c_21371,c_21153,c_20989,c_20873,c_20799,c_20734,c_20653,c_20510,c_20287,c_20233,c_19931,c_19188,c_11551,c_279,c_532,c_101,c_113,c_184,c_194,c_301,c_304,c_322,c_356,c_375,c_385,c_413,c_500,c_1089]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR034+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/5.59 % Computer : n026.cluster.edu
% 0.13/5.59 % Model : x86_64 x86_64
% 0.13/5.59 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/5.59 % Memory : 8046.5625MB
% 0.13/5.59 % OS : Linux 6.8.0-71-generic
% 0.13/5.59 % CPULimit : 300
% 0.13/5.59 % WCLimit : 300
% 0.13/5.59 % DateTime : Fri Sep 25 08:21:16 UTC 2026
% 0.17/5.60 % CPUTime :
% 0.17/5.60 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.17/5.64 Running first-order theorem proving
% 0.17/5.64 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.17/5.65
% 0.17/5.65 % ======== iProver multi-core TPTP/SMT =========
% 0.17/5.65
% 0.17/5.65 % Detected problem language: tptp
% 0.17/5.66 % Proving...
% 14.73/8.08 % SZS status Started for theBenchmark.p
% 14.73/8.08 % SZS status Theorem for theBenchmark.p
% 14.73/8.08
% 14.73/8.08 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 14.73/8.08
% 14.73/8.08 % ------ iProver source info
% 14.73/8.08
% 14.73/8.08 % git: date: 2026-07-19 20:42:38 +0200
% 14.73/8.08 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 14.73/8.08 % git: non_committed_changes: false
% 14.73/8.08
% 14.73/8.08 % ------ Parsing...
% 14.73/8.08 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 14.73/8.08
% 14.73/8.08 % ------ Preprocessing... sf_s rm: 30 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe:16:0s pe:32:0s pe:64:0s pe:128:0s pe_e %
% 14.73/8.08
% 14.73/8.08 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 14.73/8.08 % ------ Proving...
% 14.73/8.08 % ------ Problem Properties
% 14.73/8.08
% 14.73/8.08 %
% 14.73/8.08 % clauses 764
% 14.73/8.08 % conjectures 2
% 14.73/8.08 % EPR 716
% 14.73/8.08 % Horn 764
% 14.73/8.08 % unary 274
% 14.73/8.08 % binary 455
% 14.73/8.08 % lits 1289
% 14.73/8.08 % lits eq 0
% 14.73/8.08 % fd_pure 0
% 14.73/8.08 % fd_pseudo 0
% 14.73/8.08 % fd_cond 0
% 14.73/8.08 % fd_pseudo_cond 0
% 14.73/8.08 % AC symbols 0
% 14.73/8.08
% 14.73/8.08 % ------ Input Options Time Limit: Unbounded
% 14.73/8.08
% 14.73/8.08
% 14.73/8.08 % ------
% 14.73/8.08 % Current options:
% 14.73/8.08 % ------
% 14.73/8.08
% 14.73/8.08
% 14.73/8.08 %
% 14.73/8.08
% 14.73/8.08 % ------ Proving...
% 14.73/8.08 %
% 14.73/8.08
% 14.73/8.08 % SZS status Theorem for theBenchmark.p
% 14.73/8.08
% 14.73/8.08 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 14.73/8.08
% 14.73/8.08
%------------------------------------------------------------------------------