%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR114+29 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n018.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:36 EDT 2022
% Result : Theorem 5.93s 6.63s
% Output : Proof 6.00s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : CSR114+29 : TPTP v8.1.0. Released v4.0.0.
% 0.04/0.14 % Command : leancop_casc.sh %s %d
% 0.14/0.35 % Computer : n018.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 600
% 0.14/0.35 % DateTime : Fri Jun 10 03:16:24 EDT 2022
% 0.14/0.35 % CPUTime :
% 5.93/6.63 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.93/6.64 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.93/6.64
% 5.93/6.64 %-----------------------------------------------------
% 5.93/6.64 fof(synth_qa07_004_qn2_75_a281, conjecture, ? [_435747, _435750, _435753, _435756, _435759] : (in(_435753, _435747) & attr(_435747, _435750) & loc(_435759, _435753) & scar(_435759, _435756) & sub(_435750, name_1_1) & sub(_435747, stadt__1_1) & sub(_435756, kolosseum_1_1) & subs(_435759, stehen_1_1) & val(_435750, rom_0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', synth_qa07_004_qn2_75_a281)).
% 5.93/6.64 fof(ave07_era5_synth_qa07_004_qn2_75_a281, hypothesis, assoc(c10, c0) & assoc(c10, c130) & ctxt(c10, c171) & loc(c10, c170) & obj(c10, c150) & scar(c10, c127) & subs(c10, haben_1_1) & temp(c10, abend_2_1) & temp(c10, c135) & attr(c127, c128) & attr(c127, c129) & sub(c127, kirchenf__374rst_1_1) & sub(c128, eigenname_1_1) & val(c128, johannes_0) & sub(c129, familiename_1_1) & val(c129, paul_0) & sub(c135, freiertag_1_1) & loc(c140, c169) & sub(c140, kolosseum_1_1) & attr(c147, c148) & sub(c147, stadt__1_1) & sub(c148, name_1_1) & val(c148, rom_0) & prop(c150, althergebracht_1_1) & sub(c150, kreuzung_1_1) & in(c169, c147) & an(c170, c140) & subm(c171, c9) & pred(c9, gl__344ubig_2_1) & sub(kirchenf__374rst_1_1, mensch_1_1) & assoc(kreuzung_1_1, kreuz_1_1) & sub(kreuzung_1_1, weg_1_1) & chsp2(zelebrieren_1_1, c0) & sort(c10, st) & fact(c10, real) & gener(c10, sp) & sort(c0, tq) & sort(c130, oq) & card(c130, int2) & sort(c171, o) & card(c171, card_c) & etype(c171, int1) & fact(c171, real) & gener(c171, gener_c) & quant(c171, quant_c) & refer(c171, refer_c) & varia(c171, varia_c) & sort(c170, l) & card(c170, int1) & etype(c170, int0) & fact(c170, real) & gener(c170, sp) & quant(c170, one) & refer(c170, det) & varia(c170, con) & sort(c150, d) & card(c150, int1) & etype(c150, int0) & fact(c150, real) & gener(c150, sp) & quant(c150, one) & refer(c150, det) & varia(c150, con) & sort(c127, d) & card(c127, int1) & etype(c127, int0) & fact(c127, real) & gener(c127, sp) & quant(c127, one) & refer(c127, det) & varia(c127, con) & sort(haben_1_1, st) & fact(haben_1_1, real) & gener(haben_1_1, ge) & sort(abend_2_1, t) & card(abend_2_1, int1) & etype(abend_2_1, int0) & fact(abend_2_1, real) & gener(abend_2_1, sp) & quant(abend_2_1, one) & refer(abend_2_1, refer_c) & varia(abend_2_1, varia_c) & sort(c135, ta) & card(c135, int1) & etype(c135, int0) & fact(c135, real) & gener(c135, sp) & quant(c135, one) & refer(c135, det) & varia(c135, con) & sort(c128, na) & card(c128, int1) & etype(c128, int0) & fact(c128, real) & gener(c128, sp) & quant(c128, one) & refer(c128, indet) & varia(c128, varia_c) & 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(kirchenf__374rst_1_1, d) & card(kirchenf__374rst_1_1, int1) & etype(kirchenf__374rst_1_1, int0) & fact(kirchenf__374rst_1_1, real) & gener(kirchenf__374rst_1_1, ge) & quant(kirchenf__374rst_1_1, one) & refer(kirchenf__374rst_1_1, refer_c) & varia(kirchenf__374rst_1_1, varia_c) & sort(eigenname_1_1, na) & card(eigenname_1_1, int1) & etype(eigenname_1_1, int0) & fact(eigenname_1_1, real) & gener(eigenname_1_1, ge) & quant(eigenname_1_1, one) & refer(eigenname_1_1, refer_c) & varia(eigenname_1_1, varia_c) & sort(johannes_0, fe) & 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(paul_0, fe) & sort(freiertag_1_1, ta) & card(freiertag_1_1, int1) & etype(freiertag_1_1, int0) & fact(freiertag_1_1, real) & gener(freiertag_1_1, ge) & quant(freiertag_1_1, one) & refer(freiertag_1_1, refer_c) & varia(freiertag_1_1, varia_c) & sort(c140, d) & card(c140, int1) & etype(c140, int0) & fact(c140, real) & gener(c140, sp) & quant(c140, one) & refer(c140, det) & varia(c140, con) & sort(c169, l) & card(c169, int1) & etype(c169, int0) & fact(c169, real) & gener(c169, sp) & quant(c169, one) & refer(c169, det) & varia(c169, con) & sort(kolosseum_1_1, d) & card(kolosseum_1_1, int1) & etype(kolosseum_1_1, int0) & fact(kolosseum_1_1, real) & gener(kolosseum_1_1, sp) & quant(kolosseum_1_1, one) & refer(kolosseum_1_1, det) & varia(kolosseum_1_1, con) & sort(c147, d) & sort(c147, io) & card(c147, int1) & etype(c147, int0) & fact(c147, real) & gener(c147, sp) & quant(c147, one) & refer(c147, det) & varia(c147, con) & sort(c148, na) & card(c148, int1) & etype(c148, int0) & fact(c148, real) & gener(c148, sp) & quant(c148, one) & refer(c148, indet) & varia(c148, 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(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(rom_0, fe) & sort(althergebracht_1_1, nq) & sort(kreuzung_1_1, d) & card(kreuzung_1_1, int1) & etype(kreuzung_1_1, int0) & fact(kreuzung_1_1, real) & gener(kreuzung_1_1, ge) & quant(kreuzung_1_1, one) & refer(kreuzung_1_1, refer_c) & varia(kreuzung_1_1, varia_c) & sort(c9, o) & card(c9, cons(x_constant, cons(int1, nil))) & etype(c9, int1) & fact(c9, real) & gener(c9, gener_c) & quant(c9, mult) & refer(c9, indet) & varia(c9, varia_c) & sort(gl__344ubig_2_1, o) & card(gl__344ubig_2_1, int1) & etype(gl__344ubig_2_1, int0) & fact(gl__344ubig_2_1, real) & gener(gl__344ubig_2_1, ge) & quant(gl__344ubig_2_1, one) & refer(gl__344ubig_2_1, refer_c) & varia(gl__344ubig_2_1, varia_c) & sort(mensch_1_1, ent) & card(mensch_1_1, card_c) & etype(mensch_1_1, etype_c) & fact(mensch_1_1, real) & gener(mensch_1_1, gener_c) & quant(mensch_1_1, quant_c) & refer(mensch_1_1, refer_c) & varia(mensch_1_1, varia_c) & sort(kreuz_1_1, d) & sort(kreuz_1_1, io) & card(kreuz_1_1, int1) & etype(kreuz_1_1, int0) & fact(kreuz_1_1, real) & gener(kreuz_1_1, ge) & quant(kreuz_1_1, one) & refer(kreuz_1_1, refer_c) & varia(kreuz_1_1, varia_c) & sort(weg_1_1, d) & card(weg_1_1, int1) & etype(weg_1_1, int0) & fact(weg_1_1, real) & gener(weg_1_1, ge) & quant(weg_1_1, one) & refer(weg_1_1, refer_c) & varia(weg_1_1, varia_c) & sort(zelebrieren_1_1, da) & fact(zelebrieren_1_1, real) & gener(zelebrieren_1_1, ge), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ave07_era5_synth_qa07_004_qn2_75_a281)).
% 5.93/6.64 fof(loc__stehen_1_1_loc, axiom, ! [_439373, _439376] : (loc(_439373, _439376) => ? [_439394] : (loc(_439394, _439376) & scar(_439394, _439373) & subs(_439394, stehen_1_1))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', loc__stehen_1_1_loc)).
% 5.93/6.64
% 5.93/6.64 cnf(1, plain, [in(_193216, _193214), attr(_193214, _193215), loc(_193218, _193216), scar(_193218, _193217), sub(_193215, name_1_1), sub(_193214, stadt__1_1), sub(_193217, kolosseum_1_1), subs(_193218, stehen_1_1), val(_193215, rom_0)], clausify(synth_qa07_004_qn2_75_a281)).
% 5.93/6.64 cnf(2, plain, [-(loc(c140, c169))], clausify(ave07_era5_synth_qa07_004_qn2_75_a281)).
% 5.93/6.64 cnf(3, plain, [-(sub(c140, kolosseum_1_1))], clausify(ave07_era5_synth_qa07_004_qn2_75_a281)).
% 5.93/6.64 cnf(4, plain, [-(attr(c147, c148))], clausify(ave07_era5_synth_qa07_004_qn2_75_a281)).
% 5.93/6.64 cnf(5, plain, [-(sub(c147, stadt__1_1))], clausify(ave07_era5_synth_qa07_004_qn2_75_a281)).
% 5.93/6.64 cnf(6, plain, [-(sub(c148, name_1_1))], clausify(ave07_era5_synth_qa07_004_qn2_75_a281)).
% 5.93/6.64 cnf(7, plain, [-(val(c148, rom_0))], clausify(ave07_era5_synth_qa07_004_qn2_75_a281)).
% 5.93/6.64 cnf(8, plain, [-(in(c169, c147))], clausify(ave07_era5_synth_qa07_004_qn2_75_a281)).
% 5.93/6.64 cnf(9, plain, [loc(_132387, _132388), -(loc(63 ^ [_132388, _132387], _132388))], clausify(loc__stehen_1_1_loc)).
% 5.93/6.64 cnf(10, plain, [loc(_132387, _132388), -(scar(63 ^ [_132388, _132387], _132387))], clausify(loc__stehen_1_1_loc)).
% 5.93/6.64 cnf(11, plain, [loc(_132387, _132388), -(subs(63 ^ [_132388, _132387], stehen_1_1))], clausify(loc__stehen_1_1_loc)).
% 5.93/6.64
% 5.93/6.64 cnf('1',plain,[in(c169, c147), attr(c147, c148), loc(63 ^ [c169, c140], c169), scar(63 ^ [c169, c140], c140), sub(c148, name_1_1), sub(c147, stadt__1_1), sub(c140, kolosseum_1_1), subs(63 ^ [c169, c140], stehen_1_1), val(c148, rom_0)],start(1,bind([[_193216, _193214, _193217, _193218, _193215], [c169, c147, c140, 63 ^ [c169, c140], c148]]))).
% 5.93/6.64 cnf('1.1',plain,[-(in(c169, c147))],extension(8)).
% 5.93/6.64 cnf('1.2',plain,[-(attr(c147, c148))],extension(4)).
% 5.93/6.64 cnf('1.3',plain,[-(loc(63 ^ [c169, c140], c169)), loc(c140, c169)],extension(9,bind([[_132387, _132388], [c140, c169]]))).
% 5.93/6.64 cnf('1.3.1',plain,[-(loc(c140, c169))],extension(2)).
% 5.93/6.64 cnf('1.4',plain,[-(scar(63 ^ [c169, c140], c140)), loc(c140, c169)],extension(10,bind([[_132387, _132388], [c140, c169]]))).
% 5.93/6.64 cnf('1.4.1',plain,[-(loc(c140, c169))],extension(2)).
% 5.93/6.64 cnf('1.5',plain,[-(sub(c148, name_1_1))],extension(6)).
% 5.93/6.64 cnf('1.6',plain,[-(sub(c147, stadt__1_1))],extension(5)).
% 5.93/6.64 cnf('1.7',plain,[-(sub(c140, kolosseum_1_1))],extension(3)).
% 5.93/6.64 cnf('1.8',plain,[-(subs(63 ^ [c169, c140], stehen_1_1)), loc(c140, c169)],extension(11,bind([[_132387, _132388], [c140, c169]]))).
% 5.93/6.64 cnf('1.8.1',plain,[-(loc(c140, c169))],extension(2)).
% 5.93/6.64 cnf('1.9',plain,[-(val(c148, rom_0))],extension(7)).
% 5.93/6.64 %-----------------------------------------------------
% 6.00/6.65
% 6.00/6.65 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------