%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PRO010+4 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n013.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:37:29 EDT 2024
% Result : Theorem 0.91s 1.07s
% Output : Refutation 0.91s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.13 % Problem : PRO010+4 : TPTP v8.1.2. Released v4.0.0.
% 0.13/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n013.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Thu May 9 03:23:08 EDT 2024
% 0.14/0.36 % CPUTime :
% 0.91/1.07 % Version: 1.5
% 0.91/1.07 % SZS status Theorem
% 0.91/1.07 % SZS output start CNFRefutation
% 0.91/1.07 fof(sos_44,axiom,tptp1!=tptp2,file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_44)).
% 0.91/1.07 cnf(c33,plain,tptp1!=tptp2,inference(split_conjunct,[status(thm)],[sos_44])).
% 0.91/1.07 cnf(symmetry,axiom,X133!=X132|X132=X133,theory(equality)).
% 0.91/1.07 fof(sos_08,axiom,(![X28]:(![X29]:(![X30]:((occurrence_of(X28,X29)&occurrence_of(X28,X30))=>X29=X30)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_08)).
% 0.91/1.07 fof(c193,plain,(![X28]:(![X29]:(![X30]:((~occurrence_of(X28,X29)|~occurrence_of(X28,X30))|X29=X30)))),inference(fof_nnf,[status(thm)],[sos_08])).
% 0.91/1.07 fof(c194,plain,(![X100]:(![X101]:(![X102]:((~occurrence_of(X100,X101)|~occurrence_of(X100,X102))|X101=X102)))),inference(variable_rename,[status(thm)],[c193])).
% 0.91/1.07 cnf(c195,plain,~occurrence_of(X289,X291)|~occurrence_of(X289,X290)|X291=X290,inference(split_conjunct,[status(thm)],[c194])).
% 0.91/1.07 fof(goals,conjecture,(![X105]:(occurrence_of(X105,tptp0)=>(?[X106]:(?[X107]:((leaf_occ(X107,X105)&(occurrence_of(X107,tptp1)=>(~(?[X108]:(occurrence_of(X108,tptp2)&min_precedes(X106,X108,tptp0))))))&(occurrence_of(X107,tptp2)=>(~(?[X109]:(occurrence_of(X109,tptp1)&min_precedes(X106,X109,tptp0)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', goals)).
% 0.91/1.07 fof(c17,negated_conjecture,(~(![X105]:(occurrence_of(X105,tptp0)=>(?[X106]:(?[X107]:((leaf_occ(X107,X105)&(occurrence_of(X107,tptp1)=>(~(?[X108]:(occurrence_of(X108,tptp2)&min_precedes(X106,X108,tptp0))))))&(occurrence_of(X107,tptp2)=>(~(?[X109]:(occurrence_of(X109,tptp1)&min_precedes(X106,X109,tptp0))))))))))),inference(assume_negation,[status(cth)],[goals])).
% 0.91/1.07 fof(c18,negated_conjecture,(?[X105]:(occurrence_of(X105,tptp0)&(![X106]:(![X107]:((~leaf_occ(X107,X105)|(occurrence_of(X107,tptp1)&(?[X108]:(occurrence_of(X108,tptp2)&min_precedes(X106,X108,tptp0)))))|(occurrence_of(X107,tptp2)&(?[X109]:(occurrence_of(X109,tptp1)&min_precedes(X106,X109,tptp0))))))))),inference(fof_nnf,[status(thm)],[c17])).
% 0.91/1.07 fof(c19,negated_conjecture,(?[X2]:(occurrence_of(X2,tptp0)&(![X3]:(![X4]:((~leaf_occ(X4,X2)|(occurrence_of(X4,tptp1)&(?[X5]:(occurrence_of(X5,tptp2)&min_precedes(X3,X5,tptp0)))))|(occurrence_of(X4,tptp2)&(?[X6]:(occurrence_of(X6,tptp1)&min_precedes(X3,X6,tptp0))))))))),inference(variable_rename,[status(thm)],[c18])).
% 0.91/1.07 fof(c21,negated_conjecture,(![X3]:(![X4]:(occurrence_of(skolem0001,tptp0)&((~leaf_occ(X4,skolem0001)|(occurrence_of(X4,tptp1)&(occurrence_of(skolem0002(X3,X4),tptp2)&min_precedes(X3,skolem0002(X3,X4),tptp0))))|(occurrence_of(X4,tptp2)&(occurrence_of(skolem0003(X3,X4),tptp1)&min_precedes(X3,skolem0003(X3,X4),tptp0))))))),inference(shift_quantors,[status(thm)],[fof(c20,negated_conjecture,(occurrence_of(skolem0001,tptp0)&(![X3]:(![X4]:((~leaf_occ(X4,skolem0001)|(occurrence_of(X4,tptp1)&(occurrence_of(skolem0002(X3,X4),tptp2)&min_precedes(X3,skolem0002(X3,X4),tptp0))))|(occurrence_of(X4,tptp2)&(occurrence_of(skolem0003(X3,X4),tptp1)&min_precedes(X3,skolem0003(X3,X4),tptp0))))))),inference(skolemize,[status(esa)],[c19])).])).
% 0.91/1.07 fof(c22,negated_conjecture,(![X3]:(![X4]:(occurrence_of(skolem0001,tptp0)&((((~leaf_occ(X4,skolem0001)|occurrence_of(X4,tptp1))|occurrence_of(X4,tptp2))&(((~leaf_occ(X4,skolem0001)|occurrence_of(X4,tptp1))|occurrence_of(skolem0003(X3,X4),tptp1))&((~leaf_occ(X4,skolem0001)|occurrence_of(X4,tptp1))|min_precedes(X3,skolem0003(X3,X4),tptp0))))&((((~leaf_occ(X4,skolem0001)|occurrence_of(skolem0002(X3,X4),tptp2))|occurrence_of(X4,tptp2))&(((~leaf_occ(X4,skolem0001)|occurrence_of(skolem0002(X3,X4),tptp2))|occurrence_of(skolem0003(X3,X4),tptp1))&((~leaf_occ(X4,skolem0001)|occurrence_of(skolem0002(X3,X4),tptp2))|min_precedes(X3,skolem0003(X3,X4),tptp0))))&(((~leaf_occ(X4,skolem0001)|min_precedes(X3,skolem0002(X3,X4),tptp0))|occurrence_of(X4,tptp2))&(((~leaf_occ(X4,skolem0001)|min_precedes(X3,skolem0002(X3,X4),tptp0))|occurrence_of(skolem0003(X3,X4),tptp1))&((~leaf_occ(X4,skolem0001)|min_precedes(X3,skolem0002(X3,X4),tptp0))|min_precedes(X3,skolem0003(X3,X4),tptp0))))))))),inference(distribute,[status(thm)],[c21])).
% 0.91/1.07 cnf(c23,negated_conjecture,occurrence_of(skolem0001,tptp0),inference(split_conjunct,[status(thm)],[c22])).
% 0.91/1.07 fof(sos_32,axiom,(![X101]:(occurrence_of(X101,tptp0)=>(?[X102]:(?[X103]:(?[X104]:((((((occurrence_of(X102,tptp3)&root_occ(X102,X101))&occurrence_of(X103,tptp4))&next_subocc(X102,X103,tptp0))&(occurrence_of(X104,tptp1)|occurrence_of(X104,tptp2)))&next_subocc(X103,X104,tptp0))&leaf_occ(X104,X101))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_32)).
% 0.91/1.07 fof(c46,plain,(![X101]:(~occurrence_of(X101,tptp0)|(?[X102]:(?[X103]:(?[X104]:((((((occurrence_of(X102,tptp3)&root_occ(X102,X101))&occurrence_of(X103,tptp4))&next_subocc(X102,X103,tptp0))&(occurrence_of(X104,tptp1)|occurrence_of(X104,tptp2)))&next_subocc(X103,X104,tptp0))&leaf_occ(X104,X101))))))),inference(fof_nnf,[status(thm)],[sos_32])).
% 0.91/1.07 fof(c47,plain,(![X7]:(~occurrence_of(X7,tptp0)|(?[X8]:(?[X9]:(?[X10]:((((((occurrence_of(X8,tptp3)&root_occ(X8,X7))&occurrence_of(X9,tptp4))&next_subocc(X8,X9,tptp0))&(occurrence_of(X10,tptp1)|occurrence_of(X10,tptp2)))&next_subocc(X9,X10,tptp0))&leaf_occ(X10,X7))))))),inference(variable_rename,[status(thm)],[c46])).
% 0.91/1.07 fof(c48,plain,(![X7]:(~occurrence_of(X7,tptp0)|((((((occurrence_of(skolem0004(X7),tptp3)&root_occ(skolem0004(X7),X7))&occurrence_of(skolem0005(X7),tptp4))&next_subocc(skolem0004(X7),skolem0005(X7),tptp0))&(occurrence_of(skolem0006(X7),tptp1)|occurrence_of(skolem0006(X7),tptp2)))&next_subocc(skolem0005(X7),skolem0006(X7),tptp0))&leaf_occ(skolem0006(X7),X7)))),inference(skolemize,[status(esa)],[c47])).
% 0.91/1.07 fof(c49,plain,(![X7]:(((((((~occurrence_of(X7,tptp0)|occurrence_of(skolem0004(X7),tptp3))&(~occurrence_of(X7,tptp0)|root_occ(skolem0004(X7),X7)))&(~occurrence_of(X7,tptp0)|occurrence_of(skolem0005(X7),tptp4)))&(~occurrence_of(X7,tptp0)|next_subocc(skolem0004(X7),skolem0005(X7),tptp0)))&(~occurrence_of(X7,tptp0)|(occurrence_of(skolem0006(X7),tptp1)|occurrence_of(skolem0006(X7),tptp2))))&(~occurrence_of(X7,tptp0)|next_subocc(skolem0005(X7),skolem0006(X7),tptp0)))&(~occurrence_of(X7,tptp0)|leaf_occ(skolem0006(X7),X7)))),inference(distribute,[status(thm)],[c48])).
% 0.91/1.07 cnf(c56,plain,~occurrence_of(X247,tptp0)|leaf_occ(skolem0006(X247),X247),inference(split_conjunct,[status(thm)],[c49])).
% 0.91/1.07 cnf(c267,plain,leaf_occ(skolem0006(skolem0001),skolem0001),inference(resolution,[status(thm)],[c56, c23])).
% 0.91/1.07 fof(sos_09,axiom,(![X31]:(![X32]:(![X33]:((occurrence_of(X31,X33)&leaf_occ(X32,X31))=>(~(?[X34]:min_precedes(X32,X34,X33))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_09)).
% 0.91/1.07 fof(c189,plain,(![X31]:(![X32]:(![X33]:((~occurrence_of(X31,X33)|~leaf_occ(X32,X31))|(![X34]:~min_precedes(X32,X34,X33)))))),inference(fof_nnf,[status(thm)],[sos_09])).
% 0.91/1.07 fof(c191,plain,(![X96]:(![X97]:(![X98]:(![X99]:((~occurrence_of(X96,X98)|~leaf_occ(X97,X96))|~min_precedes(X97,X99,X98)))))),inference(shift_quantors,[status(thm)],[fof(c190,plain,(![X96]:(![X97]:(![X98]:((~occurrence_of(X96,X98)|~leaf_occ(X97,X96))|(![X99]:~min_precedes(X97,X99,X98)))))),inference(variable_rename,[status(thm)],[c189])).])).
% 0.91/1.07 cnf(c192,plain,~occurrence_of(X367,X366)|~leaf_occ(X368,X367)|~min_precedes(X368,X369,X366),inference(split_conjunct,[status(thm)],[c191])).
% 0.91/1.07 cnf(c26,negated_conjecture,~leaf_occ(X282,skolem0001)|occurrence_of(X282,tptp1)|min_precedes(X281,skolem0003(X281,X282),tptp0),inference(split_conjunct,[status(thm)],[c22])).
% 0.91/1.07 cnf(c294,plain,occurrence_of(skolem0006(skolem0001),tptp1)|min_precedes(X442,skolem0003(X442,skolem0006(skolem0001)),tptp0),inference(resolution,[status(thm)],[c26, c267])).
% 0.91/1.07 cnf(c672,plain,occurrence_of(skolem0006(skolem0001),tptp1)|~occurrence_of(X554,tptp0)|~leaf_occ(X555,X554),inference(resolution,[status(thm)],[c294, c192])).
% 0.91/1.07 cnf(c1194,plain,occurrence_of(skolem0006(skolem0001),tptp1)|~occurrence_of(skolem0001,tptp0),inference(resolution,[status(thm)],[c672, c267])).
% 0.91/1.07 cnf(c1195,plain,occurrence_of(skolem0006(skolem0001),tptp1),inference(resolution,[status(thm)],[c1194, c23])).
% 0.91/1.07 cnf(c1197,plain,~occurrence_of(skolem0006(skolem0001),X556)|X556=tptp1,inference(resolution,[status(thm)],[c1195, c195])).
% 0.91/1.07 cnf(c30,negated_conjecture,~leaf_occ(X300,skolem0001)|min_precedes(X299,skolem0002(X299,X300),tptp0)|occurrence_of(X300,tptp2),inference(split_conjunct,[status(thm)],[c22])).
% 0.91/1.07 cnf(c323,plain,min_precedes(X447,skolem0002(X447,skolem0006(skolem0001)),tptp0)|occurrence_of(skolem0006(skolem0001),tptp2),inference(resolution,[status(thm)],[c30, c267])).
% 0.91/1.07 cnf(c764,plain,occurrence_of(skolem0006(skolem0001),tptp2)|~occurrence_of(X579,tptp0)|~leaf_occ(X580,X579),inference(resolution,[status(thm)],[c323, c192])).
% 0.91/1.07 cnf(c1302,plain,occurrence_of(skolem0006(skolem0001),tptp2)|~occurrence_of(skolem0001,tptp0),inference(resolution,[status(thm)],[c764, c267])).
% 0.91/1.07 cnf(c1303,plain,occurrence_of(skolem0006(skolem0001),tptp2),inference(resolution,[status(thm)],[c1302, c23])).
% 0.91/1.07 cnf(c1304,plain,tptp2=tptp1,inference(resolution,[status(thm)],[c1303, c1197])).
% 0.91/1.07 cnf(c1325,plain,tptp1=tptp2,inference(resolution,[status(thm)],[c1304, symmetry])).
% 0.91/1.07 cnf(c1338,plain,$false,inference(resolution,[status(thm)],[c1325, c33])).
% 0.91/1.07 % SZS output end CNFRefutation
% 0.91/1.07
% 0.91/1.07 % Initial clauses : 109
% 0.91/1.07 % Processed clauses : 423
% 0.91/1.07 % Factors computed : 9
% 0.91/1.07 % Resolvents computed: 1094
% 0.91/1.07 % Tautologies deleted: 10
% 0.91/1.07 % Forward subsumed : 231
% 0.91/1.07 % Backward subsumed : 33
% 0.91/1.07 % -------- CPU Time ---------
% 0.91/1.07 % User time : 0.692 s
% 0.91/1.07 % System time : 0.018 s
% 0.91/1.07 % Total time : 0.710 s
%------------------------------------------------------------------------------