%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR113+8 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n025.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 192.45s 185.69s
% Output : Proof 192.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : CSR113+8 : TPTP v8.1.0. Released v4.0.0.
% 0.10/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n025.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 : Thu Jun 9 16:35:50 EDT 2022
% 0.12/0.33 % CPUTime :
% 192.45/185.69 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 192.45/185.69 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 192.53/185.70
% 192.53/185.70 %-----------------------------------------------------
% 192.53/185.70 fof(ave07_era5_synth_qa07_003_mira_news_520_a19713, hypothesis, attr(c18, c19) & sub(c18, stadt__1_1) & sub(c19, name_1_1) & val(c19, washington_0) & attr(c25, c26) & attr(c25, c27) & sub(c26, tag_1_1) & val(c26, c23) & sub(c27, monat_1_1) & val(c27, c24) & pred(c78576, masse_1_1) & sub(c78582, sich_1_1) & sub(c78588, freiheit_1_1) & prop(c78613, ber__374hmt_1_1) & pred(c78615, wort_2_1) & sub(c78624, freiheitsstatue_1_1) & attr(c78630, c78631) & sub(c78630, stadt__1_1) & sub(c78631, name_1_1) & val(c78631, new_york_0) & tupl_p9(c79332, c78559, c78576, c78582, c78588, c78613, c78615, c78624, c78630) & tupl(c92, c18, c25) & assoc(freiheitsstatue_1_1, freiheit_1_1) & sub(freiheitsstatue_1_1, statue_1_1) & sort(c18, d) & sort(c18, io) & card(c18, int1) & etype(c18, int0) & fact(c18, real) & gener(c18, sp) & quant(c18, one) & refer(c18, det) & varia(c18, con) & sort(c19, na) & card(c19, int1) & etype(c19, int0) & fact(c19, real) & gener(c19, sp) & quant(c19, one) & refer(c19, indet) & varia(c19, 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(washington_0, fe) & sort(c25, t) & card(c25, int1) & etype(c25, int0) & fact(c25, real) & gener(c25, sp) & quant(c25, one) & refer(c25, det) & varia(c25, con) & sort(c26, me) & sort(c26, oa) & sort(c26, ta) & card(c26, card_c) & etype(c26, etype_c) & fact(c26, real) & gener(c26, sp) & quant(c26, quant_c) & refer(c26, refer_c) & varia(c26, varia_c) & sort(c27, me) & sort(c27, oa) & sort(c27, ta) & card(c27, card_c) & etype(c27, etype_c) & fact(c27, real) & gener(c27, sp) & quant(c27, quant_c) & refer(c27, refer_c) & varia(c27, 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(c23, nu) & card(c23, int2) & 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(c24, nu) & card(c24, int3) & sort(c78576, io) & card(c78576, cons(x_constant, cons(int1, nil))) & etype(c78576, int2) & fact(c78576, real) & gener(c78576, gener_c) & quant(c78576, mult) & refer(c78576, indet) & varia(c78576, varia_c) & sort(masse_1_1, io) & card(masse_1_1, card_c) & etype(masse_1_1, int1) & fact(masse_1_1, real) & gener(masse_1_1, ge) & quant(masse_1_1, quant_c) & refer(masse_1_1, refer_c) & varia(masse_1_1, varia_c) & sort(c78582, o) & card(c78582, int1) & etype(c78582, int0) & fact(c78582, real) & gener(c78582, gener_c) & quant(c78582, one) & refer(c78582, refer_c) & varia(c78582, 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(c78588, as) & sort(c78588, io) & card(c78588, int1) & etype(c78588, int0) & fact(c78588, real) & gener(c78588, sp) & quant(c78588, one) & refer(c78588, det) & varia(c78588, con) & 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(c78613, o) & card(c78613, cons(x_constant, cons(int1, nil))) & etype(c78613, int1) & fact(c78613, real) & gener(c78613, sp) & quant(c78613, mult) & refer(c78613, det) & varia(c78613, con) & sort(ber__374hmt_1_1, nq) & sort(c78615, d) & sort(c78615, io) & card(c78615, cons(x_constant, cons(int1, nil))) & etype(c78615, int1) & fact(c78615, real) & gener(c78615, gener_c) & quant(c78615, mult) & refer(c78615, indet) & varia(c78615, varia_c) & sort(wort_2_1, d) & sort(wort_2_1, io) & card(wort_2_1, int1) & etype(wort_2_1, int0) & fact(wort_2_1, real) & gener(wort_2_1, ge) & quant(wort_2_1, one) & refer(wort_2_1, refer_c) & varia(wort_2_1, varia_c) & sort(c78624, d) & card(c78624, int1) & etype(c78624, int0) & fact(c78624, real) & gener(c78624, sp) & quant(c78624, one) & refer(c78624, det) & varia(c78624, 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(c78630, d) & sort(c78630, io) & card(c78630, int1) & etype(c78630, int0) & fact(c78630, real) & gener(c78630, sp) & quant(c78630, one) & refer(c78630, det) & varia(c78630, con) & sort(c78631, na) & card(c78631, int1) & etype(c78631, int0) & fact(c78631, real) & gener(c78631, sp) & quant(c78631, one) & refer(c78631, indet) & varia(c78631, varia_c) & sort(new_york_0, fe) & sort(c79332, ent) & card(c79332, card_c) & etype(c79332, etype_c) & fact(c79332, real) & gener(c79332, gener_c) & quant(c79332, quant_c) & refer(c79332, refer_c) & varia(c79332, varia_c) & sort(c78559, d) & card(c78559, int1) & etype(c78559, int0) & fact(c78559, real) & gener(c78559, sp) & quant(c78559, one) & refer(c78559, det) & varia(c78559, varia_c) & sort(c92, ent) & card(c92, card_c) & etype(c92, etype_c) & fact(c92, real) & gener(c92, gener_c) & quant(c92, quant_c) & refer(c92, refer_c) & varia(c92, 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/sandbox2/benchmark/theBenchmark.p', ave07_era5_synth_qa07_003_mira_news_520_a19713)).
% 192.53/185.70 fof(attr_name__abk__374rzung_stehen_1_b_f__374r, axiom, ! [_732106, _732109, _732112] : (attr(_732112, _732106) & member(_732109, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil)))) & sub(_732106, _732109) => ? [_732171] : (mcont(_732171, _732112) & obj(_732171, _732112) & scar(_732171, _732112) & subs(_732171, stehen_1_b))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', attr_name__abk__374rzung_stehen_1_b_f__374r)).
% 192.53/185.70 fof(member_second, axiom, ! [_733248, _733251, _733254] : (member(_733248, _733254) => member(_733248, cons(_733251, _733254))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', member_second)).
% 192.53/185.70 fof(member_first, axiom, ! [_735865, _735868] : member(_735865, cons(_735865, _735868)), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', member_first)).
% 192.53/185.70 fof(synth_qa07_003_mira_news_520_a19713, conjecture, ? [_740129, _740132, _740135, _740138] : (attr(_740132, _740129) & scar(_740135, _740138) & sub(_740129, name_1_1) & val(_740129, new_york_0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', synth_qa07_003_mira_news_520_a19713)).
% 192.53/185.70
% 192.53/185.70 cnf(1, plain, [-(val(c78631, new_york_0))], clausify(ave07_era5_synth_qa07_003_mira_news_520_a19713)).
% 192.53/185.70 cnf(2, plain, [-(sub(c78631, name_1_1))], clausify(ave07_era5_synth_qa07_003_mira_news_520_a19713)).
% 192.53/185.70 cnf(3, plain, [-(scar(52 ^ [_131995, _131994, _131993], _131995)), attr(_131995, _131993), member(_131994, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil)))), sub(_131993, _131994)], clausify(attr_name__abk__374rzung_stehen_1_b_f__374r)).
% 192.53/185.70 cnf(4, plain, [member(_129908, _129910), -(member(_129908, cons(_129909, _129910)))], clausify(member_second)).
% 192.53/185.70 cnf(5, plain, [-(attr(c78630, c78631))], clausify(ave07_era5_synth_qa07_003_mira_news_520_a19713)).
% 192.53/185.70 cnf(6, plain, [-(member(_129897, cons(_129897, _129898)))], clausify(member_first)).
% 192.53/185.70 cnf(7, plain, [attr(_193239, _193238), scar(_193240, _193241), sub(_193238, name_1_1), val(_193238, new_york_0)], clausify(synth_qa07_003_mira_news_520_a19713)).
% 192.53/185.70
% 192.53/185.70 cnf('1',plain,[attr(c78630, c78631), scar(52 ^ [c78630, name_1_1, c78631], c78630), sub(c78631, name_1_1), val(c78631, new_york_0)],start(7,bind([[_193239, _193240, _193241, _193238], [c78630, 52 ^ [c78630, name_1_1, c78631], c78630, c78631]]))).
% 192.53/185.70 cnf('1.1',plain,[-(attr(c78630, c78631))],extension(5)).
% 192.53/185.70 cnf('1.2',plain,[-(scar(52 ^ [c78630, name_1_1, c78631], c78630)), attr(c78630, c78631), member(name_1_1, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil)))), sub(c78631, name_1_1)],extension(3,bind([[_131995, _131993, _131994], [c78630, c78631, name_1_1]]))).
% 192.53/185.70 cnf('1.2.1',plain,[-(attr(c78630, c78631))],extension(5)).
% 192.53/185.70 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(4,bind([[_129909, _129908, _129910], [eigenname_1_1, name_1_1, cons(familiename_1_1, cons(name_1_1, nil))]]))).
% 192.53/185.70 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(4,bind([[_129909, _129908, _129910], [familiename_1_1, name_1_1, cons(name_1_1, nil)]]))).
% 192.53/185.70 cnf('1.2.2.1.1',plain,[-(member(name_1_1, cons(name_1_1, nil)))],extension(6,bind([[_129897, _129898], [name_1_1, nil]]))).
% 192.53/185.70 cnf('1.2.3',plain,[-(sub(c78631, name_1_1))],extension(2)).
% 192.53/185.70 cnf('1.3',plain,[-(sub(c78631, name_1_1))],extension(2)).
% 192.53/185.70 cnf('1.4',plain,[-(val(c78631, new_york_0))],extension(1)).
% 192.53/185.70 %-----------------------------------------------------
% 192.53/185.70
% 192.53/185.70 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------