> ./leo s4/SYM/SYM001+1 LEO-II: read-problem-file s4/SYM/SYM001+1 . LEO-II: prove-with-fo-atp e LEO II: timeout set (600 seconds). ........ LEO-II tries to prove the following (sub)problems. (0) Problem: % Problem related to split clause no. 10 thf(tp_meq_prop,type,(meq_prop: (($i>$o)>(($i>$o)>($i>$o))))). thf(tp_mweakly_dense,type,(mweakly_dense: (($i>($i>$o))>$o))). thf(tp_mweakly_directed,type,(mweakly_directed: (($i>($i>$o))>$o))). thf(tp_f,type,(f: (mu>($i>$o)))). thf(tp_minvalid,type,(minvalid: (($i>$o)>$o))). thf(tp_mreflexive,type,(mreflexive: (($i>($i>$o))>$o))). thf(tp_mequiv,type,(mequiv: (($i>$o)>(($i>$o)>($i>$o))))). thf(tp_rel_s4,type,(rel_s4: ($i>($i>$o)))). thf(tp_msymmetric,type,(msymmetric: (($i>($i>$o))>$o))). thf(tp_mor,type,(mor: (($i>$o)>(($i>$o)>($i>$o))))). thf(tp_mfunctional,type,(mfunctional: (($i>($i>$o))>$o))). thf(tp_mweakly_connected,type,(mweakly_connected: (($i>($i>$o))>$o))). thf(tp_mnot,type,(mnot: (($i>$o)>($i>$o)))). thf(tp_mexists_prop,type,(mexists_prop: ((($i>$o)>($i>$o))>($i>$o)))). thf(tp_mimplied,type,(mimplied: (($i>$o)>(($i>$o)>($i>$o))))). thf(tp_mbox,type,(mbox: (($i>($i>$o))>(($i>$o)>($i>$o))))). thf(tp_mforall_ind,type,(mforall_ind: ((mu>($i>$o))>($i>$o)))). thf(tp_mcountersatisfiable,type,(mcountersatisfiable: (($i>$o)>$o))). thf(tp_meq_ind,type,(meq_ind: (mu>(mu>($i>$o))))). thf(tp_mtrue,type,(mtrue: ($i>$o))). thf(tp_mand,type,(mand: (($i>$o)>(($i>$o)>($i>$o))))). thf(tp_mdia_s4,type,(mdia_s4: (($i>$o)>($i>$o)))). thf(tp_mxor,type,(mxor: (($i>$o)>(($i>$o)>($i>$o))))). thf(tp_mu,type,(mu: tType)). thf(tp_mpartially_functional,type,(mpartially_functional: (($i>($i>$o))>$o))). thf(tp_mvalid,type,(mvalid: (($i>$o)>$o))). thf(tp_msatisfiable,type,(msatisfiable: (($i>$o)>$o))). thf(tp_sK3,type,(sK3: mu)). thf(tp_mdia,type,(mdia: (($i>($i>$o))>(($i>$o)>($i>$o))))). thf(tp_mserial,type,(mserial: (($i>($i>$o))>$o))). thf(tp_sK2,type,(sK2: $i)). thf(tp_mfalse,type,(mfalse: ($i>$o))). thf(tp_mexists_ind,type,(mexists_ind: ((mu>($i>$o))>($i>$o)))). thf(tp_mtransitive,type,(mtransitive: (($i>($i>$o))>$o))). thf(tp_meuclidean,type,(meuclidean: (($i>($i>$o))>$o))). thf(tp_mbox_s4,type,(mbox_s4: (($i>$o)>($i>$o)))). thf(tp_sK1,type,(sK1: $i)). thf(tp_mimplies,type,(mimplies: (($i>$o)>(($i>$o)>($i>$o))))). thf(tp_mforall_prop,type,(mforall_prop: ((($i>$o)>($i>$o))>($i>$o)))). thf(a11,axiom,(![SY40:$i,SY41:$i,SY42:$i]: (((~ ((rel_s4@SY40)@SY41)) | (~ ((rel_s4@SY41)@SY42))) | ((rel_s4@SY40)@SY42)))). thf(a7,axiom,(![SY46:$i]: ((rel_s4@SY46)@SY46))). thf(c10,negated_conjecture,((![SY48:mu,SY49:$i]: ((~ ((rel_s4@sK1)@SY49)) | ((f@SY48)@SY49))) & (((rel_s4@sK1)@sK2) & (~ ((f@sK3)@sK2))))). *** Trying Problem: 0 [Unidepth=8]... *** ATPs configured.[E:30s] *** Eureka --- Thanks to Corina --- Subproblem solved. An empty clause is: 39 Flag flag-write_fo-like-clauses is not set. No FO-like clauses file written! ******************************** * All subproblems solved!!! * ******************************** % SZS status Theorem for s4/SYM/SYM001+1 (rf:0,ps:3,sos:true,u:8,ude:true) %**** Solved all splitted subproblems! Generating the combined proof object **** %**** Beginning of derivation protocol in tstp **** Clause has not been found in protocol. You may have deactivated the proof output. Try command flag-proof-output or option --proofoutput to activate proof output. %**** End of derivation protocol in tstp **** %**** no. of clauses in derivation: 0 **** ******************************** * All subproblems solved!!! * ******************************** % SZS status Theorem for s4/SYM/SYM001+1 (rf:0,ps:3,sos:true,u:8,ude:true) 0.020: Total Reasoning Time (s4/SYM/SYM001+1) 0.015: s4/SYM/SYM001+1(atp-loop-0) >