%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR115+62 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n022.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:49 EDT 2022
% Result : Theorem 114.04s 110.42s
% Output : Proof 114.04s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : CSR115+62 : TPTP v8.1.0. Released v4.0.0.
% 0.07/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.34 % Computer : n022.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Fri Jun 10 20:32:49 EDT 2022
% 0.13/0.35 % CPUTime :
% 114.04/110.42 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 114.04/110.43 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 114.04/110.44
% 114.04/110.44 %-----------------------------------------------------
% 114.04/110.44 fof(synth_qa07_007_mira_wp_469, conjecture, ? [_427952, _427955, _427958, _427961, _427964, _427967, _427970, _427973] : (agt(_427964, _427961) & attr(_427952, _427955) & attr(_427961, _427958) & attr(_427967, _427970) & has_card_leq(_427973, int1994) & sub(_427955, name_1_1) & sub(_427952, firma_1_1) & sub(_427958, name_1_1) & sub(_427970, jahr__1_1) & subs(_427964, n374bernehmen_1_1) & temp(_427964, _427967) & val(_427955, bmw_0) & val(_427958, bmw_0) & val(_427970, _427973)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', synth_qa07_007_mira_wp_469)).
% 114.04/110.44 fof(ave07_era5_synth_qa07_007_mira_wp_469, hypothesis, sub(c12, eisenbahn__1_1) & agt(c126, c128) & loc(c126, c132) & obj(c126, c26) & subs(c126, n374bernehmen_1_1) & temp(c126, c7) & attr(c128, c129) & sub(c128, firma_1_1) & sub(c129, name_1_1) & val(c129, bmw_0) & in(c132, c12) & aff(c16, c22) & attch(c16, c12) & subs(c16, deregulation_1_1) & pred(c22, unternehmen_1_1) & prop(c22, staatlich__1_1) & sub(c26, firma_1_1) & attr(c7, c8) & sub(c8, jahr__1_1) & val(c8, c4) & sort(c12, d) & card(c12, int1) & etype(c12, int0) & fact(c12, real) & gener(c12, sp) & quant(c12, one) & refer(c12, det) & varia(c12, con) & sort(eisenbahn__1_1, d) & card(eisenbahn__1_1, int1) & etype(eisenbahn__1_1, int0) & fact(eisenbahn__1_1, real) & gener(eisenbahn__1_1, ge) & quant(eisenbahn__1_1, one) & refer(eisenbahn__1_1, refer_c) & varia(eisenbahn__1_1, varia_c) & sort(c126, da) & fact(c126, real) & gener(c126, sp) & sort(c128, d) & sort(c128, io) & card(c128, int1) & etype(c128, int0) & fact(c128, real) & gener(c128, sp) & quant(c128, one) & refer(c128, det) & varia(c128, con) & sort(c132, l) & card(c132, int1) & etype(c132, int0) & fact(c132, real) & gener(c132, sp) & quant(c132, one) & refer(c132, det) & varia(c132, con) & sort(c26, d) & sort(c26, io) & card(c26, int1) & etype(c26, int0) & fact(c26, real) & gener(c26, sp) & quant(c26, one) & refer(c26, det) & varia(c26, con) & sort(n374bernehmen_1_1, da) & fact(n374bernehmen_1_1, real) & gener(n374bernehmen_1_1, ge) & sort(c7, t) & card(c7, int1) & etype(c7, int0) & fact(c7, real) & gener(c7, sp) & quant(c7, one) & refer(c7, det) & varia(c7, con) & sort(c129, na) & card(c129, int1) & etype(c129, int0) & fact(c129, real) & gener(c129, sp) & quant(c129, one) & refer(c129, indet) & varia(c129, 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(c16, ad) & card(c16, int1) & etype(c16, int0) & fact(c16, real) & gener(c16, sp) & quant(c16, one) & refer(c16, det) & varia(c16, con) & sort(c22, d) & sort(c22, io) & card(c22, cons(x_constant, cons(int1, nil))) & etype(c22, int1) & fact(c22, real) & gener(c22, sp) & quant(c22, mult) & refer(c22, indet) & varia(c22, varia_c) & sort(deregulation_1_1, ad) & card(deregulation_1_1, int1) & etype(deregulation_1_1, int0) & fact(deregulation_1_1, real) & gener(deregulation_1_1, ge) & quant(deregulation_1_1, one) & refer(deregulation_1_1, refer_c) & varia(deregulation_1_1, varia_c) & sort(unternehmen_1_1, d) & sort(unternehmen_1_1, io) & card(unternehmen_1_1, int1) & etype(unternehmen_1_1, int0) & fact(unternehmen_1_1, real) & gener(unternehmen_1_1, ge) & quant(unternehmen_1_1, one) & refer(unternehmen_1_1, refer_c) & varia(unternehmen_1_1, varia_c) & sort(staatlich__1_1, tq) & sort(c8, me) & sort(c8, oa) & sort(c8, ta) & card(c8, card_c) & etype(c8, etype_c) & fact(c8, real) & gener(c8, sp) & quant(c8, quant_c) & refer(c8, refer_c) & varia(c8, varia_c) & sort(jahr__1_1, me) & sort(jahr__1_1, oa) & sort(jahr__1_1, ta) & card(jahr__1_1, card_c) & etype(jahr__1_1, etype_c) & fact(jahr__1_1, real) & gener(jahr__1_1, ge) & quant(jahr__1_1, quant_c) & refer(jahr__1_1, refer_c) & varia(jahr__1_1, varia_c) & sort(c4, nu) & card(c4, int1994), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ave07_era5_synth_qa07_007_mira_wp_469)).
% 114.04/110.44 fof(has_card_eq, axiom, ! [_430431, _430434] : (card(_430431, _430434) => has_card_leq(_430431, _430434)), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', has_card_eq)).
% 114.04/110.44
% 114.04/110.44 cnf(1, plain, [agt(_192425, _192424), attr(_192421, _192422), attr(_192424, _192423), attr(_192426, _192427), has_card_leq(_192428, int1994), sub(_192422, name_1_1), sub(_192421, firma_1_1), sub(_192423, name_1_1), sub(_192427, jahr__1_1), subs(_192425, n374bernehmen_1_1), temp(_192425, _192426), val(_192422, bmw_0), val(_192423, bmw_0), val(_192427, _192428)], clausify(synth_qa07_007_mira_wp_469)).
% 114.04/110.44 cnf(2, plain, [-(agt(c126, c128))], clausify(ave07_era5_synth_qa07_007_mira_wp_469)).
% 114.04/110.44 cnf(3, plain, [-(subs(c126, n374bernehmen_1_1))], clausify(ave07_era5_synth_qa07_007_mira_wp_469)).
% 114.04/110.44 cnf(4, plain, [-(temp(c126, c7))], clausify(ave07_era5_synth_qa07_007_mira_wp_469)).
% 114.04/110.44 cnf(5, plain, [-(attr(c128, c129))], clausify(ave07_era5_synth_qa07_007_mira_wp_469)).
% 114.04/110.44 cnf(6, plain, [-(sub(c128, firma_1_1))], clausify(ave07_era5_synth_qa07_007_mira_wp_469)).
% 114.04/110.44 cnf(7, plain, [-(sub(c129, name_1_1))], clausify(ave07_era5_synth_qa07_007_mira_wp_469)).
% 114.04/110.44 cnf(8, plain, [-(val(c129, bmw_0))], clausify(ave07_era5_synth_qa07_007_mira_wp_469)).
% 114.04/110.44 cnf(9, plain, [-(attr(c7, c8))], clausify(ave07_era5_synth_qa07_007_mira_wp_469)).
% 114.04/110.44 cnf(10, plain, [-(sub(c8, jahr__1_1))], clausify(ave07_era5_synth_qa07_007_mira_wp_469)).
% 114.04/110.44 cnf(11, plain, [-(val(c8, c4))], clausify(ave07_era5_synth_qa07_007_mira_wp_469)).
% 114.04/110.44 cnf(12, plain, [-(card(c4, int1994))], clausify(ave07_era5_synth_qa07_007_mira_wp_469)).
% 114.04/110.44 cnf(13, plain, [card(_129569, _129570), -(has_card_leq(_129569, _129570))], clausify(has_card_eq)).
% 114.04/110.44
% 114.04/110.44 cnf('1',plain,[agt(c126, c128), attr(c128, c129), attr(c128, c129), attr(c7, c8), has_card_leq(c4, int1994), sub(c129, name_1_1), sub(c128, firma_1_1), sub(c129, name_1_1), sub(c8, jahr__1_1), subs(c126, n374bernehmen_1_1), temp(c126, c7), val(c129, bmw_0), val(c129, bmw_0), val(c8, c4)],start(1,bind([[_192424, _192421, _192425, _192426, _192422, _192423, _192427, _192428], [c128, c128, c126, c7, c129, c129, c8, c4]]))).
% 114.04/110.44 cnf('1.1',plain,[-(agt(c126, c128))],extension(2)).
% 114.04/110.44 cnf('1.2',plain,[-(attr(c128, c129))],extension(5)).
% 114.04/110.44 cnf('1.3',plain,[-(attr(c128, c129))],extension(5)).
% 114.04/110.44 cnf('1.4',plain,[-(attr(c7, c8))],extension(9)).
% 114.04/110.44 cnf('1.5',plain,[-(has_card_leq(c4, int1994)), card(c4, int1994)],extension(13,bind([[_129569, _129570], [c4, int1994]]))).
% 114.04/110.44 cnf('1.5.1',plain,[-(card(c4, int1994))],extension(12)).
% 114.04/110.44 cnf('1.6',plain,[-(sub(c129, name_1_1))],extension(7)).
% 114.04/110.44 cnf('1.7',plain,[-(sub(c128, firma_1_1))],extension(6)).
% 114.04/110.44 cnf('1.8',plain,[-(sub(c129, name_1_1))],extension(7)).
% 114.04/110.44 cnf('1.9',plain,[-(sub(c8, jahr__1_1))],extension(10)).
% 114.04/110.44 cnf('1.10',plain,[-(subs(c126, n374bernehmen_1_1))],extension(3)).
% 114.04/110.44 cnf('1.11',plain,[-(temp(c126, c7))],extension(4)).
% 114.04/110.44 cnf('1.12',plain,[-(val(c129, bmw_0))],extension(8)).
% 114.04/110.44 cnf('1.13',plain,[-(val(c129, bmw_0))],extension(8)).
% 114.04/110.44 cnf('1.14',plain,[-(val(c8, c4))],extension(11)).
% 114.04/110.44 %-----------------------------------------------------
% 114.04/110.44
% 114.04/110.44 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------