%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PRO011+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n006.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.92s 1.07s
% Output : Refutation 0.92s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : PRO011+3 : TPTP v8.1.2. Released v4.0.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n006.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 : Thu May 9 03:24:23 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.92/1.07 % Version: 1.5
% 0.92/1.07 % SZS status Theorem
% 0.92/1.07 % SZS output start CNFRefutation
% 0.92/1.07 fof(sos_51,axiom,(~atomic(tptp0)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_51)).
% 0.92/1.07 fof(c50,plain,~atomic(tptp0),inference(fof_simplification,[status(thm)],[sos_51])).
% 0.92/1.07 cnf(c51,plain,~atomic(tptp0),inference(split_conjunct,[status(thm)],[c50])).
% 0.92/1.07 fof(goals,conjecture,(![X165]:(occurrence_of(X165,tptp0)=>(?[X166]:(?[X167]:((leaf_occ(X167,X165)&(occurrence_of(X167,tptp1)=>(~(?[X168]:((occurrence_of(X168,tptp2)&subactivity_occurrence(X168,X165))&min_precedes(X166,X168,tptp0))))))&(occurrence_of(X167,tptp2)=>(~(?[X169]:((occurrence_of(X169,tptp1)&subactivity_occurrence(X169,X165))&min_precedes(X166,X169,tptp0)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', goals)).
% 0.92/1.07 fof(c17,negated_conjecture,(~(![X165]:(occurrence_of(X165,tptp0)=>(?[X166]:(?[X167]:((leaf_occ(X167,X165)&(occurrence_of(X167,tptp1)=>(~(?[X168]:((occurrence_of(X168,tptp2)&subactivity_occurrence(X168,X165))&min_precedes(X166,X168,tptp0))))))&(occurrence_of(X167,tptp2)=>(~(?[X169]:((occurrence_of(X169,tptp1)&subactivity_occurrence(X169,X165))&min_precedes(X166,X169,tptp0))))))))))),inference(assume_negation,[status(cth)],[goals])).
% 0.92/1.07 fof(c18,negated_conjecture,(?[X165]:(occurrence_of(X165,tptp0)&(![X166]:(![X167]:((~leaf_occ(X167,X165)|(occurrence_of(X167,tptp1)&(?[X168]:((occurrence_of(X168,tptp2)&subactivity_occurrence(X168,X165))&min_precedes(X166,X168,tptp0)))))|(occurrence_of(X167,tptp2)&(?[X169]:((occurrence_of(X169,tptp1)&subactivity_occurrence(X169,X165))&min_precedes(X166,X169,tptp0))))))))),inference(fof_nnf,[status(thm)],[c17])).
% 0.92/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)&subactivity_occurrence(X5,X2))&min_precedes(X3,X5,tptp0)))))|(occurrence_of(X4,tptp2)&(?[X6]:((occurrence_of(X6,tptp1)&subactivity_occurrence(X6,X2))&min_precedes(X3,X6,tptp0))))))))),inference(variable_rename,[status(thm)],[c18])).
% 0.92/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)&subactivity_occurrence(skolem0002(X3,X4),skolem0001))&min_precedes(X3,skolem0002(X3,X4),tptp0))))|(occurrence_of(X4,tptp2)&((occurrence_of(skolem0003(X3,X4),tptp1)&subactivity_occurrence(skolem0003(X3,X4),skolem0001))&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)&subactivity_occurrence(skolem0002(X3,X4),skolem0001))&min_precedes(X3,skolem0002(X3,X4),tptp0))))|(occurrence_of(X4,tptp2)&((occurrence_of(skolem0003(X3,X4),tptp1)&subactivity_occurrence(skolem0003(X3,X4),skolem0001))&min_precedes(X3,skolem0003(X3,X4),tptp0))))))),inference(skolemize,[status(esa)],[c19])).])).
% 0.92/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))|subactivity_occurrence(skolem0003(X3,X4),skolem0001)))&((~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))|subactivity_occurrence(skolem0003(X3,X4),skolem0001)))&((~leaf_occ(X4,skolem0001)|occurrence_of(skolem0002(X3,X4),tptp2))|min_precedes(X3,skolem0003(X3,X4),tptp0))))&(((~leaf_occ(X4,skolem0001)|subactivity_occurrence(skolem0002(X3,X4),skolem0001))|occurrence_of(X4,tptp2))&((((~leaf_occ(X4,skolem0001)|subactivity_occurrence(skolem0002(X3,X4),skolem0001))|occurrence_of(skolem0003(X3,X4),tptp1))&((~leaf_occ(X4,skolem0001)|subactivity_occurrence(skolem0002(X3,X4),skolem0001))|subactivity_occurrence(skolem0003(X3,X4),skolem0001)))&((~leaf_occ(X4,skolem0001)|subactivity_occurrence(skolem0002(X3,X4),skolem0001))|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))|subactivity_occurrence(skolem0003(X3,X4),skolem0001)))&((~leaf_occ(X4,skolem0001)|min_precedes(X3,skolem0002(X3,X4),tptp0))|min_precedes(X3,skolem0003(X3,X4),tptp0))))))))),inference(distribute,[status(thm)],[c21])).
% 0.92/1.07 cnf(c23,negated_conjecture,occurrence_of(skolem0001,tptp0),inference(split_conjunct,[status(thm)],[c22])).
% 0.92/1.07 fof(sos_07,axiom,(![X16]:(![X17]:(occurrence_of(X16,X17)=>(arboreal(X16)<=>atomic(X17))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_07)).
% 0.92/1.07 fof(c289,plain,(![X16]:(![X17]:(~occurrence_of(X16,X17)|((~arboreal(X16)|atomic(X17))&(~atomic(X17)|arboreal(X16)))))),inference(fof_nnf,[status(thm)],[sos_07])).
% 0.92/1.07 fof(c290,plain,(![X173]:(![X174]:(~occurrence_of(X173,X174)|((~arboreal(X173)|atomic(X174))&(~atomic(X174)|arboreal(X173)))))),inference(variable_rename,[status(thm)],[c289])).
% 0.92/1.07 fof(c291,plain,(![X173]:(![X174]:((~occurrence_of(X173,X174)|(~arboreal(X173)|atomic(X174)))&(~occurrence_of(X173,X174)|(~atomic(X174)|arboreal(X173)))))),inference(distribute,[status(thm)],[c290])).
% 0.92/1.07 cnf(c292,plain,~occurrence_of(X282,X281)|~arboreal(X282)|atomic(X281),inference(split_conjunct,[status(thm)],[c291])).
% 0.92/1.07 cnf(c342,plain,~arboreal(skolem0001)|atomic(tptp0),inference(resolution,[status(thm)],[c292, c23])).
% 0.92/1.07 fof(sos_61,axiom,tptp1!=tptp2,file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_61)).
% 0.92/1.07 cnf(c40,plain,tptp1!=tptp2,inference(split_conjunct,[status(thm)],[sos_61])).
% 0.92/1.07 cnf(symmetry,axiom,X192!=X193|X193=X192,theory(equality)).
% 0.92/1.07 fof(sos_02,axiom,(![X4]:(![X5]:(![X6]:((occurrence_of(X4,X5)&occurrence_of(X4,X6))=>X5=X6)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_02)).
% 0.92/1.07 fof(c307,plain,(![X4]:(![X5]:(![X6]:((~occurrence_of(X4,X5)|~occurrence_of(X4,X6))|X5=X6)))),inference(fof_nnf,[status(thm)],[sos_02])).
% 0.92/1.07 fof(c308,plain,(![X184]:(![X185]:(![X186]:((~occurrence_of(X184,X185)|~occurrence_of(X184,X186))|X185=X186)))),inference(variable_rename,[status(thm)],[c307])).
% 0.92/1.07 cnf(c309,plain,~occurrence_of(X360,X359)|~occurrence_of(X360,X358)|X359=X358,inference(split_conjunct,[status(thm)],[c308])).
% 0.92/1.07 fof(sos_46,axiom,(![X148]:(![X149]:(![X150]:(min_precedes(X148,X149,X150)=>arboreal(X148))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_46)).
% 0.92/1.07 fof(c72,plain,(![X148]:(![X149]:(![X150]:(~min_precedes(X148,X149,X150)|arboreal(X148))))),inference(fof_nnf,[status(thm)],[sos_46])).
% 0.92/1.07 fof(c73,plain,(![X148]:((![X149]:(![X150]:~min_precedes(X148,X149,X150)))|arboreal(X148))),inference(shift_quantors,[status(thm)],[c72])).
% 0.92/1.07 fof(c75,plain,(![X21]:(![X22]:(![X23]:(~min_precedes(X21,X22,X23)|arboreal(X21))))),inference(shift_quantors,[status(thm)],[fof(c74,plain,(![X21]:((![X22]:(![X23]:~min_precedes(X21,X22,X23)))|arboreal(X21))),inference(variable_rename,[status(thm)],[c73])).])).
% 0.92/1.07 cnf(c76,plain,~min_precedes(X223,X224,X222)|arboreal(X223),inference(split_conjunct,[status(thm)],[c75])).
% 0.92/1.07 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/sandbox2/benchmark/theBenchmark.p', sos_49)).
% 0.92/1.07 fof(c53,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.92/1.07 fof(c54,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)],[c53])).
% 0.92/1.07 fof(c55,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)],[c54])).
% 0.92/1.07 fof(c56,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)],[c55])).
% 0.92/1.07 cnf(c63,plain,~occurrence_of(X300,tptp0)|leaf_occ(skolem0006(X300),X300),inference(split_conjunct,[status(thm)],[c56])).
% 0.92/1.07 cnf(c353,plain,leaf_occ(skolem0006(skolem0001),skolem0001),inference(resolution,[status(thm)],[c63, c23])).
% 0.92/1.07 cnf(c27,negated_conjecture,~leaf_occ(X369,skolem0001)|occurrence_of(X369,tptp1)|min_precedes(X368,skolem0003(X368,X369),tptp0),inference(split_conjunct,[status(thm)],[c22])).
% 0.92/1.07 cnf(c417,plain,occurrence_of(skolem0006(skolem0001),tptp1)|min_precedes(X615,skolem0003(X615,skolem0006(skolem0001)),tptp0),inference(resolution,[status(thm)],[c27, c353])).
% 0.92/1.07 cnf(c968,plain,occurrence_of(skolem0006(skolem0001),tptp1)|arboreal(X616),inference(resolution,[status(thm)],[c417, c76])).
% 0.92/1.07 cnf(c1007,plain,occurrence_of(skolem0006(skolem0001),tptp1)|atomic(tptp0),inference(resolution,[status(thm)],[c968, c342])).
% 0.92/1.07 cnf(c1037,plain,occurrence_of(skolem0006(skolem0001),tptp1),inference(resolution,[status(thm)],[c1007, c51])).
% 0.92/1.07 cnf(c1039,plain,~occurrence_of(skolem0006(skolem0001),X626)|X626=tptp1,inference(resolution,[status(thm)],[c1037, c309])).
% 0.92/1.07 cnf(c36,negated_conjecture,~leaf_occ(X394,skolem0001)|min_precedes(X393,skolem0002(X393,X394),tptp0)|occurrence_of(X394,tptp2),inference(split_conjunct,[status(thm)],[c22])).
% 0.92/1.07 cnf(c516,plain,min_precedes(X674,skolem0002(X674,skolem0006(skolem0001)),tptp0)|occurrence_of(skolem0006(skolem0001),tptp2),inference(resolution,[status(thm)],[c36, c353])).
% 0.92/1.07 cnf(c1312,plain,occurrence_of(skolem0006(skolem0001),tptp2)|arboreal(X675),inference(resolution,[status(thm)],[c516, c76])).
% 0.92/1.07 cnf(c1351,plain,arboreal(X678)|tptp2=tptp1,inference(resolution,[status(thm)],[c1312, c1039])).
% 0.92/1.07 cnf(c1390,plain,arboreal(X681)|tptp1=tptp2,inference(resolution,[status(thm)],[c1351, symmetry])).
% 0.92/1.07 cnf(c1474,plain,arboreal(X682),inference(resolution,[status(thm)],[c1390, c40])).
% 0.92/1.07 cnf(c1480,plain,atomic(tptp0),inference(resolution,[status(thm)],[c1474, c342])).
% 0.92/1.07 cnf(c1481,plain,$false,inference(resolution,[status(thm)],[c1480, c51])).
% 0.92/1.07 % SZS output end CNFRefutation
% 0.92/1.07
% 0.92/1.07 % Initial clauses : 138
% 0.92/1.07 % Processed clauses : 401
% 0.92/1.07 % Factors computed : 20
% 0.92/1.07 % Resolvents computed: 1141
% 0.92/1.07 % Tautologies deleted: 9
% 0.92/1.07 % Forward subsumed : 199
% 0.92/1.07 % Backward subsumed : 55
% 0.92/1.07 % -------- CPU Time ---------
% 0.92/1.07 % User time : 0.702 s
% 0.92/1.07 % System time : 0.015 s
% 0.92/1.07 % Total time : 0.717 s
%------------------------------------------------------------------------------