%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP219^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 : n014.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:15 AM UTC 2026
% Result : Theorem 37.69s 9.87s
% Output : Refutation 38.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 4
% Syntax : Number of formulae : 21 ( 11 unt; 0 typ; 0 def)
% Number of atoms : 42 ( 12 equ; 0 cnn)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 92 ( 23 ~; 13 |; 0 &; 52 @)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 5 avg)
% Number of types : 237 ( 236 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 7 ( 4 usr; 5 con; 0-2 aty)
% Number of variables : 17 ( 0 ^; 17 !; 0 ?; 17 :)
% 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_Pr8634505666381077339nt_int_type,type,
set_Pr8634505666381077339nt_int: $tType ).
thf(list_P362550909693114634et_nat_type,type,
list_P362550909693114634et_nat: $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(produc2732055786443039994et_nat_type,type,
produc2732055786443039994et_nat: $tType ).
thf(produc1319942482725812455at_nat_type,type,
produc1319942482725812455at_nat: $tType ).
thf(list_P6548900253507351021at_nat_type,type,
list_P6548900253507351021at_nat: $tType ).
thf(set_Pr5564308138774400199at_nat_type,type,
set_Pr5564308138774400199at_nat: $tType ).
thf(produc1906917888121415911at_nat_type,type,
produc1906917888121415911at_nat: $tType ).
thf(list_P7828571989066258726nteger_type,type,
list_P7828571989066258726nteger: $tType ).
thf(set_Pr1281608226676607948nteger_type,type,
set_Pr1281608226676607948nteger: $tType ).
thf(produc989692990947075319atural_type,type,
produc989692990947075319atural: $tType ).
thf(produc1908205239877642774nteger_type,type,
produc1908205239877642774nteger: $tType ).
thf(list_P651320350408439699nt_int_type,type,
list_P651320350408439699nt_int: $tType ).
thf(set_Pr9222295170931077689nt_int_type,type,
set_Pr9222295170931077689nt_int: $tType ).
thf(list_P6107040726529854061_nat_o_type,type,
list_P6107040726529854061_nat_o: $tType ).
thf(set_Pr2161125870931222855_nat_o_type,type,
set_Pr2161125870931222855_nat_o: $tType ).
thf(produc2285326912895808259nt_int_type,type,
produc2285326912895808259nt_int: $tType ).
thf(list_P2321686559999237006et_nat_type,type,
list_P2321686559999237006et_nat: $tType ).
thf(set_Pr3286484037609594932et_nat_type,type,
set_Pr3286484037609594932et_nat: $tType ).
thf(produc4928098042776334183_nat_o_type,type,
produc4928098042776334183_nat_o: $tType ).
thf(produc4530688714081574576n_assn_type,type,
produc4530688714081574576n_assn: $tType ).
thf(produc3925858234332021118et_nat_type,type,
produc3925858234332021118et_nat: $tType ).
thf(produc8731074985263844745atural_type,type,
produc8731074985263844745atural: $tType ).
thf(produc8763457246119570046nteger_type,type,
produc8763457246119570046nteger: $tType ).
thf(list_P1316552470764441098e_term_type,type,
list_P1316552470764441098e_term: $tType ).
thf(set_Pr7604974323444597168e_term_type,type,
set_Pr7604974323444597168e_term: $tType ).
thf(list_P1743416141875011707e_term_type,type,
list_P1743416141875011707e_term: $tType ).
thf(set_Pr3642885161833720865e_term_type,type,
set_Pr3642885161833720865e_term: $tType ).
thf(list_P8915022641806594461nt_int_type,type,
list_P8915022641806594461nt_int: $tType ).
thf(set_Pr1872883991513573699nt_int_type,type,
set_Pr1872883991513573699nt_int: $tType ).
thf(set_Pr4333006031979791559at_nat_type,type,
set_Pr4333006031979791559at_nat: $tType ).
thf(set_Pr6863447823992824007n_assn_type,type,
set_Pr6863447823992824007n_assn: $tType ).
thf(produc7773217078559923341nt_int_type,type,
produc7773217078559923341nt_int: $tType ).
thf(set_Pr8551490117392284871at_nat_type,type,
set_Pr8551490117392284871at_nat: $tType ).
thf(produc424102278133772007at_nat_type,type,
produc424102278133772007at_nat: $tType ).
thf(produc337509097454979815n_assn_type,type,
produc337509097454979815n_assn: $tType ).
thf(list_s4242580248156217677at_nat_type,type,
list_s4242580248156217677at_nat: $tType ).
thf(produc6756470014200349799atural_type,type,
produc6756470014200349799atural: $tType ).
thf(produc4166570645942440679at_nat_type,type,
produc4166570645942440679at_nat: $tType ).
thf(list_P5464809261938338413at_nat_type,type,
list_P5464809261938338413at_nat: $tType ).
thf(list_P28140577958321773n_assn_type,type,
list_P28140577958321773n_assn: $tType ).
thf(set_Pr4329608150637261639at_nat_type,type,
set_Pr4329608150637261639at_nat: $tType ).
thf(set_Pr8116311503512020807n_assn_type,type,
set_Pr8116311503512020807n_assn: $tType ).
thf(option8956607266484857688it_nat_type,type,
option8956607266484857688it_nat: $tType ).
thf(produc3843707927480180839at_nat_type,type,
produc3843707927480180839at_nat: $tType ).
thf(produc9053633027152450663n_assn_type,type,
produc9053633027152450663n_assn: $tType ).
thf(set_Pr457366540195662369at_nat_type,type,
set_Pr457366540195662369at_nat: $tType ).
thf(set_Pr488414391616402044st_nat_type,type,
set_Pr488414391616402044st_nat: $tType ).
thf(set_Pr4898238009683259096st_int_type,type,
set_Pr4898238009683259096st_int: $tType ).
thf(set_Pr7093487733527993602n_assn_type,type,
set_Pr7093487733527993602n_assn: $tType ).
thf(set_Pr4168565316758867366n_assn_type,type,
set_Pr4168565316758867366n_assn: $tType ).
thf(list_P8469869581646625389at_nat_type,type,
list_P8469869581646625389at_nat: $tType ).
thf(set_Pr8693737435421807431at_nat_type,type,
set_Pr8693737435421807431at_nat: $tType ).
thf(produc8664842809031399944it_nat_type,type,
produc8664842809031399944it_nat: $tType ).
thf(produc732395585841259969at_nat_type,type,
produc732395585841259969at_nat: $tType ).
thf(set_Pr1932065953672099015od_o_o_type,type,
set_Pr1932065953672099015od_o_o: $tType ).
thf(produc6654255674790325574st_nat_type,type,
produc6654255674790325574st_nat: $tType ).
thf(produc4164172529858598818st_int_type,type,
produc4164172529858598818st_int: $tType ).
thf(produc2555908794901494476n_assn_type,type,
produc2555908794901494476n_assn: $tType ).
thf(produc8582807064127716720n_assn_type,type,
produc8582807064127716720n_assn: $tType ).
thf(list_P7985473006766602707_nat_o_type,type,
list_P7985473006766602707_nat_o: $tType ).
thf(produc5835291356934675326atural_type,type,
produc5835291356934675326atural: $tType ).
thf(set_Pr4532377907799695533_nat_o_type,type,
set_Pr4532377907799695533_nat_o: $tType ).
thf(list_i8448526496819171953e_term_type,type,
list_i8448526496819171953e_term: $tType ).
thf(produc859450856879609959at_nat_type,type,
produc859450856879609959at_nat: $tType ).
thf(set_in3461395444621081367e_term_type,type,
set_in3461395444621081367e_term: $tType ).
thf(produc2934264451710624999od_o_o_type,type,
produc2934264451710624999od_o_o: $tType ).
thf(list_P9062070895058802706et_nat_type,type,
list_P9062070895058802706et_nat: $tType ).
thf(set_Pr3948176798113811640et_nat_type,type,
set_Pr3948176798113811640et_nat: $tType ).
thf(list_P2911967483291296064sn_nat_type,type,
list_P2911967483291296064sn_nat: $tType ).
thf(list_P421884338359569308sn_int_type,type,
list_P421884338359569308sn_int: $tType ).
thf(list_P7711101519850957926n_assn_type,type,
list_P7711101519850957926n_assn: $tType ).
thf(list_P1495281457390866698n_assn_type,type,
list_P1495281457390866698n_assn: $tType ).
thf(set_Pr4672072672689440998sn_nat_type,type,
set_Pr4672072672689440998sn_nat: $tType ).
thf(set_Pr2181989527757714242sn_int_type,type,
set_Pr2181989527757714242sn_int: $tType ).
thf(set_Pr247834672394327052n_assn_type,type,
set_Pr247834672394327052n_assn: $tType ).
thf(set_Pr3255386646789011632n_assn_type,type,
set_Pr3255386646789011632n_assn: $tType ).
thf(produc4972180933644002618e_term_type,type,
produc4972180933644002618e_term: $tType ).
thf(produc6241069584506657477e_term_type,type,
produc6241069584506657477e_term: $tType ).
thf(produc3658429121746597890et_nat_type,type,
produc3658429121746597890et_nat: $tType ).
thf(list_P5953897101696565392at_nat_type,type,
list_P5953897101696565392at_nat: $tType ).
thf(list_P3463813956764838636at_int_type,type,
list_P3463813956764838636at_int: $tType ).
thf(list_P1909269847677398966at_nat_type,type,
list_P1909269847677398966at_nat: $tType ).
thf(list_P812186867033400410at_nat_type,type,
list_P812186867033400410at_nat: $tType ).
thf(set_Pr2539167527615954998at_nat_type,type,
set_Pr2539167527615954998at_nat: $tType ).
thf(set_Pr49084382684228242at_int_type,type,
set_Pr49084382684228242at_int: $tType ).
thf(set_Pr7717912310451564380at_nat_type,type,
set_Pr7717912310451564380at_nat: $tType ).
thf(set_Pr6620829329807565824at_nat_type,type,
set_Pr6620829329807565824at_nat: $tType ).
thf(produc3672657496626091440sn_nat_type,type,
produc3672657496626091440sn_nat: $tType ).
thf(produc8718178513971670540sn_int_type,type,
produc8718178513971670540sn_int: $tType ).
thf(produc1407301962063123414n_assn_type,type,
produc1407301962063123414n_assn: $tType ).
thf(produc3167338625816234618n_assn_type,type,
produc3167338625816234618n_assn: $tType ).
thf(list_s9130966667114977576at_nat_type,type,
list_s9130966667114977576at_nat: $tType ).
thf(produc254973753779126261st_nat_type,type,
produc254973753779126261st_nat: $tType ).
thf(produc5834231552977413017st_int_type,type,
produc5834231552977413017st_int: $tType ).
thf(set_Pr3451248702717554689st_nat_type,type,
set_Pr3451248702717554689st_nat: $tType ).
thf(set_Pr7861072320784411741st_int_type,type,
set_Pr7861072320784411741st_int: $tType ).
thf(set_Pr5578615432719617117st_nat_type,type,
set_Pr5578615432719617117st_nat: $tType ).
thf(set_Pr765067013931698361st_int_type,type,
set_Pr765067013931698361st_int: $tType ).
thf(list_l6351802567095793725n_assn_type,type,
list_l6351802567095793725n_assn: $tType ).
thf(produc8551481072490612790e_term_type,type,
produc8551481072490612790e_term: $tType ).
thf(list_P5578671422887162913nteger_type,type,
list_P5578671422887162913nteger: $tType ).
thf(set_Pr4811707699266497531nteger_type,type,
set_Pr4811707699266497531nteger: $tType ).
thf(option6357759511663192854e_term_type,type,
option6357759511663192854e_term: $tType ).
thf(set_Pr3005433631314115148st_nat_type,type,
set_Pr3005433631314115148st_nat: $tType ).
thf(set_Pr7415257249380972200st_int_type,type,
set_Pr7415257249380972200st_int: $tType ).
thf(set_Pr6760183905301009355st_nat_type,type,
set_Pr6760183905301009355st_nat: $tType ).
thf(set_Pr1946635486513090599st_int_type,type,
set_Pr1946635486513090599st_int: $tType ).
thf(set_Pr9082979648927643218list_d_type,type,
set_Pr9082979648927643218list_d: $tType ).
thf(set_Pr2380792130361903057list_c_type,type,
set_Pr2380792130361903057list_c: $tType ).
thf(produc6653097349344004940it_nat_type,type,
produc6653097349344004940it_nat: $tType ).
thf(produc8373899037510109440at_nat_type,type,
produc8373899037510109440at_nat: $tType ).
thf(produc4196048018000912732at_int_type,type,
produc4196048018000912732at_int: $tType ).
thf(produc7248412053542808358at_nat_type,type,
produc7248412053542808358at_nat: $tType ).
thf(produc1062882101152166346at_nat_type,type,
produc1062882101152166346at_nat: $tType ).
thf(set_Pr5674772971416283335list_d_type,type,
set_Pr5674772971416283335list_d: $tType ).
thf(set_Pr8195957489705318982list_c_type,type,
set_Pr8195957489705318982list_c: $tType ).
thf(set_Pr8760529213406277896list_d_type,type,
set_Pr8760529213406277896list_d: $tType ).
thf(set_Pr2058341694840537735list_c_type,type,
set_Pr2058341694840537735list_c: $tType ).
thf(produc1828647624359046049st_nat_type,type,
produc1828647624359046049st_nat: $tType ).
thf(produc8561936516282095101st_int_type,type,
produc8561936516282095101st_int: $tType ).
thf(produc3676724955757786621st_nat_type,type,
produc3676724955757786621st_nat: $tType ).
thf(produc1186641810826059865st_int_type,type,
produc1186641810826059865st_int: $tType ).
thf(list_s1210847774152347623at_nat_type,type,
list_s1210847774152347623at_nat: $tType ).
thf(list_P8527749157015355191n_assn_type,type,
list_P8527749157015355191n_assn: $tType ).
thf(set_se7855581050983116737at_nat_type,type,
set_se7855581050983116737at_nat: $tType ).
thf(set_Pr5949110396991348497n_assn_type,type,
set_Pr5949110396991348497n_assn: $tType ).
thf(produc7822875418678951345atural_type,type,
produc7822875418678951345atural: $tType ).
thf(produc8923325533196201883nteger_type,type,
produc8923325533196201883nteger: $tType ).
thf(produc2433097559162738582st_nat_type,type,
produc2433097559162738582st_nat: $tType ).
thf(produc9166386451085787634st_int_type,type,
produc9166386451085787634st_int: $tType ).
thf(produc1766198083622830229st_nat_type,type,
produc1766198083622830229st_nat: $tType ).
thf(produc8499486975545879281st_int_type,type,
produc8499486975545879281st_int: $tType ).
thf(produc1726512871120090780list_d_type,type,
produc1726512871120090780list_d: $tType ).
thf(produc1655478831073744795list_c_type,type,
produc1655478831073744795list_c: $tType ).
thf(multis2468970476368604999at_nat_type,type,
multis2468970476368604999at_nat: $tType ).
thf(produc2783776724613635559list_d_type,type,
produc2783776724613635559list_d: $tType ).
thf(produc2712742684567289574list_c_type,type,
produc2712742684567289574list_c: $tType ).
thf(produc8056257125849822888list_d_type,type,
produc8056257125849822888list_d: $tType ).
thf(produc7985223085803476903list_c_type,type,
produc7985223085803476903list_c: $tType ).
thf(filter1242075044329608583at_nat_type,type,
filter1242075044329608583at_nat: $tType ).
thf(list_P6011104703257516679at_nat_type,type,
list_P6011104703257516679at_nat: $tType ).
thf(list_P3521021558325789923at_int_type,type,
list_P3521021558325789923at_int: $tType ).
thf(list_P8198026277950538467nt_nat_type,type,
list_P8198026277950538467nt_nat: $tType ).
thf(list_P5707943133018811711nt_int_type,type,
list_P5707943133018811711nt_int: $tType ).
thf(set_Pr1261947904930325089at_nat_type,type,
set_Pr1261947904930325089at_nat: $tType ).
thf(set_Pr7995236796853374141at_int_type,type,
set_Pr7995236796853374141at_int: $tType ).
thf(set_Pr3448869479623346877nt_nat_type,type,
set_Pr3448869479623346877nt_nat: $tType ).
thf(set_Pr958786334691620121nt_int_type,type,
set_Pr958786334691620121nt_int: $tType ).
thf(produc6575502325842934193n_assn_type,type,
produc6575502325842934193n_assn: $tType ).
thf(list_P1934797086108301456_d_nat_type,type,
list_P1934797086108301456_d_nat: $tType ).
thf(list_P8668085978031350508_d_int_type,type,
list_P8668085978031350508_d_int: $tType ).
thf(list_P5561950507774946575_c_nat_type,type,
list_P5561950507774946575_c_nat: $tType ).
thf(list_P3071867362843219819_c_int_type,type,
list_P3071867362843219819_c_int: $tType ).
thf(list_P3064893870870525238_nat_d_type,type,
list_P3064893870870525238_nat_d: $tType ).
thf(list_P2993859830824179253_nat_c_type,type,
list_P2993859830824179253_nat_c: $tType ).
thf(set_Pr3276347184212964150_d_nat_type,type,
set_Pr3276347184212964150_d_nat: $tType ).
thf(set_Pr786264039281237394_d_int_type,type,
set_Pr786264039281237394_d_int: $tType ).
thf(set_Pr6903500605879609269_c_nat_type,type,
set_Pr6903500605879609269_c_nat: $tType ).
thf(set_Pr4413417460947882513_c_int_type,type,
set_Pr4413417460947882513_c_int: $tType ).
thf(set_Pr4406443968975187932_nat_d_type,type,
set_Pr4406443968975187932_nat_d: $tType ).
thf(set_Pr4335409928928841947_nat_c_type,type,
set_Pr4335409928928841947_nat_c: $tType ).
thf(produc6271795597528267376eger_o_type,type,
produc6271795597528267376eger_o: $tType ).
thf(heap_T5738788834812785303t_unit_type,type,
heap_T5738788834812785303t_unit: $tType ).
thf(list_P8926467638345140077od_d_d_type,type,
list_P8926467638345140077od_d_d: $tType ).
thf(list_P8855433598298794092od_d_c_type,type,
list_P8855433598298794092od_d_c: $tType ).
thf(list_P338744602095350958od_c_d_type,type,
list_P338744602095350958od_c_d: $tType ).
thf(list_P267710562049004973od_c_c_type,type,
list_P267710562049004973od_c_c: $tType ).
thf(set_Product_prod_d_d_type,type,
set_Product_prod_d_d: $tType ).
thf(set_Product_prod_d_c_type,type,
set_Product_prod_d_c: $tType ).
thf(set_Product_prod_c_d_type,type,
set_Product_prod_c_d: $tType ).
thf(set_Product_prod_c_c_type,type,
set_Product_prod_c_c: $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_nat_type,type,
product_prod_nat_nat: $tType ).
thf(product_prod_nat_int_type,type,
product_prod_nat_int: $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(list_nat_nat_type,type,
list_nat_nat: $tType ).
thf(filter_set_nat_type,type,
filter_set_nat: $tType ).
thf(product_prod_d_nat_type,type,
product_prod_d_nat: $tType ).
thf(product_prod_d_int_type,type,
product_prod_d_int: $tType ).
thf(product_prod_c_nat_type,type,
product_prod_c_nat: $tType ).
thf(product_prod_c_int_type,type,
product_prod_c_int: $tType ).
thf(product_prod_nat_d_type,type,
product_prod_nat_d: $tType ).
thf(product_prod_nat_c_type,type,
product_prod_nat_c: $tType ).
thf(list_list_nat_type,type,
list_list_nat: $tType ).
thf(list_list_int_type,type,
list_list_int: $tType ).
thf(list_set_nat_type,type,
list_set_nat: $tType ).
thf(list_set_int_type,type,
list_set_int: $tType ).
thf(list_Code_integer_type,type,
list_Code_integer: $tType ).
thf(set_set_nat_type,type,
set_set_nat: $tType ).
thf(set_Code_integer_type,type,
set_Code_integer: $tType ).
thf(product_prod_d_d_type,type,
product_prod_d_d: $tType ).
thf(product_prod_d_c_type,type,
product_prod_d_c: $tType ).
thf(product_prod_c_d_type,type,
product_prod_c_d: $tType ).
thf(product_prod_c_c_type,type,
product_prod_c_c: $tType ).
thf(list_assn_type,type,
list_assn: $tType ).
thf(product_prod_o_o_type,type,
product_prod_o_o: $tType ).
thf(list_set_o_type,type,
list_set_o: $tType ).
thf(set_assn_type,type,
set_assn: $tType ).
thf(filter_nat_type,type,
filter_nat: $tType ).
thf(list_rat_type,type,
list_rat: $tType ).
thf(list_num_type,type,
list_num: $tType ).
thf(list_nat_type,type,
list_nat: $tType ).
thf(list_int_type,type,
list_int: $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(list_d_type,type,
list_d: $tType ).
thf(list_c_type,type,
list_c: $tType ).
thf(set_d_type,type,
set_d: $tType ).
thf(set_c_type,type,
set_c: $tType ).
thf(list_o_type,type,
list_o: $tType ).
thf(assn_type,type,
assn: $tType ).
thf(set_o_type,type,
set_o: $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(d_type,type,
d: $tType ).
thf(c_type,type,
c: $tType ).
thf(entails_decl,type,
entails: assn > assn > $o ).
thf(bot_bot_assn_decl,type,
bot_bot_assn: assn ).
thf(p_decl,type,
p: assn ).
thf(q_decl,type,
q: assn ).
thf(44,axiom,
! [A: assn,B: assn] :
( ( entails @ A @ B )
=> ( ( entails @ B @ A )
=> ( A = B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3_ent__iffI) ).
thf(152,plain,
! [A: assn,B: assn] :
( ( entails @ A @ B )
=> ( ( entails @ B @ A )
=> ( A = B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(153,plain,
! [B: assn,A: assn] :
( ~ ( entails @ A @ B )
| ~ ( entails @ B @ A )
| ( A = B ) ),
inference(cnf,[status(esa)],[152]) ).
thf(154,plain,
! [B: assn,A: assn] :
( ( A = B )
| ~ ( entails @ A @ B )
| ~ ( entails @ B @ A ) ),
inference(lifteq,[status(thm)],[153]) ).
thf(35,axiom,
! [A: assn] : ( entails @ bot_bot_assn @ A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_7_ent__false) ).
thf(134,plain,
! [A: assn] : ( entails @ bot_bot_assn @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(135,plain,
! [A: assn] : ( entails @ bot_bot_assn @ A ),
inference(cnf,[status(esa)],[134]) ).
thf(1,conjecture,
entails @ p @ q,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
thf(2,negated_conjecture,
~ ( entails @ p @ q ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(48,plain,
~ ( entails @ p @ q ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(254,plain,
! [A: assn] :
( ~ $true
| ( ( entails @ bot_bot_assn @ A )
!= ( entails @ p @ q ) ) ),
inference(paramod_ordered,[status(thm)],[135,48]) ).
thf(255,plain,
! [A: assn] :
( ( entails @ bot_bot_assn @ A )
!= ( entails @ p @ q ) ),
inference(simp,[status(thm)],[254]) ).
thf(257,plain,
! [A: assn] :
( ( p != bot_bot_assn )
| ( A != q ) ),
inference(simp,[status(thm)],[255]) ).
thf(259,plain,
p != bot_bot_assn,
inference(simp,[status(thm)],[257]) ).
thf(5658,plain,
! [B: assn,A: assn] :
( ~ ( entails @ A @ B )
| ~ ( entails @ B @ A )
| ( B != bot_bot_assn )
| ( A != p ) ),
inference(paramod_ordered,[status(thm)],[154,259]) ).
thf(5659,plain,
! [A: assn] :
( ~ ( entails @ p @ A )
| ~ ( entails @ A @ p )
| ( A != bot_bot_assn ) ),
inference(pattern_uni,[status(thm)],[5658:[bind(A,$thf( p ))]]) ).
thf(5888,plain,
( ~ ( entails @ p @ bot_bot_assn )
| ~ ( entails @ bot_bot_assn @ p ) ),
inference(simp,[status(thm)],[5659]) ).
thf(41,axiom,
entails @ p @ bot_bot_assn,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1__092_060open_062P_A_092_060Longrightarrow_062_092_060_094sub_062A_Afalse_092_060close_062) ).
thf(147,plain,
entails @ p @ bot_bot_assn,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(6343,plain,
( ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[5888,147,135]) ).
thf(6344,plain,
$false,
inference(simp,[status(thm)],[6343]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP219^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.09/0.20 % Computer : n014.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Tue Sep 29 20:18:15 UTC 2026
% 0.09/0.21 % CPUTime :
% 0.09/0.21 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
% 0.89/0.79 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 5.31/2.00 % [INFO] Parsing done (1211ms).
% 5.31/2.02 % [INFO] Running in sequential loop mode.
% 6.44/2.41 % [INFO] eprover registered as external prover.
% 6.44/2.42 % [INFO] Scanning for conjecture ...
% 7.68/2.80 % [INFO] Found a conjecture (or negated_conjecture) and 5786 axioms. Running axiom selection ...
% 7.97/2.95 % [INFO] Axiom selection finished. Selected 45 axioms (removed 5741 axioms).
% 7.97/3.01 % [INFO] Problem is higher-order (TPTP THF).
% 7.97/3.02 % [INFO] Type checking passed.
% 7.97/3.03 % [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 ...
% 37.69/9.86 % [INFO] Killing All external provers ...
% 37.69/9.87 % Time passed: 9521ms (effective reasoning time: 7836ms)
% 37.69/9.87 % 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)>
% 37.69/9.87 % Axioms used in derivation (3): fact_3_ent__iffI, fact_7_ent__false, fact_1__092_060open_062P_A_092_060Longrightarrow_062_092_060_094sub_062A_Afalse_092_060close_062
% 37.69/9.87 % No. of inferences in proof: 21
% 37.69/9.87 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 9521 ms resp. 7836 ms w/o parsing
% 38.19/9.91 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 38.19/9.91 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------