%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR113+19 : 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:27 EDT 2022
% Result : Theorem 0.99s 1.41s
% Output : Proof 0.99s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : CSR113+19 : TPTP v8.1.0. Released v4.0.0.
% 0.12/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.34 % Computer : n025.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 : Thu Jun 9 21:40:51 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.99/1.41 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.99/1.42 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.99/1.42
% 0.99/1.42 %-----------------------------------------------------
% 0.99/1.42 fof(synth_qa07_003_mira_wp_226_a19713, conjecture, ? [_431984, _431987, _431990, _431993, _431996] : (flp(_431984, _431990) & attr(_431990, _431987) & scar(_431993, _431996) & sub(_431987, name_1_1) & subs(_431993, stehen_1_1) & val(_431987, new_york_0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', synth_qa07_003_mira_wp_226_a19713)).
% 0.99/1.42 fof(ave07_era5_synth_qa07_003_mira_wp_226_a19713, hypothesis, agt(c1953, c1971) & dircl(c1953, c2020) & mannr(c1953, spaet_1_1) & subs(c1953, kommen_1_1) & temp(c1953, c3) & attr(c1971, c1972) & sub(c1971, stadt__1_1) & sub(c1972, name_1_1) & val(c1972, madison_0) & attr(c1976, c1977) & sub(c1976, stadt__1_1) & sub(c1977, name_1_1) & val(c1977, new_york_0) & sub(c1994, gestalt_1_1) & attr(c1999, c1994) & loc(c1999, c2018) & prop(c1999, bloss_1_1) & sub(c1999, frau_1_1) & attch(c2004, c2008) & sub(c2004, naehe_1_1) & sub(c2008, freiheitsstatue_1_1) & assoc(c2015, c1994) & exp(c2015, c1979) & semrel(c2015, c1953) & subs(c2015, auftauchen_1_1) & in(c2018, c2004) & flp(c2020, c1976) & pred(c3, jahr__1_1) & assoc(freiheitsstatue_1_1, freiheit_1_1) & sub(freiheitsstatue_1_1, statue_1_1) & sort(c1953, da) & fact(c1953, real) & gener(c1953, sp) & sort(c1971, d) & sort(c1971, io) & card(c1971, int1) & etype(c1971, int0) & fact(c1971, real) & gener(c1971, sp) & quant(c1971, one) & refer(c1971, det) & varia(c1971, con) & sort(c2020, l) & card(c2020, int1) & etype(c2020, int0) & fact(c2020, real) & gener(c2020, sp) & quant(c2020, one) & refer(c2020, det) & varia(c2020, con) & sort(spaet_1_1, mq) & sort(kommen_1_1, da) & fact(kommen_1_1, real) & gener(kommen_1_1, ge) & sort(c3, me) & sort(c3, oa) & sort(c3, ta) & card(c3, card_c) & etype(c3, etype_c) & fact(c3, real) & gener(c3, sp) & quant(c3, quant_c) & refer(c3, indet) & varia(c3, varia_c) & sort(c1972, na) & card(c1972, int1) & etype(c1972, int0) & fact(c1972, real) & gener(c1972, sp) & quant(c1972, one) & refer(c1972, indet) & varia(c1972, 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(madison_0, fe) & sort(c1976, d) & sort(c1976, io) & card(c1976, int1) & etype(c1976, int0) & fact(c1976, real) & gener(c1976, sp) & quant(c1976, one) & refer(c1976, det) & varia(c1976, con) & sort(c1977, na) & card(c1977, int1) & etype(c1977, int0) & fact(c1977, real) & gener(c1977, sp) & quant(c1977, one) & refer(c1977, indet) & varia(c1977, varia_c) & sort(new_york_0, fe) & sort(c1994, na) & card(c1994, int1) & etype(c1994, int0) & fact(c1994, real) & gener(c1994, sp) & quant(c1994, one) & refer(c1994, det) & varia(c1994, con) & sort(gestalt_1_1, na) & card(gestalt_1_1, int1) & etype(gestalt_1_1, int0) & fact(gestalt_1_1, real) & gener(gestalt_1_1, ge) & quant(gestalt_1_1, one) & refer(gestalt_1_1, refer_c) & varia(gestalt_1_1, varia_c) & sort(c1999, d) & card(c1999, int1) & etype(c1999, int0) & fact(c1999, real) & gener(c1999, sp) & quant(c1999, one) & refer(c1999, indet) & varia(c1999, varia_c) & sort(c2018, l) & card(c2018, int1) & etype(c2018, int0) & fact(c2018, real) & gener(c2018, sp) & quant(c2018, one) & refer(c2018, det) & varia(c2018, con) & sort(bloss_1_1, tq) & sort(frau_1_1, d) & card(frau_1_1, int1) & etype(frau_1_1, int0) & fact(frau_1_1, real) & gener(frau_1_1, ge) & quant(frau_1_1, one) & refer(frau_1_1, refer_c) & varia(frau_1_1, varia_c) & sort(c2004, d) & sort(c2004, io) & card(c2004, int1) & etype(c2004, int0) & fact(c2004, real) & gener(c2004, sp) & quant(c2004, one) & refer(c2004, det) & varia(c2004, con) & sort(c2008, d) & card(c2008, int1) & etype(c2008, int0) & fact(c2008, real) & gener(c2008, sp) & quant(c2008, one) & refer(c2008, det) & varia(c2008, con) & sort(naehe_1_1, d) & sort(naehe_1_1, io) & card(naehe_1_1, int1) & etype(naehe_1_1, int0) & fact(naehe_1_1, real) & gener(naehe_1_1, ge) & quant(naehe_1_1, one) & refer(naehe_1_1, refer_c) & varia(naehe_1_1, varia_c) & 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(c2015, dn) & fact(c2015, real) & gener(c2015, sp) & sort(c1979, o) & card(c1979, int1) & etype(c1979, int0) & fact(c1979, real) & gener(c1979, sp) & quant(c1979, one) & refer(c1979, det) & varia(c1979, varia_c) & sort(auftauchen_1_1, dn) & fact(auftauchen_1_1, real) & gener(auftauchen_1_1, ge) & sort(jahr__1_1, me) & sort(jahr__1_1, oa) & sort(jahr__1_1, ta) & card(jahr__1_1, card_c) & etype(jahr__1_1, etype_c) & fact(jahr__1_1, real) & gener(jahr__1_1, ge) & quant(jahr__1_1, quant_c) & refer(jahr__1_1, refer_c) & varia(jahr__1_1, 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), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ave07_era5_synth_qa07_003_mira_wp_226_a19713)).
% 0.99/1.42 fof(loc__stehen_1_1_loc, axiom, ! [_435183, _435186] : (loc(_435183, _435186) => ? [_435204] : (loc(_435204, _435186) & scar(_435204, _435183) & subs(_435204, stehen_1_1))), file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax', loc__stehen_1_1_loc)).
% 0.99/1.42
% 0.99/1.42 cnf(1, plain, [flp(_192932, _192934), attr(_192934, _192933), scar(_192935, _192936), sub(_192933, name_1_1), subs(_192935, stehen_1_1), val(_192933, new_york_0)], clausify(synth_qa07_003_mira_wp_226_a19713)).
% 0.99/1.42 cnf(2, plain, [-(attr(c1976, c1977))], clausify(ave07_era5_synth_qa07_003_mira_wp_226_a19713)).
% 0.99/1.42 cnf(3, plain, [-(sub(c1977, name_1_1))], clausify(ave07_era5_synth_qa07_003_mira_wp_226_a19713)).
% 0.99/1.42 cnf(4, plain, [-(val(c1977, new_york_0))], clausify(ave07_era5_synth_qa07_003_mira_wp_226_a19713)).
% 0.99/1.42 cnf(5, plain, [-(loc(c1999, c2018))], clausify(ave07_era5_synth_qa07_003_mira_wp_226_a19713)).
% 0.99/1.42 cnf(6, plain, [-(flp(c2020, c1976))], clausify(ave07_era5_synth_qa07_003_mira_wp_226_a19713)).
% 0.99/1.42 cnf(7, plain, [loc(_132195, _132196), -(scar(63 ^ [_132196, _132195], _132195))], clausify(loc__stehen_1_1_loc)).
% 0.99/1.42 cnf(8, plain, [loc(_132195, _132196), -(subs(63 ^ [_132196, _132195], stehen_1_1))], clausify(loc__stehen_1_1_loc)).
% 0.99/1.42
% 0.99/1.42 cnf('1',plain,[flp(c2020, c1976), attr(c1976, c1977), scar(63 ^ [c2018, c1999], c1999), sub(c1977, name_1_1), subs(63 ^ [c2018, c1999], stehen_1_1), val(c1977, new_york_0)],start(1,bind([[_192932, _192934, _192936, _192935, _192933], [c2020, c1976, c1999, 63 ^ [c2018, c1999], c1977]]))).
% 0.99/1.42 cnf('1.1',plain,[-(flp(c2020, c1976))],extension(6)).
% 0.99/1.42 cnf('1.2',plain,[-(attr(c1976, c1977))],extension(2)).
% 0.99/1.42 cnf('1.3',plain,[-(scar(63 ^ [c2018, c1999], c1999)), loc(c1999, c2018)],extension(7,bind([[_132195, _132196], [c1999, c2018]]))).
% 0.99/1.42 cnf('1.3.1',plain,[-(loc(c1999, c2018))],extension(5)).
% 0.99/1.42 cnf('1.4',plain,[-(sub(c1977, name_1_1))],extension(3)).
% 0.99/1.42 cnf('1.5',plain,[-(subs(63 ^ [c2018, c1999], stehen_1_1)), loc(c1999, c2018)],extension(8,bind([[_132195, _132196], [c1999, c2018]]))).
% 0.99/1.42 cnf('1.5.1',plain,[-(loc(c1999, c2018))],extension(5)).
% 0.99/1.42 cnf('1.6',plain,[-(val(c1977, new_york_0))],extension(4)).
% 0.99/1.42 %-----------------------------------------------------
% 0.99/1.43
% 0.99/1.43 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------