%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR115+44 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n032.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:45 EDT 2022
% Result : Theorem 0.53s 1.36s
% Output : Proof 0.60s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.10 % Problem : CSR115+44 : TPTP v8.1.0. Released v4.0.0.
% 0.10/0.11 % Command : leancop_casc.sh %s %d
% 0.10/0.29 % Computer : n032.cluster.edu
% 0.10/0.29 % Model : x86_64 x86_64
% 0.10/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.29 % Memory : 8042.1875MB
% 0.10/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.30 % CPULimit : 300
% 0.10/0.30 % WCLimit : 600
% 0.10/0.30 % DateTime : Sat Jun 11 09:06:09 EDT 2022
% 0.10/0.30 % CPUTime :
% 0.53/1.36 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.53/1.37 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.60/1.37
% 0.60/1.37 %-----------------------------------------------------
% 0.60/1.37 fof(synth_qa07_007_mira_news_1253, conjecture, ? [_431726, _431729, _431732, _431735, _431738, _431741, _431744] : (attr(_431726, _431729) & attr(_431735, _431732) & attr(_431741, _431744) & obj(_431738, _431726) & sub(_431729, name_1_1) & sub(_431726, firma_1_1) & sub(_431732, name_1_1) & val(_431729, bmw_0) & val(_431732, bmw_0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', synth_qa07_007_mira_news_1253)).
% 0.60/1.37 fof(ave07_era5_synth_qa07_007_mira_news_1253, hypothesis, attr(c557, c558) & sub(c557, firma_1_1) & sub(c558, name_1_1) & val(c558, bmw_0) & attr(c564, c565) & sub(c564, mensch_1_1) & sub(c565, familiename_1_1) & val(c565, roll_0) & attr(c570, c571) & sub(c570, mensch_1_1) & sub(c571, familiename_1_1) & val(c571, royce_0) & pred(c572, kei_1_1) & subs(c573, einstieg_1_1) & prop(c582, britisch__1_1) & sub(c582, nobelfirma_1_1) & attr(c590, c591) & sub(c590, stadt__1_1) & sub(c591, name_1_1) & val(c591, london_0) & tupl_p8(c699, c557, c564, c570, c572, c573, c582, c590) & assoc(nobelfirma_1_1, gro__337m__374tig_1_1) & sub(nobelfirma_1_1, firma_1_1) & sort(c557, d) & sort(c557, io) & card(c557, int1) & etype(c557, int0) & fact(c557, real) & gener(c557, sp) & quant(c557, one) & refer(c557, det) & varia(c557, con) & sort(c558, na) & card(c558, int1) & etype(c558, int0) & fact(c558, real) & gener(c558, sp) & quant(c558, one) & refer(c558, indet) & varia(c558, 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(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(c564, d) & card(c564, int1) & etype(c564, int0) & fact(c564, real) & gener(c564, sp) & quant(c564, one) & refer(c564, det) & varia(c564, con) & sort(c565, na) & card(c565, int1) & etype(c565, int0) & fact(c565, real) & gener(c565, sp) & quant(c565, one) & refer(c565, indet) & varia(c565, 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(c570, d) & card(c570, int1) & etype(c570, int0) & fact(c570, real) & gener(c570, sp) & quant(c570, one) & refer(c570, det) & varia(c570, con) & sort(c571, na) & card(c571, int1) & etype(c571, int0) & fact(c571, real) & gener(c571, sp) & quant(c571, one) & refer(c571, indet) & varia(c571, varia_c) & sort(royce_0, fe) & sort(c572, o) & card(c572, cons(x_constant, cons(int1, nil))) & etype(c572, int1) & fact(c572, real) & gener(c572, gener_c) & quant(c572, mult) & refer(c572, indet) & varia(c572, varia_c) & sort(kei_1_1, o) & card(kei_1_1, int1) & etype(kei_1_1, int0) & fact(kei_1_1, real) & gener(kei_1_1, ge) & quant(kei_1_1, one) & refer(kei_1_1, refer_c) & varia(kei_1_1, varia_c) & sort(c573, ad) & card(c573, int1) & etype(c573, int0) & fact(c573, real) & gener(c573, gener_c) & quant(c573, one) & refer(c573, refer_c) & varia(c573, varia_c) & sort(einstieg_1_1, ad) & card(einstieg_1_1, int1) & etype(einstieg_1_1, int0) & fact(einstieg_1_1, real) & gener(einstieg_1_1, ge) & quant(einstieg_1_1, one) & refer(einstieg_1_1, refer_c) & varia(einstieg_1_1, varia_c) & sort(c582, d) & sort(c582, io) & card(c582, int1) & etype(c582, int0) & fact(c582, real) & gener(c582, sp) & quant(c582, one) & refer(c582, det) & varia(c582, con) & sort(britisch__1_1, nq) & sort(nobelfirma_1_1, d) & sort(nobelfirma_1_1, io) & card(nobelfirma_1_1, int1) & etype(nobelfirma_1_1, int0) & fact(nobelfirma_1_1, real) & gener(nobelfirma_1_1, ge) & quant(nobelfirma_1_1, one) & refer(nobelfirma_1_1, refer_c) & varia(nobelfirma_1_1, varia_c) & sort(c590, d) & sort(c590, io) & card(c590, int1) & etype(c590, int0) & fact(c590, real) & gener(c590, sp) & quant(c590, one) & refer(c590, det) & varia(c590, con) & sort(c591, na) & card(c591, int1) & etype(c591, int0) & fact(c591, real) & gener(c591, sp) & quant(c591, one) & refer(c591, indet) & varia(c591, 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(london_0, fe) & sort(c699, ent) & card(c699, card_c) & etype(c699, etype_c) & fact(c699, real) & gener(c699, gener_c) & quant(c699, quant_c) & refer(c699, refer_c) & varia(c699, varia_c) & sort(gro__337m__374tig_1_1, nq), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ave07_era5_synth_qa07_007_mira_news_1253)).
% 0.60/1.37 fof(sub__bezeichnen_1_1_als, axiom, ! [_434680, _434683, _434686] : (arg1(_434680, _434683) & arg2(_434680, _434686) & subr(_434680, sub_0) => ? [_434724, _434727, _434730] : (arg1(_434727, _434683) & arg2(_434727, _434730) & hsit(_434680, _434724) & mcont(_434724, _434727) & obj(_434724, _434683) & sub(_434730, _434686) & subr(_434727, rprs_0) & subs(_434724, bezeichnen_1_1))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', sub__bezeichnen_1_1_als)).
% 0.60/1.37 fof(sub__sub_0_expansion, axiom, ! [_435144, _435147] : (sub(_435144, _435147) => ? [_435165] : (arg1(_435165, _435144) & arg2(_435165, _435147) & subr(_435165, sub_0))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', sub__sub_0_expansion)).
% 0.60/1.37
% 0.60/1.37 cnf(1, plain, [attr(_192725, _192726), attr(_192728, _192727), attr(_192730, _192731), obj(_192729, _192725), sub(_192726, name_1_1), sub(_192725, firma_1_1), sub(_192727, name_1_1), val(_192726, bmw_0), val(_192727, bmw_0)], clausify(synth_qa07_007_mira_news_1253)).
% 0.60/1.37 cnf(2, plain, [-(attr(c557, c558))], clausify(ave07_era5_synth_qa07_007_mira_news_1253)).
% 0.60/1.37 cnf(3, plain, [-(sub(c557, firma_1_1))], clausify(ave07_era5_synth_qa07_007_mira_news_1253)).
% 0.60/1.37 cnf(4, plain, [-(sub(c558, name_1_1))], clausify(ave07_era5_synth_qa07_007_mira_news_1253)).
% 0.60/1.37 cnf(5, plain, [-(val(c558, bmw_0))], clausify(ave07_era5_synth_qa07_007_mira_news_1253)).
% 0.60/1.37 cnf(6, plain, [-(obj(55 ^ [_131712, _131711, _131710], _131711)), arg1(_131710, _131711), arg2(_131710, _131712), subr(_131710, sub_0)], clausify(sub__bezeichnen_1_1_als)).
% 0.60/1.37 cnf(7, plain, [sub(_131725, _131726), -(arg1(58 ^ [_131726, _131725], _131725))], clausify(sub__sub_0_expansion)).
% 0.60/1.37 cnf(8, plain, [sub(_131725, _131726), -(arg2(58 ^ [_131726, _131725], _131726))], clausify(sub__sub_0_expansion)).
% 0.60/1.37 cnf(9, plain, [sub(_131725, _131726), -(subr(58 ^ [_131726, _131725], sub_0))], clausify(sub__sub_0_expansion)).
% 0.60/1.37
% 0.60/1.37 cnf('1',plain,[attr(c557, c558), attr(c557, c558), attr(c557, c558), obj(55 ^ [firma_1_1, c557, 58 ^ [firma_1_1, c557]], c557), sub(c558, name_1_1), sub(c557, firma_1_1), sub(c558, name_1_1), val(c558, bmw_0), val(c558, bmw_0)],start(1,bind([[_192728, _192730, _192731, _192729, _192725, _192726, _192727], [c557, c557, c558, 55 ^ [firma_1_1, c557, 58 ^ [firma_1_1, c557]], c557, c558, c558]]))).
% 0.60/1.37 cnf('1.1',plain,[-(attr(c557, c558))],extension(2)).
% 0.60/1.37 cnf('1.2',plain,[-(attr(c557, c558))],extension(2)).
% 0.60/1.37 cnf('1.3',plain,[-(attr(c557, c558))],extension(2)).
% 0.60/1.37 cnf('1.4',plain,[-(obj(55 ^ [firma_1_1, c557, 58 ^ [firma_1_1, c557]], c557)), arg1(58 ^ [firma_1_1, c557], c557), arg2(58 ^ [firma_1_1, c557], firma_1_1), subr(58 ^ [firma_1_1, c557], sub_0)],extension(6,bind([[_131711, _131712, _131710], [c557, firma_1_1, 58 ^ [firma_1_1, c557]]]))).
% 0.60/1.37 cnf('1.4.1',plain,[-(arg1(58 ^ [firma_1_1, c557], c557)), sub(c557, firma_1_1)],extension(7,bind([[_131725, _131726], [c557, firma_1_1]]))).
% 0.60/1.37 cnf('1.4.1.1',plain,[-(sub(c557, firma_1_1))],extension(3)).
% 0.60/1.37 cnf('1.4.2',plain,[-(arg2(58 ^ [firma_1_1, c557], firma_1_1)), sub(c557, firma_1_1)],extension(8,bind([[_131725, _131726], [c557, firma_1_1]]))).
% 0.60/1.37 cnf('1.4.2.1',plain,[-(sub(c557, firma_1_1))],extension(3)).
% 0.60/1.37 cnf('1.4.3',plain,[-(subr(58 ^ [firma_1_1, c557], sub_0)), sub(c557, firma_1_1)],extension(9,bind([[_131725, _131726], [c557, firma_1_1]]))).
% 0.60/1.37 cnf('1.4.3.1',plain,[-(sub(c557, firma_1_1))],extension(3)).
% 0.60/1.37 cnf('1.5',plain,[-(sub(c558, name_1_1))],extension(4)).
% 0.60/1.37 cnf('1.6',plain,[-(sub(c557, firma_1_1))],extension(3)).
% 0.60/1.37 cnf('1.7',plain,[-(sub(c558, name_1_1))],extension(4)).
% 0.60/1.37 cnf('1.8',plain,[-(val(c558, bmw_0))],extension(5)).
% 0.60/1.37 cnf('1.9',plain,[-(val(c558, bmw_0))],extension(5)).
% 0.60/1.37 %-----------------------------------------------------
% 0.60/1.38
% 0.60/1.38 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------