%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM139-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.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:16:11 AM UTC 2026
% Result : Unsatisfiable 2.21s 1.08s
% Output : CNFRefutation 2.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 10
% Syntax : Number of formulae : 42 ( 38 unt; 0 def)
% Number of atoms : 46 ( 19 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 22 ( 18 ~; 4 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 11 ( 3 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 4 con; 0-3 aty)
% Number of variables : 46 ( 1 sgn 16 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(prove_complete_induction3_2,axiom,
~ subclass(intersection(power_class(x),z),x),
file('theBenchmark.p',prove_complete_induction3_2) ).
cnf(c_53,plain,
~ subclass(intersection(power_class(x),z),x),
inference(clausify,[status(thm)],[prove_complete_induction3_2]) ).
fof(prove_complete_induction3_1,axiom,
~ member(not_subclass_element(intersection(power_class(x),z),x),z),
file('theBenchmark.p',prove_complete_induction3_1) ).
cnf(c_54,plain,
~ member(not_subclass_element(intersection(power_class(x),z),x),z),
inference(clausify,[status(thm)],[prove_complete_induction3_1]) ).
fof(power_class_definition,axiom,
! [VAR_0] : complement(image(element_relation,complement(VAR_0))) = power_class(VAR_0),
file('theBenchmark.p',power_class_definition) ).
cnf(c_142,plain,
complement(image(element_relation,complement(A))) = power_class(A),
inference(clausify,[status(thm)],[power_class_definition]) ).
cnf(c_143,plain,
power_class(A) = complement(image(element_relation,complement(A))),
inference(copy,[status(thm)],[c_142]) ).
fof(image,axiom,
! [VAR_0,VAR_1] : range_of(restrict(VAR_0,VAR_1,universal_class)) = image(VAR_0,VAR_1),
file('theBenchmark.p',image) ).
cnf(c_153,plain,
range_of(restrict(A,B,universal_class)) = image(A,B),
inference(clausify,[status(thm)],[image]) ).
cnf(c_154,plain,
image(A,B) = range_of(restrict(A,B,universal_class)),
inference(copy,[status(thm)],[c_153]) ).
fof(range_of,axiom,
! [VAR_0] : domain_of(inverse(VAR_0)) = range_of(VAR_0),
file('theBenchmark.p',range_of) ).
cnf(c_159,plain,
domain_of(inverse(A)) = range_of(A),
inference(clausify,[status(thm)],[range_of]) ).
cnf(c_160,plain,
range_of(A) = domain_of(inverse(A)),
inference(copy,[status(thm)],[c_159]) ).
fof(inverse,axiom,
! [VAR_0] : domain_of(flip(cross_product(VAR_0,universal_class))) = inverse(VAR_0),
file('theBenchmark.p',inverse) ).
cnf(c_161,plain,
domain_of(flip(cross_product(A,universal_class))) = inverse(A),
inference(clausify,[status(thm)],[inverse]) ).
cnf(c_162,plain,
inverse(A) = domain_of(flip(cross_product(A,universal_class))),
inference(copy,[status(thm)],[c_161]) ).
fof(restriction2,axiom,
! [VAR_0,VAR_1,VAR_2] : intersection(cross_product(VAR_0,VAR_1),VAR_2) = restrict(VAR_2,VAR_0,VAR_1),
file('theBenchmark.p',restriction2) ).
cnf(c_171,plain,
intersection(cross_product(A,B),C) = restrict(C,A,B),
inference(clausify,[status(thm)],[restriction2]) ).
cnf(c_172,plain,
restrict(A,B,C) = intersection(cross_product(B,C),A),
inference(copy,[status(thm)],[c_171]) ).
fof(restriction1,axiom,
! [VAR_0,VAR_1,VAR_2] : intersection(VAR_0,cross_product(VAR_1,VAR_2)) = restrict(VAR_0,VAR_1,VAR_2),
file('theBenchmark.p',restriction1) ).
cnf(c_173,plain,
intersection(A,cross_product(B,C)) = restrict(A,B,C),
inference(clausify,[status(thm)],[restriction1]) ).
cnf(c_2215,plain,
intersection(A,cross_product(B,C)) = intersection(cross_product(B,C),A),
inference(paramod,[status(thm)],[c_172,c_173]) ).
cnf(c_174,plain,
intersection(cross_product(A,B),C) = intersection(C,cross_product(A,B)),
inference(copy,[status(thm)],[c_2215]) ).
fof(intersection2,axiom,
! [VAR_0,VAR_1,VAR_2] :
( member(VAR_0,VAR_2)
| ~ member(VAR_0,intersection(VAR_1,VAR_2)) ),
file('theBenchmark.p',intersection2) ).
cnf(c_182,plain,
( member(A,C)
| ~ member(A,intersection(B,C)) ),
inference(clausify,[status(thm)],[intersection2]) ).
fof(not_subclass_members1,axiom,
! [VAR_0,VAR_1] :
( subclass(VAR_0,VAR_1)
| member(not_subclass_element(VAR_0,VAR_1),VAR_0) ),
file('theBenchmark.p',not_subclass_members1) ).
cnf(c_204,plain,
( subclass(A,B)
| member(not_subclass_element(A,B),A) ),
inference(clausify,[status(thm)],[not_subclass_members1]) ).
cnf(c_2216,plain,
~ member(not_subclass_element(intersection(complement(image(element_relation,complement(x))),z),x),z),
inference(paramod,[status(thm)],[c_143,c_54]) ).
cnf(c_2217,plain,
~ member(not_subclass_element(intersection(complement(range_of(restrict(element_relation,complement(x),universal_class))),z),x),z),
inference(paramod,[status(thm)],[c_154,c_2216]) ).
cnf(c_2218,plain,
~ member(not_subclass_element(intersection(complement(range_of(intersection(cross_product(complement(x),universal_class),element_relation))),z),x),z),
inference(paramod,[status(thm)],[c_172,c_2217]) ).
cnf(c_2219,plain,
~ member(not_subclass_element(intersection(complement(range_of(intersection(element_relation,cross_product(complement(x),universal_class)))),z),x),z),
inference(paramod,[status(thm)],[c_174,c_2218]) ).
cnf(c_2220,plain,
~ member(not_subclass_element(intersection(complement(domain_of(inverse(intersection(element_relation,cross_product(complement(x),universal_class))))),z),x),z),
inference(paramod,[status(thm)],[c_160,c_2219]) ).
cnf(c_231,plain,
~ member(not_subclass_element(intersection(complement(domain_of(domain_of(flip(cross_product(intersection(element_relation,cross_product(complement(x),universal_class)),universal_class))))),z),x),z),
inference(paramod,[status(thm)],[c_162,c_2220]) ).
cnf(c_2221,plain,
~ subclass(intersection(complement(image(element_relation,complement(x))),z),x),
inference(paramod,[status(thm)],[c_143,c_53]) ).
cnf(c_2222,plain,
~ subclass(intersection(complement(range_of(restrict(element_relation,complement(x),universal_class))),z),x),
inference(paramod,[status(thm)],[c_154,c_2221]) ).
cnf(c_2223,plain,
~ subclass(intersection(complement(range_of(intersection(cross_product(complement(x),universal_class),element_relation))),z),x),
inference(paramod,[status(thm)],[c_172,c_2222]) ).
cnf(c_2224,plain,
~ subclass(intersection(complement(range_of(intersection(element_relation,cross_product(complement(x),universal_class)))),z),x),
inference(paramod,[status(thm)],[c_174,c_2223]) ).
cnf(c_2225,plain,
~ subclass(intersection(complement(domain_of(inverse(intersection(element_relation,cross_product(complement(x),universal_class))))),z),x),
inference(paramod,[status(thm)],[c_160,c_2224]) ).
cnf(c_232,plain,
~ subclass(intersection(complement(domain_of(domain_of(flip(cross_product(intersection(element_relation,cross_product(complement(x),universal_class)),universal_class))))),z),x),
inference(paramod,[status(thm)],[c_162,c_2225]) ).
cnf(c_447,plain,
member(not_subclass_element(intersection(complement(domain_of(domain_of(flip(cross_product(intersection(element_relation,cross_product(complement(x),universal_class)),universal_class))))),z),x),intersection(complement(domain_of(domain_of(flip(cross_product(intersection(element_relation,cross_product(complement(x),universal_class)),universal_class))))),z)),
inference(resolve,[status(thm)],[c_232,c_204]) ).
cnf(c_2226,plain,
member(not_subclass_element(intersection(complement(domain_of(domain_of(flip(cross_product(intersection(element_relation,cross_product(complement(x),universal_class)),universal_class))))),z),x),z),
inference(resolve,[status(thm)],[c_447,c_182]) ).
cnf(c_2214,plain,
$false,
inference(resolve,[status(thm)],[c_231,c_2226]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM139-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n006.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.36 % CPULimit : 300
% 0.07/0.36 % WCLimit : 300
% 0.07/0.36 % DateTime : Sat Sep 26 02:05:55 UTC 2026
% 0.07/0.36 % CPUTime :
% 0.07/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/0.36 % Process 142279 was started by sandbox on n006,
% 0.07/0.36 % Sat Sep 26 02:05:55 2026
% 0.07/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.07/0.36
% 0.07/0.36 % From the command line: assign(max_seconds, 300).
% 2.21/1.08
% 2.21/1.08 % SZS status Unsatisfiable for theBenchmark
% 2.21/1.08
% 2.21/1.08 % Proof 1 at 0.25 (+ 0.06) seconds.
% 2.21/1.08 % Length of proof is 20.
% 2.21/1.08 % Level of proof is 5.
% 2.21/1.08 % Maximum clause weight is 96.000.
% 2.21/1.08 % Given clauses 454.
% 2.21/1.08
% 2.21/1.08 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------