%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR115+87 : 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:54 EDT 2022
% Result : Theorem 235.45s 227.36s
% Output : Proof 235.45s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : CSR115+87 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.12 % Command : leancop_casc.sh %s %d
% 0.13/0.33 % Computer : n025.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 600
% 0.13/0.33 % DateTime : Sat Jun 11 04:37:52 EDT 2022
% 0.13/0.33 % CPUTime :
% 235.45/227.36 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 235.45/227.37 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 235.45/227.37
% 235.45/227.37 %-----------------------------------------------------
% 235.45/227.37 fof(ave07_era5_synth_qa07_007_mira_wp_508, hypothesis, attr(c109, c110) & sub(c109, firma_1_1) & sub(c110, name_1_1) & val(c110, porsche_0) & attr(c125, c126) & sub(c125, firma_1_1) & sub(c126, name_1_1) & val(c126, bmw_0) & tupl_p8(c222, c57, c58, c68, c73, c68, c109, c125) & pred(c57, zasada_1_1) & pred(c58, fabrikat_1_1) & attch(c63, c58) & sub(c63, firma_1_1) & attr(c68, c69) & sub(c68, stadt__1_1) & sub(c69, name_1_1) & val(c69, steyr_0) & attr(c73, c74) & sub(c73, mensch_1_1) & sub(c74, familiename_1_1) & val(c74, puch_0) & sort(c109, d) & sort(c109, io) & card(c109, int1) & etype(c109, int0) & fact(c109, real) & gener(c109, sp) & quant(c109, one) & refer(c109, det) & varia(c109, con) & sort(c110, na) & card(c110, int1) & etype(c110, int0) & fact(c110, real) & gener(c110, sp) & quant(c110, one) & refer(c110, indet) & varia(c110, 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(porsche_0, fe) & sort(c125, d) & sort(c125, io) & card(c125, int1) & etype(c125, int0) & fact(c125, real) & gener(c125, sp) & quant(c125, one) & refer(c125, det) & varia(c125, con) & sort(c126, na) & card(c126, int1) & etype(c126, int0) & fact(c126, real) & gener(c126, sp) & quant(c126, one) & refer(c126, indet) & varia(c126, varia_c) & sort(bmw_0, fe) & sort(c222, ent) & card(c222, card_c) & etype(c222, etype_c) & fact(c222, real) & gener(c222, gener_c) & quant(c222, quant_c) & refer(c222, refer_c) & varia(c222, varia_c) & sort(c57, o) & card(c57, cons(x_constant, cons(int1, nil))) & etype(c57, int1) & fact(c57, real) & gener(c57, gener_c) & quant(c57, mult) & refer(c57, indet) & varia(c57, varia_c) & sort(c58, o) & card(c58, cons(x_constant, cons(int1, nil))) & etype(c58, int1) & fact(c58, real) & gener(c58, sp) & quant(c58, mult) & refer(c58, indet) & varia(c58, varia_c) & sort(c68, d) & sort(c68, io) & card(c68, int1) & etype(c68, int0) & fact(c68, real) & gener(c68, sp) & quant(c68, one) & refer(c68, det) & varia(c68, con) & sort(c73, d) & card(c73, int1) & etype(c73, int0) & fact(c73, real) & gener(c73, sp) & quant(c73, one) & refer(c73, det) & varia(c73, con) & sort(zasada_1_1, o) & card(zasada_1_1, int1) & etype(zasada_1_1, int0) & fact(zasada_1_1, real) & gener(zasada_1_1, ge) & quant(zasada_1_1, one) & refer(zasada_1_1, refer_c) & varia(zasada_1_1, varia_c) & sort(fabrikat_1_1, o) & card(fabrikat_1_1, int1) & etype(fabrikat_1_1, int0) & fact(fabrikat_1_1, real) & gener(fabrikat_1_1, ge) & quant(fabrikat_1_1, one) & refer(fabrikat_1_1, refer_c) & varia(fabrikat_1_1, varia_c) & sort(c63, d) & sort(c63, io) & card(c63, int1) & etype(c63, int0) & fact(c63, real) & gener(c63, sp) & quant(c63, one) & refer(c63, det) & varia(c63, con) & sort(c69, na) & card(c69, int1) & etype(c69, int0) & fact(c69, real) & gener(c69, sp) & quant(c69, one) & refer(c69, indet) & varia(c69, 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(steyr_0, fe) & sort(c74, na) & card(c74, int1) & etype(c74, int0) & fact(c74, real) & gener(c74, sp) & quant(c74, one) & refer(c74, indet) & varia(c74, 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(puch_0, fe), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ave07_era5_synth_qa07_007_mira_wp_508)).
% 235.45/227.37 fof(sub__sub_0_expansion, axiom, ! [_617906, _617909] : (sub(_617906, _617909) => ? [_617927] : (arg1(_617927, _617906) & arg2(_617927, _617909) & subr(_617927, sub_0))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', sub__sub_0_expansion)).
% 235.45/227.37 fof(synth_qa07_007_mira_wp_508, conjecture, ? [_620763, _620766, _620769, _620772, _620775, _620778, _620781] : (attr(_620763, _620766) & attr(_620772, _620769) & attr(_620778, _620781) & obj(_620775, _620763) & sub(_620766, name_1_1) & sub(_620763, firma_1_1) & sub(_620769, name_1_1) & val(_620766, bmw_0) & val(_620769, bmw_0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', synth_qa07_007_mira_wp_508)).
% 235.45/227.37 fof(sub__bezeichnen_1_1_als, axiom, ! [_625683, _625686, _625689] : (arg1(_625683, _625686) & arg2(_625683, _625689) & subr(_625683, sub_0) => ? [_625727, _625730, _625733] : (arg1(_625730, _625686) & arg2(_625730, _625733) & hsit(_625683, _625727) & mcont(_625727, _625730) & obj(_625727, _625686) & sub(_625733, _625689) & subr(_625730, rprs_0) & subs(_625727, bezeichnen_1_1))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', sub__bezeichnen_1_1_als)).
% 235.45/227.37
% 235.45/227.37 cnf(1, plain, [-(attr(c125, c126))], clausify(ave07_era5_synth_qa07_007_mira_wp_508)).
% 235.45/227.37 cnf(2, plain, [-(sub(c125, firma_1_1))], clausify(ave07_era5_synth_qa07_007_mira_wp_508)).
% 235.45/227.37 cnf(3, plain, [-(sub(c126, name_1_1))], clausify(ave07_era5_synth_qa07_007_mira_wp_508)).
% 235.45/227.37 cnf(4, plain, [-(val(c126, bmw_0))], clausify(ave07_era5_synth_qa07_007_mira_wp_508)).
% 235.45/227.37 cnf(5, plain, [sub(_131665, _131666), -(arg1(58 ^ [_131666, _131665], _131665))], clausify(sub__sub_0_expansion)).
% 235.45/227.37 cnf(6, plain, [sub(_131665, _131666), -(arg2(58 ^ [_131666, _131665], _131666))], clausify(sub__sub_0_expansion)).
% 235.45/227.37 cnf(7, plain, [sub(_131665, _131666), -(subr(58 ^ [_131666, _131665], sub_0))], clausify(sub__sub_0_expansion)).
% 235.45/227.37 cnf(8, plain, [attr(_192635, _192636), attr(_192638, _192637), attr(_192640, _192641), obj(_192639, _192635), sub(_192636, name_1_1), sub(_192635, firma_1_1), sub(_192637, name_1_1), val(_192636, bmw_0), val(_192637, bmw_0)], clausify(synth_qa07_007_mira_wp_508)).
% 235.45/227.37 cnf(9, plain, [-(obj(55 ^ [_131652, _131651, _131650], _131651)), arg1(_131650, _131651), arg2(_131650, _131652), subr(_131650, sub_0)], clausify(sub__bezeichnen_1_1_als)).
% 235.45/227.37
% 235.45/227.37 cnf('1',plain,[attr(c125, c126), attr(c125, c126), attr(c125, c126), obj(55 ^ [firma_1_1, c125, 58 ^ [firma_1_1, c125]], c125), sub(c126, name_1_1), sub(c125, firma_1_1), sub(c126, name_1_1), val(c126, bmw_0), val(c126, bmw_0)],start(8,bind([[_192638, _192640, _192641, _192639, _192635, _192636, _192637], [c125, c125, c126, 55 ^ [firma_1_1, c125, 58 ^ [firma_1_1, c125]], c125, c126, c126]]))).
% 235.45/227.37 cnf('1.1',plain,[-(attr(c125, c126))],extension(1)).
% 235.45/227.37 cnf('1.2',plain,[-(attr(c125, c126))],extension(1)).
% 235.45/227.37 cnf('1.3',plain,[-(attr(c125, c126))],extension(1)).
% 235.45/227.37 cnf('1.4',plain,[-(obj(55 ^ [firma_1_1, c125, 58 ^ [firma_1_1, c125]], c125)), arg1(58 ^ [firma_1_1, c125], c125), arg2(58 ^ [firma_1_1, c125], firma_1_1), subr(58 ^ [firma_1_1, c125], sub_0)],extension(9,bind([[_131651, _131652, _131650], [c125, firma_1_1, 58 ^ [firma_1_1, c125]]]))).
% 235.45/227.37 cnf('1.4.1',plain,[-(arg1(58 ^ [firma_1_1, c125], c125)), sub(c125, firma_1_1)],extension(5,bind([[_131665, _131666], [c125, firma_1_1]]))).
% 235.45/227.37 cnf('1.4.1.1',plain,[-(sub(c125, firma_1_1))],extension(2)).
% 235.45/227.37 cnf('1.4.2',plain,[-(arg2(58 ^ [firma_1_1, c125], firma_1_1)), sub(c125, firma_1_1)],extension(6,bind([[_131665, _131666], [c125, firma_1_1]]))).
% 235.45/227.37 cnf('1.4.2.1',plain,[-(sub(c125, firma_1_1))],extension(2)).
% 235.45/227.37 cnf('1.4.3',plain,[-(subr(58 ^ [firma_1_1, c125], sub_0)), sub(c125, firma_1_1)],extension(7,bind([[_131665, _131666], [c125, firma_1_1]]))).
% 235.45/227.37 cnf('1.4.3.1',plain,[-(sub(c125, firma_1_1))],extension(2)).
% 235.45/227.37 cnf('1.5',plain,[-(sub(c126, name_1_1))],extension(3)).
% 235.45/227.37 cnf('1.6',plain,[-(sub(c125, firma_1_1))],extension(2)).
% 235.45/227.37 cnf('1.7',plain,[-(sub(c126, name_1_1))],extension(3)).
% 235.45/227.37 cnf('1.8',plain,[-(val(c126, bmw_0))],extension(4)).
% 235.45/227.37 cnf('1.9',plain,[-(val(c126, bmw_0))],extension(4)).
% 235.45/227.37 %-----------------------------------------------------
% 235.45/227.38
% 235.45/227.38 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------