%------------------------------------------------------------------------------
% File : SATCoP---0.1
% Problem : HWV108-1 : TPTP v8.1.0. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : satcop --statistics %s
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Sat Jul 16 19:10:05 EDT 2022
% Result : Unsatisfiable 182.74s 24.06s
% Output : Proof 182.74s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(g0,plain,
~ v4914(sK23533_VarCurr),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490112)]) ).
cnf(g1,plain,
v81(sK23533_VarCurr),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490113)]) ).
cnf(g2,plain,
~ v28947(sK23533_VarCurr),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490114)]) ).
cnf(g3,plain,
( v28941(sK23533_VarCurr,bitIndex1)
| v28941(sK23533_VarCurr,bitIndex2)
| v28941(sK23533_VarCurr,bitIndex0)
| v26522(sK23533_VarCurr,bitIndex1)
| v26522(sK23533_VarCurr,bitIndex2)
| v26522(sK23533_VarCurr,bitIndex0)
| sP24007
| sP24008
| sP24009
| sP24010
| sP24011
| sP24012
| sP24013
| sP24014
| sP24015
| sP24016
| sP24017
| sP24018
| sP24019
| sP24020
| sP24021
| sP24022
| sP24023
| sP24024
| sP24025
| sP24026
| sP24027
| sP24028
| sP24029
| sP24030
| sP24031
| sP24032
| sP24033
| sP24034
| sP24035
| sP24036
| sP24037
| sP24038
| sP24039
| sP24040
| sP24041
| sP24042
| sP24043
| sP24044
| sP24045
| sP24046
| sP24047
| sP24048
| sP24049
| sP24050
| sP24051
| sP24052
| sP24053
| sP24054
| sP24055
| sP24056
| sP24057
| sP24058
| sP24059
| sP24060
| sP24061
| sP24062
| sP24063 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490115)]) ).
cnf(g4,plain,
( ~ v28941(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex2)
| v28941(sK23533_VarCurr,bitIndex1)
| v28941(sK23533_VarCurr,bitIndex0)
| v26522(sK23533_VarCurr,bitIndex1)
| v26522(sK23533_VarCurr,bitIndex0)
| sP24007
| sP24008
| sP24009
| sP24010
| sP24011
| sP24012
| sP24013
| sP24014
| sP24015
| sP24016
| sP24017
| sP24018
| sP24019
| sP24020
| sP24021
| sP24022
| sP24023
| sP24024
| sP24025
| sP24026
| sP24027
| sP24028
| sP24029
| sP24030
| sP24031
| sP24032
| sP24033
| sP24034
| sP24035
| sP24036
| sP24037
| sP24038
| sP24039
| sP24040
| sP24041
| sP24042
| sP24043
| sP24044
| sP24045
| sP24046
| sP24047
| sP24048
| sP24049
| sP24050
| sP24051
| sP24052
| sP24053
| sP24054
| sP24055
| sP24056
| sP24057
| sP24058
| sP24059
| sP24060
| sP24061
| sP24062
| sP24063 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490116)]) ).
cnf(g5,plain,
( ~ v28941(sK23533_VarCurr,bitIndex1)
| ~ v26522(sK23533_VarCurr,bitIndex1)
| v28941(sK23533_VarCurr,bitIndex2)
| v28941(sK23533_VarCurr,bitIndex0)
| v26522(sK23533_VarCurr,bitIndex2)
| v26522(sK23533_VarCurr,bitIndex0)
| sP24007
| sP24008
| sP24009
| sP24010
| sP24011
| sP24012
| sP24013
| sP24014
| sP24015
| sP24016
| sP24017
| sP24018
| sP24019
| sP24020
| sP24021
| sP24022
| sP24023
| sP24024
| sP24025
| sP24026
| sP24027
| sP24028
| sP24029
| sP24030
| sP24031
| sP24032
| sP24033
| sP24034
| sP24035
| sP24036
| sP24037
| sP24038
| sP24039
| sP24040
| sP24041
| sP24042
| sP24043
| sP24044
| sP24045
| sP24046
| sP24047
| sP24048
| sP24049
| sP24050
| sP24051
| sP24052
| sP24053
| sP24054
| sP24055
| sP24056
| sP24057
| sP24058
| sP24059
| sP24060
| sP24061
| sP24062
| sP24063 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490117)]) ).
cnf(g6,plain,
( ~ v28941(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex1)
| ~ v26522(sK23533_VarCurr,bitIndex2)
| v28941(sK23533_VarCurr,bitIndex0)
| v26522(sK23533_VarCurr,bitIndex0)
| sP24007
| sP24008
| sP24009
| sP24010
| sP24011
| sP24012
| sP24013
| sP24014
| sP24015
| sP24016
| sP24017
| sP24018
| sP24019
| sP24020
| sP24021
| sP24022
| sP24023
| sP24024
| sP24025
| sP24026
| sP24027
| sP24028
| sP24029
| sP24030
| sP24031
| sP24032
| sP24033
| sP24034
| sP24035
| sP24036
| sP24037
| sP24038
| sP24039
| sP24040
| sP24041
| sP24042
| sP24043
| sP24044
| sP24045
| sP24046
| sP24047
| sP24048
| sP24049
| sP24050
| sP24051
| sP24052
| sP24053
| sP24054
| sP24055
| sP24056
| sP24057
| sP24058
| sP24059
| sP24060
| sP24061
| sP24062
| sP24063 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490118)]) ).
cnf(g7,plain,
( ~ v28941(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex0)
| v28941(sK23533_VarCurr,bitIndex1)
| v28941(sK23533_VarCurr,bitIndex2)
| v26522(sK23533_VarCurr,bitIndex1)
| v26522(sK23533_VarCurr,bitIndex2)
| sP24007
| sP24008
| sP24009
| sP24010
| sP24011
| sP24012
| sP24013
| sP24014
| sP24015
| sP24016
| sP24017
| sP24018
| sP24019
| sP24020
| sP24021
| sP24022
| sP24023
| sP24024
| sP24025
| sP24026
| sP24027
| sP24028
| sP24029
| sP24030
| sP24031
| sP24032
| sP24033
| sP24034
| sP24035
| sP24036
| sP24037
| sP24038
| sP24039
| sP24040
| sP24041
| sP24042
| sP24043
| sP24044
| sP24045
| sP24046
| sP24047
| sP24048
| sP24049
| sP24050
| sP24051
| sP24052
| sP24053
| sP24054
| sP24055
| sP24056
| sP24057
| sP24058
| sP24059
| sP24060
| sP24061
| sP24062
| sP24063 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490119)]) ).
cnf(g8,plain,
( ~ v28941(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex0)
| v28941(sK23533_VarCurr,bitIndex1)
| v26522(sK23533_VarCurr,bitIndex1)
| sP24007
| sP24008
| sP24009
| sP24010
| sP24011
| sP24012
| sP24013
| sP24014
| sP24015
| sP24016
| sP24017
| sP24018
| sP24019
| sP24020
| sP24021
| sP24022
| sP24023
| sP24024
| sP24025
| sP24026
| sP24027
| sP24028
| sP24029
| sP24030
| sP24031
| sP24032
| sP24033
| sP24034
| sP24035
| sP24036
| sP24037
| sP24038
| sP24039
| sP24040
| sP24041
| sP24042
| sP24043
| sP24044
| sP24045
| sP24046
| sP24047
| sP24048
| sP24049
| sP24050
| sP24051
| sP24052
| sP24053
| sP24054
| sP24055
| sP24056
| sP24057
| sP24058
| sP24059
| sP24060
| sP24061
| sP24062
| sP24063 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490120)]) ).
cnf(g9,plain,
( ~ v28941(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex1)
| ~ v26522(sK23533_VarCurr,bitIndex0)
| v28941(sK23533_VarCurr,bitIndex2)
| v26522(sK23533_VarCurr,bitIndex2)
| sP24007
| sP24008
| sP24009
| sP24010
| sP24011
| sP24012
| sP24013
| sP24014
| sP24015
| sP24016
| sP24017
| sP24018
| sP24019
| sP24020
| sP24021
| sP24022
| sP24023
| sP24024
| sP24025
| sP24026
| sP24027
| sP24028
| sP24029
| sP24030
| sP24031
| sP24032
| sP24033
| sP24034
| sP24035
| sP24036
| sP24037
| sP24038
| sP24039
| sP24040
| sP24041
| sP24042
| sP24043
| sP24044
| sP24045
| sP24046
| sP24047
| sP24048
| sP24049
| sP24050
| sP24051
| sP24052
| sP24053
| sP24054
| sP24055
| sP24056
| sP24057
| sP24058
| sP24059
| sP24060
| sP24061
| sP24062
| sP24063 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490121)]) ).
cnf(g10,plain,
( ~ v28941(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex1)
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex0)
| sP24007
| sP24008
| sP24009
| sP24010
| sP24011
| sP24012
| sP24013
| sP24014
| sP24015
| sP24016
| sP24017
| sP24018
| sP24019
| sP24020
| sP24021
| sP24022
| sP24023
| sP24024
| sP24025
| sP24026
| sP24027
| sP24028
| sP24029
| sP24030
| sP24031
| sP24032
| sP24033
| sP24034
| sP24035
| sP24036
| sP24037
| sP24038
| sP24039
| sP24040
| sP24041
| sP24042
| sP24043
| sP24044
| sP24045
| sP24046
| sP24047
| sP24048
| sP24049
| sP24050
| sP24051
| sP24052
| sP24053
| sP24054
| sP24055
| sP24056
| sP24057
| sP24058
| sP24059
| sP24060
| sP24061
| sP24062
| sP24063 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490122)]) ).
cnf(g11,plain,
( v69(sK23533_VarCurr)
| v23(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490123)]) ).
cnf(g12,plain,
( v69(sK23533_VarCurr)
| v21(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490124)]) ).
cnf(g13,plain,
( ~ sP24042
| v28941(sK23533_VarCurr,bitIndex24)
| v26522(sK23533_VarCurr,bitIndex24) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490212)]) ).
cnf(g14,plain,
( ~ v28941(sK23533_VarCurr,bitIndex21)
| ~ v26522(sK23533_VarCurr,bitIndex21)
| ~ sP24045 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490201)]) ).
cnf(g15,plain,
( ~ sP24045
| v28941(sK23533_VarCurr,bitIndex21)
| v26522(sK23533_VarCurr,bitIndex21) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490200)]) ).
cnf(g16,plain,
( ~ sP24025
| v28941(sK23533_VarCurr,bitIndex41)
| v26522(sK23533_VarCurr,bitIndex41) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490280)]) ).
cnf(g17,plain,
( ~ sP24014
| v28941(sK23533_VarCurr,bitIndex52)
| v26522(sK23533_VarCurr,bitIndex52) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490324)]) ).
cnf(g18,plain,
( ~ v28941(sK23533_VarCurr,bitIndex17)
| ~ v26522(sK23533_VarCurr,bitIndex17)
| ~ sP24049 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490185)]) ).
cnf(g19,plain,
( ~ sP24049
| v28941(sK23533_VarCurr,bitIndex17)
| v26522(sK23533_VarCurr,bitIndex17) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490184)]) ).
cnf(g20,plain,
( ~ sP24059
| v28941(sK23533_VarCurr,bitIndex7)
| v26522(sK23533_VarCurr,bitIndex7) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490144)]) ).
cnf(g21,plain,
( ~ sP24056
| v28941(sK23533_VarCurr,bitIndex10)
| v26522(sK23533_VarCurr,bitIndex10) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490156)]) ).
cnf(g22,plain,
( ~ v28941(sK23533_VarCurr,bitIndex1)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex1) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g23,plain,
( ~ v28941(sK23533_VarCurr,bitIndex56)
| ~ v26522(sK23533_VarCurr,bitIndex56)
| ~ sP24010 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490341)]) ).
cnf(g24,plain,
( ~ sP24010
| v28941(sK23533_VarCurr,bitIndex56)
| v26522(sK23533_VarCurr,bitIndex56) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490340)]) ).
cnf(g25,plain,
( ~ sP24047
| v28941(sK23533_VarCurr,bitIndex19)
| v26522(sK23533_VarCurr,bitIndex19) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490192)]) ).
cnf(g26,plain,
( ~ sP24029
| v28941(sK23533_VarCurr,bitIndex37)
| v26522(sK23533_VarCurr,bitIndex37) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490264)]) ).
cnf(g27,plain,
( ~ v26522(sK23533_VarCurr,bitIndex2)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex2) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g28,plain,
( ~ sP24052
| v28941(sK23533_VarCurr,bitIndex14)
| v26522(sK23533_VarCurr,bitIndex14) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490172)]) ).
cnf(g29,plain,
( ~ v28941(sK23533_VarCurr,bitIndex2)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex2) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g30,plain,
( ~ v28941(sK23533_VarCurr,bitIndex43)
| ~ v26522(sK23533_VarCurr,bitIndex43)
| ~ sP24023 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490289)]) ).
cnf(g31,plain,
( ~ sP24023
| v28941(sK23533_VarCurr,bitIndex43)
| v26522(sK23533_VarCurr,bitIndex43) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490288)]) ).
cnf(g32,plain,
( ~ v28941(sK23533_VarCurr,bitIndex47)
| ~ v26522(sK23533_VarCurr,bitIndex47)
| ~ sP24019 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490305)]) ).
cnf(g33,plain,
( ~ sP24019
| v28941(sK23533_VarCurr,bitIndex47)
| v26522(sK23533_VarCurr,bitIndex47) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490304)]) ).
cnf(g34,plain,
( ~ v28941(sK23533_VarCurr,bitIndex11)
| ~ v26522(sK23533_VarCurr,bitIndex11)
| ~ sP24055 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490161)]) ).
cnf(g35,plain,
( ~ sP24055
| v28941(sK23533_VarCurr,bitIndex11)
| v26522(sK23533_VarCurr,bitIndex11) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490160)]) ).
cnf(g36,plain,
( ~ v28941(sK23533_VarCurr,bitIndex49)
| ~ v26522(sK23533_VarCurr,bitIndex49)
| ~ sP24017 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490313)]) ).
cnf(g37,plain,
( ~ sP24017
| v28941(sK23533_VarCurr,bitIndex49)
| v26522(sK23533_VarCurr,bitIndex49) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490312)]) ).
cnf(g38,plain,
( ~ v28941(sK23533_VarCurr,bitIndex20)
| ~ v26522(sK23533_VarCurr,bitIndex20)
| ~ sP24046 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490197)]) ).
cnf(g39,plain,
( ~ sP24046
| v28941(sK23533_VarCurr,bitIndex20)
| v26522(sK23533_VarCurr,bitIndex20) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490196)]) ).
cnf(g40,plain,
( ~ sP24036
| v28941(sK23533_VarCurr,bitIndex30)
| v26522(sK23533_VarCurr,bitIndex30) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490236)]) ).
cnf(g41,plain,
( ~ sP24050
| v28941(sK23533_VarCurr,bitIndex16)
| v26522(sK23533_VarCurr,bitIndex16) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490180)]) ).
cnf(g42,plain,
( ~ v28941(sK23533_VarCurr,bitIndex40)
| ~ v26522(sK23533_VarCurr,bitIndex40)
| ~ sP24026 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490277)]) ).
cnf(g43,plain,
( ~ sP24026
| v28941(sK23533_VarCurr,bitIndex40)
| v26522(sK23533_VarCurr,bitIndex40) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490276)]) ).
cnf(g44,plain,
( ~ sP24032
| v28941(sK23533_VarCurr,bitIndex34)
| v26522(sK23533_VarCurr,bitIndex34) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490252)]) ).
cnf(g45,plain,
( ~ sP24053
| v28941(sK23533_VarCurr,bitIndex13)
| v26522(sK23533_VarCurr,bitIndex13) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490168)]) ).
cnf(g46,plain,
( ~ sP24041
| v28941(sK23533_VarCurr,bitIndex25)
| v26522(sK23533_VarCurr,bitIndex25) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490216)]) ).
cnf(g47,plain,
( ~ sP24027
| v28941(sK23533_VarCurr,bitIndex39)
| v26522(sK23533_VarCurr,bitIndex39) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490272)]) ).
cnf(g48,plain,
( ~ v28941(sK23533_VarCurr,bitIndex6)
| ~ v26522(sK23533_VarCurr,bitIndex6)
| ~ sP24060 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490141)]) ).
cnf(g49,plain,
( ~ sP24060
| v28941(sK23533_VarCurr,bitIndex6)
| v26522(sK23533_VarCurr,bitIndex6) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490140)]) ).
cnf(g50,plain,
( ~ sP24030
| v28941(sK23533_VarCurr,bitIndex36)
| v26522(sK23533_VarCurr,bitIndex36) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490260)]) ).
cnf(g51,plain,
( ~ sP24015
| v28941(sK23533_VarCurr,bitIndex51)
| v26522(sK23533_VarCurr,bitIndex51) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490320)]) ).
cnf(g52,plain,
( ~ v28941(sK23533_VarCurr,bitIndex18)
| ~ v26522(sK23533_VarCurr,bitIndex18)
| ~ sP24048 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490189)]) ).
cnf(g53,plain,
( ~ sP24048
| v28941(sK23533_VarCurr,bitIndex18)
| v26522(sK23533_VarCurr,bitIndex18) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490188)]) ).
cnf(g54,plain,
( ~ v28941(sK23533_VarCurr,bitIndex15)
| ~ v26522(sK23533_VarCurr,bitIndex15)
| ~ sP24051 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490177)]) ).
cnf(g55,plain,
( ~ sP24051
| v28941(sK23533_VarCurr,bitIndex15)
| v26522(sK23533_VarCurr,bitIndex15) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490176)]) ).
cnf(g56,plain,
( ~ v28941(sK23533_VarCurr,bitIndex57)
| ~ v26522(sK23533_VarCurr,bitIndex57)
| ~ sP24009 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490345)]) ).
cnf(g57,plain,
( ~ sP24009
| v28941(sK23533_VarCurr,bitIndex57)
| v26522(sK23533_VarCurr,bitIndex57) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490344)]) ).
cnf(g58,plain,
( ~ v28941(sK23533_VarCurr,bitIndex48)
| ~ v26522(sK23533_VarCurr,bitIndex48)
| ~ sP24018 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490309)]) ).
cnf(g59,plain,
( ~ sP24018
| v28941(sK23533_VarCurr,bitIndex48)
| v26522(sK23533_VarCurr,bitIndex48) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490308)]) ).
cnf(g60,plain,
( ~ v28941(sK23533_VarCurr,bitIndex35)
| ~ v26522(sK23533_VarCurr,bitIndex35)
| ~ sP24031 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490257)]) ).
cnf(g61,plain,
( ~ sP24031
| v28941(sK23533_VarCurr,bitIndex35)
| v26522(sK23533_VarCurr,bitIndex35) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490256)]) ).
cnf(g62,plain,
( ~ v28941(sK23533_VarCurr,bitIndex58)
| ~ v26522(sK23533_VarCurr,bitIndex58)
| ~ sP24008 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490349)]) ).
cnf(g63,plain,
( ~ sP24008
| v28941(sK23533_VarCurr,bitIndex58)
| v26522(sK23533_VarCurr,bitIndex58) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490348)]) ).
cnf(g64,plain,
( ~ v26522(sK23533_VarCurr,bitIndex1)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex1) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g65,plain,
( ~ sP24044
| v28941(sK23533_VarCurr,bitIndex22)
| v26522(sK23533_VarCurr,bitIndex22) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490204)]) ).
cnf(g66,plain,
( ~ v28941(sK23533_VarCurr,bitIndex50)
| ~ v26522(sK23533_VarCurr,bitIndex50)
| ~ sP24016 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490317)]) ).
cnf(g67,plain,
( ~ sP24016
| v28941(sK23533_VarCurr,bitIndex50)
| v26522(sK23533_VarCurr,bitIndex50) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490316)]) ).
cnf(g68,plain,
( ~ sP24061
| v28941(sK23533_VarCurr,bitIndex5)
| v26522(sK23533_VarCurr,bitIndex5) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490136)]) ).
cnf(g69,plain,
( ~ sP24035
| v28941(sK23533_VarCurr,bitIndex31)
| v26522(sK23533_VarCurr,bitIndex31) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490240)]) ).
cnf(g70,plain,
( ~ sP24058
| v28941(sK23533_VarCurr,bitIndex8)
| v26522(sK23533_VarCurr,bitIndex8) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490148)]) ).
cnf(g71,plain,
( ~ v28941(sK23533_VarCurr,bitIndex23)
| ~ v26522(sK23533_VarCurr,bitIndex23)
| ~ sP24043 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490209)]) ).
cnf(g72,plain,
( ~ sP24043
| v28941(sK23533_VarCurr,bitIndex23)
| v26522(sK23533_VarCurr,bitIndex23) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490208)]) ).
cnf(g73,plain,
( ~ v28941(sK23533_VarCurr,bitIndex29)
| ~ v26522(sK23533_VarCurr,bitIndex29)
| ~ sP24037 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490233)]) ).
cnf(g74,plain,
( ~ sP24037
| v28941(sK23533_VarCurr,bitIndex29)
| v26522(sK23533_VarCurr,bitIndex29) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490232)]) ).
cnf(g75,plain,
( ~ sP24022
| v28941(sK23533_VarCurr,bitIndex44)
| v26522(sK23533_VarCurr,bitIndex44) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490292)]) ).
cnf(g76,plain,
( ~ v28941(sK23533_VarCurr,bitIndex33)
| ~ v26522(sK23533_VarCurr,bitIndex33)
| ~ sP24033 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490249)]) ).
cnf(g77,plain,
( ~ sP24033
| v28941(sK23533_VarCurr,bitIndex33)
| v26522(sK23533_VarCurr,bitIndex33) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490248)]) ).
cnf(g78,plain,
( ~ v28941(sK23533_VarCurr,bitIndex55)
| ~ v26522(sK23533_VarCurr,bitIndex55)
| ~ sP24011 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490337)]) ).
cnf(g79,plain,
( ~ sP24011
| v28941(sK23533_VarCurr,bitIndex55)
| v26522(sK23533_VarCurr,bitIndex55) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490336)]) ).
cnf(g80,plain,
( ~ v26522(sK23533_VarCurr,bitIndex0)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex0) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g81,plain,
( ~ v28941(sK23533_VarCurr,bitIndex3)
| ~ v26522(sK23533_VarCurr,bitIndex3)
| ~ sP24063 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490129)]) ).
cnf(g82,plain,
( ~ sP24063
| v28941(sK23533_VarCurr,bitIndex3)
| v26522(sK23533_VarCurr,bitIndex3) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490128)]) ).
cnf(g83,plain,
( ~ v28941(sK23533_VarCurr,bitIndex54)
| ~ v26522(sK23533_VarCurr,bitIndex54)
| ~ sP24012 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490333)]) ).
cnf(g84,plain,
( ~ sP24012
| v28941(sK23533_VarCurr,bitIndex54)
| v26522(sK23533_VarCurr,bitIndex54) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490332)]) ).
cnf(g85,plain,
( ~ sP24057
| v28941(sK23533_VarCurr,bitIndex9)
| v26522(sK23533_VarCurr,bitIndex9) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490152)]) ).
cnf(g86,plain,
( ~ v28941(sK23533_VarCurr,bitIndex42)
| ~ v26522(sK23533_VarCurr,bitIndex42)
| ~ sP24024 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490285)]) ).
cnf(g87,plain,
( ~ sP24024
| v28941(sK23533_VarCurr,bitIndex42)
| v26522(sK23533_VarCurr,bitIndex42) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490284)]) ).
cnf(g88,plain,
( ~ v28941(sK23533_VarCurr,bitIndex26)
| ~ v26522(sK23533_VarCurr,bitIndex26)
| ~ sP24040 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490221)]) ).
cnf(g89,plain,
( ~ sP24040
| v28941(sK23533_VarCurr,bitIndex26)
| v26522(sK23533_VarCurr,bitIndex26) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490220)]) ).
cnf(g90,plain,
( ~ sP24062
| v28941(sK23533_VarCurr,bitIndex4)
| v26522(sK23533_VarCurr,bitIndex4) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490132)]) ).
cnf(g91,plain,
( ~ sP24020
| v28941(sK23533_VarCurr,bitIndex46)
| v26522(sK23533_VarCurr,bitIndex46) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490300)]) ).
cnf(g92,plain,
( ~ sP24021
| v28941(sK23533_VarCurr,bitIndex45)
| v26522(sK23533_VarCurr,bitIndex45) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490296)]) ).
cnf(g93,plain,
( ~ v28941(sK23533_VarCurr,bitIndex53)
| ~ v26522(sK23533_VarCurr,bitIndex53)
| ~ sP24013 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490329)]) ).
cnf(g94,plain,
( ~ sP24013
| v28941(sK23533_VarCurr,bitIndex53)
| v26522(sK23533_VarCurr,bitIndex53) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490328)]) ).
cnf(g95,plain,
( ~ sP24039
| v28941(sK23533_VarCurr,bitIndex27)
| v26522(sK23533_VarCurr,bitIndex27) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490224)]) ).
cnf(g96,plain,
( ~ sP24028
| v28941(sK23533_VarCurr,bitIndex38)
| v26522(sK23533_VarCurr,bitIndex38) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490268)]) ).
cnf(g97,plain,
( ~ v28941(sK23533_VarCurr,bitIndex59)
| ~ v26522(sK23533_VarCurr,bitIndex59)
| ~ sP24007 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490353)]) ).
cnf(g98,plain,
( ~ sP24007
| v28941(sK23533_VarCurr,bitIndex59)
| v26522(sK23533_VarCurr,bitIndex59) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490352)]) ).
cnf(g99,plain,
( ~ v28941(sK23533_VarCurr,bitIndex28)
| ~ v26522(sK23533_VarCurr,bitIndex28)
| ~ sP24038 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490229)]) ).
cnf(g100,plain,
( ~ sP24038
| v28941(sK23533_VarCurr,bitIndex28)
| v26522(sK23533_VarCurr,bitIndex28) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490228)]) ).
cnf(g101,plain,
( ~ v28941(sK23533_VarCurr,bitIndex32)
| ~ v26522(sK23533_VarCurr,bitIndex32)
| ~ sP24034 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490245)]) ).
cnf(g102,plain,
( ~ sP24034
| v28941(sK23533_VarCurr,bitIndex32)
| v26522(sK23533_VarCurr,bitIndex32) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490244)]) ).
cnf(g103,plain,
( ~ v28941(sK23533_VarCurr,bitIndex25)
| ~ v26522(sK23533_VarCurr,bitIndex25)
| ~ sP24041 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490217)]) ).
cnf(g104,plain,
( ~ v28941(sK23533_VarCurr,bitIndex9)
| ~ v26522(sK23533_VarCurr,bitIndex9)
| ~ sP24057 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490153)]) ).
cnf(g105,plain,
( ~ v28941(sK23533_VarCurr,bitIndex46)
| ~ v26522(sK23533_VarCurr,bitIndex46)
| ~ sP24020 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490301)]) ).
cnf(g106,plain,
( ~ v28941(sK23533_VarCurr,bitIndex39)
| ~ v26522(sK23533_VarCurr,bitIndex39)
| ~ sP24027 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490273)]) ).
cnf(g107,plain,
( ~ v28941(sK23533_VarCurr,bitIndex30)
| ~ v26522(sK23533_VarCurr,bitIndex30)
| ~ sP24036 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490237)]) ).
cnf(g108,plain,
( ~ v28945(sK23533_VarCurr,bitIndex2)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex2) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g109,plain,
( ~ v28946(sK23533_VarCurr,bitIndex1)
| v28941(sK23533_VarCurr,bitIndex1)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g110,plain,
( ~ v28941(sK23533_VarCurr,bitIndex13)
| ~ v26522(sK23533_VarCurr,bitIndex13)
| ~ sP24053 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490169)]) ).
cnf(g111,plain,
( ~ v28941(sK23533_VarCurr,bitIndex4)
| ~ v26522(sK23533_VarCurr,bitIndex4)
| ~ sP24062 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490133)]) ).
cnf(g112,plain,
( ~ v28946(sK23533_VarCurr,bitIndex2)
| v28941(sK23533_VarCurr,bitIndex2)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g113,plain,
( ~ v28941(sK23533_VarCurr,bitIndex24)
| ~ v26522(sK23533_VarCurr,bitIndex24)
| ~ sP24042 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490213)]) ).
cnf(g114,plain,
( ~ v28941(sK23533_VarCurr,bitIndex7)
| ~ v26522(sK23533_VarCurr,bitIndex7)
| ~ sP24059 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490145)]) ).
cnf(g115,plain,
( ~ sP24054
| v28941(sK23533_VarCurr,bitIndex12)
| v26522(sK23533_VarCurr,bitIndex12) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490164)]) ).
cnf(g116,plain,
( ~ v28946(sK23533_VarCurr,bitIndex0)
| v28941(sK23533_VarCurr,bitIndex0)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g117,plain,
( ~ v28941(sK23533_VarCurr,bitIndex38)
| ~ v26522(sK23533_VarCurr,bitIndex38)
| ~ sP24028 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490269)]) ).
cnf(g118,plain,
( ~ v28945(sK23533_VarCurr,bitIndex0)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex0) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g119,plain,
( ~ v28941(sK23533_VarCurr,bitIndex31)
| ~ v26522(sK23533_VarCurr,bitIndex31)
| ~ sP24035 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490241)]) ).
cnf(g120,plain,
( ~ v69(sK23533_VarCurr)
| ~ sP38_aig_name(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u705125)]) ).
cnf(g121,plain,
( ~ sP38_aig_name(sK23533_VarCurr)
| ~ v23(sK23533_VarCurr)
| ~ v21(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u705126)]) ).
cnf(g122,plain,
( ~ v28941(sK23533_VarCurr,bitIndex5)
| ~ v26522(sK23533_VarCurr,bitIndex5)
| ~ sP24061 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490137)]) ).
cnf(g123,plain,
( ~ v28941(sK23533_VarCurr,bitIndex8)
| ~ v26522(sK23533_VarCurr,bitIndex8)
| ~ sP24058 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490149)]) ).
cnf(g124,plain,
( ~ v28941(sK23533_VarCurr,bitIndex41)
| ~ v26522(sK23533_VarCurr,bitIndex41)
| ~ sP24025 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490281)]) ).
cnf(g125,plain,
( ~ v28941(sK23533_VarCurr,bitIndex14)
| ~ v26522(sK23533_VarCurr,bitIndex14)
| ~ sP24052 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490173)]) ).
cnf(g126,plain,
( ~ v28941(sK23533_VarCurr,bitIndex12)
| ~ v26522(sK23533_VarCurr,bitIndex12)
| ~ sP24054 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490165)]) ).
cnf(g127,plain,
( ~ v28941(sK23533_VarCurr,bitIndex22)
| ~ v26522(sK23533_VarCurr,bitIndex22)
| ~ sP24044 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490205)]) ).
cnf(g128,plain,
( ~ v28941(sK23533_VarCurr,bitIndex37)
| ~ v26522(sK23533_VarCurr,bitIndex37)
| ~ sP24029 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490265)]) ).
cnf(g129,plain,
( ~ v28941(sK23533_VarCurr,bitIndex45)
| ~ v26522(sK23533_VarCurr,bitIndex45)
| ~ sP24021 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490297)]) ).
cnf(g130,plain,
( ~ v28941(sK23533_VarCurr,bitIndex27)
| ~ v26522(sK23533_VarCurr,bitIndex27)
| ~ sP24039 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490225)]) ).
cnf(g131,plain,
( ~ v28941(sK23533_VarCurr,bitIndex36)
| ~ v26522(sK23533_VarCurr,bitIndex36)
| ~ sP24030 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490261)]) ).
cnf(g132,plain,
( ~ v28941(sK23533_VarCurr,bitIndex44)
| ~ v26522(sK23533_VarCurr,bitIndex44)
| ~ sP24022 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490293)]) ).
cnf(g133,plain,
( ~ v28941(sK23533_VarCurr,bitIndex19)
| ~ v26522(sK23533_VarCurr,bitIndex19)
| ~ sP24047 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490193)]) ).
cnf(g134,plain,
( ~ v28941(sK23533_VarCurr,bitIndex34)
| ~ v26522(sK23533_VarCurr,bitIndex34)
| ~ sP24032 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490253)]) ).
cnf(g135,plain,
( ~ v28941(sK23533_VarCurr,bitIndex52)
| ~ v26522(sK23533_VarCurr,bitIndex52)
| ~ sP24014 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490325)]) ).
cnf(g136,plain,
( ~ v28941(sK23533_VarCurr,bitIndex0)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex0) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g137,plain,
( ~ v28941(sK23533_VarCurr,bitIndex16)
| ~ v26522(sK23533_VarCurr,bitIndex16)
| ~ sP24050 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490181)]) ).
cnf(g138,plain,
( ~ v28941(sK23533_VarCurr,bitIndex10)
| ~ v26522(sK23533_VarCurr,bitIndex10)
| ~ sP24056 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490157)]) ).
cnf(g139,plain,
( ~ v28945(sK23533_VarCurr,bitIndex1)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex1) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g140,plain,
( ~ v28941(sK23533_VarCurr,bitIndex51)
| ~ v26522(sK23533_VarCurr,bitIndex51)
| ~ sP24015 ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490321)]) ).
cnf(g141,plain,
( ~ v28941(sK23533_VarCurr,bitIndex6)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex6) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g142,plain,
( ~ v28941(sK23533_VarCurr,bitIndex56)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex56) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g143,plain,
( ~ v28941(sK23533_VarCurr,bitIndex51)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex51) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g144,plain,
( ~ v28941(sK23533_VarCurr,bitIndex28)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex28) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g145,plain,
( ~ v28941(sK23533_VarCurr,bitIndex38)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex38) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g146,plain,
( ~ v28941(sK23533_VarCurr,bitIndex48)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex48) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g147,plain,
( ~ v28941(sK23533_VarCurr,bitIndex19)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex19) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g148,plain,
( ~ v28941(sK23533_VarCurr,bitIndex31)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex31) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g149,plain,
( ~ v28941(sK23533_VarCurr,bitIndex16)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex16) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g150,plain,
( ~ v28941(sK23533_VarCurr,bitIndex55)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex55) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g151,plain,
( ~ v28941(sK23533_VarCurr,bitIndex58)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex58) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g152,plain,
( ~ v28941(sK23533_VarCurr,bitIndex49)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex49) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g153,plain,
( ~ v28941(sK23533_VarCurr,bitIndex54)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex54) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g154,plain,
( ~ v28941(sK23533_VarCurr,bitIndex7)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex7) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g155,plain,
( ~ v28941(sK23533_VarCurr,bitIndex12)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex12) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g156,plain,
( ~ v28941(sK23533_VarCurr,bitIndex46)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex46) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g157,plain,
( ~ v28941(sK23533_VarCurr,bitIndex14)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex14) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g158,plain,
( ~ v28941(sK23533_VarCurr,bitIndex13)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex13) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g159,plain,
( ~ v28941(sK23533_VarCurr,bitIndex50)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex50) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g160,plain,
( ~ v28941(sK23533_VarCurr,bitIndex29)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex29) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g161,plain,
( ~ v28941(sK23533_VarCurr,bitIndex35)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex35) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g162,plain,
( ~ v28941(sK23533_VarCurr,bitIndex32)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex32) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g163,plain,
( ~ v28941(sK23533_VarCurr,bitIndex47)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex47) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g164,plain,
( ~ v28941(sK23533_VarCurr,bitIndex43)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex43) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g165,plain,
( ~ v28941(sK23533_VarCurr,bitIndex25)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex25) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g166,plain,
( ~ v28941(sK23533_VarCurr,bitIndex20)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex20) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g167,plain,
( ~ v28941(sK23533_VarCurr,bitIndex17)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex17) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g168,plain,
( ~ v28941(sK23533_VarCurr,bitIndex8)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex8) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g169,plain,
( ~ v28941(sK23533_VarCurr,bitIndex27)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex27) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g170,plain,
( ~ v28941(sK23533_VarCurr,bitIndex24)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex24) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g171,plain,
( ~ v28941(sK23533_VarCurr,bitIndex18)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex18) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g172,plain,
( ~ v28941(sK23533_VarCurr,bitIndex36)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex36) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g173,plain,
( ~ v28941(sK23533_VarCurr,bitIndex57)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex57) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g174,plain,
( ~ v28941(sK23533_VarCurr,bitIndex21)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex21) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g175,plain,
( ~ v28941(sK23533_VarCurr,bitIndex26)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex26) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g176,plain,
( ~ v28941(sK23533_VarCurr,bitIndex9)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex9) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g177,plain,
( ~ v28941(sK23533_VarCurr,bitIndex22)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex22) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g178,plain,
( ~ v28941(sK23533_VarCurr,bitIndex53)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex53) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g179,plain,
( ~ v28941(sK23533_VarCurr,bitIndex11)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex11) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g180,plain,
( ~ v28941(sK23533_VarCurr,bitIndex15)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex15) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g181,plain,
( ~ v28941(sK23533_VarCurr,bitIndex44)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex44) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g182,plain,
( ~ v28941(sK23533_VarCurr,bitIndex52)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex52) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g183,plain,
( ~ v28941(sK23533_VarCurr,bitIndex30)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex30) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g184,plain,
( ~ v28941(sK23533_VarCurr,bitIndex3)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex3) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g185,plain,
( ~ v28941(sK23533_VarCurr,bitIndex40)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex40) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g186,plain,
( ~ v28941(sK23533_VarCurr,bitIndex42)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex42) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g187,plain,
( ~ v28941(sK23533_VarCurr,bitIndex5)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex5) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g188,plain,
( ~ v28941(sK23533_VarCurr,bitIndex4)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex4) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g189,plain,
( ~ v28941(sK23533_VarCurr,bitIndex34)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex34) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g190,plain,
( ~ v28941(sK23533_VarCurr,bitIndex41)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex41) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g191,plain,
( ~ v28941(sK23533_VarCurr,bitIndex39)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex39) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g192,plain,
( ~ v28941(sK23533_VarCurr,bitIndex10)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex10) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g193,plain,
( ~ v28941(sK23533_VarCurr,bitIndex23)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex23) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g194,plain,
( ~ v28941(sK23533_VarCurr,bitIndex33)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex33) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g195,plain,
( ~ v28941(sK23533_VarCurr,bitIndex59)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex59) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g196,plain,
( ~ v28941(sK23533_VarCurr,bitIndex45)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex45) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g197,plain,
( ~ v28941(sK23533_VarCurr,bitIndex37)
| v28947(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex37) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807)]) ).
cnf(g198,plain,
( ~ v28946(sK23533_VarCurr,bitIndex17)
| v28941(sK23533_VarCurr,bitIndex17)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g199,plain,
( ~ v28945(sK23533_VarCurr,bitIndex11)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex11) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g200,plain,
( ~ v28946(sK23533_VarCurr,bitIndex14)
| v28941(sK23533_VarCurr,bitIndex14)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g201,plain,
( ~ v28946(sK23533_VarCurr,bitIndex16)
| v28941(sK23533_VarCurr,bitIndex16)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g202,plain,
( ~ v28946(sK23533_VarCurr,bitIndex56)
| v28941(sK23533_VarCurr,bitIndex56)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g203,plain,
( ~ v28945(sK23533_VarCurr,bitIndex26)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex26) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g204,plain,
( ~ v28946(sK23533_VarCurr,bitIndex26)
| v28941(sK23533_VarCurr,bitIndex26)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g205,plain,
( ~ v28946(sK23533_VarCurr,bitIndex42)
| v28941(sK23533_VarCurr,bitIndex42)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g206,plain,
( ~ v28946(sK23533_VarCurr,bitIndex23)
| v28941(sK23533_VarCurr,bitIndex23)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g207,plain,
( ~ v28945(sK23533_VarCurr,bitIndex35)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex35) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g208,plain,
( ~ v28945(sK23533_VarCurr,bitIndex58)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex58) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g209,plain,
( ~ v28946(sK23533_VarCurr,bitIndex58)
| v28941(sK23533_VarCurr,bitIndex58)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g210,plain,
( ~ v28946(sK23533_VarCurr,bitIndex32)
| v28941(sK23533_VarCurr,bitIndex32)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g211,plain,
( ~ v26522(sK23533_VarCurr,bitIndex32)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex32) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g212,plain,
( ~ v28945(sK23533_VarCurr,bitIndex5)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex5) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g213,plain,
( ~ v28946(sK23533_VarCurr,bitIndex5)
| v28941(sK23533_VarCurr,bitIndex5)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g214,plain,
( ~ v28946(sK23533_VarCurr,bitIndex9)
| v28941(sK23533_VarCurr,bitIndex9)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g215,plain,
( ~ v28945(sK23533_VarCurr,bitIndex9)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex9) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g216,plain,
( ~ v28945(sK23533_VarCurr,bitIndex45)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex45) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g217,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex2)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex2) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g218,plain,
( ~ v28946(sK23533_VarCurr,bitIndex54)
| v28941(sK23533_VarCurr,bitIndex54)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g219,plain,
( ~ v28946(sK23533_VarCurr,bitIndex35)
| v28941(sK23533_VarCurr,bitIndex35)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g220,plain,
( ~ v28946(sK23533_VarCurr,bitIndex59)
| v28941(sK23533_VarCurr,bitIndex59)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g221,plain,
( ~ v28945(sK23533_VarCurr,bitIndex54)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex54) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g222,plain,
( ~ v28945(sK23533_VarCurr,bitIndex3)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex3) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g223,plain,
( ~ v28946(sK23533_VarCurr,bitIndex55)
| v28941(sK23533_VarCurr,bitIndex55)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g224,plain,
( ~ v28945(sK23533_VarCurr,bitIndex29)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex29) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g225,plain,
( ~ v28946(sK23533_VarCurr,bitIndex29)
| v28941(sK23533_VarCurr,bitIndex29)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g226,plain,
( ~ v28945(sK23533_VarCurr,bitIndex20)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex20) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g227,plain,
( ~ v28945(sK23533_VarCurr,bitIndex41)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex41) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g228,plain,
( ~ v28945(sK23533_VarCurr,bitIndex21)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex21) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g229,plain,
( ~ v28946(sK23533_VarCurr,bitIndex21)
| v28941(sK23533_VarCurr,bitIndex21)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g230,plain,
( ~ v28945(sK23533_VarCurr,bitIndex42)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex42) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g231,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex0)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex0) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g232,plain,
( ~ v28945(sK23533_VarCurr,bitIndex14)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex14) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g233,plain,
( ~ v28946(sK23533_VarCurr,bitIndex50)
| v28941(sK23533_VarCurr,bitIndex50)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g234,plain,
( ~ v28946(sK23533_VarCurr,bitIndex25)
| v28941(sK23533_VarCurr,bitIndex25)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g235,plain,
( ~ v28946(sK23533_VarCurr,bitIndex38)
| v28941(sK23533_VarCurr,bitIndex38)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g236,plain,
( ~ v28945(sK23533_VarCurr,bitIndex53)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex53) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g237,plain,
( ~ v28946(sK23533_VarCurr,bitIndex44)
| v28941(sK23533_VarCurr,bitIndex44)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g238,plain,
( ~ v28945(sK23533_VarCurr,bitIndex27)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex27) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g239,plain,
( ~ v28946(sK23533_VarCurr,bitIndex20)
| v28941(sK23533_VarCurr,bitIndex20)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g240,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex26)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex26) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g241,plain,
( ~ v28945(sK23533_VarCurr,bitIndex46)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex46) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g242,plain,
( ~ v28946(sK23533_VarCurr,bitIndex46)
| v28941(sK23533_VarCurr,bitIndex46)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g243,plain,
( ~ v28945(sK23533_VarCurr,bitIndex36)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex36) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g244,plain,
( ~ v28946(sK23533_VarCurr,bitIndex36)
| v28941(sK23533_VarCurr,bitIndex36)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g245,plain,
( ~ v28945(sK23533_VarCurr,bitIndex39)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex39) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g246,plain,
( ~ v28945(sK23533_VarCurr,bitIndex43)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex43) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g247,plain,
( ~ v28946(sK23533_VarCurr,bitIndex3)
| v28941(sK23533_VarCurr,bitIndex3)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g248,plain,
( ~ v28945(sK23533_VarCurr,bitIndex22)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex22) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g249,plain,
( ~ v28945(sK23533_VarCurr,bitIndex37)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex37) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g250,plain,
( ~ v28946(sK23533_VarCurr,bitIndex48)
| v28941(sK23533_VarCurr,bitIndex48)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g251,plain,
( ~ v28946(sK23533_VarCurr,bitIndex19)
| v28941(sK23533_VarCurr,bitIndex19)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g252,plain,
( ~ v28946(sK23533_VarCurr,bitIndex49)
| v28941(sK23533_VarCurr,bitIndex49)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g253,plain,
( ~ v28946(sK23533_VarCurr,bitIndex12)
| v28941(sK23533_VarCurr,bitIndex12)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g254,plain,
( ~ v28945(sK23533_VarCurr,bitIndex12)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex12) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g255,plain,
( ~ v28946(sK23533_VarCurr,bitIndex57)
| v28941(sK23533_VarCurr,bitIndex57)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g256,plain,
( ~ v28946(sK23533_VarCurr,bitIndex34)
| v28941(sK23533_VarCurr,bitIndex34)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g257,plain,
( ~ v28946(sK23533_VarCurr,bitIndex41)
| v28941(sK23533_VarCurr,bitIndex41)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g258,plain,
( ~ v28946(sK23533_VarCurr,bitIndex45)
| v28941(sK23533_VarCurr,bitIndex45)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g259,plain,
( ~ v28946(sK23533_VarCurr,bitIndex10)
| v28941(sK23533_VarCurr,bitIndex10)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g260,plain,
( ~ v28945(sK23533_VarCurr,bitIndex10)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex10) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g261,plain,
( ~ v28945(sK23533_VarCurr,bitIndex19)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex19) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g262,plain,
( ~ v28946(sK23533_VarCurr,bitIndex4)
| v28941(sK23533_VarCurr,bitIndex4)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g263,plain,
( ~ v28946(sK23533_VarCurr,bitIndex39)
| v28941(sK23533_VarCurr,bitIndex39)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g264,plain,
( ~ v28946(sK23533_VarCurr,bitIndex13)
| v28941(sK23533_VarCurr,bitIndex13)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g265,plain,
( ~ v28945(sK23533_VarCurr,bitIndex25)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex25) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g266,plain,
( ~ v28945(sK23533_VarCurr,bitIndex15)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex15) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g267,plain,
( ~ v28946(sK23533_VarCurr,bitIndex7)
| v28941(sK23533_VarCurr,bitIndex7)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g268,plain,
( ~ v28945(sK23533_VarCurr,bitIndex57)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex57) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g269,plain,
( ~ v28945(sK23533_VarCurr,bitIndex17)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex17) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g270,plain,
( ~ v28946(sK23533_VarCurr,bitIndex37)
| v28941(sK23533_VarCurr,bitIndex37)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g271,plain,
( ~ v28945(sK23533_VarCurr,bitIndex33)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex33) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g272,plain,
( ~ v28945(sK23533_VarCurr,bitIndex56)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex56) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g273,plain,
( ~ v28945(sK23533_VarCurr,bitIndex18)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex18) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g274,plain,
( ~ v28945(sK23533_VarCurr,bitIndex48)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex48) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g275,plain,
( ~ v28946(sK23533_VarCurr,bitIndex43)
| v28941(sK23533_VarCurr,bitIndex43)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g276,plain,
( ~ v28945(sK23533_VarCurr,bitIndex40)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex40) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g277,plain,
( ~ v28945(sK23533_VarCurr,bitIndex55)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex55) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g278,plain,
( ~ v28946(sK23533_VarCurr,bitIndex11)
| v28941(sK23533_VarCurr,bitIndex11)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g279,plain,
( ~ v28946(sK23533_VarCurr,bitIndex24)
| v28941(sK23533_VarCurr,bitIndex24)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g280,plain,
( ~ v28945(sK23533_VarCurr,bitIndex24)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex24) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g281,plain,
( ~ v28946(sK23533_VarCurr,bitIndex22)
| v28941(sK23533_VarCurr,bitIndex22)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g282,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex0)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex0) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g283,plain,
( ~ v28945(sK23533_VarCurr,bitIndex38)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex38) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g284,plain,
( ~ v28945(sK23533_VarCurr,bitIndex34)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex34) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g285,plain,
( ~ v28945(sK23533_VarCurr,bitIndex50)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex50) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g286,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex2)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex2) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g287,plain,
( ~ v28945(sK23533_VarCurr,bitIndex59)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex59) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g288,plain,
( ~ v28946(sK23533_VarCurr,bitIndex8)
| v28941(sK23533_VarCurr,bitIndex8)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g289,plain,
( ~ v28946(sK23533_VarCurr,bitIndex31)
| v28941(sK23533_VarCurr,bitIndex31)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g290,plain,
( ~ v28945(sK23533_VarCurr,bitIndex31)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex31) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g291,plain,
( ~ v28946(sK23533_VarCurr,bitIndex15)
| v28941(sK23533_VarCurr,bitIndex15)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g292,plain,
( ~ v28945(sK23533_VarCurr,bitIndex13)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex13) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g293,plain,
( ~ v28945(sK23533_VarCurr,bitIndex49)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex49) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g294,plain,
( ~ v28946(sK23533_VarCurr,bitIndex6)
| v28941(sK23533_VarCurr,bitIndex6)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g295,plain,
( ~ v28945(sK23533_VarCurr,bitIndex8)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex8) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g296,plain,
( ~ v28945(sK23533_VarCurr,bitIndex44)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex44) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g297,plain,
( ~ v28945(sK23533_VarCurr,bitIndex28)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex28) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g298,plain,
( ~ v28946(sK23533_VarCurr,bitIndex18)
| v28941(sK23533_VarCurr,bitIndex18)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g299,plain,
( ~ v28946(sK23533_VarCurr,bitIndex51)
| v28941(sK23533_VarCurr,bitIndex51)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g300,plain,
( ~ v28945(sK23533_VarCurr,bitIndex51)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex51) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g301,plain,
( ~ v28946(sK23533_VarCurr,bitIndex52)
| v28941(sK23533_VarCurr,bitIndex52)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g302,plain,
( ~ v28946(sK23533_VarCurr,bitIndex27)
| v28941(sK23533_VarCurr,bitIndex27)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g303,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex1)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex1) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g304,plain,
( ~ v28945(sK23533_VarCurr,bitIndex23)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex23) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g305,plain,
( ~ v28945(sK23533_VarCurr,bitIndex16)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex16) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g306,plain,
( ~ v28946(sK23533_VarCurr,bitIndex33)
| v28941(sK23533_VarCurr,bitIndex33)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g307,plain,
( ~ v28945(sK23533_VarCurr,bitIndex4)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex4) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g308,plain,
( ~ v28946(sK23533_VarCurr,bitIndex40)
| v28941(sK23533_VarCurr,bitIndex40)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g309,plain,
( ~ v28945(sK23533_VarCurr,bitIndex7)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex7) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g310,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex1)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex1) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g311,plain,
( ~ v28945(sK23533_VarCurr,bitIndex52)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex52) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g312,plain,
( ~ v28945(sK23533_VarCurr,bitIndex6)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex6) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g313,plain,
( ~ v28945(sK23533_VarCurr,bitIndex47)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex47) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g314,plain,
( ~ v28946(sK23533_VarCurr,bitIndex47)
| v28941(sK23533_VarCurr,bitIndex47)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g315,plain,
( ~ v28946(sK23533_VarCurr,bitIndex53)
| v28941(sK23533_VarCurr,bitIndex53)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g316,plain,
( ~ v28945(sK23533_VarCurr,bitIndex30)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex30) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
cnf(g317,plain,
( ~ v28946(sK23533_VarCurr,bitIndex28)
| v28941(sK23533_VarCurr,bitIndex28)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g318,plain,
( ~ v28946(sK23533_VarCurr,bitIndex30)
| v28941(sK23533_VarCurr,bitIndex30)
| v28947(sK23533_VarCurr) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806)]) ).
cnf(g319,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex48)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex48) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g320,plain,
( ~ v26522(sK23533_VarCurr,bitIndex48)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex48) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g321,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex56)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex56) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g322,plain,
( ~ v26522(sK23533_VarCurr,bitIndex56)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex56) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g323,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex40)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex40) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g324,plain,
( ~ v26522(sK23533_VarCurr,bitIndex40)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex40) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g325,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex58)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex58) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g326,plain,
( ~ v26522(sK23533_VarCurr,bitIndex58)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex58) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g327,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex52)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex52) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g328,plain,
( ~ v26522(sK23533_VarCurr,bitIndex52)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex52) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g329,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex28)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex28) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g330,plain,
( ~ v26522(sK23533_VarCurr,bitIndex28)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex28) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g331,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex13)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex13) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g332,plain,
( ~ v26522(sK23533_VarCurr,bitIndex13)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex13) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g333,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex18)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex18) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g334,plain,
( ~ v26522(sK23533_VarCurr,bitIndex18)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex18) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g335,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex30)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex30) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g336,plain,
( ~ v26522(sK23533_VarCurr,bitIndex30)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex30) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g337,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex31)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex31) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g338,plain,
( ~ v26522(sK23533_VarCurr,bitIndex31)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex31) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g339,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex53)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex53) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g340,plain,
( ~ v26522(sK23533_VarCurr,bitIndex53)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex53) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g341,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex23)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex23) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g342,plain,
( ~ v26522(sK23533_VarCurr,bitIndex23)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex23) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g343,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex47)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex47) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g344,plain,
( ~ v26522(sK23533_VarCurr,bitIndex47)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex47) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g345,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex54)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex54) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g346,plain,
( ~ v26522(sK23533_VarCurr,bitIndex54)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex54) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g347,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex24)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex24) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g348,plain,
( ~ v26522(sK23533_VarCurr,bitIndex24)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex24) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g349,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex49)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex49) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g350,plain,
( ~ v26522(sK23533_VarCurr,bitIndex49)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex49) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g351,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex4)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex4) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g352,plain,
( ~ v26522(sK23533_VarCurr,bitIndex4)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex4) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g353,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex34)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex34) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g354,plain,
( ~ v26522(sK23533_VarCurr,bitIndex34)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex34) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g355,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex45)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex45) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g356,plain,
( ~ v26522(sK23533_VarCurr,bitIndex45)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex45) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g357,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex14)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex14) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g358,plain,
( ~ v26522(sK23533_VarCurr,bitIndex14)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex14) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g359,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex44)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex44) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g360,plain,
( ~ v26522(sK23533_VarCurr,bitIndex44)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex44) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g361,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex5)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex5) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g362,plain,
( ~ v26522(sK23533_VarCurr,bitIndex5)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex5) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g363,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex51)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex51) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g364,plain,
( ~ v26522(sK23533_VarCurr,bitIndex51)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex51) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g365,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex37)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex37) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g366,plain,
( ~ v26522(sK23533_VarCurr,bitIndex37)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex37) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g367,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex12)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex12) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g368,plain,
( ~ v26522(sK23533_VarCurr,bitIndex12)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex12) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g369,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex59)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex59) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g370,plain,
( ~ v26522(sK23533_VarCurr,bitIndex59)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex59) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g371,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex39)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex39) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g372,plain,
( ~ v26522(sK23533_VarCurr,bitIndex39)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex39) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g373,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex15)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex15) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g374,plain,
( ~ v26522(sK23533_VarCurr,bitIndex15)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex15) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g375,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex26)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex26) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g376,plain,
( ~ v26522(sK23533_VarCurr,bitIndex26)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex26) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g377,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex19)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex19) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g378,plain,
( ~ v26522(sK23533_VarCurr,bitIndex19)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex19) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g379,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex10)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex10) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g380,plain,
( ~ v26522(sK23533_VarCurr,bitIndex10)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex10) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g381,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex3)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex3) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g382,plain,
( ~ v26522(sK23533_VarCurr,bitIndex3)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex3) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g383,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex22)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex22) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g384,plain,
( ~ v26522(sK23533_VarCurr,bitIndex22)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex22) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g385,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex29)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex29) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g386,plain,
( ~ v26522(sK23533_VarCurr,bitIndex29)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex29) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g387,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex36)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex36) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g388,plain,
( ~ v26522(sK23533_VarCurr,bitIndex36)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex36) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g389,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex57)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex57) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g390,plain,
( ~ v26522(sK23533_VarCurr,bitIndex57)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex57) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g391,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex8)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex8) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g392,plain,
( ~ v26522(sK23533_VarCurr,bitIndex8)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex8) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g393,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex35)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex35) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g394,plain,
( ~ v26522(sK23533_VarCurr,bitIndex35)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex35) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g395,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex9)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex9) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g396,plain,
( ~ v26522(sK23533_VarCurr,bitIndex9)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex9) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g397,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex38)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex38) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g398,plain,
( ~ v26522(sK23533_VarCurr,bitIndex38)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex38) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g399,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex55)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex55) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g400,plain,
( ~ v26522(sK23533_VarCurr,bitIndex55)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex55) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g401,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex21)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex21) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g402,plain,
( ~ v26522(sK23533_VarCurr,bitIndex21)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex21) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g403,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex11)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex11) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g404,plain,
( ~ v26522(sK23533_VarCurr,bitIndex11)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex11) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g405,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex17)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex17) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g406,plain,
( ~ v26522(sK23533_VarCurr,bitIndex17)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex17) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g407,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex25)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex25) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g408,plain,
( ~ v26522(sK23533_VarCurr,bitIndex25)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex25) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g409,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex41)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex41) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g410,plain,
( ~ v26522(sK23533_VarCurr,bitIndex41)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex41) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g411,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex33)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex33) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g412,plain,
( ~ v26522(sK23533_VarCurr,bitIndex33)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex33) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g413,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex46)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex46) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g414,plain,
( ~ v26522(sK23533_VarCurr,bitIndex46)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex46) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g415,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex43)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex43) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g416,plain,
( ~ v26522(sK23533_VarCurr,bitIndex43)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex43) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g417,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex16)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex16) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g418,plain,
( ~ v26522(sK23533_VarCurr,bitIndex16)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex16) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g419,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex42)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex42) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g420,plain,
( ~ v26522(sK23533_VarCurr,bitIndex42)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex42) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g421,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex32)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex32) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g422,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex20)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex20) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g423,plain,
( ~ v26522(sK23533_VarCurr,bitIndex20)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex20) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g424,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex27)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex27) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g425,plain,
( ~ v26522(sK23533_VarCurr,bitIndex27)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex27) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g426,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex7)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex7) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g427,plain,
( ~ v26522(sK23533_VarCurr,bitIndex7)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex7) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g428,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex50)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex50) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g429,plain,
( ~ v26522(sK23533_VarCurr,bitIndex50)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex50) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g430,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28945(sK23533_VarCurr,bitIndex6)
| v4914(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex6) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803)]) ).
cnf(g431,plain,
( ~ v26522(sK23533_VarCurr,bitIndex6)
| sP38_aig_name(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex6) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795)]) ).
cnf(g432,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex6)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex6) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g433,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex37)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex37) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g434,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex40)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex40) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g435,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex29)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex29) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g436,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex58)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex58) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g437,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex35)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex35) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g438,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex48)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex48) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g439,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex39)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex39) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g440,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex52)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex52) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g441,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex5)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex5) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g442,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex21)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex21) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g443,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex27)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex27) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g444,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex43)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex43) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g445,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex13)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex13) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g446,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex42)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex42) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g447,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex32)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex32) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g448,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex44)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex44) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g449,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex50)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex50) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g450,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex15)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex15) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g451,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex28)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex28) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g452,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex4)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex4) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g453,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex33)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex33) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g454,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex53)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex53) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g455,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex47)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex47) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g456,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex18)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex18) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g457,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex45)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex45) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g458,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex25)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex25) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g459,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex57)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex57) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g460,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex14)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex14) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g461,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex46)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex46) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g462,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex31)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex31) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g463,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex54)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex54) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g464,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex8)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex8) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g465,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex23)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex23) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g466,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex12)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex12) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g467,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex16)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex16) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g468,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex38)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex38) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g469,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex56)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex56) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g470,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex7)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex7) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g471,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex19)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex19) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g472,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex34)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex34) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g473,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex30)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex30) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g474,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex41)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex41) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g475,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex22)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex22) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g476,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex3)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex3) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g477,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex59)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex59) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g478,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex51)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex51) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g479,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex20)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex20) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g480,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex49)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex49) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g481,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex36)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex36) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g482,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex11)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex11) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g483,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex17)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex17) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g484,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex10)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex10) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g485,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex55)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex55) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g486,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex24)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex24) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g487,plain,
( ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,bitIndex9)
| v4914(sK23533_VarCurr)
| v28945(sK23533_VarCurr,bitIndex9) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804)]) ).
cnf(g488,plain,
( ~ v28945(sK23533_VarCurr,bitIndex32)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,bitIndex32) ),
inference(ground_cnf,[],[file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : HWV108-1 : TPTP v8.1.0. Released v6.1.0.
% 0.11/0.15 % Command : satcop --statistics %s
% 0.16/0.37 % Computer : n006.cluster.edu
% 0.16/0.37 % Model : x86_64 x86_64
% 0.16/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.37 % Memory : 8042.1875MB
% 0.16/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.37 % CPULimit : 300
% 0.16/0.37 % WCLimit : 600
% 0.16/0.37 % DateTime : Thu Jun 16 21:58:41 EDT 2022
% 0.16/0.37 % CPUTime :
% 182.74/24.06 % symbols: 28867
% 182.74/24.06 % clauses: 179938
% 182.74/24.06 % start clauses: 14
% 182.74/24.06 % iterative deepening steps: 1418
% 182.74/24.06 % maximum path limit: 2
% 182.74/24.06 % literal attempts: 97903571
% 182.74/24.06 % depth failures: 95486156
% 182.74/24.06 % regularity failures: 91366
% 182.74/24.06 % tautology failures: 80092
% 182.74/24.06 % reductions: 165164
% 182.74/24.06 % extensions: 97718745
% 182.74/24.06 % SAT variables: 1728376
% 182.74/24.06 % SAT clauses: 1457470
% 182.74/24.06 % WalkSAT solutions: 1457469
% 182.74/24.06 % CDCL solutions: 0
% 182.74/24.06 % SZS status Unsatisfiable for theBenchmark
% 182.74/24.06 % SZS output start ListOfCNF for theBenchmark
% See solution above
%------------------------------------------------------------------------------