%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SEU261+1 : TPTP v9.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Jul 25 03:45:01 PM UTC 2025
% Result : Theorem 0.09s 0.31s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 3
% Syntax : Number of formulae : 62 ( 36 unt; 0 def)
% Number of atoms : 186 ( 0 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 219 ( 95 ~; 92 |; 13 &)
% ( 1 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% 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 : 31 ( 0 sgn 10 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(t54_wellord1,plain,
! [A] :
( relation(A)
=> ! [B] :
( relation(B)
=> ! [C] :
( ( relation(C)
& function(C) )
=> ( ( well_ordering(A)
& relation_isomorphism(A,B,C) )
=> well_ordering(B) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t54_wellord1) ).
fof(t54_wellord1_negated,plain,
~ ! [A] :
( relation(A)
=> ! [B] :
( relation(B)
=> ! [C] :
( ( relation(C)
& function(C) )
=> ( ( well_ordering(A)
& relation_isomorphism(A,B,C) )
=> well_ordering(B) ) ) ) ),
inference(negate_conjecture,[status(cth)],[t54_wellord1]) ).
cnf(13,plain,
relation(sK2),
inference(cnf,[status(esa)],[t54_wellord1_negated]) ).
cnf(l0,plain,
relation(sK2),
inference(instantiation,[status(thm)],[13]) ).
fof(d4_wellord1,plain,
! [A] :
( relation(A)
=> ( well_ordering(A)
<=> ( reflexive(A)
& transitive(A)
& antisymmetric(A)
& connected(A)
& well_founded_relation(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_wellord1) ).
cnf(0,plain,
( ~ relation(X0)
| ~ well_ordering(X0)
| reflexive(X0) ),
inference(cnf,[status(esa)],[d4_wellord1]) ).
cnf(l1,plain,
( ~ relation(sK2)
| ~ well_ordering(sK2)
| reflexive(sK2) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(17,plain,
well_ordering(sK2),
inference(cnf,[status(esa)],[t54_wellord1_negated]) ).
cnf(l2,plain,
well_ordering(sK2),
inference(instantiation,[status(thm)],[17]) ).
fof(t53_wellord1,plain,
! [A] :
( relation(A)
=> ! [B] :
( relation(B)
=> ! [C] :
( ( relation(C)
& function(C) )
=> ( relation_isomorphism(A,B,C)
=> ( ( reflexive(A)
=> reflexive(B) )
& ( transitive(A)
=> transitive(B) )
& ( connected(A)
=> connected(B) )
& ( antisymmetric(A)
=> antisymmetric(B) )
& ( well_founded_relation(A)
=> well_founded_relation(B) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t53_wellord1) ).
cnf(8,plain,
( ~ function(X0)
| ~ relation(X1)
| ~ relation(X2)
| ~ relation(X0)
| ~ reflexive(X1)
| ~ relation_isomorphism(X1,X2,X0)
| reflexive(X2) ),
inference(cnf,[status(esa)],[t53_wellord1]) ).
cnf(l3,plain,
( ~ function(sK4)
| ~ relation(sK2)
| ~ relation(sK3)
| ~ relation(sK4)
| ~ reflexive(sK2)
| ~ relation_isomorphism(sK2,sK3,sK4)
| reflexive(sK3) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(5,plain,
( ~ well_founded_relation(X0)
| ~ relation(X0)
| ~ reflexive(X0)
| ~ transitive(X0)
| ~ antisymmetric(X0)
| ~ connected(X0)
| well_ordering(X0) ),
inference(cnf,[status(esa)],[d4_wellord1]) ).
cnf(l13,plain,
( ~ well_founded_relation(sK3)
| ~ relation(sK3)
| ~ reflexive(sK3)
| ~ transitive(sK3)
| ~ antisymmetric(sK3)
| ~ connected(sK3)
| well_ordering(sK3) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(18,plain,
relation_isomorphism(sK2,sK3,sK4),
inference(cnf,[status(esa)],[t54_wellord1_negated]) ).
cnf(l23,plain,
relation_isomorphism(sK2,sK3,sK4),
inference(instantiation,[status(thm)],[18]) ).
cnf(14,plain,
relation(sK3),
inference(cnf,[status(esa)],[t54_wellord1_negated]) ).
cnf(l22,plain,
relation(sK3),
inference(instantiation,[status(thm)],[14]) ).
cnf(l34,plain,
relation(sK3),
inference(instantiation,[status(thm)],[14]) ).
cnf(16,plain,
function(sK4),
inference(cnf,[status(esa)],[t54_wellord1_negated]) ).
cnf(l6,plain,
function(sK4),
inference(instantiation,[status(thm)],[16]) ).
cnf(9,plain,
( ~ function(X0)
| ~ relation(X1)
| ~ relation(X2)
| ~ relation(X0)
| ~ transitive(X1)
| ~ relation_isomorphism(X1,X2,X0)
| transitive(X2) ),
inference(cnf,[status(esa)],[t53_wellord1]) ).
cnf(l41,plain,
( ~ function(sK4)
| ~ relation(sK2)
| ~ relation(sK3)
| ~ relation(sK4)
| ~ transitive(sK2)
| ~ relation_isomorphism(sK2,sK3,sK4)
| transitive(sK3) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(10,plain,
( ~ function(X0)
| ~ relation(X1)
| ~ relation(X2)
| ~ relation(X0)
| ~ connected(X1)
| ~ relation_isomorphism(X1,X2,X0)
| connected(X2) ),
inference(cnf,[status(esa)],[t53_wellord1]) ).
cnf(l32,plain,
( ~ function(sK4)
| ~ relation(sK2)
| ~ relation(sK3)
| ~ relation(sK4)
| ~ connected(sK2)
| ~ relation_isomorphism(sK2,sK3,sK4)
| connected(sK3) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l35,plain,
relation_isomorphism(sK2,sK3,sK4),
inference(instantiation,[status(thm)],[18]) ).
cnf(15,plain,
relation(sK4),
inference(cnf,[status(esa)],[t54_wellord1_negated]) ).
cnf(l7,plain,
relation(sK4),
inference(instantiation,[status(thm)],[15]) ).
cnf(1,plain,
( ~ relation(X0)
| ~ well_ordering(X0)
| transitive(X0) ),
inference(cnf,[status(esa)],[d4_wellord1]) ).
cnf(l53,plain,
( ~ relation(sK2)
| ~ well_ordering(sK2)
| transitive(sK2) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l47,plain,
relation(sK3),
inference(instantiation,[status(thm)],[14]) ).
cnf(l39,plain,
function(sK4),
inference(instantiation,[status(thm)],[16]) ).
cnf(12,plain,
( ~ well_founded_relation(X0)
| ~ function(X1)
| ~ relation(X0)
| ~ relation(X2)
| ~ relation(X1)
| ~ relation_isomorphism(X0,X2,X1)
| well_founded_relation(X2) ),
inference(cnf,[status(esa)],[t53_wellord1]) ).
cnf(l28,plain,
( ~ well_founded_relation(sK2)
| ~ function(sK4)
| ~ relation(sK2)
| ~ relation(sK3)
| ~ relation(sK4)
| ~ relation_isomorphism(sK2,sK3,sK4)
| well_founded_relation(sK3) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(3,plain,
( ~ relation(X0)
| ~ well_ordering(X0)
| connected(X0) ),
inference(cnf,[status(esa)],[d4_wellord1]) ).
cnf(l36,plain,
( ~ relation(sK2)
| ~ well_ordering(sK2)
| connected(sK2) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l44,plain,
relation(sK4),
inference(instantiation,[status(thm)],[15]) ).
cnf(l50,plain,
function(sK4),
inference(instantiation,[status(thm)],[16]) ).
cnf(l40,plain,
relation(sK4),
inference(instantiation,[status(thm)],[15]) ).
cnf(l55,plain,
relation_isomorphism(sK2,sK3,sK4),
inference(instantiation,[status(thm)],[18]) ).
cnf(l45,plain,
relation(sK3),
inference(instantiation,[status(thm)],[14]) ).
cnf(l52,plain,
relation(sK4),
inference(instantiation,[status(thm)],[15]) ).
cnf(l61,plain,
well_ordering(sK2),
inference(instantiation,[status(thm)],[17]) ).
cnf(l29,plain,
function(sK4),
inference(instantiation,[status(thm)],[16]) ).
cnf(l43,plain,
relation_isomorphism(sK2,sK3,sK4),
inference(instantiation,[status(thm)],[18]) ).
cnf(11,plain,
( ~ function(X0)
| ~ relation(X1)
| ~ relation(X2)
| ~ relation(X0)
| ~ antisymmetric(X1)
| ~ relation_isomorphism(X1,X2,X0)
| antisymmetric(X2) ),
inference(cnf,[status(esa)],[t53_wellord1]) ).
cnf(l30,plain,
( ~ function(sK4)
| ~ relation(sK2)
| ~ relation(sK3)
| ~ relation(sK4)
| ~ antisymmetric(sK2)
| ~ relation_isomorphism(sK2,sK3,sK4)
| antisymmetric(sK3) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l75,plain,
relation(sK3),
inference(instantiation,[status(thm)],[14]) ).
cnf(l51,plain,
relation(sK3),
inference(instantiation,[status(thm)],[14]) ).
cnf(19,plain,
~ well_ordering(sK3),
inference(cnf,[status(esa)],[t54_wellord1_negated]) ).
cnf(l24,plain,
~ well_ordering(sK3),
inference(instantiation,[status(thm)],[19]) ).
cnf(4,plain,
( ~ relation(X0)
| ~ well_ordering(X0)
| well_founded_relation(X0) ),
inference(cnf,[status(esa)],[d4_wellord1]) ).
cnf(l46,plain,
( ~ relation(sK2)
| ~ well_ordering(sK2)
| well_founded_relation(sK2) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(2,plain,
( ~ relation(X0)
| ~ well_ordering(X0)
| antisymmetric(X0) ),
inference(cnf,[status(esa)],[d4_wellord1]) ).
cnf(l58,plain,
( ~ relation(sK2)
| ~ well_ordering(sK2)
| antisymmetric(sK2) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l78,plain,
well_ordering(sK2),
inference(instantiation,[status(thm)],[17]) ).
cnf(l54,plain,
well_ordering(sK2),
inference(instantiation,[status(thm)],[17]) ).
cnf(l72,plain,
well_ordering(sK2),
inference(instantiation,[status(thm)],[17]) ).
cnf(l70,plain,
function(sK4),
inference(instantiation,[status(thm)],[16]) ).
cnf(l64,plain,
relation_isomorphism(sK2,sK3,sK4),
inference(instantiation,[status(thm)],[18]) ).
cnf(l71,plain,
relation(sK4),
inference(instantiation,[status(thm)],[15]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l2,l3,l13,l23,l22,l34,l6,l41,l32,l35,l7,l53,l47,l39,l28,l36,l44,l50,l40,l55,l45,l52,l61,l29,l43,l30,l75,l51,l24,l46,l58,l78,l54,l72,l70,l64,l71]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.09 % Problem : SEU261+1 : TPTP v9.0.0. Released v3.3.0.
% 0.04/0.10 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.30 % Computer : n020.cluster.edu
% 0.09/0.30 % Model : x86_64 x86_64
% 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.30 % Memory : 8042.1875MB
% 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.30 % CPULimit : 300
% 0.09/0.30 % WCLimit : 300
% 0.09/0.30 % DateTime : Tue Jul 22 00:21:19 EDT 2025
% 0.09/0.30 % CPUTime :
% 0.09/0.30 % launching worker at depth: 2
% 0.09/0.30 % launching worker at depth: 3
% 0.09/0.30 % launching worker at depth: 6
% 0.09/0.30 % launching worker at depth: 4
% 0.09/0.30 % launching worker at depth: 5
% 0.09/0.30 % launching worker at depth: 7
% 0.09/0.30 % launching worker at depth: 1
% 0.09/0.30 % launching worker at depth: 8
% 0.09/0.30 % launching worker at depth: 9
% 0.09/0.31 % SZS status Theorem for theBenchmark
% 0.09/0.31 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------