%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRA005+1 : TPTP v8.1.2. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n014.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:32 EDT 2024
% Result : Theorem 3.18s 3.39s
% Output : Refutation 3.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : GRA005+1 : TPTP v8.1.2. Bugfixed v3.2.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.35 % Computer : n014.cluster.edu
% 0.15/0.35 % Model : x86_64 x86_64
% 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.35 % Memory : 8042.1875MB
% 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.35 % CPULimit : 300
% 0.15/0.35 % WCLimit : 300
% 0.15/0.35 % DateTime : Wed May 8 21:35:23 EDT 2024
% 0.15/0.35 % CPUTime :
% 3.18/3.39 % Version: 1.5
% 3.18/3.39 % SZS status Theorem
% 3.18/3.39 % SZS output start CNFRefutation
% 3.18/3.39 fof(no_short_cut_edge,conjecture,(![V1]:(![V2]:(![E1]:(![E2]:(![P]:((shortest_path(V1,V2,P)&precedes(E1,E2,P))=>(~(?[E3]:((edge(E3)&tail_of(E3)=tail_of(E1))&head_of(E3)=head_of(E2)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', no_short_cut_edge)).
% 3.18/3.39 fof(c16,negated_conjecture,(~(![V1]:(![V2]:(![E1]:(![E2]:(![P]:((shortest_path(V1,V2,P)&precedes(E1,E2,P))=>(~(?[E3]:((edge(E3)&tail_of(E3)=tail_of(E1))&head_of(E3)=head_of(E2))))))))))),inference(assume_negation,[status(cth)],[no_short_cut_edge])).
% 3.18/3.39 fof(c17,negated_conjecture,(?[V1]:(?[V2]:(?[E1]:(?[E2]:(?[P]:((shortest_path(V1,V2,P)&precedes(E1,E2,P))&(?[E3]:((edge(E3)&tail_of(E3)=tail_of(E1))&head_of(E3)=head_of(E2))))))))),inference(fof_nnf,[status(thm)],[c16])).
% 3.18/3.39 fof(c18,negated_conjecture,(?[V1]:(?[V2]:(?[E1]:(?[E2]:((?[P]:(shortest_path(V1,V2,P)&precedes(E1,E2,P)))&(?[E3]:((edge(E3)&tail_of(E3)=tail_of(E1))&head_of(E3)=head_of(E2)))))))),inference(shift_quantors,[status(thm)],[c17])).
% 3.18/3.39 fof(c19,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:((?[X6]:(shortest_path(X2,X3,X6)&precedes(X4,X5,X6)))&(?[X7]:((edge(X7)&tail_of(X7)=tail_of(X4))&head_of(X7)=head_of(X5)))))))),inference(variable_rename,[status(thm)],[c18])).
% 3.18/3.39 fof(c20,negated_conjecture,((shortest_path(skolem0001,skolem0002,skolem0005)&precedes(skolem0003,skolem0004,skolem0005))&((edge(skolem0006)&tail_of(skolem0006)=tail_of(skolem0003))&head_of(skolem0006)=head_of(skolem0004))),inference(skolemize,[status(esa)],[c19])).
% 3.18/3.39 cnf(c21,negated_conjecture,shortest_path(skolem0001,skolem0002,skolem0005),inference(split_conjunct,[status(thm)],[c20])).
% 3.18/3.39 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/sandbox/benchmark/Axioms/GRA001+0.ax', shortest_path_defn)).
% 3.18/3.39 fof(c63,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])).
% 3.18/3.39 fof(c64,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)],[c63])).
% 3.18/3.39 fof(c65,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)],[c64])).
% 3.18/3.39 fof(c67,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,skolem0009(X38,X39,X40))&~less_or_equal(length_of(X40),length_of(skolem0009(X38,X39,X40)))))|shortest_path(X38,X39,X40)))))))))),inference(shift_quantors,[status(thm)],[fof(c66,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,skolem0009(X38,X39,X40))&~less_or_equal(length_of(X40),length_of(skolem0009(X38,X39,X40)))))|shortest_path(X38,X39,X40)))))),inference(skolemize,[status(esa)],[c65])).])).
% 3.18/3.39 fof(c68,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,skolem0009(X38,X39,X40)))|shortest_path(X38,X39,X40))&(((~path(X38,X39,X40)|X38=X39)|~less_or_equal(length_of(X40),length_of(skolem0009(X38,X39,X40))))|shortest_path(X38,X39,X40))))))))))),inference(distribute,[status(thm)],[c67])).
% 3.18/3.39 cnf(c69,plain,~shortest_path(X159,X157,X158)|path(X159,X157,X158),inference(split_conjunct,[status(thm)],[c68])).
% 3.18/3.39 cnf(c199,plain,path(skolem0001,skolem0002,skolem0005),inference(resolution,[status(thm)],[c69, c21])).
% 3.18/3.39 fof(path_properties,axiom,(![V1]:(![V2]:(![P]:(path(V1,V2,P)=>((vertex(V1)&vertex(V2))&(?[E]:((edge(E)&V1=tail_of(E))&((V2=head_of(E)&P=path_cons(E,empty))<~>(?[TP]:(path(head_of(E),V2,TP)&P=path_cons(E,TP))))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GRA001+0.ax', path_properties)).
% 3.18/3.39 fof(c117,plain,(![V1]:(![V2]:(![P]:(path(V1,V2,P)=>((vertex(V1)&vertex(V2))&(?[E]:((edge(E)&V1=tail_of(E))&(~((V2=head_of(E)&P=path_cons(E,empty))<=>(?[TP]:(path(head_of(E),V2,TP)&P=path_cons(E,TP)))))))))))),inference(fof_simplification,[status(thm)],[path_properties])).
% 3.18/3.39 fof(c118,plain,(![V1]:(![V2]:(![P]:(~path(V1,V2,P)|((vertex(V1)&vertex(V2))&(?[E]:((edge(E)&V1=tail_of(E))&(((V2!=head_of(E)|P!=path_cons(E,empty))|(![TP]:(~path(head_of(E),V2,TP)|P!=path_cons(E,TP))))&((V2=head_of(E)&P=path_cons(E,empty))|(?[TP]:(path(head_of(E),V2,TP)&P=path_cons(E,TP)))))))))))),inference(fof_nnf,[status(thm)],[c117])).
% 3.18/3.39 fof(c119,plain,(![X68]:(![X69]:(![X70]:(~path(X68,X69,X70)|((vertex(X68)&vertex(X69))&(?[X71]:((edge(X71)&X68=tail_of(X71))&(((X69!=head_of(X71)|X70!=path_cons(X71,empty))|(![X72]:(~path(head_of(X71),X69,X72)|X70!=path_cons(X71,X72))))&((X69=head_of(X71)&X70=path_cons(X71,empty))|(?[X73]:(path(head_of(X71),X69,X73)&X70=path_cons(X71,X73)))))))))))),inference(variable_rename,[status(thm)],[c118])).
% 3.18/3.39 fof(c121,plain,(![X68]:(![X69]:(![X70]:(![X72]:(~path(X68,X69,X70)|((vertex(X68)&vertex(X69))&((edge(skolem0012(X68,X69,X70))&X68=tail_of(skolem0012(X68,X69,X70)))&(((X69!=head_of(skolem0012(X68,X69,X70))|X70!=path_cons(skolem0012(X68,X69,X70),empty))|(~path(head_of(skolem0012(X68,X69,X70)),X69,X72)|X70!=path_cons(skolem0012(X68,X69,X70),X72)))&((X69=head_of(skolem0012(X68,X69,X70))&X70=path_cons(skolem0012(X68,X69,X70),empty))|(path(head_of(skolem0012(X68,X69,X70)),X69,skolem0013(X68,X69,X70))&X70=path_cons(skolem0012(X68,X69,X70),skolem0013(X68,X69,X70)))))))))))),inference(shift_quantors,[status(thm)],[fof(c120,plain,(![X68]:(![X69]:(![X70]:(~path(X68,X69,X70)|((vertex(X68)&vertex(X69))&((edge(skolem0012(X68,X69,X70))&X68=tail_of(skolem0012(X68,X69,X70)))&(((X69!=head_of(skolem0012(X68,X69,X70))|X70!=path_cons(skolem0012(X68,X69,X70),empty))|(![X72]:(~path(head_of(skolem0012(X68,X69,X70)),X69,X72)|X70!=path_cons(skolem0012(X68,X69,X70),X72))))&((X69=head_of(skolem0012(X68,X69,X70))&X70=path_cons(skolem0012(X68,X69,X70),empty))|(path(head_of(skolem0012(X68,X69,X70)),X69,skolem0013(X68,X69,X70))&X70=path_cons(skolem0012(X68,X69,X70),skolem0013(X68,X69,X70))))))))))),inference(skolemize,[status(esa)],[c119])).])).
% 3.18/3.39 fof(c122,plain,(![X68]:(![X69]:(![X70]:(![X72]:(((~path(X68,X69,X70)|vertex(X68))&(~path(X68,X69,X70)|vertex(X69)))&(((~path(X68,X69,X70)|edge(skolem0012(X68,X69,X70)))&(~path(X68,X69,X70)|X68=tail_of(skolem0012(X68,X69,X70))))&((~path(X68,X69,X70)|((X69!=head_of(skolem0012(X68,X69,X70))|X70!=path_cons(skolem0012(X68,X69,X70),empty))|(~path(head_of(skolem0012(X68,X69,X70)),X69,X72)|X70!=path_cons(skolem0012(X68,X69,X70),X72))))&(((~path(X68,X69,X70)|(X69=head_of(skolem0012(X68,X69,X70))|path(head_of(skolem0012(X68,X69,X70)),X69,skolem0013(X68,X69,X70))))&(~path(X68,X69,X70)|(X69=head_of(skolem0012(X68,X69,X70))|X70=path_cons(skolem0012(X68,X69,X70),skolem0013(X68,X69,X70)))))&((~path(X68,X69,X70)|(X70=path_cons(skolem0012(X68,X69,X70),empty)|path(head_of(skolem0012(X68,X69,X70)),X69,skolem0013(X68,X69,X70))))&(~path(X68,X69,X70)|(X70=path_cons(skolem0012(X68,X69,X70),empty)|X70=path_cons(skolem0012(X68,X69,X70),skolem0013(X68,X69,X70))))))))))))),inference(distribute,[status(thm)],[c121])).
% 3.18/3.39 cnf(c126,plain,~path(X360,X362,X361)|X360=tail_of(skolem0012(X360,X362,X361)),inference(split_conjunct,[status(thm)],[c122])).
% 3.18/3.39 cnf(c566,plain,skolem0001=tail_of(skolem0012(skolem0001,skolem0002,skolem0005)),inference(resolution,[status(thm)],[c126, c199])).
% 3.18/3.39 cnf(reflexivity,axiom,X84=X84,theory(equality)).
% 3.18/3.39 cnf(c13,axiom,X207!=X205|X203!=X202|X206!=X204|~shortest_path(X207,X203,X206)|shortest_path(X205,X202,X204),theory(equality)).
% 3.18/3.39 cnf(c233,plain,skolem0001!=X514|skolem0002!=X515|skolem0005!=X516|shortest_path(X514,X515,X516),inference(resolution,[status(thm)],[c13, c21])).
% 3.18/3.39 cnf(c1860,plain,skolem0001!=X559|skolem0002!=X560|shortest_path(X559,X560,skolem0005),inference(resolution,[status(thm)],[c233, reflexivity])).
% 3.18/3.39 cnf(c2123,plain,skolem0001!=X561|shortest_path(X561,skolem0002,skolem0005),inference(resolution,[status(thm)],[c1860, reflexivity])).
% 3.18/3.39 cnf(c2155,plain,shortest_path(tail_of(skolem0012(skolem0001,skolem0002,skolem0005)),skolem0002,skolem0005),inference(resolution,[status(thm)],[c2123, c566])).
% 3.18/3.39 cnf(c22,negated_conjecture,precedes(skolem0003,skolem0004,skolem0005),inference(split_conjunct,[status(thm)],[c20])).
% 3.18/3.39 cnf(c24,negated_conjecture,tail_of(skolem0006)=tail_of(skolem0003),inference(split_conjunct,[status(thm)],[c20])).
% 3.18/3.39 cnf(c25,negated_conjecture,head_of(skolem0006)=head_of(skolem0004),inference(split_conjunct,[status(thm)],[c20])).
% 3.18/3.39 fof(shortest_path_properties,axiom,(![V1]:(![V2]:(![E1]:(![E2]:(![P]:((shortest_path(V1,V2,P)&precedes(E1,E2,P))=>((~(?[E3]:(tail_of(E3)=tail_of(E1)&head_of(E3)=head_of(E2))))&(~precedes(E2,E1,P))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GRA001+0.ax', shortest_path_properties)).
% 3.18/3.39 fof(c56,plain,(![V1]:(![V2]:(![E1]:(![E2]:(![P]:((shortest_path(V1,V2,P)&precedes(E1,E2,P))=>((~(?[E3]:(tail_of(E3)=tail_of(E1)&head_of(E3)=head_of(E2))))&~precedes(E2,E1,P)))))))),inference(fof_simplification,[status(thm)],[shortest_path_properties])).
% 3.18/3.39 fof(c57,plain,(![V1]:(![V2]:(![E1]:(![E2]:(![P]:((~shortest_path(V1,V2,P)|~precedes(E1,E2,P))|((![E3]:(tail_of(E3)!=tail_of(E1)|head_of(E3)!=head_of(E2)))&~precedes(E2,E1,P)))))))),inference(fof_nnf,[status(thm)],[c56])).
% 3.18/3.39 fof(c59,plain,(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:((~shortest_path(X28,X29,X32)|~precedes(X30,X31,X32))|((tail_of(X33)!=tail_of(X30)|head_of(X33)!=head_of(X31))&~precedes(X31,X30,X32))))))))),inference(shift_quantors,[status(thm)],[fof(c58,plain,(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:((~shortest_path(X28,X29,X32)|~precedes(X30,X31,X32))|((![X33]:(tail_of(X33)!=tail_of(X30)|head_of(X33)!=head_of(X31)))&~precedes(X31,X30,X32)))))))),inference(variable_rename,[status(thm)],[c57])).])).
% 3.18/3.39 fof(c60,plain,(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:(((~shortest_path(X28,X29,X32)|~precedes(X30,X31,X32))|(tail_of(X33)!=tail_of(X30)|head_of(X33)!=head_of(X31)))&((~shortest_path(X28,X29,X32)|~precedes(X30,X31,X32))|~precedes(X31,X30,X32))))))))),inference(distribute,[status(thm)],[c59])).
% 3.18/3.39 cnf(c61,plain,~shortest_path(X285,X283,X288)|~precedes(X284,X287,X288)|tail_of(X286)!=tail_of(X284)|head_of(X286)!=head_of(X287),inference(split_conjunct,[status(thm)],[c60])).
% 3.18/3.39 cnf(c465,plain,~shortest_path(X771,X773,X774)|~precedes(X772,skolem0004,X774)|tail_of(skolem0006)!=tail_of(X772),inference(resolution,[status(thm)],[c61, c25])).
% 3.18/3.39 cnf(c8816,plain,~shortest_path(X781,X782,X780)|~precedes(skolem0003,skolem0004,X780),inference(resolution,[status(thm)],[c465, c24])).
% 3.18/3.39 cnf(c8978,plain,~shortest_path(X783,X784,skolem0005),inference(resolution,[status(thm)],[c8816, c22])).
% 3.18/3.39 cnf(c8979,plain,$false,inference(resolution,[status(thm)],[c8978, c2155])).
% 3.18/3.39 % SZS output end CNFRefutation
% 3.18/3.39
% 3.18/3.39 % Initial clauses : 83
% 3.18/3.39 % Processed clauses : 638
% 3.18/3.39 % Factors computed : 17
% 3.18/3.39 % Resolvents computed: 8805
% 3.18/3.39 % Tautologies deleted: 4
% 3.18/3.39 % Forward subsumed : 213
% 3.18/3.39 % Backward subsumed : 5
% 3.18/3.39 % -------- CPU Time ---------
% 3.18/3.39 % User time : 2.980 s
% 3.18/3.39 % System time : 0.026 s
% 3.18/3.39 % Total time : 3.006 s
%------------------------------------------------------------------------------