%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU275+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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:41:31 AM UTC 2026
% Result : Theorem 75.75s 21.31s
% Output : CNFRefutation 75.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 8
% Syntax : Number of formulae : 27 ( 14 unt; 0 def)
% Number of atoms : 60 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 59 ( 26 ~; 23 |; 4 &)
% ( 1 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-1 aty)
% Number of functors : 2 ( 2 usr; 1 con; 0-1 aty)
% Number of variables : 20 ( 4 sgn 9 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d4_wellord1,axiom,
! [X0] :
( relation(X0)
=> ( 'well$uordering'(X0)
<=> ( 'well$ufounded$urelation'(X0)
& connected(X0)
& antisymmetric(X0)
& transitive(X0)
& reflexive(X0) ) ) ) ).
fof(dt_k1_wellord2,axiom,
! [X0] : relation('inclusion$urelation'(X0)) ).
fof(t2_wellord2,lemma,
! [X0] : reflexive('inclusion$urelation'(X0)) ).
fof(t3_wellord2,lemma,
! [X0] : transitive('inclusion$urelation'(X0)) ).
fof(t4_wellord2,lemma,
! [X0] :
( ordinal(X0)
=> connected('inclusion$urelation'(X0)) ) ).
fof(t5_wellord2,lemma,
! [X0] : antisymmetric('inclusion$urelation'(X0)) ).
fof(t6_wellord2,lemma,
! [X0] :
( ordinal(X0)
=> 'well$ufounded$urelation'('inclusion$urelation'(X0)) ) ).
fof(t7_wellord2,conjecture,
! [X0] :
( ordinal(X0)
=> 'well$uordering'('inclusion$urelation'(X0)) ) ).
fof(negated_conjecture,negated_conjecture,
~ ! [X0] :
( ordinal(X0)
=> 'well$uordering'('inclusion$urelation'(X0)) ),
inference(negate_conjecture,[status(cth)],[t7_wellord2]) ).
cnf(c265,plain,
( ~ connected(X0)
| ~ 'well$ufounded$urelation'(X0)
| ~ relation(X0)
| ~ antisymmetric(X0)
| 'well$uordering'(X0)
| ~ reflexive(X0)
| ~ transitive(X0) ),
inference(clausification,[status(esa)],[d4_wellord1]) ).
cnf(c375,plain,
relation('inclusion$urelation'(X0)),
inference(clausification,[status(esa)],[dt_k1_wellord2]) ).
cnf(c663,plain,
reflexive('inclusion$urelation'(X0)),
inference(clausification,[status(esa)],[t2_wellord2]) ).
cnf(c703,plain,
transitive('inclusion$urelation'(X0)),
inference(clausification,[status(esa)],[t3_wellord2]) ).
cnf(c731,plain,
( connected('inclusion$urelation'(X0))
| ~ ordinal(X0) ),
inference(clausification,[status(esa)],[t4_wellord2]) ).
cnf(c763,plain,
antisymmetric('inclusion$urelation'(X0)),
inference(clausification,[status(esa)],[t5_wellord2]) ).
cnf(c781,plain,
( 'well$ufounded$urelation'('inclusion$urelation'(X0))
| ~ ordinal(X0) ),
inference(clausification,[status(esa)],[t6_wellord2]) ).
cnf(c821,plain,
ordinal(sK953),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c822,plain,
~ 'well$uordering'('inclusion$urelation'(sK953)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
connected('inclusion$urelation'(sK953)),
inference(resolution,[status(thm)],[c731,c821]) ).
cnf(d1,plain,
( ~ reflexive('inclusion$urelation'(X0))
| 'well$uordering'('inclusion$urelation'(X0))
| ~ 'well$ufounded$urelation'('inclusion$urelation'(X0))
| ~ transitive('inclusion$urelation'(X0))
| ~ connected('inclusion$urelation'(X0))
| ~ antisymmetric('inclusion$urelation'(X0)) ),
inference(resolution,[status(thm)],[c265,c375]) ).
cnf(d2,plain,
( 'well$uordering'('inclusion$urelation'(X0))
| ~ 'well$ufounded$urelation'('inclusion$urelation'(X0))
| ~ transitive('inclusion$urelation'(X0))
| ~ connected('inclusion$urelation'(X0))
| ~ antisymmetric('inclusion$urelation'(X0)) ),
inference(resolution,[status(thm)],[c663,d1]) ).
cnf(d3,plain,
( 'well$uordering'('inclusion$urelation'(X0))
| ~ 'well$ufounded$urelation'('inclusion$urelation'(X0))
| ~ connected('inclusion$urelation'(X0))
| ~ antisymmetric('inclusion$urelation'(X0)) ),
inference(resolution,[status(thm)],[c703,d2]) ).
cnf(d4,plain,
( 'well$uordering'('inclusion$urelation'(X0))
| ~ 'well$ufounded$urelation'('inclusion$urelation'(X0))
| ~ connected('inclusion$urelation'(X0)) ),
inference(resolution,[status(thm)],[c763,d3]) ).
cnf(d5,plain,
( 'well$uordering'('inclusion$urelation'(sK953))
| ~ 'well$ufounded$urelation'('inclusion$urelation'(sK953)) ),
inference(resolution,[status(thm)],[d4,d0]) ).
cnf(d6,plain,
~ 'well$ufounded$urelation'('inclusion$urelation'(sK953)),
inference(resolution,[status(thm)],[c822,d5]) ).
cnf(d7,plain,
'well$ufounded$urelation'('inclusion$urelation'(sK953)),
inference(resolution,[status(thm)],[c781,c821]) ).
cnf(d8,plain,
$false,
inference(resolution,[status(thm)],[d7,d6]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU275+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/10.38 % Computer : n010.cluster.edu
% 0.11/10.38 % Model : x86_64 x86_64
% 0.11/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/10.38 % Memory : 8046.5625MB
% 0.11/10.38 % OS : Linux 6.8.0-71-generic
% 0.11/10.38 % CPULimit : 300
% 0.11/10.38 % WCLimit : 300
% 0.11/10.38 % DateTime : Sat Sep 26 09:04:11 UTC 2026
% 0.11/10.39 % CPUTime :
% 0.11/10.39 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 75.75/21.31 % SZS status Theorem for theBenchmark.p
% 75.75/21.31 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------