%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR114+12 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n026.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:32 EDT 2022
% Result : Theorem 5.75s 6.60s
% Output : Proof 5.75s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : CSR114+12 : TPTP v8.1.0. Released v4.0.0.
% 0.07/0.12 % Command : leancop_casc.sh %s %d
% 0.13/0.34 % Computer : n026.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 : Sat Jun 11 09:26:04 EDT 2022
% 0.13/0.34 % CPUTime :
% 5.75/6.60 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.75/6.61 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.75/6.62
% 5.75/6.62 %-----------------------------------------------------
% 5.75/6.62 fof(synth_qa07_004_mira_wp_261, conjecture, ? [_425480, _425483, _425486, _425489, _425492] : (in(_425486, _425480) & attr(_425480, _425483) & loc(_425492, _425486) & scar(_425492, _425489) & sub(_425483, name_1_1) & sub(_425480, stadt__1_1) & sub(_425489, kolosseum_1_1) & subs(_425492, stehen_1_1) & val(_425483, rom_0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', synth_qa07_004_mira_wp_261)).
% 5.75/6.62 fof(ave07_era5_synth_qa07_004_mira_wp_261, hypothesis, agt(c4, c72) & caus(c4, c99) & obj(c4, c80) & subs(c4, machen_1_6) & sub(c72, stadt__1_1) & loc(c80, c98) & prop(c80, c84) & sub(c80, amphi_theater_1_1) & supl(c84, zweitgro__337_1_1, c85) & loc(c88, c97) & sub(c88, kolosseum_1_1) & attr(c94, c95) & sub(c94, stadt__1_1) & sub(c95, name_1_1) & val(c95, rom_0) & in(c97, c94) & hinter(c98, c88) & arg1(c99, c80) & arg2(c99, erw__344hnenswert_1_1) & subr(c99, prop_0) & sort(c4, da) & fact(c4, real) & gener(c4, sp) & sort(c72, d) & sort(c72, io) & card(c72, int1) & etype(c72, int0) & fact(c72, real) & gener(c72, sp) & quant(c72, one) & refer(c72, det) & varia(c72, con) & sort(c99, st) & fact(c99, real) & gener(c99, sp) & sort(c80, o) & card(c80, int1) & etype(c80, int0) & fact(c80, real) & gener(c80, sp) & quant(c80, one) & refer(c80, det) & varia(c80, con) & sort(machen_1_6, da) & fact(machen_1_6, real) & gener(machen_1_6, ge) & 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(c98, l) & card(c98, int1) & etype(c98, int0) & fact(c98, real) & gener(c98, sp) & quant(c98, one) & refer(c98, det) & varia(c98, con) & sort(c84, tq) & sort(amphi_theater_1_1, o) & card(amphi_theater_1_1, int1) & etype(amphi_theater_1_1, int0) & fact(amphi_theater_1_1, real) & gener(amphi_theater_1_1, ge) & quant(amphi_theater_1_1, one) & refer(amphi_theater_1_1, refer_c) & varia(amphi_theater_1_1, varia_c) & sort(zweitgro__337_1_1, mq) & sort(c85, o) & card(c85, card_c) & etype(c85, int1) & etype(c85, int2) & fact(c85, real) & gener(c85, gener_c) & quant(c85, quant_c) & refer(c85, refer_c) & varia(c85, varia_c) & sort(c88, d) & card(c88, int1) & etype(c88, int0) & fact(c88, real) & gener(c88, sp) & quant(c88, one) & refer(c88, det) & varia(c88, con) & sort(c97, l) & card(c97, int1) & etype(c97, int0) & fact(c97, real) & gener(c97, sp) & quant(c97, one) & refer(c97, det) & varia(c97, 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(c94, d) & sort(c94, io) & card(c94, int1) & etype(c94, int0) & fact(c94, real) & gener(c94, sp) & quant(c94, one) & refer(c94, det) & varia(c94, con) & sort(c95, na) & card(c95, int1) & etype(c95, int0) & fact(c95, real) & gener(c95, sp) & quant(c95, one) & refer(c95, indet) & varia(c95, 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(erw__344hnenswert_1_1, ql) & sort(prop_0, st) & fact(prop_0, real) & gener(prop_0, gener_c), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ave07_era5_synth_qa07_004_mira_wp_261)).
% 5.75/6.62 fof(loc__stehen_1_1_loc, axiom, ! [_427819, _427822] : (loc(_427819, _427822) => ? [_427840] : (loc(_427840, _427822) & scar(_427840, _427819) & subs(_427840, stehen_1_1))), file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax', loc__stehen_1_1_loc)).
% 5.75/6.62
% 5.75/6.62 cnf(1, plain, [in(_192162, _192160), attr(_192160, _192161), loc(_192164, _192162), scar(_192164, _192163), sub(_192161, name_1_1), sub(_192160, stadt__1_1), sub(_192163, kolosseum_1_1), subs(_192164, stehen_1_1), val(_192161, rom_0)], clausify(synth_qa07_004_mira_wp_261)).
% 5.75/6.62 cnf(2, plain, [-(loc(c88, c97))], clausify(ave07_era5_synth_qa07_004_mira_wp_261)).
% 5.75/6.62 cnf(3, plain, [-(sub(c88, kolosseum_1_1))], clausify(ave07_era5_synth_qa07_004_mira_wp_261)).
% 5.75/6.62 cnf(4, plain, [-(attr(c94, c95))], clausify(ave07_era5_synth_qa07_004_mira_wp_261)).
% 5.75/6.62 cnf(5, plain, [-(sub(c94, stadt__1_1))], clausify(ave07_era5_synth_qa07_004_mira_wp_261)).
% 5.75/6.62 cnf(6, plain, [-(sub(c95, name_1_1))], clausify(ave07_era5_synth_qa07_004_mira_wp_261)).
% 5.75/6.62 cnf(7, plain, [-(val(c95, rom_0))], clausify(ave07_era5_synth_qa07_004_mira_wp_261)).
% 5.75/6.62 cnf(8, plain, [-(in(c97, c94))], clausify(ave07_era5_synth_qa07_004_mira_wp_261)).
% 5.75/6.62 cnf(9, plain, [loc(_131686, _131687), -(loc(63 ^ [_131687, _131686], _131687))], clausify(loc__stehen_1_1_loc)).
% 5.75/6.62 cnf(10, plain, [loc(_131686, _131687), -(scar(63 ^ [_131687, _131686], _131686))], clausify(loc__stehen_1_1_loc)).
% 5.75/6.62 cnf(11, plain, [loc(_131686, _131687), -(subs(63 ^ [_131687, _131686], stehen_1_1))], clausify(loc__stehen_1_1_loc)).
% 5.75/6.62
% 5.75/6.62 cnf('1',plain,[in(c97, c94), attr(c94, c95), loc(63 ^ [c97, c88], c97), scar(63 ^ [c97, c88], c88), sub(c95, name_1_1), sub(c94, stadt__1_1), sub(c88, kolosseum_1_1), subs(63 ^ [c97, c88], stehen_1_1), val(c95, rom_0)],start(1,bind([[_192162, _192160, _192163, _192164, _192161], [c97, c94, c88, 63 ^ [c97, c88], c95]]))).
% 5.75/6.62 cnf('1.1',plain,[-(in(c97, c94))],extension(8)).
% 5.75/6.62 cnf('1.2',plain,[-(attr(c94, c95))],extension(4)).
% 5.75/6.62 cnf('1.3',plain,[-(loc(63 ^ [c97, c88], c97)), loc(c88, c97)],extension(9,bind([[_131686, _131687], [c88, c97]]))).
% 5.75/6.62 cnf('1.3.1',plain,[-(loc(c88, c97))],extension(2)).
% 5.75/6.62 cnf('1.4',plain,[-(scar(63 ^ [c97, c88], c88)), loc(c88, c97)],extension(10,bind([[_131686, _131687], [c88, c97]]))).
% 5.75/6.62 cnf('1.4.1',plain,[-(loc(c88, c97))],extension(2)).
% 5.75/6.62 cnf('1.5',plain,[-(sub(c95, name_1_1))],extension(6)).
% 5.75/6.62 cnf('1.6',plain,[-(sub(c94, stadt__1_1))],extension(5)).
% 5.75/6.62 cnf('1.7',plain,[-(sub(c88, kolosseum_1_1))],extension(3)).
% 5.75/6.62 cnf('1.8',plain,[-(subs(63 ^ [c97, c88], stehen_1_1)), loc(c88, c97)],extension(11,bind([[_131686, _131687], [c88, c97]]))).
% 5.75/6.62 cnf('1.8.1',plain,[-(loc(c88, c97))],extension(2)).
% 5.75/6.62 cnf('1.9',plain,[-(val(c95, rom_0))],extension(7)).
% 5.75/6.62 %-----------------------------------------------------
% 5.75/6.62
% 5.75/6.63 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------