%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR115+88 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n014.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:54 EDT 2022
% Result : Theorem 223.28s 215.59s
% Output : Proof 223.28s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : CSR115+88 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.13 % Command : leancop_casc.sh %s %d
% 0.12/0.34 % Computer : n014.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:16:53 EDT 2022
% 0.12/0.34 % CPUTime :
% 223.28/215.59 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 223.28/215.60 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 223.28/215.60
% 223.28/215.60 %-----------------------------------------------------
% 223.28/215.60 fof(sub__bezeichnen_1_1_als, axiom, ! [_621827, _621830, _621833] : (arg1(_621827, _621830) & arg2(_621827, _621833) & subr(_621827, sub_0) => ? [_621871, _621874, _621877] : (arg1(_621874, _621830) & arg2(_621874, _621877) & hsit(_621827, _621871) & mcont(_621871, _621874) & obj(_621871, _621830) & sub(_621877, _621833) & subr(_621874, rprs_0) & subs(_621871, bezeichnen_1_1))), file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax', sub__bezeichnen_1_1_als)).
% 223.28/215.60 fof(ave07_era5_synth_qa07_007_mira_wp_510, hypothesis, sub(c150, firma_1_1) & attr(c155, c156) & sub(c155, mensch_1_1) & sub(c156, familiename_1_1) & val(c156, schulz_0) & pred(c159, e28_1_1) & subs(c164, touring_1_1) & pred(c167, version_1_1) & sub(c182, e28_1_1) & attr(c197, c198) & sub(c197, firma_1_1) & sub(c198, name_1_1) & val(c198, bmw_0) & tupl_p10(c318, c150, c155, c159, c164, c167, c172, c164, c182, c197) & sort(c150, d) & sort(c150, io) & card(c150, int1) & etype(c150, int0) & fact(c150, real) & gener(c150, sp) & quant(c150, one) & refer(c150, det) & varia(c150, 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(c155, d) & card(c155, int1) & etype(c155, int0) & fact(c155, real) & gener(c155, sp) & quant(c155, one) & refer(c155, det) & varia(c155, con) & sort(c156, na) & card(c156, int1) & etype(c156, int0) & fact(c156, real) & gener(c156, sp) & quant(c156, one) & refer(c156, indet) & varia(c156, 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(schulz_0, fe) & sort(c159, o) & card(c159, cons(x_constant, cons(int1, nil))) & etype(c159, int1) & fact(c159, real) & gener(c159, gener_c) & quant(c159, several) & refer(c159, refer_c) & varia(c159, varia_c) & sort(e28_1_1, o) & card(e28_1_1, int1) & etype(e28_1_1, int0) & fact(e28_1_1, real) & gener(e28_1_1, ge) & quant(e28_1_1, one) & refer(e28_1_1, refer_c) & varia(e28_1_1, varia_c) & sort(c164, ad) & card(c164, int1) & etype(c164, int0) & fact(c164, real) & gener(c164, gener_c) & quant(c164, one) & refer(c164, refer_c) & varia(c164, varia_c) & sort(touring_1_1, ad) & card(touring_1_1, int1) & etype(touring_1_1, int0) & fact(touring_1_1, real) & gener(touring_1_1, ge) & quant(touring_1_1, one) & refer(touring_1_1, refer_c) & varia(touring_1_1, varia_c) & sort(c167, d) & sort(c167, io) & card(c167, cons(x_constant, cons(int1, nil))) & etype(c167, int1) & fact(c167, real) & gener(c167, gener_c) & quant(c167, mult) & refer(c167, indet) & varia(c167, varia_c) & sort(version_1_1, d) & sort(version_1_1, io) & card(version_1_1, int1) & etype(version_1_1, int0) & fact(version_1_1, real) & gener(version_1_1, ge) & quant(version_1_1, one) & refer(version_1_1, refer_c) & varia(version_1_1, varia_c) & sort(c182, o) & card(c182, int1) & etype(c182, int0) & fact(c182, real) & gener(c182, sp) & quant(c182, one) & refer(c182, det) & varia(c182, con) & sort(c197, d) & sort(c197, io) & card(c197, int1) & etype(c197, int0) & fact(c197, real) & gener(c197, sp) & quant(c197, one) & refer(c197, det) & varia(c197, con) & sort(c198, na) & card(c198, int1) & etype(c198, int0) & fact(c198, real) & gener(c198, sp) & quant(c198, one) & refer(c198, indet) & varia(c198, 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(c318, ent) & card(c318, card_c) & etype(c318, etype_c) & fact(c318, real) & gener(c318, gener_c) & quant(c318, quant_c) & refer(c318, refer_c) & varia(c318, varia_c) & sort(c172, o) & card(c172, int1) & etype(c172, int0) & fact(c172, real) & gener(c172, sp) & quant(c172, one) & refer(c172, det) & varia(c172, varia_c), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ave07_era5_synth_qa07_007_mira_wp_510)).
% 223.28/215.60 fof(sub__sub_0_expansion, axiom, ! [_626733, _626736] : (sub(_626733, _626736) => ? [_626754] : (arg1(_626754, _626733) & arg2(_626754, _626736) & subr(_626754, sub_0))), file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax', sub__sub_0_expansion)).
% 223.28/215.60 fof(synth_qa07_007_mira_wp_510, conjecture, ? [_629924, _629927, _629930, _629933, _629936, _629939, _629942] : (attr(_629924, _629927) & attr(_629933, _629930) & attr(_629939, _629942) & obj(_629936, _629924) & sub(_629927, name_1_1) & sub(_629924, firma_1_1) & sub(_629930, name_1_1) & val(_629927, bmw_0) & val(_629930, bmw_0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', synth_qa07_007_mira_wp_510)).
% 223.28/215.60
% 223.28/215.60 cnf(1, plain, [-(106 ^ [_131544, _131543, _131542]), -(obj(103 ^ [_131544, _131543, _131542], _131543))], clausify(sub__bezeichnen_1_1_als)).
% 223.28/215.60 cnf(2, plain, [-(sub(c197, firma_1_1))], clausify(ave07_era5_synth_qa07_007_mira_wp_510)).
% 223.28/215.60 cnf(3, plain, [-(sub(c198, name_1_1))], clausify(ave07_era5_synth_qa07_007_mira_wp_510)).
% 223.28/215.60 cnf(4, plain, [106 ^ [_131544, _131543, _131542], arg1(_131542, _131543), arg2(_131542, _131544), subr(_131542, sub_0)], clausify(sub__bezeichnen_1_1_als)).
% 223.28/215.60 cnf(5, plain, [-(108 ^ [_131558, _131557]), -(arg1(107 ^ [_131558, _131557], _131557))], clausify(sub__sub_0_expansion)).
% 223.28/215.60 cnf(6, plain, [-(108 ^ [_131558, _131557]), -(subr(107 ^ [_131558, _131557], sub_0))], clausify(sub__sub_0_expansion)).
% 223.28/215.60 cnf(7, plain, [-(val(c198, bmw_0))], clausify(ave07_era5_synth_qa07_007_mira_wp_510)).
% 223.28/215.60 cnf(8, plain, [-(attr(c197, c198))], clausify(ave07_era5_synth_qa07_007_mira_wp_510)).
% 223.28/215.60 cnf(9, plain, [attr(_192475, _192476), attr(_192478, _192477), attr(_192480, _192481), obj(_192479, _192475), sub(_192476, name_1_1), sub(_192475, firma_1_1), sub(_192477, name_1_1), val(_192476, bmw_0), val(_192477, bmw_0)], clausify(synth_qa07_007_mira_wp_510)).
% 223.28/215.60 cnf(10, plain, [sub(_131557, _131558), 108 ^ [_131558, _131557]], clausify(sub__sub_0_expansion)).
% 223.28/215.60 cnf(11, plain, [-(108 ^ [_131558, _131557]), -(arg2(107 ^ [_131558, _131557], _131558))], clausify(sub__sub_0_expansion)).
% 223.28/215.60
% 223.28/215.60 cnf('1',plain,[attr(c197, c198), attr(c197, c198), attr(c197, c198), obj(103 ^ [firma_1_1, c197, 107 ^ [firma_1_1, c197]], c197), sub(c198, name_1_1), sub(c197, firma_1_1), sub(c198, name_1_1), val(c198, bmw_0), val(c198, bmw_0)],start(9,bind([[_192478, _192480, _192481, _192479, _192475, _192476, _192477], [c197, c197, c198, 103 ^ [firma_1_1, c197, 107 ^ [firma_1_1, c197]], c197, c198, c198]]))).
% 223.28/215.60 cnf('1.1',plain,[-(attr(c197, c198))],extension(8)).
% 223.28/215.60 cnf('1.2',plain,[-(attr(c197, c198))],extension(8)).
% 223.28/215.60 cnf('1.3',plain,[-(attr(c197, c198))],extension(8)).
% 223.28/215.60 cnf('1.4',plain,[-(obj(103 ^ [firma_1_1, c197, 107 ^ [firma_1_1, c197]], c197)), -(106 ^ [firma_1_1, c197, 107 ^ [firma_1_1, c197]])],extension(1,bind([[_131544, _131543, _131542], [firma_1_1, c197, 107 ^ [firma_1_1, c197]]]))).
% 223.28/215.60 cnf('1.4.1',plain,[106 ^ [firma_1_1, c197, 107 ^ [firma_1_1, c197]], arg1(107 ^ [firma_1_1, c197], c197), arg2(107 ^ [firma_1_1, c197], firma_1_1), subr(107 ^ [firma_1_1, c197], sub_0)],extension(4,bind([[_131543, _131544, _131542], [c197, firma_1_1, 107 ^ [firma_1_1, c197]]]))).
% 223.28/215.60 cnf('1.4.1.1',plain,[-(arg1(107 ^ [firma_1_1, c197], c197)), -(108 ^ [firma_1_1, c197])],extension(5,bind([[_131558, _131557], [firma_1_1, c197]]))).
% 223.28/215.60 cnf('1.4.1.1.1',plain,[108 ^ [firma_1_1, c197], sub(c197, firma_1_1)],extension(10,bind([[_131557, _131558], [c197, firma_1_1]]))).
% 223.28/215.60 cnf('1.4.1.1.1.1',plain,[-(sub(c197, firma_1_1))],extension(2)).
% 223.28/215.60 cnf('1.4.1.2',plain,[-(arg2(107 ^ [firma_1_1, c197], firma_1_1)), -(108 ^ [firma_1_1, c197])],extension(11,bind([[_131558, _131557], [firma_1_1, c197]]))).
% 223.28/215.60 cnf('1.4.1.2.1',plain,[108 ^ [firma_1_1, c197], sub(c197, firma_1_1)],extension(10,bind([[_131557, _131558], [c197, firma_1_1]]))).
% 223.28/215.60 cnf('1.4.1.2.1.1',plain,[-(sub(c197, firma_1_1))],extension(2)).
% 223.28/215.60 cnf('1.4.1.3',plain,[-(subr(107 ^ [firma_1_1, c197], sub_0)), -(108 ^ [firma_1_1, c197])],extension(6,bind([[_131558, _131557], [firma_1_1, c197]]))).
% 223.28/215.60 cnf('1.4.1.3.1',plain,[108 ^ [firma_1_1, c197], sub(c197, firma_1_1)],extension(10,bind([[_131557, _131558], [c197, firma_1_1]]))).
% 223.28/215.60 cnf('1.4.1.3.1.1',plain,[-(sub(c197, firma_1_1))],extension(2)).
% 223.28/215.60 cnf('1.5',plain,[-(sub(c198, name_1_1))],extension(3)).
% 223.28/215.60 cnf('1.6',plain,[-(sub(c197, firma_1_1))],extension(2)).
% 223.28/215.60 cnf('1.7',plain,[-(sub(c198, name_1_1))],extension(3)).
% 223.28/215.60 cnf('1.8',plain,[-(val(c198, bmw_0))],extension(7)).
% 223.28/215.60 cnf('1.9',plain,[-(val(c198, bmw_0))],extension(7)).
% 223.28/215.60 %-----------------------------------------------------
% 223.28/215.61
% 223.28/215.61 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------