%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRA003+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:31 EDT 2024
% Result : Theorem 11.24s 11.42s
% Output : Refutation 11.24s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GRA003+1 : TPTP v8.1.2. Bugfixed v3.2.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n014.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 21:36:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 11.24/11.42 % Version: 1.5
% 11.24/11.42 % SZS status Theorem
% 11.24/11.42 % SZS output start CNFRefutation
% 11.24/11.42 fof(vertices_and_edges,conjecture,(![V1]:(![V2]:(![E1]:(![E2]:(![P]:((shortest_path(V1,V2,P)&precedes(E1,E2,P))=>((((((vertex(V1)&vertex(V2))&V1!=V2)&edge(E1))&edge(E2))&E1!=E2)&path(V1,V2,P)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', vertices_and_edges)).
% 11.24/11.42 fof(c16,negated_conjecture,(~(![V1]:(![V2]:(![E1]:(![E2]:(![P]:((shortest_path(V1,V2,P)&precedes(E1,E2,P))=>((((((vertex(V1)&vertex(V2))&V1!=V2)&edge(E1))&edge(E2))&E1!=E2)&path(V1,V2,P))))))))),inference(assume_negation,[status(cth)],[vertices_and_edges])).
% 11.24/11.42 fof(c17,negated_conjecture,(?[V1]:(?[V2]:(?[E1]:(?[E2]:(?[P]:((shortest_path(V1,V2,P)&precedes(E1,E2,P))&((((((~vertex(V1)|~vertex(V2))|V1=V2)|~edge(E1))|~edge(E2))|E1=E2)|~path(V1,V2,P)))))))),inference(fof_nnf,[status(thm)],[c16])).
% 11.24/11.42 fof(c18,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:((shortest_path(X2,X3,X6)&precedes(X4,X5,X6))&((((((~vertex(X2)|~vertex(X3))|X2=X3)|~edge(X4))|~edge(X5))|X4=X5)|~path(X2,X3,X6)))))))),inference(variable_rename,[status(thm)],[c17])).
% 11.24/11.42 fof(c19,negated_conjecture,((shortest_path(skolem0001,skolem0002,skolem0005)&precedes(skolem0003,skolem0004,skolem0005))&((((((~vertex(skolem0001)|~vertex(skolem0002))|skolem0001=skolem0002)|~edge(skolem0003))|~edge(skolem0004))|skolem0003=skolem0004)|~path(skolem0001,skolem0002,skolem0005))),inference(skolemize,[status(esa)],[c18])).
% 11.24/11.42 cnf(c20,negated_conjecture,shortest_path(skolem0001,skolem0002,skolem0005),inference(split_conjunct,[status(thm)],[c19])).
% 11.24/11.42 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)).
% 11.24/11.42 fof(c53,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])).
% 11.24/11.42 fof(c54,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)],[c53])).
% 11.24/11.42 fof(c56,plain,(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:((~shortest_path(X27,X28,X31)|~precedes(X29,X30,X31))|((tail_of(X32)!=tail_of(X29)|head_of(X32)!=head_of(X30))&~precedes(X30,X29,X31))))))))),inference(shift_quantors,[status(thm)],[fof(c55,plain,(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:((~shortest_path(X27,X28,X31)|~precedes(X29,X30,X31))|((![X32]:(tail_of(X32)!=tail_of(X29)|head_of(X32)!=head_of(X30)))&~precedes(X30,X29,X31)))))))),inference(variable_rename,[status(thm)],[c54])).])).
% 11.24/11.42 fof(c57,plain,(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(((~shortest_path(X27,X28,X31)|~precedes(X29,X30,X31))|(tail_of(X32)!=tail_of(X29)|head_of(X32)!=head_of(X30)))&((~shortest_path(X27,X28,X31)|~precedes(X29,X30,X31))|~precedes(X30,X29,X31))))))))),inference(distribute,[status(thm)],[c56])).
% 11.24/11.42 cnf(c59,plain,~shortest_path(X268,X270,X271)|~precedes(X267,X269,X271)|~precedes(X269,X267,X271),inference(split_conjunct,[status(thm)],[c57])).
% 11.24/11.42 cnf(c243,plain,~shortest_path(X275,X274,X272)|~precedes(X273,X273,X272),inference(factor,[status(thm)],[c59])).
% 11.24/11.42 cnf(reflexivity,axiom,X83=X83,theory(equality)).
% 11.24/11.42 cnf(c21,negated_conjecture,precedes(skolem0003,skolem0004,skolem0005),inference(split_conjunct,[status(thm)],[c19])).
% 11.24/11.42 cnf(c12,axiom,X216!=X218|X219!=X220|X217!=X215|~precedes(X216,X219,X217)|precedes(X218,X220,X215),theory(equality)).
% 11.24/11.42 cnf(c195,plain,skolem0003!=X456|skolem0004!=X455|skolem0005!=X454|precedes(X456,X455,X454),inference(resolution,[status(thm)],[c12, c21])).
% 11.24/11.42 cnf(c873,plain,skolem0003!=X464|skolem0004!=X465|precedes(X464,X465,skolem0005),inference(resolution,[status(thm)],[c195, reflexivity])).
% 11.24/11.42 cnf(c875,plain,skolem0003!=X466|precedes(X466,skolem0004,skolem0005),inference(resolution,[status(thm)],[c873, reflexivity])).
% 11.24/11.42 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)).
% 11.24/11.42 fof(c60,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])).
% 11.24/11.42 fof(c61,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)],[c60])).
% 11.24/11.42 fof(c62,plain,((![X33]:(![X34]:(![X35]:(~shortest_path(X33,X34,X35)|((path(X33,X34,X35)&X33!=X34)&(![X36]:(~path(X33,X34,X36)|less_or_equal(length_of(X35),length_of(X36)))))))))&(![X37]:(![X38]:(![X39]:(((~path(X37,X38,X39)|X37=X38)|(?[X40]:(path(X37,X38,X40)&~less_or_equal(length_of(X39),length_of(X40)))))|shortest_path(X37,X38,X39)))))),inference(variable_rename,[status(thm)],[c61])).
% 11.24/11.42 fof(c64,plain,(![X33]:(![X34]:(![X35]:(![X36]:(![X37]:(![X38]:(![X39]:((~shortest_path(X33,X34,X35)|((path(X33,X34,X35)&X33!=X34)&(~path(X33,X34,X36)|less_or_equal(length_of(X35),length_of(X36)))))&(((~path(X37,X38,X39)|X37=X38)|(path(X37,X38,skolem0008(X37,X38,X39))&~less_or_equal(length_of(X39),length_of(skolem0008(X37,X38,X39)))))|shortest_path(X37,X38,X39)))))))))),inference(shift_quantors,[status(thm)],[fof(c63,plain,((![X33]:(![X34]:(![X35]:(~shortest_path(X33,X34,X35)|((path(X33,X34,X35)&X33!=X34)&(![X36]:(~path(X33,X34,X36)|less_or_equal(length_of(X35),length_of(X36)))))))))&(![X37]:(![X38]:(![X39]:(((~path(X37,X38,X39)|X37=X38)|(path(X37,X38,skolem0008(X37,X38,X39))&~less_or_equal(length_of(X39),length_of(skolem0008(X37,X38,X39)))))|shortest_path(X37,X38,X39)))))),inference(skolemize,[status(esa)],[c62])).])).
% 11.24/11.42 fof(c65,plain,(![X33]:(![X34]:(![X35]:(![X36]:(![X37]:(![X38]:(![X39]:((((~shortest_path(X33,X34,X35)|path(X33,X34,X35))&(~shortest_path(X33,X34,X35)|X33!=X34))&(~shortest_path(X33,X34,X35)|(~path(X33,X34,X36)|less_or_equal(length_of(X35),length_of(X36)))))&((((~path(X37,X38,X39)|X37=X38)|path(X37,X38,skolem0008(X37,X38,X39)))|shortest_path(X37,X38,X39))&(((~path(X37,X38,X39)|X37=X38)|~less_or_equal(length_of(X39),length_of(skolem0008(X37,X38,X39))))|shortest_path(X37,X38,X39))))))))))),inference(distribute,[status(thm)],[c64])).
% 11.24/11.42 cnf(c67,plain,~shortest_path(X138,X136,X137)|X138!=X136,inference(split_conjunct,[status(thm)],[c65])).
% 11.24/11.42 cnf(c164,plain,skolem0001!=skolem0002,inference(resolution,[status(thm)],[c67, c20])).
% 11.24/11.42 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)).
% 11.24/11.42 fof(c114,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])).
% 11.24/11.42 fof(c115,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)],[c114])).
% 11.24/11.42 fof(c116,plain,(![X67]:(![X68]:(![X69]:(~path(X67,X68,X69)|((vertex(X67)&vertex(X68))&(?[X70]:((edge(X70)&X67=tail_of(X70))&(((X68!=head_of(X70)|X69!=path_cons(X70,empty))|(![X71]:(~path(head_of(X70),X68,X71)|X69!=path_cons(X70,X71))))&((X68=head_of(X70)&X69=path_cons(X70,empty))|(?[X72]:(path(head_of(X70),X68,X72)&X69=path_cons(X70,X72)))))))))))),inference(variable_rename,[status(thm)],[c115])).
% 11.24/11.43 fof(c118,plain,(![X67]:(![X68]:(![X69]:(![X71]:(~path(X67,X68,X69)|((vertex(X67)&vertex(X68))&((edge(skolem0011(X67,X68,X69))&X67=tail_of(skolem0011(X67,X68,X69)))&(((X68!=head_of(skolem0011(X67,X68,X69))|X69!=path_cons(skolem0011(X67,X68,X69),empty))|(~path(head_of(skolem0011(X67,X68,X69)),X68,X71)|X69!=path_cons(skolem0011(X67,X68,X69),X71)))&((X68=head_of(skolem0011(X67,X68,X69))&X69=path_cons(skolem0011(X67,X68,X69),empty))|(path(head_of(skolem0011(X67,X68,X69)),X68,skolem0012(X67,X68,X69))&X69=path_cons(skolem0011(X67,X68,X69),skolem0012(X67,X68,X69)))))))))))),inference(shift_quantors,[status(thm)],[fof(c117,plain,(![X67]:(![X68]:(![X69]:(~path(X67,X68,X69)|((vertex(X67)&vertex(X68))&((edge(skolem0011(X67,X68,X69))&X67=tail_of(skolem0011(X67,X68,X69)))&(((X68!=head_of(skolem0011(X67,X68,X69))|X69!=path_cons(skolem0011(X67,X68,X69),empty))|(![X71]:(~path(head_of(skolem0011(X67,X68,X69)),X68,X71)|X69!=path_cons(skolem0011(X67,X68,X69),X71))))&((X68=head_of(skolem0011(X67,X68,X69))&X69=path_cons(skolem0011(X67,X68,X69),empty))|(path(head_of(skolem0011(X67,X68,X69)),X68,skolem0012(X67,X68,X69))&X69=path_cons(skolem0011(X67,X68,X69),skolem0012(X67,X68,X69))))))))))),inference(skolemize,[status(esa)],[c116])).])).
% 11.24/11.43 fof(c119,plain,(![X67]:(![X68]:(![X69]:(![X71]:(((~path(X67,X68,X69)|vertex(X67))&(~path(X67,X68,X69)|vertex(X68)))&(((~path(X67,X68,X69)|edge(skolem0011(X67,X68,X69)))&(~path(X67,X68,X69)|X67=tail_of(skolem0011(X67,X68,X69))))&((~path(X67,X68,X69)|((X68!=head_of(skolem0011(X67,X68,X69))|X69!=path_cons(skolem0011(X67,X68,X69),empty))|(~path(head_of(skolem0011(X67,X68,X69)),X68,X71)|X69!=path_cons(skolem0011(X67,X68,X69),X71))))&(((~path(X67,X68,X69)|(X68=head_of(skolem0011(X67,X68,X69))|path(head_of(skolem0011(X67,X68,X69)),X68,skolem0012(X67,X68,X69))))&(~path(X67,X68,X69)|(X68=head_of(skolem0011(X67,X68,X69))|X69=path_cons(skolem0011(X67,X68,X69),skolem0012(X67,X68,X69)))))&((~path(X67,X68,X69)|(X69=path_cons(skolem0011(X67,X68,X69),empty)|path(head_of(skolem0011(X67,X68,X69)),X68,skolem0012(X67,X68,X69))))&(~path(X67,X68,X69)|(X69=path_cons(skolem0011(X67,X68,X69),empty)|X69=path_cons(skolem0011(X67,X68,X69),skolem0012(X67,X68,X69))))))))))))),inference(distribute,[status(thm)],[c118])).
% 11.24/11.43 cnf(c120,plain,~path(X110,X108,X109)|vertex(X110),inference(split_conjunct,[status(thm)],[c119])).
% 11.24/11.43 cnf(c66,plain,~shortest_path(X154,X152,X153)|path(X154,X152,X153),inference(split_conjunct,[status(thm)],[c65])).
% 11.24/11.43 cnf(c170,plain,path(skolem0001,skolem0002,skolem0005),inference(resolution,[status(thm)],[c66, c20])).
% 11.24/11.43 cnf(c171,plain,vertex(skolem0001),inference(resolution,[status(thm)],[c170, c120])).
% 11.24/11.43 cnf(c121,plain,~path(X113,X111,X112)|vertex(X111),inference(split_conjunct,[status(thm)],[c119])).
% 11.24/11.43 cnf(c172,plain,vertex(skolem0002),inference(resolution,[status(thm)],[c170, c121])).
% 11.24/11.43 fof(on_path_properties,axiom,(![V1]:(![V2]:(![P]:(![E]:((path(V1,V2,P)&on_path(E,P))=>((edge(E)&in_path(head_of(E),P))&in_path(tail_of(E),P))))))),file('/export/starexec/sandbox/benchmark/Axioms/GRA001+0.ax', on_path_properties)).
% 11.24/11.43 fof(c108,plain,(![V1]:(![V2]:(![P]:(![E]:((~path(V1,V2,P)|~on_path(E,P))|((edge(E)&in_path(head_of(E),P))&in_path(tail_of(E),P))))))),inference(fof_nnf,[status(thm)],[on_path_properties])).
% 11.24/11.43 fof(c109,plain,(![X63]:(![X64]:(![X65]:(![X66]:((~path(X63,X64,X65)|~on_path(X66,X65))|((edge(X66)&in_path(head_of(X66),X65))&in_path(tail_of(X66),X65))))))),inference(variable_rename,[status(thm)],[c108])).
% 11.24/11.43 fof(c110,plain,(![X63]:(![X64]:(![X65]:(![X66]:((((~path(X63,X64,X65)|~on_path(X66,X65))|edge(X66))&((~path(X63,X64,X65)|~on_path(X66,X65))|in_path(head_of(X66),X65)))&((~path(X63,X64,X65)|~on_path(X66,X65))|in_path(tail_of(X66),X65))))))),inference(distribute,[status(thm)],[c109])).
% 11.24/11.43 cnf(c111,plain,~path(X172,X171,X170)|~on_path(X169,X170)|edge(X169),inference(split_conjunct,[status(thm)],[c110])).
% 11.24/11.43 cnf(c176,plain,~on_path(X179,skolem0005)|edge(X179),inference(resolution,[status(thm)],[c111, c170])).
% 11.24/11.43 fof(precedes_properties,axiom,(![P]:(![V1]:(![V2]:(path(V1,V2,P)=>(![E1]:(![E2]:(precedes(E1,E2,P)=>((on_path(E1,P)&on_path(E2,P))&(sequential(E1,E2)<~>(?[E3]:(sequential(E1,E3)&precedes(E3,E2,P)))))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GRA001+0.ax', precedes_properties)).
% 11.24/11.43 fof(c71,plain,(![P]:(![V1]:(![V2]:(path(V1,V2,P)=>(![E1]:(![E2]:(precedes(E1,E2,P)=>((on_path(E1,P)&on_path(E2,P))&(~(sequential(E1,E2)<=>(?[E3]:(sequential(E1,E3)&precedes(E3,E2,P))))))))))))),inference(fof_simplification,[status(thm)],[precedes_properties])).
% 11.24/11.43 fof(c72,plain,(![P]:(![V1]:(![V2]:(~path(V1,V2,P)|(![E1]:(![E2]:(~precedes(E1,E2,P)|((on_path(E1,P)&on_path(E2,P))&((~sequential(E1,E2)|(![E3]:(~sequential(E1,E3)|~precedes(E3,E2,P))))&(sequential(E1,E2)|(?[E3]:(sequential(E1,E3)&precedes(E3,E2,P))))))))))))),inference(fof_nnf,[status(thm)],[c71])).
% 11.24/11.43 fof(c73,plain,(![P]:((![V1]:(![V2]:~path(V1,V2,P)))|(![E1]:(![E2]:(~precedes(E1,E2,P)|((on_path(E1,P)&on_path(E2,P))&((~sequential(E1,E2)|(![E3]:(~sequential(E1,E3)|~precedes(E3,E2,P))))&(sequential(E1,E2)|(?[E3]:(sequential(E1,E3)&precedes(E3,E2,P))))))))))),inference(shift_quantors,[status(thm)],[c72])).
% 11.24/11.43 fof(c74,plain,(![X41]:((![X42]:(![X43]:~path(X42,X43,X41)))|(![X44]:(![X45]:(~precedes(X44,X45,X41)|((on_path(X44,X41)&on_path(X45,X41))&((~sequential(X44,X45)|(![X46]:(~sequential(X44,X46)|~precedes(X46,X45,X41))))&(sequential(X44,X45)|(?[X47]:(sequential(X44,X47)&precedes(X47,X45,X41))))))))))),inference(variable_rename,[status(thm)],[c73])).
% 11.24/11.43 fof(c76,plain,(![X41]:(![X42]:(![X43]:(![X44]:(![X45]:(![X46]:(~path(X42,X43,X41)|(~precedes(X44,X45,X41)|((on_path(X44,X41)&on_path(X45,X41))&((~sequential(X44,X45)|(~sequential(X44,X46)|~precedes(X46,X45,X41)))&(sequential(X44,X45)|(sequential(X44,skolem0009(X41,X44,X45))&precedes(skolem0009(X41,X44,X45),X45,X41))))))))))))),inference(shift_quantors,[status(thm)],[fof(c75,plain,(![X41]:((![X42]:(![X43]:~path(X42,X43,X41)))|(![X44]:(![X45]:(~precedes(X44,X45,X41)|((on_path(X44,X41)&on_path(X45,X41))&((~sequential(X44,X45)|(![X46]:(~sequential(X44,X46)|~precedes(X46,X45,X41))))&(sequential(X44,X45)|(sequential(X44,skolem0009(X41,X44,X45))&precedes(skolem0009(X41,X44,X45),X45,X41)))))))))),inference(skolemize,[status(esa)],[c74])).])).
% 11.24/11.43 fof(c77,plain,(![X41]:(![X42]:(![X43]:(![X44]:(![X45]:(![X46]:(((~path(X42,X43,X41)|(~precedes(X44,X45,X41)|on_path(X44,X41)))&(~path(X42,X43,X41)|(~precedes(X44,X45,X41)|on_path(X45,X41))))&((~path(X42,X43,X41)|(~precedes(X44,X45,X41)|(~sequential(X44,X45)|(~sequential(X44,X46)|~precedes(X46,X45,X41)))))&((~path(X42,X43,X41)|(~precedes(X44,X45,X41)|(sequential(X44,X45)|sequential(X44,skolem0009(X41,X44,X45)))))&(~path(X42,X43,X41)|(~precedes(X44,X45,X41)|(sequential(X44,X45)|precedes(skolem0009(X41,X44,X45),X45,X41))))))))))))),inference(distribute,[status(thm)],[c76])).
% 11.24/11.43 cnf(c78,plain,~path(X188,X187,X190)|~precedes(X191,X189,X190)|on_path(X191,X190),inference(split_conjunct,[status(thm)],[c77])).
% 11.24/11.43 cnf(c181,plain,~path(X192,X193,skolem0005)|on_path(skolem0003,skolem0005),inference(resolution,[status(thm)],[c78, c21])).
% 11.24/11.43 cnf(c182,plain,on_path(skolem0003,skolem0005),inference(resolution,[status(thm)],[c181, c170])).
% 11.24/11.43 cnf(c184,plain,edge(skolem0003),inference(resolution,[status(thm)],[c182, c176])).
% 11.24/11.43 cnf(c79,plain,~path(X199,X198,X201)|~precedes(X202,X200,X201)|on_path(X200,X201),inference(split_conjunct,[status(thm)],[c77])).
% 11.24/11.43 cnf(c187,plain,~path(X204,X203,skolem0005)|on_path(skolem0004,skolem0005),inference(resolution,[status(thm)],[c79, c21])).
% 11.24/11.43 cnf(c188,plain,on_path(skolem0004,skolem0005),inference(resolution,[status(thm)],[c187, c170])).
% 11.24/11.43 cnf(c190,plain,edge(skolem0004),inference(resolution,[status(thm)],[c188, c176])).
% 11.24/11.43 cnf(c22,negated_conjecture,~vertex(skolem0001)|~vertex(skolem0002)|skolem0001=skolem0002|~edge(skolem0003)|~edge(skolem0004)|skolem0003=skolem0004|~path(skolem0001,skolem0002,skolem0005),inference(split_conjunct,[status(thm)],[c19])).
% 11.24/11.43 cnf(c241,plain,~vertex(skolem0001)|~vertex(skolem0002)|skolem0001=skolem0002|~edge(skolem0003)|~edge(skolem0004)|skolem0003=skolem0004,inference(resolution,[status(thm)],[c22, c170])).
% 11.24/11.43 cnf(c1333,plain,~vertex(skolem0001)|~vertex(skolem0002)|skolem0001=skolem0002|~edge(skolem0003)|skolem0003=skolem0004,inference(resolution,[status(thm)],[c241, c190])).
% 11.24/11.43 cnf(c30401,plain,~vertex(skolem0001)|~vertex(skolem0002)|skolem0001=skolem0002|skolem0003=skolem0004,inference(resolution,[status(thm)],[c1333, c184])).
% 11.24/11.43 cnf(c30402,plain,~vertex(skolem0001)|skolem0001=skolem0002|skolem0003=skolem0004,inference(resolution,[status(thm)],[c30401, c172])).
% 11.24/11.43 cnf(c30403,plain,skolem0001=skolem0002|skolem0003=skolem0004,inference(resolution,[status(thm)],[c30402, c171])).
% 11.24/11.43 cnf(c30520,plain,skolem0003=skolem0004,inference(resolution,[status(thm)],[c30403, c164])).
% 11.24/11.43 cnf(c30703,plain,precedes(skolem0004,skolem0004,skolem0005),inference(resolution,[status(thm)],[c30520, c875])).
% 11.24/11.43 cnf(c31187,plain,~shortest_path(X1339,X1340,skolem0005),inference(resolution,[status(thm)],[c30703, c243])).
% 11.24/11.43 cnf(c31283,plain,$false,inference(resolution,[status(thm)],[c31187, c20])).
% 11.24/11.43 % SZS output end CNFRefutation
% 11.24/11.43
% 11.24/11.43 % Initial clauses : 81
% 11.24/11.43 % Processed clauses : 1092
% 11.24/11.43 % Factors computed : 18
% 11.24/11.43 % Resolvents computed: 31111
% 11.24/11.43 % Tautologies deleted: 4
% 11.24/11.43 % Forward subsumed : 435
% 11.24/11.43 % Backward subsumed : 12
% 11.24/11.43 % -------- CPU Time ---------
% 11.24/11.43 % User time : 11.001 s
% 11.24/11.43 % System time : 0.074 s
% 11.24/11.43 % Total time : 11.075 s
%------------------------------------------------------------------------------