%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS101+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n007.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:42 EDT 2024
% Result : Unsatisfiable 0.20s 0.59s
% Output : Refutation 0.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : KRS101+1 : TPTP v8.1.2. Released v3.1.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n007.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 9 00:18:38 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.20/0.59 % Version: 1.5
% 0.20/0.59 % SZS status Unsatisfiable
% 0.20/0.59 % SZS output start CNFRefutation
% 0.20/0.59 fof(axiom_4,axiom,cUnsatisfiable(i2003_11_14_17_20_36582),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_4)).
% 0.20/0.59 cnf(c9,plain,cUnsatisfiable(i2003_11_14_17_20_36582),inference(split_conjunct,[status(thm)],[axiom_4])).
% 0.20/0.59 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)<=>(((![Y]:(rr(X,Y)=>cd(Y)))&(![Y]:(rr(X,Y)=>((~(?[Z0]:(?[Z1]:((rs(Y,Z0)&rs(Y,Z1))&Z0!=Z1))))|cc(Y)))))&(?[Y]:(rr(X,Y)&(~(![Z0]:(![Z1]:((rs(Y,Z0)&rs(Y,Z1))=>Z0=Z1))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 0.20/0.59 fof(c14,plain,(![X]:((~cUnsatisfiable(X)|(((![Y]:(~rr(X,Y)|cd(Y)))&(![Y]:(~rr(X,Y)|((![Z0]:(![Z1]:((~rs(Y,Z0)|~rs(Y,Z1))|Z0=Z1)))|cc(Y)))))&(?[Y]:(rr(X,Y)&(?[Z0]:(?[Z1]:((rs(Y,Z0)&rs(Y,Z1))&Z0!=Z1)))))))&((((?[Y]:(rr(X,Y)&~cd(Y)))|(?[Y]:(rr(X,Y)&((?[Z0]:(?[Z1]:((rs(Y,Z0)&rs(Y,Z1))&Z0!=Z1)))&~cc(Y)))))|(![Y]:(~rr(X,Y)|(![Z0]:(![Z1]:((~rs(Y,Z0)|~rs(Y,Z1))|Z0=Z1))))))|cUnsatisfiable(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.20/0.59 fof(c15,plain,((![X]:(~cUnsatisfiable(X)|(((![Y]:(~rr(X,Y)|cd(Y)))&(![Y]:(~rr(X,Y)|((![Z0]:(![Z1]:((~rs(Y,Z0)|~rs(Y,Z1))|Z0=Z1)))|cc(Y)))))&(?[Y]:(rr(X,Y)&(?[Z0]:(?[Z1]:((rs(Y,Z0)&rs(Y,Z1))&Z0!=Z1))))))))&(![X]:((((?[Y]:(rr(X,Y)&~cd(Y)))|(?[Y]:(rr(X,Y)&((?[Z0]:(?[Z1]:((rs(Y,Z0)&rs(Y,Z1))&Z0!=Z1)))&~cc(Y)))))|(![Y]:(~rr(X,Y)|(![Z0]:(![Z1]:((~rs(Y,Z0)|~rs(Y,Z1))|Z0=Z1))))))|cUnsatisfiable(X)))),inference(shift_quantors,[status(thm)],[c14])).
% 0.20/0.59 fof(c16,plain,((![X3]:(~cUnsatisfiable(X3)|(((![X4]:(~rr(X3,X4)|cd(X4)))&(![X5]:(~rr(X3,X5)|((![X6]:(![X7]:((~rs(X5,X6)|~rs(X5,X7))|X6=X7)))|cc(X5)))))&(?[X8]:(rr(X3,X8)&(?[X9]:(?[X10]:((rs(X8,X9)&rs(X8,X10))&X9!=X10))))))))&(![X11]:((((?[X12]:(rr(X11,X12)&~cd(X12)))|(?[X13]:(rr(X11,X13)&((?[X14]:(?[X15]:((rs(X13,X14)&rs(X13,X15))&X14!=X15)))&~cc(X13)))))|(![X16]:(~rr(X11,X16)|(![X17]:(![X18]:((~rs(X16,X17)|~rs(X16,X18))|X17=X18))))))|cUnsatisfiable(X11)))),inference(variable_rename,[status(thm)],[c15])).
% 0.20/0.59 fof(c18,plain,(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(![X11]:(![X16]:(![X17]:(![X18]:((~cUnsatisfiable(X3)|(((~rr(X3,X4)|cd(X4))&(~rr(X3,X5)|(((~rs(X5,X6)|~rs(X5,X7))|X6=X7)|cc(X5))))&(rr(X3,skolem0001(X3))&((rs(skolem0001(X3),skolem0002(X3))&rs(skolem0001(X3),skolem0003(X3)))&skolem0002(X3)!=skolem0003(X3)))))&((((rr(X11,skolem0004(X11))&~cd(skolem0004(X11)))|(rr(X11,skolem0005(X11))&(((rs(skolem0005(X11),skolem0006(X11))&rs(skolem0005(X11),skolem0007(X11)))&skolem0006(X11)!=skolem0007(X11))&~cc(skolem0005(X11)))))|(~rr(X11,X16)|((~rs(X16,X17)|~rs(X16,X18))|X17=X18)))|cUnsatisfiable(X11)))))))))))),inference(shift_quantors,[status(thm)],[fof(c17,plain,((![X3]:(~cUnsatisfiable(X3)|(((![X4]:(~rr(X3,X4)|cd(X4)))&(![X5]:(~rr(X3,X5)|((![X6]:(![X7]:((~rs(X5,X6)|~rs(X5,X7))|X6=X7)))|cc(X5)))))&(rr(X3,skolem0001(X3))&((rs(skolem0001(X3),skolem0002(X3))&rs(skolem0001(X3),skolem0003(X3)))&skolem0002(X3)!=skolem0003(X3))))))&(![X11]:((((rr(X11,skolem0004(X11))&~cd(skolem0004(X11)))|(rr(X11,skolem0005(X11))&(((rs(skolem0005(X11),skolem0006(X11))&rs(skolem0005(X11),skolem0007(X11)))&skolem0006(X11)!=skolem0007(X11))&~cc(skolem0005(X11)))))|(![X16]:(~rr(X11,X16)|(![X17]:(![X18]:((~rs(X16,X17)|~rs(X16,X18))|X17=X18))))))|cUnsatisfiable(X11)))),inference(skolemize,[status(esa)],[c16])).])).
% 0.20/0.59 fof(c19,plain,(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(![X11]:(![X16]:(![X17]:(![X18]:((((~cUnsatisfiable(X3)|(~rr(X3,X4)|cd(X4)))&(~cUnsatisfiable(X3)|(~rr(X3,X5)|(((~rs(X5,X6)|~rs(X5,X7))|X6=X7)|cc(X5)))))&((~cUnsatisfiable(X3)|rr(X3,skolem0001(X3)))&(((~cUnsatisfiable(X3)|rs(skolem0001(X3),skolem0002(X3)))&(~cUnsatisfiable(X3)|rs(skolem0001(X3),skolem0003(X3))))&(~cUnsatisfiable(X3)|skolem0002(X3)!=skolem0003(X3)))))&(((((rr(X11,skolem0004(X11))|rr(X11,skolem0005(X11)))|(~rr(X11,X16)|((~rs(X16,X17)|~rs(X16,X18))|X17=X18)))|cUnsatisfiable(X11))&((((((rr(X11,skolem0004(X11))|rs(skolem0005(X11),skolem0006(X11)))|(~rr(X11,X16)|((~rs(X16,X17)|~rs(X16,X18))|X17=X18)))|cUnsatisfiable(X11))&(((rr(X11,skolem0004(X11))|rs(skolem0005(X11),skolem0007(X11)))|(~rr(X11,X16)|((~rs(X16,X17)|~rs(X16,X18))|X17=X18)))|cUnsatisfiable(X11)))&(((rr(X11,skolem0004(X11))|skolem0006(X11)!=skolem0007(X11))|(~rr(X11,X16)|((~rs(X16,X17)|~rs(X16,X18))|X17=X18)))|cUnsatisfiable(X11)))&(((rr(X11,skolem0004(X11))|~cc(skolem0005(X11)))|(~rr(X11,X16)|((~rs(X16,X17)|~rs(X16,X18))|X17=X18)))|cUnsatisfiable(X11))))&((((~cd(skolem0004(X11))|rr(X11,skolem0005(X11)))|(~rr(X11,X16)|((~rs(X16,X17)|~rs(X16,X18))|X17=X18)))|cUnsatisfiable(X11))&((((((~cd(skolem0004(X11))|rs(skolem0005(X11),skolem0006(X11)))|(~rr(X11,X16)|((~rs(X16,X17)|~rs(X16,X18))|X17=X18)))|cUnsatisfiable(X11))&(((~cd(skolem0004(X11))|rs(skolem0005(X11),skolem0007(X11)))|(~rr(X11,X16)|((~rs(X16,X17)|~rs(X16,X18))|X17=X18)))|cUnsatisfiable(X11)))&(((~cd(skolem0004(X11))|skolem0006(X11)!=skolem0007(X11))|(~rr(X11,X16)|((~rs(X16,X17)|~rs(X16,X18))|X17=X18)))|cUnsatisfiable(X11)))&(((~cd(skolem0004(X11))|~cc(skolem0005(X11)))|(~rr(X11,X16)|((~rs(X16,X17)|~rs(X16,X18))|X17=X18)))|cUnsatisfiable(X11))))))))))))))),inference(distribute,[status(thm)],[c18])).
% 0.20/0.59 cnf(c25,plain,~cUnsatisfiable(X115)|skolem0002(X115)!=skolem0003(X115),inference(split_conjunct,[status(thm)],[c19])).
% 0.20/0.59 cnf(symmetry,axiom,X54!=X53|X53=X54,theory(equality)).
% 0.20/0.59 fof(axiom_3,axiom,(![X]:(cc(X)=>(~cd(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 0.20/0.59 fof(c10,plain,(![X]:(cc(X)=>~cd(X))),inference(fof_simplification,[status(thm)],[axiom_3])).
% 0.20/0.59 fof(c11,plain,(![X]:(~cc(X)|~cd(X))),inference(fof_nnf,[status(thm)],[c10])).
% 0.20/0.59 fof(c12,plain,(![X2]:(~cc(X2)|~cd(X2))),inference(variable_rename,[status(thm)],[c11])).
% 0.20/0.59 cnf(c13,plain,~cc(X52)|~cd(X52),inference(split_conjunct,[status(thm)],[c12])).
% 0.20/0.59 cnf(c22,plain,~cUnsatisfiable(X59)|rr(X59,skolem0001(X59)),inference(split_conjunct,[status(thm)],[c19])).
% 0.20/0.59 cnf(c84,plain,rr(i2003_11_14_17_20_36582,skolem0001(i2003_11_14_17_20_36582)),inference(resolution,[status(thm)],[c22, c9])).
% 0.20/0.59 cnf(c20,plain,~cUnsatisfiable(X89)|~rr(X89,X90)|cd(X90),inference(split_conjunct,[status(thm)],[c19])).
% 0.20/0.59 cnf(c93,plain,~cUnsatisfiable(i2003_11_14_17_20_36582)|cd(skolem0001(i2003_11_14_17_20_36582)),inference(resolution,[status(thm)],[c20, c84])).
% 0.20/0.59 cnf(c95,plain,cd(skolem0001(i2003_11_14_17_20_36582)),inference(resolution,[status(thm)],[c93, c9])).
% 0.20/0.59 cnf(c96,plain,~cc(skolem0001(i2003_11_14_17_20_36582)),inference(resolution,[status(thm)],[c95, c13])).
% 0.20/0.59 cnf(c24,plain,~cUnsatisfiable(X114)|rs(skolem0001(X114),skolem0003(X114)),inference(split_conjunct,[status(thm)],[c19])).
% 0.20/0.59 cnf(c100,plain,rs(skolem0001(i2003_11_14_17_20_36582),skolem0003(i2003_11_14_17_20_36582)),inference(resolution,[status(thm)],[c24, c9])).
% 0.20/0.59 cnf(c21,plain,~cUnsatisfiable(X106)|~rr(X106,X108)|~rs(X108,X105)|~rs(X108,X107)|X105=X107|cc(X108),inference(split_conjunct,[status(thm)],[c19])).
% 0.20/0.59 cnf(c23,plain,~cUnsatisfiable(X113)|rs(skolem0001(X113),skolem0002(X113)),inference(split_conjunct,[status(thm)],[c19])).
% 0.20/0.59 cnf(c97,plain,rs(skolem0001(i2003_11_14_17_20_36582),skolem0002(i2003_11_14_17_20_36582)),inference(resolution,[status(thm)],[c23, c9])).
% 0.20/0.59 cnf(c98,plain,~cUnsatisfiable(X192)|~rr(X192,skolem0001(i2003_11_14_17_20_36582))|~rs(skolem0001(i2003_11_14_17_20_36582),X193)|X193=skolem0002(i2003_11_14_17_20_36582)|cc(skolem0001(i2003_11_14_17_20_36582)),inference(resolution,[status(thm)],[c97, c21])).
% 0.20/0.59 cnf(c137,plain,~cUnsatisfiable(X199)|~rr(X199,skolem0001(i2003_11_14_17_20_36582))|skolem0003(i2003_11_14_17_20_36582)=skolem0002(i2003_11_14_17_20_36582)|cc(skolem0001(i2003_11_14_17_20_36582)),inference(resolution,[status(thm)],[c98, c100])).
% 0.20/0.59 cnf(c141,plain,~cUnsatisfiable(i2003_11_14_17_20_36582)|skolem0003(i2003_11_14_17_20_36582)=skolem0002(i2003_11_14_17_20_36582)|cc(skolem0001(i2003_11_14_17_20_36582)),inference(resolution,[status(thm)],[c137, c84])).
% 0.20/0.59 cnf(c142,plain,skolem0003(i2003_11_14_17_20_36582)=skolem0002(i2003_11_14_17_20_36582)|cc(skolem0001(i2003_11_14_17_20_36582)),inference(resolution,[status(thm)],[c141, c9])).
% 0.20/0.59 cnf(c152,plain,skolem0003(i2003_11_14_17_20_36582)=skolem0002(i2003_11_14_17_20_36582),inference(resolution,[status(thm)],[c142, c96])).
% 0.20/0.59 cnf(c160,plain,skolem0002(i2003_11_14_17_20_36582)=skolem0003(i2003_11_14_17_20_36582),inference(resolution,[status(thm)],[c152, symmetry])).
% 0.20/0.59 cnf(c169,plain,~cUnsatisfiable(i2003_11_14_17_20_36582),inference(resolution,[status(thm)],[c160, c25])).
% 0.20/0.59 cnf(c175,plain,$false,inference(resolution,[status(thm)],[c169, c9])).
% 0.20/0.59 % SZS output end CNFRefutation
% 0.20/0.59
% 0.20/0.59 % Initial clauses : 45
% 0.20/0.59 % Processed clauses : 57
% 0.20/0.59 % Factors computed : 10
% 0.20/0.59 % Resolvents computed: 84
% 0.20/0.59 % Tautologies deleted: 8
% 0.20/0.59 % Forward subsumed : 28
% 0.20/0.59 % Backward subsumed : 4
% 0.20/0.59 % -------- CPU Time ---------
% 0.20/0.59 % User time : 0.231 s
% 0.20/0.59 % System time : 0.019 s
% 0.20/0.59 % Total time : 0.250 s
%------------------------------------------------------------------------------