%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP216^3 : TPTP v9.3.1. Bugfixed v9.2.1.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n001.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 : Wed Sep 30 08:07:14 AM UTC 2026
% Result : Theorem 47.88s 13.34s
% Output : Refutation 48.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 6
% Syntax : Number of formulae : 28 ( 18 unt; 0 typ; 2 def)
% Number of atoms : 42 ( 26 equ; 0 cnn)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 165 ( 32 ~; 9 |; 0 &; 121 @)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 5 avg)
% Number of types : 306 ( 305 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 13 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 45 ( 4 ^; 35 !; 4 ?; 45 :)
% ( 0 !>; 0 ?*; 0 @-; 2 @+)
% Comments :
%------------------------------------------------------------------------------
thf(set_Pr3444600963470892981et_nat_type,type,
set_Pr3444600963470892981et_nat: $tType ).
thf(produc5657529347773406293et_nat_type,type,
produc5657529347773406293et_nat: $tType ).
thf(set_Pr1722956316086891245nteger_type,type,
set_Pr1722956316086891245nteger: $tType ).
thf(produc824974754969098637nteger_type,type,
produc824974754969098637nteger: $tType ).
thf(set_Pr4708930517165415495nt_int_type,type,
set_Pr4708930517165415495nt_int: $tType ).
thf(produc2432570611225516007nt_int_type,type,
produc2432570611225516007nt_int: $tType ).
thf(set_Pr7928877670098842301et_nat_type,type,
set_Pr7928877670098842301et_nat: $tType ).
thf(produc6830853553727218525et_nat_type,type,
produc6830853553727218525et_nat: $tType ).
thf(set_Pr6418322821503574069e_term_type,type,
set_Pr6418322821503574069e_term: $tType ).
thf(produc8187290932660736981e_term_type,type,
produc8187290932660736981e_term: $tType ).
thf(set_Pr4675205556198584599e_term_type,type,
set_Pr4675205556198584599e_term: $tType ).
thf(set_se5120235452707311462et_nat_type,type,
set_se5120235452707311462et_nat: $tType ).
thf(set_Pr8634505666381077339nt_int_type,type,
set_Pr8634505666381077339nt_int: $tType ).
thf(produc4499399687821757879e_term_type,type,
produc4499399687821757879e_term: $tType ).
thf(set_Pr1230246726286442933_nat_o_type,type,
set_Pr1230246726286442933_nat_o: $tType ).
thf(option2860828798490689354et_nat_type,type,
option2860828798490689354et_nat: $tType ).
thf(set_Pr7705059561495379578_nat_o_type,type,
set_Pr7705059561495379578_nat_o: $tType ).
thf(set_Pr8536935166611901872et_nat_type,type,
set_Pr8536935166611901872et_nat: $tType ).
thf(produc2501202720802129403nt_int_type,type,
produc2501202720802129403nt_int: $tType ).
thf(produc4193628355235574503at_nat_type,type,
produc4193628355235574503at_nat: $tType ).
thf(set_Pr1457143144315775327_nat_o_type,type,
set_Pr1457143144315775327_nat_o: $tType ).
thf(produc4962441903510821572_nat_o_type,type,
produc4962441903510821572_nat_o: $tType ).
thf(produc2732055786443039994et_nat_type,type,
produc2732055786443039994et_nat: $tType ).
thf(set_Pr7459493094073627847at_nat_type,type,
set_Pr7459493094073627847at_nat: $tType ).
thf(produc1319942482725812455at_nat_type,type,
produc1319942482725812455at_nat: $tType ).
thf(set_Pr5564308138774400199at_nat_type,type,
set_Pr5564308138774400199at_nat: $tType ).
thf(set_se124295367203800706nteger_type,type,
set_se124295367203800706nteger: $tType ).
thf(set_Pr606876518868980121eger_o_type,type,
set_Pr606876518868980121eger_o: $tType ).
thf(produc1906917888121415911at_nat_type,type,
produc1906917888121415911at_nat: $tType ).
thf(option8051342751916580710nteger_type,type,
option8051342751916580710nteger: $tType ).
thf(set_Pr1628540301243981434e_term_type,type,
set_Pr1628540301243981434e_term: $tType ).
thf(set_Pr1281608226676607948nteger_type,type,
set_Pr1281608226676607948nteger: $tType ).
thf(set_Pr8914822823351560561eger_o_type,type,
set_Pr8914822823351560561eger_o: $tType ).
thf(produc998928222018024388e_term_type,type,
produc998928222018024388e_term: $tType ).
thf(produc989692990947075319atural_type,type,
produc989692990947075319atural: $tType ).
thf(produc1908205239877642774nteger_type,type,
produc1908205239877642774nteger: $tType ).
thf(set_se2364587433798273647nt_int_type,type,
set_se2364587433798273647nt_int: $tType ).
thf(set_Pr6358892174463501804_int_o_type,type,
set_Pr6358892174463501804_int_o: $tType ).
thf(option7541221861074943443nt_int_type,type,
option7541221861074943443nt_int: $tType ).
thf(set_Pr7309386651551657097e_term_type,type,
set_Pr7309386651551657097e_term: $tType ).
thf(set_Pr9222295170931077689nt_int_type,type,
set_Pr9222295170931077689nt_int: $tType ).
thf(set_Pr5050529186185961540_int_o_type,type,
set_Pr5050529186185961540_int_o: $tType ).
thf(set_se8543413830569400298et_nat_type,type,
set_se8543413830569400298et_nat: $tType ).
thf(set_Pr2161125870931222855_nat_o_type,type,
set_Pr2161125870931222855_nat_o: $tType ).
thf(set_Pr8959645425803247153_nat_o_type,type,
set_Pr8959645425803247153_nat_o: $tType ).
thf(produc1821397396195235155e_term_type,type,
produc1821397396195235155e_term: $tType ).
thf(produc2285326912895808259nt_int_type,type,
produc2285326912895808259nt_int: $tType ).
thf(option5190343406534369742et_nat_type,type,
option5190343406534369742et_nat: $tType ).
thf(set_Pr7140365069852192003e_term_type,type,
set_Pr7140365069852192003e_term: $tType ).
thf(produc3295550550304853304nteger_type,type,
produc3295550550304853304nteger: $tType ).
thf(set_Pr4208978187861016310_nat_o_type,type,
set_Pr4208978187861016310_nat_o: $tType ).
thf(set_Pr3286484037609594932et_nat_type,type,
set_Pr3286484037609594932et_nat: $tType ).
thf(produc4928098042776334183_nat_o_type,type,
produc4928098042776334183_nat_o: $tType ).
thf(set_Pr8208987589773510107_nat_o_type,type,
set_Pr8208987589773510107_nat_o: $tType ).
thf(set_Pr719794911490849221et_nat_type,type,
set_Pr719794911490849221et_nat: $tType ).
thf(produc1945540942535730339e_term_type,type,
produc1945540942535730339e_term: $tType ).
thf(produc4130039061994950697nteger_type,type,
produc4130039061994950697nteger: $tType ).
thf(produc7172142986261921671rm_int_type,type,
produc7172142986261921671rm_int: $tType ).
thf(produc6907119039986491712_nat_o_type,type,
produc6907119039986491712_nat_o: $tType ).
thf(produc3925858234332021118et_nat_type,type,
produc3925858234332021118et_nat: $tType ).
thf(set_Pr5070339090747523585at_nat_type,type,
set_Pr5070339090747523585at_nat: $tType ).
thf(set_Pr2072254264782222413at_nat_type,type,
set_Pr2072254264782222413at_nat: $tType ).
thf(produc8111630337999740517et_nat_type,type,
produc8111630337999740517et_nat: $tType ).
thf(produc5577056076408194680rm_int_type,type,
produc5577056076408194680rm_int: $tType ).
thf(produc2087150632810049441at_nat_type,type,
produc2087150632810049441at_nat: $tType ).
thf(produc2714363965264676845at_nat_type,type,
produc2714363965264676845at_nat: $tType ).
thf(produc8731074985263844745atural_type,type,
produc8731074985263844745atural: $tType ).
thf(produc8763457246119570046nteger_type,type,
produc8763457246119570046nteger: $tType ).
thf(set_Pr7604974323444597168e_term_type,type,
set_Pr7604974323444597168e_term: $tType ).
thf(produc5966032636589952099nteger_type,type,
produc5966032636589952099nteger: $tType ).
thf(set_se7394616247590735609nt_int_type,type,
set_se7394616247590735609nt_int: $tType ).
thf(produc5219672859094816389atural_type,type,
produc5219672859094816389atural: $tType ).
thf(set_Pr1425283071195816930_int_o_type,type,
set_Pr1425283071195816930_int_o: $tType ).
thf(produc6576344331059438605e_term_type,type,
produc6576344331059438605e_term: $tType ).
thf(set_Pr3642885161833720865e_term_type,type,
set_Pr3642885161833720865e_term: $tType ).
thf(set_Pr552903133987017116at_nat_type,type,
set_Pr552903133987017116at_nat: $tType ).
thf(set_Pr1625285437083415874at_nat_type,type,
set_Pr1625285437083415874at_nat: $tType ).
thf(option4256020574406277085nt_int_type,type,
option4256020574406277085nt_int: $tType ).
thf(set_Pr9020418513037773311e_term_type,type,
set_Pr9020418513037773311e_term: $tType ).
thf(set_Pr1872883991513573699nt_int_type,type,
set_Pr1872883991513573699nt_int: $tType ).
thf(set_Pr1604112560894399303at_nat_type,type,
set_Pr1604112560894399303at_nat: $tType ).
thf(set_Pr5052581263052047815nteger_type,type,
set_Pr5052581263052047815nteger: $tType ).
thf(produc3911288613690379145it_nat_type,type,
produc3911288613690379145it_nat: $tType ).
thf(produc2867611627572283311it_nat_type,type,
produc2867611627572283311it_nat: $tType ).
thf(set_in8474487674441654202_int_o_type,type,
set_in8474487674441654202_int_o: $tType ).
thf(set_Pr633603713510679705it_nat_type,type,
set_Pr633603713510679705it_nat: $tType ).
thf(set_op989438649584373901at_nat_type,type,
set_op989438649584373901at_nat: $tType ).
thf(option1583680563626158861at_nat_type,type,
option1583680563626158861at_nat: $tType ).
thf(produc3832618445565238089e_term_type,type,
produc3832618445565238089e_term: $tType ).
thf(produc7773217078559923341nt_int_type,type,
produc7773217078559923341nt_int: $tType ).
thf(set_Pr8551490117392284871at_nat_type,type,
set_Pr8551490117392284871at_nat: $tType ).
thf(set_Pr6777250647868329861it_nat_type,type,
set_Pr6777250647868329861it_nat: $tType ).
thf(option7428179582072448501nteger_type,type,
option7428179582072448501nteger: $tType ).
thf(set_se5479201105039950375at_nat_type,type,
set_se5479201105039950375at_nat: $tType ).
thf(produc7299876168958306407at_nat_type,type,
produc7299876168958306407at_nat: $tType ).
thf(produc6756470014200349799atural_type,type,
produc6756470014200349799atural: $tType ).
thf(produc3334582477557816039nteger_type,type,
produc3334582477557816039nteger: $tType ).
thf(set_Pr7010166363911110284_nat_o_type,type,
set_Pr7010166363911110284_nat_o: $tType ).
thf(produc3839731585411834681it_nat_type,type,
produc3839731585411834681it_nat: $tType ).
thf(set_Pr7322412474522714716atural_type,type,
set_Pr7322412474522714716atural: $tType ).
thf(option8699557107911914541at_nat_type,type,
option8699557107911914541at_nat: $tType ).
thf(set_op239864471688321678it_nat_type,type,
set_op239864471688321678it_nat: $tType ).
thf(set_op3940070208846178154it_nat_type,type,
set_op3940070208846178154it_nat: $tType ).
thf(produc4166570645942440679at_nat_type,type,
produc4166570645942440679at_nat: $tType ).
thf(produc2900562427881843919it_nat_type,type,
produc2900562427881843919it_nat: $tType ).
thf(set_Pr4329608150637261639at_nat_type,type,
set_Pr4329608150637261639at_nat: $tType ).
thf(produc6691574917238108761nteger_type,type,
produc6691574917238108761nteger: $tType ).
thf(produc4471711990508489141at_nat_type,type,
produc4471711990508489141at_nat: $tType ).
thf(set_na2454399383705037859atural_type,type,
set_na2454399383705037859atural: $tType ).
thf(set_in1345054734626228863atural_type,type,
set_in1345054734626228863atural: $tType ).
thf(produc6237349844158694175nteger_type,type,
produc6237349844158694175nteger: $tType ).
thf(set_se9180647916752606350_nat_o_type,type,
set_se9180647916752606350_nat_o: $tType ).
thf(option8956607266484857688it_nat_type,type,
option8956607266484857688it_nat: $tType ).
thf(option3216581401566546698it_nat_type,type,
option3216581401566546698it_nat: $tType ).
thf(produc5111566536631596683et_nat_type,type,
produc5111566536631596683et_nat: $tType ).
thf(produc8299537390109905600et_nat_type,type,
produc8299537390109905600et_nat: $tType ).
thf(produc3843707927480180839at_nat_type,type,
produc3843707927480180839at_nat: $tType ).
thf(set_Pr1354866905816374718it_nat_type,type,
set_Pr1354866905816374718it_nat: $tType ).
thf(produc3776562785724475560_o_int_type,type,
produc3776562785724475560_o_int: $tType ).
thf(set_Pr457366540195662369at_nat_type,type,
set_Pr457366540195662369at_nat: $tType ).
thf(set_Pr5142436192348053284it_nat_type,type,
set_Pr5142436192348053284it_nat: $tType ).
thf(produc6025053409261769070rm_int_type,type,
produc6025053409261769070rm_int: $tType ).
thf(set_Pr2352657477744078772atural_type,type,
set_Pr2352657477744078772atural: $tType ).
thf(produc8065447618272157327et_nat_type,type,
produc8065447618272157327et_nat: $tType ).
thf(set_Pr8693737435421807431at_nat_type,type,
set_Pr8693737435421807431at_nat: $tType ).
thf(set_Pr2560585780119916871nt_int_type,type,
set_Pr2560585780119916871nt_int: $tType ).
thf(produc8664842809031399944it_nat_type,type,
produc8664842809031399944it_nat: $tType ).
thf(produc732395585841259969at_nat_type,type,
produc732395585841259969at_nat: $tType ).
thf(produc6714399278180371524it_nat_type,type,
produc6714399278180371524it_nat: $tType ).
thf(set_Pr1932065953672099015od_o_o_type,type,
set_Pr1932065953672099015od_o_o: $tType ).
thf(produc3981471736659609608atural_type,type,
produc3981471736659609608atural: $tType ).
thf(produc5835291356934675326atural_type,type,
produc5835291356934675326atural: $tType ).
thf(produc3346328345660746739nteger_type,type,
produc3346328345660746739nteger: $tType ).
thf(set_Pr4532377907799695533_nat_o_type,type,
set_Pr4532377907799695533_nat_o: $tType ).
thf(produc859450856879609959at_nat_type,type,
produc859450856879609959at_nat: $tType ).
thf(produc1219242969750017639nt_int_type,type,
produc1219242969750017639nt_int: $tType ).
thf(set_in3461395444621081367e_term_type,type,
set_in3461395444621081367e_term: $tType ).
thf(set_Pr9591959067864425nteger_type,type,
set_Pr9591959067864425nteger: $tType ).
thf(option936205604648967762et_nat_type,type,
option936205604648967762et_nat: $tType ).
thf(produc2934264451710624999od_o_o_type,type,
produc2934264451710624999od_o_o: $tType ).
thf(set_Pr7577011563204128103nteger_type,type,
set_Pr7577011563204128103nteger: $tType ).
thf(set_Pr3948176798113811640et_nat_type,type,
set_Pr3948176798113811640et_nat: $tType ).
thf(produc6162884466328367972nteger_type,type,
produc6162884466328367972nteger: $tType ).
thf(set_na3661387095409732706nteger_type,type,
set_na3661387095409732706nteger: $tType ).
thf(set_in2260935666578096390nteger_type,type,
set_in2260935666578096390nteger: $tType ).
thf(produc4972180933644002618e_term_type,type,
produc4972180933644002618e_term: $tType ).
thf(produc6241069584506657477e_term_type,type,
produc6241069584506657477e_term: $tType ).
thf(set_se3372686590935047281atural_type,type,
set_se3372686590935047281atural: $tType ).
thf(set_in2553536192574375378_nat_o_type,type,
set_in2553536192574375378_nat_o: $tType ).
thf(produc6491284506569428743nteger_type,type,
produc6491284506569428743nteger: $tType ).
thf(produc3658429121746597890et_nat_type,type,
produc3658429121746597890et_nat: $tType ).
thf(set_Pr7477759153910077568at_num_type,type,
set_Pr7477759153910077568at_num: $tType ).
thf(set_Pr2539167527615954998at_nat_type,type,
set_Pr2539167527615954998at_nat: $tType ).
thf(set_Pr7717912310451564380at_nat_type,type,
set_Pr7717912310451564380at_nat: $tType ).
thf(produc366245978424229472at_nat_type,type,
produc366245978424229472at_nat: $tType ).
thf(produc3313772616054891654at_nat_type,type,
produc3313772616054891654at_nat: $tType ).
thf(produc5665947927044467078nt_int_type,type,
produc5665947927044467078nt_int: $tType ).
thf(produc382792921321436433nt_int_type,type,
produc382792921321436433nt_int: $tType ).
thf(option5403585828896915703atural_type,type,
option5403585828896915703atural: $tType ).
thf(option2651255830984564193nteger_type,type,
option2651255830984564193nteger: $tType ).
thf(set_Pr3451248702717554689st_nat_type,type,
set_Pr3451248702717554689st_nat: $tType ).
thf(set_Pr3770298976803184519nt_int_type,type,
set_Pr3770298976803184519nt_int: $tType ).
thf(produc8551481072490612790e_term_type,type,
produc8551481072490612790e_term: $tType ).
thf(set_Pr6558897299634722526_nat_o_type,type,
set_Pr6558897299634722526_nat_o: $tType ).
thf(set_se5158245632345848097at_nat_type,type,
set_se5158245632345848097at_nat: $tType ).
thf(set_Pr5488025237498180813et_nat_type,type,
set_Pr5488025237498180813et_nat: $tType ).
thf(set_Pr2522554150109002629et_int_type,type,
set_Pr2522554150109002629et_int: $tType ).
thf(set_Pr7564037697178849041atural_type,type,
set_Pr7564037697178849041atural: $tType ).
thf(set_Pr4811707699266497531nteger_type,type,
set_Pr4811707699266497531nteger: $tType ).
thf(option6357759511663192854e_term_type,type,
option6357759511663192854e_term: $tType ).
thf(produc6653097349344004940it_nat_type,type,
produc6653097349344004940it_nat: $tType ).
thf(produc9082142974458947146at_num_type,type,
produc9082142974458947146at_num: $tType ).
thf(produc7248412053542808358at_nat_type,type,
produc7248412053542808358at_nat: $tType ).
thf(produc759720530913461378nt_int_type,type,
produc759720530913461378nt_int: $tType ).
thf(set_Pr5094982260447487303t_unit_type,type,
set_Pr5094982260447487303t_unit: $tType ).
thf(set_Pr7909803484932130503_nat_o_type,type,
set_Pr7909803484932130503_nat_o: $tType ).
thf(set_mu2057375006010111271at_nat_type,type,
set_mu2057375006010111271at_nat: $tType ).
thf(set_op4508134149509766951at_nat_type,type,
set_op4508134149509766951at_nat: $tType ).
thf(set_na7251125088705586816nt_int_type,type,
set_na7251125088705586816nt_int: $tType ).
thf(set_in6154042108061588260nt_int_type,type,
set_in6154042108061588260nt_int: $tType ).
thf(option8963830502488799655at_nat_type,type,
option8963830502488799655at_nat: $tType ).
thf(produc1828647624359046049st_nat_type,type,
produc1828647624359046049st_nat: $tType ).
thf(set_Pr698032948827214833st_nat_type,type,
set_Pr698032948827214833st_nat: $tType ).
thf(set_Pr7549493975000385137at_nat_type,type,
set_Pr7549493975000385137at_nat: $tType ).
thf(produc652263959640188542_nat_o_type,type,
produc652263959640188542_nat_o: $tType ).
thf(option8057788054806935849nteger_type,type,
option8057788054806935849nteger: $tType ).
thf(set_se7855581050983116737at_nat_type,type,
set_se7855581050983116737at_nat: $tType ).
thf(set_Pr2406931829603198446nteger_type,type,
set_Pr2406931829603198446nteger: $tType ).
thf(set_Pr8415741480598773322nteger_type,type,
set_Pr8415741480598773322nteger: $tType ).
thf(set_Pr8986988648414616686er_nat_type,type,
set_Pr8986988648414616686er_nat: $tType ).
thf(set_Pr6496905503482889930er_int_type,type,
set_Pr6496905503482889930er_int: $tType ).
thf(produc7819656566062154093et_nat_type,type,
produc7819656566062154093et_nat: $tType ).
thf(produc2115011035271226405et_int_type,type,
produc2115011035271226405et_int: $tType ).
thf(produc7822875418678951345atural_type,type,
produc7822875418678951345atural: $tType ).
thf(produc8923325533196201883nteger_type,type,
produc8923325533196201883nteger: $tType ).
thf(set_Pr4577759397028426247_set_o_type,type,
set_Pr4577759397028426247_set_o: $tType ).
thf(set_Pr1763845938948868674it_nat_type,type,
set_Pr1763845938948868674it_nat: $tType ).
thf(set_Pr8497134830871917726it_int_type,type,
set_Pr8497134830871917726it_int: $tType ).
thf(set_Pr4334478416066269672t_unit_type,type,
set_Pr4334478416066269672t_unit: $tType ).
thf(set_Pr5889264611543340172t_unit_type,type,
set_Pr5889264611543340172t_unit: $tType ).
thf(set_Pr5582243495563764594_nat_o_type,type,
set_Pr5582243495563764594_nat_o: $tType ).
thf(set_Co726186806682698383nteger_type,type,
set_Co726186806682698383nteger: $tType ).
thf(produc7360885484439884007_nat_o_type,type,
produc7360885484439884007_nat_o: $tType ).
thf(multis2468970476368604999at_nat_type,type,
multis2468970476368604999at_nat: $tType ).
thf(set_set_set_list_nat_type,type,
set_set_set_list_nat: $tType ).
thf(option4927543243414619207at_nat_type,type,
option4927543243414619207at_nat: $tType ).
thf(option4624381673175914239nt_int_type,type,
option4624381673175914239nt_int: $tType ).
thf(set_se8531188866349061887nteger_type,type,
set_se8531188866349061887nteger: $tType ).
thf(set_se7118615804146677933t_unit_type,type,
set_se7118615804146677933t_unit: $tType ).
thf(produc4575160907756185873st_nat_type,type,
produc4575160907756185873st_nat: $tType ).
thf(produc1540777390238407569at_nat_type,type,
produc1540777390238407569at_nat: $tType ).
thf(set_Pr6200539531224447659at_num_type,type,
set_Pr6200539531224447659at_num: $tType ).
thf(set_Pr1261947904930325089at_nat_type,type,
set_Pr1261947904930325089at_nat: $tType ).
thf(set_Pr7995236796853374141at_int_type,type,
set_Pr7995236796853374141at_int: $tType ).
thf(set_Pr8387461105917469447nt_num_type,type,
set_Pr8387461105917469447nt_num: $tType ).
thf(set_Pr3448869479623346877nt_nat_type,type,
set_Pr3448869479623346877nt_nat: $tType ).
thf(set_Pr958786334691620121nt_int_type,type,
set_Pr958786334691620121nt_int: $tType ).
thf(produc2591615631378489102nteger_type,type,
produc2591615631378489102nteger: $tType ).
thf(produc2963269191615333738nteger_type,type,
produc2963269191615333738nteger: $tType ).
thf(produc7142191362829087448er_num_type,type,
produc7142191362829087448er_num: $tType ).
thf(produc6433947425880249742er_nat_type,type,
produc6433947425880249742er_nat: $tType ).
thf(produc2256096406371053034er_int_type,type,
produc2256096406371053034er_int: $tType ).
thf(produc7369051934464679207_set_o_type,type,
produc7369051934464679207_set_o: $tType ).
thf(set_option_set_nat_type,type,
set_option_set_nat: $tType ).
thf(set_op687863988967635939nteger_type,type,
set_op687863988967635939nteger: $tType ).
thf(set_op3165557761946182707t_unit_type,type,
set_op3165557761946182707t_unit: $tType ).
thf(set_nat_nat_o_type,type,
set_nat_nat_o: $tType ).
thf(option8137458692691377843t_unit_type,type,
option8137458692691377843t_unit: $tType ).
thf(set_set_list_nat_type,type,
set_set_list_nat: $tType ).
thf(set_Pr3149072824959771635_nat_o_type,type,
set_Pr3149072824959771635_nat_o: $tType ).
thf(set_Pr903927857289325719_int_o_type,type,
set_Pr903927857289325719_int_o: $tType ).
thf(set_Pr7040061329075590551_o_num_type,type,
set_Pr7040061329075590551_o_num: $tType ).
thf(set_Pr2101469702781467981_o_nat_type,type,
set_Pr2101469702781467981_o_nat: $tType ).
thf(set_Pr8834758594704517033_o_int_type,type,
set_Pr8834758594704517033_o_int: $tType ).
thf(produc6271795597528267376eger_o_type,type,
produc6271795597528267376eger_o: $tType ).
thf(set_set_set_nat_type,type,
set_set_set_nat: $tType ).
thf(set_set_set_int_type,type,
set_set_set_int: $tType ).
thf(set_set_Code_integer_type,type,
set_set_Code_integer: $tType ).
thf(heap_T5738788834812785303t_unit_type,type,
heap_T5738788834812785303t_unit: $tType ).
thf(heap_T6362127782908069795rray_a_type,type,
heap_T6362127782908069795rray_a: $tType ).
thf(set_set_Product_unit_type,type,
set_set_Product_unit: $tType ).
thf(heap_e7401611519738050253t_unit_type,type,
heap_e7401611519738050253t_unit: $tType ).
thf(product_prod_num_num_type,type,
product_prod_num_num: $tType ).
thf(product_prod_nat_num_type,type,
product_prod_nat_num: $tType ).
thf(product_prod_nat_nat_type,type,
product_prod_nat_nat: $tType ).
thf(product_prod_nat_int_type,type,
product_prod_nat_int: $tType ).
thf(product_prod_int_num_type,type,
product_prod_int_num: $tType ).
thf(product_prod_int_nat_type,type,
product_prod_int_nat: $tType ).
thf(product_prod_int_int_type,type,
product_prod_int_int: $tType ).
thf(set_Product_prod_o_o_type,type,
set_Product_prod_o_o: $tType ).
thf(sum_sum_nat_nat_type,type,
sum_sum_nat_nat: $tType ).
thf(set_option_num_type,type,
set_option_num: $tType ).
thf(set_option_nat_type,type,
set_option_nat: $tType ).
thf(set_option_int_type,type,
set_option_int: $tType ).
thf(option_set_nat_type,type,
option_set_nat: $tType ).
thf(option_set_int_type,type,
option_set_int: $tType ).
thf(option_Code_integer_type,type,
option_Code_integer: $tType ).
thf(option_Product_unit_type,type,
option_Product_unit: $tType ).
thf(option_nat_o_type,type,
option_nat_o: $tType ).
thf(set_list_nat_type,type,
set_list_nat: $tType ).
thf(product_prod_nat_o_type,type,
product_prod_nat_o: $tType ).
thf(product_prod_int_o_type,type,
product_prod_int_o: $tType ).
thf(product_prod_o_num_type,type,
product_prod_o_num: $tType ).
thf(product_prod_o_nat_type,type,
product_prod_o_nat: $tType ).
thf(product_prod_o_int_type,type,
product_prod_o_int: $tType ).
thf(set_set_nat_type,type,
set_set_nat: $tType ).
thf(set_set_int_type,type,
set_set_int: $tType ).
thf(set_Code_natural_type,type,
set_Code_natural: $tType ).
thf(set_Code_integer_type,type,
set_Code_integer: $tType ).
thf(option_assn_type,type,
option_assn: $tType ).
thf(ref_Product_unit_type,type,
ref_Product_unit: $tType ).
thf(set_Product_unit_type,type,
set_Product_unit: $tType ).
thf(set_option_o_type,type,
set_option_o: $tType ).
thf(set_nat_o_type,type,
set_nat_o: $tType ).
thf(option_set_o_type,type,
option_set_o: $tType ).
thf(ref_array_a_type,type,
ref_array_a: $tType ).
thf(product_prod_o_o_type,type,
product_prod_o_o: $tType ).
thf(set_assn_type,type,
set_assn: $tType ).
thf(set_set_o_type,type,
set_set_o: $tType ).
thf(option_rat_type,type,
option_rat: $tType ).
thf(option_num_type,type,
option_num: $tType ).
thf(option_nat_type,type,
option_nat: $tType ).
thf(option_int_type,type,
option_int: $tType ).
thf(list_char_type,type,
list_char: $tType ).
thf(list_nat_type,type,
list_nat: $tType ).
thf(list_int_type,type,
list_int: $tType ).
thf(set_rat_type,type,
set_rat: $tType ).
thf(set_num_type,type,
set_num: $tType ).
thf(set_nat_type,type,
set_nat: $tType ).
thf(set_int_type,type,
set_int: $tType ).
thf(code_natural_type,type,
code_natural: $tType ).
thf(code_integer_type,type,
code_integer: $tType ).
thf(product_unit_type,type,
product_unit: $tType ).
thf(option_o_type,type,
option_o: $tType ).
thf(array_a_type,type,
array_a: $tType ).
thf(list_a_type,type,
list_a: $tType ).
thf(typerep_type,type,
typerep: $tType ).
thf(assn_type,type,
assn: $tType ).
thf(set_o_type,type,
set_o: $tType ).
thf(char_type,type,
char: $tType ).
thf(rat_type,type,
rat: $tType ).
thf(num_type,type,
num: $tType ).
thf(nat_type,type,
nat: $tType ).
thf(int_type,type,
int: $tType ).
thf(a_type,type,
a: $tType ).
thf(array_of_list_a_decl,type,
array_of_list_a: list_a > heap_T6362127782908069795rray_a ).
thf(heap_T5591663578999710211rray_a_decl,type,
heap_T5591663578999710211rray_a: heap_T6362127782908069795rray_a > heap_e7401611519738050253t_unit > option3216581401566546698it_nat ).
thf(heap_T6932021131025641745rray_a_decl,type,
heap_T6932021131025641745rray_a: heap_T6362127782908069795rray_a > heap_e7401611519738050253t_unit > $o ).
thf(none_P2587165478634041381it_nat_decl,type,
none_P2587165478634041381it_nat: option3216581401566546698it_nat ).
thf(some_P6105628898608307625it_nat_decl,type,
some_P6105628898608307625it_nat: produc6714399278180371524it_nat > option3216581401566546698it_nat ).
thf(produc1733996804261680252it_nat_decl,type,
produc1733996804261680252it_nat: array_a > produc6653097349344004940it_nat > produc6714399278180371524it_nat ).
thf(h_decl,type,
h: heap_e7401611519738050253t_unit ).
thf(xs_decl,type,
xs: list_a ).
thf(sk1_decl,type,
sk1: heap_e7401611519738050253t_unit > heap_T6362127782908069795rray_a > array_a ).
thf(sk2_decl,type,
sk2: heap_e7401611519738050253t_unit > heap_T6362127782908069795rray_a > produc6653097349344004940it_nat ).
thf(sk1_def,definition,
( sk1
= ( ^ [A: heap_e7401611519738050253t_unit,B: heap_T6362127782908069795rray_a] :
@+[C: array_a] :
? [D: produc6653097349344004940it_nat] :
( ( heap_T5591663578999710211rray_a @ B @ A )
= ( some_P6105628898608307625it_nat @ ( produc1733996804261680252it_nat @ C @ D ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( ^ [A: heap_e7401611519738050253t_unit,B: heap_T6362127782908069795rray_a] :
@+[C: produc6653097349344004940it_nat] :
( ( heap_T5591663578999710211rray_a @ B @ A )
= ( some_P6105628898608307625it_nat @ ( produc1733996804261680252it_nat @ ( sk1 @ A @ B ) @ C ) ) ) ) ) ).
thf(1,conjecture,
( ( heap_T5591663578999710211rray_a @ ( array_of_list_a @ xs ) @ h )
!= none_P2587165478634041381it_nat ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
thf(2,negated_conjecture,
~ ( ( ( heap_T5591663578999710211rray_a @ ( array_of_list_a @ xs ) @ h )
!= none_P2587165478634041381it_nat ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(61,plain,
~ ( ( ( heap_T5591663578999710211rray_a @ ( array_of_list_a @ xs ) @ h )
!= none_P2587165478634041381it_nat ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(62,plain,
( ( heap_T5591663578999710211rray_a @ ( array_of_list_a @ xs ) @ h )
= none_P2587165478634041381it_nat ),
inference(polarity_switch,[status(thm)],[61]) ).
thf(63,plain,
( ( heap_T5591663578999710211rray_a @ ( array_of_list_a @ xs ) @ h )
= none_P2587165478634041381it_nat ),
inference(lifteq,[status(thm)],[62]) ).
thf(4,axiom,
! [A: heap_T6362127782908069795rray_a,B: heap_e7401611519738050253t_unit] :
( ( heap_T6932021131025641745rray_a @ A @ B )
=> ~ ! [C: array_a,D: produc6653097349344004940it_nat] :
( ( heap_T5591663578999710211rray_a @ A @ B )
!= ( some_P6105628898608307625it_nat @ ( produc1733996804261680252it_nat @ C @ D ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_119_successE) ).
thf(67,plain,
! [A: heap_T6362127782908069795rray_a,B: heap_e7401611519738050253t_unit] :
( ( heap_T6932021131025641745rray_a @ A @ B )
=> ~ ! [C: array_a,D: produc6653097349344004940it_nat] :
( ( heap_T5591663578999710211rray_a @ A @ B )
!= ( some_P6105628898608307625it_nat @ ( produc1733996804261680252it_nat @ C @ D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(68,plain,
! [A: heap_T6362127782908069795rray_a,B: heap_e7401611519738050253t_unit] :
( ( heap_T6932021131025641745rray_a @ A @ B )
=> ~ ~ ? [C: array_a,D: produc6653097349344004940it_nat] :
( ( heap_T5591663578999710211rray_a @ A @ B )
= ( some_P6105628898608307625it_nat @ ( produc1733996804261680252it_nat @ C @ D ) ) ) ),
inference(miniscope,[status(thm)],[67]) ).
thf(69,plain,
! [B: heap_e7401611519738050253t_unit,A: heap_T6362127782908069795rray_a] :
( ~ ( heap_T6932021131025641745rray_a @ A @ B )
| ( ( heap_T5591663578999710211rray_a @ A @ B )
= ( some_P6105628898608307625it_nat @ ( produc1733996804261680252it_nat @ ( sk1 @ B @ A ) @ ( sk2 @ B @ A ) ) ) ) ),
inference(cnf,[status(esa)],[68]) ).
thf(70,plain,
! [B: heap_e7401611519738050253t_unit,A: heap_T6362127782908069795rray_a] :
( ( ( heap_T5591663578999710211rray_a @ A @ B )
= ( some_P6105628898608307625it_nat @ ( produc1733996804261680252it_nat @ ( sk1 @ B @ A ) @ ( sk2 @ B @ A ) ) ) )
| ~ ( heap_T6932021131025641745rray_a @ A @ B ) ),
inference(lifteq,[status(thm)],[69]) ).
thf(7,axiom,
! [A: produc6714399278180371524it_nat] :
( none_P2587165478634041381it_nat
!= ( some_P6105628898608307625it_nat @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_84_option_Odistinct_I1_J) ).
thf(77,plain,
! [A: produc6714399278180371524it_nat] :
( none_P2587165478634041381it_nat
!= ( some_P6105628898608307625it_nat @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(78,plain,
~ ? [A: produc6714399278180371524it_nat] :
( none_P2587165478634041381it_nat
= ( some_P6105628898608307625it_nat @ A ) ),
inference(miniscope,[status(thm)],[77]) ).
thf(79,plain,
! [A: produc6714399278180371524it_nat] :
( none_P2587165478634041381it_nat
!= ( some_P6105628898608307625it_nat @ A ) ),
inference(cnf,[status(esa)],[78]) ).
thf(80,plain,
! [A: produc6714399278180371524it_nat] :
( ( some_P6105628898608307625it_nat @ A )
!= none_P2587165478634041381it_nat ),
inference(lifteq,[status(thm)],[79]) ).
thf(327,plain,
! [C: produc6714399278180371524it_nat,B: heap_e7401611519738050253t_unit,A: heap_T6362127782908069795rray_a] :
( ~ ( heap_T6932021131025641745rray_a @ A @ B )
| ( ( heap_T5591663578999710211rray_a @ A @ B )
!= none_P2587165478634041381it_nat )
| ( ( some_P6105628898608307625it_nat @ ( produc1733996804261680252it_nat @ ( sk1 @ B @ A ) @ ( sk2 @ B @ A ) ) )
!= ( some_P6105628898608307625it_nat @ C ) ) ),
inference(paramod_ordered,[status(thm)],[70,80]) ).
thf(328,plain,
! [B: heap_T6362127782908069795rray_a,A: heap_e7401611519738050253t_unit] :
( ~ ( heap_T6932021131025641745rray_a @ B @ A )
| ( ( heap_T5591663578999710211rray_a @ B @ A )
!= none_P2587165478634041381it_nat ) ),
inference(pattern_uni,[status(thm)],[327:[bind(A,$thf( I )),bind(B,$thf( H )),bind(C,$thf( produc1733996804261680252it_nat @ ( sk1 @ H @ I ) @ ( sk2 @ H @ I ) ))]]) ).
thf(329,plain,
! [B: heap_T6362127782908069795rray_a,A: heap_e7401611519738050253t_unit] :
( ~ ( heap_T6932021131025641745rray_a @ B @ A )
| ( ( heap_T5591663578999710211rray_a @ B @ A )
!= none_P2587165478634041381it_nat ) ),
inference(simp,[status(thm)],[328]) ).
thf(337,plain,
! [B: heap_T6362127782908069795rray_a,A: heap_e7401611519738050253t_unit] :
( ~ ( heap_T6932021131025641745rray_a @ B @ A )
| ( none_P2587165478634041381it_nat != none_P2587165478634041381it_nat )
| ( ( heap_T5591663578999710211rray_a @ ( array_of_list_a @ xs ) @ h )
!= ( heap_T5591663578999710211rray_a @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[63,329]) ).
thf(338,plain,
! [B: heap_T6362127782908069795rray_a,A: heap_e7401611519738050253t_unit] :
( ~ ( heap_T6932021131025641745rray_a @ B @ A )
| ( ( heap_T5591663578999710211rray_a @ ( array_of_list_a @ xs ) @ h )
!= ( heap_T5591663578999710211rray_a @ B @ A ) ) ),
inference(simp,[status(thm)],[337]) ).
thf(339,plain,
~ ( heap_T6932021131025641745rray_a @ ( array_of_list_a @ xs ) @ h ),
inference(pattern_uni,[status(thm)],[338:[bind(A,$thf( h )),bind(B,$thf( array_of_list_a @ xs ))]]) ).
thf(38,axiom,
! [A: list_a,B: heap_e7401611519738050253t_unit] : ( heap_T6932021131025641745rray_a @ ( array_of_list_a @ A ) @ B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_45_success__of__listI) ).
thf(186,plain,
! [A: list_a,B: heap_e7401611519738050253t_unit] : ( heap_T6932021131025641745rray_a @ ( array_of_list_a @ A ) @ B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(187,plain,
! [B: heap_e7401611519738050253t_unit,A: list_a] : ( heap_T6932021131025641745rray_a @ ( array_of_list_a @ A ) @ B ),
inference(cnf,[status(esa)],[186]) ).
thf(1931,plain,
~ $true,
inference(rewrite,[status(thm)],[339,187]) ).
thf(1932,plain,
$false,
inference(simp,[status(thm)],[1931]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP216^3 : TPTP v9.3.1. Bugfixed v9.2.1.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.10/0.22 % Computer : n001.cluster.edu
% 0.10/0.22 % Model : x86_64 x86_64
% 0.10/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.22 % Memory : 8046.5625MB
% 0.10/0.22 % OS : Linux 6.8.0-71-generic
% 0.10/0.22 % CPULimit : 300
% 0.10/0.22 % WCLimit : 300
% 0.10/0.22 % DateTime : Tue Sep 29 20:22:21 UTC 2026
% 0.10/0.22 % CPUTime :
% 0.10/0.22 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 1.07/0.82 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 8.94/2.78 % [INFO] Parsing done (1952ms).
% 8.94/2.80 % [INFO] Running in sequential loop mode.
% 10.36/3.23 % [INFO] eprover registered as external prover.
% 10.36/3.23 % [INFO] Scanning for conjecture ...
% 13.32/3.94 % [INFO] Found a conjecture (or negated_conjecture) and 8002 axioms. Running axiom selection ...
% 14.40/4.24 % [INFO] Axiom selection finished. Selected 58 axioms (removed 7944 axioms).
% 14.76/4.38 % [INFO] Problem is higher-order (TPTP THF).
% 15.05/4.40 % [INFO] Type checking passed.
% 15.05/4.41 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 47.88/13.33 % [INFO] Killing All external provers ...
% 47.88/13.34 % Time passed: 12969ms (effective reasoning time: 10531ms)
% 47.88/13.34 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 47.88/13.34 % Axioms used in derivation (3): fact_119_successE, fact_84_option_Odistinct_I1_J, fact_45_success__of__listI
% 47.88/13.34 % No. of inferences in proof: 26
% 47.88/13.34 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 12969 ms resp. 10531 ms w/o parsing
% 48.36/13.40 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 48.36/13.40 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------