%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR115+25 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n028.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:41 EDT 2022
% Result : Theorem 181.41s 176.33s
% Output : Proof 181.41s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : CSR115+25 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.13 % Command : leancop_casc.sh %s %d
% 0.14/0.34 % Computer : n028.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 600
% 0.14/0.34 % DateTime : Sat Jun 11 16:45:50 EDT 2022
% 0.14/0.34 % CPUTime :
% 181.41/176.33 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 181.41/176.33 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 181.41/176.34
% 181.41/176.34 %-----------------------------------------------------
% 181.41/176.34 fof(sub__sub_0_expansion, axiom, ! [_587578, _587581] : (sub(_587578, _587581) => ? [_587599] : (arg1(_587599, _587578) & arg2(_587599, _587581) & subr(_587599, sub_0))), file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax', sub__sub_0_expansion)).
% 181.41/176.34 fof(sub__bezeichnen_1_1_als, axiom, ! [_588792, _588795, _588798] : (arg1(_588792, _588795) & arg2(_588792, _588798) & subr(_588792, sub_0) => ? [_588836, _588839, _588842] : (arg1(_588839, _588795) & arg2(_588839, _588842) & hsit(_588792, _588836) & mcont(_588836, _588839) & obj(_588836, _588795) & sub(_588842, _588798) & subr(_588839, rprs_0) & subs(_588836, bezeichnen_1_1))), file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax', sub__bezeichnen_1_1_als)).
% 181.41/176.34 fof(ave07_era5_synth_qa07_007_mira_news_1163, hypothesis, assoc(betreuungsplatz_1_1, betreuung_1_1) & sub(betreuungsplatz_1_1, platz_1_1) & subs(c133316, anschaffung_1_1) & pred(c133326, betreuungsplatz_1_1) & prop(c133326, c133296) & pred(c133332, kind_1_1) & sub(c133357, know_1_1) & pred(c133366, eltern_1_1) & sub(c133371, firma_1_1) & pred(c133383, kosten__1_1) & pred(c133388, kraft_1_1) & prop(c133388, neo_1_1) & attr(c133411, c133412) & sub(c133411, mensch_1_1) & sub(c133412, eigenname_1_1) & val(c133412, peter_0) & attr(c133415, c133416) & sub(c133415, stadt__1_1) & sub(c133416, name_1_1) & val(c133416, hackenberg_0) & attr(c133463, c133464) & sub(c133463, firma_1_1) & sub(c133464, name_1_1) & val(c133464, bmw_0) & pred(c133469, grundsatzthema_1_1) & prop(c133469, personalpolitisch_1_1) & subs(c133476, engagement_1_1) & attch(c133480, c133476) & sub(c133480, firma_1_1) & tupl_p16(c133747, c133311, c133316, c133326, c133332, c133311, c133357, c133366, c133371, c133383, c133388, c133411, c133415, c133463, c133469, c133476) & chsp2(eignen_1_1, c133296) & assoc(grundsatzthema_1_1, grundsatz_1_1) & sub(grundsatzthema_1_1, motto__1_1) & assoc(personalpolitisch_1_1, personal__1_1) & impl(personalpolitisch_1_1, politisch__1_1) & sort(betreuungsplatz_1_1, d) & card(betreuungsplatz_1_1, int1) & etype(betreuungsplatz_1_1, int0) & fact(betreuungsplatz_1_1, real) & gener(betreuungsplatz_1_1, ge) & quant(betreuungsplatz_1_1, one) & refer(betreuungsplatz_1_1, refer_c) & varia(betreuungsplatz_1_1, varia_c) & sort(betreuung_1_1, ad) & card(betreuung_1_1, int1) & etype(betreuung_1_1, int0) & fact(betreuung_1_1, real) & gener(betreuung_1_1, ge) & quant(betreuung_1_1, one) & refer(betreuung_1_1, refer_c) & varia(betreuung_1_1, varia_c) & sort(platz_1_1, d) & card(platz_1_1, int1) & etype(platz_1_1, int0) & fact(platz_1_1, real) & gener(platz_1_1, ge) & quant(platz_1_1, one) & refer(platz_1_1, refer_c) & varia(platz_1_1, varia_c) & sort(c133316, ad) & card(c133316, int1) & etype(c133316, int0) & fact(c133316, real) & gener(c133316, sp) & quant(c133316, one) & refer(c133316, det) & varia(c133316, con) & sort(anschaffung_1_1, ad) & card(anschaffung_1_1, int1) & etype(anschaffung_1_1, int0) & fact(anschaffung_1_1, real) & gener(anschaffung_1_1, ge) & quant(anschaffung_1_1, one) & refer(anschaffung_1_1, refer_c) & varia(anschaffung_1_1, varia_c) & sort(c133326, d) & card(c133326, cons(x_constant, cons(int1, nil))) & etype(c133326, int1) & fact(c133326, real) & gener(c133326, gener_c) & quant(c133326, mult) & refer(c133326, refer_c) & varia(c133326, varia_c) & sort(c133296, tq) & sort(c133332, d) & card(c133332, cons(x_constant, cons(int1, nil))) & etype(c133332, int1) & fact(c133332, real) & gener(c133332, sp) & quant(c133332, mult) & refer(c133332, det) & varia(c133332, con) & sort(kind_1_1, d) & card(kind_1_1, int1) & etype(kind_1_1, int0) & fact(kind_1_1, real) & gener(kind_1_1, ge) & quant(kind_1_1, one) & refer(kind_1_1, refer_c) & varia(kind_1_1, varia_c) & sort(c133357, o) & card(c133357, int1) & etype(c133357, int0) & fact(c133357, real) & gener(c133357, sp) & quant(c133357, one) & refer(c133357, det) & varia(c133357, con) & sort(know_1_1, o) & card(know_1_1, int1) & etype(know_1_1, int0) & fact(know_1_1, real) & gener(know_1_1, ge) & quant(know_1_1, one) & refer(know_1_1, refer_c) & varia(know_1_1, varia_c) & sort(c133366, d) & card(c133366, cons(x_constant, cons(int1, nil))) & etype(c133366, int1) & fact(c133366, real) & gener(c133366, sp) & quant(c133366, mult) & refer(c133366, det) & varia(c133366, con) & sort(eltern_1_1, d) & card(eltern_1_1, int1) & etype(eltern_1_1, int0) & fact(eltern_1_1, real) & gener(eltern_1_1, ge) & quant(eltern_1_1, one) & refer(eltern_1_1, refer_c) & varia(eltern_1_1, varia_c) & sort(c133371, d) & sort(c133371, io) & card(c133371, int1) & etype(c133371, int0) & fact(c133371, real) & gener(c133371, sp) & quant(c133371, one) & refer(c133371, det) & varia(c133371, con) & 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(c133383, io) & sort(c133383, oa) & card(c133383, int1) & etype(c133383, int2) & fact(c133383, real) & gener(c133383, sp) & quant(c133383, mult) & refer(c133383, det) & varia(c133383, con) & sort(kosten__1_1, io) & sort(kosten__1_1, oa) & card(kosten__1_1, int1) & etype(kosten__1_1, int1) & fact(kosten__1_1, real) & gener(kosten__1_1, ge) & quant(kosten__1_1, one) & refer(kosten__1_1, refer_c) & varia(kosten__1_1, varia_c) & sort(c133388, io) & card(c133388, cons(x_constant, cons(int1, nil))) & etype(c133388, int1) & fact(c133388, real) & gener(c133388, gener_c) & quant(c133388, mult) & refer(c133388, refer_c) & varia(c133388, varia_c) & sort(kraft_1_1, io) & card(kraft_1_1, int1) & etype(kraft_1_1, int0) & fact(kraft_1_1, real) & gener(kraft_1_1, ge) & quant(kraft_1_1, one) & refer(kraft_1_1, refer_c) & varia(kraft_1_1, varia_c) & sort(neo_1_1, nq) & sort(c133411, d) & card(c133411, int1) & etype(c133411, int0) & fact(c133411, real) & gener(c133411, sp) & quant(c133411, one) & refer(c133411, det) & varia(c133411, con) & sort(c133412, na) & card(c133412, int1) & etype(c133412, int0) & fact(c133412, real) & gener(c133412, sp) & quant(c133412, one) & refer(c133412, indet) & varia(c133412, 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(peter_0, fe) & sort(c133415, d) & sort(c133415, io) & card(c133415, int1) & etype(c133415, int0) & fact(c133415, real) & gener(c133415, sp) & quant(c133415, one) & refer(c133415, det) & varia(c133415, con) & sort(c133416, na) & card(c133416, int1) & etype(c133416, int0) & fact(c133416, real) & gener(c133416, sp) & quant(c133416, one) & refer(c133416, indet) & varia(c133416, 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(hackenberg_0, fe) & sort(c133463, d) & sort(c133463, io) & card(c133463, int1) & etype(c133463, int0) & fact(c133463, real) & gener(c133463, sp) & quant(c133463, one) & refer(c133463, det) & varia(c133463, con) & sort(c133464, na) & card(c133464, int1) & etype(c133464, int0) & fact(c133464, real) & gener(c133464, sp) & quant(c133464, one) & refer(c133464, indet) & varia(c133464, varia_c) & sort(bmw_0, fe) & sort(c133469, io) & card(c133469, cons(x_constant, cons(int1, nil))) & etype(c133469, int1) & fact(c133469, real) & gener(c133469, gener_c) & quant(c133469, mult) & refer(c133469, refer_c) & varia(c133469, varia_c) & sort(grundsatzthema_1_1, io) & card(grundsatzthema_1_1, int1) & etype(grundsatzthema_1_1, int0) & fact(grundsatzthema_1_1, real) & gener(grundsatzthema_1_1, ge) & quant(grundsatzthema_1_1, one) & refer(grundsatzthema_1_1, refer_c) & varia(grundsatzthema_1_1, varia_c) & sort(personalpolitisch_1_1, tq) & sort(c133476, ad) & card(c133476, int1) & etype(c133476, int0) & fact(c133476, real) & gener(c133476, sp) & quant(c133476, one) & refer(c133476, det) & varia(c133476, con) & sort(engagement_1_1, ad) & card(engagement_1_1, int1) & etype(engagement_1_1, int0) & fact(engagement_1_1, real) & gener(engagement_1_1, ge) & quant(engagement_1_1, one) & refer(engagement_1_1, refer_c) & varia(engagement_1_1, varia_c) & sort(c133480, d) & sort(c133480, io) & card(c133480, int1) & etype(c133480, int0) & fact(c133480, real) & gener(c133480, sp) & quant(c133480, one) & refer(c133480, det) & varia(c133480, con) & sort(c133747, ent) & card(c133747, card_c) & etype(c133747, etype_c) & fact(c133747, real) & gener(c133747, gener_c) & quant(c133747, quant_c) & refer(c133747, refer_c) & varia(c133747, varia_c) & sort(c133311, d) & card(c133311, card_c) & etype(c133311, int1) & etype(c133311, int2) & etype(c133311, int3) & fact(c133311, real) & gener(c133311, sp) & quant(c133311, quant_c) & refer(c133311, det) & varia(c133311, varia_c) & sort(eignen_1_1, st) & fact(eignen_1_1, real) & gener(eignen_1_1, ge) & sort(grundsatz_1_1, io) & card(grundsatz_1_1, int1) & etype(grundsatz_1_1, int0) & fact(grundsatz_1_1, real) & gener(grundsatz_1_1, ge) & quant(grundsatz_1_1, one) & refer(grundsatz_1_1, refer_c) & varia(grundsatz_1_1, varia_c) & sort(motto__1_1, io) & card(motto__1_1, int1) & etype(motto__1_1, int0) & fact(motto__1_1, real) & gener(motto__1_1, ge) & quant(motto__1_1, one) & refer(motto__1_1, refer_c) & varia(motto__1_1, varia_c) & sort(personal__1_1, d) & sort(personal__1_1, io) & card(personal__1_1, card_c) & etype(personal__1_1, int1) & fact(personal__1_1, real) & gener(personal__1_1, ge) & quant(personal__1_1, quant_c) & refer(personal__1_1, refer_c) & varia(personal__1_1, varia_c) & sort(politisch__1_1, tq), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ave07_era5_synth_qa07_007_mira_news_1163)).
% 181.41/176.34 fof(synth_qa07_007_mira_news_1163, conjecture, ? [_596595, _596598, _596601, _596604, _596607, _596610, _596613] : (attr(_596595, _596598) & attr(_596604, _596601) & attr(_596610, _596613) & obj(_596607, _596595) & sub(_596598, name_1_1) & sub(_596595, firma_1_1) & sub(_596601, name_1_1) & val(_596598, bmw_0) & val(_596601, bmw_0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', synth_qa07_007_mira_news_1163)).
% 181.41/176.34
% 181.41/176.34 cnf(1, plain, [sub(_132751, _132752), -(subr(58 ^ [_132752, _132751], sub_0))], clausify(sub__sub_0_expansion)).
% 181.41/176.34 cnf(2, plain, [-(obj(55 ^ [_132738, _132737, _132736], _132737)), arg1(_132736, _132737), arg2(_132736, _132738), subr(_132736, sub_0)], clausify(sub__bezeichnen_1_1_als)).
% 181.41/176.34 cnf(3, plain, [-(attr(c133463, c133464))], clausify(ave07_era5_synth_qa07_007_mira_news_1163)).
% 181.41/176.34 cnf(4, plain, [sub(_132751, _132752), -(arg2(58 ^ [_132752, _132751], _132752))], clausify(sub__sub_0_expansion)).
% 181.41/176.34 cnf(5, plain, [sub(_132751, _132752), -(arg1(58 ^ [_132752, _132751], _132751))], clausify(sub__sub_0_expansion)).
% 181.41/176.34 cnf(6, plain, [-(val(c133464, bmw_0))], clausify(ave07_era5_synth_qa07_007_mira_news_1163)).
% 181.41/176.34 cnf(7, plain, [attr(_194278, _194279), attr(_194281, _194280), attr(_194283, _194284), obj(_194282, _194278), sub(_194279, name_1_1), sub(_194278, firma_1_1), sub(_194280, name_1_1), val(_194279, bmw_0), val(_194280, bmw_0)], clausify(synth_qa07_007_mira_news_1163)).
% 181.41/176.34 cnf(8, plain, [-(sub(c133463, firma_1_1))], clausify(ave07_era5_synth_qa07_007_mira_news_1163)).
% 181.41/176.34 cnf(9, plain, [-(sub(c133464, name_1_1))], clausify(ave07_era5_synth_qa07_007_mira_news_1163)).
% 181.41/176.34
% 181.41/176.34 cnf('1',plain,[attr(c133463, c133464), attr(c133463, c133464), attr(c133463, c133464), obj(55 ^ [firma_1_1, c133463, 58 ^ [firma_1_1, c133463]], c133463), sub(c133464, name_1_1), sub(c133463, firma_1_1), sub(c133464, name_1_1), val(c133464, bmw_0), val(c133464, bmw_0)],start(7,bind([[_194281, _194283, _194284, _194282, _194278, _194279, _194280], [c133463, c133463, c133464, 55 ^ [firma_1_1, c133463, 58 ^ [firma_1_1, c133463]], c133463, c133464, c133464]]))).
% 181.41/176.34 cnf('1.1',plain,[-(attr(c133463, c133464))],extension(3)).
% 181.41/176.34 cnf('1.2',plain,[-(attr(c133463, c133464))],extension(3)).
% 181.41/176.34 cnf('1.3',plain,[-(attr(c133463, c133464))],extension(3)).
% 181.41/176.34 cnf('1.4',plain,[-(obj(55 ^ [firma_1_1, c133463, 58 ^ [firma_1_1, c133463]], c133463)), arg1(58 ^ [firma_1_1, c133463], c133463), arg2(58 ^ [firma_1_1, c133463], firma_1_1), subr(58 ^ [firma_1_1, c133463], sub_0)],extension(2,bind([[_132737, _132738, _132736], [c133463, firma_1_1, 58 ^ [firma_1_1, c133463]]]))).
% 181.41/176.34 cnf('1.4.1',plain,[-(arg1(58 ^ [firma_1_1, c133463], c133463)), sub(c133463, firma_1_1)],extension(5,bind([[_132751, _132752], [c133463, firma_1_1]]))).
% 181.41/176.34 cnf('1.4.1.1',plain,[-(sub(c133463, firma_1_1))],extension(8)).
% 181.41/176.34 cnf('1.4.2',plain,[-(arg2(58 ^ [firma_1_1, c133463], firma_1_1)), sub(c133463, firma_1_1)],extension(4,bind([[_132751, _132752], [c133463, firma_1_1]]))).
% 181.41/176.34 cnf('1.4.2.1',plain,[-(sub(c133463, firma_1_1))],extension(8)).
% 181.41/176.34 cnf('1.4.3',plain,[-(subr(58 ^ [firma_1_1, c133463], sub_0)), sub(c133463, firma_1_1)],extension(1,bind([[_132751, _132752], [c133463, firma_1_1]]))).
% 181.41/176.34 cnf('1.4.3.1',plain,[-(sub(c133463, firma_1_1))],extension(8)).
% 181.41/176.34 cnf('1.5',plain,[-(sub(c133464, name_1_1))],extension(9)).
% 181.41/176.34 cnf('1.6',plain,[-(sub(c133463, firma_1_1))],extension(8)).
% 181.41/176.34 cnf('1.7',plain,[-(sub(c133464, name_1_1))],extension(9)).
% 181.41/176.34 cnf('1.8',plain,[-(val(c133464, bmw_0))],extension(6)).
% 181.41/176.34 cnf('1.9',plain,[-(val(c133464, bmw_0))],extension(6)).
% 181.41/176.34 %-----------------------------------------------------
% 181.41/176.34
% 181.41/176.35 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------