%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PRO010+3 : TPTP v8.1.2. Released v4.0.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:37:29 EDT 2024
% Result : Theorem 0.90s 1.06s
% Output : Refutation 0.90s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : PRO010+3 : TPTP v8.1.2. Released v4.0.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n012.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 9 03:26:08 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.90/1.06 % Version: 1.5
% 0.90/1.06 % SZS status Theorem
% 0.90/1.06 % SZS output start CNFRefutation
% 0.90/1.06 fof(sos_51,axiom,(~atomic(tptp0)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_51)).
% 0.90/1.06 fof(c43,plain,~atomic(tptp0),inference(fof_simplification,[status(thm)],[sos_51])).
% 0.90/1.06 cnf(c44,plain,~atomic(tptp0),inference(split_conjunct,[status(thm)],[c43])).
% 0.90/1.06 fof(goals,conjecture,(![X165]:(occurrence_of(X165,tptp0)=>(?[X166]:(?[X167]:((leaf_occ(X167,X165)&(occurrence_of(X167,tptp1)=>(~(?[X168]:(occurrence_of(X168,tptp2)&min_precedes(X166,X168,tptp0))))))&(occurrence_of(X167,tptp2)=>(~(?[X169]:(occurrence_of(X169,tptp1)&min_precedes(X166,X169,tptp0)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', goals)).
% 0.90/1.06 fof(c17,negated_conjecture,(~(![X165]:(occurrence_of(X165,tptp0)=>(?[X166]:(?[X167]:((leaf_occ(X167,X165)&(occurrence_of(X167,tptp1)=>(~(?[X168]:(occurrence_of(X168,tptp2)&min_precedes(X166,X168,tptp0))))))&(occurrence_of(X167,tptp2)=>(~(?[X169]:(occurrence_of(X169,tptp1)&min_precedes(X166,X169,tptp0))))))))))),inference(assume_negation,[status(cth)],[goals])).
% 0.90/1.06 fof(c18,negated_conjecture,(?[X165]:(occurrence_of(X165,tptp0)&(![X166]:(![X167]:((~leaf_occ(X167,X165)|(occurrence_of(X167,tptp1)&(?[X168]:(occurrence_of(X168,tptp2)&min_precedes(X166,X168,tptp0)))))|(occurrence_of(X167,tptp2)&(?[X169]:(occurrence_of(X169,tptp1)&min_precedes(X166,X169,tptp0))))))))),inference(fof_nnf,[status(thm)],[c17])).
% 0.90/1.06 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.90/1.06 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.90/1.06 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.90/1.06 cnf(c23,negated_conjecture,occurrence_of(skolem0001,tptp0),inference(split_conjunct,[status(thm)],[c22])).
% 0.90/1.06 fof(sos_07,axiom,(![X16]:(![X17]:(occurrence_of(X16,X17)=>(arboreal(X16)<=>atomic(X17))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_07)).
% 0.90/1.06 fof(c282,plain,(![X16]:(![X17]:(~occurrence_of(X16,X17)|((~arboreal(X16)|atomic(X17))&(~atomic(X17)|arboreal(X16)))))),inference(fof_nnf,[status(thm)],[sos_07])).
% 0.90/1.06 fof(c283,plain,(![X173]:(![X174]:(~occurrence_of(X173,X174)|((~arboreal(X173)|atomic(X174))&(~atomic(X174)|arboreal(X173)))))),inference(variable_rename,[status(thm)],[c282])).
% 0.90/1.06 fof(c284,plain,(![X173]:(![X174]:((~occurrence_of(X173,X174)|(~arboreal(X173)|atomic(X174)))&(~occurrence_of(X173,X174)|(~atomic(X174)|arboreal(X173)))))),inference(distribute,[status(thm)],[c283])).
% 0.90/1.06 cnf(c285,plain,~occurrence_of(X281,X282)|~arboreal(X281)|atomic(X282),inference(split_conjunct,[status(thm)],[c284])).
% 0.90/1.06 cnf(c335,plain,~arboreal(skolem0001)|atomic(tptp0),inference(resolution,[status(thm)],[c285, c23])).
% 0.90/1.06 fof(sos_61,axiom,tptp1!=tptp2,file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_61)).
% 0.90/1.06 cnf(c33,plain,tptp1!=tptp2,inference(split_conjunct,[status(thm)],[sos_61])).
% 0.90/1.06 cnf(symmetry,axiom,X193!=X192|X192=X193,theory(equality)).
% 0.90/1.06 fof(sos_02,axiom,(![X4]:(![X5]:(![X6]:((occurrence_of(X4,X5)&occurrence_of(X4,X6))=>X5=X6)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_02)).
% 0.90/1.06 fof(c300,plain,(![X4]:(![X5]:(![X6]:((~occurrence_of(X4,X5)|~occurrence_of(X4,X6))|X5=X6)))),inference(fof_nnf,[status(thm)],[sos_02])).
% 0.90/1.06 fof(c301,plain,(![X184]:(![X185]:(![X186]:((~occurrence_of(X184,X185)|~occurrence_of(X184,X186))|X185=X186)))),inference(variable_rename,[status(thm)],[c300])).
% 0.90/1.06 cnf(c302,plain,~occurrence_of(X359,X360)|~occurrence_of(X359,X358)|X360=X358,inference(split_conjunct,[status(thm)],[c301])).
% 0.90/1.06 fof(sos_46,axiom,(![X148]:(![X149]:(![X150]:(min_precedes(X148,X149,X150)=>arboreal(X148))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_46)).
% 0.90/1.06 fof(c65,plain,(![X148]:(![X149]:(![X150]:(~min_precedes(X148,X149,X150)|arboreal(X148))))),inference(fof_nnf,[status(thm)],[sos_46])).
% 0.90/1.06 fof(c66,plain,(![X148]:((![X149]:(![X150]:~min_precedes(X148,X149,X150)))|arboreal(X148))),inference(shift_quantors,[status(thm)],[c65])).
% 0.90/1.06 fof(c68,plain,(![X21]:(![X22]:(![X23]:(~min_precedes(X21,X22,X23)|arboreal(X21))))),inference(shift_quantors,[status(thm)],[fof(c67,plain,(![X21]:((![X22]:(![X23]:~min_precedes(X21,X22,X23)))|arboreal(X21))),inference(variable_rename,[status(thm)],[c66])).])).
% 0.90/1.06 cnf(c69,plain,~min_precedes(X224,X222,X223)|arboreal(X224),inference(split_conjunct,[status(thm)],[c68])).
% 0.90/1.06 fof(sos_49,axiom,(![X161]:(occurrence_of(X161,tptp0)=>(?[X162]:(?[X163]:(?[X164]:((((((occurrence_of(X162,tptp3)&root_occ(X162,X161))&occurrence_of(X163,tptp4))&next_subocc(X162,X163,tptp0))&(occurrence_of(X164,tptp1)|occurrence_of(X164,tptp2)))&next_subocc(X163,X164,tptp0))&leaf_occ(X164,X161))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_49)).
% 0.90/1.06 fof(c46,plain,(![X161]:(~occurrence_of(X161,tptp0)|(?[X162]:(?[X163]:(?[X164]:((((((occurrence_of(X162,tptp3)&root_occ(X162,X161))&occurrence_of(X163,tptp4))&next_subocc(X162,X163,tptp0))&(occurrence_of(X164,tptp1)|occurrence_of(X164,tptp2)))&next_subocc(X163,X164,tptp0))&leaf_occ(X164,X161))))))),inference(fof_nnf,[status(thm)],[sos_49])).
% 0.90/1.06 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.90/1.06 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.90/1.06 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.90/1.06 cnf(c56,plain,~occurrence_of(X300,tptp0)|leaf_occ(skolem0006(X300),X300),inference(split_conjunct,[status(thm)],[c49])).
% 0.90/1.06 cnf(c346,plain,leaf_occ(skolem0006(skolem0001),skolem0001),inference(resolution,[status(thm)],[c56, c23])).
% 0.90/1.06 cnf(c26,negated_conjecture,~leaf_occ(X366,skolem0001)|occurrence_of(X366,tptp1)|min_precedes(X367,skolem0003(X367,X366),tptp0),inference(split_conjunct,[status(thm)],[c22])).
% 0.90/1.06 cnf(c409,plain,occurrence_of(skolem0006(skolem0001),tptp1)|min_precedes(X597,skolem0003(X597,skolem0006(skolem0001)),tptp0),inference(resolution,[status(thm)],[c26, c346])).
% 0.90/1.06 cnf(c888,plain,occurrence_of(skolem0006(skolem0001),tptp1)|arboreal(X598),inference(resolution,[status(thm)],[c409, c69])).
% 0.90/1.06 cnf(c921,plain,occurrence_of(skolem0006(skolem0001),tptp1)|atomic(tptp0),inference(resolution,[status(thm)],[c888, c335])).
% 0.90/1.06 cnf(c996,plain,occurrence_of(skolem0006(skolem0001),tptp1),inference(resolution,[status(thm)],[c921, c44])).
% 0.90/1.06 cnf(c1001,plain,~occurrence_of(skolem0006(skolem0001),X613)|X613=tptp1,inference(resolution,[status(thm)],[c996, c302])).
% 0.90/1.06 cnf(c30,negated_conjecture,~leaf_occ(X374,skolem0001)|min_precedes(X375,skolem0002(X375,X374),tptp0)|occurrence_of(X374,tptp2),inference(split_conjunct,[status(thm)],[c22])).
% 0.90/1.06 cnf(c433,plain,min_precedes(X617,skolem0002(X617,skolem0006(skolem0001)),tptp0)|occurrence_of(skolem0006(skolem0001),tptp2),inference(resolution,[status(thm)],[c30, c346])).
% 0.90/1.06 cnf(c1097,plain,occurrence_of(skolem0006(skolem0001),tptp2)|arboreal(X618),inference(resolution,[status(thm)],[c433, c69])).
% 0.90/1.06 cnf(c1124,plain,arboreal(X620)|tptp2=tptp1,inference(resolution,[status(thm)],[c1097, c1001])).
% 0.90/1.06 cnf(c1171,plain,arboreal(X622)|tptp1=tptp2,inference(resolution,[status(thm)],[c1124, symmetry])).
% 0.90/1.06 cnf(c1196,plain,arboreal(X624),inference(resolution,[status(thm)],[c1171, c33])).
% 0.90/1.06 cnf(c1205,plain,atomic(tptp0),inference(resolution,[status(thm)],[c1196, c335])).
% 0.90/1.06 cnf(c1206,plain,$false,inference(resolution,[status(thm)],[c1205, c44])).
% 0.90/1.06 % SZS output end CNFRefutation
% 0.90/1.06
% 0.90/1.06 % Initial clauses : 131
% 0.90/1.06 % Processed clauses : 352
% 0.90/1.06 % Factors computed : 18
% 0.90/1.06 % Resolvents computed: 875
% 0.90/1.06 % Tautologies deleted: 9
% 0.90/1.06 % Forward subsumed : 145
% 0.90/1.06 % Backward subsumed : 53
% 0.90/1.06 % -------- CPU Time ---------
% 0.90/1.06 % User time : 0.687 s
% 0.90/1.06 % System time : 0.020 s
% 0.90/1.06 % Total time : 0.707 s
%------------------------------------------------------------------------------