%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEV629+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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 : Thu Sep 24 02:33:48 PM UTC 2026
% Result : Theorem 139.53s 18.33s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEV629+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.38 % Computer : n016.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Mon Sep 21 07:35:54 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.42/0.75 % Drodi V4.1.1
% 139.53/18.33 % Refutation found
% 139.53/18.33 % SZS status Theorem for theBenchmark: Theorem is valid
% 139.53/18.33 % SZS output start CNFRefutation for theBenchmark
% 139.53/18.33 fof(f181,axiom,(
% 139.53/18.33 (! [V0__A,V1__R] :( cCoq_2eRelations_2eRelation__Definitions_2ereflexive___24a2(V0__A,V1__R)<=> (! [V2__x] :( t(V2__x,V0__A)=> p(happ(happ(V1__R,V2__x),V2__x)) ) )) )),
% 139.53/18.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 139.53/18.33 fof(f290,axiom,(
% 139.53/18.33 (! [V0__A,V1__s,V2__s_27] :( cHahnSets_2eset__subset___24a3(V0__A,V1__s,V2__s_27)<=> (! [V3__x] :( t(V3__x,V0__A)=> ( p(happ(V1__s,V3__x))=> p(happ(V2__s_27,V3__x)) ) ) )) )),
% 139.53/18.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 139.53/18.33 fof(f2077,axiom,(
% 139.53/18.33 (! [V_24X1] : happ(cHahnSets_2eset__subset,V_24X1) = cHahnSets_2eset__subset___24a1(V_24X1) )),
% 139.53/18.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 139.53/18.33 fof(f2469,axiom,(
% 139.53/18.33 (! [V_24X1,V_24X2,V_24X3] :( p(happ(happ(happ(cHahnSets_2eset__subset,V_24X1),V_24X2),V_24X3))<=> cHahnSets_2eset__subset___24a3(V_24X1,V_24X2,V_24X3) ) )),
% 139.53/18.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 139.53/18.33 fof(f2963,conjecture,(
% 139.53/18.33 cCoq_2eRelations_2eRelation__Definitions_2ereflexive___24a2(c_24__type__35378,cHahnSets_2eset__subset___24a1(cA)) ),
% 139.53/18.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 139.53/18.33 fof(f2964,negated_conjecture,(
% 139.53/18.33 ~(cCoq_2eRelations_2eRelation__Definitions_2ereflexive___24a2(c_24__type__35378,cHahnSets_2eset__subset___24a1(cA)) )),
% 139.53/18.33 inference(negated_conjecture,[status(cth)],[f2963])).
% 139.53/18.33 fof(f4280,plain,(
% 139.53/18.33 ![V0__A,V1__R]: (cCoq_2eRelations_2eRelation__Definitions_2ereflexive___24a2(V0__A,V1__R)<=>(![V2__x]: (~t(V2__x,V0__A)|p(happ(happ(V1__R,V2__x),V2__x)))))),
% 139.53/18.33 inference(pre_NNF_transformation,[status(thm)],[f181])).
% 139.53/18.33 fof(f4281,plain,(
% 139.53/18.33 ![V0__A,V1__R]: ((~cCoq_2eRelations_2eRelation__Definitions_2ereflexive___24a2(V0__A,V1__R)|(![V2__x]: (~t(V2__x,V0__A)|p(happ(happ(V1__R,V2__x),V2__x)))))&(cCoq_2eRelations_2eRelation__Definitions_2ereflexive___24a2(V0__A,V1__R)|(?[V2__x]: (t(V2__x,V0__A)&~p(happ(happ(V1__R,V2__x),V2__x))))))),
% 139.53/18.33 inference(NNF_transformation,[status(thm)],[f4280])).
% 139.53/18.33 fof(f4282,plain,(
% 139.53/18.33 (![V0__A,V1__R]: (~cCoq_2eRelations_2eRelation__Definitions_2ereflexive___24a2(V0__A,V1__R)|(![V2__x]: (~t(V2__x,V0__A)|p(happ(happ(V1__R,V2__x),V2__x))))))&(![V0__A,V1__R]: (cCoq_2eRelations_2eRelation__Definitions_2ereflexive___24a2(V0__A,V1__R)|(?[V2__x]: (t(V2__x,V0__A)&~p(happ(happ(V1__R,V2__x),V2__x))))))),
% 139.53/18.33 inference(miniscoping,[status(thm)],[f4281])).
% 139.53/18.33 fof(f4283,plain,(
% 139.53/18.33 (![V0__A,V1__R]: (~cCoq_2eRelations_2eRelation__Definitions_2ereflexive___24a2(V0__A,V1__R)|(![V2__x]: (~t(V2__x,V0__A)|p(happ(happ(V1__R,V2__x),V2__x))))))&(![V0__A,V1__R]: (cCoq_2eRelations_2eRelation__Definitions_2ereflexive___24a2(V0__A,V1__R)|(t(sK223_skl(V1__R,V0__A),V0__A)&~p(happ(happ(V1__R,sK223_skl(V1__R,V0__A)),sK223_skl(V1__R,V0__A))))))),
% 139.53/18.33 inference(skolemize,[status(esa),new_symbols(skolem,[sK223_skl]),skolemize(V2__x,sK223_skl(V1__R,V0__A))],[f4282])).
% 139.53/18.33 fof(f4286,plain,(
% 139.53/18.33 ![X0,X1]: (cCoq_2eRelations_2eRelation__Definitions_2ereflexive___24a2(X0,X1)|~p(happ(happ(X1,sK223_skl(X1,X0)),sK223_skl(X1,X0))))),
% 139.53/18.33 inference(cnf_transformation,[status(thm)],[f4283])).
% 139.53/18.33 fof(f4825,plain,(
% 139.53/18.33 ![V0__A,V1__s,V2__s_27]: (cHahnSets_2eset__subset___24a3(V0__A,V1__s,V2__s_27)<=>(![V3__x]: (~t(V3__x,V0__A)|(~p(happ(V1__s,V3__x))|p(happ(V2__s_27,V3__x))))))),
% 139.53/18.33 inference(pre_NNF_transformation,[status(thm)],[f290])).
% 139.53/18.33 fof(f4826,plain,(
% 139.53/18.33 ![V0__A,V1__s,V2__s_27]: ((~cHahnSets_2eset__subset___24a3(V0__A,V1__s,V2__s_27)|(![V3__x]: (~t(V3__x,V0__A)|(~p(happ(V1__s,V3__x))|p(happ(V2__s_27,V3__x))))))&(cHahnSets_2eset__subset___24a3(V0__A,V1__s,V2__s_27)|(?[V3__x]: (t(V3__x,V0__A)&(p(happ(V1__s,V3__x))&~p(happ(V2__s_27,V3__x)))))))),
% 139.53/18.33 inference(NNF_transformation,[status(thm)],[f4825])).
% 139.53/18.33 fof(f4827,plain,(
% 139.53/18.33 (![V0__A,V1__s,V2__s_27]: (~cHahnSets_2eset__subset___24a3(V0__A,V1__s,V2__s_27)|(![V3__x]: (~t(V3__x,V0__A)|(~p(happ(V1__s,V3__x))|p(happ(V2__s_27,V3__x)))))))&(![V0__A,V1__s,V2__s_27]: (cHahnSets_2eset__subset___24a3(V0__A,V1__s,V2__s_27)|(?[V3__x]: (t(V3__x,V0__A)&(p(happ(V1__s,V3__x))&~p(happ(V2__s_27,V3__x)))))))),
% 8.65/18.63 inference(miniscoping,[status(thm)],[f4826])).
% 8.65/18.63 fof(f4828,plain,(
% 8.65/18.63 (![V0__A,V1__s,V2__s_27]: (~cHahnSets_2eset__subset___24a3(V0__A,V1__s,V2__s_27)|(![V3__x]: (~t(V3__x,V0__A)|(~p(happ(V1__s,V3__x))|p(happ(V2__s_27,V3__x)))))))&(![V0__A,V1__s,V2__s_27]: (cHahnSets_2eset__subset___24a3(V0__A,V1__s,V2__s_27)|(t(sK277_skl(V2__s_27,V1__s,V0__A),V0__A)&(p(happ(V1__s,sK277_skl(V2__s_27,V1__s,V0__A)))&~p(happ(V2__s_27,sK277_skl(V2__s_27,V1__s,V0__A)))))))),
% 8.65/18.63 inference(skolemize,[status(esa),new_symbols(skolem,[sK277_skl]),skolemize(V3__x,sK277_skl(V2__s_27,V1__s,V0__A))],[f4827])).
% 8.65/18.63 fof(f4831,plain,(
% 8.65/18.63 ![X0,X1,X2]: (cHahnSets_2eset__subset___24a3(X0,X1,X2)|p(happ(X1,sK277_skl(X2,X1,X0))))),
% 8.65/18.63 inference(cnf_transformation,[status(thm)],[f4828])).
% 8.65/18.63 fof(f4832,plain,(
% 8.65/18.63 ![X0,X1,X2]: (cHahnSets_2eset__subset___24a3(X0,X1,X2)|~p(happ(X2,sK277_skl(X2,X1,X0))))),
% 8.65/18.63 inference(cnf_transformation,[status(thm)],[f4828])).
% 8.65/18.63 fof(f11169,plain,(
% 8.65/18.63 ![X0]: (happ(cHahnSets_2eset__subset,X0)=cHahnSets_2eset__subset___24a1(X0))),
% 8.65/18.63 inference(cnf_transformation,[status(thm)],[f2077])).
% 8.65/18.63 fof(f11915,plain,(
% 8.65/18.63 ![V_24X1,V_24X2,V_24X3]: ((~p(happ(happ(happ(cHahnSets_2eset__subset,V_24X1),V_24X2),V_24X3))|cHahnSets_2eset__subset___24a3(V_24X1,V_24X2,V_24X3))&(p(happ(happ(happ(cHahnSets_2eset__subset,V_24X1),V_24X2),V_24X3))|~cHahnSets_2eset__subset___24a3(V_24X1,V_24X2,V_24X3)))),
% 8.65/18.63 inference(NNF_transformation,[status(thm)],[f2469])).
% 8.65/18.63 fof(f11916,plain,(
% 8.65/18.63 (![V_24X1,V_24X2,V_24X3]: (~p(happ(happ(happ(cHahnSets_2eset__subset,V_24X1),V_24X2),V_24X3))|cHahnSets_2eset__subset___24a3(V_24X1,V_24X2,V_24X3)))&(![V_24X1,V_24X2,V_24X3]: (p(happ(happ(happ(cHahnSets_2eset__subset,V_24X1),V_24X2),V_24X3))|~cHahnSets_2eset__subset___24a3(V_24X1,V_24X2,V_24X3)))),
% 8.65/18.63 inference(miniscoping,[status(thm)],[f11915])).
% 8.65/18.63 fof(f11918,plain,(
% 8.65/18.63 ![X0,X1,X2]: (p(happ(happ(happ(cHahnSets_2eset__subset,X0),X1),X2))|~cHahnSets_2eset__subset___24a3(X0,X1,X2))),
% 8.65/18.63 inference(cnf_transformation,[status(thm)],[f11916])).
% 8.65/18.63 fof(f13819,plain,(
% 8.65/18.63 ~cCoq_2eRelations_2eRelation__Definitions_2ereflexive___24a2(c_24__type__35378,cHahnSets_2eset__subset___24a1(cA))),
% 8.65/18.63 inference(cnf_transformation,[status(thm)],[f2964])).
% 8.65/18.63 fof(f17307,plain,(
% 8.65/18.63 ![X0,X1,X2]: (p(happ(happ(cHahnSets_2eset__subset___24a1(X0),X1),X2))|~cHahnSets_2eset__subset___24a3(X0,X1,X2))),
% 8.65/18.63 inference(forward_demodulation,[status(thm)],[f11169,f11918])).
% 8.65/18.63 fof(f46251,plain,(
% 8.65/18.63 ![X0,X1]: (cHahnSets_2eset__subset___24a3(X0,X1,X1)|cHahnSets_2eset__subset___24a3(X0,X1,X1))),
% 8.65/18.63 inference(resolution,[status(thm)],[f4832,f4831])).
% 8.65/18.63 fof(f46337,plain,(
% 8.65/18.63 ![X0,X1]: (cHahnSets_2eset__subset___24a3(X0,X1,X1))),
% 8.65/18.63 inference(duplicate_literals_removal,[status(thm)],[f46251])).
% 8.65/18.63 fof(f46344,plain,(
% 8.65/18.63 ![X0,X1]: (p(happ(happ(cHahnSets_2eset__subset___24a1(X0),X1),X1)))),
% 8.65/18.63 inference(resolution,[status(thm)],[f46337,f17307])).
% 8.65/18.63 fof(f46950,plain,(
% 8.65/18.63 ![X0,X1]: (cCoq_2eRelations_2eRelation__Definitions_2ereflexive___24a2(X0,cHahnSets_2eset__subset___24a1(X1)))),
% 8.65/18.63 inference(resolution,[status(thm)],[f46344,f4286])).
% 8.65/18.63 fof(f46952,plain,(
% 8.65/18.63 $false),
% 8.65/18.63 inference(backward_subsumption_resolution,[status(thm)],[f13819,f46950])).
% 8.65/18.63 % SZS output end CNFRefutation for theBenchmark.p
% 8.65/18.64 % Elapsed time: 18.243947 seconds
% 8.65/18.64 % CPU time: 141.145832 seconds
% 8.65/18.64 % Total memory used: 1.906 GB
% 8.65/18.64 % Net memory used: 1.865 GB
%------------------------------------------------------------------------------