%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR114+3 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n012.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.91s 6.59s
% Output : Proof 5.91s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : CSR114+3 : TPTP v8.1.0. Released v4.0.0.
% 0.06/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.33 % Computer : n012.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.34 % DateTime : Sat Jun 11 13:40:26 EDT 2022
% 0.13/0.34 % CPUTime :
% 5.91/6.59 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.91/6.59 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.91/6.60
% 5.91/6.60 %-----------------------------------------------------
% 5.91/6.60 fof(synth_qa07_004_insicht_2, conjecture, ? [_437606, _437609, _437612, _437615, _437618] : (in(_437612, _437606) & attr(_437606, _437609) & loc(_437618, _437612) & scar(_437618, _437615) & sub(_437609, name_1_1) & sub(_437606, stadt__1_1) & sub(_437615, kolosseum_1_1) & subs(_437618, stehen_1_1) & val(_437609, rom_0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', synth_qa07_004_insicht_2)).
% 5.91/6.60 fof(ave07_era5_synth_qa07_004_insicht_2, hypothesis, attch(c13, c9) & attr(c20, c21) & sub(c20, land_1_1) & sub(c21, name_1_1) & val(c21, schweiz_0) & sub(c25, sohn_1_1) & agt(c3, c9) & assoc(c3, c25) & dircl(c3, c37) & loc(c3, retro_1_1) & origl(c3, c38) & subs(c3, gehen_1_1) & temp(c3, c4) & attr(c34, c35) & sub(c34, land_1_1) & sub(c35, name_1_1) & val(c35, italien_0) & flp(c37, c34) & flp(c38, c20) & obj(c384, c389) & subs(c384, aufnehmen_1_1) & loc(c389, c403) & sub(c389, konzert__1_1) & loc(c393, c402) & sub(c393, kolosseum_1_1) & attr(c399, c400) & sub(c399, stadt__1_1) & attr(c4, c5) & sub(c400, name_1_1) & val(c400, rom_0) & in(c402, c399) & in(c403, c393) & sub(c5, jahr__1_1) & val(c5, c1) & pred(c9, eltern_1_1) & sort(c13, o) & card(c13, int1) & etype(c13, int0) & fact(c13, real) & gener(c13, sp) & quant(c13, one) & refer(c13, det) & varia(c13, varia_c) & sort(c9, d) & card(c9, cons(x_constant, cons(int1, nil))) & etype(c9, int1) & fact(c9, real) & gener(c9, sp) & quant(c9, mult) & refer(c9, det) & varia(c9, varia_c) & sort(c20, d) & sort(c20, io) & card(c20, int1) & etype(c20, int0) & fact(c20, real) & gener(c20, sp) & quant(c20, one) & refer(c20, det) & varia(c20, con) & sort(c21, na) & card(c21, int1) & etype(c21, int0) & fact(c21, real) & gener(c21, sp) & quant(c21, one) & refer(c21, indet) & varia(c21, varia_c) & sort(land_1_1, d) & sort(land_1_1, io) & card(land_1_1, int1) & etype(land_1_1, int0) & fact(land_1_1, real) & gener(land_1_1, ge) & quant(land_1_1, one) & refer(land_1_1, refer_c) & varia(land_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(schweiz_0, fe) & sort(c25, d) & card(c25, int1) & etype(c25, int0) & fact(c25, real) & gener(c25, sp) & quant(c25, one) & refer(c25, det) & varia(c25, con) & sort(sohn_1_1, d) & card(sohn_1_1, int1) & etype(sohn_1_1, int0) & fact(sohn_1_1, real) & gener(sohn_1_1, ge) & quant(sohn_1_1, one) & refer(sohn_1_1, refer_c) & varia(sohn_1_1, varia_c) & sort(c3, da) & fact(c3, real) & gener(c3, sp) & sort(c37, l) & card(c37, int1) & etype(c37, int0) & fact(c37, real) & gener(c37, sp) & quant(c37, one) & refer(c37, det) & varia(c37, con) & sort(retro_1_1, l) & card(retro_1_1, int1) & etype(retro_1_1, int0) & fact(retro_1_1, real) & gener(retro_1_1, sp) & quant(retro_1_1, one) & refer(retro_1_1, refer_c) & varia(retro_1_1, varia_c) & sort(c38, l) & card(c38, int1) & etype(c38, int0) & fact(c38, real) & gener(c38, sp) & quant(c38, one) & refer(c38, det) & varia(c38, con) & sort(gehen_1_1, da) & fact(gehen_1_1, real) & gener(gehen_1_1, ge) & sort(c4, t) & card(c4, int1) & etype(c4, int0) & fact(c4, real) & gener(c4, sp) & quant(c4, one) & refer(c4, det) & varia(c4, con) & sort(c34, d) & sort(c34, io) & card(c34, int1) & etype(c34, int0) & fact(c34, real) & gener(c34, sp) & quant(c34, one) & refer(c34, det) & varia(c34, con) & sort(c35, na) & card(c35, int1) & etype(c35, int0) & fact(c35, real) & gener(c35, sp) & quant(c35, one) & refer(c35, indet) & varia(c35, varia_c) & sort(italien_0, fe) & sort(c384, dn) & fact(c384, real) & gener(c384, sp) & sort(c389, ad) & sort(c389, d) & sort(c389, io) & card(c389, int1) & etype(c389, int0) & fact(c389, real) & gener(c389, sp) & quant(c389, one) & refer(c389, det) & varia(c389, con) & sort(aufnehmen_1_1, dn) & fact(aufnehmen_1_1, real) & gener(aufnehmen_1_1, ge) & sort(c403, l) & card(c403, int1) & etype(c403, int0) & fact(c403, real) & gener(c403, sp) & quant(c403, one) & refer(c403, det) & varia(c403, con) & sort(konzert__1_1, ad) & sort(konzert__1_1, d) & sort(konzert__1_1, io) & card(konzert__1_1, int1) & etype(konzert__1_1, int0) & fact(konzert__1_1, real) & gener(konzert__1_1, ge) & quant(konzert__1_1, one) & refer(konzert__1_1, refer_c) & varia(konzert__1_1, varia_c) & sort(c393, d) & card(c393, int1) & etype(c393, int0) & fact(c393, real) & gener(c393, sp) & quant(c393, one) & refer(c393, det) & varia(c393, con) & sort(c402, l) & card(c402, int1) & etype(c402, int0) & fact(c402, real) & gener(c402, sp) & quant(c402, one) & refer(c402, det) & varia(c402, 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(c399, d) & sort(c399, io) & card(c399, int1) & etype(c399, int0) & fact(c399, real) & gener(c399, sp) & quant(c399, one) & refer(c399, det) & varia(c399, con) & sort(c400, na) & card(c400, int1) & etype(c400, int0) & fact(c400, real) & gener(c400, sp) & quant(c400, one) & refer(c400, indet) & varia(c400, 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(c5, me) & sort(c5, oa) & sort(c5, ta) & card(c5, card_c) & etype(c5, etype_c) & fact(c5, real) & gener(c5, sp) & quant(c5, quant_c) & refer(c5, refer_c) & varia(c5, varia_c) & sort(rom_0, fe) & 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(c1, nu) & card(c1, int1970) & sort(eltern_1_1, d) & card(eltern_1_1, int1) & etype(eltern_1_1, int0) & fact(eltern_1_1, real) & gener(eltern_1_1, ge) & quant(eltern_1_1, one) & refer(eltern_1_1, refer_c) & varia(eltern_1_1, varia_c), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ave07_era5_synth_qa07_004_insicht_2)).
% 5.91/6.60 fof(loc__stehen_1_1_loc, axiom, ! [_441463, _441466] : (loc(_441463, _441466) => ? [_441484] : (loc(_441484, _441466) & scar(_441484, _441463) & subs(_441484, stehen_1_1))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', loc__stehen_1_1_loc)).
% 5.91/6.60
% 5.91/6.60 cnf(1, plain, [in(_193405, _193403), attr(_193403, _193404), loc(_193407, _193405), scar(_193407, _193406), sub(_193404, name_1_1), sub(_193403, stadt__1_1), sub(_193406, kolosseum_1_1), subs(_193407, stehen_1_1), val(_193404, rom_0)], clausify(synth_qa07_004_insicht_2)).
% 5.91/6.60 cnf(2, plain, [-(loc(c393, c402))], clausify(ave07_era5_synth_qa07_004_insicht_2)).
% 5.91/6.60 cnf(3, plain, [-(sub(c393, kolosseum_1_1))], clausify(ave07_era5_synth_qa07_004_insicht_2)).
% 5.91/6.60 cnf(4, plain, [-(attr(c399, c400))], clausify(ave07_era5_synth_qa07_004_insicht_2)).
% 5.91/6.60 cnf(5, plain, [-(sub(c399, stadt__1_1))], clausify(ave07_era5_synth_qa07_004_insicht_2)).
% 5.91/6.60 cnf(6, plain, [-(sub(c400, name_1_1))], clausify(ave07_era5_synth_qa07_004_insicht_2)).
% 5.91/6.60 cnf(7, plain, [-(val(c400, rom_0))], clausify(ave07_era5_synth_qa07_004_insicht_2)).
% 5.91/6.60 cnf(8, plain, [-(in(c402, c399))], clausify(ave07_era5_synth_qa07_004_insicht_2)).
% 5.91/6.60 cnf(9, plain, [loc(_132513, _132514), -(loc(63 ^ [_132514, _132513], _132514))], clausify(loc__stehen_1_1_loc)).
% 5.91/6.60 cnf(10, plain, [loc(_132513, _132514), -(scar(63 ^ [_132514, _132513], _132513))], clausify(loc__stehen_1_1_loc)).
% 5.91/6.60 cnf(11, plain, [loc(_132513, _132514), -(subs(63 ^ [_132514, _132513], stehen_1_1))], clausify(loc__stehen_1_1_loc)).
% 5.91/6.60
% 5.91/6.60 cnf('1',plain,[in(c402, c399), attr(c399, c400), loc(63 ^ [c402, c393], c402), scar(63 ^ [c402, c393], c393), sub(c400, name_1_1), sub(c399, stadt__1_1), sub(c393, kolosseum_1_1), subs(63 ^ [c402, c393], stehen_1_1), val(c400, rom_0)],start(1,bind([[_193405, _193403, _193406, _193407, _193404], [c402, c399, c393, 63 ^ [c402, c393], c400]]))).
% 5.91/6.60 cnf('1.1',plain,[-(in(c402, c399))],extension(8)).
% 5.91/6.60 cnf('1.2',plain,[-(attr(c399, c400))],extension(4)).
% 5.91/6.60 cnf('1.3',plain,[-(loc(63 ^ [c402, c393], c402)), loc(c393, c402)],extension(9,bind([[_132513, _132514], [c393, c402]]))).
% 5.91/6.60 cnf('1.3.1',plain,[-(loc(c393, c402))],extension(2)).
% 5.91/6.60 cnf('1.4',plain,[-(scar(63 ^ [c402, c393], c393)), loc(c393, c402)],extension(10,bind([[_132513, _132514], [c393, c402]]))).
% 5.91/6.60 cnf('1.4.1',plain,[-(loc(c393, c402))],extension(2)).
% 5.91/6.60 cnf('1.5',plain,[-(sub(c400, name_1_1))],extension(6)).
% 5.91/6.60 cnf('1.6',plain,[-(sub(c399, stadt__1_1))],extension(5)).
% 5.91/6.60 cnf('1.7',plain,[-(sub(c393, kolosseum_1_1))],extension(3)).
% 5.91/6.60 cnf('1.8',plain,[-(subs(63 ^ [c402, c393], stehen_1_1)), loc(c393, c402)],extension(11,bind([[_132513, _132514], [c393, c402]]))).
% 5.91/6.60 cnf('1.8.1',plain,[-(loc(c393, c402))],extension(2)).
% 5.91/6.60 cnf('1.9',plain,[-(val(c400, rom_0))],extension(7)).
% 5.91/6.60 %-----------------------------------------------------
% 5.91/6.60
% 5.91/6.61 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------