%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRA075+1 : TPTP v8.1.2. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n026.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:42 EDT 2024
% Result : Satisfiable 0.42s 0.62s
% Output : Saturation 0.46s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GRA075+1 : TPTP v8.1.2. Released v6.4.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n026.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.42/0.62 % Version: 1.5
% 0.42/0.62 % SZS status Satisfiable
% 0.42/0.62 % SZS output start Saturation
% 0.42/0.62 fof(complete_properties,axiom,(complete=>(![V1]:(![V2]:(((vertex(V1)&vertex(V2))&V1!=V2)=>(?[E]:(edge(E)&((V1=head_of(E)&V2=tail_of(E))<~>(V2=head_of(E)&V1=tail_of(E))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GRA001+0.ax', complete_properties)).
% 0.42/0.62 fof(c96,plain,(complete=>(![V1]:(![V2]:(((vertex(V1)&vertex(V2))&V1!=V2)=>(?[E]:(edge(E)&(~((V1=head_of(E)&V2=tail_of(E))<=>(V2=head_of(E)&V1=tail_of(E)))))))))),inference(fof_simplification,[status(thm)],[complete_properties])).
% 0.42/0.62 fof(c97,plain,(~complete|(![V1]:(![V2]:(((~vertex(V1)|~vertex(V2))|V1=V2)|(?[E]:(edge(E)&(((V1!=head_of(E)|V2!=tail_of(E))|(V2!=head_of(E)|V1!=tail_of(E)))&((V1=head_of(E)&V2=tail_of(E))|(V2=head_of(E)&V1=tail_of(E)))))))))),inference(fof_nnf,[status(thm)],[c96])).
% 0.42/0.62 fof(c98,plain,(~complete|(![X53]:(![X54]:(((~vertex(X53)|~vertex(X54))|X53=X54)|(?[X55]:(edge(X55)&(((X53!=head_of(X55)|X54!=tail_of(X55))|(X54!=head_of(X55)|X53!=tail_of(X55)))&((X53=head_of(X55)&X54=tail_of(X55))|(X54=head_of(X55)&X53=tail_of(X55)))))))))),inference(variable_rename,[status(thm)],[c97])).
% 0.42/0.62 fof(c100,plain,(![X53]:(![X54]:(~complete|(((~vertex(X53)|~vertex(X54))|X53=X54)|(edge(skolem0006(X53,X54))&(((X53!=head_of(skolem0006(X53,X54))|X54!=tail_of(skolem0006(X53,X54)))|(X54!=head_of(skolem0006(X53,X54))|X53!=tail_of(skolem0006(X53,X54))))&((X53=head_of(skolem0006(X53,X54))&X54=tail_of(skolem0006(X53,X54)))|(X54=head_of(skolem0006(X53,X54))&X53=tail_of(skolem0006(X53,X54)))))))))),inference(shift_quantors,[status(thm)],[fof(c99,plain,(~complete|(![X53]:(![X54]:(((~vertex(X53)|~vertex(X54))|X53=X54)|(edge(skolem0006(X53,X54))&(((X53!=head_of(skolem0006(X53,X54))|X54!=tail_of(skolem0006(X53,X54)))|(X54!=head_of(skolem0006(X53,X54))|X53!=tail_of(skolem0006(X53,X54))))&((X53=head_of(skolem0006(X53,X54))&X54=tail_of(skolem0006(X53,X54)))|(X54=head_of(skolem0006(X53,X54))&X53=tail_of(skolem0006(X53,X54)))))))))),inference(skolemize,[status(esa)],[c98])).])).
% 0.42/0.62 fof(c101,plain,(![X53]:(![X54]:((~complete|(((~vertex(X53)|~vertex(X54))|X53=X54)|edge(skolem0006(X53,X54))))&((~complete|(((~vertex(X53)|~vertex(X54))|X53=X54)|((X53!=head_of(skolem0006(X53,X54))|X54!=tail_of(skolem0006(X53,X54)))|(X54!=head_of(skolem0006(X53,X54))|X53!=tail_of(skolem0006(X53,X54))))))&(((~complete|(((~vertex(X53)|~vertex(X54))|X53=X54)|(X53=head_of(skolem0006(X53,X54))|X54=head_of(skolem0006(X53,X54)))))&(~complete|(((~vertex(X53)|~vertex(X54))|X53=X54)|(X53=head_of(skolem0006(X53,X54))|X53=tail_of(skolem0006(X53,X54))))))&((~complete|(((~vertex(X53)|~vertex(X54))|X53=X54)|(X54=tail_of(skolem0006(X53,X54))|X54=head_of(skolem0006(X53,X54)))))&(~complete|(((~vertex(X53)|~vertex(X54))|X53=X54)|(X54=tail_of(skolem0006(X53,X54))|X53=tail_of(skolem0006(X53,X54))))))))))),inference(distribute,[status(thm)],[c100])).
% 0.42/0.62 cnf(c103,plain,~complete|~vertex(X315)|~vertex(X314)|X315=X314|X315!=head_of(skolem0006(X315,X314))|X314!=tail_of(skolem0006(X315,X314))|X314!=head_of(skolem0006(X315,X314))|X315!=tail_of(skolem0006(X315,X314)),inference(split_conjunct,[status(thm)],[c101])).
% 0.42/0.62 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)).
% 0.42/0.62 fof(c74,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])).
% 0.42/0.62 fof(c75,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)],[c74])).
% 0.42/0.62 fof(c76,plain,(![X42]:(![X43]:(![X44]:(~path(X42,X43,X44)|((vertex(X42)&vertex(X43))&(?[X45]:((edge(X45)&X42=tail_of(X45))&(((X43!=head_of(X45)|X44!=path_cons(X45,empty))|(![X46]:(~path(head_of(X45),X43,X46)|X44!=path_cons(X45,X46))))&((X43=head_of(X45)&X44=path_cons(X45,empty))|(?[X47]:(path(head_of(X45),X43,X47)&X44=path_cons(X45,X47)))))))))))),inference(variable_rename,[status(thm)],[c75])).
% 0.42/0.62 fof(c78,plain,(![X42]:(![X43]:(![X44]:(![X46]:(~path(X42,X43,X44)|((vertex(X42)&vertex(X43))&((edge(skolem0004(X42,X43,X44))&X42=tail_of(skolem0004(X42,X43,X44)))&(((X43!=head_of(skolem0004(X42,X43,X44))|X44!=path_cons(skolem0004(X42,X43,X44),empty))|(~path(head_of(skolem0004(X42,X43,X44)),X43,X46)|X44!=path_cons(skolem0004(X42,X43,X44),X46)))&((X43=head_of(skolem0004(X42,X43,X44))&X44=path_cons(skolem0004(X42,X43,X44),empty))|(path(head_of(skolem0004(X42,X43,X44)),X43,skolem0005(X42,X43,X44))&X44=path_cons(skolem0004(X42,X43,X44),skolem0005(X42,X43,X44)))))))))))),inference(shift_quantors,[status(thm)],[fof(c77,plain,(![X42]:(![X43]:(![X44]:(~path(X42,X43,X44)|((vertex(X42)&vertex(X43))&((edge(skolem0004(X42,X43,X44))&X42=tail_of(skolem0004(X42,X43,X44)))&(((X43!=head_of(skolem0004(X42,X43,X44))|X44!=path_cons(skolem0004(X42,X43,X44),empty))|(![X46]:(~path(head_of(skolem0004(X42,X43,X44)),X43,X46)|X44!=path_cons(skolem0004(X42,X43,X44),X46))))&((X43=head_of(skolem0004(X42,X43,X44))&X44=path_cons(skolem0004(X42,X43,X44),empty))|(path(head_of(skolem0004(X42,X43,X44)),X43,skolem0005(X42,X43,X44))&X44=path_cons(skolem0004(X42,X43,X44),skolem0005(X42,X43,X44))))))))))),inference(skolemize,[status(esa)],[c76])).])).
% 0.42/0.62 fof(c79,plain,(![X42]:(![X43]:(![X44]:(![X46]:(((~path(X42,X43,X44)|vertex(X42))&(~path(X42,X43,X44)|vertex(X43)))&(((~path(X42,X43,X44)|edge(skolem0004(X42,X43,X44)))&(~path(X42,X43,X44)|X42=tail_of(skolem0004(X42,X43,X44))))&((~path(X42,X43,X44)|((X43!=head_of(skolem0004(X42,X43,X44))|X44!=path_cons(skolem0004(X42,X43,X44),empty))|(~path(head_of(skolem0004(X42,X43,X44)),X43,X46)|X44!=path_cons(skolem0004(X42,X43,X44),X46))))&(((~path(X42,X43,X44)|(X43=head_of(skolem0004(X42,X43,X44))|path(head_of(skolem0004(X42,X43,X44)),X43,skolem0005(X42,X43,X44))))&(~path(X42,X43,X44)|(X43=head_of(skolem0004(X42,X43,X44))|X44=path_cons(skolem0004(X42,X43,X44),skolem0005(X42,X43,X44)))))&((~path(X42,X43,X44)|(X44=path_cons(skolem0004(X42,X43,X44),empty)|path(head_of(skolem0004(X42,X43,X44)),X43,skolem0005(X42,X43,X44))))&(~path(X42,X43,X44)|(X44=path_cons(skolem0004(X42,X43,X44),empty)|X44=path_cons(skolem0004(X42,X43,X44),skolem0005(X42,X43,X44))))))))))))),inference(distribute,[status(thm)],[c78])).
% 0.42/0.62 cnf(c84,plain,~path(X282,X285,X284)|X285!=head_of(skolem0004(X282,X285,X284))|X284!=path_cons(skolem0004(X282,X285,X284),empty)|~path(head_of(skolem0004(X282,X285,X284)),X285,X283)|X284!=path_cons(skolem0004(X282,X285,X284),X283),inference(split_conjunct,[status(thm)],[c79])).
% 0.42/0.62 cnf(c138,plain,~path(X312,X313,X311)|X313!=head_of(skolem0004(X312,X313,X311))|X311!=path_cons(skolem0004(X312,X313,X311),empty)|~path(head_of(skolem0004(X312,X313,X311)),X313,empty),inference(factor,[status(thm)],[c84])).
% 0.42/0.62 cnf(reflexivity,axiom,X58=X58,theory(equality)).
% 0.42/0.62 fof(path_defn,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_defn)).
% 0.42/0.62 fof(c89,plain,(![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)))))))=>path(V1,V2,P))))),inference(fof_simplification,[status(thm)],[path_defn])).
% 0.42/0.62 fof(c90,plain,(![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)))))))|path(V1,V2,P))))),inference(fof_nnf,[status(thm)],[c89])).
% 0.42/0.62 fof(c92,plain,(![X48]:(![X49]:(![X50]:(![X51]:(![X52]:(((~vertex(X48)|~vertex(X49))|((~edge(X51)|X48!=tail_of(X51))|((X49!=head_of(X51)|X50!=path_cons(X51,empty))&(~path(head_of(X51),X49,X52)|X50!=path_cons(X51,X52)))))|path(X48,X49,X50))))))),inference(shift_quantors,[status(thm)],[fof(c91,plain,(![X48]:(![X49]:(![X50]:(((~vertex(X48)|~vertex(X49))|(![X51]:((~edge(X51)|X48!=tail_of(X51))|((X49!=head_of(X51)|X50!=path_cons(X51,empty))&(![X52]:(~path(head_of(X51),X49,X52)|X50!=path_cons(X51,X52)))))))|path(X48,X49,X50))))),inference(variable_rename,[status(thm)],[c90])).])).
% 0.42/0.62 fof(c93,plain,(![X48]:(![X49]:(![X50]:(![X51]:(![X52]:((((~vertex(X48)|~vertex(X49))|((~edge(X51)|X48!=tail_of(X51))|(X49!=head_of(X51)|X50!=path_cons(X51,empty))))|path(X48,X49,X50))&(((~vertex(X48)|~vertex(X49))|((~edge(X51)|X48!=tail_of(X51))|(~path(head_of(X51),X49,X52)|X50!=path_cons(X51,X52))))|path(X48,X49,X50)))))))),inference(distribute,[status(thm)],[c92])).
% 0.42/0.62 cnf(c95,plain,~vertex(X305)|~vertex(X302)|~edge(X301)|X305!=tail_of(X301)|~path(head_of(X301),X302,X304)|X303!=path_cons(X301,X304)|path(X305,X302,X303),inference(split_conjunct,[status(thm)],[c93])).
% 0.42/0.62 cnf(c142,plain,~vertex(X310)|~vertex(X309)|~edge(X308)|X310!=tail_of(X308)|~path(head_of(X308),X309,X307)|path(X310,X309,path_cons(X308,X307)),inference(resolution,[status(thm)],[c95, reflexivity])).
% 0.42/0.62 cnf(c94,plain,~vertex(X295)|~vertex(X294)|~edge(X292)|X295!=tail_of(X292)|X294!=head_of(X292)|X293!=path_cons(X292,empty)|path(X295,X294,X293),inference(split_conjunct,[status(thm)],[c93])).
% 0.42/0.62 cnf(c139,plain,~vertex(X297)|~vertex(X298)|~edge(X296)|X297!=tail_of(X296)|X298!=head_of(X296)|path(X297,X298,path_cons(X296,empty)),inference(resolution,[status(thm)],[c94, reflexivity])).
% 0.42/0.62 cnf(c140,plain,~vertex(X300)|~vertex(head_of(X299))|~edge(X299)|X300!=tail_of(X299)|path(X300,head_of(X299),path_cons(X299,empty)),inference(resolution,[status(thm)],[c139, reflexivity])).
% 0.42/0.62 cnf(c141,plain,~vertex(tail_of(X306))|~vertex(head_of(X306))|~edge(X306)|path(tail_of(X306),head_of(X306),path_cons(X306,empty)),inference(resolution,[status(thm)],[c140, reflexivity])).
% 0.42/0.62 cnf(c88,plain,~path(X289,X291,X290)|X290=path_cons(skolem0004(X289,X291,X290),empty)|X290=path_cons(skolem0004(X289,X291,X290),skolem0005(X289,X291,X290)),inference(split_conjunct,[status(thm)],[c79])).
% 0.42/0.62 cnf(c87,plain,~path(X286,X288,X287)|X287=path_cons(skolem0004(X286,X288,X287),empty)|path(head_of(skolem0004(X286,X288,X287)),X288,skolem0005(X286,X288,X287)),inference(split_conjunct,[status(thm)],[c79])).
% 0.42/0.62 cnf(c107,plain,~complete|~vertex(X280)|~vertex(X279)|X280=X279|X279=tail_of(skolem0006(X280,X279))|X280=tail_of(skolem0006(X280,X279)),inference(split_conjunct,[status(thm)],[c101])).
% 0.42/0.62 cnf(c106,plain,~complete|~vertex(X277)|~vertex(X276)|X277=X276|X276=tail_of(skolem0006(X277,X276))|X276=head_of(skolem0006(X277,X276)),inference(split_conjunct,[status(thm)],[c101])).
% 0.42/0.62 fof(in_path_properties,axiom,(![V1]:(![V2]:(![P]:(![V]:((path(V1,V2,P)&in_path(V,P))=>(vertex(V)&(?[E]:(on_path(E,P)&(V=head_of(E)|V=tail_of(E)))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GRA001+0.ax', in_path_properties)).
% 0.42/0.62 fof(c61,plain,(![V1]:(![V2]:(![P]:(![V]:((~path(V1,V2,P)|~in_path(V,P))|(vertex(V)&(?[E]:(on_path(E,P)&(V=head_of(E)|V=tail_of(E)))))))))),inference(fof_nnf,[status(thm)],[in_path_properties])).
% 0.42/0.62 fof(c62,plain,(![X33]:(![X34]:(![X35]:(![X36]:((~path(X33,X34,X35)|~in_path(X36,X35))|(vertex(X36)&(?[X37]:(on_path(X37,X35)&(X36=head_of(X37)|X36=tail_of(X37)))))))))),inference(variable_rename,[status(thm)],[c61])).
% 0.42/0.62 fof(c63,plain,(![X33]:(![X34]:(![X35]:(![X36]:((~path(X33,X34,X35)|~in_path(X36,X35))|(vertex(X36)&(on_path(skolem0003(X33,X34,X35,X36),X35)&(X36=head_of(skolem0003(X33,X34,X35,X36))|X36=tail_of(skolem0003(X33,X34,X35,X36)))))))))),inference(skolemize,[status(esa)],[c62])).
% 0.42/0.62 fof(c64,plain,(![X33]:(![X34]:(![X35]:(![X36]:(((~path(X33,X34,X35)|~in_path(X36,X35))|vertex(X36))&(((~path(X33,X34,X35)|~in_path(X36,X35))|on_path(skolem0003(X33,X34,X35,X36),X35))&((~path(X33,X34,X35)|~in_path(X36,X35))|(X36=head_of(skolem0003(X33,X34,X35,X36))|X36=tail_of(skolem0003(X33,X34,X35,X36)))))))))),inference(distribute,[status(thm)],[c63])).
% 0.42/0.62 cnf(c67,plain,~path(X271,X273,X272)|~in_path(X274,X272)|X274=head_of(skolem0003(X271,X273,X272,X274))|X274=tail_of(skolem0003(X271,X273,X272,X274)),inference(split_conjunct,[status(thm)],[c64])).
% 0.42/0.62 cnf(c105,plain,~complete|~vertex(X270)|~vertex(X269)|X270=X269|X270=head_of(skolem0006(X270,X269))|X270=tail_of(skolem0006(X270,X269)),inference(split_conjunct,[status(thm)],[c101])).
% 0.42/0.62 cnf(c104,plain,~complete|~vertex(X267)|~vertex(X266)|X267=X266|X267=head_of(skolem0006(X267,X266))|X266=head_of(skolem0006(X267,X266)),inference(split_conjunct,[status(thm)],[c101])).
% 0.42/0.62 cnf(c86,plain,~path(X263,X265,X264)|X265=head_of(skolem0004(X263,X265,X264))|X264=path_cons(skolem0004(X263,X265,X264),skolem0005(X263,X265,X264)),inference(split_conjunct,[status(thm)],[c79])).
% 0.42/0.62 cnf(c85,plain,~path(X260,X262,X261)|X262=head_of(skolem0004(X260,X262,X261))|path(head_of(skolem0004(X260,X262,X261)),X262,skolem0005(X260,X262,X261)),inference(split_conjunct,[status(thm)],[c79])).
% 0.42/0.62 fof(precedes_defn,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_defn)).
% 0.42/0.62 fof(c43,plain,(![P]:(![V1]:(![V2]:(path(V1,V2,P)=>(![E1]:(![E2]:(((on_path(E1,P)&on_path(E2,P))&(sequential(E1,E2)|(?[E3]:(sequential(E1,E3)&precedes(E3,E2,P)))))=>precedes(E1,E2,P)))))))),inference(fof_simplification,[status(thm)],[precedes_defn])).
% 0.42/0.62 fof(c44,plain,(![P]:(![V1]:(![V2]:(~path(V1,V2,P)|(![E1]:(![E2]:(((~on_path(E1,P)|~on_path(E2,P))|(~sequential(E1,E2)&(![E3]:(~sequential(E1,E3)|~precedes(E3,E2,P)))))|precedes(E1,E2,P)))))))),inference(fof_nnf,[status(thm)],[c43])).
% 0.42/0.62 fof(c45,plain,(![P]:((![V1]:(![V2]:~path(V1,V2,P)))|(![E1]:(![E2]:(((~on_path(E1,P)|~on_path(E2,P))|(~sequential(E1,E2)&(![E3]:(~sequential(E1,E3)|~precedes(E3,E2,P)))))|precedes(E1,E2,P)))))),inference(shift_quantors,[status(thm)],[c44])).
% 0.42/0.62 fof(c47,plain,(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:(![X28]:(~path(X24,X25,X23)|(((~on_path(X26,X23)|~on_path(X27,X23))|(~sequential(X26,X27)&(~sequential(X26,X28)|~precedes(X28,X27,X23))))|precedes(X26,X27,X23))))))))),inference(shift_quantors,[status(thm)],[fof(c46,plain,(![X23]:((![X24]:(![X25]:~path(X24,X25,X23)))|(![X26]:(![X27]:(((~on_path(X26,X23)|~on_path(X27,X23))|(~sequential(X26,X27)&(![X28]:(~sequential(X26,X28)|~precedes(X28,X27,X23)))))|precedes(X26,X27,X23)))))),inference(variable_rename,[status(thm)],[c45])).])).
% 0.42/0.62 fof(c48,plain,(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:(![X28]:((~path(X24,X25,X23)|(((~on_path(X26,X23)|~on_path(X27,X23))|~sequential(X26,X27))|precedes(X26,X27,X23)))&(~path(X24,X25,X23)|(((~on_path(X26,X23)|~on_path(X27,X23))|(~sequential(X26,X28)|~precedes(X28,X27,X23)))|precedes(X26,X27,X23)))))))))),inference(distribute,[status(thm)],[c47])).
% 0.42/0.62 cnf(c50,plain,~path(X257,X259,X256)|~on_path(X258,X256)|~on_path(X254,X256)|~sequential(X258,X255)|~precedes(X255,X254,X256)|precedes(X258,X254,X256),inference(split_conjunct,[status(thm)],[c48])).
% 0.42/0.62 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)).
% 0.42/0.62 fof(c20,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.42/0.62 fof(c21,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)],[c20])).
% 0.42/0.62 fof(c22,plain,((![X8]:(![X9]:(![X10]:(~shortest_path(X8,X9,X10)|((path(X8,X9,X10)&X8!=X9)&(![X11]:(~path(X8,X9,X11)|less_or_equal(length_of(X10),length_of(X11)))))))))&(![X12]:(![X13]:(![X14]:(((~path(X12,X13,X14)|X12=X13)|(?[X15]:(path(X12,X13,X15)&~less_or_equal(length_of(X14),length_of(X15)))))|shortest_path(X12,X13,X14)))))),inference(variable_rename,[status(thm)],[c21])).
% 0.42/0.62 fof(c24,plain,(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:((~shortest_path(X8,X9,X10)|((path(X8,X9,X10)&X8!=X9)&(~path(X8,X9,X11)|less_or_equal(length_of(X10),length_of(X11)))))&(((~path(X12,X13,X14)|X12=X13)|(path(X12,X13,skolem0001(X12,X13,X14))&~less_or_equal(length_of(X14),length_of(skolem0001(X12,X13,X14)))))|shortest_path(X12,X13,X14)))))))))),inference(shift_quantors,[status(thm)],[fof(c23,plain,((![X8]:(![X9]:(![X10]:(~shortest_path(X8,X9,X10)|((path(X8,X9,X10)&X8!=X9)&(![X11]:(~path(X8,X9,X11)|less_or_equal(length_of(X10),length_of(X11)))))))))&(![X12]:(![X13]:(![X14]:(((~path(X12,X13,X14)|X12=X13)|(path(X12,X13,skolem0001(X12,X13,X14))&~less_or_equal(length_of(X14),length_of(skolem0001(X12,X13,X14)))))|shortest_path(X12,X13,X14)))))),inference(skolemize,[status(esa)],[c22])).])).
% 0.46/0.62 fof(c25,plain,(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:((((~shortest_path(X8,X9,X10)|path(X8,X9,X10))&(~shortest_path(X8,X9,X10)|X8!=X9))&(~shortest_path(X8,X9,X10)|(~path(X8,X9,X11)|less_or_equal(length_of(X10),length_of(X11)))))&((((~path(X12,X13,X14)|X12=X13)|path(X12,X13,skolem0001(X12,X13,X14)))|shortest_path(X12,X13,X14))&(((~path(X12,X13,X14)|X12=X13)|~less_or_equal(length_of(X14),length_of(skolem0001(X12,X13,X14))))|shortest_path(X12,X13,X14))))))))))),inference(distribute,[status(thm)],[c24])).
% 0.46/0.62 cnf(c30,plain,~path(X251,X253,X252)|X251=X253|~less_or_equal(length_of(X252),length_of(skolem0001(X251,X253,X252)))|shortest_path(X251,X253,X252),inference(split_conjunct,[status(thm)],[c25])).
% 0.46/0.62 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)).
% 0.46/0.62 fof(c31,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])).
% 0.46/0.62 fof(c32,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)],[c31])).
% 0.46/0.62 fof(c33,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)],[c32])).
% 0.46/0.62 fof(c34,plain,(![X16]:((![X17]:(![X18]:~path(X17,X18,X16)))|(![X19]:(![X20]:(~precedes(X19,X20,X16)|((on_path(X19,X16)&on_path(X20,X16))&((~sequential(X19,X20)|(![X21]:(~sequential(X19,X21)|~precedes(X21,X20,X16))))&(sequential(X19,X20)|(?[X22]:(sequential(X19,X22)&precedes(X22,X20,X16))))))))))),inference(variable_rename,[status(thm)],[c33])).
% 0.46/0.62 fof(c36,plain,(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(~path(X17,X18,X16)|(~precedes(X19,X20,X16)|((on_path(X19,X16)&on_path(X20,X16))&((~sequential(X19,X20)|(~sequential(X19,X21)|~precedes(X21,X20,X16)))&(sequential(X19,X20)|(sequential(X19,skolem0002(X16,X19,X20))&precedes(skolem0002(X16,X19,X20),X20,X16))))))))))))),inference(shift_quantors,[status(thm)],[fof(c35,plain,(![X16]:((![X17]:(![X18]:~path(X17,X18,X16)))|(![X19]:(![X20]:(~precedes(X19,X20,X16)|((on_path(X19,X16)&on_path(X20,X16))&((~sequential(X19,X20)|(![X21]:(~sequential(X19,X21)|~precedes(X21,X20,X16))))&(sequential(X19,X20)|(sequential(X19,skolem0002(X16,X19,X20))&precedes(skolem0002(X16,X19,X20),X20,X16)))))))))),inference(skolemize,[status(esa)],[c34])).])).
% 0.46/0.62 fof(c37,plain,(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(((~path(X17,X18,X16)|(~precedes(X19,X20,X16)|on_path(X19,X16)))&(~path(X17,X18,X16)|(~precedes(X19,X20,X16)|on_path(X20,X16))))&((~path(X17,X18,X16)|(~precedes(X19,X20,X16)|(~sequential(X19,X20)|(~sequential(X19,X21)|~precedes(X21,X20,X16)))))&((~path(X17,X18,X16)|(~precedes(X19,X20,X16)|(sequential(X19,X20)|sequential(X19,skolem0002(X16,X19,X20)))))&(~path(X17,X18,X16)|(~precedes(X19,X20,X16)|(sequential(X19,X20)|precedes(skolem0002(X16,X19,X20),X20,X16))))))))))))),inference(distribute,[status(thm)],[c36])).
% 0.46/0.62 cnf(c42,plain,~path(X249,X248,X250)|~precedes(X246,X247,X250)|sequential(X246,X247)|precedes(skolem0002(X250,X246,X247),X247,X250),inference(split_conjunct,[status(thm)],[c37])).
% 0.46/0.62 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)).
% 0.46/0.62 fof(c13,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])).
% 0.46/0.62 fof(c14,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)],[c13])).
% 0.46/0.62 fof(c16,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:((~shortest_path(X2,X3,X6)|~precedes(X4,X5,X6))|((tail_of(X7)!=tail_of(X4)|head_of(X7)!=head_of(X5))&~precedes(X5,X4,X6))))))))),inference(shift_quantors,[status(thm)],[fof(c15,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:((~shortest_path(X2,X3,X6)|~precedes(X4,X5,X6))|((![X7]:(tail_of(X7)!=tail_of(X4)|head_of(X7)!=head_of(X5)))&~precedes(X5,X4,X6)))))))),inference(variable_rename,[status(thm)],[c14])).])).
% 0.46/0.62 fof(c17,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(((~shortest_path(X2,X3,X6)|~precedes(X4,X5,X6))|(tail_of(X7)!=tail_of(X4)|head_of(X7)!=head_of(X5)))&((~shortest_path(X2,X3,X6)|~precedes(X4,X5,X6))|~precedes(X5,X4,X6))))))))),inference(distribute,[status(thm)],[c16])).
% 0.46/0.62 cnf(c18,plain,~shortest_path(X229,X231,X227)|~precedes(X226,X228,X227)|tail_of(X230)!=tail_of(X226)|head_of(X230)!=head_of(X228),inference(split_conjunct,[status(thm)],[c17])).
% 0.46/0.62 cnf(c132,plain,~shortest_path(X239,X240,X241)|~precedes(X238,X237,X241)|tail_of(X237)!=tail_of(X238),inference(resolution,[status(thm)],[c18, reflexivity])).
% 0.46/0.62 cnf(c40,plain,~path(X224,X223,X225)|~precedes(X221,X222,X225)|~sequential(X221,X222)|~sequential(X221,X220)|~precedes(X220,X222,X225),inference(split_conjunct,[status(thm)],[c37])).
% 0.46/0.62 cnf(c29,plain,~path(X217,X219,X218)|X217=X219|path(X217,X219,skolem0001(X217,X219,X218))|shortest_path(X217,X219,X218),inference(split_conjunct,[status(thm)],[c25])).
% 0.46/0.62 fof(sequential_defn,axiom,(![E1]:(![E2]:(sequential(E1,E2)<=>(((edge(E1)&edge(E2))&E1!=E2)&head_of(E1)=tail_of(E2))))),file('/export/starexec/sandbox/benchmark/Axioms/GRA001+0.ax', sequential_defn)).
% 0.46/0.62 fof(c51,plain,(![E1]:(![E2]:((~sequential(E1,E2)|(((edge(E1)&edge(E2))&E1!=E2)&head_of(E1)=tail_of(E2)))&((((~edge(E1)|~edge(E2))|E1=E2)|head_of(E1)!=tail_of(E2))|sequential(E1,E2))))),inference(fof_nnf,[status(thm)],[sequential_defn])).
% 0.46/0.62 fof(c52,plain,((![E1]:(![E2]:(~sequential(E1,E2)|(((edge(E1)&edge(E2))&E1!=E2)&head_of(E1)=tail_of(E2)))))&(![E1]:(![E2]:((((~edge(E1)|~edge(E2))|E1=E2)|head_of(E1)!=tail_of(E2))|sequential(E1,E2))))),inference(shift_quantors,[status(thm)],[c51])).
% 0.46/0.62 fof(c54,plain,(![X29]:(![X30]:(![X31]:(![X32]:((~sequential(X29,X30)|(((edge(X29)&edge(X30))&X29!=X30)&head_of(X29)=tail_of(X30)))&((((~edge(X31)|~edge(X32))|X31=X32)|head_of(X31)!=tail_of(X32))|sequential(X31,X32))))))),inference(shift_quantors,[status(thm)],[fof(c53,plain,((![X29]:(![X30]:(~sequential(X29,X30)|(((edge(X29)&edge(X30))&X29!=X30)&head_of(X29)=tail_of(X30)))))&(![X31]:(![X32]:((((~edge(X31)|~edge(X32))|X31=X32)|head_of(X31)!=tail_of(X32))|sequential(X31,X32))))),inference(variable_rename,[status(thm)],[c52])).])).
% 0.46/0.62 fof(c55,plain,(![X29]:(![X30]:(![X31]:(![X32]:(((((~sequential(X29,X30)|edge(X29))&(~sequential(X29,X30)|edge(X30)))&(~sequential(X29,X30)|X29!=X30))&(~sequential(X29,X30)|head_of(X29)=tail_of(X30)))&((((~edge(X31)|~edge(X32))|X31=X32)|head_of(X31)!=tail_of(X32))|sequential(X31,X32))))))),inference(distribute,[status(thm)],[c54])).
% 0.46/0.62 cnf(c60,plain,~edge(X215)|~edge(X216)|X215=X216|head_of(X215)!=tail_of(X216)|sequential(X215,X216),inference(split_conjunct,[status(thm)],[c55])).
% 0.46/0.62 cnf(c49,plain,~path(X212,X214,X211)|~on_path(X213,X211)|~on_path(X210,X211)|~sequential(X213,X210)|precedes(X213,X210,X211),inference(split_conjunct,[status(thm)],[c48])).
% 0.46/0.62 cnf(c41,plain,~path(X208,X207,X209)|~precedes(X205,X206,X209)|sequential(X205,X206)|sequential(X205,skolem0002(X209,X205,X206)),inference(split_conjunct,[status(thm)],[c37])).
% 0.46/0.62 cnf(c11,axiom,X203!=X199|X204!=X201|X202!=X200|~shortest_path(X203,X204,X202)|shortest_path(X199,X201,X200),theory(equality)).
% 0.46/0.62 cnf(c102,plain,~complete|~vertex(X197)|~vertex(X196)|X197=X196|edge(skolem0006(X197,X196)),inference(split_conjunct,[status(thm)],[c101])).
% 0.46/0.63 cnf(c66,plain,~path(X192,X194,X193)|~in_path(X195,X193)|on_path(skolem0003(X192,X194,X193,X195),X193),inference(split_conjunct,[status(thm)],[c64])).
% 0.46/0.63 cnf(c28,plain,~shortest_path(X191,X188,X190)|~path(X191,X188,X189)|less_or_equal(length_of(X190),length_of(X189)),inference(split_conjunct,[status(thm)],[c25])).
% 0.46/0.63 cnf(c12,axiom,X185!=X187|X186!=X184|~less_or_equal(X185,X186)|less_or_equal(X187,X184),theory(equality)).
% 0.46/0.63 cnf(c10,axiom,X182!=X178|X183!=X180|X181!=X179|~precedes(X182,X183,X181)|precedes(X178,X180,X179),theory(equality)).
% 0.46/0.63 cnf(c9,axiom,X175!=X177|X176!=X174|~sequential(X175,X176)|sequential(X177,X174),theory(equality)).
% 0.46/0.63 cnf(c83,plain,~path(X171,X173,X172)|X171=tail_of(skolem0004(X171,X173,X172)),inference(split_conjunct,[status(thm)],[c79])).
% 0.46/0.63 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)).
% 0.46/0.63 fof(c68,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])).
% 0.46/0.63 fof(c69,plain,(![X38]:(![X39]:(![X40]:(![X41]:((~path(X38,X39,X40)|~on_path(X41,X40))|((edge(X41)&in_path(head_of(X41),X40))&in_path(tail_of(X41),X40))))))),inference(variable_rename,[status(thm)],[c68])).
% 0.46/0.63 fof(c70,plain,(![X38]:(![X39]:(![X40]:(![X41]:((((~path(X38,X39,X40)|~on_path(X41,X40))|edge(X41))&((~path(X38,X39,X40)|~on_path(X41,X40))|in_path(head_of(X41),X40)))&((~path(X38,X39,X40)|~on_path(X41,X40))|in_path(tail_of(X41),X40))))))),inference(distribute,[status(thm)],[c69])).
% 0.46/0.63 cnf(c73,plain,~path(X169,X168,X170)|~on_path(X167,X170)|in_path(tail_of(X167),X170),inference(split_conjunct,[status(thm)],[c70])).
% 0.46/0.63 cnf(c72,plain,~path(X165,X164,X166)|~on_path(X163,X166)|in_path(head_of(X163),X166),inference(split_conjunct,[status(thm)],[c70])).
% 0.46/0.63 cnf(c19,plain,~shortest_path(X153,X154,X151)|~precedes(X150,X152,X151)|~precedes(X152,X150,X151),inference(split_conjunct,[status(thm)],[c17])).
% 0.46/0.63 cnf(c129,plain,~shortest_path(X159,X161,X162)|~precedes(X160,X160,X162),inference(factor,[status(thm)],[c19])).
% 0.46/0.63 cnf(c8,axiom,X156!=X158|X157!=X155|~in_path(X156,X157)|in_path(X158,X155),theory(equality)).
% 0.46/0.63 cnf(c2,axiom,X99!=X101|X100!=X98|path_cons(X99,X100)=path_cons(X101,X98),theory(equality)).
% 0.46/0.63 cnf(c125,plain,X145!=X146|path_cons(X145,X147)=path_cons(X146,X147),inference(resolution,[status(thm)],[c2, reflexivity])).
% 0.46/0.63 cnf(c124,plain,X143!=X142|path_cons(X143,X143)=path_cons(X142,X142),inference(factor,[status(thm)],[c2])).
% 0.46/0.63 cnf(c7,axiom,X139!=X141|X140!=X138|~on_path(X139,X140)|on_path(X141,X138),theory(equality)).
% 0.46/0.63 cnf(c39,plain,~path(X136,X135,X137)|~precedes(X133,X134,X137)|on_path(X134,X137),inference(split_conjunct,[status(thm)],[c37])).
% 0.46/0.63 cnf(c38,plain,~path(X131,X130,X132)|~precedes(X128,X129,X132)|on_path(X128,X132),inference(split_conjunct,[status(thm)],[c37])).
% 0.46/0.63 cnf(c82,plain,~path(X125,X127,X126)|edge(skolem0004(X125,X127,X126)),inference(split_conjunct,[status(thm)],[c79])).
% 0.46/0.63 cnf(c71,plain,~path(X123,X122,X124)|~on_path(X121,X124)|edge(X121),inference(split_conjunct,[status(thm)],[c70])).
% 0.46/0.63 cnf(c65,plain,~path(X117,X119,X118)|~in_path(X120,X118)|vertex(X120),inference(split_conjunct,[status(thm)],[c64])).
% 0.46/0.63 cnf(c6,axiom,X115!=X111|X116!=X113|X114!=X112|~path(X115,X116,X114)|path(X111,X113,X112),theory(equality)).
% 0.46/0.63 cnf(c59,plain,~sequential(X109,X110)|head_of(X109)=tail_of(X110),inference(split_conjunct,[status(thm)],[c55])).
% 0.46/0.63 cnf(c3,axiom,X106!=X107|length_of(X106)=length_of(X107),theory(equality)).
% 0.46/0.63 fof(no_loops,axiom,(![E]:(edge(E)=>head_of(E)!=tail_of(E))),file('/export/starexec/sandbox/benchmark/Axioms/GRA001+0.ax', no_loops)).
% 0.46/0.63 fof(c113,plain,(![E]:(~edge(E)|head_of(E)!=tail_of(E))),inference(fof_nnf,[status(thm)],[no_loops])).
% 0.46/0.63 fof(c114,plain,(![X57]:(~edge(X57)|head_of(X57)!=tail_of(X57))),inference(variable_rename,[status(thm)],[c113])).
% 0.46/0.63 cnf(c115,plain,~edge(X105)|head_of(X105)!=tail_of(X105),inference(split_conjunct,[status(thm)],[c114])).
% 0.46/0.63 cnf(c26,plain,~shortest_path(X104,X102,X103)|path(X104,X102,X103),inference(split_conjunct,[status(thm)],[c25])).
% 0.46/0.63 cnf(c5,axiom,X95!=X96|~vertex(X95)|vertex(X96),theory(equality)).
% 0.46/0.63 cnf(c4,axiom,X92!=X93|~edge(X92)|edge(X93),theory(equality)).
% 0.46/0.63 cnf(c1,axiom,X89!=X90|tail_of(X89)=tail_of(X90),theory(equality)).
% 0.46/0.63 cnf(c27,plain,~shortest_path(X88,X86,X87)|X88!=X86,inference(split_conjunct,[status(thm)],[c25])).
% 0.46/0.63 fof(edge_ends_are_vertices,axiom,(![E]:(edge(E)=>(vertex(head_of(E))&vertex(tail_of(E))))),file('/export/starexec/sandbox/benchmark/Axioms/GRA001+0.ax', edge_ends_are_vertices)).
% 0.46/0.63 fof(c108,plain,(![E]:(~edge(E)|(vertex(head_of(E))&vertex(tail_of(E))))),inference(fof_nnf,[status(thm)],[edge_ends_are_vertices])).
% 0.46/0.63 fof(c109,plain,(![X56]:(~edge(X56)|(vertex(head_of(X56))&vertex(tail_of(X56))))),inference(variable_rename,[status(thm)],[c108])).
% 0.46/0.63 fof(c110,plain,(![X56]:((~edge(X56)|vertex(head_of(X56)))&(~edge(X56)|vertex(tail_of(X56))))),inference(distribute,[status(thm)],[c109])).
% 0.46/0.63 cnf(c112,plain,~edge(X81)|vertex(tail_of(X81)),inference(split_conjunct,[status(thm)],[c110])).
% 0.46/0.63 cnf(c0,axiom,X79!=X80|head_of(X79)=head_of(X80),theory(equality)).
% 0.46/0.63 cnf(c111,plain,~edge(X78)|vertex(head_of(X78)),inference(split_conjunct,[status(thm)],[c110])).
% 0.46/0.63 cnf(c81,plain,~path(X75,X77,X76)|vertex(X77),inference(split_conjunct,[status(thm)],[c79])).
% 0.46/0.63 cnf(c80,plain,~path(X72,X74,X73)|vertex(X72),inference(split_conjunct,[status(thm)],[c79])).
% 0.46/0.63 cnf(c58,plain,~sequential(X69,X70)|X69!=X70,inference(split_conjunct,[status(thm)],[c55])).
% 0.46/0.63 cnf(c119,plain,~sequential(X71,X71),inference(resolution,[status(thm)],[c58, reflexivity])).
% 0.46/0.63 cnf(transitivity,axiom,X68!=X67|X67!=X66|X68=X66,theory(equality)).
% 0.46/0.63 cnf(symmetry,axiom,X64!=X63|X63=X64,theory(equality)).
% 0.46/0.63 cnf(c57,plain,~sequential(X61,X62)|edge(X62),inference(split_conjunct,[status(thm)],[c55])).
% 0.46/0.63 cnf(c56,plain,~sequential(X59,X60)|edge(X59),inference(split_conjunct,[status(thm)],[c55])).
% 0.46/0.63 % SZS output end Saturation
% 0.46/0.63
% 0.46/0.63 % Initial clauses : 61
% 0.46/0.63 % Processed clauses : 71
% 0.46/0.63 % Factors computed : 11
% 0.46/0.63 % Resolvents computed: 17
% 0.46/0.63 % Tautologies deleted: 4
% 0.46/0.63 % Forward subsumed : 14
% 0.46/0.63 % Backward subsumed : 0
% 0.46/0.63 % -------- CPU Time ---------
% 0.46/0.63 % User time : 0.256 s
% 0.46/0.63 % System time : 0.014 s
% 0.46/0.63 % Total time : 0.270 s
%------------------------------------------------------------------------------