%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR113+29 : 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:29 EDT 2022
% Result : Theorem 225.83s 217.42s
% Output : Proof 225.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : CSR113+29 : TPTP v8.1.0. Released v4.0.0.
% 0.03/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 : Fri Jun 10 17:48:21 EDT 2022
% 0.12/0.33 % CPUTime :
% 225.83/217.42 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 225.83/217.42 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 225.83/217.43
% 225.83/217.43 %-----------------------------------------------------
% 225.83/217.43 fof(name_rel__attr_val_name_1_1, axiom, ! [_626056, _626059] : (name(_626059, _626056) => ? [_626077] : (attr(_626059, _626077) & sub(_626077, name_1_1) & val(_626077, _626056))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', name_rel__attr_val_name_1_1)).
% 225.83/217.43 fof(member_second, axiom, ! [_626636, _626639, _626642] : (member(_626636, _626642) => member(_626636, cons(_626639, _626642))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', member_second)).
% 225.83/217.43 fof(attr_val_name_1_1__name_rel, axiom, ! [_627205, _627208, _627211] : (attr(_627211, _627205) & sub(_627205, name_1_1) & val(_627205, _627208) => name(_627211, _627208)), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', attr_val_name_1_1__name_rel)).
% 225.83/217.43 fof(member_first, axiom, ! [_627440, _627443] : member(_627440, cons(_627440, _627443)), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', member_first)).
% 225.83/217.43 fof(attr_name__abk__374rzung_stehen_1_b_f__374r, axiom, ! [_627662, _627665, _627668] : (attr(_627668, _627662) & member(_627665, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil)))) & sub(_627662, _627665) => ? [_627727] : (mcont(_627727, _627668) & obj(_627727, _627668) & scar(_627727, _627668) & subs(_627727, stehen_1_b))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', attr_name__abk__374rzung_stehen_1_b_f__374r)).
% 225.83/217.43 fof(synth_qa07_003_qapw_40_a270, conjecture, ? [_628185, _628188, _628191, _628194] : (attr(_628188, _628185) & scar(_628191, _628194) & sub(_628185, name_1_1) & val(_628185, usa_0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', synth_qa07_003_qapw_40_a270)).
% 225.83/217.43 fof(ave07_era5_synth_qa07_003_qapw_40_a270, hypothesis, pred(c573, land_1_1) & prop(c573, vereinigt_1_1) & sub(c574, in_2_1) & attr(c581, c582) & sub(c581, stadt__1_1) & sub(c582, name_1_1) & val(c582, seattle_0) & sub(c586, westkueste_1_1) & attch(c628, c586) & attr(c628, c629) & sub(c628, land_1_1) & sub(c629, name_1_1) & val(c629, usa_0) & prop(c633, weit_1_1) & sub(c633, freiheitsstatue_1_1) & tupl_p6(c770, c573, c574, c581, c586, c633) & assoc(freiheitsstatue_1_1, freiheit_1_1) & sub(freiheitsstatue_1_1, statue_1_1) & chsp2(vereinigen_1_1, vereinigt_1_1) & assoc(westkueste_1_1, west__1_1) & sub(westkueste_1_1, kueste_1_1) & sort(c573, d) & sort(c573, io) & card(c573, cons(x_constant, cons(int1, nil))) & etype(c573, int1) & fact(c573, real) & gener(c573, gener_c) & quant(c573, mult) & refer(c573, refer_c) & varia(c573, 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(vereinigt_1_1, tq) & sort(c574, o) & card(c574, int1) & etype(c574, int0) & fact(c574, real) & gener(c574, gener_c) & quant(c574, one) & refer(c574, refer_c) & varia(c574, varia_c) & sort(in_2_1, o) & card(in_2_1, int1) & etype(in_2_1, int0) & fact(in_2_1, real) & gener(in_2_1, ge) & quant(in_2_1, one) & refer(in_2_1, refer_c) & varia(in_2_1, varia_c) & sort(c581, d) & sort(c581, io) & card(c581, int1) & etype(c581, int0) & fact(c581, real) & gener(c581, sp) & quant(c581, one) & refer(c581, det) & varia(c581, con) & sort(c582, na) & card(c582, int1) & etype(c582, int0) & fact(c582, real) & gener(c582, sp) & quant(c582, one) & refer(c582, indet) & varia(c582, 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(seattle_0, fe) & sort(c586, d) & card(c586, int1) & etype(c586, int0) & fact(c586, real) & gener(c586, sp) & quant(c586, one) & refer(c586, det) & varia(c586, con) & sort(westkueste_1_1, d) & card(westkueste_1_1, int1) & etype(westkueste_1_1, int0) & fact(westkueste_1_1, real) & gener(westkueste_1_1, ge) & quant(westkueste_1_1, one) & refer(westkueste_1_1, refer_c) & varia(westkueste_1_1, varia_c) & sort(c628, d) & sort(c628, io) & card(c628, int1) & etype(c628, int0) & fact(c628, real) & gener(c628, sp) & quant(c628, one) & refer(c628, det) & varia(c628, con) & sort(c629, na) & card(c629, int1) & etype(c629, int0) & fact(c629, real) & gener(c629, sp) & quant(c629, one) & refer(c629, indet) & varia(c629, varia_c) & sort(usa_0, fe) & sort(c633, d) & card(c633, int1) & etype(c633, int0) & fact(c633, real) & gener(c633, sp) & quant(c633, one) & refer(c633, indet) & varia(c633, varia_c) & sort(weit_1_1, mq) & 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(c770, ent) & card(c770, card_c) & etype(c770, etype_c) & fact(c770, real) & gener(c770, gener_c) & quant(c770, quant_c) & refer(c770, refer_c) & varia(c770, 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) & sort(vereinigen_1_1, dn) & fact(vereinigen_1_1, real) & gener(vereinigen_1_1, ge) & sort(west__1_1, d) & sort(west__1_1, io) & card(west__1_1, int1) & etype(west__1_1, int0) & fact(west__1_1, real) & gener(west__1_1, ge) & quant(west__1_1, one) & refer(west__1_1, refer_c) & varia(west__1_1, varia_c) & sort(kueste_1_1, d) & card(kueste_1_1, int1) & etype(kueste_1_1, int0) & fact(kueste_1_1, real) & gener(kueste_1_1, ge) & quant(kueste_1_1, one) & refer(kueste_1_1, refer_c) & varia(kueste_1_1, varia_c), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ave07_era5_synth_qa07_003_qapw_40_a270)).
% 225.83/217.43
% 225.83/217.43 cnf(1, plain, [-(122 ^ [_131936, _131935]), -(attr(_131936, 121 ^ [_131936, _131935]))], clausify(name_rel__attr_val_name_1_1)).
% 225.83/217.43 cnf(2, plain, [member(_129492, _129494), -(member(_129492, cons(_129493, _129494)))], clausify(member_second)).
% 225.83/217.43 cnf(3, plain, [-(name(_131945, _131944)), attr(_131945, _131943), sub(_131943, name_1_1), val(_131943, _131944)], clausify(attr_val_name_1_1__name_rel)).
% 225.83/217.43 cnf(4, plain, [-(member(_129481, cons(_129481, _129482)))], clausify(member_first)).
% 225.83/217.43 cnf(5, plain, [99 ^ [_131579, _131578, _131577], attr(_131579, _131577), member(_131578, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil)))), sub(_131577, _131578)], clausify(attr_name__abk__374rzung_stehen_1_b_f__374r)).
% 225.83/217.43 cnf(6, plain, [attr(_192606, _192605), scar(_192607, _192608), sub(_192605, name_1_1), val(_192605, usa_0)], clausify(synth_qa07_003_qapw_40_a270)).
% 225.83/217.43 cnf(7, plain, [name(_131936, _131935), 122 ^ [_131936, _131935]], clausify(name_rel__attr_val_name_1_1)).
% 225.83/217.43 cnf(8, plain, [-(99 ^ [_131579, _131578, _131577]), -(scar(98 ^ [_131579, _131578, _131577], _131579))], clausify(attr_name__abk__374rzung_stehen_1_b_f__374r)).
% 225.83/217.43 cnf(9, plain, [-(122 ^ [_131936, _131935]), -(val(121 ^ [_131936, _131935], _131935))], clausify(name_rel__attr_val_name_1_1)).
% 225.83/217.43 cnf(10, plain, [-(122 ^ [_131936, _131935]), -(sub(121 ^ [_131936, _131935], name_1_1))], clausify(name_rel__attr_val_name_1_1)).
% 225.83/217.43 cnf(11, plain, [-(attr(c628, c629))], clausify(ave07_era5_synth_qa07_003_qapw_40_a270)).
% 225.83/217.43 cnf(12, plain, [-(val(c629, usa_0))], clausify(ave07_era5_synth_qa07_003_qapw_40_a270)).
% 225.83/217.43 cnf(13, plain, [-(sub(c629, name_1_1))], clausify(ave07_era5_synth_qa07_003_qapw_40_a270)).
% 225.83/217.43
% 225.83/217.43 cnf('1',plain,[attr(c628, 121 ^ [c628, usa_0]), scar(98 ^ [c628, name_1_1, 121 ^ [c628, usa_0]], c628), sub(121 ^ [c628, usa_0], name_1_1), val(121 ^ [c628, usa_0], usa_0)],start(6,bind([[_192606, _192607, _192608, _192605], [c628, 98 ^ [c628, name_1_1, 121 ^ [c628, usa_0]], c628, 121 ^ [c628, usa_0]]]))).
% 225.83/217.43 cnf('1.1',plain,[-(attr(c628, 121 ^ [c628, usa_0])), -(122 ^ [c628, usa_0])],extension(1,bind([[_131936, _131935], [c628, usa_0]]))).
% 225.83/217.43 cnf('1.1.1',plain,[122 ^ [c628, usa_0], name(c628, usa_0)],extension(7,bind([[_131936, _131935], [c628, usa_0]]))).
% 225.83/217.43 cnf('1.1.1.1',plain,[-(name(c628, usa_0)), attr(c628, c629), sub(c629, name_1_1), val(c629, usa_0)],extension(3,bind([[_131945, _131943, _131944], [c628, c629, usa_0]]))).
% 225.83/217.43 cnf('1.1.1.1.1',plain,[-(attr(c628, c629))],extension(11)).
% 225.83/217.43 cnf('1.1.1.1.2',plain,[-(sub(c629, name_1_1))],extension(13)).
% 225.83/217.43 cnf('1.1.1.1.3',plain,[-(val(c629, usa_0))],extension(12)).
% 225.83/217.43 cnf('1.2',plain,[-(scar(98 ^ [c628, name_1_1, 121 ^ [c628, usa_0]], c628)), -(99 ^ [c628, name_1_1, 121 ^ [c628, usa_0]])],extension(8,bind([[_131579, _131578, _131577], [c628, name_1_1, 121 ^ [c628, usa_0]]]))).
% 225.83/217.43 cnf('1.2.1',plain,[99 ^ [c628, name_1_1, 121 ^ [c628, usa_0]], attr(c628, 121 ^ [c628, usa_0]), member(name_1_1, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil)))), sub(121 ^ [c628, usa_0], name_1_1)],extension(5,bind([[_131579, _131577, _131578], [c628, 121 ^ [c628, usa_0], name_1_1]]))).
% 225.83/217.43 cnf('1.2.1.1',plain,[-(attr(c628, 121 ^ [c628, usa_0])), -(122 ^ [c628, usa_0])],extension(1,bind([[_131936, _131935], [c628, usa_0]]))).
% 225.83/217.43 cnf('1.2.1.1.1',plain,[122 ^ [c628, usa_0], name(c628, usa_0)],extension(7,bind([[_131936, _131935], [c628, usa_0]]))).
% 225.83/217.43 cnf('1.2.1.1.1.1',plain,[-(name(c628, usa_0)), attr(c628, c629), sub(c629, name_1_1), val(c629, usa_0)],extension(3,bind([[_131945, _131943, _131944], [c628, c629, usa_0]]))).
% 225.83/217.43 cnf('1.2.1.1.1.1.1',plain,[-(attr(c628, c629))],extension(11)).
% 225.83/217.43 cnf('1.2.1.1.1.1.2',plain,[-(sub(c629, name_1_1))],extension(13)).
% 225.83/217.43 cnf('1.2.1.1.1.1.3',plain,[-(val(c629, usa_0))],extension(12)).
% 225.83/217.43 cnf('1.2.1.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(2,bind([[_129493, _129492, _129494], [eigenname_1_1, name_1_1, cons(familiename_1_1, cons(name_1_1, nil))]]))).
% 225.83/217.43 cnf('1.2.1.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(2,bind([[_129493, _129492, _129494], [familiename_1_1, name_1_1, cons(name_1_1, nil)]]))).
% 225.83/217.43 cnf('1.2.1.2.1.1',plain,[-(member(name_1_1, cons(name_1_1, nil)))],extension(4,bind([[_129481, _129482], [name_1_1, nil]]))).
% 225.83/217.43 cnf('1.2.1.3',plain,[-(sub(121 ^ [c628, usa_0], name_1_1)), -(122 ^ [c628, usa_0])],extension(10,bind([[_131936, _131935], [c628, usa_0]]))).
% 225.83/217.43 cnf('1.2.1.3.1',plain,[122 ^ [c628, usa_0], name(c628, usa_0)],extension(7,bind([[_131936, _131935], [c628, usa_0]]))).
% 225.83/217.43 cnf('1.2.1.3.1.1',plain,[-(name(c628, usa_0)), attr(c628, c629), sub(c629, name_1_1), val(c629, usa_0)],extension(3,bind([[_131945, _131943, _131944], [c628, c629, usa_0]]))).
% 225.83/217.43 cnf('1.2.1.3.1.1.1',plain,[-(attr(c628, c629))],extension(11)).
% 225.83/217.43 cnf('1.2.1.3.1.1.2',plain,[-(sub(c629, name_1_1))],extension(13)).
% 225.83/217.43 cnf('1.2.1.3.1.1.3',plain,[-(val(c629, usa_0))],extension(12)).
% 225.83/217.43 cnf('1.3',plain,[-(sub(121 ^ [c628, usa_0], name_1_1)), -(122 ^ [c628, usa_0])],extension(10,bind([[_131936, _131935], [c628, usa_0]]))).
% 225.83/217.43 cnf('1.3.1',plain,[122 ^ [c628, usa_0], name(c628, usa_0)],extension(7,bind([[_131936, _131935], [c628, usa_0]]))).
% 225.83/217.43 cnf('1.3.1.1',plain,[-(name(c628, usa_0)), attr(c628, c629), sub(c629, name_1_1), val(c629, usa_0)],extension(3,bind([[_131945, _131943, _131944], [c628, c629, usa_0]]))).
% 225.83/217.43 cnf('1.3.1.1.1',plain,[-(attr(c628, c629))],extension(11)).
% 225.83/217.43 cnf('1.3.1.1.2',plain,[-(sub(c629, name_1_1))],extension(13)).
% 225.83/217.43 cnf('1.3.1.1.3',plain,[-(val(c629, usa_0))],extension(12)).
% 225.83/217.43 cnf('1.4',plain,[-(val(121 ^ [c628, usa_0], usa_0)), -(122 ^ [c628, usa_0])],extension(9,bind([[_131936, _131935], [c628, usa_0]]))).
% 225.83/217.43 cnf('1.4.1',plain,[122 ^ [c628, usa_0], name(c628, usa_0)],extension(7,bind([[_131936, _131935], [c628, usa_0]]))).
% 225.83/217.43 cnf('1.4.1.1',plain,[-(name(c628, usa_0)), attr(c628, c629), sub(c629, name_1_1), val(c629, usa_0)],extension(3,bind([[_131945, _131943, _131944], [c628, c629, usa_0]]))).
% 225.83/217.43 cnf('1.4.1.1.1',plain,[-(attr(c628, c629))],extension(11)).
% 225.83/217.43 cnf('1.4.1.1.2',plain,[-(sub(c629, name_1_1))],extension(13)).
% 225.83/217.43 cnf('1.4.1.1.3',plain,[-(val(c629, usa_0))],extension(12)).
% 225.83/217.43 %-----------------------------------------------------
% 225.83/217.44
% 225.83/217.44 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------