%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR113+11 : 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:26 EDT 2022
% Result : Theorem 186.05s 179.29s
% Output : Proof 186.11s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : CSR113+11 : TPTP v8.1.0. Released v4.0.0.
% 0.07/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.35 % DateTime : Sat Jun 11 10:15:52 EDT 2022
% 0.13/0.35 % CPUTime :
% 186.05/179.29 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 186.05/179.30 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 186.05/179.31
% 186.05/179.31 %-----------------------------------------------------
% 186.05/179.31 fof(ave07_era5_synth_qa07_003_mira_wp_184_a19713, hypothesis, tupl_p6(c145, c46, c51, c64, c87, c94) & sub(c46, freiheitsstatue_1_1) & sub(c51, geschenk__1_1) & attch(c57, c51) & attr(c57, c58) & sub(c57, land_1_1) & sub(c58, name_1_1) & val(c58, frankreich_0) & attr(c64, c65) & sub(c64, land_1_1) & sub(c65, name_1_1) & val(c65, usa_0) & sub(c87, bootshafen_1_1) & attr(c94, c95) & sub(c94, stadt__1_1) & sub(c95, name_1_1) & val(c95, new_york_0) & assoc(freiheitsstatue_1_1, freiheit_1_1) & sub(freiheitsstatue_1_1, statue_1_1) & sort(c145, ent) & card(c145, card_c) & etype(c145, etype_c) & fact(c145, real) & gener(c145, gener_c) & quant(c145, quant_c) & refer(c145, refer_c) & varia(c145, varia_c) & sort(c46, d) & card(c46, int1) & etype(c46, int0) & fact(c46, real) & gener(c46, sp) & quant(c46, one) & refer(c46, det) & varia(c46, con) & sort(c51, co) & card(c51, card_c) & etype(c51, etype_c) & fact(c51, real) & gener(c51, sp) & quant(c51, quant_c) & refer(c51, indet) & varia(c51, varia_c) & sort(c64, d) & sort(c64, io) & card(c64, int1) & etype(c64, int0) & fact(c64, real) & gener(c64, sp) & quant(c64, one) & refer(c64, det) & varia(c64, con) & sort(c87, d) & card(c87, int1) & etype(c87, int0) & fact(c87, real) & gener(c87, sp) & quant(c87, one) & refer(c87, det) & varia(c87, con) & sort(c94, d) & sort(c94, io) & card(c94, int1) & etype(c94, int0) & fact(c94, real) & gener(c94, sp) & quant(c94, one) & refer(c94, det) & varia(c94, 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(geschenk__1_1, co) & card(geschenk__1_1, card_c) & etype(geschenk__1_1, etype_c) & fact(geschenk__1_1, real) & gener(geschenk__1_1, ge) & quant(geschenk__1_1, quant_c) & refer(geschenk__1_1, refer_c) & varia(geschenk__1_1, varia_c) & sort(c57, d) & sort(c57, io) & card(c57, int1) & etype(c57, int0) & fact(c57, real) & gener(c57, sp) & quant(c57, one) & refer(c57, det) & varia(c57, con) & sort(c58, na) & card(c58, int1) & etype(c58, int0) & fact(c58, real) & gener(c58, sp) & quant(c58, one) & refer(c58, indet) & varia(c58, 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(frankreich_0, fe) & sort(c65, na) & card(c65, int1) & etype(c65, int0) & fact(c65, real) & gener(c65, sp) & quant(c65, one) & refer(c65, indet) & varia(c65, varia_c) & sort(usa_0, fe) & 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(c95, na) & card(c95, int1) & etype(c95, int0) & fact(c95, real) & gener(c95, sp) & quant(c95, one) & refer(c95, indet) & varia(c95, 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_wp_184_a19713)).
% 186.05/179.31 fof(synth_qa07_003_mira_wp_184_a19713, conjecture, ? [_451323, _451326, _451329, _451332] : (attr(_451326, _451323) & scar(_451329, _451332) & sub(_451323, name_1_1) & val(_451323, new_york_0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', synth_qa07_003_mira_wp_184_a19713)).
% 186.05/179.31 fof(member_second, axiom, ! [_456866, _456869, _456872] : (member(_456866, _456872) => member(_456866, cons(_456869, _456872))), file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax', member_second)).
% 186.05/179.31 fof(member_first, axiom, ! [_457756, _457759] : member(_457756, cons(_457756, _457759)), file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax', member_first)).
% 186.05/179.31 fof(attr_name__abk__374rzung_stehen_1_b_f__374r, axiom, ! [_460147, _460150, _460153] : (attr(_460153, _460147) & member(_460150, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil)))) & sub(_460147, _460150) => ? [_460212] : (mcont(_460212, _460153) & obj(_460212, _460153) & scar(_460212, _460153) & subs(_460212, stehen_1_b))), file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax', attr_name__abk__374rzung_stehen_1_b_f__374r)).
% 186.05/179.31
% 186.05/179.31 cnf(1, plain, [-(attr(c94, c95))], clausify(ave07_era5_synth_qa07_003_mira_wp_184_a19713)).
% 186.05/179.31 cnf(2, plain, [-(val(c95, new_york_0))], clausify(ave07_era5_synth_qa07_003_mira_wp_184_a19713)).
% 186.05/179.31 cnf(3, plain, [attr(_192459, _192458), scar(_192460, _192461), sub(_192458, name_1_1), val(_192458, new_york_0)], clausify(synth_qa07_003_mira_wp_184_a19713)).
% 186.05/179.31 cnf(4, plain, [-(sub(c95, name_1_1))], clausify(ave07_era5_synth_qa07_003_mira_wp_184_a19713)).
% 186.05/179.31 cnf(5, plain, [member(_129396, _129398), -(member(_129396, cons(_129397, _129398)))], clausify(member_second)).
% 186.05/179.31 cnf(6, plain, [-(member(_129385, cons(_129385, _129386)))], clausify(member_first)).
% 186.05/179.31 cnf(7, plain, [-(scar(52 ^ [_131483, _131482, _131481], _131483)), attr(_131483, _131481), member(_131482, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil)))), sub(_131481, _131482)], clausify(attr_name__abk__374rzung_stehen_1_b_f__374r)).
% 186.05/179.31
% 186.05/179.31 cnf('1',plain,[attr(c94, c95), scar(52 ^ [c94, name_1_1, c95], c94), sub(c95, name_1_1), val(c95, new_york_0)],start(3,bind([[_192459, _192460, _192461, _192458], [c94, 52 ^ [c94, name_1_1, c95], c94, c95]]))).
% 186.05/179.31 cnf('1.1',plain,[-(attr(c94, c95))],extension(1)).
% 186.05/179.31 cnf('1.2',plain,[-(scar(52 ^ [c94, name_1_1, c95], c94)), attr(c94, c95), member(name_1_1, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil)))), sub(c95, name_1_1)],extension(7,bind([[_131483, _131481, _131482], [c94, c95, name_1_1]]))).
% 186.05/179.31 cnf('1.2.1',plain,[-(attr(c94, c95))],extension(1)).
% 186.05/179.31 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(5,bind([[_129397, _129396, _129398], [eigenname_1_1, name_1_1, cons(familiename_1_1, cons(name_1_1, nil))]]))).
% 186.05/179.31 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(5,bind([[_129397, _129396, _129398], [familiename_1_1, name_1_1, cons(name_1_1, nil)]]))).
% 186.05/179.31 cnf('1.2.2.1.1',plain,[-(member(name_1_1, cons(name_1_1, nil)))],extension(6,bind([[_129385, _129386], [name_1_1, nil]]))).
% 186.05/179.31 cnf('1.2.3',plain,[-(sub(c95, name_1_1))],extension(4)).
% 186.05/179.31 cnf('1.3',plain,[-(sub(c95, name_1_1))],extension(4)).
% 186.05/179.31 cnf('1.4',plain,[-(val(c95, new_york_0))],extension(2)).
% 186.05/179.31 %-----------------------------------------------------
% 186.11/179.32
% 186.11/179.32 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------