%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : CSR114+18 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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:36 AM UTC 2026
% Result : Theorem 5.16s 1.12s
% Output : CNFRefutation 5.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 3
% Syntax : Number of formulae : 29 ( 9 unt; 0 def)
% Number of atoms : 301 ( 0 equ)
% Maximal formula atoms : 209 ( 10 avg)
% Number of connectives : 325 ( 53 ~; 41 |; 230 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 209 ( 12 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 26 ( 25 usr; 1 prp; 0-2 aty)
% Number of functors : 58 ( 58 usr; 57 con; 0-2 aty)
% Number of variables : 55 ( 8 sgn 12 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
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_004_qapn_64_a281,axiom,
( varia(paar_3_1,varia_c)
& refer(paar_3_1,refer_c)
& quant(paar_3_1,quant_c)
& gener(paar_3_1,ge)
& fact(paar_3_1,real)
& etype(paar_3_1,int1)
& card(paar_3_1,card_c)
& sort(paar_3_1,d)
& varia(ehe_2_1,varia_c)
& refer(ehe_2_1,refer_c)
& quant(ehe_2_1,one)
& gener(ehe_2_1,ge)
& fact(ehe_2_1,real)
& etype(ehe_2_1,int0)
& card(ehe_2_1,int1)
& sort(ehe_2_1,re)
& sort(ehe_2_1,as)
& gener(erleben_1_1,ge)
& fact(erleben_1_1,real)
& sort(erleben_1_1,dn)
& gener(c31,sp)
& fact(c31,real)
& sort(c31,dn)
& varia(ehepaar_3_1,varia_c)
& refer(ehepaar_3_1,refer_c)
& quant(ehepaar_3_1,quant_c)
& gener(ehepaar_3_1,ge)
& fact(ehepaar_3_1,real)
& etype(ehepaar_3_1,int1)
& card(ehepaar_3_1,card_c)
& sort(ehepaar_3_1,d)
& sort(n344gyptisch_1_1,nq)
& varia(c25,varia_c)
& refer(c25,indet)
& quant(c25,one)
& gener(c25,sp)
& fact(c25,real)
& etype(c25,int1)
& card(c25,int1)
& sort(c25,d)
& gener(steigen_1_2,ge)
& fact(steigen_1_2,real)
& sort(steigen_1_2,da)
& gener(wollen_0,gener_c)
& fact(wollen_0,real)
& sort(wollen_0,md)
& varia(c245,con)
& refer(c245,det)
& quant(c245,one)
& gener(c245,sp)
& fact(c245,real)
& etype(c245,int0)
& card(c245,int1)
& sort(c245,l)
& varia(c244,con)
& refer(c244,det)
& quant(c244,one)
& gener(c244,sp)
& fact(c244,real)
& etype(c244,int0)
& card(c244,int1)
& sort(c244,l)
& varia(c243,varia_c)
& refer(c243,det)
& quant(c243,one)
& gener(c243,sp)
& fact(c243,real)
& etype(c243,int0)
& card(c243,int1)
& sort(c243,l)
& gener(c205,sp)
& fact(c205,real)
& sort(c205,da)
& varia(auto__1_1,varia_c)
& refer(auto__1_1,refer_c)
& quant(auto__1_1,one)
& gener(auto__1_1,ge)
& fact(auto__1_1,real)
& etype(auto__1_1,int0)
& card(auto__1_1,int1)
& sort(auto__1_1,d)
& sort(rom_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(c197,varia_c)
& refer(c197,indet)
& quant(c197,one)
& gener(c197,sp)
& fact(c197,real)
& etype(c197,int0)
& card(c197,int1)
& sort(c197,na)
& varia(c196,con)
& refer(c196,det)
& quant(c196,one)
& gener(c196,sp)
& fact(c196,real)
& etype(c196,int0)
& card(c196,int1)
& sort(c196,io)
& sort(c196,d)
& varia(kolosseum_1_1,con)
& refer(kolosseum_1_1,det)
& quant(kolosseum_1_1,one)
& gener(kolosseum_1_1,sp)
& fact(kolosseum_1_1,real)
& etype(kolosseum_1_1,int0)
& card(kolosseum_1_1,int1)
& sort(kolosseum_1_1,d)
& varia(c190,con)
& refer(c190,det)
& quant(c190,one)
& gener(c190,sp)
& fact(c190,real)
& etype(c190,int0)
& card(c190,int1)
& sort(c190,d)
& varia(c204,varia_c)
& refer(c204,det)
& quant(c204,one)
& gener(c204,sp)
& fact(c204,real)
& etype(c204,int0)
& card(c204,int1)
& sort(c204,d)
& varia(c184,varia_c)
& refer(c184,det)
& quant(c184,one)
& gener(c184,sp)
& fact(c184,real)
& etype(c184,int0)
& card(c184,int1)
& sort(c184,o)
& varia(dienstag__1_1,varia_c)
& refer(dienstag__1_1,refer_c)
& quant(dienstag__1_1,one)
& gener(dienstag__1_1,ge)
& fact(dienstag__1_1,real)
& etype(dienstag__1_1,int0)
& card(dienstag__1_1,int1)
& sort(dienstag__1_1,ta)
& varia(c15,con)
& refer(c15,det)
& quant(c15,one)
& gener(c15,sp)
& fact(c15,real)
& etype(c15,int0)
& card(c15,int1)
& sort(c15,ta)
& varia(n374berraschung_1_1,varia_c)
& refer(n374berraschung_1_1,refer_c)
& quant(n374berraschung_1_1,one)
& gener(n374berraschung_1_1,ge)
& fact(n374berraschung_1_1,real)
& etype(n374berraschung_1_1,int0)
& card(n374berraschung_1_1,int1)
& sort(n374berraschung_1_1,ad)
& sort(arglistig_1_1,nq)
& varia(c10,varia_c)
& refer(c10,indet)
& quant(c10,one)
& gener(c10,sp)
& fact(c10,real)
& etype(c10,int0)
& card(c10,int1)
& sort(c10,ad)
& sub(ehepaar_3_1,paar_3_1)
& assoc(ehepaar_3_1,ehe_2_1)
& temp(c31,c205)
& temp(c31,c15)
& subs(c31,erleben_1_1)
& obj(c31,c10)
& exp(c31,c25)
& sub(c25,ehepaar_3_1)
& prop(c25,n344gyptisch_1_1)
& vor(c245,c190)
& in(c244,c196)
& in(c243,c204)
& subs(c205,steigen_1_2)
& modl(c205,wollen_0)
& loc(c205,c245)
& loc(c205,c244)
& dircl(c205,c243)
& agt(c205,c184)
& sub(c204,auto__1_1)
& val(c197,rom_0)
& sub(c197,name_1_1)
& sub(c196,stadt__1_1)
& attr(c196,c197)
& sub(c190,kolosseum_1_1)
& poss(c184,c204)
& sub(c15,dienstag__1_1)
& subs(c10,n374berraschung_1_1)
& prop(c10,arglistig_1_1) ),
file('theBenchmark.p',ave07_era5_synth_qa07_004_qapn_64_a281) ).
fof(synth_qa07_004_qapn_64_a281,conjecture,
? [X0,X1,X2,X3,X4] :
( val(X1,rom_0)
& subs(X4,stehen_1_1)
& sub(X0,stadt__1_1)
& sub(X1,name_1_1)
& scar(X4,X3)
& loc(X4,X2)
& attr(X0,X1)
& in(X2,X0) ),
file('theBenchmark.p',synth_qa07_004_qapn_64_a281) ).
fof(synth_qa07_004_qapn_64_a281_neg,negated_conjecture,
~ ? [X0,X1,X2,X3,X4] :
( val(X1,rom_0)
& subs(X4,stehen_1_1)
& sub(X0,stadt__1_1)
& sub(X1,name_1_1)
& scar(X4,X3)
& loc(X4,X2)
& attr(X0,X1)
& in(X2,X0) ),
inference(assume_negation,[status(cth)],[synth_qa07_004_qapn_64_a281]) ).
fof(nnf_40,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_40]) ).
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_201,plain,
( loc(sK0(A,B),B)
| ~ loc(A,B) ),
inference(split_conjunct,[status(thm)],[sk_loc__stehen_1_1_loc]) ).
cnf(c_202,plain,
( scar(sK0(A,B),A)
| ~ loc(A,B) ),
inference(split_conjunct,[status(thm)],[sk_loc__stehen_1_1_loc]) ).
cnf(c_203,plain,
( subs(sK0(A,B),stehen_1_1)
| ~ loc(A,B) ),
inference(split_conjunct,[status(thm)],[sk_loc__stehen_1_1_loc]) ).
cnf(c_216,plain,
attr(c196,c197),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_004_qapn_64_a281]) ).
cnf(c_217,plain,
sub(c196,stadt__1_1),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_004_qapn_64_a281]) ).
cnf(c_218,plain,
sub(c197,name_1_1),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_004_qapn_64_a281]) ).
cnf(c_219,plain,
val(c197,rom_0),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_004_qapn_64_a281]) ).
cnf(c_223,plain,
loc(c205,c244),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_004_qapn_64_a281]) ).
cnf(c_228,plain,
in(c244,c196),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_004_qapn_64_a281]) ).
cnf(c_420,negated_conjecture,
( ~ val(C,rom_0)
| ~ subs(D,stehen_1_1)
| ~ sub(B,stadt__1_1)
| ~ sub(C,name_1_1)
| ~ scar(D,E)
| ~ loc(D,A)
| ~ attr(B,C)
| ~ in(A,B) ),
inference(clausify,[status(thm)],[synth_qa07_004_qapn_64_a281_neg]) ).
cnf(c_3489,negated_conjecture,
( ~ val(c197,rom_0)
| ~ subs(C,stehen_1_1)
| ~ sub(B,stadt__1_1)
| ~ scar(C,D)
| ~ loc(C,A)
| ~ attr(B,c197)
| ~ in(A,B) ),
inference(resolve,[status(thm)],[c_218,c_420]) ).
cnf(c_824,negated_conjecture,
( ~ subs(C,stehen_1_1)
| ~ sub(B,stadt__1_1)
| ~ scar(C,D)
| ~ loc(C,A)
| ~ attr(B,c197)
| ~ in(A,B) ),
inference(resolve,[status(thm)],[c_219,c_3489]) ).
cnf(c_3490,plain,
( ~ subs(A,stehen_1_1)
| ~ sub(c196,stadt__1_1)
| ~ scar(A,B)
| ~ loc(A,c244)
| ~ attr(c196,c197) ),
inference(resolve,[status(thm)],[c_228,c_824]) ).
cnf(c_3491,plain,
( ~ subs(A,stehen_1_1)
| ~ sub(c196,stadt__1_1)
| ~ scar(A,B)
| ~ loc(A,c244) ),
inference(resolve,[status(thm)],[c_216,c_3490]) ).
cnf(c_903,plain,
( ~ subs(A,stehen_1_1)
| ~ scar(A,B)
| ~ loc(A,c244) ),
inference(resolve,[status(thm)],[c_217,c_3491]) ).
cnf(c_3369,plain,
( ~ subs(sK0(A,c244),stehen_1_1)
| ~ scar(sK0(A,c244),B)
| ~ loc(A,c244) ),
inference(resolve,[status(thm)],[c_201,c_903]) ).
cnf(c_3376,plain,
loc(sK0(c205,c244),c244),
inference(resolve,[status(thm)],[c_201,c_223]) ).
cnf(c_3492,plain,
( ~ subs(sK0(A,c244),stehen_1_1)
| ~ loc(A,c244)
| ~ loc(A,c244) ),
inference(resolve,[status(thm)],[c_202,c_3369]) ).
cnf(c_3404,plain,
( ~ subs(sK0(A,c244),stehen_1_1)
| ~ loc(A,c244) ),
inference(copy,[status(thm)],[c_3492]) ).
cnf(c_3493,plain,
( ~ loc(A,c244)
| ~ loc(A,c244) ),
inference(resolve,[status(thm)],[c_203,c_3404]) ).
cnf(c_3487,plain,
~ loc(A,c244),
inference(copy,[status(thm)],[c_3493]) ).
cnf(c_3488,plain,
$false,
inference(resolve,[status(thm)],[c_3487,c_3376]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR114+18 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n017.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 27 01:00:34 UTC 2026
% 0.13/0.35 % CPUTime :
% 0.13/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/0.36 % Process 2040642 was started by sandbox2 on n017,
% 0.13/0.36 % Sun Sep 27 01:00:34 2026
% 0.13/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 5.16/1.12
% 5.16/1.12 % SInE (scan): 84 to sos (tol 1.5x), 22 to usable (tol 2.0x), 10082 zapped, of 10188 axioms (depth 3).
% 5.16/1.12
% 5.16/1.12 % From the command line: assign(max_seconds, 300).
% 5.16/1.12
% 5.16/1.12 % given #500 (F,wt=14): 2780 -scar(f8(c205,steigen_1_2),A) | -subs(B,stehen_1_1) | -subs(eintreffen_1_2,C) | -subs(C,B). [resolve(2779,b,170,c)].
% 5.16/1.12
% 5.16/1.12 % SZS status Theorem for theBenchmark
% 5.16/1.12
% 5.16/1.12 % Proof 1 at 0.57 (+ 0.11) seconds.
% 5.16/1.12 % Length of proof is 20.
% 5.16/1.12 % Level of proof is 7.
% 5.16/1.12 % Maximum clause weight is 24.000.
% 5.16/1.12 % Given clauses 595.
% 5.16/1.12
% 5.16/1.12 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------