%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS070+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n012.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:28:37 EDT 2024
% Result : Unsatisfiable 0.53s 0.72s
% Output : Refutation 0.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : KRS070+1 : TPTP v8.1.2. Released v3.1.0.
% 0.03/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n012.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 9 00:08:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.53/0.72 % Version: 1.5
% 0.53/0.72 % SZS status Unsatisfiable
% 0.53/0.72 % SZS output start CNFRefutation
% 0.53/0.72 fof(axiom_8,axiom,cUnsatisfiable(i2003_11_14_17_18_32242),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_8)).
% 0.53/0.72 cnf(c41,plain,cUnsatisfiable(i2003_11_14_17_18_32242),inference(split_conjunct,[status(thm)],[axiom_8])).
% 0.53/0.72 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)<=>(((?[Y]:(rrx4(X,Y)&cc2(Y)))&(~(?[Y]:((rrx3(X,Y)&cc2(Y))&cc1(Y)))))&(?[Y]:(rrx3(X,Y)&cc1(Y)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 0.53/0.72 fof(c57,plain,(![X]:((~cUnsatisfiable(X)|(((?[Y]:(rrx4(X,Y)&cc2(Y)))&(![Y]:((~rrx3(X,Y)|~cc2(Y))|~cc1(Y))))&(?[Y]:(rrx3(X,Y)&cc1(Y)))))&((((![Y]:(~rrx4(X,Y)|~cc2(Y)))|(?[Y]:((rrx3(X,Y)&cc2(Y))&cc1(Y))))|(![Y]:(~rrx3(X,Y)|~cc1(Y))))|cUnsatisfiable(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.53/0.72 fof(c58,plain,((![X]:(~cUnsatisfiable(X)|(((?[Y]:(rrx4(X,Y)&cc2(Y)))&(![Y]:((~rrx3(X,Y)|~cc2(Y))|~cc1(Y))))&(?[Y]:(rrx3(X,Y)&cc1(Y))))))&(![X]:((((![Y]:(~rrx4(X,Y)|~cc2(Y)))|(?[Y]:((rrx3(X,Y)&cc2(Y))&cc1(Y))))|(![Y]:(~rrx3(X,Y)|~cc1(Y))))|cUnsatisfiable(X)))),inference(shift_quantors,[status(thm)],[c57])).
% 0.53/0.72 fof(c59,plain,((![X33]:(~cUnsatisfiable(X33)|(((?[X34]:(rrx4(X33,X34)&cc2(X34)))&(![X35]:((~rrx3(X33,X35)|~cc2(X35))|~cc1(X35))))&(?[X36]:(rrx3(X33,X36)&cc1(X36))))))&(![X37]:((((![X38]:(~rrx4(X37,X38)|~cc2(X38)))|(?[X39]:((rrx3(X37,X39)&cc2(X39))&cc1(X39))))|(![X40]:(~rrx3(X37,X40)|~cc1(X40))))|cUnsatisfiable(X37)))),inference(variable_rename,[status(thm)],[c58])).
% 0.53/0.72 fof(c61,plain,(![X33]:(![X35]:(![X37]:(![X38]:(![X40]:((~cUnsatisfiable(X33)|(((rrx4(X33,skolem0001(X33))&cc2(skolem0001(X33)))&((~rrx3(X33,X35)|~cc2(X35))|~cc1(X35)))&(rrx3(X33,skolem0002(X33))&cc1(skolem0002(X33)))))&((((~rrx4(X37,X38)|~cc2(X38))|((rrx3(X37,skolem0003(X37))&cc2(skolem0003(X37)))&cc1(skolem0003(X37))))|(~rrx3(X37,X40)|~cc1(X40)))|cUnsatisfiable(X37)))))))),inference(shift_quantors,[status(thm)],[fof(c60,plain,((![X33]:(~cUnsatisfiable(X33)|(((rrx4(X33,skolem0001(X33))&cc2(skolem0001(X33)))&(![X35]:((~rrx3(X33,X35)|~cc2(X35))|~cc1(X35))))&(rrx3(X33,skolem0002(X33))&cc1(skolem0002(X33))))))&(![X37]:((((![X38]:(~rrx4(X37,X38)|~cc2(X38)))|((rrx3(X37,skolem0003(X37))&cc2(skolem0003(X37)))&cc1(skolem0003(X37))))|(![X40]:(~rrx3(X37,X40)|~cc1(X40))))|cUnsatisfiable(X37)))),inference(skolemize,[status(esa)],[c59])).])).
% 0.53/0.72 fof(c62,plain,(![X33]:(![X35]:(![X37]:(![X38]:(![X40]:(((((~cUnsatisfiable(X33)|rrx4(X33,skolem0001(X33)))&(~cUnsatisfiable(X33)|cc2(skolem0001(X33))))&(~cUnsatisfiable(X33)|((~rrx3(X33,X35)|~cc2(X35))|~cc1(X35))))&((~cUnsatisfiable(X33)|rrx3(X33,skolem0002(X33)))&(~cUnsatisfiable(X33)|cc1(skolem0002(X33)))))&((((((~rrx4(X37,X38)|~cc2(X38))|rrx3(X37,skolem0003(X37)))|(~rrx3(X37,X40)|~cc1(X40)))|cUnsatisfiable(X37))&((((~rrx4(X37,X38)|~cc2(X38))|cc2(skolem0003(X37)))|(~rrx3(X37,X40)|~cc1(X40)))|cUnsatisfiable(X37)))&((((~rrx4(X37,X38)|~cc2(X38))|cc1(skolem0003(X37)))|(~rrx3(X37,X40)|~cc1(X40)))|cUnsatisfiable(X37))))))))),inference(distribute,[status(thm)],[c61])).
% 0.53/0.72 cnf(c64,plain,~cUnsatisfiable(X150)|cc2(skolem0001(X150)),inference(split_conjunct,[status(thm)],[c62])).
% 0.53/0.72 cnf(c170,plain,cc2(skolem0001(i2003_11_14_17_18_32242)),inference(resolution,[status(thm)],[c64, c41])).
% 0.53/0.72 cnf(c2,axiom,X159!=X160|~cc2(X159)|cc2(X160),theory(equality)).
% 0.53/0.72 fof(axiom_16,axiom,(![X]:(![Y]:(rrx4(X,Y)=>rrx(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_16)).
% 0.53/0.72 fof(c17,plain,(![X]:(![Y]:(~rrx4(X,Y)|rrx(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_16])).
% 0.53/0.72 fof(c18,plain,(![X2]:(![X3]:(~rrx4(X2,X3)|rrx(X2,X3)))),inference(variable_rename,[status(thm)],[c17])).
% 0.53/0.72 cnf(c19,plain,~rrx4(X128,X129)|rrx(X128,X129),inference(split_conjunct,[status(thm)],[c18])).
% 0.53/0.72 cnf(c63,plain,~cUnsatisfiable(X158)|rrx4(X158,skolem0001(X158)),inference(split_conjunct,[status(thm)],[c62])).
% 0.53/0.72 cnf(c173,plain,rrx4(i2003_11_14_17_18_32242,skolem0001(i2003_11_14_17_18_32242)),inference(resolution,[status(thm)],[c63, c41])).
% 0.53/0.72 cnf(c175,plain,rrx(i2003_11_14_17_18_32242,skolem0001(i2003_11_14_17_18_32242)),inference(resolution,[status(thm)],[c173, c19])).
% 0.53/0.72 fof(axiom_9,axiom,(![X]:(![Y]:(rrx3(X,Y)=>rrx(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_9)).
% 0.53/0.72 fof(c38,plain,(![X]:(![Y]:(~rrx3(X,Y)|rrx(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_9])).
% 0.53/0.72 fof(c39,plain,(![X16]:(![X17]:(~rrx3(X16,X17)|rrx(X16,X17)))),inference(variable_rename,[status(thm)],[c38])).
% 0.53/0.72 cnf(c40,plain,~rrx3(X149,X148)|rrx(X149,X148),inference(split_conjunct,[status(thm)],[c39])).
% 0.53/0.72 cnf(c66,plain,~cUnsatisfiable(X162)|rrx3(X162,skolem0002(X162)),inference(split_conjunct,[status(thm)],[c62])).
% 0.53/0.72 cnf(c177,plain,rrx3(i2003_11_14_17_18_32242,skolem0002(i2003_11_14_17_18_32242)),inference(resolution,[status(thm)],[c66, c41])).
% 0.53/0.72 cnf(c178,plain,rrx(i2003_11_14_17_18_32242,skolem0002(i2003_11_14_17_18_32242)),inference(resolution,[status(thm)],[c177, c40])).
% 0.53/0.72 fof(axiom_3,axiom,(![X]:(![Y]:(![Z]:((rrx(X,Y)&rrx(X,Z))=>Y=Z)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 0.53/0.72 fof(c54,plain,(![X]:(![Y]:(![Z]:((~rrx(X,Y)|~rrx(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.53/0.72 fof(c55,plain,(![X30]:(![X31]:(![X32]:((~rrx(X30,X31)|~rrx(X30,X32))|X31=X32)))),inference(variable_rename,[status(thm)],[c54])).
% 0.53/0.72 cnf(c56,plain,~rrx(X225,X223)|~rrx(X225,X224)|X223=X224,inference(split_conjunct,[status(thm)],[c55])).
% 0.53/0.72 cnf(c193,plain,~rrx(i2003_11_14_17_18_32242,X310)|X310=skolem0002(i2003_11_14_17_18_32242),inference(resolution,[status(thm)],[c56, c178])).
% 0.53/0.72 cnf(c212,plain,skolem0001(i2003_11_14_17_18_32242)=skolem0002(i2003_11_14_17_18_32242),inference(resolution,[status(thm)],[c193, c175])).
% 0.53/0.72 cnf(c216,plain,~cc2(skolem0001(i2003_11_14_17_18_32242))|cc2(skolem0002(i2003_11_14_17_18_32242)),inference(resolution,[status(thm)],[c212, c2])).
% 0.53/0.72 cnf(c286,plain,cc2(skolem0002(i2003_11_14_17_18_32242)),inference(resolution,[status(thm)],[c216, c170])).
% 0.53/0.72 cnf(c67,plain,~cUnsatisfiable(X151)|cc1(skolem0002(X151)),inference(split_conjunct,[status(thm)],[c62])).
% 0.53/0.72 cnf(c171,plain,cc1(skolem0002(i2003_11_14_17_18_32242)),inference(resolution,[status(thm)],[c67, c41])).
% 0.53/0.72 cnf(c65,plain,~cUnsatisfiable(X317)|~rrx3(X317,X316)|~cc2(X316)|~cc1(X316),inference(split_conjunct,[status(thm)],[c62])).
% 0.53/0.72 cnf(c229,plain,~cUnsatisfiable(i2003_11_14_17_18_32242)|~cc2(skolem0002(i2003_11_14_17_18_32242))|~cc1(skolem0002(i2003_11_14_17_18_32242)),inference(resolution,[status(thm)],[c65, c177])).
% 0.53/0.72 cnf(c302,plain,~cUnsatisfiable(i2003_11_14_17_18_32242)|~cc2(skolem0002(i2003_11_14_17_18_32242)),inference(resolution,[status(thm)],[c229, c171])).
% 0.53/0.72 cnf(c303,plain,~cUnsatisfiable(i2003_11_14_17_18_32242),inference(resolution,[status(thm)],[c302, c286])).
% 0.53/0.72 cnf(c304,plain,$false,inference(resolution,[status(thm)],[c303, c41])).
% 0.53/0.72 % SZS output end CNFRefutation
% 0.53/0.72
% 0.53/0.72 % Initial clauses : 73
% 0.53/0.72 % Processed clauses : 118
% 0.53/0.72 % Factors computed : 6
% 0.53/0.72 % Resolvents computed: 134
% 0.53/0.72 % Tautologies deleted: 8
% 0.53/0.72 % Forward subsumed : 52
% 0.53/0.72 % Backward subsumed : 4
% 0.53/0.72 % -------- CPU Time ---------
% 0.53/0.72 % User time : 0.341 s
% 0.53/0.72 % System time : 0.020 s
% 0.53/0.72 % Total time : 0.361 s
%------------------------------------------------------------------------------