%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : ALG201+1 : TPTP v8.1.2. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n019.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:14:54 EDT 2024
% Result : Theorem 10.60s 10.80s
% Output : Refutation 10.60s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : ALG201+1 : TPTP v8.1.2. Released v2.7.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.35 % Computer : n019.cluster.edu
% 0.15/0.35 % Model : x86_64 x86_64
% 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.35 % Memory : 8042.1875MB
% 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.35 % CPULimit : 300
% 0.15/0.35 % WCLimit : 300
% 0.15/0.35 % DateTime : Thu May 9 00:34:53 EDT 2024
% 0.15/0.35 % CPUTime :
% 10.60/10.80 % Version: 1.5
% 10.60/10.80 % SZS status Theorem
% 10.60/10.80 % SZS output start CNFRefutation
% 10.60/10.80 fof(ax4,axiom,(~(![U]:(sorti2(U)=>op2(U,U)!=U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax4)).
% 10.60/10.80 fof(c16,plain,(?[U]:(sorti2(U)&op2(U,U)=U)),inference(fof_nnf,[status(thm)],[ax4])).
% 10.60/10.80 fof(c17,plain,(?[X10]:(sorti2(X10)&op2(X10,X10)=X10)),inference(variable_rename,[status(thm)],[c16])).
% 10.60/10.80 fof(c18,plain,(sorti2(skolem0001)&op2(skolem0001,skolem0001)=skolem0001),inference(skolemize,[status(esa)],[c17])).
% 10.60/10.80 cnf(c19,plain,sorti2(skolem0001),inference(split_conjunct,[status(thm)],[c18])).
% 10.60/10.80 fof(co1,conjecture,(((![U]:(sorti1(U)=>sorti2(h(U))))&(![V]:(sorti2(V)=>sorti1(j(V)))))=>(~((((![W]:(sorti1(W)=>(![X]:(sorti1(X)=>h(op1(W,X))=op2(h(W),h(X))))))&(![Y]:(sorti2(Y)=>(![Z]:(sorti2(Z)=>j(op2(Y,Z))=op1(j(Y),j(Z)))))))&(![X1]:(sorti2(X1)=>h(j(X1))=X1)))&(![X2]:(sorti1(X2)=>j(h(X2))=X2))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1)).
% 10.60/10.80 fof(c6,negated_conjecture,(~(((![U]:(sorti1(U)=>sorti2(h(U))))&(![V]:(sorti2(V)=>sorti1(j(V)))))=>(~((((![W]:(sorti1(W)=>(![X]:(sorti1(X)=>h(op1(W,X))=op2(h(W),h(X))))))&(![Y]:(sorti2(Y)=>(![Z]:(sorti2(Z)=>j(op2(Y,Z))=op1(j(Y),j(Z)))))))&(![X1]:(sorti2(X1)=>h(j(X1))=X1)))&(![X2]:(sorti1(X2)=>j(h(X2))=X2)))))),inference(assume_negation,[status(cth)],[co1])).
% 10.60/10.80 fof(c7,negated_conjecture,(((![U]:(~sorti1(U)|sorti2(h(U))))&(![V]:(~sorti2(V)|sorti1(j(V)))))&((((![W]:(~sorti1(W)|(![X]:(~sorti1(X)|h(op1(W,X))=op2(h(W),h(X))))))&(![Y]:(~sorti2(Y)|(![Z]:(~sorti2(Z)|j(op2(Y,Z))=op1(j(Y),j(Z)))))))&(![X1]:(~sorti2(X1)|h(j(X1))=X1)))&(![X2]:(~sorti1(X2)|j(h(X2))=X2)))),inference(fof_nnf,[status(thm)],[c6])).
% 10.60/10.80 fof(c9,negated_conjecture,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:(((~sorti1(X2)|sorti2(h(X2)))&(~sorti2(X3)|sorti1(j(X3))))&((((~sorti1(X4)|(~sorti1(X5)|h(op1(X4,X5))=op2(h(X4),h(X5))))&(~sorti2(X6)|(~sorti2(X7)|j(op2(X6,X7))=op1(j(X6),j(X7)))))&(~sorti2(X8)|h(j(X8))=X8))&(~sorti1(X9)|j(h(X9))=X9))))))))))),inference(shift_quantors,[status(thm)],[fof(c8,negated_conjecture,(((![X2]:(~sorti1(X2)|sorti2(h(X2))))&(![X3]:(~sorti2(X3)|sorti1(j(X3)))))&((((![X4]:(~sorti1(X4)|(![X5]:(~sorti1(X5)|h(op1(X4,X5))=op2(h(X4),h(X5))))))&(![X6]:(~sorti2(X6)|(![X7]:(~sorti2(X7)|j(op2(X6,X7))=op1(j(X6),j(X7)))))))&(![X8]:(~sorti2(X8)|h(j(X8))=X8)))&(![X9]:(~sorti1(X9)|j(h(X9))=X9)))),inference(variable_rename,[status(thm)],[c7])).])).
% 10.60/10.80 cnf(c11,negated_conjecture,~sorti2(X24)|sorti1(j(X24)),inference(split_conjunct,[status(thm)],[c9])).
% 10.60/10.80 cnf(c35,plain,sorti1(j(skolem0001)),inference(resolution,[status(thm)],[c11, c19])).
% 10.60/10.80 fof(ax3,axiom,(![U]:(sorti1(U)=>op1(U,U)!=U)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax3)).
% 10.60/10.80 fof(c21,plain,(![U]:(~sorti1(U)|op1(U,U)!=U)),inference(fof_nnf,[status(thm)],[ax3])).
% 10.60/10.80 fof(c22,plain,(![X11]:(~sorti1(X11)|op1(X11,X11)!=X11)),inference(variable_rename,[status(thm)],[c21])).
% 10.60/10.80 cnf(c23,plain,~sorti1(X42)|op1(X42,X42)!=X42,inference(split_conjunct,[status(thm)],[c22])).
% 10.60/10.80 cnf(transitivity,axiom,X22!=X21|X21!=X23|X22=X23,theory(equality)).
% 10.60/10.80 cnf(c20,plain,op2(skolem0001,skolem0001)=skolem0001,inference(split_conjunct,[status(thm)],[c18])).
% 10.60/10.80 cnf(c3,axiom,X48!=X49|j(X48)=j(X49),theory(equality)).
% 10.60/10.80 cnf(c78,plain,j(op2(skolem0001,skolem0001))=j(skolem0001),inference(resolution,[status(thm)],[c3, c20])).
% 10.60/10.80 cnf(c277,plain,X157!=j(op2(skolem0001,skolem0001))|X157=j(skolem0001),inference(resolution,[status(thm)],[c78, transitivity])).
% 10.60/10.80 cnf(symmetry,axiom,X18!=X17|X17=X18,theory(equality)).
% 10.60/10.80 cnf(c13,negated_conjecture,~sorti2(X61)|~sorti2(X60)|j(op2(X61,X60))=op1(j(X61),j(X60)),inference(split_conjunct,[status(thm)],[c9])).
% 10.60/10.80 cnf(c108,plain,~sorti2(X118)|j(op2(X118,X118))=op1(j(X118),j(X118)),inference(factor,[status(thm)],[c13])).
% 10.60/10.80 cnf(c1168,plain,j(op2(skolem0001,skolem0001))=op1(j(skolem0001),j(skolem0001)),inference(resolution,[status(thm)],[c108, c19])).
% 10.60/10.80 cnf(c12943,plain,op1(j(skolem0001),j(skolem0001))=j(op2(skolem0001,skolem0001)),inference(resolution,[status(thm)],[c1168, symmetry])).
% 10.60/10.80 cnf(c21369,plain,op1(j(skolem0001),j(skolem0001))=j(skolem0001),inference(resolution,[status(thm)],[c12943, c277])).
% 10.60/10.80 cnf(c21405,plain,~sorti1(j(skolem0001)),inference(resolution,[status(thm)],[c21369, c23])).
% 10.60/10.80 cnf(c21463,plain,$false,inference(resolution,[status(thm)],[c21405, c35])).
% 10.60/10.80 % SZS output end CNFRefutation
% 10.60/10.80
% 10.60/10.80 % Initial clauses : 20
% 10.60/10.80 % Processed clauses : 864
% 10.60/10.80 % Factors computed : 7
% 10.60/10.80 % Resolvents computed: 21425
% 10.60/10.80 % Tautologies deleted: 4
% 10.60/10.80 % Forward subsumed : 579
% 10.60/10.80 % Backward subsumed : 0
% 10.60/10.80 % -------- CPU Time ---------
% 10.60/10.80 % User time : 10.383 s
% 10.60/10.80 % System time : 0.058 s
% 10.60/10.80 % Total time : 10.441 s
%------------------------------------------------------------------------------