%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU223+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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:45:29 AM UTC 2026
% Result : Theorem 30.51s 9.82s
% Output : CNFRefutation 30.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 8
% Syntax : Number of formulae : 40 ( 15 unt; 0 def)
% Number of atoms : 108 ( 24 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 114 ( 46 ~; 41 |; 15 &)
% ( 1 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-2 aty)
% Number of variables : 38 ( 2 sgn 19 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(dt_k6_relat_1,axiom,
! [A] : relation(identity_relation(A)),
file('theBenchmark.p',dt_k6_relat_1) ).
fof(fc2_funct_1,axiom,
! [A] :
( function(identity_relation(A))
& relation(identity_relation(A)) ),
file('theBenchmark.p',fc2_funct_1) ).
fof(t21_funct_1,axiom,
! [A,B] :
( ( function(B)
& relation(B) )
=> ! [C] :
( ( function(C)
& relation(C) )
=> ( in(A,relation_dom(relation_composition(C,B)))
<=> ( in(apply(C,A),relation_dom(B))
& in(A,relation_dom(C)) ) ) ) ),
file('theBenchmark.p',t21_funct_1) ).
fof(t22_funct_1,axiom,
! [A,B] :
( ( function(B)
& relation(B) )
=> ! [C] :
( ( function(C)
& relation(C) )
=> ( in(A,relation_dom(relation_composition(C,B)))
=> apply(relation_composition(C,B),A) = apply(B,apply(C,A)) ) ) ),
file('theBenchmark.p',t22_funct_1) ).
fof(t35_funct_1,axiom,
! [A,B] :
( in(B,A)
=> apply(identity_relation(A),B) = B ),
file('theBenchmark.p',t35_funct_1) ).
fof(t71_relat_1,axiom,
! [A] :
( relation_rng(identity_relation(A)) = A
& relation_dom(identity_relation(A)) = A ),
file('theBenchmark.p',t71_relat_1) ).
fof(t94_relat_1,axiom,
! [A,B] :
( relation(B)
=> relation_dom_restriction(B,A) = relation_composition(identity_relation(A),B) ),
file('theBenchmark.p',t94_relat_1) ).
fof(t70_funct_1,conjecture,
! [A,B,C] :
( ( function(C)
& relation(C) )
=> ( in(B,relation_dom(relation_dom_restriction(C,A)))
=> apply(relation_dom_restriction(C,A),B) = apply(C,B) ) ),
file('theBenchmark.p',t70_funct_1) ).
fof(t70_funct_1_neg,negated_conjecture,
~ ! [A,B,C] :
( ( function(C)
& relation(C) )
=> ( in(B,relation_dom(relation_dom_restriction(C,A)))
=> apply(relation_dom_restriction(C,A),B) = apply(C,B) ) ),
inference(assume_negation,[status(cth)],[t70_funct_1]) ).
cnf(c_463,plain,
relation(identity_relation(A)),
inference(clausify,[status(thm)],[dt_k6_relat_1]) ).
cnf(c_478,plain,
function(identity_relation(A)),
inference(clausify,[status(thm)],[fc2_funct_1]) ).
cnf(c_555,plain,
( in(C,relation_dom(B))
| ~ in(C,relation_dom(relation_composition(B,A)))
| ~ function(B)
| ~ relation(B)
| ~ function(A)
| ~ relation(A) ),
inference(clausify,[status(thm)],[t21_funct_1]) ).
cnf(c_558,plain,
( apply(relation_composition(B,A),C) = apply(A,apply(B,C))
| ~ in(C,relation_dom(relation_composition(B,A)))
| ~ function(B)
| ~ relation(B)
| ~ function(A)
| ~ relation(A) ),
inference(clausify,[status(thm)],[t22_funct_1]) ).
cnf(c_575,plain,
( apply(identity_relation(B),A) = A
| ~ in(A,B) ),
inference(clausify,[status(thm)],[t35_funct_1]) ).
cnf(c_648,plain,
relation_dom(identity_relation(A)) = A,
inference(clausify,[status(thm)],[t71_relat_1]) ).
cnf(c_666,plain,
( relation_composition(identity_relation(B),A) = relation_dom_restriction(A,B)
| ~ relation(A) ),
inference(clausify,[status(thm)],[t94_relat_1]) ).
cnf(c_667,plain,
( relation_dom_restriction(A,B) = relation_composition(identity_relation(B),A)
| ~ relation(A) ),
inference(copy,[status(thm)],[c_666]) ).
fof(nnf_236,plain,
? [A,B,C] :
( apply(relation_dom_restriction(C,A),B) != apply(C,B)
& in(B,relation_dom(relation_dom_restriction(C,A)))
& function(C)
& relation(C) ),
inference(fof_nnf,[status(thm)],[t70_funct_1_neg]) ).
fof(sk_t70_funct_1_neg,plain,
( apply(relation_dom_restriction(sK0,sK2),sK1) != apply(sK0,sK1)
& in(sK1,relation_dom(relation_dom_restriction(sK0,sK2)))
& function(sK0)
& relation(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(A,sK2),skolemize(B,sK1),skolemize(C,sK0)],[nnf_236]) ).
cnf(c_670,negated_conjecture,
relation(sK0),
inference(split_conjunct,[status(thm)],[sk_t70_funct_1_neg]) ).
cnf(c_671,negated_conjecture,
function(sK0),
inference(split_conjunct,[status(thm)],[sk_t70_funct_1_neg]) ).
cnf(c_672,negated_conjecture,
in(sK1,relation_dom(relation_dom_restriction(sK0,sK2))),
inference(split_conjunct,[status(thm)],[sk_t70_funct_1_neg]) ).
cnf(c_673,negated_conjecture,
apply(relation_dom_restriction(sK0,sK2),sK1) != apply(sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_t70_funct_1_neg]) ).
cnf(c_7088,plain,
relation_dom_restriction(sK0,A) = relation_composition(identity_relation(A),sK0),
inference(resolve,[status(thm)],[c_667,c_670]) ).
cnf(c_8662,negated_conjecture,
apply(relation_composition(identity_relation(sK2),sK0),sK1) != apply(sK0,sK1),
inference(paramod,[status(thm)],[c_7088,c_673]) ).
cnf(c_8663,negated_conjecture,
in(sK1,relation_dom(relation_composition(identity_relation(sK2),sK0))),
inference(paramod,[status(thm)],[c_7088,c_672]) ).
cnf(c_24516,negated_conjecture,
( in(sK1,relation_dom(identity_relation(sK2)))
| ~ function(identity_relation(sK2))
| ~ relation(identity_relation(sK2))
| ~ function(sK0)
| ~ relation(sK0) ),
inference(resolve,[status(thm)],[c_555,c_8663]) ).
cnf(c_24517,negated_conjecture,
( in(sK1,sK2)
| ~ function(identity_relation(sK2))
| ~ relation(identity_relation(sK2))
| ~ function(sK0)
| ~ relation(sK0) ),
inference(paramod,[status(thm)],[c_648,c_24516]) ).
cnf(c_24518,negated_conjecture,
( in(sK1,sK2)
| ~ function(identity_relation(sK2))
| ~ relation(identity_relation(sK2))
| ~ function(sK0) ),
inference(resolve,[status(thm)],[c_670,c_24517]) ).
cnf(c_24519,negated_conjecture,
( in(sK1,sK2)
| ~ function(identity_relation(sK2))
| ~ relation(identity_relation(sK2)) ),
inference(resolve,[status(thm)],[c_671,c_24518]) ).
cnf(c_24520,negated_conjecture,
( in(sK1,sK2)
| ~ function(identity_relation(sK2)) ),
inference(resolve,[status(thm)],[c_463,c_24519]) ).
cnf(c_24354,negated_conjecture,
in(sK1,sK2),
inference(resolve,[status(thm)],[c_478,c_24520]) ).
cnf(c_24383,plain,
apply(identity_relation(sK2),sK1) = sK1,
inference(resolve,[status(thm)],[c_24354,c_575]) ).
cnf(c_24521,negated_conjecture,
( apply(relation_composition(identity_relation(sK2),sK0),sK1) = apply(sK0,apply(identity_relation(sK2),sK1))
| ~ function(identity_relation(sK2))
| ~ relation(identity_relation(sK2))
| ~ function(sK0)
| ~ relation(sK0) ),
inference(resolve,[status(thm)],[c_558,c_8663]) ).
cnf(c_24522,negated_conjecture,
( apply(relation_composition(identity_relation(sK2),sK0),sK1) = apply(sK0,sK1)
| ~ function(identity_relation(sK2))
| ~ relation(identity_relation(sK2))
| ~ function(sK0)
| ~ relation(sK0) ),
inference(paramod,[status(thm)],[c_24383,c_24521]) ).
cnf(c_24523,negated_conjecture,
( apply(relation_composition(identity_relation(sK2),sK0),sK1) = apply(sK0,sK1)
| ~ function(identity_relation(sK2))
| ~ relation(identity_relation(sK2))
| ~ function(sK0) ),
inference(resolve,[status(thm)],[c_670,c_24522]) ).
cnf(c_24524,negated_conjecture,
( apply(relation_composition(identity_relation(sK2),sK0),sK1) = apply(sK0,sK1)
| ~ function(identity_relation(sK2))
| ~ relation(identity_relation(sK2)) ),
inference(resolve,[status(thm)],[c_671,c_24523]) ).
cnf(c_24525,negated_conjecture,
( apply(relation_composition(identity_relation(sK2),sK0),sK1) = apply(sK0,sK1)
| ~ function(identity_relation(sK2)) ),
inference(resolve,[status(thm)],[c_463,c_24524]) ).
cnf(c_24526,negated_conjecture,
apply(relation_composition(identity_relation(sK2),sK0),sK1) = apply(sK0,sK1),
inference(resolve,[status(thm)],[c_478,c_24525]) ).
cnf(c_24515,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_8662,c_24526]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU223+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.36 % Computer : n019.cluster.edu
% 0.09/5.36 % Model : x86_64 x86_64
% 0.09/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.36 % Memory : 8046.5625MB
% 0.09/5.36 % OS : Linux 6.8.0-71-generic
% 0.09/5.36 % CPULimit : 300
% 0.09/5.36 % WCLimit : 300
% 0.09/5.36 % DateTime : Sat Sep 26 08:53:56 UTC 2026
% 0.09/5.36 % CPUTime :
% 0.09/5.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/5.36 % Process 906583 was started by sandbox2 on n019,
% 0.09/5.36 % Sat Sep 26 08:53:56 2026
% 0.09/5.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.14/5.42
% 0.14/5.42 % From the command line: assign(max_seconds, 300).
% 0.14/5.42
% 0.14/5.42 % SInE: 181 to sos, 56 to usable, of 237 axioms (tolerance 2.00, depth 0 fixpoint).
% 30.51/9.82
% 30.51/9.82 % given #500 (A,wt=211): 389 set_union2(A,B) != C | in(D,C) | -in(D,B) # tptp_name(d2_xboole_0) # sine_depth(3). [clausify(18)].
% 30.51/9.82
% 30.51/9.82 % given #1000 (T,wt=9): 11707 relation(relation_composition(identity_relation(A),set_difference(c1,set_difference(c1,c8)))). [resolve(11666,a,466,a),rewrite([11701(6)])].
% 30.51/9.82
% 30.51/9.82 % given #1500 (W,wt=5): 17618 relation(relation_dom(f42(f42(c4)))). [resolve(17201,a,488,a)].
% 30.51/9.82
% 30.51/9.82 % SZS status Theorem for theBenchmark
% 30.51/9.82
% 30.51/9.82 % Proof 1 at 3.52 (+ 0.80) seconds.
% 30.51/9.82 % Length of proof is 26.
% 30.51/9.82 % Level of proof is 7.
% 30.51/9.82 % Maximum clause weight is 105.000.
% 30.51/9.82 % Given clauses 1919.
% 30.51/9.82
% 30.51/9.82 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------