%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS097+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n010.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:41 EDT 2024
% Result : Unsatisfiable 0.48s 0.64s
% Output : Refutation 0.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : KRS097+1 : TPTP v8.1.2. Released v3.1.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n010.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.48/0.64 % Version: 1.5
% 0.48/0.64 % SZS status Unsatisfiable
% 0.48/0.64 % SZS output start CNFRefutation
% 0.48/0.64 fof(axiom_6,axiom,(![X]:(~(cd(X)&cc(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_6)).
% 0.48/0.64 fof(c38,plain,(![X]:(~cd(X)|~cc(X))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 0.48/0.64 fof(c39,plain,(![X15]:(~cd(X15)|~cc(X15))),inference(variable_rename,[status(thm)],[c38])).
% 0.48/0.64 cnf(c40,plain,~cd(X108)|~cc(X108),inference(split_conjunct,[status(thm)],[c39])).
% 0.48/0.64 fof(axiom_4,axiom,cUnsatisfiable(i2003_11_14_17_20_21603),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_4)).
% 0.48/0.64 cnf(c44,plain,cUnsatisfiable(i2003_11_14_17_20_21603),inference(split_conjunct,[status(thm)],[axiom_4])).
% 0.48/0.64 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)<=>((((?[Y0]:rr(X,Y0))&(?[Y]:(rr(X,Y)&cd(Y))))&(~(?[Y0]:(?[Y1]:((rr(X,Y0)&rr(X,Y1))&Y0!=Y1)))))&(?[Y]:(rr(X,Y)&cc(Y)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 0.48/0.64 fof(c53,plain,(![X]:((~cUnsatisfiable(X)|((((?[Y0]:rr(X,Y0))&(?[Y]:(rr(X,Y)&cd(Y))))&(![Y0]:(![Y1]:((~rr(X,Y0)|~rr(X,Y1))|Y0=Y1))))&(?[Y]:(rr(X,Y)&cc(Y)))))&(((((![Y0]:~rr(X,Y0))|(![Y]:(~rr(X,Y)|~cd(Y))))|(?[Y0]:(?[Y1]:((rr(X,Y0)&rr(X,Y1))&Y0!=Y1))))|(![Y]:(~rr(X,Y)|~cc(Y))))|cUnsatisfiable(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.48/0.64 fof(c54,plain,((![X]:(~cUnsatisfiable(X)|((((?[Y0]:rr(X,Y0))&(?[Y]:(rr(X,Y)&cd(Y))))&(![Y0]:(![Y1]:((~rr(X,Y0)|~rr(X,Y1))|Y0=Y1))))&(?[Y]:(rr(X,Y)&cc(Y))))))&(![X]:(((((![Y0]:~rr(X,Y0))|(![Y]:(~rr(X,Y)|~cd(Y))))|(?[Y0]:(?[Y1]:((rr(X,Y0)&rr(X,Y1))&Y0!=Y1))))|(![Y]:(~rr(X,Y)|~cc(Y))))|cUnsatisfiable(X)))),inference(shift_quantors,[status(thm)],[c53])).
% 0.48/0.64 fof(c55,plain,((![X19]:(~cUnsatisfiable(X19)|((((?[X20]:rr(X19,X20))&(?[X21]:(rr(X19,X21)&cd(X21))))&(![X22]:(![X23]:((~rr(X19,X22)|~rr(X19,X23))|X22=X23))))&(?[X24]:(rr(X19,X24)&cc(X24))))))&(![X25]:(((((![X26]:~rr(X25,X26))|(![X27]:(~rr(X25,X27)|~cd(X27))))|(?[X28]:(?[X29]:((rr(X25,X28)&rr(X25,X29))&X28!=X29))))|(![X30]:(~rr(X25,X30)|~cc(X30))))|cUnsatisfiable(X25)))),inference(variable_rename,[status(thm)],[c54])).
% 0.48/0.64 fof(c57,plain,(![X19]:(![X22]:(![X23]:(![X25]:(![X26]:(![X27]:(![X30]:((~cUnsatisfiable(X19)|(((rr(X19,skolem0001(X19))&(rr(X19,skolem0002(X19))&cd(skolem0002(X19))))&((~rr(X19,X22)|~rr(X19,X23))|X22=X23))&(rr(X19,skolem0003(X19))&cc(skolem0003(X19)))))&((((~rr(X25,X26)|(~rr(X25,X27)|~cd(X27)))|((rr(X25,skolem0004(X25))&rr(X25,skolem0005(X25)))&skolem0004(X25)!=skolem0005(X25)))|(~rr(X25,X30)|~cc(X30)))|cUnsatisfiable(X25)))))))))),inference(shift_quantors,[status(thm)],[fof(c56,plain,((![X19]:(~cUnsatisfiable(X19)|(((rr(X19,skolem0001(X19))&(rr(X19,skolem0002(X19))&cd(skolem0002(X19))))&(![X22]:(![X23]:((~rr(X19,X22)|~rr(X19,X23))|X22=X23))))&(rr(X19,skolem0003(X19))&cc(skolem0003(X19))))))&(![X25]:(((((![X26]:~rr(X25,X26))|(![X27]:(~rr(X25,X27)|~cd(X27))))|((rr(X25,skolem0004(X25))&rr(X25,skolem0005(X25)))&skolem0004(X25)!=skolem0005(X25)))|(![X30]:(~rr(X25,X30)|~cc(X30))))|cUnsatisfiable(X25)))),inference(skolemize,[status(esa)],[c55])).])).
% 0.48/0.64 fof(c58,plain,(![X19]:(![X22]:(![X23]:(![X25]:(![X26]:(![X27]:(![X30]:(((((~cUnsatisfiable(X19)|rr(X19,skolem0001(X19)))&((~cUnsatisfiable(X19)|rr(X19,skolem0002(X19)))&(~cUnsatisfiable(X19)|cd(skolem0002(X19)))))&(~cUnsatisfiable(X19)|((~rr(X19,X22)|~rr(X19,X23))|X22=X23)))&((~cUnsatisfiable(X19)|rr(X19,skolem0003(X19)))&(~cUnsatisfiable(X19)|cc(skolem0003(X19)))))&((((((~rr(X25,X26)|(~rr(X25,X27)|~cd(X27)))|rr(X25,skolem0004(X25)))|(~rr(X25,X30)|~cc(X30)))|cUnsatisfiable(X25))&((((~rr(X25,X26)|(~rr(X25,X27)|~cd(X27)))|rr(X25,skolem0005(X25)))|(~rr(X25,X30)|~cc(X30)))|cUnsatisfiable(X25)))&((((~rr(X25,X26)|(~rr(X25,X27)|~cd(X27)))|skolem0004(X25)!=skolem0005(X25))|(~rr(X25,X30)|~cc(X30)))|cUnsatisfiable(X25))))))))))),inference(distribute,[status(thm)],[c57])).
% 0.48/0.64 cnf(c64,plain,~cUnsatisfiable(X137)|cc(skolem0003(X137)),inference(split_conjunct,[status(thm)],[c58])).
% 0.48/0.64 cnf(c164,plain,cc(skolem0003(i2003_11_14_17_20_21603)),inference(resolution,[status(thm)],[c64, c44])).
% 0.48/0.64 cnf(c2,axiom,X138!=X139|~cc(X138)|cc(X139),theory(equality)).
% 0.48/0.64 cnf(c63,plain,~cUnsatisfiable(X153)|rr(X153,skolem0003(X153)),inference(split_conjunct,[status(thm)],[c58])).
% 0.48/0.64 cnf(c175,plain,rr(i2003_11_14_17_20_21603,skolem0003(i2003_11_14_17_20_21603)),inference(resolution,[status(thm)],[c63, c44])).
% 0.48/0.64 cnf(c59,plain,~cUnsatisfiable(X148)|rr(X148,skolem0001(X148)),inference(split_conjunct,[status(thm)],[c58])).
% 0.48/0.64 cnf(c172,plain,rr(i2003_11_14_17_20_21603,skolem0001(i2003_11_14_17_20_21603)),inference(resolution,[status(thm)],[c59, c44])).
% 0.48/0.64 cnf(c62,plain,~cUnsatisfiable(X269)|~rr(X269,X270)|~rr(X269,X268)|X270=X268,inference(split_conjunct,[status(thm)],[c58])).
% 0.48/0.64 cnf(c194,plain,~cUnsatisfiable(i2003_11_14_17_20_21603)|~rr(i2003_11_14_17_20_21603,X286)|X286=skolem0001(i2003_11_14_17_20_21603),inference(resolution,[status(thm)],[c62, c172])).
% 0.48/0.64 cnf(c206,plain,~cUnsatisfiable(i2003_11_14_17_20_21603)|skolem0003(i2003_11_14_17_20_21603)=skolem0001(i2003_11_14_17_20_21603),inference(resolution,[status(thm)],[c194, c175])).
% 0.48/0.64 cnf(c208,plain,skolem0003(i2003_11_14_17_20_21603)=skolem0001(i2003_11_14_17_20_21603),inference(resolution,[status(thm)],[c206, c44])).
% 0.48/0.64 cnf(c214,plain,~cc(skolem0003(i2003_11_14_17_20_21603))|cc(skolem0001(i2003_11_14_17_20_21603)),inference(resolution,[status(thm)],[c208, c2])).
% 0.48/0.64 cnf(c236,plain,cc(skolem0001(i2003_11_14_17_20_21603)),inference(resolution,[status(thm)],[c214, c164])).
% 0.48/0.64 cnf(c238,plain,~cd(skolem0001(i2003_11_14_17_20_21603)),inference(resolution,[status(thm)],[c236, c40])).
% 0.48/0.64 cnf(c61,plain,~cUnsatisfiable(X136)|cd(skolem0002(X136)),inference(split_conjunct,[status(thm)],[c58])).
% 0.48/0.64 cnf(c162,plain,cd(skolem0002(i2003_11_14_17_20_21603)),inference(resolution,[status(thm)],[c61, c44])).
% 0.48/0.64 cnf(c3,axiom,X141!=X142|~cd(X141)|cd(X142),theory(equality)).
% 0.48/0.64 cnf(c60,plain,~cUnsatisfiable(X152)|rr(X152,skolem0002(X152)),inference(split_conjunct,[status(thm)],[c58])).
% 0.48/0.64 cnf(c174,plain,rr(i2003_11_14_17_20_21603,skolem0002(i2003_11_14_17_20_21603)),inference(resolution,[status(thm)],[c60, c44])).
% 0.48/0.64 cnf(c207,plain,~cUnsatisfiable(i2003_11_14_17_20_21603)|skolem0002(i2003_11_14_17_20_21603)=skolem0001(i2003_11_14_17_20_21603),inference(resolution,[status(thm)],[c194, c174])).
% 0.48/0.64 cnf(c261,plain,skolem0002(i2003_11_14_17_20_21603)=skolem0001(i2003_11_14_17_20_21603),inference(resolution,[status(thm)],[c207, c44])).
% 0.48/0.64 cnf(c270,plain,~cd(skolem0002(i2003_11_14_17_20_21603))|cd(skolem0001(i2003_11_14_17_20_21603)),inference(resolution,[status(thm)],[c261, c3])).
% 0.48/0.64 cnf(c290,plain,cd(skolem0001(i2003_11_14_17_20_21603)),inference(resolution,[status(thm)],[c270, c162])).
% 0.48/0.64 cnf(c292,plain,$false,inference(resolution,[status(thm)],[c290, c238])).
% 0.48/0.64 % SZS output end CNFRefutation
% 0.48/0.64
% 0.48/0.64 % Initial clauses : 71
% 0.48/0.64 % Processed clauses : 106
% 0.48/0.64 % Factors computed : 8
% 0.48/0.64 % Resolvents computed: 129
% 0.48/0.64 % Tautologies deleted: 10
% 0.48/0.64 % Forward subsumed : 56
% 0.48/0.64 % Backward subsumed : 6
% 0.48/0.64 % -------- CPU Time ---------
% 0.48/0.64 % User time : 0.278 s
% 0.48/0.64 % System time : 0.016 s
% 0.48/0.64 % Total time : 0.294 s
%------------------------------------------------------------------------------