IPTP solved : 209 (76.3%) proved : 127 refuted : 82 >600s: : 60 errors : 5 stack overflow : 4 too large,deep or complex: 1 test conditions: HP SD64000 64bit PA-RISC PA-8700 750MHz CPU HP-UX11i, 33 CPUs, time limit: 600 sec. 274 propositional problems (ILTP-Library v1.1.2) date: Jul 15 2006 ATP-system : IPTP authors : Alessandro Avellone, Guido Fiorino and Ugo Moscato version : programming language : C++ compiler : gcc 3.4.3 description : Parallel version of a duplication-free tableau calculus for propositional logic implemented in C++. Decision procedure for propositional problems. reference : A. Avellone, G. Fiorino, U. Moscato. A Parallel Implementation of a Decision Procedure for Propositional Intuitionistic Logic. TABLEAUX 2003 (Position Papers and Tutorials), Technical Report RT-DIA-80-2003, Dipartimento di Informatica e Automazione, Università degli Studi di Roma 3, pages 14-22, 2003. web-site : http://www.dimequant.unimib.it/ IPTP/ problem time in sec. LCL181+1 (0.12) LCL230+1 (0.08) SYN001+1 (0.09) SYN007+1.014 large SYN040+1 (0.10) SYN041+1 0.08 SYN044+1 0.09 SYN045+1 0.09 SYN046+1 (0.09) SYN047+1 (0.09) SYN387+1 (0.08) SYN388+1 (0.08) SYN389+1 (0.08) SYN390+1 0.11 SYN391+1 0.11 SYN392+1 (0.09) SYN393+1 (0.10) SYN416+1 (0.08) SYN915+1 0.14 SYN916+1 (0.12) SYN977+1 (0.08) SYN978+1 0.09 SYJ101+1 0.08 SYJ102+1 0.08 SYJ103+1 0.08 SYJ104+1 0.08 SYJ105+1.002 0.08 SYJ105+1.003 0.09 SYJ105+1.004 0.09 SYJ106+1 0.08 SYJ107+1.001 0.09 SYJ107+1.002 0.09 SYJ107+1.003 0.10 SYJ107+1.004 0.11 SYJ201+1.001 0.08 SYJ201+1.002 0.09 SYJ201+1.003 0.10 SYJ201+1.004 0.11 SYJ201+1.005 0.12 SYJ201+1.006 0.16 SYJ201+1.007 0.19 SYJ201+1.008 0.25 SYJ201+1.009 0.30 SYJ201+1.010 0.38 SYJ201+1.011 0.48 SYJ201+1.012 0.61 SYJ201+1.013 0.81 SYJ201+1.014 1.33 SYJ201+1.015 1.28 SYJ201+1.016 1.79 SYJ201+1.017 1.95 SYJ201+1.018 2.31 SYJ201+1.019 2.82 SYJ201+1.020 3.47 SYJ202+1.001 0.08 SYJ202+1.002 0.09 SYJ202+1.003 0.13 SYJ202+1.004 0.20 SYJ202+1.005 0.40 SYJ202+1.006 2.27 SYJ202+1.007 13.38 SYJ202+1.008 97.33 SYJ202+1.009 >600 SYJ202+1.010 >600 SYJ202+1.011 >600 SYJ202+1.012 >600 SYJ202+1.013 >600 SYJ202+1.014 >600 SYJ202+1.015 >600 SYJ202+1.016 >600 SYJ202+1.017 >600 SYJ202+1.018 >600 SYJ202+1.019 stack SYJ202+1.020 stack SYJ203+1.001 0.08 SYJ203+1.002 0.10 SYJ203+1.003 0.09 SYJ203+1.004 0.09 SYJ203+1.005 0.08 SYJ203+1.006 0.55 SYJ203+1.007 0.08 SYJ203+1.008 0.95 SYJ203+1.009 0.09 SYJ203+1.010 0.23 SYJ203+1.011 0.10 SYJ203+1.012 0.12 SYJ203+1.013 0.11 SYJ203+1.014 0.13 SYJ203+1.015 0.11 SYJ203+1.016 0.11 SYJ203+1.017 0.15 SYJ203+1.018 1.03 SYJ203+1.019 0.18 SYJ203+1.020 0.14 SYJ204+1.001 0.08 SYJ204+1.002 0.08 SYJ204+1.003 0.09 SYJ204+1.004 0.39 SYJ204+1.005 0.21 SYJ204+1.006 0.21 SYJ204+1.007 0.09 SYJ204+1.008 0.09 SYJ204+1.009 0.10 SYJ204+1.010 0.09 SYJ204+1.011 0.10 SYJ204+1.012 0.09 SYJ204+1.013 0.10 SYJ204+1.014 0.09 SYJ204+1.015 0.09 SYJ204+1.016 0.09 SYJ204+1.017 0.12 SYJ204+1.018 0.65 SYJ204+1.019 0.27 SYJ204+1.020 0.12 SYJ205+1.001 0.09 SYJ205+1.002 0.09 SYJ205+1.003 0.09 SYJ205+1.004 0.08 SYJ205+1.005 0.09 SYJ205+1.006 0.08 SYJ205+1.007 0.08 SYJ205+1.008 0.10 SYJ205+1.009 0.09 SYJ205+1.010 0.08 SYJ205+1.011 0.09 SYJ205+1.012 0.09 SYJ205+1.013 0.09 SYJ205+1.014 0.09 SYJ205+1.015 0.09 SYJ205+1.016 0.10 SYJ205+1.017 0.09 SYJ205+1.018 0.09 SYJ205+1.019 0.09 SYJ205+1.020 0.10 SYJ206+1.001 0.07 SYJ206+1.002 0.07 SYJ206+1.003 0.07 SYJ206+1.004 0.16 SYJ206+1.005 0.07 SYJ206+1.006 0.07 SYJ206+1.007 0.08 SYJ206+1.008 0.08 SYJ206+1.009 0.10 SYJ206+1.010 0.12 SYJ206+1.011 0.15 SYJ206+1.012 0.21 SYJ206+1.013 0.36 SYJ206+1.014 0.63 SYJ206+1.015 1.23 SYJ206+1.016 2.37 SYJ206+1.017 4.66 SYJ206+1.018 9.01 SYJ206+1.019 18.22 SYJ206+1.020 36.35 SYJ207+1.001 (0.38) SYJ207+1.002 (0.11) SYJ207+1.003 (5.71) SYJ207+1.004 >600 SYJ207+1.005 >600 SYJ207+1.006 >600 SYJ207+1.007 >600 SYJ207+1.008 >600 SYJ207+1.009 >600 SYJ207+1.010 >600 SYJ207+1.011 >600 SYJ207+1.012 >600 SYJ207+1.013 >600 SYJ207+1.014 >600 SYJ207+1.015 >600 SYJ207+1.016 >600 SYJ207+1.017 >600 SYJ207+1.018 >600 SYJ207+1.019 >600 SYJ207+1.020 >600 SYJ208+1.001 (0.08) SYJ208+1.002 (0.09) SYJ208+1.003 (0.15) SYJ208+1.004 (0.37) SYJ208+1.005 (0.40) SYJ208+1.006 (2.45) SYJ208+1.007 (22.59) SYJ208+1.008 (257.74) SYJ208+1.009 >600 SYJ208+1.010 >600 SYJ208+1.011 >600 SYJ208+1.012 >600 SYJ208+1.013 >600 SYJ208+1.014 >600 SYJ208+1.015 >600 SYJ208+1.016 >600 SYJ208+1.017 >600 SYJ208+1.018 >600 SYJ208+1.019 stack SYJ208+1.020 stack SYJ209+1.001 (0.08) SYJ209+1.002 (0.20) SYJ209+1.003 (0.20) SYJ209+1.004 (0.23) SYJ209+1.005 (0.57) SYJ209+1.006 (2.49) SYJ209+1.007 (15.02) SYJ209+1.008 (137.87) SYJ209+1.009 >600 SYJ209+1.010 >600 SYJ209+1.011 >600 SYJ209+1.012 >600 SYJ209+1.013 >600 SYJ209+1.014 >600 SYJ209+1.015 >600 SYJ209+1.016 >600 SYJ209+1.017 >600 SYJ209+1.018 >600 SYJ209+1.019 >600 SYJ209+1.020 >600 SYJ210+1.001 (0.07) SYJ210+1.002 (0.07) SYJ210+1.003 (0.07) SYJ210+1.004 (0.07) SYJ210+1.005 (0.07) SYJ210+1.006 (0.08) SYJ210+1.007 (0.07) SYJ210+1.008 (0.07) SYJ210+1.009 (0.08) SYJ210+1.010 (0.07) SYJ210+1.011 (0.07) SYJ210+1.012 (0.08) SYJ210+1.013 (0.07) SYJ210+1.014 (0.07) SYJ210+1.015 (0.07) SYJ210+1.016 (0.08) SYJ210+1.017 (0.08) SYJ210+1.018 (0.08) SYJ210+1.019 (0.08) SYJ210+1.020 (0.30) SYJ211+1.001 (0.07) SYJ211+1.002 (0.08) SYJ211+1.003 (0.08) SYJ211+1.004 (0.10) SYJ211+1.005 (0.14) SYJ211+1.006 (0.25) SYJ211+1.007 (0.48) SYJ211+1.008 (1.09) SYJ211+1.009 (1.81) SYJ211+1.010 (3.95) SYJ211+1.011 (7.54) SYJ211+1.012 (15.42) SYJ211+1.013 (31.54) SYJ211+1.014 (64.41) SYJ211+1.015 (130.76) SYJ211+1.016 (266.23) SYJ211+1.017 (541.59) SYJ211+1.018 >600 SYJ211+1.019 >600 SYJ211+1.020 >600 SYJ212+1.001 (0.09) SYJ212+1.002 (1.06) SYJ212+1.003 (0.11) SYJ212+1.004 (0.78) SYJ212+1.005 (0.24) SYJ212+1.006 (0.34) SYJ212+1.007 (4.33) SYJ212+1.008 (1.89) SYJ212+1.009 (15.27) SYJ212+1.010 (47.69) SYJ212+1.011 (188.05) SYJ212+1.012 (457.02) SYJ212+1.013 >600 SYJ212+1.014 >600 SYJ212+1.015 >600 SYJ212+1.016 >600 SYJ212+1.017 >600 SYJ212+1.018 >600 SYJ212+1.019 >600 SYJ212+1.020 >600 abbreviations: 123.45 - proved in 123.45 sec. (123.45) - refuted in 123.45 sec.