%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU261+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n018.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:56:24 PM UTC 2026
% Result : Theorem 7.30s 1.83s
% Output : CNFRefutation 7.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 3
% Syntax : Number of formulae : 61 ( 15 unt; 0 def)
% Number of atoms : 297 ( 0 equ)
% Maximal formula atoms : 15 ( 4 avg)
% Number of connectives : 405 ( 169 ~; 163 |; 53 &)
% ( 2 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 6 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 10 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% Number of variables : 67 ( 0 sgn 61 !; 6 ?; 21 :)
% Comments :
%------------------------------------------------------------------------------
fof(f51,axiom,
! [X0] :
( relation(X0)
=> ( well_ordering(X0)
<=> ( well_founded_relation(X0)
& connected(X0)
& antisymmetric(X0)
& transitive(X0)
& reflexive(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_wellord1) ).
fof(f280,axiom,
! [X0] :
( relation(X0)
=> ! [X1] :
( relation(X1)
=> ! [X2] :
( ( function(X2)
& relation(X2) )
=> ( relation_isomorphism(X0,X1,X2)
=> ( ( well_founded_relation(X0)
=> well_founded_relation(X1) )
& ( antisymmetric(X0)
=> antisymmetric(X1) )
& ( connected(X0)
=> connected(X1) )
& ( transitive(X0)
=> transitive(X1) )
& ( reflexive(X0)
=> reflexive(X1) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t53_wellord1) ).
fof(f283,conjecture,
! [X0] :
( relation(X0)
=> ! [X1] :
( relation(X1)
=> ! [X2] :
( ( function(X2)
& relation(X2) )
=> ( ( relation_isomorphism(X0,X1,X2)
& well_ordering(X0) )
=> well_ordering(X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t54_wellord1) ).
fof(f284,negated_conjecture,
~ ! [X0] :
( relation(X0)
=> ! [X1] :
( relation(X1)
=> ! [X2] :
( ( function(X2)
& relation(X2) )
=> ( ( relation_isomorphism(X0,X1,X2)
& well_ordering(X0) )
=> well_ordering(X1) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f283]) ).
fof(f377,plain,
! [X0] :
( ~ relation(X0)
| ( well_ordering(X0)
<=> ( well_founded_relation(X0)
& connected(X0)
& antisymmetric(X0)
& transitive(X0)
& reflexive(X0) ) ) ),
inference(ennf_transformation,[],[f51]) ).
fof(f595,plain,
! [X0] :
( ~ relation(X0)
| ! [X1] :
( ~ relation(X1)
| ! [X2] :
( ~ function(X2)
| ~ relation(X2)
| ~ relation_isomorphism(X0,X1,X2)
| ( ( ~ well_founded_relation(X0)
| well_founded_relation(X1) )
& ( ~ antisymmetric(X0)
| antisymmetric(X1) )
& ( ~ connected(X0)
| connected(X1) )
& ( ~ transitive(X0)
| transitive(X1) )
& ( ~ reflexive(X0)
| reflexive(X1) ) ) ) ) ),
inference(ennf_transformation,[],[f280]) ).
fof(f596,plain,
! [X0] :
( ~ relation(X0)
| ! [X1] :
( ~ relation(X1)
| ! [X2] :
( ~ function(X2)
| ~ relation(X2)
| ~ relation_isomorphism(X0,X1,X2)
| ( ( ~ well_founded_relation(X0)
| well_founded_relation(X1) )
& ( ~ antisymmetric(X0)
| antisymmetric(X1) )
& ( ~ connected(X0)
| connected(X1) )
& ( ~ transitive(X0)
| transitive(X1) )
& ( ~ reflexive(X0)
| reflexive(X1) ) ) ) ) ),
inference(flattening,[],[f595]) ).
fof(f601,plain,
? [X0] :
( relation(X0)
& ? [X1] :
( relation(X1)
& ? [X2] :
( function(X2)
& relation(X2)
& relation_isomorphism(X0,X1,X2)
& well_ordering(X0)
& ~ well_ordering(X1) ) ) ),
inference(ennf_transformation,[],[f284]) ).
fof(f602,plain,
? [X0] :
( relation(X0)
& ? [X1] :
( relation(X1)
& ? [X2] :
( function(X2)
& relation(X2)
& relation_isomorphism(X0,X1,X2)
& well_ordering(X0)
& ~ well_ordering(X1) ) ) ),
inference(flattening,[],[f601]) ).
fof(f756,plain,
! [X0] :
( ~ relation(X0)
| ( ( ~ well_ordering(X0)
| ( well_founded_relation(X0)
& connected(X0)
& antisymmetric(X0)
& transitive(X0)
& reflexive(X0) ) )
& ( ~ well_founded_relation(X0)
| ~ connected(X0)
| ~ antisymmetric(X0)
| ~ transitive(X0)
| ~ reflexive(X0)
| well_ordering(X0) ) ) ),
inference(nnf_transformation,[],[f377]) ).
fof(f757,plain,
! [X0] :
( ~ relation(X0)
| ( ( ~ well_ordering(X0)
| ( well_founded_relation(X0)
& connected(X0)
& antisymmetric(X0)
& transitive(X0)
& reflexive(X0) ) )
& ( ~ well_founded_relation(X0)
| ~ connected(X0)
| ~ antisymmetric(X0)
| ~ transitive(X0)
| ~ reflexive(X0)
| well_ordering(X0) ) ) ),
inference(flattening,[],[f756]) ).
fof(f880,plain,
( relation(sK119)
& relation(sK120)
& function(sK121)
& relation(sK121)
& relation_isomorphism(sK119,sK120,sK121)
& well_ordering(sK119)
& ~ well_ordering(sK120) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK119,sK120,sK121]),skolemize(X0,sK119),skolemize(X1,sK120),skolemize(X2,sK121)],[f602]) ).
fof(f1091,plain,
! [X0] :
( ~ relation(X0)
| ~ well_ordering(X0)
| well_founded_relation(X0) ),
inference(cnf_transformation,[],[f757]) ).
fof(f1092,plain,
! [X0] :
( ~ relation(X0)
| ~ well_ordering(X0)
| connected(X0) ),
inference(cnf_transformation,[],[f757]) ).
fof(f1093,plain,
! [X0] :
( ~ relation(X0)
| ~ well_ordering(X0)
| antisymmetric(X0) ),
inference(cnf_transformation,[],[f757]) ).
fof(f1094,plain,
! [X0] :
( ~ relation(X0)
| ~ well_ordering(X0)
| transitive(X0) ),
inference(cnf_transformation,[],[f757]) ).
fof(f1095,plain,
! [X0] :
( ~ relation(X0)
| ~ well_ordering(X0)
| reflexive(X0) ),
inference(cnf_transformation,[],[f757]) ).
fof(f1096,plain,
! [X0] :
( ~ relation(X0)
| ~ well_founded_relation(X0)
| ~ connected(X0)
| ~ antisymmetric(X0)
| ~ transitive(X0)
| ~ reflexive(X0)
| well_ordering(X0) ),
inference(cnf_transformation,[],[f757]) ).
fof(f1486,plain,
! [X2,X0,X1] :
( ~ relation(X0)
| ~ relation(X1)
| ~ function(X2)
| ~ relation(X2)
| ~ relation_isomorphism(X0,X1,X2)
| ~ well_founded_relation(X0)
| well_founded_relation(X1) ),
inference(cnf_transformation,[],[f596]) ).
fof(f1487,plain,
! [X2,X0,X1] :
( ~ relation(X0)
| ~ relation(X1)
| ~ function(X2)
| ~ relation(X2)
| ~ relation_isomorphism(X0,X1,X2)
| ~ antisymmetric(X0)
| antisymmetric(X1) ),
inference(cnf_transformation,[],[f596]) ).
fof(f1488,plain,
! [X2,X0,X1] :
( ~ relation(X0)
| ~ relation(X1)
| ~ function(X2)
| ~ relation(X2)
| ~ relation_isomorphism(X0,X1,X2)
| ~ connected(X0)
| connected(X1) ),
inference(cnf_transformation,[],[f596]) ).
fof(f1489,plain,
! [X2,X0,X1] :
( ~ relation(X0)
| ~ relation(X1)
| ~ function(X2)
| ~ relation(X2)
| ~ relation_isomorphism(X0,X1,X2)
| ~ transitive(X0)
| transitive(X1) ),
inference(cnf_transformation,[],[f596]) ).
fof(f1490,plain,
! [X2,X0,X1] :
( ~ relation(X0)
| ~ relation(X1)
| ~ function(X2)
| ~ relation(X2)
| ~ relation_isomorphism(X0,X1,X2)
| ~ reflexive(X0)
| reflexive(X1) ),
inference(cnf_transformation,[],[f596]) ).
fof(f1504,plain,
relation(sK119),
inference(cnf_transformation,[],[f880]) ).
fof(f1505,plain,
relation(sK120),
inference(cnf_transformation,[],[f880]) ).
fof(f1506,plain,
function(sK121),
inference(cnf_transformation,[],[f880]) ).
fof(f1507,plain,
relation(sK121),
inference(cnf_transformation,[],[f880]) ).
fof(f1508,plain,
relation_isomorphism(sK119,sK120,sK121),
inference(cnf_transformation,[],[f880]) ).
fof(f1509,plain,
well_ordering(sK119),
inference(cnf_transformation,[],[f880]) ).
fof(f1510,plain,
~ well_ordering(sK120),
inference(cnf_transformation,[],[f880]) ).
tcf(c_238,plain,
! [X0: $i] :
( well_ordering(X0)
| ~ reflexive(X0)
| ~ well_founded_relation(X0)
| ~ transitive(X0)
| ~ connected(X0)
| ~ antisymmetric(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f1096]) ).
tcf(c_239,plain,
! [X0: $i] :
( reflexive(X0)
| ~ well_ordering(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f1095]) ).
tcf(c_240,plain,
! [X0: $i] :
( transitive(X0)
| ~ well_ordering(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f1094]) ).
tcf(c_241,plain,
! [X0: $i] :
( antisymmetric(X0)
| ~ well_ordering(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f1093]) ).
tcf(c_242,plain,
! [X0: $i] :
( connected(X0)
| ~ well_ordering(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f1092]) ).
tcf(c_243,plain,
! [X0: $i] :
( well_founded_relation(X0)
| ~ well_ordering(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f1091]) ).
tcf(c_631,plain,
! [X0: $i,X1: $i,X2: $i] :
( reflexive(X1)
| ~ reflexive(X0)
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0)
| ~ function(X2)
| ~ relation_isomorphism(X0,X1,X2) ),
inference(cnf_transformation,[],[f1490]) ).
tcf(c_632,plain,
! [X0: $i,X1: $i,X2: $i] :
( transitive(X1)
| ~ transitive(X0)
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0)
| ~ function(X2)
| ~ relation_isomorphism(X0,X1,X2) ),
inference(cnf_transformation,[],[f1489]) ).
tcf(c_633,plain,
! [X0: $i,X1: $i,X2: $i] :
( connected(X1)
| ~ connected(X0)
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0)
| ~ function(X2)
| ~ relation_isomorphism(X0,X1,X2) ),
inference(cnf_transformation,[],[f1488]) ).
tcf(c_634,plain,
! [X0: $i,X1: $i,X2: $i] :
( antisymmetric(X1)
| ~ antisymmetric(X0)
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0)
| ~ function(X2)
| ~ relation_isomorphism(X0,X1,X2) ),
inference(cnf_transformation,[],[f1487]) ).
tcf(c_635,plain,
! [X0: $i,X1: $i,X2: $i] :
( well_founded_relation(X1)
| ~ well_founded_relation(X0)
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0)
| ~ function(X2)
| ~ relation_isomorphism(X0,X1,X2) ),
inference(cnf_transformation,[],[f1486]) ).
tcf(c_649,negated_conjecture,
~ well_ordering(sK120),
inference(cnf_transformation,[],[f1510]) ).
tcf(c_650,negated_conjecture,
well_ordering(sK119),
inference(cnf_transformation,[],[f1509]) ).
tcf(c_651,negated_conjecture,
relation_isomorphism(sK119,sK120,sK121),
inference(cnf_transformation,[],[f1508]) ).
tcf(c_652,negated_conjecture,
relation(sK121),
inference(cnf_transformation,[],[f1507]) ).
tcf(c_653,negated_conjecture,
function(sK121),
inference(cnf_transformation,[],[f1506]) ).
tcf(c_654,negated_conjecture,
relation(sK120),
inference(cnf_transformation,[],[f1505]) ).
tcf(c_655,negated_conjecture,
relation(sK119),
inference(cnf_transformation,[],[f1504]) ).
tcf(c_790,plain,
( well_founded_relation(sK119)
| ~ well_ordering(sK119) ),
inference(superposition,[status(thm)],[c_655,c_243]) ).
tcf(c_799,plain,
( connected(sK119)
| ~ well_ordering(sK119) ),
inference(superposition,[status(thm)],[c_655,c_242]) ).
tcf(c_808,plain,
( antisymmetric(sK119)
| ~ well_ordering(sK119) ),
inference(superposition,[status(thm)],[c_655,c_241]) ).
tcf(c_817,plain,
( transitive(sK119)
| ~ well_ordering(sK119) ),
inference(superposition,[status(thm)],[c_655,c_240]) ).
tcf(c_846,plain,
( well_founded_relation(sK120)
| ~ well_founded_relation(sK119)
| ~ relation(sK121)
| ~ relation(sK119)
| ~ relation(sK120)
| ~ function(sK121) ),
inference(superposition,[status(thm)],[c_651,c_635]) ).
tcf(c_861,plain,
( antisymmetric(sK120)
| ~ antisymmetric(sK119)
| ~ relation(sK121)
| ~ relation(sK119)
| ~ relation(sK120)
| ~ function(sK121) ),
inference(superposition,[status(thm)],[c_651,c_634]) ).
tcf(c_876,plain,
( connected(sK120)
| ~ connected(sK119)
| ~ relation(sK121)
| ~ relation(sK119)
| ~ relation(sK120)
| ~ function(sK121) ),
inference(superposition,[status(thm)],[c_651,c_633]) ).
tcf(c_891,plain,
( transitive(sK120)
| ~ transitive(sK119)
| ~ relation(sK121)
| ~ relation(sK119)
| ~ relation(sK120)
| ~ function(sK121) ),
inference(superposition,[status(thm)],[c_651,c_632]) ).
tcf(c_906,plain,
( reflexive(sK120)
| ~ reflexive(sK119)
| ~ relation(sK121)
| ~ relation(sK119)
| ~ relation(sK120)
| ~ function(sK121) ),
inference(superposition,[status(thm)],[c_651,c_631]) ).
tcf(c_971,plain,
( reflexive(sK120)
| ~ reflexive(sK119) ),
inference(global_subsumption_just,[status(thm)],[c_906,c_655,c_654,c_653,c_652,c_906]) ).
tcf(c_1229,plain,
( reflexive(sK119)
| ~ well_ordering(sK119) ),
inference(superposition,[status(thm)],[c_655,c_239]) ).
tcf(c_1486,plain,
( well_ordering(sK120)
| ~ reflexive(sK120)
| ~ well_founded_relation(sK120)
| ~ transitive(sK120)
| ~ connected(sK120)
| ~ antisymmetric(sK120) ),
inference(superposition,[status(thm)],[c_654,c_238]) ).
tcf(c_1488,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_1486,c_1229,c_971,c_891,c_876,c_861,c_846,c_817,c_808,c_799,c_790,c_649,c_650,c_652,c_653,c_654,c_655]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU261+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.07 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.16/0.43 % Computer : n018.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Thu Sep 24 13:29:03 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.44 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.22/0.50 Running first-order theorem proving
% 0.22/0.50 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.22/0.52
% 0.22/0.52 % ======== iProver multi-core TPTP/SMT =========
% 0.22/0.52
% 0.22/0.52 % Detected problem language: tptp
% 0.22/0.53 % Proving...
% 7.30/1.83 % SZS status Started for theBenchmark.p
% 7.30/1.83 % SZS status Theorem for theBenchmark.p
% 7.30/1.83
% 7.30/1.83 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 7.30/1.83
% 7.30/1.83 % ------ iProver source info
% 7.30/1.83
% 7.30/1.83 % git: date: 2026-07-19 20:42:38 +0200
% 7.30/1.83 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 7.30/1.83 % git: non_committed_changes: false
% 7.30/1.83
% 7.30/1.83 % ------ Parsing...
% 7.30/1.83 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 7.30/1.83 % ------ Proving...
% 7.30/1.83 % ------ Problem Properties
% 7.30/1.83
% 7.30/1.83 %
% 7.30/1.83 % clauses 667
% 7.30/1.83 % conjectures 7
% 7.30/1.83 % EPR 123
% 7.30/1.83 % Horn 533
% 7.30/1.83 % unary 109
% 7.30/1.83 % binary 158
% 7.30/1.83 % lits 1982
% 7.30/1.83 % lits eq 290
% 7.30/1.83 % fd_pure 0
% 7.30/1.83 % fd_pseudo 0
% 7.30/1.83 % fd_cond 21
% 7.30/1.83 % fd_pseudo_cond 101
% 7.30/1.83 % AC symbols 0
% 7.30/1.84
% 7.30/1.84 % ------ Input Options Time Limit: Unbounded
% 7.30/1.84
% 7.30/1.84
% 7.30/1.84 % ------
% 7.30/1.84 % Current options:
% 7.30/1.84 % ------
% 7.30/1.84
% 7.30/1.84
% 7.30/1.84 %
% 7.30/1.84
% 7.30/1.84 % ------ Proving...
% 7.30/1.84 %
% 7.30/1.84
% 7.30/1.84 % ------ Proving...
% 7.30/1.84 %
% 7.30/1.84
% 7.30/1.84 % SZS status Theorem for theBenchmark.p
% 7.30/1.84
% 7.30/1.84 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 7.30/1.84
%------------------------------------------------------------------------------