%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR113+23 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n019.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 : 600s
% DateTime : Fri Jul 15 21:16:28 EDT 2022
% Result : Theorem 184.86s 178.49s
% Output : Proof 184.91s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : CSR113+23 : TPTP v8.1.0. Released v4.0.0.
% 0.04/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.35 % Computer : n019.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Sat Jun 11 14:27:55 EDT 2022
% 0.13/0.35 % CPUTime :
% 184.86/178.49 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 184.91/178.49 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 184.91/178.50
% 184.91/178.50 %-----------------------------------------------------
% 184.91/178.50 fof(ave07_era5_synth_qa07_003_mira_wp_253, hypothesis, pred(c43330, lef__350vre_1_1) & attr(c43332, c43333) & sub(c43332, mensch_1_1) & sub(c43333, eigenname_1_1) & val(c43333, c43334) & tupl(c43334, edouard_0, ren__351_0) & attr(c43341, c43342) & prop(c43341, de_1_1) & sub(c43341, mensch_1_1) & sub(c43342, familiename_1_1) & val(c43342, laboulaye_0) & pred(c43346, enkel__1_1) & attch(c43350, c43346) & sub(c43350, marquis_1_1) & attr(c43358, c43359) & prop(c43358, de_1_1) & sub(c43358, stadt__1_1) & sub(c43359, name_1_1) & val(c43359, lafayette_0) & pred(c43362, bartholdi_1_1) & attr(c43364, c43365) & sub(c43364, mensch_1_1) & sub(c43365, eigenname_1_1) & val(c43365, c43366) & tupl(c43366, fr__351d__351ric_0, auguste_0) & prop(c43375, jugendlich_1_1) & sub(c43375, k__374nstler_1_1) & attr(c43384, c43385) & sub(c43384, gebiet_1_1) & sub(c43385, name_1_1) & val(c43385, elsa__337_0) & obj(c43400, c43404) & subs(c43400, finanzierung_1_1) & sub(c43404, freiheitsstatue_1_1) & sub(c43411, geschenk__1_1) & attr(c43441, c43442) & sub(c43441, land_1_1) & sub(c43442, name_1_1) & val(c43442, usa_0) & obj(c43449, c43444) & subs(c43449, einweihung_1_1) & prop(c43461, c43325) & tupl_p17(c44809, c43332, c43330, c43341, c43346, c43358, c43364, c43362, c43375, c43384, c43375, c43400, c43411, c43441, c43449, c43451, c43461) & assoc(freiheitsstatue_1_1, freiheit_1_1) & sub(freiheitsstatue_1_1, statue_1_1) & chsp2(miterleben_1_1, c43325) & sort(c43330, o) & card(c43330, cons(x_constant, cons(int1, nil))) & etype(c43330, int1) & fact(c43330, real) & gener(c43330, gener_c) & quant(c43330, mult) & refer(c43330, indet) & varia(c43330, varia_c) & sort(lef__350vre_1_1, o) & card(lef__350vre_1_1, int1) & etype(lef__350vre_1_1, int0) & fact(lef__350vre_1_1, real) & gener(lef__350vre_1_1, ge) & quant(lef__350vre_1_1, one) & refer(lef__350vre_1_1, refer_c) & varia(lef__350vre_1_1, varia_c) & sort(c43332, d) & card(c43332, int1) & etype(c43332, int0) & fact(c43332, real) & gener(c43332, sp) & quant(c43332, one) & refer(c43332, det) & varia(c43332, con) & sort(c43333, na) & card(c43333, int1) & etype(c43333, int0) & fact(c43333, real) & gener(c43333, sp) & quant(c43333, one) & refer(c43333, indet) & varia(c43333, varia_c) & sort(mensch_1_1, d) & card(mensch_1_1, int1) & etype(mensch_1_1, int0) & fact(mensch_1_1, real) & gener(mensch_1_1, ge) & quant(mensch_1_1, one) & refer(mensch_1_1, refer_c) & varia(mensch_1_1, varia_c) & sort(eigenname_1_1, na) & card(eigenname_1_1, int1) & etype(eigenname_1_1, int0) & fact(eigenname_1_1, real) & gener(eigenname_1_1, ge) & quant(eigenname_1_1, one) & refer(eigenname_1_1, refer_c) & varia(eigenname_1_1, varia_c) & sort(c43334, fe) & sort(edouard_0, fe) & sort(ren__351_0, fe) & sort(c43341, d) & card(c43341, int1) & etype(c43341, int0) & fact(c43341, real) & gener(c43341, sp) & quant(c43341, one) & refer(c43341, det) & varia(c43341, con) & sort(c43342, na) & card(c43342, int1) & etype(c43342, int0) & fact(c43342, real) & gener(c43342, sp) & quant(c43342, one) & refer(c43342, det) & varia(c43342, varia_c) & sort(de_1_1, gq) & sort(familiename_1_1, na) & card(familiename_1_1, int1) & etype(familiename_1_1, int0) & fact(familiename_1_1, real) & gener(familiename_1_1, ge) & quant(familiename_1_1, one) & refer(familiename_1_1, refer_c) & varia(familiename_1_1, varia_c) & sort(laboulaye_0, fe) & sort(c43346, d) & card(c43346, cons(x_constant, cons(int1, nil))) & etype(c43346, int1) & fact(c43346, real) & gener(c43346, sp) & quant(c43346, mult) & refer(c43346, det) & varia(c43346, con) & sort(enkel__1_1, d) & card(enkel__1_1, int1) & etype(enkel__1_1, int0) & fact(enkel__1_1, real) & gener(enkel__1_1, ge) & quant(enkel__1_1, one) & refer(enkel__1_1, refer_c) & varia(enkel__1_1, varia_c) & sort(c43350, o) & card(c43350, int1) & etype(c43350, int0) & fact(c43350, real) & gener(c43350, sp) & quant(c43350, one) & refer(c43350, det) & varia(c43350, con) & sort(marquis_1_1, o) & card(marquis_1_1, int1) & etype(marquis_1_1, int0) & fact(marquis_1_1, real) & gener(marquis_1_1, ge) & quant(marquis_1_1, one) & refer(marquis_1_1, refer_c) & varia(marquis_1_1, varia_c) & sort(c43358, d) & sort(c43358, io) & card(c43358, int1) & etype(c43358, int0) & fact(c43358, real) & gener(c43358, sp) & quant(c43358, one) & refer(c43358, det) & varia(c43358, con) & sort(c43359, na) & card(c43359, int1) & etype(c43359, int0) & fact(c43359, real) & gener(c43359, sp) & quant(c43359, one) & refer(c43359, det) & varia(c43359, varia_c) & sort(stadt__1_1, d) & sort(stadt__1_1, io) & card(stadt__1_1, int1) & etype(stadt__1_1, int0) & fact(stadt__1_1, real) & gener(stadt__1_1, ge) & quant(stadt__1_1, one) & refer(stadt__1_1, refer_c) & varia(stadt__1_1, varia_c) & sort(name_1_1, na) & card(name_1_1, int1) & etype(name_1_1, int0) & fact(name_1_1, real) & gener(name_1_1, ge) & quant(name_1_1, one) & refer(name_1_1, refer_c) & varia(name_1_1, varia_c) & sort(lafayette_0, fe) & sort(c43362, o) & card(c43362, cons(x_constant, cons(int1, nil))) & etype(c43362, int1) & fact(c43362, real) & gener(c43362, gener_c) & quant(c43362, mult) & refer(c43362, indet) & varia(c43362, varia_c) & sort(bartholdi_1_1, o) & card(bartholdi_1_1, int1) & etype(bartholdi_1_1, int0) & fact(bartholdi_1_1, real) & gener(bartholdi_1_1, ge) & quant(bartholdi_1_1, one) & refer(bartholdi_1_1, refer_c) & varia(bartholdi_1_1, varia_c) & sort(c43364, d) & card(c43364, int1) & etype(c43364, int0) & fact(c43364, real) & gener(c43364, sp) & quant(c43364, one) & refer(c43364, det) & varia(c43364, con) & sort(c43365, na) & card(c43365, int1) & etype(c43365, int0) & fact(c43365, real) & gener(c43365, sp) & quant(c43365, one) & refer(c43365, indet) & varia(c43365, varia_c) & sort(c43366, fe) & sort(fr__351d__351ric_0, fe) & sort(auguste_0, fe) & sort(c43375, d) & card(c43375, int1) & etype(c43375, int0) & fact(c43375, real) & gener(c43375, sp) & quant(c43375, one) & refer(c43375, indet) & varia(c43375, varia_c) & sort(jugendlich_1_1, nq) & sort(k__374nstler_1_1, d) & card(k__374nstler_1_1, int1) & etype(k__374nstler_1_1, int0) & fact(k__374nstler_1_1, real) & gener(k__374nstler_1_1, ge) & quant(k__374nstler_1_1, one) & refer(k__374nstler_1_1, refer_c) & varia(k__374nstler_1_1, varia_c) & sort(c43384, d) & card(c43384, int1) & etype(c43384, int0) & fact(c43384, real) & gener(c43384, sp) & quant(c43384, one) & refer(c43384, det) & varia(c43384, con) & sort(c43385, na) & card(c43385, int1) & etype(c43385, int0) & fact(c43385, real) & gener(c43385, sp) & quant(c43385, one) & refer(c43385, indet) & varia(c43385, varia_c) & sort(gebiet_1_1, d) & card(gebiet_1_1, int1) & etype(gebiet_1_1, int0) & fact(gebiet_1_1, real) & gener(gebiet_1_1, ge) & quant(gebiet_1_1, one) & refer(gebiet_1_1, refer_c) & varia(gebiet_1_1, varia_c) & sort(elsa__337_0, fe) & sort(c43400, ad) & card(c43400, int1) & etype(c43400, int0) & fact(c43400, real) & gener(c43400, sp) & quant(c43400, one) & refer(c43400, det) & varia(c43400, con) & sort(c43404, d) & card(c43404, int1) & etype(c43404, int0) & fact(c43404, real) & gener(c43404, sp) & quant(c43404, one) & refer(c43404, det) & varia(c43404, con) & sort(finanzierung_1_1, ad) & card(finanzierung_1_1, int1) & etype(finanzierung_1_1, int0) & fact(finanzierung_1_1, real) & gener(finanzierung_1_1, ge) & quant(finanzierung_1_1, one) & refer(finanzierung_1_1, refer_c) & varia(finanzierung_1_1, varia_c) & sort(freiheitsstatue_1_1, d) & card(freiheitsstatue_1_1, int1) & etype(freiheitsstatue_1_1, int0) & fact(freiheitsstatue_1_1, real) & gener(freiheitsstatue_1_1, ge) & quant(freiheitsstatue_1_1, one) & refer(freiheitsstatue_1_1, refer_c) & varia(freiheitsstatue_1_1, varia_c) & sort(c43411, co) & card(c43411, card_c) & etype(c43411, etype_c) & fact(c43411, real) & gener(c43411, sp) & quant(c43411, quant_c) & refer(c43411, indet) & varia(c43411, varia_c) & sort(geschenk__1_1, co) & card(geschenk__1_1, card_c) & etype(geschenk__1_1, etype_c) & fact(geschenk__1_1, real) & gener(geschenk__1_1, ge) & quant(geschenk__1_1, quant_c) & refer(geschenk__1_1, refer_c) & varia(geschenk__1_1, varia_c) & sort(c43441, d) & sort(c43441, io) & card(c43441, int1) & etype(c43441, int0) & fact(c43441, real) & gener(c43441, sp) & quant(c43441, one) & refer(c43441, det) & varia(c43441, con) & sort(c43442, na) & card(c43442, int1) & etype(c43442, int0) & fact(c43442, real) & gener(c43442, sp) & quant(c43442, one) & refer(c43442, indet) & varia(c43442, varia_c) & sort(land_1_1, d) & sort(land_1_1, io) & card(land_1_1, int1) & etype(land_1_1, int0) & fact(land_1_1, real) & gener(land_1_1, ge) & quant(land_1_1, one) & refer(land_1_1, refer_c) & varia(land_1_1, varia_c) & sort(usa_0, fe) & sort(c43449, ad) & card(c43449, int1) & etype(c43449, int0) & fact(c43449, real) & gener(c43449, sp) & quant(c43449, one) & refer(c43449, det) & varia(c43449, varia_c) & sort(c43444, co) & card(c43444, card_c) & etype(c43444, etype_c) & fact(c43444, real) & gener(c43444, sp) & quant(c43444, quant_c) & refer(c43444, det) & varia(c43444, varia_c) & sort(einweihung_1_1, ad) & card(einweihung_1_1, int1) & etype(einweihung_1_1, int0) & fact(einweihung_1_1, real) & gener(einweihung_1_1, ge) & quant(einweihung_1_1, one) & refer(einweihung_1_1, refer_c) & varia(einweihung_1_1, varia_c) & sort(c43461, o) & card(c43461, int1) & etype(c43461, int0) & fact(c43461, real) & gener(c43461, gener_c) & quant(c43461, one) & refer(c43461, refer_c) & varia(c43461, varia_c) & sort(c43325, tq) & sort(c44809, ent) & card(c44809, card_c) & etype(c44809, etype_c) & fact(c44809, real) & gener(c44809, gener_c) & quant(c44809, quant_c) & refer(c44809, refer_c) & varia(c44809, varia_c) & sort(c43451, o) & card(c43451, int1) & etype(c43451, int0) & fact(c43451, real) & gener(c43451, sp) & quant(c43451, one) & refer(c43451, det) & varia(c43451, varia_c) & sort(freiheit_1_1, as) & sort(freiheit_1_1, io) & card(freiheit_1_1, int1) & etype(freiheit_1_1, int0) & fact(freiheit_1_1, real) & gener(freiheit_1_1, ge) & quant(freiheit_1_1, one) & refer(freiheit_1_1, refer_c) & varia(freiheit_1_1, varia_c) & sort(statue_1_1, d) & card(statue_1_1, int1) & etype(statue_1_1, int0) & fact(statue_1_1, real) & gener(statue_1_1, ge) & quant(statue_1_1, one) & refer(statue_1_1, refer_c) & varia(statue_1_1, varia_c) & sort(miterleben_1_1, dn) & fact(miterleben_1_1, real) & gener(miterleben_1_1, ge), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ave07_era5_synth_qa07_003_mira_wp_253)).
% 184.91/178.50 fof(member_second, axiom, ! [_589634, _589637, _589640] : (member(_589634, _589640) => member(_589634, cons(_589637, _589640))), file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax', member_second)).
% 184.91/178.50 fof(attr_name__abk__374rzung_stehen_1_b_f__374r, axiom, ! [_590152, _590155, _590158] : (attr(_590158, _590152) & member(_590155, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil)))) & sub(_590152, _590155) => ? [_590217] : (mcont(_590217, _590158) & obj(_590217, _590158) & scar(_590217, _590158) & subs(_590217, stehen_1_b))), file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax', attr_name__abk__374rzung_stehen_1_b_f__374r)).
% 184.91/178.50 fof(synth_qa07_003_mira_wp_253, conjecture, ? [_592764, _592767, _592770, _592773] : (attr(_592767, _592764) & scar(_592770, _592773) & sub(_592764, name_1_1) & val(_592764, usa_0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', synth_qa07_003_mira_wp_253)).
% 184.91/178.50 fof(member_first, axiom, ! [_593170, _593173] : member(_593170, cons(_593170, _593173)), file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax', member_first)).
% 184.91/178.50
% 184.91/178.50 cnf(1, plain, [-(sub(c43442, name_1_1))], clausify(ave07_era5_synth_qa07_003_mira_wp_253)).
% 184.91/178.50 cnf(2, plain, [-(attr(c43441, c43442))], clausify(ave07_era5_synth_qa07_003_mira_wp_253)).
% 184.91/178.50 cnf(3, plain, [-(val(c43442, usa_0))], clausify(ave07_era5_synth_qa07_003_mira_wp_253)).
% 184.91/178.50 cnf(4, plain, [member(_130861, _130863), -(member(_130861, cons(_130862, _130863)))], clausify(member_second)).
% 184.91/178.50 cnf(5, plain, [-(scar(52 ^ [_132948, _132947, _132946], _132948)), attr(_132948, _132946), member(_132947, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil)))), sub(_132946, _132947)], clausify(attr_name__abk__374rzung_stehen_1_b_f__374r)).
% 184.91/178.50 cnf(6, plain, [attr(_194672, _194671), scar(_194673, _194674), sub(_194671, name_1_1), val(_194671, usa_0)], clausify(synth_qa07_003_mira_wp_253)).
% 184.91/178.50 cnf(7, plain, [-(member(_130850, cons(_130850, _130851)))], clausify(member_first)).
% 184.91/178.50
% 184.91/178.50 cnf('1',plain,[attr(c43441, c43442), scar(52 ^ [c43441, name_1_1, c43442], c43441), sub(c43442, name_1_1), val(c43442, usa_0)],start(6,bind([[_194672, _194673, _194674, _194671], [c43441, 52 ^ [c43441, name_1_1, c43442], c43441, c43442]]))).
% 184.91/178.50 cnf('1.1',plain,[-(attr(c43441, c43442))],extension(2)).
% 184.91/178.50 cnf('1.2',plain,[-(scar(52 ^ [c43441, name_1_1, c43442], c43441)), attr(c43441, c43442), member(name_1_1, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil)))), sub(c43442, name_1_1)],extension(5,bind([[_132948, _132946, _132947], [c43441, c43442, name_1_1]]))).
% 184.91/178.50 cnf('1.2.1',plain,[-(attr(c43441, c43442))],extension(2)).
% 184.91/178.50 cnf('1.2.2',plain,[-(member(name_1_1, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil))))), member(name_1_1, cons(familiename_1_1, cons(name_1_1, nil)))],extension(4,bind([[_130862, _130861, _130863], [eigenname_1_1, name_1_1, cons(familiename_1_1, cons(name_1_1, nil))]]))).
% 184.91/178.50 cnf('1.2.2.1',plain,[-(member(name_1_1, cons(familiename_1_1, cons(name_1_1, nil)))), member(name_1_1, cons(name_1_1, nil))],extension(4,bind([[_130862, _130861, _130863], [familiename_1_1, name_1_1, cons(name_1_1, nil)]]))).
% 184.91/178.50 cnf('1.2.2.1.1',plain,[-(member(name_1_1, cons(name_1_1, nil)))],extension(7,bind([[_130850, _130851], [name_1_1, nil]]))).
% 184.91/178.50 cnf('1.2.3',plain,[-(sub(c43442, name_1_1))],extension(1)).
% 184.91/178.50 cnf('1.3',plain,[-(sub(c43442, name_1_1))],extension(1)).
% 184.91/178.50 cnf('1.4',plain,[-(val(c43442, usa_0))],extension(3)).
% 184.91/178.50 %-----------------------------------------------------
% 184.91/178.50
% 184.91/178.50 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------