%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : CSR113+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:07:34 AM UTC 2026
% Result : Theorem 36.48s 10.84s
% Output : CNFRefutation 36.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 4
% Syntax : Number of formulae : 31 ( 11 unt; 0 def)
% Number of atoms : 395 ( 0 equ)
% Maximal formula atoms : 299 ( 12 avg)
% Number of connectives : 414 ( 50 ~; 42 |; 320 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 299 ( 14 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 27 ( 26 usr; 1 prp; 0-3 aty)
% Number of functors : 68 ( 68 usr; 67 con; 0-2 aty)
% Number of variables : 53 ( 0 sgn 14 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(local_function___flp,axiom,
! [X0,X1] :
( ( bei(X0,X1)
| an(X0,X1)
| in(X0,X1) )
=> flp(X0,X1) ),
file('theBenchmark.p',local_function___flp) ).
fof(loc__stehen_1_1_loc,axiom,
! [X0,X1] :
( loc(X0,X1)
=> ? [X2] :
( subs(X2,stehen_1_1)
& scar(X2,X0)
& loc(X2,X1) ) ),
file('theBenchmark.p',loc__stehen_1_1_loc) ).
fof(ave07_era5_synth_qa07_003_insicht_4,axiom,
( varia(vater_1_1,varia_c)
& refer(vater_1_1,refer_c)
& quant(vater_1_1,one)
& gener(vater_1_1,ge)
& fact(vater_1_1,real)
& etype(vater_1_1,int0)
& card(vater_1_1,int1)
& sort(vater_1_1,d)
& varia(ansinnen_1_1,varia_c)
& refer(ansinnen_1_1,refer_c)
& quant(ansinnen_1_1,one)
& gener(ansinnen_1_1,ge)
& fact(ansinnen_1_1,real)
& etype(ansinnen_1_1,int0)
& card(ansinnen_1_1,int1)
& sort(ansinnen_1_1,io)
& sort(ansinnen_1_1,ad)
& varia(hilfe_1_1,varia_c)
& refer(hilfe_1_1,refer_c)
& quant(hilfe_1_1,one)
& gener(hilfe_1_1,ge)
& fact(hilfe_1_1,real)
& etype(hilfe_1_1,int0)
& card(hilfe_1_1,int1)
& sort(hilfe_1_1,io)
& sort(hilfe_1_1,ad)
& varia(statue_1_1,varia_c)
& refer(statue_1_1,refer_c)
& quant(statue_1_1,one)
& gener(statue_1_1,ge)
& fact(statue_1_1,real)
& etype(statue_1_1,int0)
& card(statue_1_1,int1)
& sort(statue_1_1,d)
& varia(freiheit_1_1,varia_c)
& refer(freiheit_1_1,refer_c)
& quant(freiheit_1_1,one)
& gener(freiheit_1_1,ge)
& fact(freiheit_1_1,real)
& etype(freiheit_1_1,int0)
& card(freiheit_1_1,int1)
& sort(freiheit_1_1,io)
& sort(freiheit_1_1,as)
& sort(vienna_0,fe)
& varia(c9,varia_c)
& refer(c9,indet)
& quant(c9,one)
& gener(c9,sp)
& fact(c9,real)
& etype(c9,int0)
& card(c9,int1)
& sort(c9,na)
& varia(c8,con)
& refer(c8,det)
& quant(c8,one)
& gener(c8,sp)
& fact(c8,real)
& etype(c8,int0)
& card(c8,int1)
& sort(c8,io)
& sort(c8,d)
& gener(rufen_1_2,ge)
& fact(rufen_1_2,real)
& sort(rufen_1_2,da)
& gener(c55,sp)
& fact(c55,real)
& sort(c55,da)
& varia(leben_1_1,varia_c)
& refer(leben_1_1,refer_c)
& quant(leben_1_1,one)
& gener(leben_1_1,ge)
& fact(leben_1_1,real)
& etype(leben_1_1,int0)
& card(leben_1_1,int1)
& sort(leben_1_1,ad)
& varia(c47,con)
& refer(c47,det)
& quant(c47,one)
& gener(c47,sp)
& fact(c47,real)
& etype(c47,int0)
& card(c47,int1)
& sort(c47,ad)
& sort(new_york_0,fe)
& varia(name_1_1,varia_c)
& refer(name_1_1,refer_c)
& quant(name_1_1,one)
& gener(name_1_1,ge)
& fact(name_1_1,real)
& etype(name_1_1,int0)
& card(name_1_1,int1)
& sort(name_1_1,na)
& varia(stadt__1_1,varia_c)
& refer(stadt__1_1,refer_c)
& quant(stadt__1_1,one)
& gener(stadt__1_1,ge)
& fact(stadt__1_1,real)
& etype(stadt__1_1,int0)
& card(stadt__1_1,int1)
& sort(stadt__1_1,io)
& sort(stadt__1_1,d)
& varia(c45,varia_c)
& refer(c45,indet)
& quant(c45,one)
& gener(c45,sp)
& fact(c45,real)
& etype(c45,int0)
& card(c45,int1)
& sort(c45,na)
& varia(c44,con)
& refer(c44,det)
& quant(c44,one)
& gener(c44,sp)
& fact(c44,real)
& etype(c44,int0)
& card(c44,int1)
& sort(c44,io)
& sort(c44,d)
& varia(freiheitsstatue_1_1,varia_c)
& refer(freiheitsstatue_1_1,refer_c)
& quant(freiheitsstatue_1_1,one)
& gener(freiheitsstatue_1_1,ge)
& fact(freiheitsstatue_1_1,real)
& etype(freiheitsstatue_1_1,int0)
& card(freiheitsstatue_1_1,int1)
& sort(freiheitsstatue_1_1,d)
& varia(c74,con)
& refer(c74,det)
& quant(c74,one)
& gener(c74,sp)
& fact(c74,real)
& etype(c74,int0)
& card(c74,int1)
& sort(c74,l)
& varia(hilfeprojekt_1_1,varia_c)
& refer(hilfeprojekt_1_1,refer_c)
& quant(hilfeprojekt_1_1,one)
& gener(hilfeprojekt_1_1,ge)
& fact(hilfeprojekt_1_1,real)
& etype(hilfeprojekt_1_1,int0)
& card(hilfeprojekt_1_1,int1)
& sort(hilfeprojekt_1_1,io)
& sort(hilfeprojekt_1_1,ad)
& sort(para_1_1,rq)
& varia(c38,con)
& refer(c38,det)
& quant(c38,one)
& gener(c38,sp)
& fact(c38,real)
& etype(c38,int0)
& card(c38,int1)
& sort(c38,d)
& varia(c32,varia_c)
& refer(c32,indet)
& quant(c32,one)
& gener(c32,sp)
& fact(c32,real)
& etype(c32,int0)
& card(c32,int1)
& sort(c32,io)
& sort(c32,ad)
& varia(idol_1_1,varia_c)
& refer(idol_1_1,refer_c)
& quant(idol_1_1,one)
& gener(idol_1_1,ge)
& fact(idol_1_1,real)
& etype(idol_1_1,int0)
& card(idol_1_1,int1)
& sort(idol_1_1,d)
& varia(c27,con)
& refer(c27,det)
& quant(c27,one)
& gener(c27,sp)
& fact(c27,real)
& etype(c27,int0)
& card(c27,int1)
& sort(c27,d)
& varia(aktion_1_1,varia_c)
& refer(aktion_1_1,refer_c)
& quant(aktion_1_1,one)
& gener(aktion_1_1,ge)
& fact(aktion_1_1,real)
& etype(aktion_1_1,int0)
& card(aktion_1_1,int1)
& sort(aktion_1_1,ad)
& varia(c75,con)
& refer(c75,det)
& quant(c75,one)
& gener(c75,sp)
& fact(c75,real)
& etype(c75,int0)
& card(c75,int1)
& sort(c75,l)
& varia(c21,con)
& refer(c21,det)
& quant(c21,one)
& gener(c21,sp)
& fact(c21,hypo)
& etype(c21,int0)
& card(c21,int1)
& sort(c21,ad)
& sort(zilk_0,fe)
& varia(familiename_1_1,varia_c)
& refer(familiename_1_1,refer_c)
& quant(familiename_1_1,one)
& gener(familiename_1_1,ge)
& fact(familiename_1_1,real)
& etype(familiename_1_1,int0)
& card(familiename_1_1,int1)
& sort(familiename_1_1,na)
& sort(helmut_0,fe)
& varia(eigenname_1_1,varia_c)
& refer(eigenname_1_1,refer_c)
& quant(eigenname_1_1,one)
& gener(eigenname_1_1,ge)
& fact(eigenname_1_1,real)
& etype(eigenname_1_1,int0)
& card(eigenname_1_1,int1)
& sort(eigenname_1_1,na)
& varia(c17,varia_c)
& refer(c17,indet)
& quant(c17,one)
& gener(c17,sp)
& fact(c17,real)
& etype(c17,int0)
& card(c17,int1)
& sort(c17,na)
& varia(c16,varia_c)
& refer(c16,indet)
& quant(c16,one)
& gener(c16,sp)
& fact(c16,real)
& etype(c16,int0)
& card(c16,int1)
& sort(c16,na)
& varia(c15,varia_c)
& refer(c15,det)
& quant(c15,one)
& gener(c15,sp)
& fact(c15,real)
& etype(c15,int0)
& card(c15,int1)
& sort(c15,d)
& varia(stadtvater_1_1,varia_c)
& refer(stadtvater_1_1,refer_c)
& quant(stadtvater_1_1,one)
& gener(stadtvater_1_1,ge)
& fact(stadtvater_1_1,real)
& etype(stadtvater_1_1,int0)
& card(stadtvater_1_1,int1)
& sort(stadtvater_1_1,d)
& sort(ehemalig_1_1,tq)
& varia(c1,varia_c)
& refer(c1,refer_c)
& quant(c1,quant_c)
& gener(c1,gener_c)
& fact(c1,fact_c)
& etype(c1,etype_c)
& card(c1,card_c)
& sort(c1,ent)
& sub(stadtvater_1_1,vater_1_1)
& assoc(stadtvater_1_1,stadt__1_1)
& sub(hilfeprojekt_1_1,ansinnen_1_1)
& assoc(hilfeprojekt_1_1,hilfe_1_1)
& sub(freiheitsstatue_1_1,statue_1_1)
& assoc(freiheitsstatue_1_1,freiheit_1_1)
& val(c9,vienna_0)
& sub(c9,name_1_1)
& sub(c8,stadt__1_1)
& attr(c8,c9)
& attch(c8,c15)
& flp(c75,c27)
& in(c74,c44)
& subs(c55,rufen_1_2)
& mcont(c55,c21)
& assoc(c55,c47)
& agt(c55,c15)
& subs(c47,leben_1_1)
& val(c45,new_york_0)
& sub(c45,name_1_1)
& sub(c44,stadt__1_1)
& attr(c44,c45)
& sub(c38,freiheitsstatue_1_1)
& loc(c38,c74)
& sub(c32,hilfeprojekt_1_1)
& propr(c32,para_1_1)
& benf(c32,c38)
& attch(c32,c27)
& sub(c27,idol_1_1)
& subs(c21,aktion_1_1)
& dircl(c21,c75)
& val(c17,zilk_0)
& sub(c17,familiename_1_1)
& val(c16,helmut_0)
& sub(c16,eigenname_1_1)
& sub(c15,c1)
& attr(c15,c17)
& attr(c15,c16)
& pmod(c1,ehemalig_1_1,stadtvater_1_1) ),
file('theBenchmark.p',ave07_era5_synth_qa07_003_insicht_4) ).
fof(synth_qa07_003_insicht_4,conjecture,
? [X0,X1,X2,X3,X4] :
( val(X1,new_york_0)
& subs(X3,stehen_1_1)
& sub(X4,freiheitsstatue_1_1)
& sub(X1,name_1_1)
& scar(X3,X4)
& loc(X3,X0)
& attr(X2,X1)
& flp(X0,X2) ),
file('theBenchmark.p',synth_qa07_003_insicht_4) ).
fof(synth_qa07_003_insicht_4_neg,negated_conjecture,
~ ? [X0,X1,X2,X3,X4] :
( val(X1,new_york_0)
& subs(X3,stehen_1_1)
& sub(X4,freiheitsstatue_1_1)
& sub(X1,name_1_1)
& scar(X3,X4)
& loc(X3,X0)
& attr(X2,X1)
& flp(X0,X2) ),
inference(assume_negation,[status(cth)],[synth_qa07_003_insicht_4]) ).
cnf(c_296,plain,
( flp(A,B)
| ~ in(A,B) ),
inference(clausify,[status(thm)],[local_function___flp]) ).
fof(nnf_52,plain,
! [X0,X1] :
( ? [X2] :
( subs(X2,stehen_1_1)
& scar(X2,X0)
& loc(X2,X1) )
| ~ loc(X0,X1) ),
inference(fof_nnf,[status(thm)],[loc__stehen_1_1_loc]) ).
fof(sk_loc__stehen_1_1_loc_sk,plain,
! [X0,X1] :
( ( subs(sK0(X0,X1),stehen_1_1)
& scar(sK0(X0,X1),X0)
& loc(sK0(X0,X1),X1) )
| ~ loc(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X2,sK0(X0,X1))],[nnf_52]) ).
fof(sk_loc__stehen_1_1_loc,plain,
( ! [VAR_0,VAR_1] :
( subs(sK0(VAR_0,VAR_1),stehen_1_1)
| ~ loc(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( scar(sK0(VAR_0,VAR_1),VAR_0)
| ~ loc(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( loc(sK0(VAR_0,VAR_1),VAR_1)
| ~ loc(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_loc__stehen_1_1_loc_sk]) ).
cnf(c_299,plain,
( loc(sK0(A,B),B)
| ~ loc(A,B) ),
inference(split_conjunct,[status(thm)],[sk_loc__stehen_1_1_loc]) ).
cnf(c_300,plain,
( scar(sK0(A,B),A)
| ~ loc(A,B) ),
inference(split_conjunct,[status(thm)],[sk_loc__stehen_1_1_loc]) ).
cnf(c_301,plain,
( subs(sK0(A,B),stehen_1_1)
| ~ loc(A,B) ),
inference(split_conjunct,[status(thm)],[sk_loc__stehen_1_1_loc]) ).
cnf(c_323,plain,
loc(c38,c74),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_003_insicht_4]) ).
cnf(c_324,plain,
sub(c38,freiheitsstatue_1_1),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_003_insicht_4]) ).
cnf(c_325,plain,
attr(c44,c45),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_003_insicht_4]) ).
cnf(c_327,plain,
sub(c45,name_1_1),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_003_insicht_4]) ).
cnf(c_328,plain,
val(c45,new_york_0),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_003_insicht_4]) ).
cnf(c_334,plain,
in(c74,c44),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_003_insicht_4]) ).
cnf(c_605,negated_conjecture,
( ~ val(C,new_york_0)
| ~ subs(D,stehen_1_1)
| ~ sub(E,freiheitsstatue_1_1)
| ~ sub(C,name_1_1)
| ~ scar(D,E)
| ~ loc(D,A)
| ~ attr(B,C)
| ~ flp(A,B) ),
inference(clausify,[status(thm)],[synth_qa07_003_insicht_4_neg]) ).
cnf(c_16718,negated_conjecture,
( ~ val(c45,new_york_0)
| ~ subs(B,stehen_1_1)
| ~ sub(C,freiheitsstatue_1_1)
| ~ sub(c45,name_1_1)
| ~ scar(B,C)
| ~ loc(B,A)
| ~ flp(A,c44) ),
inference(resolve,[status(thm)],[c_325,c_605]) ).
cnf(c_16719,negated_conjecture,
( ~ val(c45,new_york_0)
| ~ subs(B,stehen_1_1)
| ~ sub(C,freiheitsstatue_1_1)
| ~ scar(B,C)
| ~ loc(B,A)
| ~ flp(A,c44) ),
inference(resolve,[status(thm)],[c_327,c_16718]) ).
cnf(c_1367,negated_conjecture,
( ~ subs(B,stehen_1_1)
| ~ sub(C,freiheitsstatue_1_1)
| ~ scar(B,C)
| ~ loc(B,A)
| ~ flp(A,c44) ),
inference(resolve,[status(thm)],[c_328,c_16719]) ).
cnf(c_1417,plain,
( ~ subs(B,stehen_1_1)
| ~ scar(B,c38)
| ~ loc(B,A)
| ~ flp(A,c44) ),
inference(resolve,[status(thm)],[c_1367,c_324]) ).
cnf(c_4566,plain,
( ~ subs(B,stehen_1_1)
| ~ scar(B,c38)
| ~ loc(B,A)
| ~ in(A,c44) ),
inference(resolve,[status(thm)],[c_296,c_1417]) ).
cnf(c_5932,plain,
loc(sK0(c38,c74),c74),
inference(resolve,[status(thm)],[c_299,c_323]) ).
cnf(c_5985,plain,
scar(sK0(c38,c74),c38),
inference(resolve,[status(thm)],[c_300,c_323]) ).
cnf(c_6039,plain,
subs(sK0(c38,c74),stehen_1_1),
inference(resolve,[status(thm)],[c_301,c_323]) ).
cnf(c_9117,plain,
( ~ subs(A,stehen_1_1)
| ~ scar(A,c38)
| ~ loc(A,c74) ),
inference(resolve,[status(thm)],[c_4566,c_334]) ).
cnf(c_16720,plain,
( ~ subs(sK0(c38,c74),stehen_1_1)
| ~ scar(sK0(c38,c74),c38) ),
inference(resolve,[status(thm)],[c_5932,c_9117]) ).
cnf(c_16721,plain,
~ subs(sK0(c38,c74),stehen_1_1),
inference(resolve,[status(thm)],[c_5985,c_16720]) ).
cnf(c_16717,plain,
$false,
inference(resolve,[status(thm)],[c_6039,c_16721]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR113+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/5.43 % Computer : n016.cluster.edu
% 0.15/5.43 % Model : x86_64 x86_64
% 0.15/5.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/5.43 % Memory : 8046.5625MB
% 0.15/5.43 % OS : Linux 6.8.0-71-generic
% 0.15/5.43 % CPULimit : 300
% 0.15/5.43 % WCLimit : 300
% 0.15/5.43 % DateTime : Sun Sep 27 01:08:36 UTC 2026
% 0.15/5.43 % CPUTime :
% 0.15/5.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.15/5.44 % Process 2099368 was started by sandbox on n016,
% 0.15/5.44 % Sun Sep 27 01:08:36 2026
% 0.15/5.44 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 36.48/10.84
% 36.48/10.84 % SInE (scan): 95 to sos (tol 1.5x), 33 to usable (tol 2.0x), 10060 zapped, of 10188 axioms (depth 3).
% 36.48/10.84
% 36.48/10.84 % From the command line: assign(max_seconds, 300).
% 36.48/10.84
% 36.48/10.84 % given #500 (T,wt=8): 536 refer(leben_1_1,refer_c) # tptp_name(ave07_era5_synth_qa07_003_insicht_4) # sine_depth(1). [clausify(54)].
% 36.48/10.84
% 36.48/10.84 % given #1000 (F,wt=17): 5470 -scar(c38,c8) | -sub(stadt__1_1,c38) | -subs(c38,A) | -subs(A,stehen_1_1). [back_unit_del(2481),unit_del(a,4596)].
% 36.48/10.84
% 36.48/10.84 % given #1500 (W,wt=8): 6165 has_card_leq(ansinnen_1_1,card_c). [ur(84,a,590,a)].
% 36.48/10.84
% 36.48/10.84 % SZS status Theorem for theBenchmark
% 36.48/10.84
% 36.48/10.84 % Proof 1 at 4.63 (+ 0.50) seconds.
% 36.48/10.84 % Length of proof is 23.
% 36.48/10.84 % Level of proof is 6.
% 36.48/10.84 % Maximum clause weight is 29.000.
% 36.48/10.84 % Given clauses 1857.
% 36.48/10.84
% 36.48/10.84 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------