%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN074+1 : TPTP v8.1.2. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n011.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:47:18 EDT 2024
% Result : Theorem 6.75s 6.93s
% Output : Refutation 6.75s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SYN074+1 : TPTP v8.1.2. Released v2.0.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n011.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 20:04:08 EDT 2024
% 0.14/0.35 % CPUTime :
% 6.75/6.93 % Version: 1.5
% 6.75/6.93 % SZS status Theorem
% 6.75/6.93 % SZS output start CNFRefutation
% 6.75/6.93 fof(pel51_1,axiom,(?[Z]:(?[W]:(![X]:(![Y]:(big_f(X,Y)<=>(X=Z&Y=W)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', pel51_1)).
% 6.75/6.93 fof(c12,plain,(?[Z]:(?[W]:(![X]:(![Y]:((~big_f(X,Y)|(X=Z&Y=W))&((X!=Z|Y!=W)|big_f(X,Y))))))),inference(fof_nnf,[status(thm)],[pel51_1])).
% 6.75/6.93 fof(c13,plain,(?[Z]:(?[W]:((![X]:(![Y]:(~big_f(X,Y)|(X=Z&Y=W))))&(![X]:(![Y]:((X!=Z|Y!=W)|big_f(X,Y))))))),inference(shift_quantors,[status(thm)],[c12])).
% 6.75/6.93 fof(c14,plain,(?[X9]:(?[X10]:((![X11]:(![X12]:(~big_f(X11,X12)|(X11=X9&X12=X10))))&(![X13]:(![X14]:((X13!=X9|X14!=X10)|big_f(X13,X14))))))),inference(variable_rename,[status(thm)],[c13])).
% 6.75/6.93 fof(c16,plain,(![X11]:(![X12]:(![X13]:(![X14]:((~big_f(X11,X12)|(X11=skolem0004&X12=skolem0005))&((X13!=skolem0004|X14!=skolem0005)|big_f(X13,X14))))))),inference(shift_quantors,[status(thm)],[fof(c15,plain,((![X11]:(![X12]:(~big_f(X11,X12)|(X11=skolem0004&X12=skolem0005))))&(![X13]:(![X14]:((X13!=skolem0004|X14!=skolem0005)|big_f(X13,X14))))),inference(skolemize,[status(esa)],[c14])).])).
% 6.75/6.93 fof(c17,plain,(![X11]:(![X12]:(![X13]:(![X14]:(((~big_f(X11,X12)|X11=skolem0004)&(~big_f(X11,X12)|X12=skolem0005))&((X13!=skolem0004|X14!=skolem0005)|big_f(X13,X14))))))),inference(distribute,[status(thm)],[c16])).
% 6.75/6.93 cnf(c18,plain,~big_f(X20,X19)|X20=skolem0004,inference(split_conjunct,[status(thm)],[c17])).
% 6.75/6.93 cnf(reflexivity,axiom,X15=X15,theory(equality)).
% 6.75/6.93 fof(pel51,conjecture,(?[Z]:(![X]:((?[W]:(![Y]:(big_f(X,Y)<=>Y=W)))<=>X=Z))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', pel51)).
% 6.75/6.93 fof(c1,negated_conjecture,(~(?[Z]:(![X]:((?[W]:(![Y]:(big_f(X,Y)<=>Y=W)))<=>X=Z)))),inference(assume_negation,[status(cth)],[pel51])).
% 6.75/6.93 fof(c2,negated_conjecture,(![Z]:(?[X]:(((![W]:(?[Y]:((~big_f(X,Y)|Y!=W)&(big_f(X,Y)|Y=W))))|X!=Z)&((?[W]:(![Y]:((~big_f(X,Y)|Y=W)&(Y!=W|big_f(X,Y)))))|X=Z)))),inference(fof_nnf,[status(thm)],[c1])).
% 6.75/6.93 fof(c3,negated_conjecture,(![Z]:(?[X]:(((![W]:(?[Y]:((~big_f(X,Y)|Y!=W)&(big_f(X,Y)|Y=W))))|X!=Z)&((?[W]:((![Y]:(~big_f(X,Y)|Y=W))&(![Y]:(Y!=W|big_f(X,Y)))))|X=Z)))),inference(shift_quantors,[status(thm)],[c2])).
% 6.75/6.93 fof(c4,negated_conjecture,(![X2]:(?[X3]:(((![X4]:(?[X5]:((~big_f(X3,X5)|X5!=X4)&(big_f(X3,X5)|X5=X4))))|X3!=X2)&((?[X6]:((![X7]:(~big_f(X3,X7)|X7=X6))&(![X8]:(X8!=X6|big_f(X3,X8)))))|X3=X2)))),inference(variable_rename,[status(thm)],[c3])).
% 6.75/6.93 fof(c6,negated_conjecture,(![X2]:(![X4]:(![X7]:(![X8]:((((~big_f(skolem0001(X2),skolem0002(X2,X4))|skolem0002(X2,X4)!=X4)&(big_f(skolem0001(X2),skolem0002(X2,X4))|skolem0002(X2,X4)=X4))|skolem0001(X2)!=X2)&(((~big_f(skolem0001(X2),X7)|X7=skolem0003(X2))&(X8!=skolem0003(X2)|big_f(skolem0001(X2),X8)))|skolem0001(X2)=X2)))))),inference(shift_quantors,[status(thm)],[fof(c5,negated_conjecture,(![X2]:(((![X4]:((~big_f(skolem0001(X2),skolem0002(X2,X4))|skolem0002(X2,X4)!=X4)&(big_f(skolem0001(X2),skolem0002(X2,X4))|skolem0002(X2,X4)=X4)))|skolem0001(X2)!=X2)&(((![X7]:(~big_f(skolem0001(X2),X7)|X7=skolem0003(X2)))&(![X8]:(X8!=skolem0003(X2)|big_f(skolem0001(X2),X8))))|skolem0001(X2)=X2))),inference(skolemize,[status(esa)],[c4])).])).
% 6.75/6.93 fof(c7,negated_conjecture,(![X2]:(![X4]:(![X7]:(![X8]:((((~big_f(skolem0001(X2),skolem0002(X2,X4))|skolem0002(X2,X4)!=X4)|skolem0001(X2)!=X2)&((big_f(skolem0001(X2),skolem0002(X2,X4))|skolem0002(X2,X4)=X4)|skolem0001(X2)!=X2))&(((~big_f(skolem0001(X2),X7)|X7=skolem0003(X2))|skolem0001(X2)=X2)&((X8!=skolem0003(X2)|big_f(skolem0001(X2),X8))|skolem0001(X2)=X2))))))),inference(distribute,[status(thm)],[c6])).
% 6.75/6.93 cnf(c11,negated_conjecture,X44!=skolem0003(X43)|big_f(skolem0001(X43),X44)|skolem0001(X43)=X43,inference(split_conjunct,[status(thm)],[c7])).
% 6.75/6.93 cnf(c31,plain,big_f(skolem0001(X45),skolem0003(X45))|skolem0001(X45)=X45,inference(resolution,[status(thm)],[c11, reflexivity])).
% 6.75/6.93 cnf(c34,plain,skolem0001(X47)=X47|skolem0001(X47)=skolem0004,inference(resolution,[status(thm)],[c31, c18])).
% 6.75/6.93 cnf(c49,plain,skolem0001(skolem0004)=skolem0004,inference(factor,[status(thm)],[c34])).
% 6.75/6.93 cnf(c19,plain,~big_f(X22,X21)|X21=skolem0005,inference(split_conjunct,[status(thm)],[c17])).
% 6.75/6.93 cnf(c9,negated_conjecture,big_f(skolem0001(X49),skolem0002(X49,X48))|skolem0002(X49,X48)=X48|skolem0001(X49)!=X49,inference(split_conjunct,[status(thm)],[c7])).
% 6.75/6.93 cnf(c64,plain,big_f(skolem0001(skolem0004),skolem0002(skolem0004,X152))|skolem0002(skolem0004,X152)=X152,inference(resolution,[status(thm)],[c49, c9])).
% 6.75/6.93 cnf(c715,plain,skolem0002(skolem0004,X483)=X483|skolem0002(skolem0004,X483)=skolem0005,inference(resolution,[status(thm)],[c64, c19])).
% 6.75/6.93 cnf(c4945,plain,skolem0002(skolem0004,skolem0005)=skolem0005,inference(factor,[status(thm)],[c715])).
% 6.75/6.93 cnf(c8,negated_conjecture,~big_f(skolem0001(X40),skolem0002(X40,X39))|skolem0002(X40,X39)!=X39|skolem0001(X40)!=X40,inference(split_conjunct,[status(thm)],[c7])).
% 6.75/6.93 cnf(c0,axiom,X32!=X34|X35!=X33|~big_f(X32,X35)|big_f(X34,X33),theory(equality)).
% 6.75/6.93 cnf(c20,plain,X29!=skolem0004|X30!=skolem0005|big_f(X29,X30),inference(split_conjunct,[status(thm)],[c17])).
% 6.75/6.93 cnf(c24,plain,X31!=skolem0004|big_f(X31,skolem0005),inference(resolution,[status(thm)],[c20, reflexivity])).
% 6.75/6.93 cnf(c63,plain,big_f(skolem0001(skolem0004),skolem0005),inference(resolution,[status(thm)],[c49, c24])).
% 6.75/6.93 cnf(c67,plain,skolem0001(skolem0004)!=X163|skolem0005!=X162|big_f(X163,X162),inference(resolution,[status(thm)],[c63, c0])).
% 6.75/6.93 cnf(c757,plain,skolem0005!=X165|big_f(skolem0001(skolem0004),X165),inference(resolution,[status(thm)],[c67, reflexivity])).
% 6.75/6.93 cnf(symmetry,axiom,X16!=X17|X17=X16,theory(equality)).
% 6.75/6.93 cnf(c5006,plain,skolem0005=skolem0002(skolem0004,skolem0005),inference(resolution,[status(thm)],[c4945, symmetry])).
% 6.75/6.93 cnf(c5017,plain,big_f(skolem0001(skolem0004),skolem0002(skolem0004,skolem0005)),inference(resolution,[status(thm)],[c5006, c757])).
% 6.75/6.93 cnf(c5087,plain,skolem0002(skolem0004,skolem0005)!=skolem0005|skolem0001(skolem0004)!=skolem0004,inference(resolution,[status(thm)],[c5017, c8])).
% 6.75/6.93 cnf(c17688,plain,skolem0001(skolem0004)!=skolem0004,inference(resolution,[status(thm)],[c5087, c4945])).
% 6.75/6.93 cnf(c17707,plain,$false,inference(resolution,[status(thm)],[c17688, c49])).
% 6.75/6.93 % SZS output end CNFRefutation
% 6.75/6.93
% 6.75/6.93 % Initial clauses : 11
% 6.75/6.93 % Processed clauses : 347
% 6.75/6.93 % Factors computed : 14
% 6.75/6.93 % Resolvents computed: 17734
% 6.75/6.93 % Tautologies deleted: 2
% 6.75/6.93 % Forward subsumed : 944
% 6.75/6.93 % Backward subsumed : 8
% 6.75/6.93 % -------- CPU Time ---------
% 6.75/6.93 % User time : 6.520 s
% 6.75/6.93 % System time : 0.057 s
% 6.75/6.93 % Total time : 6.577 s
%------------------------------------------------------------------------------