%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEV629+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 : n007.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:48:59 AM UTC 2026
% Result : Theorem 41.34s 8.72s
% Output : CNFRefutation 41.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEV629+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.10/0.38 % Computer : n007.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sat Sep 26 11:23:25 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 41.34/8.72 % SZS status Theorem for theBenchmark.p
% 41.34/8.72 % SZS output start CNFRefutation for theBenchmark.p
% 41.34/8.72 fof($_def_Coq.Relations.Relation_Definitions.reflexive, axiom, ! [X0] : ! [X1] : (('cCoq$u2eRelations$u2eRelation$u$uDefinitions$u2ereflexive$u$u$u24a2'(X0,X1) <=> ! [X2] : ((t(X2,X0) => p(happ(happ(X1,X2),X2))))))).
% 41.34/8.72 fof($_def_HahnSets.set_subset, axiom, ! [X0] : ! [X1] : ! [X2] : (('cHahnSets$u2eset$u$usubset$u$u$u24a3'(X0,X1,X2) <=> ! [X3] : ((t(X3,X0) => (p(happ(X1,X3)) => p(happ(X2,X3)))))))).
% 41.34/8.72 fof($adef_HahnSets.set_subset_$a1, axiom, ! [X0] : happ('cHahnSets$u2eset$u$usubset',X0) = 'cHahnSets$u2eset$u$usubset$u$u$u24a1'(X0)).
% 41.34/8.72 fof($adef_HahnSets.set_subset_$a3, axiom, ! [X0] : ! [X1] : ! [X2] : ((p(happ(happ(happ('cHahnSets$u2eset$u$usubset',X0),X1),X2)) <=> 'cHahnSets$u2eset$u$usubset$u$u$u24a3'(X0,X1,X2)))).
% 41.34/8.72 fof(_HAMMER_GOAL, conjecture, 'cCoq$u2eRelations$u2eRelation$u$uDefinitions$u2ereflexive$u$u$u24a2'('c$u24$u$utype$u$u35378','cHahnSets$u2eset$u$usubset$u$u$u24a1'(cA))).
% 41.34/8.72 fof(negated_conjecture, negated_conjecture, ~'cCoq$u2eRelations$u2eRelation$u$uDefinitions$u2ereflexive$u$u$u24a2'('c$u24$u$utype$u$u35378','cHahnSets$u2eset$u$usubset$u$u$u24a1'(cA)), inference(negate_conjecture, [status(cth)], [_HAMMER_GOAL])).
% 41.34/8.72 cnf(c12, plain, 'cCoq$u2eRelations$u2eRelation$u$uDefinitions$u2ereflexive$u$u$u24a2'(X0,X1) | ~p(happ(happ(X1,sK10(X0,X1)),sK10(X0,X1))), inference(clausification, [status(esa)], [$_def_Coq.Relations.Relation_Definitions.reflexive])).
% 41.34/8.72 cnf(c34, plain, 'cHahnSets$u2eset$u$usubset$u$u$u24a3'(X0,X1,X2) | p(happ(X1,sK34(X0,X1,X2))), inference(clausification, [status(esa)], [$_def_HahnSets.set_subset])).
% 41.34/8.72 cnf(c35, plain, 'cHahnSets$u2eset$u$usubset$u$u$u24a3'(X0,X1,X2) | ~p(happ(X2,sK34(X0,X1,X2))), inference(clausification, [status(esa)], [$_def_HahnSets.set_subset])).
% 41.34/8.72 cnf(c132, plain, happ('cHahnSets$u2eset$u$usubset',X0) = 'cHahnSets$u2eset$u$usubset$u$u$u24a1'(X0), inference(clausification, [status(esa)], [$adef_HahnSets.set_subset_$a1])).
% 41.34/8.72 cnf(c139, plain, p(happ(happ(happ('cHahnSets$u2eset$u$usubset',X0),X1),X2)) | ~'cHahnSets$u2eset$u$usubset$u$u$u24a3'(X0,X1,X2), inference(clausification, [status(esa)], [$adef_HahnSets.set_subset_$a3])).
% 41.34/8.72 cnf(c144, plain, ~'cCoq$u2eRelations$u2eRelation$u$uDefinitions$u2ereflexive$u$u$u24a2'('c$u24$u$utype$u$u35378','cHahnSets$u2eset$u$usubset$u$u$u24a1'(cA)), inference(clausification, [status(esa)], [negated_conjecture])).
% 41.34/8.72 cnf(d0, plain, p(happ(happ('cHahnSets$u2eset$u$usubset$u$u$u24a1'(X0),X1),X2)) | ~'cHahnSets$u2eset$u$usubset$u$u$u24a3'(X0,X1,X2), inference(demodulation, [status(thm)], [c139,c132])).
% 41.34/8.72 cnf(d1, plain, ~'cHahnSets$u2eset$u$usubset$u$u$u24a3'(X0,sK10(X1,'cHahnSets$u2eset$u$usubset$u$u$u24a1'(X0)),sK10(X1,'cHahnSets$u2eset$u$usubset$u$u$u24a1'(X0))) | 'cCoq$u2eRelations$u2eRelation$u$uDefinitions$u2ereflexive$u$u$u24a2'(X1,'cHahnSets$u2eset$u$usubset$u$u$u24a1'(X0)), inference(resolution, [status(thm)], [d0,c12])).
% 41.34/8.72 cnf(d2, plain, 'cHahnSets$u2eset$u$usubset$u$u$u24a3'(X0,X1,X1) | 'cHahnSets$u2eset$u$usubset$u$u$u24a3'(X0,X1,X1), inference(resolution, [status(thm)], [c35,c34])).
% 41.34/8.72 cnf(d3, plain, 'cCoq$u2eRelations$u2eRelation$u$uDefinitions$u2ereflexive$u$u$u24a2'(X0,'cHahnSets$u2eset$u$usubset$u$u$u24a1'(X1)), inference(resolution, [status(thm)], [d2,d1])).
% 41.34/8.72 cnf(d4, plain, $false, inference(resolution, [status(thm)], [d3,c144])).
% 41.34/8.72 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------