%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU156+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n003.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 : Fri Sep 25 02:55:38 PM UTC 2026
% Result : Theorem 4.68s 1.30s
% Output : CNFRefutation 4.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 7
% Syntax : Number of formulae : 69 ( 24 unt; 0 def)
% Number of atoms : 181 ( 145 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 173 ( 61 ~; 82 |; 24 &)
% ( 2 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-3 aty)
% Number of variables : 117 ( 0 sgn 110 !; 7 ?; 21 :)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k2_tarski) ).
fof(f10,axiom,
! [X0,X1,X2] :
( X2 = unordered_pair(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ( X3 = X1
| X3 = X0 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_tarski) ).
fof(f16,axiom,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_tarski) ).
fof(f61,conjecture,
! [X0,X1,X2,X3] :
( ordered_pair(X0,X1) = ordered_pair(X2,X3)
=> ( X1 = X3
& X0 = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t33_zfmisc_1) ).
fof(f62,negated_conjecture,
~ ! [X0,X1,X2,X3] :
( ordered_pair(X0,X1) = ordered_pair(X2,X3)
=> ( X1 = X3
& X0 = X2 ) ),
inference(negated_conjecture,[status(cth)],[f61]) ).
fof(f76,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f84,axiom,
! [X0,X1,X2] :
( singleton(X0) = unordered_pair(X1,X2)
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_zfmisc_1) ).
fof(f85,axiom,
! [X0,X1,X2] :
( singleton(X0) = unordered_pair(X1,X2)
=> X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t9_zfmisc_1) ).
fof(f117,plain,
? [X0,X1,X2,X3] :
( ordered_pair(X0,X1) = ordered_pair(X2,X3)
& ( X1 != X3
| X0 != X2 ) ),
inference(ennf_transformation,[],[f62]) ).
fof(f131,plain,
! [X0,X1,X2] :
( singleton(X0) != unordered_pair(X1,X2)
| X0 = X1 ),
inference(ennf_transformation,[],[f84]) ).
fof(f132,plain,
! [X0,X1,X2] :
( singleton(X0) != unordered_pair(X1,X2)
| X1 = X2 ),
inference(ennf_transformation,[],[f85]) ).
fof(f144,plain,
! [X0,X1,X2] :
( ( unordered_pair(X0,X1) != X2
| ! [X3] :
( ( ~ in(X3,X2)
| X3 = X1
| X3 = X0 )
& ( ( X1 != X3
& X0 != X3 )
| in(X3,X2) ) ) )
& ( ? [X3] :
( ( in(X3,X2)
| X3 = X1
| X3 = X0 )
& ( ~ in(X3,X2)
| ( X1 != X3
& X0 != X3 ) ) )
| X2 = unordered_pair(X0,X1) ) ),
inference(nnf_transformation,[],[f10]) ).
fof(f145,plain,
! [X0,X1,X2] :
( ( unordered_pair(X0,X1) != X2
| ! [X3] :
( ( ~ in(X3,X2)
| X3 = X1
| X3 = X0 )
& ( ( X1 != X3
& X0 != X3 )
| in(X3,X2) ) ) )
& ( ? [X3] :
( ( in(X3,X2)
| X3 = X1
| X3 = X0 )
& ( ~ in(X3,X2)
| ( X1 != X3
& X0 != X3 ) ) )
| X2 = unordered_pair(X0,X1) ) ),
inference(flattening,[],[f144]) ).
fof(f146,plain,
! [X0,X1,X2] :
( ( unordered_pair(X0,X1) != X2
| ! [X4] :
( ( ~ in(X4,X2)
| X1 = X4
| X0 = X4 )
& ( ( X1 != X4
& X0 != X4 )
| in(X4,X2) ) ) )
& ( ? [X3] :
( ( in(X3,X2)
| X3 = X1
| X3 = X0 )
& ( ~ in(X3,X2)
| ( X1 != X3
& X0 != X3 ) ) )
| X2 = unordered_pair(X0,X1) ) ),
inference(rectify,[],[f145]) ).
fof(f147,plain,
! [X0,X1,X2] :
( ( unordered_pair(X0,X1) != X2
| ! [X4] :
( ( ~ in(X4,X2)
| X1 = X4
| X0 = X4 )
& ( ( X1 != X4
& X0 != X4 )
| in(X4,X2) ) ) )
& ( ( ( in(sK3(X0,X1,X2),X2)
| sK3(X0,X1,X2) = X1
| sK3(X0,X1,X2) = X0 )
& ( ~ in(sK3(X0,X1,X2),X2)
| ( sK3(X0,X1,X2) != X1
& sK3(X0,X1,X2) != X0 ) ) )
| X2 = unordered_pair(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X3,sK3(X0,X1,X2))],[f146]) ).
fof(f175,plain,
( ordered_pair(sK14,sK15) = ordered_pair(sK16,sK17)
& ( sK15 != sK17
| sK14 != sK16 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14,sK15,sK16,sK17]),skolemize(X0,sK14),skolemize(X1,sK15),skolemize(X2,sK16),skolemize(X3,sK17)],[f117]) ).
fof(f182,plain,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
inference(cnf_transformation,[],[f3]) ).
fof(f198,plain,
! [X2,X0,X1,X4] :
( unordered_pair(X0,X1) != X2
| ~ in(X4,X2)
| X1 = X4
| X0 = X4 ),
inference(cnf_transformation,[],[f147]) ).
fof(f199,plain,
! [X2,X0,X1,X4] :
( unordered_pair(X0,X1) != X2
| X1 != X4
| in(X4,X2) ),
inference(cnf_transformation,[],[f147]) ).
fof(f200,plain,
! [X2,X0,X1,X4] :
( unordered_pair(X0,X1) != X2
| X0 != X4
| in(X4,X2) ),
inference(cnf_transformation,[],[f147]) ).
fof(f231,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
inference(cnf_transformation,[],[f16]) ).
fof(f273,plain,
ordered_pair(sK14,sK15) = ordered_pair(sK16,sK17),
inference(cnf_transformation,[],[f175]) ).
fof(f274,plain,
( sK15 != sK17
| sK14 != sK16 ),
inference(cnf_transformation,[],[f175]) ).
fof(f292,plain,
! [X0] : singleton(X0) = unordered_pair(X0,X0),
inference(cnf_transformation,[],[f76]) ).
fof(f301,plain,
! [X2,X0,X1] :
( singleton(X0) != unordered_pair(X1,X2)
| X0 = X1 ),
inference(cnf_transformation,[],[f131]) ).
fof(f302,plain,
! [X2,X0,X1] :
( singleton(X0) != unordered_pair(X1,X2)
| X1 = X2 ),
inference(cnf_transformation,[],[f132]) ).
fof(f303,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),
inference(definition_unfolding,[],[f231,f292]) ).
fof(f335,plain,
unordered_pair(unordered_pair(sK14,sK15),unordered_pair(sK14,sK14)) = unordered_pair(unordered_pair(sK16,sK17),unordered_pair(sK16,sK16)),
inference(definition_unfolding,[],[f273,f303,f303]) ).
fof(f339,plain,
! [X2,X0,X1] :
( unordered_pair(X0,X0) != unordered_pair(X1,X2)
| X0 = X1 ),
inference(definition_unfolding,[],[f301,f292]) ).
fof(f340,plain,
! [X2,X0,X1] :
( unordered_pair(X0,X0) != unordered_pair(X1,X2)
| X1 = X2 ),
inference(definition_unfolding,[],[f302,f292]) ).
fof(f349,plain,
! [X2,X1,X4] :
( unordered_pair(X4,X1) != X2
| in(X4,X2) ),
inference(equality_resolution,[],[f200]) ).
fof(f350,plain,
! [X1,X4] : in(X4,unordered_pair(X4,X1)),
inference(equality_resolution,[],[f349]) ).
fof(f351,plain,
! [X2,X0,X4] :
( unordered_pair(X0,X4) != X2
| in(X4,X2) ),
inference(equality_resolution,[],[f199]) ).
fof(f352,plain,
! [X0,X4] : in(X4,unordered_pair(X0,X4)),
inference(equality_resolution,[],[f351]) ).
fof(f353,plain,
! [X0,X1,X4] :
( ~ in(X4,unordered_pair(X0,X1))
| X1 = X4
| X0 = X4 ),
inference(equality_resolution,[],[f198]) ).
tcf(c_51,plain,
! [X0: $i,X1: $i] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
inference(cnf_transformation,[],[f182]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i] : in(X0,unordered_pair(X0,X1)),
inference(cnf_transformation,[],[f350]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i] : in(X0,unordered_pair(X1,X0)),
inference(cnf_transformation,[],[f352]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = X2 )
| ( X0 = X1 )
| ~ in(X0,unordered_pair(X1,X2)) ),
inference(cnf_transformation,[],[f353]) ).
tcf(c_141,negated_conjecture,
( ( sK15 != sK17 )
| ( sK14 != sK16 ) ),
inference(cnf_transformation,[],[f274]) ).
tcf(c_142,negated_conjecture,
unordered_pair(unordered_pair(sK14,sK15),unordered_pair(sK14,sK14)) = unordered_pair(unordered_pair(sK16,sK17),unordered_pair(sK16,sK16)),
inference(cnf_transformation,[],[f335]) ).
tcf(c_167,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = X1 )
| ( unordered_pair(X0,X0) != unordered_pair(X1,X2) ) ),
inference(cnf_transformation,[],[f339]) ).
tcf(c_168,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X1 = X2 )
| ( unordered_pair(X0,X0) != unordered_pair(X1,X2) ) ),
inference(cnf_transformation,[],[f340]) ).
tcf(c_232,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = X2 )
| ( unordered_pair(X0,X0) != unordered_pair(X1,X2) ) ),
inference(superposition,[status(thm)],[c_51,c_167]) ).
tcf(c_252,plain,
unordered_pair(unordered_pair(sK14,sK14),unordered_pair(sK14,sK15)) = unordered_pair(unordered_pair(sK16,sK16),unordered_pair(sK16,sK17)),
inference(demodulation,[status(thm)],[c_142,c_51]) ).
tcf(c_253,plain,
in(unordered_pair(sK16,sK17),unordered_pair(unordered_pair(sK14,sK14),unordered_pair(sK14,sK15))),
inference(superposition,[status(thm)],[c_252,c_71]) ).
tcf(c_254,plain,
in(unordered_pair(sK16,sK16),unordered_pair(unordered_pair(sK14,sK14),unordered_pair(sK14,sK15))),
inference(superposition,[status(thm)],[c_252,c_70]) ).
tcf(c_255,plain,
! [X0: $i] :
( ( unordered_pair(sK16,sK17) = X0 )
| ( unordered_pair(sK16,sK16) = X0 )
| ~ in(X0,unordered_pair(unordered_pair(sK14,sK14),unordered_pair(sK14,sK15))) ),
inference(superposition,[status(thm)],[c_252,c_72]) ).
tcf(c_292,plain,
( ( unordered_pair(sK14,sK15) = unordered_pair(sK16,sK16) )
| ( unordered_pair(sK14,sK14) = unordered_pair(sK16,sK16) ) ),
inference(superposition,[status(thm)],[c_254,c_72]) ).
tcf(c_293,plain,
( ( unordered_pair(sK14,sK15) = unordered_pair(sK16,sK17) )
| ( unordered_pair(sK14,sK14) = unordered_pair(sK16,sK17) ) ),
inference(superposition,[status(thm)],[c_253,c_72]) ).
tcf(c_309,plain,
( ( unordered_pair(sK14,sK15) = unordered_pair(sK16,sK17) )
| ( unordered_pair(sK14,sK15) = unordered_pair(sK16,sK16) ) ),
inference(superposition,[status(thm)],[c_71,c_255]) ).
tcf(c_463,plain,
! [X0: $i] :
( ( X0 = sK16 )
| ( unordered_pair(sK14,sK14) = unordered_pair(sK16,sK16) )
| ~ in(X0,unordered_pair(sK14,sK15)) ),
inference(superposition,[status(thm)],[c_292,c_72]) ).
tcf(c_519,plain,
( in(sK17,unordered_pair(sK14,sK15))
| ( unordered_pair(sK14,sK14) = unordered_pair(sK16,sK17) ) ),
inference(superposition,[status(thm)],[c_293,c_71]) ).
tcf(c_610,plain,
( in(sK16,unordered_pair(sK14,sK15))
| ( unordered_pair(sK14,sK15) = unordered_pair(sK16,sK16) ) ),
inference(superposition,[status(thm)],[c_309,c_70]) ).
tcf(c_612,plain,
! [X0: $i] :
( ( X0 = sK17 )
| ( X0 = sK16 )
| ( unordered_pair(sK14,sK15) = unordered_pair(sK16,sK16) )
| ~ in(X0,unordered_pair(sK14,sK15)) ),
inference(superposition,[status(thm)],[c_309,c_72]) ).
tcf(c_794,plain,
( ( sK14 = sK16 )
| ( unordered_pair(sK14,sK14) = unordered_pair(sK16,sK16) ) ),
inference(superposition,[status(thm)],[c_70,c_463]) ).
tcf(c_990,plain,
( ( sK15 = sK17 )
| ( sK14 = sK17 )
| ( unordered_pair(sK14,sK14) = unordered_pair(sK16,sK17) ) ),
inference(superposition,[status(thm)],[c_519,c_72]) ).
tcf(c_1152,plain,
( ( sK16 = sK15 )
| ( sK14 = sK16 )
| ( unordered_pair(sK14,sK15) = unordered_pair(sK16,sK16) ) ),
inference(superposition,[status(thm)],[c_610,c_72]) ).
tcf(c_1195,plain,
( ( sK15 = sK17 )
| ( sK16 = sK15 )
| ( unordered_pair(sK14,sK15) = unordered_pair(sK16,sK16) ) ),
inference(superposition,[status(thm)],[c_71,c_612]) ).
tcf(c_2224,plain,
sK14 = sK16,
inference(forward_subsumption_resolution,[status(thm)],[c_794,c_167]) ).
tcf(c_2252,plain,
sK15 != sK17,
inference(superposition,[status(thm)],[c_2224,c_141]) ).
tcf(c_2551,plain,
( ( unordered_pair(sK14,sK14) = unordered_pair(sK16,sK17) )
| ( sK14 = sK17 ) ),
inference(global_subsumption_just,[status(thm)],[c_990,c_990,c_2252]) ).
tcf(c_2552,plain,
( ( sK14 = sK17 )
| ( unordered_pair(sK14,sK14) = unordered_pair(sK16,sK17) ) ),
inference(renaming,[status(thm)],[c_2551]) ).
tcf(c_2555,plain,
sK14 = sK17,
inference(forward_subsumption_resolution,[status(thm)],[c_2552,c_232]) ).
tcf(c_2643,plain,
( ( sK16 = sK15 )
| ( unordered_pair(sK14,sK15) = unordered_pair(sK16,sK16) ) ),
inference(global_subsumption_just,[status(thm)],[c_1152,c_1195,c_2252]) ).
tcf(c_2647,plain,
( ( sK14 = sK15 )
| ( unordered_pair(sK14,sK14) = unordered_pair(sK14,sK15) ) ),
inference(light_normalisation,[status(thm)],[c_2643,c_2224]) ).
tcf(c_2650,plain,
sK14 = sK15,
inference(forward_subsumption_resolution,[status(thm)],[c_2647,c_168]) ).
tcf(c_5678,plain,
sK14 != sK14,
inference(light_normalisation,[status(thm)],[c_2252,c_2555,c_2650]) ).
tcf(c_5679,plain,
$false,
inference(equality_resolution_simp,[status(thm)],[c_5678]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU156+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.34 % Computer : n003.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Thu Sep 24 13:00:21 UTC 2026
% 0.09/0.34 % CPUTime :
% 0.09/0.34 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/0.39 Running first-order theorem proving
% 0.13/0.39 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.40
% 0.13/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.40
% 0.13/0.40 % Detected problem language: tptp
% 0.13/0.41 % Proving...
% 4.68/1.30 % SZS status Started for theBenchmark.p
% 4.68/1.30 % SZS status Theorem for theBenchmark.p
% 4.68/1.30
% 4.68/1.30 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 4.68/1.30
% 4.68/1.30 % ------ iProver source info
% 4.68/1.30
% 4.68/1.30 % git: date: 2026-07-19 20:42:38 +0200
% 4.68/1.30 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 4.68/1.30 % git: non_committed_changes: false
% 4.68/1.30
% 4.68/1.30 % ------ Parsing...
% 4.68/1.30 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 4.68/1.30 % ------ Proving...
% 4.68/1.30 % ------ Problem Properties
% 4.68/1.30
% 4.68/1.30 %
% 4.68/1.30 % clauses 120
% 4.68/1.30 % conjectures 2
% 4.68/1.30 % EPR 24
% 4.68/1.30 % Horn 95
% 4.68/1.30 % unary 32
% 4.68/1.30 % binary 50
% 4.68/1.30 % lits 251
% 4.68/1.30 % lits eq 74
% 4.68/1.30 % fd_pure 0
% 4.68/1.30 % fd_pseudo 0
% 4.68/1.30 % fd_cond 3
% 4.68/1.30 % fd_pseudo_cond 29
% 4.68/1.30 % AC symbols 0
% 4.68/1.30
% 4.68/1.30 % ------ Input Options Time Limit: Unbounded
% 4.68/1.30
% 4.68/1.30
% 4.68/1.30 % ------
% 4.68/1.30 % Current options:
% 4.68/1.30 % ------
% 4.68/1.30
% 4.68/1.30
% 4.68/1.30 %
% 4.68/1.30
% 4.68/1.30 % ------ Proving...
% 4.68/1.30 %
% 4.68/1.30
% 4.68/1.30 % SZS status Theorem for theBenchmark.p
% 4.68/1.30
% 4.68/1.30 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 4.68/1.30
% 4.68/1.30
%------------------------------------------------------------------------------