%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR113+5 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n008.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:31 EDT 2022
% Result : Theorem 186.96s 180.32s
% Output : Proof 186.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : CSR113+5 : TPTP v8.1.0. Released v4.0.0.
% 0.08/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.34 % Computer : n008.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:04:52 EDT 2022
% 0.13/0.35 % CPUTime :
% 186.96/180.32 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 186.96/180.33 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 186.96/180.34
% 186.96/180.34 %-----------------------------------------------------
% 186.96/180.34 fof(member_second, axiom, ! [_462955, _462958, _462961] : (member(_462955, _462961) => member(_462955, cons(_462958, _462961))), file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax', member_second)).
% 186.96/180.34 fof(ave07_era5_synth_qa07_003_mira_news_508, hypothesis, sub(c61153, freiheitsstatue_1_1) & attch(c61204, c61207) & sub(c61207, fackel_1_1) & sub(c61214, lilie_1_1) & sub(c61231, sich_1_1) & pred(c61236, alkoholfahne_1_1) & attch(c61243, c61236) & attr(c61243, c61244) & sub(c61243, land_1_1) & sub(c61244, name_1_1) & val(c61244, usa_0) & attr(c61248, c61249) & sub(c61248, gebiet_1_1) & sub(c61249, name_1_1) & val(c61249, bosnien_0) & sub(c61250, herzegowina_1_1) & tupl_p9(c62887, c61153, c61207, c61214, c61228, c61231, c61236, c61248, c61250) & assoc(freiheitsstatue_1_1, freiheit_1_1) & sub(freiheitsstatue_1_1, statue_1_1) & sort(c61153, d) & card(c61153, int1) & etype(c61153, int0) & fact(c61153, real) & gener(c61153, sp) & quant(c61153, one) & refer(c61153, det) & varia(c61153, con) & 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(c61204, o) & card(c61204, int1) & etype(c61204, int0) & fact(c61204, real) & gener(c61204, sp) & quant(c61204, one) & refer(c61204, det) & varia(c61204, varia_c) & sort(c61207, d) & card(c61207, int1) & etype(c61207, int0) & fact(c61207, real) & gener(c61207, sp) & quant(c61207, one) & refer(c61207, det) & varia(c61207, varia_c) & sort(fackel_1_1, d) & card(fackel_1_1, int1) & etype(fackel_1_1, int0) & fact(fackel_1_1, real) & gener(fackel_1_1, ge) & quant(fackel_1_1, one) & refer(fackel_1_1, refer_c) & varia(fackel_1_1, varia_c) & sort(c61214, d) & card(c61214, int1) & etype(c61214, int0) & fact(c61214, real) & gener(c61214, sp) & quant(c61214, one) & refer(c61214, indet) & varia(c61214, varia_c) & sort(lilie_1_1, d) & card(lilie_1_1, int1) & etype(lilie_1_1, int0) & fact(lilie_1_1, real) & gener(lilie_1_1, ge) & quant(lilie_1_1, one) & refer(lilie_1_1, refer_c) & varia(lilie_1_1, varia_c) & sort(c61231, o) & card(c61231, int1) & etype(c61231, int0) & fact(c61231, real) & gener(c61231, gener_c) & quant(c61231, one) & refer(c61231, refer_c) & varia(c61231, varia_c) & sort(sich_1_1, o) & card(sich_1_1, int1) & etype(sich_1_1, int0) & fact(sich_1_1, real) & gener(sich_1_1, gener_c) & quant(sich_1_1, one) & refer(sich_1_1, refer_c) & varia(sich_1_1, varia_c) & sort(c61236, d) & card(c61236, cons(x_constant, cons(int1, nil))) & etype(c61236, int1) & fact(c61236, real) & gener(c61236, sp) & quant(c61236, mult) & refer(c61236, det) & varia(c61236, con) & sort(alkoholfahne_1_1, d) & card(alkoholfahne_1_1, int1) & etype(alkoholfahne_1_1, int0) & fact(alkoholfahne_1_1, real) & gener(alkoholfahne_1_1, ge) & quant(alkoholfahne_1_1, one) & refer(alkoholfahne_1_1, refer_c) & varia(alkoholfahne_1_1, varia_c) & sort(c61243, d) & sort(c61243, io) & card(c61243, int1) & etype(c61243, int0) & fact(c61243, real) & gener(c61243, sp) & quant(c61243, one) & refer(c61243, det) & varia(c61243, con) & sort(c61244, na) & card(c61244, int1) & etype(c61244, int0) & fact(c61244, real) & gener(c61244, sp) & quant(c61244, one) & refer(c61244, indet) & varia(c61244, 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(usa_0, fe) & sort(c61248, d) & card(c61248, int1) & etype(c61248, int0) & fact(c61248, real) & gener(c61248, sp) & quant(c61248, one) & refer(c61248, det) & varia(c61248, con) & sort(c61249, na) & card(c61249, int1) & etype(c61249, int0) & fact(c61249, real) & gener(c61249, sp) & quant(c61249, one) & refer(c61249, indet) & varia(c61249, varia_c) & sort(gebiet_1_1, d) & card(gebiet_1_1, int1) & etype(gebiet_1_1, int0) & fact(gebiet_1_1, real) & gener(gebiet_1_1, ge) & quant(gebiet_1_1, one) & refer(gebiet_1_1, refer_c) & varia(gebiet_1_1, varia_c) & sort(bosnien_0, fe) & sort(c61250, o) & card(c61250, int1) & etype(c61250, int0) & fact(c61250, real) & gener(c61250, gener_c) & quant(c61250, one) & refer(c61250, refer_c) & varia(c61250, varia_c) & sort(herzegowina_1_1, o) & card(herzegowina_1_1, int1) & etype(herzegowina_1_1, int0) & fact(herzegowina_1_1, real) & gener(herzegowina_1_1, ge) & quant(herzegowina_1_1, one) & refer(herzegowina_1_1, refer_c) & varia(herzegowina_1_1, varia_c) & sort(c62887, ent) & card(c62887, card_c) & etype(c62887, etype_c) & fact(c62887, real) & gener(c62887, gener_c) & quant(c62887, quant_c) & refer(c62887, refer_c) & varia(c62887, varia_c) & sort(c61228, o) & card(c61228, int1) & etype(c61228, int0) & fact(c61228, real) & gener(c61228, sp) & quant(c61228, one) & refer(c61228, det) & varia(c61228, varia_c) & 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_508)).
% 186.96/180.34 fof(synth_qa07_003_mira_news_508, conjecture, ? [_466533, _466536, _466539, _466542] : (attr(_466536, _466533) & scar(_466539, _466542) & sub(_466533, name_1_1) & val(_466533, usa_0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', synth_qa07_003_mira_news_508)).
% 186.96/180.34 fof(member_first, axiom, ! [_470900, _470903] : member(_470900, cons(_470900, _470903)), file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax', member_first)).
% 186.96/180.34 fof(attr_name__abk__374rzung_stehen_1_b_f__374r, axiom, ! [_474306, _474309, _474312] : (attr(_474312, _474306) & member(_474309, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil)))) & sub(_474306, _474309) => ? [_474371] : (mcont(_474371, _474312) & obj(_474371, _474312) & scar(_474371, _474312) & subs(_474371, stehen_1_b))), file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax', attr_name__abk__374rzung_stehen_1_b_f__374r)).
% 186.96/180.34
% 186.96/180.34 cnf(1, plain, [member(_129669, _129671), -(member(_129669, cons(_129670, _129671)))], clausify(member_second)).
% 186.96/180.34 cnf(2, plain, [-(val(c61244, usa_0))], clausify(ave07_era5_synth_qa07_003_mira_news_508)).
% 186.96/180.34 cnf(3, plain, [attr(_192873, _192872), scar(_192874, _192875), sub(_192872, name_1_1), val(_192872, usa_0)], clausify(synth_qa07_003_mira_news_508)).
% 186.96/180.34 cnf(4, plain, [-(attr(c61243, c61244))], clausify(ave07_era5_synth_qa07_003_mira_news_508)).
% 186.96/180.34 cnf(5, plain, [-(member(_129658, cons(_129658, _129659)))], clausify(member_first)).
% 186.96/180.34 cnf(6, plain, [-(sub(c61244, name_1_1))], clausify(ave07_era5_synth_qa07_003_mira_news_508)).
% 186.96/180.34 cnf(7, plain, [-(scar(52 ^ [_131756, _131755, _131754], _131756)), attr(_131756, _131754), member(_131755, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil)))), sub(_131754, _131755)], clausify(attr_name__abk__374rzung_stehen_1_b_f__374r)).
% 186.96/180.34
% 186.96/180.34 cnf('1',plain,[attr(c61243, c61244), scar(52 ^ [c61243, name_1_1, c61244], c61243), sub(c61244, name_1_1), val(c61244, usa_0)],start(3,bind([[_192873, _192874, _192875, _192872], [c61243, 52 ^ [c61243, name_1_1, c61244], c61243, c61244]]))).
% 186.96/180.34 cnf('1.1',plain,[-(attr(c61243, c61244))],extension(4)).
% 186.96/180.34 cnf('1.2',plain,[-(scar(52 ^ [c61243, name_1_1, c61244], c61243)), attr(c61243, c61244), member(name_1_1, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil)))), sub(c61244, name_1_1)],extension(7,bind([[_131756, _131754, _131755], [c61243, c61244, name_1_1]]))).
% 186.96/180.34 cnf('1.2.1',plain,[-(attr(c61243, c61244))],extension(4)).
% 186.96/180.34 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(1,bind([[_129670, _129669, _129671], [eigenname_1_1, name_1_1, cons(familiename_1_1, cons(name_1_1, nil))]]))).
% 186.96/180.34 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(1,bind([[_129670, _129669, _129671], [familiename_1_1, name_1_1, cons(name_1_1, nil)]]))).
% 186.96/180.34 cnf('1.2.2.1.1',plain,[-(member(name_1_1, cons(name_1_1, nil)))],extension(5,bind([[_129658, _129659], [name_1_1, nil]]))).
% 186.96/180.34 cnf('1.2.3',plain,[-(sub(c61244, name_1_1))],extension(6)).
% 186.96/180.34 cnf('1.3',plain,[-(sub(c61244, name_1_1))],extension(6)).
% 186.96/180.34 cnf('1.4',plain,[-(val(c61244, usa_0))],extension(2)).
% 186.96/180.34 %-----------------------------------------------------
% 186.96/180.35
% 186.96/180.35 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------