%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU266+1 : 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 : n011.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:38 AM UTC 2026
% Result : Theorem 4.17s 0.94s
% Output : CNFRefutation 4.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 14
% Syntax : Number of formulae : 88 ( 15 unt; 0 def)
% Number of atoms : 262 ( 76 equ)
% Maximal formula atoms : 16 ( 2 avg)
% Number of connectives : 284 ( 110 ~; 129 |; 27 &)
% ( 6 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 4 con; 0-3 aty)
% Number of variables : 183 ( 21 sgn 82 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cc1_relset_1,axiom,
! [A,B,C] :
( element(C,powerset(cartesian_product2(A,B)))
=> relation(C) ),
file('theBenchmark.p',cc1_relset_1) ).
fof(commutativity_k2_tarski,axiom,
! [A,B] : unordered_pair(A,B) = unordered_pair(B,A),
file('theBenchmark.p',commutativity_k2_tarski) ).
fof(d5_relat_1,axiom,
! [A] :
( relation(A)
=> ! [B] :
( B = relation_rng(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] : in(ordered_pair(D,C),A) ) ) ),
file('theBenchmark.p',d5_relat_1) ).
fof(d5_tarski,axiom,
! [A,B] : ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)),
file('theBenchmark.p',d5_tarski) ).
fof(dt_k5_relset_1,axiom,
! [A,B,C] :
( relation_of2(C,A,B)
=> element(relation_rng_as_subset(A,B,C),powerset(B)) ),
file('theBenchmark.p',dt_k5_relset_1) ).
fof(dt_m2_relset_1,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
=> element(C,powerset(cartesian_product2(A,B))) ),
file('theBenchmark.p',dt_m2_relset_1) ).
fof(redefinition_k5_relset_1,axiom,
! [A,B,C] :
( relation_of2(C,A,B)
=> relation_rng_as_subset(A,B,C) = relation_rng(C) ),
file('theBenchmark.p',redefinition_k5_relset_1) ).
fof(redefinition_m2_relset_1,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
<=> relation_of2(C,A,B) ),
file('theBenchmark.p',redefinition_m2_relset_1) ).
fof(t20_relat_1,axiom,
! [A,B,C] :
( relation(C)
=> ( in(ordered_pair(A,B),C)
=> ( in(B,relation_rng(C))
& in(A,relation_dom(C)) ) ) ),
file('theBenchmark.p',t20_relat_1) ).
fof(t2_subset,axiom,
! [A,B] :
( element(A,B)
=> ( in(A,B)
| empty(B) ) ),
file('theBenchmark.p',t2_subset) ).
fof(t2_tarski,axiom,
! [A,B] :
( ! [C] :
( in(C,A)
<=> in(C,B) )
=> A = B ),
file('theBenchmark.p',t2_tarski) ).
fof(t4_subset,axiom,
! [A,B,C] :
( ( element(B,powerset(C))
& in(A,B) )
=> element(A,C) ),
file('theBenchmark.p',t4_subset) ).
fof(t5_subset,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('theBenchmark.p',t5_subset) ).
fof(t23_relset_1,conjecture,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
=> ( ! [D] :
~ ( ! [E] : ~ in(ordered_pair(E,D),C)
& in(D,B) )
<=> relation_rng_as_subset(A,B,C) = B ) ),
file('theBenchmark.p',t23_relset_1) ).
fof(t23_relset_1_neg,negated_conjecture,
~ ! [A,B,C] :
( relation_of2_as_subset(C,A,B)
=> ( ! [D] :
~ ( ! [E] : ~ in(ordered_pair(E,D),C)
& in(D,B) )
<=> relation_rng_as_subset(A,B,C) = B ) ),
inference(assume_negation,[status(cth)],[t23_relset_1]) ).
fof(nnf_4,plain,
! [A] :
( ! [B] :
( ( ? [C] :
( ( ! [D] : ~ in(ordered_pair(D,C),A)
| ~ in(C,B) )
& ( ? [X3] : in(ordered_pair(X3,C),A)
| in(C,B) ) )
| relation_rng(A) = B )
& ( ! [X0] :
( ( ! [X2] : ~ in(ordered_pair(X2,X0),A)
| in(X0,B) )
& ( ? [X1] : in(ordered_pair(X1,X0),A)
| ~ in(X0,B) ) )
| relation_rng(A) != B ) )
| ~ relation(A) ),
inference(fof_nnf,[status(thm)],[d5_relat_1]) ).
fof(sk_d5_relat_1_sk,plain,
! [A] :
( ! [B] :
( ( ( ( ! [D] : ~ in(ordered_pair(D,sK7(A,B)),A)
| ~ in(sK7(A,B),B) )
& ( in(ordered_pair(sK8(A,B),sK7(A,B)),A)
| in(sK7(A,B),B) ) )
| relation_rng(A) = B )
& ( ! [X0] :
( ( ! [X2] : ~ in(ordered_pair(X2,X0),A)
| in(X0,B) )
& ( in(ordered_pair(sK0(A,B,X0),X0),A)
| ~ in(X0,B) ) )
| relation_rng(A) != B ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK7,sK8]),skolemize(X1,sK0(A,B,X0)),skolemize(C,sK7(A,B)),skolemize(X3,sK8(A,B))],[nnf_4]) ).
fof(sk_d5_relat_1,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( ~ in(ordered_pair(VAR_2,sK7(VAR_0,VAR_1)),VAR_0)
| ~ in(sK7(VAR_0,VAR_1),VAR_1)
| relation_rng(VAR_0) = VAR_1
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( in(ordered_pair(sK8(VAR_0,VAR_1),sK7(VAR_0,VAR_1)),VAR_0)
| in(sK7(VAR_0,VAR_1),VAR_1)
| relation_rng(VAR_0) = VAR_1
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ in(ordered_pair(VAR_3,VAR_2),VAR_0)
| in(VAR_2,VAR_1)
| relation_rng(VAR_0) != VAR_1
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(ordered_pair(sK0(VAR_0,VAR_1,VAR_2),VAR_2),VAR_0)
| ~ in(VAR_2,VAR_1)
| relation_rng(VAR_0) != VAR_1
| ~ relation(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_d5_relat_1_sk]) ).
cnf(c_38,plain,
( in(ordered_pair(sK0(A,B,C),C),A)
| ~ in(C,B)
| relation_rng(A) != B
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d5_relat_1]) ).
cnf(c_39,plain,
( relation(A)
| ~ element(A,powerset(cartesian_product2(B,C))) ),
inference(clausify,[status(thm)],[cc1_relset_1]) ).
cnf(c_44,plain,
( in(C,relation_rng(A))
| ~ in(ordered_pair(B,C),A)
| ~ relation(A) ),
inference(clausify,[status(thm)],[t20_relat_1]) ).
cnf(c_45,plain,
( relation_of2(A,B,C)
| ~ relation_of2_as_subset(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_m2_relset_1]) ).
cnf(c_47,plain,
( relation_rng_as_subset(B,C,A) = relation_rng(A)
| ~ relation_of2(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_k5_relset_1]) ).
cnf(c_49,plain,
( element(relation_rng_as_subset(B,C,A),powerset(C))
| ~ relation_of2(A,B,C) ),
inference(clausify,[status(thm)],[dt_k5_relset_1]) ).
cnf(c_51,plain,
( ~ relation_of2_as_subset(C,A,B)
| element(relation_rng_as_subset(A,B,C),powerset(B)) ),
inference(resolve,[status(thm)],[c_49,c_45]) ).
cnf(c_52,plain,
( ~ relation_of2_as_subset(C,A,B)
| relation_rng_as_subset(A,B,C) = relation_rng(C) ),
inference(resolve,[status(thm)],[c_47,c_45]) ).
cnf(c_53,plain,
( element(A,powerset(cartesian_product2(B,C)))
| ~ relation_of2_as_subset(A,B,C) ),
inference(clausify,[status(thm)],[dt_m2_relset_1]) ).
fof(nnf_37,plain,
? [A,B,C] :
( ( relation_rng_as_subset(A,B,C) != B
| ? [D] :
( ! [E] : ~ in(ordered_pair(E,D),C)
& in(D,B) ) )
& ( relation_rng_as_subset(A,B,C) = B
| ! [X3] :
( ? [X0] : in(ordered_pair(X0,X3),C)
| ~ in(X3,B) ) )
& relation_of2_as_subset(C,A,B) ),
inference(fof_nnf,[status(thm)],[t23_relset_1_neg]) ).
fof(sk_t23_relset_1_neg_sk,plain,
( ( relation_rng_as_subset(sK2,sK3,sK1) != sK3
| ( ! [E] : ~ in(ordered_pair(E,sK6),sK1)
& in(sK6,sK3) ) )
& ( relation_rng_as_subset(sK2,sK3,sK1) = sK3
| ! [X3] :
( in(ordered_pair(sK5(X3),X3),sK1)
| ~ in(X3,sK3) ) )
& relation_of2_as_subset(sK1,sK2,sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK5,sK6]),skolemize(A,sK2),skolemize(B,sK3),skolemize(C,sK1),skolemize(X0,sK5(X3)),skolemize(D,sK6)],[nnf_37]) ).
fof(sk_t23_relset_1_neg,plain,
( ! [VAR_0] :
( relation_rng_as_subset(sK2,sK3,sK1) != sK3
| ~ in(ordered_pair(VAR_0,sK6),sK1) )
& ( relation_rng_as_subset(sK2,sK3,sK1) != sK3
| in(sK6,sK3) )
& ! [VAR_0] :
( relation_rng_as_subset(sK2,sK3,sK1) = sK3
| in(ordered_pair(sK5(VAR_0),VAR_0),sK1)
| ~ in(VAR_0,sK3) )
& relation_of2_as_subset(sK1,sK2,sK3) ),
inference(cnf_transformation,[status(thm)],[sk_t23_relset_1_neg_sk]) ).
cnf(c_55,negated_conjecture,
relation_of2_as_subset(sK1,sK2,sK3),
inference(split_conjunct,[status(thm)],[sk_t23_relset_1_neg]) ).
cnf(c_63,plain,
unordered_pair(A,B) = unordered_pair(B,A),
inference(clausify,[status(thm)],[commutativity_k2_tarski]) ).
cnf(c_64,plain,
ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)),
inference(clausify,[status(thm)],[d5_tarski]) ).
cnf(c_72,plain,
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(clausify,[status(thm)],[t2_subset]) ).
fof(nnf_30,plain,
! [A,B] :
( B = A
| ? [C] :
( ( ~ in(C,B)
| ~ in(C,A) )
& ( in(C,B)
| in(C,A) ) ) ),
inference(fof_nnf,[status(thm)],[t2_tarski]) ).
fof(sk_t2_tarski_sk,plain,
! [A,B] :
( B = A
| ( ( ~ in(sK4(A,B),B)
| ~ in(sK4(A,B),A) )
& ( in(sK4(A,B),B)
| in(sK4(A,B),A) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(C,sK4(A,B))],[nnf_30]) ).
fof(sk_t2_tarski,plain,
( ! [VAR_0,VAR_1] :
( VAR_1 = VAR_0
| ~ in(sK4(VAR_0,VAR_1),VAR_1)
| ~ in(sK4(VAR_0,VAR_1),VAR_0) )
& ! [VAR_0,VAR_1] :
( VAR_1 = VAR_0
| in(sK4(VAR_0,VAR_1),VAR_1)
| in(sK4(VAR_0,VAR_1),VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_t2_tarski_sk]) ).
cnf(c_73,plain,
( B = A
| in(sK4(A,B),B)
| in(sK4(A,B),A) ),
inference(split_conjunct,[status(thm)],[sk_t2_tarski]) ).
cnf(c_74,plain,
( B = A
| ~ in(sK4(A,B),B)
| ~ in(sK4(A,B),A) ),
inference(split_conjunct,[status(thm)],[sk_t2_tarski]) ).
cnf(c_75,plain,
( element(A,C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(clausify,[status(thm)],[t4_subset]) ).
cnf(c_76,plain,
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(clausify,[status(thm)],[t5_subset]) ).
cnf(c_80,negated_conjecture,
( relation_rng_as_subset(sK2,sK3,sK1) = sK3
| in(ordered_pair(sK5(A),A),sK1)
| ~ in(A,sK3) ),
inference(split_conjunct,[status(thm)],[sk_t23_relset_1_neg]) ).
cnf(c_2429,negated_conjecture,
( relation_rng_as_subset(sK2,sK3,sK1) = sK3
| in(unordered_pair(unordered_pair(sK5(A),A),singleton(sK5(A))),sK1)
| ~ in(A,sK3) ),
inference(paramod,[status(thm)],[c_64,c_80]) ).
cnf(c_81,negated_conjecture,
( relation_rng_as_subset(sK2,sK3,sK1) = sK3
| in(unordered_pair(unordered_pair(A,sK5(A)),singleton(sK5(A))),sK1)
| ~ in(A,sK3) ),
inference(paramod,[status(thm)],[c_63,c_2429]) ).
cnf(c_82,negated_conjecture,
( relation_rng_as_subset(sK2,sK3,sK1) != sK3
| in(sK6,sK3) ),
inference(split_conjunct,[status(thm)],[sk_t23_relset_1_neg]) ).
cnf(c_83,negated_conjecture,
( relation_rng_as_subset(sK2,sK3,sK1) != sK3
| ~ in(ordered_pair(A,sK6),sK1) ),
inference(split_conjunct,[status(thm)],[sk_t23_relset_1_neg]) ).
cnf(c_84,negated_conjecture,
( relation_rng_as_subset(sK2,sK3,sK1) != sK3
| ~ in(unordered_pair(unordered_pair(A,sK6),singleton(A)),sK1) ),
inference(paramod,[status(thm)],[c_64,c_83]) ).
cnf(c_85,plain,
( ~ element(A,powerset(cartesian_product2(D,E)))
| in(ordered_pair(sK0(A,B,C),C),A)
| ~ in(C,B)
| relation_rng(A) != B ),
inference(resolve,[status(thm)],[c_38,c_39]) ).
cnf(c_2430,plain,
( ~ element(A,powerset(cartesian_product2(D,E)))
| in(unordered_pair(unordered_pair(sK0(A,B,C),C),singleton(sK0(A,B,C))),A)
| ~ in(C,B)
| relation_rng(A) != B ),
inference(paramod,[status(thm)],[c_64,c_85]) ).
cnf(c_86,plain,
( ~ element(A,powerset(cartesian_product2(D,E)))
| in(unordered_pair(unordered_pair(C,sK0(A,B,C)),singleton(sK0(A,B,C))),A)
| ~ in(C,B)
| relation_rng(A) != B ),
inference(paramod,[status(thm)],[c_63,c_2430]) ).
cnf(c_95,plain,
( ~ element(C,powerset(cartesian_product2(D,E)))
| in(B,relation_rng(C))
| ~ in(ordered_pair(A,B),C) ),
inference(resolve,[status(thm)],[c_44,c_39]) ).
cnf(c_96,plain,
( ~ element(C,powerset(cartesian_product2(D,E)))
| in(B,relation_rng(C))
| ~ in(unordered_pair(unordered_pair(A,B),singleton(A)),C) ),
inference(paramod,[status(thm)],[c_64,c_95]) ).
cnf(c_105,negated_conjecture,
element(sK1,powerset(cartesian_product2(sK2,sK3))),
inference(resolve,[status(thm)],[c_55,c_53]) ).
cnf(c_106,negated_conjecture,
relation_rng_as_subset(sK2,sK3,sK1) = relation_rng(sK1),
inference(resolve,[status(thm)],[c_55,c_52]) ).
cnf(c_107,negated_conjecture,
element(relation_rng_as_subset(sK2,sK3,sK1),powerset(sK3)),
inference(resolve,[status(thm)],[c_55,c_51]) ).
cnf(c_108,negated_conjecture,
element(relation_rng(sK1),powerset(sK3)),
inference(paramod,[status(thm)],[c_106,c_107]) ).
cnf(c_110,negated_conjecture,
( relation_rng(sK1) != sK3
| ~ in(unordered_pair(unordered_pair(A,sK6),singleton(A)),sK1) ),
inference(paramod,[status(thm)],[c_106,c_84]) ).
cnf(c_111,negated_conjecture,
( relation_rng(sK1) != sK3
| in(sK6,sK3) ),
inference(paramod,[status(thm)],[c_106,c_82]) ).
cnf(c_112,negated_conjecture,
( relation_rng(sK1) = sK3
| in(unordered_pair(unordered_pair(A,sK5(A)),singleton(sK5(A))),sK1)
| ~ in(A,sK3) ),
inference(paramod,[status(thm)],[c_106,c_81]) ).
cnf(c_180,plain,
( in(B,relation_rng(sK1))
| ~ in(unordered_pair(unordered_pair(A,B),singleton(A)),sK1) ),
inference(resolve,[status(thm)],[c_105,c_96]) ).
cnf(c_189,plain,
( ~ empty(sK3)
| ~ in(A,relation_rng(sK1)) ),
inference(resolve,[status(thm)],[c_108,c_76]) ).
cnf(c_190,plain,
( element(A,sK3)
| ~ in(A,relation_rng(sK1)) ),
inference(resolve,[status(thm)],[c_108,c_75]) ).
cnf(c_208,plain,
( relation_rng(sK1) != sK3
| ~ in(unordered_pair(unordered_pair(sK6,A),singleton(A)),sK1) ),
inference(paramod,[status(thm)],[c_63,c_110]) ).
cnf(c_209,plain,
( sK3 = A
| in(sK4(A,sK3),A)
| relation_rng(sK1) = sK3
| in(unordered_pair(unordered_pair(sK4(A,sK3),sK5(sK4(A,sK3))),singleton(sK5(sK4(A,sK3)))),sK1) ),
inference(resolve,[status(thm)],[c_112,c_73]) ).
cnf(c_475,plain,
( in(A,relation_rng(sK1))
| ~ in(unordered_pair(unordered_pair(A,B),singleton(B)),sK1) ),
inference(paramod,[status(thm)],[c_63,c_180]) ).
cnf(c_1932,plain,
( in(sK4(A,sK3),relation_rng(sK1))
| sK3 = A
| in(sK4(A,sK3),A)
| relation_rng(sK1) = sK3 ),
inference(resolve,[status(thm)],[c_209,c_475]) ).
cnf(c_2431,plain,
( sK3 = relation_rng(sK1)
| in(sK4(relation_rng(sK1),sK3),relation_rng(sK1))
| relation_rng(sK1) = sK3 ),
inference(factor,[status(thm)],[c_1932]) ).
cnf(c_2432,plain,
( relation_rng(sK1) = sK3
| in(sK4(relation_rng(sK1),sK3),relation_rng(sK1))
| relation_rng(sK1) = sK3 ),
inference(copy,[status(thm)],[c_2431]) ).
cnf(c_1945,plain,
( in(sK4(relation_rng(sK1),sK3),relation_rng(sK1))
| relation_rng(sK1) = sK3 ),
inference(copy,[status(thm)],[c_2432]) ).
cnf(c_1948,plain,
( element(sK4(relation_rng(sK1),sK3),sK3)
| relation_rng(sK1) = sK3 ),
inference(resolve,[status(thm)],[c_1945,c_190]) ).
cnf(c_1949,plain,
( ~ empty(sK3)
| relation_rng(sK1) = sK3 ),
inference(resolve,[status(thm)],[c_1945,c_189]) ).
cnf(c_2433,plain,
( sK3 = relation_rng(sK1)
| ~ in(sK4(relation_rng(sK1),sK3),sK3)
| relation_rng(sK1) = sK3 ),
inference(resolve,[status(thm)],[c_1945,c_74]) ).
cnf(c_2434,plain,
( relation_rng(sK1) = sK3
| ~ in(sK4(relation_rng(sK1),sK3),sK3)
| relation_rng(sK1) = sK3 ),
inference(copy,[status(thm)],[c_2433]) ).
cnf(c_1958,plain,
( ~ in(sK4(relation_rng(sK1),sK3),sK3)
| relation_rng(sK1) = sK3 ),
inference(copy,[status(thm)],[c_2434]) ).
cnf(c_1961,plain,
( in(sK4(relation_rng(sK1),sK3),sK3)
| empty(sK3)
| relation_rng(sK1) = sK3 ),
inference(resolve,[status(thm)],[c_1948,c_72]) ).
cnf(c_2435,plain,
( relation_rng(sK1) = sK3
| empty(sK3)
| relation_rng(sK1) = sK3 ),
inference(resolve,[status(thm)],[c_1961,c_1958]) ).
cnf(c_2024,plain,
( empty(sK3)
| relation_rng(sK1) = sK3 ),
inference(copy,[status(thm)],[c_2435]) ).
cnf(c_2436,plain,
( relation_rng(sK1) = sK3
| relation_rng(sK1) = sK3 ),
inference(resolve,[status(thm)],[c_2024,c_1949]) ).
cnf(c_2025,plain,
relation_rng(sK1) = sK3,
inference(copy,[status(thm)],[c_2436]) ).
cnf(c_2437,plain,
( sK3 != sK3
| ~ in(unordered_pair(unordered_pair(sK6,A),singleton(A)),sK1) ),
inference(paramod,[status(thm)],[c_2025,c_208]) ).
cnf(c_2122,plain,
~ in(unordered_pair(unordered_pair(sK6,A),singleton(A)),sK1),
inference(copy,[status(thm)],[c_2437]) ).
cnf(c_2438,negated_conjecture,
( sK3 != sK3
| in(sK6,sK3) ),
inference(paramod,[status(thm)],[c_2025,c_111]) ).
cnf(c_2129,negated_conjecture,
in(sK6,sK3),
inference(copy,[status(thm)],[c_2438]) ).
cnf(c_2439,negated_conjecture,
( ~ element(A,powerset(cartesian_product2(B,C)))
| in(unordered_pair(unordered_pair(sK6,sK0(A,sK3,sK6)),singleton(sK0(A,sK3,sK6))),A)
| relation_rng(A) != sK3 ),
inference(resolve,[status(thm)],[c_86,c_2129]) ).
cnf(c_2440,negated_conjecture,
( ~ element(sK1,powerset(cartesian_product2(A,B)))
| relation_rng(sK1) != sK3 ),
inference(resolve,[status(thm)],[c_2439,c_2122]) ).
cnf(c_2441,negated_conjecture,
relation_rng(sK1) != sK3,
inference(resolve,[status(thm)],[c_2440,c_105]) ).
cnf(c_2442,negated_conjecture,
sK3 != sK3,
inference(paramod,[status(thm)],[c_2025,c_2441]) ).
cnf(c_2428,negated_conjecture,
$false,
inference(copy,[status(thm)],[c_2442]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU266+1 : 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/0.36 % Computer : n011.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 09:01:30 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 125533 was started by sandbox2 on n011,
% 0.09/0.37 % Sat Sep 26 09:01:30 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.37
% 0.09/0.37 % From the command line: assign(max_seconds, 300).
% 4.17/0.94
% 4.17/0.94 % given #500 (F,wt=20): 1358 -in(unordered_pair(unordered_pair(unordered_pair(singleton(A),unordered_pair(A,B)),C),singleton(C)),f4(D,unordered_pair(singleton(A),unordered_pair(A,B)))). [para(63(a,1),810(a,1,1))].
% 4.17/0.94
% 4.17/0.94 % SZS status Theorem for theBenchmark
% 4.17/0.94
% 4.17/0.94 % Proof 1 at 0.41 (+ 0.10) seconds.
% 4.17/0.94 % Length of proof is 64.
% 4.17/0.94 % Level of proof is 13.
% 4.17/0.94 % Maximum clause weight is 28.000.
% 4.17/0.94 % Given clauses 627.
% 4.17/0.94
% 4.17/0.94 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------