%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : ALG202+1 : TPTP v8.1.2. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n009.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 1.76s 1.96s
% Output : Refutation 1.76s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : ALG202+1 : TPTP v8.1.2. Released v2.7.0.
% 0.10/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n009.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Thu May 9 00:34:38 EDT 2024
% 0.14/0.34 % CPUTime :
% 1.76/1.96 % Version: 1.5
% 1.76/1.96 % SZS status Theorem
% 1.76/1.96 % SZS output start CNFRefutation
% 1.76/1.96 fof(ax4,axiom,(~(![U]:(sorti2(U)=>op2(U,U)=U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax4)).
% 1.76/1.96 fof(c16,plain,(?[U]:(sorti2(U)&op2(U,U)!=U)),inference(fof_nnf,[status(thm)],[ax4])).
% 1.76/1.96 fof(c17,plain,(?[X10]:(sorti2(X10)&op2(X10,X10)!=X10)),inference(variable_rename,[status(thm)],[c16])).
% 1.76/1.96 fof(c18,plain,(sorti2(skolem0001)&op2(skolem0001,skolem0001)!=skolem0001),inference(skolemize,[status(esa)],[c17])).
% 1.76/1.96 cnf(c20,plain,op2(skolem0001,skolem0001)!=skolem0001,inference(split_conjunct,[status(thm)],[c18])).
% 1.76/1.96 cnf(symmetry,axiom,X18!=X17|X17=X18,theory(equality)).
% 1.76/1.96 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)).
% 1.76/1.96 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])).
% 1.76/1.96 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])).
% 1.76/1.96 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])).])).
% 1.76/1.96 cnf(c14,negated_conjecture,~sorti2(X43)|h(j(X43))=X43,inference(split_conjunct,[status(thm)],[c9])).
% 1.76/1.96 cnf(c19,plain,sorti2(skolem0001),inference(split_conjunct,[status(thm)],[c18])).
% 1.76/1.96 fof(ax2,axiom,(![U]:(sorti2(U)=>(![V]:(sorti2(V)=>sorti2(op2(U,V)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax2)).
% 1.76/1.96 fof(c24,plain,(![U]:(~sorti2(U)|(![V]:(~sorti2(V)|sorti2(op2(U,V)))))),inference(fof_nnf,[status(thm)],[ax2])).
% 1.76/1.96 fof(c26,plain,(![X12]:(![X13]:(~sorti2(X12)|(~sorti2(X13)|sorti2(op2(X12,X13)))))),inference(shift_quantors,[status(thm)],[fof(c25,plain,(![X12]:(~sorti2(X12)|(![X13]:(~sorti2(X13)|sorti2(op2(X12,X13)))))),inference(variable_rename,[status(thm)],[c24])).])).
% 1.76/1.96 cnf(c27,plain,~sorti2(X53)|~sorti2(X54)|sorti2(op2(X53,X54)),inference(split_conjunct,[status(thm)],[c26])).
% 1.76/1.96 cnf(c72,plain,~sorti2(X55)|sorti2(op2(X55,X55)),inference(factor,[status(thm)],[c27])).
% 1.76/1.96 cnf(c76,plain,sorti2(op2(skolem0001,skolem0001)),inference(resolution,[status(thm)],[c72, c19])).
% 1.76/1.96 cnf(c80,plain,h(j(op2(skolem0001,skolem0001)))=op2(skolem0001,skolem0001),inference(resolution,[status(thm)],[c76, c14])).
% 1.76/1.96 cnf(c626,plain,op2(skolem0001,skolem0001)=h(j(op2(skolem0001,skolem0001))),inference(resolution,[status(thm)],[c80, symmetry])).
% 1.76/1.96 cnf(transitivity,axiom,X22!=X21|X21!=X23|X22=X23,theory(equality)).
% 1.76/1.96 cnf(c48,plain,h(j(skolem0001))=skolem0001,inference(resolution,[status(thm)],[c14, c19])).
% 1.76/1.96 cnf(c52,plain,X79!=h(j(skolem0001))|X79=skolem0001,inference(resolution,[status(thm)],[c48, transitivity])).
% 1.76/1.96 cnf(c2,axiom,X44!=X45|h(X44)=h(X45),theory(equality)).
% 1.76/1.96 cnf(c11,negated_conjecture,~sorti2(X24)|sorti1(j(X24)),inference(split_conjunct,[status(thm)],[c9])).
% 1.76/1.96 cnf(c35,plain,sorti1(j(skolem0001)),inference(resolution,[status(thm)],[c11, c19])).
% 1.76/1.96 fof(ax3,axiom,(![U]:(sorti1(U)=>op1(U,U)=U)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax3)).
% 1.76/1.96 fof(c21,plain,(![U]:(~sorti1(U)|op1(U,U)=U)),inference(fof_nnf,[status(thm)],[ax3])).
% 1.76/1.96 fof(c22,plain,(![X11]:(~sorti1(X11)|op1(X11,X11)=X11)),inference(variable_rename,[status(thm)],[c21])).
% 1.76/1.96 cnf(c23,plain,~sorti1(X42)|op1(X42,X42)=X42,inference(split_conjunct,[status(thm)],[c22])).
% 1.76/1.96 cnf(c44,plain,op1(j(skolem0001),j(skolem0001))=j(skolem0001),inference(resolution,[status(thm)],[c23, c35])).
% 1.76/1.96 cnf(c156,plain,X153!=op1(j(skolem0001),j(skolem0001))|X153=j(skolem0001),inference(resolution,[status(thm)],[c44, transitivity])).
% 1.76/1.96 cnf(c13,negated_conjecture,~sorti2(X57)|~sorti2(X58)|j(op2(X57,X58))=op1(j(X57),j(X58)),inference(split_conjunct,[status(thm)],[c9])).
% 1.76/1.96 cnf(c84,plain,~sorti2(X101)|j(op2(X101,X101))=op1(j(X101),j(X101)),inference(factor,[status(thm)],[c13])).
% 1.76/1.96 cnf(c704,plain,j(op2(skolem0001,skolem0001))=op1(j(skolem0001),j(skolem0001)),inference(resolution,[status(thm)],[c84, c19])).
% 1.76/1.96 cnf(c4635,plain,j(op2(skolem0001,skolem0001))=j(skolem0001),inference(resolution,[status(thm)],[c704, c156])).
% 1.76/1.96 cnf(c4755,plain,h(j(op2(skolem0001,skolem0001)))=h(j(skolem0001)),inference(resolution,[status(thm)],[c4635, c2])).
% 1.76/1.96 cnf(c4900,plain,h(j(op2(skolem0001,skolem0001)))=skolem0001,inference(resolution,[status(thm)],[c4755, c52])).
% 1.76/1.96 cnf(c4913,plain,X223!=h(j(op2(skolem0001,skolem0001)))|X223=skolem0001,inference(resolution,[status(thm)],[c4900, transitivity])).
% 1.76/1.96 cnf(c5358,plain,op2(skolem0001,skolem0001)=skolem0001,inference(resolution,[status(thm)],[c4913, c626])).
% 1.76/1.96 cnf(c5494,plain,$false,inference(resolution,[status(thm)],[c5358, c20])).
% 1.76/1.96 % SZS output end CNFRefutation
% 1.76/1.96
% 1.76/1.96 % Initial clauses : 20
% 1.76/1.96 % Processed clauses : 351
% 1.76/1.96 % Factors computed : 7
% 1.76/1.96 % Resolvents computed: 5456
% 1.76/1.96 % Tautologies deleted: 4
% 1.76/1.96 % Forward subsumed : 128
% 1.76/1.96 % Backward subsumed : 0
% 1.76/1.96 % -------- CPU Time ---------
% 1.76/1.96 % User time : 1.592 s
% 1.76/1.96 % System time : 0.025 s
% 1.76/1.96 % Total time : 1.617 s
%------------------------------------------------------------------------------