PITPINV solved : 262 (95.6%) proved : 128 refuted : 134 >600s: : 11 errors (too large input): 1 test conditions: Xeon 3.4 GHz, Mandrake 10.2, time limit: 600 sec. 274 propositional problems (ILTP-Library v1.1.2) date: 23 Jun 2007 ATP-system : PITPINV authors : Alessandro Avellone, Guido Fiorino and Ugo Moscato version : programming language : C++ compiler : g++ 3.4.3 description : Duplication-free tableau calculus for propositional logic implemented in C++. Decision procedure for propositional problems. This version implements the same FT search strategy, namely for the semi invertible rules the non invertible branch is the first to be visited. reference : Alessandro Avellone, Guido Fiorino, Ugo Moscato. A New o(n log n)-Space Decision Procedure for Propositional Intuitionistic Logic. Kurt Goedel Society Collegium Logicum, volume VIII, pages 17-33, 2004. web-site : http://www.dimequant.unimib.it/PITP problem time in sec. LCL181+1 (<0.01) LCL230+1 (<0.01) SYN001+1 (<0.01) SYN007+1.014 large SYN040+1 (<0.01) SYN041+1 <0.01 SYN044+1 <0.01 SYN045+1 <0.01 SYN046+1 (<0.01) SYN047+1 (<0.01) SYN387+1 (<0.01) SYN388+1 (<0.01) SYN389+1 (<0.01) SYN390+1 <0.01 SYN391+1 <0.01 SYN392+1 (<0.01) SYN393+1 (<0.01) SYN416+1 (<0.01) SYN915+1 <0.01 SYN916+1 (<0.01) SYN977+1 (<0.01) SYN978+1 <0.01 SYJ101+1 <0.01 SYJ102+1 <0.01 SYJ103+1 <0.01 SYJ104+1 <0.01 SYJ105+1.002 <0.01 SYJ105+1.003 <0.01 SYJ105+1.004 <0.01 SYJ106+1 <0.01 SYJ107+1.001 <0.01 SYJ107+1.002 <0.01 SYJ107+1.003 <0.01 SYJ107+1.004 <0.01 SYJ201+1.001 <0.01 SYJ201+1.002 <0.01 SYJ201+1.003 <0.01 SYJ201+1.004 <0.01 SYJ201+1.005 <0.01 SYJ201+1.006 <0.01 SYJ201+1.007 <0.01 SYJ201+1.008 <0.01 SYJ201+1.009 <0.01 SYJ201+1.010 <0.01 SYJ201+1.011 <0.01 SYJ201+1.012 0.01 SYJ201+1.013 <0.01 SYJ201+1.014 <0.01 SYJ201+1.015 0.01 SYJ201+1.016 0.01 SYJ201+1.017 0.01 SYJ201+1.018 0.01 SYJ201+1.019 0.01 SYJ201+1.020 0.01 SYJ202+1.001 <0.01 SYJ202+1.002 <0.01 SYJ202+1.003 <0.01 SYJ202+1.004 <0.01 SYJ202+1.005 <0.01 SYJ202+1.006 0.03 SYJ202+1.007 0.31 SYJ202+1.008 3.47 SYJ202+1.009 42.68 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 >600 SYJ202+1.020 >600 SYJ203+1.001 <0.01 SYJ203+1.002 <0.01 SYJ203+1.003 <0.01 SYJ203+1.004 <0.01 SYJ203+1.005 <0.01 SYJ203+1.006 <0.01 SYJ203+1.007 <0.01 SYJ203+1.008 <0.01 SYJ203+1.009 <0.01 SYJ203+1.010 <0.01 SYJ203+1.011 <0.01 SYJ203+1.012 <0.01 SYJ203+1.013 <0.01 SYJ203+1.014 <0.01 SYJ203+1.015 <0.01 SYJ203+1.016 <0.01 SYJ203+1.017 <0.01 SYJ203+1.018 <0.01 SYJ203+1.019 <0.01 SYJ203+1.020 <0.01 SYJ204+1.001 <0.01 SYJ204+1.002 <0.01 SYJ204+1.003 <0.01 SYJ204+1.004 <0.01 SYJ204+1.005 <0.01 SYJ204+1.006 <0.01 SYJ204+1.007 <0.01 SYJ204+1.008 <0.01 SYJ204+1.009 <0.01 SYJ204+1.010 <0.01 SYJ204+1.011 <0.01 SYJ204+1.012 <0.01 SYJ204+1.013 <0.01 SYJ204+1.014 <0.01 SYJ204+1.015 <0.01 SYJ204+1.016 <0.01 SYJ204+1.017 <0.01 SYJ204+1.018 <0.01 SYJ204+1.019 <0.01 SYJ204+1.020 <0.01 SYJ205+1.001 <0.01 SYJ205+1.002 <0.01 SYJ205+1.003 <0.01 SYJ205+1.004 <0.01 SYJ205+1.005 <0.01 SYJ205+1.006 <0.01 SYJ205+1.007 <0.01 SYJ205+1.008 <0.01 SYJ205+1.009 <0.01 SYJ205+1.010 0.02 SYJ205+1.011 0.04 SYJ205+1.012 0.08 SYJ205+1.013 0.17 SYJ205+1.014 0.38 SYJ205+1.015 0.82 SYJ205+1.016 1.73 SYJ205+1.017 3.58 SYJ205+1.018 7.49 SYJ205+1.019 15.89 SYJ205+1.020 33.45 SYJ206+1.001 <0.01 SYJ206+1.002 <0.01 SYJ206+1.003 <0.01 SYJ206+1.004 <0.01 SYJ206+1.005 <0.01 SYJ206+1.006 <0.01 SYJ206+1.007 <0.01 SYJ206+1.008 <0.01 SYJ206+1.009 <0.01 SYJ206+1.010 <0.01 SYJ206+1.011 <0.01 SYJ206+1.012 <0.01 SYJ206+1.013 0.02 SYJ206+1.014 0.05 SYJ206+1.015 0.10 SYJ206+1.016 0.23 SYJ206+1.017 0.47 SYJ206+1.018 0.96 SYJ206+1.019 1.93 SYJ206+1.020 3.89 SYJ207+1.001 (<0.01) SYJ207+1.002 (<0.01) SYJ207+1.003 (<0.01) SYJ207+1.004 (<0.01) SYJ207+1.005 (<0.01) SYJ207+1.006 (<0.01) SYJ207+1.007 (0.01) SYJ207+1.008 (0.03) SYJ207+1.009 (0.07) SYJ207+1.010 (0.15) SYJ207+1.011 (0.32) SYJ207+1.012 (0.71) SYJ207+1.013 (1.52) SYJ207+1.014 (3.31) SYJ207+1.015 (7.12) SYJ207+1.016 (15.19) SYJ207+1.017 (32.17) SYJ207+1.018 (68.71) SYJ207+1.019 (145.85) SYJ207+1.020 (305.21) SYJ208+1.001 (<0.01) SYJ208+1.002 (<0.01) SYJ208+1.003 (<0.01) SYJ208+1.004 (<0.01) SYJ208+1.005 (<0.01) SYJ208+1.006 (<0.01) SYJ208+1.007 (<0.01) SYJ208+1.008 (<0.01) SYJ208+1.009 (0.01) SYJ208+1.010 (0.04) SYJ208+1.011 (0.07) SYJ208+1.012 (0.09) SYJ208+1.013 (0.14) SYJ208+1.014 (0.23) SYJ208+1.015 (0.31) SYJ208+1.016 (0.47) SYJ208+1.017 (0.60) SYJ208+1.018 (0.95) SYJ208+1.019 (1.35) SYJ208+1.020 (1.80) SYJ209+1.001 (<0.01) SYJ209+1.002 (<0.01) SYJ209+1.003 (<0.01) SYJ209+1.004 (<0.01) SYJ209+1.005 (<0.01) SYJ209+1.006 (<0.01) SYJ209+1.007 (<0.01) SYJ209+1.008 (0.01) SYJ209+1.009 (0.01) SYJ209+1.010 (0.02) SYJ209+1.011 (0.06) SYJ209+1.012 (0.13) SYJ209+1.013 (0.29) SYJ209+1.014 (0.63) SYJ209+1.015 (1.33) SYJ209+1.016 (2.92) SYJ209+1.017 (6.32) SYJ209+1.018 (13.44) SYJ209+1.019 (28.68) SYJ209+1.020 (60.54) SYJ210+1.001 (<0.01) SYJ210+1.002 (<0.01) SYJ210+1.003 (<0.01) SYJ210+1.004 (<0.01) SYJ210+1.005 (<0.01) SYJ210+1.006 (<0.01) SYJ210+1.007 (<0.01) SYJ210+1.008 (<0.01) SYJ210+1.009 (<0.01) SYJ210+1.010 (<0.01) SYJ210+1.011 (<0.01) SYJ210+1.012 (<0.01) SYJ210+1.013 (<0.01) SYJ210+1.014 (<0.01) SYJ210+1.015 (<0.01) SYJ210+1.016 (<0.01) SYJ210+1.017 (<0.01) SYJ210+1.018 (<0.01) SYJ210+1.019 (<0.01) SYJ210+1.020 (<0.01) SYJ211+1.001 (<0.01) SYJ211+1.002 (<0.01) SYJ211+1.003 (<0.01) SYJ211+1.004 (<0.01) SYJ211+1.005 (<0.01) SYJ211+1.006 (<0.01) SYJ211+1.007 (<0.01) SYJ211+1.008 (0.01) SYJ211+1.009 (0.03) SYJ211+1.010 (0.07) SYJ211+1.011 (0.15) SYJ211+1.012 (0.33) SYJ211+1.013 (0.74) SYJ211+1.014 (1.54) SYJ211+1.015 (3.35) SYJ211+1.016 (7.07) SYJ211+1.017 (14.44) SYJ211+1.018 (31.51) SYJ211+1.019 (66.58) SYJ211+1.020 (139.67) SYJ212+1.001 (<0.01) SYJ212+1.002 (<0.01) SYJ212+1.003 (<0.01) SYJ212+1.004 (<0.01) SYJ212+1.005 (<0.01) SYJ212+1.006 (<0.01) SYJ212+1.007 (<0.01) SYJ212+1.008 (<0.01) SYJ212+1.009 (<0.01) SYJ212+1.010 (<0.01) SYJ212+1.011 (0.01) SYJ212+1.012 (<0.01) SYJ212+1.013 (0.03) SYJ212+1.014 (0.07) SYJ212+1.015 (0.15) SYJ212+1.016 (0.31) SYJ212+1.017 (0.69) SYJ212+1.018 (1.37) SYJ212+1.019 (2.75) SYJ212+1.020 (5.51) abbreviations: 123.45 - proved in 123.45 sec. (123.45) - refuted in 123.45 sec. large - input formula too large