%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR113+16 : 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:27 EDT 2022
% Result : Theorem 5.84s 6.66s
% Output : Proof 5.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : CSR113+16 : TPTP v8.1.0. Released v4.0.0.
% 0.08/0.15 % Command : leancop_casc.sh %s %d
% 0.15/0.37 % Computer : n008.cluster.edu
% 0.15/0.37 % Model : x86_64 x86_64
% 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.37 % Memory : 8042.1875MB
% 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.37 % CPULimit : 300
% 0.15/0.37 % WCLimit : 600
% 0.15/0.37 % DateTime : Sat Jun 11 08:01:52 EDT 2022
% 0.15/0.37 % CPUTime :
% 5.84/6.66 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.84/6.67 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.84/6.68
% 5.84/6.68 %-----------------------------------------------------
% 5.84/6.68 fof(synth_qa07_003_mira_wp_208_a19713, conjecture, ? [_429360, _429363, _429366, _429369, _429372] : (attr(_429366, _429363) & loc(_429369, _429360) & scar(_429369, _429372) & sub(_429363, name_1_1) & subs(_429369, stehen_1_1) & val(_429363, new_york_0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', synth_qa07_003_mira_wp_208_a19713)).
% 5.84/6.68 fof(ave07_era5_synth_qa07_003_mira_wp_208_a19713, hypothesis, scar(c24, c33) & subs(c24, geh__366ren_1_1) & sub(c33, freiheitsstatue_1_1) & attch(c41, c33) & attr(c41, c42) & sub(c41, stadt__1_1) & sub(c42, name_1_1) & val(c42, new_york_0) & loc(c50171, c55271) & sub(c50171, insel__1_1) & equ(c50180, c50171) & arg1(c54369, c50180) & arg2(c54369, c50171) & assoc(c54369, c7) & modl(c54369, nicht_1_1) & semrel(c54369, c24) & subr(c54369, equ_0) & arg1(c55236, c55070) & arg2(c55236, c55267) & semrel(c55236, c54369) & subs(c55236, geh__366ren_1_3) & attr(c55267, c55268) & sub(c55267, gebietsinstitution_1_1) & sub(c55268, name_1_1) & val(c55268, new_jersey_0) & auf(c55271, c33) & assoc(freiheitsstatue_1_1, freiheit_1_1) & sub(freiheitsstatue_1_1, statue_1_1) & chsp2(plazieren_1_1, c7) & sort(c24, st) & fact(c24, real) & gener(c24, sp) & sort(c33, d) & card(c33, int1) & etype(c33, int0) & fact(c33, real) & gener(c33, sp) & quant(c33, one) & refer(c33, det) & varia(c33, con) & sort(geh__366ren_1_1, st) & fact(geh__366ren_1_1, real) & gener(geh__366ren_1_1, ge) & 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(c50171, d) & card(c50171, int1) & etype(c50171, int0) & fact(c50171, real) & gener(c50171, sp) & quant(c50171, one) & refer(c50171, det) & varia(c50171, con) & sort(c55271, l) & card(c55271, int1) & etype(c55271, int0) & fact(c55271, real) & gener(c55271, sp) & quant(c55271, one) & refer(c55271, det) & varia(c55271, varia_c) & sort(insel__1_1, d) & card(insel__1_1, int1) & etype(insel__1_1, int0) & fact(insel__1_1, real) & gener(insel__1_1, ge) & quant(insel__1_1, one) & refer(insel__1_1, refer_c) & varia(insel__1_1, varia_c) & sort(c50180, o) & card(c50180, int1) & etype(c50180, int0) & fact(c50180, real) & gener(c50180, sp) & quant(c50180, one) & refer(c50180, det) & varia(c50180, varia_c) & sort(c54369, st) & fact(c54369, real) & gener(c54369, sp) & sort(c7, tq) & sort(nicht_1_1, md) & fact(nicht_1_1, real) & gener(nicht_1_1, gener_c) & sort(equ_0, st) & fact(equ_0, real) & gener(equ_0, gener_c) & sort(c55236, st) & fact(c55236, real) & gener(c55236, sp) & sort(c55070, o) & card(c55070, int1) & etype(c55070, int0) & fact(c55070, real) & gener(c55070, sp) & quant(c55070, one) & refer(c55070, det) & varia(c55070, varia_c) & sort(c55267, d) & sort(c55267, io) & card(c55267, int1) & etype(c55267, int0) & fact(c55267, real) & gener(c55267, sp) & quant(c55267, one) & refer(c55267, det) & varia(c55267, con) & sort(geh__366ren_1_3, st) & fact(geh__366ren_1_3, real) & gener(geh__366ren_1_3, ge) & sort(c55268, na) & card(c55268, int1) & etype(c55268, int0) & fact(c55268, real) & gener(c55268, sp) & quant(c55268, one) & refer(c55268, indet) & varia(c55268, varia_c) & sort(gebietsinstitution_1_1, d) & sort(gebietsinstitution_1_1, io) & card(gebietsinstitution_1_1, int1) & etype(gebietsinstitution_1_1, int0) & fact(gebietsinstitution_1_1, real) & gener(gebietsinstitution_1_1, ge) & quant(gebietsinstitution_1_1, one) & refer(gebietsinstitution_1_1, refer_c) & varia(gebietsinstitution_1_1, varia_c) & sort(new_jersey_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) & sort(plazieren_1_1, da) & fact(plazieren_1_1, real) & gener(plazieren_1_1, ge), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ave07_era5_synth_qa07_003_mira_wp_208_a19713)).
% 5.84/6.68 fof(loc__stehen_1_1_loc, axiom, ! [_432162, _432165] : (loc(_432162, _432165) => ? [_432183] : (loc(_432183, _432165) & scar(_432183, _432162) & subs(_432183, stehen_1_1))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', loc__stehen_1_1_loc)).
% 5.84/6.68
% 5.84/6.68 cnf(1, plain, [attr(_192619, _192618), loc(_192620, _192617), scar(_192620, _192621), sub(_192618, name_1_1), subs(_192620, stehen_1_1), val(_192618, new_york_0)], clausify(synth_qa07_003_mira_wp_208_a19713)).
% 5.84/6.68 cnf(2, plain, [-(attr(c41, c42))], clausify(ave07_era5_synth_qa07_003_mira_wp_208_a19713)).
% 5.84/6.68 cnf(3, plain, [-(sub(c42, name_1_1))], clausify(ave07_era5_synth_qa07_003_mira_wp_208_a19713)).
% 5.84/6.68 cnf(4, plain, [-(val(c42, new_york_0))], clausify(ave07_era5_synth_qa07_003_mira_wp_208_a19713)).
% 5.84/6.68 cnf(5, plain, [-(loc(c50171, c55271))], clausify(ave07_era5_synth_qa07_003_mira_wp_208_a19713)).
% 5.84/6.68 cnf(6, plain, [loc(_131985, _131986), -(loc(63 ^ [_131986, _131985], _131986))], clausify(loc__stehen_1_1_loc)).
% 5.84/6.68 cnf(7, plain, [loc(_131985, _131986), -(scar(63 ^ [_131986, _131985], _131985))], clausify(loc__stehen_1_1_loc)).
% 5.84/6.68 cnf(8, plain, [loc(_131985, _131986), -(subs(63 ^ [_131986, _131985], stehen_1_1))], clausify(loc__stehen_1_1_loc)).
% 5.84/6.68
% 5.84/6.68 cnf('1',plain,[attr(c41, c42), loc(63 ^ [c55271, c50171], c55271), scar(63 ^ [c55271, c50171], c50171), sub(c42, name_1_1), subs(63 ^ [c55271, c50171], stehen_1_1), val(c42, new_york_0)],start(1,bind([[_192619, _192617, _192621, _192620, _192618], [c41, c55271, c50171, 63 ^ [c55271, c50171], c42]]))).
% 5.84/6.68 cnf('1.1',plain,[-(attr(c41, c42))],extension(2)).
% 5.84/6.68 cnf('1.2',plain,[-(loc(63 ^ [c55271, c50171], c55271)), loc(c50171, c55271)],extension(6,bind([[_131985, _131986], [c50171, c55271]]))).
% 5.84/6.68 cnf('1.2.1',plain,[-(loc(c50171, c55271))],extension(5)).
% 5.84/6.68 cnf('1.3',plain,[-(scar(63 ^ [c55271, c50171], c50171)), loc(c50171, c55271)],extension(7,bind([[_131985, _131986], [c50171, c55271]]))).
% 5.84/6.68 cnf('1.3.1',plain,[-(loc(c50171, c55271))],extension(5)).
% 5.84/6.68 cnf('1.4',plain,[-(sub(c42, name_1_1))],extension(3)).
% 5.84/6.68 cnf('1.5',plain,[-(subs(63 ^ [c55271, c50171], stehen_1_1)), loc(c50171, c55271)],extension(8,bind([[_131985, _131986], [c50171, c55271]]))).
% 5.84/6.68 cnf('1.5.1',plain,[-(loc(c50171, c55271))],extension(5)).
% 5.84/6.68 cnf('1.6',plain,[-(val(c42, new_york_0))],extension(4)).
% 5.84/6.68 %-----------------------------------------------------
% 5.96/6.69
% 5.96/6.69 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------