%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR114+23 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n020.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:34 EDT 2022
% Result : Theorem 5.96s 6.57s
% Output : Proof 5.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : CSR114+23 : TPTP v8.1.0. Released v4.0.0.
% 0.10/0.11 % Command : leancop_casc.sh %s %d
% 0.11/0.32 % Computer : n020.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 600
% 0.11/0.32 % DateTime : Thu Jun 9 19:09:36 EDT 2022
% 0.11/0.32 % CPUTime :
% 5.96/6.57 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.96/6.58 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.96/6.58
% 5.96/6.58 %-----------------------------------------------------
% 5.96/6.58 fof(synth_qa07_004_qapw_67, conjecture, ? [_1193256, _1193259, _1193262, _1193265, _1193268] : (in(_1193262, _1193256) & attr(_1193256, _1193259) & loc(_1193268, _1193262) & scar(_1193268, _1193265) & sub(_1193259, name_1_1) & sub(_1193256, stadt__1_1) & sub(_1193265, kolosseum_1_1) & subs(_1193268, stehen_1_1) & val(_1193259, rom_0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', synth_qa07_004_qapw_67)).
% 5.96/6.58 fof(ave07_era5_synth_qa07_004_qapw_67, hypothesis, agt(c11, c209) & ctxt(c11, c4) & loc(c11, c208) & subs(c11, spielen_1_2) & temp(c11, c178) & attr(c167, c168) & attr(c167, c169) & sub(c167, mensch_1_1) & sub(c168, eigenname_1_1) & val(c168, bryan_0) & sub(c169, familiename_1_1) & val(c169, adams_0) & attr(c178, c179) & attr(c178, c180) & attr(c178, c181) & sub(c179, tag_1_1) & val(c179, c175) & sub(c180, monat_1_1) & val(c180, c176) & sub(c181, jahr__1_1) & val(c181, c177) & loc(c185, c207) & pred(c185, zuschauer__1_1) & loc(c190, c206) & sub(c190, gratiskonzert_1_1) & loc(c196, c205) & sub(c196, kolosseum_1_1) & attr(c202, c203) & sub(c202, stadt__1_1) & sub(c203, name_1_1) & val(c203, rom_0) & in(c205, c202) & vor(c206, c196) & bei(c207, c190) & vor(c208, c185) & itms(c209, c13, c167) & agt(c210, c185) & subs(c210, zugucken_1_1) & subs(c4, abschlu__337_1_1) & attch(c8, c4) & subs(c8, europatour_1_1) & assoc(europatour_1_1, europa_0) & subs(europatour_1_1, tour_1_1) & assoc(gratiskonzert_1_1, gratis_1_1) & sub(gratiskonzert_1_1, konzert__1_1) & sort(c11, da) & fact(c11, real) & gener(c11, sp) & sort(c209, o) & card(c209, int2) & etype(c209, int1) & fact(c209, real) & gener(c209, sp) & quant(c209, nfquant) & refer(c209, det) & varia(c209, varia_c) & sort(c4, ad) & card(c4, int1) & etype(c4, int0) & fact(c4, real) & gener(c4, sp) & quant(c4, one) & refer(c4, det) & varia(c4, varia_c) & sort(c208, l) & card(c208, int500000) & etype(c208, int1) & fact(c208, real) & gener(c208, sp) & quant(c208, nfquant) & refer(c208, refer_c) & varia(c208, varia_c) & sort(spielen_1_2, da) & fact(spielen_1_2, real) & gener(spielen_1_2, ge) & sort(c178, t) & card(c178, int1) & etype(c178, int0) & fact(c178, real) & gener(c178, sp) & quant(c178, one) & refer(c178, det) & varia(c178, con) & sort(c167, d) & card(c167, int1) & etype(c167, int0) & fact(c167, real) & gener(c167, sp) & quant(c167, one) & refer(c167, det) & varia(c167, con) & sort(c168, na) & card(c168, int1) & etype(c168, int0) & fact(c168, real) & gener(c168, sp) & quant(c168, one) & refer(c168, indet) & varia(c168, varia_c) & sort(c169, na) & card(c169, int1) & etype(c169, int0) & fact(c169, real) & gener(c169, sp) & quant(c169, one) & refer(c169, indet) & varia(c169, varia_c) & sort(mensch_1_1, d) & card(mensch_1_1, int1) & etype(mensch_1_1, int0) & fact(mensch_1_1, real) & gener(mensch_1_1, ge) & quant(mensch_1_1, one) & refer(mensch_1_1, refer_c) & varia(mensch_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(bryan_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(adams_0, fe) & sort(c179, me) & sort(c179, oa) & sort(c179, ta) & card(c179, card_c) & etype(c179, etype_c) & fact(c179, real) & gener(c179, sp) & quant(c179, quant_c) & refer(c179, det) & varia(c179, varia_c) & sort(c180, me) & sort(c180, oa) & sort(c180, ta) & card(c180, card_c) & etype(c180, etype_c) & fact(c180, real) & gener(c180, sp) & quant(c180, quant_c) & refer(c180, det) & varia(c180, varia_c) & sort(c181, me) & sort(c181, oa) & sort(c181, ta) & card(c181, card_c) & etype(c181, etype_c) & fact(c181, real) & gener(c181, sp) & quant(c181, quant_c) & refer(c181, refer_c) & varia(c181, varia_c) & sort(tag_1_1, me) & sort(tag_1_1, oa) & sort(tag_1_1, ta) & card(tag_1_1, card_c) & etype(tag_1_1, etype_c) & fact(tag_1_1, real) & gener(tag_1_1, ge) & quant(tag_1_1, quant_c) & refer(tag_1_1, refer_c) & varia(tag_1_1, varia_c) & sort(c175, nu) & card(c175, int31) & sort(monat_1_1, me) & sort(monat_1_1, oa) & sort(monat_1_1, ta) & card(monat_1_1, card_c) & etype(monat_1_1, etype_c) & fact(monat_1_1, real) & gener(monat_1_1, ge) & quant(monat_1_1, quant_c) & refer(monat_1_1, refer_c) & varia(monat_1_1, varia_c) & sort(c176, nu) & card(c176, int7) & 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(c177, nu) & card(c177, int2006) & sort(c185, d) & card(c185, int500000) & etype(c185, int1) & fact(c185, real) & gener(c185, sp) & quant(c185, nfquant) & refer(c185, indet) & varia(c185, varia_c) & sort(c207, l) & card(c207, int1) & etype(c207, int0) & fact(c207, real) & gener(c207, sp) & quant(c207, one) & refer(c207, indet) & varia(c207, varia_c) & sort(zuschauer__1_1, d) & card(zuschauer__1_1, int1) & etype(zuschauer__1_1, int0) & fact(zuschauer__1_1, real) & gener(zuschauer__1_1, ge) & quant(zuschauer__1_1, one) & refer(zuschauer__1_1, refer_c) & varia(zuschauer__1_1, varia_c) & sort(c190, ad) & sort(c190, d) & sort(c190, io) & card(c190, int1) & etype(c190, int0) & fact(c190, real) & gener(c190, sp) & quant(c190, one) & refer(c190, indet) & varia(c190, varia_c) & sort(c206, l) & card(c206, int1) & etype(c206, int0) & fact(c206, real) & gener(c206, sp) & quant(c206, one) & refer(c206, det) & varia(c206, con) & sort(gratiskonzert_1_1, ad) & sort(gratiskonzert_1_1, d) & sort(gratiskonzert_1_1, io) & card(gratiskonzert_1_1, int1) & etype(gratiskonzert_1_1, int0) & fact(gratiskonzert_1_1, real) & gener(gratiskonzert_1_1, ge) & quant(gratiskonzert_1_1, one) & refer(gratiskonzert_1_1, refer_c) & varia(gratiskonzert_1_1, varia_c) & sort(c196, d) & card(c196, int1) & etype(c196, int0) & fact(c196, real) & gener(c196, sp) & quant(c196, one) & refer(c196, det) & varia(c196, con) & sort(c205, l) & card(c205, int1) & etype(c205, int0) & fact(c205, real) & gener(c205, sp) & quant(c205, one) & refer(c205, det) & varia(c205, 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(c202, d) & sort(c202, io) & card(c202, int1) & etype(c202, int0) & fact(c202, real) & gener(c202, sp) & quant(c202, one) & refer(c202, det) & varia(c202, con) & sort(c203, na) & card(c203, int1) & etype(c203, int0) & fact(c203, real) & gener(c203, sp) & quant(c203, one) & refer(c203, indet) & varia(c203, 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(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(c210, da) & fact(c210, real) & gener(c210, sp) & sort(zugucken_1_1, da) & fact(zugucken_1_1, real) & gener(zugucken_1_1, ge) & sort(abschlu__337_1_1, ad) & card(abschlu__337_1_1, int1) & etype(abschlu__337_1_1, int0) & fact(abschlu__337_1_1, real) & gener(abschlu__337_1_1, ge) & quant(abschlu__337_1_1, one) & refer(abschlu__337_1_1, refer_c) & varia(abschlu__337_1_1, varia_c) & sort(c8, ad) & card(c8, int1) & etype(c8, int0) & fact(c8, real) & gener(c8, sp) & quant(c8, one) & refer(c8, det) & varia(c8, con) & sort(europatour_1_1, ad) & card(europatour_1_1, int1) & etype(europatour_1_1, int0) & fact(europatour_1_1, real) & gener(europatour_1_1, ge) & quant(europatour_1_1, one) & refer(europatour_1_1, refer_c) & varia(europatour_1_1, varia_c) & sort(europa_0, fe) & sort(tour_1_1, ad) & card(tour_1_1, int1) & etype(tour_1_1, int0) & fact(tour_1_1, real) & gener(tour_1_1, ge) & quant(tour_1_1, one) & refer(tour_1_1, refer_c) & varia(tour_1_1, varia_c) & sort(gratis_1_1, gq) & 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), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ave07_era5_synth_qa07_004_qapw_67)).
% 5.96/6.58 fof(loc__stehen_1_1_loc, axiom, ! [_1198147, _1198150] : (loc(_1198147, _1198150) => ? [_1198168] : (loc(_1198168, _1198150) & scar(_1198168, _1198147) & subs(_1198168, stehen_1_1))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', loc__stehen_1_1_loc)).
% 5.96/6.58
% 5.96/6.58 cnf(1, plain, [in(_260998, _260996), attr(_260996, _260997), loc(_261000, _260998), scar(_261000, _260999), sub(_260997, name_1_1), sub(_260996, stadt__1_1), sub(_260999, kolosseum_1_1), subs(_261000, stehen_1_1), val(_260997, rom_0)], clausify(synth_qa07_004_qapw_67)).
% 5.96/6.58 cnf(2, plain, [-(loc(c196, c205))], clausify(ave07_era5_synth_qa07_004_qapw_67)).
% 5.96/6.58 cnf(3, plain, [-(sub(c196, kolosseum_1_1))], clausify(ave07_era5_synth_qa07_004_qapw_67)).
% 5.96/6.58 cnf(4, plain, [-(attr(c202, c203))], clausify(ave07_era5_synth_qa07_004_qapw_67)).
% 5.96/6.58 cnf(5, plain, [-(sub(c202, stadt__1_1))], clausify(ave07_era5_synth_qa07_004_qapw_67)).
% 5.96/6.58 cnf(6, plain, [-(sub(c203, name_1_1))], clausify(ave07_era5_synth_qa07_004_qapw_67)).
% 5.96/6.58 cnf(7, plain, [-(val(c203, rom_0))], clausify(ave07_era5_synth_qa07_004_qapw_67)).
% 5.96/6.58 cnf(8, plain, [-(in(c205, c202))], clausify(ave07_era5_synth_qa07_004_qapw_67)).
% 5.96/6.58 cnf(9, plain, [loc(_138079, _138080), -(loc(63 ^ [_138080, _138079], _138080))], clausify(loc__stehen_1_1_loc)).
% 5.96/6.58 cnf(10, plain, [loc(_138079, _138080), -(scar(63 ^ [_138080, _138079], _138079))], clausify(loc__stehen_1_1_loc)).
% 5.96/6.58 cnf(11, plain, [loc(_138079, _138080), -(subs(63 ^ [_138080, _138079], stehen_1_1))], clausify(loc__stehen_1_1_loc)).
% 5.96/6.58
% 5.96/6.58 cnf('1',plain,[in(c205, c202), attr(c202, c203), loc(63 ^ [c205, c196], c205), scar(63 ^ [c205, c196], c196), sub(c203, name_1_1), sub(c202, stadt__1_1), sub(c196, kolosseum_1_1), subs(63 ^ [c205, c196], stehen_1_1), val(c203, rom_0)],start(1,bind([[_260998, _260996, _260999, _261000, _260997], [c205, c202, c196, 63 ^ [c205, c196], c203]]))).
% 5.96/6.58 cnf('1.1',plain,[-(in(c205, c202))],extension(8)).
% 5.96/6.58 cnf('1.2',plain,[-(attr(c202, c203))],extension(4)).
% 5.96/6.58 cnf('1.3',plain,[-(loc(63 ^ [c205, c196], c205)), loc(c196, c205)],extension(9,bind([[_138079, _138080], [c196, c205]]))).
% 5.96/6.58 cnf('1.3.1',plain,[-(loc(c196, c205))],extension(2)).
% 5.96/6.58 cnf('1.4',plain,[-(scar(63 ^ [c205, c196], c196)), loc(c196, c205)],extension(10,bind([[_138079, _138080], [c196, c205]]))).
% 5.96/6.58 cnf('1.4.1',plain,[-(loc(c196, c205))],extension(2)).
% 5.96/6.58 cnf('1.5',plain,[-(sub(c203, name_1_1))],extension(6)).
% 5.96/6.58 cnf('1.6',plain,[-(sub(c202, stadt__1_1))],extension(5)).
% 5.96/6.58 cnf('1.7',plain,[-(sub(c196, kolosseum_1_1))],extension(3)).
% 5.96/6.58 cnf('1.8',plain,[-(subs(63 ^ [c205, c196], stehen_1_1)), loc(c196, c205)],extension(11,bind([[_138079, _138080], [c196, c205]]))).
% 5.96/6.58 cnf('1.8.1',plain,[-(loc(c196, c205))],extension(2)).
% 5.96/6.58 cnf('1.9',plain,[-(val(c203, rom_0))],extension(7)).
% 5.96/6.58 %-----------------------------------------------------
% 5.96/6.59
% 5.96/6.59 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------