%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR115+6 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n025.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:51 EDT 2022
% Result : Theorem 217.31s 210.73s
% Output : Proof 217.41s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : CSR115+6 : TPTP v8.1.0. Released v4.0.0.
% 0.07/0.13 % Command : leancop_casc.sh %s %d
% 0.14/0.35 % Computer : n025.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 600
% 0.14/0.35 % DateTime : Fri Jun 10 21:57:36 EDT 2022
% 0.14/0.35 % CPUTime :
% 217.31/210.73 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 217.31/210.74 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 217.31/210.75
% 217.31/210.75 %-----------------------------------------------------
% 217.31/210.75 fof(state_adjective__in_state, axiom, ! [_468540, _468543, _468546] : (prop(_468540, _468543) & state_adjective_state_binding(_468543, _468546) => ? [_468574, _468577, _468580] : (in(_468580, _468574) & attr(_468574, _468577) & loc(_468540, _468580) & sub(_468574, land_1_1) & sub(_468577, name_1_1) & val(_468577, _468546))), file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax', state_adjective__in_state)).
% 217.31/210.75 fof(ave07_era5_synth_qa07_007_mira_news_1094, hypothesis, assoc(autokonzern_1_1, auto__1_1) & sub(autokonzern_1_1, firmengruppe_1_1) & attr(c18, c19) & sub(c18, stadt__1_1) & sub(c19, name_1_1) & val(c19, london_0) & sub(c21, feb_1_1) & tupl(c34, c18, c21) & attr(c55667, c55668) & prop(c55667, bundesdeutsch_1_1) & sub(c55667, autokonzern_1_1) & sub(c55668, name_1_1) & val(c55668, bmw_0) & prop(c55687, pass__351_1_1) & sub(c55687, woche_1_1) & subs(c55693, ankauf__1_1) & attch(c55986, c55693) & attr(c55986, c55987) & prop(c55986, britisch__1_1) & sub(c55986, firma_1_1) & sub(c55987, name_1_1) & val(c55987, rover_0) & subs(c55995, interesse_1_1) & subs(c55999, ankauf__1_1) & attch(c56008, c55999) & prop(c56008, britisch__1_1) & sub(c56008, luxusmarke_1_1) & attr(c56019, c56008) & attr(c56019, c56020) & sub(c56019, mensch_1_1) & sub(c56020, familiename_1_1) & val(c56020, roll_0) & attr(c56024, c56025) & sub(c56024, mensch_1_1) & sub(c56025, eigenname_1_1) & val(c56025, royce_0) & tupl_p8(c56046, c55667, c55669, c55687, c55693, c55995, c55999, c56024) & assoc(luxusmarke_1_1, luxus__1_1) & sub(luxusmarke_1_1, marke_1_1) & sort(autokonzern_1_1, d) & sort(autokonzern_1_1, io) & card(autokonzern_1_1, int1) & etype(autokonzern_1_1, int0) & fact(autokonzern_1_1, real) & gener(autokonzern_1_1, ge) & quant(autokonzern_1_1, one) & refer(autokonzern_1_1, refer_c) & varia(autokonzern_1_1, varia_c) & sort(auto__1_1, d) & card(auto__1_1, int1) & etype(auto__1_1, int0) & fact(auto__1_1, real) & gener(auto__1_1, ge) & quant(auto__1_1, one) & refer(auto__1_1, refer_c) & varia(auto__1_1, varia_c) & sort(firmengruppe_1_1, d) & sort(firmengruppe_1_1, io) & card(firmengruppe_1_1, int1) & etype(firmengruppe_1_1, int0) & fact(firmengruppe_1_1, real) & gener(firmengruppe_1_1, ge) & quant(firmengruppe_1_1, one) & refer(firmengruppe_1_1, refer_c) & varia(firmengruppe_1_1, varia_c) & sort(c18, d) & sort(c18, io) & card(c18, int1) & etype(c18, int0) & fact(c18, real) & gener(c18, sp) & quant(c18, one) & refer(c18, det) & varia(c18, con) & sort(c19, na) & card(c19, int1) & etype(c19, int0) & fact(c19, real) & gener(c19, sp) & quant(c19, one) & refer(c19, indet) & varia(c19, 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(london_0, fe) & sort(c21, o) & card(c21, int1) & etype(c21, int0) & fact(c21, real) & gener(c21, gener_c) & quant(c21, one) & refer(c21, refer_c) & varia(c21, varia_c) & sort(feb_1_1, o) & card(feb_1_1, int1) & etype(feb_1_1, int0) & fact(feb_1_1, real) & gener(feb_1_1, ge) & quant(feb_1_1, one) & refer(feb_1_1, refer_c) & varia(feb_1_1, varia_c) & sort(c34, ent) & card(c34, card_c) & etype(c34, etype_c) & fact(c34, real) & gener(c34, gener_c) & quant(c34, quant_c) & refer(c34, refer_c) & varia(c34, varia_c) & sort(c55667, d) & sort(c55667, io) & card(c55667, int1) & etype(c55667, int0) & fact(c55667, real) & gener(c55667, sp) & quant(c55667, one) & refer(c55667, det) & varia(c55667, con) & sort(c55668, na) & card(c55668, int1) & etype(c55668, int0) & fact(c55668, real) & gener(c55668, sp) & quant(c55668, one) & refer(c55668, indet) & varia(c55668, varia_c) & sort(bundesdeutsch_1_1, tq) & sort(bmw_0, fe) & sort(c55687, me) & sort(c55687, oa) & sort(c55687, ta) & card(c55687, card_c) & etype(c55687, etype_c) & fact(c55687, real) & gener(c55687, sp) & quant(c55687, quant_c) & refer(c55687, det) & varia(c55687, con) & sort(pass__351_1_1, tq) & sort(woche_1_1, me) & sort(woche_1_1, oa) & sort(woche_1_1, ta) & card(woche_1_1, card_c) & etype(woche_1_1, etype_c) & fact(woche_1_1, real) & gener(woche_1_1, ge) & quant(woche_1_1, quant_c) & refer(woche_1_1, refer_c) & varia(woche_1_1, varia_c) & sort(c55693, ad) & card(c55693, int1) & etype(c55693, int0) & fact(c55693, real) & gener(c55693, sp) & quant(c55693, one) & refer(c55693, det) & varia(c55693, con) & sort(ankauf__1_1, ad) & card(ankauf__1_1, int1) & etype(ankauf__1_1, int0) & fact(ankauf__1_1, real) & gener(ankauf__1_1, ge) & quant(ankauf__1_1, one) & refer(ankauf__1_1, refer_c) & varia(ankauf__1_1, varia_c) & sort(c55986, d) & sort(c55986, io) & card(c55986, int1) & etype(c55986, int0) & fact(c55986, real) & gener(c55986, sp) & quant(c55986, one) & refer(c55986, det) & varia(c55986, con) & sort(c55987, na) & card(c55987, int1) & etype(c55987, int0) & fact(c55987, real) & gener(c55987, sp) & quant(c55987, one) & refer(c55987, indet) & varia(c55987, varia_c) & sort(britisch__1_1, nq) & sort(firma_1_1, d) & sort(firma_1_1, io) & card(firma_1_1, int1) & etype(firma_1_1, int0) & fact(firma_1_1, real) & gener(firma_1_1, ge) & quant(firma_1_1, one) & refer(firma_1_1, refer_c) & varia(firma_1_1, varia_c) & sort(rover_0, fe) & sort(c55995, as) & card(c55995, int1) & etype(c55995, int0) & fact(c55995, real) & gener(c55995, gener_c) & quant(c55995, one) & refer(c55995, refer_c) & varia(c55995, varia_c) & sort(interesse_1_1, as) & card(interesse_1_1, int1) & etype(interesse_1_1, int0) & fact(interesse_1_1, real) & gener(interesse_1_1, ge) & quant(interesse_1_1, one) & refer(interesse_1_1, refer_c) & varia(interesse_1_1, varia_c) & sort(c55999, ad) & card(c55999, int1) & etype(c55999, int0) & fact(c55999, real) & gener(c55999, sp) & quant(c55999, one) & refer(c55999, det) & varia(c55999, con) & sort(c56008, io) & sort(c56008, oa) & card(c56008, int1) & etype(c56008, int0) & fact(c56008, real) & gener(c56008, sp) & quant(c56008, one) & refer(c56008, det) & varia(c56008, con) & sort(luxusmarke_1_1, io) & sort(luxusmarke_1_1, oa) & card(luxusmarke_1_1, int1) & etype(luxusmarke_1_1, int0) & fact(luxusmarke_1_1, real) & gener(luxusmarke_1_1, ge) & quant(luxusmarke_1_1, one) & refer(luxusmarke_1_1, refer_c) & varia(luxusmarke_1_1, varia_c) & sort(c56019, d) & card(c56019, int1) & etype(c56019, int0) & fact(c56019, real) & gener(c56019, sp) & quant(c56019, one) & refer(c56019, det) & varia(c56019, con) & sort(c56020, na) & card(c56020, int1) & etype(c56020, int0) & fact(c56020, real) & gener(c56020, sp) & quant(c56020, one) & refer(c56020, indet) & varia(c56020, 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(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(roll_0, fe) & sort(c56024, d) & card(c56024, int1) & etype(c56024, int0) & fact(c56024, real) & gener(c56024, sp) & quant(c56024, one) & refer(c56024, det) & varia(c56024, con) & sort(c56025, na) & card(c56025, int1) & etype(c56025, int0) & fact(c56025, real) & gener(c56025, sp) & quant(c56025, one) & refer(c56025, indet) & varia(c56025, 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(royce_0, fe) & sort(c56046, ent) & card(c56046, card_c) & etype(c56046, etype_c) & fact(c56046, real) & gener(c56046, gener_c) & quant(c56046, quant_c) & refer(c56046, refer_c) & varia(c56046, varia_c) & sort(c55669, o) & card(c55669, int1) & etype(c55669, int0) & fact(c55669, real) & gener(c55669, sp) & quant(c55669, one) & refer(c55669, det) & varia(c55669, varia_c) & sort(luxus__1_1, io) & card(luxus__1_1, int1) & etype(luxus__1_1, int0) & fact(luxus__1_1, real) & gener(luxus__1_1, ge) & quant(luxus__1_1, one) & refer(luxus__1_1, refer_c) & varia(luxus__1_1, varia_c) & sort(marke_1_1, io) & sort(marke_1_1, oa) & card(marke_1_1, int1) & etype(marke_1_1, int0) & fact(marke_1_1, real) & gener(marke_1_1, ge) & quant(marke_1_1, one) & refer(marke_1_1, refer_c) & varia(marke_1_1, varia_c), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ave07_era5_synth_qa07_007_mira_news_1094)).
% 217.31/210.75 fof(synth_qa07_007_mira_news_1094, conjecture, ? [_473235, _473238, _473241, _473244, _473247, _473250, _473253] : (attr(_473235, _473238) & attr(_473244, _473241) & attr(_473250, _473253) & obj(_473247, _473235) & sub(_473238, name_1_1) & sub(_473241, name_1_1) & val(_473238, bmw_0) & val(_473241, bmw_0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', synth_qa07_007_mira_news_1094)).
% 217.31/210.75 fof(loc__geben_1_1_loc, axiom, ! [_476588, _476591] : (has_fact_leq(_476591, real) & loc(_476591, _476588) => ? [_476619] : (loc(_476619, _476588) & obj(_476619, _476591) & subs(_476619, geben_1_1))), file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax', loc__geben_1_1_loc)).
% 217.31/210.75 fof(has_fact_eq, axiom, ! [_479050, _479053] : (fact(_479050, _479053) => has_fact_leq(_479050, _479053)), file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax', has_fact_eq)).
% 217.31/210.75 fof(fact_8849, axiom, state_adjective_state_binding(bundesdeutsch_1_1, bundesrepublik_0), file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax', fact_8849)).
% 217.31/210.75
% 217.31/210.75 cnf(1, plain, [-(loc(_132440, 50 ^ [_132442, _132441, _132440])), prop(_132440, _132441), state_adjective_state_binding(_132441, _132442)], clausify(state_adjective__in_state)).
% 217.31/210.75 cnf(2, plain, [-(attr(c55667, c55668))], clausify(ave07_era5_synth_qa07_007_mira_news_1094)).
% 217.31/210.75 cnf(3, plain, [attr(_194025, _194026), attr(_194028, _194027), attr(_194030, _194031), obj(_194029, _194025), sub(_194026, name_1_1), sub(_194027, name_1_1), val(_194026, bmw_0), val(_194027, bmw_0)], clausify(synth_qa07_007_mira_news_1094)).
% 217.31/210.75 cnf(4, plain, [-(sub(c55668, name_1_1))], clausify(ave07_era5_synth_qa07_007_mira_news_1094)).
% 217.31/210.75 cnf(5, plain, [-(obj(3 ^ [_131327, _131326], _131327)), has_fact_leq(_131327, real), loc(_131327, _131326)], clausify(loc__geben_1_1_loc)).
% 217.31/210.75 cnf(6, plain, [fact(_130544, _130545), -(has_fact_leq(_130544, _130545))], clausify(has_fact_eq)).
% 217.31/210.75 cnf(7, plain, [-(state_adjective_state_binding(bundesdeutsch_1_1, bundesrepublik_0))], clausify(fact_8849)).
% 217.31/210.75 cnf(8, plain, [-(prop(c55667, bundesdeutsch_1_1))], clausify(ave07_era5_synth_qa07_007_mira_news_1094)).
% 217.31/210.75 cnf(9, plain, [-(fact(c55667, real))], clausify(ave07_era5_synth_qa07_007_mira_news_1094)).
% 217.31/210.75 cnf(10, plain, [-(val(c55668, bmw_0))], clausify(ave07_era5_synth_qa07_007_mira_news_1094)).
% 217.31/210.75
% 217.31/210.75 cnf('1',plain,[attr(c55667, c55668), attr(c55667, c55668), attr(c55667, c55668), obj(3 ^ [c55667, 50 ^ [bundesrepublik_0, bundesdeutsch_1_1, c55667]], c55667), sub(c55668, name_1_1), sub(c55668, name_1_1), val(c55668, bmw_0), val(c55668, bmw_0)],start(3,bind([[_194028, _194030, _194031, _194029, _194025, _194026, _194027], [c55667, c55667, c55668, 3 ^ [c55667, 50 ^ [bundesrepublik_0, bundesdeutsch_1_1, c55667]], c55667, c55668, c55668]]))).
% 217.31/210.75 cnf('1.1',plain,[-(attr(c55667, c55668))],extension(2)).
% 217.31/210.75 cnf('1.2',plain,[-(attr(c55667, c55668))],extension(2)).
% 217.31/210.75 cnf('1.3',plain,[-(attr(c55667, c55668))],extension(2)).
% 217.31/210.75 cnf('1.4',plain,[-(obj(3 ^ [c55667, 50 ^ [bundesrepublik_0, bundesdeutsch_1_1, c55667]], c55667)), has_fact_leq(c55667, real), loc(c55667, 50 ^ [bundesrepublik_0, bundesdeutsch_1_1, c55667])],extension(5,bind([[_131327, _131326], [c55667, 50 ^ [bundesrepublik_0, bundesdeutsch_1_1, c55667]]]))).
% 217.31/210.75 cnf('1.4.1',plain,[-(has_fact_leq(c55667, real)), fact(c55667, real)],extension(6,bind([[_130544, _130545], [c55667, real]]))).
% 217.31/210.75 cnf('1.4.1.1',plain,[-(fact(c55667, real))],extension(9)).
% 217.31/210.75 cnf('1.4.2',plain,[-(loc(c55667, 50 ^ [bundesrepublik_0, bundesdeutsch_1_1, c55667])), prop(c55667, bundesdeutsch_1_1), state_adjective_state_binding(bundesdeutsch_1_1, bundesrepublik_0)],extension(1,bind([[_132440, _132441, _132442], [c55667, bundesdeutsch_1_1, bundesrepublik_0]]))).
% 217.31/210.75 cnf('1.4.2.1',plain,[-(prop(c55667, bundesdeutsch_1_1))],extension(8)).
% 217.31/210.75 cnf('1.4.2.2',plain,[-(state_adjective_state_binding(bundesdeutsch_1_1, bundesrepublik_0))],extension(7)).
% 217.31/210.75 cnf('1.5',plain,[-(sub(c55668, name_1_1))],extension(4)).
% 217.31/210.75 cnf('1.6',plain,[-(sub(c55668, name_1_1))],extension(4)).
% 217.31/210.75 cnf('1.7',plain,[-(val(c55668, bmw_0))],extension(10)).
% 217.31/210.75 cnf('1.8',plain,[-(val(c55668, bmw_0))],extension(10)).
% 217.31/210.75 %-----------------------------------------------------
% 217.41/210.75
% 217.41/210.76 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------