%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR114+25 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n013.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:35 EDT 2022
% Result : Theorem 5.71s 6.57s
% Output : Proof 5.71s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : CSR114+25 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.13 % Command : leancop_casc.sh %s %d
% 0.12/0.34 % Computer : n013.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Sat Jun 11 03:34:14 EDT 2022
% 0.12/0.34 % CPUTime :
% 5.71/6.57 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.71/6.58 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.71/6.58
% 5.71/6.58 %-----------------------------------------------------
% 5.71/6.58 fof(synth_qa07_004_qapw_81, conjecture, ? [_432547, _432550, _432553, _432556, _432559] : (in(_432553, _432547) & attr(_432547, _432550) & loc(_432559, _432553) & scar(_432559, _432556) & sub(_432550, name_1_1) & sub(_432547, stadt__1_1) & sub(_432556, kolosseum_1_1) & subs(_432559, stehen_1_1) & val(_432550, rom_0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', synth_qa07_004_qapw_81)).
% 5.71/6.58 fof(ave07_era5_synth_qa07_004_qapw_81, hypothesis, chsp2(auskl__374geln_1_1, c0) & pred(c11, er_fahrung_1_1) & loc(c13125, c13134) & sub(c13125, kolosseum_1_1) & attr(c13131, c13132) & sub(c13131, stadt__1_1) & sub(c13132, name_1_1) & val(c13132, rom_0) & in(c13134, c13131) & pred(c20, bau_1_1) & assoc(c21, c20) & obj(c21, c11) & reas(c21, c24) & scar(c21, c4) & subs(c21, haben_1_1) & agt(c24, c9825) & benf(c24, c13125) & circ(c24, c9847) & mannr(c24, wie_1_1) & modl(c24, nicht_1_1) & obj(c24, c9837) & subs(c24, geben_1_4) & sub(c4, man_1_1) & prop(c9837, c0) & sub(c9837, technik__1_1) & preds(c9847, anlage_1_1) & prop(c9847, spaet_1_1) & attch(c9853, c9847) & subs(c9853, art_1_1) & sort(auskl__374geln_1_1, dn) & fact(auskl__374geln_1_1, real) & gener(auskl__374geln_1_1, ge) & sort(c0, tq) & sort(c11, as) & sort(c11, io) & card(c11, cons(x_constant, cons(int1, nil))) & etype(c11, int1) & fact(c11, nonreal) & gener(c11, sp) & quant(c11, mult) & refer(c11, indet) & varia(c11, varia_c) & sort(er_fahrung_1_1, as) & sort(er_fahrung_1_1, io) & card(er_fahrung_1_1, int1) & etype(er_fahrung_1_1, int0) & fact(er_fahrung_1_1, real) & gener(er_fahrung_1_1, ge) & quant(er_fahrung_1_1, one) & refer(er_fahrung_1_1, refer_c) & varia(er_fahrung_1_1, varia_c) & sort(c13125, d) & card(c13125, int1) & etype(c13125, int0) & fact(c13125, real) & gener(c13125, sp) & quant(c13125, one) & refer(c13125, det) & varia(c13125, con) & sort(c13134, l) & card(c13134, int1) & etype(c13134, int0) & fact(c13134, real) & gener(c13134, sp) & quant(c13134, one) & refer(c13134, det) & varia(c13134, 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(c13131, d) & sort(c13131, io) & card(c13131, int1) & etype(c13131, int0) & fact(c13131, real) & gener(c13131, sp) & quant(c13131, one) & refer(c13131, det) & varia(c13131, con) & sort(c13132, na) & card(c13132, int1) & etype(c13132, int0) & fact(c13132, real) & gener(c13132, sp) & quant(c13132, one) & refer(c13132, indet) & varia(c13132, 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(c20, d) & card(c20, cons(x_constant, cons(int1, nil))) & etype(c20, int1) & fact(c20, real) & gener(c20, sp) & quant(c20, mult) & refer(c20, det) & varia(c20, varia_c) & sort(bau_1_1, d) & card(bau_1_1, int1) & etype(bau_1_1, int0) & fact(bau_1_1, real) & gener(bau_1_1, ge) & quant(bau_1_1, one) & refer(bau_1_1, refer_c) & varia(bau_1_1, varia_c) & sort(c21, st) & fact(c21, real) & gener(c21, sp) & sort(c24, da) & fact(c24, real) & gener(c24, sp) & sort(c4, d) & card(c4, int1) & etype(c4, int0) & fact(c4, real) & gener(c4, ge) & quant(c4, one) & refer(c4, refer_c) & varia(c4, varia_c) & sort(haben_1_1, st) & fact(haben_1_1, real) & gener(haben_1_1, ge) & sort(c9825, o) & card(c9825, int1) & etype(c9825, int0) & fact(c9825, real) & gener(c9825, sp) & quant(c9825, one) & refer(c9825, det) & varia(c9825, varia_c) & sort(c9847, as) & card(c9847, cons(x_constant, cons(int1, nil))) & etype(c9847, int1) & fact(c9847, real) & gener(c9847, sp) & quant(c9847, mult) & refer(c9847, det) & varia(c9847, varia_c) & sort(wie_1_1, mq) & sort(nicht_1_1, md) & fact(nicht_1_1, real) & gener(nicht_1_1, gener_c) & sort(c9837, io) & card(c9837, int1) & etype(c9837, int0) & fact(c9837, real) & gener(c9837, sp) & quant(c9837, one) & refer(c9837, det) & varia(c9837, con) & sort(geben_1_4, da) & fact(geben_1_4, real) & gener(geben_1_4, ge) & sort(man_1_1, d) & card(man_1_1, int1) & etype(man_1_1, int0) & fact(man_1_1, real) & gener(man_1_1, ge) & quant(man_1_1, one) & refer(man_1_1, refer_c) & varia(man_1_1, varia_c) & sort(technik__1_1, io) & card(technik__1_1, int1) & etype(technik__1_1, int0) & fact(technik__1_1, real) & gener(technik__1_1, ge) & quant(technik__1_1, one) & refer(technik__1_1, refer_c) & varia(technik__1_1, varia_c) & sort(anlage_1_1, as) & card(anlage_1_1, int1) & etype(anlage_1_1, int0) & fact(anlage_1_1, real) & gener(anlage_1_1, ge) & quant(anlage_1_1, one) & refer(anlage_1_1, refer_c) & varia(anlage_1_1, varia_c) & sort(spaet_1_1, mq) & sort(c9853, ad) & card(c9853, int1) & etype(c9853, int1) & fact(c9853, real) & gener(c9853, sp) & quant(c9853, one) & refer(c9853, det) & varia(c9853, varia_c) & sort(art_1_1, ad) & card(art_1_1, card_c) & etype(art_1_1, int1) & fact(art_1_1, real) & gener(art_1_1, ge) & quant(art_1_1, quant_c) & refer(art_1_1, refer_c) & varia(art_1_1, varia_c), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ave07_era5_synth_qa07_004_qapw_81)).
% 5.71/6.58 fof(loc__stehen_1_1_loc, axiom, ! [_435794, _435797] : (loc(_435794, _435797) => ? [_435815] : (loc(_435815, _435797) & scar(_435815, _435794) & subs(_435815, stehen_1_1))), file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax', loc__stehen_1_1_loc)).
% 5.71/6.58
% 5.71/6.58 cnf(1, plain, [in(_192907, _192905), attr(_192905, _192906), loc(_192909, _192907), scar(_192909, _192908), sub(_192906, name_1_1), sub(_192905, stadt__1_1), sub(_192908, kolosseum_1_1), subs(_192909, stehen_1_1), val(_192906, rom_0)], clausify(synth_qa07_004_qapw_81)).
% 5.71/6.58 cnf(2, plain, [-(loc(c13125, c13134))], clausify(ave07_era5_synth_qa07_004_qapw_81)).
% 5.71/6.58 cnf(3, plain, [-(sub(c13125, kolosseum_1_1))], clausify(ave07_era5_synth_qa07_004_qapw_81)).
% 5.71/6.58 cnf(4, plain, [-(attr(c13131, c13132))], clausify(ave07_era5_synth_qa07_004_qapw_81)).
% 5.71/6.58 cnf(5, plain, [-(sub(c13131, stadt__1_1))], clausify(ave07_era5_synth_qa07_004_qapw_81)).
% 5.71/6.58 cnf(6, plain, [-(sub(c13132, name_1_1))], clausify(ave07_era5_synth_qa07_004_qapw_81)).
% 5.71/6.58 cnf(7, plain, [-(val(c13132, rom_0))], clausify(ave07_era5_synth_qa07_004_qapw_81)).
% 5.71/6.58 cnf(8, plain, [-(in(c13134, c13131))], clausify(ave07_era5_synth_qa07_004_qapw_81)).
% 5.71/6.58 cnf(9, plain, [loc(_132177, _132178), -(loc(63 ^ [_132178, _132177], _132178))], clausify(loc__stehen_1_1_loc)).
% 5.71/6.58 cnf(10, plain, [loc(_132177, _132178), -(scar(63 ^ [_132178, _132177], _132177))], clausify(loc__stehen_1_1_loc)).
% 5.71/6.58 cnf(11, plain, [loc(_132177, _132178), -(subs(63 ^ [_132178, _132177], stehen_1_1))], clausify(loc__stehen_1_1_loc)).
% 5.71/6.58
% 5.71/6.58 cnf('1',plain,[in(c13134, c13131), attr(c13131, c13132), loc(63 ^ [c13134, c13125], c13134), scar(63 ^ [c13134, c13125], c13125), sub(c13132, name_1_1), sub(c13131, stadt__1_1), sub(c13125, kolosseum_1_1), subs(63 ^ [c13134, c13125], stehen_1_1), val(c13132, rom_0)],start(1,bind([[_192907, _192905, _192908, _192909, _192906], [c13134, c13131, c13125, 63 ^ [c13134, c13125], c13132]]))).
% 5.71/6.58 cnf('1.1',plain,[-(in(c13134, c13131))],extension(8)).
% 5.71/6.58 cnf('1.2',plain,[-(attr(c13131, c13132))],extension(4)).
% 5.71/6.58 cnf('1.3',plain,[-(loc(63 ^ [c13134, c13125], c13134)), loc(c13125, c13134)],extension(9,bind([[_132177, _132178], [c13125, c13134]]))).
% 5.71/6.58 cnf('1.3.1',plain,[-(loc(c13125, c13134))],extension(2)).
% 5.71/6.58 cnf('1.4',plain,[-(scar(63 ^ [c13134, c13125], c13125)), loc(c13125, c13134)],extension(10,bind([[_132177, _132178], [c13125, c13134]]))).
% 5.71/6.58 cnf('1.4.1',plain,[-(loc(c13125, c13134))],extension(2)).
% 5.71/6.58 cnf('1.5',plain,[-(sub(c13132, name_1_1))],extension(6)).
% 5.71/6.58 cnf('1.6',plain,[-(sub(c13131, stadt__1_1))],extension(5)).
% 5.71/6.58 cnf('1.7',plain,[-(sub(c13125, kolosseum_1_1))],extension(3)).
% 5.71/6.58 cnf('1.8',plain,[-(subs(63 ^ [c13134, c13125], stehen_1_1)), loc(c13125, c13134)],extension(11,bind([[_132177, _132178], [c13125, c13134]]))).
% 5.71/6.58 cnf('1.8.1',plain,[-(loc(c13125, c13134))],extension(2)).
% 5.71/6.58 cnf('1.9',plain,[-(val(c13132, rom_0))],extension(7)).
% 5.71/6.58 %-----------------------------------------------------
% 5.71/6.59
% 5.71/6.59 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------