%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR115+46 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n029.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:46 EDT 2022
% Result : Theorem 0.64s 1.42s
% Output : Proof 0.73s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : CSR115+46 : TPTP v8.1.0. Released v4.0.0.
% 0.07/0.13 % Command : leancop_casc.sh %s %d
% 0.12/0.34 % Computer : n029.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Sat Jun 11 08:40:23 EDT 2022
% 0.12/0.35 % CPUTime :
% 0.64/1.42 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.64/1.42 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.73/1.43
% 0.73/1.43 %-----------------------------------------------------
% 0.73/1.43 fof(synth_qa07_007_mira_news_1258, conjecture, ? [_429520, _429523, _429526, _429529, _429532, _429535, _429538] : (attr(_429520, _429523) & attr(_429529, _429526) & attr(_429535, _429538) & obj(_429532, _429520) & sub(_429523, name_1_1) & sub(_429520, firma_1_1) & sub(_429526, name_1_1) & val(_429523, bmw_0) & val(_429526, bmw_0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', synth_qa07_007_mira_news_1258)).
% 0.73/1.43 fof(ave07_era5_synth_qa07_007_mira_news_1258, hypothesis, assoc(autofirma_1_1, auto__1_1) & sub(autofirma_1_1, firma_1_1) & agt(c484, c893) & benf(c484, c858) & obj(c484, c902) & subs(c484, nehmen_1_7) & temp(c484, c865) & attr(c858, c859) & sub(c858, firma_1_1) & sub(c859, name_1_1) & val(c859, bmw_0) & prop(c865, pass__351_1_1) & sub(c865, sommer__1_1) & attr(c893, c894) & sub(c893, autofirma_1_1) & sub(c894, name_1_1) & val(c894, rover_0) & prop(c902, britisch__1_1) & prop(c902, unabh__344ngig_1_1) & sub(c902, c904) & pmod(c904, letzt_1_1, massenhersteller_1_1) & agt(c907, c902) & subs(c907, herstellen_1_1) & assoc(massenhersteller_1_1, masse_1_1) & sub(massenhersteller_1_1, fabrikant_1_1) & sort(autofirma_1_1, d) & sort(autofirma_1_1, io) & card(autofirma_1_1, int1) & etype(autofirma_1_1, int0) & fact(autofirma_1_1, real) & gener(autofirma_1_1, ge) & quant(autofirma_1_1, one) & refer(autofirma_1_1, refer_c) & varia(autofirma_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(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(c484, da) & fact(c484, real) & gener(c484, sp) & sort(c893, d) & sort(c893, io) & card(c893, int1) & etype(c893, int0) & fact(c893, real) & gener(c893, sp) & quant(c893, one) & refer(c893, det) & varia(c893, con) & sort(c858, d) & sort(c858, io) & card(c858, int1) & etype(c858, int0) & fact(c858, real) & gener(c858, sp) & quant(c858, one) & refer(c858, det) & varia(c858, con) & sort(c902, io) & card(c902, int1) & etype(c902, int0) & fact(c902, real) & gener(c902, sp) & quant(c902, one) & refer(c902, det) & varia(c902, con) & sort(nehmen_1_7, da) & fact(nehmen_1_7, real) & gener(nehmen_1_7, ge) & sort(c865, ta) & card(c865, int1) & etype(c865, int0) & fact(c865, real) & gener(c865, sp) & quant(c865, one) & refer(c865, det) & varia(c865, con) & sort(c859, na) & card(c859, int1) & etype(c859, int0) & fact(c859, real) & gener(c859, sp) & quant(c859, one) & refer(c859, indet) & varia(c859, 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(pass__351_1_1, tq) & sort(sommer__1_1, ta) & card(sommer__1_1, int1) & etype(sommer__1_1, int0) & fact(sommer__1_1, real) & gener(sommer__1_1, ge) & quant(sommer__1_1, one) & refer(sommer__1_1, refer_c) & varia(sommer__1_1, varia_c) & sort(c894, na) & card(c894, int1) & etype(c894, int0) & fact(c894, real) & gener(c894, sp) & quant(c894, one) & refer(c894, indet) & varia(c894, varia_c) & sort(rover_0, fe) & sort(britisch__1_1, nq) & sort(unabh__344ngig_1_1, nq) & sort(c904, d) & sort(c904, io) & card(c904, int1) & etype(c904, int0) & fact(c904, real) & gener(c904, ge) & quant(c904, one) & refer(c904, refer_c) & varia(c904, varia_c) & sort(letzt_1_1, oq) & card(letzt_1_1, card_c) & sort(massenhersteller_1_1, d) & sort(massenhersteller_1_1, io) & card(massenhersteller_1_1, int1) & etype(massenhersteller_1_1, int0) & fact(massenhersteller_1_1, real) & gener(massenhersteller_1_1, ge) & quant(massenhersteller_1_1, one) & refer(massenhersteller_1_1, refer_c) & varia(massenhersteller_1_1, varia_c) & sort(c907, da) & fact(c907, real) & gener(c907, sp) & sort(herstellen_1_1, da) & fact(herstellen_1_1, real) & gener(herstellen_1_1, ge) & sort(masse_1_1, io) & card(masse_1_1, card_c) & etype(masse_1_1, int1) & fact(masse_1_1, real) & gener(masse_1_1, ge) & quant(masse_1_1, quant_c) & refer(masse_1_1, refer_c) & varia(masse_1_1, varia_c) & sort(fabrikant_1_1, d) & sort(fabrikant_1_1, io) & card(fabrikant_1_1, int1) & etype(fabrikant_1_1, int0) & fact(fabrikant_1_1, real) & gener(fabrikant_1_1, ge) & quant(fabrikant_1_1, one) & refer(fabrikant_1_1, refer_c) & varia(fabrikant_1_1, varia_c), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ave07_era5_synth_qa07_007_mira_news_1258)).
% 0.73/1.43 fof(sub__bezeichnen_1_1_als, axiom, ! [_432181, _432184, _432187] : (arg1(_432181, _432184) & arg2(_432181, _432187) & subr(_432181, sub_0) => ? [_432225, _432228, _432231] : (arg1(_432228, _432184) & arg2(_432228, _432231) & hsit(_432181, _432225) & mcont(_432225, _432228) & obj(_432225, _432184) & sub(_432231, _432187) & subr(_432228, rprs_0) & subs(_432225, bezeichnen_1_1))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', sub__bezeichnen_1_1_als)).
% 0.73/1.43 fof(sub__sub_0_expansion, axiom, ! [_432645, _432648] : (sub(_432645, _432648) => ? [_432666] : (arg1(_432666, _432645) & arg2(_432666, _432648) & subr(_432666, sub_0))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', sub__sub_0_expansion)).
% 0.73/1.43
% 0.73/1.43 cnf(1, plain, [attr(_192487, _192488), attr(_192490, _192489), attr(_192492, _192493), obj(_192491, _192487), sub(_192488, name_1_1), sub(_192487, firma_1_1), sub(_192489, name_1_1), val(_192488, bmw_0), val(_192489, bmw_0)], clausify(synth_qa07_007_mira_news_1258)).
% 0.73/1.43 cnf(2, plain, [-(attr(c858, c859))], clausify(ave07_era5_synth_qa07_007_mira_news_1258)).
% 0.73/1.43 cnf(3, plain, [-(sub(c858, firma_1_1))], clausify(ave07_era5_synth_qa07_007_mira_news_1258)).
% 0.73/1.43 cnf(4, plain, [-(sub(c859, name_1_1))], clausify(ave07_era5_synth_qa07_007_mira_news_1258)).
% 0.73/1.43 cnf(5, plain, [-(val(c859, bmw_0))], clausify(ave07_era5_synth_qa07_007_mira_news_1258)).
% 0.73/1.43 cnf(6, plain, [-(obj(55 ^ [_131557, _131556, _131555], _131556)), arg1(_131555, _131556), arg2(_131555, _131557), subr(_131555, sub_0)], clausify(sub__bezeichnen_1_1_als)).
% 0.73/1.43 cnf(7, plain, [sub(_131570, _131571), -(arg1(58 ^ [_131571, _131570], _131570))], clausify(sub__sub_0_expansion)).
% 0.73/1.43 cnf(8, plain, [sub(_131570, _131571), -(arg2(58 ^ [_131571, _131570], _131571))], clausify(sub__sub_0_expansion)).
% 0.73/1.43 cnf(9, plain, [sub(_131570, _131571), -(subr(58 ^ [_131571, _131570], sub_0))], clausify(sub__sub_0_expansion)).
% 0.73/1.43
% 0.73/1.43 cnf('1',plain,[attr(c858, c859), attr(c858, c859), attr(c858, c859), obj(55 ^ [firma_1_1, c858, 58 ^ [firma_1_1, c858]], c858), sub(c859, name_1_1), sub(c858, firma_1_1), sub(c859, name_1_1), val(c859, bmw_0), val(c859, bmw_0)],start(1,bind([[_192490, _192492, _192493, _192491, _192487, _192488, _192489], [c858, c858, c859, 55 ^ [firma_1_1, c858, 58 ^ [firma_1_1, c858]], c858, c859, c859]]))).
% 0.73/1.43 cnf('1.1',plain,[-(attr(c858, c859))],extension(2)).
% 0.73/1.43 cnf('1.2',plain,[-(attr(c858, c859))],extension(2)).
% 0.73/1.43 cnf('1.3',plain,[-(attr(c858, c859))],extension(2)).
% 0.73/1.43 cnf('1.4',plain,[-(obj(55 ^ [firma_1_1, c858, 58 ^ [firma_1_1, c858]], c858)), arg1(58 ^ [firma_1_1, c858], c858), arg2(58 ^ [firma_1_1, c858], firma_1_1), subr(58 ^ [firma_1_1, c858], sub_0)],extension(6,bind([[_131556, _131557, _131555], [c858, firma_1_1, 58 ^ [firma_1_1, c858]]]))).
% 0.73/1.43 cnf('1.4.1',plain,[-(arg1(58 ^ [firma_1_1, c858], c858)), sub(c858, firma_1_1)],extension(7,bind([[_131570, _131571], [c858, firma_1_1]]))).
% 0.73/1.43 cnf('1.4.1.1',plain,[-(sub(c858, firma_1_1))],extension(3)).
% 0.73/1.43 cnf('1.4.2',plain,[-(arg2(58 ^ [firma_1_1, c858], firma_1_1)), sub(c858, firma_1_1)],extension(8,bind([[_131570, _131571], [c858, firma_1_1]]))).
% 0.73/1.43 cnf('1.4.2.1',plain,[-(sub(c858, firma_1_1))],extension(3)).
% 0.73/1.43 cnf('1.4.3',plain,[-(subr(58 ^ [firma_1_1, c858], sub_0)), sub(c858, firma_1_1)],extension(9,bind([[_131570, _131571], [c858, firma_1_1]]))).
% 0.73/1.43 cnf('1.4.3.1',plain,[-(sub(c858, firma_1_1))],extension(3)).
% 0.73/1.43 cnf('1.5',plain,[-(sub(c859, name_1_1))],extension(4)).
% 0.73/1.43 cnf('1.6',plain,[-(sub(c858, firma_1_1))],extension(3)).
% 0.73/1.43 cnf('1.7',plain,[-(sub(c859, name_1_1))],extension(4)).
% 0.73/1.43 cnf('1.8',plain,[-(val(c859, bmw_0))],extension(5)).
% 0.73/1.43 cnf('1.9',plain,[-(val(c859, bmw_0))],extension(5)).
% 0.73/1.43 %-----------------------------------------------------
% 0.73/1.43
% 0.73/1.44 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------