%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEV625+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 : n009.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 118.27s 18.41s
% Output : CNFRefutation 118.27s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEV625+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.09/0.35 % Computer : n009.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 26 11:23:29 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 118.27/18.41 % SZS status Theorem for theBenchmark.p
% 118.27/18.41 % SZS output start CNFRefutation for theBenchmark.p
% 118.27/18.41 fof($_def_Coq.Relations.Relation_Definitions.inclusion, axiom, ! [X0] : ! [X1] : ! [X2] : (('cCoq$u2eRelations$u2eRelation$u$uDefinitions$u2einclusion$u$u$u24a3'(X0,X1,X2) <=> ! [X3] : ((t(X3,X0) => ! [X4] : ((t(X4,X0) => (p(happ(happ(X1,X3),X4)) => p(happ(happ(X2,X3),X4)))))))))).
% 118.27/18.41 fof($_def_HahnRelationsBasic.eqv_rel, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : (('cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a4'(X0,X1,X2,X3) <=> (X2 = X3 & p(happ(X1,X2)))))).
% 118.27/18.41 fof($_def_HahnRelationsBasic.functional, axiom, ! [X0] : ! [X1] : (('cHahnRelationsBasic$u2efunctional$u$u$u24a2'(X0,X1) <=> ! [X2] : ((t(X2,X0) => ! [X3] : ((t(X3,X0) => ! [X4] : ((t(X4,X0) => (p(happ(happ(X1,X2),X3)) => (p(happ(happ(X1,X2),X4)) => X3 = X4))))))))))).
% 118.27/18.41 fof(HahnRelationsBasic.BasicProperties.inclusion_eqv_rel_true, axiom, 'cCoq$u2eRelations$u2eRelation$u$uDefinitions$u2einclusion$u$u$u24a3'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom),'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,'c$u24$u$ulam$u$u167045'))).
% 118.27/18.41 fof($adef_HahnRelationsBasic.eqv_rel_$a4, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ((p(happ(happ(happ(happ('cHahnRelationsBasic$u2eeqv$u$urel',X0),X1),X2),X3)) <=> 'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a4'(X0,X1,X2,X3)))).
% 118.27/18.41 fof($adef_HahnRelationsBasic.eqv_rel_$a2, axiom, ! [X0] : ! [X1] : happ(happ('cHahnRelationsBasic$u2eeqv$u$urel',X0),X1) = 'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(X0,X1)).
% 118.27/18.41 fof(_HAMMER_GOAL, conjecture, 'cHahnRelationsBasic$u2efunctional$u$u$u24a2'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom))).
% 118.27/18.41 fof(negated_conjecture, negated_conjecture, ~'cHahnRelationsBasic$u2efunctional$u$u$u24a2'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)), inference(negate_conjecture, [status(cth)], [_HAMMER_GOAL])).
% 118.27/18.41 cnf(c2, plain, ~'cCoq$u2eRelations$u2eRelation$u$uDefinitions$u2einclusion$u$u$u24a3'(X0,X1,X2) | X3(X0,X1,X2), inference(clausification, [status(esa)], [$_def_Coq.Relations.Relation_Definitions.inclusion])).
% 118.27/18.41 cnf(c4, plain, ~t(X0,X1) | ~t(X2,X1) | ~X3(X1,X4,X5) | p(happ(happ(X5,X0),X2)) | ~p(happ(happ(X4,X0),X2)), inference(clausification, [status(esa)], [$_def_Coq.Relations.Relation_Definitions.inclusion])).
% 118.27/18.41 cnf(c22, plain, ~'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a4'(X0,X1,X2,X3) | X2 = X3, inference(clausification, [status(esa)], [$_def_HahnRelationsBasic.eqv_rel])).
% 118.27/18.41 cnf(c26, plain, 'cHahnRelationsBasic$u2efunctional$u$u$u24a2'(X0,X1) | ~X2(X0,X1), inference(clausification, [status(esa)], [$_def_HahnRelationsBasic.functional])).
% 118.27/18.41 cnf(c27, plain, ~t(X0,X1) | ~X2(X1,X3) | ~t(X4,X1) | X5 = X0 | ~p(happ(happ(X3,X4),X5)) | ~t(X5,X1) | ~p(happ(happ(X3,X4),X0)), inference(clausification, [status(esa)], [$_def_HahnRelationsBasic.functional])).
% 118.27/18.41 cnf(c28, plain, X0(X1,X2) | t(sK35(X1,X2),X1), inference(clausification, [status(esa)], [$_def_HahnRelationsBasic.functional])).
% 118.27/18.41 cnf(c29, plain, X0(X1,X2) | t(sK36(X1,X2),X1), inference(clausification, [status(esa)], [$_def_HahnRelationsBasic.functional])).
% 118.27/18.41 cnf(c31, plain, X0(X1,X2) | p(happ(happ(X2,sK35(X1,X2)),sK36(X1,X2))), inference(clausification, [status(esa)], [$_def_HahnRelationsBasic.functional])).
% 118.27/18.41 cnf(c32, plain, X0(X1,X2) | p(happ(happ(X2,sK35(X1,X2)),sK37(X1,X2))), inference(clausification, [status(esa)], [$_def_HahnRelationsBasic.functional])).
% 118.27/18.41 cnf(c33, plain, X0(X1,X2) | sK36(X1,X2) != sK37(X1,X2), inference(clausification, [status(esa)], [$_def_HahnRelationsBasic.functional])).
% 118.27/18.41 cnf(c173, plain, 'cCoq$u2eRelations$u2eRelation$u$uDefinitions$u2einclusion$u$u$u24a3'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom),'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,'c$u24$u$ulam$u$u167045')), inference(clausification, [status(esa)], [HahnRelationsBasic.BasicProperties.inclusion_eqv_rel_true])).
% 118.27/18.41 cnf(c188, plain, ~p(happ(happ(happ(happ('cHahnRelationsBasic$u2eeqv$u$urel',X0),X1),X2),X3)) | 'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a4'(X0,X1,X2,X3), inference(clausification, [status(esa)], [$adef_HahnRelationsBasic.eqv_rel_$a4])).
% 118.27/18.41 cnf(c191, plain, happ(happ('cHahnRelationsBasic$u2eeqv$u$urel',X0),X1) = 'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(X0,X1), inference(clausification, [status(esa)], [$adef_HahnRelationsBasic.eqv_rel_$a2])).
% 118.27/18.41 cnf(c205, plain, ~'cHahnRelationsBasic$u2efunctional$u$u$u24a2'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)), inference(clausification, [status(esa)], [negated_conjecture])).
% 118.27/18.41 cnf(d0, plain, ~p(happ(happ('cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(X0,X1),X2),X3)) | 'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a4'(X0,X1,X2,X3), inference(demodulation, [status(thm)], [c188,c191])).
% 118.27/18.41 cnf(d1, plain, 'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a4'(X0,X1,sK35(X2,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(X0,X1)),sK37(X2,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(X0,X1))) | 'Ts29'(X2,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(X0,X1)), inference(resolution, [status(thm)], [d0,c32])).
% 118.27/18.41 cnf(d2, plain, 'Ts29'(X0,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(X1,X2)) | sK35(X0,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(X1,X2)) = sK37(X0,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(X1,X2)), inference(resolution, [status(thm)], [d1,c22])).
% 118.27/18.41 cnf(d3, plain, sK35(X0,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(X1,X2)) = sK37(X0,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(X1,X2)) | 'cHahnRelationsBasic$u2efunctional$u$u$u24a2'(X0,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(X1,X2)), inference(resolution, [status(thm)], [d2,c26])).
% 118.27/18.41 cnf(d4, plain, sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) = sK37(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)), inference(resolution, [status(thm)], [d3,c205])).
% 118.27/18.41 cnf(d5, plain, sK36(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) != sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) | 'Ts29'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)), inference(superposition, [status(thm)], [d4,c33])).
% 118.27/18.41 cnf(d6, plain, 'Ts2'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom),'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,'c$u24$u$ulam$u$u167045')), inference(resolution, [status(thm)], [c173,c2])).
% 118.27/18.41 cnf(d7, plain, 'Ts29'(X0,X1) | ~'Ts2'(X2,X1,X3) | ~t(sK35(X0,X1),X2) | ~t(sK36(X0,X1),X2) | p(happ(happ(X3,sK35(X0,X1)),sK36(X0,X1))), inference(resolution, [status(thm)], [c31,c4])).
% 118.27/18.41 cnf(d8, plain, ~'Ts2'(X0,X1,X2) | ~t(sK35(X0,X1),X0) | p(happ(happ(X2,sK35(X0,X1)),sK36(X0,X1))) | 'Ts29'(X0,X1) | 'Ts29'(X0,X1), inference(resolution, [status(thm)], [d7,c29])).
% 118.27/18.41 cnf(d9, plain, 'Ts29'(X0,X1) | ~'Ts2'(X2,X1,X3) | ~t(sK35(X0,X1),X2) | ~t(sK37(X0,X1),X2) | p(happ(happ(X3,sK35(X0,X1)),sK37(X0,X1))), inference(resolution, [status(thm)], [c32,c4])).
% 118.27/18.41 cnf(d10, plain, ~t(sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)),X0) | ~'Ts2'(X0,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom),X1) | ~t(sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)),X0) | p(happ(happ(X1,sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom))),sK37(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)))) | 'Ts29'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)), inference(superposition, [status(thm)], [d4,d9])).
% 118.27/18.41 cnf(d11, plain, ~'Ts2'(X0,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom),X1) | ~t(sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)),X0) | p(happ(happ(X1,sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom))),sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)))) | 'Ts29'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)), inference(demodulation, [status(thm)], [d10,d4])).
% 118.27/18.41 cnf(d12, plain, ~'Ts2'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom),X0) | p(happ(happ(X0,sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom))),sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)))) | 'Ts29'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) | 'Ts29'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)), inference(resolution, [status(thm)], [d11,c28])).
% 118.27/18.41 cnf(d13, plain, ~'Ts2'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom),X0) | 'Ts29'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) | X1 = sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) | ~t(X1,X2) | ~t(sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)),X2) | ~t(sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)),X2) | ~p(happ(happ(X0,sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom))),X1)) | ~'Ts29'(X2,X0), inference(resolution, [status(thm)], [d12,c27])).
% 118.27/18.41 cnf(d14, plain, sK36(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) = sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) | ~'Ts2'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom),X0) | ~t(sK36(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)),X1) | ~t(sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)),X1) | ~'Ts29'(X1,X0) | 'Ts29'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) | ~'Ts2'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom),X0) | ~t(sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)),cA) | 'Ts29'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)), inference(resolution, [status(thm)], [d13,d8])).
% 118.27/18.41 cnf(d15, plain, sK36(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) = sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) | ~'Ts2'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom),X0) | ~t(sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)),cA) | ~t(sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)),cA) | ~'Ts29'(cA,X0) | 'Ts29'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) | 'Ts29'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)), inference(resolution, [status(thm)], [d14,c29])).
% 118.27/18.41 cnf(d16, plain, sK36(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) = sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) | ~'Ts2'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom),X0) | ~'Ts29'(cA,X0) | 'Ts29'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) | 'Ts29'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)), inference(resolution, [status(thm)], [d15,c28])).
% 118.27/18.41 cnf(d17, plain, sK36(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) = sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) | ~'Ts29'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,'c$u24$u$ulam$u$u167045')) | 'Ts29'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)), inference(resolution, [status(thm)], [d16,d6])).
% 118.27/18.41 cnf(d18, plain, sK36(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) = sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) | 'Ts29'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) | sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,'c$u24$u$ulam$u$u167045')) = sK37(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,'c$u24$u$ulam$u$u167045')), inference(resolution, [status(thm)], [d17,d2])).
% 118.27/18.41 cnf(d19, plain, sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,'c$u24$u$ulam$u$u167045')) = sK37(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,'c$u24$u$ulam$u$u167045')) | sK36(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) = sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) | 'cHahnRelationsBasic$u2efunctional$u$u$u24a2'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)), inference(resolution, [status(thm)], [d18,c26])).
% 118.27/18.41 cnf(d20, plain, sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,'c$u24$u$ulam$u$u167045')) = sK37(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,'c$u24$u$ulam$u$u167045')) | sK36(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) = sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)), inference(resolution, [status(thm)], [c205,d19])).
% 118.27/18.41 cnf(d21, plain, sK36(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,'c$u24$u$ulam$u$u167045')) != sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,'c$u24$u$ulam$u$u167045')) | 'Ts29'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,'c$u24$u$ulam$u$u167045')) | sK36(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) = sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)), inference(superposition, [status(thm)], [d20,c33])).
% 118.27/18.41 cnf(d22, plain, 'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a4'(X0,X1,sK35(X2,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(X0,X1)),sK36(X2,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(X0,X1))) | 'Ts29'(X2,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(X0,X1)), inference(resolution, [status(thm)], [d0,c31])).
% 118.27/18.41 cnf(d23, plain, 'Ts29'(X0,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(X1,X2)) | sK35(X0,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(X1,X2)) = sK36(X0,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(X1,X2)), inference(resolution, [status(thm)], [d22,c22])).
% 118.27/18.41 cnf(d24, plain, sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,'c$u24$u$ulam$u$u167045')) = sK36(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,'c$u24$u$ulam$u$u167045')) | sK36(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) = sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) | 'Ts29'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)), inference(resolution, [status(thm)], [d23,d17])).
% 118.27/18.41 cnf(d25, plain, sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,'c$u24$u$ulam$u$u167045')) = sK36(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,'c$u24$u$ulam$u$u167045')) | sK36(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) = sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) | 'cHahnRelationsBasic$u2efunctional$u$u$u24a2'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)), inference(resolution, [status(thm)], [d24,c26])).
% 118.27/18.41 cnf(d26, plain, sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,'c$u24$u$ulam$u$u167045')) = sK36(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,'c$u24$u$ulam$u$u167045')) | sK36(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) = sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)), inference(resolution, [status(thm)], [c205,d25])).
% 118.27/18.41 cnf(d27, plain, sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,'c$u24$u$ulam$u$u167045')) != sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,'c$u24$u$ulam$u$u167045')) | sK36(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) = sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) | 'Ts29'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,'c$u24$u$ulam$u$u167045')) | sK36(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) = sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)), inference(superposition, [status(thm)], [d26,d21])).
% 118.27/18.41 cnf(d28, plain, sK36(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) = sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) | 'Ts29'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,'c$u24$u$ulam$u$u167045')), inference(equality_resolution, [status(thm)], [d27])).
% 118.27/18.41 cnf(d29, plain, sK36(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) = sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) | sK36(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) = sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) | 'Ts29'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)), inference(resolution, [status(thm)], [d28,d17])).
% 118.27/18.41 cnf(d30, plain, sK36(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) = sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) | 'cHahnRelationsBasic$u2efunctional$u$u$u24a2'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)), inference(resolution, [status(thm)], [d29,c26])).
% 118.27/18.41 cnf(d31, plain, sK36(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)) = sK35(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)), inference(resolution, [status(thm)], [c205,d30])).
% 118.27/18.41 cnf(d32, plain, 'Ts29'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)), inference(resolution, [status(thm)], [d31,d5])).
% 118.27/18.41 cnf(d33, plain, 'cHahnRelationsBasic$u2efunctional$u$u$u24a2'(cA,'cHahnRelationsBasic$u2eeqv$u$urel$u$u$u24a2'(cA,cdom)), inference(resolution, [status(thm)], [d32,c26])).
% 118.27/18.41 cnf(d34, plain, $false, inference(resolution, [status(thm)], [c205,d33])).
% 118.27/18.41 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------