%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRA002+4 : TPTP v8.1.2. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n003.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:22:31 EDT 2024
% Result : Theorem 0.91s 1.11s
% Output : Refutation 0.91s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GRA002+4 : TPTP v8.1.2. Bugfixed v3.2.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n003.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 : Wed May 8 21:35:53 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.91/1.11 % Version: 1.5
% 0.91/1.11 % SZS status Theorem
% 0.91/1.11 % SZS output start CNFRefutation
% 0.91/1.11 fof(maximal_path_length,conjecture,(complete=>(![P]:(![V1]:(![V2]:(shortest_path(V1,V2,P)=>less_or_equal(minus(length_of(P),n1),number_of_in(triangles,graph))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', maximal_path_length)).
% 0.91/1.11 fof(c16,negated_conjecture,(~(complete=>(![P]:(![V1]:(![V2]:(shortest_path(V1,V2,P)=>less_or_equal(minus(length_of(P),n1),number_of_in(triangles,graph)))))))),inference(assume_negation,[status(cth)],[maximal_path_length])).
% 0.91/1.11 fof(c17,negated_conjecture,(complete&(?[P]:(?[V1]:(?[V2]:(shortest_path(V1,V2,P)&~less_or_equal(minus(length_of(P),n1),number_of_in(triangles,graph))))))),inference(fof_nnf,[status(thm)],[c16])).
% 0.91/1.11 fof(c18,negated_conjecture,(complete&(?[P]:((?[V1]:(?[V2]:shortest_path(V1,V2,P)))&~less_or_equal(minus(length_of(P),n1),number_of_in(triangles,graph))))),inference(shift_quantors,[status(thm)],[c17])).
% 0.91/1.11 fof(c19,negated_conjecture,(complete&(?[X2]:((?[X3]:(?[X4]:shortest_path(X3,X4,X2)))&~less_or_equal(minus(length_of(X2),n1),number_of_in(triangles,graph))))),inference(variable_rename,[status(thm)],[c18])).
% 0.91/1.11 fof(c20,negated_conjecture,(complete&(shortest_path(skolem0002,skolem0003,skolem0001)&~less_or_equal(minus(length_of(skolem0001),n1),number_of_in(triangles,graph)))),inference(skolemize,[status(esa)],[c19])).
% 0.91/1.11 cnf(c23,negated_conjecture,~less_or_equal(minus(length_of(skolem0001),n1),number_of_in(triangles,graph)),inference(split_conjunct,[status(thm)],[c20])).
% 0.91/1.11 cnf(symmetry,axiom,X90!=X89|X89=X90,theory(equality)).
% 0.91/1.11 cnf(c22,negated_conjecture,shortest_path(skolem0002,skolem0003,skolem0001),inference(split_conjunct,[status(thm)],[c20])).
% 0.91/1.11 fof(shortest_path_defn,axiom,(![V1]:(![V2]:(![SP]:(shortest_path(V1,V2,SP)<=>((path(V1,V2,SP)&V1!=V2)&(![P]:(path(V1,V2,P)=>less_or_equal(length_of(SP),length_of(P))))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GRA001+0.ax', shortest_path_defn)).
% 0.91/1.11 fof(c66,plain,(![V1]:(![V2]:(![SP]:((~shortest_path(V1,V2,SP)|((path(V1,V2,SP)&V1!=V2)&(![P]:(~path(V1,V2,P)|less_or_equal(length_of(SP),length_of(P))))))&(((~path(V1,V2,SP)|V1=V2)|(?[P]:(path(V1,V2,P)&~less_or_equal(length_of(SP),length_of(P)))))|shortest_path(V1,V2,SP)))))),inference(fof_nnf,[status(thm)],[shortest_path_defn])).
% 0.91/1.11 fof(c67,plain,((![V1]:(![V2]:(![SP]:(~shortest_path(V1,V2,SP)|((path(V1,V2,SP)&V1!=V2)&(![P]:(~path(V1,V2,P)|less_or_equal(length_of(SP),length_of(P)))))))))&(![V1]:(![V2]:(![SP]:(((~path(V1,V2,SP)|V1=V2)|(?[P]:(path(V1,V2,P)&~less_or_equal(length_of(SP),length_of(P)))))|shortest_path(V1,V2,SP)))))),inference(shift_quantors,[status(thm)],[c66])).
% 0.91/1.11 fof(c68,plain,((![X34]:(![X35]:(![X36]:(~shortest_path(X34,X35,X36)|((path(X34,X35,X36)&X34!=X35)&(![X37]:(~path(X34,X35,X37)|less_or_equal(length_of(X36),length_of(X37)))))))))&(![X38]:(![X39]:(![X40]:(((~path(X38,X39,X40)|X38=X39)|(?[X41]:(path(X38,X39,X41)&~less_or_equal(length_of(X40),length_of(X41)))))|shortest_path(X38,X39,X40)))))),inference(variable_rename,[status(thm)],[c67])).
% 0.91/1.11 fof(c70,plain,(![X34]:(![X35]:(![X36]:(![X37]:(![X38]:(![X39]:(![X40]:((~shortest_path(X34,X35,X36)|((path(X34,X35,X36)&X34!=X35)&(~path(X34,X35,X37)|less_or_equal(length_of(X36),length_of(X37)))))&(((~path(X38,X39,X40)|X38=X39)|(path(X38,X39,skolem0006(X38,X39,X40))&~less_or_equal(length_of(X40),length_of(skolem0006(X38,X39,X40)))))|shortest_path(X38,X39,X40)))))))))),inference(shift_quantors,[status(thm)],[fof(c69,plain,((![X34]:(![X35]:(![X36]:(~shortest_path(X34,X35,X36)|((path(X34,X35,X36)&X34!=X35)&(![X37]:(~path(X34,X35,X37)|less_or_equal(length_of(X36),length_of(X37)))))))))&(![X38]:(![X39]:(![X40]:(((~path(X38,X39,X40)|X38=X39)|(path(X38,X39,skolem0006(X38,X39,X40))&~less_or_equal(length_of(X40),length_of(skolem0006(X38,X39,X40)))))|shortest_path(X38,X39,X40)))))),inference(skolemize,[status(esa)],[c68])).])).
% 0.91/1.11 fof(c71,plain,(![X34]:(![X35]:(![X36]:(![X37]:(![X38]:(![X39]:(![X40]:((((~shortest_path(X34,X35,X36)|path(X34,X35,X36))&(~shortest_path(X34,X35,X36)|X34!=X35))&(~shortest_path(X34,X35,X36)|(~path(X34,X35,X37)|less_or_equal(length_of(X36),length_of(X37)))))&((((~path(X38,X39,X40)|X38=X39)|path(X38,X39,skolem0006(X38,X39,X40)))|shortest_path(X38,X39,X40))&(((~path(X38,X39,X40)|X38=X39)|~less_or_equal(length_of(X40),length_of(skolem0006(X38,X39,X40))))|shortest_path(X38,X39,X40))))))))))),inference(distribute,[status(thm)],[c70])).
% 0.91/1.11 cnf(c72,plain,~shortest_path(X154,X155,X153)|path(X154,X155,X153),inference(split_conjunct,[status(thm)],[c71])).
% 0.91/1.11 cnf(c176,plain,path(skolem0002,skolem0003,skolem0001),inference(resolution,[status(thm)],[c72, c22])).
% 0.91/1.11 fof(path_length_sequential_pairs,axiom,(![V1]:(![V2]:(![P]:(path(V1,V2,P)=>number_of_in(sequential_pairs,P)=minus(length_of(P),n1))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', path_length_sequential_pairs)).
% 0.91/1.11 fof(c41,plain,(![V1]:(![V2]:(![P]:(~path(V1,V2,P)|number_of_in(sequential_pairs,P)=minus(length_of(P),n1))))),inference(fof_nnf,[status(thm)],[path_length_sequential_pairs])).
% 0.91/1.11 fof(c42,plain,(![X16]:(![X17]:(![X18]:(~path(X16,X17,X18)|number_of_in(sequential_pairs,X18)=minus(length_of(X18),n1))))),inference(variable_rename,[status(thm)],[c41])).
% 0.91/1.11 cnf(c43,plain,~path(X296,X295,X297)|number_of_in(sequential_pairs,X297)=minus(length_of(X297),n1),inference(split_conjunct,[status(thm)],[c42])).
% 0.91/1.11 cnf(c413,plain,number_of_in(sequential_pairs,skolem0001)=minus(length_of(skolem0001),n1),inference(resolution,[status(thm)],[c43, c176])).
% 0.91/1.11 cnf(c423,plain,minus(length_of(skolem0001),n1)=number_of_in(sequential_pairs,skolem0001),inference(resolution,[status(thm)],[c413, symmetry])).
% 0.91/1.11 cnf(transitivity,axiom,X93!=X92|X92!=X91|X93=X91,theory(equality)).
% 0.91/1.11 cnf(c21,negated_conjecture,complete,inference(split_conjunct,[status(thm)],[c20])).
% 0.91/1.11 fof(triangles_and_sequential_pairs,plain,(complete=>(![P]:(![V1]:(![V2]:(shortest_path(V1,V2,P)=>number_of_in(sequential_pairs,P)=number_of_in(triangles,P)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', triangles_and_sequential_pairs)).
% 0.91/1.11 fof(c24,plain,(~complete|(![P]:(![V1]:(![V2]:(~shortest_path(V1,V2,P)|number_of_in(sequential_pairs,P)=number_of_in(triangles,P)))))),inference(fof_nnf,[status(thm)],[triangles_and_sequential_pairs])).
% 0.91/1.11 fof(c25,plain,(~complete|(![P]:((![V1]:(![V2]:~shortest_path(V1,V2,P)))|number_of_in(sequential_pairs,P)=number_of_in(triangles,P)))),inference(shift_quantors,[status(thm)],[c24])).
% 0.91/1.11 fof(c27,plain,(![X5]:(![X6]:(![X7]:(~complete|(~shortest_path(X6,X7,X5)|number_of_in(sequential_pairs,X5)=number_of_in(triangles,X5)))))),inference(shift_quantors,[status(thm)],[fof(c26,plain,(~complete|(![X5]:((![X6]:(![X7]:~shortest_path(X6,X7,X5)))|number_of_in(sequential_pairs,X5)=number_of_in(triangles,X5)))),inference(variable_rename,[status(thm)],[c25])).])).
% 0.91/1.11 cnf(c28,plain,~complete|~shortest_path(X279,X278,X280)|number_of_in(sequential_pairs,X280)=number_of_in(triangles,X280),inference(split_conjunct,[status(thm)],[c27])).
% 0.91/1.11 cnf(c287,plain,~complete|number_of_in(sequential_pairs,skolem0001)=number_of_in(triangles,skolem0001),inference(resolution,[status(thm)],[c28, c22])).
% 0.91/1.11 cnf(c377,plain,number_of_in(sequential_pairs,skolem0001)=number_of_in(triangles,skolem0001),inference(resolution,[status(thm)],[c287, c21])).
% 0.91/1.11 cnf(c381,plain,X383!=number_of_in(sequential_pairs,skolem0001)|X383=number_of_in(triangles,skolem0001),inference(resolution,[status(thm)],[c377, transitivity])).
% 0.91/1.11 cnf(c766,plain,minus(length_of(skolem0001),n1)=number_of_in(triangles,skolem0001),inference(resolution,[status(thm)],[c381, c423])).
% 0.91/1.11 cnf(c773,plain,number_of_in(triangles,skolem0001)=minus(length_of(skolem0001),n1),inference(resolution,[status(thm)],[c766, symmetry])).
% 0.91/1.11 cnf(reflexivity,axiom,X84=X84,theory(equality)).
% 0.91/1.11 fof(graph_has_them_all,axiom,(![Things]:(![InThese]:less_or_equal(number_of_in(Things,InThese),number_of_in(Things,graph)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', graph_has_them_all)).
% 0.91/1.11 fof(c29,plain,(![X8]:(![X9]:less_or_equal(number_of_in(X8,X9),number_of_in(X8,graph)))),inference(variable_rename,[status(thm)],[graph_has_them_all])).
% 0.91/1.11 cnf(c30,plain,less_or_equal(number_of_in(X157,X156),number_of_in(X157,graph)),inference(split_conjunct,[status(thm)],[c29])).
% 0.91/1.11 cnf(c14,axiom,X251!=X252|X250!=X253|~less_or_equal(X251,X250)|less_or_equal(X252,X253),theory(equality)).
% 0.91/1.11 cnf(c230,plain,number_of_in(X482,X483)!=X484|number_of_in(X482,graph)!=X481|less_or_equal(X484,X481),inference(resolution,[status(thm)],[c14, c30])).
% 0.91/1.11 cnf(c1431,plain,number_of_in(X489,X488)!=X490|less_or_equal(X490,number_of_in(X489,graph)),inference(resolution,[status(thm)],[c230, reflexivity])).
% 0.91/1.11 cnf(c1436,plain,less_or_equal(minus(length_of(skolem0001),n1),number_of_in(triangles,graph)),inference(resolution,[status(thm)],[c1431, c773])).
% 0.91/1.11 cnf(c1474,plain,$false,inference(resolution,[status(thm)],[c1436, c23])).
% 0.91/1.11 % SZS output end CNFRefutation
% 0.91/1.11
% 0.91/1.11 % Initial clauses : 82
% 0.91/1.11 % Processed clauses : 266
% 0.91/1.11 % Factors computed : 17
% 0.91/1.11 % Resolvents computed: 1323
% 0.91/1.11 % Tautologies deleted: 4
% 0.91/1.11 % Forward subsumed : 108
% 0.91/1.11 % Backward subsumed : 6
% 0.91/1.11 % -------- CPU Time ---------
% 0.91/1.11 % User time : 0.734 s
% 0.91/1.11 % System time : 0.016 s
% 0.91/1.11 % Total time : 0.750 s
%------------------------------------------------------------------------------