%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEV677+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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:49:03 AM UTC 2026
% Result : Theorem 71.91s 11.01s
% Output : CNFRefutation 71.91s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEV677+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n019.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 26 11:37:35 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 71.91/11.01 % SZS status Theorem for theBenchmark.p
% 71.91/11.01 % SZS output start CNFRefutation for theBenchmark.p
% 71.91/11.01 fof($_def_UrysohnsLemma.Urysohns_Lemma_construction.Un, axiom, ! [X0] : (('cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X0) => ((X0 = 'cCoq$u2eInit$u2eDatatypes$u2eO' & 'cUrysohnsLemma$u2eUrysohns$u$uLemma$u$uconstruction$u2eUn$u$u$u24a1'(X0) = cU0) | ? [X1] : (('cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X1) & ('cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X1) => (X0 = 'cCoq$u2eInit$u2eDatatypes$u2eS$u$u$u24a1'(X1) & ((X1 = 'cCoq$u2eInit$u2eDatatypes$u2eO' & 'cUrysohnsLemma$u2eUrysohns$u$uLemma$u$uconstruction$u2eUn$u$u$u24a1'(X0) = cU1) | ? [X2] : (('cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X2) & (X1 = 'cCoq$u2eInit$u2eDatatypes$u2eS$u$u$u24a1'(X2) & 'cUrysohnsLemma$u2eUrysohns$u$uLemma$u$uconstruction$u2eUn$u$u$u24a1'(X0) = 'cCoq$u2eSets$u2eEnsembles$u2eFull$u$uset$u$u$u24a1'('cTopology$u2eTopologicalSpaces$u2epoint$u$uset$u$u$u24a1'(cX)))))))))))))).
% 71.91/11.01 fof($_discrim_Coq.Init.Datatypes.O$Coq.Init.Datatypes.S, axiom, ! [X0] : 'cCoq$u2eInit$u2eDatatypes$u2eO' != 'cCoq$u2eInit$u2eDatatypes$u2eS$u$u$u24a1'(X0)).
% 71.91/11.01 fof($_typeof_Coq.Init.Datatypes.O, axiom, 'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'('cCoq$u2eInit$u2eDatatypes$u2eO')).
% 71.91/11.01 fof($_typeof_X, axiom, 'cTopology$u2eTopologicalSpaces$u2eTopologicalSpace$u$u$u24t'(cX)).
% 71.91/11.01 fof(Topology.TopologicalSpaces.open_full, axiom, ! [X0] : (('cTopology$u2eTopologicalSpaces$u2eTopologicalSpace$u$u$u24t'(X0) => 'cTopology$u2eTopologicalSpaces$u2eopen$u$u$u24a2'(X0,'cCoq$u2eSets$u2eEnsembles$u2eFull$u$uset$u$u$u24a1'('cTopology$u2eTopologicalSpaces$u2epoint$u$uset$u$u$u24a1'(X0)))))).
% 71.91/11.01 fof(U0_open, axiom, 'cTopology$u2eTopologicalSpaces$u2eopen$u$u$u24a2'(cX,cU0)).
% 71.91/11.01 fof(U1_open, axiom, 'cTopology$u2eTopologicalSpaces$u2eopen$u$u$u24a2'(cX,cU1)).
% 71.91/11.01 fof(_HAMMER_GOAL, conjecture, ! [X0] : (('cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X0) => 'cTopology$u2eTopologicalSpaces$u2eopen$u$u$u24a2'(cX,'cUrysohnsLemma$u2eUrysohns$u$uLemma$u$uconstruction$u2eUn$u$u$u24a1'(X0))))).
% 71.91/11.01 fof(negated_conjecture, negated_conjecture, ~! [X0] : (('cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X0) => 'cTopology$u2eTopologicalSpaces$u2eopen$u$u$u24a2'(cX,'cUrysohnsLemma$u2eUrysohns$u$uLemma$u$uconstruction$u2eUn$u$u$u24a1'(X0)))), inference(negate_conjecture, [status(cth)], [_HAMMER_GOAL])).
% 71.91/11.01 cnf(c30, plain, ~'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X0) | X0 = 'cCoq$u2eInit$u2eDatatypes$u2eO' | X1(X0), inference(clausification, [status(esa)], [$_def_UrysohnsLemma.Urysohns_Lemma_construction.Un])).
% 71.91/11.01 cnf(c31, plain, ~'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X0) | 'cUrysohnsLemma$u2eUrysohns$u$uLemma$u$uconstruction$u2eUn$u$u$u24a1'(X0) = cU0 | X1(X0), inference(clausification, [status(esa)], [$_def_UrysohnsLemma.Urysohns_Lemma_construction.Un])).
% 71.91/11.01 cnf(c34, plain, ~X0(X1,X2) | 'cUrysohnsLemma$u2eUrysohns$u$uLemma$u$uconstruction$u2eUn$u$u$u24a1'(X1) = 'cCoq$u2eSets$u2eEnsembles$u2eFull$u$uset$u$u$u24a1'('cTopology$u2eTopologicalSpaces$u2epoint$u$uset$u$u$u24a1'(cX)), inference(clausification, [status(esa)], [$_def_UrysohnsLemma.Urysohns_Lemma_construction.Un])).
% 71.91/11.01 cnf(c35, plain, ~X0(X1) | 'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(sK34(X1)), inference(clausification, [status(esa)], [$_def_UrysohnsLemma.Urysohns_Lemma_construction.Un])).
% 71.91/11.01 cnf(c36, plain, ~X0(X1) | ~'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(sK34(X1)) | X1 = 'cCoq$u2eInit$u2eDatatypes$u2eS$u$u$u24a1'(sK34(X1)), inference(clausification, [status(esa)], [$_def_UrysohnsLemma.Urysohns_Lemma_construction.Un])).
% 71.91/11.01 cnf(c38, plain, ~X0(X1) | ~'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(sK34(X1)) | 'cUrysohnsLemma$u2eUrysohns$u$uLemma$u$uconstruction$u2eUn$u$u$u24a1'(X1) = cU1 | X2(X1,sK34(X1)), inference(clausification, [status(esa)], [$_def_UrysohnsLemma.Urysohns_Lemma_construction.Un])).
% 71.91/11.01 cnf(c39, plain, 'cCoq$u2eInit$u2eDatatypes$u2eO' != 'cCoq$u2eInit$u2eDatatypes$u2eS$u$u$u24a1'(X0), inference(clausification, [status(esa)], [$_discrim_Coq.Init.Datatypes.O$Coq.Init.Datatypes.S])).
% 71.91/11.01 cnf(c61, plain, 'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'('cCoq$u2eInit$u2eDatatypes$u2eO'), inference(clausification, [status(esa)], [$_typeof_Coq.Init.Datatypes.O])).
% 71.91/11.01 cnf(c65, plain, 'cTopology$u2eTopologicalSpaces$u2eTopologicalSpace$u$u$u24t'(cX), inference(clausification, [status(esa)], [$_typeof_X])).
% 71.91/11.01 cnf(c216, plain, ~'cTopology$u2eTopologicalSpaces$u2eTopologicalSpace$u$u$u24t'(X0) | 'cTopology$u2eTopologicalSpaces$u2eopen$u$u$u24a2'(X0,'cCoq$u2eSets$u2eEnsembles$u2eFull$u$uset$u$u$u24a1'('cTopology$u2eTopologicalSpaces$u2epoint$u$uset$u$u$u24a1'(X0))), inference(clausification, [status(esa)], [Topology.TopologicalSpaces.open_full])).
% 71.91/11.01 cnf(c220, plain, 'cTopology$u2eTopologicalSpaces$u2eopen$u$u$u24a2'(cX,cU0), inference(clausification, [status(esa)], [U0_open])).
% 71.91/11.01 cnf(c221, plain, 'cTopology$u2eTopologicalSpaces$u2eopen$u$u$u24a2'(cX,cU1), inference(clausification, [status(esa)], [U1_open])).
% 71.91/11.01 cnf(c241, plain, 'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(sK436), inference(clausification, [status(esa)], [negated_conjecture])).
% 71.91/11.01 cnf(c242, plain, ~'cTopology$u2eTopologicalSpaces$u2eopen$u$u$u24a2'(cX,'cUrysohnsLemma$u2eUrysohns$u$uLemma$u$uconstruction$u2eUn$u$u$u24a1'(sK436)), inference(clausification, [status(esa)], [negated_conjecture])).
% 71.91/11.01 cnf(d0, plain, 'cUrysohnsLemma$u2eUrysohns$u$uLemma$u$uconstruction$u2eUn$u$u$u24a1'('cCoq$u2eInit$u2eDatatypes$u2eO') = cU0 | 'Ts31'('cCoq$u2eInit$u2eDatatypes$u2eO'), inference(resolution, [status(thm)], [c31,c61])).
% 71.91/11.01 cnf(d1, plain, ~'Ts31'(X0) | X0 = 'cCoq$u2eInit$u2eDatatypes$u2eS$u$u$u24a1'(sK34(X0)) | ~'Ts31'(X0), inference(resolution, [status(thm)], [c35,c36])).
% 71.91/11.01 cnf(d2, plain, 'cCoq$u2eInit$u2eDatatypes$u2eO' = 'cCoq$u2eInit$u2eDatatypes$u2eS$u$u$u24a1'(sK34('cCoq$u2eInit$u2eDatatypes$u2eO')) | 'cUrysohnsLemma$u2eUrysohns$u$uLemma$u$uconstruction$u2eUn$u$u$u24a1'('cCoq$u2eInit$u2eDatatypes$u2eO') = cU0, inference(resolution, [status(thm)], [d1,d0])).
% 71.91/11.01 cnf(d3, plain, 'cUrysohnsLemma$u2eUrysohns$u$uLemma$u$uconstruction$u2eUn$u$u$u24a1'('cCoq$u2eInit$u2eDatatypes$u2eO') = cU0, inference(resolution, [status(thm)], [c39,d2])).
% 71.91/11.01 cnf(d4, plain, sK436 = 'cCoq$u2eInit$u2eDatatypes$u2eO' | 'Ts31'(sK436), inference(resolution, [status(thm)], [c30,c241])).
% 71.91/11.01 cnf(d5, plain, ~'Ts31'(X0) | 'cUrysohnsLemma$u2eUrysohns$u$uLemma$u$uconstruction$u2eUn$u$u$u24a1'(X0) = cU1 | ~'Ts31'(X0) | 'Ts30'(X0,sK34(X0)), inference(resolution, [status(thm)], [c35,c38])).
% 71.91/11.01 cnf(d6, plain, 'cUrysohnsLemma$u2eUrysohns$u$uLemma$u$uconstruction$u2eUn$u$u$u24a1'(X0) = cU1 | ~'Ts31'(X0) | 'cUrysohnsLemma$u2eUrysohns$u$uLemma$u$uconstruction$u2eUn$u$u$u24a1'(X0) = 'cCoq$u2eSets$u2eEnsembles$u2eFull$u$uset$u$u$u24a1'('cTopology$u2eTopologicalSpaces$u2epoint$u$uset$u$u$u24a1'(cX)), inference(resolution, [status(thm)], [d5,c34])).
% 71.91/11.01 cnf(d7, plain, 'cUrysohnsLemma$u2eUrysohns$u$uLemma$u$uconstruction$u2eUn$u$u$u24a1'(sK436) = 'cCoq$u2eSets$u2eEnsembles$u2eFull$u$uset$u$u$u24a1'('cTopology$u2eTopologicalSpaces$u2epoint$u$uset$u$u$u24a1'(cX)) | 'cUrysohnsLemma$u2eUrysohns$u$uLemma$u$uconstruction$u2eUn$u$u$u24a1'(sK436) = cU1 | sK436 = 'cCoq$u2eInit$u2eDatatypes$u2eO', inference(resolution, [status(thm)], [d6,d4])).
% 71.91/11.01 cnf(d8, plain, 'cTopology$u2eTopologicalSpaces$u2eopen$u$u$u24a2'(cX,'cUrysohnsLemma$u2eUrysohns$u$uLemma$u$uconstruction$u2eUn$u$u$u24a1'(sK436)) | ~'cTopology$u2eTopologicalSpaces$u2eTopologicalSpace$u$u$u24t'(cX) | 'cUrysohnsLemma$u2eUrysohns$u$uLemma$u$uconstruction$u2eUn$u$u$u24a1'(sK436) = cU1 | sK436 = 'cCoq$u2eInit$u2eDatatypes$u2eO', inference(superposition, [status(thm)], [d7,c216])).
% 71.91/11.01 cnf(d9, plain, 'cUrysohnsLemma$u2eUrysohns$u$uLemma$u$uconstruction$u2eUn$u$u$u24a1'(sK436) = cU1 | sK436 = 'cCoq$u2eInit$u2eDatatypes$u2eO' | ~'cTopology$u2eTopologicalSpaces$u2eTopologicalSpace$u$u$u24t'(cX), inference(resolution, [status(thm)], [c242,d8])).
% 71.91/11.01 cnf(d10, plain, 'cUrysohnsLemma$u2eUrysohns$u$uLemma$u$uconstruction$u2eUn$u$u$u24a1'(sK436) = cU1 | sK436 = 'cCoq$u2eInit$u2eDatatypes$u2eO', inference(resolution, [status(thm)], [c65,d9])).
% 71.91/11.01 cnf(d11, plain, ~'cTopology$u2eTopologicalSpaces$u2eopen$u$u$u24a2'(cX,cU1) | sK436 = 'cCoq$u2eInit$u2eDatatypes$u2eO', inference(superposition, [status(thm)], [d10,c242])).
% 71.91/11.01 cnf(d12, plain, sK436 = 'cCoq$u2eInit$u2eDatatypes$u2eO', inference(resolution, [status(thm)], [c221,d11])).
% 71.91/11.01 cnf(d13, plain, ~'cTopology$u2eTopologicalSpaces$u2eopen$u$u$u24a2'(cX,'cUrysohnsLemma$u2eUrysohns$u$uLemma$u$uconstruction$u2eUn$u$u$u24a1'('cCoq$u2eInit$u2eDatatypes$u2eO')), inference(demodulation, [status(thm)], [c242,d12])).
% 71.91/11.01 cnf(d14, plain, ~'cTopology$u2eTopologicalSpaces$u2eopen$u$u$u24a2'(cX,cU0), inference(demodulation, [status(thm)], [d13,d3])).
% 71.91/11.01 cnf(d15, plain, $false, inference(resolution, [status(thm)], [c220,d14])).
% 71.91/11.01 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------