%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : CSR114+23 : TPTP v9.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.ejCWOf0xCJ true
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Oct 2 04:31:54 PM UTC 2025
% Result : Theorem 6.01s 1.49s
% Output : Refutation 6.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 3
% Syntax : Number of formulae : 26 ( 8 unt; 0 typ; 0 def)
% Number of atoms : 468 ( 0 equ; 0 cnn)
% Maximal formula atoms : 368 ( 18 avg)
% Number of connectives : 1459 ( 68 ~; 56 |; 385 &; 949 @)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 370 ( 23 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 108 ( 107 usr; 83 con; 0-3 aty)
% Number of variables : 54 ( 0 ^; 43 !; 11 ?; 54 :)
% Comments :
%------------------------------------------------------------------------------
thf(ad_type,type,
ad: $i ).
thf(spielen_1_2_type,type,
spielen_1_2: $i ).
thf(da_type,type,
da: $i ).
thf(bryan_0_type,type,
bryan_0: $i ).
thf(int0_type,type,
int0: $i ).
thf(c209_type,type,
c209: $i ).
thf(c177_type,type,
c177: $i ).
thf(temp_type,type,
temp: $i > $i > $o ).
thf(quant_c_type,type,
quant_c: $i ).
thf(jahr__1_1_type,type,
jahr__1_1: $i ).
thf(oa_type,type,
oa: $i ).
thf(adams_0_type,type,
adams_0: $i ).
thf(etype_c_type,type,
etype_c: $i ).
thf(c207_type,type,
c207: $i ).
thf(scar_type,type,
scar: $i > $i > $o ).
thf(assoc_type,type,
assoc: $i > $i > $o ).
thf(refer_c_type,type,
refer_c: $i ).
thf(fact_type,type,
fact: $i > $i > $o ).
thf(gratis_1_1_type,type,
gratis_1_1: $i ).
thf(t_type,type,
t: $i ).
thf(nfquant_type,type,
nfquant: $i ).
thf(konzert__1_1_type,type,
konzert__1_1: $i ).
thf(tour_1_1_type,type,
tour_1_1: $i ).
thf(card_type,type,
card: $i > $i > $o ).
thf(c206_type,type,
c206: $i ).
thf(mensch_1_1_type,type,
mensch_1_1: $i ).
thf(quant_type,type,
quant: $i > $i > $o ).
thf(ge_type,type,
ge: $i ).
thf(zuschauer__1_1_type,type,
zuschauer__1_1: $i ).
thf(c181_type,type,
c181: $i ).
thf(vor_type,type,
vor: $i > $i > $o ).
thf(c168_type,type,
c168: $i ).
thf(val_type,type,
val: $i > $i > $o ).
thf(int2_type,type,
int2: $i ).
thf(sort_type,type,
sort: $i > $i > $o ).
thf(me_type,type,
me: $i ).
thf(indet_type,type,
indet: $i ).
thf(gratiskonzert_1_1_type,type,
gratiskonzert_1_1: $i ).
thf(familiename_1_1_type,type,
familiename_1_1: $i ).
thf(gq_type,type,
gq: $i ).
thf(attr_type,type,
attr: $i > $i > $o ).
thf(loc_type,type,
loc: $i > $i > $o ).
thf(c202_type,type,
c202: $i ).
thf(sub_type,type,
sub: $i > $i > $o ).
thf(int500000_type,type,
int500000: $i ).
thf(refer_type,type,
refer: $i > $i > $o ).
thf(rom_0_type,type,
rom_0: $i ).
thf(na_type,type,
na: $i ).
thf(monat_1_1_type,type,
monat_1_1: $i ).
thf(c208_type,type,
c208: $i ).
thf(etype_type,type,
etype: $i > $i > $o ).
thf(c11_type,type,
c11: $i ).
thf(int7_type,type,
int7: $i ).
thf(nu_type,type,
nu: $i ).
thf(itms_type,type,
itms: $i > $i > $i > $o ).
thf(c179_type,type,
c179: $i ).
thf(l_type,type,
l: $i ).
thf(varia_type,type,
varia: $i > $i > $o ).
thf(c178_type,type,
c178: $i ).
thf(card_c_type,type,
card_c: $i ).
thf(subs_type,type,
subs: $i > $i > $o ).
thf(stadt__1_1_type,type,
stadt__1_1: $i ).
thf(in_type,type,
in: $i > $i > $o ).
thf(real_type,type,
real: $i ).
thf(bei_type,type,
bei: $i > $i > $o ).
thf(sp_type,type,
sp: $i ).
thf(tag_1_1_type,type,
tag_1_1: $i ).
thf(o_type,type,
o: $i ).
thf(con_type,type,
con: $i ).
thf(c167_type,type,
c167: $i ).
thf(c13_type,type,
c13: $i ).
thf(c175_type,type,
c175: $i ).
thf(one_type,type,
one: $i ).
thf(varia_c_type,type,
varia_c: $i ).
thf(int2006_type,type,
int2006: $i ).
thf(c176_type,type,
c176: $i ).
thf(c4_type,type,
c4: $i ).
thf(c180_type,type,
c180: $i ).
thf(attch_type,type,
attch: $i > $i > $o ).
thf(fe_type,type,
fe: $i ).
thf(c196_type,type,
c196: $i ).
thf(c185_type,type,
c185: $i ).
thf(zugucken_1_1_type,type,
zugucken_1_1: $i ).
thf(kolosseum_1_1_type,type,
kolosseum_1_1: $i ).
thf(europa_0_type,type,
europa_0: $i ).
thf(c190_type,type,
c190: $i ).
thf(abschlu__337_1_1_type,type,
abschlu__337_1_1: $i ).
thf(int31_type,type,
int31: $i ).
thf(pred_type,type,
pred: $i > $i > $o ).
thf(c205_type,type,
c205: $i ).
thf(io_type,type,
io: $i ).
thf(c203_type,type,
c203: $i ).
thf(ta_type,type,
ta: $i ).
thf(stehen_1_1_type,type,
stehen_1_1: $i ).
thf(int1_type,type,
int1: $i ).
thf(sk__8_type,type,
sk__8: $i > $i > $i ).
thf(gener_type,type,
gener: $i > $i > $o ).
thf(ctxt_type,type,
ctxt: $i > $i > $o ).
thf(c169_type,type,
c169: $i ).
thf(europatour_1_1_type,type,
europatour_1_1: $i ).
thf(d_type,type,
d: $i ).
thf(c210_type,type,
c210: $i ).
thf(agt_type,type,
agt: $i > $i > $o ).
thf(det_type,type,
det: $i ).
thf(name_1_1_type,type,
name_1_1: $i ).
thf(c8_type,type,
c8: $i ).
thf(eigenname_1_1_type,type,
eigenname_1_1: $i ).
thf(ave07_era5_synth_qa07_004_qapw_67,axiom,
( ( varia @ konzert__1_1 @ varia_c )
& ( refer @ konzert__1_1 @ refer_c )
& ( quant @ konzert__1_1 @ one )
& ( gener @ konzert__1_1 @ ge )
& ( fact @ konzert__1_1 @ real )
& ( etype @ konzert__1_1 @ int0 )
& ( card @ konzert__1_1 @ int1 )
& ( sort @ konzert__1_1 @ io )
& ( sort @ konzert__1_1 @ d )
& ( sort @ konzert__1_1 @ ad )
& ( sort @ gratis_1_1 @ gq )
& ( varia @ tour_1_1 @ varia_c )
& ( refer @ tour_1_1 @ refer_c )
& ( quant @ tour_1_1 @ one )
& ( gener @ tour_1_1 @ ge )
& ( fact @ tour_1_1 @ real )
& ( etype @ tour_1_1 @ int0 )
& ( card @ tour_1_1 @ int1 )
& ( sort @ tour_1_1 @ ad )
& ( sort @ europa_0 @ fe )
& ( varia @ europatour_1_1 @ varia_c )
& ( refer @ europatour_1_1 @ refer_c )
& ( quant @ europatour_1_1 @ one )
& ( gener @ europatour_1_1 @ ge )
& ( fact @ europatour_1_1 @ real )
& ( etype @ europatour_1_1 @ int0 )
& ( card @ europatour_1_1 @ int1 )
& ( sort @ europatour_1_1 @ ad )
& ( varia @ c8 @ con )
& ( refer @ c8 @ det )
& ( quant @ c8 @ one )
& ( gener @ c8 @ sp )
& ( fact @ c8 @ real )
& ( etype @ c8 @ int0 )
& ( card @ c8 @ int1 )
& ( sort @ c8 @ ad )
& ( varia @ abschlu__337_1_1 @ varia_c )
& ( refer @ abschlu__337_1_1 @ refer_c )
& ( quant @ abschlu__337_1_1 @ one )
& ( gener @ abschlu__337_1_1 @ ge )
& ( fact @ abschlu__337_1_1 @ real )
& ( etype @ abschlu__337_1_1 @ int0 )
& ( card @ abschlu__337_1_1 @ int1 )
& ( sort @ abschlu__337_1_1 @ ad )
& ( gener @ zugucken_1_1 @ ge )
& ( fact @ zugucken_1_1 @ real )
& ( sort @ zugucken_1_1 @ da )
& ( gener @ c210 @ sp )
& ( fact @ c210 @ real )
& ( sort @ c210 @ da )
& ( varia @ c13 @ varia_c )
& ( refer @ c13 @ det )
& ( quant @ c13 @ one )
& ( gener @ c13 @ sp )
& ( fact @ c13 @ real )
& ( etype @ c13 @ int0 )
& ( card @ c13 @ int1 )
& ( sort @ c13 @ o )
& ( sort @ rom_0 @ fe )
& ( varia @ name_1_1 @ varia_c )
& ( refer @ name_1_1 @ refer_c )
& ( quant @ name_1_1 @ one )
& ( gener @ name_1_1 @ ge )
& ( fact @ name_1_1 @ real )
& ( etype @ name_1_1 @ int0 )
& ( card @ name_1_1 @ int1 )
& ( sort @ name_1_1 @ na )
& ( varia @ stadt__1_1 @ varia_c )
& ( refer @ stadt__1_1 @ refer_c )
& ( quant @ stadt__1_1 @ one )
& ( gener @ stadt__1_1 @ ge )
& ( fact @ stadt__1_1 @ real )
& ( etype @ stadt__1_1 @ int0 )
& ( card @ stadt__1_1 @ int1 )
& ( sort @ stadt__1_1 @ io )
& ( sort @ stadt__1_1 @ d )
& ( varia @ c203 @ varia_c )
& ( refer @ c203 @ indet )
& ( quant @ c203 @ one )
& ( gener @ c203 @ sp )
& ( fact @ c203 @ real )
& ( etype @ c203 @ int0 )
& ( card @ c203 @ int1 )
& ( sort @ c203 @ na )
& ( varia @ c202 @ con )
& ( refer @ c202 @ det )
& ( quant @ c202 @ one )
& ( gener @ c202 @ sp )
& ( fact @ c202 @ real )
& ( etype @ c202 @ int0 )
& ( card @ c202 @ int1 )
& ( sort @ c202 @ io )
& ( sort @ c202 @ d )
& ( varia @ kolosseum_1_1 @ con )
& ( refer @ kolosseum_1_1 @ det )
& ( quant @ kolosseum_1_1 @ one )
& ( gener @ kolosseum_1_1 @ sp )
& ( fact @ kolosseum_1_1 @ real )
& ( etype @ kolosseum_1_1 @ int0 )
& ( card @ kolosseum_1_1 @ int1 )
& ( sort @ kolosseum_1_1 @ d )
& ( varia @ c205 @ con )
& ( refer @ c205 @ det )
& ( quant @ c205 @ one )
& ( gener @ c205 @ sp )
& ( fact @ c205 @ real )
& ( etype @ c205 @ int0 )
& ( card @ c205 @ int1 )
& ( sort @ c205 @ l )
& ( varia @ c196 @ con )
& ( refer @ c196 @ det )
& ( quant @ c196 @ one )
& ( gener @ c196 @ sp )
& ( fact @ c196 @ real )
& ( etype @ c196 @ int0 )
& ( card @ c196 @ int1 )
& ( sort @ c196 @ d )
& ( varia @ gratiskonzert_1_1 @ varia_c )
& ( refer @ gratiskonzert_1_1 @ refer_c )
& ( quant @ gratiskonzert_1_1 @ one )
& ( gener @ gratiskonzert_1_1 @ ge )
& ( fact @ gratiskonzert_1_1 @ real )
& ( etype @ gratiskonzert_1_1 @ int0 )
& ( card @ gratiskonzert_1_1 @ int1 )
& ( sort @ gratiskonzert_1_1 @ io )
& ( sort @ gratiskonzert_1_1 @ d )
& ( sort @ gratiskonzert_1_1 @ ad )
& ( varia @ c206 @ con )
& ( refer @ c206 @ det )
& ( quant @ c206 @ one )
& ( gener @ c206 @ sp )
& ( fact @ c206 @ real )
& ( etype @ c206 @ int0 )
& ( card @ c206 @ int1 )
& ( sort @ c206 @ l )
& ( varia @ c190 @ varia_c )
& ( refer @ c190 @ indet )
& ( quant @ c190 @ one )
& ( gener @ c190 @ sp )
& ( fact @ c190 @ real )
& ( etype @ c190 @ int0 )
& ( card @ c190 @ int1 )
& ( sort @ c190 @ io )
& ( sort @ c190 @ d )
& ( sort @ c190 @ ad )
& ( varia @ zuschauer__1_1 @ varia_c )
& ( refer @ zuschauer__1_1 @ refer_c )
& ( quant @ zuschauer__1_1 @ one )
& ( gener @ zuschauer__1_1 @ ge )
& ( fact @ zuschauer__1_1 @ real )
& ( etype @ zuschauer__1_1 @ int0 )
& ( card @ zuschauer__1_1 @ int1 )
& ( sort @ zuschauer__1_1 @ d )
& ( varia @ c207 @ varia_c )
& ( refer @ c207 @ indet )
& ( quant @ c207 @ one )
& ( gener @ c207 @ sp )
& ( fact @ c207 @ real )
& ( etype @ c207 @ int0 )
& ( card @ c207 @ int1 )
& ( sort @ c207 @ l )
& ( varia @ c185 @ varia_c )
& ( refer @ c185 @ indet )
& ( quant @ c185 @ nfquant )
& ( gener @ c185 @ sp )
& ( fact @ c185 @ real )
& ( etype @ c185 @ int1 )
& ( card @ c185 @ int500000 )
& ( sort @ c185 @ d )
& ( card @ c177 @ int2006 )
& ( sort @ c177 @ nu )
& ( varia @ jahr__1_1 @ varia_c )
& ( refer @ jahr__1_1 @ refer_c )
& ( quant @ jahr__1_1 @ quant_c )
& ( gener @ jahr__1_1 @ ge )
& ( fact @ jahr__1_1 @ real )
& ( etype @ jahr__1_1 @ etype_c )
& ( card @ jahr__1_1 @ card_c )
& ( sort @ jahr__1_1 @ ta )
& ( sort @ jahr__1_1 @ oa )
& ( sort @ jahr__1_1 @ me )
& ( card @ c176 @ int7 )
& ( sort @ c176 @ nu )
& ( varia @ monat_1_1 @ varia_c )
& ( refer @ monat_1_1 @ refer_c )
& ( quant @ monat_1_1 @ quant_c )
& ( gener @ monat_1_1 @ ge )
& ( fact @ monat_1_1 @ real )
& ( etype @ monat_1_1 @ etype_c )
& ( card @ monat_1_1 @ card_c )
& ( sort @ monat_1_1 @ ta )
& ( sort @ monat_1_1 @ oa )
& ( sort @ monat_1_1 @ me )
& ( card @ c175 @ int31 )
& ( sort @ c175 @ nu )
& ( varia @ tag_1_1 @ varia_c )
& ( refer @ tag_1_1 @ refer_c )
& ( quant @ tag_1_1 @ quant_c )
& ( gener @ tag_1_1 @ ge )
& ( fact @ tag_1_1 @ real )
& ( etype @ tag_1_1 @ etype_c )
& ( card @ tag_1_1 @ card_c )
& ( sort @ tag_1_1 @ ta )
& ( sort @ tag_1_1 @ oa )
& ( sort @ tag_1_1 @ me )
& ( varia @ c181 @ varia_c )
& ( refer @ c181 @ refer_c )
& ( quant @ c181 @ quant_c )
& ( gener @ c181 @ sp )
& ( fact @ c181 @ real )
& ( etype @ c181 @ etype_c )
& ( card @ c181 @ card_c )
& ( sort @ c181 @ ta )
& ( sort @ c181 @ oa )
& ( sort @ c181 @ me )
& ( varia @ c180 @ varia_c )
& ( refer @ c180 @ det )
& ( quant @ c180 @ quant_c )
& ( gener @ c180 @ sp )
& ( fact @ c180 @ real )
& ( etype @ c180 @ etype_c )
& ( card @ c180 @ card_c )
& ( sort @ c180 @ ta )
& ( sort @ c180 @ oa )
& ( sort @ c180 @ me )
& ( varia @ c179 @ varia_c )
& ( refer @ c179 @ det )
& ( quant @ c179 @ quant_c )
& ( gener @ c179 @ sp )
& ( fact @ c179 @ real )
& ( etype @ c179 @ etype_c )
& ( card @ c179 @ card_c )
& ( sort @ c179 @ ta )
& ( sort @ c179 @ oa )
& ( sort @ c179 @ me )
& ( sort @ adams_0 @ fe )
& ( varia @ familiename_1_1 @ varia_c )
& ( refer @ familiename_1_1 @ refer_c )
& ( quant @ familiename_1_1 @ one )
& ( gener @ familiename_1_1 @ ge )
& ( fact @ familiename_1_1 @ real )
& ( etype @ familiename_1_1 @ int0 )
& ( card @ familiename_1_1 @ int1 )
& ( sort @ familiename_1_1 @ na )
& ( sort @ bryan_0 @ fe )
& ( varia @ eigenname_1_1 @ varia_c )
& ( refer @ eigenname_1_1 @ refer_c )
& ( quant @ eigenname_1_1 @ one )
& ( gener @ eigenname_1_1 @ ge )
& ( fact @ eigenname_1_1 @ real )
& ( etype @ eigenname_1_1 @ int0 )
& ( card @ eigenname_1_1 @ int1 )
& ( sort @ eigenname_1_1 @ na )
& ( varia @ mensch_1_1 @ varia_c )
& ( refer @ mensch_1_1 @ refer_c )
& ( quant @ mensch_1_1 @ one )
& ( gener @ mensch_1_1 @ ge )
& ( fact @ mensch_1_1 @ real )
& ( etype @ mensch_1_1 @ int0 )
& ( card @ mensch_1_1 @ int1 )
& ( sort @ mensch_1_1 @ d )
& ( varia @ c169 @ varia_c )
& ( refer @ c169 @ indet )
& ( quant @ c169 @ one )
& ( gener @ c169 @ sp )
& ( fact @ c169 @ real )
& ( etype @ c169 @ int0 )
& ( card @ c169 @ int1 )
& ( sort @ c169 @ na )
& ( varia @ c168 @ varia_c )
& ( refer @ c168 @ indet )
& ( quant @ c168 @ one )
& ( gener @ c168 @ sp )
& ( fact @ c168 @ real )
& ( etype @ c168 @ int0 )
& ( card @ c168 @ int1 )
& ( sort @ c168 @ na )
& ( varia @ c167 @ con )
& ( refer @ c167 @ det )
& ( quant @ c167 @ one )
& ( gener @ c167 @ sp )
& ( fact @ c167 @ real )
& ( etype @ c167 @ int0 )
& ( card @ c167 @ int1 )
& ( sort @ c167 @ d )
& ( varia @ c178 @ con )
& ( refer @ c178 @ det )
& ( quant @ c178 @ one )
& ( gener @ c178 @ sp )
& ( fact @ c178 @ real )
& ( etype @ c178 @ int0 )
& ( card @ c178 @ int1 )
& ( sort @ c178 @ t )
& ( gener @ spielen_1_2 @ ge )
& ( fact @ spielen_1_2 @ real )
& ( sort @ spielen_1_2 @ da )
& ( varia @ c208 @ varia_c )
& ( refer @ c208 @ refer_c )
& ( quant @ c208 @ nfquant )
& ( gener @ c208 @ sp )
& ( fact @ c208 @ real )
& ( etype @ c208 @ int1 )
& ( card @ c208 @ int500000 )
& ( sort @ c208 @ l )
& ( varia @ c4 @ varia_c )
& ( refer @ c4 @ det )
& ( quant @ c4 @ one )
& ( gener @ c4 @ sp )
& ( fact @ c4 @ real )
& ( etype @ c4 @ int0 )
& ( card @ c4 @ int1 )
& ( sort @ c4 @ ad )
& ( varia @ c209 @ varia_c )
& ( refer @ c209 @ det )
& ( quant @ c209 @ nfquant )
& ( gener @ c209 @ sp )
& ( fact @ c209 @ real )
& ( etype @ c209 @ int1 )
& ( card @ c209 @ int2 )
& ( sort @ c209 @ o )
& ( gener @ c11 @ sp )
& ( fact @ c11 @ real )
& ( sort @ c11 @ da )
& ( sub @ gratiskonzert_1_1 @ konzert__1_1 )
& ( assoc @ gratiskonzert_1_1 @ gratis_1_1 )
& ( subs @ europatour_1_1 @ tour_1_1 )
& ( assoc @ europatour_1_1 @ europa_0 )
& ( subs @ c8 @ europatour_1_1 )
& ( attch @ c8 @ c4 )
& ( subs @ c4 @ abschlu__337_1_1 )
& ( subs @ c210 @ zugucken_1_1 )
& ( agt @ c210 @ c185 )
& ( itms @ c209 @ c13 @ c167 )
& ( vor @ c208 @ c185 )
& ( bei @ c207 @ c190 )
& ( vor @ c206 @ c196 )
& ( in @ c205 @ c202 )
& ( val @ c203 @ rom_0 )
& ( sub @ c203 @ name_1_1 )
& ( sub @ c202 @ stadt__1_1 )
& ( attr @ c202 @ c203 )
& ( sub @ c196 @ kolosseum_1_1 )
& ( loc @ c196 @ c205 )
& ( sub @ c190 @ gratiskonzert_1_1 )
& ( loc @ c190 @ c206 )
& ( pred @ c185 @ zuschauer__1_1 )
& ( loc @ c185 @ c207 )
& ( val @ c181 @ c177 )
& ( sub @ c181 @ jahr__1_1 )
& ( val @ c180 @ c176 )
& ( sub @ c180 @ monat_1_1 )
& ( val @ c179 @ c175 )
& ( sub @ c179 @ tag_1_1 )
& ( attr @ c178 @ c181 )
& ( attr @ c178 @ c180 )
& ( attr @ c178 @ c179 )
& ( val @ c169 @ adams_0 )
& ( sub @ c169 @ familiename_1_1 )
& ( val @ c168 @ bryan_0 )
& ( sub @ c168 @ eigenname_1_1 )
& ( sub @ c167 @ mensch_1_1 )
& ( attr @ c167 @ c169 )
& ( attr @ c167 @ c168 )
& ( temp @ c11 @ c178 )
& ( subs @ c11 @ spielen_1_2 )
& ( loc @ c11 @ c208 )
& ( ctxt @ c11 @ c4 )
& ( agt @ c11 @ c209 ) ) ).
thf(zip_derived_cl366,plain,
sub @ c202 @ stadt__1_1,
inference(cnf,[status(esa)],[ave07_era5_synth_qa07_004_qapw_67]) ).
thf(zip_derived_cl369,plain,
loc @ c196 @ c205,
inference(cnf,[status(esa)],[ave07_era5_synth_qa07_004_qapw_67]) ).
thf(zip_derived_cl368,plain,
sub @ c196 @ kolosseum_1_1,
inference(cnf,[status(esa)],[ave07_era5_synth_qa07_004_qapw_67]) ).
thf(loc__stehen_1_1_loc,axiom,
! [X0: $i,X1: $i] :
( ( loc @ X0 @ X1 )
=> ? [X2: $i] :
( ( subs @ X2 @ stehen_1_1 )
& ( scar @ X2 @ X0 )
& ( loc @ X2 @ X1 ) ) ) ).
thf(zip_derived_cl23,plain,
! [X0: $i,X1: $i] :
( ( scar @ ( sk__8 @ X0 @ X1 ) @ X1 )
| ~ ( loc @ X1 @ X0 ) ),
inference(cnf,[status(esa)],[loc__stehen_1_1_loc]) ).
thf(zip_derived_cl24,plain,
! [X0: $i,X1: $i] :
( ( loc @ ( sk__8 @ X0 @ X1 ) @ X0 )
| ~ ( loc @ X1 @ X0 ) ),
inference(cnf,[status(esa)],[loc__stehen_1_1_loc]) ).
thf(zip_derived_cl22,plain,
! [X0: $i,X1: $i] :
( ( subs @ ( sk__8 @ X0 @ X1 ) @ stehen_1_1 )
| ~ ( loc @ X1 @ X0 ) ),
inference(cnf,[status(esa)],[loc__stehen_1_1_loc]) ).
thf(zip_derived_cl364,plain,
val @ c203 @ rom_0,
inference(cnf,[status(esa)],[ave07_era5_synth_qa07_004_qapw_67]) ).
thf(synth_qa07_004_qapw_67,conjecture,
? [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( val @ X1 @ rom_0 )
& ( subs @ X4 @ stehen_1_1 )
& ( sub @ X3 @ kolosseum_1_1 )
& ( sub @ X0 @ stadt__1_1 )
& ( sub @ X1 @ name_1_1 )
& ( scar @ X4 @ X3 )
& ( loc @ X4 @ X2 )
& ( attr @ X0 @ X1 )
& ( in @ X2 @ X0 ) ) ).
thf(zf_stmt_0,negated_conjecture,
~ ? [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( val @ X1 @ rom_0 )
& ( subs @ X4 @ stehen_1_1 )
& ( sub @ X3 @ kolosseum_1_1 )
& ( sub @ X0 @ stadt__1_1 )
& ( sub @ X1 @ name_1_1 )
& ( scar @ X4 @ X3 )
& ( loc @ X4 @ X2 )
& ( attr @ X0 @ X1 )
& ( in @ X2 @ X0 ) ),
inference('cnf.neg',[status(esa)],[synth_qa07_004_qapw_67]) ).
thf(zip_derived_cl395,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ~ ( val @ X0 @ rom_0 )
| ~ ( sub @ X1 @ kolosseum_1_1 )
| ~ ( sub @ X2 @ stadt__1_1 )
| ~ ( sub @ X0 @ name_1_1 )
| ~ ( attr @ X2 @ X0 )
| ~ ( in @ X3 @ X2 )
| ~ ( loc @ X4 @ X3 )
| ~ ( scar @ X4 @ X1 )
| ~ ( subs @ X4 @ stehen_1_1 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl720,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ( subs @ X0 @ stehen_1_1 )
| ~ ( scar @ X0 @ X1 )
| ~ ( loc @ X0 @ X2 )
| ~ ( in @ X2 @ X3 )
| ~ ( attr @ X3 @ c203 )
| ~ ( sub @ c203 @ name_1_1 )
| ~ ( sub @ X3 @ stadt__1_1 )
| ~ ( sub @ X1 @ kolosseum_1_1 ) ),
inference('sup-',[status(thm)],[zip_derived_cl364,zip_derived_cl395]) ).
thf(zip_derived_cl365,plain,
sub @ c203 @ name_1_1,
inference(cnf,[status(esa)],[ave07_era5_synth_qa07_004_qapw_67]) ).
thf(zip_derived_cl721,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ( subs @ X0 @ stehen_1_1 )
| ~ ( scar @ X0 @ X1 )
| ~ ( loc @ X0 @ X2 )
| ~ ( in @ X2 @ X3 )
| ~ ( attr @ X3 @ c203 )
| ~ ( sub @ X3 @ stadt__1_1 )
| ~ ( sub @ X1 @ kolosseum_1_1 ) ),
inference(demod,[status(thm)],[zip_derived_cl720,zip_derived_cl365]) ).
thf(zip_derived_cl736,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ~ ( loc @ X0 @ X1 )
| ~ ( sub @ X2 @ kolosseum_1_1 )
| ~ ( sub @ X3 @ stadt__1_1 )
| ~ ( attr @ X3 @ c203 )
| ~ ( in @ X4 @ X3 )
| ~ ( loc @ ( sk__8 @ X1 @ X0 ) @ X4 )
| ~ ( scar @ ( sk__8 @ X1 @ X0 ) @ X2 ) ),
inference('sup-',[status(thm)],[zip_derived_cl22,zip_derived_cl721]) ).
thf(zip_derived_cl779,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ( loc @ X1 @ X0 )
| ~ ( scar @ ( sk__8 @ X0 @ X1 ) @ X2 )
| ~ ( in @ X0 @ X3 )
| ~ ( attr @ X3 @ c203 )
| ~ ( sub @ X3 @ stadt__1_1 )
| ~ ( sub @ X2 @ kolosseum_1_1 )
| ~ ( loc @ X1 @ X0 ) ),
inference('sup-',[status(thm)],[zip_derived_cl24,zip_derived_cl736]) ).
thf(zip_derived_cl780,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ( sub @ X2 @ kolosseum_1_1 )
| ~ ( sub @ X3 @ stadt__1_1 )
| ~ ( attr @ X3 @ c203 )
| ~ ( in @ X0 @ X3 )
| ~ ( scar @ ( sk__8 @ X0 @ X1 ) @ X2 )
| ~ ( loc @ X1 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl779]) ).
thf(zip_derived_cl950,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( loc @ X0 @ X1 )
| ~ ( loc @ X0 @ X1 )
| ~ ( in @ X1 @ X2 )
| ~ ( attr @ X2 @ c203 )
| ~ ( sub @ X2 @ stadt__1_1 )
| ~ ( sub @ X0 @ kolosseum_1_1 ) ),
inference('sup-',[status(thm)],[zip_derived_cl23,zip_derived_cl780]) ).
thf(zip_derived_cl951,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( sub @ X0 @ kolosseum_1_1 )
| ~ ( sub @ X2 @ stadt__1_1 )
| ~ ( attr @ X2 @ c203 )
| ~ ( in @ X1 @ X2 )
| ~ ( loc @ X0 @ X1 ) ),
inference(simplify,[status(thm)],[zip_derived_cl950]) ).
thf(zip_derived_cl953,plain,
! [X0: $i,X1: $i] :
( ~ ( loc @ c196 @ X0 )
| ~ ( in @ X0 @ X1 )
| ~ ( attr @ X1 @ c203 )
| ~ ( sub @ X1 @ stadt__1_1 ) ),
inference('sup-',[status(thm)],[zip_derived_cl368,zip_derived_cl951]) ).
thf(zip_derived_cl957,plain,
! [X0: $i] :
( ~ ( sub @ X0 @ stadt__1_1 )
| ~ ( attr @ X0 @ c203 )
| ~ ( in @ c205 @ X0 ) ),
inference('sup-',[status(thm)],[zip_derived_cl369,zip_derived_cl953]) ).
thf(zip_derived_cl960,plain,
( ~ ( in @ c205 @ c202 )
| ~ ( attr @ c202 @ c203 ) ),
inference('sup-',[status(thm)],[zip_derived_cl366,zip_derived_cl957]) ).
thf(zip_derived_cl363,plain,
in @ c205 @ c202,
inference(cnf,[status(esa)],[ave07_era5_synth_qa07_004_qapw_67]) ).
thf(zip_derived_cl367,plain,
attr @ c202 @ c203,
inference(cnf,[status(esa)],[ave07_era5_synth_qa07_004_qapw_67]) ).
thf(zip_derived_cl963,plain,
$false,
inference(demod,[status(thm)],[zip_derived_cl960,zip_derived_cl363,zip_derived_cl367]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.15 % Problem : CSR114+23 : TPTP v9.2.0. Released v4.0.0.
% 0.07/0.16 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.ejCWOf0xCJ true
% 0.12/0.37 % Computer : n005.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8042.1875MB
% 0.12/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Wed Oct 1 14:47:24 EDT 2025
% 0.12/0.37 % CPUTime :
% 0.12/0.37 % Running portfolio for 300 s
% 0.12/0.37 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.37 % Number of cores: 8
% 0.12/0.37 % Python version: Python 3.6.8
% 0.12/0.37 % Running in FO mode
% 0.55/0.67 % Total configuration time : 435
% 0.55/0.67 % Estimated wc time : 1092
% 0.55/0.67 % Estimated cpu time (7 cpus) : 156.0
% 0.57/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.57/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.57/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.57/0.78 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.57/0.79 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.57/0.79 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.57/0.79 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 6.01/1.49 % Solved by fo/fo4.sh.
% 6.01/1.49 % done 553 iterations in 0.671s
% 6.01/1.49 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 6.01/1.49 % SZS output start Refutation
% See solution above
% 6.01/1.49
% 6.01/1.49
% 6.01/1.49 % Terminating...
% 6.69/1.58 % Runner terminated.
% 6.69/1.60 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------