%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR113+4 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n015.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:30 EDT 2022
% Result : Theorem 185.98s 179.61s
% Output : Proof 185.98s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : CSR113+4 : TPTP v8.1.0. Released v4.0.0.
% 0.06/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n015.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Sat Jun 11 11:46:05 EDT 2022
% 0.12/0.33 % CPUTime :
% 185.98/179.61 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 185.98/179.61 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 185.98/179.62
% 185.98/179.62 %-----------------------------------------------------
% 185.98/179.62 fof(synth_qa07_003_mira_news_499_a270, conjecture, ? [_484661, _484664, _484667, _484670] : (attr(_484664, _484661) & scar(_484667, _484670) & sub(_484661, name_1_1) & val(_484661, usa_0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', synth_qa07_003_mira_news_499_a270)).
% 185.98/179.62 fof(name_rel__attr_val_name_1_1, axiom, ! [_486493, _486496] : (name(_486496, _486493) => ? [_486514] : (attr(_486496, _486514) & sub(_486514, name_1_1) & val(_486514, _486493))), file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax', name_rel__attr_val_name_1_1)).
% 185.98/179.62 fof(member_second, axiom, ! [_487571, _487574, _487577] : (member(_487571, _487577) => member(_487571, cons(_487574, _487577))), file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax', member_second)).
% 185.98/179.62 fof(ave07_era5_synth_qa07_003_mira_news_499_a270, hypothesis, assoc(auftaktveranstaltung_1_1, auftakt_1_1) & sub(auftaktveranstaltung_1_1, event_1_1) & sub(c103, auftaktveranstaltung_1_1) & poss(c108, c103) & attr(c113, c114) & prop(c113, aktuell_1_1) & sub(c113, land_1_1) & sub(c114, name_1_1) & val(c114, usa_0) & sub(c115, regierung_1_1) & tupl_p7(c163, c86, c95, c97, c103, c113, c115) & sub(c86, freiheitsstatue_1_1) & attr(c95, c96) & sub(c95, stadt__1_1) & sub(c96, name_1_1) & val(c96, new_york_0) & assoc(freiheitsstatue_1_1, freiheit_1_1) & sub(freiheitsstatue_1_1, statue_1_1) & sort(auftaktveranstaltung_1_1, ad) & sort(auftaktveranstaltung_1_1, io) & card(auftaktveranstaltung_1_1, int1) & etype(auftaktveranstaltung_1_1, int0) & fact(auftaktveranstaltung_1_1, real) & gener(auftaktveranstaltung_1_1, ge) & quant(auftaktveranstaltung_1_1, one) & refer(auftaktveranstaltung_1_1, refer_c) & varia(auftaktveranstaltung_1_1, varia_c) & sort(auftakt_1_1, ad) & sort(auftakt_1_1, io) & card(auftakt_1_1, int1) & etype(auftakt_1_1, int0) & fact(auftakt_1_1, real) & gener(auftakt_1_1, ge) & quant(auftakt_1_1, one) & refer(auftakt_1_1, refer_c) & varia(auftakt_1_1, varia_c) & sort(event_1_1, ad) & sort(event_1_1, io) & card(event_1_1, int1) & etype(event_1_1, int0) & fact(event_1_1, real) & gener(event_1_1, ge) & quant(event_1_1, one) & refer(event_1_1, refer_c) & varia(event_1_1, varia_c) & sort(c103, ad) & sort(c103, io) & card(c103, int1) & etype(c103, int0) & fact(c103, real) & gener(c103, sp) & quant(c103, one) & refer(c103, det) & varia(c103, varia_c) & sort(c108, o) & card(c108, int1) & etype(c108, int0) & fact(c108, real) & gener(c108, sp) & quant(c108, one) & refer(c108, det) & varia(c108, varia_c) & sort(c113, d) & sort(c113, io) & card(c113, int1) & etype(c113, int0) & fact(c113, real) & gener(c113, sp) & quant(c113, one) & refer(c113, det) & varia(c113, con) & sort(c114, na) & card(c114, int1) & etype(c114, int0) & fact(c114, real) & gener(c114, sp) & quant(c114, one) & refer(c114, indet) & varia(c114, varia_c) & sort(aktuell_1_1, nq) & 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(usa_0, fe) & sort(c115, d) & sort(c115, io) & card(c115, int1) & etype(c115, int1) & fact(c115, real) & gener(c115, gener_c) & quant(c115, one) & refer(c115, refer_c) & varia(c115, varia_c) & sort(regierung_1_1, d) & sort(regierung_1_1, io) & card(regierung_1_1, card_c) & etype(regierung_1_1, int1) & fact(regierung_1_1, real) & gener(regierung_1_1, ge) & quant(regierung_1_1, quant_c) & refer(regierung_1_1, refer_c) & varia(regierung_1_1, varia_c) & sort(c163, ent) & card(c163, card_c) & etype(c163, etype_c) & fact(c163, real) & gener(c163, gener_c) & quant(c163, quant_c) & refer(c163, refer_c) & varia(c163, varia_c) & sort(c86, d) & card(c86, int1) & etype(c86, int0) & fact(c86, real) & gener(c86, sp) & quant(c86, one) & refer(c86, det) & varia(c86, con) & sort(c95, d) & sort(c95, io) & card(c95, int1) & etype(c95, int0) & fact(c95, real) & gener(c95, sp) & quant(c95, one) & refer(c95, det) & varia(c95, con) & sort(c97, o) & card(c97, int1) & etype(c97, int0) & fact(c97, real) & gener(c97, sp) & quant(c97, one) & refer(c97, det) & varia(c97, varia_c) & sort(freiheitsstatue_1_1, d) & card(freiheitsstatue_1_1, int1) & etype(freiheitsstatue_1_1, int0) & fact(freiheitsstatue_1_1, real) & gener(freiheitsstatue_1_1, ge) & quant(freiheitsstatue_1_1, one) & refer(freiheitsstatue_1_1, refer_c) & varia(freiheitsstatue_1_1, varia_c) & sort(c96, na) & card(c96, int1) & etype(c96, int0) & fact(c96, real) & gener(c96, sp) & quant(c96, one) & refer(c96, indet) & varia(c96, 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(new_york_0, fe) & sort(freiheit_1_1, as) & sort(freiheit_1_1, io) & card(freiheit_1_1, int1) & etype(freiheit_1_1, int0) & fact(freiheit_1_1, real) & gener(freiheit_1_1, ge) & quant(freiheit_1_1, one) & refer(freiheit_1_1, refer_c) & varia(freiheit_1_1, varia_c) & sort(statue_1_1, d) & card(statue_1_1, int1) & etype(statue_1_1, int0) & fact(statue_1_1, real) & gener(statue_1_1, ge) & quant(statue_1_1, one) & refer(statue_1_1, refer_c) & varia(statue_1_1, varia_c), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ave07_era5_synth_qa07_003_mira_news_499_a270)).
% 185.98/179.62 fof(attr_val_name_1_1__name_rel, axiom, ! [_495155, _495158, _495161] : (attr(_495161, _495155) & sub(_495155, name_1_1) & val(_495155, _495158) => name(_495161, _495158)), file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax', attr_val_name_1_1__name_rel)).
% 185.98/179.62 fof(attr_name__abk__374rzung_stehen_1_b_f__374r, axiom, ! [_497319, _497322, _497325] : (attr(_497325, _497319) & member(_497322, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil)))) & sub(_497319, _497322) => ? [_497384] : (mcont(_497384, _497325) & obj(_497384, _497325) & scar(_497384, _497325) & subs(_497384, stehen_1_b))), file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax', attr_name__abk__374rzung_stehen_1_b_f__374r)).
% 185.98/179.62 fof(member_first, axiom, ! [_497711, _497714] : member(_497711, cons(_497711, _497714)), file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax', member_first)).
% 185.98/179.62
% 185.98/179.62 cnf(1, plain, [attr(_192641, _192640), scar(_192642, _192643), sub(_192640, name_1_1), val(_192640, usa_0)], clausify(synth_qa07_003_mira_news_499_a270)).
% 185.98/179.62 cnf(2, plain, [name(_131961, _131960), -(sub(61 ^ [_131961, _131960], name_1_1))], clausify(name_rel__attr_val_name_1_1)).
% 185.98/179.62 cnf(3, plain, [member(_129517, _129519), -(member(_129517, cons(_129518, _129519)))], clausify(member_second)).
% 185.98/179.62 cnf(4, plain, [-(sub(c114, name_1_1))], clausify(ave07_era5_synth_qa07_003_mira_news_499_a270)).
% 185.98/179.62 cnf(5, plain, [-(val(c114, usa_0))], clausify(ave07_era5_synth_qa07_003_mira_news_499_a270)).
% 185.98/179.62 cnf(6, plain, [name(_131961, _131960), -(attr(_131961, 61 ^ [_131961, _131960]))], clausify(name_rel__attr_val_name_1_1)).
% 185.98/179.62 cnf(7, plain, [-(attr(c113, c114))], clausify(ave07_era5_synth_qa07_003_mira_news_499_a270)).
% 185.98/179.62 cnf(8, plain, [-(name(_131970, _131969)), attr(_131970, _131968), sub(_131968, name_1_1), val(_131968, _131969)], clausify(attr_val_name_1_1__name_rel)).
% 185.98/179.62 cnf(9, plain, [-(scar(52 ^ [_131604, _131603, _131602], _131604)), attr(_131604, _131602), member(_131603, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil)))), sub(_131602, _131603)], clausify(attr_name__abk__374rzung_stehen_1_b_f__374r)).
% 185.98/179.62 cnf(10, plain, [-(member(_129506, cons(_129506, _129507)))], clausify(member_first)).
% 185.98/179.62
% 185.98/179.62 cnf('1',plain,[attr(c113, c114), scar(52 ^ [c113, name_1_1, 61 ^ [c113, usa_0]], c113), sub(c114, name_1_1), val(c114, usa_0)],start(1,bind([[_192641, _192642, _192643, _192640], [c113, 52 ^ [c113, name_1_1, 61 ^ [c113, usa_0]], c113, c114]]))).
% 185.98/179.62 cnf('1.1',plain,[-(attr(c113, c114))],extension(7)).
% 185.98/179.62 cnf('1.2',plain,[-(scar(52 ^ [c113, name_1_1, 61 ^ [c113, usa_0]], c113)), attr(c113, 61 ^ [c113, usa_0]), member(name_1_1, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil)))), sub(61 ^ [c113, usa_0], name_1_1)],extension(9,bind([[_131604, _131602, _131603], [c113, 61 ^ [c113, usa_0], name_1_1]]))).
% 185.98/179.62 cnf('1.2.1',plain,[-(attr(c113, 61 ^ [c113, usa_0])), name(c113, usa_0)],extension(6,bind([[_131961, _131960], [c113, usa_0]]))).
% 185.98/179.62 cnf('1.2.1.1',plain,[-(name(c113, usa_0)), attr(c113, c114), sub(c114, name_1_1), val(c114, usa_0)],extension(8,bind([[_131970, _131968, _131969], [c113, c114, usa_0]]))).
% 185.98/179.62 cnf('1.2.1.1.1',plain,[-(attr(c113, c114))],extension(7)).
% 185.98/179.62 cnf('1.2.1.1.2',plain,[-(sub(c114, name_1_1))],extension(4)).
% 185.98/179.62 cnf('1.2.1.1.3',plain,[-(val(c114, usa_0))],extension(5)).
% 185.98/179.62 cnf('1.2.2',plain,[-(member(name_1_1, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil))))), member(name_1_1, cons(familiename_1_1, cons(name_1_1, nil)))],extension(3,bind([[_129518, _129517, _129519], [eigenname_1_1, name_1_1, cons(familiename_1_1, cons(name_1_1, nil))]]))).
% 185.98/179.62 cnf('1.2.2.1',plain,[-(member(name_1_1, cons(familiename_1_1, cons(name_1_1, nil)))), member(name_1_1, cons(name_1_1, nil))],extension(3,bind([[_129518, _129517, _129519], [familiename_1_1, name_1_1, cons(name_1_1, nil)]]))).
% 185.98/179.62 cnf('1.2.2.1.1',plain,[-(member(name_1_1, cons(name_1_1, nil)))],extension(10,bind([[_129506, _129507], [name_1_1, nil]]))).
% 185.98/179.62 cnf('1.2.3',plain,[-(sub(61 ^ [c113, usa_0], name_1_1)), name(c113, usa_0)],extension(2,bind([[_131961, _131960], [c113, usa_0]]))).
% 185.98/179.62 cnf('1.2.3.1',plain,[-(name(c113, usa_0)), attr(c113, c114), sub(c114, name_1_1), val(c114, usa_0)],extension(8,bind([[_131970, _131968, _131969], [c113, c114, usa_0]]))).
% 185.98/179.62 cnf('1.2.3.1.1',plain,[-(attr(c113, c114))],extension(7)).
% 185.98/179.62 cnf('1.2.3.1.2',plain,[-(sub(c114, name_1_1))],extension(4)).
% 185.98/179.62 cnf('1.2.3.1.3',plain,[-(val(c114, usa_0))],extension(5)).
% 185.98/179.62 cnf('1.3',plain,[-(sub(c114, name_1_1))],extension(4)).
% 185.98/179.62 cnf('1.4',plain,[-(val(c114, usa_0))],extension(5)).
% 185.98/179.62 %-----------------------------------------------------
% 185.98/179.62
% 185.98/179.63 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------