%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : CSR115+90 : TPTP v9.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.ym7XDgGbFR true
% Computer : n013.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:32:09 PM UTC 2025
% Result : Theorem 42.06s 9.20s
% Output : Refutation 42.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 4
% Syntax : Number of formulae : 33 ( 9 unt; 0 typ; 0 def)
% Number of atoms : 414 ( 0 equ; 0 cnn)
% Maximal formula atoms : 310 ( 12 avg)
% Number of connectives : 1310 ( 69 ~; 45 |; 330 &; 860 @)
% ( 0 <=>; 2 =>; 4 <=; 0 <~>)
% Maximal formula depth : 312 ( 18 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 111 ( 110 usr; 82 con; 0-14 aty)
% Number of variables : 92 ( 0 ^; 74 !; 18 ?; 92 :)
% Comments :
%------------------------------------------------------------------------------
thf(ad_type,type,
ad: $i ).
thf(c37341_type,type,
c37341: $i ).
thf(bundeswehr_1_1_type,type,
bundeswehr_1_1: $i ).
thf(da_type,type,
da: $i ).
thf(c37246_type,type,
c37246: $i ).
thf(int0_type,type,
int0: $i ).
thf(boxer_2_1_type,type,
boxer_2_1: $i ).
thf(fahrzeug__1_1_type,type,
fahrzeug__1_1: $i ).
thf(quant_c_type,type,
quant_c: $i ).
thf(c37402_type,type,
c37402: $i ).
thf(arg1_type,type,
arg1: $i > $i > $o ).
thf(n__374rnberg_0_type,type,
n__374rnberg_0: $i ).
thf(etype_c_type,type,
etype_c: $i ).
thf(c37291_type,type,
c37291: $i ).
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(c37345_type,type,
c37345: $i ).
thf(rprs_0_type,type,
rprs_0: $i ).
thf(cons_type,type,
cons: $i > $i > $i ).
thf(prop_type,type,
prop: $i > $i > $o ).
thf(card_type,type,
card: $i > $i > $o ).
thf(c37298_type,type,
c37298: $i ).
thf(quant_type,type,
quant: $i > $i > $o ).
thf(ge_type,type,
ge: $i ).
thf(ackerbautreibend_1_1_type,type,
ackerbautreibend_1_1: $i ).
thf(faun_1_1_type,type,
faun_1_1: $i ).
thf(val_type,type,
val: $i > $i > $o ).
thf(sort_type,type,
sort: $i > $i > $o ).
thf(arg2_type,type,
arg2: $i > $i > $o ).
thf(me_type,type,
me: $i ).
thf(indet_type,type,
indet: $i ).
thf(lypsoid_1_1_type,type,
lypsoid_1_1: $i ).
thf(sk__57_type,type,
sk__57: $i > $i > $i ).
thf(nfquant_type,type,
nfquant: $i ).
thf(gq_type,type,
gq: $i ).
thf(attr_type,type,
attr: $i > $i > $o ).
thf(int26_type,type,
int26: $i ).
thf(sub_0_type,type,
sub_0: $i ).
thf(co_type,type,
co: $i ).
thf(last_1_1_type,type,
last_1_1: $i ).
thf(sub_type,type,
sub: $i > $i > $o ).
thf(int1_type,type,
int1: $i ).
thf(c37356_type,type,
c37356: $i ).
thf(refer_type,type,
refer: $i > $i > $o ).
thf(na_type,type,
na: $i ).
thf(c37331_type,type,
c37331: $i ).
thf(hsit_type,type,
hsit: $i > $i > $o ).
thf(mcont_type,type,
mcont: $i > $i > $o ).
thf(bundeswehrausf__374hrung_1_1_type,type,
bundeswehrausf__374hrung_1_1: $i ).
thf(etype_type,type,
etype: $i > $i > $o ).
thf(boxermotor_1_1_type,type,
boxermotor_1_1: $i ).
thf(x_constant_type,type,
x_constant: $i ).
thf(nu_type,type,
nu: $i ).
thf(int750_type,type,
int750: $i ).
thf(tupl_p14_type,type,
tupl_p14: $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $o ).
thf(sk__54_type,type,
sk__54: $i > $i > $i > $i ).
thf(c37268_type,type,
c37268: $i ).
thf(kilo__1_1_type,type,
kilo__1_1: $i ).
thf(c37339_type,type,
c37339: $i ).
thf(pferdest__344rke_1_1_type,type,
pferdest__344rke_1_1: $i ).
thf(varia_type,type,
varia: $i > $i > $o ).
thf(ausf__374hrung_1_1_type,type,
ausf__374hrung_1_1: $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(real_type,type,
real: $i ).
thf(sp_type,type,
sp: $i ).
thf(c37229_type,type,
c37229: $i ).
thf(gener_c_type,type,
gener_c: $i ).
thf(c37233_type,type,
c37233: $i ).
thf(c37359_type,type,
c37359: $i ).
thf(o_type,type,
o: $i ).
thf(con_type,type,
con: $i ).
thf(aq_type,type,
aq: $i ).
thf(quant_p3_type,type,
quant_p3: $i > $i > $i > $o ).
thf(c37238_type,type,
c37238: $i ).
thf(tq_type,type,
tq: $i ).
thf(einsatz_1_1_type,type,
einsatz_1_1: $i ).
thf(one_type,type,
one: $i ).
thf(c37313_type,type,
c37313: $i ).
thf(varia_c_type,type,
varia_c: $i ).
thf(chsp2_type,type,
chsp2: $i > $i > $o ).
thf(c37274_type,type,
c37274: $i ).
thf(motor__1_1_type,type,
motor__1_1: $i ).
thf(c37272_type,type,
c37272: $i ).
thf(attch_type,type,
attch: $i > $i > $o ).
thf(obj_type,type,
obj: $i > $i > $o ).
thf(mult_type,type,
mult: $i ).
thf(fe_type,type,
fe: $i ).
thf(n22x12_1_1_type,type,
n22x12_1_1: $i ).
thf(m_type,type,
m: $i ).
thf(c37284_type,type,
c37284: $i ).
thf(pmod_type,type,
pmod: $i > $i > $i > $o ).
thf(bezeichnen_1_1_type,type,
bezeichnen_1_1: $i ).
thf(reifen__1_1_type,type,
reifen__1_1: $i ).
thf(pred_type,type,
pred: $i > $i > $o ).
thf(io_type,type,
io: $i ).
thf(drosseln_1_1_type,type,
drosseln_1_1: $i ).
thf(ent_type,type,
ent: $i ).
thf(gener_type,type,
gener: $i > $i > $o ).
thf(nil_type,type,
nil: $i ).
thf(c37245_type,type,
c37245: $i ).
thf(d_type,type,
d: $i ).
thf(det_type,type,
det: $i ).
thf(c37361_type,type,
c37361: $i ).
thf(name_1_1_type,type,
name_1_1: $i ).
thf(bmw_1_1_type,type,
bmw_1_1: $i ).
thf(int4_type,type,
int4: $i ).
thf(subr_type,type,
subr: $i > $i > $o ).
thf(ave07_era5_synth_qa07_007_mira_wp_514,axiom,
( ( gener @ drosseln_1_1 @ ge )
& ( fact @ drosseln_1_1 @ real )
& ( sort @ drosseln_1_1 @ da )
& ( varia @ c37313 @ varia_c )
& ( refer @ c37313 @ refer_c )
& ( quant @ c37313 @ one )
& ( gener @ c37313 @ gener_c )
& ( fact @ c37313 @ real )
& ( etype @ c37313 @ int0 )
& ( card @ c37313 @ int1 )
& ( sort @ c37313 @ o )
& ( varia @ c37233 @ varia_c )
& ( refer @ c37233 @ det )
& ( quant @ c37233 @ one )
& ( gener @ c37233 @ sp )
& ( fact @ c37233 @ real )
& ( etype @ c37233 @ int0 )
& ( card @ c37233 @ int1 )
& ( sort @ c37233 @ o )
& ( varia @ c37402 @ varia_c )
& ( refer @ c37402 @ refer_c )
& ( quant @ c37402 @ quant_c )
& ( gener @ c37402 @ gener_c )
& ( fact @ c37402 @ real )
& ( etype @ c37402 @ etype_c )
& ( card @ c37402 @ card_c )
& ( sort @ c37402 @ ent )
& ( gener @ kilo__1_1 @ ge )
& ( sort @ kilo__1_1 @ me )
& ( card @ c37356 @ int750 )
& ( sort @ c37356 @ nu )
& ( varia @ c37361 @ con )
& ( refer @ c37361 @ refer_c )
& ( quant @ c37361 @ quant_c )
& ( gener @ c37361 @ gener_c )
& ( fact @ c37361 @ real )
& ( etype @ c37361 @ etype_c )
& ( card @ c37361 @ card_c )
& ( sort @ c37361 @ m )
& ( sort @ c37361 @ co )
& ( varia @ last_1_1 @ varia_c )
& ( refer @ last_1_1 @ refer_c )
& ( quant @ last_1_1 @ one )
& ( gener @ last_1_1 @ ge )
& ( fact @ last_1_1 @ real )
& ( etype @ last_1_1 @ int0 )
& ( card @ last_1_1 @ int1 )
& ( sort @ last_1_1 @ io )
& ( varia @ c37359 @ varia_c )
& ( refer @ c37359 @ refer_c )
& ( quant @ c37359 @ one )
& ( gener @ c37359 @ gener_c )
& ( fact @ c37359 @ real )
& ( etype @ c37359 @ int0 )
& ( card @ c37359 @ int1 )
& ( sort @ c37359 @ io )
& ( varia @ c37345 @ varia_c )
& ( refer @ c37345 @ refer_c )
& ( quant @ c37345 @ one )
& ( gener @ c37345 @ gener_c )
& ( fact @ c37345 @ real )
& ( etype @ c37345 @ int0 )
& ( card @ c37345 @ int1 )
& ( sort @ c37345 @ d )
& ( varia @ bmw_1_1 @ varia_c )
& ( refer @ bmw_1_1 @ refer_c )
& ( quant @ bmw_1_1 @ one )
& ( gener @ bmw_1_1 @ ge )
& ( fact @ bmw_1_1 @ real )
& ( etype @ bmw_1_1 @ int0 )
& ( card @ bmw_1_1 @ int1 )
& ( sort @ bmw_1_1 @ d )
& ( sort @ c37229 @ tq )
& ( varia @ c37341 @ varia_c )
& ( refer @ c37341 @ refer_c )
& ( quant @ c37341 @ one )
& ( gener @ c37341 @ gener_c )
& ( fact @ c37341 @ real )
& ( etype @ c37341 @ int0 )
& ( card @ c37341 @ int1 )
& ( sort @ c37341 @ d )
& ( gener @ pferdest__344rke_1_1 @ ge )
& ( sort @ pferdest__344rke_1_1 @ me )
& ( card @ c37331 @ int26 )
& ( sort @ c37331 @ nu )
& ( varia @ c37339 @ con )
& ( refer @ c37339 @ refer_c )
& ( quant @ c37339 @ quant_c )
& ( gener @ c37339 @ gener_c )
& ( fact @ c37339 @ real )
& ( etype @ c37339 @ etype_c )
& ( card @ c37339 @ card_c )
& ( sort @ c37339 @ m )
& ( sort @ c37339 @ co )
& ( sort @ n22x12_1_1 @ gq )
& ( varia @ lypsoid_1_1 @ varia_c )
& ( refer @ lypsoid_1_1 @ refer_c )
& ( quant @ lypsoid_1_1 @ one )
& ( gener @ lypsoid_1_1 @ ge )
& ( fact @ lypsoid_1_1 @ real )
& ( etype @ lypsoid_1_1 @ int0 )
& ( card @ lypsoid_1_1 @ int1 )
& ( sort @ lypsoid_1_1 @ o )
& ( varia @ c37298 @ varia_c )
& ( refer @ c37298 @ refer_c )
& ( quant @ c37298 @ mult )
& ( gener @ c37298 @ gener_c )
& ( fact @ c37298 @ real )
& ( etype @ c37298 @ int1 )
& ( card @ c37298 @ ( cons @ x_constant @ ( cons @ int1 @ nil ) ) )
& ( sort @ c37298 @ o )
& ( varia @ reifen__1_1 @ varia_c )
& ( refer @ reifen__1_1 @ refer_c )
& ( quant @ reifen__1_1 @ one )
& ( gener @ reifen__1_1 @ ge )
& ( fact @ reifen__1_1 @ real )
& ( etype @ reifen__1_1 @ int0 )
& ( card @ reifen__1_1 @ int1 )
& ( sort @ reifen__1_1 @ d )
& ( varia @ c37291 @ varia_c )
& ( refer @ c37291 @ det )
& ( quant @ c37291 @ nfquant )
& ( gener @ c37291 @ sp )
& ( fact @ c37291 @ real )
& ( etype @ c37291 @ int1 )
& ( card @ c37291 @ int4 )
& ( sort @ c37291 @ d )
& ( varia @ c37284 @ con )
& ( refer @ c37284 @ det )
& ( quant @ c37284 @ one )
& ( gener @ c37284 @ sp )
& ( fact @ c37284 @ real )
& ( etype @ c37284 @ int0 )
& ( card @ c37284 @ int1 )
& ( sort @ c37284 @ io )
& ( sort @ c37284 @ d )
& ( sort @ c37284 @ ad )
& ( varia @ fahrzeug__1_1 @ varia_c )
& ( refer @ fahrzeug__1_1 @ refer_c )
& ( quant @ fahrzeug__1_1 @ one )
& ( gener @ fahrzeug__1_1 @ ge )
& ( fact @ fahrzeug__1_1 @ real )
& ( etype @ fahrzeug__1_1 @ int0 )
& ( card @ fahrzeug__1_1 @ int1 )
& ( sort @ fahrzeug__1_1 @ d )
& ( varia @ c37274 @ varia_c )
& ( refer @ c37274 @ refer_c )
& ( quant @ c37274 @ one )
& ( gener @ c37274 @ gener_c )
& ( fact @ c37274 @ real )
& ( etype @ c37274 @ int0 )
& ( card @ c37274 @ int1 )
& ( sort @ c37274 @ d )
& ( varia @ einsatz_1_1 @ varia_c )
& ( refer @ einsatz_1_1 @ refer_c )
& ( quant @ einsatz_1_1 @ one )
& ( gener @ einsatz_1_1 @ ge )
& ( fact @ einsatz_1_1 @ real )
& ( etype @ einsatz_1_1 @ int0 )
& ( card @ einsatz_1_1 @ int1 )
& ( sort @ einsatz_1_1 @ io )
& ( sort @ einsatz_1_1 @ ad )
& ( sort @ ackerbautreibend_1_1 @ aq )
& ( varia @ c37272 @ varia_c )
& ( refer @ c37272 @ refer_c )
& ( quant @ c37272 @ one )
& ( gener @ c37272 @ ge )
& ( fact @ c37272 @ real )
& ( etype @ c37272 @ int0 )
& ( card @ c37272 @ int1 )
& ( sort @ c37272 @ io )
& ( sort @ c37272 @ ad )
& ( varia @ c37268 @ con )
& ( refer @ c37268 @ det )
& ( quant @ c37268 @ one )
& ( gener @ c37268 @ sp )
& ( fact @ c37268 @ real )
& ( etype @ c37268 @ int0 )
& ( card @ c37268 @ int1 )
& ( sort @ c37268 @ io )
& ( sort @ c37268 @ ad )
& ( sort @ n__374rnberg_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 @ c37246 @ varia_c )
& ( refer @ c37246 @ indet )
& ( quant @ c37246 @ one )
& ( gener @ c37246 @ sp )
& ( fact @ c37246 @ real )
& ( etype @ c37246 @ int0 )
& ( card @ c37246 @ int1 )
& ( sort @ c37246 @ na )
& ( varia @ c37245 @ con )
& ( refer @ c37245 @ det )
& ( quant @ c37245 @ one )
& ( gener @ c37245 @ sp )
& ( fact @ c37245 @ real )
& ( etype @ c37245 @ int0 )
& ( card @ c37245 @ int1 )
& ( sort @ c37245 @ io )
& ( sort @ c37245 @ d )
& ( varia @ faun_1_1 @ varia_c )
& ( refer @ faun_1_1 @ refer_c )
& ( quant @ faun_1_1 @ one )
& ( gener @ faun_1_1 @ ge )
& ( fact @ faun_1_1 @ real )
& ( etype @ faun_1_1 @ int0 )
& ( card @ faun_1_1 @ int1 )
& ( sort @ faun_1_1 @ o )
& ( varia @ c37238 @ varia_c )
& ( refer @ c37238 @ refer_c )
& ( quant @ c37238 @ one )
& ( gener @ c37238 @ gener_c )
& ( fact @ c37238 @ real )
& ( etype @ c37238 @ int0 )
& ( card @ c37238 @ int1 )
& ( sort @ c37238 @ o )
& ( varia @ ausf__374hrung_1_1 @ varia_c )
& ( refer @ ausf__374hrung_1_1 @ refer_c )
& ( quant @ ausf__374hrung_1_1 @ one )
& ( gener @ ausf__374hrung_1_1 @ ge )
& ( fact @ ausf__374hrung_1_1 @ real )
& ( etype @ ausf__374hrung_1_1 @ int0 )
& ( card @ ausf__374hrung_1_1 @ int1 )
& ( sort @ ausf__374hrung_1_1 @ io )
& ( sort @ ausf__374hrung_1_1 @ d )
& ( sort @ ausf__374hrung_1_1 @ ad )
& ( varia @ bundeswehr_1_1 @ varia_c )
& ( refer @ bundeswehr_1_1 @ refer_c )
& ( quant @ bundeswehr_1_1 @ quant_c )
& ( gener @ bundeswehr_1_1 @ ge )
& ( fact @ bundeswehr_1_1 @ real )
& ( etype @ bundeswehr_1_1 @ int1 )
& ( card @ bundeswehr_1_1 @ card_c )
& ( sort @ bundeswehr_1_1 @ io )
& ( sort @ bundeswehr_1_1 @ d )
& ( varia @ bundeswehrausf__374hrung_1_1 @ varia_c )
& ( refer @ bundeswehrausf__374hrung_1_1 @ refer_c )
& ( quant @ bundeswehrausf__374hrung_1_1 @ one )
& ( gener @ bundeswehrausf__374hrung_1_1 @ ge )
& ( fact @ bundeswehrausf__374hrung_1_1 @ real )
& ( etype @ bundeswehrausf__374hrung_1_1 @ int0 )
& ( card @ bundeswehrausf__374hrung_1_1 @ int1 )
& ( sort @ bundeswehrausf__374hrung_1_1 @ io )
& ( sort @ bundeswehrausf__374hrung_1_1 @ d )
& ( sort @ bundeswehrausf__374hrung_1_1 @ ad )
& ( varia @ motor__1_1 @ varia_c )
& ( refer @ motor__1_1 @ refer_c )
& ( quant @ motor__1_1 @ one )
& ( gener @ motor__1_1 @ ge )
& ( fact @ motor__1_1 @ real )
& ( etype @ motor__1_1 @ int0 )
& ( card @ motor__1_1 @ int1 )
& ( sort @ motor__1_1 @ d )
& ( varia @ boxer_2_1 @ varia_c )
& ( refer @ boxer_2_1 @ refer_c )
& ( quant @ boxer_2_1 @ one )
& ( gener @ boxer_2_1 @ ge )
& ( fact @ boxer_2_1 @ real )
& ( etype @ boxer_2_1 @ int0 )
& ( card @ boxer_2_1 @ int1 )
& ( sort @ boxer_2_1 @ d )
& ( varia @ boxermotor_1_1 @ varia_c )
& ( refer @ boxermotor_1_1 @ refer_c )
& ( quant @ boxermotor_1_1 @ one )
& ( gener @ boxermotor_1_1 @ ge )
& ( fact @ boxermotor_1_1 @ real )
& ( etype @ boxermotor_1_1 @ int0 )
& ( card @ boxermotor_1_1 @ int1 )
& ( sort @ boxermotor_1_1 @ d )
& ( chsp2 @ drosseln_1_1 @ c37229 )
& ( tupl_p14 @ c37402 @ c37233 @ c37238 @ c37245 @ c37268 @ c37274 @ c37284 @ c37291 @ c37313 @ c37339 @ c37341 @ c37345 @ c37361 @ c37359 )
& ( quant_p3 @ c37361 @ c37356 @ kilo__1_1 )
& ( sub @ c37359 @ last_1_1 )
& ( sub @ c37345 @ boxermotor_1_1 )
& ( sub @ c37341 @ bmw_1_1 )
& ( prop @ c37341 @ c37229 )
& ( quant_p3 @ c37339 @ c37331 @ pferdest__344rke_1_1 )
& ( prop @ c37298 @ n22x12_1_1 )
& ( pred @ c37298 @ lypsoid_1_1 )
& ( attch @ c37298 @ c37291 )
& ( pred @ c37291 @ reifen__1_1 )
& ( sub @ c37284 @ bundeswehrausf__374hrung_1_1 )
& ( sub @ c37274 @ fahrzeug__1_1 )
& ( pmod @ c37272 @ ackerbautreibend_1_1 @ einsatz_1_1 )
& ( sub @ c37268 @ c37272 )
& ( val @ c37246 @ n__374rnberg_0 )
& ( sub @ c37246 @ name_1_1 )
& ( sub @ c37245 @ stadt__1_1 )
& ( attr @ c37245 @ c37246 )
& ( sub @ c37238 @ faun_1_1 )
& ( sub @ bundeswehrausf__374hrung_1_1 @ ausf__374hrung_1_1 )
& ( assoc @ bundeswehrausf__374hrung_1_1 @ bundeswehr_1_1 )
& ( sub @ boxermotor_1_1 @ motor__1_1 )
& ( assoc @ boxermotor_1_1 @ boxer_2_1 ) ) ).
thf(zip_derived_cl10670,plain,
attr @ c37245 @ c37246,
inference(cnf,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_514]) ).
thf(sub__sub_0_expansion,axiom,
! [X0: $i,X1: $i] :
( ( sub @ X0 @ X1 )
=> ? [X2: $i] :
( ( subr @ X2 @ sub_0 )
& ( arg2 @ X2 @ X1 )
& ( arg1 @ X2 @ X0 ) ) ) ).
thf(zip_derived_cl313,plain,
! [X0: $i,X1: $i] :
( ( arg1 @ ( sk__57 @ X0 @ X1 ) @ X1 )
| ~ ( sub @ X1 @ X0 ) ),
inference(cnf,[status(esa)],[sub__sub_0_expansion]) ).
thf(zip_derived_cl312,plain,
! [X0: $i,X1: $i] :
( ( arg2 @ ( sk__57 @ X0 @ X1 ) @ X0 )
| ~ ( sub @ X1 @ X0 ) ),
inference(cnf,[status(esa)],[sub__sub_0_expansion]) ).
thf(sub__bezeichnen_1_1_als,axiom,
! [X0: $i,X1: $i,X2: $i] :
( ( ( arg1 @ X0 @ X1 )
& ( arg2 @ X0 @ X2 )
& ( subr @ X0 @ sub_0 ) )
=> ? [X3: $i,X4: $i,X5: $i] :
( ( subs @ X3 @ bezeichnen_1_1 )
& ( subr @ X4 @ rprs_0 )
& ( sub @ X5 @ X2 )
& ( obj @ X3 @ X1 )
& ( mcont @ X3 @ X4 )
& ( hsit @ X0 @ X3 )
& ( arg2 @ X4 @ X5 )
& ( arg1 @ X4 @ X1 ) ) ) ).
thf(zip_derived_cl305,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( subr @ X0 @ sub_0 )
| ~ ( arg1 @ X0 @ X1 )
| ~ ( arg2 @ X0 @ X2 )
| ( obj @ ( sk__54 @ X2 @ X1 @ X0 ) @ X1 ) ),
inference(cnf,[status(esa)],[sub__bezeichnen_1_1_als]) ).
thf(synth_qa07_007_mira_wp_514,conjecture,
? [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( ( sub @ X2 @ name_1_1 )
& ( sub @ X1 @ name_1_1 )
& ( obj @ X4 @ X0 )
& ( attr @ X5 @ X6 )
& ( attr @ X3 @ X2 )
& ( attr @ X0 @ X1 ) ) ).
thf(zf_stmt_0,negated_conjecture,
~ ? [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( ( sub @ X2 @ name_1_1 )
& ( sub @ X1 @ name_1_1 )
& ( obj @ X4 @ X0 )
& ( attr @ X5 @ X6 )
& ( attr @ X3 @ X2 )
& ( attr @ X0 @ X1 ) ),
inference('cnf.neg',[status(esa)],[synth_qa07_007_mira_wp_514]) ).
thf(zip_derived_cl10365,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( ~ ( sub @ X0 @ name_1_1 )
| ~ ( sub @ X1 @ name_1_1 )
| ~ ( obj @ X2 @ X3 )
| ~ ( attr @ X4 @ X0 )
| ~ ( attr @ X3 @ X1 )
| ~ ( attr @ X5 @ X6 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl10678,plain,
( ! [X1: $i,X2: $i,X3: $i] :
( ~ ( obj @ X2 @ X3 )
| ~ ( sub @ X1 @ name_1_1 )
| ~ ( attr @ X3 @ X1 ) )
<= ! [X1: $i,X2: $i,X3: $i] :
( ~ ( obj @ X2 @ X3 )
| ~ ( sub @ X1 @ name_1_1 )
| ~ ( attr @ X3 @ X1 ) ) ),
inference(split,[status(esa)],[zip_derived_cl10365]) ).
thf(zip_derived_cl10670_001,plain,
attr @ c37245 @ c37246,
inference(cnf,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_514]) ).
thf(zip_derived_cl10676,plain,
( ! [X5: $i,X6: $i] :
~ ( attr @ X5 @ X6 )
<= ! [X5: $i,X6: $i] :
~ ( attr @ X5 @ X6 ) ),
inference(split,[status(esa)],[zip_derived_cl10365]) ).
thf('0',plain,
~ ! [X5: $i,X6: $i] :
~ ( attr @ X5 @ X6 ),
inference('s_sup-',[status(thm)],[zip_derived_cl10670,zip_derived_cl10676]) ).
thf(zip_derived_cl10677,plain,
( ! [X0: $i,X4: $i] :
( ~ ( sub @ X0 @ name_1_1 )
| ~ ( attr @ X4 @ X0 ) )
<= ! [X0: $i,X4: $i] :
( ~ ( sub @ X0 @ name_1_1 )
| ~ ( attr @ X4 @ X0 ) ) ),
inference(split,[status(esa)],[zip_derived_cl10365]) ).
thf(zip_derived_cl10670_002,plain,
attr @ c37245 @ c37246,
inference(cnf,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_514]) ).
thf(zip_derived_cl21743,plain,
( ~ ( sub @ c37246 @ name_1_1 )
<= ! [X0: $i,X4: $i] :
( ~ ( sub @ X0 @ name_1_1 )
| ~ ( attr @ X4 @ X0 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl10677,zip_derived_cl10670]) ).
thf(zip_derived_cl10668,plain,
sub @ c37246 @ name_1_1,
inference(cnf,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_514]) ).
thf('1',plain,
~ ! [X0: $i,X4: $i] :
( ~ ( sub @ X0 @ name_1_1 )
| ~ ( attr @ X4 @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl21743,zip_derived_cl10668]) ).
thf('2',plain,
( ! [X1: $i,X2: $i,X3: $i] :
( ~ ( obj @ X2 @ X3 )
| ~ ( sub @ X1 @ name_1_1 )
| ~ ( attr @ X3 @ X1 ) )
| ! [X0: $i,X4: $i] :
( ~ ( sub @ X0 @ name_1_1 )
| ~ ( attr @ X4 @ X0 ) )
| ! [X5: $i,X6: $i] :
~ ( attr @ X5 @ X6 ) ),
inference(split,[status(esa)],[zip_derived_cl10365]) ).
thf('3',plain,
! [X1: $i,X2: $i,X3: $i] :
( ~ ( obj @ X2 @ X3 )
| ~ ( sub @ X1 @ name_1_1 )
| ~ ( attr @ X3 @ X1 ) ),
inference('sat_resolution*',[status(thm)],['0','1','2']) ).
thf(zip_derived_cl21747,plain,
! [X1: $i,X2: $i,X3: $i] :
( ~ ( obj @ X2 @ X3 )
| ~ ( sub @ X1 @ name_1_1 )
| ~ ( attr @ X3 @ X1 ) ),
inference(simpl_trail,[status(thm)],[zip_derived_cl10678,'3']) ).
thf(zip_derived_cl31422,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ( arg2 @ X1 @ X2 )
| ~ ( arg1 @ X1 @ X0 )
| ~ ( subr @ X1 @ sub_0 )
| ~ ( sub @ X3 @ name_1_1 )
| ~ ( attr @ X0 @ X3 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl305,zip_derived_cl21747]) ).
thf(zip_derived_cl32324,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ( sub @ X1 @ X0 )
| ~ ( arg1 @ ( sk__57 @ X0 @ X1 ) @ X2 )
| ~ ( subr @ ( sk__57 @ X0 @ X1 ) @ sub_0 )
| ~ ( sub @ X3 @ name_1_1 )
| ~ ( attr @ X2 @ X3 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl312,zip_derived_cl31422]) ).
thf(zip_derived_cl311,plain,
! [X0: $i,X1: $i] :
( ( subr @ ( sk__57 @ X0 @ X1 ) @ sub_0 )
| ~ ( sub @ X1 @ X0 ) ),
inference(cnf,[status(esa)],[sub__sub_0_expansion]) ).
thf(zip_derived_cl32579,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ( attr @ X2 @ X3 )
| ~ ( sub @ X3 @ name_1_1 )
| ~ ( arg1 @ ( sk__57 @ X0 @ X1 ) @ X2 )
| ~ ( sub @ X1 @ X0 ) ),
inference(clc,[status(thm)],[zip_derived_cl32324,zip_derived_cl311]) ).
thf(zip_derived_cl32580,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( sub @ X0 @ X1 )
| ~ ( attr @ X0 @ X2 )
| ~ ( sub @ X2 @ name_1_1 )
| ~ ( sub @ X0 @ X1 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl313,zip_derived_cl32579]) ).
thf(zip_derived_cl32581,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( sub @ X2 @ name_1_1 )
| ~ ( attr @ X0 @ X2 )
| ~ ( sub @ X0 @ X1 ) ),
inference(simplify,[status(thm)],[zip_derived_cl32580]) ).
thf(zip_derived_cl32582,plain,
! [X0: $i] :
( ~ ( sub @ c37246 @ name_1_1 )
| ~ ( sub @ c37245 @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl10670,zip_derived_cl32581]) ).
thf(zip_derived_cl10668_003,plain,
sub @ c37246 @ name_1_1,
inference(cnf,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_514]) ).
thf(zip_derived_cl32583,plain,
! [X0: $i] :
~ ( sub @ c37245 @ X0 ),
inference(demod,[status(thm)],[zip_derived_cl32582,zip_derived_cl10668]) ).
thf(zip_derived_cl10669,plain,
sub @ c37245 @ stadt__1_1,
inference(cnf,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_514]) ).
thf(zip_derived_cl32584,plain,
$false,
inference('s_sup+',[status(thm)],[zip_derived_cl32583,zip_derived_cl10669]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : CSR115+90 : TPTP v9.2.0. Released v4.0.0.
% 0.07/0.12 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.ym7XDgGbFR true
% 0.07/0.32 % Computer : n013.cluster.edu
% 0.07/0.32 % Model : x86_64 x86_64
% 0.07/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.32 % Memory : 8042.1875MB
% 0.07/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.32 % CPULimit : 300
% 0.07/0.32 % WCLimit : 300
% 0.07/0.32 % DateTime : Wed Oct 1 15:00:53 EDT 2025
% 0.07/0.32 % CPUTime :
% 0.07/0.32 % Running portfolio for 300 s
% 0.07/0.32 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.32 % Number of cores: 8
% 0.07/0.32 % Python version: Python 3.6.8
% 0.13/0.33 % Running in FO mode
% 0.13/0.56 % Total configuration time : 435
% 0.13/0.56 % Estimated wc time : 1092
% 0.13/0.56 % Estimated cpu time (7 cpus) : 156.0
% 0.70/0.64 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.70/0.69 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.89/0.71 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.89/0.73 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.89/0.73 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.89/0.73 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.89/0.74 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 3.36/1.35 % /export/starexec/sandbox/solver/bin/fo/fo1_lcnf.sh running for 50s
% 4.69/1.64 % /export/starexec/sandbox/solver/bin/fo/fo17_bce.sh running for 50s
% 42.06/9.20 % Solved by fo/fo1_av.sh.
% 42.06/9.20 % done 2780 iterations in 8.423s
% 42.06/9.20 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 42.06/9.20 % SZS output start Refutation
% See solution above
% 42.06/9.20
% 42.06/9.20
% 42.06/9.20 % Terminating...
% 42.99/9.36 % Runner terminated.
% 42.99/9.37 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------