%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR113+27 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n017.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:29 EDT 2022
% Result : Theorem 196.72s 189.98s
% Output : Proof 196.72s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : CSR113+27 : TPTP v8.1.0. Released v4.0.0.
% 0.12/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n017.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 21:31:05 EDT 2022
% 0.12/0.33 % CPUTime :
% 196.72/189.98 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 196.72/189.98 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 196.72/189.99
% 196.72/189.99 %-----------------------------------------------------
% 196.72/189.99 fof(member_second, axiom, ! [_712939, _712942, _712945] : (member(_712939, _712945) => member(_712939, cons(_712942, _712945))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', member_second)).
% 196.72/189.99 fof(ave07_era5_synth_qa07_003_qapn_26_a19713, hypothesis, pred(c78483, masse_1_1) & sub(c78489, sich_1_1) & sub(c78495, freiheit_1_1) & prop(c78520, ber__374hmt_1_1) & pred(c78522, wort_2_1) & sub(c78531, freiheitsstatue_1_1) & attr(c78537, c78538) & sub(c78537, stadt__1_1) & sub(c78538, name_1_1) & val(c78538, new_york_0) & tupl_p9(c79239, c78466, c78483, c78489, c78495, c78520, c78522, c78531, c78537) & assoc(freiheitsstatue_1_1, freiheit_1_1) & sub(freiheitsstatue_1_1, statue_1_1) & sort(c78483, io) & card(c78483, cons(x_constant, cons(int1, nil))) & etype(c78483, int2) & fact(c78483, real) & gener(c78483, gener_c) & quant(c78483, mult) & refer(c78483, indet) & varia(c78483, 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(c78489, o) & card(c78489, int1) & etype(c78489, int0) & fact(c78489, real) & gener(c78489, gener_c) & quant(c78489, one) & refer(c78489, refer_c) & varia(c78489, 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(c78495, as) & sort(c78495, io) & card(c78495, int1) & etype(c78495, int0) & fact(c78495, real) & gener(c78495, sp) & quant(c78495, one) & refer(c78495, det) & varia(c78495, 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(c78520, o) & card(c78520, cons(x_constant, cons(int1, nil))) & etype(c78520, int1) & fact(c78520, real) & gener(c78520, sp) & quant(c78520, mult) & refer(c78520, det) & varia(c78520, con) & sort(ber__374hmt_1_1, nq) & sort(c78522, d) & sort(c78522, io) & card(c78522, cons(x_constant, cons(int1, nil))) & etype(c78522, int1) & fact(c78522, real) & gener(c78522, gener_c) & quant(c78522, mult) & refer(c78522, indet) & varia(c78522, 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(c78531, d) & card(c78531, int1) & etype(c78531, int0) & fact(c78531, real) & gener(c78531, sp) & quant(c78531, one) & refer(c78531, det) & varia(c78531, 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(c78537, d) & sort(c78537, io) & card(c78537, int1) & etype(c78537, int0) & fact(c78537, real) & gener(c78537, sp) & quant(c78537, one) & refer(c78537, det) & varia(c78537, con) & sort(c78538, na) & card(c78538, int1) & etype(c78538, int0) & fact(c78538, real) & gener(c78538, sp) & quant(c78538, one) & refer(c78538, indet) & varia(c78538, 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(c79239, ent) & card(c79239, card_c) & etype(c79239, etype_c) & fact(c79239, real) & gener(c79239, gener_c) & quant(c79239, quant_c) & refer(c79239, refer_c) & varia(c79239, varia_c) & sort(c78466, d) & card(c78466, int1) & etype(c78466, int0) & fact(c78466, real) & gener(c78466, sp) & quant(c78466, one) & refer(c78466, det) & varia(c78466, 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_qapn_26_a19713)).
% 196.72/189.99 fof(synth_qa07_003_qapn_26_a19713, conjecture, ? [_716879, _716882, _716885, _716888] : (attr(_716882, _716879) & scar(_716885, _716888) & sub(_716879, name_1_1) & val(_716879, new_york_0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', synth_qa07_003_qapn_26_a19713)).
% 196.72/189.99 fof(member_first, axiom, ! [_718442, _718445] : member(_718442, cons(_718442, _718445)), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', member_first)).
% 196.72/189.99 fof(attr_name__abk__374rzung_stehen_1_b_f__374r, axiom, ! [_720279, _720282, _720285] : (attr(_720285, _720279) & member(_720282, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil)))) & sub(_720279, _720282) => ? [_720344] : (mcont(_720344, _720285) & obj(_720344, _720285) & scar(_720344, _720285) & subs(_720344, stehen_1_b))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', attr_name__abk__374rzung_stehen_1_b_f__374r)).
% 196.72/189.99
% 196.72/189.99 cnf(1, plain, [member(_129373, _129375), -(member(_129373, cons(_129374, _129375)))], clausify(member_second)).
% 196.72/189.99 cnf(2, plain, [-(attr(c78537, c78538))], clausify(ave07_era5_synth_qa07_003_qapn_26_a19713)).
% 196.72/189.99 cnf(3, plain, [attr(_192436, _192435), scar(_192437, _192438), sub(_192435, name_1_1), val(_192435, new_york_0)], clausify(synth_qa07_003_qapn_26_a19713)).
% 196.72/189.99 cnf(4, plain, [-(sub(c78538, name_1_1))], clausify(ave07_era5_synth_qa07_003_qapn_26_a19713)).
% 196.72/189.99 cnf(5, plain, [-(member(_129362, cons(_129362, _129363)))], clausify(member_first)).
% 196.72/189.99 cnf(6, plain, [-(val(c78538, new_york_0))], clausify(ave07_era5_synth_qa07_003_qapn_26_a19713)).
% 196.72/189.99 cnf(7, plain, [-(scar(52 ^ [_131460, _131459, _131458], _131460)), attr(_131460, _131458), member(_131459, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil)))), sub(_131458, _131459)], clausify(attr_name__abk__374rzung_stehen_1_b_f__374r)).
% 196.72/189.99
% 196.72/189.99 cnf('1',plain,[attr(c78537, c78538), scar(52 ^ [c78537, name_1_1, c78538], c78537), sub(c78538, name_1_1), val(c78538, new_york_0)],start(3,bind([[_192436, _192437, _192438, _192435], [c78537, 52 ^ [c78537, name_1_1, c78538], c78537, c78538]]))).
% 196.72/189.99 cnf('1.1',plain,[-(attr(c78537, c78538))],extension(2)).
% 196.72/189.99 cnf('1.2',plain,[-(scar(52 ^ [c78537, name_1_1, c78538], c78537)), attr(c78537, c78538), member(name_1_1, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil)))), sub(c78538, name_1_1)],extension(7,bind([[_131460, _131458, _131459], [c78537, c78538, name_1_1]]))).
% 196.72/189.99 cnf('1.2.1',plain,[-(attr(c78537, c78538))],extension(2)).
% 196.72/189.99 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([[_129374, _129373, _129375], [eigenname_1_1, name_1_1, cons(familiename_1_1, cons(name_1_1, nil))]]))).
% 196.72/189.99 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([[_129374, _129373, _129375], [familiename_1_1, name_1_1, cons(name_1_1, nil)]]))).
% 196.72/189.99 cnf('1.2.2.1.1',plain,[-(member(name_1_1, cons(name_1_1, nil)))],extension(5,bind([[_129362, _129363], [name_1_1, nil]]))).
% 196.72/189.99 cnf('1.2.3',plain,[-(sub(c78538, name_1_1))],extension(4)).
% 196.72/189.99 cnf('1.3',plain,[-(sub(c78538, name_1_1))],extension(4)).
% 196.72/189.99 cnf('1.4',plain,[-(val(c78538, new_york_0))],extension(6)).
% 196.72/189.99 %-----------------------------------------------------
% 196.72/189.99
% 196.72/189.99 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------