%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : COM146+1 : TPTP v8.1.2. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n032.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:17:56 EDT 2024
% Result : Theorem 159.97s 160.14s
% Output : Refutation 159.97s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.09 % Problem : COM146+1 : TPTP v8.1.2. Released v6.4.0.
% 0.06/0.10 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.29 % Computer : n032.cluster.edu
% 0.09/0.29 % Model : x86_64 x86_64
% 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.29 % Memory : 8042.1875MB
% 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.29 % CPULimit : 300
% 0.09/0.29 % WCLimit : 300
% 0.09/0.29 % DateTime : Thu May 9 07:10:22 EDT 2024
% 0.09/0.29 % CPUTime :
% 159.97/160.14 % Version: 1.5
% 159.97/160.14 % SZS status Theorem
% 159.97/160.14 % SZS output start CNFRefutation
% 159.97/160.14 fof(isSomeExp1,axiom,(![Ve]:(![VOptExp0]:(VOptExp0=vsomeExp(Ve)=>visSomeExp(VOptExp0)))),file('/export/starexec/sandbox2/benchmark/Axioms/COM001+0.ax', isSomeExp1)).
% 159.97/160.14 fof(c10124,plain,(![Ve]:(![VOptExp0]:(VOptExp0!=vsomeExp(Ve)|visSomeExp(VOptExp0)))),inference(fof_nnf,[status(thm)],[isSomeExp1])).
% 159.97/160.14 fof(c10125,plain,(![X140]:(![X141]:(X141!=vsomeExp(X140)|visSomeExp(X141)))),inference(variable_rename,[status(thm)],[c10124])).
% 159.97/160.14 cnf(c10126,plain,X374!=vsomeExp(X375)|visSomeExp(X374),inference(split_conjunct,[status(thm)],[c10125])).
% 159.97/160.14 cnf(transitivity,axiom,X368!=X367|X367!=X369|X368=X369,theory(equality)).
% 159.97/160.14 fof('T-Preservation-T-var',conjecture,(![Vx]:(![VC]:(![Veout]:(![VT]:((vreduce(vvar(Vx))=vsomeExp(Veout)&vtcheck(VC,vvar(Vx),VT))=>vtcheck(VC,Veout,VT)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'T-Preservation-T-var')).
% 159.97/160.14 fof(c18,negated_conjecture,(~(![Vx]:(![VC]:(![Veout]:(![VT]:((vreduce(vvar(Vx))=vsomeExp(Veout)&vtcheck(VC,vvar(Vx),VT))=>vtcheck(VC,Veout,VT))))))),inference(assume_negation,[status(cth)],['T-Preservation-T-var'])).
% 159.97/160.14 fof(c19,negated_conjecture,(?[Vx]:(?[VC]:(?[Veout]:(?[VT]:((vreduce(vvar(Vx))=vsomeExp(Veout)&vtcheck(VC,vvar(Vx),VT))&~vtcheck(VC,Veout,VT)))))),inference(fof_nnf,[status(thm)],[c18])).
% 159.97/160.14 fof(c20,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:((vreduce(vvar(X2))=vsomeExp(X4)&vtcheck(X3,vvar(X2),X5))&~vtcheck(X3,X4,X5)))))),inference(variable_rename,[status(thm)],[c19])).
% 159.97/160.14 fof(c21,negated_conjecture,((vreduce(vvar(skolem0001))=vsomeExp(skolem0003)&vtcheck(skolem0002,vvar(skolem0001),skolem0004))&~vtcheck(skolem0002,skolem0003,skolem0004)),inference(skolemize,[status(esa)],[c20])).
% 159.97/160.14 cnf(c22,negated_conjecture,vreduce(vvar(skolem0001))=vsomeExp(skolem0003),inference(split_conjunct,[status(thm)],[c21])).
% 159.97/160.14 cnf(c31372,plain,X1686!=vreduce(vvar(skolem0001))|X1686=vsomeExp(skolem0003),inference(resolution,[status(thm)],[c22, transitivity])).
% 159.97/160.14 cnf(c11,axiom,X467!=X466|vreduce(X467)=vreduce(X466),theory(equality)).
% 159.97/160.14 cnf(c0,axiom,X377!=X376|vvar(X377)=vvar(X376),theory(equality)).
% 159.97/160.14 cnf(reflexivity,axiom,X360=X360,theory(equality)).
% 159.97/160.14 fof(getSomeType0,axiom,(![VOptTyp0]:(![RESULT]:(![Ve]:(VOptTyp0=vsomeType(Ve)=>(RESULT=vgetSomeType(VOptTyp0)=>RESULT=Ve))))),file('/export/starexec/sandbox2/benchmark/Axioms/COM001+0.ax', getSomeType0)).
% 159.97/160.14 fof(c31239,plain,(![VOptTyp0]:(![RESULT]:(![Ve]:(VOptTyp0!=vsomeType(Ve)|(RESULT!=vgetSomeType(VOptTyp0)|RESULT=Ve))))),inference(fof_nnf,[status(thm)],[getSomeType0])).
% 159.97/160.14 fof(c31240,plain,(![X274]:(![X275]:(![X276]:(X274!=vsomeType(X276)|(X275!=vgetSomeType(X274)|X275=X276))))),inference(variable_rename,[status(thm)],[c31239])).
% 159.97/160.14 cnf(c31241,plain,X955!=vsomeType(X954)|X956!=vgetSomeType(X955)|X956=X954,inference(split_conjunct,[status(thm)],[c31240])).
% 159.97/160.14 cnf(c32373,plain,X958!=vsomeType(X957)|vgetSomeType(X958)=X957,inference(resolution,[status(thm)],[c31241, reflexivity])).
% 159.97/160.14 cnf(c32379,plain,vgetSomeType(vsomeType(X961))=X961,inference(resolution,[status(thm)],[c32373, reflexivity])).
% 159.97/160.14 cnf(c32404,plain,vvar(vgetSomeType(vsomeType(X1025)))=vvar(X1025),inference(resolution,[status(thm)],[c32379, c0])).
% 159.97/160.14 cnf(c32780,plain,vreduce(vvar(vgetSomeType(vsomeType(X2786))))=vreduce(vvar(X2786)),inference(resolution,[status(thm)],[c32404, c11])).
% 159.97/160.14 cnf(c46899,plain,vreduce(vvar(vgetSomeType(vsomeType(skolem0001))))=vsomeExp(skolem0003),inference(resolution,[status(thm)],[c32780, c31372])).
% 159.97/160.14 cnf(c72584,plain,visSomeExp(vreduce(vvar(vgetSomeType(vsomeType(skolem0001))))),inference(resolution,[status(thm)],[c46899, c10126])).
% 159.97/160.14 fof(isSomeExp0,axiom,(![VOptExp0]:(VOptExp0=vnoExp=>(~visSomeExp(VOptExp0)))),file('/export/starexec/sandbox2/benchmark/Axioms/COM001+0.ax', isSomeExp0)).
% 159.97/160.14 fof(c10127,plain,(![VOptExp0]:(VOptExp0=vnoExp=>~visSomeExp(VOptExp0))),inference(fof_simplification,[status(thm)],[isSomeExp0])).
% 159.97/160.14 fof(c10128,plain,(![VOptExp0]:(VOptExp0!=vnoExp|~visSomeExp(VOptExp0))),inference(fof_nnf,[status(thm)],[c10127])).
% 159.97/160.14 fof(c10129,plain,(![X142]:(X142!=vnoExp|~visSomeExp(X142))),inference(variable_rename,[status(thm)],[c10128])).
% 159.97/160.14 cnf(c10130,plain,X366!=vnoExp|~visSomeExp(X366),inference(split_conjunct,[status(thm)],[c10129])).
% 159.97/160.14 cnf(symmetry,axiom,X363!=X362|X362=X363,theory(equality)).
% 159.97/160.14 fof(getSomeExp0,axiom,(![VOptExp0]:(![RESULT]:(![Ve]:(VOptExp0=vsomeExp(Ve)=>(RESULT=vgetSomeExp(VOptExp0)=>RESULT=Ve))))),file('/export/starexec/sandbox2/benchmark/Axioms/COM001+0.ax', getSomeExp0)).
% 159.97/160.14 fof(c10121,plain,(![VOptExp0]:(![RESULT]:(![Ve]:(VOptExp0!=vsomeExp(Ve)|(RESULT!=vgetSomeExp(VOptExp0)|RESULT=Ve))))),inference(fof_nnf,[status(thm)],[getSomeExp0])).
% 159.97/160.14 fof(c10122,plain,(![X137]:(![X138]:(![X139]:(X137!=vsomeExp(X139)|(X138!=vgetSomeExp(X137)|X138=X139))))),inference(variable_rename,[status(thm)],[c10121])).
% 159.97/160.14 cnf(c10123,plain,X571!=vsomeExp(X569)|X570!=vgetSomeExp(X571)|X570=X569,inference(split_conjunct,[status(thm)],[c10122])).
% 159.97/160.14 cnf(c31430,plain,X575!=vsomeExp(X576)|vgetSomeExp(X575)=X576,inference(resolution,[status(thm)],[c10123, reflexivity])).
% 159.97/160.14 cnf(c31432,plain,vgetSomeExp(vsomeExp(X577))=X577,inference(resolution,[status(thm)],[c31430, reflexivity])).
% 159.97/160.14 cnf(c31454,plain,vgetSomeExp(vgetSomeExp(vsomeExp(vsomeExp(X640))))=X640,inference(resolution,[status(thm)],[c31432, c31430])).
% 159.97/160.14 cnf(c31649,plain,X688=vgetSomeExp(vgetSomeExp(vsomeExp(vsomeExp(X688)))),inference(resolution,[status(thm)],[c31454, symmetry])).
% 159.97/160.14 cnf(c32029,plain,vvar(X2294)=vvar(vgetSomeExp(vgetSomeExp(vsomeExp(vsomeExp(X2294))))),inference(resolution,[status(thm)],[c31649, c0])).
% 159.97/160.14 fof(reduce0,axiom,(![Vx]:(![VExp0]:(![RESULT]:(VExp0=vvar(Vx)=>(RESULT=vreduce(VExp0)=>RESULT=vnoExp))))),file('/export/starexec/sandbox2/benchmark/Axioms/COM001+0.ax', reduce0)).
% 159.97/160.14 fof(c10116,plain,(![Vx]:(![VExp0]:(![RESULT]:(VExp0!=vvar(Vx)|(RESULT!=vreduce(VExp0)|RESULT=vnoExp))))),inference(fof_nnf,[status(thm)],[reduce0])).
% 159.97/160.14 fof(c10117,plain,(![Vx]:(![VExp0]:(VExp0!=vvar(Vx)|(![RESULT]:(RESULT!=vreduce(VExp0)|RESULT=vnoExp))))),inference(shift_quantors,[status(thm)],[c10116])).
% 159.97/160.14 fof(c10119,plain,(![X134]:(![X135]:(![X136]:(X135!=vvar(X134)|(X136!=vreduce(X135)|X136=vnoExp))))),inference(shift_quantors,[status(thm)],[fof(c10118,plain,(![X134]:(![X135]:(X135!=vvar(X134)|(![X136]:(X136!=vreduce(X135)|X136=vnoExp))))),inference(variable_rename,[status(thm)],[c10117])).])).
% 159.97/160.14 cnf(c10120,plain,X6226!=vvar(X6228)|X6227!=vreduce(X6226)|X6227=vnoExp,inference(split_conjunct,[status(thm)],[c10119])).
% 159.97/160.14 cnf(c81956,plain,X6230!=vvar(X6229)|vreduce(X6230)=vnoExp,inference(resolution,[status(thm)],[c10120, reflexivity])).
% 159.97/160.14 cnf(c82061,plain,vreduce(vvar(X6231))=vnoExp,inference(resolution,[status(thm)],[c81956, c32029])).
% 159.97/160.14 cnf(c82300,plain,~visSomeExp(vreduce(vvar(X6232))),inference(resolution,[status(thm)],[c82061, c10130])).
% 159.97/160.14 cnf(c82377,plain,$false,inference(resolution,[status(thm)],[c82300, c72584])).
% 159.97/160.14 % SZS output end CNFRefutation
% 159.97/160.14
% 159.97/160.14 % Initial clauses : 31162
% 159.97/160.14 % Processed clauses : 1947
% 159.97/160.14 % Factors computed : 10
% 159.97/160.14 % Resolvents computed: 51041
% 159.97/160.14 % Tautologies deleted: 5
% 159.97/160.14 % Forward subsumed : 2390
% 159.97/160.14 % Backward subsumed : 0
% 159.97/160.14 % -------- CPU Time ---------
% 159.97/160.14 % User time : 159.560 s
% 159.97/160.14 % System time : 0.293 s
% 159.97/160.14 % Total time : 159.853 s
%------------------------------------------------------------------------------