%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR113+18 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n018.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:27 EDT 2022
% Result : Theorem 0.58s 1.42s
% Output : Proof 0.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : CSR113+18 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.34 % Computer : n018.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.34 % DateTime : Fri Jun 10 15:03:24 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.58/1.42 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.58/1.42 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.58/1.43
% 0.58/1.43 %-----------------------------------------------------
% 0.58/1.43 fof(synth_qa07_003_mira_wp_222_a19713, conjecture, ? [_422387, _422390, _422393, _422396, _422399] : (attr(_422393, _422390) & loc(_422396, _422387) & scar(_422396, _422399) & sub(_422390, name_1_1) & sub(_422399, freiheitsstatue_1_1) & subs(_422396, stehen_1_1) & val(_422390, new_york_0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', synth_qa07_003_mira_wp_222_a19713)).
% 0.58/1.43 fof(ave07_era5_synth_qa07_003_mira_wp_222_a19713, hypothesis, supl(c34, bekannt_1_1, c35) & prop(c4, c34) & sub(c4, freiheitsstatue_1_1) & attr(c41, c42) & sub(c41, stadt__1_1) & sub(c42, name_1_1) & val(c42, new_york_0) & mexp(c44, c50) & semrel(c44, c8) & subs(c44, sehen_1_1) & vor(c53, c41) & loc(c8, c53) & scar(c8, c4) & subs(c8, stehen_1_1) & assoc(freiheitsstatue_1_1, freiheit_1_1) & sub(freiheitsstatue_1_1, statue_1_1) & sort(c34, tq) & sort(bekannt_1_1, nq) & sort(c35, o) & card(c35, card_c) & etype(c35, int1) & etype(c35, int2) & fact(c35, real) & gener(c35, gener_c) & quant(c35, quant_c) & refer(c35, refer_c) & varia(c35, varia_c) & sort(c4, d) & card(c4, int1) & etype(c4, int0) & fact(c4, real) & gener(c4, sp) & quant(c4, one) & refer(c4, det) & varia(c4, 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(c41, d) & sort(c41, io) & card(c41, int1) & etype(c41, int0) & fact(c41, real) & gener(c41, sp) & quant(c41, one) & refer(c41, det) & varia(c41, con) & sort(c42, na) & card(c42, int1) & etype(c42, int0) & fact(c42, real) & gener(c42, sp) & quant(c42, one) & refer(c42, indet) & varia(c42, 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(c44, dn) & fact(c44, real) & gener(c44, sp) & sort(c50, d) & card(c50, int1) & etype(c50, int0) & fact(c50, real) & gener(c50, sp) & quant(c50, one) & refer(c50, det) & varia(c50, varia_c) & sort(c8, st) & fact(c8, real) & gener(c8, sp) & sort(sehen_1_1, dn) & fact(sehen_1_1, real) & gener(sehen_1_1, ge) & sort(c53, l) & card(c53, int1) & etype(c53, int0) & fact(c53, real) & gener(c53, sp) & quant(c53, one) & refer(c53, det) & varia(c53, con) & sort(stehen_1_1, st) & fact(stehen_1_1, real) & gener(stehen_1_1, ge) & 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_222_a19713)).
% 0.58/1.43
% 0.58/1.43 cnf(1, plain, [attr(_192033, _192032), loc(_192034, _192031), scar(_192034, _192035), sub(_192032, name_1_1), sub(_192035, freiheitsstatue_1_1), subs(_192034, stehen_1_1), val(_192032, new_york_0)], clausify(synth_qa07_003_mira_wp_222_a19713)).
% 0.58/1.43 cnf(2, plain, [-(sub(c4, freiheitsstatue_1_1))], clausify(ave07_era5_synth_qa07_003_mira_wp_222_a19713)).
% 0.58/1.43 cnf(3, plain, [-(attr(c41, c42))], clausify(ave07_era5_synth_qa07_003_mira_wp_222_a19713)).
% 0.58/1.43 cnf(4, plain, [-(sub(c42, name_1_1))], clausify(ave07_era5_synth_qa07_003_mira_wp_222_a19713)).
% 0.58/1.43 cnf(5, plain, [-(val(c42, new_york_0))], clausify(ave07_era5_synth_qa07_003_mira_wp_222_a19713)).
% 0.58/1.43 cnf(6, plain, [-(loc(c8, c53))], clausify(ave07_era5_synth_qa07_003_mira_wp_222_a19713)).
% 0.58/1.43 cnf(7, plain, [-(scar(c8, c4))], clausify(ave07_era5_synth_qa07_003_mira_wp_222_a19713)).
% 0.58/1.43 cnf(8, plain, [-(subs(c8, stehen_1_1))], clausify(ave07_era5_synth_qa07_003_mira_wp_222_a19713)).
% 0.58/1.43
% 0.58/1.43 cnf('1',plain,[attr(c41, c42), loc(c8, c53), scar(c8, c4), sub(c42, name_1_1), sub(c4, freiheitsstatue_1_1), subs(c8, stehen_1_1), val(c42, new_york_0)],start(1,bind([[_192033, _192031, _192035, _192034, _192032], [c41, c53, c4, c8, c42]]))).
% 0.58/1.43 cnf('1.1',plain,[-(attr(c41, c42))],extension(3)).
% 0.58/1.43 cnf('1.2',plain,[-(loc(c8, c53))],extension(6)).
% 0.58/1.43 cnf('1.3',plain,[-(scar(c8, c4))],extension(7)).
% 0.58/1.43 cnf('1.4',plain,[-(sub(c42, name_1_1))],extension(4)).
% 0.58/1.43 cnf('1.5',plain,[-(sub(c4, freiheitsstatue_1_1))],extension(2)).
% 0.58/1.43 cnf('1.6',plain,[-(subs(c8, stehen_1_1))],extension(8)).
% 0.58/1.43 cnf('1.7',plain,[-(val(c42, new_york_0))],extension(5)).
% 0.58/1.43 %-----------------------------------------------------
% 0.58/1.43
% 0.58/1.44 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------