[] = """Euler-1.3.9 8 Aug 2005 20:53:00 GMT ----- Prover9 July-2005C, 7 July 2005 ----- Process 3344 was started by amdus on vam1627, Mon Aug 8 22:53:00 2005 The command was "prover9 -f C:\DOCUME~1\amdus.BE\LOCALS~1\Temp\prover9.in". % Reading from file C:\DOCUME~1\amdus.BE\LOCALS~1\Temp\prover9.in set(auto). % set(auto) -> set(auto1). % set(auto1) -> set(auto_inference). % set(auto1) -> set(fof_reduction). % set(auto1) -> set(predicate_elimination). % set(auto1) -> set(unfold_eq). % set(unfold_eq) -> assign(unfold_eq_limit, 2147483647). % set(unfold_eq) -> clear(fold_eq). % set(auto1) -> set(inverse_order). % set(auto1) -> assign(new_constants, 1). % assign(new_constants, 1) -> clear(x_proofs). % assign(new_constants, 1) -> clear(rx_proofs). % set(auto1) -> assign(lex_dep_demod_lim, 11). % set(auto1) -> set(lex_dep_demod_sane). % set(auto1) -> assign(max_weight, 100). % set(auto1) -> assign(age_part, 1). % set(auto1) -> assign(weight_part, 2). % set(auto1) -> assign(weight_neg_part, 2). % set(auto1) -> assign(sos_limit, 10000). % set(auto1) -> clear(x_proofs). % set(auto1) -> assign(stats, lots). % set(auto1) -> assign(max_megs, 200). % set(auto1) -> clear(clocks). assign(sos_limit,100000). assign(max_megs,800). set(quiet). clear(print_initial_clauses). clear(print_given). clauses(sos). qname("e:") = iri("http://eulersharp.sourceforge.net/2003/03swap/log-rules#"). qname("q:") = iri("http://www.w3.org/2004/ql#"). qname("g:") = iri("http://www.agfa.com/w3c/euler/graph#"). qname("rdfs:") = iri("http://www.w3.org/2000/01/rdf-schema#"). qname("log:") = iri("http://www.w3.org/2000/10/swap/log#"). qname("owl:") = iri("http://www.w3.org/2002/07/owl#"). qname("rdf:") = iri("http://www.w3.org/1999/02/22-rdf-syntax-ns#"). qname("g:path") = qname("g:route"). qname("g:parijs") = qname("g:paris"). triple(qname("g:paris"),qname("g:twoway"),qname("g:orleans")). triple(qname("g:paris"),qname("g:twoway"),qname("g:chartres")). triple(qname("g:parijs"),qname("g:twoway"),qname("g:amiens")). triple(qname("g:orleans"),qname("g:twoway"),qname("g:blois")). triple(qname("g:orleans"),qname("g:twoway"),qname("g:bourges")). triple(qname("g:blois"),qname("g:twoway"),qname("g:tours")). triple(qname("g:chartres"),qname("g:twoway"),qname("g:lemans")). triple(qname("g:lemans"),qname("g:twoway"),qname("g:angers")). triple(qname("g:lemans"),qname("g:twoway"),qname("g:tours")). triple(qname("g:angers"),qname("g:oneway"),qname("g:nantes")). triple(qname("g:oneway"),qname("rdfs:subPropertyOf"),qname("g:path")). triple(qname("g:twoway"),qname("rdfs:subPropertyOf"),qname("g:oneway")). triple(qname("g:twoway"),qname("rdf:type"),qname("owl:SymmetricProperty")). triple(qname("g:path"),qname("rdf:type"),qname("owl:TransitiveProperty")). - triple(x,qname("rdfs:subPropertyOf"),y) | - triple(z,x,u) | triple(z,y,u). - triple(x,qname("rdf:type"),qname("owl:SymmetricProperty")) | - triple(y,x,z) | triple(z,x,y). - triple(x,qname("rdf:type"),qname("owl:TransitiveProperty")) | - triple(y,x,z) | - triple(u,x,y) | triple(u,x,z). - triple(qname("g:parijs"),qname("g:route"),qname("g:nantes")) | triple(qname("e:quod"),qname("e:erat"),qname("e:demonstrandum")). triple(skf_e136_0_,qname("e:hint"),"assign%28sos_limit%2C100000%29.assign%28max_megs%2C800%29.set%28quiet%29.clear%28print_initial_clauses%29.clear%28print_given%29."). - triple(qname("e:quod"),qname("e:erat"),qname("e:demonstrandum")). end_of_list. % Finished reading the input. % Entering prover search function. % Assigned IDs to 29 clauses. % Starting search at 0.03 seconds. -------- Proof 1 -------- (0.04 + 0.00 seconds) -------- PROOF -------- Length of proof is 29. Maximum clause weight is 18. 8 qname("g:path") = qname("g:route"). [input] 9 qname("g:parijs") = qname("g:paris"). [input] 11 triple(qname("g:paris"),qname("g:twoway"),qname("g:chartres")). [input] 27 - triple(qname("g:parijs"),qname("g:route"),qname("g:nantes")) | triple(qname("e:quod"),qname("e:erat"),qname("e:demonstrandum")). [input] 37 qname("g:route") = qname("g:path"). [copy 8 flip a] 38 qname("g:paris") = qname("g:parijs"). [copy 9 flip a] 40 triple(qname("g:parijs"),qname("g:twoway"),qname("g:chartres")). [copy 11 demod (38)] 45 triple(qname("g:chartres"),qname("g:twoway"),qname("g:lemans")). [input] 46 triple(qname("g:lemans"),qname("g:twoway"),qname("g:angers")). [input] 48 triple(qname("g:angers"),qname("g:oneway"),qname("g:nantes")). [input] 49 triple(qname("g:oneway"),qname("rdfs:subPropertyOf"),qname("g:path")). [input] 50 triple(qname("g:twoway"),qname("rdfs:subPropertyOf"),qname("g:oneway")). [input] 52 triple(qname("g:path"),qname("rdf:type"),qname("owl:TransitiveProperty")). [input] 53 - triple(x,qname("rdfs:subPropertyOf"),y) | - triple(z,x,u) | triple(z,y,u). [input] 55 - triple(x,qname("rdf:type"),qname("owl:TransitiveProperty")) | - triple(y,x,z) | - triple(u,x,y) | triple(u,x,z). [input] 56 - triple(qname("g:parijs"),qname("g:path"),qname("g:nantes")) | triple(qname("e:quod"),qname("e:erat"),qname("e:demonstrandum")). [copy 27 demod (37)] 58 - triple(qname("e:quod"),qname("e:erat"),qname("e:demonstrandum")). [input] 60 triple(qname("g:lemans"),qname("g:oneway"),qname("g:angers")). [hyper (53 a 50 a b 46 a)] 61 triple(qname("g:chartres"),qname("g:oneway"),qname("g:lemans")). [hyper (53 a 50 a b 45 a)] 66 triple(qname("g:parijs"),qname("g:oneway"),qname("g:chartres")). [hyper (53 a 50 a b 40 a)] 68 triple(qname("g:angers"),qname("g:path"),qname("g:nantes")). [hyper (53 a 49 a b 48 a)] 78 - triple(qname("g:parijs"),qname("g:path"),qname("g:nantes")). [ur (56 b 58 a)] 80 triple(qname("g:lemans"),qname("g:path"),qname("g:angers")). [hyper (53 a 49 a b 60 a)] 83 triple(qname("g:chartres"),qname("g:path"),qname("g:lemans")). [hyper (53 a 49 a b 61 a)] 89 triple(qname("g:parijs"),qname("g:path"),qname("g:chartres")). [hyper (53 a 49 a b 66 a)] 91 - triple(qname("g:parijs"),qname("g:path"),qname("g:angers")). [ur (55 a 52 a b 68 a d 78 a)] 105 - triple(qname("g:parijs"),qname("g:path"),qname("g:lemans")). [ur (55 a 52 a b 80 a d 91 a)] 108 - triple(qname("g:parijs"),qname("g:path"),qname("g:chartres")). [ur (55 a 52 a b 83 a d 105 a)] 109 $F. [resolve (108 a 89 a)] -------- end of proof ------- Given=62. Generated=99. Kept=79. Proofs=1. Usable=61. Sos=16. Demods=9. Goals=0. Limbo=0, Disabled=30. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=20. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=9 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=662. Demod_rewrites=3. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=5. Megabytes=0.08. User_CPU=0.04, System_CPU=0.00, Wall_clock=0. THEOREM PROVED Exiting with 1 proof. Process 3344 exit (max_proofs) Mon Aug 8 22:53:00 2005 """.