ILTP-v1.1.2-prop-comparison --------------------------- ft ljt strip pitp Prolog C solved 188 199 175 202 238 (%) 68.6 72.6 63.9 73.7 86.9 proved 104 106 108 119 128 refuted 84 93 67 83 110 classic. invalid 1 1 1 1 1 int. not class. inv. 83 92 66 82 109 status unknown 0 0 0 0 0 solved after 0 - 1 s 173 185 166 178 215 1 - 10 s 5 6 4 11 15 10- 100s 6 7 2 11 6 100-600s 4 1 3 2 2 time out >600s 86 75 47 43 35 average time (*) 4.59 0.82 4.56 0.97 1.44 intuit. rating 0.00 159 160 160 160 160 0.01..0.33 22 23 9 32 32 0.34..0.67 5 14 6 10 30 0.68..1.00 2 2 0 0 16 solved only by this prover (logic-spec.) 0 0 0 0 16 errors 0 0 52 29 1 stack overflow 0 0 52 28 0 memory allocation 0 0 0 1 0 not representable 0 0 0 0 1 (*) computed only for formulas that were solved by all intuit. provers (58.0% of all formulas) solved proved refuted total LCL SYN SYJ total LCL SYN SYJ total LCL SYN SYJ ---------------------------------------------------------------------- ft Prolog 188 2 20 166 104 0 7 97 84 2 13 69 ft C 199 2 20 177 106 0 7 99 93 2 13 78 ljt 175 2 19 154 108 0 7 101 67 2 12 53 strip 202 2 19 181 119 0 7 112 83 2 12 69 pitp 238 2 19 217 128 0 7 121 110 2 12 96 test conditions: 274 propositional formulas time limit: 600 sec., Xeon 3.4 GHz, Mandrake 10.2 date: 1 Mar 2007 problem ft ljt strip pitp Prolog C LCL181+1 (<0.01) (<0.01) (<0.01) (0.35) (<0.01) LCL230+1 (<0.01) (<0.01) (<0.01) (0.04) (<0.01) SYN001+1 (<0.01) (<0.01) (<0.01) (0.05) (<0.01) SYN007+1.014 (<0.01) (<0.01) stack mem large SYN040+1 (<0.01) (<0.01) (<0.01) (0.05) (<0.01) SYN041+1 <0.01 <0.01 <0.01 0.03 <0.01 SYN044+1 <0.01 <0.01 <0.01 0.03 <0.01 SYN045+1 <0.01 <0.01 <0.01 0.03 <0.01 SYN046+1 (<0.01) (<0.01) (<0.01) (0.03) (<0.01) SYN047+1 (<0.01) (<0.01) (<0.01) (0.03) (<0.01) SYN387+1 (<0.01) (<0.01) (<0.01) (0.03) (<0.01) SYN388+1 (<0.01) (<0.01) (<0.01) (0.03) (<0.01) SYN389+1 (<0.01) (<0.01) (<0.01) (0.03) (<0.01) SYN390+1 <0.01 <0.01 <0.01 0.03 <0.01 SYN391+1 <0.01 <0.01 <0.01 0.04 <0.01 SYN392+1 (<0.01) (<0.01) (<0.01) (0.04) (<0.01) SYN393+1 (<0.01) (<0.01) (<0.01) (0.03) (<0.01) SYN416+1 (<0.01) (<0.01) (<0.01) (0.03) (<0.01) SYN915+1 <0.01 <0.01 <0.01 0.06 <0.01 SYN916+1 (<0.01) (<0.01) (<0.01) (0.03) (<0.01) SYN977+1 (<0.01) (<0.01) (<0.01) (0.02) (<0.01) SYN978+1 <0.01 <0.01 <0.01 0.01 <0.01 SYJ101+1 <0.01 <0.01 <0.01 0.04 <0.01 SYJ102+1 <0.01 <0.01 <0.01 0.04 <0.01 SYJ103+1 <0.01 <0.01 <0.01 0.03 <0.01 SYJ104+1 <0.01 <0.01 <0.01 0.03 <0.01 SYJ105+1.002 <0.01 <0.01 <0.01 0.03 <0.01 SYJ105+1.003 <0.01 <0.01 <0.01 0.03 <0.01 SYJ105+1.004 <0.01 <0.01 <0.01 0.03 <0.01 SYJ106+1 <0.01 <0.01 <0.01 0.03 <0.01 SYJ107+1.001 <0.01 <0.01 <0.01 0.03 <0.01 SYJ107+1.002 <0.01 <0.01 <0.01 0.03 <0.01 SYJ107+1.003 <0.01 <0.01 <0.01 0.03 <0.01 SYJ107+1.004 <0.01 <0.01 <0.01 0.04 <0.01 SYJ201+1.001 <0.01 <0.01 <0.01 0.04 <0.01 SYJ201+1.002 <0.01 <0.01 <0.01 0.04 <0.01 SYJ201+1.003 <0.01 <0.01 0.01 0.04 <0.01 SYJ201+1.004 <0.01 <0.01 0.01 0.04 <0.01 SYJ201+1.005 <0.01 <0.01 0.01 0.04 <0.01 SYJ201+1.006 0.01 <0.01 0.02 0.06 <0.01 SYJ201+1.007 0.01 <0.01 0.02 0.05 <0.01 SYJ201+1.008 0.03 <0.01 0.04 0.05 <0.01 SYJ201+1.009 0.03 <0.01 0.06 0.07 <0.01 SYJ201+1.010 0.03 0.01 0.08 0.08 <0.01 SYJ201+1.011 0.05 0.01 0.10 0.10 <0.01 SYJ201+1.012 0.07 0.01 0.12 0.12 <0.01 SYJ201+1.013 0.09 0.01 0.16 0.16 0.01 SYJ201+1.014 0.11 0.02 0.21 0.20 0.01 SYJ201+1.015 0.14 0.02 0.25 0.23 0.01 SYJ201+1.016 0.19 0.02 0.29 0.28 0.01 SYJ201+1.017 0.25 0.03 0.35 0.35 0.01 SYJ201+1.018 0.28 0.04 0.40 0.45 0.01 SYJ201+1.019 0.36 0.04 0.47 0.49 0.01 SYJ201+1.020 0.37 0.05 0.55 0.60 0.01 SYJ202+1.001 <0.01 <0.01 <0.01 0.05 <0.01 SYJ202+1.002 <0.01 <0.01 <0.01 0.04 <0.01 SYJ202+1.003 <0.01 <0.01 <0.01 0.05 <0.01 SYJ202+1.004 0.02 <0.01 0.09 0.09 <0.01 SYJ202+1.005 0.61 0.03 stack 0.44 <0.01 SYJ202+1.006 15.98 0.48 stack 11.28 0.04 SYJ202+1.007 516.55 76.30 stack stack 0.34 SYJ202+1.008 >600 >600 stack stack 3.85 SYJ202+1.009 >600 >600 stack stack 50.25 SYJ202+1.010 >600 >600 stack stack >600 SYJ202+1.011 >600 >600 stack stack >600 SYJ202+1.012 >600 >600 stack stack >600 SYJ202+1.013 >600 >600 stack stack >600 SYJ202+1.014 >600 >600 stack stack >600 SYJ202+1.015 >600 >600 stack stack >600 SYJ202+1.016 >600 >600 stack stack >600 SYJ202+1.017 >600 >600 stack stack >600 SYJ202+1.018 >600 >600 stack stack >600 SYJ202+1.019 >600 >600 stack stack >600 SYJ202+1.020 >600 >600 stack stack >600 SYJ203+1.001 <0.01 <0.01 <0.01 0.04 <0.01 SYJ203+1.002 <0.01 <0.01 <0.01 0.04 <0.01 SYJ203+1.003 <0.01 <0.01 <0.01 0.04 <0.01 SYJ203+1.004 <0.01 <0.01 <0.01 0.04 <0.01 SYJ203+1.005 <0.01 <0.01 <0.01 0.04 <0.01 SYJ203+1.006 <0.01 <0.01 <0.01 0.04 <0.01 SYJ203+1.007 <0.01 <0.01 <0.01 0.04 <0.01 SYJ203+1.008 <0.01 <0.01 <0.01 0.05 <0.01 SYJ203+1.009 <0.01 <0.01 <0.01 0.04 <0.01 SYJ203+1.010 <0.01 <0.01 <0.01 0.04 <0.01 SYJ203+1.011 <0.01 <0.01 <0.01 0.04 <0.01 SYJ203+1.012 <0.01 <0.01 <0.01 0.04 <0.01 SYJ203+1.013 <0.01 <0.01 <0.01 0.04 <0.01 SYJ203+1.014 <0.01 <0.01 <0.01 0.06 <0.01 SYJ203+1.015 <0.01 <0.01 <0.01 0.04 <0.01 SYJ203+1.016 <0.01 <0.01 <0.01 0.04 <0.01 SYJ203+1.017 <0.01 <0.01 <0.01 0.04 <0.01 SYJ203+1.018 <0.01 <0.01 <0.01 0.04 <0.01 SYJ203+1.019 <0.01 <0.01 <0.01 0.04 <0.01 SYJ203+1.020 <0.01 <0.01 <0.01 0.04 <0.01 SYJ204+1.001 <0.01 <0.01 <0.01 0.04 <0.01 SYJ204+1.002 <0.01 <0.01 <0.01 0.03 <0.01 SYJ204+1.003 <0.01 <0.01 <0.01 0.03 <0.01 SYJ204+1.004 <0.01 <0.01 <0.01 0.10 <0.01 SYJ204+1.005 <0.01 <0.01 <0.01 0.04 <0.01 SYJ204+1.006 <0.01 <0.01 <0.01 0.03 <0.01 SYJ204+1.007 <0.01 <0.01 <0.01 0.04 <0.01 SYJ204+1.008 <0.01 <0.01 0.01 0.04 <0.01 SYJ204+1.009 <0.01 <0.01 <0.01 0.03 <0.01 SYJ204+1.010 <0.01 <0.01 <0.01 0.03 <0.01 SYJ204+1.011 <0.01 <0.01 <0.01 0.04 <0.01 SYJ204+1.012 <0.01 <0.01 <0.01 0.03 <0.01 SYJ204+1.013 <0.01 <0.01 <0.01 0.03 <0.01 SYJ204+1.014 <0.01 <0.01 <0.01 0.03 <0.01 SYJ204+1.015 <0.01 <0.01 <0.01 0.03 <0.01 SYJ204+1.016 <0.01 <0.01 <0.01 0.03 <0.01 SYJ204+1.017 <0.01 <0.01 <0.01 0.04 <0.01 SYJ204+1.018 <0.01 <0.01 <0.01 0.04 <0.01 SYJ204+1.019 <0.01 <0.01 <0.01 0.04 <0.01 SYJ204+1.020 <0.01 <0.01 <0.01 0.03 <0.01 SYJ205+1.001 <0.01 <0.01 <0.01 0.05 <0.01 SYJ205+1.002 <0.01 <0.01 <0.01 0.05 <0.01 SYJ205+1.003 <0.01 <0.01 <0.01 0.04 <0.01 SYJ205+1.004 0.01 <0.01 <0.01 0.04 <0.01 SYJ205+1.005 0.05 <0.01 <0.01 0.04 <0.01 SYJ205+1.006 0.43 0.05 0.01 0.04 <0.01 SYJ205+1.007 4.66 0.58 <0.01 0.05 <0.01 SYJ205+1.008 60.26 6.69 <0.01 0.07 <0.01 SYJ205+1.009 >600 85.84 <0.01 0.24 <0.01 SYJ205+1.010 >600 >600 <0.01 0.69 <0.01 SYJ205+1.011 >600 >600 0.01 3.02 <0.01 SYJ205+1.012 >600 >600 <0.01 13.26 <0.01 SYJ205+1.013 >600 >600 <0.01 58.73 <0.01 SYJ205+1.014 >600 >600 0.01 267.39 <0.01 SYJ205+1.015 >600 >600 <0.01 >600 <0.01 SYJ205+1.016 >600 >600 <0.01 >600 <0.01 SYJ205+1.017 >600 >600 <0.01 >600 <0.01 SYJ205+1.018 >600 >600 0.01 >600 <0.01 SYJ205+1.019 >600 >600 <0.01 >600 <0.01 SYJ205+1.020 >600 >600 0.01 >600 <0.01 SYJ206+1.001 <0.01 <0.01 <0.01 0.09 <0.01 SYJ206+1.002 <0.01 <0.01 <0.01 0.04 <0.01 SYJ206+1.003 <0.01 <0.01 <0.01 0.03 <0.01 SYJ206+1.004 <0.01 <0.01 <0.01 0.04 <0.01 SYJ206+1.005 0.01 <0.01 0.01 0.03 <0.01 SYJ206+1.006 0.01 <0.01 >600 0.03 <0.01 SYJ206+1.007 0.04 0.01 >600 0.04 <0.01 SYJ206+1.008 0.51 0.08 >600 0.04 <0.01 SYJ206+1.009 7.36 1.07 >600 0.05 <0.01 SYJ206+1.010 144.50 20.02 >600 0.07 <0.01 SYJ206+1.011 >600 481.98 stack 0.11 <0.01 SYJ206+1.012 >600 >600 stack 0.26 <0.01 SYJ206+1.013 >600 >600 stack 0.38 0.01 SYJ206+1.014 >600 >600 stack 0.64 0.05 SYJ206+1.015 >600 >600 stack 1.47 0.11 SYJ206+1.016 >600 >600 stack 2.61 0.22 SYJ206+1.017 >600 >600 stack 5.37 0.52 SYJ206+1.018 >600 >600 stack 10.93 1.01 SYJ206+1.019 >600 >600 stack 18.29 1.95 SYJ206+1.020 >600 >600 stack 37.64 3.92 SYJ207+1.001 (<0.01) (<0.01) (<0.01) (0.05) (<0.01) SYJ207+1.002 (<0.01) (<0.01) (0.02) (0.04) (<0.01) SYJ207+1.003 (0.01) (<0.01) (2.64) (0.10) (<0.01) SYJ207+1.004 (0.09) (0.01) >600 (9.30) (0.15) SYJ207+1.005 (1.30) (0.20) >600 >600 (2.63) SYJ207+1.006 (20.41) (3.10) >600 >600 (68.50) SYJ207+1.007 (358.05) (51.13) >600 >600 >600 SYJ207+1.008 >600 >600 >600 >600 >600 SYJ207+1.009 >600 >600 >600 >600 >600 SYJ207+1.010 >600 >600 >600 >600 >600 SYJ207+1.011 >600 >600 >600 >600 >600 SYJ207+1.012 >600 >600 >600 >600 >600 SYJ207+1.013 >600 >600 >600 >600 >600 SYJ207+1.014 >600 >600 >600 >600 >600 SYJ207+1.015 >600 >600 >600 >600 >600 SYJ207+1.016 >600 >600 >600 >600 >600 SYJ207+1.017 >600 >600 >600 >600 >600 SYJ207+1.018 >600 >600 >600 >600 >600 SYJ207+1.019 >600 >600 >600 >600 >600 SYJ207+1.020 >600 >600 >600 >600 >600 SYJ208+1.001 (<0.01) (<0.01) (<0.01) (0.04) (<0.01) SYJ208+1.002 (<0.01) (<0.01) (<0.01) (0.04) (<0.01) SYJ208+1.003 (<0.01) (<0.01) (<0.01) (0.04) (<0.01) SYJ208+1.004 (<0.01) (<0.01) (0.01) (0.05) (<0.01) SYJ208+1.005 (0.01) (<0.01) (0.18) (0.07) (<0.01) SYJ208+1.006 (0.18) (<0.01) stack (0.24) (<0.01) SYJ208+1.007 (3.18) (<0.01) stack stack (0.01) SYJ208+1.008 (65.41) (0.01) stack stack (0.01) SYJ208+1.009 >600 (0.01) stack stack (0.02) SYJ208+1.010 >600 (0.03) stack stack (0.03) SYJ208+1.011 >600 (0.07) stack stack (0.07) SYJ208+1.012 >600 (0.16) stack stack (0.09) SYJ208+1.013 >600 (0.41) stack stack (0.14) SYJ208+1.014 >600 (0.84) stack stack (0.24) SYJ208+1.015 >600 (1.90) stack stack (0.34) SYJ208+1.016 >600 (4.53) stack stack (0.49) SYJ208+1.017 >600 (81.41) stack stack (0.64) SYJ208+1.018 >600 >600 stack stack (0.99) SYJ208+1.019 >600 >600 stack stack (1.36) SYJ208+1.020 >600 >600 stack stack (1.76) SYJ209+1.001 (<0.01) (<0.01) (<0.01) (0.04) (<0.01) SYJ209+1.002 (<0.01) (<0.01) (<0.01) (0.07) (<0.01) SYJ209+1.003 (<0.01) (<0.01) (<0.01) (0.04) (<0.01) SYJ209+1.004 (<0.01) (<0.01) (<0.01) (0.04) (<0.01) SYJ209+1.005 (0.01) (<0.01) (0.01) (0.04) (<0.01) SYJ209+1.006 (0.07) (0.01) (0.06) (0.05) (0.02) SYJ209+1.007 (0.45) (0.09) (0.54) (0.15) (0.22) SYJ209+1.008 (4.36) (0.80) (4.58) (1.14) (2.02) SYJ209+1.009 (46.87) (8.25) (43.47) (11.58) (19.45) SYJ209+1.010 (543.09) (96.99) (461.27) (132.55) (206.65) SYJ209+1.011 >600 >600 >600 >600 >600 SYJ209+1.012 >600 >600 >600 >600 >600 SYJ209+1.013 >600 >600 >600 >600 >600 SYJ209+1.014 >600 >600 >600 >600 >600 SYJ209+1.015 >600 >600 >600 >600 >600 SYJ209+1.016 >600 >600 >600 >600 >600 SYJ209+1.017 >600 >600 >600 >600 >600 SYJ209+1.018 >600 >600 >600 >600 >600 SYJ209+1.019 >600 >600 >600 >600 >600 SYJ209+1.020 >600 >600 >600 >600 >600 SYJ210+1.001 (<0.01) (<0.01) (<0.01) (0.04) (<0.01) SYJ210+1.002 (<0.01) (<0.01) (<0.01) (0.04) (<0.01) SYJ210+1.003 (<0.01) (<0.01) (<0.01) (0.04) (<0.01) SYJ210+1.004 (<0.01) (<0.01) (<0.01) (0.04) (<0.01) SYJ210+1.005 (<0.01) (<0.01) (<0.01) (0.04) (<0.01) SYJ210+1.006 (<0.01) (<0.01) (<0.01) (0.03) (<0.01) SYJ210+1.007 (<0.01) (<0.01) (<0.01) (0.03) (<0.01) SYJ210+1.008 (<0.01) (<0.01) (<0.01) (0.03) (<0.01) SYJ210+1.009 (<0.01) (<0.01) (<0.01) (0.03) (<0.01) SYJ210+1.010 (<0.01) (<0.01) (<0.01) (0.10) (<0.01) SYJ210+1.011 (<0.01) (<0.01) (<0.01) (0.03) (<0.01) SYJ210+1.012 (<0.01) (<0.01) (<0.01) (0.03) (<0.01) SYJ210+1.013 (<0.01) (<0.01) (<0.01) (0.05) (<0.01) SYJ210+1.014 (<0.01) (<0.01) (0.01) (0.04) (<0.01) SYJ210+1.015 (<0.01) (<0.01) (0.01) (0.05) (<0.01) SYJ210+1.016 (<0.01) (<0.01) (<0.01) (0.04) (<0.01) SYJ210+1.017 (<0.01) (<0.01) (<0.01) (0.04) (<0.01) SYJ210+1.018 (<0.01) (<0.01) (<0.01) (0.04) (<0.01) SYJ210+1.019 (<0.01) (<0.01) (<0.01) (0.04) (<0.01) SYJ210+1.020 (<0.01) (<0.01) (<0.01) (0.04) (<0.01) SYJ211+1.001 (<0.01) (<0.01) (<0.01) (0.05) (<0.01) SYJ211+1.002 (0.01) (<0.01) (<0.01) (0.03) (<0.01) SYJ211+1.003 (0.51) (0.12) (<0.01) (0.04) (<0.01) SYJ211+1.004 (66.62) (17.25) (0.04) (0.04) (<0.01) SYJ211+1.005 >600 >600 (0.41) (0.05) (<0.01) SYJ211+1.006 >600 >600 (4.19) (0.14) (<0.01) SYJ211+1.007 >600 >600 (46.31) (1.01) (0.01) SYJ211+1.008 >600 >600 (546.46) (9.36) (0.02) SYJ211+1.009 >600 >600 >600 (97.63) (0.05) SYJ211+1.010 >600 >600 >600 >600 (0.11) SYJ211+1.011 >600 >600 >600 >600 (0.24) SYJ211+1.012 >600 >600 >600 >600 (0.50) SYJ211+1.013 >600 >600 >600 >600 (1.10) SYJ211+1.014 >600 >600 >600 >600 (2.26) SYJ211+1.015 >600 >600 >600 >600 (4.81) SYJ211+1.016 >600 >600 >600 >600 (9.97) SYJ211+1.017 >600 >600 >600 >600 (20.88) SYJ211+1.018 >600 >600 >600 >600 (43.65) SYJ211+1.019 >600 >600 >600 >600 (91.75) SYJ211+1.020 >600 >600 >600 >600 (191.57) SYJ212+1.001 (<0.01) (<0.01) (<0.01) (0.19) (<0.01) SYJ212+1.002 (<0.01) (<0.01) (<0.01) (0.03) (<0.01) SYJ212+1.003 (<0.01) (<0.01) (<0.01) (0.04) (<0.01) SYJ212+1.004 (<0.01) (<0.01) (<0.01) (0.03) (<0.01) SYJ212+1.005 (<0.01) (<0.01) (0.07) (0.03) (<0.01) SYJ212+1.006 (<0.01) (<0.01) (3.15) (0.03) (<0.01) SYJ212+1.007 (<0.01) (<0.01) (204.98) (0.04) (<0.01) SYJ212+1.008 (<0.01) (<0.01) >600 (0.04) (<0.01) SYJ212+1.009 (<0.01) (<0.01) >600 (0.05) (<0.01) SYJ212+1.010 (<0.01) (<0.01) >600 (0.07) (<0.01) SYJ212+1.011 (<0.01) (<0.01) stack (0.22) (<0.01) SYJ212+1.012 (<0.01) (<0.01) stack (0.27) (0.01) SYJ212+1.013 (<0.01) (<0.01) stack (0.37) (0.02) SYJ212+1.014 (<0.01) (<0.01) stack (0.63) (0.06) SYJ212+1.015 (<0.01) (<0.01) stack (1.20) (0.18) SYJ212+1.016 (<0.01) (<0.01) stack (2.44) (0.32) SYJ212+1.017 (0.01) (<0.01) stack (5.03) (0.69) SYJ212+1.018 (0.01) (<0.01) stack (10.63) (1.31) SYJ212+1.019 (<0.01) (<0.01) stack (17.14) (2.70) SYJ212+1.020 (0.01) (<0.01) stack (36.79) (5.51) abbreviations: (123.45) - refuted in 123.45 sec. 123.45 - proved in 123.45 sec. stack - stack overflow mem - memory allocation error large - too large input string