%------------------------------------------------------------------------------
% File : LEO-II---2.3.1
% Problem : PUZ036-1.005 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Oct 7 10:36:43 AM UTC 2026
% Result : Unsatisfiable 6.77s 1.53s
% Output : CNFRefutation 6.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 6
% Syntax : Number of formulae : 90 ( 81 unt; 0 typ; 0 def)
% Number of atoms : 343 ( 89 equ; 0 cnn)
% Maximal formula atoms : 2 ( 3 avg)
% Number of connectives : 3292 ( 77 ~; 75 |; 0 &;3140 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 43 ( 11 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 24 ( 21 usr; 22 con; 0-20 aty)
% Number of variables : 1500 ( 0 ^;1500 !; 0 ?;1500 :)
% Comments :
%------------------------------------------------------------------------------
thf(tp_p_1,type,
p_1: $i ).
thf(tp_p_10,type,
p_10: $i ).
thf(tp_p_11,type,
p_11: $i ).
thf(tp_p_12,type,
p_12: $i ).
thf(tp_p_13,type,
p_13: $i ).
thf(tp_p_14,type,
p_14: $i ).
thf(tp_p_15,type,
p_15: $i ).
thf(tp_p_16,type,
p_16: $i ).
thf(tp_p_17,type,
p_17: $i ).
thf(tp_p_18,type,
p_18: $i ).
thf(tp_p_19,type,
p_19: $i ).
thf(tp_p_2,type,
p_2: $i ).
thf(tp_p_20,type,
p_20: $i ).
thf(tp_p_3,type,
p_3: $i ).
thf(tp_p_4,type,
p_4: $i ).
thf(tp_p_5,type,
p_5: $i ).
thf(tp_p_6,type,
p_6: $i ).
thf(tp_p_7,type,
p_7: $i ).
thf(tp_p_8,type,
p_8: $i ).
thf(tp_p_9,type,
p_9: $i ).
thf(tp_state,type,
state: $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $o ).
thf(1,axiom,
! [X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
( ~ ( state @ X1 @ X2 @ X3 @ X4 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 )
| ( state @ X4 @ X3 @ X2 @ X1 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',flip) ).
thf(2,axiom,
! [X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
( ~ ( state @ X1 @ X2 @ X3 @ X4 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 )
| ( state @ X20 @ X1 @ X2 @ X3 @ X4 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',move_right) ).
thf(3,axiom,
! [X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
( ~ ( state @ X1 @ X2 @ X3 @ X4 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 )
| ( state @ X2 @ X3 @ X4 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 @ X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',move_left) ).
thf(4,axiom,
state @ p_5 @ p_4 @ p_3 @ p_2 @ p_1 @ p_6 @ p_7 @ p_8 @ p_9 @ p_10 @ p_11 @ p_12 @ p_13 @ p_14 @ p_15 @ p_16 @ p_17 @ p_18 @ p_19 @ p_20,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',initial_configuration) ).
thf(5,conjecture,
$false,
file('no conjecture given, we try to refute the axioms',dummy_conjecture) ).
thf(6,negated_conjecture,
$false = $false,
inference(negate_conjecture,[status(cth)],[5]) ).
thf(7,negated_conjecture,
~ ( state @ p_1 @ p_2 @ p_3 @ p_4 @ p_5 @ p_6 @ p_7 @ p_8 @ p_9 @ p_10 @ p_11 @ p_12 @ p_13 @ p_14 @ p_15 @ p_16 @ p_17 @ p_18 @ p_19 @ p_20 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',make_like_this) ).
thf(8,plain,
$false = $false,
inference(unfold_def,[status(thm)],[6]) ).
thf(9,plain,
( ( ! [X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
( ~ ( state @ X1 @ X2 @ X3 @ X4 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 )
| ( state @ X4 @ X3 @ X2 @ X1 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[1]) ).
thf(10,plain,
( ( ! [X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
( ~ ( state @ X1 @ X2 @ X3 @ X4 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 )
| ( state @ X20 @ X1 @ X2 @ X3 @ X4 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[2]) ).
thf(11,plain,
( ( ! [X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
( ~ ( state @ X1 @ X2 @ X3 @ X4 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 )
| ( state @ X2 @ X3 @ X4 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 @ X1 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[3]) ).
thf(12,plain,
( ( state @ p_5 @ p_4 @ p_3 @ p_2 @ p_1 @ p_6 @ p_7 @ p_8 @ p_9 @ p_10 @ p_11 @ p_12 @ p_13 @ p_14 @ p_15 @ p_16 @ p_17 @ p_18 @ p_19 @ p_20 )
= $true ),
inference(unfold_def,[status(thm)],[4]) ).
thf(13,plain,
( ( ~ ( state @ p_1 @ p_2 @ p_3 @ p_4 @ p_5 @ p_6 @ p_7 @ p_8 @ p_9 @ p_10 @ p_11 @ p_12 @ p_13 @ p_14 @ p_15 @ p_16 @ p_17 @ p_18 @ p_19 @ p_20 ) )
= $true ),
inference(unfold_def,[status(thm)],[7]) ).
thf(14,plain,
( ( ~ $false ) = $true ),
inference(polarity_switch,[status(thm)],[8]) ).
thf(15,plain,
( ( ~ ( state @ p_1 @ p_2 @ p_3 @ p_4 @ p_5 @ p_6 @ p_7 @ p_8 @ p_9 @ p_10 @ p_11 @ p_12 @ p_13 @ p_14 @ p_15 @ p_16 @ p_17 @ p_18 @ p_19 @ p_20 ) )
= $true ),
inference(copy,[status(thm)],[13]) ).
thf(16,plain,
( ( state @ p_5 @ p_4 @ p_3 @ p_2 @ p_1 @ p_6 @ p_7 @ p_8 @ p_9 @ p_10 @ p_11 @ p_12 @ p_13 @ p_14 @ p_15 @ p_16 @ p_17 @ p_18 @ p_19 @ p_20 )
= $true ),
inference(copy,[status(thm)],[12]) ).
thf(17,plain,
( ( ! [X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
( ~ ( state @ X1 @ X2 @ X3 @ X4 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 )
| ( state @ X2 @ X3 @ X4 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 @ X1 ) ) )
= $true ),
inference(copy,[status(thm)],[11]) ).
thf(18,plain,
( ( ! [X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
( ~ ( state @ X1 @ X2 @ X3 @ X4 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 )
| ( state @ X20 @ X1 @ X2 @ X3 @ X4 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 ) ) )
= $true ),
inference(copy,[status(thm)],[10]) ).
thf(19,plain,
( ( ! [X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
( ~ ( state @ X1 @ X2 @ X3 @ X4 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 )
| ( state @ X4 @ X3 @ X2 @ X1 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 ) ) )
= $true ),
inference(copy,[status(thm)],[9]) ).
thf(20,plain,
( ( ~ $false ) = $true ),
inference(copy,[status(thm)],[14]) ).
thf(21,plain,
( ( state @ p_1 @ p_2 @ p_3 @ p_4 @ p_5 @ p_6 @ p_7 @ p_8 @ p_9 @ p_10 @ p_11 @ p_12 @ p_13 @ p_14 @ p_15 @ p_16 @ p_17 @ p_18 @ p_19 @ p_20 )
= $false ),
inference(extcnf_not_pos,[status(thm)],[15]) ).
thf(22,plain,
! [SV1: $i] :
( ( ! [SY60: $i,SY61: $i,SY62: $i,SY63: $i,SY64: $i,SY65: $i,SY66: $i,SY67: $i,SY68: $i,SY69: $i,SY70: $i,SY71: $i,SY72: $i,SY73: $i,SY74: $i,SY75: $i,SY76: $i,SY77: $i,SY78: $i] :
( ~ ( state @ SV1 @ SY60 @ SY61 @ SY62 @ SY63 @ SY64 @ SY65 @ SY66 @ SY67 @ SY68 @ SY69 @ SY70 @ SY71 @ SY72 @ SY73 @ SY74 @ SY75 @ SY76 @ SY77 @ SY78 )
| ( state @ SY60 @ SY61 @ SY62 @ SY63 @ SY64 @ SY65 @ SY66 @ SY67 @ SY68 @ SY69 @ SY70 @ SY71 @ SY72 @ SY73 @ SY74 @ SY75 @ SY76 @ SY77 @ SY78 @ SV1 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[17]) ).
thf(23,plain,
! [SV2: $i] :
( ( ! [SY79: $i,SY80: $i,SY81: $i,SY82: $i,SY83: $i,SY84: $i,SY85: $i,SY86: $i,SY87: $i,SY88: $i,SY89: $i,SY90: $i,SY91: $i,SY92: $i,SY93: $i,SY94: $i,SY95: $i,SY96: $i,SY97: $i] :
( ~ ( state @ SV2 @ SY79 @ SY80 @ SY81 @ SY82 @ SY83 @ SY84 @ SY85 @ SY86 @ SY87 @ SY88 @ SY89 @ SY90 @ SY91 @ SY92 @ SY93 @ SY94 @ SY95 @ SY96 @ SY97 )
| ( state @ SY97 @ SV2 @ SY79 @ SY80 @ SY81 @ SY82 @ SY83 @ SY84 @ SY85 @ SY86 @ SY87 @ SY88 @ SY89 @ SY90 @ SY91 @ SY92 @ SY93 @ SY94 @ SY95 @ SY96 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[18]) ).
thf(24,plain,
! [SV3: $i] :
( ( ! [SY98: $i,SY99: $i,SY100: $i,SY101: $i,SY102: $i,SY103: $i,SY104: $i,SY105: $i,SY106: $i,SY107: $i,SY108: $i,SY109: $i,SY110: $i,SY111: $i,SY112: $i,SY113: $i,SY114: $i,SY115: $i,SY116: $i] :
( ~ ( state @ SV3 @ SY98 @ SY99 @ SY100 @ SY101 @ SY102 @ SY103 @ SY104 @ SY105 @ SY106 @ SY107 @ SY108 @ SY109 @ SY110 @ SY111 @ SY112 @ SY113 @ SY114 @ SY115 @ SY116 )
| ( state @ SY100 @ SY99 @ SY98 @ SV3 @ SY101 @ SY102 @ SY103 @ SY104 @ SY105 @ SY106 @ SY107 @ SY108 @ SY109 @ SY110 @ SY111 @ SY112 @ SY113 @ SY114 @ SY115 @ SY116 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[19]) ).
thf(25,plain,
$false = $false,
inference(extcnf_not_pos,[status(thm)],[20]) ).
thf(26,plain,
! [SV4: $i,SV1: $i] :
( ( ! [SY117: $i,SY118: $i,SY119: $i,SY120: $i,SY121: $i,SY122: $i,SY123: $i,SY124: $i,SY125: $i,SY126: $i,SY127: $i,SY128: $i,SY129: $i,SY130: $i,SY131: $i,SY132: $i,SY133: $i,SY134: $i] :
( ~ ( state @ SV1 @ SV4 @ SY117 @ SY118 @ SY119 @ SY120 @ SY121 @ SY122 @ SY123 @ SY124 @ SY125 @ SY126 @ SY127 @ SY128 @ SY129 @ SY130 @ SY131 @ SY132 @ SY133 @ SY134 )
| ( state @ SV4 @ SY117 @ SY118 @ SY119 @ SY120 @ SY121 @ SY122 @ SY123 @ SY124 @ SY125 @ SY126 @ SY127 @ SY128 @ SY129 @ SY130 @ SY131 @ SY132 @ SY133 @ SY134 @ SV1 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[22]) ).
thf(27,plain,
! [SV5: $i,SV2: $i] :
( ( ! [SY135: $i,SY136: $i,SY137: $i,SY138: $i,SY139: $i,SY140: $i,SY141: $i,SY142: $i,SY143: $i,SY144: $i,SY145: $i,SY146: $i,SY147: $i,SY148: $i,SY149: $i,SY150: $i,SY151: $i,SY152: $i] :
( ~ ( state @ SV2 @ SV5 @ SY135 @ SY136 @ SY137 @ SY138 @ SY139 @ SY140 @ SY141 @ SY142 @ SY143 @ SY144 @ SY145 @ SY146 @ SY147 @ SY148 @ SY149 @ SY150 @ SY151 @ SY152 )
| ( state @ SY152 @ SV2 @ SV5 @ SY135 @ SY136 @ SY137 @ SY138 @ SY139 @ SY140 @ SY141 @ SY142 @ SY143 @ SY144 @ SY145 @ SY146 @ SY147 @ SY148 @ SY149 @ SY150 @ SY151 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[23]) ).
thf(28,plain,
! [SV6: $i,SV3: $i] :
( ( ! [SY153: $i,SY154: $i,SY155: $i,SY156: $i,SY157: $i,SY158: $i,SY159: $i,SY160: $i,SY161: $i,SY162: $i,SY163: $i,SY164: $i,SY165: $i,SY166: $i,SY167: $i,SY168: $i,SY169: $i,SY170: $i] :
( ~ ( state @ SV3 @ SV6 @ SY153 @ SY154 @ SY155 @ SY156 @ SY157 @ SY158 @ SY159 @ SY160 @ SY161 @ SY162 @ SY163 @ SY164 @ SY165 @ SY166 @ SY167 @ SY168 @ SY169 @ SY170 )
| ( state @ SY154 @ SY153 @ SV6 @ SV3 @ SY155 @ SY156 @ SY157 @ SY158 @ SY159 @ SY160 @ SY161 @ SY162 @ SY163 @ SY164 @ SY165 @ SY166 @ SY167 @ SY168 @ SY169 @ SY170 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[24]) ).
thf(29,plain,
! [SV7: $i,SV4: $i,SV1: $i] :
( ( ! [SY171: $i,SY172: $i,SY173: $i,SY174: $i,SY175: $i,SY176: $i,SY177: $i,SY178: $i,SY179: $i,SY180: $i,SY181: $i,SY182: $i,SY183: $i,SY184: $i,SY185: $i,SY186: $i,SY187: $i] :
( ~ ( state @ SV1 @ SV4 @ SV7 @ SY171 @ SY172 @ SY173 @ SY174 @ SY175 @ SY176 @ SY177 @ SY178 @ SY179 @ SY180 @ SY181 @ SY182 @ SY183 @ SY184 @ SY185 @ SY186 @ SY187 )
| ( state @ SV4 @ SV7 @ SY171 @ SY172 @ SY173 @ SY174 @ SY175 @ SY176 @ SY177 @ SY178 @ SY179 @ SY180 @ SY181 @ SY182 @ SY183 @ SY184 @ SY185 @ SY186 @ SY187 @ SV1 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[26]) ).
thf(30,plain,
! [SV8: $i,SV5: $i,SV2: $i] :
( ( ! [SY188: $i,SY189: $i,SY190: $i,SY191: $i,SY192: $i,SY193: $i,SY194: $i,SY195: $i,SY196: $i,SY197: $i,SY198: $i,SY199: $i,SY200: $i,SY201: $i,SY202: $i,SY203: $i,SY204: $i] :
( ~ ( state @ SV2 @ SV5 @ SV8 @ SY188 @ SY189 @ SY190 @ SY191 @ SY192 @ SY193 @ SY194 @ SY195 @ SY196 @ SY197 @ SY198 @ SY199 @ SY200 @ SY201 @ SY202 @ SY203 @ SY204 )
| ( state @ SY204 @ SV2 @ SV5 @ SV8 @ SY188 @ SY189 @ SY190 @ SY191 @ SY192 @ SY193 @ SY194 @ SY195 @ SY196 @ SY197 @ SY198 @ SY199 @ SY200 @ SY201 @ SY202 @ SY203 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[27]) ).
thf(31,plain,
! [SV9: $i,SV6: $i,SV3: $i] :
( ( ! [SY205: $i,SY206: $i,SY207: $i,SY208: $i,SY209: $i,SY210: $i,SY211: $i,SY212: $i,SY213: $i,SY214: $i,SY215: $i,SY216: $i,SY217: $i,SY218: $i,SY219: $i,SY220: $i,SY221: $i] :
( ~ ( state @ SV3 @ SV6 @ SV9 @ SY205 @ SY206 @ SY207 @ SY208 @ SY209 @ SY210 @ SY211 @ SY212 @ SY213 @ SY214 @ SY215 @ SY216 @ SY217 @ SY218 @ SY219 @ SY220 @ SY221 )
| ( state @ SY205 @ SV9 @ SV6 @ SV3 @ SY206 @ SY207 @ SY208 @ SY209 @ SY210 @ SY211 @ SY212 @ SY213 @ SY214 @ SY215 @ SY216 @ SY217 @ SY218 @ SY219 @ SY220 @ SY221 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[28]) ).
thf(32,plain,
! [SV10: $i,SV7: $i,SV4: $i,SV1: $i] :
( ( ! [SY222: $i,SY223: $i,SY224: $i,SY225: $i,SY226: $i,SY227: $i,SY228: $i,SY229: $i,SY230: $i,SY231: $i,SY232: $i,SY233: $i,SY234: $i,SY235: $i,SY236: $i,SY237: $i] :
( ~ ( state @ SV1 @ SV4 @ SV7 @ SV10 @ SY222 @ SY223 @ SY224 @ SY225 @ SY226 @ SY227 @ SY228 @ SY229 @ SY230 @ SY231 @ SY232 @ SY233 @ SY234 @ SY235 @ SY236 @ SY237 )
| ( state @ SV4 @ SV7 @ SV10 @ SY222 @ SY223 @ SY224 @ SY225 @ SY226 @ SY227 @ SY228 @ SY229 @ SY230 @ SY231 @ SY232 @ SY233 @ SY234 @ SY235 @ SY236 @ SY237 @ SV1 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[29]) ).
thf(33,plain,
! [SV11: $i,SV8: $i,SV5: $i,SV2: $i] :
( ( ! [SY238: $i,SY239: $i,SY240: $i,SY241: $i,SY242: $i,SY243: $i,SY244: $i,SY245: $i,SY246: $i,SY247: $i,SY248: $i,SY249: $i,SY250: $i,SY251: $i,SY252: $i,SY253: $i] :
( ~ ( state @ SV2 @ SV5 @ SV8 @ SV11 @ SY238 @ SY239 @ SY240 @ SY241 @ SY242 @ SY243 @ SY244 @ SY245 @ SY246 @ SY247 @ SY248 @ SY249 @ SY250 @ SY251 @ SY252 @ SY253 )
| ( state @ SY253 @ SV2 @ SV5 @ SV8 @ SV11 @ SY238 @ SY239 @ SY240 @ SY241 @ SY242 @ SY243 @ SY244 @ SY245 @ SY246 @ SY247 @ SY248 @ SY249 @ SY250 @ SY251 @ SY252 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[30]) ).
thf(34,plain,
! [SV12: $i,SV9: $i,SV6: $i,SV3: $i] :
( ( ! [SY254: $i,SY255: $i,SY256: $i,SY257: $i,SY258: $i,SY259: $i,SY260: $i,SY261: $i,SY262: $i,SY263: $i,SY264: $i,SY265: $i,SY266: $i,SY267: $i,SY268: $i,SY269: $i] :
( ~ ( state @ SV3 @ SV6 @ SV9 @ SV12 @ SY254 @ SY255 @ SY256 @ SY257 @ SY258 @ SY259 @ SY260 @ SY261 @ SY262 @ SY263 @ SY264 @ SY265 @ SY266 @ SY267 @ SY268 @ SY269 )
| ( state @ SV12 @ SV9 @ SV6 @ SV3 @ SY254 @ SY255 @ SY256 @ SY257 @ SY258 @ SY259 @ SY260 @ SY261 @ SY262 @ SY263 @ SY264 @ SY265 @ SY266 @ SY267 @ SY268 @ SY269 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[31]) ).
thf(35,plain,
! [SV13: $i,SV10: $i,SV7: $i,SV4: $i,SV1: $i] :
( ( ! [SY270: $i,SY271: $i,SY272: $i,SY273: $i,SY274: $i,SY275: $i,SY276: $i,SY277: $i,SY278: $i,SY279: $i,SY280: $i,SY281: $i,SY282: $i,SY283: $i,SY284: $i] :
( ~ ( state @ SV1 @ SV4 @ SV7 @ SV10 @ SV13 @ SY270 @ SY271 @ SY272 @ SY273 @ SY274 @ SY275 @ SY276 @ SY277 @ SY278 @ SY279 @ SY280 @ SY281 @ SY282 @ SY283 @ SY284 )
| ( state @ SV4 @ SV7 @ SV10 @ SV13 @ SY270 @ SY271 @ SY272 @ SY273 @ SY274 @ SY275 @ SY276 @ SY277 @ SY278 @ SY279 @ SY280 @ SY281 @ SY282 @ SY283 @ SY284 @ SV1 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[32]) ).
thf(36,plain,
! [SV14: $i,SV11: $i,SV8: $i,SV5: $i,SV2: $i] :
( ( ! [SY285: $i,SY286: $i,SY287: $i,SY288: $i,SY289: $i,SY290: $i,SY291: $i,SY292: $i,SY293: $i,SY294: $i,SY295: $i,SY296: $i,SY297: $i,SY298: $i,SY299: $i] :
( ~ ( state @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SY285 @ SY286 @ SY287 @ SY288 @ SY289 @ SY290 @ SY291 @ SY292 @ SY293 @ SY294 @ SY295 @ SY296 @ SY297 @ SY298 @ SY299 )
| ( state @ SY299 @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SY285 @ SY286 @ SY287 @ SY288 @ SY289 @ SY290 @ SY291 @ SY292 @ SY293 @ SY294 @ SY295 @ SY296 @ SY297 @ SY298 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[33]) ).
thf(37,plain,
! [SV15: $i,SV12: $i,SV9: $i,SV6: $i,SV3: $i] :
( ( ! [SY300: $i,SY301: $i,SY302: $i,SY303: $i,SY304: $i,SY305: $i,SY306: $i,SY307: $i,SY308: $i,SY309: $i,SY310: $i,SY311: $i,SY312: $i,SY313: $i,SY314: $i] :
( ~ ( state @ SV3 @ SV6 @ SV9 @ SV12 @ SV15 @ SY300 @ SY301 @ SY302 @ SY303 @ SY304 @ SY305 @ SY306 @ SY307 @ SY308 @ SY309 @ SY310 @ SY311 @ SY312 @ SY313 @ SY314 )
| ( state @ SV12 @ SV9 @ SV6 @ SV3 @ SV15 @ SY300 @ SY301 @ SY302 @ SY303 @ SY304 @ SY305 @ SY306 @ SY307 @ SY308 @ SY309 @ SY310 @ SY311 @ SY312 @ SY313 @ SY314 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[34]) ).
thf(38,plain,
! [SV16: $i,SV13: $i,SV10: $i,SV7: $i,SV4: $i,SV1: $i] :
( ( ! [SY315: $i,SY316: $i,SY317: $i,SY318: $i,SY319: $i,SY320: $i,SY321: $i,SY322: $i,SY323: $i,SY324: $i,SY325: $i,SY326: $i,SY327: $i,SY328: $i] :
( ~ ( state @ SV1 @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SY315 @ SY316 @ SY317 @ SY318 @ SY319 @ SY320 @ SY321 @ SY322 @ SY323 @ SY324 @ SY325 @ SY326 @ SY327 @ SY328 )
| ( state @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SY315 @ SY316 @ SY317 @ SY318 @ SY319 @ SY320 @ SY321 @ SY322 @ SY323 @ SY324 @ SY325 @ SY326 @ SY327 @ SY328 @ SV1 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[35]) ).
thf(39,plain,
! [SV17: $i,SV14: $i,SV11: $i,SV8: $i,SV5: $i,SV2: $i] :
( ( ! [SY329: $i,SY330: $i,SY331: $i,SY332: $i,SY333: $i,SY334: $i,SY335: $i,SY336: $i,SY337: $i,SY338: $i,SY339: $i,SY340: $i,SY341: $i,SY342: $i] :
( ~ ( state @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SY329 @ SY330 @ SY331 @ SY332 @ SY333 @ SY334 @ SY335 @ SY336 @ SY337 @ SY338 @ SY339 @ SY340 @ SY341 @ SY342 )
| ( state @ SY342 @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SY329 @ SY330 @ SY331 @ SY332 @ SY333 @ SY334 @ SY335 @ SY336 @ SY337 @ SY338 @ SY339 @ SY340 @ SY341 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[36]) ).
thf(40,plain,
! [SV18: $i,SV15: $i,SV12: $i,SV9: $i,SV6: $i,SV3: $i] :
( ( ! [SY343: $i,SY344: $i,SY345: $i,SY346: $i,SY347: $i,SY348: $i,SY349: $i,SY350: $i,SY351: $i,SY352: $i,SY353: $i,SY354: $i,SY355: $i,SY356: $i] :
( ~ ( state @ SV3 @ SV6 @ SV9 @ SV12 @ SV15 @ SV18 @ SY343 @ SY344 @ SY345 @ SY346 @ SY347 @ SY348 @ SY349 @ SY350 @ SY351 @ SY352 @ SY353 @ SY354 @ SY355 @ SY356 )
| ( state @ SV12 @ SV9 @ SV6 @ SV3 @ SV15 @ SV18 @ SY343 @ SY344 @ SY345 @ SY346 @ SY347 @ SY348 @ SY349 @ SY350 @ SY351 @ SY352 @ SY353 @ SY354 @ SY355 @ SY356 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[37]) ).
thf(41,plain,
! [SV19: $i,SV16: $i,SV13: $i,SV10: $i,SV7: $i,SV4: $i,SV1: $i] :
( ( ! [SY357: $i,SY358: $i,SY359: $i,SY360: $i,SY361: $i,SY362: $i,SY363: $i,SY364: $i,SY365: $i,SY366: $i,SY367: $i,SY368: $i,SY369: $i] :
( ~ ( state @ SV1 @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SY357 @ SY358 @ SY359 @ SY360 @ SY361 @ SY362 @ SY363 @ SY364 @ SY365 @ SY366 @ SY367 @ SY368 @ SY369 )
| ( state @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SY357 @ SY358 @ SY359 @ SY360 @ SY361 @ SY362 @ SY363 @ SY364 @ SY365 @ SY366 @ SY367 @ SY368 @ SY369 @ SV1 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[38]) ).
thf(42,plain,
! [SV20: $i,SV17: $i,SV14: $i,SV11: $i,SV8: $i,SV5: $i,SV2: $i] :
( ( ! [SY370: $i,SY371: $i,SY372: $i,SY373: $i,SY374: $i,SY375: $i,SY376: $i,SY377: $i,SY378: $i,SY379: $i,SY380: $i,SY381: $i,SY382: $i] :
( ~ ( state @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SY370 @ SY371 @ SY372 @ SY373 @ SY374 @ SY375 @ SY376 @ SY377 @ SY378 @ SY379 @ SY380 @ SY381 @ SY382 )
| ( state @ SY382 @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SY370 @ SY371 @ SY372 @ SY373 @ SY374 @ SY375 @ SY376 @ SY377 @ SY378 @ SY379 @ SY380 @ SY381 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[39]) ).
thf(43,plain,
! [SV21: $i,SV18: $i,SV15: $i,SV12: $i,SV9: $i,SV6: $i,SV3: $i] :
( ( ! [SY383: $i,SY384: $i,SY385: $i,SY386: $i,SY387: $i,SY388: $i,SY389: $i,SY390: $i,SY391: $i,SY392: $i,SY393: $i,SY394: $i,SY395: $i] :
( ~ ( state @ SV3 @ SV6 @ SV9 @ SV12 @ SV15 @ SV18 @ SV21 @ SY383 @ SY384 @ SY385 @ SY386 @ SY387 @ SY388 @ SY389 @ SY390 @ SY391 @ SY392 @ SY393 @ SY394 @ SY395 )
| ( state @ SV12 @ SV9 @ SV6 @ SV3 @ SV15 @ SV18 @ SV21 @ SY383 @ SY384 @ SY385 @ SY386 @ SY387 @ SY388 @ SY389 @ SY390 @ SY391 @ SY392 @ SY393 @ SY394 @ SY395 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[40]) ).
thf(44,plain,
! [SV22: $i,SV19: $i,SV16: $i,SV13: $i,SV10: $i,SV7: $i,SV4: $i,SV1: $i] :
( ( ! [SY396: $i,SY397: $i,SY398: $i,SY399: $i,SY400: $i,SY401: $i,SY402: $i,SY403: $i,SY404: $i,SY405: $i,SY406: $i,SY407: $i] :
( ~ ( state @ SV1 @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SY396 @ SY397 @ SY398 @ SY399 @ SY400 @ SY401 @ SY402 @ SY403 @ SY404 @ SY405 @ SY406 @ SY407 )
| ( state @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SY396 @ SY397 @ SY398 @ SY399 @ SY400 @ SY401 @ SY402 @ SY403 @ SY404 @ SY405 @ SY406 @ SY407 @ SV1 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[41]) ).
thf(45,plain,
! [SV23: $i,SV20: $i,SV17: $i,SV14: $i,SV11: $i,SV8: $i,SV5: $i,SV2: $i] :
( ( ! [SY408: $i,SY409: $i,SY410: $i,SY411: $i,SY412: $i,SY413: $i,SY414: $i,SY415: $i,SY416: $i,SY417: $i,SY418: $i,SY419: $i] :
( ~ ( state @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SY408 @ SY409 @ SY410 @ SY411 @ SY412 @ SY413 @ SY414 @ SY415 @ SY416 @ SY417 @ SY418 @ SY419 )
| ( state @ SY419 @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SY408 @ SY409 @ SY410 @ SY411 @ SY412 @ SY413 @ SY414 @ SY415 @ SY416 @ SY417 @ SY418 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[42]) ).
thf(46,plain,
! [SV24: $i,SV21: $i,SV18: $i,SV15: $i,SV12: $i,SV9: $i,SV6: $i,SV3: $i] :
( ( ! [SY420: $i,SY421: $i,SY422: $i,SY423: $i,SY424: $i,SY425: $i,SY426: $i,SY427: $i,SY428: $i,SY429: $i,SY430: $i,SY431: $i] :
( ~ ( state @ SV3 @ SV6 @ SV9 @ SV12 @ SV15 @ SV18 @ SV21 @ SV24 @ SY420 @ SY421 @ SY422 @ SY423 @ SY424 @ SY425 @ SY426 @ SY427 @ SY428 @ SY429 @ SY430 @ SY431 )
| ( state @ SV12 @ SV9 @ SV6 @ SV3 @ SV15 @ SV18 @ SV21 @ SV24 @ SY420 @ SY421 @ SY422 @ SY423 @ SY424 @ SY425 @ SY426 @ SY427 @ SY428 @ SY429 @ SY430 @ SY431 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[43]) ).
thf(47,plain,
! [SV25: $i,SV22: $i,SV19: $i,SV16: $i,SV13: $i,SV10: $i,SV7: $i,SV4: $i,SV1: $i] :
( ( ! [SY432: $i,SY433: $i,SY434: $i,SY435: $i,SY436: $i,SY437: $i,SY438: $i,SY439: $i,SY440: $i,SY441: $i,SY442: $i] :
( ~ ( state @ SV1 @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SV25 @ SY432 @ SY433 @ SY434 @ SY435 @ SY436 @ SY437 @ SY438 @ SY439 @ SY440 @ SY441 @ SY442 )
| ( state @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SV25 @ SY432 @ SY433 @ SY434 @ SY435 @ SY436 @ SY437 @ SY438 @ SY439 @ SY440 @ SY441 @ SY442 @ SV1 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[44]) ).
thf(48,plain,
! [SV26: $i,SV23: $i,SV20: $i,SV17: $i,SV14: $i,SV11: $i,SV8: $i,SV5: $i,SV2: $i] :
( ( ! [SY443: $i,SY444: $i,SY445: $i,SY446: $i,SY447: $i,SY448: $i,SY449: $i,SY450: $i,SY451: $i,SY452: $i,SY453: $i] :
( ~ ( state @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SV26 @ SY443 @ SY444 @ SY445 @ SY446 @ SY447 @ SY448 @ SY449 @ SY450 @ SY451 @ SY452 @ SY453 )
| ( state @ SY453 @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SV26 @ SY443 @ SY444 @ SY445 @ SY446 @ SY447 @ SY448 @ SY449 @ SY450 @ SY451 @ SY452 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[45]) ).
thf(49,plain,
! [SV27: $i,SV24: $i,SV21: $i,SV18: $i,SV15: $i,SV12: $i,SV9: $i,SV6: $i,SV3: $i] :
( ( ! [SY454: $i,SY455: $i,SY456: $i,SY457: $i,SY458: $i,SY459: $i,SY460: $i,SY461: $i,SY462: $i,SY463: $i,SY464: $i] :
( ~ ( state @ SV3 @ SV6 @ SV9 @ SV12 @ SV15 @ SV18 @ SV21 @ SV24 @ SV27 @ SY454 @ SY455 @ SY456 @ SY457 @ SY458 @ SY459 @ SY460 @ SY461 @ SY462 @ SY463 @ SY464 )
| ( state @ SV12 @ SV9 @ SV6 @ SV3 @ SV15 @ SV18 @ SV21 @ SV24 @ SV27 @ SY454 @ SY455 @ SY456 @ SY457 @ SY458 @ SY459 @ SY460 @ SY461 @ SY462 @ SY463 @ SY464 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[46]) ).
thf(50,plain,
! [SV28: $i,SV25: $i,SV22: $i,SV19: $i,SV16: $i,SV13: $i,SV10: $i,SV7: $i,SV4: $i,SV1: $i] :
( ( ! [SY465: $i,SY466: $i,SY467: $i,SY468: $i,SY469: $i,SY470: $i,SY471: $i,SY472: $i,SY473: $i,SY474: $i] :
( ~ ( state @ SV1 @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SV25 @ SV28 @ SY465 @ SY466 @ SY467 @ SY468 @ SY469 @ SY470 @ SY471 @ SY472 @ SY473 @ SY474 )
| ( state @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SV25 @ SV28 @ SY465 @ SY466 @ SY467 @ SY468 @ SY469 @ SY470 @ SY471 @ SY472 @ SY473 @ SY474 @ SV1 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[47]) ).
thf(51,plain,
! [SV29: $i,SV26: $i,SV23: $i,SV20: $i,SV17: $i,SV14: $i,SV11: $i,SV8: $i,SV5: $i,SV2: $i] :
( ( ! [SY475: $i,SY476: $i,SY477: $i,SY478: $i,SY479: $i,SY480: $i,SY481: $i,SY482: $i,SY483: $i,SY484: $i] :
( ~ ( state @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SV26 @ SV29 @ SY475 @ SY476 @ SY477 @ SY478 @ SY479 @ SY480 @ SY481 @ SY482 @ SY483 @ SY484 )
| ( state @ SY484 @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SV26 @ SV29 @ SY475 @ SY476 @ SY477 @ SY478 @ SY479 @ SY480 @ SY481 @ SY482 @ SY483 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[48]) ).
thf(52,plain,
! [SV30: $i,SV27: $i,SV24: $i,SV21: $i,SV18: $i,SV15: $i,SV12: $i,SV9: $i,SV6: $i,SV3: $i] :
( ( ! [SY485: $i,SY486: $i,SY487: $i,SY488: $i,SY489: $i,SY490: $i,SY491: $i,SY492: $i,SY493: $i,SY494: $i] :
( ~ ( state @ SV3 @ SV6 @ SV9 @ SV12 @ SV15 @ SV18 @ SV21 @ SV24 @ SV27 @ SV30 @ SY485 @ SY486 @ SY487 @ SY488 @ SY489 @ SY490 @ SY491 @ SY492 @ SY493 @ SY494 )
| ( state @ SV12 @ SV9 @ SV6 @ SV3 @ SV15 @ SV18 @ SV21 @ SV24 @ SV27 @ SV30 @ SY485 @ SY486 @ SY487 @ SY488 @ SY489 @ SY490 @ SY491 @ SY492 @ SY493 @ SY494 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[49]) ).
thf(53,plain,
! [SV31: $i,SV28: $i,SV25: $i,SV22: $i,SV19: $i,SV16: $i,SV13: $i,SV10: $i,SV7: $i,SV4: $i,SV1: $i] :
( ( ! [SY495: $i,SY496: $i,SY497: $i,SY498: $i,SY499: $i,SY500: $i,SY501: $i,SY502: $i,SY503: $i] :
( ~ ( state @ SV1 @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SV25 @ SV28 @ SV31 @ SY495 @ SY496 @ SY497 @ SY498 @ SY499 @ SY500 @ SY501 @ SY502 @ SY503 )
| ( state @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SV25 @ SV28 @ SV31 @ SY495 @ SY496 @ SY497 @ SY498 @ SY499 @ SY500 @ SY501 @ SY502 @ SY503 @ SV1 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[50]) ).
thf(54,plain,
! [SV32: $i,SV29: $i,SV26: $i,SV23: $i,SV20: $i,SV17: $i,SV14: $i,SV11: $i,SV8: $i,SV5: $i,SV2: $i] :
( ( ! [SY504: $i,SY505: $i,SY506: $i,SY507: $i,SY508: $i,SY509: $i,SY510: $i,SY511: $i,SY512: $i] :
( ~ ( state @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SV26 @ SV29 @ SV32 @ SY504 @ SY505 @ SY506 @ SY507 @ SY508 @ SY509 @ SY510 @ SY511 @ SY512 )
| ( state @ SY512 @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SV26 @ SV29 @ SV32 @ SY504 @ SY505 @ SY506 @ SY507 @ SY508 @ SY509 @ SY510 @ SY511 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[51]) ).
thf(55,plain,
! [SV33: $i,SV30: $i,SV27: $i,SV24: $i,SV21: $i,SV18: $i,SV15: $i,SV12: $i,SV9: $i,SV6: $i,SV3: $i] :
( ( ! [SY513: $i,SY514: $i,SY515: $i,SY516: $i,SY517: $i,SY518: $i,SY519: $i,SY520: $i,SY521: $i] :
( ~ ( state @ SV3 @ SV6 @ SV9 @ SV12 @ SV15 @ SV18 @ SV21 @ SV24 @ SV27 @ SV30 @ SV33 @ SY513 @ SY514 @ SY515 @ SY516 @ SY517 @ SY518 @ SY519 @ SY520 @ SY521 )
| ( state @ SV12 @ SV9 @ SV6 @ SV3 @ SV15 @ SV18 @ SV21 @ SV24 @ SV27 @ SV30 @ SV33 @ SY513 @ SY514 @ SY515 @ SY516 @ SY517 @ SY518 @ SY519 @ SY520 @ SY521 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[52]) ).
thf(56,plain,
! [SV34: $i,SV31: $i,SV28: $i,SV25: $i,SV22: $i,SV19: $i,SV16: $i,SV13: $i,SV10: $i,SV7: $i,SV4: $i,SV1: $i] :
( ( ! [SY522: $i,SY523: $i,SY524: $i,SY525: $i,SY526: $i,SY527: $i,SY528: $i,SY529: $i] :
( ~ ( state @ SV1 @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SV25 @ SV28 @ SV31 @ SV34 @ SY522 @ SY523 @ SY524 @ SY525 @ SY526 @ SY527 @ SY528 @ SY529 )
| ( state @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SV25 @ SV28 @ SV31 @ SV34 @ SY522 @ SY523 @ SY524 @ SY525 @ SY526 @ SY527 @ SY528 @ SY529 @ SV1 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[53]) ).
thf(57,plain,
! [SV35: $i,SV32: $i,SV29: $i,SV26: $i,SV23: $i,SV20: $i,SV17: $i,SV14: $i,SV11: $i,SV8: $i,SV5: $i,SV2: $i] :
( ( ! [SY530: $i,SY531: $i,SY532: $i,SY533: $i,SY534: $i,SY535: $i,SY536: $i,SY537: $i] :
( ~ ( state @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SV26 @ SV29 @ SV32 @ SV35 @ SY530 @ SY531 @ SY532 @ SY533 @ SY534 @ SY535 @ SY536 @ SY537 )
| ( state @ SY537 @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SV26 @ SV29 @ SV32 @ SV35 @ SY530 @ SY531 @ SY532 @ SY533 @ SY534 @ SY535 @ SY536 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[54]) ).
thf(58,plain,
! [SV36: $i,SV33: $i,SV30: $i,SV27: $i,SV24: $i,SV21: $i,SV18: $i,SV15: $i,SV12: $i,SV9: $i,SV6: $i,SV3: $i] :
( ( ! [SY538: $i,SY539: $i,SY540: $i,SY541: $i,SY542: $i,SY543: $i,SY544: $i,SY545: $i] :
( ~ ( state @ SV3 @ SV6 @ SV9 @ SV12 @ SV15 @ SV18 @ SV21 @ SV24 @ SV27 @ SV30 @ SV33 @ SV36 @ SY538 @ SY539 @ SY540 @ SY541 @ SY542 @ SY543 @ SY544 @ SY545 )
| ( state @ SV12 @ SV9 @ SV6 @ SV3 @ SV15 @ SV18 @ SV21 @ SV24 @ SV27 @ SV30 @ SV33 @ SV36 @ SY538 @ SY539 @ SY540 @ SY541 @ SY542 @ SY543 @ SY544 @ SY545 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[55]) ).
thf(59,plain,
! [SV37: $i,SV34: $i,SV31: $i,SV28: $i,SV25: $i,SV22: $i,SV19: $i,SV16: $i,SV13: $i,SV10: $i,SV7: $i,SV4: $i,SV1: $i] :
( ( ! [SY546: $i,SY547: $i,SY548: $i,SY549: $i,SY550: $i,SY551: $i,SY552: $i] :
( ~ ( state @ SV1 @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SV25 @ SV28 @ SV31 @ SV34 @ SV37 @ SY546 @ SY547 @ SY548 @ SY549 @ SY550 @ SY551 @ SY552 )
| ( state @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SV25 @ SV28 @ SV31 @ SV34 @ SV37 @ SY546 @ SY547 @ SY548 @ SY549 @ SY550 @ SY551 @ SY552 @ SV1 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[56]) ).
thf(60,plain,
! [SV38: $i,SV35: $i,SV32: $i,SV29: $i,SV26: $i,SV23: $i,SV20: $i,SV17: $i,SV14: $i,SV11: $i,SV8: $i,SV5: $i,SV2: $i] :
( ( ! [SY553: $i,SY554: $i,SY555: $i,SY556: $i,SY557: $i,SY558: $i,SY559: $i] :
( ~ ( state @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SV26 @ SV29 @ SV32 @ SV35 @ SV38 @ SY553 @ SY554 @ SY555 @ SY556 @ SY557 @ SY558 @ SY559 )
| ( state @ SY559 @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SV26 @ SV29 @ SV32 @ SV35 @ SV38 @ SY553 @ SY554 @ SY555 @ SY556 @ SY557 @ SY558 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[57]) ).
thf(61,plain,
! [SV39: $i,SV36: $i,SV33: $i,SV30: $i,SV27: $i,SV24: $i,SV21: $i,SV18: $i,SV15: $i,SV12: $i,SV9: $i,SV6: $i,SV3: $i] :
( ( ! [SY560: $i,SY561: $i,SY562: $i,SY563: $i,SY564: $i,SY565: $i,SY566: $i] :
( ~ ( state @ SV3 @ SV6 @ SV9 @ SV12 @ SV15 @ SV18 @ SV21 @ SV24 @ SV27 @ SV30 @ SV33 @ SV36 @ SV39 @ SY560 @ SY561 @ SY562 @ SY563 @ SY564 @ SY565 @ SY566 )
| ( state @ SV12 @ SV9 @ SV6 @ SV3 @ SV15 @ SV18 @ SV21 @ SV24 @ SV27 @ SV30 @ SV33 @ SV36 @ SV39 @ SY560 @ SY561 @ SY562 @ SY563 @ SY564 @ SY565 @ SY566 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[58]) ).
thf(62,plain,
! [SV40: $i,SV37: $i,SV34: $i,SV31: $i,SV28: $i,SV25: $i,SV22: $i,SV19: $i,SV16: $i,SV13: $i,SV10: $i,SV7: $i,SV4: $i,SV1: $i] :
( ( ! [SY567: $i,SY568: $i,SY569: $i,SY570: $i,SY571: $i,SY572: $i] :
( ~ ( state @ SV1 @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SV25 @ SV28 @ SV31 @ SV34 @ SV37 @ SV40 @ SY567 @ SY568 @ SY569 @ SY570 @ SY571 @ SY572 )
| ( state @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SV25 @ SV28 @ SV31 @ SV34 @ SV37 @ SV40 @ SY567 @ SY568 @ SY569 @ SY570 @ SY571 @ SY572 @ SV1 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[59]) ).
thf(63,plain,
! [SV41: $i,SV38: $i,SV35: $i,SV32: $i,SV29: $i,SV26: $i,SV23: $i,SV20: $i,SV17: $i,SV14: $i,SV11: $i,SV8: $i,SV5: $i,SV2: $i] :
( ( ! [SY573: $i,SY574: $i,SY575: $i,SY576: $i,SY577: $i,SY578: $i] :
( ~ ( state @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SV26 @ SV29 @ SV32 @ SV35 @ SV38 @ SV41 @ SY573 @ SY574 @ SY575 @ SY576 @ SY577 @ SY578 )
| ( state @ SY578 @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SV26 @ SV29 @ SV32 @ SV35 @ SV38 @ SV41 @ SY573 @ SY574 @ SY575 @ SY576 @ SY577 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[60]) ).
thf(64,plain,
! [SV42: $i,SV39: $i,SV36: $i,SV33: $i,SV30: $i,SV27: $i,SV24: $i,SV21: $i,SV18: $i,SV15: $i,SV12: $i,SV9: $i,SV6: $i,SV3: $i] :
( ( ! [SY579: $i,SY580: $i,SY581: $i,SY582: $i,SY583: $i,SY584: $i] :
( ~ ( state @ SV3 @ SV6 @ SV9 @ SV12 @ SV15 @ SV18 @ SV21 @ SV24 @ SV27 @ SV30 @ SV33 @ SV36 @ SV39 @ SV42 @ SY579 @ SY580 @ SY581 @ SY582 @ SY583 @ SY584 )
| ( state @ SV12 @ SV9 @ SV6 @ SV3 @ SV15 @ SV18 @ SV21 @ SV24 @ SV27 @ SV30 @ SV33 @ SV36 @ SV39 @ SV42 @ SY579 @ SY580 @ SY581 @ SY582 @ SY583 @ SY584 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[61]) ).
thf(65,plain,
! [SV43: $i,SV40: $i,SV37: $i,SV34: $i,SV31: $i,SV28: $i,SV25: $i,SV22: $i,SV19: $i,SV16: $i,SV13: $i,SV10: $i,SV7: $i,SV4: $i,SV1: $i] :
( ( ! [SY585: $i,SY586: $i,SY587: $i,SY588: $i,SY589: $i] :
( ~ ( state @ SV1 @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SV25 @ SV28 @ SV31 @ SV34 @ SV37 @ SV40 @ SV43 @ SY585 @ SY586 @ SY587 @ SY588 @ SY589 )
| ( state @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SV25 @ SV28 @ SV31 @ SV34 @ SV37 @ SV40 @ SV43 @ SY585 @ SY586 @ SY587 @ SY588 @ SY589 @ SV1 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[62]) ).
thf(66,plain,
! [SV44: $i,SV41: $i,SV38: $i,SV35: $i,SV32: $i,SV29: $i,SV26: $i,SV23: $i,SV20: $i,SV17: $i,SV14: $i,SV11: $i,SV8: $i,SV5: $i,SV2: $i] :
( ( ! [SY590: $i,SY591: $i,SY592: $i,SY593: $i,SY594: $i] :
( ~ ( state @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SV26 @ SV29 @ SV32 @ SV35 @ SV38 @ SV41 @ SV44 @ SY590 @ SY591 @ SY592 @ SY593 @ SY594 )
| ( state @ SY594 @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SV26 @ SV29 @ SV32 @ SV35 @ SV38 @ SV41 @ SV44 @ SY590 @ SY591 @ SY592 @ SY593 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[63]) ).
thf(67,plain,
! [SV45: $i,SV42: $i,SV39: $i,SV36: $i,SV33: $i,SV30: $i,SV27: $i,SV24: $i,SV21: $i,SV18: $i,SV15: $i,SV12: $i,SV9: $i,SV6: $i,SV3: $i] :
( ( ! [SY595: $i,SY596: $i,SY597: $i,SY598: $i,SY599: $i] :
( ~ ( state @ SV3 @ SV6 @ SV9 @ SV12 @ SV15 @ SV18 @ SV21 @ SV24 @ SV27 @ SV30 @ SV33 @ SV36 @ SV39 @ SV42 @ SV45 @ SY595 @ SY596 @ SY597 @ SY598 @ SY599 )
| ( state @ SV12 @ SV9 @ SV6 @ SV3 @ SV15 @ SV18 @ SV21 @ SV24 @ SV27 @ SV30 @ SV33 @ SV36 @ SV39 @ SV42 @ SV45 @ SY595 @ SY596 @ SY597 @ SY598 @ SY599 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[64]) ).
thf(68,plain,
! [SV46: $i,SV43: $i,SV40: $i,SV37: $i,SV34: $i,SV31: $i,SV28: $i,SV25: $i,SV22: $i,SV19: $i,SV16: $i,SV13: $i,SV10: $i,SV7: $i,SV4: $i,SV1: $i] :
( ( ! [SY600: $i,SY601: $i,SY602: $i,SY603: $i] :
( ~ ( state @ SV1 @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SV25 @ SV28 @ SV31 @ SV34 @ SV37 @ SV40 @ SV43 @ SV46 @ SY600 @ SY601 @ SY602 @ SY603 )
| ( state @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SV25 @ SV28 @ SV31 @ SV34 @ SV37 @ SV40 @ SV43 @ SV46 @ SY600 @ SY601 @ SY602 @ SY603 @ SV1 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[65]) ).
thf(69,plain,
! [SV47: $i,SV44: $i,SV41: $i,SV38: $i,SV35: $i,SV32: $i,SV29: $i,SV26: $i,SV23: $i,SV20: $i,SV17: $i,SV14: $i,SV11: $i,SV8: $i,SV5: $i,SV2: $i] :
( ( ! [SY604: $i,SY605: $i,SY606: $i,SY607: $i] :
( ~ ( state @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SV26 @ SV29 @ SV32 @ SV35 @ SV38 @ SV41 @ SV44 @ SV47 @ SY604 @ SY605 @ SY606 @ SY607 )
| ( state @ SY607 @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SV26 @ SV29 @ SV32 @ SV35 @ SV38 @ SV41 @ SV44 @ SV47 @ SY604 @ SY605 @ SY606 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[66]) ).
thf(70,plain,
! [SV48: $i,SV45: $i,SV42: $i,SV39: $i,SV36: $i,SV33: $i,SV30: $i,SV27: $i,SV24: $i,SV21: $i,SV18: $i,SV15: $i,SV12: $i,SV9: $i,SV6: $i,SV3: $i] :
( ( ! [SY608: $i,SY609: $i,SY610: $i,SY611: $i] :
( ~ ( state @ SV3 @ SV6 @ SV9 @ SV12 @ SV15 @ SV18 @ SV21 @ SV24 @ SV27 @ SV30 @ SV33 @ SV36 @ SV39 @ SV42 @ SV45 @ SV48 @ SY608 @ SY609 @ SY610 @ SY611 )
| ( state @ SV12 @ SV9 @ SV6 @ SV3 @ SV15 @ SV18 @ SV21 @ SV24 @ SV27 @ SV30 @ SV33 @ SV36 @ SV39 @ SV42 @ SV45 @ SV48 @ SY608 @ SY609 @ SY610 @ SY611 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[67]) ).
thf(71,plain,
! [SV49: $i,SV46: $i,SV43: $i,SV40: $i,SV37: $i,SV34: $i,SV31: $i,SV28: $i,SV25: $i,SV22: $i,SV19: $i,SV16: $i,SV13: $i,SV10: $i,SV7: $i,SV4: $i,SV1: $i] :
( ( ! [SY612: $i,SY613: $i,SY614: $i] :
( ~ ( state @ SV1 @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SV25 @ SV28 @ SV31 @ SV34 @ SV37 @ SV40 @ SV43 @ SV46 @ SV49 @ SY612 @ SY613 @ SY614 )
| ( state @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SV25 @ SV28 @ SV31 @ SV34 @ SV37 @ SV40 @ SV43 @ SV46 @ SV49 @ SY612 @ SY613 @ SY614 @ SV1 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[68]) ).
thf(72,plain,
! [SV50: $i,SV47: $i,SV44: $i,SV41: $i,SV38: $i,SV35: $i,SV32: $i,SV29: $i,SV26: $i,SV23: $i,SV20: $i,SV17: $i,SV14: $i,SV11: $i,SV8: $i,SV5: $i,SV2: $i] :
( ( ! [SY615: $i,SY616: $i,SY617: $i] :
( ~ ( state @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SV26 @ SV29 @ SV32 @ SV35 @ SV38 @ SV41 @ SV44 @ SV47 @ SV50 @ SY615 @ SY616 @ SY617 )
| ( state @ SY617 @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SV26 @ SV29 @ SV32 @ SV35 @ SV38 @ SV41 @ SV44 @ SV47 @ SV50 @ SY615 @ SY616 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[69]) ).
thf(73,plain,
! [SV51: $i,SV48: $i,SV45: $i,SV42: $i,SV39: $i,SV36: $i,SV33: $i,SV30: $i,SV27: $i,SV24: $i,SV21: $i,SV18: $i,SV15: $i,SV12: $i,SV9: $i,SV6: $i,SV3: $i] :
( ( ! [SY618: $i,SY619: $i,SY620: $i] :
( ~ ( state @ SV3 @ SV6 @ SV9 @ SV12 @ SV15 @ SV18 @ SV21 @ SV24 @ SV27 @ SV30 @ SV33 @ SV36 @ SV39 @ SV42 @ SV45 @ SV48 @ SV51 @ SY618 @ SY619 @ SY620 )
| ( state @ SV12 @ SV9 @ SV6 @ SV3 @ SV15 @ SV18 @ SV21 @ SV24 @ SV27 @ SV30 @ SV33 @ SV36 @ SV39 @ SV42 @ SV45 @ SV48 @ SV51 @ SY618 @ SY619 @ SY620 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[70]) ).
thf(74,plain,
! [SV52: $i,SV49: $i,SV46: $i,SV43: $i,SV40: $i,SV37: $i,SV34: $i,SV31: $i,SV28: $i,SV25: $i,SV22: $i,SV19: $i,SV16: $i,SV13: $i,SV10: $i,SV7: $i,SV4: $i,SV1: $i] :
( ( ! [SY621: $i,SY622: $i] :
( ~ ( state @ SV1 @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SV25 @ SV28 @ SV31 @ SV34 @ SV37 @ SV40 @ SV43 @ SV46 @ SV49 @ SV52 @ SY621 @ SY622 )
| ( state @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SV25 @ SV28 @ SV31 @ SV34 @ SV37 @ SV40 @ SV43 @ SV46 @ SV49 @ SV52 @ SY621 @ SY622 @ SV1 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[71]) ).
thf(75,plain,
! [SV53: $i,SV50: $i,SV47: $i,SV44: $i,SV41: $i,SV38: $i,SV35: $i,SV32: $i,SV29: $i,SV26: $i,SV23: $i,SV20: $i,SV17: $i,SV14: $i,SV11: $i,SV8: $i,SV5: $i,SV2: $i] :
( ( ! [SY623: $i,SY624: $i] :
( ~ ( state @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SV26 @ SV29 @ SV32 @ SV35 @ SV38 @ SV41 @ SV44 @ SV47 @ SV50 @ SV53 @ SY623 @ SY624 )
| ( state @ SY624 @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SV26 @ SV29 @ SV32 @ SV35 @ SV38 @ SV41 @ SV44 @ SV47 @ SV50 @ SV53 @ SY623 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[72]) ).
thf(76,plain,
! [SV54: $i,SV51: $i,SV48: $i,SV45: $i,SV42: $i,SV39: $i,SV36: $i,SV33: $i,SV30: $i,SV27: $i,SV24: $i,SV21: $i,SV18: $i,SV15: $i,SV12: $i,SV9: $i,SV6: $i,SV3: $i] :
( ( ! [SY625: $i,SY626: $i] :
( ~ ( state @ SV3 @ SV6 @ SV9 @ SV12 @ SV15 @ SV18 @ SV21 @ SV24 @ SV27 @ SV30 @ SV33 @ SV36 @ SV39 @ SV42 @ SV45 @ SV48 @ SV51 @ SV54 @ SY625 @ SY626 )
| ( state @ SV12 @ SV9 @ SV6 @ SV3 @ SV15 @ SV18 @ SV21 @ SV24 @ SV27 @ SV30 @ SV33 @ SV36 @ SV39 @ SV42 @ SV45 @ SV48 @ SV51 @ SV54 @ SY625 @ SY626 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[73]) ).
thf(77,plain,
! [SV55: $i,SV52: $i,SV49: $i,SV46: $i,SV43: $i,SV40: $i,SV37: $i,SV34: $i,SV31: $i,SV28: $i,SV25: $i,SV22: $i,SV19: $i,SV16: $i,SV13: $i,SV10: $i,SV7: $i,SV4: $i,SV1: $i] :
( ( ! [SY627: $i] :
( ~ ( state @ SV1 @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SV25 @ SV28 @ SV31 @ SV34 @ SV37 @ SV40 @ SV43 @ SV46 @ SV49 @ SV52 @ SV55 @ SY627 )
| ( state @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SV25 @ SV28 @ SV31 @ SV34 @ SV37 @ SV40 @ SV43 @ SV46 @ SV49 @ SV52 @ SV55 @ SY627 @ SV1 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[74]) ).
thf(78,plain,
! [SV56: $i,SV53: $i,SV50: $i,SV47: $i,SV44: $i,SV41: $i,SV38: $i,SV35: $i,SV32: $i,SV29: $i,SV26: $i,SV23: $i,SV20: $i,SV17: $i,SV14: $i,SV11: $i,SV8: $i,SV5: $i,SV2: $i] :
( ( ! [SY628: $i] :
( ~ ( state @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SV26 @ SV29 @ SV32 @ SV35 @ SV38 @ SV41 @ SV44 @ SV47 @ SV50 @ SV53 @ SV56 @ SY628 )
| ( state @ SY628 @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SV26 @ SV29 @ SV32 @ SV35 @ SV38 @ SV41 @ SV44 @ SV47 @ SV50 @ SV53 @ SV56 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[75]) ).
thf(79,plain,
! [SV57: $i,SV54: $i,SV51: $i,SV48: $i,SV45: $i,SV42: $i,SV39: $i,SV36: $i,SV33: $i,SV30: $i,SV27: $i,SV24: $i,SV21: $i,SV18: $i,SV15: $i,SV12: $i,SV9: $i,SV6: $i,SV3: $i] :
( ( ! [SY629: $i] :
( ~ ( state @ SV3 @ SV6 @ SV9 @ SV12 @ SV15 @ SV18 @ SV21 @ SV24 @ SV27 @ SV30 @ SV33 @ SV36 @ SV39 @ SV42 @ SV45 @ SV48 @ SV51 @ SV54 @ SV57 @ SY629 )
| ( state @ SV12 @ SV9 @ SV6 @ SV3 @ SV15 @ SV18 @ SV21 @ SV24 @ SV27 @ SV30 @ SV33 @ SV36 @ SV39 @ SV42 @ SV45 @ SV48 @ SV51 @ SV54 @ SV57 @ SY629 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[76]) ).
thf(80,plain,
! [SV58: $i,SV55: $i,SV52: $i,SV49: $i,SV46: $i,SV43: $i,SV40: $i,SV37: $i,SV34: $i,SV31: $i,SV28: $i,SV25: $i,SV22: $i,SV19: $i,SV16: $i,SV13: $i,SV10: $i,SV7: $i,SV4: $i,SV1: $i] :
( ( ~ ( state @ SV1 @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SV25 @ SV28 @ SV31 @ SV34 @ SV37 @ SV40 @ SV43 @ SV46 @ SV49 @ SV52 @ SV55 @ SV58 )
| ( state @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SV25 @ SV28 @ SV31 @ SV34 @ SV37 @ SV40 @ SV43 @ SV46 @ SV49 @ SV52 @ SV55 @ SV58 @ SV1 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[77]) ).
thf(81,plain,
! [SV59: $i,SV56: $i,SV53: $i,SV50: $i,SV47: $i,SV44: $i,SV41: $i,SV38: $i,SV35: $i,SV32: $i,SV29: $i,SV26: $i,SV23: $i,SV20: $i,SV17: $i,SV14: $i,SV11: $i,SV8: $i,SV5: $i,SV2: $i] :
( ( ~ ( state @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SV26 @ SV29 @ SV32 @ SV35 @ SV38 @ SV41 @ SV44 @ SV47 @ SV50 @ SV53 @ SV56 @ SV59 )
| ( state @ SV59 @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SV26 @ SV29 @ SV32 @ SV35 @ SV38 @ SV41 @ SV44 @ SV47 @ SV50 @ SV53 @ SV56 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[78]) ).
thf(82,plain,
! [SV60: $i,SV57: $i,SV54: $i,SV51: $i,SV48: $i,SV45: $i,SV42: $i,SV39: $i,SV36: $i,SV33: $i,SV30: $i,SV27: $i,SV24: $i,SV21: $i,SV18: $i,SV15: $i,SV12: $i,SV9: $i,SV6: $i,SV3: $i] :
( ( ~ ( state @ SV3 @ SV6 @ SV9 @ SV12 @ SV15 @ SV18 @ SV21 @ SV24 @ SV27 @ SV30 @ SV33 @ SV36 @ SV39 @ SV42 @ SV45 @ SV48 @ SV51 @ SV54 @ SV57 @ SV60 )
| ( state @ SV12 @ SV9 @ SV6 @ SV3 @ SV15 @ SV18 @ SV21 @ SV24 @ SV27 @ SV30 @ SV33 @ SV36 @ SV39 @ SV42 @ SV45 @ SV48 @ SV51 @ SV54 @ SV57 @ SV60 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[79]) ).
thf(83,plain,
! [SV58: $i,SV55: $i,SV52: $i,SV49: $i,SV46: $i,SV43: $i,SV40: $i,SV37: $i,SV34: $i,SV31: $i,SV28: $i,SV25: $i,SV22: $i,SV19: $i,SV16: $i,SV13: $i,SV10: $i,SV7: $i,SV4: $i,SV1: $i] :
( ( ( ~ ( state @ SV1 @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SV25 @ SV28 @ SV31 @ SV34 @ SV37 @ SV40 @ SV43 @ SV46 @ SV49 @ SV52 @ SV55 @ SV58 ) )
= $true )
| ( ( state @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SV25 @ SV28 @ SV31 @ SV34 @ SV37 @ SV40 @ SV43 @ SV46 @ SV49 @ SV52 @ SV55 @ SV58 @ SV1 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[80]) ).
thf(84,plain,
! [SV59: $i,SV56: $i,SV53: $i,SV50: $i,SV47: $i,SV44: $i,SV41: $i,SV38: $i,SV35: $i,SV32: $i,SV29: $i,SV26: $i,SV23: $i,SV20: $i,SV17: $i,SV14: $i,SV11: $i,SV8: $i,SV5: $i,SV2: $i] :
( ( ( ~ ( state @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SV26 @ SV29 @ SV32 @ SV35 @ SV38 @ SV41 @ SV44 @ SV47 @ SV50 @ SV53 @ SV56 @ SV59 ) )
= $true )
| ( ( state @ SV59 @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SV26 @ SV29 @ SV32 @ SV35 @ SV38 @ SV41 @ SV44 @ SV47 @ SV50 @ SV53 @ SV56 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[81]) ).
thf(85,plain,
! [SV60: $i,SV57: $i,SV54: $i,SV51: $i,SV48: $i,SV45: $i,SV42: $i,SV39: $i,SV36: $i,SV33: $i,SV30: $i,SV27: $i,SV24: $i,SV21: $i,SV18: $i,SV15: $i,SV12: $i,SV9: $i,SV6: $i,SV3: $i] :
( ( ( ~ ( state @ SV3 @ SV6 @ SV9 @ SV12 @ SV15 @ SV18 @ SV21 @ SV24 @ SV27 @ SV30 @ SV33 @ SV36 @ SV39 @ SV42 @ SV45 @ SV48 @ SV51 @ SV54 @ SV57 @ SV60 ) )
= $true )
| ( ( state @ SV12 @ SV9 @ SV6 @ SV3 @ SV15 @ SV18 @ SV21 @ SV24 @ SV27 @ SV30 @ SV33 @ SV36 @ SV39 @ SV42 @ SV45 @ SV48 @ SV51 @ SV54 @ SV57 @ SV60 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[82]) ).
thf(86,plain,
! [SV58: $i,SV55: $i,SV52: $i,SV49: $i,SV46: $i,SV43: $i,SV40: $i,SV37: $i,SV34: $i,SV31: $i,SV28: $i,SV25: $i,SV22: $i,SV19: $i,SV16: $i,SV13: $i,SV10: $i,SV7: $i,SV4: $i,SV1: $i] :
( ( ( state @ SV1 @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SV25 @ SV28 @ SV31 @ SV34 @ SV37 @ SV40 @ SV43 @ SV46 @ SV49 @ SV52 @ SV55 @ SV58 )
= $false )
| ( ( state @ SV4 @ SV7 @ SV10 @ SV13 @ SV16 @ SV19 @ SV22 @ SV25 @ SV28 @ SV31 @ SV34 @ SV37 @ SV40 @ SV43 @ SV46 @ SV49 @ SV52 @ SV55 @ SV58 @ SV1 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[83]) ).
thf(87,plain,
! [SV59: $i,SV56: $i,SV53: $i,SV50: $i,SV47: $i,SV44: $i,SV41: $i,SV38: $i,SV35: $i,SV32: $i,SV29: $i,SV26: $i,SV23: $i,SV20: $i,SV17: $i,SV14: $i,SV11: $i,SV8: $i,SV5: $i,SV2: $i] :
( ( ( state @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SV26 @ SV29 @ SV32 @ SV35 @ SV38 @ SV41 @ SV44 @ SV47 @ SV50 @ SV53 @ SV56 @ SV59 )
= $false )
| ( ( state @ SV59 @ SV2 @ SV5 @ SV8 @ SV11 @ SV14 @ SV17 @ SV20 @ SV23 @ SV26 @ SV29 @ SV32 @ SV35 @ SV38 @ SV41 @ SV44 @ SV47 @ SV50 @ SV53 @ SV56 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[84]) ).
thf(88,plain,
! [SV60: $i,SV57: $i,SV54: $i,SV51: $i,SV48: $i,SV45: $i,SV42: $i,SV39: $i,SV36: $i,SV33: $i,SV30: $i,SV27: $i,SV24: $i,SV21: $i,SV18: $i,SV15: $i,SV12: $i,SV9: $i,SV6: $i,SV3: $i] :
( ( ( state @ SV3 @ SV6 @ SV9 @ SV12 @ SV15 @ SV18 @ SV21 @ SV24 @ SV27 @ SV30 @ SV33 @ SV36 @ SV39 @ SV42 @ SV45 @ SV48 @ SV51 @ SV54 @ SV57 @ SV60 )
= $false )
| ( ( state @ SV12 @ SV9 @ SV6 @ SV3 @ SV15 @ SV18 @ SV21 @ SV24 @ SV27 @ SV30 @ SV33 @ SV36 @ SV39 @ SV42 @ SV45 @ SV48 @ SV51 @ SV54 @ SV57 @ SV60 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[85]) ).
thf(89,plain,
$false = $true,
inference(fo_atp_e,[status(thm)],[16,88,87,86,25,21]) ).
thf(90,plain,
$false,
inference(solved_all_splits,[solved_all_splits(join,[])],[89]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ036-1.005 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.04 % Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.17 % Computer : n002.cluster.edu
% 0.11/0.17 % Model : x86_64 x86_64
% 0.11/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.17 % Memory : 8046.5625MB
% 0.11/0.17 % OS : Linux 6.8.0-71-generic
% 0.11/0.17 % CPULimit : 300
% 0.11/0.17 % WCLimit : 300
% 0.11/0.17 % DateTime : Tue Oct 6 14:00:52 UTC 2026
% 0.11/0.17 % CPUTime :
% 0.11/0.17 Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.77/1.53
% 6.77/1.53 No.of.Axioms: 5
% 6.77/1.53
% 6.77/1.53 Length.of.Defs: 0
% 6.77/1.53
% 6.77/1.53 Contains.Choice.Funs: false
% 6.77/1.53 ........
% 6.77/1.53
% 6.77/1.53 ********************************
% 6.77/1.53 * All subproblems solved! *
% 6.77/1.53 ********************************
% 6.77/1.53 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:1,axioms:5,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:299,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:89,loop_count:0,foatp_calls:1,translation:fof_full)
% 6.77/1.53
% 6.77/1.53 %**** Beginning of derivation protocol ****
% 6.77/1.53 % SZS output start CNFRefutation
% See solution above
% 6.77/1.53
% 6.77/1.53 %**** End of derivation protocol ****
% 6.77/1.53 %**** no. of clauses in derivation: 90 ****
% 6.77/1.53 %**** clause counter: 89 ****
% 6.77/1.53
% 6.77/1.53 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:1,axioms:5,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:299,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:89,loop_count:0,foatp_calls:1,translation:fof_full)
%------------------------------------------------------------------------------