%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : CSR115+81 : 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 : n014.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:48 AM UTC 2026
% Result : Theorem 0.19s 0.54s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 2
% Syntax : Number of formulae : 20 ( 8 unt; 0 def)
% Number of atoms : 248 ( 0 equ)
% Maximal formula atoms : 166 ( 12 avg)
% Number of connectives : 284 ( 56 ~; 45 |; 183 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 166 ( 14 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 20 ( 19 usr; 1 prp; 0-4 aty)
% Number of functors : 47 ( 47 usr; 46 con; 0-2 aty)
% Number of variables : 54 ( 20 sgn 0 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ave07_era5_synth_qa07_007_mira_wp_491,axiom,
( varia(nabe_1_1,varia_c)
& refer(nabe_1_1,refer_c)
& quant(nabe_1_1,one)
& gener(nabe_1_1,ge)
& fact(nabe_1_1,real)
& etype(nabe_1_1,int0)
& card(nabe_1_1,int1)
& sort(nabe_1_1,o)
& varia(rotor_1_1,varia_c)
& refer(rotor_1_1,refer_c)
& quant(rotor_1_1,one)
& gener(rotor_1_1,ge)
& fact(rotor_1_1,real)
& etype(rotor_1_1,int0)
& card(rotor_1_1,int1)
& sort(rotor_1_1,o)
& varia(anlage_1_1,varia_c)
& refer(anlage_1_1,refer_c)
& quant(anlage_1_1,one)
& gener(anlage_1_1,ge)
& fact(anlage_1_1,real)
& etype(anlage_1_1,int0)
& card(anlage_1_1,int1)
& sort(anlage_1_1,as)
& varia(motor__1_1,varia_c)
& refer(motor__1_1,refer_c)
& quant(motor__1_1,one)
& gener(motor__1_1,ge)
& fact(motor__1_1,real)
& etype(motor__1_1,int0)
& card(motor__1_1,int1)
& sort(motor__1_1,d)
& varia(motoranlage_1_1,varia_c)
& refer(motoranlage_1_1,refer_c)
& quant(motoranlage_1_1,one)
& gener(motoranlage_1_1,ge)
& fact(motoranlage_1_1,real)
& etype(motoranlage_1_1,int0)
& card(motoranlage_1_1,int1)
& sort(motoranlage_1_1,as)
& varia(c9,varia_c)
& refer(c9,refer_c)
& quant(c9,one)
& gener(c9,gener_c)
& fact(c9,real)
& etype(c9,int0)
& card(c9,int1)
& sort(c9,as)
& sort(bmw_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(firma_1_1,varia_c)
& refer(firma_1_1,refer_c)
& quant(firma_1_1,one)
& gener(firma_1_1,ge)
& fact(firma_1_1,real)
& etype(firma_1_1,int0)
& card(firma_1_1,int1)
& sort(firma_1_1,io)
& sort(firma_1_1,d)
& varia(c58,varia_c)
& refer(c58,indet)
& quant(c58,one)
& gener(c58,sp)
& fact(c58,real)
& etype(c58,int0)
& card(c58,int1)
& sort(c58,na)
& gener(n374bernehmen_1_1,ge)
& fact(n374bernehmen_1_1,real)
& sort(n374bernehmen_1_1,da)
& varia(c62,con)
& refer(c62,det)
& quant(c62,nfquant)
& gener(c62,sp)
& fact(c62,real)
& etype(c62,int1)
& card(c62,int3)
& sort(c62,o)
& gener(sollen_0,gener_c)
& fact(sollen_0,real)
& sort(sollen_0,md)
& varia(c57,con)
& refer(c57,det)
& quant(c57,one)
& gener(c57,sp)
& fact(c57,real)
& etype(c57,int0)
& card(c57,int1)
& sort(c57,io)
& sort(c57,d)
& gener(c45,sp)
& fact(c45,real)
& sort(c45,da)
& varia(konstruktion_1_1,varia_c)
& refer(konstruktion_1_1,refer_c)
& quant(konstruktion_1_1,one)
& gener(konstruktion_1_1,ge)
& fact(konstruktion_1_1,real)
& etype(konstruktion_1_1,int0)
& card(konstruktion_1_1,int1)
& sort(konstruktion_1_1,d)
& varia(c4,con)
& refer(c4,det)
& quant(c4,one)
& gener(c4,sp)
& fact(c4,real)
& etype(c4,int0)
& card(c4,int1)
& sort(c4,d)
& varia(rotornabe_1_1,varia_c)
& refer(rotornabe_1_1,refer_c)
& quant(rotornabe_1_1,one)
& gener(rotornabe_1_1,ge)
& fact(rotornabe_1_1,real)
& etype(rotornabe_1_1,int0)
& card(rotornabe_1_1,int1)
& sort(rotornabe_1_1,o)
& varia(c16,varia_c)
& refer(c16,indet)
& quant(c16,mult)
& gener(c16,gener_c)
& fact(c16,real)
& etype(c16,int1)
& card(c16,cons(x_constant,cons(int1,nil)))
& sort(c16,o)
& varia(getriebe__1_1,varia_c)
& refer(getriebe__1_1,refer_c)
& quant(getriebe__1_1,one)
& gener(getriebe__1_1,ge)
& fact(getriebe__1_1,real)
& etype(getriebe__1_1,int0)
& card(getriebe__1_1,int1)
& sort(getriebe__1_1,d)
& varia(c12,varia_c)
& refer(c12,indet)
& quant(c12,mult)
& gener(c12,gener_c)
& fact(c12,real)
& etype(c12,int1)
& card(c12,cons(x_constant,cons(int1,nil)))
& sort(c12,d)
& sub(rotornabe_1_1,nabe_1_1)
& assoc(rotornabe_1_1,rotor_1_1)
& subs(motoranlage_1_1,anlage_1_1)
& assoc(motoranlage_1_1,motor__1_1)
& subs(c9,motoranlage_1_1)
& attch(c9,c4)
& itms_p4(c62,c4,c12,c16)
& val(c58,bmw_0)
& sub(c58,name_1_1)
& sub(c57,firma_1_1)
& attr(c57,c58)
& subs(c45,n374bernehmen_1_1)
& obj(c45,c62)
& modl(c45,sollen_0)
& agt(c45,c57)
& sub(c4,konstruktion_1_1)
& pred(c16,rotornabe_1_1)
& pred(c12,getriebe__1_1) ),
file('theBenchmark.p',ave07_era5_synth_qa07_007_mira_wp_491) ).
fof(synth_qa07_007_mira_wp_491,conjecture,
? [X0,X1,X2,X3,X4,X5,X6] :
( val(X2,bmw_0)
& val(X1,bmw_0)
& subs(X4,n374bernehmen_1_1)
& sub(X2,name_1_1)
& sub(X0,firma_1_1)
& sub(X1,name_1_1)
& attr(X5,X6)
& attr(X3,X2)
& attr(X0,X1)
& agt(X4,X3) ),
file('theBenchmark.p',synth_qa07_007_mira_wp_491) ).
fof(synth_qa07_007_mira_wp_491_neg,negated_conjecture,
~ ? [X0,X1,X2,X3,X4,X5,X6] :
( val(X2,bmw_0)
& val(X1,bmw_0)
& subs(X4,n374bernehmen_1_1)
& sub(X2,name_1_1)
& sub(X0,firma_1_1)
& sub(X1,name_1_1)
& attr(X5,X6)
& attr(X3,X2)
& attr(X0,X1)
& agt(X4,X3) ),
inference(assume_negation,[status(cth)],[synth_qa07_007_mira_wp_491]) ).
cnf(c_171,plain,
agt(c45,c57),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_007_mira_wp_491]) ).
cnf(c_174,plain,
subs(c45,n374bernehmen_1_1),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_007_mira_wp_491]) ).
cnf(c_175,plain,
attr(c57,c58),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_007_mira_wp_491]) ).
cnf(c_176,plain,
sub(c57,firma_1_1),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_007_mira_wp_491]) ).
cnf(c_177,plain,
sub(c58,name_1_1),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_007_mira_wp_491]) ).
cnf(c_178,plain,
val(c58,bmw_0),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_007_mira_wp_491]) ).
cnf(c_334,negated_conjecture,
( ~ val(E,bmw_0)
| ~ val(D,bmw_0)
| ~ subs(A,n374bernehmen_1_1)
| ~ sub(E,name_1_1)
| ~ sub(C,firma_1_1)
| ~ sub(D,name_1_1)
| ~ attr(F,V6)
| ~ attr(B,E)
| ~ attr(C,D)
| ~ agt(A,B) ),
inference(clausify,[status(thm)],[synth_qa07_007_mira_wp_491_neg]) ).
cnf(c_348,negated_conjecture,
( ~ val(C,bmw_0)
| ~ val(c58,bmw_0)
| ~ subs(A,n374bernehmen_1_1)
| ~ sub(C,name_1_1)
| ~ sub(c57,firma_1_1)
| ~ sub(c58,name_1_1)
| ~ attr(D,E)
| ~ attr(B,C)
| ~ agt(A,B) ),
inference(resolve,[status(thm)],[c_175,c_334]) ).
cnf(c_349,negated_conjecture,
( ~ val(C,bmw_0)
| ~ val(c58,bmw_0)
| ~ subs(A,n374bernehmen_1_1)
| ~ sub(C,name_1_1)
| ~ sub(c57,firma_1_1)
| ~ attr(D,E)
| ~ attr(B,C)
| ~ agt(A,B) ),
inference(resolve,[status(thm)],[c_177,c_348]) ).
cnf(c_350,negated_conjecture,
( ~ val(C,bmw_0)
| ~ val(c58,bmw_0)
| ~ subs(A,n374bernehmen_1_1)
| ~ sub(C,name_1_1)
| ~ attr(D,E)
| ~ attr(B,C)
| ~ agt(A,B) ),
inference(resolve,[status(thm)],[c_176,c_349]) ).
cnf(c_340,negated_conjecture,
( ~ val(C,bmw_0)
| ~ subs(A,n374bernehmen_1_1)
| ~ sub(C,name_1_1)
| ~ attr(D,E)
| ~ attr(B,C)
| ~ agt(A,B) ),
inference(resolve,[status(thm)],[c_178,c_350]) ).
cnf(c_351,plain,
( ~ val(c58,bmw_0)
| ~ subs(A,n374bernehmen_1_1)
| ~ sub(c58,name_1_1)
| ~ attr(B,C)
| ~ agt(A,c57) ),
inference(resolve,[status(thm)],[c_340,c_175]) ).
cnf(c_352,plain,
( ~ val(c58,bmw_0)
| ~ subs(A,n374bernehmen_1_1)
| ~ attr(B,C)
| ~ agt(A,c57) ),
inference(resolve,[status(thm)],[c_177,c_351]) ).
cnf(c_342,plain,
( ~ subs(A,n374bernehmen_1_1)
| ~ attr(B,C)
| ~ agt(A,c57) ),
inference(resolve,[status(thm)],[c_178,c_352]) ).
cnf(c_353,plain,
( ~ subs(c45,n374bernehmen_1_1)
| ~ attr(A,B) ),
inference(resolve,[status(thm)],[c_342,c_171]) ).
cnf(c_346,plain,
~ attr(A,B),
inference(resolve,[status(thm)],[c_174,c_353]) ).
cnf(c_347,plain,
$false,
inference(resolve,[status(thm)],[c_346,c_175]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR115+81 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n014.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 01:11:47 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.38 % Process 295699 was started by sandbox on n014,
% 0.11/0.38 % Sun Sep 27 01:11:47 2026
% 0.11/0.38 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.19/0.54
% 0.19/0.54 % SInE (scan): 66 to sos (tol 1.5x), 16 to usable (tol 2.0x), 10106 zapped, of 10188 axioms (depth 3).
% 0.19/0.54
% 0.19/0.54 % From the command line: assign(max_seconds, 300).
% 0.19/0.54
% 0.19/0.54 % SZS status Theorem for theBenchmark
% 0.19/0.54
% 0.19/0.54 % Proof 1 at 0.03 (+ 0.02) seconds.
% 0.19/0.54 % Length of proof is 13.
% 0.19/0.54 % Level of proof is 5.
% 0.19/0.54 % Maximum clause weight is 32.000.
% 0.19/0.54 % Given clauses 40.
% 0.19/0.54
% 0.19/0.54 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------