%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWB010+2 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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 08:51:29 AM UTC 2026
% Result : Theorem 0.21s 0.51s
% Output : CNFRefutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 10
% Syntax : Number of formulae : 72 ( 15 unt; 0 def)
% Number of atoms : 245 ( 5 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 265 ( 92 ~; 116 |; 45 &)
% ( 5 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 22 ( 22 usr; 21 con; 0-3 aty)
% Number of variables : 147 ( 12 sgn 37 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(simple_ir,axiom,
! [X] : ir(X),
file('theBenchmark.p',simple_ir) ).
fof(rdfs_cext_def,axiom,
! [X,C] :
( iext(uri_rdf_type,X,C)
<=> icext(C,X) ),
file('theBenchmark.p',rdfs_cext_def) ).
fof(owl_prop_sourceindividual_ext,axiom,
! [X,Y] :
( iext(uri_owl_sourceIndividual,X,Y)
=> ( ir(Y)
& icext(uri_owl_NegativePropertyAssertion,X) ) ),
file('theBenchmark.p',owl_prop_sourceindividual_ext) ).
fof(owl_prop_onproperty_ext,axiom,
! [X,Y] :
( iext(uri_owl_onProperty,X,Y)
=> ( ip(Y)
& icext(uri_owl_Restriction,X) ) ),
file('theBenchmark.p',owl_prop_onproperty_ext) ).
fof(owl_bool_complementof_class,axiom,
! [Z,C] :
( iext(uri_owl_complementOf,Z,C)
=> ( ! [X] :
( icext(Z,X)
<=> ~ icext(C,X) )
& ic(C)
& ic(Z) ) ),
file('theBenchmark.p',owl_bool_complementof_class) ).
fof(owl_enum_class_001,axiom,
! [Z,S1,A1] :
( ( iext(uri_rdf_rest,S1,uri_rdf_nil)
& iext(uri_rdf_first,S1,A1) )
=> ( iext(uri_owl_oneOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> X = A1 )
& ic(Z) ) ) ),
file('theBenchmark.p',owl_enum_class_001) ).
fof(owl_restrict_allvaluesfrom,axiom,
! [Z,P,C] :
( ( iext(uri_owl_onProperty,Z,P)
& iext(uri_owl_allValuesFrom,Z,C) )
=> ! [X] :
( icext(Z,X)
<=> ! [Y] :
( iext(P,X,Y)
=> icext(C,Y) ) ) ),
file('theBenchmark.p',owl_restrict_allvaluesfrom) ).
fof(owl_npa_object_fi,axiom,
! [P,A1,A2] :
( ( ~ iext(P,A1,A2)
& ir(A2)
& ip(P)
& ir(A1) )
=> ? [Z] :
( iext(uri_owl_targetIndividual,Z,A2)
& iext(uri_owl_assertionProperty,Z,P)
& iext(uri_owl_sourceIndividual,Z,A1) ) ),
file('theBenchmark.p',owl_npa_object_fi) ).
fof(testcase_premise_fullish_010_Negative_Property_Assertions,axiom,
? [BNODE_x1,BNODE_x2,BNODE_x3,BNODE_x4] :
( iext(uri_rdf_rest,BNODE_x4,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_x4,uri_ex_o)
& iext(uri_owl_oneOf,BNODE_x3,BNODE_x4)
& iext(uri_owl_complementOf,BNODE_x2,BNODE_x3)
& iext(uri_owl_allValuesFrom,BNODE_x1,BNODE_x2)
& iext(uri_owl_onProperty,BNODE_x1,uri_ex_p)
& iext(uri_rdf_type,uri_ex_s,BNODE_x1)
& iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty) ),
file('theBenchmark.p',testcase_premise_fullish_010_Negative_Property_Assertions) ).
fof(testcase_conclusion_fullish_010_Negative_Property_Assertions,conjecture,
? [BNODE_z] :
( iext(uri_owl_targetIndividual,BNODE_z,uri_ex_o)
& iext(uri_owl_assertionProperty,BNODE_z,uri_ex_p)
& iext(uri_owl_sourceIndividual,BNODE_z,uri_ex_s)
& iext(uri_rdf_type,BNODE_z,uri_owl_NegativePropertyAssertion) ),
file('theBenchmark.p',testcase_conclusion_fullish_010_Negative_Property_Assertions) ).
fof(testcase_conclusion_fullish_010_Negative_Property_Assertions_neg,negated_conjecture,
~ ? [BNODE_z] :
( iext(uri_owl_targetIndividual,BNODE_z,uri_ex_o)
& iext(uri_owl_assertionProperty,BNODE_z,uri_ex_p)
& iext(uri_owl_sourceIndividual,BNODE_z,uri_ex_s)
& iext(uri_rdf_type,BNODE_z,uri_owl_NegativePropertyAssertion) ),
inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_010_Negative_Property_Assertions]) ).
fof(nnf_8,plain,
! [P,A1,A2] :
( ? [Z] :
( iext(uri_owl_targetIndividual,Z,A2)
& iext(uri_owl_assertionProperty,Z,P)
& iext(uri_owl_sourceIndividual,Z,A1) )
| iext(P,A1,A2)
| ~ ir(A2)
| ~ ip(P)
| ~ ir(A1) ),
inference(fof_nnf,[status(thm)],[owl_npa_object_fi]) ).
fof(sk_owl_npa_object_fi_sk,plain,
! [P,A1,A2] :
( ( iext(uri_owl_targetIndividual,sK0(P,A1,A2),A2)
& iext(uri_owl_assertionProperty,sK0(P,A1,A2),P)
& iext(uri_owl_sourceIndividual,sK0(P,A1,A2),A1) )
| iext(P,A1,A2)
| ~ ir(A2)
| ~ ip(P)
| ~ ir(A1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(Z,sK0(P,A1,A2))],[nnf_8]) ).
fof(sk_owl_npa_object_fi,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( iext(uri_owl_targetIndividual,sK0(VAR_1,VAR_0,VAR_2),VAR_2)
| iext(VAR_1,VAR_0,VAR_2)
| ~ ir(VAR_2)
| ~ ip(VAR_1)
| ~ ir(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( iext(uri_owl_assertionProperty,sK0(VAR_1,VAR_0,VAR_2),VAR_1)
| iext(VAR_1,VAR_0,VAR_2)
| ~ ir(VAR_2)
| ~ ip(VAR_1)
| ~ ir(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( iext(uri_owl_sourceIndividual,sK0(VAR_1,VAR_0,VAR_2),VAR_0)
| iext(VAR_1,VAR_0,VAR_2)
| ~ ir(VAR_2)
| ~ ip(VAR_1)
| ~ ir(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_owl_npa_object_fi_sk]) ).
cnf(c_11,plain,
( iext(uri_owl_sourceIndividual,sK0(B,A,C),A)
| iext(B,A,C)
| ~ ir(C)
| ~ ip(B)
| ~ ir(A) ),
inference(split_conjunct,[status(thm)],[sk_owl_npa_object_fi]) ).
cnf(c_12,plain,
( ip(B)
| ~ iext(uri_owl_onProperty,A,B) ),
inference(clausify,[status(thm)],[owl_prop_onproperty_ext]) ).
cnf(c_13,plain,
( iext(uri_owl_assertionProperty,sK0(B,A,C),B)
| iext(B,A,C)
| ~ ir(C)
| ~ ip(B)
| ~ ir(A) ),
inference(split_conjunct,[status(thm)],[sk_owl_npa_object_fi]) ).
cnf(c_14,plain,
( iext(uri_owl_targetIndividual,sK0(B,A,C),C)
| iext(B,A,C)
| ~ ir(C)
| ~ ip(B)
| ~ ir(A) ),
inference(split_conjunct,[status(thm)],[sk_owl_npa_object_fi]) ).
cnf(c_32,plain,
ir(A),
inference(clausify,[status(thm)],[simple_ir]) ).
cnf(c_33,plain,
( icext(B,A)
| ~ iext(uri_rdf_type,A,B) ),
inference(clausify,[status(thm)],[rdfs_cext_def]) ).
cnf(c_34,plain,
( ~ icext(B,A)
| iext(uri_rdf_type,A,B) ),
inference(clausify,[status(thm)],[rdfs_cext_def]) ).
cnf(c_35,plain,
( icext(uri_owl_NegativePropertyAssertion,A)
| ~ iext(uri_owl_sourceIndividual,A,B) ),
inference(clausify,[status(thm)],[owl_prop_sourceindividual_ext]) ).
cnf(c_37,plain,
( ~ icext(B,C)
| ~ icext(A,C)
| ~ iext(uri_owl_complementOf,A,B) ),
inference(clausify,[status(thm)],[owl_bool_complementof_class]) ).
cnf(c_40,plain,
( B != D
| icext(C,D)
| ~ iext(uri_owl_oneOf,C,A)
| ~ iext(uri_rdf_rest,A,uri_rdf_nil)
| ~ iext(uri_rdf_first,A,B) ),
inference(clausify,[status(thm)],[owl_enum_class_001]) ).
cnf(c_41,plain,
( icext(B,E)
| ~ iext(C,D,E)
| ~ icext(A,D)
| ~ iext(uri_owl_onProperty,A,C)
| ~ iext(uri_owl_allValuesFrom,A,B) ),
inference(clausify,[status(thm)],[owl_restrict_allvaluesfrom]) ).
fof(nnf_9,plain,
? [BNODE_x1,BNODE_x2,BNODE_x3,BNODE_x4] :
( iext(uri_rdf_rest,BNODE_x4,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_x4,uri_ex_o)
& iext(uri_owl_oneOf,BNODE_x3,BNODE_x4)
& iext(uri_owl_complementOf,BNODE_x2,BNODE_x3)
& iext(uri_owl_allValuesFrom,BNODE_x1,BNODE_x2)
& iext(uri_owl_onProperty,BNODE_x1,uri_ex_p)
& iext(uri_rdf_type,uri_ex_s,BNODE_x1)
& iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty) ),
inference(fof_nnf,[status(thm)],[testcase_premise_fullish_010_Negative_Property_Assertions]) ).
fof(sk_testcase_premise_fullish_010_Negative_Property_Assertions,plain,
( iext(uri_rdf_rest,sK4,uri_rdf_nil)
& iext(uri_rdf_first,sK4,uri_ex_o)
& iext(uri_owl_oneOf,sK3,sK4)
& iext(uri_owl_complementOf,sK2,sK3)
& iext(uri_owl_allValuesFrom,sK1,sK2)
& iext(uri_owl_onProperty,sK1,uri_ex_p)
& iext(uri_rdf_type,uri_ex_s,sK1)
& iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4]),skolemize(BNODE_x1,sK1),skolemize(BNODE_x2,sK2),skolemize(BNODE_x3,sK3),skolemize(BNODE_x4,sK4)],[nnf_9]) ).
cnf(c_45,plain,
iext(uri_rdf_type,uri_ex_s,sK1),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_010_Negative_Property_Assertions]) ).
cnf(c_46,plain,
iext(uri_owl_onProperty,sK1,uri_ex_p),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_010_Negative_Property_Assertions]) ).
cnf(c_47,plain,
iext(uri_owl_allValuesFrom,sK1,sK2),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_010_Negative_Property_Assertions]) ).
cnf(c_48,plain,
iext(uri_owl_complementOf,sK2,sK3),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_010_Negative_Property_Assertions]) ).
cnf(c_49,plain,
iext(uri_owl_oneOf,sK3,sK4),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_010_Negative_Property_Assertions]) ).
cnf(c_50,plain,
iext(uri_rdf_first,sK4,uri_ex_o),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_010_Negative_Property_Assertions]) ).
cnf(c_51,plain,
iext(uri_rdf_rest,sK4,uri_rdf_nil),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_010_Negative_Property_Assertions]) ).
cnf(c_52,negated_conjecture,
( ~ iext(uri_owl_targetIndividual,A,uri_ex_o)
| ~ iext(uri_owl_assertionProperty,A,uri_ex_p)
| ~ iext(uri_owl_sourceIndividual,A,uri_ex_s)
| ~ iext(uri_rdf_type,A,uri_owl_NegativePropertyAssertion) ),
inference(clausify,[status(thm)],[testcase_conclusion_fullish_010_Negative_Property_Assertions_neg]) ).
cnf(c_53,plain,
( ~ iext(uri_owl_onProperty,D,C)
| iext(uri_owl_sourceIndividual,sK0(C,A,B),A)
| iext(C,A,B)
| ~ ir(B)
| ~ ir(A) ),
inference(resolve,[status(thm)],[c_11,c_12]) ).
cnf(c_177,plain,
( ~ iext(uri_owl_onProperty,D,B)
| iext(uri_owl_sourceIndividual,sK0(B,C,A),C)
| iext(B,C,A)
| ~ ir(A) ),
inference(resolve,[status(thm)],[c_32,c_53]) ).
cnf(c_54,plain,
( ~ iext(uri_owl_onProperty,D,A)
| iext(uri_owl_sourceIndividual,sK0(A,B,C),B)
| iext(A,B,C) ),
inference(resolve,[status(thm)],[c_32,c_177]) ).
cnf(c_55,plain,
( ~ iext(uri_owl_onProperty,D,C)
| iext(uri_owl_assertionProperty,sK0(C,A,B),C)
| iext(C,A,B)
| ~ ir(B)
| ~ ir(A) ),
inference(resolve,[status(thm)],[c_13,c_12]) ).
cnf(c_178,plain,
( ~ iext(uri_owl_onProperty,D,B)
| iext(uri_owl_assertionProperty,sK0(B,C,A),B)
| iext(B,C,A)
| ~ ir(A) ),
inference(resolve,[status(thm)],[c_32,c_55]) ).
cnf(c_56,plain,
( ~ iext(uri_owl_onProperty,D,A)
| iext(uri_owl_assertionProperty,sK0(A,B,C),A)
| iext(A,B,C) ),
inference(resolve,[status(thm)],[c_32,c_178]) ).
cnf(c_57,plain,
( ~ iext(uri_owl_onProperty,D,C)
| iext(uri_owl_targetIndividual,sK0(C,A,B),B)
| iext(C,A,B)
| ~ ir(B)
| ~ ir(A) ),
inference(resolve,[status(thm)],[c_14,c_12]) ).
cnf(c_179,plain,
( ~ iext(uri_owl_onProperty,D,B)
| iext(uri_owl_targetIndividual,sK0(B,C,A),A)
| iext(B,C,A)
| ~ ir(A) ),
inference(resolve,[status(thm)],[c_32,c_57]) ).
cnf(c_58,plain,
( ~ iext(uri_owl_onProperty,D,A)
| iext(uri_owl_targetIndividual,sK0(A,B,C),C)
| iext(A,B,C) ),
inference(resolve,[status(thm)],[c_32,c_179]) ).
cnf(c_66,plain,
icext(sK1,uri_ex_s),
inference(resolve,[status(thm)],[c_45,c_33]) ).
cnf(c_70,plain,
( icext(A,C)
| ~ iext(uri_ex_p,B,C)
| ~ icext(sK1,B)
| ~ iext(uri_owl_allValuesFrom,sK1,A) ),
inference(resolve,[status(thm)],[c_46,c_41]) ).
cnf(c_80,plain,
( ~ icext(sK3,A)
| ~ icext(sK2,A) ),
inference(resolve,[status(thm)],[c_48,c_37]) ).
cnf(c_180,plain,
( uri_ex_o != B
| icext(A,B)
| ~ iext(uri_owl_oneOf,A,sK4)
| ~ iext(uri_rdf_rest,sK4,uri_rdf_nil) ),
inference(resolve,[status(thm)],[c_40,c_50]) ).
cnf(c_181,plain,
( uri_ex_o != B
| icext(A,B)
| ~ iext(uri_owl_oneOf,A,sK4) ),
inference(resolve,[status(thm)],[c_180,c_51]) ).
cnf(c_182,plain,
( uri_ex_o != A
| icext(sK3,A) ),
inference(resolve,[status(thm)],[c_181,c_49]) ).
cnf(c_108,plain,
icext(sK3,uri_ex_o),
inference(xxres,[status(thm)],[c_182]) ).
cnf(c_110,plain,
( iext(uri_owl_sourceIndividual,sK0(uri_ex_p,A,B),A)
| iext(uri_ex_p,A,B) ),
inference(resolve,[status(thm)],[c_54,c_46]) ).
cnf(c_111,plain,
( iext(uri_owl_assertionProperty,sK0(uri_ex_p,A,B),uri_ex_p)
| iext(uri_ex_p,A,B) ),
inference(resolve,[status(thm)],[c_56,c_46]) ).
cnf(c_112,plain,
( iext(uri_owl_targetIndividual,sK0(uri_ex_p,A,B),B)
| iext(uri_ex_p,A,B) ),
inference(resolve,[status(thm)],[c_58,c_46]) ).
cnf(c_119,plain,
~ icext(sK2,uri_ex_o),
inference(resolve,[status(thm)],[c_108,c_80]) ).
cnf(c_183,plain,
( icext(sK2,C)
| ~ iext(A,B,C)
| ~ icext(sK1,B)
| ~ iext(uri_owl_onProperty,sK1,A) ),
inference(resolve,[status(thm)],[c_41,c_47]) ).
cnf(c_184,plain,
( icext(sK2,B)
| ~ iext(uri_ex_p,A,B)
| ~ icext(sK1,A) ),
inference(resolve,[status(thm)],[c_183,c_46]) ).
cnf(c_185,plain,
( icext(sK2,A)
| ~ iext(uri_ex_p,uri_ex_s,A) ),
inference(resolve,[status(thm)],[c_184,c_66]) ).
cnf(c_123,plain,
~ iext(uri_ex_p,uri_ex_s,uri_ex_o),
inference(resolve,[status(thm)],[c_185,c_119]) ).
cnf(c_141,plain,
( icext(sK2,B)
| ~ iext(uri_ex_p,A,B)
| ~ icext(sK1,A) ),
inference(resolve,[status(thm)],[c_70,c_47]) ).
cnf(c_155,plain,
( icext(uri_owl_NegativePropertyAssertion,sK0(uri_ex_p,A,B))
| iext(uri_ex_p,A,B) ),
inference(resolve,[status(thm)],[c_110,c_35]) ).
cnf(c_186,plain,
( icext(sK2,A)
| ~ iext(uri_ex_p,uri_ex_s,A) ),
inference(resolve,[status(thm)],[c_141,c_66]) ).
cnf(c_161,plain,
( icext(uri_owl_NegativePropertyAssertion,sK0(uri_ex_p,uri_ex_s,A))
| icext(sK2,A) ),
inference(resolve,[status(thm)],[c_186,c_155]) ).
cnf(c_166,plain,
( iext(uri_rdf_type,sK0(uri_ex_p,uri_ex_s,A),uri_owl_NegativePropertyAssertion)
| icext(sK2,A) ),
inference(resolve,[status(thm)],[c_161,c_34]) ).
cnf(c_187,negated_conjecture,
( icext(sK2,A)
| ~ iext(uri_owl_targetIndividual,sK0(uri_ex_p,uri_ex_s,A),uri_ex_o)
| ~ iext(uri_owl_assertionProperty,sK0(uri_ex_p,uri_ex_s,A),uri_ex_p)
| ~ iext(uri_owl_sourceIndividual,sK0(uri_ex_p,uri_ex_s,A),uri_ex_s) ),
inference(resolve,[status(thm)],[c_52,c_166]) ).
cnf(c_188,negated_conjecture,
( iext(uri_ex_p,uri_ex_s,A)
| icext(sK2,A)
| ~ iext(uri_owl_targetIndividual,sK0(uri_ex_p,uri_ex_s,A),uri_ex_o)
| ~ iext(uri_owl_assertionProperty,sK0(uri_ex_p,uri_ex_s,A),uri_ex_p) ),
inference(resolve,[status(thm)],[c_187,c_110]) ).
cnf(c_189,negated_conjecture,
( iext(uri_ex_p,uri_ex_s,A)
| iext(uri_ex_p,uri_ex_s,A)
| icext(sK2,A)
| ~ iext(uri_owl_targetIndividual,sK0(uri_ex_p,uri_ex_s,A),uri_ex_o) ),
inference(resolve,[status(thm)],[c_188,c_111]) ).
cnf(c_190,negated_conjecture,
( iext(uri_ex_p,uri_ex_s,uri_ex_o)
| iext(uri_ex_p,uri_ex_s,uri_ex_o)
| iext(uri_ex_p,uri_ex_s,uri_ex_o)
| icext(sK2,uri_ex_o) ),
inference(resolve,[status(thm)],[c_189,c_112]) ).
cnf(c_191,negated_conjecture,
( iext(uri_ex_p,uri_ex_s,uri_ex_o)
| iext(uri_ex_p,uri_ex_s,uri_ex_o)
| icext(sK2,uri_ex_o) ),
inference(copy,[status(thm)],[c_190]) ).
cnf(c_192,negated_conjecture,
( iext(uri_ex_p,uri_ex_s,uri_ex_o)
| icext(sK2,uri_ex_o) ),
inference(copy,[status(thm)],[c_191]) ).
cnf(c_193,negated_conjecture,
iext(uri_ex_p,uri_ex_s,uri_ex_o),
inference(resolve,[status(thm)],[c_119,c_192]) ).
cnf(c_176,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_123,c_193]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWB010+2 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.21/0.46 % Computer : n015.cluster.edu
% 0.21/0.46 % Model : x86_64 x86_64
% 0.21/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.21/0.46 % Memory : 8046.5625MB
% 0.21/0.46 % OS : Linux 6.8.0-71-generic
% 0.21/0.46 % CPULimit : 300
% 0.21/0.46 % WCLimit : 300
% 0.21/0.46 % DateTime : Sat Sep 26 11:45:29 UTC 2026
% 0.21/0.46 % CPUTime :
% 0.21/0.47 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.21/0.47 % Process 3952773 was started by sandbox2 on n015,
% 0.21/0.47 % Sat Sep 26 11:45:29 2026
% 0.21/0.47 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.21/0.48
% 0.21/0.48 % From the command line: assign(max_seconds, 300).
% 0.21/0.51
% 0.21/0.51 % SZS status Theorem for theBenchmark
% 0.21/0.51
% 0.21/0.51 % Proof 1 at 0.02 (+ 0.00) seconds.
% 0.21/0.51 % Length of proof is 49.
% 0.21/0.51 % Level of proof is 8.
% 0.21/0.51 % Maximum clause weight is 25.000.
% 0.21/0.51 % Given clauses 108.
% 0.21/0.51
% 0.21/0.51 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------