The question is on this webpage on Stack Overflow.
To my knowledge, imogen (like the g4-prover.pl that I did from seqprover.pl) is only a prover and not a counter-model finder, unfortunately. As prover AND counter-model finder, I know Dominique Larchey’s STRIP. But if STRIP is an automated theorem (ATP) prover designed for proof search and counter-model generation it is for Propositional Logic only, by contrast with imogen dedicated to FOL.
And I should forget neither fcube in Prolog nor Mauro Ferrari provers.
imogen is impressive, it does not crash with this formula:
joseph@mx:~$ imogen fol prove -i "
> ( ( o11 & o21 ) | ( ( o11 & o31 ) | ( ( o11 & o41 ) | ( ( o11 & o51 ) | ( ( o11 & o61 ) | ( ( o11 & o71 ) | ( ( o11 & o81 ) | ( ( o11 & o91 ) | ( ( o11 & o101 ) | ( ( o11 & o111 ) | ( ( o11 & o121 ) | ( ( o11 & o131 ) | ( ( o11 & o141 ) | ( ( o21 & o31 ) | ( ( o21 & o41 ) | ( ( o21 & o51 ) | ( ( o21 & o61 ) | ( ( o21 & o71 ) | ( ( o21 & o81 ) | ( ( o21 & o91 ) | ( ( o21 & o101 ) | ( ( o21 & o111 ) | ( ( o21 & o121 ) | ( ( o21 & o131 ) | ( ( o21 & o141 ) | ( ( o31 & o41 ) | ( ( o31 & o51 ) | ( ( o31 & o61 ) | ( ( o31 & o71 ) | ( ( o31 & o81 ) | ( ( o31 & o91 ) | ( ( o31 & o101 ) | ( ( o31 & o111 ) | ( ( o31 & o121 ) | ( ( o31 & o131 ) | ( ( o31 & o141 ) | ( ( o41 & o51 ) | ( ( o41 & o61 ) | ( ( o41 & o71 ) | ( ( o41 & o81 ) | ( ( o41 & o91 ) | ( ( o41 & o101 ) | ( ( o41 & o111 ) | ( ( o41 & o121 ) | ( ( o41 & o131 ) | ( ( o41 & o141 ) | ( ( o51 & o61 ) | ( ( o51 & o71 ) | ( ( o51 & o81 ) | ( ( o51 & o91 ) | ( ( o51 & o101 ) | ( ( o51 & o111 ) | ( ( o51 & o121 ) | ( ( o51 & o131 ) | ( ( o51 & o141 ) | ( ( o61 & o71 ) | ( ( o61 & o81 ) | ( ( o61 & o91 ) | ( ( o61 & o101 ) | ( ( o61 & o111 ) | ( ( o61 & o121 ) | ( ( o61 & o131 ) | ( ( o61 & o141 ) | ( ( o71 & o81 ) | ( ( o71 & o91 ) | ( ( o71 & o101 ) | ( ( o71 & o111 ) | ( ( o71 & o121 ) | ( ( o71 & o131 ) | ( ( o71 & o141 ) | ( ( o81 & o91 ) | ( ( o81 & o101 ) | ( ( o81 & o111 ) | ( ( o81 & o121 ) | ( ( o81 & o131 ) | ( ( o81 & o141 ) | ( ( o91 & o101 ) | ( ( o91 & o111 ) | ( ( o91 & o121 ) | ( ( o91 & o131 ) | ( ( o91 & o141 ) | ( ( o101 & o111 ) | ( ( o101 & o121 ) | ( ( o101 & o131 ) | ( ( o101 & o141 ) | ( ( o111 & o121 ) | ( ( o111 & o131 ) | ( ( o111 & o141 ) | ( ( o121 & o131 ) | ( ( o121 & o141 ) | ( ( o131 & o141 ) | ( ( o12 & o22 ) | ( ( o12 & o32 ) | ( ( o12 & o42 ) | ( ( o12 & o52 ) | ( ( o12 & o62 ) | ( ( o12 & o72 ) | ( ( o12 & o82 ) | ( ( o12 & o92 ) | ( ( o12 & o102 ) | ( ( o12 & o112 ) | ( ( o12 & o122 ) | ( ( o12 & o132 ) | ( ( o12 & o142 ) | ( ( o22 & o32 ) | ( ( o22 & o42 ) | ( ( o22 & o52 ) | ( ( o22 & o62 ) | ( ( o22 & o72 ) | ( ( o22 & o82 ) | ( ( o22 & o92 ) | ( ( o22 & o102 ) | ( ( o22 & o112 ) | ( ( o22 & o122 ) | ( ( o22 & o132 ) | ( ( o22 & o142 ) | ( ( o32 & o42 ) | ( ( o32 & o52 ) | ( ( o32 & o62 ) | ( ( o32 & o72 ) | ( ( o32 & o82 ) | ( ( o32 & o92 ) | ( ( o32 & o102 ) | ( ( o32 & o112 ) | ( ( o32 & o122 ) | ( ( o32 & o132 ) | ( ( o32 & o142 ) | ( ( o42 & o52 ) | ( ( o42 & o62 ) | ( ( o42 & o72 ) | ( ( o42 & o82 ) | ( ( o42 & o92 ) | ( ( o42 & o102 ) | ( ( o42 & o112 ) | ( ( o42 & o122 ) | ( ( o42 & o132 ) | ( ( o42 & o142 ) | ( ( o52 & o62 ) | ( ( o52 & o72 ) | ( ( o52 & o82 ) | ( ( o52 & o92 ) | ( ( o52 & o102 ) | ( ( o52 & o112 ) | ( ( o52 & o122 ) | ( ( o52 & o132 ) | ( ( o52 & o142 ) | ( ( o62 & o72 ) | ( ( o62 & o82 ) | ( ( o62 & o92 ) | ( ( o62 & o102 ) | ( ( o62 & o112 ) | ( ( o62 & o122 ) | ( ( o62 & o132 ) | ( ( o62 & o142 ) | ( ( o72 & o82 ) | ( ( o72 & o92 ) | ( ( o72 & o102 ) | ( ( o72 & o112 ) | ( ( o72 & o122 ) | ( ( o72 & o132 ) | ( ( o72 & o142 ) | ( ( o82 & o92 ) | ( ( o82 & o102 ) | ( ( o82 & o112 ) | ( ( o82 & o122 ) | ( ( o82 & o132 ) | ( ( o82 & o142 ) | ( ( o92 & o102 ) | ( ( o92 & o112 ) | ( ( o92 & o122 ) | ( ( o92 & o132 ) | ( ( o92 & o142 ) | ( ( o102 & o112 ) | ( ( o102 & o122 ) | ( ( o102 & o132 ) | ( ( o102 & o142 ) | ( ( o112 & o122 ) | ( ( o112 & o132 ) | ( ( o112 & o142 ) | ( ( o122 & o132 ) | ( ( o122 & o142 ) | ( ( o132 & o142 ) | ( ( o13 & o23 ) | ( ( o13 & o33 ) | ( ( o13 & o43 ) | ( ( o13 & o53 ) | ( ( o13 & o63 ) | ( ( o13 & o73 ) | ( ( o13 & o83 ) | ( ( o13 & o93 ) | ( ( o13 & o103 ) | ( ( o13 & o113 ) | ( ( o13 & o123 ) | ( ( o13 & o133 ) | ( ( o13 & o143 ) | ( ( o23 & o33 ) | ( ( o23 & o43 ) | ( ( o23 & o53 ) | ( ( o23 & o63 ) | ( ( o23 & o73 ) | ( ( o23 & o83 ) | ( ( o23 & o93 ) | ( ( o23 & o103 ) | ( ( o23 & o113 ) | ( ( o23 & o123 ) | ( ( o23 & o133 ) | ( ( o23 & o143 ) | ( ( o33 & o43 ) | ( ( o33 & o53 ) | ( ( o33 & o63 ) | ( ( o33 & o73 ) | ( ( o33 & o83 ) | ( ( o33 & o93 ) | ( ( o33 & o103 ) | ( ( o33 & o113 ) | ( ( o33 & o123 ) | ( ( o33 & o133 ) | ( ( o33 & o143 ) | ( ( o43 & o53 ) | ( ( o43 & o63 ) | ( ( o43 & o73 ) | ( ( o43 & o83 ) | ( ( o43 & o93 ) | ( ( o43 & o103 ) | ( ( o43 & o113 ) | ( ( o43 & o123 ) | ( ( o43 & o133 ) | ( ( o43 & o143 ) | ( ( o53 & o63 ) | ( ( o53 & o73 ) | ( ( o53 & o83 ) | ( ( o53 & o93 ) | ( ( o53 & o103 ) | ( ( o53 & o113 ) | ( ( o53 & o123 ) | ( ( o53 & o133 ) | ( ( o53 & o143 ) | ( ( o63 & o73 ) | ( ( o63 & o83 ) | ( ( o63 & o93 ) | ( ( o63 & o103 ) | ( ( o63 & o113 ) | ( ( o63 & o123 ) | ( ( o63 & o133 ) | ( ( o63 & o143 ) | ( ( o73 & o83 ) | ( ( o73 & o93 ) | ( ( o73 & o103 ) | ( ( o73 & o113 ) | ( ( o73 & o123 ) | ( ( o73 & o133 ) | ( ( o73 & o143 ) | ( ( o83 & o93 ) | ( ( o83 & o103 ) | ( ( o83 & o113 ) | ( ( o83 & o123 ) | ( ( o83 & o133 ) | ( ( o83 & o143 ) | ( ( o93 & o103 ) | ( ( o93 & o113 ) | ( ( o93 & o123 ) | ( ( o93 & o133 ) | ( ( o93 & o143 ) | ( ( o103 & o113 ) | ( ( o103 & o123 ) | ( ( o103 & o133 ) | ( ( o103 & o143 ) | ( ( o113 & o123 ) | ( ( o113 & o133 ) | ( ( o113 & o143 ) | ( ( o123 & o133 ) | ( ( o123 & o143 ) | ( ( o133 & o143 ) | ( ( o14 & o24 ) | ( ( o14 & o34 ) | ( ( o14 & o44 ) | ( ( o14 & o54 ) | ( ( o14 & o64 ) | ( ( o14 & o74 ) | ( ( o14 & o84 ) | ( ( o14 & o94 ) | ( ( o14 & o104 ) | ( ( o14 & o114 ) | ( ( o14 & o124 ) | ( ( o14 & o134 ) | ( ( o14 & o144 ) | ( ( o24 & o34 ) | ( ( o24 & o44 ) | ( ( o24 & o54 ) | ( ( o24 & o64 ) | ( ( o24 & o74 ) | ( ( o24 & o84 ) | ( ( o24 & o94 ) | ( ( o24 & o104 ) | ( ( o24 & o114 ) | ( ( o24 & o124 ) | ( ( o24 & o134 ) | ( ( o24 & o144 ) | ( ( o34 & o44 ) | ( ( o34 & o54 ) | ( ( o34 & o64 ) | ( ( o34 & o74 ) | ( ( o34 & o84 ) | ( ( o34 & o94 ) | ( ( o34 & o104 ) | ( ( o34 & o114 ) | ( ( o34 & o124 ) | ( ( o34 & o134 ) | ( ( o34 & o144 ) | ( ( o44 & o54 ) | ( ( o44 & o64 ) | ( ( o44 & o74 ) | ( ( o44 & o84 ) | ( ( o44 & o94 ) | ( ( o44 & o104 ) | ( ( o44 & o114 ) | ( ( o44 & o124 ) | ( ( o44 & o134 ) | ( ( o44 & o144 ) | ( ( o54 & o64 ) | ( ( o54 & o74 ) | ( ( o54 & o84 ) | ( ( o54 & o94 ) | ( ( o54 & o104 ) | ( ( o54 & o114 ) | ( ( o54 & o124 ) | ( ( o54 & o134 ) | ( ( o54 & o144 ) | ( ( o64 & o74 ) | ( ( o64 & o84 ) | ( ( o64 & o94 ) | ( ( o64 & o104 ) | ( ( o64 & o114 ) | ( ( o64 & o124 ) | ( ( o64 & o134 ) | ( ( o64 & o144 ) | ( ( o74 & o84 ) | ( ( o74 & o94 ) | ( ( o74 & o104 ) | ( ( o74 & o114 ) | ( ( o74 & o124 ) | ( ( o74 & o134 ) | ( ( o74 & o144 ) | ( ( o84 & o94 ) | ( ( o84 & o104 ) | ( ( o84 & o114 ) | ( ( o84 & o124 ) | ( ( o84 & o134 ) | ( ( o84 & o144 ) | ( ( o94 & o104 ) | ( ( o94 & o114 ) | ( ( o94 & o124 ) | ( ( o94 & o134 ) | ( ( o94 & o144 ) | ( ( o104 & o114 ) | ( ( o104 & o124 ) | ( ( o104 & o134 ) | ( ( o104 & o144 ) | ( ( o114 & o124 ) | ( ( o114 & o134 ) | ( ( o114 & o144 ) | ( ( o124 & o134 ) | ( ( o124 & o144 ) | ( ( o134 & o144 ) | ( ( o15 & o25 ) | ( ( o15 & o35 ) | ( ( o15 & o45 ) | ( ( o15 & o55 ) | ( ( o15 & o65 ) | ( ( o15 & o75 ) | ( ( o15 & o85 ) | ( ( o15 & o95 ) | ( ( o15 & o105 ) | ( ( o15 & o115 ) | ( ( o15 & o125 ) | ( ( o15 & o135 ) | ( ( o15 & o145 ) | ( ( o25 & o35 ) | ( ( o25 & o45 ) | ( ( o25 & o55 ) | ( ( o25 & o65 ) | ( ( o25 & o75 ) | ( ( o25 & o85 ) | ( ( o25 & o95 ) | ( ( o25 & o105 ) | ( ( o25 & o115 ) | ( ( o25 & o125 ) | ( ( o25 & o135 ) | ( ( o25 & o145 ) | ( ( o35 & o45 ) | ( ( o35 & o55 ) | ( ( o35 & o65 ) | ( ( o35 & o75 ) | ( ( o35 & o85 ) | ( ( o35 & o95 ) | ( ( o35 & o105 ) | ( ( o35 & o115 ) | ( ( o35 & o125 ) | ( ( o35 & o135 ) | ( ( o35 & o145 ) | ( ( o45 & o55 ) | ( ( o45 & o65 ) | ( ( o45 & o75 ) | ( ( o45 & o85 ) | ( ( o45 & o95 ) | ( ( o45 & o105 ) | ( ( o45 & o115 ) | ( ( o45 & o125 ) | ( ( o45 & o135 ) | ( ( o45 & o145 ) | ( ( o55 & o65 ) | ( ( o55 & o75 ) | ( ( o55 & o85 ) | ( ( o55 & o95 ) | ( ( o55 & o105 ) | ( ( o55 & o115 ) | ( ( o55 & o125 ) | ( ( o55 & o135 ) | ( ( o55 & o145 ) | ( ( o65 & o75 ) | ( ( o65 & o85 ) | ( ( o65 & o95 ) | ( ( o65 & o105 ) | ( ( o65 & o115 ) | ( ( o65 & o125 ) | ( ( o65 & o135 ) | ( ( o65 & o145 ) | ( ( o75 & o85 ) | ( ( o75 & o95 ) | ( ( o75 & o105 ) | ( ( o75 & o115 ) | ( ( o75 & o125 ) | ( ( o75 & o135 ) | ( ( o75 & o145 ) | ( ( o85 & o95 ) | ( ( o85 & o105 ) | ( ( o85 & o115 ) | ( ( o85 & o125 ) | ( ( o85 & o135 ) | ( ( o85 & o145 ) | ( ( o95 & o105 ) | ( ( o95 & o115 ) | ( ( o95 & o125 ) | ( ( o95 & o135 ) | ( ( o95 & o145 ) | ( ( o105 & o115 ) | ( ( o105 & o125 ) | ( ( o105 & o135 ) | ( ( o105 & o145 ) | ( ( o115 & o125 ) | ( ( o115 & o135 ) | ( ( o115 & o145 ) | ( ( o125 & o135 ) | ( ( o125 & o145 ) | ( ( o135 & o145 ) | ( ( o16 & o26 ) | ( ( o16 & o36 ) | ( ( o16 & o46 ) | ( ( o16 & o56 ) | ( ( o16 & o66 ) | ( ( o16 & o76 ) | ( ( o16 & o86 ) | ( ( o16 & o96 ) | ( ( o16 & o106 ) | ( ( o16 & o116 ) | ( ( o16 & o126 ) | ( ( o16 & o136 ) | ( ( o16 & o146 ) | ( ( o26 & o36 ) | ( ( o26 & o46 ) | ( ( o26 & o56 ) | ( ( o26 & o66 ) | ( ( o26 & o76 ) | ( ( o26 & o86 ) | ( ( o26 & o96 ) | ( ( o26 & o106 ) | ( ( o26 & o116 ) | ( ( o26 & o126 ) | ( ( o26 & o136 ) | ( ( o26 & o146 ) | ( ( o36 & o46 ) | ( ( o36 & o56 ) | ( ( o36 & o66 ) | ( ( o36 & o76 ) | ( ( o36 & o86 ) | ( ( o36 & o96 ) | ( ( o36 & o106 ) | ( ( o36 & o116 ) | ( ( o36 & o126 ) | ( ( o36 & o136 ) | ( ( o36 & o146 ) | ( ( o46 & o56 ) | ( ( o46 & o66 ) | ( ( o46 & o76 ) | ( ( o46 & o86 ) | ( ( o46 & o96 ) | ( ( o46 & o106 ) | ( ( o46 & o116 ) | ( ( o46 & o126 ) | ( ( o46 & o136 ) | ( ( o46 & o146 ) | ( ( o56 & o66 ) | ( ( o56 & o76 ) | ( ( o56 & o86 ) | ( ( o56 & o96 ) | ( ( o56 & o106 ) | ( ( o56 & o116 ) | ( ( o56 & o126 ) | ( ( o56 & o136 ) | ( ( o56 & o146 ) | ( ( o66 & o76 ) | ( ( o66 & o86 ) | ( ( o66 & o96 ) | ( ( o66 & o106 ) | ( ( o66 & o116 ) | ( ( o66 & o126 ) | ( ( o66 & o136 ) | ( ( o66 & o146 ) | ( ( o76 & o86 ) | ( ( o76 & o96 ) | ( ( o76 & o106 ) | ( ( o76 & o116 ) | ( ( o76 & o126 ) | ( ( o76 & o136 ) | ( ( o76 & o146 ) | ( ( o86 & o96 ) | ( ( o86 & o106 ) | ( ( o86 & o116 ) | ( ( o86 & o126 ) | ( ( o86 & o136 ) | ( ( o86 & o146 ) | ( ( o96 & o106 ) | ( ( o96 & o116 ) | ( ( o96 & o126 ) | ( ( o96 & o136 ) | ( ( o96 & o146 ) | ( ( o106 & o116 ) | ( ( o106 & o126 ) | ( ( o106 & o136 ) | ( ( o106 & o146 ) | ( ( o116 & o126 ) | ( ( o116 & o136 ) | ( ( o116 & o146 ) | ( ( o126 & o136 ) | ( ( o126 & o146 ) | ( ( o136 & o146 ) | ( ( o17 & o27 ) | ( ( o17 & o37 ) | ( ( o17 & o47 ) | ( ( o17 & o57 ) | ( ( o17 & o67 ) | ( ( o17 & o77 ) | ( ( o17 & o87 ) | ( ( o17 & o97 ) | ( ( o17 & o107 ) | ( ( o17 & o117 ) | ( ( o17 & o127 ) | ( ( o17 & o137 ) | ( ( o17 & o147 ) | ( ( o27 & o37 ) | ( ( o27 & o47 ) | ( ( o27 & o57 ) | ( ( o27 & o67 ) | ( ( o27 & o77 ) | ( ( o27 & o87 ) | ( ( o27 & o97 ) | ( ( o27 & o107 ) | ( ( o27 & o117 ) | ( ( o27 & o127 ) | ( ( o27 & o137 ) | ( ( o27 & o147 ) | ( ( o37 & o47 ) | ( ( o37 & o57 ) | ( ( o37 & o67 ) | ( ( o37 & o77 ) | ( ( o37 & o87 ) | ( ( o37 & o97 ) | ( ( o37 & o107 ) | ( ( o37 & o117 ) | ( ( o37 & o127 ) | ( ( o37 & o137 ) | ( ( o37 & o147 ) | ( ( o47 & o57 ) | ( ( o47 & o67 ) | ( ( o47 & o77 ) | ( ( o47 & o87 ) | ( ( o47 & o97 ) | ( ( o47 & o107 ) | ( ( o47 & o117 ) | ( ( o47 & o127 ) | ( ( o47 & o137 ) | ( ( o47 & o147 ) | ( ( o57 & o67 ) | ( ( o57 & o77 ) | ( ( o57 & o87 ) | ( ( o57 & o97 ) | ( ( o57 & o107 ) | ( ( o57 & o117 ) | ( ( o57 & o127 ) | ( ( o57 & o137 ) | ( ( o57 & o147 ) | ( ( o67 & o77 ) | ( ( o67 & o87 ) | ( ( o67 & o97 ) | ( ( o67 & o107 ) | ( ( o67 & o117 ) | ( ( o67 & o127 ) | ( ( o67 & o137 ) | ( ( o67 & o147 ) | ( ( o77 & o87 ) | ( ( o77 & o97 ) | ( ( o77 & o107 ) | ( ( o77 & o117 ) | ( ( o77 & o127 ) | ( ( o77 & o137 ) | ( ( o77 & o147 ) | ( ( o87 & o97 ) | ( ( o87 & o107 ) | ( ( o87 & o117 ) | ( ( o87 & o127 ) | ( ( o87 & o137 ) | ( ( o87 & o147 ) | ( ( o97 & o107 ) | ( ( o97 & o117 ) | ( ( o97 & o127 ) | ( ( o97 & o137 ) | ( ( o97 & o147 ) | ( ( o107 & o117 ) | ( ( o107 & o127 ) | ( ( o107 & o137 ) | ( ( o107 & o147 ) | ( ( o117 & o127 ) | ( ( o117 & o137 ) | ( ( o117 & o147 ) | ( ( o127 & o137 ) | ( ( o127 & o147 ) | ( ( o137 & o147 ) | ( ( o18 & o28 ) | ( ( o18 & o38 ) | ( ( o18 & o48 ) | ( ( o18 & o58 ) | ( ( o18 & o68 ) | ( ( o18 & o78 ) | ( ( o18 & o88 ) | ( ( o18 & o98 ) | ( ( o18 & o108 ) | ( ( o18 & o118 ) | ( ( o18 & o128 ) | ( ( o18 & o138 ) | ( ( o18 & o148 ) | ( ( o28 & o38 ) | ( ( o28 & o48 ) | ( ( o28 & o58 ) | ( ( o28 & o68 ) | ( ( o28 & o78 ) | ( ( o28 & o88 ) | ( ( o28 & o98 ) | ( ( o28 & o108 ) | ( ( o28 & o118 ) | ( ( o28 & o128 ) | ( ( o28 & o138 ) | ( ( o28 & o148 ) | ( ( o38 & o48 ) | ( ( o38 & o58 ) | ( ( o38 & o68 ) | ( ( o38 & o78 ) | ( ( o38 & o88 ) | ( ( o38 & o98 ) | ( ( o38 & o108 ) | ( ( o38 & o118 ) | ( ( o38 & o128 ) | ( ( o38 & o138 ) | ( ( o38 & o148 ) | ( ( o48 & o58 ) | ( ( o48 & o68 ) | ( ( o48 & o78 ) | ( ( o48 & o88 ) | ( ( o48 & o98 ) | ( ( o48 & o108 ) | ( ( o48 & o118 ) | ( ( o48 & o128 ) | ( ( o48 & o138 ) | ( ( o48 & o148 ) | ( ( o58 & o68 ) | ( ( o58 & o78 ) | ( ( o58 & o88 ) | ( ( o58 & o98 ) | ( ( o58 & o108 ) | ( ( o58 & o118 ) | ( ( o58 & o128 ) | ( ( o58 & o138 ) | ( ( o58 & o148 ) | ( ( o68 & o78 ) | ( ( o68 & o88 ) | ( ( o68 & o98 ) | ( ( o68 & o108 ) | ( ( o68 & o118 ) | ( ( o68 & o128 ) | ( ( o68 & o138 ) | ( ( o68 & o148 ) | ( ( o78 & o88 ) | ( ( o78 & o98 ) | ( ( o78 & o108 ) | ( ( o78 & o118 ) | ( ( o78 & o128 ) | ( ( o78 & o138 ) | ( ( o78 & o148 ) | ( ( o88 & o98 ) | ( ( o88 & o108 ) | ( ( o88 & o118 ) | ( ( o88 & o128 ) | ( ( o88 & o138 ) | ( ( o88 & o148 ) | ( ( o98 & o108 ) | ( ( o98 & o118 ) | ( ( o98 & o128 ) | ( ( o98 & o138 ) | ( ( o98 & o148 ) | ( ( o108 & o118 ) | ( ( o108 & o128 ) | ( ( o108 & o138 ) | ( ( o108 & o148 ) | ( ( o118 & o128 ) | ( ( o118 & o138 ) | ( ( o118 & o148 ) | ( ( o128 & o138 ) | ( ( o128 & o148 ) | ( ( o138 & o148 ) | ( ( o19 & o29 ) | ( ( o19 & o39 ) | ( ( o19 & o49 ) | ( ( o19 & o59 ) | ( ( o19 & o69 ) | ( ( o19 & o79 ) | ( ( o19 & o89 ) | ( ( o19 & o99 ) | ( ( o19 & o109 ) | ( ( o19 & o119 ) | ( ( o19 & o129 ) | ( ( o19 & o139 ) | ( ( o19 & o149 ) | ( ( o29 & o39 ) | ( ( o29 & o49 ) | ( ( o29 & o59 ) | ( ( o29 & o69 ) | ( ( o29 & o79 ) | ( ( o29 & o89 ) | ( ( o29 & o99 ) | ( ( o29 & o109 ) | ( ( o29 & o119 ) | ( ( o29 & o129 ) | ( ( o29 & o139 ) | ( ( o29 & o149 ) | ( ( o39 & o49 ) | ( ( o39 & o59 ) | ( ( o39 & o69 ) | ( ( o39 & o79 ) | ( ( o39 & o89 ) | ( ( o39 & o99 ) | ( ( o39 & o109 ) | ( ( o39 & o119 ) | ( ( o39 & o129 ) | ( ( o39 & o139 ) | ( ( o39 & o149 ) | ( ( o49 & o59 ) | ( ( o49 & o69 ) | ( ( o49 & o79 ) | ( ( o49 & o89 ) | ( ( o49 & o99 ) | ( ( o49 & o109 ) | ( ( o49 & o119 ) | ( ( o49 & o129 ) | ( ( o49 & o139 ) | ( ( o49 & o149 ) | ( ( o59 & o69 ) | ( ( o59 & o79 ) | ( ( o59 & o89 ) | ( ( o59 & o99 ) | ( ( o59 & o109 ) | ( ( o59 & o119 ) | ( ( o59 & o129 ) | ( ( o59 & o139 ) | ( ( o59 & o149 ) | ( ( o69 & o79 ) | ( ( o69 & o89 ) | ( ( o69 & o99 ) | ( ( o69 & o109 ) | ( ( o69 & o119 ) | ( ( o69 & o129 ) | ( ( o69 & o139 ) | ( ( o69 & o149 ) | ( ( o79 & o89 ) | ( ( o79 & o99 ) | ( ( o79 & o109 ) | ( ( o79 & o119 ) | ( ( o79 & o129 ) | ( ( o79 & o139 ) | ( ( o79 & o149 ) | ( ( o89 & o99 ) | ( ( o89 & o109 ) | ( ( o89 & o119 ) | ( ( o89 & o129 ) | ( ( o89 & o139 ) | ( ( o89 & o149 ) | ( ( o99 & o109 ) | ( ( o99 & o119 ) | ( ( o99 & o129 ) | ( ( o99 & o139 ) | ( ( o99 & o149 ) | ( ( o109 & o119 ) | ( ( o109 & o129 ) | ( ( o109 & o139 ) | ( ( o109 & o149 ) | ( ( o119 & o129 ) | ( ( o119 & o139 ) | ( ( o119 & o149 ) | ( ( o129 & o139 ) | ( ( o129 & o149 ) | ( ( o139 & o149 ) | ( ( o110 & o210 ) | ( ( o110 & o310 ) | ( ( o110 & o410 ) | ( ( o110 & o510 ) | ( ( o110 & o610 ) | ( ( o110 & o710 ) | ( ( o110 & o810 ) | ( ( o110 & o910 ) | ( ( o110 & o1010 ) | ( ( o110 & o1110 ) | ( ( o110 & o1210 ) | ( ( o110 & o1310 ) | ( ( o110 & o1410 ) | ( ( o210 & o310 ) | ( ( o210 & o410 ) | ( ( o210 & o510 ) | ( ( o210 & o610 ) | ( ( o210 & o710 ) | ( ( o210 & o810 ) | ( ( o210 & o910 ) | ( ( o210 & o1010 ) | ( ( o210 & o1110 ) | ( ( o210 & o1210 ) | ( ( o210 & o1310 ) | ( ( o210 & o1410 ) | ( ( o310 & o410 ) | ( ( o310 & o510 ) | ( ( o310 & o610 ) | ( ( o310 & o710 ) | ( ( o310 & o810 ) | ( ( o310 & o910 ) | ( ( o310 & o1010 ) | ( ( o310 & o1110 ) | ( ( o310 & o1210 ) | ( ( o310 & o1310 ) | ( ( o310 & o1410 ) | ( ( o410 & o510 ) | ( ( o410 & o610 ) | ( ( o410 & o710 ) | ( ( o410 & o810 ) | ( ( o410 & o910 ) | ( ( o410 & o1010 ) | ( ( o410 & o1110 ) | ( ( o410 & o1210 ) | ( ( o410 & o1310 ) | ( ( o410 & o1410 ) | ( ( o510 & o610 ) | ( ( o510 & o710 ) | ( ( o510 & o810 ) | ( ( o510 & o910 ) | ( ( o510 & o1010 ) | ( ( o510 & o1110 ) | ( ( o510 & o1210 ) | ( ( o510 & o1310 ) | ( ( o510 & o1410 ) | ( ( o610 & o710 ) | ( ( o610 & o810 ) | ( ( o610 & o910 ) | ( ( o610 & o1010 ) | ( ( o610 & o1110 ) | ( ( o610 & o1210 ) | ( ( o610 & o1310 ) | ( ( o610 & o1410 ) | ( ( o710 & o810 ) | ( ( o710 & o910 ) | ( ( o710 & o1010 ) | ( ( o710 & o1110 ) | ( ( o710 & o1210 ) | ( ( o710 & o1310 ) | ( ( o710 & o1410 ) | ( ( o810 & o910 ) | ( ( o810 & o1010 ) | ( ( o810 & o1110 ) | ( ( o810 & o1210 ) | ( ( o810 & o1310 ) | ( ( o810 & o1410 ) | ( ( o910 & o1010 ) | ( ( o910 & o1110 ) | ( ( o910 & o1210 ) | ( ( o910 & o1310 ) | ( ( o910 & o1410 ) | ( ( o1010 & o1110 ) | ( ( o1010 & o1210 ) | ( ( o1010 & o1310 ) | ( ( o1010 & o1410 ) | ( ( o1110 & o1210 ) | ( ( o1110 & o1310 ) | ( ( o1110 & o1410 ) | ( ( o1210 & o1310 ) | ( ( o1210 & o1410 ) | ( ( o1310 & o1410 ) | ( ( o111 & o211 ) | ( ( o111 & o311 ) | ( ( o111 & o411 ) | ( ( o111 & o511 ) | ( ( o111 & o611 ) | ( ( o111 & o711 ) | ( ( o111 & o811 ) | ( ( o111 & o911 ) | ( ( o111 & o1011 ) | ( ( o111 & o1111 ) | ( ( o111 & o1211 ) | ( ( o111 & o1311 ) | ( ( o111 & o1411 ) | ( ( o211 & o311 ) | ( ( o211 & o411 ) | ( ( o211 & o511 ) | ( ( o211 & o611 ) | ( ( o211 & o711 ) | ( ( o211 & o811 ) | ( ( o211 & o911 ) | ( ( o211 & o1011 ) | ( ( o211 & o1111 ) | ( ( o211 & o1211 ) | ( ( o211 & o1311 ) | ( ( o211 & o1411 ) | ( ( o311 & o411 ) | ( ( o311 & o511 ) | ( ( o311 & o611 ) | ( ( o311 & o711 ) | ( ( o311 & o811 ) | ( ( o311 & o911 ) | ( ( o311 & o1011 ) | ( ( o311 & o1111 ) | ( ( o311 & o1211 ) | ( ( o311 & o1311 ) | ( ( o311 & o1411 ) | ( ( o411 & o511 ) | ( ( o411 & o611 ) | ( ( o411 & o711 ) | ( ( o411 & o811 ) | ( ( o411 & o911 ) | ( ( o411 & o1011 ) | ( ( o411 & o1111 ) | ( ( o411 & o1211 ) | ( ( o411 & o1311 ) | ( ( o411 & o1411 ) | ( ( o511 & o611 ) | ( ( o511 & o711 ) | ( ( o511 & o811 ) | ( ( o511 & o911 ) | ( ( o511 & o1011 ) | ( ( o511 & o1111 ) | ( ( o511 & o1211 ) | ( ( o511 & o1311 ) | ( ( o511 & o1411 ) | ( ( o611 & o711 ) | ( ( o611 & o811 ) | ( ( o611 & o911 ) | ( ( o611 & o1011 ) | ( ( o611 & o1111 ) | ( ( o611 & o1211 ) | ( ( o611 & o1311 ) | ( ( o611 & o1411 ) | ( ( o711 & o811 ) | ( ( o711 & o911 ) | ( ( o711 & o1011 ) | ( ( o711 & o1111 ) | ( ( o711 & o1211 ) | ( ( o711 & o1311 ) | ( ( o711 & o1411 ) | ( ( o811 & o911 ) | ( ( o811 & o1011 ) | ( ( o811 & o1111 ) | ( ( o811 & o1211 ) | ( ( o811 & o1311 ) | ( ( o811 & o1411 ) | ( ( o911 & o1011 ) | ( ( o911 & o1111 ) | ( ( o911 & o1211 ) | ( ( o911 & o1311 ) | ( ( o911 & o1411 ) | ( ( o1011 & o1111 ) | ( ( o1011 & o1211 ) | ( ( o1011 & o1311 ) | ( ( o1011 & o1411 ) | ( ( o1111 & o1211 ) | ( ( o1111 & o1311 ) | ( ( o1111 & o1411 ) | ( ( o1211 & o1311 ) | ( ( o1211 & o1411 ) | ( ( o1311 & o1411 ) | ( ( o112 & o212 ) | ( ( o112 & o312 ) | ( ( o112 & o412 ) | ( ( o112 & o512 ) | ( ( o112 & o612 ) | ( ( o112 & o712 ) | ( ( o112 & o812 ) | ( ( o112 & o912 ) | ( ( o112 & o1012 ) | ( ( o112 & o1112 ) | ( ( o112 & o1212 ) | ( ( o112 & o1312 ) | ( ( o112 & o1412 ) | ( ( o212 & o312 ) | ( ( o212 & o412 ) | ( ( o212 & o512 ) | ( ( o212 & o612 ) | ( ( o212 & o712 ) | ( ( o212 & o812 ) | ( ( o212 & o912 ) | ( ( o212 & o1012 ) | ( ( o212 & o1112 ) | ( ( o212 & o1212 ) | ( ( o212 & o1312 ) | ( ( o212 & o1412 ) | ( ( o312 & o412 ) | ( ( o312 & o512 ) | ( ( o312 & o612 ) | ( ( o312 & o712 ) | ( ( o312 & o812 ) | ( ( o312 & o912 ) | ( ( o312 & o1012 ) | ( ( o312 & o1112 ) | ( ( o312 & o1212 ) | ( ( o312 & o1312 ) | ( ( o312 & o1412 ) | ( ( o412 & o512 ) | ( ( o412 & o612 ) | ( ( o412 & o712 ) | ( ( o412 & o812 ) | ( ( o412 & o912 ) | ( ( o412 & o1012 ) | ( ( o412 & o1112 ) | ( ( o412 & o1212 ) | ( ( o412 & o1312 ) | ( ( o412 & o1412 ) | ( ( o512 & o612 ) | ( ( o512 & o712 ) | ( ( o512 & o812 ) | ( ( o512 & o912 ) | ( ( o512 & o1012 ) | ( ( o512 & o1112 ) | ( ( o512 & o1212 ) | ( ( o512 & o1312 ) | ( ( o512 & o1412 ) | ( ( o612 & o712 ) | ( ( o612 & o812 ) | ( ( o612 & o912 ) | ( ( o612 & o1012 ) | ( ( o612 & o1112 ) | ( ( o612 & o1212 ) | ( ( o612 & o1312 ) | ( ( o612 & o1412 ) | ( ( o712 & o812 ) | ( ( o712 & o912 ) | ( ( o712 & o1012 ) | ( ( o712 & o1112 ) | ( ( o712 & o1212 ) | ( ( o712 & o1312 ) | ( ( o712 & o1412 ) | ( ( o812 & o912 ) | ( ( o812 & o1012 ) | ( ( o812 & o1112 ) | ( ( o812 & o1212 ) | ( ( o812 & o1312 ) | ( ( o812 & o1412 ) | ( ( o912 & o1012 ) | ( ( o912 & o1112 ) | ( ( o912 & o1212 ) | ( ( o912 & o1312 ) | ( ( o912 & o1412 ) | ( ( o1012 & o1112 ) | ( ( o1012 & o1212 ) | ( ( o1012 & o1312 ) | ( ( o1012 & o1412 ) | ( ( o1112 & o1212 ) | ( ( o1112 & o1312 ) | ( ( o1112 & o1412 ) | ( ( o1212 & o1312 ) | ( ( o1212 & o1412 ) | ( ( o1312 & o1412 ) | ( ( o113 & o213 ) | ( ( o113 & o313 ) | ( ( o113 & o413 ) | ( ( o113 & o513 ) | ( ( o113 & o613 ) | ( ( o113 & o713 ) | ( ( o113 & o813 ) | ( ( o113 & o913 ) | ( ( o113 & o1013 ) | ( ( o113 & o1113 ) | ( ( o113 & o1213 ) | ( ( o113 & o1313 ) | ( ( o113 & o1413 ) | ( ( o213 & o313 ) | ( ( o213 & o413 ) | ( ( o213 & o513 ) | ( ( o213 & o613 ) | ( ( o213 & o713 ) | ( ( o213 & o813 ) | ( ( o213 & o913 ) | ( ( o213 & o1013 ) | ( ( o213 & o1113 ) | ( ( o213 & o1213 ) | ( ( o213 & o1313 ) | ( ( o213 & o1413 ) | ( ( o313 & o413 ) | ( ( o313 & o513 ) | ( ( o313 & o613 ) | ( ( o313 & o713 ) | ( ( o313 & o813 ) | ( ( o313 & o913 ) | ( ( o313 & o1013 ) | ( ( o313 & o1113 ) | ( ( o313 & o1213 ) | ( ( o313 & o1313 ) | ( ( o313 & o1413 ) | ( ( o413 & o513 ) | ( ( o413 & o613 ) | ( ( o413 & o713 ) | ( ( o413 & o813 ) | ( ( o413 & o913 ) | ( ( o413 & o1013 ) | ( ( o413 & o1113 ) | ( ( o413 & o1213 ) | ( ( o413 & o1313 ) | ( ( o413 & o1413 ) | ( ( o513 & o613 ) | ( ( o513 & o713 ) | ( ( o513 & o813 ) | ( ( o513 & o913 ) | ( ( o513 & o1013 ) | ( ( o513 & o1113 ) | ( ( o513 & o1213 ) | ( ( o513 & o1313 ) | ( ( o513 & o1413 ) | ( ( o613 & o713 ) | ( ( o613 & o813 ) | ( ( o613 & o913 ) | ( ( o613 & o1013 ) | ( ( o613 & o1113 ) | ( ( o613 & o1213 ) | ( ( o613 & o1313 ) | ( ( o613 & o1413 ) | ( ( o713 & o813 ) | ( ( o713 & o913 ) | ( ( o713 & o1013 ) | ( ( o713 & o1113 ) | ( ( o713 & o1213 ) | ( ( o713 & o1313 ) | ( ( o713 & o1413 ) | ( ( o813 & o913 ) | ( ( o813 & o1013 ) | ( ( o813 & o1113 ) | ( ( o813 & o1213 ) | ( ( o813 & o1313 ) | ( ( o813 & o1413 ) | ( ( o913 & o1013 ) | ( ( o913 & o1113 ) | ( ( o913 & o1213 ) | ( ( o913 & o1313 ) | ( ( o913 & o1413 ) | ( ( o1013 & o1113 ) | ( ( o1013 & o1213 ) | ( ( o1013 & o1313 ) | ( ( o1013 & o1413 ) | ( ( o1113 & o1213 ) | ( ( o1113 & o1313 ) | ( ( o1113 & o1413 ) | ( ( o1213 & o1313 ) | ( ( o1213 & o1413 ) | ( o1313 & o1413 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )"
Unprovable.
doesn’t seem to be the case generally, in SWISH the sandbox precludes
?- op(100, xfy, &).
but on my box after the declaration I get quickly
?- F=( ( ... ) ),display(F).
'|'(&(o11,o21),'|'(&(o11,o31),'|'(&(o11,o41),'|'(&(o11,o51),'|'(&(o11,o61),'|'(&(o11,o71),'|'(&(o11,o81),'|'(&(o11,o91),'|'(&(o11,o101),'|'(...etc etc
F = (o11&o21| o11&o31| o11&o41| o11&o51| o11&o61| o11&o71| o11&o81| o11&o91| ... & ...| ...| ...).
Unfortunately both read/1 and write/1 are eventually implemented as a recursive C function and thus may run out of stack. The default stack on Linux is a lot larger than the default on Windows and thus it takes a bit longer. C is notoriously poor at handling stack overflows. There is some noise on segmented stacks to resolve this issue, but this is AFAIK not yet widely available (and I do not know how much it would slow down normal C execution).
Eventually, these functions will need to be rewritten as a loop managing its own stack, just as happened for almost all recursive C functions quite a while back. These two beasts are pretty complicated though, making this a nasty job. Slightly simpler might be to guard against overflow. Although simpler, this is highly non-portable. You either need to compute the stack limit (non-portable) and check by hand or handle the exception cleanly (also non-portable).
SWI-Prolog allows for cyclic terms. That is more or less disconnected. It also avoids the native stack almost everywhere. I think only read/1, write/1 and control structures in the compiler still use the native stack. Even there, parts optimize for last argument handling to avoid a recursive call.