%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR113+21 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n023.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:28 EDT 2022
% Result : Theorem 186.59s 180.64s
% Output : Proof 186.63s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : CSR113+21 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n023.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 : Fri Jun 10 08:57:52 EDT 2022
% 0.12/0.33 % CPUTime :
% 186.59/180.64 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 186.59/180.64 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 186.63/180.65
% 186.63/180.65 %-----------------------------------------------------
% 186.63/180.65 fof(attr_val_name_1_1__name_rel, axiom, ! [_447998, _448001, _448004] : (attr(_448004, _447998) & sub(_447998, name_1_1) & val(_447998, _448001) => name(_448004, _448001)), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', attr_val_name_1_1__name_rel)).
% 186.63/180.65 fof(name_rel__attr_val_name_1_1, axiom, ! [_449362, _449365] : (name(_449365, _449362) => ? [_449383] : (attr(_449365, _449383) & sub(_449383, name_1_1) & val(_449383, _449362))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', name_rel__attr_val_name_1_1)).
% 186.63/180.65 fof(ave07_era5_synth_qa07_003_mira_wp_232_a19713, hypothesis, sub(c28049, ironie_1_1) & poss(c28053, c28049) & sub(c28060, gedanke_1_1) & sub(c28066, bootshafen_1_1) & attr(c28073, c28074) & sub(c28073, stadt__1_1) & sub(c28074, name_1_1) & val(c28074, new_york_0) & sub(c28075, freiheitsstatue_1_1) & tupl_p8(c28887, c28013, c28049, c28060, c28066, c28073, c28075, c28013) & assoc(freiheitsstatue_1_1, freiheit_1_1) & sub(freiheitsstatue_1_1, statue_1_1) & sort(c28049, as) & sort(c28049, io) & card(c28049, int1) & etype(c28049, int0) & fact(c28049, real) & gener(c28049, sp) & quant(c28049, one) & refer(c28049, det) & varia(c28049, varia_c) & sort(ironie_1_1, as) & sort(ironie_1_1, io) & card(ironie_1_1, int1) & etype(ironie_1_1, int0) & fact(ironie_1_1, real) & gener(ironie_1_1, ge) & quant(ironie_1_1, one) & refer(ironie_1_1, refer_c) & varia(ironie_1_1, varia_c) & sort(c28053, o) & card(c28053, int1) & etype(c28053, int0) & fact(c28053, real) & gener(c28053, sp) & quant(c28053, one) & refer(c28053, det) & varia(c28053, varia_c) & sort(c28060, as) & sort(c28060, io) & card(c28060, int1) & etype(c28060, int0) & fact(c28060, real) & gener(c28060, sp) & quant(c28060, one) & refer(c28060, det) & varia(c28060, con) & sort(gedanke_1_1, as) & sort(gedanke_1_1, io) & card(gedanke_1_1, int1) & etype(gedanke_1_1, int0) & fact(gedanke_1_1, real) & gener(gedanke_1_1, ge) & quant(gedanke_1_1, one) & refer(gedanke_1_1, refer_c) & varia(gedanke_1_1, varia_c) & sort(c28066, d) & card(c28066, int1) & etype(c28066, int0) & fact(c28066, real) & gener(c28066, sp) & quant(c28066, one) & refer(c28066, det) & varia(c28066, con) & sort(bootshafen_1_1, d) & card(bootshafen_1_1, int1) & etype(bootshafen_1_1, int0) & fact(bootshafen_1_1, real) & gener(bootshafen_1_1, ge) & quant(bootshafen_1_1, one) & refer(bootshafen_1_1, refer_c) & varia(bootshafen_1_1, varia_c) & sort(c28073, d) & sort(c28073, io) & card(c28073, int1) & etype(c28073, int0) & fact(c28073, real) & gener(c28073, sp) & quant(c28073, one) & refer(c28073, det) & varia(c28073, con) & sort(c28074, na) & card(c28074, int1) & etype(c28074, int0) & fact(c28074, real) & gener(c28074, sp) & quant(c28074, one) & refer(c28074, indet) & varia(c28074, 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(new_york_0, fe) & sort(c28075, d) & card(c28075, int1) & etype(c28075, int0) & fact(c28075, real) & gener(c28075, sp) & quant(c28075, one) & refer(c28075, indet) & varia(c28075, 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(c28887, ent) & card(c28887, card_c) & etype(c28887, etype_c) & fact(c28887, real) & gener(c28887, gener_c) & quant(c28887, quant_c) & refer(c28887, refer_c) & varia(c28887, varia_c) & sort(c28013, d) & card(c28013, int1) & etype(c28013, int0) & fact(c28013, real) & gener(c28013, sp) & quant(c28013, one) & refer(c28013, det) & varia(c28013, 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/sandbox2/benchmark/theBenchmark.p', ave07_era5_synth_qa07_003_mira_wp_232_a19713)).
% 186.63/180.65 fof(synth_qa07_003_mira_wp_232_a19713, conjecture, ? [_453251, _453254, _453257, _453260] : (attr(_453254, _453251) & scar(_453257, _453260) & sub(_453251, name_1_1) & val(_453251, new_york_0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', synth_qa07_003_mira_wp_232_a19713)).
% 186.63/180.65 fof(attr_name__abk__374rzung_stehen_1_b_f__374r, axiom, ! [_457494, _457497, _457500] : (attr(_457500, _457494) & member(_457497, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil)))) & sub(_457494, _457497) => ? [_457559] : (mcont(_457559, _457500) & obj(_457559, _457500) & scar(_457559, _457500) & subs(_457559, stehen_1_b))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', attr_name__abk__374rzung_stehen_1_b_f__374r)).
% 186.63/180.65 fof(member_second, axiom, ! [_458407, _458410, _458413] : (member(_458407, _458413) => member(_458407, cons(_458410, _458413))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', member_second)).
% 186.63/180.65 fof(member_first, axiom, ! [_459906, _459909] : member(_459906, cons(_459906, _459909)), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', member_first)).
% 186.63/180.65
% 186.63/180.65 cnf(1, plain, [-(name(_131755, _131754)), attr(_131755, _131753), sub(_131753, name_1_1), val(_131753, _131754)], clausify(attr_val_name_1_1__name_rel)).
% 186.63/180.65 cnf(2, plain, [name(_131746, _131745), -(attr(_131746, 61 ^ [_131746, _131745]))], clausify(name_rel__attr_val_name_1_1)).
% 186.63/180.65 cnf(3, plain, [-(attr(c28073, c28074))], clausify(ave07_era5_synth_qa07_003_mira_wp_232_a19713)).
% 186.63/180.65 cnf(4, plain, [attr(_192319, _192318), scar(_192320, _192321), sub(_192318, name_1_1), val(_192318, new_york_0)], clausify(synth_qa07_003_mira_wp_232_a19713)).
% 186.63/180.65 cnf(5, plain, [-(val(c28074, new_york_0))], clausify(ave07_era5_synth_qa07_003_mira_wp_232_a19713)).
% 186.63/180.65 cnf(6, plain, [name(_131746, _131745), -(sub(61 ^ [_131746, _131745], name_1_1))], clausify(name_rel__attr_val_name_1_1)).
% 186.63/180.65 cnf(7, plain, [-(scar(52 ^ [_131389, _131388, _131387], _131389)), attr(_131389, _131387), member(_131388, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil)))), sub(_131387, _131388)], clausify(attr_name__abk__374rzung_stehen_1_b_f__374r)).
% 186.63/180.65 cnf(8, plain, [member(_129302, _129304), -(member(_129302, cons(_129303, _129304)))], clausify(member_second)).
% 186.63/180.65 cnf(9, plain, [-(sub(c28074, name_1_1))], clausify(ave07_era5_synth_qa07_003_mira_wp_232_a19713)).
% 186.63/180.65 cnf(10, plain, [-(member(_129291, cons(_129291, _129292)))], clausify(member_first)).
% 186.63/180.65
% 186.63/180.65 cnf('1',plain,[attr(c28073, c28074), scar(52 ^ [c28073, name_1_1, 61 ^ [c28073, new_york_0]], c28073), sub(c28074, name_1_1), val(c28074, new_york_0)],start(4,bind([[_192319, _192320, _192321, _192318], [c28073, 52 ^ [c28073, name_1_1, 61 ^ [c28073, new_york_0]], c28073, c28074]]))).
% 186.63/180.65 cnf('1.1',plain,[-(attr(c28073, c28074))],extension(3)).
% 186.63/180.65 cnf('1.2',plain,[-(scar(52 ^ [c28073, name_1_1, 61 ^ [c28073, new_york_0]], c28073)), attr(c28073, 61 ^ [c28073, new_york_0]), member(name_1_1, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil)))), sub(61 ^ [c28073, new_york_0], name_1_1)],extension(7,bind([[_131389, _131387, _131388], [c28073, 61 ^ [c28073, new_york_0], name_1_1]]))).
% 186.63/180.65 cnf('1.2.1',plain,[-(attr(c28073, 61 ^ [c28073, new_york_0])), name(c28073, new_york_0)],extension(2,bind([[_131746, _131745], [c28073, new_york_0]]))).
% 186.63/180.65 cnf('1.2.1.1',plain,[-(name(c28073, new_york_0)), attr(c28073, c28074), sub(c28074, name_1_1), val(c28074, new_york_0)],extension(1,bind([[_131755, _131753, _131754], [c28073, c28074, new_york_0]]))).
% 186.63/180.65 cnf('1.2.1.1.1',plain,[-(attr(c28073, c28074))],extension(3)).
% 186.63/180.65 cnf('1.2.1.1.2',plain,[-(sub(c28074, name_1_1))],extension(9)).
% 186.63/180.65 cnf('1.2.1.1.3',plain,[-(val(c28074, new_york_0))],extension(5)).
% 186.63/180.65 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(8,bind([[_129303, _129302, _129304], [eigenname_1_1, name_1_1, cons(familiename_1_1, cons(name_1_1, nil))]]))).
% 186.63/180.65 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(8,bind([[_129303, _129302, _129304], [familiename_1_1, name_1_1, cons(name_1_1, nil)]]))).
% 186.63/180.65 cnf('1.2.2.1.1',plain,[-(member(name_1_1, cons(name_1_1, nil)))],extension(10,bind([[_129291, _129292], [name_1_1, nil]]))).
% 186.63/180.65 cnf('1.2.3',plain,[-(sub(61 ^ [c28073, new_york_0], name_1_1)), name(c28073, new_york_0)],extension(6,bind([[_131746, _131745], [c28073, new_york_0]]))).
% 186.63/180.65 cnf('1.2.3.1',plain,[-(name(c28073, new_york_0)), attr(c28073, c28074), sub(c28074, name_1_1), val(c28074, new_york_0)],extension(1,bind([[_131755, _131753, _131754], [c28073, c28074, new_york_0]]))).
% 186.63/180.65 cnf('1.2.3.1.1',plain,[-(attr(c28073, c28074))],extension(3)).
% 186.63/180.65 cnf('1.2.3.1.2',plain,[-(sub(c28074, name_1_1))],extension(9)).
% 186.63/180.65 cnf('1.2.3.1.3',plain,[-(val(c28074, new_york_0))],extension(5)).
% 186.63/180.65 cnf('1.3',plain,[-(sub(c28074, name_1_1))],extension(9)).
% 186.63/180.65 cnf('1.4',plain,[-(val(c28074, new_york_0))],extension(5)).
% 186.63/180.65 %-----------------------------------------------------
% 186.63/180.65
% 186.63/180.65 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------