%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR115+72 : 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 234.16s 225.55s
% Output : Proof 234.16s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : CSR115+72 : TPTP v8.1.0. Released v4.0.0.
% 0.08/0.13 % Command : leancop_casc.sh %s %d
% 0.14/0.34 % Computer : n025.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 : Thu Jun 9 22:28:36 EDT 2022
% 0.14/0.34 % CPUTime :
% 234.16/225.55 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 234.16/225.55 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 234.16/225.56
% 234.16/225.56 %-----------------------------------------------------
% 234.16/225.56 fof(ave07_era5_synth_qa07_007_mira_wp_482, hypothesis, agt(c2, c1) & avrt(c2, c456) & benf(c2, c451) & subs(c2, verlassen_1_3) & attr(c451, c452) & attr(c451, c453) & sub(c451, hauptaktion__344r_1_1) & sub(c452, eigenname_1_1) & val(c452, camillo_0) & sub(c453, familiename_1_1) & val(c453, castiglioni_0) & sub(c456, firma_1_1) & sub(c528, namensrechte_1_1) & attr(c595, c596) & sub(c595, firma_1_1) & sub(c596, name_1_1) & val(c596, bmw_0) & agt(c598, c1) & dircl(c598, c601) & obj(c598, c528) & semrel(c598, c2) & subs(c598, mitnehmen_1_1) & flp(c601, c595) & assoc(hauptaktion__344r_1_1, haupt_1_1) & sub(hauptaktion__344r_1_1, aktion__344r_1_1) & assoc(namensrechte_1_1, name_1_1) & sub(namensrechte_1_1, rechte_1_1) & sort(c2, da) & fact(c2, real) & gener(c2, sp) & sort(c1, co) & card(c1, card_c) & etype(c1, etype_c) & fact(c1, real) & gener(c1, sp) & quant(c1, quant_c) & refer(c1, refer_c) & varia(c1, varia_c) & sort(c456, d) & sort(c456, io) & card(c456, int1) & etype(c456, int0) & fact(c456, real) & gener(c456, sp) & quant(c456, one) & refer(c456, det) & varia(c456, con) & sort(c451, d) & card(c451, int1) & etype(c451, int0) & fact(c451, real) & gener(c451, sp) & quant(c451, one) & refer(c451, det) & varia(c451, varia_c) & sort(verlassen_1_3, da) & fact(verlassen_1_3, real) & gener(verlassen_1_3, ge) & sort(c452, na) & card(c452, int1) & etype(c452, int0) & fact(c452, real) & gener(c452, sp) & quant(c452, one) & refer(c452, indet) & varia(c452, varia_c) & sort(c453, na) & card(c453, int1) & etype(c453, int0) & fact(c453, real) & gener(c453, sp) & quant(c453, one) & refer(c453, det) & varia(c453, varia_c) & sort(hauptaktion__344r_1_1, d) & sort(hauptaktion__344r_1_1, io) & card(hauptaktion__344r_1_1, int1) & etype(hauptaktion__344r_1_1, int0) & fact(hauptaktion__344r_1_1, real) & gener(hauptaktion__344r_1_1, ge) & quant(hauptaktion__344r_1_1, one) & refer(hauptaktion__344r_1_1, refer_c) & varia(hauptaktion__344r_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(camillo_0, fe) & 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(castiglioni_0, fe) & 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(c528, d) & sort(c528, io) & card(c528, int1) & etype(c528, int1) & fact(c528, real) & gener(c528, sp) & quant(c528, one) & refer(c528, det) & varia(c528, con) & sort(namensrechte_1_1, d) & sort(namensrechte_1_1, io) & card(namensrechte_1_1, card_c) & etype(namensrechte_1_1, int1) & fact(namensrechte_1_1, real) & gener(namensrechte_1_1, ge) & quant(namensrechte_1_1, quant_c) & refer(namensrechte_1_1, refer_c) & varia(namensrechte_1_1, varia_c) & sort(c595, d) & sort(c595, io) & card(c595, int1) & etype(c595, int0) & fact(c595, real) & gener(c595, sp) & quant(c595, one) & refer(c595, det) & varia(c595, con) & sort(c596, na) & card(c596, int1) & etype(c596, int0) & fact(c596, real) & gener(c596, sp) & quant(c596, one) & refer(c596, indet) & varia(c596, 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(bmw_0, fe) & sort(c598, da) & fact(c598, real) & gener(c598, sp) & sort(c601, l) & card(c601, int1) & etype(c601, int0) & fact(c601, real) & gener(c601, sp) & quant(c601, one) & refer(c601, det) & varia(c601, con) & sort(mitnehmen_1_1, da) & fact(mitnehmen_1_1, real) & gener(mitnehmen_1_1, ge) & sort(haupt_1_1, d) & card(haupt_1_1, int1) & etype(haupt_1_1, int0) & fact(haupt_1_1, real) & gener(haupt_1_1, ge) & quant(haupt_1_1, one) & refer(haupt_1_1, refer_c) & varia(haupt_1_1, varia_c) & sort(aktion__344r_1_1, d) & sort(aktion__344r_1_1, io) & card(aktion__344r_1_1, int1) & etype(aktion__344r_1_1, int0) & fact(aktion__344r_1_1, real) & gener(aktion__344r_1_1, ge) & quant(aktion__344r_1_1, one) & refer(aktion__344r_1_1, refer_c) & varia(aktion__344r_1_1, varia_c) & sort(rechte_1_1, d) & sort(rechte_1_1, io) & card(rechte_1_1, card_c) & etype(rechte_1_1, int1) & fact(rechte_1_1, real) & gener(rechte_1_1, ge) & quant(rechte_1_1, quant_c) & refer(rechte_1_1, refer_c) & varia(rechte_1_1, varia_c), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ave07_era5_synth_qa07_007_mira_wp_482)).
% 234.16/225.56 fof(synth_qa07_007_mira_wp_482, conjecture, ? [_754669, _754672, _754675, _754678, _754681, _754684, _754687] : (attr(_754669, _754672) & attr(_754678, _754675) & attr(_754684, _754687) & obj(_754681, _754669) & sub(_754672, name_1_1) & sub(_754669, firma_1_1) & sub(_754675, name_1_1) & val(_754672, bmw_0) & val(_754675, bmw_0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', synth_qa07_007_mira_wp_482)).
% 234.16/225.56 fof(sub__sub_0_expansion, axiom, ! [_755562, _755565] : (sub(_755562, _755565) => ? [_755583] : (arg1(_755583, _755562) & arg2(_755583, _755565) & subr(_755583, sub_0))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', sub__sub_0_expansion)).
% 234.16/225.56 fof(sub__bezeichnen_1_1_als, axiom, ! [_758556, _758559, _758562] : (arg1(_758556, _758559) & arg2(_758556, _758562) & subr(_758556, sub_0) => ? [_758600, _758603, _758606] : (arg1(_758603, _758559) & arg2(_758603, _758606) & hsit(_758556, _758600) & mcont(_758600, _758603) & obj(_758600, _758559) & sub(_758606, _758562) & subr(_758603, rprs_0) & subs(_758600, bezeichnen_1_1))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', sub__bezeichnen_1_1_als)).
% 234.16/225.56
% 234.16/225.56 cnf(1, plain, [-(attr(c595, c596))], clausify(ave07_era5_synth_qa07_007_mira_wp_482)).
% 234.16/225.56 cnf(2, plain, [attr(_192694, _192695), attr(_192697, _192696), attr(_192699, _192700), obj(_192698, _192694), sub(_192695, name_1_1), sub(_192694, firma_1_1), sub(_192696, name_1_1), val(_192695, bmw_0), val(_192696, bmw_0)], clausify(synth_qa07_007_mira_wp_482)).
% 234.16/225.56 cnf(3, plain, [-(sub(c596, name_1_1))], clausify(ave07_era5_synth_qa07_007_mira_wp_482)).
% 234.16/225.56 cnf(4, plain, [sub(_131709, _131710), -(arg1(58 ^ [_131710, _131709], _131709))], clausify(sub__sub_0_expansion)).
% 234.16/225.56 cnf(5, plain, [sub(_131709, _131710), -(arg2(58 ^ [_131710, _131709], _131710))], clausify(sub__sub_0_expansion)).
% 234.16/225.56 cnf(6, plain, [-(sub(c595, firma_1_1))], clausify(ave07_era5_synth_qa07_007_mira_wp_482)).
% 234.16/225.56 cnf(7, plain, [-(obj(55 ^ [_131696, _131695, _131694], _131695)), arg1(_131694, _131695), arg2(_131694, _131696), subr(_131694, sub_0)], clausify(sub__bezeichnen_1_1_als)).
% 234.16/225.56 cnf(8, plain, [sub(_131709, _131710), -(subr(58 ^ [_131710, _131709], sub_0))], clausify(sub__sub_0_expansion)).
% 234.16/225.56 cnf(9, plain, [-(val(c596, bmw_0))], clausify(ave07_era5_synth_qa07_007_mira_wp_482)).
% 234.16/225.56
% 234.16/225.56 cnf('1',plain,[attr(c595, c596), attr(c595, c596), attr(c595, c596), obj(55 ^ [firma_1_1, c595, 58 ^ [firma_1_1, c595]], c595), sub(c596, name_1_1), sub(c595, firma_1_1), sub(c596, name_1_1), val(c596, bmw_0), val(c596, bmw_0)],start(2,bind([[_192697, _192699, _192700, _192698, _192694, _192695, _192696], [c595, c595, c596, 55 ^ [firma_1_1, c595, 58 ^ [firma_1_1, c595]], c595, c596, c596]]))).
% 234.16/225.56 cnf('1.1',plain,[-(attr(c595, c596))],extension(1)).
% 234.16/225.56 cnf('1.2',plain,[-(attr(c595, c596))],extension(1)).
% 234.16/225.56 cnf('1.3',plain,[-(attr(c595, c596))],extension(1)).
% 234.16/225.56 cnf('1.4',plain,[-(obj(55 ^ [firma_1_1, c595, 58 ^ [firma_1_1, c595]], c595)), arg1(58 ^ [firma_1_1, c595], c595), arg2(58 ^ [firma_1_1, c595], firma_1_1), subr(58 ^ [firma_1_1, c595], sub_0)],extension(7,bind([[_131695, _131696, _131694], [c595, firma_1_1, 58 ^ [firma_1_1, c595]]]))).
% 234.16/225.56 cnf('1.4.1',plain,[-(arg1(58 ^ [firma_1_1, c595], c595)), sub(c595, firma_1_1)],extension(4,bind([[_131709, _131710], [c595, firma_1_1]]))).
% 234.16/225.56 cnf('1.4.1.1',plain,[-(sub(c595, firma_1_1))],extension(6)).
% 234.16/225.56 cnf('1.4.2',plain,[-(arg2(58 ^ [firma_1_1, c595], firma_1_1)), sub(c595, firma_1_1)],extension(5,bind([[_131709, _131710], [c595, firma_1_1]]))).
% 234.16/225.56 cnf('1.4.2.1',plain,[-(sub(c595, firma_1_1))],extension(6)).
% 234.16/225.56 cnf('1.4.3',plain,[-(subr(58 ^ [firma_1_1, c595], sub_0)), sub(c595, firma_1_1)],extension(8,bind([[_131709, _131710], [c595, firma_1_1]]))).
% 234.16/225.56 cnf('1.4.3.1',plain,[-(sub(c595, firma_1_1))],extension(6)).
% 234.16/225.56 cnf('1.5',plain,[-(sub(c596, name_1_1))],extension(3)).
% 234.16/225.56 cnf('1.6',plain,[-(sub(c595, firma_1_1))],extension(6)).
% 234.16/225.56 cnf('1.7',plain,[-(sub(c596, name_1_1))],extension(3)).
% 234.16/225.56 cnf('1.8',plain,[-(val(c596, bmw_0))],extension(9)).
% 234.16/225.56 cnf('1.9',plain,[-(val(c596, bmw_0))],extension(9)).
% 234.16/225.56 %-----------------------------------------------------
% 234.16/225.57
% 234.16/225.57 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------